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: CategoryTheory.WalkingIso
• one: CategoryTheory.WalkingIso

instance CategoryTheory.WalkingIso.instCategory : CategoryTheory.Category.{0, u_1} CategoryTheory.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'} [CategoryTheory.Category.{v', u'} C] (F : CategoryTheory.Functor CategoryTheory.WalkingIso C) : F.obj CategoryTheory.WalkingIso.zero ≅ F.obj CategoryTheory.WalkingIso.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'} [CategoryTheory.Category.{v', u'} C] {X Y : C} (e : X ≅ Y) : CategoryTheory.Functor CategoryTheory.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'} [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.

def CategoryTheory.WalkingIso.coev (i : CategoryTheory.WalkingIso) : CategoryTheory.Functor (Fin 1) CategoryTheory.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) : SSet.standardSimplex.obj (SimplexCategory.mk 0) ⟶ SSet.coherentIso

Equations

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