🗄️
math-debrief
  • Math Debrief
  • Math: TIMELINE
  • 100-fundamentals
    • debrief-name: math section-code: 000 section-name: general section-desc: Elementary topics pervasive
      • About Mathematics
      • abstraction-in-math
      • About Math
      • Axiom schema
      • Basic concepts in math
      • Collections
      • Elementary concepts in objects
      • Elements of mathematics
      • math-as-a-language
      • Mathematical structures
      • List of mathematics-based methods
      • Mathematics and Reality
      • Mathematics: General
      • Controversial mathematics
      • the-elements-of-math
      • What is mathematics
    • The foundation of mathematics
      • Mathematical foundations
      • Foundations of Mathematics
      • Axiomatization of mathematics
      • Foundational crisis of mathematics
      • Foundations
      • Hilbert's problems
      • impl-of-math-in-set-theory
      • Gödel's Incompleteness Theorem
      • Theorems in the foundations of mathematics
      • The list of FOM candidates
      • Logicism
    • Philosophy of mathematics
      • Constructive mathematics
      • Constructive mathematics
      • Metamathematics
      • Philosophy of mathematics
      • Schools of mathematics
    • terms
      • Terms
      • Arithmetic
      • Axiom
      • The Axiomatic Method
      • discrete-math
      • 201 Discrete mathematics
      • Euclidean space
      • Formal system
      • Function
      • Generalization
      • Geometry
      • Higher-order
      • Impredicativity
      • Level of measurement
      • Mathematical definition
      • FAQ
      • Mathematical function
      • Mathematical induction
      • Mathematical object
      • Mathematical object
      • Equivalent definitions of mathematical structures
      • Mathematics
      • Mathematical model
      • mathematical-notation
      • Mathematical pages
      • Mathematical terminology
      • Mathematical adjective
      • Numbers
      • plane
      • Primer: Set Theory
      • Mathematical primitive
      • Set
      • Space
      • theory
      • Variable
  • 200 Set and Set theory
    • Sets: Hierarchy
    • set.TERMS
    • SETS › TOPICS
    • 201 Set concepts
      • Mathematical collections
      • The notion of sets
      • Specification of sets
    • Set cardinality
      • Cardinality of the continuum
      • Cardinality
      • Set Cardinality
      • cardinality2
      • Set cardinality
    • Set operations
      • Disjoint sets
      • Overlapping sets
      • Product
      • set-interactions
      • Set qualities
      • Set relations
    • Set properties
      • Basic set properties
      • Set properties
    • Set relations
      • Basic set relations
      • Disjoint sets
      • Inclusion relation
      • Membership Relation
      • Set membership
    • Summary
      • Set FAQ
      • Sets: Summary
    • Set theories
      • Axiomatic set theory
      • Set Theories
      • Naive Set Theory
      • Morse-Kelley set theory
      • von Neumann-Bernays-Gödel Set Theory
      • Quine's New Foundations (NF)
      • Cantor's set theory
      • Zermelo-Fraenkel set theory
    • Axioms of set theory
      • axiom-of-choice
      • The Axiom of Extensionality
      • Axiom of infinity
      • axiom-of-pairing
      • Axiom of powerset
      • Axiom of Regularity
      • Axiom of replacement
      • Axiom of union
      • Axiom of well-ordering
      • axiom-schema-of-comprehension
      • Axiom Schema of Specification
      • Axioms of set theories
      • List of axioms in set theory
      • ZFC Axioms
    • Sets: Terms
      • Bell Number
      • Cardinal number
      • Class (set theory)
      • Closure
      • empty-set
      • Extended set operations
      • Extensions by definitions
      • Family of sets
      • Fundamental sets
      • fundamental-sets2
      • Georg Cantor
      • History of set theory
      • Implementation of mathematics in set theory
      • Indexed family of sets
      • Extensional and intensional definitions
      • Involution
      • list-of-axioms-of-set-theory
      • Implementation of mathematics in set theory
      • Set membership
      • Naive Set Theory
      • Number of relations
      • empty-relation
      • Set Partitioning
      • Powerset
      • Russell's paradox
      • Set-builder notation
      • Set equivalence
      • Set Notation in latex
      • Set notation
      • Set partition
      • Intensional and extensional set specification
      • Set notation
      • Basic concepts in set theory
      • set-theory
      • Set Types
      • set
      • subset
      • Transfinite number
      • Tuples
      • ur-elements
  • Relations
    • basic-concepts
      • algebraic-axioms
      • Elements of a relation
      • Types of Relations
      • Named Relations
      • Relation theory
      • Relations
      • Types of relations
    • Relations
      • Definitions
      • Reflexivity
      • Symmetry
      • Transitivity
    • relation-properties
      • Uniqueness properties of relations
    • Types of relations
      • Transitivity
      • Binary Relation
      • Congruence relation
      • Connex relation
      • axioms-sets-zfc
      • Endorelation
      • Equivalence relation
      • Euclidean
      • Finitary relation
      • Heterogeneous relation
      • Homogeneous relation
      • Transitivity
      • Partial equivalence relation
      • Transitivity
      • Transitivity
      • Reflexive relation
      • Reflexivity
      • Index of relations
      • Serial relation
      • Symmetry
      • Transitivity
      • Ternary relation
      • Trichotomy
      • Universal relation
      • Well-foundedness
    • terms
      • Relations
      • Binary relation
      • Relations
      • _finitary-rel
      • Relations: Overview
      • Relations
      • Index of relations
      • Binary relations
      • Composition of relations
      • Equivalence class
      • Notation
      • Relation
      • Relations
      • Sets: Summary
      • Aggregation: Sets, Relations, Functions
  • Order theory
    • Order theory
    • List of order structures in mathematics
    • List of order theory topics
    • Order theory
      • Hasse diagram
      • Order theory
      • ordered-set
      • Partial order
      • Partially ordered set
      • Total order
  • Function Theory
    • Function Theory: GLOSSARY
    • Function Theory: HIERARCHY
    • Function Theory: LINKS
    • Function Theory: TERMS
    • Function Theory: TOPIC
    • Function Theory: WIKI
    • _articles
      • about-functions
      • Function
      • Formal definition
      • Definition
      • constant
      • Introduction
      • Types of functions
      • Functions: Summary of Notations
      • Functions: Overview
      • Properties of functions
      • Function properties
      • Functions: Summary
      • Function
    • Abjections
      • Bijective function
      • Function (abjections)
      • Injective function
      • Surjective function
    • topics
      • Function: TERMS
      • Codomain
      • Composition of functions
      • Currying
      • Division of functions
      • Domain
      • Function fixed points
      • Function cardinality
      • Function definition
      • Elements of a function
      • Function in mathematics
      • Function notion
      • Function operations
      • Function properties
      • Functional statements
      • Functions in programing languages
      • Image and Preimage
      • Image
      • Inverse function
      • Notion of functions
      • Number and types of functions between two sets
      • Operation
      • Range
      • Successor function
      • Time complexity classes
  • debrief-name: math section-code: 280 section-name: domain-theory section-desc:
    • Domain theory: LINKS
    • Domain theory
  • Logic
    • Logic: CHRONO TERMS
    • Logic: CLUSTERS
    • lo.GLOSSARY
    • Logic: Wiki links
    • 305-basic-concepts
      • Introduction to Logic
      • Argumentation
      • Logic: Basic terminology
      • Logic: Terminology
      • Truth function
      • Truth function
    • README
      • Mathematical Logic
      • Types of Logic
      • BHK interpretation
      • FOL
      • Index of Logic Forms
      • History of logic
      • Logic Indices
      • Interpretation of symbols in logic and math
      • logic-systems
      • Mathematical Logic: People and Events
      • Index of logical fallacies
      • Logical symbols
      • Mathematical conjecture
      • Mathematical induction
      • Mathematical lemma
      • Mathematical Logic
      • Mathematical proof
      • Mathematical theorem
      • Mathematical theory
      • Monotonicity of entailment
      • Satisfiability Modulo Theories
      • Sequent Calculus
      • Sequent
      • Tableaux
      • Truth tables
    • 360-propositional-logic
      • Propositional Logic
      • Propositional Logic
    • 370-predicate-logic
      • Predicate Logic
      • First-order logic
      • Predicate calculus
      • Examples of predicate formulae
    • 380-proof-theory
      • Argument-deduction-proof distinctions
      • Direct proof
      • Mathematical induction
      • Mathematical induction
      • Mathematical proof
      • Natural deduction
      • Natural deduction
      • Proof by induction
      • Proof by induction
      • proof-calculus
      • Proof Theory
      • Structural induction
      • System L
      • Proof theory
    • Logic: Indices
      • Gödel's Incompleteness Theorem
      • The History of Mathematical Logic
      • forallx
      • Logic for CS
      • Lectures in Logic and Set Theory
      • _logicomix
    • Logic
      • Logical connectives
      • Logical equivalence
    • Rules of Inference
      • WIKI
      • Conjunction elimination
      • Conjunction introduction
      • Cut rule
      • Disjunction elimination
      • Disjunction introduction
      • Disjunctive syllogism
      • Exportation
      • implication-elimination
      • implication-introduction
      • Rules of Inference: Index
      • Rules of inference
      • Rules of Inference for Natural Deduction
      • Logical Inference
      • Reiteration
      • Rule of inference
      • Structural rules
      • substitution
    • Logic
      • The principle of bivalence
      • The principle of explosion
      • The Law of Identity (ID)
      • Laws of thought
      • Properties of logic systems
      • List of laws in logic
      • The law of non-contradiction
    • Logic
      • Logic systems: LINKS
      • Logic system
      • logic-systems
      • logic-typ
      • logics-by-purpose
      • _logics
      • Affine logic
      • Algebraic logic
      • Bunched logic
      • Classical logic
      • Traditional first-order logic
      • Hoare logic
      • Linear logic
      • Modal logic
      • Non-monotonic logic
      • Syntax
      • Predicate logic
      • Propositional Logic
      • Relevance logic
      • Separation logic
      • Substructural logics
      • Syllogistic logic
    • Logic: Sections: Elementary
    • Logic: Topics
      • Pages in Logic
      • Logic ❱ Terms ❱ List
      • Logic ❱ Terms ❱ Definitions
      • Absoluteness
      • Assumption
      • Automated theorem proving
      • Canonical normal form
      • Categorical proposition
      • Classical linear logic
      • Consequence
      • Decidability
      • Deduction systems
      • deduction-theorem
      • Deductive reasoning
      • Diagonal lemma
      • Fallacy
      • Fitch notation
      • Formal language
      • formal-system
      • Formalism
      • Formula
      • functionally complete
      • Hilbert system
      • Hoare logic
      • horn-clause
      • Mathematical induction
      • Induction
      • Inductive Reasoning
      • Intuitionistic logic
      • Intuitionistic logic
      • Intuitionistic logic
      • Judgement
      • Judgments
      • Linear logic
      • Logic in computer science
      • Logic
      • Logical connective
      • Logical consequence
      • Logical constant
      • Logical form
      • axioms-sets
      • Logical reasoning
      • Ludics
      • Non-logical symbol
      • Predicate
      • Premise
      • Quantification
      • Realizability
      • Boolean satisfiability problem
      • DPLL algorithm
      • Satisfiability
      • Semantics of logic
      • Skolemization
      • SAT and SMT
      • Syntax
      • Tautology
      • Term
      • Unification
      • Validity
  • 510 Lambda Calculi
    • Lambda Calculus: GLOSSARY
    • Lambda calculi: LINKS
    • Lambda Calculus: OUTLINE
    • Lambda Calculus: Basic concepts
      • Introduction
      • Lambda expressions
      • Free variables
    • Lambda Calculi
      • Lambda calculus: LINKS
      • Lambda calculus combinators in Haskell
      • Lambda calculus: Combinators
      • Combinators
      • combos-all.js
      • combos-bird.js
      • combos-birds-list.js
      • combos-birds.js
      • Fixed-point combinator
      • Fixpoint operator
      • Lambda calculus: Fixpoint
    • combinatory-logic
      • algebraic-structures
      • Combinatory logic
      • Combinatory logic
      • relation-classification
      • 04-definition
    • Lambda calculus encoding schemes
      • bohm-berarducci-encoding
      • Index of Church encodings
      • Church encodings
      • Church Numerals
      • Encoding data structures
      • Encoding schemes in lambda calculi
      • Lambda encoding
      • Mogensen-Scott encoding
      • Parigot encoding
      • encodings
        • Encoding data structures
        • Encoding of Data Types in the λ-calculus
        • church-booleans
        • Church data structures
        • Church encoding
        • Church Numerals: Church encoding of natural numbers
        • Lambda Calculus: Church encoding
        • Lambda Calculus: Church encoding
        • church-numerals
        • Lambda Calculus: Church encoding: Numerals
        • Church pair
        • Pair
        • Lambda Calculus: Church encoding
        • Alternative encodings
        • Encoding schemes
        • Encoding schemes
        • Encodings in Untyped Lambda Calculus
        • Lambda calculus
        • Scott encoding
        • Lambda calculus: Scott encoding
    • lambda-calculus-evaluation
      • Call-by-name
      • Call-by-need
      • Call-by-value
    • lambda-calculus-forms
      • Beta normal form
      • Lambda terms
      • Fixity of lambda-terms
    • lambda-calculus-reductions
      • Alpha conversion
      • Beta reduction
      • Delta reduction
      • Eta conversion
      • Eta conversion
      • Lambda calculus: η-conversion
    • lambda-calculus
      • Alonzo Church
      • Inference rules for lambda calculus
      • Lambda Calculus: Introduction
      • Lambda abstraction
      • Lambda application
      • Lambda Calculus: Definition
      • About λ-calculus
      • Type inference
      • Lambda Calculus
      • Lambda Calculus: Introduction
      • Introduction to λ-calculus
      • Lambda calculus
      • Definition of Lambda Calculus
      • Functions in lambda calculus
      • History of Lambda Calculus
      • Using the Lambda Calculus
      • Name capturing
      • Variable occurrences
      • Variables
    • Lambda Calculus
      • Church-Rosser theorem
      • Curry's paradox
      • De Bruijn index
      • de Bruijn notation
      • Deductive lambda calculus
      • Kleene-Rosser paradox
      • Aspects of the lambda calculus
      • Function Refactoring
      • Lambda lifting
      • Let expression
      • Reduction strategy
      • Substitution
    • typed-lambda-calculi
      • Lambda Cube
      • Simply typed lambda calculus
      • System F
      • Typed lambda calculi
  • Type theory
    • Type Theory: GLOSSARY
    • Type theorists
    • Type Theory: SUMMARY
    • TERMS: Type Theory
      • Types
      • History of type theory
      • History of Type Theory
    • curry-howard-correspondence
      • The Curry-Howard Correspondence in Haskell
      • Curry-Howard correspondence
      • Curry-Howard correspondence
      • Curry-Howard correspondence
      • Curry-Howard-Lambek correspondence - HaskellWiki
    • dependent-types
      • Dependent type
      • Dependent type
    • Hindley-Milner type-system
      • Hindley-Milner type system
      • Monomorphism vs polymorphism
      • Let-polymorphism
      • The Hindley-Milner type system
      • Algorithm W in Haskell
      • Hindley-Milner Type Inference: W Algorithm
      • hindley–milner-type-system
      • Hindley-Milner type system
      • HM inference examples
      • HM in ML
      • Type Inference
    • Homotopy type theory
      • Homotopy type theory
      • Univalent Type theory as the foundations of mathematics
    • Intuitionistic type theory
      • Inductive definition
      • Inductive type
      • Intuitionistic type theory
    • Type Theory
      • TTTools
      • Coinduction
      • Impredicativity
      • Lean
      • Subsumption
    • Type Theory : Topics
      • Type Theory : Terms
      • Recursion types
      • Recursive data type
      • Subtyping
      • Type Class
      • Type Equivalence
      • Type Inference
      • Type rule
      • Type system
      • Variance
    • type-theories
      • Calculus of Constructions
      • Constructive type theory
      • ramified-type-theory
      • simple-type-theory
      • Substructural type systems
    • type-theory-general
      • Linear types
      • History of Type Theory
      • Type Theory
      • Overview
      • Type Theory
  • Abstract Algebra
    • 410-group-theory
      • Abelian group
    • algebras
      • Associative Algebra
      • Field
      • Group-like algebraic structures
      • group
      • Lattice
      • Magma
      • monoid
      • Overview of Algebras
      • Quasigroup
      • Rack and quandle
      • Ring
      • Semigroup
      • Algebra of sets
      • Setoid
    • boolean-algebra
      • Boolean algebra
      • Axioms in Boolean Algebra
      • Boolean algebra
      • Boolean Algebra Laws
      • Boolean Algebra Laws
      • Two-element Boolean algebra
      • Boolean algebra
      • Boolean domain
    • terms
      • Algebra
      • Axioms of abstract algebra
      • Algebraic notation for algebraic data types
      • Algebraic structure
      • Algebraic structure
      • Field of sets
      • Homomorphism
      • Isomorphism
      • Algebraic structures
      • Mathematical structure
      • Polynomials
      • Relation algebra
  • Category Theory
    • CT GLOSSARY
    • Category Theory: OUTLINE
    • CT SUMMARY
    • A First Introduction to Categories (2009)
      • Sets, maps, composition
      • 02-history
      • axioms-logic
      • Bijection of functions
      • Commutative diagram
      • Directed graph
      • CT prerequisites
      • String diagram
      • Transitive closure
    • Category Theory Fundamentals
      • Introduction
      • Interpretation
      • Fundamental concepts
      • Category theory
      • Category
      • Category Theory: Definitions
    • Key concepts
      • Duality
      • Functor
      • Homeset
      • Initial Object
      • Morphism
      • Natural transformation
      • Object
      • Terminal Object
    • Categorical constructions
      • Categorical constructions
      • Coproduct
      • Diagram
      • Product
      • Universal construction
    • Types of categories
      • Concrete category
      • Discrete category
      • Functor category
      • Groupoid
      • Hask
      • Kleisli category
      • Locally small category
      • Monoid
      • monoidal-categories.md
      • Index of named categories
      • Opposite category
      • Ordered category
      • Set category
      • Small category
      • Subcategory
    • Types of Functors
      • Adjoint functor
      • relation-arity
      • Endofunctor
      • Faithful functor
      • Forgetful functor
      • Hom functor
      • Identity functor
      • Inverse functor
      • Monad
      • Powerset functor
    • Types of Morphisms
      • Anamorphism
      • Automorphism
      • Catamorphism
      • Endomorphism
      • Epimorphism
      • Homomorphism
      • Hylomorphism
      • Idempotent morphism
      • Identity morphism
      • Inverse morphism
      • Isomorphism
      • Metamorphism
      • monomorphism
      • Natural isomorphism
      • Split morphism
    • 20-advanced-concepts
      • Coalgebra
      • (Co)Inductive types
      • Recursion Schemes
    • Category Theory
      • Category Theory: TERMS
      • Algebraic Data Types
      • Category Theory
      • Category
      • Coproduct
      • Function type
      • Functoriality
      • Initial Object
      • Limits and Colimits
      • Natural Transformation
      • 5. Products
      • Terminal Object
    • Category Theory :: Contents
      • CT :: Links
      • Category Theory :: Terms
      • Category :: Definition
      • F-Algebra
      • Functor
      • Initial object
      • Monoid
      • Natural Transformation
      • Number of morphisms
      • Terminal object
      • Transitive closure
      • Types of morphisms
      • Categories by cardinality
      • Types of functors
  • Number Theory
    • Invariance and Monovariance Principle
    • 615-arithmetic
      • Addition
      • Aliquot sum
      • Arithmetic function
      • Laws
      • Arithmetic operations
      • Index of arithmetic operations
      • Arithmetic operations
      • Arithmetic
      • Divisibility rules
      • Divisibility
      • division
      • Divisor Function
      • Divisor Summatory Function
      • Divisor
      • Euclidean division
      • Hyperoperations
      • hyperops
      • Modular arithmetic
      • Multiplication
      • Number Theory: primer in numbers
      • Percentage
      • Rules of Divisibility
      • Subtraction
    • The fundamental sets of numbers
      • Algebraic numbers
      • Complex numbers
      • Fractions
      • Fundamental number sets
      • Imaginary numbers
      • Integers
      • Irrational numbers
      • Natural number
      • Rational numbers
      • Real numbers
      • Transcendental numbers
      • Ulam's spiral
      • The whole numbers
    • COUNTING THEORY
      • Counting Theory
      • counting
      • Fundamental Counting Rules
    • 630-combinatorics
      • Combinatorics
      • Combinations
      • Combinatorics
      • Counting theory
      • Counting theory
      • Enumerative combinatorics
      • Partition
      • Pascals triangle
      • Permutations
      • Twelvefold way
    • Probability theory
      • Statistics › Probability theory: Glossary
      • Statistics › Probability theory › Topics
      • Statistics › Probability theory › Wiki Links
      • Conditional Probability
      • Distribution
      • Probability theory
      • Probability
    • Number theory
      • euclids-lemma
      • gcd-lcm
      • Induction
      • Infinity
      • Numbers and numerals with interesting properties
      • Lagrange's four-square theorem
      • Matrix
      • Matrix
      • List of Number Systems
      • Number Theory
      • Number Theory with Glenn Olsen
      • Number
      • Arithmetic
      • Numbers
      • numeral-prefixes
      • Numeral system
      • Numeral
      • Ordinal numbers
      • Parity
      • Peano axioms
      • Polynomial
      • Polynomial
      • Positional notation
      • Probability
      • Symbol
      • Well Ordering Principle
    • topics
      • Coprimality
      • Facorization of composite numbers
      • Fundamental Theorem of Arithmetic
      • Prime factorisation
      • Prime number
      • Prime numbers
  • Theory of computation
    • Theory of computation: Abbreviations
    • Theory of computation: CHRONOLOGICAL TOPICS
    • Theory of computation: GLOSSARY
    • Theory of Computation: HIERARCHY
    • Theory of computation: LINKS
    • Theory of computation: TERMS
    • Theory of computation: TOPICS
    • Theory of computation: WIKI
    • Theory of Computation
      • _toc-more
      • Theory of Computation
    • 610-automata-theory
      • Abstract machine
      • Automata Theory
      • Automaton
      • Edit distance
      • Finite-state Machine
      • Automata Theory: WIKI
    • Formal systems
      • Abstract interpretation
      • Alphabet
      • Binary combinatory logic
      • Chomsky hierarchy
      • Epsilon calculus
      • Formal language
      • Iota and Jot
      • Regular expression
      • Regular Language
      • SKI combinator calculus
    • 621-grammar
      • Backus-Naur Form (BNF)
      • Context-free grammar
      • Context-sensitive grammar
      • Extended Backus–Naur Form (EBNF)
      • Regular Language
      • Terminal and nonterminal symbols
    • 622-syntax
      • Syntax
    • 624-semantics
      • Axiomatic semantics
      • Denotational Semantics: Summary
      • Denotational Semantics
      • Denotational Semantics
      • Denotational semantics
      • Formal semantics
      • Operational semantics
      • Semantics in CS
      • Semantics
    • 630-computability-theory
      • Computability (recursion) theory: TERMS
      • Computability (recursion) theory: TOPICS
      • Effective Computability
      • Church Thesis
      • Church-Turing Thesis
      • Computability theory
      • Computability
      • Computable function
      • Entscheidungsproblem
      • Halting problem
      • Machine that always halts
      • McCarthy Formalism
      • Super-recursive algorithm
      • Recursion theory
    • 632-recursive-function-theory
      • Recursion Theory
      • Ackermann function
      • General recursive function
      • Minimization operator
      • Partial functions
      • Recursion Function Theory
      • Sudan function
    • 634-primitive-recursive-functions
      • Primitive Recursive Function
      • Initial functions
      • The list of primitive recursive functions
      • Primitive combination
      • Primitive composition
      • Primitive recursion
      • Successor function
    • 640-models-of-computation
      • Models of computation: Summaries
      • Model of computation
    • 680-complexity-theory
      • Algorithmic Complexity
      • Complexity Theory
  • debrief-name: math section-code: 900 section-name: aggregations section-desc: Aggregations, indices,
    • Index of closures
    • List of mathematical entities
    • List of mathematical objects
    • Enumeration of mathematical structures
    • Math : Axioms as Formulae
    • 950-math-areas
      • Areas of mathematics
      • Areas of mathematics
    • 970-links
      • check
      • Math: Links
      • Math Debrief: Links
      • Math Primer: LINKS
      • Links
      • Math: LINKS: ncatlab
      • Math: LINKS
      • WIKI
      • WIKI
      • WIKI_ALL
      • Math: Wiki lists
      • Glossary of areas of mathematics
      • WIKI_collections
      • Mathematics for Computer Science
      • Mathematics Classification
      • math
      • Resources
      • Math on YouTubel Video Playlists
      • wiki resources
    • 980-hierarchy
      • HIERAR
      • Math: Hierarchy
      • Math HIERARCHY
      • classification
        • Mathematics
        • https://ncatlab.org/nlab/all_pages https://ncatlab.org/nlab/all_pages/reference https://ncatlab.org/
        • Math Classification and Topical Pages
        • Areas of mathematics
        • Areas of mathematics
        • Math Classification: CCS
        • Math hierarchy
        • Computational mathematics
        • Taxonomy: Mathematics
        • Areas of mathematics
        • Mathematics Subject Classification
        • Math fields
        • math-topics
        • Mathematics Subject Classification – MSC
        • MSC Classification Codes
        • mss-top-levels-filenames
        • MSC classification: Top Levels
        • Math classification
    • 990-appendix
      • Math glossary at ENCYCLOPÆDIA BRITANNICA
      • Bibliography
      • Math: Abbreviations
      • math.GLOSSARY
    • Math : Canon
      • Main branches of mathematics
      • Enumeration: Math paradigms
      • enum-math-symbols
      • List of mathematical theories
      • enum-algebras
        • Group-like algebraic structures
        • Group
        • Groupoid
        • magma
        • Monoid
        • Semigroup
      • enum-axioms-indices
        • 03-variants
        • axioms-relations
        • disjoint-sets
        • ordered-pair
      • enum-axioms
        • Axiom of Extensionality
        • Axioms
          • List of Axioms
          • List of Axioms
          • LINKS
          • Index of axioms
          • Index of axioms
          • List of Axioms
          • List of Axioms in Relations
          • _laws
          • Index of axioms
          • Index of properties
          • Axioms in Boolean Algebra
          • Axioms for the Real Numbers and Integers
          • Axioms for the Real Numbers and Integers
          • ZF Axioms
          • ZFC Axioms
          • Axioms in logic
          • Axioms in set theory
          • List of axioms in set theory
        • Axioms
          • Absorption
          • Annihilation
          • Associativity
          • Cancellation
          • Closure
          • Commutativity
          • Complement laws
          • Distributivity
          • Domination
          • Idempotency
          • identity
          • Invertibility
          • involution
          • Linearity
          • Monotonicity
          • Well-definedness
          • Well-formedness
          • Well-foundedness
          • Well-ordering
      • enum-inference-rules
        • Enumeration: Rules of Inference
        • Enumeration: Rules of Inference for Intuitionistic Natural Deduction
      • Math › Logic formulae
        • Logic formulas concerning functions
        • Logic formulas concerning orders
        • Logic formulas concerning relations
        • Logic formulas concerning sets
      • enum-logic-system-elements
        • Conjecture
      • enum-logic-system-properties
        • Completeness
        • Consistency
        • Decidability
      • enum-topical-hierarchies
        • Outline of category theory
    • Mathematical Lists and Indices
      • Index of algebraic structures
      • Math equations and formulas
      • The fundamental number sets
      • index-of-math-elements
      • Arity
      • List of binary relations
      • Pretty formulae
      • Index of integer sequences
      • List of conjectures
      • Mathematical objects
      • Theorems
      • List of mathematical theories
      • list-of-unsolved-problems
      • Lists of problems in math
      • People
      • list-of-quotes-and-phrases
    • Mathematical elements
      • Mathematical (elements): PAGES
      • Mathematical abstraction
      • Mathematical analysis
      • Mathematical argumentation
      • Mathematical axiom
      • Mathematical concept
      • Mathematical constant
      • Mathematical deduction
      • Mathematical definition
      • Mathematical element
      • Mathematical expression
      • Mathematical formula
      • Mathematical method
      • Mathematical model
      • Mathematical notation
      • Mathematical object
      • Mathematical primitive
      • Mathematical reasoning
      • Mathematical statement
      • Mathematical structure
      • Mathematical symbol
      • Mathematical synthesis
  • debrief-name: math section-code: 800 section-name: misc section-desc: Misc and unclassified mathemat
    • 810-statistics
      • STATISTICS: HIERARCHY
      • STATISTICS: TERMS
      • Statistics › Topics
      • Statistics WIKI LINKS
      • Mathematical Concepts
      • Linear Regression
    • 888-calculus
      • Calculus
      • Math › Calculus › TERMS
Powered by GitBook
On this page
  • Intro
  • Set Theory and a Paradox
  • Toward a New Foundational System

Was this helpful?

  1. Type theory
  2. Homotopy type theory

Univalent Type theory as the foundations of mathematics

Univalent Foundations of Mathematics https://www.math.ias.edu/vladimir/Univalent_Foundations

Intro

The view that the foundation of mathematics rests on the set theory (ZF set theory) is the stance that majority of modern mathematicians takes.

The foundation of mathematics is a field primarily concerned with the research of those mathematical theories that may be placed at the heart of all mathematics.

the most fundamental mathematical theory, from which the entire mathematics can be derived.

Like any foundational system, set theory provides a collection of basic concepts and rules, which can be used to construct the rest of mathematics.

Set theory has sufficed as a foundation for more than a century, but it can't readily be translated into a form that computers can use to check proofs. So with his decision to start formalizing mathematics on the computer, Vladimir Voevodsky set in motion a process of discovery that ultimately led to something far more ambitious: a recasting of the underpinnings of mathematics. (using Coq, a proof assistant that provides mathematicians with an environment in which to write mathematical arguments).

Voevodsky is a permanent faculty member at the Institute for Advanced Study (IAS) in Princeton, N.J. He was born in Moscow but speaks nearly flawless English, and he has the confident bearing of someone who has no need to prove himself to anyone. In 2002 he won the Fields Medal, which is the most prestigious award in mathematics.

Set Theory and a Paradox

Set theory grew out of an impulse to put mathematics on an entirely rigorous footing - a logical basis even more secure than numbers themselves. Set theory begins with the set containing nothing - the null set - which is used to define the number zero. The number 1 can then be built by defining a new set with one element - the null set. The number 2 is the set that contains two elements - the null set (0) and the set that contains the null set (1). In this way, each whole number can be defined as the set of sets that came before it.

Set theory as a foundation includes these basic objects - sets - and logical rules for manipulating those sets, from which the theorems in mathematics are derived. An advantage of set theory as a foundational system is that it is very economical - every object mathematicians could possibly want to use is ultimately built from the null set.

On the other hand, it can be tedious to encode complicated mathematical objects as elaborate hierarchies of sets. This limitation becomes problematic when mathematicians want to think about objects that are equivalent or isomorphic in some sense, if not necessarily equal in all respects. For example, the fraction ½ and the decimal 0.5 represent the same real number but are encoded very differently in terms of sets.

On the other hand, it can be tedious to encode complicated mathematical objects as elaborate hierarchies of sets. This limitation becomes problematic when mathematicians want to think about objects that are equivalent or isomorphic in some sense, if not necessarily equal in all respects. For example, the fraction ½ and the decimal 0.5 represent the same real number but are encoded very differently in terms of sets.

"You have to build up a specific object and you're stuck with it," Awodey said. "If you want to work with a different but isomorphic object, you'd have to build that up."

But set theory isn't the only way to do mathematics. The proof assistant programs Coq and Agda, for example, are based on a different formal system called type theory.

Type theory has its origins in an attempt to fix a critical flaw in early versions of set theory, which was identified by the philosopher and logician Bertrand Russell in 1901. Russell noted that some sets contain themselves as a member. For example, consider the set of all things that are not spaceships. This set - the set of non-spaceships - is itself not a spaceship, so it is a member of itself.

Russell defined a new set: the set of all sets that do not contain themselves. He asked whether that set contains itself, and he showed that answering that question produces a paradox: If the set does contain itself, then it doesn't contain itself (because the only objects in the set are sets that don't contain themselves). But if it doesn't contain itself, it does contain itself (because the set contains all the sets that don't contain themselves).

Russell created type theory as a way out of this paradox. In place of set theory, Russell's system used more carefully defined objects called types. Russell's type theory begins with a universe of objects, just like set theory, and those objects can be collected in a "type" called a SET. Within type theory, the type SET is defined so that it is only allowed to collect objects that aren't collections of other things. If a collection does contain other collections, it is no longer allowed to be a SET, but is instead something that can be thought of as a MEGASET - a new kind of type defined specifically as a collection of objects which themselves are collections of objects.

From here, the whole system arises in an orderly fashion. One can imagine, say, a type called a SUPERMEGASET that collects only objects that are MEGASETS. Within this rigid framework, it becomes illegal, so to speak, to even ask the paradox-inducing question, "Does the set of all sets that do not contain themselves contain itself?" In type theory, SETS only contain objects that are not collections of other objects.

An important distinction between set theory and type theory lies in the way theorems are treated. In set theory, a theorem is not itself a set - it's a statement about sets. By contrast, in some versions of type theory, theorems and SETS are on equal footing. They are "types" - a new kind of mathematical object. A theorem is the type whose elements are all the different ways the theorem can be proved. So, for example, there is a single type that collects all the proofs to the Pythagorean theorem.

To illustrate this difference between set theory and type theory, consider two sets: Set A contains two apples and Set B contains two oranges. A mathematician might consider these sets equivalent, or isomorphic, because they have the same number of objects. The way to show formally that these two sets are equivalent is to pair objects from the first set with objects from the second. If they pair evenly, with no objects left over on either side, they're equivalent.

When you do this pairing, you quickly see that there are two ways to show the equivalence: Apple 1 can be paired with Orange 1 and Apple 2 with Orange 2, or Apple 1 can be paired with Orange 2 and Apple 2 with Orange 1. Another way to say this is to state that the two sets are isomorphic to each other in two ways.

In a traditional set theory proof of the theorem Set A ≅ Set B (where the symbol ≅ means "is isomorphic to"), mathematicians are concerned only with whether one such pairing exists. In type theory, the theorem Set A ≅ Set B can be interpreted as a collection, consisting of all the different ways of demonstrating the isomorphism (which in this case is two). There are often good reasons in mathematics to keep track of the various ways in which two objects (like these two sets) are equivalent, and type theory does this automatically by bundling equivalences together into a single type.

This is especially useful in topology, a branch of mathematics that studies the intrinsic properties of spaces, like a circle or the surface of a doughnut. Studying spaces would be impractical if topologists had to think separately about all possible variations of spaces with the same intrinsic properties. (For example, circles can come in any size, yet every circle shares the same basic qualities.) A solution is to reduce the number of distinct spaces by considering some of them to be equivalent. One way topologists do this is with the notion of homotopy, which provides a useful definition of equivalence: Spaces are homotopy equivalent if, roughly speaking, one can be deformed into the other by shrinking or thickening regions, without tearing.

The point and the line are homotopy equivalent, which is another way of saying they're of the same homotopy type. The letter P is of the same homotopy type as the letter O (the tail of the P can be collapsed to a point on the boundary of the letter's upper circle), and both P and O are of the same homotopy type as the other letters of the alphabet that contain one hole - A, D, Q and R.

Homotopy types are used to classify the essential features of an object. The letters A, R and Q all have one hole, and so are the same homotopy type. The letters C, X and K are also of the same homotopy type, as they can all transform into a line.

Topologists use different methods for assessing the qualities of a space and determining its homotopy type. One way is to study the collection of paths between distinct points in the space, and type theory is well-suited to keeping track of these paths. For instance, a topologist might think of two points in a space as equivalent whenever there is a path connecting them. Then the collection of all paths between points x and y can itself be viewed as a single type, which represents all proofs of the theorem x = y.

Homotopy types can be constructed from paths between points, but an enterprising mathematician can also keep track of paths between paths, and paths between paths between paths, and so on. These paths between paths can be thought of as higher-order relationships between points in a space.

Voevodsky tried on and off for 20 years, starting as an undergraduate at Moscow State University in the mid-1980s, to formalize mathematics in a way that would make these higher-order relationships - paths of paths of paths - easy to work with. Like many others during this period, he tried to accomplish this within the framework of a formal system called category theory. And while he achieved limited success in using category theory to formalize particular regions of mathematics, there remained regions of mathematics that categories couldn't reach.

Voevodsky returned to the problem of studying higher-order relationships with renewed interest in the years after he won the Fields Medal. In late 2005, he had something of an epiphany. As soon as he started thinking about higher-order relationships in terms of objects called infinity-groupoids, he said, "many things started to fall into place."

Infinity-groupoids encode all the paths in a space, including paths of paths, and paths of paths of paths. They crop up in other frontiers of mathematical research as ways of encoding similar higher-order relationships, but they are unwieldy objects from the point of view of set theory. Because of this, they were thought to be useless for Voevodsky's goal of formalizing mathematics.

Yet Voevodsky was able to create an interpretation of type theory in the language of infinity-groupoids, an advance that allows mathematicians to reason efficiently about infinity-groupoids without ever having to think of them in terms of sets. This advance ultimately led to the development of univalent foundations.

Voevodsky was excited by the potential of a formal system built on groupoids, but also daunted by the amount of technical work required to realize the idea. He was also concerned that any progress he made would be too complicated to be reliably verified through peer review, which Voevodsky said he was "losing faith in" at the time.

Toward a New Foundational System

With groupoids, Voevodsky had his object, which left him needing only a formal framework in which to organize them. In 2005 he found it in an unpublished paper called FOLDS, which introduced Voevodsky to a formal system that fit uncannily well with the kind of higher-order mathematics he wanted to practice.

In 1972 the Swedish logician Per Martin-Löf introduced his own version of type theory inspired by ideas from Automath, a formal language for checking proofs on the computer. Martin-Löf type theory (MLTT) was eagerly adopted by computer scientists, who have used it as the basis for proof-assistant programs.

In the mid-1990s, MLTT intersected with pure mathematics when Michael Makkai, a specialist in mathematical logic who retired from McGill University in 2010, realized it might be used to formalize categorical and higher-categorical mathematics. Voevodsky said that when he first read Makkai's work, set forth in FOLDS, the experience was "almost like talking to myself, in a good sense."

Voevodsky followed Makkai's path but used groupoids instead of categories. This allowed him to create deep connections between homotopy theory and type theory.

"This is one of the most magical things, that somehow it happened that these programmers really wanted to formalize [type theory]," Shulman said, "and it turns out they ended up formalizing homotopy theory."

Voevodsky agrees that the connection is magical, though he sees the significance a little differently. To him, the real potential of type theory informed by homotopy theory is as a new foundation for mathematics that's uniquely well-suited both to computerized verification and to studying higher-order relationships.

Voevodsky first perceived this connection when he read Makkai's paper, but it took him another four years to make it mathematically precise. From 2005 to 2009 Voevodsky developed several pieces of machinery that allow mathematicians to work with sets in MLTT "in a consistent and convenient way for the first time," he said. These include a new axiom, known as the univalence axiom, and a complete interpretation of MLTT in the language of simplicial sets, which (in addition to groupoids) are another way of representing homotopy types.

This consistency and convenience reflects something deeper about the program, said Daniel Grayson, an emeritus professor of mathematics at the University of Illinois at Urbana-Champaign. The strength of univalent foundations lies in the fact that it taps into a previously hidden structure in mathematics.

"What's appealing and different about [univalent foundations], especially if you start viewing it as replacing set theory," he said, "is that it appears that ideas from topology come into the very foundation of mathematics."

From Idea to Action Building a new foundation for mathematics is one thing. Getting people to use it is another. By late 2009 Voevodsky had worked out the details of univalent foundations and felt ready to begin sharing his ideas. He understood people were likely to be skeptical. "It's a big thing to say I have something which should probably replace set theory," he said.

Voevodsky first discussed univalent foundations publicly in lectures at Carnegie Mellon in early 2010 and at the Oberwolfach Research Institute for Mathematics in Germany in 2011. At the Carnegie Mellon talks he met Steve Awodey, who had been doing research with his graduate students Michael Warren and Peter Lumsdaine on homotopy type theory. Soon after, Voevodsky decided to bring researchers together for a period of intensive collaboration in order to jump-start the field's development.

Along with Thierry Coquand, a computer scientist at the University of Gothenburg in Sweden, Voevodsky and Awodey organized a special research year to take place at IAS during the 2012-2013 academic year. More than thirty computer scientists, logicians and mathematicians came from around the world to participate. Voevodsky said the ideas they discussed were so strange that at the outset, "there wasn't a single person there who was entirely comfortable with it."

The ideas may have been slightly alien, but they were also exciting. Shulman deferred the start of a new job in order to take part in the project. "I think a lot of us felt we were on the cusp of something big, something really important," he said, "and it was worth making some sacrifices to be involved with the genesis of it."

Following the special research year, activity split in a few different directions. One group of researchers, which includes Shulman and is referred to as the HoTT community (for homotopy type theory), set off to explore the possibilities for new discoveries within the framework they'd developed. Another group, which identifies as UniMath and includes Voevodsky, began rewriting mathematics in the language of univalent foundations. Their goal is to create a library of basic mathematical elements - lemmas, proofs, propositions - that mathematicians can use to formalize their own work in univalent foundations.

As the HoTT and UniMath communities have grown, the ideas that underlie them have become more visible among mathematicians, logicians and computer scientists. Henry Towsner, a logician at the University of Pennsylvania, said that there seems to be at least one presentation on homotopy type theory at every conference he attends these days, and that the more he learns about the approach, the more it makes sense. "It was this buzzword," he said. "It took me awhile to understand what they were actually doing and why it was interesting and a good idea, not a gimmicky thing."

A lot of the attention univalent foundations has received is owing to Voevodsky's standing as one of the greatest mathematicians of his generation. Michael Harris, a mathematician at Columbia University, includes a long discussion of univalent foundations in his new book, Mathematics Without Apologies. He is impressed by the mathematics that surround the univalence model, but he is more skeptical of Voevodsky's larger vision of a world in which all mathematicians formalize their work in univalent foundations and check it on the computer.

"The drive to mechanize proof and proof verification doesn't strongly motivate most mathematicians as far as I can tell," he said. "I can understand why computer scientists and logicians would be excited, but I think mathematicians are looking for something else."

Voevodsky is aware that a new foundation for mathematics is a tough sell, and he admits that "at the moment there is really more hype and noise than the field is ready for." He is currently using the language of univalent foundations to formalize the relationship between MLTT and homotopy theory, which he considers a necessary next step in the development of the field. Voevodsky also has plans to formalize his proof of the Milnor conjecture, the achievement for which he earned a Fields Medal. He hopes that doing so might act as "a milestone which can be used to create motivation in the field."

Voevodsky would eventually like to use univalent foundations to study aspects of mathematics that have been inaccessible within the framework of set theory. But for now he's approaching the development of univalent foundations cautiously. Set theory has undergirded mathematics for more than a century, and if univalent foundations is to have similar longevity, Voevodsky knows it's important to get things right at the start.

PreviousHomotopy type theoryNextIntuitionistic type theory

Last updated 3 years ago

Was this helpful?