------------------------------------------------------------------------
-- Equality lemmata.
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
open import Graded.Modality

module Definition.Typed.Consequences.Equality
  {a} {M : Set a}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  where

open Type-restrictions R

open import Definition.Untyped M
open import Definition.Untyped.Neutral M type-variant
open import Definition.Untyped.Neutral.Atomic M type-variant
open import Definition.Untyped.Sup R
open import Definition.Untyped.Whnf M type-variant
open import Definition.Typed R
import Definition.Typed.Consequences.Inequality R as I
open import Definition.Typed.Properties R
open import Definition.Typed.EqRelInstance R
open import Definition.Typed.Inversion R
open import Definition.Typed.Well-formed R
open import Definition.LogicalRelation R
open import Definition.LogicalRelation.Hidden R
open import Definition.LogicalRelation.Fundamental.Reducibility R
open import Definition.LogicalRelation.Substitution.Introductions R

open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (1+)
open import Tools.Product as Σ
import Tools.PropositionalEquality as PE
open import Tools.Relation

private
  variable
    ∇         : DCon (Term ) _
    Γ         : Cons _ _
    A B C t u : Term _
    l         : Lvl _
    V         : Set a
    b         : BinderMode
    p q       : M
    s         : Strength

opaque

  -- If the WHNF A is judgmentally equal to Level, then A is
  -- propositionally equal to Level (given a certain assumption).

  Level≡A :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ Level ≡ A → Whnf (Γ .defs) A → A PE.≡ Level
  Level≡A {Γ} {A} Level≡A A-whnf =
                $⟨ Level≡A ⟩
    Γ ⊢ Level ≡ A       →⟨ ⊩Level≡⇔ .proj₁ ∘→ proj₂ ∘→ reducible-⊩≡ ⟩
    Γ ⊩Level Level ≡ A  ≡⟨ PE.refl ⟩→
    Γ ⊢ A ⇒* Level      →⟨ flip whnfRed* A-whnf ⟩
    A PE.≡ Level        □

opaque

  -- If equality reflection is allowed and Level is a small type, then
  -- there is a WHNF A that is judgementally equal to Level but not
  -- propositionally equal to Level (given a certain assumption).

  whnf≢Level :
    Equality-reflection →
    Level-is-small →
    » ∇ →
    ∃₂ λ (Γ : Con Term ) (A : Term ) →
      ∇ » Γ ⊢ Level ≡ A × Whnf ∇ A × A PE.≢ Level
  whnf≢Level ok Level-ok »∇ =
    ε ∙ Id U₀ Level Empty ,
    Empty ,
    univ
      (equality-reflection′ ok $
       var₀ (Idⱼ′ (Levelⱼ (ε »∇) Level-ok) (Emptyⱼ (ε »∇)))) ,
    Emptyₙ ,
    (λ ())

opaque

  -- If the WHNF A is judgmentally equal to U l, then A is
  -- propositionally equal to U something (given a certain
  -- assumption).

  U≡A :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ U l ≡ A → Whnf (Γ .defs) A → ∃ λ k → A PE.≡ U k
  U≡A {Γ} {l} {A} U≡A A-whnf =    $⟨ U≡A ⟩
    Γ ⊢ U l ≡ A                   →⟨ reducible-⊩≡ ⟩
    (∃ λ l′ → Γ ⊩⟨ l′ ⟩ U l ≡ A)  →⟨ (λ (_ , U≡A) → let (_ , _ , u , d , _) = ⊩U≡⇔ .proj₁ U≡A in u , d) ⟩
    (∃ λ k → Γ ⊢ A ⇒* U k)        →⟨ Σ.map idᶠ (flip whnfRed* A-whnf) ⟩
    (∃ λ k → A PE.≡ U k)          □

opaque

  -- If equality reflection is allowed, then there is a WHNF A that is
  -- judgementally equal to a universe but not propositionally
  -- equal to any universe (given a certain assumption).

  whnf≢U :
    Equality-reflection →
    Unitʷ-allowed →
    » ∇ →
    ∃₃ λ (Γ : Con Term ) (l : Lvl ) (A : Term ) →
      ∇ » Γ ⊢ U l ≡ A × Whnf ∇ A × ¬ ∃ λ l → A PE.≡ U l
  whnf≢U ok₁ ok₂ »∇ =
    ε ∙
      Id (U (level (sucᵘ zeroᵘ))) U₀ (Lift (level (sucᵘ zeroᵘ)) Empty) ,
    zeroᵘₗ ,
    Lift (level (sucᵘ zeroᵘ)) Empty ,
    univ
      (equality-reflection′ ok₁ $
       var₀ $
       Idⱼ′
         (Uⱼ (⊢zeroᵘ (ε »∇)))
         (_⊢_∷_.conv (Liftⱼ′ (⊢1ᵘ+ (⊢zeroᵘ (ε »∇))) (Emptyⱼ (ε »∇))) $
          U-cong-⊢≡ (supᵘₗ-zeroˡ (⊢1ᵘ+ (⊢zeroᵘ (ε »∇)))))) ,
    Liftₙ ,
    (λ ())

opaque

  -- If the WHNF A is judgmentally equal to Lift l B, then A is
  -- propositionally equal to Lift something (given a certain
  -- assumption).

  Lift≡A :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ Lift l B ≡ A → Whnf (Γ .defs) A → ∃₂ λ k C → A PE.≡ Lift k C
  Lift≡A {Γ} {l} {B} {A} Lift≡A A-whnf = $⟨ Lift≡A ⟩
    Γ ⊢ Lift l B ≡ A                     →⟨ reducible-⊩≡ ⟩
    (∃ λ l′ → Γ ⊩⟨ l′ ⟩ Lift l B ≡ A)    →⟨ (λ (_ , Lift≡A) → let _ , _ , D , _ = ⊩Lift≡⇔ .proj₁ Lift≡A in _ , _ , D) ⟩
    (∃₂ λ k C → Γ ⊢ A ⇒* Lift k C)       →⟨ Σ.map idᶠ $ Σ.map idᶠ (flip whnfRed* A-whnf) ⟩
    (∃₂ λ k C → A PE.≡ Lift k C)         □

opaque

  -- If equality reflection is allowed, then there is a WHNF A that is
  -- judgementally equal to a Lift type but not propositionally
  -- equal to any Lift type (given a certain assumption).

  whnf≢Lift :
    Equality-reflection →
    Unitʷ-allowed →
    » ∇ →
    ∃₄ λ (Γ : Con Term ) (l : Lvl ) (B : Term ) (A : Term ) →
      ∇ » Γ ⊢ Lift l B ≡ A × Whnf ∇ A × ¬ ∃₂ λ l B → A PE.≡ Lift l B
  whnf≢Lift ok₁ ok₂ »∇ =
    ε ∙ Id (U (zeroᵘₗ supᵘₗ zeroᵘₗ)) (Lift zeroᵘₗ ℕ) Unitʷ ,
    zeroᵘₗ ,
    ℕ ,
    Unitʷ ,
    univ
      (equality-reflection′ ok₁ $
       var₀ $
       Idⱼ′ (Liftⱼ′ (⊢zeroᵘ (ε »∇)) (ℕⱼ (ε »∇))) $
       _⊢_∷_.conv (Unitⱼ (ε »∇) ok₂) $
       U-cong-⊢≡ (sym-⊢≡∷L (supᵘₗ-zeroˡ (⊢zeroᵘ (ε »∇))))) ,
    Unitₙ ,
    (λ ())

opaque

  -- If the WHNF A is judgmentally equal to ℕ, then A is
  -- propositionally equal to ℕ (given a certain assumption).

  ℕ≡A :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ ℕ ≡ A → Whnf (Γ .defs) A → A PE.≡ ℕ
  ℕ≡A {Γ} {A} ℕ≡A A-whnf =
                $⟨ ℕ≡A ⟩
    Γ ⊢ ℕ ≡ A   →⟨ ⊩ℕ≡⇔ .proj₁ ∘→ proj₂ ∘→ reducible-⊩≡ ⟩
    Γ ⊩ℕ ℕ ≡ A  ≡⟨ PE.refl ⟩→
    Γ ⊢ A ⇒* ℕ  →⟨ flip whnfRed* A-whnf ⟩
    A PE.≡ ℕ    □

opaque

  -- If equality reflection is allowed, then there is a WHNF A that is
  -- judgementally equal to ℕ but not propositionally equal to ℕ.

  whnf≢ℕ :
    Equality-reflection →
    » ∇ →
    ∃₂ λ (Γ : Con Term ) (A : Term ) →
      ∇ » Γ ⊢ ℕ ≡ A × Whnf ∇ A × A PE.≢ ℕ
  whnf≢ℕ ok »∇ =
    ε ∙ Id U₀ ℕ Empty ,
    Empty ,
    univ
      (equality-reflection′ ok $
       var₀ (Idⱼ′ (ℕⱼ (ε »∇)) (Emptyⱼ (ε »∇)))) ,
    Emptyₙ ,
    (λ ())

opaque

  -- If the WHNF A is judgmentally equal to Empty, then A is
  -- propositionally equal to Empty (given a certain assumption).

  Empty≡A :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ Empty ≡ A → Whnf (Γ .defs) A → A PE.≡ Empty
  Empty≡A {Γ} {A} Empty≡A A-whnf =
                        $⟨ Empty≡A ⟩
    Γ ⊢ Empty ≡ A       →⟨ ⊩Empty≡⇔ .proj₁ ∘→ proj₂ ∘→ reducible-⊩≡ ⟩
    Γ ⊩Empty Empty ≡ A  ≡⟨ PE.refl ⟩→
    Γ ⊢ A ⇒* Empty      →⟨ flip whnfRed* A-whnf ⟩
    A PE.≡ Empty        □

opaque

  -- If equality reflection is allowed, then there is a WHNF A that is
  -- judgementally equal to Empty but not propositionally equal
  -- to Empty.

  whnf≢Empty :
    Equality-reflection →
    » ∇ →
    ∃₂ λ (Γ : Con Term ) (A : Term ) →
      ∇ » Γ ⊢ Empty ≡ A × Whnf ∇ A × A PE.≢ Empty
  whnf≢Empty ok »∇ =
    ε ∙ Id U₀ Empty ℕ ,
    ℕ ,
    univ
      (equality-reflection′ ok $
       var₀ (Idⱼ′ (Emptyⱼ (ε »∇)) (ℕⱼ (ε »∇)))) ,
    ℕₙ ,
    (λ ())

opaque

  -- If the WHNF A is judgmentally equal to Unit s, then A is
  -- propositionally equal to Unit s (given a certain assumption).

  Unit≡A :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ Unit s ≡ A → Whnf (Γ .defs) A → A PE.≡ Unit s
  Unit≡A {Γ} {s} {A} Unit≡A A-whnf =
                                       $⟨ Unit≡A ⟩
    Γ ⊢ Unit s ≡ A                   →⟨ reducible-⊩≡ ⟩
    (∃ λ l′ → Γ ⊩⟨ l′ ⟩ Unit s ≡ A)  →⟨ (λ (_ , Unit≡A) →
                                            case ⊩Unit≡⇔ .proj₁ Unit≡A of λ {
                                              (⇒Unit , ok) →
                                            ⇒Unit }) ⟩
    Γ ⊢ A ⇒* Unit s        →⟨ flip whnfRed* A-whnf ⟩
    A PE.≡ Unit s          □

opaque

  -- If equality reflection is allowed, then there is a WHNF A that is
  -- judgementally equal to a unit type but not propositionally equal
  -- to any unit type (given a certain assumption).

  whnf≢Unit :
    Equality-reflection →
    Unit-allowed s →
    » ∇ →
    ∃₂ λ (Γ : Con Term ) (A : Term ) →
      ∇ » Γ ⊢ Unit s ≡ A × Whnf ∇ A ×
      ¬ ∃ λ s → A PE.≡ Unit s
  whnf≢Unit {s} ok₁ ok₂ »∇ =
    ε ∙ Id U₀ (Unit s) (Id (Unit s) (star s) (star s)) ,
    Id (Unit s) (star s) (star s) ,
    univ
      (equality-reflection′ ok₁ $ var₀ $
       let ⊢ε = ε »∇ in
       Idⱼ′ (Unitⱼ ⊢ε ok₂) $ Idⱼ (Unitⱼ ⊢ε ok₂) (starⱼ ⊢ε ok₂) (starⱼ ⊢ε ok₂)) ,
    Idₙ ,
    (λ ())

opaque

  -- If the neutral term B is judgmentally equal to the WHNF A, then A
  -- is neutral (given a certain assumption).

  ne≡A :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Neutral No-equality-reflection (Γ .defs) B →
    Γ ⊢ B ≡ A →
    Whnf (Γ .defs) A →
    Neutral No-equality-reflection (Γ .defs) A
  ne≡A {Γ} {B} {A} B-ne B≡A A-whnf =                       $⟨ B≡A ⟩
    Γ ⊢ B ≡ A                                              →⟨ reducible-⊩≡ ⟩
    (∃ λ l → Γ ⊩⟨ l ⟩ B ≡ A)                               →⟨ Σ.map idᶠ (Σ.map idᶠ proj₁) ∘→ ⊩ne≡⇔ B-ne .proj₁ ∘→ proj₂ ⟩
    (∃ λ C → Neutral No-equality-reflection (Γ .defs) C ×
             Γ ⊢ A ⇒* C)                                   →⟨ (λ (_ , C-ne , A⇒*C) →
                                                                 PE.subst (Neutral _ (Γ .defs)) (PE.sym $ whnfRed* A⇒*C A-whnf) C-ne) ⟩
    Neutral No-equality-reflection (Γ .defs) A             □

opaque

  -- If equality reflection is allowed, then there is a WHNF B that is
  -- judgementally equal (as a type) to a neutral term A but not
  -- propositionally equal to A.

  whnf≢ne :
    Equality-reflection →
    » ∇ →
    ∃₃ λ (Γ : Con Term ) (A B : Term ) →
      ∇ » Γ ⊢ A ≡ B × Neutral⁺ ∇ A × Whnf ∇ B × A PE.≢ B
  whnf≢ne ok »∇ =
    ε ∙ U₀ ∙ Id U₀ (var x0) Empty ,
    var x1 ,
    Empty ,
    univ
      (equality-reflection′ ok $
       var₀ (Idⱼ′ (var₀ (⊢U₀ (ε »∇))) (Emptyⱼ (∙ ⊢U₀ (ε »∇))))) ,
    var⁺ _ ,
    Emptyₙ ,
    (λ ())

opaque

  -- If a WHNF C is definitionally equal to ΠΣ⟨ b ⟩ p , q ▷ A ▹ B,
  -- then C has the shape ΠΣ⟨ b ⟩ p , q ▷ _ ▹ _ (given a certain
  -- assumption).

  ΠΣ≡Whnf :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B ≡ C → Whnf (Γ .defs) C →
    ∃₂ λ A′ B′ → C PE.≡ ΠΣ⟨ b ⟩ p , q ▷ A′ ▹ B′
  ΠΣ≡Whnf {Γ} {b} {p} {q} {A} {B} {C} ΠΣ≡C C-whnf =  $⟨ ΠΣ≡C ⟩
    Γ ⊢ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B ≡ C                    →⟨ reducible-⊩≡ ⟩
    (∃ λ l → Γ ⊩⟨ l ⟩ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B ≡ C)     →⟨ Σ.map idᶠ (Σ.map idᶠ proj₁) ∘→ proj₂ ∘→ proj₂ ∘→ ⊩ΠΣ≡⇔ .proj₁ ∘→ proj₂ ⟩
    (∃₂ λ A′ B′ → Γ ⊢ C ⇒* ΠΣ⟨ b ⟩ p , q ▷ A′ ▹ B′)  →⟨ Σ.map idᶠ $ Σ.map idᶠ (flip whnfRed* C-whnf) ⟩
    (∃₂ λ A′ B′ → C PE.≡ ΠΣ⟨ b ⟩ p , q ▷ A′ ▹ B′)    □

opaque

  -- If equality reflection is allowed, then there is a WHNF C that is
  -- judgementally equal to ΠΣ⟨ b ⟩ p , q ▷ A ▹ B but not
  -- propositionally equal to any Π- or Σ-type (given a certain
  -- assumption).

  whnf≢ΠΣ :
    Equality-reflection →
    ΠΣ-allowed b p q →
    » ∇ →
    ∃₄ λ (Γ : Con Term ) A B C →
      ∇ » Γ ⊢ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B ≡ C × Whnf ∇ C ×
      ¬ ∃₅ λ b p q A B → C PE.≡ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B
  whnf≢ΠΣ {b} {p} {q} ok₁ ok₂ »∇ =
    ε ∙ Id U₀ (ΠΣ⟨ b ⟩ p , q ▷ ℕ ▹ ℕ) ℕ ,
    ℕ , ℕ , ℕ ,
    univ
      (equality-reflection′ ok₁ $
       let ⊢ε = ε »∇ in
       var₀ $
       Idⱼ′ (ΠΣⱼ (⊢zeroᵘ (ε »∇)) (ℕⱼ (ε »∇)) (ℕⱼ (∙ ⊢ℕ (ε »∇))) ok₂)
         (ℕⱼ (ε »∇))) ,
    ℕₙ ,
    (λ ())

opaque

  -- If a WHNF A is definitionally equal to Π p , q ▷ B ▹ C, then A
  -- has the shape Π p , q ▷ _ ▹ _ (given a certain assumption).

  Π≡A :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ Π p , q ▷ B ▹ C ≡ A → Whnf (Γ .defs) A →
    ∃₂ λ B′ C′ → A PE.≡ Π p , q ▷ B′ ▹ C′
  Π≡A = ΠΣ≡Whnf

opaque

  -- If a WHNF A is definitionally equal to Σ⟨ s ⟩ p , q ▷ B ▹ C, then
  -- A has the shape Σ⟨ s ⟩ p , q ▷ _ ▹ _ (given a certain
  -- assumption).

  Σ≡A :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ Σ⟨ s ⟩ p , q ▷ B ▹ C ≡ A → Whnf (Γ .defs) A →
    ∃₂ λ B′ C′ → A PE.≡ Σ⟨ s ⟩ p , q ▷ B′ ▹ C′
  Σ≡A = ΠΣ≡Whnf

opaque

  -- If the WHNF B is judgmentally equal to Id A t u, then there are
  -- A′, t′ and u′ such that B is propositionally equal to Id A′ t′ u′
  -- (given a certain assumption).

  Id≡Whnf :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ Id A t u ≡ B → Whnf (Γ .defs) B →
    ∃₃ λ A′ t′ u′ → B PE.≡ Id A′ t′ u′
  Id≡Whnf {Γ} {A} {t} {u} {B} Id≡B B-whnf =
                                            $⟨ Id≡B ⟩
    Γ ⊢ Id A t u ≡ B                        →⟨ reducible-⊩≡ ⟩
    (∃ λ l → Γ ⊩⟨ l ⟩ Id A t u ≡ B)         →⟨ Σ.map idᶠ (Σ.map idᶠ (Σ.map idᶠ proj₁)) ∘→ proj₂ ∘→ ⊩Id≡⇔ .proj₁ ∘→ proj₂ ⟩
    (∃₃ λ A′ t′ u′ → Γ ⊢ B ⇒* Id A′ t′ u′)  →⟨ Σ.map idᶠ $ Σ.map idᶠ $ Σ.map idᶠ (flip whnfRed* B-whnf) ⟩
    (∃₃ λ A′ t′ u′ → B PE.≡ Id A′ t′ u′)    □

opaque

  -- If equality reflection is allowed, then there is a WHNF B that is
  -- judgementally equal to Id A t u but not propositionally equal to
  -- any identity type.

  whnf≢Id :
    Equality-reflection →
    » ∇ →
    ∃₅ λ (Γ : Con Term ) A t u B →
      ∇ » Γ ⊢ Id A t u ≡ B × Whnf ∇ B ×
      ¬ ∃₃ λ A t u → B PE.≡ Id A t u
  whnf≢Id ok »∇ =
    ε ∙ Id U₀ (Id ℕ zero zero) ℕ ,
    ℕ , zero , zero , ℕ ,
    univ
      (equality-reflection′ ok $
       let ⊢ε = ε »∇ in
       var₀ (Idⱼ′ (Idⱼ (ℕⱼ ⊢ε) (zeroⱼ ⊢ε) (zeroⱼ ⊢ε)) (ℕⱼ ⊢ε))) ,
    ℕₙ ,
    (λ ())

opaque

  -- If t is definitionally equal to rfl, then t reduces to rfl (given
  -- a certain assumption).

  rfl-norm :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ t ≡ rfl ∷ A → Γ ⊢ t ⇒* rfl ∷ A
  rfl-norm t≡rfl =
    case inversion-rfl (wf-⊢ t≡rfl .proj₂ .proj₂) of λ
      (_ , _ , _ , _ , A≡Id) →
    case ⊩≡∷Id⇔ .proj₁ $ proj₂ $ reducible-⊩≡∷ $
         conv t≡rfl A≡Id of λ
      (t′ , _ , t⇒*u , rfl⇒*v , _ , _ , u∼v) →
    case whnfRed*Term rfl⇒*v rflₙ of λ {
      PE.refl →
    case u∼v of λ where
      (rfl₌ _) →
        conv* t⇒*u (sym A≡Id)
      (ne _ (ne () _) _) }

opaque

  -- If equality reflection is allowed, then there is a term that is
  -- judgementally equal to rfl but that does not reduce to rfl.

  rfl-not-norm :
    Equality-reflection →
    » ∇ →
    ∃₃ λ (Γ : Con Term ) A t →
      ∇ » Γ ⊢ t ≡ rfl ∷ A × ¬ ∃₂ λ Δ B → ∇ » Δ ⊢ t ⇒* rfl ∷ B
  rfl-not-norm ok »∇ =
    let ⊢Id = Idⱼ′ (zeroⱼ (ε »∇)) (zeroⱼ (ε »∇)) in
    ε ∙ Id ℕ zero zero ∙ Id (Id ℕ zero zero) (var x0) rfl ,
    Id ℕ zero zero , var x1 ,
    (equality-reflection′ ok $
     var₀ (Idⱼ′ (var₀ ⊢Id) (rflⱼ (zeroⱼ (∙ ⊢Id))))) ,
    (λ { (_ , _ , x1⇒ ⇨ _) → neRedTerm x1⇒ (var⁺ _) })

opaque

  -- If the WHNF t is judgmentally equal to rfl, then t is
  -- propositionally equal to rfl (given a certain assumption).

  whnf≡rfl :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ t ≡ rfl ∷ A → Whnf (Γ .defs) t → t PE.≡ rfl
  whnf≡rfl = whnfRed*Term ∘→ rfl-norm

opaque

  -- If equality reflection is allowed, then there is a WHNF t that is
  -- judgementally equal to rfl but not propositionally equal to rfl.

  whnf≢rfl :
    Equality-reflection →
    » ∇ →
    ∃₃ λ (Γ : Con Term ) A t →
      ∇ » Γ ⊢ t ≡ rfl ∷ A × Whnf ∇ t × t PE.≢ rfl
  whnf≢rfl ok »∇ =
    let ⊢Id = Idⱼ′ (zeroⱼ (ε »∇)) (zeroⱼ (ε »∇)) in
    ε ∙ Id ℕ zero zero ∙ Id (Id ℕ zero zero) (var x0) rfl ,
    Id ℕ zero zero , var x1 ,
    (equality-reflection′ ok $
     var₀ (Idⱼ′ (var₀ ⊢Id) (rflⱼ (zeroⱼ (∙ ⊢Id))))) ,
    ne (var⁺ _) ,
    (λ ())

opaque

  -- If the WHNF C is judgmentally equal to Quot A B, then there are
  -- A′ and B′ such that C is propositionally equal to Quot A′ B′
  -- (given a certain assumption).

  Quot≡Whnf :
    ⦃ ok : No-equality-reflection or-empty (Γ .vars) ⦄ →
    Γ ⊢ Quot A B ≡ C → Whnf (Γ .defs) C →
    ∃₂ λ A′ B′ → C PE.≡ Quot A′ B′
  Quot≡Whnf Quot≡C C-whnf =
    let _ , _ , _ , _ , C⇒* , _ =
          ⊩Quot≡⇔ .proj₁ (reducible-⊩≡ Quot≡C .proj₂)
    in
    _ , _ , whnfRed* C⇒* C-whnf

opaque

  -- If equality reflection and quotient types are allowed, then there
  -- is a WHNF C that is judgementally equal to Quot A B but not
  -- propositionally equal to any quotient type (if the definition
  -- context is well-formed).

  whnf≢Quot :
    Equality-reflection →
    Quot-allowed →
    » ∇ →
    ∃₄ λ (Γ : Con Term ) A B C →
      ∇ » Γ ⊢ Quot A B ≡ C × Whnf ∇ C ×
      ¬ ∃₂ λ A B → C PE.≡ Quot A B
  whnf≢Quot ok₁ ok₂ »∇ =
    ε ∙ Id U₀ (Quot ℕ ℕ) ℕ , ℕ , ℕ , ℕ ,
    univ
      (equality-reflection′ ok₁ $
       let ⊢ε = ε »∇ in
       var₀ $
       Idⱼ′ (Quot ok₂ (⊢zeroᵘ ⊢ε) (ℕⱼ ⊢ε) (ℕⱼ (⊢Quot-rel-Con (⊢ℕ ⊢ε))))
         (ℕⱼ ⊢ε)) ,
    ℕₙ ,
    (λ ())