Not sure what the 'W' stands for, could be from the Martin-Löf concept of 'wellorderings'. I think its a 'W' and not omega. Though it seems related to 'ω-complete partial order' (see cpo) from denotational semantics/domain theory.
In category theory this is an initial algebra for a polynomial endofunctor.
In type theory it is a free term algebra.
In category theory the locally closed Cartesian category is the counterpart of extensional type theory.
For intensional type theory we need to add quotient completions - used for modeling extensional type theories into intensional ones.
a categorification of the concept of “theory”.
Setoids are discussed on this page.
In mathematics, a setoid (X, ~) is a set (or type) X equipped with an equivalence relation ~.
Often in mathematics, when one defines an equivalence relation on a set, one immediately forms the quotient set (turning equivalence into equality). In contrast, setoids may be used when a difference between identity and equivalence must be maintained, often with an interpretation of intensional equality (the equality on the original set) and extensional equality (the equivalence relation, or the equality on the quotient set). - From Wiki
One way to define a setoid is define a tuple consisting of:
- A type T (the carrier set).
- A relation ~.
- A proof that ~ is an equivalence relation over T
- the reflexivity a ~ a.
- the symmetry a ~ b if and only if b ~ a.
- the transitivity if a ~ b and b ~ c, then a ~ c.
Extensionality of functions
if f(x) = g(x) for all x
then f = g
Example - consider the two functions f and g mapping from and to natural numbers, defined as follows:
- To find f(x), first add 5 to x, then multiply by 2.
- To find g(x), first multiply x by 2, then add 10.
These functions are extensionally equal; given the same input, both functions always produce the same value. But the definitions of the functions are not equal, and in that intensional sense the functions are not the same.
Functions between Setoids
Extensional Functions between Setoids
A function between setoids is a function between the undelying types (sets) together with a proof of extensionality:
A function |f| : |X|->|Y| is extensional, with respect to the equalities of X and Y,if there is a term of type:
f ~X=>Y g: Π|x|,|x'|:|X| x ~X x' -> |f|(x) ~Y |f|(y)
The bars, as in |x|, indicate x is an element of the underlying type. This distinction will usually be dropped if extensionality applies.
Algebra of Extensional Trees
Topological Space and W-types
Are the structures of topological Spaces (especially Alexandrov topology) and W-types related in some way?
They both seem to be able to code linear structures and trees but not loops (circles).
Category Theory and W-types
In category theory W-types are initial algebras for polynomial endofunctors.
- Quotient completion for the foundation of constructive mathematics - pdf
- W-types in setoids - pdf
- Elementry Doctrine (Lawvere) - pdf
- Split Fibration.
- Constructive Mathematics
- extensionality of functions
For more information about the relationship between type theory and category theory see this page.