Conventions:
A rule is written [conclusion] >> [premise] ... [premise].
When a rule has no premises, the >> is omitted.
The variables a metavariable may depend on is the intersection of the variables in scope in each of its appearances.
The argument n is the length of the context G2, in rules where
G2 appears.
Omitted extracts in the conclusion are taken to be (). Omitted
extracts in premises are unused.
Note that no effort was made to keep the set of rules minimal. Many rules that would follow from other rules are nonetheless included for the sake of convenience or performance. Since the rules are (nearly) all verified, there is no robustness advantage to minimizing the set of rules.
Rules are given here in human-readable format, using explicit variables. The official rules, using de Bruijn indices, are given here.
Structural
Reduction
Dependent functions
Functions
T-Functions
K-Functions
Intersection types
Guarded types
Strong sums
Products
Semi-dependent products
Union types
Couarded types
Disjoint sums
Future modality
Recursive types
Inductive types
Void
Unit
Bool
Natural numbers
Universes
Kinds
Levels
Equality
Typing
Type equality
Type formation
Subtyping
Subset types
Intensional subset types
Squash
Intensional squash
Quotient types
Impredicative universals
Impredicative polymorphism
Impredicative existentials
Miscellaneous
Syntactic equality
Partial types
Let hypotheses
Integers
Rewriting
hypothesis n
G1, x : A, G2 |- A ext x
hypothesisOf n
G1, x : A, G2 |- x : A
hypothesisEq n
G1, x : A, G2 |- x = x : A
hypothesisOfTp n
G1, x : type, G2 |- x : type
hypothesisEqTp n
G1, x : type, G2 |- x = x : type
weaken m n
G1, G2, G3 |- A ext M
>>
G1, G3 |- A ext M
(where m = length(G3) and n = length(G2))
exchange l m n
G1, G2, G3, G4 |- A ext M
>>
G1, G3, G2, G4 |- A ext M
(where l = length(G4), m = length(G3), n = length(G2))
reduce red
G |- C ext M
>>
G |- D ext M
(where red reduces C to D)
unreduce C red
G |- D ext M
>>
G |- C ext M
(where red reduces C to D)
reduceAt i C M red
G |- [M / x]C ext P
>>
G |- [N / x]C ext P
(where red reduces M to N, x is the ith variable in C's scope)
unreduceAt i C M red
G |- [N / x]C ext P
>>
G |- [M / x]C ext P
(where red reduces M to N, x is the ith variable in C's scope)
reduceHyp n red
G1, y : C, G2 |- C ext M
>>
G1, y : D, G2 |- C ext M
(where red reduces C to D)
unreduceHyp n C red
G1, y : D, G2 |- C ext M
>>
G1, y : C, G2 |- C ext M
(where red reduces C to D)
reduceHypAt n i H M red
G1, y : [M / x]H, G2 |- C ext P
>>
G1, y : [N / x]H, G2 |- C ext P
(where red reduces M to N, x is the ith variable in H's scope)
unreduceHypAt n i H M red
G1, y : [N / x]H, G2 |- C ext P
>>
G1, y : [M / x]H, G2 |- C ext P
(where red reduces M to N, x is the ith variable in H's scope)
whnfHardConcl
G |- C ext M
>>
G |- D ext M
(where the hard weak-head normal form of C is D)
whnfHardHyp n
G1, x : H, G2 |- C ext M
>>
G1, x : H', G2 |- C ext M
(where the hard weak-head normal form of H is H')
normalizeConcl
G |- C ext M
>>
G |- D ext M
(where the normal form of C is D)
normalizeHyp n
G1, x : H, G2 |- C ext M
>>
G1, x : H', G2 |- C ext M
(where the normal form of H is H')
forallForm A B
G |- (forall (x : A) . B) : type
>>
G |- A : type
G, x : A |- B : type
forallEq A A' B B'
G |- (forall (x : A) . B) = (forall (x : A') . B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
forallFormUniv A B I
G |- (forall (x : A) . B) : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
forallEqUniv A A' B B' I
G |- (forall (x : A) . B) = (forall (x : A') . B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
forallSub A A' B B'
G |- (forall (x : A) . B) <: (forall (x : A') . B')
>>
G |- A' <: A
G, x : A' |- B <: B'
G, x : A |- B : type
forallIntroOf A B M
G |- (fn x . M) : forall (x : A) . B
>>
G |- A : type
G, x : A |- M : B
forallIntroEq A B M N
G |- (fn x . M) = (fn x . N) : (forall (x : A) . B)
>>
G |- A : type
G, x : A |- M = N : B
forallIntro A B
G |- forall (x : A) . B ext fn x . M
>>
G |- A : type
G, x : A |- B ext M
forallElimOf A B M P
G |- M P : [P / x]B
>>
G |- M : forall (x : A) . B
G |- P : A
forallElimEq A B M N P Q
G |- M P = N Q : [P / x]B
>>
G |- M = N : (forall (x : A) . B)
G |- P = Q : A
forallElim A B P
G |- [P / x]B ext M P
>>
G |- forall (x : A) . B ext M
G |- P : A
forallEta A B M
G |- M = (fn x . M x) : (forall (x : A) . B)
>>
G |- M : forall (x : A) . B
forallExt A B M N
G |- M = N : (forall (x : A) . B)
>>
G |- M : forall (x : A) . B
G |- N : forall (x : A) . B
G, x : A |- M x = N x : B
forallExt' A A' A'' B B' B'' M N
G |- M = N : (forall (x : A) . B)
>>
G |- A : type
G |- M : forall (x : A') . B'
G |- N : forall (x : A'') . B''
G, x : A |- M x = N x : B
forallOfExt A A' B B' M
G |- M : forall (x : A) . B
>>
G |- A : type
G |- M : forall (x : A') . B'
G, x : A |- M x : B
forallFormInv1 A B
G |- A : type
>>
G |- (forall (x : A) . B) : type
forallFormInv2 A B M
G |- [M / x]B : type
>>
G |- (forall (x : A) . B) : type
G |- M : A
arrowForm A B
G |- (A -> B) : type
>>
G |- A : type
G, x : A |- B : type
arrowEq A A' B B'
G |- (A -> B) = (A' -> B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
arrowFormUniv A B I
G |- (A -> B) : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
arrowEqUniv A A' B B' I
G |- (A -> B) = (A' -> B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
arrowForallEq A A' B B'
G |- (A -> B) = (forall (x : A') . B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
arrowForallEqUniv A A' B B' I
G |- (A -> B) = (forall (x : A') . B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
arrowSub A A' B B'
G |- (A -> B) <: (A' -> B')
>>
G |- A' <: A
G |- B <: B'
arrowForallSub A A' B B'
G |- (A -> B) <: (forall (x : A') . B')
>>
G |- A' <: A
G, x : A' |- B <: B'
G |- B : type
forallArrowSub A A' B B'
G |- (forall (x : A) . B) <: (A' -> B')
>>
G |- A' <: A
G, x : A' |- B <: B'
G, x : A |- B : type
arrowIntroOf A B M
G |- (fn x . M) : A -> B
>>
G |- A : type
G, x : A |- M : B
arrowIntroEq A B M N
G |- (fn x . M) = (fn x . N) : (A -> B)
>>
G |- A : type
G, x : A |- M = N : B
arrowIntro A B
G |- A -> B ext fn x . M
>>
G |- A : type
G, x : A |- B ext M
arrowElimOf A B M P
G |- M P : B
>>
G |- M : A -> B
G |- P : A
arrowElimEq A B M N P Q
G |- M P = N Q : B
>>
G |- M = N : (A -> B)
G |- P = Q : A
arrowElim A B
G |- B ext M P
>>
G |- A -> B ext M
G |- A ext P
arrowEta A B M
G |- M = (fn x . M x) : (A -> B)
>>
G |- M : A -> B
arrowExt A B M N
G |- M = N : (A -> B)
>>
G |- M : A -> B
G |- N : A -> B
G, x : A |- M x = N x : B
arrowExt' A A' A'' B B' B'' M N
G |- M = N : (A -> B)
>>
G |- A : type
G |- M : forall (x : A') . B'
G |- N : forall (x : A'') . B''
G, x : A |- M x = N x : B
arrowOfExt A A' B B' M
G |- M : A -> B
>>
G |- A : type
G |- M : forall (x : A') . B'
G, x : A |- M x : B
arrowFormInv1 A B
G |- A : type
>>
G |- (A -> B) : type
arrowFormInv2 A B M
G |- B : type
>>
G |- (A -> B) : type
G |- M : A
tarrowKind A I K
G |- (A -t> K) : kind I
>>
G |- A : univ I
G |- K : kind I
tarrowKindEq A A' I K K'
G |- (A -t> K) = (A' -t> K') : kind I
>>
G |- A = A' : univ I
G |- K = K' : kind I
tarrowForm A B
G |- (A -t> B) : type
>>
G |- A : type
G |- B : type
tarrowEq A A' B B'
G |- (A -t> B) = (A' -t> B') : type
>>
G |- A = A' : type
G |- B = B' : type
tarrowFormUniv A B I
G |- (A -t> B) : univ I
>>
G |- A : univ I
G |- B : univ I
tarrowEqUniv A A' B B' I
G |- (A -t> B) = (A' -t> B') : univ I
>>
G |- A = A' : univ I
G |- B = B' : univ I
tarrowArrowEq A A' B B'
G |- (A -t> B) = (A' -> B') : type
>>
G |- A = A' : type
G |- B = B' : type
tarrowArrowEqUniv A A' B B' I
G |- (A -t> B) = (A' -> B') : univ I
>>
G |- A = A' : univ I
G |- B = B' : univ I
tarrowForallEq A A' B B'
G |- (A -t> B) = (forall (x : A') . B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
G |- B : type
tarrowForallEqUniv A A' B B' I
G |- (A -t> B) = (forall (x : A') . B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
G |- B : univ I
tarrowIntroOf A B M
G |- (fn x . M) : A -t> B
>>
G |- A : type
G |- B : type
G, x : A |- M : B
tarrowIntroEq A B M N
G |- (fn x . M) = (fn x . N) : (A -t> B)
>>
G |- A : type
G |- B : type
G, x : A |- M = N : B
tarrowIntro A B
G |- A -t> B ext fn x . M
>>
G |- A : type
G |- B : type
G, x : A |- B ext M
tarrowElimOf A B M P
G |- M P : B
>>
G |- M : A -t> B
G |- P : A
tarrowElimEq A B M N P Q
G |- M P = N Q : B
>>
G |- M = N : (A -t> B)
G |- P = Q : A
tarrowElim A B
G |- B ext M P
>>
G |- A -t> B ext M
G |- A ext P
tarrowEta A B M
G |- M = (fn x . M x) : (A -t> B)
>>
G |- M : A -t> B
tarrowExt A B M N
G |- M = N : (A -t> B)
>>
G |- B : type
G |- M : A -t> B
G |- N : A -t> B
G, x : A |- M x = N x : B
tarrowOfExt A A' B B' M
G |- M : A -t> B
>>
G |- A : type
G |- B : type
G |- M : forall (x : A') . B'
G, x : A |- M x : B
karrowKind I K L
G |- (K -k> L) : kind I
>>
G |- K : kind I
G |- L : kind I
karrowKindEq I K K' L L'
G |- (K -k> L) = (K' -k> L') : kind I
>>
G |- K = K' : kind I
G |- L = L' : kind I
karrowForm A B
G |- (A -k> B) : type
>>
G |- A : type
G |- B : type
karrowEq A A' B B'
G |- (A -k> B) = (A' -k> B') : type
>>
G |- A = A' : type
G |- B = B' : type
karrowFormUniv A B I
G |- (A -k> B) : univ I
>>
G |- A : univ I
G |- B : univ I
karrowEqUniv A A' B B' I
G |- (A -k> B) = (A' -k> B') : univ I
>>
G |- A = A' : univ I
G |- B = B' : univ I
karrowArrowEq A A' B B'
G |- (A -k> B) = (A' -> B') : type
>>
G |- A = A' : type
G |- B = B' : type
karrowArrowEqUniv A A' B B' I
G |- (A -k> B) = (A' -> B') : univ I
>>
G |- A = A' : univ I
G |- B = B' : univ I
karrowForallEq A A' B B'
G |- (A -k> B) = (forall (x : A') . B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
G |- B : type
karrowForallEqUniv A A' B B' I
G |- (A -k> B) = (forall (x : A') . B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
G |- B : univ I
karrowIntroOf A B M
G |- (fn x . M) : A -k> B
>>
G |- A : type
G |- B : type
G, x : A |- M : B
karrowIntroEq A B M N
G |- (fn x . M) = (fn x . N) : (A -k> B)
>>
G |- A : type
G |- B : type
G, x : A |- M = N : B
karrowIntro A B
G |- A -k> B ext fn x . M
>>
G |- A : type
G |- B : type
G, x : A |- B ext M
karrowElimOf A B M P
G |- M P : B
>>
G |- M : A -k> B
G |- P : A
karrowElimEq A B M N P Q
G |- M P = N Q : B
>>
G |- M = N : (A -k> B)
G |- P = Q : A
karrowElim A B
G |- B ext M P
>>
G |- A -k> B ext M
G |- A ext P
karrowEta A B M
G |- M = (fn x . M x) : (A -k> B)
>>
G |- M : A -k> B
karrowExt A B M N
G |- M = N : (A -k> B)
>>
G |- B : type
G |- M : A -k> B
G |- N : A -k> B
G, x : A |- M x = N x : B
karrowOfExt A A' B B' M
G |- M : A -k> B
>>
G |- A : type
G |- B : type
G |- M : forall (x : A') . B'
G, x : A |- M x : B
intersectForm A B
G |- (intersect (x : A) . B) : type
>>
G |- A : type
G, x : A |- B : type
intersectEq A A' B B'
G |- (intersect (x : A) . B) = (intersect (x : A') . B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
intersectFormUniv A B I
G |- (intersect (x : A) . B) : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
intersectEqUniv A A' B B' I
G |- (intersect (x : A) . B) = (intersect (x : A') . B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
intersectSub A A' B B'
G |- (intersect (x : A) . B) <: (intersect (x : A') . B')
>>
G |- A' <: A
G, x : A' |- B <: B'
G, x : A |- B : type
intersectIntroOf A B M
G |- M : intersect (x : A) . B
>>
G |- A : type
G, x : A |- M : B
intersectIntroEq A B M N
G |- M = N : (intersect (x : A) . B)
>>
G |- A : type
G, x : A |- M = N : B
intersectIntro A B
G |- intersect (x : A) . B ext [() / x]M
>>
G |- A : type
G, x (hidden) : A |- B ext M
intersectElimOf A B M P
G |- M : [P / x]B
>>
G |- M : intersect (x : A) . B
G |- P : A
intersectElimEq A B M N P
G |- M = N : [P / x]B
>>
G |- M = N : (intersect (x : A) . B)
G |- P : A
intersectElim A B P
G |- [P / x]B ext M
>>
G |- intersect (x : A) . B ext M
G |- P : A
intersectFormInv1 A B
G |- A : type
>>
G |- (intersect (x : A) . B) : type
intersectFormInv2 A B M
G |- [M / x]B : type
>>
G |- (intersect (x : A) . B) : type
G |- M : A
guardForm A B
G |- (A -g> B) : type
>>
G |- A : type
G, x : A |- B : type
guardEq A A' B B'
G |- (A -g> B) = (A' -g> B') : type
>>
G |- iff A A'
G, x : A |- B = B' : type
guardFormUniv A B I
G |- (A -g> B) : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
guardEqUniv A A' B B' I
G |- (A -g> B) = (A' -g> B') : univ I
>>
G |- A : univ I
G |- A' : univ I
G |- iff A A'
G, x : A |- B = B' : univ I
guardIntroOf A B M
G |- M : A -g> B
>>
G |- A : type
G, x : A |- M : B
guardIntroEq A B M N
G |- M = N : (A -g> B)
>>
G |- A : type
G, x : A |- M = N : B
guardIntro A B
G |- A -g> B ext [() / x]M
>>
G |- A : type
G, x (hidden) : A |- B ext M
guardElimOf A B M
G |- M : B
>>
G |- M : A -g> B
G |- A
guardElimEq A B M N
G |- M = N : B
>>
G |- M = N : (A -g> B)
G |- A
guardElim A B
G |- B ext M
>>
G |- A -g> B ext M
G |- A
guardSatEq A B
G |- B = (A -g> B) : type
>>
G |- B : type
G |- A
guardSub A A' B B'
G |- (A -g> B) <: (A' -g> B')
>>
G |- A' -> A
G |- A : type
G, x : A' |- B <: B'
G, x : A |- B : type
guardSubIntro A B C
G |- C <: (A -g> B)
>>
G |- A : type
G, x : A |- C <: B
G |- C : type
existsForm A B
G |- (exists (x : A) . B) : type
>>
G |- A : type
G, x : A |- B : type
existsEq A A' B B'
G |- (exists (x : A) . B) = (exists (x : A') . B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
existsFormUniv A B I
G |- (exists (x : A) . B) : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
existsEqUniv A A' B B' I
G |- (exists (x : A) . B) = (exists (x : A') . B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
existsSub A A' B B'
G |- (exists (x : A) . B) <: (exists (x : A') . B')
>>
G |- A <: A'
G, x : A |- B <: B'
G, x : A' |- B' : type
existsIntroOf A B M N
G |- (M , N) : exists (x : A) . B
>>
G, x : A |- B : type
G |- M : A
G |- N : [M / x]B
existsIntroEq A B M M' N N'
G |- (M , N) = (M' , N') : (exists (x : A) . B)
>>
G, x : A |- B : type
G |- M = M' : A
G |- N = N' : [M / x]B
existsIntro A B M
G |- exists (x : A) . B ext (M , N)
>>
G, x : A |- B : type
G |- M : A
G |- [M / x]B ext N
existsElim1Of A B M
G |- M #1 : A
>>
G |- M : exists (x : A) . B
existsElim1Eq A B M N
G |- M #1 = N #1 : A
>>
G |- M = N : (exists (x : A) . B)
existsElim1 A B
G |- A ext M #1
>>
G |- exists (x : A) . B ext M
existsElim2Of A B M
G |- M #2 : [M #1 / x]B
>>
G |- M : exists (x : A) . B
existsElim2Eq A B M N
G |- M #2 = N #2 : [M #1 / x]B
>>
G |- M = N : (exists (x : A) . B)
existsEta A B M
G |- M = (M #1 , M #2) : (exists (x : A) . B)
>>
G |- M : exists (x : A) . B
existsExt A B M N
G |- M = N : (exists (x : A) . B)
>>
G |- M : exists (x : A) . B
G |- N : exists (x : A) . B
G |- M #1 = N #1 : A
G |- M #2 = N #2 : [M #1 / x]B
existsLeft n A B C
G1, x : (exists (y : A) . B), G2 |- C ext [x #1, x #2 / y, z]M
>>
G1, y : A, z : B, [(y , z) / x]G2 |- [(y , z) / x]C ext M
existsFormInv1 A B
G |- A : type
>>
G |- (exists (x : A) . B) : type
existsFormInv2 A B M
G |- [M / x]B : type
>>
G |- (exists (x : A) . B) : type
G |- M : A
existsFormInv2Eq A B M N
G |- [M / x]B = [N / x]B : type
>>
G |- (exists (x : A) . B) : type
G |- M = N : A
prodKind I K L
G |- K & L : kind I
>>
G |- K : kind I
G |- L : kind I
prodKindEq I K K' L L'
G |- (K & L) = (K' & L') : kind I
>>
G |- K = K' : kind I
G |- L = L' : kind I
prodForm A B
G |- A & B : type
>>
G |- A : type
G |- B : type
prodEq A A' B B'
G |- (A & B) = (A' & B') : type
>>
G |- A = A' : type
G |- B = B' : type
prodFormUniv A B I
G |- A & B : univ I
>>
G |- A : univ I
G |- B : univ I
prodEqUniv A A' B B' I
G |- (A & B) = (A' & B') : univ I
>>
G |- A = A' : univ I
G |- B = B' : univ I
prodExistsEq A A' B B'
G |- (A & B) = (exists (x : A') . B') : type
>>
G |- A = A' : type
G |- B = B' : type
prodExistsEqUniv A A' B B' I
G |- (A & B) = (exists (x : A') . B') : univ I
>>
G |- A = A' : univ I
G |- B = B' : univ I
prodSub A A' B B'
G |- (A & B) <: (A' & B')
>>
G |- A <: A'
G |- B <: B'
prodExistsSub A A' B B'
G |- (A & B) <: (exists (x : A') . B')
>>
G |- A <: A'
G, x : A |- B <: B'
G |- B : type
G, x : A' |- B' : type
existsProdSub A A' B B'
G |- (exists (x : A) . B) <: (A' & B')
>>
G |- A <: A'
G, x : A |- B <: B'
G |- B' : type
prodIntroOf A B M N
G |- (M , N) : A & B
>>
G |- M : A
G |- N : B
prodIntroEq A B M M' N N'
G |- (M , N) = (M' , N') : (A & B)
>>
G |- M = M' : A
G |- N = N' : B
prodIntro A B
G |- A & B ext (M , N)
>>
G |- A ext M
G |- B ext N
prodElim1Of A B M
G |- M #1 : A
>>
G |- M : A & B
prodElim1Eq A B M N
G |- M #1 = N #1 : A
>>
G |- M = N : (A & B)
prodElim1 A B
G |- A ext M #1
>>
G |- A & B ext M
prodElim2Of A B M
G |- M #2 : B
>>
G |- M : A & B
prodElim2Eq A B M N
G |- M #2 = N #2 : B
>>
G |- M = N : (A & B)
prodElim2 A B
G |- B ext M #2
>>
G |- A & B ext M
prodEta A B M
G |- M = (M #1 , M #2) : (A & B)
>>
G |- M : A & B
prodExt A B M N
G |- M = N : (A & B)
>>
G |- M : A & B
G |- N : A & B
G |- M #1 = N #1 : A
G |- M #2 = N #2 : B
prodLeft n A B C
G1, x : (A & B), G2 |- C ext [x #1, x #2 / y, z]M
>>
G1, y : A, z : B, [(y , z) / x]G2 |- [(y , z) / x]C ext M
prodFormInv1 A B
G |- A : type
>>
G |- A & B : type
prodFormInv2 A B
G |- B : type
>>
G |- A & B : type
G |- A
dprodForm A B
G |- dprod A B : type
>>
G |- A : type
G, x : A |- B : type
dprodEq A A' B B'
G |- dprod A B = dprod A' B' : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
dprodFormUniv A B I
G |- dprod A B : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
dprodEqUniv A A' B B' I
G |- dprod A B = dprod A' B' : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
dprodExistsEq A A' B B'
G |- dprod A B = (exists (x : A') . B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
dprodExistsEqUniv A A' B B' I
G |- dprod A B = (exists (x : A') . B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
prodDprodEq A A' B B'
G |- (A & B) = dprod A' B' : type
>>
G |- A = A' : type
G |- B = B' : type
prodDprodEqUniv A A' B B' I
G |- (A & B) = dprod A' B' : univ I
>>
G |- A = A' : univ I
G |- B = B' : univ I
dprodSub A A' B B'
G |- dprod A B <: dprod A' B'
>>
G |- A <: A'
G, x : A |- B <: B'
G, x : A' |- B' : type
dprodExistsSub A A' B B'
G |- dprod A B <: (exists (x : A') . B')
>>
G |- A <: A'
G, x : A |- B <: B'
G, x : A' |- B' : type
existsDprodSub A A' B B'
G |- (exists (x : A) . B) <: dprod A' B'
>>
G |- A <: A'
G, x : A |- B <: B'
G, x : A' |- B' : type
dprodProdSub A A' B B'
G |- dprod A B <: (A' & B')
>>
G |- A <: A'
G, x : A |- B <: B'
G |- B' : type
prodDprodSub A A' B B'
G |- (A & B) <: dprod A' B'
>>
G |- A <: A'
G, x : A |- B <: B'
G |- B : type
G, x : A' |- B' : type
dprodIntroOf A B M N
G |- (M , N) : dprod A B
>>
G |- M : A
G |- N : B
dprodIntroEq A B M M' N N'
G |- (M , N) = (M' , N') : dprod A B
>>
G |- M = M' : A
G |- N = N' : B
dprodIntro A B
G |- dprod A B ext (M , N)
>>
G |- A ext M
G |- B ext N
dprodElim1Of A B M
G |- M #1 : A
>>
G |- M : dprod A B
dprodElim1Eq A B M N
G |- M #1 = N #1 : A
>>
G |- M = N : dprod A B
dprodElim1 A B
G |- A ext M #1
>>
G |- dprod A B ext M
dprodElim2Of A B M
G |- M #2 : B
>>
G |- M : dprod A B
dprodElim2Eq A B M N
G |- M #2 = N #2 : B
>>
G |- M = N : dprod A B
dprodElim2 A B
G |- B ext M #2
>>
G |- dprod A B ext M
dprodEta A B M
G |- M = (M #1 , M #2) : dprod A B
>>
G |- M : dprod A B
dprodExt A B M N
G |- M = N : dprod A B
>>
G |- M : dprod A B
G |- N : dprod A B
G |- M #1 = N #1 : A
G |- M #2 = N #2 : B
dprodLeft n A B C
G1, x : (dprod A B), G2 |- C ext [x #1, x #2 / y, z]M
>>
G1, y : A, z : B, [(y , z) / x]G2 |- [(y , z) / x]C ext M
dprodFormInv1 A B
G |- A : type
>>
G |- dprod A B : type
dprodFormInv2 A B M
G |- B : type
>>
G |- dprod A B : type
G |- M : A
unionForm A B
G |- (union (x : A) . B) : type
>>
G |- A : type
G, x : A |- B : type
unionEq A A' B B'
G |- (union (x : A) . B) = (union (x : A') . B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
unionFormUniv A B I
G |- (union (x : A) . B) : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
unionEqUniv A A' B B' I
G |- (union (x : A) . B) = (union (x : A') . B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
unionIntroOf A B M N
G |- N : union (x : A) . B
>>
G, x : A |- B : type
G |- M : A
G |- N : [M / x]B
unionSub A A' B B'
G |- (union (x : A) . B) <: (union (x : A') . B')
>>
G |- A <: A'
G, x : A |- B <: B'
G, x : A' |- B' : type
unionIntroEq A B M N N'
G |- N = N' : (union (x : A) . B)
>>
G, x : A |- B : type
G |- M : A
G |- N = N' : [M / x]B
unionIntro A B M
G |- union (x : A) . B ext N
>>
G, x : A |- B : type
G |- M : A
G |- [M / x]B ext N
unionElimOf A B C M P
G |- [M / y]P : C
>>
G, x : A, y : B |- P : C
G |- M : union (x : A) . B
unionElimEq A B C M N P Q
G |- [M / y]P = [N / y]Q : C
>>
G, x : A, y : B |- P = Q : C
G |- M = N : (union (x : A) . B)
unionElim A B C M
G |- C ext [(), M / x, y]P
>>
G, x (hidden) : A, y : B |- C ext P
G |- M : union (x : A) . B
unionElimOfDep A B C M P
G |- [M / y]P : [M / y]C
>>
G, x : A, y : B |- P : C
G |- M : union (x : A) . B
unionElimEqDep A B C M N P Q
G |- [M / y]P = [N / y]Q : [M / y]C
>>
G, x : A, y : B |- P = Q : C
G |- M = N : (union (x : A) . B)
unionElimDep A B C M
G |- [M / y]C ext [(), M / x, y]P
>>
G, x (hidden) : A, y : B |- C ext P
G |- M : union (x : A) . B
unionElimIstype A B C M
G |- [M / y]C : type
>>
G, x : A, y : B |- C : type
G |- M : union (x : A) . B
unionElimEqtype A B C D M N
G |- [M / y]C = [N / y]D : type
>>
G, x : A, y : B |- C = D : type
G |- M = N : (union (x : A) . B)
coguardForm A B
G |- A &g B : type
>>
G |- A : type
G, x : A |- B : type
coguardEq A A' B B'
G |- (A &g B) = (A' &g B') : type
>>
G |- iff A A'
G, x : A |- B = B' : type
coguardFormUniv A B I
G |- A &g B : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
coguardEqUniv A A' B B' I
G |- (A &g B) = (A' &g B') : univ I
>>
G |- A : univ I
G |- A' : univ I
G |- iff A A'
G, x : A |- B = B' : univ I
coguardIntroEq A B M N
G |- M = N : (A &g B)
>>
G |- A
G |- M = N : B
coguardIntroOf A B M
G |- M : A &g B
>>
G |- A
G |- M : B
coguardIntroOfSquash A B M
G |- M : A &g B
>>
G |- A : type
G |- {A}
G |- M : B
coguardIntro A B
G |- A &g B ext M
>>
G |- A
G |- B ext M
coguardElim1 A B
G |- {A}
>>
G |- A : type
G |- A &g B
coguardElim2Eq A B M N
G |- M = N : B
>>
G |- M = N : (A &g B)
coguardElim2Of A B M
G |- M : B
>>
G |- M : A &g B
coguardElim2 A B
G |- B ext M
>>
G |- A &g B ext M
coguardLeft n A B C
G1, x : (A &g B), G2 |- C ext [() / y]M
>>
G1 |- A : type
G1, x : B, y (hidden) : A, G2 |- C ext M
coguardSatEq A B
G |- B = (A &g B) : type
>>
G |- B : type
G |- A
coguardSub A A' B B'
G |- (A &g B) <: (A' &g B')
>>
G |- A -> A'
G |- A' : type
G, x : A |- B <: B'
G, x : A' |- B' : type
coguardSubElim A B C
G |- (A &g B) <: C
>>
G |- A : type
G, x : A |- B <: C
G |- C : type
sumForm A B
G |- A % B : type
>>
G |- A : type
G |- B : type
sumEq A A' B B'
G |- (A % B) = (A' % B') : type
>>
G |- A = A' : type
G |- B = B' : type
sumFormUniv A B I
G |- A % B : univ I
>>
G |- A : univ I
G |- B : univ I
sumEqUniv A A' B B' I
G |- (A % B) = (A' % B') : univ I
>>
G |- A = A' : univ I
G |- B = B' : univ I
sumSub A A' B B'
G |- (A % B) <: (A' % B')
>>
G |- A <: A'
G |- B <: B'
sumIntro1Of A B M
G |- inl M : A % B
>>
G |- B : type
G |- M : A
sumIntro1Eq A B M N
G |- inl M = inl N : (A % B)
>>
G |- B : type
G |- M = N : A
sumIntro1 A B
G |- A % B ext inl M
>>
G |- B : type
G |- A ext M
sumIntro2Of A B M
G |- inr M : A % B
>>
G |- A : type
G |- M : B
sumIntro2Eq A B M N
G |- inr M = inr N : (A % B)
>>
G |- A : type
G |- M = N : B
sumIntro2 A B
G |- A % B ext inr M
>>
G |- A : type
G |- B ext M
sumElimOf A B C M P R
G |- sum_case M (fn x . P) (fn x . R) : [M / y]C
>>
G |- M : A % B
G, x : A |- P : [inl x / y]C
G, x : B |- R : [inr x / y]C
sumElimOfNondep A B C M P R
G |- sum_case M (fn x . P) (fn x . R) : C
>>
G |- M : A % B
G, x : A |- P : C
G, x : B |- R : C
sumElimEq A B C M N P Q R S
G |- sum_case M (fn x . P) (fn x . R) = sum_case N (fn x . Q) (fn x . S) : [M / y]C
>>
G |- M = N : (A % B)
G, x : A |- P = Q : [inl x / y]C
G, x : B |- R = S : [inr x / y]C
sumElim A B C M
G |- [M / y]C ext sum_case M (fn x . P) (fn x . R)
>>
G |- M : A % B
G, x : A |- [inl x / y]C ext P
G, x : B |- [inr x / y]C ext R
sumElimNondep A B C
G |- C ext sum_case M (fn x . P) (fn x . R)
>>
G |- A % B ext M
G, x : A |- C ext P
G, x : B |- C ext R
sumElimIstype A B C E M
G |- sum_case M (fn x . C) (fn x . E) : type
>>
G |- M : A % B
G, x : A |- C : type
G, x : B |- E : type
sumElimEqtype A B C D E F M N
G |- sum_case M (fn x . C) (fn x . E) = sum_case N (fn x . D) (fn x . F) : type
>>
G |- M = N : (A % B)
G, x : A |- C = D : type
G, x : B |- E = F : type
sumLeft n A B C
G1, x : (A % B), G2 |- C ext sum_case x (fn y . M) (fn y . N)
>>
G1, y : A, [inl y / x]G2 |- [inl y / x]C ext M
G1, y : B, [inr y / x]G2 |- [inl r / x]C ext N
sumContradiction A B C M N
G |- C
>>
G |- inl M = inr N : (A % B)
sumInjection1 A B M N
G |- M = N : A
>>
G |- inl M = inl N : (A % B)
sumInjection2 A B M N
G |- M = N : B
>>
G |- inr M = inr N : (A % B)
sum_caseType
G |- sum_case : intersect (i : level) . intersect (a : univ i) . intersect (b : univ i) . intersect (c : univ i) . a % b -> (a -> c) -> (b -> c) -> c
sumFormInv1 A B
G |- A : type
>>
G |- A % B : type
sumFormInv2 A B
G |- B : type
>>
G |- A % B : type
futureKind I K
G |- future K : kind I
>>
G |- I : level
promote(G) |- K : kind I
futureKindEq I K L
G |- future K = future L : kind I
>>
G |- I : level
promote(G) |- K = L : kind I
futureForm A
G |- future A : type
>>
promote(G) |- A : type
futureEq A B
G |- future A = future B : type
>>
promote(G) |- A = B : type
futureFormUniv A I
G |- future A : univ I
>>
G |- I : level
promote(G) |- A : univ I
futureEqUniv A B I
G |- future A = future B : univ I
>>
G |- I : level
promote(G) |- A = B : univ I
futureSub A B
G |- future A <: future B
>>
promote(G) |- A <: B
futureIntroOf A M
G |- next M : future A
>>
promote(G) |- M : A
futureIntroEq A M N
G |- next M = next N : future A
>>
promote(G) |- M = N : A
futureIntro A
G |- future A ext next M
>>
promote(G) |- A ext M
futureElimOf A B M P
G |- [M #prev / x]P : [M #prev / x]B
>>
promote(G) |- A : type
G |- M : future A
G, x (later) : A |- P : B
futureElimOfLetnext A B M P
G |- letnext M (fn x . P) : [M #prev / x]B
>>
promote(G) |- A : type
G |- M : future A
G, x (later) : A |- P : B
futureElimOfLetnextNondep A B M P
G |- letnext M (fn x . P) : B
>>
promote(G) |- A : type
G |- M : future A
G, x (later) : A |- P : B
futureElimEq A B M N P Q
G |- [M #prev / x]P = [N #prev / x]Q : [M #prev / x]B
>>
promote(G) |- A : type
G |- M = N : future A
G, x (later) : A |- P = Q : B
futureElim A B M
G |- [M #prev / x]B ext [M #prev / x]P
>>
promote(G) |- A : type
G |- M : future A
G, x (later) : A |- B ext P
futureElimIstype A B M
G |- [M #prev / x]B : type
>>
promote(G) |- A : type
G |- M : future A
G, x (later) : A |- B : type
futureElimIstypeLetnext A B M
G |- letnext M (fn x . B) : type
>>
promote(G) |- A : type
G |- M : future A
G, x (later) : A |- B : type
futureElimEqtype A B C M N
G |- [M #prev / x]B = [N #prev / x]C : type
>>
promote(G) |- A : type
G |- M = N : future A
G, x (later) : A |- B = C : type
futureEta A M
G |- M = next (M #prev) : future A
>>
G |- M : future A
futureExt A M N
G |- M = N : future A
>>
G |- M : future A
G |- N : future A
promote(G) |- M #prev = N #prev : A
futureLeft n A B
G1, x : (future A), G2 |- B ext [x #prev / y]M
>>
promote(G1) |- A : type
G1, y (later) : A, [next y / x]G2 |- [next y / x]B ext M
futureInjection A M N
G |- future (M = N : A) ext next ()
>>
promote(G) |- A : type
G |- next M = next N : future A
recKind I K
G |- (rec x . K) : kind I
>>
G |- I : level
G, x (later) : (kind I) |- K : kind I
recKindEq I K L
G |- (rec x . K) = (rec x . L) : kind I
>>
G |- I : level
G, x (later) : (kind I) |- K = L : kind I
recForm A
G |- (rec x . A) : type
>>
G, x (later) : type |- A : type
recEq A B
G |- (rec x . A) = (rec x . B) : type
>>
G, x (later) : type |- A = B : type
recFormUniv A I
G |- (rec x . A) : univ I
>>
G |- I : level
G, x (later) : (univ I) |- A : univ I
recEqUniv A B I
G |- (rec x . A) = (rec x . B) : univ I
>>
G |- I : level
G, x (later) : (univ I) |- A = B : univ I
recUnroll A
G |- (rec x . A) = [rec x . A / x]A : type
>>
G, x (later) : type |- A : type
recUnrollUniv A I
G |- (rec x . A) = [rec x . A / x]A : univ I
>>
G |- I : level
G, x (later) : (univ I) |- A : univ I
recBisimilar A B
G |- B = (rec x . A) : type
>>
G, x (later) : type |- A : type
G |- B = [B / x]A : type
muForm A
G |- (mu t . A) : type
>>
G, t : type |- A : type
G |- positive (fn t . A)
muEq A B
G |- (mu t . A) = (mu t . B) : type
>>
G, t : type |- A = B : type
G |- positive (fn t . A)
G |- positive (fn t . B)
muFormUniv A I
G |- (mu t . A) : univ I
>>
G |- I : level
G, t : (univ I) |- A : univ I
G |- positive (fn t . A)
muEqUniv A B I
G |- (mu t . A) = (mu t . B) : univ I
>>
G |- I : level
G, t : (univ I) |- A = B : univ I
G |- positive (fn t . A)
G |- positive (fn t . B)
muUnroll A
G |- eeqtp (mu t . A) [mu t . A / t]A ext (() , ())
>>
G, t : type |- A : type
G |- positive (fn t . A)
muUnrollUniv A I
G |- eeqtp (mu t . A) [mu t . A / t]A ext (() , ())
>>
G |- I : level
G, t : (univ I) |- A : univ I
G |- positive (fn t . A)
muInd A B M
G |- [M / w]B ext fix (fn z . fn x . [(), () / y, t']N) M
>>
G, t : type |- A : type
G |- positive (fn t . A)
G, t' (hidden) : type, x : [t' / t]A, y : (t' <: (mu t'' . [t'' / t]A)), z : (forall (w : t') . B) |- [x / w]B ext N
G |- M : mu t . A
muIndUniv A B I M
G |- [M / w]B ext fix (fn z . fn x . [(), () / y, t']N #1) M
>>
G |- I : level
G, t : (univ I) |- A : univ I
G |- positive (fn t . A)
G, t' (hidden) : (univ I), x : [t' / t]A, y : (t' <: (mu t'' . [t'' / t]A)), z : (forall (w : t') . B) |- [x / w]B & ([x / w]B : univ I) ext N
G |- M : mu t . A
checkPositive
Proves valid goals of the form:
G |- positive (fn t . A)
checkNegative
Proves valid goals of the form:
G |- negative (fn t . A)
voidForm
G |- void : type
voidEq
G |- void = void : type
voidFormUniv I
G |- void : univ I
>>
G |- I : level
voidEqUniv I
G |- void = void : univ I
>>
G |- I : level
voidElim A
G |- A
>>
G |- void
voidSub A
G |- void <: A
>>
G |- A : type
abortType
G |- abort : intersect (i : level) . intersect (a : univ i) . void -> a
unitKind I
G |- unit : kind I
>>
G |- I : level
unitKindEq I
G |- unit = unit : kind I
>>
G |- I : level
unitForm
G |- unit : type
unitEq
G |- unit = unit : type
unitFormUniv I
G |- unit : univ I
>>
G |- I : level
unitEqUniv I
G |- unit = unit : univ I
>>
G |- I : level
unitIntroOf
G |- () : unit
unitIntro
G |- unit
unitExt M N
G |- M = N : unit
>>
G |- M : unit
G |- N : unit
unitLeft n B
G1, x : unit, G2 |- B ext M
>>
G1, [() / x]G2 |- [() / x]B ext M
boolForm
G |- bool : type
boolEq
G |- bool = bool : type
boolFormUniv I
G |- bool : univ I
>>
G |- I : level
boolEqUniv I
G |- bool = bool : univ I
>>
G |- I : level
boolIntro1Of
G |- true : bool
boolIntro2Of
G |- false : bool
boolElimOf A M P R
G |- ite M P R : [M / x]A
>>
G |- M : bool
G |- P : [true / x]A
G |- R : [false / x]A
boolElimOfNondep A M P R
G |- ite M P R : A
>>
G |- M : bool
G |- P : A
G |- R : A
boolElimEq A M N P Q R S
G |- ite M P R = ite N Q S : [M / x]A
>>
G |- M = N : bool
G |- P = Q : [true / x]A
G |- R = S : [false / x]A
boolElim A M
G |- [M / x]A ext ite M P R
>>
G |- M : bool
G |- [true / x]A ext P
G |- [false / x]A ext R
boolElimIstype A C M
G |- ite M A C : type
>>
G |- M : bool
G |- A : type
G |- C : type
boolElimEqtype A B C D M N
G |- ite M A C = ite N B D : type
>>
G |- M = N : bool
G |- A = B : type
G |- C = D : type
boolLeft n A
G1, x : bool, G2 |- A ext ite x M N
>>
G1, [true / x]G2 |- [true / x]A ext M
G1, [false / x]G2 |- [false / x]A ext N
boolContradiction A
G |- A
>>
G |- true = false : bool
iteType
G |- ite : intersect (i : level) . intersect (a : univ i) . bool -> a -> a -> a
natForm
G |- nat : type
natEq
G |- nat = nat : type
natFormUniv I
G |- nat : univ I
>>
G |- I : level
natEqUniv I
G |- nat = nat : univ I
>>
G |- I : level
natElimEq A M N P Q R S
G |- natcase M P (fn x . R) = natcase N Q (fn x . S) : [M / y]A
>>
G |- M = N : nat
G |- P = Q : [zero / y]A
G, x : nat |- R = S : [succ x / y]A
natElimEqtype A B C D M N
G |- natcase M A (fn x . C) = natcase N B (fn x . D) : type
>>
G |- M = N : nat
G |- A = B : type
G, x : nat |- C = D : type
natUnroll
G |- eeqtp nat (unit % nat) ext (() , ())
natContradiction A M
G |- A
>>
G |- zero = succ M : nat
natInjection M N
G |- M = N : nat
>>
G |- succ M = succ N : nat
zeroType
G |- zero : nat
succType
G |- succ : nat -> nat
univKind I J
G |- univ J : kind I
>>
G |- J = I : level
univKindEq I J K
G |- univ J = univ K : kind I
>>
G |- J = K : level
G |- J = I : level
univForm I
G |- univ I : type
>>
G |- I : level
univEq I J
G |- univ I = univ J : type
>>
G |- I = J : level
univFormUniv I J
G |- univ J : univ I
>>
G |- lsucc J <l= I
univFormUnivSucc I
G |- univ I : univ (lsucc I)
>>
G |- I : level
univEqUniv I J K
G |- univ J = univ K : univ I
>>
G |- J = K : level
G |- lsucc J <l= I
univCumulativeOf A I J
G |- A : univ J
>>
G |- A : univ I
G |- I <l= J
univCumulativeEq A B I J
G |- A = B : univ J
>>
G |- A = B : univ I
G |- I <l= J
univCumulativeSuccOf A I
G |- A : univ (lsucc I)
>>
G |- A : univ I
univSub I J
G |- univ I <: univ J
>>
G |- I <l= J
univForgetOf A I
G |- A : type
>>
G |- A : univ I
univForgetEq A B I
G |- A = B : type
>>
G |- A = B : univ I
univIntroEqtype A B I
G |- A = B : univ I
>>
G |- A = B : type
G |- A : univ I
G |- B : univ I
univFormInv I
G |- I : level
>>
G |- univ I : type
kindForm I
G |- kind I : type
>>
G |- I : level
kindEq I J
G |- kind I = kind J : type
>>
G |- I = J : level
kindFormUniv I K
G |- kind I : univ K
>>
G |- lsucc (lsucc I) <l= K
kindEqUniv I J K
G |- kind I = kind J : univ K
>>
G |- I = J : level
G |- lsucc (lsucc I) <l= K
kindForgetOf A I
G |- A : univ (lsucc I)
>>
G |- A : kind I
kindForgetEq A B I
G |- A = B : univ (lsucc I)
>>
G |- A = B : kind I
kindUnivSub I J
G |- kind I <: univ J
>>
G |- lsucc I <l= J
levelForm
G |- level : type
levelEq
G |- level = level : type
levelFormUniv I
G |- level : univ I
>>
G |- I : level
levelEqUniv I
G |- level = level : univ I
>>
G |- I : level
lleqForm I J
G |- I <l= J : type
>>
G |- I : level
G |- J : level
lleqEq I I' J J'
G |- (I <l= J) = (I' <l= J') : type
>>
G |- I = I' : level
G |- J = J' : level
lleqFormUniv I J K
G |- I <l= J : univ K
>>
G |- I : level
G |- J : level
G |- K : level
lleqEqUniv I I' J J' K
G |- (I <l= J) = (I' <l= J') : univ K
>>
G |- I = I' : level
G |- J = J' : level
G |- K : level
lzeroLevel
G |- lzero : level
lsuccLevel M
G |- lsucc M : level
>>
G |- M : level
lsuccEq M N
G |- lsucc M = lsucc N : level
>>
G |- M = N : level
lmaxLevel M N
G |- lmax M N : level
>>
G |- M : level
G |- N : level
lmaxEq M M' N N'
G |- lmax M N = lmax M' N' : level
>>
G |- M = M' : level
G |- N = N' : level
lleqRefl M
G |- M <l= M
>>
G |- M : level
lleqTrans M N P
G |- M <l= P
>>
G |- M <l= N
G |- N <l= P
lleqZero M
G |- lzero <l= M
>>
G |- M : level
lleqSucc M N
G |- lsucc M <l= lsucc N
>>
G |- M <l= N
lleqIncrease M N
G |- M <l= lsucc N
>>
G |- M <l= N
lleqMaxL M N P
G |- lmax M N <l= P
>>
G |- M <l= P
G |- N <l= P
lleqMaxR1 M N P
G |- M <l= lmax N P
>>
G |- M <l= N
G |- P : level
lleqMaxR2 M N P
G |- M <l= lmax N P
>>
G |- M <l= P
G |- N : level
lleqResp M M' N N'
G |- M <l= N
>>
G |- M' = M : level
G |- N' = N : level
G |- M' <l= N'
lsuccMaxDistTrans M N P
G |- M = lsucc (lmax N P) : level
>>
G |- M = lmax (lsucc N) (lsucc P) : level
lzeroType
G |- lzero : level
lsuccType
G |- lsucc : level -> level
lmaxType
G |- lmax : level -> level -> level
eqForm A M P
G |- M = P : A : type
>>
G |- M : A
G |- P : A
eqEq A B M N P Q
G |- (M = P : A) = (N = Q : B) : type
>>
G |- A = B : type
G |- M = N : A
G |- P = Q : A
eqFormUniv A I M P
G |- M = P : A : univ I
>>
G |- A : univ I
G |- M : A
G |- P : A
eqEqUniv A B I M N P Q
G |- (M = P : A) = (N = Q : B) : univ I
>>
G |- A = B : univ I
G |- M = N : A
G |- P = Q : A
eqIntro A M N
G |- () : M = N : A
>>
G |- M = N : A
eqElim A M N P
G |- M = N : A
>>
G |- P : M = N : A
eqTrivialize A M N
G |- M = N : A
>>
G |- M = N : A
eqExt A M N P Q
G |- P = Q : (M = N : A)
>>
G |- P : M = N : A
G |- Q : M = N : A
eqLeft n A B P Q
G1, x : (P = Q : A), G2 |- B ext M
>>
G1, [() / x]G2 |- [() / x]B ext M
eqRefl A M
G |- M = M : A
>>
G |- M : A
eqSymm A M N
G |- M = N : A
>>
G |- N = M : A
eqTrans A M N P
G |- M = P : A
>>
G |- M = N : A
G |- N = P : A
eqFormInv1 A M N
G |- A : type
>>
G |- M = N : A : type
eqFormInv2 A M N
G |- M : A
>>
G |- M = N : A : type
eqFormInv3 A M N
G |- N : A
>>
G |- M = N : A : type
ofForm A M
G |- (M : A) : type
>>
G |- M : A
ofEq A B M N
G |- (M : A) = (N : B) : type
>>
G |- A = B : type
G |- M = N : A
ofFormUniv A I M
G |- (M : A) : univ I
>>
G |- A : univ I
G |- M : A
ofEqUniv A B I M N
G |- (M : A) = (N : B) : univ I
>>
G |- A = B : univ I
G |- M = N : A
ofIntro A M
G |- () : M : A
>>
G |- M : A
ofElim A M P
G |- M : A
>>
G |- P : M : A
ofTrivialize A M
G |- M : A
>>
G |- M : A
ofExt A M P Q
G |- P = Q : (M : A)
>>
G |- P : M : A
G |- Q : M : A
ofLeft n A B P
G1, x : (P : A), G2 |- B ext M
>>
G1, [() / x]G2 |- [() / x]B ext M
ofEquand1 A M N
G |- M : A
>>
G |- M = N : A
ofEquand2 A M N
G |- N : A
>>
G |- M = N : A
eqtpForm A B
G |- A = B : type : type
>>
G |- A : type
G |- B : type
eqtpEq A B C D
G |- (A = C : type) = (B = D : type) : type
>>
G |- A = B : type
G |- C = D : type
eqtpFormUniv A B I
G |- A = B : type : univ I
>>
G |- A : univ I
G |- B : univ I
eqtpEqUniv A B C D I
G |- (A = C : type) = (B = D : type) : univ I
>>
G |- A = B : univ I
G |- C = D : univ I
eqtpIntro A B
G |- () : A = B : type
>>
G |- A = B : type
eqtpElim A B P
G |- A = B : type
>>
G |- P : A = B : type
eqtpExt A B P Q
G |- P = Q : (A = B : type)
>>
G |- P : A = B : type
G |- Q : A = B : type
eqtpLeft n A B C
G1, x : (A = B : type), G2 |- C ext M
>>
G1, [() / x]G2 |- [() / x]C ext M
eqtpFunct A B M N
G |- [M / x]B = [N / x]B : type
>>
G, x : A |- B : type
G |- M = N : A
eqtpFunctType A B B'
G |- [B / x]A = [B' / x]A : type
>>
G, x : type |- A : type
G |- B = B' : type
equivalenceOf A B M
G |- M : B
>>
G |- A = B : type
G |- M : A
equivalenceEq A B M N
G |- M = N : B
>>
G |- A = B : type
G |- M = N : A
equivalence A B
G |- B ext M
>>
G |- A = B : type
G |- A ext M
equivalenceLeft n A B C
G1, x : A, G2 |- C ext M
>>
G1, y : (A : type) |- A = B : type
G1, x : B, G2 |- C ext M
equivalenceLeftAlt n A B C
G1, x : A, G2 |- C ext M
>>
G1, x : A, G2 |- A = B : type
G1, x : B, G2 |- C ext M
eqtpRefl A
G |- A = A : type
>>
G |- A : type
eqtpSymm A B
G |- A = B : type
>>
G |- B = A : type
eqtpTrans A B C
G |- A = C : type
>>
G |- A = B : type
G |- B = C : type
istpForm A
G |- (A : type) : type
>>
G |- A : type
istpEq A B
G |- (A : type) = (B : type) : type
>>
G |- A = B : type
istpFormUniv A I
G |- (A : type) : univ I
>>
G |- A : univ I
istpEqUniv A B I
G |- (A : type) = (B : type) : univ I
>>
G |- A = B : univ I
istpIntro A
G |- () : A : type
>>
G |- A : type
istpElim A P
G |- A : type
>>
G |- P : A : type
istpExt A P Q
G |- P = Q : (A : type)
>>
G |- P : A : type
G |- Q : A : type
istpLeft n A B
G1, x : (A : type), G2 |- B ext M
>>
G1, [() / x]G2 |- [() / x]B ext M
inhabitedForm A
G |- A : type
>>
G |- A
subtypeForm A B
G |- A <: B : type
>>
G |- A : type
G |- B : type
subtypeEq A B C D
G |- (A <: C) = (B <: D) : type
>>
G |- A = B : type
G |- C = D : type
subtypeFormUniv A B I
G |- A <: B : univ I
>>
G |- A : univ I
G |- B : univ I
subtypeEqUniv A B C D I
G |- (A <: C) = (B <: D) : univ I
>>
G |- A = B : univ I
G |- C = D : univ I
subtypeIntro A B
G |- () : A <: B
>>
G |- A <: B
subtypeElim A B P
G |- A <: B
>>
G |- P : A <: B
subtypeExt A B P Q
G |- P = Q : (A <: B)
>>
G |- P : A <: B
G |- Q : A <: B
subtypeLeft n A B C
G1, x : (A <: B), G2 |- C ext M
>>
G1, [() / x]G2 |- [() / x]C ext M
subtypeEstablish A B
G |- A <: B
>>
G |- A : type
G |- B : type
G, x : A |- x : B
subsumptionOf A B M
G |- M : B
>>
G |- A <: B
G |- M : A
subsumptionEq A B M N
G |- M = N : B
>>
G |- A <: B
G |- M = N : A
subsumption A B
G |- B ext M
>>
G |- A <: B
G |- A ext M
subsumptionAlt A B
G |- B ext M
>>
G |- eeqtp B A
G |- A ext M
subsumptionLeft n A B C
G1, x : A, G2 |- C ext M
>>
G1, y : (A : type) |- eeqtp A B
G1, x : B, G2 |- C ext M
subsumptionLeftAlt n A B C
G1, x : A, G2 |- C ext M
>>
G1, x : A, G2 |- eeqtp A B
G1, x : B, G2 |- C ext M
subsumptionLast n A B C
G1, x : A, G2 |- C ext M
>>
G1, x : A |- A <: B
G1, x : B |- C ext M
subtypeRefl A
G |- A <: A
>>
G |- A : type
subtypeReflEqtype A B
G |- A <: B
>>
G |- A = B : type
subtypeTrans A B C
G |- A <: C
>>
G |- A <: B
G |- B <: C
subtypeIstp1 A B
G |- A : type
>>
G |- A <: B
subtypeIstp2 A B
G |- B : type
>>
G |- A <: B
eeqtpForm A B
G |- eeqtp A B : type
>>
G |- A : type
G |- B : type
eeqtpEq A B C D
G |- eeqtp A C = eeqtp B D : type
>>
G |- A = B : type
G |- C = D : type
eeqtpFormUniv A B I
G |- eeqtp A B : univ I
>>
G |- A : univ I
G |- B : univ I
eeqtpEqUniv A B C D I
G |- eeqtp A C = eeqtp B D : univ I
>>
G |- A = B : univ I
G |- C = D : univ I
setForm A B
G |- {x : A | B} : type
>>
G |- A : type
G, x : A |- B : type
setEq A A' B B'
G |- {x : A | B} = {x : A' | B'} : type
>>
G |- A = A' : type
G, x : A |- iff B B'
setFormUniv A B I
G |- {x : A | B} : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
setEqUniv A A' B B' I
G |- {x : A | B} = {x : A' | B'} : univ I
>>
G |- A = A' : univ I
G, x : A |- B : univ I
G, x : A |- B' : univ I
G, x : A |- iff B B'
setWeakenOf A B M
G |- M : A
>>
G |- M : {x : A | B}
setWeakenEq A B M N
G |- M = N : A
>>
G |- M = N : {x : A | B}
setWeaken A B
G |- A ext M
>>
G |- {x : A | B} ext M
setIntroOf A B M
G |- M : {x : A | B}
>>
G, x : A |- B : type
G |- M : A
G |- [M / x]B
setIntroEq A B M N
G |- M = N : {x : A | B}
>>
G, x : A |- B : type
G |- M = N : A
G |- [M / x]B
setIntro A B M
G |- {x : A | B} ext M
>>
G, x : A |- B : type
G |- M : A
G |- [M / x]B
setIntroOfSquash A B M
G |- M : {x : A | B}
>>
G, x : A |- B : type
G |- M : A
G |- {[M / x]B}
squashIntroOfSquash A
G |- () : {A}
>>
G |- A : type
G |- {A}
setElim A B C M
G |- C ext [() / y]N
>>
G, x : A |- B : type
G |- M : {x : A | B}
G, y (hidden) : [M / x]B |- C ext N
setLeft n A B C
G1, x : {x : A | B}, G2 |- C ext [() / y]M
>>
G1, x : A |- B : type
G1, x : A, y (hidden) : B, G2 |- C ext M
setSquash A B
G |- {x : A | B} = {x : A | {B}} : type
>>
G |- {x : A | B} : type
setFormInv A B
G |- A : type
>>
G |- {x : A | B} : type
setSubElim A A' B
G |- {x : A | B} <: A'
>>
G |- A <: A'
G, x : A |- B : type
isetForm A B
G |- iset A (fn x . B) : type
>>
G |- A : type
G, x : A |- B : type
isetEq A A' B B'
G |- iset A (fn x . B) = iset A' (fn x . B') : type
>>
G |- A = A' : type
G, x : A |- B = B' : type
isetFormUniv A B I
G |- iset A (fn x . B) : univ I
>>
G |- A : univ I
G, x : A |- B : univ I
isetEqUniv A A' B B' I
G |- iset A (fn x . B) = iset A' (fn x . B') : univ I
>>
G |- A = A' : univ I
G, x : A |- B = B' : univ I
isetWeakenOf A B M
G |- M : A
>>
G |- M : iset A (fn x . B)
isetWeakenEq A B M N
G |- M = N : A
>>
G |- M = N : iset A (fn x . B)
isetWeaken A B
G |- A ext M
>>
G |- iset A (fn x . B) ext M
isetIntroOf A B M
G |- M : iset A (fn x . B)
>>
G, x : A |- B : type
G |- M : A
G |- [M / x]B
isetIntroEq A B M N
G |- M = N : iset A (fn x . B)
>>
G, x : A |- B : type
G |- M = N : A
G |- [M / x]B
isetIntro A B M
G |- iset A (fn x . B) ext M
>>
G, x : A |- B : type
G |- M : A
G |- [M / x]B
isetIntroOfSquash A B M
G |- M : iset A (fn x . B)
>>
G, x : A |- B : type
G |- M : A
G |- {[M / x]B}
isetElim A B C M
G |- C ext [() / y]N
>>
G |- M : iset A (fn x . B)
G, y (hidden) : [M / x]B |- C ext N
isetLeft n A B C
G1, x : (iset A (fn x . B)), G2 |- C ext [() / y]M
>>
G1, x : A, y (hidden) : B, G2 |- C ext M
isetFormInv1 A B
G |- A : type
>>
G |- iset A (fn x . B) : type
isetFormInv2 A B M
G |- [M / x]B : type
>>
G |- iset A (fn x . B) : type
G |- M : A
isetSubElim A A' B
G |- iset A (fn x . B) <: A'
>>
G |- A <: A'
G, x : A |- B : type
squashForm A
G |- {A} : type
>>
G |- A : type
squashEq A B
G |- {A} = {B} : type
>>
G |- iff A B
squashFormUniv A I
G |- {A} : univ I
>>
G |- A : univ I
squashEqUniv A B I
G |- {A} = {B} : univ I
>>
G |- A : univ I
G |- B : univ I
G |- iff A B
squashIntroOf A
G |- () : {A}
>>
G |- A
squashIntro A
G |- {A}
>>
G |- A
squashElim A C M
G |- C ext [() / x]N
>>
G |- M : {A}
G |- A : type
G, x (hidden) : A |- C ext N
squashExt A M N
G |- M = N : {A}
>>
G |- M : {A}
G |- N : {A}
G |- A : type
squashLeft n A C
G1, x : {A}, G2 |- C ext [() / y]M
>>
G1 |- A : type
G1, y (hidden) : A, [() / x]G2 |- [() / x]C ext M
squashSub A B
G |- {A} <: {B}
>>
G |- B : type
G |- A -> B
isquashForm A
G |- isquash A : type
>>
G |- A : type
isquashEq A B
G |- isquash A = isquash B : type
>>
G |- A = B : type
isquashFormUniv A I
G |- isquash A : univ I
>>
G |- A : univ I
isquashEqUniv A B I
G |- isquash A = isquash B : univ I
>>
G |- A : univ I
G |- B : univ I
G |- A = B : univ I
isquashIntroOf A
G |- () : isquash A
>>
G |- A
isquashIntro A
G |- isquash A
>>
G |- A
isquashIntroOfIsquash A
G |- () : isquash A
>>
G |- isquash A
isquashElim A C M
G |- C ext [() / x]N
>>
G |- M : isquash A
G, x (hidden) : A |- C ext N
isquashExt A M N
G |- M = N : isquash A
>>
G |- M : isquash A
G |- N : isquash A
isquashLeft n A C
G1, x : (isquash A), G2 |- C ext [() / y]M
>>
G1, y (hidden) : A, [() / x]G2 |- [() / x]C ext M
isquashSub A B
G |- isquash A <: isquash B
>>
G |- B : type
G |- A -> B
isquashFormInv A
G |- A : type
>>
G |- isquash A : type
quotientForm A B
G |- (quotient (x y : A) . B) : type
>>
G |- A : type
G, x : A, y : A |- B : type
G, x' : A, y' : A, w : [x', y' / x, y]B |- [y', x' / x, y]B
G, x' : A, y' : A, z' : A, w : [x', y' / x, y]B, w' : [y', z' / x, y]B |- [x', z' / x, y]B
quotientEq A A' B B'
G |- (quotient (x y : A) . B) = (quotient (x y : A') . B') : type
>>
G |- A = A' : type
G, x : A, y : A |- B : type
G, x : A, y : A |- B' : type
G, x : A, y : A, w : B |- B'
G, x : A, y : A, w : B' |- B
G, x' : A, y' : A, w : [x', y' / x, y]B |- [y', x' / x, y]B
G, x' : A, y' : A, z' : A, w : [x', y' / x, y]B, w' : [y', z' / x, y]B |- [x', z' / x, y]B
quotientFormUniv A B I
G |- (quotient (x y : A) . B) : univ I
>>
G |- A : univ I
G, x : A, y : A |- B : univ I
G, x' : A, y' : A, w : [x', y' / x, y]B |- [y', x' / x, y]B
G, x' : A, y' : A, z' : A, w : [x', y' / x, y]B, w' : [y', z' / x, y]B |- [x', z' / x, y]B
quotientEqUniv A A' B B' I
G |- (quotient (x y : A) . B) = (quotient (x y : A') . B') : univ I
>>
G |- A = A' : univ I
G, x : A, y : A |- B : univ I
G, x : A, y : A |- B' : univ I
G, x : A, y : A, w : B |- B'
G, x : A, y : A, w : B' |- B
G, x' : A, y' : A, w : [x', y' / x, y]B |- [y', x' / x, y]B
G, x' : A, y' : A, z' : A, w : [x', y' / x, y]B, w' : [y', z' / x, y]B |- [x', z' / x, y]B
quotientIntroOf A B M
G |- M : quotient (x y : A) . B
>>
G |- (quotient (x y : A) . B) : type
G |- M : A
G |- [M, M / x, y]B
quotientIntroEq A B M N
G |- M = N : (quotient (x y : A) . B)
>>
G |- (quotient (x y : A) . B) : type
G |- M : A
G |- N : A
G |- [M, N / x, y]B
quotientElimOf A B C M P
G |- [M / z]P : [M / z]C
>>
G |- M : quotient (x y : A) . B
G, x : A, y : A |- B : type
G, z : (quotient (x y : A) . B) |- C : type
G, x : A, y : A, w : B |- [x / z]P = [y / z]P : [x / z]C
quotientElimEq A B C M N P Q
G |- [M / z]P = [N / z]Q : [M / z]C
>>
G |- M = N : (quotient (x y : A) . B)
G, x : A, y : A |- B : type
G, z : (quotient (x y : A) . B) |- C : type
G, x : A, y : A, w : B |- [x / z]P = [y / z]Q : [x / z]C
quotientElimIstype A B C M
G |- [M / z]C : type
>>
G |- M : quotient (x y : A) . B
G, x : A, y : A |- B : type
G, x : A, y : A, w : B |- [x / z]C = [y / z]C : type
quotientElimEqtype A B C D M N
G |- [M / z]C = [N / z]D : type
>>
G |- M = N : (quotient (x y : A) . B)
G, x : A, y : A |- B : type
G, x : A, y : A, w : B |- [x / z]C = [y / z]D : type
quotientDescent A B C M N
G |- C ext [() / z]P
>>
G, x : A, y : A |- B : type
G |- C : type
G |- M : A
G |- N : A
G |- M = N : (quotient (x y : A) . B)
G, z (hidden) : [M, N / x, y]B |- C ext P
quotientLeft n A B C
G1, z : (quotient (x y : A) . B), G2 |- C ext [() / z']M
>>
G1, z : (quotient (x y : A) . B), G2 |- C : type
G1, z' (hidden) : A, [z' / z]G2 |- [z' / z]C ext M
quotientLeftRefl n A B C
G1, z : (quotient (x y : A) . B), G2 |- C ext [(), () / v, w]M
>>
G1, x : A, y : A |- B : type
G1, z : (quotient (x y : A) . B), G2 |- C : type
G1, v (hidden) : A, w (hidden) : [v, v / x, y]B, [v / z]G2 |- [v / z]C ext M
quotientLeftIstype n A B C
G1, z : (quotient (x y : A) . B), G2 |- C : type
>>
G1, x : A, y : A |- B : type
G1, x : A, y : A, w : B, [x / z]G2 |- [x / z]C = [y / z]C : type
quotientLeftEqtype n A B C D
G1, z : (quotient (x y : A) . B), G2 |- C = D : type
>>
G1, x : A, y : A |- B : type
G1, x : A, y : A, w : B, [x / z]G2 |- [x / z]C = [y / z]D : type
quotientLeftOf n A B C M
G1, z : (quotient (x y : A) . B), G2 |- M : C
>>
G1, x : A, y : A |- B : type
G1, x : A, y : A, w : B, [x / z]G2 |- [x / z]M = [y / z]M : C
quotientLeftEq n A B C M N
G1, z : (quotient (x y : A) . B), G2 |- M = N : C
>>
G1, x : A, y : A |- B : type
G1, x : A, y : A, w : B, [x / z]G2 |- [x / z]M = [y / z]N : C
quotientLeftOfDep n A B C M
G1, z : (quotient (x y : A) . B), G2 |- M : C
>>
G1, x : A, y : A |- B : type
G1, x : A, y : A, w : B, [x / z]G2 |- [x / z]C = [y / z]C : type
G1, x : A, y : A, w : B, [x / z]G2 |- [x / z]M = [y / z]M : [x / z]C
quotientLeftEqDep n A B C M N
G1, z : (quotient (x y : A) . B), G2 |- M = N : C
>>
G1, x : A, y : A |- B : type
G1, x : A, y : A, w : B, [x / z]G2 |- [x / z]C = [y / z]C : type
G1, x : A, y : A, w : B, [x / z]G2 |- [x / z]M = [y / z]N : [x / z]C
quotientFormInv A B
G |- A : type
>>
G |- (quotient (x y : A) . B) : type
iforallForm A I K
G |- (iforall I (x : K) . A) : type
>>
G |- K : kind I
G, x : K |- A : type
iforallEq A B I K L
G |- (iforall I (x : K) . A) = (iforall I (x : L) . B) : type
>>
G |- K = L : kind I
G, x : K |- A = B : type
iforallFormUniv A I J K
G |- (iforall I (x : K) . A) : univ J
>>
G |- K : kind I
G |- I <l= J
G, x : K |- A : univ J
iforallEqUniv A B I J K L
G |- (iforall I (x : K) . A) = (iforall I (x : L) . B) : univ J
>>
G |- K = L : kind I
G |- I <l= J
G, x : K |- A = B : univ J
iforallIntroOf A I K M
G |- M : iforall I (x : K) . A
>>
G |- K : kind I
G, x : K |- M : A
iforallIntroEq A I K M N
G |- M = N : (iforall I (x : K) . A)
>>
G |- K : kind I
G, x : K |- M = N : A
iforallIntro A I K
G |- iforall I (x : K) . A ext [() / x]M
>>
G |- K : kind I
G, x (hidden) : K |- A ext M
iforallElimOf A I K M P
G |- M : [P / x]A
>>
G, x : K |- A : type
G |- M : iforall I (x : K) . A
G |- P : K
iforallElimEq A I K M N P
G |- M = N : [P / x]A
>>
G, x : K |- A : type
G |- M = N : (iforall I (x : K) . A)
G |- P : K
iforallElim A I K P
G |- [P / x]A ext M
>>
G, x : K |- A : type
G |- iforall I (x : K) . A ext M
G |- P : K
foralltpForm A
G |- (foralltp t . A) : type
>>
G, t : type |- A : type
foralltpEq A B
G |- (foralltp t . A) = (foralltp t . B) : type
>>
G, t : type |- A = B : type
foralltpIntroOf A M
G |- M : foralltp t . A
>>
G, t : type |- M : A
foralltpIntroEq A M N
G |- M = N : (foralltp t . A)
>>
G, t : type |- M = N : A
foralltpIntro A
G |- foralltp t . A ext [() / t]M
>>
G, t (hidden) : type |- A ext M
foralltpElimOf A B M
G |- M : [B / t]A
>>
G, t : type |- A : type
G |- M : foralltp t . A
G |- B : type
foralltpElimEq A B M N
G |- M = N : [B / t]A
>>
G, t : type |- A : type
G |- M = N : (foralltp t . A)
G |- B : type
foralltpElim A B
G |- [B / t]A ext M
>>
G, t : type |- A : type
G |- foralltp t . A ext M
G |- B : type
iexistsForm A I K
G |- (iexists I (x : K) . A) : type
>>
G |- K : kind I
G, x : K |- A : type
iexistsEq A B I K L
G |- (iexists I (x : K) . A) = (iexists I (x : L) . B) : type
>>
G |- K = L : kind I
G, x : K |- A = B : type
iexistsFormUniv A I J K
G |- (iexists I (x : K) . A) : univ J
>>
G |- K : kind I
G |- I <l= J
G, x : K |- A : univ J
iexistsEqUniv A B I J K L
G |- (iexists I (x : K) . A) = (iexists I (x : L) . B) : univ J
>>
G |- K = L : kind I
G |- I <l= J
G, x : K |- A = B : univ J
iexistsIntroOf A B I K M
G |- M : iexists I (x : K) . A
>>
G |- K : kind I
G, x : K |- A : type
G |- B : K
G |- M : [B / x]A
iexistsIntroEq A B I K M N
G |- M = N : (iexists I (x : K) . A)
>>
G |- K : kind I
G, x : K |- A : type
G |- B : K
G |- M = N : [B / x]A
iexistsIntro A B I K
G |- iexists I (x : K) . A ext M
>>
G |- K : kind I
G, x : K |- A : type
G |- B : K
G |- [B / x]A ext M
iexistsElimOf A B I K M P
G |- [M / y]P : B
>>
G |- K : type
G, x : K |- A : type
G, x : K, y : A |- P : B
G |- M : iexists I (x : K) . A
iexistsElimEq A B I K M N P Q
G |- [M / y]P = [N / y]Q : B
>>
G |- K : type
G, x : K |- A : type
G, x : K, y : A |- P = Q : B
G |- M = N : (iexists I (x : K) . A)
iexistsElim A B I K M
G |- B ext [(), M / x, y]P
>>
G |- K : type
G, x : K |- A : type
G, x (hidden) : K, y : A |- B ext P
G |- M : iexists I (x : K) . A
iexistsElimIstype A B I K M
G |- [M / y]B : type
>>
G |- K : type
G, x : K |- A : type
G, x : K, y : A |- B : type
G |- M : iexists I (x : K) . A
iexistsElimEqtype A B C I K M N
G |- [M / y]B = [N / y]C : type
>>
G |- K : type
G, x : K |- A : type
G, x : K, y : A |- B = C : type
G |- M = N : (iexists I (x : K) . A)
substitution n A B M
G1, x : A, G2 |- B ext N
>>
G1, x : A, G2 |- B : type
G1, x : A, G2 |- x = M : A
G1, [M / x]G2 |- [M / x]B ext N
substitutionSimple n A B M
G1, x : A, G2 |- B ext N
>>
G1, x : A, G2 |- x = M : A
G1, [M / x]G2 |- B ext N
generalize A B M
G |- [M / x]B ext [M / x]N
>>
G |- M : A
G, x : A |- B ext N
assert A B
G |- B ext let M (fn x . N)
>>
G |- A ext M
G, x : A |- B ext N
assert' A B
G |- B ext [M / x]N
>>
G |- A ext M
G, x : A |- B ext N
inhabitant A M
G |- A ext M
>>
G |- M : A
letForm A B M N
G |- let M (fn x . N) : B
>>
G |- M : A
G, x : A |- N : B
lethForm A B M N
G |- leth M (fn x . N) : B
>>
G |- M : A
G, x : A |- N : B
leteForm A B M N
G |- lete M (fn x . N) : B
>>
G |- M : A
G, x : A |- N : B
accInd A B I M N R
G |- [M / w]B ext fix (fn g . fn x . [fn y . fn r . g y / z]P) M
>>
G |- A : univ I
G |- R : A -> A -> univ I
G, x : A, z : (forall (y : A) . R y x -> [y / w]B) |- [x / w]B ext P
G |- M : A
G |- N : acc A R M
insert n
G1, G2 |- C ext [() / x]M
>>
G1, x : unit, G2 |- C ext M
forallLeft M
G, x : (forall (y : A) . B) |- C ext [x M / y]N
>>
G |- M : A
G, y : [M / x]B |- C ext N
(where x is not free in C)
arrowLeft
G, x : (A -> B) |- C ext [x M / y/N
>>
G |- A ext M
G, y : B |- C ext N
(where x is not free in C)
sequalForm M
G |- sequal M M : type
sequalIntroOf M
G |- () : sequal M M
sequalIntro M
G |- sequal M M
sequalTrivialize M N
G |- sequal M N
>>
G |- sequal M N
sequalExt M N P Q
G |- P = Q : sequal M N
>>
G |- P : sequal M N
G |- Q : sequal M N
sequalLeft n C M N
G1, x : (sequal M N), G2 |- C ext P
>>
G1, [() / x]G2 |- [() / x]C ext P
sequalEq A M N
G |- M = N : A
>>
G |- sequal M N
G |- M : A
sequalEqtp A B
G |- A = B : type
>>
G |- sequal A B
G |- A : type
sequivalence A B
G |- B ext M
>>
G |- sequal A B
G |- A ext M
sequivalenceLeft n A B C
G1, x : A, G2 |- C ext M
>>
G1, x : A, G2 |- sequal A B
G1, x : B, G2 |- C ext M
substitutionSyntactic n A B M
G1, x : A, G2 |- B ext N
>>
G1, x : A, G2 |- sequal x M
G1, [M / x]G2 |- [M / x]B ext N
sequalSymm M N
G |- sequal N M
>>
G |- sequal M N
sequalTrans M N P
G |- sequal M P
>>
G |- sequal M N
G |- sequal N P
sequalCompat M N P
G |- sequal [M / x]P [N / x]P
>>
G |- sequal M N
forallEtaSequal A B M
G |- sequal M (fn x . M x)
>>
G |- M : forall (x : A) . B
arrowEtaSequal A B M
G |- sequal M (fn x . M x)
>>
G |- M : A -> B
existsEtaSequal A B M
G |- sequal M (M #1 , M #2)
>>
G |- M : exists (x : A) . B
prodEtaSequal A B M
G |- sequal M (M #1 , M #2)
>>
G |- M : A & B
futureEtaSequal A M
G |- sequal M (next (M #prev))
>>
G |- M : future A
partialForm A
G |- partial A : type
>>
G |- A : type
partialEq A B
G |- partial A = partial B : type
>>
G |- A = B : type
partialFormUniv A I
G |- partial A : univ I
>>
G |- A : univ I
partialEqUniv A B I
G |- partial A = partial B : univ I
>>
G |- A = B : univ I
partialSub A B
G |- partial A <: partial B
>>
G |- A <: B
partialStrict A
G |- partial A <: partial (partial A)
>>
G |- A : type
partialStrictConverse A
G |- partial (partial A) <: partial A
>>
G |- A : type
partialIdem A
G |- eeqtp (partial (partial A)) (partial A) ext (() , ())
>>
G |- A : type
haltsForm A M
G |- halts M : type
>>
G |- M : partial A
haltsEq A M N
G |- halts M = halts N : type
>>
G |- M = N : partial A
haltsFormUniv A I M
G |- halts M : univ I
>>
G |- I : level
G |- M : partial A
haltsEqUniv A I M N
G |- halts M = halts N : univ I
>>
G |- I : level
G |- M = N : partial A
partialIntroBottomOf A
G |- bottom : partial A
>>
G |- A : type
bottomDiverges
G |- void
>>
G |- halts bottom
partialExt A M N
G |- M = N : partial A
>>
G |- A : type
G |- iff (halts M) (halts N)
G, x : (halts M) |- M = N : A
partialElimEq A M N
G |- M = N : A
>>
G |- M = N : partial A
G |- halts M
partialElimOf A M
G |- M : A
>>
G |- M : partial A
G |- halts M
haltsTrivialize M
G |- halts M
>>
G |- halts M
haltsExt M N P
G |- N = P : halts M
>>
G |- N : halts M
G |- P : halts M
haltsLeft n C M
G1, x : (halts M), G2 |- C ext N
>>
G1, [() / x]G2 |- [() / x]C ext N
haltsValue
G |- halts M
>>
(where M is valuable)
fixpointInductionEq A M N
G |- fix M = fix N : partial A
>>
G |- M = N : (partial A -> partial A)
G |- admiss A
fixpointInductionOf A M
G |- fix M : partial A
>>
G |- M : partial A -> partial A
G |- admiss A
partialFormInv A
G |- A : type
>>
G |- partial A : type
seqBind A B M M' N N'
G |- seq M (fn x . N) = seq M' (fn x . N') : partial B
>>
G |- M = M' : partial A
G, x : A |- N = N' : partial B
G |- B : type
activeApp A B M N
G |- M N : partial B
>>
G |- M : partial A
G, x : A |- x N : partial B
G |- B : type
activeAppSeq A B M N
G |- M N = seq M (fn x . x N) : partial B
>>
G |- M : partial A
G, x : A |- x N : partial B
G |- B : type
appHaltsInv M N
G |- halts M
>>
G |- halts (M N)
activePi1 A B M
G |- M #1 : partial B
>>
G |- M : partial A
G, x : A |- x #1 : partial B
G |- B : type
activePi1Seq A B M
G |- M #1 = seq M (fn x . x #1) : partial B
>>
G |- M : partial A
G, x : A |- x #1 : partial B
G |- B : type
pi1HaltsInv M
G |- halts M
>>
G |- halts (M #1)
activePi2 A B M
G |- M #2 : partial B
>>
G |- M : partial A
G, x : A |- x #2 : partial B
G |- B : type
activePi2Seq A B M
G |- M #2 = seq M (fn x . x #2) : partial B
>>
G |- M : partial A
G, x : A |- x #2 : partial B
G |- B : type
pi2HaltsInv M
G |- halts M
>>
G |- halts (M #2)
prevHaltsInv M
G |- halts M
>>
G |- halts (M #prev)
activeCase A B M P R
G |- sum_case M (fn y . P) (fn y . R) : partial B
>>
G |- M : partial A
G, x : A |- sum_case x (fn y . P) (fn y . R) : partial B
G |- B : type
activeCaseSeq A B M P R
G |- sum_case M (fn y . P) (fn y . R) = seq M (fn x . sum_case x (fn y . P) (fn y . R)) : partial B
>>
G |- M : partial A
G, x : A |- sum_case x (fn y . P) (fn y . R) : partial B
G |- B : type
caseHaltsInv M P R
G |- halts M
>>
G |- halts (sum_case M (fn y . P) (fn y . R))
seqHaltsSequal M N
G |- sequal (seq M (fn x . N)) [M / x]N
>>
G |- halts M
seqHaltsInv M N
G |- halts M
>>
G |- halts (seq M N)
sequalUnderSeq M M' N
G |- sequal (seq M (fn x . N)) [M' / x]N
>>
G |- seq M (fn x . sequal x M')
totalStrict A
G |- A <: partial A
>>
G |- A : type
G, x : A |- halts x
voidTotal'
G |- total void ext fn x . ()
voidStrict
G |- void <: partial void
unitTotal M
G |- halts M
>>
G |- M : unit
unitTotal'
G |- total unit ext fn x . ()
unitStrict
G |- unit <: partial unit
boolTotal M
G |- halts M
>>
G |- M : bool
boolTotal'
G |- total bool ext fn x . ()
boolStrict
G |- bool <: partial bool
forallTotal A B M
G |- halts M
>>
G |- M : forall (x : A) . B
forallTotal' A B
G |- total (forall (x : A) . B) ext fn x . ()
>>
G |- A : type
G, x : A |- B : type
forallStrict A B
G |- (forall (x : A) . B) <: partial (forall (x : A) . B)
>>
G |- A : type
G, x : A |- B : type
arrowTotal A B M
G |- halts M
>>
G |- M : A -> B
arrowTotal' A B
G |- total (A -> B) ext fn x . ()
>>
G |- A : type
G, x : A |- B : type
arrowStrict A B
G |- (A -> B) <: partial (A -> B)
>>
G |- A : type
G |- B : type
intersectStrict A B
G |- (intersect (x : A) . B) <: partial (intersect (x : A) . B)
>>
G |- A
G, x : A |- B <: partial B
existsTotal A B M
G |- halts M
>>
G |- M : exists (x : A) . B
existsTotal' A B
G |- total (exists (x : A) . B) ext fn x . ()
>>
G |- A : type
G, x : A |- B : type
existsStrict A B
G |- (exists (x : A) . B) <: partial (exists (x : A) . B)
>>
G |- A : type
G, x : A |- B : type
prodTotal A B M
G |- halts M
>>
G |- M : A & B
prodTotal' A B
G |- total (A & B) ext fn x . ()
>>
G |- A : type
G |- B : type
prodStrict A B
G |- (A & B) <: partial (A & B)
>>
G |- A : type
G |- B : type
dprodTotal A B M
G |- halts M
>>
G |- M : dprod A B
dprodTotal' A B
G |- total (dprod A B) ext (() , fn x . ())
>>
G |- A : type
G |- B : type
dprodStrict A B
G |- dprod A B <: partial (dprod A B)
>>
G |- A : type
G |- B : type
sumTotal A B M
G |- halts M
>>
G |- M : A % B
sumTotal' A B
G |- total (A % B) ext fn x . ()
>>
G |- A : type
G |- B : type
sumStrict A B
G |- (A % B) <: partial (A % B)
>>
G |- A : type
G |- B : type
futureTotal A M
G |- halts M
>>
G |- M : future A
futureTotal' A
G |- total (future A) ext fn x . ()
>>
promote(G) |- A : type
futureStrict A
G |- future A <: partial (future A)
>>
promote(G) |- A : type
setTotal' A B
G |- total {x : A | B} ext (() , fn x . ())
>>
G, x : A |- B : type
G |- total A
setStrict A B
G |- {x : A | B} <: partial {x : A | B}
>>
G, x : A |- B : type
G |- A <: partial A
isetTotal' A B
G |- total (iset A (fn x . B)) ext (() , fn x . ())
>>
G, x : A |- B : type
G |- total A
isetStrict A B
G |- iset A (fn x . B) <: partial (iset A (fn x . B))
>>
G, x : A |- B : type
G |- A <: partial A
quotientTotal' A B
G |- total (quotient (x y : A) . B) ext (() , fn x . ())
>>
G |- (quotient (x y : A) . B) : type
G, x : A, y : A |- B : type
G |- total A
natTotal M
G |- halts M
>>
G |- M : nat
natTotal'
G |- total nat ext fn x . ()
natStrict
G |- nat <: partial nat
typeHalts A
G |- halts A
>>
G |- A : type
reduceSeqTotal A M N
G |- sequal (seq M (fn x . N)) [M / x]N
>>
G |- M : A
G |- total A
haltsTotal A M
G |- halts M
>>
G |- M : A
G |- total A
uptypeForm A
G |- uptype A : type
>>
G |- A : type
uptypeEq A B
G |- uptype A = uptype B : type
>>
G |- A = B : type
uptypeFormUniv A I
G |- uptype A : univ I
>>
G |- A : univ I
uptypeEqUniv A B I
G |- uptype A = uptype B : univ I
>>
G |- A = B : univ I
uptypeTrivialize A
G |- uptype A
>>
G |- uptype A
uptypeExt A M N
G |- M = N : uptype A
>>
G |- M : uptype A
G |- N : uptype A
uptypeLeft n A B
G1, x : (uptype A), G2 |- B ext M
>>
G1, [() / x]G2 |- [() / x]B ext M
uptypeEeqtp A B
G |- uptype B
>>
G |- uptype A
G |- eeqtp A B
uptypeUnitary A
G |- uptype A
>>
G |- A <: unit
voidUptype
G |- uptype void
unitUptype
G |- uptype unit
boolUptype
G |- uptype bool
forallUptype A B
G |- uptype (forall (x : A) . B)
>>
G |- A : type
G, x : A |- uptype B
arrowUptype A B
G |- uptype (A -> B)
>>
G |- A : type
G |- uptype B
intersectUptype A B
G |- uptype (intersect (x : A) . B)
>>
G |- A : type
G, x : A |- uptype B
existsUptype A B
G |- uptype (exists (x : A) . B)
>>
G |- uptype A
G, x : A |- uptype B
prodUptype A B
G |- uptype (A & B)
>>
G |- uptype A
G |- uptype B
dprodUptype A B
G |- uptype (dprod A B)
>>
G |- uptype A
G, x : A |- uptype B
sumUptype A B
G |- uptype (A % B)
>>
G |- uptype A
G |- uptype B
futureUptype A
G |- uptype (future A)
>>
promote(G) |- uptype A
eqUptype A M N
G |- uptype (M = N : A)
>>
G |- M : A
G |- N : A
ofUptype A M
G |- uptype (M : A)
>>
G |- M : A
eqtpUptype A B
G |- uptype (A = B : type)
>>
G |- A : type
G |- B : type
istpUptype A
G |- uptype (A : type)
>>
G |- A : type
subtypeUptype A B
G |- uptype (A <: B)
>>
G |- A : type
G |- B : type
setUptype A B
G |- uptype {x : A | B}
>>
G |- uptype A
G, x : A |- B : type
isetUptype A B
G |- uptype (iset A (fn x . B))
>>
G |- uptype A
G, x : A |- B : type
muUptype A
G |- uptype (mu t . A)
>>
G, t : type |- A : type
G, t : type, x : (uptype t) |- uptype A
G |- positive (fn t . A)
muUptypeUniv A I
G |- uptype (mu t . A)
>>
G |- I : level
G, t : (univ I) |- A : univ I
G, t : (univ I), x : (uptype t) |- uptype A
G |- positive (fn t . A)
recUptype A
G |- uptype (rec t . A)
>>
G, t (later) : type |- A : type
G, t (later) : type, x (later) : (uptype t) |- uptype A
recUptypeUniv A I
G |- uptype (rec t . A)
>>
G |- I : level
G, t (later) : (univ I) |- A : univ I
G, t (later) : (univ I), x (later) : (uptype t) |- uptype A
natUptype
G |- uptype nat
uptypeFormInv A
G |- A : type
>>
G |- uptype A : type
admissForm A
G |- admiss A : type
>>
G |- A : type
admissEq A B
G |- admiss A = admiss B : type
>>
G |- A = B : type
admissFormUniv A I
G |- admiss A : univ I
>>
G |- A : univ I
admissEqUniv A B I
G |- admiss A = admiss B : univ I
>>
G |- A = B : univ I
admissTrivialize A
G |- admiss A
>>
G |- admiss A
admissExt A M N
G |- M = N : admiss A
>>
G |- M : admiss A
G |- N : admiss A
admissLeft n A B
G1, x : (admiss A), G2 |- B ext M
>>
G1, [() / x]G2 |- [() / x]B ext M
admissEeqtp A B
G |- admiss B
>>
G |- admiss A
G |- eeqtp A B
uptypeAdmiss A
G |- admiss A
>>
G |- uptype A
partialAdmiss A
G |- admiss (partial A)
>>
G |- admiss A
voidAdmiss
G |- admiss void
unitAdmiss
G |- admiss unit
boolAdmiss
G |- admiss bool
forallAdmiss A B
G |- admiss (forall (x : A) . B)
>>
G |- A : type
G, x : A |- admiss B
arrowAdmiss A B
G |- admiss (A -> B)
>>
G |- A : type
G |- admiss B
intersectAdmiss A B
G |- admiss (intersect (x : A) . B)
>>
G |- A : type
G, x : A |- admiss B
existsAdmissUptype A B
G |- admiss (exists (x : A) . B)
>>
G |- uptype A
G, x : A |- admiss B
prodAdmiss A B
G |- admiss (A & B)
>>
G |- admiss A
G |- admiss B
dprodAdmissUptype A B
G |- admiss (dprod A B)
>>
G |- uptype A
G, x : A |- admiss B
sumAdmiss A B
G |- admiss (A % B)
>>
G |- admiss A
G |- admiss B
futureAdmiss A
G |- admiss (future A)
>>
promote(G) |- admiss A
eqAdmiss A M N
G |- admiss (M = N : A)
>>
G |- M : A
G |- N : A
ofAdmiss A M
G |- admiss (M : A)
>>
G |- M : A
eqtpAdmiss A B
G |- admiss (A = B : type)
>>
G |- A : type
G |- B : type
istpAdmiss A
G |- admiss (A : type)
>>
G |- A : type
subtypeAdmiss A B
G |- admiss (A <: B)
>>
G |- A : type
G |- B : type
recAdmiss A
G |- admiss (rec t . A)
>>
G, t (later) : type |- A : type
G, t (later) : type, x (later) : (admiss t) |- admiss A
recAdmissUniv A I
G |- admiss (rec t . A)
>>
G |- I : level
G, t (later) : (univ I) |- A : univ I
G, t (later) : (univ I), x (later) : (admiss t) |- admiss A
natAdmiss
G |- admiss nat
admissFormInv A
G |- A : type
>>
G |- admiss A : type
partialType
G |- partial : intersect (i : level) . univ i -> univ i
haltsType
G |- halts : intersect (i : level) . intersect (a : univ i) . partial a -> univ lzero
admissType
G |- admiss : intersect (i : level) . univ i -> univ i
uptypeType
G |- uptype : intersect (i : level) . univ i -> univ i
seqType
G |- seq : intersect (i : level) . intersect (a : univ i) . intersect (b : univ i) . partial a -> (a -> partial b) -> partial b
letIntro n M
G1, G2 |- C ext [M / x]N
>>
G1, x = M, G2 |- C ext N
letSubst n
G1, x = M, G2 |- C ext N
>>
G1, [M / x]G2 |- [M / x]C ext N
letFold n C
G1, x = M, G2 |- [M / y]C ext N
>>
G1, x = M, G2 |- [x / y]C ext N
letUnfold n C
G1, x = M, G2 |- [x / y]C ext N
>>
G1, x = M, G2 |- [M / y]C ext N
letFoldHyp (m+n+1) m H
G1, x = M, G2, z : [M / y]H, G3 |- C ext N
>>
G1, x = M, G2, z : [x / y]H, G3 |- C ext N
(where m = length(G3) and n = length(G2))
letUnfoldHyp (m+n+1) m H
G1, x = M, G2, z : [x / y]H, G3 |- C ext N
>>
G1, x = M, G2, z : [M / y]H, G3 |- C ext N
(where m = length(G3) and n = length(G2))
integerForm
G |- integer : type
integerEq
G |- integer = integer : type
integerFormUniv I
G |- integer : univ I
>>
G |- I : level
integerEqUniv I
G |- integer = integer : univ I
>>
G |- I : level
integerIntroOf
G |- M : integer
(where M is an integer literal)
integerIntroEq
G |- M = M : integer
(where M is an integer literal)
The remaining integer rules establish the properties of Istari’s
native integer operations through an isomorphism to Integer, which
defines the integers as a quotient over pairs of natural numbers
(quotient (x y : nat & nat) . x #1 + y #2 = x #2 + y #1 : nat).
integerToDefType
G |- integer_to_Integer : integer -> Integer
integerFromDefType
G |- integer_from_Integer : Integer -> integer
integerIsomorphism1
G |- (fn x . integer_from_Integer (integer_to_Integer x)) = (fn x . x) : (integer -> integer)
integerIsomorphism2
G |- (fn x . integer_to_Integer (integer_from_Integer x)) = (fn x . x) : (Integer -> Integer)
pluszSpec
G |- plusz
= (fn x . fn y . integer_from_Integer (Plusz (integer_to_Integer x) (integer_to_Integer y)))
: (integer -> integer -> integer)
negzSpec
G |- negz
= (fn x . integer_from_Integer (Negz (integer_to_Integer x)))
: (integer -> integer)
eqzbSpec
G |- eqzb
= (fn x . fn y . Eqzb (integer_to_Integer x) (integer_to_Integer y))
: (integer -> integer -> bool)
leqzbSpec
G |- leqzb
= (fn x . fn y . Leqzb (integer_to_Integer x) (integer_to_Integer y))
: (integer -> integer -> bool)
timeszSpec
G |- timesz
= (fn x . fn y . integer_from_Integer (Timesz (integer_to_Integer x) (integer_to_Integer y)))
: (integer -> integer -> integer)
integerTotal M
G |- halts M
>>
G |- M : integer
integerStrict
G |- integer <: partial integer
integerUptype
G |- uptype integer
integerAdmiss
G |- admiss integer
integerSequal M N
G |- sequal M N
>>
G |- M = N : integer
symbolForm
G |- symbol : type
symbolEq
G |- symbol = symbol : type
symbolFormUniv I
G |- symbol : univ I
>>
G |- I : level
symbolEqUniv I
G |- symbol = symbol : univ I
>>
G |- I : level
symbolIntroOf
G |- M : symbol
(where M is an symbol literal)
symbolIntroEq
G |- M = M : symbol
(where M is an symbol literal)
symbol_eqbType
G |- symbol_eqb : symbol -> symbol -> bool
symbol_eqbSpec1 M N
G |- symbol_eqb M N = true : bool
>>
G |- M = N : symbol
symbol_eqbSpec2 M N
G |- M = N : symbol
>>
G |- symbol_eqb M N = true : bool
symbolTotal M
G |- halts M
>>
G |- M : symbol
symbolStrict
G |- symbol <: partial symbol
symbolUptype
G |- uptype symbol
symbolAdmiss
G |- admiss symbol
symbolSequal M N
G |- sequal M N
>>
G |- M = N : symbol
These rules are tailor-made to justify certain transformations in the rewriter, to improve performance and robustness. (Some of the justifying derivations are quite large.)
eeqtpRefl A
G |- eeqtp A A ext (() , ())
>>
G |- A : type
eeqtpSymm A B
G |- eeqtp A B ext (() , ())
>>
G |- eeqtp B A
eeqtpTrans A B C
G |- eeqtp A C ext (() , ())
>>
G |- eeqtp A B
G |- eeqtp B C
weakenEqtpEeqtp A B
G |- eeqtp A B ext (() , ())
>>
G |- A = B : type
weakenSubtypeArrow A B
G |- A -> B ext fn x . x
>>
G |- A <: B
weakenEeqtpIff A B
G |- iff A B ext (fn x . x , fn x . x)
>>
G |- eeqtp A B
compatGuardEqtp1 A B B'
G |- (A -g> B) = (A -g> B') : type
>>
G |- A : type
G |- B = B' : type
compatSetEqtp0 A A' B
G |- {x : A | B} = {x : A' | B} : type
>>
G |- A = A' : type
G, x : A |- B : type
forallEeq A A' B B'
G |- eeqtp (forall (x : A) . B) (forall (x : A') . B') ext (() , ())
>>
G |- eeqtp A A'
G, x : A |- eeqtp B B'
existsEeq A A' B B'
G |- eeqtp (exists (x : A) . B) (exists (x : A') . B') ext (() , ())
>>
G |- eeqtp A A'
G, x : A |- eeqtp B B'
arrowEeq A A' B B'
G |- eeqtp (A -> B) (A' -> B') ext (() , ())
>>
G |- eeqtp A A'
G |- eeqtp B B'
prodEeq A A' B B'
G |- eeqtp (A & B) (A' & B') ext (() , ())
>>
G |- eeqtp A A'
G |- eeqtp B B'
dprodEeq A A' B B'
G |- eeqtp (dprod A B) (dprod A' B') ext (() , ())
>>
G |- eeqtp A A'
G, x : A |- eeqtp B B'
sumEeq A A' B B'
G |- eeqtp (A % B) (A' % B') ext (() , ())
>>
G |- eeqtp A A'
G |- eeqtp B B'
futureEeq A A'
G |- eeqtp (future A) (future A') ext (() , ())
>>
promote(G) |- eeqtp A A'
intersectEeq A A' B B'
G |- eeqtp (intersect (x : A) . B) (intersect (x : A') . B') ext (() , ())
>>
G |- eeqtp A A'
G, x : A |- eeqtp B B'
unionEeq A A' B B'
G |- eeqtp (union (x : A) . B) (union (x : A') . B') ext (() , ())
>>
G |- eeqtp A A'
G, x : A |- eeqtp B B'
compatGuardEeq1 A B B'
G |- eeqtp (A -g> B) (A -g> B') ext (() , ())
>>
G |- A : type
G |- eeqtp B B'
compatSetEeq0 A A' B
G |- eeqtp {x : A | B} {x : A' | B} ext (() , ())
>>
G |- eeqtp A A'
G, x : A |- B : type
compatIsetEeq0 A A' B
G |- eeqtp (iset A (fn x . B)) (iset A' (fn x . B)) ext (() , ())
>>
G |- eeqtp A A'
G, x : A |- B : type
compatIsetIff1 A B B'
G |- eeqtp (iset A (fn x . B)) (iset A (fn x . B')) ext (() , ())
>>
G |- A : type
G, x : A |- iff B B'
compatForallSubtype0 A A' B
G |- (forall (x : A) . B) <: (forall (x : A') . B)
>>
G |- A' <: A
G, x : A |- B : type
compatForallSubtype1 A B B'
G |- (forall (x : A) . B) <: (forall (x : A) . B')
>>
G |- A : type
G, x : A |- B <: B'
compatExistsSubtype0 A A' B
G |- (exists (x : A) . B) <: (exists (x : A') . B)
>>
G |- A <: A'
G, x : A' |- B : type
compatExistsSubtype1 A B B'
G |- (exists (x : A) . B) <: (exists (x : A) . B')
>>
G |- A : type
G, x : A |- B <: B'
compatIntersectSubtype0 A A' B
G |- (intersect (x : A) . B) <: (intersect (x : A') . B)
>>
G |- A' <: A
G, x : A |- B : type
compatIntersectSubtype1 A B B'
G |- (intersect (x : A) . B) <: (intersect (x : A) . B')
>>
G |- A : type
G, x : A |- B <: B'
compatUnionSubtype0 A A' B
G |- (union (x : A) . B) <: (union (x : A') . B)
>>
G |- A <: A'
G, x : A' |- B : type
compatUnionSubtype1 A B B'
G |- (union (x : A) . B) <: (union (x : A) . B')
>>
G |- A : type
G, x : A |- B <: B'
compatGuardArrow0 A A' B
G |- (A -g> B) <: (A' -g> B)
>>
G |- A : type
G |- B : type
G |- A' -> A
compatGuardSubtype1 A B B'
G |- (A -g> B) <: (A -g> B')
>>
G |- A : type
G |- B <: B'
compatSetSubtype0 A A' B
G |- {x : A | B} <: {x : A' | B}
>>
G |- A <: A'
G, x : A' |- B : type
compatSetArrow1 A B B'
G |- {x : A | B} <: {x : A | B'}
>>
G |- A : type
G, x : A |- B' : type
G, x : A |- B -> B'
compatIsetSubtype0 A A' B
G |- iset A (fn x . B) <: iset A' (fn x . B)
>>
G |- A <: A'
G, x : A' |- B : type
compatIsetArrow1 A B B'
G |- iset A (fn x . B) <: iset A (fn x . B')
>>
G |- A : type
G, x : A |- B' : type
G, x : A |- B -> B'
compatForallIff1 A B B'
G |- iff (forall (x : A) . B) (forall (x : A) . B') ext (fn f . fn x . M #1 (f x) , fn f . fn x . M #2 (f x))
>>
G |- A : type
G, x : A |- iff B B' ext M
compatExistsIff1 A B B'
G |- iff (exists (x : A) . B) (exists (x : A) . B') ext (fn p . (p #1 , [p #1 / x]M #1 (p #2)) , fn p . (p #1 , [p #1 / x]M #2 (p #2)))
>>
G |- A : type
G, x : A |- iff B B' ext M
compatArrowIff0 A A' B
G |- iff (A -> B) (A' -> B) ext (fn f . fn x . f (M #2 x) , fn f . fn x . f (M #1 x))
>>
G |- B : type
G |- iff A A' ext M
compatArrowIff1 A B B'
G |- iff (A -> B) (A -> B') ext (fn f . fn x . M #1 (f x) , fn f . fn x . M #2 (f x))
>>
G |- A : type
G |- iff B B' ext M
compatProdIff0 A A' B
G |- iff (A & B) (A' & B) ext (fn x . (M #1 (x #1) , x #2) , fn x . (M #2 (x #1) , x #2))
>>
G |- B : type
G |- iff A A' ext M
compatProdIff1 A B B'
G |- iff (A & B) (A & B') ext (fn x . (x #1 , M #1 (x #2)) , fn x . (x #1 , M #2 (x #2)))
>>
G |- A : type
G |- iff B B' ext M
compatDprodIff0 A A' B
G |- iff (dprod A B) (dprod A' B) ext (fn x . (M #1 (x #1) , x #2) , fn x . (M #2 (x #1) , x #2))
>>
G, x : A |- B : type
G |- iff A A' ext M
compatDprodIff1 A B B'
G |- iff (dprod A B) (dprod A B') ext (fn x . (x #1 , M #1 (x #2)) , fn x . (x #1 , M #2 (x #2)))
>>
G |- A : type
G |- iff B B' ext M
compatSumIff0 A A' B
G |- iff (A % B) (A' % B) ext (fn x . sum_case x (fn y . inl (M #1 y)) (fn y . inr y) , fn x . sum_case x (fn y . inl (M #2 y)) (fn y . inr y))
>>
G |- B : type
G |- iff A A' ext M
compatSumIff1 A B B'
G |- iff (A % B) (A % B') ext (fn x . sum_case x (fn y . inl y) (fn y . inr (M #1 y)) , fn x . sum_case x (fn y . inl y) (fn y . inr (M #2 y)))
>>
G |- A : type
G |- iff B B' ext M
compatFutureIff A A'
G |- iff (future A) (future A') ext (fn x . letnext x (fn y . next (M #1 y)) , fn x . letnext x (fn y . next (M #2 y)))
>>
promote(G) |- iff A A' ext M
compatForallArrow1 A B B'
G |- (forall (x : A) . B) -> forall (x : A) . B' ext fn f . fn x . M (f x)
>>
G |- A : type
G, x : A |- B -> B' ext M
compatExistsArrow1 A B B'
G |- (exists (x : A) . B) -> exists (x : A) . B' ext fn p . (p #1 , [p #1 / x]M (p #2))
>>
G |- A : type
G, x : A |- B' : type
G, x : A |- B -> B' ext M
compatArrowArrow0 A A' B
G |- (A -> B) -> A' -> B ext fn f . fn x . f (M x)
>>
G |- A : type
G |- B : type
G |- A' -> A ext M
compatArrowArrow1 A B B'
G |- (A -> B) -> A -> B' ext fn f . fn x . M (f x)
>>
G |- A : type
G |- B -> B' ext M
compatProdArrow0 A A' B
G |- A & B -> A' & B ext fn x . (M (x #1) , x #2)
>>
G |- B : type
G |- A -> A' ext M
compatProdArrow1 A B B'
G |- A & B -> A & B' ext fn x . (x #1 , M (x #2))
>>
G |- A : type
G |- B -> B' ext M
compatDprodArrow0 A A' B
G |- dprod A B -> dprod A' B ext fn x . (M (x #1) , x #2)
>>
G |- B : type
G |- A -> A' ext M
compatDprodArrow1 A B B'
G |- dprod A B -> dprod A B' ext fn x . (x #1 , M (x #2))
>>
G |- A : type
G |- B -> B' ext M
compatSumArrow0 A A' B
G |- A % B -> A' % B ext fn x . sum_case x (fn y . inl (M y)) (fn y . inr y)
>>
G |- A' : type
G |- B : type
G |- A -> A' ext M
compatSumArrow1 A B B'
G |- A % B -> A % B' ext fn x . sum_case x (fn y . inl y) (fn y . inr (M y))
>>
G |- A : type
G |- B' : type
G |- B -> B' ext M
compatFutureArrow A A'
G |- future A -> future A' ext fn x . letnext x (fn y . next (M y))
>>
promote(G) |- A -> A' ext M
compatForallEntails1 A B B'
G |- forall (x : A) . B' ext fn x . [F x / y]M
>>
G, x : A, y : B |- B' ext M
G |- forall (x : A) . B ext F
compatArrowEntails1 A B B'
G |- A -> B' ext fn x . [F x / y]M
>>
G, y : B |- B' ext M
G |- A -> B ext F
compatProdEntails0 A A' B
G |- A' & B ext ([P #1 / x]M , P #2)
>>
G, x : A |- A' ext M
G |- A & B ext P
compatProdEntails1 A B B'
G |- A & B' ext (P #1 , [P #2 / x]M)
>>
G, x : B |- B' ext M
G |- A & B ext P
compatDprodEntails0 A A' B
G |- dprod A' B ext ([P #1 / x]M , P #2)
>>
G, x : A |- A' ext M
G |- dprod A B ext P
compatDprodEntails1 A B B'
G |- dprod A B' ext (P #1 , [P #2 / y]M)
>>
G, y : B |- B' ext M
G |- dprod A B ext P