# HG changeset patch # User Shinji KONO # Date 1555644048 -32400 # Node ID a3e124e36acf9d85fc213ca0756601e592474124 # Parent ca5eba647990b8d6c70eb3a2a70983016954515b nat in ccc-2 diff -r ca5eba647990 -r a3e124e36acf CCChom.agda --- a/CCChom.agda Thu Apr 18 20:07:22 2019 +0900 +++ b/CCChom.agda Fri Apr 19 12:20:48 2019 +0900 @@ -56,7 +56,11 @@ 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 - + nat-2 : {a b c : Obj A} → {f : Hom A (b * c) (b * c) } → {g : Hom A a (b * c) } + → (A × A) [ (A × A) [ IsoS.≅→ ccc-2 f o (g , g) ] ≈ IsoS.≅→ ccc-2 ( A [ f o g ] ) ] + +open import CCC + record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where field @@ -67,8 +71,6 @@ 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 @@ -78,6 +80,7 @@ ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 ; cong← = c105 ; cong→ = c106 } ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 ; cong← = c205; cong→ = c206 } ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 ; cong← = c305 ; cong→ = c306 } + ; nat-2 = nat-2 } } where c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj @@ -128,6 +131,14 @@ ≈⟨ cdr ( IsCCC.π-cong (CCC.isCCC c ) (car f=g ) refl-hom) ⟩ CCC.ε c o CCC.<_,_> c ( g o CCC.π c ) ( CCC.π' c ) ∎ where open ≈-Reasoning A + nat-2 : {a b : Obj A} {c = c₁ : Obj A} {f : Hom A ((c CCC.∧ b) c₁) ((c CCC.∧ b) c₁)} + {g : Hom A a ((c CCC.∧ b) c₁)} → (A × A) [ (A × A) [ c201 f o g , g ] ≈ c201 (A [ f o g ]) ] + nat-2 {a} {b} {c₁} {f} {g} = ( begin + ( CCC.π c o f) o g + ≈↑⟨ assoc ⟩ + ( CCC.π c ) o (f o g) + ∎ ) , (sym-hom assoc) where open ≈-Reasoning A + open CCChom @@ -196,35 +207,16 @@ -- a -------------> b * c ------> b -- a -------------> b * c ------> c -- - e31 : {a b c : Obj A} → {f : Hom A ((_*_ h b) c) ((_*_ h b) c) } → {g : Hom A a ((_*_ h b) c) } - → (A × A) [ (A × A) [ ≅→ (ccc-2 (isCCChom h)) f o (g , g ) ] ≈ ≅→ (ccc-2 (isCCChom h)) ( A [ f o g ] ) ] - e31 = {!!} - e30 : {a b c : Obj A} → {g : Hom A a ((_*_ h b) c) } - → (A × A) [ (A × A) [ (≅→ (ccc-2 (isCCChom h)) (id1 A ((_*_ h b) c))) o (g , g) ] ≈ (≅→ (ccc-2 (isCCChom h)) (A [ id1 A ((_*_ h b) c) o g ] ) ) ] - e30 {a} {b} {c} {g} = begin - (≅→ (ccc-2 (isCCChom h)) (id1 A ((_*_ h b) c))) o (g , g) - ≈⟨⟩ - ( π , π' ) o ( g , g ) - ≈⟨⟩ - ( _[_o_] A π g , _[_o_] A π' g ) - ≈↑⟨ cdr1 A (iso← (ccc-2 (isCCChom h))) , cdr1 A (iso← (ccc-2 (isCCChom h))) ⟩ - ( _[_o_] A (proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h b c) ))) (≅← (ccc-2 (isCCChom h))((≅→ (ccc-2 (isCCChom h))) g)) , - _[_o_] A π' (≅← (ccc-2 (isCCChom h))((≅→ (ccc-2 (isCCChom h))) g)) ) - ≈⟨ {!!} ⟩ - ( proj₁ ((≅→ (ccc-2 (isCCChom h))) g) , proj₂ ((≅→ (ccc-2 (isCCChom h))) g) ) - ≈⟨⟩ - ≅→ (ccc-2 (isCCChom h)) g - ≈↑⟨ cong→ (ccc-2 (isCCChom h)) ( idL1 A ) ⟩ - ≅→ (ccc-2 (isCCChom h)) (_[_o_] A ( id1 A ((_*_ h b) c)) g ) - ∎ where open ≈-Reasoning (A × A) cong-proj₁ : {a b c d : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₁ f ≈ proj₁ g ] cong-proj₁ eq = proj₁ eq + cong-proj₂ : {a b c d : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₂ f ≈ proj₂ g ] + cong-proj₂ eq = proj₂ eq 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)) - ≈⟨ cong-proj₁ e30 ⟩ + ≈⟨ cong-proj₁ (nat-2 (isCCChom h)) ⟩ proj₁ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) )) ≈⟨ cong-proj₁ ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩ proj₁ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) )) @@ -234,9 +226,34 @@ 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 = {!!} + e3b {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)) + ≈⟨ cong-proj₂ (nat-2 (isCCChom h)) ⟩ + proj₂ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) )) + ≈⟨ cong-proj₂ ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩ + proj₂ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) )) + ≈⟨ cong-proj₂ ( iso→ (ccc-2 (isCCChom h))) ⟩ + proj₂ ( f , g ) + ≈⟨⟩ + g + ∎ where open ≈-Reasoning A e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ] - e3c = {!!} + e3c {a} {b} {c} {f} = begin + <,> ( π o f ) ( π' o f ) + ≈⟨⟩ + ≅← (ccc-2 (isCCChom h)) ( ( proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) ))) o f + , ( proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b)))) o f ) + ≈⟨⟩ + ≅← (ccc-2 (isCCChom h)) (_[_o_] (A × A) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) (f , f ) ) + ≈⟨ cong← (ccc-2 (isCCChom h)) (nat-2 (isCCChom h)) ⟩ + ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) o f )) + ≈⟨ cong← (ccc-2 (isCCChom h)) (cong→ (ccc-2 (isCCChom h)) idL ) ⟩ + ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) f ) + ≈⟨ iso← (ccc-2 (isCCChom h)) ⟩ + f + ∎ where open ≈-Reasoning A π-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 @@ -257,6 +274,9 @@ ≈⟨⟩ ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π')) ≈⟨ {!!} ⟩ + ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) + (_[_o_] (A × A) ( ≅← (ccc-3 (isCCChom h)) k , id1 A b ) ( π , π'))) + ≈⟨ {!!} ⟩ ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k) ≈⟨ iso→ (ccc-3 (isCCChom h)) ⟩ k