Description: The "embedding functor" from the category of sets into the category of
extensible structures which sends each set to an extensible structure
consisting of the base set slot only is an embedding. According to
definition 3.27 (1) of Adamek p. 34, a functor "F is called an
embedding provided that F is injective on morphisms", or according to
remark 3.28 (1) in Adamek p. 34, "a functor is an embedding if and
only if it is faithful and injective on objects". (Contributed by AV, 31-Mar-2020)
Ref
Expression
Hypotheses
funcsetcestrc.s
|- S = ( SetCat ` U )
funcsetcestrc.c
|- C = ( Base ` S )
funcsetcestrc.f
|- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )
funcsetcestrc.u
|- ( ph -> U e. WUni )
funcsetcestrc.o
|- ( ph -> _om e. U )
funcsetcestrc.g
|- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )