factoring through |_| and summary of "joins of hprops"

[Nicolai Kraus]

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.

[Michael Shulman]

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

> ...

> D) The factorization can be done if X is the coproduct of two propositions,
> 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
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

[Martin Escardo]

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

[Nicolai Kraus]

Thanks! Yes, I agree; we should not call those maps "constant". The
property is useful and should have a name though; if we don't want
"constant", we have to think about something else.
Nicolai

[Michael Shulman]

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

[Martin Escardo]

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.

[Michael Shulman]

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.

[Jason Gross]

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  

[Martin Escardo]

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:

[Guillaume Brunerie]

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

[Michael Shulman]

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.

[Nicolai Kraus]

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

[Guillaume Brunerie]

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

[Michael Shulman]

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

[Peter LeFanu Lumsdaine]

One possible objection to the definition "equal to a function of the form (fun x => y0)" is that the unique function from the empty set to itself is then not constant. Classical usage would perhaps be better captured by "if ||X||, then f is equal to a function of the form (fun x => y0)". I don't think I'd argue that that's actually the better definition, though :-)

-p.

Sent from my iPhone.

[Martin Escardo]

The type of such constant functions X->Y is not equivalent to Y if X
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

[Guillaume Brunerie]

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

[Martin Escardo]

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
maps X->Y are equal.

Martin

[Martin Escardo]

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

Martin

[Peter LeFanu Lumsdaine]

"Being constant" is not just an hprop, though (in this definition), so equality of constant functions is not just equality of their underlying functions.

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.

[Michael Shulman]

I'm not saying that your notion of "constant" isn't interesting, just
that it doesn't deserve the name "constant".

[Michael Shulman]

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

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

[Andrej Bauer]

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

1. steady function
2. static function
3. invariable function

[Martin Escardo]

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

[Guillaume Brunerie]

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.

[Robert Harper]

how about merely constant vs manifestly constant?

(sent from handheld)

[Martin Escardo]

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

In fact (our TLCA paper this year with Nicolai, Thierry, and
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

[Martin Escardo]

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

Sorry.

[Martin Escardo]

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

[Nicolai Kraus]

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

[Martin Escardo]

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.

[Michael Shulman]

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

[Nicolai Kraus]

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

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