Open txa opened 2 months ago
In this chapter we give up on agnosticism and admit non-propositional equalities. This allows us to talk about univalent categories with the analogy to the move from preorders to partial orders. Details need to be sketched on on wb first.
In this chapter we give up on agnosticism and admit non-propositional equalities. This allows us to talk about univalent categories with the analogy to the move from preorders to partial orders. Details need to be sketched on on wb first.