module Definition.Untyped.Inversion {a} (M : Set a) where
open import Definition.Untyped M
open import Tools.Fin
open import Tools.Product
open import Tools.PropositionalEquality
private variable
x : Fin _
ρ : Wk _ _
A B t u v w : Term _
p q r : M
s : SigmaMode
b : BinderMode
wk-var :
wk ρ t ≡ var x →
∃ λ x′ → t ≡ var x′ × wkVar ρ x′ ≡ x
wk-var {t = var _} refl = _ , refl , refl
wk-U : wk ρ t ≡ U → t ≡ U
wk-U {t = U} refl = refl
wk-ΠΣ :
wk ρ t ≡ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B →
∃₂ λ A′ B′ →
t ≡ ΠΣ⟨ b ⟩ p , q ▷ A′ ▹ B′ ×
wk ρ A′ ≡ A × wk (lift ρ) B′ ≡ B
wk-ΠΣ {t = ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _} refl =
_ , _ , refl , refl , refl
wk-lam :
wk ρ t ≡ lam p u →
∃ λ u′ → t ≡ lam p u′ × wk (lift ρ) u′ ≡ u
wk-lam {t = lam _ _} refl = _ , refl , refl
wk-∘ :
wk ρ t ≡ u ∘⟨ p ⟩ v →
∃₂ λ u′ v′ → t ≡ u′ ∘⟨ p ⟩ v′ × wk ρ u′ ≡ u × wk ρ v′ ≡ v
wk-∘ {t = _ ∘⟨ _ ⟩ _} refl = _ , _ , refl , refl , refl
wk-prod :
wk ρ t ≡ prod s p u v →
∃₂ λ u′ v′ → t ≡ prod s p u′ v′ × wk ρ u′ ≡ u × wk ρ v′ ≡ v
wk-prod {t = prod _ _ _ _} refl = _ , _ , refl , refl , refl
wk-fst :
wk ρ t ≡ fst p u →
∃ λ u′ → t ≡ fst p u′ × wk ρ u′ ≡ u
wk-fst {t = fst _ _} refl = _ , refl , refl
wk-snd :
wk ρ t ≡ snd p u →
∃ λ u′ → t ≡ snd p u′ × wk ρ u′ ≡ u
wk-snd {t = snd _ _} refl = _ , refl , refl
wk-prodrec :
wk ρ t ≡ prodrec r p q A u v →
∃₃ λ A′ u′ v′ →
t ≡ prodrec r p q A′ u′ v′ ×
wk (lift ρ) A′ ≡ A × wk ρ u′ ≡ u × wk (lift (lift ρ)) v′ ≡ v
wk-prodrec {t = prodrec _ _ _ _ _ _} refl =
_ , _ , _ , refl , refl , refl , refl
wk-Unit : wk ρ t ≡ Unit → t ≡ Unit
wk-Unit {t = Unit} refl = refl
wk-star : wk ρ t ≡ star → t ≡ star
wk-star {t = star} refl = refl
wk-Empty : wk ρ t ≡ Empty → t ≡ Empty
wk-Empty {t = Empty} refl = refl
wk-emptyrec :
wk ρ t ≡ emptyrec p A u →
∃₂ λ A′ u′ → t ≡ emptyrec p A′ u′ × wk ρ A′ ≡ A × wk ρ u′ ≡ u
wk-emptyrec {t = emptyrec _ _ _} refl =
_ , _ , refl , refl , refl
wk-ℕ : wk ρ t ≡ ℕ → t ≡ ℕ
wk-ℕ {t = ℕ} refl = refl
wk-zero : wk ρ t ≡ zero → t ≡ zero
wk-zero {t = zero} refl = refl
wk-suc :
wk ρ t ≡ suc u →
∃ λ u′ → t ≡ suc u′ × wk ρ u′ ≡ u
wk-suc {t = suc _} refl = _ , refl , refl
wk-natrec :
wk ρ t ≡ natrec p q r A u v w →
∃₄ λ A′ u′ v′ w′ →
t ≡ natrec p q r A′ u′ v′ w′ ×
wk (lift ρ) A′ ≡ A ×
wk ρ u′ ≡ u × wk (lift (lift ρ)) v′ ≡ v × wk ρ w′ ≡ w
wk-natrec {t = natrec _ _ _ _ _ _ _} refl =
_ , _ , _ , _ , refl , refl , refl , refl , refl