proposition: Theorem ixapp_naturality : ∀ {I J K A B C D} (f : A → C) (g : B → D) (u : F I J A) (v : F J K B), ixmap (f *** g) (u ** v) = (ixmap f u) ** (ixmap g v).
proof: Proof. intros. unfold ixapp_prod. rewrite <- app_ixmap_unit. rewrite ixfun_composition_x. repeat (rewrite <- app_ixmap_unit). rewrite <- ixapp_composition. rewrite <- ixapp_composition. rewrite <- ixapp_composition. rewrite <- ixapp_composition. rewrite ixapp_composition. rewrite ixapp_composition. rewrite_ixapp_homomorphisms. rewrite ixfun_composition_x. rewrite ixfun_composition_x. rewrite ixapp_interchange. rewrite app_ixmap_unit. rewrite ixfun_composition_x. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple