Mercurial > hg > Members > kono > Proof > category
diff discrete.agda @ 455:55a9b6177ed4
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 Mar 2017 14:58:40 +0900 |
| parents | 2f07f4dd9a6d |
| children | 4d97955ea419 |
line wrap: on
line diff
--- a/discrete.agda Thu Mar 02 13:25:05 2017 +0900 +++ b/discrete.agda Thu Mar 02 14:58:40 2017 +0900 @@ -26,17 +26,14 @@ --- -----→ --- g -data Arrow {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where - id-t0 : Arrow t0 t0 - id-t1 : Arrow t1 t1 - arrow-f : Arrow t0 t1 - arrow-g : Arrow t0 t1 +data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where + id-t0 : TwoHom t0 t0 + id-t1 : TwoHom t1 t1 + arrow-f : TwoHom t0 t1 + arrow-g : TwoHom t0 t1 -record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁} ) : Set ( c₂) where - field - hom : Arrow {c₁} {c₂} a b -comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → Arrow {c₁} {c₂} b c → Arrow {c₁} {c₂} a b → Arrow {c₁} {c₂} a c +comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → TwoHom {c₁} {c₂} b c → TwoHom {c₁} {c₂} a b → TwoHom {c₁} {c₂} a c comp {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f comp {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g comp {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1 @@ -47,20 +44,20 @@ open TwoHom _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c ) -_×_ {c₁} {c₂} {a} {b} {c} f g = record { hom = comp {c₁} {c₂} {a} {b} {c} (hom f) (hom g ) } +_×_ {c₁} {c₂} {a} {b} {c} f g = comp {c₁} {c₂} {a} {b} {c} f g -- f g h -- d <- c <- b <- a -- --- It can be proved without Arrow constraints +-- It can be proved without TwoHom constraints assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } {f : (TwoHom {c₁} {c₂ } c d )} → {g : (TwoHom {c₁} {c₂ } b c )} → {h : (TwoHom {c₁} {c₂ } a b )} → - hom ( f × (g × h)) ≡ hom ((f × g) × h ) -assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with hom f | hom g | hom h + ( f × (g × h)) ≡ ((f × g) × h ) +assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with f | g | h assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0 | id-t0 | id-t0 = refl assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0 | id-t0 = refl assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0 | id-t0 = refl @@ -71,18 +68,18 @@ assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1 | id-t1 | id-t1 = refl TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) -TwoId {_} {_} t0 = record { hom = id-t0 } -TwoId {_} {_} t1 = record { hom = id-t1 } +TwoId {_} {_} t0 = id-t0 +TwoId {_} {_} t1 = id-t1 open import Relation.Binary open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) -TwoCat : {c₁ c₂ ℓ : Level } → Category c₁ c₂ c₂ -TwoCat {c₁} {c₂} {ℓ} = record { +TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂ +TwoCat {c₁} {c₂} = record { Obj = TwoObject {c₁} ; Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ; _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ; - _≈_ = λ x y → hom x ≡ hom y ; + _≈_ = λ x y → x ≡ y ; Id = λ{a} → TwoId {c₁ } { c₂} a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; @@ -92,36 +89,35 @@ associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} } } where - identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ((TwoId B) × f) ≡ hom f - identityL {c₁} {c₂} {a} {b} {f} with hom f + identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f + identityL {c₁} {c₂} {a} {b} {f} with f identityL {c₁} {c₂} {t1} {t1} | id-t1 = refl identityL {c₁} {c₂} {t0} {t0} | id-t0 = refl identityL {c₁} {c₂} {t0} {t1} | arrow-f = refl identityL {c₁} {c₂} {t0} {t1} | arrow-g = refl - identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ( f × TwoId A ) ≡ hom f - identityR {c₁} {c₂} {_} {_} {f} with hom f + identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f + identityR {c₁} {c₂} {_} {_} {f} with f identityR {c₁} {c₂} {t1} {t1} | id-t1 = refl identityR {c₁} {c₂} {t0} {t0} | id-t0 = refl identityR {c₁} {c₂} {t0} {t1} | arrow-f = refl identityR {c₁} {c₂} {t0} {t1} | arrow-g = refl o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → - hom f ≡ hom g → hom h ≡ hom i → hom ( h × f ) ≡ hom ( i × g ) + f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ≡-Reasoning in begin - hom ( h × f ) + ( h × f ) ≡⟨ refl ⟩ - comp (hom h) (hom f) - ≡⟨ cong (λ x → comp ( hom h ) x ) f==g ⟩ - comp (hom h) (hom g) - ≡⟨ cong (λ x → comp x ( hom g ) ) h==i ⟩ - comp (hom i) (hom g) + comp (h) (f) + ≡⟨ cong (λ x → comp ( h ) x ) f==g ⟩ + comp (h) (g) + ≡⟨ cong (λ x → comp x ( g ) ) h==i ⟩ + comp (i) (g) ≡⟨ refl ⟩ - hom ( i × g ) + ( i × g ) ∎ -indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → - (obj→ : Obj A -> TwoObject {c₁}) (hom→ : {a b : Obj A} -> Hom A a b -> TwoHom {c₁} {c₂} (obj→ a) (obj→ b) ) → Functor A A -indexFunctor {c₁} {c₂} {ℓ} A a b f g obj→ hom→ = record { +indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) A +indexFunctor {c₁} {c₂} {ℓ} A a b f g = record { FObj = λ a → fobj a ; FMap = λ {a} {b} f → fmap {a} {b} f ; isFunctor = record { @@ -130,38 +126,57 @@ ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} } } where - fobj : Obj A → Obj A - fobj x with obj→ x - fobj x | t0 = a - fobj x | t1 = b - fmap : {x y : Obj A } → (Hom A x y ) → Hom A (fobj x) (fobj y) - fmap {x} {y} h with obj→ x | obj→ y | hom ( hom→ h ) - fmap h | t0 | t0 | id-t0 = id1 A a - fmap h | t1 | t1 | id-t1 = id1 A b - fmap h | t0 | t1 | arrow-f = f - fmap h | t0 | t1 | arrow-g = g - ≈-cong : {a : Obj A} {b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ fmap f ≈ fmap g ] - ≈-cong {a} {b} {f} {g} f≈g = {!!} - identity : (x : Obj A ) -> A [ {!!} ≈ {!!} ] -- {!!} -- A [ fmap (id1 A x) ≈ id1 A (fobj x) ] - identity x with obj→ x - identity x | t0 = let open ≈-Reasoning (A) in begin - fmap (id1 A x) - ≈⟨ {!!} ⟩ - id1 A {!!} - ≈⟨⟩ - id1 A (fobj x ) - ∎ - identity _ | t1 = let open ≈-Reasoning (A) in {!!} - distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} → - A [ fmap (A [ g o f ]) ≈ A [ fmap g o fmap f ] ] - distr1 {a} {b} {c} {f} {g} = {!!} - -- distr1 {a} {b} {c} {f} {g} with (obj→ a) | (obj→ b ) | ( obj→ c ) | ( hom→ f ) | ( hom→ g ) - -- distr1 {a} {b} {c} {f} {g} | _ | _ | _ | _ | _ = ? - - - - - + T = TwoCat {c₁} {c₂} + fobj : Obj T → Obj A + fobj t0 = a + fobj t1 = b + fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y) + fmap {t0} {t0} id-t0 = id1 A a + fmap {t1} {t1} id-t1 = id1 A b + fmap {t0} {t1} arrow-f = f + fmap {t0} {t1} arrow-g = g + ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ] + ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom + identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ] + identity t0 = let open ≈-Reasoning A in refl-hom + identity t1 = let open ≈-Reasoning A in refl-hom + distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} → + A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ] + distr1 {a} {b} {c} {f} {g} with f | g + distr1 {t0} {t0} {t0} {f} {g} | id-t0 | id-t0 = let open ≈-Reasoning A in sym-hom idL + distr1 {t1} {t1} {t1} {f} {g} | id-t1 | id-t1 = let open ≈-Reasoning A in begin + id1 A b + ≈↑⟨ idL ⟩ + id1 A b o id1 A b + ∎ + distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-f = let open ≈-Reasoning A in begin + fmap (comp arrow-f id-t0) + ≈⟨⟩ + fmap arrow-f + ≈↑⟨ idR ⟩ + fmap arrow-f o id1 A a + ∎ + distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-g = let open ≈-Reasoning A in begin + fmap (comp arrow-g id-t0) + ≈⟨⟩ + fmap arrow-g + ≈↑⟨ idR ⟩ + fmap arrow-g o id1 A a + ∎ + distr1 {t0} {t1} {t1} {f} {g} | arrow-f | id-t1 = let open ≈-Reasoning A in begin + fmap (comp id-t1 arrow-f) + ≈⟨⟩ + fmap arrow-f + ≈↑⟨ idL ⟩ + id1 A b o fmap arrow-f + ∎ + distr1 {t0} {t1} {t1} {f} {g} | arrow-g | id-t1 = let open ≈-Reasoning A in begin + fmap (comp id-t1 arrow-g) + ≈⟨⟩ + fmap arrow-g + ≈↑⟨ idL ⟩ + id1 A b o fmap arrow-g + ∎ --- Equalizer --- f @@ -187,33 +202,34 @@ open Limit open NTrans -equlimit : {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A I) -> - Hom A ( limit-c comp ({!!} )) a -equlimit A I f g comp = {!!} +equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A (TwoCat {c₁} {c₂} )) -> + Hom A ( limit-c comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) a +equlimit A f g comp = {!!} -lim-to-equ : {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ) - (comp : Complete A I) +lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + (comp : Complete A (TwoCat {c₁} {c₂} ) ) → {a b : Obj A} (f g : Hom A a b ) - → IsEqualizer A (equlimit A I f g comp ) f g -lim-to-equ {c₁} {c₂} {ℓ} A I comp {a} {b} f g = record { - fe=ge = {!!} + → (fe=ge : A [ A [ f o (equlimit A f g comp ) ] ≈ A [ g o (equlimit A f g comp ) ] ] ) + → IsEqualizer A (equlimit A f g comp ) f g +lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge = record { + fe=ge = fe=ge ; k = λ {d} h fh=gh → k {d} h fh=gh ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' } where - open ≈-Reasoning A + I = TwoCat {c₁} {c₂} Γ : Functor I A - Γ = {!!} + Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g eqlim = isLimit comp Γ - c = {!!} - e = {!!} - k : {d : Obj A} (h : Hom A d a) → {!!} -- A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - k = {!!} -- {d} h fh=gh = {!!} - ek=h : (d : Obj A ) (h : Hom A d a ) → {!!} -- ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ] + c = limit-c comp Γ + e = equlimit A f g comp + k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c + k {d} h fh=gh = {!!} + ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ] ek=h = {!!} - uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) → {!!} -- A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ] + uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ] uniq-nat = {!!} uniquness : (d : Obj A ) (h : Hom A d a ) → ? → -- ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → ( k' : Hom A d c ) - → {!!} -- A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] + → A [ A [ e o k' ] ≈ h ] → A [ k h {!!} ≈ k' ] uniquness = {!!}