$$\def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$

Pi package contains basic theorems about Pi types. Pi type is built in core of any dependent type checker. Type checkers with Pi only type are called Pure Type Systems. See OM language for our Erlang implementation.

Pi (A: U) (B: A -> U): U = (x: A) -> B x

Pi is a dependent function type, the generalization of functions. As a function it can serve the wide range of mathematical constructions, objects, types, or spaces. The known domain and codomain spaces could be: sets, functions, polynomial functors, $\infty$-groupoids, topological $\infty$-groupoid, cw-complexes, categories, languages, etc. We give here immediate isomorphism of Pi types, the fibrations or fiber bundles.

The adjoints Pi and Sigma is not the only adjoints could be presented in type system. Axiomatic cohesions could contain a set of adjoint pairs as a core type checker operations.

Geometrically, Pi type is a space of sections, while the dependent codomain is a space of fibrations. Lambda functions are sections or points in these spaces, while the function result is a fibration. Pi type also represents the cartesian family of sets, generalizing the cartesian product of sets.


Definition (Section). A section of morphism $f: A \rightarrow B$ in some category is the morphism $g: B \rightarrow A$ such that $f \circ g: B \mapright{g} A \mapright{f} B$ equals the identity morphism on B.

Definition (Fiber). The fiber of the map $p: E \rightarrow B$ in a point $y: B$ is all points $x: E$ such that $p(x)=y$.

Definition (Fiber Bundle). The fiber bundle $ F \rightarrow E \mapright{p} B$ on a total space $E$ with fiber layer $F$ and base $B$ is a structure $(F,E,p,B)$ where $p: E \rightarrow B$ is a surjective map with following property: for any point $y: B$ exists a neighborhood $U_b$ for which a homeomorphism $f: p^{-1}(U_b) \rightarrow U_b \times F$ making the following diagram commute.

$$ \begin{array}{ccc} p^{-1}(U_b) & \mapright{f} & U_b \times F \\ \mapdown{\mathbf{p}} & \mapdiagr{pr_1} & \\ U_b & & \\ \end{array} $$

Definition (Cartesian Product of Family over B). Is a set $F$ of sections of the bundle with elimination map $app : F \times B \rightarrow E$. such that

$$ F \times B \mapright{\mathbf{app}} E \mapright{\mathbf{pr_1}} B $$

$pr_1$ is a product projection, so $pr_1$, $app$ are moriphisms of slice category $Set_{/B}$. The universal mapping property of $F$: for all $A$ and morphism $A \times B \rightarrow E$ in $Set_{/B}$ exists unique map $A \rightarrow F$ such that everything commute. So a category with all dependent products is necessarily a category with all pullbacks.

Definition (Trivial Fiber Bundle). When total space $E$ is cartesian product $\Sigma(B,F)$ and $p = pr_1$ then such bundle is called trivial $(F,\Sigma(B,F),pr_1,B)$.

Definition (Dependent Product). The dependent product along morphism $g: B \rightarrow A$ in category $C$ is the right adjoint $\Pi_g : C_{/B} \rightarrow C_{/A}$ of the base change functor.

Definition (Space of Sections). Let $\mathbf{H}$ be a $(\infty,1)$-topos, and let $E \rightarrow B : \mathbf{H}_{/B}$ a bundle in $\mathbf{H}$, object in the slice topos. Then the space of sections $\Gamma_\Sigma(E)$ of this bundle is the Dependent Product:

$$ \Gamma_\Sigma(E) = \Pi_\Sigma (E) \in \mathbf{H}. $$


Lambda constructor defines a new lambda closure that could be saved or passed by in context.

lambda (A B: U) (b: B): A -> B = \ (x: A) -> b lam (A: U) (B: A -> U) (a: A) (b: B a) : A -> B a = \ (x: A) -> b



Application reduces the term by using recursive substitution.

apply (A B: U) (f: A -> B) (x: A): B = f(x) app (A: U) (B: A -> U) (a: A) (f: A -> B a): B a = f a


Composition is using application of appropriate singnatures.

ot (A B C: U) : U = (B -> C) -> (A -> B) -> (A -> C) o (A B C: U) : ot A B C = \ (x: A) -> f (g x) O (F G: U -> U) (t: U): U = F (G t)



Beta rule shows that composition $lam \circ app$ could be fused.

Pi_Beta (A: U) (B: A -> U) (a: A) (f: A -> B a) : Path (B a) (app A B a (lam A B a (f a))) (f a) = refl (B a) (f a)


Eta rule shows that composition $app \circ lam$ could be fused.

Pi_Eta (A: U) (B: A -> U) (a: A) (f: A -> B a) : Path (A -> B a) f (\(x:A) -> f x) = refl (A -> B a) f


Theorem (Functions Preserve Paths). For a function $f: (x:A) \rightarrow B(x)$ there is an $ap_f : Path_A(x,y) \rightarrow Path_{B(x)}(f(x),f(y))$. This is called application of $f$ to path or congruence property (for non-dependent case — $cong$ function). This property behaves functoriality as if paths are groupoid morphisms and types are objects.

Theorem (Trivial Fiber equals Family of Sets). Inverse image (fiber) of fiber bundle $(F,B*F,pr_1,B)$ in point $y:B$ equals $F(y)$.

FiberPi (B: U) (F: B -> U) (y: B) : Path U (fiber (Sigma B F) B (pi1 B F) y) (F y)

Theorem (Homotopy Equivalence). If fiber space is set for all base, and there are two functions $f,g : (x:A) \rightarrow B(x)$ and two homotopies between them, then these homotopies are equal.

setPi (A: U) (B: A -> U) (h: (x: A) -> isSet (B x)) (f g: Pi A B) (p q: Path (Pi A B) f g) : Path (Path (Pi A B) f g) p q

Theorem (HomSet). If codomain is set then space of sections is a set.

setFun (A B : U) (_: isSet B) : isSet (A -> B)

Theorem (Contractability). If domain and codomain is contractible then the space of sections is contractible.

piIsContr (A: U) (B: A -> U) (u: isContr A) (q: (x: A) -> isContr (B x)) : isContr (Pi A B)
pathPi (A:U) (B:A->U) (f g : Pi A B) : Path U (Path (Pi A B) f g) ((x:A) -> Path (B x) (f x) (g x))