{-# OPTIONS --universe-polymorphism #-}
module NaPa.LogicalRelation where

-- nearly identical to NaPa.LogicalRelation.Bijection

open import Level
open import Abstractor
open import Irrelevance
open import Data.Nat.NP hiding (_⊔_) renaming (_+_ to _+ℕ_; _≤_ to _≤ℕ_; _≤?_ to _≤?ℕ_; _<_ to _<ℕ_
                                              ;module == to ==ℕ; _==_ to _==ℕ_)
open import Data.Nat.Logical renaming (_≟_ to _≟ℕ_)
open import Data.Nat.Properties as Nat
open import Data.Empty
open import Data.Unit
open import Data.Maybe.NP
open import Data.Bool.Extras
open import Data.Sum.NP
open import Data.Product.Extras
import Relation.Binary.PropositionalEquality as ≡
open ≡ using (_≡_)
open ≡.≡-Reasoning
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary.Extras
open import Relation.Binary.Logical
open import Function
open import Function.Equality as ⟶≡ using (_⟶_; _⟨$⟩_)
open import Function.Injection.NP using (Injection; Injective; module
    Injection; _∈_)
open import NaPa hiding (_∈_)

private
  module Inj = Injection
  module ℕs = Setoid ⟦ℕ⟧-setoid
  module ==ℕs = Setoid ==ℕ.setoid
  module ℕe = Equality ⟦ℕ⟧-equality

_⟨$⟩ᵢ_ : ∀ {f₁ f₂ t₁ t₂}
           {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
         → Injection From To → Setoid.Carrier From → Setoid.Carrier To
_⟨$⟩ᵢ_ = ⟶≡._⟨$⟩_ ∘ Inj.to -- inj x = Inj.to inj ⟨$⟩ x

==ℕ-dec : ∀ x y → ⟦Bool⟧ ⌊ x ≟ℕ y ⌋ (x ==ℕ y)
==ℕ-dec x y with x ≟ℕ y
... | yes p = ⟦true⟧′  (==ℕs.reflexive (ℕe.to-propositional p))
... | no ¬p = ⟦false⟧′ (T'¬'not (¬p ∘ ℕs.reflexive ∘ ==ℕ.sound _ _))

⟦dec⟧ : ∀ {P Q : Set} (decP : Dec P) (decQ : Dec Q) → (P → Q) → (Q → P) → ⟦Bool⟧ ⌊ decP ⌋ ⌊ decQ ⌋
⟦dec⟧ (yes _) (yes _) _ _ = ⟦true⟧
⟦dec⟧ (no  _) (no  _) _ _ = ⟦false⟧
⟦dec⟧ (yes p) (no ¬q) f _ = ⊥-elim (¬q (f p))
⟦dec⟧ (no ¬p) (yes q) _ g = ⊥-elim (¬p (g q))

⟦World⟧ : (α₁ α₂ : World) → Set
⟦World⟧ = Injection on Nm

-- dup with NotSoFresh.LogicalRelation
⟦WorldPred⟧ : (P₁ P₂ : Pred zero World) → Set₁
⟦WorldPred⟧ = ⟦Pred⟧ _ ⟦World⟧

⟦WorldRel⟧ : (R₁ R₂ : Rel World zero) → Set₁
⟦WorldRel⟧ = ⟦Rel⟧ ⟦World⟧ zero

_⟦↑1⟧ : (⟦World⟧ ⟦→⟧ ⟦World⟧) _↑1 _↑1
_⟦↑1⟧ {α₁} {α₂} αᵣ = record { to = to; injective = to-inj } where
  to : Nm (α₁ ↑1) ⟶ Nm (α₂ ↑1)
  to = Name→-to-Nm⟶ (lift↑1 (_⟨$⟩ᵢ_ αᵣ))
  to-inj : Injective to
  to-inj {zero  , _} {zero  , _} zero    = zero
  to-inj {suc _ , _} {suc _ , _} (suc e) = suc (Inj.injective αᵣ e)
  to-inj {suc _ , _} {zero  , _} ()
  to-inj {zero  , _} {suc _ , _} ()

_⟦+1⟧ : (⟦World⟧ ⟦→⟧ ⟦World⟧) _+1 _+1
_⟦+1⟧ {α₁} {α₂} αᵣ = record { to = to; injective = inj } where
  to : Nm (α₁ +1) ⟶ Nm (α₂ +1)
  to = Name→-to-Nm⟶ (λ x → su (αᵣ ⟨$⟩ᵢ (predNm x)))
  inj : Injective to
  inj {zero  , _} {zero  , _} _       = zero
  inj {suc _ , _} {suc _ , _} (suc e) = suc (Inj.injective αᵣ e)
  inj {suc _ , _} {zero  , ()} _
  inj {zero  , ()} {suc _ , _} _

_⟦↑_⟧ : (⟦World⟧ ⟦→⟧ ⟦ℕ⟧ ⟦→⟧ ⟦World⟧) _↑_ _↑_
_⟦↑_⟧ αᵣ zero    = αᵣ
_⟦↑_⟧ αᵣ (suc k) = αᵣ ⟦↑ k ⟧ ⟦↑1⟧

_⟦+_⟧ : (⟦World⟧ ⟦→⟧ ⟦ℕ⟧ ⟦→⟧ ⟦World⟧) _+[_] _+[_]
_⟦+_⟧ αᵣ zero    = αᵣ
_⟦+_⟧ αᵣ (suc k) = αᵣ ⟦+ k ⟧ ⟦+1⟧

⟦Name⟧ : ⟦Pred⟧ zero ⟦World⟧ Name Name
⟦Name⟧ αᵣ x₁ x₂ = ( x₁ , x₂ ) ∈ αᵣ

⟦Name⟧≡ : ⟦WorldPred⟧ Name Name
⟦Name⟧≡ αᵣ x₁ x₂ = αᵣ ⟨$⟩ᵢ x₁ ≡ x₂

⟦ø⟧ : ⟦World⟧ ø ø
⟦ø⟧ = record { to = Name→-to-Nm⟶ Nameø-elim
             ; injective = λ{x} → Nameø-elim x }

_⟦==nm⟧_ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟦Name⟧ αᵣ ⟦→⟧ ⟦Name⟧ αᵣ ⟦→⟧ ⟦Bool⟧) _==nm_ _==nm_
_⟦==nm⟧_ αᵣ {_} {x₂} xᵣ {_} {y₂} yᵣ = helper (≡nm⇒≡ {_} {_} {x₂} xᵣ) (≡nm⇒≡ {_} {_} {y₂} yᵣ) where
  helper : (⟦Name⟧≡ αᵣ ⟦→⟧ ⟦Name⟧≡ αᵣ ⟦→⟧ ⟦Bool⟧) _==nm_ _==nm_
  helper {x} ≡.refl {y} ≡.refl =
       x ==nm y      ≈⟨ sym (==ℕ-dec _ _) ⟩
       ⌊ x ≟nm y ⌋   ≈⟨ ⟦dec⟧ (x ≟nm y) (x′ ≟nm y′) (⟶≡.cong (Inj.to αᵣ)) (Inj.injective αᵣ) ⟩
       ⌊ x′ ≟nm y′ ⌋ ≈⟨ ==ℕ-dec _ _ ⟩∎
       x′ ==nm y′ ∎
    where
      x′ = αᵣ ⟨$⟩ᵢ x
      y′ = αᵣ ⟨$⟩ᵢ y
      open ⟦Bool⟧-Props using (sym)
      open ⟦Bool⟧-Reasoning

⟦ze⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟦Name⟧ (αᵣ ⟦↑1⟧)) ze ze
⟦ze⟧ _ = zero

⟦su⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟦Name⟧ αᵣ ⟦→⟧ ⟦Name⟧ (αᵣ ⟦+1⟧)) su su
⟦su⟧ _ = suc

⟦su↑⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟦Name⟧ αᵣ ⟦→⟧ ⟦Name⟧ (αᵣ ⟦↑1⟧)) su↑ su↑
⟦su↑⟧ _ = suc

⟦predNm⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟦Name⟧ (αᵣ ⟦+1⟧) ⟦→⟧ ⟦Name⟧ αᵣ) predNm predNm
⟦predNm⟧ _ = ⟦ℕ⟧-cong (λ x → x ∸ 1)

⟦+nm⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟦Name⟧ αᵣ ⟦→⟧ (⟨ kᵣ ∶ ⟦ℕ⟧ ⟩⟦→⟧ ⟦Name⟧ (αᵣ ⟦+ kᵣ ⟧))) _+nm_ _+nm_
⟦+nm⟧ _ x zero = x
⟦+nm⟧ {α₁} {α₂} αᵣ {x₁} {x₂} x (suc {k₁} {k₂} kᵣ)
   = ℕ.suc (name (αᵣ ⟦+ kᵣ ⟧ ⟨$⟩ᵢ (k₁ +ℕ name x₁ , _{-p-})))
   ≈⟨ ≡nm-⟦ℕ⟧-cong (λ x → suc (name (αᵣ ⟦+ kᵣ ⟧ ⟨$⟩ᵢ x))) ℕe.refl ⟩
     suc (name (αᵣ ⟦+ kᵣ ⟧ ⟨$⟩ᵢ (k₁ +ℕ name x₁ , _{-q-})))
   ≈⟨ suc (⟦+nm⟧ αᵣ {x₁} {x₂} x kᵣ) ⟩∎
     suc (k₂ +ℕ name x₂)
   ∎ where open ⟦ℕ⟧-Reasoning

⟦subtract⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟨ kᵣ ∶ ⟦ℕ⟧ ⟩⟦→⟧ ⟦Name⟧ (αᵣ ⟦+ kᵣ ⟧) ⟦→⟧ ⟦Name⟧ αᵣ) subtract subtract
⟦subtract⟧ _ zero x = x
⟦subtract⟧ {α₁} {α₂} αᵣ (suc {k₁} {k₂} kᵣ) {x₁} {x₂} xᵣ
   = name (αᵣ ⟨$⟩ᵢ (name x₁ ∸ suc k₁ , _{-p-}))
   ≈⟨ ≡-⟦ℕ⟧-cong (λ x → name (αᵣ ⟨$⟩ᵢ x)) (name-injective (≡.sym (∸-+-assoc (name x₁) 1 k₁))) ⟩
      name (αᵣ ⟨$⟩ᵢ (name x₁ ∸ 1 ∸ k₁ , _{-r-}))
   ≈⟨ ⟦subtract⟧ αᵣ kᵣ {predNm x₁} {predNm x₂} (⟦predNm⟧ (αᵣ ⟦+ kᵣ ⟧) {x₁} {x₂} xᵣ)  ⟩
      (name x₂ ∸ 1) ∸ k₂
   ≈⟨ ℕe.reflexive (∸-+-assoc (name x₂) 1 k₂) ⟩∎
      name x₂ ∸ suc k₂
   ∎ where open ⟦ℕ⟧-Reasoning

⟦>nm-bool⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟨ kᵣ ∶ ⟦ℕ⟧ ⟩⟦→⟧ ⟦Name⟧ (αᵣ ⟦↑ kᵣ ⟧) ⟦→⟧ ⟦Bool⟧) >nm-bool >nm-bool
⟦>nm-bool⟧ αᵣ kᵣ {x₁} {x₂} xᵣ = helper kᵣ {x₁} {x₂} (≡nm⇒≡ xᵣ) where
  helper : (⟨ kᵣ ∶ ⟦ℕ⟧ ⟩⟦→⟧ ⟦Name⟧≡ (αᵣ ⟦↑ kᵣ ⟧) ⟦→⟧ ⟦Bool⟧) >nm-bool >nm-bool
  helper zero                   ≡.refl  = ⟦false⟧
  helper (suc kᵣ) {zero  , _ }  ≡.refl  = ⟦true⟧
  helper (suc kᵣ) {suc x , pf₁} ≡.refl  = helper kᵣ {x , pf₁} ≡.refl

⟦easy->nm⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟨ kᵣ ∶ ⟦ℕ⟧ ⟩⟦→⟧
                  ⟦Name⟧ (αᵣ ⟦↑ kᵣ ⟧) ⟦→⟧ ⟦Name⟧ (⟦ø⟧ ⟦↑ kᵣ ⟧) ⟦⊎⟧ ⟦Name⟧ (αᵣ ⟦+ kᵣ ⟧)
             ) easy->nm easy->nm
⟦easy->nm⟧ αᵣ kᵣ {x₁} {x₂} xᵣ = helper kᵣ {x₁} {x₂} (≡nm⇒≡ xᵣ) where
  helper : (⟨ kᵣ ∶ ⟦ℕ⟧ ⟩⟦→⟧ ⟦Name⟧≡ (αᵣ ⟦↑ kᵣ ⟧) ⟦→⟧ ⟦Name⟧ (⟦ø⟧ ⟦↑ kᵣ ⟧) ⟦⊎⟧ ⟦Name⟧ (αᵣ ⟦+ kᵣ ⟧)) easy->nm easy->nm
  helper zero                             ≡.refl = inj₂ (≡nm-⟦ℕ⟧-cong (λ x → name (αᵣ ⟨$⟩ᵢ x)) ℕe.refl)
  helper (suc kᵣ)           {zero  , _ }  ≡.refl = inj₁ zero
  helper (suc {k₁} {k₂} kᵣ) {suc x , pf₁} ≡.refl
    = ⟦map⟧ _ _ _ _ suc suc (helper kᵣ {x , pf₁} ≡.refl)

⟦>nm⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟨ kᵣ ∶ ⟦ℕ⟧ ⟩⟦→⟧
                  ⟦Name⟧ (αᵣ ⟦↑ kᵣ ⟧) ⟦→⟧ ⟦Name⟧ (⟦ø⟧ ⟦↑ kᵣ ⟧) ⟦⊎⟧ ⟦Name⟧ (αᵣ ⟦+ kᵣ ⟧)
         ) >nm >nm
⟦>nm⟧ {α₁} {α₂} αᵣ {k₁} {k₂} kᵣ {x₁} {x₂} xᵣ =
   ≡.subst (λ x → (⟦Name⟧ (⟦ø⟧ ⟦↑ kᵣ ⟧) ⟦⊎⟧ ⟦Name⟧ (αᵣ ⟦+ kᵣ ⟧)) (>nm {α₁} k₁ x₁) x)
           (easy->nm≗>nm {α₂} k₂ x₂)
           (≡.subst (λ x → (⟦Name⟧ (⟦ø⟧ ⟦↑ kᵣ ⟧) ⟦⊎⟧ ⟦Name⟧ (αᵣ ⟦+ kᵣ ⟧)) x
                    (easy->nm {α₂} k₂ x₂))
                    (easy->nm≗>nm {α₁} k₁ x₁) (⟦easy->nm⟧ αᵣ kᵣ {x₁} {x₂} xᵣ))

⟦lift↑1⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ βᵣ ∶ ⟦World⟧ ⟩⟦→⟧
           (⟦Name⟧ αᵣ ⟦→⟧ ⟦Name⟧ βᵣ) ⟦→⟧ (⟦Name⟧ (αᵣ ⟦↑1⟧) ⟦→⟧ ⟦Name⟧ (βᵣ ⟦↑1⟧))) lift↑1 lift↑1
⟦lift↑1⟧ {α₁} {α₂} αᵣ {β₁} {β₂} βᵣ {f₁} {f₂} fᵣ {x₁} {x₂} xᵣ = helper {x₁} {x₂} (≡nm⇒≡ xᵣ) where
   helper : (⟦Name⟧≡ (αᵣ ⟦↑1⟧) ⟦→⟧ ⟦Name⟧ (βᵣ ⟦↑1⟧)) (lift↑1 f₁) (lift↑1 f₂)
   helper {zero ,  _}  ≡.refl = zero
   helper {suc x , pf} ≡.refl = suc (fᵣ ℕe.refl)

_⟦⊆⟧b_ : ⟦WorldRel⟧ _⊆_ _⊆_
_⟦⊆⟧b_ αᵣ βᵣ α⊆β₁ α⊆β₂
  = (⟦Name⟧ αᵣ ⟦→⟧ ⟦Name⟧ βᵣ) (coe α⊆β₁) (coe α⊆β₂)

data _⟦⊆⟧_ {α₁ α₂} (αᵣ : ⟦World⟧ α₁ α₂) {β₁ β₂} (βᵣ : ⟦World⟧ β₁ β₂) (x : α₁ ⊆ β₁) (y : α₂ ⊆ β₂) : Set where
  mk⟦⊆⟧ : _⟦⊆⟧b_ αᵣ βᵣ x y → _⟦⊆⟧_ αᵣ βᵣ x y

un⟦⊆⟧ : ∀ {α₁ α₂} {αᵣ : ⟦World⟧ α₁ α₂} {β₁ β₂} {βᵣ : ⟦World⟧ β₁ β₂} {x : α₁ ⊆ β₁} {y : α₂ ⊆ β₂} →
  _⟦⊆⟧_ αᵣ βᵣ x y → _⟦⊆⟧b_ αᵣ βᵣ x y
un⟦⊆⟧ (mk⟦⊆⟧ x) {a} {b} c = x {a} {b} c

⟦⊆-refl⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ αᵣ ⟦⊆⟧ αᵣ) ⊆-refl ⊆-refl
⟦⊆-refl⟧ _ = mk⟦⊆⟧ (λ xᵣ → xᵣ)

⟦⊆-trans⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ βᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ γᵣ ∶ ⟦World⟧ ⟩⟦→⟧
                  αᵣ ⟦⊆⟧ βᵣ ⟦→⟧ (βᵣ ⟦⊆⟧ γᵣ ⟦→⟧ (αᵣ ⟦⊆⟧ γᵣ))) ⊆-trans ⊆-trans
⟦⊆-trans⟧ _ _ _ {_} {f₂} f g = mk⟦⊆⟧ (λ {x₁} {x₂} xᵣ → un⟦⊆⟧ g {_} {coe f₂ x₂} (un⟦⊆⟧ f {x₁} {x₂} xᵣ))

⟦coe⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ βᵣ ∶ ⟦World⟧ ⟩⟦→⟧ αᵣ ⟦⊆⟧ βᵣ ⟦→⟧ (⟦Name⟧ αᵣ ⟦→⟧ ⟦Name⟧ βᵣ)) coe coe
⟦coe⟧ _ _ α⊆βᵣ {x₁} {x₂} xᵣ = un⟦⊆⟧ α⊆βᵣ {x₁} {x₂} xᵣ

⟦¬Nameø⟧ : (⟦¬⟧(⟦Name⟧ ⟦ø⟧)) ¬Nameø ¬Nameø
⟦¬Nameø⟧ {_ , ()}

⟦⊆-cong-↑1⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ βᵣ ∶ ⟦World⟧ ⟩⟦→⟧ αᵣ ⟦⊆⟧ βᵣ ⟦→⟧ (αᵣ ⟦↑1⟧) ⟦⊆⟧ (βᵣ ⟦↑1⟧)) ⊆-cong-↑1 ⊆-cong-↑1
⟦⊆-cong-↑1⟧ αᵣ βᵣ {α⊆β₁} {α⊆β₂} α⊆βᵣ = mk⟦⊆⟧ (λ {x₁} {x₂} xᵣ → helper {x₁} {x₂} (≡nm⇒≡ xᵣ)) where
  helper : (⟦Name⟧≡ (αᵣ ⟦↑1⟧) ⟦→⟧ ⟦Name⟧ (βᵣ ⟦↑1⟧)) (coe (⊆-cong-↑1 α⊆β₁)) (coe (⊆-cong-↑1 α⊆β₂))
  helper {zero  , _} ≡.refl = zero
  helper {suc x , p} ≡.refl = suc (un⟦⊆⟧ α⊆βᵣ {x , p} {αᵣ ⟨$⟩ᵢ (x , p)} ℕe.refl)

⟦⊆-cong-+1⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ βᵣ ∶ ⟦World⟧ ⟩⟦→⟧ αᵣ ⟦⊆⟧ βᵣ ⟦→⟧ (αᵣ ⟦+1⟧) ⟦⊆⟧ (βᵣ ⟦+1⟧)) ⊆-cong-+1 ⊆-cong-+1
⟦⊆-cong-+1⟧ αᵣ βᵣ {α⊆β₁} {α⊆β₂} α⊆βᵣ = mk⟦⊆⟧ (λ {x₁} {x₂} xᵣ → helper {x₁} {x₂} (≡nm⇒≡ xᵣ)) where
  helper : (⟦Name⟧≡ (αᵣ ⟦+1⟧) ⟦→⟧ ⟦Name⟧ (βᵣ ⟦+1⟧)) (coe (⊆-cong-+1 α⊆β₁)) (coe (⊆-cong-+1 α⊆β₂))
  helper {zero  , ()} _
  helper {suc x , p} ≡.refl = suc (un⟦⊆⟧ α⊆βᵣ {x , p} {αᵣ ⟨$⟩ᵢ (x , p)} ℕe.refl)

⟦⊆-+1↑1⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ (αᵣ ⟦+1⟧) ⟦⊆⟧ (αᵣ ⟦↑1⟧)) ⊆-+1↑1 ⊆-+1↑1
⟦⊆-+1↑1⟧ αᵣ = mk⟦⊆⟧ (λ {x₁} {x₂} xᵣ → helper {x₁} {x₂} (≡nm⇒≡ xᵣ)) where
  helper : (⟦Name⟧≡ (αᵣ ⟦+1⟧) ⟦→⟧ ⟦Name⟧ (αᵣ ⟦↑1⟧)) (coe ⊆-+1↑1) (coe +1↑1)
  helper {zero  , ()} _
  helper {suc x , p} ≡.refl = suc ℕe.refl

⟦⊆-ø-bottom⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟦ø⟧ ⟦⊆⟧ αᵣ) ⊆-ø-bottom ⊆-ø-bottom
⟦⊆-ø-bottom⟧ αᵣ = mk⟦⊆⟧ (λ {η₁} {η₂} η → helper {η₁} {η₂} η) where
   helper : (⟦ø⟧ ⟦⊆⟧b αᵣ) ⊆-ø-bottom ⊆-ø-bottom
   helper {_ , ()}

⟦⊆-+1-inj⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ βᵣ ∶ ⟦World⟧ ⟩⟦→⟧ (αᵣ ⟦+1⟧) ⟦⊆⟧ (βᵣ ⟦+1⟧) ⟦→⟧ αᵣ ⟦⊆⟧ βᵣ) ⊆-+1-inj ⊆-+1-inj
⟦⊆-+1-inj⟧ _ _ α+⊆β+ᵣ = mk⟦⊆⟧ (λ {x₁} {x₂} xᵣ → ⟦ℕ⟧-cong (λ x → x ∸ 1) (un⟦⊆⟧ α+⊆β+ᵣ {su x₁} {su x₂} (suc xᵣ)))

⟦⊆-↑1-inj⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ βᵣ ∶ ⟦World⟧ ⟩⟦→⟧ (αᵣ ⟦↑1⟧) ⟦⊆⟧ (βᵣ ⟦↑1⟧) ⟦→⟧ αᵣ ⟦⊆⟧ βᵣ) ⊆-↑1-inj ⊆-↑1-inj
⟦⊆-↑1-inj⟧ _ _ α↑⊆β↑ᵣ = mk⟦⊆⟧ (λ {x₁} {x₂} xᵣ → ⟦ℕ⟧-cong (λ x → x ∸ 1) (un⟦⊆⟧ α↑⊆β↑ᵣ {su↑ x₁} {su↑ x₂} (suc xᵣ)))

⟦⊆-unctx-+1↑1⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ βᵣ ∶ ⟦World⟧ ⟩⟦→⟧ (αᵣ ⟦+1⟧) ⟦⊆⟧ (βᵣ ⟦↑1⟧) ⟦→⟧ αᵣ ⟦⊆⟧ βᵣ) ⊆-unctx-+1↑1 ⊆-unctx-+1↑1
⟦⊆-unctx-+1↑1⟧ _ _ α+⊆β↑ᵣ = mk⟦⊆⟧ (λ {x₁} {x₂} xᵣ → ⟦ℕ⟧-cong (λ x → x ∸ 1) (un⟦⊆⟧ α+⊆β↑ᵣ {su x₁} {su x₂} (suc xᵣ)))

⟦α⊆ø→α+1⊆ø⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ αᵣ ⟦⊆⟧ ⟦ø⟧ ⟦→⟧ αᵣ ⟦+1⟧ ⟦⊆⟧ ⟦ø⟧) α⊆ø→α+1⊆ø α⊆ø→α+1⊆ø
⟦α⊆ø→α+1⊆ø⟧ _ {α⊆ø} _ = mk⟦⊆⟧ (λ {x} _ → Name-elim α⊆ø (predNm x))

⟦α+1⊆ø→α⊆ø⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ αᵣ ⟦+1⟧ ⟦⊆⟧ ⟦ø⟧ ⟦→⟧ αᵣ ⟦⊆⟧ ⟦ø⟧) α+1⊆ø→α⊆ø α+1⊆ø→α⊆ø
⟦α+1⊆ø→α⊆ø⟧ _ {α+1⊆ø} _ = mk⟦⊆⟧ (λ {x} _ → Name-elim α+1⊆ø (su x))

-- not primitive

⟦exportName⟧-core : ∀ {α₁ α₂} (αᵣ : ⟦World⟧ α₁ α₂) x
                    → ⟦Maybe⟧ (⟦Name⟧ αᵣ) (exportName 1 x) (exportName 1 (lift↑1 (_⟨$⟩ᵢ_ αᵣ) x))
⟦exportName⟧-core _  (zero  , _) = ⟦nothing⟧
⟦exportName⟧-core αᵣ (suc _ , _) = ⟦just⟧ (⟶≡.cong (Inj.to αᵣ) ℕe.refl)

⟦exportName⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ⟦Name⟧ (αᵣ ⟦↑1⟧) ⟦→⟧ ⟦Maybe⟧ (⟦Name⟧ αᵣ)) (exportName 1) (exportName 1)
⟦exportName⟧ {_} {α₂} αᵣ {x₁} {x₂} xᵣ = helper {x₂} (≡nm⇒≡ xᵣ)
    -- BUG: the 'with' notation failed here
  where helper : ∀ {x₂} (eq : lift↑1 (_⟨$⟩ᵢ_ αᵣ) x₁ ≡ x₂) → ⟦Maybe⟧ (⟦Name⟧ αᵣ) (exportName 1 x₁) (exportName 1 x₂)
        helper ≡.refl = ⟦exportName⟧-core αᵣ x₁

⟦⊆-ctx-+1↑1⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ ∀⟨ βᵣ ∶ ⟦World⟧ ⟩⟦→⟧ αᵣ ⟦⊆⟧ βᵣ ⟦→⟧ (αᵣ ⟦+1⟧) ⟦⊆⟧ (βᵣ ⟦↑1⟧)) ⊆-ctx-+1↑1 ⊆-ctx-+1↑1
⟦⊆-ctx-+1↑1⟧ αᵣ βᵣ {α⊆β₁} {α⊆β₂} α⊆βᵣ = mk⟦⊆⟧ (λ {x₁} {x₂} xᵣ → helper {x₁} {x₂} (≡nm⇒≡ xᵣ)) where
  helper : (⟦Name⟧≡ (αᵣ ⟦+1⟧) ⟦→⟧ ⟦Name⟧ (βᵣ ⟦↑1⟧)) (coe (⊆-ctx-+1↑1 α⊆β₁)) (coe (⊆-ctx-+1↑1 α⊆β₂))
  helper {zero  , ()} _
  helper {suc x , p} ≡.refl = suc (un⟦⊆⟧ α⊆βᵣ {x , p} {αᵣ ⟨$⟩ᵢ (x , p)} ℕe.refl)

⟦¬Name⟧ : (∀⟨ αᵣ ∶ ⟦World⟧ ⟩⟦→⟧ αᵣ ⟦⊆⟧ ⟦ø⟧ ⟦→⟧ (⟦¬⟧(⟦Name⟧ αᵣ))) ¬Name ¬Name
⟦¬Name⟧ _ {α⊆ø₁} _ {x₁} _ = Name-elim α⊆ø₁ x₁