We are working in homotopy type theory.
Given a type $I$ and a family of pointed types $P : \prod i : I, \sum T : Type, T$, we can define the wedge product $\bigvee\limits_{i : I} P(i)$ as a certain homotopy pushout. More precisely, there is
- a base point $base : \bigvee\limits_{i : I} P(i)$
- a function $inc : \prod i : I, p_1(P(i)) \to \bigvee\limits_{i : I} P(i)$
- a function $paths : \prod i : I, base =_{\bigvee\limits_{i : I} P(i)} inc(i)(p_2(P(i)))$
If $I$ is a set, and for all $i : I$, $p_1(P(i))$ is a connected $1$-type, is $\bigvee\limits_{i : I} P(i)$ also a 1-type? Equivalently, if $I$ is a set and for all $i : I$, the loop space of $P(i)$ is a set, is the loop space of $\bigvee\limits_{i : I} P(i)$ at the base point also a set?
We can answer this question in the affirmative when $I$ has decidable equality and when, for all $i$, the loop space of $P(i)$ has decidable equality. To do this, let $F$ be the set of all sequences over $\sum i : I, loopSpace(P(i))$ such that no element of the sequence is reflexivity, and no consecutive elements $a, b$ of the sequence satisfy $p_1(a) = p_2(b)$. Note that $F$ can be given the structure of the free product of the loop space groups, but this is only true because all loop spaces and $I$ itself have decidable equality.
With this explicit description of $F$, we can do a standard encode-decode argument to show that the loop space $base =_{\bigvee\limits_{i : I} P(i)} base$ is equivalent to (the underlying set of) $F$. To do this, we first define a function $code : \bigvee\limits_{i : I} P(i) \to Type$ as follows. We let $code(base) = F$. For each $i$, we define $code(inc(i)(x))$ to be the set of pairs $(a : F, b : p_2(i) = x)$ such that if $a$ is nonempty, then its last element $k$ satisfies $p_1(k) \neq i$. For each $i$, we define $ap_{code}(paths(i))$ to be the equality induced by the obvious bijection, which sends $a : F$ to $(a, refl)$ if $a$ does not a last element $k$ such that $p_1(k) = i$; otherwise, let $a'$ be $a$ without its last element, and send $a$ to $(a', p_2(k))$. We can now define $decode : \prod\limits_{x : \bigvee\limits_{i : I} P(i)} code(x) \to base = x$ as follows. We first define the obvious map $decodeBase : F \to base = base$. We define $decodeBase((i_1, p_1), \ldots, (i_n, p_n)) = paths(i_1) \cdot ap_{inc(i_1)}(p_1) \cdot paths(i_1)^{-1} \cdot \ldots \cdot paths(i_n) \cdot ap_{inc(i_n)}(p_n) \cdot paths(i_n)^{-1}$. Now define $decode(base) = decodeBase$ and $decode(i, y, a, b) = decodeBase(a) \cdot paths(i) \cdot ap_{inc(i)} b$. We can then define the action of $decode$ on $paths(i)$ in the obvious way. From here, we apply Lemma 8.9.1 of the HoTT book with $c_0$ the empty sequence. It suffices to show part (iii), that for all $c : code(base)$, $transport^{code}(decode(c), c_0) = c$. We do this by induction on the length of $c$. For the inductive step, it suffices to show that $transport^{code}(ap_{inc(i)}(p), (a, b)) = (a, b \cdot p)$ for all $i : I$, $(a, b) : code(i)$, $p : p_1(P(i)) = p_1(P(i))$. The trick is to generalize the above to work for all $x, y : P(i)$ and $p : x = y$ and proceed via path induction. This completes the proof.
However, note the above proof relies very heavily on decidable equality for the various sets involved. I don't see a way to make everything work without this assumption. However, since it's consistent with HoTT that all sets have decidable equality, it is not possible to come up with a counterexample explicitly.
This follows from the very recent work of David Wärn. As far as I know there is so far only a short note on this at https://dwarn.se/po-paths.pdf and a HoTTEST talk. See Example 12 in the note for this particular example.