{-# OPTIONS --universe-polymorphism #-}
module NaPa.LogicalRelation where
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
==ℕ-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
⟦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₁ , _)))
≈⟨ ≡nm-⟦ℕ⟧-cong (λ x → suc (name (αᵣ ⟦+ kᵣ ⟧ ⟨$⟩ᵢ x))) ℕe.refl ⟩
suc (name (αᵣ ⟦+ kᵣ ⟧ ⟨$⟩ᵢ (k₁ +ℕ name x₁ , _)))
≈⟨ 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₁ , _))
≈⟨ ≡-⟦ℕ⟧-cong (λ x → name (αᵣ ⟨$⟩ᵢ x)) (name-injective (≡.sym (∸-+-assoc (name x₁) 1 k₁))) ⟩
name (αᵣ ⟨$⟩ᵢ (name x₁ ∸ 1 ∸ k₁ , _))
≈⟨ ⟦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))
⟦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ᵣ)
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₁