open import Definition.Typed.Restrictions
open import Graded.Modality
module Definition.Typed.Inversion
{ℓ} {M : Set ℓ}
{𝕄 : Modality M}
(R : Type-restrictions 𝕄)
where
open Type-restrictions R
open import Definition.Typed R
import Definition.Typed.Inversion.Primitive R as I
open import Definition.Typed.Properties.Admissible.Identity.Primitive R
open import Definition.Typed.Properties.Admissible.Level.Primitive R
open import Definition.Typed.Properties.Admissible.U.Primitive R
open import Definition.Typed.Properties.Well-formed R
open import Definition.Typed.Substitution.Primitive R
import Definition.Typed.Weakening R as W
open import Definition.Typed.Well-formed R
open import Definition.Untyped M
open import Definition.Untyped.Allowed-literal R
import Definition.Untyped.Erased 𝕄 as Erased
open import Definition.Untyped.Properties M
open import Definition.Untyped.Quotient 𝕄
open import Definition.Untyped.Sup R
open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.Nat as N
open import Tools.Product as Σ
import Tools.PropositionalEquality as PE
open import Tools.Reasoning.PropositionalEquality
open import Tools.Relation
open import Tools.Sum as ⊎
open I public
private variable
α m n : Nat
x : Fin _
Γ : Cons _ _
A B C D t t₁ t₂ u v w : Term _
l l₁ l₂ : Lvl _
b : BinderMode
s : Strength
p q q′ r : M
opaque
inversion-var : Γ ⊢ var x ∷ A → ∃ λ B → x ∷ B ∈ Γ .vars × Γ ⊢ A ≡ B
inversion-var ⊢x@(var _ x∈) =
_ , x∈ , refl (wf-⊢ ⊢x)
inversion-var (conv ⊢var eq) =
let a , b , c = inversion-var ⊢var in
a , b , trans (sym eq) c
opaque
inversion-defn : Γ ⊢ defn α ∷ A
→ ∃ λ A′ → α ↦∷ A′ ∈ Γ .defs × (Γ ⊢ A ≡ wk wk₀ A′)
inversion-defn (defn {A′ = A} ⊢Γ α↦t PE.refl) =
A , α↦t , refl (W.wk (W.wk₀∷ʷ⊇ ⊢Γ) (wf-↦∈ α↦t (defn-wf ⊢Γ)))
inversion-defn (conv ⊢α eq) =
let A , α↦t , A≡A′ = inversion-defn ⊢α
in A , α↦t , trans (sym eq) A≡A′
opaque
inversion-sucᵘ :
Γ ⊢ sucᵘ t ∷ A →
Γ ⊢ t ∷ Level × Γ ⊢ A ≡ Level
inversion-sucᵘ (sucᵘⱼ ⊢t) =
let ok = inversion-Level-⊢ (wf-⊢ ⊢t) in
⊢t , refl (Levelⱼ′ ok (wf ⊢t))
inversion-sucᵘ (conv ⊢sucᵘ eq) =
let ⊢t , A≡ = inversion-sucᵘ ⊢sucᵘ in
⊢t , trans (sym eq) A≡
opaque
inversion-sucᵘ-⊢ :
Γ ⊢ sucᵘ t →
Γ ⊢ t ∷ Level × ∃ λ l → Γ ⊢ U l ≡ Level
inversion-sucᵘ-⊢ (univ ⊢sucᵘ) =
let ⊢t , U≡Level = inversion-sucᵘ ⊢sucᵘ in
⊢t , _ , U≡Level
opaque
inversion-1ᵘ+-⊢∷L :
Γ ⊢ 1ᵘ+ l ∷Level →
Γ ⊢ l ∷Level
inversion-1ᵘ+-⊢∷L {l = level _} (term ok ⊢sucᵘ) =
term ok (inversion-sucᵘ ⊢sucᵘ .proj₁)
inversion-1ᵘ+-⊢∷L {l = level _} (literal ok ⊢Γ) =
literal
(Allowed-literal-level-⇔ .proj₂ $
Σ.map (Level-literal-1ᵘ+-⇔ .proj₁) idᶠ $
Allowed-literal-level-⇔ .proj₁ ok)
⊢Γ
inversion-1ᵘ+-⊢∷L {l = ωᵘ+ _} (literal ok ⊢Γ) =
literal
(Allowed-literal-ωᵘ+-⇔ .proj₂ $
Allowed-literal-ωᵘ+-⇔ .proj₁ ok)
⊢Γ
opaque
inversion-1ᵘ+ⁿ : ∀ n → Γ ⊢ 1ᵘ+ⁿ n l ∷Level → Γ ⊢ l ∷Level
inversion-1ᵘ+ⁿ 0 = idᶠ
inversion-1ᵘ+ⁿ (1+ n) = inversion-1ᵘ+ⁿ n ∘→ inversion-1ᵘ+-⊢∷L
opaque
unfolding ↓ᵘ_
inversion-↓ᵘ : Γ ⊢ ↓ᵘ n ∷ A → Γ ⊢ A ≡ Level
inversion-↓ᵘ {n = 0} = inversion-zeroᵘ
inversion-↓ᵘ {n = 1+ _} = proj₂ ∘→ inversion-sucᵘ
opaque
unfolding ↓ᵘ_
inversion-↓ᵘ-⊢ : Γ ⊢ (↓ᵘ n) → ∃ λ l → Γ ⊢ U l ≡ Level
inversion-↓ᵘ-⊢ {n = 0} = inversion-zeroᵘ-⊢
inversion-↓ᵘ-⊢ {n = 1+ _} = proj₂ ∘→ inversion-sucᵘ-⊢
opaque
inversion-supᵘ :
Γ ⊢ t₁ supᵘ t₂ ∷ A →
Γ ⊢ t₁ ∷ Level × Γ ⊢ t₂ ∷ Level × Γ ⊢ A ≡ Level
inversion-supᵘ (supᵘⱼ ⊢t₁ ⊢t₂) =
let ok = inversion-Level-⊢ (wf-⊢ ⊢t₁) in
⊢t₁ , ⊢t₂ , refl (Levelⱼ′ ok (wf ⊢t₁))
inversion-supᵘ (conv ⊢supᵘ eq) =
let ⊢t₁ , ⊢t₂ , A≡ = inversion-supᵘ ⊢supᵘ in
⊢t₁ , ⊢t₂ , trans (sym eq) A≡
opaque
inversion-supᵘ-⊢ :
Γ ⊢ t₁ supᵘ t₂ →
Γ ⊢ t₁ ∷ Level × Γ ⊢ t₂ ∷ Level × ∃ λ l → Γ ⊢ U l ≡ Level
inversion-supᵘ-⊢ (univ eq) =
let ⊢t₁ , ⊢t₂ , U≡Level = inversion-supᵘ eq in
⊢t₁ , ⊢t₂ , _ , U≡Level
opaque
unfolding _supᵘₗ′_
inversion-supᵘₗ′-⊢∷ :
Γ ⊢ t₁ supᵘₗ′ t₂ ∷ A →
Γ ⊢ t₁ ∷ Level × Γ ⊢ t₂ ∷ Level × Γ ⊢ A ≡ Level
inversion-supᵘₗ′-⊢∷ {t₁} {t₂} ⊢sup
with Level-literal? t₁ ×-dec Level-literal? t₂
… | no _ =
inversion-supᵘ ⊢sup
… | yes (t₁-lit , t₂-lit) =
let ≡Level = inversion-↓ᵘ ⊢sup
ok = inversion-Level-⊢ (wf-⊢ ≡Level .proj₂)
⊢Γ = wf ≡Level
in
⊢∷Level→⊢∷Level ok (Level-literal→⊢∷L ⊢Γ (level t₁-lit) (λ ())) ,
⊢∷Level→⊢∷Level ok (Level-literal→⊢∷L ⊢Γ (level t₂-lit) (λ ())) ,
≡Level
opaque
unfolding _supᵘₗ_
inversion-supᵘₗ-⊢∷ :
Γ ⊢ t₁ supᵘₗ t₂ ∷ A →
Γ ⊢ t₁ ∷ Level × Γ ⊢ t₂ ∷ Level × Γ ⊢ A ≡ Level
inversion-supᵘₗ-⊢∷ ⊢sup with level-support
… | only-literals = inversion-supᵘₗ′-⊢∷ ⊢sup
… | level-type _ = inversion-supᵘ ⊢sup
opaque
inversion-supᵘₗ-⊢ :
Γ ⊢ t₁ supᵘₗ t₂ →
Γ ⊢ t₁ ∷ Level × Γ ⊢ t₂ ∷ Level × (∃ λ l → Γ ⊢ U l ≡ Level)
inversion-supᵘₗ-⊢ ⊢sup = inversion-supᵘₗ-⊢′ ⊢sup PE.refl
where
inversion-supᵘₗ-⊢′ :
Γ ⊢ A → t₁ supᵘₗ t₂ PE.≡ A →
Γ ⊢ t₁ ∷ Level × Γ ⊢ t₂ ∷ Level × (∃ λ l → Γ ⊢ U l ≡ Level)
inversion-supᵘₗ-⊢′ (Levelⱼ _ _) eq =
⊥-elim (supᵘₗ≢Level eq)
inversion-supᵘₗ-⊢′ (univ ⊢sup) PE.refl =
let ⊢t₁ , ⊢t₂ , ≡Level = inversion-supᵘₗ-⊢∷ ⊢sup in
⊢t₁ , ⊢t₂ , _ , ≡Level
inversion-supᵘₗ-⊢′ (Liftⱼ _ _) eq =
⊥-elim (supᵘₗ≢Lift eq)
inversion-supᵘₗ-⊢′ (ΠΣⱼ _ _) eq =
⊥-elim (supᵘₗ≢ΠΣ eq)
inversion-supᵘₗ-⊢′ (Idⱼ _ _ _) eq =
⊥-elim (supᵘₗ≢Id eq)
inversion-supᵘₗ-⊢′ (Quot _ _) eq =
⊥-elim (supᵘₗ≢Quot eq)
opaque
unfolding _supᵘₗ_
inversion-supᵘₗ-level :
Γ ⊢ level (t₁ supᵘₗ t₂) ∷Level →
Γ ⊢ level t₁ ∷Level × Γ ⊢ level t₂ ∷Level
inversion-supᵘₗ-level {t₁} {t₂} (term {t} ok ⊢t) =
let ⊢t₁ , ⊢t₂ , _ =
inversion-supᵘ $
PE.subst (flip (_⊢_∷_ _) _)
(level-PE-injectivity
(level t ≡⟨⟩
level t₁ supᵘₗ level t₂ ≡⟨ supᵘₗ≡supᵘ ok ⟩
level (t₁ supᵘ t₂) ∎))
⊢t
in
term ok ⊢t₁ , term ok ⊢t₂
inversion-supᵘₗ-level (literal ok ⊢Γ) =
let not-ok , t₁-lit , t₂-lit =
Level-literal-supᵘₗ-level-→ (Allowed-literal→Level-literal ok)
in
literal (Allowed-literal-level-⇔ .proj₂ (t₁-lit , not-ok)) ⊢Γ ,
literal (Allowed-literal-level-⇔ .proj₂ (t₂-lit , not-ok)) ⊢Γ
opaque
unfolding _supᵘₗ_
inversion-supᵘₗ :
Γ ⊢ l₁ supᵘₗ l₂ ∷Level →
l₁ supᵘₗ l₂ PE.≡ l₁ × Γ ⊢ l₁ ∷Level ⊎
l₁ supᵘₗ l₂ PE.≡ l₂ × Γ ⊢ l₂ ∷Level ⊎
Γ ⊢ l₁ ∷Level × Γ ⊢ l₂ ∷Level
inversion-supᵘₗ {l₁ = ωᵘ+ m₁} {l₂ = ωᵘ+ m₂} ⊢⊔ with N.≤-total m₁ m₂
… | inj₁ m₁≤m₂ =
let eq = PE.cong ωᵘ+ (m≤n⇒m⊔n≡n m₁≤m₂) in
inj₂ (inj₁ (eq , PE.subst (_⊢_∷Level _) eq ⊢⊔))
… | inj₂ m₂≤m₁ =
let eq = PE.cong ωᵘ+ (m≥n⇒m⊔n≡m m₂≤m₁) in
inj₁ (eq , PE.subst (_⊢_∷Level _) eq ⊢⊔)
inversion-supᵘₗ {l₁ = ωᵘ+ _} {l₂ = level _} ⊢⊔ =
inj₁ (PE.refl , ⊢⊔)
inversion-supᵘₗ {l₁ = level _} {l₂ = ωᵘ+ _} ⊢⊔ =
inj₂ (inj₁ (PE.refl , ⊢⊔))
inversion-supᵘₗ {l₁ = level _} {l₂ = level _} ⊢⊔ =
inj₂ (inj₂ (inversion-supᵘₗ-level ⊢⊔))
opaque
inversion-ωᵘ+ :
Γ ⊢ ωᵘ+ m ∷Level →
Omega-plus-allowed × ⊢ Γ
inversion-ωᵘ+ (literal ok ⊢Γ) =
Allowed-literal-ωᵘ+-⇔ .proj₁ ok , ⊢Γ
opaque
inversion-level :
Γ ⊢ level t ∷Level →
Level-allowed × Γ ⊢ t ∷ Level ⊎
¬ Level-allowed × Level-literal t × ⊢ Γ
inversion-level (term ok ⊢t) =
inj₁ (ok , ⊢t)
inversion-level (literal ok ⊢Γ) =
let not-ok , lit = Allowed-literal-level-⇔ .proj₁ ok in
inj₂ (lit , not-ok , ⊢Γ)
opaque
inversion-lower : Γ ⊢ lower t ∷ A → ∃₂ λ l B → Γ ⊢ t ∷ Lift l B × Γ ⊢ A ≡ B
inversion-lower (conv x x₁) =
let _ , _ , ⊢t , A≡B = inversion-lower x
in _ , _ , ⊢t , trans (sym x₁) A≡B
inversion-lower (lowerⱼ x) = _ , _ , x , refl (inversion-Lift (wf-⊢ x) .proj₂)
opaque
⊢∷Unit→Unit-allowed : Γ ⊢ t ∷ Unit s → Unit-allowed s
⊢∷Unit→Unit-allowed {Γ} {t} {s} =
Γ ⊢ t ∷ Unit s →⟨ wf-⊢ ⟩
Γ ⊢ Unit s →⟨ inversion-Unit ⟩
Unit-allowed s □
opaque
inversion-unitrec :
Γ ⊢ unitrec p q A t u ∷ B →
(Γ »∙ Unitʷ ⊢ A) ×
Γ ⊢ t ∷ Unitʷ ×
Γ ⊢ u ∷ A [ starʷ ]₀ ×
Γ ⊢ B ≡ A [ t ]₀
inversion-unitrec (unitrecⱼ ⊢A ⊢t ⊢u) =
⊢A , ⊢t , ⊢u , refl (subst-⊢₀ ⊢A ⊢t)
inversion-unitrec (conv ⊢ur eq) =
let a , b , c , d = inversion-unitrec ⊢ur
in a , b , c , trans (sym eq) d
opaque
⊢∷ΠΣ→ΠΣ-allowed :
Γ ⊢ t ∷ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B → ΠΣ-allowed b p q
⊢∷ΠΣ→ΠΣ-allowed {Γ} {t} {b} {p} {q} {A} {B} =
Γ ⊢ t ∷ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B →⟨ wf-⊢ ⟩
Γ ⊢ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B →⟨ proj₂ ∘→ proj₂ ∘→ inversion-ΠΣ ⟩
ΠΣ-allowed b p q □
opaque
inversion-lam :
Γ ⊢ lam p t ∷ A →
∃₃ λ B C q →
(Γ ⊢ B) × Γ »∙ B ⊢ t ∷ C ×
Γ ⊢ A ≡ Π p , q ▷ B ▹ C ×
Π-allowed p q
inversion-lam (lamⱼ _ ⊢t ok) =
let ⊢B = wf-⊢ ⊢t in
_ , _ , _ , ⊢∙→⊢ (wf ⊢B) , ⊢t , refl (ΠΣⱼ ⊢B ok) , ok
inversion-lam (conv ⊢lam eq) =
let a , b , c , d , e , f , g = inversion-lam ⊢lam in
a , b , c , d , e , trans (sym eq) f , g
opaque
inversion-app :
Γ ⊢ t ∘⟨ p ⟩ u ∷ A →
∃₃ λ B C q → Γ ⊢ t ∷ Π p , q ▷ B ▹ C × Γ ⊢ u ∷ B × Γ ⊢ A ≡ C [ u ]₀
inversion-app (⊢t ∘ⱼ ⊢u) =
_ , _ , _ , ⊢t , ⊢u , refl (substTypeΠ (wf-⊢ ⊢t) ⊢u)
inversion-app (conv ⊢app eq) =
let a , b , c , d , e , f = inversion-app ⊢app in
a , b , c , d , e , trans (sym eq) f
opaque
inversion-snd :
Γ ⊢ snd p t ∷ A →
∃₃ λ B C q →
(Γ ⊢ B) × (Γ »∙ B ⊢ C) ×
Γ ⊢ t ∷ Σˢ p , q ▷ B ▹ C ×
Γ ⊢ A ≡ C [ fst p t ]₀
inversion-snd (sndⱼ ⊢C ⊢t) =
_ , _ , _ , ⊢∙→⊢ (wf ⊢C) , ⊢C , ⊢t ,
refl (subst-⊢₀ ⊢C (fstⱼ ⊢C ⊢t))
inversion-snd (conv ⊢snd eq) =
let a , b , c , d , e , f , g = inversion-snd ⊢snd in
a , b , c , d , e , f , trans (sym eq) g
opaque
inversion-prodrec :
Γ ⊢ prodrec r p q′ A t u ∷ B →
∃₃ λ C D q →
(Γ ⊢ C) × (Γ »∙ C ⊢ D) ×
(Γ »∙ Σʷ p , q ▷ C ▹ D ⊢ A) ×
Γ ⊢ t ∷ Σʷ p , q ▷ C ▹ D ×
Γ »∙ C »∙ D ⊢ u ∷ A [ prodʷ p (var x1) (var x0) ]↑² ×
Γ ⊢ B ≡ A [ t ]₀
inversion-prodrec (prodrecⱼ ⊢A ⊢t ⊢u) =
let ⊢D = ⊢∙→⊢ (wf ⊢u) in
_ , _ , _ , ⊢∙→⊢ (wf ⊢D) , ⊢D , ⊢A , ⊢t , ⊢u ,
refl (subst-⊢₀ ⊢A ⊢t)
inversion-prodrec (conv ⊢pr eq) =
let a , b , c , d , e , f , g , h , i = inversion-prodrec ⊢pr in
a , b , c , d , e , f , g , h , trans (sym eq) i
opaque
inversion-natrec :
Γ ⊢ natrec p q r A t u v ∷ B →
(Γ »∙ ℕ ⊢ A) ×
Γ ⊢ t ∷ A [ zero ]₀ ×
Γ »∙ ℕ »∙ A ⊢ u ∷ A [ suc (var x1) ]↑² ×
Γ ⊢ v ∷ ℕ ×
Γ ⊢ B ≡ A [ v ]₀
inversion-natrec (natrecⱼ ⊢t ⊢u ⊢v) =
let ⊢A = ⊢∙→⊢ (wf ⊢u) in
⊢A , ⊢t , ⊢u , ⊢v , refl (subst-⊢₀ ⊢A ⊢v)
inversion-natrec (conv ⊢nr eq) =
let a , b , c , d , e = inversion-natrec ⊢nr in
a , b , c , d , trans (sym eq) e
opaque
inversion-Id-U :
Γ ⊢ Id A t u ∷ B →
∃ λ l → Γ ⊢ A ∷ U l × Γ ⊢ t ∷ A × Γ ⊢ u ∷ A × Γ ⊢ B ≡ U l
inversion-Id-U = λ where
(Idⱼ ⊢A ⊢t ⊢u) →
_ , ⊢A , ⊢t , ⊢u ,
refl (⊢U (inversion-U-Level (wf-⊢ ⊢A)))
(conv ⊢Id C≡B) →
case inversion-Id-U ⊢Id of λ {
(_ , ⊢A , ⊢t , ⊢u , C≡U) →
_ , ⊢A , ⊢t , ⊢u , trans (sym C≡B) C≡U }
opaque
inversion-Id∷U :
Γ ⊢ Id A t u ∷ U l →
Γ ⊢ A ∷ U l × Γ ⊢ t ∷ A × Γ ⊢ u ∷ A
inversion-Id∷U ⊢Id =
let _ , ⊢A , ⊢t , ⊢u , ≡U = inversion-Id-U ⊢Id in
conv ⊢A (sym ≡U) , ⊢t , ⊢u
opaque
inversion-rfl :
Γ ⊢ rfl ∷ A →
∃₂ λ B t → (Γ ⊢ B) × Γ ⊢ t ∷ B × Γ ⊢ A ≡ Id B t t
inversion-rfl = λ where
⊢rfl@(rflⱼ ⊢t) →
_ , _ , wf-⊢ ⊢t , ⊢t , refl (wf-⊢ ⊢rfl)
(conv ⊢rfl eq) →
let a , b , c , d , e = inversion-rfl ⊢rfl in
a , b , c , d , trans (sym eq) e
opaque
inversion-J :
Γ ⊢ J p q A t B u v w ∷ C →
(Γ ⊢ A) ×
Γ ⊢ t ∷ A ×
(Γ »∙ A »∙ Id (wk1 A) (wk1 t) (var x0) ⊢ B) ×
Γ ⊢ u ∷ B [ t , rfl ]₁₀ ×
Γ ⊢ v ∷ A ×
Γ ⊢ w ∷ Id A t v ×
Γ ⊢ C ≡ B [ v , w ]₁₀
inversion-J = λ where
⊢J@(Jⱼ ⊢t ⊢B ⊢u ⊢v ⊢w) →
⊢∙→⊢ (wf (⊢∙→⊢ (wf ⊢B))) , ⊢t , ⊢B , ⊢u , ⊢v , ⊢w ,
refl (wf-⊢ ⊢J)
(conv ⊢J eq) →
let a , b , c , d , e , f , g = inversion-J ⊢J in
a , b , c , d , e , f , trans (sym eq) g
opaque
inversion-K :
Γ ⊢ K p A t B u v ∷ C →
(Γ ⊢ A) ×
Γ ⊢ t ∷ A ×
(Γ »∙ Id A t t ⊢ B) ×
Γ ⊢ u ∷ B [ rfl ]₀ ×
Γ ⊢ v ∷ Id A t t ×
K-allowed ×
Γ ⊢ C ≡ B [ v ]₀
inversion-K = λ where
⊢K@(Kⱼ ⊢B ⊢u ⊢v ok) →
let ⊢A , ⊢t , _ = inversion-Id (⊢∙→⊢ (wf ⊢B)) in
⊢A , ⊢t , ⊢B , ⊢u , ⊢v , ok
, refl (wf-⊢ ⊢K)
(conv ⊢K eq) →
let a , b , c , d , e , f , g = inversion-K ⊢K in
a , b , c , d , e , f , trans (sym eq) g
opaque
inversion-[]-cong :
Γ ⊢ []-cong s l A t u v ∷ B →
let open Erased s in
Γ ⊢ l ∷Level ×
(Γ ⊢ A) ×
Γ ⊢ t ∷ A ×
Γ ⊢ u ∷ A ×
Γ ⊢ v ∷ Id A t u ×
[]-cong-allowed s ×
Γ ⊢ B ≡ Id (Erased l A) ([ t ]) ([ u ])
inversion-[]-cong = λ where
⊢[]-cong@([]-congⱼ ⊢l ⊢A ⊢t ⊢u ⊢v ok) →
⊢l , ⊢A , ⊢t , ⊢u , ⊢v , ok
, refl (wf-⊢ ⊢[]-cong)
(conv ⊢bc eq) →
let a , b , c , d , e , f , g = inversion-[]-cong ⊢bc in
a , b , c , d , e , f , trans (sym eq) g
opaque
inversion-class :
Γ ⊢ class t ∷ A →
∃₂ λ B C →
(Γ ⊢ Quot B C) ×
Γ ⊢ t ∷ B ×
Γ ⊢ A ≡ Quot B C
inversion-class (class ⊢Q ⊢t) =
_ , _ , ⊢Q , ⊢t , refl ⊢Q
inversion-class (conv ⊢c ≡A) =
let _ , _ , ⊢Q , ⊢t , ≡Q = inversion-class ⊢c in
_ , _ , ⊢Q , ⊢t , trans (sym ≡A) ≡Q
opaque
inversion-resp :
Γ ⊢ resp A B t u v ∷ C →
(Γ ⊢ Quot A B) ×
Γ ⊢ t ∷ A ×
Γ ⊢ u ∷ A ×
Γ ⊢ v ∷ B [ t , u ]₁₀ ×
Γ ⊢ C ≡ Id (Quot A B) (class t) (class u)
inversion-resp (resp ⊢Q ⊢t ⊢u ⊢v) =
⊢Q , ⊢t , ⊢u , ⊢v ,
refl (Idⱼ′ (class ⊢Q ⊢t) (class ⊢Q ⊢u))
inversion-resp (conv ⊢r ≡C) =
let ⊢Q , ⊢t , ⊢u , ⊢v , ≡Id = inversion-resp ⊢r in
⊢Q , ⊢t , ⊢u , ⊢v , trans (sym ≡C) ≡Id
opaque
inversion-set :
Γ ⊢ set A B t u v w ∷ C →
(Γ ⊢ Quot A B) ×
Γ ⊢ t ∷ Quot A B ×
Γ ⊢ u ∷ Quot A B ×
Γ ⊢ v ∷ Id (Quot A B) t u ×
Γ ⊢ w ∷ Id (Quot A B) t u ×
Γ ⊢ C ≡ Id (Id (Quot A B) t u) v w
inversion-set (set ⊢Q ⊢t ⊢u ⊢v ⊢w) =
⊢Q , ⊢t , ⊢u , ⊢v , ⊢w , refl (Idⱼ′ ⊢v ⊢w)
inversion-set (conv ⊢s ≡C) =
let ⊢Q , ⊢t , ⊢u , ⊢v , ⊢w , ≡Id = inversion-set ⊢s in
⊢Q , ⊢t , ⊢u , ⊢v , ⊢w , trans (sym ≡C) ≡Id
opaque
inversion-qrec :
Γ ⊢ qrec C t u v w ∷ D →
∃₂ λ A B →
(Γ »∙ Quot A B ⊢ C) ×
Γ »∙ A ⊢ t ∷ C [ class (var x0) ]↑ ×
Resp-Cons Γ A B ⊢ u ∷ Resp-type A B C t ×
Is-set-Cons Γ A B C ⊢ v ∷ Is-set-type C ×
Γ ⊢ w ∷ Quot A B ×
Γ ⊢ D ≡ C [ w ]₀
inversion-qrec (qrec ⊢C ⊢t ⊢u ⊢v ⊢w) =
_ , _ , ⊢C , ⊢t , ⊢u , ⊢v , ⊢w , refl (subst-⊢₀ ⊢C ⊢w)
inversion-qrec (conv ⊢q ≡D) =
let _ , _ , ⊢C , ⊢t , ⊢u , ⊢v , ⊢w , ≡[]₀ = inversion-qrec ⊢q in
_ , _ , ⊢C , ⊢t , ⊢u , ⊢v , ⊢w , trans (sym ≡D) ≡[]₀