3
$\begingroup$

I have posted this question here on M.SE but since it received little attention and since it seems difficult to find helpfule references I reposting it here.

In Jacob's Categorical logic and Type Theory in relation to fibrations with equality the author gives the following definition (Remark 3.6.6):

...call two morphisms of Eq-fibrations $(K,H),(K',H') \colon p \to q$ between two Eq-fibrations $p \colon \mathbb E \to \mathbb B$ and $q \colon \mathbb D \to \mathbb A$ equivalent if:

(1) $H=H' : \mathbb{E} \to \mathbb{D}$, and on objects $K=K' \colon \text{Obj}(\mathbb B) \to \text{Obj}(\mathbb A)$;

(2) $K(u)$ and $K'(u)$ are internally equal in $q$, for each morphism $u$ in $\mathbb B$.

This definition troubles me for the following reason.

Assume $(H,K)$ and $(H',K')$ are as above (i.e. they are an equivalent pair of morphisms of Eq-fibrations) and let $u$ be a morphism of $\mathbb B$.

Since $p$ is a fibration, and we assume that all the fibers are not empty categories (assumption reasonable for instance for the classifying fibration of an equational theory), we have a cartesian lifting of $u$, so we have a morphism $v$ in $\mathbb E$ such that $p(v)=u$.

Since by hypothesis $H=H'$ we should have $$q \circ H(v)=q \circ H'(v)$$ and since $(H,K)$ and $(H',K')$ are morphism of fibrations $$K\circ p(v) = K' \circ p(v)$$ hence $$K(u) = K'(u)\ .$$

Since we made no assumption on $u$, with the exception of being in the image of $p$ which should hold in all classifying fibration (if I am not mistaken), it seems that it should follow that $K=K'$ and so that Eq-fibration morphisms should equivalent only if they are equal, which seems counterintuitive since the author proposes it as an equivalence alternative to equality.

So here is my question.

Did I make any mistake in my argument above? In case not, how can the definition above be fixed to obtain a non trivial equivalence between Eq-fibration morphisms?

Thanks in advance for any help.

$\endgroup$

1 Answer 1

3
$\begingroup$

Yes, I agree with your argument that any two equivalent morphisms in this sense must be equal, if all fibers of $q$ are non-empty. To present it a bit more concisely: Any fibration with non-empty fibers must be full and surjective on objects. We have $qH = Kp = K'p = qH'$; so since $qH = qH'$ and $q$ is full and surjective on objects, we must have $H = H'$.

I also agree this shows that it can’t be what Jacobs intended there, since the example sketched immediately following the definition seems to require non-equal morphisms of fibrations to be equivalent in this sense. $\newcommand{\E}{\mathbb{E}}\newcommand{\D}{\mathbb{D}}$

A possible fix: weaken the condition “$H = H'$” to “on objects, $H = H'$”. This seems to make reasonable sense, and work for showing that the two Eq-fibrations in the sketched example are equivalent.

It’s also easy to imagine how the error could have arisen, if this is what Jacobs intended: in an early draft, he could have written something like “$H = H'$ and $K = K'$ on objects”, and then when fleshing it out in later editing, could have misremembered his intention and turned it into the current text.

But since this notion isn’t developed much in the book, it’s difficult to know if this is what Jacobs really intended, unless it’s studied elsewhere in the literature; and at least for me, it doesn’t ring any bells.

$\endgroup$
1
  • 1
    $\begingroup$ @MaliceVidrine: thanks yes, that was indeed a typo! Fixed. $\endgroup$ Aug 26, 2018 at 10:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.