From 275ff7bffd7818175f4e79a5eb9d99e27dd97ea5 Mon Sep 17 00:00:00 2001 From: Stefania Damato Date: Thu, 29 May 2025 14:07:27 +0100 Subject: [PATCH 01/11] Updated README --- README.md | 100 +++++------------------------------------------------- 1 file changed, 9 insertions(+), 91 deletions(-) diff --git a/README.md b/README.md index 7b34cd241f..3433bd5013 100644 --- a/README.md +++ b/README.md @@ -1,93 +1,11 @@ -A standard library for Cubical Agda -=================================== +A fork of the Cubical Agda library, including code from our formalisation of [Distributive Laws of Monadic Containers](https://arxiv.org/abs/2503.17191) +---------------------------------------- -The source code has a glorious clickable [rendered version](https://agda.github.io/cubical/Cubical.README.html). +### Chris Purdy and Stefania Damato +
-There is also a [discord server](https://discord.gg/yjTKHzepMx), shared with [agda-unimath](https://unimath.github.io/agda-unimath/) and the [1lab](https://1lab.dev/). - -Compiling, using and installing -------------------------------- -This library checks with [Agda](https://github.com/agda/agda/) version indicated in the table below. -For detailed install instructions see the -[INSTALL](https://github.com/agda/cubical/blob/master/INSTALL.md) -file. -If you want to use some specific release of Agda, -the following table lists which releases of Agda are known to work with which release of this library. -Most likely, a lot more combinations work as well. -Agda versions as written below, correspond to tags. - -| cubical library version | Agda versions | -|-------------------------|--------------------------------| -| current master | `v2.7.0.1` | -| `v0.8` | `v2.6.4.1` `v2.7.0.1` | -| `v0.7` | `v2.6.4` `v2.6.4.1` | -| `v0.6` | `v2.6.4` | -| `v0.5` | `v2.6.3` `v2.6.4` | -| `v0.4` | `v2.6.2.2` | -| `v0.3` | `v2.6.2` | -| `v0.2` | `v2.6.1.3` | -| `v0.1` | `v2.6.0.1` | - -For example, if you have Agda 2.6.2.2, you can switch to version 0.4 of the cubical library with -``` -git checkout v0.4 -``` - -Learning materials ------------------- -* Introductory material from the HoTTest summer school: - [literate agda files](https://github.com/martinescardo/HoTTEST-Summer-School/tree/main/Agda/Cubical) - [recordings on youtube](https://www.youtube.com/channel/UC-9jDbJ-HegCFuWuam1SfvQ) - -* For an introduction to this library, see this [blog - post](https://homotopytypetheory.org/2018/12/06/cubical-agda/). Note that many - files and results have moved since this blog post was written. - -* For some introductory lecture notes see the material for the Cubical Agda course - of the [EPIT 2021 spring school](https://github.com/HoTT/EPIT-2020/blob/main/04-cubical-type-theory/). - - -Theoretical background ----------------------- -For a paper with details about Cubical Agda, see [Cubical Agda: a dependently typed -programming language with univalence and higher inductive -types](https://dl.acm.org/doi/10.1145/3341691) by Andrea Vezzosi, Anders -Mörtberg, and Andreas Abel. - -The type theory that Cubical Agda implements is a variation of the -cubical type theory of: - -[Cubical Type Theory: a constructive interpretation of the univalence -axiom](https://arxiv.org/abs/1611.02108) - Cyril Cohen, Thierry -Coquand, Simon Huber, Anders Mörtberg. - - -The key difference is that the Kan composition operations are -decomposed into homogeneous composition and generalized transport as -in: - -[On Higher Inductive Types in Cubical Type -Theory](https://arxiv.org/abs/1802.01170) - Thierry Coquand, Simon -Huber, Anders Mörtberg. - -This makes it possible to directly represent higher inductive types. - - -Reviewing of [pull requests](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+draft%3Afalse) --------------------------- -If you switch your draft pull request (PR) to 'ready to merge', -or directly create an open PR, -we should request a review, by one of the reviewers below. -If that doesn't happen, you can also request a reviewer yourself (for reviewer expertise see below), -to make us aware of the open PR. Feel free to use Discord to get in touch with a reviewer in case reviewing is taking a very long time. - -| Reviewer | github handle | Area of expertise | -|-------------------------------------------------------------------------|---------------|---------------------------------------------| -| [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) | [mortberg](https://github.com/mortberg) | *Most topics* | -| [Evan Cavallo](https://ecavallo.net/) | [ecavallo](https://github.com/ecavallo) | *Most topics* | -| [Felix Cherubini](https://felix-cherubini.de) | [felixwellen](https://github.com/felixwellen) | *Mainly algebra related topics* | -| [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461) | [mzeuner](https://github.com/mzeuner) | *Algebra related topics* | -| [Axel Ljungström](https://aljungstrom.github.io) | [aljungstrom](https://github.com/aljungstrom) | *Synthetic homotopy theory and cohomology* | -| [Andrea Vezzosi](http://saizan.github.io/) | [Saizan](https://github.com/Saizan) | *Inactive* | - -[Overview](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) of the current open PRs, descending time since last action. +The formalisation includes: +* monadic and directed container examples, +* monadic, directed, monadic-directed, and directed-monadic distributive laws, +* distributive law examples, +* and proofs of uniqueness of certain concrete distributive laws. \ No newline at end of file From e5268afdd865c5b943a4a58606633f345da16e2a Mon Sep 17 00:00:00 2001 From: Stefania Damato Date: Fri, 30 May 2025 18:02:05 +0100 Subject: [PATCH 02/11] Added Set containers --- Cubical/Data/Containers.agda | 10 ++ .../Containers/ContainerExtensionProofs.agda | 2 +- .../Containers/{ => Generalised}/Base.agda | 2 +- Cubical/Data/Containers/Set/Base.agda | 117 ++++++++++++++++++ 4 files changed, 129 insertions(+), 2 deletions(-) create mode 100644 Cubical/Data/Containers.agda rename Cubical/Data/Containers/{ => Generalised}/Base.agda (98%) create mode 100644 Cubical/Data/Containers/Set/Base.agda diff --git a/Cubical/Data/Containers.agda b/Cubical/Data/Containers.agda new file mode 100644 index 0000000000..8bf611fb8f --- /dev/null +++ b/Cubical/Data/Containers.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --safe #-} + +module Cubical.Data.Containers where + +open import Cubical.Data.Containers.Set.Base public +open import Cubical.Data.Containers.Generalised.Base public + +open import Cubical.Data.Containers.Algebras public +open import Cubical.Data.Containers.ContainerExtensionProofs public +open import Cubical.Data.Containers.InductiveContainers public diff --git a/Cubical/Data/Containers/ContainerExtensionProofs.agda b/Cubical/Data/Containers/ContainerExtensionProofs.agda index 4445bd85e8..a518eeda50 100644 --- a/Cubical/Data/Containers/ContainerExtensionProofs.agda +++ b/Cubical/Data/Containers/ContainerExtensionProofs.agda @@ -27,7 +27,7 @@ open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.Functors open import Cubical.Categories.Yoneda -open import Cubical.Data.Containers.Base +open import Cubical.Data.Containers.Generalised.Base open import Cubical.Data.Sigma private diff --git a/Cubical/Data/Containers/Base.agda b/Cubical/Data/Containers/Generalised/Base.agda similarity index 98% rename from Cubical/Data/Containers/Base.agda rename to Cubical/Data/Containers/Generalised/Base.agda index 0f79e4a38b..68c6c77118 100644 --- a/Cubical/Data/Containers/Base.agda +++ b/Cubical/Data/Containers/Generalised/Base.agda @@ -12,7 +12,7 @@ {-# OPTIONS --safe #-} -module Cubical.Data.Containers.Base where +module Cubical.Data.Containers.Generalised.Base where open import Cubical.Categories.Category.Base open import Cubical.Categories.Functor diff --git a/Cubical/Data/Containers/Set/Base.agda b/Cubical/Data/Containers/Set/Base.agda new file mode 100644 index 0000000000..1e774b815b --- /dev/null +++ b/Cubical/Data/Containers/Set/Base.agda @@ -0,0 +1,117 @@ +{-# OPTIONS --safe #-} + +module Cubical.Data.Containers.Set.Base where + +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧) +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Prelude hiding (_◁_) +open import Cubical.Foundations.Function +open import Cubical.Data.Unit + +private + variable + ℓs ℓs' ℓp ℓp' : Level + +record SetCon : Type (ℓ-suc (ℓ-max ℓs ℓp)) where + constructor _◁_&_&_ + field + Shape : Type ℓs + Position : Shape → Type ℓp + isSetShape : isSet Shape + isSetPos : ∀ {s} → isSet (Position s) +open SetCon + +-------------------------------------------- +-- ⟦_⟧f : SetCon → Functor Set Set +-------------------------------------------- + +⟦_⟧ : ∀ {ℓ : Level} → SetCon {ℓs} {ℓp} → (hSet ℓ → hSet (ℓ-max (ℓ-max ℓs ℓp) ℓ)) +fst (⟦ S ◁ P & isSetS & _ ⟧ (X , isSetX)) = Σ[ s ∈ S ] (P s → X) +snd (⟦ S ◁ P & isSetS & _ ⟧ (X , isSetX)) = isSetΣ isSetS (λ s → isSetΠ λ _ → isSetX) + +⟦_⟧m : ∀ {ℓ : Level} (C : SetCon {ℓs} {ℓp} ) {X Y : hSet ℓ} → SET ℓ [ X , Y ] → + SET (ℓ-max (ℓ-max ℓs ℓp) ℓ) [ ⟦ C ⟧ X , ⟦ C ⟧ Y ] +⟦ S ◁ P & isSetS & _ ⟧m {X} {Y} X→Y (s , p) = s , λ ps → X→Y (p ps) + +open Functor + +⟦_⟧f : SetCon {ℓs} {ℓp} → Functor (SET (ℓ-max ℓs ℓp)) (SET (ℓ-max ℓs ℓp)) +F-ob ⟦ C ⟧f X = ⟦ C ⟧ X +F-hom ⟦ C ⟧f {X} {Y} = ⟦ C ⟧m {X} {Y} +F-id ⟦ C ⟧f i (s , p) = s , p +fst (F-seq ⟦ C ⟧f f g i (s , p)) = s +snd (F-seq ⟦ C ⟧f f g i (s , p)) ps = g (f (p ps)) + +-- Set container morphism +record _⇒ᶜ_ (Γ : SetCon {ℓs} {ℓp}) (Δ : SetCon {ℓs'} {ℓp'}) : + Type (ℓ-max ℓs (ℓ-max ℓs' (ℓ-max ℓp ℓp'))) where + constructor _◁m_ + field + u : Shape Γ → Shape Δ + f : (s : Shape Γ) → Position Δ (u s) → Position Γ s + +open _⇒ᶜ_ + +-------------------------------------------- +-- SetCons form a category +-------------------------------------------- + +isSet⇒ᶜ : ∀ {ℓs ℓp} {C D : SetCon {ℓs} {ℓp}} → isSet (C ⇒ᶜ D) +u (isSet⇒ᶜ {ℓs} {ℓp} {C} {D} (u₁ ◁m f₁) (u₂ ◁m f₂) p q i j) s = + isSet→SquareP + (λ _ _ → D .isSetShape) + (λ k → u (p k) s) + (λ k → u (q k) s) + (λ _ → u₁ s) + (λ _ → u₂ s) + i j +f (isSet⇒ᶜ {ℓs} {ℓp} {S₁ ◁ P₁ & setS₁ & setP₁} {S₂ ◁ P₂ & setS₂ & setP₂} (u₁ ◁m f₁) (u₂ ◁m f₂) p q i j) s₁ = + isSet→SquareP + {A = λ i j → P₂ (isSet→SquareP + (λ _ _ → setS₂) (λ k → u (p k) s₁) (λ k → u (q k) s₁) (λ _ → u₁ s₁) (λ _ → u₂ s₁) i j) → + P₁ s₁} + (λ _ _ → isSetΠ λ _ → setP₁ {s₁}) + (λ k → f (p k) s₁) + (λ k → f (q k) s₁) + (λ _ → f₁ s₁) + (λ _ → f₂ s₁) + i j + +open Category hiding (_∘_) + +-- Category of SetCons +SetCont : ∀ {ℓs ℓp : Level} → Category _ _ +ob (SetCont {ℓs} {ℓp}) = SetCon {ℓs} {ℓp} +Hom[_,_] SetCont = _⇒ᶜ_ +u (id SetCont) s = s +f (id SetCont) s p = p +u ((SetCont ⋆ (u₁ ◁m f₁)) (u₂ ◁m f₂)) = u₂ ∘ u₁ +f ((SetCont ⋆ (u₁ ◁m f₁)) (u₂ ◁m f₂)) s p = f₁ s (f₂ (u₁ s) p) +⋆IdL SetCont (u ◁m f) = refl +⋆IdR SetCont (u ◁m f)= refl +⋆Assoc SetCont (u₁ ◁m f₁) (u₂ ◁m f₂) (u₃ ◁m f₃) = refl +isSetHom SetCont = isSet⇒ᶜ + +-- Identity SetCon +idC : SetCon {ℓs} {ℓp} +Shape idC = Unit* +Position idC _ = Unit* +isSetShape idC = isSetUnit* +isSetPos idC = isSetUnit* + +◇ : {S : Type ℓs} {SS : isSet S} {T : Type ℓs'} {TT : isSet T} + (P : S → Type ℓp) {PP : ∀ {s} → isSet (P s)}(Q : T → Type ℓp') → + fst (⟦ S ◁ P & SS & PP ⟧ (T , TT)) → Type (ℓ-max ℓp ℓp') +◇ P Q (s , f) = Σ (P s) (Q ∘ f) + +-- Composition of SetCons +_∘ᶜ_ : SetCon {ℓs} {ℓp} → SetCon {ℓs'} {ℓp'} → SetCon +Shape (C ∘ᶜ (T ◁ Q & setT & _)) = fst (⟦ C ⟧ (T , setT)) +Position ((S ◁ P & setS & setP) ∘ᶜ (T ◁ Q & setT & _)) = ◇ {SS = setS} {TT = setT} P {PP = setP} Q +isSetShape (C ∘ᶜ (T ◁ Q & setT & _)) = snd (⟦ C ⟧ (T , setT)) +isSetPos ((S ◁ P & _ & setP) ∘ᶜ (T ◁ Q & _ & setQ)) = isSetΣ setP (λ _ → setQ) + From 633b8f34079fb59d535f88c174a8d17a3cb3bb00 Mon Sep 17 00:00:00 2001 From: Stefania Damato Date: Fri, 30 May 2025 19:05:26 +0100 Subject: [PATCH 03/11] Mnd&Dir Containers and their distr laws --- Cubical/Algebra/DirContainer.agda | 5 + Cubical/Algebra/DirContainer/Base.agda | 30 +++++ Cubical/Algebra/DistributiveLaw.agda | 9 ++ Cubical/Algebra/DistributiveLaw/Base.agda | 21 ++++ .../DistributiveLaw/DirDistributiveLaw.agda | 84 ++++++++++++++ .../DistributiveLaw/MndDistributiveLaw.agda | 109 ++++++++++++++++++ Cubical/Algebra/MndContainer.agda | 7 ++ Cubical/Algebra/MndContainer/Base.agda | 73 ++++++++++++ .../MndContainer/MndContainerMorphism.agda | 46 ++++++++ 9 files changed, 384 insertions(+) create mode 100644 Cubical/Algebra/DirContainer.agda create mode 100644 Cubical/Algebra/DirContainer/Base.agda create mode 100644 Cubical/Algebra/DistributiveLaw.agda create mode 100644 Cubical/Algebra/DistributiveLaw/Base.agda create mode 100644 Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda create mode 100644 Cubical/Algebra/DistributiveLaw/MndDistributiveLaw.agda create mode 100644 Cubical/Algebra/MndContainer.agda create mode 100644 Cubical/Algebra/MndContainer/Base.agda create mode 100644 Cubical/Algebra/MndContainer/MndContainerMorphism.agda diff --git a/Cubical/Algebra/DirContainer.agda b/Cubical/Algebra/DirContainer.agda new file mode 100644 index 0000000000..ce2dc9b17d --- /dev/null +++ b/Cubical/Algebra/DirContainer.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DirContainer where + +open import Cubical.Algebra.DirContainer.Base public diff --git a/Cubical/Algebra/DirContainer/Base.agda b/Cubical/Algebra/DirContainer/Base.agda new file mode 100644 index 0000000000..081cda077a --- /dev/null +++ b/Cubical/Algebra/DirContainer/Base.agda @@ -0,0 +1,30 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DirContainer.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Containers.Set.Base + +private + variable + ℓs ℓp : Level + +open SetCon + +record DirectedContainer (C : SetCon {ℓs} {ℓp}) : Type (ℓ-suc (ℓ-max ℓs ℓp)) where + S = Shape C + P = Position C + field + o : (s : S) → P s + _↓_ : (s : S) → P s → S + _⊕_ : {s : S} → (p : P s) → P (s ↓ p) → P s + unitl-↓ : (s : S) → s ↓ (o _) ≡ s + distr-↓-⊕ : (s : S) (p : P s) (p' : P (s ↓ p)) → + s ↓ (p ⊕ p') ≡ (s ↓ p) ↓ p' + unitl-⊕ : (s : S) (p : P (s ↓ o s)) → + PathP (λ i → P (unitl-↓ s (~ i))) (o s ⊕ p) p + unitr-⊕ : (s : S) (p : P s) → p ⊕ (o (s ↓ p)) ≡ p + assoc-⊕ : (s : S) (p : P s) (p' : P (s ↓ p)) → + PathP (λ i → P (distr-↓-⊕ s p p' i) → P s) + (λ p'' → (p ⊕ p') ⊕ p'') + (λ p'' → p ⊕ (p' ⊕ p'')) diff --git a/Cubical/Algebra/DistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw.agda new file mode 100644 index 0000000000..de14004a26 --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw.agda @@ -0,0 +1,9 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw where + +open import Cubical.Algebra.DistributiveLaw.Base public + +open import Cubical.Algebra.DistributiveLaw.MndDistributiveLaw public +open import Cubical.Algebra.DistributiveLaw.DirDistributiveLaw public + diff --git a/Cubical/Algebra/DistributiveLaw/Base.agda b/Cubical/Algebra/DistributiveLaw/Base.agda new file mode 100644 index 0000000000..ae52104d72 --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/Base.agda @@ -0,0 +1,21 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.Base where + +open import Cubical.Foundations.Prelude + +private + variable + ℓs ℓp ℓt ℓr ℓq : Level + +-- ⟨_,_⟩ notation - extremely dependent function pairing +[_,_,_]⟨_,_⟩ : {S : Type ℓs} {T : Type ℓt} {R : Type ℓr} + (P : S → Type ℓp) (Q : T → Type ℓq) (s : S) (f : P s → T) + (g : (Σ[ p ∈ P s ] Q (f p)) → R) (x : P s) → Σ[ t ∈ T ] (Q t → R) +[ P , Q , s ]⟨ f , g ⟩ x = (f x , λ y → g (x , y)) + +-- A curried version of the above (i.e. where the second function can be curried) +[_,_,_]⟨_,_⟩' : {S : Type ℓs} {T : Type ℓt} {R : Type ℓr} (P : S → Type ℓp) + (Q : T → Type ℓq) (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → R) (x : P s) → + Σ[ t ∈ T ] (Q t → R) +[ P , Q , s ]⟨ f , g ⟩' x = (f x , g x) diff --git a/Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda new file mode 100644 index 0000000000..062181b414 --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda @@ -0,0 +1,84 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.DirDistributiveLaw where + +open import Cubical.Foundations.Prelude +open import Cubical.Algebra.DirContainer as DC +open import Cubical.Algebra.DistributiveLaw.Base +open import Cubical.Data.Containers.Set.Base + +open DC.DirectedContainer + +private + variable + ℓs ℓp : Level + +-- Distributive law direction: Aₘ ∘ Bₘ → Bₘ ∘ Aₘ +record DirectedDistributiveLaw (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s)) + (T : Type ℓs) (Q : T → Type ℓp) (setT : isSet T) (setQ : ∀ {t} → isSet (Q t)) + (Aₘ : DirectedContainer (S ◁ P & setS & setP)) (Bₘ : DirectedContainer (T ◁ Q & setT & setQ)) : + Type (ℓ-suc (ℓ-max ℓs ℓp)) where + + _⊕ᵃ_ = _⊕_ Aₘ + _↓ᵃ_ = _↓_ Aₘ + _⊕ᵇ_ = _⊕_ Bₘ + _↓ᵇ_ = _↓_ Bₘ + + field + u₁ : (s : S) (f : P s → T) → T + u₂ : (s : S) (f : P s → T) → Q (u₁ s f) → S + + v₁ : {s : S} {f : P s → T} (q : Q (u₁ s f)) → P (u₂ s f q) → P s + v₂ : {s : S} {f : P s → T} (q : Q (u₁ s f)) (p : P (u₂ s f q)) → Q (f (v₁ q p)) + + unit-oA-shape : (s : S) (f : P s → T) → u₁ s f ≡ f (o Aₘ s) + unit-oA-pos₁ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (unit-oA-shape s f i)) → P s) + (λ q → v₁ q (o Aₘ (u₂ s f q))) + (λ q → o Aₘ s) + unit-oA-pos₂ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (unit-oA-shape s f i)) → Q (f (unit-oA-pos₁ s f i q))) + (λ q → v₂ q (o Aₘ (u₂ s f q))) + (λ q → q) + + mul-A-shape₁ : (s : S) (f : P s → T) → u₁ s f ≡ u₁ s (λ p → u₁ (s ↓ᵃ p) (λ p' → f (p ⊕ᵃ p'))) + mul-A-shape₂ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f i)) → S) + (λ q → u₂ s f q) + (λ q → u₂ s (λ p → u₁ (s ↓ᵃ p) (λ p' → f (p ⊕ᵃ p'))) q) + mul-A-shape₃ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f i)) (p : P (mul-A-shape₂ s f i q)) → S) + (λ q p → u₂ s f q ↓ᵃ p) + (λ q p → u₂ (s ↓ᵃ v₁ q p) (λ p' → f (v₁ q p ⊕ᵃ p')) (v₂ q p)) + + mul-A-pos₁ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f i)) (p : P (mul-A-shape₂ s f i q)) → P (mul-A-shape₃ s f i q p) → P s) + (λ q p p' → v₁ q (p ⊕ᵃ p')) + (λ q p p' → v₁ q p ⊕ᵃ v₁ (v₂ q p) p') + mul-A-pos₂ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f i)) (p : P (mul-A-shape₂ s f i q)) → (p' : P (mul-A-shape₃ s f i q p)) → Q (f (mul-A-pos₁ s f i q p p'))) + (λ q p p' → v₂ q (p ⊕ᵃ p')) + (λ q p p' → v₂ (v₂ q p) p') + + unit-oB-shape : (s : S) (f : P s → T) → u₂ s f (o Bₘ _) ≡ s + unit-oB-pos₁ : (s : S) (f : P s → T) (p : P (u₂ s f (o Bₘ _))) → + PathP (λ i → P (unit-oB-shape s f (~ i))) + (v₁ (o Bₘ _) p) + p + unit-oB-pos₂ : (s : S) (f : P s → T) (p : P (u₂ s f (o Bₘ _))) → v₂ (o Bₘ _) p ≡ o Bₘ _ + + mul-B-shape₁ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → u₁ s f ↓ᵇ q ≡ u₁ (u₂ s f q) (λ p → f (v₁ q p) ↓ᵇ v₂ q p) + + mul-B-shape₂ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → + PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) → S) + (λ q' → u₂ s f (q ⊕ᵇ q')) + (λ q' → u₂ (u₂ s f q) ((λ p → f (v₁ q p) ↓ᵇ v₂ q p)) q') + + mul-B-pos₁ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → + PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) (p : P (mul-B-shape₂ s f q i q')) → P s) + (λ q' p → v₁ (q ⊕ᵇ q') p) + (λ q' p → v₁ q (v₁ q' p)) + mul-B-pos₂ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → + PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) (p : P (mul-B-shape₂ s f q i q')) → Q (f (mul-B-pos₁ s f q i q' p))) + (λ q' p → v₂ (q ⊕ᵇ q') p) + (λ q' p → v₂ q (v₁ q' p) ⊕ᵇ (v₂ q' p)) diff --git a/Cubical/Algebra/DistributiveLaw/MndDistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw/MndDistributiveLaw.agda new file mode 100644 index 0000000000..99b69f71cc --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/MndDistributiveLaw.agda @@ -0,0 +1,109 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.MndDistributiveLaw where + +open import Cubical.Foundations.Function +open import Cubical.Foundations.Prelude +open import Cubical.Algebra.MndContainer.Base as MC +open import Cubical.Algebra.DistributiveLaw.Base +open import Cubical.Data.Containers.Set.Base + +open MC.MndContainer + +private + variable + ℓs ℓp : Level + +-- Distributive law direction: Aₘ ∘ Bₘ → Bₘ ∘ Aₘ +record MndDistributiveLaw (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s)) + (T : Type ℓs) (Q : T → Type ℓp) (setT : isSet T) (setQ : ∀ {t} → isSet (Q t)) + (Aₘ : MndContainer (S ◁ P & setS & setP)) (Bₘ : MndContainer (T ◁ Q & setT & setQ)) : + Type (ℓ-suc (ℓ-max ℓs ℓp)) where + field + u₁ : (s : S) (f : P s → T) → T + u₂ : (s : S) (f : P s → T) → Q (u₁ s f) → S + + v₁ : {s : S} {f : P s → T} (q : Q (u₁ s f)) → P (u₂ s f q) → P s + v₂ : {s : S} {f : P s → T} (q : Q (u₁ s f)) (p : P (u₂ s f q)) → Q (f (v₁ q p)) + + unit-ιB-shape₁ : (s : S) → u₁ s (const (ι Bₘ)) ≡ ι Bₘ + unit-ιB-shape₂ : (s : S) → + PathP (λ i → Q (unit-ιB-shape₁ s i) → S) + (u₂ s (const (ι Bₘ))) + (const s) + + unit-ιB-pos₁ : (s : S) → + PathP (λ i → (q : Q (unit-ιB-shape₁ s i)) → P (unit-ιB-shape₂ s i q) → P s) + v₁ + (λ q p → p) + + unit-ιB-pos₂ : (s : S) → + PathP (λ i → (q : Q (unit-ιB-shape₁ s i)) → (p : P (unit-ιB-shape₂ s i q)) → Q (ι Bₘ)) + v₂ + (λ q p → q) + + unit-ιA-shape₁ : (t : T) → u₁ (ι Aₘ) (const t) ≡ t + unit-ιA-shape₂ : (t : T) → + PathP (λ i → Q (unit-ιA-shape₁ t i) → S) + (u₂ (ι Aₘ) (const t)) + (const (ι Aₘ)) + + unit-ιA-pos₁ : (t : T) → + PathP (λ i → (q : Q (unit-ιA-shape₁ t i)) → P (unit-ιA-shape₂ t i q) → P (ι Aₘ)) + v₁ + (λ q p → p) + + unit-ιA-pos₂ : (t : T) → + PathP (λ i → (q : Q (unit-ιA-shape₁ t i)) → P (unit-ιA-shape₂ t i q) → Q t) + v₂ + (λ q p → q) + + mul-A-shape₁ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + u₁ (σ Aₘ s f) (uncurry g ∘ (pr Aₘ _ _)) ≡ + u₁ s (uncurry u₁ ∘ [ P , _ , _ ]⟨ f , g ⟩') + + mul-A-shape₂ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + PathP (λ i → Q (mul-A-shape₁ s f g i) → S) + (λ q → (u₂ (σ Aₘ s f) (uncurry g ∘ pr Aₘ _ _)) q) + (λ q → uncurry (σ Aₘ) ([ Q , P , _ ]⟨ u₂ s (uncurry u₁ ∘ [ P , _ , _ ]⟨ f , g ⟩') , + (λ q p → (uncurry u₂ ∘ [ P , _ , _ ]⟨ f , g ⟩') (v₁ q p) (v₂ q p)) ⟩' q)) + + mul-A-pos₁ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f g i)) → P (mul-A-shape₂ s f g i q) → P s) + (λ q p → pr₁ Aₘ s _ (v₁ q p)) + (λ q p → v₁ q (pr₁ Aₘ _ _ p)) + + mul-A-pos₂₁ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f g i)) (p : P (mul-A-shape₂ s f g i q)) → P (f (mul-A-pos₁ s f g i q p))) + (λ q p → pr₂ Aₘ _ _ (v₁ q p)) + (λ q p → v₁ (v₂ q (pr₁ Aₘ _ _ p)) (pr₂ Aₘ _ _ p)) + + mul-A-pos₂₂ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f g i)) (p : P (mul-A-shape₂ s f g i q)) → Q (g (mul-A-pos₁ s f g i q p) (mul-A-pos₂₁ s f g i q p))) + (λ q p → v₂ q p) + (λ q p → v₂ (v₂ q (pr₁ Aₘ _ _ p)) (pr₂ Aₘ _ _ p)) + + mul-B-shape₁ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + u₁ s (uncurry (σ Bₘ) ∘ [ P , _ , _ ]⟨ f , g ⟩') + ≡ σ Bₘ (u₁ s f) (uncurry u₁ ∘ [ Q , _ , _ ]⟨ u₂ s f , (λ q p → g (v₁ q p) (v₂ q p)) ⟩') + + mul-B-shape₂ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + PathP (λ i → Q (mul-B-shape₁ s f g i) → S) + (λ q → u₂ s (uncurry (σ Bₘ) ∘ [ P , _ , _ ]⟨ f , g ⟩') q ) + (λ q → (uncurry (uncurry u₂ ∘ [ Q , _ , _ ]⟨ u₂ s f , (λ q p → g (v₁ q p) (v₂ q p)) ⟩') ∘ pr Bₘ _ _) q) + + mul-B-pos₁ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + PathP (λ i → (q : Q (mul-B-shape₁ s f g i)) (p : P (mul-B-shape₂ s f g i q)) → P s) + (λ q p → v₁ q p) + (λ q p → v₁ (pr₁ Bₘ _ _ q) (v₁ (pr₂ Bₘ _ _ q) p)) + + mul-B-pos₂₁ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + PathP (λ i → (q : Q (mul-B-shape₁ s f g i)) (p : P (mul-B-shape₂ s f g i q)) → Q (f (mul-B-pos₁ s f g i q p))) + (λ q p → pr₁ Bₘ _ _ (v₂ q p)) + (λ q p → v₂ (pr₁ Bₘ _ _ q) (v₁ (pr₂ Bₘ _ _ q) p)) + + mul-B-pos₂₂ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + PathP (λ i → (q : Q (mul-B-shape₁ s f g i)) (p : P (mul-B-shape₂ s f g i q)) → + Q (g (mul-B-pos₁ s f g i q p) (mul-B-pos₂₁ s f g i q p))) + (λ q p → pr₂ Bₘ _ _ (v₂ q p)) + (λ q p → v₂ (pr₂ Bₘ _ _ q) p) diff --git a/Cubical/Algebra/MndContainer.agda b/Cubical/Algebra/MndContainer.agda new file mode 100644 index 0000000000..6348362eb2 --- /dev/null +++ b/Cubical/Algebra/MndContainer.agda @@ -0,0 +1,7 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.MndContainer where + +open import Cubical.Algebra.MndContainer.Base public +open import Cubical.Algebra.MndContainer.MndContainerMorphism public + diff --git a/Cubical/Algebra/MndContainer/Base.agda b/Cubical/Algebra/MndContainer/Base.agda new file mode 100644 index 0000000000..db14b07bfc --- /dev/null +++ b/Cubical/Algebra/MndContainer/Base.agda @@ -0,0 +1,73 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.MndContainer.Base where + +open import Cubical.Foundations.Function +open import Cubical.Foundations.Prelude +open import Cubical.Data.Containers.Set.Base + +private + variable + ℓs ℓp : Level + +record IsMndContainer (S : Type ℓs) (P : S → Type ℓp) + (ι : S) + (σ : (s : S) → (P s → S) → S) + (pr₁ : (s : S) (f : P s → S) → P (σ s f) → P s) + (pr₂ : (s : S) (f : P s → S) (p : P (σ s f)) → P (f (pr₁ s f p))) : + Type (ℓ-suc (ℓ-max ℓs ℓp)) where + field + unit-l : (s : S) → σ ι (const s) ≡ s + unit-r : (s : S) → σ s (const ι) ≡ s + assoc : (a : S) (b : P a → S) (c : (p : P a) → P (b p) → S) → + σ a (λ p → σ (b p) (c p)) ≡ σ (σ a b) (λ p → c (pr₁ _ _ p) (pr₂ _ _ p)) + pr-unit-r : {s : S} → + PathP (λ i → (p : P (unit-r s i)) → P s) + (pr₁ _ _) + (λ p → p) + pr-unit-l : {s : S} → + PathP (λ i → (p : P (unit-l s i)) → P s) + (pr₂ _ _) + (λ p → p) + pr-mul₁ : {a : S} {b : P a → S} {c : (p : P a) → P (b p) → S} → + PathP (λ i → P (assoc a b c i) → P a) + (λ q → pr₁ a (λ p → σ (b p) (c p)) q) + (λ q → pr₁ a b (pr₁ (σ a b) ((λ r → c (pr₁ _ _ r) (pr₂ _ _ r))) q)) + pr-mul₁₂ : {a : S} {b : P a → S} {c : (p : P a) → P (b p) → S} → + PathP (λ i → (p : P (assoc a b c i)) → P (b (pr-mul₁ i p))) + (λ q → pr₁ _ _ (pr₂ _ _ q)) + (λ q → pr₂ _ _ (pr₁ _ _ q)) + pr-mul₂₂ : {a : S} {b : P a → S} {c : (p : P a) → P (b p) → S} → + PathP (λ i → (q : P (assoc a b c i)) → P (c (pr-mul₁ i q) (pr-mul₁₂ i q))) + (λ q → pr₂ _ _ (pr₂ _ _ q)) + (λ q → pr₂ _ _ q) + +open SetCon + +record MndContainer (C : SetCon {ℓs} {ℓp}) : Type (ℓ-suc (ℓ-max ℓs ℓp)) where + S = Shape C + P = Position C + field + ι : S + σ : (s : S) → (P s → S) → S + pr₁ : (s : S) (f : P s → S) → P (σ s f) → P s + pr₂ : (s : S) (f : P s → S) (p : P (σ s f)) → P (f (pr₁ s f p)) + isMndContainer : IsMndContainer S P ι σ pr₁ pr₂ + + pr : (s : S) (f : P s → S) → P (σ s f) → Σ[ p ∈ P s ] P (f p) + pr s f p = pr₁ _ _ p , pr₂ _ _ p + +open MndContainer + +mContBuilder : (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s)) + (ι : S) + (σ : (s : S) → (P s → S) → S) + (pr₁ : (s : S) (f : P s → S) → P (σ s f) → P s) + (pr₂ : (s : S) (f : P s → S) (p : P (σ s f)) → P (f (pr₁ s f p))) + (isMndCont : IsMndContainer S P ι σ pr₁ pr₂) → + MndContainer (S ◁ P & setS & setP) +ι (mContBuilder S P setS setP ι σ pr₁ pr₂ isMndCont) = ι +σ (mContBuilder S P setS setP ι σ pr₁ pr₂ isMndCont) = σ +pr₁ (mContBuilder S P setS setP ι σ pr₁ pr₂ isMndCont) = pr₁ +pr₂ (mContBuilder S P setS setP ι σ pr₁ pr₂ isMndCont) = pr₂ +isMndContainer (mContBuilder S P setS setP ι σ pr₁ pr₂ isMndCont) = isMndCont diff --git a/Cubical/Algebra/MndContainer/MndContainerMorphism.agda b/Cubical/Algebra/MndContainer/MndContainerMorphism.agda new file mode 100644 index 0000000000..43901ca58e --- /dev/null +++ b/Cubical/Algebra/MndContainer/MndContainerMorphism.agda @@ -0,0 +1,46 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.MndContainer.MndContainerMorphism where + +open import Cubical.Foundations.Prelude hiding (_▷_) renaming (fst to π₁ ; snd to π₂) +open import Cubical.Foundations.Function +open import Cubical.Algebra.MndContainer.Base +open import Cubical.Data.Sigma +open import Cubical.Data.Containers.Set.Base + +private + variable + ℓs ℓp ℓs' ℓp' : Level + +open SetCon +open MndContainer + +record IsMndContainerMorphism (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s)) + (T : Type ℓs') (Q : T → Type ℓp') (setT : isSet T) (setQ : ∀ {t} → isSet (Q t)) + (Aₘ : MndContainer (S ◁ P & setS & setP)) + (Bₘ : MndContainer (T ◁ Q & setT & setQ)) + (shapeₘ : S → T) (positionₘ : {s : S} → Q (shapeₘ s) → P s) : + Type (ℓ-suc (ℓ-max ℓs (ℓ-max ℓs' (ℓ-max ℓp ℓp')))) where + field + ι-pres : shapeₘ (ι Aₘ) ≡ ι Bₘ + σ-pres : (s : S) (f : P s → S) → shapeₘ (σ Aₘ s f) ≡ σ Bₘ (shapeₘ s) (shapeₘ ∘ f ∘ positionₘ) + pr₁-pres : (s : S) (f : P s → S) → + PathP (λ i → Q (σ-pres s f i) → P s) + (λ q → pr₁ Aₘ s f (positionₘ q)) + (λ q → positionₘ (pr₁ Bₘ (shapeₘ s) (shapeₘ ∘ f ∘ positionₘ) q)) + pr₂-pres : (s : S) (f : P s → S) → + PathP (λ i → (q : Q (σ-pres s f i)) → P (f (pr₁-pres s f i q))) + (λ q → pr₂ Aₘ s f (positionₘ q)) + (λ q → positionₘ (pr₂ Bₘ (shapeₘ s) (shapeₘ ∘ f ∘ positionₘ) q)) + + +record MndContainerMorphism (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s)) + (T : Type ℓs') (Q : T → Type ℓp') (setT : isSet T) (setQ : ∀ {t} → isSet (Q t)) + (Aₘ : MndContainer (S ◁ P & setS & setP)) + (Bₘ : MndContainer (T ◁ Q & setT & setQ)) : + Type (ℓ-suc (ℓ-max ℓs (ℓ-max ℓs' (ℓ-max ℓp ℓp')))) where + field + shapeₘ : S → T + positionₘ : {s : S} → Q (shapeₘ s) → P s + isMCMorphism : IsMndContainerMorphism S P setS setP T Q setT setQ Aₘ Bₘ shapeₘ positionₘ + From 47af45e996acb364f0965bd109149f4edd47ce18 Mon Sep 17 00:00:00 2001 From: Stefania Damato Date: Mon, 2 Jun 2025 14:08:52 +0100 Subject: [PATCH 04/11] DirMnd and MndDir distr laws --- Cubical/Algebra/DirContainer/Base.agda | 2 +- Cubical/Algebra/DistributiveLaw.agda | 3 + .../DistributiveLaw/DirDistributiveLaw.agda | 4 +- .../DirMndDistributiveLaw.agda | 97 ++++++++++++++++ .../MndDirDistributiveLaw.agda | 107 ++++++++++++++++++ 5 files changed, 210 insertions(+), 3 deletions(-) create mode 100644 Cubical/Algebra/DistributiveLaw/DirMndDistributiveLaw.agda create mode 100644 Cubical/Algebra/DistributiveLaw/MndDirDistributiveLaw.agda diff --git a/Cubical/Algebra/DirContainer/Base.agda b/Cubical/Algebra/DirContainer/Base.agda index 081cda077a..105b0d1304 100644 --- a/Cubical/Algebra/DirContainer/Base.agda +++ b/Cubical/Algebra/DirContainer/Base.agda @@ -11,7 +11,7 @@ private open SetCon -record DirectedContainer (C : SetCon {ℓs} {ℓp}) : Type (ℓ-suc (ℓ-max ℓs ℓp)) where +record DirContainer (C : SetCon {ℓs} {ℓp}) : Type (ℓ-suc (ℓ-max ℓs ℓp)) where S = Shape C P = Position C field diff --git a/Cubical/Algebra/DistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw.agda index de14004a26..ad3d78c165 100644 --- a/Cubical/Algebra/DistributiveLaw.agda +++ b/Cubical/Algebra/DistributiveLaw.agda @@ -6,4 +6,7 @@ open import Cubical.Algebra.DistributiveLaw.Base public open import Cubical.Algebra.DistributiveLaw.MndDistributiveLaw public open import Cubical.Algebra.DistributiveLaw.DirDistributiveLaw public +open import Cubical.Algebra.DistributiveLaw.MndDirDistributiveLaw public +open import Cubical.Algebra.DistributiveLaw.DirMndDistributiveLaw public + diff --git a/Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda index 062181b414..f9618a0355 100644 --- a/Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda +++ b/Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda @@ -7,7 +7,7 @@ open import Cubical.Algebra.DirContainer as DC open import Cubical.Algebra.DistributiveLaw.Base open import Cubical.Data.Containers.Set.Base -open DC.DirectedContainer +open DC.DirContainer private variable @@ -16,7 +16,7 @@ private -- Distributive law direction: Aₘ ∘ Bₘ → Bₘ ∘ Aₘ record DirectedDistributiveLaw (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s)) (T : Type ℓs) (Q : T → Type ℓp) (setT : isSet T) (setQ : ∀ {t} → isSet (Q t)) - (Aₘ : DirectedContainer (S ◁ P & setS & setP)) (Bₘ : DirectedContainer (T ◁ Q & setT & setQ)) : + (Aₘ : DirContainer (S ◁ P & setS & setP)) (Bₘ : DirContainer (T ◁ Q & setT & setQ)) : Type (ℓ-suc (ℓ-max ℓs ℓp)) where _⊕ᵃ_ = _⊕_ Aₘ diff --git a/Cubical/Algebra/DistributiveLaw/DirMndDistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw/DirMndDistributiveLaw.agda new file mode 100644 index 0000000000..e4a55c1e2d --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/DirMndDistributiveLaw.agda @@ -0,0 +1,97 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.DirMndDistributiveLaw where + +open import Cubical.Foundations.Function +open import Cubical.Foundations.Prelude +open import Cubical.Algebra.DirContainer as DC +open import Cubical.Algebra.MndContainer as MC +open import Cubical.Algebra.DistributiveLaw.Base +open import Cubical.Data.Containers.Set.Base + +open DC.DirContainer +open MC.MndContainer + +private + variable + ℓs ℓp : Level + +-- Distributive law direction: Aₘ ∘ Bₘ → Bₘ ∘ Aₘ +record DirMndDistributiveLaw (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s)) + (T : Type ℓs) (Q : T → Type ℓp) (setT : isSet T) (setQ : ∀ {t} → isSet (Q t)) + (Aₘ : MndContainer (S ◁ P & setS & setP)) (Bₘ : DirContainer (T ◁ Q & setT & setQ)) : + Type (ℓ-suc (ℓ-max ℓs ℓp)) where + + _⊕ᵇ_ = _⊕_ Bₘ + _↓ᵇ_ = _↓_ Bₘ + + field + u₁ : (s : S) (f : P s → T) → T + u₂ : (s : S) (f : P s → T) → Q (u₁ s f) → S + + v₁ : {s : S} {f : P s → T} (q : Q (u₁ s f)) → P (u₂ s f q) → P s + v₂ : {s : S} {f : P s → T} (q : Q (u₁ s f)) (p : P (u₂ s f q)) → Q (f (v₁ q p)) + + unit-ιA-shape₁ : (t : T) → u₁ (ι Aₘ) (const t) ≡ t + unit-ιA-shape₂ : (t : T) → + PathP (λ i → (q : Q (unit-ιA-shape₁ t i)) → S) + (u₂ (ι Aₘ) (const t)) + (const (ι Aₘ)) + + unit-ιA-pos₁ : (t : T) → + PathP (λ i → (q : Q (unit-ιA-shape₁ t i)) → P (unit-ιA-shape₂ t i q) → P (ι Aₘ)) + v₁ + (λ q p → p) + + unit-ιA-pos₂ : (t : T) → + PathP (λ i → (q : Q (unit-ιA-shape₁ t i)) → P (unit-ιA-shape₂ t i q) → Q t) + v₂ + (λ q p → q) + + mul-A-shape₁ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + u₁ (σ Aₘ s f) (uncurry g ∘ (pr Aₘ _ _)) ≡ + u₁ s (uncurry u₁ ∘ [ P , _ , _ ]⟨ f , g ⟩') + + mul-A-shape₂ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + PathP (λ i → Q (mul-A-shape₁ s f g i) → S) + (λ q → (u₂ (σ Aₘ s f) (uncurry g ∘ pr Aₘ _ _)) q) + (λ q → uncurry (σ Aₘ) ([ Q , P , _ ]⟨ u₂ s (uncurry u₁ ∘ [ P , _ , _ ]⟨ f , g ⟩') , + (λ q p → (uncurry u₂ ∘ [ P , _ , _ ]⟨ f , g ⟩') (v₁ q p) (v₂ q p)) ⟩' q)) + + mul-A-pos₁ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f g i)) → P (mul-A-shape₂ s f g i q) → P s) + (λ q p → pr₁ Aₘ s _ (v₁ q p)) + (λ q p → v₁ q (pr₁ Aₘ _ _ p)) + + mul-A-pos₂₁ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f g i)) (p : P (mul-A-shape₂ s f g i q)) → P (f (mul-A-pos₁ s f g i q p))) + (λ q p → pr₂ Aₘ _ _ (v₁ q p)) + (λ q p → v₁ (v₂ q (pr₁ Aₘ _ _ p)) (pr₂ Aₘ _ _ p)) + + mul-A-pos₂₂ : (s : S) (f : P s → S) (g : (p : P s) → P (f p) → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f g i)) (p : P (mul-A-shape₂ s f g i q)) → Q (g (mul-A-pos₁ s f g i q p) (mul-A-pos₂₁ s f g i q p))) + (λ q p → v₂ q p) + (λ q p → v₂ (v₂ q (pr₁ Aₘ _ _ p)) (pr₂ Aₘ _ _ p)) + + unit-oB-shape : (s : S) (f : P s → T) → u₂ s f (o Bₘ _) ≡ s + unit-oB-pos₁ : (s : S) (f : P s → T) (p : P (u₂ s f (o Bₘ _))) → + PathP (λ i → P (unit-oB-shape s f (~ i))) + (v₁ (o Bₘ _) p) + p + unit-oB-pos₂ : (s : S) (f : P s → T) (p : P (u₂ s f (o Bₘ _))) → v₂ (o Bₘ _) p ≡ o Bₘ _ + + mul-B-shape₁ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → u₁ s f ↓ᵇ q ≡ u₁ (u₂ s f q) (λ p → f (v₁ q p) ↓ᵇ v₂ q p) + + mul-B-shape₂ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → + PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) → S) + (λ q' → u₂ s f (q ⊕ᵇ q')) + (λ q' → u₂ (u₂ s f q) (λ p → f (v₁ q p) ↓ᵇ v₂ q p) q') + + mul-B-pos₁ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → + PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) (p : P (mul-B-shape₂ s f q i q')) → P s) + (λ q' p → v₁ (q ⊕ᵇ q') p) + (λ q' p → v₁ q (v₁ q' p)) + mul-B-pos₂ : (s : S) (f : P s → T) (q : Q (u₁ s f)) → + PathP (λ i → (q' : Q (mul-B-shape₁ s f q i)) (p : P (mul-B-shape₂ s f q i q')) → Q (f (mul-B-pos₁ s f q i q' p))) + (λ q' p → v₂ (q ⊕ᵇ q') p) + (λ q' p → v₂ q (v₁ q' p) ⊕ᵇ (v₂ q' p)) diff --git a/Cubical/Algebra/DistributiveLaw/MndDirDistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw/MndDirDistributiveLaw.agda new file mode 100644 index 0000000000..33cc3fcba6 --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/MndDirDistributiveLaw.agda @@ -0,0 +1,107 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.MndDirDistributiveLaw where + +open import Cubical.Foundations.Function +open import Cubical.Foundations.Prelude +open import Cubical.Algebra.DirContainer as DC +open import Cubical.Algebra.MndContainer as MC +open import Cubical.Algebra.DistributiveLaw.Base +open import Cubical.Data.Containers.Set.Base + +open DC.DirContainer +open MC.MndContainer + +private + variable + ℓs ℓp : Level + +-- Distributive law direction: Aₘ ∘ Bₘ → Bₘ ∘ Aₘ +record MndDirDistributiveLaw (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s)) + (T : Type ℓs) (Q : T → Type ℓp) (setT : isSet T) (setQ : ∀ {t} → isSet (Q t)) + (Aₘ : DirContainer (S ◁ P & setS & setP)) (Bₘ : MndContainer (T ◁ Q & setT & setQ)) : + Type (ℓ-suc (ℓ-max ℓs ℓp)) where + + _⊕ᵃ_ = _⊕_ Aₘ + _↓ᵃ_ = _↓_ Aₘ + + field + u₁ : (s : S) (f : P s → T) → T + u₂ : (s : S) (f : P s → T) → Q (u₁ s f) → S + + v₁ : {s : S} {f : P s → T} (q : Q (u₁ s f)) → P (u₂ s f q) → P s + v₂ : {s : S} {f : P s → T} (q : Q (u₁ s f)) (p : P (u₂ s f q)) → Q (f (v₁ q p)) + + unit-oA-shape : (s : S) (f : P s → T) → u₁ s f ≡ f (o Aₘ s) + unit-oA-pos₁ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (unit-oA-shape s f i)) → P s) + (λ q → v₁ q (o Aₘ (u₂ s f q))) + (λ q → o Aₘ s) + unit-oA-pos₂ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (unit-oA-shape s f i)) → Q (f (unit-oA-pos₁ s f i q))) + (λ q → v₂ q (o Aₘ (u₂ s f q))) + (λ q → q) + + -- Redundant - follows from unit-oA-shape + mul-A-shape₁ : (s : S) (f : P s → T) → u₁ s f ≡ u₁ s (λ p → u₁ (s ↓ᵃ p) (λ p' → f (p ⊕ᵃ p'))) + -- Redundant - follows from unit-oA-shape + mul-A-shape₂ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f i)) → S) + (λ q → u₂ s f q) + (λ q → u₂ s (λ p → u₁ (s ↓ᵃ p) (λ p' → f (p ⊕ᵃ p'))) q) + mul-A-shape₃ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f i)) (p : P (mul-A-shape₂ s f i q)) → S) + (λ q p → u₂ s f q ↓ᵃ p) + (λ q p → u₂ (s ↓ᵃ v₁ q p) (λ p' → f (v₁ q p ⊕ᵃ p')) (v₂ q p)) + + mul-A-pos₁ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f i)) (p : P (mul-A-shape₂ s f i q)) → P (mul-A-shape₃ s f i q p) → P s) + (λ q p p' → v₁ q (p ⊕ᵃ p')) + (λ q p p' → v₁ q p ⊕ᵃ v₁ (v₂ q p) p') + mul-A-pos₂ : (s : S) (f : P s → T) → + PathP (λ i → (q : Q (mul-A-shape₁ s f i)) (p : P (mul-A-shape₂ s f i q)) → (p' : P (mul-A-shape₃ s f i q p)) → Q (f (mul-A-pos₁ s f i q p p'))) + (λ q p p' → v₂ q (p ⊕ᵃ p')) + (λ q p p' → v₂ (v₂ q p) p') + + -- Redundant - follows from unit-oA-shape + unit-ιB-shape₁ : (s : S) → u₁ s (const (ι Bₘ)) ≡ ι Bₘ + unit-ιB-shape₂ : (s : S) → + PathP (λ i → (q : Q (unit-ιB-shape₁ s i)) → S) + (u₂ s (const (ι Bₘ))) + (const s) + + unit-ιB-pos₁ : (s : S) → + PathP (λ i → (q : Q (unit-ιB-shape₁ s i)) → P (unit-ιB-shape₂ s i q) → P s) + v₁ + (λ q p → p) + + unit-ιB-pos₂ : (s : S) → + PathP (λ i → (q : Q (unit-ιB-shape₁ s i)) → (p : P (unit-ιB-shape₂ s i q)) → Q (ι Bₘ)) + v₂ + (λ q p → q) + + -- Redundant - follows from unit-oA-shape + mul-B-shape₁ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + u₁ s (uncurry (σ Bₘ) ∘ [ P , _ , _ ]⟨ f , g ⟩') + ≡ σ Bₘ (u₁ s f) (uncurry u₁ ∘ [ Q , _ , _ ]⟨ u₂ s f , (λ q p → g (v₁ q p) (v₂ q p)) ⟩') + + mul-B-shape₂ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + PathP (λ i → Q (mul-B-shape₁ s f g i) → S) + (λ q → u₂ s (uncurry (σ Bₘ) ∘ [ P , _ , _ ]⟨ f , g ⟩') q ) + (λ q → (uncurry (uncurry u₂ ∘ [ Q , _ , _ ]⟨ u₂ s f , (λ q p → g (v₁ q p) (v₂ q p)) ⟩') ∘ pr Bₘ _ _) q) + + mul-B-pos₁ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + PathP (λ i → (q : Q (mul-B-shape₁ s f g i)) (p : P (mul-B-shape₂ s f g i q)) → P s) + (λ q p → v₁ q p) + (λ q p → v₁ (pr₁ Bₘ _ _ q) (v₁ (pr₂ Bₘ _ _ q) p)) + + mul-B-pos₂₁ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + PathP (λ i → (q : Q (mul-B-shape₁ s f g i)) (p : P (mul-B-shape₂ s f g i q)) → Q (f (mul-B-pos₁ s f g i q p))) + (λ q p → pr₁ Bₘ _ _ (v₂ q p)) + (λ q p → v₂ (pr₁ Bₘ _ _ q) (v₁ (pr₂ Bₘ _ _ q) p)) + + mul-B-pos₂₂ : (s : S) (f : P s → T) (g : (p : P s) → Q (f p) → T) → + PathP (λ i → (q : Q (mul-B-shape₁ s f g i)) (p : P (mul-B-shape₂ s f g i q)) → + Q (g (mul-B-pos₁ s f g i q p) (mul-B-pos₂₁ s f g i q p))) + (λ q p → pr₂ Bₘ _ _ (v₂ q p)) + (λ q p → v₂ (pr₂ Bₘ _ _ q) p) From a34f264379c8c3f8697af12977112995babd26a8 Mon Sep 17 00:00:00 2001 From: Stefania Damato Date: Mon, 2 Jun 2025 16:32:54 +0100 Subject: [PATCH 05/11] Mnd & Dir examples --- Cubical/Algebra/DirContainer.agda | 1 + Cubical/Algebra/DirContainer/Examples.agda | 54 ++++++++ Cubical/Algebra/MndContainer.agda | 2 +- Cubical/Algebra/MndContainer/Examples.agda | 148 +++++++++++++++++++++ 4 files changed, 204 insertions(+), 1 deletion(-) create mode 100644 Cubical/Algebra/DirContainer/Examples.agda create mode 100644 Cubical/Algebra/MndContainer/Examples.agda diff --git a/Cubical/Algebra/DirContainer.agda b/Cubical/Algebra/DirContainer.agda index ce2dc9b17d..dd4a69187a 100644 --- a/Cubical/Algebra/DirContainer.agda +++ b/Cubical/Algebra/DirContainer.agda @@ -3,3 +3,4 @@ module Cubical.Algebra.DirContainer where open import Cubical.Algebra.DirContainer.Base public +open import Cubical.Algebra.DirContainer.Examples public diff --git a/Cubical/Algebra/DirContainer/Examples.agda b/Cubical/Algebra/DirContainer/Examples.agda new file mode 100644 index 0000000000..a947ee28aa --- /dev/null +++ b/Cubical/Algebra/DirContainer/Examples.agda @@ -0,0 +1,54 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DirContainer.Examples where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function +open import Cubical.Algebra.DirContainer.Base +open import Cubical.Data.Containers.Set.Base +open import Cubical.Data.Unit +open import Cubical.Data.Nat hiding (_·_) +open import Cubical.Data.Bool hiding (_⊕_ ; ⊕-assoc) +open import Cubical.Data.Empty +open import Cubical.Data.Sum + + +private + variable + ℓs ℓp : Level + +open DirContainer + +-- Examples of directed containers + +WriterC : (A : hSet ℓs) → DirContainer {ℓs} {ℓp} (fst A ◁ (const (Unit* {ℓp})) & snd A & isSetUnit*) +o (WriterC A) _ = tt* +_↓_ (WriterC A) a tt* = a +_⊕_ (WriterC A) tt* tt* = tt* +unitl-↓ (WriterC A) a = refl +distr-↓-⊕ (WriterC A) a tt* tt* = refl +unitl-⊕ (WriterC A) a tt* = refl +unitr-⊕ (WriterC A) a tt* = refl +assoc-⊕ (WriterC A) a tt* tt* i tt* = tt* + +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.Monoid.Instances.Nat +open import Cubical.Algebra.Semigroup +open MonoidStr +open IsMonoid +open IsSemigroup + +ReaderC : (A : Type ℓp) (mon : MonoidStr A) → + DirContainer {ℓs} {ℓp} ((Unit* {ℓs}) ◁ (const A) & isSetUnit* & mon .isMonoid .isSemigroup .is-set) +o (ReaderC A mon) tt* = mon .ε +_↓_ (ReaderC A mon) tt* a = tt* +_⊕_ (ReaderC A mon) = mon ._·_ +unitl-↓ (ReaderC A mon) tt* = refl +distr-↓-⊕ (ReaderC A mon) tt* a a' = refl +unitl-⊕ (ReaderC A mon) tt* = mon .isMonoid .·IdL +unitr-⊕ (ReaderC A mon) tt* = mon .isMonoid .·IdR +assoc-⊕ (ReaderC A mon) tt* a a' i a'' = mon .isMonoid .·Assoc a a' a'' (~ i) + +StreamC : DirContainer {ℓs} {ℓ-zero} ((Unit* {ℓs}) ◁ (const ℕ) & isSetUnit* & isSetℕ) +StreamC = ReaderC (fst NatMonoid) (snd NatMonoid) diff --git a/Cubical/Algebra/MndContainer.agda b/Cubical/Algebra/MndContainer.agda index 6348362eb2..ae33d19fab 100644 --- a/Cubical/Algebra/MndContainer.agda +++ b/Cubical/Algebra/MndContainer.agda @@ -4,4 +4,4 @@ module Cubical.Algebra.MndContainer where open import Cubical.Algebra.MndContainer.Base public open import Cubical.Algebra.MndContainer.MndContainerMorphism public - +open import Cubical.Algebra.MndContainer.Examples public diff --git a/Cubical/Algebra/MndContainer/Examples.agda b/Cubical/Algebra/MndContainer/Examples.agda new file mode 100644 index 0000000000..ba72e5b980 --- /dev/null +++ b/Cubical/Algebra/MndContainer/Examples.agda @@ -0,0 +1,148 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.MndContainer.Examples where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function +open import Cubical.Algebra.MndContainer.Base +open import Cubical.Data.Containers.Set.Base +open import Cubical.Data.Unit +open import Cubical.Data.Nat hiding (_·_) +open import Cubical.Data.Bool +open import Cubical.Data.Empty +open import Cubical.Data.Sum + + +private + variable + ℓs ℓp ℓ ℓ' ℓ'' : Level + +open MndContainer +open IsMndContainer + +State : (S : hSet ℓ) → SetCon {ℓ} {ℓ} +State (S , setS) = (S → S) ◁ (λ _ → S) & isSetΠ (λ _ → setS) & setS + +JustOrNothing : Bool* {ℓ} → Type ℓ' +JustOrNothing (lift false) = ⊥* +JustOrNothing (lift true) = Unit* + +isSetJustOrNothing : ∀ {ℓ ℓ'} → {s : Bool* {ℓ}} → isSet {ℓ'} (JustOrNothing {ℓ} {ℓ'} s) +isSetJustOrNothing {_} {_} {lift false} x = rec* x +isSetJustOrNothing {_} {_} {lift true} = isSetUnit* + +Maybe : SetCon {ℓs} {ℓp} +Maybe {ℓs} {ℓp} = Bool* {ℓs} ◁ JustOrNothing {ℓs} {ℓp} & isSetBool* & (λ {s} → isSetJustOrNothing {_} {_} {s}) + where + isSetBool* : isSet (Bool* {ℓ}) + isSetBool* {ℓ} a b = J (λ _ p → ∀ q → p ≡ q) (K-Bool* {ℓ} (refl ≡_) refl) + where + K-Bool* + : ∀ {ℓ} → (P : {b : Bool* {ℓ}} → b ≡ b → Type ℓ) + → (∀{b} → P {b} refl) + → ∀{b} → (q : b ≡ b) → P q + K-Bool* P Pr {lift false} = J (λ{ (lift false) q → P q ; (lift true) _ → Lift ⊥ }) Pr + K-Bool* P Pr {lift true} = J (λ{ (lift true) q → P q ; (lift false) _ → Lift ⊥ }) Pr + +LOrR : {A : Type ℓ} {B : Type ℓ'} → A ⊎ B → Type ℓ'' +LOrR (inl a) = Unit* +LOrR (inr b) = ⊥* + +isSetLOrR : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {x : A ⊎ B} → isSet {ℓ''} (LOrR x) +isSetLOrR {_} {_} {_} {A} {B} {inl a} = isSetUnit* +isSetLOrR {_} {_} {_} {A} {B} {inr b} x = rec* x + +-- Examples of monadic containers + +ReaderM : (A : hSet ℓp) → MndContainer {ℓs} {ℓp} (Unit* ◁ (λ _ → fst A) & isSetUnit* & snd A) +ι (ReaderM A) = tt* +σ (ReaderM A) _ _ = tt* +pr₁ (ReaderM A) _ _ p = p +pr₂ (ReaderM A) _ _ p = p +unit-l (isMndContainer (ReaderM A)) tt* = refl +unit-r (isMndContainer (ReaderM A)) tt* = refl +assoc (isMndContainer (ReaderM A)) tt* _ _ = refl +pr-unit-r (isMndContainer (ReaderM A)) = refl +pr-unit-l (isMndContainer (ReaderM A)) = refl +pr-mul₁ (isMndContainer (ReaderM A)) = refl +pr-mul₁₂ (isMndContainer (ReaderM A)) = refl +pr-mul₂₂ (isMndContainer (ReaderM A)) = refl + +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.Monoid.Instances.Nat +open MonoidStr +open IsMonoid + +WriterM : (A : hSet ℓs) (mon : MonoidStr (fst A)) → MndContainer {ℓs} {ℓp} (fst A ◁ const Unit* & snd A & isSetUnit*) +ι (WriterM A mon) = mon .ε +σ (WriterM A mon) a b = (mon ._·_) a (b tt*) +pr₁ (WriterM A mon) _ _ tt* = tt* +pr₂ (WriterM A mon) _ _ tt* = tt* +unit-l (isMndContainer (WriterM A mon)) a = mon .·IdL a +unit-r (isMndContainer (WriterM A mon)) a = mon .·IdR a +assoc (isMndContainer (WriterM A mon)) a b c = mon .·Assoc a (b tt*) (c tt* tt*) +pr-unit-r (isMndContainer (WriterM A mon)) i tt* = tt* +pr-unit-l (isMndContainer (WriterM A mon)) i tt* = tt* +pr-mul₁ (isMndContainer (WriterM A mon)) i tt* = tt* +pr-mul₁₂ (isMndContainer (WriterM A mon)) i tt* = tt* +pr-mul₂₂ (isMndContainer (WriterM A mon)) i tt* = tt* + +StreamM : MndContainer {ℓs} {ℓ-zero} (Unit* ◁ const ℕ & isSetUnit* & isSetℕ) +StreamM = ReaderM (ℕ , isSetℕ) + +StateM : (S : hSet ℓs) → MndContainer {ℓs} {ℓs} (State S) +ι (StateM S) s = s +σ (StateM S) f g s = g s (f s) +pr₁ (StateM S) _ _ s = s +pr₂ (StateM S) f _ s = f s +unit-l (isMndContainer (StateM S)) f = refl +unit-r (isMndContainer (StateM S)) f = refl +assoc (isMndContainer (StateM S)) f g h = refl +pr-unit-r (isMndContainer (StateM S)) = refl +pr-unit-l (isMndContainer (StateM S)) = refl +pr-mul₁ (isMndContainer (StateM S)) = refl +pr-mul₁₂ (isMndContainer (StateM S)) = refl +pr-mul₂₂ (isMndContainer (StateM S)) = refl + +MaybeM : MndContainer {ℓs} {ℓp} Maybe +ι MaybeM = true* +σ MaybeM (lift true) f = f tt* +σ MaybeM (lift false) f = false* +pr₁ MaybeM (lift true) _ _ = tt* +pr₂ MaybeM (lift true) _ p = p +pr₂ MaybeM (lift false) _ () +unit-l (isMndContainer MaybeM) a = refl +unit-r (isMndContainer MaybeM) (lift true) = refl +unit-r (isMndContainer MaybeM) (lift false) = refl +assoc (isMndContainer MaybeM) (lift true) b c = refl +assoc (isMndContainer MaybeM) (lift false) b c = refl +pr-unit-r (isMndContainer MaybeM) {lift true} i tt* = tt* +pr-unit-l (isMndContainer MaybeM) {lift true} i p = p +pr-mul₁ (isMndContainer MaybeM) {lift true} {b} {c} i = λ _ → tt* +pr-mul₁₂ (isMndContainer MaybeM) {lift true} {b} {c} i p' = pr₁ MaybeM (b tt*) (c tt*) p' +pr-mul₂₂ (isMndContainer MaybeM) {lift true} {b} {c} i p' = pr₂ MaybeM (b tt*) (c tt*) p' + +-- Note: MaybeM is also special case of CoproductM when E = ⊤ + +CoproductM : ∀ {ℓs ℓs'} (E : hSet ℓs) → + MndContainer {ℓ-max ℓs ℓs'} {ℓs'} ((Unit* {ℓs'} ⊎ (fst E)) ◁ LOrR & (isSet⊎ isSetUnit* (snd E)) & isSetLOrR) +ι (CoproductM E) = inl tt* +σ (CoproductM E) (inl tt*) f = f tt* +σ (CoproductM E) (inr e) f = inr e +pr₁ (CoproductM E) (inl tt*) _ _ = tt* +pr₂ (CoproductM E) (inl tt*) _ y = y +unit-l (isMndContainer (CoproductM E)) _ = refl +unit-r (isMndContainer (CoproductM E)) (inl tt*) = refl +unit-r (isMndContainer (CoproductM E)) (inr e) = refl +assoc (isMndContainer (CoproductM E)) (inl tt*) b c = refl +assoc (isMndContainer (CoproductM E)) (inr e) b c = refl +pr-unit-r (isMndContainer (CoproductM E)) {inl tt*} i tt* = tt* +pr-unit-l (isMndContainer (CoproductM E)) = refl +pr-mul₁ (isMndContainer (CoproductM E)) {inl tt*} = refl +pr-mul₁ (isMndContainer (CoproductM E)) {inr e} i () +pr-mul₁₂ (isMndContainer (CoproductM E)) {inl tt*} = refl +pr-mul₁₂ (isMndContainer (CoproductM E)) {inr e} i () +pr-mul₂₂ (isMndContainer (CoproductM E)) {inl tt*} = refl +pr-mul₂₂ (isMndContainer (CoproductM E)) {inr e} i () + From 27f61070bbb70a25ba2698167eaa77a96c075f8f Mon Sep 17 00:00:00 2001 From: Stefania Damato Date: Mon, 2 Jun 2025 18:39:19 +0100 Subject: [PATCH 06/11] Distr law examples --- Cubical/Algebra/DistributiveLaw.agda | 9 +- Cubical/Algebra/DistributiveLaw/Dir.agda | 5 + .../Base.agda} | 2 +- Cubical/Algebra/DistributiveLaw/DirMnd.agda | 5 + .../Base.agda} | 2 +- Cubical/Algebra/DistributiveLaw/Mnd.agda | 6 + .../Base.agda} | 6 +- .../Algebra/DistributiveLaw/Mnd/Examples.agda | 263 ++++++++++++++++++ Cubical/Algebra/DistributiveLaw/MndDir.agda | 6 + .../Base.agda} | 2 +- .../DistributiveLaw/MndDir/Examples.agda | 124 +++++++++ Cubical/Algebra/MndContainer/Examples.agda | 11 - Cubical/Data/Bool/Properties.agda | 10 + 13 files changed, 429 insertions(+), 22 deletions(-) create mode 100644 Cubical/Algebra/DistributiveLaw/Dir.agda rename Cubical/Algebra/DistributiveLaw/{DirDistributiveLaw.agda => Dir/Base.agda} (98%) create mode 100644 Cubical/Algebra/DistributiveLaw/DirMnd.agda rename Cubical/Algebra/DistributiveLaw/{DirMndDistributiveLaw.agda => DirMnd/Base.agda} (98%) create mode 100644 Cubical/Algebra/DistributiveLaw/Mnd.agda rename Cubical/Algebra/DistributiveLaw/{MndDistributiveLaw.agda => Mnd/Base.agda} (97%) create mode 100644 Cubical/Algebra/DistributiveLaw/Mnd/Examples.agda create mode 100644 Cubical/Algebra/DistributiveLaw/MndDir.agda rename Cubical/Algebra/DistributiveLaw/{MndDirDistributiveLaw.agda => MndDir/Base.agda} (98%) create mode 100644 Cubical/Algebra/DistributiveLaw/MndDir/Examples.agda diff --git a/Cubical/Algebra/DistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw.agda index ad3d78c165..4ea4be1ebd 100644 --- a/Cubical/Algebra/DistributiveLaw.agda +++ b/Cubical/Algebra/DistributiveLaw.agda @@ -4,9 +4,8 @@ module Cubical.Algebra.DistributiveLaw where open import Cubical.Algebra.DistributiveLaw.Base public -open import Cubical.Algebra.DistributiveLaw.MndDistributiveLaw public -open import Cubical.Algebra.DistributiveLaw.DirDistributiveLaw public -open import Cubical.Algebra.DistributiveLaw.MndDirDistributiveLaw public -open import Cubical.Algebra.DistributiveLaw.DirMndDistributiveLaw public - +open import Cubical.Algebra.DistributiveLaw.Mnd public +open import Cubical.Algebra.DistributiveLaw.Dir public +open import Cubical.Algebra.DistributiveLaw.MndDir public +open import Cubical.Algebra.DistributiveLaw.DirMnd public diff --git a/Cubical/Algebra/DistributiveLaw/Dir.agda b/Cubical/Algebra/DistributiveLaw/Dir.agda new file mode 100644 index 0000000000..ab1a9e41d7 --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/Dir.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.Dir where + +open import Cubical.Algebra.DistributiveLaw.Dir.Base public diff --git a/Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw/Dir/Base.agda similarity index 98% rename from Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda rename to Cubical/Algebra/DistributiveLaw/Dir/Base.agda index f9618a0355..cddbc0ad41 100644 --- a/Cubical/Algebra/DistributiveLaw/DirDistributiveLaw.agda +++ b/Cubical/Algebra/DistributiveLaw/Dir/Base.agda @@ -1,6 +1,6 @@ {-# OPTIONS --safe #-} -module Cubical.Algebra.DistributiveLaw.DirDistributiveLaw where +module Cubical.Algebra.DistributiveLaw.Dir.Base where open import Cubical.Foundations.Prelude open import Cubical.Algebra.DirContainer as DC diff --git a/Cubical/Algebra/DistributiveLaw/DirMnd.agda b/Cubical/Algebra/DistributiveLaw/DirMnd.agda new file mode 100644 index 0000000000..ff493bd53e --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/DirMnd.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.DirMnd where + +open import Cubical.Algebra.DistributiveLaw.DirMnd.Base public diff --git a/Cubical/Algebra/DistributiveLaw/DirMndDistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw/DirMnd/Base.agda similarity index 98% rename from Cubical/Algebra/DistributiveLaw/DirMndDistributiveLaw.agda rename to Cubical/Algebra/DistributiveLaw/DirMnd/Base.agda index e4a55c1e2d..625e9c3755 100644 --- a/Cubical/Algebra/DistributiveLaw/DirMndDistributiveLaw.agda +++ b/Cubical/Algebra/DistributiveLaw/DirMnd/Base.agda @@ -1,6 +1,6 @@ {-# OPTIONS --safe #-} -module Cubical.Algebra.DistributiveLaw.DirMndDistributiveLaw where +module Cubical.Algebra.DistributiveLaw.DirMnd.Base where open import Cubical.Foundations.Function open import Cubical.Foundations.Prelude diff --git a/Cubical/Algebra/DistributiveLaw/Mnd.agda b/Cubical/Algebra/DistributiveLaw/Mnd.agda new file mode 100644 index 0000000000..845347e13c --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/Mnd.agda @@ -0,0 +1,6 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.Mnd where + +open import Cubical.Algebra.DistributiveLaw.Mnd.Base public +open import Cubical.Algebra.DistributiveLaw.Mnd.Examples public diff --git a/Cubical/Algebra/DistributiveLaw/MndDistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw/Mnd/Base.agda similarity index 97% rename from Cubical/Algebra/DistributiveLaw/MndDistributiveLaw.agda rename to Cubical/Algebra/DistributiveLaw/Mnd/Base.agda index 99b69f71cc..4ea4e9948b 100644 --- a/Cubical/Algebra/DistributiveLaw/MndDistributiveLaw.agda +++ b/Cubical/Algebra/DistributiveLaw/Mnd/Base.agda @@ -1,14 +1,14 @@ {-# OPTIONS --safe #-} -module Cubical.Algebra.DistributiveLaw.MndDistributiveLaw where +module Cubical.Algebra.DistributiveLaw.Mnd.Base where open import Cubical.Foundations.Function open import Cubical.Foundations.Prelude -open import Cubical.Algebra.MndContainer.Base as MC +open import Cubical.Algebra.MndContainer.Base open import Cubical.Algebra.DistributiveLaw.Base open import Cubical.Data.Containers.Set.Base -open MC.MndContainer +open MndContainer private variable diff --git a/Cubical/Algebra/DistributiveLaw/Mnd/Examples.agda b/Cubical/Algebra/DistributiveLaw/Mnd/Examples.agda new file mode 100644 index 0000000000..ea1838a638 --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/Mnd/Examples.agda @@ -0,0 +1,263 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.Mnd.Examples where + +open import Cubical.Foundations.Function +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Algebra.MndContainer.Base +open import Cubical.Algebra.MndContainer.Examples +open import Cubical.Algebra.DistributiveLaw.Mnd.Base +open import Cubical.Data.Containers.Set.Base +open import Cubical.Data.Bool +open import Cubical.Data.Unit +open import Cubical.Data.Empty + +open MndContainer +open IsMndContainer +open MndDistributiveLaw + +private + variable + ℓs ℓp : Level + +MaybeDistr : (S : Type ℓs) (P : S → Type ℓp) {setS : isSet S} {setP : ∀ {s} → isSet (P s)} + (MC : MndContainer {ℓs} {ℓp} (S ◁ P & setS & setP)) → + MndDistributiveLaw {ℓs} {ℓp} Bool* JustOrNothing isSetBool* isSetJustOrNothing S P setS setP MaybeM MC +u₁ (MaybeDistr S P MC) (lift true) f = f tt* +u₁ (MaybeDistr S P MC) (lift false) f = MC .ι +u₂ (MaybeDistr S P MC) (lift true) f _ = true* +u₂ (MaybeDistr S P MC) (lift false) f _ = false* +v₁ (MaybeDistr S P MC) {lift true} _ x = tt* +v₂ (MaybeDistr S P MC) {lift true} {f} p x = p +unit-ιB-shape₁ (MaybeDistr S P MC) (lift true) = refl +unit-ιB-shape₁ (MaybeDistr S P MC) (lift false) = refl +unit-ιB-shape₂ (MaybeDistr S P MC) (lift true) = refl +unit-ιB-shape₂ (MaybeDistr S P MC) (lift false) = refl +unit-ιB-pos₁ (MaybeDistr S P MC) (lift true) i q tt* = tt* +unit-ιB-pos₂ (MaybeDistr S P MC) (lift true) i q tt* = q +unit-ιA-shape₁ (MaybeDistr S P MC) _ = refl +unit-ιA-shape₂ (MaybeDistr S P MC) _ = refl +unit-ιA-pos₁ (MaybeDistr S P MC) s i q tt* = tt* +unit-ιA-pos₂ (MaybeDistr S P MC) s i q tt* = q +mul-A-shape₁ (MaybeDistr S P MC) (lift true) f g = refl +mul-A-shape₁ (MaybeDistr S P MC) (lift false) f g = refl +mul-A-shape₂ (MaybeDistr S P MC) (lift true) f g = refl +mul-A-shape₂ (MaybeDistr S P MC) (lift false) f g = refl +mul-A-pos₁ (MaybeDistr S P MC) (lift true) f g = refl +mul-A-pos₁ (MaybeDistr {ℓs} {ℓp} S P MC) (lift false) f g i q () +mul-A-pos₂₁ (MaybeDistr S P MC) (lift true) f g = refl +mul-A-pos₂₁ (MaybeDistr {ℓs} {ℓp} S P MC) (lift false) f g i q () +mul-A-pos₂₂ (MaybeDistr S P MC) (lift true) f g = refl +mul-A-pos₂₂ (MaybeDistr S P MC) (lift false) f g i q () +mul-B-shape₁ (MaybeDistr S P MC) (lift true) f g = refl +mul-B-shape₁ (MaybeDistr S P MC) (lift false) f g i = unit-r (isMndContainer MC) (MC .ι) (~ i) +mul-B-shape₂ (MaybeDistr S P MC) (lift true) f g = refl +mul-B-shape₂ (MaybeDistr S P MC) (lift false) f g i = λ _ → false* +mul-B-pos₁ (MaybeDistr S P MC) (lift true) f g i q tt* = tt* +mul-B-pos₁ (MaybeDistr S P MC) (lift false) f g i q () +mul-B-pos₂₁ (MaybeDistr S P MC) (lift true) f g i q tt* = (MC .pr₁) (f tt*) (g tt*) q +mul-B-pos₂₁ (MaybeDistr S P MC) (lift false) f g i q () +mul-B-pos₂₂ (MaybeDistr S P MC) (lift true) f g i q tt* = (MC .pr₂) (f tt*) (g tt*) q +mul-B-pos₂₂ (MaybeDistr S P MC) (lift false) f g i q () + +lemF : ∀ {ℓ ℓ'} {A : Type ℓ} (f g : ⊥* {ℓ'} → A) → f ≡ g +lemF f g = sym (isContrΠ⊥* .snd f) ∙ isContrΠ⊥* .snd g + +Unit*-singleton : ∀ {ℓ} → (x : Unit* {ℓ}) → x ≡ tt* +Unit*-singleton tt* i = tt* + +module MaybeDistrUnique (S : Type ℓs) (P : S → Type ℓp) (setS : isSet S) (setP : ∀ {s} → isSet (P s)) + (MC : MndContainer {ℓs} {ℓp} (S ◁ P & setS & setP)) + (l : MndDistributiveLaw {ℓs} {ℓp} Bool* JustOrNothing isSetBool* isSetJustOrNothing S P setS setP MaybeM MC) where + + L₀ = MaybeDistr S P MC + + u1 : (s : Bool*) (f : JustOrNothing s → S) → u₁ L₀ s f ≡ u₁ l s f + u1 (lift true) f i = hcomp (λ j → λ { (i = i0) → f tt* + ; (i = i1) → u₁ l true* (λ x → f (Unit*-singleton x (~ j))) + }) + (unit-ιA-shape₁ l (f tt*) (~ i)) + u1 (lift false) f i = hcomp (λ j → λ { (i = i0) → ι MC + ; (i = i1) → u₁ l false* (lemF (const (ι MC)) f j) + }) + (unit-ιB-shape₁ l false* (~ i)) + + u2 : (s : Bool*) (f : JustOrNothing s → S) → + PathP (λ i → P (u1 s f i) → Bool*) (u₂ L₀ s f) (u₂ l s f) + u2 (lift true) f i = comp (λ j → P (compPath-filler (λ i' → unit-ιA-shape₁ l (f tt*) (~ i')) + (λ i' → u₁ l true* (λ x → f (Unit*-singleton x (~ i')))) j i + ) → Bool* {ℓs}) + (λ j → λ { (i = i0) → λ p → true* ; + (i = i1) → λ p → u₂ l true* (λ x → f (Unit*-singleton x (~ j))) p }) + (λ p → unit-ιA-shape₂ l (f tt*) (~ i) p) + u2 (lift false) f = compPathP' {B = (λ x → P x → Bool*)} + {x' = λ x → unit-ιB-shape₂ l false* (~ i0) x} + {y' = λ p → unit-ιB-shape₂ l false* (~ i1) p} + {z' = λ p → u₂ l false* (lemF (const (ι MC)) f i1) p} + (λ i p → unit-ιB-shape₂ l false* (~ i) p) + (λ i p → u₂ l false* (lemF (const (ι MC)) f i) p) + + v1 : (s : Bool*) (f : JustOrNothing s → S) → + PathP (λ i → (p : P (u1 s f i)) → JustOrNothing (u2 s f i p) → JustOrNothing s) + (λ p q → v₁ L₀ {s} {f} p q) + (λ p q → v₁ l {s} {f} p q) + v1 (lift true) f i = comp (λ j → (p : P (compPath-filler (λ k → unit-ιA-shape₁ l (f tt*) (~ k)) + (λ k → u₁ l true* (λ x → f (Unit*-singleton x (~ k)))) j i + )) → + JustOrNothing {ℓs} {ℓp} (compPathP'-filler {B = (λ x → P x → Bool*)} + (λ k p' → unit-ιA-shape₂ l (f tt*) (~ k) p') + (λ k p' → u₂ l true* (λ x → f (Unit*-singleton x (~ k))) p') j i p + ) → + Unit* {ℓp} + ) + (λ j → λ { (i = i0) → λ p q → tt* ; + (i = i1) → λ p q → Unit*-singleton (v₁ l p q) (~ j) + }) + (λ p q → tt*) + v1 (lift false) f = toPathP (funExt λ p → funExt (λ q → rec* (subst JustOrNothing (lem p) q))) + where + lem : (p : P (u₁ l false* f)) → u₂ l false* f p ≡ false* + lem p = funExt⁻ (sym (fromPathP (u2 false* f))) p + + v2 : (s : Bool*) (f : JustOrNothing s → S) → + PathP (λ i → (p : P (u1 s f i)) (q : JustOrNothing (u2 s f i p)) → P (f (v1 s f i p q))) + (λ p q → v₂ L₀ {s} {f} p q) + (λ p q → v₂ l {s} {f} p q) + v2 (lift true) f i = + comp (λ j → (p : P (compPath-filler (λ k → unit-ιA-shape₁ l (f tt*) (~ k)) + (λ k → u₁ l true* (λ x → f (Unit*-singleton x (~ k)))) j i + )) → + (q : JustOrNothing {ℓs} {ℓp} (compPathP'-filler {B = (λ x → P x → Bool*)} + (λ k p' → unit-ιA-shape₂ l (f tt*) (~ k) p') + (λ k p' → u₂ l true* (λ x → f (Unit*-singleton x (~ k))) p') j i p + )) → + P (f (fill (λ k' → (p : P (compPath-filler (λ k → unit-ιA-shape₁ l (f tt*) (~ k)) + (λ k → u₁ l true* (λ x → f (Unit*-singleton x (~ k)))) k' i + )) → + JustOrNothing {ℓs} {ℓp} (compPathP'-filler {B = (λ x → P x → Bool*)} + (λ k p' → unit-ιA-shape₂ l (f tt*) (~ k) p') + (λ k p' → u₂ l true* (λ x → f (Unit*-singleton x (~ k))) p') k' i p + ) → + Unit* {ℓp} + ) + (λ k' → λ { (i = i0) → λ p q → tt* + ; (i = i1) → λ p q → Unit*-singleton (v₁ l p q) (~ k') + }) + (inS (λ p q → tt*)) + j p q + )) + ) + (λ j → λ { (i = i0) → λ p q → p + ; (i = i1) → λ p q → v₂ l {true*} {λ x → f (Unit*-singleton x (~ j))} p q + }) + (λ p q → unit-ιA-pos₂ l (f tt*) (~ i) p q) + + v2 (lift false) f = toPathP (funExt λ p → funExt (λ q → rec* (subst JustOrNothing (lem p) q))) + where + lem : (p : P (u₁ l false* f)) → u₂ l false* f p ≡ false* + lem p = funExt⁻ (sym (fromPathP (u2 false* f))) p + +ReaderDistr : (A : hSet ℓp) (S : Type ℓs) (P : S → Type ℓp) {setS : isSet S} {setP : ∀ {s} → isSet (P s)} + (MC : MndContainer {ℓs} {ℓp} (S ◁ P & setS & setP)) + → MndDistributiveLaw {ℓs} {ℓp} S P setS setP (Unit* {ℓs}) (const (fst A)) isSetUnit* (snd A) MC (ReaderM A) +u₁ (ReaderDistr A S P MC) s _ = tt* +u₂ (ReaderDistr A S P MC) s _ a = s +v₁ (ReaderDistr A S P MC) a p = p +v₂ (ReaderDistr A S P MC) a p = a +unit-ιB-shape₂ (ReaderDistr A S P MC) s = refl +unit-ιB-shape₁ (ReaderDistr A S P MC) s = refl +unit-ιB-pos₁ (ReaderDistr A S P MC) s = refl +unit-ιB-pos₂ (ReaderDistr A S P MC) s i a p = a +unit-ιA-shape₂ (ReaderDistr A S P MC) tt* = refl +unit-ιA-shape₁ (ReaderDistr A S P MC) tt* = refl +unit-ιA-pos₁ (ReaderDistr A S P MC) tt* = refl +unit-ιA-pos₂ (ReaderDistr A S P MC) tt* = refl +mul-A-shape₁ (ReaderDistr A S P MC) s f g = refl +mul-A-shape₂ (ReaderDistr A S P MC) s f g = refl +mul-A-pos₁ (ReaderDistr A S P MC) s f g = refl +mul-A-pos₂₁ (ReaderDistr A S P MC) s f g = refl +mul-A-pos₂₂ (ReaderDistr A S P MC) s f g = refl +mul-B-shape₁ (ReaderDistr A S P MC) s f g = refl +mul-B-shape₂ (ReaderDistr A S P MC) s f g = refl +mul-B-pos₁ (ReaderDistr A S P MC) s f g = refl +mul-B-pos₂₁ (ReaderDistr A S P MC) s f g = refl +mul-B-pos₂₂ (ReaderDistr A S P MC) s f g = refl + +module ReaderDistrUnique (A : hSet ℓp) (S : Type ℓs) (P : S → Type ℓp) {setS : isSet S} {setP : ∀ {s} → isSet (P s)} + (MC : MndContainer {ℓs} {ℓp} (S ◁ P & setS & setP)) + (L : MndDistributiveLaw {ℓs} {ℓp} S P setS setP (Unit* {ℓs}) (const (fst A)) isSetUnit* (snd A) MC (ReaderM A)) where + + L₀ = ReaderDistr A S P MC + + lemUnit* : (s : S) (f : P s → Unit* {ℓs}) → f ≡ const tt* + lemUnit* s f i p = Unit*-singleton (f p) i + + u1 : (s : S) (f : P s → Unit* {ℓs}) → u₁ L₀ s f ≡ u₁ L s f + u1 s f i = Unit*-singleton (u₁ L s f) (~ i) + + u2 : (s : S) (f : P s → Unit* {ℓs}) (a : fst A) → u₂ L₀ s f a ≡ u₂ L s f a + u2 s f a i = hcomp (λ j → λ { (i = i0) → s + ; (i = i1) → u₂ L s (lemUnit* s f (~ j)) a }) (unit-ιB-shape₂ L s (~ i) a) + + v1 : (s : S) (f : P s → Unit* {ℓs}) (a : fst A) → + PathP (λ i → P (u2 s f a i) → P s) + (v₁ L₀ {s} {f} a) + (v₁ L {s} {f} a) + v1 s f a i p = compPathP' {B = (λ x → P x → P s)} side2 side1 i p + where + side1 : PathP (λ i → P (u₂ L s (lemUnit* s f (~ i)) a) → P s) + (v₁ L {s} {const tt*} a) + (v₁ L {s} {f} a) + side1 i p = v₁ L {s} {lemUnit* s f (~ i)} a p + + side2 : PathP (λ i → P (unit-ιB-shape₂ L s (~ i) a) → P s) + (λ p → p) + (v₁ L {s} {const tt*} a) + side2 i p = unit-ιB-pos₁ L s (~ i) a p + + v2 : (s : S) (f : P s → Unit* {ℓs}) (a : fst A) → + PathP (λ i → P (u2 s f a i) → fst A) + (v₂ L₀ {s} {f} a) + (v₂ L {s} {f} a) + v2 s f a i p = compPathP' {B = (λ x → P x → fst A)} side2 side1 i p + where + side1 : PathP (λ i → P (u₂ L s (lemUnit* s f (~ i)) a) → fst A) + (v₂ L {s} {const tt*} a) + (v₂ L {s} {f} a) + side1 i p = v₂ L {s} {lemUnit* s f (~ i)} a p + + side2 : PathP (λ i → P (unit-ιB-shape₂ L s (~ i) a) → fst A) + (λ _ → a) + (v₂ L {s} {const tt*} a) + side2 i p = unit-ιB-pos₂ L s (~ i) a p + +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.Monoid.Instances.Nat + +-- An example of a distributive law, this one is not unique for specific S ▷ P +WriterDistr : (A S : Type ℓs) (P : S → Type ℓp) {setA : isSet A} {setS : isSet S} {setP : ∀ {s} → isSet (P s)} + (mon : MonoidStr A) → (MC : MndContainer {ℓs} {ℓp} (S ◁ P & setS & setP)) → + MndDistributiveLaw {ℓs} {ℓp} A (const Unit*) setA isSetUnit* S P setS setP (WriterM (A , setA) mon) MC +u₁ (WriterDistr A S P mon MC) a s = s tt* +u₂ (WriterDistr A S P mon MC) a s _ = a +v₁ (WriterDistr A S P mon MC) _ tt* = tt* +v₂ (WriterDistr A S P mon MC) p tt* = p +unit-ιB-shape₁ (WriterDistr A S P mon MC) a = refl +unit-ιB-shape₂ (WriterDistr A S P mon MC) a = refl +unit-ιB-pos₁ (WriterDistr A S P mon MC) a i p tt* = tt* +unit-ιB-pos₂ (WriterDistr A S P mon MC) a i p tt* = p +unit-ιA-shape₁ (WriterDistr A S P mon MC) s = refl +unit-ιA-shape₂ (WriterDistr A S P mon MC) s = refl +unit-ιA-pos₁ (WriterDistr A S P mon MC) s i p tt* = tt* +unit-ιA-pos₂ (WriterDistr A S P mon MC) s i p tt* = p +mul-A-shape₁ (WriterDistr A S P mon MC) a f g = refl +mul-A-shape₂ (WriterDistr A S P mon MC) a f g = refl +mul-A-pos₁ (WriterDistr A S P mon MC) a f g i p tt* = tt* +mul-A-pos₂₁ (WriterDistr A S P mon MC) a f g i p tt* = tt* +mul-A-pos₂₂ (WriterDistr A S P mon MC) a f g i p tt* = p +mul-B-shape₁ (WriterDistr A S P mon MC) a f g = refl +mul-B-shape₂ (WriterDistr A S P mon MC) a f g = refl +mul-B-pos₁ (WriterDistr A S P mon MC) a f g i p tt* = tt* +mul-B-pos₂₁ (WriterDistr A S P mon MC) a f g i p tt* = pr₁ MC (f tt*) (g tt*) p +mul-B-pos₂₂ (WriterDistr A S P mon MC) a f g i p tt* = pr₂ MC (f tt*) (g tt*) p diff --git a/Cubical/Algebra/DistributiveLaw/MndDir.agda b/Cubical/Algebra/DistributiveLaw/MndDir.agda new file mode 100644 index 0000000000..ac78400daa --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/MndDir.agda @@ -0,0 +1,6 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.MndDir where + +open import Cubical.Algebra.DistributiveLaw.MndDir.Base public +open import Cubical.Algebra.DistributiveLaw.MndDir.Examples public diff --git a/Cubical/Algebra/DistributiveLaw/MndDirDistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw/MndDir/Base.agda similarity index 98% rename from Cubical/Algebra/DistributiveLaw/MndDirDistributiveLaw.agda rename to Cubical/Algebra/DistributiveLaw/MndDir/Base.agda index 33cc3fcba6..b9c09d14e7 100644 --- a/Cubical/Algebra/DistributiveLaw/MndDirDistributiveLaw.agda +++ b/Cubical/Algebra/DistributiveLaw/MndDir/Base.agda @@ -1,6 +1,6 @@ {-# OPTIONS --safe #-} -module Cubical.Algebra.DistributiveLaw.MndDirDistributiveLaw where +module Cubical.Algebra.DistributiveLaw.MndDir.Base where open import Cubical.Foundations.Function open import Cubical.Foundations.Prelude diff --git a/Cubical/Algebra/DistributiveLaw/MndDir/Examples.agda b/Cubical/Algebra/DistributiveLaw/MndDir/Examples.agda new file mode 100644 index 0000000000..7b8a971d13 --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/MndDir/Examples.agda @@ -0,0 +1,124 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.MndDir.Examples where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Algebra.DistributiveLaw.MndDir.Base +open import Cubical.Algebra.DistributiveLaw.Mnd.Examples using (Unit*-singleton) +open import Cubical.Algebra.DirContainer.Examples +open import Cubical.Algebra.MndContainer.Examples +open import Cubical.Data.Unit + +open MndDirDistributiveLaw + +private + variable + ℓs ℓp : Level + +WriterCReaderMDistr : (A : Type ℓs) {setA : isSet A} (B : hSet ℓp) → + MndDirDistributiveLaw {ℓs} {ℓp} A (const (Unit* {ℓp})) setA isSetUnit* + (Unit* {ℓs}) (const (fst B)) isSetUnit* (snd B) (WriterC (A , setA)) (ReaderM B) +u₁ (WriterCReaderMDistr A B) a f = tt* +u₂ (WriterCReaderMDistr A B) a f b = a +v₁ (WriterCReaderMDistr A B) b tt* = tt* +v₂ (WriterCReaderMDistr A B) b tt* = b +unit-oA-shape (WriterCReaderMDistr A B) a f i = Unit*-singleton (f tt*) (~ i) +unit-oA-pos₁ (WriterCReaderMDistr A B) a f i b = tt* +unit-oA-pos₂ (WriterCReaderMDistr A B) a f i b = b +mul-A-shape₁ (WriterCReaderMDistr A B) a f = refl +mul-A-shape₂ (WriterCReaderMDistr A B) a f = refl +mul-A-shape₃ (WriterCReaderMDistr A B) a f i b tt* = a +mul-A-pos₁ (WriterCReaderMDistr A B) s f i b tt* tt* = tt* +mul-A-pos₂ (WriterCReaderMDistr A B) s f i b tt* tt* = b +unit-ιB-shape₁ (WriterCReaderMDistr A B) a = refl +unit-ιB-shape₂ (WriterCReaderMDistr A B) a = refl +unit-ιB-pos₁ (WriterCReaderMDistr A B) a i b tt* = tt* +unit-ιB-pos₂ (WriterCReaderMDistr A B) a i b tt* = b +mul-B-shape₁ (WriterCReaderMDistr A B) a f g = refl +mul-B-shape₂ (WriterCReaderMDistr A B) a f g = refl +mul-B-pos₁ (WriterCReaderMDistr A B) a f g i b tt* = tt* +mul-B-pos₂₁ (WriterCReaderMDistr A B) a f g i b tt* = b +mul-B-pos₂₂ (WriterCReaderMDistr A B) a f g i b tt* = b + +module WriterCReaderMDistrUnique (A : Type ℓs) {setA : isSet A} (B : hSet ℓp) + (L : MndDirDistributiveLaw {ℓs} {ℓp} A (const (Unit* {ℓp})) setA isSetUnit* + (Unit* {ℓs}) (const (fst B)) isSetUnit* (snd B) (WriterC (A , setA)) (ReaderM B)) where + + L₀ = WriterCReaderMDistr A {setA} B + + lemUnit* : (a : A) (f : Unit* {ℓp} → Unit* {ℓs}) → f ≡ const tt* + lemUnit* a f i p = Unit*-singleton (f p) i + + u1 : (a : A) (f : Unit* {ℓp} → Unit* {ℓs}) → u₁ L₀ a f ≡ u₁ L a f + u1 a f i = Unit*-singleton (u₁ L a f) (~ i) + + u2 : (a : A) (f : Unit* {ℓp} → Unit* {ℓs}) (b : fst B) → u₂ L₀ a f b ≡ u₂ L a f b + u2 a f b i = hcomp (λ j → λ { (i = i0) → a + ; (i = i1) → u₂ L a (lemUnit* a f (~ j)) b }) (unit-ιB-shape₂ L a (~ i) b) + + v1 : (a : A) (f : Unit* {ℓp} → Unit* {ℓs}) (b : fst B) (x : Unit* {ℓp}) → v₁ L₀ {a} {f} b x ≡ v₁ L {a} {f} b x + v1 a f b tt* i = hcomp (λ j → λ { (i = i0) → tt* + ; (i = i1) → v₁ L {a} {lemUnit* a f (~ j)} b tt* }) (unit-ιB-pos₁ L a (~ i) b tt*) + + v2 : (a : A) (f : Unit* {ℓp} → Unit* {ℓs}) (b : fst B) (x : Unit* {ℓp}) → v₂ L₀ {a} {f} b x ≡ v₂ L {a} {f} b x + v2 a f b tt* i = hcomp (λ j → λ { (i = i0) → b + ; (i = i1) → v₂ L {a} {lemUnit* a f (~ j)} b tt* }) (unit-ιB-pos₂ L a (~ i) b tt*) + + +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.Monoid.Instances.Nat + +record MonoidFuncAction {ℓa ℓb : Level} (A : Type ℓa) (B : Type ℓb) + (monA : MonoidStr A) (monB : MonoidStr B) : + Type (ℓ-suc (ℓ-max ℓa ℓb)) where + open MonoidStr monA renaming (ε to eᴬ ; _·_ to _⊕ᴬ_) + open MonoidStr monB renaming (ε to eᴮ ; _·_ to _⊕ᴮ_) + field + χ : (A → B) → A → A + eᴬ-pres : (f : A → B) → χ f eᴬ ≡ eᴬ + ⊕ᴬ-pres : (f : A → B) (a a' : A) → + χ f (a ⊕ᴬ a') ≡ χ f a ⊕ᴬ χ (λ x → f (χ f a ⊕ᴬ x)) a' + eᴮ-pres : (a : A) → χ (const eᴮ) a ≡ a + ⊕ᴮ-pres : (f g : A → B) (a : A) → χ (λ x → f x ⊕ᴮ g x) a ≡ χ f (χ (λ x → g (χ f x)) a) + +open import Cubical.Algebra.DirContainer.Base +open import Cubical.Algebra.Semigroup +open MonoidFuncAction +open MonoidStr +open DirContainer +open IsMonoid +open IsSemigroup + +ReaderCWriterMDistr : (A : Type ℓp) (B : Type ℓs) {setB : isSet B} → + (monA : MonoidStr A) (monB : MonoidStr B) → + (t : MonoidFuncAction A B monA monB) → + MndDirDistributiveLaw {ℓs} {ℓp} Unit* (const A) isSetUnit* (monA .isMonoid .isSemigroup .is-set) + B (const Unit*) setB isSetUnit* (ReaderC A monA) (WriterM (B , setB) monB) +u₁ (ReaderCWriterMDistr {ℓs} {ℓp} A B monA monB t) tt* f = f (o (ReaderC {ℓs} {ℓp} A monA) tt*) +u₂ (ReaderCWriterMDistr A B monA monB t) tt* f tt* = tt* +v₁ (ReaderCWriterMDistr A B monA monB t) {tt*} {f} tt* a = χ t f a +v₂ (ReaderCWriterMDistr A B monA monB t) {tt*} {f} tt* a = tt* +unit-oA-shape (ReaderCWriterMDistr A B monA monB t) tt* f = refl +unit-oA-pos₁ (ReaderCWriterMDistr A B monA monB t) tt* f i tt* = eᴬ-pres t f i +unit-oA-pos₂ (ReaderCWriterMDistr A B monA monB t) tt* f i tt* = tt* +mul-A-shape₁ (ReaderCWriterMDistr A B monA monB t) tt* f i = f (monA .·IdL (monA .ε) (~ i) ) +mul-A-shape₂ (ReaderCWriterMDistr A B monA monB t) tt* f i tt* = tt* +mul-A-shape₃ (ReaderCWriterMDistr A B monA monB t) tt* f i tt* a = tt* +mul-A-pos₁ (ReaderCWriterMDistr A B monA monB t) tt* f i tt* a a' = (⊕ᴬ-pres t f a a' ∙ sym lem) i + where + lem : (monA · χ t (λ p → f ((monA · p) (monA .ε))) a) (χ t (λ p' → f ((monA · χ t (λ p → f ((monA · p) (monA .ε))) a) p')) a') + ≡ (monA · χ t f a) (χ t (λ x → f ((monA · χ t f a) x)) a') + lem i = (monA · χ t (λ p → f (monA .·IdR p i)) a) (χ t (λ x → f ((monA · χ t (λ p → f (monA .·IdR p i)) a) x)) a') +mul-A-pos₂ (ReaderCWriterMDistr A B monA monB t) tt* f i tt* a a' = tt* +unit-ιB-shape₁ (ReaderCWriterMDistr A B monA monB t) tt* = refl +unit-ιB-shape₂ (ReaderCWriterMDistr A B monA monB t) tt* i tt* = tt* +unit-ιB-pos₁ (ReaderCWriterMDistr A B monA monB t) tt* i tt* a = eᴮ-pres t a i +unit-ιB-pos₂ (ReaderCWriterMDistr A B monA monB t) tt* i tt* a = tt* +mul-B-shape₁ (ReaderCWriterMDistr A B monA monB t) tt* f g i = (monB · f (monA .ε)) (g (eᴬ-pres t f (~ i)) tt*) +mul-B-shape₂ (ReaderCWriterMDistr A B monA monB t) tt* f g i tt* = tt* +mul-B-pos₁ (ReaderCWriterMDistr A B monA monB t) tt* f g i tt* a = ⊕ᴮ-pres t f (λ x → g x tt*) a i +mul-B-pos₂₁ (ReaderCWriterMDistr A B monA monB t) tt* f g i tt* a = tt* +mul-B-pos₂₂ (ReaderCWriterMDistr A B monA monB t) tt* f g i tt* a = tt* + diff --git a/Cubical/Algebra/MndContainer/Examples.agda b/Cubical/Algebra/MndContainer/Examples.agda index ba72e5b980..8d114f32a0 100644 --- a/Cubical/Algebra/MndContainer/Examples.agda +++ b/Cubical/Algebra/MndContainer/Examples.agda @@ -13,7 +13,6 @@ open import Cubical.Data.Bool open import Cubical.Data.Empty open import Cubical.Data.Sum - private variable ℓs ℓp ℓ ℓ' ℓ'' : Level @@ -34,16 +33,6 @@ isSetJustOrNothing {_} {_} {lift true} = isSetUnit* Maybe : SetCon {ℓs} {ℓp} Maybe {ℓs} {ℓp} = Bool* {ℓs} ◁ JustOrNothing {ℓs} {ℓp} & isSetBool* & (λ {s} → isSetJustOrNothing {_} {_} {s}) - where - isSetBool* : isSet (Bool* {ℓ}) - isSetBool* {ℓ} a b = J (λ _ p → ∀ q → p ≡ q) (K-Bool* {ℓ} (refl ≡_) refl) - where - K-Bool* - : ∀ {ℓ} → (P : {b : Bool* {ℓ}} → b ≡ b → Type ℓ) - → (∀{b} → P {b} refl) - → ∀{b} → (q : b ≡ b) → P q - K-Bool* P Pr {lift false} = J (λ{ (lift false) q → P q ; (lift true) _ → Lift ⊥ }) Pr - K-Bool* P Pr {lift true} = J (λ{ (lift true) q → P q ; (lift false) _ → Lift ⊥ }) Pr LOrR : {A : Type ℓ} {B : Type ℓ'} → A ⊎ B → Type ℓ'' LOrR (inl a) = Unit* diff --git a/Cubical/Data/Bool/Properties.agda b/Cubical/Data/Bool/Properties.agda index 276af18567..b2407b226f 100644 --- a/Cubical/Data/Bool/Properties.agda +++ b/Cubical/Data/Bool/Properties.agda @@ -73,6 +73,16 @@ K-Bool P Pr {true} = J (λ{ true q → P q ; false _ → Lift ⊥ }) Pr isSetBool : isSet Bool isSetBool a b = J (λ _ p → ∀ q → p ≡ q) (K-Bool (refl ≡_) refl) +K-Bool* + : ∀ {ℓ} → (P : {b : Bool* {ℓ}} → b ≡ b → Type ℓ) + → (∀{b} → P {b} refl) + → ∀{b} → (q : b ≡ b) → P q +K-Bool* P Pr {lift false} = J (λ{ (lift false) q → P q ; (lift true) _ → Lift ⊥ }) Pr +K-Bool* P Pr {lift true} = J (λ{ (lift true) q → P q ; (lift false) _ → Lift ⊥ }) Pr + +isSetBool* : isSet (Bool* {ℓ}) +isSetBool* {ℓ} a b = J (λ _ p → ∀ q → p ≡ q) (K-Bool* {ℓ} (refl ≡_) refl) + true≢false : ¬ true ≡ false true≢false p = subst (λ b → if b then Bool else ⊥) p true From 808b1f82f532284af9dfa212ed6acc3dcddceb36 Mon Sep 17 00:00:00 2001 From: Stefania Damato Date: Mon, 2 Jun 2025 18:57:38 +0100 Subject: [PATCH 07/11] No-go theorem --- Cubical/Algebra/DistributiveLaw.agda | 2 + .../Algebra/DistributiveLaw/NoGoTheorem.agda | 232 ++++++++++++++++++ 2 files changed, 234 insertions(+) create mode 100644 Cubical/Algebra/DistributiveLaw/NoGoTheorem.agda diff --git a/Cubical/Algebra/DistributiveLaw.agda b/Cubical/Algebra/DistributiveLaw.agda index 4ea4be1ebd..50a1c5aef3 100644 --- a/Cubical/Algebra/DistributiveLaw.agda +++ b/Cubical/Algebra/DistributiveLaw.agda @@ -9,3 +9,5 @@ open import Cubical.Algebra.DistributiveLaw.Dir public open import Cubical.Algebra.DistributiveLaw.MndDir public open import Cubical.Algebra.DistributiveLaw.DirMnd public +open import Cubical.Algebra.DistributiveLaw.NoGoTheorem public + diff --git a/Cubical/Algebra/DistributiveLaw/NoGoTheorem.agda b/Cubical/Algebra/DistributiveLaw/NoGoTheorem.agda new file mode 100644 index 0000000000..246b4382f5 --- /dev/null +++ b/Cubical/Algebra/DistributiveLaw/NoGoTheorem.agda @@ -0,0 +1,232 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.DistributiveLaw.NoGoTheorem where + +open import Cubical.Foundations.Function +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Transport +open import Cubical.Data.Nat +open import Cubical.Data.Fin +open import Cubical.Data.Sigma +open import Cubical.Data.Sum hiding (rec) +open import Cubical.Data.Empty +open import Cubical.Data.Containers.Set.Base +open import Cubical.Algebra.MndContainer.Base +open import Cubical.Algebra.DistributiveLaw.Mnd +open import Cubical.Relation.Nullary + +open MndContainer +open IsMndContainer +open MndDistributiveLaw + +private + variable + ℓs ℓp : Level + +-- Helper functions for the no-go theorem + +case : ∀ {ℓ ℓ'} {P : Type ℓ} {A : Type ℓ'} → A → A → (Dec P) → A +case ifyes ifno (yes _) = ifyes +case ifyes ifno (no _) = ifno + +cased : ∀ {ℓ ℓ' ℓ''} {P : Type ℓ} {A : Type ℓ'} {B : A → Type ℓ''} + → (a a' : A) (b : B a) (b' : B a') + → (p : Dec P) → B (case a a' p) +cased _ _ ifyes ifno (yes _) = ifyes +cased _ _ ifyes ifno (no _) = ifno + +decLem₁ : {ℓa ℓb ℓc ℓp : Level} {A : Type ℓa} {B : A → Type ℓb} {C : Type ℓc} + {P : Type ℓp} (dec : Discrete P) + (a₁ a₂ : A) (b₁ : B a₁) (b₂ : B a₂) (g : (a : A) → B a → C) + (p p' : P) + → case (g a₁ b₁) (g a₂ b₂) (dec p p') + ≡ g (case a₁ a₂ (dec p p')) (cased a₁ a₂ b₁ b₂ (dec p p')) +decLem₁ dec a₁ a₂ b₁ b₂ g p p' i with dec p p' +... | (yes _) = g a₁ b₁ +... | (no _) = g a₂ b₂ + +decLem₂ : {ℓa ℓb ℓc ℓp : Level} {A : Type ℓa} {B : A → Type ℓb} {C : Type ℓc} + {P : Type ℓp} (dec : Discrete P) + (a₁ a₂ : A) (c₁ c₂ : C) + (p p' : P) + → cased {B = λ a → B a → C} a₁ a₂ (const c₁) (const c₂) (dec p p') + ≡ const (case c₁ c₂ (dec p p')) +decLem₂ dec a₁ a₂ c₁ c₂ p p' i with dec p p' +... | (yes _) = const c₁ +... | (no _) = const c₂ + +decLem₃ : {ℓa ℓp : Level} {A : Type ℓa} + {P : Type ℓp} (dec : Discrete P) + (a₁ a₂ a₃ : A) (p₁ p₂ p₃ : P) + (pdist : ¬ (p₁ ≡ p₂)) + → case a₁ (case a₂ a₃ (dec p₃ p₂)) (dec p₃ p₁) + ≡ case a₂ (case a₁ a₃ (dec p₃ p₁)) (dec p₃ p₂) +decLem₃ dec a₁ a₂ a₃ p₁ p₂ p₃ pdist with dec p₃ p₁ | dec p₃ p₂ +... | (yes e) | (yes e') = rec (pdist (sym e ∙ e')) +... | (yes e) | (no e') = refl +... | (no e) | (yes e') = refl +... | (no e) | (no e') = refl + +dec⊤ : {ℓ : Level} → Discrete (Unit* {ℓ}) +dec⊤ tt* tt* = yes refl + +decRefl : {ℓ : Level} {A : Type ℓ} + (dec : Discrete A) (a : A) + → Σ[ e ∈ a ≡ a ] dec a a ≡ yes e +decRefl dec a with dec a a +... | (yes e) = (e , refl) +... | (no e) = rec (e refl) + +transpFun : {ℓa ℓb ℓc : Level} {A : Type ℓa} {B : A → Type ℓb} {C : Type ℓc} + (a a' : A) (e : a ≡ a') + (f : B a → C) + → transport (λ i → B (e i) → C) f ≡ f ∘ transport (λ i → B (e (~ i))) +transpFun {B = B} a a' e f i b = transportRefl (f (transp (λ j → B (e (~ j))) i0 b)) i + +-------- + +ConstantShape : (ℓs ℓp : Level) + (S : Type ℓs) (P : S → Type ℓp) + (s : S) → Type (ℓ-suc ℓp) +ConstantShape _ _ S P s = P s ≡ ⊥* + +record S3Property (S : Type ℓs) (P : S → Type ℓp) {setS : isSet S} {setP : ∀ {s} → isSet (P s)} + (Aₘ : MndContainer (S ◁ P & setS & setP)) + (s : S) (f : P s → S) : Type (ℓ-suc (ℓ-max ℓs ℓp)) where + field + posInhabited : NonEmpty (P s) + decEq : Discrete (P s) + s3Shape : (p : P s) → σ Aₘ s (λ p' → case + (ι Aₘ) + (f p') + (decEq p' p)) ≡ ι Aₘ + s3Pos : (p : P s) → PathP (λ i → P (s3Shape p i) → P s) + (λ p' → pr₁ Aₘ _ _ p') + (λ p' → p) +open S3Property + +compositeS3 : (S : Type ℓs) (P : S → Type ℓp) {setS : isSet S} {setP : ∀ {s} → isSet (P s)} + (Aₘ : MndContainer (S ◁ P & setS & setP)) + (s : S) (f : P s → S) + (s3 : S3Property S P Aₘ s f) + (T : Type ℓs) (Q : T → Type ℓp) {setT : isSet T} {setQ : ∀ {t} → isSet (Q t)} + (Bₘ : MndContainer (T ◁ Q & setT & setQ)) + (distr : MndDistributiveLaw S P setS setP T Q setT setQ Aₘ Bₘ) + (t : T) (p : P s) + → u₁ distr s (λ p' → case t (ι Bₘ) (decEq s3 p' p)) ≡ t +compositeS3 S P Aₘ s f s3 T Q Bₘ distr t p = step₁ ∙ step₂ ∙ step₃ ∙ step₄ ∙ step₅ ∙ unit-ιA-shape₁ distr t + where + step₁ : u₁ distr s (λ p' → case + t + (ι Bₘ) + (decEq s3 p' p)) + ≡ u₁ distr s (λ p' → case + (u₁ distr (ι Aₘ) (λ _ → t)) + (u₁ distr (f p') (λ _ → ι Bₘ)) + (decEq s3 p' p)) + step₁ i = u₁ distr s (λ p' → case + (unit-ιA-shape₁ distr t (~ i)) + (unit-ιB-shape₁ distr (f p') (~ i)) + (decEq s3 p' p)) + + step₂ : u₁ distr s (λ p' → case + (u₁ distr (ι Aₘ) (λ _ → t)) + (u₁ distr (f p') (λ _ → ι Bₘ)) + (decEq s3 p' p)) + ≡ u₁ distr s (λ p' → + u₁ distr (case (ι Aₘ) (f p') (decEq s3 p' p)) + (const (case t (ι Bₘ) (decEq s3 p' p))) + ) + step₂ i = u₁ distr s (λ p' → (decLem₁ (decEq s3) (ι Aₘ) (f p') (const t) (const (ι Bₘ)) (u₁ distr) p' p + ∙ cong (u₁ distr (case (ι Aₘ) (f p') (decEq s3 p' p))) (decLem₂ (decEq s3) _ _ _ _ p' p) + ) i + ) + + step₃ : u₁ distr s (λ p' → u₁ distr + (case (ι Aₘ) (f p') (decEq s3 p' p)) + (const (case t (ι Bₘ) (decEq s3 p' p))) + ) + ≡ u₁ distr + (σ Aₘ s (λ p' → case (ι Aₘ) (f p') (decEq s3 p' p))) + (λ p' → case t (ι Bₘ) (decEq s3 (pr₁ Aₘ _ _ p') p)) + step₃ i = mul-A-shape₁ distr s (λ p' → case (ι Aₘ) (f p') (decEq s3 p' p)) (λ p₁ _ → case t (ι Bₘ) (decEq s3 p₁ p)) (~ i) + + step₄ : u₁ distr + (σ Aₘ s (λ p' → case (ι Aₘ) (f p') (decEq s3 p' p))) + (λ p' → case t (ι Bₘ) (decEq s3 (pr₁ Aₘ _ _ p') p)) + ≡ u₁ distr (ι Aₘ) (λ p' → case t (ι Bₘ) (decEq s3 p p)) + step₄ i = u₁ distr (s3Shape s3 p i) (λ p' → case t (ι Bₘ) (decEq s3 (s3Pos s3 p i p') p)) + + step₅ : u₁ distr (ι Aₘ) (λ p' → case t (ι Bₘ) (decEq s3 p p)) + ≡ u₁ distr (ι Aₘ) (const t) + step₅ i = u₁ distr (ι Aₘ) (λ p' → case t (ι Bₘ) (snd (decRefl (decEq s3) p) i)) + +module _ (S : Type ℓs) (P : S → Type ℓp) {setS : isSet S} {setP : ∀ {s} → isSet (P s)} + (Aₘ : MndContainer (S ◁ P & setS & setP)) + (s : S) (f : P s → S) + (s3 : S3Property S P Aₘ s f) + (T : Type ℓs) (Q : T → Type ℓp) {setT : isSet T} {setQ : ∀ {t} → isSet (Q t)} + (Bₘ : MndContainer (T ◁ Q & setT & setQ)) + (distr : MndDistributiveLaw S P setS setP T Q setT setQ Aₘ Bₘ) where + + step₁ : (t t' : T) (constt : ConstantShape _ _ _ Q t) + (p p' : P s) + → σ Bₘ t (const (ι Bₘ)) + ≡ σ Bₘ (u₁ distr s (λ y → case t (ι Bₘ) (decEq s3 y p))) + (λ y → u₁ distr (u₂ distr s (λ z → case t (ι Bₘ) (decEq s3 z p)) y) + (λ z → case t' (ι Bₘ) (decEq s3 (v₁ distr y z) p')) + ) + step₁ t t' constt p p' i = σ Bₘ (compositeS3 S P Aₘ s f s3 T Q Bₘ distr t p (~ i)) + (toPathP {A = λ i → Q (compositeS3 S P Aₘ s f s3 T Q Bₘ distr t p (~ i)) → T} + {x = const (ι Bₘ)} + {y = λ y → u₁ distr (u₂ distr s (λ z → case t (ι Bₘ) (decEq s3 z p)) y) + (λ z → case t' (ι Bₘ) (decEq s3 (v₁ distr y z) p')) + } + (transpFun {B = Q} _ _ (sym (compositeS3 S P Aₘ s f s3 T Q Bₘ distr t p)) (const (ι Bₘ)) + ∙ funExt (λ x → rec* (transport constt (subst⁻ Q (sym (compositeS3 S P Aₘ s f s3 T Q Bₘ distr t p)) x))) + ) + i + ) + + step₂ : (t t' : T) (p p' : P s) + → σ Bₘ (u₁ distr s (λ y → case t (ι Bₘ) (decEq s3 y p))) + (λ y → u₁ distr (u₂ distr s (λ z → case t (ι Bₘ) (decEq s3 z p)) y) + (λ z → case t' (ι Bₘ) (decEq s3 (v₁ distr y z) p')) + ) + ≡ u₁ distr s (λ y → σ Bₘ (case t (ι Bₘ) (decEq s3 y p)) (const (case t' (ι Bₘ) (decEq s3 y p')))) + step₂ t t' p p' = sym (mul-B-shape₁ distr _ _ _) + + step₃Aux : (t t' : T) (p p' : P s) (pdist : ¬ (p ≡ p')) + (y : P s) + → σ Bₘ (case t (ι Bₘ) (decEq s3 y p)) (const (case t' (ι Bₘ) (decEq s3 y p'))) + ≡ case t (case t' (ι Bₘ) (decEq s3 y p')) (decEq s3 y p) + step₃Aux t t' p p' pdist y with decEq s3 y p | decEq s3 y p' + ... | (yes e) | (yes e') = rec (pdist (sym e ∙ e')) + ... | (yes e) | (no e') = unit-r (isMndContainer Bₘ) t + ... | (no e) | (yes e') = unit-l (isMndContainer Bₘ) t' + ... | (no e) | (no e') = unit-r (isMndContainer Bₘ) (ι Bₘ) + + step₃ : (t t' : T) (p p' : P s) (pdist : ¬ (p ≡ p')) + → u₁ distr s (λ y → σ Bₘ (case t (ι Bₘ) (decEq s3 y p)) (const (case t' (ι Bₘ) (decEq s3 y p')))) + ≡ u₁ distr s (λ y → case t (case t' (ι Bₘ) (decEq s3 y p')) (decEq s3 y p)) + step₃ t t' p p' pdist i = u₁ distr s (λ y → step₃Aux t t' p p' pdist y i) + + mainLem : (t t' : T) (constt : ConstantShape _ _ _ Q t) + (p p' : P s) (pdist : ¬ (p ≡ p')) + → t ≡ u₁ distr s (λ y → case t (case t' (ι Bₘ) (decEq s3 y p')) (decEq s3 y p)) + mainLem t t' constt p p' pdist = sym (unit-r (isMndContainer Bₘ) t) ∙ step₁ t t' constt p p' ∙ step₂ t t' p p' ∙ step₃ t t' p p' pdist + + noGoTheorem : (t t' : T) (tdist : ¬ (t ≡ t')) + (constt : ConstantShape _ _ _ Q t) + (constt' : ConstantShape _ _ _ Q t') + (p p' : P s) (pdist : ¬ (p ≡ p')) + → ⊥ + noGoTheorem t t' tdist constt constt' p p' pdist = tdist (mainLem t t' constt p p' pdist + ∙ aux + ∙ sym (mainLem t' t constt' p' p (pdist ∘ sym)) + ) + where + aux : u₁ distr s (λ y → case t (case t' (ι Bₘ) (decEq s3 y p')) (decEq s3 y p)) + ≡ u₁ distr s (λ y → case t' (case t (ι Bₘ) (decEq s3 y p)) (decEq s3 y p')) + aux i = u₁ distr s (λ y → decLem₃ (decEq s3) t t' (ι Bₘ) p p' y pdist i) From c6deb6065733b7189f3160540a39697d40b74062 Mon Sep 17 00:00:00 2001 From: Stefania Damato Date: Tue, 3 Jun 2025 11:05:10 +0100 Subject: [PATCH 08/11] Minor (levels) --- Cubical/Algebra/DistributiveLaw/NoGoTheorem.agda | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/Cubical/Algebra/DistributiveLaw/NoGoTheorem.agda b/Cubical/Algebra/DistributiveLaw/NoGoTheorem.agda index 246b4382f5..2451ae11c1 100644 --- a/Cubical/Algebra/DistributiveLaw/NoGoTheorem.agda +++ b/Cubical/Algebra/DistributiveLaw/NoGoTheorem.agda @@ -86,10 +86,9 @@ transpFun {B = B} a a' e f i b = transportRefl (f (transp (λ j → B (e (~ j))) -------- -ConstantShape : (ℓs ℓp : Level) - (S : Type ℓs) (P : S → Type ℓp) +ConstantShape : (S : Type ℓs) (P : S → Type ℓp) (s : S) → Type (ℓ-suc ℓp) -ConstantShape _ _ S P s = P s ≡ ⊥* +ConstantShape S P s = P s ≡ ⊥* record S3Property (S : Type ℓs) (P : S → Type ℓp) {setS : isSet S} {setP : ∀ {s} → isSet (P s)} (Aₘ : MndContainer (S ◁ P & setS & setP)) @@ -170,7 +169,7 @@ module _ (S : Type ℓs) (P : S → Type ℓp) {setS : isSet S} {setP : ∀ {s} (Bₘ : MndContainer (T ◁ Q & setT & setQ)) (distr : MndDistributiveLaw S P setS setP T Q setT setQ Aₘ Bₘ) where - step₁ : (t t' : T) (constt : ConstantShape _ _ _ Q t) + step₁ : (t t' : T) (constt : ConstantShape _ Q t) (p p' : P s) → σ Bₘ t (const (ι Bₘ)) ≡ σ Bₘ (u₁ distr s (λ y → case t (ι Bₘ) (decEq s3 y p))) @@ -212,14 +211,14 @@ module _ (S : Type ℓs) (P : S → Type ℓp) {setS : isSet S} {setP : ∀ {s} ≡ u₁ distr s (λ y → case t (case t' (ι Bₘ) (decEq s3 y p')) (decEq s3 y p)) step₃ t t' p p' pdist i = u₁ distr s (λ y → step₃Aux t t' p p' pdist y i) - mainLem : (t t' : T) (constt : ConstantShape _ _ _ Q t) + mainLem : (t t' : T) (constt : ConstantShape _ Q t) (p p' : P s) (pdist : ¬ (p ≡ p')) → t ≡ u₁ distr s (λ y → case t (case t' (ι Bₘ) (decEq s3 y p')) (decEq s3 y p)) mainLem t t' constt p p' pdist = sym (unit-r (isMndContainer Bₘ) t) ∙ step₁ t t' constt p p' ∙ step₂ t t' p p' ∙ step₃ t t' p p' pdist noGoTheorem : (t t' : T) (tdist : ¬ (t ≡ t')) - (constt : ConstantShape _ _ _ Q t) - (constt' : ConstantShape _ _ _ Q t') + (constt : ConstantShape _ Q t) + (constt' : ConstantShape _ Q t') (p p' : P s) (pdist : ¬ (p ≡ p')) → ⊥ noGoTheorem t t' tdist constt constt' p p' pdist = tdist (mainLem t t' constt p p' pdist From 992eb807c7e40257afb8d41b1909b567ee80fd00 Mon Sep 17 00:00:00 2001 From: chrisjpurdy <33040507+chrisjpurdy@users.noreply.github.com> Date: Thu, 5 Jun 2025 11:38:56 +0100 Subject: [PATCH 09/11] Add set container to generalised container on set proofs --- Cubical/Data/Containers.agda | 1 + Cubical/Data/Containers/Set/Properties.agda | 77 +++++++++++++++++++++ 2 files changed, 78 insertions(+) create mode 100644 Cubical/Data/Containers/Set/Properties.agda diff --git a/Cubical/Data/Containers.agda b/Cubical/Data/Containers.agda index 8bf611fb8f..02a2973af3 100644 --- a/Cubical/Data/Containers.agda +++ b/Cubical/Data/Containers.agda @@ -3,6 +3,7 @@ module Cubical.Data.Containers where open import Cubical.Data.Containers.Set.Base public +open import Cubical.Data.Containers.Set.Properties public open import Cubical.Data.Containers.Generalised.Base public open import Cubical.Data.Containers.Algebras public diff --git a/Cubical/Data/Containers/Set/Properties.agda b/Cubical/Data/Containers/Set/Properties.agda new file mode 100644 index 0000000000..c17f5300b8 --- /dev/null +++ b/Cubical/Data/Containers/Set/Properties.agda @@ -0,0 +1,77 @@ +{-# OPTIONS --safe #-} + +module Cubical.Data.Containers.Set.Properties where + +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧) +open import Cubical.Foundations.Prelude hiding (_◁_) +open import Cubical.Foundations.Isomorphism +open import Cubical.Data.Containers.Generalised.Base +open import Cubical.Categories.Instances.Sets +open import Cubical.HITs.PropositionalTruncation +open import Cubical.Categories.Equivalence.Base +open import Cubical.Data.Containers.Set.Base + +open Iso +open SetCon +open GenContainer +open _⇒ᶜ_ +open Functor + +-- Type of SetCont is iso to GenContainer SET +setToGenCont : ∀ {ℓ} → Iso (SetCon {ℓ} {ℓ}) (GenContainer (SET ℓ)) +S (fun setToGenCont C) = Shape C +P (fun setToGenCont C) s = (Position C s , isSetPos C) +isSetS (fun setToGenCont C) = isSetShape C +Shape (inv setToGenCont C) = S C +Position (inv setToGenCont C) s = fst (P C s) +isSetShape (inv setToGenCont C) = isSetS C +isSetPos (inv setToGenCont C) {s} = snd (P C s) +rightInv setToGenCont _ = refl +leftInv setToGenCont _ = refl + +open Conts +open _≃ᶜ_ +open _⇒c_ + +-- Category of set containers is equivalent to category of generalised containers on SET +equivSetContGenContSet : ∀ {ℓ} → SetCont {ℓ} {ℓ} ≃ᶜ Cont (SET ℓ) +F-ob (func equivSetContGenContSet) = fun setToGenCont +shape (F-hom (func equivSetContGenContSet) g) = u g +pos (F-hom (func equivSetContGenContSet) g) = f g +F-id (func equivSetContGenContSet) = refl +shape (F-seq (func equivSetContGenContSet) g h i) s = u h (u g s) +pos (F-seq (func equivSetContGenContSet) g h i) s p = f g s (f h (u g s) p) +isEquiv (equivSetContGenContSet {ℓ}) = ∣ winv ∣₁ + where + open WeakInverse + winv : WeakInverse {ℓ-suc ℓ} {ℓ} {ℓ-suc (ℓ-suc ℓ)} {ℓ-suc (ℓ-suc ℓ)} + {SetCont {ℓ} {ℓ}} {Cont {ℓ-suc ℓ} {ℓ} (SET ℓ)} (func equivSetContGenContSet) + F-ob (invFunc winv) = inv setToGenCont + u (F-hom (invFunc winv) g) = shape g + f (F-hom (invFunc winv) g) = pos g + F-id (invFunc winv) = refl + u (F-seq (invFunc winv) g h i) s = shape h (shape g s) + f (F-seq (invFunc winv) g h i) s p = pos g s (pos h (shape g s) p) + u (NatTrans.N-ob (NatIso.trans (η winv)) C) s = s + f (NatTrans.N-ob (NatIso.trans (η winv)) C) s p = p + u (NatTrans.N-hom (NatIso.trans (η winv)) g i) s = u g s + f (NatTrans.N-hom (NatIso.trans (η winv)) g i) s p = f g s p + u (isIso.inv (NatIso.nIso (η winv) C)) s = s + f (isIso.inv (NatIso.nIso (η winv) C)) s p = p + u (isIso.sec (NatIso.nIso (η winv) C) i) s = s + f (isIso.sec (NatIso.nIso (η winv) C) i) s p = p + u (isIso.ret (NatIso.nIso (η winv) C) i) s = s + f (isIso.ret (NatIso.nIso (η winv) C) i) s p = p + shape (NatTrans.N-ob (NatIso.trans (ε winv)) C) s = s + pos (NatTrans.N-ob (NatIso.trans (ε winv)) C) s p = p + shape (NatTrans.N-hom (NatIso.trans (ε winv)) g i) s = shape g s + pos (NatTrans.N-hom (NatIso.trans (ε winv)) g i) s p = pos g s p + shape (isIso.inv (NatIso.nIso (ε winv) C)) s = s + pos (isIso.inv (NatIso.nIso (ε winv) C)) s p = p + shape (isIso.sec (NatIso.nIso (ε winv) C) i) s = s + pos (isIso.sec (NatIso.nIso (ε winv) C) i) s p = p + shape (isIso.ret (NatIso.nIso (ε winv) C) i) s = s + pos (isIso.ret (NatIso.nIso (ε winv) C) i) s p = p From c889399dd0891e9a54d6d91559f65e1a1aba6f30 Mon Sep 17 00:00:00 2001 From: chrisjpurdy <33040507+chrisjpurdy@users.noreply.github.com> Date: Thu, 5 Jun 2025 17:33:54 +0100 Subject: [PATCH 10/11] Work towards bijection between monad containers and monads over container functors --- Cubical/Algebra/MndContainer/Properties.agda | 68 ++++++++++++++++++++ Cubical/Categories/Instances/Sets.agda | 17 +++++ 2 files changed, 85 insertions(+) create mode 100644 Cubical/Algebra/MndContainer/Properties.agda diff --git a/Cubical/Algebra/MndContainer/Properties.agda b/Cubical/Algebra/MndContainer/Properties.agda new file mode 100644 index 0000000000..3bdc58696f --- /dev/null +++ b/Cubical/Algebra/MndContainer/Properties.agda @@ -0,0 +1,68 @@ +{-# OPTIONS --safe #-} + +module Cubical.Algebra.MndContainer.Properties where + +open import Cubical.Foundations.Prelude hiding (_▷_) renaming (fst to π₁ ; snd to π₂) +open import Cubical.Foundations.Function +open import Cubical.Algebra.MndContainer.Base +open import Cubical.Data.Sigma +open import Cubical.Data.Containers.Set.Base +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels + +open import Cubical.Categories.Functor +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Monad.Base +open import Cubical.Categories.NaturalTransformation.Base +open import Cubical.Categories.NaturalTransformation.Properties +open import Cubical.Categories.Instances.Sets + +private + variable + ℓs ℓp : Level + +module _ (C : SetCon {ℓs} {ℓp}) (isMnd : IsMonad ⟦ C ⟧f) where + open MndContainer + open IsMndContainer + open IsMonad isMnd + + fromMonad : MndContainer {ℓs} {ℓp} C + ι fromMonad = {! !} + σ fromMonad = {! !} + pr₁ fromMonad = {! !} + pr₂ fromMonad = {! !} + unit-l (isMndContainer fromMonad) = {! !} + unit-r (isMndContainer fromMonad) = {! !} + assoc (isMndContainer fromMonad) = {! !} + pr-unit-r (isMndContainer fromMonad) = {! !} + pr-unit-l (isMndContainer fromMonad) = {! !} + pr-mul₁ (isMndContainer fromMonad) = {! !} + pr-mul₁₂ (isMndContainer fromMonad) = {! !} + pr-mul₂₂ (isMndContainer fromMonad) = {! !} + +module _ (C : SetCon {ℓs} {ℓp}) (mCont : MndContainer {ℓs} {ℓp} C) where + open MndContainer mCont + open IsMndContainer isMndContainer + open NatTrans + open IsMonad + + toMonad : IsMonad ⟦ C ⟧f + N-ob (η toMonad) X x = (ι , const x) + N-hom (η toMonad) f = refl + N-ob (μ toMonad) X (s , f) = (σ s (fst ∘ f) , λ p → snd (f (pr₁ _ _ p)) (pr₂ _ _ p)) + N-hom (μ toMonad) f = refl + idl-μ toMonad = natEqSET {ℓ-max ℓs ℓp} F-rUnit + (compTrans (μ toMonad) (η toMonad ∘ˡ ⟦ C ⟧f)) + (idTrans ⟦ C ⟧f) + (λ X i x → (unit-l (fst x) i , λ p → snd x (pr-unit-l i p))) + idr-μ toMonad = natEqSET {ℓ-max ℓs ℓp} F-lUnit + (compTrans (μ toMonad) (⟦ C ⟧f ∘ʳ η toMonad)) + (idTrans ⟦ C ⟧f) + (λ X i x → (unit-r (fst x) i , λ p → snd x (pr-unit-r i p))) + assoc-μ toMonad = natEqSET {ℓ-max ℓs ℓp} F-assoc + (compTrans (μ toMonad) (⟦ C ⟧f ∘ʳ μ toMonad)) + (compTrans (μ toMonad) (μ toMonad ∘ˡ ⟦ C ⟧f)) + (λ X i x → (assoc (fst x) (fst ∘ (snd x)) (λ p p' → fst (snd (snd x p) p')) i + , λ p → snd (snd (snd x (pr-mul₁ i p)) (pr-mul₁₂ i p)) (pr-mul₂₂ i p) + ) + ) diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index 2f97272096..f190b0096e 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -230,3 +230,20 @@ module _ {ℓ : Level} where cInv (snd (limSetIso J D)) cc = liftCone J D (cc .lower) sec (snd (limSetIso J D)) = funExt (λ _ → liftExt (cone≡ λ _ → refl)) ret (snd (limSetIso J D)) = funExt (λ _ → cone≡ λ _ → refl) + +-- Paths between the object maps of natural transformations between functors +-- into SET can be lifted to paths between the natural transformations. +module _ {ℓ} {F F' G : Functor (SET ℓ) (SET ℓ)} where + open NatTrans + + natEqSET : (F-eq : F ≡ F') (α : NatTrans F G) (β : NatTrans F' G) → + (∀ X → PathP (λ i → SET ℓ [ F-ob (F-eq i) X , F-ob G X ]) (N-ob α X) (N-ob β X)) → + PathP (λ i → NatTrans (F-eq i) G) α β + N-ob (natEqSET F-eq α β obP i) X = obP X i + N-hom (natEqSET F-eq α β obP i) {X} {Y} f j = + isSet→SquareP {ℓ} {A = λ i' _ → fst (F-ob (F-eq i') X) → fst (F-ob G Y)} + (λ _ _ → isSetΠ (λ _ → snd (G .F-ob Y))) + {N-hom α f i0} {N-hom α f i1} (N-hom α f) + {N-hom β f i0} {N-hom β f i1} (N-hom β f) + (λ k z → obP Y k (F-hom (F-eq k) f z)) + (λ k z → F-hom G f (obP X k z)) i j From 509679b0f8fda80e919263dedd6bde686b8325de Mon Sep 17 00:00:00 2001 From: chrisjpurdy <33040507+chrisjpurdy@users.noreply.github.com> Date: Thu, 5 Jun 2025 17:35:14 +0100 Subject: [PATCH 11/11] Minor: remove unneded implicit args in natEqSET --- Cubical/Categories/Instances/Sets.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index f190b0096e..417a5dfa30 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -243,7 +243,6 @@ module _ {ℓ} {F F' G : Functor (SET ℓ) (SET ℓ)} where N-hom (natEqSET F-eq α β obP i) {X} {Y} f j = isSet→SquareP {ℓ} {A = λ i' _ → fst (F-ob (F-eq i') X) → fst (F-ob G Y)} (λ _ _ → isSetΠ (λ _ → snd (G .F-ob Y))) - {N-hom α f i0} {N-hom α f i1} (N-hom α f) - {N-hom β f i0} {N-hom β f i1} (N-hom β f) + (N-hom α f) (N-hom β f) (λ k z → obP Y k (F-hom (F-eq k) f z)) (λ k z → F-hom G f (obP X k z)) i j