# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1614186097 -32400
# Node ID 396bf884f5e7ecbb441b6eeeaf9c18dc45975a47
# Parent  0128a662eb029f91cba7af531e2e0d5c14d35811
bi-cartesian

diff -r 0128a662eb02 -r 396bf884f5e7 src/CCC.agda
--- a/src/CCC.agda	Tue Feb 23 16:32:06 2021 +0900
+++ b/src/CCC.agda	Thu Feb 25 02:01:37 2021 +0900
@@ -149,7 +149,7 @@
         (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ]))
         (char : {a b : Obj A} → (m :  Hom A b a) → Mono A m  → Hom A a Ω) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
-         char-ker  : {a b : Obj A } {h : Hom A a Ω} 
+         char-ker  : {a b : Obj A } (h : Hom A a Ω)
              → A [ char (equalizer (Ker h)) record { isMono = λ f g → monic (Ker h) } ≈ h ]
          ker-char : {a b : Obj A} →  (m :  Hom A b a) → (mono : Mono A m)  → Iso A b (  equalizer-c (Ker ( char m mono ))) 
 
diff -r 0128a662eb02 -r 396bf884f5e7 src/ToposEx.agda
--- a/src/ToposEx.agda	Tue Feb 23 16:32:06 2021 +0900
+++ b/src/ToposEx.agda	Thu Feb 25 02:01:37 2021 +0900
@@ -61,4 +61,26 @@
              IsEqualizer.k (isEqualizer (Ker t h)) p1' (lemma1 p1' p2' eq)  ≈⟨ IsEqualizer.uniqueness  (isEqualizer (Ker t h)) pe1 ⟩
              p' ∎ 
 
+topos-m-pullback : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
+  → (e2  : {a : Obj A} → ∀ { f : Hom A a １ } →  A [ f ≈ ○ a ] )
+  → (t : Topos A １ ○ ) → {a b : Obj A}  → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono )  (⊤ t)
+topos-m-pullback A １ ○ e2 t {a} {b} m mono  = topos-pullback A １ ○ e2 t {a} (char t m mono)
 
+---
+---
+---
+
+-- SubObjectFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →  ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
+--   → (e2  : {a : Obj A} → ∀ { f : Hom A a １ } →  A [ f ≈ ○ a ] )  → (t : Topos A １ ○ ) →  Functor A A
+-- SubObjectFunctor A １ ○  e2 t = record {
+--       FObj = λ x → Ω t
+--     ; FMap = {!!}
+--     ; isFunctor = record {
+--           identity = {!!}
+--         ; distr = {!!}
+--         ; ≈-cong  = {!!}
+--       }
+--    }
+
+
+
diff -r 0128a662eb02 -r 396bf884f5e7 src/bi-ccc.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/bi-ccc.agda	Thu Feb 25 02:01:37 2021 +0900
@@ -0,0 +1,73 @@
+module bi-ccc where
+
+open import Category
+open import CCC
+open import Level
+open import HomReasoning
+open import cat-utility
+
+record IsBICCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+      ( ⊥ : Obj A)  -- ０
+      ( □ : (a : Obj A ) → Hom A ⊥ a )
+      ( _∨_ :  Obj A → Obj A → Obj A  )
+      ( [_,_] : {a b c : Obj A } → Hom A a c → Hom A b c → Hom A (a ∨ b) c  )
+      ( κ : {a b : Obj A }  → Hom A a (a ∨ b)  )
+      ( κ' : {a b : Obj A } → Hom A b (a ∨ b)  )
+             :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+   field
+       e5 : {a : Obj A} → { f : Hom A ⊥ a } →  A [ f ≈ □ a ]
+       e6a : {a b c : Obj A} → { f : Hom A a c }{ g : Hom A b c } →  A [ A [ [ f , g ] o κ  ] ≈ f ]
+       e6b : {a b c : Obj A} → { f : Hom A a c }{ g : Hom A b c } →  A [ A [ [ f , g ] o κ'  ] ≈ g ]
+       e6c : {a b c : Obj A} → { h : Hom A (a ∨ b ) c } →  A [ [ A [ h o κ ] , A [ h o κ' ] ] ≈ h ]
+       κ-cong :  {a b c : Obj A} → { f f' : Hom A a c }{ g g' : Hom A b c } → A [ f ≈ f' ]  → A [ g ≈ g' ]  →  A [ [ f , g ]  ≈ [ f' , g' ] ] 
+
+record BICCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+   field
+      ⊥ : Obj A
+      □ : (a : Obj A ) → Hom A ⊥ a 
+      _∨_ :  Obj A → Obj A → Obj A  
+      [_,_] : {a b c : Obj A } → Hom A a c → Hom A b c → Hom A (a ∨ b) c  
+      κ : {a b : Obj A }  → Hom A a (a ∨ b)  
+      κ' : {a b : Obj A } → Hom A b (a ∨ b)  
+      isBICCC : IsBICCC A ⊥ □ _∨_  [_,_] κ κ'
+
+bi-ccc-⊥ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → (C : CCC A ) → (B : BICCC A ) → {a : Obj A} → Hom A a (BICCC.⊥ B) → Iso A a (BICCC.⊥ B)
+bi-ccc-⊥ A C B {a} f = record {
+      ≅→ = f
+    ; ≅← = □ a
+    ; iso→  = bi-ccc-1
+    ; iso←  = bi-ccc-2 } where
+       open ≈-Reasoning A
+       open CCC.CCC C
+       open BICCC B
+       bi-ccc-0 :  A [ A [ □ ( a ∧ ⊥ ) o π' ] ≈ id1 A ( a ∧ ⊥ ) ]
+       bi-ccc-0 = begin
+             □ ( a ∧ ⊥ ) o π'
+          ≈⟨ {!!}  ⟩
+             id1 A ( a ∧ ⊥ )
+          ∎ 
+       bi-ccc-1 :  A [ A [ □ a o f ] ≈ id1 A a ]
+       bi-ccc-1 = begin
+             □ a o f
+          ≈⟨ resp (sym (IsCCC.e3b isCCC) ) (sym ( IsBICCC.e5 isBICCC)) ⟩
+             (π  o  □ ( a ∧ ⊥ )) o (π' o < id1 A a , f > )
+          ≈⟨ sym assoc ⟩
+             π  o  ( □ ( a ∧ ⊥ ) o (π' o < id1 A a , f > ))
+          ≈⟨ cdr (assoc) ⟩
+             π  o  ( □ ( a ∧ ⊥ ) o π' ) o < id1 A a , f > 
+          ≈⟨ cdr (car bi-ccc-0) ⟩
+             π  o  id1 A _ o < id1 A a , f > 
+          ≈⟨ cdr idL ⟩
+             π  o  < id1 A a , f > 
+          ≈⟨ IsCCC.e3a isCCC  ⟩
+             id1 A a 
+          ∎ 
+       bi-ccc-2 :  A [ A [ f o □ a ] ≈ id1 A ⊥  ]
+       bi-ccc-2 = begin
+             f o □  a 
+          ≈⟨ IsBICCC.e5 isBICCC  ⟩
+             □  _ 
+          ≈↑⟨ IsBICCC.e5 isBICCC  ⟩
+             id1 A ⊥ 
+          ∎ 
+