As of May 31, 2023, we have updated our Code of Conduct.

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).

Filter by
Sorted by
Tagged with
9 votes
1 answer

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 "...
Russoul's user avatar
  • 183
10 votes
1 answer

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 ...
Trebor's user avatar
  • 3,490
8 votes
1 answer

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 ...
KANG Rongji's user avatar