HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k stars 185 forks source link

Prove that the universal property of pullback is an equivalence #1966

Closed MintChocoManju closed 1 month ago

MintChocoManju commented 1 month ago

I couldn't find this proof anywhere in the library, although this result maybe of interest somewhere else.