Mercurial > hg > Members > kono > Proof > category
view CCChom.agda @ 786:287d25c87b60
on going CCC
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 18 Apr 2019 10:00:20 +0900 |
| parents | a67959bcd44b |
| children | ca5eba647990 |
line wrap: on
line source
open import Level open import Category module CCChom where open import HomReasoning open import cat-utility open import Data.Product renaming (_×_ to _∧_) open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality open Functor -- ccc-1 : Hom A a 1 ≅ {*} -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c data One : Set where OneObj : One -- () in Haskell ( or any one object set ) OneCat : Category Level.zero Level.zero Level.zero OneCat = record { Obj = One ; Hom = λ a b → One ; _o_ = λ{a} {b} {c} x y → OneObj ; _≈_ = λ x y → x ≡ y ; Id = λ{a} → OneObj ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; identityL = λ{a b f} → lemma {a} {b} {f} ; identityR = λ{a b f} → lemma {a} {b} {f} ; o-resp-≈ = λ{a b c f g h i} _ _ → refl ; associative = λ{a b c d f g h } → refl } } where lemma : {a b : One } → { f : One } → OneObj ≡ f lemma {a} {b} {f} with f ... | OneObj = refl record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where field ≅→ : Hom A a b → Hom B a' b' ≅← : Hom B a' b' → Hom A a b iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where field ccc-1 : {a : Obj A} {b c : Obj OneCat} → -- Hom A a １ ≅ {*} IsoS A OneCat a １ b c ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b ) IsoS A (A × A) c (a * b) (c , c ) (a , b ) ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c IsoS A A a (c ^ b) (a * b) c record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where field one : Obj A _*_ : Obj A → Obj A → Obj A _^_ : Obj A → Obj A → Obj A isCCChom : IsCCChom A one _*_ _^_ open import HomReasoning open import CCC CCC→hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) → CCChom A CCC→hom A c = record { one = CCC.１ c ; _*_ = CCC._∧_ c ; _^_ = CCC._<=_ c ; isCCChom = record { ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 } ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 } ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 } } } where c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj c101 _ = OneObj c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.１ c) c102 {a} OneObj = CCC.○ c a c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f c103 {a} {OneObj} {OneObj} {OneObj} = refl c104 : {a : Obj A} → {f : Hom A a (CCC.１ c)} → A [ (c102 ( c101 f )) ≈ f ] c104 {a} {f} = let open ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) f ) c201 : { c₁ a b : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b) c201 f = ( A [ CCC.π c o f ] , A [ CCC.π' c o f ] ) c202 : { c₁ a b : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b) c202 (f , g ) = CCC.<_,_> c f g c203 : { c₁ a b : Obj A} → {f : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ (c201 ( c202 f )) ≈ f ] c203 = ( IsCCC.e3a (CCC.isCCC c) , IsCCC.e3b (CCC.isCCC c)) c204 : { c₁ a b : Obj A} → {f : Hom A c₁ ((c CCC.∧ a) b)} → A [ (c202 ( c201 f )) ≈ f ] c204 = IsCCC.e3c (CCC.isCCC c) c301 : { d a b : Obj A} → Hom A a ((c CCC.<= d) b) → Hom A ((c CCC.∧ a) b) d -- a -> d <= b -> (a ∧ b ) -> d c301 {d} {a} {b} f = A [ CCC.ε c o CCC.<_,_> c ( A [ f o CCC.π c ] ) ( CCC.π' c ) ] c302 : { d a b : Obj A} → Hom A ((c CCC.∧ a) b) d → Hom A a ((c CCC.<= d) b) c302 f = CCC._* c f c303 : { c₁ a b : Obj A} → {f : Hom A ((c CCC.∧ a) b) c₁} → A [ (c301 ( c302 f )) ≈ f ] c303 = IsCCC.e4a (CCC.isCCC c) c304 : { c₁ a b : Obj A} → {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f )) ≈ f ] c304 = IsCCC.e4b (CCC.isCCC c) open CCChom open IsCCChom open IsoS hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A hom→CCC A h = record { １ = １ ; ○ = ○ ; _∧_ = _/\_ ; <_,_> = <,> ; π = π ; π' = π' ; _<=_ = _<=_ ; _* = _* ; ε = ε ; isCCC = isCCC } where １ : Obj A １ = one h ○ : (a : Obj A ) → Hom A a １ ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj _/\_ : Obj A → Obj A → Obj A _/\_ a b = _*_ h a b <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a /\ b) <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g ) π : {a b : Obj A } → Hom A (a /\ b) a π {a} {b} = proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) )) π' : {a b : Obj A } → Hom A (a /\ b) b π' {a} {b} = proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) )) _<=_ : (a b : Obj A ) → Obj A _<=_ = _^_ h _* : {a b c : Obj A } → Hom A (a /\ b) c → Hom A a (c <= b) _* = ≅← ( ccc-3 (isCCChom h ) ) ε : {a b : Obj A } → Hom A ((a <= b ) /\ b) a ε {a} {b} = ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) isCCC : CCC.IsCCC A １ ○ _/\_ <,> π π' _<=_ _* ε isCCC = record { e2 = e2 ; e3a = e3a ; e3b = e3b ; e3c = e3c ; π-cong = π-cong ; e4a = e4a ; e4b = e4b } where e20 : ∀ ( f : Hom OneCat OneObj OneObj ) → _[_≈_] OneCat {OneObj} {OneObj} f OneObj e20 OneObj = refl e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ] e2 {a} f = begin f ≈↑⟨ iso← ( ccc-1 (isCCChom h )) ⟩ ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj}) ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f ) ≈⟨ ≡-cong {Level.zero} {Level.zero} {Level.zero} {OneCat} {OneObj} {OneObj} ( λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) ) ⟩ ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) OneObj ≈⟨⟩ ○ a ∎ where open ≈-Reasoning A e30 : {a b c d e : Obj A} → { f : Hom A ((_*_ h b) c) ((_*_ h d) e) } → {g : Hom A a ((_*_ h b) c) } → A [ A [ proj₁ (≅→ (ccc-2 (isCCChom h)) f ) o g ] ≈ proj₁ (≅→ (ccc-2 (isCCChom h)) (A [ f o g ] ) ) ] e30 = {!!} e31 : {a b c d e : Obj A} → {i : Hom (A × A) (b , c) (d , e )} → { f : Hom A a b } → {g : Hom A a c } → A [ A [ {!!} o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ] ≈ ( ≅← (ccc-2 (isCCChom h)) ( _[_o_] (A × A) i (f , g ) )) ] e31 = {!!} e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o <,> f g ] ≈ f ] e3a {a} {b} {c} {f} {g} = begin π o <,> f g ≈⟨⟩ proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o (≅← (ccc-2 (isCCChom h)) (f , g)) ≈⟨ e30 ⟩ proj₁ (≅→ (ccc-2 (isCCChom h)) (_[_o_] A ( id1 A ( _*_ h a b )) ( ≅← (ccc-2 (isCCChom h)) (f , g) ) )) ≈⟨ {!!} ⟩ proj₁ (≅→ (ccc-2 (isCCChom h)) (≅← (ccc-2 (isCCChom h)) ( _[_o_] (A × A ) ( id1 A a , id1 A b ) (f , g) ))) ≈⟨ {!!} ⟩ proj₁ ( f , g ) ≈⟨⟩ f ∎ where open ≈-Reasoning A e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o <,> f g ] ≈ g ] e3b = {!!} e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ] e3c = {!!} π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ <,> f g ≈ <,> f' g' ] π-cong {a} {b} {c} {f} {f'} {g} {g'} eq1 eq2 = begin <,> f g ≈⟨⟩ ≅← (ccc-2 (isCCChom h)) (f , g) ≈⟨ ≡-cong {!!} {!!} ⟩ ≅← (ccc-2 (isCCChom h)) (f' , g') ≈⟨⟩ <,> f' g' ∎ where open ≈-Reasoning A e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] e4a {a} {b} {c} {k} = begin ε o ( <,> ((k *) o π ) π' ) ≈⟨⟩ ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π')) ≈⟨ {!!} ⟩ k ∎ where open ≈-Reasoning A e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ] e4b = {!!}