Mercurial > hg > Members > kono > Proof > category

changeset 966:cb970ab7c32b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Feb 2021 11:13:31 +0900
parents 396bf884f5e7
children 472bcadfd216
files src/bi-ccc.agda
diffstat 1 files changed, 15 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/bi-ccc.agda	Thu Feb 25 02:01:37 2021 +0900
+++ b/src/bi-ccc.agda	Thu Feb 25 11:13:31 2021 +0900
@@ -40,10 +40,24 @@
        open ≈-Reasoning A
        open CCC.CCC C
        open BICCC B
+       bi-hom← : {a c : Obj A } → Hom A (a ∧ ⊥) c → Hom A ⊥ (c <= a )
+       bi-hom← f = (f o < π' , π > ) *
+       bi-hom→ : {a c : Obj A } →  Hom A ⊥ (c <= a ) → Hom A (a ∧ ⊥) c
+       bi-hom→ f =  ε o ( < π' , π > o < π , f o π' > )
+       bi-hom-iso : {a : Obj A } → {f : Hom A  (a ∧ ⊥) (a ∧ ⊥)}  →  A [ bi-hom→ (bi-hom← f )  ≈ f ] 
+       bi-hom-iso = {!!}
+       bi-hom-cong : {a c : Obj A } → {f g : Hom A ⊥ (c <= a )} → A [ f ≈ g ]  →  A [ bi-hom→ f   ≈ bi-hom→ g ]
+       bi-hom-cong = {!!}
        bi-ccc-0 :  A [ A [ □ ( a ∧ ⊥ ) o π' ] ≈ id1 A ( a ∧ ⊥ ) ]
        bi-ccc-0 = begin
              □ ( a ∧ ⊥ ) o π'
-          ≈⟨ {!!}  ⟩
+          ≈↑⟨ bi-hom-iso ⟩
+             bi-hom→ (bi-hom← ( □ ( a ∧ ⊥ ) o π' ))
+          ≈⟨ bi-hom-cong  (IsBICCC.e5 isBICCC ) ⟩
+             bi-hom→ ( □ ( ( a ∧ ⊥ ) <=  a) )
+          ≈↑⟨ bi-hom-cong  (IsBICCC.e5 isBICCC ) ⟩
+             bi-hom→ (bi-hom← (id1 A ( a ∧ ⊥ )))
+          ≈⟨ bi-hom-iso ⟩
              id1 A ( a ∧ ⊥ )
           ∎ 
        bi-ccc-1 :  A [ A [ □ a o f ] ≈ id1 A a ]