instIsEquivalenceMonoOverRepresentative

English

The representative functor is an equivalence; Subobject X is categorically the same as MonoOver X via representative.

Русский

Функтор representative является эквивалентностью; Subobject X и MonoOver X эквивалентны через representative.

LaTeX

$$$\\text{representative} : Subobject(X) \\to MonoOver(X) \\text{ is an equivalence.}$$$

Lean4

instance : (representative (X := X)).IsEquivalence :=
  (equivMonoOver X).isEquivalence_functor

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