I have fixed some formatting issues that I had left in that section

some cdots instead of cdot and a broken anchor link. Notice that none of the $(\infty,1)$-entries work for pointing to anchors inside them via

```
[text](name#anchor)
```

because the parenthesis in the name confuse the parser (though if it were more clever it should be able to handle this…)

At times I have for that reason made redirects that omit the “,1”. But this is not a robust solution in the long run, for in the far bright future that lies ahead, the $n$Lab will be full of articles on $\infty$-category theory in the genuine sense of $(\infty,\infty)$-categories…

So here I just made the page name without any parenthesis a redirect.

]]>Thank you. I see that this is basic stuff. Good.

I have started to add some of this to the section in the entry, towards the end. But I don’t have much time at the moment and the whole section remains in a somewhat curious state for the time being.

]]>Yes. Concatenation with any path $p:y=z$ defines an equivalence $(x=y)\to (x=z)$, whose inverse is concatenation with $p^{-1}$. And the action of any equivalence on path-spaces is itself an equivalence. Combining those in the case $p=g_2$, we get an equivalence $(g_1\cdot g_2^{-1} =\phi(d))\to ((g_1 \cdot g_2^{-1})\cdot g_2= \phi(d)\cdot g_2)$. Then we just concatenate on the left by the coherence path $g_1 = (g_1 \cdot g_2^{-1})\cdot g_2$.

]]>Thanks, Mike!

Of course the key step is the first one

$d:D, g_1:G, g_2:G \vdash cancelright \colon (g_1\cdot g_2^{-1} = \phi(d)) = (g_1 = \phi(d)\cdot g_2)$

In the external proofs that I had considered, all the work was in reducing the situation to the situation in $sSet$ and then in $Set$, such as to then be able to appeal to this cancellation there.

I trust that you easily deduce the term $cancelright$ for the case that $G \coloneqq (x = x)_X$?

]]>any ∞-category $C$ which admits a finite-limit-preserving embedding in a presheaf ∞-category.

That would be *every* ∞-category, by the Yoneda embedding, right?

Here’s a HoTT proof of your second statement.

$\begin{aligned} D\times_G (G\times G) &= \sum_{d:D} \sum_{g_1:G} \sum_{g_2:G} (g_1\cdot g_2^{-1} = \phi(d)) \\ &= \sum_{d:D} \sum_{g_1:G} \sum_{g_2:G} (g_1 = \phi(d)\cdot g_2) \\ &= \sum_{d:D} \sum_{g_2:G} \sum_{g_1:G} (g_1 = \phi(d)\cdot g_2) \\ &= \sum_{d:D} \sum_{g_2:G} \mathbf{1}\\ &= D\times G \end{aligned}$The third-to-fourth line is because $\sum_{g_1:G} (g_1 = \phi(d)\cdot g_2)$ is a one-sided based path-space (called by some a “coconut” for obscure reasons), hence contractible.

This proof only requires $G$ to be a grouplike associative H-space, and since it doesn’t use univalence it works in any lcc $(\infty,1)$-category.

]]>Oh, I bet it is something like $(g,d) \mapsto (\phi(d)\cdot g,g)$, where $\phi: D\to G$. Right?

]]>What is the map $G\times D \to G\times G$?

]]>The only point to be proved is that $X\times_B Y$ is the fiber of $f \cdot g^{-1}$, right?

Yes, exactly.

And the other thing that it would be nice to have internal proof of is that there is a homotopy pullback of the form

$\array{ G \times D &\longrightarrow& D \\ \downarrow && \downarrow \\ G \times G &\stackrel{(-)\cdot (-)^{-1}}{\longrightarrow}& G }$for all $D\to G$. (This implies the first statement.)

]]>The only point to be proved is that $X\times_B Y$ is the fiber of $f \cdot g^{-1}$, right? That should be easy to do internally in HoTT.

]]>Ah but the sequence $B \to B\times B\to B$ to be proved a fiber sequence is in fact equivalent to the trivial fiber sequence

$B \xrightarrow{(id,e)} B \times B \xrightarrow{\pi_2} B,$by sending $(b_1,b_2)$ to $(b_1 b_2^{-1}, b_2)$ in the middle term. So you get this fiber sequence for any group object in any $\infty$-category.

]]>Oh, of course, thanks. That also answers my other question.

On the other hand it would be nice to know how much one may say without making recourse to a site of definition, but just working internally.

]]>Can’t you just do everything pointwise? The assumption that $B \to B\times B\to B$ is a fiber sequence for $B$ an ∞-group holds in $\infty Grpd$, hence it should hold in any ∞-category $C$ which admits a finite-limit-preserving embedding in a presheaf ∞-category.

]]>at *Mayer-Vietoris sequence* I had once recorded (previous nForum discussion is here) some observations about the generality in which Mayer-Vietoris-like homotopy fiber sequences exist in infinity-toposes.

In the section *Over an infinity-group* are discussed sufficient conditions such that for $f : X \to B$ and $g: Y \to B$ two morphisms in an $\infty$-topos to an object $B$ that carries $\infty$-group structure, we obtain a long homotopy fiber sequence of the form

The discussion in Example 2 in that section in that entry gives this under the assumption that the $\infty$-topos is 1-localic, hence that it has a 1-site of definition. Or rather, in that case another discussion gives that every group object in the $\infty$-topos is presented by a presheaf of simplicial groups, and the discussion at *Mayer-Vietoris sequence* takes that to deduce the above fiber sequence.

But all this smells like a hack for a statement that should be true more generally. In which generality do we have the above statement?

]]>