outlined(?) proofs from functor composition
	modified:   Functors.agda
	modified:   RestrictionCat.agda