Post #2117130

A note to future me! I would really love to have the following: The assignment: \(A : X \to \mathcal{U}\) to \(\lambda x.\, \bigcirc_{\mathrm{grpd}}\, A\,x : X \to \mathcal{U}\) sends cocartesian families to covariant families. This seems obvious: the fibers are exactly what you would expect at least. However, it's really hard (for me at least) to understand \(\prod_{i : \mathbb{I}} \bigcirc_{\mathrm{grpd}}A(x\,i) \) in general and to argue that it's covariant. If anyone wishes to demolish my problem for me, I'd very much appreciate it! It would make a lot of calculations much much easier...