The context I'm working in here is dependent type theory used in proof formalization (in particular in Lean, though is likely not relevant).

The question I have is best explained through examples. A very simple example is "currying". Let $\alpha, \beta, \gamma$ be types. Then the types $\nu := \alpha \to (\beta \to \gamma)$ and $\mu:= (\alpha \times \beta) \to \gamma$ both can be though of as the type of functions with an argument of type $\alpha$, an argument of type $\beta$, and an output of type $\gamma$. But of course these two types are formally different (or at the very least they could be formally different depending on how everything is construct), yet they should be thought of as "equivalent" in some way. What is the proper formalization of this notion of equivalence? We want to be able to say something like "every theorem we have about $\nu$ we have about $\mu$ and vice versa" (of course this isn't precisely true, but something like it should be true).

Here are some more examples of types we should be able to say are equivalent in some sense (I get that this is a bit of "tall order"; if you have an answer that gives the correct idea without responding to every point, please give it):

1) Let $\nu := \alpha \times \beta$ and $\mu := \beta \times \alpha$.

2) Inductively defined types with different names given to their constructors, constructors given in different orders, and different names given to their fields.

3) Structures defined using mathematical equivalent definitions, e.g.:

i) Groups defined with right inverse and right identity vs. with left inverse left identity.

ii) Groups defined by existence of inverse vs. groups defined with inverse functions $G \to G$.

  • $\begingroup$ Two types $X$ and $Y$ are isomorphic if there is a term $x : X \vdash s : Y$ and a term $y : Y \vdash t : X$ such that $y : Y \vdash s[t/x] = y$ and $x : X \vdash t[s/y] = x$. This can be derived by translating the notion of isomorphism from category theory into syntactic terms. (In intensional type theory, you would usually want a weaker notion, e.g. an equivalence in HoTT.) $\endgroup$
    – varkor
    Commented May 15, 2020 at 12:44
  • $\begingroup$ @varkor I'm not 100% sure what your notation of $\vdash$ means, but it seems to me this is only like a "bijection between types". Under this conception, I think the type $real$ and the type $complex$ would be isomorphic, but this is bad, because they are certainly not isomorphic in any usual, mathematical sense. $\endgroup$ Commented May 15, 2020 at 13:00
  • $\begingroup$ $\vdash$ here is the usual notation for separating a context from a term. That's true: the isomorphism here is analogous to an isomorphism of sets (under which $\mathbb R \cong \mathbb C$). If you want to ensure that structure is preserved under the isomorphism, you need extra conditions. For algebraic data types, for instance, the correct notion is isomorphism in the category of $F$-algebras, for $F$ a finitary polynomial functor. Translating into a category-theoretic context is helpful, as there's a strong focus on isomorphism-invariance there. $\endgroup$
    – varkor
    Commented May 15, 2020 at 14:38

1 Answer 1


Mathematicians have a fluid interface to mathematics, and cannot always agree on what is actually going on under the hood. $\alpha\times\beta$ and $\beta\times\alpha$ may be either the same or different depending on what you are doing. For example, if $\alpha$ and $\beta$ are different subsets of $\mathbb{R}$ then $\alpha\times\beta$ and $\beta\times\alpha$ might represent different subsets of $\mathbb{R}^2$. But if we are only using the product as a way of carrying around a pair of elements, then $\alpha\times\beta$ and $\beta\times\alpha$ can be thought of as different implementations of the same formal specification. An example of where this happens in practice is $\mathbb{R}^3$, which can be implemented as $(\mathbb{R}\times\mathbb{R})\times\mathbb{R}$ and as $\mathbb{R}\times(\mathbb{R}\times\mathbb{R})$, as well as in several other ways. Mathematicians do not ask if the vector $v\in\mathbb{R}^3$ happens to be an ordered pair or an ordered triple or a function from $\{0,1,2\}$ to $\mathbb{R}$ because this is not relevant. Mathematicians have taken a vow to only access $\mathbb{R}^3$ via its interface, which is built on top of its specification. Because of this, they have no problems with calling different implementations "equal", because they have the same specification. This means that they "satisfy the same mathematical theorems". This is where the vow comes in. We can ask questions such as "OK so the origin in $\mathbb{R}^3$ is a set in set theory; is it finite or infinite?" This is not a mathematical question because the axioms of a vector space do not say anything about the elements of elements of a vector space. It is a question about implementation.

In Lean when two objects are equal in this way, the transport and transfer tactics can be used to move properties from one object to another. But transporting structure is hard work; in Lean's maths library we tend to make one implementation which is somehow "the best from the point of view of computer science" (perhaps computer scientists have a lot of say in the implementation) and then prove the specification and go on to extract more interface (mathematicians do this part -- the interface is just the standard theorems about the object, so this is the part that's like a computer game).

There are times in a mathematician's life where it becomes very convenient to identify different implementations of the same specification as being "equal" or "equivalent" or whatever word you want to use for it, and because the implementations satisfy the same specification and our vow is to only use the specification, we talk of them as being equal. They are not actually equal, but we know this doesn't matter. Unfortunately the theorem provers are still struggling to understand this fluid use of equality. Neither Lean's = nor the univalent = capture it correctly. Some wise people call the concept "canonical isomorphism". I am with Weil -- I think this concept is hogwash in some cases and needs to be better explained. But mostly it's fine.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .