Mercurial > hg > Members > kono > Proof > category

annotate freyd1.agda @ 486:56cf6581c5f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some lemma but no use
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Mar 2017 14:48:14 +0900
parents da4486523f73
children c257347a27f3
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
483
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
25 -- F : A → C
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
26 -- G : A → C
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
27 --
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
28
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 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
30 FIA {I} Γ = record {
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
31 FObj = λ x → obj (FObj Γ x ) ;
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
32 FMap = λ {a} {b} f → arrow (FMap Γ f ) ;
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
33 isFunctor = record {
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
34 identity = identity
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
35 ; distr = IsFunctor.distr (isFunctor Γ)
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
36 ; ≈-cong = IsFunctor.≈-cong (isFunctor Γ)
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
37 }} where
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
38 identity : {x : Obj I } → A [ arrow (FMap Γ (id1 I x)) ≈ id1 A (obj (FObj Γ x)) ]
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
39 identity {x} = let open ≈-Reasoning (A) in begin
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
40 arrow (FMap Γ (id1 I x))
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
41 ≈⟨ IsFunctor.identity (isFunctor Γ) ⟩
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
42 id1 A (obj (FObj Γ x))
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
43 ∎
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
45 NIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory )
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
46 (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ ) → NTrans I A ( K A I (obj c) ) (FIA Γ)
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
47 NIA {I} Γ c ta = record {
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
48 TMap = λ x → arrow (TMap ta x )
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
49 ; isNTrans = record { commute = comm1 }
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
50 } where
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
51 comm1 : {a b : Obj I} {f : Hom I a b} →
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
52 A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ]
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
53 comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta )
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
54
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
55 tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B )
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
56 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) →
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
57 ( U : Functor B C) → NTrans I C ( K C I (FObj U lim) ) (U ○ Γ)
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
58 tb B I Γ lim tb U = record {
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
59 TMap = TMap (Functor*Nat I C U tb) ;
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
60 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
61 FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
62 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
63 TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
64 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
65 TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
66 ∎
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
67 } }
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
68
485
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
69 FICG : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
70 FICG {I} Γ = G ○ (FIA Γ)
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
71
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
72 FICF : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
73 FICF {I} Γ = F ○ (FIA Γ)
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
74
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
75 FINAT : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → NTrans I C (FICF Γ) (FICG Γ)
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
76 FINAT {I} Γ = record {
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
77 TMap = λ i → tmap i
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
78 ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
79 } where
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
80 tmap : (i : Obj I ) → Hom C (FObj (FICF Γ) i) (FObj (FICG Γ) i)
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
81 tmap i = hom (FObj Γ i )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
82 commute : {a b : Obj I} → {f : Hom I a b} → C [ C [ FMap (FICG Γ) f o tmap a ] ≈ C [ tmap b o FMap (FICF Γ) f ] ]
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
83 commute {a} {b} {f} = comm ( FMap Γ f )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
84
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
85 revΓ : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I CommaCategory
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
86 revΓ {I} Γ = record {
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
87 FObj = λ x → record {
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
88 obj = obj ( FObj Γ x )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
89 ; hom = TMap (FINAT Γ) x
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
90 }
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
91 ; FMap = λ {a} {b} f → record {
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
92 arrow = arrow ( FMap Γ f )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
93 ; comm = IsNTrans.commute ( isNTrans (FINAT Γ) )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
94 }
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
95 ; isFunctor = record {
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
96 identity = IsFunctor.identity ( isFunctor Γ )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
97 ; distr = IsFunctor.distr ( isFunctor Γ )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
98 ; ≈-cong = IsFunctor.≈-cong ( isFunctor Γ )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
99 }} where
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
100
483
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
101 NIC : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory )
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
102 (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) ) → NTrans I C ( K C I (FObj G (obj c)) ) (G ○ ( FIA Γ) )
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
103 NIC {I} Γ c ta = tb A I (FIA Γ) (obj c) ta G
483
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
104
484
fcae3025d900 fix Limit pu a0 and t0 in record definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 483
diff changeset
105 LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I )
485
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
106 → ( glimit : ( Γ : Functor I A )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
107 → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
108 → ( Γ : Functor I CommaCategory )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
109 → Limit C I (FICG Γ)
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
110 LimitC {I} comp glimit Γ = glimit (FIA Γ) (isLimit comp (FIA Γ))
483
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
111
485
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
112 revLimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
113 → ( glimit : ( Γ : Functor I A )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
114 → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
115 → ( Γ : Functor I CommaCategory )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
116 → Limit C I ( G ○ (FIA (revΓ Γ) ))
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
117 revLimitC {I} comp glimit Γ = glimit (FIA (revΓ Γ)) (isLimit comp (FIA (revΓ Γ )))
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
118
486
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
119
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
120 a0F : ( I : Category c₁ c₂ ℓ ) → (a1 : Obj A) → Functor I A
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
121 a0F I a1 = record {
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
122 FObj = λ x → a1
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
123 ; FMap = λ {a} {b} f → id1 A a1
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
124 ; isFunctor = record {
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
125 identity = let open ≈-Reasoning (A) in refl-hom
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
126 ; distr = let open ≈-Reasoning (A) in ( sym idL )
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
127 ; ≈-cong = λ _ → let open ≈-Reasoning (A) in refl-hom
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
128 }} where
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
129
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
130 t0F : ( I : Category c₁ c₂ ℓ ) → (a1 : Obj A )
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
131 → NTrans I A (K A I a1 ) (a0F I a1 )
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
132 t0F I a1 = record {
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
133 TMap = λ i → id1 A a1
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
134 ; isNTrans = record { commute = λ {a b f} → commute {a} {b} {f} }
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
135 } where
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
136 commute : {a b : Obj I} {f : Hom I a b} → A [
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
137 A [ FMap (a0F I a1 ) f o id1 A a1 ] ≈
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
138 A [ id1 A a1 o FMap (K A I a1) f ] ]
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
139 commute {a} {b} {f} = let open ≈-Reasoning (A) in begin
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
140 FMap (a0F I a1 ) f o id1 A a1
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
141 ≈⟨ idR ⟩
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
142 FMap (a0F I a1 ) f
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
143 ≈⟨⟩
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
144 id1 A a1
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
145 ≈⟨⟩
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
146 FMap (K A I a1) f
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
147 ≈↑⟨ idL ⟩
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
148 id1 A a1 o FMap (K A I a1) f
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
149 ∎
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
150
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
151 hoge : ( a : Obj A ) → ( I : Category c₁ c₂ ℓ ) → (comp : Complete A I ) → ∀ { i : Obj I } →
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
152 A [ A [ TMap ( limit-u comp (a0F I a)) i o limit (isLimit comp (a0F I a)) a (t0F I a) ] ≈ id1 A a ]
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
153 hoge a I comp {i} = t0f=t (isLimit comp (a0F I a))
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
154
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
155
485
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
156 commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
157 → ( glimit : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
158 → Obj CommaCategory
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
159 commaLimit {I} comp Γ glimit = record {
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 obj = limit-c comp (FIA Γ)
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 ; hom = limitHom
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 } where
486
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
163 frev : {i : Obj I } → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i))
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
164 frev {i} = TMap (t0 ( isLimit comp (FIA Γ))) i
485
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
165 tu : NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (FICG Γ)
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
166 tu = record {
486
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
167 TMap = λ i → C [ hom ( FObj Γ i ) o FMap F frev ]
485
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
168 ; isNTrans = {!!}
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
169 }
486
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
170 forward : Hom C (FObj G (limit-c comp (FIA Γ))) (a0 (LimitC comp glimit Γ))
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
171 forward = limit (LimitC comp glimit Γ) (FObj G (limit-c comp (FIA Γ)))
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
172 ( record { TMap = λ i → C [ FMap G frev o {!!} ] ; isNTrans = {!!} } )
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
173 rev : Hom C (a0 (LimitC comp glimit Γ)) (FObj G (limit-c comp (FIA Γ)))
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
174 rev = C [ FMap G {!!} o TMap (t0 (LimitC comp glimit Γ)) {!!} ]
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
486
56cf6581c5f6 add some lemma but no use
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
176 limitHom = C [ rev o limit (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
177
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory )
485
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
180 → ( glimit : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
181 → NTrans I CommaCategory (K CommaCategory I {!!}) Γ
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
182 commaNat {I} comp Γ gilmit = record {
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
183 TMap = λ x → {!!}
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184 ; isNTrans = record { commute = {!!} }
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 } where
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I )
485
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
189 → ( glimit : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
190 → ( Γ : Functor I CommaCategory )
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
191 → Limit CommaCategory I Γ
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
192 hasLimit {I} comp glimit Γ = record {
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
193 a0 = {!!} ;
da4486523f73 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 484
diff changeset
194 t0 = {!!} ;
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 limit = λ a t → {!!} ;
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196 t0f=t = λ {a t i } → {!!} ;
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 limit-uniqueness = λ {a} {t} f t=f → {!!}
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
198 }