Bartosz MilewskiAnother blog post in the HoTT series.
https://bartoszmilewski.com/2026/03/10/the-axiom-of-univalence/
https://bartoszmilewski.com/2026/03/10/the-axiom-of-univalence/
Tom de Jong@BartoszMilewski Maybe you already know this, but what you wrote is not quite the univalence axiom, see e.g. Section 3 of https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.6/LIPIcs.TYPES.2017.6.pdf
@de_Jong_Tom
What am I missing?
It looks like my definition (which is Axiom 2.10.3 in the HoTT book) is Def 3.2 in the paper you're citing.
I used an alternative definition of equivalence: 2.4.10 in the HoTT book.
@BartoszMilewski You're postulating that there is *some* equivalence, not that the canonical map idtoeqv (that sends refl to the identity equivalence) is an equivalence. So what you have is Def 3.3 ("naive univalence") in that paper. The difference between the two is precisely Theorem 3.5.
Aside: Note that the "proper" univalence axiom is a property, i.e. the type that expresses it is a proposition, while the naive univalence axiom is not (I think — at least not obviously).
@de_Jong_Tom
I see. The word "hence" is very meaningful here. To invert this you need the computation rule.
I see. The word "hence" is very meaningful here. To invert this you need the computation rule.
Maxime Augier@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 ?
@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.
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.
@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 ?
@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.
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.