------------------------------------------------------------------------
-- The coinductive type family Coherently
------------------------------------------------------------------------

-- This type family is used to define the lenses in
-- Lens.Non-dependent.Higher.Coinductive and
-- Lens.Non-dependent.Higher.Coinductive.Small.

{-# OPTIONS --cubical --guardedness #-}

import Equality.Path as P

module Lens.Non-dependent.Higher.Coherently.Coinductive
  {e⁺} (eq :  {a p}  P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

import Equality.Path.Univalence as EPU
open import Prelude

open import Bijection equality-with-J as B using (_↔_)
import Bijection P.equality-with-J as PB
open import Container.Indexed equality-with-J
open import Container.Indexed.Coalgebra equality-with-J
open import Container.Indexed.M.Codata eq
import Container.Indexed.M.Function equality-with-J as F
open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
  using () renaming (opaque-univ to univ)
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence P.equality-with-J as PEq
import Extensionality P.equality-with-J as PExt
open import Function-universe equality-with-J hiding (id; _∘_)
import Function-universe P.equality-with-J as PF
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹; ∣_∣)
open import Univalence-axiom equality-with-J
import Univalence-axiom P.equality-with-J as PU

import Lens.Non-dependent.Higher.Coherently.Not-coinductive eq as NC

private
  variable
    a b  p p₁ p₂ : Level
    A A₁ A₂ B C   : Type a
    f q x y       : A
    n             : 

------------------------------------------------------------------------
-- The type family

-- Coherently P step f means that f and all variants of f built using
-- step (in a certain way) satisfy the property P.
--
-- Paolo Capriotti came up with a coinductive definition of lenses.
-- Andrea Vezzosi suggested that one could use a kind of indexed
-- M-type to make it easier to prove that two variants of coinductive
-- lenses are equivalent: the lemma Coherently-cong-≡ below is based
-- on his idea, and Coherently is a less general variant of the M-type
-- that he suggested. See also Coherently-with-restriction′ below,
-- which is defined as an indexed M-type.

record 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 p where
  coinductive
  field
    property : P f
    coherent : Coherently P step (step f property)

open Coherently public

------------------------------------------------------------------------
-- An equivalence

-- Coherently is pointwise equivalent to NC.Coherently.

Coherently≃Not-coinductive-coherently :
  {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} 
  Coherently P step f  NC.Coherently P step f
Coherently≃Not-coinductive-coherently
  {a = a} {B = B} {P = P} {step = step} {f = f} =
  block λ b 

  Coherently P step f     ↝⟨ Eq.↔→≃ to from
                               (_↔_.from ≡↔≡  to-from)
                               (_↔_.from ≡↔≡  from-to) 
  M (CC step) (_ , f)     ↝⟨ carriers-of-final-coalgebras-equivalent
                               (M-coalgebra (CC step) , M-final univ univ)
                               (F.M-coalgebra b ext (CC step) , F.M-final b ext ext)
                               _ 
  F.M (CC step) (_ , f)   ↔⟨⟩
  NC.Coherently P step f  
  where
  CC = NC.Coherently-container P

  to :
    {step : {A : Type a} (f : A  B)  P f   A ∥¹  B} {f : A  B} 
    Coherently P step f  M (CC step) (_ , f)
  to c .out-M .proj₁   = c .property
  to c .out-M .proj₂ _ = to (c .coherent)

  from :
    {step : {A : Type a} (f : A  B)  P f   A ∥¹  B} {f : A  B} 
    M (CC step) (_ , f)  Coherently P step f
  from c .property = c .out-M .proj₁
  from c .coherent = from (c .out-M .proj₂ _)

  to-from :
    {step : {A : Type a} (f : A  B)  P f   A ∥¹  B} {f : A  B} 
    (c : M (CC step) (_ , f)) 
    to (from c) P.≡ c
  to-from c i .out-M .proj₁   = c .out-M .proj₁
  to-from c i .out-M .proj₂ _ = to-from (c .out-M .proj₂ _) i

  from-to :
    {step : {A : Type a} (f : A  B)  P f   A ∥¹  B} {f : A  B} 
    (c : Coherently P step f) 
    from (to c) P.≡ c
  from-to c i .property = c .property
  from-to c i .coherent = from-to (c .coherent) i

------------------------------------------------------------------------
-- Preservation lemmas

private opaque

  -- A preservation lemma for Coherently.

  Coherently-cong-≡ :
    {P₁ P₂ : {A : Type a}  (A  B)  Type p}
    {step₁ : {A : Type a} (f : A  B)  P₁ f   A ∥¹  B}
    {step₂ : {A : Type a} (f : A  B)  P₂ f   A ∥¹  B}
    (P₁≃P₂ : {A : Type a} (f : A  B)  P₁ f  P₂ f) 
    ({A : Type a} (f : A  B) (x : P₂ f) 
     step₁ f (_≃_.from (P₁≃P₂ f) x)  step₂ f x) 
    Coherently P₁ step₁ f P.≡ Coherently P₂ step₂ f
  Coherently-cong-≡
    {a = a} {B = B} {p = p} {f = f} {P₁ = P₁} {P₂ = P₂}
    {step₁ = step₁} {step₂ = step₂} P₁≃P₂′ step₁≡step₂ =

    P.cong  ((P , step) :
               λ (P : (A : Type a)  (A  B)  Type p) 
                  {A : Type a} (f : A  B)  P A f   A ∥¹  B) 
             Coherently (P _) step f) $

    P.Σ-≡,≡→≡′

      (P.⟨ext⟩ λ A  P.⟨ext⟩ λ (f : A  B) 
       EPU.≃⇒≡ (P₁≃P₂ f))

      (PExt.implicit-extensionality P.ext λ A  P.⟨ext⟩ λ f 
         P.subst  P  {A : Type a} (f : A  B)  P A f   A ∥¹  B)
           (P.⟨ext⟩ λ A  P.⟨ext⟩ λ (f : A  B) 
            EPU.≃⇒≡ (P₁≃P₂ f))
           step₁ f                                                      P.≡⟨ P.trans (P.cong (_$ f) $ P.sym $
                                                                                      P.push-subst-implicit-application
                                                                                        (P.⟨ext⟩ λ A  P.⟨ext⟩ λ (f : A  B)  EPU.≃⇒≡ (P₁≃P₂ f))
                                                                                         P A  (f : A  B)  P A f   A ∥¹  B)
                                                                                        {f = const _} {g = step₁}) $
                                                                             P.sym $ P.push-subst-application
                                                                                       (P.⟨ext⟩ λ A  P.⟨ext⟩ λ (f : A  B)  EPU.≃⇒≡ (P₁≃P₂ f))
                                                                                        P f  P A f   A ∥¹  B)
                                                                                       {f = const f} {g = step₁} 
         P.subst  P  P A f   A ∥¹  B)
           (P.⟨ext⟩ λ A  P.⟨ext⟩ λ (f : A  B) 
            EPU.≃⇒≡ (P₁≃P₂ f))
           (step₁ f)                                                    P.≡⟨⟩

         P.subst  P  P   A ∥¹  B)
           (EPU.≃⇒≡ (P₁≃P₂ f))
           (step₁ f)                                                    P.≡⟨ P.sym $
                                                                             PU.transport-theorem
                                                                                P  P   A ∥¹  B)
                                                                               (PF.→-cong₁ _)
                                                                                _  P.refl)
                                                                               EPU.univ
                                                                               (P₁≃P₂ f)
                                                                               (step₁ f) 
         PF.→-cong₁ _ (P₁≃P₂ f) (step₁ f)                               P.≡⟨⟩

         step₁ f  PEq._≃_.from (P₁≃P₂ f)                               P.≡⟨ P.⟨ext⟩ (_↔_.to ≡↔≡  step₁≡step₂ f) ⟩∎

         step₂ f                                                        )
    where
    P₁≃P₂ : (f : A  B)  P₁ f PEq.≃ P₂ f
    P₁≃P₂ f = _↔_.to ≃↔≃ (P₁≃P₂′ f)

private opaque
  unfolding Coherently-cong-≡

  -- A "computation rule".

  to-Coherently-cong-≡-property :
    {P₁ P₂ : {A : Type a}  (A  B)  Type p}
    {step₁ : {A : Type a} (f : A  B)  P₁ f   A ∥¹  B}
    {step₂ : {A : Type a} (f : A  B)  P₂ f   A ∥¹  B}
    (P₁≃P₂ : {A : Type a} (f : A  B)  P₁ f  P₂ f)
    (step₁≡step₂ :
       {A : Type a} (f : A  B) (x : P₂ f) 
       step₁ f (_≃_.from (P₁≃P₂ f) x)  step₂ f x)
    (c : Coherently P₁ step₁ f) 
    PU.≡⇒→ (Coherently-cong-≡ P₁≃P₂ step₁≡step₂) c .property P.≡
    _≃_.to (P₁≃P₂ f) (c .property)
  to-Coherently-cong-≡-property
    {f = f} {P₁ = P₁} {P₂ = P₂} P₁≃P₂ step₁≡step₂ c =

    P.transport  _  P₂ f) P.0̲
      (_≃_.to (P₁≃P₂ f) (P.transport  _  P₁ f) P.0̲ (c .property)))  P.≡⟨ P.cong (_$ _≃_.to (P₁≃P₂ f)
                                                                                             (P.transport  _  P₁ f) P.0̲ (c .property))) $
                                                                                P.transport-refl P.0̲ 

    _≃_.to (P₁≃P₂ f) (P.transport  _  P₁ f) P.0̲ (c .property))      P.≡⟨ P.cong  g  _≃_.to (P₁≃P₂ f) (g (c .property))) $
                                                                                P.transport-refl P.0̲ ⟩∎
    _≃_.to (P₁≃P₂ f) (c .property)                                     

private opaque
  unfolding Coherently-cong-≡

  -- Another "computation rule".

  from-Coherently-cong-≡-property :
    {P₁ P₂ : {A : Type a}  (A  B)  Type p}
    {step₁ : {A : Type a} (f : A  B)  P₁ f   A ∥¹  B}
    {step₂ : {A : Type a} (f : A  B)  P₂ f   A ∥¹  B}
    (P₁≃P₂ : {A : Type a} (f : A  B)  P₁ f  P₂ f)
    (step₁≡step₂ :
       {A : Type a} (f : A  B) (x : P₂ f) 
       step₁ f (_≃_.from (P₁≃P₂ f) x)  step₂ f x)
    (c : Coherently P₂ step₂ f) 
    PEq._≃_.from
      (PU.≡⇒≃ (Coherently-cong-≡ {step₁ = step₁} P₁≃P₂ step₁≡step₂))
      c .property P.≡
    _≃_.from (P₁≃P₂ f) (c .property)
  from-Coherently-cong-≡-property
    {f = f} {P₁ = P₁} {P₂ = P₂} P₁≃P₂ step₁≡step₂ c =

    P.transport  _  P₁ f) P.0̲
      (_≃_.from (P₁≃P₂ f) (P.transport  _  P₂ f) P.0̲ (c .property)))  P.≡⟨ P.cong (_$ _≃_.from (P₁≃P₂ f)
                                                                                           (P.transport  _  P₂ f) P.0̲ (c .property))) $
                                                                              P.transport-refl P.0̲ 

    _≃_.from (P₁≃P₂ f) (P.transport  _  P₂ f) P.0̲ (c .property))      P.≡⟨ P.cong  g  _≃_.from (P₁≃P₂ f) (g (c .property))) $
                                                                              P.transport-refl P.0̲ ⟩∎
    _≃_.from (P₁≃P₂ f) (c .property)                                     

private

  -- A preservation lemma for Coherently.
  --
  -- The two directions of this equivalence compute the property
  -- fields in certain ways, see the "unit tests" below.
  --
  -- Note that P₁ and P₂ have to target the same universe. A more
  -- general result is given below (Coherently-cong).

  Coherently-cong-≃ :
    {P₁ P₂ : {A : Type a}  (A  B)  Type p}
    {step₁ : {A : Type a} (f : A  B)  P₁ f   A ∥¹  B}
    {step₂ : {A : Type a} (f : A  B)  P₂ f   A ∥¹  B}
    (P₁≃P₂ : {A : Type a} (f : A  B)  P₁ f  P₂ f) 
    ({A : Type a} (f : A  B) (x : P₂ f) 
     step₁ f (_≃_.from (P₁≃P₂ f) x)  step₂ f x) 
    Coherently P₁ step₁ f  Coherently P₂ step₂ f
  Coherently-cong-≃
    {f = f} {P₁ = P₁} {P₂ = P₂} {step₁ = step₁} {step₂ = step₂}
    P₁≃P₂ step₁≡step₂ =

    Eq.with-other-inverse
      (Eq.with-other-function equiv to (_↔_.from ≡↔≡  ≡to))
      from
      (_↔_.from ≡↔≡  ≡from)

    where

    equiv : Coherently P₁ step₁ f  Coherently P₂ step₂ f
    equiv =
      _↔_.from ≃↔≃ $ PU.≡⇒≃ $
      Coherently-cong-≡ P₁≃P₂ step₁≡step₂

    to : Coherently P₁ step₁ f  Coherently P₂ step₂ f
    to c .property = _≃_.to (P₁≃P₂ f) (c .property)
    to c .coherent =
      P.subst
        (Coherently P₂ step₂)
        (P.cong (step₂ f) $
         to-Coherently-cong-≡-property P₁≃P₂ step₁≡step₂ c) $
      _≃_.to equiv c .coherent

    ≡to :  c  _≃_.to equiv c P.≡ to c
    ≡to c i .property = to-Coherently-cong-≡-property
                          P₁≃P₂ step₁≡step₂ c i
    ≡to c i .coherent = lemma i
      where
      lemma :
        P.[  i  Coherently P₂ step₂
                     (step₂ f
                        (to-Coherently-cong-≡-property
                           P₁≃P₂ step₁≡step₂ c i))) ]
          _≃_.to equiv c .coherent 
          P.subst
            (Coherently P₂ step₂)
            (P.cong (step₂ f) $
             to-Coherently-cong-≡-property P₁≃P₂ step₁≡step₂ c)
            (_≃_.to equiv c .coherent)
      lemma =
        PB._↔_.from (P.heterogeneous↔homogeneous _) P.refl

    from :
      Coherently P₂ step₂ f  Coherently P₁ step₁ f
    from c .property = _≃_.from (P₁≃P₂ f) (c .property)
    from c .coherent =
      P.subst
        (Coherently P₁ step₁)
        (P.cong (step₁ f) $
         from-Coherently-cong-≡-property P₁≃P₂ step₁≡step₂ c) $
      _≃_.from equiv c .coherent

    ≡from :  c  _≃_.from equiv c P.≡ from c
    ≡from c i .property = from-Coherently-cong-≡-property
                            P₁≃P₂ step₁≡step₂ c i
    ≡from c i .coherent = lemma i
      where
      lemma :
        P.[  i  Coherently P₁ step₁
                     (step₁ f
                        (from-Coherently-cong-≡-property
                           P₁≃P₂ step₁≡step₂ c i))) ]
          _≃_.from equiv c .coherent 
          P.subst
            (Coherently P₁ step₁)
            (P.cong (step₁ f) $
             from-Coherently-cong-≡-property P₁≃P₂ step₁≡step₂ c)
            (_≃_.from equiv c .coherent)
      lemma =
        PB._↔_.from (P.heterogeneous↔homogeneous _) P.refl

  -- Unit tests that ensure that Coherently-cong-≃ computes the
  -- property fields in certain ways.

  module _
    {P₁ P₂ : {A : Type a}  (A  B)  Type p}
    {step₁ : {A : Type a} (f : A  B)  P₁ f   A ∥¹  B}
    {step₂ : {A : Type a} (f : A  B)  P₂ f   A ∥¹  B}
    {P₁≃P₂ : {A : Type a} (f : A  B)  P₁ f  P₂ f}
    {step₁≡step₂ :
       {A : Type a} (f : A  B) (x : P₂ f) 
       step₁ f (_≃_.from (P₁≃P₂ f) x)  step₂ f x}
    where

    _ :
      {c : Coherently P₁ step₁ f} 
      _≃_.to (Coherently-cong-≃ P₁≃P₂ step₁≡step₂) c .property 
      _≃_.to (P₁≃P₂ f) (c .property)
    _ = refl _

    _ :
      {c : Coherently P₂ step₂ f} 
      _≃_.from (Coherently-cong-≃ {step₁ = step₁} P₁≃P₂ step₁≡step₂)
        c .property 
      _≃_.from (P₁≃P₂ f) (c .property)
    _ = refl _

  -- A lemma involving Coherently and ↑.

  Coherently-↑ :
    {P : {A : Type a}  (A  B)  Type p}
    {step : {A : Type a} (f : A  B)  P f   A ∥¹  B} 
    Coherently (   P) ((_∘ lower)  step) f 
    Coherently P step f
  Coherently-↑ { = } {P = P} {step = step} =
    Eq.↔→≃
      to
      from
      (_↔_.from ≡↔≡  to-from)
      (_↔_.from ≡↔≡  from-to)
    where
    to :
      Coherently (   P) ((_∘ lower)  step) f 
      Coherently P step f
    to c .property = lower (c .property)
    to c .coherent = to (c .coherent)

    from :
      Coherently P step f 
      Coherently (   P) ((_∘ lower)  step) f
    from c .property = lift (c .property)
    from c .coherent = from (c .coherent)

    to-from :
      (c : Coherently P step f) 
      to (from c) P.≡ c
    to-from c i .property = c .property
    to-from c i .coherent = to-from (c .coherent) i

    from-to :
      (c : Coherently (   P) ((_∘ lower)  step) f) 
      from (to c) P.≡ c
    from-to c i .property = c .property
    from-to c i .coherent = from-to (c .coherent) i

-- A preservation lemma for Coherently.
--
-- The two directions of this equivalence compute the property
-- fields in certain ways, see the "unit tests" below.

Coherently-cong :
  {P₁ : {A : Type a}  (A  B)  Type p₁}
  {P₂ : {A : Type a}  (A  B)  Type p₂}
  {step₁ : {A : Type a} (f : A  B)  P₁ f   A ∥¹  B}
  {step₂ : {A : Type a} (f : A  B)  P₂ f   A ∥¹  B}
  (P₁≃P₂ : {A : Type a} (f : A  B)  P₁ f  P₂ f) 
  ({A : Type a} (f : A  B) (x : P₂ f) 
   step₁ f (_≃_.from (P₁≃P₂ f) x)  step₂ f x) 
  Coherently P₁ step₁ f  Coherently P₂ step₂ f
Coherently-cong
  {p₁ = p₁} {p₂ = p₂} {f = f}
  {P₁ = P₁} {P₂ = P₂} {step₁ = step₁} {step₂ = step₂}
  P₁≃P₂ step₁≡step₂ =

  Coherently P₁ step₁ f                          ↝⟨ inverse Coherently-↑ 

  Coherently ( p₂  P₁) ((_∘ lower)  step₁) f  ↝⟨ Coherently-cong-≃
                                                       f 
     p₂ (P₁ f)                                          ↔⟨ B.↑↔ 
    P₁ f                                                 ↝⟨ P₁≃P₂ f 
    P₂ f                                                 ↔⟨ inverse B.↑↔ ⟩□
     p₁ (P₂ f)                                          )
                                                      ((_∘ lower)  step₁≡step₂) 

  Coherently ( p₁  P₂) ((_∘ lower)  step₂) f  ↝⟨ Coherently-↑ ⟩□

  Coherently P₂ step₂ f                          

-- Unit tests that ensure that Coherently-cong computes the
-- property fields in certain ways.

module _
  {P₁ : {A : Type a}  (A  B)  Type p₁}
  {P₂ : {A : Type a}  (A  B)  Type p₂}
  {step₁ : {A : Type a} (f : A  B)  P₁ f   A ∥¹  B}
  {step₂ : {A : Type a} (f : A  B)  P₂ f   A ∥¹  B}
  {P₁≃P₂ : {A : Type a} (f : A  B)  P₁ f  P₂ f}
  {step₁≡step₂ :
     {A : Type a} (f : A  B) (x : P₂ f) 
     step₁ f (_≃_.from (P₁≃P₂ f) x)  step₂ f x}
  where

  _ :
    {c : Coherently P₁ step₁ f} 
    _≃_.to (Coherently-cong P₁≃P₂ step₁≡step₂) c .property 
    _≃_.to (P₁≃P₂ f) (c .property)
  _ = refl _

  _ :
    {c : Coherently P₂ step₂ f} 
    _≃_.from (Coherently-cong {step₁ = step₁} P₁≃P₂ step₁≡step₂)
      c .property 
    _≃_.from (P₁≃P₂ f) (c .property)
  _ = refl _

-- Another preservation lemma for Coherently.

Coherently-cong′ :
  {P : {A : Type a}  (A  B)  Type p}
  {step : {A : Type a} (f : A  B)  P f   A ∥¹  B} 
  (A₁≃A₂ : A₁  A₂) 
  Coherently P step (f  _≃_.to A₁≃A₂)  Coherently P step f
Coherently-cong′ {f = f} {P = P} {step = step} A₁≃A₂ =
  ≃-elim₁ univ
     A₁≃A₂ 
       Coherently P step (f  _≃_.to A₁≃A₂) 
       Coherently P step f)
    Eq.id
    A₁≃A₂

------------------------------------------------------------------------
-- Another lemma

-- A "computation rule".

subst-Coherently-property :
   {A : C  Type a} {B : Type b}
    {P : C  {A : Type a}  (A  B)  Type p}
    {step : (c : C) {A : Type a} (f : A  B)  P c f   A ∥¹  B}
    {f : (c : C)  A c  B} {eq : x  y} {c} 
  subst  x  Coherently (P x) (step x) (f x)) eq c .property 
  subst  x  P x (f x)) eq (c .property)
subst-Coherently-property
  {P = P} {step = step} {f = f} {eq = eq} {c = c} =
  elim¹
     eq 
       subst  x  Coherently (P x) (step x) (f x)) eq c .property 
       subst  x  P x (f x)) eq (c .property))
    (subst  x  Coherently (P x) (step x) (f x)) (refl _) c .property  ≡⟨ cong property $ subst-refl _ _ 
     c .property                                                         ≡⟨ sym $ subst-refl _ _ ⟩∎
     subst  x  P x (f x)) (refl _) (c .property)                      )
    eq

------------------------------------------------------------------------
-- Coherently-with-restriction

-- A variant of Coherently. An extra predicate Q is included, so that
-- one can restrict the "f" functions (and their domains).

record Coherently-with-restriction
         {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)
         (Q : {A : Type a}  (A  B)  Type q)
         (pres : {A : Type a} {f : A  B} {p : P f} 
                 Q f  Q (step f p))
         (q : Q f) : Type p where
  coinductive
  field
    property : P f
    coherent :
      Coherently-with-restriction
        P step (step f property)
        Q pres (pres q)

open Coherently-with-restriction public

-- Coherently P step f is equivalent to
-- Coherently-with-restriction P step f Q pres q.

Coherently≃Coherently-with-restriction :
  {P : {A : Type a}  (A  B)  Type p}
  {step : {A : Type a} (f : A  B)  P f   A ∥¹  B}
  {Q : {A : Type a}  (A  B)  Type q}
  {pres : {A : Type a} {f : A  B} {p : P f}  Q f  Q (step f p)}
  {q : Q f} 
  Coherently P step f  Coherently-with-restriction P step f Q pres q
Coherently≃Coherently-with-restriction
  {P = P} {step = step} {Q = Q} {pres = pres} =
  Eq.↔→≃ to (from _)
     c  _↔_.from ≡↔≡ (to-from c))
     c  _↔_.from ≡↔≡ (from-to _ c))
  where
  to :
    Coherently P step f 
    Coherently-with-restriction P step f Q pres q
  to c .property = c .property
  to c .coherent = to (c .coherent)

  from :
     q 
    Coherently-with-restriction P step f Q pres q 
    Coherently P step f
  from _ c .property = c .property
  from _ c .coherent = from _ (c .coherent)

  to-from :
    (c : Coherently-with-restriction P step f Q pres q) 
    to (from q c) P.≡ c
  to-from c i .property = c .property
  to-from c i .coherent = to-from (c .coherent) i

  from-to :  q (c : Coherently P step f)  from q (to c) P.≡ c
  from-to _ c i .property = c .property
  from-to q c i .coherent = from-to (pres q) (c .coherent) i

-- A container that is used to define Coherently-with-restriction′.

Coherently-with-restriction-container :
  {B : Type b}
  (P : {A : Type a}  (A  B)  Type p)
  (step : {A : Type a} (f : A  B)  P f   A ∥¹  B) 
  (Q : {A : Type a}  (A  B)  Type q) 
  ({A : Type a} {f : A  B} {p : P f}  Q f  Q (step f p)) 
  Container ( λ (A : Type a)   λ (f : A  B)  Q f) p lzero
Coherently-with-restriction-container P step _ pres = λ where
  .Shape (_ , f , _)                P f
  .Position _                       
  .index {o = A , f , q} {s = p} _   A ∥¹ , step f p , pres q

-- A variant of Coherently-with-restriction, defined using an indexed
-- container.

Coherently-with-restriction′ :
  {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) 
  (Q : {A : Type a}  (A  B)  Type q) 
  ({A : Type a} {f : A  B} {p : P f}  Q f  Q (step f p)) 
  Q f 
  Type (lsuc a  b  p  q)
Coherently-with-restriction′ P step f Q pres q =
  M (Coherently-with-restriction-container P step Q pres) (_ , f , q)

-- Coherently-with-restriction P step f Q pres q is equivalent to
-- Coherently-with-restriction′ P step f Q pres q.

Coherently-with-restriction≃Coherently-with-restriction′ :
  {P : {A : Type a}  (A  B)  Type p}
  {step : {A : Type a} (f : A  B)  P f   A ∥¹  B}
  {Q : {A : Type a}  (A  B)  Type q}
  {pres : {A : Type a} {f : A  B} {p : P f}  Q f  Q (step f p)}
  {q : Q f} 
  Coherently-with-restriction P step f Q pres q 
  Coherently-with-restriction′ P step f Q pres q
Coherently-with-restriction≃Coherently-with-restriction′
  {P = P} {step = step} {Q = Q} {pres = pres} =
  Eq.↔→≃ to (from _)
     c  _↔_.from ≡↔≡ (to-from _ c))
     c  _↔_.from ≡↔≡ (from-to c))
  where
  to :
    Coherently-with-restriction P step f Q pres q 
    Coherently-with-restriction′ P step f Q pres q
  to c .out-M .proj₁   = c .property
  to c .out-M .proj₂ _ = to (c .coherent)

  from :
     q 
    Coherently-with-restriction′ P step f Q pres q 
    Coherently-with-restriction P step f Q pres q
  from _ c .property = c .out-M .proj₁
  from _ c .coherent = from _ (c .out-M .proj₂ _)

  to-from :
     q (c : Coherently-with-restriction′ P step f Q pres q) 
    to (from q c) P.≡ c
  to-from _ c i .out-M .proj₁   = c .out-M .proj₁
  to-from q c i .out-M .proj₂ _ = to-from (pres q) (c .out-M .proj₂ _) i

  from-to :
    (c : Coherently-with-restriction P step f Q pres q) 
    from q (to c) P.≡ c
  from-to c i .property = c .property
  from-to c i .coherent = from-to (c .coherent) i

------------------------------------------------------------------------
-- H-levels

-- I think that Paolo Capriotti suggested that one could prove that
-- certain instances of Coherently have certain h-levels by using the
-- result (due to Ahrens, Capriotti and Spadotti, see "Non-wellfounded
-- trees in Homotopy Type Theory") that M-types for indexed containers
-- have h-level n if all shapes have h-level n. The use of containers
-- with "restrictions" is my idea.

-- If P f has h-level n for every function f for which Q holds, then
-- Coherently-with-restriction P step f Q pres q has h-level n.

H-level-Coherently-with-restriction :
  {P : {A : Type a}  (A  B)  Type p}
  {step : {A : Type a} (f : A  B)  P f   A ∥¹  B}
  {Q : {A : Type a}  (A  B)  Type q}
  {pres : {A : Type a} {f : A  B} {p : P f}  Q f  Q (step f p)}
  {q : Q f} 
  ({A : Type a} {f : A  B}  Q f  H-level n (P f)) 
  H-level n (Coherently-with-restriction P step f Q pres q)
H-level-Coherently-with-restriction
  {B = B} {f = f} {n = n} {P = P} {step = step} {Q = Q}
  {pres = pres} {q = q} =

  (∀ {A} {f : A  B}  Q f  H-level n (P f))                        ↝⟨  h (_ , _ , q)  h q) 
  (((_ , f , _) :  λ A   λ (f : A  B)  Q f)  H-level n (P f))  ↝⟨  h  H-level-M univ univ h) 
  H-level n (Coherently-with-restriction′ P step f Q pres q)         ↝⟨ H-level-cong _ n
                                                                          (inverse Coherently-with-restriction≃Coherently-with-restriction′) ⟩□
  H-level n (Coherently-with-restriction P step f Q pres q)          

-- If P f has h-level n, and (for any f and p) P (step f p) has
-- h-level n when P f has h-level n, then Coherently P step f has
-- h-level n.

H-level-Coherently :
  {P : {A : Type a}  (A  B)  Type p}
  {step : {A : Type a} (f : A  B)  P f   A ∥¹  B} 
  H-level n (P f) 
  ({A : Type a} {f : A  B} {p : P f} 
   H-level n (P f)  H-level n (P (step f p))) 
  H-level n (Coherently P step f)
H-level-Coherently {n = n} {f = f} {P = P} {step = step} h₁ h₂ =
                                            $⟨ H-level-Coherently-with-restriction id 
  H-level n
    (Coherently-with-restriction P step f
        f  H-level n (P f)) h₂ h₁)       ↝⟨ H-level-cong _ n (inverse Coherently≃Coherently-with-restriction)  (_  _) ⟩□

  H-level n (Coherently P step f)           

-- A variant of H-level-Coherently for type-valued functions.

H-level-Coherently-→Type :
  {P : {A : Type a}  (A  Type f)  Type p}
  {step : {A : Type a} (F : A  Type f)  P F   A ∥¹  Type f}
  {F : A  Type f} 
  ((a : A)  H-level n (F a)) 
  ({A : Type a} {F : A  Type f} 
   ((a : A)  H-level n (F a))  H-level n (P F)) 
  ({A : Type a} {F : A  Type f} {p : P F} 
   ((a : A)  H-level n (F a)) 
   (a : A)  H-level n (step F p  a )) 
  H-level n (Coherently P step F)
H-level-Coherently-→Type
  {a = a} {f = f} {n = n} {P = P} {step = step} {F = F} h₁ h₂ h₃ =
                                              $⟨ H-level-Coherently-with-restriction h₂ 
  H-level n
    (Coherently-with-restriction P step F
        F   a  H-level n (F a)) h₃′ h₁)  ↝⟨ H-level-cong _ n (inverse Coherently≃Coherently-with-restriction)  (_  _) ⟩□

  H-level n (Coherently P step F)             
  where
  h₃′ :
    {F : A  Type f} {p : P F} 
    ((a : A)  H-level n (F a)) 
    (a :  A ∥¹)  H-level n (step F p a)
  h₃′ h = O.elim λ where
    .O.∣∣ʳ               h₃ h
    .O.∣∣-constantʳ _ _  H-level-propositional ext n _ _