# [Agda] another possible without-K problem

Nils Anders Danielsson nad at cse.gu.se
Fri Aug 23 11:31:50 CEST 2013

```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 ⇒ …

--