some categorical packaging of proofs
	modified:   Library.agda
	modified:   SpinelessValues.agda
	modified:   Term.agda