started some work on ∏ types
This commit is contained in:
parent
efd7a84631
commit
8e1cc0e551
174
src/CwF.lagda.md
174
src/CwF.lagda.md
|
|
@ -1,175 +1,3 @@
|
|||
---
|
||||
references:
|
||||
- type: article-journal
|
||||
id: abd2008
|
||||
editor:
|
||||
- family: Jacques Carrigue
|
||||
- family: Manuel V. Hermengildo
|
||||
author:
|
||||
- family: Andreas Abel
|
||||
- family: Thierry Coquand
|
||||
- family: Peter Dybjer
|
||||
issued:
|
||||
date-parts:
|
||||
- - 2008
|
||||
title: 'On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory'
|
||||
journal: "Lecture Notes in Computer Science"
|
||||
volume: 4989
|
||||
url: http://link.springer.com/10.1007/978-3-540-78969-7_2
|
||||
page: 3-13
|
||||
language: en-GB
|
||||
- type: book-section
|
||||
id: hoffmann97
|
||||
author:
|
||||
- family: Martin Hoffmann
|
||||
issued:
|
||||
date-parts:
|
||||
- - 1997
|
||||
title: 'Syntax and semantics of dependent types'
|
||||
journal: "Extensional Constructs in Intensional Type Theory"
|
||||
volume: 4989
|
||||
url: https://doi.org/10.1007/978-1-4471-0963-1_2
|
||||
page: 13-54
|
||||
language: en-GB
|
||||
|
||||
citation-style: ./ieee.csl
|
||||
---
|
||||
```
|
||||
open import Cat.Prelude
|
||||
open import Cat.Diagram.Terminal
|
||||
open import Fams
|
||||
|
||||
module CwF where
|
||||
```
|
||||
# Categories with families
|
||||
|
||||
A Category with families, a CwF, is a category in which we can interpret the synax of a type theory. The objects of a CwF are contexts and the morphisms are a list of judgements. The morphisms, being lists of judgements, are able to describe substitution and weakening. For a more detailed introduction to CwFs see the introductory paper by Hoffmann. [@hoffmann97]
|
||||
|
||||
This file defines a CwF, without any particular type formers. Here CwFs are thought of as GATs (generalised algebraic theories), as is presented in a paper by Abel, Coquand and Dybjer. [@abd2008]
|
||||
|
||||
A category $\mathcal C$ is said to be a CwF if there is a contravariant functor $\mathcal F : \mathcal C^{op} \to \mathcal Fam$, and it fufills the laws of the GAT.
|
||||
|
||||
```
|
||||
record is-CwF {o h f : _} (𝓒 : Precategory o h) : Type (lsuc (o ⊔ h ⊔ f)) where
|
||||
field
|
||||
𝓕 : Functor (𝓒 ^op) (Fams f)
|
||||
```
|
||||
|
||||
Two functions, $Ty$ and $Tm$ are defined in terms of $\mathcal F$, giving a context's set of syntactic types, and terms respectively.
|
||||
```
|
||||
open Precategory 𝓒
|
||||
open Functor 𝓕
|
||||
|
||||
Ty : Ob → Set f
|
||||
Ty Γ = F₀ Γ .fst
|
||||
|
||||
Tr : (Γ : Ob) → ∣ Ty Γ ∣ → Set f
|
||||
Tr Γ σ = F₀ Γ .snd σ
|
||||
```
|
||||
|
||||
From functoriality of $\mathcal F$ it can be derived that these support substitution in both types and terms.
|
||||
```
|
||||
_⟦_⟧ : {Δ Γ : Ob} → ∣ Ty Γ ∣ → Hom Δ Γ → ∣ Ty Δ ∣
|
||||
A ⟦ γ ⟧ = F₁ γ .fst A
|
||||
|
||||
_[_] : {Δ Γ : Ob} {A : ∣ Ty Γ ∣} (a : ∣ Tr Γ A ∣)
|
||||
(γ : Hom Δ Γ) → ∣ Tr Δ (A ⟦ γ ⟧) ∣
|
||||
_[_] {_} {_} {A} a γ = F₁ γ .snd A a
|
||||
```
|
||||
|
||||
Likewise, it follows that the substitution operators respect composition and identity.
|
||||
```
|
||||
⟦⟧-compose : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣)
|
||||
→ A ⟦ γ ∘ δ ⟧ ≡ A ⟦ γ ⟧ ⟦ δ ⟧
|
||||
⟦⟧-compose {_} {_} {_} γ δ A i = F-∘ δ γ i .fst A
|
||||
|
||||
⟦⟧-id : {Γ : Ob} (A : ∣ Ty Γ ∣)
|
||||
→ A ⟦ id ⟧ ≡ A
|
||||
⟦⟧-id {Γ} A i = F-id i .fst A
|
||||
```
|
||||
|
||||
Since the terms are indexed by types there will be some commonly used paths between types.
|
||||
```
|
||||
⟦⟧-tr-comp : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣)
|
||||
→ ∣ Tr Θ (A ⟦ γ ∘ δ ⟧) ∣ ≡ ∣ Tr Θ (A ⟦ γ ⟧ ⟦ δ ⟧) ∣
|
||||
⟦⟧-tr-comp {_} {_} {Θ} γ δ A i = ∣ Tr Θ (⟦⟧-compose γ δ A i) ∣
|
||||
|
||||
⟦⟧-tr-id : {Γ : Ob} (A : ∣ Ty Γ ∣)
|
||||
→ ∣ Tr Γ (A ⟦ id ⟧) ∣ ≡ ∣ Tr Γ A ∣
|
||||
⟦⟧-tr-id {Γ} A i = ∣ Tr Γ (⟦⟧-id A i) ∣
|
||||
```
|
||||
|
||||
Using the paths defined above, composition and identity laws for terms can be stated and proven.
|
||||
```
|
||||
[]-compose : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣)
|
||||
{a : ∣ Tr Γ A ∣}
|
||||
→ PathP (λ i → ⟦⟧-tr-comp γ δ A i)
|
||||
(a [ γ ∘ δ ])
|
||||
(a [ γ ] [ δ ])
|
||||
[]-compose {_} {_} {_} γ δ A {a} i = F-∘ δ γ i .snd A a
|
||||
|
||||
[]-id : {Γ : Ob} {A : ∣ Ty Γ ∣} {a : ∣ Tr Γ A ∣}
|
||||
→ PathP (λ i → ⟦⟧-tr-id A i) (a [ id ]) a
|
||||
[]-id {Γ} {A} {a} i = F-id i .snd A a
|
||||
```
|
||||
|
||||
A CwF has a terminal object representing the empty context.
|
||||
```
|
||||
field
|
||||
terminal : Terminal 𝓒
|
||||
```
|
||||
|
||||
For any context $\Gamma$ and $A \in Ty(\Gamma)$ there is a context $\Gamma;A$, extending $\Gamma$ by $A$.
|
||||
```
|
||||
_;_ : (Γ : Ob) → ∣ Ty Γ ∣ → Ob
|
||||
```
|
||||
Thus contexts can be built by repeatedly extending the empty context.
|
||||
|
||||
For any list of judgements between $\Delta$ and $\Gamma$, there should be a weakened version from $\Delta$ to $\Gamma;A$.
|
||||
```
|
||||
⟨_,_⟩ : {Γ Δ : Ob} {A : ∣ Ty Γ ∣} (γ : Hom Δ Γ) (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣ )
|
||||
→ Hom Δ (Γ ; A)
|
||||
```
|
||||
|
||||
For every context $\Gamma$ and $A ∈ Ty(\Gamma)$ there is a projection map $p_{\ \Gamma;A} : \Gamma;A → \Gamma$ and a term $q_{\ \Gamma;A} : Tr(\Gamma;A, A \llbracket p_{\ \Gamma;A}\rrbracket)$.
|
||||
|
||||
```
|
||||
p : {Γ : Ob} {A : ∣ Ty Γ ∣} → Hom (Γ ; A) Γ
|
||||
q : {Γ : Ob} {A : ∣ Ty Γ ∣} → ∣ Tr (Γ ; A) (A ⟦ p ⟧) ∣
|
||||
```
|
||||
|
||||
Dubbing $p$ a projection is no coincidence, it projects a map out of a weakened map.
|
||||
```
|
||||
field
|
||||
p-∘ : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣)
|
||||
→ p ∘ ⟨ γ , a ⟩ ≡ γ
|
||||
```
|
||||
|
||||
Likewise, $q$ "projects" an object out of a weakened substitution.
|
||||
```
|
||||
q-∘-pathp : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣)
|
||||
→ ∣ Tr Δ (A ⟦ p ⟧ ⟦ ⟨ γ , a ⟩ ⟧) ∣ ≡ ∣ Tr Δ (A ⟦ γ ⟧) ∣
|
||||
q-∘-pathp {Δ} {Γ} {γ} {A} a =
|
||||
∣ Tr Δ (A ⟦ p ⟧ ⟦ ⟨ γ , a ⟩ ⟧) ∣ ≡˘⟨ ⟦⟧-tr-comp p ⟨ γ , a ⟩ A ⟩
|
||||
∣ Tr Δ (A ⟦ p ∘ ⟨ γ , a ⟩ ⟧) ∣ ≡⟨ (λ i → ∣ Tr Δ (A ⟦ p-∘ a i ⟧) ∣) ⟩
|
||||
∣ Tr Δ (A ⟦ γ ⟧) ∣ ∎
|
||||
|
||||
field
|
||||
q-∘ : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} {a : ∣ Tr Δ (A ⟦ γ ⟧) ∣}
|
||||
→ PathP (λ i → q-∘-pathp a i)
|
||||
(q [ ⟨ γ , a ⟩ ])
|
||||
a
|
||||
```
|
||||
|
||||
Further motivating the use of the word projection, pairing up the two projections in a weakened map must result in the identity.
|
||||
```
|
||||
pq-id : {Γ : Ob} {A : ∣ Ty Γ ∣} → ⟨ p , q ⟩ ≡ id {Γ ; A}
|
||||
```
|
||||
|
||||
Lastly, it is required that the weakening map behaves as expected under composition.
|
||||
```
|
||||
⟨⟩-∘ : {Δ Γ Θ : Ob} {γ : Hom Γ Δ} {δ : Hom Δ Θ} {A : ∣ Ty Θ ∣}
|
||||
{a : ∣ Tr Δ (A ⟦ δ ⟧) ∣}
|
||||
→ ⟨ δ , a ⟩ ∘ γ
|
||||
≡ ⟨ δ ∘ γ , transport (sym (⟦⟧-tr-comp δ γ A)) (a [ γ ]) ⟩
|
||||
```
|
||||
open import public CwF.Base
|
||||
185
src/CwF/Base.lagda.md
Normal file
185
src/CwF/Base.lagda.md
Normal file
|
|
@ -0,0 +1,185 @@
|
|||
---
|
||||
references:
|
||||
- type: article-journal
|
||||
id: abd2008
|
||||
editor:
|
||||
- family: Jacques Carrigue
|
||||
- family: Manuel V. Hermengildo
|
||||
author:
|
||||
- family: Andreas Abel
|
||||
- family: Thierry Coquand
|
||||
- family: Peter Dybjer
|
||||
issued:
|
||||
date-parts:
|
||||
- - 2008
|
||||
title: 'On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory'
|
||||
journal: "Lecture Notes in Computer Science"
|
||||
volume: 4989
|
||||
url: http://link.springer.com/10.1007/978-3-540-78969-7_2
|
||||
page: 3-13
|
||||
language: en-GB
|
||||
- type: book-section
|
||||
id: hoffmann97
|
||||
author:
|
||||
- family: Martin Hoffmann
|
||||
issued:
|
||||
date-parts:
|
||||
- - 1997
|
||||
title: 'Syntax and semantics of dependent types'
|
||||
journal: "Extensional Constructs in Intensional Type Theory"
|
||||
volume: 4989
|
||||
url: https://doi.org/10.1007/978-1-4471-0963-1_2
|
||||
page: 13-54
|
||||
language: en-GB
|
||||
|
||||
citation-style: ./ieee.csl
|
||||
---
|
||||
```
|
||||
open import Cat.Prelude
|
||||
open import Cat.Diagram.Terminal
|
||||
open import Fams
|
||||
|
||||
module CwF.Base where
|
||||
```
|
||||
# Categories with families
|
||||
|
||||
A Category with families, a CwF, is a category in which we can interpret the synax of a type theory. The objects of a CwF are contexts and the morphisms are a list of judgements. The morphisms, being lists of judgements, are able to describe substitution and weakening. For a more detailed introduction to CwFs see the introductory paper by Hoffmann. [@hoffmann97]
|
||||
|
||||
This file defines a CwF, without any particular type formers. Here CwFs are thought of as GATs (generalised algebraic theories), as is presented in a paper by Abel, Coquand and Dybjer. [@abd2008]
|
||||
|
||||
A category $\mathcal C$ is said to be a CwF if there is a contravariant functor $\mathcal F : \mathcal C^{op} \to \mathcal Fam$, and it fufills the laws of the GAT.
|
||||
|
||||
```
|
||||
record is-CwF {o h f : _} (𝓒 : Precategory o h) : Type (lsuc (o ⊔ h ⊔ f)) where
|
||||
field
|
||||
𝓕 : Functor (𝓒 ^op) (Fams f)
|
||||
```
|
||||
|
||||
Two functions, $Ty$ and $Tm$ are defined in terms of $\mathcal F$, giving a context's set of syntactic types, and terms respectively.
|
||||
```
|
||||
open Precategory 𝓒
|
||||
open Functor 𝓕
|
||||
|
||||
Ty : Ob → Set f
|
||||
Ty Γ = F₀ Γ .fst
|
||||
|
||||
Tr : (Γ : Ob) → ∣ Ty Γ ∣ → Set f
|
||||
Tr Γ σ = F₀ Γ .snd σ
|
||||
```
|
||||
|
||||
From functoriality of $\mathcal F$ it can be derived that these support substitution in both types and terms.
|
||||
```
|
||||
_⟦_⟧ : {Δ Γ : Ob} → ∣ Ty Γ ∣ → Hom Δ Γ → ∣ Ty Δ ∣
|
||||
A ⟦ γ ⟧ = F₁ γ .fst A
|
||||
|
||||
_[_] : {Δ Γ : Ob} {A : ∣ Ty Γ ∣} (a : ∣ Tr Γ A ∣)
|
||||
(γ : Hom Δ Γ) → ∣ Tr Δ (A ⟦ γ ⟧) ∣
|
||||
_[_] {_} {_} {A} a γ = F₁ γ .snd A a
|
||||
```
|
||||
|
||||
Likewise, it follows that the substitution operators respect composition and identity.
|
||||
```
|
||||
⟦⟧-compose : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣)
|
||||
→ A ⟦ γ ∘ δ ⟧ ≡ A ⟦ γ ⟧ ⟦ δ ⟧
|
||||
⟦⟧-compose {_} {_} {_} γ δ A i = F-∘ δ γ i .fst A
|
||||
|
||||
⟦⟧-id : {Γ : Ob} (A : ∣ Ty Γ ∣)
|
||||
→ A ⟦ id ⟧ ≡ A
|
||||
⟦⟧-id {Γ} A i = F-id i .fst A
|
||||
```
|
||||
|
||||
Since the terms are indexed by types there will be some commonly used paths between types.
|
||||
```
|
||||
⟦⟧-tr-comp : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣)
|
||||
→ ∣ Tr Θ (A ⟦ γ ∘ δ ⟧) ∣ ≡ ∣ Tr Θ (A ⟦ γ ⟧ ⟦ δ ⟧) ∣
|
||||
⟦⟧-tr-comp {_} {_} {Θ} γ δ A i = ∣ Tr Θ (⟦⟧-compose γ δ A i) ∣
|
||||
|
||||
⟦⟧-tr-id : {Γ : Ob} (A : ∣ Ty Γ ∣)
|
||||
→ ∣ Tr Γ (A ⟦ id ⟧) ∣ ≡ ∣ Tr Γ A ∣
|
||||
⟦⟧-tr-id {Γ} A i = ∣ Tr Γ (⟦⟧-id A i) ∣
|
||||
```
|
||||
|
||||
Using the paths defined above, composition and identity laws for terms can be stated and proven.
|
||||
```
|
||||
[]-compose : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣)
|
||||
{a : ∣ Tr Γ A ∣}
|
||||
→ PathP (λ i → ⟦⟧-tr-comp γ δ A i)
|
||||
(a [ γ ∘ δ ])
|
||||
(a [ γ ] [ δ ])
|
||||
[]-compose {_} {_} {_} γ δ A {a} i = F-∘ δ γ i .snd A a
|
||||
|
||||
[]-id : {Γ : Ob} {A : ∣ Ty Γ ∣} {a : ∣ Tr Γ A ∣}
|
||||
→ PathP (λ i → ⟦⟧-tr-id A i) (a [ id ]) a
|
||||
[]-id {Γ} {A} {a} i = F-id i .snd A a
|
||||
```
|
||||
|
||||
A CwF has a terminal object representing the empty context.
|
||||
```
|
||||
field
|
||||
terminal : Terminal 𝓒
|
||||
```
|
||||
|
||||
For any context $\Gamma$ and $A \in Ty(\Gamma)$ there is a context $\Gamma;A$, extending $\Gamma$ by $A$.
|
||||
```
|
||||
_;_ : (Γ : Ob) → ∣ Ty Γ ∣ → Ob
|
||||
```
|
||||
Thus contexts can be built by repeatedly extending the empty context.
|
||||
|
||||
For any list of judgements between $\Delta$ and $\Gamma$, there should be a weakened version from $\Delta$ to $\Gamma;A$.
|
||||
```
|
||||
⟨_,_⟩ : {Γ Δ : Ob} {A : ∣ Ty Γ ∣} (γ : Hom Δ Γ) (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣ )
|
||||
→ Hom Δ (Γ ; A)
|
||||
```
|
||||
|
||||
It is often the case that weakening maps will take a composition of morphisms, or an identity morphism, which will cause the second element to no longer have the same type definitionally. These helpers are defined to get around this with transports.
|
||||
```
|
||||
⟨_∘∘_,_⟩ : {Δ Γ Θ : Ob} {A : ∣ Ty Γ ∣} (γ : Hom Δ Γ)
|
||||
(δ : Hom Θ Δ) → (a : ∣ Tr Θ (A ⟦ γ ⟧ ⟦ δ ⟧) ∣ ) → Hom Θ (Γ ; A)
|
||||
⟨_∘∘_,_⟩ {_} {_} {Θ} {A} γ δ a = ⟨ γ ∘ δ , transport (λ i → ⟦⟧-tr-comp γ δ A (~ i)) a ⟩
|
||||
|
||||
⟨id,_⟩ : {Γ : Ob} {A : ∣ Ty Γ ∣} (a : ∣ Tr Γ A ∣) → Hom Γ (Γ ; A)
|
||||
⟨id,_⟩ {_} {A} a = ⟨ id , transport (λ i → ⟦⟧-tr-id A (~ i)) a ⟩
|
||||
```
|
||||
|
||||
For every context $\Gamma$ and $A ∈ Ty(\Gamma)$ there is a projection map $p_{\ \Gamma;A} : \Gamma;A → \Gamma$ and a term $q_{\ \Gamma;A} : Tr(\Gamma;A, A \llbracket p_{\ \Gamma;A}\rrbracket)$.
|
||||
|
||||
```
|
||||
field
|
||||
p : {Γ : Ob} {A : ∣ Ty Γ ∣} → Hom (Γ ; A) Γ
|
||||
q : {Γ : Ob} {A : ∣ Ty Γ ∣} → ∣ Tr (Γ ; A) (A ⟦ p ⟧) ∣
|
||||
```
|
||||
|
||||
Dubbing $p$ a projection is no coincidence, it projects a map out of a weakened map.
|
||||
```
|
||||
field
|
||||
p-∘ : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣)
|
||||
→ p ∘ ⟨ γ , a ⟩ ≡ γ
|
||||
```
|
||||
|
||||
Likewise, $q$ "projects" an object out of a weakened substitution.
|
||||
```
|
||||
q-∘-pathp : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣)
|
||||
→ ∣ Tr Δ (A ⟦ p ⟧ ⟦ ⟨ γ , a ⟩ ⟧) ∣ ≡ ∣ Tr Δ (A ⟦ γ ⟧) ∣
|
||||
q-∘-pathp {Δ} {Γ} {γ} {A} a =
|
||||
∣ Tr Δ (A ⟦ p ⟧ ⟦ ⟨ γ , a ⟩ ⟧) ∣ ≡˘⟨ ⟦⟧-tr-comp p ⟨ γ , a ⟩ A ⟩
|
||||
∣ Tr Δ (A ⟦ p ∘ ⟨ γ , a ⟩ ⟧) ∣ ≡⟨ (λ i → ∣ Tr Δ (A ⟦ p-∘ a i ⟧) ∣) ⟩
|
||||
∣ Tr Δ (A ⟦ γ ⟧) ∣ ∎
|
||||
|
||||
field
|
||||
q-∘ : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} {a : ∣ Tr Δ (A ⟦ γ ⟧) ∣}
|
||||
→ PathP (λ i → q-∘-pathp a i)
|
||||
(q [ ⟨ γ , a ⟩ ])
|
||||
a
|
||||
```
|
||||
|
||||
Further motivating the use of the word projection, pairing up the two projections in a weakened map must result in the identity.
|
||||
```
|
||||
pq-id : {Γ : Ob} {A : ∣ Ty Γ ∣} → ⟨ p , q ⟩ ≡ id {Γ ; A}
|
||||
```
|
||||
|
||||
Lastly, it is required that the weakening map behaves as expected under composition.
|
||||
```
|
||||
⟨⟩-∘ : {Δ Γ Θ : Ob} {γ : Hom Γ Δ} {δ : Hom Δ Θ} {A : ∣ Ty Θ ∣}
|
||||
{a : ∣ Tr Δ (A ⟦ δ ⟧) ∣}
|
||||
→ ⟨ δ , a ⟩ ∘ γ ≡ ⟨ δ ∘∘ γ , a [ γ ] ⟩
|
||||
```
|
||||
74
src/CwF/Structures.lagda.md
Normal file
74
src/CwF/Structures.lagda.md
Normal file
|
|
@ -0,0 +1,74 @@
|
|||
```
|
||||
open import Cat.Prelude
|
||||
open import CwF.Base
|
||||
|
||||
module CwF.Structures where
|
||||
```
|
||||
|
||||
This file defines several additional structures a CwF might have, such as Pi types, universes, sigma types, and identity types.
|
||||
|
||||
First are Pi types, because a type theory without them are pretty uninteresting.
|
||||
```
|
||||
record has-Pi {o h f : _} {𝓒 : Precategory o h}
|
||||
(cwf : is-CwF {o} {h} {f} 𝓒) : Type (lsuc (o ⊔ h ⊔ f)) where
|
||||
open Precategory 𝓒
|
||||
open is-CwF cwf
|
||||
field
|
||||
```
|
||||
|
||||
The type formation rule for pi types is straight forward.
|
||||
```
|
||||
∏ : {Γ : Ob} (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣) → ∣ Ty Γ ∣
|
||||
```
|
||||
|
||||
Likewise, the introduction rule is what one would expect.
|
||||
```
|
||||
Cλ : {Γ : Ob} (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣) (b : ∣ Tr (Γ ; A) B ∣)
|
||||
→ ∣ Tr Γ (∏ A B) ∣
|
||||
```
|
||||
|
||||
Application also needs to be introduced.
|
||||
```
|
||||
app : {Γ : Ob} {A : ∣ Ty Γ ∣} {B : ∣ Ty (Γ ; A) ∣} (f : ∣ Tr Γ (∏ A B) ∣)
|
||||
(x : ∣ Tr Γ A ∣) → ∣ Tr Γ (B ⟦ ⟨id, x ⟩ ⟧ ) ∣
|
||||
```
|
||||
|
||||
Substitution must also be closed under all of these.
|
||||
|
||||
```
|
||||
∏-subst : {Δ Γ : Ob} (γ : Hom Δ Γ) (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣)
|
||||
→ ∏ A B ⟦ γ ⟧
|
||||
≡ ∏ (A ⟦ γ ⟧) (B ⟦ ⟨ γ ∘∘ p , q ⟩ ⟧)
|
||||
|
||||
Cλ-subst : {Δ Γ : Ob} (γ : Hom Δ Γ) (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣)
|
||||
(b : ∣ Tr (Γ ; A) B ∣)
|
||||
→ PathP (λ i → ∣ Tr Δ (∏-subst γ A B i) ∣)
|
||||
(Cλ A B b [ γ ])
|
||||
(Cλ (A ⟦ γ ⟧) (B ⟦ ⟨ γ ∘∘ p , q ⟩ ⟧) (b [ ⟨ γ ∘∘ p , q ⟩ ]))
|
||||
```
|
||||
|
||||
There's quite a hefty pathp here...
|
||||
typeof app (transport (λ i → ∣ Tr Δ (∏-subst γ A B i) ∣) (f [ γ ])) (x [ γ ])
|
||||
B ⟦ ⟨ γ ∘ p , q ⟩ ⟧ ⟦ ⟨id, x [ γ ] ⟩ ⟧
|
||||
B ⟦ ⟨ γ ∘ p , q ⟩ ∘ ⟨id, x [ γ ] ⟩ ⟧
|
||||
B ⟦ ⟨ γ ∘ p ∘ ⟨id, x [ γ ] ⟩, q [ ⟨id, x [ γ ] ⟩ ] ⟩ ⟧
|
||||
B ⟦ ⟨ γ ∘ id, x [ γ ] ⟩ ⟧
|
||||
B ⟦ ⟨ id ∘ γ , x [ γ ] ⟩ ⟧
|
||||
B ⟦ ⟨ id, x ⟩ ⟧ ⟦ γ ⟧
|
||||
typeof app f x [ γ ]
|
||||
|
||||
```
|
||||
|
||||
app-subst : {Δ Γ : Ob} (γ : Hom Δ Γ) {A : ∣ Ty Γ ∣} {B : ∣ Ty (Γ ; A) ∣}
|
||||
(f : ∣ Tr Γ (∏ A B) ∣) (x : ∣ Tr Γ A ∣)
|
||||
→ PathP {! !}
|
||||
(app f x [ γ ])
|
||||
(app (transport (λ i → ∣ Tr Δ (∏-subst γ A B i) ∣) (f [ γ ])) (x [ γ ]))
|
||||
```
|
||||
|
||||
Lastly comes the star of the show, $\beta$ reduction.
|
||||
```
|
||||
Cβ : {Γ : Ob} (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣) (b : ∣ Tr (Γ ; A) B ∣)
|
||||
(a : ∣ Tr Γ A ∣)
|
||||
→ app (Cλ A B b) a ≡ b [ ⟨id, a ⟩ ]
|
||||
```
|
||||
Loading…
Reference in New Issue
Block a user