A.2.6 Coproduct types

{mathparpagebreakable}\\inferrule

*[right= $+$ -form]Γ ⊢A : $\\mathcal{U}$ _i
Γ ⊢B : $\\mathcal{U}$ _iΓ ⊢A+B : $\\mathcal{U}$ _i
\\inferrule*[right= $+$ -intro ${}_{1}$ ]Γ ⊢A : $\\mathcal{U}$ _i
Γ ⊢B : $\\mathcal{U}$ _i

Γ ⊢a : AΓ ⊢ ${\\mathsf{inl}}$ (a) : A+B\\inferrule*[right= $+$ -intro ${}_{2}$ ]Γ ⊢A : $\\mathcal{U}$ _i
Γ ⊢B : $\\mathcal{U}$ _i

Γ ⊢b : BΓ ⊢ ${\\mathsf{inr}}$ (b) : A+B
\\inferrule*[right= $+$ -elim]Γ,z : (A+B) ⊢C : $\\mathcal{U}$ _i

Γ,x : A ⊢c : C[ ${\\mathsf{inl}}$ (x)/z]
Γ,y : B ⊢d : C[ ${\\mathsf{inr}}$ (y)/z]

Γ ⊢e : A+BΓ ⊢ind_A+B(z.C,x.c,y.d,e) : C[e/z]\\inferrule*[right= $+$ -comp ${}_{1}$ ]Γ,z : (A+B) ⊢C : $\\mathcal{U}$ _i
Γ,x : A ⊢c : C[ ${\\mathsf{inl}}$ (x)/z]
Γ,y : B ⊢d : C[ ${\\mathsf{inr}}$ (y)/z]

Γ ⊢a : AΓ ⊢ind_A+B(z.C,x.c,y.d, ${\\mathsf{inl}}$ (a)) ≡c[a/x] : C[ ${\\mathsf{inl}}$ (a)/z]\\inferrule*[right= $+$ -comp ${}_{2}$ ]Γ,z : (A+B) ⊢C : $\\mathcal{U}$ _i
Γ,x : A ⊢c : C[ ${\\mathsf{inl}}$ (x)/z]
Γ,y : B ⊢d : C[ ${\\mathsf{inr}}$ (y)/z]

Γ ⊢b : BΓ ⊢ind_A+B(z.C,x.c,y.d, ${\\mathsf{inr}}$ (b)) ≡d[b/y] : C[ ${\\mathsf{inr}}$ (b)/z]In $\\mathsf{ind}_{A+B}$ , $z$ is bound in $C$ , $x$ is bound in $c$ , and $y$ is bound in $d$ .

单词	A26CoproductTypes
释义	A.2.6 Coproduct types {mathparpagebreakable}\\inferrule [right= $+$ -form]Γ ⊢A : $\\mathcal{U}$ _i Γ ⊢B : $\\mathcal{U}$ _iΓ ⊢A+B : $\\mathcal{U}$ _i \\inferrule[right= $+$ -intro ${}_{1}$ ]Γ ⊢A : $\\mathcal{U}$ _i Γ ⊢B : $\\mathcal{U}$ _i Γ ⊢a : AΓ ⊢ ${\\mathsf{inl}}$ (a) : A+B\\inferrule[right= $+$ -intro ${}_{2}$ ]Γ ⊢A : $\\mathcal{U}$ _i Γ ⊢B : $\\mathcal{U}$ _i Γ ⊢b : BΓ ⊢ ${\\mathsf{inr}}$ (b) : A+B \\inferrule[right= $+$ -elim]Γ,z : (A+B) ⊢C : $\\mathcal{U}$ _i Γ,x : A ⊢c : C[ ${\\mathsf{inl}}$ (x)/z] Γ,y : B ⊢d : C[ ${\\mathsf{inr}}$ (y)/z] Γ ⊢e : A+BΓ ⊢ind_A+B(z.C,x.c,y.d,e) : C[e/z]\\inferrule[right= $+$ -comp ${}_{1}$ ]Γ,z : (A+B) ⊢C : $\\mathcal{U}$ _i Γ,x : A ⊢c : C[ ${\\mathsf{inl}}$ (x)/z] Γ,y : B ⊢d : C[ ${\\mathsf{inr}}$ (y)/z] Γ ⊢a : AΓ ⊢ind_A+B(z.C,x.c,y.d, ${\\mathsf{inl}}$ (a)) ≡c[a/x] : C[ ${\\mathsf{inl}}$ (a)/z]\\inferrule[right= $+$ -comp ${}_{2}$ ]Γ,z : (A+B) ⊢C : $\\mathcal{U}$ _i Γ,x : A ⊢c : C[ ${\\mathsf{inl}}$ (x)/z] Γ,y : B ⊢d : C[ ${\\mathsf{inr}}$ (y)/z] Γ ⊢b : BΓ ⊢ind_A+B(z.C,x.c,y.d, ${\\mathsf{inr}}$ (b)) ≡d[b/y] : C[ ${\\mathsf{inr}}$ (b)/z]In $\\mathsf{ind}_{A+B}$ , $z$ is bound in $C$ , $x$ is bound in $c$ , and $y$ is bound in $d$ .
随便看	SerreSwanTheorem Serre-Swan theorem SerretFrenetEquations Serret-Frenet equations SerretFrenetEquationsInmathbbR2 Serret-Frenet equations in ℝ^2 Serre’s twisting theorem SesquilinearFormsOverGeneralFields sesquilinear forms over general fields Set set SetClosedUnderAnOperation set closed under an operation SetDifference set difference Set is a Π⁢𝖶-pretopos SetOfSampling set of sampling Sets and n-types SetsInUnivalentFoundations Sets in univalent foundations SetsThatDoNotHaveAnInfimum sets that do not have an infimum SetsWhereSequenceOfContinuousFunctionsDiverge sets where sequence of continuous functions diverge