TypeFamKanExt.v

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

From HoTT Require Import Basics.

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).

    exact (@equiv_contr_sigma (hfiber j (j x)) _ _).


  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).

    exact (@equiv_contr_forall _ (hfiber j (j x)) _ _).


  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).

  snapply contr_forall.

  apply (Empty_rec (ynin x p)).


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

  snapply equiv_adjointify.

 exact (fun w : {x : X & P x} => (j w.1; (w.1; idpath); w.2)).

 exact (fun '((y; ((x; p); y')) : {y : Y & (P <| j) y}) => (x; y')).

 by intros [y [[x []] y']].


Definition equiv_rightkanfam `{Funext} {X : Type} {Y : Type}
  (P : X -> Type@{w}) (j : X -> Y)
  : (forall x, P x) <~> (forall y, (P |> j) y).

  snapply equiv_adjointify.

 exact (fun h x => h (j x) (x; idpath)).

 by apply path_forall.


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

  snapply (transport (fun a => P a.1) _ z).

  srapply path_ishprop.


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

  exact (transport R p C).


Definition unit_rightkanfam {X Y : Type} (R : Y -> Type) (j : X -> Y)
  : R >=> ((R o j) |> j).

  exact (transport R p^ C).


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


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}.

  apply (Build_Contr _ (univ_property_leftkanfam a)).

 (* Do now to avoid inversion in the first subgoal. *)

 srefine (ap10 (F w) c).

    lhs napply transport_forall_constant.

    lhs napply transport_paths_Fl.

    rhs napply concat_p1.

    unfold compose_mapfam, unit_leftkanfam.

    pose (i := fun px: P x => ((x; 1); px) : (P <| j) (j x)).

    lhs napply (ap_compose (fun k : (P <| j) >=> R => k (j x)) (fun ka => ka o i)).

    (* [ap (fun k => k (j x))] is exactly [apD10], so it cancels the first [path_forall]. *)

lhs nrefine (ap _ (apD10_path_forall _ _ _ _)).

    lhs rapply (ap_precompose _ i).

    unfold path_forall, ap10.

    rewrite (eisretr apD10); cbn.


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}.

 exact (a x (p^ # A)).


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}.

  apply (Build_Contr _ (univ_property_rightkanfam a)).

 (* Do now to avoid inversion in the first subgoal. *)

 srefine (ap10 (F x) C).

    lhs napply transport_forall_constant.

    lhs napply transport_paths_Fl.

    lhs napply concat_p1.

    unfold compose_mapfam.

    lhs napply (ap_compose (fun k : R >=> (P |> j) => k (j x)) (fun ka => _ o ka)).

    (* [ap (fun k => k (j x))] is exactly [apD10], so it cancels the first [path_forall]. *)

lhs nrefine (ap _ (apD10_path_forall _ _ _ _)).

    lhs napply ap_postcompose.

    unfold path_forall, ap10.

    rewrite (eisretr apD10).

    change (ap _ ?p) with (apD10 p (x; 1)).

    napply moveR_equiv_V.

    exact (apD10_path_forall _ _ _ (x; _)).


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

  snapply equiv_adjointify.

 exact (a (j x) ((x; idpath); B)).

 intros b y [[x p] C].

 exact (p # (b x C)).

 by funext y [[x []] C].


Definition rightadjoint_rightkanfam `{Funext} {X Y : Type} (P : X -> Type)
  (R : Y -> Type) (j : X -> Y)
  : (R >=> (P |> j)) <~> (R o j >=> P).

  snapply equiv_adjointify.

 exact (a (j x) C (x; idpath)).


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

    snapply isequiv_adjointify.

 exact (fun '(((x; p); C) : (P <| j) y) => ((x; p); ((x; idpath); C))).

 by intros [[x []] C].

 intros [[x []] [[x' p'] C]]; cbn; cbn in C, p'.

      revert p'; apply (equiv_ind (ap j)).


  (** 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) }.

    rapply isequiv_counit_leftkanfam_leftkanfam.


  #[export] Instance isequiv_leftkanfam_counit_equiv
    : IsEquiv leftkanfam_counit_equiv.

    snapply isequiv_adjointify.

 srapply path_sigma_hprop; cbn.

      exact (path_universe _ (feq:=e y)).

      rapply isext_leftkanfam.


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


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

    snapply isequiv_adjointify.

 exact (C (x; p) (x; idpath)).

      rapply (@transport _ (fun t => C t (t.1; idpath) = C (x; idpath) t) _ w
        (center _ (isem (j x) (x; idpath) w)) idpath).


  Definition rightkanfam_unit_equiv (P : X -> Type)
    : {R : Y -> Type & forall y, IsEquiv (unit_rightkanfam R j y)}.

    rapply isequiv_unit_rightkanfam_rightkanfam.

      
  #[export] Instance isequiv_rightkanfam_unit_equiv
    : IsEquiv rightkanfam_unit_equiv.

    snapply isequiv_adjointify.

 srapply path_sigma_hprop; cbn.

      symmetry; exact (path_universe _ (feq:=e y)).

      rapply isext_rightkanfam.


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

Timings for TypeFamKanExt.v