full equality check in coercion boundary #26

New Issue

Closed

opened 2023-08-19 07:22:32 -04:00 by rhi · 2 comments

rhi commented

2023-08-19 07:22:32 -04:00

Owner

e.g.

eq : A ≡ A : ★ ⊢ coe (𝑖 ⇒ eq @𝑖) @p @q s ⇝ s

should work even tho 𝑖 is mentioned

also needs some kind of "known stuck" flag so it doesn't try it again and again if it hasn't changed

e.g. ``` eq : A ≡ A : ★ ⊢ coe (𝑖 ⇒ eq @𝑖) @p @q s ⇝ s ``` should work even tho 𝑖 is mentioned also needs some kind of "known stuck" flag so it doesn't try it again and again if it hasn't changed

rhi added the

bug

label 2023-08-19 07:22:32 -04:00

rhi commented

2024-04-14 15:35:18 -04:00

Author

Owner

the rule in xtt (coercion regularity):


\frac{
  Ψ, j, j' \mid Γ ⊢ A〈j/i〉 = A〈j'/i〉 \; \mathit{type}_k
}{
  Ψ \mid Γ ⊢ \mathsf{coe} \; (i ⇒ A) \; p \; q \; s = (s ∷ A〈q/i〉) ⇒ A〈q/i〉
}

my current rule (shit):


\frac{
  i ∉ \mathsf{fdv}(A)
}{
  Ψ \mid Γ ⊢ \mathsf{coe} \; (i ⇒ A) \; p \; q \; s = (s ∷ A) ⇒ A
}

equivalent to the real rule that may or may not be easier:


\frac{
  Ψ \mid Γ ⊢ A〈0/i〉 = A〈1/i〉 \; \mathit{type}_k
}{
  Ψ \mid Γ ⊢ \mathsf{coe} \; (i ⇒ A) \; p \; q \; s = (s ∷ A〈1/i〉) ⇒ A〈1/i〉
}

the rule in xtt (coercion regularity): $$ \frac{ Ψ, j, j' \mid Γ ⊢ A〈j/i〉 = A〈j'/i〉 \; \mathit{type}_k }{ Ψ \mid Γ ⊢ \mathsf{coe} \; (i ⇒ A) \; p \; q \; s = (s ∷ A〈q/i〉) ⇒ A〈q/i〉 } $$ my current rule (shit): $$ \frac{ i ∉ \mathsf{fdv}(A) }{ Ψ \mid Γ ⊢ \mathsf{coe} \; (i ⇒ A) \; p \; q \; s = (s ∷ A) ⇒ A } $$ --- equivalent to the real rule that may or may not be easier: $$ \frac{ Ψ \mid Γ ⊢ A〈0/i〉 = A〈1/i〉 \; \mathit{type}_k }{ Ψ \mid Γ ⊢ \mathsf{coe} \; (i ⇒ A) \; p \; q \; s = (s ∷ A〈1/i〉) ⇒ A〈1/i〉 } $$

rhi commented

2024-04-14 16:09:29 -04:00

Author

Owner

test case:

def0 ugh : (A : ★) → (AA : A ≡ A : ★) → (s : A) →
           (P : A → ★) → P s → P (coe (𝑖 ⇒ AA @𝑖) s) =
  λ A AA s P p ⇒ p

test case: ```quox def0 ugh : (A : ★) → (AA : A ≡ A : ★) → (s : A) → (P : A → ★) → P s → P (coe (𝑖 ⇒ AA @𝑖) s) = λ A AA s P p ⇒ p ```

rhi referenced a pull request that will close this issue

2024-04-15 16:41:31 -04:00

coercion regularity #43

rhi closed this issue

2024-04-18 16:18:20 -04:00

No Label

No Milestone

No Assignees

1 Participants

Notifications

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: rhi/quox#26

No description provided.