Dear anyone currently lost listening to the #ylj19 keynote: it's totally fine, there's a bunch of implied context here.
(For example, what a 'family of types' is, or [earlier] what the typeclass and GADT notations refer to.)
Conversation
One thing that might help with understanding ‘identity types’ is looking at the definition in haskellish syntax:
data (=) :: a -> a -> Type where
refl :: (x :: a) -> x = x
Other notations used in the talk are:
x = y == Id x y
x = y == x =a y
#YLJ19
1
1
2
Yes. But half of it wasn't introduced; I was trying to make a point about the inaccessibility of a beginner keynote talk.
1
1
Yeah, agreed. Sorry, was just trying to provide a bit more context for anyone who might be reading along.
1
1
Thanks; it's appreciated. Sorry for getting defensive. 😰
1