:: FUNCTOR1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster non empty transitive with_units reflexive AltCatStr ;
existence
ex b1 being non empty AltCatStr st
( b1 is transitive & b1 is with_units & b1 is reflexive )
proof end;
end;

registration
let A be non empty reflexive AltCatStr ;
cluster non empty reflexive SubCatStr of A;
existence
ex b1 being SubCatStr of A st
( not b1 is empty & b1 is reflexive )
proof end;
end;

registration
let C1, C2 be non empty reflexive AltCatStr ;
let F be feasible FunctorStr of C1,C2;
let A be non empty reflexive SubCatStr of C1;
cluster F | A -> feasible ;
coherence
F | A is feasible
;
end;

theorem :: FUNCTOR1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds id X is onto
proof end;

theorem :: FUNCTOR1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B, C being non empty Subset of A
for D being non empty Subset of B st C = D holds
incl C = (incl B) * (incl D)
proof end;

theorem Th3: :: FUNCTOR1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for f being Function of X,Y st f is bijective holds
f " is Function of Y,X
proof end;

theorem :: FUNCTOR1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )
proof end;

theorem Th5: :: FUNCTOR1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)
proof end;

theorem Th6: :: FUNCTOR1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty AltCatStr
for F being FunctorStr of A,B st F is bijective holds
( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )
proof end;

theorem Th7: :: FUNCTOR1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is one-to-one & G is one-to-one holds
G * F is one-to-one
proof end;

theorem Th8: :: FUNCTOR1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is faithful & G is faithful holds
G * F is faithful
proof end;

theorem Th9: :: FUNCTOR1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is onto & G is onto holds
G * F is onto
proof end;

theorem Th10: :: FUNCTOR1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is full & G is full holds
G * F is full
proof end;

theorem Th11: :: FUNCTOR1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is injective & G is injective holds
G * F is injective
proof end;

theorem Th12: :: FUNCTOR1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is surjective & G is surjective holds
G * F is surjective
proof end;

theorem Th13: :: FUNCTOR1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3 st F is bijective & G is bijective holds
G * F is bijective
proof end;

theorem :: FUNCTOR1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, I being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr of A,I holds F | C = (F | B) | D
proof end;

theorem :: FUNCTOR1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2, C3 being non empty reflexive AltCatStr
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of C2,C3
for A being non empty reflexive SubCatStr of C1 holds (G * F) | A = G * (F | A) by FUNCTOR0:33;

theorem :: FUNCTOR1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCTOR1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty AltCatStr
for B being non empty SubCatStr of A holds
( B is full iff incl B is full )
proof end;

theorem :: FUNCTOR1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr of C1,C2 holds
( F is full iff for o1, o2 being object of C1 holds Morph-Map F,o1,o2 is onto )
proof end;

theorem :: FUNCTOR1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr of C1,C2 holds
( F is faithful iff for o1, o2 being object of C1 holds Morph-Map F,o1,o2 is one-to-one )
proof end;

theorem :: FUNCTOR1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty transitive with_units AltCatStr holds (id A) " = id A
proof end;

theorem :: FUNCTOR1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr of A,B st F is bijective holds
for G being feasible FunctorStr of B,A st FunctorStr(# the ObjectMap of G,the MorphMap of G #) = F " holds
F * G = id B
proof end;

Lm1: for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
proof end;

theorem :: FUNCTOR1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr of A,B st F is bijective holds
(F " ) * F = id A
proof end;

theorem :: FUNCTOR1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr of A,B st F is bijective holds
(F " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
proof end;

theorem :: FUNCTOR1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being non empty transitive with_units reflexive AltCatStr
for G being feasible FunctorStr of A,B
for F being feasible FunctorStr of B,C
for GI being feasible FunctorStr of B,A
for FI being feasible FunctorStr of C,B st F is bijective & G is bijective & FI is bijective & GI is bijective & FunctorStr(# the ObjectMap of GI,the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI,the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
proof end;