inductive CategoryTheory.WalkingIso : Type u

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

instance CategoryTheory.WalkingIso.instCategory : Category.{0, u_1} WalkingIso

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) : F.obj zero ≅ F.obj one

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 := ⋯ }

def CategoryTheory.WalkingIso.fromIso {C : Type u'} [Category.{v', u'} C] {X Y : C} (e : X ≅ Y) : Functor WalkingIso C

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.

def CategoryTheory.WalkingIso.equiv {C : Type u'} [Category.{v', u'} C] : Functor WalkingIso C ≃ (X : C) × (Y : C) × (X ≅ Y)

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.WalkingIso.coev (i : WalkingIso) : Functor (Fin 1) WalkingIso

Equations

• i.coev = CategoryTheory.ComposableArrows.mk₀ i

def SSet.coherentIso : SSet

Equations

• SSet.coherentIso = CategoryTheory.nerve CategoryTheory.WalkingIso

def SSet.coherentIso.pt (i : CategoryTheory.WalkingIso) : stdSimplex.obj (SimplexCategory.mk 0) ⟶ coherentIso

Equations

• SSet.coherentIso.pt i = (SSet.coherentIso.yonedaEquiv (SimplexCategory.mk 0)).symm i.coev