search

mikeshulman / Coq-HoTT

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

Sum is a functor #15

Closed mikeshulman closed 4 years ago

tslilc commented 4 years ago

Except for some breakage about universe lengths in PropResizing/Nat.v, this is done? ¯\(ツ)/¯