What is the right kind of isomorphism for groupoids

Stream: general

[Praneeth Kolichala]

I want to prove that $\pi(X \times Y) = \pi(X) \times \pi(Y)$ for topological spaces $X$ and $Y$, where $\pi$ is the fundamental groupoid functor. However, this "equals to" is hiding a lot. Normally, I would want to interpret it as "isomorphic as groupoids;" that is there are functors (which are the morphisms in the category of groupoids) $A: \pi(X \times Y) \rightarrow \pi(X) \times \pi(Y)$ and $B: \pi(X) \times \pi(Y) \rightarrow \pi(X \times Y)$ such that $A\circ B = \mathbf{1}$ and $B\circ A = \mathbf{1}$ (and also $A$ is precisely the product of the maps $\pi(X \times Y) \rightarrow \pi(X)$ and $\pi(X \times Y)\rightarrow \pi(Y)$ induced by the projections $X\times Y \rightarrow X$ and $X\times Y \rightarrow Y$ respectively, so that $\pi$ really does "preserve products").

Unfortunately, this involves proving equality of functors, which it says in the docs that I should avoid. In particular, as far as I can see, the functor $A \circ B$ does not a priori map an object $x \in \pi(X) \times \pi(Y)$ to itself, and similarly for $B \circ A$. So in order to show that they are inverses, we have to have use functor.ext or functor.hext.

The alternative would be to show that $\pi(X \times Y)$ and $\pi(X)\times \pi(Y)$ are not isomorphic but equivalent, which is a lot weaker.

Am I doing something wrong? What is the best way to do this?

[Adam Topaz]

This is a difficult question because in order to avoid talking about equality of functors you would need to consider $\pi$ as a pseudofunctor into the 2-category of groupoids, which still does not exist. For now, i suggest defining the isomorphism as an isomorphism in the category docs#category_theory.Groupoid (which will involve equality of functors), but also provide the API that would be used to eventually construct such a pseudofunctor.