:: YONEDA_1 semantic presentation

begin

definition
let A be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
func EnsHom A -> ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) equals :: YONEDA_1:def 1
 Ens (Hom A : ( ( ) ( ) CatStr ) ) : ( ( ) ( ) set ) : ( ( non empty non void strict ) ( non empty non void V55() strict ) CatStr ) ;
end;

theorem :: YONEDA_1:1
for A being ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category)
for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for m1, m2 being ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) st cod m1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) = dom m2 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) & [[(dom m1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,(cod m1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V1() ) Element of the carrier of K210((EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) ,f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ] : ( ( ) ( V1() ) set ) = m1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) & [[(dom m2 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,(cod m2 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V1() ) Element of the carrier of K210((EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) ,g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ] : ( ( ) ( V1() ) set ) = m2 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) holds
[[(dom m1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,(cod m2 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V1() ) Element of the carrier of K210((EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) ,(g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) * f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) ] : ( ( ) ( V1() ) set ) = m2 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) (*) m1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier' of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ;

definition
let A be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
let a be ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ;
func <|a,?> -> ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Functor of A : ( ( ) ( ) CatStr ) , EnsHom A : ( ( ) ( ) CatStr ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) equals :: YONEDA_1:def 2
 hom?- a : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined Maps (Hom A : ( ( ) ( ) CatStr ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Element of K32(K33( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ,(Maps (Hom A : ( ( ) ( ) CatStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: YONEDA_1:2
for A being ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category)
for f being ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) holds <|(cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) is_naturally_transformable_to <|(dom f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ;

definition
let A be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
let f be ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ;
func <|f,?> -> ( ( ) ( non empty Relation-like the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) natural_transformation of <|(cod f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Functor of A : ( ( ) ( ) CatStr ) , EnsHom A : ( ( ) ( ) CatStr ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ,<|(dom f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Functor of A : ( ( ) ( ) CatStr ) , EnsHom A : ( ( ) ( ) CatStr ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ) means :: YONEDA_1:def 3
 for o being ( ( ) ( ) Object of ( ( ) ( ) set ) ) holds it : ( ( Function-like quasi_total ) ( Relation-like f : ( ( ) ( ) set ) -defined A : ( ( ) ( ) CatStr ) -valued Function-like quasi_total ) Element of K32(K33(f : ( ( ) ( ) set ) ,A : ( ( ) ( ) CatStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . o : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Morphism of <|(cod f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Functor of A : ( ( ) ( ) CatStr ) , EnsHom A : ( ( ) ( ) CatStr ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) . b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,<|(dom f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Functor of A : ( ( ) ( ) CatStr ) , EnsHom A : ( ( ) ( ) CatStr ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) . b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) = [[(Hom ((cod f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of K32( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,(Hom ((dom f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of K32( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ] : ( ( ) ( V1() ) set ) ,(hom (f : ( ( ) ( ) set ) ,(id o : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like quasi_total ) ( Relation-like Hom ((cod f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,(dom (id b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Hom ((dom f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,(cod (id b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of K32(K33((Hom ((cod f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,(dom (id b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) )) : ( ( ) ( ) Element of K32( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,(Hom ((dom f : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,(cod (id b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) )) : ( ( ) ( ) Element of K32( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ] : ( ( ) ( V1() ) set ) ;
end;

theorem :: YONEDA_1:3
for A being ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category)
for f being ( ( ) ( ) Element of the carrier' of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) holds [[<|(cod f : ( ( ) ( ) Element of the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ,<|(dom f : ( ( ) ( ) Element of the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ] : ( ( ) ( V1() ) set ) ,<|f : ( ( ) ( ) Element of the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) natural_transformation of <|(cod b2 : ( ( ) ( ) Element of the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ,<|(dom b2 : ( ( ) ( ) Element of the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ) ] : ( ( ) ( V1() ) set ) is ( ( ) ( ) Element of the carrier' of (Functors (A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) ;

definition
let A be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
func Yoneda A -> ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (Functors (A : ( ( ) ( ) CatStr ) ,(EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Contravariant_Functor of A : ( ( ) ( ) CatStr ) , Functors (A : ( ( ) ( ) CatStr ) ,(EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) means :: YONEDA_1:def 4
 for f being ( ( ) ( ) Morphism of ( ( ) ( ) set ) ) holds it : ( ( ) ( ) set ) . f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier' of (Functors (A : ( ( ) ( ) CatStr ) ,(EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) = [[<|(cod f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Functor of A : ( ( ) ( ) CatStr ) , EnsHom A : ( ( ) ( ) CatStr ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ,<|(dom f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Functor of A : ( ( ) ( ) CatStr ) , EnsHom A : ( ( ) ( ) CatStr ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ] : ( ( ) ( V1() ) set ) ,<|f : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) natural_transformation of <|(cod b1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Functor of A : ( ( ) ( ) CatStr ) , EnsHom A : ( ( ) ( ) CatStr ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ,<|(dom b1 : ( ( ) ( ) Morphism of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) ,?> : ( ( ) ( non empty Relation-like the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier' of (EnsHom A : ( ( ) ( ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Functor of A : ( ( ) ( ) CatStr ) , EnsHom A : ( ( ) ( ) CatStr ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ) ] : ( ( ) ( V1() ) set ) ;
end;

definition
let A, B be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
let F be ( ( ) ( non empty Relation-like the carrier' of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of B : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,B : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ;
let c be ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ;
func F . c -> ( ( ) ( ) Object of ( ( ) ( ) set ) ) equals :: YONEDA_1:def 5
(Obj F : ( ( Function-like quasi_total ) ( Relation-like B : ( ( ) ( ) set ) -defined A : ( ( ) ( ) CatStr ) -valued Function-like quasi_total ) Element of K32(K33(B : ( ( ) ( ) set ) ,A : ( ( ) ( ) CatStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) -defined the carrier of B : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V17( the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) quasi_total ) Element of K32(K33( the carrier of A : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) , the carrier of B : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( Function-like quasi_total ) ( Relation-like B : ( ( ) ( ) set ) -defined A : ( ( ) ( ) CatStr ) -valued Function-like quasi_total ) Element of K32(K33(B : ( ( ) ( ) set ) ,A : ( ( ) ( ) CatStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of B : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: YONEDA_1:4
for A being ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category)
for F being ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , Functors (A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) st Obj F : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K32(K33( the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) is one-to-one & F : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) is faithful holds
F : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) is one-to-one ;

definition
let C, D be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
let T be ( ( ) ( non empty Relation-like the carrier' of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of D : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,D : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ;
attr T is faithful means :: YONEDA_1:def 6
 for c, c9 being ( ( ) ( ) Object of ( ( ) ( ) set ) ) st Hom (c : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,c9 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier' of C : ( ( ) ( ) CatStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ) set ) holds
for f1, f2 being ( ( ) ( ) Morphism of c : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,c9 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) st T : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( ) ( ) CatStr ) -valued Function-like quasi_total ) Element of K32(K33(D : ( ( ) ( ) set ) ,C : ( ( ) ( ) CatStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . f1 : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier' of D : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = T : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( ) ( ) CatStr ) -valued Function-like quasi_total ) Element of K32(K33(D : ( ( ) ( ) set ) ,C : ( ( ) ( ) CatStr ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . f2 : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier' of D : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
f1 : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) = f2 : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: YONEDA_1:5
for A being ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category)
for F being ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , Functors (A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) st Obj F : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K32(K33( the carrier of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) , the carrier of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) is one-to-one & F : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) is faithful holds
F : ( ( ) ( non empty Relation-like the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) , Functors (b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,(EnsHom b1 : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) is one-to-one ;

registration
let A be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
cluster Yoneda A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty Relation-like the carrier' of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ,(EnsHom A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) , Functors (A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ,(EnsHom A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) -> faithful ;
end;

registration
let A be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
cluster Yoneda A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty Relation-like the carrier' of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ,(EnsHom A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) quasi_total faithful ) Contravariant_Functor of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) , Functors (A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ,(EnsHom A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) -> one-to-one ;
end;

definition
let C, D be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
let T be ( ( ) ( non empty Relation-like the carrier' of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of D : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,D : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) ;
attr T is full means :: YONEDA_1:def 7
 for c, c9 being ( ( ) ( ) Object of ( ( ) ( ) set ) ) st Hom ((T : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K32(K33(D : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . c9 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Object of ( ( ) ( ) set ) ) ,(T : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K32(K33(D : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Object of ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier' of D : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ) set ) holds
for g being ( ( ) ( ) Morphism of T : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K32(K33(D : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . c9 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Object of ( ( ) ( ) set ) ) ,T : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K32(K33(D : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Object of ( ( ) ( ) set ) ) ) holds
( Hom (c : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,c9 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier' of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ) set ) & ex f being ( ( ) ( ) Morphism of c : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,c9 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) st g : ( ( ) ( ) Morphism of T : ( ( ) ( non empty Relation-like the carrier' of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of D : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,D : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) . b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,T : ( ( ) ( non empty Relation-like the carrier' of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -defined the carrier' of D : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) -valued Function-like V17( the carrier' of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) : ( ( ) ( non empty ) set ) ) quasi_total ) Contravariant_Functor of C : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ,D : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) . b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) = T : ( ( Function-like quasi_total ) ( Relation-like D : ( ( ) ( ) set ) -defined C : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K32(K33(D : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . f : ( ( ) ( ) Morphism of b1 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) Object of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier' of D : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
end;

registration
let A be ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ;
cluster Yoneda A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty Relation-like the carrier' of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -defined the carrier' of (Functors (A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ,(EnsHom A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) )) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one V17( the carrier' of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) : ( ( ) ( non empty ) set ) ) quasi_total faithful ) Contravariant_Functor of A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) , Functors (A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ,(EnsHom A : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) CatStr ) ) : ( ( non empty non void Category-like V68() V69() V70() with_identities ) ( non empty non void V55() Category-like V68() V69() V70() with_identities ) Category) ) : ( ( non empty non void strict Category-like V68() V69() V70() with_identities ) ( non empty non void V55() strict Category-like V68() V69() V70() with_identities ) CatStr ) ) -> full ;
end;