Is there any existing literature on what the internal language of a groupoid might look like?
Please excuse the syntax bashing of this amateur, but i came up with:
symmetry (structural rule): $$ \frac{ \Gamma \vdash Y : e : X \dashv \Delta }{ \Delta \vdash X : e : Y \dashv \Gamma } $$
abstraction introduction: $$ \frac{ \Gamma, x : A \vdash D : e : B \dashv C : x, \Delta }{ \Gamma \vdash A \leftrightarrow B : \lambda x. e : D \leftrightarrow C \dashv \Delta } $$
(I'm not sure whether perhaps I should just have $A$ and $B$ with $C := A$ and $ D := B$, or should I go in the other direction and use $ A \rightarrow B : \lambda x.e : C \rightarrow D$. Similarly, I'm unsure whether I want one $x$ used twice, or an $x$ and a $y$.)
abstraction elimination: $$ \frac{ \Gamma \vdash A \leftrightarrow B : f : D \leftrightarrow C \dashv \Delta \qquad \Gamma \vdash C : e : A \dashv \Delta }{ \Gamma \vdash D : f e : B \dashv \Delta } $$
for a closed grouoid, which "seems truthy" to me.
The idea of sharing the terms between paired typing judgements is downright loony, I'll freely admit, but corresponds to the "symmetry by construction" of an arbitrary groupoid.
If this does turn out to be...not wrong, is it useful? I don't much intuition for what one can do with the "pointful" lambda parameters that is easier to do than with the "point free" external language.
If it helps, I would like to use this stuff to construct a isomorphism between dependent sums [not generalize to "dependent isomorphisms", which seem absurd to me at this stage] in a suitable groupoid. Even more concretely, imagine coercing GADTs in System $F_C$, and using the coercions of the variant to coerce other fields which otherwise couldn't be coerced.