Mercurial > hg > Members > kono > Proof > category

comparison freyd1.agda @ 484:fcae3025d900

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Limit pu a0 and t0 in record definition
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Mar 2017 16:38:08 +0900
parents 265f13adf93b
children da4486523f73
comparison
equal deleted inserted replaced
483:265f13adf93b 484:fcae3025d900
14 14
15 open import Category.Cat 15 open import Category.Cat
16 16
17 open NTrans 17 open NTrans
18 18
19
20 tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B )
21 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) →
22 ( U : Functor B C) → NTrans I C ( K C I (FObj U lim) ) (U ○ Γ)
23 tb B I Γ lim tb U = record {
24 TMap = TMap (Functor*Nat I C U tb) ;
25 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin
26 FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a
27 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
28 TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f
29 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
30 TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
31 ∎
32 } }
33 19
34 open Complete 20 open Complete
35 open CommaObj 21 open CommaObj
36 open CommaHom 22 open CommaHom
37 open Limit 23 open Limit
64 } where 50 } where
65 comm1 : {a b : Obj I} {f : Hom I a b} → 51 comm1 : {a b : Obj I} {f : Hom I a b} →
66 A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ] 52 A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ]
67 comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta ) 53 comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta )
68 54
55 tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B )
56 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) →
57 ( U : Functor B C) → NTrans I C ( K C I (FObj U lim) ) (U ○ Γ)
58 tb B I Γ lim tb U = record {
59 TMap = TMap (Functor*Nat I C U tb) ;
60 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin
61 FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a
62 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
63 TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f
64 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
65 TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
66 ∎
67 } }
68
69 FIC : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C
70 FIC {I} Γ = G ○ (FIA Γ)
71
69 NIC : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) 72 NIC : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory )
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 Γ) ) 73 (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 Γ) )
71 NIC {I} Γ c ta = record { 74 NIC {I} Γ c ta = tb A I (FIA Γ) (obj c) ta G
72 TMap = λ x → FMap G (TMap ta x )
73 ; isNTrans = record { commute = comm1 }
74 } where
75 comm1 : {a b : Obj I} {f : Hom I a b} →
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 ] ]
77 comm1 {a} {b} {f} = let open ≈-Reasoning (C) in begin
78 FMap (G ○ FIA Γ) f o FMap G (TMap ta a)
79 ≈↑⟨ distr G ⟩
80 FMap G ( A [ FMap (FIA Γ) f o TMap ta a ] )
81 ≈⟨ fcong G ( nat ta ) ⟩
82 FMap G ( A [ TMap ta b o FMap (K A I (obj c)) f ] )
83 ≈⟨ distr G ⟩
84 FMap G (TMap ta b) o FMap G (FMap (K A I (obj c)) f )
85 ≈⟨ cdr ( IsFunctor.identity (isFunctor G )) ⟩
86 FMap G (TMap ta b) o id1 C (FObj G (obj c))
87 ≈⟨⟩
88 FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f
89 ∎
90 75
91 76 LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I )
92 NIComma : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) 77 → ( Glimit : ( Γ : Functor I A ) (lim : Obj A )
93 (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) ) → NTrans I CommaCategory ( K CommaCategory I c ) Γ 78 → ( limita : Limit A I Γ lim ta ) → Limit C I (G ○ Γ) (FObj G lim) (tb A I Γ lim ta G ) )
94 NIComma {I} Γ c ta = record { 79 → ( lim : Obj CommaCategory ) → ( Γ : Functor I CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I ? ) Γ )
95 TMap = λ x → record { 80 → Limit C I (FIC Γ) {!!} ( NIC Γ {!!} (NIA Γ {!!} ta) )
96 arrow = TMap ta x 81 LimitC {I} comp Glimit lim Γ ta = Glimit (FIA Γ) {!!} (NIA Γ {!!} ta ) (isLimit comp (FIA Γ))
97 ; comm = comm1 x
98 }
99 ; isNTrans = record { commute = {!!} }
100 } where
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) ] ]
102 comm1 x = let open ≈-Reasoning (C) in begin
103 FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x)
104 ≈⟨ {!!} ⟩
105 hom (FObj Γ x) o FMap F (TMap ta x)
106 ∎
107
108
109 82
110 commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) → Obj CommaCategory 83 commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) → Obj CommaCategory
111 commaLimit {I} comp Γ = record { 84 commaLimit {I} comp Γ = record {
112 obj = limit-c comp (FIA Γ) 85 obj = limit-c comp (FIA Γ)
113 ; hom = limitHom 86 ; hom = limitHom
114 } where 87 } where
115 ll = ( limit (isLimit comp (FIA Γ)) (limit-c comp (FIA Γ)) {!!}) 88 ll = ( limit (isLimit comp (FIA Γ)) (limit-c comp (FIA Γ)) (NIA Γ {!!} {!!} ))
116 limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) 89 limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
117 limitHom = C [ FMap G ll o C [ {!!} o FMap F ll ] ] 90 limitHom = {!!}
118 91
119 92
120 commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) 93 commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory )
121 → (c : Obj CommaCategory ) 94 → (c : Obj CommaCategory )
122 → ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ ) 95 → ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ )
125 TMap = λ x → tmap x 98 TMap = λ x → tmap x
126 ; isNTrans = record { commute = {!!} } 99 ; isNTrans = record { commute = {!!} }
127 } where 100 } where
128 tmap : (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I c) i) (FObj Γ i) 101 tmap : (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I c) i) (FObj Γ i)
129 tmap i = record { 102 tmap i = record {
130 arrow = A [ arrow ( TMap ta i) o A [ {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ] 103 arrow = A [ arrow ( TMap ta i) o A [ {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ]
131 ; comm = {!!} 104 ; comm = {!!}
132 } 105 }
133 commute : {a b : Obj I} {f : Hom I a b} → 106 commute : {a b : Obj I} {f : Hom I a b} →
134 CommaCategory [ CommaCategory [ FMap Γ f o tmap a ] ≈ CommaCategory [ tmap b o FMap (K CommaCategory I c) f ] ] 107 CommaCategory [ CommaCategory [ FMap Γ f o tmap a ] ≈ CommaCategory [ tmap b o FMap (K CommaCategory I c) f ] ]
135 commute {a} {b} {f} = {!!} 108 commute {a} {b} {f} = {!!}