From cd08197d66817211905106a02b62628779c7cb91 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 31 Oct 2022 16:05:18 -0500
Subject: [PATCH] update

---
 cubical-playground.agda-lib |  2 +-
 src/Ch6.agda                | 75 +++++++++++++++++++++++++++++++++++++
 src/HIT.agda                | 13 +++++++
 src/loopspace.agda          | 20 ++++++++++
 4 files changed, 109 insertions(+), 1 deletion(-)
 create mode 100644 src/Ch6.agda
 create mode 100644 src/HIT.agda
 create mode 100644 src/loopspace.agda

diff --git a/cubical-playground.agda-lib b/cubical-playground.agda-lib
index 672cf91..53c7164 100644
--- a/cubical-playground.agda-lib
+++ b/cubical-playground.agda-lib
@@ -1,2 +1,2 @@
 include: src
-depend: standard-library
+depend: standard-library cubical
diff --git a/src/Ch6.agda b/src/Ch6.agda
new file mode 100644
index 0000000..053da39
--- /dev/null
+++ b/src/Ch6.agda
@@ -0,0 +1,75 @@
+{-# OPTIONS --cubical #-}
+
+module Ch6 where
+
+open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
+
+open import HIT using (S¹; base; loop; apd)
+
+-- Lemma 6.2.5, if A is a type together with a : A and p : a = a, then there is
+-- a function f : 𝕊¹ → A with f(base) :≡ a and ap\_f(loop) := p
+
+lemma625 : {A : Type} → (a : A) → (p : a ≡ a) → (S¹ → A)
+lemma625 a p base = a
+lemma625 a p (loop i) = a
+
+lemma625prop1 : {A : Type} {a : A} {p : a ≡ a} → (lemma625 a p base ≡ a)
+lemma625prop1 = refl
+
+lemma625prop2 : {A : Type} {a : A} {p : a ≡ a} → (apd (lemma625 a p) loop ≡ p)
+lemma625prop2 {a} {p} = ?
+
+-- Lemma 6.2.8
+
+lemma628 : {A : Type} (f g : S¹ → A)
+  → (p : f base ≡ g base)
+  → (q : f loop ≡ g loop)
+  → ((x : S¹) → f x ≡ g x)
+
+-- Lemma 6.2.9
+
+-- lemma629f : {A : Type} → (g : S¹ → A) → {x : A} → Σ A (x ≡ x)
+-- 
+-- lemma629 : {A : Type} → (S¹ → A) ≡ ((x : A) → x ≡ x)
+-- lemma629 = ?
+
+-- Lemma 6.3.1
+-- Type I is contractible
+
+record is-contr {ℓ} (A : Type ℓ) : Type ℓ where
+  constructor contr
+  field
+    centre : A
+    paths : (x : A) → centre ≡ x
+open is-contr public
+
+-- Lemma 6.3.2
+-- Function extensionality
+
+lemma632 : {A B : Type} {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
+lemma632 {A} {B} {f} {g} p =
+  -- For all x : A, define a function pₓ : I → B
+  ?
+  where
+    pₓ : {x : A} → I → B
+    -- pₓ {x} i0 = f x
+    -- pₓ {x} i1 = g x
+--       pₓ i0 = f x
+--       pₓ i1 = g x
+--       pₓ seg = p x in
+--   let q : I → (A → B)
+--       q i x = pₓ i in
+
+-- Lemma 6.4.1
+
+open import Data.Empty using (⊥; ⊥-elim)
+
+¬_ : Set → Set
+¬ A = A → ⊥
+
+_≢_ : ∀ {A : Set} → A → A → Set
+x ≢ y  =  ¬ (x ≡ y)
+
+lemma641 : loop ≢ refl
+lemma641 p = ?
diff --git a/src/HIT.agda b/src/HIT.agda
new file mode 100644
index 0000000..4197665
--- /dev/null
+++ b/src/HIT.agda
@@ -0,0 +1,13 @@
+{-# OPTIONS --cubical #-}
+
+module HIT where
+
+open import Cubical.Core.Everything
+
+data S¹ : Set where
+  base : S¹
+  loop : base ≡ base
+
+apd : {A : Set} {B : A → Set} (f : (x : A) → B x) {x y : A} (p : x ≡ y)
+  → PathP (λ i → B (p i)) (f x) (f y)
+apd f p i = f (p i)
diff --git a/src/loopspace.agda b/src/loopspace.agda
new file mode 100644
index 0000000..886399e
--- /dev/null
+++ b/src/loopspace.agda
@@ -0,0 +1,20 @@
+-- TODO: Define arbitrary high loop spaces
+
+-- Prelude stuff
+{-# OPTIONS --cubical #-}
+
+open import Agda.Primitive public renaming ( Set to Type )
+open import Agda.Builtin.Cubical.Path public
+
+variable
+  ℓ : Level
+
+Path : ∀ {ℓ} (A : Type ℓ) → A → A → Type ℓ
+Path A a b = PathP (λ _ → A) a b
+
+-- Circle
+data S¹ : Type where
+  base : S¹
+  loop : base ≡ base
+
+