Mercurial > hg > Members > kono > Proof > category
changeset 469:65ab0da524b8
discrete f ≡ refl should be passed, but it doesn't
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 06 Mar 2017 17:16:27 +0900 |
| parents | c375d8f93a2c |
| children | f0fe49acd45d f3d6d0275a0a |
| files | discrete.agda limit-to.agda |
| diffstat | 2 files changed, 75 insertions(+), 61 deletions(-) [+] |
line wrap: on
line diff
--- a/discrete.agda Mon Mar 06 15:45:51 2017 +0900 +++ b/discrete.agda Mon Mar 06 17:16:27 2017 +0900 @@ -92,49 +92,64 @@ -- Category with no arrow but identity -record DiscreteObj {c₁ : Level } : Set c₁ - where +record DiscreteObj {c₁ : Level } (S : Set c₁) : Set c₁ where + field + obj : S open DiscreteObj -record DiscreteHom { c₁ : Level} (a : DiscreteObj {c₁} ) (b : DiscreteObj {c₁} ) +record DiscreteHom { c₁ : Level} { S : Set c₁} (a : DiscreteObj {c₁} S) (b : DiscreteObj {c₁} S) : Set c₁ where + field + discrete : a ≡ b open DiscreteHom -_*_ : ∀ {c₁} → {a b c : DiscreteObj {c₁}} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c -_*_ {_} {a} {b} {c} x _ = record { } +_*_ : ∀ {c₁} → {S : Set c₁} {a b c : DiscreteObj {c₁} S} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c +_*_ {_} {a} {b} {c} x y = record {discrete = trans ( discrete y) (discrete x) } -DiscreteId : { c₁ : Level} ( a : DiscreteObj ) → DiscreteHom {c₁} a a -DiscreteId a = record { } +DiscreteId : { c₁ : Level} { S : Set c₁} ( a : DiscreteObj {c₁} S ) → DiscreteHom {c₁} a a +DiscreteId a = record { discrete = refl } + +open import Relation.Binary.PropositionalEquality -assoc-* : {c₁ : Level } {a b c d : DiscreteObj {c₁} } - {f : (DiscreteHom {c₁} c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} → +assoc-* : {c₁ : Level } { S : Set c₁} {a b c d : DiscreteObj {c₁} S} + {f : (DiscreteHom c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} → ( f * (g * h)) ≡ ((f * g) * h ) -assoc-* {c₁} {a} {b} {c} {d} {f} {g} {h } = refl +assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } with discrete f | discrete g | discrete h +assoc-* {c₁} {S} {a} {.a} {.a} {.a} {f} {g} {h } | refl | refl | refl = refl -DiscreteCat : {c₁ : Level } → Category c₁ c₁ c₁ -DiscreteCat {c₁} = record { - Obj = DiscreteObj ; - Hom = λ a b → DiscreteHom a b ; - _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {a} {b} {c} x y ; +DiscreteCat : {c₁ : Level } → (S : Set c₁) → Category c₁ c₁ c₁ +DiscreteCat {c₁} S = record { + Obj = DiscreteObj {c₁} S ; + Hom = λ a b → DiscreteHom {c₁} {S} a b ; + _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ; _≈_ = λ x y → x ≡ y ; Id = λ{a} → DiscreteId a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; - identityL = λ{a b f} → identityL {c₁} {a} {b} {f} ; - identityR = λ{a b f} → identityR {c₁} {a} {b} {f} ; - o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {a} {b} {c} {f} {g} {h} {i} ; - associative = λ{a b c d f g h } → assoc-* {c₁} {a} {b} {c} {d} {f} {g} {h} + identityL = λ{a b f} → identityL {a} {b} {f} ; + identityR = λ{a b f} → identityR {a} {b} {f} ; + o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; + associative = λ{a b c d f g h } → assoc-* { c₁} {S} {a} {b} {c} {d} {f} {g} {h} } } where - identityL : {c₁ : Level } {a b : DiscreteObj {c₁}} {f : ( DiscreteHom {c₁} a b) } → ((DiscreteId b) * f) ≡ f - identityL {c₁} {a} {b} {f} = refl - identityR : {c₁ : Level } {A B : DiscreteObj {c₁}} {f : ( DiscreteHom {c₁} A B) } → ( f * DiscreteId A ) ≡ f - identityR {c₁} {a} {b} {f} = refl - o-resp-≈ : {c₁ : Level } {A B C : DiscreteObj {c₁} } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} → + identityL : {a b : DiscreteObj {c₁} S} {f : ( DiscreteHom {c₁} a b) } → ((DiscreteId b) * f) ≡ f + identityL {a} {b} {f} with discrete f + identityL {a} {.a} {f} | refl = let open ≡-Reasoning in begin + record { discrete = trans refl refl } + ≡⟨⟩ + record { discrete = refl } + ≡⟨ sym ( ≡-cong ( \x -> record { discrete = x } ) {!!} ) ⟩ + record { discrete = discrete f } + ≡⟨⟩ + f + ∎ + identityR : {A B : DiscreteObj S} {f : ( DiscreteHom {c₁} A B) } → ( f * DiscreteId A ) ≡ f + identityR {a} {b} {f} = {!!} + o-resp-≈ : {A B C : DiscreteObj S } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} → f ≡ g → h ≡ i → ( h * f ) ≡ ( i * g ) - o-resp-≈ {c₁} {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl + o-resp-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl
--- a/limit-to.agda Mon Mar 06 15:45:51 2017 +0900 +++ b/limit-to.agda Mon Mar 06 17:16:27 2017 +0900 @@ -10,7 +10,7 @@ open import discrete ---- Equalizer from Limit ( 2->A functor Γ and Nat : K -> Γ) +--- Equalizer from Limit ( 2->A IdnexFunctor Γ and IndexNat : K -> Γ) --- --- --- f @@ -230,77 +230,76 @@ ∎ -plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A ( DiscreteCat {c₁} ) ) - → ( Γ : Functor (DiscreteCat {c₁}) A ) → Obj A -plimit A comp Γ = limit-c comp Γ +--- Product from Limit ( given Discrete->A functor Γ and pnat : K -> Γ) + +open DiscreteHom -pnat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A ( DiscreteCat {c₁} ) ) - → (Γ : Functor (DiscreteCat {c₁}) A ) - → (q : Obj A ) ( qi : (i : Obj ( DiscreteCat {c₁} )) → Hom A q (FObj Γ i) ) - → NTrans DiscreteCat A (K A DiscreteCat q) Γ -pnat {c₁} A comp Γ q qi = record { +plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁) (comp : Complete A ( DiscreteCat S ) ) + → ( Γ : Functor (DiscreteCat S ) A ) → Obj A +plimit A S comp Γ = limit-c comp Γ + +pnat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁) (comp : Complete A ( DiscreteCat S ) ) + → (Γ : Functor (DiscreteCat S ) A ) + → (q : Obj A ) ( qi : (i : Obj ( DiscreteCat S)) → Hom A q (FObj Γ i) ) + → NTrans (DiscreteCat S )A (K A (DiscreteCat S) q) Γ +pnat A S comp Γ q qi = record { TMap = qi ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } } where - commute : {a b : Obj (DiscreteCat {c₁}) } {f : Hom ( DiscreteCat {c₁}) a b} → + commute : {a b : Obj (DiscreteCat S) } {f : Hom ( DiscreteCat S) a b} → A [ A [ FMap Γ f o qi a ] ≈ - A [ qi b o FMap (K A (DiscreteCat {c₁} )q) f ] ] - commute {a} {b} {f} = let open ≈-Reasoning A in begin + A [ qi b o FMap (K A (DiscreteCat S )q) f ] ] + commute {a} {b} {f} with discrete f + commute {a} {b} {f} | refl = let open ≈-Reasoning A in begin FMap Γ f o qi a - ≈⟨⟩ - FMap Γ (id1 (DiscreteCat {c₁}) b ) o qi a - ≈⟨ car ( IsFunctor.identity ( isFunctor Γ )) ⟩ - id (FObj Γ b) o qi a - ≈⟨ idL ⟩ - qi a - ≈⟨⟩ + ≈⟨ {!!} ⟩ qi b ≈↑⟨ idR ⟩ qi b o id q ≈⟨⟩ - qi b o FMap (K A (DiscreteCat {c₁} )q) f + qi b o FMap (K A (DiscreteCat S) q) f ∎ -lim-to-product : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - (comp : Complete A ( DiscreteCat {c₁} ) ) - → ( Γ : Functor (DiscreteCat {c₁}) A ) - → IProduct {c₁} A (Obj ( DiscreteCat {c₁}) )(plimit A comp Γ) (λ i → FObj Γ i ) ( λ i → TMap (limit-u comp Γ) i ) -lim-to-product {c₁} A comp Γ = record { +lim-to-product : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set c₁ ) + (comp : Complete A ( DiscreteCat S ) ) + → ( Γ : Functor (DiscreteCat S ) A ) + → IProduct A (Obj ( DiscreteCat S ) )(plimit A S comp Γ) (λ i → FObj Γ i ) ( λ i → TMap (limit-u comp Γ) i ) +lim-to-product A S comp Γ = record { iproduct = λ {q} qi → iproduct {q} qi ; pif=q = λ {q } qi { i } → pif=q {q} qi {i} ; ip-uniqueness = λ {q } { h } → ip-uniqueness {q} {h} ; ip-cong = λ {q } { qi } { qi' } qi=qi' → ip-cong {q} {qi} {qi'} qi=qi' } where - D = DiscreteCat {c₁} - I = Obj ( DiscreteCat {c₁} ) + D = DiscreteCat S + I = Obj ( DiscreteCat S ) lim = isLimit comp Γ ai = λ i → FObj Γ i p = limit-c comp Γ pi = λ i → TMap (limit-u comp Γ) i iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p - iproduct {q} qi = limit lim q (pnat A comp Γ q qi ) + iproduct {q} qi = limit lim q (pnat A S comp Γ q qi ) pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ] - pif=q {q} qi {i} = t0f=t lim {q} {pnat A comp Γ q qi } {i} + pif=q {q} qi {i} = t0f=t lim {q} {pnat A S comp Γ q qi } {i} ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ] ipu {i} q h = let open ≈-Reasoning A in refl-hom ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] - ip-uniqueness {q} {h} = limit-uniqueness lim {q} {pnat A comp Γ q (λ i → A [ pi i o h ] )} h (ipu q h) + ip-uniqueness {q} {h} = limit-uniqueness lim {q} {pnat A S comp Γ q (λ i → A [ pi i o h ] )} h (ipu q h) ipc : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } → (i : I ) → A [ qi i ≈ qi' i ] → - A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A comp Γ q qi) i ] + A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S comp Γ q qi) i ] ipc {q} {qi} {qi'} i qi=qi' = let open ≈-Reasoning A in begin TMap (limit-u comp Γ) i o iproduct qi' ≈⟨⟩ - TMap (limit-u comp Γ) i o limit lim q (pnat A comp Γ q qi' ) - ≈⟨ t0f=t lim {q} {pnat A comp Γ q qi'} {i} ⟩ - TMap (pnat A comp Γ q qi') i + TMap (limit-u comp Γ) i o limit lim q (pnat A S comp Γ q qi' ) + ≈⟨ t0f=t lim {q} {pnat A S comp Γ q qi'} {i} ⟩ + TMap (pnat A S comp Γ q qi') i ≈⟨⟩ qi' i ≈↑⟨ qi=qi' ⟩ qi i ≈⟨⟩ - TMap (pnat A comp Γ q qi) i + TMap (pnat A S comp Γ q qi) i ∎ ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ] - ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness lim {q} {pnat A comp Γ q qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i)) + ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness lim {q} {pnat A S comp Γ q qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))