Questions tagged [univalence]
A bundle is said to be univalent if every other bundle is a pullback of it in at most one way (up to homotopy). (from nLab).
3
questions
9
votes
1
answer
175
views
What is the intuition behind the `Glue` type in Cubical Type Theories
I have some clues regarding Glue based on a paper here and the accepted answer here.
The first resource says that Glue "...
- 183
10
votes
1
answer
214
views
What is realignment and is it useful in non-univalent theories?
From my rough understanding, an (external/internal) realignment property says that given a type $A$, a proposition $p : \Omega$, and a partial isomorph $B : p \to \sum_{A'} A' \cong A$, we can extend ...
- 3,490
8
votes
1
answer
194
views
Is there any universe polymorphic version of univalence?
People would say in univalent type theory, anything you defined for types should respect equivalence since univalence told you equivalence equivalent to equality. But that's not correct. Only ...
- 660