auto gitdoc commit

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

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

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