[Agda] another possible without-K problem

[Nils Anders Danielsson]

On 2013-07-10 17:45, Andreas Abel wrote:
> Do you have a syntactic analysis for hset we could build into Agda?

Let's see:

* 0, 1, and 2 are sets.

* If B x is a set for all x, then Π A B is a set. (Assuming
   extensionality of functions, but I don't see any problems in making
   use of this assumption in the analysis.)

* If A is a set, and B x is a set for all x, then Σ A B is a set.

* If A is a set, then W A B is a set (assuming extensionality).

* If A is a set, then M A B is a set (assuming that bisimilarity for M,
   bisimilarity for bisimilarity for M, and equality are related in a
   certain way).

* If A is a set and x, y : A, then x ≡ y is a set.

* If there is a split surjection (or bijection) from A to B, and A is a
   set, then B is a set.

* Set is /not/ a set (assuming univalence).

The rules above give us a simple, syntactic analysis (if the assumptions
are acceptable). However, this analysis may be too simplistic. One may
for instance want to accept the following code:

   foo : {A : Set} → Is-set A → {xs : List A} → xs ≡ xs → …
   foo _ refl = …

I'm not sure if this spooky action at a distance is a good idea, though.

An alternative may be to add a second argument to Set, so that
"A : Set u h" means that A has universe level u and h-level h (and
Set u h has type Set (suc u) ∞):

   foo : ∀ {a} {A : Set a 2} {xs : List A} → xs ≡ xs → …
   foo refl = …

I'm not sure if this makes sense, but even if it does, I'm still
somewhat reluctant to go down this route.

If we had a version of Epigram that didn't rely on K, then we could
presumably program our own eliminator that worked in those cases in
which we do have a set, and use a polytypic program to establish
set-ness (in many cases). Speculative code:

   foo : (A : Set) → Is-set A → {xs : List A} → xs ≡ xs → …
   foo A A-set p    ⇐ K-case (is-set (List-code (k A)) A-set) p
   foo A A-set refl ⇒ …

-- 
/NAD