fouche
That's exactly the kind of feedback I'd like to receive ;-) It might take me a couple of days to merge but thanks a lot!
> @tetrapharmakon suggests that repetitions quickly make code less readable > > ``` > \mor A ["h",below]:[bend right,->] B; > \mor * ["k", above]:[bend left,->] *; > \mor * ["\sigma\Uparrow",black,mid]:[->,white]...
It is very likely. I indeed have 2.0 on both machines... So it's me! Good to know.
You probably mean #352 but it seems I can't pull it locally (it's a work in progress)
I now realize that I haven't seen a MLTT analogue of Freyd's argument that if a locally small category is largely complete it is a poset. Can it be done,...
At the moment I am still trying to type correctly the `O` functor from `[C,Setoid]^o` to `[C^o,Setoid]`: on objects, it sends the copresheaf $P$ to the presheaf $C\mapsto \hom_{[C,Setoid]}(P,yC)$ where...