Containers (and W and M)

Cubical/Codata/Containers/Coalgebras.agda

@@ -0,0 +1,28 @@
+{-# OPTIONS --safe --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

Cubical/Codata/Containers/CoinductiveContainers.agda

@@ -0,0 +1,199 @@
+{- Proof that containers are closed under greatest fixed points
+
+Adapted from 'Containers: Constructing strictly positive types'
+by Abbott, Altenkirch, Ghani
+
+-}
+
+{-# OPTIONS --safe --guardedness #-}
+
+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.Codata.Containers.Coalgebras
+open import Cubical.Data.Containers.Algebras
+open M
+open M-R
+
+module Cubical.Codata.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 S Q
+    open Coalgs S Q
+
+    β̅₁ : Y → M S Q
+    shape (β̅₁ y) = βs y
+    pos (β̅₁ y) = β̅₁ ∘ βh y
+
+    β̅₂ : (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 P MAlg i m → X i)
+    β̅ y = β̅₁ y , β̅₂ y
+
+    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 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 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
+
+      -- 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 P 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 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
+        R-intro : (y : Y) → R (β̃₁ y) (β̅₁ y)
+
+      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₁))
+
+      fstEq : (y : Y) → β̃₁ y ≡ β̅₁ y
+      fstEq y = MCoind {S} {Q} R isBisimR (R-intro y)
+        where
+          -- Coinduction principle for M
+          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)
+
+                    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 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))
+                   (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 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 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 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))
+            (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 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 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)
+                                   (β̅₁ ∘ β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 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
+                {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 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)) →
+                         (β̅₂ y) ≡ (β̃₂ y))
+                (λ _ → refl)
+                λ comm3 comm4 → funExt (λ ind → funExt (sndEqAux β̃₂ comm3 comm4 y ind)))
+              comm1
+        where
+          -- 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 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 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 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

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

Cubical/Codata/M/MRecord.agda

@@ -0,0 +1,35 @@
+{- Alternative definition of M as a record type, together with some of its properties
+
+-}
+
+{-# OPTIONS --safe --guardedness #-}
+
+module Cubical.Codata.M.MRecord where
+
+open import Cubical.Foundations.Prelude
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+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
+
+-- 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

Cubical/Data/Containers/Algebras.agda

@@ -0,0 +1,47 @@
+{- Basic definitions required for co/inductive container proofs
+
+- Definition of Pos
+
+-}
+
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Containers.Algebras where
+
+open import Cubical.Data.W.W
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+
+private
+  variable
+    ℓ ℓ' ℓ'' ℓ''' : Level
+
+module Algs (S : Type ℓ)
+            (Q : S → Type ℓ') where
+
+  open Iso
+
+  -- Fixed point algebras
+  record ContFuncIso : Type (ℓ-max (ℓ-suc ℓ'') (ℓ-max ℓ ℓ')) where
+    constructor iso
+    field
+      carrier : Type ℓ''
+      χ : Iso (Σ[ s ∈ S ] (Q s → carrier)) carrier
+
+  open ContFuncIso
+
+  WAlg : ContFuncIso
+  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
+
+  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 P FP i (snd (FP .χ .inv wm) q) → Pos P FP i wm