the embedding, faithfulness, and other tidying
	modified:   Categories.agda
	modified:   Functors.agda
	modified:   PartialMaybe.agda
	modified:   RestrictionCat.agda