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

---
 src/HottBook/Chapter1.lagda.md | 91 ++++++++++++++++++++++++++++++----
 1 file changed, 80 insertions(+), 11 deletions(-)

diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index 60ecffd..e81ce45 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -1,32 +1,101 @@
 ```
 module HottBook.Chapter1 where
 
-open import Relation.Binary.PropositionalEquality
-open import Data.Empty
-open import Data.Sum
-
-open import HottBook.Common
+open import Agda.Primitive
 ```
 
+## 1.1 Type theory versus set theory
+
+## 1.2 Function types
+
+## 1.3 Universes and families
+
+## 1.4 Dependent function types (Π-types)
+
+## 1.5 Product types
+
+```
+data 𝟙 : Set where
+  tt : 𝟙
+
+```
+
+## 1.6 Dependent pair types (Σ-types)
+
+```
+record Σ {l₁ l₂} (A : Set l₁) (B : A → Set l₂) : Set (l₁ ⊔ l₂) where
+  constructor _,_
+  field
+    fst : A
+    snd : B fst
+open Σ
+infixr 4 _,_
+{-# BUILTIN SIGMA Σ #-}
+syntax Σ A (λ x → B) = Σ[ x ∈ A ] B
+
+_×_ : {l : Level} (A B : Set l) → Set l
+_×_ A B = Σ A (λ _ → B)
+```
+
+
 ## 1.7 Coproduct types
 
 ```
-infixl 6 _+_
-_+_ : (A B : Type) → Type
-A + B = A ⊎ B
+-- infixl 6 _+_
+-- _+_ : (A B : Set) → Set
+-- A + B = A ⊎ B
+```
+
+## 1.8 The type of booleans
+
+```
+data 𝟚 : Set where
+  true : 𝟚
+  false : 𝟚
+```
+
+## 1.9 The natural numbers
+
+```
+data ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+{-# BUILTIN NATURAL ℕ #-}
+
+rec-ℕ : (C : Set) → C → (ℕ → C → C) → ℕ → C
+rec-ℕ C z s zero = z
+rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)
 ```
 
 ## 1.11 Propositions as types
 
 ```
-¬_ : (A : Type) → Type
+¬_ : (A : Set) → Set
 ¬ A = A → ⊥
 ```
 
-## 1.12.1 Path Induction
+## 1.12 Identity types
 
 ```
-J : {A : Type} → (C : (x y : A) → x ≡ y → Type)
+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
+
+```
+_≢_ : {A : Set} (x y : A) → Set
+_≢_ x y = (p : x ≡ y) → ⊥
+```
+
+### 1.12.1 Path induction
+
+```
+J : {l₁ l₂ : Level} {A : Set l₁}
+  → (C : (x y : A) → x ≡ y → Set l₂)
   → (c : (x : A) → C x x refl)
   → (x y : A) → (p : x ≡ y) → C x y p
 J C c x x refl = c x