Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 613:afddfebea797

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
t0f=t0 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Jun 2017 22:36:54 +0900
parents f924056bf08a
children e6be03d94284
comparison
equal deleted inserted replaced
612:f924056bf08a 613:afddfebea797
151 t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) (i : Obj I) 151 t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) (i : Obj I)
152 → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ≈ TMap t i ] 152 → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ≈ TMap t i ]
153 t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin 153 t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin
154 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ) x 154 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ) x
155 ≈⟨⟩ 155 ≈⟨⟩
156 (FMap (HomA A b) ( TMap (t0 lim) i)) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) 156 FMap (HomA A b) ( TMap (t0 lim) i) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
157 ≈⟨ {!!} ⟩ 157 ≈⟨⟩
158 FMap (HomA A b) (A [ TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) ]) (id1 A b ) 158 TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b )
159 ≈⟨ ? ⟩ 159 ≈⟨ cdr idR ⟩
160 FMap (HomA A b) (TMap t i x) (id1 A b ) 160 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t )
161 ≈⟨ {!!} ⟩ 161 ≈⟨ t0f=t (isLimit lim) ⟩
162 {!!} o TMap t i x 162 TMap (ta a x t) i
163 ≈⟨ idL ⟩ 163 ≈⟨⟩
164 TMap t i x 164 TMap t i x
165 ∎ )) 165 ∎ ))
166 166
167 167
168 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) 168 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)