progress
This commit is contained in:
parent
5c35f42baf
commit
87ab99506c
7 changed files with 294 additions and 92 deletions
7
Makefile
7
Makefile
|
|
@ -1,7 +1,12 @@
|
|||
GENDIR := html/src/generated
|
||||
build-to-html:
|
||||
find src/HottBook \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \
|
||||
| rust-parallel -0 agda --html --html-dir=$(GENDIR) --html-highlight=auto || true
|
||||
| rust-parallel -0 agda \
|
||||
--html \
|
||||
--html-dir=$(GENDIR) \
|
||||
--allow-unsolved-metas \
|
||||
--html-highlight=auto \
|
||||
|| true
|
||||
fd --no-ignore "html$$" $(GENDIR) -x rm
|
||||
|
||||
deploy: build-to-html
|
||||
|
|
|
|||
4
html/.gitignore
vendored
4
html/.gitignore
vendored
|
|
@ -1,3 +1,5 @@
|
|||
book
|
||||
src/generated/*
|
||||
!src/generated/.gitkeep
|
||||
!src/generated/.gitkeep
|
||||
theme/pagetoc.css
|
||||
theme/pagetoc.js
|
||||
|
|
@ -5,5 +5,8 @@ multilingual = false
|
|||
src = "src"
|
||||
title = "HoTT Book"
|
||||
|
||||
[preprocessor.pagetoc]
|
||||
|
||||
[output.html]
|
||||
additional-css = ["src/generated/Agda.css", "style.css"]
|
||||
additional-js = ["theme/pagetoc.js"]
|
||||
additional-css = ["src/generated/Agda.css", "style.css", "theme/pagetoc.css"]
|
||||
|
|
|
|||
|
|
@ -1,13 +1,11 @@
|
|||
|
||||
@font-face {
|
||||
font-family: "PragmataPro Mono Liga";
|
||||
src:
|
||||
url("/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2") format("woff2"),
|
||||
url("https://mzhang.io/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2")
|
||||
format("woff2");
|
||||
}
|
||||
|
||||
font-family: "PragmataPro Mono Liga";
|
||||
src:
|
||||
url("/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2") format("woff2"),
|
||||
url("https://mzhang.io/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2")
|
||||
format("woff2");
|
||||
}
|
||||
|
||||
pre.Agda {
|
||||
font-family: "PragmataPro Mono Liga", monospace;
|
||||
font-family: "PragmataPro Mono Liga", monospace;
|
||||
}
|
||||
|
|
@ -12,6 +12,11 @@ open import Agda.Primitive
|
|||
|
||||
## 1.4 Dependent function types (Π-types)
|
||||
|
||||
```
|
||||
id : {l : Level} {A : Set l} → A → A
|
||||
id x = x
|
||||
```
|
||||
|
||||
## 1.5 Product types
|
||||
|
||||
```
|
||||
|
|
@ -153,6 +158,8 @@ composite : {A B C : Set}
|
|||
→ A → C
|
||||
composite f g x = g (f x)
|
||||
|
||||
-- https://agda.github.io/agda-stdlib/master/Function.Base.html
|
||||
infixr 9 _∘_
|
||||
_∘_ : {l : Level} {A B C : Set l}
|
||||
→ (g : B → C)
|
||||
→ (f : A → B)
|
||||
|
|
|
|||
|
|
@ -13,12 +13,16 @@ open import HottBook.Util
|
|||
|
||||
## 2.1 Types are higher groupoids
|
||||
|
||||
### Lemma 2.1.1
|
||||
|
||||
```
|
||||
sym : {l : Level} {A : Set l} {x y : A}
|
||||
→ (x ≡ y) → y ≡ x
|
||||
sym {l} {A} {x} {y} p = J (λ x y p → y ≡ x) (λ x → refl) x y p
|
||||
```
|
||||
|
||||
### Lemma 2.1.2
|
||||
|
||||
```
|
||||
trans : {l : Level} {A : Set l} {x y z : A}
|
||||
→ (x ≡ y)
|
||||
|
|
@ -32,6 +36,78 @@ trans {l} {A} {x} {y} {z} p q =
|
|||
_∙_ = trans
|
||||
```
|
||||
|
||||
### Equational Reasoning
|
||||
|
||||
```
|
||||
module ≡-Reasoning where
|
||||
infix 1 begin_
|
||||
begin_ : {A : Set} {x y : A} → (x ≡ y) → (x ≡ y)
|
||||
begin x = x
|
||||
|
||||
_≡⟨⟩_ : {A : Set} (x {y} : A) → x ≡ y → x ≡ y
|
||||
_ ≡⟨⟩ x≡y = x≡y
|
||||
|
||||
infixr 2 _≡⟨⟩_ step-≡
|
||||
step-≡ : {A : Set} (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
|
||||
step-≡ _ y≡z x≡y = trans x≡y y≡z
|
||||
syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z
|
||||
|
||||
infix 3 _∎
|
||||
_∎ : {A : Set} (x : A) → (x ≡ x)
|
||||
_ ∎ = refl
|
||||
```
|
||||
|
||||
### Lemma 2.1.4
|
||||
|
||||
```
|
||||
record lemma2∙1∙4-statement {A : Set} {x y z w : A}
|
||||
(p : x ≡ y) (q : y ≡ z) (r : z ≡ w) : Set where
|
||||
field
|
||||
i1 : p ≡ p ∙ refl
|
||||
i2 : p ≡ refl ∙ p
|
||||
ii1 : (sym p) ∙ p ≡ refl
|
||||
ii2 : p ∙ (sym p) ≡ refl
|
||||
iii : sym (sym p) ≡ p
|
||||
iv : p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
|
||||
|
||||
lemma2∙1∙4 : {A : Set} {x y z w : A}
|
||||
→ (p : x ≡ y)
|
||||
→ (q : y ≡ z)
|
||||
→ (r : z ≡ w)
|
||||
→ lemma2∙1∙4-statement p q r
|
||||
```
|
||||
|
||||
(Proof appears below ap)
|
||||
|
||||
### Definition 2.1.7 (pointed type)
|
||||
|
||||
This comes first, since it is needed to define Theorem 2.1.6.
|
||||
|
||||
```
|
||||
record pointed (l : Level) : Set (lsuc l) where
|
||||
eta-equality
|
||||
constructor mkPointed
|
||||
field
|
||||
A : Set l
|
||||
a : A
|
||||
```
|
||||
|
||||
### Definition 2.1.8 (loop space)
|
||||
|
||||
```
|
||||
Ω : {l : Level} → pointed l → pointed l
|
||||
Ω (mkPointed A a) = mkPointed (a ≡ a) refl
|
||||
```
|
||||
|
||||
### Theorem 2.1.6 (Eckmann-Hilton)
|
||||
|
||||
TODO
|
||||
|
||||
```
|
||||
Ω² : {l : Level} → pointed l → pointed l
|
||||
Ω² p = Ω (Ω p)
|
||||
```
|
||||
|
||||
## 2.2 Functions are functors
|
||||
|
||||
### Lemma 2.2.1
|
||||
|
|
@ -44,6 +120,43 @@ ap : {l : Level} {A B : Set l} {x y : A}
|
|||
ap {l} {A} {B} {x} {y} f p = J (λ x y p → f x ≡ f y) (λ x → refl) x y p
|
||||
```
|
||||
|
||||
<details>
|
||||
<summary>Proof of Lemma 2.1.4</summary>
|
||||
|
||||
```
|
||||
|
||||
lemma2∙1∙4 {A} {x} {y} {z} {w} p q r =
|
||||
let
|
||||
i2 : (x y : A) (p : x ≡ y) → p ≡ refl ∙ p
|
||||
i2 x y p = J (λ x y p → p ≡ refl ∙ p) (λ _ → refl) x y p
|
||||
in record
|
||||
{ i1 = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p
|
||||
; i2 = i2 x y p
|
||||
; ii1 = J (λ x y p → (sym p) ∙ p ≡ refl) (λ _ → refl) x y p
|
||||
; ii2 = J (λ x y p → p ∙ (sym p) ≡ refl) (λ _ → refl) x y p
|
||||
; iii = J (λ x y p → sym (sym p) ≡ p) (λ _ → refl) x y p
|
||||
; iv =
|
||||
let
|
||||
C : (x y : A) → (p : x ≡ y) → Set
|
||||
C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
|
||||
|
||||
wtf : (x : A) (q1 : x ≡ z) → (q1 ∙ r) ≡ (refl ∙ (q1 ∙ r))
|
||||
wtf x q1 = i2 x w (q1 ∙ r)
|
||||
|
||||
wtf2 : (x : A) (q1 : x ≡ z) → q1 ≡ (refl ∙ q1)
|
||||
wtf2 x q1 = i2 x z q1
|
||||
|
||||
wtf3 : (x : A) (q1 : x ≡ z) → (q1 ∙ r) ≡ ((refl ∙ q1) ∙ r)
|
||||
wtf3 x q1 = ap (λ x → x ∙ r) (wtf2 x q1)
|
||||
|
||||
c : (x : A) → C x x refl
|
||||
c x q1 = trans (sym (wtf x q1)) (wtf3 x q1)
|
||||
in J C c x y p q
|
||||
}
|
||||
```
|
||||
|
||||
</details>
|
||||
|
||||
## 2.3 Type families are fibrations
|
||||
|
||||
### Lemma 2.3.1 (Transport)
|
||||
|
|
@ -118,23 +231,22 @@ lemma2∙3∙8 {l} {A} {B} f {x} {y} p =
|
|||
### Lemma 2.3.9
|
||||
|
||||
```
|
||||
-- lemma239 : {A : Set} {P : A → Set} {x y z : A}
|
||||
-- → (p : x ≡ y) → (q : y ≡ z) → (u : P x)
|
||||
-- → transport P q (transport P p u) ≡ transport P (p ∙ q) u
|
||||
-- lemma239 {A} {P} p q u =
|
||||
-- let
|
||||
-- inner : transport P refl (transport P p u) ≡ transport P p u
|
||||
-- inner = refl
|
||||
|
||||
-- ok : p ∙ refl ≡ p
|
||||
-- ok = J (λ _ r → r ∙ refl ≡ r) p refl
|
||||
|
||||
-- bruh : transport P (p ∙ refl) u ≡ transport P p u
|
||||
-- bruh = ap (λ r → transport P r u) ok
|
||||
-- in
|
||||
-- J (λ _ what →
|
||||
-- transport P what (transport P p u) ≡ transport P (p ∙ what) u
|
||||
-- ) q (inner ∙ sym bruh)
|
||||
lemma2∙3∙9 : {A : Set}
|
||||
→ {x y z : A}
|
||||
→ (P : A → Set)
|
||||
→ (p : x ≡ y) → (q : y ≡ z) → (u : P x)
|
||||
→ transport P q (transport P p u) ≡ transport P (p ∙ q) u
|
||||
lemma2∙3∙9 {A} {x} {y} {z} P p q u =
|
||||
let
|
||||
f2 : (x1 : A) → (q1 : x1 ≡ z) (u1 : P x1) → transport P q1 u1 ≡ transport P (refl ∙ q1) u1
|
||||
f2 x1 q1 u1 =
|
||||
let
|
||||
properties = lemma2∙1∙4 q1 refl refl
|
||||
property = lemma2∙1∙4-statement.i2 properties
|
||||
in
|
||||
ap (λ x → transport P x u1) property
|
||||
f1 = J (λ x1 y1 p1 → (q1 : y1 ≡ z) → (u1 : P x1) → transport P q1 (transport P p1 u1) ≡ transport P (p1 ∙ q1) u1) f2 x y p
|
||||
in f1 q u
|
||||
```
|
||||
|
||||
### Lemma 2.3.10
|
||||
|
|
@ -186,16 +298,16 @@ Homotopy forms an equivalence relation:
|
|||
∼-refl f x = refl
|
||||
|
||||
∼-sym : {A : Set} {P : A → Set}
|
||||
→ (f g : (x : A) → P x)
|
||||
→ {f g : (x : A) → P x}
|
||||
→ f ∼ g → g ∼ f
|
||||
∼-sym f g f∼g x = sym (f∼g x)
|
||||
∼-sym {f} {g} f∼g x = sym (f∼g x)
|
||||
|
||||
∼-trans : {A : Set} {P : A → Set}
|
||||
→ (f g h : (x : A) → P x)
|
||||
∼-trans : {l : Level} {A : Set l} {P : A → Set l}
|
||||
→ {f g h : (x : A) → P x}
|
||||
→ f ∼ g
|
||||
→ g ∼ h
|
||||
→ f ∼ h
|
||||
∼-trans f g h f∼g g∼h x = f∼g x ∙ g∼h x
|
||||
∼-trans {l} {A} {P} {f} {g} {h} f∼g g∼h x = f∼g x ∙ g∼h x
|
||||
```
|
||||
|
||||
### Lemma 2.4.3
|
||||
|
|
@ -214,31 +326,55 @@ record qinv {l : Level} {A B : Set l} (f : A → B) : Set l where
|
|||
constructor mkQinv
|
||||
field
|
||||
g : B → A
|
||||
α : f ∘ g ∼ id
|
||||
β : g ∘ f ∼ id
|
||||
α : (f ∘ g) ∼ id
|
||||
β : (g ∘ f) ∼ id
|
||||
```
|
||||
|
||||
### Example 2.4.7
|
||||
|
||||
```
|
||||
id-qinv : {l : Level} {A : Set l} → qinv {l} {A} id
|
||||
id-qinv = record
|
||||
{ g = id
|
||||
; α = λ _ → refl
|
||||
; β = λ _ → refl
|
||||
}
|
||||
id-qinv = mkQinv id (λ _ → refl) (λ _ → refl)
|
||||
```
|
||||
|
||||
### Example 2.4.8
|
||||
|
||||
```
|
||||
|
||||
```
|
||||
|
||||
### Example 2.4.9
|
||||
|
||||
```
|
||||
transport-qinv : {A : Set}
|
||||
→ {x y : A}
|
||||
→ (P : A → Set)
|
||||
→ (p : x ≡ y)
|
||||
→ qinv (transport P p)
|
||||
transport-qinv P p = mkQinv (transport P (sym p))
|
||||
(λ py →
|
||||
let wtf = lemma2∙3∙9 P (sym p) p py in
|
||||
let properties = lemma2∙1∙4 p refl refl in
|
||||
let property = lemma2∙1∙4-statement.ii1 properties in
|
||||
trans wtf (ap (λ x → transport P x py) property))
|
||||
(λ px →
|
||||
let wtf = lemma2∙3∙9 P p (sym p) px in
|
||||
let properties = lemma2∙1∙4 p refl refl in
|
||||
let property = lemma2∙1∙4-statement.ii2 properties in
|
||||
trans wtf (ap (λ x → transport P x px) property))
|
||||
```
|
||||
|
||||
### Definition 2.4.10
|
||||
|
||||
```
|
||||
record isequiv {l : Level} {A B : Set l} (f : A → B) : Set l where
|
||||
eta-equality
|
||||
constructor mkIsEquiv
|
||||
field
|
||||
g : B → A
|
||||
g-id : f ∘ g ∼ id
|
||||
g-id : (f ∘ g) ∼ id
|
||||
h : B → A
|
||||
h-id : h ∘ f ∼ id
|
||||
h-id : (h ∘ f) ∼ id
|
||||
```
|
||||
|
||||
```
|
||||
|
|
@ -246,12 +382,25 @@ qinv-to-isequiv : {l : Level} {A B : Set l}
|
|||
→ {f : A → B}
|
||||
→ qinv f
|
||||
→ isequiv f
|
||||
qinv-to-isequiv q = record
|
||||
{ g = qinv.g q
|
||||
; g-id = qinv.α q
|
||||
; h = qinv.g q
|
||||
; h-id = qinv.β q
|
||||
}
|
||||
qinv-to-isequiv (mkQinv g α β) = mkIsEquiv g α g β
|
||||
```
|
||||
|
||||
Still kinda shaky on this one, TODO study it later:
|
||||
|
||||
```
|
||||
isequiv-to-qinv : {l : Level} {A B : Set l}
|
||||
→ {f : A → B}
|
||||
→ isequiv f
|
||||
→ qinv f
|
||||
isequiv-to-qinv {l} {A} {B} {f} (mkIsEquiv g g-id h h-id) =
|
||||
let
|
||||
γ : g ∼ h
|
||||
γ x = (sym (h-id (g x))) ∙ ap h (g-id x)
|
||||
|
||||
β : (g ∘ f) ∼ id
|
||||
β x = γ (f x) ∙ h-id x
|
||||
in
|
||||
mkQinv g g-id β
|
||||
```
|
||||
|
||||
### Definition 2.4.11
|
||||
|
|
@ -261,6 +410,49 @@ _≃_ : {l : Level} → (A B : Set l) → Set l
|
|||
A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
|
||||
```
|
||||
|
||||
### Lemma 2.4.12
|
||||
|
||||
```
|
||||
id-equiv : (A : Set) → A ≃ A
|
||||
id-equiv A = id , e
|
||||
where
|
||||
e : isequiv id
|
||||
e = mkIsEquiv id (λ _ → refl) id (λ _ → refl)
|
||||
|
||||
sym-equiv : {A B : Set} → (f : A ≃ B) → B ≃ A
|
||||
sym-equiv {A} {B} (f , eqv) =
|
||||
let (mkQinv g α β) = isequiv-to-qinv eqv
|
||||
in g , qinv-to-isequiv (mkQinv f β α)
|
||||
|
||||
trans-equiv : {A B C : Set} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
|
||||
trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) =
|
||||
let
|
||||
(mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
|
||||
(mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv
|
||||
|
||||
open ≡-Reasoning
|
||||
|
||||
forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id
|
||||
forward c =
|
||||
begin
|
||||
((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩
|
||||
(g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩
|
||||
(g ∘ id ∘ g-inv) c ≡⟨⟩
|
||||
(g ∘ g-inv) c ≡⟨ g-inv-left c ⟩
|
||||
id c ∎
|
||||
|
||||
backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id
|
||||
backward a =
|
||||
begin
|
||||
((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩
|
||||
(f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩
|
||||
(f-inv ∘ (id ∘ f)) a ≡⟨⟩
|
||||
(f-inv ∘ f) a ≡⟨ f-inv-right a ⟩
|
||||
id a ∎
|
||||
|
||||
in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)
|
||||
```
|
||||
|
||||
## 2.7 Σ-types
|
||||
|
||||
### Theorem 2.7.2
|
||||
|
|
@ -280,10 +472,10 @@ theorem2∙7∙2 {l} {A} {P} (w @ (w1 , w2)) (w' @ (w'1 , w'2)) =
|
|||
g : Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2) → (w ≡ w')
|
||||
g (refl , refl) = refl
|
||||
|
||||
forwards : f ∘ g ∼ id
|
||||
forwards : (f ∘ g) ∼ id
|
||||
forwards (refl , refl) = refl
|
||||
|
||||
backwards : g ∘ f ∼ id
|
||||
backwards : (g ∘ f) ∼ id
|
||||
backwards refl = refl
|
||||
```
|
||||
|
||||
|
|
@ -352,44 +544,16 @@ postulate
|
|||
### Lemma 2.10.1
|
||||
|
||||
```
|
||||
-- idToEquiv : {A B : Set}
|
||||
-- → (A ≡ B)
|
||||
-- → A ≃ B
|
||||
-- idToEquiv {A} {B} p = func , equiv
|
||||
-- where
|
||||
-- func : A → B
|
||||
-- func a = transport id p a
|
||||
idtoeqv : {l : Level} {A B : Set l}
|
||||
→ (A ≡ B)
|
||||
→ (A ≃ B)
|
||||
idtoeqv {l} {A} {B} p = J C c A B p
|
||||
where
|
||||
C : (x y : Set l) (p : x ≡ y) → Set l
|
||||
C x y p = x ≃ y
|
||||
|
||||
-- func-inv : B → A
|
||||
-- func-inv b = transport id (sym p) b
|
||||
|
||||
-- p* : A → B
|
||||
-- p* = transport id p
|
||||
|
||||
-- wtf3 : A → A
|
||||
-- wtf3 = J (λ A' B' p' → A → A') (λ A' → {! id !}) A B p
|
||||
|
||||
-- wtf3-is-id : wtf3 ∼ id
|
||||
-- wtf3-is-id x = {! !}
|
||||
|
||||
-- wtf3-qinv : qinv wtf3
|
||||
-- wtf3-qinv = record
|
||||
-- { g = wtf3
|
||||
-- ; α = λ x → {! !}
|
||||
-- ; β = λ x → {! !}
|
||||
-- }
|
||||
|
||||
-- -- homotopy : (func ∘ func-inv) ∼ id
|
||||
-- -- homotopy x =
|
||||
-- -- let
|
||||
-- -- in {! !}
|
||||
|
||||
-- equiv = record
|
||||
-- { g = func-inv
|
||||
-- ; g-id = {! !}
|
||||
-- ; h = func-inv
|
||||
-- ; h-id = {! !}
|
||||
-- }
|
||||
c : (x : Set l) → C x x refl
|
||||
c x = id , qinv-to-isequiv id-qinv
|
||||
```
|
||||
|
||||
### Axiom 2.10.3 (Univalence)
|
||||
|
|
@ -399,6 +563,32 @@ postulate
|
|||
ua : {A B : Set} (eqv : A ≃ B) → (A ≡ B)
|
||||
```
|
||||
|
||||
### Lemma 2.10.5
|
||||
|
||||
```
|
||||
-- lemma2∙10∙5 : {l : Level} {A : Set l} {B : A → Set l}
|
||||
-- → (x y : A)
|
||||
-- → (p : x ≡ y)
|
||||
-- → (u : B x)
|
||||
-- → transport B p u ≡ transport id (ap B p) u
|
||||
```
|
||||
|
||||
## 2.11 Identity Type
|
||||
|
||||
### Theorem 2.11.1
|
||||
|
||||
```
|
||||
theorem2∙11∙1 : {A B : Set}
|
||||
→ (eqv @ (f , f-eqv) : A ≃ B)
|
||||
→ (a a' : A)
|
||||
→ (a ≡ a') ≃ (f a ≡ f a')
|
||||
theorem2∙11∙1 (f , mkIsEquiv g g-id h h-id) a a' = ap f , qinv-to-isequiv eqv
|
||||
where
|
||||
inv : f a ≡ f a' → a ≡ a'
|
||||
inv p = trans {! !} (trans (ap g p) {! !})
|
||||
eqv = mkQinv {! !} {! !} {! !}
|
||||
```
|
||||
|
||||
## 2.13 Natural numbers
|
||||
|
||||
```
|
||||
|
|
@ -496,4 +686,4 @@ theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl)
|
|||
where
|
||||
g : (X → A) × (X → B) → (X → A × B)
|
||||
g (f1 , f2) = λ x → (f1 x , f2 x)
|
||||
```
|
||||
```
|
||||
|
|
@ -1,6 +1,3 @@
|
|||
module HottBook.Util where
|
||||
|
||||
open import Agda.Primitive
|
||||
|
||||
id : {l : Level} {A : Set l} → A → A
|
||||
id x = x
|
||||
Loading…
Reference in a new issue