open import Definition.Typed.Restrictions
module Definition.Conversion.EqRelInstance
{a} {M : Set a}
(R : Type-restrictions M)
where
open import Definition.Untyped M hiding (_∷_)
open import Definition.Typed R
open import Definition.Typed.Properties R
open import Definition.Typed.Weakening R using (_∷_⊇_; wkEq)
open import Definition.Conversion R
open import Definition.Conversion.Reduction R
open import Definition.Conversion.Universe R
open import Definition.Conversion.Stability R
open import Definition.Conversion.Soundness R
open import Definition.Conversion.Lift R
open import Definition.Conversion.Conversion R
open import Definition.Conversion.Symmetry R
open import Definition.Conversion.Transitivity R
open import Definition.Conversion.Weakening R
open import Definition.Typed.EqualityRelation R
open import Definition.Typed.Consequences.Syntactic R
open import Definition.Typed.Consequences.Substitution R
open import Definition.Typed.Consequences.Stability R
open import Definition.Typed.Consequences.Injectivity R
open import Definition.Typed.Consequences.Equality R
open import Definition.Typed.Consequences.Reduction R
open import Tools.Fin
open import Tools.Function
open import Tools.Nat
open import Tools.Product
open import Tools.Function
import Tools.PropositionalEquality as PE
private
variable
m n : Nat
Γ : Con Term n
ρ : Wk m n
p p₁ p₂ p′ q q′ q₁ q₂ r r′ : M
record _⊢_~_∷_ (Γ : Con Term n) (k l A : Term n) : Set a where
inductive
constructor ↑
field
{B} : Term n
A≡B : Γ ⊢ A ≡ B
k~↑l : Γ ⊢ k ~ l ↑ B
~-var : ∀ {x A} → Γ ⊢ var x ∷ A → Γ ⊢ var x ~ var x ∷ A
~-var x =
let ⊢A = syntacticTerm x
in ↑ (refl ⊢A) (var-refl x PE.refl)
~-app : ∀ {f g a b F G}
→ Γ ⊢ f ~ g ∷ Π p , q ▷ F ▹ G
→ Γ ⊢ a [conv↑] b ∷ F
→ Γ ⊢ f ∘⟨ p ⟩ a ~ g ∘⟨ p ⟩ b ∷ G [ a ]₀
~-app (↑ A≡B x) x₁ =
let _ , ⊢B = syntacticEq A≡B
B′ , whnfB′ , D = whNorm ⊢B
ΠFG≡B′ = trans A≡B (subset* (red D))
_ , ⊢f , _ = syntacticEqTerm (soundnessConv↑Term x₁)
in
case Π≡A ΠFG≡B′ whnfB′ of λ {
(H , E , B≡ΠHE) →
case injectivity (PE.subst (λ x → _ ⊢ _ ≡ x) B≡ΠHE ΠFG≡B′) of λ {
(F≡H , G≡E , _ , _) →
↑ (substTypeEq G≡E (refl ⊢f))
(app-cong
(PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡ΠHE
([~] _ (red D) whnfB′ x))
(convConvTerm x₁ F≡H)) }}
~-fst :
∀ {p r F G} →
Γ ⊢ p ~ r ∷ Σₚ p′ , q ▷ F ▹ G →
Γ ⊢ fst p′ p ~ fst p′ r ∷ F
~-fst (↑ A≡B p~r) =
case syntacticEq A≡B of λ (_ , ⊢B) →
case whNorm ⊢B of λ (B′ , whnfB′ , D) →
case trans A≡B (subset* (red D)) of λ ΣFG≡B′ →
case Σ≡A ΣFG≡B′ whnfB′ of λ where
(H , _ , PE.refl) →
case Σ-injectivity ΣFG≡B′ of λ where
(F≡H , _ , _ , _) →
↑ F≡H (fst-cong ([~] _ (red D) whnfB′ p~r))
~-snd :
∀ {p r F G} →
Γ ⊢ p ~ r ∷ Σ p′ , q ▷ F ▹ G →
Γ ⊢ snd p′ p ~ snd p′ r ∷ G [ fst p′ p ]₀
~-snd (↑ A≡B p~r) =
case syntacticEq A≡B of λ (⊢ΣFG , ⊢B) →
case whNorm ⊢B of λ (B′ , whnfB′ , D) →
case trans A≡B (subset* (red D)) of λ ΣFG≡B′ →
case Σ≡A ΣFG≡B′ whnfB′ of λ where
(_ , E , PE.refl) →
case Σ-injectivity ΣFG≡B′ of λ where
(_ , G≡E , _ , _) →
let p~r↓ = [~] _ (red D) whnfB′ p~r
⊢F , ⊢G = syntacticΣ ⊢ΣFG
_ , ⊢p , _ = syntacticEqTerm (soundness~↑ p~r)
⊢fst = fstⱼ ⊢F ⊢G (conv ⊢p (sym A≡B))
in
↑ (substTypeEq G≡E (refl ⊢fst)) (snd-cong p~r↓)
~-natrec : ∀ {z z′ s s′ n n′ F F′}
→ Γ ∙ ℕ ⊢ F
→ (Γ ∙ ℕ) ⊢ F [conv↑] F′ →
Γ ⊢ z [conv↑] z′ ∷ (F [ zero ]₀) →
Γ ∙ ℕ ∙ F ⊢ s [conv↑] s′ ∷ F [ suc (var x1) ]↑² →
Γ ⊢ n ~ n′ ∷ ℕ →
Γ ⊢ natrec p q r F z s n ~ natrec p q r F′ z′ s′ n′ ∷ (F [ n ]₀)
~-natrec _ x x₁ x₂ (↑ A≡B x₄) =
let _ , ⊢B = syntacticEq A≡B
B′ , whnfB′ , D = whNorm ⊢B
ℕ≡B′ = trans A≡B (subset* (red D))
B≡ℕ = ℕ≡A ℕ≡B′ whnfB′
k~l′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡ℕ
([~] _ (red D) whnfB′ x₄)
⊢F , _ = syntacticEq (soundnessConv↑ x)
_ , ⊢n , _ = syntacticEqTerm (soundness~↓ k~l′)
in ↑ (refl (substType ⊢F ⊢n))
(natrec-cong x x₁ x₂ k~l′)
~-prodrec :
∀ {F G A A′ t t′ u u′} →
Γ ⊢ F →
Γ ∙ F ⊢ G →
Γ ∙ (Σᵣ p , q ▷ F ▹ G) ⊢ A [conv↑] A′ →
Γ ⊢ t ~ t′ ∷ (Σᵣ p , q ▷ F ▹ G) →
Γ ∙ F ∙ G ⊢ u [conv↑] u′ ∷ A [ prodᵣ p (var x1) (var x0) ]↑² →
Γ ⊢ prodrec r p q′ A t u ~ prodrec r p q′ A′ t′ u′ ∷ (A [ t ]₀)
~-prodrec x x₁ x₂ (↑ A≡B k~↑l) x₄ =
case syntacticEq A≡B of λ (_ , ⊢B) →
case whNorm ⊢B of λ (B′ , whnfB′ , D) →
case _⊢_≡_.trans A≡B (subset* (red D)) of λ Σ≡Σ′ →
case Σ≡A (trans A≡B (subset* (red D))) whnfB′ of λ where
(F′ , G′ , PE.refl) →
case Σ-injectivity Σ≡Σ′ of λ where
(F≡F′ , G≡G′ , _ , _ , _) →
let t~t′ = [~] _ (red D) whnfB′ k~↑l
⊢Γ = wf ⊢B
⊢Γ≡Γ = reflConEq ⊢Γ
⊢A , _ = syntacticEq (soundnessConv↑ x₂)
_ , ⊢t , _ = syntacticEqTerm (soundness~↑ k~↑l)
in
↑ (refl (substType ⊢A (conv ⊢t (sym A≡B))))
(prodrec-cong (stabilityConv↑ (⊢Γ≡Γ ∙ Σ≡Σ′) x₂)
t~t′ (stabilityConv↑Term (⊢Γ≡Γ ∙ F≡F′ ∙ G≡G′) x₄))
~-emptyrec : ∀ {n n′ F F′}
→ Γ ⊢ F [conv↑] F′ →
Γ ⊢ n ~ n′ ∷ Empty →
Γ ⊢ emptyrec p F n ~ emptyrec p F′ n′ ∷ F
~-emptyrec x (↑ A≡B x₄) =
let _ , ⊢B = syntacticEq A≡B
B′ , whnfB′ , D = whNorm ⊢B
Empty≡B′ = trans A≡B (subset* (red D))
B≡Empty = Empty≡A Empty≡B′ whnfB′
k~l′ = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡Empty
([~] _ (red D) whnfB′ x₄)
⊢F , _ = syntacticEq (soundnessConv↑ x)
_ , ⊢n , _ = syntacticEqTerm (soundness~↓ k~l′)
in ↑ (refl ⊢F)
(emptyrec-cong x k~l′)
~-sym : ∀ {k l A} → Γ ⊢ k ~ l ∷ A → Γ ⊢ l ~ k ∷ A
~-sym (↑ A≡B x) =
let ⊢Γ = wfEq A≡B
B , A≡B′ , l~k = sym~↑ (reflConEq ⊢Γ) x
in ↑ (trans A≡B A≡B′) l~k
~-trans : ∀ {k l m A}
→ Γ ⊢ k ~ l ∷ A → Γ ⊢ l ~ m ∷ A
→ Γ ⊢ k ~ m ∷ A
~-trans (↑ x x₁) (↑ x₂ x₃) =
let ⊢Γ = wfEq x
k~m , _ = trans~↑ x₁ x₃
in ↑ x k~m
~-wk : ∀ {k l A} {ρ : Wk m n} {Γ Δ} →
ρ ∷ Δ ⊇ Γ →
⊢ Δ → Γ ⊢ k ~ l ∷ A → Δ ⊢ wk ρ k ~ wk ρ l ∷ wk ρ A
~-wk x x₁ (↑ x₂ x₃) = ↑ (wkEq x x₁ x₂) (wk~↑ x x₁ x₃)
~-conv : ∀ {k l A B} →
Γ ⊢ k ~ l ∷ A → Γ ⊢ A ≡ B → Γ ⊢ k ~ l ∷ B
~-conv (↑ x x₁) x₂ = ↑ (trans (sym x₂) x) x₁
~-to-conv : ∀ {k l A} →
Γ ⊢ k ~ l ∷ A → Γ ⊢ k [conv↑] l ∷ A
~-to-conv (↑ x x₁) = convConvTerm (lift~toConv↑ x₁) (sym x)
instance eqRelInstance : EqRelSet
eqRelInstance = record {
_⊢_≅_ = _⊢_[conv↑]_;
_⊢_≅_∷_ = _⊢_[conv↑]_∷_;
_⊢_~_∷_ = _⊢_~_∷_;
~-to-≅ₜ = ~-to-conv;
≅-eq = soundnessConv↑;
≅ₜ-eq = soundnessConv↑Term;
≅-univ = univConv↑;
≅-sym = symConv;
≅ₜ-sym = symConvTerm;
~-sym = ~-sym;
≅-trans = transConv;
≅ₜ-trans = transConvTerm;
~-trans = ~-trans;
≅-conv = convConvTerm;
~-conv = ~-conv;
≅-wk = wkConv↑;
≅ₜ-wk = wkConv↑Term;
~-wk = ~-wk;
≅-red = λ x x₁ x₂ x₃ x₄ → reductionConv↑ x x₁ x₄;
≅ₜ-red = λ x x₁ x₂ x₃ x₄ x₅ x₆ → reductionConv↑Term x x₁ x₂ x₆;
≅-Urefl = liftConv ∘ᶠ U-refl;
≅-ℕrefl = liftConv ∘ᶠ ℕ-refl;
≅ₜ-ℕrefl = λ x → liftConvTerm (univ (ℕⱼ x) (ℕⱼ x) (ℕ-refl x));
≅-Emptyrefl = liftConv ∘ᶠ Empty-refl;
≅ₜ-Emptyrefl = λ x → liftConvTerm (univ (Emptyⱼ x) (Emptyⱼ x) (Empty-refl x));
≅-Unitrefl = λ ⊢Γ → liftConv ∘→ Unit-refl ⊢Γ;
≅ₜ-Unitrefl = λ ⊢Γ ok →
liftConvTerm $
univ (Unitⱼ ⊢Γ ok) (Unitⱼ ⊢Γ ok) (Unit-refl ⊢Γ ok);
≅ₜ-η-unit = λ [e] [e'] → let u , uWhnf , uRed = whNormTerm [e]
u' , u'Whnf , u'Red = whNormTerm [e']
[u] = ⊢u-redₜ uRed
[u'] = ⊢u-redₜ u'Red
in [↑]ₜ Unit u u'
(red (idRed:*: (syntacticTerm [e])))
(redₜ uRed)
(redₜ u'Red)
Unitₙ uWhnf u'Whnf
(η-unit [u] [u'] uWhnf u'Whnf);
≅-ΠΣ-cong = λ x x₁ x₂ ok → liftConv (ΠΣ-cong x x₁ x₂ ok);
≅ₜ-ΠΣ-cong = λ x x₁ x₂ ok →
let _ , F∷U , H∷U = syntacticEqTerm (soundnessConv↑Term x₁)
_ , G∷U , E∷U = syntacticEqTerm (soundnessConv↑Term x₂)
⊢Γ = wfTerm F∷U
F<>H = univConv↑ x₁
G<>E = univConv↑ x₂
F≡H = soundnessConv↑ F<>H
E∷U′ = stabilityTerm (reflConEq ⊢Γ ∙ F≡H) E∷U
in
liftConvTerm $
univ (ΠΣⱼ F∷U G∷U ok) (ΠΣⱼ H∷U E∷U′ ok) (ΠΣ-cong x F<>H G<>E ok);
≅ₜ-zerorefl = liftConvTerm ∘ᶠ zero-refl;
≅-suc-cong = liftConvTerm ∘ᶠ suc-cong;
≅-prod-cong = λ x x₁ x₂ x₃ x₄ →
liftConvTerm (prod-cong x x₁ x₂ x₃ x₄);
≅-η-eq = λ x x₁ x₂ x₃ x₄ x₅ → liftConvTerm (η-eq x₁ x₂ x₃ x₄ x₅);
≅-Σ-η = λ x x₁ x₂ x₃ x₄ x₅ x₆ x₇ → (liftConvTerm (Σ-η x₂ x₃ x₄ x₅ x₆ x₇));
~-var = ~-var;
~-app = ~-app;
~-fst = λ x x₁ x₂ → ~-fst x₂;
~-snd = λ x x₁ x₂ → ~-snd x₂;
~-natrec = ~-natrec;
~-prodrec = λ ⊢A ⊢B C↑D t₁~t₂ u₁↑u₂ _ →
~-prodrec ⊢A ⊢B C↑D t₁~t₂ u₁↑u₂;
~-emptyrec = ~-emptyrec }