Commit 2020-08-15 20:41 2e890e61

feat(category_theory/comma): constructing isos in the comma,over,under cats (#3797) Constructors to give isomorphisms in comma, over and under categories - essentially these just let you omit checking one of the commuting squares using the fact that the components are iso and the other square works.