DESCRIPTION

CONTENT OF THIS LIBRARY

(1) DIRECTORIES
(2) ./CAT
(3) ./STS (thesis chapter 7)
(4) ./COMP (obsolete)
(5) ./ORDER (obsolete)
(6) ./PROP_untyped (thesis chapter 8)
(7) ./RPCF (thesis chapter 9)

(1) DIRECTORIES

  ./CAT : general category theory + examples

  ./STS : category of representations of simply typed signature
          has an initial object

  ./{ULC,TLC,PCF} : syntax of untyped lambda calculus, simply-typed lc
	  and PCF, respectively.
	  the syntaxes are endomonads over Set resp. [T,Set]
	  they are also relative monads to preorders
	  in *_terms some constants are defined
 
  ./COMP : 
	   syntactic compilation, i. e. with change of object types
	   see further down for which files to view 

  ./ORDER : 
	    initiality without change of object types
	    proof for ULC
	    proof for TLC

  ./PROP_untyped : 
	    initiality for untyped syntax with semantics
		in form of reduction rules
	      implementation of the contents of preprint
		"Modules over relative monads ..."
	
  ./RPCF : compilation of PCF+red to ULC+beta
	  

(2) ./CAT
     
  . contains category theory + examples
  . description of file content in recommended reading order
  . naming scheme : instances are given in CAPITAL LETTERS, e. g. 
       SET is the category of sets

   ./CAT/category.v : 
        definition of Cat and Category
	some trivial lemmata
	heterogeneous equality of morphisms

   ./CAT/monic_epi.v
	monics
	epis
	invertibles
	composition of monics is monic
	composition of epis is epi
	monic (f ;; g) => monic f
	epi (f ;; g) => epi g
	uniqueness of inverse
	inverse is invertible
	f^{-1}^{-1} = f
	putting inv. morphism on other side
	inverse of a composition of invertibles

   ./CAT/product.v
	definition of product on a category
	definition of product of morphisms
	fusion laws of product of morphisms, identity, composition
	product is assoc up to isomorphism
	
   ./CAT/coproduct.v
	same as product.v, but for coproduct

   ./CAT/functor.v
	definition of Func and Functor
	composition and identity of functors
	EXT heterogeneous equality on functors
	some lemmata connecting heterogeneous equality of morphisms with
 	  EXT het equality of functors
	instance Cat_CAT

   ./CAT/functor_leibniz_eq.v
	lemma for proving two functors Leibniz-equal
	proof of associativity and neutrality of 
	  composition wrt Leibniz (as opposed to EXT in functor.v)
	proof that EXT eq implies extensional Leibniz eq on object function
   	  (assuming functional_extensionality_dep)
	proof that composition is a setoid morphism wrt EXT equality
	  (assuming functional_ext_dep and PI)
	
   ./CAT/functor_properties.v
	definition of "full" and "faithful"
	composition of full / faithful functors is full / faithful
   
   ./CAT/NT.v
	definition of NatTrans and NT
	extensional equality on natural transformations is equivalence rel
	vertical composition (for hor. comp. see horcomp.v)
	neutrality and assoc for vertical composition
 
   ./CAT/CatFunct.v
	category of functors, nat trans and vertical composition
	extensionality principle on natural transformations
	  a : F --> G, b : H --> K, F = H, G = K 
	  het eq on all morphisms => het eq in cat of functors and nat trans
            depends on JMeq_eq by dependent induction

   ./CAT/initial_terminal.v
	definition of Initial and Terminal

   ./CAT/horcomp.v
   	lemma : no choice in defining horizontal composition
	definition of horizontal composition
	def of neutral nat transformation wrt horizontal composition
	extensional heterogeneous equality for 
	  a : F -> G and b : F' -> G'
	setoidal properties for ext het eq
	neutrality of neutral nat trans wrt to ext het eq
	record {| F ; G ; alpha : F -> G |}
	ext het eq is an equivalence relation on above type	

   ./CAT/smon_cats.v
	functor C -> C x C, c \mapsto (c,e) 
	ditto with e left
	functor A x (B x C) -> (A x B) x C
	definition of strict monoidal category
	
	instance End (C) of endofunctors over C
	  - tensor : on objects (F, G) -> F o G
	             on morphisms (a,b) -> horcomp a b
	  - uses PI and functional_ext_dep

   ./CAT/mon_cats.v
	definition of monoidal cat C
	  - tens : C x C -> C
	  - I : C
	  - composition laws up to isomorphism
	category SET of sets with cartesian product as tens is monoidal

   ./CAT/enriched_cat.v
	definition of category enriched over monoidal cat M
	category enriched over SET is an ordinary category

   ./CAT/limits.v
	diagonal functor C ---> [J, C]
	category of cones 
	definition of limit as terminal object in category of cones

   ./CAT/subcategories.v
	subcategory given by predicates on obj and mor that are compatible
	  with identity and composition
	a subcategory is a category
	injection functor FINJ : S --> C for S a subcategory
	FINJ is faithful

   ./CAT/monad_haskell.v
	definition of monad as kleisli structure
	join 
	lift and functoriality
	
   ./CAT/monad_h_morphism.v
	definition of morphism of monads (as in monad_haskell.v)
	naturality of morphisms of monads
	category MONAD of monads and their morphisms
	
   ./CAT/monad_h_module.v
	definition of module over a monad (haskell style = kleisli)
	mlift and functoriality
	morphisms of modules
	naturality of module morphisms 
	category (MOD P D) of modules over P with codomain D
	tautological module
	pullback module + functoriality
	product module + categorical product properties
	constant module
	terminal module (if D has terminal object)

   ./CAT/monad_h_morphism_gen.v
	generalized morphism of monads as in
	  - P : Monad C
	  - Q : Monad D
	  - F : Functor C D
	  - Tau : forall c, F (P c) --> Q (F c)
	naturality of Tau
	pullback along a gen monad morphism
		
   ./CAT/monad_def.v
	definition of monad in terms of eta and mu (multiplication)
	
   ./CAT/monad_morphism.v
	morphism of monads (as in monad_def.v)
	category MONAD of monads
	
	definition of left modules over monads
	pullback module
	morphism of left modules
	category MOD_R of left modules 
	
   ./CAT/small_cat.v
	definition of small cat, obj and mor are sets
	category of small cats, SMALLCAT

   ./CAT/cat_DISCRETE.v
	any type T is a discrete category DISCRETE T
	
   ./CAT/cat_TYPE.v
	category where objects are types and morphisms are total functions
	initial object {}
	terminal object {*}
	
   ./CAT/cat_INDEXED_TYPE.v
	category ITYPE T for a type T
	  - obj : families of types indexed by T
	  - morphisms : families of functions
	opt monad (adding one element)
	derivation of modules
	fibre module


(3) ./STS
	
   ./STS/STS_arities.v
	definition of simply typed signature
	examples of signatures : TLC and PCF
	multiple addition of variables
	functoriality of addition of vars
	lshift, the capture avoiding thing for lists of vars
	derived module wrt a list of variables
	the module "of arguments" of a constructor 
 	  (prod of fibres of derived mods)
	source and target modules of an arity
	representation of an arity
	representation of a signature
	the product fibre derived module morphism 
	  (left vertical of comm diag of morphism of reps)
	commutative diagram for morphism of representations
	def of morphism of representations

   ./STS/STS_representations.v
	identity representation of a signature
	composition of representations
	category of representations REPRESENTATION S

   ./STS/STS_initial.v
	carrier STS of initial monad of REP(S)
	rename, the functoriality
	inj, the renaming into terms with one more variable
	_shift, for avoiding capture
	subst, simultaneous substitution
	substar, single value substitution
	fusion laws for these functions
	monadicity of STS
	isomorphism STS_list <-> prod_mod_c STSM
	representation structure of STSM
	init, the (carrier of) the initial morphism
	init commutes with renaming
	init commutes with shifting
	init commutes with substitution
	init is a morphism of representations
	init is unique 
	REPRESENTATION S has an initial object
  
	
(4) ./COMP
   
   ./COMP/PCF_rep_quant.v
	representation of PCF consists of f : T -> U etc.
   
   ./COMP/PCF_rep_hom_quant.v
	lemmas about distributivity of arrows
	morphism of representations of PCF, starting with g : U->U'
   
   ./COMP/PCF_rep_eq_quant.v
	inductive predicate for equality of morphisms of PCF-reps
	proof of equivalence properties
	definition of identity representation morphism

   ./COMP/PCF_rep_comp_quant.v
	composition of representation monad morphisms gives
	representation
	
   ./COMP/PCF_rep_cat_quant.v
	category of representations of PCF
	
   ./COMP/PCF_quant.v
	monad of PCF + its constructors give a representation of PCF
	carrier of initial morphism
	init commutes with lift and substitution
	init is a morphism of reps
	init is unique
	PCF is initial

   ./COMP/PCF_ULC_nounit.v
	equipping uULC with a rep of PCF, yielding rep PCF_ULC
	
   ./COMP/PCF_ULC_comp.v
	some examples of PCF terms compiled to ULC via initial morph

(5) ./ORDER

   ./ORDER/ulc_order_rep.v
	representation of ULC+beta
	morphisms of ULC+beta
	
   ./ORDER/ulc_order_rep_eq.v
	equality on morphisms of ULC+beta
	identity morphisms
	composition of morphisms
	category of representations of ULC+beta

   ./ORDER/ulc.v
	relative monad of ULC with constructors 
	  yield rep of ULC+beta
	
   ./ORDER/ulc_init.v
	carrier of initial morphism
	compatibility with renaming and substitution
	compatibility with beta relations (several steps)
	init is a morph of reps
	init is unique
	ULCbeta is initial rep

(6) ./PROP_untyped
	
	the 3 files arities.v, representations.v, 
	 initial.v are actually similar to their 
	 friends in ./STS
	 difference : only untyped arities, 
	   representations in *relative* monads

   ./PROP_untyped/arities.v
	definition of untyped signature
	multiple addition of variables
	functoriality of addition of vars
	lshift, the capture avoiding thing for lists of vars
	derived module wrt a list of variables
	the module "of arguments" of a constructor 
 	  (prod of derived mods)
	source and target modules of an arity
	representation of an arity
	representation of a signature
	the product derived module morphism 
	  (left vertical of comm diag of morphism of reps)
	commutative diagram for morphism of representations
	def of morphism of representations

   ./PROP_untyped/representations.v
	identity representation of a signature
	composition of representations
	category of representations REPRESENTATION S

   ./PROP_untyped/initial.v
	** the initial object in the category of representations 
	   without any equations is given by the type UTS, 
	   equipped with the diagonal order, i.e. the smallest 
	   possible preorder.
	   
	carrier UTS of initial monad of REP(S)
	rename, the functoriality
	inj, the renaming into terms with one more variable
	_shift, for avoiding capture
	subst, simultaneous substitution
	substar, single value substitution
	fusion laws for these functions
	monadicity of UTS
	isomorphism UTS_list <-> prod_mod_c UTS
	representation structure of UTSM
	init, the (carrier of) the initial morphism
	init commutes with renaming
	init commutes with shifting
	init commutes with substitution
	init is a morphism of representations
	init is unique 
	REPRESENTATION S has an initial object	
   
   ./PROP_untyped/prop_arities.v (* superseded by next file *)
	definition of half-equation, propositional arity,
	  algebraic equation
	subcategory PROP_REP of representations verifying a set of 
	  inequations, 
	definition of the order on terms of UTS, giving UTSP
	representation structure on UTSP -> UTSPREPR
	initiality of UTSPREPR in PROP_REP
	
   ./PROP_untyped/prop_arities_initial.v
	definition of half-equation, propositional arity,
	  algebraic equation
	subcategory PROP_REP of representations verifying a set of 
	  inequations
	definition of the order associated to a set of equations
	  on terms of UTS, giving UTSP
	representation structure on UTSP, yielding rep UTSPROPREPR
	  initiality of UTSPROPREPR in PROP_REP
	 	
(7) ./RPCF

   ./RPCF/RPCF_rep.v
	definition of representation of semantic PCF
	
   ./RPCF/RPCF_rep_hom.v
	definition of morphism of representations of s. PCF

   ./RPCF/RPCF_rep_eq.v
	definition of equality of 2 parallel morphisms
	  of representations of PCF
	proof of setoidality of equality

   ./RPCF/RPCF_rep_comp.v
	definition of composition of 2 morphisms of 
	  reps of PCF

   ./RPCF/RPCF_rep_id.v
	definition of identity morphism of reps

   ./RPCF/RPCF_rep_cat.v
	definition of category of representations, in part.
	  proof of assoc of composition and neutrality

   ./RPCF/RPCF_syntax_rep.v
	PCFE is the monad underlying a representation of PCF

   ./RPCF/RPCF_syntax_init.v
	definition of a morphism of representations from 
	  PCFE to any R, i.e. weak initiality
	
   ./RPCF/RPCF_INIT.v
	proof of unicity of above morphism
	initiality
	
   ./RPCF/RPCF_ULC_nounit.v
	representation of PCF in ULC, a monad obtained
	  via a map from monads over Delta to monads 
	  over * -> Delta
   
   ./RPCF/ULC_comp.v
	some examples of translations from PCF to ULC