{-# OPTIONS --rewriting #-} module HottBook.Chapter5 where open import Agda.Primitive open import HottBook.Chapter1
5.1 Introduction to inductive types
Theorem 5.1.1
-- theorem5∙1∙1 : {E : ℕ → Set} -- → (f g : (x : ℕ) → E x) -- → (z : f 0 ≡ g 0) -- → (s : -- → f ≡ g
Definition 5.4.1
ℕAlg : {l : Level} → Set (lsuc l) ℕAlg {l} = Σ (Set l) (λ C → C × (C → C))
Definition 5.4.2
ℕHom : {l : Level} → ℕAlg {l} → ℕAlg {l} → Set l ℕHom alg1@(C , (cz , cs)) alg2@(D , (dz , ds)) = Σ (C → D) λ h → (h cz ≡ dz) × ((c : C) → h (cs c) ≡ ds (h c))