From 4808bfada716817e186060025e7827d448fcbb53 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 23 Feb 2023 04:20:35 -0600
Subject: [PATCH] ice

---
 src/Ch2.agda        | 72 ++++++++++++++++++++++++++++++++++++++++
 src/Ch6.agda        | 80 ++++++++++++++++++++++++++++++++++++++++-----
 src/Divergence.agda | 15 +++++++++
 src/Simple.agda     | 40 +++++++++++++++++++++++
 src/jasontime.agda  | 69 ++++++++++++++++++++++++++++++++++++++
 5 files changed, 268 insertions(+), 8 deletions(-)
 create mode 100644 src/Ch2.agda
 create mode 100644 src/Divergence.agda
 create mode 100644 src/Simple.agda
 create mode 100644 src/jasontime.agda

diff --git a/src/Ch2.agda b/src/Ch2.agda
new file mode 100644
index 0000000..6cae3ef
--- /dev/null
+++ b/src/Ch2.agda
@@ -0,0 +1,72 @@
+{-# OPTIONS --cubical #-}
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+
+-- Path induction
+
+path-ind : {A : Set}
+  → (C : (x y : A) → x ≡ y → Set)
+  → (c : (x : A) → C x x refl)
+  → (x y : A) → (p : x ≡ y) → C x y p
+path-ind C c x y p = ?
+
+-- Lemma 2.1.1
+
+-- TODO: Not sure if there's actually a way to express inductive principle of
+-- identity in code?
+lemma211 : {A : Set} → (x y : A) → (x ≡ y) → (y ≡ x)
+lemma211 x y p = (λ i → p (~ i))
+
+D : {A : Set} → (x y : A) → x ≡ y → Set
+D x y p = y ≡ x
+
+d : {A : Set} → (x : A) → D x x refl
+d x = refl
+
+-- Lemma 2.1.2
+
+lemma212 : {A : Set} → {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
+lemma212 p q = p ∙ q
+-- (x ≡ z) i0 = x
+-- (x ≡ z) i1 = z
+--
+-- if i = i0 then
+--   p i0 = x
+--   q i0 = y
+--
+-- if i = i1 then
+--   p i1 = y
+--   q i1 = z
+--
+-- overall
+--   p i = i0 ∧ i
+--   q i = i1 ∨ i
+
+-- Lemma 2.11.1
+
+ap : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
+ap f p i = f (p i)
+
+lemma2111 : {A B : Set} → (f : A → B) → (ie : isEquiv f) → {a a′ : A}
+  → isEquiv (ap f)
+lemma2111 f ie .equiv-proof y = ?
+
+-- Lemma 2.11.2
+
+lemma2112a : {A : Set} → (a : A) → {x₁ x₂ : A} → (p : x₁ ≡ x₂) → (q : a ≡ x₁)
+  → transport ? p ≡ q ∙ p
+lemma2112a a p q = ?
+
+-- Lemma 2.11.3
+
+lemma2113 : {A B : Set}
+  → (f g : A → B)
+  → {a a′ : A}
+  → (p : a ≡ a′)
+  → (q : f a ≡ g a)
+  → Set
+  -- TODO:
+  -- → transport (λ i → f a′ ≡ g a′) x ≡ (sym (ap f p)) ∙ q ∙ (ap g p)
diff --git a/src/Ch6.agda b/src/Ch6.agda
index 053da39..e0bc775 100644
--- a/src/Ch6.agda
+++ b/src/Ch6.agda
@@ -3,29 +3,69 @@
 module Ch6 where
 
 open import Cubical.Core.Everything
+open import Cubical.Data.Equality
 open import Cubical.Foundations.Prelude
+open import Cubical.HITs.S1
 
-open import HIT using (S¹; base; loop; apd)
+-- private
+--   variable
+--     ℓ ℓ' : Level
+--     A : Type ℓ
+-- 
+-- transport′ : ∀ (C : A → Type ℓ') {x y : A} → x ≡ y → C x → C y                
+-- transport′ C refl b = b                                                       
+-- 
+-- apd : {C : A → Type ℓ} (f : (x : A) → C x) {x y : A} (p : x ≡ y) → transport′ C p (f x) ≡ f y              
+-- apd f refl = refl
+
+-- apd : {A : Set} {B : A → Set} (f : (x : A) → B x) {x y : A} (p : x ≡ y)
+--  → transport p (f x ≡ f y)
+  -- → PathP (λ i → B (p i)) (f x) (f y)
+-- apd f p i = f (p i)
+-- apd f p = \i . f (p i)
 
 -- 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
+lemma625 a p (loop i) = p i
 
 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} = ?
+ap : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
+ap f p i = f (p i)
+
+lemma625prop2 : {A : Type} (a : A) → (p : a ≡ a) → ap (lemma625 a p) loop ≡ p
+lemma625prop2 a p = refl
+
+-- Lemma 2.3.2 (Path lifting)
 
 -- Lemma 6.2.8
+ 
+-- a : (A : Type) → (f : S¹ → A) → apd f loop
+apd : {A : Type} {P : A → Type} (f : (x : A) → P x) {x y : A} (p : x ≡ y)
+  → PathP (λ i → P (p i)) (f x) (f y)
+apd f p i = f (p i)
 
 lemma628 : {A : Type} (f g : S¹ → A)
   → (p : f base ≡ g base)
-  → (q : f loop ≡ g loop)
-  → ((x : S¹) → f x ≡ g x)
+  → (q : PathP (λ i → p i ≡ p i) (ap f loop) (ap g loop))
+  → (x : S¹)
+  → f x ≡ g x
+lemma628 f g p q base = p
+lemma628 f g p q x = {! !} -- ICE: Try to split on x
+-- f (loop i) = g (loop i)
+-- when i = i0
+--   f base = g base
+--   _ j0 = f base
+--   _ j1 = g base
+-- when i = i1
+--   f base = g base
+--   _ j0 = f base
+--   _ j1 = g base
+-- lemma628 f g p q (loop i) j = p j
 
 -- Lemma 6.2.9
 
@@ -63,6 +103,8 @@ lemma632 {A} {B} {f} {g} p =
 
 -- Lemma 6.4.1
 
+open import Data.Bool
+open import Data.Unit
 open import Data.Empty using (⊥; ⊥-elim)
 
 ¬_ : Set → Set
@@ -71,5 +113,27 @@ open import Data.Empty using (⊥; ⊥-elim)
 _≢_ : ∀ {A : Set} → A → A → Set
 x ≢ y  =  ¬ (x ≡ y)
 
-lemma641 : loop ≢ refl
-lemma641 p = ?
+Bool-size : Bool → Type
+Bool-size true = ⊤
+Bool-size false = ⊥
+
+true≢false : true ≢ false
+true≢false p = let x = subst Bool-size p tt in ?
+
+-- lemma641 : loop ≢ refl
+-- lemma641 p = true≢false 
+
+-- Lemma 6.4.5
+
+open import Cubical.Data.Sigma
+
+lemma645 : (A : Set)
+  → (P : A → Set)
+  → (x y : A)
+  → (p q : x ≡ y)
+  → (r : p ≡ q)
+  → (u : P x)
+  → ⊤
+-- lemma645 A P x y p q r u =
+--   let x = transport {A = p} r ? in
+--   ?
diff --git a/src/Divergence.agda b/src/Divergence.agda
new file mode 100644
index 0000000..d36f903
--- /dev/null
+++ b/src/Divergence.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --cubical #-}
+
+module Divergence where
+
+open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
+open import Data.Nat
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary using (¬_)
+
+_≢_ : {ℓ : Level} {A : Set ℓ} → Rel A ℓ
+x ≢ y = ¬ x ≡ y
+
+_ : 0 ≢ 1
+_ = ?
diff --git a/src/Simple.agda b/src/Simple.agda
new file mode 100644
index 0000000..c9249a7
--- /dev/null
+++ b/src/Simple.agda
@@ -0,0 +1,40 @@
+{-# OPTIONS --cubical #-}
+
+open import Cubical.Foundations.Prelude 
+  using (_≡_; refl; _∙_; _≡⟨_⟩_; _∎; cong; sym; fst; snd; _,_; ~_)
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Foundations.Equiv using (isEquiv; equivProof; equiv-proof)
+open import Relation.Nullary using (¬_)
+open import Relation.Binary.Core using (Rel)
+open import Data.Nat
+
+sanity : 1 + 1 ≡ 2
+sanity = refl
+
++-comm : (a b : ℕ) → a + b ≡ b + a
++-comm zero zero = refl
++-comm (suc a) zero = cong suc (+-comm a zero)
+
+-- +-comm (suc a) zero = suc a + zero
+--   ≡⟨ refl ⟩
+--     -- suc n + m = suc (n + m)
+--     suc (a + zero)
+--   ≡⟨ cong suc (+-comm a zero) ⟩
+--     suc (zero + a)
+--   ≡⟨ refl ⟩
+--     -- zero  + m = m
+--     suc a
+--   ≡⟨ refl ⟩
+--     zero + suc a
+--   ∎
+--
+-- inner-eq : a ≡ b
+-- cong app inner-eq : app a ≡ app b
+
+
+-- a + b
+-- _+_ : (a b : ℕ) → ℕ
+-- _+_+_+_ : (a b c d : ℕ) → ℕ
+-- _[_;_]′
+-- a [ 34 ; b ]
+--
diff --git a/src/jasontime.agda b/src/jasontime.agda
new file mode 100644
index 0000000..a9c3889
--- /dev/null
+++ b/src/jasontime.agda
@@ -0,0 +1,69 @@
+{-# OPTIONS --cubical #-}
+
+module jasontime where
+
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Univalence
+open import Data.Product
+open import Relation.Nullary
+open import Function.LeftInverse hiding (id; _∘_)
+open import Relation.Binary.PropositionalEquality hiding (_≡_)
+
+-- Cribbed from https://stackoverflow.com/a/13441191
+Surjective : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
+Surjective {A = A} {B = B} f = ∀ (y : B) → ∃ λ (x : A) → f x ≡ y
+
+Injective : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
+Injective {A = A} {B = B} f = ∀ (x y : A) → f x ≡ f y → x ≡ y
+
+-- contrapositive : {A B : Set} → (A → B) → (¬ B → ¬ A)
+-- contrapositive f g = g ∘ f
+-- 
+-- Prove: f x ≡ f y → x ≡ y
+-- Contra: x ≢ y → f x ≢ f y
+-- contrapositive-statement : {S T : Set} → (f : S → T) → Surjective f → (x y : S) → x ≡ y → f x ≡ f y
+-- 
+-- wtf : {A : Set} {x y : A} → ¬ (x ≢ y) → x ≡ y
+-- wtf s = ?
+
+id : {A : Set} → A → A
+id x = x
+
+surjective-is-right-inverse : {S T : Set} → (f : S → T) → Surjective f → ∃ (λ g → f ∘ g ≡ id)
+surjective-is-right-inverse f sj .fst t = Σ.fst (sj t)
+surjective-is-right-inverse {S} {T} f sj .snd =
+  let g = Σ.fst (surjective-is-right-inverse f sj) in
+  ?
+  -- funExt (λ s i → 
+  --   let t = f s in
+  --   let surjectivity = sj t in
+  --   let sj-proof = Σ.snd surjectivity in
+  --   let g∘f = g ∘ f in
+  --   let Fuck! = transport {A = T} {B = T} ? ? in
+  --   ?
+  -- )
+  -- funExt {A = S} {B = λ x i → ?} (λ x → ?) ? ?
+
+left-inverse-is-injective : {S T : Set} → (g : T → S) → ∃ (λ f → f ∘ g ≡ id) → Injective g
+
+jasontime-lemma : {S T : Set} → (f : S → T) → Surjective f → ∃ {A = T → S} (λ g → Injective g)
+jasontime-lemma {S} {T} f sj .fst t = 
+  let rinv = surjective-is-right-inverse f sj in
+  let rinv-fn = Σ.fst rinv in
+  rinv-fn t
+jasontime-lemma f sj .snd x y p =
+  ?
+  where
+    rinv = surjective-is-right-inverse f sj
+    g = Σ.fst rinv
+
+    TheLeftInverse : ∃ (λ f → f ∘ g ≡ id)
+    TheLeftInverse .fst = ?
+    TheLeftInverse .snd = ?
+
+    Fuck! = left-inverse-is-injective ? TheLeftInverse
+    rinv-prf = Σ.snd rinv
+    left-inv = Σ.fst TheLeftInverse