module Free where
open import Data.Unit hiding (unit)
open import Relation.Binary.PropositionalEquality
open import Data.Product hiding (map)
open import Function hiding (_$_)

_>>_ : ∀ {I} (X Y : I → Set) → Set
X >> Y = ∀ {i} → X i → Y i

-- Functor {I} _⇒_ X is the action of morphisms of X as functor from I to Set
Functor : {I : Set} (_⇒_ : I → I → Set) → (I → Set) → Set
Functor _⇒_ X = ∀ {i j} → i ⇒ j → X i → X j

record IC (I O : Set) : Set₁ where
  constructor ic
  field
    S : O → Set
    P : ∀ {o} → S o → Set
    r : ∀ {o s} → P {o} s → I
open IC

⟦_⟧ : ∀ {I O} → IC I O → (I → Set) → O → Set
⟦ ic S P r ⟧ X o = Σ (S o) \ s → ∀ (p : P s) → X (r p)


data Free {I} (F : IC I I) (X : I → Set) (i : I) : Set where
  η : X i → Free F X i
  <_> : ⟦ F ⟧ (Free F X) i → Free F X i

bind : ∀ {I F X Y} → X >> Free {I} F Y → Free F X >> Free F Y
bind f (η x)       = f x
bind f < (s , t) > = < (s , λ p → bind f (t p)) >

module FunctorFree {I : Set} (_⇒_ : I → I → Set)  where

  FunctorIC : IC I I → Set
  FunctorIC (ic S P r) = ∀ {i j} → i ⇒ j → (si : S i) → Σ (S j) \ sj → ∀ (pj : P sj) → Σ (P si) \ pi → r pi ⇒ r pj 
  
  mapIC : ∀ (F : IC I I) -> FunctorIC F -> ∀ {X} -> Functor _⇒_ X -> Functor _⇒_ (⟦ F ⟧ X)
  mapIC F mapF mapX f (s , t) = proj₁ (mapF f s) , 
                                (λ fp → let x = proj₂ (mapF f s) fp in
                                        mapX (proj₂ x) (t (proj₁ x)))

  mapFree : ∀ {F X} → FunctorIC F → Functor _⇒_ X → Functor _⇒_ (Free F X)
  mapFree mapF mapX f (η x)        = η (mapX f x)
  mapFree mapF mapX f < (s , ts) > = < (proj₁ (mapF f s) , 
                                       (λ fp → let x = proj₂ (mapF f s) fp in 
                                               mapFree mapF mapX (proj₂ x) (ts (proj₁ x)))) >


module ContravariantYoneda {I : Set} (_⇒_ : I → I → Set) (_∘_ : ∀ {i j k} → (j ⇒ k) → (i ⇒ j) → i ⇒ k)  where
  record Yoneda (F : I → Set) (i : I) : Set where
    constructor _/_
    field
      {j} : I
      ρ : j ⇒ i
      body : F j

  open Yoneda public

  map : ∀ {X} → Functor _⇒_ (Yoneda X)
  map f (g / u) = (f ∘ g) / u

  map₂ : ∀ {X Y} → X >> Y → Yoneda X >> Yoneda Y
  map₂ f (ρ / u) = ρ / f u

  lower : ∀ {X} → Functor _⇒_ X → Yoneda X >> X
  lower f (ρ / u) = f ρ u

  Ybind : ∀ {X Y} → X >> Yoneda Y → Yoneda X >> Yoneda Y
  Ybind f y = lower map (map₂ f y)

open import Vars
open import Injection
open import Syntax hiding (Tm; Term; sub; subs; ren; rens)
    
Ix = Ctx × Ty

Ix⟨_,_⟩ : Ix → Ix → Set
Ix⟨ (DA , TA) , (DB , TB) ⟩ = Inj DA DB × TA ≡ TB

data TmS (Sg : Ctx) : Ix → Set where
    con : ∀ {D Ss B} → (c : Sg ∋ (Ss ->> B)) → TmS Sg (D , ! B)
    var : ∀ {D Ss B} → (x : D ∋ (Ss ->> B)) → TmS Sg (D , ! B)
    lam : ∀ {D S Ss B} → TmS Sg (D , S :> Ss ->> B)
   
TmP : ∀ {Sg i} → TmS Sg i → Set
TmP (con {Ss = Ss} c) = ∃ (_∋_ Ss)
TmP (var {Ss = Ss} x) = ∃ (_∋_ Ss)
TmP lam               = ⊤

Tmr : ∀ {Sg i s} → TmP {Sg} {i} s → Ix
Tmr {Sg} {D , [] ->> B}         {con c} (T , _) = D , T
Tmr {Sg} {D , ([] ->> B)}       {var x} (T , _) = D , T
Tmr {Sg} {D , ((S ∷ Ss) ->> B)} {lam}   p       = (D <: S) , (Ss ->> B) 

TmIC : ∀ Sg → IC Ix Ix
TmIC Sg = ic (TmS Sg) TmP (\ {i} {s} → Tmr {Sg} {i} {s})

module FF = FunctorFree Ix⟨_,_⟩

mapTmIC : ∀ {Sg} → FF.FunctorIC (TmIC Sg)
mapTmIC (f , refl) (con c) = (con c)       , (λ pj → pj , (f      , refl))
mapTmIC (f , refl) (var x) = (var (f $ x)) , (λ pj → pj , (f      , refl))
mapTmIC (f , refl) lam     = lam           , (λ pj → pj , (cons f , refl))

MTy⟨_,_⟩ : MTy → MTy → Set
MTy⟨ i , j ⟩ = Ix⟨ (ctx i , ! type i) , (ctx j , ! type j) ⟩

module Y = ContravariantYoneda {MTy} MTy⟨_,_⟩ (λ f g → (proj₁ f ∘i proj₁ g) , trans (proj₂ g) (proj₂ f))
open Y using (_/_; Yoneda)

data Fun (F : MTy → Set) : Ix → Set where
  fun : ∀ {D B} → F (B <<- D) → Fun F (D , ! B)   

record UnFun (F : Ix → Set) (T : MTy) : Set where
  constructor wrap_
  field
    unwrap : F (ctx T , ! type T)
open UnFun

counit : ∀ {F} → Fun (UnFun F) >> F
counit (fun x) = unwrap x

unit : ∀ {F} → F >> UnFun (Fun F)
unit x = wrap fun x

mapFun : ∀ {F} -> Functor MTy⟨_,_⟩ F -> Functor Ix⟨_,_⟩ (Fun F)
mapFun mapF (f , refl) (fun x) = fun (mapF (f , refl) x)

mapFun₂ : ∀ {F G} → F >> G → Fun F >> Fun G
mapFun₂ f (fun x) = fun (f x)

Tm : ∀ Sg G i → Set
Tm Sg G = Free (TmIC Sg) (Fun (Yoneda (_∋_ G)))

ren : ∀ {Sg G} → Functor Ix⟨_,_⟩ (Tm Sg G)
ren = FF.mapFree mapTmIC (mapFun Y.map)

renx : ∀ {Sg G₀ G} → _∋_ G₀ >> UnFun (Tm Sg G) → Yoneda (_∋_ G₀) >> UnFun (Tm Sg G)
renx f y = wrap Y.lower ren (Y.map₂ (unwrap ∘ f) y)

sub : ∀ {Sg G₀ G} → _∋_ G₀ >> UnFun (Tm Sg G) → Tm Sg G₀ >> Tm Sg G
sub f x = bind (counit ∘ mapFun₂ (renx f)) x