All Questions
Tagged with category-theory univalence
1
question
10
votes
1
answer
290
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 ...
- 4,025