exercises3.agda

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

module exercises3 where
{-
Please rename your file to exercises3-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

-- 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

-- Egbert writes "Id x y" for the type of identifications from x to y. 
-- Note it's not possible to call this type "x = y" or "x =_A y" since agda uses "=" for something else.
-- In the homotopy type theory community, other notations are fairly common, such as:
_==_ : {i : Level}{A : UU i} → A → A → UU i
x == y = Id x y

-- Or type "\equiv" for "≡"
_≡_ : {i : Level}{A : UU i} → A → A → UU i
x ≡ y = Id x y
-- If you prefer either of these, feel free to use them in what follows.

-- Here is path-ind_a, the one-sided path induction function: 
path-ind : {i j : Level}(A : UU i)(a : A)(P : (x : A) → (p : Id a x) → UU j) → (P a refl) → ((x : A) → (p : Id a x) → (P x p))
path-ind A a P pf x refl = pf

-- It's possible to use path-ind to prove theorems, like the invertibility of paths:
inverse-law : {i : Level}{A : UU i}{x y : A} → (Id x y) → (Id y x)
inverse-law {A = A}{x = x}{y = y} = path-ind A x (λ z p → (Id z x)) refl y
-- Here I'm telling agda to apply the function path-ind to the type family "z : A, p : Id x z ⊢ Id z x".
-- For agda to know about the type A and the term x, I needed to make some of the implicit variables of inverse-law explicit by writing {A = A}{x = x}. 
-- For the last argument of path-ind, agda needs to know {y = y} too.

-- But agda gives you another strategy to make definitions by path induction: instead of appealing to the function path-inv
-- you can define a function, like "inv" below, that takes as input a term "p : Id x y". Then type "inv p = ?" and C-c C-l to load. 
-- Type "p" in the hole followed by C-c C-c to case split. By doing so you're telling agda to apply path induction on p.
-- Compare the definition of "inv" below with the definition of "inverse-law" above.

-- Definition 5.2.2: define "inv", the function that reverses paths
inv : {i : Level}{A : UU i}{x y : A} → (Id x y) → (Id y x)
inv refl = refl

-- Definition 5.2.1: definition of path concatenation; type "\cdot" for "·"
-- Type "p · q = ?" and load with C-c C-l. Type either p or q (or both) into the hole to apply path induction to that variable. 
-- Which term did I induct over here?
_·_ : {i : Level}{A : UU i}{x y z : A} → (Id x y) → (Id y z) → (Id x z)
refl · q = q

-- Definition 5.2.3: definition of "assoc", the identification between (p · q) · r and p · (q · r)
assoc : {i : Level}{A : UU i}{w x y z : A} → (p : Id w x) → (q : Id x y) → (r : Id y z) → (Id ((p · q) · r) (p · (q · r)))
assoc refl q r = refl
-- Note if you defined _∘_ in a different way than I did, this might not work.

-- Exercise (Definition 5.2.4): define "left-unit" and "right-unit"

-- Exercise (Definition 5.2.5): define "left-inv" and "right-inv"

-- Exercise 5.1: define distributive-inv-concat
-- distributive-inv-concat : {i : Level}{A : UU i}{x y z : A} → (p : Id x y) → (q : Id y z) → (Id (inv (p · q)) ((inv q) · (inv p)))

-- Exercise 5.2: define inv-con
-- inv-con : {i : Level}{A : UU i}{x y z : A} → (p : Id x y) → (q : Id y z) → (r : Id x z) → (Id (p · q) r) → (Id q ((inv p) · r))

-- Challenge Exercise 5.2: define con-inv (Hint: to get a term in (Id p (r · inv q)) use _·_ to concatenate paths)
-- con-inv : {i : Level}{A : UU i}{x y z : A} → (p : Id x y) → (q : Id y z) → (r : Id x z) → (Id (p · q) r) → (Id p (r · (inv q)))

-- Exercise (Definition 5.3.1): define "ap" the application of functions on paths

-- Definition 5.4.1: here is 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

data Σ {i j : Level}(A : UU i)(B : A → UU j) : UU (i ⊔ j) where
    pair : (a : A) → B a → Σ A B

-- Exercise 5.3: Given a type family z : A ⊢ B z type a path p : a = x in A and a term b : B a define a path "lift B p b" 
-- in the dependent pair type from "pair a b" to "pair x (tr B p b)"

data ℕ : UU lzero where
    zero-ℕ : ℕ
    succ-ℕ : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
-- This isn't strictly necessary for what follows but allows me to write "0" instead of "zero-ℕ" and "1" instead of "succ-ℕ zero-ℕ"

add-ℕ : ℕ → ℕ → ℕ
add-ℕ m zero-ℕ = m
add-ℕ m (succ-ℕ n) = succ-ℕ (add-ℕ m n)

-- Exercise: define the following functions. Can you define one of them without using induction on ℕ? 
-- right-unit-law-add-ℕ : (m : ℕ) → Id (add-ℕ m 0) m

-- left-unit-law-add-ℕ : (m : ℕ) → Id (add-ℕ 0 m) m

-- Exercise: define right-successor-law-add-ℕ and left-successor-law-add-ℕ 
-- right-successor-law-add-ℕ : (m n : ℕ) → Id (add-ℕ m (succ-ℕ n)) (succ-ℕ (add-ℕ m n))

-- left-successor-law-add-ℕ : (m n : ℕ) → Id (add-ℕ (succ-ℕ m) n) (succ-ℕ (add-ℕ m n))

-- Exercise: define associative-add-ℕ, proving (k + m) + n = k + (m + n)

-- Challenge Exercise: define commutative-add-ℕ, proving m + n = n + m

mul-ℕ : ℕ → ℕ → ℕ
mul-ℕ m zero-ℕ = 0
mul-ℕ m (succ-ℕ n) = add-ℕ (mul-ℕ m n) m

-- Exercise 5.5.a: verify the following multiplication laws:
-- left-zero-law-mul-ℕ : (m : ℕ ) → Id (mul-ℕ m 0) 0

-- right-zero-law-mul-ℕ : (m : ℕ) → Id (mul-ℕ 0 m) 0

-- left-unit-law-mul-ℕ : (m : ℕ) → Id (mul-ℕ m 1) m

-- right-unit-law-mul-ℕ : (m : ℕ) → Id (mul-ℕ 1 m) m

-- Challenge exercise 5.5.a:
-- left-successor-law-mul-ℕ : (m n : ℕ) → Id (mul-ℕ m (succ-ℕ n)) (add-ℕ (mul-ℕ m n) m)

-- Challenge exercise 5.5.a:
-- right-successor-law-mul-ℕ : (m n : ℕ) → Id (mul-ℕ (succ-ℕ m) n) (add-ℕ (mul-ℕ m n) n)

-- If you thought that was tough, have a look at Egbert's formalization of the rest of the exercises from this section!
-- https://github.com/HoTT-Intro/Agda/blob/master/book/05-identity-types.agda