Lan.agda

module Lan where

open import Categories.Kan
open import Data.Product
open import Level
open import Function renaming (id to funId)
open import Categories.Functor
open import Categories.Category.Instance.Sets
open Functor
open import Relation.Binary.PropositionalEquality
open import Axiom.Extensionality.Propositional
postulate
  funext : ∀{a}{b} → Extensionality a b
  funextImpl : ∀{a}{b} → ExtensionalityImplicit a b

-- extending H along G
LeftKan : {a b c d : _} (along : Set a → Set b) (of : Set a → Set c) (A : Set d) → Set (suc a ⊔ b ⊔ c ⊔ d)
LeftKan along of A = Σ _ λ B → of B × (along B → A)

LeftKan-fmap : {a b c d e : _} {G : Set a → Set b} {H : Set a → Set c} {A : Set d} {B : Set e} → (A → B) → LeftKan G H A → LeftKan G H B
LeftKan-fmap f (fst , snd , thr) = fst , snd , f ∘ thr

LeftKan-fmap-id : {a b c d : _} {G : Set a → Set b} {H : Set a → Set c} {A : Set d} {x : LeftKan G H A} → LeftKan-fmap funId x ≡ x
LeftKan-fmap-id = refl

LeftKan-fmap-∘ : {a b c d e z : _} {G : Set a → Set b} {H : Set a → Set c} {A : Set d}{B : Set e}{C : Set z}
  → {f : A → B} {g : B → C} {x : LeftKan G H A}
  → LeftKan-fmap (g ∘ f) x ≡ LeftKan-fmap g (LeftKan-fmap f x)
LeftKan-fmap-∘ = refl

open import Data.Product.Properties

LeftKan-Functor : {a b c d : _} (G : Set a → Set b) (H : Set a → Set c) → Functor (Sets d) (Sets (suc a ⊔ b ⊔ c ⊔ d))
F₀ (LeftKan-Functor G H) = LeftKan G H
F₁ (LeftKan-Functor G H) = LeftKan-fmap
identity (LeftKan-Functor G H) = LeftKan-fmap-id
homomorphism (LeftKan-Functor G H) {f = f} {g = g} = LeftKan-fmap-∘ {f = f} {g = g}
F-resp-≈ (LeftKan-Functor G H) y {x} = Σ-≡,≡→≡ (refl , (Σ-≡,≡→≡ (refl , (funext (λ z → y)))))

lift-Sets : {a b : _} → Functor (Sets a) (Sets (a ⊔ b))
F₀ (lift-Sets {b = b}) = Lift b
F₁ lift-Sets f x = lift (f (lower x))
identity lift-Sets = refl
homomorphism lift-Sets = refl
F-resp-≈ lift-Sets eq = cong lift eq

open Lan
open import Categories.NaturalTransformation
module _ {a b c : _}
  (G : Functor (Sets a) (Sets b)) (H : Functor (Sets a) (Sets c)) where

  Lan-LeftKan : Lan G (lift-Sets {b = suc a ⊔ b} ∘F H)
  L Lan-LeftKan = LeftKan-Functor (F₀ G) (F₀ H)
  η Lan-LeftKan = ntHelper (record
    { η = λ X (lift x) → X , x , λ y → y
    ; commute = λ f {(lift x)} → {! needs cowedge !}
    })
  σ Lan-LeftKan M α = ntHelper (record
    { η = λ X (B , x , f) → M .F₁ f (α .NaturalTransformation.η _ (lift x))
    ; commute = λ _ → M .homomorphism
    })
  commutes Lan-LeftKan M α = sym (M .identity)
  σ-unique Lan-LeftKan {M} {α} σ' comm = {! needs cowedge (i think) !}