# HG changeset patch # User Shinji KONO # Date 1555585642 -32400 # Node ID ca5eba647990b8d6c70eb3a2a70983016954515b # Parent 287d25c87b60904710b7f31ccc8ced26cfc67b14 ... diff -r 287d25c87b60 -r ca5eba647990 CCC.agda --- a/CCC.agda Thu Apr 18 10:00:20 2019 +0900 +++ b/CCC.agda Thu Apr 18 20:07:22 2019 +0900 @@ -30,6 +30,7 @@ -- closed e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ] e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ] + *-cong : {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ] → A [ f * ≈ f' * ] e'2 : A [ ○ １ ≈ id1 A １ ] e'2 = let open ≈-Reasoning A in begin diff -r 287d25c87b60 -r ca5eba647990 CCChom.agda --- a/CCChom.agda Thu Apr 18 10:00:20 2019 +0900 +++ b/CCChom.agda Thu Apr 18 20:07:22 2019 +0900 @@ -43,6 +43,8 @@ ≅← : 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 ] + cong→ : {f g : Hom A a b } → A [ f ≈ g ] → B [ ≅→ f ≈ ≅→ g ] + cong← : {f g : Hom B a' b'} → B [ f ≈ g ] → A [ ≅← f ≈ ≅← g ] record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) @@ -73,9 +75,9 @@ ; _*_ = 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 } + 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 } } } where c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj @@ -102,6 +104,31 @@ 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) + c105 : {a : Obj A } {f g : Hom OneCat OneObj OneObj} → _[_≈_] OneCat {OneObj} {OneObj} f g → A [ c102 {a} f ≈ c102 {a} g ] + c105 refl = let open ≈-Reasoning A in refl-hom + c106 : { a : Obj A } {f g : Hom A a (CCC.１ c)} → A [ f ≈ g ] → _[_≈_] OneCat {OneObj} {OneObj} OneObj OneObj + c106 _ = refl + c205 : { a b c₁ : Obj A } {f g : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ f ≈ g ] → A [ c202 f ≈ c202 g ] + c205 f=g = IsCCC.π-cong (CCC.isCCC c ) (proj₁ f=g ) (proj₂ f=g ) + c206 : { a b c₁ : Obj A } {f g : Hom A c₁ ((c CCC.∧ a) b)} → A [ f ≈ g ] → (A × A) [ c201 f ≈ c201 g ] + c206 {a} {b} {c₁} {f} {g} f=g = ( begin + CCC.π c o f + ≈⟨ cdr f=g ⟩ + CCC.π c o g + ∎ ) , ( begin + CCC.π' c o f + ≈⟨ cdr f=g ⟩ + CCC.π' c o g + ∎ ) where open ≈-Reasoning A + c305 : { a b c₁ : Obj A } {f g : Hom A ((c CCC.∧ a) b) c₁} → A [ f ≈ g ] → A [ (c CCC.*) f ≈ (c CCC.*) g ] + c305 f=g = IsCCC.*-cong (CCC.isCCC c ) f=g + c306 : { a b c₁ : Obj A } {f g : Hom A a ((c CCC.<= c₁) b)} → A [ f ≈ g ] → A [ c301 f ≈ c301 g ] + c306 {a} {b} {c₁} {f} {g} f=g = begin + CCC.ε c o CCC.<_,_> c ( f o CCC.π c ) ( CCC.π' c ) + ≈⟨ 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 + open CCChom open IsCCChom @@ -147,6 +174,7 @@ ; π-cong = π-cong ; e4a = e4a ; e4b = e4b + ; *-cong = *-cong } where e20 : ∀ ( f : Hom OneCat OneObj OneObj ) → _[_≈_] OneCat {OneObj} {OneObj} f OneObj e20 OneObj = refl @@ -161,22 +189,46 @@ ≈⟨⟩ ○ 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 ) )) ] + -- + -- g id + -- a -------------> b * c ------> b * c + -- + -- 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 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) ))) - ≈⟨ {!!} ⟩ + ≈⟨ cong-proj₁ e30 ⟩ + 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 ) ≈⟨⟩ f @@ -190,20 +242,37 @@ <,> f g ≈⟨⟩ ≅← (ccc-2 (isCCChom h)) (f , g) - ≈⟨ ≡-cong {!!} {!!} ⟩ + ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 ) ⟩ ≅← (ccc-2 (isCCChom h)) (f' , g') ≈⟨⟩ <,> f' g' ∎ where open ≈-Reasoning A + e40 : {a c : Obj A} → { f : Hom A (_*_ h a c ) a } → A [ ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) f) ≈ f ] + e40 = iso→ (ccc-3 (isCCChom h)) + e41 : {a c : Obj A} → { f : Hom A a (_^_ h c a )} → A [ ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) f) ≈ f ] + e41 = iso← (ccc-3 (isCCChom h)) 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 π ) , π')) + ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π')) ≈⟨ {!!} ⟩ + ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k) + ≈⟨ iso→ (ccc-3 (isCCChom h)) ⟩ 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 = {!!} + e4b {a} {b} {c} {k} = begin + ( ε o ( <,> ( k o π ) π' ) ) * + ≈⟨⟩ + ≅← (ccc-3 (isCCChom h)) ( ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) o (≅← (ccc-2 (isCCChom h)) ( k o π , π'))) + ≈⟨ {!!} ⟩ + ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k) + ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩ + k + ∎ where open ≈-Reasoning A + *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ] + *-cong eq = cong← ( ccc-3 (isCCChom h )) eq + + diff -r 287d25c87b60 -r ca5eba647990 HomReasoning.agda --- a/HomReasoning.agda Thu Apr 18 10:00:20 2019 +0900 +++ b/HomReasoning.agda Thu Apr 18 20:07:22 2019 +0900 @@ -54,11 +54,19 @@ car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → x ≈ y → ( x o f ) ≈ ( y o f ) - car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq + car eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq + + car1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → + A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y o f ] ] + car1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) ) eq cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → x ≈ y → f o x ≈ f o y - cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) + cdr eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) + + cdr1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → + A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f o y ] ] + cdr1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) ) id : (a : Obj A ) → Hom A a a id a = (Id {_} {_} {_} {A} a)