Which is a more appropriate type for composition of bundles?

Question

I'm trying to understand and mangle pullbacks and limits/colimits into Coq.

Some of the notations are ambiguous. There are also differences of terminology I don't understand.

Which is better?

Precomposition as a bifunctor of an arrow category and an over category?

$$ (f: \mathrm{Arr} (C)) \times C/\mathrm{dom}(f) \rightarrow C/\mathrm{cod}(f)$$

Or precomposition as a bifunctor of an over category?

$$ (f: C/c) \times C/\mathrm{dom}(f) \rightarrow C/c$$

Or something else?

Also apparently you can just ignore the result of the function? I don't get that.

$$ (x: C) \times C/x \rightarrow C$$

Wouldn't that be something like?

$$ (f: C/1) \times C/\mathrm{dom}(f) \rightarrow C/1$$

I'm also not sure how to think of it as a bifunctor as some kind of monoid or something.

Answer 1

This is not really an answer, but just a note:

• Firstly I believe both these things work just fine in theory. Note that in the first case you are using a free $c$, that you might want to bind in your definition, doing so yields $$ (c:C) \times (f:C/c)\times C/\operatorname{dom}(f) \to C/c $$ And from there, you can note that $$ (c : C) \times (f:C/c) \simeq (f:Arr(C)) $$ So both formulation are completely equivalent, at least from a logical point of view.

• There is a big caveat that I want to add though, about proof relevance and categories. You might want to be very careful about how you handle proof-relevance (and if you have sorted this already, you should tell us what your choice is). This is particularly important if you look at over categories. The morphisms in the over categories are commutative triangles. In particular, when formalizing in Coq, you would write the type of morphisms to be something like $$ \operatorname{hom}_{C/c}(f:d\to c, f':d'\to c) = (g : d \to d') \times (f'\circ g = f) $$ If you want to reproduce usual category theory, you really don't want to take in account the witness. More precisely, what I mean is that if you have a morphism $g$ and two proofs $p : f'\circ g = f$ and $q : f'\circ g = f$, you really don't want to define $(g,p)$ and $(g,p')$ as two distinct morphisms in the over category. So you probably need to take some kind of truncation. Again you might be already doing that, but I think you should explain to us how you do it, as it might matter for the aswer you are looking for.

• In the dark, without knowing your implementation, I would think the formulation $$ (c:C)\times (f:C/c)\times C/\operatorname{dom}(f) \to C/c$$ has more chances to have better computational behaviour. The reason for this is that in this case you ensures that $\operatorname{cod}(f)$ is definitionally equal to $c$, and that might save up some computation.

• I am not sure I understand your last question, you can understand the morphism $$ (x:C) \times C/x \to C$$ very easily on its own. Given an object $x$ of $C$ and a morphism $f$ of codomain $x$, it returns the domain of $f$. You can also define a the precompostion of morphisms above the terminal object, as you have noted $$ (f:C/1)\times C/\operatorname{dom}(f) \to C/1 $$ But there is an isomorphism $C/1\simeq C$, and under this isomoprhism, those two are the same