import Equality.Path as P
module Lens.Non-dependent.Higher.Coherently.Not-coinductive
{e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where
open P.Derived-definitions-and-properties eq
open import Prelude
open import Container.Indexed equality-with-J
open import Container.Indexed.M.Function equality-with-J
open import H-level.Truncation.Propositional.One-step eq using (∥_∥¹)
private
variable
a b p : Level
Coherently-container :
{B : Type b}
(P : {A : Type a} → (A → B) → Type p)
(step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B) →
Container (∃ λ (A : Type a) → A → B) p lzero
Coherently-container P step = λ where
.Shape (_ , f) → P f
.Position _ → ⊤
.index {o = A , f} {s = p} _ → ∥ A ∥¹ , step f p
Coherently :
{A : Type a} {B : Type b}
(P : {A : Type a} → (A → B) → Type p)
(step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B) →
(f : A → B) →
Type (lsuc a ⊔ b ⊔ p)
Coherently P step f =
M (Coherently-container P step) (_ , f)