Mercurial > hg > Members > kono > Proof > category
annotate freyd1.agda @ 487:c257347a27f3
found limit in freyd
isLimit introduced
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 12 Mar 2017 19:46:07 +0900 |
| parents | 56cf6581c5f6 |
| children | 016087cfa75a |
| 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 |
| 485 | 60 commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) |
| 487 | 61 → ( glimit : LimitPreserve A I C G ) |
| 62 → Obj CommaCategory | |
| 485 | 63 commaLimit {I} comp Γ glimit = record { |
|
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 obj = limit-c comp (FIA Γ) |
|
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 ; hom = limitHom |
|
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 } where |
|
486
56cf6581c5f6
add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
485
diff
changeset
|
67 frev : {i : Obj I } → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i)) |
| 487 | 68 frev {i} = TMap (t0 ( climit comp (FIA Γ))) i |
| 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 ] ] | |
| 71 ≈ C [ C [ hom (FObj Γ b) o FMap F frev ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ] | |
| 72 commute {a} {b} {f} = ? | |
| 485 | 73 tu : NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (FICG Γ) |
| 74 tu = record { | |
|
486
56cf6581c5f6
add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
485
diff
changeset
|
75 TMap = λ i → C [ hom ( FObj Γ i ) o FMap F frev ] |
| 487 | 76 ; isNTrans = record { commute = λ {a} {b} {f}→ commute {a} {b} {f} } |
| 485 | 77 } |
| 487 | 78 uHomF : Hom C ( FObj F ( limit-c comp (FIA Γ) ) ) (FObj G ( (a0 (climit comp (FIA Γ) )))) |
| 79 uHomF = limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) tu | |
|
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) |
| 487 | 81 limitHom = uHomF |
|
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 |
|
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 |
|
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) |
| 485 | 85 → ( glimit : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) ) |
| 86 → NTrans I CommaCategory (K CommaCategory I {!!}) Γ | |
| 87 commaNat {I} comp Γ gilmit = record { | |
| 88 TMap = λ x → {!!} | |
|
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 ; isNTrans = record { commute = {!!} } |
|
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 } where |
|
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
91 |
|
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 |
|
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) |
| 485 | 94 → ( glimit : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) ) |
| 95 → ( Γ : Functor I CommaCategory ) | |
| 96 → Limit CommaCategory I Γ | |
| 97 hasLimit {I} comp glimit Γ = record { | |
| 98 a0 = {!!} ; | |
| 99 t0 = {!!} ; | |
| 487 | 100 isLimit = record { |
| 101 limit = λ a t → {!!} ; | |
| 102 t0f=t = λ {a t i } → {!!} ; | |
| 103 limit-uniqueness = λ {a} {t} f t=f → {!!} | |
| 104 } | |
|
481
65e6906782bb
Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 } |