Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 614:e6be03d94284

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Representational Functor preserve limit done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Jun 2017 22:53:44 +0900
parents afddfebea797
children a45c32ceca97
comparison
equal deleted inserted replaced
613:afddfebea797 614:e6be03d94284
118 (Γ : Functor I A) (limita : Limit A I Γ) → 118 (Γ : Functor I A) (limita : Limit A I Γ) →
119 IsLimit Sets I (HomA A b ○ Γ) (FObj (HomA A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) 119 IsLimit Sets I (HomA A b ○ Γ) (FObj (HomA A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b))
120 UpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { 120 UpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record {
121 limit = λ a t → ψ a t 121 limit = λ a t → ψ a t
122 ; t0f=t = λ {a t i} → t0f=t0 a t i 122 ; t0f=t = λ {a t i} → t0f=t0 a t i
123 ; limit-uniqueness = λ {b} {t} {f} t0f=t → {!!} 123 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t
124 } where 124 } where
125 hat0 : NTrans I Sets (K Sets I (FObj (HomA A b) (a0 lim))) (HomA A b ○ Γ) 125 hat0 : NTrans I Sets (K Sets I (FObj (HomA A b) (a0 lim))) (HomA A b ○ Γ)
126 hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b) 126 hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)
127 haa0 : Obj Sets 127 haa0 : Obj Sets
128 haa0 = FObj (HomA A b) (a0 lim) 128 haa0 = FObj (HomA A b) (a0 lim)
160 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) 160 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t )
161 ≈⟨ t0f=t (isLimit lim) ⟩ 161 ≈⟨ t0f=t (isLimit lim) ⟩
162 TMap (ta a x t) i 162 TMap (ta a x t) i
163 ≈⟨⟩ 163 ≈⟨⟩
164 TMap t i x 164 TMap t i x
165 ∎ ))
166 limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)} {f : Hom Sets a (FObj (HomA A b) (a0 lim))} →
167 ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o f ] ≈ TMap t i ]) →
168 Sets [ ψ a t ≈ f ]
169 limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin
170 ψ a t x
171 ≈⟨⟩
172 FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )
173 ≈⟨⟩
174 limit (isLimit lim) b (ta a x t ) o id1 A b
175 ≈⟨ idR ⟩
176 limit (isLimit lim) b (ta a x t )
177 ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≡-≈ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩
178 f x
165 ∎ )) 179 ∎ ))
166 180
167 181
168 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) 182 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
169 (b : Obj A ) → LimitPreserve A I Sets (HomA A b) 183 (b : Obj A ) → LimitPreserve A I Sets (HomA A b)