# Heterogeneous equality incompatible with univalence even --without-K #1408

Closed
opened this Issue Aug 8, 2015 · 9 comments

Projects
None yet
2 participants

### GoogleCodeExporter commented Aug 8, 2015

 Paradox found by Andrea Vezzosi: ```{-# OPTIONS --without-K #-} -- {-# OPTIONS -v tc.lhs.unify:15 #-} open import Common.Equality open import Common.Prelude data Fin : (n : Nat) → Set where zero : {n : Nat} → Fin (suc n) suc : {n : Nat} (i : Fin n) → Fin (suc n) data _≅_ {A : Set} (a : A) : {B : Set} (b : B) → Set1 where refl : a ≅ a OffDiag : ∀ {n m} → Fin n → Fin m → Set OffDiag zero zero = ⊥ OffDiag (suc _) (suc _) = ⊥ OffDiag _ _ = ⊤ inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → OffDiag i j → ⊥ inj-Fin-≅ {i = zero} {zero} eq () inj-Fin-≅ {i = zero} {suc j} () inj-Fin-≅ {i = suc i} {zero} () inj-Fin-≅ {i = suc i} {suc j} p () cast : ∀ {α} → {A B : Set α} (p : A ≡ B) (a : A) → B cast refl a = a intro : ∀ {A B : Set}{a b} → (eq : A ≡ B) → cast eq a ≡ b → a ≅ b intro refl refl = refl -- we can get these from univalence postulate swap : Fin 2 ≡ Fin 2 swap-lemma : cast swap zero ≡ suc zero bottom : ⊥ bottom = inj-Fin-≅ (intro swap swap-lemma) _``` Original issue reported on code.google.com by `andreas....@gmail.com` on 19 Jan 2015 at 2:33

### GoogleCodeExporter commented Aug 8, 2015

 The original example from #292 can also be adapted, `Bool` is as "equal" to `Fin 2`, as `D true` is "equal" to `D false`. ```{-# OPTIONS --without-K #-} open import Data.Empty open import Data.Bool open import Data.Product open import Relation.Binary.HeterogeneousEquality hiding (subst) open import Relation.Binary.PropositionalEquality data D : Bool → Set where x : D true y : D false P : Set -> Set P S = Σ S (\s → s ≅ x) pbool : P (D true) pbool = _ , refl ¬pfin : P (D false) → ⊥ ¬pfin (y , ()) tada : D true ≡ D false → ⊥ tada eq = ⊥-elim ( ¬pfin (subst (\ S → P S) eq pbool ) )``` Original comment by `sanzhi...@gmail.com` on 19 Jan 2015 at 2:44

### GoogleCodeExporter commented Aug 8, 2015

 I think we should listen to this remark by Andrea: According to "A few constructions on constructors" the types don't need to be strictly equal, but in addition of having the same shape you need equality constraints for all the arguments of the family. In particular, in the second clause of `inj-Fin-≅`, Agda should require that `n = m` when refuting `zero {n} = suc {m} j` (and similarly for the third clause). Since there is no way to get `n = m`, unification should just fail (as opposed to refuting the equations). Alternatively, we could disable heterogeneous equations altogether when working `--without-K`. Are there cases (again, when working `--without-K`) where this is undesirable? Original comment by `jesper.c...@gmail.com` on 19 Jan 2015 at 3:02

### GoogleCodeExporter commented Aug 8, 2015

 In the issue #292 there are a few examples that should be fine even `--without-K` but still require to consider equations that are not homogeneous "on the nose". e.g. in the following the definition of Foo is justified because we can conclude `d₁ /== d₂` under the assumption that `i₁ == i₂`. ```module Bug where postulate I : Set i₁ i₂ : I data D : I → Set where d₁ : D i₁ d₂ : D i₂ data P : ∀ {i} → D i → Set where p₁ : P d₁ p₂ : P d₂ Foo : P d₁ → Set₁ Foo p₁ = Set``` Original comment by `sanzhi...@gmail.com` on 19 Jan 2015 at 5:30

### GoogleCodeExporter commented Aug 8, 2015

 I see. Currently, your definition of `Foo` isn't accepted by `--without-K` either because the first equation gets stuck on `i₁ = i₁`, but I agree that it should be. So there seem to be two (related) problems: When --without-K is enabled, the unifier gives up immediately when it encounters a reflexive equation. Instead, it should postpone this equation in the hope that it will encounter another equation dependent on this one. For example, when working on the equations `i₁ = i₁ ; d₁ = d₁` for checking the definition of `Foo` in #3, rather than giving up on `i₁ = i₁`, the unifier should postpone this equation. When applying injectivity to `d₁ = d₁`, it should then detect that this also solves the postponed equation (because `i₁` is in the index of the type of `d₁`). This can be justified theoretically by appealing to the general (heterogeneous) injectivity rule in my paper, instead of the homogeneous one. The second problem is that shape-based unification fails to take into account whether the arguments that go into the shape are equal. In general, it is also important why they are equal (since in HoTT there may be multiple distinct equality proofs). However, this is not the case when applying the conflict rule, since an absurd clause has no RHS that can depend on the result of unification (i.e. the conflict rule factors through the empty type). So for absurd clauses, we only need to care that there is some evidence that makes the types equal, but we don't care what it is. So a proper solution would be: when trying to apply the conflict rule, first check equality of the indices of the types of the constructors, making use of previously delayed equations in the process. If they are equal under the given assumptions, we win. Otherwise, delay this equation as well and continue unifying. Of course, implementing this could be rather tricky, as it is not clear to me how to do this "equality checking under given assumptions". I hope I made myself clear, these things can be rather tricky to explain. Feel free to ask if I can clarify something further :) Original comment by `jesper.c...@gmail.com` on 20 Jan 2015 at 5:24

### GoogleCodeExporter commented Aug 8, 2015

 On point 2, I figure we still need to be careful about discharging other reflexive constraints lying around though, like what you'd get by splitting on `true ~= false`. At the moment that throws a WithoutK exception, and we should keep it so. Original comment by `sanzhi...@gmail.com` on 20 Jan 2015 at 11:48

### GoogleCodeExporter commented Aug 8, 2015

 Since "equality checking given assumptions" might need some proper work, I've removed (hopefully) the incompatibility with univalence by forcing the types to unify in a heterogeneous constructor mismatch: e06d5e7 Original comment by `sanzhi...@gmail.com` on 21 Jan 2015 at 4:52

### GoogleCodeExporter commented Aug 8, 2015

 Seems fine to me on first sight. I've been doing some more thinking on "equality checking giving assumptions", and I think a proper solution would first need a reworking of the HomHet type to include more information about the exact position where the heterogenity occurs (e.g. `Het (Fin m) (Fin n)` is not the same as `Fin (Het m n)`, and possibly also the evidence of why they are equal (e.g. a list of postponed equations that need to be solved first). Does this seem like a good idea? Original comment by `jesper.c...@gmail.com` on 21 Jan 2015 at 5:17

### GoogleCodeExporter commented Aug 8, 2015

 It's well motivated by the uses of PathOver in HoTT-Agda, I think. Original comment by `sanzhi...@gmail.com` on 22 Jan 2015 at 1:55
Contributor

### jespercockx commented Jan 6, 2016

 Fixed by the new unifier, see a92c76e.