```module BoundSig where

open import Function
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Fin hiding (_+_)
open import Data.Nat
open import Data.Sum
open import Data.Product
open import Relation.Unary
open import Relation.Binary.PropositionalEquality

-- * Worlds

record World (Ctxts : Set)(Types : Set) : Set₁ where
field
_⇒_ : (Γ Δ : Ctxts) → Set

_⊗_ : (Γ Δ : Ctxts) → Ctxts
inl : ∀{Γ Δ} → Γ ⇒ (Γ ⊗ Δ)
inr : ∀{Γ Δ} → Δ ⇒ (Γ ⊗ Δ)

⟦_⟧ : Ctxts → (Types → Set)
⟦_⟧map : ∀{Γ Δ} → Γ ⇒ Δ → ⟦ Γ ⟧ ⊆ ⟦ Δ ⟧
strict-⟦⟧ : ∀{Γ Δ} → ⟦ Γ ⊗ Δ ⟧ ⊆ ⟦ Γ ⟧ ∪ ⟦ Δ ⟧

module MapW {Ctxts : Set}{Types : Set}(w : World Ctxts Types) where

open World w

inl-⟦⟧ :  ∀ {Γ} Δ → ⟦ Γ ⟧ ⊆ ⟦ Γ ⊗ Δ ⟧
inl-⟦⟧ Δ = ⟦ inl ⟧map

inr-⟦⟧ : ∀ {Δ} Γ → ⟦ Δ ⟧ ⊆ ⟦ Γ ⊗ Δ ⟧
inr-⟦⟧ Δ = ⟦ inr ⟧map

mapL : ∀{Γ Δ Ω : Ctxts} →
(⟦ Γ ⟧ ⊆ ⟦ Δ ⟧) → ⟦ Γ ⊗ Ω ⟧ ⊆ ⟦ Δ ⊗ Ω ⟧
mapL ρ k = [ inl-⟦⟧ _ ∘ ρ , inr-⟦⟧ _ ]′ (strict-⟦⟧ k)

-- * Presentations

-- A Presentation is a multi-sorted, binding signature :

record Presentation (Ctxts : Set)(Types : Set) : Set₁ where
field
-- Operations:
Op : Types → Set
-- Aritites:
Ar : ∀{T} → Op T → Set
-- Bindings:
Bi : ∀ {T sh} → Ar {T} sh → Ctxts
-- Typings of recursive arguments:
Ty : ∀ {T sh} → Ar {T} sh → Types

-- * Free term algebra

-- From a presentation, we can build the syntax of terms (defined by
-- Tm) with bindings (defined by Scope[_]).

module Terms {Ctxts Types}(w : World Ctxts Types)
(Σ : Presentation Ctxts Types) where

open World w
open Presentation Σ

mutual
-- Term of type I in context W:
data Tm (Γ : Ctxts) : Types → Set where
`var : ∀{T} → ⟦ Γ ⟧ T → Tm Γ T
`op : ∀{T} → (sh : Op T)
(Xs : (pos : Ar sh) → Scope[ Bi pos ] Γ (Ty pos)) → Tm Γ T

-- Binder of Ω-variables :
data Scope[_] (Ω Γ : Ctxts)(T : Types) : Set where
sc : Tm (Γ ⊗ Ω) T → Scope[ Ω ] Γ T

-- Question: According to the ncat lab
-- [http://ncatlab.org/nlab/show/tensorial+strength], having a strong
-- functor equivalent to having an enriched functor. We use the
-- stength only once in 'scopeSub' to build the term:
--   λ v → str mapTm (Data.Sum.map ρ id (mon⟦⟧ v)) : ⟦ Γ ⟧ ⊗ ⟦ Ω ⟧ ⊆ Tm (Δ ⊗ Ω)
--     with ρ : ⟦ Γ ⟧ ⊆ Tm Δ
-- I wonder if adopting an enriched approach could absorb this term.

-- * Substitution structure

module Subst {Ctxts Types}(w : World Ctxts Types)
(Σ : Presentation Ctxts Types) where

open World w
open MapW w
open Presentation Σ
open Terms w Σ

mutual
-- Scope[ Ω ] : W → Set/I is a functor
--   ie. for f ∈ W(Γ, Δ)
--         we have a functorial map
--           mapSc f ∈ Set/I(Scope Γ, Scope Δ)
mapSc : ∀{Ω Γ Δ} →
(⟦ Γ ⟧ ⊆ ⟦ Δ ⟧) → Scope[ Ω ] Γ ⊆ Scope[ Ω ] Δ
mapSc {Ω} ρ (sc tm) = sc (mapTm (mapL {Ω = Ω} ρ) tm)

-- Tm : W → Set/I is a functor
--   ie. for f ∈ W(Γ, Δ),
--         we have a functorial map
--           mapTm f ∈ Set/I(Tm Γ, Tm Δ)
mapTm : ∀{Γ Δ} →
(⟦ Γ ⟧ ⊆ ⟦ Δ ⟧) → Tm Γ ⊆ Tm Δ
mapTm ρ (`var x) = `var (ρ x)
mapTm ρ (`op sh Xs) = `op sh λ pos → mapSc {Bi pos} ρ (Xs pos)

-- Tm is a (relative-)strong:
str : {Γ Δ : Ctxts} → Tm Γ ∪ ⟦ Δ ⟧ ⊆ Tm (Γ ⊗ Δ)
str {Δ = Δ} (inj₁ tm) = mapTm (inl-⟦⟧ Δ) tm
str (inj₂ k) = `var (inr-⟦⟧ _ k)

-- Tm Σ : W → Set/I is a relative monad over ⟦_⟧ : W → Set/I
--   ie.
--    1. we have a natural transformation
--         return : ∀ Γ. Set/I(⟦ Γ ⟧, Tm Γ)

return : ∀{Γ} → ⟦ Γ ⟧ ⊆ Tm Γ
return = `var

mutual
--    2. we have a natural transformation
--         bind : ∀ Γ Δ. Set/I(⟦ Γ ⟧, Tm Δ) → Set/I(Tm Γ, Tm Δ)

sub : ∀{Γ Δ} → (⟦ Γ ⟧ ⊆ Tm Δ) → Tm Γ ⊆ Tm Δ
sub ρ (`var x) = ρ x
sub ρ (`op sh Xs) = `op sh (λ pos → scopeSub {Bi pos} ρ (Xs pos))

-- Scope[ Ω ] : W → Set/I is a Tm-module
--   ie. we have a natural transformation
--         scopeSub : ∀ Γ Δ. Set/I(⟦ Γ ⟧, Tm Δ) → Set/I(Scope[ Ω ] Γ, Scope[ Ω ] Δ)

scopeSub : ∀{Ω Γ Δ} → (⟦ Γ ⟧ ⊆ Tm Δ) → Scope[ Ω ] Γ ⊆ Scope[ Ω ] Δ
scopeSub {Ω} ρ (sc tm) = sc (sub (λ v → str (Data.Sum.map ρ id (strict-⟦⟧ v))) tm)

-- * Example: Well-scoped, untyped lambda-calculus

module LC where

-- ** World

monFin : ∀{n m} → Fin (n + m) → Fin m ⊎ Fin n
monFin {zero} xs = inj₁ xs
monFin {suc m} zero = inj₂ zero
monFin {suc m} (suc xs) with monFin {m} xs
monFin {suc m} (suc xs) | inj₁ x = inj₁ x
monFin {suc m} (suc xs) | inj₂ y = inj₂ (suc y)

monFin⁻¹ : ∀{n m} → Fin m ⊎ Fin n → Fin (n + m)
monFin⁻¹ {n}{m} k = [ raise n , inject+ m ]′ k

ℕW : World ℕ ⊤
ℕW = record
{ _⇒_ = λ m n → Fin m → Fin n
; _⊗_ = λ m n → n + m
; inl = λ {Γ}{Δ} → raise Δ
; inr = λ {Γ}{Δ} → inject+ Γ
; ⟦_⟧ = λ n tt → Fin n
; ⟦_⟧map = λ ρ → ρ
; strict-⟦⟧ = monFin
}

-- ** Terms

Σλam : Presentation ℕ ⊤
Σλam = record { Op = λ tt → Bool
; Ar = λ { true → ⊤
; false → Bool }
; Bi = λ { {_} {true} tt → 1
; {_} {false} b → 0 }
; Ty = λ { {_} {true} tt → tt
; {_} {false} a → tt  }  }

open Terms ℕW Σλam

λam : ℕ → Set
λam n = Tm n tt

var : ∀{n} → Fin n → λam n
var = `var

app : ∀{n} → λam n → λam n → λam n
app f s = `op false (λ { true → sc f
; false → sc s })

abs : ∀{n} → λam (suc n) → λam n
abs b = `op true (λ { tt → sc b })

-- ** Substitution

open Subst ℕW Σλam

subst⊢ : ∀{m n} → λam m → (Fin m → λam n) → λam n
subst⊢ tm ρ = sub ρ tm

-- ** Example

tm1 : λam 0
tm1 = abs (var zero)

tm2 : λam 1
tm2 = abs (app (var (suc zero)) (var zero))

tm3 : λam 0
tm3 = subst⊢ tm2 ρ
where ρ : Fin 1 → λam 0
ρ zero = tm1
ρ (suc ())

-- * Example: well-typed lambda-calculus

module STLC where

data Typ : Set where
`■ : Typ
_`⇒_ : (A B : Typ) → Typ

-- ** World

data Ctxt : Set where
ε : Ctxt
_▹_ : Ctxt → Typ → Ctxt

data _`∈_ (T : Typ) : (Γ : Ctxt) → Set where
ze : ∀{Γ} → T `∈ (Γ ▹ T)
suc : ∀{Γ T'} → T `∈ Γ → T `∈ (Γ ▹ T')

_∷_ : Ctxt → Ctxt → Ctxt
Γ ∷ ε = Γ
Γ ∷ (Ω ▹ S) = (Γ ∷ Ω) ▹ S

monW : ∀{Ω Γ T} → T `∈ (Γ ∷ Ω) → T `∈ Γ ⊎ T `∈ Ω
monW {ε} k = inj₁ k
monW {Ω ▹ T} ze = inj₂ ze
monW {Ω ▹ x} (suc k) with monW {Ω} k
monW {Ω ▹ x₁} (suc k) | inj₁ x = inj₁ x
monW {Ω ▹ x} (suc k) | inj₂ y = inj₂ (suc y)

raiseW : ∀ {Γ} Δ → ∀{T} → T `∈ Γ → T `∈ (Γ ∷ Δ)
raiseW ε k = k
raiseW (Δ ▹ x) k = suc (raiseW Δ k)

injectW : ∀ {Γ} Δ → ∀{T} → T `∈ Γ → T `∈ (Δ ∷ Γ)
injectW Δ ze = ze
injectW Δ (suc k) = suc (injectW Δ k)

monW⁻¹ : ∀{Ω Γ T} → T `∈ Γ ⊎ T `∈ Ω → T `∈ (Γ ∷ Ω)
monW⁻¹ {Ω}{Γ} = [ raiseW Ω , injectW Γ ]′

CtxtW : World Ctxt Typ
CtxtW = record
{ _⇒_ = λ Γ Δ → ∀ {T} → T `∈ Γ → T `∈ Δ
; _⊗_ = _∷_
; inl = λ {Γ}{Δ} → raiseW {Γ} Δ
; inr =  λ {Γ}{Δ} → injectW {Δ} Γ
; ⟦_⟧ = λ Γ T → T `∈ Γ
; ⟦_⟧map = λ ρ → ρ
; strict-⟦⟧ = monW
}

-- ** Terms

Σλam : Presentation Ctxt Typ
Σλam = record { Op = λ T → Typ ⊎ (Σ[ A ∈ Typ ] Σ[ B ∈ Typ ] T ≡ A `⇒ B)
; Ar = λ { (inj₁ S) → Bool
; (inj₂ (A , B , q)) → ⊤ }
; Bi = λ {T} → λ { {sh = inj₁ S} x → ε
; {sh = inj₂ (A , B , q)} tt → ε ▹ A }
; Ty = λ {T} → λ { {sh = inj₁ S} true → S `⇒ T
; {sh = inj₁ S} false → S
; {sh = inj₂ (A , B , q)} tt → B } }

open Terms CtxtW Σλam

_⊢_ : (Γ : Ctxt) → Typ → Set
Γ ⊢ T = Tm Γ T

var : ∀{Γ T} → T `∈ Γ → Γ ⊢ T
var k = `var k

app : ∀{Γ S T} → Γ ⊢ (S `⇒ T) → Γ ⊢ S → Γ ⊢ T
app {S = S} f s = `op (inj₁ S) (λ { true → sc f
; false → sc s })

abs : ∀{Γ S T} → (Γ ▹ S) ⊢ T → Γ ⊢ (S `⇒ T)
abs {S = S}{T = T} b = `op (inj₂ (S , T , refl))
(λ { tt → sc b })

-- ** Substitution

open Subst CtxtW Σλam

subst⊢ : ∀{Γ Δ T} → Γ ⊢ T → (∀{T} → T `∈ Γ → Δ ⊢ T) → Δ ⊢ T
subst⊢ tm ρ = sub ρ tm

-- ** Example

tm1 : ε ⊢ (`■ `⇒ `■)
tm1 = abs (var ze)

tm2 : (ε ▹ (`■ `⇒ `■)) ⊢ (`■ `⇒ `■)
tm2 = abs (app (var (suc ze)) (var ze))

tm3 : ε ⊢ (`■ `⇒ `■)
tm3 = subst⊢ tm2 ρ
where ρ : ∀{T} → T `∈ (ε ▹ (`■ `⇒ `■)) → ε ⊢ T
ρ ze = tm1
ρ (suc ())

--  test : tm3 ≡ abs (app (abs (var ze)) (var ze))
--  test = {!!}
{-
-- * Example: System F

module F where

-- ** World

monFin : ∀{n m} → Fin (n + m) → Fin m ⊎ Fin n
monFin {zero} xs = inj₁ xs
monFin {suc m} zero = inj₂ zero
monFin {suc m} (suc xs) with monFin {m} xs
monFin {suc m} (suc xs) | inj₁ x = inj₁ x
monFin {suc m} (suc xs) | inj₂ y = inj₂ (suc y)

monFin⁻¹ : ∀{n m} → Fin m ⊎ Fin n → Fin (n + m)
monFin⁻¹ {n}{m} k = [ raise n , inject+ m ]′ k

ℕW : World ⊤ ℕ
ℕW = record { ⟦_⟧ = λ n tt → Fin n
; _⊗_ = λ m n → n + m
; mon⟦⟧ = monFin
; mon⟦⟧⁻¹ = monFin⁻¹ }

-- ** Terms

data FTy : Set where
base arrow forll : FTy

ΣFTy : Presentation ℕ ⊤
ΣFTy = record { Op = λ tt → FTy
; Ar = λ { base → ⊥
; arrow → Bool
; forll → ⊤ }
; Bi = λ { {_} {base} b → 0
; {_} {arrow} b → 0
; {_} {forll} b → 1 }
; Ty = λ _ → tt }

module Ty where
open Terms ℕW ΣFTy

Ty : ℕ → Set
Ty n = Tm n tt

tvar : ∀{n} → Fin n → Ty n
tvar = `var

_`⇒_ : ∀{n} → Ty n → Ty n → Ty n
σ `⇒ τ = `op arrow (λ { true → sc σ
; false → sc τ })

`∀ : ∀{n} → Ty (suc n) → Ty n
`∀ τ = `op forll (λ { tt → sc τ })

open Ty

-- ** Substitution

subst⊢ : ∀{m n} → Ty m → (Fin m → Ty n) → Ty n
subst⊢ tm ρ = sub ρ tm
where open Subst ℕW ΣFTy

-- ** Term World

data Ctxt (n : ℕ) : Set where
ε : Ctxt n
_▹_ : Ctxt n → Ty n → Ctxt n

data _`∈_ {n} (T : Ty n) : (Γ : Ctxt n) → Set where
ze : ∀{Γ} → T `∈ (Γ ▹ T)
suc : ∀{Γ T'} → T `∈ Γ → T `∈ (Γ ▹ T')

weakenCtxt : ∀{n} → Ctxt n → Ctxt (1 + n)
weakenCtxt ε = ε
weakenCtxt (Γ ▹ T) = weakenCtxt Γ ▹ mapTm suc T
where open Subst ℕW ΣFTy

∫Γ : Set
∫Γ = Σ[ n ∈ ℕ ] Ctxt n

∫T : Set
∫T = Σ[ n ∈ ℕ ] Ty n

_∷_ : ∫Γ → ∫Γ → ∫Γ
Γ ∷ Δ = {!!}

∫GW : World (Σ ℕ Ty) ∫Γ
∫GW = record { ⟦_⟧ = λ { (n , Γ) (k , T) → Σ[ q ∈ k ≡ n ] subst Ty q T `∈ Γ }
; _⊗_ = _∷_
; mon⟦⟧ = {!!}
; mon⟦⟧⁻¹ = {!!} }

bind : ∀{n} → (σ : Ty n)(τ : Ty (1 + n)) → Ty n
bind σ τ = subst⊢ τ (λ { zero → σ ; (suc k) → tvar k })

data FTm (n : ℕ)(τ' : Ty n) : Set where
`abs : (σ : Ty n)(τ : Ty n)(q : τ' ≡ σ `⇒ τ) → FTm n τ'
`app : (σ : Ty n) → FTm n τ'
`tabs : (τ : Ty (1 + n))(q : τ' ≡ `∀ τ) → FTm n τ'
`tapp : (σ : Ty n)(τ : Ty (1 + n))(q : τ' ≡ bind σ τ) → FTm n τ'

ΣFTm : Presentation ∫Γ ∫T
ΣFTm = record { Op = λ { (n , τ') → FTm n τ' }
; Ar = λ { {(n , τ')} (`abs σ τ q) → ⊤
; {(n , τ)} (`app σ) → Bool
; {(n , τ')} (`tabs τ q) → ⊤
; {(n , τ')} (`tapp σ τ q) → ⊤ }
; Bi = λ { {(n , τ')} {`abs σ τ q} tt → n , (ε ▹ σ)
; {(n , τ)} {`app σ} true → (n , ε)
; {(n , τ)} {`app σ} false → n , ε
; {(n , τ')} {`tabs τ q} tt → 1 + n , ε
; {(n , τ')} {`tapp σ τ q} tt → n , ε }
; Ty = λ { {(n , τ')} {`abs σ τ q} tt → n , τ
; {(n , τ)} {`app σ} true → n , σ `⇒ τ
; {(n , τ)} {`app σ} false → n , σ
; {(n , τ')} {`tabs τ q} tt → 1 + n , τ
; {(n , τ')} {`tapp σ τ q} tt → n , `∀ τ } }

module Tm where
open Terms ∫GW ΣFTm

_⊢_ : {m : ℕ} → Ctxt m → Ty m → Set
_⊢_ {n} Γ T = Tm (n , Γ) (n , T)

var : ∀{n}{Γ : Ctxt n}{τ : Ty n} → τ `∈ Γ → Γ ⊢ τ
var k = `var (refl , k)

lam :  ∀{n}{Γ : Ctxt n}{σ τ : Ty n} → (Γ ▹ σ) ⊢ τ → Γ ⊢ (σ `⇒ τ)
lam {σ = σ}{τ = τ} b = `op (`abs σ τ refl) (λ { tt → sc b })

app : ∀{n}{Γ : Ctxt n}{σ τ : Ty n} → Γ ⊢ (σ `⇒ τ) → Γ ⊢ σ → Γ ⊢ τ
app {σ = σ} f s = `op (`app σ) (λ { true → sc f
; false → sc s })

tlam : ∀{n}{Γ : Ctxt n}{τ : Ty (1 + n)} → weakenCtxt Γ ⊢ τ → Γ ⊢ `∀ τ
tlam {τ = τ} f = `op (`tabs τ refl) (λ { tt → sc f })

tapp : ∀{n}{Γ : Ctxt n}{σ : Ty n}{τ : Ty (1 + n)} → Γ ⊢ `∀ τ → Γ ⊢ bind σ τ
tapp {σ = σ}{τ = τ} t = `op (`tapp σ τ refl) (λ { tt → sc t })

open Tm

-- * Outro

-- Local Variables:
-- mode: outline-minor
-- outline-regexp: "-- [*\f]+"
-- outline-level: outline-level
-- End:

-}```