Extracted from #5948:
{-# OPTIONS --prop --cumulativity #-}
-- This combination of options breaks canonicity.
-- Counterexample by Szumi, based on a fragment by Andreas.
-- Issue #5948 discussion, 2024-09-18.
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
data Foo : Prop where
tt ff : Foo
-- Outright matching on Foo is rejected.
-- rejected : Foo → Bool
-- rejected tt = true
-- rejected ff = false
-- -- Cannot split on datatype in Prop unless target is in Prop
-- -- when checking that the pattern tt has type Foo
-- But we can sneak it in via Prop <= Set cumulativity:
Boo : Set
Boo = Foo
allowed : Boo → Bool
allowed tt = true
allowed ff = false
foo-to-boo : Foo → Boo
foo-to-boo x = x
f : Foo → Bool
f x = allowed (foo-to-boo x)
-- This leads to non-canoncial booleans.
_ : f tt ≡ true
_ = refl
-- Error: allowed _ != true of type Bool
Coq does not have SProp <= Type, according to https://coq.inria.fr/doc/V8.18.0/refman/language/cic.html#subtyping-rules:
note: SProp is not related by cumulativity to any other term
They have Prop <= Type though but I vaguely remember some talk in the 2000s that this isn't entirely unproblematic either. (I couldn't easily google something on this, though.)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4