{-# OPTIONS --allow-unsolved-metas #-}

{-

'(agda-input-user-translations
   (quote
    (("i" "βŠƒ") ("e" "⊒") ("t" "⊩")
     ("f" "𝑓") ("f2" "𝑓²") ("f3" "𝑓³") ("fn" "𝑓ⁿ")
     ("v" "𝑣") ("v2" "𝑣²") ("v3" "𝑣³") ("vn" "𝑣ⁿ")
     ("l" "πœ†") ("l2" "πœ†Β²") ("l3" "πœ†Β³") ("ln" "πœ†βΏ")
     ("o" "∘") ("o2" "∘²") ("o3" "∘³") ("on" "∘ⁿ")
     ("p" "𝑝") ("p2" "𝑝²") ("p3" "𝑝³") ("pn" "𝑝ⁿ")
     ("1" "πœ‹β‚€") ("12" "πœ‹β‚€Β²") ("13" "πœ‹β‚€Β³") ("1n" "πœ‹β‚€βΏ")
     ("2" "πœ‹β‚") ("22" "πœ‹β‚Β²") ("23" "πœ‹β‚Β³") ("2n" "πœ‹β‚βΏ")
     ("u" "⇑") ("u2" "⇑²") ("u3" "⇑³") ("un" "⇑ⁿ")
     ("d" "⇓") ("d2" "⇓²") ("d3" "⇓³") ("dn" "⇓ⁿ"))))

-}

module A201602.Try5 where

open import Data.Fin using (Fin; zero; suc; toβ„•)
open import Data.Nat using (β„•; zero; suc; _+_)
open import Data.Product using (Ξ£; _Γ—_; _,_)


data Vec (X : Set) : β„• β†’ Set where
  βˆ…   : Vec X zero
  _,_ : βˆ€{n} β†’ Vec X n β†’ X β†’ Vec X (suc n)

data _∈_ {X : Set} : βˆ€{n} β†’ X β†’ Vec X n β†’ Set where
  Z  : βˆ€{n x} {xs : Vec X n}
     β†’ x ∈ (xs , x)
  S_ : βˆ€{n x y} {xs : Vec X n}
     β†’ x ∈ xs
     β†’ x ∈ (xs , y)


data Pr : Set where
  βŠ₯ : Pr

PCx : β„• β†’ Set
PCx = Vec Pr

infixr 1 _βŠƒ_
data Ty {m : β„•} (Ξ” : PCx m) : Set where
  𝑓_ : βˆ€{P} β†’ P ∈ Ξ” β†’ Ty Ξ”
  _βŠƒ_ : Ty Ξ” β†’ Ty Ξ” β†’ Ty Ξ”
  β– _ : Ty Ξ” β†’ Ty Ξ”

TCx : βˆ€{m} β†’ PCx m β†’ β„• β†’ Set
TCx Ξ” = Vec (Ty Ξ”)

infixl 4 _∘_
infixr 3 πœ†_
infixr 0 _⊒_
data _⊒_ {m n : β„•} {Ξ” : PCx m} (Ξ“ : TCx Ξ” n) : Ty Ξ” β†’ Set where
  𝑣_ : βˆ€{A} β†’ A ∈ Ξ“ β†’ Ξ“ ⊒ A
  πœ†_ : βˆ€{A B} β†’ (Ξ“ , A) ⊒ B β†’ Ξ“ ⊒ (A βŠƒ B)
  _∘_ : βˆ€{A B} β†’ Ξ“ ⊒ (A βŠƒ B) β†’ Ξ“ ⊒ A β†’ Ξ“ ⊒ B

infixr 0 ⊩_
⊩_ : Ty βˆ… β†’ Set
⊩_ A = βˆ€{n} {Ξ“ : TCx βˆ… n} β†’ Ξ“ ⊒ A

F : βˆ€{m} (Ξ” : PCx m) β†’ Ty Ξ” β†’ Set
F Ξ” A = βˆ€{n} {Ξ“ : TCx Ξ” n} β†’ Ξ“ ⊒ A

tI : βˆ€{A} β†’ ⊩ A βŠƒ A
tI = πœ† 𝑣 Z

tK : βˆ€{A B} β†’ ⊩ A βŠƒ B βŠƒ A
tK = πœ† πœ† 𝑣 S Z

tS : βˆ€{A B C} β†’ ⊩ (A βŠƒ B βŠƒ C) βŠƒ (A βŠƒ B) βŠƒ A βŠƒ C
tS = πœ† πœ† πœ† (𝑣 S S Z ∘ 𝑣 Z) ∘ (𝑣 S Z ∘ 𝑣 Z)

tJ : βˆ€{x} β†’ F (βˆ… , x) (β–  𝑓 Z)
tJ = {!!}