proposition: Lemma InterChange_law : (T o_NTh T') o_NTv U o_NTh U' =_NT (T o_NTv U) o_NTh T' o_NTv U'.
proof: Proof. unfold Equal_NT in |- *; intro a; simpl in |- *. unfold CompH_NT, Comp_Functor in |- *; simpl in |- *. unfold Ast, Comp_tau in |- *; simpl in |- *. unfold Comp_tau in |- *. apply Trans with ((T' (F a) o U' (F a)) o FMor H' (T a) o FMor H' (U a)). apply Trans with (T' (F a) o FMor G' (T a) o U' (G a) o FMor H' (U a)). apply Ass1. apply Trans with (T' (F a) o U' (F a) o FMor H' (T a) o FMor H' (U a)). apply Comp_l. apply Trans with ((FMor G' (T a) o U' (G a)) o FMor H' (U a)). apply Ass. apply Trans with ((U' (F a) o FMor H' (T a)) o FMor H' (U a)). apply Comp_r; apply NatCond. apply Ass1. apply Ass. apply Comp_l; apply FComp1. Qed.
imports: CatFunct