# HG changeset patch # User Shinji KONO # Date 1700783361 -32400 # Node ID 0e750446e463864c986d3d24cfe0f3474e91bba0 # Parent 73c72679421c7c00e985ebcf95002832e0d857e3 ... diff -r 73c72679421c -r 0e750446e463 src/Definitions.agda --- 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 diff -r 73c72679421c -r 0e750446e463 src/SetsCompleteness.agda --- 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 Γ diff -r 73c72679421c -r 0e750446e463 src/freyd.agda --- 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 ) diff -r 73c72679421c -r 0e750446e463 src/freyd2.agda --- 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 diff -r 73c72679421c -r 0e750446e463 src/system-f.agda --- 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