>>12229979Who is "they"?
I never did much formall MLTT, but I assume on the informal level, "they" would give a quite "proof" involving the universal property of the thing.
In this case, the defining property of the pair to do exactly that can maybe be proven indpendently of you dealing with functions f and g there, i.e. just prove it for pairs (x,y)=(a,b) => x=a and y=b.
For set theory, this is e.g. exactly what the Wikipedia article on the ordered pair tries to establish as soon as they introduce a model of the pair (see bottom of pic)
The property of univalence is only a 10 year old idea or so. The MLTT rule for equality is I think still there and is what lets one otherwise deal with equality (it looks like induction, but uglier).
Not all type theories have extensionality, but I think they are glad that they have it.
(It makes it so the (n+2)^2 and n^2+4n+4 are necessarily the same function, and so is the function that takes n, generates a random sudoku, solves it, and only then returns n^2+4n+4. Although the context in which intensionality/extensionality comes into play is generally not complexity theory.)
Semi-related
Functions and extensionality has also some funny properties like the following:
Consider some proposition P and define sets
A = {x in {0,1} | x=0 or (x=1 and P)}
B = {x in {0,1} | x=1 or (x=0 and P)}
Then if P, then A=B={0,1}. If not P, then A={0} and B={1}. In either case, 0 is in A and 1 is in B.
But we don't know the truth value of P.
Now funny enough, assuming the Axiom of Choice for this (sub)finite set {A,B} implies LEM.
To see this, try to find a function
with
f : {A,B} -> {0, 1}
and
f(v) in v
