prove example 3.1.9

src/CubicalHott/Definition8-4-3.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Definition8-4-3 where
+
+

src/CubicalHott/Example3-1-9.agda

@@ -0,0 +1,51 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Example3-1-9 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Function
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Bool.Base
+open import CubicalHott.Remark2-12-6
+
+lemma : ∀ {l} → ¬ (isSet (Type l))
+lemma {l} p = true≢false lol where
+  f : Lift Bool → Lift Bool
+  f (lift false) = lift true
+  f (lift true) = lift false
+
+  g : (a : Lift Bool) → f (f a) ≡ a
+  g (lift false) = refl
+  g (lift true) = refl
+  
+  f-equiv : Lift Bool ≃ Lift Bool
+  f-equiv = isoToEquiv (iso f f g g) 
+  
+  f-path : Lift Bool ≡ Lift Bool
+  f-path = ua f-equiv
+
+  bogus : idfun (Lift Bool) ≡ f
+  bogus =
+    let
+      helper : f-path ≡ refl
+      helper = p (Lift Bool) (Lift Bool) f-path refl
+
+      wtf : pathToEquiv (ua f-equiv) ≡ pathToEquiv refl
+      wtf = cong pathToEquiv helper
+
+      wtf2 : fst (pathToEquiv (ua f-equiv)) ≡ idfun (Lift Bool)
+      wtf2 = cong fst wtf ∙ funExt transportRefl
+
+      wtf3 : fst (pathToEquiv (ua f-equiv)) ≡ f
+      wtf3 = cong fst (pathToEquiv-ua f-equiv)
+
+      wtf4 : f ≡ idfun (Lift Bool)
+      wtf4 = sym wtf3 ∙ wtf2
+
+    in sym wtf4
+
+  lol : true ≡ false
+  lol = cong (λ f → Lift.lower (f (lift true))) bogus

src/CubicalHott/Lemma4-1-1.agda

@@ -0,0 +1,22 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma4-1-1 where
+
+open import Cubical.Foundations.Equiv.Base
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Univalence
+
+lemma : {A B : Type} → (f : A → B) → isIso f → isIso f ≃ ((x : A) → (x ≡ x))
+lemma {A} {B} f (g , fg , gf) = isoToEquiv (iso f' {!  g' !} {!   !} {!   !}) where
+  f' : isIso f → (x : A) → x ≡ x
+  f' (g , fg , gf) x = refl
+
+  g' : ((x : A) → x ≡ x) → isIso f
+  g' h = {!   !} , {!   !} , {!   !}
+
+  -- f-equiv : A ≃ B
+  -- f-equiv = isoToEquiv (iso f g fg gf)
+
+  -- f-id : A ≡ B
+  -- f-id = ua f-equiv

src/CubicalHott/Lemma6-10-2.agda

@@ -0,0 +1,17 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma6-10-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Functions.Surjection
+open import Cubical.HITs.SetQuotients
+open import Cubical.HITs.PropositionalTruncation
+
+private
+  variable
+    l : Level
+
+lemma : (A : Type l) (R : A → A → Type l)
+  → (q : A → A / R)
+  → isSurjection q
+lemma {l} A R q x = {!   !}

src/CubicalHott/Lemma6-4-1.agda

@@ -0,0 +1,10 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma6-4-1 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Relation.Nullary
+open import Cubical.HITs.S1
+
+loop≢refl : ¬ (loop ≡ refl)
+loop≢refl p = {!   !}

src/CubicalHott/Lemma6-5-1.agda

@@ -4,11 +4,12 @@
 
 module CubicalHott.Lemma6-5-1 where
 
-open import CubicalHott.Prelude
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv.Base
+open import Cubical.Foundations.Isomorphism
 open import Cubical.HITs.Susp
 open import Cubical.HITs.S1
 open import Cubical.Data.Int
-open import Cubical.Data.Nat
 open import Cubical.Data.Bool
 
 -- Lemma 6.5.1

src/CubicalHott/Lemma6-5-4.agda

@@ -0,0 +1,10 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma6-5-4 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+
+private
+  variable
+    l : Level

src/CubicalHott/Lemma6-8-2.agda

@@ -0,0 +1,16 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma6-8-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Colimit
+open import Cubical.Data.Graph.Base
+
+private
+  variable
+    l : Level
+
+lemma : {l : Level} {A B C E : Type l} {f : C → A} {g : C → B}
+  → (Pushout f g → E) ≃ Cocone l (record {  }) E

src/CubicalHott/Lemma6-9-1.agda

@@ -0,0 +1,18 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma6-9-1 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.HITs.Truncation
+open import Agda.Builtin.Unit
+
+lemma : {A : Type} → {B : ∥ A ∥ 0 → Type}
+  → (g : (a : A) → B (∣ a ∣ₕ))
+  → ((x : ∥ A ∥ 0) → isSet (B x))
+  → Σ ((x : ∥ A ∥ 0) → B x) (λ f → (a : A) → f (∣ a ∣ₕ) ≡ g a)
+lemma {A} {B} g f = h , p where
+  h : (x : ∥ A ∥ 0) → B x
+  h (lift tt) = g {!   !}
+
+  p : (a : A) → h (lift tt) ≡ g a
+  p a = {!   !}

src/CubicalHott/Lemma6-9-2.agda

@@ -0,0 +1,8 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma6-9-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.HITs.PropositionalTruncation
+
+-- lemma : {A B : Type} → isSet B → (∥ A ∥₀ → B) ≃ (A → B)

src/CubicalHott/Lemma9-1-8.agda

@@ -0,0 +1,9 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma9-1-8 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Category
+
+lemma : ∀ {l l2} → (C : Category l l2) → isGroupoid (Category.ob C)
+lemma C x y p q r s = {!   !}

src/CubicalHott/Remark2-12-6.agda

@@ -0,0 +1,29 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Remark2-12-6 where
+
+open import Cubical.Foundations.Equiv.Base
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.HITs.Pushout
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Bool.Base
+open import Cubical.Data.Empty
+
+module _ where
+  private
+    variable
+      A B : Type
+      a0 : A
+      b : B
+
+data Unit : Type where
+  tt : Unit
+
+true≢false : ¬ (true ≡ false)
+true≢false p = subst P p tt where
+  P : Bool → Type
+  P false = ⊥
+  P true = Unit
+
+

src/CubicalHott/Theorem8-1.agda

@@ -0,0 +1,53 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem8-1 where
+
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Univalence
+open import Cubical.HITs.S1 hiding (encode; decode)
+open import Cubical.Homotopy.Loopspace
+open import Data.Nat hiding (pred; _+_) renaming (suc to nsuc)
+open import Data.Integer
+
+private
+  variable
+    l : Level
+
+-- Definition 8.1.1
+
+code : S¹ → Type
+code base = ℤ
+code (loop i) = ua suc≃ i where
+  suc≃ : ℤ ≃ ℤ
+  suc≃ = isoToEquiv (iso suc pred sec ret) where
+    sec : section suc pred
+    sec (+_ zero) = refl
+    sec +[1+ n ] = refl
+    sec (-[1+_] zero) = refl
+    sec (-[1+_] (nsuc n)) = refl
+    ret : retract suc pred
+    ret (+_ zero) = refl
+    ret +[1+ n ] = refl
+    ret (-[1+_] zero) = refl
+    ret (-[1+_] (nsuc n)) = refl
+
+-- Lemma 8.1.2
+
+lemma8-1-2a : (x : ℤ) → subst code loop x ≡ suc x
+lemma8-1-2a x = {!   !}
+
+-- Definition 8.1.5
+
+encode : (x : S¹) → base ≡ x → code x
+encode s p = subst code p +0
+
+-- Definition 8.1.6
+
+decode : (x : S¹) → code x → base ≡ x
+
+-- Corollary 8.1.10
+          
+corollary8-1-10 : Ω (S¹ , base) ≃∙ ℤ , +0

src/CubicalHott/Theorem8-2-1.agda

@@ -0,0 +1,12 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem8-2-1 where
+
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude
+open import Cubical.Homotopy.Connected
+open import Cubical.HITs.Susp
+open import Data.Nat
+
+theorem : {A : Type} → (n : HLevel) → isConnected n A → isConnected (suc n) (Susp A)
+theorem n n-connected = {!   !}