idmap is a functor between Type and Type

mikeshulman / Coq-HoTT

Homotopy type theory

http://homotopytypetheory.org/

Other

12 stars 4 forks source link

Closed Alizter closed 4 years ago

Alizter commented 4 years ago

Should this go in WildCat/Type?

mikeshulman commented 4 years ago

Well, idmap is actually a functor from any category to itself.