English
The canonical terminal comparison map is an isomorphism.
Русский
Каноническое отображение сравнения терминальных объектов является изоморфизмом.
LaTeX
$$$\\operatorname{terminalComparison}(G) \\; \\text{is an iso.}$$$
Lean4
theorem iff_of_equiv : sq₁.IsPullback ↔ sq₂.IsPullback :=
by
rw [← IsPullback.map_iff sq₁ uliftFunctor.{max u v}, ← IsPullback.map_iff sq₂ uliftFunctor.{max u v}]
refine
iff_of_iso
(Square.isoMk (((Equiv.trans Equiv.ulift e₁).trans Equiv.ulift.symm).toIso)
(((Equiv.trans Equiv.ulift e₂).trans Equiv.ulift.symm).toIso)
(((Equiv.trans Equiv.ulift e₃).trans Equiv.ulift.symm).toIso)
(((Equiv.trans Equiv.ulift e₄).trans Equiv.ulift.symm).toIso) ?_ ?_ ?_ ?_)
all_goals ext; apply ULift.down_injective
· simpa [types_comp, uliftFunctor_map] using congrFun comm₁₂ _
· simpa [types_comp, uliftFunctor_map] using congrFun comm₁₃ _
· simpa [types_comp, uliftFunctor_map] using congrFun comm₂₄ _
· simpa [types_comp, uliftFunctor_map] using congrFun comm₃₄ _
