def SSet.coherentIso.equivFun {n : ℕ} : coherentIso.obj (Opposite.op { len := n }) ≃ (Fin (n + 1) → CategoryTheory.WalkingIso)

Since the morphisms in WalkingIso do not carry information, an n-simplex of coherentIso is equivalent to an (n + 1)-vector of the objects of WalkingIso.

Equations

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

@[implicit_reducible]

instance SSet.coherentIso.instDecidableEqObjOppositeSimplexCategoryOpMk_infinityCosmos (n : ℕ) : DecidableEq (coherentIso.obj (Opposite.op { len := n }))

Since Fin 2 has decidable equality, the simplices of coherentIso have decidable equality as well.

Equations

• SSet.coherentIso.instDecidableEqObjOppositeSimplexCategoryOpMk_infinityCosmos n x✝¹ x✝ = decidable_of_iff (SSet.coherentIso.equivFun x✝¹ = SSet.coherentIso.equivFun x✝) ⋯

def SSet.coherentIso.src : stdSimplex.obj { len := 0 } ⟶ coherentIso

The inclusion of the source vertex of CoherentIso.

Equations

• SSet.coherentIso.src = SSet.yonedaEquiv.symm SSet.coherentIso.x₀

def SSet.coherentIso.tgt : stdSimplex.obj { len := 0 } ⟶ coherentIso

The inclusion of the target vertex of CoherentIso.

Equations

• SSet.coherentIso.tgt = SSet.yonedaEquiv.symm SSet.coherentIso.x₁