Mercurial > hg > Members > kono > Proof > category
changeset 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 |
| files | CCChom.agda |
| diffstat | 1 files changed, 49 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/CCChom.agda Wed Apr 17 21:32:56 2019 +0900 +++ b/CCChom.agda Thu Apr 18 10:00:20 2019 +0900 @@ -148,18 +148,62 @@ ; 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 f = {!!} + 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 = {!!} + 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 = {!!} - e4a : {a b c : Obj A} → { h : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (h *) o π ] ) π') ] ≈ h ] - e4a = {!!} + π-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 = {!!}