Proof of ⊥ with --safe --cubical #5838
Assignees
Labels
cubical
Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp
false
Proof of the empty type which checks without known-unsafe flags (e.g. without --type-in-type)
hits
Higher inductive types
univalence
Glue reduction; Inconsistency with postulated univalence even --without-K
Milestone
Comments
andreasabel
added
univalence
|
Here is a version with explicit imports: {-# OPTIONS --safe --cubical #-}
open import Cubical.Foundations.Prelude using
( Type; i0; i1; ~_; _∧_; _∨_
; Path; PathP; _≡_; cong; hcomp; refl; sym; transp; transport; transportRefl; _∙∙_∙∙_
; _,_
)
open import Cubical.Foundations.Equiv using (equivEq; idEquiv)
open import Cubical.Foundations.Univalence using (Glue)
open import Cubical.HITs.S1 using (S¹; base; rotLoop; winding)
open import Cubical.Data.Empty using (⊥)
open import Cubical.Data.Unit using (Unit; tt)
open import Cubical.Data.Nat.Literals
open import Cubical.Data.Int renaming (Int to ℤ) using (pos)
-- Transposition of 2-loops
--
-- sq: transpose sq:
--
-- p p
-- x --→-- y x --→-- y
-- | | | |
-- r ↓ ⇒ ↓ q → r ↓ ⇓ ↓ q
-- | | | |
-- w --→-- z w --→-- z
-- s s
transpose : ∀ {ℓ} {A : Type ℓ} {x y z w : A}
{p : x ≡ y} {q : y ≡ z}
{r : x ≡ w} {s : w ≡ z}
→ PathP (λ i → p i ≡ s i) r q
→ PathP (λ i → r i ≡ q i) p s
transpose sq i j = sq j i
-- Transposition of 2-loops is equal to inversion (sym)
transpose-sym : ∀ {ℓ} {A : Type ℓ} {x : A} (p : Path (x ≡ x) refl refl) →
Path (Path (x ≡ x) refl refl)
(transpose p)
(sym p)
transpose-sym p i j k =
hcomp (λ l → λ { (i = i0) → p k j
; (i = i1) → p (~ j) k
; (j = i0) → p (i ∨ k ∨ l) (i ∧ k)
; (j = i1) → p (~ i ∧ k ∧ ~ l) (~ i ∨ k)
; (k = i0) → p (i ∧ ~ j ∧ ~ l) (~ i ∧ j)
; (k = i1) → p (~ i ∨ ~ j ∨ l) (i ∨ j)
})
(p ((~ j ∧ k) ∨ (i ∧ ~ j) ∨ (~ i ∧ k)) ((j ∧ k) ∨ (~ i ∧ j) ∨ (i ∧ k)))
-- Candidate implementation of "local-global looping principle" as
-- Nicolai Kraus called it. I am not certain if these are really
-- correct, but they demonstrate the bug.
global : ∀ {ℓ} {A : Type ℓ} → ((x : A) → x ≡ x) → Path (A ≡ A) refl refl
global {A = A} h i j =
Glue A (λ { (i = i0) → A , idEquiv A
; (i = i1) → A , idEquiv A
; (j = i0) → A , equivEq {e = idEquiv A} {f = idEquiv A} (λ k x → h x k) i
; (j = i1) → A , idEquiv A
})
-- This seems OK:
local : ∀ {ℓ} {A : Type ℓ} → Path (A ≡ A) refl refl → ((x : A) → x ≡ x)
local {A = A} h x = sym (transportRefl x) ∙∙ (λ i → transp (λ j → h i j) i0 x) ∙∙ transportRefl x
-- This one seems problematic:
local' : ∀ {ℓ} {A : Type ℓ} → Path (A ≡ A) refl refl → ((x : A) → x ≡ x)
local' h x i = transp (λ j → h i j) (i ∨ ~ i) x
-- Now a specific example, the circle S¹
-- 𝔾 is supposed to be equivalent to ℤ
𝔾 : Type₁
𝔾 = Path (Path Type₀ S¹ S¹) refl refl
𝟙 : 𝔾
𝟙 = global rotLoop
-- by above, these are supposed to be equal
*𝔾 -𝔾 : 𝔾 → 𝔾
*𝔾 = transpose
-𝔾 = sym
-- seemingly correct conversion to ints
toℤ : 𝔾 → ℤ
toℤ n = winding (local n base)
_ : toℤ (*𝔾 𝟙) ≡ toℤ (-𝔾 𝟙)
_ = refl {x = -1}
-- problematic conversion to ints
problem : 𝔾 → ℤ
problem n = winding (local' n base)
-- it doesn't respect transpose-sym!
_ : problem (*𝔾 𝟙) ≡ 0 -- ???
_ = refl
_ : problem (-𝔾 𝟙) ≡ -1
_ = refl
-- so we get a contradiction
bad : 0 ≡ -1
bad = cong problem (transpose-sym (global rotLoop))
boom : ⊥
boom = transport (λ i → iszero (bad i)) tt
where
iszero : ℤ → Type₀
iszero (pos 0) = Unit
iszero _ = ⊥I could reproduce the bug on 2.6.2 and |
|
This looks like a consequence of #5755. |
|
Thanks, glad to see you all are already on the case! Feel free to close this issue if desired, of course. Side note: I thought maybe the problematic |
|
Shrinking action by 4 C/H type theorists and me produced this simplification in 3 hours: {-# OPTIONS --safe --cubical #-}
open import Cubical.Foundations.Prelude using
( Type; I; i0; i1; ~_; _∧_; _∨_
; Path; _≡_; refl; transp
; _,_
)
open import Cubical.Foundations.Equiv using (_≃_; equivEq; idEquiv)
open import Cubical.Foundations.Univalence using (Glue; ua)
open import Cubical.HITs.S1 using (S¹; base; loop; rotLoop)
open import Cubical.Data.Bool using (Bool; true; false; notEquiv)
-- A minus-one in a type equivalent to the integers.
minus-one : Path (Path Type₀ S¹ S¹) refl refl
minus-one i j = Glue S¹ λ
{ (i = i0) → S¹ , equivEq {e = idEquiv S¹} {f = idEquiv S¹} (λ k x → rotLoop x k) j
; (i = i1) → S¹ , idEquiv S¹
; (j = i0) → S¹ , idEquiv S¹
; (j = i1) → S¹ , idEquiv S¹
}
DoubleCover : S¹ → Type₀
DoubleCover base = Bool
DoubleCover (loop i) = ua notEquiv i
bad : true ≡ false
bad k = transp (λ i → DoubleCover (transp (λ j → minus-one i j) (k ∧ (i ∨ ~ i)) base)) i0 false
|
|
Inlining the cubical library, this confirms the problem existed from the beginning (Agda 2.6.0), maybe unsurprisingly: {-# OPTIONS --safe --cubical #-}
open import Agda.Builtin.Bool
open import Agda.Builtin.Sigma
open import Agda.Primitive.Cubical
open import Agda.Primitive.Cubical public
renaming ( primIMin to _∧_ -- I → I → I
; primIMax to _∨_ -- I → I → I
; primINeg to ~_ -- I → I
; isOneEmpty to empty
; primComp to comp
; primHComp to hcomp
; primTransp to transp
; itIsOne to 1=1 )
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Glue; open Helpers public
open import Agda.Builtin.Cubical.Sub public
renaming ( inc to inS
; primSubOut to outS
)
---------------------------------------------------------------------------
-- Foundations
Type = Set
Path : (A : Type) → A → A → Type
Path A a b = PathP (λ _ → A) a b
isProp : Type → Type
isProp A = (x y : A) → x ≡ y
toPathP : {A : I → Type} {x : A i0} {y : A i1} → transp (λ i → A i) i0 x ≡ y → PathP A x y
toPathP {A = A} {x = x} p i =
hcomp (λ j → λ { (i = i0) → x
; (i = i1) → p j })
(transp (λ j → A (i ∧ j)) (~ i) x)
isProp→PathP : ∀ {B : I → Type} → ((i : I) → isProp (B i))
→ (b0 : B i0) (b1 : B i1)
→ PathP (λ i → B i) b0 b1
isProp→PathP hB b0 b1 = toPathP (hB _ _ _)
---------------------------------------------------------------------------
-- Equivalence
-- The identity equivalence
idIsEquiv : (A : Type) → isEquiv (λ (x : A) → x)
idIsEquiv A .equiv-proof y =
(y , refl) , λ z i → z .snd (~ i) , λ j → z .snd (~ i ∨ j)
idEquiv : (A : Type) → A ≃ A
idEquiv A .fst = λ x → x
idEquiv A .snd = idIsEquiv A
isPropIsEquiv : {A B : Type} (f : A → B) → isProp (isEquiv f)
isPropIsEquiv f p q i .equiv-proof y =
let p2 = p .equiv-proof y .snd
q2 = q .equiv-proof y .snd
in p2 (q .equiv-proof y .fst) i
, λ w j → hcomp (λ k → λ { (i = i0) → p2 w j
; (i = i1) → q2 w (j ∨ ~ k)
; (j = i0) → p2 (q2 w (~ k)) i
; (j = i1) → w })
(p2 w (i ∨ j))
equivEq : {A B : Type} {e f : A ≃ B} → (h : e .fst ≡ f .fst) → e ≡ f
equivEq {e = e} {f = f} h i =
h i , isProp→PathP (λ i → isPropIsEquiv (h i)) (e .snd) (f .snd) i
---------------------------------------------------------------------------
-- Univalence
Glue : (A : Type) {φ : I}
→ (Te : Partial φ (Σ Type λ T → T ≃ A))
→ Type
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)
ua : ∀ {A B : Type} → A ≃ B → A ≡ B
ua {A = A} {B = B} e i = Glue B (λ { (i = i0) → (A , e)
; (i = i1) → (B , idEquiv B) })
---------------------------------------------------------------------------
-- Isomorphisms
record Iso (A B : Type) : Type where
no-eta-equality
constructor iso
field
fun : A → B
inv : B → A
rightInv : ∀ b → fun (inv b) ≡ b
leftInv : ∀ a → inv (fun a) ≡ a
-- Any iso is an equivalence
module _ {A B : Type} (i : Iso A B) where
open Iso i renaming ( fun to f
; inv to g
; rightInv to s
; leftInv to t)
private
module _ (y : B) (x0 x1 : A) (p0 : f x0 ≡ y) (p1 : f x1 ≡ y) where
fill0 : I → I → A
fill0 i = hfill (λ k → λ { (i = i1) → t x0 k
; (i = i0) → g y })
(inS (g (p0 (~ i))))
fill1 : I → I → A
fill1 i = hfill (λ k → λ { (i = i1) → t x1 k
; (i = i0) → g y })
(inS (g (p1 (~ i))))
fill2 : I → I → A
fill2 i = hfill (λ k → λ { (i = i1) → fill1 k i1
; (i = i0) → fill0 k i1 })
(inS (g y))
p : x0 ≡ x1
p i = fill2 i i1
sq : I → I → A
sq i j = hcomp (λ k → λ { (i = i1) → fill1 j (~ k)
; (i = i0) → fill0 j (~ k)
; (j = i1) → t (fill2 i i1) (~ k)
; (j = i0) → g y })
(fill2 i j)
sq1 : I → I → B
sq1 i j = hcomp (λ k → λ { (i = i1) → s (p1 (~ j)) k
; (i = i0) → s (p0 (~ j)) k
; (j = i1) → s (f (p i)) k
; (j = i0) → s y k })
(f (sq i j))
lemIso : (x0 , p0) ≡ (x1 , p1)
lemIso i .fst = p i
lemIso i .snd = λ j → sq1 i (~ j)
isoToIsEquiv : isEquiv f
isoToIsEquiv .equiv-proof y .fst .fst = g y
isoToIsEquiv .equiv-proof y .fst .snd = s y
isoToIsEquiv .equiv-proof y .snd z = lemIso y (g y) (fst z) (s y) (snd z)
isoToEquiv : A ≃ B
isoToEquiv .fst = _
isoToEquiv .snd = isoToIsEquiv
---------------------------------------------------------------------------
-- Booleans
notEquiv : Bool ≃ Bool
notEquiv = isoToEquiv (iso not not notnot notnot)
where
not : Bool → Bool
not true = false
not false = true
notnot : ∀ x → not (not x) ≡ x
notnot true = refl
notnot false = refl
---------------------------------------------------------------------------
-- Circle
data S¹ : Type where
base : S¹
loop : base ≡ base
-- rot, used in the Hopf fibration
-- we will denote rotation by _·_
-- it is called μ in the HoTT-book in "8.5.2 The Hopf construction"
rotLoop : (a : S¹) → a ≡ a
rotLoop base = loop
rotLoop (loop i) j =
hcomp (λ k → λ { (i = i0) → loop (j ∨ ~ k)
; (i = i1) → loop (j ∧ k)
; (j = i0) → loop (i ∨ ~ k)
; (j = i1) → loop (i ∧ k)}) base
---------------------------------------------------------------------------
-- Inconsistency distilled from #5838
-- twisted-square : Path (Path Type₀ S¹ S¹) refl refl
twisted-square : (i j : I) → Type
twisted-square i j = Glue S¹ λ
{ (i = i0) → S¹ , equivEq {e = idEquiv S¹} {f = idEquiv S¹} (λ k x → rotLoop x k) j
; (i = i1) → S¹ , idEquiv S¹
; (j = i0) → S¹ , idEquiv S¹
; (j = i1) → S¹ , idEquiv S¹
}
DoubleCover : S¹ → Type
DoubleCover base = Bool
DoubleCover (loop i) = ua notEquiv i
bad : true ≡ false
bad k = transp (λ i → DoubleCover (transp (λ j → twisted-square i j) (k ∧ (i ∨ ~ i)) base)) i0 false |
|
Here is an addendum to Issue5838.agda which shows (I think?) that |
|
@simhu, do you also have a fix for this? The current PR (#5846) implements (hopefully) the fix mentioned in #5755 (comment). |
Yeah, I think that any changes made to transp for Glue should also be made for transp for HCompU. |
andreasabel
added a commit
that referenced
this issue
Mar 25, 2022
andreasabel
added a commit
that referenced
this issue
Mar 25, 2022
This was suggested by Tom Jack and Anders Mörtberg.
andreasabel
added a commit
that referenced
this issue
Mar 27, 2022
- update Cubical reductions according to Simon Huber (jww Christian Sattler and Tom Jack) - port Huber's fix also to @compHCompU DoTransp@ This was suggested by Tom Jack and Anders Mörtberg. - fix comment As requested by Anders M.
andreasabel
added a commit
that referenced
this issue
Mar 27, 2022
- update Cubical reductions according to Simon Huber (jww Christian Sattler and Tom Jack) - port Huber's fix also to @compHCompU DoTransp@ This was suggested by Tom Jack and Anders Mörtberg. - fix comment As requested by Anders M. Conflicts: src/full/Agda/TypeChecking/Primitive/Cubical.hs
andreasabel
added a commit
that referenced
this issue
Mar 27, 2022
andreasabel
added a commit
that referenced
this issue
Mar 27, 2022
- update Cubical reductions according to Simon Huber (jww Christian Sattler and Tom Jack) - port Huber's fix also to @compHCompU DoTransp@ This was suggested by Tom Jack and Anders Mörtberg. - fix comment As requested by Anders M.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I stumbled upon a proof of ⊥ based on computations over univalence. In the example, I am using the cubical library.
I really don't understand anything more about what is going wrong. Is there a bug in transp on Glue when φ is not i0, maybe?
The text was updated successfully, but these errors were encountered: