Homotopy Type Theory
SEPS > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Idea
< SEPS
Mike Shulman’s dependently typed first-order theory SEPS.
Definition
A model of SEPS consists of
-
A type , whose terms are called “sets”.
-
For each “set” , a set , whose terms are called “elements”.
-
For each “set” and , a set , whose terms are called “pairs”.
-
For each “set” and , a function with functions and
-
For each “set” , a type , whose terms are called “subsets”, and a term
A “relation” is a term .
-
For each “set” , , , a function
and a term
where is the propositional truncation of the type .
-
For each “set” , , a relation
and terms
Let the type of all functional entire “relations” between “sets” and in be defined as
-
For each “set” and , a function and a term .
-
A “set” with a term .
-
For each “set” , there is a function , and for every subset there is an injection? .
-
For each “set” , a “set” and a “relation” and a term
-
A “set” with functional entire “relations” and and a term
- For each “set” and function , a “set” with a functional entire “relation” , a function and terms
See also
Revision on June 7, 2022 at 22:18:35 by
Anonymous?.
See the history of this page for a list of all contributions to it.