Conjecture

Conjecture

[Martin Escardo]

This is a question I would like to see eventually answered.

I posed it a few years ago in a conference (and privately among some of
you), but I would like to have it here in this list for the record.

Definition. A modulus of constancy for a function f:X->Y is a function
(x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli
of constancy, but if Y is a set then it can have at most one.)

We know that if Y is a set and f comes with a modulus of constancy, then
f factors through |-|: X -> ||Y||, meaning that we can exhibit an
f':||X||->Y with f'|x| = f(x).

Conjecture. If for all types X and Y and all functions f:X->Y equipped
with a modulus of constancy we can exhibit f':||X||->Y with f'|x| =
f(x), then all types are sets.

For this conjecture, I assume function extensionality and propositional
extensionality, but not (general) univalence. But feel free to play with
the assumptions.

Martin

Re: [HoTT] Conjecture

[Nicolai Kraus]

Hi Martin, I also would like to know the answer to this conjecture.
I am not sure whether I expect that it holds in the quite minimalistic
setting that you suggested (but of course we know that the premise of
the conjecture is inconsistent in "full HoTT" by Mike's argument).

Here is a small thought. Let's allow the innocent-looking HIT which we
can write as {-}, known as "generalised circle" or "pseudo truncation"
or "1-step truncation", where {X} has constructors
   [-] : X -> {X}  and  c : (x y : X) -> [x] = [y].
Then, from the premise of your conjecture, it follows that every {X}
has split support, which looks a bit suspicious. I don't know whether
you can get anything out of this idea (especially without univalence).
But it would certainly be enough to show that every such {X} is a set,
since then in particular {1} aka S^1 would be a set, and consequently
every type.

Nicolai


On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote:
> This is a question I would like to see eventually answered.
>
> I posed it a few years ago in a conference (and privately among some of
> you), but I would like to have it here in this list for the record.
>
> Definition. A modulus of constancy for a function f:X->Y is a function
> (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli
> of constancy, but if Y is a set then it can have at most one.)
>
> We know that if Y is a set and f comes with a modulus of constancy, then
> f factors through |-|: X -> ||Y||, meaning that we can exhibit an
> f':||X||->Y with f'|x| = f(x).
>
> Conjecture. If for all types X and Y and all functions f:X->Y equipped
> with a modulus of constancy we can exhibit f':||X||->Y with f'|x| =
> f(x), then all types are sets.
>
> For this conjecture, I assume function extensionality and propositional
> extensionality, but not (general) univalence. But feel free to play with
> the assumptions.
>
> Martin
>

Re: [HoTT] Conjecture

[Martin Escardo]

Thanks, Nicolai. I don't have anything to add to your remarks.

But here is an example where the factorization of constant functions
is possible and gives something interesting/useful, whose formulation
doesn't refer to constant functions or factorizations.

(This is part of joint work with Cory Knapp.)

For a type X, define its type of partial elements to be

  LX := Sigma(P:U), isProp P * (P->X).

If X is a set, then LX is a directed-complete partially ordered set
(with a minimal element).

This claim is proved using the factorization of constant functions
through the propositional truncation of their domains, where the
codomains are sets, as follows.

The order is defined (in the obvious way) by

 (P:U,-,f:P->X) <= (Q:U,-,g:Q->X)

    := Sigma(t:P->Q), Pi(p:P), f(p)=g(t(p)).

(Where you use the blanks "-" and the assumption that X is a set to
show that this is a partial order.)

Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct
its least upper bound.

Its extent of definition is the proposition ||Sigma_i, P_i||, and the
question is how we define

   f:||Sigma_i, P_i||->X.

We know how to define

   f':(Sigma_i, P_i)->X

from the f_i's (by the universal property of Sigma). But X is not a
proposition, and hence we can't add ||-|| to f' to get f using the
universal property of ||-||.

But we can show that f' is constant from the assumption of
directedness, and then get the desired f:||Sigma_i, P_i||->X by the
factorization property, using the assumption that X is a set. Then the
remaining details are routine.

What if X is not a set? Then we won't get a partial order, but still
we may wish to ask whether the resulting category-like structure has
filtered colimits in a suitable sense. But when trying to do this, we
stumble on the fact that the factorization used in the above
construction won't be available in general when X is not a set.

So, in addition to the conjecture, I would also like to know
(independently of the above example), *precisely when* the
factorization through ||-|| is possible for a function with a given
modulus of constancy.

(I've come across of a number of examples where such factorizations of
constant functions proved useful. Perhaps others have too? I'd like to
know.)

Best,
Martin



On 29/03/17 22:08, Nicolai Kraus wrote:
> Hi Martin, I also would like to know the answer to this conjecture.
> I am not sure whether I expect that it holds in the quite minimalistic
> setting that you suggested (but of course we know that the premise of
> the conjecture is inconsistent in "full HoTT" by Mike's argument).
> 
> Here is a small thought. Let's allow the innocent-looking HIT which we
> can write as {-}, known as "generalised circle" or "pseudo truncation"
> or "1-step truncation", where {X} has constructors
>   [-] : X -> {X}  and  c : (x y : X) -> [x] = [y].
> Then, from the premise of your conjecture, it follows that every {X}
> has split support, which looks a bit suspicious. I don't know whether
> you can get anything out of this idea (especially without univalence).
> But it would certainly be enough to show that every such {X} is a set,
> since then in particular {1} aka S^1 would be a set, and consequently
> every type.
> 
> Nicolai
> 
> 
> On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote:
>> This is a question I would like to see eventually answered.
>>
>> I posed it a few years ago in a conference (and privately among some of
>> you), but I would like to have it here in this list for the record.
>>
>> Definition. A modulus of constancy for a function f:X->Y is a function
>> (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli
>> of constancy, but if Y is a set then it can have at most one.)
>>
>> We know that if Y is a set and f comes with a modulus of constancy, then
>> f factors through |-|: X -> ||Y||, meaning that we can exhibit an
>> f':||X||->Y with f'|x| = f(x).
>>
>> Conjecture. If for all types X and Y and all functions f:X->Y equipped
>> with a modulus of constancy we can exhibit f':||X||->Y with f'|x| =
>> f(x), then all types are sets.
>>
>> For this conjecture, I assume function extensionality and propositional
>> extensionality, but not (general) univalence. But feel free to play with
>> the assumptions.
>>
>> Martin
>>
> 

Re: [HoTT] Conjecture

[Michael Shulman]

Note that Nicolai
(http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf), Floris
(arXiv:1512.02274), and Egbert (arXiv:1701.07538) have all recently
given (different) constructions of ||-|| in terms of a sequential
colimit of nonrecursive HITs.  Each of those constructions gives an
answer to "precisely when the factorization through ||-|| is
possible".

On Wed, Mar 29, 2017 at 6:05 PM, 'Martin Escardo' via Homotopy Type
Theory <HomotopyT...@googlegroups.com> wrote:
> Thanks, Nicolai. I don't have anything to add to your remarks.
>
> But here is an example where the factorization of constant functions
> is possible and gives something interesting/useful, whose formulation
> doesn't refer to constant functions or factorizations.
>
> (This is part of joint work with Cory Knapp.)
>
> For a type X, define its type of partial elements to be
>
>   LX := Sigma(P:U), isProp P * (P->X).
>
> If X is a set, then LX is a directed-complete partially ordered set
> (with a minimal element).
>
> This claim is proved using the factorization of constant functions
> through the propositional truncation of their domains, where the
> codomains are sets, as follows.
>
> The order is defined (in the obvious way) by
>
>  (P:U,-,f:P->X) <= (Q:U,-,g:Q->X)
>
>     := Sigma(t:P->Q), Pi(p:P), f(p)=g(t(p)).
>
> (Where you use the blanks "-" and the assumption that X is a set to
> show that this is a partial order.)
>
> Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct
> its least upper bound.
>
> Its extent of definition is the proposition ||Sigma_i, P_i||, and the
> question is how we define
>
>    f:||Sigma_i, P_i||->X.
>
> We know how to define
>
>    f':(Sigma_i, P_i)->X
>
> from the f_i's (by the universal property of Sigma). But X is not a
> proposition, and hence we can't add ||-|| to f' to get f using the
> universal property of ||-||.
>
> But we can show that f' is constant from the assumption of
> directedness, and then get the desired f:||Sigma_i, P_i||->X by the
> factorization property, using the assumption that X is a set. Then the
> remaining details are routine.
>
> What if X is not a set? Then we won't get a partial order, but still
> we may wish to ask whether the resulting category-like structure has
> filtered colimits in a suitable sense. But when trying to do this, we
> stumble on the fact that the factorization used in the above
> construction won't be available in general when X is not a set.
>
> So, in addition to the conjecture, I would also like to know
> (independently of the above example), *precisely when* the
> factorization through ||-|| is possible for a function with a given
> modulus of constancy.
>
> (I've come across of a number of examples where such factorizations of
> constant functions proved useful. Perhaps others have too? I'd like to
> know.)
>
> Best,
> Martin
>
>
>
> On 29/03/17 22:08, Nicolai Kraus wrote:
>> Hi Martin, I also would like to know the answer to this conjecture.
>> I am not sure whether I expect that it holds in the quite minimalistic
>> setting that you suggested (but of course we know that the premise of
>> the conjecture is inconsistent in "full HoTT" by Mike's argument).
>>
>> Here is a small thought. Let's allow the innocent-looking HIT which we
>> can write as {-}, known as "generalised circle" or "pseudo truncation"
>> or "1-step truncation", where {X} has constructors
>>   [-] : X -> {X}  and  c : (x y : X) -> [x] = [y].
>> Then, from the premise of your conjecture, it follows that every {X}
>> has split support, which looks a bit suspicious. I don't know whether
>> you can get anything out of this idea (especially without univalence).
>> But it would certainly be enough to show that every such {X} is a set,
>> since then in particular {1} aka S^1 would be a set, and consequently
>> every type.
>>
>> Nicolai
>>
>>
>> On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote:
>>> This is a question I would like to see eventually answered.
>>>
>>> I posed it a few years ago in a conference (and privately among some of
>>> you), but I would like to have it here in this list for the record.
>>>
>>> Definition. A modulus of constancy for a function f:X->Y is a function
>>> (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli
>>> of constancy, but if Y is a set then it can have at most one.)
>>>
>>> We know that if Y is a set and f comes with a modulus of constancy, then
>>> f factors through |-|: X -> ||Y||, meaning that we can exhibit an
>>> f':||X||->Y with f'|x| = f(x).
>>>
>>> Conjecture. If for all types X and Y and all functions f:X->Y equipped
>>> with a modulus of constancy we can exhibit f':||X||->Y with f'|x| =
>>> f(x), then all types are sets.
>>>
>>> For this conjecture, I assume function extensionality and propositional
>>> extensionality, but not (general) univalence. But feel free to play with
>>> the assumptions.
>>>
>>> Martin
>>>
>>
>
> --
> 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] Conjecture

[Egbert Rijke]

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

There seems to be a coherence condition missing in the conjecture: it would
be natural to say that the precomposition map

(||X|| -> Y) -> ({X} -> Y),

or equivalently the canonical map

(||X|| -> Y) -> (Sigma (f : X -> Y). Pi (x,y:X). fx = fy)

has a section (or even is an equivalence), but in that case we would also
have to assume that the homotopy Pi (x,y :X). fx = fy is compatible with
the action on paths of the map ||X|| -> Y.

Is it intentional that this coherence is missing from the conjecture?

Best,
Egbert

On Thu, Mar 30, 2017 at 6:59 AM, Michael Shulman <shu...@sandiego.edu>
wrote:

> Note that Nicolai
> (http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf), Floris
> (arXiv:1512.02274), and Egbert (arXiv:1701.07538) have all recently
> given (different) constructions of ||-|| in terms of a sequential
> colimit of nonrecursive HITs.  Each of those constructions gives an
> answer to "precisely when the factorization through ||-|| is
> possible".
>
> On Wed, Mar 29, 2017 at 6:05 PM, 'Martin Escardo' via Homotopy Type
> Theory <HomotopyT...@googlegroups.com> wrote:
> > Thanks, Nicolai. I don't have anything to add to your remarks.
> >
> > But here is an example where the factorization of constant functions
> > is possible and gives something interesting/useful, whose formulation
> > doesn't refer to constant functions or factorizations.
> >
> > (This is part of joint work with Cory Knapp.)
> >
> > For a type X, define its type of partial elements to be
> >
> >   LX := Sigma(P:U), isProp P * (P->X).
> >
> > If X is a set, then LX is a directed-complete partially ordered set
> > (with a minimal element).
> >
> > This claim is proved using the factorization of constant functions
> > through the propositional truncation of their domains, where the
> > codomains are sets, as follows.
> >
> > The order is defined (in the obvious way) by
> >
> >  (P:U,-,f:P->X) <= (Q:U,-,g:Q->X)
> >
> >     := Sigma(t:P->Q), Pi(p:P), f(p)=g(t(p)).
> >
> > (Where you use the blanks "-" and the assumption that X is a set to
> > show that this is a partial order.)
> >
> > Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct
> > its least upper bound.
> >
> > Its extent of definition is the proposition ||Sigma_i, P_i||, and the
> > question is how we define
> >
> >    f:||Sigma_i, P_i||->X.
> >
> > We know how to define
> >
> >    f':(Sigma_i, P_i)->X
> >
> > from the f_i's (by the universal property of Sigma). But X is not a
> > proposition, and hence we can't add ||-|| to f' to get f using the
> > universal property of ||-||.
> >
> > But we can show that f' is constant from the assumption of
> > directedness, and then get the desired f:||Sigma_i, P_i||->X by the
> > factorization property, using the assumption that X is a set. Then the
> > remaining details are routine.
> >
> > What if X is not a set? Then we won't get a partial order, but still
> > we may wish to ask whether the resulting category-like structure has
> > filtered colimits in a suitable sense. But when trying to do this, we
> > stumble on the fact that the factorization used in the above
> > construction won't be available in general when X is not a set.
> >
> > So, in addition to the conjecture, I would also like to know
> > (independently of the above example), *precisely when* the
> > factorization through ||-|| is possible for a function with a given
> > modulus of constancy.
> >
> > (I've come across of a number of examples where such factorizations of
> > constant functions proved useful. Perhaps others have too? I'd like to
> > know.)
> >
> > Best,
> > Martin
> >
> >
> >
> > On 29/03/17 22:08, Nicolai Kraus wrote:
> >> Hi Martin, I also would like to know the answer to this conjecture.
> >> I am not sure whether I expect that it holds in the quite minimalistic
> >> setting that you suggested (but of course we know that the premise of
> >> the conjecture is inconsistent in "full HoTT" by Mike's argument).
> >>
> >> Here is a small thought. Let's allow the innocent-looking HIT which we
> >> can write as {-}, known as "generalised circle" or "pseudo truncation"
> >> or "1-step truncation", where {X} has constructors
> >>   [-] : X -> {X}  and  c : (x y : X) -> [x] = [y].
> >> Then, from the premise of your conjecture, it follows that every {X}
> >> has split support, which looks a bit suspicious. I don't know whether
> >> you can get anything out of this idea (especially without univalence).
> >> But it would certainly be enough to show that every such {X} is a set,
> >> since then in particular {1} aka S^1 would be a set, and consequently
> >> every type.
> >>
> >> Nicolai
> >>
> >>
> >> On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote:
> >>> This is a question I would like to see eventually answered.
> >>>
> >>> I posed it a few years ago in a conference (and privately among some of
> >>> you), but I would like to have it here in this list for the record.
> >>>
> >>> Definition. A modulus of constancy for a function f:X->Y is a function
> >>> (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli
> >>> of constancy, but if Y is a set then it can have at most one.)
> >>>
> >>> We know that if Y is a set and f comes with a modulus of constancy,
> then
> >>> f factors through |-|: X -> ||Y||, meaning that we can exhibit an
> >>> f':||X||->Y with f'|x| = f(x).
> >>>
> >>> Conjecture. If for all types X and Y and all functions f:X->Y equipped
> >>> with a modulus of constancy we can exhibit f':||X||->Y with f'|x| =
> >>> f(x), then all types are sets.
> >>>
> >>> For this conjecture, I assume function extensionality and propositional
> >>> extensionality, but not (general) univalence. But feel free to play
> with
> >>> the assumptions.
> >>>
> >>> Martin
> >>>
> >>
> >
> > --
> > 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.
>



-- 
egbertrijke.com

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

Re: [HoTT] Conjecture

[Nicolai Kraus]

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

Egbert, this map becomes an equivalence if you add a tower of coherences
to the codomain (by arXiv:1411.2682), I don't see a simple single coherence
that you can reasonably add - what do you have in mind? What do you
mean by "the homotopy is compatible with the action on paths"?
Nicolai


On 30/03/17 20:22, Egbert Rijke wrote:
> There seems to be a coherence condition missing in the conjecture: it 
> would be natural to say that the precomposition map
>
> (||X|| -> Y) -> ({X} -> Y),
>
> or equivalently the canonical map
>
> (||X|| -> Y) -> (Sigma (f : X -> Y). Pi (x,y:X). fx = fy)
>
> has a section (or even is an equivalence), but in that case we would 
> also have to assume that the homotopy Pi (x,y :X). fx = fy is 
> compatible with the action on paths of the map ||X|| -> Y.
>
> Is it intentional that this coherence is missing from the conjecture?
>
> Best,
> Egbert
>
> On Thu, Mar 30, 2017 at 6:59 AM, Michael Shulman <shu...@sandiego.edu 
> <mailto:shu...@sandiego.edu>> wrote:
>
>     Note that Nicolai
>     (http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf
>     <http://www.cs.nott.ac.uk/%7Epsznk/docs/pseudotruncations.pdf>),
>     Floris
>     (arXiv:1512.02274), and Egbert (arXiv:1701.07538) have all recently
>     given (different) constructions of ||-|| in terms of a sequential
>     colimit of nonrecursive HITs.  Each of those constructions gives an
>     answer to "precisely when the factorization through ||-|| is
>     possible".
>
>     On Wed, Mar 29, 2017 at 6:05 PM, 'Martin Escardo' via Homotopy Type
>     Theory <HomotopyT...@googlegroups.com
>     <mailto:HomotopyT...@googlegroups.com>> wrote:
>     > Thanks, Nicolai. I don't have anything to add to your remarks.
>     >
>     > But here is an example where the factorization of constant functions
>     > is possible and gives something interesting/useful, whose
>     formulation
>     > doesn't refer to constant functions or factorizations.
>     >
>     > (This is part of joint work with Cory Knapp.)
>     >
>     > For a type X, define its type of partial elements to be
>     >
>     >   LX := Sigma(P:U), isProp P * (P->X).
>     >
>     > If X is a set, then LX is a directed-complete partially ordered set
>     > (with a minimal element).
>     >
>     > This claim is proved using the factorization of constant functions
>     > through the propositional truncation of their domains, where the
>     > codomains are sets, as follows.
>     >
>     > The order is defined (in the obvious way) by
>     >
>     >  (P:U,-,f:P->X) <= (Q:U,-,g:Q->X)
>     >
>     >     := Sigma(t:P->Q), Pi(p:P), f(p)=g(t(p)).
>     >
>     > (Where you use the blanks "-" and the assumption that X is a set to
>     > show that this is a partial order.)
>     >
>     > Now, given a directed family (P_i,-,f_i:P_i->X), we want to
>     construct
>     > its least upper bound.
>     >
>     > Its extent of definition is the proposition ||Sigma_i, P_i||,
>     and the
>     > question is how we define
>     >
>     >    f:||Sigma_i, P_i||->X.
>     >
>     > We know how to define
>     >
>     >    f':(Sigma_i, P_i)->X
>     >
>     > from the f_i's (by the universal property of Sigma). But X is not a
>     > proposition, and hence we can't add ||-|| to f' to get f using the
>     > universal property of ||-||.
>     >
>     > But we can show that f' is constant from the assumption of
>     > directedness, and then get the desired f:||Sigma_i, P_i||->X by the
>     > factorization property, using the assumption that X is a set.
>     Then the
>     > remaining details are routine.
>     >
>     > What if X is not a set? Then we won't get a partial order, but still
>     > we may wish to ask whether the resulting category-like structure has
>     > filtered colimits in a suitable sense. But when trying to do
>     this, we
>     > stumble on the fact that the factorization used in the above
>     > construction won't be available in general when X is not a set.
>     >
>     > So, in addition to the conjecture, I would also like to know
>     > (independently of the above example), *precisely when* the
>     > factorization through ||-|| is possible for a function with a given
>     > modulus of constancy.
>     >
>     > (I've come across of a number of examples where such
>     factorizations of
>     > constant functions proved useful. Perhaps others have too? I'd
>     like to
>     > know.)
>     >
>     > Best,
>     > Martin
>     >
>     >
>     >
>     > On 29/03/17 22:08, Nicolai Kraus wrote:
>     >> Hi Martin, I also would like to know the answer to this conjecture.
>     >> I am not sure whether I expect that it holds in the quite
>     minimalistic
>     >> setting that you suggested (but of course we know that the
>     premise of
>     >> the conjecture is inconsistent in "full HoTT" by Mike's argument).
>     >>
>     >> Here is a small thought. Let's allow the innocent-looking HIT
>     which we
>     >> can write as {-}, known as "generalised circle" or "pseudo
>     truncation"
>     >> or "1-step truncation", where {X} has constructors
>     >>   [-] : X -> {X}  and  c : (x y : X) -> [x] = [y].
>     >> Then, from the premise of your conjecture, it follows that
>     every {X}
>     >> has split support, which looks a bit suspicious. I don't know
>     whether
>     >> you can get anything out of this idea (especially without
>     univalence).
>     >> But it would certainly be enough to show that every such {X} is
>     a set,
>     >> since then in particular {1} aka S^1 would be a set, and
>     consequently
>     >> every type.
>     >>
>     >> Nicolai
>     >>
>     >>
>     >> On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote:
>     >>> This is a question I would like to see eventually answered.
>     >>>
>     >>> I posed it a few years ago in a conference (and privately
>     among some of
>     >>> you), but I would like to have it here in this list for the
>     record.
>     >>>
>     >>> Definition. A modulus of constancy for a function f:X->Y is a
>     function
>     >>> (x,y:X)->f(x)=f(y). (Such a function can have zero, one or
>     more moduli
>     >>> of constancy, but if Y is a set then it can have at most one.)
>     >>>
>     >>> We know that if Y is a set and f comes with a modulus of
>     constancy, then
>     >>> f factors through |-|: X -> ||Y||, meaning that we can exhibit an
>     >>> f':||X||->Y with f'|x| = f(x).
>     >>>
>     >>> Conjecture. If for all types X and Y and all functions f:X->Y
>     equipped
>     >>> with a modulus of constancy we can exhibit f':||X||->Y with
>     f'|x| =
>     >>> f(x), then all types are sets.
>     >>>
>     >>> For this conjecture, I assume function extensionality and
>     propositional
>     >>> extensionality, but not (general) univalence. But feel free to
>     play with
>     >>> the assumptions.
>     >>>
>     >>> Martin
>     >>>
>     >>
>     >
>     > --
>     > 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:HomotopyTypeTheo...@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:HomotopyTypeTheo...@googlegroups.com>.
>     For more options, visit https://groups.google.com/d/optout
>     <https://groups.google.com/d/optout>.
>
>
>
>
> -- 
> egbertrijke.com <https://egbertrijke.com/>
> -- 
> 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: 14193 bytes --]

Re: [HoTT] Conjecture

[Nicolai Kraus]

Interesting construction by Cory and you! And I think I can help
you with the factorisation that you asked for, as follows:

On 29/03/17 23:05, 'Martin Escardo' via Homotopy Type Theory wrote:
> Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct
> its least upper bound.
>
> Its extent of definition is the proposition ||Sigma_i, P_i||, and the
> question is how we define
>
>     f:||Sigma_i, P_i||->X.
>
> We know how to define
>
>     f':(Sigma_i, P_i)->X
>
> [...]
>
> What if X is not a set?

(I assume that it is i : Nat in the above.)
We can construct the proof of constancy for f' by only going
"steps of length 1", i.e. we do it only using the equality proofs
of the form f'(i,_) = f'(i+1,_).
This constancy proof is coherent up to whichever level you want.
By arXiv:1411.2682 Thm 10.5, this means that you can replace the
condition "X is a set" by "X is 1-truncated" or "X is 17-truncated" or
any finite number you want (this uses funext, but nothing else).

With a different strategy, we can do better and drop all assumptions
on X. Given this family (P_i, -, f_i), we can define the HIT R with
constructors

   r : (i : Nat) -> P_i -> R
   s : (i : Nat) -> (p : P_i) -> (r i p) = (r (i+1) (t i p)

(where t i : P_i -> P_{i+1} comes from the proof that the family is
directed).
Now, we can show that R is a proposition. (One way is this: To show
R -> isContr(R), we can assume that we are given (r i p : R), and we
can prove that this is a centre of contraction.)

R is equivalent to ||Sigma_i, P_i||, and it's easy to construct R -> X.

Best,
Nicolai

Re: [HoTT] Conjecture

[Martin Escardo]

On 30/03/17 23:49, Nicolai Kraus wrote:
> Interesting construction by Cory and you! And I think I can help
> you with the factorisation that you asked for, as follows:

Thanks for this, Nicolai.

Cory and I a battling against the clock to get our submission ready for
a conference. I'll continue the discussion after that.

Best,
Martin

Re: [HoTT] Conjecture

[Martin Escardo]

On 31/03/17 17:09, 'Martin Escardo' via Homotopy Type Theory wrote:
> 
> 
> On 30/03/17 23:49, Nicolai Kraus wrote:
>> Interesting construction by Cory and you! And I think I can help
>> you with the factorisation that you asked for, as follows:
> 
> Thanks for this, Nicolai.
> 
> Cory and I a battling against the clock to get our submission ready for
> a conference. I'll continue the discussion after that.

I may as well give a link to the paper now that we have finished and
submitted it, which is about partial functions in univalent type theory:
http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf

The conjecture in the initial message of this thread goes well beyond
this, and is even unrelated. But I am still very interested in the
conjecture independently of any use of it.

Martin

Re: [HoTT] Conjecture

[Jon Sterling]

Martin,

This looks like a very interesting paper, thank you for sharing. I look
forward to reading it in more detail.

I am curious, does this development use univalence except to establish
functional extensionality and propositional extensionality? The reason I
ask is, I wonder if it is possible to do a similar development of
computability theory in extensional type theory and get analogous
results. Additionally, I am curious whether you have found cases in
which univalence clarifies or sharpens this development, since I'm
trying to keep track of interesting use-cases of univalence.

Best,
Jon


On Wed, Apr 5, 2017, at 12:37 PM, 'Martin Escardo' via Homotopy Type
Theory wrote:
> 
> 
> On 31/03/17 17:09, 'Martin Escardo' via Homotopy Type Theory wrote:
> > 
> > 
> > On 30/03/17 23:49, Nicolai Kraus wrote:
> >> Interesting construction by Cory and you! And I think I can help
> >> you with the factorisation that you asked for, as follows:
> > 
> > Thanks for this, Nicolai.
> > 
> > Cory and I a battling against the clock to get our submission ready for
> > a conference. I'll continue the discussion after that.
> 
> I may as well give a link to the paper now that we have finished and
> submitted it, which is about partial functions in univalent type theory:
> http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf
> 
> The conjecture in the initial message of this thread goes well beyond
> this, and is even unrelated. But I am still very interested in the
> conjecture independently of any use of it.
> 
> Martin
> 
> -- 
> 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] Conjecture

[Martin Escardo]

On 06/04/17 01:23, Jon Sterling wrote:
> I am curious, does this development use univalence except to establish
> functional extensionality and propositional extensionality? The reason I
> ask is, I wonder if it is possible to do a similar development of
> computability theory in extensional type theory and get analogous
> results. Additionally, I am curious whether you have found cases in
> which univalence clarifies or sharpens this development, since I'm
> trying to keep track of interesting use-cases of univalence.

Currently the only place that uses univalence is the equivalence of
(X->Y) with the type of single-valued relations X->Y->U.  (This was
proved by Egbert in his mater thesis.)

But another point, compared with previous developments in topos logic
an extensional type theory, is that a number of things work as they
should for types more general than sets by replacing
subobject-classifier-valued functions by universe-valued functions.

An example is this: Consider the lifing in its representation with
subsingletons

   L(X) = (Sigma(A:X->U), isProp(Sigma(x:X), A(x))).

If we replaced U by Prop in this definition, this wouldn't work well
for types that are not sets.

For example, if X is the circle, any function into a set, and hence
any function into Prop, is constant, and so L(X) would be
contractible.

However, with the definition as it is, with U, we always have that X
is embedded into L(X), even if X is not a set.

The same phenomenon applies to the equivalence of (X->Y) with the type
of single-valued relations X->Y->U discussed above, but this
additionally requires univalence.

Martin

Re: [HoTT] Conjecture

[Vladimir Voevodsky]

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

I looks like like you would also need the resizing rule to place hProp into a lower universe. Is it so?

Vladimir.

> On Apr 6, 2017, at 1:55 AM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote:
> 
> 
> 
> On 06/04/17 01:23, Jon Sterling wrote:
>> I am curious, does this development use univalence except to establish
>> functional extensionality and propositional extensionality? The reason I
>> ask is, I wonder if it is possible to do a similar development of
>> computability theory in extensional type theory and get analogous
>> results. Additionally, I am curious whether you have found cases in
>> which univalence clarifies or sharpens this development, since I'm
>> trying to keep track of interesting use-cases of univalence.
> 
> Currently the only place that uses univalence is the equivalence of
> (X->Y) with the type of single-valued relations X->Y->U.  (This was
> proved by Egbert in his mater thesis.)
> 
> But another point, compared with previous developments in topos logic
> an extensional type theory, is that a number of things work as they
> should for types more general than sets by replacing
> subobject-classifier-valued functions by universe-valued functions.
> 
> An example is this: Consider the lifing in its representation with
> subsingletons
> 
>  L(X) = (Sigma(A:X->U), isProp(Sigma(x:X), A(x))).
> 
> If we replaced U by Prop in this definition, this wouldn't work well
> for types that are not sets.
> 
> For example, if X is the circle, any function into a set, and hence
> any function into Prop, is constant, and so L(X) would be
> contractible.
> 
> However, with the definition as it is, with U, we always have that X
> is embedded into L(X), even if X is not a set.
> 
> The same phenomenon applies to the equivalence of (X->Y) with the type
> of single-valued relations X->Y->U discussed above, but this
> additionally requires univalence.
> 
> Martin
> 
> --
> 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.


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

Re: [HoTT] Conjecture

[Martin Escardo]

On 06/04/17 13:40, Vladimir Voevodsky wrote:
> I looks like like you would also need the resizing rule to place
> hProp into a lower universe. Is it so?

I think that this is most natural way.

But, to convince myself that often resizing is not needed, I wrote in
Agda examples of similar "monads" T (e.g. the propositional truncation
defined by ||X|| : (P : U) -> isProp P -> (X -> P) -> P) with universe
juggling, by decorating the occurrences of U with indices. Although TX
will live in the next universe, and hence so will the unit and the
multiplication, and the monad laws (can be written down and) hold.

Here I show the types only, where "i" is the level of the propositions
you are considering:

T : {i j : Level} → U j → U (j ⊔ lsuc i)

η : {i j : Level} {X : U j} → X → T {i} {j} X

T-extend : {i j k : Level} {X : U j} {Y : U k}
         → (X → T {i} {k} Y) → (T {i} {j} X → T {i} {k} Y)

kleisli-law₀ : {i j : Level} {X : U j}
            → T-extend η ≡ id

kleisli-law₁ : {i j k : Level} {X : U j} {Y : U k}
               (f : X → T {i} {k} Y)
            → T-extend f ∘ η ≡ f

kleisli-law₂ : {i j k l : Level} {X : U j} {Y : U k} {Z : U l}
                (f : X → T {i} {k} Y)
                (g : Y → T {i} {l} Z)
             → T-extend(T-extend g ∘ f) ≡ (T-extend g) ∘ (T-extend f)

μ : {i j : Level} {X : U j}
  → T {i} {j ⊔ lsuc i} (T {i} {j} X) → T {i} {j} X

T-functor : {i j k : Level} {X : U j} {Y : U k}
          → (X → Y) → (T {i} {j} X → T {i} {k} Y)

This works for the above example, and for lifting too.

(Of course all this universe subscripting is ugly.)

But I would prefer that somebody proved that propositional resizing
(is consistent and) doesn't destroy normalization (e.g. in cubical
type theory), and just use resizing. Or just keep my fingers crossed
and work with propositional resizing. :-)

Martin

> 
> Vladimir.
> 
>> On Apr 6, 2017, at 1:55 AM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote:
>>
>>
>>
>> On 06/04/17 01:23, Jon Sterling wrote:
>>> I am curious, does this development use univalence except to establish
>>> functional extensionality and propositional extensionality? The reason I
>>> ask is, I wonder if it is possible to do a similar development of
>>> computability theory in extensional type theory and get analogous
>>> results. Additionally, I am curious whether you have found cases in
>>> which univalence clarifies or sharpens this development, since I'm
>>> trying to keep track of interesting use-cases of univalence.
>>
>> Currently the only place that uses univalence is the equivalence of
>> (X->Y) with the type of single-valued relations X->Y->U.  (This was
>> proved by Egbert in his mater thesis.)
>>
>> But another point, compared with previous developments in topos logic
>> an extensional type theory, is that a number of things work as they
>> should for types more general than sets by replacing
>> subobject-classifier-valued functions by universe-valued functions.
>>
>> An example is this: Consider the lifing in its representation with
>> subsingletons
>>
>>  L(X) = (Sigma(A:X->U), isProp(Sigma(x:X), A(x))).
>>
>> If we replaced U by Prop in this definition, this wouldn't work well
>> for types that are not sets.
>>
>> For example, if X is the circle, any function into a set, and hence
>> any function into Prop, is constant, and so L(X) would be
>> contractible.
>>
>> However, with the definition as it is, with U, we always have that X
>> is embedded into L(X), even if X is not a set.
>>
>> The same phenomenon applies to the equivalence of (X->Y) with the type
>> of single-valued relations X->Y->U discussed above, but this
>> additionally requires univalence.
>>
>> Martin
>>
>> --
>> 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] Conjecture

[Martin Escardo]

Another remark about size is that if the propositions in your dominance
are in the first universe, then all universes except the first one are
closed under lifting, and hence we way as well just work from the second
universe onwards as an alternative to resizing. Martin


On 06/04/17 17:08, Martin Escardo wrote:
> Another remark about size is that if the propositions in your dominance
> are in the first universe, then all universes except the first one are
> closed under lifting, and hence we way as well just work from the second
> universe onwards as an alternative to resizing. Martin
> 
> On 06/04/17 14:50, 'Martin Escardo' via Homotopy Type Theory wrote:
>>
>>
>> On 06/04/17 13:40, Vladimir Voevodsky wrote:
>>> I looks like like you would also need the resizing rule to place
>>> hProp into a lower universe. Is it so?
>>
>> I think that this is most natural way.
>>
>> But, to convince myself that often resizing is not needed, I wrote in
>> Agda examples of similar "monads" T (e.g. the propositional truncation
>> defined by ||X|| : (P : U) -> isProp P -> (X -> P) -> P) with universe
>> juggling, by decorating the occurrences of U with indices. Although TX
>> will live in the next universe, and hence so will the unit and the
>> multiplication, and the monad laws (can be written down and) hold.
>>
>> Here I show the types only, where "i" is the level of the propositions
>> you are considering:
>>
>> T : {i j : Level} → U j → U (j ⊔ lsuc i)
>>
>> η : {i j : Level} {X : U j} → X → T {i} {j} X
>>
>> T-extend : {i j k : Level} {X : U j} {Y : U k}
>>          → (X → T {i} {k} Y) → (T {i} {j} X → T {i} {k} Y)
>>
>> kleisli-law₀ : {i j : Level} {X : U j}
>>             → T-extend η ≡ id
>>
>> kleisli-law₁ : {i j k : Level} {X : U j} {Y : U k}
>>                (f : X → T {i} {k} Y)
>>             → T-extend f ∘ η ≡ f
>>
>> kleisli-law₂ : {i j k l : Level} {X : U j} {Y : U k} {Z : U l}
>>                 (f : X → T {i} {k} Y)
>>                 (g : Y → T {i} {l} Z)
>>              → T-extend(T-extend g ∘ f) ≡ (T-extend g) ∘ (T-extend f)
>>
>> μ : {i j : Level} {X : U j}
>>   → T {i} {j ⊔ lsuc i} (T {i} {j} X) → T {i} {j} X
>>
>> T-functor : {i j k : Level} {X : U j} {Y : U k}
>>           → (X → Y) → (T {i} {j} X → T {i} {k} Y)
>>
>> This works for the above example, and for lifting too.
>>
>> (Of course all this universe subscripting is ugly.)
>>
>> But I would prefer that somebody proved that propositional resizing
>> (is consistent and) doesn't destroy normalization (e.g. in cubical
>> type theory), and just use resizing. Or just keep my fingers crossed
>> and work with propositional resizing. :-)
>>
>> Martin
>>
>>>
>>> Vladimir.
>>>
>>>> On Apr 6, 2017, at 1:55 AM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote:
>>>>
>>>>
>>>>
>>>> On 06/04/17 01:23, Jon Sterling wrote:
>>>>> I am curious, does this development use univalence except to establish
>>>>> functional extensionality and propositional extensionality? The reason I
>>>>> ask is, I wonder if it is possible to do a similar development of
>>>>> computability theory in extensional type theory and get analogous
>>>>> results. Additionally, I am curious whether you have found cases in
>>>>> which univalence clarifies or sharpens this development, since I'm
>>>>> trying to keep track of interesting use-cases of univalence.
>>>>
>>>> Currently the only place that uses univalence is the equivalence of
>>>> (X->Y) with the type of single-valued relations X->Y->U.  (This was
>>>> proved by Egbert in his mater thesis.)
>>>>
>>>> But another point, compared with previous developments in topos logic
>>>> an extensional type theory, is that a number of things work as they
>>>> should for types more general than sets by replacing
>>>> subobject-classifier-valued functions by universe-valued functions.
>>>>
>>>> An example is this: Consider the lifing in its representation with
>>>> subsingletons
>>>>
>>>>  L(X) = (Sigma(A:X->U), isProp(Sigma(x:X), A(x))).
>>>>
>>>> If we replaced U by Prop in this definition, this wouldn't work well
>>>> for types that are not sets.
>>>>
>>>> For example, if X is the circle, any function into a set, and hence
>>>> any function into Prop, is constant, and so L(X) would be
>>>> contractible.
>>>>
>>>> However, with the definition as it is, with U, we always have that X
>>>> is embedded into L(X), even if X is not a set.
>>>>
>>>> The same phenomenon applies to the equivalence of (X->Y) with the type
>>>> of single-valued relations X->Y->U discussed above, but this
>>>> additionally requires univalence.
>>>>
>>>> Martin
>>>>
>>>> --
>>>> 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] Conjecture

[Thomas Streicher]

> This looks like a very interesting paper, thank you for sharing. I look
> forward to reading it in more detail.
> 
> I am curious, does this development use univalence except to establish
> functional extensionality and propositional extensionality? The reason I
> ask is, I wonder if it is possible to do a similar development of
> computability theory in extensional type theory and get analogous
> results. Additionally, I am curious whether you have found cases in
> which univalence clarifies or sharpens this development, since I'm
> trying to keep track of interesting use-cases of univalence.

For synthetic domain theory a formulation in extensional type theory
has been given in

MR1694130 (2000f:68069) 
Reus, Bernhard; Streicher, Thomas
General synthetic domain theory ¡X a logical approach. (English summary)
Math. Structures Comput. Sci. 9 (1999), no. 2, 177¡V223.

There is no need whatsoever to use univalence or something like that.
The only benefit would be to solve domain equations up to equality
which even computer scientists find unnecessary (for good reasons).

Andrej Bauer has written on Synthetic Recursion Theory, see
math.andrej.com/data/synthetic.pdf.

So I tend to the opinion that theer can't be an intrinsic use of
Univalence or HITs. But if there is I am curious to learn which one!

Thomas

Re: [HoTT] Conjecture

[Martin Escardo]

Dear Thomas,

Sorry it took so long to answer, but I needed to find time to be able
to write my reaction to your remarks.

(1) Indeed, I do like to think of the fragment of univalent type
theory consisting of function extensionality + proposition
extensionality + propositional truncation as essentially the same
thing as topos logic, provided we have propositional resizing. (But,
as discussed, much can be done without propositional resizing (but not
all), and one way of looking at HIT's is as a mechanism to avoid
resizing.)

This is good: this fragment leaves us in familiar territory.

(2) I don't see univalent type theory as simply the extension of type
theory with univalence (and hence function and proposition
extensionality). Before we extend dependent type theory with any
axiom, we can start to think "univalently".

In particular, the notions of h-level, proposition, contractibility,
equivalence, the distinction of existence as proposition or structure,
so as to be able to define e.g. embeddings, surjections, and many
others correctly, can be formulated and understood before we bring
univalence.

In this way "univalent type theory" is a different way to understand
good old type theory. Of course, with univalence we get more, and what
you are saying, and I don't disagree fundamentally, is that this
"more" are types of higher h-level and theorems and constructions with
them (such as the type of categories, if we want to avoid homotopy in
the discussion).

Although we don't use univalence in our paper, we formulate our
notions in the light of this new, alternative understanding of type
theory.

One example, already mentioned in the above answer to Jon, is
something that kept Cory and I working for an afternoon, but perhaps
is not adequately emphasized in the paper.

In topos logic, you define (for the dominance of all propositions)

  Lift(X) = { A:X->Omega | (exists(x:X), A x) &
                           forall(x,y:X), A x -> A y -> x = y }

If we want, in univalent type theory, this to work for types of higher
h-levels, how should we define this?

The above definition works well and can be kept as it is if X is a
set. To generalize it to types of higher levels, we need two
modifications:

  (i)  Change Omega to the universe U.
  (ii) Reformulate the condition on A as isProp(Sigma(x:X), A x).

When X is a set, the reformulation (i)-(ii) makes no
difference. However, in the general case, it is (i) and (ii) that give
the right definition. For instance, with the right definition, we
always get an embedding X->Lift X, whereas if we had taken the
original topos-theoretic version of Lift, then Lift S^1 would be a
singleton and hence wouldn't embed S^1. We would get the wrong notion
of partial function.

Thus, although we haven't used univalence, we took care of formulating
the notions so that they are not restricted to the realm of sets, and
in this sense what we are doing can be considered as univalent type
theory.

(3) We should have cited Andrej's and Bernhard's references below, and
we will (and many other things, to reflect the amount of work done
about this in the context of topos theory). Of course we are aware of
them, but thanks for mentioning them in this list!

(4) A last point is that, as opposed to most of the work in the topos
literature for dominances in realizability toposes as in (3), we
deliberately don't use Markov's principle or countable choice in our
internal development of computability in univalent type theory
(Section 3 of the paper). Moreover, we are *not* looking at synthetic
computability. We are looking at plain computability.

Best,
Martin


On 06/04/17 12:52, Thomas Streicher wrote:
>> This looks like a very interesting paper, thank you for sharing. I look
>> forward to reading it in more detail.
>>
>> I am curious, does this development use univalence except to establish
>> functional extensionality and propositional extensionality? The reason I
>> ask is, I wonder if it is possible to do a similar development of
>> computability theory in extensional type theory and get analogous
>> results. Additionally, I am curious whether you have found cases in
>> which univalence clarifies or sharpens this development, since I'm
>> trying to keep track of interesting use-cases of univalence.
> 
> For synthetic domain theory a formulation in extensional type theory
> has been given in
> 
> MR1694130 (2000f:68069) 
> Reus, Bernhard; Streicher, Thomas
> General synthetic domain theory — a logical approach. (English summary)
> Math. Structures Comput. Sci. 9 (1999), no. 2, 177–223.
> 
> There is no need whatsoever to use univalence or something like that.
> The only benefit would be to solve domain equations up to equality
> which even computer scientists find unnecessary (for good reasons).
> 
> Andrej Bauer has written on Synthetic Recursion Theory, see
> math.andrej.com/data/synthetic.pdf.
> 
> So I tend to the opinion that theer can't be an intrinsic use of
> Univalence or HITs. But if there is I am curious to learn which one!
> 
> Thomas
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

Re: [HoTT] Conjecture

[Michael Shulman]

On Fri, Apr 7, 2017 at 2:49 AM, 'Martin Escardo' via Homotopy Type
Theory <HomotopyT...@googlegroups.com> wrote:
> (1) Indeed, I do like to think of the fragment of univalent type
> theory consisting of function extensionality + proposition
> extensionality + propositional truncation as essentially the same
> thing as topos logic, provided we have propositional resizing. (But,
> as discussed, much can be done without propositional resizing (but not
> all), and one way of looking at HIT's is as a mechanism to avoid
> resizing.)

I would say that to really be talking about (elementary) topos logic,
one should also do without universes other than hProp.  Of course,
elementary 1-toposes also validate UIP.

If we also omit hProp and propositional resizing, but include
nonrecursive HITs as well as ordinary inductive types, then it ought
to be basically Pi-W-pretopos logic; right?

> This is good: this fragment leaves us in familiar territory.
>
> (2) I don't see univalent type theory as simply the extension of type
> theory with univalence (and hence function and proposition
> extensionality). Before we extend dependent type theory with any
> axiom, we can start to think "univalently".
>
> In particular, the notions of h-level, proposition, contractibility,
> equivalence, the distinction of existence as proposition or structure,
> so as to be able to define e.g. embeddings, surjections, and many
> others correctly, can be formulated and understood before we bring
> univalence.
>
> In this way "univalent type theory" is a different way to understand
> good old type theory. Of course, with univalence we get more, and what
> you are saying, and I don't disagree fundamentally, is that this
> "more" are types of higher h-level and theorems and constructions with
> them (such as the type of categories, if we want to avoid homotopy in
> the discussion).
>
> Although we don't use univalence in our paper, we formulate our
> notions in the light of this new, alternative understanding of type
> theory.
>
> One example, already mentioned in the above answer to Jon, is
> something that kept Cory and I working for an afternoon, but perhaps
> is not adequately emphasized in the paper.
>
> In topos logic, you define (for the dominance of all propositions)
>
>   Lift(X) = { A:X->Omega | (exists(x:X), A x) &
>                            forall(x,y:X), A x -> A y -> x = y }
>
> If we want, in univalent type theory, this to work for types of higher
> h-levels, how should we define this?
>
> The above definition works well and can be kept as it is if X is a
> set. To generalize it to types of higher levels, we need two
> modifications:
>
>   (i)  Change Omega to the universe U.
>   (ii) Reformulate the condition on A as isProp(Sigma(x:X), A x).
>
> When X is a set, the reformulation (i)-(ii) makes no
> difference. However, in the general case, it is (i) and (ii) that give
> the right definition. For instance, with the right definition, we
> always get an embedding X->Lift X, whereas if we had taken the
> original topos-theoretic version of Lift, then Lift S^1 would be a
> singleton and hence wouldn't embed S^1. We would get the wrong notion
> of partial function.
>
> Thus, although we haven't used univalence, we took care of formulating
> the notions so that they are not restricted to the realm of sets, and
> in this sense what we are doing can be considered as univalent type
> theory.
>
> (3) We should have cited Andrej's and Bernhard's references below, and
> we will (and many other things, to reflect the amount of work done
> about this in the context of topos theory). Of course we are aware of
> them, but thanks for mentioning them in this list!
>
> (4) A last point is that, as opposed to most of the work in the topos
> literature for dominances in realizability toposes as in (3), we
> deliberately don't use Markov's principle or countable choice in our
> internal development of computability in univalent type theory
> (Section 3 of the paper). Moreover, we are *not* looking at synthetic
> computability. We are looking at plain computability.
>
> Best,
> Martin
>
>
> On 06/04/17 12:52, Thomas Streicher wrote:
>>> This looks like a very interesting paper, thank you for sharing. I look
>>> forward to reading it in more detail.
>>>
>>> I am curious, does this development use univalence except to establish
>>> functional extensionality and propositional extensionality? The reason I
>>> ask is, I wonder if it is possible to do a similar development of
>>> computability theory in extensional type theory and get analogous
>>> results. Additionally, I am curious whether you have found cases in
>>> which univalence clarifies or sharpens this development, since I'm
>>> trying to keep track of interesting use-cases of univalence.
>>
>> For synthetic domain theory a formulation in extensional type theory
>> has been given in
>>
>> MR1694130 (2000f:68069)
>> Reus, Bernhard; Streicher, Thomas
>> General synthetic domain theory — a logical approach. (English summary)
>> Math. Structures Comput. Sci. 9 (1999), no. 2, 177–223.
>>
>> There is no need whatsoever to use univalence or something like that.
>> The only benefit would be to solve domain equations up to equality
>> which even computer scientists find unnecessary (for good reasons).
>>
>> Andrej Bauer has written on Synthetic Recursion Theory, see
>> math.andrej.com/data/synthetic.pdf.
>>
>> So I tend to the opinion that theer can't be an intrinsic use of
>> Univalence or HITs. But if there is I am curious to learn which one!
>>
>> Thomas
>>
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
>
> --
> 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] Conjecture

[Martin Escardo]

On 07/04/17 18:11, Michael Shulman wrote:
> On Fri, Apr 7, 2017 at 2:49 AM, 'Martin Escardo' via Homotopy Type
> Theory <HomotopyT...@googlegroups.com> wrote:
>> (1) Indeed, I do like to think of the fragment of univalent type
>> theory consisting of function extensionality + proposition
>> extensionality + propositional truncation as essentially the same
>> thing as topos logic, provided we have propositional resizing. (But,
>> as discussed, much can be done without propositional resizing (but not
>> all), and one way of looking at HIT's is as a mechanism to avoid
>> resizing.)
> 
> I would say that to really be talking about (elementary) topos logic,
> one should also do without universes other than hProp.  Of course,
> elementary 1-toposes also validate UIP.

Agreed. (But you can consider elementary toposes with a universe object,
and a number of people have worked on that independently of any
connection with dependent type theory.)

> If we also omit hProp and propositional resizing, but include
> nonrecursive HITs as well as ordinary inductive types, then it ought
> to be basically Pi-W-pretopos logic; right?

I'd let the experts on these details to answer this.

I noticed the following mistake immediately after I send my message this
morning, and this is a good opportunity to rectify it:

>> In topos logic, you define (for the dominance of all propositions)
>>
>>   Lift(X) = { A:X->Omega | (exists(x:X), A x) &
>>                            forall(x,y:X), A x -> A y -> x = y }
>>

  Lift(X) = { A:X->Omega | forall(x,y:X), A x -> A y -> x = y }

If anybody noticed, they probably knew I meant that, and, if they didn't
notice, they probably understood that. There are other possibilities, of
course. :-)

Martin

Re: Conjecture

[Daniel R. Grayson]

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

Here's a fact related to the current discussion, which I have formalized 
today.  I would appreciate knowing
whether it's already known.  It gives a criterion for factoring through the 
propositional truncation
when the target is of h-level 3.

  Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3}
             (f : X -> Y) (c : ∏ x x', f x = f x') :
    (∏ x, c x x = idpath (f x)) ->
    (∏ x x' x'', c x x'' = c x x' @ c x' x'') ->
    ∥ X ∥ -> Y.

You may find it in WellOrderedSets.v 
<https://github.com/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrderedSets.v> on 
one of my branches.



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

Re: [HoTT] Re: Conjecture

[Favonia]

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

Yes, this has been known from Nicolai's work on truncation (e.g. "The
General Universal Property"). I just learned that this has been mechanized
in Agda by Nils as well.
http://www.cse.chalmers.se/~nad/listings/equality/H-level.Truncation.html#18216
By
the way, the condition (∏ x, c x x = idpath (f x)) is provable from
transitivity. -Favonia

On Sun, Apr 2, 2017 at 8:35 PM Daniel R. Grayson <
danielrich...@gmail.com> wrote:

Here's a fact related to the current discussion, which I have formalized
today.  I would appreciate knowing
whether it's already known.  It gives a criterion for factoring through the
propositional truncation
when the target is of h-level 3.

  Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3}
             (f : X -> Y) (c : ∏ x x', f x = f x') :
    (∏ x, c x x = idpath (f x)) ->
    (∏ x x' x'', c x x'' = c x x' @ c x' x'') ->
    ∥ X ∥ -> Y.

You may find it in WellOrderedSets.v
<https://github.com/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrderedSets.v>
on
one of my branches.


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

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

Re: [HoTT] Re: Conjecture

[Nicolai Kraus]

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

Dan, this is one instance of my "general universal property of the 
propositional truncation", arXiv:1411.2682.
In that paper I show that, if you fix a number n, then for a type Y of 
h-level n, the function type
   ||X|| -> Y
is equivalent to the Sigma-type with the following components:
(1) a function X -> Y
(2) the condition that (1) is weakly constant
(3) a coherence condition for (2)
(4) a coherence condition for (3)
...
(n) a coherence condition for (n-1)

This can be presented as a natural transformation between 
semi-simplicial types.
What you have formalized is the case n=3 (one direction).
(In my presentation, I don't use the component "c x x = idpath (f x)" 
because it can be inferred,
and if you go higher than 3, this component would make additional 
coherence conditions necessary.)
Nicolai

On 03/04/17 01:35, Daniel R. Grayson wrote:
> Here's a fact related to the current discussion, which I have 
> formalized today.  I would appreciate knowing
> whether it's already known.  It gives a criterion for factoring 
> through the propositional truncation
> when the target is of h-level 3.
>
>   Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3}
>              (f : X -> Y) (c : ∏ x x', f x = f x') :
>     (∏ x, c x x = idpath (f x)) ->
>     (∏ x x' x'', c x x'' = c x x' @ c x' x'') ->
>     ∥ X ∥ -> Y.
>
> You may find it in WellOrderedSets.v 
> <https://github.com/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrderedSets.v> on 
> one of my branches.
>
>
> -- 
> 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: 3410 bytes --]

Re: [HoTT] Re: Conjecture

[Daniel R. Grayson]

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

Thanks, Nicolai and Favonia.  It's a nice result, Nicolai!

On Monday, April 3, 2017 at 5:56:36 AM UTC-4, Nicolai Kraus wrote:
>
> Dan, this is one instance of my "general universal property of the 
> propositional truncation", arXiv:1411.2682.
> In that paper I show that, if you fix a number n, then for a type Y of 
> h-level n, the function type
>   ||X|| -> Y
> is equivalent to the Sigma-type with the following components:
> (1) a function X -> Y
> (2) the condition that (1) is weakly constant
> (3) a coherence condition for (2)
> (4) a coherence condition for (3)
> ...
> (n) a coherence condition for (n-1)
>
> This can be presented as a natural transformation between semi-simplicial 
> types.
> What you have formalized is the case n=3 (one direction). 
> (In my presentation, I don't use the component "c x x = idpath (f x)" 
> because it can be inferred, 
> and if you go higher than 3, this component would make additional 
> coherence conditions necessary.)
> Nicolai
>
> On 03/04/17 01:35, Daniel R. Grayson wrote:
>
> Here's a fact related to the current discussion, which I have formalized 
> today.  I would appreciate knowing 
> whether it's already known.  It gives a criterion for factoring through 
> the propositional truncation
> when the target is of h-level 3.
>
>   Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3}
>              (f : X -> Y) (c : ∏ x x', f x = f x') :
>     (∏ x, c x x = idpath (f x)) ->
>     (∏ x x' x'', c x x'' = c x x' @ c x' x'') ->
>     ∥ X ∥ -> Y.
>
> You may find it in WellOrderedSets.v 
> <https://github.com/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrderedSets.v> on 
> one of my branches.
>
>

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