category.pvs

category [ obj,arr: TYPE,
           dom,cod: [arr -> obj],
	   id: [obj -> arr],
	   o: [[f:arr, {g:arr | cod(g) = dom(f)}] -> arr]
	 ]: THEORY

BEGIN

 ASSUMING IMPORTING category_assumptions[obj,arr]

  this_is_category: ASSUMPTION
    is_category? (dom,cod,id,o)

 ENDASSUMING

 IMPORTING category_definitions[obj,arr,dom,cod,id,o]

 uniqueness_of_identity: THEOREM
   FORALL (A:obj, f:arr | from?(f,A) AND to?(f,A)):
     (FORALL (g:arr | from?(g,A)): g o f = g) AND
     (FORALL (h:arr | to?(h,A)): f o h = h) IMPLIES
     f = id(A)

 uniqueness_of_inverse: THEOREM
   FORALL (f:arr): FORALL (g,h:{x:arr | cod(x) = dom(f) AND dom(x) = cod(f)}):
     (inverse? (f,g) AND inverse? (f,h)) IMPLIES g = h

 isomorphic_reflexive: THEOREM
   FORALL (A:obj): isomorphic? (A,A)

 isomorphic_symmetric: THEOREM
   FORALL (A,B:obj) : isomorphic? (A,B) IMPLIES isomorphic? (B,A)

 isomorphic_transitive: THEOREM
   FORALL (A,B,C:obj):
     (isomorphic? (A,B) AND isomorphic? (B,C)) IMPLIES isomorphic? (A,C)

 iso_monic_epic: THEOREM
   FORALL (f:arr): iso? (f) IMPLIES (monic? (f) AND epic? (f))

 IMPORTING functor_assumptions[obj,arr,obj,arr]
 trivial_functor: THEOREM
   is_functor? (dom,cod,dom,cod,id,id,o,o,
		(LAMBDA (X:obj): X),
		(LAMBDA (x:arr): x))

 initials_isomorphic: THEOREM
   FORALL (A,B:obj):
     (initial? (A) AND initial? (B)) IMPLIES isomorphic? (A,B)

END category