Mercurial > hg > Members > kono > Proof > category
changeset 1124:f683d96fbc93 default tip
safe fix done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Jul 2024 22:28:50 +0900 |
| parents | b6ab443f7a43 |
| children | |
| files | src/Ch0101.agda src/SetsCompleteness.agda src/ToposEx.agda src/adj-monad.agda src/category-ex.agda src/epi.agda src/free-monoid.agda src/list-level.agda src/list-monoid-cat.agda src/list-nat.agda src/list-nat0.agda src/list.agda src/maybeCat.agda src/monad→monoidal.agda src/negnat.agda src/representable.agda src/yoneda.agda |
| diffstat | 17 files changed, 316 insertions(+), 356 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Ch0101.agda Sun Jul 07 22:28:50 2024 +0900 @@ -0,0 +1,87 @@ +{-# OPTIONS --cubical-compatible --safe #-} + +module Ch0101 where +open import Category +open import Category.Sets +open import Category.Rel +open import Level +open import Relation.Binary +open import Relation.Binary.Core + +GObj : ∀{ℓ} → Set ℓ → RelObj ℓ +GObj a = a + +data GMap {ℓ} {A B : Set ℓ} (f : A → B) (x : A) : B → Set (suc ℓ) where + Graph : GMap f x (f x) + +GraphFunctor : ∀{ℓ} → Functor (Sets {ℓ}) (Rels {ℓ}) +GraphFunctor {ℓ} = record { FObj = GObj + ; FMap = GMap + ; isFunctor = isFunctor + } + where + isFunctor : IsFunctor (Sets {ℓ}) (Rels {ℓ}) GObj GMap + isFunctor = record { ≈-cong = ≈-cong + ; identity = identity + ; distr = distr + } + where + ≈-cong : {A B : Set ℓ} → {φ ψ : A → B} → φ == ψ → GMap φ ≈ GMap ψ + ≈-cong {A} {B} {φ} {ψ} eq = exactly (λ g → ?) ? + identity : {A : Set ℓ} → GMap (λ x → x) ≈ RelId {A = A} + identity {A} = exactly lhs rhs + where + lhs : {i j : A} → GMap (λ x → x) i j → RelId i j + lhs {i} {.i} Graph = ReflRel + rhs : {i j : A} → RelId i j -> GMap (λ x → x) i j + rhs {i} {.i} ReflRel = Graph + distr : {A B C : Set ℓ} {φ : A → B} {ψ : B → C} + → (GMap (λ x → ψ ( φ x))) ≈ (GMap ψ ∘ GMap φ) + distr {A} {B} {C} {φ} {ψ} = exactly ? ? -- lhs rhs + -- where + -- lhs : {i : A} {k : C} → GMap (λ x → ψ ( φ x)) ≈ (GMap ψ ∘ GMap φ) i k → (GMap ψ ∘ GMap φ) i k + -- lhs {i} .{ψ (φ i)} Graph = Comp {a = Graph} {b = Graph} + -- rhs : {i : A} {k : C} → (GMap ψ ∘ GMap φ) i k → GMap (λ x → ψ ( φ x)) i k + -- rhs {i} .{ψ (φ i)} (Comp {a = Graph} {Graph}) = Graph + +OpObj : ∀{ℓ} → RelObj ℓ → RelObj ℓ +OpObj x = x + +data OpMap {ℓ} {A B : RelObj ℓ} (P : A -Rel⟶ B) (b : B) (a : A) : Set (suc ℓ) where + complement : P a b → OpMap P b a + +ComplementFunctor : ∀{ℓ} → Functor (Category.op (Rels {ℓ})) (Rels {ℓ}) +ComplementFunctor {ℓ} = record { FObj = OpObj + ; FMap = OpMap + ; isFunctor = isFunctor + } + where + isFunctor : IsFunctor (Category.op (Rels {ℓ})) (Rels {ℓ}) OpObj OpMap + isFunctor = record { ≈-cong = ≈-cong + ; identity = identity + ; distr = distr + } + where + ≈-cong : {A B : Set ℓ} {P Q : B -Rel⟶ A} → P ≈ Q → OpMap P ≈ OpMap Q + ≈-cong {A} {B} {P} {Q} (exactly P⇒Q Q⇒P) = exactly lhs rhs + where + lhs : {i : A} {j : B} → OpMap P i j → OpMap Q i j + lhs (complement Pji) = complement (P⇒Q Pji) + rhs : {i : A} {j : B} → OpMap Q i j → OpMap P i j + rhs (complement Qji) = complement (Q⇒P Qji) + + identity : {A : Set ℓ} → OpMap (RelId {A = A}) ≈ RelId {A = OpObj A} + identity {A} = exactly lhs rhs + where + lhs : {i j : A} → OpMap RelId i j → RelId i j + lhs {i} .{i} (complement ReflRel) = ReflRel + rhs : {i j : A} → RelId i j → OpMap RelId i j + rhs {i} .{i} ReflRel = complement ReflRel + + distr : {A B C : Set ℓ} {P : B -Rel⟶ A} {Q : C -Rel⟶ B} → OpMap (P ∘ Q) ≈ (OpMap Q ∘ OpMap P) + distr {A} {B} {C} {P} {Q} = exactly lhs rhs + where + lhs : {i : A} {k : C} → OpMap (P ∘ Q) i k → (OpMap Q ∘ OpMap P) i k + lhs {i} {k} (complement (Comp {a = Pjk} {Qij} ))= Comp {a = complement Qij} {b = complement Pjk} + rhs : {i : A} {k : C} → (OpMap Q ∘ OpMap P) i k → OpMap (P ∘ Q) i k + rhs {i} {k} (Comp {a = complement Qij} {b = complement Pjk}) = complement (Comp {a = Pjk} {Qij})
--- a/src/SetsCompleteness.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/SetsCompleteness.agda Sun Jul 07 22:28:50 2024 +0900 @@ -56,7 +56,7 @@ open import Axiom.Extensionality.Propositional SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) - → Extensionality c₂ c₂ + → Extensionality c₂ c₂ -- cannot avoid this here → IProduct I ( Sets { c₂} ) ai SetsIProduct {c₂} I fi ext = record { iprod = iproduct I fi
--- a/src/ToposEx.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/ToposEx.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,5 +1,5 @@ -{-# OPTIONS --cubical-compatible --safe #-} --- {-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --allow-unsolved-metas #-} +-- {-# OPTIONS --cubical-compatible --safe #-} -- {-# OPTIONS --cubical-compatible #-}
--- a/src/adj-monad.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/adj-monad.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,10 +1,3 @@ --- Monad --- Category A --- A = Category --- Functor T : A → A ---T(a) = t(a) ---T(f) = tf(f) - {-# OPTIONS --cubical-compatible --safe #-} open import Category -- https://github.com/konn/category-agda @@ -22,6 +15,13 @@ -- ---- +-- Monad +-- Category A +-- A = Category +-- Functor T : A → A +--T(a) = t(a) +--T(f) = tf(f) + open NTrans open Functor
--- a/src/category-ex.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/category-ex.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,20 +1,16 @@ --- {-# OPTIONS --cubical-compatible --safe #-} +{-# OPTIONS --cubical-compatible --safe #-} module category-ex where open import Level open import Category -postulate c₁ c₂ ℓ : Level -postulate A : Category c₁ c₂ ℓ + +module _ {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a b c : Obj A) (g : Hom A a b) (f : Hom A b c) where -postulate a b c : Obj A -postulate g : Hom A a b -postulate f : Hom A b c + open Category.Category -open Category.Category + h = _o_ A f g -h = _o_ A f g - -i = A [ f o g ] + i = A [ f o g ]
--- a/src/epi.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/epi.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical-compatible --safe #-} open import Category -- https://github.com/konn/category-agda open import Level @@ -138,29 +139,29 @@ epi : {a b c : FourObject } (f₁ f₂ : Hom FourCat a b ) ( h : Hom FourCat b c ) → h ・ f₁ ≡ h ・ f₂ → f₁ ≡ f₂ -epi id-ta id-ta _ refl = refl -epi id-tb id-tb _ refl = refl -epi id-tc id-tc _ refl = refl -epi id-td id-td _ refl = refl -epi arrow-ca arrow-ca _ refl = refl -epi arrow-ab arrow-ab _ refl = refl -epi arrow-bd arrow-bd _ refl = refl -epi arrow-cb arrow-cb _ refl = refl -epi arrow-ad arrow-ad _ refl = refl -epi arrow-cd arrow-cd _ refl = refl +epi id-ta id-ta _ eq = refl +epi id-tb id-tb _ eq = refl +epi id-tc id-tc _ eq = refl +epi id-td id-td _ eq = refl +epi arrow-ca arrow-ca _ eq = refl +epi arrow-ab arrow-ab _ eq = refl +epi arrow-bd arrow-bd _ eq = refl +epi arrow-cb arrow-cb _ eq = refl +epi arrow-ad arrow-ad _ eq = refl +epi arrow-cd arrow-cd _ eq = refl monic : {a b c : FourObject } (g₁ g₂ : Hom FourCat b c ) ( h : Hom FourCat a b ) → g₁ ・ h ≡ g₂ ・ h → g₁ ≡ g₂ -monic id-ta id-ta _ refl = refl -monic id-tb id-tb _ refl = refl -monic id-tc id-tc _ refl = refl -monic id-td id-td _ refl = refl -monic arrow-ca arrow-ca _ refl = refl -monic arrow-ab arrow-ab _ refl = refl -monic arrow-bd arrow-bd _ refl = refl -monic arrow-cb arrow-cb _ refl = refl -monic arrow-ad arrow-ad _ refl = refl -monic arrow-cd arrow-cd _ refl = refl +monic id-ta id-ta _ eq = refl +monic id-tb id-tb _ eq = refl +monic id-tc id-tc _ eq = refl +monic id-td id-td _ eq = refl +monic arrow-ca arrow-ca _ eq = refl +monic arrow-ab arrow-ab _ eq = refl +monic arrow-bd arrow-bd _ eq = refl +monic arrow-cb arrow-cb _ eq = refl +monic arrow-ad arrow-ad _ eq = refl +monic arrow-cd arrow-cd _ eq = refl open import Definitions open import Relation.Nullary
--- a/src/free-monoid.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/free-monoid.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,14 +1,14 @@ --- Free Monoid and it's Universal Mapping ----- using Sets and forgetful functor - --- Shinji KONO <kono@ie.u-ryukyu.ac.jp> - {-# OPTIONS --cubical-compatible --safe #-} open import Category -- https://github.com/konn/category-agda open import Level module free-monoid { c c₁ c₂ ℓ : Level } where +-- Free Monoid and it's Universal Mapping +---- using Sets and forgetful functor + +-- Shinji KONO <kono@ie.u-ryukyu.ac.jp> + open import Category.Sets hiding (_==_) open import Category.Cat open import HomReasoning @@ -110,32 +110,28 @@ M-id = record { morph = λ x → x ; identity = refl ; homo = refl } _==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c -_==_ f g = morph f ≡ morph g - --- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming ) --- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) --- postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c +_==_ {a} f g = (x : Carrier a) → morph f x ≡ morph g x isMonoids : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id) isMonoids = record { isEquivalence = isEquivalence1 - ; identityL = refl - ; identityR = refl - ; associative = refl + ; identityL = λ {a} {b} {f} x → refl + ; identityR = λ {a} {b} {f} x → refl + ; associative = λ x → refl ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} } where isEquivalence1 : { a b : ≡-Monoid } → IsEquivalence {_} {_} {Monomorph a b} _==_ isEquivalence1 = -- this is the same function as A's equivalence but has different types - record { refl = refl - ; sym = sym - ; trans = trans + record { refl = λ x → refl + ; sym = λ {s} {t} s=t y → sym ( s=t y ) + ; trans = λ a=b b=c x → trans (a=b x) (b=c x) } o-resp-≈ : {a b c : ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → f == g → h == i → (h + f) == (i + g) - o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ≡-Reasoning in begin - morph ( h + f ) - ≡⟨ ≡-cong ( λ g → ( ( λ (x : Carrier a ) → g x ) )) ? ⟩ -- (extensionality (Sets ) {Carrier a} lemma11) ⟩ - morph ( i + g ) + o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i x = let open ≡-Reasoning in begin + morph ( h + f ) x + ≡⟨ lemma11 x ⟩ + morph ( i + g ) x ∎ where lemma11 : (x : Carrier a) → morph (h + f) x ≡ morph (i + g) x @@ -143,9 +139,9 @@ morph ( h + f ) x ≡⟨⟩ morph h ( ( morph f ) x ) - ≡⟨ ≡-cong ( \y -> morph h ( y x ) ) f==g ⟩ + ≡⟨ ≡-cong ( λ y → morph h y ) ( f==g x) ⟩ morph h ( morph g x ) - ≡⟨ ≡-cong ( \y -> y ( morph g x ) ) h==i ⟩ + ≡⟨ h==i _ ⟩ morph i ( morph g x ) ≡⟨⟩ morph ( i + g ) x @@ -164,20 +160,17 @@ ; isCategory = isMonoids } -A = Sets {c} -B = Monoids - open Functor -U : Functor B A +U : Functor Monoids Sets U = record { FObj = λ m → Carrier m ; FMap = λ f → morph f ; isFunctor = record { - ≈-cong = λ x → x - ; identity = refl - ; distr = refl - } + ≈-cong = λ f=g x → f=g x + ; identity = λ {a} x → refl + ; distr = λ {a b c} {f} {g} x → refl + } } -- FObj @@ -193,17 +186,17 @@ ; identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) } } -Generator : Obj A → Obj B +Generator : Obj Sets → Obj Monoids Generator s = list s -- solution -- [a,b,c] → f(a) ∙ f(b) ∙ f(c) -Φ : {a : Obj A } {b : Obj B} ( f : Hom A a (FObj U b) ) → List a → Carrier b +Φ : {a : Obj Sets } {b : Obj Monoids} ( f : Hom Sets a (FObj U b) ) → List a → Carrier b Φ {a} {b} f [] = ε b Φ {a} {b} f ( x :: xs ) = b < ( f x ) ∙ (Φ {a} {b} f xs ) > -solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) → Hom B (Generator a ) b +solution : (a : Obj Sets ) (b : Obj Monoids) ( f : Hom Sets a (FObj U b) ) → Hom Monoids (Generator a ) b solution a b f = record { morph = λ (l : List a) → Φ f l ; identity = refl; @@ -230,10 +223,10 @@ Φ {a} {b} f ((Generator a) < ( x :: xs) ∙ y > ) ∎ ) -eta : (a : Obj A) → Hom A a ( FObj U (Generator a) ) +eta : (a : Obj Sets) → Hom Sets a ( FObj U (Generator a) ) eta a = λ ( x : a ) → x :: [] -FreeMonoidUniveralMapping : UniversalMapping A B U +FreeMonoidUniveralMapping : UniversalMapping Sets Monoids U FreeMonoidUniveralMapping = record { F = Generator ; @@ -244,30 +237,19 @@ uniquness = λ {a b f g} → uniquness {a} {b} {f} {g} } } where - universalMapping : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → ? -- FMap U ( solution a b f ) o eta a ≡ f - universalMapping {a} {b} {f} = + universalMapping : {a : Obj Sets } {b : Obj Monoids} { f : Hom Sets a (FObj U b) } → Sets [ Sets [ Φ {a} {b} f o eta a ] ≈ f ] + universalMapping {a} {b} {f} x = begin - FMap U ( solution a b f ) o eta a - ≡⟨ refl ⟩ - ( λ (x : a ) → Φ {a} {b} f (eta a x) ) - ≡⟨ refl ⟩ - ( λ (x : a ) → Φ {a} {b} f ( x :: [] ) ) - ≡⟨ refl ⟩ - ( λ (x : a ) → b < ( f x ) ∙ (Φ {a} {b} f [] ) > ) - ≡⟨ refl ⟩ - ( λ (x : a ) → b < ( f x ) ∙ ( ε b ) > ) - ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality A {a} lemma-ext1) ⟩ - ( λ (x : a ) → f x ) - ≡⟨ refl ⟩ - f + Φ {a} {b} f ( eta a x) ≡⟨⟩ + b < f x ∙ ε b > ≡⟨ lemma-ext1 x ⟩ + f x ∎ where open ≡-Reasoning lemma-ext1 : ∀( x : a ) → b < ( f x ) ∙ ( ε b ) > ≡ f x lemma-ext1 x = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x) - uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → - { g : Hom B (Generator a) b } → (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ] - uniquness {a} {b} {f} {g} eq = - extensionality A lemma-ext2 where + uniquness : {a : Obj Sets } {b : Obj Monoids} { f : Hom Sets a (FObj U b) } → + { g : Hom Monoids (Generator a) b } → Sets [ Sets [ morph g o eta a ] ≈ f ] → Monoids [ solution a b f ≈ g ] + uniquness {a} {b} {f} {g} eq x = lemma-ext2 x where lemma-ext2 : ( ∀( x : List a ) → (morph ( solution a b f)) x ≡ (morph g) x ) -- (morph ( solution a b f)) [] ≡ (morph g) [] ) lemma-ext2 [] = let open ≡-Reasoning in @@ -279,73 +261,60 @@ (morph g) [] ∎ lemma-ext2 (x :: xs) = let open ≡-Reasoning in - begin - (morph ( solution a b f)) ( x :: xs ) + begin (morph ( solution a b f)) ( x :: xs ) ≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩ b < ((morph ( solution a b f)) ( x :: []) ) ∙ ((morph ( solution a b f)) xs ) > ≡⟨ ≡-cong ( λ k → (b < ((morph ( solution a b f)) ( x :: []) ) ∙ k > )) (lemma-ext2 xs ) ⟩ b < ((morph ( solution a b f)) ( x :: []) ) ∙((morph g) ( xs )) > - ≡⟨ ≡-cong ( λ k → ( b < ( k x ) ∙ ((morph g) ( xs )) > )) ( + ≡⟨ ≡-cong ( λ k → ( b < k ∙ ((morph g) ( xs )) > )) ( begin - ( λ x → (morph ( solution a b f)) ( x :: [] ) ) - ≡⟨ extensionality A {a} lemma-ext3 ⟩ - ( λ x → (morph g) ( x :: [] ) ) + morph ( solution a b f) ( x :: [] ) + ≡⟨ lemma-ext3 x ⟩ + morph g ( x :: [] ) ∎ ) ⟩ b < ((morph g) ( x :: [] )) ∙((morph g) ( xs )) > ≡⟨ sym ( homo g ) ⟩ (morph g) ( x :: xs ) ∎ where - lemma-ext3 : ∀( x : a ) → (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] ) - lemma-ext3 x = let open ≡-Reasoning in - begin - (morph ( solution a b f)) (x :: []) - ≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩ - f x - ≡⟨ sym ( ≡-cong (λ f → f x ) eq ) ⟩ - (morph g) ( x :: [] ) - ∎ + lemma-ext3 : ∀( x : a ) → (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] ) + lemma-ext3 x = let open ≡-Reasoning in + begin + (morph ( solution a b f)) (x :: []) + ≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩ + f x + ≡⟨ sym (eq x) ⟩ + (morph g) ( x :: [] ) + ∎ open NTrans -- fm-ε b = Φ -fm-ε : NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor -fm-ε = nat-ε A B FreeMonoidUniveralMapping --- TMap = λ a → solution (FObj U a) a (λ x → x ) ; --- isNTrans = record { --- commute = commute1 --- } --- } where --- commute1 : {a b : Obj B} {f : Hom B a b} → let open ≈-Reasoning B renaming (_o_ to _*_ ) in --- ( FMap (identityFunctor {_} {_} {_} {B}) f * solution (FObj U a) a (λ x → x) ) ≈ --- ( solution (FObj U b) b (λ x → x) * FMap (FunctorF A B FreeMonoidUniveralMapping ○ U) f ) --- commute1 {a} {b} {f} = let open ≡-Reasoning in begin --- morph ((B ≈-Reasoning.o FMap identityFunctor f) (solution (FObj U a) a (λ x → x))) --- ≡⟨ {!!} ⟩ --- morph ((B ≈-Reasoning.o solution (FObj U b) b (λ x → x)) (FMap (FunctorF A B FreeMonoidUniveralMapping ○ U) f)) --- ∎ +fm-ε : NTrans Monoids Monoids ( ( FunctorF Sets Monoids FreeMonoidUniveralMapping) ○ U) identityFunctor +fm-ε = nat-ε Sets Monoids FreeMonoidUniveralMapping - -fm-η : NTrans A A identityFunctor ( U ○ ( FunctorF A B FreeMonoidUniveralMapping) ) +fm-η : NTrans Sets Sets identityFunctor ( U ○ ( FunctorF Sets Monoids FreeMonoidUniveralMapping) ) fm-η = record { TMap = λ a → λ (x : a) → x :: [] ; isNTrans = record { commute = commute1 } } where - commute1 : {a b : Obj A} {f : Hom A a b} → let open ≈-Reasoning A renaming (_o_ to _*_ ) in - (( FMap (U ○ FunctorF A B FreeMonoidUniveralMapping) f ) * (λ x → x :: []) ) ≈ ( (λ x → x :: []) * (λ z → FMap (identityFunctor {_} {_} {_} {A}) f z ) ) - commute1 {a} {b} {f} = refl -- λ (x : a ) → f x :: [] + commute1 : {a b : Obj Sets} {f : Hom Sets a b} → let open ≈-Reasoning Sets renaming (_o_ to _*_ ) in + (( FMap (U ○ FunctorF Sets Monoids FreeMonoidUniveralMapping) f ) * (λ x → x :: []) ) ≈ ( (λ x → x :: []) * (λ z → FMap (identityFunctor {_} {_} {_} {Sets}) f z ) ) + commute1 {a} {b} {f} x = begin + morph (solution a (list b) (λ y → (f y :: []))) ((λ x₁ → x₁ :: []) x) ≡⟨ refl ⟩ + (λ x₁ → x₁ :: []) (f x) ∎ where open ≡-Reasoning --- A = Sets {c} --- B = Monoids +-- Sets = Sets {c} +-- Monoids = Monoids -- U underline funcotr -- F generator = x :: [] -- Eta x :: [] -- Epsiron morph = Φ -adj = UMAdjunction A B U FreeMonoidUniveralMapping +adj = UMAdjunction Sets Monoids U FreeMonoidUniveralMapping
--- a/src/list-level.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/list-level.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,19 +1,16 @@ -module list-level where - -open import Level - +{-# OPTIONS --cubical-compatible --safe #-} -postulate A : Set -postulate B : Set -postulate C : Set - -postulate a : A -postulate b : A -postulate c : A +open import Level +module list-level (A B C : Set) where + +data A3 : Set where + a0 : A3 + b0 : A3 + c0 : A3 infixr 40 _::_ -data List {a} (A : Set a) : Set a where +data List {l : Level} (A : Set l) : Set l where [] : List A _::_ : A → List A → List A @@ -23,8 +20,8 @@ [] ++ ys = ys (x :: xs) ++ ys = x :: (xs ++ ys) -l1 = a :: [] -l2 = a :: b :: a :: c :: [] +l1 = a0 :: [] +l2 = a0 :: b0 :: a0 :: c0 :: [] l3 = l1 ++ l2 @@ -41,7 +38,7 @@ flatten ( leaf a ) = a :: [] flatten ( node a b ) = flatten a ++ flatten b -n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c )) +n1 = node ( leaf a0 ) ( node ( leaf b0 ) ( leaf c0 )) open import Relation.Binary.PropositionalEquality @@ -79,7 +76,7 @@ module ==-Reasoning {n} (A : Set n ) where - infixr 2 _∎ + infixr 3 _∎ infixr 2 _==⟨_⟩_ _==⟨⟩_ infix 1 begin_
--- a/src/list-monoid-cat.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/list-monoid-cat.agda Sun Jul 07 22:28:50 2024 +0900 @@ -4,6 +4,8 @@ open import Level open import HomReasoning open import Definitions +open import Relation.Binary + module list-monoid-cat (c : Level ) where @@ -47,12 +49,12 @@ o-resp-≈ : {A : Set} → {f g : List A } → {h i : List A } → f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) o-resp-≈ {A} refl refl = refl - isEquivalence1 : {A : Set} → ? -- IsEquivalence {_} {_} {List A } _≡_ - isEquivalence1 {A} = ? -- this is the same function as A's equivalence but has different types - -- record { refl = refl - -- ; sym = sym - -- ; trans = trans - -- } + isEquivalence1 : {A : Set} → IsEquivalence {_} {_} {List A } _≡_ + isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types + record { refl = refl + ; sym = sym + ; trans = trans + } ListCategory : (A : Set) → Category _ _ _ ListCategory A = record { Obj = ListObj @@ -91,12 +93,12 @@ o-resp-≈ : {M : ≡-Monoid c} → {f g : Carrier M } → {h i : Carrier M } → f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g) o-resp-≈ {A} refl refl = refl - isEquivalence1 : {M : ≡-Monoid c} → ? -- IsEquivalence {_} {_} {Carrier M } _≡_ - isEquivalence1 {A} = ? -- this is the same function as A's equivalence but has different types - -- record { refl = refl - -- ; sym = sym - -- ; trans = trans - -- } + isEquivalence1 : {M : ≡-Monoid c} → IsEquivalence {_} {_} {Carrier M } _≡_ + isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types + record { refl = refl + ; sym = sym + ; trans = trans + } MonoidCategory : (M : ≡-Monoid c) → Category _ _ _ MonoidCategory M = record { Obj = MonoidObj
--- a/src/list-nat.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/list-nat.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,13 +1,12 @@ -module list-nat where - +{-# OPTIONS --cubical-compatible --safe #-} + open import Level - +module list-nat where -postulate A : Set - -postulate a : A -postulate b : A -postulate c : A +data A : Set where + a : A + b : A + c : A infixr 40 _::_ @@ -31,8 +30,8 @@ node : Node A → Node A → Node A flatten : { A : Set } → Node A → List A -flatten ( leaf a ) = a :: [] -flatten ( node a b ) = flatten a ++ flatten b +flatten ( leaf x ) = x :: [] +flatten ( node x y ) = flatten x ++ flatten y n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c )) @@ -47,8 +46,8 @@ ( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y cong1 f reflection = reflection -eq-cons : {A : Set } {x y : List A} ( a : A ) → x == y → ( a :: x ) == ( a :: y ) -eq-cons a z = cong1 ( λ x → ( a :: x) ) z +eq-cons : {A : Set } {x y : List A} ( w : A ) → x == y → ( w :: x ) == ( w :: y ) +eq-cons w z = cong1 ( λ x → ( w :: x) ) z trans-list : {A : Set } {x y z : List A} → x == y → y == z → x == z trans-list reflection reflection = reflection
--- a/src/list-nat0.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/list-nat0.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,11 +1,12 @@ +{-# OPTIONS --cubical-compatible --safe #-} module list-nat0 where open import Level - -postulate a : Set -postulate b : Set -postulate c : Set +data i3 : Set where + a : i3 + b : i3 + c : i3 infixr 40 _::_ @@ -59,8 +60,8 @@ ( f : A → B ) → {x : A } → {y : A} → x ≡ y → f x ≡ f y cong1 f refl = refl -lemma11 : ∀{n} → ( Set n ) IsRelatedTo ( Set n ) -lemma11 = relTo refl +-- lemma11 : ∀{n} → ( Set n ) IsRelatedTo ( Set n ) +-- lemma11 = relTo refl lemma12 : {L : Set} ( x : List L ) → x ++ x ≡ x ++ x lemma12 x = begin x ++ x ∎
--- a/src/list.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/list.agda Sun Jul 07 22:28:50 2024 +0900 @@ -9,5 +9,5 @@ l1 = [ a ] -l2 = ( a :: [] ) +l2 = ( a ∷ [] )
--- a/src/maybeCat.agda Sun Jul 07 17:05:16 2024 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,136 +0,0 @@ -{-# OPTIONS --cubical-compatible --safe #-} - -open import Category -- https://github.com/konn/category-agda -open import Level - -module maybeCat { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where - -open import Definitions -open import HomReasoning -open import Relation.Binary -open import Relation.Binary.Core -open import Relation.Binary.PropositionalEquality hiding (sym) - -open import Data.Maybe -open import Data.Empty - -open Functor - - -data MaybeHom { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) : (a b : Maybe (Obj A )) → Set (ℓ ⊔ c₂) where - hom : {a b : Obj A} → (f : Hom A a b ) → MaybeHom A (just a) (just b) - non-hom1 : {b : Obj A} → MaybeHom A (just b) nothing - non-hom2 : {b : Obj A} → MaybeHom A nothing (just b) - non-hom3 : {b : Obj A} → MaybeHom A nothing nothing - -open MaybeHom - -_+_ : { c₁ c₂ ℓ : Level} → { A : Category c₁ c₂ ℓ } → {a b c : Obj A } → MaybeHom A b c → MaybeHom A a b → MaybeHom A a c -_+_ {x} {y} {z} {A} {a} {b} {c} f g with hom f | hom g -_+_ {_} {_} {_} {A} {a} {b} {c} f g | nothing | _ = record { hom = nothing } -_+_ {_} {_} {_} {A} {a} {b} {c} f g | _ | nothing = record { hom = nothing } -_+_ {_} {_} {_} {A} {a} {b} {c} _ _ | (just f) | (just g) = record { hom = just ( A [ f o g ] ) } - -MaybeHomId : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } (a : Obj A ) → MaybeHom A a a -MaybeHomId {_} {_} {_} {A} a = record { hom = just ( id1 A a) } - -_[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → Rel (Maybe (Hom A a b)) ℓ -_[_≡≡_] A f g with f | g -... | nothing | _ = Lift _ ⊥ -... | _ | nothing = Lift _ ⊥ -... | just f | just g = A [ f ≈ g ] - - -module ≡≡-Reasoning { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) where - - infixr 2 _∎ - infixr 2 _≡≡⟨_⟩_ _≡≡⟨⟩_ - infix 1 begin_ - - ≡≡-refl : {a b : Obj A } → {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ] - ≡≡-refl {_} {_} {just x} = just refl-hom where open ≈-Reasoning (A) - ≡≡-refl {_} {_} {nothing} = nothing - - ≡≡-sym : {a b : Obj A } → {x y : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ x ] - ≡≡-sym (just x≈y) = just (sym x≈y) where open ≈-Reasoning (A) - ≡≡-sym nothing = nothing - - ≡≡-trans : {a b : Obj A } → {x y z : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ] - ≡≡-trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z) where open ≈-Reasoning (A) - ≡≡-trans nothing nothing = nothing - - ≡≡-cong : ∀{ a b c d } → ∀ {x y : Maybe (Hom A a b )} → - (f : Maybe (Hom A a b ) → Maybe (Hom A c d ) ) → x ≡ y → A [ f x ≡≡ f y ] - ≡≡-cong {a} {b } {c} {d} {nothing} {nothing} f refl = ≡≡-refl - ≡≡-cong {a} {b } {c} {d} {just x} {just .x} f refl = ≡≡-refl - - data _IsRelatedTo_ {a b : Obj A} (x y : (Maybe (Hom A a b ))) : - Set (ℓ ⊔ c₂) where - relTo : (x≈y : A [ x ≡≡ y ] ) → x IsRelatedTo y - - begin_ : {a b : Obj A} {x : Maybe (Hom A a b ) } {y : Maybe (Hom A a b )} → - x IsRelatedTo y → A [ x ≡≡ y ] - begin relTo x≈y = x≈y - - _≡≡⟨_⟩_ : {a b : Obj A} (x : Maybe (Hom A a b )) {y z : Maybe (Hom A a b ) } → - A [ x ≡≡ y ] → y IsRelatedTo z → x IsRelatedTo z - _ ≡≡⟨ x≈y ⟩ relTo y≈z = relTo (≡≡-trans x≈y y≈z) - - _≡≡⟨⟩_ : {a b : Obj A} (x : Maybe (Hom A a b )) {y : Maybe (Hom A a b )} - → x IsRelatedTo y → x IsRelatedTo y - _ ≡≡⟨⟩ x≈y = x≈y - - _∎ : {a b : Obj A} (x : Maybe (Hom A a b )) → x IsRelatedTo x - _∎ _ = relTo ≡≡-refl - - - - -MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂) -MaybeCat { c₁} {c₂} {ℓ} ( A ) = record { - Obj = Maybe (Obj A) ; - Hom = λ a b → MaybeHom A a b ; - _o_ = _+_ ; - _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ; - Id = λ {a} → MaybeHomId a ; - isCategory = record { - isEquivalence = let open ≡≡-Reasoning (A) in record {refl = ≡≡-refl ; trans = ≡≡-trans ; sym = ≡≡-sym } ; - identityL = λ {a b f} → identityL {a} {b} {f} ; - identityR = λ {a b f} → identityR {a} {b} {f}; - o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; - associative = λ {a b c d f g h } → associative {a } { b } { c } { d } { f } { g } { h } - } - } where - identityL : { a b : Obj A } { f : MaybeHom A a b } → A [ hom (MaybeHomId b + f) ≡≡ hom f ] - identityL {a} {b} {f} with hom f - identityL {a} {b} {_} | nothing = nothing - identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A ) {a} {b} {f} ) - - identityR : { a b : Obj A } { f : MaybeHom A a b } → A [ hom (f + MaybeHomId a ) ≡≡ hom f ] - identityR {a} {b} {f} with hom f - identityR {a} {b} {_} | nothing = nothing - identityR {a} {b} {_} | just f = just ( IsCategory.identityR ( Category.isCategory A ) {a} {b} {f} ) - - o-resp-≈ : {a b c : Obj A} → {f g : MaybeHom A a b } → {h i : MaybeHom A b c } → - A [ hom f ≡≡ hom g ] → A [ hom h ≡≡ hom i ] → A [ hom (h + f) ≡≡ hom (i + g) ] - o-resp-≈ {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi with hom f | hom g | hom h | hom i - o-resp-≈ {a} {b} {c} {_} {_} {_} {_} (just eq-fg) (just eq-hi) | just f | just g | just h | just i = - just ( IsCategory.o-resp-≈ ( Category.isCategory A ) {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi ) - o-resp-≈ {a} {b} {c} {f} {g} {h} {i} (just _) nothing | just _ | just _ | nothing | nothing = nothing - o-resp-≈ {a} {b} {c} {f} {g} {h} {i} nothing (just _) | nothing | nothing | just _ | just _ = nothing - o-resp-≈ {a} {b} {c} {f} {g} {h} {i} nothing nothing | nothing | nothing | nothing | nothing = nothing - - - associative : {a b c d : Obj A} → {f : MaybeHom A c d } → {g : MaybeHom A b c } → {h : MaybeHom A a b } → - A [ hom (f + (g + h)) ≡≡ hom ((f + g) + h) ] - associative {_} {_} {_} {_} {f} {g} {h} with hom f | hom g | hom h - associative {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ = nothing - associative {_} {_} {_} {_} {f} {g} {h} | just _ | nothing | _ = nothing - associative {_} {_} {_} {_} {f} {g} {h} | just _ | just _ | nothing = nothing - associative {a} {b} {c} {d} {_} {_} {_} | just f | just g | just h = - just ( IsCategory.associative ( Category.isCategory A ) {a} {b} {c} {d} {f} {g} {h} ) - -≈-to-== : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → { a b : Obj A } - { f g : Hom A a b } → - A [ f ≈ g ] → (MaybeCat A) [ record { hom = just f } ≈ record { hom = just g } ] -≈-to-== A {a} {b} {f} {g} f≈g = just f≈g
--- a/src/monad→monoidal.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/monad→monoidal.agda Sun Jul 07 22:28:50 2024 +0900 @@ -64,9 +64,6 @@ fcong : {b c : Obj (Sets {l})} → {f g : Hom (Sets {l}) b c } → (x : FObj T b) → ((x : b) → f x ≡ g x) → FMap T f x ≡ FMap T g x fcong x eq = IsFunctor.≈-cong (isFunctor T) eq x - fcong₂ : {b c : Obj (Sets {l})} → {f g : Hom (Sets {l}) b c } → (x y : FObj T b) - → ((x : b) → f x ≡ g x) → x ≡ y → FMap T f x ≡ FMap T g y - fcong₂ x x eq refl = IsFunctor.≈-cong (isFunctor T) eq x natφ : { a b c d : Obj Sets } { x : FObj T a} { y : FObj T b} { f : a → c } { g : b → d } → FMap T (map f g) (φ (x , y)) ≡ φ (FMap T f x , FMap T g y) natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin @@ -144,39 +141,49 @@ id1 Sets (FObj T a) x ≡⟨ refl ⟩ x ∎ -Monad→Applicative : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m ) -Monad→Applicative {l} monad = record { - pure = pure - ; <*> = _<*>_ - ; isApplicative = record { - identity = identity - ; composition = composition - ; homomorphism = homomorphism - ; interchange = interchange - } - } where - F = Monad.T monad - isM = Monoidal.isMonoidal ( MonoidalSets {l} ) - η = NTrans.TMap (Monad.η monad ) - μ = NTrans.TMap (Monad.μ monad) - pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) - pure {a} = η a - _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b - _<*>_ {a} {b} f x = ( NTrans.TMap (Monad.μ monad ) b ) ( (FMap F (λ k → FMap F k x )) f ) - open IsMonoidal - id : { a : Obj (Sets {l}) } → a → a - id x = x - ≡cong = Relation.Binary.PropositionalEquality.cong - identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u - identity {a} {u} = ? - composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a } - → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) - composition {a} {b} {c} {u} {v} {w} = ? - homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) - homomorphism {a} {b} {f} {x} = ? - interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u - interchange {a} {b} {u} {x} = ? - +-- Someday... +-- +-- Monad→Applicative : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m ) +-- Monad→Applicative {l} monad = record { +-- pure = pure +-- ; <*> = _<*>_ +-- ; isApplicative = record { +-- identity = identity +-- ; composition = composition +-- ; homomorphism = homomorphism +-- ; interchange = interchange +-- } +-- } where +-- open Monad monad +-- isM = Monoidal.isMonoidal (MonoidalSets {l} ) +-- unit : FObj T One +-- unit = TMap η One OneObj +-- φ : {a b : Obj Sets} → Hom Sets ((FObj T a) * (FObj T b )) ( FObj T ( a * b ) ) +-- φ {a} {b} (x , y) = TMap μ (a * b) (FMap T ( λ f → FMap T ( λ g → ( f , g )) y ) x ) +-- open IsMonoidal +-- id : { a : Obj (Sets {l}) } → a → a +-- id x = x +-- fdistr : {a b c : Obj (Sets {l})} → {f : Hom (Sets {l}) b c } {g : Hom (Sets {l} ) a b } → (x : FObj T a) +-- → FMap T (λ z → f (g z)) x ≡ FMap T f ( FMap T g x ) +-- fdistr x = IsFunctor.distr (isFunctor T) x +-- fcong : {b c : Obj (Sets {l})} → {f g : Hom (Sets {l}) b c } → (x : FObj T b) +-- → ((x : b) → f x ≡ g x) → FMap T f x ≡ FMap T g x +-- fcong x eq = IsFunctor.≈-cong (isFunctor T) eq x +-- +-- pure : {a : Obj Sets} → Hom Sets a ( FObj T a ) +-- pure {a} = TMap η a +-- _<*>_ : {a b : Obj Sets} → FObj T ( a → b ) → FObj T a → FObj T b +-- _<*>_ {a} {b} f x = ( NTrans.TMap (Monad.μ monad ) b ) ( (FMap T (λ k → FMap T k x )) f ) +-- identity : { a : Obj Sets } { u : FObj T a } → pure ( id1 Sets a ) <*> u ≡ u +-- identity {a} {u} = ? +-- composition : { a b c : Obj Sets } { u : FObj T ( b → c ) } { v : FObj T (a → b ) } { w : FObj T a } +-- → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) +-- composition {a} {b} {c} {u} {v} {w} = ? +-- homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) +-- homomorphism {a} {b} {f} {x} = ? +-- interchange : { a b : Obj Sets } { u : FObj T ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u +-- interchange {a} {b} {u} {x} = ? +-- -- an easy one ( we already have HaskellMonoidal→Applicative ) Monad→Applicative' : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m )
--- a/src/negnat.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/negnat.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,13 +1,14 @@ +{-# OPTIONS --cubical-compatible --safe #-} module negnat where open import Data.Nat -open import Relation.Nullary +open import Relation.Nullary hiding (proof) open import Data.Empty open import Data.Unit open import Data.Fin renaming ( suc to fsuc ; zero to fzero ; _+_ to _++_ ) open import Relation.Binary.Core -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality hiding (J) -- http://stackoverflow.com/questions/22580842/non-trivial-negation-in-agda
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/representable.agda Sun Jul 07 22:28:50 2024 +0900 @@ -0,0 +1,38 @@ +{-# OPTIONS --cubical-compatible --safe #-} + +open import Category -- https://github.com/konn/category-agda +open import Level +open import Category.Sets + +module representable + where + +open import HomReasoning +open import Definitions hiding (Yoneda ; Representable ) +open import Relation.Binary.Core +open import Function +open import freyd2 + +open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ; resp ) + +-- 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 + +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₂ + +---- +-- +-- Hom ( a, - ) is Object mapping in Yoneda Functor +-- +---- + +open NTrans +open Functor +open Limit +open IsLimit +open import Category.Cat + +hom-product : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Functor A A +hom-product = ?
--- a/src/yoneda.agda Sun Jul 07 17:05:16 2024 +0900 +++ b/src/yoneda.agda Sun Jul 07 22:28:50 2024 +0900 @@ -1,5 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} --- {-# OPTIONS --cubical-compatible --safe #-} +{-# OPTIONS --cubical-compatible --safe #-} --- -- -- A → Sets^A^op : Yoneda Functor @@ -7,7 +6,6 @@ -- Nat(h_a,F) -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> ---- --- {-# OPTIONS --cubical-compatible #-} open import Level open import Category.Sets hiding (_==_)