Skip to main content
11 votes
Accepted

What is realignment and is it useful in non-univalent theories?

This is a very good question. What is realignment for? One application of realignment that is particularly useful is to construct a cumulative hierarchy of universes; what cumulativity means in the &...
Jonathan Sterling's user avatar
4 votes

What is the intuition behind the `Glue` type in Cubical Type Theories

I would say Glue types are the "in-between" part of a path equality. For instance, take the Booleans. We can construct a type $$\mathsf{Glue}^i_{\color{brown}{\mathbb B}}\begin{cases} (i=0) \...
Trebor's user avatar
  • 4,025
4 votes
Accepted

Is there any universe polymorphic version of univalence?

At least in papers on cubical type theory, 'respecting equivalence' is somewhat independent of universes. There is a judgmental notion of paths: $$Γ,i ⊢ T\ \mathsf{type} \\ Γ,i ⊢ t : T$$ The top being ...
Dan Doel's user avatar
  • 982

Only top scored, non community-wiki answers of a minimum length are eligible