Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.UniverseTypes.Prod.Require Import Colimits.GraphQuotient.LocalOpen Scope path_scope.(** * Homotopy coequalizers *)(** ** Definition *)DefinitionCoeq@{i j u} {B : Type@{i}} {A : Type@{j}} (f g : B -> A) : Type@{u}
:= GraphQuotient@{i j u} (funab => {x : B & (f x = a) * (g x = b)}).Definitioncoeq {BAfg} (a : A) : @Coeq B A f g := gq a.Definitioncglue {BAfg} b : @coeq B A f g (f b) = coeq (g b)
:= gqglue (b; (idpath,idpath)).Arguments Coeq : simpl never.Arguments coeq : simpl never.Arguments cglue : simpl never.
B, A: Type f, g: B -> A P: Coeq f g -> Type coeq': foralla : A, P (coeq a) cglue': forallb : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b)
forallw : Coeq f g, P w
B, A: Type f, g: B -> A P: Coeq f g -> Type coeq': foralla : A, P (coeq a) cglue': forallb : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b)
forallw : Coeq f g, P w
B, A: Type f, g: B -> A P: Coeq f g -> Type coeq': foralla : A, P (coeq a) cglue': forallb : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b)
forall (ab : A)
(s : {x : B & (f x = a) * (g x = b)}),
transport P (gqglue s) (?Goal a) = ?Goal b
B, A: Type f, g: B -> A P: Coeq f g -> Type coeq': foralla : A, P (coeq a) cglue': forallb : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b) a, b: A x: B
transport P (gqglue (x; (1, 1))) (?Goal (f x)) =
?Goal (g x)
exact (cglue' x).Defined.
B, A: Type f, g: B -> A P: Coeq f g -> Type coeq': foralla : A, P (coeq a) cglue': forallb : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b) b: B
apD (Coeq_ind P coeq' cglue') (cglue b) = cglue' b
B, A: Type f, g: B -> A P: Coeq f g -> Type coeq': foralla : A, P (coeq a) cglue': forallb : B,
transport P (cglue b) (coeq' (f b)) =
coeq' (g b) b: B
apD (Coeq_ind P coeq' cglue') (cglue b) = cglue' b
rapply GraphQuotient_ind_beta_gqglue.Defined.
B, A: Type f, g: B -> A P: Type coeq': A -> P cglue': forallb : B, coeq' (f b) = coeq' (g b)
Coeq f g -> P
B, A: Type f, g: B -> A P: Type coeq': A -> P cglue': forallb : B, coeq' (f b) = coeq' (g b)
Coeq f g -> P
B, A: Type f, g: B -> A P: Type coeq': A -> P cglue': forallb : B, coeq' (f b) = coeq' (g b)
forallab : A,
{x : B & (f x = a) * (g x = b)} -> ?Goal a = ?Goal b
B, A: Type f, g: B -> A P: Type coeq': A -> P cglue': forallb : B, coeq' (f b) = coeq' (g b) a, b: A x: B
?Goal (f x) = ?Goal (g x)
exact (cglue' x).Defined.
B, A: Type f, g: B -> A P: Type coeq': A -> P cglue': forallb : B, coeq' (f b) = coeq' (g b) b: B
ap (Coeq_rec P coeq' cglue') (cglue b) = cglue' b
B, A: Type f, g: B -> A P: Type coeq': A -> P cglue': forallb : B, coeq' (f b) = coeq' (g b) b: B
ap (Coeq_rec P coeq' cglue') (cglue b) = cglue' b
rapply GraphQuotient_rec_beta_gqglue.Defined.(** ** Universal property *)(** See Colimits/CoeqUnivProp.v for a similar universal property without [Funext]. *)
B, A: Type f, g: B -> A P: Type h: Coeq f g -> P
{k : A -> P & k o f == k o g}
B, A: Type f, g: B -> A P: Type h: Coeq f g -> P
{k : A -> P & k o f == k o g}
B, A: Type f, g: B -> A P: Type h: Coeq f g -> P
(funx : B => h (coeq (f x))) ==
(funx : B => h (coeq (g x)))
B, A: Type f, g: B -> A P: Type h: Coeq f g -> P b: B
h (coeq (f b)) = h (coeq (g b))
exact (ap h (cglue b)).Defined.
H: Funext B, A: Type f, g: B -> A P: Type
IsEquiv
(funp : {h : A -> P & h o f == h o g} =>
Coeq_rec P p.1 p.2)
H: Funext B, A: Type f, g: B -> A P: Type
IsEquiv
(funp : {h : A -> P & h o f == h o g} =>
Coeq_rec P p.1 p.2)
H: Funext B, A: Type f, g: B -> A P: Type
(funp : {h : A -> P & h o f == h o g} =>
Coeq_rec P p.1 p.2) o Coeq_unrec f g == idmap
H: Funext B, A: Type f, g: B -> A P: Type
Coeq_unrec f g
o (funp : {h : A -> P & h o f == h o g} =>
Coeq_rec P p.1 p.2) == idmap
H: Funext B, A: Type f, g: B -> A P: Type
(funp : {h : A -> P & h o f == h o g} =>
Coeq_rec P p.1 p.2) o Coeq_unrec f g == idmap
H: Funext B, A: Type f, g: B -> A P: Type h: Coeq f g -> P
Coeq_rec P (Coeq_unrec f g h).1 (Coeq_unrec f g h).2 =
h
H: Funext B, A: Type f, g: B -> A P: Type h: Coeq f g -> P
Coeq_rec P (Coeq_unrec f g h).1 (Coeq_unrec f g h).2 ==
h
H: Funext B, A: Type f, g: B -> A P: Type h: Coeq f g -> P b: A
(funw : Coeq f g =>
Coeq_rec P (Coeq_unrec f g h).1 (Coeq_unrec f g h).2
w = h w) (coeq b)
H: Funext B, A: Type f, g: B -> A P: Type h: Coeq f g -> P b: B
transport
(funw : Coeq f g =>
Coeq_rec P (Coeq_unrec f g h).1
(Coeq_unrec f g h).2 w = h w) (cglue b)
((funb : A => ?Goal) (f b)) =
(funb : A => ?Goal) (g b)
H: Funext B, A: Type f, g: B -> A P: Type h: Coeq f g -> P b: B
transport
(funw : Coeq f g =>
Coeq_rec P (Coeq_unrec f g h).1
(Coeq_unrec f g h).2 w = h w) (cglue b)
((funb : A =>
1
:
(funw : Coeq f g =>
Coeq_rec P (Coeq_unrec f g h).1
(Coeq_unrec f g h).2 w = h w) (coeq b)) (f b)) =
(funb : A =>
1
:
(funw : Coeq f g =>
Coeq_rec P (Coeq_unrec f g h).1 (Coeq_unrec f g h).2
w = h w) (coeq b)) (g b)
H: Funext B, A: Type f, g: B -> A P: Type h: Coeq f g -> P b: B
transport
(funw : Coeq f g =>
Coeq_rec P (funx : A => h (coeq x))
(funb : B => ap h (cglue b)) w = h w) (cglue b)
1 = 1
H: Funext B, A: Type f, g: B -> A P: Type h: Coeq f g -> P b: B
ap
(Coeq_rec P (funx : A => h (coeq x))
(funb : B => ap h (cglue b))) (cglue b) @ 1 =
1 @ ap h (cglue b)
H: Funext B, A: Type f, g: B -> A P: Type h: Coeq f g -> P b: B
ap
(Coeq_rec P (funx : A => h (coeq x))
(funb : B => ap h (cglue b))) (cglue b) =
ap h (cglue b)
nrapply Coeq_rec_beta_cglue.
H: Funext B, A: Type f, g: B -> A P: Type
Coeq_unrec f g
o (funp : {h : A -> P & h o f == h o g} =>
Coeq_rec P p.1 p.2) == idmap
H: Funext B, A: Type f, g: B -> A P: Type h: A -> P q: (funx : B => h (f x)) == (funx : B => h (g x))
(funx : A => Coeq_rec P (h; q).1 (h; q).2 (coeq x)) =
h
H: Funext B, A: Type f, g: B -> A P: Type h: A -> P q: (funx : B => h (f x)) == (funx : B => h (g x))
transport
(funk : A -> P =>
(funx : B => k (f x)) == (funx : B => k (g x)))
?p
(funb : B =>
ap (Coeq_rec P (h; q).1 (h; q).2) (cglue b)) = q
H: Funext B, A: Type f, g: B -> A P: Type h: A -> P q: (funx : B => h (f x)) == (funx : B => h (g x))
(funx : A => Coeq_rec P (h; q).1 (h; q).2 (coeq x)) =
h
reflexivity.
H: Funext B, A: Type f, g: B -> A P: Type h: A -> P q: (funx : B => h (f x)) == (funx : B => h (g x))
transport
(funk : A -> P =>
(funx : B => k (f x)) == (funx : B => k (g x))) 1
(funb : B =>
ap (Coeq_rec P (h; q).1 (h; q).2) (cglue b)) = q
H: Funext B, A: Type f, g: B -> A P: Type h: A -> P q: (funx : B => h (f x)) == (funx : B => h (g x))
(funb : B => ap (Coeq_rec P h q) (cglue b)) = q
H: Funext B, A: Type f, g: B -> A P: Type h: A -> P q: (funx : B => h (f x)) == (funx : B => h (g x)) b: B
ap (Coeq_rec P h q) (cglue b) = q b
apply Coeq_rec_beta_cglue.Defined.Definitionequiv_Coeq_rec `{Funext} {B A} (f g : B -> A) P
: {h : A -> P & h o f == h o g} <~> (Coeq f g -> P)
:= Build_Equiv _ _ _ (isequiv_Coeq_rec f g P).(** ** Functoriality *)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h
Coeq f g -> Coeq f' g'
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h
Coeq f g -> Coeq f' g'
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h b: B
coeq (k (f b)) = coeq (k (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h b: B
coeq (f' (h b)) = coeq (g' (h b))
apply cglue.Defined.Definitionfunctor_coeq_beta_cglue {BAfgB'A'f'g'}
(h : B -> B') (k : A -> A')
(p : k o f == f' o h) (q : k o g == g' o h)
(b : B)
: ap (functor_coeq h k p q) (cglue b)
= ap coeq (p b) @ cglue (h b) @ ap coeq (q b)^
:= (Coeq_rec_beta_cglue _ _ _ b).
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h'
functor_coeq (h' o h) (k' o k)
(funb : B => ap k' (p b) @ p' (h b))
(funb : B => ap k' (q b) @ q' (h b)) ==
functor_coeq h' k' p' q' o functor_coeq h k p q
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h'
functor_coeq (h' o h) (k' o k)
(funb : B => ap k' (p b) @ p' (h b))
(funb : B => ap k' (q b) @ q' (h b)) ==
functor_coeq h' k' p' q' o functor_coeq h k p q
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h' b: B
transport
(funw : Coeq f g =>
functor_coeq (funx : B => h' (h x))
(funx : A => k' (k x))
(funb : B => ap k' (p b) @ p' (h b))
(funb : B => ap k' (q b) @ q' (h b)) w =
functor_coeq h' k' p' q' (functor_coeq h k p q w))
(cglue b) 1 = 1
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h' b: B
ap
(functor_coeq (funx : B => h' (h x))
(funx : A => k' (k x))
(funb : B => ap k' (p b) @ p' (h b))
(funb : B => ap k' (q b) @ q' (h b))) (cglue b) @
1 =
1 @
ap
(funx : Coeq f g =>
functor_coeq h' k' p' q' (functor_coeq h k p q x))
(cglue b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h' b: B
ap
(funx : Coeq f g =>
functor_coeq h' k' p' q' (functor_coeq h k p q x))
(cglue b) =
ap
(functor_coeq (funx : B => h' (h x))
(funx : A => k' (k x))
(funb : B => ap k' (p b) @ p' (h b))
(funb : B => ap k' (q b) @ q' (h b))) (cglue b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h' b: B
ap (functor_coeq h' k' p' q')
(ap (functor_coeq h k p q) (cglue b)) =
ap
(functor_coeq (funx : B => h' (h x))
(funx : A => k' (k x))
(funb : B => ap k' (p b) @ p' (h b))
(funb : B => ap k' (q b) @ q' (h b))) (cglue b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h' b: B
(ap (functor_coeq h' k' p' q') (ap coeq (p b)) @
((ap coeq (p' (h b)) @ cglue (h' (h b))) @
ap coeq (q' (h b))^)) @
ap (functor_coeq h' k' p' q') (ap coeq (q b)^) =
((ap coeq (ap k' (p b)) @ ap coeq (p' (h b))) @
cglue (h' (h b))) @ ap coeq (ap k' (q b) @ q' (h b))^
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h' b: B
(ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(p b) @
((ap coeq (p' (h b)) @ cglue (h' (h b))) @
ap coeq (q' (h b))^)) @
ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(q b)^ =
((ap (funx : A' => coeq (k' x)) (p b) @
ap coeq (p' (h b))) @ cglue (h' (h b))) @
ap coeq (ap k' (q b) @ q' (h b))^
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h' b: B
(ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(p b) @
((ap coeq (p' (h b)) @ cglue (h' (h b))) @
ap coeq (q' (h b))^)) @
ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(q b)^ =
((ap (funx : A' => coeq (k' x)) (p b) @
ap coeq (p' (h b))) @ cglue (h' (h b))) @
ap coeq (ap k' (q b) @ q' (h b))^
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' B'', A'': Type f'', g'': B'' -> A'' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B'' k': A' -> A'' p': k' o f' == f'' o h' q': k' o g' == g'' o h' b: B
(((ap
(funx : A' => functor_coeq h' k' p' q' (coeq x))
(p b) @ ap coeq (p' (h b))) @ cglue (h' (h b))) @
(ap coeq (q' (h b)))^) @
(ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(q b))^ =
(((ap (funx : A' => coeq (k' x)) (p b) @
ap coeq (p' (h b))) @ cglue (h' (h b))) @
(ap coeq (q' (h b)))^) @
(ap (funx : A' => coeq (k' x)) (q b))^
reflexivity.Qed.
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b) @ p' b = p b @ ap f' (r b) v: forallb : B, s (g b) @ q' b = q b @ ap g' (r b)
functor_coeq h k p q == functor_coeq h' k' p' q'
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b) @ p' b = p b @ ap f' (r b) v: forallb : B, s (g b) @ q' b = q b @ ap g' (r b)
functor_coeq h k p q == functor_coeq h' k' p' q'
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b) @ p' b = p b @ ap f' (r b) v: forallb : B, s (g b) @ q' b = q b @ ap g' (r b) b: B
transport
(funw : Coeq f g =>
functor_coeq h k p q w = functor_coeq h' k' p' q' w)
(cglue b) (ap coeq (s (f b))) = ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b) @ p' b = p b @ ap f' (r b) v: forallb : B, s (g b) @ q' b = q b @ ap g' (r b) b: B
((ap (functor_coeq h k p q) (cglue b))^ @
ap coeq (s (f b))) @
ap (functor_coeq h' k' p' q') (cglue b) =
ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b) @ p' b = p b @ ap f' (r b) v: forallb : B, s (g b) @ q' b = q b @ ap g' (r b) b: B
ap coeq (s (f b)) @
ap (functor_coeq h' k' p' q') (cglue b) =
ap (functor_coeq h k p q) (cglue b) @
ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b) @ p' b = p b @ ap f' (r b) v: forallb : B, s (g b) @ q' b = q b @ ap g' (r b) b: B
ap coeq (s (f b)) @
((ap coeq (p' b) @ cglue (h' b)) @ ap coeq (q' b)^) =
((ap coeq (p b) @ cglue (h b)) @ ap coeq (q b)^) @
ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b)
@' p' b = p b
@' ap f' (r b) v: forallb : B, s (g b)
@' q' b = q b
@' ap g' (r b) b: B
ap coeq (s (f b))
@' (ap coeq (p' b)
@' cglue (h' b)
@' ap coeq (q' b)^) =
ap coeq (p b)
@' cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b)
@' p' b = p b
@' ap f' (r b) v: forallb : B, s (g b)
@' q' b = q b
@' ap g' (r b) b: B
ap coeq (s (f b))
@' ap coeq (p' b)
@' cglue (h' b)
@' ap coeq (q' b)^ =
ap coeq (p b)
@' cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b)
@' p' b = p b
@' ap f' (r b) v: forallb : B, s (g b)
@' q' b = q b
@' ap g' (r b) b: B
ap coeq (s (f b)
@' p' b)
@' cglue (h' b)
@' ap coeq (q' b)^ =
ap coeq (p b)
@' cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b)
@' p' b = p b
@' ap f' (r b) v: forallb : B, s (g b)
@' q' b = q b
@' ap g' (r b) b: B
ap coeq (ap f' (r b))
@' cglue (h' b)
@' ap coeq (q' b)^ =
cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b)
@' p' b = p b
@' ap f' (r b) v: forallb : B, s (g b)
@' q' b = q b
@' ap g' (r b) b: B
ap coeq (ap f' (r b))
@' cglue (h' b) =
cglue (h b)
@' ap coeq (q b)^
@' ap coeq (s (g b))
@' ap coeq (q' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b)
@' p' b = p b
@' ap f' (r b) v: forallb : B, s (g b)
@' q' b = q b
@' ap g' (r b) b: B
ap coeq (ap f' (r b))
@' cglue (h' b) =
cglue (h b)
@' (ap coeq (q b)^
@' ap coeq (s (g b)
@' q' b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b)
@' p' b = p b
@' ap f' (r b) v: forallb : B, s (g b)
@' q' b = q b
@' ap g' (r b) b: B
ap coeq (ap f' (r b))
@' cglue (h' b) = cglue (h b)
@' ap coeq (ap g' (r b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B -> B' k': A -> A' p': k' o f == f' o h' q': k' o g == g' o h' r: h == h' s: k == k' u: forallb : B, s (f b)
@' p' b = p b
@' ap f' (r b) v: forallb : B, s (g b)
@' q' b = q b
@' ap g' (r b) b: B
ap (funx : B' => coeq (f' x)) (r b)
@' cglue (h' b) =
cglue (h b)
@' ap (funx : B' => coeq (g' x)) (r b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b) v: forallb : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
functor_coeq h' k' p' q' o functor_coeq h k p q ==
idmap
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b) v: forallb : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b)
functor_coeq h' k' p' q' o functor_coeq h k p q ==
idmap
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b) v: forallb : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b) b: B
transport
(funw : Coeq f g =>
functor_coeq h' k' p' q' (functor_coeq h k p q w) =
w) (cglue b) (ap coeq (s (f b))) =
ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b) v: forallb : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b) b: B
((ap (functor_coeq h' k' p' q')
(ap (functor_coeq h k p q) (cglue b)))^ @
ap coeq (s (f b))) @ cglue b = ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b) v: forallb : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b) b: B
ap coeq (s (f b)) @ cglue b =
ap (functor_coeq h' k' p' q')
(ap (functor_coeq h k p q) (cglue b)) @
ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b) v: forallb : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b) b: B
ap coeq (s (f b)) @ cglue b =
((ap (functor_coeq h' k' p' q') (ap coeq (p b)) @
ap (functor_coeq h' k' p' q') (cglue (h b))) @
ap (functor_coeq h' k' p' q') (ap coeq (q b)^)) @
ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b) v: forallb : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b) b: B
ap coeq (s (f b)) @ cglue b =
((ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(p b) @
ap (functor_coeq h' k' p' q') (cglue (h b))) @
ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(q b)^) @ ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
(ap k' (p b) @ p' (h b)) @ ap f (r b) = s (f b) v: forallb : B,
(ap k' (q b) @ q' (h b)) @ ap g (r b) = s (g b) b: B
ap coeq (s (f b)) @ cglue b =
((ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(p b) @
((ap coeq (p' (h b)) @ cglue (h' (h b))) @
ap coeq (q' (h b))^)) @
ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(q b)^) @ ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b) v: forallb : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b) b: B
ap coeq (s (f b))
@' cglue b =
ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(p b)
@' (ap coeq (p' (h b))
@' cglue (h' (h b))
@' ap coeq (q' (h b))^)
@' ap
(funx : A' => functor_coeq h' k' p' q' (coeq x))
(q b)^
@' ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b) v: forallb : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b) b: B
ap coeq (s (f b))
@' cglue b =
ap (funx : A' => functor_coeq h' k' p' q' (coeq x))
(p b)
@' ap coeq (p' (h b))
@' cglue (h' (h b))
@' ap coeq (q' (h b))^
@' ap
(funx : A' => functor_coeq h' k' p' q' (coeq x))
(q b)^
@' ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b) v: forallb : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b) b: B
ap coeq (ap k' (p b))
@' ap coeq (p' (h b))
@' ap coeq (ap f (r b))
@' cglue b =
ap coeq (ap k' (p b))
@' ap coeq (p' (h b))
@' cglue (h' (h b))
@' ap coeq (q' (h b))^
@' ap coeq (ap k' (q b)^)
@' ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b) v: forallb : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b) b: B
ap coeq (ap f (r b))
@' cglue b =
cglue (h' (h b))
@' (ap coeq (q' (h b))^
@' (ap coeq (ap k' (q b)^)
@' ap coeq (s (g b))))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b) v: forallb : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b) b: B
ap coeq (ap f (r b))
@' cglue b =
cglue (h' (h b))
@' ap coeq (q' (h b))^
@' ap coeq (ap k' (q b)^)
@' ap coeq (s (g b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b) v: forallb : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b) b: B
ap coeq (ap f (r b))
@' cglue b =
cglue (h' (h b))
@' ap coeq (q' (h b))^
@' ap coeq (ap k' (q b)^)
@' ap coeq (ap k' (q b)
@' q' (h b)
@' ap g (r b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b) v: forallb : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b) b: B
ap coeq (ap f (r b))
@' cglue b = cglue (h' (h b))
@' ap coeq (ap g (r b))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' p: k o f == f' o h q: k o g == g' o h h': B' -> B k': A' -> A p': k' o f' == f o h' q': k' o g' == g o h' r: h' o h == idmap s: k' o k == idmap u: forallb : B,
ap k' (p b)
@' p' (h b)
@' ap f (r b) = s (f b) v: forallb : B,
ap k' (q b)
@' q' (h b)
@' ap g (r b) = s (g b) b: B
ap (funx : B => coeq (f x)) (r b)
@' cglue b =
cglue (h' (h b))
@' ap (funx : B => coeq (g x)) (r b)
exact (concat_Ap cglue (r b)).Close Scope long_path_scope.Qed.SectionIsEquivFunctorCoeq.Context {BAfgB'A'f'g'}
(h : B -> B') (k : A -> A')
`{IsEquiv _ _ h} `{IsEquiv _ _ k}
(p : k o f == f' o h) (q : k o g == g' o h).
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
Coeq f' g' -> Coeq f g
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
Coeq f' g' -> Coeq f g
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
(funx : B' => k^-1 (f' x)) ==
(funx : B' => f (h^-1 x))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
(funx : B' => k^-1 (g' x)) ==
(funx : B' => g (h^-1 x))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
(funx : B' => k^-1 (f' x)) ==
(funx : B' => f (h^-1 x))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
k^-1 (f' b) = f (h^-1 b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
k^-1 (f' (h (h^-1 b))) = k^-1 (k (f (h^-1 b)))
apply ap, inverse, p.
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
(funx : B' => k^-1 (g' x)) ==
(funx : B' => g (h^-1 x))
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
k^-1 (g' b) = g (h^-1 b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
k^-1 (g' (h (h^-1 b))) = k^-1 (k (g (h^-1 b)))
apply ap, inverse, q.Defined.
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
functor_coeq h k p q o functor_coeq_inverse == idmap
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
functor_coeq h k p q o functor_coeq_inverse == idmap
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
functor_coeq h k p q o functor_coeq_inverse == idmap
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k
(ap (funx : B' => k^-1 (f' x)) (eisretr h b)^
@' ap k^-1 (p (h^-1 b))^
@' eissect k (f (h^-1 b)))
@' p (h^-1 b)
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k
(ap (funx : B' => k^-1 (g' x)) (eisretr h b)^
@' ap k^-1 (q (h^-1 b))^
@' eissect k (g (h^-1 b)))
@' q (h^-1 b)
@' ap g' (eisretr h b) = eisretr k (g' b)
(** The two proofs are identical modulo replacing [f] by [g], [f'] by [g'], and [p] by [q]. *)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k (ap (funx : B' => k^-1 (f' x)) (eisretr h b)^)
@' ap k (ap k^-1 (p (h^-1 b))^)
@' eisretr k (k (f (h^-1 b)))
@' p (h^-1 b)
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k (ap (funx : B' => k^-1 (g' x)) (eisretr h b)^)
@' ap k (ap k^-1 (q (h^-1 b))^)
@' eisretr k (k (g (h^-1 b)))
@' q (h^-1 b)
@' ap g' (eisretr h b) = eisretr k (g' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k (ap (funx : B' => k^-1 (f' x)) (eisretr h b)^)
@' ap (funx : A' => k (k^-1 x)) (p (h^-1 b))^
@' eisretr k (k (f (h^-1 b)))
@' p (h^-1 b)
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k (ap (funx : B' => k^-1 (g' x)) (eisretr h b)^)
@' ap (funx : A' => k (k^-1 x)) (q (h^-1 b))^
@' eisretr k (k (g (h^-1 b)))
@' q (h^-1 b)
@' ap g' (eisretr h b) = eisretr k (g' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k (ap (funx : B' => k^-1 (f' x)) (eisretr h b)^)
@' eisretr k (f' (h (h^-1 b)))
@' (p (h^-1 b))^
@' p (h^-1 b)
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k (ap (funx : B' => k^-1 (g' x)) (eisretr h b)^)
@' eisretr k (g' (h (h^-1 b)))
@' (q (h^-1 b))^
@' q (h^-1 b)
@' ap g' (eisretr h b) = eisretr k (g' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k (ap (funx : B' => k^-1 (f' x)) (eisretr h b)^)
@' eisretr k (f' (h (h^-1 b)))
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap k (ap (funx : B' => k^-1 (g' x)) (eisretr h b)^)
@' eisretr k (g' (h (h^-1 b)))
@' ap g' (eisretr h b) = eisretr k (g' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap (funx : B' => k (k^-1 (f' x))) (eisretr h b)^
@' eisretr k (f' (h (h^-1 b)))
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap (funx : B' => k (k^-1 (g' x))) (eisretr h b)^
@' eisretr k (g' (h (h^-1 b)))
@' ap g' (eisretr h b) = eisretr k (g' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap (funx : A' => k (k^-1 x)) (ap f' (eisretr h b)^)
@' eisretr k (f' (h (h^-1 b)))
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
ap (funx : A' => k (k^-1 x)) (ap g' (eisretr h b)^)
@' eisretr k (g' (h (h^-1 b)))
@' ap g' (eisretr h b) = eisretr k (g' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
eisretr k (f' b)
@' ap f' (eisretr h b)^
@' ap f' (eisretr h b) = eisretr k (f' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B'
eisretr k (g' b)
@' ap g' (eisretr h b)^
@' ap g' (eisretr h b) = eisretr k (g' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
functor_coeq_inverse o functor_coeq h k p q == idmap
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
functor_coeq_inverse o functor_coeq h k p q == idmap
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h
functor_coeq_inverse o functor_coeq h k p q == idmap
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1 (p b)
@' (ap (funx : B' => k^-1 (f' x)) (eisretr h (h b))^
@' ap k^-1 (p (h^-1 (h b)))^
@' eissect k (f (h^-1 (h b))))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1 (q b)
@' (ap (funx : B' => k^-1 (g' x)) (eisretr h (h b))^
@' ap k^-1 (q (h^-1 (h b)))^
@' eissect k (g (h^-1 (h b))))
@' ap g (eissect h b) = eissect k (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1 (p b)
@' ap (funx : B => k^-1 (f' (h x))) (eissect h b)^
@' ap k^-1 (p (h^-1 (h b)))^
@' eissect k (f (h^-1 (h b)))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1 (q b)
@' ap (funx : B => k^-1 (g' (h x))) (eissect h b)^
@' ap k^-1 (q (h^-1 (h b)))^
@' eissect k (g (h^-1 (h b)))
@' ap g (eissect h b) = eissect k (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1 (p b)
@' ap k^-1 (ap (funx : B => f' (h x)) (eissect h b)^)
@' ap k^-1 (p (h^-1 (h b)))^
@' eissect k (f (h^-1 (h b)))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1 (q b)
@' ap k^-1 (ap (funx : B => g' (h x)) (eissect h b)^)
@' ap k^-1 (q (h^-1 (h b)))^
@' eissect k (g (h^-1 (h b)))
@' ap g (eissect h b) = eissect k (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1
(p b
@' (ap (funx : B => f' (h x)) (eissect h b)^
@' (p (h^-1 (h b)))^))
@' (eissect k (f (h^-1 (h b)))
@' ap f (eissect h b)) = eissect k (f b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1
(q b
@' (ap (funx : B => g' (h x)) (eissect h b)^
@' (q (h^-1 (h b)))^))
@' (eissect k (g (h^-1 (h b)))
@' ap g (eissect h b)) = eissect k (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1
(p b
@' ((p b)^
@' ap (funb : B => k (f b)) (eissect h b)^))
@' (eissect k (f (h^-1 (h b)))
@' ap f (eissect h b)) = eissect k (f b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1
(q b
@' (ap (funx : B => g' (h x)) (eissect h b)^
@' (q (h^-1 (h b)))^))
@' (eissect k (g (h^-1 (h b)))
@' ap g (eissect h b)) = eissect k (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1
(p b
@' ((p b)^
@' ap (funb : B => k (f b)) (eissect h b)^))
@' (eissect k (f (h^-1 (h b)))
@' ap f (eissect h b)) = eissect k (f b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1
(q b
@' ((q b)^
@' ap (funb : B => k (g b)) (eissect h b)^))
@' (eissect k (g (h^-1 (h b)))
@' ap g (eissect h b)) = eissect k (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1 (ap (funb : B => k (f b)) (eissect h b)^)
@' eissect k (f (h^-1 (h b)))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap k^-1 (ap (funb : B => k (g b)) (eissect h b)^)
@' eissect k (g (h^-1 (h b)))
@' ap g (eissect h b) = eissect k (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap (funx : A => k^-1 (k x)) (ap f (eissect h b)^)
@' eissect k (f (h^-1 (h b)))
@' ap f (eissect h b) = eissect k (f b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
ap (funx : A => k^-1 (k x)) (ap g (eissect h b)^)
@' eissect k (g (h^-1 (h b)))
@' ap g (eissect h b) = eissect k (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
eissect k (f b)
@' ap f (eissect h b)^
@' ap f (eissect h b) = eissect k (f b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' h: B -> B' k: A -> A' H: IsEquiv h H0: IsEquiv k p: k o f == f' o h q: k o g == g' o h b: B
eissect k (g b)
@' ap g (eissect h b)^
@' ap g (eissect h b) = eissect k (g b)
all:rewrite ap_V, concat_pV_p; reflexivity.Close Scope long_path_scope.Qed.Global Instanceisequiv_functor_coeq
: IsEquiv (functor_coeq h k p q)
:= isequiv_adjointify _ functor_coeq_inverse
functor_coeq_eissect functor_coeq_eisretr.Definitionequiv_functor_coeq
: @Coeq B A f g <~> @Coeq B' A' f' g'
:= Build_Equiv _ _ (functor_coeq h k p q) _.EndIsEquivFunctorCoeq.Definitionequiv_functor_coeq' {BAfgB'A'f'g'}
(h : B <~> B') (k : A <~> A')
(p : k o f == f' o h) (q : k o g == g' o h)
: @Coeq B A f g <~> @Coeq B' A' f' g'
:= equiv_functor_coeq h k p q.(** ** A double recursion principle *)SectionCoeqRec2.Context {BA : Type} {fg : B -> A} {B'A' : Type} {f'g' : B' -> A'}
(P : Type) (coeq' : A -> A' -> P)
(cgluel : forallba', coeq' (f b) a' = coeq' (g b) a')
(cgluer : forallab', coeq' a (f' b') = coeq' a (g' b'))
(cgluelr : forallbb', cgluel b (f' b') @ cgluer (g b) b'
= cgluer (f b) b' @ cgluel b (g' b')).
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
Coeq f g -> Coeq f' g' -> P
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
Coeq f g -> Coeq f' g' -> P
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') y: Coeq f' g'
Coeq f g -> P
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') y: Coeq f' g'
A -> P
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') y: Coeq f' g'
forallb : B, ?coeq' (f b) = ?coeq' (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') y: Coeq f' g'
A -> P
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') y: Coeq f' g' a: A
P
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') a: A
Coeq f' g' -> P
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') a: A
A' -> P
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') a: A
forallb : B', ?coeq' (f' b) = ?coeq' (g' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') a: A
A' -> P
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') a: A a': A'
P
exact (coeq' a a').
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') a: A
forallb : B',
(funa' : A' => coeq' a a') (f' b) =
(funa' : A' => coeq' a a') (g' b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') a: A b': B'
coeq' a (f' b') = coeq' a (g' b')
apply cgluer.
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') y: Coeq f' g'
forallb : B,
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) y) (f b) =
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) y) (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') y: Coeq f' g' b: B
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) y) (f b) =
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) y) (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B
forally : Coeq f' g',
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) y) (f b) =
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) y) (g b)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B
foralla : A',
(funw : Coeq f' g' =>
(funa0 : A =>
Coeq_rec P (funa' : A' => coeq' a0 a')
(funb' : B' =>
cgluer a0 b'
:
(funa' : A' => coeq' a0 a') (f' b') =
(funa' : A' => coeq' a0 a') (g' b')) w) (f b) =
(funa0 : A =>
Coeq_rec P (funa' : A' => coeq' a0 a')
(funb' : B' =>
cgluer a0 b'
:
(funa' : A' => coeq' a0 a') (f' b') =
(funa' : A' => coeq' a0 a') (g' b')) w) (g b))
(coeq a)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B
forallb0 : B',
transport
(funw : Coeq f' g' =>
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) w)
(f b) =
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) w)
(g b)) (cglue b0) (?coeq' (f' b0)) =
?coeq' (g' b0)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B
foralla : A',
(funw : Coeq f' g' =>
(funa0 : A =>
Coeq_rec P (funa' : A' => coeq' a0 a')
(funb' : B' =>
cgluer a0 b'
:
(funa' : A' => coeq' a0 a') (f' b') =
(funa' : A' => coeq' a0 a') (g' b')) w) (f b) =
(funa0 : A =>
Coeq_rec P (funa' : A' => coeq' a0 a')
(funb' : B' =>
cgluer a0 b'
:
(funa' : A' => coeq' a0 a') (f' b') =
(funa' : A' => coeq' a0 a') (g' b')) w) (g b))
(coeq a)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B a': A'
(funw : Coeq f' g' =>
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) w) (f b) =
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) w) (g b))
(coeq a')
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B a': A'
Coeq_rec P (funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b') (coeq a') =
Coeq_rec P (funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') (coeq a')
apply cgluel.
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B
forallb0 : B',
transport
(funw : Coeq f' g' =>
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) w) (f b) =
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) w) (g b))
(cglue b0)
((funa' : A' =>
cgluel b a'
:
(funw : Coeq f' g' =>
(funa : A =>
Coeq_rec P (funa'0 : A' => coeq' a a'0)
(funb' : B' =>
cgluer a b'
:
(funa'0 : A' => coeq' a a'0) (f' b') =
(funa'0 : A' => coeq' a a'0) (g' b')) w)
(f b) =
(funa : A =>
Coeq_rec P (funa'0 : A' => coeq' a a'0)
(funb' : B' =>
cgluer a b'
:
(funa'0 : A' => coeq' a a'0) (f' b') =
(funa'0 : A' => coeq' a a'0) (g' b')) w)
(g b)) (coeq a')) (f' b0)) =
(funa' : A' =>
cgluel b a'
:
(funw : Coeq f' g' =>
(funa : A =>
Coeq_rec P (funa'0 : A' => coeq' a a'0)
(funb' : B' =>
cgluer a b'
:
(funa'0 : A' => coeq' a a'0) (f' b') =
(funa'0 : A' => coeq' a a'0) (g' b')) w) (f b) =
(funa : A =>
Coeq_rec P (funa'0 : A' => coeq' a a'0)
(funb' : B' =>
cgluer a b'
:
(funa'0 : A' => coeq' a a'0) (f' b') =
(funa'0 : A' => coeq' a a'0) (g' b')) w) (g b))
(coeq a')) (g' b0)
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B b': B'
transport
(funw : Coeq f' g' =>
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) w) (f b) =
(funa : A =>
Coeq_rec P (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
(funa' : A' => coeq' a a') (f' b') =
(funa' : A' => coeq' a a') (g' b')) w) (g b))
(cglue b')
((funa' : A' =>
cgluel b a'
:
(funw : Coeq f' g' =>
(funa : A =>
Coeq_rec P (funa'0 : A' => coeq' a a'0)
(funb' : B' =>
cgluer a b'
:
(funa'0 : A' => coeq' a a'0) (f' b') =
(funa'0 : A' => coeq' a a'0) (g' b')) w)
(f b) =
(funa : A =>
Coeq_rec P (funa'0 : A' => coeq' a a'0)
(funb' : B' =>
cgluer a b'
:
(funa'0 : A' => coeq' a a'0) (f' b') =
(funa'0 : A' => coeq' a a'0) (g' b')) w)
(g b)) (coeq a')) (f' b')) =
(funa' : A' =>
cgluel b a'
:
(funw : Coeq f' g' =>
(funa : A =>
Coeq_rec P (funa'0 : A' => coeq' a a'0)
(funb' : B' =>
cgluer a b'
:
(funa'0 : A' => coeq' a a'0) (f' b') =
(funa'0 : A' => coeq' a a'0) (g' b')) w) (f b) =
(funa : A =>
Coeq_rec P (funa'0 : A' => coeq' a a'0)
(funb' : B' =>
cgluer a b'
:
(funa'0 : A' => coeq' a a'0) (f' b') =
(funa'0 : A' => coeq' a a'0) (g' b')) w) (g b))
(coeq a')) (g' b')
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B b': B'
ap
(Coeq_rec P (funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) (cglue b') @
cgluel b (g' b') =
cgluel b (f' b') @
ap
(Coeq_rec P (funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b')) (cglue b')
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B b': B'
ap
(Coeq_rec P (funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) (cglue b') =
?Goal
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B b': B'
?Goal @ cgluel b (g' b') =
cgluel b (f' b') @
ap
(Coeq_rec P (funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b'))
(cglue b')
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B b': B'
cgluer (f b) b' @ cgluel b (g' b') =
cgluel b (f' b') @
ap
(Coeq_rec P (funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b')) (cglue b')
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B b': B'
cgluer (f b) b' @ cgluel b (g' b') =
cgluel b (f' b') @ ?Goal
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B b': B'
ap
(Coeq_rec P (funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b'))
(cglue b') = ?Goal
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B b': B'
cgluer (f b) b' @ cgluel b (g' b') =
cgluel b (f' b') @ cgluer (g b) b'
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B b': B'
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b')
apply cgluelr.Defined.DefinitionCoeq_rec2_beta (a : A) (a' : A')
: Coeq_rec2 (coeq a) (coeq a') = coeq' a a'
:= 1.
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') a: A b': B'
ap (Coeq_rec2 (coeq a)) (cglue b') = cgluer a b'
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') a: A b': B'
ap (Coeq_rec2 (coeq a)) (cglue b') = cgluer a b'
nrapply Coeq_rec_beta_cglue.Defined.
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B a': A'
ap (funx : Coeq f g => Coeq_rec2 x (coeq a'))
(cglue b) = cgluel b a'
B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Type coeq': A -> A' -> P cgluel: forall (b : B) (a' : A'),
coeq' (f b) a' = coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
coeq' a (f' b') = coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
cgluel b (f' b') @ cgluer (g b) b' =
cgluer (f b) b' @ cgluel b (g' b') b: B a': A'
ap (funx : Coeq f g => Coeq_rec2 x (coeq a'))
(cglue b) = cgluel b a'
nrapply Coeq_rec_beta_cglue.Defined.(** TODO: [Coeq_rec2_beta_cgluelr] *)EndCoeqRec2.(** ** A double induction principle *)SectionCoeqInd2.Context `{Funext}
{B A : Type} {f g : B -> A} {B' A' : Type} {f' g' : B' -> A'}
(P : Coeq f g -> Coeq f' g' -> Type)
(coeq' : forallaa', P (coeq a) (coeq a'))
(cgluel : forallba',
transport (funx => P x (coeq a')) (cglue b)
(coeq' (f b) a') = coeq' (g b) a')
(cgluer : forallab',
transport (funy => P (coeq a) y) (cglue b')
(coeq' a (f' b')) = coeq' a (g' b'))
(** Perhaps this should really be written using [concatD]. *)
(cgluelr : forallbb',
ap (transport (P (coeq (g b))) (cglue b')) (cgluel b (f' b'))
@ cgluer (g b) b'
= transport_transport P (cglue b) (cglue b') (coeq' (f b) (f' b'))
@ ap (transport (funx => P x (coeq (g' b'))) (cglue b))
(cgluer (f b) b')
@ cgluel b (g' b')).
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forall (x : Coeq f g) (y : Coeq f' g'), P x y
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forall (x : Coeq f g) (y : Coeq f' g'), P x y
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
foralla : A,
(funw : Coeq f g => forally : Coeq f' g', P w y)
(coeq a)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forallb : B,
transport
(funw : Coeq f g => forally : Coeq f' g', P w y)
(cglue b) (?coeq' (f b)) =
?coeq' (g b)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
foralla : A,
(funw : Coeq f g => forally : Coeq f' g', P w y)
(coeq a)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') a: A
(funw : Coeq f g => forally : Coeq f' g', P w y)
(coeq a)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') a: A
foralla0 : A', P (coeq a) (coeq a0)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') a: A
forallb : B',
transport (P (coeq a)) (cglue b) (?coeq' (f' b)) =
?coeq' (g' b)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') a: A
foralla0 : A', P (coeq a) (coeq a0)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') a: A a': A'
P (coeq a) (coeq a')
exact (coeq' a a').
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') a: A
forallb : B',
transport (P (coeq a)) (cglue b)
((funa' : A' => coeq' a a') (f' b)) =
(funa' : A' => coeq' a a') (g' b)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') a: A b': B'
transport (P (coeq a)) (cglue b') (coeq' a (f' b')) =
coeq' a (g' b')
apply cgluer.
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b')
forallb : B,
transport
(funw : Coeq f g => forally : Coeq f' g', P w y)
(cglue b)
((funa : A =>
Coeq_ind (P (coeq a)) (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
transport (P (coeq a)) (cglue b')
((funa' : A' => coeq' a a') (f' b')) =
(funa' : A' => coeq' a a') (g' b'))) (f b)) =
(funa : A =>
Coeq_ind (P (coeq a)) (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
transport (P (coeq a)) (cglue b')
((funa' : A' => coeq' a a') (f' b')) =
(funa' : A' => coeq' a a') (g' b'))) (g b)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B
transport
(funw : Coeq f g => forally : Coeq f' g', P w y)
(cglue b)
((funa : A =>
Coeq_ind (P (coeq a)) (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
transport (P (coeq a)) (cglue b')
((funa' : A' => coeq' a a') (f' b')) =
(funa' : A' => coeq' a a') (g' b'))) (f b)) =
(funa : A =>
Coeq_ind (P (coeq a)) (funa' : A' => coeq' a a')
(funb' : B' =>
cgluer a b'
:
transport (P (coeq a)) (cglue b')
((funa' : A' => coeq' a a') (f' b')) =
(funa' : A' => coeq' a a') (g' b'))) (g b)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B a: Coeq f' g'
transport
(funw : Coeq f g => forally : Coeq f' g', P w y)
(cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) a =
Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') a
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B
foralla : A',
(funw : Coeq f' g' =>
transport
(funw0 : Coeq f g => forally : Coeq f' g', P w0 y)
(cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) w =
Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') w) (coeq a)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B
forallb0 : B',
transport
(funw : Coeq f' g' =>
transport
(funw0 : Coeq f g =>
forally : Coeq f' g', P w0 y)
(cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) w =
Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') w)
(cglue b0) (?coeq' (f' b0)) =
?coeq' (g' b0)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B
foralla : A',
(funw : Coeq f' g' =>
transport
(funw0 : Coeq f g => forally : Coeq f' g', P w0 y)
(cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) w =
Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') w) (coeq a)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B a': A'
(funw : Coeq f' g' =>
transport
(funw0 : Coeq f g => forally : Coeq f' g', P w0 y)
(cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) w =
Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') w) (coeq a')
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B a': A'
transport
(funw : Coeq f g => forally : Coeq f' g', P w y)
(cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) (coeq a') =
Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') (coeq a')
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B a': A'
transport (funx : Coeq f g => P x (coeq a'))
(cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b') (coeq a')) =
Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') (coeq a')
apply cgluel.
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B
forallb0 : B',
transport
(funw : Coeq f' g' =>
transport
(funw0 : Coeq f g =>
forally : Coeq f' g', P w0 y) (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) w =
Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') w) (cglue b0)
((funa' : A' =>
transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa'0 : A' => coeq' (f b) a'0)
(funb' : B' => cgluer (f b) b')) (coeq a') @
cgluel b a'
:
(funw : Coeq f' g' =>
transport
(funw0 : Coeq f g =>
forally : Coeq f' g', P w0 y) (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa'0 : A' => coeq' (f b) a'0)
(funb' : B' => cgluer (f b) b')) w =
Coeq_ind (P (coeq (g b)))
(funa'0 : A' => coeq' (g b) a'0)
(funb' : B' => cgluer (g b) b') w) (coeq a'))
(f' b0)) =
(funa' : A' =>
transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa'0 : A' => coeq' (f b) a'0)
(funb' : B' => cgluer (f b) b')) (coeq a') @
cgluel b a'
:
(funw : Coeq f' g' =>
transport
(funw0 : Coeq f g =>
forally : Coeq f' g', P w0 y) (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa'0 : A' => coeq' (f b) a'0)
(funb' : B' => cgluer (f b) b')) w =
Coeq_ind (P (coeq (g b)))
(funa'0 : A' => coeq' (g b) a'0)
(funb' : B' => cgluer (g b) b') w) (coeq a'))
(g' b0)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B b': B'
transport
(funw : Coeq f' g' =>
transport
(funw0 : Coeq f g =>
forally : Coeq f' g', P w0 y) (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) w =
Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b') w) (cglue b')
(transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b'))
(coeq (f' b')) @ cgluel b (f' b')) =
transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) (coeq (g' b')) @
cgluel b (g' b')
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B b': B'
((apD
(transport
(funw : Coeq f g =>
forally : Coeq f' g', P w y) (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')))
(cglue b'))^ @
ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b'))
(coeq (f' b')) @ cgluel b (f' b'))) @
apD
(Coeq_ind (P (coeq (g b)))
(funa' : A' => coeq' (g b) a')
(funb' : B' => cgluer (g b) b')) (cglue b') =
transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) (coeq (g' b')) @
cgluel b (g' b')
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')) @ cgluer (g b) b' =
(transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b')) @
ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')) @
cgluel b (g' b') b: B b': B'
((apD
(transport
(funw : Coeq f g =>
forally : Coeq f' g', P w y) (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')))
(cglue b'))^ @
ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b'))
(coeq (f' b')) @ cgluel b (f' b'))) @
cgluer (g b) b' =
transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) (coeq (g' b')) @
cgluel b (g' b')
(** Now begins the long haul. *)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B'
(apD
(transport
(funw : Coeq f g =>
forally : Coeq f' g', P w y) (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b'))) (cglue b'))^
@' ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b'))
(coeq (f' b'))
@' cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) (coeq (g' b'))
@' cgluel b (g' b')
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B'
(apD
(transport
(funw : Coeq f g =>
forally : Coeq f' g', P w y) (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b'))) (cglue b'))^
@' (ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b'))
(coeq (f' b')))
@' ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b')))
@' cgluer (g b) b' =
transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) (coeq (g' b'))
@' cgluel b (g' b')
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B'
(apD
(transport
(funw : Coeq f g =>
forally : Coeq f' g', P w y) (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b'))) (cglue b'))^
@' ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b'))
(coeq (f' b')))
@' ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b)
(Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb' : B' => cgluer (f b) b')) (coeq (g' b'))
@' cgluel b (g' b')
(** Our first order of business is to get rid of the [Coeq_ind]s, which only occur in the following incarnation. *)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B' G:= Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb'0 : B' => cgluer (f b) b'0): forallw : Coeq f' g', P (coeq (f b)) w
(apD
(transport
(funw : Coeq f g =>
forally : Coeq f' g', P w y) (cglue b) G)
(cglue b'))^
@' ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b) G
(coeq (f' b')))
@' ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b) G (coeq (g' b'))
@' cgluel b (g' b')
(** Let's reduce the [apD (loop # G)] first. *)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B' G:= Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb'0 : B' => cgluer (f b) b'0): forallw : Coeq f' g', P (coeq (f b)) w
(ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b) G
(coeq (f' b')))
@' transport_transport P (cglue b) (cglue b')
(coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g => P x (coeq (g' b')))
(cglue b)) (apD G (cglue b'))
@' (transport_forall_constant (cglue b) G
(coeq (g' b')))^)^
@' ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b) G
(coeq (f' b')))
@' ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b) G (coeq (g' b'))
@' cgluel b (g' b')
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B' G:= Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb'0 : B' => cgluer (f b) b'0): forallw : Coeq f' g', P (coeq (f b)) w
transport_forall_constant (cglue b) G (coeq (g' b'))
@' ((ap
(transport
(funx : Coeq f g => P x (coeq (g' b')))
(cglue b)) (apD G (cglue b')))^
@' ((transport_transport P (cglue b) (cglue b')
(coeq' (f b) (f' b')))^
@' (ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b) G
(coeq (f' b'))))^))
@' ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b) G
(coeq (f' b')))
@' ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_forall_constant (cglue b) G (coeq (g' b'))
@' cgluel b (g' b')
(** Now we can cancel a [transport_forall_constant]. *)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B' G:= Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb'0 : B' => cgluer (f b) b'0): forallw : Coeq f' g', P (coeq (f b)) w
(ap
(transport (funx : Coeq f g => P x (coeq (g' b')))
(cglue b)) (apD G (cglue b')))^
@' ((transport_transport P (cglue b) (cglue b')
(coeq' (f b) (f' b')))^
@' ((ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b) G
(coeq (f' b'))))^
@' (ap (transport (P (coeq (g b))) (cglue b'))
(transport_forall_constant (cglue b) G
(coeq (f' b')))
@' (ap
(transport (P (coeq (g b)))
(cglue b')) (cgluel b (f' b'))
@' cgluer (g b) b')))) =
cgluel b (g' b')
(** And a path-inverse pair. This removes all the [transport_forall_constant]s. *)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B' G:= Coeq_ind (P (coeq (f b)))
(funa' : A' => coeq' (f b) a')
(funb'0 : B' => cgluer (f b) b'0): forallw : Coeq f' g', P (coeq (f b)) w
(ap
(transport (funx : Coeq f g => P x (coeq (g' b')))
(cglue b)) (apD G (cglue b')))^
@' (transport_transport P (cglue b) (cglue b')
(coeq' (f b) (f' b')))^
@' ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' = cgluel b (g' b')
(** Now we can beta-reduce the last remaining [G]. *)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B'
(ap
(transport (funx : Coeq f g => P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b'))^
@' (transport_transport P (cglue b) (cglue b')
(coeq' (f b) (f' b')))^
@' ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' = cgluel b (g' b')
(** Now we just have to rearrange it a bit. *)
H: Funext B, A: Type f, g: B -> A B', A': Type f', g': B' -> A' P: Coeq f g -> Coeq f' g' -> Type coeq': forall (a : A) (a' : A'), P (coeq a) (coeq a') cgluel: forall (b : B) (a' : A'),
transport (funx : Coeq f g => P x (coeq a'))
(cglue b) (coeq' (f b) a') =
coeq' (g b) a' cgluer: forall (a : A) (b' : B'),
transport
(funy : Coeq f' g' => P (coeq a) y)
(cglue b') (coeq' a (f' b')) =
coeq' a (g' b') cgluelr: forall (b : B) (b' : B'),
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b)
(cglue b') (coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g =>
P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b') b: B b': B'
ap (transport (P (coeq (g b))) (cglue b'))
(cgluel b (f' b'))
@' cgluer (g b) b' =
transport_transport P (cglue b) (cglue b')
(coeq' (f b) (f' b'))
@' ap
(transport
(funx : Coeq f g => P x (coeq (g' b')))
(cglue b)) (cgluer (f b) b')
@' cgluel b (g' b')
apply cgluelr.Close Scope long_path_scope.Qed.EndCoeqInd2.(** ** Symmetry *)DefinitionCoeq_sym_map {BA} (fg : B -> A) : Coeq f g -> Coeq g f :=
Coeq_rec (Coeq g f) coeq (funb : B => (cglue b)^).
B, A: Type f, g: B -> A
Coeq_sym_map f g o Coeq_sym_map g f == idmap
B, A: Type f, g: B -> A
Coeq_sym_map f g o Coeq_sym_map g f == idmap
B, A: Type f, g: B -> A
foralla : A,
(funw : Coeq g f =>
(Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
(coeq a)
B, A: Type f, g: B -> A
forallb : B,
transport
(funw : Coeq g f =>
(Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
(cglue b) (?coeq' (g b)) = ?coeq' (f b)
B, A: Type f, g: B -> A
foralla : A,
(funw : Coeq g f =>
(Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
(coeq a)
reflexivity.
B, A: Type f, g: B -> A
forallb : B,
transport
(funw : Coeq g f =>
(Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
(cglue b) ((funa : A => 1) (g b)) =
(funa : A => 1) (f b)
B, A: Type f, g: B -> A b: B
transport
(funw : Coeq g f =>
(Coeq_sym_map f g o Coeq_sym_map g f) w = idmap w)
(cglue b) ((funa : A => 1) (g b)) =
(funa : A => 1) (f b)
B, A: Type f, g: B -> A b: B
transport
(funw : Coeq g f =>
Coeq_sym_map f g (Coeq_sym_map g f w) = w)
(cglue b) 1 = 1
exact (equiv_adjointify (Coeq_sym_map f g) (Coeq_sym_map g f) sect_Coeq_sym_map sect_Coeq_sym_map).Defined.(** ** Flattening *)(** The flattening lemma for coequalizers follows from the flattening lemma for graph quotients. *)SectionFlattening.Context `{Univalence} {B A : Type} {f g : B -> A}
(F : A -> Type) (e : forallb, F (f b) <~> F (g b)).Definitioncoeq_flatten_fam : Coeq f g -> Type
:= Coeq_rec Type F (funx => path_universe (e x)).Local DefinitionR (ab : A) := {x : B & (f x = a) * (g x = b)}.
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a, b: A
R a b -> F a <~> F b
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a, b: A
R a b -> F a <~> F b
intros [x [[] []]]; exact (e x).Defined.
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
{x : _ & coeq_flatten_fam x} <~>
Coeq (functor_sigma f (funa : B => idmap))
(functor_sigma g (funb : B => e b))
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
{x : _ & coeq_flatten_fam x} <~>
Coeq (functor_sigma f (funa : B => idmap))
(functor_sigma g (funb : B => e b))
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
GraphQuotient
(funab : {x : _ & F x} =>
{r : R a.1 b.1 & e' a.1 b.1 r a.2 = b.2}) <~>
Coeq (functor_sigma f (funa : B => idmap))
(functor_sigma g (funb : B => e b))
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
{x : _ & coeq_flatten_fam x} <~>
{x : _ & DGraphQuotient F e' x}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
GraphQuotient
(funab : {x : _ & F x} =>
{r : R a.1 b.1 & e' a.1 b.1 r a.2 = b.2}) <~>
Coeq (functor_sigma f (funa : B => idmap))
(functor_sigma g (funb : B => e b))
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
{x : _ & F x} <~> {x : _ & F x}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
forallab : {x : _ & F x},
(funa0b0 : {x : _ & F x} =>
{r : R a0.1 b0.1 & e' a0.1 b0.1 r a0.2 = b0.2}) a b <~>
(funa0b0 : {x : _ & F x} =>
{x : {H : B & F (f H)} &
(functor_sigma f (funa1 : B => idmap) x = a0) *
(functor_sigma g (funb1 : B => e b1) x = b0)})
(?f0 a) (?f0 b)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
forallab : {x : _ & F x},
(funa0b0 : {x : _ & F x} =>
{r : R a0.1 b0.1 & e' a0.1 b0.1 r a0.2 = b0.2}) a b <~>
(funa0b0 : {x : _ & F x} =>
{x : {H : B & F (f H)} &
(functor_sigma f (funa1 : B => idmap) x = a0) *
(functor_sigma g (funb1 : B => e b1) x = b0)})
(1%equiv a) (1%equiv b)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b
{r : R a b & e' a b r x = y} <~>
{x0 : {H : B & F (f H)} &
(functor_sigma f (funa : B => idmap) x0 = (a; x)) *
(functor_sigma g (funb : B => e b) x0 = (b; y))}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b
{r : R a b & e' a b r x = y} <~>
{x0 : {H : B & F (f H)} &
((f x0.1; x0.2) = (a; x)) *
((g x0.1; e x0.1 x0.2) = (b; y))}
(* We use [equiv_path_sigma] twice on the RHS: *)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b
{r : R a b & e' a b r x = y} <~>
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}} <~>
{x0 : {H : B & F (f H)} &
((f x0.1; x0.2) = (a; x)) *
((g x0.1; e x0.1 x0.2) = (b; y))}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}} <~>
{x0 : {H : B & F (f H)} &
((f x0.1; x0.2) = (a; x)) *
((g x0.1; e x0.1 x0.2) = (b; y))}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b c: B z: F (f c)
{p : f c = a & transport F p z = x} *
{q : g c = b & transport F q (e c z) = y} <~>
((f c; z) = (a; x)) * ((g c; e c z) = (b; y))
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b c: B z: F (f c)
{p : f c = a & transport F p z = x} <~>
(f c; z) = (a; x)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b c: B z: F (f c)
{q : g c = b & transport F q (e c z) = y} <~>
(g c; e c z) = (b; y)
all: apply (equiv_path_sigma _ (_; _) (_; _)).
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b
{r : R a b & e' a b r x = y} <~>
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}}
(* [make_equiv_contr_basedpaths.] handles the rest, but is slow, so we do some steps manually. *)(* The RHS can be shuffled to this form: *)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b
{r : R a b & e' a b r x = y} <~>
{r : R a b &
{x02 : F (f r.1) &
(transport F (fst r.2) x02 = x) *
(transport F (snd r.2) (e r.1 x02) = y)}}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b
{r : R a b &
{x02 : F (f r.1) &
(transport F (fst r.2) x02 = x) *
(transport F (snd r.2) (e r.1 x02) = y)}} <~>
{x0 : {H0 : B & F (f H0)} &
{p : f x0.1 = a & transport F p x0.2 = x} *
{q : g x0.1 = b & transport F q (e x0.1 x0.2) = y}}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b
{r : R a b & e' a b r x = y} <~>
{r : R a b &
{x02 : F (f r.1) &
(transport F (fst r.2) x02 = x) *
(transport F (snd r.2) (e r.1 x02) = y)}}
(* Three path contractions handle the rest. *)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) a: A x: F a b: A y: F b c: B p: f c = a q: g c = b
e' a b (c; (p, q)) x = y <~>
{x02 : F (f (c; (p, q)).1) &
(transport F (fst (c; (p, q)).2) x02 = x) *
(transport F (snd (c; (p, q)).2) (e (c; (p, q)).1 x02) =
y)}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) c: B x: F (f c) y: F (g c)
e c x = y <~>
{x02 : F (f c) & (x02 = x) * (e c x02 = y)}
make_equiv_contr_basedpaths.
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
{x : _ & coeq_flatten_fam x} <~>
{x : _ & DGraphQuotient F e' x}
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) x: Coeq f g
coeq_flatten_fam x <~> DGraphQuotient F e' x
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) x: Coeq f g
coeq_flatten_fam x = DGraphQuotient F e' x
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
foralla : A,
(funw : Coeq f g =>
coeq_flatten_fam w = DGraphQuotient F e' w) (coeq a)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
forallb : B,
transport
(funw : Coeq f g =>
coeq_flatten_fam w = DGraphQuotient F e' w)
(cglue b) (?coeq' (f b)) = ?coeq' (g b)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
forallb : B,
transport
(funw : Coeq f g =>
coeq_flatten_fam w = DGraphQuotient F e' w)
(cglue b) ((funa : A => 1) (f b)) =
(funa : A => 1) (g b)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b)
forallb : B,
transport
(funw : Coeq f g =>
coeq_flatten_fam w = DGraphQuotient F e' w)
(cglue b) 1 = 1
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) b: B
transport
(funw : Coeq f g =>
coeq_flatten_fam w = DGraphQuotient F e' w)
(cglue b) 1 = 1
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) b: B
1 @ ap (DGraphQuotient F e') (cglue b) =
ap coeq_flatten_fam (cglue b) @ 1
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) b: B
ap (DGraphQuotient F e') (cglue b) =
ap coeq_flatten_fam (cglue b)
H: Univalence B, A: Type f, g: B -> A F: A -> Type e: forallb : B, F (f b) <~> F (g b) b: B
ap (DGraphQuotient F e') (cglue b) =
path_universe (e b)
exact (GraphQuotient_rec_beta_gqglue _
(funabs => path_universe (e' a b s)) _ _ _).Defined.EndFlattening.