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

[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

[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

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

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

[Egbert Rijke]

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

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

For more options, visit https://groups.google.com/d/optout.

--

egbertrijke.com

[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

[Nicolai Kraus]

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

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

[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

[Daniel R. Grayson]

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 on one of my branches.

[Favonia]

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

[Nicolai Kraus]

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

[Daniel R. Grayson]

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

[Martin Escardo]

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

[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

[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

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

[Vladimir Voevodsky]

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

Vladimir.

[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

[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

[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

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

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

[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