Mercurial > hg > Members > kono > Proof > category
diff limit-to.agda @ 387:2f59c2db9d98
what is this ?
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 14 Mar 2016 20:33:58 +0900 |
| parents | 1e136aaad5cb |
| children | a0ab2643eee7 |
line wrap: on
line diff
--- a/limit-to.agda Mon Mar 14 17:44:45 2016 +0900 +++ b/limit-to.agda Mon Mar 14 20:33:58 2016 +0900 @@ -18,16 +18,7 @@ --- 0 1 --- ------> --- g ---- f ---- e ------> ---- c ------> a b ---- ^ / ------> ---- |k h g ---- | / ---- | / ---- | / ---- |/ ---- d + data TwoObject {c₁ : Level} : Set c₁ where @@ -36,85 +27,39 @@ data Arrow {ℓ : Level } : Set ℓ where id-t0 : Arrow - id-t1 : Arrow arrow-f : Arrow arrow-g : Arrow record RawHom {c₁ ℓ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set (c₁ ⊔ ℓ) where field RawMap : Maybe ( Arrow {ℓ }) - RawSel : Maybe ( TwoObject {c₁} ) open RawHom -arrow2hom : {c₁ ℓ : Level} (a b : TwoObject {c₁} ) -> Maybe (Arrow {ℓ} ) -> RawHom {c₁} {ℓ} a b -arrow2hom {_} {_} t0 t0 (just id-t0) = record { RawMap = just id-t0 ; RawSel = just t0 } -arrow2hom {_} {_} t0 t1 (just arrow-f) = record { RawMap = just arrow-f ; RawSel = just t0 } -arrow2hom {_} {_} t0 t1 (just arrow-g) = record { RawMap = just arrow-g ; RawSel = just t1 } -arrow2hom {_} {_} t1 t1 (just id-t1) = record { RawMap = just id-t1 ; RawSel = just t0 } -arrow2hom {_} {_} a b _ = record { RawMap = nothing ; RawSel = nothing } - - record Two-Hom { c₁ ℓ : Level } (a : TwoObject { c₁} ) (b : TwoObject { c₁} ) : Set (c₁ ⊔ ℓ) where field hom : RawHom { c₁} {ℓ } a b - two-hom-iso : arrow2hom a b (RawMap hom) ≡ hom Map : Maybe Arrow Map = RawMap hom - Sel : Maybe TwoObject - Sel = RawSel hom Two-id : {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) -> Two-Hom {c₁} { ℓ} a a -Two-id t0 = record { hom = record { RawMap = just id-t0 ; RawSel = just t0 } ; two-hom-iso = refl } -Two-id t1 = record { hom = record { RawMap = just id-t1 ; RawSel = just t0 } ; two-hom-iso = refl } +Two-id t0 = record { hom = record { RawMap = just id-t0 } } +Two-id t1 = record { hom = record { RawMap = just id-t0 } } Two-nothing : {c₁ ℓ : Level } -> ( a b : TwoObject {c₁} ) -> Two-Hom {c₁} { ℓ} a b -Two-nothing a b = record { hom = record { RawMap = nothing ; RawSel = nothing } ; two-hom-iso = nothing-iso a b } - where - nothing-iso : (a b : TwoObject ) -> arrow2hom a b nothing ≡ record { RawMap = nothing ; RawSel = nothing } - nothing-iso t0 t0 = refl - nothing-iso t0 t1 = refl - nothing-iso t1 t0 = refl - nothing-iso t1 t1 = refl +Two-nothing a b = record { hom = record { RawMap = nothing } } open Two-Hom -- arrow composition twocomp : {ℓ : Level } -> Maybe (Arrow {ℓ }) -> Maybe (Arrow {ℓ }) -> Maybe (Arrow {ℓ } ) -twocomp (just arrow-f) (just id-t0) = just arrow-f -twocomp (just arrow-g) (just id-t0) = just arrow-g -twocomp (just id-t1) (just arrow-f) = just arrow-f -twocomp (just id-t1) (just arrow-g) = just arrow-g -twocomp (just id-t0) (just id-t0) = just id-t0 -twocomp (just id-t1) (just id-t1) = just id-t1 +twocomp (just id-t0) (just f) = just f +twocomp (just f) (just id-t0) = just f twocomp _ _ = nothing _×_ : { c₁ ℓ : Level } -> {A B C : TwoObject { c₁} } → Two-Hom { c₁} {ℓ} B C → Two-Hom { c₁} {ℓ} A B → Two-Hom { c₁} {ℓ} A C -_×_ { c₁} {ℓ} {a} {b} {c} f g = record { hom = arrow2hom a c ( twocomp (Map f) (Map g) ); two-hom-iso = comp-iso a c } - where - comp-iso : (a c : TwoObject ) → arrow2hom a c (RawMap (arrow2hom a c (twocomp (Map f) (Map g)))) ≡ arrow2hom a c (twocomp (Map f) (Map g)) - comp-iso a c with (twocomp (Map f) (Map g)) - comp-iso t0 t0 | nothing = refl - comp-iso t0 t1 | nothing = refl - comp-iso t1 t0 | nothing = refl - comp-iso t1 t1 | nothing = refl - comp-iso t0 t0 | just id-t0 = refl - comp-iso t0 t1 | just id-t0 = refl - comp-iso t1 t0 | just id-t0 = refl - comp-iso t1 t1 | just id-t0 = refl - comp-iso t0 t0 | just id-t1 = refl - comp-iso t0 t1 | just id-t1 = refl - comp-iso t1 t0 | just id-t1 = refl - comp-iso t1 t1 | just id-t1 = refl - comp-iso t1 t1 | just arrow-f = refl - comp-iso t0 t0 | just arrow-f = refl - comp-iso t0 t1 | just arrow-f = refl - comp-iso t1 t0 | just arrow-f = refl - comp-iso t1 t1 | just arrow-g = refl - comp-iso t0 t0 | just arrow-g = refl - comp-iso t0 t1 | just arrow-g = refl - comp-iso t1 t0 | just arrow-g = refl +_×_ { c₁} {ℓ} {a} {b} {c} f g = record { hom = record { RawMap = twocomp (Map f) (Map g) }} TwoCat : { c₁ c₂ ℓ : Level } -> Category c₁ (ℓ ⊔ c₁) ℓ @@ -140,38 +85,78 @@ identityL {t0} {t1} {f} | nothing = refl identityL {t1} {t0} {f} | nothing = refl identityL {t1} {t1} {f} | nothing = refl - identityL {t1} {t1} {f} | just id-t1 = refl + identityL {t1} {t1} {f} | just id-t0 = refl identityL {t0} {t1} {f} | just arrow-f = refl identityL {t0} {t1} {f} | just arrow-g = refl identityL {t0} {t0} {f} | just id-t0 = refl - identityL {a} {b} {f} | just fa = let open ≡-Reasoning in - begin - RawMap (arrow2hom a b (twocomp (RawMap (hom (Two-id b))) (just fa))) - ≡⟨ {!!} ⟩ - just fa - ∎ + identityL {a} {t0} {f} | just fa = refl + identityL {a} {t1} {f} | just fa = refl identityR : {A B : TwoObject} {f : Two-Hom A B} → Map ( f × Two-id A ) ≡ Map f - identityR {a} {b} {f} = let open ≡-Reasoning in - begin - {!!} - ≡⟨ {!!} ⟩ - {!!} - ∎ + identityR {a} {b} {f} with Map f + identityR {t0} {t0} {f} | nothing = refl + identityR {t0} {t1} {f} | nothing = refl + identityR {t1} {t0} {f} | nothing = refl + identityR {t1} {t1} {f} | nothing = refl + identityR {t1} {t1} {f} | just id-t0 = refl + identityR {t0} {t1} {f} | just arrow-f = refl + identityR {t0} {t1} {f} | just arrow-g = refl + identityR {t0} {t0} {f} | just id-t0 = refl + identityR {t0} {_} {f} | just id-t0 = refl + identityR {t0} {_} {f} | just arrow-f = refl + identityR {t0} {_} {f} | just arrow-g = refl + identityR {t1} {_} {f} | just id-t0 = refl + identityR {t1} {_} {f} | just arrow-f = refl + identityR {t1} {_} {f} | just arrow-g = refl o-resp-≈ : {A B C : TwoObject} {f g : Two-Hom A B} {h i : Two-Hom B C} → Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g ) o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = let open ≡-Reasoning in begin - {!!} - ≡⟨ {!!} ⟩ - Map (i × g) + Map (h × f) + ≡⟨⟩ + twocomp (Map h) (Map f) + ≡⟨ ≡-cong (\x -> twocomp (Map h) x ) f≡g ⟩ + twocomp (Map h) (Map g) + ≡⟨ ≡-cong (\x -> twocomp x (Map g) ) h≡i ⟩ + twocomp (Map i) (Map g) + ≡⟨⟩ + Map (i × g) ∎ associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h ) - associative {_} {_} {_} {_} {f} {g} {h} = let open ≡-Reasoning in - begin - Map ( f × (g × h) ) - ≡⟨ {!!} ⟩ - Map ( (f × g) × h ) - ∎ + associative {_} {_} {_} {_} {f} {g} {h} with Map f | Map g | Map h + associative {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ = refl + associative {_} {_} {_} {_} {f} {g} {h} | just id-t0 | nothing | _ = refl + associative {_} {_} {_} {_} {f} {g} {h} | just arrow-f | nothing | _ = refl + associative {_} {_} {_} {_} {f} {g} {h} | just arrow-g | nothing | _ = refl + associative {_} {_} {_} {_} {f} {g} {h} | just id-t0 | just id-t0 | nothing = refl + associative {_} {_} {_} {_} {f} {g} {h} | just id-t0 | just arrow-f | nothing = refl + associative {_} {_} {_} {_} {f} {g} {h} | just id-t0 | just arrow-g | nothing = refl + associative {_} {_} {_} {_} {f} {g} {h} | just arrow-f | just id-t0 | nothing = refl + associative {_} {_} {_} {_} {f} {g} {h} | just arrow-f | just arrow-f | nothing = refl + associative {_} {_} {_} {_} {f} {g} {h} | just arrow-f | just arrow-g | nothing = refl + associative {_} {_} {_} {_} {f} {g} {h} | just arrow-g | just id-t0 | nothing = refl + associative {_} {_} {_} {_} {f} {g} {h} | just arrow-g | just arrow-f | nothing = refl + associative {_} {_} {_} {_} {f} {g} {h} | just arrow-g | just arrow-g | nothing = refl + associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just id-t0 | just h = refl + associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-f | just id-t0 = refl + associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-g | just id-t0 = refl + associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-f | just arrow-f = refl + associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-f | just arrow-g = refl + associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-g | just arrow-f = refl + associative {_} {_} {_} {_} {_} {_} {_} | just id-t0 | just arrow-g | just arrow-g = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just id-t0 | just h = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-f | just id-t0 = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-f | just arrow-f = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-f | just arrow-g = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-g | just id-t0 = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-g | just arrow-f = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-f | just arrow-g | just arrow-g = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just id-t0 | just h = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-f | just id-t0 = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-f | just arrow-f = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-f | just arrow-g = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-g | just id-t0 = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-g | just arrow-f = refl + associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-g | just arrow-g = refl indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A ) ( f g : Hom A a b ) -> Functor TwoCat A @@ -193,7 +178,7 @@ fmap {t0} {t1} x | just arrow-f = f fmap {t0} {t1} x | just arrow-g = g fmap {t0} {t0} x | just id-t0 = id1 A a - fmap {t1} {t1} x | just id-t1 = id1 A b + fmap {t1} {t1} x | just id-t0 = id1 A b fmap {_} {_} x | _ = {!!} identity : {x : Obj I} → A [ fmap (id1 I x) ≈ id1 A (fobj x) ] identity = {!!} @@ -202,6 +187,18 @@ ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → A [ fmap f ≈ fmap g ] ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in {!!} +--- Equalizer +--- f +--- e ------> +--- c ------> a b +--- ^ / ------> +--- |k h g +--- | / +--- | / +--- | / +--- |/ +--- d + open Limit lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)