13 lines
545 B
Plaintext
13 lines
545 B
Plaintext
|
-- this definition depends on coercion regularity in xtt. which is this
|
|||
|
|
-- (adapted to quox):
|
|||
|
|
--
|
|||
|
|
-- Ψ | Γ ⊢ 0 · A‹0/𝑖› = A‹1/𝑖› ⇐ ★
|
|||
|
|
-- ---------------------------------------------------------
|
|||
|
|
-- Ψ | Γ ⊢ π · coe (𝑖 ⇒ A) @p @q s ⇝ (s ∷ A‹1/𝑖›) ⇒ A‹1/𝑖›
|
|||
|
|
--
|
|||
|
|
-- otherwise, the types P (coe ⋯ s) and P s are incompatible
|
|||
|
|
|
|||
|
|
def0 reggie : (A : ★) → (AA : A ≡ A : ★) → (s : A) →
|
|||
|
|
(P : A → ★) → P (coe (𝑖 ⇒ AA @𝑖) s) → P s =
|
|||
|
|
λ A AA s P p ⇒ p
|