open import Definition.Typed.EqualityRelation
open import Definition.Typed.Restrictions
module Definition.LogicalRelation
{a} {Mod : Set a}
(R : Type-restrictions Mod)
{{eqrel : EqRelSet R}}
where
open EqRelSet {{...}}
open Type-restrictions R
open import Definition.Untyped Mod as U hiding (_∷_)
open import Definition.Typed.Properties R
open import Definition.Typed R
open import Definition.Typed.Weakening R
open import Tools.Level
open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE
private
variable
p q : Mod
ℓ : Nat
Γ : Con Term ℓ
record _⊩ne_ {ℓ : Nat} (Γ : Con Term ℓ) (A : Term ℓ) : Set a where
constructor ne
field
K : Term ℓ
D : Γ ⊢ A :⇒*: K
neK : Neutral K
K≡K : Γ ⊢ K ~ K ∷ U
record _⊩ne_≡_/_ (Γ : Con Term ℓ) (A B : Term ℓ) ([A] : Γ ⊩ne A) : Set a where
constructor ne₌
open _⊩ne_ [A]
field
M : Term ℓ
D′ : Γ ⊢ B :⇒*: M
neM : Neutral M
K≡M : Γ ⊢ K ~ M ∷ U
record _⊩neNf_∷_ (Γ : Con Term ℓ) (k A : Term ℓ) : Set a where
inductive
constructor neNfₜ
field
neK : Neutral k
⊢k : Γ ⊢ k ∷ A
k≡k : Γ ⊢ k ~ k ∷ A
record _⊩ne_∷_/_ (Γ : Con Term ℓ) (t A : Term ℓ) ([A] : Γ ⊩ne A) : Set a where
inductive
constructor neₜ
open _⊩ne_ [A]
field
k : Term ℓ
d : Γ ⊢ t :⇒*: k ∷ K
nf : Γ ⊩neNf k ∷ K
record _⊩neNf_≡_∷_ (Γ : Con Term ℓ) (k m A : Term ℓ) : Set a where
inductive
constructor neNfₜ₌
field
neK : Neutral k
neM : Neutral m
k≡m : Γ ⊢ k ~ m ∷ A
record _⊩ne_≡_∷_/_ (Γ : Con Term ℓ) (t u A : Term ℓ) ([A] : Γ ⊩ne A) : Set a where
constructor neₜ₌
open _⊩ne_ [A]
field
k m : Term ℓ
d : Γ ⊢ t :⇒*: k ∷ K
d′ : Γ ⊢ u :⇒*: m ∷ K
nf : Γ ⊩neNf k ≡ m ∷ K
_⊩ℕ_ : (Γ : Con Term ℓ) (A : Term ℓ) → Set a
Γ ⊩ℕ A = Γ ⊢ A :⇒*: ℕ
_⊩ℕ_≡_ : (Γ : Con Term ℓ) (A B : Term ℓ) → Set a
Γ ⊩ℕ A ≡ B = Γ ⊢ B ⇒* ℕ
mutual
record _⊩ℕ_∷ℕ (Γ : Con Term ℓ) (t : Term ℓ) : Set a where
inductive
constructor ℕₜ
field
n : Term ℓ
d : Γ ⊢ t :⇒*: n ∷ ℕ
n≡n : Γ ⊢ n ≅ n ∷ ℕ
prop : Natural-prop Γ n
data Natural-prop (Γ : Con Term ℓ) : (n : Term ℓ) → Set a where
sucᵣ : ∀ {n} → Γ ⊩ℕ n ∷ℕ → Natural-prop Γ (suc n)
zeroᵣ : Natural-prop Γ zero
ne : ∀ {n} → Γ ⊩neNf n ∷ ℕ → Natural-prop Γ n
mutual
record _⊩ℕ_≡_∷ℕ (Γ : Con Term ℓ) (t u : Term ℓ) : Set a where
inductive
constructor ℕₜ₌
field
k k′ : Term ℓ
d : Γ ⊢ t :⇒*: k ∷ ℕ
d′ : Γ ⊢ u :⇒*: k′ ∷ ℕ
k≡k′ : Γ ⊢ k ≅ k′ ∷ ℕ
prop : [Natural]-prop Γ k k′
data [Natural]-prop (Γ : Con Term ℓ) : (n n′ : Term ℓ) → Set a where
sucᵣ : ∀ {n n′} → Γ ⊩ℕ n ≡ n′ ∷ℕ → [Natural]-prop Γ (suc n) (suc n′)
zeroᵣ : [Natural]-prop Γ zero zero
ne : ∀ {n n′} → Γ ⊩neNf n ≡ n′ ∷ ℕ → [Natural]-prop Γ n n′
natural : ∀ {n} → Natural-prop Γ n → Natural n
natural (sucᵣ x) = sucₙ
natural zeroᵣ = zeroₙ
natural (ne (neNfₜ neK ⊢k k≡k)) = ne neK
split : ∀ {a b} → [Natural]-prop Γ a b → Natural a × Natural b
split (sucᵣ x) = sucₙ , sucₙ
split zeroᵣ = zeroₙ , zeroₙ
split (ne (neNfₜ₌ neK neM k≡m)) = ne neK , ne neM
_⊩Empty_ : (Γ : Con Term ℓ) (A : Term ℓ) → Set a
Γ ⊩Empty A = Γ ⊢ A :⇒*: Empty
_⊩Empty_≡_ : (Γ : Con Term ℓ) (A B : Term ℓ) → Set a
Γ ⊩Empty A ≡ B = Γ ⊢ B ⇒* Empty
data Empty-prop (Γ : Con Term ℓ) : (n : Term ℓ) → Set a where
ne : ∀ {n} → Γ ⊩neNf n ∷ Empty → Empty-prop Γ n
record _⊩Empty_∷Empty (Γ : Con Term ℓ) (t : Term ℓ) : Set a where
inductive
constructor Emptyₜ
field
n : Term ℓ
d : Γ ⊢ t :⇒*: n ∷ Empty
n≡n : Γ ⊢ n ≅ n ∷ Empty
prop : Empty-prop Γ n
data [Empty]-prop (Γ : Con Term ℓ) : (n n′ : Term ℓ) → Set a where
ne : ∀ {n n′} → Γ ⊩neNf n ≡ n′ ∷ Empty → [Empty]-prop Γ n n′
record _⊩Empty_≡_∷Empty (Γ : Con Term ℓ) (t u : Term ℓ) : Set a where
inductive
constructor Emptyₜ₌
field
k k′ : Term ℓ
d : Γ ⊢ t :⇒*: k ∷ Empty
d′ : Γ ⊢ u :⇒*: k′ ∷ Empty
k≡k′ : Γ ⊢ k ≅ k′ ∷ Empty
prop : [Empty]-prop Γ k k′
empty : ∀ {n} → Empty-prop Γ n → Neutral n
empty (ne (neNfₜ neK _ _)) = neK
esplit : ∀ {a b} → [Empty]-prop Γ a b → Neutral a × Neutral b
esplit (ne (neNfₜ₌ neK neM k≡m)) = neK , neM
record _⊩Unit_ (Γ : Con Term ℓ) (A : Term ℓ) : Set a where
no-eta-equality
pattern
constructor Unitₜ
field
⇒*-Unit : Γ ⊢ A :⇒*: Unit
ok : Unit-allowed
_⊩Unit_≡_ : (Γ : Con Term ℓ) (A B : Term ℓ) → Set a
Γ ⊩Unit A ≡ B = Γ ⊢ B ⇒* Unit
record _⊩Unit_∷Unit (Γ : Con Term ℓ) (t : Term ℓ) : Set a where
inductive
constructor Unitₜ
field
n : Term ℓ
d : Γ ⊢ t :⇒*: n ∷ Unit
prop : Whnf n
record _⊩Unit_≡_∷Unit (Γ : Con Term ℓ) (t u : Term ℓ) : Set a where
constructor Unitₜ₌
field
⊢t : Γ ⊢ t ∷ Unit
⊢u : Γ ⊢ u ∷ Unit
data TypeLevel : Set where
⁰ : TypeLevel
¹ : TypeLevel
data _<_ : (i j : TypeLevel) → Set where
0<1 : ⁰ < ¹
record LogRelKit : Set (lsuc a) where
constructor Kit
field
_⊩U : (Γ : Con Term ℓ) → Set a
_⊩B⟨_⟩_ : (Γ : Con Term ℓ) (W : BindingType) → Term ℓ → Set a
_⊩_ : (Γ : Con Term ℓ) → Term ℓ → Set a
_⊩_≡_/_ : (Γ : Con Term ℓ) (A B : Term ℓ) → Γ ⊩ A → Set a
_⊩_∷_/_ : (Γ : Con Term ℓ) (t A : Term ℓ) → Γ ⊩ A → Set a
_⊩_≡_∷_/_ : (Γ : Con Term ℓ) (t u A : Term ℓ) → Γ ⊩ A → Set a
module LogRel (l : TypeLevel) (rec : ∀ {l′} → l′ < l → LogRelKit) where
record _⊩₁U (Γ : Con Term ℓ) : Set a where
constructor Uᵣ
field
l′ : TypeLevel
l< : l′ < l
⊢Γ : ⊢ Γ
_⊩₁U≡_ : (Γ : Con Term ℓ) (B : Term ℓ) → Set a
Γ ⊩₁U≡ B = B PE.≡ U
record _⊩₁U_∷U/_ {l′} (Γ : Con Term ℓ) (t : Term ℓ) (l< : l′ < l) : Set a where
constructor Uₜ
open LogRelKit (rec l<)
field
A : Term ℓ
d : Γ ⊢ t :⇒*: A ∷ U
typeA : Type A
A≡A : Γ ⊢ A ≅ A ∷ U
[t] : Γ ⊩ t
record _⊩₁U_≡_∷U/_ {l′} (Γ : Con Term ℓ) (t u : Term ℓ) (l< : l′ < l) : Set a where
constructor Uₜ₌
open LogRelKit (rec l<)
field
A B : Term ℓ
d : Γ ⊢ t :⇒*: A ∷ U
d′ : Γ ⊢ u :⇒*: B ∷ U
typeA : Type A
typeB : Type B
A≡B : Γ ⊢ A ≅ B ∷ U
[t] : Γ ⊩ t
[u] : Γ ⊩ u
[t≡u] : Γ ⊩ t ≡ u / [t]
mutual
record _⊩ₗB⟨_⟩_ (Γ : Con Term ℓ) (W : BindingType) (A : Term ℓ) : Set a where
inductive
constructor Bᵣ
eta-equality
field
F : Term ℓ
G : Term (1+ ℓ)
D : Γ ⊢ A :⇒*: ⟦ W ⟧ F ▹ G
⊢F : Γ ⊢ F
⊢G : Γ ∙ F ⊢ G
A≡A : Γ ⊢ ⟦ W ⟧ F ▹ G ≅ ⟦ W ⟧ F ▹ G
[F] : ∀ {m} {ρ : Wk m ℓ} {Δ : Con Term m} → ρ ∷ Δ ⊇ Γ → ⊢ Δ → Δ ⊩ₗ U.wk ρ F
[G] : ∀ {m} {ρ : Wk m ℓ} {Δ : Con Term m} {a : Term m}
→ ([ρ] : ρ ∷ Δ ⊇ Γ) (⊢Δ : ⊢ Δ)
→ Δ ⊩ₗ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ
→ Δ ⊩ₗ U.wk (lift ρ) G [ a ]₀
G-ext : ∀ {m} {ρ : Wk m ℓ} {Δ : Con Term m} {a b}
→ ([ρ] : ρ ∷ Δ ⊇ Γ) (⊢Δ : ⊢ Δ)
→ ([a] : Δ ⊩ₗ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
→ ([b] : Δ ⊩ₗ b ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
→ Δ ⊩ₗ a ≡ b ∷ U.wk ρ F / [F] [ρ] ⊢Δ
→ Δ ⊩ₗ U.wk (lift ρ) G [ a ]₀ ≡ U.wk (lift ρ) G [ b ]₀ / [G] [ρ] ⊢Δ [a]
ok : BindingType-allowed W
record _⊩ₗB⟨_⟩_≡_/_ (Γ : Con Term ℓ) (W : BindingType) (A B : Term ℓ) ([A] : Γ ⊩ₗB⟨ W ⟩ A) : Set a where
inductive
constructor B₌
eta-equality
open _⊩ₗB⟨_⟩_ [A]
field
F′ : Term ℓ
G′ : Term (1+ ℓ)
D′ : Γ ⊢ B ⇒* ⟦ W ⟧ F′ ▹ G′
A≡B : Γ ⊢ ⟦ W ⟧ F ▹ G ≅ ⟦ W ⟧ F′ ▹ G′
[F≡F′] : {m : Nat} {ρ : Wk m ℓ} {Δ : Con Term m}
→ ([ρ] : ρ ∷ Δ ⊇ Γ) (⊢Δ : ⊢ Δ)
→ Δ ⊩ₗ U.wk ρ F ≡ U.wk ρ F′ / [F] [ρ] ⊢Δ
[G≡G′] : ∀ {m} {ρ : Wk m ℓ} {Δ : Con Term m} {a}
→ ([ρ] : ρ ∷ Δ ⊇ Γ) (⊢Δ : ⊢ Δ)
→ ([a] : Δ ⊩ₗ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
→ Δ ⊩ₗ U.wk (lift ρ) G [ a ]₀ ≡ U.wk (lift ρ) G′ [ a ]₀ / [G] [ρ] ⊢Δ [a]
_⊩ₗΠ_∷_/_ : {ℓ : Nat} {p q : Mod} (Γ : Con Term ℓ) (t A : Term ℓ) ([A] : Γ ⊩ₗB⟨ BΠ p q ⟩ A) → Set a
_⊩ₗΠ_∷_/_ {ℓ} {p} {q} Γ t A (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _) =
∃ λ f → Γ ⊢ t :⇒*: f ∷ Π p , q ▷ F ▹ G
× Function f
× Γ ⊢ f ≅ f ∷ Π p , q ▷ F ▹ G
× (∀ {m} {ρ : Wk m ℓ} {Δ : Con Term m} {a b}
([ρ] : ρ ∷ Δ ⊇ Γ) (⊢Δ : ⊢ Δ)
([a] : Δ ⊩ₗ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
([b] : Δ ⊩ₗ b ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
([a≡b] : Δ ⊩ₗ a ≡ b ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
→ Δ ⊩ₗ U.wk ρ f ∘⟨ p ⟩ a ≡ U.wk ρ f ∘⟨ p ⟩ b ∷ U.wk (lift ρ) G [ a ]₀ / [G] [ρ] ⊢Δ [a])
× (∀ {m} {ρ : Wk m ℓ} {Δ : Con Term m} {a} → ([ρ] : ρ ∷ Δ ⊇ Γ) (⊢Δ : ⊢ Δ)
→ ([a] : Δ ⊩ₗ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
→ Δ ⊩ₗ U.wk ρ f ∘⟨ p ⟩ a ∷ U.wk (lift ρ) G [ a ]₀ / [G] [ρ] ⊢Δ [a])
_⊩ₗΠ_≡_∷_/_ : {ℓ : Nat} {p q : Mod} (Γ : Con Term ℓ) (t u A : Term ℓ) ([A] : Γ ⊩ₗB⟨ BΠ p q ⟩ A) → Set a
_⊩ₗΠ_≡_∷_/_
{ℓ} {p} {q} Γ t u A [A]@(Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _) =
∃₂ λ f g → Γ ⊢ t :⇒*: f ∷ Π p , q ▷ F ▹ G
× Γ ⊢ u :⇒*: g ∷ Π p , q ▷ F ▹ G
× Function f
× Function g
× Γ ⊢ f ≅ g ∷ Π p , q ▷ F ▹ G
× Γ ⊩ₗΠ t ∷ A / [A]
× Γ ⊩ₗΠ u ∷ A / [A]
× (∀ {m} {ρ : Wk m ℓ} {Δ : Con Term m} {a} ([ρ] : ρ ∷ Δ ⊇ Γ) (⊢Δ : ⊢ Δ)
([a] : Δ ⊩ₗ a ∷ U.wk ρ F / [F] [ρ] ⊢Δ)
→ Δ ⊩ₗ U.wk ρ f ∘⟨ p ⟩ a ≡ U.wk ρ g ∘⟨ p ⟩ a ∷ U.wk (lift ρ) G [ a ]₀ / [G] [ρ] ⊢Δ [a])
_⊩ₗΣ_∷_/_ :
{p q : Mod} {m : SigmaMode} (Γ : Con Term ℓ) (t A : Term ℓ)
([A] : Γ ⊩ₗB⟨ BΣ m p q ⟩ A) → Set a
_⊩ₗΣ_∷_/_
{p = p} {q = q} {m = m} Γ t A
[A]@(Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _) =
∃ λ u → Γ ⊢ t :⇒*: u ∷ Σ⟨ m ⟩ p , q ▷ F ▹ G
× Γ ⊢ u ≅ u ∷ Σ⟨ m ⟩ p , q ▷ F ▹ G
× Σ (Product u) λ pProd
→ Σ-prop m u Γ [A] pProd
Σ-prop : ∀ {A p q} (m : SigmaMode) (t : Term ℓ) → (Γ : Con Term ℓ)
→ ([A] : Γ ⊩ₗB⟨ BΣ m p q ⟩ A) → (Product t) → Set a
Σ-prop {p = p} Σₚ t Γ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _) _ =
Σ (Γ ⊩ₗ fst p t ∷ U.wk id F / [F] id (wf ⊢F)) λ [fst] →
Γ ⊩ₗ snd p t ∷ U.wk (lift id) G [ fst p t ]₀ /
[G] id (wf ⊢F) [fst]
Σ-prop
{p = p} Σᵣ t Γ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _)
(prodₙ {p = p′} {t = p₁} {u = p₂} {m = m}) =
p PE.≡ p′ ×
Σ (Γ ⊩ₗ p₁ ∷ U.wk id F / [F] id (wf ⊢F)) λ [p₁]
→ Γ ⊩ₗ p₂ ∷ U.wk (lift id) G [ p₁ ]₀ / [G] id (wf ⊢F) [p₁]
× m PE.≡ Σᵣ
Σ-prop
{p = p} {q = q}
Σᵣ t Γ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _) (ne x) =
Γ ⊢ t ~ t ∷ Σᵣ p , q ▷ F ▹ G
_⊩ₗΣ_≡_∷_/_ :
{p q : Mod} {m : SigmaMode} (Γ : Con Term ℓ) (t u A : Term ℓ)
([A] : Γ ⊩ₗB⟨ BΣ m p q ⟩ A) → Set a
_⊩ₗΣ_≡_∷_/_
{p = p} {q = q} {m} Γ t u A
[A]@(Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _) =
∃₂ λ t′ u′ → Γ ⊢ t :⇒*: t′ ∷ Σ⟨ m ⟩ p , q ▷ F ▹ G
× Γ ⊢ u :⇒*: u′ ∷ Σ⟨ m ⟩ p , q ▷ F ▹ G
× Γ ⊢ t′ ≅ u′ ∷ Σ⟨ m ⟩ p , q ▷ F ▹ G
× Γ ⊩ₗΣ t ∷ A / [A]
× Γ ⊩ₗΣ u ∷ A / [A]
× Σ (Product t′) λ pProd
→ Σ (Product u′) λ rProd
→ [Σ]-prop m t′ u′ Γ [A] pProd rProd
[Σ]-prop :
∀ {A p q} (m : SigmaMode) (t r : Term ℓ) (Γ : Con Term ℓ)
([A] : Γ ⊩ₗB⟨ BΣ m p q ⟩ A) → Product t → Product r → Set a
[Σ]-prop {p = p} Σₚ t r Γ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _) _ _ =
Σ (Γ ⊩ₗ fst p t ∷ U.wk id F / [F] id (wf ⊢F)) λ [fstp]
→ Γ ⊩ₗ fst p r ∷ U.wk id F / [F] id (wf ⊢F)
× Γ ⊩ₗ fst p t ≡ fst p r ∷ U.wk id F / [F] id (wf ⊢F)
× Γ ⊩ₗ snd p t ≡ snd p r ∷ U.wk (lift id) G [ fst p t ]₀
/ [G] id (wf ⊢F) [fstp]
[Σ]-prop
{p = p} Σᵣ t r Γ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _)
(prodₙ {p = p′} {t = p₁} {u = p₂})
(prodₙ {p = p″} {t = r₁} {u = r₂}) =
p PE.≡ p′ × p PE.≡ p″ ×
Σ (Γ ⊩ₗ p₁ ∷ U.wk id F / [F] id (wf ⊢F)) λ [p₁] →
Σ (Γ ⊩ₗ r₁ ∷ U.wk id F / [F] id (wf ⊢F)) λ [r₁]
→ (Γ ⊩ₗ p₂ ∷ U.wk (lift id) G [ p₁ ]₀ / [G] id (wf ⊢F) [p₁])
× (Γ ⊩ₗ r₂ ∷ U.wk (lift id) G [ r₁ ]₀ / [G] id (wf ⊢F) [r₁])
× (Γ ⊩ₗ p₁ ≡ r₁ ∷ U.wk id F / [F] id (wf ⊢F))
× (Γ ⊩ₗ p₂ ≡ r₂ ∷ U.wk (lift id) G [ p₁ ]₀ / [G] id (wf ⊢F) [p₁])
[Σ]-prop
Σᵣ t r Γ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _)
(prodₙ {t = p₁} {u = p₂}) (ne y) =
Lift a PE.⊥
[Σ]-prop
Σᵣ t r Γ (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext ok)
(ne x) (prodₙ {t = r₁} {u = r₂}) =
Lift a PE.⊥
[Σ]-prop
{p = p} {q = q} Σᵣ t r Γ
(Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext _) (ne x) (ne y) =
Γ ⊢ t ~ r ∷ Σᵣ p , q ▷ F ▹ G
data _⊩ₗ_ (Γ : Con Term ℓ) : Term ℓ → Set a where
Uᵣ : Γ ⊩₁U → Γ ⊩ₗ U
ℕᵣ : ∀ {A} → Γ ⊩ℕ A → Γ ⊩ₗ A
Emptyᵣ : ∀ {A} → Γ ⊩Empty A → Γ ⊩ₗ A
Unitᵣ : ∀ {A} → Γ ⊩Unit A → Γ ⊩ₗ A
ne : ∀ {A} → Γ ⊩ne A → Γ ⊩ₗ A
Bᵣ : ∀ {A} W → Γ ⊩ₗB⟨ W ⟩ A → Γ ⊩ₗ A
emb : ∀ {A l′} (l< : l′ < l) (let open LogRelKit (rec l<))
([A] : Γ ⊩ A) → Γ ⊩ₗ A
_⊩ₗ_≡_/_ : (Γ : Con Term ℓ) (A B : Term ℓ) → Γ ⊩ₗ A → Set a
Γ ⊩ₗ A ≡ B / Uᵣ UA = Γ ⊩₁U≡ B
Γ ⊩ₗ A ≡ B / ℕᵣ D = Γ ⊩ℕ A ≡ B
Γ ⊩ₗ A ≡ B / Emptyᵣ D = Γ ⊩Empty A ≡ B
Γ ⊩ₗ A ≡ B / Unitᵣ D = Γ ⊩Unit A ≡ B
Γ ⊩ₗ A ≡ B / ne neA = Γ ⊩ne A ≡ B / neA
Γ ⊩ₗ A ≡ B / Bᵣ W BA = Γ ⊩ₗB⟨ W ⟩ A ≡ B / BA
Γ ⊩ₗ A ≡ B / emb l< [A] = Γ ⊩ A ≡ B / [A]
where open LogRelKit (rec l<)
_⊩ₗ_∷_/_ : (Γ : Con Term ℓ) (t A : Term ℓ) → Γ ⊩ₗ A → Set a
Γ ⊩ₗ t ∷ .U / Uᵣ (Uᵣ l′ l< ⊢Γ) = Γ ⊩₁U t ∷U/ l<
Γ ⊩ₗ t ∷ A / ℕᵣ D = Γ ⊩ℕ t ∷ℕ
Γ ⊩ₗ t ∷ A / Emptyᵣ D = Γ ⊩Empty t ∷Empty
Γ ⊩ₗ t ∷ A / Unitᵣ D = Γ ⊩Unit t ∷Unit
Γ ⊩ₗ t ∷ A / ne neA = Γ ⊩ne t ∷ A / neA
Γ ⊩ₗ t ∷ A / Bᵣ BΠ! ΠA = Γ ⊩ₗΠ t ∷ A / ΠA
Γ ⊩ₗ t ∷ A / Bᵣ BΣ! ΣA = Γ ⊩ₗΣ t ∷ A / ΣA
Γ ⊩ₗ t ∷ A / emb l< [A] = Γ ⊩ t ∷ A / [A]
where open LogRelKit (rec l<)
_⊩ₗ_≡_∷_/_ : (Γ : Con Term ℓ) (t u A : Term ℓ) → Γ ⊩ₗ A → Set a
Γ ⊩ₗ t ≡ u ∷ .U / Uᵣ (Uᵣ l′ l< ⊢Γ) = Γ ⊩₁U t ≡ u ∷U/ l<
Γ ⊩ₗ t ≡ u ∷ A / ℕᵣ D = Γ ⊩ℕ t ≡ u ∷ℕ
Γ ⊩ₗ t ≡ u ∷ A / Emptyᵣ D = Γ ⊩Empty t ≡ u ∷Empty
Γ ⊩ₗ t ≡ u ∷ A / Unitᵣ D = Γ ⊩Unit t ≡ u ∷Unit
Γ ⊩ₗ t ≡ u ∷ A / ne neA = Γ ⊩ne t ≡ u ∷ A / neA
Γ ⊩ₗ t ≡ u ∷ A / Bᵣ BΠ! ΠA = Γ ⊩ₗΠ t ≡ u ∷ A / ΠA
Γ ⊩ₗ t ≡ u ∷ A / Bᵣ BΣ! ΣA = Γ ⊩ₗΣ t ≡ u ∷ A / ΣA
Γ ⊩ₗ t ≡ u ∷ A / emb l< [A] = Γ ⊩ t ≡ u ∷ A / [A]
where open LogRelKit (rec l<)
kit : LogRelKit
kit = Kit _⊩₁U _⊩ₗB⟨_⟩_
_⊩ₗ_ _⊩ₗ_≡_/_ _⊩ₗ_∷_/_ _⊩ₗ_≡_∷_/_
open LogRel public using (Uᵣ; ℕᵣ; Emptyᵣ; Unitᵣ; ne; Bᵣ; B₌; emb; Uₜ; Uₜ₌)
pattern Πₜ f d funcF f≡f [f] [f]₁ = f , d , funcF , f≡f , [f] , [f]₁
pattern Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g] = f , g , d , d′ , funcF , funcG , f≡g , [f] , [g] , [f≡g]
pattern Σₜ p d p≡p pProd prop = p , d , p≡p , pProd , prop
pattern Σₜ₌ p r d d′ pProd rProd p≅r [t] [u] prop = p , r , d , d′ , p≅r , [t] , [u] , pProd , rProd , prop
pattern Uᵣ′ a b c = Uᵣ (Uᵣ a b c)
pattern ne′ a b c d = ne (ne a b c d)
pattern Bᵣ′ W a b c d e f g h i j = Bᵣ W (Bᵣ a b c d e f g h i j)
pattern Πᵣ′ a b c d e f g h i j = Bᵣ′ BΠ! a b c d e f g h i j
pattern Σᵣ′ a b c d e f g h i j = Bᵣ′ BΣ! a b c d e f g h i j
logRelRec : ∀ l {l′} → l′ < l → LogRelKit
logRelRec ⁰ = λ ()
logRelRec ¹ 0<1 = LogRel.kit ⁰ (λ ())
kit : ∀ (i : TypeLevel) → LogRelKit
kit l = LogRel.kit l (logRelRec l)
_⊩′⟨_⟩U : (Γ : Con Term ℓ) (l : TypeLevel) → Set a
Γ ⊩′⟨ l ⟩U = Γ ⊩U where open LogRelKit (kit l)
_⊩′⟨_⟩B⟨_⟩_ : (Γ : Con Term ℓ) (l : TypeLevel) (W : BindingType) → Term ℓ → Set a
Γ ⊩′⟨ l ⟩B⟨ W ⟩ A = Γ ⊩B⟨ W ⟩ A where open LogRelKit (kit l)
_⊩⟨_⟩_ : (Γ : Con Term ℓ) (l : TypeLevel) → Term ℓ → Set a
Γ ⊩⟨ l ⟩ A = Γ ⊩ A where open LogRelKit (kit l)
_⊩⟨_⟩_≡_/_ : (Γ : Con Term ℓ) (l : TypeLevel) (A B : Term ℓ) → Γ ⊩⟨ l ⟩ A → Set a
Γ ⊩⟨ l ⟩ A ≡ B / [A] = Γ ⊩ A ≡ B / [A] where open LogRelKit (kit l)
_⊩⟨_⟩_∷_/_ : (Γ : Con Term ℓ) (l : TypeLevel) (t A : Term ℓ) → Γ ⊩⟨ l ⟩ A → Set a
Γ ⊩⟨ l ⟩ t ∷ A / [A] = Γ ⊩ t ∷ A / [A] where open LogRelKit (kit l)
_⊩⟨_⟩_≡_∷_/_ : (Γ : Con Term ℓ) (l : TypeLevel) (t u A : Term ℓ) → Γ ⊩⟨ l ⟩ A → Set a
Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A] = Γ ⊩ t ≡ u ∷ A / [A] where open LogRelKit (kit l)