Mercurial > hg > Members > kono > Proof > category
changeset 490:1a42f06e7ae1
commaNat done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 13 Mar 2017 09:51:44 +0900 |
| parents | 75a60ceb55af |
| children | 04da2c458d44 |
| files | freyd1.agda |
| diffstat | 1 files changed, 4 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd1.agda Sun Mar 12 22:10:54 2017 +0900 +++ b/freyd1.agda Mon Mar 13 09:51:44 2017 +0900 @@ -46,9 +46,6 @@ FICG : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C FICG {I} Γ = G ○ (FIA Γ) -FICF : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C -FICF {I} Γ = F ○ (FIA Γ) - open LimitPreserve LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) @@ -136,10 +133,10 @@ comm2 : {a b : Obj I} {f : Hom I a b} → CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ] ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f ] ] - comm2 {a} {b} {f} = let open ≈-Reasoning (CommaCategory) in begin - FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } - ≈⟨ {!!} ⟩ - record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f + comm2 {a} {b} {f} = let open ≈-Reasoning (A) in begin + FMap (FIA Γ) f o TMap (limit-u comp (FIA Γ)) a + ≈⟨ IsNTrans.commute (isNTrans (limit-u comp (FIA Γ))) ⟩ + TMap (limit-u comp (FIA Γ)) b o FMap (K A I (limit-c comp (FIA Γ))) f ∎