Mercurial > hg > Members > kono > Proof > category
annotate freyd1.agda @ 489:75a60ceb55af
on going ..
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 12 Mar 2017 22:10:54 +0900 |
parents | 016087cfa75a |
children | 1a42f06e7ae1 |
rev | line source |
---|---|
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Category -- https://github.com/konn/category-agda |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Level |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 module freyd1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 ( F : Functor A C ) ( G : Functor A C ) where |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import cat-utility |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import HomReasoning |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import Relation.Binary.Core |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open Functor |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 open import Comma1 F G |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 open import freyd CommaCategory |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open import Category.Cat |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 open NTrans |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 open Complete |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 open CommaObj |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 open CommaHom |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 open Limit |
487 | 24 open IsLimit |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 |
483 | 26 -- F : A → C |
27 -- G : A → C | |
28 -- | |
29 | |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 FIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I A |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 FIA {I} Γ = record { |
482 | 32 FObj = λ x → obj (FObj Γ x ) ; |
33 FMap = λ {a} {b} f → arrow (FMap Γ f ) ; | |
34 isFunctor = record { | |
35 identity = identity | |
36 ; distr = IsFunctor.distr (isFunctor Γ) | |
37 ; ≈-cong = IsFunctor.≈-cong (isFunctor Γ) | |
38 }} where | |
39 identity : {x : Obj I } → A [ arrow (FMap Γ (id1 I x)) ≈ id1 A (obj (FObj Γ x)) ] | |
40 identity {x} = let open ≈-Reasoning (A) in begin | |
41 arrow (FMap Γ (id1 I x)) | |
42 ≈⟨ IsFunctor.identity (isFunctor Γ) ⟩ | |
43 id1 A (obj (FObj Γ x)) | |
44 ∎ | |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 |
485 | 46 FICG : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C |
47 FICG {I} Γ = G ○ (FIA Γ) | |
48 | |
49 FICF : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C | |
50 FICF {I} Γ = F ○ (FIA Γ) | |
51 | |
487 | 52 open LimitPreserve |
483 | 53 |
484
fcae3025d900
fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
483
diff
changeset
|
54 LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) |
485 | 55 → ( Γ : Functor I CommaCategory ) |
487 | 56 → ( glimit : LimitPreserve A I C G ) |
485 | 57 → Limit C I (FICG Γ) |
487 | 58 LimitC {I} comp Γ glimit = plimit glimit (FIA Γ) (climit comp (FIA Γ)) |
486
56cf6581c5f6
add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
485
diff
changeset
|
59 |
489 | 60 frev : { I : Category c₁ c₂ ℓ } → (comp : Complete A I) → ( Γ : Functor I CommaCategory ) (i : Obj I ) → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i)) |
61 frev comp Γ i = TMap (t0 ( climit comp (FIA Γ))) i | |
62 | |
63 tu : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) | |
64 → NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (FICG Γ) | |
65 tu {I} comp Γ = record { | |
66 TMap = λ i → C [ hom ( FObj Γ i ) o FMap F (frev comp Γ i) ] | |
67 ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } | |
68 } where | |
69 commute : {a b : Obj I} {f : Hom I a b} → | |
70 C [ C [ FMap (FICG Γ) f o C [ hom (FObj Γ a) o FMap F (frev comp Γ a) ] ] | |
71 ≈ C [ C [ hom (FObj Γ b) o FMap F (frev comp Γ b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ] | |
72 commute {a} {b} {f} = let open ≈-Reasoning (C) in begin | |
73 FMap (FICG Γ) f o ( hom (FObj Γ a) o FMap F (frev comp Γ a) ) | |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
74 ≈⟨⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
75 FMap G (arrow (FMap Γ f ) ) o ( hom (FObj Γ a) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a )) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
76 ≈⟨ assoc ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
77 (FMap G (arrow (FMap Γ f ) ) o hom (FObj Γ a)) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
78 ≈⟨ car ( comm (FMap Γ f)) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
79 (hom (FObj Γ b) o FMap F (arrow (FMap Γ f)) ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
80 ≈↑⟨ assoc ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
81 hom (FObj Γ b) o ( FMap F (arrow (FMap Γ f)) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ) ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
82 ≈↑⟨ cdr (distr F) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
83 hom (FObj Γ b) o ( FMap F (A [ arrow (FMap Γ f) o TMap (t0 ( climit comp (FIA Γ))) a ] ) ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
84 ≈⟨⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
85 hom (FObj Γ b) o ( FMap F (A [ FMap (FIA Γ) f o TMap (t0 ( climit comp (FIA Γ))) a ] ) ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
86 ≈⟨ cdr ( fcong F ( IsNTrans.commute (isNTrans (t0 ( climit comp (FIA Γ))) ))) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
87 hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K A I (a0 (climit comp (FIA Γ)))) f ] )) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
88 ≈⟨⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
89 hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o id1 A (limit-c comp (FIA Γ)) ] )) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
90 ≈⟨ cdr ( distr F ) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
91 hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o FMap F (id1 A (limit-c comp (FIA Γ)))) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
92 ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
93 hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ)))) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
94 ≈⟨ assoc ⟩ |
489 | 95 ( hom (FObj Γ b) o FMap F (frev comp Γ b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
96 ∎ |
489 | 97 limitHom : { I : Category c₁ c₂ ℓ } → (comp : Complete A I) → ( Γ : Functor I CommaCategory ) |
98 → ( glimit : LimitPreserve A I C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) | |
99 limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) | |
100 | |
101 commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) | |
102 → ( glimit : LimitPreserve A I C G ) | |
103 → Obj CommaCategory | |
104 commaLimit {I} comp Γ glimit = record { | |
105 obj = limit-c comp (FIA Γ) | |
106 ; hom = limitHom comp Γ glimit | |
107 } | |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
108 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
109 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
110 commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
111 → ( glimit : LimitPreserve A I C G ) |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
112 → NTrans I CommaCategory (K CommaCategory I (commaLimit {I} comp Γ glimit)) Γ |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
113 commaNat {I} comp Γ glimit = record { |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
114 TMap = λ x → record { |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
115 arrow = TMap ( limit-u comp (FIA Γ ) ) x |
489 | 116 ; comm = comm1 x |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
117 } |
489 | 118 ; isNTrans = record { commute = comm2 } |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
119 } where |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
120 comm1 : (x : Obj I ) → |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
121 C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) ] |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
122 ≈ C [ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ] ] |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
123 comm1 x = let open ≈-Reasoning (C) in begin |
489 | 124 FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) |
125 ≈⟨⟩ | |
126 FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (commaLimit comp Γ glimit) | |
127 ≈⟨⟩ | |
128 FMap G (TMap (limit-u comp (FIA Γ)) x) o limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) | |
129 ≈⟨⟩ | |
130 TMap (t0 ( LimitC comp Γ glimit )) x o limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) | |
131 ≈⟨ t0f=t ( isLimit ( LimitC comp Γ glimit ) ) ⟩ | |
132 TMap (tu comp Γ) x | |
133 ≈⟨⟩ | |
134 hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) | |
135 ∎ | |
136 comm2 : {a b : Obj I} {f : Hom I a b} → | |
137 CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ] | |
138 ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f ] ] | |
139 comm2 {a} {b} {f} = let open ≈-Reasoning (CommaCategory) in begin | |
140 FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } | |
141 ≈⟨ {!!} ⟩ | |
142 record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f | |
143 ∎ | |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
144 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
145 |
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
146 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
147 → ( glimit : LimitPreserve A I C G ) |
485 | 148 → ( Γ : Functor I CommaCategory ) |
149 → Limit CommaCategory I Γ | |
150 hasLimit {I} comp glimit Γ = record { | |
488
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
151 a0 = commaLimit {I} comp Γ glimit ; |
016087cfa75a
commaLimit done, commaNat trying..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
487
diff
changeset
|
152 t0 = commaNat { I} comp Γ glimit ; |
487 | 153 isLimit = record { |
154 limit = λ a t → {!!} ; | |
155 t0f=t = λ {a t i } → {!!} ; | |
156 limit-uniqueness = λ {a} {t} f t=f → {!!} | |
157 } | |
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
158 } |