Mastodawn

Another blog post in the HoTT series.
https://bartoszmilewski.com/2026/03/10/the-axiom-of-univalence/

The Axiom of Univalence

Previously: Modeling Identity Types. On first viewing, the identity type seems odd. Does it make sense to replace the traditional yes/no equality predicate with an elaborate type of equality proofs…

Bartosz Milewski's Programming Cafe

Show thread

Maxime Augier Mar 11

@BartoszMilewski I'm used to Haskell GADTs enforcing, I quote, "The result type of each constructor must begin with the type constructor being defined".

Intuitively, I'd say this is required to keep pattern matching sound and/or manageable.

What is happening here with your definition of loop ? Do you have to give up pattern matching on ≡ ? And what is the significance of `loop` appearing in the definition of S1 ? Could we put it somewhere else ?

Show thread

Bartosz Milewski Mar 11

@max
Pattern matching is used to define the "mapping out" of a type. In type theory it's called a recursor. Here's a recursor for the circle. I'll explain the syntax.
```
S¹-rec : {A : Type ℓ}
→ (a : A)
→ a ≡ a
→ S¹ → A
S¹-rec a l base = a
S¹-rec a l (loop i) = l i
```
In order to define the mapping out, S¹ → A, from the circle to some type A, you have to provide a value a : A and a path a ≡ a. So, yes, you pattern-match on equality. This is analogous to the mapping out of a Bool, where you provide values for True and False. Pattern matchin is just a convenient sytax for that.

Show thread

Maxime Augier Mar 13

@BartoszMilewski I guess I was more wondering about the recursor for the equality type, if there is such a thing. Or alternatively, what would prevent me from writing something like:

```
data Bad : Type where
base0: Bad
base1: Bad
loop: base0 ≡ base1

bad_f : Bad -> Bool
bad_f base0 = True
bad_f base1 = False
bad_f loop = ???
```

and use congruence over bad_f to prove that True ≡ False. Wouldn't that be a problem ?

Show thread

Bartosz Milewski

@max
The recursor for equality is the J-rule:
```
J : {A : Set}
(D : (x y : A) → x ≡ y → Set) →
((x : A) → D x x refl) →
(x y : A) (p : x ≡ y) → D x y p
J D p x .x refl = p x
```
The recursor for the circle is:
```
S¹-rec : {A : Type ℓ}
→ (a : A)
→ a ≡ a
→ S¹ → A
S¹-rec a l base = a
S¹-rec a l (loop i) = l i
```
If you want to use a recursor for Bad, you'd have to provide the proof that True ≡ False.