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

Why do the induction principles for identity types not allow us to construct a function $f : \prod x : A \prod p : x \equiv x (p \equiv refl_{x})$ with the defining equation $f (x, refl_{x}) :\equiv refl_refl_{x}$ ?

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.

Research