6
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

Extensionality is basically the reversibility of the introduction rule. Negative types have reversible introduction rules, while positive types have reversible elimination rules. So you are looking in the wrong direction.

The nlab entry for sum types mentions polarity at the very end.

$\endgroup$
7
  • 1
    $\begingroup$ Can you expand on that? It sounds more like an eta-rule than extensionality to me, but I'm guessing there's a connection I'm not seeing. Is there a connection to equality reflection? $\endgroup$
    – jmite
    Nov 2 '21 at 16:11
  • 3
    $\begingroup$ 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. $\endgroup$ Nov 2 '21 at 18:26
  • $\begingroup$ Is there a name for 'reversibility of elimination rules'? $\endgroup$
    – ice1000
    Nov 2 '21 at 20:33
  • 1
    $\begingroup$ @ice1000 Intuitionistic type theory is inherently biased towards positive types. I doubt there is a name for that. $\endgroup$
    – Trebor
    Nov 3 '21 at 0:01
  • 1
    $\begingroup$ There is a family of equality checking algorithms that can deal with judgemental extensionality rules. See An extensible equality checking algorithm for dependent type theories, and references therein for precursors on which the aglorithm is based. (Apologies for shameless self-promotion.) $\endgroup$ Nov 3 '21 at 18:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.