Mercurial > hg > Members > kono > Proof > category
changeset 294:db4ecbdbf9e9
limit1 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 25 Sep 2013 19:54:35 +0900 |
| parents | fb0ab8c72e15 |
| children | 26e8f0227ebd |
| files | pullback.agda |
| diffstat | 1 files changed, 19 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Wed Sep 25 19:34:10 2013 +0900 +++ b/pullback.agda Wed Sep 25 19:54:35 2013 +0900 @@ -486,7 +486,25 @@ TMap = tfmap a t ; isNTrans = record { commute = λ {a'} {b} {f} → let open ≈-Reasoning (B) in begin FMap Γ f o tfmap a t a' - ≈⟨ {!!} ⟩ + ≈⟨⟩ + FMap Γ f o ( TMap ε (FObj Γ a') o FMap F (TMap t a')) + ≈⟨ assoc ⟩ + (FMap Γ f o TMap ε (FObj Γ a') ) o FMap F (TMap t a') + ≈⟨ car (nat ε) ⟩ + (TMap ε (FObj Γ b) o FMap (F ○ U) (FMap Γ f) ) o FMap F (TMap t a') + ≈↑⟨ assoc ⟩ + TMap ε (FObj Γ b) o ( FMap (F ○ U) (FMap Γ f) o FMap F (TMap t a') ) + ≈↑⟨ cdr ( distr F ) ⟩ + TMap ε (FObj Γ b) o ( FMap F (A [ FMap U (FMap Γ f) o TMap t a' ] ) ) + ≈⟨ cdr ( fcong F (nat t) ) ⟩ + TMap ε (FObj Γ b) o FMap F (A [ TMap t b o FMap (K A I a) f ]) + ≈⟨⟩ + TMap ε (FObj Γ b) o FMap F (A [ TMap t b o id1 A (FObj (K A I a) b) ]) + ≈⟨ cdr ( fcong F (IsCategory.identityR (Category.isCategory A))) ⟩ + TMap ε (FObj Γ b) o FMap F (TMap t b ) + ≈↑⟨ idR ⟩ + ( TMap ε (FObj Γ b) o FMap F (TMap t b)) o id1 B (FObj F (FObj (K A I a) b)) + ≈⟨⟩ tfmap a t b o FMap (K B I (FObj F a)) f ∎ } }