[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents \section{Function extensionality from interval type} I feel that one just uses more transport to prove function extensionality without judgmental computation rules. \section{Test 2} Given a type $A$, elements $a:A$ and $b:A$, and identity $q:a =_A b$, let us define the function $f:\mathbb{I} \to A$ from an [[interval type]] $\mathbb{I}$ to $A$ by * $\beta_f^0:f(0) =_A a$ * $\beta_f^1:f(1) =_A b$ * $\beta_f^p:\mathrm{ap}_f(p) =_{f(0) =_A f(1)} \mathrm{concat}_{f(0), b, f(1)}(\mathrm{concat}_{f(0), a, b}(\beta_f^0, q), \mathrm{inv}_{f(1), b}(\beta_f^1))$ Now, time for the dependent functions... Given a type $A$, a dependent type $x:A \vdash B$, elements $a_0:A$ and $a_1:A$, identity $q:a_0 =_A a_1$, elements $b_0:B[a_0/x]$ and $b_1:B[a_1/x]$, and dependent identity $r:\mathrm{trans}_B^q(b_0) =_B[a_1/x] b_1$, let us define the function $f:\prod_{x:\mathbb{I}} B(x)$ by * $\beta_f^0:f(0) =_{B[a_0/x]} b_0$ * $\beta_f^1:f(1) =_{B[a_1/x]} b_1$ * $\beta_f^p:\mathrm{apd}_f(p) =_{\mathrm{trans}_B^q(f(0)) =_{B[a_1/x]} f(1)} \mathrm{concat}_{\mathrm{trans}_B^q(f(0)), b_1, f(1)}(\mathrm{concat}_{\mathrm{trans}_B^q(f(0)), \mathrm{trans}_B^q(b_0), b_1}(\mathrm{apd}_{\mathrm{trans}_B^q}(\beta_f^0), q), \mathrm{inv}_{f(1), b}(\beta_f^1))$ \section{Test} Literal basic stuff about high school algebra: * What is a variable? * What are free and bound variables? * What is substitution of terms for variables? \section{Variables} A variable is a symbol $x$ which represents an arbitrary instantiation of a type $T$. Variables are thus types and written as $x:T$. Variables are usually found in the context, as $\Gamma, x:T, \Delta \vdash \mathcal{J}$ for arbitrary judgment $\mathcal{J}$. \section{Free and bound variables} \section{Substitution} \section{Change of bound variables} category: redirected to nlab