(* -*- mode: coq; mode: visual-line -*-  *)
(** * Localization *)

Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Extensions.
Require Import ReflectiveSubuniverse Accessible.

Local Open Scope nat_scope.
Local Open Scope path_scope.

(** Suppose given a family of maps [f : forall (i:I), S i -> T i].  A type [X] is said to be [f]-local if for all [i:I], the map [(T i -> X) -> (S i -> X)] given by precomposition with [f i] is an equivalence.  Our goal is to show that the [f]-local types form a reflective subuniverse, with a reflector constructed by localization.  That is, morally we want to say

<<
Inductive Localize f (X : Type) : Type :=
| loc : X -> Localize X
| islocal_localize : forall i, IsEquiv (fun (g : T i -> X) => g o f i).
>>

This is not a valid HIT by the usual rules, but if we expand out the definition of [IsEquiv] and apply [path_sigma] and [path_forall], then it becomes one.  We get a simpler definition (no 2-path constructors) if we do this with [BiInv] rather than [IsEquiv]:

<<
Inductive Localize f (X : Type) : Type :=
| loc : X -> Localize X
| lsect : forall i (g : S i -> X), T i -> X
| lissect : forall i (g : S i -> X) (s : S i), lsect i g (f i s) = g s
| lretr : forall i (g : S i -> X), T i -> X
| lisretr : forall i (h : T i -> X) (t : T i), lretr i (h o f i) t = h t.
>>

This definition works, and from it one can prove that the [f]-local types form a reflective subuniverse.  However, the proof inextricably involves [Funext].  We can avoid [Funext] in the same way that we did in the definition of a [ReflectiveSubuniverse], by using pointwise path-split precomposition equivalences.  Observe that the assertion [ExtendableAlong n f C] consists entirely of points, paths, and higher paths in [C].  Therefore, for any [n] we might choose, we can define [Localize f X] as a HIT to universally force [ExtendableAlong n (f i) (fun _ => Localize f X)] to hold for all [i].  For instance, when [n] is 2 (the smallest value which will ensure that [Localize f X] is actually [f]-local), we get

<<
Inductive Localize f (X : Type) : Type :=
| loc : X -> Localize X
| lrec : forall i (g : S i -> X), T i -> X
| lrec_beta : forall i (g : S i -> X) (s : T i), lrec i g (f i s) = g s
| lindpaths : forall i (h k : T i -> X) (p : h o f i == k o f i) (t : T i), h t = k t
| lindpaths_beta : forall i (h k : T i -> X) (p : h o f i == k o f i) (s : S i),
                     lindpaths i h k p (f i s) = p s.
>>

However, just as for [ReflectiveSubuniverse], in order to completely avoid [Funext] we need the [oo]-version of path-splitness.  Written out as above, this would involve infinitely many constructors (but it would not otherwise be problematic, so for instance it can be constructed semantically in model categories).  We can't actually write out infinitely many constructors in Coq, of course, but since we have a finite definition of [ooExtendableAlong], we can just assert directly that [ooExtendableAlong (f i) (fun _ => Localize f X)] holds for all [i].

Then, however, we have to express the hypotheses of the induction principle.  We know what these should be for each path-constructor and higher path-constructor, so all we need is a way to package up those infinitely many hypotheses into a single one, analogously to [ooExtendableAlong].  Thus, we begin this file by defining a "dependent" version of [ooExtendableAlong], and of course we start this with a version for finite [n].  *)

(** ** Dependent extendability *)

Fixpoint ExtendableAlong_Over@{a b c d m | a <= m, b <= m, c <= m, d <= m}
         (n : nat) {A : Type@{a}} {B : Type@{b}} (f : A -> B)
         (C : B -> Type@{c})
         (D : forall b, C b -> Type@{d})
         (ext : ExtendableAlong@{a b c m} n f C)
: Type@{m}
  := match n return ExtendableAlong@{a b c m} n f C -> Type@{m} with
       | 0 => fun _ => Unit
       | S n => fun ext' =>
                (forall (g : forall a, C (f a)) (g' : forall a, D (f a) (g a)),
                  sig@{m m}     (** Control universe parameters *)
                  (fun (rec : forall b, D b ((fst ext' g).1 b)) =>
                         forall a, (fst ext' g).2 a # rec (f a) = g' a )) *
                forall (h k : forall b, C b)
                       (h' : forall b, D b (h b)) (k' : forall b, D b (k b)),
                  ExtendableAlong_Over n f (fun b => h b = k b)
                    (fun b c => c # h' b = k' b) (snd ext' h k)
     end ext.

(** Like [ExtendableAlong], these can be postcomposed with known equivalences. *)
Definition extendable_over_postcompose' (n : nat)
           {A B : Type} (C : B -> Type) (f : A -> B)
           (ext : ExtendableAlong n f C)
           (D E : forall b, C b -> Type)
           (g : forall b c, D b c <~> E b c)
: ExtendableAlong_Over n f C D ext
  -> ExtendableAlong_Over n f C E ext.
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ExtendableAlong_Over n f C D ext ->
ExtendableAlong_Over n f C E ext
Proof.
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ExtendableAlong_Over n f C D ext ->
ExtendableAlong_Over n f C E ext
  revert C ext D E g; simple_induction n n IHn; intros C ext D E g; simpl.
A, B: Type
f: A -> B
C: B -> Type
ext: ExtendableAlong 0 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
Unit -> Unit
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
(forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a) (rec (f a)) =
 g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b) (snd ext h k)) ->
(forall (g : forall a : A, C (f a))
 (g' : forall a : A, E (f a) (g a)),
 {rec : forall b : B, E b ((fst ext g).1 b) &
 forall a : A,
 transport (E (f a)) ((fst ext g).2 a) (rec (f a)) =
 g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, E b (h b))
 (k' : forall b : B, E b (k b)),
 ExtendableAlong_Over n f (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (E b) c (h' b) = k' b) (snd ext h k))
  1:by apply idmap.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
(forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a) (rec (f a)) =
 g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b) (snd ext h k)) ->
(forall (g : forall a : A, C (f a))
 (g' : forall a : A, E (f a) (g a)),
 {rec : forall b : B, E b ((fst ext g).1 b) &
 forall a : A,
 transport (E (f a)) ((fst ext g).2 a) (rec (f a)) =
 g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, E b (h b))
 (k' : forall b : B, E b (k b)),
 ExtendableAlong_Over n f (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (E b) c (h' b) = k' b) (snd ext h k))
  intros ext'.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
(forall (g : forall a : A, C (f a))
 (g' : forall a : A, E (f a) (g a)),
 {rec : forall b : B, E b ((fst ext g).1 b) &
 forall a : A,
 transport (E (f a)) ((fst ext g).2 a) (rec (f a)) =
 g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, E b (h b))
 (k' : forall b : B, E b (k b)),
 ExtendableAlong_Over n f (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (E b) c (h' b) = k' b) (snd ext h k))
  split.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
forall (g : forall a : A, C (f a))
(g' : forall a : A, E (f a) (g a)),
{rec : forall b : B, E b ((fst ext g).1 b) &
forall a : A,
transport (E (f a)) ((fst ext g).2 a) (rec (f a)) =
g' a}
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type)
(ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext ->
ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
forall (h k : forall b : B, C b)
(h' : forall b : B, E b (h b))
(k' : forall b : B, E b (k b)),
ExtendableAlong_Over n f 
  (fun b : B => h b = k b)
  (fun (b : B) (c : h b = k b) =>
   transport (E b) c (h' b) = k' b) 
  (snd ext h k)
  -
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
forall (g : forall a : A, C (f a))
(g' : forall a : A, E (f a) (g a)),
{rec : forall b : B, E b ((fst ext g).1 b) &
forall a : A,
transport (E (f a)) ((fst ext g).2 a) (rec (f a)) =
g' a} intros h k.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
h: forall a : A, C (f a)
k: forall a : A, E (f a) (h a)
{rec : forall b : B, E b ((fst ext h).1 b) &
forall a : A,
transport (E (f a)) ((fst ext h).2 a) (rec (f a)) =
k a}
    exists (fun b => g b ((fst ext h).1 b)
                     ((fst ext' h (fun a => (g _ _)^-1 (k a))).1 b)).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
h: forall a : A, C (f a)
k: forall a : A, E (f a) (h a)
forall a : A,
transport (E (f a)) ((fst ext h).2 a)
  (g (f a) ((fst ext h).1 (f a))
     ((fst ext' h
         (fun a0 : A => (g (f a0) (h a0))^-1 (k a0))).1
        (f a))) = k a
    intros a.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
h: forall a : A, C (f a)
k: forall a : A, E (f a) (h a)
a: A
transport (E (f a)) ((fst ext h).2 a)
  (g (f a) ((fst ext h).1 (f a))
     ((fst ext' h
         (fun a : A => (g (f a) (h a))^-1 (k a))).1
        (f a))) = k a
    refine ((ap_transport ((fst ext h).2 a) (g (f a)) _)^ @ _).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
h: forall a : A, C (f a)
k: forall a : A, E (f a) (h a)
a: A
g (f a) (h a)
  (transport (D (f a)) ((fst ext h).2 a)
     ((fst ext' h
         (fun a : A => (g (f a) (h a))^-1 (k a))).1
        (f a))) = k a
    apply moveR_equiv_M.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
h: forall a : A, C (f a)
k: forall a : A, E (f a) (h a)
a: A
transport (D (f a)) ((fst ext h).2 a)
  ((fst ext' h (fun a : A => (g (f a) (h a))^-1 (k a))).1
     (f a)) = (g (f a) (h a))^-1 (k a)
    exact ((fst ext' h (fun a => (g _ _)^-1 (k a))).2 a).
  -
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
forall (h k : forall b : B, C b)
(h' : forall b : B, E b (h b))
(k' : forall b : B, E b (k b)),
ExtendableAlong_Over n f (fun b : B => h b = k b)
  (fun (b : B) (c : h b = k b) =>
   transport (E b) c (h' b) = k' b) (snd ext h k) intros p q p' q'.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
p, q: forall b : B, C b
p': forall b : B, E b (p b)
q': forall b : B, E b (q b)
ExtendableAlong_Over n f (fun b : B => p b = q b)
  (fun (b : B) (c : p b = q b) =>
   transport (E b) c (p' b) = q' b) (snd ext p q)
    refine (IHn (fun b => p b = q b) _
                (fun b => fun c => transport (D b) c ((g b (p b))^-1 (p' b))
                                   = ((g b (q b))^-1 (q' b)))
                _ _
                (snd ext' p q (fun b => (g b (p b))^-1 (p' b))
                              (fun b => (g b (q b))^-1 (q' b)))).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
p, q: forall b : B, C b
p': forall b : B, E b (p b)
q': forall b : B, E b (q b)
forall (b : B) (c : p b = q b),
transport (D b) c ((g b (p b))^-1 (p' b)) =
(g b (q b))^-1 (q' b) <~>
transport (E b) c (p' b) = q' b
    intros b c.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
p, q: forall b : B, C b
p': forall b : B, E b (p b)
q': forall b : B, E b (q b)
b: B
c: p b = q b
transport (D b) c ((g b (p b))^-1 (p' b)) =
(g b (q b))^-1 (q' b) <~>
transport (E b) c (p' b) = q' b
    refine (_ oE equiv_moveR_equiv_M _ _).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
p, q: forall b : B, C b
p': forall b : B, E b (p b)
q': forall b : B, E b (q b)
b: B
c: p b = q b
g b (q b) (transport (D b) c ((g b (p b))^-1 (p' b))) =
q' b <~> transport (E b) c (p' b) = q' b
    apply equiv_concat_l.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
p, q: forall b : B, C b
p': forall b : B, E b (p b)
q': forall b : B, E b (q b)
b: B
c: p b = q b
transport (E b) c (p' b) =
g b (q b) (transport (D b) c ((g b (p b))^-1 (p' b)))
    refine (_ @ (ap_transport c (g b) _)^).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D E : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c <~> E b c) ->
ExtendableAlong_Over n f C D ext -> ExtendableAlong_Over n f C E ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D, E: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c <~> E b c
ext': (forall (g : forall a : A, C (f a))
 (g' : forall a : A, D (f a) (g a)),
 {rec : forall b : B, D b ((fst ext g).1 b) &
 forall a : A,
 transport (D (f a)) ((fst ext g).2 a)
   (rec (f a)) = g' a}) *
(forall (h k : forall b : B, C b)
 (h' : forall b : B, D b (h b))
 (k' : forall b : B, D b (k b)),
 ExtendableAlong_Over n f
   (fun b : B => h b = k b)
   (fun (b : B) (c : h b = k b) =>
    transport (D b) c (h' b) = k' b)
   (snd ext h k))
p, q: forall b : B, C b
p': forall b : B, E b (p b)
q': forall b : B, E b (q b)
b: B
c: p b = q b
transport (E b) c (p' b) =
transport (E b) c (g b (p b) ((g b (p b))^-1 (p' b)))
    apply ap, symmetry, eisretr.
Defined.

Definition extendable_over_postcompose (n : nat)
           {A B : Type} (C : B -> Type) (f : A -> B)
           (ext : ExtendableAlong n f C)
           (D E : forall b, C b -> Type)
           (g : forall b c, D b c -> E b c)
           `{forall b c, IsEquiv (g b c)}
: ExtendableAlong_Over n f C D ext
  -> ExtendableAlong_Over n f C E ext
:= extendable_over_postcompose' n C f ext D E
     (fun b c => Build_Equiv _ _ (g b c) _).

(** And if the dependency is trivial, we obtain them from an ordinary [ExtendableAlong]. *)
Definition extendable_over_const
           (n : nat) {A B : Type} (C : B -> Type) (f : A -> B)
           (ext : ExtendableAlong n f C) (D : B -> Type)
: ExtendableAlong n f D
  -> ExtendableAlong_Over n f C (fun b _ => D b) ext.
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n f C
D: B -> Type
ExtendableAlong n f D ->
ExtendableAlong_Over n f C
  (fun (b : B) (_ : C b) => D b) ext
Proof.
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n f C
D: B -> Type
ExtendableAlong n f D ->
ExtendableAlong_Over n f C
  (fun (b : B) (_ : C b) => D b) ext
  revert C ext D.
n: nat
A, B: Type
f: A -> B
forall (C : B -> Type) (ext : ExtendableAlong n f C)
(D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C
  (fun (b : B) (_ : C b) => D b) ext
  simple_induction n n IHn; intros C ext D ext'.
A, B: Type
f: A -> B
C: B -> Type
ext: ExtendableAlong 0 f C
D: B -> Type
ext': ExtendableAlong 0 f D
ExtendableAlong_Over 0 f C
  (fun (b : B) (_ : C b) => D b) ext
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type)
(ext : ExtendableAlong n f C) 
(D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C
  (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
ExtendableAlong_Over n.+1 f C
  (fun (b : B) (_ : C b) => D b) ext
  1:exact tt.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C) (D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
ExtendableAlong_Over n.+1 f C
  (fun (b : B) (_ : C b) => D b) ext
  split.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C) (D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
forall (g : forall a : A, C (f a))
(g' : forall a : A, D (f a)),
{rec : forall b : B, D b &
forall a : A,
transport (fun _ : C (f a) => D (f a))
  ((fst ext g).2 a) (rec (f a)) = g' a}
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type)
(ext : ExtendableAlong n f C) 
(D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C
  (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
forall (h k : forall b : B, C b)
(h' k' : forall b : B, D b),
ExtendableAlong_Over n f 
  (fun b : B => h b = k b)
  (fun (b : B) (c : h b = k b) =>
   transport (fun _ : C b => D b) c (h' b) = k' b)
  (snd ext h k)
  -
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C) (D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
forall (g : forall a : A, C (f a))
(g' : forall a : A, D (f a)),
{rec : forall b : B, D b &
forall a : A,
transport (fun _ : C (f a) => D (f a))
  ((fst ext g).2 a) (rec (f a)) = g' a} intros g g'.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C) (D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
g: forall a : A, C (f a)
g': forall a : A, D (f a)
{rec : forall b : B, D b &
forall a : A,
transport (fun _ : C (f a) => D (f a))
  ((fst ext g).2 a) (rec (f a)) = g' a}
    exists ((fst ext' g').1).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C) (D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
g: forall a : A, C (f a)
g': forall a : A, D (f a)
forall a : A,
transport (fun _ : C (f a) => D (f a))
  ((fst ext g).2 a) ((fst ext' g').1 (f a)) = g' a
    exact (fun a => transport_const ((fst ext g).2 a) _
                                    @ (fst ext' g').2 a).
  -
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C) (D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
forall (h k : forall b : B, C b)
(h' k' : forall b : B, D b),
ExtendableAlong_Over n f (fun b : B => h b = k b)
  (fun (b : B) (c : h b = k b) =>
   transport (fun _ : C b => D b) c (h' b) = k' b)
  (snd ext h k) intros h k h' k'.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C) (D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
h, k: forall b : B, C b
h', k': forall b : B, D b
ExtendableAlong_Over n f (fun b : B => h b = k b)
  (fun (b : B) (c : h b = k b) =>
   transport (fun _ : C b => D b) c (h' b) = k' b)
  (snd ext h k)
    refine (extendable_over_postcompose' _ _ _ _ _ _ _
              (IHn (fun b => h b = k b) (snd ext h k)
                   (fun b => h' b = k' b) (snd ext' h' k'))).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ExtendableAlong n f C) (D : B -> Type),
ExtendableAlong n f D ->
ExtendableAlong_Over n f C (fun (b : B) (_ : C b) => D b) ext
C: B -> Type
ext: ExtendableAlong n.+1 f C
D: B -> Type
ext': ExtendableAlong n.+1 f D
h, k: forall b : B, C b
h', k': forall b : B, D b
forall (b : B) (c : h b = k b),
h' b = k' b <~>
transport (fun _ : C b => D b) c (h' b) = k' b
    exact (fun b c => equiv_concat_l (transport_const c (h' b)) (k' b)).
Defined.

(** This lemma will be used in stating the computation rule for localization. *)
Fixpoint apD_extendable_eq (n : nat) {A B : Type} (C : B -> Type) (f : A -> B)
         (ext : ExtendableAlong n f C) (D : forall b, C b -> Type)
         (g : forall b c, D b c)
         (ext' : ExtendableAlong_Over n f C D ext)
         {struct n}
: Type.
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over n f C D ext
Type
Proof.
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over n f C D ext
Type
  destruct n.
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong 0 f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over 0 f C D ext
Type
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n.+1 f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over n.+1 f C D ext
Type
  -
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong 0 f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over 0 f C D ext
Type exact Unit.
  -
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n.+1 f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over n.+1 f C D ext
Type apply prod.
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n.+1 f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over n.+1 f C D ext
Type
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n.+1 f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over n.+1 f C D ext
Type
    +
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n.+1 f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over n.+1 f C D ext
Type exact (forall (h : forall a, C (f a)) (b : B),
               g b ((fst ext h).1 b) = (fst ext' h (fun a => g (f a) (h a))).1 b).
    +
apD_extendable_eq: forall (n : nat) (A B : Type)
(C : B -> Type) (f : A -> B)
(ext : ExtendableAlong n f C)
(D : forall b : B, C b -> Type),
(forall (b : B) (c : C b), D b c) ->
ExtendableAlong_Over n f C D ext ->
Type
n: nat
A, B: Type
C: B -> Type
f: A -> B
ext: ExtendableAlong n.+1 f C
D: forall b : B, C b -> Type
g: forall (b : B) (c : C b), D b c
ext': ExtendableAlong_Over n.+1 f C D ext
Type exact (forall h k, apD_extendable_eq
                           n A B (fun b => h b = k b) f (snd ext h k)
                           (fun b c => c # g b (h b) = g b (k b))
                           (fun b c => apD (g b) c)
                           (snd ext' h k _ _)).
Defined.

(** Here's the [oo]-version. *)
Definition ooExtendableAlong_Over@{a b c d m | a <= m, b <= m, c <= m, d <= m}
         {A : Type@{a}} {B : Type@{b}} (f : A -> B) (C : B -> Type@{c})
         (D : forall b, C b -> Type@{d}) (ext : ooExtendableAlong f C)
  := forall n, ExtendableAlong_Over@{a b c d m} n f C D (ext n).

(** The [oo]-version for trivial dependency. *)
Definition ooextendable_over_const
           {A B : Type} (C : B -> Type) (f : A -> B)
           (ext : ooExtendableAlong f C) (D : B -> Type)
: ooExtendableAlong f D
  -> ooExtendableAlong_Over f C (fun b _ => D b) ext
:= fun ext' n => extendable_over_const n C f (ext n) D (ext' n).

(** A crucial fact: the [oo]-version is inherited by types of homotopies. *)
Definition ooextendable_over_homotopy
           {A B : Type} (C : B -> Type) (f : A -> B)
           (ext : ooExtendableAlong f C)
           (D : forall b, C b -> Type)
           (r s : forall b c, D b c)
: ooExtendableAlong_Over f C D ext
  -> ooExtendableAlong_Over f C (fun b c => r b c = s b c) ext.
A, B: Type
C: B -> Type
f: A -> B
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ooExtendableAlong_Over f C D ext ->
ooExtendableAlong_Over f C
  (fun (b : B) (c : C b) => r b c = s b c) ext
Proof.
A, B: Type
C: B -> Type
f: A -> B
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ooExtendableAlong_Over f C D ext ->
ooExtendableAlong_Over f C
  (fun (b : B) (c : C b) => r b c = s b c) ext
  intros ext' n.
A, B: Type
C: B -> Type
f: A -> B
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
n: nat
ExtendableAlong_Over n f C
  (fun (b : B) (c : C b) => r b c = s b c) (ext n)
  revert C ext D r s ext'.
A, B: Type
f: A -> B
n: nat
forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type)
(r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C
  (fun (b : B) (c : C b) => r b c = s b c) (ext n)
  simple_induction n n IHn; intros C ext D r s ext'.
A, B: Type
f: A -> B
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
ExtendableAlong_Over 0 f C
  (fun (b : B) (c : C b) => r b c = s b c) (ext 0)
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type)
(ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type)
(r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C
  (fun (b : B) (c : C b) => r b c = s b c)
  (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
ExtendableAlong_Over n.+1 f C
  (fun (b : B) (c : C b) => r b c = s b c) 
  (ext n.+1)
  1:exact tt.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
ExtendableAlong_Over n.+1 f C
  (fun (b : B) (c : C b) => r b c = s b c) (ext n.+1)
  split.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
forall (g : forall a : A, C (f a))
(g' : forall a : A, r (f a) (g a) = s (f a) (g a)),
{rec
: forall b : B,
  r b ((fst (ext n.+1) g).1 b) =
  s b ((fst (ext n.+1) g).1 b) &
forall a : A,
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a) (rec (f a)) = g' a}
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type)
(ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type)
(r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C
  (fun (b : B) (c : C b) => r b c = s b c)
  (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
forall (h k : forall b : B, C b)
(h' : forall b : B, r b (h b) = s b (h b))
(k' : forall b : B, r b (k b) = s b (k b)),
ExtendableAlong_Over n f 
  (fun b : B => h b = k b)
  (fun (b : B) (c : h b = k b) =>
   transport (fun c0 : C b => r b c0 = s b c0) c
     (h' b) = k' b) (snd (ext n.+1) h k)
  -
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
forall (g : forall a : A, C (f a))
(g' : forall a : A, r (f a) (g a) = s (f a) (g a)),
{rec
: forall b : B,
  r b ((fst (ext n.+1) g).1 b) =
  s b ((fst (ext n.+1) g).1 b) &
forall a : A,
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a) (rec (f a)) = g' a} intros g g'.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
{rec
: forall b : B,
  r b ((fst (ext n.+1) g).1 b) =
  s b ((fst (ext n.+1) g).1 b) &
forall a : A,
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a) (rec (f a)) = g' a}
    simple refine (_;_); simpl.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
forall b : B,
r b ((fst (ext n.+1) g).1 b) =
s b ((fst (ext n.+1) g).1 b)
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type)
(ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type)
(r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C
  (fun (b : B) (c : C b) => r b c = s b c)
  (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
forall a : A,
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a) 
  (?Goal0 (f a)) = g' a
    +
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
forall b : B,
r b ((fst (ext n.+1) g).1 b) =
s b ((fst (ext n.+1) g).1 b) intros b.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
b: B
r b ((fst (ext n.+1) g).1 b) =
s b ((fst (ext n.+1) g).1 b)
      refine (_ @ (fst (snd (ext' 2) _ _
                            (fun b' => r b' ((fst (ext n.+1) g).1 b'))
                            (fun b' => s b' ((fst (ext n.+1) g).1 b')))
                       (fun _ => 1) _).1 b).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
b: B
r b ((fst (ext n.+1) g).1 b) =
transport (D b)
  ((fst
      (snd (ext 2) (fst (ext n.+1) g).1
         (fst (ext n.+1) g).1) (fun a : A => 1)).1 b)
  (r b ((fst (ext n.+1) g).1 b))
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type)
(ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type)
(r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C
  (fun (b : B) (c : C b) => r b c = s b c)
  (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
b: B
forall a : A,
transport (D (f a)) 1
  (r (f a) ((fst (ext n.+1) g).1 (f a))) =
s (f a) ((fst (ext n.+1) g).1 (f a))
      *
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
b: B
r b ((fst (ext n.+1) g).1 b) =
transport (D b)
  ((fst
      (snd (ext 2) (fst (ext n.+1) g).1
         (fst (ext n.+1) g).1) (fun a : A => 1)).1 b)
  (r b ((fst (ext n.+1) g).1 b)) refine (transport2 (D b) (p := 1) _ _).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
b: B
1 =
(fst
   (snd (ext 2) (fst (ext n.+1) g).1
      (fst (ext n.+1) g).1) (fun a : A => 1)).1 b
        refine ((fst (snd (snd (ext 3) _ _) (fun b' => 1)
                          ((fst (snd (ext 2) _ _) (fun a : A => 1)).1)
                ) _).1 b); intros a.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
b: B
a: A
1 =
(fst
   (snd (ext 2) (fst (ext n.+1) g).1
      (fst (ext n.+1) g).1) (fun a : A => 1)).1 (f a)
        symmetry; refine ((fst (snd (ext 2) _ _) (fun a' => 1)).2 a).
      *
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
b: B
forall a : A,
transport (D (f a)) 1
  (r (f a) ((fst (ext n.+1) g).1 (f a))) =
s (f a) ((fst (ext n.+1) g).1 (f a)) intros a; simpl.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
b: B
a: A
r (f a) ((fst (ext n.+1) g).1 (f a)) =
s (f a) ((fst (ext n.+1) g).1 (f a))
        refine (_ @
          ap (transport (D (f a)) ((fst (ext n.+1) g).2 a)^) (g' a)
          @ _);
        [ symmetry; by apply apD
        | by apply apD ].
    +
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
forall a : A,
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  ((fun b : B =>
    transport2 (D b)
      ((fst
          (snd
             (snd (ext 3) (fst (ext n.+1) g).1
                (fst (ext n.+1) g).1)
             (fun b' : B => 1)
             (fst
                (snd (ext 2) (fst (ext n.+1) g).1
                   (fst (ext n.+1) g).1)
                (fun a0 : A => 1)).1)
          (fun a0 : A =>
           ((fst
               (snd (ext 2) (fst (ext n.+1) g).1
                  (fst (ext n.+1) g).1)
               (fun a' : A => 1)).2 a0)^)).1 b)
      (r b ((fst (ext n.+1) g).1 b)) @
    (fst
       (snd (ext' 2) (fst (ext n.+1) g).1
          (fst (ext n.+1) g).1
          (fun b' : B =>
           r b' ((fst (ext n.+1) g).1 b'))
          (fun b' : B =>
           s b' ((fst (ext n.+1) g).1 b')))
       (fun a0 : A => 1)
       (fun a0 : A =>
        ((apD (r (f a0)) ((fst (ext n.+1) g).2 a0)^)^ @
         ap
           (transport (D (f a0))
              ((fst (ext n.+1) g).2 a0)^) (g' a0)) @
        apD (s (f a0)) ((fst (ext n.+1) g).2 a0)^
        :
        transport (D (f a0)) 1
          (r (f a0) ((fst (ext n.+1) g).1 (f a0))) =
        s (f a0) ((fst (ext n.+1) g).1 (f a0)))).1 b)
     (f a)) = g' a intros a; simpl.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (transport2 (D (f a))
     ((fst
         (snd
            (snd (ext 3) (fst (ext n.+1) g).1
               (fst (ext n.+1) g).1) (fun b' : B => 1)
            (fst
               (snd (ext 2) (fst (ext n.+1) g).1
                  (fst (ext n.+1) g).1)
               (fun a : A => 1)).1)
         (fun a : A =>
          ((fst
              (snd (ext 2) (fst (ext n.+1) g).1
                 (fst (ext n.+1) g).1)
              (fun a' : A => 1)).2 a)^)).1 (f a))
     (r (f a) ((fst (ext n.+1) g).1 (f a))) @
   (fst
      (snd (ext' 2) (fst (ext n.+1) g).1
         (fst (ext n.+1) g).1
         (fun b' : B => r b' ((fst (ext n.+1) g).1 b'))
         (fun b' : B => s b' ((fst (ext n.+1) g).1 b')))
      (fun a : A => 1)
      (fun a : A =>
       ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
        ap
          (transport (D (f a))
             ((fst (ext n.+1) g).2 a)^) (g' a)) @
       apD (s (f a)) ((fst (ext n.+1) g).2 a)^)).1
     (f a)) = g' a
      set (h := (fst (ext n.+1) g).1).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (transport2 (D (f a))
     ((fst
         (snd (snd (ext 3) h h) (fun b' : B => 1)
            (fst (snd (ext 2) h h) (fun a : A => 1)).1)
         (fun a : A =>
          ((fst (snd (ext 2) h h) (fun a' : A => 1)).2
             a)^)).1 (f a)) (r (f a) (h (f a))) @
   (fst
      (snd (ext' 2) h h (fun b' : B => r b' (h b'))
         (fun b' : B => s b' (h b'))) (fun a : A => 1)
      (fun a : A =>
       ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
        ap
          (transport (D (f a))
             ((fst (ext n.+1) g).2 a)^) (g' a)) @
       apD (s (f a)) ((fst (ext n.+1) g).2 a)^)).1
     (f a)) = g' a
      match goal with
          |- context[   (fst (snd (ext' 2) _ _ ?k1 ?k2) (fun _ => 1) ?l).1 ]
          => pose (p := (fst (snd (ext' 2) _ _  k1  k2) (fun _ => 1) l).2 a);
            simpl in p
      end.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
p:= (fst
   (snd (ext' 2) h h (fun b' : B => r b' (h b'))
      (fun b' : B => s b' (h b'))) 
   (fun a : A => 1)
   (fun a : A =>
    ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
     ap
       (transport (D (f a))
          ((fst (ext n.+1) g).2 a)^) 
       (g' a)) @
    apD (s (f a)) ((fst (ext n.+1) g).2 a)^)).2 a: transport
  (fun c : h (f a) = h (f a) =>
   transport (D (f a)) c (r (f a) (h (f a))) =
   s (f a) (h (f a)))
  ((fst (snd (ext 2) h h) (fun a : A => 1)).2 a)
  ((fst
      (snd (ext' 2) h h
         (fun b' : B => r b' (h b'))
         (fun b' : B => s b' (h b')))
      (fun a : A => 1)
      (fun a : A =>
       ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
        ap
          (transport (D (f a))
             ((fst (ext n.+1) g).2 a)^) 
          (g' a)) @
       apD (s (f a)) ((fst (ext n.+1) g).2 a)^)).1
     (f a)) =
((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
 ap
   (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
   (g' a)) @
apD (s (f a)) ((fst (ext n.+1) g).2 a)^
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (transport2 (D (f a))
     ((fst
         (snd (snd (ext 3) h h) (fun b' : B => 1)
            (fst (snd (ext 2) h h) (fun a : A => 1)).1)
         (fun a : A =>
          ((fst (snd (ext 2) h h) (fun a' : A => 1)).2
             a)^)).1 (f a)) (r (f a) (h (f a))) @
   (fst
      (snd (ext' 2) h h (fun b' : B => r b' (h b'))
         (fun b' : B => s b' (h b'))) (fun a : A => 1)
      (fun a : A =>
       ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
        ap
          (transport (D (f a))
             ((fst (ext n.+1) g).2 a)^) (g' a)) @
       apD (s (f a)) ((fst (ext n.+1) g).2 a)^)).1
     (f a)) = g' a
      rewrite transport_paths_Fl in p.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
p: (ap
   (fun x : h (f a) = h (f a) =>
    transport (D (f a)) x (r (f a) (h (f a))))
   ((fst (snd (ext 2) h h) (fun a : A => 1)).2 a))^ @
(fst
   (snd (ext' 2) h h (fun b' : B => r b' (h b'))
      (fun b' : B => s b' (h b')))
   (fun a : A => 1)
   (fun a : A =>
    ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
     ap
       (transport (D (f a))
          ((fst (ext n.+1) g).2 a)^) 
       (g' a)) @
    apD (s (f a)) ((fst (ext n.+1) g).2 a)^)).1
  (f a) =
((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
 ap
   (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
   (g' a)) @
apD (s (f a)) ((fst (ext n.+1) g).2 a)^
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (transport2 (D (f a))
     ((fst
         (snd (snd (ext 3) h h) (fun b' : B => 1)
            (fst (snd (ext 2) h h) (fun a : A => 1)).1)
         (fun a : A =>
          ((fst (snd (ext 2) h h) (fun a' : A => 1)).2
             a)^)).1 (f a)) (r (f a) (h (f a))) @
   (fst
      (snd (ext' 2) h h (fun b' : B => r b' (h b'))
         (fun b' : B => s b' (h b'))) (fun a : A => 1)
      (fun a : A =>
       ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
        ap
          (transport (D (f a))
             ((fst (ext n.+1) g).2 a)^) (g' a)) @
       apD (s (f a)) ((fst (ext n.+1) g).2 a)^)).1
     (f a)) = g' a
      apply moveL_Mp in p.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
p: (fst
   (snd (ext' 2) h h (fun b' : B => r b' (h b'))
      (fun b' : B => s b' (h b')))
   (fun a : A => 1)
   (fun a : A =>
    ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
     ap
       (transport (D (f a))
          ((fst (ext n.+1) g).2 a)^) 
       (g' a)) @
    apD (s (f a)) ((fst (ext n.+1) g).2 a)^)).1
  (f a) =
ap
  (fun x : h (f a) = h (f a) =>
   transport (D (f a)) x (r (f a) (h (f a))))
  ((fst (snd (ext 2) h h) (fun a : A => 1)).2 a) @
(((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
  ap
    (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
    (g' a)) @
 apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (transport2 (D (f a))
     ((fst
         (snd (snd (ext 3) h h) (fun b' : B => 1)
            (fst (snd (ext 2) h h) (fun a : A => 1)).1)
         (fun a : A =>
          ((fst (snd (ext 2) h h) (fun a' : A => 1)).2
             a)^)).1 (f a)) (r (f a) (h (f a))) @
   (fst
      (snd (ext' 2) h h (fun b' : B => r b' (h b'))
         (fun b' : B => s b' (h b'))) (fun a : A => 1)
      (fun a : A =>
       ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
        ap
          (transport (D (f a))
             ((fst (ext n.+1) g).2 a)^) (g' a)) @
       apD (s (f a)) ((fst (ext n.+1) g).2 a)^)).1
     (f a)) = g' a
      refine (ap (transport _ _) (1 @@ p) @ _); clear p.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (transport2 (D (f a))
     ((fst
         (snd (snd (ext 3) h h) (fun b' : B => 1)
            (fst (snd (ext 2) h h) (fun a : A => 1)).1)
         (fun a : A =>
          ((fst (snd (ext 2) h h) (fun a' : A => 1)).2
             a)^)).1 (f a)) (r (f a) (h (f a))) @
   (ap
      (fun x : h (f a) = h (f a) =>
       transport (D (f a)) x (r (f a) (h (f a))))
      ((fst (snd (ext 2) h h) (fun a : A => 1)).2 a) @
    (((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
      ap
        (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
        (g' a)) @
     apD (s (f a)) ((fst (ext n.+1) g).2 a)^))) = 
g' a
      unfold transport2; rewrite concat_p_pp.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  ((ap
      (fun p' : h (f a) = h (f a) =>
       transport (D (f a)) p' (r (f a) (h (f a))))
      ((fst
          (snd (snd (ext 3) h h) (fun b' : B => 1)
             (fst (snd (ext 2) h h) (fun a : A => 1)).1)
          (fun a : A =>
           ((fst (snd (ext 2) h h) (fun a' : A => 1)).2
              a)^)).1 (f a)) @
    ap
      (fun x : h (f a) = h (f a) =>
       transport (D (f a)) x (r (f a) (h (f a))))
      ((fst (snd (ext 2) h h) (fun a : A => 1)).2 a)) @
   (((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
     ap
       (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
       (g' a)) @
    apD (s (f a)) ((fst (ext n.+1) g).2 a)^)) = g' a
      match goal with
          |- transport ?P ?p ((ap ?f ?q @ ap ?f ?r) @ ?s) = ?t
          => refine (ap (transport P p) ((ap_pp f q r)^ @@ (idpath s)) @ _)
      end.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (ap
     (fun p' : h (f a) = h (f a) =>
      transport (D (f a)) p' (r (f a) (h (f a))))
     ((fst
         (snd (snd (ext 3) h h) (fun b' : B => 1)
            (fst (snd (ext 2) h h) (fun a : A => 1)).1)
         (fun a : A =>
          ((fst (snd (ext 2) h h) (fun a' : A => 1)).2
             a)^)).1 (f a) @
      (fst (snd (ext 2) h h) (fun a : A => 1)).2 a) @
   (((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
     ap
       (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
       (g' a)) @
    apD (s (f a)) ((fst (ext n.+1) g).2 a)^)) = g' a
      pose (p := (fst (snd (snd (ext 3) h h) (fun b' : B => 1)
                           ((fst (snd (ext 2) h h) (fun a0 : A => 1)).1))
                      (fun a' : A => ((fst (snd (ext 2) h h)
                                           (fun a' : A => 1)).2 a')^)).2 a);
        simpl in p.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
p:= (fst
   (snd (snd (ext 3) h h) 
      (fun b' : B => 1)
      (fst (snd (ext 2) h h) (fun a0 : A => 1)).1)
   (fun a' : A =>
    ((fst (snd (ext 2) h h) (fun a'0 : A => 1)).2
       a')^)).2 a: (fst
   (snd (snd (ext 3) h h) 
      (fun b' : B => 1)
      (fst (snd (ext 2) h h) (fun a0 : A => 1)).1)
   (fun a' : A =>
    ((fst (snd (ext 2) h h) (fun a'0 : A => 1)).2
       a')^)).1 (f a) =
((fst (snd (ext 2) h h) (fun a' : A => 1)).2 a)^
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (ap
     (fun p' : h (f a) = h (f a) =>
      transport (D (f a)) p' (r (f a) (h (f a))))
     ((fst
         (snd (snd (ext 3) h h) (fun b' : B => 1)
            (fst (snd (ext 2) h h) (fun a : A => 1)).1)
         (fun a : A =>
          ((fst (snd (ext 2) h h) (fun a' : A => 1)).2
             a)^)).1 (f a) @
      (fst (snd (ext 2) h h) (fun a : A => 1)).2 a) @
   (((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
     ap
       (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
       (g' a)) @
    apD (s (f a)) ((fst (ext n.+1) g).2 a)^)) = g' a
      refine (ap (transport _ _) (ap (ap _) (p @@ 1) @@ 1) @ _); clear p.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (ap
     (fun p' : h (f a) = h (f a) =>
      transport (D (f a)) p' (r (f a) (h (f a))))
     (((fst (snd (ext 2) h h) (fun a' : A => 1)).2 a)^ @
      (fst (snd (ext 2) h h) (fun a : A => 1)).2 a) @
   (((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
     ap
       (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
       (g' a)) @
    apD (s (f a)) ((fst (ext n.+1) g).2 a)^)) = g' a
      rewrite concat_Vp; simpl; rewrite concat_1p.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
transport (fun c : C (f a) => r (f a) c = s (f a) c)
  ((fst (ext n.+1) g).2 a)
  (((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
    ap (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
      (g' a)) @
   apD (s (f a)) ((fst (ext n.+1) g).2 a)^) = g' a
      refine (transport_paths_FlFr_D _ _ @ _).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
((apD (r (f a)) ((fst (ext n.+1) g).2 a))^ @
 ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
   (((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^ @
     ap
       (transport (D (f a)) ((fst (ext n.+1) g).2 a)^)
       (g' a)) @
    apD (s (f a)) ((fst (ext n.+1) g).2 a)^)) @
apD (s (f a)) ((fst (ext n.+1) g).2 a) = g' a
      Open Scope long_path_scope.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
(apD (r (f a)) ((fst (ext n.+1) g).2 a))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     ((apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^
      @' ap
           (transport (D (f a))
              ((fst (ext n.+1) g).2 a)^) (g' a)
      @' apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
@' apD (s (f a)) ((fst (ext n.+1) g).2 a) = g' a
      rewrite !ap_pp, !concat_p_pp, ap_transport_pV.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
(apD (r (f a)) ((fst (ext n.+1) g).2 a))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^
@' (transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
      (r (f a) (g a))
    @' g' a
    @' (transport_pV (D (f a))
          ((fst (ext n.+1) g).2 a) (s (f a) (g a)))^)
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
@' apD (s (f a)) ((fst (ext n.+1) g).2 a) = g' a
      (* Even though https://github.com/coq/coq/issues/4533 is closed, this workaround is still needed. Without the Opaque setting, the [rewrite] unfolds the first [transport_pV] in the goal, and the first [moveR_Vp] below fails. *)
      Local Opaque transport_pV. (* work around bug 4533 *)
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
(apD (r (f a)) ((fst (ext n.+1) g).2 a))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^
@' (transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
      (r (f a) (g a))
    @' g' a
    @' (transport_pV (D (f a))
          ((fst (ext n.+1) g).2 a) (s (f a) (g a)))^)
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
@' apD (s (f a)) ((fst (ext n.+1) g).2 a) = g' a
      rewrite !concat_p_pp.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
(apD (r (f a)) ((fst (ext n.+1) g).2 a))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^
@' transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
     (r (f a) (g a))
@' g' a
@' (transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
      (s (f a) (g a)))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
@' apD (s (f a)) ((fst (ext n.+1) g).2 a) = g' a
      Local Transparent transport_pV. (* work around bug 4533 *)
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
(apD (r (f a)) ((fst (ext n.+1) g).2 a))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^
@' transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
     (r (f a) (g a))
@' g' a
@' (transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
      (s (f a) (g a)))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
@' apD (s (f a)) ((fst (ext n.+1) g).2 a) = g' a
      refine ((((_  @@ 1) @ concat_1p _) @@ 1 @@ 1 @@ 1) @ _).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
(apD (r (f a)) ((fst (ext n.+1) g).2 a))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^
@' transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
     (r (f a) (g a)) = 1
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type)
(ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type)
(r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C
  (fun (b : B) (c : C b) => r b c = s b c)
  (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
g' a
@' (transport_pV (D (f a)) 
      ((fst (ext n.+1) g).2 a) 
      (s (f a) (g a)))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
@' apD (s (f a)) ((fst (ext n.+1) g).2 a) = 
g' a
      *
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
(apD (r (f a)) ((fst (ext n.+1) g).2 a))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (r (f a)) ((fst (ext n.+1) g).2 a)^)^
@' transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
     (r (f a) (g a)) = 1 rewrite ap_V, concat_pp_p.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
(apD (r (f a)) ((fst (ext n.+1) g).2 a))^
@' ((ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
       (apD (r (f a)) ((fst (ext n.+1) g).2 a)^))^
    @' transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
         (r (f a) (g a))) = 1
        do 2 apply moveR_Vp.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
  (r (f a) (g a)) =
ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
  (apD (r (f a)) ((fst (ext n.+1) g).2 a)^)
@' (apD (r (f a)) ((fst (ext n.+1) g).2 a)
    @' 1)
        rewrite concat_p1.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
  (r (f a) (g a)) =
ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
  (apD (r (f a)) ((fst (ext n.+1) g).2 a)^)
@' apD (r (f a)) ((fst (ext n.+1) g).2 a)
        symmetry; apply transport_pV_ap.
      *
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
g' a
@' (transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
      (s (f a) (g a)))^
@' ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
     (apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
@' apD (s (f a)) ((fst (ext n.+1) g).2 a) = g' a rewrite !concat_pp_p.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
g' a
@' ((transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
       (s (f a) (g a)))^
    @' (ap
          (transport (D (f a))
             ((fst (ext n.+1) g).2 a))
          (apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
        @' apD (s (f a)) ((fst (ext n.+1) g).2 a))) =
g' a
        refine ((1 @@ _) @ (concat_p1 _)).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
(transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
   (s (f a) (g a)))^
@' (ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
      (apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
    @' apD (s (f a)) ((fst (ext n.+1) g).2 a)) = 1
        apply moveR_Vp; rewrite concat_p1.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
g: forall a : A, C (f a)
g': forall a : A, r (f a) (g a) = s (f a) (g a)
a: A
h:= (fst (ext n.+1) g).1: forall y : B, C y
ap (transport (D (f a)) ((fst (ext n.+1) g).2 a))
  (apD (s (f a)) ((fst (ext n.+1) g).2 a)^)
@' apD (s (f a)) ((fst (ext n.+1) g).2 a) =
transport_pV (D (f a)) ((fst (ext n.+1) g).2 a)
  (s (f a) (g a))
        apply transport_pV_ap.
      Close Scope long_path_scope.
  -
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
forall (h k : forall b : B, C b)
(h' : forall b : B, r b (h b) = s b (h b))
(k' : forall b : B, r b (k b) = s b (k b)),
ExtendableAlong_Over n f (fun b : B => h b = k b)
  (fun (b : B) (c : h b = k b) =>
   transport (fun c0 : C b => r b c0 = s b c0) c
     (h' b) = k' b) (snd (ext n.+1) h k) intros h k h' k'.
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
h, k: forall b : B, C b
h': forall b : B, r b (h b) = s b (h b)
k': forall b : B, r b (k b) = s b (k b)
ExtendableAlong_Over n f (fun b : B => h b = k b)
  (fun (b : B) (c : h b = k b) =>
   transport (fun c0 : C b => r b c0 = s b c0) c
     (h' b) = k' b) (snd (ext n.+1) h k)
    refine (extendable_over_postcompose' _ _ _ _ _ _
             (fun b c => equiv_cancelL (apD (r b) c) _ _) _).
A, B: Type
f: A -> B
n: nat
IHn: forall (C : B -> Type) (ext : ooExtendableAlong f C)
(D : forall b : B, C b -> Type) (r s : forall (b : B) (c : C b), D b c),
ooExtendableAlong_Over f C D ext ->
ExtendableAlong_Over n f C (fun (b : B) (c : C b) => r b c = s b c) (ext n)
C: B -> Type
ext: ooExtendableAlong f C
D: forall b : B, C b -> Type
r, s: forall (b : B) (c : C b), D b c
ext': ooExtendableAlong_Over f C D ext
h, k: forall b : B, C b
h': forall b : B, r b (h b) = s b (h b)
k': forall b : B, r b (k b) = s b (k b)
ExtendableAlong_Over n f (fun b : B => h b = k b)
  (fun (b : B) (c : h b = k b) =>
   apD (r b) c @
   transport (fun c0 : C b => r b c0 = s b c0) c
     (h' b) = apD (r b) c @ k' b) (snd (ext n.+1) h k)
    refine (IHn _ _ _ _ _
                (fun n => snd (ext' n.+1) h k
                              (fun b => r b (h b)) (fun b => s b (k b)))).
Qed.

(** ** Local types *)

Import IsLocal_Internal.

Definition islocal_equiv_islocal (f : LocalGenerators@{a})
           (X : Type@{i}) {Y : Type@{j}}
           (Xloc : IsLocal@{i i' a} f X)
           (g : X -> Y) `{IsEquiv@{i j} _ _ g}
: IsLocal@{j j' a} f Y.
f: LocalGenerators
X, Y: Type
Xloc: IsLocal f X
g: X -> Y
H: IsEquiv g
IsLocal f Y
Proof.
f: LocalGenerators
X, Y: Type
Xloc: IsLocal f X
g: X -> Y
H: IsEquiv g
IsLocal f Y
  intros i.
f: LocalGenerators
X, Y: Type
Xloc: IsLocal f X
g: X -> Y
H: IsEquiv g
i: lgen_indices f
ooExtendableAlong (f i)
  (fun _ : lgen_codomain f i => Y)
  (** We have to fiddle with the max universes to get this to work, since [ooextendable_postcompose] requires the max universe in both cases to be the same, whereas we don't want to assume that the hypothesis and conclusion are related in any way. *)
  apply lift_ooextendablealong@{a a a a a a j j j k j'}.
f: LocalGenerators
X, Y: Type
Xloc: IsLocal f X
g: X -> Y
H: IsEquiv g
i: lgen_indices f
ooExtendableAlong (f i)
  (fun _ : lgen_codomain f i => Y)
  refine (ooextendable_postcompose@{a a i j k k k k k k}
            _ _ (f i) (fun _ => g) _).
f: LocalGenerators
X, Y: Type
Xloc: IsLocal f X
g: X -> Y
H: IsEquiv g
i: lgen_indices f
ooExtendableAlong (f i)
  (fun _ : lgen_codomain f i => X)
  apply lift_ooextendablealong@{a a a a a a i i i i' k}.
f: LocalGenerators
X, Y: Type
Xloc: IsLocal f X
g: X -> Y
H: IsEquiv g
i: lgen_indices f
ooExtendableAlong (f i)
  (fun _ : lgen_codomain f i => X)
  apply Xloc.
Defined.

(** ** Localization as a HIT *)

Module Export LocalizationHIT.

  Cumulative Private Inductive Localize (f : LocalGenerators@{a}) (X : Type@{i})
  : Type@{max(a,i)} :=
  | loc : X -> Localize f X.

  Arguments loc {f X} x.

  (** Note that the following axiom actually contains a point-constructor.  We could separate out that point-constructor and make it an actual argument of the private inductive type, thereby getting a judgmental computation rule for it.  However, since locality is an hprop, there seems little point to this. *)
  Axiom islocal_localize
  : forall (f : LocalGenerators@{a}) (X : Type@{i}),
      IsLocal@{i k a} f (Localize f X).

  Definition Localize_ind
           (f : LocalGenerators@{a}) (X : Type@{i})
           (P : Localize f X -> Type@{j})
           (loc' : forall x, P (loc x))
           (islocal' : forall i, ooExtendableAlong_Over@{a a i j k}
                                   (f i) (fun _ => Localize@{a i} f X)
                                   (fun _ => P)
                                   (islocal_localize@{a i k} f X i))
           (z : Localize f X)
  : P z
    := match z with
         | loc x => fun _ => loc' x
       end islocal'.

  (** We now state the computation rule for [islocal_localize].  Since locality is an hprop, we never actually have any use for it, but the fact that we can state it is a reassuring check that we have defined a meaningful HIT. *)
  Axiom Localize_ind_islocal_localize_beta :
    forall (f : LocalGenerators) (X : Type)
           (P : Localize f X -> Type)
           (loc' : forall x, P (loc x))
           (islocal' : forall i, ooExtendableAlong_Over
                                   (f i) (fun _ => Localize f X)
                                   (fun _ => P)
                                   (islocal_localize f X i))
           i n,
      apD_extendable_eq n (fun _ => Localize f X) (f i)
                        (islocal_localize f X i n) (fun _ => P)
                        (fun _ => Localize_ind f X P loc' islocal')
                        (islocal' i n).

End LocalizationHIT.

(** Now we prove that localization is a reflective subuniverse. *)

Section Localization.

  Context (f : LocalGenerators).

  (** The induction principle is an equivalence. *)
  Definition ext_localize_ind (X : Type)
      (P : Localize f X -> Type)
      (Ploc : forall i, ooExtendableAlong_Over
                          (f i) (fun _ => Localize f X)
                          (fun _ => P) (islocal_localize f X i))
  : ooExtendableAlong loc P.
f: LocalGenerators
X: Type
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
ooExtendableAlong loc P
  Proof.
f: LocalGenerators
X: Type
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
ooExtendableAlong loc P
    intros n; generalize dependent P.
f: LocalGenerators
X: Type
n: nat
forall P : Localize f X -> Type,
(forall i : lgen_indices f,
 ooExtendableAlong_Over (f i)
   (fun _ : lgen_codomain f i => Localize f X)
   (fun _ : lgen_codomain f i => P)
   (islocal_localize f X i)) ->
ExtendableAlong n loc P
    simple_induction n n IHn; intros P Ploc.
f: LocalGenerators
X: Type
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
ExtendableAlong 0 loc P
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
 ooExtendableAlong_Over (f i)
   (fun _ : lgen_codomain f i => Localize f X)
   (fun _ : lgen_codomain f i => P)
   (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
ExtendableAlong n.+1 loc P
    1:exact tt.
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
ooExtendableAlong_Over (f i) (fun _ : lgen_codomain f i => Localize f X)
(fun _ : lgen_codomain f i => P) (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
ExtendableAlong n.+1 loc P
    split.
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
ooExtendableAlong_Over (f i) (fun _ : lgen_codomain f i => Localize f X)
(fun _ : lgen_codomain f i => P) (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
forall g : forall a : X, P (loc a),
ExtensionAlong loc P g
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
 ooExtendableAlong_Over (f i)
   (fun _ : lgen_codomain f i => Localize f X)
   (fun _ : lgen_codomain f i => P)
   (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
forall h k : forall b : Localize f X, P b,
ExtendableAlong n loc
  (fun b : Localize f X => h b = k b)
    -
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
ooExtendableAlong_Over (f i) (fun _ : lgen_codomain f i => Localize f X)
(fun _ : lgen_codomain f i => P) (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
forall g : forall a : X, P (loc a),
ExtensionAlong loc P g intros g.
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
ooExtendableAlong_Over (f i) (fun _ : lgen_codomain f i => Localize f X)
(fun _ : lgen_codomain f i => P) (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
g: forall a : X, P (loc a)
ExtensionAlong loc P g
      exists (Localize_ind f X P g Ploc).
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
ooExtendableAlong_Over (f i) (fun _ : lgen_codomain f i => Localize f X)
(fun _ : lgen_codomain f i => P) (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
g: forall a : X, P (loc a)
forall x : X, Localize_ind f X P g Ploc (loc x) = g x
      intros x; reflexivity.
    -
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
ooExtendableAlong_Over (f i) (fun _ : lgen_codomain f i => Localize f X)
(fun _ : lgen_codomain f i => P) (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
forall h k : forall b : Localize f X, P b,
ExtendableAlong n loc
  (fun b : Localize f X => h b = k b) intros h k; apply IHn; intros i m.
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
ooExtendableAlong_Over (f i) (fun _ : lgen_codomain f i => Localize f X)
(fun _ : lgen_codomain f i => P) (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
h, k: forall b : Localize f X, P b
i: lgen_indices f
m: nat
ExtendableAlong_Over m (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun (_ : lgen_codomain f i) (b : Localize f X) =>
   h b = k b) (islocal_localize f X i m)
      apply ooextendable_over_homotopy.
f: LocalGenerators
X: Type
n: nat
IHn: forall P : Localize f X -> Type,
(forall i : lgen_indices f,
ooExtendableAlong_Over (f i) (fun _ : lgen_codomain f i => Localize f X)
(fun _ : lgen_codomain f i => P) (islocal_localize f X i)) ->
ExtendableAlong n loc P
P: Localize f X -> Type
Ploc: forall i : lgen_indices f,
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun _ : lgen_codomain f i => P)
  (islocal_localize f X i)
h, k: forall b : Localize f X, P b
i: lgen_indices f
m: nat
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun (_ : lgen_codomain f i) (c : Localize f X) =>
   P c) (islocal_localize f X i)
      exact (Ploc i).
  Defined.

End Localization.

Definition Loc@{a i} (f : LocalGenerators@{a}) : ReflectiveSubuniverse@{i}.
f: LocalGenerators
ReflectiveSubuniverse
Proof.
f: LocalGenerators
ReflectiveSubuniverse
  snrefine (Build_ReflectiveSubuniverse
                                 (Build_Subuniverse (IsLocal f) _ _)
                                 (fun A => Build_PreReflects _ A (Localize f A) _ (@loc f A))
                                 (fun A => Build_Reflects _ _ _ _)).
f: LocalGenerators
Funext -> forall T : Type, IsHProp (IsLocal f T)
f: LocalGenerators
forall T U : Type,
IsLocal f T ->
forall f0 : T -> U, IsEquiv f0 -> IsLocal f U
f: LocalGenerators
A: Type
In
  {|
    In_internal := IsLocal f;
    hprop_inO_internal := ?hprop_inO_internal;
    inO_equiv_inO_internal := ?inO_equiv_inO_internal
  |} (Localize f A)
f: LocalGenerators
A: Type
forall Q : Type,
In
  {|
    In_internal := IsLocal f;
    hprop_inO_internal := ?hprop_inO_internal;
    inO_equiv_inO_internal := ?inO_equiv_inO_internal
  |} Q ->
ooExtendableAlong
  (to
     {|
       In_internal := IsLocal f;
       hprop_inO_internal := ?hprop_inO_internal;
       inO_equiv_inO_internal :=
         ?inO_equiv_inO_internal
     |} A)
  (fun
     _ : O_reflector
           {|
             In_internal := IsLocal f;
             hprop_inO_internal := ?hprop_inO_internal;
             inO_equiv_inO_internal :=
               ?inO_equiv_inO_internal
           |} A => Q)
  - (** Typeclass inference can find this, but we give it explicitly to prevent extra universes from cropping up. *)
f: LocalGenerators
Funext -> forall T : Type, IsHProp (IsLocal f T)
    intros ? T; unfold IsLocal.
f: LocalGenerators
H: Funext
T: Type
IsHProp
  (forall i : lgen_indices f,
   ooExtendableAlong (f i)
     (fun _ : lgen_codomain f i => T))
    nrefine (istrunc_forall@{a i i}); try assumption.
f: LocalGenerators
H: Funext
T: Type
forall a : lgen_indices f,
IsHProp
  (ooExtendableAlong (f a)
     (fun _ : lgen_codomain f a => T))
    intros i.
f: LocalGenerators
H: Funext
T: Type
i: lgen_indices f
IsHProp
  (ooExtendableAlong (f i)
     (fun _ : lgen_codomain f i => T))
    apply ishprop_ooextendable@{a a i i i
                                i i i i i
                                i i i i i i}.
  -
f: LocalGenerators
forall T U : Type,
IsLocal f T ->
forall f0 : T -> U, IsEquiv f0 -> IsLocal f U apply islocal_equiv_islocal.
  -
f: LocalGenerators
A: Type
In
  {|
    In_internal := IsLocal f;
    hprop_inO_internal :=
      fun (H : Funext) (T : Type) =>
      istrunc_forall : IsHProp (IsLocal f T);
    inO_equiv_inO_internal := islocal_equiv_islocal f
  |} (Localize f A) apply islocal_localize.
  -
f: LocalGenerators
A: Type
forall Q : Type,
In
  {|
    In_internal := IsLocal f;
    hprop_inO_internal :=
      fun (H : Funext) (T : Type) =>
      istrunc_forall : IsHProp (IsLocal f T);
    inO_equiv_inO_internal := islocal_equiv_islocal f
  |} Q ->
ooExtendableAlong
  (to
     {|
       In_internal := IsLocal f;
       hprop_inO_internal :=
         fun (H : Funext) (T : Type) =>
         istrunc_forall : IsHProp (IsLocal f T);
       inO_equiv_inO_internal :=
         islocal_equiv_islocal f
     |} A)
  (fun
     _ : O_reflector
           {|
             In_internal := IsLocal f;
             hprop_inO_internal :=
               fun (H : Funext) (T : Type) =>
               istrunc_forall : IsHProp (IsLocal f T);
             inO_equiv_inO_internal :=
               islocal_equiv_islocal f
           |} A => Q) cbn.
f: LocalGenerators
A: Type
forall Q : Type,
IsLocal f Q ->
ooExtendableAlong loc (fun _ : Localize f A => Q) intros Q Q_inO.
f: LocalGenerators
A, Q: Type
Q_inO: IsLocal f Q
ooExtendableAlong loc (fun _ : Localize f A => Q)
    apply ext_localize_ind; intros ?.
f: LocalGenerators
A, Q: Type
Q_inO: IsLocal f Q
i: lgen_indices f
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f A)
  (fun (_ : lgen_codomain f i) (_ : Localize f A) => Q)
  (islocal_localize f A i)
    apply ooextendable_over_const.
f: LocalGenerators
A, Q: Type
Q_inO: IsLocal f Q
i: lgen_indices f
ooExtendableAlong (f i)
  (fun _ : lgen_codomain f i => Q)
    apply Q_inO.
Defined.

(** Here is the "real" definition of the notation [IsLocal].  Defining it this way allows it to inherit typeclass inference from [In], unlike (for instance) the slightly annoying case of [IsTrunc n] versus [In (Tr n)]. *)
Notation IsLocal f := (In (Loc f)).

Section LocalTypes.
  Context (f : LocalGenerators).

  (** A remark on universes: recall that [ooExtendableAlong] takes four universe parameters, three for the sizes of the types involved and one for the max of all of them.  In the definition of [IsLocal f X] we set that max universe to be the same as the size of [X], so that [In (Loc f) X] would lie in the same universes as [X], which is necessary for our definition of a reflective subuniverse.  However, in practice we may need this extendability property with the max universe being larger, to avoid coalescing universes undesiredly.  Thus, in making it available by the following name, we also insert a [lift] to generalize the max universe. *)
  Definition ooextendable_islocal {X : Type@{i}} {Xloc : IsLocal f X} i
  : ooExtendableAlong@{a a i k} (f i) (fun _ => X)
    := (lift_ooextendablealong _ _ (Xloc i)).

  Global Instance islocal_loc (X : Type) : IsLocal f (Localize f X)
    := islocal_localize f X.

  Global Instance isequiv_precomp_islocal `{Funext}
         {X : Type} `{IsLocal f X} i
  : IsEquiv (fun g => g o f i)
  := isequiv_ooextendable (fun _ => X) (f i) (ooextendable_islocal i).

  (** The non-dependent eliminator *)
  Definition Localize_rec {X Z : Type} `{IsLocal f Z} (g : X -> Z)
  : Localize f X -> Z.
f: LocalGenerators
X, Z: Type
IsLocal0: In (Loc f) Z
g: X -> Z
Localize f X -> Z
  Proof.
f: LocalGenerators
X, Z: Type
IsLocal0: In (Loc f) Z
g: X -> Z
Localize f X -> Z
    refine (Localize_ind f X (fun _ => Z) g _); intros i.
f: LocalGenerators
X, Z: Type
IsLocal0: In (Loc f) Z
g: X -> Z
i: lgen_indices f
ooExtendableAlong_Over (f i)
  (fun _ : lgen_codomain f i => Localize f X)
  (fun (_ : lgen_codomain f i) (_ : Localize f X) => Z)
  (islocal_localize f X i)
    apply ooextendable_over_const.
f: LocalGenerators
X, Z: Type
IsLocal0: In (Loc f) Z
g: X -> Z
i: lgen_indices f
ooExtendableAlong (f i)
  (fun _ : lgen_codomain f i => Z)
    apply ooextendable_islocal.
  Defined.

  Definition local_rec {X} `{IsLocal f X} {i} (g : lgen_domain f i -> X)
  : lgen_codomain f i -> X
  := (fst (ooextendable_islocal i 1%nat) g).1.

  Definition local_rec_beta {X} `{IsLocal f X} {i} (g : lgen_domain f i -> X) s
  : local_rec g (f i s) = g s
    := (fst (ooextendable_islocal i 1%nat) g).2 s.

  Definition local_indpaths {X} `{IsLocal f X} {i} {h k : lgen_codomain f i -> X}
             (p : h o f i == k o f i)
  : h == k
    := (fst (snd (ooextendable_islocal i 2) h k) p).1.

  Definition local_indpaths_beta {X} `{IsLocal f X} {i} (h k : lgen_codomain f i -> X)
             (p : h o f i == k o f i) s
  : local_indpaths p (f i s) = p s
    := (fst (snd (ooextendable_islocal i 2) h k) p).2 s.

End LocalTypes.

Arguments local_rec : simpl never.
Arguments local_rec_beta : simpl never.
Arguments local_indpaths : simpl never.
Arguments local_indpaths_beta : simpl never.

(** ** Localization and accessibility *)

(** Localization subuniverses are accessible, essentially by definition.  Without the universe annotations, [a] and [i] get collapsed. *)
Global Instance accrsu_loc@{a i} (f : LocalGenerators@{a}) : IsAccRSU@{a i} (Loc@{a i} f).
f: LocalGenerators
IsAccRSU (Loc f)
Proof.
f: LocalGenerators
IsAccRSU (Loc f)
  unshelve econstructor.
f: LocalGenerators
LocalGenerators
f: LocalGenerators
forall X : Type,
In (Loc f) X <-> IsLocal_Internal.IsLocal ?acc_lgen X
  -
f: LocalGenerators
LocalGenerators exact f.
  -
f: LocalGenerators
forall X : Type,
In (Loc f) X <-> IsLocal_Internal.IsLocal f X intros; split; apply idmap.
Defined.

(** Conversely, if a subuniverse is accessible, then the corresponding localization subuniverse is equivalent to it, and moreover exists at every universe level and satisfies its computation rules judgmentally.  This is called [lift_accrsu] but in fact it works equally well to *lower* the universe level, as long as both levels are no smaller than the size [a] of the generators. *)
Definition lift_accrsu@{a i j} (O : Subuniverse@{i}) `{IsAccRSU@{a i} O}
  : ReflectiveSubuniverse@{j}
  := Loc@{a j} (acc_lgen O).

(** The lifted universe agrees with the original one, on any universe contained in both [i] and [j] *)
Global Instance O_eq_lift_accrsu@{a i j k} (O : Subuniverse@{i}) `{IsAccRSU@{a i} O}
  : O_eq@{i j k} O (lift_accrsu@{a i j} O).
O: Subuniverse
H: IsAccRSU O
O <=> lift_accrsu O
Proof.
O: Subuniverse
H: IsAccRSU O
O <=> lift_accrsu O
  (** Anyone stepping through this proof should do [Set Printing Universes]. *)
  split; intros A A_inO.
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In O A
In (lift_accrsu O) A
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (lift_accrsu O) A
In O A 
  -
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In O A
In (lift_accrsu O) A intros i.
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In O A
i: lgen_indices (acc_lgen O)
ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
    assert (e := fst (inO_iff_islocal O A) A_inO i).
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In O A
i: lgen_indices (acc_lgen O)
e: ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
    apply (lift_ooextendablealong@{a a a a a a i j k i j} (acc_lgen O i) (fun _ => A)).
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In O A
i: lgen_indices (acc_lgen O)
e: ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
    exact e.
  -
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (lift_accrsu O) A
In O A apply (inO_iff_islocal O).
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (lift_accrsu O) A
IsLocal_Internal.IsLocal (acc_lgen O) A
    intros i.
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (lift_accrsu O) A
i: lgen_indices (acc_lgen O)
ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
    pose (e := A_inO i).
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (lift_accrsu O) A
i: lgen_indices (acc_lgen O)
e:= A_inO i: ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
    apply (lift_ooextendablealong@{a a a a a a j i k j i} (acc_lgen O i) (fun _ => A)).
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (lift_accrsu O) A
i: lgen_indices (acc_lgen O)
e:= A_inO i: ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => A)
    exact e.
Defined.

Definition O_leq_lift_accrsu@{a i1 i2}
           (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{IsAccRSU@{a i1} O1}
           `{O_leq@{i1 i2 i2} O1 O2}
  : O_leq@{i2 i2 i2} (lift_accrsu@{a i1 i2} O1) O2.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
lift_accrsu O1 <= O2
Proof.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
lift_accrsu O1 <= O2
  intros B B_inO1.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
B: Type
B_inO1: In (lift_accrsu O1) B
In O2 B
  apply (inO_leq@{i1 i2 i2} O1 O2).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
B: Type
B_inO1: In (lift_accrsu O1) B
In O1 B
  apply (snd (inO_iff_islocal O1 B)).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
B: Type
B_inO1: In (lift_accrsu O1) B
IsLocal_Internal.IsLocal (acc_lgen O1) B
  intros i.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
B: Type
B_inO1: In (lift_accrsu O1) B
i: lgen_indices (acc_lgen O1)
ooExtendableAlong (acc_lgen O1 i)
  (fun _ : lgen_codomain (acc_lgen O1) i => B) specialize (B_inO1 i).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
B: Type
i: lgen_indices (acc_lgen O1)
B_inO1: ooExtendableAlong (acc_lgen O1 i)
  (fun _ : lgen_codomain (acc_lgen O1) i => B)
ooExtendableAlong (acc_lgen O1 i)
  (fun _ : lgen_codomain (acc_lgen O1) i => B)
  apply (lift_ooextendablealong@{a a a a a a i2 i1 i2 i2 i1} (acc_lgen O1 i) (fun _ => B)).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
B: Type
i: lgen_indices (acc_lgen O1)
B_inO1: ooExtendableAlong (acc_lgen O1 i)
  (fun _ : lgen_codomain (acc_lgen O1) i => B)
ooExtendableAlong (acc_lgen O1 i)
  (fun _ : lgen_codomain (acc_lgen O1) i => B)
  exact B_inO1.
Defined.

(** Similarly, because localization is a HIT that has an elimination rule into types in *all* universes, for accessible reflective subuniverses we can show that containment implies connectedness properties with the universe containments in the other order. *)
Definition isconnected_O_leq'@{a i1 i2}
           (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{IsAccRSU@{a i1} O1}
           (** Compared to [O_leq@{i1 i2 i1}] and [A : Type@{i1}] in [isconnected_O_leq], these two lines are what make [i2 <= i1] instead of vice versa. *)
           `{O_leq@{i1 i2 i2} O1 O2} (A : Type@{i2}) 
           `{IsConnected O2 A}
  : IsConnected O1 A.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
IsConnected O1 A
Proof.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
IsConnected O1 A
  (** Anyone stepping through this proof should do [Set Printing Universes]. *)
  srefine (isconnected_O_leq O1 (lift_accrsu@{a i1 i1} O1) A).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
IsAccRSU O1
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
O1 <= lift_accrsu O1
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
IsConnected (lift_accrsu O1) A
  1-2:exact _.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
IsConnected (lift_accrsu O1) A
  change (Contr@{i1} (Localize@{a i2} (acc_lgen@{a i1} O1) A)).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
Contr (Localize (acc_lgen O1) A)
  (** At this point you should also do [Unset Printing Notations] to see the universe annotation on [IsTrunc] change. *)
  refine (contr_equiv'@{i2 i1} _ 1%equiv).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
Contr (Localize (acc_lgen O1) A)
  change (IsConnected@{i2} (lift_accrsu@{a i1 i2} O1) A).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
IsConnected (lift_accrsu O1) A
  srapply (isconnected_O_leq _ O2).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A: Type
H1: IsConnected O2 A
lift_accrsu O1 <= O2
  rapply O_leq_lift_accrsu.
Defined.

(** And similarly for connected maps. *)
Definition conn_map_O_leq'@{a i1 i2}
           (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{IsAccRSU@{a i1} O1}
           `{O_leq@{i1 i2 i2} O1 O2} {A B : Type@{i2}}
           (f : A -> B) `{IsConnMap O2 A B f}
  : IsConnMap O1 f.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
IsConnMap O1 f
Proof.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
IsConnMap O1 f
  (** Anyone stepping through this proof should do [Set Printing Universes]. *)
  intros b.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
IsConnected O1 (hfiber f b)
  apply (isconnected_equiv' O1 (hfiber@{i2 i2} f b)).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
hfiber f b <~> hfiber f b
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
IsConnected O1 (hfiber f b)
  -
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
hfiber f b <~> hfiber f b srapply equiv_adjointify.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
hfiber f b -> hfiber f b
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
hfiber f b -> hfiber f b
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
?f o ?g == idmap
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
?g o ?f == idmap
    1-2:intros [u p]; exact (u;p).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
(fun X : hfiber f b =>
 (fun (u : A) (p : f u = b) => (u; p)) X.1 X.2)
o (fun X : hfiber f b =>
   (fun (u : A) (p : f u = b) => (u; p)) X.1 X.2) ==
idmap
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
(fun X : hfiber f b =>
 (fun (u : A) (p : f u = b) => (u; p)) X.1 X.2)
o (fun X : hfiber f b =>
   (fun (u : A) (p : f u = b) => (u; p)) X.1 X.2) ==
idmap
    all:intros [u p]; reflexivity.
  -
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
IsConnected O1 (hfiber f b) apply (isconnected_O_leq' O1 O2).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
H1: IsConnMap O2 f
b: B
IsConnected O2 (hfiber f b)
    apply isconnected_hfiber_conn_map.
Defined.

(** The same is true for inverted maps, too. *)
Definition O_inverts_O_leq'@{a i1 i2}
           (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{IsAccRSU@{a i1} O1}
           `{O_leq@{i1 i2 i2} O1 O2} {A B : Type@{i2}}
           (f : A -> B) `{O_inverts O2 f}
  : O_inverts O1 f.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
O_inverts0: O_inverts O2 f
O_inverts O1 f
Proof.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
O_inverts0: O_inverts O2 f
O_inverts O1 f
  assert (oleq := O_leq_lift_accrsu O1 O2).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
O_inverts0: O_inverts O2 f
oleq: lift_accrsu O1 <= O2
O_inverts O1 f
  assert (e := O_inverts_O_leq (lift_accrsu@{a i1 i2} O1) O2 f); clear oleq.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
O_inverts0: O_inverts O2 f
e: O_inverts (lift_accrsu O1) f
O_inverts O1 f
  nrapply (O_inverts_O_leq O1 (lift_accrsu@{a i1 i1} O1) f).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
O_inverts0: O_inverts O2 f
e: O_inverts (lift_accrsu O1) f
O1 <= lift_accrsu O1
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
O_inverts0: O_inverts O2 f
e: O_inverts (lift_accrsu O1) f
O_inverts (lift_accrsu O1) f
  1:exact _.
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
O_inverts0: O_inverts O2 f
e: O_inverts (lift_accrsu O1) f
O_inverts (lift_accrsu O1) f
  (** It looks like we can say [exact e], but that would collapse the universes [i1] and [i2].  You can check with [Set Printing Universes. Unset Printing Notations.] that [e] and the goal have different universes.  So instead we do this: *)
  refine (@isequiv_homotopic _ _ _ _ e _).
O1, O2: ReflectiveSubuniverse
H: IsAccRSU O1
H0: O1 <= O2
A, B: Type
f: A -> B
O_inverts0: O_inverts O2 f
e: O_inverts (lift_accrsu O1) f
O_functor (lift_accrsu O1) f ==
O_functor (lift_accrsu O1) f
  apply O_indpaths; intros x; reflexivity.
Defined.