Re: [HoTT] about the HTS

[Matt Oliveri <atm...@gmail.com>]

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