unique uniqueness

[Martin Escardo]

What is the most general known form of this phenomenon?

(There is nothing new here, just a question about known facts.)

Given a square of types and functions

p
A -----------> X
| |
| |
q | | f
| |
v v
Y -------------W
g

and a type A' and two maps p':A'->X and q':A'->Y defining an outer
square, let

M(p',q') := Sigma(m:A'->A). p o m ~ p' x q o m = q'.

In MLTT with funext, we can prove that for

A := Sigma(x:X).Sigma(y:X). f x = g y

and p,q the projections, the type M(p',q') of "mediating maps" is
contractible, or a singleton, for any A' and p':A'->X and q':A'->Y.

The point is that we *cannot* prove that "there is a unique m:A'->A
such that p o m ~ p' and q o m = q'" if uniqueness is to mean that the
conditions p o m ~ p' & q o m = q' and p o m' ~ p' and q o m' = q'
together implies m=m'. This fails for two reasons in MLTT: for lack of
UIP, and for lack of funext.

But, with funext and *without* UIP, we can prove that the type
M(p',q') of mediating maps is a singleton.

There are many other situations like this (such as natural number
types, analogue to natural number objects in category theory).

How do we place this phenomenon in a general setting? Categories
internal to MLTT won't do, not in the sense of the HoTT book, and not
in a naive sense either.

In general, perhaps we may wish to read

(Sigma(x:X).A(x)) x Pi(x,y).A(x)->A(y)->x=y

as "there is a unique x:A such that A(x)" (for backwards mathematical
compatibility) and

isContr(Sigma(x:X).A(x))

as "there uniquely exists a unique x:X such that A(x)".

In any case, apart from the terminology, what is the most general (and
natural) situation capturing the above HoTT pull-back definition in
MLTT(+funext)?

We certainly have a terminality situation, but not in a category in
the sense of the HoTT book.

Martin