3 views

Skip to first unread message

Jul 23, 2013, 7:29:45 PM7/23/13

to homotopyt...@googlegroups.com

The recent discussion on "joins of hprops" has motivated another

factorization result.

Let's first summarize some steps of the discussion:

Let P and Q be two h-propositions.

1. As Mike said in the very beginning, their join P*Q (i.e. the pushout

of P <- PxQ -> Q) is equivalent to ||P+Q||.

This is noteworthy as the pushout has a stronger induction principle

than ||P+Q||.

2. Martin asked whether ||P+Q|| has the universal property of the

pushout even without assuming that the pushout exists.

Put differently: Is ||P+Q|| in HoTT with HITs really so much stronger

than in HoTT without HITs?

3. Martin then rephrased the question: Given a constant function f : P+Q

-> X, can we factorize it through |-|? In particular, can we construct a

function ||P+Q|| -> X?

Here (and for the rest of my message), a function g : X -> Y is

"constant" iff (x x' : X) -> g(x) = g(x').

This latter question is interesting. In fact, this has already been

discussed a couple of times. Favonia asked on the UF mailing list

whether a constant function X -> Y can be factorized through ||X||; that

discussion can be found at [1]. In that discussion, I have argued that

this cannot be possible in general due to coherence issues, which would

force us to make a non-canonical choice of paths at some point. The

construction would then allow us to "create non-trivial paths out of

nothing". That is not a very satisfactory argument but I still don't

know a better one. However, there are some cases where we can do it:

Given a constant f : X -> Y, we can construct f' : ||X|| -> Y such that

f' . |-| = f in each of the following cases:

A) We know a point x: X. This is trivial: We can just take "const f(x)"

for f'.

B) Y is a set (has unique equality proofs). This works because all

coherence problems are solved automatically in that case.

C) We have any function h : Y -> X. Then, the coherence issues are still

there, but we can suddenly make a non-canonical choice. The intuition is

that a constant function X -> Y induces some "asymmetry" in Y (the point

that serves as the image is special). To make the non-canonical choice,

we need some "asymmetry" in X; and our assumption allows us to transfer

this asymmetry from Y to X. There is some detailed proof in this

blogpost [2]. (note that the composition of h and f is a constant

endofunction).

With the help of Christian Sattler, I showed that the answer to question

3 above is positive. So, we also get

D) The factorization can be done if X is the coproduct of two

propositions, X = P+Q. The reason why it works here is that we can

choose to "ignore" most of the constancy proof; all we really need is a

path from f(inl p) to f(inr q), should p and q exist. Such a "single"

path does not cause coherence problems. Formalizing the proof is quite

laborious, it can be found at [3]. Under the links, I paste a

prose-version of the proof (a combination of emails from Christian and

myself) if someone is interested (my Agda file is not very readable).

This means that ||P+Q|| has the property of the pushout even in HoTT

without HITs.

Here are some links to the sources mentioned above:

[1]

https://groups.google.com/forum/#!topic/univalent-foundations/MiC6smfhcEw

[2]

http://homotopytypetheory.org/2012/11/27/on-h-propositional-reflection-and-hedbergs-theorem/

[3] http://red.cs.nott.ac.uk/~ngk/Factorize/Own.Factor-const-from-prop.html

Here is one more surprising thing: Given propositions P,Q,R and a

constant map f : P+Q+R -> Y. Does it factorize through ||P+Q+R|| ? This

seems as if it was doable by just using the argument of D twice. In

general, one would think that, by an obvious induction, a constant map

from a finite sum of propositions lifts through ||-||.

Well, I strongly believe that this is *not* the case. Even for three

propositions, we cannot do the factorization. (We could if we had

additional coherence information on f, which we don't have.) While we

can get a map ||P+Q|| +R -> Y, it is probably impossible to show that

this map is constant, and that's why we cannot do the induction.

Best,

Nicolai

=== "attachment" : proof of D ===

Given

f : P+Q -> X

c : (p:P) -> (q:Q) -> f(inl p) = f(inr q).

(Note that c can be constructed from the proof that f is constant; this

is where we "forget" the potentially non-coherent information).

We will define a map ||P+Q|| -> X.

Define A to be the Sigma-type with the following components (it uses

three Sigmas):

x : X

s : (p:P) -> f(inl p) = x

t : (q:Q) -> f(inr q) = x

(p:P) -> (q:Q) -> (s p) . !(t q) = c p q

There is a map

||P+Q|| x A -> X

(just a projection, it's the first component of A)

There is also a map

P+Q -> ||P+Q|| x A

(inl p) mapsto |inl p| , f(inl p) , \p' -> [some trivial proof] , \q

-> !(c p q) , \p -> \q -> [some canonical proof]

(inr q) analogously

The important observation is that ||P+Q|| x A is a proposition (shown

below), meaning that we also get a map ||P+Q|| -> ||P+Q|| x A. The map

that we want to find is thus such a composition with the projection

mentioned above.

So, why is ||P+Q|| x A a proposition? It is enough to show that, under

the assumption ||P+Q||, the type A is a proposition. As "being a

proposition" is a proposition, we can even assume P+Q. So, we actually

may assume that we are given p:P [or the symmetric case q:Q].

In that case, the first two components of A can be written as "path-to

f(inl p)", the second two can be written as (q:Q) -> path-to (!(s p) . c

p q) or similar. Christian has spelled out the chain of type

isomorphisms as follows:

Assume we have p_0 : P. First "recall" that given c_0 : C and (c : C) ->

c_0 = c, we have

[1] (c : C) -> X c equivalent to X c_0

[2] (c : C) x X c equivalent to X c_0

We should now have the following chain of equivalences:

x : X

s : (p:P) -> f(inl p) = x

t : (q:Q) -> f(inr q) = x

(p:P) -> (q:Q) -> (s p) . !(t q) = c p q

-- permute s and t:

x : X

t : (q:Q) -> f(inr q) = x

s : (p:P) -> f(inl p) = x

(p:P) -> (q:Q) -> (s p) . !(t q) = c p q

-- reverse "axiom of choice":

x : X

t : (q:Q) -> f(inr q) = x

(p:P) ->

s : f(inl p) = x

(q:Q) -> (s p) . !(t q) = c p q

-- property [1]:

x : X

t : (q:Q) -> f(inr q) = x

s : f(inl p_0) = x

(q:Q) -> s . !(t q) = c p_0 q

-- permute t and s:

x : X

s : f(inl p_0) = x

t : (q:Q) -> f(inr q) = x

(q:Q) -> s . !(t q) = c p q

-- definition of path-from:

(x, s) : path-from(f(inl p_0))

t : (q:Q) -> f(inr q) = x

(q:Q) -> s . !(t q) = c p q

-- property [2]:

t : (q:Q) -> f(inr q) = f(inl p_0)

(q:Q) -> refl . !(t q) = c p q

-- reverse "axiom of choice" (and basic path rules):

(q:Q) ->

t : f(inr q) = f(inl p_0)

t q = !(c p q)

-- definition of path-to:

(q:Q) -> path-to(!(c p_0 q))

... and now, just use that path-to is contractible.

factorization result.

Let's first summarize some steps of the discussion:

Let P and Q be two h-propositions.

1. As Mike said in the very beginning, their join P*Q (i.e. the pushout

of P <- PxQ -> Q) is equivalent to ||P+Q||.

This is noteworthy as the pushout has a stronger induction principle

than ||P+Q||.

2. Martin asked whether ||P+Q|| has the universal property of the

pushout even without assuming that the pushout exists.

Put differently: Is ||P+Q|| in HoTT with HITs really so much stronger

than in HoTT without HITs?

3. Martin then rephrased the question: Given a constant function f : P+Q

-> X, can we factorize it through |-|? In particular, can we construct a

function ||P+Q|| -> X?

Here (and for the rest of my message), a function g : X -> Y is

"constant" iff (x x' : X) -> g(x) = g(x').

This latter question is interesting. In fact, this has already been

discussed a couple of times. Favonia asked on the UF mailing list

whether a constant function X -> Y can be factorized through ||X||; that

discussion can be found at [1]. In that discussion, I have argued that

this cannot be possible in general due to coherence issues, which would

force us to make a non-canonical choice of paths at some point. The

construction would then allow us to "create non-trivial paths out of

nothing". That is not a very satisfactory argument but I still don't

know a better one. However, there are some cases where we can do it:

Given a constant f : X -> Y, we can construct f' : ||X|| -> Y such that

f' . |-| = f in each of the following cases:

A) We know a point x: X. This is trivial: We can just take "const f(x)"

for f'.

B) Y is a set (has unique equality proofs). This works because all

coherence problems are solved automatically in that case.

C) We have any function h : Y -> X. Then, the coherence issues are still

there, but we can suddenly make a non-canonical choice. The intuition is

that a constant function X -> Y induces some "asymmetry" in Y (the point

that serves as the image is special). To make the non-canonical choice,

we need some "asymmetry" in X; and our assumption allows us to transfer

this asymmetry from Y to X. There is some detailed proof in this

blogpost [2]. (note that the composition of h and f is a constant

endofunction).

With the help of Christian Sattler, I showed that the answer to question

3 above is positive. So, we also get

D) The factorization can be done if X is the coproduct of two

propositions, X = P+Q. The reason why it works here is that we can

choose to "ignore" most of the constancy proof; all we really need is a

path from f(inl p) to f(inr q), should p and q exist. Such a "single"

path does not cause coherence problems. Formalizing the proof is quite

laborious, it can be found at [3]. Under the links, I paste a

prose-version of the proof (a combination of emails from Christian and

myself) if someone is interested (my Agda file is not very readable).

This means that ||P+Q|| has the property of the pushout even in HoTT

without HITs.

Here are some links to the sources mentioned above:

[1]

https://groups.google.com/forum/#!topic/univalent-foundations/MiC6smfhcEw

[2]

http://homotopytypetheory.org/2012/11/27/on-h-propositional-reflection-and-hedbergs-theorem/

[3] http://red.cs.nott.ac.uk/~ngk/Factorize/Own.Factor-const-from-prop.html

Here is one more surprising thing: Given propositions P,Q,R and a

constant map f : P+Q+R -> Y. Does it factorize through ||P+Q+R|| ? This

seems as if it was doable by just using the argument of D twice. In

general, one would think that, by an obvious induction, a constant map

from a finite sum of propositions lifts through ||-||.

Well, I strongly believe that this is *not* the case. Even for three

propositions, we cannot do the factorization. (We could if we had

additional coherence information on f, which we don't have.) While we

can get a map ||P+Q|| +R -> Y, it is probably impossible to show that

this map is constant, and that's why we cannot do the induction.

Best,

Nicolai

=== "attachment" : proof of D ===

Given

f : P+Q -> X

c : (p:P) -> (q:Q) -> f(inl p) = f(inr q).

(Note that c can be constructed from the proof that f is constant; this

is where we "forget" the potentially non-coherent information).

We will define a map ||P+Q|| -> X.

Define A to be the Sigma-type with the following components (it uses

three Sigmas):

x : X

s : (p:P) -> f(inl p) = x

t : (q:Q) -> f(inr q) = x

(p:P) -> (q:Q) -> (s p) . !(t q) = c p q

There is a map

||P+Q|| x A -> X

(just a projection, it's the first component of A)

There is also a map

P+Q -> ||P+Q|| x A

(inl p) mapsto |inl p| , f(inl p) , \p' -> [some trivial proof] , \q

-> !(c p q) , \p -> \q -> [some canonical proof]

(inr q) analogously

The important observation is that ||P+Q|| x A is a proposition (shown

below), meaning that we also get a map ||P+Q|| -> ||P+Q|| x A. The map

that we want to find is thus such a composition with the projection

mentioned above.

So, why is ||P+Q|| x A a proposition? It is enough to show that, under

the assumption ||P+Q||, the type A is a proposition. As "being a

proposition" is a proposition, we can even assume P+Q. So, we actually

may assume that we are given p:P [or the symmetric case q:Q].

In that case, the first two components of A can be written as "path-to

f(inl p)", the second two can be written as (q:Q) -> path-to (!(s p) . c

p q) or similar. Christian has spelled out the chain of type

isomorphisms as follows:

Assume we have p_0 : P. First "recall" that given c_0 : C and (c : C) ->

c_0 = c, we have

[1] (c : C) -> X c equivalent to X c_0

[2] (c : C) x X c equivalent to X c_0

We should now have the following chain of equivalences:

x : X

s : (p:P) -> f(inl p) = x

t : (q:Q) -> f(inr q) = x

(p:P) -> (q:Q) -> (s p) . !(t q) = c p q

-- permute s and t:

x : X

t : (q:Q) -> f(inr q) = x

s : (p:P) -> f(inl p) = x

(p:P) -> (q:Q) -> (s p) . !(t q) = c p q

-- reverse "axiom of choice":

x : X

t : (q:Q) -> f(inr q) = x

(p:P) ->

s : f(inl p) = x

(q:Q) -> (s p) . !(t q) = c p q

-- property [1]:

x : X

t : (q:Q) -> f(inr q) = x

s : f(inl p_0) = x

(q:Q) -> s . !(t q) = c p_0 q

-- permute t and s:

x : X

s : f(inl p_0) = x

t : (q:Q) -> f(inr q) = x

(q:Q) -> s . !(t q) = c p q

-- definition of path-from:

(x, s) : path-from(f(inl p_0))

t : (q:Q) -> f(inr q) = x

(q:Q) -> s . !(t q) = c p q

-- property [2]:

t : (q:Q) -> f(inr q) = f(inl p_0)

(q:Q) -> refl . !(t q) = c p q

-- reverse "axiom of choice" (and basic path rules):

(q:Q) ->

t : f(inr q) = f(inl p_0)

t q = !(c p q)

-- definition of path-to:

(q:Q) -> path-to(!(c p_0 q))

... and now, just use that path-to is contractible.

Jul 23, 2013, 7:40:15 PM7/23/13

to Nicolai Kraus, homotopyt...@googlegroups.com

Very nice!

On Tue, Jul 23, 2013 at 4:29 PM, Nicolai Kraus <nicola...@gmail.com> wrote:

> Favonia asked on the UF mailing list whether a

> constant function X -> Y can be factorized through ||X||

> ...

points of the circle makes a strong argument that maps of this sort

(having the property that (x x' : X) -> g(x) = g(x')) should not be

called "constant". The map P+Q -> S^1 together with its "constancy

proof" is not really "constant" in any homotopical sense of the word:

it goes *around* the circle!

Mike

On Tue, Jul 23, 2013 at 4:29 PM, Nicolai Kraus <nicola...@gmail.com> wrote:

> Favonia asked on the UF mailing list whether a

> constant function X -> Y can be factorized through ||X||

> D) The factorization can be done if X is the coproduct of two propositions,

> X = P+Q.

> ...
> X = P+Q.

> This means that ||P+Q|| has the property of the pushout even in HoTT without

> HITs.

For what it's worth, I think the fact that this produces nonstandard
> HITs.

points of the circle makes a strong argument that maps of this sort

(having the property that (x x' : X) -> g(x) = g(x')) should not be

called "constant". The map P+Q -> S^1 together with its "constancy

proof" is not really "constant" in any homotopical sense of the word:

it goes *around* the circle!

Mike

Jul 23, 2013, 7:47:24 PM7/23/13

to Nicolai Kraus, homotopyt...@googlegroups.com

This is very nice (as discussed privately among some of us in the last

few days).

It shows that ||P+Q|| has the universal property of P*Q without

postulating a HIT for _*_.

With P=1 and Q=1, this generalizes the fact that ||1+1|| has the

universal property of the interval. Almost. As a future development, I

would like to see the correct behaviour for the analogue of seg in the

interval, and also the induction principle for your situation.

The observation about ||P+Q+R|| is nice, and it resonates with my

thoughts about factorizations of constant functions through ||-||.

A question we discussed (the two of us) a few weeks ago was whether

the assertion that all constant functions X->Y factor through ||X||

should be a constructive taboo or a homotopical taboo. I would like to

make this public, particularly after Mike's message of a few minutes

ago.

In any case, there is still a remote possibility that the

factorization is possible in general, even in the case

X=||P+Q+R||. But I very much doubt that.

Martin

Jul 23, 2013, 7:49:31 PM7/23/13

to Michael Shulman, homotopyt...@googlegroups.com

property is useful and should have a name though; if we don't want

"constant", we have to think about something else.

Nicolai

Jul 23, 2013, 7:51:20 PM7/23/13

to Nicolai Kraus, homotopyt...@googlegroups.com

We could always use something like "quasi-constant", at least until

someone thinks of a better name.

> --

> 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/groups/opt_out.

>

>

someone thinks of a better name.

> 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/groups/opt_out.

>

>

Jul 23, 2013, 8:03:25 PM7/23/13

to Michael Shulman, Nicolai Kraus, homotopyt...@googlegroups.com

On 24/07/13 00:40, Michael Shulman wrote:

> For what it's worth, I think the fact that this produces nonstandard

> points of the circle makes a strong argument that maps of this sort

> (having the property that (x x' : X) -> g(x) = g(x')) should not be

> called "constant".

I agree with that, provided you give up using the symbol "=" for paths.
> points of the circle makes a strong argument that maps of this sort

> (having the property that (x x' : X) -> g(x) = g(x')) should not be

> called "constant".

Jul 23, 2013, 8:13:31 PM7/23/13

to Martin Escardo, Nicolai Kraus, homotopyt...@googlegroups.com

No, it's totally different. Isomorphism/equivalence is the only

meaningful notion of equality between types. But there is another

perfectly good, and more sensible, meaning of "constant function",

namely \x -> y0 for some y0:Y.

meaningful notion of equality between types. But there is another

perfectly good, and more sensible, meaning of "constant function",

namely \x -> y0 for some y0:Y.

Jul 23, 2013, 8:15:10 PM7/23/13

to Martin Escardo, Michael Shulman, Nicolai Kraus, homotopyt...@googlegroups.com

Does this this property induce some kind of contractility result, in the same way that (x x' : X) -> x = x' implies that X is contractible? It seems to me that this is saying that the image g(X) is contractible, though I'm not sure if this is phrasible in HoTT.

-Jason

Jul 23, 2013, 8:22:13 PM7/23/13

to Nicolai Kraus, homotopyt...@googlegroups.com

One further remark. This result constitutes a further non-trivial

advance to our knowledge.

We knew that the factorization problem through ||-|| for constant

functions X->Y is possible if ||X|->X or if Y is an hset.

However, if ||P+Q||->P+Q for all hpropositions P and Q, then all types

have decidable equality (we proved this in our TLCA paper this year).

Hence this gives an example of a possible factorization without

assuming ||X|->X or Y hset.

Best,

Martin

On 24/07/13 00:29, Nicolai Kraus wrote:

On 24/07/13 00:29, Nicolai Kraus wrote:

Jul 23, 2013, 8:23:50 PM7/23/13

to Michael Shulman, Martin Escardo, Nicolai Kraus, homotopyt...@googlegroups.com

Are you suggesting that a good definition of "constant" is "equal to a function of the form \x -> y0"?

This definition has exactly the same problems as "quasi-constant", for instance the obvious function Bool -> Circle is constant in a lot of different ways.

Guillaume

Jul 23, 2013, 8:28:58 PM7/23/13

to Guillaume Brunerie, Martin Escardo, Nicolai Kraus, homotopyt...@googlegroups.com

On Tue, Jul 23, 2013 at 5:23 PM, Guillaume Brunerie

<guillaume...@gmail.com> wrote:

> Are you suggesting that a good definition of "constant" is "equal to a

> function of the form \x -> y0"?

>

> This definition has exactly the same problems as "quasi-constant", for

> instance the obvious function Bool -> Circle is constant in a lot of

> different ways.

Why is that a problem (and why is it the same problem)? Note that
<guillaume...@gmail.com> wrote:

> Are you suggesting that a good definition of "constant" is "equal to a

> function of the form \x -> y0"?

>

> This definition has exactly the same problems as "quasi-constant", for

> instance the obvious function Bool -> Circle is constant in a lot of

> different ways.

with such a definition, the type of all constant functions

\sm{f:X->Y}{y0:Y} (f = \lam{x} y0)

is equivalent to Y, which seems sensible to me: to give a constant

function is exactly to give the point at which it is constant.

Jul 23, 2013, 8:42:49 PM7/23/13

to Jason Gross, Martin Escardo, Michael Shulman, homotopyt...@googlegroups.com

On 24/07/13 01:15, Jason Gross wrote:

Does this this property induce some kind of contractility result, in the same way that (x x' : X) -> x = x' implies that X is contractible? It seems to me that this is saying that the image g(X) is contractible, though I'm not sure if this is phrasible in HoTT.

-Jason

Good question. My understanding is that this is how the
factorization is done. We try to factorize f : X -> Y by
"expressing the image f(X) as a proposition".

This is all really informally though.

When you say "the image of f", I think about [at most] two points in Y. Then, the constancy proof gives us in total four paths: Two of them are loops, the other two are in opposite directions (but not necessarily inverses!). The combination of points and paths will not be coherent / will not be a proposition. The trick is that we can safely forget the loops and one of the two paths between the points. Thus, we have reduced the "image of f" to two points with only one path between them. Now, that is contractible, so there is no reason any more why the factorization should fail, and indeed, it works.

But that's just for intuition. I don't see what kind of other contractibility result it could give us.

-- Nicolai

This is all really informally though.

When you say "the image of f", I think about [at most] two points in Y. Then, the constancy proof gives us in total four paths: Two of them are loops, the other two are in opposite directions (but not necessarily inverses!). The combination of points and paths will not be coherent / will not be a proposition. The trick is that we can safely forget the loops and one of the two paths between the points. Thus, we have reduced the "image of f" to two points with only one path between them. Now, that is contractible, so there is no reason any more why the factorization should fail, and indeed, it works.

But that's just for intuition. I don't see what kind of other contractibility result it could give us.

-- Nicolai

Jul 23, 2013, 8:49:24 PM7/23/13

to Michael Shulman, Martin Escardo, Nicolai Kraus, homotopyt...@googlegroups.com

Right, sorry. I was thinking that at least when X is inhabited you get the same definition as "quasi-constant", but that's wrong, with your definition there are no more coherence issues.

Guillaume

Jul 24, 2013, 1:03:01 AM7/24/13

to Nicolai Kraus, homotopyt...@googlegroups.com

On Tue, Jul 23, 2013 at 4:29 PM, Nicolai Kraus <nicola...@gmail.com> wrote:

> Even for three

> propositions, we cannot do the factorization. (We could if we had additional

> coherence information on f, which we don't have.)

Indeed, the join argument shows that ||P+Q+R|| is equivalent to the
> propositions, we cannot do the factorization. (We could if we had additional

> coherence information on f, which we don't have.)

triple join P*Q*R, which doesn't only join everything in P to

everything in Q and similarly P to R and Q to R, but also contains a

coherence between the joining paths if P /\ Q /\ R.

Here is a proposed counterexample to the factorization for three

propositions, which is essentially the "universal" one. Consider the

triple pushout of P, Q, and R over PxQ, PxR, and QxR, i.e. the type Y

with point-constructors inP:P->Y, inQ:Q->Y, inR:R->Y and

path-constructors (p:P)->(q:Q)->inP p = inQ q and two more similar

ones (but no triple coherence). Then we have an obvious map P+Q+R ->

Y, but there are models in which ||P+Q+R||=1 but Y has no global

element.

The most straightforward such model is presheaves on the poset of

proper subsets of {a,b,c}, with P={a,b}, Q={b,c}, and R={a,c}. In

this model, we have Y(S) = 1 for all nonempty proper subsets S, while

Y(\emptyset) = S^1, and it's easy to see that Y has no global

sections.

Mike

Jul 24, 2013, 3:14:57 AM7/24/13

to Michael Shulman, Guillaume Brunerie, Martin Escardo, Nicolai Kraus, homotopyt...@googlegroups.com

-p.

Sent from my iPhone.

Jul 24, 2013, 7:32:32 AM7/24/13

to Michael Shulman, Guillaume Brunerie, Nicolai Kraus, homotopyt...@googlegroups.com

is empty.

And, if you restrict attention to pointed types X, then the two

notions of constancy are equivalent. So the only difference is when X

is potentially empty, and that you require Y to be pointed.

Here is an interesting example. Let a:N->2 be a binary sequence and let

X = {n : N | a n = 1}.

Then knowing whether or not X is inhabited is equivalent to LPO, a

constructive taboo. Nevertheless, you can define a constant function

f : X -> X

by f(n,p) = (least m<=n such that q:a m = 1, q).

Because we know that a type A admits a constant function A->A if and

only if we have a choice function ||A||->A, we conclude that

||Sigma n:N, a n = 1|| -> Sigma n:N, a n = 1.

This gives another proof of a fact we already know.

This also shows that the statement "every type has a constant endomap"

contradicts univalence, because it is equivalent to "every type X has

a choice function ||X||->X". So here we have a HoTT

taboo. Interestingly, this assumption also gives a constructive taboo,

in pure intensional MLTT (without any postulate): if every type has a

constant endofunction, then every type has decidable equality.

Another example is Hedberg's theorem: a type X is an hset iff every

path space x=y has a constant endomap. Because equality is not

decidable in general, for this theorem you need the definition of

constancy that allows the possibility that x=y is empty.

A third example is this. The following function is constant but we

don't know whether the domain is inhabited in general, unless we have

decidable equality. Take any type X, and three points x,a,b. Define

f:(x=a)+(x=b)->U

by

f(inl p)=(x=a)

f(inr q)=(x=b).

If you have p:x=a and q:x=b, then (x=a)=(x=b)=(a=b) and hence the

function is constant. It is an interesting puzzle (considered by

Nicolai and myself) to factor f through ||(x=a)+(x=b)|| (without using

the general theorem proved by Nicolai, or the previous version by

Guillaume and you).

A fourth example is this. For a type X, let CX be the type of constant

endomaps of X, and let DX=(CX->X). Without knowing whether X is empty,

we cannot know whether DX is empty. Nevertheless, there is a constant map

F : DX->DX

defined by, for all g:CX->X and f:CX

F(g)(f)=f(g f).

(I am deliberately uncareful here for the sake of making this

readable. This definition works in set theory, but in type theory you

need to fill in more data.)

Now the type of fixed points of any constant endomap is an

hproposition. We call the type of fixed points of F "populated X". It

has the property it is exactly the assumption needed to get a point

out of a constant endomap X->X.

It is equivalent to the large type

for every hprop P, if P is logically equivalent to X, then P holds.

So, this notion of constancy may be weird, but it is quite interesting

and I would say useful (e.g. Hedberg). We know that

(constant maps X->X) ~ (choice functions ||X||->X).

The more general question is whether

(constant maps X->Y) ~ (functions ||X||->Y).

This looks plausible at first sight, and unplausible when you look at

it more deeply, as already discussed. Is it a HoTT taboo and/or a

constructive taboo? What makes this difficult is that it holds if X

has a choice function ||X||->X (in particular if X is empty or

inhabited) or if Y is an hset. Perhaps this indicates that a

constructive taboo won't be possible, because it is (computationally)

consistent with MLTT that all types are hsets.

Best,

Martin

Jul 24, 2013, 7:52:55 AM7/24/13

to Martin Escardo, Nicolai Kraus, homotopyt...@googlegroups.com, Michael Shulman

Le 24 juil. 2013 13:29, "Martin Escardo" <escardo...@googlemail.com> a écrit :

>

> On 24/07/13 01:28, Michael Shulman wrote:

>>

>> On Tue, Jul 23, 2013 at 5:23 PM, Guillaume Brunerie

>> <guillaume...@gmail.com> wrote:

>>>

>>> Are you suggesting that a good definition of "constant" is "equal to a

>>> function of the form \x -> y0"?

>>>

>>> This definition has exactly the same problems as "quasi-constant", for

>>> instance the obvious function Bool -> Circle is constant in a lot of

>>> different ways.

>>

>>

>> Why is that a problem (and why is it the same problem)? Note that

>> with such a definition, the type of all constant functions

>>

>> \sm{f:X->Y}{y0:Y} (f = \lam{x} y0)

>>

>> is equivalent to Y, which seems sensible to me: to give a constant

>> function is exactly to give the point at which it is constant.

>

>

> The type of such constant functions X->Y is not equivalent to Y if X

> is empty.

Yes it is. A constant function is a map f : X -> Y together with a y0 : Y and an equality f = \x -> y0.

When X is empty, such a constant function is just a point in Y.

> And, if you restrict attention to pointed types X, then the two

> notions of constancy are equivalent. So the only difference is when X

> is potentially empty, and that you require Y to be pointed.

They are logically equivalent but not equivalent. For instance there are Circle-many constant maps Unit -> Circle but (Circle × Int)-many such quasi-constant maps (because you need to provide an additional proof that f(tt) = f(tt))

Guillaume

Jul 24, 2013, 8:50:19 AM7/24/13

to Guillaume Brunerie, Nicolai Kraus, homotopyt...@googlegroups.com, Michael Shulman

On 24/07/13 12:52, Guillaume Brunerie wrote:

> > The type of such constant functions X->Y is not equivalent to Y if X

> > is empty.

>

> Yes it is. A constant function is a map f : X -> Y together with a y0 :

> Y and an equality f = \x -> y0.

> When X is empty, such a constant function is just a point in Y.

When X is empty, all maps X->Y are equal, and in particular all constant
> > The type of such constant functions X->Y is not equivalent to Y if X

> > is empty.

>

> Yes it is. A constant function is a map f : X -> Y together with a y0 :

> Y and an equality f = \x -> y0.

> When X is empty, such a constant function is just a point in Y.

maps X->Y are equal.

Martin

Jul 24, 2013, 8:56:16 AM7/24/13

to Guillaume Brunerie, Nicolai Kraus, homotopyt...@googlegroups.com, Michael Shulman

Martin

Jul 24, 2013, 8:54:03 AM7/24/13

to Martin Escardo, Guillaume Brunerie, Nicolai Kraus, homotopyt...@googlegroups.com, Michael Shulman

To see that (for any X) this type of constant functions is equivalent to Y, just reorder the data: it consists of a point y0, a function f, and an equality proof h : f = (fun _ -> y0). But the space of such pairs (f,h) is always contractible: it's the homotopy singleton of (fun _ -> y0). So the data consists essentially just of the point y0 : Y.

-p.

Jul 24, 2013, 11:48:37 AM7/24/13

to Martin Escardo, homotopyt...@googlegroups.com

I'm not saying that your notion of "constant" isn't interesting, just

that it doesn't deserve the name "constant".

that it doesn't deserve the name "constant".

Jul 24, 2013, 12:07:18 PM7/24/13

to Martin Escardo, homotopyt...@googlegroups.com

On Wed, Jul 24, 2013 at 5:56 AM, Martin Escardo

<escardo...@googlemail.com> wrote:

> Oh, I see. Your definition of constant map has y0 as data. Sorry.

You may be thinking of the related notion of a "merely constant" function. (-:
<escardo...@googlemail.com> wrote:

> Oh, I see. Your definition of constant map has y0 as data. Sorry.

Here is another way to think of it. Suppose f:X->Y. On the one hand,

we can consider the property that we are unable to detect any

variation in the values of f. That is, no matter what inputs x1, x2

we take, the value of f on these two inputs is the same, f(x1) =

f(x2). On the other hand, we can consider the property that there is

a specific witness to the fact that f does not vary, i.e. a point y0:Y

such that f(x) = y0 for all x:X.

I would argue that the latter is a more "constructive" notion of

constancy. For the former, it seems to me that a natural name would

be something like "variationless". (I would be tempted by

"non-varying" except that that might suggest instead the classically

equivalent negative notion of there not existing x1,x2:X such that

f(x1) \neq f(x2). And "invariant" unfortunately has too many other

meanings.)

Mike

Jul 25, 2013, 3:06:57 AM7/25/13

to homotopyt...@googlegroups.com

How about one of these (in order of my personal preference):

1. steady function

2. static function

3. invariable function

1. steady function

2. static function

3. invariable function

Jul 25, 2013, 4:51:03 AM7/25/13

to Andrej Bauer, homotopyt...@googlegroups.com

With apologies to all, I will stick to "constant". The only interesting

theorems I know so far about constant functions apply to this notion of

constancy (any two values of the function are the same). Martin

theorems I know so far about constant functions apply to this notion of

constancy (any two values of the function are the same). Martin

Jul 25, 2013, 5:53:33 AM7/25/13

to Martin Escardo, Andrej Bauer, homotopyt...@googlegroups.com

Do you have any real-world example of a constant function X -> Y (in your sense) for which you cannot prove (or it's difficult to prove) that it factors through ||X|| ?

For instance you gave earlier the example of given a : Nat -> Bool and X = {n : Nat | a n = 1}, there is a constant function f : X -> X defined by f n = (the smallest m <= n such that a m = 1).

Let's prove that this map factors through ||X||.

Consider the type A = {n : Nat | a n = 1 and for all m < n, a m = 0}. A is the type of all smallest n such that a n = 1.

It's easy to see that A is a prop (there is at most one smallest such n), and moreover there is a map X -> A : if there is some n0 such that a n0 = 1, then there is a smallest one because you can check everyone below n0.

Hence there is a map ||X|| -> A and it's easy to see that the composition X -> ||X|| -> A -fst-> X is the map f above.

Guillaume

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/groups/opt_out.

--

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.

Jul 25, 2013, 6:44:45 AM7/25/13

to Andrej Bauer, homotopyt...@googlegroups.com

how about merely constant vs manifestly constant?

(sent from handheld)

(sent from handheld)

Jul 25, 2013, 7:03:54 AM7/25/13

to Guillaume Brunerie, Andrej Bauer, homotopyt...@googlegroups.com

On 25/07/13 10:53, Guillaume Brunerie wrote:

> Do you have any real-world example of a constant function X -> Y (in

> your sense) for which you cannot prove (or it's difficult to prove) that

> it factors through ||X|| ?

Hi Guillaume. This is precisely the question we (Nicolai and I) are
> Do you have any real-world example of a constant function X -> Y (in

> your sense) for which you cannot prove (or it's difficult to prove) that

> it factors through ||X|| ?

investigating.

> For instance you gave earlier the example of given a : Nat -> Bool and X

> = {n : Nat | a n = 1}, there is a constant function f : X -> X defined

> by f n = (the smallest m <= n such that a m = 1).

> Let's prove that this map factors through ||X||.

Thorsten): for any type X, every constant endomap X->X factors through

||X||. The question becomes difficult when you consider constant maps

X->Y when X and Y are not (known to be) the same.

The sketch of the proof for X=Y is this. The type of fixed points of

any constant X->X is an hproposition (non-trivial proof, due to

Nicolai), and the constant map factors through this type. Furthermore,

a constant map X->X factors through ||X|| if and only if it factors

through some hproposition P (easy).

For this you easily conclude that X admits a constant endomap if and

only it has a choice function ||X||->X.

In connection with my mistake yesterday, let's distinguish the type of

constant maps, and the property of being constant.

For *endomaps* several of the possibly different notions of constancy

agree with "any two values of the function are the same", which is the

one used for the above claims.

Here are some possible additions to Mike's list of notions of

constancy for functions f:X->Y (where some of which were already

mentioned in the IAS mailing list earlier this year, and (1)-(3) are

Mike's from his recent message):

(1) For all x1,x2:X, we have f(x1)=f(x2).

Then a type X is an hproposition <=> the identity function is

(1)-constant, <=> any function X->X is (1)-constant, <=> any

function A->X is (1)-constant.

(2) f factors through ||X||.

My Wild Question 3 of a message of a few days ago is equivalent to

asking whether there is at most one such factorization.

As remarked above, (1) implies (2) in the case X=Y. In the general

case, this should not be the case (Mike even gave a counter-model,

but I don't understand his argument at the moment).

However, the implication (1)=>(2) holds if X has a choice function

||X||->X, or if Y is an hset, or if X=||P+Q|| for hpropositions P

and Q, as shown by Nicolai and Settler a few days ago.

(3) There is y0:Y such that f = \x -> y0.

This forces Y to be inhabited, which the previous notions

don't. This is not equivalent to saying that f factors through 1,

because X may be 0. But if X=Y, this is equivalent to the

factorization through 1. Thus, and an hprop P, a function is

(3)-constant iff P=1.

(4) f factors through some (1)-constant function X->X.

Then, using the above, you get that any (4)-constant function X->Y

is (1)- and (2)-constant. ((1) is easy. As for (2), using the

constant function X->X, construct the choice function ||X||->X as

above, and then compose it with f.)

(4') X has some constant endomap (equivalently X has a choice function

||X||->X), and (1) holds.

This is equivalent to (4). From the endomap, you get the choice

function ||X||->X, and you compose that with f. Hence the

"factorization" part of (4) is superfluous.

(5) The image of f is an hproposition.

Because being an hprop is an hprop, the statement "f is

(5)-constant" is an hprop. This is in the spirit of (1),(2),(4).

For X=Y, (1),(2),(4),(5) are equivalent.

In general, condition (5) implies (2) and hence (1): This is easy:

just use the universal property of truncation.

(6) The image of f is contractible.

Again "f is (6)-constant" is an hproposition, and this time the

notion is in the spirit of (3), but doesn't allow X to be empty,

because it forces ||X|| to be inhabited.

This is in the spirit of (3).

(5) and (6) have the advantage that the constant functions (in

their respective sense) form a sub-type of the type of all

functions X->Y.

There are probably more naturally occurring notions of constancy. They

proliferate for three reasons (1) constructive, (2) homotopic, (3) the

decision on whether we should insist that a constant function has a

particular designated value.

For any of the notions, let K(X,Y) be the type of constant

functions. We have a map:

K(X,Y) -> (||X||->Y).

We can ask: Does it split? (This the factorization problem.) Is it

surjective? (This is ||the factorization problem||.)

Martin

Jul 25, 2013, 7:38:05 AM7/25/13

to Guillaume Brunerie, Andrej Bauer, homotopyt...@googlegroups.com

On 25/07/13 12:03, Martin Escardo wrote:

> For any of the notions, let K(X,Y) be the type of constant

> functions. We have a map:

>

> K(X,Y) -> (||X||->Y).

I mean a map in the other direction, by composing with |-|:X->||X||.
> For any of the notions, let K(X,Y) be the type of constant

> functions. We have a map:

>

> K(X,Y) -> (||X||->Y).

Sorry.

Jul 25, 2013, 9:49:16 AM7/25/13

to Guillaume Brunerie, Andrej Bauer, homotopyt...@googlegroups.com

On 25/07/13 10:53, Guillaume Brunerie wrote:

> Do you have any real-world example of a constant function X -> Y (in

> your sense) for which you cannot prove (or it's difficult to prove) that

> it factors through ||X|| ?

Following from my previous message, here is why this question is
> your sense) for which you cannot prove (or it's difficult to prove) that

> it factors through ||X|| ?

difficult. You would have to come up with a constant function (any two

values are the same) such that ||X||->X is not available (in particular

you don't know whether X is empty of inhabited) and Y is not an hset.

Even assuming this, the factorization may be possible, e.g. when

X=||P+Q|| (which you cannot know to have ||X||->X in general, as having

this in general gives you decidability of equality for all types, and

hence that all types are hsets, and hence that univalence fails).

Martin

Jul 25, 2013, 12:15:30 PM7/25/13

to HomotopyT...@googlegroups.com

Martin,

Thanks for sharing this. There is one part which I am puzzled about:

On 24/07/13 12:32, Martin Escardo wrote:

> A third example is this. The following function is constant but we

> don't know whether the domain is inhabited in general, unless we have

> decidable equality. Take any type X, and three points x,a,b. Define

>

> f:(x=a)+(x=b)->U

>

> by

>

> f(inl p)=(x=a)

> f(inr q)=(x=b).

>

> If you have p:x=a and q:x=b, then (x=a)=(x=b)=(a=b) and hence the

> function is constant. It is an interesting puzzle (considered by

> Nicolai and myself) to factor f through ||(x=a)+(x=b)|| (without using

> the general theorem proved by Nicolai, or the previous version by

> Guillaume and you).

Is this an application of the factorization of P+Q -> X? I don't see it.

(On the other hand, there is a trivial factorization in this case,

namely \_ -> x=x)

Nicolai

Thanks for sharing this. There is one part which I am puzzled about:

On 24/07/13 12:32, Martin Escardo wrote:

> A third example is this. The following function is constant but we

> don't know whether the domain is inhabited in general, unless we have

> decidable equality. Take any type X, and three points x,a,b. Define

>

> f:(x=a)+(x=b)->U

>

> by

>

> f(inl p)=(x=a)

> f(inr q)=(x=b).

>

> If you have p:x=a and q:x=b, then (x=a)=(x=b)=(a=b) and hence the

> function is constant. It is an interesting puzzle (considered by

> Nicolai and myself) to factor f through ||(x=a)+(x=b)|| (without using

> the general theorem proved by Nicolai, or the previous version by

> Guillaume and you).

(On the other hand, there is a trivial factorization in this case,

namely \_ -> x=x)

Nicolai

Jul 25, 2013, 12:42:11 PM7/25/13

to Nicolai Kraus, HomotopyT...@googlegroups.com

Well, you just gave the answer to the puzzle! (Which you had given

before privately to me.) Martin

PS. So you were puzzled about the puzzle.

before privately to me.) Martin

PS. So you were puzzled about the puzzle.

Jul 25, 2013, 12:58:42 PM7/25/13

to Martin Escardo, Andrej Bauer, homotopyt...@googlegroups.com

On Thu, Jul 25, 2013 at 1:51 AM, Martin Escardo

<escardo...@googlemail.com> wrote:

> With apologies to all, I will stick to "constant". The only interesting

> theorems I know so far about constant functions apply to this notion of

> constancy (any two values of the function are the same).

You probably won't like this, but I would probably argue that there
<escardo...@googlemail.com> wrote:

> With apologies to all, I will stick to "constant". The only interesting

> theorems I know so far about constant functions apply to this notion of

> constancy (any two values of the function are the same).

should *not* be interesting theorems about constant functions, because

they are like, y'know, *constant*. So the fact that the only

interesting theorems you know are about your definition is actually

more evidence that it should *not* be the one called "constant". The

reason the theorems are interesting is precisely because it's the

"wrong" notion in general, but in certain special cases it turns out

to be sufficient.

Mike

Jul 25, 2013, 12:59:16 PM7/25/13

to HomotopyT...@googlegroups.com

On 25/07/13 10:53, Guillaume Brunerie
wrote:

Do you have any real-world example of a constant function X -> Y (in your sense) for which you cannot prove (or it's difficult to prove) that it factors through ||X|| ?

A "real-world example"? That's an interesting notion, what does it
mean? Do you think about something that turns up whey you formalize
homotopy theory? That wouldn't be very objective though.

How about the following (similar to an earlier example that Martin wrote about, but with an important difference):

Given a type X and points a,b,c : X. Define

f : (a=b + b=c + c=a) -> Type

f (in1 p) := a=b

f (in2 q) := b=c

f (in3 r) := c=a

This map is "quasi-constant"/"constant" [maps any two inputs to equal values] as we have (a=b) = (a=a) as soon as a=b is inhabited, and so on.

Can you factorize this through ||a=b + b=c + c=a|| ? It seems that, in order to to this, you need to "guess" first which of the equalities might hold.

You could also consider the map with the same domain and pointed types (let's write Type*) as the codomain:

g : (a=b + b=c + c=a) -> Type*

g (in1 p) := (a=b , p)

g (in2 q) := (b=c , q)

g (in3 r) := (c=a , r)

This map is still "constant" (e.g. for the pairs (a=b , p) and (a=b , p') we prove that the first components are equal by using the isomorphism _.!p.p', the second components become equal trivially).

If you could factor it and get g: ||a=b + b=c + c=a|| -> Type*, you would have

g(|inl p|) = f(inl p) = (a=b , p)

This would be very strange - basically, you could recover p by applying g on |inl p|.

How about the following (similar to an earlier example that Martin wrote about, but with an important difference):

Given a type X and points a,b,c : X. Define

f : (a=b + b=c + c=a) -> Type

f (in1 p) := a=b

f (in2 q) := b=c

f (in3 r) := c=a

This map is "quasi-constant"/"constant" [maps any two inputs to equal values] as we have (a=b) = (a=a) as soon as a=b is inhabited, and so on.

Can you factorize this through ||a=b + b=c + c=a|| ? It seems that, in order to to this, you need to "guess" first which of the equalities might hold.

You could also consider the map with the same domain and pointed types (let's write Type*) as the codomain:

g : (a=b + b=c + c=a) -> Type*

g (in1 p) := (a=b , p)

g (in2 q) := (b=c , q)

g (in3 r) := (c=a , r)

This map is still "constant" (e.g. for the pairs (a=b , p) and (a=b , p') we prove that the first components are equal by using the isomorphism _.!p.p', the second components become equal trivially).

If you could factor it and get g: ||a=b + b=c + c=a|| -> Type*, you would have

g(|inl p|) = f(inl p) = (a=b , p)

This would be very strange - basically, you could recover p by applying g on |inl p|.

For instance you gave earlier the example of given a : Nat -> Bool and X = {n : Nat | a n = 1}, there is a constant function f : X -> X defined by f n = (the smallest m <= n such that a m = 1).

Let's prove that this map factors through ||X||.

Of course you can do that: As Martin said, this map is an
endofunction (point C in my original message), but not only this, it
also has an hset as codomain (point B in my original message).

Nicolai

P.S.: I don't like to argue about notation/names of properties, but basically I agree with Martin: "forall x y, fx = fy" seems to be the most interesting property. The other notion that Mike prefers is really "constant *at a point*", so it already has its own name in a natural way. You can argue that the first notion does not deserve the name "constant"; but neither does the second, I think...

Nicolai

P.S.: I don't like to argue about notation/names of properties, but basically I agree with Martin: "forall x y, fx = fy" seems to be the most interesting property. The other notion that Mike prefers is really "constant *at a point*", so it already has its own name in a natural way. You can argue that the first notion does not deserve the name "constant"; but neither does the second, I think...