update

src/2024-05-09-perry-meeting.agda

@@ -0,0 +1,29 @@
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Util
+
+test : {A B : Set}
+  → (equiv @ (f , fIsEquiv) : A ≃ B)
+  → (x y : A)
+  → (x ≡ y) ≃ (f x ≡ f y)
+test (equiv @ (f , mkIsEquiv g g-id h h-id)) x y = f2 , f2IsEquiv
+  where
+    f2 : x ≡ y → f x ≡ f y
+    f2 p = ap f p
+
+    g2 : f x ≡ f y → x ≡ y
+    g2 p = 
+      let p1 = ap h p in
+      let p2 = trans p1 (h-id y) in
+      let p3 = trans (sym (h-id x)) p2 in
+      p3
+
+    forwards : f2 ∘ g2 ∼ id
+    forwards b = {!   !}
+      where
+        q = let y = f2 ∘ g2 in {!   !}
+
+    backwards : g2 ∘ f2 ∼ id
+    backwards b = {!   !}
+
+    f2IsEquiv = mkIsEquiv g2 forwards g2 backwards

src/Crypto/RSA.agda

@@ -1,36 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module Crypto.RSA where
-
-open import Agda.Builtin.Cubical.Path
-open import Crypto.RSA.Nat
-
-refl : {A : Set} {x y : A} → x ≡ y
-refl {A} {x} {y} i = x
-
-data Σ (A : Set) (B : A → Set) : Set where
-  ⟨_,_⟩ : (x : A) → B x → Σ A B
-
-∃ : ∀ {A : Set} (B : A → Set) → Set
-∃ {A} B = Σ A B
-
-∃-syntax = ∃
-syntax ∃-syntax (λ x → B) = ∃[ x ] B
-
-record divides (d n : ℕ) : Set where
-  constructor mkDivides
-  field
-    p : ∃[ m ] (d * m ≡ n)
-
--- doesDivide : (d n : ℕ) → Dec (divides d n)
--- doesDivide zero n = yes refl
--- doesDivide (suc d) n = ?
-
-record prime (n : ℕ) : Set where
-  constructor mkPrime
-  field
-    p : ∀ (x y : ℕ) → ¬ (x * y ≡ n)
-
-isPrime : (n : ℕ) → Dec (prime n)
-isPrime zero = ?
-isPrime (suc n) = ?

src/Crypto/RSA/Nat.agda

@@ -1,39 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module Crypto.RSA.Nat where
-
-open import Agda.Builtin.Cubical.Path
-
-infixl 6 _+_
-infixl 7 _*_
-
-data Bool : Set where
-  true : Bool
-  false : Bool
-
-record ⊥ : Set where
-
-¬_ : Set → Set
-¬ x = ⊥
-
-data Dec (A : Set) : Set where
-  yes : A → Dec A
-  no : ¬ A → Dec A
-
-data ℕ : Set where
-  zero : ℕ
-  suc : ℕ → ℕ
-
-{-# BUILTIN NATURAL ℕ #-}
-
-data Fin : ℕ → Set where
-  zero : {n : ℕ} → Fin (suc n)
-  suc : {n : ℕ} → (i : Fin n) → Fin (suc n)
-
-_+_ : ℕ → ℕ → ℕ
-zero + y = y
-suc x + y = suc (x + y)
-
-_*_ : ℕ → ℕ → ℕ
-zero * y = zero
-suc x * y = y + x * y

src/HottBook/Chapter2.lagda.md

@@ -1,10 +1,15 @@
-```
-module HottBook.Chapter2 where
+<details>
+  <summary>Imports</summary>
 
-open import Agda.Primitive
-open import HottBook.Chapter1
-open import HottBook.Util
-```
+  ```
+  module HottBook.Chapter2 where
+
+  open import Agda.Primitive
+  open import HottBook.Chapter1
+  open import HottBook.Util
+  ```
+
+</details>
 
 ## 2.1 Types are higher groupoids
 
@@ -256,7 +261,7 @@ _≃_ : {l : Level} → (A B : Set l) → Set l
 A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
 ```
 
-## 2.8 Σ-types
+## 2.7 Σ-types
 
 ### Theorem 2.7.2
 

src/HottBook/Chapter3.lagda.md

@@ -53,20 +53,20 @@ isProp P = (x y : P) → x ≡ y
 ### Lemma 3.3.2
 
 ```
-lemma3∙2∙2 : {P : Set}
-  → isProp P
-  → (x₀ : P)
-  → P ≃ 𝟙
-lemma3∙2∙2 {P} PisProp x₀ = f , mkIsEquiv g {!  forwards !} g {!   !}
-  where
-    f : P → 𝟙
-    f x = tt
+-- lemma3∙2∙2 : {P : Set}
+--   → isProp P
+--   → (x₀ : P)
+--   → P ≃ 𝟙
+-- lemma3∙2∙2 {P} PisProp x₀ = f , mkIsEquiv g {!  forwards !} g {!   !}
+--   where
+--     f : P → 𝟙
+--     f x = tt
 
-    g : 𝟙 → P
-    g u = x₀
+--     g : 𝟙 → P
+--     g u = x₀
 
-    forwards : f ∘ g ∼ id
-    forwards x = {! refl  !}
+--     forwards : f ∘ g ∼ id
+--     forwards x = {! refl  !}
 ```
 
 ## 3.4 Classical vs. intuitionistic logic

src/HottBook/Chapter4.lagda.md

@@ -1,5 +1,9 @@
 ```
 module HottBook.Chapter4 where
+
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Chapter3
 ```
 
 ## 4.1 Quasi-inverses
@@ -7,3 +11,14 @@ module HottBook.Chapter4 where
 ```
 -- qinv : {A B : Type} (f : A → B) → 
 ```
+
+### Theorem 4.1.3
+
+There exist types A and B and a function f : A → B such that qinv( f ) is not a mere proposition.
+
+```
+theorem4∙1∙3 : {A B : Set}
+  → (f : A → B)
+  → isProp (qinv f) → ⊥
+theorem4∙1∙3 f p = {!   !}
+```