[Agda] Re: Yet another way Agda --without-K is incompatible with univalence

[Andreas Abel]

Thanks for clarifying.

We are also not relieved, probably... ;-)

What does your own version of --without-K say?

Cheers,
Andreas

On 17.01.2014 14:43, Jesper Cockx wrote:
> I'm not relieved. The problem is still there.
>
>
> On Fri, Jan 17, 2014 at 2:38 PM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
>     Can you explain, please?
>
>     You say you did not expect to be able to prove 'problem' from
>     'equiv-to-id' which you thought was univalence.  Martin tells you
>     that 'equiv-to-id' is a consequence of univalence.  Now you are
>     relieved. But still 'problem' follows from univalence.  Why are you
>     relieved now?
>
>     Sorry, I am a bit confused now...
>     Andreas
>
>
>     On 17.01.2014 13:39, Jesper Cockx wrote:
>
>         As Martin pointed out to me, my definition of equiv-to-id is not the
>         univalence axiom, but merely a (much weaker) consequence of it.
>         Thank you.
>
>         Best,
>         Jesper
>
>
>         On Fri, Jan 17, 2014 at 12:19 PM, Jesper Cockx
>         <Jesper at sikanda.be <mailto:Jesper at sikanda.be>
>         <mailto:Jesper at sikanda.be <mailto:Jesper at sikanda.be>>> wrote:
>
>              Dear all,
>
>              Much to my own surprise, I encountered another problem with the
>              --without-K option. This is on the latest darcs version of
>         Agda and
>              is unrelated to the termination checker. As far as I
>         understand, the
>              unification algorithm is applying the injectivity rule too
>         liberally
>              for data types indexed over indexed data. But maybe someone
>         else can
>              give a better explanation?
>
>              === BEGIN CODE ===
>
>              {-# OPTIONS --without-K #-}
>
>              module YetAnotherWithoutKProblem where
>
>              -- First, some preliminaries to make this file self-contained.
>              data _≡_ {a} {A : Set a} (x : A) : A → Set where
>                 refl : x ≡ x
>
>              subst : ∀ {a b} {A : Set a} {x : A} (B : (y : A) → Set b) →
>                       {y : A} → x ≡ y → B x → B y
>              subst B refl b = b
>
>              record _≃_ (A B : Set) : Set where
>                 constructor equiv
>                 field
>                   f : A → B
>                   g : B → A
>                   i : (x : A) → g (f x) ≡ x
>                   j : (y : B) → f (g y) ≡ y
>
>              -- The univalence axiom.
>              postulate equiv-to-id : {A B : Set} → A ≃ B → A ≡ B
>
>              -- Now consider any concrete space 'mySpace' with a point
>         'myPoint'.
>              -- We will show that mySpace has no structure above
>         dimension 2.
>              postulate mySpace : Set
>              postulate myPoint : mySpace
>
>              -- We define Foo in a way such that 'Foo e' is equivalent
>         with 'refl
>              ≡ e'.
>              data Foo : myPoint ≡ myPoint → Set where
>                 foo : Foo refl
>
>              Foo-equiv : {e : myPoint ≡ myPoint} → Foo e ≃ (refl ≡ e)
>              Foo-equiv = equiv f g i j
>                 where
>                   f : {e : myPoint ≡ myPoint} → Foo e → refl ≡ e
>                   f foo = refl
>
>                   g : {e : myPoint ≡ myPoint} → refl ≡ e → Foo e
>                   g refl = foo
>
>                   i : {e : myPoint ≡ myPoint} (m : Foo e) → g (f m) ≡ m
>                   i foo = refl
>
>                   j : {e : myPoint ≡ myPoint} (i : refl ≡ e) → f (g i) ≡ i
>                   j refl = refl
>
>              -- Here comes the real problem: by injectivity, 'Foo e' is
>         a set ...
>              test : {e : myPoint ≡ myPoint} → (a : Foo e) → (i : a ≡ a)
>         → i ≡ refl
>              test foo refl = refl
>
>              -- ... hence by univalence, so is 'refl ≡ e'.
>              problem : {e : myPoint ≡ myPoint} → (a : refl ≡ e) → (i : a
>         ≡ a) → i
>              ≡ refl
>              problem = subst (λ X → (x : X) → (i : x ≡ x) → i ≡ refl)
>                               (equiv-to-id Foo-equiv)
>                               test
>
>              === END CODE ===
>
>              All the best,
>              Jesper
>
>
>
>
>         _________________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         https://lists.chalmers.se/__mailman/listinfo/agda
>         <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>     --
>     Andreas Abel  <><      Du bist der geliebte Mensch.
>
>     Theoretical Computer Science, University of Munich
>     Oettingenstr. 67, D-80538 Munich, GERMANY
>
>     andreas.abel at ifi.lmu.de <mailto:andreas.abel at ifi.lmu.de>
>     http://www2.tcs.ifi.lmu.de/~__abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/