nLab congruence rule

Redirected from "typal congruence rules".

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Deduction and Induction

Constructivism, Realizability, Computability

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Definition

Judgmental congruence rules

In dependent type theory with judgmental equality, a (judgmental) congruence rule is an inference rule which states that judgmental equality is respected.

For example, there is a congruence rule for element conversion, which states that given judgmentally equal types AA and BB and judgmentally equal elements aa and bb of AA, aa and bb are judgmentally equal elements of BB:

ΓABtypeΓab:AΓab:B\frac{\Gamma \vdash A \equiv B \; \mathrm{type} \quad \Gamma \vdash a \equiv b:A}{\Gamma \vdash a \equiv b:B}

There are many other different judgmental congruence rules, one for every term or type that is formed in the natural deduction inference rules in the type theory:

Congruence rules for dependent function types

ΓAAtypeΓ,x:AB(x)B(x)typeΓ x:AB(x) x:AB(x)type\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \end{array} }{\Gamma \vdash \prod_{x:A} B(x) \equiv \prod_{x:A'} B'(x)\; \mathrm{type}}
ΓAtypeΓ,x:AB(x)typeΓ,x:Ab(x):B(x)Γ,x:Ab(x):B(x) Γ,x:Ab(x)b(x):B(x)Γλx:A.b(x)λx:A.b(x): x:A.B(x)\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B(x) \quad \Gamma, x:A \vdash b'(x):B(x) \\ \Gamma, x:A \vdash b(x) \equiv b'(x):B(x) \end{array} }{\Gamma \vdash \lambda x:A.b(x) \equiv \lambda x:A.b'(x):\prod_{x:A}.B(x)}
ΓAtypeΓ,x:AB(x)typeΓf: x:AB(x)f: x:AB(x) Γff: x:AB(x)Γ,x:Af(x)f(x):B(x)\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B(x) \quad f':\prod_{x:A} B(x) \\ \Gamma \vdash f \equiv f':\prod_{x:A} B(x) \end{array} }{\Gamma, x:A \vdash f(x) \equiv f'(x):B(x)}

If the dependent function type is weak, then there are also the following congruence rules for the computation and uniqueness rules of dependent function types:

ΓAtypeΓ,x:AB(x)typeΓ,x:Ab(x):B(x)Γ,x:Ab(x):B(x) Γ,x:Ab(x)b(x):B(x)Γβ A,Bx:A.b(x)β A,Bx:A.b(x): x:Ab(x)= B(x)(λx:A.b(x))(x)\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B(x) \quad \Gamma, x:A \vdash b'(x):B(x) \\ \Gamma, x:A \vdash b(x) \equiv b'(x):B(x) \end{array} }{\Gamma \vdash \beta_{\prod}^{A, B} x:A.b(x) \equiv \beta_{\prod}^{A, B} x:A.b'(x):\prod_{x:A} b(x) =_{B(x)} (\lambda x:A.b(x))(x)}
ΓAtypeΓ,x:AB(x)typeΓ,x:AB(x)type Γ,x:AB(x)B(x)typeΓη A,Bη A,B: f: x:AB(x)f= x:AB(x)λx:A.f(x)\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash B'(x) \; \mathrm{type} \\ \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \end{array} }{\Gamma \vdash \eta_{\prod}^{A, B} \equiv \eta_{\prod}^{A, B'}:\prod_{f:\prod_{x:A} B(x)} f =_{\prod_{x:A} B(x)} \lambda x:A.f(x)}

Congruence rules for dependent pair types:

ΓAAtypeΓ,x:AB(x)B(x)typeΓ x:AB(x) x:AB(x)type\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \end{array} }{\Gamma \vdash \sum_{x:A} B(x) \equiv \sum_{x:A'} B'(x)\; \mathrm{type}}
ΓAAtypeΓ,x:AB(x)B(x)typeΓ,x:A,y:B(x)pair A,Bpair A,B: x:AB(x)\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \end{array} }{\Gamma, x:A, y:B(x) \vdash \mathrm{pair}_{\sum}^{A, B} \equiv \mathrm{pair}_{\sum}^{A', B'}:\sum_{x:A} B(x)}
ΓAAtypeΓ,x:AB(x)B(x)typeΓ,z: x:AB(x)C(z)C(z)typeΓind A,B,Cind A,B,C: g: x:A y:B(x)C(pair A,B(x,y)) z: x:AB(x)C(z)\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C(z) \equiv C'(z) \; \mathrm{type} \end{array} }{\Gamma \vdash \mathrm{ind}_{\sum}^{A, B, C} \equiv \mathrm{ind}_{\sum}^{A', B', C'}:\prod_{g:\prod_{x:A} \prod_{y:B(x)} C(\mathrm{pair}_{\sum}^{A, B}(x, y))} \prod_{z:\sum_{x:A} B(x)} C(z)}

If the dependent pair type is weak, then there is also the following congruence rule for the computation rule of dependent pair types:

ΓAAtypeΓ,x:AB(x)B(x)typeΓ,z: x:AB(x)C(z)C(z)typeΓβ A,B,Cβ A,B,C: g: x:A y:B(x)C(pair A,B(x,y)) x:A y:B(x)ind A,B,C(g,pair A,B(x,y))= C(pair A,B(x,y))g(x,y)\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C(z) \equiv C'(z) \; \mathrm{type} \end{array} }{\Gamma \vdash \beta_{\sum}^{A, B, C} \equiv \beta_{\sum}^{A', B', C'}:\prod_{g:\prod_{x:A} \prod_{y:B(x)} C(\mathrm{pair}_{\sum}^{A, B}(x, y))} \prod_{x:A} \prod_{y:B(x)} \mathrm{ind}_{\sum}^{A, B, C}(g, \mathrm{pair}_{\sum}^{A, B}(x, y)) =_{C(\mathrm{pair}_{\sum}^{A, B}(x, y))} g(x, y)}

Congruence rules for identity types:

ΓAAtypeΓ,x:A,y:Ax= Ayx= Ay\frac{\Gamma \vdash A \equiv A' \; \mathrm{type}}{\Gamma, x:A, y:A \vdash x =_A y \equiv x =_{A'} y}
ΓAAtypeΓrefl Arefl A: x:Ax= Ax\frac{\Gamma \vdash A \equiv A' \; \mathrm{type}}{\Gamma \vdash \mathrm{refl}_A \equiv \mathrm{refl}_{A'}:\prod_{x:A} x =_A x}
ΓAAtypeΓ,x:A,y:A,p:x= AyC(x,y,p)C(x,y,p)typeΓind = A,Cind = A,C: t: x:AC(x,x,refl A(x)) x:A y:A p:x= AyC(x,y,p)\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A, y:A, p:x =_A y \vdash C(x, y, p) \equiv C'(x, y, p) \; \mathrm{type} \end{array} }{\Gamma \vdash \mathrm{ind}_{=}^{A, C} \equiv \mathrm{ind}_{=}^{A', C'}:\prod_{t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x))} \prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} C(x, y, p)}

If the identity types are weak, then there is also the following congruence rule for the computation rule of identity types:

ΓAAtypeΓ,x:A,y:A,p:x= AyC(x,y,p)C(x,y,p)typeΓβ ind = A,Cβ ind = A,C: t: x:AC(x,x,refl A(x)) x:Aind = A,C(t,x,x,refl A(x))= C(x,x,refl A(x))t(x)\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A, y:A, p:x =_A y \vdash C(x, y, p) \equiv C'(x, y, p) \; \mathrm{type} \end{array} }{\Gamma \vdash \beta_{ \mathrm{ind}_=}^{A, C} \equiv \beta_{\mathrm{ind}_=}^{A', C'}:\prod_{t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x))} \prod_{x:A} \mathrm{ind}_{=}^{A, C}(t, x, x, \mathrm{refl}_A(x)) =_{C(x, x, \mathrm{refl}_A(x))} t(x)}

Congruence rules for the empty type:

Γ,x:C(x)C(x)typeΓind Cind C: x:C(x)type\frac{\Gamma, x:\emptyset \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{ind}_\emptyset^C \equiv \mathrm{ind}_\emptyset^{C'}:\prod_{x:\emptyset} C(x) \; \mathrm{type}}

Congruence rules for the type of booleans:

Γ,x:𝟚C(x)C(x)typeΓind 𝟚 Cind 𝟚 C: a:C(0) b:C(1) x:𝟚C(x)\frac{\Gamma, x:\mathbb{2} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{ind}_\mathbb{2}^C \equiv \mathrm{ind}_\mathbb{2}^{C'}:\prod_{a:C(0)} \prod_{b:C(1)} \prod_{x:\mathbb{2}} C(x)}

If the type of booleans is weak, then there are also the following congruence rules for the computation rules of the type of booleans:

Γ,x:𝟚C(x)C(x)typeΓβ 𝟚 0,Cβ 𝟚 0,C: a:C(0) b:C(1)ind 𝟚 C(a,b,0)= C(0)a\frac{\Gamma, x:\mathbb{2} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \beta_\mathbb{2}^{0, C} \equiv \beta_\mathbb{2}^{0, C'}:\prod_{a:C(0)} \prod_{b:C(1)} \mathrm{ind}_\mathbb{2}^C(a, b, 0) =_{C(0)} a}
Γ,x:𝟚C(x)C(x)typeΓβ 𝟚 1,Cβ 𝟚 1,C: a:C(0) b:C(1)ind 𝟚 C(a,b,1)= C(1)b\frac{\Gamma, x:\mathbb{2} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \beta_\mathbb{2}^{1, C} \equiv \beta_\mathbb{2}^{1, C'}:\prod_{a:C(0)} \prod_{b:C(1)} \mathrm{ind}_\mathbb{2}^C(a, b, 1) =_{C(1)} b}

Congruence rules for the natural numbers type:

Γ,x:C(x)C(x)typeΓind Cind C: c 0:C(0) c s: x:C(x)C(s(x)) x:C(x)\frac{\Gamma, x:\mathbb{N} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C \equiv \mathrm{ind}_\mathbb{N}^{C'}:\prod_{c_0:C(0)} \prod_{c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))} \prod_{x:\mathbb{N} C(x)}}

If the natural numbers type is weak, then there are also the following congruence rules for the computation rules of the natural numbers type:

Γ,x:C(x)C(x)typeΓβ 0,Cβ 0,C: c 0:C(0) c s: x:C(x)C(s(x))ind C(c 0,c s,0)= C(0)c 0\frac{\Gamma, x:\mathbb{N} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \beta_\mathbb{N}^{0, C} \equiv \beta_\mathbb{N}^{0, C'}:\prod_{c_0:C(0)} \prod_{c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))} \mathrm{ind}_\mathbb{N}^C(c_0, c_s, 0) =_{C(0)} c_0}
Γ,x:C(x)C(x)typeΓβ s,Cβ s,C: c 0:C(0) c s: x:C(x)C(s(x)) x:ind C(c 0,c s,s(x))= C(s(x))c s(x)(ind C(c 0,c s,x))\frac{\Gamma, x:\mathbb{N} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \beta_\mathbb{N}^{s, C} \equiv \beta_\mathbb{N}^{s, C'}:\prod_{c_0:C(0)} \prod_{c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))} \prod_{x:\mathbb{N}} \mathrm{ind}_\mathbb{N}^C(c_0, c_s, s(x)) =_{C(s(x))} c_s(x)(\mathrm{ind}_\mathbb{N}^C(c_0, c_s, x))}

Congruence rules for axioms

Similarly, we have congruence rules for every axiom in the dependent type theory, such as

ΓAAtypeΓ,x:AB(x)B(x)typeΓfunext A,Bfunext A,B: f; x:AB(x) g: x:AB(x)(f= x:AB(x)g) x:Af(x)= B(x)g(x)\frac{\Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{funext}_{A, B} \equiv \mathrm{funext}_{A', B'}:\prod_{f;\prod_{x:A} B(x)} \prod_{g:\prod_{x:A} B(x)} (f =_{\prod_{x:A} B(x)} g) \simeq \prod_{x:A} f(x) =_{B(x)} g(x)}
ΓAAtypeΓ,x:AB(x)B(x)typeΓ,x:A,y:B(x)C(x,y)C(x,y)typeΓchoice A,B,Cchoice A,B,C:(isSet(A)× x:AisSet(B(x)))x:A.y:B(x).C(x,y)g: x:AB(x).x:A.C(x,g(x))\frac{\Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \quad \Gamma, x:A, y:B(x) \vdash C(x, y) \equiv C'(x, y) \; \mathrm{type}}{\Gamma \vdash \mathrm{choice}_{A, B, C} \equiv \mathrm{choice}_{A', B', C'}:\left(\mathrm{isSet}(A) \times \prod_{x:A} \mathrm{isSet}(B(x))\right) \to \forall x:A.\exists y:B(x).C(x, y) \to \exists g:\prod_{x:A} B(x).\forall x:A.C(x, g(x))}

Typal congruence rules

In dependent type theory, a typal congruence rule is an derivable inference rule which states that given identifications of the component terms and equivalences of the component types in the hypotheses of the natural deduction inference rules, one could derive the corresponding identification and equivalences of the derived terms and types in the conclusion of the inference rules.

For example, the typal congruence rule for element conversion states that given equivalent types AA and BB with equivalence e:ABe:A \simeq B and typally equal elements aa and bb of AA with identification p:a= Abp:a =_A b, e(a)e(a) and e(b)e(b) are typally elements of BB, and is given by application of ee to pp:

ΓAtypeΓBtypeΓe:ABΓa:AΓb:AΓp:a= AbΓap e(a,b,p):e(a)= Be(b)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b}{\Gamma \vdash \mathrm{ap}_e(a, b, p):e(a) =_B e(b)}

There are many other different typal congruence rules which are derivable, one for every term or type that is formed in the natural deduction inference rules in the type theory:

Congruence rules for dependent function types

ΓAtypeΓAtypeΓe A:AA Γ,x:AB(x)typeΓ,x:AB(x)typeΓ,x:Ae B(x):B(x)B(x)Γcongform x:AB(x):( x:AB(x))( x:AB(x))\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash A' \; \mathrm{type} \quad \Gamma \vdash e_A:A \simeq A' \\ \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash B'(x) \; \mathrm{type} \quad \Gamma, x:A \vdash e_B(x):B(x) \simeq B'(x) \end{array} }{\Gamma \vdash \mathrm{congform}_{\prod_{x:A} B(x)}:\left(\prod_{x:A} B(x)\right) \simeq \left(\prod_{x:A'} B'(x)\right)}
ΓAtypeΓ,x:AB(x)typeΓ,x:Ab(x):B(x)Γ,x:Ab(x):B(x) Γ,x:Ap(x):b(x)= B(x)b(x)ΓcongIntro x:AB(x) x:A.b(x),x:A.b(x),x:A.p(x):λx:A.b(x)= x:A.B(x)λx:A.b(x)\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B(x) \quad \Gamma, x:A \vdash b'(x):B(x) \\ \Gamma, x:A \vdash p(x):b(x) =_{B(x)} b'(x) \end{array} }{\Gamma \vdash \mathrm{congIntro}_{\prod_{x:A} B(x)}^{x:A.b(x), x:A.b'(x), x:A.p(x)}:\lambda x:A.b(x) =_{\prod_{x:A}.B(x)} \lambda x:A.b'(x)}
ΓAtypeΓ,x:AB(x)typeΓf: x:AB(x)f: x:AB(x) Γp:f= x:AB(x)fΓ,x:AcongElim x:AB(x)(p,x):f(x)= B(x)f(x)\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B(x) \quad f':\prod_{x:A} B(x) \\ \Gamma \vdash p:f =_{\prod_{x:A} B(x)} f' \end{array} }{\Gamma, x:A \vdash \mathrm{congElim}_{\prod_{x:A} B(x)}(p, x):f(x) =_{B(x)} f'(x)}

Congruence rules for identity types:

ΓAtypeΓAtypeΓe A:AAΓ,x:A,y:Acongform = A(e A,x,y):(x= Ay)(e(x)= Ae(y))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash A' \; \mathrm{type} \quad \Gamma \vdash e_A:A \simeq A'}{\Gamma, x:A, y:A \vdash \mathrm{congform}_{=_A}(e_A, x, y):(x =_A y) \simeq (e(x) =_{A'} e(y))}
ΓAtypeΓAtypeΓe A:AAΓcongIntro = A(e A):congForm x:Ax= Ax(refl A)= x:Ax= Axrefl A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash A' \; \mathrm{type} \quad \Gamma \vdash e_A:A \simeq A'}{\Gamma \vdash \mathrm{congIntro}_{=_A}(e_A):\mathrm{congForm}_{\prod_{x:A} x =_A x}(\mathrm{refl}_A) =_{\prod_{x:A'} x =_A x} \mathrm{refl}_{A'}}
ΓAtypeΓ,z: x:A y:Ax= AyC(z)typeΓ,z: x:A y:Ax= AyC(z)type ΓAtypeΓe C: z: x:A y:Ax= AyC(z)C(z) ΓcongElim = A(e C):congForm t: x:AC(Δ A(x)) z: x:A y:Ax= AyC(z)(congForm z: x:A y:Ax= AyC(z)(ind = A,C))= t: x:AC(Δ A(x)) z: x:A y:Ax= AyC(z)ind = A,C\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} \sum_{y:A} x =_A y \vdash C(z) \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} \sum_{y:A} x =_A y \vdash C'(z) \; \mathrm{type} \\ \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash e_C:\prod_{z:\sum_{x:A} \sum_{y:A} x =_A y} C(z) \simeq C'(z) \\ \end{array} }{\Gamma \vdash \mathrm{congElim}_{=_A}(e_C):\mathrm{congForm}_{\prod_{t:\prod_{x:A} C'(\Delta_A(x))} \prod_{z:\sum_{x:A} \sum_{y:A} x =_A y} C'(z)}(\mathrm{congForm}_{\prod_{z:\sum_{x:A} \sum_{y:A} x =_A y} C'(z)}(\mathrm{ind}_{=}^{A, C})) =_{\prod_{t:\prod_{x:A} C'(\Delta_A(x))} \prod_{z:\sum_{x:A} \sum_{y:A} x =_A y} C'(z)} \mathrm{ind}_{=}^{A, C'}}

where Δ A(x)(x,x,refl A(x)): x:A y:Ax= Ay\Delta_A(x) \coloneqq (x, x, \mathrm{refl}_A(x)):\sum_{x:A} \sum_{y:A} x =_A y is the diagonal function of AA.

 See also

References

Last revised on November 25, 2023 at 19:30:36. See the history of this page for a list of all contributions to it.