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'}
[CategoryTheory.Category.{v', u'} C]
(F : CategoryTheory.Functor CategoryTheory.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 := ⋯ }
Instances For
def
CategoryTheory.WalkingIso.fromIso
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{X : C}
{Y : C}
(e : X ≅ Y)
:
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.
Instances For
def
CategoryTheory.WalkingIso.equiv
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
:
CategoryTheory.Functor CategoryTheory.WalkingIso C ≃ (X : C) × (Y : C) × (X ≅ Y)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- i.coev = CategoryTheory.ComposableArrows.mk₀ i
Instances For
Instances For
Equations
- SSet.coherentIso.pt i = (SSet.coherentIso.yonedaEquiv (SimplexCategory.mk 0)).symm i.coev