Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(** * Functors involving coproduct categories *)
[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 Notationtype_inl := inl.Local Notationtype_inr := inr.(** ** Injections [inl : C → C + D] and [inr : D → C + D] *)Sectionsum_functors.VariablesCD : PreCategory.Definitioninl : Functor C (C + D)
:= Build_Functor C (C + D)
(@inl _ _)
(fun__m => m)
(fun_____ => idpath)
(fun_ => idpath).Definitioninr : Functor D (C + D)
:= Build_Functor D (C + D)
(@inr _ _)
(fun__m => m)
(fun_____ => idpath)
(fun_ => idpath).Endsum_functors.(** ** Coproduct of functors [F + F' : C + C' → D] *)Sectionsum.VariablesCC'D : PreCategory.
C, C', D: PreCategory 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
refine (Build_Functor
(C + C') D
(funcc'
=> match cc' with
| type_inl c => F c
| type_inr c' => F' c'
end)
(funsd
=> match s, d with
| type_inl cs, type_inl cd
=> funm : morphism _ cs cd => F _1 m
| type_inr c's, type_inr c'd
=> funm : morphism _ c's c'd => F' _1 m
| _, _ => funm => match m withendend%morphism)
_
_);
abstract (
repeat (intros [] || intro);
simplin *;
auto with functor
).Defined.Endsum.(** ** swap : [C + D → D + C] *)Sectionswap_functor.DefinitionswapCD
: Functor (C + D) (D + C)
:= sum (inr _ _) (inl _ _).LocalOpen Scope functor_scope.Definitionswap_involutive_helper {CD} c
: (swap C D) ((swap D C) c)
= c
:= match c with type_inl _ => idpath | type_inr _ => idpath end.
H: Funext C, D: PreCategory
swap C D o swap D C = 1
H: Funext C, D: PreCategory
swap C D o swap D C = 1
H: Funext C, D: PreCategory
{HO
: (func : D + C =>
matchmatch c with
| type_inl _ _ c0 => type_inr C c0
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c0 => type_inr D c0
| type_inr _ _ c' => type_inl C c'
end) = idmap &
transport
(funGO : D + C -> D + C =>
forallsd : 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
endend ->
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
endend) HO
(fun (sd : 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
endend) =>
matchmatch s with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas s0
return
(match s0 with
| type_inl _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d0 => morphism C s1 d0
| type_inr _ _ _ => Empty
end
| type_inr _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism D s1 d0
endend ->
matchmatch s0 with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ s1 =>
matchmatchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d0 => morphism D s1 d0
| type_inr _ _ _ => Empty
end
| type_inr _ _ s1 =>
matchmatchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism C s1 d0
endend)
with
| type_inl _ _ cs =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d0
return
(match d0 with
| type_inl _ _ d1 => morphism C cs d1
| type_inr _ _ _ => Empty
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism C cs d1
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm0 : Empty =>
match m0 return Empty withendend
| type_inr _ _ c's =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d0
return
(match d0 with
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism D c's d1
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d1 => morphism D c's d1
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm0 : Empty =>
match m0 return Empty withend
| type_inr _ _ c'd => idmap
endend
(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
endend ->
matchmatch s0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d0 => morphism C s1 d0
| type_inr _ _ _ => Empty
end
| type_inr _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism D s1 d0
endend)
with
| type_inl _ _ cs =>
match
d as d0
return
(match d0 with
| type_inl _ _ d1 => morphism D cs d1
| type_inr _ _ _ => Empty
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism D cs d1
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm0 : Empty =>
match m0 return Empty withendend
| type_inr _ _ c's =>
match
d as d0
return
(match d0 with
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism C c's d1
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d1 => morphism C c's d1
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm0 : Empty =>
match m0 return Empty withend
| type_inr _ _ c'd => idmap
endend m)) = (funsd : D + C => idmap)}
H: Funext C, D: PreCategory
transport
(funGO : D + C -> D + C =>
forallsd : 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
endend ->
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
endend)
(path_forall
(func : (D + C)%category =>
((swap C D) _0 ((swap D C) _0 c))%object) idmap
swap_involutive_helper)
(fun (sd : 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
endend) =>
matchmatch s with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas s0
return
(match s0 with
| type_inl _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d0 => morphism C s1 d0
| type_inr _ _ _ => Empty
end
| type_inr _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism D s1 d0
endend ->
matchmatch s0 with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ s1 =>
matchmatchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d0 => morphism D s1 d0
| type_inr _ _ _ => Empty
end
| type_inr _ _ s1 =>
matchmatchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism C s1 d0
endend)
with
| type_inl _ _ cs =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d0
return
(match d0 with
| type_inl _ _ d1 => morphism C cs d1
| type_inr _ _ _ => Empty
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism C cs d1
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm0 : Empty =>
match m0 return Empty withendend
| type_inr _ _ c's =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d0
return
(match d0 with
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism D c's d1
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d1 => morphism D c's d1
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm0 : Empty =>
match m0 return Empty withend
| type_inr _ _ c'd => idmap
endend
(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
endend ->
matchmatch s0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d0 => morphism C s1 d0
| type_inr _ _ _ => Empty
end
| type_inr _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism D s1 d0
endend)
with
| type_inl _ _ cs =>
match
d as d0
return
(match d0 with
| type_inl _ _ d1 => morphism D cs d1
| type_inr _ _ _ => Empty
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism D cs d1
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm0 : Empty =>
match m0 return Empty withendend
| type_inr _ _ c's =>
match
d as d0
return
(match d0 with
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism C c's d1
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d1 => morphism C c's d1
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm0 : Empty =>
match m0 return Empty withend
| type_inr _ _ c'd => idmap
endend m)) = (funsd : D + C => idmap)
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
endend
transport
(funGO : D + C -> D + C =>
forallsd : 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
endend ->
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
endend)
(path_forall
(func : (D + C)%category =>
((swap C D) _0 ((swap D C) _0 c))%object) idmap
swap_involutive_helper)
(fun (sd : 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
endend) =>
matchmatch s with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas s0
return
(match s0 with
| type_inl _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d0 => morphism C s1 d0
| type_inr _ _ _ => Empty
end
| type_inr _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism D s1 d0
endend ->
matchmatch s0 with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ s1 =>
matchmatchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d0 => morphism D s1 d0
| type_inr _ _ _ => Empty
end
| type_inr _ _ s1 =>
matchmatchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism C s1 d0
endend)
with
| type_inl _ _ cs =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d0
return
(match d0 with
| type_inl _ _ d1 => morphism C cs d1
| type_inr _ _ _ => Empty
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism C cs d1
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm0 : Empty =>
match m0 return Empty withendend
| type_inr _ _ c's =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d0
return
(match d0 with
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism D c's d1
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d1 => morphism D c's d1
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm0 : Empty =>
match m0 return Empty withend
| type_inr _ _ c'd => idmap
endend
(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
endend ->
matchmatch s0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d0 => morphism C s1 d0
| type_inr _ _ _ => Empty
end
| type_inr _ _ s1 =>
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism D s1 d0
endend)
with
| type_inl _ _ cs =>
match
d as d0
return
(match d0 with
| type_inl _ _ d1 => morphism D cs d1
| type_inr _ _ _ => Empty
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism D cs d1
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm0 : Empty =>
match m0 return Empty withendend
| type_inr _ _ c's =>
match
d as d0
return
(match d0 with
| type_inl _ _ _ => Empty
| type_inr _ _ d1 => morphism C c's d1
end ->
matchmatch d0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d1 => morphism C c's d1
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm0 : Empty =>
match m0 return Empty withend
| type_inr _ _ c'd => idmap
endend m)) x x0 x1 = x1
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
endend
transport
(funx1 : 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
endend)
(path_forall
(func : D + C =>
matchmatch c with
| type_inl _ _ c0 => type_inr C c0
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c0 => type_inr D c0
| type_inr _ _ c' => type_inl C c'
end) idmap swap_involutive_helper)
(matchmatch x with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas s
return
(match s with
| type_inl _ _ s0 =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d => morphism C s0 d
| type_inr _ _ _ => Empty
end
| type_inr _ _ s0 =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d => morphism D s0 d
endend ->
matchmatch s with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ s0 =>
matchmatchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d => morphism D s0 d
| type_inr _ _ _ => Empty
end
| type_inr _ _ s0 =>
matchmatchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d => morphism C s0 d
endend)
with
| type_inl _ _ cs =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d
return
(match d with
| type_inl _ _ d0 => morphism C cs d0
| type_inr _ _ _ => Empty
end ->
matchmatch d with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism C cs d0
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm : Empty =>
match m return Empty withendend
| type_inr _ _ c's =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d
return
(match d with
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism D c's d0
end ->
matchmatch d with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d0 => morphism D c's d0
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm : Empty =>
match m return Empty withend
| type_inr _ _ c'd => idmap
endend
(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
endend ->
matchmatch s with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ s0 =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d => morphism C s0 d
| type_inr _ _ _ => Empty
end
| type_inr _ _ s0 =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d => morphism D s0 d
endend)
with
| type_inl _ _ cs =>
match
x0 as d
return
(match d with
| type_inl _ _ d0 => morphism D cs d0
| type_inr _ _ _ => Empty
end ->
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism D cs d0
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm : Empty =>
match m return Empty withendend
| type_inr _ _ c's =>
match
x0 as d
return
(match d with
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism C c's d0
end ->
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d0 => morphism C c's d0
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm : Empty =>
match m return Empty withend
| type_inr _ _ c'd => idmap
endend x1)) = x1
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
endend
transport
(funy : 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
endend) (swap_involutive_helper x0)
(transport
(funy : D + C =>
match y with
| type_inl _ _ s =>
matchmatchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d => morphism D s d
| type_inr _ _ _ => Empty
end
| type_inr _ _ s =>
matchmatchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d => morphism C s d
endend) (swap_involutive_helper x)
(matchmatch x with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas s
return
(match s with
| type_inl _ _ s0 =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d => morphism C s0 d
| type_inr _ _ _ => Empty
end
| type_inr _ _ s0 =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d => morphism D s0 d
endend ->
matchmatch s with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ s0 =>
matchmatchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d => morphism D s0 d
| type_inr _ _ _ => Empty
end
| type_inr _ _ s0 =>
matchmatchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d => morphism C s0 d
endend)
with
| type_inl _ _ cs =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d
return
(match d with
| type_inl _ _ d0 => morphism C cs d0
| type_inr _ _ _ => Empty
end ->
matchmatch d with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism C cs d0
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm : Empty =>
match m return Empty withendend
| type_inr _ _ c's =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endas d
return
(match d with
| type_inl _ _ _ => Empty
| type_inr _ _ d0 => morphism D c's d0
end ->
matchmatch d with
| type_inl _ _ c => type_inr D c
| type_inr _ _ c' => type_inl C c'
endwith
| type_inl _ _ d0 => morphism D c's d0
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm : Empty =>
match m return Empty withend
| type_inr _ _ c'd => idmap
endend
(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
endend ->
matchmatch s with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ s0 =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d => morphism C s0 d
| type_inr _ _ _ => Empty
end
| type_inr _ _ s0 =>
matchmatch x0 with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d => morphism D s0 d
endend)
with
| type_inl _ _ cs =>
match
x0 as d
return
(match d with
| type_inl _ _ d0 =>
morphism D cs d0
| type_inr _ _ _ => Empty
end ->
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ _ => Empty
| type_inr _ _ d0 =>
morphism D cs d0
end)
with
| type_inl _ _ cd => idmap
| type_inr _ _ _ =>
funm : Empty =>
match m return Empty withendend
| type_inr _ _ c's =>
match
x0 as d
return
(match d with
| type_inl _ _ _ => Empty
| type_inr _ _ d0 =>
morphism C c's d0
end ->
matchmatch d with
| type_inl _ _ c => type_inr C c
| type_inr _ _ c' => type_inl D c'
endwith
| type_inl _ _ d0 =>
morphism C c's d0
| type_inr _ _ _ => Empty
end)
with
| type_inl _ _ _ =>
funm : Empty =>
match m return Empty withend
| type_inr _ _ c'd => idmap
endend x1))) = x1
byrepeatmatch goal with
| [ H : Empty |- _ ] => destruct H
| [ H : (_ + _)%type |- _ ] => destruct H
| _ => progresshnfin *
end.Qed.Endswap_functor.ModuleExport FunctorSumNotations.Notation"F + G" := (sum F G) : functor_scope.EndFunctorSumNotations.