rhi/quox

Fork 0

full equality check in coercion boundary #26

New issue

Closed

opened 2023-08-19 13:22:32 +02:00 by rhi · 2 comments

rhi commented

2023-08-19 13:22:32 +02: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 13:22:32 +02:00

rhi commented

2024-04-14 21:35:18 +02: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 22:09:29 +02: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 this issue from a pull request that will close it,

2024-04-15 22:41:31 +02:00

coercion regularity #43

rhi closed this issue

2024-04-18 22:18:20 +02:00

No labels

No milestone

No project

No assignees

1 participant

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.

Rows
Columns