Mercurial > hg > Members > kono > Proof > category

annotate freyd.agda @ 312:702adc45704f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
is this right direction?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jan 2014 23:37:12 +0900
parents cf278f4d0b32
children d72730946ba5
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category -- https://github.com/konn/category-agda
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 where
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
7 open import cat-utility
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
8 open import HomReasoning
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Binary.Core
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
10 open Functor
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
311
cf278f4d0b32 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
12 -- C is small full subcategory of A ( C is image of F )
304
bd7b3f3d1d4c Freyd Adjoint Functor Theorem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
14 record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
15 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
16 : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
306
92475fe5f59e Small Full Subcategory (underconstruction)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
17 field
307
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
18 ≈→≡ : {a b : Obj A } → { x y : Hom A (FObj F a) (FObj F b) } →
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
19 (x≈y : A [ FMap F x ≈ FMap F y ]) → FMap F x ≡ FMap F y -- co-comain of FMap is local small
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
20 full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ]
9872bddec072 small full subcategory done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 306
diff changeset
21 full← : { a b : Obj A } { x : Hom A a b } → A [ FMap← ( FMap F x ) ≈ x ]
305
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
22
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
23 -- pre-initial
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
24
311
cf278f4d0b32 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
25 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
cf278f4d0b32 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
26 (F : Functor A A ) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
308
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
27 field
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
28 preinitial : ∀{ a : Obj A } → { b : Obj A } → Hom A ( FObj F b ) a
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
29 uniqueness : ∀{ a : Obj A } → { b : Obj A } → ( f : Hom A ( FObj F b ) a ) →
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
30 A [ f ≈ preinitial {a} {b} ]
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
31
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
32 -- initial object
308
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
33
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
34 record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
35 field
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
36 initial : ( a : Obj A ) → Hom A i a
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
37 uniqueness : ( a : Obj A ) → ( f : Hom A i a ) → A [ f ≈ initial a ]
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
38
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
39
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
40 -- A has initial object if it has PreInitial-SmallFullSubcategory
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
41
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
42 open NTrans
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
43 open Limit
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
44
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
45 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
46 (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
47 (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
48 (SFS : SmallFullSubcategory A F FMap← ) →
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
49 (PreInitial A F ) → { a0 : Obj A } → { u : (a : Obj A) → NTrans A A (K A A a) F }
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
50 → HasInitialObject A a0
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
51 initialFromPreInitialFullSubcategory A F FMap← lim SFS PI {a0} {u} = record {
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
52 initial = λ a → limit (lim F {a} {u a} ) a0 (u a0) ;
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
53 uniqueness = λ a f → lemma1 a f
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
54 } where
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
55 lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ limit (lim F) a0 (u a0) ]
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
56 lemma1 a f = let open ≈-Reasoning (A) in
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
57 begin
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
58 f
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
59 ≈↑⟨ limit-uniqueness (lim F) ( λ {i} →
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
60 begin
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
61 TMap (u a) i o f
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
62 ≈⟨ ? ⟩
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
63 TMap (u a0) i
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
64 ∎
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
65 )⟩
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
66 limit (lim F) a0 (u a0)
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
67 ∎
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
68