--- a/src/bi-ccc.agda	Thu Feb 25 11:13:31 2021 +0900
+++ b/src/bi-ccc.agda	Thu Feb 25 13:08:17 2021 +0900
@@ -45,9 +45,31 @@
        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-iso {a} {f} = begin
+            bi-hom→ (bi-hom← f )
+          ≈⟨⟩
+            ε o ( < π' , π > o < π , ((f o < π' , π > ) *) o π' > )
+          ≈⟨ cdr (IsCCC.π-exchg isCCC)  ⟩
+            ε o ( < ((f o < π' , π > ) *) o π' , π > )
+          ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom (sym idL)) ⟩
+            ε o ( < ((f o < π' , π > ) *) o π' , id1 A _ o π > )
+          ≈↑⟨ cdr (IsCCC.exchg-π isCCC) ⟩
+            ε o (( < ((f o < π' , π > ) *) o π , id1 A _ o π' > ) o < π' , π > )
+          ≈⟨ cdr (car ( IsCCC.π-cong isCCC refl-hom idL)) ⟩
+            ε o (( < ((f o < π' , π > ) *) o π , π' > ) o < π' , π > )
+          ≈⟨ assoc ⟩
+            (ε o ( < ((f o < π' , π > ) *) o π , π' > )) o < π' , π > 
+          ≈⟨ car (IsCCC.e4a isCCC) ⟩
+            (f o < π' , π >) o < π' , π >
+          ≈⟨ sym assoc ⟩
+            f o (< π' , π > o < π' , π >)
+          ≈⟨ cdr (IsCCC.π'π isCCC) ⟩
+            f o id1 A _
+          ≈⟨ idR ⟩
+            f  
+          ∎ 
        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-hom-cong f=g = cdr ( cdr (IsCCC.π-cong isCCC refl-hom (car f=g) ))
        bi-ccc-0 :  A [ A [ □ ( a ∧ ⊥ ) o π' ] ≈ id1 A ( a ∧ ⊥ ) ]
        bi-ccc-0 = begin
              □ ( a ∧ ⊥ ) o π'