`{Funext} C D : swap C D o swap D C = 1. Proof. path_functor. exists (path_forall _ _ swap_involutive_helper). repeat (apply (@path_forall _); intro). repeat match goal with | [ |- context[transport (fun x' => forall y, @?C x' y) ?p ?f ?x] ] => simpl rewrite (@transport_forall_constant _ _ C _ _ p f x) end. transport_path_forall_hammer. by repeat match goal with | [ H : Empty |- _ ] => destruct H | [ H : (_ + _) |- _ ] => destruct H | _ => progress hnf in * end. Qed.
Require Import Category.Sum Functor.Core Functor.Composition.Core Functor.Identity. Require Import Functor.Paths HoTT.Tactics Types.Forall. Require Import Basics.Tactics.