From cea834551edb2177b72d13329c3a8a8fd8e71251 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@stefbook.local>
Date: Tue, 28 May 2024 16:07:59 +0100
Subject: [PATCH 01/12] Added W and M

---
 Cubical/Codata/M/MRecord.agda | 50 +++++++++++++++++++++++++++++++++++
 Cubical/Data/W.agda           |  5 ++++
 Cubical/Data/W/W.agda         | 13 +++++++++
 3 files changed, 68 insertions(+)
 create mode 100644 Cubical/Codata/M/MRecord.agda
 create mode 100644 Cubical/Data/W.agda
 create mode 100644 Cubical/Data/W/W.agda

diff --git a/Cubical/Codata/M/MRecord.agda b/Cubical/Codata/M/MRecord.agda
new file mode 100644
index 000000000..7ec584a08
--- /dev/null
+++ b/Cubical/Codata/M/MRecord.agda
@@ -0,0 +1,50 @@
+{- Alternative definition of M as a record type, together with some of its properties
+
+-}
+
+{-# OPTIONS --cubical --guardedness --safe #-}
+
+open import Cubical.Foundations.Prelude
+
+module Cubical.Codata.M.MRecord where
+
+record M' (S : Type) (P : S → Type) : Type where
+  constructor sup-M
+  coinductive
+  field
+    shape : S
+    pos : P shape → M' S P
+open M'
+
+-- Lifting M' to relations
+record M'-R {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type) (m₀ m₁ : M' S Q) : Type where
+  field
+   s-eq : shape m₀ ≡ shape m₁        
+   p-eq : (q₀ : Q (shape m₀))(q₁ : Q (shape m₁))(q-eq : PathP (λ i → Q (s-eq i)) q₀ q₁)
+          → R (pos m₀ q₀) (pos m₁ q₁)
+open M'-R
+
+-- Coinduction principle for M
+CoInd-M' : {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type)
+          (is-bisim : {m₀ m₁ : M' S Q} → R m₀ m₁ → M'-R R m₀ m₁)
+          {m₀ m₁ : M' S Q} → R m₀ m₁ → m₀ ≡ m₁ 
+shape (CoInd-M' R is-bisim r i) = s-eq (is-bisim r) i
+pos (CoInd-M' {S} {Q} R is-bisim {m₀ = m₀}{m₁ = m₁} r i) q =
+  CoInd-M' R is-bisim {m₀ = pos m₀ q₀} {m₁ = pos m₁ q₁} (p-eq (is-bisim r) q₀ q₁ q₂) i
+    where QQ : I → Type
+          QQ i = Q (s-eq (is-bisim r) i)
+
+          q₀ : QQ i0
+          q₀ = transp (λ j → QQ (~ j ∧ i)) (~ i) q
+
+          q₁ : QQ i1
+          q₁ = transp (λ j → QQ (j ∨ i)) i q
+
+          q₂ : PathP (λ i → QQ i) q₀ q₁
+          q₂ k = transp (λ j → QQ ((~ k ∧ ~ j ∧ i) ∨ (k ∧ (j ∨ i)) ∨
+                 ((~ j ∧ i) ∧ (j ∨ i)))) ((~ k ∧ ~ i) ∨ (k ∧ i)) q
+                 
+-- (Propositional) η-equality for M'
+M'-eta-eq : {S' : Type} {Q' : S' → Type} (m : M' S' Q') → sup-M (shape m) (pos m) ≡ m
+shape (M'-eta-eq m i) = shape m
+pos (M'-eta-eq m i) = pos m
diff --git a/Cubical/Data/W.agda b/Cubical/Data/W.agda
new file mode 100644
index 000000000..fb0e0abbf
--- /dev/null
+++ b/Cubical/Data/W.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --without-K --guardedness --cubical --safe #-}
+
+module Cubical.Data.W where
+
+open import Cubical.Data.W.W public
diff --git a/Cubical/Data/W/W.agda b/Cubical/Data/W/W.agda
new file mode 100644
index 000000000..b40becf09
--- /dev/null
+++ b/Cubical/Data/W/W.agda
@@ -0,0 +1,13 @@
+{-# OPTIONS --cubical --safe #-}
+
+open import Cubical.Foundations.Prelude
+
+module Cubical.Data.W.W where
+
+data W (S : Type) (P : S → Type) : Type where
+  sup-W : (s : S) → (P s → W S P) → W S P
+
+W-ind : (S : Type) (P : S → Type) (M : W S P → Type) →
+        (e : {s : S} {f : P s → W S P} → ((p : P s) → M (f p)) → M (sup-W s f)) →
+        (w : W S P) → M w
+W-ind S P M e (sup-W s f) = e {s} {f} (λ p → W-ind S P M e (f p))

From d590f940aead97daab189960e97d2ee4409647c0 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@stefbook.local>
Date: Tue, 28 May 2024 16:13:14 +0100
Subject: [PATCH 02/12] Fixed flags

---
 Cubical/Data/W.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Data/W.agda b/Cubical/Data/W.agda
index fb0e0abbf..2e56d002a 100644
--- a/Cubical/Data/W.agda
+++ b/Cubical/Data/W.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K --guardedness --cubical --safe #-}
+{-# OPTIONS --cubical --safe #-}
 
 module Cubical.Data.W where
 

From 85e84c1eca3da1d3b1c0380aeeff8566b1ca2bb6 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@stefbook.local>
Date: Tue, 28 May 2024 17:08:16 +0100
Subject: [PATCH 03/12] Added containers proofs

---
 Cubical/Data/Containers/Algebras.agda         |  65 +++++++
 Cubical/Data/Containers/Base.agda             | 168 +++++++++++++++++
 .../Containers/CoinductiveContainers.agda     | 173 ++++++++++++++++++
 .../Containers/ContainerExtensionProofs.agda  | 149 +++++++++++++++
 .../Data/Containers/InductiveContainers.agda  |  72 ++++++++
 5 files changed, 627 insertions(+)
 create mode 100644 Cubical/Data/Containers/Algebras.agda
 create mode 100644 Cubical/Data/Containers/Base.agda
 create mode 100644 Cubical/Data/Containers/CoinductiveContainers.agda
 create mode 100644 Cubical/Data/Containers/ContainerExtensionProofs.agda
 create mode 100644 Cubical/Data/Containers/InductiveContainers.agda

diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda
new file mode 100644
index 000000000..a091a8a57
--- /dev/null
+++ b/Cubical/Data/Containers/Algebras.agda
@@ -0,0 +1,65 @@
+{- Basic definitions required for co/inductive container proofs
+
+- Proposition elimination
+
+- Definition of Pos
+
+-}
+
+{-# OPTIONS --cubical --guardedness --safe #-}
+
+open import Cubical.Data.W
+open import Cubical.Codata.M.MRecord renaming (M' to M)
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+
+module Cubical.Data.Containers.Algebras where
+
+-- Proposition elimination
+prop-elim : ∀ {ℓ} {A : Type ℓ} (t : isProp A) → (D : A → Type ℓ) →
+            (x : A) → D x → (a : A) → D a
+prop-elim t D x pr a = subst D (t x a) pr
+
+module Algs (Ind : Type)
+         (S : Type)
+         (P : Ind → S → Type)
+         (Q : S → Type)
+         (X : Ind → Type)
+         (Y : Type) where
+
+  open M
+  open Iso
+
+  -- Fixed point algebras
+  record ContFuncIso (S : Type) (P : S → Type) : Type₁ where
+    constructor iso
+    field
+      carrier : Type
+      χ : Iso (Σ[ s ∈ S ] (P s → carrier)) carrier
+
+  open ContFuncIso
+
+  WAlg : ContFuncIso S Q
+  WAlg = iso (W S Q) isom
+    where
+      isom : Iso (Σ[ s ∈ S ] (Q s → W S Q)) (W S Q)
+      fun isom = uncurry sup-W
+      inv isom (sup-W s f) = s , f
+      rightInv isom (sup-W s f) = refl
+      leftInv isom (s , f) = refl
+
+  MAlg : ContFuncIso S Q
+  MAlg = iso (M S Q) isom
+    where
+      isom : Iso (Σ[ s ∈ S ] (Q s → M S Q)) (M S Q)
+      fun isom = uncurry sup-M
+      inv isom m = shape m , pos m
+      rightInv isom m = M'-eta-eq m
+      leftInv isom (s , f) = refl
+
+  data Pos (FP : ContFuncIso S Q) (i : Ind) : carrier FP → Type where
+    here : {wm : carrier FP} → P i (fst (FP .χ .inv wm)) → Pos FP i wm
+    below : {wm : carrier FP} → (q : Q (fst (FP .χ .inv wm))) →
+            Pos FP i (snd (FP .χ .inv wm) q) → Pos FP i wm
+
diff --git a/Cubical/Data/Containers/Base.agda b/Cubical/Data/Containers/Base.agda
new file mode 100644
index 000000000..e2ee0e363
--- /dev/null
+++ b/Cubical/Data/Containers/Base.agda
@@ -0,0 +1,168 @@
+{- Basic container definitions:
+
+- Definition of generalised container parameterised by category C
+
+- Category Cont whose objects are generalised containers
+
+- Functor ⟦_⟧ : Cont → Functor C Set
+
+- Example of List as a generalised container
+
+-}
+
+
+{-# OPTIONS --cubical --safe #-}
+
+open import Cubical.Categories.Category.Base 
+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 (_◁_)
+
+module Cubical.Data.Containers.Base where
+
+private
+  variable
+    ℓ ℓ' : Level
+
+open Category
+open Functor
+open NatTrans
+
+-- Definition of generalised container
+record GenContainer (C : Category ℓ ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+  constructor _◁_&_ 
+  field
+    S : Type ℓ' 
+    P : S → ob C
+    isSetS : isSet S
+
+open GenContainer
+
+module Conts {C : Category ℓ ℓ'} where
+
+  -- Category Cont with objects of type GenContainer C
+  record _⇒c_ (C₁ C₂ : GenContainer C) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+    constructor _◁_
+    field
+      u : S C₁ → S C₂
+      f : (s : S C₁) → C [ P C₂ (u s) , P C₁ s ]
+
+  open _⇒c_
+
+  id-c : {Con : GenContainer C} → Con ⇒c Con
+  id-c = (λ s → s) ◁ λ _ → C .id
+
+  _⋆c_ : {C₁ C₂ C₃ : GenContainer C} → C₁ ⇒c C₂ → C₂ ⇒c C₃ → C₁ ⇒c C₃
+  _⋆c_ (u ◁ f) (v ◁ g) = (λ a → v (u a)) ◁ λ a → (g (u a)) ⋆⟨ C ⟩ (f a)
+
+  assoc-c : {C₁ C₂ C₃ C₄ : GenContainer C} (f : C₁ ⇒c C₂) (g : C₂ ⇒c C₃) (h : C₃ ⇒c C₄) →
+            (f ⋆c g) ⋆c h ≡ f ⋆c (g ⋆c h)
+  assoc-c (u ◁ f) (v ◁ g) (w ◁ h) i = (λ a → w (v (u a))) ◁ λ a → C .⋆Assoc (h (v (u a))) (g (u a)) (f a) (~ i)
+
+  isSet⇒c : {C₁ C₂ : GenContainer C} → isSet (C₁ ⇒c C₂)
+  u (isSet⇒c {A ◁ B & set-A} {E ◁ F & set-C} m n p q i j) a =
+    set-C (u m a) (u n a) (λ k → u (p k) a) (λ k → u (q k) a) i j
+  f (isSet⇒c {A ◁ B & set-A} {E ◁ F & set-C} m n p q i j) a =
+    isSet→SquareP
+      {A = λ i j → C [ (F (set-C (u m a) (u n a) (λ k → u (p k) a) (λ k → u (q k) a) i j)) ,  B a ]} 
+      (λ i j → C .isSetHom {F (set-C (u m a) (u n a) (λ k → u (p k) a) (λ k → u (q k) a) i j)} {B a})
+      (λ k → f (p k) a)
+      (λ k → f (q k) a)
+      (λ _ → f m a)
+      (λ _ → f n a)
+      i j
+
+  Cont : Category (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-suc (ℓ-max ℓ ℓ'))
+  Cont = record
+           { ob = GenContainer C
+           ; Hom[_,_] = _⇒c_
+           ; id = id-c
+           ; _⋆_ = _⋆c_
+           ; ⋆IdL = λ m i → (u m) ◁ (λ a → C .⋆IdR (f m a) i)
+           ; ⋆IdR = λ m i → (u m) ◁ (λ a → C .⋆IdL (f m a) i)
+           ; ⋆Assoc = assoc-c
+           ; isSetHom = isSet⇒c
+           }
+
+  -- Definition of functor ⟦_⟧ : Cont → Functor C Set
+
+  -- Type alias for (S : Type) (P : S → C .ob) (X : C .ob) ↦ Σ S (λ s → C [ P s , X ]) 
+  cont-func : (S : Type ℓ') (P : S → C .ob) (X : C .ob) → Type ℓ'
+  cont-func S P X = Σ S (λ s → C [ P s , X ])
+
+  isSetContFunc : (A : Type ℓ') (B : A → ob C) (X : ob C) (isSetA : isSet A) → isSet (cont-func A B X)
+  fst (isSetContFunc A B X setA s₁ s₂ p q i j) =
+    setA (fst s₁) (fst s₂) (λ k → fst (p k)) (λ k → fst (q k)) i j
+  snd (isSetContFunc A B X setA s₁ s₂ p q i j) = 
+      isSet→SquareP
+      {A = λ i j → C [ (B (setA (fst s₁) (fst s₂) (λ k → fst (p k)) (λ k → fst (q k)) i j)) , X ]}
+      (λ i j → C .isSetHom {B (setA (fst s₁) (fst s₂) (λ k → fst (p k)) (λ k → fst (q k)) i j)} {X})
+      (λ k → snd (p k))
+      (λ k → snd (q k))
+      (λ _ → snd s₁)
+      (λ _ → snd s₂)
+      i j
+
+  cont-mor : {A : Type ℓ'} {B : A → ob C} {X Y : ob C} (f : C [ X , Y ]) →
+             cont-func A B X → cont-func A B Y
+  cont-mor f (s , g) = s , (g ⋆⟨ C ⟩ f)
+
+  ⟦_⟧-obj : GenContainer C → Functor C (SET ℓ')
+  ⟦ (A ◁ B & set-A) ⟧-obj = record {
+                                    F-ob = λ X → cont-func A B X , isSetContFunc A B X set-A ;
+                                    F-hom = cont-mor ;
+                                    F-id = funExt λ {(a , b) i → a , C .⋆IdR b i} ;
+                                    F-seq = λ f g i (a , b) → a , C .⋆Assoc b f g (~ i) 
+                                   }
+
+  ⟦_⟧-mor : {C₁ C₂ : GenContainer C} → C₁ ⇒c C₂ → NatTrans ⟦ C₁ ⟧-obj ⟦ C₂ ⟧-obj
+  N-ob (⟦_⟧-mor (u ◁ f)) X (s , p) = u s , ((f s) ⋆⟨ C ⟩ p)
+  N-hom (⟦_⟧-mor (u ◁ f)) xy i (a , b) = u a , C .⋆Assoc (f a) b xy (~ i)
+
+  ⟦_⟧-id : {C₁ : GenContainer C} → ⟦_⟧-mor {C₁} {C₁} (id-c {C₁}) ≡ idTrans ⟦ C₁ ⟧-obj
+  N-ob (⟦_⟧-id {S ◁ P & set-S} i) X (s , p) = s , C .⋆IdL p i
+  N-hom (⟦_⟧-id {S ◁ P & set-S} i) {X} {Y} xy j (s , p) = square i j
+    where
+      square : Square
+                 (λ j → N-hom (⟦_⟧-mor {S ◁ P & set-S} {S ◁ P & set-S} id-c) xy j (s , p))
+                 (λ j → N-hom (idTrans ⟦ S ◁ P & set-S ⟧-obj) xy j (s , p))
+                 (λ i → s , C .⋆IdL ((C ⋆ p) xy) i)
+                 (λ i → s , (C ⋆ C .⋆IdL p i) xy)
+      square = isSet→SquareP (λ i j → isSetContFunc S P Y set-S) _ _ _ _
+
+  ⟦_⟧-comp : {U V W : GenContainer C} (g : U ⇒c V) (h : V ⇒c W) →
+             ⟦ g ⋆c h ⟧-mor ≡ ⟦ g ⟧-mor ⋆⟨ FUNCTOR C (SET ℓ') ⟩ ⟦ h ⟧-mor
+  N-ob (⟦_⟧-comp {U} {V} {W} (ug ◁ fg) (uh ◁ fh) i) A (s , p) = uh (ug s) , C .⋆Assoc (fh (ug s)) (fg s) p i
+  N-hom (⟦_⟧-comp {U} {V} {W} (ug ◁ fg) (uh ◁ fh) i) {X} {Y} xy j (s , p) = square i j 
+    where
+      square : Square
+                (λ j → N-hom (⟦_⟧-mor {U} {W} (_⋆c_ {U} {V} {W} (ug ◁ fg) (uh ◁ fh))) {X} {Y} xy j (s , p))
+                (λ j → N-hom (seq' (FUNCTOR C (SET ℓ')) {⟦ U ⟧-obj} {⟦ V ⟧-obj} {⟦ W ⟧-obj}
+                       (⟦_⟧-mor {U} {V} (ug ◁ fg)) (⟦_⟧-mor {V} {W} (uh ◁ fh))) xy j (s , p)) 
+                (λ i → uh (ug s) , C .⋆Assoc (fh (ug s)) (fg s) ((C ⋆ p) xy) i)
+                (λ i → uh (ug s) , (C ⋆ C .⋆Assoc (fh (ug s)) (fg s) p i) xy)
+      square = isSet→SquareP (λ i j → isSetContFunc (S W) (P W) Y (isSetS W)) _ _ _ _
+
+  ⟦_⟧ : Functor Cont (FUNCTOR C (SET ℓ'))
+  ⟦_⟧ = record {
+                F-ob = ⟦_⟧-obj ;
+                F-hom = ⟦_⟧-mor ;
+                F-id = λ {A} → ⟦_⟧-id {A} ;
+                F-seq = ⟦_⟧-comp
+               }
+              
+-- Example
+
+open Conts {C = SET (ℓ-zero)}
+
+open import Cubical.Data.Fin
+open import Cubical.Data.Nat
+
+ListC : GenContainer (SET (ℓ-zero))
+ListC = ℕ ◁ (λ n → Fin n , isSetFin) & isSetℕ
+
+ListF : Functor (SET (ℓ-zero)) (SET (ℓ-zero))
+ListF = ⟦ ListC ⟧-obj
diff --git a/Cubical/Data/Containers/CoinductiveContainers.agda b/Cubical/Data/Containers/CoinductiveContainers.agda
new file mode 100644
index 000000000..e32b3e769
--- /dev/null
+++ b/Cubical/Data/Containers/CoinductiveContainers.agda
@@ -0,0 +1,173 @@
+{- Proof that containers are closed under greatest fixed points
+
+Adapted from 'Containers: Constructing strictly positive types'
+by Abbott, Altenkirch, Ghani
+
+-}
+
+{-# OPTIONS --without-K --guardedness --cubical #-}
+
+open import Cubical.Codata.M.MRecord
+open import Cubical.Data.Sigma
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+
+open import Cubical.Data.Containers.Algebras
+open M'
+open M'-R
+
+module Cubical.Data.Containers.CoinductiveContainers
+         (Ind : Type)
+         (S : Type)
+         (setS : isSet S)
+         (P : Ind → S → Type)
+         (Q : S → Type)
+         (setM : isSet S → isSet (M' S Q))
+         (X : Ind → Type)
+         (Y : Type)
+         (βs : Y → S)
+         (βg : (y : Y) → (i : Ind) → P i (βs y) → X i)
+         (βh : (y : Y) → Q (βs y) → Y) where
+         
+    open Algs Ind S P Q X Y
+
+    β̅₁ : Y → M' S Q
+    shape (β̅₁ y) = βs y
+    pos (β̅₁ y) = β̅₁ ∘ βh y
+
+    β̅₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̅₁ y) → X ind
+    β̅₂ y ind (here p) = βg y ind p
+    β̅₂ y ind (below q p) = β̅₂ (βh y q) ind p
+
+    β̅ : Y → Σ[ m ∈ M' S Q ] ((i : Ind) → Pos MAlg i m → X i)
+    β̅ y = β̅₁ y , β̅₂ y
+    
+    out : Σ[ m ∈ M' S Q ] ((i : Ind) → Pos MAlg i m → X i) →
+          Σ[ (s , f) ∈ Σ[ s ∈ S ] (Q s → M' S Q) ]
+            (((i : Ind) → P i s → X i) ×
+            ((i : Ind) (q : Q s) → Pos MAlg i (f q) → X i))
+    out (m , k) = (shape m , pos m) , ((λ i p → k i (here p)) , (λ i q p → k i (below q p)))
+
+    module _ (β̃₁ : Y → M' S Q)
+             (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)
+             (comm : (y : Y) →
+                     out (β̃₁ y , β̃₂ y) ≡
+                     ((βs y , λ q → (β̃₁ (βh y q))) , (βg y , λ i q → (β̃₂ (βh y q)) i))) where
+
+      -- Diagram commutes
+      β̅-comm : (y : Y) → out (β̅ y) ≡ ((βs y , β̅₁ ∘ (βh y)) , (βg y , λ i q → β̅₂ (βh y q) i))
+      β̅-comm y = refl
+
+      β̃ : Y → Σ (M' S Q) (λ m → (i : Ind) → Pos MAlg i m → X i)
+      β̃ y = β̃₁ y , β̃₂ y
+
+      ----------
+
+      comm1 : (y : Y) → shape (β̃₁ y) ≡ shape (β̅₁ y)
+      comm1 y i = fst (fst (comm y i))
+
+      comm2 : (y : Y) →
+                   PathP (λ i → Q (comm1 y i) → M' S Q)
+                         (pos (β̃₁ y)) (λ q → β̃₁ (βh y q))
+      comm2 y i = snd (fst (comm y i))
+
+      comm3 : (y : Y) → PathP (λ i → (ind : Ind) → P ind (comm1 y i) → X ind)
+                              (λ ind p → β̃₂ y ind (here p))
+                              (βg y)
+      comm3 y i = fst (snd (comm y i))
+
+      comm4 : (y : Y) → PathP (λ i → (ind : Ind) → (q : Q (comm1 y i)) →
+                              Pos MAlg ind (comm2 y i q) → X ind)
+                              (λ ind q b → β̃₂ y ind (below q b))
+                              (λ ind q b → β̃₂ (βh y q) ind b)
+      comm4 y i = snd (snd (comm y i))
+
+      data R : M' S Q → M' S Q → Type where
+        R-intro : (y : Y) → R (β̃₁ y) (β̅₁ y)
+
+      is-bisim-R : {m₀ : M' S Q} {m₁ : M' S Q} → R m₀ m₁ → M'-R R m₀ m₁
+      s-eq (is-bisim-R (R-intro y)) = comm1 y
+      p-eq (is-bisim-R (R-intro y)) q₀ q₁ q-eq = 
+        transport (λ i → R (comm2 y (~ i) (q-eq (~ i))) (β̅₁ (βh y q₁))) (R-intro (βh y q₁))
+
+      fst-eq : (y : Y) → β̃₁ y ≡ β̅₁ y
+      fst-eq y = CoInd-M' {S} {Q} R is-bisim-R (R-intro y)
+
+      snd-eq-gen : (y : Y) (β̃₁ : Y → M' S Q) (p : β̅₁ ≡ β̃₁)
+                   (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)
+                   (comm1 : shape ∘ β̃₁ ≡ βs)
+                   (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M' S Q)
+                                            (pos (β̃₁ y)) (β̃₁ ∘ βh y))
+                   (comm3 : (y : Y) → PathP (λ i  → (ind : Ind) → P ind (comm1 i y) → X ind)
+                                            (λ ind p → β̃₂ y ind (here p))
+                                            (βg y))
+                   (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (comm1 i y)) →
+                                            Pos MAlg ind (comm2 y i q) → X ind)
+                                            (λ ind q b → β̃₂ y ind (below q b))
+                                            λ ind q b → β̃₂ (βh y q) ind b) →
+                   PathP (λ i → (ind : Ind) → Pos MAlg ind (p i y) → X ind)
+                         (β̅₂ y) (β̃₂ y)
+      snd-eq-gen y =
+        J>_ -- we're applying J to p : makeβ̅₁ βs βg βh ≡ β̅₁
+          {P = λ β̃₁ p →
+            (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)
+            (comm1 : shape ∘ β̃₁ ≡ βs)
+            (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M' S Q) (pos (β̃₁ y)) (β̃₁ ∘ βh y))
+            (comm3 : (y : Y) → PathP (λ i  → (ind : Ind) → P ind (comm1 i y) → X ind)
+                     (λ ind p → β̃₂ y ind (here p))
+                     (βg y))
+            (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (comm1 i y)) → Pos MAlg ind
+                               (comm2 y i q) → X ind)
+                     (λ ind q b → β̃₂ y ind (below q b))
+                     λ ind q b → β̃₂ (βh y q) ind b) →
+            PathP (λ i → (ind : Ind) → Pos MAlg ind (p i y) → X ind)
+            (β̅₂ y) 
+            (β̃₂ y)}
+          λ β̃₂ comm1 →
+            prop-elim -- S is a set so equality on S is a prop
+              {A = (λ y → βs y) ≡ βs}
+              (isSetΠ (λ _ → setS) (λ y → βs y) βs)
+              (λ s-eq →
+                (comm2 : (y : Y) → PathP (λ i → Q (s-eq i y) → M' S Q)
+                                   (β̅₁ ∘ βh y) (β̅₁ ∘ βh y))
+                (comm3 : (y : Y) → PathP (λ i  → (ind : Ind) → P ind (s-eq i y) → X ind)
+                                   (λ ind p → β̃₂ y ind (here p)) (βg y))
+                (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (s-eq i y)) → Pos MAlg ind
+                                   (comm2 y i q) → X ind)
+                                   (λ ind q b → β̃₂ y ind (below q b))
+                                   (λ ind q b → β̃₂ (βh y q) ind b)) →
+                         (β̅₂ y) ≡ (β̃₂ y))
+              refl
+              (prop-elim -- M' is a set so equality on M' is a prop
+                {A = (y : Y) →
+                     (λ x → β̅₁ (βh y x)) ≡ (λ x → β̅₁ (βh y x))}
+                (isPropΠ λ y' → isSetΠ (λ _ → setM setS) (β̅₁ ∘ βh y') (β̅₁ ∘ βh y'))
+                (λ m-eq → 
+                  (comm3 : (y : Y) → (λ ind p → β̃₂ y ind (here p)) ≡ (βg y))
+                  (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (βs y)) → Pos MAlg ind
+                                     (m-eq y i q) → X ind)
+                                     (λ ind q b → β̃₂ y ind (below q b))
+                                     (λ ind q b → β̃₂ (βh y q) ind b)) →
+                         (β̅₂ y) ≡ (β̃₂ y))
+                (λ _ → refl)
+                λ comm3 comm4 → funExt (λ ind → funExt (snd-eq-aux β̃₂ comm3 comm4 y ind)))
+              comm1
+        where
+          snd-eq-aux : (β̃₂ : (s : Y) (i : Ind) → Pos MAlg i (β̅₁ s) → X i)
+                       (c3 : (s : Y) → (λ ind p → β̃₂ s ind (here p)) ≡ βg s)
+                       (c4 : (s : Y) → (λ ind q b → β̃₂ s ind (below q b)) ≡
+                                       (λ ind q → β̃₂ (βh s q) ind))
+                       (y : Y) (ind : Ind) (pos : Pos MAlg ind (β̅₁ y)) → β̅₂ y ind pos ≡ β̃₂ y ind pos
+          snd-eq-aux β̃₂ c3 c4 y ind (here x) = sym (funExt⁻ (funExt⁻ (c3 y) ind) x)
+          snd-eq-aux β̃₂ c3 c4 y ind (below q x) =
+            snd-eq-aux β̃₂ c3 c4 (βh y q) ind x ∙ funExt⁻ (funExt⁻ (sym (funExt⁻ (c4 y) ind)) q) x
+
+      snd-eq : (y : Y) → PathP (λ i → (ind : Ind) → Pos MAlg ind (fst-eq y i) → X ind) (β̃₂ y) (β̅₂ y)
+      snd-eq y i = snd-eq-gen y β̃₁ (sym (funExt fst-eq)) β̃₂ (funExt comm1) comm2 comm3 comm4 (~ i)
+
+      -- β̅ is unique
+      β̅-unique : β̃ ≡ β̅
+      fst (β̅-unique i y) = fst-eq y i
+      snd (β̅-unique i y) = snd-eq y i
+
diff --git a/Cubical/Data/Containers/ContainerExtensionProofs.agda b/Cubical/Data/Containers/ContainerExtensionProofs.agda
new file mode 100644
index 000000000..eed15a8d9
--- /dev/null
+++ b/Cubical/Data/Containers/ContainerExtensionProofs.agda
@@ -0,0 +1,149 @@
+{- 2 presentations of the proof that the functor ⟦_⟧ : Cont → Func
+   is full and faithful
+
+- First one is adapted from 'Containers: Constructing strictly positive types'
+  by Abbott, Altenkirch, Ghani
+
+- Second one uses the Yoneda lemma
+
+-}
+
+{-# OPTIONS --cubical --safe #-}
+
+open import Agda.Builtin.Cubical.HCompU
+
+open import Cubical.Categories.Category.Base 
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧)
+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.Sigma
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude hiding (_◁_)
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism 
+open import Cubical.Foundations.Function
+
+module Cubical.Data.Containers.ContainerExtensionProofs where
+
+private
+  variable
+    ℓ ℓ' ℓ'' ℓ''' ℓ'''' : Level
+
+open Category hiding (_∘_)
+open Functor
+open NatTrans
+open Iso
+
+module _ {C : Category ℓ ℓ'} where
+
+    open Conts {ℓ} {ℓ'} {C}   
+
+    -- Proof 1 that the functor ⟦_⟧ is full and faithful
+    -- Adapted from 'Containers: Constructing strictly positive types'
+
+    ⟦_⟧-fully-faithful : isFullyFaithful ⟦_⟧
+    equiv-proof (⟦_⟧-fully-faithful (S ◁ P & set-S) (T ◁ Q & set-T)) (natTrans mors nat) =
+      (fib (natTrans mors nat) , fib-pf) , unique
+      where
+        fib : NatTrans ⟦ (S ◁ P & set-S) ⟧-obj ⟦ (T ◁ Q & set-T) ⟧-obj →
+              (S ◁ P & set-S) ⇒c (T ◁ Q & set-T)
+        fib (natTrans mors _) = (fst ∘ tq) ◁ (snd ∘ tq)
+          where
+            tq : (s : S) → cont-func T Q (P s)
+            tq s = mors (P s) (s , C .id {P s}) 
+
+        fib-pf : ⟦ fib (natTrans mors nat) ⟧-mor ≡ (natTrans mors nat)
+        fib-pf = cong₂
+                   natTrans
+                   ((funExt λ X → funExt λ {(s , h) →
+                     sym (funExt⁻ (nat h) (s , C .id)) ∙ cong (λ Z → mors X (s , Z)) (C .⋆IdL h)})) 
+                   (isProp→PathP (λ i → isPropImplicitΠ2 (λ X Y → isPropΠ (λ f →
+                     isSetΠ (λ _ → isSetContFunc T Q Y set-T) _ _))) _ _) 
+
+        ret : ∀ X→Y → fib (⟦ X→Y ⟧-mor) ≡ X→Y
+        ret (u ◁ f) i = u ◁ λ s → C .⋆IdR (f s) i
+        
+        unique : (y : Helpers.fiber (⟦_⟧-mor) (natTrans mors nat)) → (fib (natTrans mors nat) , fib-pf) ≡ y
+        unique (m , m-eq) = ΣPathP (cong (fib) (sym m-eq) ∙ ret m , square)
+          where
+            square : Square (λ i → fib-pf i)
+                            (λ i → m-eq i)
+                            (λ i → F-hom ⟦_⟧ (((λ j → fib (m-eq (~ j))) ∙ ret m) i))
+                            refl
+            square = isSet→SquareP (λ _ _ → isSetNatTrans) _ _ _ _
+
+    -- Proof 2 that the functor ⟦_⟧ is full and faithful
+    -- Uses the Yoneda lemma
+
+    -- Distributivity of Π over Σ
+    distrΠΣ : {A : Type ℓ''}{B : A → Type ℓ'''}{C : (a : A) → B a → Type ℓ''''} →
+              Iso ((a : A) → Σ (B a) (λ b → C a b))
+                  (Σ ((a : A) → B a) (λ f → (a : A) → C a (f a)))
+    distrΠΣ = iso
+               (λ f → (λ a → fst (f a)) , λ a → snd (f a))
+               (λ {(f , g) → λ a → f a , g a})
+               (λ _ → refl)
+               (λ _ → refl)
+
+    -- Compose heterogenous with homogenous equality
+    comp-het-hom : {A : I → Type ℓ'} (x : A i0) (y : A i1) (z : A i1) →
+                   PathP (λ i → A i) x y → y ≡ z → PathP (λ i → A i) x z
+    comp-het-hom {A} x y z p eq i = subst (λ c → PathP A x c) eq p i 
+
+    ⟦_⟧-fully-faithful' : isFullyFaithful ⟦_⟧
+    equiv-proof (⟦_⟧-fully-faithful' (S ◁ P & set-S) (T ◁ Q & set-T)) (natTrans mors nat) =
+      (mor , mor-eq) , unique
+      where
+        nat-trans : (s : S) → FUNCTOR C (SET ℓ') [ C [ P s ,-] , ⟦ T ◁ Q & set-T ⟧-obj ]
+        nat-trans s = natTrans (λ X → curry (mors X) s) nat'
+          where
+            nat' : N-hom-Type (C [ P s ,-]) ⟦ T ◁ Q & set-T ⟧-obj (λ X → curry (mors X) s)
+            nat' {X} {Y} X→Y = funExt (λ Ps→X → funExt⁻ (nat {X} {Y} X→Y) (s , Ps→X))
+
+        apply-yo : (s : S) → cont-func T Q (P s)
+        apply-yo s = (fun (yoneda ⟦ T ◁ Q & set-T ⟧-obj (P s))) (nat-trans s)
+
+        apply-distrΠΣ : Σ (S → T) (λ f → (s : S) → C [ Q (f s) , P s ])
+        apply-distrΠΣ = (fun distrΠΣ) (apply-yo)
+
+        mor : (S ◁ P & set-S) ⇒c (T ◁ Q & set-T)
+        mor = fst apply-distrΠΣ ◁ snd apply-distrΠΣ
+        
+        mor-eq : ⟦ mor ⟧-mor ≡ natTrans mors nat
+        mor-eq = cong₂
+                   natTrans
+                   (funExt (λ X → funExt (λ {(s , f) →
+                     sym (funExt⁻ (nat {P s} {X} f) (s , C .id)) ∙
+                     cong (λ Z → mors X (s , Z)) (C .⋆IdL f)})))
+                   ((isProp→PathP (λ i → isPropImplicitΠ2 (λ X Y → isPropΠ (λ f →
+                     isSetΠ (λ _ → isSetContFunc T Q Y set-T) _ _))) _ _))
+
+        
+        
+        unique : (y : Helpers.fiber (⟦_⟧-mor) (natTrans mors nat)) → (mor , mor-eq) ≡ y
+        unique ((u ◁ f) , m-eq) =
+          ΣPathP
+            (cong₂ _◁_ (funExt (λ s i → fst (N-ob (m-eq (~ i)) (P s) (s , C .id))))
+                       (funExt (λ s i → comp-het-hom
+                                         (snd (mors (P s) (s , C .id)))
+                                         (f s ⋆⟨ C ⟩ (C .id))
+                                         (f s)
+                                         (λ j → snd (N-ob (m-eq (~ j)) (P s) (s , C .id)))
+                                         (C .⋆IdR (f s)) i))
+            ,
+            square)
+             where
+               square : Square (λ i → mor-eq i)
+                               (λ i → m-eq i)
+                               (λ i → ⟦_⟧-mor {S ◁ P & set-S} {T ◁ Q & set-T}
+                                              (funExt (λ s j → fst (N-ob (m-eq (~ j)) (P s) (s , C .id))) i ◁
+                                              funExt (λ s j → comp-het-hom
+                                                                 (snd (mors (P s) (s , C .id)))
+                                                                 (seq' C (f s) (C .id)) (f s)
+                                                                 (λ k → snd (N-ob (m-eq (~ k)) (P s) (s , C .id)))
+                                                                 (C .⋆IdR (f s)) j) i))
+                               (λ j → natTrans mors nat)
+               square = isSet→SquareP (λ _ _ → isSetNatTrans) _ _ _ _
diff --git a/Cubical/Data/Containers/InductiveContainers.agda b/Cubical/Data/Containers/InductiveContainers.agda
new file mode 100644
index 000000000..27d4ea71c
--- /dev/null
+++ b/Cubical/Data/Containers/InductiveContainers.agda
@@ -0,0 +1,72 @@
+{- Proof that containers are closed over least fixed points
+
+Adapted from 'Containers: Constructing strictly positive types'
+by Abbott, Altenkirch, Ghani
+
+-}
+
+{-# OPTIONS --cubical --guardedness --safe #-}
+
+open import Cubical.Data.W
+open import Cubical.Data.Containers.Algebras
+open import Cubical.Data.Sigma
+open import Cubical.Foundations.Prelude
+
+module Cubical.Data.Containers.InductiveContainers
+                           (Ind : Type)
+                           (S : Type)
+                           (P : Ind → S → Type)
+                           (Q : S → Type)
+                           (X : Ind → Type)
+                           (Y : Type)
+                           (α : Σ S (λ s → Σ ((i : Ind) → P i s → X i) (λ _ → Q s → Y)) → Y) where
+
+  open Algs Ind S P Q X Y
+         
+  into : Σ[ (s , f) ∈ Σ[ s ∈ S ] (Q s → W S Q) ]
+           (((i : Ind) → P i s → X i) ×
+           ((i : Ind) (q : Q s) → Pos WAlg i (f q) → X i)) →
+         Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i)  
+  into ((s , f) , (g , h)) = sup-W s f , λ i → λ {(here p) → g i p ; (below q b) → h i q b}
+
+  α̅' : (w : W S Q) → ((i : Ind) → Pos WAlg i w → X i) → Y
+  α̅' (sup-W s f) k = α (s , g , λ q → α̅' (f q)  (λ i → h i q))
+    where
+      g : (i : Ind) → P i s → X i
+      g i p = k i (here p)
+      
+      h : (i : Ind) → (q : Q s) → Pos WAlg i (f q) → X i
+      h i q b = k i (below q b)
+
+  α̅ : Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i) → Y
+  α̅ (w , k) = α̅' w k
+
+  -- Diagram commutes 
+  α̅-comm : (s : S) (f : Q s → W S Q) (g : (i : Ind) → P i s → X i)
+           (h : (i : Ind) (q : Q s) → Pos WAlg i (f q) → X i) →
+           α̅ (into ((s , f) , (g , h))) ≡ α (s , g , λ q → α̅ (f q , λ i → h i q))
+  α̅-comm s f g h = refl
+
+  -- α̅ is unique
+  α̅-unique : (α̃ : Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i) → Y) →
+             ((s : S) (f : Q s → W S Q) (g : (i : Ind) → P i s → X i)
+             (h : (i : Ind) (q : Q s) → Pos WAlg i (f q) → X i) →
+             α̃ (into ((s , f) , (g , h))) ≡ α (s , g , λ q → α̃ (f q , λ i → h i q))) →
+             α̅ ≡ α̃
+  α̅-unique α̃ α̃-comm = funExt w-rec
+    where
+      lemma : (s : S) (f : Q s → W S Q) (g : (i : Ind) → Pos WAlg i (sup-W s f) → X i) →
+              α̃ (into ((s , f) , (λ i p → g i (here p)) , (λ i q b → g i (below q b)))) ≡
+              α̃ (sup-W s f , g)
+      lemma s f g = cong₂ (λ w fun → α̃ (w , fun)) refl (funExt λ i → funExt (λ {(here p) → refl ; (below q b) → refl})) 
+
+      w-rec : (x : Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i)) → α̅ x ≡ α̃ x
+      w-rec (w , k) = W-ind S Q
+                               (λ w → (k : (i : Ind) → Pos WAlg i w → X i) → α̅ (w , k) ≡ α̃ (w , k))
+                               (λ {s'} {f'} ind k →
+                                 (λ i → α (s' , (λ i p → k i (here p)) ,
+                                        λ q → ind q (λ i pos → k i (below q pos)) i)) ∙
+                                 sym (α̃-comm s' f' (λ i p → k i (here p))
+                                   (λ i q b → k i (below q b))) ∙
+                                 lemma s' f' k)
+                               w k

From d2a15438f5cf0b38e88a48aab61e8c4bab77f207 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@stefbook.local>
Date: Tue, 28 May 2024 17:15:58 +0100
Subject: [PATCH 04/12] Fixed flags

---
 Cubical/Data/Containers/CoinductiveContainers.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Data/Containers/CoinductiveContainers.agda b/Cubical/Data/Containers/CoinductiveContainers.agda
index e32b3e769..6439cc578 100644
--- a/Cubical/Data/Containers/CoinductiveContainers.agda
+++ b/Cubical/Data/Containers/CoinductiveContainers.agda
@@ -5,7 +5,7 @@ by Abbott, Altenkirch, Ghani
 
 -}
 
-{-# OPTIONS --without-K --guardedness --cubical #-}
+{-# OPTIONS --guardedness --cubical --safe #-}
 
 open import Cubical.Codata.M.MRecord
 open import Cubical.Data.Sigma

From b07daa3f6452093b2a2f285ff4330689d4100105 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@stefbook.local>
Date: Tue, 28 May 2024 17:56:20 +0100
Subject: [PATCH 05/12] Refactors to follow conventions

---
 Cubical/Data/Containers/Algebras.agda         | 17 ++----
 Cubical/Data/Containers/Base.agda             |  2 +-
 .../Containers/CoinductiveContainers.agda     | 59 ++++++++++---------
 .../Containers/ContainerExtensionProofs.agda  | 44 +++++++-------
 .../Data/Containers/InductiveContainers.agda  | 10 ++--
 5 files changed, 66 insertions(+), 66 deletions(-)

diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda
index a091a8a57..aa115d4fc 100644
--- a/Cubical/Data/Containers/Algebras.agda
+++ b/Cubical/Data/Containers/Algebras.agda
@@ -6,7 +6,7 @@
 
 -}
 
-{-# OPTIONS --cubical --guardedness --safe #-}
+{-# OPTIONS --guardedness --safe #-}
 
 open import Cubical.Data.W
 open import Cubical.Codata.M.MRecord renaming (M' to M)
@@ -16,17 +16,12 @@ open import Cubical.Foundations.Prelude
 
 module Cubical.Data.Containers.Algebras where
 
--- Proposition elimination
-prop-elim : ∀ {ℓ} {A : Type ℓ} (t : isProp A) → (D : A → Type ℓ) →
-            (x : A) → D x → (a : A) → D a
-prop-elim t D x pr a = subst D (t x a) pr
-
 module Algs (Ind : Type)
-         (S : Type)
-         (P : Ind → S → Type)
-         (Q : S → Type)
-         (X : Ind → Type)
-         (Y : Type) where
+            (S : Type)
+            (P : Ind → S → Type)
+            (Q : S → Type)
+            (X : Ind → Type)
+            (Y : Type) where
 
   open M
   open Iso
diff --git a/Cubical/Data/Containers/Base.agda b/Cubical/Data/Containers/Base.agda
index e2ee0e363..01d18f741 100644
--- a/Cubical/Data/Containers/Base.agda
+++ b/Cubical/Data/Containers/Base.agda
@@ -11,7 +11,7 @@
 -}
 
 
-{-# OPTIONS --cubical --safe #-}
+{-# OPTIONS --safe #-}
 
 open import Cubical.Categories.Category.Base 
 open import Cubical.Categories.Functor
diff --git a/Cubical/Data/Containers/CoinductiveContainers.agda b/Cubical/Data/Containers/CoinductiveContainers.agda
index 6439cc578..71b1dba37 100644
--- a/Cubical/Data/Containers/CoinductiveContainers.agda
+++ b/Cubical/Data/Containers/CoinductiveContainers.agda
@@ -5,7 +5,7 @@ by Abbott, Altenkirch, Ghani
 
 -}
 
-{-# OPTIONS --guardedness --cubical --safe #-}
+{-# OPTIONS --guardedness --safe #-}
 
 open import Cubical.Codata.M.MRecord
 open import Cubical.Data.Sigma
@@ -56,8 +56,8 @@ module Cubical.Data.Containers.CoinductiveContainers
                      ((βs y , λ q → (β̃₁ (βh y q))) , (βg y , λ i q → (β̃₂ (βh y q)) i))) where
 
       -- Diagram commutes
-      β̅-comm : (y : Y) → out (β̅ y) ≡ ((βs y , β̅₁ ∘ (βh y)) , (βg y , λ i q → β̅₂ (βh y q) i))
-      β̅-comm y = refl
+      β̅Comm : (y : Y) → out (β̅ y) ≡ ((βs y , β̅₁ ∘ (βh y)) , (βg y , λ i q → β̅₂ (βh y q) i))
+      β̅Comm y = refl
 
       β̃ : Y → Σ (M' S Q) (λ m → (i : Ind) → Pos MAlg i m → X i)
       β̃ y = β̃₁ y , β̃₂ y
@@ -86,15 +86,15 @@ module Cubical.Data.Containers.CoinductiveContainers
       data R : M' S Q → M' S Q → Type where
         R-intro : (y : Y) → R (β̃₁ y) (β̅₁ y)
 
-      is-bisim-R : {m₀ : M' S Q} {m₁ : M' S Q} → R m₀ m₁ → M'-R R m₀ m₁
-      s-eq (is-bisim-R (R-intro y)) = comm1 y
-      p-eq (is-bisim-R (R-intro y)) q₀ q₁ q-eq = 
+      isBisimR : {m₀ : M' S Q} {m₁ : M' S Q} → R m₀ m₁ → M'-R R m₀ m₁
+      s-eq (isBisimR (R-intro y)) = comm1 y
+      p-eq (isBisimR (R-intro y)) q₀ q₁ q-eq = 
         transport (λ i → R (comm2 y (~ i) (q-eq (~ i))) (β̅₁ (βh y q₁))) (R-intro (βh y q₁))
 
-      fst-eq : (y : Y) → β̃₁ y ≡ β̅₁ y
-      fst-eq y = CoInd-M' {S} {Q} R is-bisim-R (R-intro y)
+      fstEq : (y : Y) → β̃₁ y ≡ β̅₁ y
+      fstEq y = CoInd-M' {S} {Q} R isBisimR (R-intro y)
 
-      snd-eq-gen : (y : Y) (β̃₁ : Y → M' S Q) (p : β̅₁ ≡ β̃₁)
+      sndEqGen : (y : Y) (β̃₁ : Y → M' S Q) (p : β̅₁ ≡ β̃₁)
                    (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)
                    (comm1 : shape ∘ β̃₁ ≡ βs)
                    (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M' S Q)
@@ -108,7 +108,7 @@ module Cubical.Data.Containers.CoinductiveContainers
                                             λ ind q b → β̃₂ (βh y q) ind b) →
                    PathP (λ i → (ind : Ind) → Pos MAlg ind (p i y) → X ind)
                          (β̅₂ y) (β̃₂ y)
-      snd-eq-gen y =
+      sndEqGen y =
         J>_ -- we're applying J to p : makeβ̅₁ βs βg βh ≡ β̅₁
           {P = λ β̃₁ p →
             (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)
@@ -125,7 +125,7 @@ module Cubical.Data.Containers.CoinductiveContainers
             (β̅₂ y) 
             (β̃₂ y)}
           λ β̃₂ comm1 →
-            prop-elim -- S is a set so equality on S is a prop
+            propElim -- S is a set so equality on S is a prop
               {A = (λ y → βs y) ≡ βs}
               (isSetΠ (λ _ → setS) (λ y → βs y) βs)
               (λ s-eq →
@@ -139,7 +139,7 @@ module Cubical.Data.Containers.CoinductiveContainers
                                    (λ ind q b → β̃₂ (βh y q) ind b)) →
                          (β̅₂ y) ≡ (β̃₂ y))
               refl
-              (prop-elim -- M' is a set so equality on M' is a prop
+              (propElim -- M' is a set so equality on M' is a prop
                 {A = (y : Y) →
                      (λ x → β̅₁ (βh y x)) ≡ (λ x → β̅₁ (βh y x))}
                 (isPropΠ λ y' → isSetΠ (λ _ → setM setS) (β̅₁ ∘ βh y') (β̅₁ ∘ βh y'))
@@ -151,23 +151,28 @@ module Cubical.Data.Containers.CoinductiveContainers
                                      (λ ind q b → β̃₂ (βh y q) ind b)) →
                          (β̅₂ y) ≡ (β̃₂ y))
                 (λ _ → refl)
-                λ comm3 comm4 → funExt (λ ind → funExt (snd-eq-aux β̃₂ comm3 comm4 y ind)))
+                λ comm3 comm4 → funExt (λ ind → funExt (sndEqAux β̃₂ comm3 comm4 y ind)))
               comm1
         where
-          snd-eq-aux : (β̃₂ : (s : Y) (i : Ind) → Pos MAlg i (β̅₁ s) → X i)
-                       (c3 : (s : Y) → (λ ind p → β̃₂ s ind (here p)) ≡ βg s)
-                       (c4 : (s : Y) → (λ ind q b → β̃₂ s ind (below q b)) ≡
-                                       (λ ind q → β̃₂ (βh s q) ind))
-                       (y : Y) (ind : Ind) (pos : Pos MAlg ind (β̅₁ y)) → β̅₂ y ind pos ≡ β̃₂ y ind pos
-          snd-eq-aux β̃₂ c3 c4 y ind (here x) = sym (funExt⁻ (funExt⁻ (c3 y) ind) x)
-          snd-eq-aux β̃₂ c3 c4 y ind (below q x) =
-            snd-eq-aux β̃₂ c3 c4 (βh y q) ind x ∙ funExt⁻ (funExt⁻ (sym (funExt⁻ (c4 y) ind)) q) x
-
-      snd-eq : (y : Y) → PathP (λ i → (ind : Ind) → Pos MAlg ind (fst-eq y i) → X ind) (β̃₂ y) (β̅₂ y)
-      snd-eq y i = snd-eq-gen y β̃₁ (sym (funExt fst-eq)) β̃₂ (funExt comm1) comm2 comm3 comm4 (~ i)
+          -- Proposition elimination
+          propElim : ∀ {ℓ} {A : Type ℓ} (t : isProp A) → (D : A → Type ℓ) →
+                      (x : A) → D x → (a : A) → D a
+          propElim t D x pr a = subst D (t x a) pr
+
+          sndEqAux : (β̃₂ : (s : Y) (i : Ind) → Pos MAlg i (β̅₁ s) → X i)
+                     (c3 : (s : Y) → (λ ind p → β̃₂ s ind (here p)) ≡ βg s)
+                     (c4 : (s : Y) → (λ ind q b → β̃₂ s ind (below q b)) ≡
+                                     (λ ind q → β̃₂ (βh s q) ind))
+                     (y : Y) (ind : Ind) (pos : Pos MAlg ind (β̅₁ y)) → β̅₂ y ind pos ≡ β̃₂ y ind pos
+          sndEqAux β̃₂ c3 c4 y ind (here x) = sym (funExt⁻ (funExt⁻ (c3 y) ind) x)
+          sndEqAux β̃₂ c3 c4 y ind (below q x) =
+            sndEqAux β̃₂ c3 c4 (βh y q) ind x ∙ funExt⁻ (funExt⁻ (sym (funExt⁻ (c4 y) ind)) q) x
+
+      sndEq : (y : Y) → PathP (λ i → (ind : Ind) → Pos MAlg ind (fstEq y i) → X ind) (β̃₂ y) (β̅₂ y)
+      sndEq y i = sndEqGen y β̃₁ (sym (funExt fstEq)) β̃₂ (funExt comm1) comm2 comm3 comm4 (~ i)
 
       -- β̅ is unique
-      β̅-unique : β̃ ≡ β̅
-      fst (β̅-unique i y) = fst-eq y i
-      snd (β̅-unique i y) = snd-eq y i
+      β̅Unique : β̃ ≡ β̅
+      fst (β̅Unique i y) = fstEq y i
+      snd (β̅Unique i y) = sndEq y i
 
diff --git a/Cubical/Data/Containers/ContainerExtensionProofs.agda b/Cubical/Data/Containers/ContainerExtensionProofs.agda
index eed15a8d9..249b79150 100644
--- a/Cubical/Data/Containers/ContainerExtensionProofs.agda
+++ b/Cubical/Data/Containers/ContainerExtensionProofs.agda
@@ -8,7 +8,7 @@
 
 -}
 
-{-# OPTIONS --cubical --safe #-}
+{-# OPTIONS --safe #-}
 
 open import Agda.Builtin.Cubical.HCompU
 
@@ -44,8 +44,8 @@ module _ {C : Category ℓ ℓ'} where
     -- Proof 1 that the functor ⟦_⟧ is full and faithful
     -- Adapted from 'Containers: Constructing strictly positive types'
 
-    ⟦_⟧-fully-faithful : isFullyFaithful ⟦_⟧
-    equiv-proof (⟦_⟧-fully-faithful (S ◁ P & set-S) (T ◁ Q & set-T)) (natTrans mors nat) =
+    ⟦_⟧FullyFaithful : isFullyFaithful ⟦_⟧
+    equiv-proof (⟦_⟧FullyFaithful (S ◁ P & set-S) (T ◁ Q & set-T)) (natTrans mors nat) =
       (fib (natTrans mors nat) , fib-pf) , unique
       where
         fib : NatTrans ⟦ (S ◁ P & set-S) ⟧-obj ⟦ (T ◁ Q & set-T) ⟧-obj →
@@ -78,25 +78,24 @@ module _ {C : Category ℓ ℓ'} where
     -- Proof 2 that the functor ⟦_⟧ is full and faithful
     -- Uses the Yoneda lemma
 
-    -- Distributivity of Π over Σ
-    distrΠΣ : {A : Type ℓ''}{B : A → Type ℓ'''}{C : (a : A) → B a → Type ℓ''''} →
-              Iso ((a : A) → Σ (B a) (λ b → C a b))
-                  (Σ ((a : A) → B a) (λ f → (a : A) → C a (f a)))
-    distrΠΣ = iso
-               (λ f → (λ a → fst (f a)) , λ a → snd (f a))
-               (λ {(f , g) → λ a → f a , g a})
-               (λ _ → refl)
-               (λ _ → refl)
-
-    -- Compose heterogenous with homogenous equality
-    comp-het-hom : {A : I → Type ℓ'} (x : A i0) (y : A i1) (z : A i1) →
-                   PathP (λ i → A i) x y → y ≡ z → PathP (λ i → A i) x z
-    comp-het-hom {A} x y z p eq i = subst (λ c → PathP A x c) eq p i 
-
-    ⟦_⟧-fully-faithful' : isFullyFaithful ⟦_⟧
-    equiv-proof (⟦_⟧-fully-faithful' (S ◁ P & set-S) (T ◁ Q & set-T)) (natTrans mors nat) =
+    ⟦_⟧FullyFaithful' : isFullyFaithful ⟦_⟧
+    equiv-proof (⟦_⟧FullyFaithful' (S ◁ P & set-S) (T ◁ Q & set-T)) (natTrans mors nat) =
       (mor , mor-eq) , unique
       where
+        -- Distributivity of Π over Σ
+        distrΠΣ : {A : Type ℓ''}{B : A → Type ℓ'''}{C : (a : A) → B a → Type ℓ''''} →
+                  Iso ((a : A) → Σ (B a) (λ b → C a b))
+                      (Σ ((a : A) → B a) (λ f → (a : A) → C a (f a)))
+        fun distrΠΣ f = (λ a → fst (f a)) , λ a → snd (f a)
+        inv distrΠΣ (f , g) a = f a , g a
+        rightInv distrΠΣ _ = refl
+        leftInv distrΠΣ _ = refl
+
+        -- Compose heterogenous with homogenous equality
+        compHetHomP : {A : I → Type ℓ'} (x : A i0) (y : A i1) (z : A i1) →
+                       PathP (λ i → A i) x y → y ≡ z → PathP (λ i → A i) x z
+        compHetHomP {A} x y z p eq i = subst (λ c → PathP A x c) eq p i
+        
         nat-trans : (s : S) → FUNCTOR C (SET ℓ') [ C [ P s ,-] , ⟦ T ◁ Q & set-T ⟧-obj ]
         nat-trans s = natTrans (λ X → curry (mors X) s) nat'
           where
@@ -127,7 +126,7 @@ module _ {C : Category ℓ ℓ'} where
         unique ((u ◁ f) , m-eq) =
           ΣPathP
             (cong₂ _◁_ (funExt (λ s i → fst (N-ob (m-eq (~ i)) (P s) (s , C .id))))
-                       (funExt (λ s i → comp-het-hom
+                       (funExt (λ s i → compHetHomP
                                          (snd (mors (P s) (s , C .id)))
                                          (f s ⋆⟨ C ⟩ (C .id))
                                          (f s)
@@ -140,10 +139,11 @@ module _ {C : Category ℓ ℓ'} where
                                (λ i → m-eq i)
                                (λ i → ⟦_⟧-mor {S ◁ P & set-S} {T ◁ Q & set-T}
                                               (funExt (λ s j → fst (N-ob (m-eq (~ j)) (P s) (s , C .id))) i ◁
-                                              funExt (λ s j → comp-het-hom
+                                              funExt (λ s j → compHetHomP
                                                                  (snd (mors (P s) (s , C .id)))
                                                                  (seq' C (f s) (C .id)) (f s)
                                                                  (λ k → snd (N-ob (m-eq (~ k)) (P s) (s , C .id)))
                                                                  (C .⋆IdR (f s)) j) i))
                                (λ j → natTrans mors nat)
                square = isSet→SquareP (λ _ _ → isSetNatTrans) _ _ _ _
+               
diff --git a/Cubical/Data/Containers/InductiveContainers.agda b/Cubical/Data/Containers/InductiveContainers.agda
index 27d4ea71c..f2aa7baf5 100644
--- a/Cubical/Data/Containers/InductiveContainers.agda
+++ b/Cubical/Data/Containers/InductiveContainers.agda
@@ -5,7 +5,7 @@ by Abbott, Altenkirch, Ghani
 
 -}
 
-{-# OPTIONS --cubical --guardedness --safe #-}
+{-# OPTIONS --guardedness --safe #-}
 
 open import Cubical.Data.W
 open import Cubical.Data.Containers.Algebras
@@ -42,18 +42,18 @@ module Cubical.Data.Containers.InductiveContainers
   α̅ (w , k) = α̅' w k
 
   -- Diagram commutes 
-  α̅-comm : (s : S) (f : Q s → W S Q) (g : (i : Ind) → P i s → X i)
+  α̅Comm : (s : S) (f : Q s → W S Q) (g : (i : Ind) → P i s → X i)
            (h : (i : Ind) (q : Q s) → Pos WAlg i (f q) → X i) →
            α̅ (into ((s , f) , (g , h))) ≡ α (s , g , λ q → α̅ (f q , λ i → h i q))
-  α̅-comm s f g h = refl
+  α̅Comm s f g h = refl
 
   -- α̅ is unique
-  α̅-unique : (α̃ : Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i) → Y) →
+  α̅Unique : (α̃ : Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i) → Y) →
              ((s : S) (f : Q s → W S Q) (g : (i : Ind) → P i s → X i)
              (h : (i : Ind) (q : Q s) → Pos WAlg i (f q) → X i) →
              α̃ (into ((s , f) , (g , h))) ≡ α (s , g , λ q → α̃ (f q , λ i → h i q))) →
              α̅ ≡ α̃
-  α̅-unique α̃ α̃-comm = funExt w-rec
+  α̅Unique α̃ α̃-comm = funExt w-rec
     where
       lemma : (s : S) (f : Q s → W S Q) (g : (i : Ind) → Pos WAlg i (sup-W s f) → X i) →
               α̃ (into ((s , f) , (λ i p → g i (here p)) , (λ i q b → g i (below q b)))) ≡

From c04e8607de1e684571157d847c96544472e22ebe Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@stefbook.local>
Date: Tue, 28 May 2024 18:03:20 +0100
Subject: [PATCH 06/12] More refactoring

---
 Cubical/Codata/M/MRecord.agda                      | 14 +++++++-------
 Cubical/Data/Containers/Algebras.agda              |  4 ++--
 Cubical/Data/Containers/CoinductiveContainers.agda |  2 +-
 Cubical/Data/Containers/InductiveContainers.agda   |  4 ++--
 Cubical/Data/W.agda                                |  5 -----
 Cubical/Data/W/W.agda                              |  6 +++---
 6 files changed, 15 insertions(+), 20 deletions(-)
 delete mode 100644 Cubical/Data/W.agda

diff --git a/Cubical/Codata/M/MRecord.agda b/Cubical/Codata/M/MRecord.agda
index 7ec584a08..88f2981e2 100644
--- a/Cubical/Codata/M/MRecord.agda
+++ b/Cubical/Codata/M/MRecord.agda
@@ -25,12 +25,12 @@ record M'-R {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type) (m₀ m
 open M'-R
 
 -- Coinduction principle for M
-CoInd-M' : {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type)
+M'Coind : {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type)
           (is-bisim : {m₀ m₁ : M' S Q} → R m₀ m₁ → M'-R R m₀ m₁)
           {m₀ m₁ : M' S Q} → R m₀ m₁ → m₀ ≡ m₁ 
-shape (CoInd-M' R is-bisim r i) = s-eq (is-bisim r) i
-pos (CoInd-M' {S} {Q} R is-bisim {m₀ = m₀}{m₁ = m₁} r i) q =
-  CoInd-M' R is-bisim {m₀ = pos m₀ q₀} {m₁ = pos m₁ q₁} (p-eq (is-bisim r) q₀ q₁ q₂) i
+shape (M'Coind R is-bisim r i) = s-eq (is-bisim r) i
+pos (M'Coind {S} {Q} R is-bisim {m₀ = m₀}{m₁ = m₁} r i) q =
+  M'Coind R is-bisim {m₀ = pos m₀ q₀} {m₁ = pos m₁ q₁} (p-eq (is-bisim r) q₀ q₁ q₂) i
     where QQ : I → Type
           QQ i = Q (s-eq (is-bisim r) i)
 
@@ -45,6 +45,6 @@ pos (CoInd-M' {S} {Q} R is-bisim {m₀ = m₀}{m₁ = m₁} r i) q =
                  ((~ j ∧ i) ∧ (j ∨ i)))) ((~ k ∧ ~ i) ∨ (k ∧ i)) q
                  
 -- (Propositional) η-equality for M'
-M'-eta-eq : {S' : Type} {Q' : S' → Type} (m : M' S' Q') → sup-M (shape m) (pos m) ≡ m
-shape (M'-eta-eq m i) = shape m
-pos (M'-eta-eq m i) = pos m
+ηEqM' : {S' : Type} {Q' : S' → Type} (m : M' S' Q') → sup-M (shape m) (pos m) ≡ m
+shape (ηEqM' m i) = shape m
+pos (ηEqM' m i) = pos m
diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda
index aa115d4fc..f7ea874ef 100644
--- a/Cubical/Data/Containers/Algebras.agda
+++ b/Cubical/Data/Containers/Algebras.agda
@@ -8,7 +8,7 @@
 
 {-# OPTIONS --guardedness --safe #-}
 
-open import Cubical.Data.W
+open import Cubical.Data.W.W
 open import Cubical.Codata.M.MRecord renaming (M' to M)
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
@@ -50,7 +50,7 @@ module Algs (Ind : Type)
       isom : Iso (Σ[ s ∈ S ] (Q s → M S Q)) (M S Q)
       fun isom = uncurry sup-M
       inv isom m = shape m , pos m
-      rightInv isom m = M'-eta-eq m
+      rightInv isom m = ηEqM' m
       leftInv isom (s , f) = refl
 
   data Pos (FP : ContFuncIso S Q) (i : Ind) : carrier FP → Type where
diff --git a/Cubical/Data/Containers/CoinductiveContainers.agda b/Cubical/Data/Containers/CoinductiveContainers.agda
index 71b1dba37..61a593724 100644
--- a/Cubical/Data/Containers/CoinductiveContainers.agda
+++ b/Cubical/Data/Containers/CoinductiveContainers.agda
@@ -92,7 +92,7 @@ module Cubical.Data.Containers.CoinductiveContainers
         transport (λ i → R (comm2 y (~ i) (q-eq (~ i))) (β̅₁ (βh y q₁))) (R-intro (βh y q₁))
 
       fstEq : (y : Y) → β̃₁ y ≡ β̅₁ y
-      fstEq y = CoInd-M' {S} {Q} R isBisimR (R-intro y)
+      fstEq y = M'Coind {S} {Q} R isBisimR (R-intro y)
 
       sndEqGen : (y : Y) (β̃₁ : Y → M' S Q) (p : β̅₁ ≡ β̃₁)
                    (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)
diff --git a/Cubical/Data/Containers/InductiveContainers.agda b/Cubical/Data/Containers/InductiveContainers.agda
index f2aa7baf5..4063f5340 100644
--- a/Cubical/Data/Containers/InductiveContainers.agda
+++ b/Cubical/Data/Containers/InductiveContainers.agda
@@ -7,7 +7,7 @@ by Abbott, Altenkirch, Ghani
 
 {-# OPTIONS --guardedness --safe #-}
 
-open import Cubical.Data.W
+open import Cubical.Data.W.W
 open import Cubical.Data.Containers.Algebras
 open import Cubical.Data.Sigma
 open import Cubical.Foundations.Prelude
@@ -61,7 +61,7 @@ module Cubical.Data.Containers.InductiveContainers
       lemma s f g = cong₂ (λ w fun → α̃ (w , fun)) refl (funExt λ i → funExt (λ {(here p) → refl ; (below q b) → refl})) 
 
       w-rec : (x : Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i)) → α̅ x ≡ α̃ x
-      w-rec (w , k) = W-ind S Q
+      w-rec (w , k) = WInd S Q
                                (λ w → (k : (i : Ind) → Pos WAlg i w → X i) → α̅ (w , k) ≡ α̃ (w , k))
                                (λ {s'} {f'} ind k →
                                  (λ i → α (s' , (λ i p → k i (here p)) ,
diff --git a/Cubical/Data/W.agda b/Cubical/Data/W.agda
deleted file mode 100644
index 2e56d002a..000000000
--- a/Cubical/Data/W.agda
+++ /dev/null
@@ -1,5 +0,0 @@
-{-# OPTIONS --cubical --safe #-}
-
-module Cubical.Data.W where
-
-open import Cubical.Data.W.W public
diff --git a/Cubical/Data/W/W.agda b/Cubical/Data/W/W.agda
index b40becf09..c1a5acd20 100644
--- a/Cubical/Data/W/W.agda
+++ b/Cubical/Data/W/W.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical --safe #-}
+{-# OPTIONS --safe #-}
 
 open import Cubical.Foundations.Prelude
 
@@ -7,7 +7,7 @@ module Cubical.Data.W.W where
 data W (S : Type) (P : S → Type) : Type where
   sup-W : (s : S) → (P s → W S P) → W S P
 
-W-ind : (S : Type) (P : S → Type) (M : W S P → Type) →
+WInd : (S : Type) (P : S → Type) (M : W S P → Type) →
         (e : {s : S} {f : P s → W S P} → ((p : P s) → M (f p)) → M (sup-W s f)) →
         (w : W S P) → M w
-W-ind S P M e (sup-W s f) = e {s} {f} (λ p → W-ind S P M e (f p))
+WInd S P M e (sup-W s f) = e {s} {f} (λ p → WInd S P M e (f p))

From 9a81c817e84d0e43dd54aaf150200db275d09936 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@stefbook.local>
Date: Tue, 28 May 2024 18:16:35 +0100
Subject: [PATCH 07/12] Changes due to --guardedness flag

---
 Cubical/Codata/M/MRecord.agda                 | 22 +------------------
 Cubical/Data/Containers/Algebras.agda         |  2 +-
 .../Containers/CoinductiveContainers.agda     | 20 +++++++++++++++++
 3 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/Cubical/Codata/M/MRecord.agda b/Cubical/Codata/M/MRecord.agda
index 88f2981e2..70590ac20 100644
--- a/Cubical/Codata/M/MRecord.agda
+++ b/Cubical/Codata/M/MRecord.agda
@@ -2,7 +2,7 @@
 
 -}
 
-{-# OPTIONS --cubical --guardedness --safe #-}
+{-# OPTIONS --cubical --safe #-}
 
 open import Cubical.Foundations.Prelude
 
@@ -24,26 +24,6 @@ record M'-R {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type) (m₀ m
           → R (pos m₀ q₀) (pos m₁ q₁)
 open M'-R
 
--- Coinduction principle for M
-M'Coind : {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type)
-          (is-bisim : {m₀ m₁ : M' S Q} → R m₀ m₁ → M'-R R m₀ m₁)
-          {m₀ m₁ : M' S Q} → R m₀ m₁ → m₀ ≡ m₁ 
-shape (M'Coind R is-bisim r i) = s-eq (is-bisim r) i
-pos (M'Coind {S} {Q} R is-bisim {m₀ = m₀}{m₁ = m₁} r i) q =
-  M'Coind R is-bisim {m₀ = pos m₀ q₀} {m₁ = pos m₁ q₁} (p-eq (is-bisim r) q₀ q₁ q₂) i
-    where QQ : I → Type
-          QQ i = Q (s-eq (is-bisim r) i)
-
-          q₀ : QQ i0
-          q₀ = transp (λ j → QQ (~ j ∧ i)) (~ i) q
-
-          q₁ : QQ i1
-          q₁ = transp (λ j → QQ (j ∨ i)) i q
-
-          q₂ : PathP (λ i → QQ i) q₀ q₁
-          q₂ k = transp (λ j → QQ ((~ k ∧ ~ j ∧ i) ∨ (k ∧ (j ∨ i)) ∨
-                 ((~ j ∧ i) ∧ (j ∨ i)))) ((~ k ∧ ~ i) ∨ (k ∧ i)) q
-                 
 -- (Propositional) η-equality for M'
 ηEqM' : {S' : Type} {Q' : S' → Type} (m : M' S' Q') → sup-M (shape m) (pos m) ≡ m
 shape (ηEqM' m i) = shape m
diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda
index f7ea874ef..8eac049ad 100644
--- a/Cubical/Data/Containers/Algebras.agda
+++ b/Cubical/Data/Containers/Algebras.agda
@@ -6,7 +6,7 @@
 
 -}
 
-{-# OPTIONS --guardedness --safe #-}
+{-# OPTIONS --safe #-}
 
 open import Cubical.Data.W.W
 open import Cubical.Codata.M.MRecord renaming (M' to M)
diff --git a/Cubical/Data/Containers/CoinductiveContainers.agda b/Cubical/Data/Containers/CoinductiveContainers.agda
index 61a593724..c164efd0d 100644
--- a/Cubical/Data/Containers/CoinductiveContainers.agda
+++ b/Cubical/Data/Containers/CoinductiveContainers.agda
@@ -93,6 +93,26 @@ module Cubical.Data.Containers.CoinductiveContainers
 
       fstEq : (y : Y) → β̃₁ y ≡ β̅₁ y
       fstEq y = M'Coind {S} {Q} R isBisimR (R-intro y)
+        where
+          -- Coinduction principle for M
+          M'Coind : {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type)
+                    (is-bisim : {m₀ m₁ : M' S Q} → R m₀ m₁ → M'-R R m₀ m₁)
+                    {m₀ m₁ : M' S Q} → R m₀ m₁ → m₀ ≡ m₁ 
+          shape (M'Coind R is-bisim r i) = s-eq (is-bisim r) i
+          pos (M'Coind {S} {Q} R is-bisim {m₀ = m₀}{m₁ = m₁} r i) q =
+            M'Coind R is-bisim {m₀ = pos m₀ q₀} {m₁ = pos m₁ q₁} (p-eq (is-bisim r) q₀ q₁ q₂) i
+              where QQ : I → Type
+                    QQ i = Q (s-eq (is-bisim r) i)
+
+                    q₀ : QQ i0
+                    q₀ = transp (λ j → QQ (~ j ∧ i)) (~ i) q
+
+                    q₁ : QQ i1
+                    q₁ = transp (λ j → QQ (j ∨ i)) i q
+
+                    q₂ : PathP (λ i → QQ i) q₀ q₁
+                    q₂ k = transp (λ j → QQ ((~ k ∧ ~ j ∧ i) ∨ (k ∧ (j ∨ i)) ∨
+                           ((~ j ∧ i) ∧ (j ∨ i)))) ((~ k ∧ ~ i) ∨ (k ∧ i)) q
 
       sndEqGen : (y : Y) (β̃₁ : Y → M' S Q) (p : β̅₁ ≡ β̃₁)
                    (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)

From 4732ffcc25780a98f2f1188804aafae5832a78f2 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@stefbook.local>
Date: Tue, 28 May 2024 18:46:00 +0100
Subject: [PATCH 08/12] Moved CoinductiveContainers to Codata

---
 Cubical/{Data => Codata}/Containers/CoinductiveContainers.agda | 2 +-
 Cubical/Data/Containers/InductiveContainers.agda               | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)
 rename Cubical/{Data => Codata}/Containers/CoinductiveContainers.agda (99%)

diff --git a/Cubical/Data/Containers/CoinductiveContainers.agda b/Cubical/Codata/Containers/CoinductiveContainers.agda
similarity index 99%
rename from Cubical/Data/Containers/CoinductiveContainers.agda
rename to Cubical/Codata/Containers/CoinductiveContainers.agda
index c164efd0d..a4df01e7e 100644
--- a/Cubical/Data/Containers/CoinductiveContainers.agda
+++ b/Cubical/Codata/Containers/CoinductiveContainers.agda
@@ -17,7 +17,7 @@ open import Cubical.Data.Containers.Algebras
 open M'
 open M'-R
 
-module Cubical.Data.Containers.CoinductiveContainers
+module Cubical.Codata.Containers.CoinductiveContainers
          (Ind : Type)
          (S : Type)
          (setS : isSet S)
diff --git a/Cubical/Data/Containers/InductiveContainers.agda b/Cubical/Data/Containers/InductiveContainers.agda
index 4063f5340..d7911a79e 100644
--- a/Cubical/Data/Containers/InductiveContainers.agda
+++ b/Cubical/Data/Containers/InductiveContainers.agda
@@ -5,7 +5,7 @@ by Abbott, Altenkirch, Ghani
 
 -}
 
-{-# OPTIONS --guardedness --safe #-}
+{-# OPTIONS --safe #-}
 
 open import Cubical.Data.W.W
 open import Cubical.Data.Containers.Algebras

From 266ae08ffaf21bcd2f1c18a41e88f6ad57d6ce8b Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@stefbook.local>
Date: Tue, 28 May 2024 18:49:24 +0100
Subject: [PATCH 09/12] Edited comment

---
 Cubical/Data/Containers/Algebras.agda | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda
index 8eac049ad..cc4995063 100644
--- a/Cubical/Data/Containers/Algebras.agda
+++ b/Cubical/Data/Containers/Algebras.agda
@@ -1,7 +1,5 @@
 {- Basic definitions required for co/inductive container proofs
 
-- Proposition elimination
-
 - Definition of Pos
 
 -}

From 902c976d2483d3567a1e4c653c5021d0390d4600 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@eduroam-10-200-20-20.local.su.se>
Date: Tue, 25 Jun 2024 15:22:24 +0200
Subject: [PATCH 10/12] Cleaning with Anders

---
 Cubical/Codata/Containers/Coalgebras.agda     |  28 ++++
 .../Containers/CoinductiveContainers.agda     |  97 ++++++-------
 Cubical/Codata/M/MRecord.agda                 |  37 ++---
 Cubical/Data/Containers/Algebras.agda         |  41 ++----
 Cubical/Data/Containers/Base.agda             | 132 +++++++-----------
 .../Containers/ContainerExtensionProofs.agda  | 123 ++++++----------
 .../Data/Containers/InductiveContainers.agda  |  48 +++----
 Cubical/Data/W/W.agda                         |  16 ++-
 8 files changed, 231 insertions(+), 291 deletions(-)
 create mode 100644 Cubical/Codata/Containers/Coalgebras.agda

diff --git a/Cubical/Codata/Containers/Coalgebras.agda b/Cubical/Codata/Containers/Coalgebras.agda
new file mode 100644
index 000000000..af71cd796
--- /dev/null
+++ b/Cubical/Codata/Containers/Coalgebras.agda
@@ -0,0 +1,28 @@
+{-# OPTIONS --guardedness #-}
+
+module Cubical.Codata.Containers.Coalgebras where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+
+open import Cubical.Codata.M.MRecord
+open import Cubical.Data.Containers.Algebras
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module Coalgs (S : Type ℓ) (Q : S → Type ℓ') where
+  open Algs S Q
+  open Iso
+  open M
+
+  MAlg : ContFuncIso
+  MAlg = iso (M S Q) isom
+    where
+      isom : Iso (Σ[ s ∈ S ] (Q s → M S Q)) (M S Q)
+      fun isom = uncurry sup-M
+      inv isom m = shape m , pos m
+      rightInv isom m = ηEqM m
+      leftInv isom (s , f) = refl
diff --git a/Cubical/Codata/Containers/CoinductiveContainers.agda b/Cubical/Codata/Containers/CoinductiveContainers.agda
index a4df01e7e..97221b01e 100644
--- a/Cubical/Codata/Containers/CoinductiveContainers.agda
+++ b/Cubical/Codata/Containers/CoinductiveContainers.agda
@@ -5,7 +5,7 @@ by Abbott, Altenkirch, Ghani
 
 -}
 
-{-# OPTIONS --guardedness --safe #-}
+{-# OPTIONS --guardedness #-}
 
 open import Cubical.Codata.M.MRecord
 open import Cubical.Data.Sigma
@@ -13,9 +13,10 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 
+open import Cubical.Codata.Containers.Coalgebras
 open import Cubical.Data.Containers.Algebras
-open M'
-open M'-R
+open M
+open M-R
 
 module Cubical.Codata.Containers.CoinductiveContainers
          (Ind : Type)
@@ -23,34 +24,35 @@ module Cubical.Codata.Containers.CoinductiveContainers
          (setS : isSet S)
          (P : Ind → S → Type)
          (Q : S → Type)
-         (setM : isSet S → isSet (M' S Q))
+         (setM : isSet S → isSet (M S Q))
          (X : Ind → Type)
          (Y : Type)
          (βs : Y → S)
          (βg : (y : Y) → (i : Ind) → P i (βs y) → X i)
          (βh : (y : Y) → Q (βs y) → Y) where
-         
-    open Algs Ind S P Q X Y
 
-    β̅₁ : Y → M' S Q
+    open Algs S Q
+    open Coalgs S Q
+
+    β̅₁ : Y → M S Q
     shape (β̅₁ y) = βs y
     pos (β̅₁ y) = β̅₁ ∘ βh y
 
-    β̅₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̅₁ y) → X ind
+    β̅₂ : (y : Y) (ind : Ind) → Pos P MAlg ind (β̅₁ y) → X ind
     β̅₂ y ind (here p) = βg y ind p
     β̅₂ y ind (below q p) = β̅₂ (βh y q) ind p
 
-    β̅ : Y → Σ[ m ∈ M' S Q ] ((i : Ind) → Pos MAlg i m → X i)
+    β̅ : Y → Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i)
     β̅ y = β̅₁ y , β̅₂ y
-    
-    out : Σ[ m ∈ M' S Q ] ((i : Ind) → Pos MAlg i m → X i) →
-          Σ[ (s , f) ∈ Σ[ s ∈ S ] (Q s → M' S Q) ]
+
+    out : Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i) →
+          Σ[ (s , f) ∈ Σ[ s ∈ S ] (Q s → M S Q) ]
             (((i : Ind) → P i s → X i) ×
-            ((i : Ind) (q : Q s) → Pos MAlg i (f q) → X i))
+            ((i : Ind) (q : Q s) → Pos P MAlg i (f q) → X i))
     out (m , k) = (shape m , pos m) , ((λ i p → k i (here p)) , (λ i q p → k i (below q p)))
 
-    module _ (β̃₁ : Y → M' S Q)
-             (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)
+    module _ (β̃₁ : Y → M S Q)
+             (β̃₂ : (y : Y) (ind : Ind) → Pos P MAlg ind (β̃₁ y) → X ind)
              (comm : (y : Y) →
                      out (β̃₁ y , β̃₂ y) ≡
                      ((βs y , λ q → (β̃₁ (βh y q))) , (βg y , λ i q → (β̃₂ (βh y q)) i))) where
@@ -59,7 +61,7 @@ module Cubical.Codata.Containers.CoinductiveContainers
       β̅Comm : (y : Y) → out (β̅ y) ≡ ((βs y , β̅₁ ∘ (βh y)) , (βg y , λ i q → β̅₂ (βh y q) i))
       β̅Comm y = refl
 
-      β̃ : Y → Σ (M' S Q) (λ m → (i : Ind) → Pos MAlg i m → X i)
+      β̃ : Y → Σ (M S Q) (λ m → (i : Ind) → Pos P MAlg i m → X i)
       β̃ y = β̃₁ y , β̃₂ y
 
       ----------
@@ -68,7 +70,7 @@ module Cubical.Codata.Containers.CoinductiveContainers
       comm1 y i = fst (fst (comm y i))
 
       comm2 : (y : Y) →
-                   PathP (λ i → Q (comm1 y i) → M' S Q)
+                   PathP (λ i → Q (comm1 y i) → M S Q)
                          (pos (β̃₁ y)) (λ q → β̃₁ (βh y q))
       comm2 y i = snd (fst (comm y i))
 
@@ -78,29 +80,29 @@ module Cubical.Codata.Containers.CoinductiveContainers
       comm3 y i = fst (snd (comm y i))
 
       comm4 : (y : Y) → PathP (λ i → (ind : Ind) → (q : Q (comm1 y i)) →
-                              Pos MAlg ind (comm2 y i q) → X ind)
+                              Pos P MAlg ind (comm2 y i q) → X ind)
                               (λ ind q b → β̃₂ y ind (below q b))
                               (λ ind q b → β̃₂ (βh y q) ind b)
       comm4 y i = snd (snd (comm y i))
 
-      data R : M' S Q → M' S Q → Type where
+      data R : M S Q → M S Q → Type where
         R-intro : (y : Y) → R (β̃₁ y) (β̅₁ y)
 
-      isBisimR : {m₀ : M' S Q} {m₁ : M' S Q} → R m₀ m₁ → M'-R R m₀ m₁
+      isBisimR : {m₀ : M S Q} {m₁ : M S Q} → R m₀ m₁ → M-R R m₀ m₁
       s-eq (isBisimR (R-intro y)) = comm1 y
-      p-eq (isBisimR (R-intro y)) q₀ q₁ q-eq = 
+      p-eq (isBisimR (R-intro y)) q₀ q₁ q-eq =
         transport (λ i → R (comm2 y (~ i) (q-eq (~ i))) (β̅₁ (βh y q₁))) (R-intro (βh y q₁))
 
       fstEq : (y : Y) → β̃₁ y ≡ β̅₁ y
-      fstEq y = M'Coind {S} {Q} R isBisimR (R-intro y)
+      fstEq y = MCoind {S} {Q} R isBisimR (R-intro y)
         where
           -- Coinduction principle for M
-          M'Coind : {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type)
-                    (is-bisim : {m₀ m₁ : M' S Q} → R m₀ m₁ → M'-R R m₀ m₁)
-                    {m₀ m₁ : M' S Q} → R m₀ m₁ → m₀ ≡ m₁ 
-          shape (M'Coind R is-bisim r i) = s-eq (is-bisim r) i
-          pos (M'Coind {S} {Q} R is-bisim {m₀ = m₀}{m₁ = m₁} r i) q =
-            M'Coind R is-bisim {m₀ = pos m₀ q₀} {m₁ = pos m₁ q₁} (p-eq (is-bisim r) q₀ q₁ q₂) i
+          MCoind : {S : Type} {Q : S → Type} (R : M S Q → M S Q → Type)
+                    (is-bisim : {m₀ m₁ : M S Q} → R m₀ m₁ → M-R R m₀ m₁)
+                    {m₀ m₁ : M S Q} → R m₀ m₁ → m₀ ≡ m₁
+          shape (MCoind R is-bisim r i) = s-eq (is-bisim r) i
+          pos (MCoind {S} {Q} R is-bisim {m₀ = m₀}{m₁ = m₁} r i) q =
+            MCoind R is-bisim {m₀ = pos m₀ q₀} {m₁ = pos m₁ q₁} (p-eq (is-bisim r) q₀ q₁ q₂) i
               where QQ : I → Type
                     QQ i = Q (s-eq (is-bisim r) i)
 
@@ -114,58 +116,58 @@ module Cubical.Codata.Containers.CoinductiveContainers
                     q₂ k = transp (λ j → QQ ((~ k ∧ ~ j ∧ i) ∨ (k ∧ (j ∨ i)) ∨
                            ((~ j ∧ i) ∧ (j ∨ i)))) ((~ k ∧ ~ i) ∨ (k ∧ i)) q
 
-      sndEqGen : (y : Y) (β̃₁ : Y → M' S Q) (p : β̅₁ ≡ β̃₁)
-                   (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)
+      sndEqGen : (y : Y) (β̃₁ : Y → M S Q) (p : β̅₁ ≡ β̃₁)
+                   (β̃₂ : (y : Y) (ind : Ind) → Pos P MAlg ind (β̃₁ y) → X ind)
                    (comm1 : shape ∘ β̃₁ ≡ βs)
-                   (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M' S Q)
+                   (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M S Q)
                                             (pos (β̃₁ y)) (β̃₁ ∘ βh y))
                    (comm3 : (y : Y) → PathP (λ i  → (ind : Ind) → P ind (comm1 i y) → X ind)
                                             (λ ind p → β̃₂ y ind (here p))
                                             (βg y))
                    (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (comm1 i y)) →
-                                            Pos MAlg ind (comm2 y i q) → X ind)
+                                            Pos P MAlg ind (comm2 y i q) → X ind)
                                             (λ ind q b → β̃₂ y ind (below q b))
                                             λ ind q b → β̃₂ (βh y q) ind b) →
-                   PathP (λ i → (ind : Ind) → Pos MAlg ind (p i y) → X ind)
+                   PathP (λ i → (ind : Ind) → Pos P MAlg ind (p i y) → X ind)
                          (β̅₂ y) (β̃₂ y)
       sndEqGen y =
         J>_ -- we're applying J to p : makeβ̅₁ βs βg βh ≡ β̅₁
           {P = λ β̃₁ p →
-            (β̃₂ : (y : Y) (ind : Ind) → Pos MAlg ind (β̃₁ y) → X ind)
+            (β̃₂ : (y : Y) (ind : Ind) → Pos P MAlg ind (β̃₁ y) → X ind)
             (comm1 : shape ∘ β̃₁ ≡ βs)
-            (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M' S Q) (pos (β̃₁ y)) (β̃₁ ∘ βh y))
+            (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M S Q) (pos (β̃₁ y)) (β̃₁ ∘ βh y))
             (comm3 : (y : Y) → PathP (λ i  → (ind : Ind) → P ind (comm1 i y) → X ind)
                      (λ ind p → β̃₂ y ind (here p))
                      (βg y))
-            (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (comm1 i y)) → Pos MAlg ind
+            (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (comm1 i y)) → Pos P MAlg ind
                                (comm2 y i q) → X ind)
                      (λ ind q b → β̃₂ y ind (below q b))
                      λ ind q b → β̃₂ (βh y q) ind b) →
-            PathP (λ i → (ind : Ind) → Pos MAlg ind (p i y) → X ind)
-            (β̅₂ y) 
+            PathP (λ i → (ind : Ind) → Pos P MAlg ind (p i y) → X ind)
+            (β̅₂ y)
             (β̃₂ y)}
           λ β̃₂ comm1 →
             propElim -- S is a set so equality on S is a prop
               {A = (λ y → βs y) ≡ βs}
               (isSetΠ (λ _ → setS) (λ y → βs y) βs)
               (λ s-eq →
-                (comm2 : (y : Y) → PathP (λ i → Q (s-eq i y) → M' S Q)
+                (comm2 : (y : Y) → PathP (λ i → Q (s-eq i y) → M S Q)
                                    (β̅₁ ∘ βh y) (β̅₁ ∘ βh y))
                 (comm3 : (y : Y) → PathP (λ i  → (ind : Ind) → P ind (s-eq i y) → X ind)
                                    (λ ind p → β̃₂ y ind (here p)) (βg y))
-                (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (s-eq i y)) → Pos MAlg ind
+                (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (s-eq i y)) → Pos P MAlg ind
                                    (comm2 y i q) → X ind)
                                    (λ ind q b → β̃₂ y ind (below q b))
                                    (λ ind q b → β̃₂ (βh y q) ind b)) →
                          (β̅₂ y) ≡ (β̃₂ y))
               refl
-              (propElim -- M' is a set so equality on M' is a prop
+              (propElim -- M is a set so equality on M is a prop
                 {A = (y : Y) →
                      (λ x → β̅₁ (βh y x)) ≡ (λ x → β̅₁ (βh y x))}
                 (isPropΠ λ y' → isSetΠ (λ _ → setM setS) (β̅₁ ∘ βh y') (β̅₁ ∘ βh y'))
-                (λ m-eq → 
+                (λ m-eq →
                   (comm3 : (y : Y) → (λ ind p → β̃₂ y ind (here p)) ≡ (βg y))
-                  (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (βs y)) → Pos MAlg ind
+                  (comm4 : (y : Y) → PathP (λ i → (ind : Ind) (q : Q (βs y)) → Pos P MAlg ind
                                      (m-eq y i q) → X ind)
                                      (λ ind q b → β̃₂ y ind (below q b))
                                      (λ ind q b → β̃₂ (βh y q) ind b)) →
@@ -175,24 +177,23 @@ module Cubical.Codata.Containers.CoinductiveContainers
               comm1
         where
           -- Proposition elimination
-          propElim : ∀ {ℓ} {A : Type ℓ} (t : isProp A) → (D : A → Type ℓ) →
+          propElim : ∀ {ℓ ℓ'} {A : Type ℓ} (t : isProp A) → (D : A → Type ℓ') →
                       (x : A) → D x → (a : A) → D a
           propElim t D x pr a = subst D (t x a) pr
 
-          sndEqAux : (β̃₂ : (s : Y) (i : Ind) → Pos MAlg i (β̅₁ s) → X i)
+          sndEqAux : (β̃₂ : (s : Y) (i : Ind) → Pos P MAlg i (β̅₁ s) → X i)
                      (c3 : (s : Y) → (λ ind p → β̃₂ s ind (here p)) ≡ βg s)
                      (c4 : (s : Y) → (λ ind q b → β̃₂ s ind (below q b)) ≡
                                      (λ ind q → β̃₂ (βh s q) ind))
-                     (y : Y) (ind : Ind) (pos : Pos MAlg ind (β̅₁ y)) → β̅₂ y ind pos ≡ β̃₂ y ind pos
+                     (y : Y) (ind : Ind) (pos : Pos P MAlg ind (β̅₁ y)) → β̅₂ y ind pos ≡ β̃₂ y ind pos
           sndEqAux β̃₂ c3 c4 y ind (here x) = sym (funExt⁻ (funExt⁻ (c3 y) ind) x)
           sndEqAux β̃₂ c3 c4 y ind (below q x) =
             sndEqAux β̃₂ c3 c4 (βh y q) ind x ∙ funExt⁻ (funExt⁻ (sym (funExt⁻ (c4 y) ind)) q) x
 
-      sndEq : (y : Y) → PathP (λ i → (ind : Ind) → Pos MAlg ind (fstEq y i) → X ind) (β̃₂ y) (β̅₂ y)
+      sndEq : (y : Y) → PathP (λ i → (ind : Ind) → Pos P MAlg ind (fstEq y i) → X ind) (β̃₂ y) (β̅₂ y)
       sndEq y i = sndEqGen y β̃₁ (sym (funExt fstEq)) β̃₂ (funExt comm1) comm2 comm3 comm4 (~ i)
 
       -- β̅ is unique
       β̅Unique : β̃ ≡ β̅
       fst (β̅Unique i y) = fstEq y i
       snd (β̅Unique i y) = sndEq y i
-
diff --git a/Cubical/Codata/M/MRecord.agda b/Cubical/Codata/M/MRecord.agda
index 70590ac20..d55f5027b 100644
--- a/Cubical/Codata/M/MRecord.agda
+++ b/Cubical/Codata/M/MRecord.agda
@@ -2,29 +2,34 @@
 
 -}
 
-{-# OPTIONS --cubical --safe #-}
+{-# OPTIONS --guardedness #-}
+
+module Cubical.Codata.M.MRecord where
 
 open import Cubical.Foundations.Prelude
 
-module Cubical.Codata.M.MRecord where
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
 
-record M' (S : Type) (P : S → Type) : Type where
+record M (S : Type ℓ) (P : S → Type ℓ') : Type (ℓ-max ℓ ℓ') where
   constructor sup-M
   coinductive
   field
     shape : S
-    pos : P shape → M' S P
-open M'
+    pos : P shape → M S P
+open M
 
--- Lifting M' to relations
-record M'-R {S : Type} {Q : S → Type} (R : M' S Q → M' S Q → Type) (m₀ m₁ : M' S Q) : Type where
+-- Lifting M to relations
+record M-R {S : Type ℓ} {Q : S → Type ℓ'} (R : M S Q → M S Q → Type ℓ'')
+           (m₀ m₁ : M S Q) : Type (ℓ-max ℓ (ℓ-max ℓ' ℓ'')) where
   field
-   s-eq : shape m₀ ≡ shape m₁        
-   p-eq : (q₀ : Q (shape m₀))(q₁ : Q (shape m₁))(q-eq : PathP (λ i → Q (s-eq i)) q₀ q₁)
-          → R (pos m₀ q₀) (pos m₁ q₁)
-open M'-R
-
--- (Propositional) η-equality for M'
-ηEqM' : {S' : Type} {Q' : S' → Type} (m : M' S' Q') → sup-M (shape m) (pos m) ≡ m
-shape (ηEqM' m i) = shape m
-pos (ηEqM' m i) = pos m
+   s-eq : shape m₀ ≡ shape m₁
+   p-eq : (q₀ : Q (shape m₀)) (q₁ : Q (shape m₁))
+          (q-eq : PathP (λ i → Q (s-eq i)) q₀ q₁) → R (pos m₀ q₀) (pos m₁ q₁)
+open M-R
+
+-- (Propositional) η-equality for M
+ηEqM : {S' : Type ℓ} {Q' : S' → Type ℓ'} (m : M S' Q') → sup-M (shape m) (pos m) ≡ m
+shape (ηEqM m i) = shape m
+pos (ηEqM m i) = pos m
diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda
index cc4995063..db939004e 100644
--- a/Cubical/Data/Containers/Algebras.agda
+++ b/Cubical/Data/Containers/Algebras.agda
@@ -4,36 +4,32 @@
 
 -}
 
-{-# OPTIONS --safe #-}
+module Cubical.Data.Containers.Algebras where
 
 open import Cubical.Data.W.W
-open import Cubical.Codata.M.MRecord renaming (M' to M)
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Prelude
 
-module Cubical.Data.Containers.Algebras where
+private
+  variable
+    ℓ ℓ' ℓ'' ℓ''' : Level
 
-module Algs (Ind : Type)
-            (S : Type)
-            (P : Ind → S → Type)
-            (Q : S → Type)
-            (X : Ind → Type)
-            (Y : Type) where
+module Algs (S : Type ℓ)
+            (Q : S → Type ℓ') where
 
-  open M
   open Iso
 
   -- Fixed point algebras
-  record ContFuncIso (S : Type) (P : S → Type) : Type₁ where
+  record ContFuncIso : Type (ℓ-max (ℓ-suc ℓ'') (ℓ-max ℓ ℓ')) where
     constructor iso
     field
-      carrier : Type
-      χ : Iso (Σ[ s ∈ S ] (P s → carrier)) carrier
+      carrier : Type ℓ''
+      χ : Iso (Σ[ s ∈ S ] (Q s → carrier)) carrier
 
   open ContFuncIso
 
-  WAlg : ContFuncIso S Q
+  WAlg : ContFuncIso
   WAlg = iso (W S Q) isom
     where
       isom : Iso (Σ[ s ∈ S ] (Q s → W S Q)) (W S Q)
@@ -42,17 +38,8 @@ module Algs (Ind : Type)
       rightInv isom (sup-W s f) = refl
       leftInv isom (s , f) = refl
 
-  MAlg : ContFuncIso S Q
-  MAlg = iso (M S Q) isom
-    where
-      isom : Iso (Σ[ s ∈ S ] (Q s → M S Q)) (M S Q)
-      fun isom = uncurry sup-M
-      inv isom m = shape m , pos m
-      rightInv isom m = ηEqM' m
-      leftInv isom (s , f) = refl
-
-  data Pos (FP : ContFuncIso S Q) (i : Ind) : carrier FP → Type where
-    here : {wm : carrier FP} → P i (fst (FP .χ .inv wm)) → Pos FP i wm
+  data Pos {Ind : Type ℓ'''} (P : Ind → S → Type ℓ'') (FP : ContFuncIso {ℓ}) (i : Ind) :
+           carrier FP → Type (ℓ-max (ℓ-suc ℓ) (ℓ-max ℓ'' ℓ')) where
+    here : {wm : carrier FP} → P i (fst (FP .χ .inv wm)) → Pos P FP i wm
     below : {wm : carrier FP} → (q : Q (fst (FP .χ .inv wm))) →
-            Pos FP i (snd (FP .χ .inv wm) q) → Pos FP i wm
-
+            Pos P FP i (snd (FP .χ .inv wm) q) → Pos P FP i wm
diff --git a/Cubical/Data/Containers/Base.agda b/Cubical/Data/Containers/Base.agda
index 01d18f741..717f5a945 100644
--- a/Cubical/Data/Containers/Base.agda
+++ b/Cubical/Data/Containers/Base.agda
@@ -10,10 +10,9 @@
 
 -}
 
+module Cubical.Data.Containers.Base where
 
-{-# OPTIONS --safe #-}
-
-open import Cubical.Categories.Category.Base 
+open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Instances.Functors
@@ -21,8 +20,6 @@ open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧)
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Prelude hiding (_◁_)
 
-module Cubical.Data.Containers.Base where
-
 private
   variable
     ℓ ℓ' : Level
@@ -33,22 +30,22 @@ open NatTrans
 
 -- Definition of generalised container
 record GenContainer (C : Category ℓ ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
-  constructor _◁_&_ 
+  constructor _◁_&_
   field
-    S : Type ℓ' 
-    P : S → ob C
+    S : Type ℓ'
+    P : S → C .ob
     isSetS : isSet S
 
 open GenContainer
 
-module Conts {C : Category ℓ ℓ'} where
+module Conts (C : Category ℓ ℓ') where
 
   -- Category Cont with objects of type GenContainer C
   record _⇒c_ (C₁ C₂ : GenContainer C) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
     constructor _◁_
     field
-      u : S C₁ → S C₂
-      f : (s : S C₁) → C [ P C₂ (u s) , P C₁ s ]
+      shape : S C₁ → S C₂
+      pos : (s : S C₁) → C [ P C₂ (shape s) , P C₁ s ]
 
   open _⇒c_
 
@@ -63,106 +60,73 @@ module Conts {C : Category ℓ ℓ'} where
   assoc-c (u ◁ f) (v ◁ g) (w ◁ h) i = (λ a → w (v (u a))) ◁ λ a → C .⋆Assoc (h (v (u a))) (g (u a)) (f a) (~ i)
 
   isSet⇒c : {C₁ C₂ : GenContainer C} → isSet (C₁ ⇒c C₂)
-  u (isSet⇒c {A ◁ B & set-A} {E ◁ F & set-C} m n p q i j) a =
-    set-C (u m a) (u n a) (λ k → u (p k) a) (λ k → u (q k) a) i j
-  f (isSet⇒c {A ◁ B & set-A} {E ◁ F & set-C} m n p q i j) a =
+  shape (isSet⇒c {A ◁ B & set-A} {E ◁ F & set-C} m n p q i j) a =
+    set-C (shape m a) (shape n a) (λ k → shape (p k) a) (λ k → shape (q k) a) i j
+  pos (isSet⇒c {A ◁ B & set-A} {E ◁ F & set-C} m n p q i j) a =
     isSet→SquareP
-      {A = λ i j → C [ (F (set-C (u m a) (u n a) (λ k → u (p k) a) (λ k → u (q k) a) i j)) ,  B a ]} 
-      (λ i j → C .isSetHom {F (set-C (u m a) (u n a) (λ k → u (p k) a) (λ k → u (q k) a) i j)} {B a})
-      (λ k → f (p k) a)
-      (λ k → f (q k) a)
-      (λ _ → f m a)
-      (λ _ → f n a)
+      {A = λ i j → C [ (F (set-C (shape m a) (shape n a) (λ k → shape (p k) a) (λ k → shape (q k) a) i j)) ,  B a ]}
+      (λ i j → C .isSetHom {F (set-C (shape m a) (shape n a) (λ k → shape (p k) a) (λ k → shape (q k) a) i j)} {B a})
+      (λ k → pos (p k) a)
+      (λ k → pos (q k) a)
+      (λ _ → pos m a)
+      (λ _ → pos n a)
       i j
 
   Cont : Category (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-suc (ℓ-max ℓ ℓ'))
-  Cont = record
-           { ob = GenContainer C
-           ; Hom[_,_] = _⇒c_
-           ; id = id-c
-           ; _⋆_ = _⋆c_
-           ; ⋆IdL = λ m i → (u m) ◁ (λ a → C .⋆IdR (f m a) i)
-           ; ⋆IdR = λ m i → (u m) ◁ (λ a → C .⋆IdL (f m a) i)
-           ; ⋆Assoc = assoc-c
-           ; isSetHom = isSet⇒c
-           }
+  ob Cont = GenContainer C
+  Hom[_,_] Cont = _⇒c_
+  id Cont = id-c
+  _⋆_ Cont = _⋆c_
+  ⋆IdL Cont m i = (shape m) ◁ (λ a → C .⋆IdR (pos m a) i)
+  ⋆IdR Cont m i = (shape m) ◁ (λ a → C .⋆IdL (pos m a) i)
+  ⋆Assoc Cont = assoc-c
+  isSetHom Cont = isSet⇒c
 
   -- Definition of functor ⟦_⟧ : Cont → Functor C Set
 
-  -- Type alias for (S : Type) (P : S → C .ob) (X : C .ob) ↦ Σ S (λ s → C [ P s , X ]) 
+  -- Type alias for (S : Type) (P : S → C .ob) (X : C .ob) ↦ Σ S (λ s → C [ P s , X ])
   cont-func : (S : Type ℓ') (P : S → C .ob) (X : C .ob) → Type ℓ'
   cont-func S P X = Σ S (λ s → C [ P s , X ])
 
-  isSetContFunc : (A : Type ℓ') (B : A → ob C) (X : ob C) (isSetA : isSet A) → isSet (cont-func A B X)
-  fst (isSetContFunc A B X setA s₁ s₂ p q i j) =
-    setA (fst s₁) (fst s₂) (λ k → fst (p k)) (λ k → fst (q k)) i j
-  snd (isSetContFunc A B X setA s₁ s₂ p q i j) = 
-      isSet→SquareP
-      {A = λ i j → C [ (B (setA (fst s₁) (fst s₂) (λ k → fst (p k)) (λ k → fst (q k)) i j)) , X ]}
-      (λ i j → C .isSetHom {B (setA (fst s₁) (fst s₂) (λ k → fst (p k)) (λ k → fst (q k)) i j)} {X})
-      (λ k → snd (p k))
-      (λ k → snd (q k))
-      (λ _ → snd s₁)
-      (λ _ → snd s₂)
-      i j
+  isSetContFunc : (A : Type ℓ') (B : A → C .ob) (X : C .ob) (isSetA : isSet A) → isSet (cont-func A B X)
+  isSetContFunc A B X setA = isSetΣ setA (λ _ → C .isSetHom)
 
-  cont-mor : {A : Type ℓ'} {B : A → ob C} {X Y : ob C} (f : C [ X , Y ]) →
+  cont-mor : {A : Type ℓ'} {B : A → C .ob} {X Y : C .ob} (f : C [ X , Y ]) →
              cont-func A B X → cont-func A B Y
   cont-mor f (s , g) = s , (g ⋆⟨ C ⟩ f)
 
   ⟦_⟧-obj : GenContainer C → Functor C (SET ℓ')
-  ⟦ (A ◁ B & set-A) ⟧-obj = record {
-                                    F-ob = λ X → cont-func A B X , isSetContFunc A B X set-A ;
-                                    F-hom = cont-mor ;
-                                    F-id = funExt λ {(a , b) i → a , C .⋆IdR b i} ;
-                                    F-seq = λ f g i (a , b) → a , C .⋆Assoc b f g (~ i) 
-                                   }
+  F-ob ⟦ A ◁ B & set-A ⟧-obj X = cont-func A B X , isSetContFunc A B X set-A
+  F-hom ⟦ A ◁ B & set-A ⟧-obj = cont-mor
+  F-id ⟦ A ◁ B & set-A ⟧-obj = funExt λ {(a , b) i → a , C .⋆IdR b i}
+  F-seq ⟦ A ◁ B & set-A ⟧-obj f g i (a , b) = a , C .⋆Assoc b f g (~ i)
 
   ⟦_⟧-mor : {C₁ C₂ : GenContainer C} → C₁ ⇒c C₂ → NatTrans ⟦ C₁ ⟧-obj ⟦ C₂ ⟧-obj
   N-ob (⟦_⟧-mor (u ◁ f)) X (s , p) = u s , ((f s) ⋆⟨ C ⟩ p)
   N-hom (⟦_⟧-mor (u ◁ f)) xy i (a , b) = u a , C .⋆Assoc (f a) b xy (~ i)
 
   ⟦_⟧-id : {C₁ : GenContainer C} → ⟦_⟧-mor {C₁} {C₁} (id-c {C₁}) ≡ idTrans ⟦ C₁ ⟧-obj
-  N-ob (⟦_⟧-id {S ◁ P & set-S} i) X (s , p) = s , C .⋆IdL p i
-  N-hom (⟦_⟧-id {S ◁ P & set-S} i) {X} {Y} xy j (s , p) = square i j
-    where
-      square : Square
-                 (λ j → N-hom (⟦_⟧-mor {S ◁ P & set-S} {S ◁ P & set-S} id-c) xy j (s , p))
-                 (λ j → N-hom (idTrans ⟦ S ◁ P & set-S ⟧-obj) xy j (s , p))
-                 (λ i → s , C .⋆IdL ((C ⋆ p) xy) i)
-                 (λ i → s , (C ⋆ C .⋆IdL p i) xy)
-      square = isSet→SquareP (λ i j → isSetContFunc S P Y set-S) _ _ _ _
+  ⟦_⟧-id = makeNatTransPath λ i X (s , p) → s , C .⋆IdL p i
 
   ⟦_⟧-comp : {U V W : GenContainer C} (g : U ⇒c V) (h : V ⇒c W) →
              ⟦ g ⋆c h ⟧-mor ≡ ⟦ g ⟧-mor ⋆⟨ FUNCTOR C (SET ℓ') ⟩ ⟦ h ⟧-mor
-  N-ob (⟦_⟧-comp {U} {V} {W} (ug ◁ fg) (uh ◁ fh) i) A (s , p) = uh (ug s) , C .⋆Assoc (fh (ug s)) (fg s) p i
-  N-hom (⟦_⟧-comp {U} {V} {W} (ug ◁ fg) (uh ◁ fh) i) {X} {Y} xy j (s , p) = square i j 
-    where
-      square : Square
-                (λ j → N-hom (⟦_⟧-mor {U} {W} (_⋆c_ {U} {V} {W} (ug ◁ fg) (uh ◁ fh))) {X} {Y} xy j (s , p))
-                (λ j → N-hom (seq' (FUNCTOR C (SET ℓ')) {⟦ U ⟧-obj} {⟦ V ⟧-obj} {⟦ W ⟧-obj}
-                       (⟦_⟧-mor {U} {V} (ug ◁ fg)) (⟦_⟧-mor {V} {W} (uh ◁ fh))) xy j (s , p)) 
-                (λ i → uh (ug s) , C .⋆Assoc (fh (ug s)) (fg s) ((C ⋆ p) xy) i)
-                (λ i → uh (ug s) , (C ⋆ C .⋆Assoc (fh (ug s)) (fg s) p i) xy)
-      square = isSet→SquareP (λ i j → isSetContFunc (S W) (P W) Y (isSetS W)) _ _ _ _
+  ⟦_⟧-comp (ug ◁ fg) (uh ◁ fh) =
+    makeNatTransPath λ i A (s , p) → uh (ug s) , C .⋆Assoc (fh (ug s)) (fg s) p i
 
   ⟦_⟧ : Functor Cont (FUNCTOR C (SET ℓ'))
-  ⟦_⟧ = record {
-                F-ob = ⟦_⟧-obj ;
-                F-hom = ⟦_⟧-mor ;
-                F-id = λ {A} → ⟦_⟧-id {A} ;
-                F-seq = ⟦_⟧-comp
-               }
-              
--- Example
+  F-ob ⟦_⟧ = ⟦_⟧-obj
+  F-hom ⟦_⟧ = ⟦_⟧-mor
+  F-id ⟦_⟧ = ⟦_⟧-id
+  F-seq ⟦_⟧ = ⟦_⟧-comp
 
-open Conts {C = SET (ℓ-zero)}
+module Example where
+  open Conts (SET ℓ-zero)
 
-open import Cubical.Data.Fin
-open import Cubical.Data.Nat
+  open import Cubical.Data.Fin
+  open import Cubical.Data.Nat
 
-ListC : GenContainer (SET (ℓ-zero))
-ListC = ℕ ◁ (λ n → Fin n , isSetFin) & isSetℕ
+  ListC : GenContainer (SET ℓ-zero)
+  ListC = ℕ ◁ (λ n → Fin n , isSetFin) & isSetℕ
 
-ListF : Functor (SET (ℓ-zero)) (SET (ℓ-zero))
-ListF = ⟦ ListC ⟧-obj
+  ListF : Functor (SET ℓ-zero) (SET ℓ-zero)
+  ListF = ⟦ ListC ⟧-obj
diff --git a/Cubical/Data/Containers/ContainerExtensionProofs.agda b/Cubical/Data/Containers/ContainerExtensionProofs.agda
index 249b79150..ffde6a754 100644
--- a/Cubical/Data/Containers/ContainerExtensionProofs.agda
+++ b/Cubical/Data/Containers/ContainerExtensionProofs.agda
@@ -8,29 +8,29 @@
 
 -}
 
-{-# OPTIONS --safe #-}
+module Cubical.Data.Containers.ContainerExtensionProofs where
+
+open import Cubical.Foundations.Prelude hiding (_◁_)
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
 
-open import Agda.Builtin.Cubical.HCompU
+open import Cubical.Functions.FunExtEquiv
 
-open import Cubical.Categories.Category.Base 
+open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor
 open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧)
 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.Sigma
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Prelude hiding (_◁_)
-open import Cubical.Foundations.Equiv
-open import Cubical.Foundations.Isomorphism 
-open import Cubical.Foundations.Function
-
-module Cubical.Data.Containers.ContainerExtensionProofs where
 
 private
   variable
-    ℓ ℓ' ℓ'' ℓ''' ℓ'''' : Level
+    ℓ ℓ' : Level
 
 open Category hiding (_∘_)
 open Functor
@@ -39,7 +39,7 @@ open Iso
 
 module _ {C : Category ℓ ℓ'} where
 
-    open Conts {ℓ} {ℓ'} {C}   
+    open Conts {ℓ} {ℓ'} C
 
     -- Proof 1 that the functor ⟦_⟧ is full and faithful
     -- Adapted from 'Containers: Constructing strictly positive types'
@@ -53,27 +53,18 @@ module _ {C : Category ℓ ℓ'} where
         fib (natTrans mors _) = (fst ∘ tq) ◁ (snd ∘ tq)
           where
             tq : (s : S) → cont-func T Q (P s)
-            tq s = mors (P s) (s , C .id {P s}) 
+            tq s = mors (P s) (s , C .id {P s})
 
         fib-pf : ⟦ fib (natTrans mors nat) ⟧-mor ≡ (natTrans mors nat)
-        fib-pf = cong₂
-                   natTrans
-                   ((funExt λ X → funExt λ {(s , h) →
-                     sym (funExt⁻ (nat h) (s , C .id)) ∙ cong (λ Z → mors X (s , Z)) (C .⋆IdL h)})) 
-                   (isProp→PathP (λ i → isPropImplicitΠ2 (λ X Y → isPropΠ (λ f →
-                     isSetΠ (λ _ → isSetContFunc T Q Y set-T) _ _))) _ _) 
+        fib-pf = makeNatTransPath
+          (funExt₂ λ X (s , h) → sym (funExt⁻ (nat h) (s , C .id)) ∙
+                                 cong (λ Z → mors X (s , Z)) (C .⋆IdL h))
 
         ret : ∀ X→Y → fib (⟦ X→Y ⟧-mor) ≡ X→Y
         ret (u ◁ f) i = u ◁ λ s → C .⋆IdR (f s) i
-        
-        unique : (y : Helpers.fiber (⟦_⟧-mor) (natTrans mors nat)) → (fib (natTrans mors nat) , fib-pf) ≡ y
-        unique (m , m-eq) = ΣPathP (cong (fib) (sym m-eq) ∙ ret m , square)
-          where
-            square : Square (λ i → fib-pf i)
-                            (λ i → m-eq i)
-                            (λ i → F-hom ⟦_⟧ (((λ j → fib (m-eq (~ j))) ∙ ret m) i))
-                            refl
-            square = isSet→SquareP (λ _ _ → isSetNatTrans) _ _ _ _
+
+        unique : (y : fiber (⟦_⟧-mor) (natTrans mors nat)) → (fib (natTrans mors nat) , fib-pf) ≡ y
+        unique (m , m-eq) = Σ≡Prop (λ _ → isSetNatTrans _ _) (cong fib (sym m-eq) ∙ ret m)
 
     -- Proof 2 that the functor ⟦_⟧ is full and faithful
     -- Uses the Yoneda lemma
@@ -82,68 +73,32 @@ module _ {C : Category ℓ ℓ'} where
     equiv-proof (⟦_⟧FullyFaithful' (S ◁ P & set-S) (T ◁ Q & set-T)) (natTrans mors nat) =
       (mor , mor-eq) , unique
       where
-        -- Distributivity of Π over Σ
-        distrΠΣ : {A : Type ℓ''}{B : A → Type ℓ'''}{C : (a : A) → B a → Type ℓ''''} →
-                  Iso ((a : A) → Σ (B a) (λ b → C a b))
-                      (Σ ((a : A) → B a) (λ f → (a : A) → C a (f a)))
-        fun distrΠΣ f = (λ a → fst (f a)) , λ a → snd (f a)
-        inv distrΠΣ (f , g) a = f a , g a
-        rightInv distrΠΣ _ = refl
-        leftInv distrΠΣ _ = refl
-
         -- Compose heterogenous with homogenous equality
-        compHetHomP : {A : I → Type ℓ'} (x : A i0) (y : A i1) (z : A i1) →
+        compHetHomP : {A : I → Type ℓ'} {x : A i0} {y : A i1} {z : A i1} →
                        PathP (λ i → A i) x y → y ≡ z → PathP (λ i → A i) x z
-        compHetHomP {A} x y z p eq i = subst (λ c → PathP A x c) eq p i
-        
+        compHetHomP {A} {x} {y} {z} p eq i = subst (λ c → PathP A x c) eq p i
+
         nat-trans : (s : S) → FUNCTOR C (SET ℓ') [ C [ P s ,-] , ⟦ T ◁ Q & set-T ⟧-obj ]
-        nat-trans s = natTrans (λ X → curry (mors X) s) nat'
-          where
-            nat' : N-hom-Type (C [ P s ,-]) ⟦ T ◁ Q & set-T ⟧-obj (λ X → curry (mors X) s)
-            nat' {X} {Y} X→Y = funExt (λ Ps→X → funExt⁻ (nat {X} {Y} X→Y) (s , Ps→X))
+        N-ob (nat-trans s) X = curry (mors X) s
+        N-hom (nat-trans s) X→Y i Ps→X = nat X→Y i (s , Ps→X)
 
         apply-yo : (s : S) → cont-func T Q (P s)
-        apply-yo s = (fun (yoneda ⟦ T ◁ Q & set-T ⟧-obj (P s))) (nat-trans s)
+        apply-yo s = yoneda ⟦ T ◁ Q & set-T ⟧-obj (P s) .fun (nat-trans s)
 
-        apply-distrΠΣ : Σ (S → T) (λ f → (s : S) → C [ Q (f s) , P s ])
-        apply-distrΠΣ = (fun distrΠΣ) (apply-yo)
+        apply-Σ-Π-Iso : Σ (S → T) (λ f → (s : S) → C [ Q (f s) , P s ])
+        apply-Σ-Π-Iso = Σ-Π-Iso .fun apply-yo
 
         mor : (S ◁ P & set-S) ⇒c (T ◁ Q & set-T)
-        mor = fst apply-distrΠΣ ◁ snd apply-distrΠΣ
-        
+        mor = fst apply-Σ-Π-Iso ◁ snd apply-Σ-Π-Iso
+
         mor-eq : ⟦ mor ⟧-mor ≡ natTrans mors nat
-        mor-eq = cong₂
-                   natTrans
-                   (funExt (λ X → funExt (λ {(s , f) →
-                     sym (funExt⁻ (nat {P s} {X} f) (s , C .id)) ∙
-                     cong (λ Z → mors X (s , Z)) (C .⋆IdL f)})))
-                   ((isProp→PathP (λ i → isPropImplicitΠ2 (λ X Y → isPropΠ (λ f →
-                     isSetΠ (λ _ → isSetContFunc T Q Y set-T) _ _))) _ _))
-
-        
-        
-        unique : (y : Helpers.fiber (⟦_⟧-mor) (natTrans mors nat)) → (mor , mor-eq) ≡ y
-        unique ((u ◁ f) , m-eq) =
-          ΣPathP
-            (cong₂ _◁_ (funExt (λ s i → fst (N-ob (m-eq (~ i)) (P s) (s , C .id))))
-                       (funExt (λ s i → compHetHomP
-                                         (snd (mors (P s) (s , C .id)))
-                                         (f s ⋆⟨ C ⟩ (C .id))
-                                         (f s)
-                                         (λ j → snd (N-ob (m-eq (~ j)) (P s) (s , C .id)))
-                                         (C .⋆IdR (f s)) i))
-            ,
-            square)
-             where
-               square : Square (λ i → mor-eq i)
-                               (λ i → m-eq i)
-                               (λ i → ⟦_⟧-mor {S ◁ P & set-S} {T ◁ Q & set-T}
-                                              (funExt (λ s j → fst (N-ob (m-eq (~ j)) (P s) (s , C .id))) i ◁
-                                              funExt (λ s j → compHetHomP
-                                                                 (snd (mors (P s) (s , C .id)))
-                                                                 (seq' C (f s) (C .id)) (f s)
-                                                                 (λ k → snd (N-ob (m-eq (~ k)) (P s) (s , C .id)))
-                                                                 (C .⋆IdR (f s)) j) i))
-                               (λ j → natTrans mors nat)
-               square = isSet→SquareP (λ _ _ → isSetNatTrans) _ _ _ _
-               
+        mor-eq = makeNatTransPath
+                   (funExt₂ λ X (s , f) → sym (funExt⁻ (nat f) (s , C .id)) ∙
+                   cong (λ Z → mors X (s , Z)) (C .⋆IdL f))
+
+        unique : (y : fiber (⟦_⟧-mor) (natTrans mors nat)) → (mor , mor-eq) ≡ y
+        unique ((u ◁ f) , m-eq) = Σ≡Prop (λ _ → isSetNatTrans _ _)
+                                         λ i → (λ s → fst (N-ob (m-eq (~ i)) (P s) (s , C .id))) ◁
+                                                λ s → compHetHomP
+                                                       (λ j → snd (N-ob (m-eq (~ j)) (P s) (s , C .id)))
+                                                       (C .⋆IdR (f s)) i
diff --git a/Cubical/Data/Containers/InductiveContainers.agda b/Cubical/Data/Containers/InductiveContainers.agda
index d7911a79e..29a7f8dae 100644
--- a/Cubical/Data/Containers/InductiveContainers.agda
+++ b/Cubical/Data/Containers/InductiveContainers.agda
@@ -5,8 +5,6 @@ by Abbott, Altenkirch, Ghani
 
 -}
 
-{-# OPTIONS --safe #-}
-
 open import Cubical.Data.W.W
 open import Cubical.Data.Containers.Algebras
 open import Cubical.Data.Sigma
@@ -21,52 +19,52 @@ module Cubical.Data.Containers.InductiveContainers
                            (Y : Type)
                            (α : Σ S (λ s → Σ ((i : Ind) → P i s → X i) (λ _ → Q s → Y)) → Y) where
 
-  open Algs Ind S P Q X Y
-         
+  open Algs S Q
+
   into : Σ[ (s , f) ∈ Σ[ s ∈ S ] (Q s → W S Q) ]
            (((i : Ind) → P i s → X i) ×
-           ((i : Ind) (q : Q s) → Pos WAlg i (f q) → X i)) →
-         Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i)  
+           ((i : Ind) (q : Q s) → Pos P WAlg i (f q) → X i)) →
+         Σ[ w ∈ W S Q ] ((i : Ind) → Pos P WAlg i w → X i)
   into ((s , f) , (g , h)) = sup-W s f , λ i → λ {(here p) → g i p ; (below q b) → h i q b}
 
-  α̅' : (w : W S Q) → ((i : Ind) → Pos WAlg i w → X i) → Y
+  α̅' : (w : W S Q) → ((i : Ind) → Pos P WAlg i w → X i) → Y
   α̅' (sup-W s f) k = α (s , g , λ q → α̅' (f q)  (λ i → h i q))
     where
       g : (i : Ind) → P i s → X i
       g i p = k i (here p)
-      
-      h : (i : Ind) → (q : Q s) → Pos WAlg i (f q) → X i
+
+      h : (i : Ind) → (q : Q s) → Pos P WAlg i (f q) → X i
       h i q b = k i (below q b)
 
-  α̅ : Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i) → Y
+  α̅ : Σ[ w ∈ W S Q ] ((i : Ind) → Pos P WAlg i w → X i) → Y
   α̅ (w , k) = α̅' w k
 
-  -- Diagram commutes 
+  -- Diagram commutes
   α̅Comm : (s : S) (f : Q s → W S Q) (g : (i : Ind) → P i s → X i)
-           (h : (i : Ind) (q : Q s) → Pos WAlg i (f q) → X i) →
+           (h : (i : Ind) (q : Q s) → Pos P WAlg i (f q) → X i) →
            α̅ (into ((s , f) , (g , h))) ≡ α (s , g , λ q → α̅ (f q , λ i → h i q))
   α̅Comm s f g h = refl
 
   -- α̅ is unique
-  α̅Unique : (α̃ : Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i) → Y) →
+  α̅Unique : (α̃ : Σ[ w ∈ W S Q ] ((i : Ind) → Pos P WAlg i w → X i) → Y) →
              ((s : S) (f : Q s → W S Q) (g : (i : Ind) → P i s → X i)
-             (h : (i : Ind) (q : Q s) → Pos WAlg i (f q) → X i) →
+             (h : (i : Ind) (q : Q s) → Pos P WAlg i (f q) → X i) →
              α̃ (into ((s , f) , (g , h))) ≡ α (s , g , λ q → α̃ (f q , λ i → h i q))) →
              α̅ ≡ α̃
   α̅Unique α̃ α̃-comm = funExt w-rec
     where
-      lemma : (s : S) (f : Q s → W S Q) (g : (i : Ind) → Pos WAlg i (sup-W s f) → X i) →
+      lemma : (s : S) (f : Q s → W S Q) (g : (i : Ind) → Pos P WAlg i (sup-W s f) → X i) →
               α̃ (into ((s , f) , (λ i p → g i (here p)) , (λ i q b → g i (below q b)))) ≡
               α̃ (sup-W s f , g)
-      lemma s f g = cong₂ (λ w fun → α̃ (w , fun)) refl (funExt λ i → funExt (λ {(here p) → refl ; (below q b) → refl})) 
+      lemma s f g = cong₂ (λ w fun → α̃ (w , fun)) refl (funExt λ i → funExt (λ {(here p) → refl ; (below q b) → refl}))
 
-      w-rec : (x : Σ[ w ∈ W S Q ] ((i : Ind) → Pos WAlg i w → X i)) → α̅ x ≡ α̃ x
+      w-rec : (x : Σ[ w ∈ W S Q ] ((i : Ind) → Pos P WAlg i w → X i)) → α̅ x ≡ α̃ x
       w-rec (w , k) = WInd S Q
-                               (λ w → (k : (i : Ind) → Pos WAlg i w → X i) → α̅ (w , k) ≡ α̃ (w , k))
-                               (λ {s'} {f'} ind k →
-                                 (λ i → α (s' , (λ i p → k i (here p)) ,
-                                        λ q → ind q (λ i pos → k i (below q pos)) i)) ∙
-                                 sym (α̃-comm s' f' (λ i p → k i (here p))
-                                   (λ i q b → k i (below q b))) ∙
-                                 lemma s' f' k)
-                               w k
+                         (λ w → (k : (i : Ind) → Pos P WAlg i w → X i) → α̅ (w , k) ≡ α̃ (w , k))
+                         (λ {s'} {f'} ind k →
+                           (λ i → α (s' , (λ i p → k i (here p)) ,
+                                  λ q → ind q (λ i pos → k i (below q pos)) i)) ∙
+                           sym (α̃-comm s' f' (λ i p → k i (here p))
+                             (λ i q b → k i (below q b))) ∙
+                           lemma s' f' k)
+                         w k
diff --git a/Cubical/Data/W/W.agda b/Cubical/Data/W/W.agda
index c1a5acd20..eff4d9036 100644
--- a/Cubical/Data/W/W.agda
+++ b/Cubical/Data/W/W.agda
@@ -1,13 +1,15 @@
-{-# OPTIONS --safe #-}
+module Cubical.Data.W.W where
 
 open import Cubical.Foundations.Prelude
 
-module Cubical.Data.W.W where
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
 
-data W (S : Type) (P : S → Type) : Type where
+data W (S : Type ℓ) (P : S → Type ℓ') : Type (ℓ-max ℓ ℓ') where
   sup-W : (s : S) → (P s → W S P) → W S P
 
-WInd : (S : Type) (P : S → Type) (M : W S P → Type) →
-        (e : {s : S} {f : P s → W S P} → ((p : P s) → M (f p)) → M (sup-W s f)) →
-        (w : W S P) → M w
-WInd S P M e (sup-W s f) = e {s} {f} (λ p → WInd S P M e (f p))
+WInd : (S : Type ℓ) (P : S → Type ℓ') (M : W S P → Type ℓ'') →
+       (e : {s : S} {f : P s → W S P} → ((p : P s) → M (f p)) → M (sup-W s f)) →
+       (w : W S P) → M w
+WInd S P M e (sup-W s f) = e (λ p → WInd S P M e (f p))

From 312c52d446b7a7e79eb0a47849f20621f1169ac4 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@eduroam-10-200-20-20.local.su.se>
Date: Tue, 25 Jun 2024 15:33:36 +0200
Subject: [PATCH 11/12] Added --safe

---
 Cubical/Codata/Containers/Coalgebras.agda            | 2 +-
 Cubical/Codata/Containers/CoinductiveContainers.agda | 2 +-
 Cubical/Codata/Everything.agda                       | 3 +++
 Cubical/Codata/M/MRecord.agda                        | 2 +-
 Cubical/Data/Containers/Algebras.agda                | 2 ++
 Cubical/Data/W/W.agda                                | 2 ++
 6 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/Cubical/Codata/Containers/Coalgebras.agda b/Cubical/Codata/Containers/Coalgebras.agda
index af71cd796..ecaf72b58 100644
--- a/Cubical/Codata/Containers/Coalgebras.agda
+++ b/Cubical/Codata/Containers/Coalgebras.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --guardedness #-}
+{-# OPTIONS --safe --guardedness #-}
 
 module Cubical.Codata.Containers.Coalgebras where
 
diff --git a/Cubical/Codata/Containers/CoinductiveContainers.agda b/Cubical/Codata/Containers/CoinductiveContainers.agda
index 97221b01e..5e221d43d 100644
--- a/Cubical/Codata/Containers/CoinductiveContainers.agda
+++ b/Cubical/Codata/Containers/CoinductiveContainers.agda
@@ -5,7 +5,7 @@ by Abbott, Altenkirch, Ghani
 
 -}
 
-{-# OPTIONS --guardedness #-}
+{-# OPTIONS --safe --guardedness #-}
 
 open import Cubical.Codata.M.MRecord
 open import Cubical.Data.Sigma
diff --git a/Cubical/Codata/Everything.agda b/Cubical/Codata/Everything.agda
index 163e33549..3ab1d38cc 100644
--- a/Cubical/Codata/Everything.agda
+++ b/Cubical/Codata/Everything.agda
@@ -6,6 +6,9 @@ import Cubical.Codata.Conat.Bounded
 import Cubical.Codata.M.Coalg
 import Cubical.Codata.M.Coalg.Base
 import Cubical.Codata.M.Container
+import Cubical.Codata.Containers.Coalgebras
+import Cubical.Codata.Containers.CoinductiveContainers
+import Cubical.Codata.M.MRecord
 import Cubical.Codata.M.M
 import Cubical.Codata.M.M.Base
 import Cubical.Codata.M.M.Properties
diff --git a/Cubical/Codata/M/MRecord.agda b/Cubical/Codata/M/MRecord.agda
index d55f5027b..48fb15f21 100644
--- a/Cubical/Codata/M/MRecord.agda
+++ b/Cubical/Codata/M/MRecord.agda
@@ -2,7 +2,7 @@
 
 -}
 
-{-# OPTIONS --guardedness #-}
+{-# OPTIONS --safe --guardedness #-}
 
 module Cubical.Codata.M.MRecord where
 
diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda
index db939004e..69ad7060d 100644
--- a/Cubical/Data/Containers/Algebras.agda
+++ b/Cubical/Data/Containers/Algebras.agda
@@ -4,6 +4,8 @@
 
 -}
 
+{-# OPTIONS --safe #-}
+
 module Cubical.Data.Containers.Algebras where
 
 open import Cubical.Data.W.W
diff --git a/Cubical/Data/W/W.agda b/Cubical/Data/W/W.agda
index eff4d9036..ac9c84db7 100644
--- a/Cubical/Data/W/W.agda
+++ b/Cubical/Data/W/W.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --safe #-}
+
 module Cubical.Data.W.W where
 
 open import Cubical.Foundations.Prelude

From 99be07304b88d06034739c811d14d3ef803b1cf8 Mon Sep 17 00:00:00 2001
From: Stefania Damato <stefania@eduroam-10-200-20-20.local.su.se>
Date: Tue, 25 Jun 2024 15:39:13 +0200
Subject: [PATCH 12/12] More --safe flags

---
 Cubical/Data/Containers/Base.agda                     | 2 ++
 Cubical/Data/Containers/ContainerExtensionProofs.agda | 2 ++
 Cubical/Data/Containers/InductiveContainers.agda      | 2 ++
 3 files changed, 6 insertions(+)

diff --git a/Cubical/Data/Containers/Base.agda b/Cubical/Data/Containers/Base.agda
index 717f5a945..0f79e4a38 100644
--- a/Cubical/Data/Containers/Base.agda
+++ b/Cubical/Data/Containers/Base.agda
@@ -10,6 +10,8 @@
 
 -}
 
+{-# OPTIONS --safe #-}
+
 module Cubical.Data.Containers.Base where
 
 open import Cubical.Categories.Category.Base
diff --git a/Cubical/Data/Containers/ContainerExtensionProofs.agda b/Cubical/Data/Containers/ContainerExtensionProofs.agda
index ffde6a754..4445bd85e 100644
--- a/Cubical/Data/Containers/ContainerExtensionProofs.agda
+++ b/Cubical/Data/Containers/ContainerExtensionProofs.agda
@@ -8,6 +8,8 @@
 
 -}
 
+{-# OPTIONS --safe #-}
+
 module Cubical.Data.Containers.ContainerExtensionProofs where
 
 open import Cubical.Foundations.Prelude hiding (_◁_)
diff --git a/Cubical/Data/Containers/InductiveContainers.agda b/Cubical/Data/Containers/InductiveContainers.agda
index 29a7f8dae..a744636b0 100644
--- a/Cubical/Data/Containers/InductiveContainers.agda
+++ b/Cubical/Data/Containers/InductiveContainers.agda
@@ -5,6 +5,8 @@ by Abbott, Altenkirch, Ghani
 
 -}
 
+{-# OPTIONS --safe #-}
+
 open import Cubical.Data.W.W
 open import Cubical.Data.Containers.Algebras
 open import Cubical.Data.Sigma