Re:Category theory is a universal modeling language
by ukj on Thursday April 29, 2021 @03:40PM
(#26985683)
That's precisely what it is. Homotopy/Category theory is strongly-normalising.
Which is roughly what the Univalence axiom tells us: identity is equivalent to equivalence.
The identity type is the normal/canonical/unique form for all object of a particular type.
Yet another perspective is the question "Do A and B have the same structure? Are they isomorphic?". When you are dealing with finite data types the answer to such questions is inevitably in the domain of Finite Model Theory ( https://en.wikipedia.org/wiki/Finite_model_theory ). Finite categories are the same sort objects as DB schemas.
Which is roughly what the Univalence axiom tells us: identity is equivalent to equivalence.
The identity type is the normal/canonical/unique form for all object of a particular type.
Yet another perspective is the question "Do A and B have the same structure? Are they isomorphic?". When you are dealing with finite data types the answer to such questions is inevitably in the domain of Finite Model Theory ( https://en.wikipedia.org/wiki/Finite_model_theory ). Finite categories are the same sort objects as DB schemas.