{-# 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.Try6 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)


Pr : Set
Pr = β„•

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

mutual
  infixl 7 _∘_
  infixr 5 πœ†_
--  infixl 3 _∧_
  infixr 2 _βŠƒ_
  infixl 1 _∷_
  infixr 0 _βˆ™_⊒_

  data Ty {m : β„•} (Ξ” : Cx m) : Set where
    Ξ±_  : Pr β†’ Ty Ξ”
    _βŠƒ_ : Ty Ξ” β†’ Ty Ξ” β†’ Ty Ξ”
--    _∧_ : Ty Ξ” β†’ Ty Ξ” β†’ Ty Ξ”

  data Ass {n m : β„•} (Ξ” : Cx m) (Ξ“ : Cx n) : Set where
    Ο„_  : Ty Ξ” β†’ Ass Ξ” Ξ“
    _∷_ : (A : Ass Ξ” Ξ“) β†’ Ξ” βˆ™ Ξ“ ⊒ A β†’ Ass Ξ” Ξ“

  data _βˆ™_⊒_ {m n : β„•} (Ξ” : Cx m) (Ξ“ : Cx n) : Ass Ξ” Ξ“ β†’ Set where
    𝑓_ : βˆ€{A}
       β†’ A ∈ Ξ”
       β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ Ξ± A

    𝑓²_ : βˆ€{A}
        β†’ (x : A ∈ Ξ”)
        β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ Ξ± A ∷ 𝑓 x

    𝑓³_ : βˆ€{A}
        β†’ (x : A ∈ Ξ”)
        β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ Ξ± A ∷ 𝑓 x ∷ 𝑓² x

    𝑣_ : βˆ€{A}
       β†’ A ∈ Ξ“
       β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ Ξ± A

    𝑣²_ : βˆ€{A}
        β†’ (x : A ∈ Ξ“)
        β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ Ξ± A ∷ 𝑣 x

    𝑣³_ : βˆ€{A}
        β†’ (x : A ∈ Ξ“)
        β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ Ξ± A ∷ 𝑣 x ∷ 𝑣² x

    πœ†_ : βˆ€{A B}
       β†’ Ξ” βˆ™ Ξ“ , A ⊒ Ο„ B
       β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ (Ξ± A βŠƒ B)

    πœ†Β²_ : βˆ€{A B t}
        β†’ Ξ” βˆ™ Ξ“ , A ⊒ Ο„ B ∷ t
        β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ (Ξ± A βŠƒ B) ∷ πœ† t

    πœ†Β³_ : βˆ€{A B t tβ‚‚}
        β†’ Ξ” βˆ™ Ξ“ , A ⊒ Ο„ B ∷ t ∷ tβ‚‚
        β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ (Ξ± A βŠƒ B) ∷ πœ† t ∷ πœ†Β² tβ‚‚

    _∘_ : βˆ€{A B}
        β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ (A βŠƒ B)    β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ A
        β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ B

    _∘²_ : βˆ€{A B t s}
         β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ (A βŠƒ B) ∷ t    β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ A ∷ s
         β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ B ∷ t ∘ s

    _∘³_ : βˆ€{A B t tβ‚‚ s sβ‚‚}
         β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ (A βŠƒ B) ∷ t ∷ tβ‚‚    β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ A ∷ s ∷ sβ‚‚
         β†’ Ξ” βˆ™ Ξ“ ⊒ Ο„ B ∷ t ∘ s ∷ tβ‚‚ ∘² sβ‚‚

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 = {!πœ† ?!}


--     _𝑝_ : βˆ€{A B}
--         β†’ Ξ” βˆ™ Ξ“ ⊒ A    β†’ Ξ” βˆ™ Ξ“ ⊒ B
--         β†’ Ξ” βˆ™ Ξ“ ⊒ A ∧ B

--     πœ‹β‚€_ : βˆ€{A B}
--         β†’ Ξ” βˆ™ Ξ“ ⊒ A ∧ B
--         β†’ Ξ” βˆ™ Ξ“ ⊒ A

--     πœ‹β‚_ : βˆ€{A B}
--         β†’ Ξ” βˆ™ Ξ“ ⊒ A ∧ B
--         β†’ Ξ” βˆ™ Ξ“ ⊒ B

--     !_ : βˆ€{A}
--        β†’ Ξ” βˆ™ Ξ“ ⊒ A
--        β†’ Ξ” βˆ™ Ξ“ ⊒ A

-- {-    ⇑_ : βˆ€{A u}
--        β†’ (t : Ξ” βˆ™ βˆ… ⊒ A ∷ u)
--        β†’ Ξ” βˆ™ Ξ“ ⊒ A ∷ u ∷ ! t

--     ⇓_ : βˆ€{A t}
--        β†’ Ξ” βˆ™ Ξ“ ⊒ A ∷ t
--        β†’ Ξ” βˆ™ Ξ“ ⊒ A-}

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

-- -- TTTm : Ty βˆ… β†’ Set
-- -- TTTm = TTm βˆ…

-- -- TTTI : βˆ€{A} β†’ TTTm (A βŠƒ A)
-- -- TTTI = πœ† 𝑣 Z

-- -- TTTK : βˆ€{A B} β†’ TTTm (A βŠƒ B βŠƒ A)
-- -- TTTK = πœ† πœ† 𝑣 S Z

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


-- -- --axT : βˆ€{x A} β†’ TTm (βˆ… , x) ((A ∷ 𝑓 Z) βŠƒ A ∷ πœ† ⇓ 𝑣 Z)
-- -- --axT = {!!}

-- -- --axK : βˆ€{f x A} β†’ TTm (βˆ… , f , x) (A βŠƒ B ∷