Here's a sort of sketch of the pieces I had in mind. Many of them could probably be parallelized.
WildCat/Displayed.v contains a start, up through displayed 0-coherent 1-functors. Most of the rest of Core can presumably be likewise mimicked, along with proofs that the sigma-type of a displayed category inherits a category structure with the same amount of coherence.
Define one or more wild categories of wild categories, perhaps with varying amounts of coherence.
A sufficiently coherent functor A -> WildCat should induce by covariant Grothendieck construction a displayed category over A.
Similarly, a functor A^op -> WildCat should induced by contravariant Grothendieck construction a displayed category over A.
Here's a sort of sketch of the pieces I had in mind. Many of them could probably be parallelized.
WildCat/Displayed.v contains a start, up through displayed 0-coherent 1-functors. Most of the rest of Core can presumably be likewise mimicked, along with proofs that the sigma-type of a displayed category inherits a category structure with the same amount of coherence.
Define one or more wild categories of wild categories, perhaps with varying amounts of coherence.
A sufficiently coherent functor A -> WildCat should induce by covariant Grothendieck construction a displayed category over A.
Similarly, a functor A^op -> WildCat should induced by contravariant Grothendieck construction a displayed category over A.