wip

Author: 5HT

foundations/mltt/pi/index.pug

@@ -80,8 +80,8 @@ block content
                 h2 Elimination
 
                 +tex.
-                    $\mathbf{Definition\ 1.3}$ ($\Pi$-Induction Principle). States that
-                    if predicate holds for lambda function
+                    $\mathbf{Definition\ 1.3}$ ($\Pi$-Induction Principle).
+                    States that if predicate holds for lambda function
                     then there is a function from function space to the space of predicate.
                 +code.
                     def П-ind (A : U) (B : A -> U)
@@ -190,8 +190,8 @@ block content
                 br.
 
                 +tex.
-                    $\mathbf{Theorem\ 1.10}$ (Contractability). If domain and codomain is contractible then
-                    the space of sections is contractible.
+                    $\mathbf{Theorem\ 1.10}$ (Contractability).
+                    If domain and codomain is contractible then the space of sections is contractible.
 
                 +code.
                     def piIsContr (A: U) (B: A -> U) (u: isContr A)

foundations/mltt/sigma/index.pug

@@ -34,8 +34,8 @@ block content
             h2 Formation
 
             +tex.
-                $\mathbf{Definition\ 2.1}$ ($\Sigma$-Formation, Dependent Sum). The dependent sum
-                type is indexed over type $A$ in the sense of coproduct or disjoint union,
+                $\mathbf{Definition\ 2.1}$ ($\Sigma$-Formation, Dependent Sum).
+                The dependent sum type is indexed over type $A$ in the sense of coproduct or disjoint union,
                 where only one fiber codomain $B(x)$ is present in pair.
             +tex(true).
                 $$