From 0543fa1b6075b3b2f79eb3ce260e4d515640ee02 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 3 Jul 2021 09:13:51 +0100 Subject: [PATCH 1/5] Add proof that FinSetoids is cartesian --- .../Monoidal/Instance/FinSetoids.agda | 86 +++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 src/Categories/Category/Monoidal/Instance/FinSetoids.agda diff --git a/src/Categories/Category/Monoidal/Instance/FinSetoids.agda b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda new file mode 100644 index 000000000..4251e476a --- /dev/null +++ b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda @@ -0,0 +1,86 @@ +{-# OPTIONS --without-K --safe #-} + +module Categories.Category.Monoidal.Instance.FinSetoids where + +open import Data.Fin.Base +open import Data.Fin.Properties hiding (setoid) +import Data.Nat.Base as ℕ +open import Data.Product +open import Data.Product.Relation.Binary.Pointwise.NonDependent +open import Data.Unit.Polymorphic +open import Function +open import Function.Equality using (Π) +open import Level using (Lift) +open import Relation.Binary +open import Relation.Binary.Reasoning.MultiSetoid +open import Relation.Binary.PropositionalEquality + +open import Categories.Category.Cartesian +open import Categories.Category.Instance.FinSetoids +open import Categories.Category.Instance.SingletonSet + +map-cong₂ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {f g : A → B} {h i : C → D} → + f ≗ g → h ≗ i → map f h ≗ map g i +map-cong₂ p q (x , y) = cong₂ _,_ (p x) (q y) + +module _ {c ℓ} where + FinSetoids-Cartesian : Cartesian (FinSetoids c ℓ) + FinSetoids-Cartesian = record + { terminal = record + { ⊤ = record + { fst = SingletonSetoid + ; snd = 1 , record + { cong₁ = λ _ → refl + ; inverse = record + { fst = λ { zero → refl } + } + } + } + } + ; products = record + { product = λ {A} {B} → + let + module A = Σ A + module B = Σ B + in record + { A×B = record + { fst = ×-setoid A.proj₁ B.proj₁ + ; snd = proj₁ A.proj₂ ℕ.* proj₁ B.proj₂ , record + { f = uncurry combine ∘ map (Inverse.f (proj₂ A.proj₂)) (Inverse.f (proj₂ B.proj₂)) + ; f⁻¹ = map (Inverse.f⁻¹ (proj₂ A.proj₂)) (Inverse.f⁻¹ (proj₂ B.proj₂)) ∘ remQuot (proj₁ B.proj₂) + ; cong₁ = λ { (p , q) → cong₂ combine (Inverse.cong₁ (proj₂ A.proj₂) p) (Inverse.cong₁ (proj₂ B.proj₂) q) } + ; cong₂ = λ { refl → Setoid.refl (×-setoid A.proj₁ B.proj₁) } + ; inverse = record + { fst = λ x → begin⟨ setoid (Fin (proj₁ A.proj₂ ℕ.* proj₁ B.proj₂)) ⟩ + uncurry combine (map (Inverse.f (proj₂ A.proj₂) ∘ Inverse.f⁻¹ (proj₂ A.proj₂)) (Inverse.f (proj₂ B.proj₂) ∘ Inverse.f⁻¹ (proj₂ B.proj₂)) (remQuot (proj₁ B.proj₂) x)) + ≡⟨ cong (uncurry combine) (map-cong₂ (proj₁ (Inverse.inverse (proj₂ A.proj₂))) (proj₁ (Inverse.inverse (proj₂ B.proj₂))) (remQuot (proj₁ B.proj₂) x)) ⟩ + uncurry (combine {proj₁ A.proj₂} {proj₁ B.proj₂}) (remQuot (proj₁ B.proj₂) x) + ≡⟨ combine-remQuot {proj₁ A.proj₂} (proj₁ B.proj₂) x ⟩ + x ∎ + ; snd = λ x → begin⟨ ×-setoid A.proj₁ B.proj₁ ⟩ + map (Inverse.f⁻¹ (proj₂ A.proj₂)) (Inverse.f⁻¹ (proj₂ B.proj₂)) (remQuot (proj₁ B.proj₂) (uncurry combine (map (Inverse.f (proj₂ A.proj₂)) (Inverse.f (proj₂ B.proj₂)) x))) + ≈⟨ Setoid.reflexive (×-setoid A.proj₁ B.proj₁) (cong (map (Inverse.f⁻¹ (proj₂ A.proj₂)) (Inverse.f⁻¹ (proj₂ B.proj₂))) (uncurry remQuot-combine (map (Inverse.f (proj₂ A.proj₂)) (Inverse.f (proj₂ B.proj₂)) x))) ⟩ + map (Inverse.f⁻¹ (proj₂ A.proj₂) ∘ Inverse.f (proj₂ A.proj₂)) (Inverse.f⁻¹ (proj₂ B.proj₂) ∘ Inverse.f (proj₂ B.proj₂)) x + ≈⟨ proj₂ (Inverse.inverse (proj₂ A.proj₂)) (proj₁ x) , proj₂ (Inverse.inverse (proj₂ B.proj₂)) (proj₂ x) ⟩ + x ∎ + } + } + } + ; π₁ = record + { _⟨$⟩_ = proj₁ + ; cong = proj₁ + } + ; π₂ = record + { _⟨$⟩_ = proj₂ + ; cong = proj₂ + } + ; ⟨_,_⟩ = λ f g → record + { _⟨$⟩_ = < f Π.⟨$⟩_ , g Π.⟨$⟩_ > + ; cong = < Π.cong f , Π.cong g > + } + ; project₁ = λ {X} {h} {i} → Π.cong h + ; project₂ = λ {X} {h} {i} → Π.cong i + ; unique = λ {X} π₁∘h≈i π₂∘h≈j x≈y → Setoid.sym A.proj₁ (π₁∘h≈i (Setoid.sym (proj₁ X) x≈y)) , Setoid.sym B.proj₁ (π₂∘h≈j (Setoid.sym (proj₁ X) x≈y)) + } + } + } From 235e4bfe76ac062a6eb22b4fa6cc000fa4e75d19 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 4 Jul 2021 08:33:21 +0100 Subject: [PATCH 2/5] Simplify FinSetoids Cartesian proofs a bit --- .../Monoidal/Instance/FinSetoids.agda | 62 ++++++++++--------- 1 file changed, 32 insertions(+), 30 deletions(-) diff --git a/src/Categories/Category/Monoidal/Instance/FinSetoids.agda b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda index 4251e476a..60635a9ad 100644 --- a/src/Categories/Category/Monoidal/Instance/FinSetoids.agda +++ b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda @@ -9,7 +9,7 @@ open import Data.Product open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Data.Unit.Polymorphic open import Function -open import Function.Equality using (Π) +open import Function.Equality using (Π; _⟨$⟩_) open import Level using (Lift) open import Relation.Binary open import Relation.Binary.Reasoning.MultiSetoid @@ -40,47 +40,49 @@ module _ {c ℓ} where ; products = record { product = λ {A} {B} → let - module A = Σ A - module B = Σ B + A-Setoid , ∣A∣ , A-Finite = A + module A-Setoid = Setoid A-Setoid + module A-Finite = Inverse A-Finite + B-Setoid , ∣B∣ , B-Finite = B + module B-Setoid = Setoid B-Setoid + module B-Finite = Inverse B-Finite in record - { A×B = record - { fst = ×-setoid A.proj₁ B.proj₁ - ; snd = proj₁ A.proj₂ ℕ.* proj₁ B.proj₂ , record - { f = uncurry combine ∘ map (Inverse.f (proj₂ A.proj₂)) (Inverse.f (proj₂ B.proj₂)) - ; f⁻¹ = map (Inverse.f⁻¹ (proj₂ A.proj₂)) (Inverse.f⁻¹ (proj₂ B.proj₂)) ∘ remQuot (proj₁ B.proj₂) - ; cong₁ = λ { (p , q) → cong₂ combine (Inverse.cong₁ (proj₂ A.proj₂) p) (Inverse.cong₁ (proj₂ B.proj₂) q) } - ; cong₂ = λ { refl → Setoid.refl (×-setoid A.proj₁ B.proj₁) } - ; inverse = record - { fst = λ x → begin⟨ setoid (Fin (proj₁ A.proj₂ ℕ.* proj₁ B.proj₂)) ⟩ - uncurry combine (map (Inverse.f (proj₂ A.proj₂) ∘ Inverse.f⁻¹ (proj₂ A.proj₂)) (Inverse.f (proj₂ B.proj₂) ∘ Inverse.f⁻¹ (proj₂ B.proj₂)) (remQuot (proj₁ B.proj₂) x)) - ≡⟨ cong (uncurry combine) (map-cong₂ (proj₁ (Inverse.inverse (proj₂ A.proj₂))) (proj₁ (Inverse.inverse (proj₂ B.proj₂))) (remQuot (proj₁ B.proj₂) x)) ⟩ - uncurry (combine {proj₁ A.proj₂} {proj₁ B.proj₂}) (remQuot (proj₁ B.proj₂) x) - ≡⟨ combine-remQuot {proj₁ A.proj₂} (proj₁ B.proj₂) x ⟩ - x ∎ - ; snd = λ x → begin⟨ ×-setoid A.proj₁ B.proj₁ ⟩ - map (Inverse.f⁻¹ (proj₂ A.proj₂)) (Inverse.f⁻¹ (proj₂ B.proj₂)) (remQuot (proj₁ B.proj₂) (uncurry combine (map (Inverse.f (proj₂ A.proj₂)) (Inverse.f (proj₂ B.proj₂)) x))) - ≈⟨ Setoid.reflexive (×-setoid A.proj₁ B.proj₁) (cong (map (Inverse.f⁻¹ (proj₂ A.proj₂)) (Inverse.f⁻¹ (proj₂ B.proj₂))) (uncurry remQuot-combine (map (Inverse.f (proj₂ A.proj₂)) (Inverse.f (proj₂ B.proj₂)) x))) ⟩ - map (Inverse.f⁻¹ (proj₂ A.proj₂) ∘ Inverse.f (proj₂ A.proj₂)) (Inverse.f⁻¹ (proj₂ B.proj₂) ∘ Inverse.f (proj₂ B.proj₂)) x - ≈⟨ proj₂ (Inverse.inverse (proj₂ A.proj₂)) (proj₁ x) , proj₂ (Inverse.inverse (proj₂ B.proj₂)) (proj₂ x) ⟩ - x ∎ - } + { A×B = ×-setoid A-Setoid B-Setoid , ∣A∣ ℕ.* ∣B∣ , record + { f = uncurry combine ∘ map A-Finite.f B-Finite.f + ; f⁻¹ = map A-Finite.f⁻¹ B-Finite.f⁻¹ ∘ remQuot ∣B∣ + ; cong₁ = λ { (p , q) → cong₂ combine (A-Finite.cong₁ p) (B-Finite.cong₁ q) } + ; cong₂ = λ { refl → Setoid.refl (×-setoid A-Setoid B-Setoid) } + ; inverse = record + { fst = λ x → begin⟨ setoid _ ⟩ + uncurry combine (map (A-Finite.f ∘ A-Finite.f⁻¹) (B-Finite.f ∘ B-Finite.f⁻¹) (remQuot ∣B∣ x)) + ≡⟨ cong (uncurry combine) (map-cong₂ (proj₁ A-Finite.inverse) (proj₁ B-Finite.inverse) (remQuot ∣B∣ x)) ⟩ + uncurry (combine {∣A∣}) (remQuot ∣B∣ x) + ≡⟨ combine-remQuot {∣A∣} ∣B∣ x ⟩ + x ∎ + ; snd = λ x → begin⟨ ×-setoid A-Setoid B-Setoid ⟩ + map A-Finite.f⁻¹ B-Finite.f⁻¹ (remQuot ∣B∣ (uncurry combine (map A-Finite.f B-Finite.f x))) + ≡⟨ cong (map A-Finite.f⁻¹ B-Finite.f⁻¹) (uncurry remQuot-combine (map A-Finite.f B-Finite.f x)) ⟩ + map (A-Finite.f⁻¹ ∘ A-Finite.f) (B-Finite.f⁻¹ ∘ B-Finite.f) x + ≈⟨ proj₂ A-Finite.inverse (proj₁ x) , proj₂ B-Finite.inverse (proj₂ x) ⟩ + x ∎ } } ; π₁ = record { _⟨$⟩_ = proj₁ - ; cong = proj₁ + ; cong = proj₁ } ; π₂ = record { _⟨$⟩_ = proj₂ - ; cong = proj₂ + ; cong = proj₂ } ; ⟨_,_⟩ = λ f g → record - { _⟨$⟩_ = < f Π.⟨$⟩_ , g Π.⟨$⟩_ > + { _⟨$⟩_ = λ x → f ⟨$⟩ x , g ⟨$⟩ x ; cong = < Π.cong f , Π.cong g > } - ; project₁ = λ {X} {h} {i} → Π.cong h - ; project₂ = λ {X} {h} {i} → Π.cong i - ; unique = λ {X} π₁∘h≈i π₂∘h≈j x≈y → Setoid.sym A.proj₁ (π₁∘h≈i (Setoid.sym (proj₁ X) x≈y)) , Setoid.sym B.proj₁ (π₂∘h≈j (Setoid.sym (proj₁ X) x≈y)) + ; project₁ = λ {X h i} → Π.cong h + ; project₂ = λ {X h i} → Π.cong i + ; unique = λ {X} π₁∘h≈i π₂∘h≈j x≈y → + < A-Setoid.sym ∘ π₁∘h≈i , B-Setoid.sym ∘ π₂∘h≈j > (Setoid.sym (proj₁ X) x≈y) } } } From 73e13947332e0e76e72ad444eb06628cac1653d0 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 4 Jul 2021 09:12:21 +0100 Subject: [PATCH 3/5] =?UTF-8?q?Hide=20map-cong=E2=82=82?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit There's no reason this module would export it --- .../Category/Monoidal/Instance/FinSetoids.agda | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Categories/Category/Monoidal/Instance/FinSetoids.agda b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda index 60635a9ad..3a632f06d 100644 --- a/src/Categories/Category/Monoidal/Instance/FinSetoids.agda +++ b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda @@ -19,10 +19,6 @@ open import Categories.Category.Cartesian open import Categories.Category.Instance.FinSetoids open import Categories.Category.Instance.SingletonSet -map-cong₂ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {f g : A → B} {h i : C → D} → - f ≗ g → h ≗ i → map f h ≗ map g i -map-cong₂ p q (x , y) = cong₂ _,_ (p x) (q y) - module _ {c ℓ} where FinSetoids-Cartesian : Cartesian (FinSetoids c ℓ) FinSetoids-Cartesian = record @@ -86,3 +82,8 @@ module _ {c ℓ} where } } } + where + -- this should be in the next release of stdlib + map-cong₂ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {f g : A → B} {h i : C → D} → + f ≗ g → h ≗ i → map f h ≗ map g i + map-cong₂ p q (x , y) = cong₂ _,_ (p x) (q y) From 2b35f2c04e4632596127ae2cb46b784333e76d09 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 4 Jul 2021 09:17:06 +0100 Subject: [PATCH 4/5] Don't use record syntax for products for terminal --- .../Category/Monoidal/Instance/FinSetoids.agda | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/Categories/Category/Monoidal/Instance/FinSetoids.agda b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda index 3a632f06d..d3f73b97d 100644 --- a/src/Categories/Category/Monoidal/Instance/FinSetoids.agda +++ b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda @@ -23,13 +23,10 @@ module _ {c ℓ} where FinSetoids-Cartesian : Cartesian (FinSetoids c ℓ) FinSetoids-Cartesian = record { terminal = record - { ⊤ = record - { fst = SingletonSetoid - ; snd = 1 , record - { cong₁ = λ _ → refl - ; inverse = record - { fst = λ { zero → refl } - } + { ⊤ = SingletonSetoid , 1 , record + { cong₁ = λ _ → refl + ; inverse = record + { fst = λ { zero → refl } } } } From 7429fe956a4046807151ca7b77e2e0ca29ee72f3 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sun, 4 Jul 2021 21:34:03 +0100 Subject: [PATCH 5/5] FinSetoids is cocartesian too --- .../Monoidal/Instance/FinSetoids.agda | 87 ++++++++++++++++++- 1 file changed, 86 insertions(+), 1 deletion(-) diff --git a/src/Categories/Category/Monoidal/Instance/FinSetoids.agda b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda index d3f73b97d..777055709 100644 --- a/src/Categories/Category/Monoidal/Instance/FinSetoids.agda +++ b/src/Categories/Category/Monoidal/Instance/FinSetoids.agda @@ -2,20 +2,26 @@ module Categories.Category.Monoidal.Instance.FinSetoids where +open import Data.Empty.Polymorphic open import Data.Fin.Base open import Data.Fin.Properties hiding (setoid) import Data.Nat.Base as ℕ open import Data.Product open import Data.Product.Relation.Binary.Pointwise.NonDependent +open import Data.Sum as ∑ hiding (map) +import Data.Sum.Properties as ∑ +open import Data.Sum.Relation.Binary.Pointwise open import Data.Unit.Polymorphic open import Function open import Function.Equality using (Π; _⟨$⟩_) -open import Level using (Lift) +open import Level using (Lift; _⊔_) open import Relation.Binary open import Relation.Binary.Reasoning.MultiSetoid open import Relation.Binary.PropositionalEquality open import Categories.Category.Cartesian +open import Categories.Category.Cocartesian +open import Categories.Category.Instance.EmptySet open import Categories.Category.Instance.FinSetoids open import Categories.Category.Instance.SingletonSet @@ -84,3 +90,82 @@ module _ {c ℓ} where map-cong₂ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {f g : A → B} {h i : C → D} → f ≗ g → h ≗ i → map f h ≗ map g i map-cong₂ p q (x , y) = cong₂ _,_ (p x) (q y) + + FinSetoids-Cocartesian : Cocartesian (FinSetoids c (c ⊔ ℓ)) + FinSetoids-Cocartesian = record + { initial = record + { ⊥ = EmptySetoid , 0 , record + { f = ⊥-elim + ; f⁻¹ = λ { () } + ; cong₁ = λ { {()} } + ; cong₂ = λ { {()} } + ; inverse = (λ ()) , (λ ()) + } + ; ⊥-is-initial = record + { ! = λ {A} → record + { _⟨$⟩_ = ⊥-elim + ; cong = λ { {()} } + } + ; !-unique = λ { f {()} } + } + } + ; coproducts = record + { coproduct = λ {A B} → + let + A-Setoid , ∣A∣ , A-Finite = A + module A-Setoid = Setoid A-Setoid + module A-Finite = Inverse A-Finite + B-Setoid , ∣B∣ , B-Finite = B + module B-Setoid = Setoid B-Setoid + module B-Finite = Inverse B-Finite + in record + { A+B = ⊎-setoid A-Setoid B-Setoid , ∣A∣ ℕ.+ ∣B∣ , record + { f = join ∣A∣ ∣B∣ ∘ ∑.map A-Finite.f B-Finite.f + ; f⁻¹ = ∑.map A-Finite.f⁻¹ B-Finite.f⁻¹ ∘ splitAt ∣A∣ + ; cong₁ = λ + { (inj₁ p) → cong (inject+ ∣B∣) (A-Finite.cong₁ p) + ; (inj₂ q) → cong (raise ∣A∣) (B-Finite.cong₁ q) + } + ; cong₂ = λ { refl → Setoid.refl (⊎-setoid A-Setoid B-Setoid) } + ; inverse = record + { fst = λ x → begin⟨ setoid _ ⟩ + join ∣A∣ ∣B∣ (∑.map A-Finite.f B-Finite.f (∑.map A-Finite.f⁻¹ B-Finite.f⁻¹ (splitAt ∣A∣ x))) + ≡⟨ cong (join ∣A∣ ∣B∣) (∑.map-commute (splitAt ∣A∣ x)) ⟩ + join ∣A∣ ∣B∣ (∑.map (A-Finite.f ∘ A-Finite.f⁻¹) (B-Finite.f ∘ B-Finite.f⁻¹) (splitAt ∣A∣ x)) + ≡⟨ cong (join ∣A∣ ∣B∣) (∑.map-cong (proj₁ A-Finite.inverse) (proj₁ B-Finite.inverse) (splitAt ∣A∣ x)) ⟩ + join ∣A∣ ∣B∣ (∑.map id id (splitAt ∣A∣ x)) + ≡⟨ cong (join ∣A∣ ∣B∣) (∑.map-id (splitAt ∣A∣ x)) ⟩ + join ∣A∣ ∣B∣ (splitAt ∣A∣ x) + ≡⟨ join-splitAt ∣A∣ ∣B∣ x ⟩ + x ∎ + ; snd = λ + { (inj₁ x) → begin⟨ ⊎-setoid A-Setoid B-Setoid ⟩ + ∑.map A-Finite.f⁻¹ B-Finite.f⁻¹ (splitAt ∣A∣ (inject+ ∣B∣ (A-Finite.f x))) + ≡⟨ cong (∑.map A-Finite.f⁻¹ B-Finite.f⁻¹) (splitAt-inject+ ∣A∣ ∣B∣ (A-Finite.f x)) ⟩ + inj₁ (A-Finite.f⁻¹ (A-Finite.f x)) + ≈⟨ inj₁ (proj₂ A-Finite.inverse x) ⟩ + inj₁ x ∎ + ; (inj₂ x) → begin⟨ ⊎-setoid A-Setoid B-Setoid ⟩ + ∑.map A-Finite.f⁻¹ B-Finite.f⁻¹ (splitAt ∣A∣ (raise ∣A∣ (B-Finite.f x))) + ≡⟨ cong (∑.map A-Finite.f⁻¹ B-Finite.f⁻¹) (splitAt-raise ∣A∣ ∣B∣ (B-Finite.f x)) ⟩ + inj₂ (B-Finite.f⁻¹ (B-Finite.f x)) + ≈⟨ inj₂ (proj₂ B-Finite.inverse x) ⟩ + inj₂ x ∎ + } + } + } + ; i₁ = record { _⟨$⟩_ = inj₁; cong = inj₁ } + ; i₂ = record { _⟨$⟩_ = inj₂; cong = inj₂ } + ; [_,_] = λ f g → record + { _⟨$⟩_ = ∑.[ f ⟨$⟩_ , g ⟨$⟩_ ] + ; cong = λ { (inj₁ x) → Π.cong f x ; (inj₂ x) → Π.cong g x } + } + ; inject₁ = λ {_} {f} {g} → Π.cong f + ; inject₂ = λ {_} {f} {g} → Π.cong g + ; unique = λ + { {C} h≈f h≈g (inj₁ x) → Setoid.sym (proj₁ C) (h≈f (A-Setoid.sym x)) + ; {C} h≈f h≈g (inj₂ x) → Setoid.sym (proj₁ C) (h≈g (B-Setoid.sym x)) + } + } + } + }