Lean4
/-- The canonical transition map `(Uᵢ ×[Z] Y) ×[X] Uⱼ ⟶ (Uⱼ ×[Z] Y) ×[X] Uᵢ` given by the fact
that pullbacks are associative and symmetric. -/
def t (i j : 𝒰.I₀) : v 𝒰 f g i j ⟶ v 𝒰 f g j i :=
by
have : HasPullback (pullback.snd _ _ ≫ 𝒰.f i ≫ f) g := hasPullback_assoc_symm (𝒰.f j) (𝒰.f i) (𝒰.f i ≫ f) g
have : HasPullback (pullback.snd _ _ ≫ 𝒰.f j ≫ f) g := hasPullback_assoc_symm (𝒰.f i) (𝒰.f j) (𝒰.f j ≫ f) g
refine (pullbackSymmetry ..).hom ≫ (pullbackAssoc ..).inv ≫ ?_
refine ?_ ≫ (pullbackAssoc ..).hom ≫ (pullbackSymmetry ..).hom
refine pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) ?_ ?_
· rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id]
· rw [Category.comp_id, Category.id_comp]
