Jason (jcreed) wrote,
Jason
jcreed

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

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?
Tags: hott, math
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments