Mercurial > hg > Members > kono > Proof > category
changeset 472:f3d6d0275a0a
discrete equality as a dom equality
product from limit done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Mar 2017 03:21:46 +0900 |
| parents | 65ab0da524b8 |
| children | 2d32ded94aaf |
| files | discrete.agda limit-to.agda |
| diffstat | 2 files changed, 24 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/discrete.agda Mon Mar 06 17:16:27 2017 +0900 +++ b/discrete.agda Tue Mar 07 03:21:46 2017 +0900 @@ -102,6 +102,8 @@ : Set c₁ where field discrete : a ≡ b + dom : DiscreteObj S + dom = a open DiscreteHom @@ -115,16 +117,15 @@ 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₁} {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 + dom ( f * (g * h)) ≡ dom ((f * g) * h ) +assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl 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 ; + _≈_ = λ x y → dom x ≡ dom y ; Id = λ{a} → DiscreteId a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; @@ -134,24 +135,16 @@ associative = λ{a b c d f g h } → assoc-* { c₁} {S} {a} {b} {c} {d} {f} {g} {h} } } where - 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} = {!!} + identityL : {a b : DiscreteObj {c₁} S} {f : ( DiscreteHom {c₁} a b) } → dom ((DiscreteId b) * f) ≡ dom f + identityL {a} {b} {f} = refl + identityR : {A B : DiscreteObj S} {f : ( DiscreteHom {c₁} A B) } → dom ( f * DiscreteId A ) ≡ dom f + identityR {a} {b} {f} = refl 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-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl + dom f ≡ dom g → dom h ≡ dom i → dom ( h * f ) ≡ dom ( i * g ) + o-resp-≈ {a} {b} {c} {f} {g} {h} {i} refl refl = refl +
--- a/limit-to.agda Mon Mar 06 17:16:27 2017 +0900 +++ b/limit-to.agda Tue Mar 07 03:21:46 2017 +0900 @@ -238,6 +238,9 @@ → ( Γ : Functor (DiscreteCat S ) A ) → Obj A plimit A S comp Γ = limit-c comp Γ +discrete-identity : { c₁ : Level} { S : Set c₁} { a : DiscreteObj {c₁} S } → (f : DiscreteHom a a ) → (DiscreteCat S) [ f ≈ id1 (DiscreteCat S) a ] +discrete-identity f = refl + 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) ) @@ -250,14 +253,18 @@ A [ A [ FMap Γ f o qi a ] ≈ 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 + commute {a} {.a} {f} | refl = let open ≈-Reasoning A in begin FMap Γ f o qi a - ≈⟨ {!!} ⟩ - qi b + ≈⟨ car ( fcong Γ (discrete-identity f )) ⟩ + FMap Γ (id1 (DiscreteCat S) a ) o qi a + ≈⟨ car ( IsFunctor.identity (isFunctor Γ) ) ⟩ + id1 A (FObj Γ a) o qi a + ≈⟨ idL ⟩ + qi a ≈↑⟨ idR ⟩ - qi b o id q + qi a o id q ≈⟨⟩ - qi b o FMap (K A (DiscreteCat S) q) f + qi a o FMap (K A (DiscreteCat S) q) f ∎ lim-to-product : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set c₁ )