(** * Kan extensions of type families *)

(** This is part of the formalization of section 4 of the paper: Injective Types in Univalent Mathematics by Martín Escardó.  Many proofs are guided by Martín Escardó's original Agda formalization of this paper which can be found at: https://www.cs.bham.ac.uk/~mhe/TypeTopology/InjectiveTypes.Article.html. *)

Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Sigma Types.Unit Types.Arrow Types.Forall Types.Empty Types.Universe Types.Equiv Types.Paths.
Require Import HFiber.
Require Import Truncations.Core.
Require Import Modalities.ReflectiveSubuniverse Modalities.Modality.

(** We are careful about universe variables for these first few definitions because they are used in the rest of the paper.  We use [u], [v], [w], etc. as our typical universe variables. Our convention for the max of two universes [u] and [v] is [uv]. *)

Section UniverseStructure.
  Universes u v w uv uw vw uvw.
  Constraint u <= uv, v <= uv, u <= uw, w <= uw, v <= vw, w <= vw,
    uv <= uvw, uw <= uvw, vw <= uvw.

  Definition LeftKanFam@{} {X : Type@{u}} {Y : Type@{v}} (P : X -> Type@{w}) (j : X -> Y)
    : Y -> Type@{uvw}
    := fun y => sig@{uv w} (fun (w : hfiber j y) => P (w.1)).

  Definition RightKanFam@{} {X : Type@{u}} {Y : Type@{v}} (P : X -> Type@{w}) (j : X -> Y)
    : Y -> Type@{uvw}
    := fun y => forall (w : hfiber j y), P (w.1).

  (** Below we will introduce notations [P <| j] and [P |> j] for these Kan extensions. *)

  (** If [j] is an embedding, then [P <| j] and [P |> j] are extensions in the following sense: [(P <| j o j) x <~> P x <~> (P |> j o j) x].  So, with univalence, we get that they are extensions. *)

  Definition isext_equiv_leftkanfam@{} {X : Type@{u}} {Y : Type@{v}}
    (P : X -> Type@{w}) (j : X -> Y) (isem : IsEmbedding@{u v uv} j) (x : X)
    : Equiv@{uvw w} (LeftKanFam@{} P j (j x)) (P x).
X, Y: Type
P: X -> Type
j: X -> Y
isem: IsEmbedding j
x: X
LeftKanFam P j (j x) <~> P x
  Proof.
X, Y: Type
P: X -> Type
j: X -> Y
isem: IsEmbedding j
x: X
LeftKanFam P j (j x) <~> P x
    exact (@equiv_contr_sigma (hfiber j (j x)) _ _).
  Defined.

  Definition isext_equiv_rightkanfam@{} `{Funext} {X : Type@{u}} {Y : Type@{v}}
    (P : X -> Type@{w}) (j : X -> Y) (isem : IsEmbedding@{u v uv} j) (x : X)
    : Equiv@{uvw w} (RightKanFam@{} P j (j x)) (P x).
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
isem: IsEmbedding j
x: X
RightKanFam P j (j x) <~> P x
  Proof.
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
isem: IsEmbedding j
x: X
RightKanFam P j (j x) <~> P x
    exact (@equiv_contr_forall _ (hfiber j (j x)) _ _).
  Defined.

  Definition isext_leftkanfam@{suvw | uvw < suvw} `{Univalence} {X : Type@{u}} {Y : Type@{v}}
    (P : X -> Type@{w}) (j : X -> Y) (isem : IsEmbedding@{u v uv} j) (x : X)
    : @paths@{suvw} Type@{uvw} (LeftKanFam@{} P j (j x)) (P x)
    := path_universe_uncurried (isext_equiv_leftkanfam _ _ _ _).

  Definition isext_rightkanfam@{suvw | uvw < suvw} `{Univalence} {X : Type@{u}} {Y : Type@{v}}
    (P : X -> Type@{w}) (j : X -> Y) (isem : IsEmbedding@{u v uv} j) (x : X)
    : @paths@{suvw} Type@{uvw} (RightKanFam@{} P j (j x)) (P x)
    := path_universe_uncurried (isext_equiv_rightkanfam _ _ _ _).

End UniverseStructure.

Notation "P <| j" := (LeftKanFam P j) : function_scope.
Notation "P |> j" := (RightKanFam P j) : function_scope.

(** For [y : Y] not in the image of [j], [(P <| j) y] is empty and [(P |> j) y] is contractible. *)
Definition isempty_leftkanfam {X : Type} {Y : Type}
  (P : X -> Type) (j : X -> Y) (y : Y) (ynin : forall x : X, j x <> y)
  : (P <| j) y -> Empty
  := fun '((x; p); _) => ynin x p.

Definition contr_rightkanfam `{Funext} {X : Type} {Y : Type}
  (P : X -> Type@{w}) (j : X -> Y) (y : Y) (ynin : forall x : X, j x <> y)
  : Contr ((P |> j) y).
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
y: Y
ynin: forall x : X, j x <> y
Contr ((P |> j) y)
Proof.
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
y: Y
ynin: forall x : X, j x <> y
Contr ((P |> j) y)
  snapply contr_forall.
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
y: Y
ynin: forall x : X, j x <> y
forall a : hfiber j y,
Contr ((fun a0 : hfiber j y => P a0.1) a)
  intros [x p].
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
y: Y
ynin: forall x : X, j x <> y
x: X
p: j x = y
Contr (P (x; p).1)
  apply (Empty_rec (ynin x p)).
Defined.

(** The following equivalences tell us that [{ y : Y & (P <| j) y}] and [forall y : Y, (P |> j) y] can be thought of as just different notation for the sum and product of a type family. *)
Definition equiv_leftkanfam {X : Type} {Y : Type}
  (P : X -> Type) (j : X -> Y)
  : {x : X & P x} <~> {y : Y & (P <| j) y}.
X, Y: Type
P: X -> Type
j: X -> Y
{x : X & P x} <~> {y : Y & (P <| j) y}
Proof.
X, Y: Type
P: X -> Type
j: X -> Y
{x : X & P x} <~> {y : Y & (P <| j) y}
  snapply equiv_adjointify.
X, Y: Type
P: X -> Type
j: X -> Y
{x : X & P x} -> {y : Y & (P <| j) y}
X, Y: Type
P: X -> Type
j: X -> Y
{y : Y & (P <| j) y} -> {x : X & P x}
X, Y: Type
P: X -> Type
j: X -> Y
?f o ?g == idmap
X, Y: Type
P: X -> Type
j: X -> Y
?g o ?f == idmap
  -
X, Y: Type
P: X -> Type
j: X -> Y
{x : X & P x} -> {y : Y & (P <| j) y} exact (fun w : {x : X & P x} => (j w.1; (w.1; idpath); w.2)).
  -
X, Y: Type
P: X -> Type
j: X -> Y
{y : Y & (P <| j) y} -> {x : X & P x} exact (fun '((y; ((x; p); y')) : {y : Y & (P <| j) y}) => (x; y')).
  -
X, Y: Type
P: X -> Type
j: X -> Y
(fun w : {x : X & P x} => (j w.1; (w.1; 1); w.2))
o (fun pat : {y : Y & (P <| j) y} =>
   let x := pat in
   let y := x.1 in
   let proj2 := x.2 in
   let proj3 := proj2 in
   let proj1 := proj3.1 in
   let y' := proj3.2 in
   (let proj4 := proj1 in
    let x0 := proj4.1 in
    let p := proj4.2 in
    fun y'0 : P (x0; p).1 => (x0; y'0)) y') == idmap by intros [y [[x []] y']].
  -
X, Y: Type
P: X -> Type
j: X -> Y
(fun pat : {y : Y & (P <| j) y} =>
 let x := pat in
 let y := x.1 in
 let proj2 := x.2 in
 let proj3 := proj2 in
 let proj1 := proj3.1 in
 let y' := proj3.2 in
 (let proj4 := proj1 in
  let x0 := proj4.1 in
  let p := proj4.2 in
  fun y'0 : P (x0; p).1 => (x0; y'0)) y')
o (fun w : {x : X & P x} => (j w.1; (w.1; 1); w.2)) ==
idmap reflexivity.
Defined.

Definition equiv_rightkanfam `{Funext} {X : Type} {Y : Type}
  (P : X -> Type@{w}) (j : X -> Y)
  : (forall x, P x) <~> (forall y, (P |> j) y).
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
(forall x : X, P x) <~> (forall y : Y, (P |> j) y)
Proof.
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
(forall x : X, P x) <~> (forall y : Y, (P |> j) y)
  snapply equiv_adjointify.
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
(forall x : X, P x) -> forall y : Y, (P |> j) y
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
(forall y : Y, (P |> j) y) -> forall x : X, P x
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
?f o ?g == idmap
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
?g o ?f == idmap
  -
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
(forall x : X, P x) -> forall y : Y, (P |> j) y intros g y w.
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
g: forall x : X, P x
y: Y
w: hfiber j y
P w.1 exact (g w.1).
  -
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
(forall y : Y, (P |> j) y) -> forall x : X, P x exact (fun h x => h (j x) (x; idpath)).
  -
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
(fun (g : forall x : X, P x) (y : Y) =>
 (fun w : hfiber j y => g w.1) : (P |> j) y)
o (fun (h : forall y : Y, (P |> j) y) (x : X) =>
   h (j x) (x; 1)) == idmap intros h.
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
h: forall y : Y, (P |> j) y
(fun (y : Y) (w : hfiber j y) => h (j w.1) (w.1; 1)) =
h by funext y [x []].
  -
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
(fun (h : forall y : Y, (P |> j) y) (x : X) =>
 h (j x) (x; 1))
o (fun (g : forall x : X, P x) (y : Y) =>
   (fun w : hfiber j y => g w.1) : (P |> j) y) ==
idmap intros g.
H: Funext
X, Y: Type
P: X -> Type
j: X -> Y
g: forall x : X, P x
(fun x : X => g (x; 1).1) = g by apply path_forall.
Defined.

(** Here we are taking the perspective of a type family [P : X -> Type] as an oo-presheaf, considering the interpretation of [X] as an oo-groupoid and [Type] as a universe of spaces i.e. an appropriate generalization of the category of sets. It is easy to see that a type family [P] is functorial if we define its action on paths with [transport]. Functoriality then reduces to known lemmas about the [transport] function. *)

(** With this in mind, we define the type of transformations between two type families. [concat_Ap] says that these transformations are automatically natural. *)
Definition MapFam {X : Type} (P : X -> Type) (R : X -> Type)
  := forall x, P x -> R x.

Notation "P >=> R" := (MapFam P R) : function_scope.

(** Composition of transformations. *)
Definition compose_mapfam {X} {P R Q : X -> Type} (b : R >=> Q) (a : P >=> R)
  : P >=> Q
  := fun x => (b x) o (a x).

(** If [j] is an embedding then [(P <| j) =< (P |> j)]. *)
Definition transform_leftkanfam_rightkanfam {X Y : Type}
  (P : X -> Type) (j : X -> Y) (isem : IsEmbedding j)
  : (P <| j) >=> (P |> j).
X, Y: Type
P: X -> Type
j: X -> Y
isem: IsEmbedding j
P <| j >=> P |> j
Proof.
X, Y: Type
P: X -> Type
j: X -> Y
isem: IsEmbedding j
P <| j >=> P |> j
  intros y [w' z] w.
X, Y: Type
P: X -> Type
j: X -> Y
isem: IsEmbedding j
y: Y
w': hfiber j y
z: P w'.1
w: hfiber j y
P w.1
  snapply (transport (fun a => P a.1) _ z).
X, Y: Type
P: X -> Type
j: X -> Y
isem: IsEmbedding j
y: Y
w': hfiber j y
z: P w'.1
w: hfiber j y
w' = w
  srapply path_ishprop.
Defined.

(** Under this interpretation, we can think of the maps [P <| j] and [P |> j] as left and right Kan extensions of [P : X -> Type] along [j : X -> Y]. To see this we can construct the (co)unit transformations of our extensions. *)
Definition unit_leftkanfam {X Y : Type} (P : X -> Type) (j : X -> Y)
  : P >=> ((P <| j) o j)
  := fun x A => ((x; idpath); A).

Definition counit_rightkanfam {X Y : Type} (P : X -> Type) (j : X -> Y)
  : ((P |> j) o j) >=> P
  := fun x A => A (x; idpath).

Definition counit_leftkanfam {X Y : Type} (R : Y -> Type) (j : X -> Y)
  : ((R o j) <| j) >=> R.
X, Y: Type
R: Y -> Type
j: X -> Y
(R o j) <| j >=> R
Proof.
X, Y: Type
R: Y -> Type
j: X -> Y
(R o j) <| j >=> R
  intros y [[x p] C].
X, Y: Type
R: Y -> Type
j: X -> Y
y: Y
x: X
p: j x = y
C: R (j (x; p).1)
R y
  exact (transport R p C).
Defined.

Definition unit_rightkanfam {X Y : Type} (R : Y -> Type) (j : X -> Y)
  : R >=> ((R o j) |> j).
X, Y: Type
R: Y -> Type
j: X -> Y
R >=> (R o j) |> j
Proof.
X, Y: Type
R: Y -> Type
j: X -> Y
R >=> (R o j) |> j
  intros y C [x p].
X, Y: Type
R: Y -> Type
j: X -> Y
y: Y
C: R y
x: X
p: j x = y
R (j (x; p).1)
  exact (transport R p^ C).
Defined.

(** Universal property of the Kan extensions. *)
Definition univ_property_leftkanfam {X Y} {j : X -> Y}
  {P : X -> Type} {R : Y -> Type} (a : P >=> R o j)
  : { b : P <| j >=> R & compose_mapfam (b o j) (unit_leftkanfam P j) == a}.
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
{b : P <| j >=> R &
compose_mapfam (b o j) (unit_leftkanfam P j) == a}
Proof.
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
{b : P <| j >=> R &
compose_mapfam (b o j) (unit_leftkanfam P j) == a}
  snrefine (_; _).
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
P <| j >=> R
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
(fun b : P <| j >=> R =>
 compose_mapfam (b o j) (unit_leftkanfam P j) == a)
  ?proj1
  -
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
P <| j >=> R intros y [[x p] A].
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
y: Y
x: X
p: j x = y
A: P (x; p).1
R y exact (p # a x A).
  -
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
(fun b : P <| j >=> R =>
 compose_mapfam (b o j) (unit_leftkanfam P j) == a)
  ((fun (y : Y) (X0 : (P <| j) y) =>
    (fun proj1 : hfiber j y =>
     (fun (x : X) (p : j x = y) (A : P (x; p).1) =>
      transport R p (a x A)) proj1.1 proj1.2) X0.1
      X0.2)
   :
   P <| j >=> R) intros x.
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
x: X
compose_mapfam
  (fun (x : X) (X0 : (P <| j) (j x)) =>
   transport R (X0.1).2 (a (X0.1).1 X0.2))
  (unit_leftkanfam P j) x = a x reflexivity.
Defined.

Definition contr_univ_property_leftkanfam `{Funext} {X Y} {j : X -> Y}
  {P : X -> Type} {R : Y -> Type} {a : P >=> R o j}
  : Contr { b : P <| j >=> R | compose_mapfam (b o j) (unit_leftkanfam P j) == a}.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
Contr
  {b : P <| j >=> R &
  compose_mapfam (b o j) (unit_leftkanfam P j) == a}
Proof.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
Contr
  {b : P <| j >=> R &
  compose_mapfam (b o j) (unit_leftkanfam P j) == a}
  apply (Build_Contr _ (univ_property_leftkanfam a)).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
forall
y : {b : P <| j >=> R &
    compose_mapfam (fun x : X => b (j x))
      (unit_leftkanfam P j) == a},
univ_property_leftkanfam a = y
  intros [b F].
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
univ_property_leftkanfam a = (b; F)
  symmetry. (* Do now to avoid inversion in the first subgoal. *)
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
(b; F) = univ_property_leftkanfam a
  srapply path_sigma.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
(b; F).1 = (univ_property_leftkanfam a).1
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
transport
  (fun b : P <| j >=> R =>
   compose_mapfam (fun x : X => b (j x))
     (unit_leftkanfam P j) == a) ?p (b; F).2 =
(univ_property_leftkanfam a).2
  -
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
(b; F).1 = (univ_property_leftkanfam a).1 funext y.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
y: Y
(b; F).1 y = (univ_property_leftkanfam a).1 y funext [[w []] c].
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
y: Y
w: X
c: P (w; 1).1
(b; F).1 (j w) ((w; 1); c) =
(univ_property_leftkanfam a).1 (j w) ((w; 1); c) srefine (ap10 (F w) c).
  -
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
transport
  (fun b : P <| j >=> R =>
   compose_mapfam (fun x : X => b (j x))
     (unit_leftkanfam P j) == a)
  (path_forall (b; F).1 (univ_property_leftkanfam a).1
     ((fun y : Y =>
       path_forall ((b; F).1 y)
         ((univ_property_leftkanfam a).1 y)
         ((fun x : (P <| j) y =>
           (fun proj1 : hfiber j y =>
            (fun (w : X) (proj2 : j w = y) =>
             match
               proj2 as p in (_ = y0)
               return
                 (forall proj3 : P ....1,
                  ....1 y0 ... = ....1 y0 ...)
             with
             | 1 => fun c : P (w; 1).1 => ap10 (F w) c
             end) proj1.1 proj1.2) x.1 x.2)
          :
          (b; F).1 y ==
          (univ_property_leftkanfam a).1 y))
      :
      (b; F).1 == (univ_property_leftkanfam a).1))
  (b; F).2 = (univ_property_leftkanfam a).2 simpl.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
transport
  (fun b : P <| j >=> R =>
   compose_mapfam (fun x : X => b (j x))
     (unit_leftkanfam P j) == a)
  (path_forall b
     (fun (y : Y) (X0 : (P <| j) y) =>
      transport R (X0.1).2 (a (X0.1).1 X0.2))
     (fun y : Y =>
      path_forall (b y)
        (fun X0 : (P <| j) y =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun x : (P <| j) y =>
         match
           (x.1).2 as p in (_ = y0)
           return
             (forall proj2 : P (x.1).1,
              b y0 (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => ap10 (F (x.1).1) c
         end x.2))) F = (fun x : X => 1)
    funext x.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
transport
  (fun b : P <| j >=> R =>
   compose_mapfam (fun x : X => b (j x))
     (unit_leftkanfam P j) == a)
  (path_forall b
     (fun (y : Y) (X0 : (P <| j) y) =>
      transport R (X0.1).2 (a (X0.1).1 X0.2))
     (fun y : Y =>
      path_forall (b y)
        (fun X0 : (P <| j) y =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun x : (P <| j) y =>
         match
           (x.1).2 as p in (_ = y0)
           return
             (forall proj2 : P (x.1).1,
              b y0 (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => ap10 (F (x.1).1) c
         end x.2))) F x = 1
    lhs napply transport_forall_constant.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
transport
  (fun x0 : P <| j >=> R =>
   compose_mapfam (fun x : X => x0 (j x))
     (unit_leftkanfam P j) x = a x)
  (path_forall b
     (fun (y : Y) (X0 : (P <| j) y) =>
      transport R (X0.1).2 (a (X0.1).1 X0.2))
     (fun y : Y =>
      path_forall (b y)
        (fun X0 : (P <| j) y =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun x : (P <| j) y =>
         match
           (x.1).2 as p in (_ = y0)
           return
             (forall proj2 : P (x.1).1,
              b y0 (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => ap10 (F (x.1).1) c
         end x.2))) (F x) = 1
    lhs napply transport_paths_Fl.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
(ap
   (fun x0 : P <| j >=> R =>
    compose_mapfam (fun x : X => x0 (j x))
      (unit_leftkanfam P j) x)
   (path_forall b
      (fun (y : Y) (X0 : (P <| j) y) =>
       transport R (X0.1).2 (a (X0.1).1 X0.2))
      (fun y : Y =>
       path_forall (b y)
         (fun X0 : (P <| j) y =>
          transport R (X0.1).2 (a (X0.1).1 X0.2))
         (fun x : (P <| j) y =>
          match
            (x.1).2 as p in (_ = y0)
            return
              (forall proj2 : P (x.1).1,
               b y0 (((x.1).1; p); proj2) =
               transport R p (a (x.1).1 proj2))
          with
          | 1 =>
              fun c : P (x.1).1 => ap10 (F (x.1).1) c
          end x.2))))^ @ F x = 1
    apply moveR_Vp.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
F x =
ap
  (fun x0 : P <| j >=> R =>
   compose_mapfam (fun x : X => x0 (j x))
     (unit_leftkanfam P j) x)
  (path_forall b
     (fun (y : Y) (X0 : (P <| j) y) =>
      transport R (X0.1).2 (a (X0.1).1 X0.2))
     (fun y : Y =>
      path_forall (b y)
        (fun X0 : (P <| j) y =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun x : (P <| j) y =>
         match
           (x.1).2 as p in (_ = y0)
           return
             (forall proj2 : P (x.1).1,
              b y0 (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => ap10 (F (x.1).1) c
         end x.2))) @ 1
    rhs napply concat_p1.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
F x =
ap
  (fun x0 : P <| j >=> R =>
   compose_mapfam (fun x : X => x0 (j x))
     (unit_leftkanfam P j) x)
  (path_forall b
     (fun (y : Y) (X0 : (P <| j) y) =>
      transport R (X0.1).2 (a (X0.1).1 X0.2))
     (fun y : Y =>
      path_forall (b y)
        (fun X0 : (P <| j) y =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun x : (P <| j) y =>
         match
           (x.1).2 as p in (_ = y0)
           return
             (forall proj2 : P (x.1).1,
              b y0 (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => ap10 (F (x.1).1) c
         end x.2)))
    unfold compose_mapfam, unit_leftkanfam.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
F x =
ap
  (fun (x0 : P <| j >=> R) (x1 : P x) =>
   x0 (j x) ((x; 1); x1))
  (path_forall b
     (fun (y : Y) (X0 : (P <| j) y) =>
      transport R (X0.1).2 (a (X0.1).1 X0.2))
     (fun y : Y =>
      path_forall (b y)
        (fun X0 : (P <| j) y =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun x : (P <| j) y =>
         match
           (x.1).2 as p in (_ = y0)
           return
             (forall proj2 : P (x.1).1,
              b y0 (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => ap10 (F (x.1).1) c
         end x.2)))
    symmetry.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
ap
  (fun (x0 : P <| j >=> R) (x1 : P x) =>
   x0 (j x) ((x; 1); x1))
  (path_forall b
     (fun (y : Y) (X0 : (P <| j) y) =>
      transport R (X0.1).2 (a (X0.1).1 X0.2))
     (fun y : Y =>
      path_forall (b y)
        (fun X0 : (P <| j) y =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun x : (P <| j) y =>
         match
           (x.1).2 as p in (_ = y0)
           return
             (forall proj2 : P (x.1).1,
              b y0 (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => ap10 (F (x.1).1) c
         end x.2))) = F x
    pose (i := fun px: P x => ((x; 1); px) : (P <| j) (j x)).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
i:= fun px : P x => ((x; 1); px) : (P <| j) (j x): P x -> (P <| j) (j x)
ap
  (fun (x0 : P <| j >=> R) (x1 : P x) =>
   x0 (j x) ((x; 1); x1))
  (path_forall b
     (fun (y : Y) (X0 : (P <| j) y) =>
      transport R (X0.1).2 (a (X0.1).1 X0.2))
     (fun y : Y =>
      path_forall (b y)
        (fun X0 : (P <| j) y =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun x : (P <| j) y =>
         match
           (x.1).2 as p in (_ = y0)
           return
             (forall proj2 : P (x.1).1,
              b y0 (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => ap10 (F (x.1).1) c
         end x.2))) = F x
    lhs napply (ap_compose (fun k : (P <| j) >=> R => k (j x)) (fun ka => ka o i)).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
i:= fun px : P x => ((x; 1); px) : (P <| j) (j x): P x -> (P <| j) (j x)
ap
  (fun (ka : (P <| j) (j x) -> R (j x)) (x : P x) =>
   ka (i x))
  (ap (fun k : P <| j >=> R => k (j x))
     (path_forall b
        (fun (y : Y) (X0 : (P <| j) y) =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun y : Y =>
         path_forall (b y)
           (fun X0 : (P <| j) y =>
            transport R (X0.1).2 (a (X0.1).1 X0.2))
           (fun x : (P <| j) y =>
            match
              (x.1).2 as p in (_ = y0)
              return
                (forall proj2 : P (x.1).1,
                 b y0 (((x.1).1; p); proj2) =
                 transport R p (a (x.1).1 proj2))
            with
            | 1 =>
                fun c : P (x.1).1 =>
                ap10 (F (x.1).1) c
            end x.2)))) = F x
    (* [ap (fun k => k (j x))] is exactly [apD10], so it cancels the first [path_forall]. *)
    lhs nrefine (ap _ (apD10_path_forall _ _ _ _)).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
i:= fun px : P x => ((x; 1); px) : (P <| j) (j x): P x -> (P <| j) (j x)
ap
  (fun (ka : (P <| j) (j x) -> R (j x)) (x : P x) =>
   ka (i x))
  (path_forall (b (j x))
     (fun X0 : (P <| j) (j x) =>
      transport R (X0.1).2 (a (X0.1).1 X0.2))
     (fun x : (P <| j) (j x) =>
      match
        (x.1).2 as p in (_ = y)
        return
          (forall proj2 : P (x.1).1,
           b y (((x.1).1; p); proj2) =
           transport R p (a (x.1).1 proj2))
      with
      | 1 => fun c : P (x.1).1 => ap10 (F (x.1).1) c
      end x.2)) = F x
    lhs rapply (ap_precompose _ i).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
i:= fun px : P x => ((x; 1); px) : (P <| j) (j x): P x -> (P <| j) (j x)
path_arrow (fun x0 : P x => b (j x) (i x0))
  (fun x0 : P x =>
   transport R ((i x0).1).2 (a ((i x0).1).1 (i x0).2))
  (fun x0 : P x =>
   ap10
     (path_forall (b (j x))
        (fun X0 : (P <| j) (j x) =>
         transport R (X0.1).2 (a (X0.1).1 X0.2))
        (fun x : (P <| j) (j x) =>
         match
           (x.1).2 as p in (_ = y)
           return
             (forall proj2 : P (x.1).1,
              b y (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => ap10 (F (x.1).1) c
         end x.2)) (i x0)) = F x
    unfold path_forall, ap10.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
i:= fun px : P x => ((x; 1); px) : (P <| j) (j x): P x -> (P <| j) (j x)
path_arrow (fun x0 : P x => b (j x) (i x0))
  (fun x0 : P x =>
   transport R ((i x0).1).2 (a ((i x0).1).1 (i x0).2))
  (fun x0 : P x =>
   apD10
     (apD10^-1
        (fun x : (P <| j) (j x) =>
         match
           (x.1).2 as p in (_ = y)
           return
             (forall proj2 : P (x.1).1,
              b y (((x.1).1; p); proj2) =
              transport R p (a (x.1).1 proj2))
         with
         | 1 =>
             fun c : P (x.1).1 => apD10 (F (x.1).1) c
         end x.2)) (i x0)) = F x
    rewrite (eisretr apD10); cbn.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: P >=> R o j
b: P <| j >=> R
F: compose_mapfam (fun x : X => b (j x))
  (unit_leftkanfam P j) == a
x: X
i:= fun px : P x => ((x; 1); px) : (P <| j) (j x): P x -> (P <| j) (j x)
path_arrow (fun x0 : P x => b (j x) (i x0))
  (fun x0 : P x => a x x0)
  (fun x0 : P x => apD10 (F x) x0) = F x
    apply eissect.
Defined.

Definition univ_property_rightkanfam {X Y} {j : X -> Y}
  {P : X -> Type} {R : Y -> Type} (a : R o j >=> P)
  : { b : R >=> P |> j & compose_mapfam (counit_rightkanfam P j) (b o j) == a}.
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
{b : R >=> P |> j &
compose_mapfam (counit_rightkanfam P j) (b o j) == a}
Proof.
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
{b : R >=> P |> j &
compose_mapfam (counit_rightkanfam P j) (b o j) == a}
  snrefine (_; _).
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
R >=> P |> j
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
(fun b : R >=> P |> j =>
 compose_mapfam (counit_rightkanfam P j) (b o j) == a)
  ?proj1
  -
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
R >=> P |> j intros y A [x p].
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
y: Y
A: R y
x: X
p: j x = y
P (x; p).1 exact (a x (p^ # A)).
  -
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
(fun b : R >=> P |> j =>
 compose_mapfam (counit_rightkanfam P j) (b o j) == a)
  ((fun (y : Y) (A : R y) =>
    (fun w : hfiber j y =>
     (fun (x : X) (p : j x = y) =>
      a x (transport R p^ A)) w.1 w.2)
    :
    (P |> j) y)
   :
   R >=> P |> j) intro x.
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
x: X
compose_mapfam (counit_rightkanfam P j)
  (fun (x : X) (A : R (j x)) (w : hfiber j (j x)) =>
   a w.1 (transport R (w.2)^ A)) x = a x reflexivity.
Defined.

Definition contr_univ_property_rightkanfam `{Funext} {X Y} {j : X -> Y}
  {P : X -> Type} {R : Y -> Type} (a : R o j >=> P)
  : Contr { b : R >=> P |> j & compose_mapfam (counit_rightkanfam P j) (b o j) == a}.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
Contr
  {b : R >=> P |> j &
  compose_mapfam (counit_rightkanfam P j) (b o j) == a}
Proof.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
Contr
  {b : R >=> P |> j &
  compose_mapfam (counit_rightkanfam P j) (b o j) == a}
  apply (Build_Contr _ (univ_property_rightkanfam a)).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
forall
y : {b : R >=> P |> j &
    compose_mapfam (counit_rightkanfam P j)
      (fun x : X => b (j x)) == a},
univ_property_rightkanfam a = y
  intros [b F].
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
univ_property_rightkanfam a = (b; F)
  symmetry. (* Do now to avoid inversion in the first subgoal. *)
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
(b; F) = univ_property_rightkanfam a
  srapply path_sigma.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
(b; F).1 = (univ_property_rightkanfam a).1
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
transport
  (fun b : R >=> P |> j =>
   compose_mapfam (counit_rightkanfam P j)
     (fun x : X => b (j x)) == a) ?p (b; F).2 =
(univ_property_rightkanfam a).2
  -
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
(b; F).1 = (univ_property_rightkanfam a).1 funext y.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
y: Y
(b; F).1 y = (univ_property_rightkanfam a).1 y funext C.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
y: Y
C: R y
(b; F).1 y C = (univ_property_rightkanfam a).1 y C funext [x p].
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
y: Y
C: R y
x: X
p: j x = y
(b; F).1 y C (x; p) =
(univ_property_rightkanfam a).1 y C (x; p) destruct p.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
C: R (j x)
(b; F).1 (j x) C (x; 1) =
(univ_property_rightkanfam a).1 (j x) C (x; 1) srefine (ap10 (F x) C).
  -
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
transport
  (fun b : R >=> P |> j =>
   compose_mapfam (counit_rightkanfam P j)
     (fun x : X => b (j x)) == a)
  (path_forall (b; F).1
     (univ_property_rightkanfam a).1
     ((fun y : Y =>
       path_forall ((b; F).1 y)
         ((univ_property_rightkanfam a).1 y)
         ((fun C : R y =>
           path_forall ((b; F).1 y C)
             ((univ_property_rightkanfam a).1 y C)
             ((fun x0 : hfiber j y =>
               (fun (x : X) (p : j x = y) =>
                match
                  p as p0 in (...) return (...)
                with
                | 1 => fun C0 : ... => ap10 (...) C0
                end C) x0.1 x0.2)
              :
              (b; F).1 y C ==
              (univ_property_rightkanfam a).1 y C))
          :
          (b; F).1 y ==
          (univ_property_rightkanfam a).1 y))
      :
      (b; F).1 == (univ_property_rightkanfam a).1))
  (b; F).2 = (univ_property_rightkanfam a).2 simpl.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
transport
  (fun b : R >=> P |> j =>
   compose_mapfam (counit_rightkanfam P j)
     (fun x : X => b (j x)) == a)
  (path_forall b
     (fun (y : Y) (A : R y) (w : hfiber j y) =>
      a w.1 (transport R (w.2)^ A))
     (fun y : Y =>
      path_forall (b y)
        (fun (A : R y) (w : hfiber j y) =>
         a w.1 (transport R (w.2)^ A))
        (fun C : R y =>
         path_forall (b y C)
           (fun w : hfiber j y =>
            a w.1 (transport R (w.2)^ C))
           (fun x0 : hfiber j y =>
            match
              x0.2 as p in (_ = y0)
              return
                (forall C0 : R y0,
                 b y0 C0 (x0.1; p) =
                 a x0.1 (transport R p^ C0))
            with
            | 1 =>
                fun C0 : R (j x0.1) =>
                ap10 (F x0.1) C0
            end C)))) F = (fun x : X => 1)
    funext x.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
transport
  (fun b : R >=> P |> j =>
   compose_mapfam (counit_rightkanfam P j)
     (fun x : X => b (j x)) == a)
  (path_forall b
     (fun (y : Y) (A : R y) (w : hfiber j y) =>
      a w.1 (transport R (w.2)^ A))
     (fun y : Y =>
      path_forall (b y)
        (fun (A : R y) (w : hfiber j y) =>
         a w.1 (transport R (w.2)^ A))
        (fun C : R y =>
         path_forall (b y C)
           (fun w : hfiber j y =>
            a w.1 (transport R (w.2)^ C))
           (fun x0 : hfiber j y =>
            match
              x0.2 as p in (_ = y0)
              return
                (forall C0 : R y0,
                 b y0 C0 (x0.1; p) =
                 a x0.1 (transport R p^ C0))
            with
            | 1 =>
                fun C0 : R (j x0.1) =>
                ap10 (F x0.1) C0
            end C)))) F x = 1
    lhs napply transport_forall_constant.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
transport
  (fun x0 : R >=> P |> j =>
   compose_mapfam (counit_rightkanfam P j)
     (fun x : X => x0 (j x)) x = a x)
  (path_forall b
     (fun (y : Y) (A : R y) (w : hfiber j y) =>
      a w.1 (transport R (w.2)^ A))
     (fun y : Y =>
      path_forall (b y)
        (fun (A : R y) (w : hfiber j y) =>
         a w.1 (transport R (w.2)^ A))
        (fun C : R y =>
         path_forall (b y C)
           (fun w : hfiber j y =>
            a w.1 (transport R (w.2)^ C))
           (fun x0 : hfiber j y =>
            match
              x0.2 as p in (_ = y0)
              return
                (forall C0 : R y0,
                 b y0 C0 (x0.1; p) =
                 a x0.1 (transport R p^ C0))
            with
            | 1 =>
                fun C0 : R (j x0.1) =>
                ap10 (F x0.1) C0
            end C)))) (F x) = 1
    lhs napply transport_paths_Fl.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
(ap
   (fun x0 : R >=> P |> j =>
    compose_mapfam (counit_rightkanfam P j)
      (fun x : X => x0 (j x)) x)
   (path_forall b
      (fun (y : Y) (A : R y) (w : hfiber j y) =>
       a w.1 (transport R (w.2)^ A))
      (fun y : Y =>
       path_forall (b y)
         (fun (A : R y) (w : hfiber j y) =>
          a w.1 (transport R (w.2)^ A))
         (fun C : R y =>
          path_forall (b y C)
            (fun w : hfiber j y =>
             a w.1 (transport R (w.2)^ C))
            (fun x0 : hfiber j y =>
             match
               x0.2 as p in (_ = y0)
               return
                 (forall C0 : R y0,
                  b y0 C0 (x0.1; p) =
                  a x0.1 (transport R p^ C0))
             with
             | 1 =>
                 fun C0 : R (j x0.1) =>
                 ap10 (F x0.1) C0
             end C)))))^ @ F x = 1
    apply moveR_Vp.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
F x =
ap
  (fun x0 : R >=> P |> j =>
   compose_mapfam (counit_rightkanfam P j)
     (fun x : X => x0 (j x)) x)
  (path_forall b
     (fun (y : Y) (A : R y) (w : hfiber j y) =>
      a w.1 (transport R (w.2)^ A))
     (fun y : Y =>
      path_forall (b y)
        (fun (A : R y) (w : hfiber j y) =>
         a w.1 (transport R (w.2)^ A))
        (fun C : R y =>
         path_forall (b y C)
           (fun w : hfiber j y =>
            a w.1 (transport R (w.2)^ C))
           (fun x0 : hfiber j y =>
            match
              x0.2 as p in (_ = y0)
              return
                (forall C0 : R y0,
                 b y0 C0 (x0.1; p) =
                 a x0.1 (transport R p^ C0))
            with
            | 1 =>
                fun C0 : R (j x0.1) =>
                ap10 (F x0.1) C0
            end C)))) @ 1
    symmetry.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
ap
  (fun x0 : R >=> P |> j =>
   compose_mapfam (counit_rightkanfam P j)
     (fun x : X => x0 (j x)) x)
  (path_forall b
     (fun (y : Y) (A : R y) (w : hfiber j y) =>
      a w.1 (transport R (w.2)^ A))
     (fun y : Y =>
      path_forall (b y)
        (fun (A : R y) (w : hfiber j y) =>
         a w.1 (transport R (w.2)^ A))
        (fun C : R y =>
         path_forall (b y C)
           (fun w : hfiber j y =>
            a w.1 (transport R (w.2)^ C))
           (fun x0 : hfiber j y =>
            match
              x0.2 as p in (_ = y0)
              return
                (forall C0 : R y0,
                 b y0 C0 (x0.1; p) =
                 a x0.1 (transport R p^ C0))
            with
            | 1 =>
                fun C0 : R (j x0.1) =>
                ap10 (F x0.1) C0
            end C)))) @ 1 = F x
    lhs napply concat_p1.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
ap
  (fun x0 : R >=> P |> j =>
   compose_mapfam (counit_rightkanfam P j)
     (fun x : X => x0 (j x)) x)
  (path_forall b
     (fun (y : Y) (A : R y) (w : hfiber j y) =>
      a w.1 (transport R (w.2)^ A))
     (fun y : Y =>
      path_forall (b y)
        (fun (A : R y) (w : hfiber j y) =>
         a w.1 (transport R (w.2)^ A))
        (fun C : R y =>
         path_forall (b y C)
           (fun w : hfiber j y =>
            a w.1 (transport R (w.2)^ C))
           (fun x0 : hfiber j y =>
            match
              x0.2 as p in (_ = y0)
              return
                (forall C0 : R y0,
                 b y0 C0 (x0.1; p) =
                 a x0.1 (transport R p^ C0))
            with
            | 1 =>
                fun C0 : R (j x0.1) =>
                ap10 (F x0.1) C0
            end C)))) = F x
    unfold compose_mapfam.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
ap
  (fun (x0 : R >=> P |> j) (x1 : R (j x)) =>
   counit_rightkanfam P j x (x0 (j x) x1))
  (path_forall b
     (fun (y : Y) (A : R y) (w : hfiber j y) =>
      a w.1 (transport R (w.2)^ A))
     (fun y : Y =>
      path_forall (b y)
        (fun (A : R y) (w : hfiber j y) =>
         a w.1 (transport R (w.2)^ A))
        (fun C : R y =>
         path_forall (b y C)
           (fun w : hfiber j y =>
            a w.1 (transport R (w.2)^ C))
           (fun x0 : hfiber j y =>
            match
              x0.2 as p in (_ = y0)
              return
                (forall C0 : R y0,
                 b y0 C0 (x0.1; p) =
                 a x0.1 (transport R p^ C0))
            with
            | 1 =>
                fun C0 : R (j x0.1) =>
                ap10 (F x0.1) C0
            end C)))) = F x
    lhs napply (ap_compose (fun k : R >=> (P |> j) => k (j x)) (fun ka => _ o ka)).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
ap
  (fun (ka : R (j x) -> (P |> j) (j x)) (x0 : R (j x))
   => counit_rightkanfam P j x (ka x0))
  (ap (fun k : R >=> P |> j => k (j x))
     (path_forall b
        (fun (y : Y) (A : R y) (w : hfiber j y) =>
         a w.1 (transport R (w.2)^ A))
        (fun y : Y =>
         path_forall (b y)
           (fun (A : R y) (w : hfiber j y) =>
            a w.1 (transport R (w.2)^ A))
           (fun C : R y =>
            path_forall (b y C)
              (fun w : hfiber j y =>
               a w.1 (transport R (w.2)^ C))
              (fun x0 : hfiber j y =>
               match
                 x0.2 as p in (_ = y0)
                 return
                   (forall C0 : R y0,
                    b y0 C0 (x0.1; p) =
                    a x0.1 (transport R p^ C0))
               with
               | 1 =>
                   fun C0 : R (j x0.1) =>
                   ap10 (F x0.1) C0
               end C))))) = F x
    (* [ap (fun k => k (j x))] is exactly [apD10], so it cancels the first [path_forall]. *)
    lhs nrefine (ap _ (apD10_path_forall _ _ _ _)).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
ap
  (fun (ka : R (j x) -> (P |> j) (j x)) (x0 : R (j x))
   => counit_rightkanfam P j x (ka x0))
  (path_forall (b (j x))
     (fun (A : R (j x)) (w : hfiber j (j x)) =>
      a w.1 (transport R (w.2)^ A))
     (fun C : R (j x) =>
      path_forall (b (j x) C)
        (fun w : hfiber j (j x) =>
         a w.1 (transport R (w.2)^ C))
        (fun x0 : hfiber j (j x) =>
         match
           x0.2 as p in (_ = y)
           return
             (forall C0 : R y,
              b y C0 (x0.1; p) =
              a x0.1 (transport R p^ C0))
         with
         | 1 =>
             fun C0 : R (j x0.1) => ap10 (F x0.1) C0
         end C))) = F x
    lhs napply ap_postcompose.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
path_arrow
  (fun x0 : R (j x) =>
   counit_rightkanfam P j x (b (j x) x0))
  (fun x0 : R (j x) =>
   counit_rightkanfam P j x
     (fun w : hfiber j (j x) =>
      a w.1 (transport R (w.2)^ x0)))
  (fun q : R (j x) =>
   ap (counit_rightkanfam P j x)
     (ap10
        (path_forall (b (j x))
           (fun (A : R (j x)) (w : hfiber j (j x)) =>
            a w.1 (transport R (w.2)^ A))
           (fun C : R (j x) =>
            path_forall (b (j x) C)
              (fun w : hfiber j (j x) =>
               a w.1 (transport R (w.2)^ C))
              (fun x0 : hfiber j (j x) =>
               match
                 x0.2 as p in (_ = y)
                 return
                   (forall C0 : R y,
                    b y C0 (x0.1; p) =
                    a x0.1 (transport R p^ C0))
               with
               | 1 =>
                   fun C0 : R (j x0.1) =>
                   ap10 (F x0.1) C0
               end C))) q)) = F x
    unfold path_forall, ap10.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
path_arrow
  (fun x0 : R (j x) =>
   counit_rightkanfam P j x (b (j x) x0))
  (fun x0 : R (j x) =>
   counit_rightkanfam P j x
     (fun w : hfiber j (j x) =>
      a w.1 (transport R (w.2)^ x0)))
  (fun q : R (j x) =>
   ap (counit_rightkanfam P j x)
     (apD10
        (apD10^-1
           (fun C : R (j x) =>
            apD10^-1
              (fun x0 : hfiber j (j x) =>
               match
                 x0.2 as p in (_ = y)
                 return
                   (forall C0 : R y,
                    b y C0 (x0.1; p) =
                    a x0.1 (transport R p^ C0))
               with
               | 1 =>
                   fun C0 : R (j x0.1) =>
                   apD10 (F x0.1) C0
               end C))) q)) = F x
    rewrite (eisretr apD10).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
path_arrow
  (fun x0 : R (j x) =>
   counit_rightkanfam P j x (b (j x) x0))
  (fun x0 : R (j x) =>
   counit_rightkanfam P j x
     (fun w : hfiber j (j x) =>
      a w.1 (transport R (w.2)^ x0)))
  (fun q : R (j x) =>
   ap (counit_rightkanfam P j x)
     (apD10^-1
        (fun x0 : hfiber j (j x) =>
         match
           x0.2 as p in (_ = y)
           return
             (forall C : R y,
              b y C (x0.1; p) =
              a x0.1 (transport R p^ C))
         with
         | 1 => fun C : R (j x0.1) => apD10 (F x0.1) C
         end q))) = F x
    change (ap _ ?p) with (apD10 p (x; 1)).
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
path_arrow
  (fun x0 : R (j x) =>
   counit_rightkanfam P j x (b (j x) x0))
  (fun x0 : R (j x) =>
   counit_rightkanfam P j x
     (fun w : hfiber j (j x) =>
      a w.1 (transport R (w.2)^ x0)))
  (fun q : R (j x) =>
   apD10
     (apD10^-1
        (fun x0 : hfiber j (j x) =>
         match
           x0.2 as p in (_ = y)
           return
             (forall C : R y,
              b y C (x0.1; p) =
              a x0.1 (transport R p^ C))
         with
         | 1 => fun C : R (j x0.1) => apD10 (F x0.1) C
         end q)) (x; 1)) = F x
    napply moveR_equiv_V.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
(fun q : R (j x) =>
 apD10
   (apD10^-1
      (fun x0 : hfiber j (j x) =>
       match
         x0.2 as p in (_ = y)
         return
           (forall C : R y,
            b y C (x0.1; p) =
            a x0.1 (transport R p^ C))
       with
       | 1 => fun C : R (j x0.1) => apD10 (F x0.1) C
       end q)) (x; 1)) = apD10 (F x)
    funext r.
H: Funext
X, Y: Type
j: X -> Y
P: X -> Type
R: Y -> Type
a: R o j >=> P
b: R >=> P |> j
F: compose_mapfam (counit_rightkanfam P j)
  (fun x : X => b (j x)) == a
x: X
r: R (j x)
apD10
  (apD10^-1
     (fun x0 : hfiber j (j x) =>
      match
        x0.2 as p in (_ = y)
        return
          (forall C : R y,
           b y C (x0.1; p) = a x0.1 (transport R p^ C))
      with
      | 1 => fun C : R (j x0.1) => apD10 (F x0.1) C
      end r)) (x; 1) = apD10 (F x) r
    exact (apD10_path_forall _ _ _ (x; _)).
Defined.

(** The above (co)unit constructions are special cases of the following, which tells us that these extensions are adjoint to restriction by [j] *)
Definition leftadjoint_leftkanfam `{Funext} {X Y : Type} (P : X -> Type)
  (R : Y -> Type) (j : X -> Y)
  : ((P <| j) >=> R) <~> (P >=> R o j).
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
P <| j >=> R <~> P >=> R o j
Proof.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
P <| j >=> R <~> P >=> R o j
  snapply equiv_adjointify.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
P <| j >=> R -> P >=> R o j
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
P >=> R o j -> P <| j >=> R
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
?f o ?g == idmap
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
?g o ?f == idmap
  -
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
P <| j >=> R -> P >=> R o j intros a x B.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
a: P <| j >=> R
x: X
B: P x
R (j x) exact (a (j x) ((x; idpath); B)).
  -
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
P >=> R o j -> P <| j >=> R intros b y [[x p] C].
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
b: P >=> R o j
y: Y
x: X
p: j x = y
C: P (x; p).1
R y exact (p # (b x C)).
  -
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
(fun a : P <| j >=> R =>
 (fun (x : X) (B : P x) => a (j x) ((x; 1); B))
 :
 P >=> R o j)
o (fun b : P >=> R o j =>
   (fun (y : Y) (X0 : (P <| j) y) =>
    (fun proj1 : hfiber j y =>
     (fun (x : X) (p : j x = y) (C : P (x; p).1) =>
      transport R p (b x C)) proj1.1 proj1.2) X0.1
      X0.2)
   :
   P <| j >=> R) == idmap intros b.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
b: P >=> (fun x : X => R (j x))
(fun (x : X) (B : P x) => transport R 1 (b x B)) = b by funext x C.
  -
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
(fun b : P >=> R o j =>
 (fun (y : Y) (X0 : (P <| j) y) =>
  (fun proj1 : hfiber j y =>
   (fun (x : X) (p : j x = y) (C : P (x; p).1) =>
    transport R p (b x C)) proj1.1 proj1.2) X0.1 X0.2)
 :
 P <| j >=> R)
o (fun a : P <| j >=> R =>
   (fun (x : X) (B : P x) => a (j x) ((x; 1); B))
   :
   P >=> R o j) == idmap intros a.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
a: P <| j >=> R
(fun (y : Y) (X0 : (P <| j) y) =>
 transport R (X0.1).2
   (a (j (X0.1).1) (((X0.1).1; 1); X0.2))) = a by funext y [[x []] C].
Defined.

Definition rightadjoint_rightkanfam `{Funext} {X Y : Type} (P : X -> Type)
  (R : Y -> Type) (j : X -> Y)
  : (R >=> (P |> j)) <~> (R o j >=> P).
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
R >=> P |> j <~> R o j >=> P
Proof.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
R >=> P |> j <~> R o j >=> P
  snapply equiv_adjointify.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
R >=> P |> j -> R o j >=> P
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
R o j >=> P -> R >=> P |> j
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
?f o ?g == idmap
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
?g o ?f == idmap
  -
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
R >=> P |> j -> R o j >=> P intros a x C.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
a: R >=> P |> j
x: X
C: R (j x)
P x exact (a (j x) C (x; idpath)).
  -
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
R o j >=> P -> R >=> P |> j intros a y C [x p].
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
a: R o j >=> P
y: Y
C: R y
x: X
p: j x = y
P (x; p).1 apply (a x).
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
a: R o j >=> P
y: Y
C: R y
x: X
p: j x = y
R (j x) exact (p^ # C).
  -
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
(fun a : R >=> P |> j =>
 (fun (x : X) (C : R (j x)) => a (j x) C (x; 1))
 :
 R o j >=> P)
o (fun a : R o j >=> P =>
   (fun (y : Y) (C : R y) =>
    (fun w : hfiber j y =>
     (fun (x : X) (p : j x = y) =>
      a x (transport R p^ C)) w.1 w.2)
    :
    (P |> j) y)
   :
   R >=> P |> j) == idmap intros a.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
a: (fun x : X => R (j x)) >=> P
(fun (x : X) (C : R (j x)) => a x (transport R 1^ C)) =
a by funext x C.
  -
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
(fun a : R o j >=> P =>
 (fun (y : Y) (C : R y) =>
  (fun w : hfiber j y =>
   (fun (x : X) (p : j x = y) =>
    a x (transport R p^ C)) w.1 w.2)
  :
  (P |> j) y)
 :
 R >=> P |> j)
o (fun a : R >=> P |> j =>
   (fun (x : X) (C : R (j x)) => a (j x) C (x; 1))
   :
   R o j >=> P) == idmap intros b.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
b: R >=> P |> j
(fun (y : Y) (C : R y) (w : hfiber j y) =>
 b (j w.1) (transport R (w.2)^ C) (w.1; 1)) = b funext y C [x p].
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
b: R >=> P |> j
y: Y
C: R y
x: X
p: j x = y
b (j x) (transport R p^ C) (x; 1) = b y C (x; p) destruct p; cbn.
H: Funext
X, Y: Type
P: X -> Type
R: Y -> Type
j: X -> Y
b: R >=> P |> j
x: X
C: R (j x)
b (j x) C (x; 1) = b (j x) C (x; 1) reflexivity.
Defined.

(** This section is all set up for the proof that the left Kan extension of an embedding is an embedding of type families. *)
Section EmbedProofLeft.
  Context `{Univalence} {X Y : Type} (j : X -> Y) (isem : IsEmbedding j).

  (** The counit transformation of a type family of the form [P <| j] has each of its components an equivalence.  In other words, the type family [P <| j] is the left Kan extension of its restriction along [j]. *)
  Definition isequiv_counit_leftkanfam_leftkanfam (P : X -> Type) {y : Y}
    : IsEquiv (counit_leftkanfam (P <| j) j y).
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
IsEquiv (counit_leftkanfam (P <| j) j y)
  Proof.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
IsEquiv (counit_leftkanfam (P <| j) j y)
    snapply isequiv_adjointify.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
(P <| j) y -> ((P <| j o j) <| j) y
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
counit_leftkanfam (P <| j) j y o ?g == idmap
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
?g o counit_leftkanfam (P <| j) j y == idmap
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
(P <| j) y -> ((P <| j o j) <| j) y exact (fun '(((x; p); C) : (P <| j) y) => ((x; p); ((x; idpath); C))).
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
counit_leftkanfam (P <| j) j y
o (fun pat : (P <| j) y =>
   let x := pat in
   let proj1 := x.1 in
   let C := x.2 in
   (let proj2 := proj1 in
    let x0 := proj2.1 in
    let p := proj2.2 in
    fun C0 : P (x0; p).1 => ((x0; p); (x0; 1); C0)) C) ==
idmap by intros [[x []] C].
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
(fun pat : (P <| j) y =>
 let x := pat in
 let proj1 := x.1 in
 let C := x.2 in
 (let proj2 := proj1 in
  let x0 := proj2.1 in
  let p := proj2.2 in
  fun C0 : P (x0; p).1 => ((x0; p); (x0; 1); C0)) C)
o counit_leftkanfam (P <| j) j y == idmap intros [[x []] [[x' p'] C]]; cbn; cbn in C, p'.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
x, x': X
p': j x' = j x
C: P x'
((x'; p'); (x'; 1); C) = ((x; 1); (x'; p'); C)
      revert p'; apply (equiv_ind (ap j)).
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
x, x': X
C: P x'
forall x0 : x' = x,
((x'; ap j x0); (x'; 1); C) =
((x; 1); (x'; ap j x0); C)
      by intros [].
  Defined.

  (** We now use the above fact to show that type families over [X] are equivalent to type families over [Y] such that the counit map is a natural isomorphism. *)
  Definition leftkanfam_counit_equiv (P : X -> Type)
    : { R : Y -> Type & forall y, IsEquiv (counit_leftkanfam R j y) }.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
{R : Y -> Type &
forall y : Y, IsEquiv (counit_leftkanfam R j y)}
  Proof.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
{R : Y -> Type &
forall y : Y, IsEquiv (counit_leftkanfam R j y)}
    exists (P <| j).
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
forall y : Y, IsEquiv (counit_leftkanfam (P <| j) j y)
    rapply isequiv_counit_leftkanfam_leftkanfam.
  Defined.

  #[export] Instance isequiv_leftkanfam_counit_equiv
    : IsEquiv leftkanfam_counit_equiv.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
IsEquiv leftkanfam_counit_equiv
  Proof.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
IsEquiv leftkanfam_counit_equiv
    snapply isequiv_adjointify.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
{R : Y -> Type &
forall y : Y, IsEquiv (counit_leftkanfam R j y)} ->
X -> Type
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
leftkanfam_counit_equiv o ?g == idmap
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
?g o leftkanfam_counit_equiv == idmap
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
{R : Y -> Type &
forall y : Y, IsEquiv (counit_leftkanfam R j y)} ->
X -> Type intros [R e].
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
R: Y -> Type
e: forall y : Y, IsEquiv (counit_leftkanfam R j y)
X -> Type exact (R o j).
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
leftkanfam_counit_equiv
o (fun
     X0 : {R : Y -> Type &
          forall y : Y,
          IsEquiv (counit_leftkanfam R j y)} =>
   (fun (R : Y -> Type)
      (_ : forall y : Y,
           IsEquiv (counit_leftkanfam R j y)) => R o j)
     X0.1 X0.2) == idmap intros [R e].
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
R: Y -> Type
e: forall y : Y, IsEquiv (counit_leftkanfam R j y)
leftkanfam_counit_equiv (fun x : X => R (j x)) =
(R; e) srapply path_sigma_hprop; cbn.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
R: Y -> Type
e: forall y : Y, IsEquiv (counit_leftkanfam R j y)
(fun x : X => R (j x)) <| j = R
      funext y.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
R: Y -> Type
e: forall y : Y, IsEquiv (counit_leftkanfam R j y)
y: Y
((fun x : X => R (j x)) <| j) y = R y
      exact (path_universe _ (feq:=e y)).
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
(fun
   X0 : {R : Y -> Type &
        forall y : Y,
        IsEquiv (counit_leftkanfam R j y)} =>
 (fun (R : Y -> Type)
    (_ : forall y : Y,
         IsEquiv (counit_leftkanfam R j y)) => R o j)
   X0.1 X0.2) o leftkanfam_counit_equiv == idmap intros P.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
(fun x : X => (leftkanfam_counit_equiv P).1 (j x)) = P
      funext x.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
x: X
(leftkanfam_counit_equiv P).1 (j x) = P x
      rapply isext_leftkanfam.
  Defined.

  (** Using these facts we can show that the map [_ <| j] is an embedding if [j] is an embedding. *)
  Definition isembed_leftkanfam_ext
    : IsEmbedding (fun P => P <| j)
    := mapinO_compose (O:=-1) leftkanfam_counit_equiv pr1.

End EmbedProofLeft.

(** Dual proof for the right Kan extension. *)
Section EmbedProofRight.
  Context `{Univalence} {X Y : Type} (j : X -> Y) (isem : IsEmbedding j).

  Definition isequiv_unit_rightkanfam_rightkanfam (P : X -> Type) {y : Y}
    : IsEquiv (unit_rightkanfam (P |> j) j y).
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
IsEquiv (unit_rightkanfam (P |> j) j y)
  Proof.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
IsEquiv (unit_rightkanfam (P |> j) j y)
    snapply isequiv_adjointify.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
((P |> j o j) |> j) y -> (P |> j) y
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
unit_rightkanfam (P |> j) j y o ?g == idmap
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
?g o unit_rightkanfam (P |> j) j y == idmap
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
((P |> j o j) |> j) y -> (P |> j) y intros C [x p].
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
C: ((P |> j o j) |> j) y
x: X
p: j x = y
P (x; p).1 exact (C (x; p) (x; idpath)).
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
unit_rightkanfam (P |> j) j y
o (fun C : ((P |> j o j) |> j) y =>
   (fun w : hfiber j y =>
    (fun (x : X) (p : j x = y) => C (x; p) (x; 1)) w.1
      w.2)
   :
   (P |> j) y) == idmap intros C.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
C: ((fun x : X => (P |> j) (j x)) |> j) y
unit_rightkanfam (P |> j) j y
  (fun w : hfiber j y => C (w.1; w.2) (w.1; 1)) = C funext [x p].
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
C: ((fun x : X => (P |> j) (j x)) |> j) y
x: X
p: j x = y
unit_rightkanfam (P |> j) j y
  (fun w : hfiber j y => C (w.1; w.2) (w.1; 1)) (x; p) =
C (x; p) destruct p.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
x: X
C: ((fun x : X => (P |> j) (j x)) |> j) (j x)
unit_rightkanfam (P |> j) j (j x)
  (fun w : hfiber j (j x) => C (w.1; w.2) (w.1; 1))
  (x; 1) = C (x; 1) funext w.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
x: X
C: ((fun x : X => (P |> j) (j x)) |> j) (j x)
w: hfiber j (j (x; 1).1)
unit_rightkanfam (P |> j) j (j x)
  (fun w : hfiber j (j x) => C (w.1; w.2) (w.1; 1))
  (x; 1) w = C (x; 1) w
      rapply (@transport _ (fun t => C t (t.1; idpath) = C (x; idpath) t) _ w
        (center _ (isem (j x) (x; idpath) w)) idpath).
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
(fun C : ((P |> j o j) |> j) y =>
 (fun w : hfiber j y =>
  (fun (x : X) (p : j x = y) => C (x; p) (x; 1)) w.1
    w.2)
 :
 (P |> j) y) o unit_rightkanfam (P |> j) j y == idmap intros a.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
a: (P |> j) y
(fun w : hfiber j y =>
 unit_rightkanfam (P |> j) j y a (w.1; w.2) (w.1; 1)) =
a funext [x p].
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
y: Y
a: (P |> j) y
x: X
p: j x = y
unit_rightkanfam (P |> j) j y a (x; p) (x; 1) =
a (x; p) destruct p.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
x: X
a: (P |> j) (j x)
unit_rightkanfam (P |> j) j (j x) a (x; 1) (x; 1) =
a (x; 1)
      reflexivity.
  Defined.

  Definition rightkanfam_unit_equiv (P : X -> Type)
    : {R : Y -> Type & forall y, IsEquiv (unit_rightkanfam R j y)}.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
{R : Y -> Type &
forall y : Y, IsEquiv (unit_rightkanfam R j y)}
  Proof.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
{R : Y -> Type &
forall y : Y, IsEquiv (unit_rightkanfam R j y)}
    exists (P |> j).
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
forall y : Y, IsEquiv (unit_rightkanfam (P |> j) j y)
    rapply isequiv_unit_rightkanfam_rightkanfam.
  Defined.

  #[export] Instance isequiv_rightkanfam_unit_equiv
    : IsEquiv rightkanfam_unit_equiv.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
IsEquiv rightkanfam_unit_equiv
  Proof.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
IsEquiv rightkanfam_unit_equiv
    snapply isequiv_adjointify.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
{R : Y -> Type &
forall y : Y, IsEquiv (unit_rightkanfam R j y)} ->
X -> Type
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
rightkanfam_unit_equiv o ?g == idmap
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
?g o rightkanfam_unit_equiv == idmap
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
{R : Y -> Type &
forall y : Y, IsEquiv (unit_rightkanfam R j y)} ->
X -> Type intros [R e].
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
R: Y -> Type
e: forall y : Y, IsEquiv (unit_rightkanfam R j y)
X -> Type exact (R o j).
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
rightkanfam_unit_equiv
o (fun
     X0 : {R : Y -> Type &
          forall y : Y,
          IsEquiv (unit_rightkanfam R j y)} =>
   (fun (R : Y -> Type)
      (_ : forall y : Y,
           IsEquiv (unit_rightkanfam R j y)) => R o j)
     X0.1 X0.2) == idmap intros [R e].
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
R: Y -> Type
e: forall y : Y, IsEquiv (unit_rightkanfam R j y)
rightkanfam_unit_equiv (fun x : X => R (j x)) = (R; e) srapply path_sigma_hprop; cbn.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
R: Y -> Type
e: forall y : Y, IsEquiv (unit_rightkanfam R j y)
(fun x : X => R (j x)) |> j = R
      funext y.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
R: Y -> Type
e: forall y : Y, IsEquiv (unit_rightkanfam R j y)
y: Y
((fun x : X => R (j x)) |> j) y = R y
      symmetry; exact (path_universe _ (feq:=e y)).
    -
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
(fun
   X0 : {R : Y -> Type &
        forall y : Y, IsEquiv (unit_rightkanfam R j y)}
 =>
 (fun (R : Y -> Type)
    (_ : forall y : Y,
         IsEquiv (unit_rightkanfam R j y)) => R o j)
   X0.1 X0.2) o rightkanfam_unit_equiv == idmap intros P.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
(fun x : X => (rightkanfam_unit_equiv P).1 (j x)) = P
      funext x.
H: Univalence
X, Y: Type
j: X -> Y
isem: IsEmbedding j
P: X -> Type
x: X
(rightkanfam_unit_equiv P).1 (j x) = P x
      rapply isext_rightkanfam.
  Defined.

  (** The map [_ |> j] is an embedding if [j] is an embedding. *)
  Definition isembed_rightkanfam_ext
    : IsEmbedding (fun P => P |> j)
    := mapinO_compose (O:=-1) rightkanfam_unit_equiv pr1.

End EmbedProofRight.