Disclaimer: This question is vague. It reports on a curious similarity in the hope that discussion might perhaps turn it into something more rigorous, but it's entirely possible that there's nothing to be found here. Equally, perhaps it's well-understood and I'm just not aware.
The curious similarity is between homotopy type theory and zero knowledge proofs:
In Homotopy Type Theory, there's the concept of Propositional Truncation. Informally, one forgets all homotopical structure of a type and only cares whether it's inhabited or not. Formally, for a type $X$, its propositional truncation is the initial map $X\to\|X\|$ into a propositional type $\|X\|$ (where a proposition is a type where all elements are equal). Intuitively (to me, at least), proving $\|\|$ proves $X$. without exhibiting a specific witness in $X$.
In Cryptography, the concept of Zero Knowledge does something very similar: Informally, proving a proposition in zero knowledge demonstrates that the proposition is true without revealing a witness to the verifier.
Conceptually, both things seem very close, and I wonder if there's some formal connection that can be drawn here, such as a cryptographically motivated semantics for Homotopy Type Theory (which would necessarily take computational complexity into account). Higher dimensional structures have also entered computational complexity in the form of higher dimensional expanders, amplifying my curiosity further.
This is not correct. In a constructive theory, there's no way to exhibit $\Vert X \Vert$ without exhibiting an $X$, and someone consuming your construction of $\Vert X \Vert$ will have access to the $X$ you constructed.
What $\Vert X \Vert$ does is add equivalences such that distinct $X$ values produce equivalent proofs of $\Vert X \Vert$ (and so on). This also means that someone consuming your $\Vert X \Vert$ construction must produce a result that is equivalent to results based on any other $X$ value. However, this doesn't mean that they don't get to know which $X$ you used.
One way of seeing this is with a type like $\Vert Σ_{n:ℕ} P(n) \Vert$, where $P$ somehow characterizes a unique natural number. In this case, it is possible to extract the natural number in question. In a proof assistant, this might look something like:
where the ellipses handle the formal paths added by the truncation. Note that the case for the base points just extracts the numeric witness, suggesting that the base point proofs of $\Vert Σ_{n:ℕ} P(n) \Vert$ are actually represented (in part) by numbers. The cases in the ellipses just constitute a proof that the same number will be extracted from every point, so that it is okay for this function to be admitted. And evaluating this function on a proof will extract the (uniquely determined) number used to prove it.
If $P$ is decidable, then it's actually possible to write a similar function even if $P$ does not determine a unique number, because any proof gives us some $n$ that satisfies $P$, and we can search for the least $m$ that satisfies $P$ below it.
A zero-knowledge proof seems more analogous to double negation in an intuitionistic setting. $(X → ⊥) → ⊥$ is always a proposition, and without double negation elimination, you cannot extract an $X$ from it, even in the sort of scenarios above. You may imagine that a value of that type just calls a function with a given value (although that is not really a sensible interpretation in general), but there is no mechanism for inspecting a function to observe which value it is using.
However, as Zhen Lin mentioned, zero-knowledge proofs usually incorporate a tractability aspect that is not automatically incorporated into existing type theories. A function implemented by brute force is the same function as one implemented using secret knowlege to solve the problem efficiently. So to properly incorporate this aspect, you'd need to model runtime complexity somehow in a type theory, or design a theory that has complexity as an inherent aspect.
Edit: perhaps I should note, much of the above is still similar even classically. You can still 'extract' a $ℕ$ from a truncation if it is uniquely characterized, as if values of the truncation contained numbers. And $((X → ⊥) → ⊥) → X$ for $X$ that are not propositions is a choice principle that you might not admit. However, what is different is that you may not need to exhibit an $X$ to prove $\Vert X \Vert$. However, this is not limited to truncation. Instead it leads to, for instance, definitions of natural numbers that don't have a definite corresponding construction.