Initial commit
added Categories and Functors
minor tweaking functors
some infrastructure and define trivial rest cat and rest cat for partial functions implemented using Maybe
	modified:   Categories.agda
	modified:   Functors.agda
	modified:   Categories.agda
	modified:   Functors.agda
	modified:   PartialMaybe.agda
	modified:   RestrictionCat.agda
	modified:   RestrictionCat.agda
switched to heterogeneous equality, dealt with consequences, added some equality module, proved TotEq.
	modified:   Categories.agda
	new file:   Equality.agda
	modified:   Functors.agda
	modified:   Kleisli.agda
	modified:   MaybeMonad.agda
	modified:   Monads.agda
	modified:   PartialMaybe.agda
	modified:   RestrictionCat.agda
	modified:   Sets.agda
define restriciton category of total maps, I think
	modified:   RestrictionCat.agda
renamed begin_ to proof_
	modified:   Categories.agda
	modified:   Functors.agda
	modified:   PartialMaybe.agda
	modified:   RestrictionCat.agda
trivial
	modified:   RestrictionCat.agda
outlined(?) proofs from functor composition
	modified:   Functors.agda
	modified:   RestrictionCat.agda
the embedding, faithfulness, and other tidying
	modified:   Categories.agda
	modified:   Functors.agda
	modified:   PartialMaybe.agda
	modified:   RestrictionCat.agda
added two defs of pullbacks
	modified:   Categories.agda
defined the necessary map for the first pasting lemma, need to prove various things commute and then completeness.
	modified:   Categories.agda
finished pasting lemma 1
	modified:   Categories.agda
proved that inverses are unique
	modified:   Categories.agda
	modified:   RestrictionCat.agda
updated the readme
modified:   README.md
proved antisymmetry of \leq
modified:   RestrictionCat.agda
working on second pasting lemma. sync.
modified:   Categories.agda