proposition: Lemma LAdj_nt_law : NT_law LAdj_tau.
proof: Proof. unfold NT_law in |- *; intros a b f. apply Trans with (UA_diese (LAdj_unit a) (f o UA_mor (LAdj_unit' b))). apply (UA_unic (u:=LAdj_unit a)). apply Trans with ((UA_mor (LAdj_unit a) o FMor G (FMor F f)) o FMor G (LAdj_tau b)). apply Trans with (UA_mor (LAdj_unit a) o FMor G (FMor F f) o FMor G (LAdj_tau b)). apply Comp_l; apply FComp. apply Ass. apply Trans with ((f o UA_mor (LAdj_unit b)) o FMor G (LAdj_tau b)). apply Comp_r; apply Sym; apply (Prf_NT_law (Unit_NT la) f). apply Trans with (f o UA_mor (LAdj_unit b) o FMor G (LAdj_tau b)). apply Ass1. apply Comp_l; apply (UA_diag (LAdj_unit b) (UA_mor (LAdj_unit' b))). apply (UA_unic1 (u:=LAdj_unit a)). apply Trans with (UA_mor (LAdj_unit a) o FMor G (LAdj_tau a) o FMor G (FMor F' f)). apply Comp_l; apply FComp. apply Trans with ((UA_mor (LAdj_unit a) o FMor G (LAdj_tau a)) o FMor G (FMor F' f)). apply Ass. apply Trans with (UA_mor (LAdj_unit' a) o FMor G (FMor F' f)). apply Comp_r; apply (UA_diag (LAdj_unit a) (UA_mor (LAdj_unit' a))). apply Sym; apply (Prf_NT_law (Unit_NT la') f). Qed.
imports: Adjunction1