# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1617299292 -32400
# Node ID b6dbec7e535bb3bdf1c39231af9652d787b566d0
# Parent  40c39d3e6a758d163b9192a7f3e20a32e2c74d94
...

diff -r 40c39d3e6a75 -r b6dbec7e535b src/ToposEx.agda
--- a/src/ToposEx.agda	Wed Mar 31 15:58:02 2021 +0900
+++ b/src/ToposEx.agda	Fri Apr 02 02:48:12 2021 +0900
@@ -115,7 +115,7 @@
 
 --
 --
---   Hom equality and Ω
+--   Hom equality and Ω    (p.94 cl(Δ a) in Takeuchi )
 --
 --
 --       a -----------→ +
@@ -319,19 +319,42 @@
                      < (nsuc iNat) o π ,  g' o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨ car ( IsCCC.π-cong isCCC refl-hom (car (sym g=g')) ) ⟩
                      < (nsuc iNat) o π ,  g  o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩
                      nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ∎
---  
---    open Functor
---    open import Category.Sets
---    open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
---    record SubObjectFuntor : Set  ( suc (suc c₁ ) ⊔  suc (suc c₂) ⊔ suc ℓ )  where
---       field
---          Sub    : Functor A  (Sets {c₂})
---          smonic : Mono A {!!}
---  
---    open SubObjectFuntor
---    postulate  ≡←≈ :   {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
---    sub→topos : (Ω : Obj A) → (S : SubObjectFuntor) → Representable A ≡←≈ (Sub S) Ω → Topos A c
---    sub→topos Ω S R = record {
+ 
+--   open Functor
+--   open import Category.Sets
+--   open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
+-- 
+--   record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+--      field
+--         sb : Obj A
+--         sm : Hom A sb a 
+--         smono : Mono A sm
+-- 
+--   postulate
+--      S : (a : Set (c₁ ⊔ c₂ ⊔ ℓ))  → Set c₂
+--      solv← : (x : Obj A) → S (SubObject x) → SubObject x
+--      solv→ : (x : Obj A) → SubObject x → S (SubObject x)
+--      -- soiso← : (x :  Set (c₁ ⊔ c₂ ⊔ ℓ)) → solv← (solv→ x) ≡ x
+--      -- soiso→ : (x : Set c₂ ) → solv→ (solv← x) ≡ x
+--      ≡←≈ :   {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
+--   open SubObject 
+-- 
+--   smap : {x y : Obj A} → Hom A y x → SubObject x → SubObject y
+--   smap h s = record { sb = sb s ; sm = A [ {!!} o sm s ] ; smono = record { isMono = λ f g eq → Mono.isMono (smono s) f g {!!} } } 
+--    -- A [ A [ A [ h o  (sm s) ] o f ] ≈ A [ A [ h o (sm s) ] o g ]  → A [ A [ sm s o f ] ≈ A [ sm s o g ] ]
+-- 
+--   Smap : {x y : Obj A} → Hom A y x → Hom Sets (S (SubObject x)) (S (SubObject y))
+--   Smap {x} {y} h s = solv→ y (smap h (solv← x s))
+-- 
+--   SubObjectFuntor  : Functor  (Category.op A)  (Sets {c₂})
+--   SubObjectFuntor  = record {
+--        FObj = λ x → S (SubObject x)
+--      ; FMap = Smap
+--      ; isFunctor  = {!!}
+--      } 
+-- 
+--   sub→topos : (Ω : Obj A) → Representable A ≡←≈ SubObjectFuntor Ω → Topos A c
+--   sub→topos Ω R = record {
 --           Ω =  Ω
 --        ;  ⊤ = {!!}
 --        ;  Ker = {!!}
@@ -341,16 +364,15 @@
 --        ;  ker-m = {!!}
 --           } }
 --  
---    topos→sub : (t : Topos A c ) → SubObjectFuntor
---    topos→sub t = record {
---           Sub = record {
---              FObj = {!!}
---            ; FMap = {!!}
---            ; isFunctor = {!!}
---         } ; smonic = {!!}
---       }
---  
---    topos→rep : (t : Topos A c ) → Representable A ≡←≈ (Sub (topos→sub t)) (Topos.Ω t)
---    topos→rep t = {!!}
+--   topos→rep : (t : Topos A c ) → Representable A ≡←≈ SubObjectFuntor (Topos.Ω t)
+--   topos→rep t = record {
+--         repr→ = record { TMap = λ a Sa → Topos.char t (sm (solv← a Sa)) (smono (solv← a Sa)) ; isNTrans = record { commute = {!!} } } -- Hom A a Ω
+--       ; repr← = record { TMap = λ a h →  solv→ a record {sb = equalizer-c (Ker t h) ; sm = equalizer (Ker t h) ; smono =
+--          {!!} } ; isNTrans = {!!} }  -- FObj (Sub S) a
+--       ; reprId→  = {!!}
+--       ; reprId←  = {!!}
+--     }
 --  
 --  
+-- 
+-- 
diff -r 40c39d3e6a75 -r b6dbec7e535b src/cat-utility.agda
--- a/src/cat-utility.agda	Wed Mar 31 15:58:02 2021 +0900
+++ b/src/cat-utility.agda	Fri Apr 02 02:48:12 2021 +0900
@@ -534,37 +534,37 @@
         postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
         
         Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( ≡←≈ :   {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y )
-           (a : Obj A) → Functor A (Sets {c₂})
+           (a : Obj A) → Functor (Category.op A) (Sets {c₂})
         Yoneda  {c₁} {c₂} {ℓ} A ≡←≈ a = record {
-            FObj = λ b → Hom A a b
-          ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ]    --   f : Hom A x y  → Hom Sets (Hom A a x ) (Hom A a y)
+            FObj = λ b → Hom (Category.op A) a b
+          ; FMap = λ {x} {y} (f : Hom A y x ) → λ ( g : Hom A x a ) →  (Category.op A)  [ f o g ]    --   f : Hom A x y  → Hom Sets (Hom A a x ) (Hom A a y)
           ; isFunctor = record {
-                     identity =  λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ;
+                     identity =  λ {b} → extensionality  (Category.op A)  ( λ x → lemma-y-obj1 {b} x ) ;
                      distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ;
-                     ≈-cong = λ eq → extensionality A ( λ x →  lemma-y-obj3 x eq ) 
+                     ≈-cong = λ eq → extensionality  (Category.op A)  ( λ x →  lemma-y-obj3 x eq ) 
                 } 
             }  where
-                lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) →  A [ id1 A b o x ] ≡ x
-                lemma-y-obj1 {b} x = let open ≈-Reasoning A  in ≡←≈ idL
-                lemma-y-obj2 :  (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ 
-                       A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
-                lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ ( sym assoc )
-                lemma-y-obj3 :  {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] →   A [ f o x ] ≡ A [ g o x ]
-                lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning A in ≡←≈ ( resp refl-hom eq )
+                lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) →   (Category.op A)  [ id1 A b o x ] ≡ x
+                lemma-y-obj1 {b} x = let open ≈-Reasoning  (Category.op A)   in ≡←≈ idL
+                lemma-y-obj2 :  (a₁ b c : Obj A) (f : Hom A b a₁)  (g : Hom A c b ) → (x : Hom A a₁ a )→ 
+                        (Category.op A)  [  (Category.op A)  [ g o f ] o x ] ≡ (Sets [ _[_o_]  (Category.op A)  g o _[_o_]  (Category.op A)  f ]) x
+                lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning  (Category.op A)  in ≡←≈ ( sym assoc )
+                lemma-y-obj3 :  {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) →  (Category.op A)  [ f ≈ g ] →    (Category.op A)  [ f o x ] ≡  (Category.op A)  [ g o x ]
+                lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning  (Category.op A)  in ≡←≈ ( resp refl-hom eq )
         
         -- Representable  U  ≈　Hom(A,-)
         
         record Representable  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
-              ( ≡←≈ :   {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y )
-              ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
+              ( ≡←≈ :   {a b : Obj A } { x y : Hom A b a } →  (x≈y :  (Category.op A)  [ x ≈ y  ]) → x ≡ y )
+              ( U : Functor  (Category.op A)  (Sets {c₂}) ) (a : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
            field
                  -- FObj U x  :  A  → Set
                  -- FMap U f  =  Set → Set (locally small)
                  -- λ b → Hom (a,b) :  A → Set
                  -- λ f → Hom (a,-) = λ b → Hom  a b    
         
-                 repr→ : NTrans A (Sets {c₂}) U (Yoneda A  ≡←≈  a )
-                 repr← : NTrans A (Sets {c₂}) (Yoneda A  ≡←≈  a)  U
+                 repr→ : NTrans  (Category.op A)  (Sets {c₂}) U (Yoneda A  ≡←≈  a )
+                 repr← : NTrans  (Category.op A)  (Sets {c₂}) (Yoneda A  ≡←≈  a)  U
                  reprId→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A  ≡←≈  a) x )]
                  reprId←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
         
diff -r 40c39d3e6a75 -r b6dbec7e535b src/freyd2.agda
--- a/src/freyd2.agda	Wed Mar 31 15:58:02 2021 +0900
+++ b/src/freyd2.agda	Fri Apr 02 02:48:12 2021 +0900
@@ -6,7 +6,7 @@
    where
 
 open import HomReasoning
-open import cat-utility hiding (Yoneda)
+open import cat-utility hiding (Yoneda ; Representable )
 open import Relation.Binary.Core
 open import Function
 
@@ -24,10 +24,6 @@
 -- A is localy small
 postulate ≡←≈ :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
 
-Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
-Yoneda  {c₁} {c₂} {ℓ} A a = cat-utility.Yoneda A (≡←≈ A) a
-
-
 import Axiom.Extensionality.Propositional
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
@@ -44,47 +40,47 @@
 open IsLimit
 open import Category.Cat
 
--- Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
--- Yoneda  {c₁} {c₂} {ℓ} A a = record {
---     FObj = λ b → Hom A a b
---   ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ]    --   f : Hom A x y  → Hom Sets (Hom A a x ) (Hom A a y)
---   ; isFunctor = record {
---              identity =  λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ;
---              distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ;
---              ≈-cong = λ eq → extensionality A ( λ x →  lemma-y-obj3 x eq ) 
---         } 
---     }  where
---         lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) →  A [ id1 A b o x ] ≡ x
---         lemma-y-obj1 {b} x = let open ≈-Reasoning A  in ≡←≈ A idL
---         lemma-y-obj2 :  (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ 
---                A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
---         lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ A ( begin
---                A [ A [ g o f ] o x ]
---              ≈↑⟨ assoc ⟩
---                A [ g o A [ f o x ] ]
---              ≈⟨⟩
---                ( λ x →  A [ g o x  ]  ) ( ( λ x → A [ f o x ] ) x )
---              ∎ )
---         lemma-y-obj3 :  {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] →   A [ f o x ] ≡ A [ g o x ]
---         lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning A in ≡←≈ A ( begin
---                 A [ f o x ]
---              ≈⟨ resp refl-hom eq ⟩
---                 A [ g o x ]
---              ∎ )
+Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
+Yoneda  {c₁} {c₂} {ℓ} A a = record {
+    FObj = λ b → Hom A a b
+  ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ]    --   f : Hom A x y  → Hom Sets (Hom A a x ) (Hom A a y)
+  ; isFunctor = record {
+             identity =  λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ;
+             distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ;
+             ≈-cong = λ eq → extensionality A ( λ x →  lemma-y-obj3 x eq ) 
+        } 
+    }  where
+        lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) →  A [ id1 A b o x ] ≡ x
+        lemma-y-obj1 {b} x = let open ≈-Reasoning A  in ≡←≈ A idL
+        lemma-y-obj2 :  (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ 
+               A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
+        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ A ( begin
+               A [ A [ g o f ] o x ]
+             ≈↑⟨ assoc ⟩
+               A [ g o A [ f o x ] ]
+             ≈⟨⟩
+               ( λ x →  A [ g o x  ]  ) ( ( λ x → A [ f o x ] ) x )
+             ∎ )
+        lemma-y-obj3 :  {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] →   A [ f o x ] ≡ A [ g o x ]
+        lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning A in ≡←≈ A ( begin
+                A [ f o x ]
+             ≈⟨ resp refl-hom eq ⟩
+                A [ g o x ]
+             ∎ )
 
 -- -- Representable  U  ≈　Hom(A,-)
 
--- record Representable  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
---    field
---          -- FObj U x  :  A  → Set
---          -- FMap U f  =  Set → Set (locally small)
---          -- λ b → Hom (a,b) :  A → Set
---          -- λ f → Hom (a,-) = λ b → Hom  a b    
+record Representable  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
+   field
+         -- FObj U x  :  A  → Set
+         -- FMap U f  =  Set → Set (locally small)
+         -- λ b → Hom (a,b) :  A → Set
+         -- λ f → Hom (a,-) = λ b → Hom  a b    
 
---          repr→ : NTrans A (Sets {c₂}) U (Yoneda A a )
---          repr← : NTrans A (Sets {c₂}) (Yoneda A a)  U
---          reprId→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )]
---          reprId←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
+         repr→ : NTrans A (Sets {c₂}) U (Yoneda A a )
+         repr← : NTrans A (Sets {c₂}) (Yoneda A a)  U
+         reprId→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )]
+         reprId←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
 
 open Representable
 
@@ -285,7 +281,7 @@
      (U : Functor A (Sets {c₂}) )
      ( i : Obj ( K A Sets * ↓ U) )
      (In : HasInitialObject ( K A Sets * ↓ U) i ) 
-       → Representable A (≡←≈ A) U (obj i)
+       → Representable A  U (obj i)
 UisRepresentable A U i In = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
         ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }