about the HTS

about the HTS

[Vladimir Voevodsky]

Just a thought… Can we devise a version of the HTS where exact equality types are not available for the universes such that, even with the exact equality, HTS would remain a univalent theory.

Maybe only some types should be equipped with the exact equality and this should be a special quality of types.

Vladimir.

PS If there are higher inductive types then the exact equality should not be available for them either. 

Re: [HoTT] about the HTS

[Benedikt Ahrens]

On 02/23/2017 03:47 PM, Vladimir Voevodsky wrote:
> Just a thought… Can we devise a version of the HTS where exact
> equality types are not available for the universes such that, even
> with the exact equality, HTS would remain a univalent theory.
> 
> Maybe only some types should be equipped with the exact equality and
> this should be a special quality of types.
> 
> Vladimir.
> 
> PS If there are higher inductive types then the exact equality should
> not be available for them either.


Paolo Capriotti, in his PhD thesis "Models of Type Theory with Strict
Equality" [1], has studied strict equality in type theory.

From page 69:

"Finally, universes in the strict fragment of our system are not assumed
to be fibrant types, like in HTS."

You might be interested in Section 4.1.1, "Differences with HTS".

[1] https://arxiv.org/abs/1702.04912

Re: [HoTT] about the HTS

[Vladimir Voevodsky]

I could not find where he defines the univalent (intensional) equality. It seems that all his equalities are strict.


> On Feb 23, 2017, at 9:57 AM, Benedikt Ahrens <benedik...@gmail.com> wrote:
> 
> 
> 
> On 02/23/2017 03:47 PM, Vladimir Voevodsky wrote:
>> Just a thought… Can we devise a version of the HTS where exact
>> equality types are not available for the universes such that, even
>> with the exact equality, HTS would remain a univalent theory.
>> 
>> Maybe only some types should be equipped with the exact equality and
>> this should be a special quality of types.
>> 
>> Vladimir.
>> 
>> PS If there are higher inductive types then the exact equality should
>> not be available for them either.
> 
> 
> Paolo Capriotti, in his PhD thesis "Models of Type Theory with Strict
> Equality" [1], has studied strict equality in type theory.
> 
>> From page 69:
> 
> "Finally, universes in the strict fragment of our system are not assumed
> to be fibrant types, like in HTS."
> 
> You might be interested in Section 4.1.1, "Differences with HTS".
> 
> [1] https://arxiv.org/abs/1702.04912
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] about the HTS

[Benedikt Ahrens]

Section 1.4.8 "Equality" gives an informal account and points to several
precise definitions.
On page 43 two equality types are considered, one intensional one and
one with reflection rule.

Maybe Paolo (in CC) can explain his setup himself.

On 02/23/2017 07:08 PM, Vladimir Voevodsky wrote:
> I could not find where he defines the univalent (intensional)
> equality. It seems that all his equalities are strict.
> 
> 
>> On Feb 23, 2017, at 9:57 AM, Benedikt Ahrens
>> <benedik...@gmail.com> wrote:
>> 
>> 
>> 
>> On 02/23/2017 03:47 PM, Vladimir Voevodsky wrote:
>>> Just a thought… Can we devise a version of the HTS where exact 
>>> equality types are not available for the universes such that,
>>> even with the exact equality, HTS would remain a univalent
>>> theory.
>>> 
>>> Maybe only some types should be equipped with the exact equality
>>> and this should be a special quality of types.
>>> 
>>> Vladimir.
>>> 
>>> PS If there are higher inductive types then the exact equality
>>> should not be available for them either.
>> 
>> 
>> Paolo Capriotti, in his PhD thesis "Models of Type Theory with
>> Strict Equality" [1], has studied strict equality in type theory.
>> 
>>> From page 69:
>> 
>> "Finally, universes in the strict fragment of our system are not
>> assumed to be fibrant types, like in HTS."
>> 
>> You might be interested in Section 4.1.1, "Differences with HTS".
>> 
>> [1] https://arxiv.org/abs/1702.04912
>> 
>> -- You received this message because you are subscribed to the
>> Google Groups "Homotopy Type Theory" group. To unsubscribe from
>> this group and stop receiving emails from it, send an email to
>> HomotopyTypeThe...@googlegroups.com. For more options,
>> visit https://groups.google.com/d/optout.
> 

Re: [HoTT] about the HTS

[Vladimir Voevodsky]

BTW It is a little dangerous to define presheaves as functors C -> Sets^{op}. While it gives the correct objects, the morphisms between presheaves are not morphisms in the category of functors C -> Sets^{op} but in the opposite category.


> On Feb 23, 2017, at 1:52 PM, Benedikt Ahrens <benedik...@gmail.com> wrote:
> 
> Section 1.4.8 "Equality" gives an informal account and points to several
> precise definitions.
> On page 43 two equality types are considered, one intensional one and
> one with reflection rule.
> 
> Maybe Paolo (in CC) can explain his setup himself.
> 
> On 02/23/2017 07:08 PM, Vladimir Voevodsky wrote:
>> I could not find where he defines the univalent (intensional)
>> equality. It seems that all his equalities are strict.
>> 
>> 
>>> On Feb 23, 2017, at 9:57 AM, Benedikt Ahrens
>>> <benedik...@gmail.com> wrote:
>>> 
>>> 
>>> 
>>> On 02/23/2017 03:47 PM, Vladimir Voevodsky wrote:
>>>> Just a thought… Can we devise a version of the HTS where exact 
>>>> equality types are not available for the universes such that,
>>>> even with the exact equality, HTS would remain a univalent
>>>> theory.
>>>> 
>>>> Maybe only some types should be equipped with the exact equality
>>>> and this should be a special quality of types.
>>>> 
>>>> Vladimir.
>>>> 
>>>> PS If there are higher inductive types then the exact equality
>>>> should not be available for them either.
>>> 
>>> 
>>> Paolo Capriotti, in his PhD thesis "Models of Type Theory with
>>> Strict Equality" [1], has studied strict equality in type theory.
>>> 
>>>> From page 69:
>>> 
>>> "Finally, universes in the strict fragment of our system are not
>>> assumed to be fibrant types, like in HTS."
>>> 
>>> You might be interested in Section 4.1.1, "Differences with HTS".
>>> 
>>> [1] https://arxiv.org/abs/1702.04912
>>> 
>>> -- You received this message because you are subscribed to the
>>> Google Groups "Homotopy Type Theory" group. To unsubscribe from
>>> this group and stop receiving emails from it, send an email to
>>> HomotopyTypeThe...@googlegroups.com. For more options,
>>> visit https://groups.google.com/d/optout.
>> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [UniMath] Re: [HoTT] about the HTS

[Vladimir Voevodsky]

The slice category over P is equivalent to presheaves on the category of elements of P. What is your definition of the category of elements of $P$? Objects are pairs $(X:C,p:P(X))$, and morphisms from $(X,p)$ to $(X’,p’)$ are…?

> On Feb 24, 2017, at 9:33 AM, Paolo Capriotti <pa...@capriotti.io> wrote:
> 
>>> On Feb 23, 2017, at 1:52 PM, Benedikt Ahrens <benedik...@gmail.com> wrote:
>>> Section 1.4.8 "Equality" gives an informal account and points to several
>>> precise definitions.
>>> On page 43 two equality types are considered, one intensional one and
>>> one with reflection rule.
> 
> I haven't actually considered something like what Vladimir suggested, though.  In the systems that I described in my thesis, exact equality is defined for every type.
> 
> Vladimir Voevodsky writes:
>> BTW It is a little dangerous to define presheaves as functors C -> Sets^{op}. While it gives the correct objects, the morphisms between presheaves are not morphisms in the category of functors C -> Sets^{op} but in the opposite category.
> 
> Ah, right.  The reason why I defined presheaves this way is that you can just say that the slice category over a presheaf $P$ is presheaves over the category of elements of $P$, rather than copresheaves, so it's more uniform and certain proofs become a little bit nicer.  Of course, one could start with C^{op} and use copresheaves throughout, but then I think things would get quite confusing with the Yoneda embedding.
> 
> But thanks for pointing out this problem.  Somehow, it had never occured to me that natural transformations are going in the wrong direction with my definition.
> 
> Paolo
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Univalent Mathematics" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to univalent-mathem...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at https://groups.google.com/group/univalent-mathematics.
> To view this discussion on the web visit https://groups.google.com/d/msgid/univalent-mathematics/87k28fek09.fsf%40capriotti.io.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] about the HTS

[Paolo Capriotti]

[-- Attachment #1.1: Type: text/plain, Size: 1343 bytes --]

>> On Feb 23, 2017, at 1:52 PM, Benedikt Ahrens 
>> <benedik...@gmail.com> wrote:
>> 
>> Section 1.4.8 "Equality" gives an informal account and points 
>> to several
>> precise definitions.
>> On page 43 two equality types are considered, one intensional 
>> one and
>> one with reflection rule.

I haven't actually considered something like what Vladimir 
suggested, though.  In the systems that I described in my thesis, 
exact equality is defined for every type.

Vladimir Voevodsky writes:
> BTW It is a little dangerous to define presheaves as functors C 
> -> Sets^{op}. While it gives the correct objects, the morphisms 
> between presheaves are not morphisms in the category of functors 
> C -> Sets^{op} but in the opposite category.

Ah, right.  The reason why I defined presheaves this way is that 
you can just say that the slice category over a presheaf $P$ is 
presheaves over the category of elements of $P$, rather than 
copresheaves, so it's more uniform and certain proofs become a 
little bit nicer.  Of course, one could start with C^{op} and use 
copresheaves throughout, but then I think things would get quite 
confusing with the Yoneda embedding.

But thanks for pointing out this problem.  Somehow, it had never 
occured to me that natural transformations are going in the wrong 
direction with my definition.

Paolo


[-- Attachment #1.2: Type: text/html, Size: 1844 bytes --]

Re: [UniMath] Re: [HoTT] about the HTS

[Paolo Capriotti]

[-- Attachment #1.1: Type: text/plain, Size: 877 bytes --]

Vladimir Voevodsky writes:
> The slice category over P is equivalent to presheaves on the category of 
elements of P. What is your definition of the category of elements of $P$? 
Objects are pairs $(X:C,p:P(X))$, and morphisms from $(X,p)$ to $(X’,p’)$ 
are…?

...morphisms $f : C(X',X)$ such that $Pf(p) = p'$.

The slice category of the category of functors $A -> Set$ over a functor 
$F$ is equivalent to functors $el(F) -> Set$, right?  Now if you define 
presheaves as functors $C^{op} -> Set$, you get that presheaves on $C$ over 
a presheaf $P$ are equivalent to *functors* $el(P) -> Set$, not presheaves 
on $el(P)$.

That's why I was trying to be clever and use that unnatural definition of 
presheaves, but, as you pointed out, that doesn't work either, because the 
resulting category of presheaves is the opposite of what we want.

Paolo


[-- Attachment #1.2: Type: text/html, Size: 1031 bytes --]

Re: [UniMath] Re: [HoTT] about the HTS

[Vladimir Voevodsky]

[-- Attachment #1: Type: text/plain, Size: 2133 bytes --]

Our definition of the category of elements (cf. ElementsOp.v in UniMath/UniMath/Ktheory), and I think it is the standard one, is that morphisms are morphisms f:X -> X’ such that  p=P(f)(p’). Then all works as expected.


> On Feb 24, 2017, at 10:06 AM, Paolo Capriotti <p.cap...@gmail.com> wrote:
> 
> Vladimir Voevodsky writes:
> > The slice category over P is equivalent to presheaves on the category of elements of P. What is your definition of the category of elements of $P$? Objects are pairs $(X:C,p:P(X))$, and morphisms from $(X,p)$ to $(X’,p’)$ are…?
> 
> ...morphisms $f : C(X',X)$ such that $Pf(p) = p'$.
> 
> The slice category of the category of functors $A -> Set$ over a functor $F$ is equivalent to functors $el(F) -> Set$, right?  Now if you define presheaves as functors $C^{op} -> Set$, you get that presheaves on $C$ over a presheaf $P$ are equivalent to *functors* $el(P) -> Set$, not presheaves on $el(P)$.
> 
> That's why I was trying to be clever and use that unnatural definition of presheaves, but, as you pointed out, that doesn't work either, because the resulting category of presheaves is the opposite of what we want.
> 
> Paolo
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Univalent Mathematics" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to univalent-mathem...@googlegroups.com <mailto:univalent-mathem...@googlegroups.com>.
> To post to this group, send email to univalent-...@googlegroups.com <mailto:univalent-...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/univalent-mathematics <https://groups.google.com/group/univalent-mathematics>.
> To view this discussion on the web visit https://groups.google.com/d/msgid/univalent-mathematics/ebf61361-d581-4a25-98cf-0e345e2e2035%40googlegroups.com <https://groups.google.com/d/msgid/univalent-mathematics/ebf61361-d581-4a25-98cf-0e345e2e2035%40googlegroups.com?utm_medium=email&utm_source=footer>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 3158 bytes --]

Re: [HoTT] about the HTS

[Thierry Coquand]

[-- Attachment #1: Type: text/plain, Size: 1819 bytes --]

 Here is note <http://www.cse.chalmers.se/~coquand/bishop.pdf> which should be connected to this message. It contains first a self contained
presentation of the cubical set model, and then a notion of “Bishop set” which corresponds
to the fact that any two paths between the same end points are -judgmentally- equal.
One defines a subpresheaf of the universe which classifies these sets, and  one notices
that this notion is closed by the Kan filling operation of the universe (because this is defined
in term of glueing, and this notion is closed by the glueing operation), and hence it is fibrant
(and univalent).

 If this is correct, one expects a corresponding type system with decidable type-checking, and
connections with what has
been done in observational type theory (and it will be interesting to see if this can also be connected
to the more recent work of Thorsten et al.) while staying in a univalent theory.
 Thierry


On 23 Feb 2017, at 15:47, Vladimir Voevodsky <vlad...@ias.edu<mailto:vlad...@ias.edu>> wrote:

Just a thought… Can we devise a version of the HTS where exact equality types are not available for the universes such that, even with the exact equality, HTS would remain a univalent theory.

Maybe only some types should be equipped with the exact equality and this should be a special quality of types.

Vladimir.

PS If there are higher inductive types then the exact equality should not be available for them either.

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.


[-- Attachment #2: Type: text/html, Size: 2906 bytes --]

Re: [UniMath] [HoTT] about the HTS

[Vladimir Voevodsky]

[-- Attachment #1: Type: text/plain, Size: 353 bytes --]


> On Feb 25, 2017, at 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:
> 
>  “Bishop set” which corresponds
> to the fact that any two paths between the same end points are -judgmentally- equal.

This is not what I mean by a strict set. A strict set is a Bishop set where any two points connected by a path are judgmentally equal.



[-- Attachment #2: Type: text/html, Size: 1531 bytes --]

Re: [UniMath] [HoTT] about the HTS

[Vladimir Voevodsky]

[-- Attachment #1: Type: text/plain, Size: 875 bytes --]

BTW, even if the universe of strict sets is not fibrant we can still have a judgement that something is a strict set and the rule that a = b implies a is definitionally equal to b if a and b are elements of a strict set.

It is such a structure that would make many things very convenient. 

It is non- clear to, however, why typing would be decidable in such a system.

Vladimir.




> On Feb 27, 2017, at 1:50 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> 
> 
>> On Feb 25, 2017, at 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> wrote:
>> 
>>  “Bishop set” which corresponds
>> to the fact that any two paths between the same end points are -judgmentally- equal.
> 
> This is not what I mean by a strict set. A strict set is a Bishop set where any two points connected by a path are judgmentally equal.
> 
> 


[-- Attachment #2: Type: text/html, Size: 2686 bytes --]

Re: [UniMath] [HoTT] about the HTS

[Thierry Coquand]

[-- Attachment #1: Type: text/plain, Size: 1884 bytes --]


Exactly.


 In my note, I consider three universes (all fibrant)


 sProp

 sSet

 bSet


 sProp sub-presheaf of sSet sub-presheaf bSet sub-presheaf U


 They correspond to 3 properties


 G |- A sprop

 G |- A sset

 G |- A bset


that can be described semantically in a simple way.


 For sprop and sset, to have a fibration structure is a property

and


 G |- A sset and fibrant


should correspond to the notion of covering space.


 But sSet does not correspond to a decidable type system, while

it should be the case that sProp and bSet corresponds to a decidable

type system.


 At least with bSet we validate axiom K and all developments that have

been done using this axiom.




________________________________
From: Vladimir Voevodsky <vlad...@ias.edu>
Sent: Monday, February 27, 2017 7:53 PM
To: Thierry Coquand
Cc: Prof. Vladimir Voevodsky; univalent-...@googlegroups.com; homotopytypetheory
Subject: Re: [UniMath] [HoTT] about the HTS

BTW, even if the universe of strict sets is not fibrant we can still have a judgement that something is a strict set and the rule that a = b implies a is definitionally equal to b if a and b are elements of a strict set.

It is such a structure that would make many things very convenient.

It is non- clear to, however, why typing would be decidable in such a system.

Vladimir.




On Feb 27, 2017, at 1:50 PM, Vladimir Voevodsky <vlad...@ias.edu<mailto:vlad...@ias.edu>> wrote:


On Feb 25, 2017, at 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se<mailto:Thierry...@cse.gu.se>> wrote:

 "Bishop set" which corresponds
to the fact that any two paths between the same end points are -judgmentally- equal.

This is not what I mean by a strict set. A strict set is a Bishop set where any two points connected by a path are judgmentally equal.




[-- Attachment #2: Type: text/html, Size: 4535 bytes --]

Re: [UniMath] [HoTT] about the HTS

[Vladimir Voevodsky]

[-- Attachment #1: Type: text/plain, Size: 2620 bytes --]

We also validate axiom K with the hSet, as far as I understand.

BTW why do you call elements of bSet Bishop sets?


> On Feb 27, 2017, at 1:58 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:
> 
> 
> Exactly.
> 
>  In my note, I consider three universes (all fibrant)
> 
>  sProp 
>  sSet
>  bSet
> 
>  sProp sub-presheaf of sSet sub-presheaf bSet sub-presheaf U
> 
>  They correspond to 3 properties
> 
>  G |- A sprop
>  G |- A sset
>  G |- A bset
> 
> that can be described semantically in a simple way.
> 
>  For sprop and sset, to have a fibration structure is a property
> and 
> 
>  G |- A sset and fibrant
> 
> should correspond to the notion of covering space.
> 
>  But sSet does not correspond to a decidable type system, while
> it should be the case that sProp and bSet corresponds to a decidable
> type system.
> 
>  At least with bSet we validate axiom K and all developments that have
> been done using this axiom.
> 
> 
> 
> 
> From: Vladimir Voevodsky <vlad...@ias.edu <mailto:vlad...@ias.edu>>
> Sent: Monday, February 27, 2017 7:53 PM
> To: Thierry Coquand
> Cc: Prof. Vladimir Voevodsky; univalent-...@googlegroups.com <mailto:univalent-...@googlegroups.com>; homotopytypetheory
> Subject: Re: [UniMath] [HoTT] about the HTS
>  
> BTW, even if the universe of strict sets is not fibrant we can still have a judgement that something is a strict set and the rule that a = b implies a is definitionally equal to b if a and b are elements of a strict set.
> 
> It is such a structure that would make many things very convenient. 
> 
> It is non- clear to, however, why typing would be decidable in such a system.
> 
> Vladimir.
> 
> 
> 
> 
>> On Feb 27, 2017, at 1:50 PM, Vladimir Voevodsky <vlad...@ias.edu <mailto:vlad...@ias.edu>> wrote:
>> 
>> 
>>> On Feb 25, 2017, at 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> wrote:
>>> 
>>>  “Bishop set” which corresponds
>>> to the fact that any two paths between the same end points are -judgmentally- equal.
>> 
>> This is not what I mean by a strict set. A strict set is a Bishop set where any two points connected by a path are judgmentally equal.
>> 
>> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 12430 bytes --]

Re: [UniMath] [HoTT] about the HTS

[Thierry Coquand]

> We also validate axiom K with the hSet, as far as I understand.
> 
> BTW why do you call elements of bSet Bishop sets?

 If G |- A is a fibration and A is a strict set then the fibers over any point
can be thought of as ordinary sets (all paths are constant paths), and we have unique path lifting
property (like for covering space).
 
 If G |- A is a fibration and A is a “Bishop” set, then the fibers over any
point can be thought of as graphs of equivalence relations
(the paths don’t need to be constant, but there is at most one
path between two points, and more generally all cubes are determined
by its vertices).
This is quite close to how Bishop defined a set: a set is defined
by a collection of elements with an equivalence relation.
If we furthermore look at a fibration of “Bishop” sets this corresponds
exactly to the notion of family of sets as defined by Richman
in his book on constructive algebra (or in the book by Bishop and
Bridges Exercise 3.2).

 In any case, both notions of strict sets and “Bishop” sets
give rise to sub-presheaves of the first universe and we have sSet sub-presheaf bSet.
 
 There is also a sub-presheaf of “strict” propositions, which justifies
the rule

    G |- A sProp    G |- a0 : A      G |- a1: A
 ———————————————————
             G |- a0 = a1 : A

(but this type sProp is probably not equivalent in general to the type
of hPropositions)



 Both sSet and bSet should be closed by sum and product types.

  However, they are not closed by quotient (even by propositional truncation)
in general.

   Indeed axiom K is already validated with hSets.

  Maybe the notion of sProp, and bSet is interesting since it should keep conversion
and type-checking decidable, and simplify some proofs, and some computations
by introducing judgmental proof irrelevance (so that we know that we don’t need
to consider some part of a term for computation and conversion).

 In any case, if all this is correct, it is interesting that we can keep some ideas of HTS
(with sSet or bSet) and still be in an univalent framework.

     Thierry

HIT

[Thierry Coquand]

[-- Attachment #1: Type: text/plain, Size: 682 bytes --]

  For completness, I wrote here<http://www.cse.chalmers.se/~coquand/fac.pdf> the semantics of some HIT (the circle and the
trivial cofibration-fibration factorisation of a map) in constructive set theory.
Since one has to define inductively at the same time a family of sets and
suitable maps between these sets, this is an example of an indexed
inductive-recursive definition, and one can follow Stuart Allen’s idea
(LICS 1987) of defining by induction instead relations which should represent
the -graphs- of these functions, and prove then by induction that these are functional graphs.
(This replaces the transfinite induction of the small object argument.)
 Thierry

[-- Attachment #2: Type: text/html, Size: 1146 bytes --]

Re: about the HTS

[Matt Oliveri]

[-- Attachment #1.1: Type: text/plain, Size: 579 bytes --]

So the answer was yes, right? Problem solved?

On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:
>
> Just a thought… Can we devise a version of the HTS where exact equality 
> types are not available for the universes such that, even with the exact 
> equality, HTS would remain a univalent theory. 
>
> Maybe only some types should be equipped with the exact equality and this 
> should be a special quality of types. 
>
> Vladimir. 
>
> PS If there are higher inductive types then the exact equality should not 
> be available for them either.
>

[-- Attachment #1.2: Type: text/html, Size: 721 bytes --]

Re: [HoTT] about the HTS

[Thierry Coquand]

[-- Attachment #1: Type: text/plain, Size: 1597 bytes --]


If my note was correct, it describes in the cubical set model two univalent universes
(subpresheaf of the first universe)  that satisfy

 (1)   if   A : sSet    and   p : Path A a b   then   a = b : A  and p is the constant path a
(equality reflection rule)

 (2)   if A : bSet and p and q of type Path A a b   then p = q : Path A a b
(judgemental form of UIP)

 Maybe (1) or (2) could be used instead of HTS (and we would remain in an univalent
theory, where all types are fibrant)

 For testing this, one question is:  can we define semi-simplicial types in (1)? in (2)?

 Best regards,
 Thierry



On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com<mailto:atm...@gmail.com>> wrote:

So the answer was yes, right? Problem solved?

On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:
Just a thought… Can we devise a version of the HTS where exact equality types are not available for the universes such that, even with the exact equality, HTS would remain a univalent theory.

Maybe only some types should be equipped with the exact equality and this should be a special quality of types.

Vladimir.

PS If there are higher inductive types then the exact equality should not be available for them either.

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.


[-- Attachment #2: Type: text/html, Size: 3127 bytes --]

Re: [HoTT] about the HTS

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 2944 bytes --]

1. As Thierry pointed out previously, the problem with sSet is that if we postulate that nat:sSet, then for any (small) type T, the function type T -> nat is in sSet, e.g. nat -> nat is in sSet.

Since it is possible to construct two elements of nat -> nat the equality between which is an undecidable proposition, it implies that the definitional equality in any sufficiently advanced type system with sSet and nat:sSet is undecidable.

That means that witnesses, in some language, of definitional equality need to be carried around and therefore the design of a proof assistant where the proof term is the proof is not possible in this system.

2. It is not so clear what would happen with only bSet and nat:bSet.

Vladimir.





> On Mar 22, 2017, at 5:49 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:
> 
> 
> If my note was correct, it describes in the cubical set model two univalent universes
> (subpresheaf of the first universe)  that satisfy
> 
>  (1)   if   A : sSet    and   p : Path A a b   then   a = b : A  and p is the constant path a
> (equality reflection rule)
> 
>  (2)   if A : bSet and p and q of type Path A a b   then p = q : Path A a b
> (judgemental form of UIP)
> 
>  Maybe (1) or (2) could be used instead of HTS (and we would remain in an univalent
> theory, where all types are fibrant)
> 
>  For testing this, one question is:  can we define semi-simplicial types in (1)? in (2)?
> 
>  Best regards,
>  Thierry
> 
> 
> 
>> On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com <mailto:atm...@gmail.com>> wrote:
>> 
>> So the answer was yes, right? Problem solved?
>> 
>> On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:
>> Just a thought… Can we devise a version of the HTS where exact equality types are not available for the universes such that, even with the exact equality, HTS would remain a univalent theory.
>> 
>> Maybe only some types should be equipped with the exact equality and this should be a special quality of types.
>> 
>> Vladimir.
>> 
>> PS If there are higher inductive types then the exact equality should not be available for them either.
>> 
>> --
>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
> 
> 
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #1.2: Type: text/html, Size: 5207 bytes --]

[-- Attachment #2: Message signed with OpenPGP --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] about the HTS

[Matt Oliveri]

[-- Attachment #1.1: Type: text/plain, Size: 5154 bytes --]

Thanks.

I agree that with the sSet option, with an equality reflection rule, it 
would be infeasible to check judgments without extra stuff from outside the 
type theory proper. But what's wrong with that? We add extra stuff anyway, 
like type classes, proof scripts, and implicit arguments. To me, it seems 
that the practical concern of checking the truth of judgments does not need 
to be solved by the design of the core type theory. Indeed, it seems like 
better separation of concerns *not* to solve it there.

Anyway, my understanding of bSet, from what Thierry Coquand said, is that 
it'd be a more OTT-like version of sSet, which is more ETT-like. So instead 
of paths between bSets being reflectable to judgmental equalities, they 
would be "strict propositions" (sProp), whose elements are not only all 
(typally) equal, but they also have no computational content. So any 
"transport" across a strict equality reduces away, as long as it doesn't 
change the type. (It doesn't have to be (judgmentally equal to) 
reflexivity.)

I figure the idea is that bSet should be able to do everything sSet can, 
just with extra computationally-irrelevant transports thrown in to appease 
a decidable type checker.

I don't actually see how either of these universes would help define 
semi-simplicial types. I didn't realize that was the goal here. I thought 
we were just trying to make set-level math more convenient.

-----------

Though I haven't given it a serious thinking-about, I figured that stuff 
with cohesion would be a good way to make semi-simplicial types definable, 
without adding non-fibrant types. 
(https://homotopytypetheory.org/2015/09/25/realcohesion/) It sounded like 
cohesion gives you a set-level view of non-hsets, so I figured you should 
be able to use strict equality in the construction of non-hsets that way.

I suppose strict sets and cohesion can be combined. A set-level view of 
things should yield only strict sets, not arbitrary hsets. (I guess that 
requires a whole hierarchy of strict set universes. But unlike HTS, they're 
all "included" in the univalent universes, not the other way around.)

On Wednesday, March 22, 2017 at 5:01:16 PM UTC-4, v v wrote:
>
> 1. As Thierry pointed out previously, the problem with sSet is that if we 
> postulate that nat:sSet, then for any (small) type T, the function type T 
> -> nat is in sSet, e.g. nat -> nat is in sSet.
>
> Since it is possible to construct two elements of nat -> nat the equality 
> between which is an undecidable proposition, it implies that the 
> definitional equality in any sufficiently advanced type system with sSet 
> and nat:sSet is undecidable.
>
> That means that witnesses, in some language, of definitional equality need 
> to be carried around and therefore the design of a proof assistant where 
> the proof term is the proof is not possible in this system.
>
> 2. It is not so clear what would happen with only bSet and nat:bSet. 
>
> Vladimir.
>
>
>
>
>
> On Mar 22, 2017, at 5:49 PM, Thierry Coquand <Thier...@cse.gu.se 
> <javascript:>> wrote:
>
>
> If my note was correct, it describes in the cubical set model two 
> univalent universes
> (subpresheaf of the first universe)  that satisfy
>
>  (1)   if   A : sSet    and   p : Path A a b   then   a = b : A  and p is 
> the constant path a
> (equality reflection rule)
>
>  (2)   if A : bSet and p and q of type Path A a b   then p = q : Path A a b
> (judgemental form of UIP)
>
>  Maybe (1) or (2) could be used instead of HTS (and we would remain in an 
> univalent
> theory, where all types are fibrant)
>
>  For testing this, one question is:  can we define semi-simplicial types 
> in (1)? in (2)?
>
>  Best regards,
>  Thierry
>
>
>
> On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com <javascript:>> 
> wrote:
>
> So the answer was yes, right? Problem solved?
>
> On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote: 
>>
>> Just a thought… Can we devise a version of the HTS where exact equality 
>> types are not available for the universes such that, even with the exact 
>> equality, HTS would remain a univalent theory. 
>>
>> Maybe only some types should be equipped with the exact equality and this 
>> should be a special quality of types. 
>>
>> Vladimir. 
>>
>> PS If there are higher inductive types then the exact equality should not 
>> be available for them either.
>>
>
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to HomotopyTypeThe...@googlegroups.com <javascript:>.
> For more options, visit https://groups.google.com/d/optout.
>
>
>
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to HomotopyTypeThe...@googlegroups.com <javascript:>.
> For more options, visit https://groups.google.com/d/optout.
>
>

[-- Attachment #1.2: Type: text/html, Size: 7413 bytes --]

Re: [HoTT] about the HTS

[Michael Shulman]

Unless I misunderstand, that's not at all what cohesion is about.
Lawvere's cohesion is about relating discrete sets to space-like
objects (in the non-homotopical up-to-homeomorphism sense).  Higher
cohesion is about relating oo-groupoids to "topological oo-groupoids"
in an analogous way.

On Thu, Mar 23, 2017 at 4:22 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Thanks.
>
> I agree that with the sSet option, with an equality reflection rule, it
> would be infeasible to check judgments without extra stuff from outside the
> type theory proper. But what's wrong with that? We add extra stuff anyway,
> like type classes, proof scripts, and implicit arguments. To me, it seems
> that the practical concern of checking the truth of judgments does not need
> to be solved by the design of the core type theory. Indeed, it seems like
> better separation of concerns *not* to solve it there.
>
> Anyway, my understanding of bSet, from what Thierry Coquand said, is that
> it'd be a more OTT-like version of sSet, which is more ETT-like. So instead
> of paths between bSets being reflectable to judgmental equalities, they
> would be "strict propositions" (sProp), whose elements are not only all
> (typally) equal, but they also have no computational content. So any
> "transport" across a strict equality reduces away, as long as it doesn't
> change the type. (It doesn't have to be (judgmentally equal to)
> reflexivity.)
>
> I figure the idea is that bSet should be able to do everything sSet can,
> just with extra computationally-irrelevant transports thrown in to appease a
> decidable type checker.
>
> I don't actually see how either of these universes would help define
> semi-simplicial types. I didn't realize that was the goal here. I thought we
> were just trying to make set-level math more convenient.
>
> -----------
>
> Though I haven't given it a serious thinking-about, I figured that stuff
> with cohesion would be a good way to make semi-simplicial types definable,
> without adding non-fibrant types.
> (https://homotopytypetheory.org/2015/09/25/realcohesion/) It sounded like
> cohesion gives you a set-level view of non-hsets, so I figured you should be
> able to use strict equality in the construction of non-hsets that way.
>
> I suppose strict sets and cohesion can be combined. A set-level view of
> things should yield only strict sets, not arbitrary hsets. (I guess that
> requires a whole hierarchy of strict set universes. But unlike HTS, they're
> all "included" in the univalent universes, not the other way around.)
>
> On Wednesday, March 22, 2017 at 5:01:16 PM UTC-4, v v wrote:
>>
>> 1. As Thierry pointed out previously, the problem with sSet is that if we
>> postulate that nat:sSet, then for any (small) type T, the function type T ->
>> nat is in sSet, e.g. nat -> nat is in sSet.
>>
>> Since it is possible to construct two elements of nat -> nat the equality
>> between which is an undecidable proposition, it implies that the
>> definitional equality in any sufficiently advanced type system with sSet and
>> nat:sSet is undecidable.
>>
>> That means that witnesses, in some language, of definitional equality need
>> to be carried around and therefore the design of a proof assistant where the
>> proof term is the proof is not possible in this system.
>>
>> 2. It is not so clear what would happen with only bSet and nat:bSet.
>>
>> Vladimir.
>>
>>
>>
>>
>>
>> On Mar 22, 2017, at 5:49 PM, Thierry Coquand <Thier...@cse.gu.se> wrote:
>>
>>
>> If my note was correct, it describes in the cubical set model two
>> univalent universes
>> (subpresheaf of the first universe)  that satisfy
>>
>>  (1)   if   A : sSet    and   p : Path A a b   then   a = b : A  and p is
>> the constant path a
>> (equality reflection rule)
>>
>>  (2)   if A : bSet and p and q of type Path A a b   then p = q : Path A a
>> b
>> (judgemental form of UIP)
>>
>>  Maybe (1) or (2) could be used instead of HTS (and we would remain in an
>> univalent
>> theory, where all types are fibrant)
>>
>>  For testing this, one question is:  can we define semi-simplicial types
>> in (1)? in (2)?
>>
>>  Best regards,
>>  Thierry
>>
>>
>>
>> On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com> wrote:
>>
>> So the answer was yes, right? Problem solved?
>>
>> On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:
>>>
>>> Just a thought… Can we devise a version of the HTS where exact equality
>>> types are not available for the universes such that, even with the exact
>>> equality, HTS would remain a univalent theory.
>>>
>>> Maybe only some types should be equipped with the exact equality and this
>>> should be a special quality of types.
>>>
>>> Vladimir.
>>>
>>> PS If there are higher inductive types then the exact equality should not
>>> be available for them either.
>>
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>>
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] about the HTS

[Matt Oliveri]

[-- Attachment #1.1: Type: text/plain, Size: 6669 bytes --]

Mike has explained to me that the approach I'm thinking of is not cohesion. 
Sorry about that.

On Thursday, March 23, 2017 at 7:33:32 AM UTC-4, Michael Shulman wrote:
>
> Unless I misunderstand, that's not at all what cohesion is about. 
> Lawvere's cohesion is about relating discrete sets to space-like 
> objects (in the non-homotopical up-to-homeomorphism sense).  Higher 
> cohesion is about relating oo-groupoids to "topological oo-groupoids" 
> in an analogous way. 
>
> On Thu, Mar 23, 2017 at 4:22 AM, Matt Oliveri <atm...@gmail.com 
> <javascript:>> wrote: 
> > Thanks. 
> > 
> > I agree that with the sSet option, with an equality reflection rule, it 
> > would be infeasible to check judgments without extra stuff from outside 
> the 
> > type theory proper. But what's wrong with that? We add extra stuff 
> anyway, 
> > like type classes, proof scripts, and implicit arguments. To me, it 
> seems 
> > that the practical concern of checking the truth of judgments does not 
> need 
> > to be solved by the design of the core type theory. Indeed, it seems 
> like 
> > better separation of concerns *not* to solve it there. 
> > 
> > Anyway, my understanding of bSet, from what Thierry Coquand said, is 
> that 
> > it'd be a more OTT-like version of sSet, which is more ETT-like. So 
> instead 
> > of paths between bSets being reflectable to judgmental equalities, they 
> > would be "strict propositions" (sProp), whose elements are not only all 
> > (typally) equal, but they also have no computational content. So any 
> > "transport" across a strict equality reduces away, as long as it doesn't 
> > change the type. (It doesn't have to be (judgmentally equal to) 
> > reflexivity.) 
> > 
> > I figure the idea is that bSet should be able to do everything sSet can, 
> > just with extra computationally-irrelevant transports thrown in to 
> appease a 
> > decidable type checker. 
> > 
> > I don't actually see how either of these universes would help define 
> > semi-simplicial types. I didn't realize that was the goal here. I 
> thought we 
> > were just trying to make set-level math more convenient. 
> > 
> > ----------- 
> > 
> > Though I haven't given it a serious thinking-about, I figured that stuff 
> > with cohesion would be a good way to make semi-simplicial types 
> definable, 
> > without adding non-fibrant types. 
> > (https://homotopytypetheory.org/2015/09/25/realcohesion/) It sounded 
> like 
> > cohesion gives you a set-level view of non-hsets, so I figured you 
> should be 
> > able to use strict equality in the construction of non-hsets that way. 
> > 
> > I suppose strict sets and cohesion can be combined. A set-level view of 
> > things should yield only strict sets, not arbitrary hsets. (I guess that 
> > requires a whole hierarchy of strict set universes. But unlike HTS, 
> they're 
> > all "included" in the univalent universes, not the other way around.) 
> > 
> > On Wednesday, March 22, 2017 at 5:01:16 PM UTC-4, v v wrote: 
> >> 
> >> 1. As Thierry pointed out previously, the problem with sSet is that if 
> we 
> >> postulate that nat:sSet, then for any (small) type T, the function type 
> T -> 
> >> nat is in sSet, e.g. nat -> nat is in sSet. 
> >> 
> >> Since it is possible to construct two elements of nat -> nat the 
> equality 
> >> between which is an undecidable proposition, it implies that the 
> >> definitional equality in any sufficiently advanced type system with 
> sSet and 
> >> nat:sSet is undecidable. 
> >> 
> >> That means that witnesses, in some language, of definitional equality 
> need 
> >> to be carried around and therefore the design of a proof assistant 
> where the 
> >> proof term is the proof is not possible in this system. 
> >> 
> >> 2. It is not so clear what would happen with only bSet and nat:bSet. 
> >> 
> >> Vladimir. 
> >> 
> >> 
> >> 
> >> 
> >> 
> >> On Mar 22, 2017, at 5:49 PM, Thierry Coquand <Thier...@cse.gu.se> 
> wrote: 
> >> 
> >> 
> >> If my note was correct, it describes in the cubical set model two 
> >> univalent universes 
> >> (subpresheaf of the first universe)  that satisfy 
> >> 
> >>  (1)   if   A : sSet    and   p : Path A a b   then   a = b : A  and p 
> is 
> >> the constant path a 
> >> (equality reflection rule) 
> >> 
> >>  (2)   if A : bSet and p and q of type Path A a b   then p = q : Path A 
> a 
> >> b 
> >> (judgemental form of UIP) 
> >> 
> >>  Maybe (1) or (2) could be used instead of HTS (and we would remain in 
> an 
> >> univalent 
> >> theory, where all types are fibrant) 
> >> 
> >>  For testing this, one question is:  can we define semi-simplicial 
> types 
> >> in (1)? in (2)? 
> >> 
> >>  Best regards, 
> >>  Thierry 
> >> 
> >> 
> >> 
> >> On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com> wrote: 
> >> 
> >> So the answer was yes, right? Problem solved? 
> >> 
> >> On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote: 
> >>> 
> >>> Just a thought… Can we devise a version of the HTS where exact 
> equality 
> >>> types are not available for the universes such that, even with the 
> exact 
> >>> equality, HTS would remain a univalent theory. 
> >>> 
> >>> Maybe only some types should be equipped with the exact equality and 
> this 
> >>> should be a special quality of types. 
> >>> 
> >>> Vladimir. 
> >>> 
> >>> PS If there are higher inductive types then the exact equality should 
> not 
> >>> be available for them either. 
> >> 
> >> 
> >> -- 
> >> You received this message because you are subscribed to the Google 
> Groups 
> >> "Homotopy Type Theory" group. 
> >> To unsubscribe from this group and stop receiving emails from it, send 
> an 
> >> email to HomotopyTypeThe...@googlegroups.com <javascript:>. 
>
> >> For more options, visit https://groups.google.com/d/optout. 
> >> 
> >> 
> >> 
> >> -- 
> >> You received this message because you are subscribed to the Google 
> Groups 
> >> "Homotopy Type Theory" group. 
> >> To unsubscribe from this group and stop receiving emails from it, send 
> an 
> >> email to HomotopyTypeThe...@googlegroups.com <javascript:>. 
>
> >> For more options, visit https://groups.google.com/d/optout. 
> > 
> > -- 
> > You received this message because you are subscribed to the Google 
> Groups 
> > "Homotopy Type Theory" group. 
> > To unsubscribe from this group and stop receiving emails from it, send 
> an 
> > email to HomotopyTypeThe...@googlegroups.com <javascript:>. 
> > For more options, visit https://groups.google.com/d/optout. 
>

[-- Attachment #1.2: Type: text/html, Size: 9758 bytes --]