English
The natural equivalence between CostructuredArrow (S.prod S') (T, T') and CostructuredArrow S T × CostructuredArrow S' T'.
Русский
Естественная эквалентность между CostructuredArrow (S.prod S') (T, T') и CostructuredArrow S T × CostructuredArrow S' T'.
LaTeX
$$$$ \\text{prodEquivalence} : \\text{CostructuredArrow} (S \\prod S') (T,T') \\simeq \\text{CostructuredArrow} (S T) \\times \\text{CostructuredArrow} (S' T'). $$$$
Lean4
/-- The natural equivalence
`CostructuredArrow (S.prod S') (T, T') ≌ CostructuredArrow S T × CostructuredArrow S' T'`. -/
@[simps]
def prodEquivalence : CostructuredArrow (S.prod S') (T, T') ≌ CostructuredArrow S T × CostructuredArrow S' T'
where
functor := CostructuredArrow.prodFunctor S S' T T'
inverse := CostructuredArrow.prodInverse S S' T T'
unitIso := NatIso.ofComponents (fun f => Iso.refl _) (by simp)
counitIso := NatIso.ofComponents (fun f => Iso.refl _) (by simp)
