[Agda] another possible without-K problem

[Bas Spitters]

In Coq we have been experimenting with the use of type classes to
automatically derive that something is an hSet/n-Type.

For instance, this allows us to automatically derive that e.g. nat*nat is a
again a set.

Instance trunc_prod `{IsTrunc n A} `{IsTrunc n B} : IsTrunc n (A * B) | 100.

https://github.com/HoTT/HoTT/blob/master/theories/types/Prod.v


On Fri, Aug 23, 2013 at 11:31 AM, Nils Anders Danielsson <nad at cse.gu.se>wrote:

> 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
>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130823/3909cd44/attachment.html