And from the previous article:
> What I do love about category theory is that it is not some framework, or design pattern, or best practice that somebody came up with empirically because it helped them solve their problem, but it has strong mathematical foundations. It always adds up, things click smoothly, and it is just so satisfying and fun to experience this.
I was thinking about that in the context of nominal and structural typing. From my (limited) understanding, set theory is equivalent to structural typing. That would mean the following:
type point = { x: int; y: int }
type my_point = { x: int; y: int }
let example (p: point) = p.x + p.y
let po: point = { x = 5; y = 6 }
let my_po: my_point = { x = 1; y = 2 }
example po // => 11
example my_po // => type error
po ∈ point // Valid statement, which happens to be true
po ∈ my_point // Valid statement, which happens to be false
my_po ∈ point // Valid statement, which happens to be false
my_po ∈ my_point // Valid statement, which happens to be true
po : point // Valid expression, since the annotation passes the type checker; equivalent to `po`
po : my_point // Invalid expression, since the annotation doesn't pass the type checker
my_po : point // Invalid expression, since the annotation doesn't pass the type checker
my_po : my_point // Valid expression, since the annotation passes the type checker; equivalent to `my_po`While it's about HoTT, it starts with a very clear general-audience explanation on why and how type theory is different from set theory.
Your two types are isomorphic. They are not equal.