From 1535baed6a74c2651bd182ed766063013bd963b8 Mon Sep 17 00:00:00 2001 From: aljungstrom Date: Fri, 12 Jul 2024 14:25:47 +0200 Subject: [PATCH 1/3] done --- .../Containers/CoinductiveContainers.agda | 418 ++++++++++-------- Cubical/Codata/M/MRecord.agda | 20 + Cubical/Data/Containers/Algebras.agda | 83 +++- 3 files changed, 339 insertions(+), 182 deletions(-) diff --git a/Cubical/Codata/Containers/CoinductiveContainers.agda b/Cubical/Codata/Containers/CoinductiveContainers.agda index 5e221d43d..c4130b966 100644 --- a/Cubical/Codata/Containers/CoinductiveContainers.agda +++ b/Cubical/Codata/Containers/CoinductiveContainers.agda @@ -7,193 +7,257 @@ by Abbott, Altenkirch, Ghani {-# OPTIONS --safe --guardedness #-} +module Cubical.Codata.Containers.CoinductiveContainers where + open import Cubical.Codata.M.MRecord -open import Cubical.Data.Sigma +open import Cubical.Codata.Containers.Coalgebras + open import Cubical.Foundations.HLevels open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Transport -open import Cubical.Codata.Containers.Coalgebras +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma 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 +module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} + (Ind : Type ℓInd) + (S : Type ℓS) + (P : Ind → S → Type ℓP) + (Q : S → Type ℓQ) + (X : Ind → Type ℓX) + (Y : Type ℓY) where + open Algs S Q + open Coalgs S Q + + open ContFuncIso + open Iso - open Algs S Q - open Coalgs S Q + -- Construction of a generic + -- β : Y → Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i) + module β1 (βs : Y → S) + (βh : (y : Y) → Q (βs y) → Y) where β̅₁ : 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 + pos (β̅₁ y) t = β̅₁ (βh y t) + + module β2 (βg : (y : Y) → (i : Ind) → P i (βs y) → X i) where + β̅₂ : (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 + + -- Characterisation of the equality type of the first projection of + -- such a β + module makeFirstEq + (β̃₁ : Y → M S Q) + (β̃₂ : (y : Y) (ind : Ind) → Pos P MAlg ind (β̃₁ y) → X ind) + (βs : Y → S) + (comm1 : shape ∘ β̃₁ ≡ βs) + (βh : (y : Y) → Q (βs y) → Y) + (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M S Q) + (pos (β̃₁ y)) (λ q → β̃₁ (βh y q))) + where + open β1 + + data R : M S Q → M S Q → Type (ℓ-max ℓS (ℓ-max ℓY ℓQ)) where + R-intro : (y : Y) → R (β̃₁ y) (β̅₁ βs βh y) + + isBisimR : {m₀ : M S Q} {m₁ : M S Q} → R m₀ m₁ → M-R R m₀ m₁ + s-eq (isBisimR (R-intro y)) i = comm1 i y + p-eq (isBisimR (R-intro y)) q₀ q₁ q-eq = + transport (λ i → R (comm2 y (~ i) (q-eq (~ i))) + (β̅₁ βs βh (βh y q₁))) + (R-intro (βh y q₁)) + + -- first main result + pre-fst-eq : (y : Y) → β̃₁ y ≡ β̅₁ βs βh y + pre-fst-eq y = MCoind R isBisimR (R-intro y) + + -- Because pre-fst-eq is defined using MCoind, its proof term for + -- in the pos case is rather complicated. It _should_ look like this: + pre-fst-eq-pos : (y : Y) + → PathP (λ i → Q (shape (pre-fst-eq y i)) → M S Q) + (pos (β̃₁ y)) (λ t → β̅₁ βs βh (βh y t)) + pre-fst-eq-pos y i q = + hcomp (λ j → λ { (i = i0) → pos (β̃₁ y) q ; + (i = i1) → pre-fst-eq (βh y q) j }) + (comm2 y i q) + -- but this definition is not accepted by the termination checker... + + + -- Fortunately, we can prove that (cong pos ∘ pre-fst-eq) and + -- pre-fst-eq-pos are equal up to a path (by J and some technical + -- transport juggling). + pre-fst-eq-id : (β̃₁ : Y → M S Q) + (β̃₂ : (y : Y) (ind : Ind) → Pos P MAlg ind (β̃₁ y) → X ind) + (βs : Y → S) + (comm1 : shape ∘ β̃₁ ≡ βs) + (βh : (y : Y) → Q (βs y) → Y) + (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M S Q) + (pos (β̃₁ y)) (λ q → β̃₁ (βh y q))) + (y : _) + → cong pos (makeFirstEq.pre-fst-eq β̃₁ β̃₂ βs comm1 βh comm2 y) + ≡ makeFirstEq.pre-fst-eq-pos β̃₁ β̃₂ βs comm1 βh comm2 y + pre-fst-eq-id β̃₁ β̃₂ = + J> λ βh comm2 y + → (λ j i q → MCoind (R βh comm2) + (isBisimR βh comm2) + {m₀ = pos (β̃₁ y) (transportRefl q (~ i ∨ j))} + {m₁ = pos (β̅₁ ((λ r → shape r) ∘ β̃₁) βh y) (transportRefl q (i ∨ j))} + ((p-eq (isBisimR βh comm2 (R-intro y)) + (transportRefl q (~ i ∨ j)) (transportRefl q (i ∨ j)) + λ k → transp (λ _ → Q (shape (β̃₁ y))) + (((~ k ∧ (~ i)) ∨ (k ∧ i)) ∨ j) q)) i) + ∙ cong funExt (funExt λ q + → lUnit _ + ∙ (λ j → (λ s → comm2 y (j ∧ s) q) + ∙ MCoind {S = S} {Q = Q} (R βh comm2 ) + (isBisimR βh comm2) + {m₀ = comm2 y j q} + {m₁ = pos (β̅₁ ((λ r → shape r) ∘ β̃₁) βh y) q} + (transp (λ i → R βh comm2 (comm2 y (~ i ∨ j) q) + (β̅₁ ((λ r → shape r) ∘ β̃₁) βh (βh y q))) + j + (R-intro (βh y q))))) + where + open β1 + open makeFirstEq β̃₁ β̃₂ _ refl + + -- main part of the proof + module _ + (βs : Y → S) + (βh : (y : Y) → Q (βs y) → Y) + (βg : (y : Y) → (i : Ind) → P i (βs y) → X i) + (β̃ : Y → Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i)) + (βh : (y : Y) → Q (βs y) → Y) + (comm1 : (y : _) → shape (fst (β̃ y)) ≡ βs y) + (comm2 : (y : Y) → + PathP (λ i → Q (comm1 y i) → M S Q) + (pos (fst (β̃ y))) (λ q → fst (β̃ (βh y q)))) + (comm3 : (y : Y) → PathP (λ i → (ind : Ind) → P ind (comm1 y i) → X ind) + (λ ind p → snd (β̃ y) ind (here p)) + (βg y)) + (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 → snd (β̃ y) ind (below q b)) + (λ ind q b → snd (β̃ (βh y q)) ind b)) + where + private + β̃₁ = fst ∘ β̃ + β̃₂ = snd ∘ β̃ + + open β1 βs βh + open β2 βg + open makeFirstEq β̃₁ β̃₂ βs (funExt comm1) βh comm2 + + fst-eq : (y : Y) → β̃₁ y ≡ β̅₁ y + fst-eq = pre-fst-eq + + snd-eq : (y : Y) + → PathP (λ i → (ind : Ind) → Pos P MAlg ind (fst-eq y i) → X ind) + (β̃₂ y) (β̅₂ y) + snd-eq y = funExt λ ind + → toPathP (funExt λ x → transportRefl _ + ∙ mainlem ind x) + where + module _ (ind : Ind) where + mainlem-here : (t : Y) (x : P ind _) + → β̃₂ t ind (subst (Pos P MAlg ind) (sym (fst-eq t)) (here x)) + ≡ β̅₂ t ind (here x) + mainlem-here y x = + cong (β̃₂ y ind) + (transportPresHere ind _ (sym (fst-eq y)) _) + ∙ funExtDep⁻ (funExt⁻ (comm3 y) ind) + λ j → (transp (λ i → P ind (comm1 y (~ i ∨ j))) j x) + + mainlem-below : (t : Y) (q : Q (βs t)) + (e : Pos P MAlg ind (β̅₁ (βh t q))) + → β̃₂ (βh t q) ind + (subst (Pos P MAlg ind) (sym (fst-eq (βh t q))) (transport refl e)) + ≡ β̅₂ (βh t q) ind (transport refl e) + → β̃₂ t ind (subst (Pos P MAlg ind) (sym (fst-eq t)) + (below q e)) + ≡ β̅₂ (βh t q) ind e + mainlem-below t q e indh = + cong (β̃₂ t ind) + (transportPresBelow ind _ _ _ e + ∙ cong (below (subst (Q ∘ shape) (sym (fst-eq t)) q)) + (cong (λ p → subst (Pos P MAlg ind) p e) + (λ i j → comm2' i j) + ∙ moveTransp)) + ∙ comm4' + ∙ ind' + where + comm2' : I → I → M S Q + comm2' j i = + hcomp (λ k + → λ {(i = i0) → fst-eq (βh t q) i1 + ; (i = i1) → pos-t + ; (j = i1) → cpf i1 i + ; (j = i0) → pre-fst-eq-id β̃₁ β̃₂ βs (funExt comm1) βh comm2 t + (~ k) (~ i) + (transp (λ i₁ → Q (comm1 t (~ i ∨ ~ i₁))) + (~ i) q)}) + (hcomp (λ k + → λ {(i = i0) → fst-eq (βh t q) k + ; (i = i1) → pos-t + ; (j = i1) → cpf k i}) + (comm2 t (~ i) + (transp (λ i₁ → Q (comm1 t (~ i ∨ ~ i₁))) + (~ i) + q))) + where + pos-t = pos (β̃₁ t) (transport (sym (cong Q (comm1 t))) q) + cpf = compPath-filler' + (sym (fst-eq (βh t q))) + (sym (funExtDep⁻ (comm2 t) + (λ j₁ → transp (λ i₂ → Q (comm1 t (j₁ ∨ ~ i₂))) + j₁ q))) + + moveTransp = + substComposite + (Pos P MAlg ind) + (sym (fst-eq (βh t q))) + (sym (funExtDep⁻ (comm2 t) + (λ j → transp (λ i → Q (shape (fst-eq t (j ∨ ~ i)))) j q))) e + + comm4' : _ ≡ β̃₂ (βh t q) ind + (subst (Pos P MAlg ind) + (sym (fst-eq (βh t q))) e) + comm4' = + sym (transportRefl _) + ∙ funExt⁻ (fromPathP (funExtDep⁻ (funExt⁻ (comm4 t) ind) + λ j → transp (λ i → Q (shape (fst-eq t (j ∨ ~ i)))) j q)) + (subst (Pos P MAlg ind) (λ i → fst-eq (βh t q) (~ i)) e) + + ind' : β̃₂ (βh t q) ind + (subst (Pos P MAlg ind) (sym (fst-eq (βh t q))) e) + ≡ β̅₂ (βh t q) ind e + ind' = cong (β̃₂ (βh t q) ind) + (cong (subst (Pos P MAlg ind) (sym (fst-eq (βh t q)))) + (sym (transportRefl e))) + ∙∙ indh + ∙∙ cong (β̅₂ (βh t q) ind) (transportRefl e) + + mainlem : (x : Pos P MAlg ind (β̅₁ y)) + → β̃₂ y ind (transport (λ j → Pos P MAlg ind (fst-eq y (~ j))) x) + ≡ β̅₂ y ind x + mainlem = + pos-rec-fun P MAlg ind β̅₁ _ (λ t q → (βh t q) , refl) + mainlem-here mainlem-below y + + -- main result + β̅Unique : β̃ ≡ β̅ + fst (β̅Unique i y) = fst-eq y i + snd (β̅Unique i y) = snd-eq y i diff --git a/Cubical/Codata/M/MRecord.agda b/Cubical/Codata/M/MRecord.agda index 48fb15f21..3650b749a 100644 --- a/Cubical/Codata/M/MRecord.agda +++ b/Cubical/Codata/M/MRecord.agda @@ -33,3 +33,23 @@ open M-R η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 + +-- 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 = 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 diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda index 69ad7060d..7b35cd967 100644 --- a/Cubical/Data/Containers/Algebras.agda +++ b/Cubical/Data/Containers/Algebras.agda @@ -1,6 +1,7 @@ {- Basic definitions required for co/inductive container proofs - Definition of Pos +- Elimination principle -} @@ -9,6 +10,8 @@ module Cubical.Data.Containers.Algebras where open import Cubical.Data.W.W +open import Cubical.Data.Nat +open import Cubical.Data.Empty as ⊥ open import Cubical.Foundations.Function open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Prelude @@ -40,8 +43,78 @@ module Algs (S : Type ℓ) 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 + data Pos {ℓ ℓ'' ℓ'''} {Ind : Type ℓ'''} + (P : Ind → S → Type ℓ'') (FP : ContFuncIso {ℓ}) (i : Ind) : + carrier FP → Type (ℓ-max (ℓ-suc ℓ''') (ℓ-max ℓ'' (ℓ-max ℓ' ℓ))) where + here : {wm : carrier FP} (r : 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 + + -- Height of an element of pos + heightPos : ∀ {ℓInd ℓP ℓFP} {Ind : Type ℓInd} {P : Ind → S → Type ℓP} + {FP : ContFuncIso {ℓFP}} {i : Ind} {wm : _} + → Pos P FP i wm → ℕ + heightPos (here r) = 0 + heightPos (below q x) = suc (heightPos x) + + -- Elimination principle for Pos P FP i (β y) + -- where β : Y → carrier FP + pos-rec-fun : ∀ {ℓY ℓInd ℓW ℓFP} {Y : Type ℓY} {Ind : Type ℓInd} + (P : Ind → S → Type ℓ'') + (FP : ContFuncIso {ℓFP}) (i : Ind) + (β : Y → carrier FP) + (W : (y : Y) → Pos P FP i (β y) → Type ℓW) + (βid : (t : Y) (q : Q (fst (FP .χ .inv (β t)))) -- additional assumption: β is nice + → Σ[ t' ∈ Y ] ((snd (FP .χ .inv (β t)) q) ≡ β t')) + (here* : (t : Y) (x : P i (fst (FP .χ .inv (β t)))) → W t (here x)) + (below* : (t : Y) (q : Q (fst (FP .χ .inv (β t)))) + (e : Pos P FP i (snd (FP .χ .inv (β t)) q)) + → W _ (subst (Pos P FP i) (βid t q .snd) e) + → W t (below q e)) + (t : Y) (e : Pos P FP i (β t)) → W t e + pos-rec-fun {Ind} P FP i β W βid non non2 t e = + pos-rec-fun-help _ t e refl + where + pos-rec-fun-help : + (n : ℕ) + (t : _) (e : Pos P FP i (β t)) + → heightPos e ≡ n + → W t e + pos-rec-fun-help zero t (here r) p = non t r + pos-rec-fun-help zero t (below q e) p = ⊥.rec (snotz p) + pos-rec-fun-help (suc n) t (here r) p = ⊥.rec (snotz (sym p)) + pos-rec-fun-help (suc n) t (below q e) p = + non2 t q e + (pos-rec-fun-help n + _ (subst (Pos P FP i) (βid t q .snd) e) + (substPresHeight _ _ ∙ cong predℕ p)) + where + substPresHeight : (b : _) (p : _ ≡ b) + → heightPos (subst (Pos P FP i) p e) ≡ heightPos e + substPresHeight = J> cong heightPos (transportRefl e) + + + -- transport preserves here and below + module _ {ℓ ℓ'' ℓ''' : Level} {Ind : Type ℓ'''} + {P : Ind → S → Type ℓ''} + {FP : ContFuncIso {ℓ}} (i : Ind) where + + transportPresHere : {a : _} (b : _) (p : a ≡ b) (x : _) + → subst (Pos P FP i) p (here x) + ≡ here (subst (P i ∘ fst ∘ (FP .χ .inv)) p x) + transportPresHere = + J> λ x → transportRefl (here x) + ∙ cong here (sym (transportRefl _)) + + transportPresBelow : {a : _} (b : _) (p : a ≡ b) (q : _) (x : _) + → subst (Pos P FP i) p (below q x) + ≡ below (subst (Q ∘ fst ∘ (FP .χ .inv)) p q) + (subst (Pos P FP i) + (λ j → snd (FP .χ .inv (p j)) + (transp (λ i → Q (fst (FP .χ .inv (p (j ∧ i))))) + (~ j) q)) + x) + transportPresBelow = + J> λ q x → transportRefl (below q x) + ∙ cong₂ below (sym (transportRefl q)) + (toPathP refl) From 997480756ce68a09a0836e90a80b18ed3134befc Mon Sep 17 00:00:00 2001 From: aljungstrom Date: Thu, 18 Jul 2024 11:14:21 +0200 Subject: [PATCH 2/3] renaming --- Cubical/Codata/Containers/Coalgebras.agda | 2 +- .../Containers/CoinductiveContainers.agda | 137 ++++++++++-------- Cubical/Data/Containers/Algebras.agda | 33 ++--- 3 files changed, 90 insertions(+), 82 deletions(-) diff --git a/Cubical/Codata/Containers/Coalgebras.agda b/Cubical/Codata/Containers/Coalgebras.agda index ecaf72b58..17be2b48e 100644 --- a/Cubical/Codata/Containers/Coalgebras.agda +++ b/Cubical/Codata/Containers/Coalgebras.agda @@ -18,7 +18,7 @@ module Coalgs (S : Type ℓ) (Q : S → Type ℓ') where open Iso open M - MAlg : ContFuncIso + MAlg : FixedPoint MAlg = iso (M S Q) isom where isom : Iso (Σ[ s ∈ S ] (Q s → M S Q)) (M S Q) diff --git a/Cubical/Codata/Containers/CoinductiveContainers.agda b/Cubical/Codata/Containers/CoinductiveContainers.agda index c4130b966..56943b884 100644 --- a/Cubical/Codata/Containers/CoinductiveContainers.agda +++ b/Cubical/Codata/Containers/CoinductiveContainers.agda @@ -37,11 +37,17 @@ module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} open Algs S Q open Coalgs S Q - open ContFuncIso + open FixedPoint open Iso + 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))) + -- Construction of a generic - -- β : Y → Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i) + -- β̅ : Y → Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i) module β1 (βs : Y → S) (βh : (y : Y) → Q (βs y) → Y) where @@ -57,16 +63,20 @@ module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} β̅ : Y → Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i) β̅ y = β̅₁ y , β̅₂ y + -- Diagram commutes + β̅Comm : (y : Y) → out (β̅ y) ≡ ((βs y , β̅₁ ∘ (βh y)) , (βg y , λ i q → β̅₂ (βh y q) i)) + β̅Comm y = refl + -- Characterisation of the equality type of the first projection of - -- such a β + -- such a β̅ module makeFirstEq (β̃₁ : Y → M S Q) (β̃₂ : (y : Y) (ind : Ind) → Pos P MAlg ind (β̃₁ y) → X ind) (βs : Y → S) - (comm1 : shape ∘ β̃₁ ≡ βs) + (comm1 : (λ y → fst (fst (out (β̃₁ y , β̃₂ y)))) ≡ βs) --(comm1 : shape ∘ β̃₁ ≡ βs) (βh : (y : Y) → Q (βs y) → Y) - (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M S Q) - (pos (β̃₁ y)) (λ q → β̃₁ (βh y q))) + (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M S Q) + (λ q → snd (fst (out (β̃₁ y , β̃₂ y))) q) (λ q → β̃₁ (βh y q))) where open β1 @@ -81,25 +91,24 @@ module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} (R-intro (βh y q₁)) -- first main result - pre-fst-eq : (y : Y) → β̃₁ y ≡ β̅₁ βs βh y - pre-fst-eq y = MCoind R isBisimR (R-intro y) + preFstEq : (y : Y) → β̃₁ y ≡ β̅₁ βs βh y + preFstEq y = MCoind R isBisimR (R-intro y) - -- Because pre-fst-eq is defined using MCoind, its proof term for + -- Because preFstEq is defined using MCoind, its proof term -- in the pos case is rather complicated. It _should_ look like this: - pre-fst-eq-pos : (y : Y) - → PathP (λ i → Q (shape (pre-fst-eq y i)) → M S Q) + preFstEq-pos : (y : Y) + → PathP (λ i → Q (shape (preFstEq y i)) → M S Q) (pos (β̃₁ y)) (λ t → β̅₁ βs βh (βh y t)) - pre-fst-eq-pos y i q = + preFstEq-pos y i q = hcomp (λ j → λ { (i = i0) → pos (β̃₁ y) q ; - (i = i1) → pre-fst-eq (βh y q) j }) + (i = i1) → preFstEq (βh y q) j }) (comm2 y i q) -- but this definition is not accepted by the termination checker... - - -- Fortunately, we can prove that (cong pos ∘ pre-fst-eq) and - -- pre-fst-eq-pos are equal up to a path (by J and some technical + -- Fortunately, we can prove that (cong pos ∘ preFstEq) and + -- preFstEq-pos are equal up to a path (by J and some technical -- transport juggling). - pre-fst-eq-id : (β̃₁ : Y → M S Q) + preFstEqId : (β̃₁ : Y → M S Q) (β̃₂ : (y : Y) (ind : Ind) → Pos P MAlg ind (β̃₁ y) → X ind) (βs : Y → S) (comm1 : shape ∘ β̃₁ ≡ βs) @@ -107,9 +116,9 @@ module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} (comm2 : (y : Y) → PathP (λ i → Q (comm1 i y) → M S Q) (pos (β̃₁ y)) (λ q → β̃₁ (βh y q))) (y : _) - → cong pos (makeFirstEq.pre-fst-eq β̃₁ β̃₂ βs comm1 βh comm2 y) - ≡ makeFirstEq.pre-fst-eq-pos β̃₁ β̃₂ βs comm1 βh comm2 y - pre-fst-eq-id β̃₁ β̃₂ = + → cong pos (makeFirstEq.preFstEq β̃₁ β̃₂ βs comm1 βh comm2 y) + ≡ makeFirstEq.preFstEq-pos β̃₁ β̃₂ βs comm1 βh comm2 y + preFstEqId β̃₁ β̃₂ = J> λ βh comm2 y → (λ j i q → MCoind (R βh comm2) (isBisimR βh comm2) @@ -139,60 +148,60 @@ module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} (βs : Y → S) (βh : (y : Y) → Q (βs y) → Y) (βg : (y : Y) → (i : Ind) → P i (βs y) → X i) - (β̃ : Y → Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i)) + (β̃₁ : Y → M S Q) + (β̃₂ : (y : Y) (ind : Ind) → Pos P MAlg ind (β̃₁ y) → X ind) (βh : (y : Y) → Q (βs y) → Y) - (comm1 : (y : _) → shape (fst (β̃ y)) ≡ βs y) - (comm2 : (y : Y) → - PathP (λ i → Q (comm1 y i) → M S Q) - (pos (fst (β̃ y))) (λ q → fst (β̃ (βh y q)))) + (comm1 : (y : Y) → fst (fst (out (β̃₁ y , β̃₂ y))) ≡ βs y) + (comm2 : (y : Y) → PathP (λ i → Q (comm1 y i) → M S Q) + (λ q → snd (fst (out (β̃₁ y , β̃₂ y))) q) (λ q → β̃₁ (βh y q))) (comm3 : (y : Y) → PathP (λ i → (ind : Ind) → P ind (comm1 y i) → X ind) - (λ ind p → snd (β̃ y) ind (here p)) - (βg y)) + (fst (snd (out (β̃₁ y , β̃₂ y)))) + (βg y)) (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 → snd (β̃ y) ind (below q b)) - (λ ind q b → snd (β̃ (βh y q)) ind b)) + (snd (snd (out (β̃₁ y , β̃₂ y)))) + (λ ind q b → (β̃₂ (βh y q)) ind b)) where private - β̃₁ = fst ∘ β̃ - β̃₂ = snd ∘ β̃ + β̃ : Y → Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i) + β̃ y = β̃₁ y , β̃₂ y open β1 βs βh open β2 βg open makeFirstEq β̃₁ β̃₂ βs (funExt comm1) βh comm2 - fst-eq : (y : Y) → β̃₁ y ≡ β̅₁ y - fst-eq = pre-fst-eq + fstEq : (y : Y) → β̃₁ y ≡ β̅₁ y + fstEq = preFstEq - snd-eq : (y : Y) - → PathP (λ i → (ind : Ind) → Pos P MAlg ind (fst-eq y i) → X ind) - (β̃₂ y) (β̅₂ y) - snd-eq y = funExt λ ind + sndEq : (y : Y) + → PathP (λ i → (ind : Ind) → Pos P MAlg ind (fstEq y i) → X ind) + (β̃₂ y) (β̅₂ y) + sndEq y = funExt λ ind → toPathP (funExt λ x → transportRefl _ ∙ mainlem ind x) where module _ (ind : Ind) where - mainlem-here : (t : Y) (x : P ind _) - → β̃₂ t ind (subst (Pos P MAlg ind) (sym (fst-eq t)) (here x)) + mainlemHere : (t : Y) (x : P ind _) + → β̃₂ t ind (subst (Pos P MAlg ind) (sym (fstEq t)) (here x)) ≡ β̅₂ t ind (here x) - mainlem-here y x = + mainlemHere y x = cong (β̃₂ y ind) - (transportPresHere ind _ (sym (fst-eq y)) _) + (transportPresHere ind _ (sym (fstEq y)) _) ∙ funExtDep⁻ (funExt⁻ (comm3 y) ind) λ j → (transp (λ i → P ind (comm1 y (~ i ∨ j))) j x) - mainlem-below : (t : Y) (q : Q (βs t)) + mainlemBelow : (t : Y) (q : Q (βs t)) (e : Pos P MAlg ind (β̅₁ (βh t q))) → β̃₂ (βh t q) ind - (subst (Pos P MAlg ind) (sym (fst-eq (βh t q))) (transport refl e)) + (subst (Pos P MAlg ind) (sym (fstEq (βh t q))) (transport refl e)) ≡ β̅₂ (βh t q) ind (transport refl e) - → β̃₂ t ind (subst (Pos P MAlg ind) (sym (fst-eq t)) + → β̃₂ t ind (subst (Pos P MAlg ind) (sym (fstEq t)) (below q e)) - ≡ β̅₂ (βh t q) ind e - mainlem-below t q e indh = + ≡ β̅₂ (βh t q) ind e + mainlemBelow t q e indh = cong (β̃₂ t ind) (transportPresBelow ind _ _ _ e - ∙ cong (below (subst (Q ∘ shape) (sym (fst-eq t)) q)) + ∙ cong (below (subst (Q ∘ shape) (sym (fstEq t)) q)) (cong (λ p → subst (Pos P MAlg ind) p e) (λ i j → comm2' i j) ∙ moveTransp)) @@ -202,15 +211,15 @@ module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} comm2' : I → I → M S Q comm2' j i = hcomp (λ k - → λ {(i = i0) → fst-eq (βh t q) i1 + → λ {(i = i0) → fstEq (βh t q) i1 ; (i = i1) → pos-t ; (j = i1) → cpf i1 i - ; (j = i0) → pre-fst-eq-id β̃₁ β̃₂ βs (funExt comm1) βh comm2 t + ; (j = i0) → preFstEqId β̃₁ β̃₂ βs (funExt comm1) βh comm2 t (~ k) (~ i) (transp (λ i₁ → Q (comm1 t (~ i ∨ ~ i₁))) (~ i) q)}) (hcomp (λ k - → λ {(i = i0) → fst-eq (βh t q) k + → λ {(i = i0) → fstEq (βh t q) k ; (i = i1) → pos-t ; (j = i1) → cpf k i}) (comm2 t (~ i) @@ -220,7 +229,7 @@ module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} where pos-t = pos (β̃₁ t) (transport (sym (cong Q (comm1 t))) q) cpf = compPath-filler' - (sym (fst-eq (βh t q))) + (sym (fstEq (βh t q))) (sym (funExtDep⁻ (comm2 t) (λ j₁ → transp (λ i₂ → Q (comm1 t (j₁ ∨ ~ i₂))) j₁ q))) @@ -228,36 +237,36 @@ module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} moveTransp = substComposite (Pos P MAlg ind) - (sym (fst-eq (βh t q))) + (sym (fstEq (βh t q))) (sym (funExtDep⁻ (comm2 t) - (λ j → transp (λ i → Q (shape (fst-eq t (j ∨ ~ i)))) j q))) e + (λ j → transp (λ i → Q (shape (fstEq t (j ∨ ~ i)))) j q))) e comm4' : _ ≡ β̃₂ (βh t q) ind (subst (Pos P MAlg ind) - (sym (fst-eq (βh t q))) e) + (sym (fstEq (βh t q))) e) comm4' = sym (transportRefl _) ∙ funExt⁻ (fromPathP (funExtDep⁻ (funExt⁻ (comm4 t) ind) - λ j → transp (λ i → Q (shape (fst-eq t (j ∨ ~ i)))) j q)) - (subst (Pos P MAlg ind) (λ i → fst-eq (βh t q) (~ i)) e) + λ j → transp (λ i → Q (shape (fstEq t (j ∨ ~ i)))) j q)) + (subst (Pos P MAlg ind) (λ i → fstEq (βh t q) (~ i)) e) ind' : β̃₂ (βh t q) ind - (subst (Pos P MAlg ind) (sym (fst-eq (βh t q))) e) + (subst (Pos P MAlg ind) (sym (fstEq (βh t q))) e) ≡ β̅₂ (βh t q) ind e ind' = cong (β̃₂ (βh t q) ind) - (cong (subst (Pos P MAlg ind) (sym (fst-eq (βh t q)))) + (cong (subst (Pos P MAlg ind) (sym (fstEq (βh t q)))) (sym (transportRefl e))) ∙∙ indh ∙∙ cong (β̅₂ (βh t q) ind) (transportRefl e) mainlem : (x : Pos P MAlg ind (β̅₁ y)) - → β̃₂ y ind (transport (λ j → Pos P MAlg ind (fst-eq y (~ j))) x) + → β̃₂ y ind (transport (λ j → Pos P MAlg ind (fstEq y (~ j))) x) ≡ β̅₂ y ind x mainlem = - pos-rec-fun P MAlg ind β̅₁ _ (λ t q → (βh t q) , refl) - mainlem-here mainlem-below y + PosIndFun P MAlg ind β̅₁ _ (λ t q → (βh t q) , refl) + mainlemHere mainlemBelow y - -- main result + -- β̅ makes the diagram commute uniquely β̅Unique : β̃ ≡ β̅ - fst (β̅Unique i y) = fst-eq y i - snd (β̅Unique i y) = snd-eq y i + fst (β̅Unique i y) = fstEq y i + snd (β̅Unique i y) = sndEq y i diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda index 7b35cd967..854f59c97 100644 --- a/Cubical/Data/Containers/Algebras.agda +++ b/Cubical/Data/Containers/Algebras.agda @@ -26,15 +26,15 @@ module Algs (S : Type ℓ) open Iso -- Fixed point algebras - record ContFuncIso : Type (ℓ-max (ℓ-suc ℓ'') (ℓ-max ℓ ℓ')) where + record FixedPoint : Type (ℓ-max (ℓ-suc ℓ'') (ℓ-max ℓ ℓ')) where constructor iso field carrier : Type ℓ'' χ : Iso (Σ[ s ∈ S ] (Q s → carrier)) carrier - open ContFuncIso + open FixedPoint - WAlg : ContFuncIso + WAlg : FixedPoint WAlg = iso (W S Q) isom where isom : Iso (Σ[ s ∈ S ] (Q s → W S Q)) (W S Q) @@ -44,7 +44,7 @@ module Algs (S : Type ℓ) leftInv isom (s , f) = refl data Pos {ℓ ℓ'' ℓ'''} {Ind : Type ℓ'''} - (P : Ind → S → Type ℓ'') (FP : ContFuncIso {ℓ}) (i : Ind) : + (P : Ind → S → Type ℓ'') (FP : FixedPoint {ℓ}) (i : Ind) : carrier FP → Type (ℓ-max (ℓ-suc ℓ''') (ℓ-max ℓ'' (ℓ-max ℓ' ℓ))) where here : {wm : carrier FP} (r : P i (fst (FP .χ .inv wm))) → Pos P FP i wm below : {wm : carrier FP} (q : Q (fst (FP .χ .inv wm))) @@ -52,16 +52,16 @@ module Algs (S : Type ℓ) -- Height of an element of pos heightPos : ∀ {ℓInd ℓP ℓFP} {Ind : Type ℓInd} {P : Ind → S → Type ℓP} - {FP : ContFuncIso {ℓFP}} {i : Ind} {wm : _} + {FP : FixedPoint {ℓFP}} {i : Ind} {wm : _} → Pos P FP i wm → ℕ heightPos (here r) = 0 heightPos (below q x) = suc (heightPos x) -- Elimination principle for Pos P FP i (β y) -- where β : Y → carrier FP - pos-rec-fun : ∀ {ℓY ℓInd ℓW ℓFP} {Y : Type ℓY} {Ind : Type ℓInd} + PosIndFun : ∀ {ℓY ℓInd ℓW ℓFP} {Y : Type ℓY} {Ind : Type ℓInd} (P : Ind → S → Type ℓ'') - (FP : ContFuncIso {ℓFP}) (i : Ind) + (FP : FixedPoint {ℓFP}) (i : Ind) (β : Y → carrier FP) (W : (y : Y) → Pos P FP i (β y) → Type ℓW) (βid : (t : Y) (q : Q (fst (FP .χ .inv (β t)))) -- additional assumption: β is nice @@ -72,20 +72,20 @@ module Algs (S : Type ℓ) → W _ (subst (Pos P FP i) (βid t q .snd) e) → W t (below q e)) (t : Y) (e : Pos P FP i (β t)) → W t e - pos-rec-fun {Ind} P FP i β W βid non non2 t e = - pos-rec-fun-help _ t e refl + PosIndFun {Ind} P FP i β W βid non non2 t e = + PosIndFunHelp _ t e refl where - pos-rec-fun-help : + PosIndFunHelp : (n : ℕ) (t : _) (e : Pos P FP i (β t)) → heightPos e ≡ n → W t e - pos-rec-fun-help zero t (here r) p = non t r - pos-rec-fun-help zero t (below q e) p = ⊥.rec (snotz p) - pos-rec-fun-help (suc n) t (here r) p = ⊥.rec (snotz (sym p)) - pos-rec-fun-help (suc n) t (below q e) p = + PosIndFunHelp zero t (here r) p = non t r + PosIndFunHelp zero t (below q e) p = ⊥.rec (snotz p) + PosIndFunHelp (suc n) t (here r) p = ⊥.rec (snotz (sym p)) + PosIndFunHelp (suc n) t (below q e) p = non2 t q e - (pos-rec-fun-help n + (PosIndFunHelp n _ (subst (Pos P FP i) (βid t q .snd) e) (substPresHeight _ _ ∙ cong predℕ p)) where @@ -93,11 +93,10 @@ module Algs (S : Type ℓ) → heightPos (subst (Pos P FP i) p e) ≡ heightPos e substPresHeight = J> cong heightPos (transportRefl e) - -- transport preserves here and below module _ {ℓ ℓ'' ℓ''' : Level} {Ind : Type ℓ'''} {P : Ind → S → Type ℓ''} - {FP : ContFuncIso {ℓ}} (i : Ind) where + {FP : FixedPoint {ℓ}} (i : Ind) where transportPresHere : {a : _} (b : _) (p : a ≡ b) (x : _) → subst (Pos P FP i) p (here x) From 3ed52e39899c3b1aad4ce1f625447da380699734 Mon Sep 17 00:00:00 2001 From: aljungstrom Date: Tue, 23 Jul 2024 04:08:17 +0200 Subject: [PATCH 3/3] paper --- .../Containers/CoinductiveContainers.agda | 1 - Cubical/Papers/Containers.agda | 147 ++++++++++++++++++ 2 files changed, 147 insertions(+), 1 deletion(-) create mode 100644 Cubical/Papers/Containers.agda diff --git a/Cubical/Codata/Containers/CoinductiveContainers.agda b/Cubical/Codata/Containers/CoinductiveContainers.agda index 56943b884..363c07942 100644 --- a/Cubical/Codata/Containers/CoinductiveContainers.agda +++ b/Cubical/Codata/Containers/CoinductiveContainers.agda @@ -162,7 +162,6 @@ module _ {ℓInd ℓS ℓP ℓQ ℓX ℓY : Level} (snd (snd (out (β̃₁ y , β̃₂ y)))) (λ ind q b → (β̃₂ (βh y q)) ind b)) where - private β̃ : Y → Σ[ m ∈ M S Q ] ((i : Ind) → Pos P MAlg i m → X i) β̃ y = β̃₁ y , β̃₂ y diff --git a/Cubical/Papers/Containers.agda b/Cubical/Papers/Containers.agda new file mode 100644 index 000000000..ad2b7ca28 --- /dev/null +++ b/Cubical/Papers/Containers.agda @@ -0,0 +1,147 @@ +{- +Please do not move this file. Changes should only be made if +necessary. + +This file contains pointers to the code examples and main results from +the paper: + +Formalising inductive and coinductive containers, + +-} + +-- The "--safe" flag ensures that there are no postulates or +-- unfinished goals +{-# OPTIONS --safe --cubical --guardedness #-} + +module Cubical.Papers.Containers where + +-- 2 +open import Cubical.Data.Unit as UnitType +open import Cubical.Data.Empty as EmptyType +open import Cubical.Data.Nat as Nat hiding (isEven) +open import Cubical.Codata.Stream as StreamType +open StreamType.Equality≅Bisimulation renaming (bisim to id) +open import Cubical.Foundations.Prelude as Foundations + +open import Cubical.Data.W.W as W-Type +open import Cubical.Codata.M.MRecord as M-Type + +open import Cubical.Data.Containers.Base as Container + +-- 3 +open import Cubical.Data.Containers.Algebras as ContAlg +open import Cubical.Codata.Containers.Coalgebras as ContCoAlg + +-- 4 +open import Cubical.Data.Containers.InductiveContainers as IndCon +open import Cubical.Codata.Containers.CoinductiveContainers as CoIndCon + +-- Unit type: +open UnitType renaming (Unit to ⊤) + +-- Empty type: +open EmptyType using (⊥) + +-- Natural numbers: +open Nat using (ℕ) + +-- Σ-type: +-- omitted (we use a primitive version) + +-- Streams +open StreamType using (Stream) + +-- isEven, isEven+ +isEven : ℕ → Type +isEven zero = ⊤ +isEven (suc zero) = ⊥ +isEven (suc (suc n)) = isEven n + +isEven+ : (n : ℕ) → isEven n → isEven (2 + n) +isEven+ n p = p + +-- The interval type +open Foundations using (I ; _∧_ ; _∨_ ; ~_ ; i0 ; i1) + +-- The path type +open Foundations using (_≡_) + +-- refl and ⁻¹ +open Foundations using (refl ; sym) + +-- hcomp +open Foundations using (hcomp) + +-- construction of top +module _ {A : Type} {x y z w : A} {p : x ≡ z} {q : x ≡ y} {r : y ≡ w} + where + top : z ≡ w + top i = hcomp (λ j → λ {(i = i0) → p j ; + (i = i1) → r j}) + (q i) + +-- transport and subst +open Foundations using (transport ; subst) + +-- funExt +open Foundations using (funExt) + +-- bisimulation and identity type of streams +open StreamType.Equality≅Bisimulation + using (_≈_) renaming (bisim to id) + + +-- 2.2 The W-type and the M-type + +-- The W-type +open W-Type using (W) + +-- The M-type +open M-Type using (M) + +-- MCoind +open M-Type using (MCoind) + +-- 2.3 Containers +-- Definition 3 +open Container using (GenContainer) + +-- Definitions 4 and 5 +-- Omitted (not used explicitly in formalisation) + + +---- 3 Setting up ---- +-- Fixed points: +open ContAlg.Algs using (FixedPoint) + +-- WAlg +open ContAlg.Algs using (WAlg) + +-- MAlg +open ContCoAlg.Coalgs using (MAlg) + +-- Pos +open ContAlg.Algs using (Pos) + +-- Definition 6 +-- Omitted (used implicitly) + +-- Lemma 7 +open ContAlg.Algs using (PosIndFun) + + +---- 4 Fixed points ---- +-- Theorem 8 +open IndCon using (into ; α̅ ; α̅Comm ; α̅Unique) + +-- Theorem 9 +open CoIndCon using (β̅Unique) + +-- Lemma 10 +open CoIndCon.β1.β2 using (β̅) + +-- Lemma 11 (fstEq and sndEq) +open CoIndCon using (fstEq ; sndEq) + +-- Lemma 12 +open CoIndCon using (preFstEqId)