In the theory, the rule looks like this:
A = : \Type0=C2=A0 =C2=A0 p : isSet A
-------------------------------= ---
=C2=A0 =C2=A0 =C2=A0 F(A,p) : \Set0

= and we also add an equivalence between A and F(A,p). In the actual implemen= tation, you can do this using \use \level construction. If you can prove th= at some \data or \record satisfies isSet (or, more generally, that it is an= n-type), then you can put this proof in \use \level function corresponding= to this definition and it will be put in the corresponding universe. So, y= ou can define \data F(A,p) with one constructor with one parameter of type = A and put it in \Set0.

Regards,
Valery Isaev

=D1=81=D0=B1, 10 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 12= :47, Michael Shulman <shulman@sa= ndiego.edu>:
On Thu, Aug 8, 2019 at 2:56 AM Valery Isaev <valery.isaev@gmail.com> wrote:<= br> > You can say that they are hidden in the background, but I prefer to th= ink about this in a different way. I think about \Set0 as a strict subtype = of \Type0. In comparison, the type \Sigma (A : \Type0) (isSet A) is only ho= motopically embeds into \Type0. It is equivalent to \Set0, but not isomorph= ic to it. In particular, this means that every type in \Set0 satisfies isSe= t and every type in \Type0 which satisfies isSet is equivalent to some type= in \Set0, but not necessarily belongs to \Set0 itself. So, if we have (1),= we also have (2) and we do not have (3). It may be true that A is a 2-type= , which means that there is a type A' : \2-Type 1 equivalent to A, but = A itself does not belong to \2-Type 1.

How do you ensure that "every type in \Type0 which satisfies isSet is<= br> equivalent to some type in \Set0"?=C2=A0 Is it just an axiom?

Also, since \Prop "has no predicative level", does this property<= br> applied to \Prop imply that propositional resizing holds?

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https= ://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520fuDN9yffbCT6Hxv9kvB%3= DWW%2BiUcTf%3DJuXi7kuD5NknWbfg%40mail.gmail.com.
--000000000000f8b54b058fc27772--