search

HoTT / Coq-HoTT

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

make opposite Is1Natural definitionally involutive #1969

Closed Alizter closed 1 month ago

Alizter commented 1 month ago

Carry out the suggestion in #1961. This will allow for more of the data of a monoidal category or (2,1)-category to be definitionally involutive.

Alizter commented 1 month ago

Turns out we don't get definitionally involutive associators and unitors since we are taking inverses there. I have updated the tests to show the current state of the opposite involutions. This isn't strictly needed for #1929 anyway.

jdchristensen commented 1 month ago

LGTM.