search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
25 stars 5 forks source link

Identity Systems #58

Open maxsnew opened 9 months ago

maxsnew commented 9 months ago

The cubical library implements univalence by saying idToEquiv is an equivalence but a more ergonomic approach is in terms of Identity systems, e.g., https://1lab.dev/1Lab.Path.IdentitySystem.html . It would be nice if someone could port that formulation to cubical