Compare commits
2 commits
a6d602c0f7
...
56df3385e6
Author | SHA1 | Date | |
---|---|---|---|
56df3385e6 | |||
b95699f2f0 |
6 changed files with 68 additions and 94 deletions
29
src/2024-05-09-perry-meeting.agda
Normal file
29
src/2024-05-09-perry-meeting.agda
Normal file
|
@ -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
|
|
@ -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) = ?
|
|
@ -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
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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 = {! !}
|
||||
```
|
Loading…
Reference in a new issue