Home

関数は関手である

module foundations.functions-are-functors where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.groupoid-laws
open import foundations.function

任意の関数は関手となる。

private variable
  ℓ : Level
  A B C : Type ℓ

ap : ∀ (f : A → B) {x y : A} → x ＝ y → f x ＝ f y
ap f refl = refl

ap∙ : ∀ (f : A → B) {x y z : A}
  → ∀ (p : x ＝ y) (q : y ＝ z)
  → ap f (p ∙ q) ＝ ap f p ∙ ap f q
ap∙ f refl q =
  ap (ap f) (lunitId q) ∙ sym (lunitId (ap f q))

apSym : ∀ (f : A → B) {x y : A}
  → ∀ (p : x ＝ y)
  → ap f (sym p) ＝ sym (ap f p)
apSym f refl = ap (ap f) symRefl ∙ sym symRefl

apAp : ∀ (f : A → B) (g : B → C) {x y : A}
  → ∀ (p : x ＝ y)
  → ap g (ap f p) ＝ ap (g ∘ f) p
apAp _ _ refl = refl

apId : ∀ {x y : A} (p : x ＝ y)
  → ap (λ v → v) p ＝ p
apId refl = refl