Why bother with Agda.Builtin.Cubical.Id?

[amp12]

The following is a question/comment, rather than a bug report.

As I understand it, Agda.Builtin.Cubical.Id hardwires into
Agda-cubical Andrew Swan's trick for creating an identity type with
definitional computational rule within the cubical sets model of Type
Theory.

Why bother? There is already a perfectly good identity type with
definitional computational rule within Agda, given by
Agda.Builtin.Equality (≡). This can be proved to be path equivalent to
Agda-cubical's path type (here denoted ~ to distinguish it from
≡) -- see the proof
here.

The advantage of ≡ over Id from Agda.Builtin.Cubical.Id is that we
have access to pattern matching on refl.

[martinescardo]

(1) One question is whether there is an extension of MLTT in which univalence holds with respect to the MLTT identity type, with J with its definitional rule. Swan's cubical identity type answers this positively. (2) If one wants to work in a basic univalent type theory (for example so that our development works in a variety of models, including arbitrary infty-toposes), then cubical type theory is not for this job. However, one can still prove things in Agda + univalent assumptions, including J with its computation rule, and *then* use cubical Agda to compute results. For these reasons, I use the identity type rather than the path type, and in fact the HoTT/UF interface provided in the library. This is for the sake of generality. Martin

…

On 18/06/2019 13:27, ***@***.*** wrote: {-# OPTIONS --cubical #-} module WhyBotherWithBuiltinCubicalId where {- The following is a question/comment, rather than a bug report. As I understand it, Agda.Builtin.Cubical.Id hardwires into Agda-cubical Andrew Swan's trick for creating an identity type with definitional computational rule within the cubical sets model of Type Theory. Why bother? There is already a perfectly good identity type with definitional computational rule within Agda, given by Agda.Builtin.Equality (≡). This can be proved to be path equivalent to Agda-cubical's path type (here denoted /~/ to distinguish it from /≡/) -- see the proof below. The advantage of /≡/ over Id from Agda.Builtin.Cubical.Id is that we have access to pattern matching on refl. -} open import Agda.Builtin.Cubical.Path renaming (/≡/ to /~/) open import Agda.Builtin.Equality open import Agda.Primitive open import Agda.Primitive.Cubical ~refl : {l : Level} {A : Set l} {x : A} → ---------- x ~ x ~refl {x = x} _ = x transport : {l : Level} {A B : Set l} (p : A ~ B) → ------------ A → B transport p x = primComp (λ i → p i) i0 (λ _ ()) x transportrefl : {l : Level} {A : Set l} (x : A) → ------------------- transport ~refl x ~ x transportrefl {A = A} x i = primComp (λ _ → A) i (λ _ _ → x) x ~elim : {l m : Level} {A : Set l} {x : A} (P : ∀ y → x ~ y → Set m) (d : P x ~refl) {y : A} (p : x ~ y) → ----------------------- P y p ~elim P d p = transport (λ i → P (p i) (λ j → p (primIMin i j))) d ------------------------------------------------------------------------ -- Inductive identity types and path types are path-equivalent ≡2~ : {ℓ : Level} {A : Set ℓ} {x y : A} → ----------- x ≡ y → x ~ y ≡2~ refl = ~refl ~2≡ : {ℓ : Level} {A : Set ℓ} {x y : A} → ----------- x ~ y → x ≡ y ~2≡ {x = x} p = transport (λ i → x ≡ p i) refl ≡2∘2≡ : {ℓ : Level} {A : Set ℓ} {x y : A} (p : x ~ y) → ------------- ≡2~ (2≡ p) ~ p ≡2∘~2≡ = elim (λ _ p → ≡2 (2≡ p) ~ p) (λ i → ≡2 (transportrefl refl i)) 2≡∘≡2 : {ℓ : Level} {A : Set ℓ} {x y : A} (p : x ≡ y) → ------------- 2≡ (≡2 p) ~ p 2≡∘≡2 refl = transportrefl refl — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#157?email_source=notifications&email_token=ABASAE3IFULTVJEYYJFYFB3P3DIBNA5CNFSM4HY7P2YKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4G2EERRQ>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABASAE7VV37UE4OJSUAD6XLP3DIBNANCNFSM4HY7P2YA>.

-- Martin Escardo http://www.cs.bham.ac.uk/~mhe

[martinescardo]

Also using this trick of yours (which I tried myself to be able to do pattern atching on refl as you say) breaks computation, and this is a reason for not using the Agda builtin equality with cubical Agda.

[Saizan]

Soon transp will actually compute for inductive families, which should indeed make the equality from Agda.Builtin.Equality no lesser than Swan's Id.

[martinescardo]

That'd be great.

[martinescardo]

It will mean that I have to do nothing to port my development from Agda to cubical Agda.

[amp12]

@martinescardo: could you elaborate your comment about it breaking computation? (an example?)

[martinescardo]

In principle I could. But I will not try as I can't come up with a quick example. The way we discovered this, with Chuangjie, was when porting his PhD thesis Agda code to cubical.

http://www.cs.bham.ac.uk/~mhe/chuangjie-xu-thesis-cubical/

The first thing we tried was precisely your trick. Then when we tried to compute a modulus of uniform continuity, which should have been zero, we instead got a pattern matching runtime error.

We then instead used Swan's identity type and converted all definitions by pattern matching to uses of J, which took 10 hours.

[amp12]

you are truly dedicated scholars! :-)

[martinescardo]

I think it is enough to use an example that uses funext to compute a number, such as the one I gave in this file https://github.com/agda/cubical/blob/master/Cubical/Foundations/HoTT-UF.agda

[Saizan]

Here's a small example.

open import Agda.Builtin.Equality
open import Agda.Primitive.Cubical renaming (primTransp to transp)

coerce : ∀ {A B : Set} → A ≡ B → A → B
coerce refl x = x

data D : Set where
  d : D

test = coerce (transp (\ _ → D ≡ D) i0 refl) d

{-                                                                                                                                                                                     
                                                                                                                                                                                       
C-c C-n test                                                                                                                                                                           
                                                                                                                                                                                       
Time: 2ms                                                                                                                                                                              
coerce (transp (λ _ → D ≡ D) i0 refl) d                                                                                                                                                
                                                                                                                                                                                       
-}

[martinescardo]

@Saizan : I am puzzled how being able to compute with inductive families will make the above example work.

[martinescardo]

@amp12 To elaborate a bit, what happens is that Agda computes by matching on refl, but then instead of seeing a refl it sees something injected in the identity type by the equivalence you describe, which is not a refl, and then Agda doesn't know what to do.

[Saizan]

@martinescardo In the future, coerce will be automatically given extra clauses that will be able to deal with the residual transports on the index, as those too will be canonical elements, given that they cannot be represented by refl.