Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Defining equivalence of arrows of concrete categories

Shea Levy (Nov 01 2020 at 23:56):

If we're defining some concrete category (speaking loosely) inside of some existing set or type theory, do we still take pointwise equality as our notion of arrow equivalence like we do with $Set$ (or $Type$ or whatever)? Or could the notion of equivalence change depending on the structure the morphisms preserve?

For example, I'm defining the ordinals as isomorphism classes of well-ordered types in coq. Is "a function $f$ such that there exists an $f^{-1}$ such that $x \prec y \to f(x) \prec f(y)$, $x' \prec y' \to f^{-1}(x') \prec f^{-1}(y')$, $\forall x, f^{-1} (f(x)) \equiv x$ and $\forall x', f (f^{-1}(x')) \equiv x$" the right notion of isomorphism? Or is there some finer meaning of $f \circ f^{-1} \equiv id$ when we're no longer dealing with arbitrary functions?

Chad Nester (Nov 02 2020 at 08:57):

A common approach in type theory is to work with setoids (aka Bishop sets), which are sets $X$ equipped with an equivalence relation $=_X \subseteq X \times X$. A category can be given as a setoid of objects together with hom-setoids for every pair of objects, subject to the usual associativity and unit axioms.

Chad Nester (Nov 02 2020 at 09:10):

For example, it looks like this is what the agda-categories people use: https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Core.agda

James Wood (Nov 02 2020 at 09:29):

Shea Levy said:

For example, I'm defining the ordinals as isomorphism classes of well-ordered types in coq. Is "a function $f$ such that there exists an $f^{-1}$ such that $x \prec y \to f(x) \prec f(y)$, $x' \prec y' \to f^{-1}(x') \prec f^{-1}(y')$, $\forall x, f^{-1} (f(x)) \equiv x$ and $\forall x', f (f^{-1}(x')) \equiv x$" the right notion of isomorphism? Or is there some finer meaning of $f \circ f^{-1} \equiv id$ when we're no longer dealing with arbitrary functions?

Monotonicity is a property, and hence doesn't affect equality of such functions. That is, equality of monotonic functions is just equality on the underlying functions. If you work through the definitions given that, then you'll find that what you said is correct.