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

{-

'(agda-input-user-translations
   (quote
    (("i" "βŠƒ") ("e" "⊒") ("t" "⊩")
     ("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.Try2 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)



{-

A ∈ Ξ“
--------- M𝑣 Z
Ξ“ , A ⊒ A
--------- Mπœ†
Ξ“ ⊒ A βŠƒ A


A ∈ Ξ“
----------------- M𝑣² Z
Ξ“ , A ⊒ 𝑣 Z : A
----------------- Mπœ†Β²
Ξ“ ⊒ πœ† 𝑣 Z : A βŠƒ A


A ∈ Ξ“
--------------------------- M𝑣³ Z
Ξ“ , A ⊒ 𝑣² Z : 𝑣 Z : A
--------------------------- Mπœ†Β³
Ξ“ ⊒ πœ†Β² 𝑣² Z : πœ† 𝑣 Z : A βŠƒ A

-}


infixl 4 _∘_ _∘²_ _∘³_
infixr 3 πœ†_ πœ†Β²_ πœ†Β³_
infixl 2 _∧_
infixr 1 _βŠƒ_
infixr 0 _⊒_ ⊩_ _⊒_∷_ ⊩_∷_ _⊒_∷_∷_ ⊩_∷_∷_


data Ty : Set where
  βŠ₯   : Ty
  _βŠƒ_ : Ty β†’ Ty β†’ Ty
  _∧_ : Ty β†’ Ty β†’ Ty


Cx : β„• β†’ Set
Cx = Vec Ty


data _⊒_ {n : β„•} (Ξ“ : Cx n) : Ty β†’ Set where
  𝑣_     : βˆ€{A}
         β†’ A ∈ Ξ“
         β†’ Ξ“ ⊒ A
  πœ†_     : βˆ€{A B}
         β†’ Ξ“ , A ⊒ B
         β†’ Ξ“ ⊒ A βŠƒ B
  _∘_    : βˆ€{A B}
         β†’ Ξ“ ⊒ A βŠƒ B    β†’ Ξ“ ⊒ A
         β†’ Ξ“ ⊒ B
  π‘βŸ¨_,_⟩ : βˆ€{A B}
         β†’ Ξ“ ⊒ A        β†’ Ξ“ ⊒ B
         β†’ Ξ“ ⊒ A ∧ B
  πœ‹β‚€_    : βˆ€{A B}
         β†’ Ξ“ ⊒ A ∧ B
         β†’ Ξ“ ⊒ A
  πœ‹β‚_    : βˆ€{A B}
         β†’ Ξ“ ⊒ A ∧ B
         β†’ Ξ“ ⊒ B

⊩_ : Ty β†’ Set
⊩ A = βˆ€{n} {Ξ“ : Cx 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)


data _⊒_∷_ {n : β„•} (Ξ“ : Cx n) : (A : Ty) β†’ Ξ“ ⊒ A β†’ Set where
  𝑣²_     : βˆ€{A}
          β†’ (x : A ∈ Ξ“)
          β†’ Ξ“ ⊒ A ∷ 𝑣 x
  πœ†Β²_     : βˆ€{A B t}
          β†’ Ξ“ , A ⊒ B ∷ t
          β†’ Ξ“ ⊒ A βŠƒ B ∷ πœ† t
  _∘²_    : βˆ€{A B t s}
          β†’ Ξ“ ⊒ A βŠƒ B ∷ t    β†’ Ξ“ ⊒ A ∷ s
          β†’ Ξ“ ⊒ B ∷ t ∘ s
  π‘Β²βŸ¨_,_⟩ : βˆ€{A B t s}
          β†’ Ξ“ ⊒ A ∷ t        β†’ Ξ“ ⊒ B ∷ s
          β†’ Ξ“ ⊒ A ∧ B ∷ π‘βŸ¨ t , s ⟩
  πœ‹β‚€Β²_    : βˆ€{A B t}
          β†’ Ξ“ ⊒ A ∧ B ∷ t
          β†’ Ξ“ ⊒ A ∷ πœ‹β‚€ t
  πœ‹β‚Β²_    : βˆ€{A B t}
          β†’ Ξ“ ⊒ A ∧ B ∷ t
          β†’ Ξ“ ⊒ B ∷ πœ‹β‚ t
  !_      : βˆ€{A t}
          β†’ Ξ“ ⊒ A ∷ t
          β†’ Ξ“ ⊒ A ∷ t

⊩_∷_ : (A : Ty) β†’ ⊩ A β†’ Set
⊩ A ∷ t = βˆ€{n} {Ξ“ : Cx n} β†’ Ξ“ ⊒ A ∷ t


tIΒ² : βˆ€{A} β†’ ⊩ A βŠƒ A
    ∷ πœ† 𝑣 Z
tIΒ² = πœ†Β² (𝑣² Z)

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

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


data _⊒_∷_∷_ {n : β„•} (Ξ“ : Cx n) : (A : Ty) β†’ (t : Ξ“ ⊒ A) β†’ Ξ“ ⊒ A ∷ t β†’ Set where
  𝑣³_     : βˆ€{A}
          β†’ (x : A ∈ Ξ“)
          β†’ Ξ“ ⊒ A ∷ 𝑣 x ∷ 𝑣² x
  πœ†Β³_     : βˆ€{A B t tβ‚‚}
          β†’ Ξ“ , A ⊒ B ∷ t ∷ tβ‚‚
          β†’ Ξ“ ⊒ A βŠƒ B ∷ πœ† t ∷ πœ†Β² tβ‚‚
  _∘³_    : βˆ€{A B t tβ‚‚ s sβ‚‚}
          β†’ Ξ“ ⊒ A βŠƒ B ∷ t ∷ tβ‚‚   β†’ Ξ“ ⊒ A ∷ s ∷ sβ‚‚
          β†’ Ξ“ ⊒ B ∷ t ∘ s ∷ tβ‚‚ ∘² sβ‚‚
  π‘Β³βŸ¨_,_⟩ : βˆ€{A B t tβ‚‚ s sβ‚‚}
          β†’ Ξ“ ⊒ A ∷ t ∷ tβ‚‚       β†’ Ξ“ ⊒ B ∷ s ∷ sβ‚‚
          β†’ Ξ“ ⊒ A ∧ B ∷ π‘βŸ¨ t , s ⟩ ∷ π‘Β²βŸ¨ tβ‚‚ , sβ‚‚ ⟩
  πœ‹β‚€Β³_    : βˆ€{A B t tβ‚‚}
          β†’ Ξ“ ⊒ A ∧ B ∷ t ∷ tβ‚‚
          β†’ Ξ“ ⊒ A ∷ πœ‹β‚€ t ∷ πœ‹β‚€Β² tβ‚‚
  πœ‹β‚Β³_    : βˆ€{A B t tβ‚‚}
          β†’ Ξ“ ⊒ A ∧ B ∷ t ∷ tβ‚‚
          β†’ Ξ“ ⊒ B ∷ πœ‹β‚ t ∷ πœ‹β‚Β² tβ‚‚
  !_      : βˆ€{A t tβ‚‚}
          β†’ Ξ“ ⊒ A ∷ t ∷ tβ‚‚
          β†’ Ξ“ ⊒ A ∷ t ∷ tβ‚‚

⇑_ : βˆ€{A n} {Ξ“ : Cx n} {u : Ξ“ ⊒ A}
   β†’ (x : Ξ“ ⊒ A ∷ u)
   β†’ Ξ“ ⊒ A ∷ u ∷ (! x)
⇑_ = {!!}

⇓_ : βˆ€{A n} {Ξ“ : Cx n} {u : Ξ“ ⊒ A}
   β†’ Ξ“ ⊒ A ∷ u
   β†’ Ξ“ ⊒ A
⇓_ {u = u} = Ξ» _ β†’ u

⊩_∷_∷_ : (A : Ty) β†’ (t : ⊩ A) β†’ ⊩ A ∷ t β†’ Set
⊩ A ∷ t ∷ tβ‚‚ = βˆ€{n} {Ξ“ : Cx n} β†’ Ξ“ ⊒ A ∷ t ∷ tβ‚‚


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

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

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