proposition: Lemma swap_involutive `{Funext} C D : swap C D o swap D C = 1.
proof: 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 : (_ + _)%type |- _ ] => destruct H | _ => progress hnf in * end. Qed.
imports: Category.Sum Functor.Core Functor.Composition.Core Functor.Identity Functor.Paths HoTT.Tactics Types.Forall Basics.Tactics