From c67854d2e11aafa5677e25a09087e176fafd3e43 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Thu, 7 May 2020 11:23:12 +0200 Subject: [PATCH] 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 --- Cubical/Codata/Everything.agda | 15 +- Cubical/Codata/M.agda | 15 +- Cubical/Codata/M/AsLimit/Coalg.agda | 5 + Cubical/Codata/M/AsLimit/Coalg/Base.agda | 39 +++++ Cubical/Codata/M/AsLimit/Container.agda | 88 ++++++++++ Cubical/Codata/M/AsLimit/M.agda | 6 + Cubical/Codata/M/AsLimit/M/Base.agda | 195 +++++++++++++++++++++ Cubical/Codata/M/AsLimit/M/Properties.agda | 51 ++++++ Cubical/Codata/M/AsLimit/helper.agda | 116 ++++++++++++ Cubical/Codata/M/AsLimit/itree.agda | 75 ++++++++ Cubical/Codata/M/AsLimit/stream.agda | 30 ++++ Cubical/Data/DiffInt/Properties.agda | 2 +- Cubical/Data/Sigma/Properties.agda | 105 +++++++++-- Cubical/Data/Unit/Properties.agda | 5 + Cubical/Experiments/EscardoSIP.agda | 2 +- Cubical/Foundations/Equiv/HalfAdjoint.agda | 65 +++++++ Cubical/Foundations/Isomorphism.agda | 23 +++ Cubical/Functions/Embedding.agda | 17 ++ Cubical/Functions/Fibration.agda | 2 +- Cubical/Functions/FunExtEquiv.agda | 2 + Cubical/HITs/KleinBottle/Properties.agda | 2 +- 21 files changed, 836 insertions(+), 24 deletions(-) create mode 100644 Cubical/Codata/M/AsLimit/Coalg.agda create mode 100644 Cubical/Codata/M/AsLimit/Coalg/Base.agda create mode 100644 Cubical/Codata/M/AsLimit/Container.agda create mode 100644 Cubical/Codata/M/AsLimit/M.agda create mode 100644 Cubical/Codata/M/AsLimit/M/Base.agda create mode 100644 Cubical/Codata/M/AsLimit/M/Properties.agda create mode 100644 Cubical/Codata/M/AsLimit/helper.agda create mode 100644 Cubical/Codata/M/AsLimit/itree.agda create mode 100644 Cubical/Codata/M/AsLimit/stream.agda diff --git a/Cubical/Codata/Everything.agda b/Cubical/Codata/Everything.agda index 2802bb300b..a103ec1b80 100644 --- 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 index b85c44f047..363e8687a0 100644 --- a/Cubical/Codata/M.agda +++ b/Cubical/Codata/M.agda @@ -32,15 +32,15 @@ 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 @@ -48,11 +48,14 @@ record M {X : Type₀} (C : IxCont X) (x : X) : Type₀ where 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 new file mode 100644 index 0000000000..01ec1311cc --- /dev/null +++ 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 new file mode 100644 index 0000000000..6aba0b0652 --- /dev/null +++ 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 new file mode 100644 index 0000000000..d972861000 --- /dev/null +++ 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 new file mode 100644 index 0000000000..4da4acae75 --- /dev/null +++ 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 new file mode 100644 index 0000000000..69eeda8de4 --- /dev/null +++ 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 diff --git a/Cubical/Codata/M/AsLimit/M/Properties.agda b/Cubical/Codata/M/AsLimit/M/Properties.agda new file mode 100644 index 0000000000..0a27e81ae5 --- /dev/null +++ b/Cubical/Codata/M/AsLimit/M/Properties.agda @@ -0,0 +1,51 @@ +{-# OPTIONS --cubical --guardedness --safe #-} + +module Cubical.Codata.M.AsLimit.M.Properties where + +open import Cubical.Data.Unit +open import Cubical.Data.Prod +open import Cubical.Data.Nat as ℕ using (ℕ ; suc ; _+_ ) +open import Cubical.Data.Sum +open import Cubical.Data.Sigma + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv using (_≃_) +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.Function +open import Cubical.Foundations.Equiv + +open import Cubical.Functions.Embedding + +open import Cubical.Codata.M.AsLimit.helper +open import Cubical.Codata.M.AsLimit.M.Base +open import Cubical.Codata.M.AsLimit.Container + +-- in-fun and out-fun are inverse + +open Iso + +in-inverse-out : ∀ {ℓ} {S : Container ℓ} -> (in-fun ∘ out-fun {S = S}) ≡ idfun (M S) +in-inverse-out {S = S} = funExt (rightInv {A = P₀ S (M S)} {B = M S} (shift-iso S)) + +out-inverse-in : ∀ {ℓ} {S : Container ℓ} -> (out-fun {S = S} ∘ in-fun {S = S}) ≡ idfun (P₀ S (M S)) +out-inverse-in {S = S} = funExt (leftInv {A = P₀ S (M S)} {B = M S} (shift-iso S)) + +in-out-id : ∀ {ℓ} {S : Container ℓ} -> ∀ {x y} → (in-fun (out-fun {S = S} x) ≡ in-fun (out-fun {S = S} y)) ≡ (x ≡ y) +in-out-id {x = x} {y} i = (in-inverse-out i x) ≡ (in-inverse-out i y) + +-- constructor properties + +in-inj : ∀ {ℓ} {S : Container ℓ} {Z : Type ℓ} -> ∀ {f g : Z → P₀ S (M S)} -> (in-fun ∘ f ≡ in-fun ∘ g) ≡ (f ≡ g) +in-inj {ℓ} {S = S} {Z = Z} {f = f} {g = g} = iso→fun-Injection-Path {ℓ = ℓ} {A = P₀ S (M S)} {B = M S} {C = Z} (shift-iso S) {f = f} {g = g} + +out-inj : ∀ {ℓ} {S : Container ℓ} {Z : Type ℓ} -> ∀ {f g : Z → M S} -> (out-fun ∘ f ≡ out-fun ∘ g) ≡ (f ≡ g) +out-inj {ℓ} {S = S} {Z = Z} {f = f} {g = g} = iso→inv-Injection-Path {ℓ = ℓ} {A = P₀ S (M S)} {B = M S} {C = Z} (shift-iso S) {f = f} {g = g} + +in-inj-x : ∀ {ℓ} {S : Container ℓ} -> ∀ {x y : P₀ S (M S)} -> (in-fun x ≡ in-fun y) ≡ (x ≡ y) +in-inj-x {ℓ} {S = S} {x = x} {y} = iso→fun-Injection-Path-x (shift-iso S) + +out-inj-x : ∀ {ℓ} {S : Container ℓ} -> ∀ {x y : M S} -> (out-fun x ≡ out-fun y) ≡ (x ≡ y) +out-inj-x {ℓ} {S = S} {x = x} {y} = iso→inv-Injection-Path-x (shift-iso S) diff --git a/Cubical/Codata/M/AsLimit/helper.agda b/Cubical/Codata/M/AsLimit/helper.agda new file mode 100644 index 0000000000..d07aa9ede4 --- /dev/null +++ b/Cubical/Codata/M/AsLimit/helper.agda @@ -0,0 +1,116 @@ +{-# OPTIONS --cubical --guardedness --safe #-} + +module Cubical.Codata.M.AsLimit.helper 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.Foundations.Transport +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Path + +open import Cubical.Functions.Embedding +open import Cubical.Functions.FunExtEquiv + +open Iso + +-- General + +iso→fun-Injection : + ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B) + → ∀ {f g : C -> A} + → (x : C) → (Iso.fun isom (f x) ≡ Iso.fun isom (g x)) ≡ (f x ≡ g x) +iso→fun-Injection {A = A} {B} {C} isom {f = f} {g} = + isEmbedding→Injection {A = A} {B} {C} (Iso.fun isom) (iso→isEmbedding {A = A} {B} isom) {f = f} {g = g} + +abstract + iso→Pi-fun-Injection : + ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B) + → ∀ {f g : C -> A} + → Iso (∀ x → (fun isom) (f x) ≡ (fun isom) (g x)) (∀ x → f x ≡ g x) + iso→Pi-fun-Injection {A = A} {B} {C} isom {f = f} {g} = + pathToIso (cong (λ k → ∀ x → k x) (funExt (iso→fun-Injection isom {f = f} {g = g}))) + +iso→fun-Injection-Iso : + ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B) + → ∀ {f g : C -> A} + → Iso (fun isom ∘ f ≡ fun isom ∘ g) (f ≡ g) +iso→fun-Injection-Iso {A = A} {B} {C} isom {f = f} {g} = + (fun isom) ∘ f ≡ (fun isom) ∘ g + Iso⟨ invIso funExtIso ⟩ + (∀ x → (fun isom) (f x) ≡ (fun isom) (g x)) + Iso⟨ iso→Pi-fun-Injection isom ⟩ + (∀ x → f x ≡ g x) + Iso⟨ funExtIso ⟩ + f ≡ g ∎Iso + +iso→fun-Injection-Path : + ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B) + → ∀ {f g : C -> A} + → (fun isom ∘ f ≡ fun isom ∘ g) ≡ (f ≡ g) +iso→fun-Injection-Path {A = A} {B} {C} isom {f = f} {g} = + isoToPath (iso→fun-Injection-Iso isom) + +iso→inv-Injection-Path : + ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B) → + ∀ {f g : C -> B} → + ----------------------- + ((inv isom) ∘ f ≡ (inv isom) ∘ g) ≡ (f ≡ g) +iso→inv-Injection-Path {A = A} {B} {C} isom {f = f} {g} = iso→fun-Injection-Path (invIso isom) + +iso→fun-Injection-Iso-x : + ∀ {ℓ} {A B : Type ℓ} + → (isom : Iso A B) + → ∀ {x y : A} + → Iso ((fun isom) x ≡ (fun isom) y) (x ≡ y) +iso→fun-Injection-Iso-x isom {x} {y} = + let tempx = λ {(lift tt) → x} + tempy = λ {(lift tt) → y} in + fun isom x ≡ fun isom y + Iso⟨ iso (λ x₁ t → x₁) + (λ x₁ → x₁ (lift tt)) + (λ x → refl) + (λ x → refl) ⟩ + (∀ (t : Lift Unit) -> (((fun isom) ∘ tempx) t ≡ ((fun isom) ∘ tempy) t)) + Iso⟨ iso→Pi-fun-Injection isom ⟩ + (∀ (t : Lift Unit) -> tempx t ≡ tempy t) + Iso⟨ iso (λ x₁ → x₁ (lift tt)) + (λ x₁ t → x₁) + (λ x → refl) + (λ x → refl) ⟩ + x ≡ y ∎Iso + +iso→inv-Injection-Iso-x : + ∀ {ℓ} {A B : Type ℓ} + → (isom : Iso A B) + → ∀ {x y : B} + → Iso ((inv isom) x ≡ (inv isom) y) (x ≡ y) +iso→inv-Injection-Iso-x {A = A} {B = B} isom = + iso→fun-Injection-Iso-x {A = B} {B = A} (invIso isom) + +iso→fun-Injection-Path-x : + ∀ {ℓ} {A B : Type ℓ} + → (isom : Iso A B) + → ∀ {x y : A} + → ((fun isom) x ≡ (fun isom) y) ≡ (x ≡ y) +iso→fun-Injection-Path-x isom {x} {y} = + isoToPath (iso→fun-Injection-Iso-x isom) + +iso→inv-Injection-Path-x : + ∀ {ℓ} {A B : Type ℓ} + → (isom : Iso A B) + → ∀ {x y : B} + → ((inv isom) x ≡ (inv isom) y) ≡ (x ≡ y) +iso→inv-Injection-Path-x isom = + isoToPath (iso→inv-Injection-Iso-x isom) + diff --git a/Cubical/Codata/M/AsLimit/itree.agda b/Cubical/Codata/M/AsLimit/itree.agda new file mode 100644 index 0000000000..068b7a28e7 --- /dev/null +++ b/Cubical/Codata/M/AsLimit/itree.agda @@ -0,0 +1,75 @@ +{-# OPTIONS --cubical --guardedness --safe #-} + +module Cubical.Codata.M.AsLimit.itree where + +open import Cubical.Data.Unit +open import Cubical.Data.Prod +open import Cubical.Data.Nat as ℕ using (ℕ ; suc ; _+_ ) +open import Cubical.Data.Sum +open import Cubical.Data.Empty +open import Cubical.Data.Bool + +open import Cubical.Foundations.Function +open import Cubical.Foundations.Prelude + +open import Cubical.Codata.M.AsLimit.Container +open import Cubical.Codata.M.AsLimit.M +open import Cubical.Codata.M.AsLimit.Coalg + +-- Delay monad defined as an M-type +delay-S : (R : Type₀) -> Container ℓ-zero +delay-S R = (Unit ⊎ R) , λ { (inr _) -> ⊥ ; (inl tt) -> Unit } + +delay : (R : Type₀) -> Type₀ +delay R = M (delay-S R) + +delay-ret : {R : Type₀} -> R -> delay R +delay-ret r = in-fun (inr r , λ ()) + +delay-tau : {R : Type₀} -> delay R -> delay R +delay-tau S = in-fun (inl tt , λ x → S) + +-- Bottom element raised +data ⊥₁ : Type₁ where + +-- TREES +tree-S : (E : Type₀ -> Type₁) (R : Type₀) -> Container (ℓ-suc ℓ-zero) +tree-S E R = (R ⊎ (Σ[ A ∈ Type₀ ] (E A))) , (λ { (inl _) -> ⊥₁ ; (inr (A , e)) -> Lift A } ) + +tree : (E : Type₀ -> Type₁) (R : Type₀) -> Type₁ +tree E R = M (tree-S E R) + +tree-ret : ∀ {E} {R} -> R -> tree E R +tree-ret {E} {R} r = in-fun (inl r , λ ()) + +tree-vis : ∀ {E} {R} -> ∀ {A} -> E A -> (A -> tree E R) -> tree E R +tree-vis {A = A} e k = in-fun (inr (A , e) , λ { (lift x) -> k x } ) + +-- ITrees (and buildup examples) +-- https://arxiv.org/pdf/1906.00046.pdf +-- Interaction Trees: Representing Recursive and Impure Programs in Coq +-- Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic + +itree-S : ∀ (E : Type₀ -> Type₁) (R : Type₀) -> Container (ℓ-suc ℓ-zero) +itree-S E R = ((Unit ⊎ R) ⊎ (Σ[ A ∈ Type₀ ] (E A))) , (λ { (inl (inl _)) -> Lift Unit ; (inl (inr _)) -> ⊥₁ ; (inr (A , e)) -> Lift A } ) + +itree : ∀ (E : Type₀ -> Type₁) (R : Type₀) -> Type₁ +itree E R = M (itree-S E R) + +ret' : ∀ {E} {R} -> R -> P₀ (itree-S E R) (itree E R) +ret' {E} {R} r = inl (inr r) , λ () + +tau' : {E : Type₀ -> Type₁} -> {R : Type₀} -> itree E R -> P₀ (itree-S E R) (itree E R) +tau' t = inl (inl tt) , λ x → t + +vis' : ∀ {E} {R} -> ∀ {A : Type₀} -> E A -> (A -> itree E R) -> P₀ (itree-S E R) (itree E R) +vis' {A = A} e k = inr (A , e) , λ { (lift x) -> k x } + +ret : ∀ {E} {R} -> R -> itree E R +ret = in-fun ∘ ret' + +tau : {E : Type₀ -> Type₁} -> {R : Type₀} -> itree E R -> itree E R +tau = in-fun ∘ tau' + +vis : ∀ {E} {R} -> ∀ {A : Type₀} -> E A -> (A -> itree E R) -> itree E R +vis {A = A} e = in-fun ∘ (vis' {A = A} e) diff --git a/Cubical/Codata/M/AsLimit/stream.agda b/Cubical/Codata/M/AsLimit/stream.agda new file mode 100644 index 0000000000..2da82b8296 --- /dev/null +++ b/Cubical/Codata/M/AsLimit/stream.agda @@ -0,0 +1,30 @@ +{-# OPTIONS --cubical --guardedness --safe #-} + +module Cubical.Codata.M.AsLimit.stream where + +open import Cubical.Data.Unit + +open import Cubical.Foundations.Prelude + +open import Cubical.Codata.M.AsLimit.M +open import Cubical.Codata.M.AsLimit.helper +open import Cubical.Codata.M.AsLimit.Container + +-------------------------------------- +-- Stream definitions using M.AsLimit -- +-------------------------------------- + +stream-S : ∀ A -> Container ℓ-zero +stream-S A = (A , (λ _ → Unit)) + +stream : ∀ (A : Type₀) -> Type₀ +stream A = M (stream-S A) + +cons : ∀ {A} -> A -> stream A -> stream A +cons x xs = in-fun (x , λ { tt -> xs } ) + +hd : ∀ {A} -> stream A -> A +hd {A} S = out-fun S .fst + +tl : ∀ {A} -> stream A -> stream A +tl {A} S = out-fun S .snd tt diff --git a/Cubical/Data/DiffInt/Properties.agda b/Cubical/Data/DiffInt/Properties.agda index 3eeb6579d2..1d50c2424b 100644 --- a/Cubical/Data/DiffInt/Properties.agda +++ b/Cubical/Data/DiffInt/Properties.agda @@ -32,7 +32,7 @@ relIsEquiv = EquivRel {A = ℕ × ℕ} relIsRefl relIsSym relIsTrans ((b1 + b0) + a0) + c1 ≡[ i ]⟨ +-comm (b1 + b0) a0 i + c1 ⟩ (a0 + (b1 + b0)) + c1 ≡[ i ]⟨ +-assoc a0 b1 b0 i + c1 ⟩ (a0 + b1) + b0 + c1 ≡⟨ sym (+-assoc (a0 + b1) b0 c1) ⟩ - (a0 + b1) + (b0 + c1) ≡⟨ cong (λ p → p . fst + p .snd) (transport (ua Σ≡) (p0 , p1))⟩ + (a0 + b1) + (b0 + c1) ≡⟨ cong (λ p → p . fst + p .snd) (transport Σ≡ (p0 , p1))⟩ (b0 + a1) + (c0 + b1) ≡⟨ sym (+-assoc b0 a1 (c0 + b1))⟩ b0 + (a1 + (c0 + b1)) ≡[ i ]⟨ b0 + (a1 + +-comm c0 b1 i) ⟩ b0 + (a1 + (b1 + c0)) ≡[ i ]⟨ b0 + +-comm a1 (b1 + c0) i ⟩ diff --git a/Cubical/Data/Sigma/Properties.agda b/Cubical/Data/Sigma/Properties.agda index 224a2c3276..f170aa76e7 100644 --- a/Cubical/Data/Sigma/Properties.agda +++ b/Cubical/Data/Sigma/Properties.agda @@ -16,6 +16,9 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Path open import Cubical.Foundations.Transport open import Cubical.Foundations.Univalence open import Cubical.Relation.Nullary @@ -41,21 +44,21 @@ mapˡ f (a , b) = (f a , b) → x ≡ y ΣPathP eq i = fst eq i , snd eq i -Σ≡ : {x y : Σ A B} → +Σ-split-iso : {x y : Σ A B} + → Iso (Σ[ q ∈ fst x ≡ fst y ] (PathP (λ i → B (q i)) (snd x) (snd y))) + (x ≡ y) +Iso.fun (Σ-split-iso) = ΣPathP +Iso.inv (Σ-split-iso) eq = (λ i → fst (eq i)) , (λ i → snd (eq i)) +Iso.rightInv (Σ-split-iso) x = refl {x = x} +Iso.leftInv (Σ-split-iso) x = refl {x = x} + +Σ≃ : {x y : Σ A B} → Σ (fst x ≡ fst y) (λ p → PathP (λ i → B (p i)) (snd x) (snd y)) ≃ (x ≡ y) -Σ≡ {A = A} {B = B} {x} {y} = isoToEquiv (iso intro elim intro-elim elim-intro) - where - intro = ΣPathP - - elim : x ≡ y → Σ (fst x ≡ fst y) (λ a≡ → PathP (λ i → B (a≡ i)) (snd x) (snd y )) - elim eq = (λ i → fst (eq i)) , (λ i → snd (eq i)) - - intro-elim : ∀ eq → intro (elim eq) ≡ eq - intro-elim eq = refl +Σ≃ {A = A} {B = B} {x} {y} = isoToEquiv (Σ-split-iso) - elim-intro : ∀ eq → elim (intro eq) ≡ eq - elim-intro eq = refl +Σ≡ : {a a' : A} {b : B a} {b' : B a'} → (Σ (a ≡ a') (λ q → PathP (λ i → B (q i)) b b')) ≡ ((a , b) ≡ (a' , b')) +Σ≡ = isoToPath Σ-split-iso -- ua Σ≃ ΣProp≡ : ((x : A) → isProp (B x)) → {u v : Σ A B} → (p : u .fst ≡ v .fst) → u ≡ v @@ -153,7 +156,7 @@ discreteΣ {B = B} Adis Bdis (a0 , b0) (a1 , b1) = discreteΣ' (Adis a0 a1) where discreteΣ'' : (b1 : B a0) → Dec ((a0 , b0) ≡ (a0 , b1)) discreteΣ'' b1 with Bdis a0 b0 b1 - ... | (yes q) = yes (transport (ua Σ≡) (refl , q)) + ... | (yes q) = yes (transport (ua Σ≃) (refl , q)) ... | (no ¬q) = no (λ r → ¬q (subst (λ X → PathP (λ i → B (X i)) b0 b1) (Discrete→isSet Adis a0 a0 (cong fst r) refl) (cong snd r))) discreteΣ' (no ¬p) = no (λ r → ¬p (cong fst r)) @@ -193,3 +196,79 @@ PiΣ = isoToEquiv (iso (λ f → fst ∘ f , snd ∘ f) swapΣEquiv : ∀ {ℓ'} (A : Type ℓ) (B : Type ℓ') → A × B ≃ B × A swapΣEquiv A B = isoToEquiv (iso (λ x → x .snd , x .fst) (λ z → z .snd , z .fst) (\ _ → refl) (\ _ → refl)) + +Σ-ap-iso₁ : ∀ {ℓ} {ℓ'} {A A' : Type ℓ} {B : A' → Type ℓ'} + → (isom : Iso A A') + → Iso (Σ A (B ∘ (Iso.fun isom))) + (Σ A' B) +Iso.fun (Σ-ap-iso₁ isom) x = (Iso.fun isom) (x .fst) , x .snd +Iso.inv (Σ-ap-iso₁ {B = B} isom) x = (Iso.inv isom) (x .fst) , subst B (sym (ε' (x .fst))) (x .snd) + where + ε' = fst (vogt isom) +Iso.rightInv (Σ-ap-iso₁ {B = B} isom) (x , y) = ΣPathP (ε' x , + transport + (sym (PathP≡Path (λ j → cong B (ε' x) j) (subst B (sym (ε' x)) y) y)) + (subst B (ε' x) (subst B (sym (ε' x)) y) + ≡⟨ sym (substComposite B (sym (ε' x)) (ε' x) y) ⟩ + subst B ((sym (ε' x)) ∙ (ε' x)) y + ≡⟨ (cong (λ a → subst B a y) (lCancel (ε' x))) ⟩ + subst B refl y + ≡⟨ substRefl {B = B} y ⟩ + y ∎)) + where + ε' = fst (vogt isom) +Iso.leftInv (Σ-ap-iso₁ {A = A} {B = B} isom@(iso f g ε η)) (x , y) = ΣPathP (η x , + transport + (sym (PathP≡Path (λ j → cong B (cong f (η x)) j) (subst B (sym (ε' (f x))) y) y)) + (subst B (cong f (η x)) (subst B (sym (ε' (f x))) y) + ≡⟨ sym (substComposite B (sym (ε' (f x))) (cong f (η x)) y) ⟩ + subst B (sym (ε' (f x)) ∙ (cong f (η x))) y + ≡⟨ cong (λ a → subst B a y) (lem x) ⟩ + subst B (refl) y + ≡⟨ substRefl {B = B} y ⟩ + y ∎)) + where + ε' = fst (vogt isom) + γ = snd (vogt isom) + + lem : (x : A) → sym (ε' (f x)) ∙ cong f (η x) ≡ refl + lem x = cong (λ a → sym (ε' (f x)) ∙ a) (γ x) ∙ lCancel (ε' (f x)) + +Σ-ap₁ : (isom : A ≡ A') → Σ A (B ∘ transport isom) ≡ Σ A' B +Σ-ap₁ isom = isoToPath (Σ-ap-iso₁ (pathToIso isom)) + +Σ-ap-iso₂ : ((x : A) → Iso (B x) (B' x)) → Iso (Σ A B) (Σ A B') +Iso.fun (Σ-ap-iso₂ isom) (x , y) = x , Iso.fun (isom x) y +Iso.inv (Σ-ap-iso₂ isom) (x , y') = x , Iso.inv (isom x) y' +Iso.rightInv (Σ-ap-iso₂ isom) (x , y) = ΣPathP (refl , Iso.rightInv (isom x) y) +Iso.leftInv (Σ-ap-iso₂ isom) (x , y') = ΣPathP (refl , Iso.leftInv (isom x) y') + +Σ-ap₂ : ((x : A) → B x ≡ B' x) → Σ A B ≡ Σ A B' +Σ-ap₂ isom = isoToPath (Σ-ap-iso₂ (pathToIso ∘ isom)) + +Σ-ap-iso : + ∀ {ℓ ℓ'} {A A' : Type ℓ} + → {B : A → Type ℓ'} {B' : A' → Type ℓ'} + → (isom : Iso A A') + → ((x : A) → Iso (B x) (B' (Iso.fun isom x))) + ------------------------ + → Iso (Σ A B) (Σ A' B') +Σ-ap-iso isom isom' = compIso (Σ-ap-iso₂ isom') (Σ-ap-iso₁ isom) + +Σ-ap : + ∀ {ℓ ℓ'} {X X' : Type ℓ} {Y : X → Type ℓ'} {Y' : X' → Type ℓ'} + → (isom : X ≡ X') + → ((x : X) → Y x ≡ Y' (transport isom x)) + ---------- + → (Σ X Y) + ≡ (Σ X' Y') +Σ-ap isom isom' = isoToPath (Σ-ap-iso (pathToIso isom) (pathToIso ∘ isom')) + +Σ-ap' : + ∀ {ℓ ℓ'} {X X' : Type ℓ} {Y : X → Type ℓ'} {Y' : X' → Type ℓ'} + → (isom : X ≡ X') + → (PathP (λ i → isom i → Type ℓ') Y Y') + ---------- + → (Σ X Y) + ≡ (Σ X' Y') +Σ-ap' {ℓ} {ℓ'} isom isom' = cong₂ (λ (a : Type ℓ) (b : a → Type ℓ') → Σ a λ x → b x) isom isom' diff --git a/Cubical/Data/Unit/Properties.agda b/Cubical/Data/Unit/Properties.agda index 606a88c78a..95b20ffb66 100644 --- a/Cubical/Data/Unit/Properties.agda +++ b/Cubical/Data/Unit/Properties.agda @@ -8,6 +8,7 @@ open import Cubical.Foundations.HLevels open import Cubical.Data.Nat open import Cubical.Data.Unit.Base +open import Cubical.Data.Prod.Base isContrUnit : isContr Unit isContrUnit = tt , λ {tt → refl} @@ -17,3 +18,7 @@ isPropUnit _ _ i = tt -- definitionally equal to: isContr→isProp isContrUnit isOfHLevelUnit : (n : ℕ) → isOfHLevel n Unit isOfHLevelUnit n = isContr→isOfHLevel n isContrUnit + +diagonal-unit : Unit ≡ Unit × Unit +diagonal-unit = isoToPath (iso (λ x → tt , tt) (λ x → tt) (λ {(tt , tt) i → tt , tt}) λ {tt i → tt}) + where open import Cubical.Foundations.Isomorphism diff --git a/Cubical/Experiments/EscardoSIP.agda b/Cubical/Experiments/EscardoSIP.agda index e75a8b20f3..dcb88a8e20 100644 --- a/Cubical/Experiments/EscardoSIP.agda +++ b/Cubical/Experiments/EscardoSIP.agda @@ -218,7 +218,7 @@ SIP S ι θ A B = (Σ[ p ∈ (typ A) ≡ (typ B) ] (ι A B (pathToEquiv p))) ≃⟨ iii ⟩ (A ≃[ ι ] B) ■ where - i = invEquiv Σ≡ + i = invEquiv Σ≃ ii = Σ-cong-≃ (hom-lemma-dep S ι θ A B) iii = Σ-change-of-variable-≃ pathToEquiv (equivIsEquiv univalence) diff --git a/Cubical/Foundations/Equiv/HalfAdjoint.agda b/Cubical/Foundations/Equiv/HalfAdjoint.agda index 98f7a4439a..d999a1e899 100644 --- a/Cubical/Foundations/Equiv/HalfAdjoint.agda +++ b/Cubical/Foundations/Equiv/HalfAdjoint.agda @@ -14,6 +14,7 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Function using (_∘_) open import Cubical.Foundations.GroupoidLaws record isHAEquiv {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) : Type (ℓ-max ℓ ℓ') where @@ -88,6 +89,27 @@ iso→HAEquiv {A = A} {B = B} (iso f g ε η) = f , (record { g = g ; sec = η ; ; (j = i1) → ε (f a) k}) (cong (cong f) (sym (Hfa≡fHa (λ x → g (f x)) η a)) i j) +-- Theorem 4.2.3. of HoTT book (similar to iso→HAEquiv) +-- This exists to make the proof of vogt (see later in the file) easier, +-- since iso→HAEquiv does not reduce fully when applied. +iso→HAEquiv' : Iso A B → HAEquiv A B +fst (iso→HAEquiv' (iso f g ε η)) = f +isHAEquiv.g (snd (iso→HAEquiv' (iso f g ε η))) = g +isHAEquiv.sec (snd (iso→HAEquiv' (iso f g ε η))) = η +isHAEquiv.ret (snd (iso→HAEquiv' (iso f g ε η))) b = sym (ε (f (g b))) ∙ (cong f (η (g b)) ∙ ε b) +isHAEquiv.com (snd (iso→HAEquiv' (iso f g ε η))) a = + cong f (η a) + ≡⟨ lUnit (cong f (η a)) ⟩ + refl ∙ cong f (η a) + ≡⟨ cong (λ m → m ∙ cong f (η a)) (sym (lCancel (ε (f (g (f a)))))) ⟩ + (sym (ε (f (g (f a)))) ∙ ε (f (g (f a)))) ∙ cong f (η a) + ≡⟨ sym (assoc (sym (ε (f (g (f a))))) (ε (f (g (f a)))) (cong f (η a))) ⟩ + sym (ε (f (g (f a)))) ∙ ε (f (g (f a))) ∙ cong f (η a) + ≡⟨ cong (λ m → sym (ε (f (g (f a)))) ∙ m) (homotopyNatural (ε ∘ f) (η a)) ⟩ + sym (ε (f (g (f a)))) ∙ (cong (f ∘ g ∘ f) (η a)) ∙ ε (f a) + ≡⟨ cong (λ m → sym (ε (f (g (f a)))) ∙ cong f m ∙ ε (f a)) (sym (Hfa≡fHa (λ x → g (f x)) η a)) ⟩ + sym (ε (f (g (f a)))) ∙ (cong f (η (g (f a)))) ∙ ε (f a) ∎ + equiv→HAEquiv : A ≃ B → HAEquiv A B equiv→HAEquiv e = iso→HAEquiv (equivToIso e) @@ -143,3 +165,46 @@ congEquiv {A = A} {B} {x} {y} e = isoToEquiv (iso intro elim intro-elim elim-int ; (j = i0) → secEq e x (i ∨ k) ; (j = i1) → secEq e y (i ∨ k) }) (secEq e (p j) i) + + +coherent : ∀ {ℓ} {A B : Type ℓ} (isom : Iso A B) → Type ℓ +coherent (iso f g H K) = ∀ x → cong f (K x) ≡ H (f x) + +-- vogt's lemma (https://ncatlab.org/nlab/show/homotopy+equivalence#vogts_lemma) +vogt : ∀ {ℓ} {X Y : Type ℓ} → (isom : Iso X Y) → Σ ((y : Y) → Iso.fun isom (Iso.inv isom y) ≡ y) λ iso' → coherent (iso (Iso.fun isom) (Iso.inv isom) iso' (Iso.leftInv isom)) +vogt {X = X} isom@(iso f g ε η) = ε' , γ + where + ε' : ∀ y → f (g y) ≡ y + ε' x = cong (f ∘ g) (sym (ε x)) ∙ cong f (η (g x)) ∙ ε x + + lem : ∀ (x : X) + → cong f (η (g (f x))) ∙ ε (f x) + ≡ cong (f ∘ g) (ε (f x)) ∙ cong f (η x) + lem x = + cong f (η (g (f x))) ∙ ε (f x) + ≡⟨ lUnit (cong (f) (η (g (f x))) ∙ ε (f x)) ⟩ + refl ∙ cong f (η (g (f x))) ∙ ε (f x) + ≡⟨ cong (λ a → a ∙ cong f (η (g (f x))) ∙ ε (f x)) (sym (rCancel (ε (f (g (f x)))))) ⟩ + (ε (f (g (f x))) ∙ sym (ε (f (g (f x))))) ∙ cong f (η (g (f x))) ∙ ε (f x) + ≡⟨ sym (assoc (ε (f (g (f x)))) (sym (ε (f (g (f x))))) (cong f (η (g (f x))) ∙ ε (f x))) ⟩ + ε (f (g (f x))) ∙ sym (ε (f (g (f x)))) ∙ cong f (η (g (f x))) ∙ ε (f x) + ≡⟨ cong (λ a → ε (f (g (f x))) ∙ a) (sym (isHAEquiv.com (iso→HAEquiv' isom .snd) x)) ⟩ + ε (f (g (f x))) ∙ cong f (η x) + ≡⟨ cong (λ a → a ∙ cong f (η x)) (Hfa≡fHa (f ∘ g) ε (f x)) ⟩ + cong (f ∘ g) (ε (f x)) ∙ cong f (η x) ∎ + + γ : coherent (iso f g ε' η) + γ x = sym + (ε' (f x) + ≡⟨ refl ⟩ + cong (f ∘ g) (sym (ε (f x))) ∙ cong f (η (g (f x))) ∙ ε (f x) + ≡⟨ cong (λ a → cong (f ∘ g) (sym (ε (f x))) ∙ a) (lem x) ⟩ + cong (f ∘ g) (sym (ε (f x))) ∙ cong (f ∘ g) (ε (f x)) ∙ cong f (η x) + ≡⟨ refl ⟩ + sym (cong (f ∘ g) (ε (f x))) ∙ cong (f ∘ g) (ε (f x)) ∙ cong f (η x) + ≡⟨ assoc (sym (cong (f ∘ g) (ε (f x)))) (cong (f ∘ g) (ε (f x))) (cong f (η x)) ⟩ + (sym (cong (f ∘ g) (ε (f x))) ∙ cong (f ∘ g) (ε (f x))) ∙ cong f (η x) + ≡⟨ cong (λ a → a ∙ cong f (η x)) (lCancel (cong (f ∘ g) (ε (f x)))) ⟩ + refl ∙ cong f (η x) + ≡⟨ sym (lUnit (cong f (η x))) ⟩ + cong f (η x) ∎) diff --git a/Cubical/Foundations/Isomorphism.agda b/Cubical/Foundations/Isomorphism.agda index 78016352c4..ff899fddb1 100644 --- a/Cubical/Foundations/Isomorphism.agda +++ b/Cubical/Foundations/Isomorphism.agda @@ -105,3 +105,26 @@ compIso (iso fun inv rightInv leftInv) (iso fun₁ inv₁ rightInv₁ leftInv₁ = cong fun₁ (rightInv (inv₁ b)) ∙ (rightInv₁ b) compIso (iso fun inv rightInv leftInv) (iso fun₁ inv₁ rightInv₁ leftInv₁) .Iso.leftInv a = cong inv (leftInv₁ (fun a) ) ∙ leftInv a + +idIso : ∀ {ℓ} {X : Type ℓ} → Iso X X +Iso.fun (idIso {X = X}) = idfun X +Iso.inv (idIso {X = X}) = idfun X +Iso.rightInv (idIso {X = X}) x = refl {x = x} +Iso.leftInv (idIso {X = X}) x = refl {x = x} + +-- Helpful notation +_Iso⟨_⟩_ : ∀ {ℓ ℓ' ℓ''} {B : Type ℓ'} {C : Type ℓ''} (X : Type ℓ) → Iso X B → Iso B C → Iso X C +_ Iso⟨ f ⟩ g = compIso f g + +_∎Iso : ∀ {ℓ} (X : Type ℓ) → Iso X X +X ∎Iso = idIso {X = X} + +infixr 0 _Iso⟨_⟩_ +infix 1 _∎Iso + +invIso : ∀ {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'} → Iso X Y → Iso Y X +Iso.fun (invIso isom) = Iso.inv isom +Iso.inv (invIso isom) = Iso.fun isom +Iso.rightInv (invIso isom) = Iso.leftInv isom +Iso.leftInv (invIso isom) = Iso.rightInv isom + diff --git a/Cubical/Functions/Embedding.agda b/Cubical/Functions/Embedding.agda index cafa849464..620d571f29 100644 --- a/Cubical/Functions/Embedding.agda +++ b/Cubical/Functions/Embedding.agda @@ -8,6 +8,7 @@ open import Cubical.Foundations.Equiv open import Cubical.Foundations.HLevels open import Cubical.Foundations.Transport open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence using (ua) private variable @@ -132,3 +133,19 @@ isEquiv→hasPropFibers e b = isContr→isProp (equiv-proof e b) isEquiv→isEmbedding : isEquiv f → isEmbedding f isEquiv→isEmbedding e = hasPropFibers→isEmbedding (isEquiv→hasPropFibers e) + +iso→isEmbedding : ∀ {ℓ} {A B : Type ℓ} + → (isom : Iso A B) + ------------------------------- + → isEmbedding (Iso.fun isom) +iso→isEmbedding {A = A} {B} isom = (isEquiv→isEmbedding (equivIsEquiv (isoToEquiv isom))) + +isEmbedding→Injection : + ∀ {ℓ} {A B C : Type ℓ} + → (a : A -> B) + → (e : isEmbedding a) + ---------------------- + → ∀ {f g : C -> A} -> + ∀ x → (a (f x) ≡ a (g x)) ≡ (f x ≡ g x) +isEmbedding→Injection a e {f = f} {g} x = sym (ua (cong a , e (f x) (g x))) + diff --git a/Cubical/Functions/Fibration.agda b/Cubical/Functions/Fibration.agda index fb91631a47..245e101a48 100644 --- a/Cubical/Functions/Fibration.agda +++ b/Cubical/Functions/Fibration.agda @@ -70,6 +70,6 @@ module _ {ℓb} (B : Type ℓb) (ℓ : Level) where fiber≡ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {b : B} (h h' : fiber f b) → (h ≡ h') ≡ fiber (cong f) (h .snd ∙∙ refl ∙∙ sym (h' .snd)) fiber≡ {f = f} h h' = - ua Σ≡ ⁻¹ ∙ + Σ≡ ⁻¹ ∙ cong (Σ (h .fst ≡ h' .fst)) (funExt λ p → flipSquarePath ∙ PathP≡doubleCompPathʳ _ _ _ _) diff --git a/Cubical/Functions/FunExtEquiv.agda b/Cubical/Functions/FunExtEquiv.agda index 5da3708a70..7a4a71e972 100644 --- a/Cubical/Functions/FunExtEquiv.agda +++ b/Cubical/Functions/FunExtEquiv.agda @@ -31,6 +31,8 @@ module _ {A : Type ℓ} {B : A → Type ℓ₁} {f g : (x : A) → B x} where funExtPath : (∀ x → f x ≡ g x) ≡ (f ≡ g) funExtPath = ua funExtEquiv + funExtIso : Iso (∀ x → f x ≡ g x) (f ≡ g) + funExtIso = iso funExt funExt⁻ (λ x → refl {x = x}) (λ x → refl {x = x}) -- Function extensionality for binary functions funExt₂ : {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂} diff --git a/Cubical/HITs/KleinBottle/Properties.agda b/Cubical/HITs/KleinBottle/Properties.agda index 500431b786..0d6e21c50f 100644 --- a/Cubical/HITs/KleinBottle/Properties.agda +++ b/Cubical/HITs/KleinBottle/Properties.agda @@ -120,7 +120,7 @@ isGroupoidKleinBottle = Path KleinBottle point point ≡⟨ (λ i → basePath i ≡ basePath i) ⟩ Path (Σ S¹ invS¹Loop) (base , base) (base , base) - ≡⟨ sym (ua Σ≡) ⟩ + ≡⟨ sym Σ≡ ⟩ Σ ΩS¹ (λ p → PathP (λ j → invS¹Loop (p j)) base base) ≡⟨ (λ i → Σ ΩS¹ (λ p → PathP (λ j → invS¹Loop (p (j ∨ i))) (twistBaseLoop (p i)) base)) ⟩ ΩS¹ × ΩS¹