The standard definition of homotopy equivalence in HoTT is a quadruple of:
- $f: A \rightarrow B$
- $g: B \rightarrow A$
- $p: \operatorname{id} A = g \circ f$
- $q: \operatorname{id} B = f \circ g$
... where the paths are homogeneous in $A \rightarrow A$ and $B \rightarrow B$ respectively.
My question is what happens if we let the paths be heterogeneous (or in the HoTT book terminology dependent) over some paths $P: (A \rightarrow A) = (A \rightarrow A)$ and $Q: (B \rightarrow B) = (B \rightarrow B)$?
Will it have practical implications for the theory (in comparison to HoTT or CTT), or will the difference be limited to the corresponding categorical semantics?
Your definition might be an interesting thing, but it's not a definition of anything that most people would call an "equivalence". You're basically saying consider two types $A$ and $B$ and functions $f:A\to B$ and $g:B\to A$ such that there is an automorphism of the type $A\to A$ that sends $g\circ f$ to $\rm id_A$ and an automorphism of the type $B\to B$ that sends $f\circ g$ to $\rm id_B$.
This situation holds, for instance, when $A = \mathbf{1}$ is the unit type and $B = \mathbf{1}+\mathbf{1} = \mathsf{Bool}$ is the two-element type. In this case $B\to B$ is a finite 4-element type, which is "transitive" in that it has an automorphism sending any element to any other element — and of course $A\to A$ is also (equivalent to) a contractible type. Most people would not consider these two types to be equivalent. (-: