GraphQuotient.v

Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Universe Types.Paths Types.Forall Types.Arrow Types.Sigma Cubical.DPath.
Require Import Homotopy.IdentitySystems.

(** * Quotient of a graph *)

(** ** Definition *)

(** The quotient of a graph is one of the simplest HITs that can be found in HoTT. It consists of a base type and a relation on it, and for every witness of a relation between two points of the type, a path.

We use graph quotients to build up all our other non-recursive HITs. Their simplicity means that we can easily prove results about them and generalise them to other HITs. *)

Local Unset Elimination Schemes.

Module Export GraphQuotient.
 Section GraphQuotient.Trying to mask the absolute name "GraphQuotient.GraphQuotient"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]

  Universes i j u.
  Constraint i <= u, j <= u.
  Context {A : Type@{i}}.

  Private Inductive GraphQuotient (R : A -> A -> Type@{j}) : Type@{u} :=
  | gq : A -> GraphQuotient R.

  Arguments gq {R} a.

  Context {R : A -> A -> Type@{j}}.

  Axiom gqglue : forall {a b : A},
    R a b -> paths (@gq R a) (gq b).

  Definition GraphQuotient_ind
    (P : GraphQuotient R -> Type@{k})
    (gq' : forall a, P (gq a))
    (gqglue' : forall a b (s : R a b), gqglue s # gq' a = gq' b)
    : forall x, P x := fun x =>
    match x with
    | gq a => fun _ => gq' a
    end gqglue'.
  (** Above we did a match with output type a function, and then outside of the match we provided the argument [gqglue'].  If we instead end with [| gq a => gq' a end.], the definition will not depend on [gqglue'], which would be incorrect.  This is the idiom referred to in ../../test/bugs/github1758.v and github1759.v. *)

  Axiom GraphQuotient_ind_beta_gqglue
  : forall (P : GraphQuotient R -> Type@{k})
    (gq' : forall a, P (gq a))
    (gqglue' : forall a b (s : R a b), gqglue s # gq' a = gq' b)
    (a b: A) (s : R a b),
    apD (GraphQuotient_ind P gq' gqglue') (gqglue s) = gqglue' a b s.

 End GraphQuotient.
End GraphQuotient.

Arguments gq {A R} a.

Definition GraphQuotient_rec {A R P} (c : A -> P) (g : forall a b, R a b -> c a = c b)
  : GraphQuotient R -> P.A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
GraphQuotient R -> P
Proof.A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
GraphQuotient R -> P
  srapply GraphQuotient_ind.A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
forall a : A, (fun _ : GraphQuotient R => P) (gq a)
A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
forall (a b : A) (s : R a b),
transport (fun _ : GraphQuotient R => P) (gqglue s)
  (?gq' a) = ?gq' b
  1: exact c.A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
forall (a b : A) (s : R a b),
transport (fun _ : GraphQuotient R => P) (gqglue s)
  (c a) = c b
  intros a b s.A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
a, b: A
s: R a b
transport (fun _ : GraphQuotient R => P) (gqglue s)
  (c a) = c b
  exact (transport_const _ _ @ g a b s).
Defined.

Definition GraphQuotient_rec_beta_gqglue {A R P}
  (c : A -> P) (g : forall a b, R a b -> c a = c b)
  (a b : A) (s : R a b)
  : ap (GraphQuotient_rec c g) (gqglue s) = g a b s.A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
a, b: A
s: R a b
ap (GraphQuotient_rec c g) (gqglue s) = g a b s
Proof.A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
a, b: A
s: R a b
ap (GraphQuotient_rec c g) (gqglue s) = g a b s
  unfold GraphQuotient_rec.A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
a, b: A
s: R a b
ap
  (GraphQuotient_ind (fun _ : GraphQuotient R => P) c
     (fun (a b : A) (s : R a b) =>
      transport_const (gqglue s) (c a) @ g a b s))
  (gqglue s) = g a b s
  refine (cancelL _ _ _ _ ).A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
a, b: A
s: R a b
?Goal0 @
ap
  (GraphQuotient_ind (fun _ : GraphQuotient R => P) c
     (fun (a b : A) (s : R a b) =>
      transport_const (gqglue s) (c a) @ g a b s))
  (gqglue s) = ?Goal0 @ g a b s
  refine ((apD_const _ _)^ @ _).A: Type
R: A -> A -> Type
P: Type
c: A -> P
g: forall a b : A, R a b -> c a = c b
a, b: A
s: R a b
apD
  (GraphQuotient_ind (fun _ : GraphQuotient R => P) c
     (fun (a b : A) (s : R a b) =>
      transport_const (gqglue s) (c a) @ g a b s))
  (gqglue s) =
transport_const (gqglue s)
  (GraphQuotient_ind (fun _ : GraphQuotient R => P) c
     (fun (a b : A) (s : R a b) =>
      transport_const (gqglue s) (c a) @ g a b s)
     (gq a)) @ g a b s
  rapply GraphQuotient_ind_beta_gqglue.
Defined.

(** ** Descent *)

(** We study "equifibrant" type families over a graph [A], with edges indexed by [R].  By univalence, the descent property tells us that these type families correspond to type families over the graph quotient, and we obtain an induction principle for such type families.  Dependent descent data over some particular descent data are "equifibrant" type families over this descent data.  The "equifibrancy" is only taken over the graph [A] and [R], but there is an extra level of dependency coming from the descent data.  In this case, we obtain an induction and recursion principle, but only with a computation rule for the recursion principle.

The theory of descent is interesting to consider in itself.  However, we will use it as a means to structure the code, and to obtain induction and recursion principles that are valuable in proving the flattening lemma, and characterizing path spaces.  Thus we will gloss over the bigger picture, and not consider equivalences of descent data, nor homotopies of their sections.  We will also not elaborate on uniqueness of the induced families.

It's possible to prove the results in the Descent, Flattening and Paths Sections without univalence, by replacing all equivalences with paths, but in practice these results will be used with equivalences as input, making the form below more convenient.  See https://github.com/HoTT/Coq-HoTT/pull/2147#issuecomment-2521570830 for further information. *)

Section Descent.

  Context `{Univalence}.

  (** Descent data over a graph [A] and [R] is an "equifibrant" or "cartesian" type family [gqd_fam : A -> Type].  If [a b : A] are related by [r : R a b], then the fibers [gqd_fam a] and [gqd_fam b] are equivalent, witnessed by [gqd_e]. *)
  Record gqDescent {A : Type} {R : A -> A -> Type} := {
    gqd_fam (a : A) : Type;
    gqd_e {a b : A} (r : R a b) : gqd_fam a <~> gqd_fam b
  }.

  Global Arguments gqDescent {A} R.

  (** Let [A] and [R] be a graph. *)
  Context {A : Type} {R : A -> A -> Type}.

  (** Descent data induces a type family over [GraphQuotient R]. *)
  Definition fam_gqdescent (Pe : gqDescent R)
    : GraphQuotient R -> Type.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
GraphQuotient R -> Type
  Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
GraphQuotient R -> Type
    snapply (GraphQuotient_rec (gqd_fam Pe)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall a b : A, R a b -> gqd_fam Pe a = gqd_fam Pe b
    intros a b r.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
gqd_fam Pe a = gqd_fam Pe b
    exact (path_universe_uncurried (gqd_e Pe r)).
  Defined.

  (** A type family over [GraphQuotient R] induces descent data. *)
  Definition gqdescent_fam (P : GraphQuotient R -> Type) : gqDescent R.H: Univalence
A: Type
R: A -> A -> Type
P: GraphQuotient R -> Type
gqDescent R
  Proof.H: Univalence
A: Type
R: A -> A -> Type
P: GraphQuotient R -> Type
gqDescent R
    snapply Build_gqDescent.H: Univalence
A: Type
R: A -> A -> Type
P: GraphQuotient R -> Type
A -> Type
H: Univalence
A: Type
R: A -> A -> Type
P: GraphQuotient R -> Type
forall a b : A, R a b -> ?gqd_fam a <~> ?gqd_fam b
    -H: Univalence
A: Type
R: A -> A -> Type
P: GraphQuotient R -> Type
A -> Type exact (P o gq).
    -H: Univalence
A: Type
R: A -> A -> Type
P: GraphQuotient R -> Type
forall a b : A, R a b -> (P o gq) a <~> (P o gq) b intros a b r.H: Univalence
A: Type
R: A -> A -> Type
P: GraphQuotient R -> Type
a, b: A
r: R a b
(P o gq) a <~> (P o gq) b
      exact (equiv_transport P (gqglue r)).
  Defined.

  (** Transporting over [fam_gqdescent] along [gqglue r] is given by [gqd_e]. *)
  Definition transport_fam_gqdescent_gqglue
    (Pe : gqDescent R) {a b : A} (r : R a b) (pa : gqd_fam Pe a)
    : transport (fam_gqdescent Pe) (gqglue r) pa = gqd_e Pe r pa.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
transport (fam_gqdescent Pe) (gqglue r) pa =
gqd_e Pe r pa
  Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
transport (fam_gqdescent Pe) (gqglue r) pa =
gqd_e Pe r pa
    napply transport_path_universe'.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
ap (fam_gqdescent Pe) (gqglue r) =
path_universe (gqd_e Pe r)
    napply GraphQuotient_rec_beta_gqglue.
  Defined.

  (** A section on the descent data is a fiberwise section that respects the equivalences. *)
  Record gqDescentSection {Pe : gqDescent R} := {
    gqds_sect (a : A) : gqd_fam Pe a;
    gqds_e {a b : A} (r : R a b)
      : gqd_e Pe r (gqds_sect a) = gqds_sect b
  }.

  Global Arguments gqDescentSection Pe : clear implicits.

  (** A descent section induces a genuine section of [fam_gqdescent Pe]. *)
  Definition gqdescent_ind {Pe : gqDescent R}
    (f : gqDescentSection Pe)
    : forall (x : GraphQuotient R), fam_gqdescent Pe x.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
f: gqDescentSection Pe
forall x : GraphQuotient R, fam_gqdescent Pe x
  Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
f: gqDescentSection Pe
forall x : GraphQuotient R, fam_gqdescent Pe x
    snapply (GraphQuotient_ind _ (gqds_sect f)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
f: gqDescentSection Pe
forall (a b : A) (s : R a b),
transport (fam_gqdescent Pe) (gqglue s)
  (gqds_sect f a) = gqds_sect f b
    intros a b r.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
f: gqDescentSection Pe
a, b: A
r: R a b
transport (fam_gqdescent Pe) (gqglue r)
  (gqds_sect f a) = gqds_sect f b
    exact (transport_fam_gqdescent_gqglue Pe r _ @ gqds_e f r).
  Defined.

  (** We record its computation rule *)
  Definition gqdescent_ind_beta_gqglue {Pe : gqDescent R}
    (f : gqDescentSection Pe) {a b : A} (r : R a b)
    : apD (gqdescent_ind f) (gqglue r) = transport_fam_gqdescent_gqglue Pe r _ @ gqds_e f r
    := GraphQuotient_ind_beta_gqglue _ (gqds_sect f) _ _ _ _.

  (** Dependent descent data over descent data [Pe : gqDescent R] consists of a type family [gqdd_fam : forall (a : A), gqd_fam Pe a -> Type] together with coherences [gqdd_e r pa]. *)
  Record gqDepDescent {Pe : gqDescent R} := {
    gqdd_fam (a : A) (pa : gqd_fam Pe a) : Type;
    gqdd_e {a b : A} (r :  R a b) (pa : gqd_fam Pe a)
      : gqdd_fam a pa <~> gqdd_fam b (gqd_e Pe r pa)
  }.

  Global Arguments gqDepDescent Pe : clear implicits.

  (** A dependent type family over [fam_gqdescent Pe] induces dependent descent data over [Pe]. *)
  Definition gqdepdescent_fam {Pe : gqDescent R}
    (Q : forall (x : GraphQuotient R), (fam_gqdescent Pe) x -> Type)
    : gqDepDescent Pe.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
gqDepDescent Pe
  Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
gqDepDescent Pe
    snapply Build_gqDepDescent.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
forall a : A, gqd_fam Pe a -> Type
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
forall (a b : A) (r : R a b) (pa : gqd_fam Pe a),
?gqdd_fam a pa <~> ?gqdd_fam b (gqd_e Pe r pa)
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
forall a : A, gqd_fam Pe a -> Type intro a; cbn.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
a: A
gqd_fam Pe a -> Type
      exact (Q (gq a)).
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
forall (a b : A) (r : R a b) (pa : gqd_fam Pe a),
(fun a0 : A => Q (gq a0) : gqd_fam Pe a0 -> Type) a pa <~>
(fun a0 : A => Q (gq a0) : gqd_fam Pe a0 -> Type) b
  (gqd_e Pe r pa) intros a b r pa.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
a, b: A
r: R a b
pa: gqd_fam Pe a
(fun a : A => Q (gq a) : gqd_fam Pe a -> Type) a pa <~>
(fun a : A => Q (gq a) : gqd_fam Pe a -> Type) b
  (gqd_e Pe r pa)
      exact (equiv_transportDD (fam_gqdescent Pe) Q
               (gqglue r) (transport_fam_gqdescent_gqglue Pe r pa)).
  Defined.

  (** Dependent descent data over [Pe] induces a dependent type family over [fam_gqdescent Pe]. *)
  Definition fam_gqdepdescent {Pe : gqDescent R} (Qe : gqDepDescent Pe)
    : forall (x : GraphQuotient R), (fam_gqdescent Pe x) -> Type.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
forall x : GraphQuotient R, fam_gqdescent Pe x -> Type
  Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
forall x : GraphQuotient R, fam_gqdescent Pe x -> Type
    snapply GraphQuotient_ind.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
forall a : A,
(fun x : GraphQuotient R => fam_gqdescent Pe x -> Type)
  (gq a)
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R =>
   fam_gqdescent Pe x -> Type) (gqglue s) (?gq' a) =
?gq' b
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
forall a : A,
(fun x : GraphQuotient R => fam_gqdescent Pe x -> Type)
  (gq a) exact (gqdd_fam Qe).
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R =>
   fam_gqdescent Pe x -> Type) (gqglue s)
  (gqdd_fam Qe a) = gqdd_fam Qe b intros a b r.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
a, b: A
r: R a b
transport
  (fun x : GraphQuotient R =>
   fam_gqdescent Pe x -> Type) (gqglue r)
  (gqdd_fam Qe a) = gqdd_fam Qe b
      napply (moveR_transport_p _ (gqglue r)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
a, b: A
r: R a b
gqdd_fam Qe a =
transport
  (fun x : GraphQuotient R =>
   fam_gqdescent Pe x -> Type) (gqglue r)^
  (gqdd_fam Qe b)
      funext pa.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
gqdd_fam Qe a pa =
transport
  (fun x : GraphQuotient R =>
   fam_gqdescent Pe x -> Type) (gqglue r)^
  (gqdd_fam Qe b) pa
      rhs napply transport_arrow_toconst.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
gqdd_fam Qe a pa =
gqdd_fam Qe b
  (transport (fam_gqdescent Pe) ((gqglue r)^)^ pa)
      rhs nrefine (ap (gqdd_fam Qe b) _).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
gqdd_fam Qe a pa = gqdd_fam Qe b ?Goal
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
transport (fam_gqdescent Pe) ((gqglue r)^)^ pa = ?Goal
      +H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
gqdd_fam Qe a pa = gqdd_fam Qe b ?Goal exact (path_universe (gqdd_e Qe r pa)).
      +H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
transport (fam_gqdescent Pe) ((gqglue r)^)^ pa =
gqd_e Pe r pa lhs napply (ap (fun x => (transport _ x _)) (inv_V (gqglue r))).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Qe: gqDepDescent Pe
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
transport (fam_gqdescent Pe) (gqglue r) pa =
gqd_e Pe r pa
        exact (transport_fam_gqdescent_gqglue _ _ _).
  Defined.

  (** A section of dependent descent data [Qe : gqDepDescent Pe] is a fiberwise section [gqdds_sect], together with coherences [gqdd_e]. *)
  Record gqDepDescentSection {Pe : gqDescent R} {Qe : gqDepDescent Pe} := {
    gqdds_sect (a : A) (pa : gqd_fam Pe a) : gqdd_fam Qe a pa;
    gqdds_e {a b : A} (r : R a b) (pa : gqd_fam Pe a)
      : gqdd_e Qe r pa (gqdds_sect a pa) = gqdds_sect b (gqd_e Pe r pa)
  }.

  Global Arguments gqDepDescentSection {Pe} Qe.

  (** A dependent descent section induces a genuine section over the total space of [fam_gqdescent Pe]. *)
  Definition gqdepdescent_ind {Pe : gqDescent R}
    {Q : forall (x : GraphQuotient R), (fam_gqdescent Pe) x -> Type}
    (f : gqDepDescentSection (gqdepdescent_fam Q))
    : forall (x : GraphQuotient R) (px : fam_gqdescent Pe x), Q x px.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
f: gqDepDescentSection (gqdepdescent_fam Q)
forall (x : GraphQuotient R)
(px : fam_gqdescent Pe x), Q x px
    Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
f: gqDepDescentSection (gqdepdescent_fam Q)
forall (x : GraphQuotient R)
(px : fam_gqdescent Pe x), Q x px
      napply (GraphQuotient_ind _ (gqdds_sect f) _).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
f: gqDepDescentSection (gqdepdescent_fam Q)
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R =>
   forall px : fam_gqdescent Pe x, Q x px) (gqglue s)
  (gqdds_sect f a) = gqdds_sect f b
      intros a b r.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
f: gqDepDescentSection (gqdepdescent_fam Q)
a, b: A
r: R a b
transport
  (fun x : GraphQuotient R =>
   forall px : fam_gqdescent Pe x, Q x px) (gqglue r)
  (gqdds_sect f a) = gqdds_sect f b
      apply dpath_forall.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
f: gqDepDescentSection (gqdepdescent_fam Q)
a, b: A
r: R a b
forall y1 : fam_gqdescent Pe (gq a),
transportD (fam_gqdescent Pe) Q (gqglue r) y1
  (gqdds_sect f a y1) =
gqdds_sect f b
  (transport (fam_gqdescent Pe) (gqglue r) y1)
      intro pa.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
f: gqDepDescentSection (gqdepdescent_fam Q)
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
transportD (fam_gqdescent Pe) Q (gqglue r) pa
  (gqdds_sect f a pa) =
gqdds_sect f b
  (transport (fam_gqdescent Pe) (gqglue r) pa)
      apply (equiv_inj (transport (Q (gq b)) (transport_fam_gqdescent_gqglue Pe r pa))).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
f: gqDepDescentSection (gqdepdescent_fam Q)
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
transport (Q (gq b))
  (transport_fam_gqdescent_gqglue Pe r pa)
  (transportD (fam_gqdescent Pe) Q (gqglue r) pa
     (gqdds_sect f a pa)) =
transport (Q (gq b))
  (transport_fam_gqdescent_gqglue Pe r pa)
  (gqdds_sect f b
     (transport (fam_gqdescent Pe) (gqglue r) pa))
      rhs exact (apD (gqdds_sect f b) (transport_fam_gqdescent_gqglue Pe r pa)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: forall x : GraphQuotient R,
fam_gqdescent Pe x -> Type
f: gqDepDescentSection (gqdepdescent_fam Q)
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
transport (Q (gq b))
  (transport_fam_gqdescent_gqglue Pe r pa)
  (transportD (fam_gqdescent Pe) Q (gqglue r) pa
     (gqdds_sect f a pa)) =
gqdds_sect f b (gqd_e Pe r pa)
      exact (gqdds_e f r pa).
    Defined.

  (** The data for a section into a constant type family. *)
  Record gqDepDescentConstSection {Pe : gqDescent R} {Q : Type} := {
    gqddcs_sect (a : A) (pa : gqd_fam Pe a) : Q;
    gqddcs_e {a b : A} (r : R a b) (pa : gqd_fam Pe a)
      : gqddcs_sect a pa = gqddcs_sect b (gqd_e Pe r pa)
  }.

  Global Arguments gqDepDescentConstSection Pe Q : clear implicits.

  (** The data for a section of a constant family induces a section over the total space of [fam_gqdescent Pe]. *)
  Definition gqdepdescent_rec {Pe : gqDescent R} {Q : Type}
    (f : gqDepDescentConstSection Pe Q)
    : forall (x : GraphQuotient R), fam_gqdescent Pe x -> Q.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
forall x : GraphQuotient R, fam_gqdescent Pe x -> Q
  Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
forall x : GraphQuotient R, fam_gqdescent Pe x -> Q
    snapply (GraphQuotient_ind _ (gqddcs_sect f)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R => fam_gqdescent Pe x -> Q)
  (gqglue s) (gqddcs_sect f a) = gqddcs_sect f b
    intros a b r.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
r: R a b
transport
  (fun x : GraphQuotient R => fam_gqdescent Pe x -> Q)
  (gqglue r) (gqddcs_sect f a) = gqddcs_sect f b
    napply dpath_arrow.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
r: R a b
forall y1 : fam_gqdescent Pe (gq a),
transport (fun _ : GraphQuotient R => Q) (gqglue r)
  (gqddcs_sect f a y1) =
gqddcs_sect f b
  (transport (fam_gqdescent Pe) (gqglue r) y1)
    intro pa.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
transport (fun _ : GraphQuotient R => Q) (gqglue r)
  (gqddcs_sect f a pa) =
gqddcs_sect f b
  (transport (fam_gqdescent Pe) (gqglue r) pa)
    lhs napply transport_const.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
gqddcs_sect f a pa =
gqddcs_sect f b
  (transport (fam_gqdescent Pe) (gqglue r) pa)
    rhs napply (ap _ (transport_fam_gqdescent_gqglue Pe r pa)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
r: R a b
pa: fam_gqdescent Pe (gq a)
gqddcs_sect f a pa = gqddcs_sect f b (gqd_e Pe r pa)
    exact (gqddcs_e f r pa).
  Defined.

  (** Here is the computation rule on paths. *)
  Definition gqdepdescent_rec_beta_gqglue {Pe : gqDescent R} {Q : Type}
    (f : gqDepDescentConstSection Pe Q)
    {a b : A} {pa : gqd_fam Pe a} {pb : gqd_fam Pe b} (r : R a b) (pr : gqd_e Pe r pa = pb)
    : ap (sig_rec (gqdepdescent_rec f)) (path_sigma _ (gq a; pa) (gq b; pb) (gqglue r) (transport_fam_gqdescent_gqglue Pe r pa @ pr))
      = gqddcs_e f r pa @ ap (gqddcs_sect f b) pr.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
pb: gqd_fam Pe b
r: R a b
pr: gqd_e Pe r pa = pb
ap (sig_rec (gqdepdescent_rec f))
  (path_sigma (fam_gqdescent Pe) (gq a; pa) (gq b; pb)
     (gqglue r)
     (transport_fam_gqdescent_gqglue Pe r pa @ pr)) =
gqddcs_e f r pa @ ap (gqddcs_sect f b) pr
  Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
pb: gqd_fam Pe b
r: R a b
pr: gqd_e Pe r pa = pb
ap (sig_rec (gqdepdescent_rec f))
  (path_sigma (fam_gqdescent Pe) (gq a; pa) (gq b; pb)
     (gqglue r)
     (transport_fam_gqdescent_gqglue Pe r pa @ pr)) =
gqddcs_e f r pa @ ap (gqddcs_sect f b) pr
    Open Scope long_path_scope.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
pb: gqd_fam Pe b
r: R a b
pr: gqd_e Pe r pa = pb
ap (sig_rec (gqdepdescent_rec f))
  (path_sigma (fam_gqdescent Pe) (gq a; pa) (gq b; pb)
     (gqglue r)
     (transport_fam_gqdescent_gqglue Pe r pa
      @' pr)) =
gqddcs_e f r pa
@' ap (gqddcs_sect f b) pr
    destruct pr.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
ap (sig_rec (gqdepdescent_rec f))
  (path_sigma (fam_gqdescent Pe) (gq a; pa)
     (gq b; gqd_e Pe r pa) (gqglue r)
     (transport_fam_gqdescent_gqglue Pe r pa
      @' 1)) =
gqddcs_e f r pa
@' ap (gqddcs_sect f b) 1
    rhs napply concat_p1.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
ap (sig_rec (gqdepdescent_rec f))
  (path_sigma (fam_gqdescent Pe) (gq a; pa)
     (gq b; gqd_e Pe r pa) (gqglue r)
     (transport_fam_gqdescent_gqglue Pe r pa
      @' 1)) = gqddcs_e f r pa
    lhs napply ap_sig_rec_path_sigma.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(transport_const (gqglue r)
   (gqdepdescent_rec f (gq a) pa))^
@' (ap
      (fun x : fam_gqdescent Pe (gq a) =>
       transport (fun _ : GraphQuotient R => Q)
         (gqglue r) (gqdepdescent_rec f (gq a) x))
      (transport_Vp (fam_gqdescent Pe) (gqglue r) pa))^
@' (transport_arrow (gqglue r)
      (gqdepdescent_rec f (gq a))
      (transport (fam_gqdescent Pe) (gqglue r) pa))^
@' ap10 (apD (gqdepdescent_rec f) (gqglue r))
     (transport (fam_gqdescent Pe) (gqglue r) pa)
@' ap (gqdepdescent_rec f (gq b))
     (transport_fam_gqdescent_gqglue Pe r pa
      @' 1) = gqddcs_e f r pa
    lhs napply (ap (fun x => _ (ap10 x _) @ _)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
apD (gqdepdescent_rec f) (gqglue r) = ?Goal
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(transport_const (gqglue r)
   (gqdepdescent_rec f (gq a) pa))^
@' (ap
      (fun x : fam_gqdescent Pe (gq a) =>
       transport (fun _ : GraphQuotient R => Q)
         (gqglue r) (gqdepdescent_rec f (gq a) x))
      (transport_Vp (fam_gqdescent Pe) (gqglue r) pa))^
@' (transport_arrow (gqglue r)
      (gqdepdescent_rec f (gq a))
      (transport (fam_gqdescent Pe) (gqglue r) pa))^
@' ap10 ?Goal
     (transport (fam_gqdescent Pe) (gqglue r) pa)
@' ap (gqdepdescent_rec f (gq b))
     (transport_fam_gqdescent_gqglue Pe r pa
      @' 1) = gqddcs_e f r pa
    1: napply GraphQuotient_ind_beta_gqglue.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(transport_const (gqglue r)
   (gqdepdescent_rec f (gq a) pa))^
@' (ap
      (fun x : fam_gqdescent Pe (gq a) =>
       transport (fun _ : GraphQuotient R => Q)
         (gqglue r) (gqdepdescent_rec f (gq a) x))
      (transport_Vp (fam_gqdescent Pe) (gqglue r) pa))^
@' (transport_arrow (gqglue r)
      (gqdepdescent_rec f (gq a))
      (transport (fam_gqdescent Pe) (gqglue r) pa))^
@' ap10
     (dpath_arrow (fam_gqdescent Pe)
        (fun _ : GraphQuotient R => Q) (gqglue r)
        (gqddcs_sect f a) (gqddcs_sect f b)
        (fun pa : fam_gqdescent Pe (gq a) =>
         transport_const (gqglue r)
           (gqddcs_sect f a pa)
         @' (gqddcs_e f r pa
             @' (ap (gqddcs_sect f b)
                   (transport_fam_gqdescent_gqglue Pe
                      r pa))^)))
     (transport (fam_gqdescent Pe) (gqglue r) pa)
@' ap (gqdepdescent_rec f (gq b))
     (transport_fam_gqdescent_gqglue Pe r pa
      @' 1) = gqddcs_e f r pa
    do 3 lhs napply concat_pp_p.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(transport_const (gqglue r)
   (gqdepdescent_rec f (gq a) pa))^
@' ((ap
       (fun x : fam_gqdescent Pe (gq a) =>
        transport (fun _ : GraphQuotient R => Q)
          (gqglue r) (gqdepdescent_rec f (gq a) x))
       (transport_Vp (fam_gqdescent Pe) (gqglue r) pa))^
    @' ((transport_arrow (gqglue r)
           (gqdepdescent_rec f (gq a))
           (transport (fam_gqdescent Pe) (gqglue r) pa))^
        @' (ap10
              (dpath_arrow (fam_gqdescent Pe)
                 (fun _ : GraphQuotient R => Q)
                 (gqglue r) (gqddcs_sect f a)
                 (gqddcs_sect f b)
                 (fun pa : fam_gqdescent Pe (gq a) =>
                  transport_const (gqglue r)
                    (gqddcs_sect f a pa)
                  @' (gqddcs_e f r pa
                      @' (ap (gqddcs_sect f b)
                            (transport_fam_gqdescent_gqglue
                               Pe r pa))^)))
              (transport (fam_gqdescent Pe) (gqglue r)
                 pa)
            @' ap (gqdepdescent_rec f (gq b))
                 (transport_fam_gqdescent_gqglue Pe r
                    pa
                  @' 1)))) = gqddcs_e f r pa
    apply moveR_Vp.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(ap
   (fun x : fam_gqdescent Pe (gq a) =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue r) (gqdepdescent_rec f (gq a) x))
   (transport_Vp (fam_gqdescent Pe) (gqglue r) pa))^
@' ((transport_arrow (gqglue r)
       (gqdepdescent_rec f (gq a))
       (transport (fam_gqdescent Pe) (gqglue r) pa))^
    @' (ap10
          (dpath_arrow (fam_gqdescent Pe)
             (fun _ : GraphQuotient R => Q) (gqglue r)
             (gqddcs_sect f a) (gqddcs_sect f b)
             (fun pa : fam_gqdescent Pe (gq a) =>
              transport_const (gqglue r)
                (gqddcs_sect f a pa)
              @' (gqddcs_e f r pa
                  @' (ap (gqddcs_sect f b)
                        (transport_fam_gqdescent_gqglue
                           Pe r pa))^)))
          (transport (fam_gqdescent Pe) (gqglue r) pa)
        @' ap (gqdepdescent_rec f (gq b))
             (transport_fam_gqdescent_gqglue Pe r pa
              @' 1))) =
transport_const (gqglue r)
  (gqdepdescent_rec f (gq a) pa)
@' gqddcs_e f r pa
    lhs nrefine (1 @@ (1 @@ (_ @@ 1))).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
ap10
  (dpath_arrow (fam_gqdescent Pe)
     (fun _ : GraphQuotient R => Q) (gqglue r)
     (gqddcs_sect f a) (gqddcs_sect f b)
     (fun pa : fam_gqdescent Pe (gq a) =>
      transport_const (gqglue r) (gqddcs_sect f a pa)
      @' (gqddcs_e f r pa
          @' (ap (gqddcs_sect f b)
                (transport_fam_gqdescent_gqglue Pe r
                   pa))^)))
  (transport (fam_gqdescent Pe) (gqglue r) pa) = ?Goal
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(ap
   (fun x : fam_gqdescent Pe (gq a) =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue r) (gqdepdescent_rec f (gq a) x))
   (transport_Vp (fam_gqdescent Pe) (gqglue r) pa))^
@' ((transport_arrow (gqglue r)
       (gqdepdescent_rec f (gq a))
       (transport (fam_gqdescent Pe) (gqglue r) pa))^
    @' (?Goal
        @' ap (gqdepdescent_rec f (gq b))
             (transport_fam_gqdescent_gqglue Pe r pa
              @' 1))) =
transport_const (gqglue r)
  (gqdepdescent_rec f (gq a) pa)
@' gqddcs_e f r pa
    1: napply (ap10_dpath_arrow (fam_gqdescent Pe) (fun _ => Q) (gqglue r)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(ap
   (fun x : fam_gqdescent Pe (gq a) =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue r) (gqdepdescent_rec f (gq a) x))
   (transport_Vp (fam_gqdescent Pe) (gqglue r) pa))^
@' ((transport_arrow (gqglue r)
       (gqdepdescent_rec f (gq a))
       (transport (fam_gqdescent Pe) (gqglue r) pa))^
    @' (transport_arrow (gqglue r)
          (gqdepdescent_rec f (gq a))
          (transport (fam_gqdescent Pe) (gqglue r) pa)
        @' ap
             (fun x : fam_gqdescent Pe (gq a) =>
              transport (fun _ : GraphQuotient R => Q)
                (gqglue r)
                (gqdepdescent_rec f (gq a) x))
             (transport_Vp (fam_gqdescent Pe)
                (gqglue r) pa)
        @' (fun pa : fam_gqdescent Pe (gq a) =>
            transport_const (gqglue r)
              (gqddcs_sect f a pa)
            @' (gqddcs_e f r pa
                @' (ap (gqddcs_sect f b)
                      (transport_fam_gqdescent_gqglue
                         Pe r pa))^)) pa
        @' ap (gqdepdescent_rec f (gq b))
             (transport_fam_gqdescent_gqglue Pe r pa
              @' 1))) =
transport_const (gqglue r)
  (gqdepdescent_rec f (gq a) pa)
@' gqddcs_e f r pa
    lhs nrefine (1 @@ _).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(transport_arrow (gqglue r)
   (gqdepdescent_rec f (gq a))
   (transport (fam_gqdescent Pe) (gqglue r) pa))^
@' (transport_arrow (gqglue r)
      (gqdepdescent_rec f (gq a))
      (transport (fam_gqdescent Pe) (gqglue r) pa)
    @' ap
         (fun x : fam_gqdescent Pe (gq a) =>
          transport (fun _ : GraphQuotient R => Q)
            (gqglue r) (gqdepdescent_rec f (gq a) x))
         (transport_Vp (fam_gqdescent Pe) (gqglue r)
            pa)
    @' (transport_const (gqglue r)
          (gqddcs_sect f a pa)
        @' (gqddcs_e f r pa
            @' (ap (gqddcs_sect f b)
                  (transport_fam_gqdescent_gqglue Pe r
                     pa))^))
    @' ap (gqdepdescent_rec f (gq b))
         (transport_fam_gqdescent_gqglue Pe r pa
          @' 1)) = ?Goal
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(ap
   (fun x : fam_gqdescent Pe (gq a) =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue r) (gqdepdescent_rec f (gq a) x))
   (transport_Vp (fam_gqdescent Pe) (gqglue r) pa))^
@' ?Goal =
transport_const (gqglue r)
  (gqdepdescent_rec f (gq a) pa)
@' gqddcs_e f r pa
    {H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(transport_arrow (gqglue r)
   (gqdepdescent_rec f (gq a))
   (transport (fam_gqdescent Pe) (gqglue r) pa))^
@' (transport_arrow (gqglue r)
      (gqdepdescent_rec f (gq a))
      (transport (fam_gqdescent Pe) (gqglue r) pa)
    @' ap
         (fun x : fam_gqdescent Pe (gq a) =>
          transport (fun _ : GraphQuotient R => Q)
            (gqglue r) (gqdepdescent_rec f (gq a) x))
         (transport_Vp (fam_gqdescent Pe) (gqglue r)
            pa)
    @' (transport_const (gqglue r)
          (gqddcs_sect f a pa)
        @' (gqddcs_e f r pa
            @' (ap (gqddcs_sect f b)
                  (transport_fam_gqdescent_gqglue Pe r
                     pa))^))
    @' ap (gqdepdescent_rec f (gq b))
         (transport_fam_gqdescent_gqglue Pe r pa
          @' 1)) = ?Goal lhs napply (1 @@ concat_pp_p _ _ _).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(transport_arrow (gqglue r)
   (gqdepdescent_rec f (gq a))
   (transport (fam_gqdescent Pe) (gqglue r) pa))^
@' (transport_arrow (gqglue r)
      (gqdepdescent_rec f (gq a))
      (transport (fam_gqdescent Pe) (gqglue r) pa)
    @' ap
         (fun x : fam_gqdescent Pe (gq a) =>
          transport (fun _ : GraphQuotient R => Q)
            (gqglue r) (gqdepdescent_rec f (gq a) x))
         (transport_Vp (fam_gqdescent Pe) (gqglue r)
            pa)
    @' (transport_const (gqglue r)
          (gqddcs_sect f a pa)
        @' (gqddcs_e f r pa
            @' (ap (gqddcs_sect f b)
                  (transport_fam_gqdescent_gqglue Pe r
                     pa))^)
        @' ap (gqdepdescent_rec f (gq b))
             (transport_fam_gqdescent_gqglue Pe r pa
              @' 1))) = ?Goal
      lhs napply (1 @@ concat_pp_p _ _ _).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(transport_arrow (gqglue r)
   (gqdepdescent_rec f (gq a))
   (transport (fam_gqdescent Pe) (gqglue r) pa))^
@' (transport_arrow (gqglue r)
      (gqdepdescent_rec f (gq a))
      (transport (fam_gqdescent Pe) (gqglue r) pa)
    @' (ap
          (fun x : fam_gqdescent Pe (gq a) =>
           transport (fun _ : GraphQuotient R => Q)
             (gqglue r) (gqdepdescent_rec f (gq a) x))
          (transport_Vp (fam_gqdescent Pe) (gqglue r)
             pa)
        @' (transport_const (gqglue r)
              (gqddcs_sect f a pa)
            @' (gqddcs_e f r pa
                @' (ap (gqddcs_sect f b)
                      (transport_fam_gqdescent_gqglue
                         Pe r pa))^)
            @' ap (gqdepdescent_rec f (gq b))
                 (transport_fam_gqdescent_gqglue Pe r
                    pa
                  @' 1)))) = ?Goal
      lhs napply concat_V_pp.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
ap
  (fun x : fam_gqdescent Pe (gq a) =>
   transport (fun _ : GraphQuotient R => Q) (gqglue r)
     (gqdepdescent_rec f (gq a) x))
  (transport_Vp (fam_gqdescent Pe) (gqglue r) pa)
@' (transport_const (gqglue r) (gqddcs_sect f a pa)
    @' (gqddcs_e f r pa
        @' (ap (gqddcs_sect f b)
              (transport_fam_gqdescent_gqglue Pe r pa))^)
    @' ap (gqdepdescent_rec f (gq b))
         (transport_fam_gqdescent_gqglue Pe r pa
          @' 1)) = ?Goal
      lhs napply (1 @@ concat_pp_p _ _ _).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
ap
  (fun x : fam_gqdescent Pe (gq a) =>
   transport (fun _ : GraphQuotient R => Q) (gqglue r)
     (gqdepdescent_rec f (gq a) x))
  (transport_Vp (fam_gqdescent Pe) (gqglue r) pa)
@' (transport_const (gqglue r) (gqddcs_sect f a pa)
    @' (gqddcs_e f r pa
        @' (ap (gqddcs_sect f b)
              (transport_fam_gqdescent_gqglue Pe r pa))^
        @' ap (gqdepdescent_rec f (gq b))
             (transport_fam_gqdescent_gqglue Pe r pa
              @' 1))) = ?Goal
      rewrite concat_p1.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
ap
  (fun x : fam_gqdescent Pe (gq a) =>
   transport (fun _ : GraphQuotient R => Q) (gqglue r)
     (gqdepdescent_rec f (gq a) x))
  (transport_Vp (fam_gqdescent Pe) (gqglue r) pa)
@' (transport_const (gqglue r) (gqddcs_sect f a pa)
    @' (gqddcs_e f r pa
        @' (ap (gqddcs_sect f b)
              (transport_fam_gqdescent_gqglue Pe r pa))^
        @' ap (gqdepdescent_rec f (gq b))
             (transport_fam_gqdescent_gqglue Pe r pa))) =
?Goal
      exact (1 @@ (1 @@ concat_pV_p _ _)). }H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
Q: Type
f: gqDepDescentConstSection Pe Q
a, b: A
pa: gqd_fam Pe a
r: R a b
(ap
   (fun x : fam_gqdescent Pe (gq a) =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue r) (gqdepdescent_rec f (gq a) x))
   (transport_Vp (fam_gqdescent Pe) (gqglue r) pa))^
@' (ap
      (fun x : fam_gqdescent Pe (gq a) =>
       transport (fun _ : GraphQuotient R => Q)
         (gqglue r) (gqdepdescent_rec f (gq a) x))
      (transport_Vp (fam_gqdescent Pe) (gqglue r) pa)
    @' (transport_const (gqglue r)
          (gqddcs_sect f a pa)
        @' gqddcs_e f r pa)) =
transport_const (gqglue r)
  (gqdepdescent_rec f (gq a) pa)
@' gqddcs_e f r pa
    napply concat_V_pp.
    Close Scope long_path_scope.
  Defined.

End Descent.

(** ** The flattening lemma *)

(** We saw above that given descent data [Pe] over a graph [A] and [R] we obtained a type family [fam_gqdescent Pe] over the graph quotient.  The flattening lemma describes the total space [sig (fam_gqdescent Pe)] of this type family as a graph quotient of [sig (gqd_fam Pe)] by a certain relation.  This follows from the work above, which shows that [sig (fam_gqdescent Pe)] has the same universal property as this graph quotient. *)

Section Flattening.

  Context `{Univalence} {A : Type} {R : A -> A -> Type} (Pe : gqDescent R).

  (** We mimic the constructors of [GraphQuotient] for the total space.  Here is the point constructor, in curried form. *)
  Definition flatten_gqd {a : A} (pa : gqd_fam Pe a) : sig (fam_gqdescent Pe)
    := (gq a; pa).

  (** And here is the path constructor. *)
  Definition flatten_gqd_glue {a b : A} (r : R a b)
    {pa : gqd_fam Pe a} {pb : gqd_fam Pe b} (pr : gqd_e Pe r pa = pb)
    : flatten_gqd pa = flatten_gqd pb.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
pb: gqd_fam Pe b
pr: gqd_e Pe r pa = pb
flatten_gqd pa = flatten_gqd pb
  Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
pb: gqd_fam Pe b
pr: gqd_e Pe r pa = pb
flatten_gqd pa = flatten_gqd pb
    snapply path_sigma.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
pb: gqd_fam Pe b
pr: gqd_e Pe r pa = pb
(flatten_gqd pa).1 = (flatten_gqd pb).1
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
pb: gqd_fam Pe b
pr: gqd_e Pe r pa = pb
transport (fam_gqdescent Pe) ?p (flatten_gqd pa).2 =
(flatten_gqd pb).2
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
pb: gqd_fam Pe b
pr: gqd_e Pe r pa = pb
(flatten_gqd pa).1 = (flatten_gqd pb).1 by apply gqglue.
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
pb: gqd_fam Pe b
pr: gqd_e Pe r pa = pb
transport (fam_gqdescent Pe) (gqglue r)
  (flatten_gqd pa).2 = (flatten_gqd pb).2 lhs napply transport_fam_gqdescent_gqglue.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
pb: gqd_fam Pe b
pr: gqd_e Pe r pa = pb
gqd_e Pe r (flatten_gqd pa).2 = (flatten_gqd pb).2
      exact pr.
  Defined.

  (** Now that we've shown that [fam_gqdescent Pe] acts like a [GraphQuotient] of [sig (gqd_fam Pe)] by an appropriate relation, we can use this to prove the flattening lemma.  The maps back and forth are very easy so this could almost be a formal consequence of the induction principle. *)
  Lemma equiv_gqd_flatten : sig (fam_gqdescent Pe) <~>
    GraphQuotient (fun a b => {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2}).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
{x : _ & fam_gqdescent Pe x} <~>
GraphQuotient
  (fun a b : {x : _ & gqd_fam Pe x} =>
   {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2})
  Proof.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
{x : _ & fam_gqdescent Pe x} <~>
GraphQuotient
  (fun a b : {x : _ & gqd_fam Pe x} =>
   {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2})
    snapply equiv_adjointify.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
{x : _ & fam_gqdescent Pe x} ->
GraphQuotient
  (fun a b : {x : _ & gqd_fam Pe x} =>
   {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2})
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
GraphQuotient
  (fun a b : {x : _ & gqd_fam Pe x} =>
   {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2}) ->
{x : _ & fam_gqdescent Pe x}
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
?f o ?g == idmap
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
?g o ?f == idmap
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
{x : _ & fam_gqdescent Pe x} ->
GraphQuotient
  (fun a b : {x : _ & gqd_fam Pe x} =>
   {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2}) snapply sig_rec.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall proj1 : GraphQuotient R,
fam_gqdescent Pe proj1 ->
GraphQuotient
  (fun a b : {x : _ & gqd_fam Pe x} =>
   {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2})
      snapply gqdepdescent_rec.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
gqDepDescentConstSection Pe
  (GraphQuotient
     (fun a b : {x : _ & gqd_fam Pe x} =>
      {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2}))
      snapply Build_gqDepDescentConstSection.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall a : A,
gqd_fam Pe a ->
GraphQuotient
  (fun a0 b : {x : _ & gqd_fam Pe x} =>
   {r : R a0.1 b.1 & gqd_e Pe r a0.2 = b.2})
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall (a b : A) (r : R a b) (pa : gqd_fam Pe a),
?gqddcs_sect a pa = ?gqddcs_sect b (gqd_e Pe r pa)
      +H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall a : A,
gqd_fam Pe a ->
GraphQuotient
  (fun a0 b : {x : _ & gqd_fam Pe x} =>
   {r : R a0.1 b.1 & gqd_e Pe r a0.2 = b.2}) exact (fun a x => gq (a; x)).
      +H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall (a b : A) (r : R a b) (pa : gqd_fam Pe a),
(fun (a0 : A) (x : gqd_fam Pe a0) => gq (a0; x)) a pa =
(fun (a0 : A) (x : gqd_fam Pe a0) => gq (a0; x)) b
  (gqd_e Pe r pa) intros a b r pa.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
(fun (a : A) (x : gqd_fam Pe a) => gq (a; x)) a pa =
(fun (a : A) (x : gqd_fam Pe a) => gq (a; x)) b
  (gqd_e Pe r pa)
      apply gqglue; exact (r; 1).
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
GraphQuotient
  (fun a b : {x : _ & gqd_fam Pe x} =>
   {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2}) ->
{x : _ & fam_gqdescent Pe x} snapply GraphQuotient_rec.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
{x : _ & gqd_fam Pe x} -> {x : _ & fam_gqdescent Pe x}
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall a b : {x : _ & gqd_fam Pe x},
(fun a0 b0 : {x : _ & gqd_fam Pe x} =>
 {r : R a0.1 b0.1 & gqd_e Pe r a0.2 = b0.2}) a b ->
?c a = ?c b
      +H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
{x : _ & gqd_fam Pe x} -> {x : _ & fam_gqdescent Pe x} exact (fun '(a; x) => (gq a; x)).
      +H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall a b : {x : _ & gqd_fam Pe x},
(fun a0 b0 : {x : _ & gqd_fam Pe x} =>
 {r : R a0.1 b0.1 & gqd_e Pe r a0.2 = b0.2}) a b ->
(fun pat : {x : _ & gqd_fam Pe x} =>
 let x := pat in
 let a0 := x.1 in let x0 := x.2 in (gq a0; x0)) a =
(fun pat : {x : _ & gqd_fam Pe x} =>
 let x := pat in
 let a0 := x.1 in let x0 := x.2 in (gq a0; x0)) b intros [a x] [b y] [r pr]; cbn in r, pr; cbn.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a: A
x: gqd_fam Pe a
b: A
y: gqd_fam Pe b
r: R a b
pr: gqd_e Pe r x = y
(gq a; x) = (gq b; y)
        exact (flatten_gqd_glue r pr).
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
sig_rec
  (gqdepdescent_rec
     {|
       gqddcs_sect :=
         fun (a : A) (x : gqd_fam Pe a) => gq (a; x);
       gqddcs_e :=
         fun (a b : A) (r : R a b) (pa : gqd_fam Pe a)
         => gqglue (r; 1)
     |})
o GraphQuotient_rec
    (fun pat : {x : _ & gqd_fam Pe x} =>
     let x := pat in
     let a := x.1 in let x0 := x.2 in (gq a; x0))
    (fun a0 : {x : _ & gqd_fam Pe x} =>
     (fun (a : A) (x : gqd_fam Pe a)
        (b0 : {x : _ & gqd_fam Pe x}) =>
      (fun (b : A) (y : gqd_fam Pe b)
         (X : {r : R (a; x).1 (b; y).1 &
              gqd_e Pe r (a; x).2 = (b; y).2}) =>
       (fun (r : R (a; x).1 (b; y).1)
          (pr : gqd_e Pe r (a; x).2 = (b; y).2) =>
        flatten_gqd_glue r pr
        :
        (let x0 := (a; x) in
         let a1 := x0.1 in
         let x1 := x0.2 in (gq a1; x1)) =
        (let x0 := (b; y) in
         let a1 := x0.1 in
         let x1 := x0.2 in (gq a1; x1))) X.1 X.2) b0.1
        b0.2) a0.1 a0.2) == idmap snapply GraphQuotient_ind.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall a : {x : _ & gqd_fam Pe x},
(fun
   x : GraphQuotient
         (fun a0 b : {x : _ & gqd_fam Pe x} =>
          {r : R a0.1 b.1 & gqd_e Pe r a0.2 = b.2}) =>
 (sig_rec
    (gqdepdescent_rec
       {|
         gqddcs_sect :=
           fun (a0 : A) (x0 : gqd_fam Pe a0) =>
           gq (a0; x0);
         gqddcs_e :=
           fun (a0 b : A) (r : R a0 b)
             (pa : gqd_fam Pe a0) => gqglue (r; 1)
       |})
  o GraphQuotient_rec
      (fun pat : {x : _ & gqd_fam Pe x} =>
       let x0 := pat in
       let a0 := x0.1 in let x1 := x0.2 in (gq a0; x1))
      (fun a0 : {x : _ & gqd_fam Pe x} =>
       (fun (a1 : A) (x0 : gqd_fam Pe a1)
          (b0 : {x : _ & gqd_fam Pe x}) =>
        (fun (b : A) (y : gqd_fam Pe b)
           (X : {r : R (a1; x0).1 (b; y).1 &
                gqd_e Pe r (a1; x0).2 = (b; y).2}) =>
         (fun (r : R (a1; x0).1 (b; y).1)
            (pr : gqd_e Pe r (a1; x0).2 = (b; y).2) =>
          flatten_gqd_glue r pr
          :
          (let x1 := (a1; x0) in
           let a2 := x1.1 in
           let x2 := x1.2 in (...; x2)) =
          (let x1 := (b; y) in
           let a2 := x1.1 in
           let x2 := x1.2 in (...; x2))) X.1 X.2) b0.1
          b0.2) a0.1 a0.2)) x = idmap x) (gq a)
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall (a b : {x : _ & gqd_fam Pe x})
(s : (fun a0 b0 : {x : _ & gqd_fam Pe x} =>
      {r : R a0.1 b0.1 & gqd_e Pe r a0.2 = b0.2}) a b),
transport
  (fun
     x : GraphQuotient
           (fun a0 b0 : {x : _ & gqd_fam Pe x} =>
            {r : R a0.1 b0.1 & gqd_e Pe r a0.2 = b0.2})
   =>
   (sig_rec
      (gqdepdescent_rec
         {|
           gqddcs_sect :=
             fun (a0 : A) (x0 : gqd_fam Pe a0) =>
             gq (a0; x0);
           gqddcs_e :=
             fun (a0 b0 : A) (r : R a0 b0)
               (pa : gqd_fam Pe a0) => gqglue (r; 1)
         |})
    o GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (gq a0; x1))
        (fun a0 : {x : _ & gqd_fam Pe x} =>
         (fun (a1 : A) (x0 : gqd_fam Pe a1)
            (b0 : {x : _ & gqd_fam Pe x}) =>
          (fun (b1 : A) (y : gqd_fam Pe b1)
             (X : {r : R (a1; x0).1 (b1; y).1 &
                  gqd_e Pe r (a1; x0).2 = (b1; y).2})
           =>
           (fun (r : R (a1; x0).1 (b1; y).1)
              (pr : gqd_e Pe r (a1; x0).2 = (b1; y).2)
            =>
            flatten_gqd_glue r pr
            :
            (let x1 := (a1; x0) in
             let a2 := x1.1 in ... ...) =
            (let x1 := (b1; y) in
             let a2 := x1.1 in ... ...)) X.1 X.2) b0.1
            b0.2) a0.1 a0.2)) x = idmap x) (gqglue s)
  (?gq' a) = ?gq' b
      1: reflexivity.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall (a b : {x : _ & gqd_fam Pe x})
(s : (fun a0 b0 : {x : _ & gqd_fam Pe x} =>
      {r : R a0.1 b0.1 & gqd_e Pe r a0.2 = b0.2}) a b),
transport
  (fun
     x : GraphQuotient
           (fun a0 b0 : {x : _ & gqd_fam Pe x} =>
            {r : R a0.1 b0.1 & gqd_e Pe r a0.2 = b0.2})
   =>
   (sig_rec
      (gqdepdescent_rec
         {|
           gqddcs_sect :=
             fun (a0 : A) (x0 : gqd_fam Pe a0) =>
             gq (a0; x0);
           gqddcs_e :=
             fun (a0 b0 : A) (r : R a0 b0)
               (pa : gqd_fam Pe a0) => gqglue (r; 1)
         |})
    o GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (gq a0; x1))
        (fun a0 : {x : _ & gqd_fam Pe x} =>
         (fun (a1 : A) (x0 : gqd_fam Pe a1)
            (b0 : {x : _ & gqd_fam Pe x}) =>
          (fun (b1 : A) (y : gqd_fam Pe b1)
             (X : {r : R (a1; x0).1 (b1; y).1 &
                  gqd_e Pe r (a1; x0).2 = (b1; y).2})
           =>
           (fun (r : R (a1; x0).1 (b1; y).1)
              (pr : gqd_e Pe r (a1; x0).2 = (b1; y).2)
            =>
            flatten_gqd_glue r pr
            :
            (let x1 := (a1; x0) in
             let a2 := x1.1 in ... ...) =
            (let x1 := (b1; y) in
             let a2 := x1.1 in ... ...)) X.1 X.2) b0.1
            b0.2) a0.1 a0.2)) x = idmap x) (gqglue s)
  ((fun a0 : {x : _ & gqd_fam Pe x} => 1) a) =
(fun a0 : {x : _ & gqd_fam Pe x} => 1) b
      intros [a x] [b y] [r pr]; cbn in r, pr; cbn.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a: A
x: gqd_fam Pe a
b: A
y: gqd_fam Pe b
r: R a b
pr: gqd_e Pe r x = y
transport
  (fun
     x : GraphQuotient
           (fun a b : {x : _ & gqd_fam Pe x} =>
            {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2}) =>
   sig_rec
     (gqdepdescent_rec
        {|
          gqddcs_sect :=
            fun (a : A) (x0 : gqd_fam Pe a) =>
            gq (a; x0);
          gqddcs_e :=
            fun (a b : A) (r : R a b)
              (pa : gqd_fam Pe a) => gqglue (r; 1)
        |})
     (GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         (gq pat.1; pat.2))
        (fun (a0 b0 : {x : _ & gqd_fam Pe x})
           (X : {r : R a0.1 b0.1 &
                gqd_e Pe r a0.2 = b0.2}) =>
         flatten_gqd_glue X.1 X.2) x) = x)
  (gqglue (r; pr)) 1 = 1
      destruct pr.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a: A
x: gqd_fam Pe a
b: A
r: R a b
transport
  (fun
     x : GraphQuotient
           (fun a b : {x : _ & gqd_fam Pe x} =>
            {r : R a.1 b.1 & gqd_e Pe r a.2 = b.2}) =>
   sig_rec
     (gqdepdescent_rec
        {|
          gqddcs_sect :=
            fun (a : A) (x0 : gqd_fam Pe a) =>
            gq (a; x0);
          gqddcs_e :=
            fun (a b : A) (r : R a b)
              (pa : gqd_fam Pe a) => gqglue (r; 1)
        |})
     (GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         (gq pat.1; pat.2))
        (fun (a0 b0 : {x : _ & gqd_fam Pe x})
           (X : {r : R a0.1 b0.1 &
                gqd_e Pe r a0.2 = b0.2}) =>
         flatten_gqd_glue X.1 X.2) x) = x)
  (gqglue (r; 1)) 1 = 1
      transport_paths FFlr; apply equiv_p1_1q.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a: A
x: gqd_fam Pe a
b: A
r: R a b
ap
  (sig_rec
     (gqdepdescent_rec
        {|
          gqddcs_sect :=
            fun (a : A) (x : gqd_fam Pe a) =>
            gq (a; x);
          gqddcs_e :=
            fun (a b : A) (r : R a b)
              (pa : gqd_fam Pe a) => gqglue (r; 1)
        |}))
  (ap
     (GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         (gq pat.1; pat.2))
        (fun (a0 b0 : {x : _ & gqd_fam Pe x})
           (X : {r : R a0.1 b0.1 &
                gqd_e Pe r a0.2 = b0.2}) =>
         flatten_gqd_glue X.1 X.2)) (gqglue (r; 1))) =
gqglue (r; 1)
      rewrite GraphQuotient_rec_beta_gqglue.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a: A
x: gqd_fam Pe a
b: A
r: R a b
ap
  (sig_rec
     (gqdepdescent_rec
        {|
          gqddcs_sect :=
            fun (a : A) (x : gqd_fam Pe a) =>
            gq (a; x);
          gqddcs_e :=
            fun (a b : A) (r : R a b)
              (pa : gqd_fam Pe a) => gqglue (r; 1)
        |})) (flatten_gqd_glue r 1) = gqglue (r; 1)
      lhs napply gqdepdescent_rec_beta_gqglue.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a: A
x: gqd_fam Pe a
b: A
r: R a b
gqddcs_e
  {|
    gqddcs_sect :=
      fun (a : A) (x : gqd_fam Pe a) => gq (a; x);
    gqddcs_e :=
      fun (a b : A) (r : R a b) (pa : gqd_fam Pe a) =>
      gqglue (r; 1)
  |} r x @
ap
  (gqddcs_sect
     {|
       gqddcs_sect :=
         fun (a : A) (x : gqd_fam Pe a) => gq (a; x);
       gqddcs_e :=
         fun (a b : A) (r : R a b) (pa : gqd_fam Pe a)
         => gqglue (r; 1)
     |} b) 1 = gqglue (r; 1)
      napply concat_p1.
    -H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
GraphQuotient_rec
  (fun pat : {x : _ & gqd_fam Pe x} =>
   let x := pat in
   let a := x.1 in let x0 := x.2 in (gq a; x0))
  (fun a0 : {x : _ & gqd_fam Pe x} =>
   (fun (a : A) (x : gqd_fam Pe a)
      (b0 : {x : _ & gqd_fam Pe x}) =>
    (fun (b : A) (y : gqd_fam Pe b)
       (X : {r : R (a; x).1 (b; y).1 &
            gqd_e Pe r (a; x).2 = (b; y).2}) =>
     (fun (r : R (a; x).1 (b; y).1)
        (pr : gqd_e Pe r (a; x).2 = (b; y).2) =>
      flatten_gqd_glue r pr
      :
      (let x0 := (a; x) in
       let a1 := x0.1 in let x1 := x0.2 in (gq a1; x1)) =
      (let x0 := (b; y) in
       let a1 := x0.1 in let x1 := x0.2 in (gq a1; x1)))
       X.1 X.2) b0.1 b0.2) a0.1 a0.2)
o sig_rec
    (gqdepdescent_rec
       {|
         gqddcs_sect :=
           fun (a : A) (x : gqd_fam Pe a) => gq (a; x);
         gqddcs_e :=
           fun (a b : A) (r : R a b)
             (pa : gqd_fam Pe a) => gqglue (r; 1)
       |}) == idmap intros [x px]; revert x px.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall (x : GraphQuotient R)
(px : fam_gqdescent Pe x),
GraphQuotient_rec
  (fun pat : {x : _ & gqd_fam Pe x} =>
   let x0 := pat in
   let a := x0.1 in let x1 := x0.2 in (gq a; x1))
  (fun (a0 b0 : {x : _ & gqd_fam Pe x})
     (X : {r : R (a0.1; a0.2).1 (b0.1; b0.2).1 &
          gqd_e Pe r (a0.1; a0.2).2 = (b0.1; b0.2).2})
   => flatten_gqd_glue X.1 X.2)
  (sig_rec
     (gqdepdescent_rec
        {|
          gqddcs_sect :=
            fun (a : A) (x0 : gqd_fam Pe a) =>
            gq (a; x0);
          gqddcs_e :=
            fun (a b : A) (r : R a b)
              (pa : gqd_fam Pe a) => gqglue (r; 1)
        |}) (x; px)) = (x; px)
      snapply gqdepdescent_ind.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
gqDepDescentSection
  (gqdepdescent_fam
     (fun (x : GraphQuotient R)
        (px : fam_gqdescent Pe x) =>
      GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         let x0 := pat in
         let a := x0.1 in let x1 := x0.2 in (gq a; x1))
        (fun (a0 b0 : {x : _ & gqd_fam Pe x})
           (X : {r : R (a0.1; a0.2).1 (b0.1; b0.2).1 &
                gqd_e Pe r (a0.1; a0.2).2 =
                (b0.1; b0.2).2}) =>
         flatten_gqd_glue X.1 X.2)
        (sig_rec
           (gqdepdescent_rec
              {|
                gqddcs_sect :=
                  fun (a : A) (x0 : gqd_fam Pe a) =>
                  gq (a; x0);
                gqddcs_e :=
                  fun (a b : A) (r : R a b)
                    (pa : gqd_fam Pe a) =>
                  gqglue (r; 1)
              |}) (x; px)) = (x; px)))
      snapply Build_gqDepDescentSection.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall (a : A) (pa : gqd_fam Pe a),
gqdd_fam
  (gqdepdescent_fam
     (fun (x : GraphQuotient R)
        (px : fam_gqdescent Pe x) =>
      GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (gq a0; x1))
        (fun (a0 b0 : {x : _ & gqd_fam Pe x})
           (X : {r : R (a0.1; a0.2).1 (b0.1; b0.2).1 &
                gqd_e Pe r (a0.1; a0.2).2 =
                (b0.1; b0.2).2}) =>
         flatten_gqd_glue X.1 X.2)
        (sig_rec
           (gqdepdescent_rec
              {|
                gqddcs_sect :=
                  fun (a0 : A) (x0 : gqd_fam Pe a0) =>
                  gq (a0; x0);
                gqddcs_e :=
                  fun (a0 b : A) (r : R a0 b)
                    (pa0 : gqd_fam Pe a0) =>
                  gqglue (r; 1)
              |}) (x; px)) = (x; px))) a pa
H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall (a b : A) (r : R a b) (pa : gqd_fam Pe a),
gqdd_e
  (gqdepdescent_fam
     (fun (x : GraphQuotient R)
        (px : fam_gqdescent Pe x) =>
      GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (gq a0; x1))
        (fun (a0 b0 : {x : _ & gqd_fam Pe x})
           (X : {r0 : R (a0.1; a0.2).1 (b0.1; b0.2).1
                &
                gqd_e Pe r0 (a0.1; a0.2).2 =
                (b0.1; b0.2).2}) =>
         flatten_gqd_glue X.1 X.2)
        (sig_rec
           (gqdepdescent_rec
              {|
                gqddcs_sect :=
                  fun (a0 : A) (x0 : gqd_fam Pe a0) =>
                  gq (a0; x0);
                gqddcs_e :=
                  fun (a0 b0 : A) (r0 : R a0 b0)
                    (pa0 : gqd_fam Pe a0) =>
                  gqglue (r0; 1)
              |}) (x; px)) = (x; px))) r pa
  (?gqdds_sect a pa) = ?gqdds_sect b (gqd_e Pe r pa)
      +H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall (a : A) (pa : gqd_fam Pe a),
gqdd_fam
  (gqdepdescent_fam
     (fun (x : GraphQuotient R)
        (px : fam_gqdescent Pe x) =>
      GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (gq a0; x1))
        (fun (a0 b0 : {x : _ & gqd_fam Pe x})
           (X : {r : R (a0.1; a0.2).1 (b0.1; b0.2).1 &
                gqd_e Pe r (a0.1; a0.2).2 =
                (b0.1; b0.2).2}) =>
         flatten_gqd_glue X.1 X.2)
        (sig_rec
           (gqdepdescent_rec
              {|
                gqddcs_sect :=
                  fun (a0 : A) (x0 : gqd_fam Pe a0) =>
                  gq (a0; x0);
                gqddcs_e :=
                  fun (a0 b : A) (r : R a0 b)
                    (pa0 : gqd_fam Pe a0) =>
                  gqglue (r; 1)
              |}) (x; px)) = (x; px))) a pa by intros a pa.
      +H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
forall (a b : A) (r : R a b) (pa : gqd_fam Pe a),
gqdd_e
  (gqdepdescent_fam
     (fun (x : GraphQuotient R)
        (px : fam_gqdescent Pe x) =>
      GraphQuotient_rec
        (fun pat : {x : _ & gqd_fam Pe x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (gq a0; x1))
        (fun (a0 b0 : {x : _ & gqd_fam Pe x})
           (X : {r0 : R (a0.1; a0.2).1 (b0.1; b0.2).1
                &
                gqd_e Pe r0 (a0.1; a0.2).2 =
                (b0.1; b0.2).2}) =>
         flatten_gqd_glue X.1 X.2)
        (sig_rec
           (gqdepdescent_rec
              {|
                gqddcs_sect :=
                  fun (a0 : A) (x0 : gqd_fam Pe a0) =>
                  gq (a0; x0);
                gqddcs_e :=
                  fun (a0 b0 : A) (r0 : R a0 b0)
                    (pa0 : gqd_fam Pe a0) =>
                  gqglue (r0; 1)
              |}) (x; px)) = (x; px))) r pa
  ((fun (a0 : A) (pa0 : gqd_fam Pe a0) => 1) a pa) =
(fun (a0 : A) (pa0 : gqd_fam Pe a0) => 1) b
  (gqd_e Pe r pa) intros a b r pa; cbn.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
transportDD (fam_gqdescent Pe)
  (fun (x : GraphQuotient R) (px : fam_gqdescent Pe x)
   =>
   GraphQuotient_rec
     (fun pat : {x : _ & gqd_fam Pe x} =>
      (gq pat.1; pat.2))
     (fun (a0 b0 : {x : _ & gqd_fam Pe x})
        (X : {r : R a0.1 b0.1 &
             gqd_e Pe r a0.2 = b0.2}) =>
      flatten_gqd_glue X.1 X.2)
     (sig_rec
        (gqdepdescent_rec
           {|
             gqddcs_sect :=
               fun (a : A) (x0 : gqd_fam Pe a) =>
               gq (a; x0);
             gqddcs_e :=
               fun (a b : A) (r : R a b)
                 (pa : gqd_fam Pe a) => gqglue (r; 1)
           |}) (x; px)) = (x; px)) (gqglue r)
  (transport_fam_gqdescent_gqglue Pe r pa) 1 = 1
        lhs napply transportDD_is_transport.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
transport
  (fun ab : {x : _ & fam_gqdescent Pe x} =>
   GraphQuotient_rec
     (fun pat : {x : _ & gqd_fam Pe x} =>
      (gq pat.1; pat.2))
     (fun (a0 b0 : {x : _ & gqd_fam Pe x})
        (X : {r : R a0.1 b0.1 &
             gqd_e Pe r a0.2 = b0.2}) =>
      flatten_gqd_glue X.1 X.2)
     (sig_rec
        (gqdepdescent_rec
           {|
             gqddcs_sect :=
               fun (a : A) (x : gqd_fam Pe a) =>
               gq (a; x);
             gqddcs_e :=
               fun (a b : A) (r : R a b)
                 (pa : gqd_fam Pe a) => gqglue (r; 1)
           |}) (ab.1; ab.2)) = (ab.1; ab.2))
  (path_sigma' (fam_gqdescent Pe) (gqglue r)
     (transport_fam_gqdescent_gqglue Pe r pa)) 1 = 1
        transport_paths FFlr; apply equiv_p1_1q.H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
ap
  (GraphQuotient_rec
     (fun pat : {x : _ & gqd_fam Pe x} =>
      (gq pat.1; pat.2))
     (fun (a0 b0 : {x : _ & gqd_fam Pe x})
        (X : {r : R a0.1 b0.1 &
             gqd_e Pe r a0.2 = b0.2}) =>
      flatten_gqd_glue X.1 X.2))
  (ap
     (sig_rec
        (gqdepdescent_rec
           {|
             gqddcs_sect :=
               fun (a : A) (x : gqd_fam Pe a) =>
               gq (a; x);
             gqddcs_e :=
               fun (a b : A) (r : R a b)
                 (pa : gqd_fam Pe a) => gqglue (r; 1)
           |}))
     (path_sigma' (fam_gqdescent Pe) (gqglue r)
        (transport_fam_gqdescent_gqglue Pe r pa))) =
path_sigma' (fam_gqdescent Pe) (gqglue r)
  (transport_fam_gqdescent_gqglue Pe r pa)
        rewrite <- (concat_p1 (transport_fam_gqdescent_gqglue _ _ _)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
ap
  (GraphQuotient_rec
     (fun pat : {x : _ & gqd_fam Pe x} =>
      (gq pat.1; pat.2))
     (fun (a0 b0 : {x : _ & gqd_fam Pe x})
        (X : {r : R a0.1 b0.1 &
             gqd_e Pe r a0.2 = b0.2}) =>
      flatten_gqd_glue X.1 X.2))
  (ap
     (sig_rec
        (gqdepdescent_rec
           {|
             gqddcs_sect :=
               fun (a : A) (x : gqd_fam Pe a) =>
               gq (a; x);
             gqddcs_e :=
               fun (a b : A) (r : R a b)
                 (pa : gqd_fam Pe a) => gqglue (r; 1)
           |}))
     (path_sigma' (fam_gqdescent Pe) (gqglue r)
        (transport_fam_gqdescent_gqglue Pe r pa @ 1))) =
path_sigma' (fam_gqdescent Pe) (gqglue r)
  (transport_fam_gqdescent_gqglue Pe r pa @ 1)
        rewrite gqdepdescent_rec_beta_gqglue. (* This needs to be in the form [transport_fam_gqdescent_gqglue Pe r pa @ p] to work, and the other [@ 1] introduced comes in handy as well. *)H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
ap
  (GraphQuotient_rec
     (fun pat : {x : _ & gqd_fam Pe x} =>
      (gq pat.1; pat.2))
     (fun (a0 b0 : {x : _ & gqd_fam Pe x})
        (X : {r : R a0.1 b0.1 &
             gqd_e Pe r a0.2 = b0.2}) =>
      flatten_gqd_glue X.1 X.2))
  (gqddcs_e
     {|
       gqddcs_sect :=
         fun (a : A) (x : gqd_fam Pe a) => gq (a; x);
       gqddcs_e :=
         fun (a b : A) (r : R a b) (pa : gqd_fam Pe a)
         => gqglue (r; 1)
     |} r pa @
   ap
     (gqddcs_sect
        {|
          gqddcs_sect :=
            fun (a : A) (x : gqd_fam Pe a) =>
            gq (a; x);
          gqddcs_e :=
            fun (a b : A) (r : R a b)
              (pa : gqd_fam Pe a) => gqglue (r; 1)
        |} b) 1) =
path_sigma' (fam_gqdescent Pe) (gqglue r)
  (transport_fam_gqdescent_gqglue Pe r pa @ 1)
        lhs napply (ap _ (concat_p1 _)).H: Univalence
A: Type
R: A -> A -> Type
Pe: gqDescent R
a, b: A
r: R a b
pa: gqd_fam Pe a
ap
  (GraphQuotient_rec
     (fun pat : {x : _ & gqd_fam Pe x} =>
      (gq pat.1; pat.2))
     (fun (a0 b0 : {x : _ & gqd_fam Pe x})
        (X : {r : R a0.1 b0.1 &
             gqd_e Pe r a0.2 = b0.2}) =>
      flatten_gqd_glue X.1 X.2))
  (gqddcs_e
     {|
       gqddcs_sect :=
         fun (a : A) (x : gqd_fam Pe a) => gq (a; x);
       gqddcs_e :=
         fun (a b : A) (r : R a b) (pa : gqd_fam Pe a)
         => gqglue (r; 1)
     |} r pa) =
path_sigma' (fam_gqdescent Pe) (gqglue r)
  (transport_fam_gqdescent_gqglue Pe r pa @ 1)
        exact (GraphQuotient_rec_beta_gqglue _ _ (a; pa) (b; _) (r; 1)).
  Defined.

End Flattening.

(** ** Characterization of path spaces*)

(** A pointed type family over a graph quotient has an identity system structure precisely when its associated descent data satisfies Kraus and von Raumer's induction principle, https://arxiv.org/pdf/1901.06022. *)

Section Paths.

  (** Let [A] and [R] be a graph, with a distinguished point [a0 : A].  Let [Pe : gqDescent R] be descent data over [A] and [R] with a distinguished point [p0 : gqd_fam Pe a0].  Assume that any dependent descent data [Qe : gqDepDescent Pe] with a distinguished point [q0 : gqdd_fam Qe a0 p0] has a section that respects the distinguished points.  This is the induction principle provided by Kraus and von Raumer. *)
  Context `{Univalence} {A : Type} {R : A -> A -> Type} (a0 : A)
    (Pe : gqDescent R) (p0 : gqd_fam Pe a0)
    (based_gqdepdescent_ind : forall (Qe : gqDepDescent Pe) (q0 : gqdd_fam Qe a0 p0),
      gqDepDescentSection Qe)
    (based_gqdepdescent_ind_beta : forall (Qe : gqDepDescent Pe) (q0 : gqdd_fam Qe a0 p0),
      gqdds_sect (based_gqdepdescent_ind Qe q0) a0 p0 = q0).

  (** Under these hypotheses, we get an identity system structure on [fam_gqdescent Pe]. *)
  Local Instance idsys_flatten_gqdescent
    : @IsIdentitySystem _ (gq a0) (fam_gqdescent Pe) p0.H: Univalence
A: Type
R: A -> A -> Type
a0: A
Pe: gqDescent R
p0: gqd_fam Pe a0
based_gqdepdescent_ind: forall Qe : gqDepDescent Pe,
gqdd_fam Qe a0 p0 ->
gqDepDescentSection Qe
based_gqdepdescent_ind_beta: forall
(Qe : gqDepDescent Pe)
(q0 : gqdd_fam Qe a0 p0),
gqdds_sect
  (based_gqdepdescent_ind
     Qe q0) a0 p0 = q0
IsIdentitySystem (fam_gqdescent Pe) p0
  Proof.H: Univalence
A: Type
R: A -> A -> Type
a0: A
Pe: gqDescent R
p0: gqd_fam Pe a0
based_gqdepdescent_ind: forall Qe : gqDepDescent Pe,
gqdd_fam Qe a0 p0 ->
gqDepDescentSection Qe
based_gqdepdescent_ind_beta: forall
(Qe : gqDepDescent Pe)
(q0 : gqdd_fam Qe a0 p0),
gqdds_sect
  (based_gqdepdescent_ind
     Qe q0) a0 p0 = q0
IsIdentitySystem (fam_gqdescent Pe) p0
    snapply Build_IsIdentitySystem.H: Univalence
A: Type
R: A -> A -> Type
a0: A
Pe: gqDescent R
p0: gqd_fam Pe a0
based_gqdepdescent_ind: forall Qe : gqDepDescent Pe,
gqdd_fam Qe a0 p0 ->
gqDepDescentSection Qe
based_gqdepdescent_ind_beta: forall
(Qe : gqDepDescent Pe)
(q0 : gqdd_fam Qe a0 p0),
gqdds_sect
  (based_gqdepdescent_ind
     Qe q0) a0 p0 = q0
forall
D : forall a : GraphQuotient R,
    fam_gqdescent Pe a -> Type,
D (gq a0) p0 ->
forall (a : GraphQuotient R) (r : fam_gqdescent Pe a),
D a r
H: Univalence
A: Type
R: A -> A -> Type
a0: A
Pe: gqDescent R
p0: gqd_fam Pe a0
based_gqdepdescent_ind: forall Qe : gqDepDescent Pe,
gqdd_fam Qe a0 p0 ->
gqDepDescentSection Qe
based_gqdepdescent_ind_beta: forall
(Qe : gqDepDescent Pe)
(q0 : gqdd_fam Qe a0 p0),
gqdds_sect
  (based_gqdepdescent_ind
     Qe q0) a0 p0 = q0
forall
(D : forall a : GraphQuotient R,
     fam_gqdescent Pe a -> Type) 
(d : D (gq a0) p0), 
?idsys_ind D d (gq a0) p0 = d
    -H: Univalence
A: Type
R: A -> A -> Type
a0: A
Pe: gqDescent R
p0: gqd_fam Pe a0
based_gqdepdescent_ind: forall Qe : gqDepDescent Pe,
gqdd_fam Qe a0 p0 ->
gqDepDescentSection Qe
based_gqdepdescent_ind_beta: forall
(Qe : gqDepDescent Pe)
(q0 : gqdd_fam Qe a0 p0),
gqdds_sect
  (based_gqdepdescent_ind
     Qe q0) a0 p0 = q0
forall
D : forall a : GraphQuotient R,
    fam_gqdescent Pe a -> Type,
D (gq a0) p0 ->
forall (a : GraphQuotient R) (r : fam_gqdescent Pe a),
D a r intros Q q0 x p.H: Univalence
A: Type
R: A -> A -> Type
a0: A
Pe: gqDescent R
p0: gqd_fam Pe a0
based_gqdepdescent_ind: forall Qe : gqDepDescent Pe,
gqdd_fam Qe a0 p0 ->
gqDepDescentSection Qe
based_gqdepdescent_ind_beta: forall
(Qe : gqDepDescent Pe)
(q0 : gqdd_fam Qe a0 p0),
gqdds_sect
  (based_gqdepdescent_ind
     Qe q0) a0 p0 = q0
Q: forall a : GraphQuotient R,
fam_gqdescent Pe a -> Type
q0: Q (gq a0) p0
x: GraphQuotient R
p: fam_gqdescent Pe x
Q x p
      snapply gqdepdescent_ind.H: Univalence
A: Type
R: A -> A -> Type
a0: A
Pe: gqDescent R
p0: gqd_fam Pe a0
based_gqdepdescent_ind: forall Qe : gqDepDescent Pe,
gqdd_fam Qe a0 p0 ->
gqDepDescentSection Qe
based_gqdepdescent_ind_beta: forall
(Qe : gqDepDescent Pe)
(q0 : gqdd_fam Qe a0 p0),
gqdds_sect
  (based_gqdepdescent_ind
     Qe q0) a0 p0 = q0
Q: forall a : GraphQuotient R,
fam_gqdescent Pe a -> Type
q0: Q (gq a0) p0
x: GraphQuotient R
p: fam_gqdescent Pe x
gqDepDescentSection (gqdepdescent_fam Q)
      by apply based_gqdepdescent_ind.
    -H: Univalence
A: Type
R: A -> A -> Type
a0: A
Pe: gqDescent R
p0: gqd_fam Pe a0
based_gqdepdescent_ind: forall Qe : gqDepDescent Pe,
gqdd_fam Qe a0 p0 ->
gqDepDescentSection Qe
based_gqdepdescent_ind_beta: forall
(Qe : gqDepDescent Pe)
(q0 : gqdd_fam Qe a0 p0),
gqdds_sect
  (based_gqdepdescent_ind
     Qe q0) a0 p0 = q0
forall
(D : forall a : GraphQuotient R,
     fam_gqdescent Pe a -> Type) (d : D (gq a0) p0),
(fun
   (Q : forall a : GraphQuotient R,
        fam_gqdescent Pe a -> Type)
   (q0 : Q (gq a0) p0) (x : GraphQuotient R)
   (p : fam_gqdescent Pe x) =>
 gqdepdescent_ind
   (based_gqdepdescent_ind (gqdepdescent_fam Q) q0) x
   p) D d (gq a0) p0 = d intros Q q0; cbn.H: Univalence
A: Type
R: A -> A -> Type
a0: A
Pe: gqDescent R
p0: gqd_fam Pe a0
based_gqdepdescent_ind: forall Qe : gqDepDescent Pe,
gqdd_fam Qe a0 p0 ->
gqDepDescentSection Qe
based_gqdepdescent_ind_beta: forall
(Qe : gqDepDescent Pe)
(q0 : gqdd_fam Qe a0 p0),
gqdds_sect
  (based_gqdepdescent_ind
     Qe q0) a0 p0 = q0
Q: forall a : GraphQuotient R,
fam_gqdescent Pe a -> Type
q0: Q (gq a0) p0
gqdds_sect
  (based_gqdepdescent_ind (gqdepdescent_fam Q) q0) a0
  p0 = q0
      napply (based_gqdepdescent_ind_beta (gqdepdescent_fam Q)).
  Defined.

  (** It follows that the fibers [fam_gqdescent Pe x] are equivalent to path spaces [(gq a0) = x]. *)
  Definition fam_gqdescent_equiv_path (x : GraphQuotient R)
    : (gq a0) = x <~> fam_gqdescent Pe x
    := @equiv_transport_identitysystem _ (gq a0) (fam_gqdescent Pe) p0 _ x.

End Paths.

(** ** Functoriality of graph quotients *)

Lemma functor_gq {A B : Type} (f : A -> B)
  {R : A -> A -> Type} {S : B -> B -> Type} (e : forall a b, R a b -> S (f a) (f b))
  : GraphQuotient R -> GraphQuotient S.A, B: Type
f: A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
GraphQuotient R -> GraphQuotient S
Proof.A, B: Type
f: A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
GraphQuotient R -> GraphQuotient S
  snapply GraphQuotient_rec.A, B: Type
f: A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
A -> GraphQuotient S
A, B: Type
f: A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
forall a b : A, R a b -> ?c a = ?c b
  1: exact (fun x => gq (f x)).A, B: Type
f: A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
forall a b : A,
R a b ->
(fun x : A => gq (f x)) a = (fun x : A => gq (f x)) b
  intros a b r.A, B: Type
f: A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
a, b: A
r: R a b
(fun x : A => gq (f x)) a = (fun x : A => gq (f x)) b
  apply gqglue.A, B: Type
f: A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
a, b: A
r: R a b
S (f a) (f b)
  apply e.A, B: Type
f: A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
a, b: A
r: R a b
R a b
  exact r.
Defined.

Definition functor_gq_beta_gqglue {A B : Type} (f : A -> B)
  {R : A -> A -> Type} {S : B -> B -> Type}
  (e : forall a b, R a b -> S (f a) (f b))
  {a b : A} (s : R a b)
  : ap (functor_gq f e) (gqglue s) = gqglue (e a b s)
  := GraphQuotient_rec_beta_gqglue _ _ _ _ _.

Lemma functor_gq_idmap {A : Type} {R : A -> A -> Type}
  : functor_gq (A:=A) (B:=A) (S:=R) idmap (fun a b r => r) == idmap.A: Type
R: A -> A -> Type
functor_gq idmap (fun a b : A => idmap) == idmap
Proof.A: Type
R: A -> A -> Type
functor_gq idmap (fun a b : A => idmap) == idmap
  snapply GraphQuotient_ind.A: Type
R: A -> A -> Type
forall a : A,
(fun
   x : GraphQuotient
         (fun a0 b : A => R (idmap a0) (idmap b)) =>
 functor_gq idmap (fun a0 b : A => idmap) x = idmap x)
  (gq a)
A: Type
R: A -> A -> Type
forall (a b : A)
(s : (fun a0 b0 : A => R (idmap a0) (idmap b0)) a b),
transport
  (fun
     x : GraphQuotient
           (fun a0 b0 : A => R (idmap a0) (idmap b0))
   =>
   functor_gq idmap (fun a0 b0 : A => idmap) x =
   idmap x) (gqglue s) (?gq' a) = ?gq' b
  1: reflexivity.A: Type
R: A -> A -> Type
forall (a b : A)
(s : (fun a0 b0 : A => R (idmap a0) (idmap b0)) a b),
transport
  (fun
     x : GraphQuotient
           (fun a0 b0 : A => R (idmap a0) (idmap b0))
   =>
   functor_gq idmap (fun a0 b0 : A => idmap) x =
   idmap x) (gqglue s) ((fun a0 : A => 1) a) =
(fun a0 : A => 1) b
  intros a b r.A: Type
R: A -> A -> Type
a, b: A
r: (fun a b : A => R (idmap a) (idmap b)) a b
transport
  (fun
     x : GraphQuotient
           (fun a b : A => R (idmap a) (idmap b)) =>
   functor_gq idmap (fun a b : A => idmap) x = idmap x)
  (gqglue r) ((fun a : A => 1) a) = (fun a : A => 1) b
  transport_paths Flr.A: Type
R: A -> A -> Type
a, b: A
r: (fun a b : A => R (idmap a) (idmap b)) a b
ap (functor_gq idmap (fun a b : A => idmap))
  (gqglue r) @ 1 = 1 @ gqglue r
  apply equiv_p1_1q.A: Type
R: A -> A -> Type
a, b: A
r: (fun a b : A => R (idmap a) (idmap b)) a b
ap (functor_gq idmap (fun a b : A => idmap))
  (gqglue r) = gqglue r
  napply GraphQuotient_rec_beta_gqglue.
Defined.

Lemma functor_gq_compose {A B C : Type} (f : A -> B) (g : B -> C)
  {R : A -> A -> Type} {S : B -> B -> Type} {T : C -> C -> Type}
  (e : forall a b, R a b -> S (f a) (f b)) (e' : forall a b, S a b -> T (g a) (g b))
  : functor_gq g e' o (functor_gq f e) == functor_gq (g o f) (fun a b r => e' _ _ (e _ _ r)).A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
functor_gq g e' o functor_gq f e ==
functor_gq (g o f)
  (fun (a b : A) (r : (fun a0 b0 : A => R a0 b0) a b)
   => e' (f a) (f b) (e a b r))
Proof.A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
functor_gq g e' o functor_gq f e ==
functor_gq (g o f)
  (fun (a b : A) (r : (fun a0 b0 : A => R a0 b0) a b)
   => e' (f a) (f b) (e a b r))
  snapply GraphQuotient_ind.A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
forall a : A,
(fun x : GraphQuotient R =>
 (functor_gq g e' o functor_gq f e) x =
 functor_gq (g o f)
   (fun (a0 b : A)
      (r : (fun a1 b0 : A => R a1 b0) a0 b) =>
    e' (f a0) (f b) (e a0 b r)) x) (gq a)
A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R =>
   (functor_gq g e' o functor_gq f e) x =
   functor_gq (g o f)
     (fun (a0 b0 : A)
        (r : (fun a1 b1 : A => R a1 b1) a0 b0) =>
      e' (f a0) (f b0) (e a0 b0 r)) x) (gqglue s)
  (?gq' a) = ?gq' b
  1: reflexivity.A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R =>
   (functor_gq g e' o functor_gq f e) x =
   functor_gq (g o f)
     (fun (a0 b0 : A)
        (r : (fun a1 b1 : A => R a1 b1) a0 b0) =>
      e' (f a0) (f b0) (e a0 b0 r)) x) (gqglue s)
  ((fun a0 : A => 1) a) = (fun a0 : A => 1) b
  intros a b s; cbn beta.A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
a, b: A
s: R a b
transport
  (fun x : GraphQuotient R =>
   functor_gq g e' (functor_gq f e x) =
   functor_gq (fun x0 : A => g (f x0))
     (fun (a b : A) (r : R a b) =>
      e' (f a) (f b) (e a b r)) x) (gqglue s) 1 = 1
  transport_paths FFlFr.A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
a, b: A
s: R a b
ap (functor_gq g e') (ap (functor_gq f e) (gqglue s)) @
1 =
1 @
ap
  (functor_gq (fun x : A => g (f x))
     (fun (a b : A) (r : R a b) =>
      e' (f a) (f b) (e a b r))) (gqglue s)
  apply equiv_p1_1q.A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
a, b: A
s: R a b
ap (functor_gq g e') (ap (functor_gq f e) (gqglue s)) =
ap
  (functor_gq (fun x : A => g (f x))
     (fun (a b : A) (r : R a b) =>
      e' (f a) (f b) (e a b r))) (gqglue s)
  lhs napply ap.A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
a, b: A
s: R a b
ap (functor_gq f e) (gqglue s) = ?Goal
A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
a, b: A
s: R a b
ap (functor_gq g e') ?Goal =
ap
  (functor_gq (fun x : A => g (f x))
     (fun (a b : A) (r : R a b) =>
      e' (f a) (f b) (e a b r))) (gqglue s)
  1: apply functor_gq_beta_gqglue.A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
a, b: A
s: R a b
ap (functor_gq g e') (gqglue (e a b s)) =
ap
  (functor_gq (fun x : A => g (f x))
     (fun (a b : A) (r : R a b) =>
      e' (f a) (f b) (e a b r))) (gqglue s)
  rhs napply (functor_gq_beta_gqglue (g o f)).A, B, C: Type
f: A -> B
g: B -> C
R: A -> A -> Type
S: B -> B -> Type
T: C -> C -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : B, S a b -> T (g a) (g b)
a, b: A
s: R a b
ap (functor_gq g e') (gqglue (e a b s)) =
gqglue (e' (f a) (f b) (e a b s))
  napply (functor_gq_beta_gqglue g).
Defined.

Lemma functor2_gq {A B : Type} (f f' : A -> B)
  {R : A -> A -> Type} {S : B -> B -> Type}
  (e : forall a b, R a b -> S (f a) (f b)) (e' : forall a b, R a b -> S (f' a) (f' b))
  (p : f == f')
  (q : forall a b r, transport011 S (p a) (p b) (e a b r) = e' a b r)
  : functor_gq f e == functor_gq f' e'.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
functor_gq f e == functor_gq f' e'
Proof.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
functor_gq f e == functor_gq f' e'
  snapply GraphQuotient_ind.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
forall a : A,
(fun x : GraphQuotient R =>
 functor_gq f e x = functor_gq f' e' x) (gq a)
A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R =>
   functor_gq f e x = functor_gq f' e' x) (gqglue s)
  (?gq' a) = ?gq' b
  -A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
forall a : A,
(fun x : GraphQuotient R =>
 functor_gq f e x = functor_gq f' e' x) (gq a) simpl; intro.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a: A
gq (f a) = gq (f' a)
    apply ap.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a: A
f a = f' a
    apply p.
  -A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R =>
   functor_gq f e x = functor_gq f' e' x) (gqglue s)
  (((fun a0 : A => ap gq (p a0))
    :
    forall a0 : A,
    (fun x : GraphQuotient R =>
     functor_gq f e x = functor_gq f' e' x) (gq a0)) a) =
((fun a0 : A => ap gq (p a0))
 :
 forall a0 : A,
 (fun x : GraphQuotient R =>
  functor_gq f e x = functor_gq f' e' x) (gq a0)) b intros a b s; simpl.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
transport
  (fun x : GraphQuotient R =>
   functor_gq f e x = functor_gq f' e' x) (gqglue s)
  (ap gq (p a)) = ap gq (p b)
    transport_paths (transport_paths_FlFr (gqglue s)).A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
ap (functor_gq f e) (gqglue s) @ ap gq (p b) =
ap gq (p a) @ ap (functor_gq f' e') (gqglue s)
    rhs napply whiskerL.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
ap (functor_gq f e) (gqglue s) @ ap gq (p b) =
ap gq (p a) @ ?Goal
A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
ap (functor_gq f' e') (gqglue s) = ?Goal
    2: napply functor_gq_beta_gqglue.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
ap (functor_gq f e) (gqglue s) @ ap gq (p b) =
ap gq (p a) @ gqglue (e' a b s)
    lhs napply whiskerR.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
ap (functor_gq f e) (gqglue s) = ?Goal
A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
?Goal @ ap gq (p b) = ap gq (p a) @ gqglue (e' a b s)
    1: napply functor_gq_beta_gqglue.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
gqglue (e a b s) @ ap gq (p b) =
ap gq (p a) @ gqglue (e' a b s)
    apply moveL_Mp.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
(ap gq (p a))^ @ (gqglue (e a b s) @ ap gq (p b)) =
gqglue (e' a b s)
    symmetry.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
gqglue (e' a b s) =
(ap gq (p a))^ @ (gqglue (e a b s) @ ap gq (p b))
    destruct (q a b s).A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
gqglue (transport011 S (p a) (p b) (e a b s)) =
(ap gq (p a))^ @ (gqglue (e a b s) @ ap gq (p b))
    lhs napply (ap_transport011 _ _ (fun s _ => gqglue)).A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
transport011 (fun s H : B => gq s = gq H) (p a) (p b)
  (gqglue (e a b s)) =
(ap gq (p a))^ @ (gqglue (e a b s) @ ap gq (p b))
    rhs napply concat_p_pp.A, B: Type
f, f': A -> B
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
e': forall a b : A, R a b -> S (f' a) (f' b)
p: f == f'
q: forall (a b : A) (r : R a b),
transport011 S (p a) (p b) (e a b r) = e' a b r
a, b: A
s: R a b
transport011 (fun s H : B => gq s = gq H) (p a) (p b)
  (gqglue (e a b s)) =
((ap gq (p a))^ @ gqglue (e a b s)) @ ap gq (p b)
    napply transport011_paths.
Defined.

(** ** Equivalence of graph quotients *)

Instance isequiv_functor_gq {A B : Type} (f : A -> B) `{IsEquiv _ _ f}
  {R : A -> A -> Type} {S : B -> B -> Type} (e : forall a b, R a b -> S (f a) (f b))
  `{forall a b, IsEquiv (e a b)}
  : IsEquiv (functor_gq f e).A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
IsEquiv (functor_gq f e)
Proof.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
IsEquiv (functor_gq f e)
  srapply isequiv_adjointify.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
GraphQuotient S -> GraphQuotient R
A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
functor_gq f e o ?g == idmap
A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
?g o functor_gq f e == idmap
  -A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
GraphQuotient S -> GraphQuotient R napply (functor_gq f^-1).A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
forall a b : B, S a b -> R (f^-1 a) (f^-1 b)
    intros a b s.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
a, b: B
s: S a b
R (f^-1 a) (f^-1 b)
    apply (e _ _)^-1.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
a, b: B
s: S a b
S (f (f^-1 a)) (f (f^-1 b))
    exact (transport011 S (eisretr f a)^ (eisretr f b)^ s).
  -A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
functor_gq f e
o functor_gq f^-1
    (fun (a b : B) (s : S a b) =>
     (e (f^-1 a) (f^-1 b))^-1
       (transport011 S (eisretr f a)^ (eisretr f b)^ s)) ==
idmap intros x.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient S
functor_gq f e
  (functor_gq f^-1
     (fun (a b : B) (s : S a b) =>
      (e (f^-1 a) (f^-1 b))^-1
        (transport011 S (eisretr f a)^ (eisretr f b)^
           s)) x) = x
    lhs napply functor_gq_compose.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient S
functor_gq (fun x : B => f (f^-1 x))
  (fun (a b : B) (r : S a b) =>
   e (f^-1 a) (f^-1 b)
     ((e (f^-1 a) (f^-1 b))^-1
        (transport011 S (eisretr f a)^ (eisretr f b)^
           r))) x = x
    rhs_V napply functor_gq_idmap.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient S
functor_gq (fun x : B => f (f^-1 x))
  (fun (a b : B) (r : S a b) =>
   e (f^-1 a) (f^-1 b)
     ((e (f^-1 a) (f^-1 b))^-1
        (transport011 S (eisretr f a)^ (eisretr f b)^
           r))) x =
functor_gq idmap (fun a b : B => idmap) x
    snapply functor2_gq; cbn beta.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient S
(fun x : B => f (f^-1 x)) == idmap
A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient S
forall (a b : B) (r : S a b),
transport011 S (?Goal0 a) (?Goal0 b)
  (e (f^-1 a) (f^-1 b)
     ((e (f^-1 a) (f^-1 b))^-1
        (transport011 S (eisretr f a)^ (eisretr f b)^
           r))) = r
    1: apply eisretr.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient S
forall (a b : B) (r : S a b),
transport011 S (eisretr f a) (eisretr f b)
  (e (f^-1 a) (f^-1 b)
     ((e (f^-1 a) (f^-1 b))^-1
        (transport011 S (eisretr f a)^ (eisretr f b)^
           r))) = r
    intros a b s.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient S
a, b: B
s: S a b
transport011 S (eisretr f a) (eisretr f b)
  (e (f^-1 a) (f^-1 b)
     ((e (f^-1 a) (f^-1 b))^-1
        (transport011 S (eisretr f a)^ (eisretr f b)^
           s))) = s
    rewrite (eisretr (e (f^-1 a) (f^-1 b))).A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient S
a, b: B
s: S a b
transport011 S (eisretr f a) (eisretr f b)
  (transport011 S (eisretr f a)^ (eisretr f b)^ s) = s
    lhs_V napply transport011_pp.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient S
a, b: B
s: S a b
transport011 S ((eisretr f a)^ @ eisretr f a)
  ((eisretr f b)^ @ eisretr f b) s = s
    by rewrite 2 concat_Vp.
  -A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
functor_gq f^-1
  (fun (a b : B) (s : S a b) =>
   (e (f^-1 a) (f^-1 b))^-1
     (transport011 S (eisretr f a)^ (eisretr f b)^ s))
o functor_gq f e == idmap intros x.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
functor_gq f^-1
  (fun (a b : B) (s : S a b) =>
   (e (f^-1 a) (f^-1 b))^-1
     (transport011 S (eisretr f a)^ (eisretr f b)^ s))
  (functor_gq f e x) = x
    lhs napply functor_gq_compose.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
functor_gq (fun x : A => f^-1 (f x))
  (fun (a b : A) (r : R a b) =>
   (e (f^-1 (f a)) (f^-1 (f b)))^-1
     (transport011 S (eisretr f (f a))^
        (eisretr f (f b))^ (e a b r))) x = x
    rhs_V napply functor_gq_idmap.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
functor_gq (fun x : A => f^-1 (f x))
  (fun (a b : A) (r : R a b) =>
   (e (f^-1 (f a)) (f^-1 (f b)))^-1
     (transport011 S (eisretr f (f a))^
        (eisretr f (f b))^ (e a b r))) x =
functor_gq idmap (fun a b : A => idmap) x
    snapply functor2_gq; cbn beta.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
(fun x : A => f^-1 (f x)) == idmap
A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
forall (a b : A) (r : R a b),
transport011 R (?Goal a) (?Goal b)
  ((e (f^-1 (f a)) (f^-1 (f b)))^-1
     (transport011 S (eisretr f (f a))^
        (eisretr f (f b))^ (e a b r))) = r
    1: apply eissect.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
forall (a b : A) (r : R a b),
transport011 R (eissect f a) (eissect f b)
  ((e (f^-1 (f a)) (f^-1 (f b)))^-1
     (transport011 S (eisretr f (f a))^
        (eisretr f (f b))^ (e a b r))) = r
    intros a b r.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
a, b: A
r: R a b
transport011 R (eissect f a) (eissect f b)
  ((e (f^-1 (f a)) (f^-1 (f b)))^-1
     (transport011 S (eisretr f (f a))^
        (eisretr f (f b))^ (e a b r))) = r
    rewrite 2 eisadj.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
a, b: A
r: R a b
transport011 R (eissect f a) (eissect f b)
  ((e (f^-1 (f a)) (f^-1 (f b)))^-1
     (transport011 S (ap f (eissect f a))^
        (ap f (eissect f b))^ (e a b r))) = r
    rewrite <- 2 ap_V.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
a, b: A
r: R a b
transport011 R (eissect f a) (eissect f b)
  ((e (f^-1 (f a)) (f^-1 (f b)))^-1
     (transport011 S (ap f (eissect f a)^)
        (ap f (eissect f b)^) (e a b r))) = r
    rewrite <- (transport011_compose S).A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
a, b: A
r: R a b
transport011 R (eissect f a) (eissect f b)
  ((e (f^-1 (f a)) (f^-1 (f b)))^-1
     (transport011 (fun x y : A => S (f x) (f y))
        (eissect f a)^ (eissect f b)^ (e a b r))) = r
    rewrite <- (ap_transport011 (Q := fun x y => S (f x) (f y)) (eissect f a)^ (eissect f b)^ e).A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
a, b: A
r: R a b
transport011 R (eissect f a) (eissect f b)
  ((e (f^-1 (f a)) (f^-1 (f b)))^-1
     (e (f^-1 (f a)) (f^-1 (f b))
        (transport011 R (eissect f a)^ (eissect f b)^
           r))) = r
    rewrite (eissect (e (f^-1 (f a)) (f^-1 (f b)))).A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
a, b: A
r: R a b
transport011 R (eissect f a) (eissect f b)
  (transport011 R (eissect f a)^ (eissect f b)^ r) = r
    lhs_V napply transport011_pp.A, B: Type
f: A -> B
H: IsEquiv f
R: A -> A -> Type
S: B -> B -> Type
e: forall a b : A, R a b -> S (f a) (f b)
H0: forall a b : A, IsEquiv (e a b)
x: GraphQuotient R
a, b: A
r: R a b
transport011 R ((eissect f a)^ @ eissect f a)
  ((eissect f b)^ @ eissect f b) r = r
    by rewrite 2 concat_Vp.
Defined.

Definition equiv_functor_gq {A B : Type} (f : A <~> B)
  (R : A -> A -> Type) (S : B -> B -> Type) (e : forall a b, R a b <~> S (f a) (f b))
  : GraphQuotient R <~> GraphQuotient S
  := Build_Equiv _ _ (functor_gq f e) _.