Jason (jcreed) wrote,

Been messing around some more in a clone of the HoTT-Agda repo. I tried, as a little exercise, proving the Yoneda embedding --- or, actually, what I usually hear called the co-Yoneda embedding, the one that goes Cop to SetsC --- is injective, thinking it would be easy.

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)))))

   I : Set
   interval-equiv : coyoneda I ≡ F


Can I extract the induction principle and β-rules out of this somehow?
Tags: hott, math

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded