Mercurial > hg > Members > kono > Proof > category

annotate freyd1.agda @ 483:265f13adf93b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add NIC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Mar 2017 10:51:12 +0900
parents fd752ad25ac0
children fcae3025d900
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 tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B )
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) →
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 ( U : Functor B C) → NTrans I C ( K C I (FObj U lim) ) (U ○ Γ)
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 tb B I Γ lim tb U = record {
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 TMap = TMap (Functor*Nat I C U tb) ;
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 ∎
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 } }
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 open Complete
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 open CommaObj
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 open CommaHom
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 open Limit
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
483
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
39 -- F : A → C
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
40 -- G : A → C
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
41 --
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
42
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 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
44 FIA {I} Γ = record {
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
45 FObj = λ x → obj (FObj Γ x ) ;
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
46 FMap = λ {a} {b} f → arrow (FMap Γ f ) ;
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
47 isFunctor = record {
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
48 identity = identity
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
49 ; distr = IsFunctor.distr (isFunctor Γ)
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
50 ; ≈-cong = IsFunctor.≈-cong (isFunctor Γ)
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
51 }} where
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
52 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
53 identity {x} = let open ≈-Reasoning (A) in begin
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
54 arrow (FMap Γ (id1 I x))
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
55 ≈⟨ IsFunctor.identity (isFunctor Γ) ⟩
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
56 id1 A (obj (FObj Γ x))
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
57 ∎
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
59 NIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory )
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
60 (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
61 NIA {I} Γ c ta = record {
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
62 TMap = λ x → arrow (TMap ta x )
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
63 ; isNTrans = record { commute = comm1 }
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
64 } where
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
65 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
66 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
67 comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta )
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
68
483
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
69 NIC : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory )
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
70 (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 Γ) )
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
71 NIC {I} Γ c ta = record {
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
72 TMap = λ x → FMap G (TMap ta x )
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
73 ; isNTrans = record { commute = comm1 }
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
74 } where
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
75 comm1 : {a b : Obj I} {f : Hom I a b} →
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
76 C [ C [ FMap (G ○ FIA Γ) f o FMap G (TMap ta a) ] ≈ C [ FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f ] ]
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
77 comm1 {a} {b} {f} = let open ≈-Reasoning (C) in begin
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
78 FMap (G ○ FIA Γ) f o FMap G (TMap ta a)
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
79 ≈↑⟨ distr G ⟩
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
80 FMap G ( A [ FMap (FIA Γ) f o TMap ta a ] )
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
81 ≈⟨ fcong G ( nat ta ) ⟩
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
82 FMap G ( A [ TMap ta b o FMap (K A I (obj c)) f ] )
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
83 ≈⟨ distr G ⟩
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
84 FMap G (TMap ta b) o FMap G (FMap (K A I (obj c)) f )
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
85 ≈⟨ cdr ( IsFunctor.identity (isFunctor G )) ⟩
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
86 FMap G (TMap ta b) o id1 C (FObj G (obj c))
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
87 ≈⟨⟩
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
88 FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
89 ∎
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
90
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
91
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
92 NIComma : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory )
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
93 (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) ) → NTrans I CommaCategory ( K CommaCategory I c ) Γ
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
94 NIComma {I} Γ c ta = record {
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
95 TMap = λ x → record {
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
96 arrow = TMap ta x
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
97 ; comm = comm1 x
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
98 }
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
99 ; isNTrans = record { commute = {!!} }
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
100 } where
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
101 comm1 : ( x : Obj I ) → C [ C [ FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x) ] ≈ C [ hom (FObj Γ x) o FMap F (TMap ta x) ] ]
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
102 comm1 x = let open ≈-Reasoning (C) in begin
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
103 FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x)
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
104 ≈⟨ {!!} ⟩
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
105 hom (FObj Γ x) o FMap F (TMap ta x)
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
106 ∎
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
107
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
108
265f13adf93b add NIC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 482
diff changeset
109
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
110 commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) → Obj CommaCategory
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 commaLimit {I} comp Γ = record {
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 obj = limit-c comp (FIA Γ)
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 ; hom = limitHom
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 } where
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
115 ll = ( limit (isLimit comp (FIA Γ)) (limit-c comp (FIA Γ)) {!!})
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
117 limitHom = C [ FMap G ll o C [ {!!} o FMap F ll ] ]
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory )
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
121 → (c : Obj CommaCategory )
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
122 → ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ )
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
123 → NTrans I CommaCategory (K CommaCategory I c) Γ
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
124 commaNat {I} comp Γ c ta = record {
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 TMap = λ x → tmap x
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 ; isNTrans = record { commute = {!!} }
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 } where
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
128 tmap : (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I c) i) (FObj Γ i)
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 tmap i = record {
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
130 arrow = A [ arrow ( TMap ta i) o A [ {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ]
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 ; comm = {!!}
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 }
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 commute : {a b : Obj I} {f : Hom I a b} →
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
134 CommaCategory [ CommaCategory [ FMap Γ f o tmap a ] ≈ CommaCategory [ tmap b o FMap (K CommaCategory I c) f ] ]
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 commute {a} {b} {f} = {!!}
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I )
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 → ( G-preserve-limit : ( Γ : Functor I A )
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 ( lim : Obj A ) ( ta : NTrans I A ( K A I lim ) Γ ) → ( limita : Limit A I Γ lim ta ) → Limit C I (G ○ Γ) (FObj G lim) (tb A I Γ lim ta G ) )
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 → ( Γ : Functor I CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I (commaLimit comp Γ) ) Γ )
482
fd752ad25ac0 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 481
diff changeset
142 → Limit CommaCategory I Γ (commaLimit comp Γ ) ( commaNat comp Γ (commaLimit comp Γ) ta )
481
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 hasLimit {I} comp gpresrve Γ ta = record {
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 limit = λ a t → {!!} ;
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 t0f=t = λ {a t i } → {!!} ;
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 limit-uniqueness = λ {a} {t} f t=f → {!!}
65e6906782bb Completeness of Comma Category begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 }