From f68001e728b9eebbb4847645a2dc3a29d70182de Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 01:27:51 +0000
Subject: [PATCH] auto gitdoc commit

---
 src/HottBook/Chapter1.lagda.md |  4 ++--
 src/HottBook/Chapter1Util.agda | 12 ++++++++++++
 src/HottBook/Util.agda         | 13 +++++++++++++
 3 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 src/HottBook/Chapter1Util.agda
 create mode 100644 src/HottBook/Util.agda

diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index e81ce45..313bc10 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -70,6 +70,8 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)
 ## 1.11 Propositions as types
 
 ```
+data ⊥ : Set where
+
 ¬_ : (A : Set) → Set
 ¬ A = A → ⊥
 ```
@@ -80,8 +82,6 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)
 data _≡_ {l} {A : Set l} : (a b : A) → Set l where
   instance refl : {x : A} → x ≡ x
 infix 4 _≡_
-
-data ⊥ : Set where
 ```
 
 ### 1.12.3 Disequality
diff --git a/src/HottBook/Chapter1Util.agda b/src/HottBook/Chapter1Util.agda
new file mode 100644
index 0000000..9c9dfc0
--- /dev/null
+++ b/src/HottBook/Chapter1Util.agda
@@ -0,0 +1,12 @@
+module HottBook.Chapter1Util where
+
+open import Agda.Primitive
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Util
+
+Σ-≡ : {l₁ l₂ : Level} {A : Set l₁} {B : A → Set l₂}
+  → {p₁ @ (a₁ , b₁) p₂ @ (a₂ , b₂) : Σ A B}
+  → Σ (a₁ ≡ a₂) (λ p → transport B p b₁ ≡ b₂)
+  → p₁ ≡ p₂
+Σ-≡ {l₁} {l₂} {A} {B} {p₁ @ (a₁ , b₁)} {p₂ @ (a₂ , b₂)} (refl , refl) = refl
diff --git a/src/HottBook/Util.agda b/src/HottBook/Util.agda
new file mode 100644
index 0000000..8ac1438
--- /dev/null
+++ b/src/HottBook/Util.agda
@@ -0,0 +1,13 @@
+module HottBook.Util where
+
+open import Agda.Primitive
+
+infixl 40 _∘_
+_∘_ : {A B C : Set}
+  → (f : A → B)
+  → (g : B → C)
+  → A → C
+(f ∘ g) x = g (f x)
+
+id : {l : Level} {A : Set l} → A → A
+id x = x
\ No newline at end of file