infryq

Sally came out to astoria so we hung out a bit. Banh mi at district saigon was amaaaaazing. Cracked open the MELL-is-decidable paper from 2015 that a Mysterious Academic Friend With Connections sent me, but haven't digested it yet.

l33tminion

What's new, DW? (And all the rest of you out there on the intertubes / blag-a-ma-phone / real world but specifically the part of the real world that is on the internet.)

As always, last week was busy and this week is busy.

Last week was partially busy because we had to take Wednesday off to take the kid to the doctor for an eye infection. Diagnosis was "it's probably viral but here's some antibiotics because obviously not going to take any chances with the ocular orbs". So little Eris gets to suffer the indignity of ointment-to-the-eyes three times a day for a week. Kid is of course not a fan of this development, but at least it doesn't sting, so she gets over the indignity of having her eyelids pried open pretty quickly after. She wasn't too bothered by the infection, and it's cleared up. Plus Julie and I so far seem uninfected.

Last weekend, we went to Jupiter, Florida to visit Kristin and Jimmy and Emilia for a dinosaur-themed birthday party for Emilia and her bestie, Jacob. Kristen threw a really fun and quite elaborate party. The kids had a blast, the parents got to hang out and relax and take a lot of cute photos. Which is really what one hopes for in a kid's birthday party. Erica definitely enjoyed the time with extended family, especially her cousin. Happy birthday, Emilia, may age four be a good year for you!

Eristic improvements: Repeating words, remembering some words by sight (?), remembering the names of some letters, better at matching shapes, better reasoning about rotation of 3D objects.

Current Mood: cheerful

jcreed

Hot today, thunderstorms. Giving the math a break and switching back to working on a dumb react toy.

jcreed

Today have been thinking about the internal definition of Grothendieck universes. Seems reasonable to me to try to impose univalence by demanding a unique name for each nameable indexed family? In which case you get a nice lemma that any two such univalent universes with the same set of nameable morphisms are isomorphic in a suitable sense.

jcreed

I wonder if there's a nice way to unify
(a) the idea that if you write a pure program over no particular monad, with no particular effects, then you should be able to use it in --- that is, canonically lift it into --- an otherwise monadic/effectful context
(b) the idea that internalizing parametricity in a logical framework feels like the ability to take a construction valid in a category C and hoisting it up to the category C^J where J can be, for example, the "free-living span" category * ⇐ * ⇒ *, in which case you get relational parametricity for a binary relation.

In both cases, it seems like you write a program "parametric over" the ambient category you're doing programming in, relying only on the fact that it's CCC, has initial algebras for whatever datatypes you need, etc. etc., and you could then instantiate it at other categories --- like the kleisli category for the monad you're interested in in (a), or the category C^J for (b), as long as those other categories support the same constructs you need to write your programs with.

jcreed

Reading some more papers on dependent types and parametricity.

jcreed

Ah, I thought for the millionth time I had a perfect definition, but now I realize I need some kind of internalization of parametricity in agda for it to work. But I'm not sure precisely how much I need, or how to be sure whatever I postulate is sound, and still don't fully grok that Atkey-Ghani-Johann paper.

The definition in question's nice and small, though:

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

open import HoTT hiding (Bool ; true ; false ; _$_ ; Path)

module Knot where

Pair : ∀ {n} → Set n → Set n
Pair X = X × X

record Bundle : Set₂ where
  constructor MkBundle
  field
    Gr : Set₁
    Bd : Gr → Set₁
    Mod : (X : Set) → Gr → Set₁
    Eq : (G : Gr) (δ : Bd G) (X : Set) (M : Mod X G) → Set

module _Next (β : Bundle) where
  open Bundle β

  nGr : Set₁
  nGr = Σ Gr (λ G → (Bd G → Set))
  nMod : Set → nGr → Set₁
  nMod X (G , C) = Σ (Mod X G) (λ M → (δ : Bd G) (c : C δ) → Eq G δ X M)
  nBd : nGr → Set₁
  nBd nG@(G , C) = Σ (Bd G) (λ δ → Pair ((X : Set) (M : nMod X nG) → Eq (fst nG) δ X (fst M)))
  nEq : (nG : nGr) (δ : nBd nG) (X : Set) (M : nMod X nG) → Set
  nEq _ (_ , δ) X M = fst δ X M == snd δ X M

  Next : Bundle
  Next = MkBundle nGr nBd nMod nEq

open _Next using (Next)

L-1 : Bundle
L-1 = MkBundle (Lift ⊤) (λ _ → Lift ⊤) (λ _ _ → Lift ⊤) (λ _ _ X _ → X)
L0 = Next L-1
L1 = Next L0
L2 = Next L1
-- etc.

The idea is that Ln gives you information the level of n-cells. Gr is the type of n-graphs, Bd is the type of n-boundaries, Mod X G is the type of models of the graph G into the set X, and Eq G δ X M is the type of paths in X filling in the boundary δ, assuming that the model M governs how lower-dimensional cells are mapped into X.

	L-1	L0	L1	L2
Gr	⊤	a set	a graph	a graph with 2-cells
Bd G	⊤	a pair of points in G	a pair of parallel paths in G	a pair of hemispheres in G
Mod X G	⊤	a point in X for every point in the graph	...and paths in X for every edge in the graph	...and 2-cells in X for every 2-cell in the 2-graph
Eq G δ X M	a point in X	a path in X between where M sends the two points of δ	a 2-cell in X between where M sends the two paths in δ	a 3-cell in X between where M sends the two 2-paths in δ

The critical twist where I thought I was merely cleverly taking advantage of the ambient world of the inductive definition of equality is where I say
... (X : Set) (M : nMod X nG) → Eq (fst nG) δ X (fst M) ...
in the definition of nBd. This is intended to be the definition of a path. A path with boundary δ is a proof that when you map the "endpoints" of δ into any set X by any model M, the image of those "endpoints" are equal.

Concretely: what's a 1-path from C to D? A proof that, for any X and any model M into X that takes 0-cells of M to points of X and 1-cells of M to paths in X, that M(C) == M(D).

(This may seem redundant with the general HoTT mindset, which easily answers the question "what's a 1-path from C to D?" with just "well, a map from the interval type", but I'm trying to build up arbitrary HITs from simpler data than postulating that various HITs exist)

jcreed

Made some really good agda progress today sketching out stuff concretely in low dimensions, but still having a little trouble tying the knot into a general definition.

l33tminion

I was doing well on posting, then suddenly I was once again super-behind.

I don't even need to know where to begin with political news. The Comey stuff wasn't very unexpected: Trump leaned on Comey to shut down the Flynn investigation, then when Comey demurred, Trump fired him. But of course Trump's core supporters are going to come out thinking this is totally fine, it's Trump being Trump.

Rumors that Trump didn't know there was a US military base in Quatar before being persuaded by the Saudis to side with them in a diplomatic crisis based on a fake news report are pretty alarming, though. Ditto for him leaving out a line about article 5 (the mutual defense pact bit) during his speech at NATO. But perhaps that's another thing that would please his supporters.

Then the UK elections happened this weekend, in a total back-fire for the Conservatives where liberal gains in parliament might ironically result in an even more right-wing UK government, as the Conservatives now are beholden to a far-right coalition partner for a majority. Or just a completely destabilized government, who knows?

In other news, the greatest climber in the world climbed El Capitan in Yosemite without ropes. Insanity, but it's amazing that a human can even accomplish such a feat.

Work's been busy, I've been shifting my focus a bit in terms of which goals I'll aim to accomplish before the end of the quarter. That's going well.

I've been watching a bit of Steven Universe with Xave over lunch break (it's a fun show, though the longer plot arcs seem to be slow to build; I love the style of visual humor, the animation is brilliant).

It's Pride week, and the parade yesterday was big and colorful as always. The weather has been hot. It's not even summer yet.

Today I was mostly out and about with the kid doing errands.

There's nothing like a cool shower in the dark after a hot day.

My parents are off on a European holiday. Enjoying the photos. Happy anniversary!

Eristic improvements: Fetching objects by name, better memory of numbers and letters, recognition of specific letters (maybe), matching shapes to outlines (including letters), some new words (including "apple" and "[ba]nana").

Current Mood: cheerful

jcreed

Rereading Cai et al.'s 2014 paper on incrementalizing computations and trying to more deeply understand bob atkey's observation that what they're doing is essentially the same thing as parametricity-via-reflexive-graphs. Thanks to arntz for directing me to that post.

S	M	T	W	T	F	S
				1	2	3
4	5	6	7	8	9	10
11	12	13	14	15	16	17
18	19	20	21	22	23	24
25	26	27	28	29	30

Reading

(no subject)

Erisaurus

(no subject)

(no subject)

(no subject)

(no subject)

(no subject)

(no subject)

Back to the Backlog Before the Week

(no subject)

Profile

June 2017

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags