26-06-07
圏論の基本的な部分はagdaで理解した方が明示的で分かりやすい。 plfaでやったところの延長で組んでみたけど、最初からやればよかった。
定義のフィールドが明示的に効いてくるのが嬉しい点で、
infix 0 _≃_
record _≃_ {ℓ₁ ℓ₂ : Level} (A : Type ℓ₁) (B : Type ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
field
to : A → B
from : B → A
from∘to : ∀ (x : A) → from (to x) ≡ x
to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_
同型を使う時にフィールドの条件が満たさないと主張が通らない。他の難しそうに見える概念もagdaの宣言におけるレコードとしてひと括りに考えられるからシンプルに理解できるので良い。この場合は≃に掛かる左辺と右辺を引数としてto∘fromとfrom∘toが成立すれば、同型であるという主張が通る。数学書読んでて、文字通りに「同型だ」と言われても全く分からないが、agdaなら分かりやすい。これが直観主義数学書の頻出ワードexplicitnessのパワー！
同型に限らず、Set以上に条件のある集合など引数の有無に関わらず、関係性にまつわる記号は「Agdaにおけるrecordのfield群」として記述できる。
なぜこれが理解しやすいかというと0 < 1(1は0より大きいよ)と根本的には同じだからだ。
module cat where
open import Agda.Primitive
using (Level; lzero; lsuc; _⊔_)
renaming (Set to Type)
open import Agda.Builtin.Equality
trans : ∀ {ℓ} {A : Type ℓ} {x y z : A}
→ x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
sym : ∀ {ℓ} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
cong : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂}
(f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl
infix 0 _≃_
record _≃_ {ℓ₁ ℓ₂ : Level} (A : Type ℓ₁) (B : Type ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
field
to : A → B
from : B → A
from∘to : ∀ (x : A) → from (to x) ≡ x
to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_
record Category (o h : Level) : Type (lsuc (o ⊔ h)) where
field
ob : Type o
hom : ob → ob → Type h
id : ∀ {A : ob} → hom A A
_·_ : ∀ {A B C : ob} → hom B C → hom A B → hom A C
left-id : ∀ {A B} (f : hom A B) → id · f ≡ f
right-id : ∀ {A B} (f : hom A B) → f · id ≡ f
assoc : ∀ {A B C D} (f : hom A B)(g : hom B C)(h : hom C D)
→ (h · g) · f ≡ h · (g · f)
record Functor {o₁ h₁ o₂ h₂}
(C : Category o₁ h₁)
(D : Category o₂ h₂)
: Type (lsuc (o₁ ⊔ h₁ ⊔ o₂ ⊔ h₂)) where
open Category
field
F₀ : ob C → ob D
F₁ : ∀ {A B} → hom C A B → hom D (F₀ A) (F₀ B)
F-id : ∀ {A} → F₁ (id C {A}) ≡ id D
F-comp : ∀ {A B C'} (f : hom C A B)(g : hom C B C')
→ F₁ (_·_ C g f) ≡ _·_ D (F₁ g) (F₁ f)
IdF : ∀ {o h} (C : Category o h) → Functor C C
IdF C = record
{ F₀ = λ A → A
; F₁ = λ f → f
; F-id = refl
; F-comp = λ f g → refl
}
_∘F_ : ∀ {o₁ h₁ o₂ h₂ o₃ h₃}
{C : Category o₁ h₁}
{D : Category o₂ h₂}
{E : Category o₃ h₃}
→ Functor D E → Functor C D → Functor C E
G ∘F F = record
{ F₀ = λ A → Functor.F₀ G (Functor.F₀ F A)
; F₁ = λ f → Functor.F₁ G (Functor.F₁ F f)
; F-id = trans (cong (Functor.F₁ G) (Functor.F-id F))
(Functor.F-id G)
; F-comp = λ f g → trans (cong (Functor.F₁ G) (Functor.F-comp F f g))
(Functor.F-comp G _ _)
}
record NatTrans {o₁ h₁ o₂ h₂}
{C : Category o₁ h₁}
{D : Category o₂ h₂}
(F G : Functor C D)
: Type (o₁ ⊔ h₁ ⊔ h₂) where
open Category D
open Functor
field
α : ∀ (A : Category.ob C) → hom (F₀ F A) (F₀ G A)
natural : ∀ {A B} (f : Category.hom C A B)
→ α B · F₁ F f ≡ F₁ G f · α A
idNat : ∀ {o₁ h₁ o₂ h₂}
{C : Category o₁ h₁}
{D : Category o₂ h₂}
(F : Functor C D)
→ NatTrans F F
idNat {D = D} F = record
{ α = λ A → Category.id D
; natural = λ f → trans (Category.left-id D _)
(sym (Category.right-id D _))
}
record Adjunction {o₁ h₁ o₂ h₂}
{C : Category o₁ h₁}
{D : Category o₂ h₂}
(F : Functor C D)
(G : Functor D C)
: Type (lsuc (o₁ ⊔ h₁ ⊔ o₂ ⊔ h₂)) where
open Category
open Functor
field
adj : ∀ (A : ob C)(B : ob D)
→ hom D (F₀ F A) B ≃ hom C A (F₀ G B)
natural-A : ∀ {A A' : ob C}{B : ob D}
(f : hom C A' A)(g : hom D (F₀ F A) B)
→ to (adj A' B) (_·_ D g (F₁ F f))
≡ _·_ C (to (adj A B) g) f
natural-B : ∀ {A : ob C}{B B' : ob D}
(h : hom D B B')(g : hom D (F₀ F A) B)
→ to (adj A B') (_·_ D h g)
≡ _·_ C (F₁ G h) (to (adj A B) g)
-- unit : A → GFA
unit : ∀ (A : ob C) → hom C A (F₀ G (F₀ F A))
unit A = to (adj A (F₀ F A)) (id D)
-- counit : FGB → B
counit : ∀ (B : ob D) → hom D (F₀ F (F₀ G B)) B
counit B = from (adj (F₀ G B) B) (id C)
record Monad {o h}
(C : Category o h)
(T : Functor C C)
: Type (o ⊔ h) where
open Category C
open Functor T renaming (F₀ to T₀; F₁ to T₁)
field
η : ∀ {A} → hom A (T₀ A)
μ : ∀ {A} → hom (T₀ (T₀ A)) (T₀ A)
left-unit : ∀ {A} → μ · η {T₀ A} ≡ id
right-unit : ∀ {A} → μ · T₁ (η {A}) ≡ id
assoc-μ : ∀ {A} → μ · μ {T₀ A} ≡ μ · T₁ (μ {A})
?26-06-08 | ?26-06-06