(** * Functors involving coproduct categories *)
Require Import Category.Sum Functor.Core Functor.Composition.Core Functor.Identity.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Functor.Paths HoTT.Tactics Types.Forall.
Require Import Basics.Tactics.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

(** We save [inl] and [inr] so we can use them to refer to the functors, too.  Outside of the [Categories/] directory, they should always be referred to as [Functor.inl] and [Functor.inr], after a [Require Functor].  Outside of this file, but in the [Categories/] directory, if you do not want to depend on all of [Functor] (for e.g., speed reasons), they should be referred to as [Functor.Sum.inl] and [Functor.Sum.inr] after a [Require Functor.Sum]. *)
Local Notation type_inl := inl.
Local Notation type_inr := inr.

(** ** Injections [inl : C → C + D] and [inr : D → C + D] *)
Section sum_functors.
  Variables C D : PreCategory.

  Definition inl : Functor C (C + D)
    := Build_Functor C (C + D)
                     (@inl _ _)
                     (fun _ _ m => m)
                     (fun _ _ _ _ _ => idpath)
                     (fun _ => idpath).

  Definition inr : Functor D (C + D)
    := Build_Functor D (C + D)
                     (@inr _ _)
                     (fun _ _ m => m)
                     (fun _ _ _ _ _ => idpath)
                     (fun _ => idpath).
End sum_functors.

(** ** Coproduct of functors [F + F' : C + C' → D] *)
Section sum.
  Variables C C' D : PreCategory.

  Definition sum (F : Functor C D) (F' : Functor C' D)
  : Functor (C + C') D.
C, C', D: PreCategory
F: Functor C D
F': Functor C' D
Functor (C + C') D
  Proof.
C, C', D: PreCategory
F: Functor C D
F': Functor C' D
Functor (C + C') D
    refine (Build_Functor
              (C + C') D
              (fun cc'
               => match cc' with
                    | type_inl c => F c
                    | type_inr c' => F' c'
                  end)
              (fun s d
               => match s, d with
                    | type_inl cs, type_inl cd
                      => fun m : morphism _ cs cd => F _1 m
                    | type_inr c's, type_inr c'd
                      => fun m : morphism _ c's c'd => F' _1 m
                    | _, _ => fun m => match m with end
                  end%morphism)
              _
              _);
    abstract (
        repeat (intros [] || intro);
        simpl in *;
          auto with functor
      ).
  Defined.
End sum.

(** ** swap : [C + D → D + C] *)
Section swap_functor.
  Definition swap C D
  : Functor (C + D) (D + C)
    := sum (inr _ _) (inl _ _).

  Local Open Scope functor_scope.

  Definition swap_involutive_helper {C D} c
  : (swap C D) ((swap D C) c)
    = c
    := match c with type_inl _ => idpath | type_inr _ => idpath end.

  Lemma swap_involutive `{Funext} C D
  : swap C D o swap D C = 1.
H: Funext
C, D: PreCategory
swap C D o swap D C = 1
  Proof.
H: Funext
C, D: PreCategory
swap C D o swap D C = 1
    path_functor.
H: Funext
C, D: PreCategory
{HO
: (fun c : D + C =>
   match
     match c with
     | type_inl _ _ c0 => type_inr C c0
     | type_inr _ _ c' => type_inl D c'
     end
   with
   | type_inl _ _ c0 => type_inr D c0
   | type_inr _ _ c' => type_inl C c'
   end) = idmap &
transport
  (fun GO : D + C -> D + C =>
   forall s d : D + C,
   match s with
   | type_inl _ _ s0 =>
       match d with
       | type_inl _ _ d0 => morphism D s0 d0
       | type_inr _ _ _ => Empty
       end
   | type_inr _ _ s0 =>
       match d with
       | type_inl _ _ _ => Empty
       | type_inr _ _ d0 => morphism C s0 d0
       end
   end ->
   match GO s with
   | type_inl _ _ s0 =>
       match GO d with
       | type_inl _ _ d0 => morphism D s0 d0
       | type_inr _ _ _ => Empty
       end
   | type_inr _ _ s0 =>
       match GO d with
       | type_inl _ _ _ => Empty
       | type_inr _ _ d0 => morphism C s0 d0
       end
   end) HO
  (fun (s d : D + C)
     (m : match s with
          | type_inl _ _ s0 =>
              match d with
              | type_inl _ _ d0 => morphism D s0 d0
              | type_inr _ _ _ => Empty
              end
          | type_inr _ _ s0 =>
              match d with
              | type_inl _ _ _ => Empty
              | type_inr _ _ d0 => morphism C s0 d0
              end
          end) =>
   match
     match s with
     | type_inl _ _ c => type_inr C c
     | type_inr _ _ c' => type_inl D c'
     end as s0
     return
       (match s0 with
        | type_inl _ _ s1 =>
            match
              match d with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ d0 => morphism C s1 d0
            | type_inr _ _ _ => Empty
            end
        | type_inr _ _ s1 =>
            match
              match d with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d0 => morphism D s1 d0
            end
        end ->
        match
          match s0 with
          | type_inl _ _ c => type_inr D c
          | type_inr _ _ c' => type_inl C c'
          end
        with
        | type_inl _ _ s1 =>
            match
              match
                match d with
                | type_inl _ _ c => type_inr C c
                | type_inr _ _ c' => type_inl D c'
                end
              with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ d0 => morphism D s1 d0
            | type_inr _ _ _ => Empty
            end
        | type_inr _ _ s1 =>
            match
              match
                match d with
                | type_inl _ _ c => type_inr C c
                | type_inr _ _ c' => type_inl D c'
                end
              with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d0 => morphism C s1 d0
            end
        end)
   with
   | type_inl _ _ cs =>
       match
         match d with
         | type_inl _ _ c => type_inr C c
         | type_inr _ _ c' => type_inl D c'
         end as d0
         return
           (match d0 with
            | type_inl _ _ d1 => morphism C cs d1
            | type_inr _ _ _ => Empty
            end ->
            match
              match d0 with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d1 => morphism C cs d1
            end)
       with
       | type_inl _ _ cd => idmap
       | type_inr _ _ _ =>
           fun m0 : Empty =>
           match m0 return Empty with
           end
       end
   | type_inr _ _ c's =>
       match
         match d with
         | type_inl _ _ c => type_inr C c
         | type_inr _ _ c' => type_inl D c'
         end as d0
         return
           (match d0 with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d1 => morphism D c's d1
            end ->
            match
              match d0 with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ d1 => morphism D c's d1
            | type_inr _ _ _ => Empty
            end)
       with
       | type_inl _ _ _ =>
           fun m0 : Empty =>
           match m0 return Empty with
           end
       | type_inr _ _ c'd => idmap
       end
   end
     (match
        s as s0
        return
          (match s0 with
           | type_inl _ _ s1 =>
               match d with
               | type_inl _ _ d0 => morphism D s1 d0
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s1 =>
               match d with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism C s1 d0
               end
           end ->
           match
             match s0 with
             | type_inl _ _ c => type_inr C c
             | type_inr _ _ c' => type_inl D c'
             end
           with
           | type_inl _ _ s1 =>
               match
                 match d with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ d0 => morphism C s1 d0
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s1 =>
               match
                 match d with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism D s1 d0
               end
           end)
      with
      | type_inl _ _ cs =>
          match
            d as d0
            return
              (match d0 with
               | type_inl _ _ d1 => morphism D cs d1
               | type_inr _ _ _ => Empty
               end ->
               match
                 match d0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d1 => morphism D cs d1
               end)
          with
          | type_inl _ _ cd => idmap
          | type_inr _ _ _ =>
              fun m0 : Empty =>
              match m0 return Empty with
              end
          end
      | type_inr _ _ c's =>
          match
            d as d0
            return
              (match d0 with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d1 => morphism C c's d1
               end ->
               match
                 match d0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ d1 => morphism C c's d1
               | type_inr _ _ _ => Empty
               end)
          with
          | type_inl _ _ _ =>
              fun m0 : Empty =>
              match m0 return Empty with
              end
          | type_inr _ _ c'd => idmap
          end
      end m)) = (fun s d : D + C => idmap)}
    exists (path_forall _ _ swap_involutive_helper).
H: Funext
C, D: PreCategory
transport
  (fun GO : D + C -> D + C =>
   forall s d : D + C,
   match s with
   | type_inl _ _ s0 =>
       match d with
       | type_inl _ _ d0 => morphism D s0 d0
       | type_inr _ _ _ => Empty
       end
   | type_inr _ _ s0 =>
       match d with
       | type_inl _ _ _ => Empty
       | type_inr _ _ d0 => morphism C s0 d0
       end
   end ->
   match GO s with
   | type_inl _ _ s0 =>
       match GO d with
       | type_inl _ _ d0 => morphism D s0 d0
       | type_inr _ _ _ => Empty
       end
   | type_inr _ _ s0 =>
       match GO d with
       | type_inl _ _ _ => Empty
       | type_inr _ _ d0 => morphism C s0 d0
       end
   end)
  (path_forall
     (fun c : (D + C)%category =>
      ((swap C D) _0 ((swap D C) _0 c))%object) idmap
     swap_involutive_helper)
  (fun (s d : D + C)
     (m : match s with
          | type_inl _ _ s0 =>
              match d with
              | type_inl _ _ d0 => morphism D s0 d0
              | type_inr _ _ _ => Empty
              end
          | type_inr _ _ s0 =>
              match d with
              | type_inl _ _ _ => Empty
              | type_inr _ _ d0 => morphism C s0 d0
              end
          end) =>
   match
     match s with
     | type_inl _ _ c => type_inr C c
     | type_inr _ _ c' => type_inl D c'
     end as s0
     return
       (match s0 with
        | type_inl _ _ s1 =>
            match
              match d with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ d0 => morphism C s1 d0
            | type_inr _ _ _ => Empty
            end
        | type_inr _ _ s1 =>
            match
              match d with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d0 => morphism D s1 d0
            end
        end ->
        match
          match s0 with
          | type_inl _ _ c => type_inr D c
          | type_inr _ _ c' => type_inl C c'
          end
        with
        | type_inl _ _ s1 =>
            match
              match
                match d with
                | type_inl _ _ c => type_inr C c
                | type_inr _ _ c' => type_inl D c'
                end
              with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ d0 => morphism D s1 d0
            | type_inr _ _ _ => Empty
            end
        | type_inr _ _ s1 =>
            match
              match
                match d with
                | type_inl _ _ c => type_inr C c
                | type_inr _ _ c' => type_inl D c'
                end
              with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d0 => morphism C s1 d0
            end
        end)
   with
   | type_inl _ _ cs =>
       match
         match d with
         | type_inl _ _ c => type_inr C c
         | type_inr _ _ c' => type_inl D c'
         end as d0
         return
           (match d0 with
            | type_inl _ _ d1 => morphism C cs d1
            | type_inr _ _ _ => Empty
            end ->
            match
              match d0 with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d1 => morphism C cs d1
            end)
       with
       | type_inl _ _ cd => idmap
       | type_inr _ _ _ =>
           fun m0 : Empty =>
           match m0 return Empty with
           end
       end
   | type_inr _ _ c's =>
       match
         match d with
         | type_inl _ _ c => type_inr C c
         | type_inr _ _ c' => type_inl D c'
         end as d0
         return
           (match d0 with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d1 => morphism D c's d1
            end ->
            match
              match d0 with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ d1 => morphism D c's d1
            | type_inr _ _ _ => Empty
            end)
       with
       | type_inl _ _ _ =>
           fun m0 : Empty =>
           match m0 return Empty with
           end
       | type_inr _ _ c'd => idmap
       end
   end
     (match
        s as s0
        return
          (match s0 with
           | type_inl _ _ s1 =>
               match d with
               | type_inl _ _ d0 => morphism D s1 d0
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s1 =>
               match d with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism C s1 d0
               end
           end ->
           match
             match s0 with
             | type_inl _ _ c => type_inr C c
             | type_inr _ _ c' => type_inl D c'
             end
           with
           | type_inl _ _ s1 =>
               match
                 match d with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ d0 => morphism C s1 d0
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s1 =>
               match
                 match d with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism D s1 d0
               end
           end)
      with
      | type_inl _ _ cs =>
          match
            d as d0
            return
              (match d0 with
               | type_inl _ _ d1 => morphism D cs d1
               | type_inr _ _ _ => Empty
               end ->
               match
                 match d0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d1 => morphism D cs d1
               end)
          with
          | type_inl _ _ cd => idmap
          | type_inr _ _ _ =>
              fun m0 : Empty =>
              match m0 return Empty with
              end
          end
      | type_inr _ _ c's =>
          match
            d as d0
            return
              (match d0 with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d1 => morphism C c's d1
               end ->
               match
                 match d0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ d1 => morphism C c's d1
               | type_inr _ _ _ => Empty
               end)
          with
          | type_inl _ _ _ =>
              fun m0 : Empty =>
              match m0 return Empty with
              end
          | type_inr _ _ c'd => idmap
          end
      end m)) = (fun s d : D + C => idmap)
    repeat (apply (@path_forall _); intro).
H: Funext
C, D: PreCategory
x, x0: D + C
x1: match x with
| type_inl _ _ s =>
    match x0 with
    | type_inl _ _ d => morphism D s d
    | type_inr _ _ _ => Empty
    end
| type_inr _ _ s =>
    match x0 with
    | type_inl _ _ _ => Empty
    | type_inr _ _ d => morphism C s d
    end
end
transport
  (fun GO : D + C -> D + C =>
   forall s d : D + C,
   match s with
   | type_inl _ _ s0 =>
       match d with
       | type_inl _ _ d0 => morphism D s0 d0
       | type_inr _ _ _ => Empty
       end
   | type_inr _ _ s0 =>
       match d with
       | type_inl _ _ _ => Empty
       | type_inr _ _ d0 => morphism C s0 d0
       end
   end ->
   match GO s with
   | type_inl _ _ s0 =>
       match GO d with
       | type_inl _ _ d0 => morphism D s0 d0
       | type_inr _ _ _ => Empty
       end
   | type_inr _ _ s0 =>
       match GO d with
       | type_inl _ _ _ => Empty
       | type_inr _ _ d0 => morphism C s0 d0
       end
   end)
  (path_forall
     (fun c : (D + C)%category =>
      ((swap C D) _0 ((swap D C) _0 c))%object) idmap
     swap_involutive_helper)
  (fun (s d : D + C)
     (m : match s with
          | type_inl _ _ s0 =>
              match d with
              | type_inl _ _ d0 => morphism D s0 d0
              | type_inr _ _ _ => Empty
              end
          | type_inr _ _ s0 =>
              match d with
              | type_inl _ _ _ => Empty
              | type_inr _ _ d0 => morphism C s0 d0
              end
          end) =>
   match
     match s with
     | type_inl _ _ c => type_inr C c
     | type_inr _ _ c' => type_inl D c'
     end as s0
     return
       (match s0 with
        | type_inl _ _ s1 =>
            match
              match d with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ d0 => morphism C s1 d0
            | type_inr _ _ _ => Empty
            end
        | type_inr _ _ s1 =>
            match
              match d with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d0 => morphism D s1 d0
            end
        end ->
        match
          match s0 with
          | type_inl _ _ c => type_inr D c
          | type_inr _ _ c' => type_inl C c'
          end
        with
        | type_inl _ _ s1 =>
            match
              match
                match d with
                | type_inl _ _ c => type_inr C c
                | type_inr _ _ c' => type_inl D c'
                end
              with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ d0 => morphism D s1 d0
            | type_inr _ _ _ => Empty
            end
        | type_inr _ _ s1 =>
            match
              match
                match d with
                | type_inl _ _ c => type_inr C c
                | type_inr _ _ c' => type_inl D c'
                end
              with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d0 => morphism C s1 d0
            end
        end)
   with
   | type_inl _ _ cs =>
       match
         match d with
         | type_inl _ _ c => type_inr C c
         | type_inr _ _ c' => type_inl D c'
         end as d0
         return
           (match d0 with
            | type_inl _ _ d1 => morphism C cs d1
            | type_inr _ _ _ => Empty
            end ->
            match
              match d0 with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d1 => morphism C cs d1
            end)
       with
       | type_inl _ _ cd => idmap
       | type_inr _ _ _ =>
           fun m0 : Empty =>
           match m0 return Empty with
           end
       end
   | type_inr _ _ c's =>
       match
         match d with
         | type_inl _ _ c => type_inr C c
         | type_inr _ _ c' => type_inl D c'
         end as d0
         return
           (match d0 with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d1 => morphism D c's d1
            end ->
            match
              match d0 with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ d1 => morphism D c's d1
            | type_inr _ _ _ => Empty
            end)
       with
       | type_inl _ _ _ =>
           fun m0 : Empty =>
           match m0 return Empty with
           end
       | type_inr _ _ c'd => idmap
       end
   end
     (match
        s as s0
        return
          (match s0 with
           | type_inl _ _ s1 =>
               match d with
               | type_inl _ _ d0 => morphism D s1 d0
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s1 =>
               match d with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism C s1 d0
               end
           end ->
           match
             match s0 with
             | type_inl _ _ c => type_inr C c
             | type_inr _ _ c' => type_inl D c'
             end
           with
           | type_inl _ _ s1 =>
               match
                 match d with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ d0 => morphism C s1 d0
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s1 =>
               match
                 match d with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism D s1 d0
               end
           end)
      with
      | type_inl _ _ cs =>
          match
            d as d0
            return
              (match d0 with
               | type_inl _ _ d1 => morphism D cs d1
               | type_inr _ _ _ => Empty
               end ->
               match
                 match d0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d1 => morphism D cs d1
               end)
          with
          | type_inl _ _ cd => idmap
          | type_inr _ _ _ =>
              fun m0 : Empty =>
              match m0 return Empty with
              end
          end
      | type_inr _ _ c's =>
          match
            d as d0
            return
              (match d0 with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d1 => morphism C c's d1
               end ->
               match
                 match d0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ d1 => morphism C c's d1
               | type_inr _ _ _ => Empty
               end)
          with
          | type_inl _ _ _ =>
              fun m0 : Empty =>
              match m0 return Empty with
              end
          | type_inr _ _ c'd => idmap
          end
      end m)) x x0 x1 = x1
    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.
H: Funext
C, D: PreCategory
x, x0: D + C
x1: match x with
| type_inl _ _ s =>
    match x0 with
    | type_inl _ _ d => morphism D s d
    | type_inr _ _ _ => Empty
    end
| type_inr _ _ s =>
    match x0 with
    | type_inl _ _ _ => Empty
    | type_inr _ _ d => morphism C s d
    end
end
transport
  (fun x1 : D + C -> D + C =>
   match x1 x with
   | type_inl _ _ s =>
       match x1 x0 with
       | type_inl _ _ d => morphism D s d
       | type_inr _ _ _ => Empty
       end
   | type_inr _ _ s =>
       match x1 x0 with
       | type_inl _ _ _ => Empty
       | type_inr _ _ d => morphism C s d
       end
   end)
  (path_forall
     (fun c : D + C =>
      match
        match c with
        | type_inl _ _ c0 => type_inr C c0
        | type_inr _ _ c' => type_inl D c'
        end
      with
      | type_inl _ _ c0 => type_inr D c0
      | type_inr _ _ c' => type_inl C c'
      end) idmap swap_involutive_helper)
  (match
     match x with
     | type_inl _ _ c => type_inr C c
     | type_inr _ _ c' => type_inl D c'
     end as s
     return
       (match s with
        | type_inl _ _ s0 =>
            match
              match x0 with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ d => morphism C s0 d
            | type_inr _ _ _ => Empty
            end
        | type_inr _ _ s0 =>
            match
              match x0 with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d => morphism D s0 d
            end
        end ->
        match
          match s with
          | type_inl _ _ c => type_inr D c
          | type_inr _ _ c' => type_inl C c'
          end
        with
        | type_inl _ _ s0 =>
            match
              match
                match x0 with
                | type_inl _ _ c => type_inr C c
                | type_inr _ _ c' => type_inl D c'
                end
              with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ d => morphism D s0 d
            | type_inr _ _ _ => Empty
            end
        | type_inr _ _ s0 =>
            match
              match
                match x0 with
                | type_inl _ _ c => type_inr C c
                | type_inr _ _ c' => type_inl D c'
                end
              with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d => morphism C s0 d
            end
        end)
   with
   | type_inl _ _ cs =>
       match
         match x0 with
         | type_inl _ _ c => type_inr C c
         | type_inr _ _ c' => type_inl D c'
         end as d
         return
           (match d with
            | type_inl _ _ d0 => morphism C cs d0
            | type_inr _ _ _ => Empty
            end ->
            match
              match d with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d0 => morphism C cs d0
            end)
       with
       | type_inl _ _ cd => idmap
       | type_inr _ _ _ =>
           fun m : Empty =>
           match m return Empty with
           end
       end
   | type_inr _ _ c's =>
       match
         match x0 with
         | type_inl _ _ c => type_inr C c
         | type_inr _ _ c' => type_inl D c'
         end as d
         return
           (match d with
            | type_inl _ _ _ => Empty
            | type_inr _ _ d0 => morphism D c's d0
            end ->
            match
              match d with
              | type_inl _ _ c => type_inr D c
              | type_inr _ _ c' => type_inl C c'
              end
            with
            | type_inl _ _ d0 => morphism D c's d0
            | type_inr _ _ _ => Empty
            end)
       with
       | type_inl _ _ _ =>
           fun m : Empty =>
           match m return Empty with
           end
       | type_inr _ _ c'd => idmap
       end
   end
     (match
        x as s
        return
          (match s with
           | type_inl _ _ s0 =>
               match x0 with
               | type_inl _ _ d => morphism D s0 d
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s0 =>
               match x0 with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d => morphism C s0 d
               end
           end ->
           match
             match s with
             | type_inl _ _ c => type_inr C c
             | type_inr _ _ c' => type_inl D c'
             end
           with
           | type_inl _ _ s0 =>
               match
                 match x0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ d => morphism C s0 d
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s0 =>
               match
                 match x0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d => morphism D s0 d
               end
           end)
      with
      | type_inl _ _ cs =>
          match
            x0 as d
            return
              (match d with
               | type_inl _ _ d0 => morphism D cs d0
               | type_inr _ _ _ => Empty
               end ->
               match
                 match d with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism D cs d0
               end)
          with
          | type_inl _ _ cd => idmap
          | type_inr _ _ _ =>
              fun m : Empty =>
              match m return Empty with
              end
          end
      | type_inr _ _ c's =>
          match
            x0 as d
            return
              (match d with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism C c's d0
               end ->
               match
                 match d with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ d0 => morphism C c's d0
               | type_inr _ _ _ => Empty
               end)
          with
          | type_inl _ _ _ =>
              fun m : Empty =>
              match m return Empty with
              end
          | type_inr _ _ c'd => idmap
          end
      end x1)) = x1
    transport_path_forall_hammer.
H: Funext
C, D: PreCategory
x, x0: D + C
x1: match x with
| type_inl _ _ s =>
    match x0 with
    | type_inl _ _ d => morphism D s d
    | type_inr _ _ _ => Empty
    end
| type_inr _ _ s =>
    match x0 with
    | type_inl _ _ _ => Empty
    | type_inr _ _ d => morphism C s d
    end
end
transport
  (fun y : D + C =>
   match x with
   | type_inl _ _ s =>
       match y with
       | type_inl _ _ d => morphism D s d
       | type_inr _ _ _ => Empty
       end
   | type_inr _ _ s =>
       match y with
       | type_inl _ _ _ => Empty
       | type_inr _ _ d => morphism C s d
       end
   end) (swap_involutive_helper x0)
  (transport
     (fun y : D + C =>
      match y with
      | type_inl _ _ s =>
          match
            match
              match x0 with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ c => type_inr D c
            | type_inr _ _ c' => type_inl C c'
            end
          with
          | type_inl _ _ d => morphism D s d
          | type_inr _ _ _ => Empty
          end
      | type_inr _ _ s =>
          match
            match
              match x0 with
              | type_inl _ _ c => type_inr C c
              | type_inr _ _ c' => type_inl D c'
              end
            with
            | type_inl _ _ c => type_inr D c
            | type_inr _ _ c' => type_inl C c'
            end
          with
          | type_inl _ _ _ => Empty
          | type_inr _ _ d => morphism C s d
          end
      end) (swap_involutive_helper x)
     (match
        match x with
        | type_inl _ _ c => type_inr C c
        | type_inr _ _ c' => type_inl D c'
        end as s
        return
          (match s with
           | type_inl _ _ s0 =>
               match
                 match x0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ d => morphism C s0 d
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s0 =>
               match
                 match x0 with
                 | type_inl _ _ c => type_inr C c
                 | type_inr _ _ c' => type_inl D c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d => morphism D s0 d
               end
           end ->
           match
             match s with
             | type_inl _ _ c => type_inr D c
             | type_inr _ _ c' => type_inl C c'
             end
           with
           | type_inl _ _ s0 =>
               match
                 match
                   match x0 with
                   | type_inl _ _ c => type_inr C c
                   | type_inr _ _ c' => type_inl D c'
                   end
                 with
                 | type_inl _ _ c => type_inr D c
                 | type_inr _ _ c' => type_inl C c'
                 end
               with
               | type_inl _ _ d => morphism D s0 d
               | type_inr _ _ _ => Empty
               end
           | type_inr _ _ s0 =>
               match
                 match
                   match x0 with
                   | type_inl _ _ c => type_inr C c
                   | type_inr _ _ c' => type_inl D c'
                   end
                 with
                 | type_inl _ _ c => type_inr D c
                 | type_inr _ _ c' => type_inl C c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d => morphism C s0 d
               end
           end)
      with
      | type_inl _ _ cs =>
          match
            match x0 with
            | type_inl _ _ c => type_inr C c
            | type_inr _ _ c' => type_inl D c'
            end as d
            return
              (match d with
               | type_inl _ _ d0 => morphism C cs d0
               | type_inr _ _ _ => Empty
               end ->
               match
                 match d with
                 | type_inl _ _ c => type_inr D c
                 | type_inr _ _ c' => type_inl C c'
                 end
               with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism C cs d0
               end)
          with
          | type_inl _ _ cd => idmap
          | type_inr _ _ _ =>
              fun m : Empty =>
              match m return Empty with
              end
          end
      | type_inr _ _ c's =>
          match
            match x0 with
            | type_inl _ _ c => type_inr C c
            | type_inr _ _ c' => type_inl D c'
            end as d
            return
              (match d with
               | type_inl _ _ _ => Empty
               | type_inr _ _ d0 => morphism D c's d0
               end ->
               match
                 match d with
                 | type_inl _ _ c => type_inr D c
                 | type_inr _ _ c' => type_inl C c'
                 end
               with
               | type_inl _ _ d0 => morphism D c's d0
               | type_inr _ _ _ => Empty
               end)
          with
          | type_inl _ _ _ =>
              fun m : Empty =>
              match m return Empty with
              end
          | type_inr _ _ c'd => idmap
          end
      end
        (match
           x as s
           return
             (match s with
              | type_inl _ _ s0 =>
                  match x0 with
                  | type_inl _ _ d => morphism D s0 d
                  | type_inr _ _ _ => Empty
                  end
              | type_inr _ _ s0 =>
                  match x0 with
                  | type_inl _ _ _ => Empty
                  | type_inr _ _ d => morphism C s0 d
                  end
              end ->
              match
                match s with
                | type_inl _ _ c => type_inr C c
                | type_inr _ _ c' => type_inl D c'
                end
              with
              | type_inl _ _ s0 =>
                  match
                    match x0 with
                    | type_inl _ _ c => type_inr C c
                    | type_inr _ _ c' => type_inl D c'
                    end
                  with
                  | type_inl _ _ d => morphism C s0 d
                  | type_inr _ _ _ => Empty
                  end
              | type_inr _ _ s0 =>
                  match
                    match x0 with
                    | type_inl _ _ c => type_inr C c
                    | type_inr _ _ c' => type_inl D c'
                    end
                  with
                  | type_inl _ _ _ => Empty
                  | type_inr _ _ d => morphism D s0 d
                  end
              end)
         with
         | type_inl _ _ cs =>
             match
               x0 as d
               return
                 (match d with
                  | type_inl _ _ d0 =>
                      morphism D cs d0
                  | type_inr _ _ _ => Empty
                  end ->
                  match
                    match d with
                    | type_inl _ _ c => type_inr C c
                    | type_inr _ _ c' => type_inl D c'
                    end
                  with
                  | type_inl _ _ _ => Empty
                  | type_inr _ _ d0 =>
                      morphism D cs d0
                  end)
             with
             | type_inl _ _ cd => idmap
             | type_inr _ _ _ =>
                 fun m : Empty =>
                 match m return Empty with
                 end
             end
         | type_inr _ _ c's =>
             match
               x0 as d
               return
                 (match d with
                  | type_inl _ _ _ => Empty
                  | type_inr _ _ d0 =>
                      morphism C c's d0
                  end ->
                  match
                    match d with
                    | type_inl _ _ c => type_inr C c
                    | type_inr _ _ c' => type_inl D c'
                    end
                  with
                  | type_inl _ _ d0 =>
                      morphism C c's d0
                  | type_inr _ _ _ => Empty
                  end)
             with
             | type_inl _ _ _ =>
                 fun m : Empty =>
                 match m return Empty with
                 end
             | type_inr _ _ c'd => idmap
             end
         end x1))) = x1
      by repeat match goal with
                  | [ H : Empty |- _ ] => destruct H
                  | [ H : (_ + _)%type |- _ ] => destruct H
                  | _ => progress hnf in *
                end.
  Qed.
End swap_functor.

Module Export FunctorSumNotations.
  Notation "F + G" := (sum F G) : functor_scope.
End FunctorSumNotations.