mikeshulman / Coq-HoTT

Homotopy type theory
http://homotopytypetheory.org/
Other
12 stars 4 forks source link

IsGraph? #29

Closed mikeshulman closed 4 years ago

mikeshulman commented 4 years ago

Consider defining IsGraph (or maybe Is0Coh0Cat?) to have a Hom but no identities or composition yet. A 0-coherent 1-functor, and a 1-natural transformation, can be defined between these alone, and we use such things when talking about diagrams and (co)limits over graphs (#27).