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.

[Benedikt Ahrens]

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

[Vladimir Voevodsky]

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

> --
> 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.

[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.

[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.

[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.

[Paolo Capriotti]

>> 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.

[Paolo Capriotti]

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

[Vladimir Voevodsky]

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.

--
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/ebf61361-d581-4a25-98cf-0e345e2e2035%40googlegroups.com.

[Thierry Coquand]

 Here is note 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

--
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.

[Vladimir Voevodsky]

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.

[Vladimir Voevodsky]

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.

[Thierry Coquand]

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

 

[Vladimir Voevodsky]

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

BTW why do you call elements of bSet Bishop sets?

[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

[Thierry Coquand]

  For completness, I wrote here 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

[Matt Oliveri]

So the answer was yes, right? Problem solved?

[Thierry Coquand]

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

[Vladimir Voevodsky]

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.

[Matt Oliveri]

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.)

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@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 HomotopyTypeTheory+unsub...@googlegroups.com.

[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.

>> 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.

[Matt Oliveri]

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

>> email to HomotopyTypeTheory+unsub...@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 HomotopyTypeTheory+unsub...@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 HomotopyTypeTheory+unsub...@googlegroups.com.