characterisation of equivalencee

[Altenkirch Thorsten]

I am wondering again how to specify equivalence.

In the book, chapter 4, we say that is-equivalence should be logically equivalent to being quasi-invertible (which I was used to call "isomorphism") and it should be propositional.

This raises the following questions:

1. Why is quasi-invertible (I would call it isomorphic) logically the correct notion?
2. Maybe we don't want to specify equvalence as a property of a function being an equivalence. How do we specify equivalence directly?

Ad 1: I guess we can argue that "isomorphic" is in a sense maximal, that is if we would identify any non-isomorphic types then this is unsound.

Ad 2: Peter Lumsdaine suggested to say that A is equivalent to B if there is a relation such that both the left fibre and the right fibre are contractible, (e.g. Pi a:A.is-contr(Sigma b:B,a R b) and the symmetric version). I prefer this notion because it is obviously symmetric but it doesn't fit into the "property of a function" mould.

Actually what happens if we replace equivalence by isomorphic (in the univalence axiom)? That would be consistent with a 1-truncated theory but does it imply 1-truncatedness? I have a feeling I have discussed this already but I don't remember the answer.

Hence, what is a convincing specification of equivalence of types.

Thorsten

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

[Michael Shulman]

On Sat, Apr 19, 2014 at 8:24 AM, Altenkirch Thorsten
<psz...@exmail.nottingham.ac.uk> wrote:
> Ad 2: Peter Lumsdaine suggested to say that A is equivalent to B if there is
> a relation such that both the left fibre and the right fibre are
> contractible, (e.g. Pi a:A.is-contr(Sigma b:B,a R b) and the symmetric
> version). I prefer this notion because it is obviously symmetric but it
> doesn't fit into the "property of a function" mould.

Exercise 4.2 suggests to extract from this definition a "property of a
function". Presumably we had an answer in mind when we wrote that
exercise, but I don't remember offhand what it was.

Of course, this definition also has the disadvantage that it goes up a
universe level.

> Actually what happens if we replace equivalence by isomorphic (in the
> univalence axiom)? That would be consistent with a 1-truncated theory but
> does it imply 1-truncatedness? I have a feeling I have discussed this
> already but I don't remember the answer.

Exercise 4.6 (which I think was added to the book since initial
release) is to show that this property (which it calls
"qinv-univalence") is inconsistent, and has a sort of hint of a way to
go about it. Now that I think about it, possibly this exercise should
be clarified a bit, since as you point out, qinv-univalence is
consistent for a universe that contains only sets. The hint in the
exercise leads to a proof that if Bool : U_1 and U_1 : U_2, then it's
inconsistent for U_1 to be any sort of univalent and U_2 to be
qinv-univalent. A similar argument would show that it's inconsistent
to have S^1 : U where U is qinv-univalent. It's an interesting
question if we just have a single qinv-univalent universe U, whether
we can prove that all types in U are sets, or that U is a 1-type.

Mike

[Nicolai Kraus]

On 19/04/14 19:56, Michael Shulman wrote:
> It's an interesting question if we just have a single qinv-univalent
> universe U, whether we can prove that all types in U are sets, or that
> U is a 1-type.

I thought I can prove this but now I noticed that my argument only shows
something weaker: If A is a type in a qinv-univalent universe, any function
p : forall a, a=a
is constanly refl. I don't know whether we can go anywhere from here
(but at least it is a positive statement, compared to "is inconsistent").

It goes like this, it's very simple (if I have not made a mistake).
Let's write (A iso B) for "A and B are isomorphic" (i.e. f: A->B with
qinv(f)), and (A eqv B) for "A and B are equvialent" (in the usual sense).

A weak form of Lemma 4.1.1 tells us that we have
f_{AB} : (A iso B) -> ((A eqv B) x forall a, a=a).

Fix some type A. Consider the type family
P : (B : Type) -> (i : A iso B) -> forall a, (refl a) = snd (f_{AB}(i)) a

Let's construct, for any B and (i : A iso B), an inhabitant of (P B i).
qinv-univalence gives us "[based] isomorphism induction" (analogous to
"equivalence induction, Corollary 5.8.5), which says that we only need
to consider the case that i is the trivial isomorphism between A and A.
But in this case, the goal is immediately true (because of the way that
f_{AB} is defined).

Now, we use that Lemma 4.1.1 actually says that f_{AB} is an
equivalence. Thus, if we start with any term
p : forall a, a=a,
we can send the pair (identity equivalence on A , p) to (A iso A) using
the inverse of f, send it back using f, and conclude that (the second
projection of the result) is equal to p, but also equal to (constant refl).

Not sure whether that helps for the original question.
By the way, if we view "iso" as the first variant of "symmetric tries to
define equivalence", then the univalence based on the n-th variant will
also imply that every function of the type
forall a, Omega^n(A,a)
is equal to the one which is constanly trivial. (By "variants of
symmetric tries", I mean this: first variant is iso/qinv, which is just
functions back and forth with the two proofs that they are inverses. The
"correct" definition is then "half-adjoint", which adds one
coherence-condition. If we add the other one as well, we get what I mean
by "second variant of a symmetric try", which is again ill-behaved. We
can add another coherence condition (out of two canonical ones) to make
up for that, but if we add both, we get the "third symmetric try" ad so on.)

Nicolai

[Michael Shulman]

Nice! I think that's essentially a beta-reduction of the intended
proof of Exercise 4.6. There are, of course, non-sets with that
property, such as K(G,1) when G has trivial center.

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

[Nicolai Kraus]

On 19/04/14 22:40, Michael Shulman wrote:
> Nice! I think that's essentially a beta-reduction of the intended
> proof of Exercise 4.6. There are, of course, non-sets with that
> property, such as K(G,1) when G has trivial center.

Thanks Mike! True, there are non-sets with the property "every term of
type forall a, a=a is constantly refl". But the quantification over all
types makes it a bit more powerful. For example, we can show this:

(Statement) In a qinv-univalent universe, every n-type is a 1-type. [In
other words: all n-truncations with 0<n<infty are the same. Even other
words: all n-th homotopy groups, with n>1, are trivial.]

That statement is a bit annoying because I would *at least* want to show
that every n-type is a set. The reason why this stronger version does
not follow from my argument is that I need the corresponding homotopy
groups to be abelian. Anyway, to prove (Statement) we can first
formulate the following:

(Lemma) If X is 1-truncated in a qinv-univalent universe such that all
its fundament groups [= loop spaces in this case] commute, then X is a set.

(Lemma) => (Statement) goes like this: given any n-type A with some base
point, take the (n-1)-th loop space and observe that it fulfills the
conditions of (Lemma).

And the proof sketch of (Lemma) : Take some point z : X and path q :
z=z. We need to show q = refl. Define the connected component of z as
Y := Sigma (x : X) . ||x = z||.

Now, we want to define
t : forall (y:Y), y=y
such that
ap fst (t(z,|refl|)) = q.
We are done if we can do this by the property proved in the last email
(note that we don't use this property for X, we use it for a newly
constructed Y - that's where we use that it is a result for all types,
not just a specific one!).

Okay, so let's construct t: given any x:X, we have a map
s : x=z -> x=x
defined by s := \p. p.q.(inverse p).

Now comes the part of this argument that I like. From the fact that the
loop spaces of X commute, we get that s is "weakly constant" / "steady"
/ however we want to call it". ;)
As x=x is a set, one of the very basic factorization results gives us a
map ||x=z|| -> x=x, and thereby t (of course we use that 'ap snd (t y)'
is trivial).

Nicolai

[Michael Shulman]

Also nice! Here's another way to explain it: Y is a K(G,1), therefore
[forall (y:Y), y=y] is the center of G (futzing with steady functions
is "just" a way to prove this without invoking any particular
construction of K(G,1)). In other words, a qinv-univalent universe
can contain a K(G,1) only if G has trivial center; therefore, since we
can construct a K(pi_n(X),1) from X by taking loop spaces and
connected components, pi_n(X) must have trivial center -- and thus, if
n>1 so that it is abelian, must be trivial.

Note that all of this depends on which type formers we assume our
qinv-univalent universe to be closed under. Your construction requires
propositional truncation, which can be obtained as a HIT. However,
it's inconsistent for a qinv-univalent universe to be closed under
*all* HITs, since S^1 is a K(G,1) with nontrivial center (the proof of
this works just as well with qinv-univalence).


If we're willing to also assume closure under set-quotients, then I
think I can show, building on your argument, that *all* 1-types in a
qinv-univalent universe must be sets. Suppose that X is a 1-type,
with z:X and q:z=z. For any x:X, consider the equivalence relation on
the set z=x defined by p ~ r iff p r^{-1} = q^n for some integer n.
Let Q(x) be its set-quotient, and let R = sum(x:X) Q(x). Of course, R
is a 1-type.

First of all, I claim that R is connected. If (x1,r1):R and
(x2,r2):R, then since ||(x1,r1)=(x2,r2)|| is a mere proposition, we
may assume r1 and r2 are the images in the set-quotient of p1:z=x1 and
p2:z=x2. But then p1^{-1} p2 : x1 = x2, and transporting p1 along
this path gives p2; hence transporting r1 along the same path gives
r2. So (x1,r1)=(x2,r2).

Thus, R has a unique fundamental group (up to non-unique isomorphism).
It has a basepoint coming from z and refl, and its fundamental group
at this basepoint is the group of paths p:z=z such that p = q^n for
some integer n. But this group is cyclic, hence abelian. So by your
Lemma, R is a set, hence contractible, and thus q = refl.


In conclusion, if a qinv-univalent universe is closed under the basic
type constructors, as well as propositional truncation and
set-quotients, then the only n-types it contains are sets, and thus
its types have no nontrivial homotopy groups. In particular, there is
no hope of naively constructing such a universe in the simplicial set
model by taking a full subuniverse of the standard one. But can we
say anything about possible nontrivial oo-connected types in a
qinv-univalent universe?

[Nicolai Kraus]

I didn't know that we can manipulate a type in this way and remove only
*some* of its paths with set-quotients. Very cool argument! I will
definitely remember that. I still don't know what to do about general
(oo-truncated) types, and ideally I would hope that we can avoid using
any sorts of HITs for this conclusion about types in a qinv-universe...
Nicolai

[Michael Shulman]

The way I thought of this is that a type family over K(G,1) is a type
acted on by G, and its Sigma-type is the homotopy quotient of that
action. And if H is a subgroup of G, then the homotopy quotient of
the G-action on G/H is a K(H,1).

On Tue, Apr 22, 2014 at 4:31 AM, Nicolai Kraus <nicola...@gmail.com> wrote:
> I didn't know that we can manipulate a type in this way and remove only
> *some* of its paths with set-quotients. Very cool argument! I will
> definitely remember that. I still don't know what to do about general
> (oo-truncated) types, and ideally I would hope that we can avoid using
> any sorts of HITs for this conclusion about types in a qinv-universe...
> Nicolai
>
>
> On 21/04/14 06:49, Michael Shulman wrote: