And of course, it actually took a bunch of struggle, but I finally ended up with
in which "Functor" is actually a lie, since I'm not requiring preservation of composition or identities. Dunno, I think it is quite pretty how everything works out, particularly how the naturality property falls out of the identity elimination.
A question: armed with the confidence that coyoneda is injective, can I use this to parsimoniously characterise HITs? Can I just define, for example, the interval by saying
F = functor (λ A → Σ A (λ a → Σ A (λ b → a ≡ b))) (λ f pkg → (f (π₁ pkg)) , ((f (π₁ (π₂ pkg))) , (ap f (π₂ (π₂ pkg))))) postulate I : Set interval-equiv : coyoneda I ≡ F
Can I extract the induction principle and β-rules out of this somehow?