<div dir="ltr">In Coq we have been experimenting with the use of type classes to automatically derive that something is an hSet/n-Type.<br><br>For instance, this allows us to automatically derive that e.g. nat*nat is a again a set.<br>

<pre><div class="" id="LC231"><span class="">Instance</span> <span class="">trunc_prod</span> <span class="">`{</span><span class="">IsTrunc</span> <span class="">n</span> <span class="">A</span><span class="">}</span> <span class="">`{</span><span class="">IsTrunc</span> <span class="">n</span> <span class="">B</span><span class="">}</span> <span class="">:</span> <span class="">IsTrunc</span> <span class="">n</span> <span class="">(</span><span class="">A</span> <span class="">*</span> <span class="">B</span><span class="">)</span> <span class="">|</span> <span class="">100</span><span class="">.</span><br>

</div></pre><a href="https://github.com/HoTT/HoTT/blob/master/theories/types/Prod.v">https://github.com/HoTT/HoTT/blob/master/theories/types/Prod.v</a><br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Aug 23, 2013 at 11:31 AM, Nils Anders Danielsson <span dir="ltr">&lt;<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 2013-07-10 17:45, Andreas Abel wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Do you have a syntactic analysis for hset we could build into Agda?<br>
</blockquote>
<br>
Let&#39;s see:<br>
<br>
* 0, 1, and 2 are sets.<br>
<br>
* If B x is a set for all x, then Π A B is a set. (Assuming<br>
  extensionality of functions, but I don&#39;t see any problems in making<br>
  use of this assumption in the analysis.)<br>
<br>
* If A is a set, and B x is a set for all x, then Σ A B is a set.<br>
<br>
* If A is a set, then W A B is a set (assuming extensionality).<br>
<br>
* If A is a set, then M A B is a set (assuming that bisimilarity for M,<br>
  bisimilarity for bisimilarity for M, and equality are related in a<br>
  certain way).<br>
<br>
* If A is a set and x, y : A, then x ≡ y is a set.<br>
<br>
* If there is a split surjection (or bijection) from A to B, and A is a<br>
  set, then B is a set.<br>
<br>
* Set is /not/ a set (assuming univalence).<br>
<br>
The rules above give us a simple, syntactic analysis (if the assumptions<br>
are acceptable). However, this analysis may be too simplistic. One may<br>
for instance want to accept the following code:<br>
<br>
  foo : {A : Set} → Is-set A → {xs : List A} → xs ≡ xs → …<br>
  foo _ refl = …<br>
<br>
I&#39;m not sure if this spooky action at a distance is a good idea, though.<br>
<br>
An alternative may be to add a second argument to Set, so that<br>
&quot;A : Set u h&quot; means that A has universe level u and h-level h (and<br>
Set u h has type Set (suc u) ∞):<br>
<br>
  foo : ∀ {a} {A : Set a 2} {xs : List A} → xs ≡ xs → …<br>
  foo refl = …<br>
<br>
I&#39;m not sure if this makes sense, but even if it does, I&#39;m still<br>
somewhat reluctant to go down this route.<br>
<br>
If we had a version of Epigram that didn&#39;t rely on K, then we could<br>
presumably program our own eliminator that worked in those cases in<br>
which we do have a set, and use a polytypic program to establish<br>
set-ness (in many cases). Speculative code:<br>
<br>
  foo : (A : Set) → Is-set A → {xs : List A} → xs ≡ xs → …<br>
  foo A A-set p    ⇐ K-case (is-set (List-code (k A)) A-set) p<br>
  foo A A-set refl ⇒ …<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>