Re: [HoTT] about the HTS

[Michael Shulman <shu...@sandiego.edu>]

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.