Mercurial > hg > Members > kono > Proof > category
diff freyd1.agda @ 495:633df882db86
fryed1 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 14 Mar 2017 13:08:03 +0900 |
| parents | ba6a67523523 |
| children | 5c7908202d5a |
line wrap: on
line diff
--- a/freyd1.agda Tue Mar 14 12:14:57 2017 +0900 +++ b/freyd1.agda Tue Mar 14 13:08:03 2017 +0900 @@ -166,10 +166,10 @@ TMap (limit-u comp (FIA Γ)) b o FMap (K A I (limit-c comp (FIA Γ))) f ∎ -gnat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → +gnat : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) + → (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ) -gnat {I} comp Γ glimit a t = record { +gnat {I} Γ a t = record { TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ] ; isNTrans = record { commute = λ {x y f} → comm1 x y f } } where @@ -209,12 +209,24 @@ ≈ C [ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ] ] comm1 = let open ≈-Reasoning (C) in begin FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a - ≈⟨ {!!} ⟩ - limit (isLimit (LimitC comp Γ glimit )) (FObj F (obj a)) (gnat comp Γ glimit a t ) - ≈⟨ limit-uniqueness (isLimit (LimitC comp Γ glimit )) - (limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) - o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) - ) ( λ {i} → begin + ≈↑⟨ limit-uniqueness (isLimit (LimitC comp Γ glimit )) ( λ {i} → begin + TMap (t0 (LimitC comp Γ glimit)) i o ( FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ) + ≈⟨ assoc ⟩ + ( TMap (t0 (LimitC comp Γ glimit)) i o FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o hom a + ≈⟨⟩ + ( FMap G ( TMap (limit-u comp (FIA Γ )) i ) o FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o hom a + ≈↑⟨ car ( distr G ) ⟩ + FMap G ( A [ TMap (limit-u comp (FIA Γ )) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] ) o hom a + ≈⟨ car ( fcong G ( t0f=t (isLimit (climit comp (FIA Γ ))))) ⟩ + FMap G (arrow (TMap t i)) o hom a + ≈⟨ comm ( TMap t i) ⟩ + hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) + ≈⟨⟩ + TMap (gnat Γ a t) i + ∎ + ) ⟩ + limit (isLimit (LimitC comp Γ glimit )) (FObj F (obj a)) (gnat Γ a t ) + ≈⟨ limit-uniqueness (isLimit (LimitC comp Γ glimit )) ( λ {i} → begin TMap (t0 (LimitC comp Γ glimit )) i o ( limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ) @@ -235,8 +247,8 @@ FMap F ( A [ TMap (t0 ( climit comp (FIA Γ))) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] ) ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) - ≈⟨ {!!} ⟩ - TMap {!!} i + ≈⟨⟩ + TMap (gnat Γ a t ) i ∎ ) ⟩ limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) @@ -261,7 +273,7 @@ → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ] comma-uniqueness {I} comp Γ glimit a t f t=f = let open ≈-Reasoning (A) in begin limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) - ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) (arrow f) t=f ⟩ + ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) t=f ⟩ arrow f ∎ @@ -275,6 +287,6 @@ isLimit = record { limit = λ a t → comma-a0 comp Γ glimit a t ; t0f=t = λ {a t i } → comma-t0f=t comp Γ glimit a t i ; - limit-uniqueness = λ {a} {t} f t=f → comma-uniqueness {I} comp Γ glimit a t f t=f + limit-uniqueness = λ {a} {t} {f} t=f → comma-uniqueness {I} comp Γ glimit a t f t=f } }