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

[Andreas Abel]

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>> 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
> 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
http://www2.tcs.ifi.lmu.de/~abel/