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

[Jesper Cockx]

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> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140117/65ab36cd/attachment.html