Some progress on left-id-law and such
Added equality stuff for Alg1 and completed Eq stuff for Alg0.
Some form of composition for Alg1 homs.
Started to work on Alg1
Did limits for alg0.
Finished associativity again for pf alg0
Some experimenting with a "different" equality type and pointfree stuff.
Lots of refactoring
Finished first attempt at showing composition law for target functor.
Some progress on composition part of target functor
Added assoc coherence law module to Target.agda, moved ApdTarget to T…
Filled in last gap in definition equaliser for alg0 and started worki…
Some progress on associativity for Alg1 morphisms.
Added coherence laws required for identity laws.
Trying to build Agda with cpp instead of cpphs.
Added explicit version of cpphs to get Agda to build.
Added Makefile and script that counts the number of admits and TODOs.
Modularised Target module.
Working on showing that finitary functors are omega-cocontinuous
Some progress on the correctness of families.
Trying to simplify equality of algebra morphisms for 1-hits.
Fiddling with correctness of families.
Some cube stuff and some stuff on families/fibrations.
Implemented Thorsten's suggestions.
Removed old files, started formalising existence of colimits in categ…
Started working on exponentials in Fin.
Reorganising whole repository
Some minor additions, working towards showing that F-alg has omega-co…
Added squares for algebra hom equality.
Uncurried the methods.
Extended the part on 1-hits.