Mercurial > hg > Members > kono > Proof > category
changeset 622:bd890a43ef5b
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Jun 2017 10:07:34 +0900 |
| parents | 19f31d22e790 |
| children | bed3be9a4168 |
| files | freyd2.agda |
| diffstat | 1 files changed, 27 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Thu Jun 22 08:56:32 2017 +0900 +++ b/freyd2.agda Fri Jun 23 10:07:34 2017 +0900 @@ -207,14 +207,23 @@ hom1 b = λ (x : Hom A a a ) → hom b x hom2 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → Hom A a a → Hom A a (obj b ) hom2 b x = hom b x + hom3 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → Hom A a (obj b ) + hom3 b = hom b (id1 A a) + hom4 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → Hom A a a → Hom A a (obj b ) + hom4 b x = A [ hom b (id1 A a) o x ] comm1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) (x : FObj (Yoneda A a ) a ) → A [ ( Sets [ FMap (Yoneda A a) (id1 A (obj b) ) o hom b ] ) x ≈ hom b x ] comm1 b x = let open ≈-Reasoning A in ≡-≈ ( cong ( λ k -> k x ) ( comm ( id1 (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a)) b ) ) ) -- hom b is Hom A a a → Hom A a (obj b) - -- hom b is Hom A a a → Hom A a (obj b) -- hom b x is ( x : Hom A a a ) → Hom A a (obj b) -- hom b (id1 A a) is ( id1 A a : Hom A a a ) → Hom A a (obj b) -- hom b (id1 A a) o x is ( x : Hom A a a ) → Hom A a (obj b) + -- x + -- a ----> a -> obj b hom b x + -- + -- x id + -- a ----> a -> obj b hom b (id a) o x + -- initial0comm1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → (x : FObj (Yoneda A a) a ) → FMap (Yoneda A a) (hom b (id1 A a)) x ≡ hom b x initial0comm1 b x = let open ≈-Reasoning A in ≈-≡ A ( begin @@ -222,8 +231,6 @@ ≈⟨⟩ hom b (id1 A a ) o x ≈⟨ {!!} ⟩ - ( Sets [ FMap (Yoneda A a) (id1 A (obj b) ) o hom b ] ) x - ≈⟨ comm1 b x ⟩ hom b x ∎ ) initial0comm : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → @@ -271,17 +278,20 @@ open SmallFullSubcategory open PreInitial - -UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - (U : Functor A (Sets {c₂}) ) - (a : Obj (Sets {c₂})) - (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) ) - (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U) (SFSF SFS )) - → Representable A U (obj (preinitialObj PI )) -UisRepresentable A U a SFS PI = record { - repr→ = record { TMap = {!!} ; isNTrans = record { commute = {!!} } } - ; repr← = record { TMap = {!!} ; isNTrans = record { commute = {!!} } } - ; reprId→ = λ {y} → ? - ; reprId← = λ {y} → ? - } - +-- +-- UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) +-- (U : Functor A (Sets {c₂}) ) +-- (a : Obj (Sets {c₂})) (ax : a) +-- (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) ) +-- (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U) (SFSF SFS )) +-- → Representable A U (obj (preinitialObj PI )) +-- UisRepresentable A U a ax SFS PI = record { +-- repr→ = record { TMap = tmap1 ; isNTrans = record { commute = {!!} } } +-- ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = {!!} } } +-- ; reprId→ = λ {y} → ? +-- ; reprId← = λ {y} → ? +-- } where +-- tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj (preinitialObj PI))) b) +-- tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) +-- tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b) +-- tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) ax )