{-# OPTIONS --without-K --rewriting #-} module ag-000O where open import MLTT.Spartan hiding (_⊔_; id) open import ag-000M using (Ty; _⇒_; Con; ◇; _▷_) open import ag-000N {-# BUILTIN REWRITE _＝_ #-}
這邊的定義很繁瑣但只是單純攤開 V、T
就能證明，並不是很重要。重點在最後用 REWRITE
避免後續需要證明一些麻煩的情況
⊑t : s ⊑ T ⊑t {V} = v⊑t ⊑t {T} = rfl v⊑ : V ⊑ s v⊑ {V} = rfl v⊑ {T} = v⊑t ⊑q⊔ : q ⊑ (q ⊔ r) ⊑q⊔ {V}{V} = rfl ⊑q⊔ {V}{T} = v⊑t ⊑q⊔ {T}{V} = rfl ⊑q⊔ {T}{T} = rfl ⊔⊔ : q ⊔ (r ⊔ s) ＝ (q ⊔ r) ⊔ s ⊔⊔ {V}{V}{V} = refl ⊔⊔ {V}{V}{T} = refl ⊔⊔ {V}{T}{V} = refl ⊔⊔ {V}{T}{T} = refl ⊔⊔ {T}{V}{V} = refl ⊔⊔ {T}{V}{T} = refl ⊔⊔ {T}{T}{V} = refl ⊔⊔ {T}{T}{T} = refl ⊔v : q ⊔ V ＝ q ⊔v {V} = refl ⊔v {T} = refl ⊔t : q ⊔ T ＝ T ⊔t {V} = refl ⊔t {T} = refl ⊑⊔r : r ⊑ (q ⊔ r) ⊑⊔r {V}{V} = rfl ⊑⊔r {V}{T} = v⊑t ⊑⊔r {T}{V} = rfl ⊑⊔r {T}{T} = rfl ⊔-self : q ⊔ q ＝ q ⊔-self {V} = refl ⊔-self {T} = refl {-# REWRITE ⊔⊔ ⊔v ⊔t ⊔-self #-}