☰
TypeTheory Proof Engine
Wolfram Institute
⋮
Resource page
Wolfram
Institute/Type
Theory
Type
Theory Proof Engine
Tutorials
Cubical Type Theory
Erased and Affine Variables
Getting Started with Type
Theory
Homotopy Type Theory
Instances and Coercions
Mathlib in Type
Theory
Rules and Computation
The Integers
The Type
Theory Prelude
Loading...
Addition
Associativity
Addition
Commutativity
Addition
Monotonicity
Addition
Subtraction
Cancellation
Addition
Successor
Left
Addition
Successor
Right
Addition
Zero
Left
Addition
Zero
Right
And
Decidable
And
Elimination
Left
And
Elimination
Right
And
Introduction
Cartesian
Product
Choice
Chosen
Witness
Chosen
Witness
Property
Circle
Base
Circle
Induction
Circle
Induction
Base
Circle
Induction
Loop
Circle
Loop
Cubical
Composition
Cubical
Transport
Decidable
Decidable
False
Decidable
True
Decide
Decide
Soundness
Definitionally
Equal
Q
Dependent
Congruence
Dependent
Pair
Dependent
Sum
Disjoint
Union
Double
Negation
Elimination
Empty
List
Equality
Congruence
Equality
Reflexivity
Equality
Substitution
Equality
Symmetry
Equality
To
Equivalence
Equality
Transitivity
Equivalence
Equivalence
Introduction
Equivalence
Proof
Equivalence
To
Equality
Equivalence
To
Path
Equivalent
Backward
Equivalent
Forward
Equivalent
Introduction
Equivalent
Reflexivity
Equivalent
Symmetry
Equivalent
Transitivity
Excluded
Middle
Exists
Introduction
False
Elimination
Fiber
Function
Extensionality
Glue
Elimination
Glue
Introduction
Glue
Type
Identity
Equivalence
Impredicative
Maximum
Inductive
Recursor
Integer
Addition
Associativity
Integer
Addition
Commutativity
Integer
Addition
Negation
Integer
Addition
Zero
Integer
Distributivity
Integer
Equality
Decidable
Integer
Less
Equal
Of
Difference
Integer
Less
Equal
Of
Multiple
Integer
Less
Equal
Reflexivity
Integer
Multiplication
Associativity
Integer
Multiplication
Commutativity
Integer
Multiplication
One
Integer
Nonnegative
Addition
Integer
Nonnegative
Cancellation
Integer
Nonnegative
Scaling
Integer
Of
Natural
Addition
Integer
Of
Natural
Less
Equal
Integer
Of
Natural
Multiplication
Integer
Square
Nonnegative
Integer
Subtraction
Negation
Interval
Join
Interval
Meet
Interval
One
Interval
Reverse
Interval
Zero
Is
Contractible
Is
Equivalence
Isomorphism
Equivalence
Is
Set
Join
Associativity
Join
Empty
Right
Left
Injection
Length
Join
Length
Map
Length
Reverse
Less
Equal
Addition
Less
Equal
Antisymmetry
Less
Equal
Decidable
Less
Equal
Predecessor
Less
Equal
Reflexivity
Less
Equal
Step
Less
Equal
Successor
Less
Equal
Totality
Less
Equal
Transitivity
Less
Equal
Zero
Less
Irreflexivity
List
Prepend
Lists
Map
Composition
Map
Join
Multiplication
Associativity
Multiplication
Cancellation
Multiplication
Commutativity
Multiplication
Distributivity
Left
Multiplication
Distributivity
Right
Multiplication
Monotonicity
Multiplication
One
Left
Multiplication
One
Right
Multiplication
Successor
Left
Multiplication
Successor
Right
Multiplication
Zero
Left
Multiplication
Zero
Right
Natural
Number
Equality
Decidable
Natural
Number
Predecessor
Natural
Number
Successor
Natural
Number
Zero
Naturals
Negation
Equivalence
Negation
Involution
Nonempty
Nonempty
Introduction
Not
Decidable
Option
Option
None
Option
Some
Or
Decidable
Or
Introduction
Left
Or
Introduction
Right
Pair
Path
Congruence
Path
Function
Extensionality
Path
Induction
Path
Symmetry
Path
Transitivity
Power
Addition
Power
One
Power
Successor
Power
Zero
Predecessor
Less
Equal
Propositional
Extensionality
Quotient
Induction
Quotient
Introduction
Quotient
Lift
Quotient
Soundness
Quotient
Type
Reverse
Join
Reverse
Reverse
Right
Injection
Set
Type
Theory
Environment
Subtraction
Self
Subtraction
Successor
Subtraction
Zero
Left
Subtraction
Zero
Right
Subtype
Subtype
Introduction
Successor
Injectivity
Successor
Not
Less
Equal
Zero
Successor
Not
Zero
Transport
Transport
Constant
True
Introduction
Typed
Implicit
Type
Theory
Axiom
Type
Theory
Check
Type
Theory
Cubical
Type
Theory
Definition
Type
Theory
Environment
Type
Theory
Inductive
Type
Type
Theory
Natural
Numbers
Type
Theory
Proof
Type
Theory
Quotients
Type
Theory
Rewrite
Rule
Type
Theory
Rules
Type
Theory
Tactic
Type
Theory
Term
Type
Theory
Theorem
Type
Theory
Translate
Type
Universe
Univalence
Univalence
Computation
Universe
Not
Set
Weak
Head
Normal
Form
$Type
Theory
Environment