大概不知道能放到哪的一些碎碎念的东西… (超小声(
也许放到blog里确实不错, 但还是不好意思往blog里灌这种水… >< (超小声(
5 个赞
(从作业里截的, 并没有什么意义 (超小声(
这种小旗子表示的证明序列可以用 flagderiv 包来排版, 应该也是flagderiv环境, 具体文档反正ctan上也有, 就不copy过来了 (超小声(
3 个赞
(\mathbb{N}, 0, \text{suc}) be initial of a category
Let’s write out the type of object first:
module prob-3-1-2 where
open import Relation.Binary using (Setoid; Rel; IsEquivalence)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
open Level renaming (zero to lzero; suc to lsuc)
open import Data.Nat using (ℕ)
open import Categories.Object.Initial using (IsInitial)
open import Function using (id; _∘_)
record Object {ℓ} : Set (lsuc ℓ) where
field
Ty : Set ℓ
init : Ty
succ : Ty → Ty
To proof our problem, we need to construct the arrow, and prove that the object is an initial.
Simply a function can fit the properties of an arrow in the category well:
record Arrow {ℓ} (A B : Object {ℓ}) : Set (lsuc ℓ) where
module A = Object A
module B = Object B
field
fn : A.Ty → B.Ty
But with only the function, it’s obvious that the arrow from (\mathbb{N}, 0, \text{suc}) is not unique,
since, for example, for set \{0, 1, 2\}, there are infinite functions.
The uniqueness can be ensured by the following properties:
intro : fn A.init ≡ B.init
keep : ∀ {a} → fn (A.succ a) ≡ B.succ (fn a)
With extensionality, we can see that this makes a category.
The equality proof in the arrows may differ, so they’re not counted in the equivalence:
cat : ∀ {ℓ} → Category (lsuc ℓ) (lsuc ℓ) ℓ
cat {ℓ} = record
{ Obj = Object {ℓ}
; _⇒_ = Arrow
; _≈_ = _≈_
; id = record { fn = id ; intro = refl ; keep = refl }
; _∘_ = compose
; assoc = refl
; sym-assoc = refl
; identityˡ = refl
; identityʳ = refl
; identity² = refl
; equiv = record { refl = refl ; sym = λ f≡g → sym f≡g ; trans = λ f≡g g≡h → trans f≡g g≡h }
; ∘-resp-≈ = λ {A} {B} {C} {f} {h} {g} {i} → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i}
}
where
_≈_ : ∀ {A B : Object {ℓ}} → Rel (Arrow A B) ℓ
_≈_ f g = Arrow.fn f ≡ Arrow.fn g
compose : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
compose g f = record
{ fn = g.fn ∘ f.fn
; intro = trans (cong g.fn f.intro) g.intro
; keep = trans (cong g.fn f.keep) g.keep
}
where
module g = Arrow g
module f = Arrow f
∘-resp-≈ : ∀ {A B C : Object} {f h : Arrow B C} {g i : Arrow A B} →
f ≈ h → g ≈ i → compose f g ≈ compose h i
∘-resp-≈ refl refl = refl
module cat {ℓ} = Category (cat {ℓ})
The construction of the arrows is canonical, and with extensionality, we can show that the object is initial:
obj : Object
obj = record { Ty = ℕ ; init = 0 ; succ = ℕ.suc }
module obj = Object obj
postulate
extensionality : ∀ {ℓ} {A B : Set ℓ} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
init : IsInitial cat obj
init = record { ! = arr ; !-unique = λ f → extensionality (uniq f) }
where
fn : ∀ (a : Object) → ℕ → Object.Ty a
fn record { init = init } ℕ.zero = init
fn a@(record { succ = succ }) (ℕ.suc i) = succ (fn a i)
arr : {a : Object} → Arrow obj a
arr {a} = record { fn = fn a ; intro = refl ; keep = refl }
uniq : ∀ {a : Object} (f : Arrow obj a) → ∀ x → fn a x ≡ Arrow.fn f x
uniq {record { init = .(f 0) }} record { fn = f ; intro = refl } ℕ.zero = refl
uniq {record { succ = succ }} f@(record { keep = keep }) (ℕ.suc x) = trans (cong succ (uniq f x)) (sym (keep {x}))
1 个赞