text:
{-# OPTIONS  --safe #-}

module Definition.Typed.Properties where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.RedSteps
import Definition.Typed.Weakening as Twk

open import Tools.Empty using (⊥; ⊥-elim)
open import Tools.Product
open import Tools.Sum hiding (id ; sym)
import Tools.PropositionalEquality as PE

import Data.Fin as Fin
import Data.Nat as Nat

-- Escape context extraction

wfTerm : ∀ {Γ A t r} → Γ ⊢ t ∷ A ^ r → ⊢ Γ
wfTerm (univ <l ⊢Γ) = ⊢Γ
wfTerm (ℕⱼ ⊢Γ) = ⊢Γ
wfTerm (Emptyⱼ ⊢Γ) = ⊢Γ
wfTerm (Πⱼ <l ▹ <l' ▹ F ▹ G) = wfTerm F
wfTerm (∃ⱼ F ▹ G) = wfTerm F
wfTerm (var ⊢Γ x₁) = ⊢Γ
wfTerm (lamⱼ _ _ F t) with wfTerm t
wfTerm (lamⱼ _ _ F t) | ⊢Γ ∙ F′ = ⊢Γ
wfTerm (g ∘ⱼ a) = wfTerm a
wfTerm (⦅ F , G , t , u ⦆ⱼ) = wfTerm t
wfTerm (fstⱼ A B t) = wfTerm t
wfTerm (sndⱼ A B t) = wfTerm t
wfTerm (zeroⱼ ⊢Γ) = ⊢Γ
wfTerm (sucⱼ n) = wfTerm n
wfTerm (natrecⱼ F z s n) = wfTerm z
wfTerm (Emptyrecⱼ A e) = wfTerm e
wfTerm (Idⱼ A t u) = wfTerm t
wfTerm (Idreflⱼ t) = wfTerm t
wfTerm (transpⱼ A P t s u e) = wfTerm t
wfTerm (castⱼ A B e t) = wfTerm t
wfTerm (castreflⱼ A t) = wfTerm t
wfTerm (conv t A≡B) = wfTerm t

wf : ∀ {Γ A r} → Γ ⊢ A ^ r → ⊢ Γ
wf (Uⱼ ⊢Γ) = ⊢Γ
wf (univ A) = wfTerm A

mutual
  wfEqTerm : ∀ {Γ A t u r} → Γ ⊢ t ≡ u ∷ A ^ r → ⊢ Γ
  wfEqTerm (refl t) = wfTerm t
  wfEqTerm (sym t≡u) = wfEqTerm t≡u
  wfEqTerm (trans t≡u u≡r) = wfEqTerm t≡u
  wfEqTerm (conv t≡u A≡B) = wfEqTerm t≡u
  wfEqTerm (Π-cong _ _ F F≡H G≡E) = wfEqTerm F≡H
  wfEqTerm (∃-cong F F≡H G≡E) = wfEqTerm F≡H
  wfEqTerm (app-cong f≡g a≡b) = wfEqTerm f≡g
  wfEqTerm (β-red _ _ F t a) = wfTerm a
  wfEqTerm (η-eq _ _ F f g f0≡g0) = wfTerm f
  wfEqTerm (suc-cong n) = wfEqTerm n
  wfEqTerm (natrec-cong F≡F′ z≡z′ s≡s′ n≡n′) = wfEqTerm z≡z′
  wfEqTerm (natrec-zero F z s) = wfTerm z
  wfEqTerm (natrec-suc n F z s) = wfTerm n
  wfEqTerm (Emptyrec-cong A≡A' _ _) = wfEq A≡A'
  wfEqTerm (proof-irrelevance t u) = wfTerm t
  wfEqTerm (Id-cong A t u) = wfEqTerm u
  wfEqTerm (Id-Π _ _ A B t u) = wfTerm t
  wfEqTerm (Id-ℕ-00 ⊢Γ) = ⊢Γ
  wfEqTerm (Id-ℕ-SS m n) = wfTerm n
  wfEqTerm (Id-U-ΠΠ A B A' B') = wfTerm A
  wfEqTerm (Id-U-ℕℕ ⊢Γ) = ⊢Γ
  wfEqTerm (Id-SProp A B) = wfTerm A
  wfEqTerm (Id-ℕ-0S n) = wfTerm n
  wfEqTerm (Id-ℕ-S0 n) = wfTerm n
  wfEqTerm (Id-U-ℕΠ A B) = wfTerm A
  wfEqTerm (Id-U-Πℕ A B) = wfTerm A
  wfEqTerm (Id-U-ΠΠ!% eq A B A' B') = wfTerm A
  wfEqTerm (cast-cong A B t _ _) = wfEqTerm t
  wfEqTerm (cast-Π A B A' B' e f) = wfTerm f
  wfEqTerm (cast-ℕ-0 e) = wfTerm e
  wfEqTerm (cast-ℕ-S e n) = wfTerm n

  wfEq : ∀ {Γ A B r} → Γ ⊢ A ≡ B ^ r → ⊢ Γ
  wfEq (univ A≡B) = wfEqTerm A≡B
  wfEq (refl A) = wf A
  wfEq (sym A≡B) = wfEq A≡B
  wfEq (trans A≡B B≡C) = wfEq A≡B

-- Reduction is a subset of conversion

subsetTerm : ∀ {Γ A t u l} → Γ ⊢ t ⇒ u ∷ A ^ l → Γ ⊢ t ≡ u ∷ A ^ [ ! , l ]
subset : ∀ {Γ A B r} → Γ ⊢ A ⇒ B ^ r → Γ ⊢ A ≡ B ^ r

subsetTerm (natrec-subst F z s n⇒n′) =
  natrec-cong (refl F) (refl z) (refl s) (subsetTerm n⇒n′)
subsetTerm (natrec-zero F z s) = natrec-zero F z s
subsetTerm (natrec-suc n F z s) = natrec-suc n F z s
subsetTerm (app-subst {rA = !} t⇒u a) = app-cong (subsetTerm t⇒u) (refl a)
subsetTerm (app-subst {rA = %} t⇒u a) = app-cong (subsetTerm t⇒u) (proof-irrelevance a a)
subsetTerm (β-red l< l<' A t a) = β-red l< l<' A t a
subsetTerm (conv t⇒u A≡B) = conv (subsetTerm t⇒u) A≡B
subsetTerm (Id-subst A t u) = Id-cong (subsetTerm A) (refl t) (refl u)
subsetTerm (Id-ℕ-subst m n) = Id-cong (refl (ℕⱼ (wfTerm n))) (subsetTerm m) (refl n)
subsetTerm (Id-ℕ-0-subst n) = let ⊢Γ = wfEqTerm (subsetTerm n) in Id-cong (refl (ℕⱼ ⊢Γ)) (refl (zeroⱼ ⊢Γ)) (subsetTerm n)
subsetTerm (Id-ℕ-S-subst m n) = Id-cong (refl (ℕⱼ (wfTerm m))) (refl (sucⱼ m)) (subsetTerm n)
subsetTerm (Id-U-subst A B) = Id-cong (refl (univ 0<1 (wfTerm B))) (subsetTerm A) (refl B)
subsetTerm (Id-U-ℕ-subst B) = let ⊢Γ = wfEqTerm (subsetTerm B) in Id-cong (refl (univ 0<1 ⊢Γ)) (refl (ℕⱼ ⊢Γ)) (subsetTerm B)
subsetTerm (Id-U-Π-subst A P B) = Id-cong (refl (univ 0<1 (wfTerm A))) (refl (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A ▹ P)) (subsetTerm B)
subsetTerm (Id-Π <l <l' A B t u) = Id-Π <l <l' A B t u
subsetTerm (Id-ℕ-00 ⊢Γ) = Id-ℕ-00 ⊢Γ
subsetTerm (Id-ℕ-SS m n) = Id-ℕ-SS m n
subsetTerm (Id-U-ΠΠ A B A' B') = Id-U-ΠΠ A B A' B'
subsetTerm (Id-U-ℕℕ ⊢Γ) = Id-U-ℕℕ ⊢Γ
subsetTerm (Id-SProp A B) = Id-SProp A B
subsetTerm (Id-ℕ-0S n) = Id-ℕ-0S n
subsetTerm (Id-ℕ-S0 n) = Id-ℕ-S0 n
subsetTerm (Id-U-ℕΠ A B) = Id-U-ℕΠ A B
subsetTerm (Id-U-Πℕ A B) = Id-U-Πℕ A B
subsetTerm (Id-U-ΠΠ!% eq A B A' B') = Id-U-ΠΠ!% eq A B A' B'
subsetTerm (cast-subst A B e t) = let ⊢Γ = wfEqTerm (subsetTerm A)
                                  in cast-cong (subsetTerm A) (refl B) (refl t) e (conv e (univ (Id-cong (refl (univ 0<1 ⊢Γ)) (subsetTerm A) (refl B))))
subsetTerm (cast-ℕ-subst B e t) = let ⊢Γ = wfEqTerm (subsetTerm B)
                                  in cast-cong (refl (ℕⱼ (wfTerm t))) (subsetTerm B) (refl t) e (conv e (univ (Id-cong (refl (univ 0<1 ⊢Γ)) (refl (ℕⱼ ⊢Γ)) (subsetTerm B))))
subsetTerm (cast-Π-subst A P B e t) = let ⊢Γ = wfTerm A
                                      in cast-cong (refl (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A ▹ P)) (subsetTerm B) (refl t) e
                                                   (conv e (univ (Id-cong (refl (univ 0<1 ⊢Γ)) (refl (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ A ▹ P)) (subsetTerm B) )))
subsetTerm (cast-Π A B A' B' e f) = cast-Π A B A' B' e f
subsetTerm (cast-ℕ-0 e) = cast-ℕ-0 e
subsetTerm (cast-ℕ-S e n) = cast-ℕ-S e n
subsetTerm (cast-ℕ-cong e n) = let ⊢Γ = wfTerm e
                                   ⊢ℕ = ℕⱼ ⊢Γ
                               in cast-cong (refl ⊢ℕ) (refl ⊢ℕ) (subsetTerm n) e e

subset (univ A⇒B) = univ (subsetTerm A⇒B)

subset*Term : ∀ {Γ A t u l } → Γ ⊢ t ⇒* u ∷ A ^ l → Γ ⊢ t ≡ u ∷ A ^ [ ! , l ]
subset*Term (id t) = refl t
subset*Term (t⇒t′ ⇨ t⇒*u) = trans (subsetTerm t⇒t′) (subset*Term t⇒*u)

subset* : ∀ {Γ A B r} → Γ ⊢ A ⇒* B ^ r → Γ ⊢ A ≡ B ^ r
subset* (id A) = refl A
subset* (A⇒A′ ⇨ A′⇒*B) = trans (subset A⇒A′) (subset* A′⇒*B)

-- Transitivity of reduction

transTerm⇒* : ∀ {Γ A t u v l } → Γ ⊢ t ⇒* u ∷ A ^ l → Γ ⊢ u ⇒* v ∷ A ^ l → Γ ⊢ t ⇒* v ∷ A ^ l
transTerm⇒* (id x) y = y
transTerm⇒* (x ⇨ x₁) y = x ⇨ transTerm⇒* x₁ y

trans⇒* : ∀ {Γ A B C r} → Γ ⊢ A ⇒* B ^ r → Γ ⊢ B ⇒* C ^ r → Γ ⊢ A ⇒* C ^ r
trans⇒* (id x) y = y
trans⇒* (x ⇨ x₁) y = x ⇨ trans⇒* x₁ y

transTerm:⇒:* : ∀ {Γ A t u v l } → Γ ⊢ t :⇒*: u ∷ A ^ l → Γ ⊢ u :⇒*: v ∷ A ^ l → Γ ⊢ t :⇒*: v ∷ A ^ l
transTerm:⇒:* [[ ⊢t , ⊢u , d ]] [[ ⊢t₁ , ⊢u₁ , d₁ ]] = [[ ⊢t , ⊢u₁ , (transTerm⇒* d d₁) ]]

conv⇒* : ∀ {Γ A B l t u} → Γ ⊢ t ⇒* u ∷ A ^ l → Γ ⊢ A ≡ B ^ [ ! , l ] → Γ ⊢ t ⇒* u ∷ B ^ l
conv⇒* (id x) e = id (conv x e)
conv⇒* (x ⇨ D) e = conv x e ⇨ conv⇒* D e

conv:⇒*: : ∀ {Γ A B l t u} → Γ ⊢ t :⇒*: u ∷ A ^ l → Γ ⊢ A ≡ B ^ [ ! , l ] → Γ ⊢ t :⇒*: u ∷ B ^ l
conv:⇒*: [[ ⊢t , ⊢u , d ]] e = [[ (conv ⊢t e) , (conv ⊢u e) , (conv⇒* d e) ]]

-- Can extract left-part of a reduction

redFirstTerm : ∀ {Γ t u A l } → Γ ⊢ t ⇒ u ∷ A ^ l → Γ ⊢ t ∷ A ^ [ ! , l ]
redFirst : ∀ {Γ A B r} → Γ ⊢ A ⇒ B ^ r → Γ ⊢ A ^ r

redFirstTerm (conv t⇒u A≡B) = conv (redFirstTerm t⇒u) A≡B
redFirstTerm (app-subst t⇒u a) = (redFirstTerm t⇒u) ∘ⱼ a
redFirstTerm (β-red {lA = lA} {lB = lB} lA< lB< ⊢A ⊢t ⊢a) = (lamⱼ lA< lB< ⊢A ⊢t) ∘ⱼ ⊢a
redFirstTerm (natrec-subst F z s n⇒n′) = natrecⱼ F z s (redFirstTerm n⇒n′)
redFirstTerm (natrec-zero F z s) = natrecⱼ F z s (zeroⱼ (wfTerm z))
redFirstTerm (natrec-suc n F z s) = natrecⱼ F z s (sucⱼ n)
redFirstTerm (Id-subst A t u) = Idⱼ (redFirstTerm A) t u
redFirstTerm (Id-ℕ-subst m n) = Idⱼ (ℕⱼ (wfTerm n)) (redFirstTerm m) n
redFirstTerm (Id-ℕ-0-subst n) = Idⱼ (ℕⱼ (wfEqTerm (subsetTerm n))) (zeroⱼ (wfEqTerm (subsetTerm n))) (redFirstTerm n)
redFirstTerm (Id-ℕ-S-subst m n) = Idⱼ (ℕⱼ (wfTerm m)) (sucⱼ m) (redFirstTerm n)
redFirstTerm (Id-U-subst A B) = Idⱼ (univ 0<1 (wfTerm B)) (redFirstTerm A) B
redFirstTerm (Id-U-ℕ-subst B) = let ⊢Γ = (wfEqTerm (subsetTerm B)) in Idⱼ (univ 0<1 ⊢Γ) (ℕⱼ ⊢Γ) (redFirstTerm B)
redFirstTerm (Id-U-Π-subst A P B) = Idⱼ (univ 0<1 (wfTerm A)) (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A ▹ P) (redFirstTerm B)
redFirstTerm (Id-Π {rA = rA} <l <l' A B t u) = Idⱼ (Πⱼ <l ▹ <l' ▹ A ▹ B) t u
redFirstTerm (Id-ℕ-00 ⊢Γ) = Idⱼ (ℕⱼ ⊢Γ) (zeroⱼ ⊢Γ) (zeroⱼ ⊢Γ)
redFirstTerm (Id-ℕ-SS m n) = Idⱼ (ℕⱼ (wfTerm m)) (sucⱼ m) (sucⱼ n)
redFirstTerm (Id-U-ΠΠ A B A' B') = Idⱼ (univ 0<1 (wfTerm A)) (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A ▹ B) (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A' ▹ B')
redFirstTerm (Id-U-ℕℕ ⊢Γ) = Idⱼ (univ 0<1 ⊢Γ) (ℕⱼ ⊢Γ) (ℕⱼ ⊢Γ)
redFirstTerm (Id-SProp A B) = Idⱼ (univ 0<1 (wfTerm A)) A B
redFirstTerm (Id-ℕ-0S n) = Idⱼ (ℕⱼ (wfTerm n)) (zeroⱼ (wfTerm n)) (sucⱼ n)
redFirstTerm (Id-ℕ-S0 n) = Idⱼ (ℕⱼ (wfTerm n)) (sucⱼ n) (zeroⱼ (wfTerm n))
redFirstTerm (Id-U-ℕΠ A B) = Idⱼ (univ 0<1 (wfTerm A)) (ℕⱼ (wfTerm A)) (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A ▹ B)
redFirstTerm (Id-U-Πℕ A B) = Idⱼ (univ 0<1 (wfTerm A)) (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A ▹ B) (ℕⱼ (wfTerm A))
redFirstTerm (Id-U-ΠΠ!% eq A B A' B') = Idⱼ (univ 0<1 (wfTerm A)) (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A ▹ B) (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A' ▹ B')
redFirstTerm (cast-subst A B e t) = castⱼ (redFirstTerm A) B e t
redFirstTerm (cast-ℕ-subst B e t) = castⱼ (ℕⱼ (wfTerm t)) (redFirstTerm B) e t
redFirstTerm (cast-Π-subst A P B e t) = castⱼ (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A ▹ P) (redFirstTerm B) e t
redFirstTerm (cast-Π A B A' B' e f) = castⱼ (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A ▹ B) (Πⱼ (≡is≤ PE.refl) ▹ (≡is≤ PE.refl) ▹ A' ▹ B') e f
redFirstTerm (cast-ℕ-0 e) = castⱼ (ℕⱼ (wfTerm e)) (ℕⱼ (wfTerm e)) e (zeroⱼ (wfTerm e))
redFirstTerm (cast-ℕ-S e n) = castⱼ (ℕⱼ (wfTerm e)) (ℕⱼ (wfTerm e)) e (sucⱼ n)
redFirstTerm (cast-ℕ-cong e n) = castⱼ (ℕⱼ (wfTerm e)) (ℕⱼ (wfTerm e)) e (redFirstTerm n)

redFirst (univ A⇒B) = univ (redFirstTerm A⇒B)

redFirst*Term : ∀ {Γ t u A l} → Γ ⊢ t ⇒* u ∷ A ^ l → Γ ⊢ t ∷ A ^ [ ! , l ]
redFirst*Term (id t) = t
redFirst*Term (t⇒t′ ⇨ t′⇒*u) = redFirstTerm t⇒t′

redFirst* : ∀ {Γ A B r} → Γ ⊢ A ⇒* B ^ r → Γ ⊢ A ^ r
redFirst* (id A) = A
redFirst* (A⇒A′ ⇨ A′⇒*B) = redFirst A⇒A′

-- Neutral types are always small

-- tyNe : ∀ {Γ t r} → Γ ⊢ t ^ r → Neutral t → Γ ⊢ t ∷ (Univ r) ^ !
-- tyNe (univ x) tn = x
-- tyNe (Idⱼ A x y) tn = Idⱼ A x y

-- Neutrals do not weak head reduce

neRedTerm : ∀ {Γ t u l A} (d : Γ ⊢ t ⇒ u ∷ A ^ l) (n : Neutral t) → ⊥
neRed : ∀ {Γ t u r} (d : Γ ⊢ t ⇒ u ^ r) (n : Neutral t) → ⊥
whnfRedTerm : ∀ {Γ t u A l} (d : Γ ⊢ t ⇒ u ∷ A ^ l) (w : Whnf t) → ⊥
whnfRed : ∀ {Γ A B r} (d : Γ ⊢ A ⇒ B ^ r) (w : Whnf A) → ⊥

neRedTerm (conv d x) n = neRedTerm d n
neRedTerm (app-subst d x) (∘ₙ n) = neRedTerm d n
neRedTerm (β-red _ _ x x₁ x₂) (∘ₙ ())
neRedTerm (natrec-zero x x₁ x₂) (natrecₙ ())
neRedTerm (natrec-suc x x₁ x₂ x₃) (natrecₙ ())
neRedTerm (natrec-subst x x₁ x₂ tr) (natrecₙ tn) = neRedTerm tr tn
neRedTerm (Id-subst tr x y) (Idₙ tn) = neRedTerm tr tn
neRedTerm (Id-ℕ-subst tr x) (Idℕₙ tn) = neRedTerm tr tn
neRedTerm (Id-ℕ-0-subst tr) (Idℕ0ₙ tn) = neRedTerm tr tn
neRedTerm (Id-ℕ-S-subst x tr) (IdℕSₙ tn) = neRedTerm tr tn
neRedTerm (Id-U-subst tr x) (IdUₙ tn) = neRedTerm tr tn
neRedTerm (Id-U-ℕ-subst tr) (IdUℕₙ tn) = neRedTerm tr tn
neRedTerm (Id-U-Π-subst A B tr) (IdUΠₙ tn) = neRedTerm tr tn
neRedTerm (Id-subst tr x y) (Idℕₙ tn) = whnfRedTerm tr ℕₙ
neRedTerm (Id-subst tr x y) (Idℕ0ₙ tn) = whnfRedTerm tr ℕₙ
neRedTerm (Id-subst tr x y) (IdℕSₙ tn) = whnfRedTerm tr ℕₙ
neRedTerm (Id-subst tr x y) (IdUₙ tn) = whnfRedTerm tr Uₙ
neRedTerm (Id-subst tr x y) (IdUℕₙ tn) = whnfRedTerm tr Uₙ
neRedTerm (Id-subst tr x y) (IdUΠₙ tn) = whnfRedTerm tr Uₙ
neRedTerm (Id-ℕ-subst tr x) (Idℕ0ₙ tn) = whnfRedTerm tr zeroₙ
neRedTerm (Id-ℕ-subst tr x) (IdℕSₙ tn) = whnfRedTerm tr sucₙ
neRedTerm (Id-U-subst tr x) (IdUℕₙ tn) = whnfRedTerm tr ℕₙ
neRedTerm (Id-U-subst tr x) (IdUΠₙ tn) = whnfRedTerm tr Πₙ
neRedTerm (Id-Π _ _ A B t u) (Idₙ ())
neRedTerm (Id-ℕ-00 tr) (Idₙ ())
neRedTerm (Id-ℕ-00 tr) (Idℕₙ ())
neRedTerm (Id-ℕ-00 tr) (Idℕ0ₙ ())
neRedTerm (Id-ℕ-SS x tr) (Idₙ ())
neRedTerm (Id-ℕ-SS x tr) (Idℕₙ ())
neRedTerm (Id-U-ΠΠ A B A' B') (Idₙ ())
neRedTerm (Id-U-ΠΠ A B A' B') (IdUₙ ())
neRedTerm (Id-U-ΠΠ A B A' B') (IdUΠₙ ())
neRedTerm (Id-U-ℕℕ x) (Idₙ ())
neRedTerm (Id-U-ℕℕ x) (IdUₙ ())
neRedTerm (Id-U-ℕℕ x) (IdUℕₙ ())
neRedTerm (Id-SProp A B) (Idₙ ())
neRedTerm (Id-ℕ-0S x) (Idₙ ())
neRedTerm (Id-ℕ-S0 x) (Idₙ ())
neRedTerm (Id-U-ℕΠ A B) (Idₙ ())
neRedTerm (Id-U-Πℕ A B) (Idₙ ())
neRedTerm (Id-U-ΠΠ!% eq A B A' B') (Idₙ ())
neRedTerm (cast-subst tr B e x) (castₙ tn) = neRedTerm tr tn
neRedTerm (cast-ℕ-subst tr e x) (castℕₙ tn) = neRedTerm tr tn
neRedTerm (cast-Π-subst A B tr e x) (castΠₙ tn) = neRedTerm tr tn
neRedTerm (cast-Π-subst A B tr e x) (castΠℕₙ) = whnfRedTerm tr ℕₙ
neRedTerm (cast-subst tr x x₁ x₂) (castℕₙ tn) = whnfRedTerm tr ℕₙ
neRedTerm (cast-subst tr x x₁ x₂) (castΠₙ tn) = whnfRedTerm tr Πₙ
neRedTerm (cast-subst tr x x₁ x₂) (castℕℕₙ tn) = whnfRedTerm tr ℕₙ
neRedTerm (cast-subst tr x x₁ x₂) (castℕΠₙ) = whnfRedTerm tr ℕₙ
neRedTerm (cast-subst tr x x₁ x₂) (castΠℕₙ) = whnfRedTerm tr Πₙ
neRedTerm (cast-ℕ-subst tr x x₁) (castℕℕₙ tn) = whnfRedTerm tr ℕₙ
neRedTerm (cast-ℕ-subst tr x x₁) (castℕΠₙ) = whnfRedTerm tr Πₙ
neRedTerm (cast-Π A B A' B' e f) (castₙ ())
neRedTerm (cast-Π A B A' B' e f) (castΠₙ ())
neRedTerm (cast-ℕ-0 x) (castₙ ())
neRedTerm (cast-ℕ-0 x) (castℕₙ ())
neRedTerm (cast-ℕ-0 x) (castℕℕₙ ())
neRedTerm (cast-ℕ-S x x₁) (castₙ ())
neRedTerm (cast-ℕ-S x x₁) (castℕₙ ())
neRedTerm (cast-ℕ-S x x₁) (castℕℕₙ ())
neRedTerm (cast-ℕ-cong x x₁) (castₙ ())
neRedTerm (cast-ℕ-cong x x₁) (castℕₙ ())
neRedTerm (cast-ℕ-cong x x₁) (castℕℕₙ t) = neRedTerm x₁ t
neRedTerm (cast-subst d x x₁ x₂) castΠΠ%!ₙ = whnfRedTerm d Πₙ
neRedTerm (cast-subst d x x₁ x₂) castΠΠ!%ₙ = whnfRedTerm d Πₙ
neRedTerm (cast-Π-subst x x₁ d x₂ x₃) castΠΠ%!ₙ = whnfRedTerm d Πₙ
neRedTerm (cast-Π-subst x x₁ d x₂ x₃) castΠΠ!%ₙ = whnfRedTerm d Πₙ

neRed (univ x) N = neRedTerm x N

whnfRedTerm (conv d x) w = whnfRedTerm d w
whnfRedTerm (app-subst d x) (ne (∘ₙ x₁)) = neRedTerm d x₁
whnfRedTerm (β-red _ _ x x₁ x₂) (ne (∘ₙ ()))
whnfRedTerm (natrec-subst x x₁ x₂ d) (ne (natrecₙ x₃)) = neRedTerm d x₃
whnfRedTerm (natrec-zero x x₁ x₂) (ne (natrecₙ ()))
whnfRedTerm (natrec-suc x x₁ x₂ x₃) (ne (natrecₙ ()))
whnfRedTerm (Id-subst d x x₁) (ne (Idₙ x₂)) = neRedTerm d x₂
whnfRedTerm (Id-subst d x x₁) (ne (Idℕₙ x₂)) = whnfRedTerm d ℕₙ
whnfRedTerm (Id-subst d x x₁) (ne (Idℕ0ₙ x₂)) = whnfRedTerm d ℕₙ
whnfRedTerm (Id-subst d x x₁) (ne (IdℕSₙ x₂)) = whnfRedTerm d ℕₙ
whnfRedTerm (Id-subst d x x₁) (ne (IdUₙ x₂)) = whnfRedTerm d Uₙ
whnfRedTerm (Id-subst d x x₁) (ne (IdUℕₙ x₂)) = whnfRedTerm d Uₙ
whnfRedTerm (Id-subst d x x₁) (ne (IdUΠₙ x₂)) = whnfRedTerm d Uₙ
whnfRedTerm (Id-ℕ-subst d x) (ne (Idℕₙ x₁)) = neRedTerm d x₁
whnfRedTerm (Id-ℕ-subst d x) (ne (Idℕ0ₙ x₁)) = whnfRedTerm d zeroₙ
whnfRedTerm (Id-ℕ-subst d x) (ne (IdℕSₙ x₁)) = whnfRedTerm d sucₙ
whnfRedTerm (Id-ℕ-0-subst d) (ne (Idℕ0ₙ x)) = neRedTerm d x
whnfRedTerm (Id-ℕ-S-subst x d) (ne (IdℕSₙ x₁)) = neRedTerm d x₁
whnfRedTerm (Id-U-subst d x) (ne (IdUₙ x₁)) = neRedTerm d x₁
whnfRedTerm (Id-U-subst d x) (ne (IdUℕₙ x₁)) = whnfRedTerm d ℕₙ
whnfRedTerm (Id-U-subst d x) (ne (IdUΠₙ x₁)) = whnfRedTerm d Πₙ
whnfRedTerm (Id-U-ℕ-subst d) (ne (IdUℕₙ x)) = neRedTerm d x
whnfRedTerm (Id-U-Π-subst x x₁ d) (ne (IdUΠₙ x₂)) = neRedTerm d x₂
whnfRedTerm (Id-Π _ _ x x₁ x₂ x₃) (ne (Idₙ ()))
whnfRedTerm (Id-ℕ-00 x) (ne (Idₙ ()))
whnfRedTerm (Id-ℕ-00 x) (ne (Idℕₙ ()))
whnfRedTerm (Id-ℕ-00 x) (ne (Idℕ0ₙ ()))
whnfRedTerm (Id-ℕ-SS x x₁) (ne (Idₙ ()))
whnfRedTerm (Id-ℕ-SS x x₁) (ne (Idℕₙ ()))
whnfRedTerm (Id-ℕ-SS x x₁) (ne (IdℕSₙ ()))
whnfRedTerm (Id-U-ΠΠ x x₁ x₂ x₃) (ne (Idₙ ()))
whnfRedTerm (Id-U-ΠΠ x x₁ x₂ x₃) (ne (IdUₙ ()))
whnfRedTerm (Id-U-ΠΠ x x₁ x₂ x₃) (ne (IdUΠₙ ()))
whnfRedTerm (Id-U-ℕℕ x) (ne (Idₙ ()))
whnfRedTerm (Id-U-ℕℕ x) (ne (IdUₙ ()))
whnfRedTerm (Id-U-ℕℕ x) (ne (IdUℕₙ ()))
whnfRedTerm (Id-SProp x x₁) (ne (Idₙ ()))
whnfRedTerm (Id-ℕ-0S x) (ne (Idₙ ()))
whnfRedTerm (Id-ℕ-S0 x) (ne (Idₙ ()))
whnfRedTerm (Id-U-ℕΠ A B) (ne (Idₙ ()))
whnfRedTerm (Id-U-Πℕ A B) (ne (Idₙ ()))
whnfRedTerm (Id-U-ΠΠ!% eq A B A' B') (ne (Idₙ ()))
whnfRedTerm (cast-subst d x x₁ x₂) (ne (castₙ x₃)) = neRedTerm d x₃
whnfRedTerm (cast-subst d x x₁ x₂) (ne (castℕₙ x₃)) = whnfRedTerm d ℕₙ
whnfRedTerm (cast-subst d x x₁ x₂) (ne (castΠₙ x₃)) = whnfRedTerm d Πₙ
whnfRedTerm (cast-subst d x x₁ x₂) (ne (castℕℕₙ x₃)) = whnfRedTerm d ℕₙ
whnfRedTerm (cast-subst d x x₁ x₂) (ne castℕΠₙ) = whnfRedTerm d ℕₙ
whnfRedTerm (cast-subst d x x₁ x₂) (ne castΠℕₙ) = whnfRedTerm d Πₙ
whnfRedTerm (cast-ℕ-subst d x x₁) (ne (castℕₙ x₂)) = neRedTerm d x₂
whnfRedTerm (cast-ℕ-subst d x x₁) (ne (castℕℕₙ x₂)) = whnfRedTerm d ℕₙ
whnfRedTerm (cast-ℕ-subst d x x₁) (ne castℕΠₙ) = whnfRedTerm d Πₙ
whnfRedTerm (cast-Π-subst x x₁ d x₂ x₃) (ne (castΠₙ x₄)) = neRedTerm d x₄
whnfRedTerm (cast-Π-subst x x₁ d x₂ x₃) (ne castΠℕₙ) = whnfRedTerm d ℕₙ
whnfRedTerm (cast-Π x x₁ x₂ x₃ x₄ x₅) (ne (castₙ ()))
whnfRedTerm (cast-Π x x₁ x₂ x₃ x₄ x₅) (ne (castΠₙ ()))
whnfRedTerm (cast-ℕ-0 x) (ne (castₙ ()))
whnfRedTerm (cast-ℕ-0 x) (ne (castℕₙ ()))
whnfRedTerm (cast-ℕ-0 x) (ne (castℕℕₙ ()))
whnfRedTerm (cast-ℕ-S x x₁) (ne (castₙ ()))
whnfRedTerm (cast-ℕ-S x x₁) (ne (castℕₙ ()))
whnfRedTerm (cast-ℕ-S x x₁) (ne (castℕℕₙ ()))
whnfRedTerm (cast-ℕ-cong x x₁) (ne (castₙ ()))
whnfRedTerm (cast-ℕ-cong x x₁) (ne (castℕₙ ()))
whnfRedTerm (cast-ℕ-cong x x₁) (ne (castℕℕₙ t)) = neRedTerm x₁ t
whnfRedTerm (cast-subst d x x₁ x₂) (ne castΠΠ%!ₙ) = whnfRedTerm d Πₙ
whnfRedTerm (cast-subst d x x₁ x₂) (ne castΠΠ!%ₙ) = whnfRedTerm d Πₙ
whnfRedTerm (cast-Π-subst x x₁ d x₂ x₃) (ne castΠΠ%!ₙ) = whnfRedTerm d Πₙ
whnfRedTerm (cast-Π-subst x x₁ d x₂ x₃) (ne castΠΠ!%ₙ) = whnfRedTerm d Πₙ

whnfRed (univ x) w = whnfRedTerm x w

whnfRed*Term : ∀ {Γ t u A l} (d : Γ ⊢ t ⇒* u ∷ A ^ l) (w : Whnf t) → t PE.≡ u
whnfRed*Term (id x) Uₙ = PE.refl
whnfRed*Term (id x) Πₙ = PE.refl
whnfRed*Term (id x) ∃ₙ = PE.refl
whnfRed*Term (id x) ℕₙ = PE.refl
whnfRed*Term (id x) Emptyₙ = PE.refl
whnfRed*Term (id x) lamₙ = PE.refl
whnfRed*Term (id x) zeroₙ = PE.refl
whnfRed*Term (id x) sucₙ = PE.refl
whnfRed*Term (id x) (ne x₁) = PE.refl
whnfRed*Term (conv x x₁ ⇨ d) w = ⊥-elim (whnfRedTerm x w)
whnfRed*Term (x ⇨ d) (ne x₁) = ⊥-elim (neRedTerm x x₁)

whnfRed* : ∀ {Γ A B r} (d : Γ ⊢ A ⇒* B ^ r) (w : Whnf A) → A PE.≡ B
whnfRed* (id x) w = PE.refl
whnfRed* (x ⇨ d) w = ⊥-elim (whnfRed x w)

-- Whr is deterministic

-- somehow the cases (cast-Π, cast-Π) and (Id-U-ΠΠ, Id-U-ΠΠ) fail if
-- we do not introduce a dummy relevance rA'. This is why we need the two
-- auxiliary functions.
whrDetTerm-aux1 : ∀{Γ t u F lF A A' rA lA lB rA' l B B' e f}
  → (d :  t PE.≡ cast l (Π A ^ rA ° lA ▹ B ° lB ° l) (Π A' ^ rA' ° lA ▹ B' ° lB ° l) e f)
  → (d′ : Γ ⊢ t ⇒ u ∷ F ^ lF)
  → (lam A' ▹ (let a = cast l (wk1 A') (wk1 A) (Idsym (Univ rA l) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0) in cast l (B [ a ]↑) B' ((snd (wk1 e)) ∘ (var 0) ^ ¹) ((wk1 f) ∘ a ^ l)) ^ l) PE.≡ u
whrDetTerm-aux1 d (conv d' x) = whrDetTerm-aux1 d d'
whrDetTerm-aux1 PE.refl (cast-subst d' x x₁ x₂) = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm-aux1 PE.refl (cast-Π-subst x x₁ d' x₂ x₃) = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm-aux1 PE.refl (cast-Π x x₁ x₂ x₃ x₄ x₅) = PE.refl

whrDetTerm-aux2 : ∀{Γ t u F lF A rA B A' rA' B'}
  → (rA≡rA' : rA PE.≡ rA')
  → (d : t PE.≡ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA' ° ⁰ ▹ B' ° ⁰ ° ⁰))
  → (d' : Γ ⊢ t ⇒ u ∷ F ^ lF)
  → (∃ (Id (Univ rA ⁰) A A') ▹ (Π (wk1 A') ^ rA ° ⁰ ▹ Id (U ⁰) ((wk (lift (step id)) B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑) (wk (lift (step id)) B') ° ¹ ° ¹ ) ) PE.≡ u
whrDetTerm-aux2 eq d (conv d' x) = whrDetTerm-aux2 eq d d'
whrDetTerm-aux2 _ PE.refl (Id-subst d' x x₁) = ⊥-elim (whnfRedTerm d' Uₙ)
whrDetTerm-aux2 _ PE.refl (Id-U-subst d' x) = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm-aux2 _ PE.refl (Id-U-Π-subst x x₁ d') = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm-aux2 _ PE.refl (Id-U-ΠΠ x x₁ x₂ x₃) = PE.refl
whrDetTerm-aux2 PE.refl PE.refl (Id-U-ΠΠ!% eq A B A' B') = ⊥-elim (eq PE.refl)
whrDetTerm : ∀{Γ t u A l u′ A′ l′} (d : Γ ⊢ t ⇒ u ∷ A ^ l) (d′ : Γ ⊢ t ⇒ u′ ∷ A′ ^ l′) → u PE.≡ u′
whrDet : ∀{Γ A B B′ r r'} (d : Γ ⊢ A ⇒ B ^ r) (d′ : Γ ⊢ A ⇒ B′ ^ r') → B PE.≡ B′

whrDetTerm (conv d x) d′ = whrDetTerm d d′
whrDetTerm (app-subst d x) (app-subst d′ x₁) rewrite whrDetTerm d d′ = PE.refl
whrDetTerm (app-subst d x) (β-red _ _ x₁ x₂ x₃) = ⊥-elim (whnfRedTerm d lamₙ)
whrDetTerm (β-red _ _ x x₁ x₂) (app-subst d' x₃) = ⊥-elim (whnfRedTerm d' lamₙ)
whrDetTerm (β-red _ _ x x₁ x₂) (β-red _ _ x₃ x₄ x₅) = PE.refl
whrDetTerm (natrec-subst x x₁ x₂ d) (natrec-subst x₃ x₄ x₅ d') rewrite whrDetTerm d d' = PE.refl
whrDetTerm (natrec-subst x x₁ x₂ d) (natrec-zero x₃ x₄ x₅) = ⊥-elim (whnfRedTerm d zeroₙ)
whrDetTerm (natrec-subst x x₁ x₂ d) (natrec-suc x₃ x₄ x₅ x₆) = ⊥-elim (whnfRedTerm d sucₙ)
whrDetTerm (natrec-zero x x₁ x₂) (natrec-subst x₃ x₄ x₅ d') = ⊥-elim (whnfRedTerm d' zeroₙ)
whrDetTerm (natrec-zero x x₁ x₂) (natrec-zero x₃ x₄ x₅) = PE.refl
whrDetTerm (natrec-suc x x₁ x₂ x₃) (natrec-subst x₄ x₅ x₆ d') = ⊥-elim (whnfRedTerm d' sucₙ)
whrDetTerm (natrec-suc x x₁ x₂ x₃) (natrec-suc x₄ x₅ x₆ x₇) = PE.refl
whrDetTerm (Id-subst d x x₁) (Id-subst d' x₂ x₃) rewrite whrDetTerm d d' = PE.refl
whrDetTerm (Id-subst d x x₁) (Id-ℕ-subst d' x₂) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-subst d x x₁) (Id-ℕ-0-subst d') = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-subst d x x₁) (Id-ℕ-S-subst x₂ d') = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-subst d x x₁) (Id-U-subst d' x₂) = ⊥-elim (whnfRedTerm d Uₙ)
whrDetTerm (Id-subst d x x₁) (Id-U-ℕ-subst d') = ⊥-elim (whnfRedTerm d Uₙ)
whrDetTerm (Id-subst d x x₁) (Id-U-Π-subst x₂ x₃ d') = ⊥-elim (whnfRedTerm d Uₙ)
whrDetTerm (Id-subst d x x₁) (Id-Π _ _ x₂ x₃ x₄ x₅) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (Id-subst d x x₁) (Id-ℕ-00 x₂) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-subst d x x₁) (Id-ℕ-SS x₂ x₃) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-subst d x x₁) (Id-U-ΠΠ x₂ x₃ x₄ x₅) = ⊥-elim (whnfRedTerm d Uₙ)
whrDetTerm (Id-subst d x x₁) (Id-U-ℕℕ x₂) = ⊥-elim (whnfRedTerm d Uₙ)
whrDetTerm (Id-subst d x x₁) (Id-SProp x₂ x₃) = ⊥-elim (whnfRedTerm d Uₙ)
whrDetTerm (Id-subst d x x₁) (Id-ℕ-0S x₂) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-subst d x x₁) (Id-ℕ-S0 x₂) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-subst d x x₁) (Id-U-ℕΠ x₂ x₃) = ⊥-elim (whnfRedTerm d Uₙ)
whrDetTerm (Id-subst d x x₁) (Id-U-Πℕ x₂ x₃) = ⊥-elim (whnfRedTerm d Uₙ)
whrDetTerm (Id-subst d x x₁) (Id-U-ΠΠ!% x₂ x₃ x₄ x₅ x₆) = ⊥-elim (whnfRedTerm d Uₙ)
whrDetTerm (Id-ℕ-subst d x) (Id-subst d' x₁ x₂) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-ℕ-subst d x) (Id-ℕ-subst d' x₁) rewrite whrDetTerm d d' = PE.refl
whrDetTerm (Id-ℕ-subst d x) (Id-ℕ-0-subst d') = ⊥-elim (whnfRedTerm d zeroₙ)
whrDetTerm (Id-ℕ-subst d x) (Id-ℕ-S-subst x₁ d') = ⊥-elim (whnfRedTerm d sucₙ)
whrDetTerm (Id-ℕ-subst d x) (Id-ℕ-00 x₁) = ⊥-elim (whnfRedTerm d zeroₙ)
whrDetTerm (Id-ℕ-subst d x) (Id-ℕ-SS x₁ x₂) = ⊥-elim (whnfRedTerm d sucₙ)
whrDetTerm (Id-ℕ-subst d x) (Id-ℕ-0S x₁) = ⊥-elim (whnfRedTerm d zeroₙ)
whrDetTerm (Id-ℕ-subst d x) (Id-ℕ-S0 x₁) = ⊥-elim (whnfRedTerm d sucₙ)
whrDetTerm (Id-ℕ-0-subst d) (Id-subst d' x x₁) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-ℕ-0-subst d) (Id-ℕ-subst d' x) = ⊥-elim (whnfRedTerm d' zeroₙ)
whrDetTerm (Id-ℕ-0-subst d) (Id-ℕ-0-subst d') rewrite whrDetTerm d d' = PE.refl
whrDetTerm (Id-ℕ-0-subst d) (Id-ℕ-00 x) = ⊥-elim (whnfRedTerm d zeroₙ)
whrDetTerm (Id-ℕ-0-subst d) (Id-ℕ-0S x) = ⊥-elim (whnfRedTerm d sucₙ)
whrDetTerm (Id-ℕ-S-subst x d) (Id-subst d' x₁ x₂) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-ℕ-S-subst x d) (Id-ℕ-subst d' x₁) = ⊥-elim (whnfRedTerm d' sucₙ)
whrDetTerm (Id-ℕ-S-subst x d) (Id-ℕ-S-subst x₁ d') rewrite whrDetTerm d d' = PE.refl
whrDetTerm (Id-ℕ-S-subst x d) (Id-ℕ-SS x₁ x₂) = ⊥-elim (whnfRedTerm d sucₙ)
whrDetTerm (Id-ℕ-S-subst x d) (Id-ℕ-S0 x₁) = ⊥-elim (whnfRedTerm d zeroₙ)
whrDetTerm (Id-U-subst d x) (Id-subst d' x₁ x₂) = ⊥-elim (whnfRedTerm d' Uₙ)
whrDetTerm (Id-U-subst d x) (Id-U-subst d' x₁) rewrite whrDetTerm d d' = PE.refl
whrDetTerm (Id-U-subst d x) (Id-U-ℕ-subst d') = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-U-subst d x) (Id-U-Π-subst x₁ x₂ d') = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (Id-U-subst d x) (Id-U-ΠΠ x₁ x₂ x₃ x₄) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (Id-U-subst d x) (Id-U-ℕℕ x₁) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-U-subst d x) (Id-U-ℕΠ x₁ x₂) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-U-subst d x) (Id-U-Πℕ x₁ x₂) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (Id-U-subst d x) (Id-U-ΠΠ!% x₁ x₂ x₃ x₄ x₅) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (Id-U-ℕ-subst d) (Id-subst d' x x₁) = ⊥-elim (whnfRedTerm d' Uₙ)
whrDetTerm (Id-U-ℕ-subst d) (Id-U-subst d' x) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-U-ℕ-subst d) (Id-U-ℕ-subst d') rewrite whrDetTerm d d' = PE.refl
whrDetTerm (Id-U-ℕ-subst d) (Id-U-ℕℕ x) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-U-ℕ-subst d) (Id-U-ℕΠ x x₁) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (Id-U-Π-subst x x₁ d) (Id-subst d' x₂ x₃) = ⊥-elim (whnfRedTerm d' Uₙ)
whrDetTerm (Id-U-Π-subst x x₁ d) (Id-U-subst d' x₂) = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm (Id-U-Π-subst x x₁ d) (Id-U-Π-subst x₂ x₃ d') rewrite whrDetTerm d d' = PE.refl
whrDetTerm (Id-U-Π-subst x x₁ d) (Id-U-ΠΠ x₂ x₃ x₄ x₅) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (Id-U-Π-subst x x₁ d) (Id-U-Πℕ x₂ x₃) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (Id-U-Π-subst x x₁ d) (Id-U-ΠΠ!% x₂ x₃ x₄ x₅ x₆) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (Id-Π _ _ x x₁ x₂ x₃) (Id-subst d' x₄ x₅) = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm (Id-Π _ _ x x₁ x₂ x₃) (Id-Π _ _ x₄ x₅ x₆ x₇) = PE.refl
whrDetTerm (Id-ℕ-00 x) (Id-subst d' x₁ x₂) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-ℕ-00 x) (Id-ℕ-subst d' x₁) = ⊥-elim (whnfRedTerm d' zeroₙ)
whrDetTerm (Id-ℕ-00 x) (Id-ℕ-0-subst d') = ⊥-elim (whnfRedTerm d' zeroₙ)
whrDetTerm (Id-ℕ-00 x) (Id-ℕ-00 x₁) = PE.refl
whrDetTerm (Id-ℕ-SS x x₁) (Id-subst d' x₂ x₃) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-ℕ-SS x x₁) (Id-ℕ-subst d' x₂) = ⊥-elim (whnfRedTerm d' sucₙ)
whrDetTerm (Id-ℕ-SS x x₁) (Id-ℕ-S-subst x₂ d') = ⊥-elim (whnfRedTerm d' sucₙ)
whrDetTerm (Id-ℕ-SS x x₁) (Id-ℕ-SS x₂ x₃) = PE.refl
whrDetTerm (Id-U-ΠΠ x x₁ x₂ x₃) d' = whrDetTerm-aux2 PE.refl PE.refl d'
whrDetTerm (Id-U-ℕℕ x) (Id-subst d' x₁ x₂) = ⊥-elim (whnfRedTerm d' Uₙ)
whrDetTerm (Id-U-ℕℕ x) (Id-U-subst d' x₁) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-U-ℕℕ x) (Id-U-ℕ-subst d') = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-U-ℕℕ x) (Id-U-ℕℕ x₁) = PE.refl
whrDetTerm (Id-SProp x x₁) (Id-subst d' x₂ x₃) = ⊥-elim (whnfRedTerm d' Uₙ)
whrDetTerm (Id-SProp x x₁) (Id-SProp x₂ x₃) = PE.refl
whrDetTerm (Id-ℕ-0S x) (Id-subst d' x₁ x₂) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-ℕ-0S x) (Id-ℕ-subst d' x₁) = ⊥-elim (whnfRedTerm d' zeroₙ)
whrDetTerm (Id-ℕ-0S x) (Id-ℕ-0-subst d') = ⊥-elim (whnfRedTerm d' sucₙ)
whrDetTerm (Id-ℕ-0S x) (Id-ℕ-0S x₁) = PE.refl
whrDetTerm (Id-ℕ-S0 x) (Id-subst d' x₁ x₂) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-ℕ-S0 x) (Id-ℕ-subst d' x₁) = ⊥-elim (whnfRedTerm d' sucₙ)
whrDetTerm (Id-ℕ-S0 x) (Id-ℕ-S-subst x₁ d') = ⊥-elim (whnfRedTerm d' zeroₙ)
whrDetTerm (Id-ℕ-S0 x) (Id-ℕ-S0 x₁) = PE.refl
whrDetTerm (Id-U-ℕΠ x x₁) (Id-subst d' x₂ x₃) = ⊥-elim (whnfRedTerm d' Uₙ)
whrDetTerm (Id-U-ℕΠ x x₁) (Id-U-subst d' x₂) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-U-ℕΠ x x₁) (Id-U-ℕ-subst d') = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm (Id-U-ℕΠ x x₁) (Id-U-ℕΠ x₂ x₃) = PE.refl
whrDetTerm (Id-U-Πℕ x x₁) (Id-subst d' x₂ x₃) = ⊥-elim (whnfRedTerm d' Uₙ)
whrDetTerm (Id-U-Πℕ x x₁) (Id-U-subst d' x₂) = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm (Id-U-Πℕ x x₁) (Id-U-Π-subst x₂ x₃ d') = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (Id-U-Πℕ x x₁) (Id-U-Πℕ x₂ x₃) = PE.refl
whrDetTerm (Id-U-ΠΠ!% eq A B A' B') (Id-subst d' x x₁) = ⊥-elim (whnfRedTerm d' Uₙ)
whrDetTerm (Id-U-ΠΠ!% eq A B A' B') (Id-U-subst d' x) = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm (Id-U-ΠΠ!% eq A B A' B') (Id-U-Π-subst x x₁ d') = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm (Id-U-ΠΠ!% eq A B A' B') (Id-U-ΠΠ x x₁ x₂ x₃) = ⊥-elim (eq PE.refl)
whrDetTerm (Id-U-ΠΠ!% eq A B A' B') (Id-U-ΠΠ!% x x₁ x₂ x₃ x₄) = PE.refl
whrDetTerm (cast-subst d x x₁ x₂) (cast-subst d' x₃ x₄ x₅) rewrite whrDetTerm d d' = PE.refl
whrDetTerm (cast-subst d x x₁ x₂) (cast-ℕ-subst d' x₃ x₄) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (cast-subst d x x₁ x₂) (cast-Π-subst x₃ x₄ d' x₅ x₆) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (cast-subst d x x₁ x₂) (cast-Π x₃ x₄ x₅ x₆ x₇ x₈) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (cast-subst d x x₁ x₂) (cast-ℕ-0 x₃) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (cast-subst d x x₁ x₂) (cast-ℕ-S x₃ x₄) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (cast-ℕ-subst d x x₁) (cast-subst d' x₂ x₃ x₄) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (cast-ℕ-subst d x x₁) (cast-ℕ-subst d' x₂ x₃) rewrite whrDetTerm d d' = PE.refl
whrDetTerm (cast-ℕ-subst d x x₁) (cast-ℕ-0 x₂) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (cast-ℕ-subst d x x₁) (cast-ℕ-S x₂ x₃) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (cast-Π-subst x x₁ d x₂ x₃) (cast-subst d' x₄ x₅ x₆) = ⊥-elim (whnfRedTerm d' Πₙ)
whrDetTerm (cast-Π-subst x x₁ d x₂ x₃) (cast-Π-subst x₄ x₅ d' x₆ x₇) rewrite whrDetTerm d d' = PE.refl
whrDetTerm (cast-Π-subst x x₁ d x₂ x₃) (cast-Π x₄ x₅ x₆ x₇ x₈ x₉) = ⊥-elim (whnfRedTerm d Πₙ)
whrDetTerm (cast-Π x x₁ x₂ x₃ x₄ x₅) d' = whrDetTerm-aux1 (PE.refl) d'
whrDetTerm (cast-ℕ-0 x) (cast-subst d' x₁ x₂ x₃) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (cast-ℕ-0 x) (cast-ℕ-subst d' x₁ x₂) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (cast-ℕ-0 x) (cast-ℕ-0 x₁) = PE.refl
whrDetTerm (cast-ℕ-S x x₁) (cast-subst d' x₂ x₃ x₄) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (cast-ℕ-S x x₁) (cast-ℕ-subst d' x₂ x₃) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (cast-ℕ-S x x₁) (cast-ℕ-S x₂ x₃) = PE.refl
whrDetTerm (cast-ℕ-cong x x₁) (cast-subst d' x₂ x₃ x₄) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (cast-ℕ-cong x x₁) (cast-ℕ-subst d' x₂ x₃) = ⊥-elim (whnfRedTerm d' ℕₙ)
whrDetTerm (cast-ℕ-cong x x₁) (cast-ℕ-cong x₂ x₃) rewrite whrDetTerm x₁ x₃ = PE.refl --
whrDetTerm (cast-subst d x x₁ x₂) (cast-ℕ-cong x₃ d′) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (cast-ℕ-subst d x x₁) (cast-ℕ-cong x₂ d′) = ⊥-elim (whnfRedTerm d ℕₙ)
whrDetTerm (cast-ℕ-0 x) (cast-ℕ-cong x₁ d′) = ⊥-elim (whnfRedTerm d′ zeroₙ)
whrDetTerm (cast-ℕ-S x x₁) (cast-ℕ-cong x₂ d′) = ⊥-elim (whnfRedTerm d′ sucₙ)
whrDetTerm (cast-ℕ-cong x d) (cast-ℕ-0 x₁) = ⊥-elim (whnfRedTerm d zeroₙ)
whrDetTerm (cast-ℕ-cong x d) (cast-ℕ-S x₁ x₂) = ⊥-elim (whnfRedTerm d sucₙ)

{-# CATCHALL #-}
whrDetTerm d (conv d′ x₁) = whrDetTerm d d′

whrDet (univ x) (univ x₁) = whrDetTerm x x₁

whrDet↘Term : ∀{Γ t u A l u′} (d : Γ ⊢ t ↘ u ∷ A ^ l) (d′ : Γ ⊢ t ⇒* u′ ∷ A ^ l)
  → Γ ⊢ u′ ⇒* u ∷ A ^ l
whrDet↘Term (proj₁ , proj₂) (id x) = proj₁
whrDet↘Term (id x , proj₂) (x₁ ⇨ d′) = ⊥-elim (whnfRedTerm x₁ proj₂)
whrDet↘Term (x ⇨ proj₁ , proj₂) (x₁ ⇨ d′) =
  whrDet↘Term (PE.subst (λ x₂ → _ ⊢ x₂ ↘ _ ∷ _ ^ _) (whrDetTerm x x₁) (proj₁ , proj₂)) d′

whrDet*Term : ∀{Γ t u A A' l u′ } (d : Γ ⊢ t ↘ u ∷ A ^ l) (d′ : Γ ⊢ t ↘ u′ ∷ A' ^ l) → u PE.≡ u′
whrDet*Term (id x , proj₂) (id x₁ , proj₄) = PE.refl
whrDet*Term (id x , proj₂) (x₁ ⇨ proj₃ , proj₄) = ⊥-elim (whnfRedTerm x₁ proj₂)
whrDet*Term (x ⇨ proj₁ , proj₂) (id x₁ , proj₄) = ⊥-elim (whnfRedTerm x proj₄)
whrDet*Term (x ⇨ proj₁ , proj₂) (x₁ ⇨ proj₃ , proj₄) =
  whrDet*Term (proj₁ , proj₂) (PE.subst (λ x₂ → _ ⊢ x₂ ↘ _ ∷ _ ^ _)
                                    (whrDetTerm x₁ x) (proj₃ , proj₄))

whrDet* : ∀{Γ A B B′ r r'} (d : Γ ⊢ A ↘ B ^ r) (d′ : Γ ⊢ A ↘ B′ ^ r') → B PE.≡ B′
whrDet* (id x , proj₂) (id x₁ , proj₄) = PE.refl
whrDet* (id x , proj₂) (x₁ ⇨ proj₃ , proj₄) = ⊥-elim (whnfRed x₁ proj₂)
whrDet* (x ⇨ proj₁ , proj₂) (id x₁ , proj₄) = ⊥-elim (whnfRed x proj₄)
whrDet* (A⇒A′ ⇨ A′⇒*B , whnfB) (A⇒A″ ⇨ A″⇒*B′ , whnfB′) =
  whrDet* (A′⇒*B , whnfB) (PE.subst (λ x → _ ⊢ x ↘ _ ^ _ )
                                     (whrDet A⇒A″ A⇒A′)
                                     (A″⇒*B′ , whnfB′))

-- Identity of syntactic reduction

idRed:*: : ∀ {Γ A r} → Γ ⊢ A ^ r → Γ ⊢ A :⇒*: A ^ r
idRed:*: A = [[ A , A , id A ]]

idRedTerm:*: : ∀ {Γ A l t} → Γ ⊢ t ∷ A ^ [ ! , l ] → Γ ⊢ t :⇒*: t ∷ A ^ l
idRedTerm:*: t = [[ t , t , id t ]]

-- U cannot be a term

UnotInA : ∀ {A Γ r r'} → Γ ⊢ (Univ r ¹) ∷ A ^ r' → ⊥
UnotInA (conv U∷U x) = UnotInA U∷U

UnotInA[t] : ∀ {A B t a Γ r r' r'' r'''}
         → t [ a ] PE.≡ (Univ r ¹)
         → Γ ⊢ a ∷ A ^ r'
         → Γ ∙ A ^ r'' ⊢ t ∷ B ^ r'''
         → ⊥
UnotInA[t] () x₁ (univ 0<1 x₂)
UnotInA[t] () x₁ (ℕⱼ x₂)
UnotInA[t] () x₁ (Emptyⱼ x₂)
UnotInA[t] () x₁ (Πⱼ _ ▹ _ ▹ x₂ ▹ x₃)
UnotInA[t] x₁ x₂ (var x₃ here) rewrite x₁ = UnotInA x₂
UnotInA[t] () x₂ (var x₃ (there x₄))
UnotInA[t] () x₁ (lamⱼ _ _ x₂ x₃)
UnotInA[t] () x₁ (x₂ ∘ⱼ x₃)
UnotInA[t] () x₁ (zeroⱼ x₂)
UnotInA[t] () x₁ (sucⱼ x₂)
UnotInA[t] () x₁ (natrecⱼ x₂ x₃ x₄ x₅)
UnotInA[t] () x₁ (Emptyrecⱼ x₂ x₃)
UnotInA[t] x x₁ (conv x₂ x₃) = UnotInA[t] x x₁ x₂

redU*Term′ : ∀ {A B U′ l Γ r} → U′ PE.≡ (Univ r ¹) → Γ ⊢ A ⇒ U′ ∷ B ^ l → ⊥
redU*Term′ U′≡U (conv A⇒U x) = redU*Term′ U′≡U A⇒U
redU*Term′ () (app-subst A⇒U x)
redU*Term′ U′≡U (β-red _ _ x x₁ x₂) = UnotInA[t] U′≡U x₂ x₁
redU*Term′ () (natrec-subst x x₁ x₂ A⇒U)
redU*Term′ U′≡U (natrec-zero x x₁ x₂) rewrite U′≡U = UnotInA x₁
redU*Term′ () (natrec-suc x x₁ x₂ x₃)

redU*Term : ∀ {A B l Γ r} → Γ ⊢ A ⇒* (Univ r ¹) ∷ B ^ l → ⊥
redU*Term (id x) = UnotInA x
redU*Term (x ⇨ A⇒*U) = redU*Term A⇒*U

-- Nothing reduces to U

redU : ∀ {A Γ r l } → Γ ⊢ A ⇒ (Univ r ¹) ^ [ ! , l ] → ⊥
redU (univ x) = redU*Term′ PE.refl x

redU* : ∀ {A Γ r l } → Γ ⊢ A ⇒* (Univ r ¹) ^ [ ! , l ] → A PE.≡ (Univ r ¹)
redU* (id x) = PE.refl
redU* (x ⇨ A⇒*U) rewrite redU* A⇒*U = ⊥-elim (redU x)

-- convertibility for irrelevant terms implies typing

typeInversion : ∀ {t u A l Γ} → Γ ⊢ t ≡ u ∷ A ^ [ % , l ] → Γ ⊢ t ∷ A ^ [ % , l ]
typeInversion (conv X x) = let d = typeInversion X in conv d x
typeInversion (proof-irrelevance x x₁) = x

-- general version of reflexivity, symmetry and transitivity

genRefl : ∀ {A Γ t r l } → Γ ⊢ t ∷ A ^ [ r , l ] → Γ ⊢ t ≡ t ∷ A ^ [ r , l ]
genRefl {r = !} d = refl d
genRefl {r = %} d = proof-irrelevance d d

-- Judgmental instance of the equality relation

genSym : ∀ {k l A Γ r lA } → Γ ⊢ k ≡ l ∷ A ^ [ r , lA ] → Γ ⊢ l ≡ k ∷ A ^ [ r , lA ]
genSym {r = !} = sym
genSym {r = %} (proof-irrelevance x x₁) = proof-irrelevance x₁ x
genSym {r = %} (conv x x₁) = conv (genSym x) x₁

genTrans : ∀ {k l m A r Γ lA } → Γ ⊢ k ≡ l ∷ A ^ [ r , lA ] → Γ ⊢ l ≡ m ∷ A ^ [ r , lA ] → Γ ⊢ k ≡ m ∷ A ^ [ r , lA ]
genTrans {r = !} = trans
genTrans {r = %} (conv X x) (conv Y x₁) = conv (genTrans X (conv Y (trans x₁ (sym x)))) x
genTrans {r = %} (conv X x) (proof-irrelevance x₁ x₂) = proof-irrelevance (conv (typeInversion X) x) x₂
genTrans {r = %} (proof-irrelevance x x₁) (conv Y x₂) = proof-irrelevance x (conv (typeInversion (genSym Y)) x₂)
genTrans {r = %} (proof-irrelevance x x₁) (proof-irrelevance x₂ x₃) = proof-irrelevance x x₃

genVar : ∀ {x A Γ r l } → Γ ⊢ var x ∷ A ^ [ r , l ] → Γ ⊢ var x ≡ var x ∷ A ^ [ r , l ]
genVar {r = !} = refl
genVar {r = %} d = proof-irrelevance d d

toLevelInj : ∀ {l₁ l₁′ : TypeLevel} {l<₁ : l₁′ <∞ l₁} {l₂ l₂′ : TypeLevel} {l<₂ : l₂′ <∞ l₂} →
               toLevel l₁′ PE.≡ toLevel l₂′ → l₁′ PE.≡ l₂′
toLevelInj {.(ι ¹)} {.(ι ⁰)} {emb<} {.(ι ¹)} {.(ι ⁰)} {emb<} e = PE.refl
toLevelInj {.∞} {.(ι ¹)} {∞<} {.(ι ¹)} {.(ι ⁰)} {emb<} ()
toLevelInj {.∞} {.(ι ¹)} {∞<} {.∞} {.(ι ¹)} {∞<} e = PE.refl

redSProp′ : ∀ {Γ A B l}
           (D : Γ ⊢ A ⇒* B ∷ SProp l ^ next l )
         → Γ ⊢ A ⇒* B ^ [ % , ι l ]
redSProp′ (id x) = id (univ x)
redSProp′ (x ⇨ D) = univ x ⇨ redSProp′ D

redSProp : ∀ {Γ A B l}
           (D : Γ ⊢ A :⇒*: B ∷ SProp l ^ next l )
         → Γ ⊢ A :⇒*: B ^ [ % , ι l ]
redSProp [[ ⊢t , ⊢u , d ]] = [[ (univ ⊢t) , (univ ⊢u) , redSProp′ d ]]

un-univ : ∀ {A r Γ l} → Γ ⊢ A ^ [ r , ι l ] → Γ ⊢ A ∷ Univ r l ^ [ ! , next l ]
un-univ (univ x) = x

un-univ≡ : ∀ {A B r Γ l} → Γ ⊢ A ≡ B ^ [ r , ι l ] → Γ ⊢ A ≡ B ∷ Univ r l ^ [ ! , next l ]
un-univ≡ (univ x) = x
un-univ≡ (refl x) = refl (un-univ x)
un-univ≡ (sym X) = sym (un-univ≡ X)
un-univ≡ (trans X Y) = trans (un-univ≡ X) (un-univ≡ Y)

univ-gen : ∀ {r Γ l} → (⊢Γ : ⊢ Γ) → Γ ⊢ Univ r l ^ [ ! , next l ]
univ-gen {l = ⁰} ⊢Γ = univ (univ 0<1 ⊢Γ )
univ-gen {l = ¹} ⊢Γ = Uⱼ ⊢Γ

un-univ⇒ : ∀ {l Γ A B r} → Γ ⊢ A ⇒ B ^ [ r , ι l ] → Γ ⊢ A ⇒ B ∷ Univ r l ^ next l
un-univ⇒ (univ x) = x

univ⇒* : ∀ {l Γ A B r} → Γ ⊢ A ⇒* B ∷ Univ r l ^ next l → Γ ⊢ A ⇒* B ^ [ r , ι l ]
univ⇒* (id x) = id (univ x)
univ⇒* (x ⇨ D) = univ x ⇨ univ⇒* D

un-univ⇒* : ∀ {l Γ A B r} → Γ ⊢ A ⇒* B ^ [ r , ι l ] → Γ ⊢ A ⇒* B ∷ Univ r l ^ next l
un-univ⇒* (id x) = id (un-univ x)
un-univ⇒* (x ⇨ D) = un-univ⇒ x ⇨ un-univ⇒* D

univ:⇒*: : ∀ {l Γ A B r} →  Γ ⊢ A :⇒*: B ∷ Univ r l ^ next l → Γ ⊢ A :⇒*: B ^ [ r , ι l ]
univ:⇒*: [[ ⊢A , ⊢B , D ]] = [[ (univ ⊢A) , (univ ⊢B) , (univ⇒* D) ]]

un-univ:⇒*: : ∀ {l Γ A B r} → Γ ⊢ A :⇒*: B ^ [ r , ι l ] → Γ ⊢ A :⇒*: B ∷ Univ r l ^ next l
un-univ:⇒*: [[ ⊢A , ⊢B , D ]] = [[ (un-univ ⊢A) , (un-univ ⊢B) , (un-univ⇒* D) ]]

IdRed*Term′ : ∀ {Γ A B t u l}
         (⊢t : Γ ⊢ t ∷ A ^ [ ! , ι l ])
         (⊢u : Γ ⊢ u ∷ A ^ [ ! , ι l ])
         (D : Γ ⊢ A ⇒* B ^ [ ! , ι l ])
       → Γ ⊢ Id A t u ⇒* Id B t u ∷ SProp l ^ next l
IdRed*Term′ ⊢t ⊢u (id (univ ⊢A)) = id (Idⱼ ⊢A ⊢t ⊢u)
IdRed*Term′ ⊢t ⊢u (univ d ⇨ D) = Id-subst d ⊢t ⊢u ⇨ IdRed*Term′ (conv ⊢t (subset (univ d))) (conv ⊢u (subset (univ d))) D

IdRed*Term : ∀ {Γ A B t u l}
          (⊢t : Γ ⊢ t ∷ A ^ [ ! , ι l ])
          (⊢u : Γ ⊢ u ∷ A ^ [ ! , ι l ])
          (D : Γ ⊢ A :⇒*: B ^ [ ! , ι l ])
        → Γ ⊢ Id A t u :⇒*: Id B t u ∷ SProp l ^ next l
IdRed*Term {Γ} {A} {B} ⊢t ⊢u [[ univ ⊢A , univ ⊢B , D ]] =
  [[ Idⱼ ⊢A ⊢t ⊢u , Idⱼ ⊢B (conv ⊢t (subset* D)) (conv ⊢u (subset* D)) ,
     IdRed*Term′ ⊢t ⊢u D ]]

IdRed* : ∀ {Γ A B t u l}
         (⊢t : Γ ⊢ t ∷ A ^ [ ! , ι l ])
         (⊢u : Γ ⊢ u ∷ A ^ [ ! , ι l ])
         (D : Γ ⊢ A ⇒* B ^ [ ! , ι l ])
       → Γ ⊢ Id A t u ⇒* Id B t u ^ [ % , ι l ]
IdRed* ⊢t ⊢u (id ⊢A) = id (univ (Idⱼ (un-univ ⊢A) ⊢t ⊢u))
IdRed* ⊢t ⊢u (d ⇨ D) = univ (Id-subst (un-univ⇒ d) ⊢t ⊢u) ⇨ IdRed* (conv ⊢t (subset d)) (conv ⊢u (subset d)) D

CastRed*Term′ : ∀ {Γ A B X e t}
         (⊢X : Γ ⊢ X ^ [ ! , ι ⁰ ])
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) A X ^ [ % , next ⁰ ])
         (⊢t : Γ ⊢ t ∷ A ^ [ ! , ι ⁰ ])
         (D : Γ ⊢ A ⇒* B ^ [ ! , ι ⁰ ])
       → Γ ⊢ cast ⁰ A X e t ⇒* cast ⁰ B X e t ∷ X ^ ι ⁰
CastRed*Term′ (univ ⊢X) ⊢e ⊢t  (id (univ ⊢A)) = id (castⱼ ⊢A ⊢X ⊢e ⊢t)
CastRed*Term′ (univ ⊢X) ⊢e ⊢t  (univ d ⇨ D) = cast-subst d ⊢X ⊢e ⊢t ⇨
              CastRed*Term′ (univ ⊢X) (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢t))) (subsetTerm d) (refl ⊢X)) )) (conv ⊢t (subset (univ d))) D

CastRed*Term : ∀ {Γ A B X t e}
         (⊢X : Γ ⊢ X ^ [ ! , ι ⁰ ])
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) A X ^ [ % , next ⁰ ])
         (⊢t : Γ ⊢ t ∷ A ^ [ ! , ι ⁰ ])
         (D : Γ ⊢ A :⇒*: B ∷ U ⁰ ^ next ⁰)
       → Γ ⊢ cast ⁰ A X e t :⇒*: cast ⁰ B X e t ∷ X ^ ι ⁰
CastRed*Term {Γ} {A} {B} (univ ⊢X) ⊢e ⊢t [[ ⊢A , ⊢B , D ]] =
  [[ castⱼ ⊢A ⊢X ⊢e ⊢t , castⱼ ⊢B ⊢X (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢t))) (subset*Term D) (refl ⊢X)) )) (conv ⊢t (univ (subset*Term D))) ,
     CastRed*Term′ (univ ⊢X) ⊢e ⊢t (univ* D) ]]

CastRed*Termℕ′ : ∀ {Γ A B e t}
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) ℕ A ^ [ % , next ⁰ ])
         (⊢t : Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ])
         (D : Γ ⊢ A ⇒* B ^ [ ! , ι ⁰ ])
       → Γ ⊢ cast ⁰ ℕ A e t ⇒* cast ⁰ ℕ B e t ∷ A ^ ι ⁰
CastRed*Termℕ′ ⊢e ⊢t  (id (univ ⊢A)) = id (castⱼ (ℕⱼ (wfTerm ⊢A)) ⊢A ⊢e ⊢t)
CastRed*Termℕ′ ⊢e ⊢t  (univ d ⇨ D) = cast-ℕ-subst d ⊢e ⊢t ⇨
                                     conv* (CastRed*Termℕ′ (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e))) (refl (ℕⱼ (wfTerm ⊢e))) (subsetTerm d))) ) ⊢t D)
                                           (sym (subset (univ d)))

CastRed*Termℕ : ∀ {Γ A B e t}
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) ℕ A ^ [ % , next ⁰ ])
         (⊢t : Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ])
         (D : Γ ⊢ A :⇒*: B ^ [ ! , ι ⁰ ])
       → Γ ⊢ cast ⁰ ℕ A e t :⇒*: cast ⁰ ℕ B e t ∷ A ^ ι ⁰
CastRed*Termℕ ⊢e ⊢t  [[ ⊢A , ⊢B , D ]] =
  [[ castⱼ (ℕⱼ (wfTerm ⊢e)) (un-univ ⊢A) ⊢e ⊢t ,
     conv (castⱼ (ℕⱼ (wfTerm ⊢e)) (un-univ ⊢B) (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e))) (refl (ℕⱼ (wfTerm ⊢e))) (subset*Term (un-univ⇒* D))))) ⊢t) (sym (subset* D)) ,
       CastRed*Termℕ′ ⊢e ⊢t D ]]

CastRed*Termℕℕ′ : ∀ {Γ e t u}
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ])
         (⊢t : Γ ⊢ t ⇒* u ∷ ℕ ^ ι ⁰ )
       → Γ ⊢ cast ⁰ ℕ ℕ e t ⇒* cast ⁰ ℕ ℕ e u ∷ ℕ ^ ι ⁰
CastRed*Termℕℕ′ ⊢e (id ⊢t) = id (castⱼ (ℕⱼ (wfTerm ⊢e)) (ℕⱼ (wfTerm ⊢e)) ⊢e ⊢t)
CastRed*Termℕℕ′ ⊢e (d ⇨ D) = cast-ℕ-cong ⊢e d ⇨ CastRed*Termℕℕ′ ⊢e D

CastRed*Termℕℕ : ∀ {Γ e t u}
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ])
         (⊢t : Γ ⊢ t :⇒*: u ∷ ℕ ^ ι ⁰ )
       → Γ ⊢ cast ⁰ ℕ ℕ e t :⇒*: cast ⁰ ℕ ℕ e u ∷ ℕ ^ ι ⁰
CastRed*Termℕℕ ⊢e [[ ⊢t , ⊢u , D ]] =
  [[ castⱼ (ℕⱼ (wfTerm ⊢e)) (ℕⱼ (wfTerm ⊢e)) ⊢e ⊢t ,
     castⱼ (ℕⱼ (wfTerm ⊢e)) (ℕⱼ (wfTerm ⊢e)) ⊢e ⊢u ,
       CastRed*Termℕℕ′ ⊢e D ]]

CastRed*Termℕsuc : ∀ {Γ e n}
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ])
         (⊢n : Γ ⊢ n ∷ ℕ ^ [ ! , ι ⁰ ])
       → Γ ⊢ cast ⁰ ℕ ℕ e (suc n) :⇒*: suc (cast ⁰ ℕ ℕ e n) ∷ ℕ ^ ι ⁰
CastRed*Termℕsuc ⊢e ⊢n =
  [[ castⱼ (ℕⱼ (wfTerm ⊢e)) (ℕⱼ (wfTerm ⊢e)) ⊢e (sucⱼ ⊢n) ,
     sucⱼ (castⱼ (ℕⱼ (wfTerm ⊢e)) (ℕⱼ (wfTerm ⊢e)) ⊢e ⊢n) ,
       cast-ℕ-S ⊢e ⊢n ⇨ id (sucⱼ (castⱼ (ℕⱼ (wfTerm ⊢e)) (ℕⱼ (wfTerm ⊢e)) ⊢e ⊢n)) ]]

CastRed*Termℕzero : ∀ {Γ e}
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) ℕ ℕ ^ [ % , next ⁰ ])
       → Γ ⊢ cast ⁰ ℕ ℕ e zero :⇒*: zero ∷ ℕ ^ ι ⁰
CastRed*Termℕzero ⊢e =
  [[ castⱼ (ℕⱼ (wfTerm ⊢e)) (ℕⱼ (wfTerm ⊢e)) ⊢e (zeroⱼ (wfTerm ⊢e)) ,
     zeroⱼ (wfTerm ⊢e) ,
       cast-ℕ-0 ⊢e ⇨ id (zeroⱼ (wfTerm ⊢e)) ]]

CastRed*TermΠ′ : ∀ {Γ F rF G A B e t}
         (⊢F : Γ ⊢ F ∷ (Univ rF ⁰) ^ [ ! , next ⁰ ])
         (⊢G : Γ ∙ F ^ [ rF , ι ⁰ ] ⊢ G ∷ U ⁰ ^ [ ! , next ⁰ ])
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) A ^ [ % , next ⁰ ])
         (⊢t : Γ ⊢ t ∷ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) ^ [ ! , ι ⁰ ])
         (D : Γ ⊢ A ⇒* B ^ [ ! , ι ⁰ ])
       → Γ ⊢ cast ⁰ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) A e t ⇒* cast ⁰ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) B e t ∷ A ^ ι ⁰
CastRed*TermΠ′ ⊢F ⊢G ⊢e ⊢t (id (univ ⊢A)) = id (castⱼ (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ ⊢F ▹ ⊢G) ⊢A ⊢e ⊢t)
CastRed*TermΠ′ ⊢F ⊢G ⊢e ⊢t (univ d ⇨ D) = cast-Π-subst ⊢F ⊢G d ⊢e ⊢t ⇨
                                     conv* (CastRed*TermΠ′ ⊢F ⊢G (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e))) (refl (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ ⊢F ▹ ⊢G)) (subsetTerm d))) ) ⊢t D)
                                           (sym (subset (univ d)))

CastRed*TermΠ : ∀ {Γ F rF G A B e t}
         (⊢F : Γ ⊢ F ∷ (Univ rF ⁰) ^ [ ! , next ⁰ ])
         (⊢G : Γ ∙ F ^ [ rF , ι ⁰ ] ⊢ G ∷ U ⁰ ^ [ ! , next ⁰ ])
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) A ^ [ % , next ⁰ ])
         (⊢t : Γ ⊢ t ∷ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) ^ [ ! , ι ⁰ ])
         (D : Γ ⊢ A :⇒*: B ^ [ ! , ι ⁰ ])
       → Γ ⊢ cast ⁰ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) A e t :⇒*: cast ⁰ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) B e t ∷ A ^ ι ⁰
CastRed*TermΠ ⊢F ⊢G ⊢e ⊢t  [[ ⊢A , ⊢B , D ]] =
  let [Π] = Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ ⊢F ▹ ⊢G
  in [[ castⱼ [Π] (un-univ ⊢A) ⊢e ⊢t ,
        conv (castⱼ [Π] (un-univ ⊢B) (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e))) (refl [Π]) (subset*Term (un-univ⇒* D))))) ⊢t) (sym (subset* D)) ,
          CastRed*TermΠ′ ⊢F ⊢G ⊢e ⊢t D ]]

IdURed*Term′ : ∀ {Γ t t′ u}
               (⊢t : Γ ⊢ t ∷ U ⁰ ^ [ ! , ι ¹ ])
               (⊢t′ : Γ ⊢ t′ ∷ U ⁰ ^ [ ! , ι ¹ ])
               (d : Γ ⊢ t ⇒* t′ ∷ U ⁰ ^ ι ¹)
               (⊢u : Γ ⊢ u ∷ U ⁰ ^ [ ! , ι ¹ ])
             → Γ ⊢ Id (U ⁰) t u ⇒* Id (U ⁰) t′ u ∷ SProp ¹ ^ ∞
IdURed*Term′ ⊢t ⊢t′ (id x) ⊢u = id (Idⱼ (univ 0<1 (wfTerm ⊢t)) ⊢t ⊢u)
IdURed*Term′ ⊢t ⊢t′ (x ⇨ d) ⊢u = _⇨_ (Id-U-subst x ⊢u) (IdURed*Term′ (redFirst*Term d) ⊢t′ d ⊢u)

IdURed*Term : ∀ {Γ t t′ u}
               (d : Γ ⊢ t :⇒*: t′ ∷ U ⁰ ^ ι ¹)
               (⊢u : Γ ⊢ u ∷ U ⁰ ^ [ ! , ι ¹ ])
             → Γ ⊢ Id (U ⁰) t u :⇒*: Id (U ⁰) t′ u ∷ SProp ¹ ^ ∞
IdURed*Term [[ ⊢t , ⊢t′ , d ]] ⊢u = [[ Idⱼ (univ 0<1 (wfTerm ⊢u)) ⊢t ⊢u , Idⱼ (univ 0<1 (wfTerm ⊢u)) ⊢t′ ⊢u  , IdURed*Term′ ⊢t ⊢t′ d ⊢u  ]]

IdUΠRed*Term′ : ∀ {Γ F rF G t t′}
               (⊢F : Γ ⊢ F ∷ Univ rF ⁰ ^ [ ! , ι ¹ ])
               (⊢G : Γ ∙ F ^ [ rF , ι ⁰ ] ⊢ G ∷ U ⁰ ^ [ ! , ι ¹ ])
               (⊢t : Γ ⊢ t ∷ U ⁰ ^ [ ! , ι ¹ ])
               (⊢t′ : Γ ⊢ t′ ∷ U ⁰ ^ [ ! , ι ¹ ])
               (d : Γ ⊢ t ⇒* t′ ∷ U ⁰ ^ ι ¹)
             → Γ ⊢ Id (U ⁰) (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) t ⇒* Id (U ⁰) (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) t′ ∷ SProp ¹ ^ ∞
IdUΠRed*Term′ ⊢F ⊢G ⊢t ⊢t′ (id x) = id (Idⱼ (univ 0<1 (wfTerm ⊢t)) (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ ⊢F ▹ ⊢G) ⊢t)
IdUΠRed*Term′ ⊢F ⊢G ⊢t ⊢t′ (x ⇨ d) = _⇨_ (Id-U-Π-subst ⊢F ⊢G x) (IdUΠRed*Term′ ⊢F ⊢G (redFirst*Term d) ⊢t′ d)

IdUΠRed*Term : ∀ {Γ F rF G t t′}
               (⊢F : Γ ⊢ F ∷ Univ rF ⁰ ^ [ ! , ι ¹ ])
               (⊢G : Γ ∙ F ^ [ rF , ι ⁰ ] ⊢ G ∷ U ⁰ ^ [ ! , ι ¹ ])
               (d : Γ ⊢ t :⇒*: t′ ∷ U ⁰ ^ ι ¹)
             → Γ ⊢ Id (U ⁰) (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) t :⇒*: Id (U ⁰) (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) t′ ∷ SProp ¹ ^ ∞
IdUΠRed*Term ⊢F ⊢G [[ ⊢t , ⊢t′ , d ]] = [[ Idⱼ (univ 0<1 (wfTerm ⊢t)) (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ ⊢F ▹ ⊢G) ⊢t ,
                                           Idⱼ (univ 0<1 (wfTerm ⊢t)) (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ ⊢F ▹ ⊢G) ⊢t′ ,
                                           IdUΠRed*Term′ ⊢F ⊢G ⊢t ⊢t′ d ]]

IdℕRed*Term′ : ∀ {Γ t t′ u}
               (⊢t : Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ])
               (⊢t′ : Γ ⊢ t′ ∷ ℕ ^ [ ! , ι ⁰ ])
               (d : Γ ⊢ t ⇒* t′ ∷ ℕ ^ ι ⁰)
               (⊢u : Γ ⊢ u ∷ ℕ ^ [ ! , ι ⁰ ])
             → Γ ⊢ Id ℕ t u ⇒* Id ℕ t′ u ∷ SProp ⁰ ^ next ⁰
IdℕRed*Term′ ⊢t ⊢t′ (id x) ⊢u = id (Idⱼ (ℕⱼ (wfTerm ⊢u)) ⊢t ⊢u)
IdℕRed*Term′ ⊢t ⊢t′ (x ⇨ d) ⊢u = _⇨_ (Id-ℕ-subst x ⊢u) (IdℕRed*Term′ (redFirst*Term d) ⊢t′ d ⊢u)

Idℕ0Red*Term′ : ∀ {Γ t t′}
                (⊢t : Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ])
                (⊢t′ : Γ ⊢ t′ ∷ ℕ ^ [ ! , ι ⁰ ])
                (d : Γ ⊢ t ⇒* t′ ∷ ℕ ^ ι ⁰)
              → Γ ⊢ Id ℕ zero t ⇒* Id ℕ zero t′ ∷ SProp ⁰ ^ next ⁰
Idℕ0Red*Term′ ⊢t ⊢t′ (id x) = id (Idⱼ (ℕⱼ (wfTerm ⊢t)) (zeroⱼ (wfTerm ⊢t)) ⊢t)
Idℕ0Red*Term′ ⊢t ⊢t′ (x ⇨ d) = Id-ℕ-0-subst x ⇨ Idℕ0Red*Term′ (redFirst*Term d) ⊢t′ d

IdℕSRed*Term′ : ∀ {Γ t u u′}
                (⊢t : Γ ⊢ t ∷ ℕ ^ [ ! , ι ⁰ ])
                (⊢u : Γ ⊢ u ∷ ℕ ^ [ ! , ι ⁰ ])
                (⊢u′ : Γ ⊢ u′ ∷ ℕ ^ [ ! , ι ⁰ ])
                (d : Γ ⊢ u ⇒* u′ ∷ ℕ ^ ι ⁰)
              → Γ ⊢ Id ℕ (suc t) u ⇒* Id ℕ (suc t) u′ ∷ SProp ⁰ ^ next ⁰
IdℕSRed*Term′ ⊢t ⊢u ⊢u′ (id x) = id (Idⱼ (ℕⱼ (wfTerm ⊢t)) (sucⱼ ⊢t) ⊢u)
IdℕSRed*Term′ ⊢t ⊢u ⊢u′ (x ⇨ d) = Id-ℕ-S-subst ⊢t x ⇨ IdℕSRed*Term′ ⊢t (redFirst*Term d) ⊢u′ d

IdUℕRed*Term′ : ∀ {Γ t t′}
               (⊢t : Γ ⊢ t ∷ U ⁰ ^ [ ! , ι ¹ ])
               (⊢t′ : Γ ⊢ t′ ∷ U ⁰ ^ [ ! , ι ¹ ])
               (d : Γ ⊢ t ⇒* t′ ∷ U ⁰ ^ ι ¹)
             → Γ ⊢ Id (U ⁰) ℕ t ⇒* Id (U ⁰) ℕ t′ ∷ SProp ¹ ^ ∞
IdUℕRed*Term′ ⊢t ⊢t′ (id x) = id (Idⱼ (univ 0<1 (wfTerm ⊢t)) (ℕⱼ (wfTerm ⊢t) ) ⊢t)
IdUℕRed*Term′ ⊢t ⊢t′ (x ⇨ d) =  _⇨_ (Id-U-ℕ-subst x) (IdUℕRed*Term′ (redFirst*Term d) ⊢t′ d)

IdUℕRed*Term : ∀ {Γ t t′}
               (d : Γ ⊢ t :⇒*: t′ ∷ U ⁰ ^ ι ¹)
             → Γ ⊢ Id (U ⁰) ℕ t :⇒*: Id (U ⁰) ℕ t′ ∷ SProp ¹ ^ ∞
IdUℕRed*Term [[ ⊢t , ⊢t′ , d ]] = [[ Idⱼ (univ 0<1 (wfTerm ⊢t)) (ℕⱼ (wfTerm ⊢t) ) ⊢t ,
                                     Idⱼ (univ 0<1 (wfTerm ⊢t)) (ℕⱼ (wfTerm ⊢t) ) ⊢t′ ,
                                     IdUℕRed*Term′ ⊢t ⊢t′ d ]]

appRed* : ∀ {Γ a t u A B rA lA lB l}
          (⊢a : Γ ⊢ a ∷ A ^ [ rA , ι lA ])
          (D : Γ ⊢ t ⇒* u ∷ (Π A ^ rA ° lA ▹ B ° lB ° l) ^ ι l)
        → Γ ⊢ t ∘ a ^ l ⇒* u ∘ a ^ l ∷ B [ a ] ^ ι lB
appRed* ⊢a (id x) = id (x ∘ⱼ ⊢a)
appRed* ⊢a (x ⇨ D) = app-subst x ⊢a ⇨ appRed* ⊢a D

castΠRed* : ∀ {Γ F rF G A B e t}
         (⊢F : Γ ⊢ F ^ [ rF , ι ⁰ ])
         (⊢G : Γ ∙ F ^ [ rF , ι ⁰ ] ⊢ G ^ [ ! , ι ⁰ ])
         (⊢e : Γ ⊢ e ∷ Id (U ⁰) (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) A ^ [ % , next ⁰ ])
         (⊢t : Γ ⊢ t ∷ Π F ^ rF ° ⁰ ▹ G ° ⁰  ° ⁰ ^ [ ! , ι ⁰ ])
         (D : Γ ⊢ A ⇒* B ^ [ ! , ι ⁰ ])
       → Γ ⊢ cast ⁰ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) A e t ⇒* cast ⁰ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) B e t ∷ A ^ ι ⁰
castΠRed* ⊢F ⊢G ⊢e ⊢t (id (univ ⊢A)) = id (castⱼ (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ un-univ ⊢F ▹ un-univ ⊢G) ⊢A ⊢e ⊢t)
castΠRed* ⊢F ⊢G ⊢e ⊢t ((univ d) ⇨ D) = cast-Π-subst (un-univ ⊢F) (un-univ ⊢G) d ⊢e ⊢t ⇨ conv* (castΠRed* ⊢F ⊢G (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wf ⊢F))) (refl (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ un-univ ⊢F ▹ un-univ ⊢G)) (subsetTerm d)))) ⊢t D) (sym (subset (univ d)))

notredUterm* : ∀ {Γ r l l' A B} → Γ ⊢ Univ r l ⇒ A ∷ B ^ l' → ⊥
notredUterm* (conv D x) = notredUterm* D

notredU* : ∀ {Γ r l l' A} → Γ ⊢ Univ r l ⇒ A ^ [ ! , l' ] → ⊥
notredU* (univ x) = notredUterm* x

redU*gen : ∀ {Γ r l r' l' l''} → Γ ⊢ Univ r l ⇒* Univ r' l' ^ [ ! , l'' ] → Univ r l PE.≡ Univ r' l'
redU*gen (id x) = PE.refl
redU*gen (univ (conv x x₁) ⇨ D) = ⊥-elim (notredUterm* x)

-- Typing of Idsym

Idsymⱼ : ∀ {Γ A l x y e}
       → Γ ⊢ A ∷ U l ^ [ ! , next l ]
       → Γ ⊢ x ∷ A ^ [ ! , ι l ]
       → Γ ⊢ y ∷ A ^ [ ! , ι l ]
       → Γ ⊢ e ∷ Id A x y ^ [ % , ι l ]
       → Γ ⊢ Idsym A x y e ∷ Id A y x ^ [ % , ι l ]
Idsymⱼ {Γ} {A} {l} {x} {y} {e} ⊢A ⊢x ⊢y ⊢e =
  let
    ⊢Γ = wfTerm ⊢A
    ⊢A = univ ⊢A
    ⊢P : Γ ∙ A ^ [ ! , ι l ] ⊢ Id (wk1 A) (var 0) (wk1 x) ^ [ % , ι l ]
    ⊢P = univ (Idⱼ (Twk.wkTerm (Twk.step Twk.id) (⊢Γ ∙ ⊢A) (un-univ ⊢A))
      (var (⊢Γ ∙ ⊢A) here)
      (Twk.wkTerm (Twk.step Twk.id) (⊢Γ ∙ ⊢A) ⊢x))
    ⊢refl : Γ ⊢ Idrefl A x ∷ Id (wk1 A) (var 0) (wk1 x) [ x ] ^ [ % , ι l ]
    ⊢refl = PE.subst₂ (λ X Y → Γ ⊢ Idrefl A x ∷ Id X x Y ^ [ % , ι l ])
      (PE.sym (wk1-singleSubst A x)) (PE.sym (wk1-singleSubst x x))
      (Idreflⱼ ⊢x)
  in PE.subst₂ (λ X Y → Γ ⊢ Idsym A x y e ∷ Id X y Y ^ [ % , ι l ])
    (wk1-singleSubst A y) (wk1-singleSubst x y)
    (transpⱼ ⊢A ⊢P ⊢x ⊢refl ⊢y ⊢e)

▹▹ⱼ_▹_▹_▹_ : ∀ {Γ F rF lF G lG r l}
             → lF ≤ l
             → lG ≤ l
             → Γ ⊢ F ∷ (Univ rF lF) ^ [ ! , next lF ]
             → Γ ⊢ G ∷ (Univ r lG) ^ [ ! , next lG ]
             → Γ ⊢ F ^ rF ° lF ▹▹ G ° lG ° l ∷ (Univ r l) ^ [ ! , next l ]
▹▹ⱼ lF≤ ▹ lG≤ ▹ F ▹ G = Πⱼ lF≤ ▹ lG≤ ▹ F ▹ un-univ (Twk.wk (Twk.step Twk.id) ((wf (univ F)) ∙ (univ F)) (univ G))

××ⱼ_▹_ : ∀ {Γ F G l}
        → Γ ⊢ F ∷ SProp l ^ [ ! , next l ]
        → Γ ⊢ G ∷ SProp l ^ [ ! , next l ]
        → Γ ⊢ F ×× G ∷ SProp l ^ [ ! , next l ]
××ⱼ F ▹ G = ∃ⱼ F ▹ un-univ (Twk.wk (Twk.step Twk.id) ((wf (univ F)) ∙ (univ F)) (univ G))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --cubical --safe #-}

module Data.Nat.Properties where

open import Data.Nat.Base
open import Agda.Builtin.Nat using () renaming (_<_ to _<ᴮ_; _==_ to _≡ᴮ_) public
open import Prelude
open import Cubical.Data.Nat using (caseNat; injSuc) public
open import Data.Nat.DivMod

mutual
  _-1⊔_ : ℕ → ℕ → ℕ
  zero  -1⊔ n = n
  suc m -1⊔ n = n ⊔ m

  _⊔_ : ℕ → ℕ → ℕ
  zero  ⊔ m = m
  suc n ⊔ m = suc (m -1⊔ n)

znots : ∀ {n} → zero ≢ suc n
znots z≡s = subst (caseNat ⊤ ⊥) z≡s tt

snotz : ∀ {n} → suc n ≢ zero
snotz s≡z = subst (caseNat ⊥ ⊤) s≡z tt

pred : ℕ → ℕ
pred (suc n) = n
pred zero = zero

sound-== : ∀ n m →  T (n ≡ᴮ m) → n ≡ m
sound-== zero zero p i = zero
sound-== (suc n) (suc m) p i = suc (sound-== n m p i)

complete-== : ∀ n → T (n ≡ᴮ n)
complete-== zero = tt
complete-== (suc n) = complete-== n

open import Relation.Nullary.Discrete.FromBoolean

discreteℕ : Discrete ℕ
discreteℕ = from-bool-eq _≡ᴮ_ sound-== complete-==

isSetℕ : isSet ℕ
isSetℕ = Discrete→isSet discreteℕ

+-suc : ∀ x y → x + suc y ≡ suc (x + y)
+-suc zero y = refl
+-suc (suc x) y = cong suc (+-suc x y)

+-idʳ : ∀ x → x + 0 ≡ x
+-idʳ zero     = refl
+-idʳ (suc x)  = cong suc (+-idʳ x)

+-comm : ∀ x y → x + y ≡ y + x
+-comm x zero = +-idʳ x
+-comm x (suc y) = +-suc x y ; cong suc (+-comm x y)

infix 4 _<_
_<_ : ℕ → ℕ → Type
n < m = T (n <ᴮ m)

infix 4 _≤ᴮ_
_≤ᴮ_ : ℕ → ℕ → Bool
n ≤ᴮ m = not (m <ᴮ n)

infix 4 _≤_
_≤_ : ℕ → ℕ → Type
n ≤ m = T (n ≤ᴮ m)

infix 4 _≥ᴮ_
_≥ᴮ_ : ℕ → ℕ → Bool
_≥ᴮ_ = flip _≤ᴮ_

+-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
+-assoc zero     y z i = y + z
+-assoc (suc x)  y z i = suc (+-assoc x y z i)

+-*-distrib : ∀ x y z → (x + y) * z ≡ x * z + y * z
+-*-distrib zero y z = refl
+-*-distrib (suc x) y z = cong (z +_) (+-*-distrib x y z) ; sym (+-assoc z (x * z) (y * z))

*-zeroʳ : ∀ x → x * zero ≡ zero
*-zeroʳ zero = refl
*-zeroʳ (suc x) = *-zeroʳ x

*-suc : ∀ x y → x + x * y ≡ x * suc y
*-suc zero    y = refl
*-suc (suc x) y = cong suc (sym (+-assoc x y (x * y)) ; cong (_+ x * y) (+-comm x y) ; +-assoc y x (x * y) ; cong (y +_) (*-suc x y))

*-comm : ∀ x y → x * y ≡ y * x
*-comm zero    y = sym (*-zeroʳ y)
*-comm (suc x) y = cong (y +_) (*-comm x y) ; *-suc y x

*-assoc : ∀ x y z → (x * y) * z ≡ x * (y * z)
*-assoc zero    y z = refl
*-assoc (suc x) y z = +-*-distrib y (x * y) z ; cong (y * z +_) (*-assoc x y z)

open import Data.Nat.DivMod
open import Agda.Builtin.Nat using (div-helper)

div-helper′ : (m n j : ℕ) → ℕ
div-helper′ m  zero    j      = zero
div-helper′ m (suc n)  zero   = suc (div-helper′ m n m)
div-helper′ m (suc n) (suc j) = div-helper′ m n j

div-helper-lemma : ∀ k m n j → div-helper k m n j ≡ k + div-helper′ m n j
div-helper-lemma k m zero j = sym (+-idʳ k)
div-helper-lemma k m (suc n) zero = div-helper-lemma (suc k) m n m ; sym (+-suc k (div-helper′ m n m))
div-helper-lemma k m (suc n) (suc j) = div-helper-lemma k m n j

Even : ℕ → Type
Even n = T (even n)

odd : ℕ → Bool
odd n = not (rem n 2 ≡ᴮ 0)

Odd : ℕ → Type
Odd n = T (odd n)

s≤s : ∀ n m → n ≤ m → suc n ≤ suc m
s≤s zero m p = tt
s≤s (suc n) m p = p

n≤s : ∀ n m → n ≤ m → n ≤ suc m
n≤s zero m p = tt
n≤s (suc zero) m p = tt
n≤s (suc (suc n)) zero p = p
n≤s (suc (suc n₁)) (suc n) p = n≤s (suc n₁) n p

div-≤ : ∀ n m → n ÷ suc m ≤ n
div-≤ n m = subst (_≤ n) (sym (div-helper-lemma 0 m n m)) (go m n m)
  where
  go : ∀ m n j → div-helper′ m n j ≤ n
  go m zero j = tt
  go m (suc n) zero = s≤s (div-helper′ m n m) n (go m n m)
  go m (suc n) (suc j) = n≤s (div-helper′ m n j) n (go m n j)

≤-trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z
≤-trans zero y z p q = tt
≤-trans (suc n) zero zero p q = p
≤-trans (suc zero) zero (suc n) p q = tt
≤-trans (suc (suc n₁)) zero (suc n) p q = ≤-trans (suc n₁) zero n p tt
≤-trans (suc n) (suc zero) zero p q = q
≤-trans (suc zero) (suc zero) (suc n) p q = tt
≤-trans (suc (suc n₁)) (suc zero) (suc n) p q = ≤-trans (suc n₁) zero n p tt
≤-trans (suc n₁) (suc (suc n)) zero p q = q
≤-trans (suc zero) (suc (suc n₁)) (suc n) p q = tt
≤-trans (suc (suc n₁)) (suc (suc n₂)) (suc n) p q = ≤-trans (suc n₁) (suc n₂) n p q

p≤n : ∀ n m → suc n ≤ m → n ≤ m
p≤n zero m p = tt
p≤n (suc n) zero p = p
p≤n (suc zero) (suc n) p = tt
p≤n (suc (suc n₁)) (suc n) p = p≤n (suc n₁) n p

p≤p : ∀ n m → suc n ≤ suc m → n ≤ m
p≤p zero m p = tt
p≤p (suc n) m p = p

≤-refl : ∀ n → n ≤ n
≤-refl zero = tt
≤-refl (suc zero) = tt
≤-refl (suc (suc n)) = ≤-refl (suc n)

linearise : ∀ n m → n ≡ m → n ≡ m
linearise n m n≡m with discreteℕ n m
... | yes p = p
... | no ¬p = ⊥-elim (¬p n≡m)

ext: agda

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- Paths and extensionality
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

module Equality.Path where

import Bijection
open import Equality hiding (module Derived-definitions-and-properties)
open import Equality.Instances-related
import Equivalence
import Equivalence.Contractible-preimages
import Equivalence.Half-adjoint
import Function-universe
import H-level
import H-level.Closure
open import Logical-equivalence using (_⇔_)
import Preimage
open import Prelude
import Univalence-axiom

------------------------------------------------------------------------
-- The interval

open import Agda.Primitive.Cubical public
  using (I; Partial; PartialP)
  renaming (i0 to 0̲; i1 to 1̲;
            IsOne to Is-one; itIsOne to is-one;
            primINeg to -_; primIMin to min; primIMax to max;
            primComp to comp; primHComp to hcomp;
            primTransp to transport)

open import Agda.Builtin.Cubical.Sub public
  renaming (Sub to _[_↦_]; inc to inˢ; primSubOut to outˢ)

------------------------------------------------------------------------
-- Some local generalisable variables

private
  variable
    a b c p q ℓ : Level
    A           : Type a
    B           : A → Type b
    P           : I → Type p
    u v w x y z : A
    f g h       : (x : A) → B x
    i j         : I
    n           : ℕ

------------------------------------------------------------------------
-- Equality

-- Homogeneous and heterogeneous equality.

open import Agda.Builtin.Cubical.Path public
  using (_≡_)
  renaming (PathP to infix 4 [_]_≡_)

------------------------------------------------------------------------
-- Filling

-- The code in this section is based on code in the cubical library
-- written by Anders Mörtberg.

-- Filling for homogenous composition.

hfill :
  {φ : I} (u : I → Partial φ A) (u₀ : A [ φ ↦ u 0̲ ]) →
  outˢ u₀ ≡ hcomp u (outˢ u₀)
hfill {φ = φ} u u₀ = λ i →
  hcomp (λ j → λ { (φ = 1̲) → u (min i j) is-one
                 ; (i = 0̲) → outˢ u₀
                 })
        (outˢ u₀)

-- Filling for heterogeneous composition.
--
-- Note that if p had been a constant level, then the final line of
-- the type signature could have been replaced by
-- [ P ] outˢ u₀ ≡ comp P u u₀.

fill :
  {p : I → Level}
  (P : ∀ i → Type (p i)) {φ : I}
  (u : ∀ i → Partial φ (P i))
  (u₀ : P 0̲ [ φ ↦ u 0̲ ]) →
  ∀ i → P i
fill P {φ} u u₀ i =
  comp (λ j → P (min i j))
       (λ j → λ { (φ = 1̲) → u (min i j) is-one
                ; (i = 0̲) → outˢ u₀
                })
       (outˢ u₀)

-- Filling for transport.

transport-fill :
  (A : Type ℓ)
  (φ : I)
  (P : (i : I) → Type ℓ [ φ ↦ (λ _ → A) ])
  (u₀ : outˢ (P 0̲)) →
  [ (λ i → outˢ (P i)) ]
    u₀ ≡ transport (λ i → outˢ (P i)) φ u₀
transport-fill _ φ P u₀ i =
  transport (λ j → outˢ (P (min i j))) (max (- i) φ) u₀

------------------------------------------------------------------------
-- Path equality satisfies the axioms of Equality-with-J

-- Reflexivity.

refl : {@0 A : Type a} {x : A} → x ≡ x
refl {x = x} = λ _ → x

-- A family of instantiations of Reflexive-relation.

reflexive-relation : ∀ ℓ → Reflexive-relation ℓ
Reflexive-relation._≡_  (reflexive-relation _) = _≡_
Reflexive-relation.refl (reflexive-relation _) = λ _ → refl

-- Symmetry.

hsym : [ P ] x ≡ y → [ (λ i → P (- i)) ] y ≡ x
hsym x≡y = λ i → x≡y (- i)

-- Transitivity.
--
-- The proof htransʳ-reflʳ is based on code in Agda's reference manual
-- written by Anders Mörtberg.
--
-- The proof htrans is suggested in the HoTT book (first version,
-- Exercise 6.1).

htransʳ : [ P ] x ≡ y → y ≡ z → [ P ] x ≡ z
htransʳ {x = x} x≡y y≡z = λ i →
  hcomp (λ { _ (i = 0̲) → x
           ; j (i = 1̲) → y≡z j
           })
        (x≡y i)

htransˡ : x ≡ y → [ P ] y ≡ z → [ P ] x ≡ z
htransˡ x≡y y≡z = hsym (htransʳ (hsym y≡z) (hsym x≡y))

htransʳ-reflʳ : (x≡y : [ P ] x ≡ y) → htransʳ x≡y refl ≡ x≡y
htransʳ-reflʳ {x = x} {y = y} x≡y = λ i j →
  hfill (λ { _ (j = 0̲) → x
           ; _ (j = 1̲) → y
           })
        (inˢ (x≡y j))
        (- i)

htransˡ-reflˡ : (x≡y : [ P ] x ≡ y) → htransˡ refl x≡y ≡ x≡y
htransˡ-reflˡ = htransʳ-reflʳ

htrans :
  {x≡y : x ≡ y} {y≡z : y ≡ z}
  (P : A → Type p) {p : P x} {q : P y} {r : P z} →
  [ (λ i → P (x≡y i)) ] p ≡ q →
  [ (λ i → P (y≡z i)) ] q ≡ r →
  [ (λ i → P (htransˡ x≡y y≡z i)) ] p ≡ r
htrans {z = z} {x≡y = x≡y} {y≡z = y≡z} P {r = r} p≡q q≡r = λ i →
  comp (λ j → P (eq j i))
       (λ { j (i = 0̲) → p≡q (- j)
          ; j (i = 1̲) → r
          })
       (q≡r i)
  where
  eq : [ (λ i → x≡y (- i) ≡ z) ] y≡z ≡ htransˡ x≡y y≡z
  eq = λ i j →
    hfill (λ { i (j = 0̲) → x≡y (- i)
             ; _ (j = 1̲) → z
             })
          (inˢ (y≡z j))
          i

-- Some equational reasoning combinators.

infix  -1 finally finally-h
infixr -2 step-≡ step-≡h step-≡hh _≡⟨⟩_

step-≡ : ∀ x → [ P ] y ≡ z → x ≡ y → [ P ] x ≡ z
step-≡ _ = flip htransˡ

syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

step-≡h : ∀ x → y ≡ z → [ P ] x ≡ y → [ P ] x ≡ z
step-≡h _ = flip htransʳ

syntax step-≡h x y≡z x≡y = x ≡⟨ x≡y ⟩h y≡z

step-≡hh :
  {x≡y : x ≡ y} {y≡z : y ≡ z}
  (P : A → Type p) (p : P x) {q : P y} {r : P z} →
  [ (λ i → P (y≡z i)) ] q ≡ r →
  [ (λ i → P (x≡y i)) ] p ≡ q →
  [ (λ i → P (htransˡ x≡y y≡z i)) ] p ≡ r
step-≡hh P _ = flip (htrans P)

syntax step-≡hh P p q≡r p≡q = p ≡⟨ p≡q ⟩[ P ] q≡r

_≡⟨⟩_ : ∀ x → [ P ] x ≡ y → [ P ] x ≡ y
_ ≡⟨⟩ x≡y = x≡y

finally : (x y : A) → x ≡ y → x ≡ y
finally _ _ x≡y = x≡y

syntax finally x y x≡y = x ≡⟨ x≡y ⟩∎ y ∎

finally-h : ∀ x y → [ P ] x ≡ y → [ P ] x ≡ y
finally-h _ _ x≡y = x≡y

syntax finally-h x y x≡y = x ≡⟨ x≡y ⟩∎h y ∎

-- The J rule.

elim :
  (P : {x y : A} → x ≡ y → Type p) →
  (∀ x → P (refl {x = x})) →
  (x≡y : x ≡ y) → P x≡y
elim {x = x} P p x≡y =
  transport (λ i → P (λ j → x≡y (min i j))) 0̲ (p x)

-- Substitutivity.

hsubst :
  ∀ (Q : ∀ {i} → P i → Type q) →
  [ P ] x ≡ y → Q x → Q y
hsubst Q x≡y p = transport (λ i → Q (x≡y i)) 0̲ p

subst : (P : A → Type p) → x ≡ y → P x → P y
subst P = hsubst P

-- Congruence.
--
-- The heterogeneous variant is based on code in the cubical library
-- written by Anders Mörtberg.

hcong :
  (f : (x : A) → B x) (x≡y : x ≡ y) →
  [ (λ i → B (x≡y i)) ] f x ≡ f y
hcong f x≡y = λ i → f (x≡y i)

cong : {B : Type b} (f : A → B) → x ≡ y → f x ≡ f y
cong f = hcong f

dcong :
  (f : (x : A) → B x) (x≡y : x ≡ y) →
  subst B x≡y (f x) ≡ f y
dcong {B = B} f x≡y = λ i →
  transport (λ j → B (x≡y (max i j))) i (f (x≡y i))

-- Transporting along reflexivity amounts to doing nothing.
--
-- This definition is based on code in Agda's reference manual written
-- by Anders Mörtberg.

transport-refl : ∀ i → transport (λ i → refl {x = A} i) i ≡ id
transport-refl {A = A} i = λ j → transport (λ _ → A) (max i j)

-- A family of instantiations of Equivalence-relation⁺.
--
-- Note that htransˡ is used to implement trans. The reason htransˡ is
-- used, rather than htransʳ, is that htransˡ is also used to
-- implement the commonly used equational reasoning combinator step-≡,
-- and I'd like this combinator to match trans.

equivalence-relation⁺ : ∀ ℓ → Equivalence-relation⁺ ℓ
equivalence-relation⁺ _ = λ where
  .Equivalence-relation⁺.reflexive-relation → reflexive-relation _
  .Equivalence-relation⁺.sym                → hsym
  .Equivalence-relation⁺.sym-refl           → refl
  .Equivalence-relation⁺.trans              → htransˡ
  .Equivalence-relation⁺.trans-refl-refl    → htransˡ-reflˡ _

-- A family of instantiations of Equality-with-J₀.

equality-with-J₀ : Equality-with-J₀ a p reflexive-relation
Equality-with-J₀.elim      equality-with-J₀ = elim
Equality-with-J₀.elim-refl equality-with-J₀ = λ _ r →
  cong (_$ r _) $ transport-refl 0̲

private
 module Temporarily-local where

  -- A family of instantiations of Equality-with-J.

  equality-with-J : Equality-with-J a p equivalence-relation⁺
  equality-with-J = λ where
    .Equality-with-J.equality-with-J₀ → equality-with-J₀
    .Equality-with-J.cong             → cong
    .Equality-with-J.cong-refl        → λ _ → refl
    .Equality-with-J.subst            → subst
    .Equality-with-J.subst-refl       → λ _ p →
                                          cong (_$ p) $ transport-refl 0̲
    .Equality-with-J.dcong            → dcong
    .Equality-with-J.dcong-refl       → λ _ → refl

-- Various derived definitions and properties.

open Equality.Derived-definitions-and-properties
       Temporarily-local.equality-with-J public
  hiding (_≡_; refl; elim; subst; cong; dcong;
          step-≡; _≡⟨⟩_; finally;
          reflexive-relation; equality-with-J₀)

------------------------------------------------------------------------
-- An extended variant of Equality-with-J

-- The following variant of Equality-with-J includes functions mapping
-- equalities to and from paths. The purpose of this definition is to
-- make it possible to instantiate these functions with identity
-- functions when paths are used as equalities (see
-- equality-with-paths below).

record Equality-with-paths
         a b (e⁺ : ∀ ℓ → Equivalence-relation⁺ ℓ) :
         Type (lsuc (a ⊔ b)) where

  field
    equality-with-J : Equality-with-J a b e⁺

  private
    module R =
      Reflexive-relation
        (Equivalence-relation⁺.reflexive-relation (e⁺ a))

  field

    -- A bijection between equality at level a and paths.

    to-path           : x R.≡ y → x ≡ y
    from-path         : x ≡ y → x R.≡ y
    to-path∘from-path : (x≡y : x ≡ y) → to-path (from-path x≡y) R.≡ x≡y
    from-path∘to-path :
      (x≡y : x R.≡ y) → from-path (to-path x≡y) R.≡ x≡y

    -- The bijection maps reflexivity to reflexivity.

    to-path-refl   : to-path (R.refl x) R.≡ refl
    from-path-refl : from-path refl R.≡ R.refl x

-- A family of instantiations of Equality-with-paths.

equality-with-paths :
  Equality-with-paths a p equivalence-relation⁺
equality-with-paths = λ where
    .E.equality-with-J   → Temporarily-local.equality-with-J
    .E.to-path           → id
    .E.from-path         → id
    .E.to-path∘from-path → λ _ → refl
    .E.from-path∘to-path → λ _ → refl
    .E.to-path-refl      → refl
    .E.from-path-refl    → refl
  where
  module E = Equality-with-paths

-- Equality-with-paths (for arbitrary universe levels) can be derived
-- from Equality-with-J (for arbitrary universe levels).

Equality-with-J⇒Equality-with-paths :
  ∀ {e⁺} →
  (∀ {a p} → Equality-with-J a p e⁺) →
  (∀ {a p} → Equality-with-paths a p e⁺)
Equality-with-J⇒Equality-with-paths eq = λ where
    .E.equality-with-J   → eq
    .E.to-path           → B._↔_.to (proj₁ ≡↔≡′)
    .E.from-path         → B._↔_.from (proj₁ ≡↔≡′)
    .E.to-path∘from-path → B._↔_.right-inverse-of (proj₁ ≡↔≡′)
    .E.from-path∘to-path → B._↔_.left-inverse-of (proj₁ ≡↔≡′)
    .E.to-path-refl      → B._↔_.from (proj₁ ≡↔≡′) (proj₁ (proj₂ ≡↔≡′))
    .E.from-path-refl    → proj₂ (proj₂ ≡↔≡′)
  where
  module E = Equality-with-paths
  module B = Bijection eq

  ≡↔≡′ =
    all-equality-types-isomorphic eq Temporarily-local.equality-with-J

-- Equality-with-paths (for arbitrary universe levels) can be derived
-- from Equality-with-J₀ (for arbitrary universe levels).

Equality-with-J₀⇒Equality-with-paths :
  ∀ {reflexive} →
  (eq : ∀ {a p} → Equality-with-J₀ a p reflexive) →
  ∀ {a p} → Equality-with-paths a p (λ _ → J₀⇒Equivalence-relation⁺ eq)
Equality-with-J₀⇒Equality-with-paths eq =
  Equality-with-J⇒Equality-with-paths (J₀⇒J eq)

module Derived-definitions-and-properties
  {e⁺}
  (equality-with-paths : ∀ {a p} → Equality-with-paths a p e⁺)
  where

  private
    module EP {a} {p} =
      Equality-with-paths (equality-with-paths {a = a} {p = p})

  open EP public using (equality-with-J)

  private
    module E =
      Equality.Derived-definitions-and-properties
        equality-with-J

  open Bijection equality-with-J

  ≡↔≡ : {A : Type a} {x y : A} → x E.≡ y ↔ x ≡ y
  ≡↔≡ {a = a} = record
    { surjection = record
      { logical-equivalence = record
        { to   = EP.to-path {p = a}
        ; from = EP.from-path
        }
      ; right-inverse-of = EP.to-path∘from-path
      }
    ; left-inverse-of = EP.from-path∘to-path
    }

  -- The isomorphism maps reflexivity to reflexivity.

  to-≡↔≡-refl : _↔_.to ≡↔≡ (E.refl x) E.≡ refl
  to-≡↔≡-refl = EP.to-path-refl

  from-≡↔≡-refl : _↔_.from ≡↔≡ refl E.≡ E.refl x
  from-≡↔≡-refl = EP.from-path-refl

  open E public

open Temporarily-local public

------------------------------------------------------------------------
-- Extensionality

open Equivalence equality-with-J using (Is-equivalence)
open H-level.Closure equality-with-J using (ext⁻¹)

-- Extensionality.

ext : Extensionality a b
apply-ext ext f≡g = λ i x → f≡g x i

⟨ext⟩ : Extensionality′ A B
⟨ext⟩ = apply-ext ext

-- The function ⟨ext⟩ is an equivalence.

ext-is-equivalence : Is-equivalence {A = ∀ x → f x ≡ g x} ⟨ext⟩
ext-is-equivalence =
    ext⁻¹
  , (λ _ → refl)
  , (λ _ → refl)
  , (λ _ → refl)

private

  -- Equality rearrangement lemmas for ⟨ext⟩. All of these lemmas hold
  -- definitionally.

  ext-refl : ⟨ext⟩ (λ x → refl {x = f x}) ≡ refl
  ext-refl = refl

  ext-const :
    (x≡y : x ≡ y) →
    ⟨ext⟩ (const {B = A} x≡y) ≡ cong const x≡y
  ext-const _ = refl

  cong-ext :
    (f≡g : ∀ x → f x ≡ g x) →
    cong (_$ x) (⟨ext⟩ f≡g) ≡ f≡g x
  cong-ext _ = refl

  subst-ext :
    ∀ {p} (f≡g : ∀ x → f x ≡ g x) →
    subst (λ f → B (f x)) (⟨ext⟩ f≡g) p ≡ subst B (f≡g x) p
  subst-ext _ = refl

  elim-ext :
    {f g : (x : A) → B x}
    (P : B x → B x → Type p)
    (p : (y : B x) → P y y)
    (f≡g : ∀ x → f x ≡ g x) →
    elim (λ {f g} _ → P (f x) (g x)) (p ∘ (_$ x)) (⟨ext⟩ f≡g) ≡
    elim (λ {x y} _ → P x y) p (f≡g x)
  elim-ext _ _ _ = refl

  -- I based the statements of the following three lemmas on code in
  -- the Lean Homotopy Type Theory Library with Jakob von Raumer and
  -- Floris van Doorn listed as authors. The file was claimed to have
  -- been ported from the Coq HoTT library. (The third lemma has later
  -- been generalised.)

  ext-sym :
    (f≡g : ∀ x → f x ≡ g x) →
    ⟨ext⟩ (sym ∘ f≡g) ≡ sym (⟨ext⟩ f≡g)
  ext-sym _ = refl

  ext-trans :
    (f≡g : ∀ x → f x ≡ g x) (g≡h : ∀ x → g x ≡ h x) →
    ⟨ext⟩ (λ x → trans (f≡g x) (g≡h x)) ≡
    trans (⟨ext⟩ f≡g) (⟨ext⟩ g≡h)
  ext-trans _ _ = refl

  cong-post-∘-ext :
    {B : A → Type b} {C : A → Type c} {f g : (x : A) → B x}
    {h : ∀ {x} → B x → C x}
    (f≡g : ∀ x → f x ≡ g x) →
    cong (h ∘_) (⟨ext⟩ f≡g) ≡ ⟨ext⟩ (cong h ∘ f≡g)
  cong-post-∘-ext _ = refl

  cong-pre-∘-ext :
    {B : Type b} {C : B → Type c} {f g : (x : B) → C x} {h : A → B}
    (f≡g : ∀ x → f x ≡ g x) →
    cong (_∘ h) (⟨ext⟩ f≡g) ≡ ⟨ext⟩ (f≡g ∘ h)
  cong-pre-∘-ext _ = refl

------------------------------------------------------------------------
-- Some properties

open Bijection equality-with-J using (_↔_)
open Function-universe equality-with-J hiding (id; _∘_)
open H-level equality-with-J
open Univalence-axiom equality-with-J

-- There is a dependent path from reflexivity for x to any dependent
-- path starting in x.

refl≡ :
  (x≡y : [ P ] x ≡ y) →
  [ (λ i → [ (λ j → P (min i j)) ] x ≡ x≡y i) ] refl {x = x} ≡ x≡y
refl≡ x≡y = λ i j → x≡y (min i j)

-- Transporting in one direction and then back amounts to doing
-- nothing.

transport∘transport :
  ∀ {p : I → Level} (P : ∀ i → Type (p i)) {p} →
  transport (λ i → P (- i)) 0̲ (transport P 0̲ p) ≡ p
transport∘transport P {p} = hsym λ i →
  comp (λ j → P (min i (- j)))
       (λ j → λ { (i = 0̲) → p
                ; (i = 1̲) → transport (λ k → P (- min j k)) (- j)
                              (transport P 0̲ p)
                })
       (transport (λ j → P (min i j)) (- i) p)

-- One form of transporting can be expressed using trans and sym.

transport-≡ :
  {p : x ≡ y} {q : u ≡ v} (r : x ≡ u) →
  transport (λ i → p i ≡ q i) 0̲ r ≡
  trans (sym p) (trans r q)
transport-≡ {x = x} {p = p} {q = q} r = elim¹
  (λ p → transport (λ i → p i ≡ q i) 0̲ r ≡
         trans (sym p) (trans r q))
  (transport (λ i → x ≡ q i) 0̲ r  ≡⟨⟩
   subst (x ≡_) q r               ≡⟨ sym trans-subst ⟩
   trans r q                      ≡⟨ sym $ trans-reflˡ _ ⟩
   trans refl (trans r q)         ≡⟨⟩
   trans (sym refl) (trans r q)   ∎)
  p

-- The function htrans {x≡y = x≡y} {y≡z = y≡z} (const A) is pointwise
-- equal to trans.
--
-- Andrea Vezzosi helped me with this proof.

htrans-const :
  (x≡y : x ≡ y) (y≡z : y ≡ z) (p : u ≡ v) {q : v ≡ w} →
  htrans {x≡y = x≡y} {y≡z = y≡z} (const A) p q ≡ trans p q
htrans-const {A = A} {w = w} _ _ p {q = q} =
  (λ i → comp (λ _ → A) (s i) (q i))                  ≡⟨⟩

  (λ i →
     hcomp (λ j x → transport (λ _ → A) j (s i j x))
       (transport (λ _ → A) 0̲ (q i)))                 ≡⟨ (λ k i → hcomp (λ j x → cong (_$ s i j x) (transport-refl j) k)
                                                                    (cong (_$ q i) (transport-refl 0̲) k)) ⟩∎
  (λ i → hcomp (s i) (q i))                           ∎
  where
  s : ∀ i j → Partial (max i (- i)) A
  s i = λ where
    j (i = 0̲) → p (- j)
    _ (i = 1̲) → w

-- The following two lemmas are due to Anders Mörtberg.
--
-- Previously Andrea Vezzosi and I had each proved the second lemma in
-- much more convoluted ways (starting from a logical equivalence
-- proved by Anders; I had also gotten some useful hints from Andrea
-- for my proof).

-- Heterogeneous equality can be expressed in terms of homogeneous
-- equality.

heterogeneous≡homogeneous :
  {P : I → Type p} {p : P 0̲} {q : P 1̲} →
  ([ P ] p ≡ q) ≡ (transport P 0̲ p ≡ q)
heterogeneous≡homogeneous {P = P} {p = p} {q = q} = λ i →
  [ (λ j → P (max i j)) ] transport (λ j → P (min i j)) (- i) p ≡ q

-- A variant of the previous lemma.

heterogeneous↔homogeneous :
  (P : I → Type p) {p : P 0̲} {q : P 1̲} →
  ([ P ] p ≡ q) ↔ transport P 0̲ p ≡ q
heterogeneous↔homogeneous P =
  subst
    ([ P ] _ ≡ _ ↔_)
    heterogeneous≡homogeneous
    (Bijection.id equality-with-J)

-- The function dcong is pointwise equal to an expression involving
-- hcong.

dcong≡hcong :
  {B : A → Type b} {x≡y : x ≡ y} (f : (x : A) → B x) →
  dcong f x≡y ≡
  _↔_.to (heterogeneous↔homogeneous (λ i → B (x≡y i))) (hcong f x≡y)
dcong≡hcong {B = B} {x≡y = x≡y} f = elim
  (λ x≡y →
     dcong f x≡y ≡
     _↔_.to (heterogeneous↔homogeneous (λ i → B (x≡y i))) (hcong f x≡y))

  (λ x →
     dcong f (refl {x = x})                                            ≡⟨⟩

     (λ i → transport (λ _ → B x) i (f x))                             ≡⟨ (λ i → comp
                                                                             (λ j → transport (λ _ → B x) (- j) (f x) ≡ f x)
                                                                             (λ { j (i = 0̲) → (λ k → transport (λ _ → B x) (max k (- j)) (f x))
                                                                                ; j (i = 1̲) → transport
                                                                                (λ k → transport (λ _ → B x) (- min k j) (f x) ≡ f x)
                                                                                0̲ refl
                                                                                })
                                                                             (transport (λ _ → f x ≡ f x) (- i) refl)) ⟩

     transport (λ i → transport (λ _ → B x) (- i) (f x) ≡ f x) 0̲ refl  ≡⟨ cong (transport (λ i → transport (λ _ → B x) (- i) (f x) ≡ f x) 0̲ ∘
                                                                                (_$ refl)) $ sym $
                                                                          transport-refl 0̲ ⟩
     transport (λ i → transport (λ _ → B x) (- i) (f x) ≡ f x) 0̲
       (transport (λ _ → f x ≡ f x) 0̲ refl)                            ≡⟨⟩

     _↔_.to (heterogeneous↔homogeneous (λ i → B (refl {x = x} i)))
       (hcong f (refl {x = x}))                                        ∎)

  x≡y

-- A "computation" rule.

from-heterogeneous↔homogeneous-const-refl :
  (B : A → Type b) {x : A} {y : B x} →
  _↔_.from (heterogeneous↔homogeneous λ _ → B x) refl ≡
  sym (subst-refl B y)
from-heterogeneous↔homogeneous-const-refl B {x = x} {y = y} =
  transport (λ _ → y ≡ transport (λ _ → B x) 0̲ y) 0̲
    (transport
       (λ i → transport (λ _ → B x) i y ≡ transport (λ _ → B x) 0̲ y) 0̲
       (λ _ → transport (λ _ → B x) 0̲ y))                               ≡⟨ cong (_$ transport
                                                                                (λ i → transport (λ _ → B x) i y ≡
                                                                                transport (λ _ → B x) 0̲ y) 0̲
                                                                                (λ _ → transport (λ _ → B x) 0̲ y)) $
                                                                           transport-refl 0̲ ⟩
  transport
    (λ i → transport (λ _ → B x) i y ≡ transport (λ _ → B x) 0̲ y) 0̲
    (λ _ → transport (λ _ → B x) 0̲ y)                                   ≡⟨ transport-≡ (λ _ → transport (λ _ → B x) 0̲ y) ⟩

  trans (λ i → transport (λ _ → B x) (- i) y)
    (trans (λ _ → transport (λ _ → B x) 0̲ y)
       (λ _ → transport (λ _ → B x) 0̲ y))                               ≡⟨ cong (trans (λ i → transport (λ _ → B x) (- i) y)) $
                                                                           trans-symʳ (λ _ → transport (λ _ → B x) 0̲ y) ⟩

  trans (λ i → transport (λ _ → B x) (- i) y) refl                      ≡⟨ trans-reflʳ _ ⟩∎

  (λ i → transport (λ _ → B x) (- i) y)                                 ∎

-- A direct proof of something with the same type as Σ-≡,≡→≡.

Σ-≡,≡→≡′ :
  {p₁ p₂ : Σ A B} →
  (p : proj₁ p₁ ≡ proj₁ p₂) →
  subst B p (proj₂ p₁) ≡ proj₂ p₂ →
  p₁ ≡ p₂
Σ-≡,≡→≡′ {B = B} {p₁ = _ , y₁} {p₂ = _ , y₂} p q i =
  p i , lemma i
  where
  lemma : [ (λ i → B (p i)) ] y₁ ≡ y₂
  lemma = _↔_.from (heterogeneous↔homogeneous _) q

-- Σ-≡,≡→≡ is pointwise equal to Σ-≡,≡→≡′.

Σ-≡,≡→≡≡Σ-≡,≡→≡′ :
  {B : A → Type b}
  {p₁ p₂ : Σ A B}
  {p : proj₁ p₁ ≡ proj₁ p₂}
  {q : subst B p (proj₂ p₁) ≡ proj₂ p₂} →
  Σ-≡,≡→≡ {B = B} p q ≡ Σ-≡,≡→≡′ p q
Σ-≡,≡→≡≡Σ-≡,≡→≡′ {B = B} {p₁ = p₁} {p₂ = p₂} {p = p} {q = q} =
  elim₁
    (λ p →
       ∀ {p₁₂} (q : subst B p p₁₂ ≡ proj₂ p₂) →
       Σ-≡,≡→≡ p q ≡ Σ-≡,≡→≡′ p q)
    (λ q →
       Σ-≡,≡→≡ refl q                                          ≡⟨ Σ-≡,≡→≡-reflˡ q ⟩
       cong (_ ,_) (trans (sym $ subst-refl B _) q)            ≡⟨ cong (cong (_ ,_)) $
                                                                  elim¹
                                                                    (λ q →
                                                                       trans (sym $ subst-refl B _) q ≡
                                                                       _↔_.from (heterogeneous↔homogeneous _) q)
                                                                    (
           trans (sym $ subst-refl B _) refl                         ≡⟨ trans-reflʳ _ ⟩
           sym (subst-refl B _)                                      ≡⟨ sym $ from-heterogeneous↔homogeneous-const-refl B ⟩∎
           _↔_.from (heterogeneous↔homogeneous _) refl               ∎)
                                                                    q ⟩
       cong (_ ,_) (_↔_.from (heterogeneous↔homogeneous _) q)  ≡⟨⟩
       Σ-≡,≡→≡′ refl q                                         ∎)
    p q

-- All instances of an interval-indexed family are equal.

index-irrelevant : (P : I → Type p) → P i ≡ P j
index-irrelevant {i = i} {j = j} P =
  λ k → P (max (min i (- k)) (min j k))

-- Positive h-levels of P i can be expressed in terms of the h-levels
-- of dependent paths over P.

H-level-suc↔H-level[]≡ :
  {P : I → Type p} →
  H-level (suc n) (P i) ↔ (∀ x y → H-level n ([ P ] x ≡ y))
H-level-suc↔H-level[]≡ {n = n} {i = i} {P = P} =
  H-level (suc n) (P i)                                            ↝⟨ H-level-cong ext _ (≡⇒≃ $ index-irrelevant P) ⟩

  H-level (suc n) (P 1̲)                                            ↝⟨ inverse $ ≡↔+ _ ext ⟩

  ((x y : P 1̲) → H-level n (x ≡ y))                                ↝⟨ (Π-cong ext (≡⇒≃ $ index-irrelevant P) λ x → ∀-cong ext λ _ →
                                                                       ≡⇒↝ _ $ cong (λ x → H-level _ (x ≡ _)) (
      x                                                                  ≡⟨ sym $ transport∘transport (λ i → P (- i)) ⟩

      transport P 0̲ (transport (λ i → P (- i)) 0̲ x)                      ≡⟨ cong (λ f → transport P 0̲ (transport (λ i → P (- i)) 0̲ (f x))) $ sym $
                                                                            transport-refl 0̲ ⟩∎
      transport P 0̲
        (transport (λ i → P (- i)) 0̲ (transport (λ _ → P 1̲) 0̲ x))        ∎)) ⟩

  ((x : P 0̲) (y : P 1̲) → H-level n (transport P 0̲ x ≡ y))          ↝⟨ (∀-cong ext λ x → ∀-cong ext λ y → H-level-cong ext n $ inverse $
                                                                       heterogeneous↔homogeneous P) ⟩□
  ((x : P 0̲) (y : P 1̲) → H-level n ([ P ] x ≡ y))                  □

private

  -- A simple lemma used below.

  H-level-suc→H-level[]≡ :
    ∀ n → H-level (1 + n) (P 0̲) → H-level n ([ P ] x ≡ y)
  H-level-suc→H-level[]≡ {P = P} {x = x} {y = y} n =
    H-level (1 + n) (P 0̲)              ↔⟨ H-level-suc↔H-level[]≡ ⟩
    (∀ x y → H-level n ([ P ] x ≡ y))  ↝⟨ (λ f → f _ _) ⟩□
    H-level n ([ P ] x ≡ y)            □

-- A form of proof irrelevance for paths that are propositional at one
-- end-point.

heterogeneous-irrelevance₀ :
  Is-proposition (P 0̲) → [ P ] x ≡ y
heterogeneous-irrelevance₀ {P = P} {x = x} {y = y} =
  Is-proposition (P 0̲)        ↝⟨ H-level-suc→H-level[]≡ _ ⟩
  Contractible ([ P ] x ≡ y)  ↝⟨ proj₁ ⟩□
  [ P ] x ≡ y                 □

-- A form of UIP for squares that are sets on one corner.

heterogeneous-UIP₀₀ :
  {P : I → I → Type p}
  {x : ∀ i → P i 0̲} {y : ∀ i → P i 1̲}
  {p : [ (λ j → P 0̲ j) ] x 0̲ ≡ y 0̲}
  {q : [ (λ j → P 1̲ j) ] x 1̲ ≡ y 1̲} →
  Is-set (P 0̲ 0̲) →
  [ (λ i → [ (λ j → P i j) ] x i ≡ y i) ] p ≡ q
heterogeneous-UIP₀₀ {P = P} {x = x} {y = y} {p = p} {q = q} =
  Is-set (P 0̲ 0̲)                                                ↝⟨ H-level-suc→H-level[]≡ 1 ⟩
  Is-proposition ([ (λ j → P 0̲ j) ] x 0̲ ≡ y 0̲)                  ↝⟨ H-level-suc→H-level[]≡ _ ⟩
  Contractible ([ (λ i → [ (λ j → P i j) ] x i ≡ y i) ] p ≡ q)  ↝⟨ proj₁ ⟩□
  [ (λ i → [ (λ j → P i j) ] x i ≡ y i) ] p ≡ q                 □

-- A variant of heterogeneous-UIP₀₀, "one level up".

heterogeneous-UIP₃₀₀ :
  {P : I → I → I → Type p}
  {x : ∀ i j → P i j 0̲} {y : ∀ i j → P i j 1̲}
  {p : ∀ i → [ (λ k → P i 0̲ k) ] x i 0̲ ≡ y i 0̲}
  {q : ∀ i → [ (λ k → P i 1̲ k) ] x i 1̲ ≡ y i 1̲}
  {r : [ (λ j → [ (λ k → P 0̲ j k) ] x 0̲ j ≡ y 0̲ j) ] p 0̲ ≡ q 0̲}
  {s : [ (λ j → [ (λ k → P 1̲ j k) ] x 1̲ j ≡ y 1̲ j) ] p 1̲ ≡ q 1̲} →
  H-level 3 (P 0̲ 0̲ 0̲) →
  [ (λ i → [ (λ j → [ (λ k → P i j k) ] x i j ≡ y i j) ] p i ≡ q i) ]
    r ≡ s
heterogeneous-UIP₃₀₀
  {P = P} {x = x} {y = y} {p = p} {q = q} {r = r} {s = s} =

  H-level 3 (P 0̲ 0̲ 0̲)                                                     ↝⟨ H-level-suc→H-level[]≡ 2 ⟩

  Is-set ([ (λ k → P 0̲ 0̲ k) ] x 0̲ 0̲ ≡ y 0̲ 0̲)                              ↝⟨ H-level-suc→H-level[]≡ 1 ⟩

  Is-proposition
    ([ (λ j → [ (λ k → P 0̲ j k) ] x 0̲ j ≡ y 0̲ j) ] p 0̲ ≡ q 0̲)             ↝⟨ H-level-suc→H-level[]≡ _ ⟩

  Contractible
    ([ (λ i → [ (λ j → [ (λ k → P i j k) ] x i j ≡ y i j) ] p i ≡ q i) ]
       r ≡ s)                                                             ↝⟨ proj₁ ⟩□

  [ (λ i → [ (λ j → [ (λ k → P i j k) ] x i j ≡ y i j) ] p i ≡ q i) ]
    r ≡ s                                                                 □

-- The following three lemmas can be used to implement the truncation
-- cases of (at least some) eliminators for (at least some) HITs. For
-- some examples, see H-level.Truncation.Propositional, Quotient and
-- Eilenberg-MacLane-space.

-- A variant of heterogeneous-irrelevance₀.

heterogeneous-irrelevance :
  {P : A → Type p} →
  (∀ x → Is-proposition (P x)) →
  {x≡y : x ≡ y} {p₁ : P x} {p₂ : P y} →
  [ (λ i → P (x≡y i)) ] p₁ ≡ p₂
heterogeneous-irrelevance {x = x} {P = P} P-prop {x≡y} {p₁} {p₂} =
                                 $⟨ P-prop ⟩
  (∀ x → Is-proposition (P x))   ↝⟨ _$ _ ⟩
  Is-proposition (P x)           ↝⟨ heterogeneous-irrelevance₀ ⟩□
  [ (λ i → P (x≡y i)) ] p₁ ≡ p₂  □

-- A variant of heterogeneous-UIP₀₀.
--
-- The cubical library contains (or used to contain) a lemma with
-- basically the same type, but with a seemingly rather different
-- proof, implemented by Zesen Qian.

heterogeneous-UIP :
  {P : A → Type p} →
  (∀ x → Is-set (P x)) →
  {eq₁ eq₂ : x ≡ y} (eq₃ : eq₁ ≡ eq₂) {p₁ : P x} {p₂ : P y}
  (eq₄ : [ (λ j → P (eq₁ j)) ] p₁ ≡ p₂)
  (eq₅ : [ (λ j → P (eq₂ j)) ] p₁ ≡ p₂) →
  [ (λ i → [ (λ j → P (eq₃ i j)) ] p₁ ≡ p₂) ] eq₄ ≡ eq₅
heterogeneous-UIP {x = x} {P = P} P-set eq₃ {p₁} {p₂} eq₄ eq₅ =
                                                         $⟨ P-set ⟩
  (∀ x → Is-set (P x))                                   ↝⟨ _$ _ ⟩
  Is-set (P x)                                           ↝⟨ heterogeneous-UIP₀₀ ⟩□
  [ (λ i → [ (λ j → P (eq₃ i j)) ] p₁ ≡ p₂) ] eq₄ ≡ eq₅  □

-- A variant of heterogeneous-UIP, "one level up".

heterogeneous-UIP₃ :
  {P : A → Type p} →
  (∀ x → H-level 3 (P x)) →
  {eq₁ eq₂ : x ≡ y} {eq₃ eq₄ : eq₁ ≡ eq₂}
  (eq₅ : eq₃ ≡ eq₄)
  {p₁ : P x} {p₂ : P y}
  {eq₆ : [ (λ k → P (eq₁ k)) ] p₁ ≡ p₂}
  {eq₇ : [ (λ k → P (eq₂ k)) ] p₁ ≡ p₂}
  (eq₈ : [ (λ j → [ (λ k → P (eq₃ j k)) ] p₁ ≡ p₂) ] eq₆ ≡ eq₇)
  (eq₉ : [ (λ j → [ (λ k → P (eq₄ j k)) ] p₁ ≡ p₂) ] eq₆ ≡ eq₇) →
  [ (λ i → [ (λ j → [ (λ k → P (eq₅ i j k)) ] p₁ ≡ p₂) ] eq₆ ≡ eq₇) ]
    eq₈ ≡ eq₉
heterogeneous-UIP₃
  {x = x} {P = P}
  P-groupoid eq₅ {p₁ = p₁} {p₂ = p₂} {eq₆ = eq₆} {eq₇ = eq₇} eq₈ eq₉ =
                                                                       $⟨ P-groupoid ⟩
  (∀ x → H-level 3 (P x))                                              ↝⟨ _$ _ ⟩
  H-level 3 (P x)                                                      ↝⟨ heterogeneous-UIP₃₀₀ ⟩□
  [ (λ i → [ (λ j → [ (λ k → P (eq₅ i j k)) ] p₁ ≡ p₂) ] eq₆ ≡ eq₇) ]
    eq₈ ≡ eq₉                                                          □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2017-07-26
-- Better error message when constructor not fully applied.

open import Agda.Builtin.Nat

test : (Nat → Nat) → Nat
test suc = suc zero

-- WAS: Type mismatch
-- NOW: Cannot pattern match on functions
-- when checking that the pattern suc has type Nat → Nat

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2018-10-17, re #2757
--
-- Don't project from erased matches.

open import Agda.Builtin.List
open import Common.Prelude

data IsCons {A : Set} : List A → Set where
  isCons : ∀{@0 x : A} {@0 xs : List A} → IsCons (x ∷ xs)

headOfErased : ∀{A} (@0 xs : List A) → IsCons xs → A
headOfErased (x ∷ xs) isCons = x

-- Should fail with error:
--
-- Variable x is declared erased, so it cannot be used here

main = printNat (headOfErased (1 ∷ 2 ∷ []) isCons)

-- Otherwise, main segfaults.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------------
-- Well-founded induction on the lexicographic order on natural numbers
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Data.Nat.Induction.NonAcc.LexicographicI where

open import FOTC.Base
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------

Lexi-wfind :
  (A : D → D → Set) →
  (∀ {m₁ n₁} → N m₁ → N n₁ →
     (∀ {m₂ n₂} → N m₂ → N n₂ → Lexi m₂ n₂ m₁ n₁ → A m₂ n₂) → A m₁ n₁) →
  ∀ {m n} → N m → N n → A m n
Lexi-wfind A h Nm Nn = h Nm Nn (helper₂ Nm Nn)
  where
  helper₁ : ∀ {m n o} → N m → N n → N o → m < o → o < succ₁ n  → m < n
  helper₁ {m} {n} {o} Nm Nn No m<o o<Sn =
    Sx≤y→x<y Nm Nn (≤-trans (nsucc Nm) No Nn
                            (x<y→Sx≤y Nm No m<o)
                            (Sx≤Sy→x≤y {o} {n} (x<y→Sx≤y No (nsucc Nn) o<Sn)))

  helper₂ : ∀ {m₁ n₁ m₂ n₂} → N m₁ → N n₁ → N m₂ → N n₂ →
            Lexi m₂ n₂ m₁ n₁ → A m₂ n₂

  helper₂ Nm₁ Nn₂ nzero nzero 00<00 =
    h nzero nzero (λ Nm' Nn' m'n'<00 → ⊥-elim (xy<00→⊥ Nm' Nn' m'n'<00))

  helper₂ nzero nzero (nsucc Nm₂) nzero Sm₂0<00 = ⊥-elim (Sxy<0y'→⊥ Sm₂0<00)

  helper₂ (nsucc Nm₁) nzero (nsucc Nm₂) nzero Sm₂0<Sm₁0 =
    h (nsucc Nm₂) nzero (λ Nm' Nn' m'n'<Sm₂0 →
      helper₂ Nm₁ nzero Nm' Nn'
              (inj₁ (helper₁ Nm' Nm₁ (nsucc Nm₂)
                             (xy<x'0→x<x' Nn' m'n'<Sm₂0)
                             (xy<x'0→x<x' nzero Sm₂0<Sm₁0))))

  helper₂ nzero (nsucc Nn₁) (nsucc Nm₂) nzero Sm₂0<0Sn₁ =
    ⊥-elim (Sxy<0y'→⊥ Sm₂0<0Sn₁)

  helper₂ (nsucc Nm₁) (nsucc Nn₁) (nsucc Nm₂) nzero Sm₂0<Sm₁Sn₁ =
    h (nsucc Nm₂) nzero (λ Nm' Nn' m'n'<Sm₂0 →
      helper₂ (nsucc Nm₁) Nn₁ Nm' Nn'
        (inj₁ (case (λ Sm₂<Sm₁ → x<y→x<Sy Nm' Nm₁
                                          (helper₁ Nm' Nm₁ (nsucc Nm₂)
                                                  (xy<x'0→x<x' Nn' m'n'<Sm₂0)
                                                  Sm₂<Sm₁))
                    (λ Sm₂≡Sm₁∧0<Sn₁ → x<y→y≡z→x<z (xy<x'0→x<x' Nn' m'n'<Sm₂0)
                                                   (∧-proj₁ Sm₂≡Sm₁∧0<Sn₁))
                    Sm₂0<Sm₁Sn₁)))

  helper₂ nzero nzero nzero (nsucc Nn₂) 0Sn₂<00 = ⊥-elim (0Sx<00→⊥ 0Sn₂<00)

  helper₂ (nsucc {m₁} Nm₁) nzero nzero (nsucc Nn₂) 0Sn₂<Sm₁0 =
    h nzero (nsucc Nn₂) (λ Nm' Nn' m'n'<0Nn₂ →
      helper₂ Nm₁ (nsucc Nn₂) Nm' Nn'
              (case (λ m'<0 → ⊥-elim (x<0→⊥ Nm' m'<0))
                    (λ m'≡0∧n'<Sn₂ →
                      case (λ 0<m₁ → inj₁ (x≡y→y<z→x<z (∧-proj₁ m'≡0∧n'<Sn₂) 0<m₁))
                           (λ 0≡m₁ → inj₂ ((trans (∧-proj₁ m'≡0∧n'<Sn₂) 0≡m₁)
                                          , (∧-proj₂ m'≡0∧n'<Sn₂)))
                           (x<Sy→x<y∨x≡y nzero Nm₁ 0<Sm₁))
                    m'n'<0Nn₂))

    where
    0<Sm₁ : zero < succ₁ m₁
    0<Sm₁ = xy<x'0→x<x' (nsucc Nn₂) 0Sn₂<Sm₁0

  helper₂ nzero (nsucc Nn₁) nzero (nsucc Nn₂) 0Sn₂<0Sn₁ =
    case (λ 0<0 → ⊥-elim (0<0→⊥ 0<0))
         (λ 0≡0∧Sn₂<Sn₁ →
           h nzero (nsucc Nn₂) (λ Nm' Nn' m'n'<0Sn₂ →
             case (λ m'<0 → ⊥-elim (x<0→⊥ Nm' m'<0))
                  (λ m'≡0∧n'<Sn₂ →
                    helper₂ nzero Nn₁ Nm' Nn'
                      (inj₂ (∧-proj₁ m'≡0∧n'<Sn₂
                            , helper₁ Nn' Nn₁ (nsucc Nn₂)
                                          (∧-proj₂ m'≡0∧n'<Sn₂)
                                          (∧-proj₂ 0≡0∧Sn₂<Sn₁))))
                  m'n'<0Sn₂))
         0Sn₂<0Sn₁

  helper₂ (nsucc Nm₁) (nsucc Nn₁) nzero (nsucc Nn₂) 0Sn₂<Sm₁Sn₁ =
    h nzero (nsucc Nn₂) (λ Nm' Nn' m'n'<0Sn₂ →
      helper₂ (nsucc Nm₁) Nn₁ Nm' Nn'
        (case (λ m'<0 → ⊥-elim (x<0→⊥ Nm' m'<0))
              (λ m'≡0∧n'<Sn₂ →
                case (λ 0<Sm₁ → inj₁ (x≡y→y<z→x<z (∧-proj₁ m'≡0∧n'<Sn₂) 0<Sm₁))
                     (λ 0≡Sn₂∧Sn₂<Sn₁ → ⊥-elim (0≢S (∧-proj₁ 0≡Sn₂∧Sn₂<Sn₁)))
                     0Sn₂<Sm₁Sn₁)
              m'n'<0Sn₂))

  helper₂ nzero nzero (nsucc Nm₂) (nsucc Nn₂) Sm₂Sn₂<00 =
    ⊥-elim (xy<00→⊥ (nsucc Nm₂) (nsucc Nn₂) Sm₂Sn₂<00)

  helper₂ (nsucc {m₁} Nm₁) nzero (nsucc {m₂} Nm₂) (nsucc Nn₂) Sm₂Sn₂<Sm₁0 =
    h (nsucc Nm₂) (nsucc Nn₂) (λ Nm' Nn' m'n'<Sm₂Sn₂ →
      helper₂ Nm₁ (nsucc Nn₂) Nm' Nn'
        (case (λ m'<Sm₂ → inj₁ (helper₁ Nm' Nm₁ (nsucc Nm₂) m'<Sm₂ Sm₂<Sm₁))
              (λ m'≡Sm₂∧n'<Sn₂ →
                case (λ m'<m₁ → inj₁ m'<m₁)
                     (λ m'≡m₁ → inj₂ (m'≡m₁ , ∧-proj₂ m'≡Sm₂∧n'<Sn₂))
                     (x<Sy→x<y∨x≡y Nm' Nm₁
                                   (x≡y→y<z→x<z (∧-proj₁ m'≡Sm₂∧n'<Sn₂) Sm₂<Sm₁)))
              m'n'<Sm₂Sn₂))

    where
    Sm₂<Sm₁ : succ₁ m₂ < succ₁ m₁
    Sm₂<Sm₁ = xy<x'0→x<x' (nsucc Nn₂) Sm₂Sn₂<Sm₁0

  helper₂ nzero (nsucc Nn₁) (nsucc Nm₂) (nsucc Nn₂) Sm₂Sn₂<0Sn₁
    = ⊥-elim (Sxy<0y'→⊥ Sm₂Sn₂<0Sn₁)

  helper₂ (nsucc Nm₁) (nsucc Nn₁) (nsucc Nm₂) (nsucc Nn₂) Sm₂Sn₂<Sm₁Sn₁ =
    h (nsucc Nm₂) (nsucc Nn₂) (λ Nm' Nn' m'n'<Sm₂Sn₂ →
      helper₂ (nsucc Nm₁) Nn₁ Nm' Nn'
        (case (λ Sm₂<Sm₁ →
                 case (λ m'<Sm₂ → inj₁ (x<y→x<Sy Nm' Nm₁ (helper₁ Nm' Nm₁ (nsucc Nm₂) m'<Sm₂ Sm₂<Sm₁)))
                      (λ m'≡Sm₂∧n'<Sn₂ → inj₁ (x≡y→y<z→x<z (∧-proj₁ m'≡Sm₂∧n'<Sn₂) Sm₂<Sm₁))
                      m'n'<Sm₂Sn₂)

              (λ Sm₂≡Sm₁∧Sn₂<Sn₁ →
                case (λ m'<Sm₂ → inj₁ (x<y→y≡z→x<z m'<Sm₂ (∧-proj₁ Sm₂≡Sm₁∧Sn₂<Sn₁)))
                     (λ m'≡Sm₂∧n'<Sn₂ → inj₂
                       (trans (∧-proj₁ m'≡Sm₂∧n'<Sn₂) (∧-proj₁ Sm₂≡Sm₁∧Sn₂<Sn₁)
                       , helper₁ Nn' Nn₁ (nsucc Nn₂) (∧-proj₂ m'≡Sm₂∧n'<Sn₂) (∧-proj₂ Sm₂≡Sm₁∧Sn₂<Sn₁)))
                     m'n'<Sm₂Sn₂)
              Sm₂Sn₂<Sm₁Sn₁))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Numeral.Natural.Oper.Divisibility where

import      Lvl
open import Data
open import Data.Boolean
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Modulo

-- Divisibility check
_∣?_ : ℕ → ℕ → Bool
𝟎    ∣? _ = 𝐹
𝐒(y) ∣? x = zero?(x mod 𝐒(y))

-- Divisibility check
_∣₀?_ : ℕ → ℕ → Bool
𝟎 ∣₀? 𝟎    = 𝑇
𝟎 ∣₀? 𝐒(_) = 𝐹
𝐒(y) ∣₀? x = zero?(x mod 𝐒(y))

{-
open import Numeral.Natural.Oper
open import Numeral.Natural.UnclosedOper
open import Data.Option as Option using (Option)

{-# TERMINATING #-}
_∣?_ : ℕ → ℕ → Bool
_    ∣? 𝟎    = 𝑇
𝟎    ∣? 𝐒(_) = 𝐹
𝐒(x) ∣? 𝐒(y) with (x −? y)
... | Option.Some(xy) = xy ∣? 𝐒(y)
... | Option.None     = 𝐹
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
record R (A : Set) : Set where field giveA : A
open R ⦃ … ⦄

record WrapR (A : Set) : Set where field instance ⦃ wrappedR ⦄ : R A
open WrapR ⦃ … ⦄

postulate
  instance R-instance : ∀ {X} → WrapR X

data D : Set where

works : D
works = giveA ⦃ WrapR.wrappedR (R-instance {D}) ⦄

fails : D
fails = giveA ⦃ {!!} ⦄
-- No instance of type R D was found in scope.

-- open import Agda.Primitive

-- {-
-- record IsBottom₀ (⊥ : Set) : Set (lsuc lzero) where
--   field
--     ⊥₀-elim : ⊥ → {A : Set lzero} → A

-- open IsBottom₀ ⦃ … ⦄ public

-- record Bottom₀ : Set (lsuc lzero) where
--   field
--     ⊥₀ : Set
--     ⦃ isBottom ⦄ : IsBottom₀ ⊥₀

-- open Bottom₀ ⦃ … ⦄ public

-- test : ⦃ bottom : ∀ {l : Set} → Bottom₀ ⦄ {fake : ⊥₀ ⦃ bottom {Level} ⦄} {real : Set} → real
-- test ⦃ bottom ⦄ {fake} {real} = ⊥₀-elim {⊥₀ ⦃ bottom ⦄} ⦃ Bottom₀.isBottom (bottom {Level}) ⦄ fake
-- -}

-- record IsBottom₀ (⊥ : Set) a : Set (lsuc a) where
--   field
--     ⊥₀-elim : ⊥ → {A : Set a} → A

-- open IsBottom₀ ⦃ … ⦄ public

-- record Bottom₀ a : Set (lsuc a) where
--   field
--     ⊥₀ : Set
--     ⦃ isBottom ⦄ : IsBottom₀ ⊥₀ a

-- open Bottom₀ ⦃ … ⦄ public

-- postulate
--   instance Bi : ∀ {a} → Bottom₀ a

-- --test : ⦃ bottom : ∀ {a} → Bottom₀ a ⦄ {fake : ⊥₀ {lzero}} {real : Set} → real
-- --test ⦃ bottom ⦄ {fake} {real} = let instance b = Bottom₀.isBottom (bottom {lzero}) in ⊥₀-elim {⊥₀ {lzero} ⦃ bottom ⦄} {lzero} ⦃ {!Bottom₀.isBottom bottom!} ⦄ fake

-- test : {fake : ⊥₀ {lzero}} {real : Set} → real
-- test {fake} {real} = ⊥₀-elim {⊥₀ {lzero} ⦃ Bi ⦄} {lzero} ⦃ Bottom₀.isBottom Bi ⦄ fake

-- -- record Bottom₀ a : Set (lsuc a) where
-- --   field
-- --     ⊥₀ : Set
-- --     ⊥₀-elim : ⊥₀ → {A : Set a} → A

-- -- open Bottom₀ ⦃ … ⦄ public

-- -- test : ⦃ bottom : ∀ {a} → Bottom₀ a ⦄ {fake : ⊥₀ {lzero}} {real : Set} → real
-- -- test ⦃ bottom ⦄ {fake} {real} = ⊥₀-elim fake -- ⊥₀-elim {⊥₀ {lzero} ⦃ bottom ⦄} {lzero} ⦃ bottom ⦄ fake

-- -- postulate
-- --   B : Set

-- -- record IsB (r : Set) a : Set (lsuc a) where
-- --   field
-- --     gotB : B
-- --     xx : r

-- -- open IsB ⦃ … ⦄ public

-- -- record RB a : Set (lsuc a) where
-- --   field
-- --     r : Set
-- --     ⦃ isB ⦄ : IsB r a

-- -- open RB ⦃ … ⦄ public

-- -- testB : ⦃ bottom : ∀ {a} → RB a ⦄ → B
-- -- testB ⦃ bottom ⦄ = gotB ⦃ {!isB bottom {lzero}!} ⦄