instIsMonoidalUnitTransportedEquivalenceTransported

English

The unit natural transformation underlying the transported equivalence is monoidal. In other words, the unit of the transported equivalence is a monoidal natural transformation.

Русский

Единичное натуральное преобразование переносимой эквивалентности обладает моноидальной структурой; единичный преобразователь переносной эквивалентности моноидален.

LaTeX

$$$\\text{NatTrans.IsMonoidal}((\\mathrm{equivalenceTransported}\; e).\\mathrm{unit})$.$$

Lean4

/-- The unit isomorphism upgrades to a monoidal isomorphism. -/
instance : NatTrans.IsMonoidal (equivalenceTransported e).unit :=
  inferInstanceAs (NatTrans.IsMonoidal (equivalenceTransported e).symm.counitIso.inv)

Похожие утверждения