Mercurial > hg > Members > kono > Proof > category
changeset 396:45ecb7b6c396
non nil dead end...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 16 Mar 2016 13:02:51 +0900 |
| parents | 2821b92e0dc9 |
| children | dd3fa0680897 |
| files | limit-to.agda |
| diffstat | 1 files changed, 66 insertions(+), 70 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Tue Mar 15 18:18:06 2016 +0900 +++ b/limit-to.agda Wed Mar 16 13:02:51 2016 +0900 @@ -29,7 +29,6 @@ id-t0 : Arrow arrow-f : Arrow arrow-g : Arrow - nil : Arrow record RawHom {c₁ ℓ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set (c₁ ⊔ ℓ) where field @@ -55,7 +54,7 @@ twocomp : {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Arrow {ℓ } twocomp id-t0 f = f twocomp f id-t0 = f -twocomp _ _ = nil +twocomp _ _ = arrow-f twocmp-associative : {ℓ : Level } -> ( f : Arrow {ℓ } ) -> ( g : Arrow {ℓ } ) -> ( h : Arrow {ℓ } ) → twocomp f (twocomp g h) ≡ twocomp (twocomp f g) h twocmp-associative id-t0 _ _ = refl @@ -63,41 +62,16 @@ twocmp-associative arrow-f arrow-f id-t0 = refl twocmp-associative arrow-f arrow-f arrow-f = refl twocmp-associative arrow-f arrow-f arrow-g = refl -twocmp-associative arrow-f arrow-f nil = refl twocmp-associative arrow-g id-t0 _ = refl -twocmp-associative arrow-f arrow-g nil = refl twocmp-associative arrow-f arrow-g id-t0 = refl twocmp-associative arrow-f arrow-g arrow-f = refl twocmp-associative arrow-f arrow-g arrow-g = refl -twocmp-associative arrow-f nil nil = refl -twocmp-associative arrow-f nil id-t0 = refl -twocmp-associative arrow-f nil arrow-f = refl -twocmp-associative arrow-f nil arrow-g = refl -twocmp-associative arrow-g arrow-f nil = refl twocmp-associative arrow-g arrow-f id-t0 = refl twocmp-associative arrow-g arrow-f arrow-f = refl twocmp-associative arrow-g arrow-f arrow-g = refl -twocmp-associative arrow-g arrow-g nil = refl twocmp-associative arrow-g arrow-g id-t0 = refl twocmp-associative arrow-g arrow-g arrow-f = refl twocmp-associative arrow-g arrow-g arrow-g = refl -twocmp-associative arrow-g nil nil = refl -twocmp-associative arrow-g nil id-t0 = refl -twocmp-associative arrow-g nil arrow-f = refl -twocmp-associative arrow-g nil arrow-g = refl -twocmp-associative nil id-t0 _ = refl -twocmp-associative nil nil nil = refl -twocmp-associative nil nil id-t0 = refl -twocmp-associative nil nil arrow-f = refl -twocmp-associative nil nil arrow-g = refl -twocmp-associative nil arrow-f nil = refl -twocmp-associative nil arrow-f id-t0 = refl -twocmp-associative nil arrow-f arrow-f = refl -twocmp-associative nil arrow-f arrow-g = refl -twocmp-associative nil arrow-g nil = refl -twocmp-associative nil arrow-g id-t0 = refl -twocmp-associative nil arrow-g arrow-f = refl -twocmp-associative nil arrow-g arrow-g = refl _×_ : { c₁ ℓ : Level } -> {A B C : TwoObject { c₁} } → Two-Hom { c₁} {ℓ} B C → Two-Hom { c₁} {ℓ} A B → Two-Hom { c₁} {ℓ} A C @@ -110,7 +84,6 @@ arrow-iso id-t0 = refl arrow-iso arrow-f = refl arrow-iso arrow-g = refl - arrow-iso nil = refl open Two-Hom @@ -137,13 +110,11 @@ identityL {_} {_} {f} | id-t0 = refl identityL {_} {_} {f} | arrow-f = refl identityL {_} {_} {f} | arrow-g = refl - identityL {_} {_} {f} | nil = refl identityR : {A B : TwoObject} {f : Two-Hom A B} → Map ( f × Two-id A ) ≡ Map f identityR {a} {b} {f} with Map f identityR {_} {_} {f} | id-t0 = refl identityR {_} {_} {f} | arrow-f = refl identityR {_} {_} {f} | arrow-g = refl - identityR {_} {_} {f} | nil = 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 @@ -166,16 +137,33 @@ Map ( (f × g) × h ) ∎ +-- +-- +-- f' +-- <----------- +-- -----------> +-- | f ^ g o fg = f +-- fg | | gf gf o g = f +-- v | f o gf'= g +-- -----------> gf'o f = g +-- g +-- +-- indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - ( a b : Obj A ) ( f g : Hom A a b ) ( nf : Hom A a b ) ( nf-rev : Hom A b a ) ( nidA : Hom A a a ) ( nidB : Hom A b b ) -> Functor (TwoCat {c₁} {c₂} {ℓ} ) A -indexFunctor {c₁} {c₂} {ℓ} A a b f g nf nf-rev nidA nidB = record { + ( a b : Obj A ) ( f g : Hom A a b ) ( f' : Hom A b a ) ( fg fg' : Hom A a a ) ( gf gf' : Hom A b b ) + ( f-iso : A [ A [ f o f' ] ≈ id1 A b ]) + ( f'-iso : A [ A [ f' o f ] ≈ id1 A a ]) + ( g-iso : A [ A [ g o f' ] ≈ id1 A b ]) + ( g'-iso : A [ A [ f' o g ] ≈ id1 A a ]) + -> Functor (TwoCat {c₁} {c₂} {ℓ} ) A +indexFunctor {c₁} {c₂} {ℓ} A a b f g f' fg fg' gf gf' f-iso f'-iso g-iso g'-iso = record { FObj = λ a → fobj a ; FMap = λ f → fmap f ; isFunctor = record { identity = \{x} -> identity {x} ; distr = \ {a} {b} {c} {f} {g} -> distr1 {a} {b} {c} {f} {g} - ; ≈-cong = {!!} + ; ≈-cong = \ {a} {b} {c} {f} -> ≈-cong {a} {b} {c} {f} } } where I = TwoCat {c₁} {c₂} {ℓ} @@ -184,13 +172,15 @@ fobj t1 = b fmap1 : {x y : Obj I } -> Arrow -> Hom A (fobj x) (fobj y) fmap1 {t0} {t1} arrow-f = f - fmap1 {t0} {t1} arrow-g = f + fmap1 {t0} {t1} arrow-g = g fmap1 {t0} {t0} id-t0 = id1 A a fmap1 {t1} {t1} id-t0 = id1 A b - fmap1 {t0} {t0} _ = id1 A a - fmap1 {t0} {t1} _ = nf - fmap1 {t1} {t0} _ = nf-rev - fmap1 {t1} {t1} _ = id1 A b + fmap1 {t0} {t0} arrow-f = fg + fmap1 {t0} {t0} arrow-g = fg' + fmap1 {t0} {t1} _ = f + fmap1 {t1} {t0} _ = f' + fmap1 {t1} {t1} arrow-f = gf + fmap1 {t1} {t1} arrow-g = gf' fmap : {x y : Obj I } -> Hom I x y -> Hom A (fobj x) (fobj y) fmap {x} {y} f = fmap1 {x} {y} ( Map f) open ≈-Reasoning (A) @@ -199,41 +189,47 @@ identity {t1} = refl-hom distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → A [ fmap (I [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ] distr1 {a1} {b1} {c} {f1} {g1} with Map f1 | Map g1 - distr1 {t0} {t1} {t0} {_} {_} | fa | arrow-f = begin - fmap1 (twocomp arrow-f fa) - ≈⟨⟩ - fmap1 nil + distr1 {t0} {t1} {t0} {_} {_} | arrow-f | arrow-f = {!!} + distr1 {t0} {t1} {t0} {_} {_} | arrow-f | arrow-g = {!!} + distr1 {t0} {t1} {t0} {_} {_} | arrow-f | id-t0 = {!!} + distr1 {t0} {t1} {t0} {_} {_} | arrow-g | arrow-f = {!!} + distr1 {t0} {t1} {t0} {_} {_} | arrow-g | arrow-g = {!!} + distr1 {t0} {t1} {t0} {_} {_} | arrow-g | id-t0 = {!!} + distr1 {t0} {t1} {t0} {_} {_} | id-t0 | arrow-f = {!!} + distr1 {t0} {t1} {t0} {_} {_} | id-t0 | arrow-g = {!!} + distr1 {t0} {t1} {t0} {_} {_} | id-t0 | id-t0 = sym f'-iso + distr1 {t1} {t0} {t1} {_} {_} | arrow-f | arrow-f = {!!} + distr1 {t1} {t0} {t1} {_} {_} | arrow-f | arrow-g = {!!} + distr1 {t1} {t0} {t1} {_} {_} | arrow-f | id-t0 = {!!} + distr1 {t1} {t0} {t1} {_} {_} | arrow-g | arrow-f = {!!} + distr1 {t1} {t0} {t1} {_} {_} | arrow-g | arrow-g = {!!} + distr1 {t1} {t0} {t1} {_} {_} | arrow-g | id-t0 = {!!} + distr1 {t1} {t0} {t1} {_} {_} | id-t0 | arrow-f = {!!} + distr1 {t1} {t0} {t1} {_} {_} | id-t0 | arrow-g = {!!} + distr1 {t1} {t0} {t1} {_} {_} | id-t0 | id-t0 = sym f-iso + distr1 {t0} {t0} {t0} {f1} {g1} | fa | id-t0 = sym idL + distr1 {t0} {t0} {t1} {f1} {g1} | arrow-f | id-t0 = {!!} + distr1 {t0} {t0} {t1} {f1} {g1} | arrow-g | id-t0 = begin + fmap1 {t0} {t1} arrow-g ≈⟨⟩ - id1 A b - ≈⟨ {!!} ⟩ - f o fmap1 fa - ≈⟨⟩ - fmap1 arrow-f o fmap1 fa - ∎ - distr1 {t0} {t1} {t0} {_} {_} | _ | _ = {!!} - distr1 {t1} {t0} {t1} {_} {_} | arrow-f | ga = begin - fmap1 (twocomp ga arrow-f) - ≈⟨⟩ - id1 A a + g ≈⟨ {!!} ⟩ - fmap1 ga o f - ≈⟨⟩ - fmap1 ga o fmap1 arrow-f + {!!} ∎ - distr1 {t1} {t0} {t1} {_} {_} | nil | ga = begin - fmap1 (twocomp ga nil ) - ≈⟨⟩ - id1 A a - ≈⟨ {!!} ⟩ - fmap1 ga o nf - ≈⟨⟩ - fmap1 ga o fmap1 nil - ∎ - distr1 {t1} {t0} {t1} {_} {_} | _ | _ = {!!} - distr1 {_} {_} {_} {_} {_} | _ | _ = {!!} - + distr1 {t0} {t0} {t1} {f1} {g1} | id-t0 | id-t0 = {!!} + distr1 {t0} {t0} {_} {f1} {g1} | fa | arrow-f = {!!} + distr1 {t0} {t0} {_} {f1} {g1} | fa | arrow-g = {!!} + distr1 {t1} {t1} {_} {f1} {g1} | id-t0 | ga = {!!} + distr1 {t1} {t1} {_} {f1} {g1} | arrow-f | ga = {!!} + distr1 {t1} {t1} {_} {f1} {g1} | arrow-g | ga = {!!} + distr1 {t1} {t0} {t0} {f1} {g1} | id-t0 | ga = {!!} + distr1 {t1} {t0} {t0} {_} {_} | arrow-f | ga = {!!} + distr1 {t1} {t0} {t0} {_} {_} | arrow-g | ga = {!!} + distr1 {t0} {t1} {t1} {_} {_} | id-t0 | ga = {!!} + distr1 {t0} {t1} {t1} {_} {_} | arrow-f | ga = {!!} + distr1 {t0} {t1} {t1} {_} {_} | arrow-g | ga = {!!} ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → A [ fmap f ≈ fmap g ] - ≈-cong {_} {_} {f1} {g1} f≈g = ≡-cong f≈g (\x -> fmap1 x) + ≈-cong {a} {b} {f1} {g1} f≈g = ≡-cong {_} {_} {_} {_} {_} {_} f≈g (\x -> fmap1 {a} {b} x) --- Equalizer @@ -261,7 +257,7 @@ ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' } where I = TwoCat {c₁} {c₂} {ℓ } - Γ = indexFunctor A a b f g nf nf-rev nidA nidB + Γ = indexFunctor A a b f g nf-rev {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} nmap : (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x) nmap x d h = {!!} commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) -> A [ A [ f o h ] ≈ A [ g o h ] ]