Mercurial > hg > Members > kono > Proof > category

changeset 1112:0e750446e463

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 Fri, 24 Nov 2023 08:49:21 +0900
parents 73c72679421c
children 918a0cf1c056
files src/Definitions.agda src/SetsCompleteness.agda src/freyd.agda src/freyd2.agda src/system-f.agda
diffstat 5 files changed, 116 insertions(+), 130 deletions(-) [+]
line wrap: on
line diff
--- a/src/Definitions.agda	Mon Oct 09 17:00:17 2023 +0900
+++ b/src/Definitions.agda	Fri Nov 24 08:49:21 2023 +0900
@@ -241,6 +241,38 @@
                 → C [ C [ ( FMap H (FMap F f )) o  ( TMap n (FObj F a)) ]  ≈ C [ (TMap n (FObj F b )) o  (FMap G (FMap F f))  ] ]
              commute  {a} {b} {f}  =  IsNTrans.commute ( isNTrans n)
 
+    record SObj {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (P : Obj A → Set ℓ ) :  Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+        field
+           s : Obj A
+           p : P s
+
+    FullSubCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (P : Obj A → Set ℓ ) → Category (suc c₁ ⊔ suc c₂ ⊔ suc ℓ)  c₂ ℓ
+    FullSubCategory A P = record {
+           Obj = SObj A P
+         ; Hom = λ a b → Hom A (SObj.s a) (SObj.s b)  -- full
+         ; _o_ = λ f g → A [ f o g ]
+         ; _≈_ = λ f g → A [ f ≈ g ]
+         ; Id = λ {a} → id1 A (SObj.s a)
+         ; isCategory = record {
+                isEquivalence = IsCategory.isEquivalence (Category.isCategory A )
+              ; identityL = idL 
+              ; identityR = idR
+              ; o-resp-≈ = resp
+              ; associative = assoc
+           }
+      } where open ≈-Reasoning A
+
+    InclusiveFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (P : Obj A → Set ℓ ) → Functor (FullSubCategory A P) A
+    InclusiveFunctor A P = record {
+         FObj = λ x → SObj.s x
+       ; FMap = λ {a} {b} f → f
+       ; isFunctor = record  {
+              ≈-cong = λ eq → eq
+            ; identity = refl-hom
+            ; distr = refl-hom
+          }
+       }  where open ≈-Reasoning A
+
     -- T ≃  (U_R ○ F_R)
     -- μ = U_R ε F_R
     --      nat-ε
@@ -525,16 +557,15 @@
          ; t0 =  LimitNat I A C Γ (a0 limita ) (t0 limita) G
          ; isLimit = preserve Γ limita }
 
-    record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' )
-            : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
+    record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
       field
-         climit :  ( Γ : Functor I A ) → Limit I A Γ
+         climit :  { I : Category c₁' c₂' ℓ' } ( Γ : Functor I A ) → Limit I A Γ
          cproduct : ( I : Set c₁' ) (fi : I → Obj A )  → IProduct I A fi -- c₁ should be a free level
          cequalizer : {a b : Obj A} (f g : Hom A a b)  → Equalizer A  f g
       open Limit
-      limit-c :  ( Γ : Functor I A ) → Obj A
+      limit-c :  {I : Category c₁' c₂' ℓ' } ( Γ : Functor I A ) → Obj A
       limit-c  Γ  = a0 ( climit Γ)
-      limit-u :  ( Γ : Functor I A ) →  NTrans I A ( K I A (limit-c Γ )) Γ
+      limit-u : {I : Category c₁' c₂' ℓ' } ( Γ : Functor I A ) →  NTrans I A ( K I A (limit-c Γ )) Γ
       limit-u  Γ  = t0 ( climit Γ)
       open Equalizer
       equalizer-p : {a b : Obj A} (f g : Hom A a b)  → Obj A
--- a/src/SetsCompleteness.agda	Mon Oct 09 17:00:17 2023 +0900
+++ b/src/SetsCompleteness.agda	Fri Nov 24 08:49:21 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS #-}
 
 open import Category -- https://github.com/konn/category-agda
 open import Level
@@ -11,8 +11,10 @@
 open import Function
 import Relation.Binary.PropositionalEquality
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → ( λ x → f x ≡ λ x → g x )
--- import Axiom.Extensionality.Propositional
--- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
+
+import Axiom.Extensionality.Propositional
+postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
+
 -- Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
 ≡cong = Relation.Binary.PropositionalEquality.cong
@@ -21,7 +23,7 @@
 
 lemma1 :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} {f g : Hom Sets a b} →
    Sets [ f ≈ g ] → (x : a ) → f x  ≡ g x
-lemma1 refl  x  = refl
+lemma1 eq  x  = ?
 
 record Σ {a} (A : Set a) (B : Set a) : Set a where
   constructor _,_
@@ -39,16 +41,16 @@
        ; π2 = λ ab → (proj₂ ab)
        ; isProduct = record {
               _×_  = λ f g  x →   record { proj₁ = f  x ;  proj₂ =  g  x }     -- ( f x ,  g x )
-              ; π1fxg=f = refl
-              ; π2fxg=g  = refl
-              ; uniqueness = refl
+              ; π1fxg=f = ?
+              ; π2fxg=g  = ?
+              ; uniqueness = ?
               ; ×-cong   =  λ {c} {f} {f'} {g} {g'} f=f g=g →  prod-cong a b f=f g=g
           }
       } where
           prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b }
               → Sets [ f ≈ f' ] → Sets [ g ≈ g' ]
               → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
-          prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl
+          prod-cong a b {c} {f} {f1} {g} {g1} eq eq1 = ?
 
 
 record iproduct {a} (I : Set a)  ( pi0 : I → Set a ) : Set a where
@@ -74,9 +76,9 @@
        iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
        iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x  }
        pif=q : {q : Obj Sets} {qi : (i : I) → Hom Sets q (fi i)} → {i : I} → Sets [ Sets [ (λ prod → pi1 prod i) o iproduct1 qi ] ≈ qi i ]
-       pif=q {q} {qi} {i} = refl
+       pif=q {q} {qi} {i} = ?
        ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ]
-       ip-uniqueness = refl
+       ip-uniqueness = ?
        ipcx : {q :  Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 qi x ≡ iproduct1 qi' x
        ipcx {q} {qi} {qi'} qi=qi x  =
               begin
@@ -102,8 +104,8 @@
           _+_ = sum
         ; κ1f+g=f = ? -- extensionality Sets (λ x → refl )
         ; κ2f+g=g = ? -- extensionality Sets (λ x → refl )
-        ; uniqueness = λ {c} {h} → extensionality Sets (λ x → uniq {c} {h} x )
-        ; +-cong = λ {c} {f} {f'} {g} {g'} feq geq → extensionality Sets (pccong feq geq)
+        ; uniqueness = λ {c} {h} → ? -- extensionality Sets (λ x → uniq {c} {h} x )
+        ; +-cong = λ {c} {f} {f'} {g} {g'} feq geq → ? -- extensionality Sets (pccong feq geq)
        }
      } where
         sum : {c : Obj Sets} → Hom Sets a c → Hom Sets b c → Hom Sets (coproduct a b ) c
@@ -135,15 +137,15 @@
         isum : {q : Obj Sets} → ((i : I) → Hom Sets (fi i) q) → Hom Sets (icoproduct I fi) q
         isum {q} fi (ki1 i x) = fi i x
         kif=q : {q : Obj Sets} {qi : (i : I) → Hom Sets (fi i) q} {i : I} → Sets [ Sets [ isum qi o (λ x → ki1 i x) ] ≈ qi i ]
-        kif=q {q} {qi} {i} =  extensionality Sets (λ x → refl )
+        kif=q {q} {qi} {i} =  ? -- extensionality Sets (λ x → refl )
         uniq : {q : Obj Sets} {h : Hom Sets (icoproduct I fi) q} → Sets [ isum (λ i → Sets [ h o (λ x → ki1 i x) ]) ≈ h ]
-        uniq {q} {h} =  extensionality Sets u1 where
+        uniq {q} {h} = ? where --   extensionality Sets u1 where
            u1 : (x : icoproduct I fi ) → isum (λ i → Sets [ h o (λ x₁ → ki1 i x₁) ]) x ≡ h x
            u1 (ki1 i x) = refl
         iccong : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets (fi i) q} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ isum qi ≈ isum qi' ]
-        iccong {q} {qi} {qi'} ieq =  extensionality Sets u2 where
+        iccong {q} {qi} {qi'} ieq = ? where --  extensionality Sets u2 where
            u2 : (x : icoproduct I fi ) → isum qi x ≡ isum qi' x
-           u2 (ki1 i x) = cong (λ k → k x ) (ieq i)
+           u2 (ki1 i x) = cong (λ k → k x ) ? -- (ieq i)
 
         --
         --         e             f
@@ -184,25 +186,25 @@
              ; uniqueness  = uniqueness
        } where
            fe=ge  :  Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
-           fe=ge  =  extensionality Sets (fe=ge0 )
+           fe=ge  =  ? -- extensionality Sets (fe=ge0 )
            k :  {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
-           k {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) eq )
+           k {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) ?  )
            ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
-           ek=h {d} {h} {eq} = refl
+           ek=h {d} {h} {eq} = ?
            injection :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} (f  : Hom Sets a b) → Set c₂
            injection f =  ∀ x y  → f x ≡ f y →  x  ≡ y
            lemma5 :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x)
-           lemma5 refl  x  = refl   -- somehow this is not equal to lemma1
+           lemma5 eq  x  = ? -- somehow this is not equal to lemma1
            uniqueness :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh  ≈ k' ]
-           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets  ( λ ( x : d ) →  begin
-                k h fh=gh x
-             ≡⟨ elm-cong ( k h fh=gh x) (  k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x )  ⟩
-                k' x
-             ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+           uniqueness  {d} {h} {fh=gh} {k'} ek'=h = ? --   extensionality Sets  ( λ ( x : d ) →  begin
+           --     k h fh=gh x
+           --  ≡⟨ elm-cong ( k h fh=gh x) (  k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x )  ⟩
+           --     k' x
+           --  ∎  ) where
+           --       open  import  Relation.Binary.PropositionalEquality
+           --       open ≡-Reasoning
 
 
 -- -- we have to make this Level c, that is {B : Set c} → (A → B) is iso to I : Set c
@@ -317,18 +319,19 @@
     comm1 :  {a b : Obj C} {f : Hom C a b} →
         Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈
         Sets [ (λ sn →  (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
-    comm1 {a} {b} {f} = extensionality Sets  ( λ  sn  →  begin
-                 FMap Γ f  (snmap sn  a )
-             ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( ≡←≈ s ( hom-iso s ))) ⟩
-                 FMap Γ ( hom← s ( hom→ s f))  (snmap sn  a )
-             ≡⟨⟩
-                 ΓMap s Γ (hom→ s f) (snmap sn a )
-             ≡⟨ sncommute sn a b  (hom→ s  f) ⟩
-                 snmap sn b
-             ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-
+    comm1 {a} {b} {f} = ?
+--   comm1 {a} {b} {f} = extensionality Sets  ( λ  sn  →  begin
+--                FMap Γ f  (snmap sn  a )
+--            ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( ≡←≈ s ( hom-iso s ))) ⟩
+--                FMap Γ ( hom← s ( hom→ s f))  (snmap sn  a )
+--            ≡⟨⟩
+--                ΓMap s Γ (hom→ s f) (snmap sn a )
+--            ≡⟨ sncommute sn a b  (hom→ s  f) ⟩
+--                snmap sn b
+--            ∎  ) where
+--                 open  import  Relation.Binary.PropositionalEquality
+--                 open ≡-Reasoning
+--
 
 SetsLimit : {  c₁ c₂ ℓ : Level} ( I :  Set  c₁ ) ( C : Category c₁ c₂ ℓ )  ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) )
     → Limit C Sets Γ
--- a/src/freyd.agda	Mon Oct 09 17:00:17 2023 +0900
+++ b/src/freyd.agda	Fri Nov 24 08:49:21 2023 +0900
@@ -13,48 +13,14 @@
 -- C is small full subcategory of A ( C is image of F )
 --    but we don't use smallness in this proof
 --
---  Exisiting self functor is stronger than a subcategory. It may not exisit constructively.
---  but it makes the proof easier.
-
-record FullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-           : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
-   field
-      FSF : Functor A A  
-      FSFMap← : { a b : Obj A } → Hom A (FObj FSF a) (FObj FSF b ) → Hom A a b 
-      full→ : { a b : Obj A } { x : Hom A (FObj FSF a) (FObj FSF b) } → A [ FMap FSF ( FSFMap← x ) ≈ x ]
-      full← : { a b : Obj A } { x : Hom A (FObj FSF a) (FObj FSF b) } → A [ FSFMap← ( FMap FSF x ) ≈ x ]
-
-record SubObj  {c₁ c₂ ℓ l : Level} (A : Category c₁ c₂ ℓ) ( P : Obj A → Set l) : Set (c₁ ⊔ l) where
-   field
-      obj : Obj A
-      pa  : P obj
-
-open SubObj
-
-SubCategory : {c₁ c₂ ℓ l : Level} (A : Category c₁ c₂ ℓ) ( P : Obj A → Set l) → Category (c₁ ⊔ l) c₂ ℓ
-SubCategory A P = record {
-   Obj = SubObj A P ;
-   Hom = λ a b  → Hom A (obj a) (obj b) ;
-   _o_ = λ { a b c } f g → A [ f o g ] ;
-   _≈_ = λ { a b  } f g → A [ f ≈ g ] ;
-   Id = λ { a } → id1 A (obj a) ;
-   isCategory = record {
-       isEquivalence = IsCategory.isEquivalence (Category.isCategory A)  
-     ; identityL = idL 
-     ; identityR = idR
-     ; associative = assoc
-     ; o-resp-≈ = resp
-     }
-  } where open ≈-Reasoning A
-
-
 -- pre-initial
 
 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-       (F : Functor A A)  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+       (P : Obj A → Set ℓ)  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
       preinitialObj : Obj A 
-      preinitialArrow : ∀{a : Obj A } →  Hom A ( FObj F preinitialObj ) a 
+      Pp : P preinitialObj
+      preinitialArrow : ∀{a : Obj A } →  Hom A ( FObj (InclusiveFunctor A P )  record { s = preinitialObj; p = Pp } ) a 
 
 -- initial object
 --   now in cat-utility
@@ -68,29 +34,29 @@
 open NTrans
 open Limit
 open IsLimit
-open FullSubcategory
 open PreInitial
 open Complete
 open Equalizer
 open IsEqualizer
 
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-      (comp : Complete A A)
-      (SFS : FullSubcategory A ) → 
-      (PI : PreInitial A  (FSF SFS )) → HasInitialObject A (limit-c comp (FSF SFS))
-initialFromPreInitialFullSubcategory A comp SFS PI = record {
+      (comp : Complete A)
+      (P : Obj A → Set ℓ ) → 
+      (PI : PreInitial A  P) → HasInitialObject A (limit-c comp (InclusiveFunctor A P))
+initialFromPreInitialFullSubcategory A comp P PI = record {
       initial = initialArrow ; 
       uniqueness  = λ {a} f → lemma1 a f
     } where
-      F : Functor A A 
-      F = FSF SFS   
-      FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b 
-      FMap←  = FSFMap←  SFS
+      S = FullSubCategory A P
+      F : Functor S A 
+      F = InclusiveFunctor A P 
+      pri : SObj A P
+      pri = record { s = preinitialObj PI ; p = Pp PI }  
       a00 : Obj A
       a00 = limit-c comp F
-      lim : ( Γ : Functor A A ) → Limit A A Γ 
+      lim : ( Γ : Functor S A ) → Limit S A Γ 
       lim Γ =  climit comp Γ 
-      u : NTrans A A (K A A a00) F
+      u : NTrans S A (K S A a00) F
       u = t0 ( lim F )
       equ : {a b : Obj A} → (f g : Hom A a b)  → IsEqualizer A (equalizer-e comp f g ) f g
       equ f g = isEqualizer ( Complete.cequalizer comp f g  )
@@ -98,14 +64,14 @@
       ep {a} {b} {f} {g} = equalizer-p comp f g
       ee :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ep {a} {b} {f} {g} ) a 
       ee {a} {b} {f} {g} = equalizer-e comp f g  
-      f : Hom A  a00 (FObj F  (preinitialObj PI ) ) 
-      f = TMap u (preinitialObj PI ) 
+      f : Hom A  a00 (FObj F pri ) 
+      f = TMap u pri 
       initialArrow :  ∀( a : Obj A )  →  Hom A a00 a
       initialArrow a  = A [ preinitialArrow PI {a}  o f ]
       equ-fi : { a : Obj A} → {f' : Hom A a00 a} → 
           IsEqualizer A ee ( A [ preinitialArrow PI {a} o  f ] ) f'
       equ-fi  {a} {f'} = equ ( A [ preinitialArrow PI {a} o  f ] ) f'
-      e=id : {e : Hom A a00 a00} → ( {c : Obj A} → A [ A [ TMap u  c o  e ]  ≈  TMap u c ] ) → A [ e  ≈ id1 A a00 ]
+      e=id : {e : Hom A a00 a00} → ( {c : Obj S} → A [ A [ TMap u  c o  e ]  ≈  TMap u c ] ) → A [ e  ≈ id1 A a00 ]
       e=id  {e} uce=uc =  let open ≈-Reasoning (A) in
             begin
               e
@@ -114,26 +80,22 @@
             ≈⟨ limit-uniqueness (isLimit (lim F))  ( λ {i} → idR ) ⟩
               id1 A a00
             ∎
-      kfuc=uc : {c k1 : Obj A} →  {p : Hom A k1 a00} → A [ A [ TMap u  c  o  
-              A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ]  
+      kfuc=uc : {c : Obj S} {k1 : Obj A} →  {p : Hom A k1 a00} → A [ A [ TMap u  c  o  
+              A [ p o A [ preinitialArrow PI {k1} o TMap u pri ] ] ]  
                       ≈ TMap u c ]
       kfuc=uc {c} {k1} {p} =  let open ≈-Reasoning (A) in
             begin
-                 TMap u  c  o ( p o ( preinitialArrow PI {k1} o TMap u (preinitialObj PI)  ))
+                 TMap u  c  o ( p o ( preinitialArrow PI {k1} o TMap u pri  ))
             ≈⟨ cdr assoc  ⟩
-                 TMap u c o ((p o preinitialArrow PI) o TMap u (preinitialObj PI))
+                 TMap u c o ((p o preinitialArrow PI) o TMap u pri)
             ≈⟨ assoc ⟩
-                 (TMap u  c  o ( p o ( preinitialArrow PI {k1} ))) o TMap u (preinitialObj PI)  
-            ≈↑⟨ car  ( full→ SFS ) ⟩
-                  FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI)
+                 (TMap u  c  o ( p o ( preinitialArrow PI {k1} ))) o TMap u pri  
             ≈⟨ nat u  ⟩
-                  TMap u c o FMap (K A A a00) (FMap← (TMap u c o p o preinitialArrow PI)) 
-            ≈⟨⟩
                   TMap u c o id1 A a00
             ≈⟨ idR ⟩
                  TMap u  c  
             ∎
-      kfuc=1 : {k1 : Obj A} →  {p : Hom A k1 a00} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a00 ]
+      kfuc=1 : {k1 : Obj A} →  {p : Hom A k1 a00} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u pri ] ] ≈ id1 A a00 ]
       kfuc=1 {k1} {p} = e=id ( kfuc=uc )
       -- if equalizer has right inverse, f = g
       lemma2 :  (a b : Obj A) {c : Obj A} ( f g : Hom A a b ) 
--- a/src/freyd2.agda	Mon Oct 09 17:00:17 2023 +0900
+++ b/src/freyd2.agda	Fri Nov 24 08:49:21 2023 +0900
@@ -2,7 +2,7 @@
 
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
-open import Category.Sets renaming ( _o_ to _*_ )
+open import Category.Sets -- renaming ( _o_ to _*_ )
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ; resp )
 
@@ -115,8 +115,7 @@
                  limit (isLimit lim) b (ta a x t ) o id1 A b 
              ≈⟨ idR ⟩
                  limit (isLimit lim) b (ta a x t ) 
-             -- ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≈←≡ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩
-             ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≈←≡ ( cong ( λ g → g x )( ? ))) ⟩
+             ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≈←≡ ( t0f=t {i} x )) ⟩
                   f x
              ∎  ))
 
@@ -418,27 +417,18 @@
       }  where open ≈-Reasoning A
     t00 : (a c d e : Obj opA) (f : Hom opA a c ) → Hom (A × A) (c , c) (d , e )
     t00 a c d e f = ≅→ (*-iso d e a  c) f  
-    nat-* : {a b c : Obj A} → NTrans (Category.op A) (Sets {c₂}) (Yoneda A (≡←≈ A) c ) (Yoneda (A × A) *eq (a , b) ○ prodFunctor )   
-    nat-* {a} {b} {c} = record { TMap = λ z f → ≅→ (*-iso a b c z) f  ; isNTrans = record { commute = nat-comm } } where
-       nat-comm : {x y : Obj opA} {f : Hom opA x y} → 
-            Sets [ Sets [ (λ g → opA [ f o proj₁ g ] , opA [ f o proj₂ g ]) o (λ f₁ → ≅→ (*-iso a b c x) f₁) ]
-               ≈  Sets [ (λ f₁ → ≅→ (*-iso a b c y) f₁) o (λ g → opA [ f o g ])  ]  ]
-       nat-comm {x} {y} {f} g =  cong₂ _,_ (  ≡←≈  A ( begin
-          ? ≈⟨ ? ⟩
-          ? ∎ )) (  ≡←≈ A  ( begin
-          ? ≈⟨ ? ⟩
-          ? ∎ )) where
-            open ≈-Reasoning A
-       -- = λ g → ( begin
-       --  opA [ f o proj₁ (≅→ (*-iso a b c x) g) ] , opA [ f o proj₂ (≅→ (*-iso a b c x) g) ] ≡⟨ cong₂ (λ j k → j , k ) (t01 g) ?  ⟩
-       --  proj₁ (≅→ (*-iso a b c y) ( opA [ f o g ] )) , proj₂ (≅→ (*-iso a b c y) ( opA [ f o g ] ) ) ≡⟨ refl ⟩
-       --  ≅→ (*-iso a b c y) ( opA [ f o g ] ) ∎ )   where 
-       --     open ≡-Reasoning
-       --     t01 :  {c : Obj A } → (g : Hom A x c) → opA [ f o proj₁ (≅→ (*-iso a b c x) g) ] ≡ proj₁ (≅→ (*-iso a b c y) (opA [ f o g ]))
-       --     t01 {c} g = begin
-       --         A [ proj₁ (≅→ (*-iso a b c x) g) o f ] ≡⟨ ≡←≈ A ? ⟩
-       --         proj₁ (≅→ (*-iso a b c y) (A [ g o f ])) ∎
-
+--    nat-* : {a b c : Obj A} → NTrans (Category.op A) (Sets {c₂}) (Yoneda A (≡←≈ A) c ) (Yoneda (A × A) *eq (a , b) ○ prodFunctor )   
+--    nat-* {a} {b} {c} = record { TMap = λ z f → ≅→ (*-iso a b c z) f  ; isNTrans = record { commute = nat-comm } } where
+--       nat-comm : {x y : Obj opA} {f : Hom opA x y} → 
+--            Sets [ Sets [ (λ g → opA [ f o proj₁ g ] , opA [ f o proj₂ g ]) o (λ f₁ → ≅→ (*-iso a b c x) f₁) ]
+--               ≈  Sets [ (λ f₁ → ≅→ (*-iso a b c y) f₁) o (λ g → opA [ f o g ])  ]  ]
+--       nat-comm {x} {y} {f} g =  cong₂ _,_ (  ≡←≈  A ( begin
+--          proj₁ (≅→ (*-iso a b c x) g) o f ≈⟨ ? ⟩
+--          proj₁ (≅→ (*-iso a b c y) (A [ g o f ]))  ∎ )) (  ≡←≈ A  ( begin
+--          ? ≈⟨ ? ⟩
+--          ? ∎ )) where
+--            open ≈-Reasoning A
+-- 
 
 
 -- end
--- a/src/system-f.agda	Mon Oct 09 17:00:17 2023 +0900
+++ b/src/system-f.agda	Fri Nov 24 08:49:21 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --universe-polymorphism #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 open import Level
 open import Relation.Binary.PropositionalEquality