← Feed

Posts

• View post

  My typical interaction with books and articles on model theory: them: 1+3=4 me: yup them: Rubik's cube forms a group me: u-huh them: polynomials form a ring me: yeah yeah them: let's call an entity 𝔚-sammlungswürdigkeit if it's a set equipped with infinite functions and infinite infinitary relations me: ... what kind of letter is that supposed to be now? them: now, since we have a notion of 𝔉-zusammengehörigkeit, we can write down 𝔉 ⊨ ∀x.∃y.∃z.(ζ(y) ∧ ∀w.ϕ(w,z,x)) and ca...

• View post

  Came to the conclusion that the difference between Markov categories and Simpson's atomic sheaf framework (as illustrated on FinInj/FinSur) can be reduced to the difference between geometric and topological descriptions. The former track probability as a measure, while the latter tracks a more abstract independence structure. That is, if we want a synthetic type theory for probability/statistics, it makes sense to start by formalizing Simpson's framework in homotopy type theory.

• View post

  Since we're on the subject, I'm curious if there's a resource that explains the practical difference between using the Bishop style (equivalence with Fin) and the Kuratowski style (list/tree quotient) for finite sets. Donnacha Kidney covers this topic in his master's thesis, but his approach is somewhat one-sided—he reduces the Kuratowski style to the Bishop style. For decidable types, the two approaches seem to be completely equivalent. I’m trying to figure out...

• View post

  @glocq I did a lot of Idris&Coq before, for the last 3 years it's mostly Cubical Agda

• View post

  Wrote up a proof of the statement 'AC implies LEM', as described by Valery Isaev: https://gist.github.com/clayrat/80f2e048831e6829a49d5cb3843b2c7d

• View post

  Both in modernity and in traditional society, socialization has always been built upon the internalization of external rules. In religion, this was expressed through bodily rituals that outwardly barely engaged consciousness. Modernity, by contrast, demands that an individual anchor themselves to "fundamental questions" and form an opinion on them. However, the very capacity to detach oneself from ritual emerges at the junction of eras - when motivation shifts from arranging li...

• View post

  Which interesting HA proofs can I run thorough the Dialectica translations to get non-trivial System T programs? I can do somewhat boring stuff like forall x. exists y. y = 2x, but is there something cooler and still compact?