# What's wrong with this "proof" involving' $n$-connectedness in HoTT?

okay, this is silly, but I can't for the life of me figure out what's wrong with the following "proof":

Claim: if $$B$$ is an $$(n-1)$$-type, then $$(n\text{-conn}(A) \to B) \simeq (\text{isCntr}(A) \to B)$$.

"proof": We have \begin{align*}(n\text{-conn}(A) \to B) & \equiv ((\sum_{x : \vert A\vert_n} \prod_{y : \vert A\vert_n} x = y) \to B)\newline & \simeq (\prod_{x : \vert A\vert_n} \prod_{y : \vert A \vert _n} x = y \to B) \end{align*}

by the universal property of $$\sum$$ types. Now, since $$B$$ is an (n-1)-type, it in an n-type, and so is every function type into $$B$$. So we may apply the universal property of $$\vert A\vert_n$$ to obtain: \begin{align*}(\prod_{x : \vert A\vert_n} \prod_{y : \vert A \vert_n} x = y \to B) & \simeq(\prod_{x : A} \prod_{y : A} x = y \to B) \newline &\simeq ((\sum_{x : A} \prod_{y : A} x = y) \to B) \newline &\equiv (\text{isCntr}(A) \to B)\end{align*} This concludes the "proof".

However, this cannot be the case, since this allows us to prove that $$! : A \to 1$$ is an equivalence for any $$n>-1$$-connected type $$A$$. Since $$\text{iseqv}(!)$$ is a $$-1$$-Type, we have $$(0\text{-conn}(A)\to \text{iseqv}(!))\simeq (\text{isCntr}(A) \to \text{iseqv}(!))$$. However, this latter type is always inhabited.

• Man I really don't have the answer to your problem, neither understand it, I'm just coming here to state that this looks like fucking wizardry. Good luck. Nov 30, 2022 at 7:14
• @LucasGiraldi lmao thank you. Not sure how much I understand whats going on either since I can't spot the mistake Nov 30, 2022 at 7:20
• @Lucas Giraldi We should all of us consider that there are many "niches" in mathematics like this one who looks "wizardry" but in fact are maybe the mathematics of tomorrow... Just like many physicists some 50 years ago were looking at quantum physics as a very "bizarre" thing... Nov 30, 2022 at 9:20

$$\left(\left(\sum\limits_{x : C} \prod\limits_{y : C} x = y\right) \to B\right) \simeq \left(\prod\limits_{x : C} \left(\left(\prod\limits_{y : C} x = y\right) \to B\right)\right)$$
You apply this identity to both $$A$$ and $$|A|_n$$, but you do so with incorrect placement of parentheses. With the correct placement, it is clear that your argument fails.