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.Arrow Types.Sigma Cubical.DPath.

(** * 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
  refine (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.

(** ** The flattening lemma *)

(** Univalence tells us that type families over a colimit correspond to cartesian families over the indexing diagram.  The flattening lemma gives an explicit description of the family over a colimit that corresponds to a given cartesian family, again using univalence.  Together, these are known as descent, a fundamental result in higher topos theory which has many implications. *)

Section Flattening.

  Context `{Univalence} {A : Type} {R : A -> A -> Type}.
  (** We consider a type family over [A] which is "equifibrant" or "cartesian": the fibers are equivalent when the base points are related by [R]. *)
  Context (F : A -> Type) (e : forall x y, R x y -> F x <~> F y).

  (** By univalence, the equivalences give equalities, which means that [F] induces a map on the quotient. *)
  Definition DGraphQuotient : GraphQuotient R -> Type
    := GraphQuotient_rec F (fun x y s => path_universe (e x y s)).

  (** The transport of [DGraphQuotient] along [gqglue] equals the equivalence [e] applied to the original point. This lemma is required a few times in the following proofs. *)
  Definition transport_DGraphQuotient {x y} (s : R x y) (a : F x)
    : transport DGraphQuotient (gqglue s) a = e x y s a.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
transport DGraphQuotient (gqglue s) a = e x y s a
  Proof.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
transport DGraphQuotient (gqglue s) a = e x y s a
    lhs nrapply transport_idmap_ap.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
transport idmap (ap DGraphQuotient (gqglue s)) a =
e x y s a
    lhs nrapply (transport2 idmap).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
ap DGraphQuotient (gqglue s) = ?Goal
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
transport idmap ?Goal a = e x y s a
    1: apply GraphQuotient_rec_beta_gqglue.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
transport idmap (path_universe (e x y s)) a =
e x y s a
    rapply transport_path_universe.
  Defined.

  (** The family [DGraphQuotient] we have defined over [GraphQuotient R] has a total space which we will describe as a [GraphQuotient] of [sig F] by an appropriate relation. *)

  (** We mimic the constructors of [GraphQuotient] for the total space. Here is the point constructor. *)
  Definition flatten_gq {x} : F x -> sig DGraphQuotient.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x: A
F x -> {x : _ & DGraphQuotient x}
  Proof.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x: A
F x -> {x : _ & DGraphQuotient x}
    intros p.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x: A
p: F x
{x : _ & DGraphQuotient x}
    exact (gq x; p).
  Defined.

  (** And here is the path constructor. *)
  Definition flatten_gqglue {x y} (s : R x y) (a : F x)
    : flatten_gq a = flatten_gq (e x y s a).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
flatten_gq a = flatten_gq (e x y s a)
  Proof.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
flatten_gq a = flatten_gq (e x y s a)
    snrapply path_sigma'.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
gq x = gq y
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
transport DGraphQuotient ?p a = e x y s a
    -
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
gq x = gq y by apply gqglue.
    -
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
transport DGraphQuotient (gqglue s) a = e x y s a apply transport_DGraphQuotient.
  Defined.

  (** This lemma is the same as [transport_DGraphQuotient] but adapted instead for [DPath]. The use of [DPath] will be apparent there. *)
  Lemma equiv_dp_dgraphquotient (x y : A) (s : R x y) (a : F x) (b : F y)
    : DPath DGraphQuotient (gqglue s) a b <~> (e x y s a = b).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
b: F y
DPath DGraphQuotient (gqglue s) a b <~> e x y s a = b
  Proof.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
b: F y
DPath DGraphQuotient (gqglue s) a b <~> e x y s a = b
    refine (equiv_concat_l _^ _).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
x, y: A
s: R x y
a: F x
b: F y
transport DGraphQuotient (gqglue s) a = e x y s a
    apply transport_DGraphQuotient.
  Defined.

  (** We can also prove an induction principle for [sig DGraphQuotient]. We won't show that it satisfies the relevant computation rules as these will not be needed. Instead we will prove the non-dependent eliminator directly so that we can better reason about it. In order to get through the path algebra here, we have opted to use dependent paths. This makes the reasoning slightly easier, but it should not matter too much. *)
  Definition flatten_ind {Q : sig DGraphQuotient -> Type}
    (Qgq : forall a (x : F a), Q (flatten_gq x))
    (Qgqglue : forall a b (s : R a b) (x : F a),
      flatten_gqglue s x # Qgq _ x = Qgq _ (e _ _ _ x))
    : forall x, Q x.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
forall x : {x : _ & DGraphQuotient x}, Q x
  Proof.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
forall x : {x : _ & DGraphQuotient x}, Q x
    apply sig_ind.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
forall (proj1 : GraphQuotient R)
(proj2 : DGraphQuotient proj1), Q (proj1; proj2)
    snrapply GraphQuotient_ind.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
forall a : A,
(fun x : GraphQuotient R =>
 forall proj2 : DGraphQuotient x, Q (x; proj2)) (gq a)
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R =>
   forall proj2 : DGraphQuotient x, Q (x; proj2))
  (gqglue s) (?gq' a) = 
?gq' b
    1: exact Qgq.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R =>
   forall proj2 : DGraphQuotient x, Q (x; proj2))
  (gqglue s) (Qgq a) = Qgq b
    intros a b s.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
transport
  (fun x : GraphQuotient R =>
   forall proj2 : DGraphQuotient x, Q (x; proj2))
  (gqglue s) (Qgq a) = Qgq b
    apply dp_forall.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
forall (x : DGraphQuotient (gq a))
(y : DGraphQuotient (gq b))
(q : DPath DGraphQuotient (gqglue s) x y),
DPath Q (path_sigma_dp (gqglue s; q)) (Qgq a x)
  (Qgq b y)
    intros x y.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
y: DGraphQuotient (gq b)
forall q : DPath DGraphQuotient (gqglue s) x y,
DPath Q (path_sigma_dp (gqglue s; q)) (Qgq a x)
  (Qgq b y)
    srapply (equiv_ind (equiv_dp_dgraphquotient a b s x y)^-1).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
y: DGraphQuotient (gq b)
forall x0 : e a b s x = y,
(fun y0 : DPath DGraphQuotient (gqglue s) x y =>
 DPath Q (path_sigma_dp (gqglue s; y0)) (Qgq a x)
   (Qgq b y))
  ((transitivity (transport_DGraphQuotient s x)^)^-1
     x0)
    intros q.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
y: DGraphQuotient (gq b)
q: e a b s x = y
(fun y0 : DPath DGraphQuotient (gqglue s) x y =>
 DPath Q (path_sigma_dp (gqglue s; y0)) (Qgq a x)
   (Qgq b y))
  ((transitivity (transport_DGraphQuotient s x)^)^-1 q)
    destruct q.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
DPath Q
  (path_sigma_dp
     (gqglue s;
     (transitivity (transport_DGraphQuotient s x)^)^-1
       1)) (Qgq a x) (Qgq b (e a b s x))
    refine (transport2 _ _ _ @ Qgqglue a b s x).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
path_sigma_dp
  (gqglue s;
  (transitivity (transport_DGraphQuotient s x)^)^-1 1) =
flatten_gqglue s x
    refine (ap (path_sigma_uncurried DGraphQuotient _ _) _).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
(gqglue s;
(transitivity (transport_DGraphQuotient s x)^)^-1 1) =
(gqglue s; transport_DGraphQuotient s x)
    snrapply path_sigma.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
(gqglue s;
(transitivity (transport_DGraphQuotient s x)^)^-1 1).1 =
(gqglue s; transport_DGraphQuotient s x).1
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
transport
  (fun
     p : (flatten_gq x).1 = (flatten_gq (e a b s x)).1
   =>
   transport DGraphQuotient p (flatten_gq x).2 =
   (flatten_gq (e a b s x)).2) 
  ?p
  (gqglue s;
  (transitivity (transport_DGraphQuotient s x)^)^-1 1).2 =
(gqglue s; transport_DGraphQuotient s x).2
    1: reflexivity.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
transport
  (fun
     p : (flatten_gq x).1 = (flatten_gq (e a b s x)).1
   =>
   transport DGraphQuotient p (flatten_gq x).2 =
   (flatten_gq (e a b s x)).2) 1
  (gqglue s;
  (transitivity (transport_DGraphQuotient s x)^)^-1 1).2 =
(gqglue s; transport_DGraphQuotient s x).2
    lhs nrapply concat_p1.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: {x : _ & DGraphQuotient x} -> Type
Qgq: forall (a : A) (x : F a), Q (flatten_gq x)
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a),
transport Q (flatten_gqglue s x) (Qgq a x) =
Qgq b (e a b s x)
a, b: A
s: R a b
x: DGraphQuotient (gq a)
((transport_DGraphQuotient s x)^)^ =
(gqglue s; transport_DGraphQuotient s x).2
    apply inv_V.
  Defined.

  (** Rather than use [flatten_ind] to define [flatten_rec] we reprove this simple case. This means we can later reason about it and derive the computation rules easily. The full computation rule for [flatten_ind] takes some work to derive and is not actually needed. *)
  Definition flatten_rec {Q : Type} (Qgq : forall a, F a -> Q)
    (Qgqglue : forall a b (s : R a b) (x : F a), Qgq a x = Qgq b (e _ _ s x))
    : sig DGraphQuotient -> Q.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
{x : _ & DGraphQuotient x} -> Q
  Proof.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
{x : _ & DGraphQuotient x} -> Q
    apply sig_rec.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
forall proj1 : GraphQuotient R,
DGraphQuotient proj1 -> Q
    snrapply GraphQuotient_ind.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
forall a : A,
(fun x : GraphQuotient R => DGraphQuotient x -> Q)
  (gq a)
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R => DGraphQuotient x -> Q)
  (gqglue s) (?gq' a) = 
?gq' b
    1: exact Qgq.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
forall (a b : A) (s : R a b),
transport
  (fun x : GraphQuotient R => DGraphQuotient x -> Q)
  (gqglue s) (Qgq a) = Qgq b
    intros a b s.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
a, b: A
s: R a b
transport
  (fun x : GraphQuotient R => DGraphQuotient x -> Q)
  (gqglue s) (Qgq a) = Qgq b
    nrapply dpath_arrow.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
a, b: A
s: R a b
forall y1 : DGraphQuotient (gq a),
transport (fun _ : GraphQuotient R => Q) (gqglue s)
  (Qgq a y1) =
Qgq b (transport DGraphQuotient (gqglue s) y1)
    intros y.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
a, b: A
s: R a b
y: DGraphQuotient (gq a)
transport (fun _ : GraphQuotient R => Q) (gqglue s)
  (Qgq a y) =
Qgq b (transport DGraphQuotient (gqglue s) y)
    lhs nrapply transport_const.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
a, b: A
s: R a b
y: DGraphQuotient (gq a)
Qgq a y =
Qgq b (transport DGraphQuotient (gqglue s) y)
    lhs nrapply (Qgqglue a b s).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
a, b: A
s: R a b
y: DGraphQuotient (gq a)
Qgq b (e a b s y) =
Qgq b (transport DGraphQuotient (gqglue s) y)
    f_ap; symmetry.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (s : R a b) 
(x : F a), Qgq a x = Qgq b (e a b s x)
a, b: A
s: R a b
y: DGraphQuotient (gq a)
transport DGraphQuotient (gqglue s) y = e a b s y
    apply transport_DGraphQuotient.
  Defined.

  (** The non-dependent eliminator computes as expected on our "path constructor". *) 
  Definition flatten_rec_beta_gqglue {Q : Type} (Qgq : forall a, F a -> Q)
    (Qgqglue : forall a b (r : R a b) (x : F a), Qgq a x = Qgq b (e _ _ r x))
    (a b : A) (s : R a b) (x : F a)
    : ap (flatten_rec Qgq Qgqglue) (flatten_gqglue s x) = Qgqglue a b s x.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
ap (flatten_rec Qgq Qgqglue) (flatten_gqglue s x) =
Qgqglue a b s x
  Proof.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
ap (flatten_rec Qgq Qgqglue) (flatten_gqglue s x) =
Qgqglue a b s x
    lhs nrapply ap_sig_rec_path_sigma; cbn.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
((((transport_const (gqglue s) (Qgq a x))^ @
   (ap
      (fun x : F a =>
       transport (fun _ : GraphQuotient R => Q)
         (gqglue s) (Qgq a x))
      (transport_Vp DGraphQuotient (gqglue s) x))^) @
  (transport_arrow (gqglue s) (Qgq a)
     (transport DGraphQuotient (gqglue s) x))^) @
 ap10
   (apD
      (GraphQuotient_ind
         (fun x : GraphQuotient R =>
          DGraphQuotient x -> Q) Qgq
         (fun (a b : A) (s : R a b) =>
          dpath_arrow DGraphQuotient
            (fun _ : GraphQuotient R => Q) (gqglue s)
            (Qgq a) (Qgq b)
            (fun y : F a =>
             transport_const (gqglue s) (Qgq a y) @
             (Qgqglue a b s y @
              match
                (transport_DGraphQuotient s y)^ in
                (_ = a0)
                return (Qgq b (e a b s y) = Qgq b a0)
              with
              | 1 => 1
              end)))) (gqglue s))
   (transport DGraphQuotient (gqglue s) x)) @
ap (Qgq b) (transport_DGraphQuotient s x) =
Qgqglue a b s x
    lhs nrapply (ap (fun x => x @ _)).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(((transport_const (gqglue s) (Qgq a x))^ @
  (ap
     (fun x : F a =>
      transport (fun _ : GraphQuotient R => Q)
        (gqglue s) (Qgq a x))
     (transport_Vp DGraphQuotient (gqglue s) x))^) @
 (transport_arrow (gqglue s) (Qgq a)
    (transport DGraphQuotient (gqglue s) x))^) @
ap10
  (apD
     (GraphQuotient_ind
        (fun x : GraphQuotient R =>
         DGraphQuotient x -> Q) Qgq
        (fun (a b : A) (s : R a b) =>
         dpath_arrow DGraphQuotient
           (fun _ : GraphQuotient R => Q) (gqglue s)
           (Qgq a) (Qgq b)
           (fun y : F a =>
            transport_const (gqglue s) (Qgq a y) @
            (Qgqglue a b s y @
             match
               (transport_DGraphQuotient s y)^ in
               (_ = a0)
               return (Qgq b (e a b s y) = Qgq b a0)
             with
             | 1 => 1
             end)))) (gqglue s))
  (transport DGraphQuotient (gqglue s) x) = ?Goal
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
?Goal @ ap (Qgq b) (transport_DGraphQuotient s x) =
Qgqglue a b s x
    {
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(((transport_const (gqglue s) (Qgq a x))^ @
  (ap
     (fun x : F a =>
      transport (fun _ : GraphQuotient R => Q)
        (gqglue s) (Qgq a x))
     (transport_Vp DGraphQuotient (gqglue s) x))^) @
 (transport_arrow (gqglue s) (Qgq a)
    (transport DGraphQuotient (gqglue s) x))^) @
ap10
  (apD
     (GraphQuotient_ind
        (fun x : GraphQuotient R =>
         DGraphQuotient x -> Q) Qgq
        (fun (a b : A) (s : R a b) =>
         dpath_arrow DGraphQuotient
           (fun _ : GraphQuotient R => Q) (gqglue s)
           (Qgq a) (Qgq b)
           (fun y : F a =>
            transport_const (gqglue s) (Qgq a y) @
            (Qgqglue a b s y @
             match
               (transport_DGraphQuotient s y)^ in
               (_ = a0)
               return (Qgq b (e a b s y) = Qgq b a0)
             with
             | 1 => 1
             end)))) (gqglue s))
  (transport DGraphQuotient (gqglue s) x) = ?Goal nrapply ap.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
ap10
  (apD
     (GraphQuotient_ind
        (fun x : GraphQuotient R =>
         DGraphQuotient x -> Q) Qgq
        (fun (a b : A) (s : R a b) =>
         dpath_arrow DGraphQuotient
           (fun _ : GraphQuotient R => Q) (gqglue s)
           (Qgq a) (Qgq b)
           (fun y : F a =>
            transport_const (gqglue s) (Qgq a y) @
            (Qgqglue a b s y @
             match
               (transport_DGraphQuotient s y)^ in
               (_ = a0)
               return (Qgq b (e a b s y) = Qgq b a0)
             with
             | 1 => 1
             end)))) (gqglue s))
  (transport DGraphQuotient (gqglue s) x) = ?Goal0
      nrapply (ap01 (fun x => ap10 x _)).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
apD
  (GraphQuotient_ind
     (fun x : GraphQuotient R => DGraphQuotient x -> Q)
     Qgq
     (fun (a b : A) (s : R a b) =>
      dpath_arrow DGraphQuotient
        (fun _ : GraphQuotient R => Q) (gqglue s)
        (Qgq a) (Qgq b)
        (fun y : F a =>
         transport_const (gqglue s) (Qgq a y) @
         (Qgqglue a b s y @
          match
            (transport_DGraphQuotient s y)^ in
            (_ = a0)
            return (Qgq b (e a b s y) = Qgq b a0)
          with
          | 1 => 1
          end)))) (gqglue s) = ?Goal0
      nrapply GraphQuotient_ind_beta_gqglue. }
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
((((transport_const (gqglue s) (Qgq a x))^ @
   (ap
      (fun x : F a =>
       transport (fun _ : GraphQuotient R => Q)
         (gqglue s) (Qgq a x))
      (transport_Vp DGraphQuotient (gqglue s) x))^) @
  (transport_arrow (gqglue s) (Qgq a)
     (transport DGraphQuotient (gqglue s) x))^) @
 ap10
   (dpath_arrow DGraphQuotient
      (fun _ : GraphQuotient R => Q) (gqglue s)
      (Qgq a) (Qgq b)
      (fun y : F a =>
       transport_const (gqglue s) (Qgq a y) @
       (Qgqglue a b s y @
        match
          (transport_DGraphQuotient s y)^ in (_ = a0)
          return (Qgq b (e a b s y) = Qgq b a0)
        with
        | 1 => 1
        end))) (transport DGraphQuotient (gqglue s) x)) @
ap (Qgq b) (transport_DGraphQuotient s x) =
Qgqglue a b s x
    apply moveR_pM.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(((transport_const (gqglue s) (Qgq a x))^ @
  (ap
     (fun x : F a =>
      transport (fun _ : GraphQuotient R => Q)
        (gqglue s) (Qgq a x))
     (transport_Vp DGraphQuotient (gqglue s) x))^) @
 (transport_arrow (gqglue s) (Qgq a)
    (transport DGraphQuotient (gqglue s) x))^) @
ap10
  (dpath_arrow DGraphQuotient
     (fun _ : GraphQuotient R => Q) (gqglue s) (Qgq a)
     (Qgq b)
     (fun y : F a =>
      transport_const (gqglue s) (Qgq a y) @
      (Qgqglue a b s y @
       match
         (transport_DGraphQuotient s y)^ in (_ = a0)
         return (Qgq b (e a b s y) = Qgq b a0)
       with
       | 1 => 1
       end))) (transport DGraphQuotient (gqglue s) x) =
Qgqglue a b s x @
(ap (Qgq b) (transport_DGraphQuotient s x))^
    apply moveL_pM.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
((((transport_const (gqglue s) (Qgq a x))^ @
   (ap
      (fun x : F a =>
       transport (fun _ : GraphQuotient R => Q)
         (gqglue s) (Qgq a x))
      (transport_Vp DGraphQuotient (gqglue s) x))^) @
  (transport_arrow (gqglue s) (Qgq a)
     (transport DGraphQuotient (gqglue s) x))^) @
 ap10
   (dpath_arrow DGraphQuotient
      (fun _ : GraphQuotient R => Q) (gqglue s)
      (Qgq a) (Qgq b)
      (fun y : F a =>
       transport_const (gqglue s) (Qgq a y) @
       (Qgqglue a b s y @
        match
          (transport_DGraphQuotient s y)^ in (_ = a0)
          return (Qgq b (e a b s y) = Qgq b a0)
        with
        | 1 => 1
        end))) (transport DGraphQuotient (gqglue s) x)) @
((ap (Qgq b) (transport_DGraphQuotient s x))^)^ =
Qgqglue a b s x
    do 3 lhs nrapply concat_pp_p.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(transport_const (gqglue s) (Qgq a x))^ @
((ap
    (fun x : F a =>
     transport (fun _ : GraphQuotient R => Q)
       (gqglue s) (Qgq a x))
    (transport_Vp DGraphQuotient (gqglue s) x))^ @
 ((transport_arrow (gqglue s) (Qgq a)
     (transport DGraphQuotient (gqglue s) x))^ @
  (ap10
     (dpath_arrow DGraphQuotient
        (fun _ : GraphQuotient R => Q) (gqglue s)
        (Qgq a) (Qgq b)
        (fun y : F a =>
         transport_const (gqglue s) (Qgq a y) @
         (Qgqglue a b s y @
          match
            (transport_DGraphQuotient s y)^ in
            (_ = a0)
            return (Qgq b (e a b s y) = Qgq b a0)
          with
          | 1 => 1
          end)))
     (transport DGraphQuotient (gqglue s) x) @
   ((ap (Qgq b) (transport_DGraphQuotient s x))^)^))) =
Qgqglue a b s x
    apply moveR_Vp.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(ap
   (fun x : F a =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue s) (Qgq a x))
   (transport_Vp DGraphQuotient (gqglue s) x))^ @
((transport_arrow (gqglue s) (Qgq a)
    (transport DGraphQuotient (gqglue s) x))^ @
 (ap10
    (dpath_arrow DGraphQuotient
       (fun _ : GraphQuotient R => Q) (gqglue s)
       (Qgq a) (Qgq b)
       (fun y : F a =>
        transport_const (gqglue s) (Qgq a y) @
        (Qgqglue a b s y @
         match
           (transport_DGraphQuotient s y)^ in (_ = a0)
           return (Qgq b (e a b s y) = Qgq b a0)
         with
         | 1 => 1
         end)))
    (transport DGraphQuotient (gqglue s) x) @
  ((ap (Qgq b) (transport_DGraphQuotient s x))^)^)) =
transport_const (gqglue s) (Qgq a x) @ Qgqglue a b s x
    lhs refine (1 @@ (1 @@ (_ @@ 1))).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
ap10
  (dpath_arrow DGraphQuotient
     (fun _ : GraphQuotient R => Q) (gqglue s) (Qgq a)
     (Qgq b)
     (fun y : F a =>
      transport_const (gqglue s) (Qgq a y) @
      (Qgqglue a b s y @
       match
         (transport_DGraphQuotient s y)^ in (_ = a0)
         return (Qgq b (e a b s y) = Qgq b a0)
       with
       | 1 => 1
       end))) (transport DGraphQuotient (gqglue s) x) =
?Goal
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(ap
   (fun x : F a =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue s) (Qgq a x))
   (transport_Vp DGraphQuotient (gqglue s) x))^ @
((transport_arrow (gqglue s) 
    (Qgq a) (transport DGraphQuotient (gqglue s) x))^ @
 (?Goal @
  ((ap (Qgq b) (transport_DGraphQuotient s x))^)^)) =
transport_const (gqglue s) (Qgq a x) @ Qgqglue a b s x
    1: nrapply (ap10_dpath_arrow DGraphQuotient (fun _ => Q) (gqglue s)).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(ap
   (fun x : F a =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue s) (Qgq a x))
   (transport_Vp DGraphQuotient (gqglue s) x))^ @
((transport_arrow (gqglue s) (Qgq a)
    (transport DGraphQuotient (gqglue s) x))^ @
 (((transport_arrow (gqglue s) (Qgq a)
      (transport DGraphQuotient (gqglue s) x) @
    ap
      (fun x : DGraphQuotient (gq a) =>
       transport (fun _ : GraphQuotient R => Q)
         (gqglue s) (Qgq a x))
      (transport_Vp DGraphQuotient (gqglue s) x)) @
   (fun y : F a =>
    transport_const (gqglue s) (Qgq a y) @
    (Qgqglue a b s y @
     match
       (transport_DGraphQuotient s y)^ in (_ = a0)
       return (Qgq b (e a b s y) = Qgq b a0)
     with
     | 1 => 1
     end)) x) @
  ((ap (Qgq b) (transport_DGraphQuotient s x))^)^)) =
transport_const (gqglue s) (Qgq a x) @ Qgqglue a b s x
    lhs refine (1 @@ (1 @@ _)).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
((transport_arrow (gqglue s) (Qgq a)
    (transport DGraphQuotient (gqglue s) x) @
  ap
    (fun x : DGraphQuotient (gq a) =>
     transport (fun _ : GraphQuotient R => Q)
       (gqglue s) (Qgq a x))
    (transport_Vp DGraphQuotient (gqglue s) x)) @
 (transport_const (gqglue s) (Qgq a x) @
  (Qgqglue a b s x @
   match
     (transport_DGraphQuotient s x)^ in (_ = a0)
     return (Qgq b (e a b s x) = Qgq b a0)
   with
   | 1 => 1
   end))) @
((ap (Qgq b) (transport_DGraphQuotient s x))^)^ =
?Goal
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(ap
   (fun x : F a =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue s) (Qgq a x))
   (transport_Vp DGraphQuotient (gqglue s) x))^ @
((transport_arrow (gqglue s) 
    (Qgq a) (transport DGraphQuotient (gqglue s) x))^ @
 ?Goal) =
transport_const (gqglue s) (Qgq a x) @ Qgqglue a b s x
    {
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
((transport_arrow (gqglue s) (Qgq a)
    (transport DGraphQuotient (gqglue s) x) @
  ap
    (fun x : DGraphQuotient (gq a) =>
     transport (fun _ : GraphQuotient R => Q)
       (gqglue s) (Qgq a x))
    (transport_Vp DGraphQuotient (gqglue s) x)) @
 (transport_const (gqglue s) (Qgq a x) @
  (Qgqglue a b s x @
   match
     (transport_DGraphQuotient s x)^ in (_ = a0)
     return (Qgq b (e a b s x) = Qgq b a0)
   with
   | 1 => 1
   end))) @
((ap (Qgq b) (transport_DGraphQuotient s x))^)^ =
?Goal lhs nrapply concat_pp_p.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(transport_arrow (gqglue s) (Qgq a)
   (transport DGraphQuotient (gqglue s) x) @
 ap
   (fun x : DGraphQuotient (gq a) =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue s) (Qgq a x))
   (transport_Vp DGraphQuotient (gqglue s) x)) @
((transport_const (gqglue s) (Qgq a x) @
  (Qgqglue a b s x @
   match
     (transport_DGraphQuotient s x)^ in (_ = a0)
     return (Qgq b (e a b s x) = Qgq b a0)
   with
   | 1 => 1
   end)) @
 ((ap (Qgq b) (transport_DGraphQuotient s x))^)^) =
?Goal
      nrapply concat_pp_p. }
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(ap
   (fun x : F a =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue s) (Qgq a x))
   (transport_Vp DGraphQuotient (gqglue s) x))^ @
((transport_arrow (gqglue s) (Qgq a)
    (transport DGraphQuotient (gqglue s) x))^ @
 (transport_arrow (gqglue s) (Qgq a)
    (transport DGraphQuotient (gqglue s) x) @
  (ap
     (fun x : DGraphQuotient (gq a) =>
      transport (fun _ : GraphQuotient R => Q)
        (gqglue s) (Qgq a x))
     (transport_Vp DGraphQuotient (gqglue s) x) @
   ((transport_const (gqglue s) (Qgq a x) @
     (Qgqglue a b s x @
      match
        (transport_DGraphQuotient s x)^ in (_ = a0)
        return (Qgq b (e a b s x) = Qgq b a0)
      with
      | 1 => 1
      end)) @
    ((ap (Qgq b) (transport_DGraphQuotient s x))^)^)))) =
transport_const (gqglue s) (Qgq a x) @ Qgqglue a b s x
    lhs nrapply (1 @@ concat_V_pp _ _).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(ap
   (fun x : F a =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue s) (Qgq a x))
   (transport_Vp DGraphQuotient (gqglue s) x))^ @
(ap
   (fun x : DGraphQuotient (gq a) =>
    transport (fun _ : GraphQuotient R => Q)
      (gqglue s) (Qgq a x))
   (transport_Vp DGraphQuotient (gqglue s) x) @
 ((transport_const (gqglue s) (Qgq a x) @
   (Qgqglue a b s x @
    match
      (transport_DGraphQuotient s x)^ in (_ = a0)
      return (Qgq b (e a b s x) = Qgq b a0)
    with
    | 1 => 1
    end)) @
  ((ap (Qgq b) (transport_DGraphQuotient s x))^)^)) =
transport_const (gqglue s) (Qgq a x) @ Qgqglue a b s x
    lhs nrapply concat_V_pp.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(transport_const (gqglue s) (Qgq a x) @
 (Qgqglue a b s x @
  match
    (transport_DGraphQuotient s x)^ in (_ = a0)
    return (Qgq b (e a b s x) = Qgq b a0)
  with
  | 1 => 1
  end)) @
((ap (Qgq b) (transport_DGraphQuotient s x))^)^ =
transport_const (gqglue s) (Qgq a x) @ Qgqglue a b s x
    lhs nrapply concat_pp_p.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
transport_const (gqglue s) (Qgq a x) @
((Qgqglue a b s x @
  match
    (transport_DGraphQuotient s x)^ in (_ = a0)
    return (Qgq b (e a b s x) = Qgq b a0)
  with
  | 1 => 1
  end) @
 ((ap (Qgq b) (transport_DGraphQuotient s x))^)^) =
transport_const (gqglue s) (Qgq a x) @ Qgqglue a b s x
    f_ap.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
(Qgqglue a b s x @
 match
   (transport_DGraphQuotient s x)^ in (_ = a0)
   return (Qgq b (e a b s x) = Qgq b a0)
 with
 | 1 => 1
 end) @
((ap (Qgq b) (transport_DGraphQuotient s x))^)^ =
Qgqglue a b s x
    lhs nrapply concat_pp_p.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
Qgqglue a b s x @
(match
   (transport_DGraphQuotient s x)^ in (_ = a0)
   return (Qgq b (e a b s x) = Qgq b a0)
 with
 | 1 => 1
 end @ ((ap (Qgq b) (transport_DGraphQuotient s x))^)^) =
Qgqglue a b s x
    apply moveR_Mp.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
match
  (transport_DGraphQuotient s x)^ in (_ = a0)
  return (Qgq b (e a b s x) = Qgq b a0)
with
| 1 => 1
end @ ((ap (Qgq b) (transport_DGraphQuotient s x))^)^ =
(Qgqglue a b s x)^ @ Qgqglue a b s x
    rhs nrapply concat_Vp.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
match
  (transport_DGraphQuotient s x)^ in (_ = a0)
  return (Qgq b (e a b s x) = Qgq b a0)
with
| 1 => 1
end @ ((ap (Qgq b) (transport_DGraphQuotient s x))^)^ =
1
    apply moveR_pV.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
match
  (transport_DGraphQuotient s x)^ in (_ = a0)
  return (Qgq b (e a b s x) = Qgq b a0)
with
| 1 => 1
end = 1 @ (ap (Qgq b) (transport_DGraphQuotient s x))^
    rhs nrapply concat_1p.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
Q: Type
Qgq: forall a : A, F a -> Q
Qgqglue: forall (a b : A) (r : R a b) 
(x : F a), Qgq a x = Qgq b (e a b r x)
a, b: A
s: R a b
x: F a
match
  (transport_DGraphQuotient s x)^ in (_ = a0)
  return (Qgq b (e a b s x) = Qgq b a0)
with
| 1 => 1
end = (ap (Qgq b) (transport_DGraphQuotient s x))^
    nrapply ap_V.
  Defined.

  (** Now that we've shown that [sig DGraphQuotient] acts like a [GraphQuotient] of [sig F] 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_gq_flatten
    : sig DGraphQuotient
    <~> GraphQuotient (fun a b => {r : R a.1 b.1 & e _ _ r a.2 = b.2}).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
{x : _ & DGraphQuotient x} <~>
GraphQuotient
  (fun a b : {x : _ & F x} =>
   {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2})
  Proof.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
{x : _ & DGraphQuotient x} <~>
GraphQuotient
  (fun a b : {x : _ & F x} =>
   {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2})
    snrapply equiv_adjointify.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
{x : _ & DGraphQuotient x} ->
GraphQuotient
  (fun a b : {x : _ & F x} =>
   {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2})
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
GraphQuotient
  (fun a b : {x : _ & F x} =>
   {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2}) ->
{x : _ & DGraphQuotient x}
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
?f o ?g == idmap
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
?g o ?f == idmap
    -
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
{x : _ & DGraphQuotient x} ->
GraphQuotient
  (fun a b : {x : _ & F x} =>
   {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2}) snrapply flatten_rec.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall a : A,
F a ->
GraphQuotient
  (fun a0 b : {x : _ & F x} =>
   {r : R a0.1 b.1 & e a0.1 b.1 r a0.2 = b.2})
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall (a b : A) (s : R a b) (x : F a),
?Qgq a x = ?Qgq b (e a b s x)
      +
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall a : A,
F a ->
GraphQuotient
  (fun a0 b : {x : _ & F x} =>
   {r : R a0.1 b.1 & e a0.1 b.1 r a0.2 = b.2}) exact (fun a x => gq (a; x)).
      +
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall (a b : A) (s : R a b) (x : F a),
(fun (a0 : A) (x0 : F a0) => gq (a0; x0)) a x =
(fun (a0 : A) (x0 : F a0) => gq (a0; x0)) b
  (e a b s x) intros a b r x.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a, b: A
r: R a b
x: F a
(fun (a : A) (x : F a) => gq (a; x)) a x =
(fun (a : A) (x : F a) => gq (a; x)) b (e a b r x)
        apply gqglue.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a, b: A
r: R a b
x: F a
{r0 : R (a; x).1 (b; e a b r x).1 &
e (a; x).1 (b; e a b r x).1 r0 (a; x).2 =
(b; e a b r x).2}
        exists r.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a, b: A
r: R a b
x: F a
e (a; x).1 (b; e a b r x).1 r (a; x).2 =
(b; e a b r x).2
        reflexivity.
    -
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
GraphQuotient
  (fun a b : {x : _ & F x} =>
   {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2}) ->
{x : _ & DGraphQuotient x} snrapply GraphQuotient_rec.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
{x : _ & F x} -> {x : _ & DGraphQuotient x}
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall a b : {x : _ & F x},
(fun a0 b0 : {x : _ & F x} =>
 {r : R a0.1 b0.1 & e a0.1 b0.1 r a0.2 = b0.2}) a b ->
?c a = ?c b
      +
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
{x : _ & F x} -> {x : _ & DGraphQuotient x} exact (fun '(a; x) => (gq a; x)).
      +
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall a b : {x : _ & F x},
(fun a0 b0 : {x : _ & F x} =>
 {r : R a0.1 b0.1 & e a0.1 b0.1 r a0.2 = b0.2}) a b ->
(fun pat : {x : _ & F x} =>
 let x := pat in
 let a0 := x.1 in let x0 := x.2 in (gq a0; x0)) a =
(fun pat : {x : _ & F 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 p].
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
y: F b
r: R (a; x).1 (b; y).1
p: e (a; x).1 (b; y).1 r (a; x).2 = (b; y).2
(let x := (a; x) in
 let a := x.1 in let x0 := x.2 in (gq a; x0)) =
(let x := (b; y) in
 let a := x.1 in let x0 := x.2 in (gq a; x0))
        simpl in p, r.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
y: F b
r: R a b
p: e a b r x = y
(let x := (a; x) in
 let a := x.1 in let x0 := x.2 in (gq a; x0)) =
(let x := (b; y) in
 let a := x.1 in let x0 := x.2 in (gq a; x0))
        destruct p.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
r: R a b
(let x := (a; x) in
 let a := x.1 in let x0 := x.2 in (gq a; x0)) =
(let x := (b; e a b r x) in
 let a := x.1 in let x0 := x.2 in (gq a; x0))
        apply flatten_gqglue.
    -
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
flatten_rec (fun (a : A) (x : F a) => gq (a; x))
  (fun (a b : A) (r : R a b) (x : F a) =>
   gqglue (r; 1))
o GraphQuotient_rec
    (fun pat : {x : _ & F x} =>
     let x := pat in
     let a := x.1 in let x0 := x.2 in (gq a; x0))
    (fun a0 : {x : _ & F x} =>
     (fun (a : A) (x : F a) (b0 : {x : _ & F x}) =>
      (fun (b : A) (y : F b)
         (X : {r : R (a; x).1 (b; y).1 &
              e (a; x).1 (b; y).1 r (a; x).2 =
              (b; y).2}) =>
       (fun (r : R (a; x).1 (b; y).1)
          (p : e (a; x).1 (b; y).1 r (a; x).2 =
               (b; y).2) =>
        match
          p in (_ = f)
          return
            ((let x0 := (a; x) in
              let a1 := x0.1 in
              let x1 := x0.2 in (gq a1; x1)) =
             (let x0 := (b; f) in
              let a1 := x0.1 in
              let x1 := x0.2 in (gq a1; x1)))
        with
        | 1 => flatten_gqglue r x
        end) X.1 X.2) b0.1 b0.2) a0.1 a0.2) == idmap snrapply GraphQuotient_ind.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall a : {x : _ & F x},
(fun
   x : GraphQuotient
         (fun a0 b : {x : _ & F x} =>
          {r : R a0.1 b.1 & e a0.1 b.1 r a0.2 = b.2})
 =>
 (flatten_rec
    (fun (a0 : A) (x0 : F a0) => gq (a0; x0))
    (fun (a0 b : A) (r : R a0 b) (x0 : F a0) =>
     gqglue (r; 1))
  o GraphQuotient_rec
      (fun pat : {x : _ & F x} =>
       let x0 := pat in
       let a0 := x0.1 in let x1 := x0.2 in (gq a0; x1))
      (fun a0 : {x : _ & F x} =>
       (fun (a1 : A) (x0 : F a1) (b0 : {x : _ & F x})
        =>
        (fun (b : A) (y : F b)
           (X : {r : R (a1; x0).1 (b; y).1 &
                e (a1; x0).1 (b; y).1 r (a1; x0).2 =
                (b; y).2}) =>
         (fun (r : R (a1; x0).1 (b; y).1)
            (p : e (a1; x0).1 (b; y).1 r (a1; x0).2 =
                 (b; y).2) =>
          match
            p in (_ = f) return ((...) = (...))
          with
          | 1 => flatten_gqglue r x0
          end) 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
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall (a b : {x : _ & F x})
(s : (fun a0 b0 : {x : _ & F x} =>
      {r : R a0.1 b0.1 & e a0.1 b0.1 r a0.2 = b0.2}) a
       b),
transport
  (fun
     x : GraphQuotient
           (fun a0 b0 : {x : _ & F x} =>
            {r : R a0.1 b0.1 &
            e a0.1 b0.1 r a0.2 = b0.2}) =>
   (flatten_rec
      (fun (a0 : A) (x0 : F a0) => gq (a0; x0))
      (fun (a0 b0 : A) (r : R a0 b0) (x0 : F a0) =>
       gqglue (r; 1))
    o GraphQuotient_rec
        (fun pat : {x : _ & F x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (gq a0; x1))
        (fun a0 : {x : _ & F x} =>
         (fun (a1 : A) (x0 : F a1)
            (b0 : {x : _ & F x}) =>
          (fun (b1 : A) (y : F b1)
             (X : {r : R (a1; x0).1 (b1; y).1 &
                  e (a1; x0).1 (b1; y).1 r (a1; x0).2 =
                  (b1; y).2}) =>
           (fun (r : R (a1; x0).1 (b1; y).1)
              (p : e (a1; x0).1 (b1; y).1 r (a1; x0).2 =
                   (b1; y).2) =>
            match p in (_ = f) return (... = ...) with
            | 1 => flatten_gqglue r x0
            end) 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
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall (a b : {x : _ & F x})
(s : (fun a0 b0 : {x : _ & F x} =>
      {r : R a0.1 b0.1 & e a0.1 b0.1 r a0.2 = b0.2}) a
       b),
transport
  (fun
     x : GraphQuotient
           (fun a0 b0 : {x : _ & F x} =>
            {r : R a0.1 b0.1 &
            e a0.1 b0.1 r a0.2 = b0.2}) =>
   (flatten_rec
      (fun (a0 : A) (x0 : F a0) => gq (a0; x0))
      (fun (a0 b0 : A) (r : R a0 b0) (x0 : F a0) =>
       gqglue (r; 1))
    o GraphQuotient_rec
        (fun pat : {x : _ & F x} =>
         let x0 := pat in
         let a0 := x0.1 in
         let x1 := x0.2 in (gq a0; x1))
        (fun a0 : {x : _ & F x} =>
         (fun (a1 : A) (x0 : F a1)
            (b0 : {x : _ & F x}) =>
          (fun (b1 : A) (y : F b1)
             (X : {r : R (a1; x0).1 (b1; y).1 &
                  e (a1; x0).1 (b1; y).1 r (a1; x0).2 =
                  (b1; y).2}) =>
           (fun (r : R (a1; x0).1 (b1; y).1)
              (p : e (a1; x0).1 (b1; y).1 r (a1; x0).2 =
                   (b1; y).2) =>
            match p in (_ = f) return (... = ...) with
            | 1 => flatten_gqglue r x0
            end) X.1 X.2) b0.1 b0.2) a0.1 a0.2)) x =
   idmap x) (gqglue s)
  ((fun a0 : {x : _ & F x} => 1) a) =
(fun a0 : {x : _ & F x} => 1) b
      intros [a x] [b y] [r p].
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
y: F b
r: R (a; x).1 (b; y).1
p: e (a; x).1 (b; y).1 r (a; x).2 = (b; y).2
transport
  (fun
     x : GraphQuotient
           (fun a b : {x : _ & F x} =>
            {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2})
   =>
   flatten_rec (fun (a : A) (x0 : F a) => gq (a; x0))
     (fun (a b : A) (r : R a b) (x0 : F a) =>
      gqglue (r; 1))
     (GraphQuotient_rec
        (fun pat : {x : _ & F x} =>
         let x0 := pat in
         let a := x0.1 in let x1 := x0.2 in (gq a; x1))
        (fun (a0 b0 : {x : _ & F x})
           (X : {r : R (a0.1; a0.2).1 (b0.1; b0.2).1 &
                e (a0.1; a0.2).1 (b0.1; b0.2).1 r
                  (a0.1; a0.2).2 = (b0.1; b0.2).2}) =>
         match
           X.2 in (_ = f)
           return
             ((let x0 := (a0.1; a0.2) in
               let a := x0.1 in
               let x1 := x0.2 in (gq a; x1)) =
              (let x0 := (b0.1; f) in
               let a := x0.1 in
               let x1 := x0.2 in (gq a; x1)))
         with
         | 1 => flatten_gqglue X.1 a0.2
         end) x) = x) (gqglue (r; p)) 1 = 1
      simpl in p, r.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
y: F b
r: R a b
p: e a b r x = y
transport
  (fun
     x : GraphQuotient
           (fun a b : {x : _ & F x} =>
            {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2})
   =>
   flatten_rec (fun (a : A) (x0 : F a) => gq (a; x0))
     (fun (a b : A) (r : R a b) (x0 : F a) =>
      gqglue (r; 1))
     (GraphQuotient_rec
        (fun pat : {x : _ & F x} =>
         let x0 := pat in
         let a := x0.1 in let x1 := x0.2 in (gq a; x1))
        (fun (a0 b0 : {x : _ & F x})
           (X : {r : R (a0.1; a0.2).1 (b0.1; b0.2).1 &
                e (a0.1; a0.2).1 (b0.1; b0.2).1 r
                  (a0.1; a0.2).2 = (b0.1; b0.2).2}) =>
         match
           X.2 in (_ = f)
           return
             ((let x0 := (a0.1; a0.2) in
               let a := x0.1 in
               let x1 := x0.2 in (gq a; x1)) =
              (let x0 := (b0.1; f) in
               let a := x0.1 in
               let x1 := x0.2 in (gq a; x1)))
         with
         | 1 => flatten_gqglue X.1 a0.2
         end) x) = x) (gqglue (r; p)) 1 = 1
      destruct p.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
r: R a b
transport
  (fun
     x : GraphQuotient
           (fun a b : {x : _ & F x} =>
            {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2})
   =>
   flatten_rec (fun (a : A) (x0 : F a) => gq (a; x0))
     (fun (a b : A) (r : R a b) (x0 : F a) =>
      gqglue (r; 1))
     (GraphQuotient_rec
        (fun pat : {x : _ & F x} =>
         let x0 := pat in
         let a := x0.1 in let x1 := x0.2 in (gq a; x1))
        (fun (a0 b0 : {x : _ & F x})
           (X : {r : R (a0.1; a0.2).1 (b0.1; b0.2).1 &
                e (a0.1; a0.2).1 (b0.1; b0.2).1 r
                  (a0.1; a0.2).2 = (b0.1; b0.2).2}) =>
         match
           X.2 in (_ = f)
           return
             ((let x0 := (a0.1; a0.2) in
               let a := x0.1 in
               let x1 := x0.2 in (gq a; x1)) =
              (let x0 := (b0.1; f) in
               let a := x0.1 in
               let x1 := x0.2 in (gq a; x1)))
         with
         | 1 => flatten_gqglue X.1 a0.2
         end) x) = x) (gqglue (r; 1)) 1 = 1
      simpl.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
r: R a b
transport
  (fun
     x : GraphQuotient
           (fun a b : {x : _ & F x} =>
            {r : R a.1 b.1 & e a.1 b.1 r a.2 = b.2})
   =>
   flatten_rec (fun (a : A) (x0 : F a) => gq (a; x0))
     (fun (a b : A) (r : R a b) (x0 : F a) =>
      gqglue (r; 1))
     (GraphQuotient_rec
        (fun pat : {x : _ & F x} => (gq pat.1; pat.2))
        (fun (a0 b0 : {x : _ & F x})
           (X : {r : R a0.1 b0.1 &
                e a0.1 b0.1 r a0.2 = b0.2}) =>
         match
           X.2 in (_ = f)
           return ((gq a0.1; a0.2) = (gq b0.1; f))
         with
         | 1 => flatten_gqglue X.1 a0.2
         end) x) = x) (gqglue (r; 1)) 1 = 1
      lhs nrapply transport_paths_FFlr.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
r: R a b
((ap
    (flatten_rec (fun (a : A) (x : F a) => gq (a; x))
       (fun (a b : A) (r : R a b) (x : F a) =>
        gqglue (r; 1)))
    (ap
       (GraphQuotient_rec
          (fun pat : {x : _ & F x} =>
           (gq pat.1; pat.2))
          (fun (a0 b0 : {x : _ & F x})
             (X : {r : R a0.1 b0.1 &
                  e a0.1 b0.1 r a0.2 = b0.2}) =>
           match
             X.2 in (_ = f)
             return ((gq a0.1; a0.2) = (gq b0.1; f))
           with
           | 1 => flatten_gqglue X.1 a0.2
           end)) (gqglue (r; 1))))^ @ 1) @
gqglue (r; 1) = 1
      rewrite GraphQuotient_rec_beta_gqglue.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
r: R a b
((ap
    (flatten_rec (fun (a : A) (x : F a) => gq (a; x))
       (fun (a b : A) (r : R a b) (x : F a) =>
        gqglue (r; 1))) (flatten_gqglue r x))^ @ 1) @
gqglue (r; 1) = 1
      refine ((_ @@ 1) @ concat_Vp _).
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
r: R a b
(ap
   (flatten_rec (fun (a : A) (x : F a) => gq (a; x))
      (fun (a b : A) (r : R a b) (x : F a) =>
       gqglue (r; 1))) (flatten_gqglue r x))^ @ 1 =
(gqglue (r; 1))^
      lhs nrapply concat_p1.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
r: R a b
(ap
   (flatten_rec (fun (a : A) (x : F a) => gq (a; x))
      (fun (a b : A) (r : R a b) (x : F a) =>
       gqglue (r; 1))) (flatten_gqglue r x))^ =
(gqglue (r; 1))^
      apply inverse2.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a: A
x: F a
b: A
r: R a b
ap
  (flatten_rec (fun (a : A) (x : F a) => gq (a; x))
     (fun (a b : A) (r : R a b) (x : F a) =>
      gqglue (r; 1))) (flatten_gqglue r x) =
gqglue (r; 1)
      nrapply flatten_rec_beta_gqglue.
    -
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
GraphQuotient_rec
  (fun pat : {x : _ & F x} =>
   let x := pat in
   let a := x.1 in let x0 := x.2 in (gq a; x0))
  (fun a0 : {x : _ & F x} =>
   (fun (a : A) (x : F a) (b0 : {x : _ & F x}) =>
    (fun (b : A) (y : F b)
       (X : {r : R (a; x).1 (b; y).1 &
            e (a; x).1 (b; y).1 r (a; x).2 = (b; y).2})
     =>
     (fun (r : R (a; x).1 (b; y).1)
        (p : e (a; x).1 (b; y).1 r (a; x).2 = (b; y).2)
      =>
      match
        p in (_ = f)
        return
          ((let x0 := (a; x) in
            let a1 := x0.1 in
            let x1 := x0.2 in (gq a1; x1)) =
           (let x0 := (b; f) in
            let a1 := x0.1 in
            let x1 := x0.2 in (gq a1; x1)))
      with
      | 1 => flatten_gqglue r x
      end) X.1 X.2) b0.1 b0.2) a0.1 a0.2)
o flatten_rec (fun (a : A) (x : F a) => gq (a; x))
    (fun (a b : A) (r : R a b) (x : F a) =>
     gqglue (r; 1)) == idmap snrapply flatten_ind.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall (a : A) (x : F a),
(fun x0 : {x : _ & DGraphQuotient x} =>
 (GraphQuotient_rec
    (fun pat : {x : _ & F x} =>
     let x1 := pat in
     let a0 := x1.1 in let x2 := x1.2 in (gq a0; x2))
    (fun a0 : {x : _ & F x} =>
     (fun (a1 : A) (x1 : F a1) (b0 : {x : _ & F x}) =>
      (fun (b : A) (y : F b)
         (X : {r : R (a1; x1).1 (b; y).1 &
              e (a1; x1).1 (b; y).1 r (a1; x1).2 =
              (b; y).2}) =>
       (fun (r : R (a1; x1).1 (b; y).1)
          (p : e (a1; x1).1 (b; y).1 r (a1; x1).2 =
               (b; y).2) =>
        match p in (_ = f) return ((...) = (...)) with
        | 1 => flatten_gqglue r x1
        end) X.1 X.2) b0.1 b0.2) a0.1 a0.2)
  o flatten_rec
      (fun (a0 : A) (x1 : F a0) => gq (a0; x1))
      (fun (a0 b : A) (r : R a0 b) (x1 : F a0) =>
       gqglue (r; 1))) x0 = idmap x0) (flatten_gq x)
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall (a b : A) (s : R a b) (x : F a),
transport
  (fun x0 : {x : _ & DGraphQuotient x} =>
   (GraphQuotient_rec
      (fun pat : {x : _ & F x} =>
       let x1 := pat in
       let a0 := x1.1 in let x2 := x1.2 in (gq a0; x2))
      (fun a0 : {x : _ & F x} =>
       (fun (a1 : A) (x1 : F a1) (b0 : {x : _ & F x})
        =>
        (fun (b1 : A) (y : F b1)
           (X : {r : R (a1; x1).1 (b1; y).1 &
                e (a1; x1).1 (b1; y).1 r (a1; x1).2 =
                (b1; y).2}) =>
         (fun (r : R (a1; x1).1 (b1; y).1)
            (p : e (a1; x1).1 (b1; y).1 r (a1; x1).2 =
                 (b1; y).2) =>
          match p in (_ = f) return (... = ...) with
          | 1 => flatten_gqglue r x1
          end) X.1 X.2) b0.1 b0.2) a0.1 a0.2)
    o flatten_rec
        (fun (a0 : A) (x1 : F a0) => gq (a0; x1))
        (fun (a0 b0 : A) (r : R a0 b0) (x1 : F a0) =>
         gqglue (r; 1))) x0 = idmap x0)
  (flatten_gqglue s x) (?Qgq a x) = ?Qgq b (e a b s x)
      1: reflexivity.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
forall (a b : A) (s : R a b) (x : F a),
transport
  (fun x0 : {x : _ & DGraphQuotient x} =>
   (GraphQuotient_rec
      (fun pat : {x : _ & F x} =>
       let x1 := pat in
       let a0 := x1.1 in let x2 := x1.2 in (gq a0; x2))
      (fun a0 : {x : _ & F x} =>
       (fun (a1 : A) (x1 : F a1) (b0 : {x : _ & F x})
        =>
        (fun (b1 : A) (y : F b1)
           (X : {r : R (a1; x1).1 (b1; y).1 &
                e (a1; x1).1 (b1; y).1 r (a1; x1).2 =
                (b1; y).2}) =>
         (fun (r : R (a1; x1).1 (b1; y).1)
            (p : e (a1; x1).1 (b1; y).1 r (a1; x1).2 =
                 (b1; y).2) =>
          match p in (_ = f) return (... = ...) with
          | 1 => flatten_gqglue r x1
          end) X.1 X.2) b0.1 b0.2) a0.1 a0.2)
    o flatten_rec
        (fun (a0 : A) (x1 : F a0) => gq (a0; x1))
        (fun (a0 b0 : A) (r : R a0 b0) (x1 : F a0) =>
         gqglue (r; 1))) x0 = idmap x0)
  (flatten_gqglue s x)
  ((fun (a0 : A) (x0 : F a0) => 1) a x) =
(fun (a0 : A) (x0 : F a0) => 1) b (e a b s x)
      intros a b r x.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a, b: A
r: R a b
x: F a
transport
  (fun x : {x : _ & DGraphQuotient x} =>
   (GraphQuotient_rec
      (fun pat : {x : _ & F x} =>
       let x0 := pat in
       let a := x0.1 in let x1 := x0.2 in (gq a; x1))
      (fun a0 : {x : _ & F x} =>
       (fun (a : A) (x0 : F a) (b0 : {x : _ & F x}) =>
        (fun (b : A) (y : F b)
           (X : {r : R (a; x0).1 (b; y).1 &
                e (a; x0).1 (b; y).1 r (a; x0).2 =
                (b; y).2}) =>
         (fun (r : R (a; x0).1 (b; y).1)
            (p : e (a; x0).1 (b; y).1 r (a; x0).2 =
                 (b; y).2) =>
          match
            p in (_ = f) return ((...) = (...))
          with
          | 1 => flatten_gqglue r x0
          end) X.1 X.2) b0.1 b0.2) a0.1 a0.2)
    o flatten_rec
        (fun (a : A) (x0 : F a) => gq (a; x0))
        (fun (a b : A) (r : R a b) (x0 : F a) =>
         gqglue (r; 1))) x = idmap x)
  (flatten_gqglue r x)
  ((fun (a : A) (x : F a) => 1) a x) =
(fun (a : A) (x : F a) => 1) b (e a b r x)
      nrapply (transport_paths_FFlr' (g := GraphQuotient_rec _ _)); apply equiv_p1_1q.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a, b: A
r: R a b
x: F a
ap
  (GraphQuotient_rec
     (fun pat : {x : _ & F x} =>
      let x := pat in
      let a := x.1 in let x0 := x.2 in (gq a; x0))
     (fun (a0 b0 : {x : _ & F x})
        (X : {r : R (a0.1; a0.2).1 (b0.1; b0.2).1 &
             e (a0.1; a0.2).1 (b0.1; b0.2).1 r
               (a0.1; a0.2).2 = (b0.1; b0.2).2}) =>
      match
        X.2 in (_ = f)
        return
          ((let x := (a0.1; a0.2) in
            let a := x.1 in
            let x0 := x.2 in (gq a; x0)) =
           (let x := (b0.1; f) in
            let a := x.1 in
            let x0 := x.2 in (gq a; x0)))
      with
      | 1 => flatten_gqglue X.1 a0.2
      end))
  (ap
     (flatten_rec (fun (a : A) (x : F a) => gq (a; x))
        (fun (a b : A) (r : R a b) (x : F a) =>
         gqglue (r; 1))) (flatten_gqglue r x)) =
flatten_gqglue r x
      rewrite flatten_rec_beta_gqglue.
H: Univalence
A: Type
R: A -> A -> Type
F: A -> Type
e: forall x y : A, R x y -> F x <~> F y
a, b: A
r: R a b
x: F a
ap
  (GraphQuotient_rec
     (fun pat : {x : _ & F x} =>
      let x := pat in
      let a := x.1 in let x0 := x.2 in (gq a; x0))
     (fun (a0 b0 : {x : _ & F x})
        (X : {r : R (a0.1; a0.2).1 (b0.1; b0.2).1 &
             e (a0.1; a0.2).1 (b0.1; b0.2).1 r
               (a0.1; a0.2).2 = (b0.1; b0.2).2}) =>
      match
        X.2 in (_ = f)
        return
          ((let x := (a0.1; a0.2) in
            let a := x.1 in
            let x0 := x.2 in (gq a; x0)) =
           (let x := (b0.1; f) in
            let a := x.1 in
            let x0 := x.2 in (gq a; x0)))
      with
      | 1 => flatten_gqglue X.1 a0.2
      end)) (gqglue (r; 1)) = flatten_gqglue r x
      exact (GraphQuotient_rec_beta_gqglue _ _ (a; x) (b; e a b r x) (r; 1)).
  Defined.

End Flattening.

(** ** 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
  snrapply 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.

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
  snrapply 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
  nrapply (transport_paths_FlFr' (gqglue r)).
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 @ ap idmap (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) = ap idmap (gqglue r)
  rhs nrapply ap_idmap.
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
  nrapply 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))
  snrapply 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.
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' o functor_gq f e) x =
   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)) x) (gqglue s)
  ((fun a : A => 1) a) = (fun a : A => 1) b
  nrapply (transport_paths_FlFr' (gqglue s)).
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
  (fun x : GraphQuotient R =>
   functor_gq g e' (functor_gq f e x)) (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
  (fun x : GraphQuotient R =>
   functor_gq g e' (functor_gq f e x)) (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 nrapply (ap_compose (functor_gq f e) (functor_gq g e') (gqglue s)).
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 nrapply 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 GraphQuotient_rec_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)
  lhs nrapply GraphQuotient_rec_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
gqglue (e' (f a) (f b) (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)
  exact (GraphQuotient_rec_beta_gqglue _ _ _ _ s)^.
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'
  snrapply 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.
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)
  (((fun a : A => ap gq (p a))
    :
    forall a : A,
    (fun x : GraphQuotient R =>
     functor_gq f e x = functor_gq f' e' x) (gq a)) a) =
((fun a : A => ap gq (p a))
 :
 forall a : A,
 (fun x : GraphQuotient R =>
  functor_gq f e x = functor_gq f' e' x) (gq a)) b
    nrapply (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 nrefine (1 @@ _).
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: apply GraphQuotient_rec_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 nrefine (_ @@ 1).
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: apply GraphQuotient_rec_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 nrapply (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 nrapply 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)
    nrapply transport011_paths.
Defined.

(** ** Equivalence of graph quotients *)

Global 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 nrapply (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 nrapply 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 nrapply 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
    snrapply 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 nrapply 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 nrapply 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 nrapply 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
    snrapply 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 nrapply 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) _.