File tree Expand file tree Collapse file tree 4 files changed +20
-2
lines changed Expand file tree Collapse file tree 4 files changed +20
-2
lines changed Original file line number Diff line number Diff line change
1
+ * Level polymorphism
2
+
3
+ ` ⊥ ` in ` Data.Empty ` and ` ⊤ ` in ` Data.Unit ` are not ` Level ` -polymorphic as that
4
+ tends to lead to unsolved metas (see discussion at issue #312 ). This is understandable
5
+ as very often the level of (say) ` ⊤ ` is under-determined by its surrounding context,
6
+ leading to unsolved metas. This is frequent enough that it makes sense for the default
7
+ versions to be monomorphic (at Level 0).
8
+
9
+ But there are other cases where exactly the opposite is needed. for that purpose,
10
+ there are level-polymorphic versions in ` Data.Empty.Polymorphic ` and
11
+ ` Data.Unit.Polymorphic ` respectively.
12
+
13
+ The same issue happens in ` Relation.Unary ` which defines ` Ø ` and ` U ` at ` Level ` 0, else
14
+ a lot of unsolved metas appear (for example in ` Relation.Unary.Properties ` ). For that
15
+ purpose, ` Relation.Unary.Polymorphic ` exists.
Original file line number Diff line number Diff line change 1
1
------------------------------------------------------------------------
2
2
-- The Agda standard library
3
3
--
4
- -- Empty type, judgementally proof irrelevant
4
+ -- Empty type, judgementally proof irrelevant, Level-monomorphic
5
5
------------------------------------------------------------------------
6
6
7
7
{-# OPTIONS --cubical-compatible --safe #-}
Original file line number Diff line number Diff line change 1
1
------------------------------------------------------------------------
2
2
-- The Agda standard library
3
3
--
4
- -- The unit type
4
+ -- The unit type, Level-monomorphic version
5
5
------------------------------------------------------------------------
6
6
7
7
{-# OPTIONS --cubical-compatible --safe #-}
Original file line number Diff line number Diff line change @@ -42,6 +42,8 @@ Pred A ℓ = A → Set ℓ
42
42
-- Special sets
43
43
44
44
-- The empty set.
45
+ -- Explicitly not level polymorphic as this often causes unsolved metas;
46
+ -- see `Relation.Unary.Polymorphic` for a level-polymorphic version.
45
47
46
48
∅ : Pred A 0ℓ
47
49
∅ = λ _ → ⊥
@@ -52,6 +54,7 @@ Pred A ℓ = A → Set ℓ
52
54
{ x } = x ≡_
53
55
54
56
-- The universal set.
57
+ -- Explicitly not level polymorphic (see comments for `∅` for more details)
55
58
56
59
U : Pred A 0ℓ
57
60
U = λ _ → ⊤
You can’t perform that action at this time.
0 commit comments