nLab dependent anafunction

Contents

 Idea

In dependent type theory, given types AA and BB, an anafunction is a type family x:A,y:BR(x,y)typex\colon A, y \colon B \vdash R(x, y) \; \mathrm{type} which comes with a family of witnesses

x:Ap(x):isContr( y:BR(x,y))x \colon A \vdash p(x) \colon \mathrm{isContr}\left(\sum_{y:B} R(x, y) \right)

that for each element x:Ax\colon A, the dependent sum type y:BR(x,y)\sum_{y\colon B} R(x, y) is a contractible type.

A dependent anafunction is like such an anafunction but where we allow BB to also depend on x:Ax\colon A.

Definition

In dependent type theory (homotopy type theory), given a type AA and a type family x:AB(x)typex\colon A \vdash B(x) \; \mathrm{type}, a dependent anafunction is a type family x:A,y:B(x)R(x,y)typex\colon A, y\colon B(x) \vdash R(x, y) \; \mathrm{type} which comes with a family of witnesses

x:Ap(x):isContr( y:B(x)R(x,y))x \colon A \vdash p(x) \colon \mathrm{isContr}\left(\sum_{y\colon B(x)} R(x, y) \right)

that for each element x:Ax\colon A, the dependent sum type y:B(x)R(x,y)\sum_{y\colon B(x)} R(x, y) is a contractible type.

 Properties

The principle of unique choice holds in dependent type theory, which means that given any dependent anafunction x:A,y:B(x)R(x,y)typex:A, y:B(x) \vdash R(x, y) \; \mathrm{type}, there is a dependent function x:Af(x):B(x)x:A \vdash f(x):B(x).

Dependent function types as types of dependent anafunctions

In the same way that one could define equivalence types as types of one-to-one correspondences and function types as types of anafunctions, one could define dependent function types as types of dependent anafunctions. This requires both identity types and heterogeneous identity types being defined first, which we shall write as a= Aba =_A b and x= B pyx =_{B}^{p} y respectively for a:Aa:A, b:Ab:A, p:a= Abp:a =_A b, x:B(a)x:B(a), and y:B(b)y:B(b). We use Agda notation (x:A)B(x)(x:A) \to B(x) for dependent function types rather than the dependent product type notation x:AB(x)\prod_{x:A} B(x) or Π(x:A).B(x)\Pi(x:A).B(x) in this section.

Rules for dependent function types

ΓAtypeΓ,x:AB(x)typeΓ(x:A)B(x)typeΓAtypeΓ,x:AB(x)typeΓ,f:(x:A)B(x),x:A,y:B(x) A,B(f,x,y)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash (x:A) \to B(x) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, f:(x:A) \to B(x), x:A, y:B(x) \vdash \mathcal{F}_{A, B}(f, x, y) \; \mathrm{type}}
ΓAtypeΓ,x:AB(x)typeΓ,x:Af(x):B(x)Γλx.f(x):(x:A)B(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash f(x):B(x)}{\Gamma \vdash \lambda x.f(x):(x:A) \to B(x)}
ΓAtypeΓ,x:AB(x)typeΓ,x:Af(x):B(x)Γ,x:Aα(x): A,B(λx.f(x),x,f(x))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash f(x):B(x)}{\Gamma, x:A \vdash \alpha(x):\mathcal{F}_{A, B}(\lambda x.f(x), x, f(x))}
ΓAtypeΓ,x:AB(x)typeΓ,f:(x:A)B(x),x:Aev(f,x):B(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, f:(x:A) \to B(x), x:A \vdash \mathrm{ev}(f, x):B(x)}
ΓAtypeΓ,x:AB(x)typeΓ,f:(x:A)B(x),x:Aβ(f,x): A,B(f,x,ev(f,x))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, f:(x:A) \to B(x), x:A \vdash \beta(f, x):\mathcal{F}_{A, B}(f, x, \mathrm{ev}(f, x))}
ΓAtypeΓ,x:AB(x)typeΓ,f:(x:A)B(x),x:A,y:B(x),u: A,B(f,x,y)κ(f,x,y,u):ev(f,x)= B(x)y\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, f:(x:A) \to B(x), x:A, y:B(x), u:\mathcal{F}_{A, B}(f, x, y) \vdash \kappa(f, x, y, u):\mathrm{ev}(f, x) =_{B(x)} y}
ΓAtypeΓ,x:AB(x)typeΓ,f:(x:A)B(x),x:A,y:B(x),u: A,B(f,x,y)η(f,x,y,u):β(f,x)= A,B(f,x) κ(f,x,y,u)u\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, f:(x:A) \to B(x), x:A, y:B(x), u:\mathcal{F}_{A, B}(f, x, y) \vdash \eta(f, x, y, u):\beta(f, x) =_{\mathcal{F}_{A, B}(f, x)}^{\kappa(f, x, y, u)} u}

By the rules for dependent pair types and dependent function types, one could derive that

ΓAtypeΓ,x:AB(x)typeΓ,f:(x:A)B(x)η(f):(x:A)isContr((y:B)× A,B(f,x,y))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, f:(x:A) \to B(x) \vdash \eta(f):(x:A) \to \mathrm{isContr}\left((y:B) \times \mathcal{F}_{A, B}(f, x, y)\right)}

which is precisely the statement that A,B(f)\mathcal{F}_{A, B}(f) is a dependent anafunction for all dependent functions f:(x:A)B(x)f:(x:A) \to B(x).

 See also

Last revised on January 7, 2023 at 04:57:32. See the history of this page for a list of all contributions to it.