What is the general definition of 'extensionality' in type theory and how is extensionality defined for positive types?

It is well-known in the literature that (internal) extensionality of a function type means $$(\prod_a f~a=g~a)\implies f=g$$ (where $$=$$ is the intensional equality type) and extensionality of a product type means $$\sum_{p:a.1=b.1}\text{transport}~p~(a.2)=b.2 \implies a=b$$, but how is extensionality of positive types defined?

I can guess that for $$a, b: X+Y$$ two inhabitants of a sum-type, we might want to say that "either ($$a=inl(a'), b=inl(b')$$ and $$a'=b'$$) or ($$a=inr(a'),b=inr(b')$$ and $$a'=b'$$) do $$a=b$$", but it looks impossible, right? Because we do not have an operation for deciding whether $$a=inl(a')$$ or not, given that $$a$$ is open.

• In the presence of $\beta$-rules and congruence rules, extensionality and $\eta$-rules are interderivable. For example if $x : A \vdash f x \equiv g x$ then $f \equiv (\lambda x . f x) \equiv (\lambda x . g x) \equiv g$, where we used the $\eta$-rule in the first and third step, and a congruence rule in the second step. Nov 2, 2021 at 18:26