Commit 2021-08-27 07:04 fe13f030

View on Github →

feat(category_theory/structured_arrow): Duality between structured and costructured arrows (#8807) This PR formally sets up the duality of structured and costructured arrows as equivalences of categories. Unfortunately, the code is a bit repetitive, as the four functors introduced all follow a similar pattern, which I wasn't able to abstract out. Suggestions are welcome!

Estimated changes

Modified src/category_theory/structured_arrow.lean

added def category_theory.costructured_arrow.to_structured_arrow'

added def category_theory.costructured_arrow.to_structured_arrow

added def category_theory.costructured_arrow_op_equivalence

added def category_theory.structured_arrow.to_costructured_arrow'

added def category_theory.structured_arrow.to_costructured_arrow

added def category_theory.structured_arrow_op_equivalence