Mercurial > hg > Members > kono > Proof > category

annotate freyd.agda @ 438:ce9edc8088e8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Aug 2016 00:19:10 +0900
parents 9be298a02c35
children bc0682b86b91
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) } →
436
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
19 (x≈y : A [ FMap F x ≈ FMap F y ]) → FMap F x ≡ FMap F y -- codomain of FMap is local small
307
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 ]
305
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 304
diff changeset
21
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
22 -- pre-initial
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
23
311
cf278f4d0b32 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
24 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
cf278f4d0b32 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
25 (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
26 field
314
d1af69c4aaf8 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
27 preinitialObj : ∀{ a : Obj A } → Obj A
d1af69c4aaf8 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
28 preinitialArrow : ∀{ a : Obj A } → Hom A ( FObj F (preinitialObj {a} )) a
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
29
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
30 -- initial object
308
7f00cd09274c pre-initial
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
31
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
32 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
33 field
314
d1af69c4aaf8 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
34 initial : ∀( a : Obj A ) → Hom A i a
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
35 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
36
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 314
diff changeset
37 -- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
38
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
39 open NTrans
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
40 open Limit
313
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
41 open SmallFullSubcategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 312
diff changeset
42 open PreInitial
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
43
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
44 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
45 (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
46 (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
47 ( equ : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
309
e213595b845e preinitial problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
48 (SFS : SmallFullSubcategory A F FMap← ) →
436
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
49 (PI : PreInitial A F ) → { a0 : Obj A } →
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
50 { u : (a : Obj A) → NTrans A A (K A A a) F } -- Does it exist?
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
51 → HasInitialObject A a0
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
52 initialFromPreInitialFullSubcategory A F FMap← lim equ SFS PI {a0} {u} = record {
314
d1af69c4aaf8 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
53 initial = initialArrow ;
312
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
54 uniqueness = λ a f → lemma1 a f
702adc45704f is this right direction?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
55 } where
437
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
56 f : {a : Obj A} -> Hom A a0 (FObj F (preinitialObj PI {a} ) )
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
57 f {a} = limit (lim F {FObj F (preinitialObj PI {a} )} {u (FObj F (preinitialObj PI))} ) a0 (u a0 )
314
d1af69c4aaf8 on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
58 initialArrow : ∀( a : Obj A ) → Hom A a0 a
437
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
59 initialArrow a = A [ preinitialArrow PI {a} o f ]
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
60 limit-u : Limit A A F a0 (u a0)
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
61 limit-u = lim F {a0} {u a0}
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
62 equ-fi : { a c : Obj A} -> { p : Hom A c a0 } -> {f' : Hom A a0 a} ->
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
63 Equalizer A p ( A [ preinitialArrow PI {a} o f ] ) f'
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
64 equ-fi {a} {c} {p} {f'} = equ ( A [ preinitialArrow PI {a} o limit (lim F) a0 (u a0) ] ) f'
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
65 e=id : {e : Hom A a0 a0} -> ( {c : Obj A} -> A [ A [ TMap (u a0) c o e ] ≈ TMap (u a0) c ] ) -> A [ e ≈ id1 A a0 ]
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
66 e=id {e} uce=uc = let open ≈-Reasoning (A) in
437
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
67 begin
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
68 e
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
69 ≈↑⟨ limit-uniqueness limit-u {a0} {u a0} {e} ( \{i} -> uce=uc ) ⟩
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
70 limit limit-u a0 (u a0)
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
71 ≈⟨ limit-uniqueness limit-u {a0} {u a0} {id1 A a0} ( \{i} -> idR ) ⟩
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
72 id1 A a0
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
73 ∎
436
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
74 open Equalizer
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
75 kfuc=uc : {c k1 : Obj A} -> A [ A [ TMap (u a0) c o
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
76 A [ equalizer (equ-fi {a0} {k1} {{!!}} {{!!}} ) o A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ]
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
77 ≈ TMap (u a0) c ]
437
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
78 kfuc=uc {k1} {c} = {!!}
9be298a02c35 add rest of equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 436
diff changeset
79 kfuc=1 : {k1 : Obj A} -> A [ A [ equalizer (equ-fi {a0} {k1} {{!!}} {{!!}} ) o
436
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
80 A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ≈ id1 A a0 ]
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
81 kfuc=1 {k1} = e=id kfuc=uc
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
82 -- if equalizer has right inverse, f = g
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
83 lemma2 : (a b : Obj A) {c : Obj A} ( f g : Hom A a b )
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
84 {e : Hom A c a } {e' : Hom A a c } ( equ : Equalizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] )
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
85 -> A [ f ≈ g ]
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
86 lemma2 a b {c} f g {e} {e'} equ inv-e = let open ≈-Reasoning (A) in
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
87 let open Equalizer in
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
88 begin
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
89 f
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
90 ≈↑⟨ idR ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
91 f o id1 A a
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
92 ≈↑⟨ cdr inv-e ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
93 f o ( e o e' )
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
94 ≈⟨ assoc ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
95 ( f o e ) o e'
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
96 ≈⟨ car ( fe=ge equ ) ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
97 ( g o e ) o e'
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
98 ≈↑⟨ assoc ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
99 g o ( e o e' )
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
100 ≈⟨ cdr inv-e ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
101 g o id1 A a
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
102 ≈⟨ idR ⟩
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
103 g
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
104 ∎
436
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
105 lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ initialArrow a ]
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
106 lemma1 a f' = let open ≈-Reasoning (A) in
436
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
107 sym (
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
108 begin
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
109 initialArrow a
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
110 ≈⟨⟩
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
111 preinitialArrow PI {a} o limit (lim F) a0 (u a0)
438
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
112 ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o limit (lim F) a0 (u a0) ]) f' equ-fi (kfuc=1 {a} ) ⟩
ce9edc8088e8 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 437
diff changeset
113 f'
436
ef37decef1ca initialFullSubCategory
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 435
diff changeset
114 ∎ )
435
9f014f34b988 f=g if equalizer k has right inverse
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 350
diff changeset
115