congruence rule (changes) in nLab

Showing changes from revision #2 to #3: Added | Removed | Changed

\tableofcontents

Definition

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

Judgmental congruence rules

For In example, there is a congruence rule for element conversion, which states that given judgmentally equal typesAAdependent type theory and withBBjudgmental equality , and a judgmentally equal elementsaa(judgmental) congruence rule and is anbbinference rule of which states thatAAjudgmental equality , is respected.aa and bb are judgmentally equal elements of BB:

Γ⊢A≡BtypeΓ⊢a≡b:AΓ⊢a≡b:B\frac{\Gamma \vdash A \equiv B \; \mathrm{type} \quad \Gamma \vdash a \equiv b:A}{\Gamma \vdash a \equiv b:B}

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:

Γ⊢A≡BtypeΓ⊢a≡b:AΓ⊢a≡b: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

Γ⊢A≡A′typeΓ,x:A⊢B(x)≡B′(x)typeΓ⊢∏ x:AB(x)≡∏ x:A′B′(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:A⊢B(x)typeΓ,x:A⊢b(x):B(x)Γ,x:A⊢b′(x):B(x) Γ,x:A⊢b(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:A⊢B(x)typeΓ⊢f:∏ x:AB(x)f′:∏ x:AB(x) Γ⊢f≡f′:∏ x:AB(x)Γ,x:A⊢f(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:A⊢B(x)typeΓ,x:A⊢b(x):B(x)Γ,x:A⊢b′(x):B(x) Γ,x:A⊢b(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:A⊢B(x)typeΓ,x:A⊢B′(x)type Γ,x:A⊢B(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:

Γ⊢A≡A′typeΓ,x:A⊢B(x)≡B′(x)typeΓ⊢∑ x:AB(x)≡∑ x:A′B′(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}}

Γ⊢A≡A′typeΓ,x:A⊢B(x)≡B′(x)typeΓ,x:A,y:B(x)⊢pair ∑ A,B≡pair ∑ 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)}

Γ⊢A≡A′typeΓ,x:A⊢B(x)≡B′(x)typeΓ,z:∑ x:AB(x)⊢C(z)≡C′(z)typeΓ⊢ind ∑ A,B,C≡ind ∑ 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:

Γ⊢A≡A′typeΓ,x:A⊢B(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:

Γ⊢A≡A′typeΓ,x:A,y:A⊢x= Ay≡x= A′y\frac{\Gamma \vdash A \equiv A' \; \mathrm{type}}{\Gamma, x:A, y:A \vdash x =_A y \equiv x =_{A'} y}

Γ⊢A≡A′typeΓ⊢refl A≡refl 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}

Γ⊢A≡A′typeΓ,x:A,y:A,p:x= Ay⊢C(x,y,p)≡C′(x,y,p)typeΓ⊢ind = A,C≡ind = 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:

Γ⊢A≡A′typeΓ,x:A,y:A,p:x= Ay⊢C(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 ∅ C≡ind ∅ 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 𝟚 C≡ind 𝟚 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 ℕ C≡ind ℕ 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

• congruence rule for function extensionality:

Γ⊢A≡A′typeΓ,x:A⊢B(x)≡B′(x)typeΓ⊢funext A,B≡funext 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)}

• congruence rule for the axiom of choice:

Γ⊢A≡A′typeΓ,x:A⊢B(x)≡B′(x)typeΓ,x:A,y:B(x)⊢C(x,y)≡C′(x,y)typeΓ⊢choice A,B,C≡choice 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:A≃Be: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:A≃BΓ⊢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Γ⊢A′typeΓ⊢e A:A≃A′ Γ,x:A⊢B(x)typeΓ,x:A⊢B′(x)typeΓ,x:A⊢e B(x):B(x)≃B′(x)Γ⊢congform ∏ x:AB(x):(∏ x:AB(x))≃(∏ x:A′B′(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:A⊢B(x)typeΓ,x:A⊢b(x):B(x)Γ,x:A⊢b′(x):B(x) Γ,x:A⊢p(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:A⊢B(x)typeΓ⊢f:∏ x:AB(x)f′:∏ x:AB(x) Γ⊢p:f= ∏ x:AB(x)f′Γ,x:A⊢congElim ∏ 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Γ⊢A′typeΓ⊢e A:A≃A′Γ,x:A,y:A⊢congform = A(e A,x,y):(x= Ay)≃(e(x)= A′e(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Γ⊢A′typeΓ⊢e A:A≃A′Γ⊢congIntro = A(e A):congForm ∏ x:Ax= Ax(refl A)= ∏ x:A′x= 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= Ay⊢C(z)typeΓ,z:∑ x:A∑ y:Ax= Ay⊢C′(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

• inference rule

• structural rule

References

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)