English
Given a 2-simplex φ and compatible edges f01, f12, f02 with φ, one obtains a term of type HoRel₂ between the corresponding arrows in the quotient.
Русский
Пусть дано 2-угольник φ и совместимые рёбра f01, f12, f02, удовлетворяющие φ; тогда получаем термин типа HoRel₂ между соответствующими стрелками в факторной категории.
LaTeX
$$$HoRel_2\\big(\\_,\\_,\\_,\\_\\big) : \\text{HoRel}_2(\\dots)$$$
Lean4
/-- A 2-simplex whose faces are identified with certain arrows in `OneTruncation₂ V` defines
a term of type `HoRel₂` between those arrows. -/
theorem mk' {V : SSet.Truncated 2} (φ : V _⦋2⦌₂) {X₀ X₁ X₂ : OneTruncation₂ V} (f₀₁ : X₀ ⟶ X₁) (f₁₂ : X₁ ⟶ X₂)
(f₀₂ : X₀ ⟶ X₂) (h₀₁ : f₀₁.edge = V.map (δ₂ 2).op φ) (h₁₂ : f₁₂.edge = V.map (δ₂ 0).op φ)
(h₀₂ : f₀₂.edge = V.map (δ₂ 1).op φ) :
HoRel₂ _ _ (Quot.mk _ (Quiver.Hom.toPath f₀₂)) (Quot.mk _ ((Quiver.Hom.toPath f₀₁).comp (Quiver.Hom.toPath f₁₂))) :=
by
obtain rfl : X₀ = ev0₂ φ :=
by
rw [← f₀₂.src_eq, h₀₂, ← FunctorToTypes.map_comp_apply, ← op_comp]
rfl
obtain rfl : X₁ = ev1₂ φ :=
by
rw [← f₀₁.tgt_eq, h₀₁, ← FunctorToTypes.map_comp_apply, ← op_comp]
rfl
obtain rfl : X₂ = ev2₂ φ :=
by
rw [← f₁₂.tgt_eq, h₁₂, ← FunctorToTypes.map_comp_apply, ← op_comp]
rfl
obtain rfl : f₀₁ = ev01₂ φ := by ext; assumption
obtain rfl : f₁₂ = ev12₂ φ := by ext; assumption
obtain rfl : f₀₂ = ev02₂ φ := by ext; assumption
constructor
