regular infinity-actions

[Michael Shulman]

In a discussion at the nForum:
https://nforum.ncatlab.org/comments.php?DiscussionID=7095
the following question arose.

Define an "oo-group" G to be a pointed connected type denoted BG.
(That is, when we regard a pointed connected type as an oo-group, we
write G for the oo-group and BG for its underlying type.) An "action"
of an oo-group G is a type family X : BG -> Type; it is said to be an
action "on" the type X(*), where *:BG is the basepoint. The action is
"regular" if \sum_{p:BG} X(p) is contractible.

Given a G-action X, define Aut_G(X) to be the oo-group with

BAut_G(X) = \sum_{P:BG->Type} || P=X ||.

and basepoint (X,refl). Then we have a BAut_G(X)-action defined by

Y : BAut_G(X) -> Type
Y(P,p) = P(*)

and because Y(X,refl) = X(*), this is an action on the same underlying type.

CONJECTURE: if the G-action X is regular, then so is the Aut_G(X)-action Y.

Any takers? This might be easy, or it might be hard; I haven't had
time to really think about it. When G is a set-group (i.e. BG is a
1-type) and X is a set, it is a classical fact; a proof is at
https://ncatlab.org/nlab/show/regular%20action. In that case there is
also a partial converse that if G acts transitively and faithfully on
X and Aut_G(X) acts regularly, then G also acts regularly. It's less
obvious how to define "transitive and faithful" in the oo-setting, but
that would be a natural next question.

Mike

[Egbert Rijke]

Hi Mike,

It would be convenient if we have a point in X(*), for instance to conclude that X(p) is equivalent to p=*. Then we would also be able to construct the center of contraction of the type

\sum_{b : BAut_G(X)} Y(b),

because it is equivalent to

\sum_{P:BG -> U} \sum_{t: ||P=X||} P(*).

With a point x0 in X(*), we would take the triple (X, refl, x0) as the center of contraction. Then let P : BG -> U, let t : || P = X ||, let p0 : P(*). To show regularity, it suffices to show

\sum_{\alpha : P = X} trans(alpha)(p0) = x0

This type is equivalent to showing that there are

K : \prod_{b:BG} P(b) \equiv X(b), and

K(*,p0) = x0

Since we need this particular fiberwise equivalence, it suffices to show that

\sum_{b:BG} P(b)

is contractible. Now this is a mere proposition, so we can eliminate t : || P = X || to obtain the proof.

Can we have a point in X(*) or not?

Best,

Egbert

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

[Michael Shulman]

Well, since \sum_{p:BG} X(p) is contractible, we have a p0:BG and
x:X(p0); so since ||p0=*|| we have ||X(*)||. And then as
contractibility is a proposition, to prove it we can assume X(*).
Nicely done!

Any takers for the converse?

[Egbert Rijke]

Here's an attempt for the converse, but I'll leave the fact whether this particular notion of principal bundle is a good candidate for Mikes "transitive and faithful" condition up for discussion.

Lets say that X : BG -> U is a principal homogeneous space for G if the following condition holds:

\prod_{x,y : X(*)} isContr( \sum_{g:G} trans(g,x)=y ).

If X is a principal homogeneous space for G and ||X(*)||, then X is regular.

Proof.

We may assume x0 : X(*). This gives us the center of contraction (*,x0). It remains to show that

\prod_{b:BG} \prod_{x:X(b)} \sum_{\alpha : b=*} \trans(\alpha,x) = x0.

Of course, it would suffice to prove the stronger statement

\prod_{b:BG} \prod_{x:X(b)} isContr (\sum_{\alpha : b=*} \trans(\alpha,x) = x0).

However, now we get to use that BG is connected. Therefore it suffices to show that

\prod_{x:X(*)} isContr (\sum_{\alpha : G} \trans(\alpha,x) = x0)

This holds by assumption.

Best,

Egbert

[Egbert Rijke]

There is a counter example to the claim that whenever the family Y : BAut_G(X) -> U is regular, then X must be regular.

Counter example:

Consider X the double cover of the circle. Its total space of X is the circle, so that is not contractible. However, the claim is that the type

\sum_{P:S1 -> U} ||P=X|| x P(*)

is contractible. The center of contraction is going to be (X,refl,true). Now let P : S1 -> U, such that ||P=X|| and p0 : P(*). We have to show that (P,p0) =  (X,true). To see this, note first that P is determined by A := P(*) and the equivalence e : A \equiv A given by transporting over loop. So we need to show that (A, e, p0) = (X, neg, true)

We obtain from ||P=X|| that ||A=2||. Recall that for types A such that ||A=2|| we have A \equiv (A = 2) in a canonical way. Since we have p0 : A, it follows from the previous observation that we get an equivalence f : A \equiv 2 such that f(p0) = true. Moreover, since it follows that (A \equiv A) \equiv 2, we can decide what the equivalence e : A \equiv A is. There are two provably distinct possibilities, and since ||P=X|| it follows that e has to be negation. This finishes the proof of contractibility.

Best,

Egbert

[Egbert Rijke]

typo: in the counter example, X is the *twisted* double cover, given by the type 2, and negation.

[Michael Shulman]

Well, in the case when G and X are sets, I don't think your definition
reduces to "transitive and faithful", since it also includes freeness.
Moreover, you didn't use the other hypothesis of the converse that the
action of Aut_G(X) is regular.

[Erik Palmgren]

A new preprint is available on arXiv:

Categories with families, FOLDS and logic enriched type theory

Erik Palmgren

http://arxiv.org/abs/1605.01586

Abstract. Categories with families (cwfs) is an established semantical
structure for dependent type theories, such as Martin-L\"of type theory.
Makkai's first-order logic with dependent sorts (FOLDS) is an example of
a so-called logic enriched type theory. We introduce in this article a
notion of hyperdoctrine over a cwf, and show how FOLDS and Aczel's and
Belo's dependently typed (intuitionistic) first-order logic (DFOL) fit
in this semantical framework. A soundness and completeness theorem is
proved for such a logic. The semantics is functorial in the sense of
Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra
for a DFOL theory. Agreement with standard first-order semantics is
established. Some applications of DFOL to constructive mathematics and
categorical foundations are given. A key feature is a local
propositions-as-types principle.