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

{-

'(agda-input-user-translations
   (quote
    (("i" "βŠƒ") ("e" "⊒") ("t" "⊩") ("N" "β„•")
     ("f" "𝑓") ("f2" "𝑓²") ("f3" "𝑓³") ("fn" "𝑓ⁿ")
     ("b" "𝑏") ("b2" "𝑏²") ("b3" "𝑏³") ("bn" "𝑏ⁿ")
     ("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.Try7 where

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)


infixl 7 _∘⁰_ _∘_ _∘²_
infixr 5 πœ†β°_ πœ†_ πœ†Β²_
infixl 3 _∧_
infixr 2 _βŠƒ_
infixl 1 _∷_
infixr 0 _⊒_

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

  data Ty : Set where
    βŠ₯ : Ty
    _βŠƒ_ : Ty β†’ Ty β†’ Ty
    _∧_ : Ty β†’ Ty β†’ Ty
    _∷_ : βˆ€{m} {Ξ“ : Cx m} (A : Ty) β†’ Ξ“ ⊒ A β†’ Ty

  data _⊒_ {m : β„•} (Ξ“ : Cx m) : Ty β†’ Set where
    𝑓⁰_   : βˆ€{A}
          β†’ β„•
          β†’ Ξ“ ⊒ A
    𝑣⁰_   : βˆ€{A}
          β†’ A ∈ Ξ“
          β†’ Ξ“ ⊒ A
    πœ†β°_   : βˆ€{A B}
          β†’ Ξ“ , A ⊒ B
          β†’ Ξ“ ⊒ A βŠƒ B
    _∘⁰_  : βˆ€{A B}
          β†’ Ξ“ ⊒ A βŠƒ B    β†’ Ξ“ ⊒ A
          β†’ Ξ“ ⊒ B

    𝑣_   : βˆ€{A}
         β†’ (x : A ∈ Ξ“)
         β†’ Ξ“ ⊒ A ∷ 𝑣⁰ x
    πœ†_   : βˆ€{A B} β†’ {t : Ξ“ , A ⊒ B}
         β†’ Ξ“ , A ⊒ B ∷ t
         β†’ Ξ“ ⊒ A βŠƒ B ∷ πœ†β° t
    _∘_  : βˆ€{A B} β†’ {t : Ξ“ ⊒ A βŠƒ B} {s : Ξ“ ⊒ A}
         β†’ Ξ“ ⊒ A βŠƒ B ∷ t    β†’ Ξ“ ⊒ A ∷ s
         β†’ Ξ“ ⊒ B ∷ t ∘⁰ s

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

    𝑣²_  : βˆ€{A}
         β†’ (x : A ∈ Ξ“)
         β†’ Ξ“ ⊒ A ∷ 𝑣⁰ x ∷ 𝑣 x
    πœ†Β²_  : βˆ€{A B} β†’ {t : Ξ“ , A ⊒ B} β†’ βˆ€{tβ‚‚}
         β†’ Ξ“ , A ⊒ B ∷ t ∷ tβ‚‚
         β†’ Ξ“ ⊒ A βŠƒ B ∷ πœ†β° t ∷ πœ† tβ‚‚
    _∘²_ : βˆ€{A B} β†’ {t : Ξ“ ⊒ A βŠƒ B} {s : Ξ“ ⊒ A} β†’ βˆ€{tβ‚‚ 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 = πœ†β° πœ†β° πœ†β° (𝑣⁰ S S Z ∘⁰ 𝑣⁰ Z) ∘⁰ (𝑣⁰ S Z ∘⁰ 𝑣⁰ Z)

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)

e11 : βˆ€{A x} β†’ βˆ… ⊒ ((A ∷ 𝑓⁰ x) βŠƒ A) ∷ πœ†β° ⇓ (𝑣⁰ Z)
e11 = {!!}