Research

This book tracks my current research goals and progress.

Current research: Formalizing spectral sequences in cubical Agda.

Resources

I have scaled down some of these materials to eBook size, for easier reading on mobile phones. The original full PDFs are linked as well.

Imports 
{-# OPTIONS --rewriting #-}

module HottBook.Chapter1 where

open import Agda.Primitive hiding (Prop) public
open import HottBook.CoreUtil

private
  variable
    l : Level

1 Type theory

1.1 Type theory versus set theory

1.2 Function types

1.3 Universes and families

1.4 Dependent function types (Π-types)

id : {A : Set l} → A → A
id x = x

1.5 Product types

module Products where
  data _×_ (A B : Set) : Set where
    _,_ : A → B → A × B

  pr₁ : {A B : Set} → A × B → A
  pr₁ (a , _) = a

  pr₂ : {A B : Set} → A × B → B
  pr₂ (_ , b) = b

  rec-× : {A B : Set}
    → (C : Set)
    → (A → B → C)
    → A × B
    → C
  rec-× C f (a , b) = f a b

data 𝟙 : Set where
  tt : 𝟙

1.6 Dependent pair types (Σ-types)

infixr 4 _,_
infixr 2 _×_

record Σ {l₁ l₂} (A : Set l₁) (B : A → Set l₂) : Set (l₁ ⊔ l₂) where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ public
{-# BUILTIN SIGMA Σ #-}
syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

_×_ : {l : Level} (A B : Set l) → Set l
_×_ A B = Σ A (λ _ → B)

1.7 Coproduct types

infixl 6 _+_
data _+_ {l : Level} (A B : Set l) : Set l where
  inl : A → A + B
  inr : B → A + B

Recursor:

rec-+ : {A B : Set}
  → (C : Set)
  → (A → C)
  → (B → C)
  → A + B
  → C
rec-+ C f g (inl x) = f x
rec-+ C f g (inr x) = g x

data ⊥ : Set where

rec-⊥ : {C : Set l} → (x : ⊥) → C
rec-⊥ ()

1.8 The type of booleans

data 𝟚 : Set where
  true : 𝟚
  false : 𝟚

neg : 𝟚 → 𝟚
neg true = false
neg false = true

1.9 The natural numbers

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

rec-ℕ : (C : Set) → C → (ℕ → C → C) → ℕ → C
rec-ℕ C z s zero = z
rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)

1.11 Propositions as types

infix 3 ¬_
¬_ : (A : Set l) → Set l
¬_ A = A → ⊥

1.12 Identity types

infix 4 _≡_
data _≡_ {A : Set l} : (a b : A) → Set l where
  instance refl : {x : A} → x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REWRITE _≡_ #-}

1.12.3 Disequality

_≢_ : {A : Set l} (x y : A) → Set l
_≢_ x y = (p : x ≡ y) → ⊥

1.12.1 Path induction

J : {l₁ l₂ : Level} {A : Set l₁}
  → (C : (x y : A) → x ≡ y → Set l₂)
  → (c : (x : A) → C x x refl)
  → (x y : A) → (p : x ≡ y) → C x y p
J C c x x refl = c x

Based path induction:

based-path-induction : {l1 l2 : Level} {A : Set l1} (a : A)
  → (C : (x : A) → (a ≡ x) → Set l2)
  → (c : C a refl)
  → (x : A) → (p : a ≡ x) → C x p
based-path-induction a C c x refl = c

Exercises

Exercise 1.1

Given functions f : A → B and g : B → C, define their composite g ◦ f : A → C. Show that we have h ◦ (g ◦ f) ≡ (h ◦ g) ◦ f.

composite : {A B C : Set}
  → (f : A → B)
  → (g : B → C)
  → A → C
composite f g x = g (f x)

-- https://agda.github.io/agda-stdlib/master/Function.Base.html
infixr 9 _∘_
_∘_ : {l1 l2 l3 : Level} {A : Set l1} {B : Set l2} {C : Set l3}
  → (g : B → C)
  → (f : A → B)
  → A → C
_∘_ g f x = g (f x)

composite-assoc : {A B C D : Set l}
  → (f : A → B)
  → (g : B → C)
  → (h : C → D)
  → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
composite-assoc f g h = refl

Exercise 1.2

Exercise 1.14

Why do the induction principles for identity types not allow us to construct a function reflx​) with the defining equation ?

Under non-UIP systems, there are identity types that are different from refl, and this ability gives us higher dimensional paths. Otherwise, we would be dealing with propositions only.

Imports 
{-# OPTIONS --rewriting #-}

module HottBook.Chapter2 where

open import Agda.Primitive.Cubical hiding (i1)
open import HottBook.Chapter1
open import HottBook.Chapter1Util
open import HottBook.Chapter2Lemma221 public
open import HottBook.Chapter2Lemma231 public
open import HottBook.Chapter2Definition217 public

private
  variable
    l l2 : Level

2 Homotopy type theory

2.1 Types are higher groupoids

Lemma 2.1.1

sym : {l : Level} {A : Set l} {x y : A} → (x ≡ y) → y ≡ x
sym {l} {A} {x} {y} refl = refl

Lemma 2.1.2

trans : {l : Level} {A : Set l} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
trans {l} {A} {x} {y} {z} refl refl = refl

infixr 30 _∙_
_∙_ = trans

Equational Reasoning

module ≡-Reasoning where
  infix 1 begin_
  begin_ : {l : Level} {A : Set l} {x y : A} → (x ≡ y) → (x ≡ y)
  begin x = x

  _≡⟨⟩_ : {l : Level} {A : Set l} (x {y} : A) → x ≡ y → x ≡ y
  _ ≡⟨⟩ x≡y = x≡y

  infixr 2 _≡⟨⟩_ step-≡
  step-≡ : {l : Level} {A : Set l} (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
  step-≡ _ y≡z x≡y = trans x≡y y≡z
  syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z

  infix 3 _∎
  _∎ : {l : Level} {A : Set l} (x : A) → (x ≡ x)
  _ ∎ = refl

Lemma 2.1.4

module lemma2∙1∙4 {l : Level} {A : Set l} where
  i1 : {x y : A} (p : x ≡ y) → p ≡ p ∙ refl
  i1 {x} {y} refl = refl

  i2 : {x y : A} (p : x ≡ y) → p ≡ refl ∙ p
  i2 {x} {y} refl = refl

  ii1 : {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
  ii1 {x} {y} refl = refl

  ii2 : {x y : A} (p : x ≡ y) → p ∙ (sym p) ≡ refl
  ii2 {x} {y} refl = refl

  iii : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
  iii {x} {y} refl = refl

  iv : {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
  iv {x} {y} {z} {w} refl refl refl = refl

Theorem 2.1.6 (Eckmann-Hilton)

-- module theorem2∙1∙6 where
--   Ω-type : (A : Set) → (a : A) → Set
--   Ω-type A a = refl {x = a} ≡ refl

--   compose1 : {A : Set} {a : A} → fst (Ω (A , a)) → fst (Ω (A , a)) → fst (Ω (A , a))
--   compose1 x y = x ∙ y

--   Ω² : {l : Level} → Set* l → Set* l
--   Ω² {l} = Ω[_] {l = l} 2

--   compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a))
--   compose2 x y = horiz x y
--     where
--       variable
--         A : Set l
--         a b c : A
--         p q : a ≡ b
--         r s : b ≡ c
--         α : p ≡ q
--         β : r ≡ s

--       _∙ᵣ_ : p ≡ q → (r : b ≡ c) → p ∙ r ≡ q ∙ r
--       α ∙ᵣ refl = sym (lemma2∙1∙4.i1 _) ∙ α ∙ lemma2∙1∙4.i1 _

--       _∙ₗ_ : (q : a ≡ b) → r ≡ s → q ∙ r ≡ q ∙ s
--       refl ∙ₗ β = sym (lemma2∙1∙4.i2 _) ∙ β ∙ lemma2∙1∙4.i2 _

--       horiz : p ≡ q → r ≡ s → p ∙ r ≡ q ∙ s
--       horiz α β = (α ∙ᵣ _) ∙ (_ ∙ₗ β)

--   compose2-commutative : {l : Level} {A : Set l} {a : A} (x y : fst (Ω² (A , a))) → compose2 x y ≡ compose2 y x
--   compose2-commutative {l} {A} {a} x y = {!  !}

Definition 2.1.7 (pointed type)

Set* : (l : Level) → Set (lsuc l)
Set* l = Σ (Set l) (λ A → A)

Definition 2.1.8 (loop space)

Ω : {l : Level} → Set* l → Set* l
Ω (A , a) = (a ≡ a) , refl

Ω[_] : {l : Level} → ℕ → Set* l → Set* l
Ω[ zero ] (A , a) = (A , a)
Ω[ suc n ] (A , a) = Ω[ n ] (Ω (A , a))

2.2 Functions are functors

Lemma 2.2.1

ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A}
  → (f : A → B)
  → (p : x ≡ y)
  → f x ≡ f y
ap {l1} {l2} {A} {B} {x} {y} f p =
  J (λ x y p → f x ≡ f y) (λ x → refl) x y p

Lemma 2.2.2

Ap rules

module lemma2∙2∙2 where
  private
    variable
      A B C : Set

  i : {f : A → B} {x y z : A} (p : x ≡ y) (q : y ≡ z) → ap f (p ∙ q) ≡ ap f p ∙ ap f q
  i {f} {x} {y} {z} refl refl = refl

  ii : {f : A → B} {x y : A} (p : x ≡ y) → ap f (sym p) ≡ sym (ap f p)
  ii {f} {x} {y} refl = refl

  iii : (f : A → B) (g : B → C) {x y : A} (p : x ≡ y) → ap g (ap f p) ≡ ap (g ∘ f) p
  iii f g {x} {y} refl = refl

  iv : {x y : A} (p : x ≡ y) → ap id p ≡ p
  iv {x} {y} refl = refl

2.3 Type families are fibrations

transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
  → (P : A → Set l₂)
  → (p : x ≡ y)
  → P x → P y
transport {l₁} {l₂} {A} {x} {y} P refl = id

Lemma 2.3.2 (Path lifting property)

module lemma2∙3∙2 where
  lift : {A : Set} {P : A → Set} {x y : A}
    → (u : P x)
    → (p : x ≡ y)
    → (x , u) ≡ (y , transport P p u)
  lift {A} {P} {x} {y} u refl = refl

  pr₁ : {A : Set} {P : A → Set}
    {x y : A}
    {u : P x} {v : P y}
    (p : (x , u) ≡ (y , v))
    → x ≡ y
  pr₁ p = ap (λ (x , y) → x) p

  open ≡-Reasoning

  lift-prop : {A : Set} {P : A → Set} {x y : A} (u : P x) → (p : x ≡ y)
    → pr₁ (lift {A} {P} u p) ≡ p
  lift-prop {A} {P} {x} {y} u refl = refl

Lemma 2.3.4 (Dependent map)

apd : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂} {x y : A}
  → (f : (x : A) → P x)
  → (p : x ≡ y)
  → transport P p (f x) ≡ f y
apd {l₁} {l₂} {A} {P} {x} {y} f refl = refl

Lemma 2.3.5

transportconst : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
  → (B : Set l₂)
  → (p : x ≡ y)
  → (b : B)
  → transport (λ _ → B) p b ≡ b
transportconst {l₁} {l₂} {A} {x} {y} B refl b = refl

{-# REWRITE transportconst #-}

Equation 2.3.6

equation2∙3∙6 : {A B : Set} {x y : A} {p : x ≡ y} {f : A → B}
  → f x ≡ f y
  → transport (λ _ → B) p (f x) ≡ f y
equation2∙3∙6 {A} {B} {x} {y} {p} {f} q = transportconst B p (f x) ∙ q

Equation 2.3.7

equation2∙3∙7 : {A B : Set} {x y : A} {p : x ≡ y} {f : A → B}
  → transport (λ _ → B) p (f x) ≡ f y
  → f x ≡ f y
equation2∙3∙7 {A} {B} {x} {y} {p} {f} q = sym (transportconst B p (f x)) ∙ q

Lemma 2.3.8

lemma2∙3∙8 : {l : Level} {A B : Set l}
  → (f : A → B) 
  → {x y : A} 
  → (p : x ≡ y)
  → apd f p ≡ transportconst B p (f x) ∙ ap f p
lemma2∙3∙8 {l} {A} {B} f {x} {y} refl = refl

Lemma 2.3.9

lemma2∙3∙9 : {A : Set}
  → {x y z : A}
  → (P : A → Set)
  → (p : x ≡ y) → (q : y ≡ z) → (u : P x)
  → transport P q (transport P p u) ≡ transport P (p ∙ q) u
lemma2∙3∙9 {A} {x} {y} {z} P refl refl u = refl

Lemma 2.3.10

lemma2∙3∙10 : {l1 l2 : Level} {A B : Set l1}
  → (f : A → B)
  → (P : B → Set l2)
  → {x y : A}
  → (p : x ≡ y)
  → (u : P (f x))
  → transport (P ∘ f) p u ≡ transport P (ap f p) u
lemma2∙3∙10 {l} {A} {B} f P {x} {y} refl u = refl

Lemma 2.3.11

lemma2∙3∙11 : {A : Set} {P Q : A → Set}
  → (f : (x : A) → P x → Q x)
  → {x y : A} (p : x ≡ y) → (u : P x)
  → transport Q p (f x u) ≡ f y (transport P p u)
lemma2∙3∙11 {A} {P} {Q} f {x} {y} refl u = refl

2.4 Homotopies and equivalences

Definition 2.4.1 (Homotopy)

infixl 18 _∼_
_∼_ : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂}
  → (f g : (x : A) → P x)
  → Set (l₁ ⊔ l₂)
_∼_ {l₁} {l₂} {A} {P} f g = (x : A) → f x ≡ g x

Lemma 2.4.2

Homotopy forms an equivalence relation:

∼-refl : {A : Set} {P : A → Set}
  → (f : (x : A) → P x)
  → f ∼ f
∼-refl f x = refl

∼-sym : {A : Set} {P : A → Set}
  → {f g : (x : A) → P x}
  → f ∼ g → g ∼ f
∼-sym {f} {g} f∼g x = sym (f∼g x)

∼-trans : {l : Level} {A : Set l} {P : A → Set l}
  → {f g h : (x : A) → P x}
  → f ∼ g
  → g ∼ h
  → f ∼ h
∼-trans {l} {A} {P} {f} {g} {h} f∼g g∼h x = f∼g x ∙ g∼h x

Lemma 2.4.3

lemma2∙4∙3 : {A B : Set} {f g : A → B} (H : f ∼ g) {x y : A} (p : x ≡ y)
  → H x ∙ ap g p ≡ ap f p ∙ H y
lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} refl =
  let open ≡-Reasoning in
  begin
    H x ∙ ap g refl ≡⟨⟩
    H x ∙ refl ≡⟨ sym (lemma2∙1∙4.i1 (H x)) ⟩
    H x ≡⟨ lemma2∙1∙4.i2 (H x) ⟩
    refl ∙ H x ≡⟨⟩
    ap f refl ∙ H x ∎

Corollary 2.4.4

-- corollary2∙4∙4 : {A : Set} {f : A → A} {H : f ∼ id}
--   → (x : A)
--   → H (f x) ≡ ap f (H x)
-- corollary2∙4∙4 {A} {f} {H} x =
--   let g p = H x in
--   -- let naturality = lemma2∙4∙3 H x in 
--   {!   !}

Definition 2.4.6

record qinv {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) : Set (l1 ⊔ l2) where
  constructor mkQinv
  field
    g : B → A
    α : (f ∘ g) ∼ id
    β : (g ∘ f) ∼ id

Example 2.4.7

id-qinv : {l : Level} {A : Set l} → qinv {l} {l} {A} {A} id
id-qinv = mkQinv id (λ _ → refl) (λ _ → refl)

Example 2.4.8

module example2∙4∙8 where
  i : {A : Set} → {x y z : A} → (p : x ≡ y) → qinv (p ∙_)
  i {A} {x} {y} {z} p = mkQinv g forward backward
    where
      g = (sym p) ∙_
      forward : (_∙_ p ∘ g) ∼ id
      forward q = lemma2∙1∙4.iv p (sym p) q ∙ ap (_∙ q) (lemma2∙1∙4.ii2 p) ∙ sym (lemma2∙1∙4.i2 q)
      backward : (q : y ≡ z) → sym p ∙ (p ∙ q) ≡ q
      backward q = lemma2∙1∙4.iv (sym p) p q ∙ ap (_∙ q) (lemma2∙1∙4.ii1 p) ∙ sym (lemma2∙1∙4.i2 q)

  ii : {A : Set} → {x y z : A} → (p : x ≡ y) → qinv (_∙ p)
  ii {A} {x} {y} {z} p = mkQinv g forward backward
    where
      g : z ≡ y → z ≡ x
      g = _∙ (sym p)
      forward : (_∙ p ∘ g) ∼ id
      forward q = sym (lemma2∙1∙4.iv q (sym p) p) ∙ ap (q ∙_) (lemma2∙1∙4.ii1 p) ∙ sym (lemma2∙1∙4.i1 q)
      backward : (g ∘ _∙ p) ∼ id
      backward q = sym (lemma2∙1∙4.iv q p (sym p)) ∙ ap (q ∙_) (lemma2∙1∙4.ii2 p) ∙ sym (lemma2∙1∙4.i1 q)

Example 2.4.9

transport-qinv : {A : Set}
  → {x y : A}
  → (P : A → Set)
  → (p : x ≡ y)
  → qinv (transport P p)
transport-qinv P p = mkQinv (transport P (sym p))
  (λ py → 
    let wtf = lemma2∙3∙9 P (sym p) p py in
    trans wtf (ap (λ x → transport P x py) (lemma2∙1∙4.ii1 p))) 
  (λ px → 
    let wtf = lemma2∙3∙9 P p (sym p) px in
    trans wtf (ap (λ x → transport P x px) (lemma2∙1∙4.ii2 p)))

Definition 2.4.10

record isequiv {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) : Set (l1 ⊔ l2) where
  eta-equality
  constructor mkIsEquiv
  field
    g : B → A
    g-id : (f ∘ g) ∼ id
    h : B → A
    h-id : (h ∘ f) ∼ id

qinv-to-isequiv : {l1 l2 : Level} {A : Set l1} {B : Set l2}
  → {f : A → B}
  → qinv f
  → isequiv f
qinv-to-isequiv (mkQinv g α β) = mkIsEquiv g α g β

Still kinda shaky on this one, TODO study it later:

isequiv-to-qinv : {l : Level} {A B : Set l}
  → {f : A → B}
  → isequiv f
  → qinv f
isequiv-to-qinv {l} {A} {B} {f} (mkIsEquiv g g-id h h-id) =
  let
    γ : g ∼ h
    γ x = (sym (h-id (g x))) ∙ ap h (g-id x)

    β : (g ∘ f) ∼ id
    β x = γ (f x) ∙ h-id x 
  in
  mkQinv g g-id β

Definition 2.4.11

_≃_ : {l1 l2 : Level} → (A : Set l1) (B : Set l2) → Set (l1 ⊔ l2)
A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)

Lemma 2.4.12

module lemma2∙4∙12 where
  id-equiv : {l : Level} → (A : Set l) → A ≃ A
  id-equiv A = id , e
    where
      e : isequiv id
      e = mkIsEquiv id (λ _ → refl) id (λ _ → refl)

  sym-equiv : {A B : Set l} → (f : A ≃ B) → B ≃ A
  sym-equiv {A} {B} (f , eqv) =
    let (mkQinv g α β) = isequiv-to-qinv eqv
    in g , qinv-to-isequiv (mkQinv f β α)

  trans-equiv : {A B C : Set l} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
  trans-equiv {l} {A} {B} {C} (f , f-eqv) (g , g-eqv) =
    let
      (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
      (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv

      open ≡-Reasoning

      forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id
      forward c =
        begin
          ((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩
          (g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩
          (g ∘ id ∘ g-inv) c ≡⟨⟩
          (g ∘ g-inv) c ≡⟨ g-inv-left c ⟩
          id c ∎

      backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id
      backward a =
        begin
          ((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩
          (f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩
          (f-inv ∘ (id ∘ f)) a ≡⟨⟩
          (f-inv ∘ f) a ≡⟨ f-inv-right a ⟩
          id a ∎
      
    in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)

≃-Reasoning

module ≃-Reasoning where
  infix 1 begin_
  begin_ : {l : Level} {A B : Set l} → (A ≃ B) → (A ≃ B)
  begin x = x

  _≃⟨⟩_ : {l : Level} (A {B} : Set l) → A ≃ B → A ≃ B
  _ ≃⟨⟩ x≃y = x≃y

  infixr 2 _≃⟨⟩_ step-≃
  step-≃ : {l : Level} (A {B C} : Set l) → B ≃ C → A ≃ B → A ≃ C
  step-≃ _ y≃z x≃y = lemma2∙4∙12.trans-equiv x≃y y≃z
  syntax step-≃ x y≃z x≃y = x ≃⟨ x≃y ⟩ y≃z

  infix 3 _∎
  _∎ : {l : Level} (A : Set l) → (A ≃ A)
  A ∎ = lemma2∙4∙12.id-equiv A

2.5 The higher groupoid structure of type formers

Definition 2.5.1

definition2∙5∙1 : {B C : Set} {b b' : B} {c c' : C}
  → ((b , c) ≡ (b' , c')) ≃ ((b ≡ b') × (c ≡ c'))
definition2∙5∙1 {B = B} {C = C} {b = b} {b' = b'} {c = c} {c' = c'} =
  f , qinv-to-isequiv (mkQinv g forward backward)
  where
    f : {b b' : B} {c c' : C} → ((b , c) ≡ (b' , c')) → ((b ≡ b') × (c ≡ c'))
    f p = ap fst p , ap snd p

    g : {b b' : B} {c c' : C} → ((b ≡ b') × (c ≡ c')) → ((b , c) ≡ (b' , c'))
    g (refl , refl) = refl

    forward : {b b' : B} {c c' : C} → (f {b} {b'} {c} {c'} ∘ g {b} {b'} {c} {c'}) ∼ id
    forward (refl , refl) = refl
    
    backward : {b b' : B} {c c' : C} → (g {b} {b'} {c} {c'} ∘ f {b} {b'} {c} {c'}) ∼ id
    backward refl = refl

2.6 Cartesian product types

Definition 2.6.1

definition2∙6∙1 : {A B : Set l} {x y : A × B}
  → (p : x ≡ y)
  → (fst x ≡ fst y) × (snd x ≡ snd y)
definition2∙6∙1 p = ap fst p , ap snd p

Theorem 2.6.2

module theorem2∙6∙2 where
  private
    variable
      A B : Set l
      x y : A × B

  pair-≡ : (fst x ≡ fst y) × (snd x ≡ snd y) → x ≡ y
  pair-≡ (refl , refl) = refl

  backward : ((definition2∙6∙1 {A = A} {B = B} {x = x} {y = y}) ∘ pair-≡) ∼ id
  backward (refl , refl) = refl

  forward : (pair-≡ ∘ (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y})) ∼ id
  forward refl = refl

  theorem2∙6∙2 : isequiv (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y})
  theorem2∙6∙2 = qinv-to-isequiv (mkQinv pair-≡ backward forward)

  pair-≃ : {A B : Set l} {x y : A × B} → (x ≡ y) ≃ ((fst x ≡ fst y) × (snd x ≡ snd y))
  pair-≃ = definition2∙6∙1 , theorem2∙6∙2
open theorem2∙6∙2 using (pair-≡)

Theorem 2.6.4

theorem2∙6∙4 : {Z : Set} {A B : Z → Set} {z w : Z}
  → (p : z ≡ w) 
  → (x : A z × B z)
  → transport (λ z → A z × B z) p x ≡ (transport A p (Σ.fst x) , transport B p (Σ.snd x))
theorem2∙6∙4 {Z} {A} {B} {z} {w} refl x = refl

Theorem 2.6.5

theorem2∙6∙5 : {A A' B B' : Set} {g : A → A'} {h : B → B'} 
  → (x y : A × B)
  → (p : Σ.fst x ≡ Σ.fst y)
  → (q : Σ.snd x ≡ Σ.snd y)
  → let
      f : A × B → A' × B'
      f z = (g (Σ.fst z) , h (Σ.snd z)) 
    in
    ap f (pair-≡ (p , q)) ≡ pair-≡ (ap g p , ap h q)
theorem2∙6∙5 x y refl refl = refl

2.7 Σ-types

Theorem 2.7.2

Suppose that P : A → U is a type family over a type A and let w, w′ : ∑(x:A) P(x). Then there is an equivalence

theorem2∙7∙2 : {l : Level} {A : Set l} {P : A → Set l}
  → ((w @ (w1 , w2)) (w' @ (w'1 , w'2)) : Σ A P)
  → (w ≡ w') ≃ Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2)
theorem2∙7∙2 {l} {A} {P} (w @ (w1 , w2)) (w' @ (w'1 , w'2)) =
  f , qinv-to-isequiv (mkQinv g forwards backwards)
  where
    f : (w ≡ w') → Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2)
    f refl = refl , refl

    g : Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2) → (w ≡ w') 
    g (refl , refl) = refl

    forwards : (f ∘ g) ∼ id
    forwards (refl , refl) = refl

    backwards : (g ∘ f) ∼ id
    backwards refl = refl

Corollary 2.7.3

For z : ∑(x:A) P(x), we have z = (pr1(z), pr2(z)).

corollary2∙7∙3 : {A : Set} {P : A → Set}
  → (z @ (a , b) : Σ A P)
  → z ≡ (a , b)
corollary2∙7∙3 z = refl

Theorem 2.7.4

-- module theorem2∙7∙4 where
--   private
--     TF = λ P Q x → Σ (P x) (λ u → Q (x , u))

--   theorem2∙7∙4 : {A : Set} {P : A → Set}
--     → (Q : Σ A P → Set)
--     → {x y : A}
--     → (p : x ≡ y)
--     → (u z : Σ (P x) (λ u → Q (x , u)))
--     → transport (λ r → Σ {!    !} {!   !}) p (u , z) ≡ (transport {!   !} p u , transport {! TF P Q  !} (pair-≡ (p , refl)) z)
--   theorem2∙7∙4 Q refl u z = refl

2.8 The unit type

Theorem 2.8.1

theorem2∙8∙1 : (x y : 𝟙) → (x ≡ y) ≃ 𝟙
theorem2∙8∙1 x y = func x y , equiv x y
  where
    func : (x y : 𝟙) → (x ≡ y) → 𝟙
    func x y _ = tt

    rev : (x y : 𝟙) → 𝟙 → (x ≡ y)
    rev tt tt _ = refl

    backwards : (x y : 𝟙) → (func x y ∘ rev x y) ∼ id
    backwards tt tt tt = refl

    forwards : (x y : 𝟙) → (rev x y ∘ func x y) ∼ id
    forwards tt tt refl = refl

    equiv : (x y : 𝟙) → isequiv (func x y)
    equiv x y = record
      { g = rev x y
      ; g-id = backwards x y
      ; h = rev x y
      ; h-id = forwards x y
      }

2.9 Π-types and the function extensionality axiom

Lemma 2.9.1

postulate
  lemma2∙9∙1 : {A : Set} {B : A → Set}
    → (f g : (x : A) → B x)
    → (f ≡ g) ≃ ((x : A) → f x ≡ g x)

Lemma 2.9.2

happly : {A : Set l} {B : A → Set l2}
  → {f g : (x : A) → B x}
  → (p : f ≡ g)
  → (x : A)
  → f x ≡ g x
happly {A} {B} {f} {g} p x = ap (λ h → h x) p

Axiom 2.9.3 (Function extensionality)

module axiom2∙9∙3 where
  private
    variable
      A : Set l
      B : A → Set l2
      f g : (x : A) → B x

  postulate
    funext : ((x : A) → f x ≡ g x) → f ≡ g
    propositional-computation : (h : (x : A) → f x ≡ g x) → happly (funext h) ≡ h
    propositional-uniqueness : (p : f ≡ g) → funext (happly p) ≡ p

  happly-isequiv : isequiv (happly {l} {l2} {A} {B} {f} {g})
  happly-isequiv = qinv-to-isequiv (mkQinv funext propositional-computation propositional-uniqueness)

  happly-equiv : (f ≡ g) ≃ ((x : A) → f x ≡ g x)
  happly-equiv = happly , happly-isequiv

Equation 2.9.4

equation2∙9∙4 : {l1 l2 : Level} {X : Set l1} {x1 x2 : X} 
  → {A B : X → Set l2}
  → (f : A x1 → B x1)
  → (p : x1 ≡ x2)
  → transport (λ x → A x → B x) p f ≡ λ x → transport B p (f (transport A (sym p) x))
equation2∙9∙4 {l1} {l2} {X} {x1} {x2} {A} {B} f refl = refl

Equation 2.9.5

module equation2∙9∙5 {X : Set} {x1 x2 : X} where
  Π : (A : X → Set) → (B : (x : X) → A x → Set) → X → Set
  Π A B x = (a : A x) → B x a

  hat : {A : X → Set} → (B : (x : X) → A x → Set) → (Σ X A) → Set
  hat B (fst , snd) = B fst snd

  --- I have no idea where this goes but this definitely needs to exist
  pair-≡-d : {A : Set} {B : A → Set} {a1 a2 : A} {b1 : B a1} {b2 : B a2}
    → (p : a1 ≡ a2) → (transport B p b1 ≡ b2) → (a1 , b1) ≡ (a2 , b2)
  pair-≡-d refl refl = refl

  equation2∙9∙5 : (A : X → Set)
    → (B : (x : X) → A x → Set)
    → (f : (a : A x1) → B x1 a)
    → (p : x1 ≡ x2)
    → (a : A x2)
    → transport (Π A B) p f a ≡ transport (hat B) (sym (pair-≡-d (sym p) refl)) (f (transport A (sym p) a))
  equation2∙9∙5 A B f refl a = refl

Lemma 2.9.6

-- module lemma2∙9∙6 where

--   P : (x : X) → Set
--   P x = A x → B x

--   lemma2∙9∙6 : (p : x ≡ y)
--     → (f : A x → B x)
--     → (g : A y → B y)
--     → (transport P p f ≡ g) ≃ ((a : A x) → transport B p (f a) ≡ g (transport A p a))
--   lemma2∙9∙6 p f g = func , qinv-to-isequiv (mkQinv {!   !} {!   !} {!   !})
--     where
--       func : (transport P p f ≡ g) → (a : A x) → transport B p (f a) ≡ g (transport A p a)
--       func p1 a = J (λ x y p' → {!   !} ≡ y (transport A {!   !} a)) {!   !} (transport P p f) g p1

2.10 Universes and the univalence axiom

Lemma 2.10.1

idtoeqv : {A B : Set l} → (A ≡ B) → (A ≃ B)
idtoeqv refl = transport id refl , qinv-to-isequiv (mkQinv id id-homotopy id-homotopy)
  where
    id-homotopy : (id ∘ id) ∼ id
    id-homotopy x = refl

Axiom 2.10.3 (Univalence)

module axiom2∙10∙3 where
  private
    variable
      A B : Set l
  postulate
    ua : (A ≃ B) → (A ≡ B)
    propositional-computation : (f : A ≃ B) → idtoeqv (ua f) ≡ f
    propositional-uniqueness : (p : A ≡ B) → p ≡ ua (idtoeqv p)

  ua-eqv : {A B : Set l} → (A ≃ B) ≃ (A ≡ B)
  ua-eqv = ua , qinv-to-isequiv
    (mkQinv idtoeqv
      (λ p → sym (propositional-uniqueness p))
      (λ e → propositional-computation e))

open axiom2∙10∙3

Lemma 2.10.5

-- lemma2∙10∙5 : {l : Level} {A : Set l} {B : A → Set l}
--   → (x y : A)
--   → (p : x ≡ y)
--   → (u : B x)
--   → transport B p u ≡ transport id (ap B p) u

2.11 Identity Type

Theorem 2.11.1

-- theorem2∙11∙1 : {A B : Set}
--   → (eqv @ (f , f-eqv) : A ≃ B)
--   → (a a' : A)
--   → (a ≡ a') ≃ (f a ≡ f a')
-- theorem2∙11∙1 (f , f-eqv) a a' =
--   let
--     open ≡-Reasoning
--     mkQinv g α β = isequiv-to-qinv f-eqv
--     inv : (f a ≡ f a') → a ≡ a'
--     inv p = (sym (β a)) ∙ (ap g p) ∙ (β a')
--     backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
--     backward q = begin
--       ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a')  ⟩
--       ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
--       ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
--       id q ∎
--     forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
--     forward p = begin
--       (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩
--       (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {!   !} ⟩
--       -- (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {!   !} ⟩
--       id p ∎
--     eqv = mkQinv inv backward forward
--   in
--   ap f , qinv-to-isequiv eqv

Lemma 2.11.2

module lemma2∙11∙2 where
  open ≡-Reasoning

  i : {l : Level} {A : Set l} {a x1 x2 : A}
    → (p : x1 ≡ x2)
    → (q : a ≡ x1)
    → transport (λ y → a ≡ y) p q ≡ q ∙ p
  i {l} {A} {a} {x1} {x2} refl refl = refl

  ii : {l : Level} {A : Set l} {a x1 x2 : A}
    → (p : x1 ≡ x2)
    → (q : x1 ≡ a)
    → transport (λ y → y ≡ a) p q ≡ sym p ∙ q
  ii {l} {A} {a} {x1} {x2} refl refl = refl

  iii : {l : Level} {A : Set l} {a x1 x2 : A}
    → (p : x1 ≡ x2)
    → (q : x1 ≡ x1)
    → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
  iii refl q =
    let
      a = i1 q
      b = i2 q
    in b ∙ ap (refl ∙_) a
    where open lemma2∙1∙4

Theorem 2.11.3

theorem2∙11∙3 : {A B : Set} → {f g : A → B} → {a a' : A}
  → (p : a ≡ a')
  → (q : f a ≡ g a)
  → transport (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ (ap g p)
theorem2∙11∙3 {A} {B} {f} {g} {a} {a'} refl q =
  let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q) in
  lemma2∙1∙4.i2 q ∙ helper

Theorem 2.11.4

theorem2∙11∙4 : {A : Set} {B : A → Set} {f g : (x : A) → B x} {a a' : A}
  → (p : a ≡ a')
  → (q : f a ≡ g a)
  → transport (λ x → f x ≡ g x) p q ≡ sym (apd f p) ∙ ap (transport B p) q ∙ apd g p
theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} refl q = 
  let
    open ≡-Reasoning
    q2 = ap id q
    q≡q2 : q ≡ q2
    q≡q2 = J (λ a b p → p ≡ ap id p) (λ x → refl) (f a) (g a) q
  in
  begin
    transport (λ z → f z ≡ g z) refl q ≡⟨⟩
    q ≡⟨ q≡q2 ⟩
    q2 ≡⟨ (let helper = ap (λ p → refl ∙ p) (lemma2∙1∙4.i1 q2) in lemma2∙1∙4.i2 q2 ∙ helper) ⟩
    refl ∙ ap (transport B refl) q ∙ refl ∎

Theorem 2.11.5

-- theorem2∙11∙5 : {A : Set} {a a' : A}
--   → (p : a ≡ a')
--   → (q : a ≡ a)
--   → (r : a' ≡ a')
--   → (transport (λ y → y ≡ y) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r)
-- theorem2∙11∙5 refl q r = f , qinv-to-isequiv (mkQinv g {!   !} {!   !})
--   where
--     f : q ≡ r → q ∙ refl ≡ refl ∙ r
--     f p = sym (lemma2∙1∙4.i1 q) ∙ p ∙ lemma2∙1∙4.i2 r

--     g : q ∙ refl ≡ refl ∙ r → id q ≡ r
--     g p = (lemma2∙1∙4.i1 q) ∙ p ∙ sym (lemma2∙1∙4.i2 r)

--     -- forward : (f ∘ g) ∼ id

2.12 Coproducts

Theorem 2.12.5

module theorem2∙12∙5 {A B : Set l} (a₀ : A) where
  open import HottBook.CoreUtil using (Lift)

  code : A + B → Set l
  code (inl a) = a₀ ≡ a
  code (inr b) = Lift ⊥

  encode : (x : A + B) → (p : inl a₀ ≡ x) → code x
  encode x p = transport code p refl

  decode : (x : A + B) → code x → inl a₀ ≡ x
  decode (inl x) c = ap inl c

  backward : (x : A + B) → (c : code x) → encode x (decode x c) ≡ c
  backward (inl x) c =
    let open ≡-Reasoning in begin
      encode (inl x) (decode (inl x) c) ≡⟨⟩
      transport code (ap inl c) refl ≡⟨ sym (lemma2∙3∙10 inl code c refl) ⟩
      transport (λ a → a₀ ≡ a) c refl ≡⟨ lemma2∙11∙2.i c refl ⟩
      refl ∙ c ≡⟨ sym (lemma2∙1∙4.i2 c) ⟩
      c ∎

  forward : (x : A + B) → (p : inl a₀ ≡ x) → decode x (encode x p) ≡ p
  forward x p = based-path-induction (inl a₀) (λ x1 p1 → decode x1 (encode x1 p1) ≡ p1) refl x p

  theorem2∙12∙5 : (x : A + B) → (inl a₀ ≡ x) ≃ (code x)
  theorem2∙12∙5 x = encode x , qinv-to-isequiv (mkQinv (decode x) (backward x) (forward x))

Remark 2.12.6

module remark2∙12∙6 where
  true≢false : true ≢ false
  true≢false p = genBot tt
    where
      Bmap : 𝟚 → Set
      Bmap true = 𝟙
      Bmap false = ⊥

      genBot : 𝟙 → ⊥
      genBot = transport Bmap p

2.13 Natural numbers

Theorem 2.13.1

For all we have .

module theorem2∙13∙1 where
  open ≡-Reasoning

  code : ℕ → ℕ → Set
  code zero zero = 𝟙
  code zero (suc y) = ⊥
  code (suc x) zero = ⊥
  code (suc x) (suc y) = code x y

  r : (n : ℕ) → code n n
  r zero = tt
  r (suc n) = r n

  encode : (m n : ℕ) → m ≡ n → code m n
  encode m n p = transport (code m) p (r m)

  decode : (m n : ℕ) → code m n → m ≡ n
  decode zero zero tt = refl
  decode (suc m) (suc n) c = ap suc (decode m n c)

  backward : (m n : ℕ) → (c : code m n) → encode m n (decode m n c) ≡ c
  backward zero zero tt = refl
  backward (suc m) (suc n) c =
    begin
      encode (suc m) (suc n) (decode (suc m) (suc n) c) ≡⟨⟩
      encode (suc m) (suc n) (ap suc (decode m n c)) ≡⟨⟩
      transport (code (suc m)) (ap suc (decode m n c)) (r (suc m)) ≡⟨ sym (lemma2∙3∙10 suc (code (suc m)) (decode m n c) (r (suc m))) ⟩
      transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m)) ≡⟨⟩
      transport (code m) (decode m n c) (r m) ≡⟨⟩
      encode m n (decode m n c) ≡⟨ backward m n c ⟩
      c ∎

  forward : (m n : ℕ) → (p : m ≡ n) → decode m n (encode m n p) ≡ p
  forward m n refl = f m
    where
      f : (x : ℕ) → decode x x (r x) ≡ refl
      f zero = refl
      f (suc x) = ap (ap suc) (f x)

  theorem2∙13∙1 : (m n : ℕ) → (m ≡ n) ≃ code m n
  theorem2∙13∙1 m n = encode m n , qinv-to-isequiv (mkQinv (decode m n) (backward m n) (forward m n))

2.14 Example: equality of structures

Definition 2.14.1

SemigroupStr : (A : Set l) → Set l
SemigroupStr A = Σ (A → A → A) (λ m → (x y z : A) → m x (m y z) ≡ m (m x y) z)

Semigroup : Set (lsuc l)
Semigroup {l = l} = Σ (Set l) SemigroupStr

2.15 Universal properties

Definition 2.15.1

definition2∙15∙1 : {X A B : Set}
  → (X → A × B)
  → (X → A) × (X → B)
definition2∙15∙1 f = Σ.fst ∘ f , Σ.snd ∘ f

Theorem 2.15.2

theorem2∙15∙2 : {X A B : Set} → isequiv (definition2∙15∙1 {X} {A} {B})
theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl)
  where
    g : (X → A) × (X → B) → (X → A × B)
    g (f1 , f2) = λ x → (f1 x , f2 x)

Equation 2.15.4

equation2∙15∙4 : {X : Set l} {A B : X → Set l}
  → ((x : X) → A x × B x)
  → ((x : X) → A x) × ((x : X) → B x)
equation2∙15∙4 f = ((λ x → Σ.fst (f x)) , λ x → Σ.snd (f x))

Theorem 2.15.5

theorem2∙15∙5 : {X : Set l} {A B : X → Set l} → isequiv (equation2∙15∙4 {X = X} {A = A} {B = B})
theorem2∙15∙5 {X = X} {A = A} {B = B} = qinv-to-isequiv (mkQinv g forward backward)
  where
    g : ((x : X) → A x) × ((x : X) → B x) → (x : X) → A x × B x
    g (f , g) x = f x , g x

    forward : (p : ((x : X) → A x) × ((x : X) → B x)) → equation2∙15∙4 (g p) ≡ p
    forward p = refl

    backward : (f : (x : X) → A x × B x) → g (equation2∙15∙4 f) ≡ f
    backward f = funext λ x → refl
      where open axiom2∙9∙3

Equation 2.15.6

equation2∙15∙6 : {X : Set} {A : X → Set} {P : (x : X) → A x → Set} 
  → ((x : X) → Σ (A x) (P x))
  → Σ ((x : X) → A x) (λ g → (x : X) → P x (g x))
equation2∙15∙6 f = (λ x → fst (f x)) , λ x → snd (f x)

Theorem 2.15.7

theorem2∙15∙7 : {X : Set} {A : X → Set} {P : (x : X) → A x → Set} → isequiv (equation2∙15∙6 {X = X} {A = A} {P = P})
theorem2∙15∙7 {X} {A} {P} = qinv-to-isequiv (mkQinv g forward backward)
  where
    open axiom2∙9∙3

    g : Σ ((x : X) → A x) (λ g → (x : X) → P x (g x)) → (x : X) → Σ (A x) (P x)
    g (f1 , f2) x = f1 x , f2 x
    
    forward : (equation2∙15∙6 ∘ g) ∼ id
    forward (f1 , f2) = Σ-≡ (refl , refl)

    backward : (g ∘ equation2∙15∙6) ∼ id
    backward f = funext λ x → refl
Imports 
{-# OPTIONS --rewriting #-}

module HottBook.Chapter3 where

open import Agda.Primitive
open import HottBook.Chapter1
open import HottBook.Chapter1Util
open import HottBook.Chapter2
open import HottBook.Chapter2Util
open import HottBook.Chapter3Definition331 public
open import HottBook.Chapter3Lemma333 public
open import HottBook.CoreUtil
open import HottBook.Util

private
  variable
    l : Level

3.1 Sets and n-types

Definition 3.1.1

isSet : (A : Set l) → Set l
isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q

Example 3.1.2

𝟙-is-Set : isSet 𝟙
𝟙-is-Set tt tt refl refl = refl

𝟙-isProp : isProp 𝟙
𝟙-isProp x y = 
  let (_ , equiv) = theorem2∙8∙1 x y in
  isequiv.g equiv tt

Example 3.1.3

⊥-is-Set : isSet ⊥
⊥-is-Set () () p q

Example 3.1.4

ℕ-is-Set : isSet ℕ
ℕ-is-Set x y p q = wtf4
  where
    open theorem2∙13∙1
    open axiom2∙10∙3
    open isequiv

    cp = encode x y p
    cq = encode x y q

    wtf : (x y : ℕ) → (p q : code x y) → p ≡ q
    wtf zero zero p q = 𝟙-isProp p q
    wtf (suc x) (suc y) p q = wtf x y p q

    wtf2 : (x y : ℕ) → (p q : code x y) → (p ≡ q) → (decode x y p) ≡ (decode x y q)
    wtf2 x y p q r = ap (decode x y) r

    wtf3 : {x y : ℕ} → (p : x ≡ y) → (p ≡ decode x y (encode x y p))
    wtf3 {x} {y} p = sym (theorem2∙13∙1 x y .snd .h-id p)

    wtf4 : p ≡ q
    wtf4 = (wtf3 p) ∙ wtf2 x y cp cq (wtf x y cp cq) ∙ sym (wtf3 q)

Example 3.1.5

×-Set : {A B : Set l} → isSet A → isSet B → isSet (A × B)
×-Set {A = A} {B = B} A-set B-set (xa , xb) (ya , yb) p q = goal
  where
    open theorem2∙6∙2
    open axiom2∙10∙3
    open isequiv

    p' = theorem2∙6∙2 .h-id p
    q' = theorem2∙6∙2 .h-id q

    pr1 : ap fst p ≡ ap fst q
    pr1 = A-set xa ya (ap fst p) (ap fst q)
    pr2 : ap snd p ≡ ap snd q
    pr2 = B-set xb yb (ap snd p) (ap snd q)

    goal = sym p' ∙ ap pair-≡ (pair-≡ (pr1 , pr2)) ∙ q'

Example 3.1.6

example3∙1∙6 : {A : Set} {B : A → Set} → ((x : A) → isSet (B x)) → isSet ((x : A) → B x)
example3∙1∙6 {A} Bset f g p q =
  let
    open axiom2∙9∙3

    p' = funext λ x → happly p x
    q' = funext λ x → happly q x

    p≡p' : p ≡ p'
    p≡p' = sym (propositional-uniqueness p)

    q≡q' : q ≡ q'
    q≡q' = sym (propositional-uniqueness q)

    lol : (x : A) → happly p x ≡ happly q x
    lol x = Bset x (f x) (g x) (happly p x) (happly q x)

    lol2 : happly p ≡ happly q
    lol2 = funext lol
  in sym (propositional-uniqueness p) ∙ ap funext lol2 ∙ (propositional-uniqueness q)

Definition 3.1.7

is-1-type : (A : Set l) → Set l
is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s

Lemma 3.1.8

"levels are upward-closed"

lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
lemma3∙1∙8 {A} A-set x y p q r s =
  let 
    g : (q : x ≡ y) → p ≡ q 
    g q = A-set x y p q

    what : (q' : x ≡ y) → (r : q ≡ q') → transport (λ p' → p ≡ p') r (g q) ≡ g q'
    what q' r = apd g r

    what2 : (q' : x ≡ y) → (r : q ≡ q') → (g q) ∙ r ≡ g q'
    what2 q' r = sym (lemma2∙11∙2.i r (g q)) ∙ what q' r

    what3 : (q' : x ≡ y) → (r s : q ≡ q') → (g q) ∙ r ≡ (g q) ∙ s
    what3 q' r s = what2 q' r ∙ sym (what2 q' s)

    what4 : (g q) ∙ (sym r) ≡ (g q) ∙ (sym s)
    what4 = what3 p (sym r) (sym s) 

  in what5
  where
    -- TODO: Dont' feel like proving this for now, will revisit later
    postulate
      what5 : r ≡ s

Example 3.1.9

example3∙1∙9 : ∀ {l} → ¬ (isSet (Set l))
example3∙1∙9 p = remark2∙12∙6.true≢false lol
  where
    open axiom2∙10∙3

    f-path : Bool ≡ Bool
    f-path = ua Bool-neg-equiv

    bogus : id ≡ Bool-neg
    bogus =
      let
        helper : f-path ≡ refl
        helper = p Bool Bool f-path refl

        wtf : idtoeqv f-path ≡ idtoeqv refl
        wtf = ap idtoeqv helper

        wtf2 : Σ.fst (idtoeqv (ua Bool-neg-equiv)) ≡ id
        wtf2 = ap Σ.fst wtf

        wtf3 : Σ.fst (idtoeqv (ua Bool-neg-equiv)) ≡ Bool-neg
        wtf3 = ap Σ.fst (propositional-computation Bool-neg-equiv)

        wtf4 : Bool-neg ≡ id
        wtf4 = sym wtf3 ∙ wtf2
      in sym wtf4

    lol : true ≡ false
    lol = ap (λ f → Lift.lower (f (lift true))) bogus

3.2 Propositions as types?

Theorem 3.2.2

TODO: Study this more

theorem3∙2∙2 : ((A : Set l) → ¬ ¬ A → A) → ⊥
theorem3∙2∙2 double-neg = conclusion
  where
    open axiom2∙10∙3

    bool = Lift 𝟚

    negl : bool → bool
    negl (lift true) = lift false
    negl (lift false) = lift true

    negl-homotopy : (negl ∘ negl) ∼ id
    negl-homotopy (lift true) = refl
    negl-homotopy (lift false) = refl

    e : bool ≃ bool
    e = negl , qinv-to-isequiv (mkQinv negl negl-homotopy negl-homotopy)

    p : bool ≡ bool
    p = ua e

    fbool : ¬ ¬ bool → bool
    fbool = double-neg bool

    apdfp : transport (λ A → ¬ ¬ A → A) p fbool ≡ fbool
    apdfp = apd double-neg p

    u : ¬ ¬ bool
    u = λ p → p (lift true)

    foranyu : transport (λ A → ¬ ¬ A → A) p fbool u ≡ fbool u
    foranyu = happly apdfp u

    what : transport (λ A → ¬ (¬ A) → A) p fbool u ≡ transport (λ X → X) p (fbool (transport (λ X → ¬ (¬ X)) (sym p) u))
    what =
      let
        x = equation2∙9∙4 {A = λ X → ¬ ¬ X} {B = λ X → X} fbool p
        in ap (λ f → f u) x

    allsame : (u v : ¬ ¬ bool) → (x : ¬ bool) → u x ≡ v x
    allsame u v x = rec-⊥ (u x)

    postulate
      allsamef : ∀ {l} {bool : Set l} → (u v : ¬ ¬ bool) → u ≡ v
    -- allsamef {l} {bool} u v = {!  !}
    
    all-dn-u-same : transport (λ A → ¬ ¬ A) (sym p) u ≡ u
    all-dn-u-same = allsamef (transport (λ A → ¬ ¬ A) (sym p) u) u

    nextStep : transport (λ A → A) p (fbool u) ≡ fbool u
    nextStep =
      let x = ap (λ x → transport id p (fbool x)) all-dn-u-same in
      let y = what ∙ x in
      sym y ∙ foranyu

    postulate
      huhh : (Σ.fst e) (fbool u) ≡ fbool u

    finalStep : (x : bool) → ¬ ((Σ.fst e) x ≡ x)
    finalStep (lift true) p = 
      let wtf = ap (λ f → Lift.lower f) p in
      remark2∙12∙6.true≢false (sym wtf)
    finalStep (lift false) p =
      let wtf = ap (λ f → Lift.lower f) p in
      remark2∙12∙6.true≢false wtf

    conclusion : ⊥
    conclusion = finalStep (fbool u) huhh

Corollary 3.2.7

corollary3∙2∙7 : ((A : Set) → (A + (¬ A))) → ⊥
corollary3∙2∙7 g = theorem3∙2∙2 helper
  where
    open WithAbstractionUtil

    helper : (A : Set) → (¬ (¬ A)) → A
    helper A u with g A | inspect g A
    helper A u | inl a | ingraph q = a
    helper A u | inr w | ingraph q = rec-⊥ (u w)

3.3 Mere propositions

Definition 3.3.1

isProp : (P : Set l) → Set l
isProp P = (x y : P) → x ≡ y

Lemma 3.3.2

lemma3∙3∙2 : {P : Set}
  → isProp P
  → (x0 : P)
  → P ≃ 𝟙
lemma3∙3∙2 {P} pp x0 =
  lemma3∙3∙3 pp 𝟙-isProp (λ _ → tt) (λ _ → x0)

Lemma 3.3.3

lemma3∙3∙3 : {P Q : Set}
  → isProp P
  → isProp Q
  → (P → Q)
  → (Q → P)
  → P ≃ Q
lemma3∙3∙3 pp qq f g = f , qinv-to-isequiv (mkQinv g backward forward)
  where
    forward : (g ∘ f) ∼ id
    forward x = pp ((g ∘ f) x) (id x)

    backward : (f ∘ g) ∼ id
    backward x = qq ((f ∘ g) x) (id x)

Lemma 3.3.4

lemma3∙3∙4 : {A : Set} → isProp A → isSet A
lemma3∙3∙4 {A} f x y p q =
  let
    g : (y : A) → x ≡ y
    g y = f x y

    step : (y z : A) → (p : y ≡ z) → transport (λ w → x ≡ w) p (g y) ≡ g z
    step y z p = apd g p

    step2 : (y z : A) → (p : y ≡ z) → (g y) ∙ p ≡ g z
    step2 y z p = sym (lemma2∙11∙2.i p (g y)) ∙ step y z p

    step3 : (y z : A) → (p : y ≡ z) → p ≡ sym (g y) ∙ (g z)
    step3 y z p =
      lemma2∙1∙4.i2 p
      ∙ ap (λ q → q ∙ p) (sym (lemma2∙1∙4.ii1 (g y)))
      ∙ sym (lemma2∙1∙4.iv (sym (g y)) (g y) p)
      ∙ ap (λ q → sym (g y) ∙ q) (step2 y z p)

    step4 = step3 x y p
    step5 = step3 x y q
  in step4 ∙ sym step5

Lemma 3.3.5

module lemma3∙3∙5 where
  open axiom2∙9∙3

  i : {A : Set} → isProp (isProp (A))
  i f g = funext λ x → funext λ y → (lemma3∙3∙4 f) x y (f x y) (g x y)

  ii : {A : Set} → isProp (isSet (A))
  ii f g = funext λ x → funext λ y → funext λ p → funext λ q →
    (lemma3∙1∙8 f) x y p q (f x y p q) (g x y p q)

3.4 Classical vs. intuitionistic logic

Definition 3.4.1 (LEM)

LEM : {l : Level} → Set (lsuc l)
LEM {l} = (A : Set l) → (isProp A) → (A + (¬ A))

Definition 3.4.2 (Double negation)

double-negation : {l : Level} → Set (lsuc l)
double-negation {l} = (A : Set l) → isProp A → (¬ ¬ A → A)

Definition 3.4.3

module definition3∙4∙3 where
  data decidable (A : Set) : Set where
    proof : A + (¬ A) → decidable A

  data decidable-family {A : Set} (B : A → Set) : Set where
    proof : (a : A) → (B a + (¬ (B a))) → decidable-family B

  decidable-equality : (A : Set) → Set
  decidable-equality A = (a b : A) → (a ≡ b) + (¬ a ≡ b)

3.5 Subsets and propositional resizing

Lemma 3.5.1

lemma3∙5∙1 : {A : Set} {P : A → Set}
  → ((x : A) → isProp (P x))
  → (u v : Σ A P)
  → (Σ.fst u ≡ Σ.fst v)
  → u ≡ v
lemma3∙5∙1 {P = P} f u v p = 
  let
    eqv = theorem2∙7∙2 u v
    func = Σ.fst (lemma2∙4∙12.sym-equiv eqv)
    prf = p , f (Σ.fst v) (transport P p (Σ.snd u)) (Σ.snd v)
  in func prf

SubProp : (l : Level) → Set (lsuc l)
SubProp l = Σ (Set l) isProp

equation3∙5∙4 : {l : Level} → SubProp l → SubProp (lsuc l)
equation3∙5∙4 {l} (A , Aprop) = Lift A , λ x y → ap lift (Aprop (Lift.lower x) (Lift.lower y))

Axiom 3.5.5

Not able to be proved, but is consistent

postulate
  propResizingEquiv : {l : Level} → isequiv (equation3∙5∙4 {l})

3.6 The logic of mere propositions

Example 3.6.1

example3∙6∙1 : {A B : Set} → isProp A → isProp B → isProp (A × B)
example3∙6∙1 {A} {B} Aprop Bprop =
  λ (x1 , x2) (y1 , y2) → Σ-≡ (Aprop x1 y1 , transportconst B (Aprop x1 y1) x2 ∙ Bprop x2 y2)

Example 3.6.2

example3∙6∙2 : {A : Set} {B : A → Set} → ((x : A) → isProp (B x)) → isProp ((x : A) → B x)
example3∙6∙2 {A} {B} allProps = λ f g → funext λ x → allProps x (f x) (g x)
  where open axiom2∙9∙3

3.7 Propositional truncation

module section3∙7 where
  postulate
    ∥_∥ : Set l → Set l
    ∣_∣ : {A : Set l} → A → ∥ A ∥
    trunc-witness : {A : Set l} → isProp (∥ A ∥)
    
    rec-trunc : {l l2 : Level} {A : Set l} {B : Set l2} → isProp B → (f : A → B) → ∥ A ∥ → B

    rec-trunc-1 : {l l2 : Level} {A : Set l} {B : Set l2}
      → (Bprop : isProp B)
      → (f : A → B)
      → (a : A)
      → rec-trunc Bprop f (∣ a ∣) ≡ f a
    {-# REWRITE rec-trunc-1 #-}

  -- ind-trunc : {A : Set} → {B : ∥ A ∥ → Set}
  --   → ((x : ∥ A ∥) → isProp (B x))
  --   → ((a : A) → B (∣ a ∣))
  --   → (x : ∥ A ∥) → B x
  -- ind-trunc f g x = rec-trunc (f x) (λ a → {! g x  !}) x

open section3∙7 public

Definition 3.7.1

module definition3∙7∙1 where
  ⊤ = 𝟙
  _∧_ = _×_
  _⇒_ : (P Q : Set l) → Set l
  P ⇒ Q = P → Q
  _⇔_ = _≡_
  -- ¬_ : (P : Set l) → Set l
  -- ¬ P = P → ⊥
  _∨_ : (P Q : Set l) → Set l
  P ∨ Q = ∥ P + Q ∥
  forall' : (A : Set l) → (P : A → Set l) → Set l
  forall' A P = (x : A) → P x
  exists' : (A : Set l) → (P : A → Set l) → Set l
  exists' A P = ∥ Σ A P ∥

3.8 The axiom of choice

Definition 3.8.1

module definition3∙8∙1 where
  private
    variable
      X : Set
      A : X → Set
      P : (x : X) → A x → Set

  postulate
    axiom-of-choice : (prop : (x : X) → (a : A x) → isProp (P x a))
      → ((x : X) → ∥ Σ (A x) (P x) ∥)
      → ∥ Σ ((x : X) → A x) (λ g → (x : X) → P x (g x)) ∥
open definition3∙8∙1 public

Lemma 3.8.2

-- module lemma3∙8∙2 where
--   definition3∙8∙3 : {X : Set} → (Y : X → Set) → ((x : X) → isSet (Y x)) → ((x : X) → ∥ (Y x) ∥) → ∥ ((x : X) → Y x) ∥
--   definition3∙8∙3 {X} Y allYSet = {!   !}

3.9 The principle of unique choice

Lemma 3.9.1

lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop witness ∣_∣ rec-func
  where
    rec-func : ∥ P ∥ → P
    rec-func = rec-trunc Pprop id

    witness : isProp ∥ P ∥
    witness = trunc-witness

Corollary 3.9.2

Principle of unique choice

-- corollary3∙9∙2 : {A : Set} {P : A → Set}
--   → ((x : A) → isProp (P x))
--   → ((x : A) → ∥ P x ∥)
--   → (x : A) → P x
-- corollary3∙9∙2 {A = A} {P = P} assump1 assump2 x = 
--   let rec = trunc-rec A (assump1 x) (λ y → {!assump2 x   !}) (∣ x ∣)
--   in rec

3.11 Contractibility

Definition 3.11.1

isContr : (A : Set l) → Set l
isContr A = Σ A (λ a → (x : A) → a ≡ x)

Lemma 3.11.3

module lemma3∙11∙3 where
  record properties (A : Set l) : Set l where
    constructor mkProperties
    field
      i : isContr A
      ii : A × isProp A
      iii : A ≃ 𝟙

  i : {A : Set} → isContr A → properties A
  i Acontr @ (a , aEq) = mkProperties p1 p2 p3
    where
      p1 = Acontr
      p2 = a , λ x y → sym (aEq x) ∙ aEq y

      forward : ((λ _ → tt) ∘ (λ _ → a)) ∼ id
      forward tt = refl
      p3 = (λ _ → tt) , qinv-to-isequiv (mkQinv (λ _ → a) forward aEq)

  ii : {A : Set} → A × isProp A → properties A
  ii Aprop @ (a , aProp) = mkProperties p1 p2 p3
    where
      p1 = a , aProp a
      p2 = Aprop

      forward : ((λ _ → tt) ∘ (λ _ → a)) ∼ id
      forward tt = refl
      p3 = (λ _ → tt) , qinv-to-isequiv (mkQinv (λ _ → a) forward (aProp a))

  iii : {A : Set} → A ≃ 𝟙 → properties A
  iii Aeqv @ (f , mkIsEquiv g g* h h*) = mkProperties p1 p2 p3
    where
      alltt : (a b : 𝟙) → a ≡ b
      alltt tt tt = refl

      p1 = h tt , λ x → ap h (alltt tt (f x)) ∙ h* x
      p2 = h tt , λ x y → sym (h* x) ∙ ap h (alltt (f x) (f y)) ∙ h* y
      p3 = Aeqv

Lemma 3.11.6

lemma3∙11∙6 : {A : Set} {P : A → Set} → ((a : A) → isContr (P a)) → isContr ((x : A) → P x)
lemma3∙11∙6 {A} {P} allContr =
  let
    Pa-isProp : isProp ((x : A) → P x)
    Pa-isProp = example3∙6∙2 λ x → Σ.snd (lemma3∙11∙3.properties.ii (lemma3∙11∙3.i (allContr x)))

    center : (x : A) → P x
    center x = Σ.fst (allContr x)
  in center , λ x → Pa-isProp center x

Retraction

record retraction {A B : Set l} (r : A → B) : Set l where
  field
    s : B → A
    ε : (y : B) → (r (s y) ≡ y)

_isRetractOf_ : (A B : Set l) → Set l
B isRetractOf A = Σ (A → B) retraction

Lemma 3.11.7

-- lemma3∙11∙7 : {A B : Set l} → B isRetractOf A → isContr A → isContr B
-- lemma3∙11∙7 {A = A} {B = B} BretractA Acontr =
--   let
--     open Σ
--     open retraction

--     r = BretractA .fst
--     s = BretractA .snd .s
--     a₀ = Σ.fst Acontr
--     b₀ = r a₀

--     ε : (y : B) → r (s y) ≡ y
--     ε = BretractA .snd .ε

--     sContr : (b : B) → s b ≡ a₀
--     sContr b = {! Acontr .snd (s b)  !}
--   in b₀ , λ b → {!   !} ∙ (ε b)

Lemma 3.11.8

lemma3∙11∙8 : (A : Set) → (a : A) → isContr (Σ A (λ x → a ≡ x))
lemma3∙11∙8 A a = center , proof
  where
    -- choose center point (a, reflₐ)
    center = (a , refl)

    proof : ((x , p) : Σ A (λ x → a ≡ x)) → center ≡ (x , p)
    proof (x , p) = Σ-≡ (p , lemma2∙11∙2.i p refl ∙ sym (lemma2∙1∙4.i2 p))

-- Same thing but flipped :facepalm:
lemma3∙11∙8' : (A : Set) → (a : A) → isContr (Σ A (λ x → x ≡ a))
lemma3∙11∙8' A a = center , proof
  where
    -- choose center point (a, reflₐ)
    center = (a , refl)

    proof : ((x , p) : Σ A (λ x → x ≡ a)) → center ≡ (x , p)
    proof (x , p) = Σ-≡ (sym p , lemma2∙11∙2.ii (sym p) refl ∙ sym (lemma2∙1∙4.i1 (sym (sym p))) ∙ lemma2∙1∙4.iii p)

Lemma 3.11.9

module lemma3∙11∙9 where
  i : ∀ {l1 l2} {A : Set l1} {P : A → Set l2} → ((x : A) → isContr (P x)) → Σ A P ≃ A
  i {l1} {l2} {A} {P} eachContr = Σ.fst , qinv-to-isequiv (mkQinv g (λ _ → refl) backward)
    where
      g : A → Σ A P
      g a = a , Σ.fst (eachContr a)

      backward : (g ∘ Σ.fst) ∼ id
      backward (x , p) = 
        let 
          xContr = eachContr x
          y : Σ.fst xContr ≡ p
          y = Σ.snd xContr p
        in Σ-≡ (refl , y)

  ii : ∀ {l1 l2} {A : Set l1} {P : A → Set l2} → ((a , _) : isContr A) → Σ A P ≃ P a
  ii {l1} {l2} {A} {P} (a , aContr) = f , qinv-to-isequiv (mkQinv g forward backward)
    where
      f : Σ A P → P a
      f (x , y) = transport P (sym (aContr x)) y

      g : P a → Σ A P
      g p = a , p

      forward : (p : P a) → transport P (sym (aContr a)) p ≡ p
      forward p = admit
        where
          postulate
            -- TODO
            admit : transport P (sym (aContr a)) p ≡ p

      backward : (g ∘ f) ∼ id
      backward (x , p) = 
        let
          lol : a ≡ x
          lol = aContr x
        in Σ-≡ (lol , y lol)
        where
          y : (q : a ≡ x) → transport P q (transport P (sym q) p) ≡ p
          y refl = refl

Lemma 3.11.10

module lemma3∙11∙10 where
  i : {A : Set} → ((x y : A) → isContr (x ≡ y)) → isProp A
  i f x y = Σ.fst (f x y)

  ii : {A : Set} → isProp A → ((x y : A) → isContr (x ≡ y))
  ii f x y = f x y , admit
    where
      postulate
        admit : (z : x ≡ y) → f x y ≡ z
Imports 
{-# OPTIONS --rewriting #-}

module HottBook.Chapter4 where

open import HottBook.Chapter1
open import HottBook.Chapter1Util
open import HottBook.Chapter2
open import HottBook.Chapter2Exercises
open import HottBook.Chapter3
open import HottBook.CoreUtil

private
  variable
    l : Level

Chapter 4 Equivalences

record satisfies-equivalence-properties {A B : Set} {f : A → B} (isequiv : (A → B) → Set) : Set where
  field
    qinv→isequiv : qinv f → isequiv f
    isequiv→qinv : isequiv f → qinv f
    isequiv-isProp : isProp (isequiv f)

4.1 Quasi-inverses

Lemma 4.1.1

lemma4∙1∙1 : {A B : Set} → (f : A → B) → qinv f → qinv f ≃ ((x : A) → x ≡ x)
lemma4∙1∙1 {A} {B} f e @ (mkQinv g _ _) = goal
  where
    open Σ
    open lemma2∙4∙12
    open axiom2∙9∙3 using (funext)
    open axiom2∙10∙3 using (ua)
    open ≡-Reasoning

    fe : A ≃ B
    fe = f , qinv-to-isequiv e

    p : A ≡ B
    p = ua fe
    
    goal : qinv f ≃ ((x : A) → x ≡ x)

    goal2 : ∀ {A B} → (p : A ≡ B) → qinv (idtoeqv p .fst) ≃ ((x : A) → x ≡ x)
    goal = trans-equiv (idtoeqv (ap qinv (ap Σ.fst (sym (axiom2∙10∙3.propositional-computation fe))))) (goal2 p)

    goal3 : ∀ {A} → qinv id ≃ ((x : A) → x ≡ x)
    goal2 refl = goal3

    convert : ∀ {A B} → (f : A → B) → qinv f ≡ Σ (B → A) (λ g → ((f ∘ g) ∼ id) × ((g ∘ f) ∼ id))
    convert f = ua ((λ (mkQinv g α β) → g , (α , β)) ,
      qinv-to-isequiv (mkQinv (λ (g , α , β) → mkQinv g α β) (λ _ → refl) λ _ → refl))

    goal4 : ∀ {A} → qinv id ≡ Σ (Σ (A → A) (λ g → g ≡ id)) (λ h → fst h ≡ id)

    goal4 {A} = begin
      qinv id ≡⟨ convert id ⟩
      Σ (A → A) (λ g → (g ∼ id) × (g ∼ id)) ≡⟨ ap (Σ (A → A)) (funext lemma) ⟩
      Σ (A → A) (λ g → (g ≡ id) × (g ≡ id)) ≡⟨ ua exercise2∙10 ⟩
      Σ (Σ (A → A) (λ g → g ≡ id)) (λ h → fst h ≡ id) ∎
      where
        lemma : (id' : A → A) → ((id' ∼ id) × (id' ∼ id)) ≡ ((id' ≡ id) × (id' ≡ id))
        lemma id' = ua (ff , qinv-to-isequiv (mkQinv gg forward backward))
          where
            open axiom2∙9∙3

            ff : (id' ∼ id × id' ∼ id) → (id' ≡ id × id' ≡ id)
            ff (l , r) = funext l , funext r

            gg : (id' ≡ id × id' ≡ id) → (id' ∼ id × id' ∼ id)
            gg (l , r) = happly l , happly r

            forward : (ff ∘ gg) ∼ id
            forward (l , r) = Σ-≡' (propositional-uniqueness l , propositional-uniqueness r)

            backward : (gg ∘ ff) ∼ id
            backward (l , r) = Σ-≡' (propositional-computation l , propositional-computation r)
      
    goal5 : ∀ {A} → isContr (Σ (A → A) (λ g → g ≡ id))
    goal5 {A} = lemma3∙11∙8' (A → A) id

    goal6 : ∀ {A} → Σ (Σ (A → A) (λ g → g ≡ id)) (λ h → fst h ≡ id) ≃ (id ≡ id)
    goal6 = lemma3∙11∙9.ii goal5

    goal7 : ∀ {A} → (id ≡ id) ≃ ((x : A) → x ≡ x)
    goal7 = axiom2∙9∙3.happly-equiv

    goal3 = trans-equiv (idtoeqv goal4) (trans-equiv goal6 goal7)

Lemma 4.1.2

lemma4∙1∙2 : {A : Set} {a : A} (q : a ≡ a)
  → isSet (a ≡ a)
  → (g : (x : A) → ∥ a ≡ x ∥)
  → ((p : a ≡ a) → p ∙ q ≡ q ∙ p)
  → Σ ((x : A) → x ≡ x) (λ f → f a ≡ q)
lemma4∙1∙2 {A} {a} q prop1 g prop3 = (λ x → {!   !}) , {!   !}
  where
    allsets : (x y : A) → isSet (x ≡ y)
    allsets x y p q r s = {!  trunc-witness ? ? !}

    ctx = let 
      f = rec-trunc A {!   !} {! g  !}
      in {!   !}

    B : (x : A) → Set
    B x = Σ (x ≡ x) (λ r → (s : a ≡ x) → r ≡ (sym s) ∙ q ∙ s)

    BisProp : (a : A) → isProp (B a)
    BisProp a x y = {!   !}

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 : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
-- theorem4∙1∙3 {l} = goal
  -- where
  --   goal : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))

  --   goal2 : ∀ {l} → Σ (Set l) (λ X → isProp ((x : X) → x ≡ x) → ⊥)
  --   goal {l} = Σ.fst (goal2 {l}) , {!   !} , {!   !} , {!   !}

  --   X : ∀ {l} → Set (lsuc l)
  --   X {l} = Σ (Set l) (λ A → ∥ Lift 𝟚 ≡ A ∥)

  --   goal2 {l} = X {lsuc l} , ?

4.2 Half adjoint equivalences

Definition 4.2.1

record ishae {A B : Set} (f : A → B) : Set where
  constructor mkIshae
  field
    g : B → A
    η : (g ∘ f) ∼ id
    ε : (f ∘ g) ∼ id
    τ : (x : A) → ap f (η x) ≡ ε (f x)

Lemma 4.2.2

lemma4∙2∙2 : ∀ {A B} 
  → (f : A → B) → (g : B → A)
  → (η : (g ∘ f) ∼ id)
  → (ε : (f ∘ g) ∼ id)
  → ((x : A) → ap f (η x) ≡ ε (f x)) ≃ ((y : B) → ap g (ε y) ≡ η (g y))
lemma4∙2∙2 f g η ε = {!   !}

ishae→qinv : {A B : Set} (f : A → B) → ishae f → qinv f
ishae→qinv f (mkIshae g η ε _) = mkQinv g ε η

Theorem 4.2.3

theorem4∙2∙3 : {A B : Set} (f : A → B) → qinv f → ishae f
theorem4∙2∙3 {A} {B} f (mkQinv g ε η) = mkIshae g' η' ε' τ
  where
    g' : B → A
    g' = g

    η' : (g' ∘ f) ∼ id
    η' = η

    ε' : (f ∘ g') ∼ id
    ε' x = {!   !}

    τ : (x : A) → ap f (η' x) ≡ ε' (f x)
    τ x = {!   !}

Definition 4.2.4

fib : ∀ {A B} → (f : A → B) → (y : B) → Set
fib {A = A} f y = Σ A (λ x → f x ≡ y)

Lemma 4.2.5

lemma4∙2∙5 : {A B : Set} 
  → (f : A → B) 
  → (y : B)
  → ((x , p) (x' , p') : fib f y)
  → ((x , p) ≡ (x' , p')) ≃ Σ (x ≡ x') (λ γ → ap f γ ∙ p' ≡ p)
lemma4∙2∙5 f y (x , p) (x' , p') = {!   !} , {!   !}
  where
    ff : (x , p) ≡ (x' , p') → Σ (x ≡ x') (λ γ → ap f γ ∙ p' ≡ p)
    ff q = ap fst q , {!   !} -- (_ : f x ≡ f x') ∙ p' ≡ p

Definition 4.2.7

module definition4∙2∙7 where
  linv : ∀ {A B} (f : A → B) → Set
  linv {A} {B} f = Σ (B → A) (λ g → (g ∘ f) ∼ id)

  rinv : ∀ {A B} (f : A → B) → Set
  rinv {A} {B} f = Σ (B → A) (λ g → (f ∘ g) ∼ id)
open definition4∙2∙7

Lemma 4.2.9

lemma4∙2∙9 : ∀ {A B} (f : A → B) → qinv f → isContr (linv f) × isContr (rinv f)
lemma4∙2∙9 f q = ({!   !} , {!   !}) , ({!   !} , {!   !})

Definition 4.2.10

module definition4∙2∙10 where
  open definition4∙2∙7

  -- lcoh : ∀ {A} {B} → (f : A → B) → linv f → rinv f → Set
  -- lcoh f (g , η) (g , ε) = ?

Theorem 4.2.13

-- theorem4∙2∙13 : {A B : Set} (f : A → B) → isProp (ishae f)

4.3 Bi-invertible maps

Definition 4.3.1

biinv : {A B : Set} (f : A → B) → Set
biinv f = linv f × rinv f

Theorem 4.3.2

theorem4∙3∙2 : ∀ {A B} → (f : A → B) → isProp (biinv f)
theorem4∙3∙2 f = {!   !}

{-# OPTIONS --rewriting #-}

module HottBook.Chapter5 where

open import Agda.Primitive
open import HottBook.Chapter1

5.1 Introduction to inductive types

Theorem 5.1.1

-- theorem5∙1∙1 : {E : ℕ → Set}
--   → (f g : (x : ℕ) → E x)
--   → (z : f 0 ≡ g 0)
--   → (s : 
--   → f ≡ g

Definition 5.4.1

ℕAlg : {l : Level} → Set (lsuc l)
ℕAlg {l} = Σ (Set l) (λ C → C × (C → C))

Definition 5.4.2

ℕHom : {l : Level} → ℕAlg {l} → ℕAlg {l} → Set l
ℕHom alg1@(C , (cz , cs)) alg2@(D , (dz , ds)) = 
  Σ (C → D) λ h → (h cz ≡ dz) × ((c : C) → h (cs c) ≡ ds (h c))
Imports 
{-# OPTIONS --rewriting #-}

module HottBook.Chapter6 where

open import HottBook.Chapter1
open import HottBook.Chapter2
open import HottBook.Chapter3
open import HottBook.Chapter6Circle
open import HottBook.CoreUtil

private
  variable
    l l2 : Level

Chapter 6 Higher Inductive Types

Using the approach from here: https://github.com/HoTT/HoTT-Agda/blob/master/old/Spaces/Circle.agda

6.2 Induction principles and dependent paths

dep-path : {l l2 : Level} {A : Set l} {x y : A} → (P : A → Set l2) → (p : x ≡ y) → (u : P x) → (v : P y) → Set l2
dep-path P p u v = transport P p u ≡ v

syntax dep-path P p u v = u ≡[ P , p ] v

Lemma 6.2.5

lemma6∙2∙5 : {A : Set} → {a : A} → {p : a ≡ a} → S¹ → A
lemma6∙2∙5 {A} {a} {p} = rec-S¹ a p
  where
    path : a ≡[ (λ _ → A) , loop ] a
    path = transportconst A loop a

Lemma 6.2.8

lemma6∙2∙8 : {A : Set} → {f g : S¹ → A}
  → (p : f S¹.base ≡ g S¹.base)
  → (q : ap f loop ≡[ (λ y → y ≡ y) , p ] (ap g loop))
  → (x : S¹) → f x ≡ g x
lemma6∙2∙8 {f = f} {g = g} p q = rec-S¹ p goal
  where
    goal : p ≡[ (λ y → f y ≡ g y) , loop ] p
    goal2 : dep-path (λ y → f y ≡ g y) loop p p
    goal = goal2
    goal3 : transport (λ y → f y ≡ g y) loop p ≡ p
    goal2 = goal3
    postulate
      admit : transport (λ y → f y ≡ g y) loop p ≡ p
    goal3 = admit
    -- goal4 : p ∙ loop ≡ loop ∙ p
    -- goal3 = theorem2∙11∙5
    -- goal4 : sym (ap f loop) ∙ p ∙ (ap g loop) ≡ p
    -- goal3 = theorem2∙11∙3 loop p ∙ goal4
    -- goal5 :

6.3 The interval

module Interval where
  postulate
    I : Set
    0I 1I : I
    seg : 0I ≡ 1I

    rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B
    rec-Interval-0I : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 0I ≡ b₀
    rec-Interval-1I : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 1I ≡ b₁
    {-# REWRITE rec-Interval-0I #-}
    {-# REWRITE rec-Interval-1I #-}

    rec-Interval-3 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → apd (rec-Interval b₀ b₁ s) seg ≡ s
    {-# REWRITE rec-Interval-3 #-}

    rec-Interval-d : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → (x : I) → B x
    rec-Interval-d-0I : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → rec-Interval-d {B = B} b₀ b₁ s 0I ≡ b₀
    rec-Interval-d-1I : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → rec-Interval-d {B = B} b₀ b₁ s 1I ≡ b₁
    {-# REWRITE rec-Interval-d-0I #-}
    {-# REWRITE rec-Interval-d-1I #-}

    rec-Interval-d-3 : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → apd (rec-Interval-d {B} b₀ b₁ s) seg ≡ s
    {-# REWRITE rec-Interval-d-3 #-}
open Interval public

Lemma 6.3.1

lemma6∙3∙1 : isContr I
lemma6∙3∙1 = 1I , f
  where
    goal : (sym seg) ≡[ (λ z → 1I ≡ z) , seg ] refl

    f : (x : I) → 1I ≡ x
    f = rec-Interval-d (sym seg) refl goal

    goal2 : transport (λ z → 1I ≡ z) seg (sym seg) ≡ refl
    goal = goal2

    goal3 : (sym seg) ∙ seg ≡ refl
    goal2 = lemma2∙11∙2.i seg (sym seg) ∙ goal3

    goal3 = lemma2∙1∙4.ii1 seg

Lemma 6.3.2

lemma6∙3∙2 : {A B : Set} {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
lemma6∙3∙2 {A = A} {B = B} {f = f} {g = g} p = apd q seg
  where
    p' : (x : A) → I → B
    p' x = rec-Interval (f x) (g x) (p x)

    q : I → (A → B)
    q i x = p' x i

6.4 Circles and sphere

module S¹ where
  postulate
    S¹ : Set
    base : S¹
    loop : base ≡ base

    rec-S¹ : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
    rec-S¹-base : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → rec-S¹ {P = P} b l base ≡ b
    {-# REWRITE rec-S¹-base #-}
    rec-S¹-loop : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (rec-S¹ b l) loop ≡ l

    -- TODO: Uncommenting this leads to a bug in the definition of z2 in lemma 6.4.1
    -- {-# REWRITE rec-S¹-loop #-}
open S¹ hiding (base) public

Lemma 6.4.1

lemma6∙4∙1 : loop ≢ refl
lemma6∙4∙1 loop≡refl = goal3
  where
    open S¹

    f : ∀ {l} {A : Set l} {x : A} {p : x ≡ x} → S¹ → A
    f {A = A} {x = x} {p = p} = rec-S¹ {P = λ _ → A} x p

    goal2 : ∀ {l} {A : Set l} → isSet A
    goal2 {l = l} {A = A} x .x p refl = z1 ∙ z2 ∙ z3
      where
        f' : S¹ → A
        f' = f {l = l} {A = A} {x = x} {p = p}

        z1 : p ≡ apd f' loop
        z1 = sym (rec-S¹-loop x p)

        z2 : apd f' loop ≡ apd {x = base} f' refl
        z2 = ap {A = base ≡ base} (apd f') loop≡refl

        z3 : apd {x = base} f' refl ≡ refl
        z3 = refl

    goal3 : ⊥
    goal3 = example3∙1∙9 (goal2 {A = Set})

Lemma 6.4.2

lemma6∙4∙2 : Σ ((x : S¹) → x ≡ x) (λ y → y ≢ (λ x → refl))
lemma6∙4∙2 = f , g
  where
    open axiom2∙9∙3

    f = rec-S¹ loop goal
      where
        goal : loop ≡[ (λ x → x ≡ x) , loop ] loop
        goal2 : sym loop ∙ loop ∙ loop ≡ loop
        goal = lemma2∙11∙2.iii {a = S¹.base} loop loop ∙ goal2
        goal3 : sym loop ∙ loop ≡ refl
        goal4 : refl ∙ loop ≡ loop
        goal5 : sym loop ∙ loop ∙ loop ≡ (sym loop ∙ loop) ∙ loop
        goal2 = goal5 ∙ ap (λ c → c ∙ loop) goal3 ∙ goal4
        goal3 = lemma2∙1∙4.ii1 loop
        goal4 = sym (lemma2∙1∙4.i2 loop)
        goal5 = lemma2∙1∙4.iv (sym loop) loop loop

    g : f ≡ (λ x → refl) → ⊥
    g p = lemma6∙4∙1 goal
      where
        goal : loop ≡ refl
        goal = ap (λ s → s S¹.base) p

Corollary 6.4.3

-- corollary6∙4∙3 : (l : Level) → ¬ (is-1-type (Set l))
-- corollary6∙4∙3 l p = {!   !}
--   where
--     open lemma2∙4∙12

--     Circle : Set l
--     Circle = Lift S¹

--     self : Set (lsuc l)
--     self = Circle ≡ Circle

--     self-equiv : Set l
--     self-equiv = Circle ≃ Circle

--     goal1 : ¬ isSet self-equiv

--     goal2 : ¬ isProp (id-equiv Circle ≡ id-equiv Circle)
--     goal1 p = goal2 λ p' q' → p (id-equiv Circle) (id-equiv Circle) p' q'

--     postulate
--       equivalence-isProp : isProp self-equiv

--     goal3 : ¬ isProp (id {A = Circle} ≡ id)
--     goal4 : (id {A = Circle} ≡ id) ≡ (id-equiv Circle ≡ id-equiv Circle)

--     A : Set l
--     goal : ⊥

Lemma 6.4.4

lemma6∙4∙4 : {A B : Set} 
  → (f : A → B)
  → {x y : A} {p q : x ≡ y}
  → (r : p ≡ q)
  → ap f p ≡ ap f q
lemma6∙4∙4 f refl = refl

ap² = lemma6∙4∙4

Lemma 6.4.5

lemma6∙4∙5 : {A : Set l}
  → (P : A → Set l2) 
  → {x y : A} {p q : x ≡ y}
  → (r : p ≡ q)
  → (u : P x)
  → transport P p u ≡ transport P q u
lemma6∙4∙5 P refl u = refl

transport² = lemma6∙4∙5

Lemma 6.4.6

dep-2-path : {l l2 : Level} {A : Set l} {x y : A}
  → (P : A → Set l2)
  → {p q : x ≡ y}
  → (r : p ≡ q)
  → {u : P x} → {v : P y}
  → (h : u ≡[ P , p ] v)
  → (k : u ≡[ P , q ] v)
  → Set l2
dep-2-path P r {u = u} h k = h ≡ transport² P r u ∙ k

syntax dep-2-path P r h k = h ≡²[ P , r ] k

lemma6∙4∙6 : {A : Set} {P : A → Set} {x y : A} {p q : x ≡ y}
  → (f : (x : A) → P x)
  → (r : p ≡ q)
  → apd f p ≡²[ P , r ] apd f q
lemma6∙4∙6 {p = p} f refl = lemma2∙1∙4.i2 (apd f p)

Sphere

module S² where
  postulate
    S² : Set
    base : S²
    surf : refl {x = base} ≡ refl

  -- TODO: Define recursion principle
open S² hiding (base)

6.5 Suspensions

module Suspension where
  private
    variable
      A : Set l

  postulate
    Susp : Set → Set
    N : Susp A
    S : Susp A
    merid : A → (N {A} ≡ S {A})

    rec-Susp : {B : Set l} → (n s : B) → (m : A → n ≡ s) → Susp A → B
    rec-Susp-N : {B : Set l} → (n s : B) → (m : A → n ≡ s) → rec-Susp n s m N ≡ n
    rec-Susp-S : {B : Set l} → (n s : B) → (m : A → n ≡ s) → rec-Susp n s m S ≡ s
    {-# REWRITE rec-Susp-N #-}
    {-# REWRITE rec-Susp-S #-}

    rec-Susp-merid : {B : Set l} (n s : B) → (m : A → n ≡ s) → (a : A) → ap (rec-Susp n s m) (merid a) ≡ m a
open Suspension public

Lemma 6.5.1

-- lemma6∙5∙1 : Susp 𝟚 ≃ S¹
-- lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward)
--   where
--     open S¹

--     m : 𝟚 → base ≡ base
--     m true = refl
--     m false = loop

--     f : Susp 𝟚 → S¹
--     f s = rec-Susp base base m s

--     g : S¹ → Susp 𝟚
--     g s = rec-S¹ N (merid false ∙ sym (merid true)) s
    
--     forward : (f ∘ g) ∼ id
--     forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl {!  refl !} x
    
--     backward : (g ∘ f) ∼ id
--     backward x = {!   !}
Imports 
{-# OPTIONS --rewriting #-}

module HottBook.Chapter7 where

open import HottBook.Chapter1
open import HottBook.Chapter2
open import HottBook.Chapter3
open import HottBook.CoreUtil

private
  variable
    l l2 : Level

7.1 Definition of -types

Definition 7.1.1

data ℕ' : Set where
  negtwo : ℕ'
  suc : ℕ' → ℕ'

is_type : (n : ℕ') → Set → Set
is negtwo type X = isContr X
is suc n type X = (x y : X) → is n type (x ≡ y)

Theorem 7.1.4

theorem7∙1∙4 : {X Y : Set} 
  → (f : X → Y) → (n : ℕ') → is n type X → is n type Y
theorem7∙1∙4 {X} {Y} f negtwo q = f (fst q) , λ y → {!   !}
theorem7∙1∙4 {X} {Y} f (suc n) q = {!   !}

module HottBook.Chapter8 where

open import Agda.Primitive
open import HottBook.Chapter1
open import HottBook.Chapter2
open import HottBook.Chapter6

Definition 8.0.1

-- TODO: Finish
postulate
  π : (n : ℕ) → (A : Set) → (a : A) → Set

8.1 π₁(S¹)

Definition 8.1.1

data ℤ : Set where

-- code : {l : Level} → S¹ → Set (lsuc l)
-- code {l} = S¹-elim (λ _ → Set l) ℤ (ua suc)

8.7 The van Kampen theorem

8.7.1 Naive van Kampen

{-# OPTIONS --no-load-primitives --cubical #-}
module CubicalHott.Chapter1 where

open import CubicalHott.Primitives public

1.4 Dependent function types (Π-types)

id : ∀ {l} {A : Type l} → A → A
id x = x

1.5 Product types

data 𝟙 : Type where
  tt : 𝟙

1.7 Coproduct types

record Σ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') : Type (ℓ ⊔ ℓ') where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

{-# BUILTIN SIGMA Σ #-}
infixr 4 _,_

syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

_×_ : {l : Level} (A B : Type l) → Type l
_×_ A B = Σ A (λ _ → B)

Unit type:

record ⊤ : Type where
  instance constructor tt
{-# BUILTIN UNIT ⊤ #-}

data ⊥ : Type where

1.8 The type of booleans

data 𝟚 : Type where
  true : 𝟚
  false : 𝟚

neg : 𝟚 → 𝟚
neg true = false
neg false = true

1.11 Propositions as types

infix 3 ¬_
¬_ : ∀ {l} (A : Type l) → Type l
¬_ A = A → ⊥

1.12 Identity types

private
  to-path : ∀ {l} {A : Type l} → (f : I → A) → Path A (f i0) (f i1)
  to-path f i = f i

refl : {l : Level} {A : Type l} {x : A} → x ≡ x
refl {x = x} = to-path (λ i → x)

1.12.3 Disequality

_≢_ : {A : Type} (x y : A) → Type
_≢_ x y = (p : x ≡ y) → ⊥

Exercises

Exercise 1.1

Given functions f : A → B and g : B → C, define their composite g ◦ f : A → C. Show that we have h ◦ (g ◦ f) ≡ (h ◦ g) ◦ f.

composite : {A B C : Type}
  → (f : A → B)
  → (g : B → C)
  → A → C
composite f g x = g (f x)

-- https://agda.github.io/agda-stdlib/master/Function.Base.html
infixr 9 _∘_
_∘_ : {l1 l2 l3 : Level} {A : Type l1} {B : Type l2} {C : Type l3}
  → (g : B → C)
  → (f : A → B)
  → A → C
_∘_ g f x = g (f x)

composite-assoc : {A B C D : Type}
  → (f : A → B)
  → (g : B → C)
  → (h : C → D)
  → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
composite-assoc f g h = refl

{-# OPTIONS --no-load-primitives --cubical #-}
module CubicalHott.Chapter2 where

open import CubicalHott.Chapter1
open import CubicalHott.Chapter2Lemma221 public

Lemma 2.1.1

sym : {l : Level} {A : Type l} {x y : A} → (x ≡ y) → y ≡ x
sym {l} {A} {x} {y} p i = p (~ i)

Lemma 2.1.2

TODO: Read more about composition here

private
  -- https://1lab.dev/1Lab.Reflection.Regularity.html#1191
  double-comp
    : ∀ {ℓ} {A : Type ℓ} {w z : A} (x y : A)
    → w ≡ x → x ≡ y → y ≡ z
    → w ≡ z
  double-comp x y p q r i = primHComp
    (λ { j (i = i0) → p (~ j) ; j (i = i1) → r j }) (q i)

trans : ∀ {l} {A : Type l} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
trans {l} {A} {x} {y} {z} p q = double-comp x y refl p q

infixr 30 _∙_
_∙_ = trans

Equational Reasoning

module ≡-Reasoning where
  infix 1 begin_
  begin_ : {l : Level} {A : Type l} {x y : A} → (x ≡ y) → (x ≡ y)
  begin x = x

  _≡⟨⟩_ : {l : Level} {A : Type l} (x {y} : A) → x ≡ y → x ≡ y
  _ ≡⟨⟩ x≡y = x≡y

  infixr 2 _≡⟨⟩_ step-≡
  step-≡ : {l : Level} {A : Type l} (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
  step-≡ _ y≡z x≡y = trans x≡y y≡z
  syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z

  infix 3 _∎
  _∎ : {l : Level} {A : Type l} (x : A) → (x ≡ x)
  _ ∎ = refl

Lemma 2.1.4

module lemma2∙1∙4 {l : Level} {A : Type l} where
  iii : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
  iii {x} {y} p i j = p j

Lemma 2.2.1

ap : {l1 l2 : Level} {A : Type l1} {B : Type l2} {x y : A}
  → (f : A → B)
  → (p : x ≡ y)
  → f x ≡ f y
ap {l1} {l2} {A} {B} {x} {y} f p i = f (p i)

Lemma 2.3.1 (Transport)

-- transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
--   → (P : A → Set l₂)
--   → (p : x ≡ y)
--   → P x → P y
-- transport {l₁} {l₂} {A} {x} {y} P refl = id

transport : ∀ {l1 l2} {A : Type l1} {x y : A}
  → (P : A → Type l2) → (p : x ≡ y) → P x → P y
transport P p = transp (λ i → P (p i)) i0

Definition 2.4.1 (Homotopy)

infixl 18 _∼_
_∼_ : {l₁ l₂ : Level} {A : Type l₁} {P : A → Type l₂}
  → (f g : (x : A) → P x)
  → Type (l₁ ⊔ l₂)
_∼_ {l₁} {l₂} {A} {P} f g = (x : A) → f x ≡ g x

Definition 2.4.6

record qinv {l1 l2 : Level} {A : Type l1} {B : Type l2} (f : A → B) : Type (l1 ⊔ l2) where
  constructor mkQinv
  field
    g : B → A
    α : (f ∘ g) ∼ id
    β : (g ∘ f) ∼ id

Definition 2.4.10

record isequiv {l1 l2 : Level} {A : Type l1} {B : Type l2} (f : A → B) : Type (l1 ⊔ l2) where
  eta-equality
  constructor mkIsEquiv
  field
    g : B → A
    g-id : (f ∘ g) ∼ id
    h : B → A
    h-id : (h ∘ f) ∼ id

qinv-to-isequiv : {l1 l2 : Level} {A : Type l1} {B : Type l2}
  → {f : A → B}
  → qinv f
  → isequiv f
qinv-to-isequiv (mkQinv g α β) = mkIsEquiv g α g β

Still kinda shaky on this one, TODO study it later:

isequiv-to-qinv : {l : Level} {A B : Type l}
  → {f : A → B}
  → isequiv f
  → qinv f
isequiv-to-qinv {l} {A} {B} {f} (mkIsEquiv g g-id h h-id) =
  let
    γ : g ∼ h
    γ x = (sym (h-id (g x))) ∙ ap h (g-id x)

    β : (g ∘ f) ∼ id
    β x = γ (f x) ∙ h-id x 
  in
  mkQinv g g-id β

Definition 2.4.11

_≃_ : {l1 l2 : Level} → (A : Type l1) (B : Type l2) → Type (l1 ⊔ l2)
A ≃ B = Σ (A → B) isequiv

Lemma 2.4.12

module lemma2∙4∙12 where
  id-equiv : {l : Level} → (A : Type l) → A ≃ A
  id-equiv A = id , qinv-to-isequiv (mkQinv id (λ _ → refl) (λ _ → refl))

  sym-equiv : {A B : Type} → (f : A ≃ B) → B ≃ A
  sym-equiv {A} {B} (f , eqv) =
    let (mkQinv g α β) = isequiv-to-qinv eqv
    in g , qinv-to-isequiv (mkQinv f β α)

  -- trans-equiv : {A B C : Type} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
  -- trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) =
  --   let
  --     (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
  --     (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv

  --     open ≡-Reasoning

  --     forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id
  --     forward c =
  --       begin
  --         ((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩
  --         (g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩
  --         (g ∘ id ∘ g-inv) c ≡⟨⟩
  --         (g ∘ g-inv) c ≡⟨ g-inv-left c ⟩
  --         id c ∎

  --     backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id
  --     backward a =
  --       begin
  --         ((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩
  --         (f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩
  --         (f-inv ∘ (id ∘ f)) a ≡⟨⟩
  --         (f-inv ∘ f) a ≡⟨ f-inv-right a ⟩
  --         id a ∎
      
  --   in {!   !}
    -- in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)

Lemma 2.9.2

happly : {A B : Type}
  → {f g : A → B}
  → (p : f ≡ g)
  → (x : A)
  → f x ≡ g x
happly {A} {B} {f} {g} p x = ap (λ h → h x) p

happlyd : {A : Type} {B : A → Type}
  → {f g : (a : A) → B a}
  → (p : f ≡ g)
  → (x : A)
  → f x ≡ g x
happlyd {A} {B} {f} {g} p x = ap (λ h → h x) p

Theorem 2.9.3 (Function extensionality)

funext : {l : Level} {A B : Type l}
  → {f g : A → B}
  → ((x : A) → f x ≡ g x)
  → f ≡ g
funext h i x = h x i

2.10 Universes and the univalence axiom

Lemma 2.10.1

-- idtoeqv : {l : Level} {A B : Type l}
--   → (A ≡ B)
--   → (A ≃ B)
-- idtoeqv {l} {A} {B} p = transport {!   !} {!   !} {! p  !} , qinv-to-isequiv (mkQinv {!   !} {!   !} {!   !})

Axiom 2.10.3 (Univalence)

module axiom2∙10∙3 where
  -- Glue : ∀ {l l2} (A : Type l)
  --    → {φ : I}
  --    → (Te : Partial φ (Σ (Type l2) (λ T → T ≃ A)))
  --    → Type l2

  postulate
    -- TODO: Provide the definition for this after reading CCHM
    ua : {l : Level} {A B : Type l} → (A ≃ B) → (A ≡ B)

  --   forward : {l : Level} {A B : Type l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
  --   -- forward eqv = {!   !}

  --   backward : {l : Level} {A B : Type l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
  --   -- backward p = {!   !}

  -- ua-eqv : {l : Level} {A : Type l} {B : Type l} → (A ≃ B) ≃ (A ≡ B)
  -- ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)

open axiom2∙10∙3

Theorem 2.11.2

-- module lemma2∙11∙2 where
--   open ≡-Reasoning

--   i : {l : Level} {A : Type l} {a x1 x2 : A}
--     → (p : x1 ≡ x2)
--     → (q : a ≡ x1)
--     → transport (λ y → a ≡ y) p q ≡ q ∙ p
--   i {l} {A} {a} {x1} {x2} p q j = {!   !}

--   ii : {l : Level} {A : Type l} {a x1 x2 : A}
--     → (p : x1 ≡ x2)
--     → (q : x1 ≡ a)
--     → transport (λ y → y ≡ a) p q ≡ sym p ∙ q
--   ii {l} {A} {a} {x1} {x2} p q = {!   !}

--   iii : {l : Level} {A : Type l} {a x1 x2 : A}
--     → (p : x1 ≡ x2)
--     → (q : x1 ≡ x1)
--     → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
--   iii {l} {A} {a} {x1} {x2} p q = {!   !}

Remark 2.12.6

module remark2∙12∙6 where
  true≢false : true ≢ false
  true≢false p = genBot tt
    where
      Bmap : 𝟚 → Type
      Bmap true = 𝟙
      Bmap false = ⊥

      genBot : 𝟙 → ⊥
      genBot = transport Bmap p

{-# OPTIONS --no-load-primitives --cubical #-}
module CubicalHott.Chapter3 where

open import CubicalHott.Chapter1
open import CubicalHott.Chapter2

Definition 3.1.1

isSet : {l : Level} (A : Type l) → Type l
isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q

Example 3.1.9

example3∙1∙9 : {l : Level} → ¬ (isSet (Type l))
example3∙1∙9 p =
  {!   !}
  where
    lol : (x : 𝟚) → neg (neg x) ≡ x
    lol true = refl
    lol false = refl

Definition 3.3.1

isProp : (P : Type) → Type
isProp P = (x y : P) → x ≡ y

3.7 Propositional truncation

module section3∙7 where
  data ∥_∥ (A : Type) : Type where
    ∣_∣ : (a : A) → ∥ A ∥
    witness : (x y : ∥ A ∥) → x ≡ y

  rec-∥_∥ : (A : Type) → {B : Type} → isProp B → (f : A → B)
    → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
  rec-∥ A ∥ {B} BisProp f = g , λ _ → refl
    where
      g : ∥ A ∥ → B
      g ∣ a ∣ = f a
      g (witness x y i) = BisProp (g x) (g y) i
open section3∙7

3.8 The axiom of choice

Equation 3.8.1 (axiom of choice AC)

postulate
  AC : {X : Type} {A : X → Type} {P : (x : X) → A x → Type}
    → ((x : X) → ∥ Σ (A x) (λ a → P x a) ∥)
    → ∥ Σ ((x : X) → A x) (λ g → (x : X) → P x (g x)) ∥

Lemma 3.8.5

3.9 The principle of unique choice

Lemma 3.9.1

lemma3∙9∙1 : {P : Type} → isProp P → P ≃ ∥ P ∥
lemma3∙9∙1 {P} Pprop = ∣_∣ , qinv-to-isequiv (mkQinv inv {!   !} {!   !})
  where
    inv : ∥ P ∥ → P
    inv ∣ a ∣ = a
    inv (witness p q i) =
      let what = ap ∥_∥ {!   !}
      in {!   !}

Chapter 4

Chapter 5

{-# OPTIONS --cubical #-}
module CubicalHott.Chapter6 where

open import CubicalHott.Chapter1
open import CubicalHott.Chapter2

6.4 Circles and spheres

data S¹ : Type where
  base : S¹
  loop : base ≡ base

Lemma 6.4.1

lemma6∙4∙1 : loop ≢ refl
lemma6∙4∙1 p =
  {!   !}
  where
    open ≡-Reasoning

    f : {A : Type} (x : A) → (p : x ≡ x) → S¹ → A
    f x p base = x
    f x p (loop i) = p i

    bad : {A : Type} (x : A) → (p : x ≡ x) → p ≡ refl
    bad x p = begin
      p ≡⟨ {!   !} ⟩
      p ≡⟨ {!   !} ⟩
      refl ∎

Chapter 7

Chapter 8

Chapter 9

{-# OPTIONS --no-load-primitives --cubical #-}
module CubicalHott.Chapter2Lemma221 where

open import CubicalHott.Chapter1

Lemma 2.2.1

ap : {l1 l2 : Level} {A : Type l1} {B : Type l2} {x y : A}
  → (f : A → B)
  → (p : x ≡ y)
  → f x ≡ f y
ap {l1} {l2} {A} {B} {x} {y} f p i = f (p i)

Definition 3.3.1

Lemma 3.3.3

{-# OPTIONS --cubical --no-load-primitives #-}
module VanDoornDissertation.Preliminaries where

open import CubicalHott.Chapter1
open import CubicalHott.Chapter2

2.2.1 Paths

2.2.3 More on paths

Pathovers

dependent-path : {A : Type} 
  → (P : A → Type) 
  → {x y : A} 
  → (p : x ≡ y)
  → (u : P x) → (v : P y) → Type
dependent-path P p u v = transport P p u ≡ v

syntax dependent-path P p u v = u ≡[ P , p ] v

-- https://git.mzhang.io/school/type-theory/issues/16
apd : ∀ {a b} {A : I → Type a} {B : (i : I) → A i → Type b}
    → (f : (i : I) → (a : A i) → B i a)
    → {x : A i0}
    → {y : A i1}
    → (p : PathP A x y)
    → PathP (λ i → B i (p i)) (f i0 x) (f i1 y)
apd f p i = f i (p i)

Squares

Square : {A : Type} {a00 a10 a01 a11 : A}
  → (p : a00 ≡ a01)
  → (q : a00 ≡ a10)
  → (s : a01 ≡ a11)
  → (r : a10 ≡ a11)
  → Type
Square p q s r = PathP (λ i → p i ≡ r i) q s

Squareovers and cubes



Paths in type formers




2.2.5 Pointed Types


Definition 2.2.6


data pointed (A : Type) : Type where
  mkPointed : (a₀ : A) → pointed A

1-is-pointed : pointed 𝟙
1-is-pointed = mkPointed tt

2-is-pointed : pointed 𝟚
2-is-pointed = mkPointed false

S⁰ = 2-is-pointed

_×_-is-pointed : {A B : Type} → pointed A → pointed B → pointed (A × B)
_×_-is-pointed {A} {B} (mkPointed a₀) (mkPointed b₀) = mkPointed (a₀ , b₀)



2.2.6 Higher inductive types


data Interval : Type where
  0I : Interval
  1I : Interval
  seg : 0I ≡ 1I

data Quotient (A : Type) (R : A → A → Type) : Type where
  x : A → Quotient A R
  glue : (a a' : A) → R a a' → x a ≡ x a'



module VanDoornDissertation.HIT where

open import HottBook.Chapter1



3 Higher Inductive Types


3.1 Propositional Truncation


postulate
  one-step-truncation : Set → Set
  f : {A : Set} → A → one-step-truncation A
  e : {A : Set} → (x y : A) → f x ≡ f y
-- data one-step-truncation (A : Set) : Set where
--   f : A → one-step-truncation A
--   e : (x y : A) → f x ≡ f y

weakly-constant : {A B : Set} → (g : A → B) → Set
weakly-constant {A} g = {x y : A} → g x ≡ g y

definition3∙1∙1 : {A : Set} → one-step-truncation A → ℕ → Set
definition3∙1∙1 {A} trunc zero = A
definition3∙1∙1 {A} trunc (suc n) = one-step-truncation (definition3∙1∙1 trunc n)

fs : {A : Set} → one-step-truncation A → (n : ℕ) → Set
fs trunc n = (definition3∙1∙1 trunc n) → (definition3∙1∙1 trunc (suc n))

-- lemma3∙1∙3 : {X : Set} → {x : X} → is