(** * Equivalence induction *)
Require Import Basics.Overture Basics.Equivalences Basics.Tactics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Equiv Types.Prod Types.Forall Types.Sigma Types.Universe.

(** We define typeclasses and tactics for doing equivalence induction. *)

Local Open Scope equiv_scope.

Class RespectsEquivalenceL@{i j k s0 s1} (A : Type@{i}) (P : forall (B : Type@{j}), (A <~> B) -> Type@{k})
  := respects_equivalenceL : sig@{s0 s1} (fun e' : forall B (e : A <~> B), P A (equiv_idmap A) <~> P B e => Funext -> equiv_idmap _ = e' A (equiv_idmap _) ).
Class RespectsEquivalenceR@{i j k s0 s1} (A : Type@{i}) (P : forall (B : Type@{j}), (B <~> A) -> Type@{k})
  := respects_equivalenceR : sig@{s0 s1} (fun e' : forall B (e : B <~> A), P A (equiv_idmap A) <~> P B e => Funext -> equiv_idmap _ = e' A (equiv_idmap _) ).
(** We use a sigma type rather than a record for two reasons:

    1. In the dependent cases, where one equivalence-respectfulness proof will show up in the body of another goal, it might be the case that using sigma types allows us to reuse the respectfulness lemmas of sigma types, rather than writing new ones for this type.

    2. We expect it to be significantly useful to see the type of the fields than the type of the record, because we expect this type to show up as a goal infrequently.  Sigma types have more informative notations than record type names; the user can run [hnf] to see what is left to do in the side conditions. *)

Global Arguments RespectsEquivalenceL : clear implicits.
Global Arguments RespectsEquivalenceR : clear implicits.

(** When doing equivalence induction, typeclass inference will either fully solve the respectfulness side-conditions, or not make any progress.  We would like to progress as far as we can on the side-conditions, so that we leave the user with as little to prove as possible.  To do this, we create a "database", implemented using typeclasses, to look up the refinement lemma, keyed on the head of the term we want to respect equivalence. *)
Class respects_equivalence_db {KT VT} (Key : KT) {lem : VT} : Type0 := make_respects_equivalence_db : Unit.
Definition get_lem' {KT VT} Key {lem} `{@respects_equivalence_db KT VT Key lem} : VT := lem.
Notation get_lem key := ltac:(let res := constr:(get_lem' key) in let res' := (eval unfold get_lem' in res) in exact res') (only parsing).

Section const.
  Context {A : Type} {T : Type}.
  #[export] Instance const_respects_equivalenceL
  : RespectsEquivalenceL A (fun _ _ => T).
A, T: Type
RespectsEquivalenceL A
  (fun (B : Type) (_ : A <~> B) => T)
  Proof.
A, T: Type
RespectsEquivalenceL A
  (fun (B : Type) (_ : A <~> B) => T)
    refine (fun _ _ => equiv_idmap T; fun _ => _).
A, T: Type
y: Funext
1 = 1
    exact idpath.
  Defined.
  #[export] Instance const_respects_equivalenceR
  : RespectsEquivalenceR A (fun _ _ => T).
A, T: Type
RespectsEquivalenceR A
  (fun (B : Type) (_ : B <~> A) => T)
  Proof.
A, T: Type
RespectsEquivalenceR A
  (fun (B : Type) (_ : B <~> A) => T)
    refine (fun _ _ => equiv_idmap _; fun _ => _).
A, T: Type
y: Funext
1 = 1
    exact idpath.
  Defined.
End const.

Instance: forall {T}, @respects_equivalence_db _ _ T (fun A => @const_respects_equivalenceL A T) := fun _ => tt.

Section id.
  Context {A : Type}.
  #[export] Instance idmap_respects_equivalenceL
  : RespectsEquivalenceL A (fun B _ => B).
A: Type
RespectsEquivalenceL A
  (fun (B : Type) (_ : A <~> B) => B)
  Proof.
A: Type
RespectsEquivalenceL A
  (fun (B : Type) (_ : A <~> B) => B)
    refine (fun B e => e; fun _ => _).
A: Type
y: Funext
1 = 1
    exact idpath.
  Defined.
  #[export] Instance idmap_respects_equivalenceR
  : RespectsEquivalenceR A (fun B _ => B).
A: Type
RespectsEquivalenceR A
  (fun (B : Type) (_ : B <~> A) => B)
  Proof.
A: Type
RespectsEquivalenceR A
  (fun (B : Type) (_ : B <~> A) => B)
    refine (fun B e => equiv_inverse e; fun _ => path_equiv _).
A: Type
y: Funext
1 = 1^-1
    apply path_forall; intro; reflexivity.
  Defined.
End id.

Section unit.
  Context {A : Type}.
  Definition unit_respects_equivalenceL
  : RespectsEquivalenceL A (fun _ _ => Unit)
    := @const_respects_equivalenceL A Unit.
  Definition unit_respects_equivalenceR
  : RespectsEquivalenceR A (fun _ _ => Unit)
    := @const_respects_equivalenceR A Unit.
End unit.

Section prod.
  #[export] Instance prod_respects_equivalenceL {A} {P Q : forall B, (A <~> B) -> Type}
         `{RespectsEquivalenceL A P, RespectsEquivalenceL A Q}
  : RespectsEquivalenceL A (fun B e => P B e * Q B e).
A: Type
P, Q: forall B : Type, A <~> B -> Type
H: RespectsEquivalenceL A P
H0: RespectsEquivalenceL A Q
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e * Q B e)
  Proof.
A: Type
P, Q: forall B : Type, A <~> B -> Type
H: RespectsEquivalenceL A P
H0: RespectsEquivalenceL A Q
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e * Q B e)
    refine ((fun B e => equiv_functor_prod' (respects_equivalenceL.1 B e) (respects_equivalenceL.1 B e)); _).
A: Type
P, Q: forall B : Type, A <~> B -> Type
H: RespectsEquivalenceL A P
H0: RespectsEquivalenceL A Q
Funext ->
1 =
respects_equivalenceL.1 A 1 *E
respects_equivalenceL.1 A 1
    exact (fun fs =>
             transport
               (fun e' => _ = equiv_functor_prod' e' _) (respects_equivalenceL.2 _)
               (transport
                  (fun e' => _ = equiv_functor_prod' _ e') (respects_equivalenceL.2 _)
                  idpath)).
  Defined.

  #[export] Instance prod_respects_equivalenceR {A} {P Q : forall B, (B <~> A) -> Type}
         `{RespectsEquivalenceR A P, RespectsEquivalenceR A Q}
  : RespectsEquivalenceR A (fun B e => P B e * Q B e).
A: Type
P, Q: forall B : Type, B <~> A -> Type
H: RespectsEquivalenceR A P
H0: RespectsEquivalenceR A Q
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e * Q B e)
  Proof.
A: Type
P, Q: forall B : Type, B <~> A -> Type
H: RespectsEquivalenceR A P
H0: RespectsEquivalenceR A Q
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e * Q B e)
    refine ((fun B e => equiv_functor_prod' (respects_equivalenceR.1 B e) (respects_equivalenceR.1 B e)); _).
A: Type
P, Q: forall B : Type, B <~> A -> Type
H: RespectsEquivalenceR A P
H0: RespectsEquivalenceR A Q
Funext ->
1 =
respects_equivalenceR.1 A 1 *E
respects_equivalenceR.1 A 1
    exact (fun fs =>
             transport
               (fun e' => _ = equiv_functor_prod' e' _) (respects_equivalenceR.2 _)
               (transport
                  (fun e' => _ = equiv_functor_prod' _ e') (respects_equivalenceR.2 _)
                  idpath)).
  Defined.

  #[export] Instance: @respects_equivalence_db _ _ (@prod) (@prod_respects_equivalenceL) := tt.
End prod.

(** A tactic to solve the identity-preservation part of equivalence-respectfulness. *)
Local Ltac t_step :=
  idtac;
  match goal with
    | [ |- _ = _ :> (_ <~> _) ] => apply path_equiv
    | _ => reflexivity
    | _ => assumption
    | _ => intro
    | [ |- _ = _ :> (forall _, _) ] => apply path_forall
    | _ => progress unfold functor_forall, functor_sigma
    | _ => progress cbn in *
    | [ |- context[?x.1] ] => let H := fresh in destruct x as [? H]; try destruct H
    | [ H : _ = _ |- _ ] => destruct H
    | [ H : ?A -> ?B, H' : ?A |- _ ] => specialize (H H')
    | [ H : ?A -> ?B, H' : ?A |- _ ] => generalize dependent (H H'); clear H
    | _ => progress rewrite ?eisretr, ?eissect
  end.
Local Ltac t :=
  repeat t_step.

Section pi.
  #[export] Instance forall_respects_equivalenceL `{Funext} {A} {P : forall B, (A <~> B) -> Type} {Q : forall B e, P B e -> Type}
         `{HP : RespectsEquivalenceL A P}
         `{HQ : forall a : P A (equiv_idmap A), RespectsEquivalenceL A (fun B e => Q B e (respects_equivalenceL.1 B e a))}
  : RespectsEquivalenceL A (fun B e => forall x : P B e, Q B e x).
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   forall x : P B e, Q B e x)
  Proof.
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   forall x : P B e, Q B e x)
    simple refine (fun B e => _; _).
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
B: Type
e: A <~> B
(fun (B : Type) (e : A <~> B) =>
 forall x : P B e, Q B e x) A 1 <~>
(fun (B : Type) (e : A <~> B) =>
 forall x : P B e, Q B e x) B e
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
(fun
   e' : forall (B : Type) (e : A <~> B),
        (fun (B0 : Type) (e0 : A <~> B0) =>
         forall x : P B0 e0, Q B0 e0 x) A 1 <~>
        (fun (B0 : Type) (e0 : A <~> B0) =>
         forall x : P B0 e0, Q B0 e0 x) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : A <~> B) => ?Goal)
    {
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
B: Type
e: A <~> B
(fun (B : Type) (e : A <~> B) =>
 forall x : P B e, Q B e x) A 1 <~>
(fun (B : Type) (e : A <~> B) =>
 forall x : P B e, Q B e x) B e refine (equiv_functor_forall'
                (equiv_inverse ((@respects_equivalenceL _ _ HP).1 B e))
                (fun b => _)).
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
B: Type
e: A <~> B
b: P B e
Q A 1 ((respects_equivalenceL.1 B e)^-1 b) <~> Q B e b
      refine (equiv_compose'
                (equiv_path _ _ (ap (Q B e) (eisretr _ _)))
                (equiv_compose'
                   ((HQ (equiv_inverse ((@respects_equivalenceL _ _ HP).1 B e) b)).1 B e)
                   (equiv_path _ _ (ap (Q A (equiv_idmap _)) _)))).
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
B: Type
e: A <~> B
b: P B e
(respects_equivalenceL.1 B e)^-1 b =
respects_equivalenceL.1 A 1
  ((respects_equivalenceL.1 B e)^-1 b)
      refine (ap10 (ap equiv_fun (respects_equivalenceL.2 _)) _). }
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
(fun
   e' : forall (B : Type) (e : A <~> B),
        (fun (B0 : Type) (e0 : A <~> B0) =>
         forall x : P B0 e0, Q B0 e0 x) A 1 <~>
        (fun (B0 : Type) (e0 : A <~> B0) =>
         forall x : P B0 e0, Q B0 e0 x) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : A <~> B) =>
   equiv_functor_forall'
     (respects_equivalenceL.1 B e)^-1
     (fun b : P B e =>
      equiv_path
        (Q B e
           (respects_equivalenceL.1 B e
              ((respects_equivalenceL.1 B e)^-1%function
                 b))) (Q B e b)
        (ap (Q B e)
           (eisretr (respects_equivalenceL.1 B e) b))
      oE ((HQ ((respects_equivalenceL.1 B e)^-1 b)).1
            B e
          oE equiv_path
               (Q A 1
                  ((respects_equivalenceL.1 B e)^-1 b))
               (Q A 1
                  (respects_equivalenceL.1 A 1
                     ((respects_equivalenceL.1 B e)^-1
                        b)))
               (ap (Q A 1)
                  (ap10
                     (ap equiv_fun
                        (respects_equivalenceL.2 H))
                     ((respects_equivalenceL.1 B e)^-1%function
                        b))))))
    {
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
(fun
   e' : forall (B : Type) (e : A <~> B),
        (fun (B0 : Type) (e0 : A <~> B0) =>
         forall x : P B0 e0, Q B0 e0 x) A 1 <~>
        (fun (B0 : Type) (e0 : A <~> B0) =>
         forall x : P B0 e0, Q B0 e0 x) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : A <~> B) =>
   equiv_functor_forall'
     (respects_equivalenceL.1 B e)^-1
     (fun b : P B e =>
      equiv_path
        (Q B e
           (respects_equivalenceL.1 B e
              ((respects_equivalenceL.1 B e)^-1%function
                 b))) (Q B e b)
        (ap (Q B e)
           (eisretr (respects_equivalenceL.1 B e) b))
      oE ((HQ ((respects_equivalenceL.1 B e)^-1 b)).1
            B e
          oE equiv_path
               (Q A 1
                  ((respects_equivalenceL.1 B e)^-1 b))
               (Q A 1
                  (respects_equivalenceL.1 A 1
                     ((respects_equivalenceL.1 B e)^-1
                        b)))
               (ap (Q A 1)
                  (ap10
                     (ap equiv_fun
                        (respects_equivalenceL.2 H))
                     ((respects_equivalenceL.1 B e)^-1%function
                        b)))))) t. }
  Defined.

  #[export] Instance forall_respects_equivalenceR `{Funext} {A} {P : forall B, (B <~> A) -> Type} {Q : forall B e, P B e -> Type}
         `{HP : RespectsEquivalenceR A P}
         `{HQ : forall a : P A (equiv_idmap A), RespectsEquivalenceR A (fun B e => Q B e (respects_equivalenceR.1 B e a))}
  : RespectsEquivalenceR A (fun B e => forall x : P B e, Q B e x).
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   forall x : P B e, Q B e x)
  Proof.
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   forall x : P B e, Q B e x)
    simple refine (fun B e => _; _).
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
B: Type
e: B <~> A
(fun (B : Type) (e : B <~> A) =>
 forall x : P B e, Q B e x) A 1 <~>
(fun (B : Type) (e : B <~> A) =>
 forall x : P B e, Q B e x) B e
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
(fun
   e' : forall (B : Type) (e : B <~> A),
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         forall x : P B0 e0, Q B0 e0 x) A 1 <~>
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         forall x : P B0 e0, Q B0 e0 x) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : B <~> A) => ?Goal)
    {
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
B: Type
e: B <~> A
(fun (B : Type) (e : B <~> A) =>
 forall x : P B e, Q B e x) A 1 <~>
(fun (B : Type) (e : B <~> A) =>
 forall x : P B e, Q B e x) B e refine (equiv_functor_forall'
                (equiv_inverse ((@respects_equivalenceR _ _ HP).1 B e))
                (fun b => _)).
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
B: Type
e: B <~> A
b: P B e
Q A 1 ((respects_equivalenceR.1 B e)^-1 b) <~> Q B e b
      refine (equiv_compose'
                (equiv_path _ _ (ap (Q B e) (eisretr _ _)))
                (equiv_compose'
                   ((HQ (equiv_inverse ((@respects_equivalenceR _ _ HP).1 B e) b)).1 B e)
                   (equiv_path _ _ (ap (Q A (equiv_idmap _)) _)))).
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
B: Type
e: B <~> A
b: P B e
(respects_equivalenceR.1 B e)^-1 b =
respects_equivalenceR.1 A 1
  ((respects_equivalenceR.1 B e)^-1 b)
      refine (ap10 (ap equiv_fun (respects_equivalenceR.2 _)) _). }
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
(fun
   e' : forall (B : Type) (e : B <~> A),
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         forall x : P B0 e0, Q B0 e0 x) A 1 <~>
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         forall x : P B0 e0, Q B0 e0 x) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : B <~> A) =>
   equiv_functor_forall'
     (respects_equivalenceR.1 B e)^-1
     (fun b : P B e =>
      equiv_path
        (Q B e
           (respects_equivalenceR.1 B e
              ((respects_equivalenceR.1 B e)^-1%function
                 b))) (Q B e b)
        (ap (Q B e)
           (eisretr (respects_equivalenceR.1 B e) b))
      oE ((HQ ((respects_equivalenceR.1 B e)^-1 b)).1
            B e
          oE equiv_path
               (Q A 1
                  ((respects_equivalenceR.1 B e)^-1 b))
               (Q A 1
                  (respects_equivalenceR.1 A 1
                     ((respects_equivalenceR.1 B e)^-1
                        b)))
               (ap (Q A 1)
                  (ap10
                     (ap equiv_fun
                        (respects_equivalenceR.2 H))
                     ((respects_equivalenceR.1 B e)^-1%function
                        b))))))
    {
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
(fun
   e' : forall (B : Type) (e : B <~> A),
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         forall x : P B0 e0, Q B0 e0 x) A 1 <~>
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         forall x : P B0 e0, Q B0 e0 x) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : B <~> A) =>
   equiv_functor_forall'
     (respects_equivalenceR.1 B e)^-1
     (fun b : P B e =>
      equiv_path
        (Q B e
           (respects_equivalenceR.1 B e
              ((respects_equivalenceR.1 B e)^-1%function
                 b))) (Q B e b)
        (ap (Q B e)
           (eisretr (respects_equivalenceR.1 B e) b))
      oE ((HQ ((respects_equivalenceR.1 B e)^-1 b)).1
            B e
          oE equiv_path
               (Q A 1
                  ((respects_equivalenceR.1 B e)^-1 b))
               (Q A 1
                  (respects_equivalenceR.1 A 1
                     ((respects_equivalenceR.1 B e)^-1
                        b)))
               (ap (Q A 1)
                  (ap10
                     (ap equiv_fun
                        (respects_equivalenceR.2 H))
                     ((respects_equivalenceR.1 B e)^-1%function
                        b)))))) t. }
  Defined.
End pi.

Section sigma.
  #[export] Instance sigma_respects_equivalenceL `{Funext} {A} {P : forall B, (A <~> B) -> Type} {Q : forall B e, P B e -> Type}
         `{HP : RespectsEquivalenceL A P}
         `{HQ : forall a : P A (equiv_idmap A), RespectsEquivalenceL A (fun B e => Q B e (respects_equivalenceL.1 B e a))}
  : RespectsEquivalenceL A (fun B e => sig (Q B e)).
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => {x : _ & Q B e x})
  Proof.
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => {x : _ & Q B e x})
    simple refine ((fun B e => equiv_functor_sigma' (respects_equivalenceL.1 B e) (fun b => _));
            _).
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
B: Type
e: A <~> B
b: P A 1
Q A 1 b <~> Q B e (respects_equivalenceL.1 B e b)
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
(fun
   e' : forall (B : Type) (e : A <~> B),
        (fun (B0 : Type) (e0 : A <~> B0) =>
         {x : _ & Q B0 e0 x}) A 1 <~>
        (fun (B0 : Type) (e0 : A <~> B0) =>
         {x : _ & Q B0 e0 x}) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : A <~> B) =>
   equiv_functor_sigma' (respects_equivalenceL.1 B e)
     (fun b : P A 1 => ?Goal))
    {
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
B: Type
e: A <~> B
b: P A 1
Q A 1 b <~> Q B e (respects_equivalenceL.1 B e b) refine (equiv_compose'
                ((HQ b).1 B e)
                (equiv_path _ _ (ap (Q A (equiv_idmap _)) _))).
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
B: Type
e: A <~> B
b: P A 1
b = respects_equivalenceL.1 A 1 b
      refine (ap10 (ap equiv_fun (respects_equivalenceL.2 _)) _). }
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
(fun
   e' : forall (B : Type) (e : A <~> B),
        (fun (B0 : Type) (e0 : A <~> B0) =>
         {x : _ & Q B0 e0 x}) A 1 <~>
        (fun (B0 : Type) (e0 : A <~> B0) =>
         {x : _ & Q B0 e0 x}) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : A <~> B) =>
   equiv_functor_sigma' (respects_equivalenceL.1 B e)
     (fun b : P A 1 =>
      (HQ b).1 B e
      oE equiv_path (Q A 1 b)
           (Q A 1 (respects_equivalenceL.1 A 1 b))
           (ap (Q A 1)
              (ap10
                 (ap equiv_fun
                    (respects_equivalenceL.2 H)) b))))
    {
H: Funext
A: Type
P: forall B : Type, A <~> B -> Type
Q: forall (B : Type) (e : A <~> B), P B e -> Type
HP: RespectsEquivalenceL A P
HQ: forall a : P A 1,
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Q B e (respects_equivalenceL.1 B e a))
(fun
   e' : forall (B : Type) (e : A <~> B),
        (fun (B0 : Type) (e0 : A <~> B0) =>
         {x : _ & Q B0 e0 x}) A 1 <~>
        (fun (B0 : Type) (e0 : A <~> B0) =>
         {x : _ & Q B0 e0 x}) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : A <~> B) =>
   equiv_functor_sigma' (respects_equivalenceL.1 B e)
     (fun b : P A 1 =>
      (HQ b).1 B e
      oE equiv_path (Q A 1 b)
           (Q A 1 (respects_equivalenceL.1 A 1 b))
           (ap (Q A 1)
              (ap10
                 (ap equiv_fun
                    (respects_equivalenceL.2 H)) b)))) t. }
  Defined.

  #[export] Instance sigma_respects_equivalenceR `{Funext} {A} {P : forall B, (B <~> A) -> Type} {Q : forall B e, P B e -> Type}
         `{HP : RespectsEquivalenceR A P}
         `{HQ : forall a : P A (equiv_idmap A), RespectsEquivalenceR A (fun B e => Q B e (respects_equivalenceR.1 B e a))}
  : RespectsEquivalenceR A (fun B e => sig (Q B e)).
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => {x : _ & Q B e x})
  Proof.
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => {x : _ & Q B e x})
    simple refine ((fun B e => equiv_functor_sigma' (respects_equivalenceR.1 B e) (fun b => _));
            _).
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
B: Type
e: B <~> A
b: P A 1
Q A 1 b <~> Q B e (respects_equivalenceR.1 B e b)
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
(fun
   e' : forall (B : Type) (e : B <~> A),
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         {x : _ & Q B0 e0 x}) A 1 <~>
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         {x : _ & Q B0 e0 x}) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : B <~> A) =>
   equiv_functor_sigma' (respects_equivalenceR.1 B e)
     (fun b : P A 1 => ?Goal))
    {
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
B: Type
e: B <~> A
b: P A 1
Q A 1 b <~> Q B e (respects_equivalenceR.1 B e b) refine (equiv_compose'
                ((HQ b).1 B e)
                (equiv_path _ _ (ap (Q A (equiv_idmap _)) _))).
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
B: Type
e: B <~> A
b: P A 1
b = respects_equivalenceR.1 A 1 b
      refine (ap10 (ap equiv_fun (respects_equivalenceR.2 _)) _). }
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
(fun
   e' : forall (B : Type) (e : B <~> A),
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         {x : _ & Q B0 e0 x}) A 1 <~>
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         {x : _ & Q B0 e0 x}) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : B <~> A) =>
   equiv_functor_sigma' (respects_equivalenceR.1 B e)
     (fun b : P A 1 =>
      (HQ b).1 B e
      oE equiv_path (Q A 1 b)
           (Q A 1 (respects_equivalenceR.1 A 1 b))
           (ap (Q A 1)
              (ap10
                 (ap equiv_fun
                    (respects_equivalenceR.2 H)) b))))
    {
H: Funext
A: Type
P: forall B : Type, B <~> A -> Type
Q: forall (B : Type) (e : B <~> A), P B e -> Type
HP: RespectsEquivalenceR A P
HQ: forall a : P A 1,
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   Q B e (respects_equivalenceR.1 B e a))
(fun
   e' : forall (B : Type) (e : B <~> A),
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         {x : _ & Q B0 e0 x}) A 1 <~>
        (fun (B0 : Type) (e0 : B0 <~> A) =>
         {x : _ & Q B0 e0 x}) B e =>
 Funext -> 1 = e' A 1)
  (fun (B : Type) (e : B <~> A) =>
   equiv_functor_sigma' (respects_equivalenceR.1 B e)
     (fun b : P A 1 =>
      (HQ b).1 B e
      oE equiv_path (Q A 1 b)
           (Q A 1 (respects_equivalenceR.1 A 1 b))
           (ap (Q A 1)
              (ap10
                 (ap equiv_fun
                    (respects_equivalenceR.2 H)) b)))) t. }
  Defined.

  #[export] Instance: @respects_equivalence_db _ _ (@sig) (@sigma_respects_equivalenceL) := tt.
End sigma.

Section equiv_transfer.
  Definition respects_equivalenceL_equiv {A A'} {P : forall B, (A <~> B) -> Type} {P' : forall B, A' <~> B -> Type}
             (eA : A <~> A')
             (eP : forall B e, P B (equiv_compose' e eA) <~> P' B e)
             `{HP : RespectsEquivalenceL A P}
  : RespectsEquivalenceL A' P'.
A, A': Type
P: forall B : Type, A <~> B -> Type
P': forall B : Type, A' <~> B -> Type
eA: A <~> A'
eP: forall (B : Type) (e : A' <~> B),
P B (e oE eA) <~> P' B e
HP: RespectsEquivalenceL A P
RespectsEquivalenceL A' P'
  Proof.
A, A': Type
P: forall B : Type, A <~> B -> Type
P': forall B : Type, A' <~> B -> Type
eA: A <~> A'
eP: forall (B : Type) (e : A' <~> B),
P B (e oE eA) <~> P' B e
HP: RespectsEquivalenceL A P
RespectsEquivalenceL A' P'
    simple refine ((fun B e => _); _).
A, A': Type
P: forall B : Type, A <~> B -> Type
P': forall B : Type, A' <~> B -> Type
eA: A <~> A'
eP: forall (B : Type) (e : A' <~> B),
P B (e oE eA) <~> P' B e
HP: RespectsEquivalenceL A P
B: Type
e: A' <~> B
P' A' 1 <~> P' B e
A, A': Type
P: forall B : Type, A <~> B -> Type
P': forall B : Type, A' <~> B -> Type
eA: A <~> A'
eP: forall (B : Type) (e : A' <~> B),
P B (e oE eA) <~> P' B e
HP: RespectsEquivalenceL A P
(fun
   e' : forall (B : Type) (e : A' <~> B),
        P' A' 1 <~> P' B e => Funext -> 1 = e' A' 1)
  (fun (B : Type) (e : A' <~> B) => ?Goal)
    {
A, A': Type
P: forall B : Type, A <~> B -> Type
P': forall B : Type, A' <~> B -> Type
eA: A <~> A'
eP: forall (B : Type) (e : A' <~> B),
P B (e oE eA) <~> P' B e
HP: RespectsEquivalenceL A P
B: Type
e: A' <~> B
P' A' 1 <~> P' B e refine (equiv_compose'
                (eP _ _)
                (equiv_compose'
                   (equiv_compose'
                      (HP.1 _ _)
                      (equiv_inverse (HP.1 _ _)))
                   (equiv_inverse (eP _ _)))). }
A, A': Type
P: forall B : Type, A <~> B -> Type
P': forall B : Type, A' <~> B -> Type
eA: A <~> A'
eP: forall (B : Type) (e : A' <~> B),
P B (e oE eA) <~> P' B e
HP: RespectsEquivalenceL A P
(fun
   e' : forall (B : Type) (e : A' <~> B),
        P' A' 1 <~> P' B e => Funext -> 1 = e' A' 1)
  (fun (B : Type) (e : A' <~> B) =>
   eP B e
   oE (HP.1 B (e oE eA) oE (HP.1 A' (1 oE eA))^-1
       oE (eP A' 1)^-1))
    {
A, A': Type
P: forall B : Type, A <~> B -> Type
P': forall B : Type, A' <~> B -> Type
eA: A <~> A'
eP: forall (B : Type) (e : A' <~> B),
P B (e oE eA) <~> P' B e
HP: RespectsEquivalenceL A P
(fun
   e' : forall (B : Type) (e : A' <~> B),
        P' A' 1 <~> P' B e => Funext -> 1 = e' A' 1)
  (fun (B : Type) (e : A' <~> B) =>
   eP B e
   oE (HP.1 B (e oE eA) oE (HP.1 A' (1 oE eA))^-1
       oE (eP A' 1)^-1)) t. }
  Defined.

  Definition respects_equivalenceR_equiv {A A'} {P : forall B, (B <~> A) -> Type} {P' : forall B, B <~> A' -> Type}
             (eA : A' <~> A)
             (eP : forall B e, P B (equiv_compose' eA e) <~> P' B e)
             `{HP : RespectsEquivalenceR A P}
  : RespectsEquivalenceR A' P'.
A, A': Type
P: forall B : Type, B <~> A -> Type
P': forall B : Type, B <~> A' -> Type
eA: A' <~> A
eP: forall (B : Type) (e : B <~> A'),
P B (eA oE e) <~> P' B e
HP: RespectsEquivalenceR A P
RespectsEquivalenceR A' P'
  Proof.
A, A': Type
P: forall B : Type, B <~> A -> Type
P': forall B : Type, B <~> A' -> Type
eA: A' <~> A
eP: forall (B : Type) (e : B <~> A'),
P B (eA oE e) <~> P' B e
HP: RespectsEquivalenceR A P
RespectsEquivalenceR A' P'
    simple refine ((fun B e => _); _).
A, A': Type
P: forall B : Type, B <~> A -> Type
P': forall B : Type, B <~> A' -> Type
eA: A' <~> A
eP: forall (B : Type) (e : B <~> A'),
P B (eA oE e) <~> P' B e
HP: RespectsEquivalenceR A P
B: Type
e: B <~> A'
P' A' 1 <~> P' B e
A, A': Type
P: forall B : Type, B <~> A -> Type
P': forall B : Type, B <~> A' -> Type
eA: A' <~> A
eP: forall (B : Type) (e : B <~> A'),
P B (eA oE e) <~> P' B e
HP: RespectsEquivalenceR A P
(fun
   e' : forall (B : Type) (e : B <~> A'),
        P' A' 1 <~> P' B e => Funext -> 1 = e' A' 1)
  (fun (B : Type) (e : B <~> A') => ?Goal)
    {
A, A': Type
P: forall B : Type, B <~> A -> Type
P': forall B : Type, B <~> A' -> Type
eA: A' <~> A
eP: forall (B : Type) (e : B <~> A'),
P B (eA oE e) <~> P' B e
HP: RespectsEquivalenceR A P
B: Type
e: B <~> A'
P' A' 1 <~> P' B e refine (equiv_compose'
                (eP _ _)
                (equiv_compose'
                   (equiv_compose'
                      (HP.1 _ _)
                      (equiv_inverse (HP.1 _ _)))
                   (equiv_inverse (eP _ _)))). }
A, A': Type
P: forall B : Type, B <~> A -> Type
P': forall B : Type, B <~> A' -> Type
eA: A' <~> A
eP: forall (B : Type) (e : B <~> A'),
P B (eA oE e) <~> P' B e
HP: RespectsEquivalenceR A P
(fun
   e' : forall (B : Type) (e : B <~> A'),
        P' A' 1 <~> P' B e => Funext -> 1 = e' A' 1)
  (fun (B : Type) (e : B <~> A') =>
   eP B e
   oE (HP.1 B (eA oE e) oE (HP.1 A' (eA oE 1))^-1
       oE (eP A' 1)^-1))
    {
A, A': Type
P: forall B : Type, B <~> A -> Type
P': forall B : Type, B <~> A' -> Type
eA: A' <~> A
eP: forall (B : Type) (e : B <~> A'),
P B (eA oE e) <~> P' B e
HP: RespectsEquivalenceR A P
(fun
   e' : forall (B : Type) (e : B <~> A'),
        P' A' 1 <~> P' B e => Funext -> 1 = e' A' 1)
  (fun (B : Type) (e : B <~> A') =>
   eP B e
   oE (HP.1 B (eA oE e) oE (HP.1 A' (eA oE 1))^-1
       oE (eP A' 1)^-1)) t. }
  Defined.

  Definition respects_equivalenceL_equiv' {A} {P P' : forall B, (A <~> B) -> Type}
             (eP : forall B e, P B e <~> P' B e)
             `{HP : RespectsEquivalenceL A P}
  : RespectsEquivalenceL A P'.
A: Type
P, P': forall B : Type, A <~> B -> Type
eP: forall (B : Type) (e : A <~> B), P B e <~> P' B e
HP: RespectsEquivalenceL A P
RespectsEquivalenceL A P'
  Proof.
A: Type
P, P': forall B : Type, A <~> B -> Type
eP: forall (B : Type) (e : A <~> B), P B e <~> P' B e
HP: RespectsEquivalenceL A P
RespectsEquivalenceL A P'
    simple refine ((fun B e => _); _).
A: Type
P, P': forall B : Type, A <~> B -> Type
eP: forall (B : Type) (e : A <~> B), P B e <~> P' B e
HP: RespectsEquivalenceL A P
B: Type
e: A <~> B
P' A 1 <~> P' B e
A: Type
P, P': forall B : Type, A <~> B -> Type
eP: forall (B : Type) (e : A <~> B), P B e <~> P' B e
HP: RespectsEquivalenceL A P
(fun
   e' : forall (B : Type) (e : A <~> B),
        P' A 1 <~> P' B e => Funext -> 1 = e' A 1)
  (fun (B : Type) (e : A <~> B) => ?Goal)
    {
A: Type
P, P': forall B : Type, A <~> B -> Type
eP: forall (B : Type) (e : A <~> B), P B e <~> P' B e
HP: RespectsEquivalenceL A P
B: Type
e: A <~> B
P' A 1 <~> P' B e refine (equiv_compose'
                (eP _ _)
                (equiv_compose'
                   (equiv_compose'
                      (HP.1 _ _)
                      (equiv_inverse (HP.1 _ _)))
                   (equiv_inverse (eP _ _)))). }
A: Type
P, P': forall B : Type, A <~> B -> Type
eP: forall (B : Type) (e : A <~> B), P B e <~> P' B e
HP: RespectsEquivalenceL A P
(fun
   e' : forall (B : Type) (e : A <~> B),
        P' A 1 <~> P' B e => Funext -> 1 = e' A 1)
  (fun (B : Type) (e : A <~> B) =>
   eP B e
   oE (HP.1 B e oE (HP.1 A 1)^-1 oE (eP A 1)^-1))
    {
A: Type
P, P': forall B : Type, A <~> B -> Type
eP: forall (B : Type) (e : A <~> B), P B e <~> P' B e
HP: RespectsEquivalenceL A P
(fun
   e' : forall (B : Type) (e : A <~> B),
        P' A 1 <~> P' B e => Funext -> 1 = e' A 1)
  (fun (B : Type) (e : A <~> B) =>
   eP B e
   oE (HP.1 B e oE (HP.1 A 1)^-1 oE (eP A 1)^-1)) t. }
  Defined.

  Definition respects_equivalenceR_equiv' {A} {P P' : forall B, (B <~> A) -> Type}
             (eP : forall B e, P B e <~> P' B e)
             `{HP : RespectsEquivalenceR A P}
  : RespectsEquivalenceR A P'.
A: Type
P, P': forall B : Type, B <~> A -> Type
eP: forall (B : Type) (e : B <~> A), P B e <~> P' B e
HP: RespectsEquivalenceR A P
RespectsEquivalenceR A P'
  Proof.
A: Type
P, P': forall B : Type, B <~> A -> Type
eP: forall (B : Type) (e : B <~> A), P B e <~> P' B e
HP: RespectsEquivalenceR A P
RespectsEquivalenceR A P'
    simple refine ((fun B e => _); _).
A: Type
P, P': forall B : Type, B <~> A -> Type
eP: forall (B : Type) (e : B <~> A), P B e <~> P' B e
HP: RespectsEquivalenceR A P
B: Type
e: B <~> A
P' A 1 <~> P' B e
A: Type
P, P': forall B : Type, B <~> A -> Type
eP: forall (B : Type) (e : B <~> A), P B e <~> P' B e
HP: RespectsEquivalenceR A P
(fun
   e' : forall (B : Type) (e : B <~> A),
        P' A 1 <~> P' B e => Funext -> 1 = e' A 1)
  (fun (B : Type) (e : B <~> A) => ?Goal)
    {
A: Type
P, P': forall B : Type, B <~> A -> Type
eP: forall (B : Type) (e : B <~> A), P B e <~> P' B e
HP: RespectsEquivalenceR A P
B: Type
e: B <~> A
P' A 1 <~> P' B e refine (equiv_compose'
                (eP _ _)
                (equiv_compose'
                   (equiv_compose'
                      (HP.1 _ _)
                      (equiv_inverse (HP.1 _ _)))
                   (equiv_inverse (eP _ _)))). }
A: Type
P, P': forall B : Type, B <~> A -> Type
eP: forall (B : Type) (e : B <~> A), P B e <~> P' B e
HP: RespectsEquivalenceR A P
(fun
   e' : forall (B : Type) (e : B <~> A),
        P' A 1 <~> P' B e => Funext -> 1 = e' A 1)
  (fun (B : Type) (e : B <~> A) =>
   eP B e
   oE (HP.1 B e oE (HP.1 A 1)^-1 oE (eP A 1)^-1))
    {
A: Type
P, P': forall B : Type, B <~> A -> Type
eP: forall (B : Type) (e : B <~> A), P B e <~> P' B e
HP: RespectsEquivalenceR A P
(fun
   e' : forall (B : Type) (e : B <~> A),
        P' A 1 <~> P' B e => Funext -> 1 = e' A 1)
  (fun (B : Type) (e : B <~> A) =>
   eP B e
   oE (HP.1 B e oE (HP.1 A 1)^-1 oE (eP A 1)^-1)) t. }
  Defined.
End equiv_transfer.

Section equiv.
  #[export] Instance equiv_respects_equivalenceL `{Funext} {A} {P Q : forall B, (A <~> B) -> Type}
         `{HP : RespectsEquivalenceL A P}
         `{HQ : RespectsEquivalenceL A Q}
  : RespectsEquivalenceL A (fun B e => P B e <~> Q B e).
H: Funext
A: Type
P, Q: forall B : Type, A <~> B -> Type
HP: RespectsEquivalenceL A P
HQ: RespectsEquivalenceL A Q
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e <~> Q B e)
  Proof.
H: Funext
A: Type
P, Q: forall B : Type, A <~> B -> Type
HP: RespectsEquivalenceL A P
HQ: RespectsEquivalenceL A Q
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e <~> Q B e)
    simple refine (fun B e => _; fun _ => _).
H: Funext
A: Type
P, Q: forall B : Type, A <~> B -> Type
HP: RespectsEquivalenceL A P
HQ: RespectsEquivalenceL A Q
B: Type
e: A <~> B
(fun (B : Type) (e : A <~> B) => P B e <~> Q B e) A 1 <~>
(fun (B : Type) (e : A <~> B) => P B e <~> Q B e) B e
H: Funext
A: Type
P, Q: forall B : Type, A <~> B -> Type
HP: RespectsEquivalenceL A P
HQ: RespectsEquivalenceL A Q
y: Funext
1 = (fun (B : Type) (e : A <~> B) => ?Goal) A 1
    {
H: Funext
A: Type
P, Q: forall B : Type, A <~> B -> Type
HP: RespectsEquivalenceL A P
HQ: RespectsEquivalenceL A Q
B: Type
e: A <~> B
(fun (B : Type) (e : A <~> B) => P B e <~> Q B e) A 1 <~>
(fun (B : Type) (e : A <~> B) => P B e <~> Q B e) B e refine (equiv_functor_equiv _ _);
      apply respects_equivalenceL.1. }
H: Funext
A: Type
P, Q: forall B : Type, A <~> B -> Type
HP: RespectsEquivalenceL A P
HQ: RespectsEquivalenceL A Q
y: Funext
1 =
(fun (B : Type) (e : A <~> B) =>
 equiv_functor_equiv (respects_equivalenceL.1 B e)
   (respects_equivalenceL.1 B e)) A 1
    {
H: Funext
A: Type
P, Q: forall B : Type, A <~> B -> Type
HP: RespectsEquivalenceL A P
HQ: RespectsEquivalenceL A Q
y: Funext
1 =
(fun (B : Type) (e : A <~> B) =>
 equiv_functor_equiv (respects_equivalenceL.1 B e)
   (respects_equivalenceL.1 B e)) A 1 t. }
  Defined.

  #[export] Instance equiv_respects_equivalenceR `{Funext} {A} {P Q : forall B, (B <~> A) -> Type}
         `{HP : RespectsEquivalenceR A P}
         `{HQ : RespectsEquivalenceR A Q}
  : RespectsEquivalenceR A (fun B e => P B e <~> Q B e).
H: Funext
A: Type
P, Q: forall B : Type, B <~> A -> Type
HP: RespectsEquivalenceR A P
HQ: RespectsEquivalenceR A Q
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e <~> Q B e)
  Proof.
H: Funext
A: Type
P, Q: forall B : Type, B <~> A -> Type
HP: RespectsEquivalenceR A P
HQ: RespectsEquivalenceR A Q
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e <~> Q B e)
    simple refine (fun B e => _; fun _ => _).
H: Funext
A: Type
P, Q: forall B : Type, B <~> A -> Type
HP: RespectsEquivalenceR A P
HQ: RespectsEquivalenceR A Q
B: Type
e: B <~> A
(fun (B : Type) (e : B <~> A) => P B e <~> Q B e) A 1 <~>
(fun (B : Type) (e : B <~> A) => P B e <~> Q B e) B e
H: Funext
A: Type
P, Q: forall B : Type, B <~> A -> Type
HP: RespectsEquivalenceR A P
HQ: RespectsEquivalenceR A Q
y: Funext
1 = (fun (B : Type) (e : B <~> A) => ?Goal) A 1
    {
H: Funext
A: Type
P, Q: forall B : Type, B <~> A -> Type
HP: RespectsEquivalenceR A P
HQ: RespectsEquivalenceR A Q
B: Type
e: B <~> A
(fun (B : Type) (e : B <~> A) => P B e <~> Q B e) A 1 <~>
(fun (B : Type) (e : B <~> A) => P B e <~> Q B e) B e refine (equiv_functor_equiv _ _);
      apply respects_equivalenceR.1. }
H: Funext
A: Type
P, Q: forall B : Type, B <~> A -> Type
HP: RespectsEquivalenceR A P
HQ: RespectsEquivalenceR A Q
y: Funext
1 =
(fun (B : Type) (e : B <~> A) =>
 equiv_functor_equiv (respects_equivalenceR.1 B e)
   (respects_equivalenceR.1 B e)) A 1
    {
H: Funext
A: Type
P, Q: forall B : Type, B <~> A -> Type
HP: RespectsEquivalenceR A P
HQ: RespectsEquivalenceR A Q
y: Funext
1 =
(fun (B : Type) (e : B <~> A) =>
 equiv_functor_equiv (respects_equivalenceR.1 B e)
   (respects_equivalenceR.1 B e)) A 1 t. }
  Defined.

  #[export] Instance: @respects_equivalence_db _ _ (@Equiv) (@equiv_respects_equivalenceL) := tt.
End equiv.

Section ap.
  #[export] Instance equiv_ap_respects_equivalenceL {A} {P Q : forall B, (A <~> B) -> A}
         `{HP : RespectsEquivalenceL A (fun B (e : A <~> B) => P B e = Q B e)}
  : RespectsEquivalenceL A (fun (B : Type) (e : A <~> B) => e (P B e) = e (Q B e)).
A: Type
P, Q: forall B : Type, A <~> B -> A
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   e (P B e) = e (Q B e))
  Proof.
A: Type
P, Q: forall B : Type, A <~> B -> A
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   e (P B e) = e (Q B e))
    simple refine (fun B e => _; fun _ => _).
A: Type
P, Q: forall B : Type, A <~> B -> A
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
B: Type
e: A <~> B
(fun (B : Type) (e : A <~> B) => e (P B e) = e (Q B e))
  A 1 <~>
(fun (B : Type) (e : A <~> B) => e (P B e) = e (Q B e))
  B e
A: Type
P, Q: forall B : Type, A <~> B -> A
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
y: Funext
1 = (fun (B : Type) (e : A <~> B) => ?Goal) A 1
    {
A: Type
P, Q: forall B : Type, A <~> B -> A
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
B: Type
e: A <~> B
(fun (B : Type) (e : A <~> B) => e (P B e) = e (Q B e))
  A 1 <~>
(fun (B : Type) (e : A <~> B) => e (P B e) = e (Q B e))
  B e refine (equiv_ap' _ _ _ oE _); simpl.
A: Type
P, Q: forall B : Type, A <~> B -> A
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
B: Type
e: A <~> B
P A 1 = Q A 1 <~> P B e = Q B e
      refine (respects_equivalenceL.1 B e). }
A: Type
P, Q: forall B : Type, A <~> B -> A
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
y: Funext
1 =
(fun (B : Type) (e : A <~> B) =>
 equiv_ap' e (P B e) (Q B e)
 oE (respects_equivalenceL.1 B e
     :
     1 (P A 1) = 1 (Q A 1) <~> P B e = Q B e)) A 1
    {
A: Type
P, Q: forall B : Type, A <~> B -> A
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
y: Funext
1 =
(fun (B : Type) (e : A <~> B) =>
 equiv_ap' e (P B e) (Q B e)
 oE (respects_equivalenceL.1 B e
     :
     1 (P A 1) = 1 (Q A 1) <~> P B e = Q B e)) A 1 t. }
  Defined.

  #[export] Instance equiv_ap_inv_respects_equivalenceL {A} {P Q : forall B, (A <~> B) -> B}
         `{HP : RespectsEquivalenceL A (fun B (e : A <~> B) => P B e = Q B e)}
  : RespectsEquivalenceL A (fun (B : Type) (e : A <~> B) => e^-1 (P B e) = e^-1 (Q B e)).
A: Type
P, Q: forall B : Type, A <~> B -> B
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   e^-1 (P B e) = e^-1 (Q B e))
  Proof.
A: Type
P, Q: forall B : Type, A <~> B -> B
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   e^-1 (P B e) = e^-1 (Q B e))
    simple refine (fun B e => _; fun _ => _).
A: Type
P, Q: forall B : Type, A <~> B -> B
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
B: Type
e: A <~> B
(fun (B : Type) (e : A <~> B) =>
 e^-1 (P B e) = e^-1 (Q B e)) A 1 <~>
(fun (B : Type) (e : A <~> B) =>
 e^-1 (P B e) = e^-1 (Q B e)) B e
A: Type
P, Q: forall B : Type, A <~> B -> B
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
y: Funext
1 = (fun (B : Type) (e : A <~> B) => ?Goal) A 1
    {
A: Type
P, Q: forall B : Type, A <~> B -> B
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
B: Type
e: A <~> B
(fun (B : Type) (e : A <~> B) =>
 e^-1 (P B e) = e^-1 (Q B e)) A 1 <~>
(fun (B : Type) (e : A <~> B) =>
 e^-1 (P B e) = e^-1 (Q B e)) B e refine (equiv_ap' _ _ _ oE _); simpl.
A: Type
P, Q: forall B : Type, A <~> B -> B
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
B: Type
e: A <~> B
P A 1 = Q A 1 <~> P B e = Q B e
      refine (respects_equivalenceL.1 B e). }
A: Type
P, Q: forall B : Type, A <~> B -> B
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
y: Funext
1 =
(fun (B : Type) (e : A <~> B) =>
 equiv_ap' e^-1 (P B e) (Q B e)
 oE (respects_equivalenceL.1 B e
     :
     1^-1 (P A 1) = 1^-1 (Q A 1) <~> P B e = Q B e)) A
  1
    {
A: Type
P, Q: forall B : Type, A <~> B -> B
HP: RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => P B e = Q B e)
y: Funext
1 =
(fun (B : Type) (e : A <~> B) =>
 equiv_ap' e^-1 (P B e) (Q B e)
 oE (respects_equivalenceL.1 B e
     :
     1^-1 (P A 1) = 1^-1 (Q A 1) <~> P B e = Q B e)) A
  1 t. }
  Defined.

  #[export] Instance equiv_ap_respects_equivalenceR {A} {P Q : forall B, (B <~> A) -> B}
         `{HP : RespectsEquivalenceR A (fun B (e : B <~> A) => P B e = Q B e)}
  : RespectsEquivalenceR A (fun (B : Type) (e : B <~> A) => e (P B e) = e (Q B e)).
A: Type
P, Q: forall B : Type, B <~> A -> B
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   e (P B e) = e (Q B e))
  Proof.
A: Type
P, Q: forall B : Type, B <~> A -> B
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   e (P B e) = e (Q B e))
    simple refine (fun B e => _; fun _ => _).
A: Type
P, Q: forall B : Type, B <~> A -> B
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
B: Type
e: B <~> A
(fun (B : Type) (e : B <~> A) => e (P B e) = e (Q B e))
  A 1 <~>
(fun (B : Type) (e : B <~> A) => e (P B e) = e (Q B e))
  B e
A: Type
P, Q: forall B : Type, B <~> A -> B
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
y: Funext
1 = (fun (B : Type) (e : B <~> A) => ?Goal) A 1
    {
A: Type
P, Q: forall B : Type, B <~> A -> B
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
B: Type
e: B <~> A
(fun (B : Type) (e : B <~> A) => e (P B e) = e (Q B e))
  A 1 <~>
(fun (B : Type) (e : B <~> A) => e (P B e) = e (Q B e))
  B e refine (equiv_ap' _ _ _ oE _); simpl.
A: Type
P, Q: forall B : Type, B <~> A -> B
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
B: Type
e: B <~> A
P A 1 = Q A 1 <~> P B e = Q B e
      refine (respects_equivalenceR.1 B e). }
A: Type
P, Q: forall B : Type, B <~> A -> B
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
y: Funext
1 =
(fun (B : Type) (e : B <~> A) =>
 equiv_ap' e (P B e) (Q B e)
 oE (respects_equivalenceR.1 B e
     :
     1 (P A 1) = 1 (Q A 1) <~> P B e = Q B e)) A 1
    {
A: Type
P, Q: forall B : Type, B <~> A -> B
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
y: Funext
1 =
(fun (B : Type) (e : B <~> A) =>
 equiv_ap' e (P B e) (Q B e)
 oE (respects_equivalenceR.1 B e
     :
     1 (P A 1) = 1 (Q A 1) <~> P B e = Q B e)) A 1 t. }
  Defined.

  #[export] Instance equiv_ap_inv_respects_equivalenceR {A} {P Q : forall B, (B <~> A) -> A}
         `{HP : RespectsEquivalenceR A (fun B (e : B <~> A) => P B e = Q B e)}
  : RespectsEquivalenceR A (fun (B : Type) (e : B <~> A) => e^-1 (P B e) = e^-1 (Q B e)).
A: Type
P, Q: forall B : Type, B <~> A -> A
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   e^-1 (P B e) = e^-1 (Q B e))
  Proof.
A: Type
P, Q: forall B : Type, B <~> A -> A
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) =>
   e^-1 (P B e) = e^-1 (Q B e))
    simple refine (fun B e => _; fun _ => _).
A: Type
P, Q: forall B : Type, B <~> A -> A
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
B: Type
e: B <~> A
(fun (B : Type) (e : B <~> A) =>
 e^-1 (P B e) = e^-1 (Q B e)) A 1 <~>
(fun (B : Type) (e : B <~> A) =>
 e^-1 (P B e) = e^-1 (Q B e)) B e
A: Type
P, Q: forall B : Type, B <~> A -> A
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
y: Funext
1 = (fun (B : Type) (e : B <~> A) => ?Goal) A 1
    {
A: Type
P, Q: forall B : Type, B <~> A -> A
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
B: Type
e: B <~> A
(fun (B : Type) (e : B <~> A) =>
 e^-1 (P B e) = e^-1 (Q B e)) A 1 <~>
(fun (B : Type) (e : B <~> A) =>
 e^-1 (P B e) = e^-1 (Q B e)) B e refine (equiv_ap' _ _ _ oE _); simpl.
A: Type
P, Q: forall B : Type, B <~> A -> A
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
B: Type
e: B <~> A
P A 1 = Q A 1 <~> P B e = Q B e
      refine (respects_equivalenceR.1 B e). }
A: Type
P, Q: forall B : Type, B <~> A -> A
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
y: Funext
1 =
(fun (B : Type) (e : B <~> A) =>
 equiv_ap' e^-1 (P B e) (Q B e)
 oE (respects_equivalenceR.1 B e
     :
     1^-1 (P A 1) = 1^-1 (Q A 1) <~> P B e = Q B e)) A
  1
    {
A: Type
P, Q: forall B : Type, B <~> A -> A
HP: RespectsEquivalenceR A
  (fun (B : Type) (e : B <~> A) => P B e = Q B e)
y: Funext
1 =
(fun (B : Type) (e : B <~> A) =>
 equiv_ap' e^-1 (P B e) (Q B e)
 oE (respects_equivalenceR.1 B e
     :
     1^-1 (P A 1) = 1^-1 (Q A 1) <~> P B e = Q B e)) A
  1 t. }
  Defined.
End ap.

(** We now write the tactic that partially solves the respectfulness side-condition.  We include cases for generic typeclass resolution, keys (heads) with zero, one, two, and three arguments, and a few cases that cannot be easily keyed (where the head is one of the arguments, or [forall]), or the head is [paths], for which we have only ad-hoc solutions at the moment. *)
Ltac step_respects_equiv :=
  idtac;
  match goal with
    | _ => progress intros
    | _ => assumption
    | _ => progress unfold respects_equivalenceL
    | _ => progress cbn
    | _ => exact _ (* case for fully solving the side-condition, when possible *)
    | [ |- RespectsEquivalenceL _ (fun _ _ => ?T) ] => rapply (get_lem T)
    | [ |- RespectsEquivalenceL _ (fun _ _ => ?T _) ] => rapply (get_lem T)
    | [ |- RespectsEquivalenceL _ (fun _ _ => ?T _ _) ] => rapply (get_lem T)
    | [ |- RespectsEquivalenceL _ (fun _ _ => ?T _ _ _) ] => rapply (get_lem T)
    | [ |- RespectsEquivalenceL _ (fun B e => equiv_fun e _ = equiv_fun e _) ] => refine equiv_ap_respects_equivalenceL
    | [ |- RespectsEquivalenceL _ (fun B e => equiv_inv e _ = equiv_inv e _) ] => refine equiv_ap_inv_respects_equivalenceL
    | [ |- RespectsEquivalenceL _ (fun B _ => B) ] => refine idmap_respects_equivalenceL
    | [ |- RespectsEquivalenceL _ (fun _ _ => forall _, _) ] => refine forall_respects_equivalenceL
  end.

Ltac equiv_induction p :=
  generalize dependent p;
  let p' := fresh in
  intro p';
    let y := match type of p' with ?x <~> ?y => constr:(y) end in
    move p' at top;
      generalize dependent y;
      let P := match goal with |- forall y p, @?P y p => constr:(P) end in
      (* We use [(fun x => x) _] to block automatic typeclass resolution in the hole for the equivalence respectful proof. *)
      refine ((fun g H B e => (@respects_equivalenceL _ P H).1 B e g) _ (_ : (fun x => x) _));
        [ intros | repeat step_respects_equiv ].

Goal forall `{Funext} A B (e : A <~> B), A -> { y : B & forall Q, Contr Q -> ((e^-1 y = e^-1 y) <~> (y = y)) * Q }.
Funext ->
forall (A B : Type) (e : A <~> B),
A ->
{y : B &
forall Q : Type,
Contr Q -> (e^-1 y = e^-1 y <~> y = y) * Q}
  intros ? ? ? ? a.
H: Funext
A, B: Type
e: A <~> B
a: A
{y : B &
forall Q : Type,
Contr Q -> (e^-1 y = e^-1 y <~> y = y) * Q}
  equiv_induction e.
A: Type
H: Funext
a: A
{y : A &
forall Q : Type,
Contr Q -> (1^-1 y = 1^-1 y <~> y = y) * Q}
A: Type
H: Funext
a, a0: A
a1: Type
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   Contr (?Goal1.1 B e a1))
A: Type
H: Funext
a, a0: A
a1: Type
a2: Contr (?Goal1.1 A 1 a1)
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   e^-1%function (?Goal0.1 B e a0) =
   e^-1%function (?Goal0.1 B e a0))
A: Type
H: Funext
a, a0: A
a1: Type
a2: Contr (?Goal1.1 A 1 a1)
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) =>
   ?Goal0.1 B e a0 = ?Goal0.1 B e a0)
A: Type
H: Funext
a, a0: A
a1: Type
a2: Contr (?Goal1.1 A 1 a1)
RespectsEquivalenceL A
  (fun (B : Type) (e : A <~> B) => ?Goal1.1 B e a1)
  -
A: Type
H: Funext
a: A
{y : A &
forall Q : Type,
Contr Q -> (1^-1 y = 1^-1 y <~> y = y) * Q} simpl.
A: Type
H: Funext
a: A
{y : A &
forall Q : Type, Contr Q -> (y = y <~> y = y) * Q}
    exists a.
A: Type
H: Funext
a: A
forall Q : Type, Contr Q -> (a = a <~> a = a) * Q
    intros Q q.
A: Type
H: Funext
a: A
Q: Type
q: Contr Q
(a = a <~> a = a) * Q
    exact (1, center _).
Abort.