And of course, it actually took a bunch of struggle, but I finally ended up with
https://github.com/jcreedcmu/HoTT-Agda/blob/experimental/Jcreed/Yoneda.agda
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?
