(** * Kan Extensions *)
Require Import Category.Core Functor.Core.
Require Import FunctorCategory.Core.
Require Import Functor.Composition.Functorial.Core.
Require Import UniversalProperties.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope category_scope.

(** Quoting nLab on Kan extensions:

    ** Idea

    The Kan extension of a functor [F : C → D] with respect to a
    functor

<<
    C
    |
    | p
    ↓
    C'
>>

    is, if it exists, a kind of best approximation to the problem of
    finding a functor [C' → D] such that

<<
        F
    C -----> D
    |       ↗
    | p   /
    |   /
    ↓ /
    C'
>>

    hence to extending the domain of [F] through [p] from [C] to [C'].

    More generally, this makes sense not only in Cat but in any
    2-category.

    Similarly, a Kan lift is the best approximation to lifting a
    morphism [F : C → D] through a morphism

<<
    D'
    |
    ↓
    D
>>

    to a morphism [F̂]

<<
                D'
              ↗ |
            /   |
        F̂ /     |
        /       |
      /   F     ↓
    C --------> D
>>

    Kan extensions are ubiquitous. See the discussion at Examples
    below.

    ** Definitions

    There are various slight variants of the definition of Kan
    extension. In good cases they all exist and all coincide, but in
    some cases only some of these will actually exist.

    We (have to) distinguish the following cases:

    - “ordinary” or “weak” Kan extensions

      These define the extension of an entire functor, by an
      adjointness relation.

      Here we (have to) distinguish further between

      - global Kan extensions,

        which define extensions of all possible functors of given
        domain and codomain (if all of them indeed exist);

      - local Kan extensions,

        which define extensions of single functors only, which may
        exist even if not every functor has an extension.

    - “pointwise” or “strong” Kan extensions

      These define the value of an extended functor on each object
      (each “point”) by a weighted (co)limit.

      Furthermore, a pointwise Kan extension can be “absolute”.

    If the pointwise version exists, then it coincides with the
    “ordinary” or “weak” version, but the former may exist without the
    pointwise version existing. See below for more.

    Some authors (such as Kelly) assert that only pointwise Kan
    extensions deserve the name “Kan extension,” and use the term as
    “weak Kan extension” for a functor equipped with a universal
    natural transformation. It is certainly true that most Kan
    extensions which arise in practice are pointwise. This distinction
    is even more important in enriched category theory. *)

Section kan_extensions.
  (** ** Ordinary or weak Kan extensions

      *** Global Kan extensions

      Let [p : C → C'] be a functor. For [D] any other category, write
      [p* : (C' → D) → (C → D)] for the induced functor on the functor
      categories: this sends a functor [h : C' → D] to the composite functor

<<
                p      h
      p* h : C --> C' --> D
>>
   *)
  (** *** Pullback-along functor *)
  Context `{Funext}.
  Variables C C' D : PreCategory.

  Section pullback_along.
    Definition pullback_along_functor
    : object ((C -> C') -> (C' -> D) -> (C -> D))
      := Functor.Composition.Functorial.Core.compose_functor _ _ _.

    Definition pullback_along (p : Functor C C')
    : object ((C' -> D) -> (C -> D))
      := Eval hnf in pullback_along_functor p.
  End pullback_along.

  (** Definition. If [p*] has a left adjoint, typically denoted [p_! :
      (C → D) → (C' → D)] or [Lan_p : (C → D) → (C' → D)] then this
      left adjoint is called the (ordinary or weak) left Kan extension
      operation along [p]. For [h ∈ (C -> D)] we call [p_! h] the left
      Kan extension of [h] along [p].

      Similarly, if [p*] has a right adjoint, this right adjoint is
      called the right Kan extension operation along [p]. It is
      typically denoted [p_* : (C → D) → (C' → D)] or [Ran = Ran_p :
      (C → D) → (C' → D)].

      The analogous definition clearly makes sense as stated in other
      contexts, such as in enriched category theory.

      Observation. If [C' = 1] is the terminal category, then

      - the left Kan extension operation forms the colimit of a functor;

      - the right Kan extension operation forms the limit of a functor. *)

  (** *** Left Kan extensions *)
  (** Colimits are initial morphisms. *)
  Definition IsLeftKanExtensionAlong (p : Functor C C') (h : Functor C D)
    := @IsInitialMorphism (_ -> _) _ h (pullback_along p).

  (** *** Right Kan extensions *)
  (** Limits are terminal morphisms *)
  Definition IsRightKanExtensionAlong (p : Functor C C') (h : Functor C D)
    := @IsTerminalMorphism _ (_ -> _) (pullback_along p) h.
End kan_extensions.