470 lines
15 KiB
Agda
470 lines
15 KiB
Agda
module univTypes.SubjectReduction.Specification where
|
||
|
||
open import Data.Nat using (ℕ; zero; suc)
|
||
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
|
||
|
||
open import univTypes.Util.Fin using (Fin; zero; suc)
|
||
|
||
-- Fixities --------------------------------------------------------------------
|
||
|
||
infix 4 _↪_ _↪*_
|
||
infix 4 _⊢_⦂_
|
||
infixl 5 _,_
|
||
infix 5 `λ_
|
||
infixl 7 _·_
|
||
infix 9 `_
|
||
infixl 9 _[_]
|
||
|
||
-- Axioms ----------------------------------------------------------------------
|
||
|
||
-- Functional Extensionality
|
||
postulate
|
||
fun-ext : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : A → Set ℓ₂} {f g : (x : A) → B x}
|
||
→ (∀ x → f x ≡ g x)
|
||
→ f ≡ g
|
||
|
||
-- No other postulates are allowed!
|
||
|
||
-- Syntax ----------------------------------------------------------------------
|
||
|
||
data Term : ℕ → Set where
|
||
`_ : ∀ {n} → Fin n → Term n
|
||
`λ_ : ∀ {n} → Term (suc n) → Term n
|
||
_·_ : ∀ {n} → Term n → Term n → Term n
|
||
∀[x⦂_]_ : ∀ {n} → Term n → Term (suc n) → Term n
|
||
|
||
-- My Extension
|
||
`Setω_ : ∀ {n} (l : Term n) → Term n
|
||
`Setn_ : ∀ {n} (l : Term n) → Term n
|
||
`Level : ∀ {n} → Term n
|
||
`lzero : ∀ {n} → Term n
|
||
`lsuc : ∀ {n} → Term n → Term n
|
||
_`⊔_ : ∀ {n} → Term n → Term n → Term n
|
||
|
||
-- Extension
|
||
∃[x⦂_]_ : ∀ {n} → Term n → Term (suc n) → Term n
|
||
_`,_ : ∀ {n} → Term n → Term n → Term n
|
||
`proj₁ : ∀ {n} → Term n → Term n
|
||
`proj₂ : ∀ {n} → Term n → Term n
|
||
_`≡_ : ∀ {n} → Term n → Term n → Term n
|
||
`refl : ∀ {n} → Term n
|
||
`subst : ∀ {n} → Term (suc n) → Term n → Term n → Term n
|
||
|
||
-- Substitution ----------------------------------------------------------------
|
||
|
||
`Set : ∀ {n} → Term n
|
||
`Set = `Setn (`lzero)
|
||
|
||
-- Renamings
|
||
|
||
Ren : ℕ → ℕ → Set
|
||
Ren m n = Fin m → Fin n
|
||
|
||
extᵣ : ∀ {m n} → Ren m n → Ren (suc m) (suc n)
|
||
extᵣ ρ zero = zero
|
||
extᵣ ρ (suc x) = suc (ρ x)
|
||
|
||
ren : ∀ {m n}
|
||
→ Ren m n
|
||
→ (Term m → Term n)
|
||
ren ρ (` x) = ` (ρ x)
|
||
ren ρ (`λ e) = `λ (ren (extᵣ ρ) e)
|
||
ren ρ (e₁ · e₂) = (ren ρ e₁) · (ren ρ e₂)
|
||
ren ρ (∀[x⦂ e₁ ] e₂) = ∀[x⦂ ren ρ e₁ ] ren (extᵣ ρ) e₂
|
||
ren ρ (`Setω l) = `Setω (ren ρ l)
|
||
ren ρ (`Setn x) = `Setn ren ρ x
|
||
ren ρ `Level = `Level
|
||
ren ρ `lzero = `lzero
|
||
ren ρ (`lsuc l) = `lsuc (ren ρ l)
|
||
ren ρ (l `⊔ r) = (ren ρ l) `⊔ (ren ρ r)
|
||
ren ρ (∃[x⦂ t₁ ] t₂) = ∃[x⦂ ren ρ t₁ ] ren (extᵣ ρ) t₂
|
||
ren ρ (e₁ `, e₂) = (ren ρ e₁) `, (ren ρ e₂)
|
||
ren ρ (`proj₁ e) = `proj₁ (ren ρ e)
|
||
ren ρ (`proj₂ e) = `proj₂ (ren ρ e)
|
||
ren ρ `refl = `refl
|
||
ren ρ (e₁ `≡ e₂) = ren ρ e₁ `≡ ren ρ e₂
|
||
ren ρ (`subst t e₁ e₂) = `subst (ren (extᵣ ρ) t) (ren ρ e₁) (ren ρ e₂)
|
||
|
||
wk : ∀ {n} → Ren n (suc n)
|
||
wk x = suc x
|
||
|
||
-- Substitutions
|
||
|
||
Sub : ℕ → ℕ → Set
|
||
Sub m n = Fin m → Term n
|
||
|
||
extₛ : ∀ {m n} → Sub m n → Sub (suc m) (suc n)
|
||
extₛ σ zero = ` zero
|
||
extₛ σ (suc x) = ren wk (σ x)
|
||
|
||
sub : ∀ {m n}
|
||
→ Sub m n
|
||
→ (Term m → Term n)
|
||
sub σ (` x) = σ x
|
||
sub σ (`λ e) = `λ (sub (extₛ σ) e)
|
||
sub σ (e₁ · e₂) = (sub σ e₁) · (sub σ e₂)
|
||
sub σ (∀[x⦂ e₁ ] e₂) = ∀[x⦂ sub σ e₁ ] sub (extₛ σ) e₂
|
||
sub σ (`Setω l) = `Setω (sub σ l)
|
||
sub σ (`Setn l) = `Setn sub σ l
|
||
sub σ (`Level) = `Level
|
||
sub σ `lzero = `lzero
|
||
sub σ (`lsuc l) = `lsuc (sub σ l)
|
||
sub σ (l `⊔ r) = (sub σ l) `⊔ (sub σ r)
|
||
sub σ (∃[x⦂ t₁ ] t₂) = ∃[x⦂ sub σ t₁ ] sub (extₛ σ) t₂
|
||
sub σ (e₁ `, e₂) = (sub σ e₁) `, (sub σ e₂)
|
||
sub σ (`proj₁ e) = `proj₁ (sub σ e)
|
||
sub σ (`proj₂ e) = `proj₂ (sub σ e)
|
||
sub σ `refl = `refl
|
||
sub σ (e₁ `≡ e₂) = sub σ e₁ `≡ sub σ e₂
|
||
sub σ (`subst t e₁ e₂) = `subst (sub (extₛ σ) t) (sub σ e₁) (sub σ e₂)
|
||
|
||
0↦ : ∀ {n} → Term n → Sub (suc n) n
|
||
(0↦ e) zero = e
|
||
(0↦ e) (suc x) = ` x
|
||
|
||
_[_] : ∀ {n} → Term (suc n) → Term n → Term n
|
||
e₁ [ e₂ ] = sub (0↦ e₂) e₁
|
||
|
||
-- Semantics -------------------------------------------------------------------
|
||
|
||
-- Values
|
||
|
||
mutual
|
||
data Value : ∀ {n} → Term n → Set where
|
||
val-λ : ∀ {n} {e : Term (suc n)}
|
||
→ Value e
|
||
------------
|
||
→ Value (`λ e)
|
||
val-∀ : ∀ {n} {e₁ : Term n} {e₂ : Term (suc n)}
|
||
→ Value e₁
|
||
→ Value e₂
|
||
--------------------
|
||
→ Value (∀[x⦂ e₁ ] e₂)
|
||
val-Setω : ∀ {n l}
|
||
→ Value {n = n} (`Setω l)
|
||
val-Setn : ∀ {n l}
|
||
→ Value l
|
||
→ Value {n = n} (`Setn l)
|
||
|
||
val-Level : ∀ {n}
|
||
→ Value {n = n} `Level
|
||
|
||
val-l : ∀ {n v}
|
||
→ Value {n = n} (`lzero)
|
||
|
||
val-lsuc : ∀ {n v l}
|
||
→ Value l
|
||
→ Value {n = n} (`lsuc l)
|
||
|
||
val-neu : ∀ {n} {e : Term n}
|
||
→ Neutral e
|
||
---------
|
||
→ Value e
|
||
val-∃ : ∀ {n} {e₁ : Term n} {e₂ : Term (suc n)}
|
||
→ Value e₁
|
||
→ Value e₂
|
||
--------------------
|
||
→ Value (∃[x⦂ e₁ ] e₂)
|
||
val-, : ∀ {n} {e₁ e₂ : Term n}
|
||
→ Value e₁
|
||
→ Value e₂
|
||
---------
|
||
→ Value (e₁ `, e₂)
|
||
val-≡ : ∀ {n} {e₁ : Term n} {e₂ : Term n}
|
||
→ Value e₁
|
||
→ Value e₂
|
||
--------------------
|
||
→ Value (e₁ `≡ e₂)
|
||
val-refl : ∀ {n}
|
||
→ Value {n = n} `refl
|
||
|
||
data Neutral : ∀ {n} → Term n → Set where
|
||
neu-` : ∀ {n} {x : Fin n}
|
||
→ Neutral (` x)
|
||
neu-· : ∀ {n} {e₁ e₂ : Term n}
|
||
→ Neutral e₁
|
||
→ Value e₂
|
||
-----------------
|
||
→ Neutral (e₁ · e₂)
|
||
neu-proj₁ : ∀ {n} {e : Term n}
|
||
→ Neutral e
|
||
-----------------
|
||
→ Neutral (`proj₁ e)
|
||
neu-proj₂ : ∀ {n} {e : Term n}
|
||
→ Neutral e
|
||
-----------------
|
||
→ Neutral (`proj₂ e)
|
||
neu-subst : ∀ {n} {t : Term (suc n)} {e₁ e₂ : Term n}
|
||
→ Value t
|
||
→ Neutral e₁
|
||
→ Value e₂
|
||
------------------------
|
||
→ Neutral (`subst t e₁ e₂)
|
||
|
||
-- Reduction
|
||
|
||
data _↪_ : ∀ {n} → Term n → Term n → Set where
|
||
β-λ : ∀ {n} {e₁ : Term (suc n)} {e₂ : Term n}
|
||
→ (`λ e₁) · e₂ ↪ e₁ [ e₂ ]
|
||
|
||
ξ-λ : ∀ {n} {e e' : Term (suc n)}
|
||
→ e ↪ e'
|
||
---------------
|
||
→ `λ e ↪ `λ e'
|
||
|
||
ξ-·₁ : ∀ {n} {e₁ e₂ e₁' : Term n}
|
||
→ e₁ ↪ e₁'
|
||
---------------------
|
||
→ e₁ · e₂ ↪ e₁' · e₂
|
||
|
||
ξ-·₂ : ∀ {n} {e₁ e₂ e₂' : Term n}
|
||
→ e₂ ↪ e₂'
|
||
---------------------
|
||
→ e₁ · e₂ ↪ e₁ · e₂'
|
||
|
||
ξ-∀₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term (suc n)}
|
||
→ t₁ ↪ t₁'
|
||
-------------------------------
|
||
→ ∀[x⦂ t₁ ] t₂ ↪ ∀[x⦂ t₁' ] t₂
|
||
|
||
ξ-∀₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term (suc n)}
|
||
→ t₂ ↪ t₂'
|
||
-------------------------------
|
||
→ ∀[x⦂ t₁ ] t₂ ↪ ∀[x⦂ t₁ ] t₂'
|
||
|
||
β-proj₁ : ∀ {n} {e₁ e₂ : Term n}
|
||
→ `proj₁ (e₁ `, e₂) ↪ e₁
|
||
|
||
β-proj₂ : ∀ {n} {e₁ e₂ : Term n}
|
||
→ `proj₂ (e₁ `, e₂) ↪ e₂
|
||
|
||
β-subst : ∀ {n} {t : Term (suc n)} {e : Term n}
|
||
→ `subst t `refl e ↪ e
|
||
|
||
ξ-∃₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term (suc n)}
|
||
→ t₁ ↪ t₁'
|
||
-------------------------------
|
||
→ ∃[x⦂ t₁ ] t₂ ↪ ∃[x⦂ t₁' ] t₂
|
||
|
||
ξ-∃₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term (suc n)}
|
||
→ t₂ ↪ t₂'
|
||
-------------------------------
|
||
→ ∃[x⦂ t₁ ] t₂ ↪ ∃[x⦂ t₁ ] t₂'
|
||
|
||
ξ-proj₁ : ∀ {n} {e e' : Term n}
|
||
→ e ↪ e'
|
||
→ `proj₁ e ↪ `proj₁ e'
|
||
|
||
ξ-proj₂ : ∀ {n} {e e' : Term n}
|
||
→ e ↪ e'
|
||
→ `proj₂ e ↪ `proj₂ e'
|
||
|
||
ξ-,₁ : ∀ {n} {e₁ e₁' e₂ : Term n}
|
||
→ e₁ ↪ e₁'
|
||
→ (e₁ `, e₂) ↪ (e₁' `, e₂)
|
||
|
||
ξ-,₂ : ∀ {n} {e₁ e₂ e₂' : Term n}
|
||
→ e₂ ↪ e₂'
|
||
→ (e₁ `, e₂) ↪ (e₁ `, e₂')
|
||
|
||
ξ-≡₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term n}
|
||
→ t₁ ↪ t₁'
|
||
-------------------------------
|
||
→ (t₁ `≡ t₂) ↪ (t₁' `≡ t₂)
|
||
|
||
ξ-≡₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term n}
|
||
→ t₂ ↪ t₂'
|
||
-------------------------------
|
||
→ (t₁ `≡ t₂) ↪ (t₁ `≡ t₂')
|
||
|
||
ξ-subst₁ : ∀ {n} {t t' : Term (suc n)} {e₁ e₂ : Term n}
|
||
→ t ↪ t'
|
||
→ `subst t e₁ e₂ ↪ `subst t' e₁ e₂
|
||
|
||
ξ-subst₂ : ∀ {n} {t : Term (suc n)} {e₁ e₁' e₂ : Term n}
|
||
→ e₁ ↪ e₁'
|
||
→ `subst t e₁ e₂ ↪ `subst t e₁' e₂
|
||
|
||
ξ-subst₃ : ∀ {n} {t : Term (suc n)} {e₁ e₂ e₂' : Term n}
|
||
→ e₂ ↪ e₂'
|
||
→ `subst t e₁ e₂ ↪ `subst t e₁ e₂'
|
||
|
||
-- Extension:
|
||
ξ-⊔₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term n}
|
||
→ t₁ ↪ t₁'
|
||
-------------------------------
|
||
→ (t₁ `⊔ t₂) ↪ (t₁' `⊔ t₂)
|
||
|
||
ξ-⊔₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term n}
|
||
→ t₂ ↪ t₂'
|
||
-------------------------------
|
||
→ (t₁ `⊔ t₂) ↪ (t₁ `⊔ t₂')
|
||
|
||
ξ-Setn : ∀ {n} {l l' : Term n}
|
||
→ l ↪ l'
|
||
→ `Setn l ↪ `Setn l'
|
||
|
||
ξ-Setω : ∀ {n} {l l' : Term n}
|
||
→ l ↪ l'
|
||
→ `Setω l ↪ `Setω l'
|
||
|
||
-- Reflexive, Transitive Closure of Reduction
|
||
|
||
data _↪*_ : ∀ {n} → Term n → Term n → Set where
|
||
↪*-refl : ∀ {n} {e : Term n}
|
||
→ e ↪* e
|
||
↪*-step : ∀ {n} {e₁ e₂ e₃ : Term n}
|
||
→ e₁ ↪ e₂
|
||
→ e₂ ↪* e₃
|
||
→ e₁ ↪* e₃
|
||
|
||
↪*-trans : ∀ {n} {e₁ e₂ e₃ : Term n}
|
||
→ e₁ ↪* e₂
|
||
→ e₂ ↪* e₃
|
||
→ e₁ ↪* e₃
|
||
↪*-trans ↪*-refl q = q
|
||
↪*-trans (↪*-step x p) q = ↪*-step x (↪*-trans p q)
|
||
|
||
module ↪*-Reasoning where
|
||
infix 1 begin_
|
||
infixr 2 _↪⟨_⟩_ _↪*⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
|
||
infix 3 _∎
|
||
|
||
begin_ : ∀ {n} {e₁ e₂ : Term n} → e₁ ↪* e₂ → e₁ ↪* e₂
|
||
begin p = p
|
||
|
||
_↪⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪ e₂ → e₂ ↪* e₃ → e₁ ↪* e₃
|
||
_ ↪⟨ p ⟩ q = ↪*-step p q
|
||
|
||
_↪*⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪* e₂ → e₂ ↪* e₃ → e₁ ↪* e₃
|
||
_ ↪*⟨ p ⟩ q = ↪*-trans p q
|
||
|
||
_≡⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ≡ e₂ → e₂ ↪* e₃ → e₁ ↪* e₃
|
||
_ ≡⟨ refl ⟩ q = q
|
||
|
||
_≡⟨⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪* e₂ → e₁ ↪* e₂
|
||
_ ≡⟨⟩ q = q
|
||
|
||
_∎ : ∀ {n} (e : Term n) → e ↪* e
|
||
_ ∎ = ↪*-refl
|
||
|
||
-- Conversion
|
||
|
||
-- Two terms are convertible iff they reduce to a common term.
|
||
|
||
infix 4 _≈_
|
||
record _≈_ {n} (e₁ e₂ : Term n) : Set where
|
||
constructor mk-≈
|
||
field
|
||
e-common : Term n
|
||
e₁↪*e-common : e₁ ↪* e-common
|
||
e₂↪*e-common : e₂ ↪* e-common
|
||
|
||
open _≈_ public
|
||
|
||
-- Typing ----------------------------------------------------------------------
|
||
|
||
data Context : ℕ → Set where
|
||
∅ : Context zero
|
||
_,_ : ∀ {n} → Context n → Term n → Context (suc n)
|
||
|
||
lookup : ∀ {n} → Context n → Fin n → Term n
|
||
lookup (Γ , e) zero = ren wk e
|
||
lookup (Γ , e) (suc x) = ren wk (lookup Γ x)
|
||
|
||
data _⊢_⦂_ : ∀ {n} → Context n → Term n → Term n → Set where
|
||
|
||
⊢-` : ∀ {n t} {Γ : Context n} (x : Fin n)
|
||
→ lookup Γ x ≡ t
|
||
--------------
|
||
→ Γ ⊢ ` x ⦂ t
|
||
|
||
⊢-λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ l : Term n} {t₂ : Term (suc n)}
|
||
→ Γ ⊢ t₁ ⦂ `Setn l
|
||
→ Γ , t₁ ⊢ e ⦂ t₂
|
||
-----------------------
|
||
→ Γ ⊢ `λ e ⦂ ∀[x⦂ t₁ ] t₂
|
||
|
||
⊢-· : ∀ {n} {Γ : Context n} {e₁ e₂ : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
|
||
→ Γ ⊢ e₁ ⦂ ∀[x⦂ t₁ ] t₂
|
||
→ Γ ⊢ e₂ ⦂ t₁
|
||
-----------------------
|
||
→ Γ ⊢ e₁ · e₂ ⦂ t₂ [ e₂ ]
|
||
|
||
⊢-∀ : ∀ {n} {Γ : Context n} {t₁ l₁ l₃ : Term n} {t₂ l₂ : Term (suc n)}
|
||
→ Γ ⊢ t₁ ⦂ `Setn l₁
|
||
→ Γ , t₁ ⊢ t₂ ⦂ `Setn l₂
|
||
-----------------------
|
||
→ Γ ⊢ ∀[x⦂ t₁ ] t₂ ⦂ `Setn l₃
|
||
|
||
⊢-≈ : ∀ {n} {Γ : Context n} {e : Term n} {t t' : Term n}
|
||
→ t ≈ t'
|
||
→ Γ ⊢ e ⦂ t
|
||
------------
|
||
→ Γ ⊢ e ⦂ t'
|
||
|
||
⊢-∃ : ∀ {n} {Γ : Context n} {t₁ : Term n} {t₂ : Term (suc n)}
|
||
→ Γ ⊢ t₁ ⦂ `Set
|
||
→ Γ , t₁ ⊢ t₂ ⦂ `Set
|
||
-----------------------
|
||
→ Γ ⊢ ∃[x⦂ t₁ ] t₂ ⦂ `Set
|
||
|
||
⊢-, : ∀ {n} {Γ : Context n} {e₁ e₂ : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
|
||
→ Γ ⊢ e₁ ⦂ t₁
|
||
→ Γ ⊢ e₂ ⦂ t₂ [ e₁ ]
|
||
-----------------------
|
||
→ Γ ⊢ (e₁ `, e₂) ⦂ ∃[x⦂ t₁ ] t₂
|
||
|
||
⊢-proj₁ : ∀ {n} {Γ : Context n} {e : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
|
||
→ Γ ⊢ e ⦂ ∃[x⦂ t₁ ] t₂
|
||
→ Γ ⊢ `proj₁ e ⦂ t₁
|
||
|
||
⊢-proj₂ : ∀ {n} {Γ : Context n} {e : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
|
||
→ Γ ⊢ e ⦂ ∃[x⦂ t₁ ] t₂
|
||
→ Γ ⊢ `proj₂ e ⦂ t₂ [ `proj₁ e ]
|
||
|
||
⊢-≡ : ∀ {n} {Γ : Context n} {e₁ e₂ t : Term n}
|
||
→ Γ ⊢ e₁ ⦂ t
|
||
→ Γ ⊢ e₂ ⦂ t
|
||
-----------------------
|
||
→ Γ ⊢ (e₁ `≡ e₂) ⦂ `Set
|
||
|
||
⊢-refl : ∀ {n} {Γ : Context n} {e t : Term n}
|
||
→ Γ ⊢ e ⦂ t
|
||
------------------
|
||
→ Γ ⊢ `refl ⦂ e `≡ e
|
||
|
||
⊢-subst : ∀ {n} {Γ : Context n} {e₁ e₂ u₁ u₂ : Term n} {t' : Term n} {t : Term (suc n)}
|
||
→ Γ , t' ⊢ t ⦂ `Set
|
||
→ Γ ⊢ u₁ ⦂ t'
|
||
→ Γ ⊢ u₂ ⦂ t'
|
||
→ Γ ⊢ e₁ ⦂ (u₁ `≡ u₂)
|
||
→ Γ ⊢ e₂ ⦂ t [ u₁ ]
|
||
------------------------------
|
||
→ Γ ⊢ `subst t e₁ e₂ ⦂ t [ u₂ ]
|
||
|
||
-- Extension
|
||
⊢-Setn : ∀ {n} {Γ : Context n} {l}
|
||
→ Γ ⊢ `Setn l ⦂ (`Setn (`lsuc l))
|
||
|
||
⊢-Setω : ∀ {n} {Γ : Context n} {l}
|
||
→ Γ ⊢ `Setω l ⦂ (`Setω (`lsuc l))
|
||
|
||
⊢-lzero : ∀ {n} {Γ : Context n}
|
||
→ Γ ⊢ `lzero ⦂ `Level
|
||
|
||
⊢-lsuc : ∀ {n} {Γ : Context n} {l}
|
||
→ Γ ⊢ l ⦂ `Level
|
||
→ Γ ⊢ `lsuc l ⦂ `Level
|
||
|
||
⊢-⊔ : ∀ {n} {Γ : Context n} {l₁ l₂}
|
||
→ Γ ⊢ l₁ ⦂ `Level
|
||
→ Γ ⊢ l₂ ⦂ `Level
|
||
→ Γ ⊢ (l₁ `⊔ l₂) ⦂ `Level
|
||
|
||
⊢-Level : ∀ {n} {Γ : Context n}
|
||
→ Γ ⊢ `Level ⦂ `Set
|
||
|
||
cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {x y u v a b} → x ≡ y → u ≡ v → a ≡ b → f x u a ≡ f y v b
|
||
cong₃ f refl refl refl = refl
|