exercises5.agda

{-# OPTIONS --without-K --exact-split --safe #-}

module exercises5 where
{-
Please rename your file to exercises5-yourusername.agda
-}

open import Agda.Primitive public
{-
open means we can access all definitions in Agda.Primitive
public means any file that imports this one gets Agda.Primitive too.
-}

UU : (i : Level) → Set (lsuc i)
UU i = Set i

-- Preliminaries on dependent pair types; "\Sigma" for "Σ"
data Σ {i j : Level}(A : UU i)(B : A → UU j) : UU(i ⊔ j) where
    pair : (x : A) → B x → Σ A B

pr1 : {i j : Level}{A : UU i}{B : A → UU j} → Σ A B → A
pr1 (pair x x₁) = x

_×_ : {i j : Level}(A : UU i)(B : UU j) → UU (i ⊔ j)
A × B = Σ A (λ x → B)

-- The one-sided identity type is the type family in context of a type A and term a : A freely generated by refl_a : Id a a.
data Id {i : Level}{A : UU i}(a : A) : A → UU i where
    refl : Id a a

-- Definition 9.1.2: the type of homotopies "f ∼ g" for a pair of dependent functions; type "\sim" for "∼"
-- The underscore in (x : _) is a reference to the implicit argument A.
_∼_ : {i j : Level}{A : UU i}{B : A → UU j} → (f g : (a : A) → B a) → UU(i ⊔ j)
f ∼ g = (x : _) → Id (f x) (g x)

-- Identities and composition; type "\circ" to get "∘"
id : {i : Level} (A : UU i) → A → A
id A a = a

_∘_ : {i j k : Level} {A : UU i} {B : UU j} {C : UU k} → (B → C) → (A → B) → (A → C)
(g ∘ f) a = g (f a)

-- Definition 9.2.1: equivalences as bi-invertible maps
sec : {i j : Level}{A : UU i}{B : UU j} → (A → B) → UU(i ⊔ j)
sec {A = A}{B = B} f = Σ (B → A) λ s → (f ∘ s) ∼ id B

retr : {i j : Level}{A : UU i}{B : UU j} → (A → B) → UU(i ⊔ j)
retr {A = A}{B = B} f = Σ (B → A) λ r → (r ∘ f) ∼ id A

is-equiv : {i j : Level}{A : UU i}{B : UU j} → (A → B) → UU(i ⊔ j)
is-equiv f = (sec f) × (retr f)

-- Exercise: prove is-equiv-id, that the identity function defines an equivalence

-- Remark 9.2.6: the type of maps that have a two-sided inverse
has-inverse : {i j : Level}{A : UU i}{B : UU j} → (A → B) → UU(i ⊔ j)
has-inverse {A = A}{B = B} f = Σ (B → A)(λ g → ((f ∘ g) ∼ (id B)) × ((g ∘ f) ∼ (id A)))

-- Exercise: prove that two-sided inverses define equivalences
-- is-equiv-has-inverse : {i j : Level}{A : UU i}{B : UU j}{f : A → B} → has-inverse(f) → is-equiv(f)

-- Here are the path inversion and concatenation functions:
inv : {i : Level}{A : UU i}{x y : A} → (Id x y) → (Id y x)
inv refl = refl

_·_ : {i : Level}{A : UU i}{x y z : A} → (Id x y) → (Id y z) → (Id x z)
refl · q = q

-- Exercise 9.1: prove is-equiv-inv, showing that (λ (p : Id x y) → inv p) is an equivalence
-- Hint: it might be useful to first define the homotopies you need

-- The type of equivalences between A and B; type "\simeq" for "≃".
_≃_ : {i j : Level} → (A : UU i) → (B : UU j) → UU(i ⊔ j)
A ≃ B = Σ (A → B)(λ f → is-equiv f)

-- Exercise 9.1: conclude that (Id x y) ≃ (Id y x)
-- equiv-inv : {i : Level} {A : UU i} (x y : A) → (Id x y) ≃ (Id y x)

-- Definition 5.3.1: the application of functions on paths
ap : {i j : Level}{A : UU i}{B : UU j}{x y : A} → (f : A → B) → (Id x y) → (Id (f x) (f y))
ap f refl = refl
   
-- Definition 5.4.1: the transport function
tr : {i j : Level}{A : UU i}(B : A → UU j){x y : A} → (Id x y) → (B x) → (B y)
tr B refl b = b

-- Exercise 9.1: prove is-equiv-tr
-- is-equiv-tr : {i j : Level}{A : UU i}(B : A → UU j){x y : A}(p : Id x y) → is-equiv(λ b → (tr B p b))

-- Challenge Exercise 9.1: prove that the function concat p z defined below is an equivalence
-- Hint: you may want to copy the definitions of some of the coherence terms
-- concat : {i : Level}{A : UU i}{x y : A} (p : Id x y) (z : A) → (Id y z) → (Id x z)
-- concat p z q = p · q

data 𝟙 : UU lzero where
    star : 𝟙

-- Exercise (Example 9.2.9): prove right-unit-law-prod showing that (A × 𝟙) ≃ A for any type A.
-- Hint: either pre-define the coherence homotopy you need or fill a hole with an expression of the form
-- "λ {x → ?}" and C_c C-space to create a new hole where the "?" appears. 
-- This allows you to type x into the new hole and case split.

data ∅ : UU lzero where

data coprod {i j : Level}(A : UU i)(B : UU j) : UU (i ⊔ j) where
    inl : A → coprod A B
    inr : B → coprod A B

_+_ : {i j : Level} → (A : UU i) → (B : UU j) → UU (i ⊔ j)
A + B = coprod A B 

-- Challenge Exercise (Example 9.2.9): prove right-unit-law-coprod that (A + ∅) ≃ A
-- Hint: Either pre-define your terms or in a hole, type a function as "λ {x → ?}" and C-c C-space
-- to create a new hole in which you can case split the variable x.

-- Definition 10.1.1: is-contr A asserts that the type A is contractible
is-contr : {i : Level}(A : UU i) → UU i
is-contr A = Σ A (λ a → (x : A) → (Id a x))

-- Exercise: show that any two points in a contractible type may be identified
-- contr-is-prop : {i : Level}{A : UU i} → is-contr A → (x y : A) → (Id x y)

-- Challenge Exercise 10.1: Show that if A is contractible then for all x y : A the identity type Id x y is contractible
-- is-prop-is-contr : {i : Level}{A : UU i} → (is-contr A) → (x y : A) → is-contr (Id x y)

terminal-map : {i : Level} → (A : UU i) → (A → 𝟙)
terminal-map A a = star

_↔_ : {i j : Level} → (A : UU i) → (B : UU j) → UU(i ⊔ j)
A ↔ B = (A → B) × (B → A)

-- Challenge Exercise 10.3.a: show is-contr A ↔ is-equiv (terminal-map A) for types A : UU lzero