<div dir="ltr"><div><div>If (the goal is that) type constructors are never provably injective, then should everything work the same if type indices are always wrapped in the irrelevant position of a data constructor?<br><br>Here is an attempt to use the same argument to extract an irrelevant field, which fails because the non-injectivity of irrelevant fields is more strictly enforced:<br></div><div><br><span style="font-family:georgia,serif">open import Common.Level<br>open import Common.Prelude<br>open import Common.Equality<br><br>data Moo : Set where<br> moo₁ moo₂ : Moo<br><br>data HasIrr : Set where<br> has-irr : .(moo : Moo) → HasIrr<br><br>data Again : (hi : HasIrr) → Set where<br> again : (moo : Moo) → Again (has-irr moo)<br><br>blah : Again (has-irr moo₁)<br>blah = again moo₁<br><br>data HEq {α} {A : Set α} (a : A) : {B : Set α} (b : B) → Set (lsuc α) where<br> refl : HEq a a<br><br>thm : ∀{F G : Moo} (a : Again (has-irr F)) (b : Again (has-irr G)) (p : HEq a b) → F ≡ G<br>thm (again F) (again .F) refl = refl -- Does not work because F and G are not identified (by non-injectivity of has-irr)<br></span><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Jan 17, 2015 at 1:56 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I don't think we should change the meaning of a ~= b, which should be<br>
given by the natural eliminator for that inductive type, like J is for<br>
homogeneous equality. All of this orthogonal from whether K is there<br>
or not.<br>
<br>
The fact that one needs to know n == m to make sensible use of (i :<br>
Fin n) ~= (j : Fin m) is, or should be, already there, because the<br>
latter only gives us Fin n == Fin m.<br>
(Fin might not be the best example, because it's provably injective<br>
from the eliminators: I wouldn't expect pattern matching to figure<br>
that out automatically but I wouldn't mind if it did.)<br>
<br>
The SING case is similar, we should only get something like (eq : SING<br>
F == SING G) and (cast eq (sing F) == sing G).<br>
<br>
In other words, (a : A) ~= (b : B) -> A == B ought to be provable, and<br>
not the culprit.<br>
<br>
A variation of your inj-Fin shows that --without-K is also<br>
inconsistent with univalence at the moment, since this is accepted:<br>
<br>
OffDiag : ∀ {n m} → Fin n → Fin m → Set<br>
OffDiag zero zero = ⊥<br>
OffDiag (suc _) (suc _) = ⊥<br>
OffDiag _ _ = ⊤<br>
<br>
inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → OffDiag i j → ⊥<br>
inj-Fin-≅ {i = zero} {zero} eq ()<br>
<span class="">inj-Fin-≅ {i = zero} {suc j} ()<br>
inj-Fin-≅ {i = suc i} {zero} ()<br>
</span>inj-Fin-≅ {i = suc i} {suc j} p ()<br>
<br>
It's easy to get a proof of (zero : Fin 2) ~= (suc zero : Fin 2) by<br>
univalence, allowing a closed proof of ⊥.<br>
A argument of type "zero ≅ suc i" is not absurd.<br>
<br>
Cheers,<br>
Andrea<br>
<div><div class="h5"><br>
On Sat, Jan 17, 2015 at 12:07 PM, Andreas Abel <<a href="mailto:abela@chalmers.se">abela@chalmers.se</a>> wrote:<br>
> This concerns only the unreleased Agda master development branch.<br>
><br>
> Using heterogeneous equality and big forced indices in a data type SING, I<br>
> manage to prove injectivity of type constructor<br>
><br>
> SING : (Set -> Set) -> Set<br>
><br>
> The rest follows Chung-Kil Hur's refutation of excluded middle, as published<br>
> in January 2010 on the Coq and Agda lists.<br>
><br>
> My development was fathered by my surprise that I could prove<br>
><br>
> inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → n ≡ m<br>
><br>
> but not by directly matching on the heterogeneous equality (which Agda<br>
> refuses as Fin n = Fin m does not yield n = m), but by first matching on i<br>
> and j, which exposes n and m in the constructor patterns and makes then<br>
> available for unification.<br>
><br>
> inj-Fin-≅ {i = zero} {zero} ≅refl = refl -- matching on ≅refl succeeds!<br>
> inj-Fin-≅ {i = zero} {suc j} ()<br>
> inj-Fin-≅ {i = suc i} {zero} ()<br>
> inj-Fin-≅ {i = suc i} {suc j} p = {!p!} -- Splitting on p succeeds!<br>
><br>
> This is weird.<br>
><br>
> A fix would be to not generate any unification constraints for forced<br>
> constructor arguments, for instance<br>
><br>
> fzero : (n : Nat) -> Fin (suc n)<br>
><br>
> fzero n : Fin (suc n) =?= fzero m : Fin (suc m)<br>
><br>
> would not simplify to n =?= m : Nat.<br>
><br>
> This change would break a lot of developments using heterogeneous equality,<br>
> as did the fix of issue 292<br>
> (<a href="https://code.google.com/p/agda/issues/detail?id=292" target="_blank">https://code.google.com/p/agda/issues/detail?id=292</a>). In particular,<br>
> heterogeneous equality would not imply the equality of the types, but the<br>
> equality of the types has to be given in order to sensibly work with<br>
> heterogeneous equality. In case of Fin, one would work with telescopes<br>
><br>
> {n m : Nat} (p : n == m) {i : Fin n} {j : Fin m} (q : i ~= j)<br>
><br>
> rather than being able to derive p from q.<br>
><br>
> This is Conor McBride's proposal for heterogeneous equality, if I am not<br>
> mistaken.<br>
><br>
> RFC,<br>
> Andreas<br>
><br>
> --<br>
> Andreas Abel <>< Du bist der geliebte Mensch.<br>
><br>
> Department of Computer Science and Engineering<br>
> Chalmers and Gothenburg University, Sweden<br>
><br>
> <a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a><br>
> <a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
><br>
</div></div>> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>