[Agda] Agda master is anti-classical, injective type constructors are back

[Owen]

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?

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:

open import Common.Level
open import Common.Prelude
open import Common.Equality

data Moo : Set where
  moo₁ moo₂ : Moo

data HasIrr : Set where
  has-irr : .(moo : Moo) → HasIrr

data Again : (hi : HasIrr) → Set where
  again : (moo : Moo) → Again (has-irr moo)

blah : Again (has-irr moo₁)
blah = again moo₁

data HEq {α} {A : Set α} (a : A) : {B : Set α} (b : B) → Set (lsuc α) where
  refl : HEq a a

thm : ∀{F G : Moo} (a : Again (has-irr F)) (b : Again (has-irr G)) (p : HEq
a b) → F ≡ G
thm (again F) (again .F) refl = refl -- Does not work because F and G are
not identified (by non-injectivity of has-irr)


On Sat, Jan 17, 2015 at 1:56 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> I don't think we should change the meaning of a ~= b, which should be
> given by the natural eliminator for that inductive type, like J is for
> homogeneous equality. All of this orthogonal from whether K is there
> or not.
>
> The fact that one needs to know n == m to make sensible use of (i :
> Fin n) ~= (j : Fin m) is, or should be, already there, because the
> latter only gives us Fin n == Fin m.
> (Fin might not be the best example, because it's provably injective
> from the eliminators: I wouldn't expect pattern matching to figure
> that out automatically but I wouldn't mind if it did.)
>
> The SING case is similar, we should only get something like (eq : SING
> F == SING G) and (cast eq (sing F) == sing G).
>
> In other words, (a : A) ~= (b : B) -> A == B ought to be provable, and
> not the culprit.
>
> A variation of your inj-Fin shows that --without-K is also
> inconsistent with univalence at the moment, since this is accepted:
>
> 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 ()
>
> It's easy to get a proof of (zero : Fin 2) ~= (suc zero : Fin 2) by
> univalence, allowing a closed proof of ⊥.
> A argument of type "zero ≅ suc i" is not absurd.
>
> Cheers,
> Andrea
>
> On Sat, Jan 17, 2015 at 12:07 PM, Andreas Abel <abela at chalmers.se> wrote:
> > This concerns only the unreleased Agda master development branch.
> >
> > Using heterogeneous equality and big forced indices in a data type SING,
> I
> > manage to prove injectivity of type constructor
> >
> >   SING : (Set -> Set) -> Set
> >
> > The rest follows Chung-Kil Hur's refutation of excluded middle, as
> published
> > in January 2010 on the Coq and Agda lists.
> >
> > My development was fathered by my surprise that I could prove
> >
> >   inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → n ≡ m
> >
> > but not by directly matching on the heterogeneous equality (which Agda
> > refuses as Fin n = Fin m does not yield n = m), but by first matching on
> i
> > and j, which exposes n and m in the constructor patterns and makes then
> > available for unification.
> >
> >   inj-Fin-≅ {i = zero}  {zero} ≅refl = refl  -- matching on ≅refl
> succeeds!
> >   inj-Fin-≅ {i = zero}  {suc j} ()
> >   inj-Fin-≅ {i = suc i} {zero} ()
> >   inj-Fin-≅ {i = suc i} {suc j} p = {!p!}   -- Splitting on p succeeds!
> >
> > This is weird.
> >
> > A fix would be to not generate any unification constraints for forced
> > constructor arguments, for instance
> >
> >   fzero : (n : Nat) -> Fin (suc n)
> >
> >   fzero n : Fin (suc n) =?= fzero m : Fin (suc m)
> >
> > would not simplify to n =?= m : Nat.
> >
> > This change would break a lot of developments using heterogeneous
> equality,
> > as did the fix of issue 292
> > (https://code.google.com/p/agda/issues/detail?id=292).  In particular,
> > heterogeneous equality would not imply the equality of the types, but the
> > equality of the types has to be given in order to sensibly work with
> > heterogeneous equality.  In case of Fin, one would work with telescopes
> >
> >   {n m : Nat} (p : n == m) {i : Fin n} {j : Fin m} (q : i ~= j)
> >
> > rather than being able to derive p from q.
> >
> > This is Conor McBride's proposal for heterogeneous equality, if I am not
> > mistaken.
> >
> > RFC,
> > Andreas
> >
> > --
> > Andreas Abel  <><      Du bist der geliebte Mensch.
> >
> > Department of Computer Science and Engineering
> > Chalmers and Gothenburg University, Sweden
> >
> > andreas.abel at gu.se
> > http://www2.tcs.ifi.lmu.de/~abel/
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150117/7ccccf2f/attachment.html