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

Research