HoTT / Coq-HoTT

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

more opposite tests #1961

Closed Alizter closed 1 month ago

Alizter commented 1 month ago

We add more tests showing functors and now bifunctors are definitionally involutive. We also show that opposite natural transformations do not have this behaviour since the proof of naturality is inverted. I think it might be time to consider adding redundant information to Is1Natural so that we also keep the inverted naturality around like we did for cat_assoc_opp.