[proofplan] The projections from a Sigma type are defined by Sigma elimination, equivalently by pattern matching on dependent pairs. The Sigma computation rule says that a function defined by this eliminator reduces on an introduced pair by substituting the displayed components. Applying that computation rule first to the constant motive returning the first component and then to the dependent motive returning the second component gives the two projection beta rules. [/proofplan] [step:Declare the Sigma type and its two projection maps] Let $A$ be a type, let $B:A\to\mathsf{Type}$ be a dependent type family, let $a:A$, and let $b:B(a)$. Define the Sigma type \begin{align*} \Sigma_B \coloneqq \sum_{x:A}B(x). \end{align*} The pair constructor gives a term $(a,b):\Sigma_B$. The first projection is the map \begin{align*} \pi_1:\Sigma_B\to A. \end{align*} It is defined by Sigma elimination with the defining clause $\pi_1((x,y))\coloneqq x$ for $x:A$ and $y:B(x)$. The second projection is the dependent map \begin{align*} \pi_2:\prod_{p:\Sigma_B}B(\pi_1(p)). \end{align*} It is defined by Sigma elimination with the defining clause $\pi_2((x,y))\coloneqq y$ for $x:A$ and $y:B(x)$. [/step] [step:Apply the Sigma computation rule to the first projection] By the Sigma type computation rule from [citetheorem:9631], a term defined by Sigma elimination reduces on an introduced pair by substituting the pair components into its defining clause. Applying this rule to the definition of $\pi_1$ at the pair $(a,b)$ gives \begin{align*} \pi_1((a,b)) \equiv a : A. \end{align*} [guided] We now use the beta computation rule for Sigma elimination. The relevant rule says: if a function out of $\sum_{x:A}B(x)$ is defined by specifying its value on a general pair $(x,y)$, then evaluating that function on the introduced pair $(a,b)$ judgmentally reduces by replacing $x$ with $a$ and $y$ with $b$. For the first projection, the defining clause is \begin{align*} \pi_1((x,y))\coloneqq x. \end{align*} Here the motive is the constant family with value $A$, so the eliminator indeed produces a map $\pi_1:\Sigma_B\to A$. Substituting the components of the particular pair $(a,b)$ into the displayed clause gives \begin{align*} \pi_1((a,b)) \equiv a : A. \end{align*} This is a judgmental equality because it is exactly the computation rule attached to the Sigma eliminator, not a separate proposition proved by induction. [/guided] [/step] [step:Apply the Sigma computation rule to the second projection] Again by the Sigma type computation rule from [citetheorem:9631], applying the eliminator defining $\pi_2$ to the introduced pair $(a,b)$ substitutes $a$ and $b$ into the defining clause for $\pi_2$. Hence \begin{align*} \pi_2((a,b)) \equiv b : B(a). \end{align*} Together with the previous step, this proves the two Sigma beta rules. If the ambient presentation records equalities propositionally, the displayed judgmental equalities yield identity terms by reflexivity, so the corresponding propositional equalities also follow. [/step]