This is the free-living isomorphism as a category with objects called
zero
and one
. Perhaps these should have different names?
- zero : WalkingIso
- one : WalkingIso
Instances For
The free isomorphism is the codiscrete category on two objects. Can we make this a special case of the other definition?
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.WalkingIso.toIso
{C : Type u'}
[Category.{v', u'} C]
(F : Functor WalkingIso C)
:
Functors out of WalkingIso
define isomorphisms in the target category.
Equations
- CategoryTheory.WalkingIso.toIso F = { hom := F.map PUnit.unit, inv := F.map PUnit.unit, hom_inv_id := ⋯, inv_hom_id := ⋯ }
From an isomorphism in a category, one can build a functor out of WalkingIso
to
that category.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.