Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.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.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Forall Types.Arrow Types.Sigma Types.Sum Types.Universe.Require Export Colimits.Coeq.Require Import Homotopy.IdentitySystems.LocalOpen Scope path_scope.(** * Homotopy Pushouts *)(** We define pushouts in terms of coproducts and coequalizers. *)DefinitionPushout@{i j k l} {A : Type@{i}} {B : Type@{j}} {C : Type@{k}}
(f : A -> B) (g : A -> C) : Type@{l}
:= Coeq@{l l _} (inl o f) (inr o g).Definitionpush {ABC : Type} {f : A -> B} {g : A -> C}
: B+C -> Pushout f g
:= @coeq _ _ (inl o f) (inr o g).Definitionpushl {ABC} {f : A -> B} {g : A -> C} (b : B)
: Pushout f g := push (inl b).Definitionpushr {ABC} {f : A -> B} {g : A -> C} (c : C)
: Pushout f g := push (inr c).Definitionpglue {ABC : Type} {f : A -> B} {g : A -> C} (a : A)
: pushl (f a) = pushr (g a)
:= @cglue A (B+C) (inl o f) (inr o g) a.(* Some versions with explicit parameters. *)Definitionpushl' {ABC} (f : A -> B) (g : A -> C) (b : B) : Pushout f g := pushl b.Definitionpushr' {ABC} (f : A -> B) (g : A -> C) (c : C) : Pushout f g := pushr c.Definitionpglue' {ABC : Type} (f : A -> B) (g : A -> C) (a : A) : pushl (f a) = pushr (g a)
:= pglue a.SectionPushoutInd.Context {ABC : Type} {f : A -> B} {g : A -> C}
(P : Pushout f g -> Type)
(pushb : forallb : B, P (pushl b))
(pushc : forallc : C, P (pushr c))
(pusha : foralla : A, (pglue a) # (pushb (f a)) = pushc (g a)).DefinitionPushout_ind
: forall (w : Pushout f g), P w
:= Coeq_ind P (sum_ind (P o push) pushb pushc) pusha.DefinitionPushout_ind_beta_pushl (b:B) : Pushout_ind (pushl b) = pushb b
:= 1.DefinitionPushout_ind_beta_pushr (c:C) : Pushout_ind (pushr c) = pushc c
:= 1.DefinitionPushout_ind_beta_pglue (a:A)
: apD Pushout_ind (pglue a) = pusha a
:= Coeq_ind_beta_cglue P (funbc => match bc with inl b => pushb b | inr c => pushc c end) pusha a.EndPushoutInd.(** But we want to allow the user to forget that we've defined pushouts in terms of coequalizers. *)Arguments Pushout : simpl never.Arguments push : simpl never.Arguments pglue : simpl never.Arguments Pushout_ind_beta_pglue : simpl never.(** However, we do allow [Pushout_ind] to simplify, as it computes on point constructors. *)DefinitionPushout_rec {ABC} {f : A -> B} {g : A -> C} (P : Type)
(pushb : B -> P)
(pushc : C -> P)
(pusha : foralla : A, pushb (f a) = pushc (g a))
: @Pushout A B C f g -> P
:= @Coeq_rec _ _ (inl o f) (inr o g) P (sum_rec P pushb pushc) pusha.
A, B, C: Type f: A -> B g: A -> C P: Type pushb: B -> P pushc: C -> P pusha: foralla : A, pushb (f a) = pushc (g a) a: A
ap (Pushout_rec P pushb pushc pusha) (pglue a) =
pusha a
A, B, C: Type f: A -> B g: A -> C P: Type pushb: B -> P pushc: C -> P pusha: foralla : A, pushb (f a) = pushc (g a) a: A
ap (Pushout_rec P pushb pushc pusha) (pglue a) =
pusha a
A, B, C, P: Type f: A -> B g: A -> C h: Pushout f g -> P
foralla : A,
fst
(funx : B => h (pushl x), funx : C => h (pushr x))
(f a) =
snd
(funx : B => h (pushl x), funx : C => h (pushr x))
(g a)
A, B, C, P: Type f: A -> B g: A -> C h: Pushout f g -> P a: A
h (pushl (f a)) = h (pushr (g a))
exact (ap h (pglue a)).Defined.
A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P
Pushout_rec P (e o pushl) (e o pushr)
(funa : A => ap e (pglue a)) == e
A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P
Pushout_rec P (e o pushl) (e o pushr)
(funa : A => ap e (pglue a)) == e
A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P
forallb : B,
(funw : Pushout f g =>
Pushout_rec P (e o pushl) (e o pushr)
(funa : A => ap e (pglue a)) w = e w) (pushl b)
A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P
forallc : C,
(funw : Pushout f g =>
Pushout_rec P (e o pushl) (e o pushr)
(funa : A => ap e (pglue a)) w = e w) (pushr c)
A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P
foralla : A,
transport
(funw : Pushout f g =>
Pushout_rec P (e o pushl) (e o pushr)
(funa0 : A => ap e (pglue a0)) w = e w)
(pglue a) (?pushb (f a)) = ?pushc (g a)
A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P
foralla : A,
transport
(funw : Pushout f g =>
Pushout_rec P (e o pushl) (e o pushr)
(funa0 : A => ap e (pglue a0)) w = e w)
(pglue a) ((funb : B => 1) (f a)) =
(func : C => 1) (g a)
A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P a: A
transport
(funw : Pushout f g =>
Pushout_rec P (funx : B => e (pushl x))
(funx : C => e (pushr x))
(funa : A => ap e (pglue a)) w = e w) (pglue a)
1 = 1
A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P a: A
ap
(Pushout_rec P (funx : B => e (pushl x))
(funx : C => e (pushr x))
(funa : A => ap e (pglue a))) (pglue a) @ 1 =
1 @ ap e (pglue a)
A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P a: A
ap
(Pushout_rec P (funx : B => e (pushl x))
(funx : C => e (pushr x))
(funa : A => ap e (pglue a))) (pglue a) =
ap e (pglue a)
napply Pushout_rec_beta_pglue.Defined.
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type
(funp : {psh : (B -> P) * (C -> P) &
foralla : A, fst psh (f a) = snd psh (g a)} =>
Pushout_rec P (fst p.1) (snd p.1) p.2)
o pushout_unrec f g == idmap
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type
pushout_unrec f g
o (funp : {psh : (B -> P) * (C -> P) &
foralla : A, fst psh (f a) = snd psh (g a)}
=> Pushout_rec P (fst p.1) (snd p.1) p.2) == idmap
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type
(funp : {psh : (B -> P) * (C -> P) &
foralla : A, fst psh (f a) = snd psh (g a)} =>
Pushout_rec P (fst p.1) (snd p.1) p.2)
o pushout_unrec f g == idmap
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P
Pushout_rec P (fst (pushout_unrec f g e).1)
(snd (pushout_unrec f g e).1)
(pushout_unrec f g e).2 = e
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type e: Pushout f g -> P
Pushout_rec P (fst (pushout_unrec f g e).1)
(snd (pushout_unrec f g e).1)
(pushout_unrec f g e).2 == e
apply pushout_rec_unrec.
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type
pushout_unrec f g
o (funp : {psh : (B -> P) * (C -> P) &
foralla : A, fst psh (f a) = snd psh (g a)}
=> Pushout_rec P (fst p.1) (snd p.1) p.2) == idmap
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type pushb: B -> P pushc: C -> P pusha: foralla : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
((funx : B =>
Pushout_rec P pushb pushc pusha (pushl x),
funx : C =>
Pushout_rec P pushb pushc pusha (pushr x));
funa : A =>
ap (Pushout_rec P pushb pushc pusha) (pglue a)) =
((pushb, pushc); pusha)
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type pushb: B -> P pushc: C -> P pusha: foralla : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
(funx : B =>
Pushout_rec P pushb pushc pusha (pushl x),
funx : C => Pushout_rec P pushb pushc pusha (pushr x)) =
(pushb, pushc)
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type pushb: B -> P pushc: C -> P pusha: foralla : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
transport
(funpsh : (B -> P) * (C -> P) =>
foralla : A, fst psh (f a) = snd psh (g a))
?p
(funa : A =>
ap (Pushout_rec P pushb pushc pusha) (pglue a)) =
pusha
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type pushb: B -> P pushc: C -> P pusha: foralla : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
(funx : B =>
Pushout_rec P pushb pushc pusha (pushl x),
funx : C => Pushout_rec P pushb pushc pusha (pushr x)) =
(pushb, pushc)
reflexivity.
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type pushb: B -> P pushc: C -> P pusha: foralla : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
transport
(funpsh : (B -> P) * (C -> P) =>
foralla : A, fst psh (f a) = snd psh (g a)) 1
(funa : A =>
ap (Pushout_rec P pushb pushc pusha) (pglue a)) =
pusha
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type pushb: B -> P pushc: C -> P pusha: foralla : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
(funa : A =>
ap (Pushout_rec P pushb pushc pusha) (pglue a)) =
pusha
H: Funext A, B, C: Type f: A -> B g: A -> C P: Type pushb: B -> P pushc: C -> P pusha: foralla : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a) a: A
ap (Pushout_rec P pushb pushc pusha) (pglue a) =
pusha a
apply Pushout_rec_beta_pglue.Defined.Definitionequiv_Pushout_rec `{Funext} {A B C} (f : A -> B) (g : A -> C) P
: {psh : (B -> P) * (C -> P) &
foralla, fst psh (f a) = snd psh (g a) }
<~> (Pushout f g -> P)
:= Build_Equiv _ _ _ (isequiv_Pushout_rec f g P).Definitionequiv_pushout_unrec `{Funext} {A B C} (f : A -> B) (g : A -> C) P
: (Pushout f g -> P)
<~> {psh : (B -> P) * (C -> P) &
foralla, fst psh (f a) = snd psh (g a) }
:= equiv_inverse (equiv_Pushout_rec f g P).(** ** Symmetry *)Definitionpushout_sym_map {ABC} {f : A -> B} {g : A -> C}
: Pushout f g -> Pushout g f
:= Pushout_rec (Pushout g f) pushr pushl (funa : A => (pglue a)^).
A, B, C: Type f: A -> B g: A -> C
pushout_sym_map o pushout_sym_map == idmap
A, B, C: Type f: A -> B g: A -> C
pushout_sym_map o pushout_sym_map == idmap
A, B, C: Type f: A -> B g: A -> C
forallb : C,
(funw : Pushout g f =>
(pushout_sym_map o pushout_sym_map) w = idmap w)
(pushl b)
A, B, C: Type f: A -> B g: A -> C
forallc : B,
(funw : Pushout g f =>
(pushout_sym_map o pushout_sym_map) w = idmap w)
(pushr c)
A, B, C: Type f: A -> B g: A -> C
foralla : A,
transport
(funw : Pushout g f =>
(pushout_sym_map o pushout_sym_map) w = idmap w)
(pglue a) (?pushb (g a)) = ?pushc (f a)
A, B, C: Type f: A -> B g: A -> C
forallb : C,
(funw : Pushout g f =>
(pushout_sym_map o pushout_sym_map) w = idmap w)
(pushl b)
intros; reflexivity.
A, B, C: Type f: A -> B g: A -> C
forallc : B,
(funw : Pushout g f =>
(pushout_sym_map o pushout_sym_map) w = idmap w)
(pushr c)
intros; reflexivity.
A, B, C: Type f: A -> B g: A -> C
foralla : A,
transport
(funw : Pushout g f =>
(pushout_sym_map o pushout_sym_map) w = idmap w)
(pglue a) ((funb : C => 1) (g a)) =
(func : B => 1) (f a)
A, B, C: Type f: A -> B g: A -> C a: A
transport
(funw : Pushout g f =>
(pushout_sym_map o pushout_sym_map) w = idmap w)
(pglue a) ((funb : C => 1) (g a)) =
(func : B => 1) (f a)
A, B, C: Type f: A -> B g: A -> C a: A
transport
(funw : Pushout g f =>
pushout_sym_map (pushout_sym_map w) = w) (pglue a)
1 = 1
abstract (rewrite transport_paths_FFlr, Pushout_rec_beta_pglue, ap_V, Pushout_rec_beta_pglue; hott_simpl).Defined.Definitionpushout_sym {ABC} {f : A -> B} {g : A -> C}
: Pushout f g <~> Pushout g f :=
equiv_adjointify pushout_sym_map pushout_sym_map sect_pushout_sym_map sect_pushout_sym_map.(** ** Functoriality *)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
Pushout f g -> Pushout f' g'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
Pushout f g -> Pushout f' g'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
A -> A'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
B + C -> B' + C'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
?k o (funx : A => inl (f x)) ==
(funx : A' => inl (f' x)) o ?h
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
?k o (funx : A => inr (g x)) ==
(funx : A' => inr (g' x)) o ?h
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
A -> A'
exact h.
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
B + C -> B' + C'
exact (functor_sum k l).
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
functor_sum k l o (funx : A => inl (f x)) ==
(funx : A' => inl (f' x)) o h
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
inl (k (f a)) = inl (f' (h a))
apply ap, p.
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h
functor_sum k l o (funx : A => inr (g x)) ==
(funx : A' => inr (g' x)) o h
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
inr (l (g a)) = inr (g' (h a))
apply ap, q.Defined.
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap (functor_pushout h k l p q) (pglue a) =
(ap pushl (p a) @ pglue (h a)) @ ap pushr (q a)^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap (functor_pushout h k l p q) (pglue a) =
(ap pushl (p a) @ pglue (h a)) @ ap pushr (q a)^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
(ap coeq (ap inl (p a)) @ cglue (h a)) @
ap coeq (ap inr (q a))^ =
(ap pushl (p a) @ pglue (h a)) @ ap pushr (q a)^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
(ap pushl (p a) @ pglue (h a)) @ ap pushr (q a)^ =
(ap coeq (ap inl (p a)) @ cglue (h a)) @
ap coeq (ap inr (q a))^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap pushl (p a) @ pglue (h a) =
ap coeq (ap inl (p a)) @ cglue (h a)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap pushr (q a)^ = ap coeq (ap inr (q a))^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap pushl (p a) @ pglue (h a) =
ap coeq (ap inl (p a)) @ cglue (h a)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap pushl (p a) = ap coeq (ap inl (p a))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap (funb : B' => push (inl b)) (p a) =
ap coeq (ap inl (p a))
napply ap_compose.
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap pushr (q a)^ = ap coeq (ap inr (q a))^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap (func : C' => push (inr c)) (q a)^ =
ap coeq (ap inr (q a))^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap push (ap inr (q a)^) = ap coeq (ap inr (q a))^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h: A -> A' k: B -> B' l: C -> C' p: k o f == f' o h q: l o g == g' o h a: A
ap inr (q a)^ = (ap inr (q a))^
napply ap_V.Defined.
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
functor_pushout h k l p q ==
functor_pushout h' k' l' p' q'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
functor_pushout h k l p q ==
functor_pushout h' k' l' p' q'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
h == h'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
functor_sum k l == functor_sum k' l'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
forallb : A,
?s ((funx : A => inl (f x)) b) @
(funa : A =>
ap inl (p' a)
:
functor_sum k' l' (inl (f a)) = inl (f' (h' a))) b =
(funa : A =>
ap inl (p a)
:
functor_sum k l (inl (f a)) = inl (f' (h a))) b @
ap (funx : A' => inl (f' x)) (?r b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
forallb : A,
?s ((funx : A => inr (g x)) b) @
(funa : A =>
ap inr (q' a)
:
functor_sum k' l' (inr (g a)) = inr (g' (h' a))) b =
(funa : A =>
ap inr (q a)
:
functor_sum k l (inr (g a)) = inr (g' (h a))) b @
ap (funx : A' => inr (g' x)) (?r b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
functor_sum k l == functor_sum k' l'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
forallb : A,
?s ((funx : A => inl (f x)) b) @
(funa : A =>
ap inl (p' a)
:
functor_sum k' l' (inl (f a)) = inl (f' (h' a))) b =
(funa : A =>
ap inl (p a)
:
functor_sum k l (inl (f a)) = inl (f' (h a))) b @
ap (funx : A' => inl (f' x)) (t b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
forallb : A,
?s ((funx : A => inr (g x)) b) @
(funa : A =>
ap inr (q' a)
:
functor_sum k' l' (inr (g a)) = inr (g' (h' a))) b =
(funa : A =>
ap inr (q a)
:
functor_sum k l (inr (g a)) = inr (g' (h a))) b @
ap (funx : A' => inr (g' x)) (t b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
forallb : A,
functor_sum_homotopic u v ((funx : A => inl (f x)) b) @
(funa : A =>
ap inl (p' a)
:
functor_sum k' l' (inl (f a)) = inl (f' (h' a))) b =
(funa : A =>
ap inl (p a)
:
functor_sum k l (inl (f a)) = inl (f' (h a))) b @
ap (funx : A' => inl (f' x)) (t b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a
forallb : A,
functor_sum_homotopic u v ((funx : A => inr (g x)) b) @
(funa : A =>
ap inr (q' a)
:
functor_sum k' l' (inr (g a)) = inr (g' (h' a))) b =
(funa : A =>
ap inr (q a)
:
functor_sum k l (inr (g a)) = inr (g' (h a))) b @
ap (funx : A' => inr (g' x)) (t b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a b: A
ap inl (u (f b)) @ ap inl (p' b) =
ap inl (p b) @ ap (funx : A' => inl (f' x)) (t b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a b: A
ap inr (v (g b)) @ ap inr (q' b) =
ap inr (q b) @ ap (funx : A' => inr (g' x)) (t b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a b: A
ap inl (u (f b)) @ ap inl (p' b) =
ap inl (p b @ ap f' (t b))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a b: A
ap inr (v (g b)) @ ap inr (q' b) =
ap inr (q b @ ap g' (t b))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a b: A
p b @ ap f' (t b) = u (f b) @ p' b
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a b: A
q b @ ap g' (t b) = v (g b) @ q' b
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' h, h': A -> A' k, k': B -> B' l, l': C -> C' p: k o f == f' o h q: l o g == g' o h p': k' o f == f' o h' q': l' o g == g' o h' t: h == h' u: k == k' v: l == l' i: foralla : A, p a @ ap f' (t a) = u (f a) @ p' a j: foralla : A, q a @ ap g' (t a) = v (g a) @ q' a b: A
q b @ ap g' (t b) = v (g b) @ q' b
exact (j b).Defined.
A, B, C: Type f: A -> B g: A -> C
functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1) == idmap
A, B, C: Type f: A -> B g: A -> C
functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1) == idmap
A, B, C: Type f: A -> B g: A -> C
forallb : B,
(funw : Pushout f g =>
functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1) w = idmap w) (pushl b)
A, B, C: Type f: A -> B g: A -> C
forallc : C,
(funw : Pushout f g =>
functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1) w = idmap w) (pushr c)
A, B, C: Type f: A -> B g: A -> C
foralla : A,
transport
(funw : Pushout f g =>
functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1) w = idmap w) (pglue a)
(?pushb (f a)) = ?pushc (g a)
A, B, C: Type f: A -> B g: A -> C
foralla : A,
transport
(funw : Pushout f g =>
functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1) w = idmap w) (pglue a)
((funb : B => 1) (f a)) = (func : C => 1) (g a)
A, B, C: Type f: A -> B g: A -> C
foralla : A,
transport
(funw : Pushout f g =>
functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1) w = w) (pglue a) 1 = 1
A, B, C: Type f: A -> B g: A -> C a: A
transport
(funw : Pushout f g =>
functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1) w = w) (pglue a) 1 = 1
A, B, C: Type f: A -> B g: A -> C a: A
ap
(functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1)) (pglue a) @ 1 = 1 @ pglue a
A, B, C: Type f: A -> B g: A -> C a: A
ap
(functor_pushout idmap idmap idmap (funx : A => 1)
(funx : A => 1)) (pglue a) = (1 @ pglue a) @ 1^
napply functor_pushout_beta_pglue.Defined.
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u'
functor_pushout (u' o u) (v' o v) (w' o w)
(funx : A => ap v' (p x) @ p' (u x))
(funx : A => ap w' (q x) @ q' (u x)) ==
functor_pushout u' v' w' p' q'
o functor_pushout u v w p q
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u'
functor_pushout (u' o u) (v' o v) (w' o w)
(funx : A => ap v' (p x) @ p' (u x))
(funx : A => ap w' (q x) @ q' (u x)) ==
functor_pushout u' v' w' p' q'
o functor_pushout u v w p q
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
functor_pushout (funx : A => u' (u x))
(funx : B => v' (v x)) (funx : C => w' (w x))
(funx : A => ap v' (p x) @ p' (u x))
(funx : A => ap w' (q x) @ q' (u x)) a =
functor_pushout u' v' w' p' q'
(functor_pushout u v w p q a)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
functor_pushout (funx : A => u' (u x))
(funx : B => v' (v x)) (funx : C => w' (w x))
(funx : A => ap v' (p x) @ p' (u x))
(funx : A => ap w' (q x) @ q' (u x)) a =
functor_coeq (funx : A => u' (u x))
(funx : B + C =>
functor_sum v' w' (functor_sum v w x))
(funb : A =>
ap (functor_sum v' w') (ap inl (p b)) @
ap inl (p' (u b)))
(funb : A =>
ap (functor_sum v' w') (ap inr (q b)) @
ap inr (q' (u b))) a
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
(funx : A => u' (u x)) == (funx : A => u' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
functor_sum (funx : B => v' (v x))
(funx : C => w' (w x)) ==
(funx : B + C =>
functor_sum v' w' (functor_sum v w x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
forallb : A,
?s ((funx : A => inl (f x)) b) @
(funb0 : A =>
ap (functor_sum v' w') (ap inl (p b0)) @
ap inl (p' (u b0))) b =
(funa : A =>
ap inl ((funx : A => ap v' (p x) @ p' (u x)) a)
:
functor_sum (funx : B => v' (v x))
(funx : C => w' (w x)) (inl (f a)) =
inl (f'' ((funx : A => u' (u x)) a))) b @
ap (funx : A'' => inl (f'' x)) (?r b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
forallb : A,
?s ((funx : A => inr (g x)) b) @
(funb0 : A =>
ap (functor_sum v' w') (ap inr (q b0)) @
ap inr (q' (u b0))) b =
(funa : A =>
ap inr ((funx : A => ap w' (q x) @ q' (u x)) a)
:
functor_sum (funx : B => v' (v x))
(funx : C => w' (w x)) (inr (g a)) =
inr (g'' ((funx : A => u' (u x)) a))) b @
ap (funx : A'' => inr (g'' x)) (?r b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
functor_sum (funx : B => v' (v x))
(funx : C => w' (w x)) ==
(funx : B + C =>
functor_sum v' w' (functor_sum v w x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
forallb : A,
?s ((funx : A => inl (f x)) b) @
(funb0 : A =>
ap (functor_sum v' w') (ap inl (p b0)) @
ap inl (p' (u b0))) b =
(funa : A =>
ap inl ((funx : A => ap v' (p x) @ p' (u x)) a)
:
functor_sum (funx : B => v' (v x))
(funx : C => w' (w x)) (inl (f a)) =
inl (f'' ((funx : A => u' (u x)) a))) b @
ap (funx : A'' => inl (f'' x)) ((funx0 : A => 1) b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
forallb : A,
?s ((funx : A => inr (g x)) b) @
(funb0 : A =>
ap (functor_sum v' w') (ap inr (q b0)) @
ap inr (q' (u b0))) b =
(funa : A =>
ap inr ((funx : A => ap w' (q x) @ q' (u x)) a)
:
functor_sum (funx : B => v' (v x))
(funx : C => w' (w x)) (inr (g a)) =
inr (g'' ((funx : A => u' (u x)) a))) b @
ap (funx : A'' => inr (g'' x)) ((funx0 : A => 1) b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
forallb : A,
functor_sum_compose ((funx : A => inl (f x)) b) @
(funb0 : A =>
ap (functor_sum v' w') (ap inl (p b0)) @
ap inl (p' (u b0))) b =
(funa : A =>
ap inl ((funx : A => ap v' (p x) @ p' (u x)) a)
:
functor_sum (funx : B => v' (v x))
(funx : C => w' (w x)) (inl (f a)) =
inl (f'' ((funx : A => u' (u x)) a))) b @
ap (funx : A'' => inl (f'' x)) ((funx0 : A => 1) b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g
forallb : A,
functor_sum_compose ((funx : A => inr (g x)) b) @
(funb0 : A =>
ap (functor_sum v' w') (ap inr (q b0)) @
ap inr (q' (u b0))) b =
(funa : A =>
ap inr ((funx : A => ap w' (q x) @ q' (u x)) a)
:
functor_sum (funx : B => v' (v x))
(funx : C => w' (w x)) (inr (g a)) =
inr (g'' ((funx : A => u' (u x)) a))) b @
ap (funx : A'' => inr (g'' x)) ((funx0 : A => 1) b)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
1 @
(ap (functor_sum v' w') (ap inl (p x)) @
ap inl (p' (u x))) =
ap inl (ap v' (p x) @ p' (u x)) @ 1
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
1 @
(ap (functor_sum v' w') (ap inr (q x)) @
ap inr (q' (u x))) =
ap inr (ap w' (q x) @ q' (u x)) @ 1
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap (functor_sum v' w') (ap inl (p x)) @
ap inl (p' (u x)) = ap inl (ap v' (p x) @ p' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap (functor_sum v' w') (ap inr (q x)) @
ap inr (q' (u x)) = ap inr (ap w' (q x) @ q' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
?Goal = ap (functor_sum v' w') (ap inl (p x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
?Goal @ ap inl (p' (u x)) =
ap inl (ap v' (p x) @ p' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
?Goal2 = ap (functor_sum v' w') (ap inr (q x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
?Goal2 @ ap inr (q' (u x)) =
ap inr (ap w' (q x) @ q' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap (functor_sum v' w' o inl) (p x) @ ap inl (p' (u x)) =
ap inl (ap v' (p x) @ p' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap (functor_sum v' w' o inr) (q x) @ ap inr (q' (u x)) =
ap inr (ap w' (q x) @ q' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap (funx : B' => inl (v' x)) (p x) @
ap inl (p' (u x)) = ap inl (ap v' (p x) @ p' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap (funx : C' => inr (w' x)) (q x) @
ap inr (q' (u x)) = ap inr (ap w' (q x) @ q' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap (funx : B' => inl (v' x)) (p x) = ?Goal
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
?Goal @ ap inl (p' (u x)) =
ap inl (ap v' (p x) @ p' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap (funx : C' => inr (w' x)) (q x) = ?Goal2
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
?Goal2 @ ap inr (q' (u x)) =
ap inr (ap w' (q x) @ q' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap inl (ap v' (p x)) @ ap inl (p' (u x)) =
ap inl (ap v' (p x) @ p' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap inr (ap w' (q x)) @ ap inr (q' (u x)) =
ap inr (ap w' (q x) @ q' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap inl (ap v' (p x) @ p' (u x)) =
ap inl (ap v' (p x)) @ ap inl (p' (u x))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' A'', B'', C'': Type f'': A'' -> B'' g'': A'' -> C'' u: A -> A' v: B -> B' w: C -> C' u': A' -> A'' v': B' -> B'' w': C' -> C'' p: v o f == f' o u q: w o g == g' o u p': v' o f' == f'' o u' q': w' o g' == g'' o u' a: Pushout f g x: A
ap inr (ap w' (q x) @ q' (u x)) =
ap inr (ap w' (q x)) @ ap inr (q' (u x))
1,2: apply ap_pp.Defined.(** ** Equivalences *)(** Pushouts preserve equivalences. *)SectionEquivPushout.Context {ABCfgA'B'C'f'g'}
(eA : A <~> A') (eB : B <~> B') (eC : C <~> C')
(p : eB o f == f' o eA) (q : eC o g == g' o eA).
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA
Pushout f g <~> Pushout f' g'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA
Pushout f g <~> Pushout f' g'
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA
(funx : A => (eB +E eC) (inl (f x))) ==
(funx : A => inl (f' (eA x)))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA
(funx : A => (eB +E eC) (inr (g x))) ==
(funx : A => inr (g' (eA x)))
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA x: A
eB (f x) = f' (eA x)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA x: A
eC (g x) = g' (eA x)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA x: A
eB (f x) = f' (eA x)
apply p.
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA x: A
eC (g x) = g' (eA x)
apply q.Defined.
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA a: A
ap equiv_pushout (pglue a) =
(ap pushl (p a) @ pglue (eA a)) @ ap pushr (q a)^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA a: A
ap equiv_pushout (pglue a) =
(ap pushl (p a) @ pglue (eA a)) @ ap pushr (q a)^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA a: A
(ap coeq (ap inl (p a)) @ cglue (eA a)) @
ap coeq (ap inr (q a))^ =
(ap pushl (p a) @ pglue (eA a)) @ ap pushr (q a)^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA a: A
ap coeq (ap inl (p a)) = ap pushl (p a)
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA a: A
ap coeq (ap inr (q a))^ = ap pushr (q a)^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA a: A
ap coeq (ap inl (p a)) = ap pushl (p a)
symmetry; exact (ap_compose inl coeq _).
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA a: A
ap coeq (ap inr (q a))^ = ap pushr (q a)^
A, B, C: Type f: A -> B g: A -> C A', B', C': Type f': A' -> B' g': A' -> C' eA: A <~> A' eB: B <~> B' eC: C <~> C' p: eB o f == f' o eA q: eC o g == g' o eA a: A
ap coeq (ap inr (q a)^) = ap pushr (q a)^
symmetry; exact (ap_compose inr coeq _).Defined.EndEquivPushout.(** ** Contractibility *)(** The pushout of a span of contractible types is contractible *)
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
Contr (Pushout f g)
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
Contr (Pushout f g)
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
forally : Pushout f g, pushl (center B) = y
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
forallb : B, pushl (center B) = pushl b
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
forallc : C, pushl (center B) = pushr c
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
foralla : A,
transport (paths (pushl (center B)))
(pglue a) (?pushb (f a)) =
?pushc (g a)
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
forallb : B, pushl (center B) = pushl b
intros b; apply ap, path_contr.
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
forallc : C, pushl (center B) = pushr c
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C c: C
pushl (center B) = pushr c
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C c: C
pushl (center B) = pushl (f (center A))
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C c: C
pushr (g (center A)) = pushr c
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C c: C
pushl (center B) = pushl (f (center A))
apply ap, path_contr.
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C c: C
pushr (g (center A)) = pushr c
apply ap, path_contr.
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
foralla : A,
transport (paths (pushl (center B))) (pglue a)
((funb : B => ap pushl (path_contr (center B) b))
(f a)) =
(func : C =>
(ap pushl (path_contr (center B) (f (center A))) @
pglue (center A)) @
ap pushr (path_contr (g (center A)) c)) (g a)
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C a: A
transport (paths (pushl (center B))) (pglue a)
((funb : B => ap pushl (path_contr (center B) b))
(f a)) =
(func : C =>
(ap pushl (path_contr (center B) (f (center A))) @
pglue (center A)) @
ap pushr (path_contr (g (center A)) c)) (g a)
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C a: A
ap pushl (path_contr (center B) (f a)) @ pglue a =
(ap pushl (path_contr (center B) (f (center A))) @
pglue (center A)) @
ap pushr (path_contr (g (center A)) (g a))
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C a: A p: center A = a
ap pushl (path_contr (center B) (f a)) @ pglue a =
(ap pushl (path_contr (center B) (f (center A))) @
pglue (center A)) @
ap pushr (path_contr (g (center A)) (g a))
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
ap pushl (path_contr (center B) (f (center A))) @
pglue (center A) =
(ap pushl (path_contr (center B) (f (center A))) @
pglue (center A)) @
ap pushr (path_contr (g (center A)) (g (center A)))
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
(ap pushl (path_contr (center B) (f (center A))) @
pglue (center A)) @ 1 =
(ap pushl (path_contr (center B) (f (center A))) @
pglue (center A)) @
ap pushr (path_contr (g (center A)) (g (center A)))
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
ap pushr 1 =
ap pushr (path_contr (g (center A)) (g (center A)))
A, B, C: Type Contr0: Contr A Contr1: Contr B Contr2: Contr C f: A -> B g: A -> C
1 = path_contr (g (center A)) (g (center A))
apply path_contr.Defined.(** ** Sigmas *)(** Pushouts commute with sigmas *)SectionEquivSigmaPushout.Context {X : Type}
(A : X -> Type) (B : X -> Type) (C : X -> Type)
(f : forallx, A x -> B x) (g : forallx, A x -> C x).
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x
foralla : {x : _ & A x},
functor_sigma idmap (funx : X => pushl)
(functor_sigma idmap f a) =
functor_sigma idmap (funx : X => pushr)
(functor_sigma idmap g a)
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
(x; pushl (f x a)) = (x; pushr (g x a))
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
pushl (f x a) = pushr (g x a)
apply pglue.Defined.
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
ap esp2 (pglue (x; a)) =
path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a)
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
ap esp2 (pglue (x; a)) =
path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a)
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
ap
(Pushout_rec {x : X & Pushout (f x) (g x)}
(functor_sigma idmap (funx : X => pushl))
(functor_sigma idmap (funx : X => pushr))
(funa0 : {x : _ & A x} =>
path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a0.2))) (pglue (x; a)) =
path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a)
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a) =
path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a)
reflexivity.Qed.
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
ap (exist (funx : X => Pushout (f x) (g x)) x)
(pglue a) =
ap
(funx0 : Pushout (f x) (g x) => esp2 (esp1 (x; x0)))
(pglue a)
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
ap (exist (funx : X => Pushout (f x) (g x)) x)
(pglue a) =
ap
(funx : {x : X & Pushout (f x) (g x)} =>
esp2 (esp1 x))
(ap (exist (funx : X => Pushout (f x) (g x)) x)
(pglue a))
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
ap (exist (funx : X => Pushout (f x) (g x)) x)
(pglue a) =
ap esp2
(ap esp1
(ap (exist (funx : X => Pushout (f x) (g x)) x)
(pglue a)))
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a) =
ap esp2
(ap esp1
(path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a)))
X: Type A, B, C: X -> Type f: forallx : X, A x -> B x g: forallx : X, A x -> C x x: X a: A x
path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a) =
path_sigma' (funx : X => Pushout (f x) (g x)) 1
(pglue a)
reflexivity.Defined.EndEquivSigmaPushout.(** ** Pushouts are associative *)SectionPushoutAssoc.Context {A1A2BCD : Type}
(f1 : A1 -> B) (g1 : A1 -> C) (f2 : A2 -> C) (g2 : A2 -> D).Definitionpushout_assoc_left := Pushout (pushr' f1 g1 o f2) g2.Letpushll : B -> pushout_assoc_left
:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1.Letpushlm : C -> pushout_assoc_left
:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1.Letpushlr : D -> pushout_assoc_left
:= pushr' (pushr' f1 g1 o f2) g2.Letpgluell : foralla1, pushll (f1 a1) = pushlm (g1 a1)
:= funa1 => ap (pushl' (pushr' f1 g1 o f2) g2) (pglue' f1 g1 a1).Letpgluelr : foralla2, pushlm (f2 a2) = pushlr (g2 a2)
:= funa2 => pglue' (pushr' f1 g1 o f2) g2 a2.
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: pushout_assoc_left -> Type pushb: forallb : B, P (pushll b) pushc: forallc : C, P (pushlm c) pushd: foralld : D, P (pushlr d) pusha1: foralla1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forallx : pushout_assoc_left, P x
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: pushout_assoc_left -> Type pushb: forallb : B, P (pushll b) pushc: forallc : C, P (pushlm c) pushd: foralld : D, P (pushlr d) pusha1: foralla1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forallx : pushout_assoc_left, P x
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: pushout_assoc_left -> Type pushb: forallb : B, P (pushll b) pushc: forallc : C, P (pushlm c) pushd: foralld : D, P (pushlr d) pusha1: foralla1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forallb : Pushout f1 g1, P (pushl b)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: pushout_assoc_left -> Type pushb: forallb : B, P (pushll b) pushc: forallc : C, P (pushlm c) pushd: foralld : D, P (pushlr d) pusha1: foralla1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
foralla : A2,
transport P (pglue a)
(?pushb ((funx : A2 => pushr' f1 g1 (f2 x)) a)) =
pushd (g2 a)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: pushout_assoc_left -> Type pushb: forallb : B, P (pushll b) pushc: forallc : C, P (pushlm c) pushd: foralld : D, P (pushlr d) pusha1: foralla1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forallb : Pushout f1 g1, P (pushl b)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: pushout_assoc_left -> Type pushb: forallb : B, P (pushll b) pushc: forallc : C, P (pushlm c) pushd: foralld : D, P (pushlr d) pusha1: foralla1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
foralla : A1,
transport (funw : Pushout f1 g1 => P (pushl w))
(pglue a) (pushb (f1 a)) = pushc (g1 a)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: pushout_assoc_left -> Type pushb: forallb : B, P (pushll b) pushc: forallc : C, P (pushlm c) pushd: foralld : D, P (pushlr d) pusha1: foralla1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2) a1: A1
transport (funw : Pushout f1 g1 => P (pushl w))
(pglue a1) (pushb (f1 a1)) = pushc (g1 a1)
exact (transport_compose P pushl _ _ @ pusha1 a1).
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: pushout_assoc_left -> Type pushb: forallb : B, P (pushll b) pushc: forallc : C, P (pushlm c) pushd: foralld : D, P (pushlr d) pusha1: foralla1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
foralla : A2,
transport P (pglue a)
(Pushout_ind (funw : Pushout f1 g1 => P (pushl w))
pushb pushc
(funa1 : A1 =>
transport_compose P pushl (pglue' f1 g1 a1)
(pushb (f1 a1)) @ pusha1 a1)
((funx : A2 => pushr' f1 g1 (f2 x)) a)) =
pushd (g2 a)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2)
pushout_assoc_left -> P
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2)
pushout_assoc_left -> P
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2)
Pushout f1 g1 -> P
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2)
foralla : A2,
?pushb ((funx : A2 => pushr' f1 g1 (f2 x)) a) =
pushd (g2 a)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2)
Pushout f1 g1 -> P
exact (Pushout_rec _ pushb pushc pusha1).
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2)
foralla : A2,
Pushout_rec P pushb pushc pusha1
((funx : A2 => pushr' f1 g1 (f2 x)) a) =
pushd (g2 a)
exact pusha2.Defined.
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2) a1: A1
ap pushout_assoc_left_rec (pgluell a1) = pusha1 a1
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2) a1: A1
ap pushout_assoc_left_rec (pgluell a1) = pusha1 a1
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2) a1: A1
ap pushout_assoc_left_rec
(ap (pushl' (funx : A2 => pushr' f1 g1 (f2 x)) g2)
(pglue' f1 g1 a1)) = pusha1 a1
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2) a1: A1
ap
(funx : Pushout f1 g1 =>
pushout_assoc_left_rec
(pushl' (funx0 : A2 => pushr' f1 g1 (f2 x0)) g2
x)) (pglue' f1 g1 a1) = pusha1 a1
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2) a1: A1
ap (Pushout_rec P pushb pushc pusha1)
(pglue' f1 g1 a1) = pusha1 a1
apply Pushout_rec_beta_pglue.Defined.
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2) a2: A2
ap pushout_assoc_left_rec (pgluelr a2) = pusha2 a2
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2) a2: A2
ap pushout_assoc_left_rec (pgluelr a2) = pusha2 a2
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) P: Type pushb: B -> P pushc: C -> P pushd: D -> P pusha1: foralla1 : A1, pushb (f1 a1) = pushc (g1 a1) pusha2: foralla2 : A2, pushc (f2 a2) = pushd (g2 a2) a2: A2
ap
(Pushout_rec P (Pushout_rec P pushb pushc pusha1)
pushd pusha2)
(pglue' (funx : A2 => pushr' f1 g1 (f2 x)) g2 a2) =
pusha2 a2
apply (Pushout_rec_beta_pglue (f := pushr' f1 g1 o f2) (g := g2)).Defined.EndPushout_Assoc_Left_Rec.Definitionpushout_assoc_right := Pushout f1 (pushl' f2 g2 o g1).Letpushrl : B -> pushout_assoc_right
:= pushl' f1 (pushl' f2 g2 o g1).Letpushrm : C -> pushout_assoc_right
:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2.Letpushrr : D -> pushout_assoc_right
:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2.Letpgluerl : foralla1, pushrl (f1 a1) = pushrm (g1 a1)
:= funa1 => pglue' f1 (pushl' f2 g2 o g1) a1.Letpgluerr : foralla2, pushrm (f2 a2) = pushrr (g2 a2)
:= funa2 => ap (pushr' f1 (pushl' f2 g2 o g1)) (pglue' f2 g2 a2).
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right pgluerl:= funa1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: foralla1 : A1,
pushrl (f1 a1) = pushrm (g1 a1) pgluerr:= funa2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
(pglue' f2 g2 a2): foralla2 : A2,
pushrm (f2 a2) = pushrr (g2 a2) P: pushout_assoc_right -> Type pushb: forallb : B, P (pushrl b) pushc: forallc : C, P (pushrm c) pushd: foralld : D, P (pushrr d) pusha1: foralla1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forallx : pushout_assoc_right, P x
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right pgluerl:= funa1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: foralla1 : A1,
pushrl (f1 a1) = pushrm (g1 a1) pgluerr:= funa2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
(pglue' f2 g2 a2): foralla2 : A2,
pushrm (f2 a2) = pushrr (g2 a2) P: pushout_assoc_right -> Type pushb: forallb : B, P (pushrl b) pushc: forallc : C, P (pushrm c) pushd: foralld : D, P (pushrr d) pusha1: foralla1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forallx : pushout_assoc_right, P x
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right pgluerl:= funa1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: foralla1 : A1,
pushrl (f1 a1) = pushrm (g1 a1) pgluerr:= funa2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
(pglue' f2 g2 a2): foralla2 : A2,
pushrm (f2 a2) = pushrr (g2 a2) P: pushout_assoc_right -> Type pushb: forallb : B, P (pushrl b) pushc: forallc : C, P (pushrm c) pushd: foralld : D, P (pushrr d) pusha1: foralla1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forallc : Pushout f2 g2, P (pushr c)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right pgluerl:= funa1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: foralla1 : A1,
pushrl (f1 a1) = pushrm (g1 a1) pgluerr:= funa2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
(pglue' f2 g2 a2): foralla2 : A2,
pushrm (f2 a2) = pushrr (g2 a2) P: pushout_assoc_right -> Type pushb: forallb : B, P (pushrl b) pushc: forallc : C, P (pushrm c) pushd: foralld : D, P (pushrr d) pusha1: foralla1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
foralla : A1,
transport P (pglue a) (pushb (f1 a)) =
?pushc ((funx : A1 => pushl' f2 g2 (g1 x)) a)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right pgluerl:= funa1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: foralla1 : A1,
pushrl (f1 a1) = pushrm (g1 a1) pgluerr:= funa2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
(pglue' f2 g2 a2): foralla2 : A2,
pushrm (f2 a2) = pushrr (g2 a2) P: pushout_assoc_right -> Type pushb: forallb : B, P (pushrl b) pushc: forallc : C, P (pushrm c) pushd: foralld : D, P (pushrr d) pusha1: foralla1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forallc : Pushout f2 g2, P (pushr c)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right pgluerl:= funa1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: foralla1 : A1,
pushrl (f1 a1) = pushrm (g1 a1) pgluerr:= funa2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
(pglue' f2 g2 a2): foralla2 : A2,
pushrm (f2 a2) = pushrr (g2 a2) P: pushout_assoc_right -> Type pushb: forallb : B, P (pushrl b) pushc: forallc : C, P (pushrm c) pushd: foralld : D, P (pushrr d) pusha1: foralla1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
foralla : A2,
transport (funw : Pushout f2 g2 => P (pushr w))
(pglue a) (pushc (f2 a)) = pushd (g2 a)
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right pgluerl:= funa1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: foralla1 : A1,
pushrl (f1 a1) = pushrm (g1 a1) pgluerr:= funa2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
(pglue' f2 g2 a2): foralla2 : A2,
pushrm (f2 a2) = pushrr (g2 a2) P: pushout_assoc_right -> Type pushb: forallb : B, P (pushrl b) pushc: forallc : C, P (pushrm c) pushd: foralld : D, P (pushrr d) pusha1: foralla1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2) a2: A2
transport (funw : Pushout f2 g2 => P (pushr w))
(pglue a2) (pushc (f2 a2)) = pushd (g2 a2)
exact (transport_compose P pushr _ _ @ pusha2 a2).
A1, A2, B, C, D: Type f1: A1 -> B g1: A1 -> C f2: A2 -> C g2: A2 -> D pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left pgluell:= funa1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
(pglue' f1 g1 a1): foralla1 : A1,
pushll (f1 a1) = pushlm (g1 a1) pgluelr:= funa2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: foralla2 : A2,
pushlm (f2 a2) = pushlr (g2 a2) pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right pgluerl:= funa1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: foralla1 : A1,
pushrl (f1 a1) = pushrm (g1 a1) pgluerr:= funa2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
(pglue' f2 g2 a2): foralla2 : A2,
pushrm (f2 a2) = pushrr (g2 a2) P: pushout_assoc_right -> Type pushb: forallb : B, P (pushrl b) pushc: forallc : C, P (pushrm c) pushd: foralld : D, P (pushrr d) pusha1: foralla1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1) pusha2: foralla2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
foralla : A1,
transport P (pglue a) (pushb (f1 a)) =
Pushout_ind (funw : Pushout f2 g2 => P (pushr w))
pushc pushd
(funa2 : A2 =>
transport_compose P pushr (pglue' f2 g2 a2)
(pushc (f2 a2)) @ pusha2 a2)
((funx : A1 => pushl' f2 g2 (g1 x)) a)
pushr' f g
o Pushout_rec C (g o f^-1) idmap
(funa : A =>
ap g (eissect f a)
:
(g o f^-1) (f a) = idmap (g a)) == idmap
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f
forallb : B,
pushr' f g
(Pushout_rec C (funx : B => g (f^-1 x)) idmap
(funa : A => ap g (eissect f a)) (pushl b)) =
pushl b
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f
forallc : C,
pushr' f g
(Pushout_rec C (funx : B => g (f^-1 x)) idmap
(funa : A => ap g (eissect f a)) (pushr c)) =
pushr c
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f
foralla : A,
transport
(funw : Pushout f g =>
pushr' f g
(Pushout_rec C (funx : B => g (f^-1 x)) idmap
(funa0 : A => ap g (eissect f a0)) w) = w)
(pglue a) (?Goal (f a)) = ?Goal0 (g a)
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f
forallb : B,
pushr' f g
(Pushout_rec C (funx : B => g (f^-1 x)) idmap
(funa : A => ap g (eissect f a)) (pushl b)) =
pushl b
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f b: B
pushr' f g (g (f^-1 b)) = pushl b
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f b: B
pushr' f g (g (f^-1 b)) = pushl' f g (f (f^-1 b))
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f b: B
pushl' f g (f (f^-1 b)) = pushl b
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f b: B
pushr' f g (g (f^-1 b)) = pushl' f g (f (f^-1 b))
symmetry; apply pglue.
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f b: B
pushl' f g (f (f^-1 b)) = pushl b
apply ap, eisretr.
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f
forallc : C,
pushr' f g
(Pushout_rec C (funx : B => g (f^-1 x)) idmap
(funa : A => ap g (eissect f a)) (pushr c)) =
pushr c
intros c; reflexivity.
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f
foralla : A,
transport
(funw : Pushout f g =>
pushr' f g
(Pushout_rec C (funx : B => g (f^-1 x)) idmap
(funa0 : A => ap g (eissect f a0)) w) = w)
(pglue a)
((funb : B =>
(pglue (f^-1 b))^ @ ap pushl (eisretr f b)) (f a)) =
(func : C => 1) (g a)
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f a: A
transport
(funw : Pushout f g =>
pushr' f g
(Pushout_rec C (funx : B => g (f^-1 x)) idmap
(funa : A => ap g (eissect f a)) w) = w)
(pglue a)
((funb : B =>
(pglue (f^-1 b))^ @ ap pushl (eisretr f b)) (f a)) =
(func : C => 1) (g a)
abstract (
rewrite transport_paths_FlFr, ap_compose, !concat_pp_p;
apply moveR_Vp; apply moveR_Vp;
rewrite Pushout_rec_beta_pglue, eisadj, ap_idmap, concat_p1;
rewrite <- ap_compose, <- (ap_compose g (pushr' f g));
exact (concat_Ap (pglue' f g) (eissect f a)) ).
A, B, C: Type f: A -> B g: A -> C H: IsEquiv f
Pushout_rec C (g o f^-1) idmap
(funa : A =>
ap g (eissect f a) : (g o f^-1) (f a) = idmap (g a))
o pushr' f g == idmap
intros c; reflexivity.Defined.
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
IsEquiv (pushl' f g)
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
IsEquiv (pushl' f g)
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
Pushout f g -> B
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
pushl' f g o ?g == idmap
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
?g o pushl' f g == idmap
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
Pushout f g -> B
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
foralla : A, idmap (f a) = (f o g^-1) (g a)
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g a: A
f a = f (g^-1 (g a))
symmetry; apply ap, eissect.
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
pushl' f g
o Pushout_rec B idmap (f o g^-1)
(funa : A =>
(ap f (eissect g a))^
:
idmap (f a) = (f o g^-1) (g a)) == idmap
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
forallb : B,
pushl' f g
(Pushout_rec B idmap (funx : C => f (g^-1 x))
(funa : A => (ap f (eissect g a))^) (pushl b)) =
pushl b
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
forallc : C,
pushl' f g
(Pushout_rec B idmap (funx : C => f (g^-1 x))
(funa : A => (ap f (eissect g a))^) (pushr c)) =
pushr c
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
foralla : A,
transport
(funw : Pushout f g =>
pushl' f g
(Pushout_rec B idmap (funx : C => f (g^-1 x))
(funa0 : A => (ap f (eissect g a0))^) w) = w)
(pglue a) (?Goal (f a)) = ?Goal0 (g a)
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
forallb : B,
pushl' f g
(Pushout_rec B idmap (funx : C => f (g^-1 x))
(funa : A => (ap f (eissect g a))^) (pushl b)) =
pushl b
intros b; reflexivity.
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
forallc : C,
pushl' f g
(Pushout_rec B idmap (funx : C => f (g^-1 x))
(funa : A => (ap f (eissect g a))^) (pushr c)) =
pushr c
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g c: C
pushl' f g (f (g^-1 c)) = pushr c
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g c: C
pushl' f g (f (g^-1 c)) = pushr' f g (g (g^-1 c))
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g c: C
pushr' f g (g (g^-1 c)) = pushr c
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g c: C
pushl' f g (f (g^-1 c)) = pushr' f g (g (g^-1 c))
apply pglue.
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g c: C
pushr' f g (g (g^-1 c)) = pushr c
apply ap, eisretr.
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g
foralla : A,
transport
(funw : Pushout f g =>
pushl' f g
(Pushout_rec B idmap (funx : C => f (g^-1 x))
(funa0 : A => (ap f (eissect g a0))^) w) = w)
(pglue a) ((funb : B => 1) (f a)) =
(func : C => pglue (g^-1 c) @ ap pushr (eisretr g c))
(g a)
A, B, C: Type f: A -> B g: A -> C H: IsEquiv g a: A
transport
(funw : Pushout f g =>
pushl' f g
(Pushout_rec B idmap (funx : C => f (g^-1 x))
(funa : A => (ap f (eissect g a))^) w) = w)
(pglue a) ((funb : B => 1) (f a)) =
(func : C => pglue (g^-1 c) @ ap pushr (eisretr g c))
(g a)
Pushout_rec B idmap (f o g^-1)
(funa : A =>
(ap f (eissect g a))^
:
idmap (f a) = (f o g^-1) (g a)) o pushl' f g ==
idmap
intros c; reflexivity.Defined.(** ** Descent *)(** We study "equifibrant" type families over a span [f : A -> B] and [g : A -> C]. By univalence, the descent property tells us that these type families correspond to type families over the pushout, and we obtain an induction principle for such type families. Dependent descent data over some particular descent data are "equifibrant" type families over this descent data. The "equifibrancy" is only taken over the span [f : A -> B] and [g : A -> C], but there is an extra level of dependency coming from the descent data. In this case, we obtain an induction and recursion principle, but only with a computation rule for the recursion principle.The theory of descent is interesting to consider in itself. However, we will use it as a means to structure the code, and to obtain induction and recursion principles that are valuable in proving the flattening lemma, and characterizing path spaces. Thus we will gloss over the bigger picture, and not consider equivalences of descent data, nor homotopies of their sections. We will also not elaborate on uniqueness of the induced families.It's possible to prove the results in the Descent, Flattening and Paths Sections without univalence, by replacing all equivalences with paths, but in practice these results will be used with equivalences as input, making the form below more convenient. See https://github.com/HoTT/Coq-HoTT/pull/2147#issuecomment-2521570830 for further information. *)SectionDescent.Context `{Univalence}.(** Descent data over [f : A -> B] and [g : A -> C] are "equifibrant" or "cartesian" type families [pod_faml : B -> Type] and [pod_famr : C -> Type]. This means that if [a : A], then the fibers [pod_faml (f a)] and [pod_famr (g a)] are equivalent, witnessed by [pod_e]. *)RecordpoDescent {ABC : Type} {f : A -> B} {g : A -> C} := {
pod_faml (b : B) : Type;
pod_famr (c : C) : Type;
pod_e (a : A) : pod_faml (f a) <~> pod_famr (g a)
}.GlobalArguments poDescent {A B C} f g.(** Let [A], [B], and [C] be types, with a morphisms [f : A -> B] and [g : A -> C]. *)Context {ABC : Type} {f : A -> B} {g : A -> C}.(** Descent data induces a type family over [Pushout f g]. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
Pushout f g -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
Pushout f g -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
foralla : A, pod_faml Pe (f a) = pod_famr Pe (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A
pod_faml Pe (f a) = pod_famr Pe (g a)
exact (path_universe_uncurried (pod_e Pe a)).Defined.(** A type family over [Pushout f g] induces descent data. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C P: Pushout f g -> Type
poDescent f g
H: Univalence A, B, C: Type f: A -> B g: A -> C P: Pushout f g -> Type
poDescent f g
H: Univalence A, B, C: Type f: A -> B g: A -> C P: Pushout f g -> Type
B -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C P: Pushout f g -> Type
C -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C P: Pushout f g -> Type
foralla : A, ?pod_faml (f a) <~> ?pod_famr (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C P: Pushout f g -> Type
B -> Type
exact (P o pushl).
H: Univalence A, B, C: Type f: A -> B g: A -> C P: Pushout f g -> Type
C -> Type
exact (P o pushr).
H: Univalence A, B, C: Type f: A -> B g: A -> C P: Pushout f g -> Type
foralla : A, (P o pushl) (f a) <~> (P o pushr) (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C P: Pushout f g -> Type a: A
(P o pushl) (f a) <~> (P o pushr) (g a)
exact (equiv_transport P (pglue a)).Defined.(** Transporting over [fam_podescent] along [pglue a] is given by [pod_e]. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
transport (fam_podescent Pe) (pglue a) pf =
pod_e Pe a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
transport (fam_podescent Pe) (pglue a) pf =
pod_e Pe a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
ap (fam_podescent Pe) (pglue a) =
path_universe (pod_e Pe a)
napply Pushout_rec_beta_pglue.Defined.(** A section on the descent data are fiberwise sections that respects the equivalences. *)RecordpoDescentSection {Pe : poDescent f g} := {
pods_sectl (b : B) : pod_faml Pe b;
pods_sectr (c : C) : pod_famr Pe c;
pods_e (a : A)
: pod_e Pe a (pods_sectl (f a)) = pods_sectr (g a)
}.GlobalArguments poDescentSection Pe : clear implicits.(** A descent section induces a genuine section of [fam_cdescent Pe]. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g s: poDescentSection Pe
forallx : Pushout f g, fam_podescent Pe x
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g s: poDescentSection Pe
forallx : Pushout f g, fam_podescent Pe x
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g s: poDescentSection Pe
foralla : A,
transport (fam_podescent Pe) (pglue a)
(pods_sectl s (f a)) = pods_sectr s (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g s: poDescentSection Pe a: A
transport (fam_podescent Pe) (pglue a)
(pods_sectl s (f a)) = pods_sectr s (g a)
exact (transport_fam_podescent_pglue Pe a _ @ pods_e s a).Defined.(** We record its computation rule *)Definitionpodescent_ind_beta_pglue {Pe : poDescent f g}
(s : poDescentSection Pe) (a : A)
: apD (podescent_ind s) (pglue a) = transport_fam_podescent_pglue Pe a _ @ pods_e s a
:= Pushout_ind_beta_pglue _ (pods_sectl s) (pods_sectr s) _ _.(** Dependent descent data over descent data [Pe : poDescent f g] consists of a type families [podd_faml : forall (b : B), pod_faml Pe b -> Type] and [podd_famr : forall (c : C), pod_famr Pe c -> Type] together with coherences [podd_e a pf]. *)RecordpoDepDescent {Pe : poDescent f g} := {
podd_faml (b : B) (pb : pod_faml Pe b) : Type;
podd_famr (c : C) (pc : pod_famr Pe c) : Type;
podd_e (a : A) (pf : pod_faml Pe (f a))
: podd_faml (f a) pf <~> podd_famr (g a) (pod_e Pe a pf)
}.GlobalArguments poDepDescent Pe : clear implicits.(** A dependent type family over [fam_podescent Pe] induces dependent descent data over [Pe]. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type
poDepDescent Pe
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type
poDepDescent Pe
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type
forallb : B, pod_faml Pe b -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type
forallc : C, pod_famr Pe c -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type
forall (a : A) (pf : pod_faml Pe (f a)),
?podd_faml (f a) pf <~>
?podd_famr (g a) (pod_e Pe a pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type
forallb : B, pod_faml Pe b -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type b: B
pod_faml Pe b -> Type
exact (Q (pushl b)).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type
forallc : C, pod_famr Pe c -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type c: C
pod_famr Pe c -> Type
exact (Q (pushr c)).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type
forall (a : A) (pf : pod_faml Pe (f a)),
(funb : B => Q (pushl b) : pod_faml Pe b -> Type)
(f a) pf <~>
(func : C => Q (pushr c) : pod_famr Pe c -> Type)
(g a) (pod_e Pe a pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type a: A pf: pod_faml Pe (f a)
(funb : B => Q (pushl b) : pod_faml Pe b -> Type)
(f a) pf <~>
(func : C => Q (pushr c) : pod_famr Pe c -> Type)
(g a) (pod_e Pe a pf)
exact (equiv_transportDD (fam_podescent Pe) Q
(pglue a) (transport_fam_podescent_pglue Pe a pf)).Defined.(** Dependent descent data over [Pe] induces a dependent type family over [fam_podescent Pe]. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe
forallx : Pushout f g, fam_podescent Pe x -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe
forallx : Pushout f g, fam_podescent Pe x -> Type
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe
forallb : B,
(funw : Pushout f g => fam_podescent Pe w -> Type)
(pushl b)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe
forallc : C,
(funw : Pushout f g => fam_podescent Pe w -> Type)
(pushr c)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe
foralla : A,
transport
(funw : Pushout f g => fam_podescent Pe w -> Type)
(pglue a) (?pushb (f a)) = ?pushc (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe
forallb : B,
(funw : Pushout f g => fam_podescent Pe w -> Type)
(pushl b)
exact (podd_faml Qe).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe
forallc : C,
(funw : Pushout f g => fam_podescent Pe w -> Type)
(pushr c)
exact (podd_famr Qe).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe
foralla : A,
transport
(funw : Pushout f g => fam_podescent Pe w -> Type)
(pglue a) (podd_faml Qe (f a)) = podd_famr Qe (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe a: A
transport
(funw : Pushout f g => fam_podescent Pe w -> Type)
(pglue a) (podd_faml Qe (f a)) = podd_famr Qe (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe a: A
podd_faml Qe (f a) =
transport
(funw : Pushout f g => fam_podescent Pe w -> Type)
(pglue a)^ (podd_famr Qe (g a))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe a: A pf: fam_podescent Pe (pushl (f a))
podd_faml Qe (f a) pf =
transport
(funw : Pushout f g => fam_podescent Pe w -> Type)
(pglue a)^ (podd_famr Qe (g a)) pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe a: A pf: fam_podescent Pe (pushl (f a))
podd_faml Qe (f a) pf =
podd_famr Qe (g a)
(transport (fam_podescent Pe) ((pglue a)^)^ pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe a: A pf: fam_podescent Pe (pushl (f a))
podd_faml Qe (f a) pf = podd_famr Qe (g a) ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe a: A pf: fam_podescent Pe (pushl (f a))
transport (fam_podescent Pe) ((pglue a)^)^ pf = ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe a: A pf: fam_podescent Pe (pushl (f a))
podd_faml Qe (f a) pf = podd_famr Qe (g a) ?Goal
exact (path_universe (podd_e _ _ _)).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe a: A pf: fam_podescent Pe (pushl (f a))
transport (fam_podescent Pe) ((pglue a)^)^ pf =
pod_e Pe a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Qe: poDepDescent Pe a: A pf: fam_podescent Pe (pushl (f a))
transport (fam_podescent Pe) (pglue a) pf =
pod_e Pe a pf
exact (transport_fam_podescent_pglue _ _ _).Defined.(** A section of dependent descent data [Qe : poDepDescent Pe] are fiberwise sections [podds_sectl] and [podds_sectr], together with coherences [pods_e]. *)RecordpoDepDescentSection {Pe : poDescent f g} {Qe : poDepDescent Pe} := {
podds_sectl (b : B) (pb : pod_faml Pe b) : podd_faml Qe b pb;
podds_sectr (c : C) (pc : pod_famr Pe c) : podd_famr Qe c pc;
podds_e (a : A) (pf : pod_faml Pe (f a))
: podd_e Qe a pf (podds_sectl (f a) pf) = podds_sectr (g a) (pod_e Pe a pf)
}.GlobalArguments poDepDescentSection {Pe} Qe.(** A dependent descent section induces a genuine section over the total space of [induced_fam_pod Pe]. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type s: poDepDescentSection (podepdescent_fam Q)
forall (x : Pushout f g) (px : fam_podescent Pe x),
Q x px
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type s: poDepDescentSection (podepdescent_fam Q)
forall (x : Pushout f g) (px : fam_podescent Pe x),
Q x px
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type s: poDepDescentSection (podepdescent_fam Q)
foralla : A,
transport
(funw : Pushout f g =>
forallpx : fam_podescent Pe w, Q w px) (pglue a)
(podds_sectl s (f a)) = podds_sectr s (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type s: poDepDescentSection (podepdescent_fam Q) a: A
transport
(funw : Pushout f g =>
forallpx : fam_podescent Pe w, Q w px) (pglue a)
(podds_sectl s (f a)) = podds_sectr s (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type s: poDepDescentSection (podepdescent_fam Q) a: A
forally1 : fam_podescent Pe (pushl (f a)),
transportD (fam_podescent Pe) Q (pglue a) y1
(podds_sectl s (f a) y1) =
podds_sectr s (g a)
(transport (fam_podescent Pe) (pglue a) y1)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type s: poDepDescentSection (podepdescent_fam Q) a: A pf: fam_podescent Pe (pushl (f a))
transportD (fam_podescent Pe) Q (pglue a) pf
(podds_sectl s (f a) pf) =
podds_sectr s (g a)
(transport (fam_podescent Pe) (pglue a) pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type s: poDepDescentSection (podepdescent_fam Q) a: A pf: fam_podescent Pe (pushl (f a))
transport (Q (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf)
(transportD (fam_podescent Pe) Q (pglue a) pf
(podds_sectl s (f a) pf)) =
transport (Q (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf)
(podds_sectr s (g a)
(transport (fam_podescent Pe) (pglue a) pf))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: forallx : Pushout f g, fam_podescent Pe x -> Type s: poDepDescentSection (podepdescent_fam Q) a: A pf: fam_podescent Pe (pushl (f a))
transport (Q (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf)
(transportD (fam_podescent Pe) Q (pglue a) pf
(podds_sectl s (f a) pf)) =
podds_sectr s (g a) (pod_e Pe a pf)
exact (podds_e s a pf).Defined.(** The data for a section into a constant type family. *)RecordpoDepDescentConstSection {Pe : poDescent f g} {Q : Type} := {
poddcs_sectl (b : B) (pb : pod_faml Pe b) : Q;
poddcs_sectr (c : C) (pc : pod_famr Pe c) : Q;
poddcs_e (a : A) (pf : pod_faml Pe (f a))
: poddcs_sectl (f a) pf = poddcs_sectr (g a) (pod_e Pe a pf)
}.GlobalArguments poDepDescentConstSection Pe Q : clear implicits.(** The data for a section of a constant family induces a section over the total space of [fam_podescent Pe]. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q
forallx : Pushout f g, fam_podescent Pe x -> Q
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q
forallx : Pushout f g, fam_podescent Pe x -> Q
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q
foralla : A,
transport
(funw : Pushout f g => fam_podescent Pe w -> Q)
(pglue a) (poddcs_sectl s (f a)) =
poddcs_sectr s (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A
transport
(funw : Pushout f g => fam_podescent Pe w -> Q)
(pglue a) (poddcs_sectl s (f a)) =
poddcs_sectr s (g a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A
forally1 : fam_podescent Pe (pushl (f a)),
transport (fun_ : Pushout f g => Q) (pglue a)
(poddcs_sectl s (f a) y1) =
poddcs_sectr s (g a)
(transport (fam_podescent Pe) (pglue a) y1)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: fam_podescent Pe (pushl (f a))
transport (fun_ : Pushout f g => Q) (pglue a)
(poddcs_sectl s (f a) pf) =
poddcs_sectr s (g a)
(transport (fam_podescent Pe) (pglue a) pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: fam_podescent Pe (pushl (f a))
poddcs_sectl s (f a) pf =
poddcs_sectr s (g a)
(transport (fam_podescent Pe) (pglue a) pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: fam_podescent Pe (pushl (f a))
poddcs_sectl s (f a) pf =
poddcs_sectr s (g a) (pod_e Pe a pf)
exact (poddcs_e s a pf).Defined.(** Here is the computation rule on paths. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
ap (sig_rec (podepdescent_rec s))
(path_sigma (fam_podescent Pe) (pushl (f a); pf)
(pushr (g a); pg) (pglue a)
(transport_fam_podescent_pglue Pe a pf @ pa)) =
poddcs_e s a pf @ ap (poddcs_sectr s (g a)) pa
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
ap (sig_rec (podepdescent_rec s))
(path_sigma (fam_podescent Pe) (pushl (f a); pf)
(pushr (g a); pg) (pglue a)
(transport_fam_podescent_pglue Pe a pf @ pa)) =
poddcs_e s a pf @ ap (poddcs_sectr s (g a)) pa
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
ap (sig_rec (podepdescent_rec s))
(path_sigma (fam_podescent Pe) (pushl (f a); pf)
(pushr (g a); pg) (pglue a)
(transport_fam_podescent_pglue Pe a pf
@' pa)) =
poddcs_e s a pf
@' ap (poddcs_sectr s (g a)) pa
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
ap (sig_rec (podepdescent_rec s))
(path_sigma (fam_podescent Pe) (pushl (f a); pf)
(pushr (g a); pod_e Pe a pf) (pglue a)
(transport_fam_podescent_pglue Pe a pf
@' 1)) =
poddcs_e s a pf
@' ap (poddcs_sectr s (g a)) 1
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
ap (sig_rec (podepdescent_rec s))
(path_sigma (fam_podescent Pe) (pushl (f a); pf)
(pushr (g a); pod_e Pe a pf) (pglue a)
(transport_fam_podescent_pglue Pe a pf
@' 1)) = poddcs_e s a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(transport_const (pglue a)
(podepdescent_rec s (pushl (f a)) pf))^
@' (ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf))^
@' (transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' ap10 (apD (podepdescent_rec s) (pglue a))
(transport (fam_podescent Pe) (pglue a) pf)
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1) = poddcs_e s a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
apD (podepdescent_rec s) (pglue a) = ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(transport_const (pglue a)
(podepdescent_rec s (pushl (f a)) pf))^
@' (ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf))^
@' (transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' ap10 ?Goal
(transport (fam_podescent Pe) (pglue a) pf)
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1) = poddcs_e s a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(transport_const (pglue a)
(podepdescent_rec s (pushl (f a)) pf))^
@' (ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf))^
@' (transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' ap10
(dpath_arrow (fam_podescent Pe)
(fun_ : Pushout f g => Q) (pglue a)
(poddcs_sectl s (f a)) (poddcs_sectr s (g a))
(funpf : fam_podescent Pe (pushl (f a)) =>
transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue Pe a
pf))^)))
(transport (fam_podescent Pe) (pglue a) pf)
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1) = poddcs_e s a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(transport_const (pglue a)
(podepdescent_rec s (pushl (f a)) pf))^
@' ((ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf))^
@' ((transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' (ap10
(dpath_arrow (fam_podescent Pe)
(fun_ : Pushout f g => Q) (pglue a)
(poddcs_sectl s (f a))
(poddcs_sectr s (g a))
(funpf : fam_podescent Pe
(pushl (f a)) =>
transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue
Pe a pf))^)))
(transport (fam_podescent Pe) (pglue a)
pf)
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a
pf
@' 1)))) = poddcs_e s a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf))^
@' ((transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' (ap10
(dpath_arrow (fam_podescent Pe)
(fun_ : Pushout f g => Q) (pglue a)
(poddcs_sectl s (f a))
(poddcs_sectr s (g a))
(funpf : fam_podescent Pe (pushl (f a))
=>
transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue
Pe a pf))^)))
(transport (fam_podescent Pe) (pglue a) pf)
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1))) =
transport_const (pglue a)
(podepdescent_rec s (pushl (f a)) pf)
@' poddcs_e s a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
ap10
(dpath_arrow (fam_podescent Pe)
(fun_ : Pushout f g => Q) (pglue a)
(poddcs_sectl s (f a)) (poddcs_sectr s (g a))
(funpf : fam_podescent Pe (pushl (f a)) =>
transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue Pe a pf))^)))
(transport (fam_podescent Pe) (pglue a) pf) = ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf))^
@' ((transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' (?Goal
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1))) =
transport_const (pglue a)
(podepdescent_rec s (pushl (f a)) pf)
@' poddcs_e s a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf))^
@' ((transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' (transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf)
@' ap
(funx : fam_podescent Pe (pushl (f a))
=>
transport (fun_ : Pushout f g => Q)
(pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe)
(pglue a) pf)
@' (funpf : fam_podescent Pe (pushl (f a)) =>
transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue
Pe a pf))^)) pf
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1))) =
transport_const (pglue a)
(podepdescent_rec s (pushl (f a)) pf)
@' poddcs_e s a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' (transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf)
@' ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q)
(pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf)
@' (transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue Pe a
pf))^))
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1)) = ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf))^
@' ?Goal =
transport_const (pglue a)
(podepdescent_rec s (pushl (f a)) pf)
@' poddcs_e s a pf
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' (transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf)
@' ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q)
(pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf)
@' (transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue Pe a
pf))^))
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1)) = ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' (transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf)
@' ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q)
(pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf)
@' (transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue Pe a
pf))^)
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1))) = ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf))^
@' (transport_arrow (pglue a)
(podepdescent_rec s (pushl (f a)))
(transport (fam_podescent Pe) (pglue a) pf)
@' (ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q)
(pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a)
pf)
@' (transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue
Pe a pf))^)
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a
pf
@' 1)))) = ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf)
@' (transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue Pe a pf))^)
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1)) = ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf)
@' (transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue Pe a pf))^
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf
@' 1))) = ?Goal
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf)
@' (transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' (poddcs_e s a pf
@' (ap (poddcs_sectr s (g a))
(transport_fam_podescent_pglue Pe a pf))^
@' ap (podepdescent_rec s (pushr (g a)))
(transport_fam_podescent_pglue Pe a pf))) =
?Goal
exact (1 @@ (1 @@ concat_pV_p _ _)).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g Q: Type s: poDepDescentConstSection Pe Q a: A pf: pod_faml Pe (f a)
(ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf))^
@' (ap
(funx : fam_podescent Pe (pushl (f a)) =>
transport (fun_ : Pushout f g => Q) (pglue a)
(podepdescent_rec s (pushl (f a)) x))
(transport_Vp (fam_podescent Pe) (pglue a) pf)
@' (transport_const (pglue a)
(poddcs_sectl s (f a) pf)
@' poddcs_e s a pf)) =
transport_const (pglue a)
(podepdescent_rec s (pushl (f a)) pf)
@' poddcs_e s a pf
napply concat_V_pp.Close Scope long_path_scope.Defined.EndDescent.(** ** The flattening lemma *)(** We saw above that given descent data [Pe] over a span [f : A -> B] and [g : A -> C], we obtained a type family [fam_podescent Pe] over the pushout. The flattening lemma describes the total space [sig (fam_podescent Pe)] of this type family as a pushout of [sig (pod_faml Pe)] and [sig (pod_famr Pe)] by a certain span. This follows from the work above, which shows that [sig (fam_podescent Pe)] has the same universal property as this pushout. *)SectionFlattening.Context `{Univalence} {A B C : Type} {f : A -> B} {g : A -> C} (Pe : poDescent f g).(** We mimic the constructors of [Pushout] for the total space. Here are the point constructors, in curried form. *)Definitionflatten_podl {b : B} (pb : pod_faml Pe b) : sig (fam_podescent Pe)
:= (pushl b; pb).Definitionflatten_podr {c : C} (pc : pod_famr Pe c) : sig (fam_podescent Pe)
:= (pushr c; pc).(** And here is the path constructor. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
flatten_podl pf = flatten_podr pg
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
flatten_podl pf = flatten_podr pg
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
(flatten_podl pf).1 = (flatten_podr pg).1
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
transport (fam_podescent Pe) ?p (flatten_podl pf).2 =
(flatten_podr pg).2
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
(flatten_podl pf).1 = (flatten_podr pg).1
byapply pglue.
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
transport (fam_podescent Pe) (pglue a)
(flatten_podl pf).2 = (flatten_podr pg).2
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a) pg: pod_famr Pe (g a) pa: pod_e Pe a pf = pg
pod_e Pe a (flatten_podl pf).2 = (flatten_podr pg).2
exact pa.Defined.(** Now that we've shown that [fam_podescent Pe] acts like a [Pushout] of [sig (pod_faml Pe)] and [sig (pod_famr Pe)] by an appropriate span, we can use this to prove the flattening lemma. The maps back and forth are very easy so this could almost be a formal consequence of the induction principle. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
{x : _ & fam_podescent Pe x} <~>
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
{x : _ & fam_podescent Pe x} <~>
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
{x : _ & fam_podescent Pe x} ->
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a)) ->
{x : _ & fam_podescent Pe x}
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
?f o ?g == idmap
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
?g o ?f == idmap
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
{x : _ & fam_podescent Pe x} ->
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forallproj1 : Pushout f g,
fam_podescent Pe proj1 ->
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
poDepDescentConstSection Pe
(Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a)))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forallb : B,
pod_faml Pe b ->
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forallc : C,
pod_famr Pe c ->
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forall (a : A) (pf : pod_faml Pe (f a)),
?poddcs_sectl (f a) pf =
?poddcs_sectr (g a) (pod_e Pe a pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forallb : B,
pod_faml Pe b ->
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
exact (funbpb => pushl (b; pb)).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forallc : C,
pod_famr Pe c ->
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
exact (funcpc => pushr (c; pc)).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forall (a : A) (pf : pod_faml Pe (f a)),
(fun (b : B) (pb : pod_faml Pe b) => pushl (b; pb))
(f a) pf =
(fun (c : C) (pc : pod_famr Pe c) => pushr (c; pc))
(g a) (pod_e Pe a pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
(fun (b : B) (pb : pod_faml Pe b) => pushl (b; pb))
(f a) pf =
(fun (c : C) (pc : pod_famr Pe c) => pushr (c; pc))
(g a) (pod_e Pe a pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
pushl (f a; pf) = pushr (g a; pod_e Pe a pf)
exact (@pglue _ _ _
(functor_sigma f (fun_ => idmap)) (functor_sigma g (pod_e Pe)) (a; pf)).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a)) ->
{x : _ & fam_podescent Pe x}
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
{x : _ & pod_faml Pe x} ->
{x : _ & fam_podescent Pe x}
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
{x : _ & pod_famr Pe x} ->
{x : _ & fam_podescent Pe x}
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
foralla : {H : A & pod_faml Pe (f H)},
?pushb (functor_sigma f (funa0 : A => idmap) a) =
?pushc (functor_sigma g (funa0 : A => pod_e Pe a0) a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
{x : _ & pod_faml Pe x} ->
{x : _ & fam_podescent Pe x}
exact (fun '(b; pb) => (pushl b; pb)).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
{x : _ & pod_famr Pe x} ->
{x : _ & fam_podescent Pe x}
exact (fun '(c; pc) => (pushr c; pc)).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
foralla : {H : A & pod_faml Pe (f H)},
(funpat : {x : _ & pod_faml Pe x} =>
letx := pat inletb := x.1inletpb := x.2in (pushl b; pb))
(functor_sigma f (funa0 : A => idmap) a) =
(funpat : {x : _ & pod_famr Pe x} =>
letx := pat inletc := x.1inletpc := x.2in (pushr c; pc))
(functor_sigma g (funa0 : A => pod_e Pe a0) a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
(pushl (f a); pf) = (pushr (g a); pod_e Pe a pf)
exact (flatten_pod_glue a 1).
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
:
(fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb)) (f a) pf =
(fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc)) (g a) (pod_e Pe a pf)
|})
o Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx := pat inletb := x.1inletpb := x.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx := pat inletc := x.1inletpc := x.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
(fun (a : A) (pf : pod_faml Pe (f a)) =>
flatten_pod_glue a 1
:
(letx :=
functor_sigma f (funa1 : A => idmap) (a; pf)
inletb := x.1inletpb := x.2in (pushl b; pb)) =
(letx :=
functor_sigma g (funa1 : A => pod_e Pe a1)
(a; pf) inletc := x.1inletpc := x.2in (pushr c; pc)))
a0.1 a0.2) == idmap
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forallb : {x : _ & pod_faml Pe x},
(funw : Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
=>
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b0 : B) (pb : pod_faml Pe b0) =>
pushl (b0; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
:
(fun (b0 : B) (pb : pod_faml Pe b0) =>
pushl (b0; pb)) (f a) pf =
(fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc)) (g a) (pod_e Pe a pf)
|})
o Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx := pat inletb0 := x.1inletpb := x.2in (pushl b0; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx := pat inletc := x.1inletpc := x.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
(fun (a : A) (pf : pod_faml Pe (f a)) =>
flatten_pod_glue a 1
:
(letx :=
functor_sigma f (funa1 : A => idmap)
(a; pf) inletb0 := x.1inletpb := x.2in (pushl b0; pb)) =
(letx :=
functor_sigma g (funa1 : A => pod_e Pe a1)
(a; pf) inletc := x.1inletpc := x.2in (pushr c; pc))) a0.1 a0.2))
w = idmap w) (pushl b)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forallc : {x : _ & pod_famr Pe x},
(funw : Pushout (functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
=>
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c0 : C) (pc : pod_famr Pe c0) =>
pushr (c0; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
:
(fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb)) (f a) pf =
(fun (c0 : C) (pc : pod_famr Pe c0) =>
pushr (c0; pc)) (g a) (pod_e Pe a pf)
|})
o Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx := pat inletb := x.1inletpb := x.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx := pat inletc0 := x.1inletpc := x.2in (pushr c0; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
(fun (a : A) (pf : pod_faml Pe (f a)) =>
flatten_pod_glue a 1
:
(letx :=
functor_sigma f (funa1 : A => idmap)
(a; pf) inletb := x.1inletpb := x.2in (pushl b; pb)) =
(letx :=
functor_sigma g (funa1 : A => pod_e Pe a1)
(a; pf) inletc0 := x.1inletpc := x.2in (pushr c0; pc))) a0.1 a0.2))
w = idmap w) (pushr c)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
foralla : {H : A & pod_faml Pe (f H)},
transport
(funw : Pushout
(functor_sigma f (funa0 : A => idmap))
(functor_sigma g
(funa0 : A => pod_e Pe a0)) =>
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a0 : A) (pf : pod_faml Pe (f a0)) =>
pglue (a0; pf)
:
(fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb)) (f a0) pf =
(fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc)) (g a0) (pod_e Pe a0 pf)
|})
o Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx := pat inletb := x.1inletpb := x.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx := pat inletc := x.1inletpc := x.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
(fun (a1 : A) (pf : pod_faml Pe (f a1)) =>
flatten_pod_glue a1 1
:
(letx :=
functor_sigma f (funa2 : A => idmap)
(a1; pf) inletb := x.1inletpb := x.2in (pushl b; pb)) =
(letx :=
functor_sigma g
(funa2 : A => pod_e Pe a2) (a1; pf) inletc := x.1inletpc := x.2in (pushr c; pc))) a0.1 a0.2))
w = idmap w) (pglue a)
(?pushb (functor_sigma f (funa0 : A => idmap) a)) =
?pushc (functor_sigma g (funa0 : A => pod_e Pe a0) a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
foralla : {H : A & pod_faml Pe (f H)},
transport
(funw : Pushout
(functor_sigma f (funa0 : A => idmap))
(functor_sigma g
(funa0 : A => pod_e Pe a0)) =>
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a0 : A) (pf : pod_faml Pe (f a0)) =>
pglue (a0; pf)
:
(fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb)) (f a0) pf =
(fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc)) (g a0) (pod_e Pe a0 pf)
|})
o Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx := pat inletb := x.1inletpb := x.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx := pat inletc := x.1inletpc := x.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
(fun (a1 : A) (pf : pod_faml Pe (f a1)) =>
flatten_pod_glue a1 1
:
(letx :=
functor_sigma f (funa2 : A => idmap)
(a1; pf) inletb := x.1inletpb := x.2in (pushl b; pb)) =
(letx :=
functor_sigma g
(funa2 : A => pod_e Pe a2) (a1; pf) inletc := x.1inletpc := x.2in (pushr c; pc))) a0.1 a0.2))
w = idmap w) (pglue a)
((funb : {x : _ & pod_faml Pe x} => 1)
(functor_sigma f (funa0 : A => idmap) a)) =
(func : {x : _ & pod_famr Pe x} => 1)
(functor_sigma g (funa0 : A => pod_e Pe a0) a)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
transport
(funw : Pushout
(functor_sigma f (funa : A => idmap))
(functor_sigma g (funa : A => pod_e Pe a))
=>
sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|})
(Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
(pushl pat.1; pat.2))
(funpat : {x : _ & pod_famr Pe x} =>
(pushr pat.1; pat.2))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11) w) = w)
(pglue (a; pf)) 1 = 1
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
ap
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|}))
(ap
(Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
(pushl pat.1; pat.2))
(funpat : {x : _ & pod_famr Pe x} =>
(pushr pat.1; pat.2))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)) (pglue (a; pf))) =
pglue (a; pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
ap
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|})) (flatten_pod_glue a 1) = pglue (a; pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
poddcs_e
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|} (a; pf).1 (a; pf).2 @
ap
(poddcs_sectr
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|} (g (a; pf).1)) 1 = pglue (a; pf)
napply concat_p1.
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx := pat inletb := x.1inletpb := x.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx := pat inletc := x.1inletpc := x.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
(fun (a : A) (pf : pod_faml Pe (f a)) =>
flatten_pod_glue a 1
:
(letx :=
functor_sigma f (funa1 : A => idmap) (a; pf)
inletb := x.1inletpb := x.2in (pushl b; pb)) =
(letx :=
functor_sigma g (funa1 : A => pod_e Pe a1)
(a; pf) inletc := x.1inletpc := x.2in (pushr c; pc)))
a0.1 a0.2)
o sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
:
(fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb)) (f a) pf =
(fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc)) (g a) (pod_e Pe a pf)
|}) == idmap
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forall (x : Pushout f g) (px : fam_podescent Pe x),
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx0 := pat inletb := x0.1inletpb := x0.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx0 := pat inletc := x0.1inletpc := x0.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|}) (x; px)) = (x; px)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
poDepDescentSection
(podepdescent_fam
(fun (x : Pushout f g) (px : fam_podescent Pe x)
=>
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx0 := pat inletb := x0.1inletpb := x0.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx0 := pat inletc := x0.1inletpc := x0.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a))
=> pglue (a; pf)
|}) (x; px)) = (x; px)))
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forall (b : B) (pb : pod_faml Pe b),
podd_faml
(podepdescent_fam
(fun (x : Pushout f g) (px : fam_podescent Pe x)
=>
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx0 := pat inletb0 := x0.1inletpb0 := x0.2in (pushl b0; pb0))
(funpat : {x : _ & pod_famr Pe x} =>
letx0 := pat inletc := x0.1inletpc := x0.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b0 : B) (pb0 : pod_faml Pe b0)
=> pushl (b0; pb0);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a))
=> pglue (a; pf)
|}) (x; px)) = (x; px))) b pb
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forall (c : C) (pc : pod_famr Pe c),
podd_famr
(podepdescent_fam
(fun (x : Pushout f g) (px : fam_podescent Pe x)
=>
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx0 := pat inletb := x0.1inletpb := x0.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx0 := pat inletc0 := x0.1inletpc0 := x0.2in (pushr c0; pc0))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c0 : C) (pc0 : pod_famr Pe c0)
=> pushr (c0; pc0);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a))
=> pglue (a; pf)
|}) (x; px)) = (x; px))) c pc
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forall (a : A) (pf : pod_faml Pe (f a)),
podd_e
(podepdescent_fam
(fun (x : Pushout f g) (px : fam_podescent Pe x)
=>
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx0 := pat inletb := x0.1inletpb := x0.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx0 := pat inletc := x0.1inletpc := x0.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a0 : A)
(pf0 : pod_faml Pe (f a0)) =>
pglue (a0; pf0)
|}) (x; px)) = (x; px))) a pf
(?podds_sectl (f a) pf) =
?podds_sectr (g a) (pod_e Pe a pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forall (b : B) (pb : pod_faml Pe b),
podd_faml
(podepdescent_fam
(fun (x : Pushout f g) (px : fam_podescent Pe x)
=>
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx0 := pat inletb0 := x0.1inletpb0 := x0.2in (pushl b0; pb0))
(funpat : {x : _ & pod_famr Pe x} =>
letx0 := pat inletc := x0.1inletpc := x0.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b0 : B) (pb0 : pod_faml Pe b0)
=> pushl (b0; pb0);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a))
=> pglue (a; pf)
|}) (x; px)) = (x; px))) b pb
byintros b pb.
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forall (c : C) (pc : pod_famr Pe c),
podd_famr
(podepdescent_fam
(fun (x : Pushout f g) (px : fam_podescent Pe x)
=>
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx0 := pat inletb := x0.1inletpb := x0.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx0 := pat inletc0 := x0.1inletpc0 := x0.2in (pushr c0; pc0))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c0 : C) (pc0 : pod_famr Pe c0)
=> pushr (c0; pc0);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a))
=> pglue (a; pf)
|}) (x; px)) = (x; px))) c pc
byintros c pc.
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g
forall (a : A) (pf : pod_faml Pe (f a)),
podd_e
(podepdescent_fam
(fun (x : Pushout f g) (px : fam_podescent Pe x)
=>
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
letx0 := pat inletb := x0.1inletpb := x0.2in (pushl b; pb))
(funpat : {x : _ & pod_famr Pe x} =>
letx0 := pat inletc := x0.1inletpc := x0.2in (pushr c; pc))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a0 : A)
(pf0 : pod_faml Pe (f a0)) =>
pglue (a0; pf0)
|}) (x; px)) = (x; px))) a pf
((fun (b : B) (pb : pod_faml Pe b) => 1) (f a) pf) =
(fun (c : C) (pc : pod_famr Pe c) => 1) (g a)
(pod_e Pe a pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
transportDD (fam_podescent Pe)
(fun (x : Pushout f g) (px : fam_podescent Pe x) =>
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
(pushl pat.1; pat.2))
(funpat : {x : _ & pod_famr Pe x} =>
(pushr pat.1; pat.2))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|}) (x; px)) = (x; px)) (pglue a)
(transport_fam_podescent_pglue Pe a pf) 1 = 1
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
transport
(funab : {x : _ & fam_podescent Pe x} =>
Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
(pushl pat.1; pat.2))
(funpat : {x : _ & pod_famr Pe x} =>
(pushr pat.1; pat.2))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11)
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|}) (ab.1; ab.2)) = (ab.1; ab.2))
(path_sigma' (fam_podescent Pe) (pglue a)
(transport_fam_podescent_pglue Pe a pf)) 1 = 1
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
ap
(Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
(pushl pat.1; pat.2))
(funpat : {x : _ & pod_famr Pe x} =>
(pushr pat.1; pat.2))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11))
(ap
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|}))
(path_sigma' (fam_podescent Pe) (pglue a)
(transport_fam_podescent_pglue Pe a pf))) =
path_sigma' (fam_podescent Pe) (pglue a)
(transport_fam_podescent_pglue Pe a pf)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
ap
(Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
(pushl pat.1; pat.2))
(funpat : {x : _ & pod_famr Pe x} =>
(pushr pat.1; pat.2))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11))
(ap
(sig_rec
(podepdescent_rec
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|}))
(path_sigma' (fam_podescent Pe) (pglue a)
(transport_fam_podescent_pglue Pe a pf @ 1))) =
path_sigma' (fam_podescent Pe) (pglue a)
(transport_fam_podescent_pglue Pe a pf @ 1)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
ap
(Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
(pushl pat.1; pat.2))
(funpat : {x : _ & pod_famr Pe x} =>
(pushr pat.1; pat.2))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11))
(poddcs_e
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|} a pf @
ap
(poddcs_sectr
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|} (g a)) 1) =
path_sigma' (fam_podescent Pe) (pglue a)
(transport_fam_podescent_pglue Pe a pf @ 1)
H: Univalence A, B, C: Type f: A -> B g: A -> C Pe: poDescent f g a: A pf: pod_faml Pe (f a)
ap
(Pushout_rec {x : _ & fam_podescent Pe x}
(funpat : {x : _ & pod_faml Pe x} =>
(pushl pat.1; pat.2))
(funpat : {x : _ & pod_famr Pe x} =>
(pushr pat.1; pat.2))
(funa0 : {H : A & pod_faml Pe (f H)} =>
flatten_pod_glue a0.11))
(poddcs_e
{|
poddcs_sectl :=
fun (b : B) (pb : pod_faml Pe b) =>
pushl (b; pb);
poddcs_sectr :=
fun (c : C) (pc : pod_famr Pe c) =>
pushr (c; pc);
poddcs_e :=
fun (a : A) (pf : pod_faml Pe (f a)) =>
pglue (a; pf)
|} a pf) =
path_sigma' (fam_podescent Pe) (pglue a)
(transport_fam_podescent_pglue Pe a pf @ 1)
exact (Pushout_rec_beta_pglue _ _ _ _ (a; pf)).Defined.EndFlattening.(** ** Characterization of path spaces *)(** A pointed type family over a pushout has an identity system structure precisely when its associated descent data satisfies Kraus and von Raumer's induction principle, https://arxiv.org/pdf/1901.06022. *)SectionPaths.(** Let [f : A -> B] and [g : A -> C] be a span, with a distinguished point [b0 : B]. We could let the distinguished point be in [C], but this is symmetric by exchanging the roles of [f] and [g]. Let [Pe : poDescent f g] be descent data over [f g] with a distinguished point [p0 : pod_faml Pe b0]. Assume that any dependent descent data [Qe : poDepDescent Pe] with a distinguished point [q0 : podd_faml Qe b0 p0] has a section that respects the distinguished points. This is the induction principle provided by Kraus and von Raumer. *)Context `{Univalence} {A B C : Type} {f : A -> B} {g : A -> C} (b0 : B)
(Pe : poDescent f g) (p0 : pod_faml Pe b0)
(based_podepdescent_ind : forall (Qe : poDepDescent Pe) (q0 : podd_faml Qe b0 p0),
poDepDescentSection Qe)
(based_podepdescent_ind_beta : forall (Qe : poDepDescent Pe) (q0 : podd_faml Qe b0 p0),
podds_sectl (based_podepdescent_ind Qe q0) b0 p0 = q0).(** Under these hypotheses, we get an identity system structure on [fam_podescent Pe]. *)
H: Univalence A, B, C: Type f: A -> B g: A -> C b0: B Pe: poDescent f g p0: pod_faml Pe b0 based_podepdescent_ind: forallQe : poDepDescent Pe,
podd_faml Qe b0 p0 ->
poDepDescentSection Qe based_podepdescent_ind_beta: forall
(Qe : poDepDescent Pe)
(q0 : podd_faml Qe b0 p0),
podds_sectl
(based_podepdescent_ind
Qe q0) b0 p0 = q0
IsIdentitySystem (fam_podescent Pe) p0
H: Univalence A, B, C: Type f: A -> B g: A -> C b0: B Pe: poDescent f g p0: pod_faml Pe b0 based_podepdescent_ind: forallQe : poDepDescent Pe,
podd_faml Qe b0 p0 ->
poDepDescentSection Qe based_podepdescent_ind_beta: forall
(Qe : poDepDescent Pe)
(q0 : podd_faml Qe b0 p0),
podds_sectl
(based_podepdescent_ind
Qe q0) b0 p0 = q0
IsIdentitySystem (fam_podescent Pe) p0
H: Univalence A, B, C: Type f: A -> B g: A -> C b0: B Pe: poDescent f g p0: pod_faml Pe b0 based_podepdescent_ind: forallQe : poDepDescent Pe,
podd_faml Qe b0 p0 ->
poDepDescentSection Qe based_podepdescent_ind_beta: forall
(Qe : poDepDescent Pe)
(q0 : podd_faml Qe b0 p0),
podds_sectl
(based_podepdescent_ind
Qe q0) b0 p0 = q0
forallD : foralla : Pushout f g, fam_podescent Pe a -> Type,
D (pushl b0) p0 ->
forall (a : Pushout f g) (r : fam_podescent Pe a),
D a r
H: Univalence A, B, C: Type f: A -> B g: A -> C b0: B Pe: poDescent f g p0: pod_faml Pe b0 based_podepdescent_ind: forallQe : poDepDescent Pe,
podd_faml Qe b0 p0 ->
poDepDescentSection Qe based_podepdescent_ind_beta: forall
(Qe : poDepDescent Pe)
(q0 : podd_faml Qe b0 p0),
podds_sectl
(based_podepdescent_ind
Qe q0) b0 p0 = q0
forall
(D : foralla : Pushout f g,
fam_podescent Pe a -> Type)
(d : D (pushl b0) p0),
?idsys_ind D d (pushl b0) p0 = d
H: Univalence A, B, C: Type f: A -> B g: A -> C b0: B Pe: poDescent f g p0: pod_faml Pe b0 based_podepdescent_ind: forallQe : poDepDescent Pe,
podd_faml Qe b0 p0 ->
poDepDescentSection Qe based_podepdescent_ind_beta: forall
(Qe : poDepDescent Pe)
(q0 : podd_faml Qe b0 p0),
podds_sectl
(based_podepdescent_ind
Qe q0) b0 p0 = q0
forallD : foralla : Pushout f g, fam_podescent Pe a -> Type,
D (pushl b0) p0 ->
forall (a : Pushout f g) (r : fam_podescent Pe a),
D a r
H: Univalence A, B, C: Type f: A -> B g: A -> C b0: B Pe: poDescent f g p0: pod_faml Pe b0 based_podepdescent_ind: forallQe : poDepDescent Pe,
podd_faml Qe b0 p0 ->
poDepDescentSection Qe based_podepdescent_ind_beta: forall
(Qe : poDepDescent Pe)
(q0 : podd_faml Qe b0 p0),
podds_sectl
(based_podepdescent_ind
Qe q0) b0 p0 = q0 Q: foralla : Pushout f g, fam_podescent Pe a -> Type q0: Q (pushl b0) p0 x: Pushout f g px: fam_podescent Pe x
Q x px
H: Univalence A, B, C: Type f: A -> B g: A -> C b0: B Pe: poDescent f g p0: pod_faml Pe b0 based_podepdescent_ind: forallQe : poDepDescent Pe,
podd_faml Qe b0 p0 ->
poDepDescentSection Qe based_podepdescent_ind_beta: forall
(Qe : poDepDescent Pe)
(q0 : podd_faml Qe b0 p0),
podds_sectl
(based_podepdescent_ind
Qe q0) b0 p0 = q0 Q: foralla : Pushout f g, fam_podescent Pe a -> Type q0: Q (pushl b0) p0 x: Pushout f g px: fam_podescent Pe x
poDepDescentSection (podepdescent_fam Q)
byapply based_podepdescent_ind.
H: Univalence A, B, C: Type f: A -> B g: A -> C b0: B Pe: poDescent f g p0: pod_faml Pe b0 based_podepdescent_ind: forallQe : poDepDescent Pe,
podd_faml Qe b0 p0 ->
poDepDescentSection Qe based_podepdescent_ind_beta: forall
(Qe : poDepDescent Pe)
(q0 : podd_faml Qe b0 p0),
podds_sectl
(based_podepdescent_ind
Qe q0) b0 p0 = q0
forall
(D : foralla : Pushout f g,
fam_podescent Pe a -> Type)
(d : D (pushl b0) p0),
(fun
(Q : foralla : Pushout f g,
fam_podescent Pe a -> Type)
(q0 : Q (pushl b0) p0) (x : Pushout f g)
(px : fam_podescent Pe x) =>
podepdescent_ind
(based_podepdescent_ind (podepdescent_fam Q) q0) x
px) D d (pushl b0) p0 = d
H: Univalence A, B, C: Type f: A -> B g: A -> C b0: B Pe: poDescent f g p0: pod_faml Pe b0 based_podepdescent_ind: forallQe : poDepDescent Pe,
podd_faml Qe b0 p0 ->
poDepDescentSection Qe based_podepdescent_ind_beta: forall
(Qe : poDepDescent Pe)
(q0 : podd_faml Qe b0 p0),
podds_sectl
(based_podepdescent_ind
Qe q0) b0 p0 = q0 Q: foralla : Pushout f g, fam_podescent Pe a -> Type q0: Q (pushl b0) p0
napply (based_podepdescent_ind_beta (podepdescent_fam Q)).Defined.(** It follows that the fibers [fam_podescent Pe x] are equivalent to path spaces [(pushl a0) = x]. *)Definitionfam_podescent_equiv_path (x : Pushout f g)
: (pushl b0) = x <~> fam_podescent Pe x
:= @equiv_transport_identitysystem _ (pushl b0) (fam_podescent Pe) p0 _ x.EndPaths.