agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
359 stars 67 forks source link

Simplify HomReasoning sequences for Comma categories #376

Closed Taneb closed 1 year ago

Taneb commented 1 year ago

I think these uses of morphism reasoning are a closer semantic match to the pen-and-paper proofs