Jason (jcreed) wrote,

I was going to go to Finding Nemo with tom and ellen but the fact that I had already seen it made it kind of hard to work up any motivation to actually leave the house.

Had a useful idea about this encoding while lying (laying? I can never remember.) in bed. I think I can throw this whole business of a limit predicate on terms out the window and just make the type-level definition
%abbrev lim = [n':nat] {n:nat} {y:phd} ({cvt:phd->hd} token n (cvt y)) -> ge n n' -> hd
and talk about terms at type lim n' for n' cranking down inductively as one chews through S while showing M . S = M' . S implies M = M'. Yeah, I think that should work.

  • (no subject)

    A nice natural example of a bicategory (non-strict 2-category) I didn't know about before: Objects are sets. Morphisms from A to B are "state…

  • (no subject)

    Read a bit about alexandrov topologies and chu spaces and stuff. Is there a good completion of the analogy preorder (i.e. alexandrov topology) :…

  • (no subject)

    Interesting paper from Noam and Paul-André. The technical condition about cartesian morphisms in the definition of a fibration of categories…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded