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

{-

'(agda-input-user-translations
   (quote
    (("i" "βŠƒ") ("e" "⊒") ("t" "⊩") ("N" "β„•")
     ("Mv" "M𝑣") ("v" "𝑣") ("v0" "𝑣⁰") ("v1" "𝑣¹") ("v2" "𝑣²") ("v3" "𝑣³") ("vn" "𝑣ⁿ")
     ("Ml" "Mπœ†") ("l" "πœ†") ("l0" "πœ†β°") ("l1" "πœ†ΒΉ") ("l2" "πœ†Β²") ("l3" "πœ†Β³") ("ln" "πœ†βΏ")
     ("Mo" "M∘") ("o" "∘") ("o0" "∘⁰") ("o1" "∘¹") ("o2" "∘²") ("o3" "∘³") ("on" "∘ⁿ")
     ("Mp" "M𝑝") ("p" "𝑝") ("p0" "𝑝⁰") ("p1" "𝑝¹") ("p2" "𝑝²") ("p3" "𝑝³") ("pn" "𝑝ⁿ")
     ("M1" "Mπœ‹β‚€") ("1" "πœ‹β‚€") ("10" "πœ‹β‚€β°") ("11" "πœ‹β‚€ΒΉ") ("12" "πœ‹β‚€Β²") ("13" "πœ‹β‚€Β³") ("1n" "πœ‹β‚€βΏ")
     ("M2" "Mπœ‹β‚") ("2" "πœ‹β‚") ("20" "πœ‹β‚β°") ("21" "πœ‹β‚ΒΉ") ("22" "πœ‹β‚Β²") ("23" "πœ‹β‚Β³") ("2n" "πœ‹β‚βΏ")
     ("Mu" "M⇑") ("u" "⇑") ("u0" "⇑⁰") ("u1" "⇑¹") ("u2" "⇑²") ("u3" "⇑³") ("un" "⇑ⁿ")
     ("Md" "M⇓") ("d" "⇓") ("d0" "⇓⁰") ("d1" "⇓¹") ("d2" "⇓²") ("d3" "⇓³") ("dn" "⇓ⁿ")
     ("M-" "M⁻") ("M+" "M⁺"))))

-}

module A201602.Try12 where

open import Data.Nat using (β„•; zero; suc; _+_)
open import Data.Product using (Σ) renaming (_,_ to ⟨_,_⟩)

infixl 5 _∘_ _∘²_
infixr 4 πœ†_,_ πœ†Β²_,_
infixr 3 _∢_
infixr 3 _β€˜_
infixl 3 _,_
infixl 2 _∧_
infixr 1 _βŠƒ_
infixr 1 _βŠƒβŠ‚_
infixr 0 _⊒_∷_
infixr 0 ⊩_ ⊩_∷_ ⊩_∷_∷_



Var : Set
Var = β„•


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

  data Tm : Set where
    𝑣_        : Var β†’ Tm
    πœ†[_]_,_   : β„• β†’ Var β†’ Tm β†’ Tm
    _∘[_]_    : Tm β†’ β„• β†’ Tm β†’ Tm
    𝑝[_]⟨_,_⟩ : β„• β†’ Tm β†’ Tm β†’ Tm
    πœ‹β‚€[_]_    : β„• β†’ Tm β†’ Tm
    πœ‹β‚[_]_    : β„• β†’ Tm β†’ Tm
    !_        : Tm β†’ Tm
    ⇑[_]_     : β„• β†’ Tm β†’ Tm
    ⇓[_]_     : β„• β†’ Tm β†’ Tm


⊀ : Ty
⊀ = βŠ₯ βŠƒ βŠ₯

Β¬_ : Ty β†’ Ty
Β¬ A = A βŠƒ βŠ₯

_βŠƒβŠ‚_ : Ty β†’ Ty β†’ Ty
A βŠƒβŠ‚ B = A βŠƒ B ∧ B βŠƒ A


πœ†_,_ : Var β†’ Tm β†’ Tm
πœ† x , t = πœ†[ 1 ] x , t

πœ†Β²_,_ : Var β†’ Tm β†’ Tm
πœ†Β² xβ‚‚ , tβ‚‚ = πœ†[ 2 ] xβ‚‚ , tβ‚‚

_∘_ : Tm β†’ Tm β†’ Tm
t ∘ s = t ∘[ 1 ] s

_∘²_ : Tm β†’ Tm β†’ Tm
tβ‚‚ ∘² sβ‚‚ = tβ‚‚ ∘[ 2 ] sβ‚‚

π‘βŸ¨_,_⟩ : Tm β†’ Tm β†’ Tm
π‘βŸ¨ t , s ⟩ = 𝑝[ 1 ]⟨ t , s ⟩

π‘Β²βŸ¨_,_⟩ : Tm β†’ Tm β†’ Tm
π‘Β²βŸ¨ tβ‚‚ , sβ‚‚ ⟩ = 𝑝[ 2 ]⟨ tβ‚‚ , sβ‚‚ ⟩

πœ‹β‚€_ : Tm β†’ Tm
πœ‹β‚€ t = πœ‹β‚€[ 1 ] t

πœ‹β‚€Β²_ : Tm β†’ Tm
πœ‹β‚€Β² tβ‚‚ = πœ‹β‚€[ 2 ] tβ‚‚

πœ‹β‚_ : Tm β†’ Tm
πœ‹β‚ t = πœ‹β‚[ 1 ] t

πœ‹β‚Β²_ : Tm β†’ Tm
πœ‹β‚Β² tβ‚‚ = πœ‹β‚[ 2 ] tβ‚‚

⇑_ : Tm β†’ Tm
⇑ t = ⇑[ 1 ] t

⇑²_ : Tm β†’ Tm
⇑² tβ‚‚ = ⇑[ 2 ] tβ‚‚

⇓_ : Tm β†’ Tm
⇓ t = ⇓[ 1 ] t

⇓²_ : Tm β†’ Tm
⇓² tβ‚‚ = ⇓[ 2 ] tβ‚‚


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


_β€œ_ : βˆ€{n m} {X : Set} β†’ Vec X n β†’ Vec X m β†’ Vec X (n + m)
βˆ…        β€œ ys = ys
(x β€˜ xs) β€œ ys = x β€˜ xs β€œ ys


foldr : βˆ€{n} {X : Set} (Y : β„• β†’ Set) β†’ (βˆ€{k} β†’ X β†’ Y k β†’ Y (suc k)) β†’ Y zero β†’ Vec X n β†’ Y n
foldr Y f yβ‚€ βˆ…        = yβ‚€
foldr Y f yβ‚€ (x β€˜ xs) = f x (foldr Y f yβ‚€ xs)

ixMap : βˆ€{n} {X Y : Set} β†’ (β„• β†’ X β†’ Y) β†’ Vec X n β†’ Vec Y n
ixMap {zero}  f βˆ…        = βˆ…
ixMap {suc n} f (x β€˜ xs) = f (suc n) x β€˜ ixMap f xs

ixZipWith : βˆ€{n} {X Y Z : Set} β†’ (β„• β†’ X β†’ Y β†’ Z) β†’ Vec X n β†’ Vec Y n β†’ Vec Z n
ixZipWith {zero}  f βˆ…        βˆ…        = βˆ…
ixZipWith {suc n} f (x β€˜ xs) (y β€˜ ys) = f (suc n) x y β€˜ ixZipWith f xs ys

map : βˆ€{n} {X Y : Set} β†’ (X β†’ Y) β†’ Vec X n β†’ Vec Y n
map f = ixMap (Ξ» _ x β†’ f x)

zipWith : βˆ€{n} {X Y Z : Set} β†’ (X β†’ Y β†’ Z) β†’ Vec X n β†’ Vec Y n β†’ Vec Z n
zipWith f = ixZipWith (Ξ» _ x y β†’ f x y)


Vars : β„• β†’ Set
Vars = Vec Var

Tms : β„• β†’ Set
Tms = Vec Tm


𝑣ⁿ_ : βˆ€{n} β†’ Vars n β†’ Tms n
𝑣ⁿ_ = map 𝑣_

πœ†βΏ_,_ : βˆ€{n} β†’ Vars n β†’ Tms n β†’ Tms n
πœ†βΏ_,_ = ixZipWith πœ†[_]_,_

_∘ⁿ_ : βˆ€{n} β†’ Tms n β†’ Tms n β†’ Tms n
_∘ⁿ_ = ixZipWith (Ξ» n t s β†’ t ∘[ n ] s)

π‘βΏβŸ¨_,_⟩ : βˆ€{n} β†’ Tms n β†’ Tms n β†’ Tms n
π‘βΏβŸ¨_,_⟩ = ixZipWith 𝑝[_]⟨_,_⟩

πœ‹β‚€βΏ_ : βˆ€{n} β†’ Tms n β†’ Tms n
πœ‹β‚€βΏ_ = ixMap πœ‹β‚€[_]_

πœ‹β‚βΏ_ : βˆ€{n} β†’ Tms n β†’ Tms n
πœ‹β‚βΏ_ = ixMap πœ‹β‚[_]_

⇑ⁿ_ : βˆ€{n} β†’ Tms n β†’ Tms n
⇑ⁿ_ = ixMap ⇑[_]_

⇓ⁿ_ : βˆ€{n} β†’ Tms n β†’ Tms n
⇓ⁿ_ = ixMap ⇓[_]_


record Hyp : Set where
  constructor H[_]_∷_
  field
    n  : β„•
    ts : Tms n
    A  : Ty

data Cx : β„• β†’ Set where
  βˆ…   : Cx zero
  _,_ : βˆ€{m} β†’ Cx m β†’ Hyp β†’ Cx (suc m)

data _∈_  : βˆ€{m} β†’ Hyp β†’ Cx m β†’ Set where
  Z  : βˆ€{m} {Ξ“ : Cx m} {h : Hyp}  β†’ h ∈ (Ξ“ , h)
  S_ : βˆ€{m} {Ξ“ : Cx m} {h hβ€² : Hyp}  β†’ h ∈ Ξ“  β†’ h ∈ (Ξ“ , hβ€²)


data _⊒_∷_ {m : β„•} (Ξ“ : Cx m) : βˆ€{n} β†’ Tms n β†’ Ty β†’ Set where
  M𝑣_ : βˆ€{n A} {ts : Tms n}  β†’ (H[ n ] ts ∷ A) ∈ Ξ“
                             β†’ Ξ“ ⊒ ts ∷ A

  Mπœ† : βˆ€{n A B} {xs : Vars n} {ts : Tms n}  β†’ Ξ“ , H[ n ] 𝑣ⁿ xs ∷ A ⊒ ts ∷ B
                                            β†’ Ξ“ ⊒ πœ†βΏ xs , ts ∷ A βŠƒ B

  M∘ : βˆ€{n A B} {ts ss : Tms n}  β†’ Ξ“ ⊒ ts ∷ A βŠƒ B  β†’ Ξ“ ⊒ ss ∷ A
                                 β†’ Ξ“ ⊒ ts ∘ⁿ ss ∷ B

  M𝑝 : βˆ€{n A B} {ts ss : Tms n}  β†’ Ξ“ ⊒ ts ∷ A  β†’ Ξ“ ⊒ ss ∷ B
                                 β†’ Ξ“ ⊒ π‘βΏβŸ¨ ts , ss ⟩ ∷ A ∧ B

  Mπœ‹β‚€ : βˆ€{n A B} {ts : Tms n}  β†’ Ξ“ ⊒ ts ∷ A ∧ B
                               β†’ Ξ“ ⊒ πœ‹β‚€βΏ ts ∷ A

  Mπœ‹β‚ : βˆ€{n A B} {ts : Tms n}  β†’ Ξ“ ⊒ ts ∷ A ∧ B
                               β†’ Ξ“ ⊒ πœ‹β‚βΏ ts ∷ B

  M⇑ : βˆ€{n A u} {ts : Tms n}  β†’ Ξ“ ⊒ ts ∷ u ∢ A
                              β†’ Ξ“ ⊒ ⇑ⁿ ts ∷ ! u ∢ u ∢ A

  M⇓ : βˆ€{n A u} {ts : Tms n}  β†’ Ξ“ ⊒ ts ∷ u ∢ A
                              β†’ Ξ“ ⊒ ⇓ⁿ ts ∷ A

  M⁻ : βˆ€{n A u} {ts : Tms n}  β†’ Ξ“ ⊒ ts ∷ u ∢ A
                              β†’ Ξ“ ⊒ ts β€œ (u β€˜ βˆ…) ∷ A

  M⁺ : βˆ€{n A u} {ts : Tms n}  β†’ Ξ“ ⊒ ts β€œ (u β€˜ βˆ…) ∷ A
                              β†’ Ξ“ ⊒ ts ∷ u ∢ A


⊩_ : Ty β†’ Set
⊩ A = βˆ€{m} {Ξ“ : Cx m} β†’ Ξ“ ⊒ βˆ… ∷ A

⊩_∷_ : Tm β†’ Ty β†’ Set
⊩ t ∷ A = βˆ€{m} {Ξ“ : Cx m} β†’ Ξ“ ⊒ t β€˜ βˆ… ∷ A

⊩_∷_∷_ : Tm β†’ Tm β†’ Ty β†’ Set
⊩ tβ‚‚ ∷ t ∷ A = βˆ€{m} {Ξ“ : Cx m} β†’ Ξ“ ⊒ tβ‚‚ β€˜ t β€˜ βˆ… ∷ A


eI⁰ : βˆ€{A}
    β†’ ⊩ A βŠƒ A
eI⁰ = Mπœ† (M𝑣 Z)

eIΒΉ : βˆ€{A x}
    β†’ ⊩ πœ† x , 𝑣 x
      ∷ A βŠƒ A
eIΒΉ = Mπœ† (M𝑣 Z)

eIΒ² : βˆ€{A x u}
    β†’ ⊩ πœ†Β² u , 𝑣 u
      ∷ πœ† x , 𝑣 x
      ∷ A βŠƒ A
eIΒ² = Mπœ† (M𝑣 Z)


eK⁰ : βˆ€{A B}
    β†’ ⊩ A βŠƒ B βŠƒ A
eK⁰ = Mπœ† (Mπœ† (M𝑣 S Z))

eKΒΉ : βˆ€{A B x y}
    β†’ ⊩ πœ† x , πœ† y , 𝑣 x
      ∷ A βŠƒ B βŠƒ A
eKΒΉ = Mπœ† (Mπœ† (M𝑣 S Z))

eKΒ² : βˆ€{A B x y u v}
    β†’ ⊩ πœ†Β² u , πœ†Β² v , 𝑣 u
      ∷ πœ† x , πœ† y , 𝑣 x
      ∷ A βŠƒ B βŠƒ A
eKΒ² = Mπœ† (Mπœ† (M𝑣 S Z))


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

eSΒΉ : βˆ€{A B C f g x}
    β†’ ⊩ πœ† f , πœ† g , πœ† x , (𝑣 f ∘ 𝑣 x) ∘ (𝑣 g ∘ 𝑣 x)
      ∷ (A βŠƒ B βŠƒ C) βŠƒ (A βŠƒ B) βŠƒ A βŠƒ C
eSΒΉ = Mπœ† (Mπœ† (Mπœ† (M∘ (M∘ (M𝑣 S S Z)
                         (M𝑣 Z))
                     (M∘ (M𝑣 S Z)
                         (M𝑣 Z)))))

eSΒ² : βˆ€{A B C f g x p q u}
    β†’ ⊩ πœ†Β² p , πœ†Β² q , πœ†Β² u , (𝑣 p ∘² 𝑣 u) ∘² (𝑣 q ∘² 𝑣 u)
      ∷ πœ† f , πœ† g , πœ† x , (𝑣 f ∘ 𝑣 x) ∘ (𝑣 g ∘ 𝑣 x)
      ∷ (A βŠƒ B βŠƒ C) βŠƒ (A βŠƒ B) βŠƒ A βŠƒ C
eSΒ² = Mπœ† (Mπœ† (Mπœ† (M∘ (M∘ (M𝑣 S S Z)
                         (M𝑣 Z))
                     (M∘ (M𝑣 S Z)
                         (M𝑣 Z)))))


e11 : βˆ€{A x y}
    β†’ ⊩ πœ† y , ⇓ 𝑣 y
      ∷ x ∢ A βŠƒ A
e11 = Mπœ† (M⇓ (M𝑣 Z))

e12 : βˆ€{A x y}
    β†’ ⊩ πœ† y , ⇑ 𝑣 y
      ∷ x ∢ A βŠƒ ! x ∢ x ∢ A
e12 = Mπœ† (M⇑ (M𝑣 Z))

e13 : βˆ€{A B x y u v}
    β†’ ⊩ πœ†Β² u , πœ†Β² v , π‘Β²βŸ¨ 𝑣 u , 𝑣 v ⟩
      ∷ πœ† x , πœ† y , π‘βŸ¨ 𝑣 x , 𝑣 y ⟩
      ∷ A βŠƒ B βŠƒ A ∧ B
e13 = Mπœ† (Mπœ† (M𝑝 (M𝑣 S Z)
                 (M𝑣 Z)))

e14 : βˆ€{A B x y u v}
    β†’ ⊩ πœ† u , πœ† v , ⇑ π‘Β²βŸ¨ 𝑣 u , 𝑣 v ⟩
      ∷ x ∢ A βŠƒ y ∢ B βŠƒ ! π‘βŸ¨ x , y ⟩ ∢ π‘βŸ¨ x , y ⟩ ∢ (A ∧ B)
e14 = Mπœ† (Mπœ† (M⇑ (M⁺ (M𝑝 (M⁻ (M𝑣 S Z))
                         (M⁻ (M𝑣 Z))))))


t0 : βˆ€{A B x y u v}
   β†’ ⊩ πœ† u , πœ† v , π‘Β²βŸ¨ 𝑣 u , 𝑣 v ⟩
     ∷ x ∢ A βŠƒ y ∢ B βŠƒ π‘βŸ¨ x , y ⟩ ∢ (A ∧ B)
t0 = Mπœ† (Mπœ† (M⁺ (M𝑝 (M⁻ (M𝑣 S Z))
                    (M⁻ (M𝑣 Z)))))

t1 : βˆ€{A B x y u}
   β†’ ⊩ πœ† u , π‘Β²βŸ¨ πœ‹β‚€ 𝑣 u , πœ‹β‚ 𝑣 u ⟩
     ∷ x ∢ A ∧ y ∢ B βŠƒ π‘βŸ¨ x , y ⟩ ∢ (A ∧ B)
t1 = Mπœ† (M⁺ (M𝑝 (M⁻ (Mπœ‹β‚€ (M𝑣 Z)))
                (M⁻ (Mπœ‹β‚ (M𝑣 Z)))))

t2 : βˆ€{A B x y u}
   β†’ ⊩ πœ† u , ⇑ π‘Β²βŸ¨ πœ‹β‚€ 𝑣 u , πœ‹β‚ 𝑣 u ⟩
     ∷ x ∢ A ∧ y ∢ B βŠƒ ! π‘βŸ¨ x , y ⟩ ∢ π‘βŸ¨ x , y ⟩ ∢ (A ∧ B)
t2 = Mπœ† (M⇑ (M⁺ (M𝑝 (M⁻ (Mπœ‹β‚€ (M𝑣 Z)))
                    (M⁻ (Mπœ‹β‚ (M𝑣 Z))))))


axK : βˆ€{A B f x p u}
    β†’ ⊩ πœ† p , πœ† u , 𝑣 p ∘² 𝑣 u
      ∷ f ∢ (A βŠƒ B) βŠƒ x ∢ A βŠƒ (f ∘ x) ∢ B
axK = Mπœ† (Mπœ† (M⁺ (M∘ (M⁻ (M𝑣 S Z))
                     (M⁻ (M𝑣 Z)))))

axT : βˆ€{A x u}
    β†’ ⊩ πœ† u , ⇓ 𝑣 u
      ∷ x ∢ A βŠƒ A
axT = e11

ax4 : βˆ€{A x u}
    β†’ ⊩ πœ† u , ⇑ 𝑣 u
      ∷ x ∢ A βŠƒ ! x ∢ x ∢ A
ax4 = e12


e2 : βˆ€{A x₃ xβ‚‚ x₁}
   β†’ ⊩ πœ†Β² x₃ , ⇓² ⇑² 𝑣 x₃
     ∷ πœ† xβ‚‚ , ⇓ ⇑ 𝑣 xβ‚‚
     ∷ x₁ ∢ A βŠƒ x₁ ∢ A
e2 = Mπœ† (M⇓ (M⇑ (M𝑣 Z)))

e2β€² : βˆ€{A x₃ xβ‚‚ x₁}
    β†’ ⊩ πœ†Β² x₃ , 𝑣 x₃
      ∷ πœ† xβ‚‚ , 𝑣 xβ‚‚
      ∷ x₁ ∢ A βŠƒ x₁ ∢ A
e2β€² = Mπœ† (M𝑣 Z)


_⊒_ : βˆ€{m} (Ξ“ : Cx m) (h : Hyp) β†’ Set
Ξ“ ⊒ (H[ n ] ts ∷ A) = Ξ“ ⊒ ts ∷ A


data _≲_ : βˆ€{m mβ€²} β†’ Cx m β†’ Cx mβ€² β†’ Set where
  base : βˆ… ≲ βˆ…
  keep : βˆ€{m mβ€² h} {Ξ“ : Cx m} {Ξ“β€² : Cx mβ€²}  β†’ Ξ“ ≲ Ξ“β€²  β†’ (Ξ“ , h) ≲ (Ξ“β€² , h)
  drop : βˆ€{m mβ€² h} {Ξ“ : Cx m} {Ξ“β€² : Cx mβ€²}  β†’ Ξ“ ≲ Ξ“β€²  β†’ Ξ“ ≲ (Ξ“β€² , h)

βˆ…β‰²Ξ“ : βˆ€{m} {Ξ“ : Cx m} β†’ βˆ… ≲ Ξ“
βˆ…β‰²Ξ“ {Ξ“ = βˆ…}     = base
βˆ…β‰²Ξ“ {Ξ“ = Ξ“ , h} = drop βˆ…β‰²Ξ“

Γ≲Γ : βˆ€{m} {Ξ“ : Cx m} β†’ Ξ“ ≲ Ξ“
Γ≲Γ {Ξ“ = βˆ…}     = base
Γ≲Γ {Ξ“ = Ξ“ , h} = keep Γ≲Γ

wk∈ : βˆ€{m mβ€² h} {Ξ“ : Cx m} {Ξ“β€² : Cx mβ€²}  β†’ Ξ“ ≲ Ξ“β€²  β†’ h ∈ Ξ“  β†’ h ∈ Ξ“β€²
wk∈ base     ()
wk∈ (keep p) Z     = Z
wk∈ (keep p) (S i) = S wk∈ p i
wk∈ (drop p) i     = S wk∈ p i

wk⊒ : βˆ€{m mβ€² h} {Ξ“ : Cx m} {Ξ“β€² : Cx mβ€²}  β†’ Ξ“ ≲ Ξ“β€²  β†’ Ξ“ ⊒ h  β†’ Ξ“β€² ⊒ h
wk⊒ p (M𝑣 i)    = M𝑣 (wk∈ p i)
wk⊒ p (Mπœ† d)    = Mπœ† (wk⊒ (keep p) d)
wk⊒ p (M∘ d dβ€²) = M∘ (wk⊒ p d) (wk⊒ p dβ€²)
wk⊒ p (M𝑝 d dβ€²) = M𝑝 (wk⊒ p d) (wk⊒ p dβ€²)
wk⊒ p (Mπœ‹β‚€ d)   = Mπœ‹β‚€ (wk⊒ p d)
wk⊒ p (Mπœ‹β‚ d)   = Mπœ‹β‚ (wk⊒ p d)
wk⊒ p (M⇑ d)    = M⇑ (wk⊒ p d)
wk⊒ p (M⇓ d)    = M⇓ (wk⊒ p d)
wk⊒ p (M⁻ d)    = M⁻ (wk⊒ p d)
wk⊒ p (M⁺ d)    = M⁺ (wk⊒ p d)


data _≳_ : βˆ€{m mβ€²} β†’ Cx m β†’ Cx mβ€² β†’ Set where
  base : βˆ… ≳ βˆ…
  once : βˆ€{m mβ€² h} {Ξ“ : Cx m} {Ξ“β€² : Cx mβ€²}  β†’ Ξ“ ≳ Ξ“β€²  β†’ (Ξ“ , h) ≳ (Ξ“β€² , h)
  more : βˆ€{m mβ€² h} {Ξ“ : Cx m} {Ξ“β€² : Cx mβ€²}  β†’ Ξ“ ≳ Ξ“β€²  β†’ (Ξ“ , h , h) ≳ (Ξ“β€² , h)

cn∈ : βˆ€{m mβ€² h} {Ξ“ : Cx m} {Ξ“β€² : Cx mβ€²}  β†’ Ξ“ ≳ Ξ“β€²  β†’ h ∈ Ξ“  β†’ h ∈ Ξ“β€²
cn∈ base     ()
cn∈ (once p) Z     = Z
cn∈ (once p) (S i) = S cn∈ p i
cn∈ (more p) Z     = Z
cn∈ (more p) (S i) = cn∈ (once p) i

cn⊒ : βˆ€{m mβ€² h} {Ξ“ : Cx m} {Ξ“β€² : Cx mβ€²}  β†’ Ξ“ ≳ Ξ“β€²  β†’ Ξ“ ⊒ h  β†’ Ξ“β€² ⊒ h
cn⊒ p (M𝑣 i)    = M𝑣 (cn∈ p i)
cn⊒ p (Mπœ† d)    = Mπœ† (cn⊒ (once p) d)
cn⊒ p (M∘ d dβ€²) = M∘ (cn⊒ p d) (cn⊒ p dβ€²)
cn⊒ p (M𝑝 d dβ€²) = M𝑝 (cn⊒ p d) (cn⊒ p dβ€²)
cn⊒ p (Mπœ‹β‚€ d)   = Mπœ‹β‚€ (cn⊒ p d)
cn⊒ p (Mπœ‹β‚ d)   = Mπœ‹β‚ (cn⊒ p d)
cn⊒ p (M⇑ d)    = M⇑ (cn⊒ p d)
cn⊒ p (M⇓ d)    = M⇓ (cn⊒ p d)
cn⊒ p (M⁻ d)    = M⁻ (cn⊒ p d)
cn⊒ p (M⁺ d)    = M⁺ (cn⊒ p d)


data _β‰ˆ_ : βˆ€{m} β†’ Cx m β†’ Cx m β†’ Set where
  base : βˆ… β‰ˆ βˆ…
  just : βˆ€{m h} {Ξ“ Ξ“β€² : Cx m}  β†’ Ξ“ β‰ˆ Ξ“β€²  β†’ (Ξ“ , h) β‰ˆ (Ξ“β€² , h)
  same : βˆ€{m h hβ€²}  {Ξ“ Ξ“β€² : Cx m}  β†’ Ξ“ β‰ˆ Ξ“β€²  β†’ (Ξ“ , h , hβ€²) β‰ˆ (Ξ“β€² , h , hβ€²)
  diff : βˆ€{m h hβ€²}  {Ξ“ Ξ“β€² : Cx m}  β†’ Ξ“ β‰ˆ Ξ“β€²  β†’ (Ξ“ , hβ€² , h) β‰ˆ (Ξ“β€² , h , hβ€²)

ex∈ : βˆ€{m h} {Ξ“ Ξ“β€² : Cx m}  β†’ Ξ“ β‰ˆ Ξ“β€²  β†’ h ∈ Ξ“  β†’ h ∈ Ξ“β€²
ex∈ base     ()
ex∈ (just p) Z         = Z
ex∈ (just p) (S i)     = S ex∈ p i
ex∈ (same p) Z         = Z
ex∈ (same p) (S Z)     = S Z
ex∈ (same p) (S (S i)) = S (S ex∈ p i)
ex∈ (diff p) Z         = S Z
ex∈ (diff p) (S Z)     = Z
ex∈ (diff p) (S (S i)) = S (S ex∈ p i)

ex⊒ : βˆ€{m h} {Ξ“ Ξ“β€² : Cx m}  β†’ Ξ“ β‰ˆ Ξ“β€²  β†’ Ξ“ ⊒ h  β†’ Ξ“β€² ⊒ h
ex⊒ p (M𝑣 i)    = M𝑣 (ex∈ p i)
ex⊒ p (Mπœ† d)    = Mπœ† (ex⊒ (just p) d)
ex⊒ p (M∘ d dβ€²) = M∘ (ex⊒ p d) (ex⊒ p dβ€²)
ex⊒ p (M𝑝 d dβ€²) = M𝑝 (ex⊒ p d) (ex⊒ p dβ€²)
ex⊒ p (Mπœ‹β‚€ d)   = Mπœ‹β‚€ (ex⊒ p d)
ex⊒ p (Mπœ‹β‚ d)   = Mπœ‹β‚ (ex⊒ p d)
ex⊒ p (M⇑ d)    = M⇑ (ex⊒ p d)
ex⊒ p (M⇓ d)    = M⇓ (ex⊒ p d)
ex⊒ p (M⁻ d)    = M⁻ (ex⊒ p d)
ex⊒ p (M⁺ d)    = M⁺ (ex⊒ p d)


postulate fresh : Var  -- XXX: Fix this!


toVec : βˆ€{m} β†’ Cx m β†’ Vec Hyp m
toVec βˆ…       = βˆ…
toVec (Ξ“ , h) = h β€˜ toVec Ξ“

fromVec : βˆ€{m} β†’ Vec Hyp m β†’ Cx m
fromVec βˆ…        = βˆ…
fromVec (h β€˜ hs) = fromVec hs , h

prefixHyp : Tm β†’ Hyp β†’ Hyp
prefixHyp t (H[ n ] ts ∷ A) = H[ suc n ] (t β€˜ ts) ∷ A

prefixHyps : βˆ€{m} β†’ Tms m β†’ Cx m β†’ Cx m
prefixHyps ts Ξ“ = fromVec (zipWith prefixHyp ts (toVec Ξ“))


in∈ : βˆ€{m h} {vs : Vars m} {Ξ“ : Cx m}
    β†’ h ∈ Ξ“  β†’ Ξ£ Var (Ξ» x β†’ prefixHyp (𝑣 x) h ∈ Ξ“)
in∈ {vs = βˆ…}      ()
in∈ {vs = x β€˜ vs} Z     = {!⟨ x , Z ⟩!}
in∈ {vs = x β€˜ vs} (S i) = {!!}

in⊒ : βˆ€{m h} {vs : Vars m} {Ξ“ : Cx m}
    β†’ Ξ“ ⊒ h  β†’ Ξ£ (Vars m β†’ Tm) (Ξ» t β†’ prefixHyps (map 𝑣_ vs) Ξ“ ⊒ prefixHyp (t vs) h)
in⊒ d = {!!}

nec : βˆ€{h}  β†’ βˆ… ⊒ h  β†’ Ξ£ Tm (Ξ» t β†’ βˆ… ⊒ prefixHyp t h)
nec d = let ⟨ s , c ⟩ = in⊒ d in ⟨ s βˆ… , c ⟩