started a new branck to improve our treatment of quotients in equating
maps in partial map categories.
making a mess in partial maps.
proved that our equivalence relation on spans is one.
congruence of span composition remains
tidied up the partial map cat def by introducing shorthands for the quotient operations.
	modified:   PartialMaps.agda
moved the quotients stuff into utilities
removed the 'crude' quotient postulate
	modified:   PartialMaps.agda
the whole pullbackiso proof was marked irrelevant. Now only the required bits are.
	modified:   Categories/Pullbacks.agda
have the iso for the congruence proof. Triangles remain.
congruence proof done.
	modified:   PartialMaps.agda
Working on soundness
	modified:   Soundness.agda
	modified:   Utilities.agda
Soundness is done.
	modified:   Soundness.agda
Pushing quotients in the completeness proof (first functor done).
	modified:   Completeness.agda
Moving quotients in completeness (first restriction functor completed)
	modified:   Completeness.agda
Trying to understand how to prove the second part of the completeness theorem using quotients.
	modified:   Completeness.agda
Both functors are ok now (with a postulate for the second).
	modified:   Completeness.agda
First completeness isomorphism theorem done
	modified:   Completeness.agda
Completeness with quotients (with a postulate)
Proof of postulate inserted (with irrelevance issues).
	modified:   Completeness.agda
	modified:   Totals.agda
added irrelevant axiom and used it explicitly in completeness proof