instConcreteCategoryFrameHomCarrier

English

Frm is a concrete category with FrameHom as morphisms; the homs are given by FrameHom and the carrier is the underlying type.

Русский

Frm является конкретной категорией с Morphisms FrameHom; гомоморфизмы задаются FrameHom, носитель — базовый тип.

LaTeX

$$$ \\text{Frm is a concrete category with } \\text{FrameHom} \\text{ as morphisms} $$$

Lean4

instance : ConcreteCategory Frm (FrameHom · ·) where
  hom := Hom.hom'
  ofHom := Hom.mk

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