jcreed

Overslept, read some category theory papers, didn't do a whole lot else productive.

Took the train back home. It was a bit annoyingly delayed due to a freight train ahead of us, which meant that I got back in the middle of rush hour instead of an hour before, so the MTA trains in turn were pretty fucked, so I had a long, hot walk back home from the train station about 4 stops away that I decided to give up from.

17776 ended today. Sad, but nice to have a contained little story instead of a sprawling Joycean glorious mess like Homestuck.

Popped over to B&G to get a new mouse (my favored years-and-years-old one is finally having debouncing failures and registering double-clicks when I single click about 20% of the time) and an external hard drive for making backups.

Saw a talk over at Cooper by Just van Rossum, Guido's little brother, who makes fonts and animations and things. Fun stuff.

Really falling in love with 17776, a story about space probes and football and lunchables and what it means to be human.

Let's say you have a weak omega-category W.

Suppose X, Y are n-cells in it with the same boundary. Say X and Y are equivalent in the expected sense that there are f and g going back and forth such that fg and gf are (coinductively, in the same sense) equivalent to identities.

I think maybe the following univalence-like property is true:
Let equivalent X, Y be given. Then for all "good" sentences P(x) with one free variable x of the same type as X, Y, we have that P(X) holds iff P(Y) holds. Where "good" means you're allowed to mention some constants drawn from W, and all logical connectives including first-order quantifiers over cells in W of a given domain and codomain, but not including any notion of on-the-nose equality.

Balanced my checkbook. More futzing with blender. Watched part of this video about the 4-color theorem that noam sent me ages ago, neat stuff.

Huh, no matter how much I think I basically understand HoTT, there's always more interesting subtleties in how it interacts with my expectations of how doing math usually works. Here's an example where a naive understanding of what it means to have unique typing derivations fails.

Suppose it were true that for any notion of term and type, where every term is well-typed and synthesizes its type (via GetTy) that every two derivations of the trivial typing relation are the same.

{-# OPTIONS --without-K --rewriting #-}

module Example where

open import HoTT

module UniqueOf (Tm : Set) (Ty : Set) (GetTy : Tm → Ty) where
  data Of (M : Tm) : Ty → Set where
    OfTm : Of M (GetTy M)

  postulate
    OfSame : (M : Tm) (A : Ty) (of1 of2 : Of M A) → of1 == of2

This seems innocuous, right? There's only one way to prove Of for a given term (namely OfTm) so any two such proofs ought to be the same.

Nope! From this we can prove uniqueness of identity types across all types, not a contradiction, but definitely anathema to the idea that types are potentially spaces with rich path structure:

EqSame : (A : Set) (a b : A) (p q : a == b) → p == q
EqSame A a b p q = ! (cvtinv p) ∙ ap cvti cvtEq ∙ cvtinv q where
  open UniqueOf A A (λ x → x)

  cvt : {a b : A} → (a == b) → Of a b
  cvt idp = OfTm
  cvti : {a b : A} → Of a b → (a == b)
  cvti OfTm = idp
  cvtinv : {a b : A} (x : a == b) → cvti (cvt x) == x
  cvtinv idp = idp

  cvtEq : cvt p == cvt q
  cvtEq = OfSame a b (cvt p) (cvt q)

(this is really just the one-endpoint vs. two-endpoint path type distinction in disguise; what I find interesting about it is that it's so shallowly disguised, but still caught me off-guard)

Trying to bash out a sketch of a proof that the Finster-Mimram definition of ω-categories has something to do with my recent guess of a definition. Finding out I haven't really internalized the definition of categories-with-families enough.

Tried to go to studio square with K and her parents, but it turned out to be closed. Tried bohemian beer garden instead, got a big ol' meat variety platter, weather was nice, had a good time.