Added construction of M-types from Signatures/Containers (#245)

* Added construction of M-types from Signatures/Containers * Added files * No longer 'Unresolved Metas', but some postulates * Removed trailing whitespace * Fixed name collision * Making progress on postulates * Making progress on postulates * removed whitespace * Trying to fix computation problems * Reduced shift definition, to pure iso's * Fixed naming collsion (again...) * Fixed naming collision (again...) * Updated files to use iso more, and made proofs more readable * Update * Removed whitespace * Update * Small step towards removing all postulates. * Update * Finished proving lemma11-Iso * All postulates cleared in M-types * Pushed abstract * Uncomment * Working but with some 'abstract' * Pushed abstract * Updated to newest version of Cubical Agda * Renamed some theorems * Renamed some theorems * Getting closer to removing all postulates * Clared the last postulate for construction of M-types * Updated folder structure * Updated infrastructure * Moved proofs * Added missing files * Working on pull request comments * Working on pull request comments * Working on pull request comments * Restructure * Restructure * Restructure * Updates based on PR comments * Working on comments on PR * Trying to simplify definition of shift * Simplifying shift definition * Working on PR comments * Working on PR comments * Working on PR comments * Working on PR comments * Working on PR comments * Rename M-type to M, and moved files
agda · May 7, 2020 · c67854d · c67854d
1 parent 658f92a
commit c67854d
Show file tree

Hide file tree

Showing 21 changed files with 836 additions and 24 deletions.
diff --git a/Cubical/Codata/Everything.agda b/Cubical/Codata/Everything.agda
@@ -13,6 +13,19 @@ open import Cubical.Codata.Conat public
 
 open import Cubical.Codata.M public
 
-
 -- Also uses {-# TERMINATING #-}.
 open import Cubical.Codata.M.Bisimilarity public
+
+{-
+-- Alternative M type implemetation, based on
+-- https://arxiv.org/pdf/1504.02949.pdf
+-- "Non-wellfounded trees in Homotopy Type Theory"
+-- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
+-}
+
+open import Cubical.Codata.M.AsLimit.M
+open import Cubical.Codata.M.AsLimit.Coalg
+open import Cubical.Codata.M.AsLimit.helper
+open import Cubical.Codata.M.AsLimit.Container
+open import Cubical.Codata.M.AsLimit.itree
+open import Cubical.Codata.M.AsLimit.stream
diff --git a/Cubical/Codata/M.agda b/Cubical/Codata/M.agda
@@ -32,27 +32,30 @@ module Helpers where
 
 open Helpers
 
-IxCont : Type₀ → Type₁
-IxCont X = Σ (X → Type₀) \ S → ∀ x → S x → X → Type₀
+IxCont : ∀ {ℓ} -> Type ℓ → Type (ℓ-suc ℓ)
+IxCont {ℓ} X = Σ (X → Type ℓ) λ S → ∀ x → S x → X → Type ℓ
 
 
-⟦_⟧ : ∀ {X : Type₀} → IxCont X → (X → Type₀) → (X → Type₀)
-⟦ (S , P) ⟧ X x = Σ (S x) \ s → ∀ y → P x s y → X y
+⟦_⟧ : ∀ {ℓ} {X : Type ℓ} → IxCont X → (X → Type ℓ) → (X → Type ℓ)
+⟦ (S , P) ⟧ X x = Σ (S x) λ s → ∀ y → P x s y → X y
 
 
-record M {X : Type₀} (C : IxCont X) (x : X) : Type₀ where
+record M {ℓ} {X : Type ℓ} (C : IxCont X) (x : X) : Type ℓ where -- Type₀
   coinductive
   field
     head : C .fst x
     tails : ∀ y → C .snd x head y → M C y
 
 open M public
 
-module _ {X : Type₀} {C : IxCont X} where
+module _ {ℓ} {X : Type ℓ} {C : IxCont X} where
 
   private
     F = ⟦ C ⟧
 
+  inM : ∀ x → F (M C) x → M C x
+  inM x (head , tail) = record { head = head ; tails = tail }
+
   out : ∀ x → M C x → F (M C) x
   out x a = (a .head) , (a .tails)
 

diff --git a/Cubical/Codata/M/AsLimit/Coalg.agda b/Cubical/Codata/M/AsLimit/Coalg.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --cubical --guardedness --safe #-}
+
+module Cubical.Codata.M.AsLimit.Coalg where
+
+open import Cubical.Codata.M.AsLimit.Coalg.Base public
diff --git a/Cubical/Codata/M/AsLimit/Coalg/Base.agda b/Cubical/Codata/M/AsLimit/Coalg/Base.agda
@@ -0,0 +1,39 @@
+{-# OPTIONS --cubical --guardedness --safe #-}
+
+module Cubical.Codata.M.AsLimit.Coalg.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function using ( _∘_ )
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.GroupoidLaws
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Nat
+open import Cubical.Data.Prod
+open import Cubical.Data.Sigma
+
+open import Cubical.Codata.M.AsLimit.Container
+open import Cubical.Codata.M.AsLimit.helper
+
+-------------------------------
+-- Definition of a Coalgebra --
+-------------------------------
+
+Coalg₀ : ∀ {ℓ} {S : Container ℓ} -> Type (ℓ-suc ℓ)
+Coalg₀ {ℓ} {S = S} = Σ[ C ∈ Type ℓ ] (C → P₀ S C)
+
+--------------------------
+-- Definition of a Cone --
+--------------------------
+
+Cone₀ : ∀ {ℓ} {S : Container ℓ} {C,γ : Coalg₀ {S = S}} -> Type ℓ
+Cone₀ {S = S} {C , _} = (n : ℕ) → C → X (sequence S) n
+
+Cone₁ : ∀ {ℓ} {S : Container ℓ} {C,γ : Coalg₀ {S = S}} -> (f : Cone₀ {C,γ = C,γ}) -> Type ℓ
+Cone₁ {S = S} {C , _} f = (n : ℕ) → π (sequence S) ∘ (f (suc n)) ≡ f n
+
+Cone : ∀ {ℓ} {S : Container ℓ} (C,γ : Coalg₀ {S = S}) -> Type ℓ
+Cone {S = S} C,γ = Σ[ Cone ∈ (Cone₀ {C,γ = C,γ}) ] (Cone₁{C,γ = C,γ} Cone)
diff --git a/Cubical/Codata/M/AsLimit/Container.agda b/Cubical/Codata/M/AsLimit/Container.agda
@@ -0,0 +1,88 @@
+{-# OPTIONS --cubical --guardedness --safe #-}
+
+module Cubical.Codata.M.AsLimit.Container where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv using (_≃_)
+open import Cubical.Foundations.Function using (_∘_)
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Prod
+open import Cubical.Data.Nat as ℕ using (ℕ ; suc ; _+_ )
+
+open import Cubical.Foundations.Transport
+
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+
+open import Cubical.Data.Sum
+
+open import Cubical.Foundations.Structure
+
+open import Cubical.Codata.M.AsLimit.helper
+
+-------------------------------------
+-- Container and Container Functor --
+-------------------------------------
+
+-- Σ[ A ∈ (Type ℓ) ] (A → Type ℓ)
+Container : ∀ ℓ -> Type (ℓ-suc ℓ)
+Container ℓ = TypeWithStr ℓ (λ x → x → Type ℓ)
+
+-- Polynomial functor (P₀ , P₁)  defined over a container
+-- https://ncatlab.org/nlab/show/polynomial+functor
+
+-- P₀ object part of functor
+P₀ : ∀ {ℓ} (S : Container ℓ) -> Type ℓ -> Type ℓ
+P₀ (A , B) X  = Σ[ a ∈ A ] (B a -> X)
+
+-- P₁ morphism part of functor
+P₁ : ∀ {ℓ} {S : Container ℓ} {X Y} (f : X -> Y) -> P₀ S X -> P₀ S Y
+P₁ {S = S} f = λ { (a , g) ->  a , f ∘ g }
+
+-----------------------
+-- Chains and Limits --
+-----------------------
+
+record Chain ℓ : Type (ℓ-suc ℓ) where
+  constructor _,,_
+  field
+    X : ℕ -> Type ℓ
+    π : {n : ℕ} -> X (suc n) -> X n
+
+open Chain public
+
+limit-of-chain : ∀ {ℓ} -> Chain ℓ → Type ℓ
+limit-of-chain (x ,, pi) = Σ[ x ∈ ((n : ℕ) → x n) ] ((n : ℕ) → pi {n = n} (x (suc n)) ≡ x n)
+
+shift-chain : ∀ {ℓ} -> Chain ℓ -> Chain ℓ
+shift-chain = λ X,π -> ((λ x → X X,π (suc x)) ,, λ {n} → π X,π {suc n})
+
+------------------------------------------------------
+-- Limit type of a Container , and Shift of a Limit --
+------------------------------------------------------
+
+Wₙ : ∀ {ℓ} -> Container ℓ -> ℕ -> Type ℓ
+Wₙ S 0 = Lift Unit
+Wₙ S (suc n) = P₀ S (Wₙ S n)
+
+πₙ : ∀ {ℓ} -> (S : Container ℓ) -> {n : ℕ} -> Wₙ S (suc n) -> Wₙ S n
+πₙ {ℓ} S {0} _ = lift tt
+πₙ S {suc n} = P₁ (πₙ S {n})
+
+sequence : ∀ {ℓ} -> Container ℓ -> Chain ℓ
+X (sequence S) n = Wₙ S n
+π (sequence S) {n} = πₙ S {n}
+
+PX,Pπ : ∀ {ℓ} (S : Container ℓ) -> Chain ℓ
+PX,Pπ {ℓ} S =
+  (λ n → P₀ S (X (sequence S) n)) ,,
+  (λ {n : ℕ} x → P₁ (λ z → z) (π (sequence S) {n = suc n} x ))
+
+-----------------------------------
+-- M type is limit of a sequence --
+-----------------------------------
+
+M : ∀ {ℓ} -> Container ℓ → Type ℓ
+M = limit-of-chain ∘ sequence
diff --git a/Cubical/Codata/M/AsLimit/M.agda b/Cubical/Codata/M/AsLimit/M.agda
@@ -0,0 +1,6 @@
+{-# OPTIONS --cubical --guardedness --safe #-}
+
+module Cubical.Codata.M.AsLimit.M where
+
+open import Cubical.Codata.M.AsLimit.M.Base public
+open import Cubical.Codata.M.AsLimit.M.Properties public
diff --git a/Cubical/Codata/M/AsLimit/M/Base.agda b/Cubical/Codata/M/AsLimit/M/Base.agda
@@ -0,0 +1,195 @@
+{-# OPTIONS --cubical --guardedness --safe #-}
+
+-- Construction of M-types from
+-- https://arxiv.org/pdf/1504.02949.pdf
+-- "Non-wellfounded trees in Homotopy Type Theory"
+-- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
+
+module Cubical.Codata.M.AsLimit.M.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv using (_≃_)
+open import Cubical.Foundations.Function using (_∘_)
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Prod
+open import Cubical.Data.Nat as ℕ using (ℕ ; suc ; _+_ )
+open import Cubical.Data.Sigma hiding (_×_)
+open import Cubical.Data.Nat.Algebra
+
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.GroupoidLaws
+
+open import Cubical.Data.Sum
+
+open import Cubical.Codata.M.AsLimit.helper
+open import Cubical.Codata.M.AsLimit.Container
+
+open import Cubical.Codata.M.AsLimit.Coalg.Base
+
+open Iso
+
+private
+  limit-collapse : ∀ {ℓ} {S : Container ℓ} (X : ℕ → Type ℓ) (l : (n : ℕ) → X n → X (suc n)) → (x₀ : X 0) → ∀ (n : ℕ) → X n
+  limit-collapse X l x₀ 0 = x₀
+  limit-collapse {S = S} X l x₀ (suc n) = l n (limit-collapse {S = S} X l x₀ n)
+
+lemma11-Iso :
+  ∀ {ℓ} {S : Container ℓ} (X : ℕ → Type ℓ) (l : (n : ℕ) → X n → X (suc n))
+  → Iso (Σ[ x ∈ ((n : ℕ) → X n)] ((n : ℕ) → x (suc n) ≡ l n (x n)))
+         (X 0)
+fun (lemma11-Iso X l) (x , y) = x 0
+inv (lemma11-Iso {S = S} X l) x₀ = limit-collapse {S = S} X l x₀ , (λ n → refl {x = limit-collapse {S = S} X l x₀ (suc n)})
+rightInv (lemma11-Iso X l) _ = refl
+leftInv (lemma11-Iso {ℓ = ℓ} {S = S} X l) (x , y) i =
+  let temp = χ-prop (x 0) (fst (inv (lemma11-Iso {S = S} X l) (fun (lemma11-Iso {S = S} X l) (x , y))) , refl , (λ n → refl {x = limit-collapse {S = S} X l (x 0) (suc n)})) (x , refl , y)
+  in temp i .fst , proj₂ (temp i .snd)
+  where
+    open AlgebraPropositionality
+    open NatSection
+
+    X-fiber-over-ℕ : (x₀ : X 0) -> NatFiber NatAlgebraℕ ℓ
+    X-fiber-over-ℕ x₀ = record { Fiber = X ; fib-zero = x₀ ; fib-suc = λ {n : ℕ} xₙ → l n xₙ }
+
+    X-section : (x₀ : X 0) → (z : Σ[ x ∈ ((n : ℕ) → X n)] (x 0 ≡ x₀) × (∀ n → (x (suc n)) ≡ l n (x n))) -> NatSection (X-fiber-over-ℕ x₀)
+    X-section = λ x₀ z → record { section = fst z ; sec-comm-zero = proj₁ (snd z) ; sec-comm-suc = proj₂ (snd z) }
+
+    Z-is-Section : (x₀ : X 0) →
+      Iso (Σ[ x ∈ ((n : ℕ) → X n)] (x 0 ≡ x₀) × (∀ n → (x (suc n)) ≡ l n (x n)))
+          (NatSection (X-fiber-over-ℕ x₀))
+    fun (Z-is-Section x₀) (x , (z , y)) = record { section = x ; sec-comm-zero = z ; sec-comm-suc = y }
+    inv (Z-is-Section x₀) x = NatSection.section x , (sec-comm-zero x , sec-comm-suc x)
+    rightInv (Z-is-Section x₀) _ = refl
+    leftInv (Z-is-Section x₀) (x , (z , y)) = refl
+
+    -- S≡T
+    χ-prop' : (x₀ : X 0) → isProp (NatSection (X-fiber-over-ℕ x₀))
+    χ-prop' x₀ a b = SectionProp.S≡T isNatInductiveℕ (X-section x₀ (inv (Z-is-Section x₀) a)) (X-section x₀ (inv (Z-is-Section x₀) b))
+
+    χ-prop : (x₀ : X 0) → isProp (Σ[ x ∈ ((n : ℕ) → X n) ] (x 0 ≡ x₀) × (∀ n → (x (suc n)) ≡ l n (x n)))
+    χ-prop x₀ = subst isProp (sym (isoToPath (Z-is-Section x₀))) (χ-prop' x₀)
+
+-----------------------------------------------------
+-- Shifting the limit of a chain is an equivalence --
+-----------------------------------------------------
+
+-- Shift is equivalence (12) and (13) in the proof of Theorem 7
+-- https://arxiv.org/pdf/1504.02949.pdf
+-- "Non-wellfounded trees in Homotopy Type Theory"
+-- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
+
+-- TODO: This definition is inefficient, it should be updated to use some cubical features!
+shift-iso : ∀ {ℓ} (S : Container ℓ) -> Iso (P₀ S (M S)) (M S)
+shift-iso S@(A , B) =
+  P₀ S (M S)
+    Iso⟨ Σ-ap-iso₂ (λ x → iso (λ f → (λ n z → f z .fst n) , λ n i a → f a .snd n i)
+                               (λ (u , q) z → (λ n → u n z) , λ n i → q n i z)
+                              (λ _ → refl)
+                              (λ _ → refl)) ⟩
+  (Σ[ a ∈ A ] (Σ[ u ∈ ((n : ℕ) → B a → X (sequence S) n) ] ((n : ℕ) → π (sequence S) ∘ (u (suc n)) ≡ u n)))
+    Iso⟨ invIso α-iso-step-5-Iso ⟩
+  (Σ[ a ∈ (Σ[ a ∈ ((n : ℕ) → A) ] ((n : ℕ) → a (suc n) ≡ a n)) ]
+        Σ[ u ∈ ((n : ℕ) → B (a .fst n) → X (sequence S) n) ]
+           ((n : ℕ) → PathP (λ x → B (a .snd n x) → X (sequence S) n)
+                               (π (sequence S) ∘ u (suc n))
+                               (u n)))
+    Iso⟨ α-iso-step-1-4-Iso-lem-12 ⟩
+  M S ∎Iso
+    where
+      α-iso-step-5-Iso-helper0 :
+        ∀ (a : (ℕ -> A))
+        → (p : (n : ℕ) → a (suc n) ≡ a n)
+        → (n : ℕ)
+        → a n ≡ a 0
+      α-iso-step-5-Iso-helper0 a p 0 = refl
+      α-iso-step-5-Iso-helper0 a p (suc n) = p n ∙ α-iso-step-5-Iso-helper0 a p n
+
+      α-iso-step-5-Iso-helper1-Iso :
+        ∀ (a : ℕ -> A)
+        → (p : (n : ℕ) → a (suc n) ≡ a n)
+        → (u : (n : ℕ) → B (a n) → Wₙ S n)
+        → (n : ℕ)
+        → Iso
+            (PathP (λ x → B (p n x) → Wₙ S n) (πₙ S ∘ u (suc n)) (u n))
+            (πₙ S ∘ (subst (\k -> B k → Wₙ S (suc n)) (α-iso-step-5-Iso-helper0 a p (suc n))) (u (suc n)) ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n))
+      α-iso-step-5-Iso-helper1-Iso  a p u n  =
+        PathP (λ x → B (p n x) → Wₙ S n) (πₙ S ∘ u (suc n)) (u n)
+          Iso⟨ pathToIso (PathP≡Path (λ x → B (p n x) → Wₙ S n) (πₙ S ∘ u (suc n)) (u n)) ⟩
+        subst (λ k → B k → Wₙ S n) (p n) (πₙ S ∘ u (suc n)) ≡ (u n)
+          Iso⟨ (invIso (temp (pathToIso (cong (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n))))) ⟩
+        (subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (subst (λ k → B k → Wₙ S n) (p n) (πₙ S ∘ u (suc n)))
+               ≡
+        subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n))
+          Iso⟨ pathToIso (λ i → (sym (substComposite (λ k → B k → Wₙ S n) (p n) (α-iso-step-5-Iso-helper0 a p n) (πₙ S ∘ u (suc n)))) i
+                            ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n)) ⟩
+        subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p (suc n)) (πₙ S ∘ u (suc n))
+          ≡
+        subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n)
+          Iso⟨ pathToIso (λ i → (substCommSlice (λ k → B k → Wₙ S (suc n)) (λ k → B k → Wₙ S n) (λ a x x₁ → (πₙ S) (x x₁)) ((α-iso-step-5-Iso-helper0 a p) (suc n)) (u (suc n))) i
+                         ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n)) ⟩
+        πₙ S ∘ subst (λ k → B k → Wₙ S (suc n)) (α-iso-step-5-Iso-helper0 a p (suc n)) (u (suc n))
+          ≡
+        subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n) ∎Iso
+        where
+          abstract
+            temp = iso→fun-Injection-Iso-x
+
+      α-iso-step-5-Iso :
+        Iso
+          (Σ[ a ∈ (Σ[ a ∈ ((n : ℕ) → A) ] ((n : ℕ) → a (suc n) ≡ a n)) ]
+            Σ[ u ∈ ((n : ℕ) → B (a .fst n) → X (sequence S) n) ]
+              ((n : ℕ) → PathP (λ x → B (a .snd n x) → X (sequence S) n)
+                                  (π (sequence S) ∘ u (suc n))
+                                  (u n)))
+            (Σ[ a ∈ A ] (Σ[ u ∈ ((n : ℕ) → B a → X (sequence S) n) ] ((n : ℕ) → π (sequence S) ∘ (u (suc n)) ≡ u n)))
+      α-iso-step-5-Iso =
+        Σ-ap-iso (lemma11-Iso {S = S} (λ _ → A) (λ _ x → x)) (λ a,p →
+          Σ-ap-iso (pathToIso (cong (λ k → (n : ℕ) → k n) (funExt λ n → cong (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 (a,p .fst) (a,p .snd) n)))) λ u →
+                              pathToIso (cong (λ k → (n : ℕ) → k n) (funExt λ n → isoToPath (α-iso-step-5-Iso-helper1-Iso (a,p .fst) (a,p .snd) u n))))
+
+      α-iso-step-1-4-Iso-lem-12 :
+        Iso (Σ[ a ∈ (Σ[ a ∈ ((n : ℕ) → A)] ((n : ℕ) → a (suc n) ≡ a n)) ]
+                  (Σ[ u ∈ ((n : ℕ) → B (a .fst n) → X (sequence S) n) ]
+                      ((n : ℕ) → PathP (λ x → B (a .snd n x) → X (sequence S) n)
+                                          (π (sequence S) ∘ u (suc n))
+                                          (u n))))
+            (limit-of-chain (sequence S))
+      fun α-iso-step-1-4-Iso-lem-12 (a , b) = (λ { 0 → lift tt ; (suc n) → (a .fst n) , (b .fst n)}) , λ { 0 → refl {x = lift tt} ; (suc m) i → a .snd m i , b .snd m i }
+      inv α-iso-step-1-4-Iso-lem-12 x = ((λ n → (x .fst) (suc n) .fst) , λ n i → (x .snd) (suc n) i .fst) , (λ n → (x .fst) (suc n) .snd) , λ n i → (x .snd) (suc n) i .snd
+      fst (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) 0 = lift tt
+      fst (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) (suc n) = refl i
+      snd (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) 0 = refl
+      snd (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) (suc n) = c (suc n)
+      leftInv α-iso-step-1-4-Iso-lem-12 (a , b) = refl
+
+shift : ∀ {ℓ} (S : Container ℓ) -> P₀ S (M S) ≡ M S
+shift S = isoToPath (shift-iso S) -- lemma 13 & lemma 12
+
+-- Transporting along shift
+
+in-fun : ∀ {ℓ} {S : Container ℓ} -> P₀ S (M S) -> M S
+in-fun {S = S} = fun (shift-iso S)
+
+out-fun : ∀ {ℓ} {S : Container ℓ} -> M S -> P₀ S (M S)
+out-fun {S = S} = inv (shift-iso S)
+
+-- Property of functions into M-types
+
+lift-to-M : ∀ {ℓ} {A : Type ℓ} {S : Container ℓ}
+  → (x : (n : ℕ) -> A → X (sequence S) n)
+  → ((n : ℕ) → (a : A) →  π (sequence S) (x (suc n) a) ≡ x n a)
+  ---------------
+  → (A → M S)
+lift-to-M x p a = (λ n → x n a) , λ n i → p n a i
+
+lift-direct-M : ∀ {ℓ} {S : Container ℓ}
+  → (x : (n : ℕ) → X (sequence S) n)
+  → ((n : ℕ) →  π (sequence S) (x (suc n)) ≡ x n)
+  ---------------
+  → M S
+lift-direct-M x p = x , p