Cubical does not ensure EQUIVFUN has left inverse

[nrosnick]

Version:
Agda version 2.6.3-dbadb16

Description:
When defining the builtins EQUIV and EQUIVFUN, we are forced to prove certain properties about them before we can use them for computing. I believe the point of EQUIVPROOF is to ensure that EQUIVFUN is surjective. However, there is no check that EQUIVFUN is injective, allowing use to define EQUIV such that we must provide a right inverse but do not require a left inverse. Using this new definition of EQUIV, we can prove that the unit type is equal to the Boolean type via Univalence. Due to only using builtins and primitives, all of this is allowed even with the --safe option.

Code:

{-# OPTIONS --cubical --safe #-}
module Test2 where

open import Agda.Primitive
open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub
open import Agda.Builtin.Cubical.HCompU
open import Agda.Builtin.Sigma

≡refl : ∀ {α} {A : Set α} {a : A} → a ≡ a
≡refl {a = a} = λ _ → a

≡sym : ∀ {α} {A : Set α} {a b : A} → a ≡ b → b ≡ a
≡sym p = λ i → p (primINeg i)

≡subst : ∀ {α β} {A : Set α} (B : A → Set β) {a b : A} → a ≡ b → B a → B b
≡subst B p h = primTransp (λ i → B (p i)) i0 h

record _≃_ {α β} (A : Set α) (B : Set β) : Set (α ⊔ β) where
  field
    ≃comp : A → B
    ≃inv : B → A
    ≃comp-inv : (b : B) → ≃comp (≃inv b) ≡ b
open _≃_
{-# BUILTIN EQUIV _≃_ #-}
{-# BUILTIN EQUIVFUN ≃comp #-}

equiv-proof : ∀ {α β} (A : Set α) (B : Set β) (f : A ≃ B) (b : B) (i : I) → Partial i (Σ A (λ a → ≃comp f a ≡ b)) → Σ A (λ a → ≃comp f a ≡ b)
equiv-proof A B f b i p = ≃inv f b , ≃comp-inv f b
{-# BUILTIN EQUIVPROOF equiv-proof #-}

primitive
  primGlue : _
  prim^glue : _
  prim^unglue : _

≃refl : ∀ {α} {A : Set α} → A ≃ A
≃comp ≃refl = λ a → a
≃inv ≃refl = λ a → a
≃comp-inv ≃refl = λ a → ≡refl

ua : ∀ {α} {A B : Set α} → A ≃ B → A ≡ B
ua {_} {A} {B} f = λ i → primGlue B (λ { (i = i0) → A ; (i = i1) → B }) λ { (i = i0) → f ; (i = i1) → ≃refl }

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

data Bool : Set where
  true false : Bool

-- The function for this equivalence is surjective but not injective
-- In particular, the inverse function is a right inverse but no left inverse is definable
Bool≃⊤ : Bool ≃ ⊤
≃comp Bool≃⊤ = λ _ → tt
≃inv Bool≃⊤ = λ _ → true
≃comp-inv Bool≃⊤ = λ _ → ≡refl

Bool≡⊤ : Bool ≡ ⊤
Bool≡⊤ = ua Bool≃⊤

⊤-compact : (a b : ⊤) → a ≡ b
⊤-compact _ _ = ≡refl

Bool-reify : Bool → Set
Bool-reify true = ⊤
Bool-reify false = ⊥

true≢false : true ≡ false → ⊥
true≢false p = ≡subst Bool-reify p tt

true≡false : true ≡ false
true≡false = ≡subst (λ A → (a b : A) → a ≡ b) (≡sym Bool≡⊤) ⊤-compact true false

-- Normal form is `tt`: Subject reduction is broken
oops : ⊥
oops = true≢false true≡false

[Saizan]

I consider the implementations in the .Builtin files part of the trusted codebase, other implementations are not supported.

The EQUIVPROOF builtin is there because it is used in the computation of transport, not necessarily to enforce properties of EQUIVFUN.

Mostly it would be silly to add tests that make sure that the given implementation of the builtins is equal to the intended one, that would just be repeating the implementation twice. The main reason these are builtins is that their implementation is easier to write as Agda programs than by manipulating the internal representation.

I also do not wish to work out a theory where isEquiv is axiomatized,

Maybe we need a mechanism so that when --safe some BUILTIN declarations are only allowed from specific Builtin modules?

[nad]

Maybe we need a mechanism so that when --safe some BUILTIN declarations are only allowed from specific Builtin modules?

I suggest that we put the builtin modules in a library called something like primitive or agda-primitive, and disallow most or all builtins in other libraries if --safe is active.

[nad]

Is there a list of the Cubical Agda builtins/primitives which one can define in "incorrect" ways? Did your change remove one or more items from this list?

[plt-amy]

Off the top of my head, the only bulitins you could mess up are EQUIVPROOF and TRANSPPROOF; the former has been fixed now. I'll have a look to make sure I'm not missing any built-ins, and document the list.

[nad]

If it is possible to mess up anything in such a way that this could lead to an inconsistency or a runtime error, then I think the corresponding binding should only be allowed in non---safe code (plus the builtin modules).

[andreasabel]

@plt-amy: Fixed issues should be added to the correct milestone, so we can automatically generate the "closed issues" section of the respective CHANGELOG.
This issue existed in 2.6.1 and 2.6.2 and is fixed in 2.6.3.

[plt-amy]

@andreasabel Ah, alright! I'll go through the issues I've closed and see whether any are missing a milestone. Thanks for the shout.