text:
module Control.Monad.Free.Quotiented where

open import Prelude
open import Data.List hiding (map)
open import Data.Fin.Sigma
open import Algebra

postulate
  uip : isSet A

--------------------------------------------------------------------------------
-- Some functors
--------------------------------------------------------------------------------

private variable
  F : Type a → Type a
  G : Type b → Type b

--------------------------------------------------------------------------------
-- A free monad without any quotients: this can be treated as the "syntax tree"
-- for the later proper free monad.
--------------------------------------------------------------------------------

data Syntax (F : Type a → Type a) (A : Type a) : Type (ℓsuc a) where
  lift   : (Fx : F A) → Syntax F A
  return : (x  : A) → Syntax F A
  _>>=_  : (xs : Syntax F B) → (k : B → Syntax F A) → Syntax F A
--                        ^
--                        This needs to be a set. So apparently, everything does

module RawMonadSyntax where
  _>>_ : Syntax F A → Syntax F B → Syntax F B
  xs >> ys = xs >>= const ys

--------------------------------------------------------------------------------
-- Quotients for functors
--------------------------------------------------------------------------------

-- All of these quotients are defined on syntax trees, since otherwise we get a
-- cyclic dependency.
record Equation (Σ : Type a → Type a) (ν : Type a) : Type (ℓsuc a) where
  constructor _⊜_
  field lhs rhs : Syntax Σ ν
open Equation public

record Law (F : Type a → Type a) : Type (ℓsuc a) where
  constructor _↦_⦂_
  field
    Γ : Type a
    ν : Type a
    eqn : Γ → Equation F ν
open Law public

Theory : (Type a → Type a) → Type (ℓsuc a)
Theory Σ = List (Law Σ)

private variable 𝒯 : Theory F

Quotiented : Theory F → (∀ {ν} → Syntax F ν → Syntax F ν → Type b) → Type _
Quotiented 𝒯 R =
      (i : Fin (length 𝒯)) → -- An index into the list of equations
      let Γ ↦ ν ⦂ 𝓉 = 𝒯 !! i in -- one of the equations in the list
      (γ : Γ) → -- The environment, basically the needed things for the equation
      R (lhs (𝓉 γ)) (rhs (𝓉 γ))

--------------------------------------------------------------------------------
-- The free monad, quotiented over a theory
--------------------------------------------------------------------------------
mutual
  data Free (F : Type a → Type a) (𝒯 : Theory F) : Type a → Type (ℓsuc a) where
  -- The first three constructors are the same as the syntax type
    lift   : (Fx : F A) → Free F 𝒯 A
    return : (x  : A) → Free F 𝒯 A
    _>>=_  : (xs : Free F 𝒯 B) → (k : B → Free F 𝒯 A) → Free F 𝒯 A

  -- The quotients for the monad laws

    >>=-idˡ   :  (f : B → Free F 𝒯 A) (x : B) → (return x >>= f) ≡ f x
    >>=-idʳ   :  (x : Free F 𝒯 A) → (x >>= return) ≡ x
    >>=-assoc : (xs : Free F 𝒯 C) (f : C → Free F 𝒯 B) (g : B → Free F 𝒯 A) →
                ((xs >>= f) >>= g) ≡ (xs >>= (λ x → f x >>= g))

  -- This is the quotient for the theory.
    quot : Quotiented 𝒯 (λ lhs rhs → ∣ lhs ∣↑ ≡ ∣ rhs ∣↑)

  -- This converts from the unquotiented syntax to the free type.
  -- You cannot go the other way!
  -- The fact that we're doing all this conversion is what makes things trickier
  -- later (and also that this is interleaved with the data definition).
  ∣_∣↑ : Syntax F A → Free F 𝒯 A
  ∣ lift x   ∣↑ = lift x
  ∣ return x ∣↑ = return x
  ∣ xs >>= k ∣↑ = ∣ xs ∣↑ >>= (∣_∣↑ ∘ k)

module FreeMonadSyntax where
  _>>_ : Free F 𝒯 A → Free F 𝒯 B → Free F 𝒯 B
  xs >> ys = xs >>= const ys

--------------------------------------------------------------------------------
-- Recursion Schemes
--------------------------------------------------------------------------------

private variable
  p : Level
  P : ∀ T → Free F 𝒯 T → Type p

-- The functor for a free monad (not really! This is a "raw" free functor)
data FreeF (F : Type a → Type a)
           (𝒯 : Theory F)
           (P : ∀ T → Free F 𝒯 T → Type b)
           (A : Type a) : Type (ℓsuc a ℓ⊔ b) where
  liftF : (Fx : F A) → FreeF F 𝒯 P A
  returnF : (x : A) → FreeF F 𝒯 P A
  bindF : (xs : Free F 𝒯 B)
          (P⟨xs⟩ : P B xs)
          (k : B → Free F 𝒯 A)
          (P⟨∘k⟩ : ∀ x → P A (k x)) → FreeF F 𝒯 P A

-- There can also be a quotiented free functor (I think)

-- The "in" function
⟪_⟫ : FreeF F 𝒯 P A → Free F 𝒯 A
⟪ liftF x ⟫ = lift x
⟪ returnF x ⟫ = return x
⟪ bindF xs P⟨xs⟩ k P⟨∘k⟩ ⟫ = xs >>= k

-- An algebra
Alg : (F : Type a → Type a) → (𝒯 : Theory F) → (P : ∀ T → Free F 𝒯 T → Type b) → Type _
Alg F 𝒯 P = ∀ {A} → (xs : FreeF F 𝒯 P A) → P A ⟪ xs ⟫

-- You can run a non-coherent algebra on a syntax tree
⟦_⟧↑ : Alg F 𝒯 P → (xs : Syntax F A) → P A ∣ xs ∣↑
⟦ alg ⟧↑ (lift x) = alg (liftF x)
⟦ alg ⟧↑ (return x) = alg (returnF x)
⟦ alg ⟧↑ (xs >>= k) = alg (bindF ∣ xs ∣↑ (⟦ alg ⟧↑ xs) (∣_∣↑ ∘ k) (⟦ alg ⟧↑ ∘ k))

-- Coherency for an algebra: an algebra that's coherent can be run on a proper
-- Free monad.
record Coherent {a p}
                {F : Type a → Type a}
                {𝒯 : Theory F}
                {P : ∀ T → Free F 𝒯 T → Type p}
                (ψ : Alg F 𝒯 P) : Type (ℓsuc a ℓ⊔ p) where
  field
    c->>=idˡ : ∀ (f : A → Free F 𝒯 B) Pf x →
      ψ (bindF (return x) (ψ (returnF x)) f Pf)
        ≡[ i ≔ P _ (>>=-idˡ f x i) ]≡ Pf x

    c->>=idʳ : ∀ (x : Free F 𝒯 A) Px →
      ψ (bindF x Px return (λ y → ψ (returnF y)))
        ≡[ i ≔ P A (>>=-idʳ x i) ]≡ Px

    c->>=assoc : ∀
      (xs : Free F 𝒯 C) Pxs
      (f : C → Free F 𝒯 B) Pf
      (g : B → Free F 𝒯 A) Pg →
      ψ (bindF (xs >>= f) (ψ (bindF xs Pxs f Pf)) g Pg)
        ≡[ i ≔ P A (>>=-assoc xs f g i) ]≡
          ψ (bindF xs Pxs (λ x → f x >>= g) λ x → ψ (bindF (f x) (Pf x) g Pg))

    c-quot : (i : Fin (length 𝒯)) →
             let Γ ↦ ν ⦂ 𝓉 = 𝒯 !! i in
             (γ : Γ) →
             ⟦ ψ ⟧↑ (lhs (𝓉 γ)) ≡[ j ≔ P ν (quot i γ j) ]≡ ⟦ ψ ⟧↑ (rhs (𝓉 γ))
open Coherent public

-- A full dependent algebra
Ψ : (F : Type a → Type a) (𝒯 : Theory F) (P : ∀ T → Free F 𝒯 T → Type p) → Type _
Ψ F 𝒯 P = Σ (Alg F 𝒯 P) Coherent

Ψ-syntax : (F : Type a → Type a) (𝒯 : Theory F) (P : ∀ {T} → Free F 𝒯 T → Type p) → Type _
Ψ-syntax F 𝒯 P = Ψ F 𝒯 (λ T → P {T})

syntax Ψ-syntax F 𝒯 (λ xs → P) = Ψ[ xs ⦂ F ⋆ * / 𝒯 ] ⇒ P

-- Non-dependent algebras
Φ : (F : Type a → Type a) → (𝒯 : Theory F) → (Type a → Type b) → Type _
Φ A 𝒯 B = Ψ A 𝒯 (λ T _ → B T)

syntax Φ F 𝒯 (λ A → B) = Φ[ F ⋆ A / 𝒯 ] ⇒ B

-- Running the algebra
module _ (ψ : Ψ F 𝒯 P) where
  ⟦_⟧ : (xs : Free F 𝒯 A) → P A xs

  -- We need the terminating pragma here because Agda can't see that ∣_∣↑ makes
  -- something the same size (I think)
  {-# TERMINATING #-}
  undecorate : (xs : Syntax F A) → ⟦ fst ψ ⟧↑ xs ≡ ⟦ ∣ xs ∣↑ ⟧
  undecorate (lift x) i = fst ψ (liftF x)
  undecorate (return x) i = fst ψ (returnF x)
  undecorate (xs >>= k) i =
    fst ψ
        (bindF ∣ xs ∣↑ (undecorate xs i) (λ x → ∣ k x ∣↑)
        (λ x → undecorate (k x) i))

  ⟦ lift x ⟧ = ψ .fst (liftF x)
  ⟦ return x ⟧ = ψ .fst (returnF x)
  ⟦ xs >>= k ⟧ = ψ .fst (bindF xs ⟦ xs ⟧ k (⟦_⟧ ∘ k))

  ⟦ >>=-idˡ f k i ⟧ = ψ .snd .c->>=idˡ f (⟦_⟧ ∘ f) k i
  ⟦ >>=-idʳ xs i ⟧ = ψ .snd .c->>=idʳ xs ⟦ xs ⟧ i
  ⟦ >>=-assoc xs f g i ⟧ =
    ψ .snd .c->>=assoc xs ⟦ xs ⟧ f (⟦_⟧ ∘ f) g (⟦_⟧ ∘ g) i

  ⟦ quot p e i ⟧ =
      subst₂ (PathP (λ j → P _ (quot p e j)))
              (undecorate _)
              (undecorate _)
              (ψ .snd .c-quot p e) i

-- For a proposition, use this to prove the algebra is coherent
prop-coh : {alg : Alg F 𝒯 P} → (∀ {T} → ∀ xs → isProp (P T xs)) → Coherent alg
prop-coh {P = P} P-isProp .c->>=idˡ f Pf x =
  toPathP (P-isProp (f x) (transp (λ i → P _ (>>=-idˡ f x i)) i0 _) _)
prop-coh {P = P} P-isProp .c->>=idʳ x Px =
  toPathP (P-isProp x (transp (λ i → P _ (>>=-idʳ x i)) i0 _) _)
prop-coh {P = P} P-isProp .c->>=assoc xs Pxs f Pf g Pg =
  toPathP (P-isProp (xs >>= (λ x → f x >>= g)) (transp (λ i → P _ (>>=-assoc xs f g i)) i0 _) _)
prop-coh {𝒯 = 𝒯} {P = P} P-isProp .c-quot i e =
  toPathP (P-isProp (∣ (𝒯 !! i) .eqn e .rhs ∣↑) (transp (λ j → P _ (quot i e j)) i0 _) _)

-- A more conventional catamorphism
module _ {ℓ} (fun : Functor ℓ ℓ) where
  open Functor fun using (map; 𝐹)
  module _ {B : Type ℓ} {𝒯 : Theory 𝐹} where
    module _ (ϕ : 𝐹 B → B) where
      ϕ₁ : Alg 𝐹 𝒯 λ T _ → (T → B) → B
      ϕ₁ (liftF x) h = ϕ (map h x)
      ϕ₁ (returnF x) h = h x
      ϕ₁ (bindF _ P⟨xs⟩ _ P⟨∘k⟩) h = P⟨xs⟩ (flip P⟨∘k⟩ h)

      InTheory : Type _
      InTheory = Quotiented 𝒯 λ lhs rhs → ∀ f → ⟦ ϕ₁ ⟧↑ lhs f ≡ ⟦ ϕ₁ ⟧↑ rhs f

      module _ (ϕ-coh : InTheory) where
        cata-coh : Coherent ϕ₁
        cata-coh .c->>=idˡ f Pf x = refl
        cata-coh .c->>=idʳ x Px = refl
        cata-coh .c->>=assoc xs Pxs f Pf g Pg = refl
        cata-coh .c-quot i e j f = ϕ-coh i e f j

        cata-alg : Φ[ 𝐹 ⋆ A / 𝒯 ] ⇒ ((A → B) → B)
        cata-alg = ϕ₁ , cata-coh

    cata : (A → B) → (ϕ : 𝐹 B → B) → InTheory ϕ → Free 𝐹 𝒯 A → B
    cata h ϕ coh xs = ⟦ cata-alg ϕ coh ⟧ xs h

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- Container combinators
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Indexed-container.Combinators where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id; const) renaming (_∘_ to _⊚_)
open import Prelude.Size

open import Bijection equality-with-J as Bijection using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J as F hiding (id; _∘_)

open import Indexed-container
open import Relation

-- An identity combinator.
--
-- Taken from "Indexed containers" by Altenkirch, Ghani, Hancock,
-- McBride and Morris (JFP, 2015).

id : ∀ {i} {I : Type i} → Container I I
id = (λ _ → ↑ _ ⊤) ◁ λ {i} _ i′ → i ≡ i′

-- An unfolding lemma for ⟦ id ⟧.

⟦id⟧↔ : ∀ {k ℓ x} {I : Type ℓ} {X : Rel x I} {i} →
        Extensionality? k ℓ (ℓ ⊔ x) →
        ⟦ id ⟧ X i ↝[ k ] X i
⟦id⟧↔ {X = X} {i} ext =
  ↑ _ ⊤ × (λ i′ → i ≡ i′) ⊆ X  ↔⟨ drop-⊤-left-× (λ _ → Bijection.↑↔) ⟩
  (λ i′ → i ≡ i′) ⊆ X          ↔⟨⟩
  (∀ {i′} → i ≡ i′ → X i′)     ↔⟨ Bijection.implicit-Π↔Π ⟩
  (∀ i′ → i ≡ i′ → X i′)       ↝⟨ inverse-ext? (λ ext → ∀-intro _ ext) ext ⟩□
  X i                          □

-- An unfolding lemma for ⟦ id ⟧₂.

⟦id⟧₂↔ :
  ∀ {k ℓ x} {I : Type ℓ} {X : Rel x I} →
  Extensionality? k ℓ ℓ →
  ∀ (R : ∀ {i} → Rel₂ ℓ (X i)) {i} →
  (x y : ⟦ id ⟧ X i) →

  ⟦ id ⟧₂ R (x , y)
    ↝[ k ]
  proj₁ x ≡ proj₁ y × R (proj₂ x refl , proj₂ y refl)

⟦id⟧₂↔ ext R {i} x@(s , f) y@(t , g) =

  ⟦ id ⟧₂ R (x , y)                               ↔⟨⟩

  (∃ λ (eq : s ≡ t) →
   ∀ {o} (p : i ≡ o) →
   R (f p , g (subst (λ _ → i ≡ o) eq p)))        ↔⟨ ∃-cong (λ _ → Bijection.implicit-Π↔Π) ⟩

  (∃ λ (eq : s ≡ t) →
   ∀ o (p : i ≡ o) →
   R (f p , g (subst (λ _ → i ≡ o) eq p)))        ↝⟨ ∃-cong (λ _ → inverse-ext? (λ ext → ∀-intro _ ext) ext) ⟩

  (∃ λ (eq : s ≡ t) →
   R (f refl , g (subst (λ _ → i ≡ i) eq refl)))  ↝⟨ ∃-cong (λ eq → ≡⇒↝ _ (cong (λ eq → R (f refl , g eq)) (subst-const eq))) ⟩

  s ≡ t × R (f refl , g refl)                     □

-- A second unfolding lemma for ⟦ id ⟧₂.

⟦id⟧₂≡↔ :
  ∀ {ℓ} {I : Type ℓ} {X : Rel ℓ I} {i} →
  Extensionality ℓ ℓ →
  (x y : ⟦ id ⟧ X i) →
  ⟦ id ⟧₂ (uncurry _≡_) (x , y) ↔ x ≡ y
⟦id⟧₂≡↔ ext x@(s , f) y@(t , g) =

  ⟦ id ⟧₂ (uncurry _≡_) (x , y)  ↝⟨ ⟦id⟧₂↔ ext (uncurry _≡_) x y ⟩

  s ≡ t × f refl ≡ g refl        ↔⟨ ∃-cong (λ _ → Eq.≃-≡ (Eq.↔⇒≃ $ inverse $ ∀-intro _ ext)) ⟩

  s ≡ t × (λ _ → f) ≡ (λ _ → g)  ↔⟨ ∃-cong (λ _ → Eq.≃-≡ (Eq.↔⇒≃ Bijection.implicit-Π↔Π)) ⟩

  s ≡ t × (λ {_} → f) ≡ g        ↝⟨ ≡×≡↔≡ ⟩

  x ≡ y                          □

-- A constant combinator.

const : ∀ {i} {I : Type i} → Rel i I → Container I I
const X = X ◁ λ _ _ → ⊥

-- An unfolding lemma for ⟦ const ⟧.

⟦const⟧↔ : ∀ {k ℓ y} {I : Type ℓ} X {Y : Rel y I} {i} →
           Extensionality? k ℓ (ℓ ⊔ y) →
           ⟦ const X ⟧ Y i ↝[ k ] X i
⟦const⟧↔ {k} {ℓ} {I = I} X {Y} {i} ext =
  X i × (∀ {i} → ⊥ → Y i)  ↔⟨ ∃-cong (λ _ → Bijection.implicit-Π↔Π) ⟩
  X i × (∀ i → ⊥ → Y i)    ↝⟨ ∃-cong (λ _ → ∀-cong ext λ _ → Π⊥↔⊤ (lower-extensionality? k lzero ℓ ext)) ⟩
  X i × (I → ⊤)            ↔⟨ drop-⊤-right (λ _ → →-right-zero) ⟩
  X i                      □

-- An unfolding lemma for ⟦ const ⟧₂.

⟦const⟧₂↔ :
  ∀ {k ℓ y} {I : Type ℓ} {X} {Y : Rel y I} →
  Extensionality? k ℓ ℓ →
  ∀ (R : ∀ {i} → Rel₂ ℓ (Y i)) {i}
  (x y : ⟦ const X ⟧ Y i) →

  ⟦ const X ⟧₂ R (x , y)
    ↝[ k ]
  proj₁ x ≡ proj₁ y

⟦const⟧₂↔ {X = X} ext R x@(s , f) y@(t , g) =

  ⟦ const X ⟧₂ R (x , y)                                ↔⟨⟩

  (∃ λ (eq : s ≡ t) →
   ∀ {o} (p : ⊥) → R (f p , g (subst (λ _ → ⊥) eq p)))  ↔⟨ ∃-cong (λ _ → Bijection.implicit-Π↔Π) ⟩

  (∃ λ (eq : s ≡ t) →
   ∀ o (p : ⊥) → R (f p , g (subst (λ _ → ⊥) eq p)))    ↝⟨ ∃-cong (λ _ → ∀-cong ext λ _ → Π⊥↔⊤ ext) ⟩

  (∃ λ (eq : s ≡ t) → ∀ o → ⊤)                          ↔⟨ drop-⊤-right (λ _ → →-right-zero) ⟩

  s ≡ t                                                 □

  where
  open Container

-- A composition combinator.

infixr 9 _∘_

_∘_ : ∀ {ℓ} {I J K : Type ℓ} →
      Container J K → Container I J → Container I K
C ∘ D =
  ⟦ C ⟧ (Shape D)
    ◁
  (λ { (s , f) i →
       ∃ λ j → ∃ λ (p : Position C s j) → Position D (f p) i })
  where
  open Container

-- An unfolding lemma for ⟦ C ∘ D ⟧.

⟦∘⟧↔ : ∀ {fk ℓ x} {I J K : Type ℓ} {X : Rel x I} →
       Extensionality? fk ℓ (ℓ ⊔ x) →
       ∀ (C : Container J K) {D : Container I J} {k} →
       ⟦ C ∘ D ⟧ X k ↝[ fk ] ⟦ C ⟧ (⟦ D ⟧ X) k
⟦∘⟧↔ {X = X} ext C {D} {k} =

  ⟦ C ∘ D ⟧ X k                                                     ↔⟨⟩

  (∃ λ { (s , f) →
         ∀ {i} →
         (∃ λ j → ∃ λ (p : Position C s j) → Position D (f p) i) →
         X i })                                                     ↔⟨ inverse Σ-assoc ⟩

  (∃ λ s →
   ∃ λ (f : Position C s ⊆ Shape D) →
     ∀ {i} →
     (∃ λ j → ∃ λ (p : Position C s j) → Position D (f p) i) →
     X i)                                                           ↝⟨ (∃-cong λ _ → ∃-cong λ _ → implicit-∀-cong ext $
                                                                        from-isomorphism currying) ⟩
  (∃ λ s →
   ∃ λ (f : Position C s ⊆ Shape D) →
     ∀ {i} j →
     (∃ λ (p : Position C s j) → Position D (f p) i) →
     X i)                                                           ↔⟨ (∃-cong λ _ → ∃-cong λ _ → Bijection.implicit-Π↔Π) ⟩

  (∃ λ s →
   ∃ λ (f : Position C s ⊆ Shape D) →
     ∀ i j →
     (∃ λ (p : Position C s j) → Position D (f p) i) →
     X i)                                                           ↔⟨ (∃-cong λ _ → ∃-cong λ _ → Π-comm) ⟩

  (∃ λ s →
   ∃ λ (f : Position C s ⊆ Shape D) →
     ∀ j i →
     (∃ λ (p : Position C s j) → Position D (f p) i) →
     X i)                                                           ↔⟨ (∃-cong λ _ → ∃-cong λ _ → inverse Bijection.implicit-Π↔Π) ⟩

  (∃ λ s →
   ∃ λ (f : Position C s ⊆ Shape D) →
     ∀ {j} i →
     (∃ λ (p : Position C s j) → Position D (f p) i) →
     X i)                                                           ↔⟨ (∃-cong λ _ → inverse implicit-ΠΣ-comm) ⟩

  (∃ λ s → ∀ {j} →
   ∃ λ (f : Position C s j → Shape D j) →
     ∀ i →
     (∃ λ (p : Position C s j) → Position D (f p) i) →
     X i)                                                           ↝⟨ (∃-cong λ _ → implicit-∀-cong ext $ ∃-cong λ _ → ∀-cong ext λ _ →
                                                                        from-isomorphism currying) ⟩
  (∃ λ s → ∀ {j} →
   ∃ λ (f : Position C s j → Shape D j) →
     ∀ i → (p : Position C s j) → Position D (f p) i → X i)         ↝⟨ (∃-cong λ _ → implicit-∀-cong ext $ ∃-cong λ _ → from-isomorphism Π-comm) ⟩

  (∃ λ s → ∀ {j} →
   ∃ λ (f : Position C s j → Shape D j) →
     (p : Position C s j) → ∀ i → Position D (f p) i → X i)         ↝⟨ (∃-cong λ _ → implicit-∀-cong ext $ from-isomorphism $ inverse ΠΣ-comm) ⟩

  (∃ λ s → ∀ {j} → Position C s j →
   ∃ λ (s′ : Shape D j) → ∀ i → Position D s′ i → X i)              ↝⟨ (∃-cong λ _ → implicit-∀-cong ext $ ∀-cong ext λ _ → ∃-cong λ _ →
                                                                        from-isomorphism $ inverse Bijection.implicit-Π↔Π) ⟩
  (∃ λ s → ∀ {j} → Position C s j →
   ∃ λ (s′ : Shape D j) → Position D s′ ⊆ X)                        ↔⟨⟩

  ⟦ C ⟧ (⟦ D ⟧ X) k                                                 □

  where
  open Container

-- TODO: Define ⟦∘⟧₂↔ (an unfolding lemma for ⟦ C ∘ D ⟧₂).

-- A reindexing combinator.
--
-- Taken from "Indexed containers".

reindex₂ : ∀ {ℓ} {I O₁ O₂ : Type ℓ} →
           (O₂ → O₁) → Container I O₁ → Container I O₂
reindex₂ f (S ◁ P) = (S ⊚ f) ◁ P

-- An unfolding lemma for ⟦ reindex₂ f C ⟧.

⟦reindex₂⟧↔ : ∀ {ℓ x} {I O₁ O₂ : Type ℓ} (f : O₂ → O₁)
              (C : Container I O₁) {X : Rel x I} {o} →
              ⟦ reindex₂ f C ⟧ X o ↔ ⟦ C ⟧ X (f o)
⟦reindex₂⟧↔ f C = Bijection.id

-- An unfolding lemma for ⟦ reindex₂ f C ⟧₂.

⟦reindex₂⟧₂↔ :
  ∀ {ℓ x} {I O : Type ℓ} {X : Rel x I}
  (C : Container I O) (f : I → O) (R : ∀ {i} → Rel₂ ℓ (X i)) {i}
  (x y : ⟦ reindex₂ f C ⟧ X i) →

  ⟦ reindex₂ f C ⟧₂ R (x , y) ↔ ⟦ C ⟧₂ R (x , y)

⟦reindex₂⟧₂↔ C f R x@(s , g) y@(t , h) =

  ⟦ reindex₂ f C ⟧₂ R (x , y)                                     ↔⟨⟩

  (∃ λ (eq : s ≡ t) →
   ∀ {o} (p : Position (reindex₂ f C) s o) →
   R (g p , h (subst (λ s → Position (reindex₂ f C) s o) eq p)))  ↔⟨⟩

  (∃ λ (eq : s ≡ t) →
   ∀ {o} (p : Position C s o) →
   R (g p , h (subst (λ s → Position C s o) eq p)))               ↔⟨⟩

  ⟦ C ⟧₂ R (x , y)                                                □

  where
  open Container

-- Another reindexing combinator.

reindex₁ : ∀ {ℓ} {I₁ I₂ O : Type ℓ} →
           (I₁ → I₂) → Container I₁ O → Container I₂ O
reindex₁ f C =
  Shape C
    ◁
  (λ s i → ∃ λ i′ → f i′ ≡ i × Position C s i′)
  where
  open Container

-- An unfolding lemma for ⟦ reindex₁ f C ⟧.

⟦reindex₁⟧↔ : ∀ {k ℓ x} {I₁ I₂ O : Type ℓ} {f : I₁ → I₂} →
              Extensionality? k ℓ (ℓ ⊔ x) →
              ∀ (C : Container I₁ O) {X : Rel x I₂} {o} →
              ⟦ reindex₁ f C ⟧ X o ↝[ k ] ⟦ C ⟧ (X ⊚ f) o
⟦reindex₁⟧↔ {f = f} ext C {X} {o} =
  ⟦ reindex₁ f C ⟧ X o                                 ↔⟨ (∃-cong λ _ → Bijection.implicit-Π↔Π) ⟩

  (∃ λ (s : Shape C o) →
   ∀ i → (∃ λ i′ → f i′ ≡ i × Position C s i′) → X i)  ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → from-isomorphism currying) ⟩

  (∃ λ (s : Shape C o) →
   ∀ i i′ → f i′ ≡ i × Position C s i′ → X i)          ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ → from-isomorphism currying) ⟩

  (∃ λ (s : Shape C o) →
   ∀ i i′ → f i′ ≡ i → Position C s i′ → X i)          ↔⟨ (∃-cong λ _ → Π-comm) ⟩

  (∃ λ (s : Shape C o) →
   ∀ i i′ → f i ≡ i′ → Position C s i → X i′)          ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → inverse-ext? (λ ext → ∀-intro _ ext) ext) ⟩

  (∃ λ (s : Shape C o) →
   ∀ i → Position C s i → X (f i))                     ↔⟨ (∃-cong λ _ → inverse Bijection.implicit-Π↔Π) ⟩

  ⟦ C ⟧ (X ⊚ f) o                                      □
  where
  open Container

-- An unfolding lemma for ⟦ reindex₁ f C ⟧₂.

⟦reindex₁⟧₂↔ :
  ∀ {k ℓ x} {I O : Type ℓ} {X : Rel x O} →
  Extensionality? k ℓ ℓ →
  ∀ (C : Container I O) (f : I → O) (R : ∀ {o} → Rel₂ ℓ (X o)) {o}
  (x y : ⟦ reindex₁ f C ⟧ X o) →

  ⟦ reindex₁ f C ⟧₂ R (x , y)

    ↝[ k ]

  ⟦ C ⟧₂ R ( (proj₁ x , λ p → proj₂ x (_ , refl , p))
           , (proj₁ y , λ p → proj₂ y (_ , refl , p))
           )

⟦reindex₁⟧₂↔ ext C f R x@(s , g) y@(t , h) =

  ⟦ reindex₁ f C ⟧₂ R (x , y)                                             ↔⟨⟩

  (∃ λ (eq : s ≡ t) →
   ∀ {o} (p : ∃ λ o′ → f o′ ≡ o × Position C s o′) →
   R (g p , h (subst (λ s → ∃ λ o′ → f o′ ≡ o × Position C s o′) eq p)))  ↝⟨ (∃-cong λ eq → implicit-∀-cong ext $ ∀-cong ext λ _ →
                                                                              ≡⇒↝ _ $ cong (R ⊚ (g _ ,_) ⊚ h) $
                                                                              lemma eq) ⟩
  (∃ λ (eq : s ≡ t) →
   ∀ {o} (p : ∃ λ o′ → f o′ ≡ o × Position C s o′) →
   R ( g p
     , h ( proj₁ p
         , proj₁ (proj₂ p)
         , subst (λ s → Position C s (proj₁ p)) eq (proj₂ (proj₂ p))
         )
     ))                                                                   ↝⟨ (∃-cong λ _ → implicit-∀-cong ext $ from-isomorphism
                                                                              currying) ⟩
  (∃ λ (eq : s ≡ t) →
   ∀ {o} o′ (p : f o′ ≡ o × Position C s o′) →
   R ( g (o′ , p)
     , h (o′ , proj₁ p , subst (λ s → Position C s o′) eq (proj₂ p))
     ))                                                                   ↝⟨ (∃-cong λ _ → implicit-∀-cong ext $ ∀-cong ext λ _ → from-isomorphism
                                                                              currying) ⟩
  (∃ λ (eq : s ≡ t) →
   ∀ {o} o′ (≡o : f o′ ≡ o) (p : Position C s o′) →
   R ( g (o′ , ≡o , p)
     , h (o′ , ≡o , subst (λ s → Position C s o′) eq p)
     ))                                                                   ↔⟨ (∃-cong λ _ →
                                                                              Bijection.implicit-Π↔Π) ⟩
  (∃ λ (eq : s ≡ t) →
   ∀ o o′ (≡o : f o′ ≡ o) (p : Position C s o′) →
   R ( g (o′ , ≡o , p)
     , h (o′ , ≡o , subst (λ s → Position C s o′) eq p)
     ))                                                                   ↔⟨ (∃-cong λ _ →
                                                                              Π-comm) ⟩
  (∃ λ (eq : s ≡ t) →
   ∀ o o′ (≡o′ : f o ≡ o′) (p : Position C s o) →
   R ( g (o , ≡o′ , p)
     , h (o , ≡o′ , subst (λ s → Position C s o) eq p)
     ))                                                                   ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ →
                                                                              inverse-ext? (λ ext → ∀-intro _ ext) ext) ⟩
  (∃ λ (eq : s ≡ t) →
   ∀ o (p : Position C s o) →
   R ( g (o , refl , p)
     , h (o , refl , subst (λ s → Position C s o) eq p)
     ))                                                                   ↔⟨ (∃-cong λ _ → inverse
                                                                              Bijection.implicit-Π↔Π) ⟩
  (∃ λ (eq : s ≡ t) →
   ∀ {o} (p : Position C s o) →
   R ( g (o , refl , p)
     , h (o , refl , subst (λ s → Position C s o) eq p)
     ))                                                                   ↔⟨⟩

  ⟦ C ⟧₂ R ((s , λ p → g (_ , refl , p)) , (t , λ p → h (_ , refl , p)))  □

  where
  open Container

  lemma = λ (eq : s ≡ t) {o} {p : ∃ λ o′ → f o′ ≡ o × Position C s o′} →

    subst (λ s → ∃ λ o′ → f o′ ≡ o × Position C s o′) eq p                ≡⟨ push-subst-pair′ {y≡z = eq} _ _ (subst-const eq) ⟩

    ( proj₁ p
    , subst (λ { (s , o′) → f o′ ≡ o × Position C s o′ })
            (Σ-≡,≡→≡ eq (subst-const eq)) (proj₂ p)
    )                                                                     ≡⟨⟩

    ( proj₁ p
    , subst (λ { (s , o′) → f o′ ≡ o × Position C s o′ })
            (Σ-≡,≡→≡ eq (trans (subst-const eq) refl)) (proj₂ p)
    )                                                                     ≡⟨ cong (λ eq → _ , subst (λ { (s , o′) → f o′ ≡ o × Position C s o′ })
                                                                                eq (proj₂ p)) $
                                                                             Σ-≡,≡→≡-subst-const eq refl ⟩
    ( proj₁ p
    , subst (λ { (s , o′) → f o′ ≡ o × Position C s o′ })
            (cong₂ _,_ eq refl) (proj₂ p)
    )                                                                     ≡⟨ cong (_ ,_) $
                                                                             push-subst-, {y≡z = cong₂ _,_ eq refl}
                                                                                ((_≡ o) ⊚ f ⊚ proj₂) (uncurry (Position C)) ⟩
    ( proj₁ p
    , subst ((_≡ o) ⊚ f ⊚ proj₂)   (cong₂ _,_ eq refl) (proj₁ (proj₂ p))
    , subst (uncurry (Position C)) (cong₂ _,_ eq refl) (proj₂ (proj₂ p))
    )                                                                     ≡⟨ cong (λ eq′ → _ , eq′
                                                                                , subst (uncurry (Position C)) (cong₂ _,_ eq refl) _) $
                                                                             subst-∘ ((_≡ o) ⊚ f) proj₂ (cong₂ _,_ eq refl) ⟩
    ( proj₁ p
    , subst ((_≡ o) ⊚ f)
            (cong proj₂ (cong₂ _,_ eq refl)) (proj₁ (proj₂ p))
    , subst (uncurry (Position C)) (cong (_, _) eq) (proj₂ (proj₂ p))
    )                                                                     ≡⟨ cong₂ (λ eq₁ eq₂ → _ , subst ((_≡ o) ⊚ f) eq₁ _ , eq₂)
                                                                             (cong-proj₂-cong₂-, eq refl)
                                                                             (sym $ subst-∘ (uncurry (Position C)) (_, _) eq) ⟩
    ( proj₁ p
    , subst ((_≡ o) ⊚ f) refl (proj₁ (proj₂ p))
    , subst (uncurry (Position C) ⊚ (_, _)) eq (proj₂ (proj₂ p))
    )                                                                     ≡⟨⟩

    ( proj₁ p
    , proj₁ (proj₂ p)
    , subst (λ s → Position C s (proj₁ p)) eq (proj₂ (proj₂ p))
    )                                                                     ∎

-- A combined reindexing combinator.
--
-- The application reindex swap is similar to the overline function
-- from Section 6.3.4.1 in Pous and Sangiorgi's "Enhancements of the
-- bisimulation proof method".

reindex : ∀ {ℓ} {I O : Type ℓ} →
          (I → O) → Container I O → Container O I
reindex f = reindex₂ f ⊚ reindex₁ f

-- An unfolding lemma for ⟦ reindex f C ⟧.

⟦reindex⟧↔ : ∀ {k ℓ x} {I O : Type ℓ} {f : I → O} →
             Extensionality? k ℓ (ℓ ⊔ x) →
             ∀ (C : Container I O) {X : Rel x O} {i} →
             ⟦ reindex f C ⟧ X i ↝[ k ] ⟦ C ⟧ (X ⊚ f) (f i)
⟦reindex⟧↔ {f = f} ext C {X} {i} =
  ⟦ reindex f C ⟧ X i                ↔⟨⟩
  ⟦ reindex₂ f (reindex₁ f C) ⟧ X i  ↔⟨⟩
  ⟦ reindex₁ f C ⟧ X (f i)           ↝⟨ ⟦reindex₁⟧↔ ext C ⟩□
  ⟦ C ⟧ (X ⊚ f) (f i)                □

-- An unfolding lemma for ⟦ reindex f C ⟧₂.

⟦reindex⟧₂↔ :
  ∀ {k ℓ x} {I O : Type ℓ} {X : Rel x O} →
  Extensionality? k ℓ ℓ →
  ∀ (C : Container I O) (f : I → O) (R : ∀ {o} → Rel₂ ℓ (X o)) {i}
  (x y : ⟦ reindex f C ⟧ X i) →

  ⟦ reindex f C ⟧₂ R (x , y)

    ↝[ k ]

  ⟦ C ⟧₂ R ( (proj₁ x , λ p → proj₂ x (_ , refl , p))
           , (proj₁ y , λ p → proj₂ y (_ , refl , p))
           )

⟦reindex⟧₂↔ ext C f R x y =

  ⟦ reindex f C ⟧₂ R (x , y)                           ↔⟨⟩

  ⟦ reindex₂ f (reindex₁ f C) ⟧₂ R (x , y)             ↔⟨⟩

  ⟦ reindex₁ f C ⟧₂ R (x , y)                          ↝⟨ ⟦reindex₁⟧₂↔ ext C f R x y ⟩□

  ⟦ C ⟧₂ R ( (proj₁ x , λ p → proj₂ x (_ , refl , p))
           , (proj₁ y , λ p → proj₂ y (_ , refl , p))
           )                                           □

-- If f is an involution, then ν (reindex f C) i is pointwise
-- logically equivalent to ν C i ⊚ f.

mutual

  ν-reindex⇔ :
    ∀ {ℓ} {I : Type ℓ} {C : Container I I} {f : I → I} →
    f ⊚ f ≡ P.id →
    ∀ {i x} → ν (reindex f C) i x ⇔ ν C i (f x)
  ν-reindex⇔ {C = C} {f} inv {i} {x} =
    ν (reindex f C) i x                     ↔⟨⟩
    ⟦ reindex f C ⟧ (ν′ (reindex f C) i) x  ↝⟨ ⟦reindex⟧↔ _ C ⟩
    ⟦ C ⟧ (ν′ (reindex f C) i ⊚ f) (f x)    ↝⟨ ⟦⟧-cong _ C (ν′-reindex⇔ inv) ⟩
    ⟦ C ⟧ (ν′ C i ⊚ f ⊚ f) (f x)            ↔⟨ ≡⇒↝ bijection $ cong (λ g → ⟦ C ⟧ (ν′ C i ⊚ g) (f x)) inv ⟩
    ⟦ C ⟧ (ν′ C i) (f x)                    ↔⟨⟩
    ν C i (f x)                             □

  ν′-reindex⇔ :
    ∀ {ℓ} {I : Type ℓ} {C : Container I I} {f : I → I} →
    f ⊚ f ≡ P.id →
    ∀ {i x} → ν′ (reindex f C) i x ⇔ ν′ C i (f x)
  ν′-reindex⇔ {C = C} {f} inv = record { to = to; from = from }
    where
    to : ∀ {i} → ν′ (reindex f C) i ⊆ ν′ C i ⊚ f
    force (to x) = _⇔_.to (ν-reindex⇔ inv) (force x)

    from : ∀ {i} → ν′ C i ⊚ f ⊆ ν′ (reindex f C) i
    force (from x) = _⇔_.from (ν-reindex⇔ inv) (force x)

-- A cartesian product combinator.
--
-- Similar to a construction in "Containers: Constructing strictly
-- positive types" by Abbott, Altenkirch and Ghani (see
-- Proposition 3.5).

infixr 2 _⊗_

_⊗_ : ∀ {ℓ} {I O : Type ℓ} →
      Container I O → Container I O → Container I O
C₁ ⊗ C₂ =
  (λ o → Shape C₁ o × Shape C₂ o)
    ◁
  (λ { (s₁ , s₂) i → Position C₁ s₁ i ⊎ Position C₂ s₂ i })
  where
  open Container

-- An unfolding lemma for ⟦ C₁ ⊗ C₂ ⟧.

⟦⊗⟧↔ : ∀ {k ℓ x} {I O : Type ℓ} →
       Extensionality? k ℓ (ℓ ⊔ x) →
       ∀ (C₁ C₂ : Container I O) {X : Rel x I} {o} →
       ⟦ C₁ ⊗ C₂ ⟧ X o ↝[ k ] ⟦ C₁ ⟧ X o × ⟦ C₂ ⟧ X o
⟦⊗⟧↔ {k} {ℓ} ext C₁ C₂ {X} {o} =
  ⟦ C₁ ⊗ C₂ ⟧ X o                                                  ↔⟨⟩

  (∃ λ (s : Shape C₁ o × Shape C₂ o) →
   (λ i → Position C₁ (proj₁ s) i ⊎ Position C₂ (proj₂ s) i) ⊆ X)  ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (s₁ : Shape C₁ o) →
   ∃ λ (s₂ : Shape C₂ o) →
   (λ i → Position C₁ s₁ i ⊎ Position C₂ s₂ i) ⊆ X)                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → implicit-∀-cong ext $
                                                                       Π⊎↔Π×Π (lower-extensionality? k lzero ℓ ext)) ⟩
  (∃ λ (s₁ : Shape C₁ o) →
   ∃ λ (s₂ : Shape C₂ o) →
   ∀ {i} → (Position C₁ s₁ i → X i) × (Position C₂ s₂ i → X i))    ↔⟨ (∃-cong λ _ → ∃-cong λ _ → implicit-ΠΣ-comm) ⟩

  (∃ λ (s₁ : Shape C₁ o) →
   ∃ λ (s₂ : Shape C₂ o) →
   Position C₁ s₁ ⊆ X × Position C₂ s₂ ⊆ X)                        ↔⟨ (∃-cong λ _ → ∃-comm) ⟩

  (∃ λ (s₁ : Shape C₁ o) →
   Position C₁ s₁ ⊆ X
     ×
   ∃ λ (s₂ : Shape C₂ o) → Position C₂ s₂ ⊆ X)                     ↔⟨ Σ-assoc ⟩

  (∃ λ (s : Shape C₁ o) → Position C₁ s ⊆ X) ×
  (∃ λ (s : Shape C₂ o) → Position C₂ s ⊆ X)                       ↔⟨⟩

  ⟦ C₁ ⟧ X o × ⟦ C₂ ⟧ X o                                          □
  where
  open Container

-- An unfolding lemma for ⟦ C₁ ⊗ C₂ ⟧₂.

⟦⊗⟧₂↔ :
  ∀ {k ℓ x} {I : Type ℓ} {X : Rel x I} →
  Extensionality? k ℓ ℓ →
  ∀ (C₁ C₂ : Container I I) (R : ∀ {i} → Rel₂ ℓ (X i)) {i}
  (x y : ⟦ C₁ ⊗ C₂ ⟧ X i) →

  let (x₁ , x₂) , f = x
      (y₁ , y₂) , g = y
  in

  ⟦ C₁ ⊗ C₂ ⟧₂ R (x , y)

    ↝[ k ]

  ⟦ C₁ ⟧₂ R ((x₁ , f ⊚ inj₁) , (y₁ , g ⊚ inj₁))
    ×
  ⟦ C₂ ⟧₂ R ((x₂ , f ⊚ inj₂) , (y₂ , g ⊚ inj₂))

⟦⊗⟧₂↔ ext C₁ C₂ R (x@(x₁ , x₂) , f) (y@(y₁ , y₂) , g) =

  ⟦ C₁ ⊗ C₂ ⟧₂ R ((x , f) , (y , g))                                      ↔⟨⟩

  (∃ λ (eq : x ≡ y) →
   ∀ {o} (p : Position (C₁ ⊗ C₂) x o) →
   R (f p , g (subst (λ s → Position (C₁ ⊗ C₂) s o) eq p)))               ↔⟨⟩

  (∃ λ (eq : x ≡ y) →
   ∀ {o} (p : Position C₁ x₁ o ⊎ Position C₂ x₂ o) →
   R ( f p
     , g (subst (λ { (s₁ , s₂) → Position C₁ s₁ o ⊎ Position C₂ s₂ o })
                eq p)
     ))                                                                   ↔⟨ inverse (Σ-cong ≡×≡↔≡ λ _ → Bijection.id) ⟩

  (∃ λ (eq : x₁ ≡ y₁ × x₂ ≡ y₂) →
   ∀ {o} (p : Position C₁ x₁ o ⊎ Position C₂ x₂ o) →
   R ( f p
     , g (subst (λ { (s₁ , s₂) → Position C₁ s₁ o ⊎ Position C₂ s₂ o })
                (cong₂ _,_ (proj₁ eq) (proj₂ eq)) p)
     ))                                                                   ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (eq₁ : x₁ ≡ y₁) →
   ∃ λ (eq₂ : x₂ ≡ y₂) →
   ∀ {o} (p : Position C₁ x₁ o ⊎ Position C₂ x₂ o) →
   R ( f p
     , g (subst (λ { (s₁ , s₂) → Position C₁ s₁ o ⊎ Position C₂ s₂ o })
                (cong₂ _,_ eq₁ eq₂) p)
     ))                                                                   ↝⟨ (∃-cong λ _ → ∃-cong λ _ → implicit-∀-cong ext $ Π⊎↔Π×Π ext) ⟩

  (∃ λ (eq₁ : x₁ ≡ y₁) →
   ∃ λ (eq₂ : x₂ ≡ y₂) →
   ∀ {o} →
   ((p : Position C₁ x₁ o) →
    R ( f (inj₁ p)
      , g (subst (λ { (s₁ , s₂) → Position C₁ s₁ o ⊎ Position C₂ s₂ o })
                 (cong₂ _,_ eq₁ eq₂) (inj₁ p))
      ))
     ×
   ((p : Position C₂ x₂ o) →
    R ( f (inj₂ p)
      , g (subst (λ { (s₁ , s₂) → Position C₁ s₁ o ⊎ Position C₂ s₂ o })
                 (cong₂ _,_ eq₁ eq₂) (inj₂ p))
      )))                                                                 ↝⟨ (∃-cong λ eq₁ → ∃-cong λ eq₂ → implicit-∀-cong ext $
                                                                              (∀-cong ext λ _ → ≡⇒↝ _ $ cong (R ⊚ (f _ ,_)) $
                                                                               lemma₁ eq₁ eq₂)
                                                                                ×-cong
                                                                              (∀-cong ext λ _ → ≡⇒↝ _ $ cong (R ⊚ (f _ ,_)) $
                                                                               lemma₂ eq₁ eq₂)) ⟩
  (∃ λ (eq₁ : x₁ ≡ y₁) →
   ∃ λ (eq₂ : x₂ ≡ y₂) →
   ∀ {o} →
   ((p : Position C₁ x₁ o) →
    R (f (inj₁ p) , g (inj₁ (subst (λ s₁ → Position C₁ s₁ o) eq₁ p))))
     ×
   ((p : Position C₂ x₂ o) →
    R (f (inj₂ p) , g (inj₂ (subst (λ s₂ → Position C₂ s₂ o) eq₂ p)))))   ↔⟨ (∃-cong λ _ → ∃-cong λ _ → implicit-ΠΣ-comm) ⟩

  (∃ λ (eq₁ : x₁ ≡ y₁) →
   ∃ λ (eq₂ : x₂ ≡ y₂) →
   (∀ {o} (p : Position C₁ x₁ o) →
    R (f (inj₁ p) , g (inj₁ (subst (λ s₁ → Position C₁ s₁ o) eq₁ p))))
     ×
   (∀ {o} (p : Position C₂ x₂ o) →
    R (f (inj₂ p) , g (inj₂ (subst (λ s₂ → Position C₂ s₂ o) eq₂ p)))))   ↔⟨ (∃-cong λ _ → ∃-comm) ⟩

  (∃ λ (eq₁ : x₁ ≡ y₁) →
   (∀ {o} (p : Position C₁ x₁ o) →
    R (f (inj₁ p) , g (inj₁ (subst (λ s₁ → Position C₁ s₁ o) eq₁ p))))
     ×
   ∃ λ (eq₂ : x₂ ≡ y₂) →
   (∀ {o} (p : Position C₂ x₂ o) →
    R (f (inj₂ p) , g (inj₂ (subst (λ s₂ → Position C₂ s₂ o) eq₂ p)))))   ↔⟨ Σ-assoc ⟩

  (∃ λ (eq : x₁ ≡ y₁) →
   (∀ {o} (p : Container.Position C₁ x₁ o) →
    R ( f (inj₁ p)
      , g (inj₁ (subst (λ s₁ → Container.Position C₁ s₁ o) eq p)))
      ))
    ×
  (∃ λ (eq : x₂ ≡ y₂) →
   (∀ {o} (p : Container.Position C₂ x₂ o) →
    R ( f (inj₂ p)
      , g (inj₂ (subst (λ s₂ → Container.Position C₂ s₂ o) eq p))
      )))                                                                 ↔⟨⟩

  ⟦ C₁ ⟧₂ R ((x₁ , f ⊚ inj₁) , (y₁ , g ⊚ inj₁))
    ×
  ⟦ C₂ ⟧₂ R ((x₂ , f ⊚ inj₂) , (y₂ , g ⊚ inj₂))                           □

  where
  open Container

  lemma₁ = λ (eq₁ : x₁ ≡ y₁) (eq₂ : x₂ ≡ y₂) {o p} →

    g (subst (λ { (s₁ , s₂) → Position C₁ s₁ o ⊎ Position C₂ s₂ o })
             (cong₂ _,_ eq₁ eq₂) (inj₁ p))                            ≡⟨ cong g $ push-subst-inj₁ {y≡z = cong₂ _,_ eq₁ eq₂} _ _ ⟩

    g (inj₁ (subst (λ { (s₁ , s₂) → Position C₁ s₁ o })
                   (cong₂ _,_ eq₁ eq₂) p))                            ≡⟨ cong (g ⊚ inj₁) $ subst-∘ _ _ (cong₂ _,_ eq₁ eq₂) ⟩

    g (inj₁ (subst (λ s₁ → Position C₁ s₁ o)
                   (cong proj₁ (cong₂ _,_ eq₁ eq₂)) p))               ≡⟨ cong (g ⊚ inj₁) $ cong (flip (subst _) _) $ cong-proj₁-cong₂-, eq₁ eq₂ ⟩∎

    g (inj₁ (subst (λ s₁ → Position C₁ s₁ o) eq₁ p))                  ∎

  lemma₂ = λ (eq₁ : x₁ ≡ y₁) (eq₂ : x₂ ≡ y₂) {o p} →

    g (subst (λ { (s₁ , s₂) → Position C₁ s₁ o ⊎ Position C₂ s₂ o })
             (cong₂ _,_ eq₁ eq₂) (inj₂ p))                            ≡⟨ cong g $ push-subst-inj₂ {y≡z = cong₂ _,_ eq₁ eq₂} _ _ ⟩

    g (inj₂ (subst (λ { (s₁ , s₂) → Position C₂ s₂ o })
                   (cong₂ _,_ eq₁ eq₂) p))                            ≡⟨ cong (g ⊚ inj₂) $ subst-∘ _ _ (cong₂ _,_ eq₁ eq₂) ⟩

    g (inj₂ (subst (λ s₂ → Position C₂ s₂ o)
                   (cong proj₂ (cong₂ _,_ eq₁ eq₂)) p))               ≡⟨ cong (g ⊚ inj₂) $ cong (flip (subst _) _) $ cong-proj₂-cong₂-, eq₁ eq₂ ⟩∎

    g (inj₂ (subst (λ s₂ → Position C₂ s₂ o) eq₂ p))                  ∎

-- The greatest fixpoint ν (C₁ ⊗ C₂) i is contained in the
-- intersection ν C₁ i ∩ ν C₂ i.

ν-⊗⊆ :
  ∀ {ℓ} {I : Type ℓ} {C₁ C₂ : Container I I} {i} →
  ν (C₁ ⊗ C₂) i ⊆ ν C₁ i ∩ ν C₂ i
ν-⊗⊆ {C₁ = C₁} {C₂} {i} =
  ν (C₁ ⊗ C₂) i                                      ⊆⟨⟩
  ⟦ C₁ ⊗ C₂ ⟧ (ν′ (C₁ ⊗ C₂) i)                       ⊆⟨ ⟦⊗⟧↔ _ C₁ C₂ ⟩
  ⟦ C₁ ⟧ (ν′ (C₁ ⊗ C₂) i) ∩ ⟦ C₂ ⟧ (ν′ (C₁ ⊗ C₂) i)  ⊆⟨ Σ-map (map C₁ ν-⊗⊆₁′) (map C₂ ν-⊗⊆₂′) ⟩
  ⟦ C₁ ⟧ (ν′ C₁ i) ∩ ⟦ C₂ ⟧ (ν′ C₂ i)                ⊆⟨ P.id ⟩∎
  ν C₁ i ∩ ν C₂ i                                    ∎
  where
  ν-⊗⊆₁′ : ν′ (C₁ ⊗ C₂) i ⊆ ν′ C₁ i
  force (ν-⊗⊆₁′ x) = proj₁ (ν-⊗⊆ (force x))

  ν-⊗⊆₂′ : ν′ (C₁ ⊗ C₂) i ⊆ ν′ C₂ i
  force (ν-⊗⊆₂′ x) = proj₂ (ν-⊗⊆ (force x))

-- A disjoint union combinator.
--
-- Similar to a construction in "Containers: Constructing strictly
-- positive types" by Abbott, Altenkirch and Ghani (see
-- Proposition 3.5).

infixr 2 _⊕_

_⊕_ : ∀ {ℓ} {I O : Type ℓ} →
      Container I O → Container I O → Container I O
C₁ ⊕ C₂ =
  (λ o → Shape C₁ o ⊎ Shape C₂ o)
    ◁
  [ Position C₁ , Position C₂ ]
  where
  open Container

-- An unfolding lemma for ⟦ C₁ ⊕ C₂ ⟧.

⟦⊕⟧↔ : ∀ {ℓ x} {I O : Type ℓ}
       (C₁ C₂ : Container I O) {X : Rel x I} {o} →
       ⟦ C₁ ⊕ C₂ ⟧ X o ↔ ⟦ C₁ ⟧ X o ⊎ ⟦ C₂ ⟧ X o
⟦⊕⟧↔ C₁ C₂ {X} {o} =
  ⟦ C₁ ⊕ C₂ ⟧ X o                               ↔⟨⟩

  (∃ λ (s : Shape C₁ o ⊎ Shape C₂ o) →
   [ Position C₁ , Position C₂ ] s ⊆ X)         ↝⟨ ∃-⊎-distrib-right ⟩

  (∃ λ (s : Shape C₁ o) → Position C₁ s ⊆ X) ⊎
  (∃ λ (s : Shape C₂ o) → Position C₂ s ⊆ X)    ↔⟨⟩

  ⟦ C₁ ⟧ X o ⊎ ⟦ C₂ ⟧ X o                       □
  where
  open Container

-- An unfolding lemma for ⟦ C₁ ⊕ C₂ ⟧₂.

⟦⊕⟧₂↔ :
  ∀ {k ℓ x} {I : Type ℓ} {X : Rel x I} →
  Extensionality? k ℓ ℓ →
  ∀ (C₁ C₂ : Container I I) (R : ∀ {i} → Rel₂ ℓ (X i)) {i}
  (x y : ⟦ C₁ ⊕ C₂ ⟧ X i) →

  ⟦ C₁ ⊕ C₂ ⟧₂ R (x , y)

    ↝[ k ]

  (curry (⟦ C₁ ⟧₂ R) ⊎-rel curry (⟦ C₂ ⟧₂ R))
    (_↔_.to (⟦⊕⟧↔ C₁ C₂) x)
    (_↔_.to (⟦⊕⟧↔ C₁ C₂) y)

⟦⊕⟧₂↔ ext C₁ C₂ R (inj₁ x , f) (inj₁ y , g) =

  ⟦ C₁ ⊕ C₂ ⟧₂ R ((inj₁ x , f) , (inj₁ y , g))                   ↔⟨⟩

  (∃ λ (eq : inj₁ x ≡ inj₁ y) →
   ∀ {o} (p : Position C₁ x o) →
   R ( f p
     , g (subst (λ s → [_,_] {C = λ _ → Rel _ _}
                         (Position C₁) (Position C₂) s o) eq p)
     ))                                                          ↔⟨ inverse $ Σ-cong Bijection.≡↔inj₁≡inj₁ (λ _ → Bijection.id) ⟩

  (∃ λ (eq : x ≡ y) →
   ∀ {o} (p : Position C₁ x o) →
   R ( f p
     , g (subst (λ s → [_,_] {C = λ _ → Rel _ _}
                         (Position C₁) (Position C₂) s o)
                         (cong inj₁ eq) p)
     ))                                                          ↝⟨ (∃-cong λ eq → implicit-∀-cong ext $ ∀-cong ext λ _ →
                                                                     ≡⇒↝ _ $ cong (λ x → R (_ , g x)) $ sym $
                                                                     subst-∘ _ _ eq) ⟩
  (∃ λ (eq : x ≡ y) →
   ∀ {o} (p : Position C₁ x o) →
   R ( f p
     , g (subst (λ s → Position C₁ s o) eq p)
     ))                                                          ↔⟨⟩

  ⟦ C₁ ⟧₂ R ((x , f) , (y , g))                                  □

  where
  open Container

⟦⊕⟧₂↔ _ C₁ C₂ R (inj₁ x , f) (inj₂ y , g) =

  ⟦ C₁ ⊕ C₂ ⟧₂ R ((inj₁ x , f) , (inj₂ y , g))  ↔⟨⟩

  (∃ λ (eq : inj₁ x ≡ inj₂ y) → _)              ↔⟨ inverse $ Σ-cong (inverse Bijection.≡↔⊎) (λ _ → Bijection.id) ⟩

  (∃ λ (eq : ⊥) → _)                            ↔⟨ Σ-left-zero ⟩

  ⊥                                             □

⟦⊕⟧₂↔ _ C₁ C₂ R (inj₂ x , f) (inj₁ y , g) =

  ⟦ C₁ ⊕ C₂ ⟧₂ R ((inj₂ x , f) , (inj₁ y , g))  ↔⟨⟩

  (∃ λ (eq : inj₂ x ≡ inj₁ y) → _)              ↔⟨ inverse $ Σ-cong (inverse Bijection.≡↔⊎) (λ _ → Bijection.id) ⟩

  (∃ λ (eq : ⊥) → _)                            ↔⟨ Σ-left-zero ⟩

  ⊥                                             □

⟦⊕⟧₂↔ ext C₁ C₂ R (inj₂ x , f) (inj₂ y , g) =

  ⟦ C₁ ⊕ C₂ ⟧₂ R ((inj₂ x , f) , (inj₂ y , g))                   ↔⟨⟩

  (∃ λ (eq : inj₂ x ≡ inj₂ y) →
   ∀ {o} (p : Position C₂ x o) →
   R ( f p
     , g (subst (λ s → [_,_] {C = λ _ → Rel _ _}
                         (Position C₁) (Position C₂) s o) eq p)
     ))                                                          ↔⟨ inverse $ Σ-cong Bijection.≡↔inj₂≡inj₂ (λ _ → Bijection.id) ⟩

  (∃ λ (eq : x ≡ y) →
   ∀ {o} (p : Position C₂ x o) →
   R ( f p
     , g (subst (λ s → [_,_] {C = λ _ → Rel _ _}
                         (Position C₁) (Position C₂) s o)
                         (cong inj₂ eq) p)
     ))                                                          ↝⟨ (∃-cong λ eq → implicit-∀-cong ext $ ∀-cong ext λ _ →
                                                                     ≡⇒↝ _ $ cong (λ x → R (_ , g x)) $ sym $
                                                                     subst-∘ _ _ eq) ⟩
  (∃ λ (eq : x ≡ y) →
   ∀ {o} (p : Position C₂ x o) →
   R ( f p
     , g (subst (λ s → Position C₂ s o) eq p)
     ))                                                          ↔⟨⟩

  ⟦ C₂ ⟧₂ R ((x , f) , (y , g))                                  □

  where
  open Container

mutual

  -- A combinator that is similar to the function ⟷ from
  -- Section 6.3.4.1 in Pous and Sangiorgi's "Enhancements of the
  -- bisimulation proof method".

  ⟷[_] : ∀ {ℓ} {I : Type ℓ} →
         Container (I × I) (I × I) → Container (I × I) (I × I)
  ⟷[ C ] = C ⟷ C

  -- A generalisation of ⟷[_].

  infix 1 _⟷_

  _⟷_ : ∀ {ℓ} {I : Type ℓ} →
        (_ _ : Container (I × I) (I × I)) → Container (I × I) (I × I)
  C₁ ⟷ C₂ = C₁ ⊗ reindex swap C₂

-- An unfolding lemma for ⟦ C₁ ⟷ C₂ ⟧.

⟦⟷⟧↔ :
  ∀ {k ℓ x} {I : Type ℓ} →
  Extensionality? k ℓ (ℓ ⊔ x) →
  ∀ (C₁ C₂ : Container (I × I) (I × I)) {X : Rel₂ x I} {i} →
  ⟦ C₁ ⟷ C₂ ⟧ X i
    ↝[ k ]
  ⟦ C₁ ⟧ X i × (⟦ C₂ ⟧ (X ⁻¹) ⁻¹) i
⟦⟷⟧↔ ext C₁ C₂ {X} {i} =
  ⟦ C₁ ⟷ C₂ ⟧ X i                       ↔⟨⟩
  ⟦ C₁ ⊗ reindex swap C₂ ⟧ X i          ↝⟨ ⟦⊗⟧↔ ext C₁ (reindex swap C₂) ⟩
  ⟦ C₁ ⟧ X i × ⟦ reindex swap C₂ ⟧ X i  ↝⟨ ∃-cong (λ _ → ⟦reindex⟧↔ ext C₂) ⟩□
  ⟦ C₁ ⟧ X i × (⟦ C₂ ⟧ (X ⁻¹) ⁻¹) i     □

-- An unfolding lemma for ⟦ C₁ ⟷ C₂ ⟧₂.

⟦⟷⟧₂↔ :
  ∀ {k ℓ x} {I : Type ℓ} {X : Rel₂ x I} →
  Extensionality? k ℓ ℓ →
  ∀ (C₁ C₂ : Container (I × I) (I × I)) (R : ∀ {i} → Rel₂ ℓ (X i)) {i}
  (x y : ⟦ C₁ ⟷ C₂ ⟧ X i) →

  let (s₁ , s₂) , f = x
      (t₁ , t₂) , g = y
  in

  ⟦ C₁ ⟷ C₂ ⟧₂ R (x , y)

    ↝[ k ]

  ⟦ C₁ ⟧₂ R ((s₁ , f ⊚ inj₁) , (t₁ , g ⊚ inj₁))
    ×
  ⟦ C₂ ⟧₂ R ( (s₂ , λ p → f (inj₂ (_ , refl , p)))
            , (t₂ , λ p → g (inj₂ (_ , refl , p)))
            )

⟦⟷⟧₂↔ ext C₁ C₂ R x@((s₁ , s₂) , f) y@((t₁ , t₂) , g) =

  ⟦ C₁ ⟷ C₂ ⟧₂ R (x , y)                                      ↔⟨⟩

  ⟦ C₁ ⊗ reindex swap C₂ ⟧₂ R (x , y)                         ↝⟨ ⟦⊗⟧₂↔ ext C₁ (reindex swap C₂) R _ (_ , g) ⟩

  ⟦ C₁ ⟧₂ R ((s₁ , f ⊚ inj₁) , (t₁ , g ⊚ inj₁))
    ×
  ⟦ reindex swap C₂ ⟧₂ R ((s₂ , f ⊚ inj₂) , (t₂ , g ⊚ inj₂))  ↝⟨ ∃-cong (λ _ → ⟦reindex⟧₂↔ ext C₂ _ R _ (_ , g ⊚ inj₂)) ⟩□

  ⟦ C₁ ⟧₂ R ((s₁ , f ⊚ inj₁) , (t₁ , g ⊚ inj₁))
    ×
  ⟦ C₂ ⟧₂ R ( (s₂ , λ p → f (inj₂ (_ , refl , p)))
            , (t₂ , λ p → g (inj₂ (_ , refl , p)))
            )                                                 □

-- The greatest fixpoint ν (C₁ ⟷ C₂) i is contained in the
-- intersection ν C₁ i ∩ ν C₂ i ⁻¹.

ν-↔⊆ : ∀ {ℓ} {I : Type ℓ} {C₁ C₂ : Container (I × I) (I × I)} {i} →
       ν (C₁ ⟷ C₂) i ⊆ ν C₁ i ∩ ν C₂ i ⁻¹
ν-↔⊆ {C₁ = C₁} {C₂} {i} =
  ν (C₁ ⟷ C₂) i                   ⊆⟨⟩
  ν (C₁ ⊗ reindex swap C₂) i      ⊆⟨ ν-⊗⊆ ⟩
  ν C₁ i ∩ ν (reindex swap C₂) i  ⊆⟨ Σ-map P.id (_⇔_.to (ν-reindex⇔ refl)) ⟩∎
  ν C₁ i ∩ ν C₂ i ⁻¹              ∎

-- The following three lemmas correspond to the second part of
-- Exercise 6.3.24 in Pous and Sangiorgi's "Enhancements of the
-- bisimulation proof method".

-- Post-fixpoints of the container reindex₂ swap id ⊗ C are
-- post-fixpoints of ⟷[ C ].

⊆reindex₂-swap-⊗→⊆⟷ :
  ∀ {ℓ r} {I : Type ℓ} {C : Container (I × I) (I × I)} {R : Rel₂ r I} →
  R ⊆ ⟦ reindex₂ swap id ⊗ C ⟧ R → R ⊆ ⟦ ⟷[ C ] ⟧ R
⊆reindex₂-swap-⊗→⊆⟷ {C = C} {R} R⊆ =
  R                          ⊆⟨ (λ x → lemma₁ x , lemma₂ x) ⟩
  ⟦ C ⟧ R ∩ R ⁻¹             ⊆⟨ Σ-map P.id lemma₃ ⟩
  ⟦ C ⟧ R ∩ ⟦ C ⟧ (R ⁻¹) ⁻¹  ⊆⟨ _⇔_.from (⟦⟷⟧↔ _ C C) ⟩∎
  ⟦ ⟷[ C ] ⟧ R               ∎
  where
  lemma₀ =
    R                                 ⊆⟨ R⊆ ⟩
    ⟦ reindex₂ swap id ⊗ C ⟧ R        ⊆⟨ ⟦⊗⟧↔ _ (reindex₂ swap id) C ⟩∎
    ⟦ reindex₂ swap id ⟧ R ∩ ⟦ C ⟧ R  ∎

  lemma₁ =
    R                                 ⊆⟨ lemma₀ ⟩
    ⟦ reindex₂ swap id ⟧ R ∩ ⟦ C ⟧ R  ⊆⟨ proj₂ ⟩∎
    ⟦ C ⟧ R                           ∎

  lemma₂ =
    R                                 ⊆⟨ lemma₀ ⟩
    ⟦ reindex₂ swap id ⟧ R ∩ ⟦ C ⟧ R  ⊆⟨ proj₁ ⟩
    ⟦ reindex₂ swap id ⟧ R            ⊆⟨ P.id ⟩
    ⟦ id ⟧ R ⁻¹                       ⊆⟨ _⇔_.to (⟦id⟧↔ _) ⟩∎
    R ⁻¹                              ∎

  lemma₃ =
    R             ⊆⟨ lemma₁ ⟩
    ⟦ C ⟧ R       ⊆⟨ map C lemma₂ ⟩∎
    ⟦ C ⟧ (R ⁻¹)  ∎

-- The symmetric closure of a post-fixpoint of ⟷[ C ] is a
-- post-fixpoint of reindex₂ swap id ⊗ C.

⊆⟷→∪-swap⊆reindex₂-swap-⊗ :
  ∀ {ℓ r} {I : Type ℓ} {C : Container (I × I) (I × I)} {R : Rel₂ r I} →
  R ⊆ ⟦ ⟷[ C ] ⟧ R →
  R ∪ R ⁻¹ ⊆ ⟦ reindex₂ swap id ⊗ C ⟧ (R ∪ R ⁻¹)
⊆⟷→∪-swap⊆reindex₂-swap-⊗ {C = C} {R} R⊆ =
  R ∪ R ⁻¹                                            ⊆⟨ (λ x → lemma₁ x , lemma₂ x) ⟩
  ⟦ reindex₂ swap id ⟧ (R ∪ R ⁻¹) ∩ ⟦ C ⟧ (R ∪ R ⁻¹)  ⊆⟨ _⇔_.from (⟦⊗⟧↔ _ (reindex₂ swap id) C) ⟩∎
  ⟦ reindex₂ swap id ⊗ C ⟧ (R ∪ R ⁻¹)                 ∎
  where
  lemma₁ =
    R ∪ R ⁻¹                         ⊆⟨ [ inj₂ , inj₁ ] ⟩
    R ⁻¹ ∪ R                         ⊆⟨ P.id ⟩
    R ⁻¹ ∪ R ⁻¹ ⁻¹                   ⊆⟨ P.id ⟩
    (R ∪ R ⁻¹) ⁻¹                    ⊆⟨ _⇔_.from (⟦id⟧↔ _) ⟩
    ⟦ id ⟧ (R ∪ R ⁻¹) ⁻¹             ⊆⟨ P.id ⟩∎
    ⟦ reindex₂ swap id ⟧ (R ∪ R ⁻¹)  ∎

  lemma₂ =
    R ∪ R ⁻¹                                               ⊆⟨ ⊎-map R⊆ R⊆ ⟩
    ⟦ ⟷[ C ] ⟧ R ∪ ⟦ ⟷[ C ] ⟧ R ⁻¹                         ⊆⟨ ⊎-map (_⇔_.to (⟦⟷⟧↔ _ C C)) (_⇔_.to (⟦⟷⟧↔ _ C C)) ⟩
    ⟦ C ⟧ R ∩ ⟦ C ⟧ (R ⁻¹) ⁻¹ ∪ ⟦ C ⟧ R ⁻¹ ∩ ⟦ C ⟧ (R ⁻¹)  ⊆⟨ ⊎-map proj₁ proj₂ ⟩
    ⟦ C ⟧ R ∪ ⟦ C ⟧ (R ⁻¹)                                 ⊆⟨ [ map C inj₁ , map C inj₂ ] ⟩∎
    ⟦ C ⟧ (R ∪ R ⁻¹)                                       ∎

-- The greatest fixpoint of ⟷[ C ] is pointwise logically equivalent
-- to the greatest fixpoint of reindex₂ swap id ⊗ C.
--
-- Note that this proof is not necessarily size-preserving. TODO:
-- Figure out if the proof can be made size-preserving.

ν-⟷⇔ :
  ∀ {ℓ} {I : Type ℓ} {C : Container (I × I) (I × I)} {p} →
  ν ⟷[ C ] ∞ p ⇔ ν (reindex₂ swap id ⊗ C) ∞ p
ν-⟷⇔ {C = C} = record
  { to =
      let R = ν ⟷[ C ] ∞ in                           $⟨ (λ {_} → ν-out _) ⟩
      R ⊆ ⟦ ⟷[ C ] ⟧ R                                ↝⟨ ⊆⟷→∪-swap⊆reindex₂-swap-⊗ ⟩
      R ∪ R ⁻¹ ⊆ ⟦ reindex₂ swap id ⊗ C ⟧ (R ∪ R ⁻¹)  ↝⟨ unfold _ ⟩
      R ∪ R ⁻¹ ⊆ ν (reindex₂ swap id ⊗ C) ∞           ↝⟨ (λ hyp {_} x → hyp (inj₁ x)) ⟩□
      R ⊆ ν (reindex₂ swap id ⊗ C) ∞                  □

  ; from =
      let R = ν (reindex₂ swap id ⊗ C) ∞ in  $⟨ (λ {_} → ν-out _) ⟩
      R ⊆ ⟦ reindex₂ swap id ⊗ C ⟧ R         ↝⟨ ⊆reindex₂-swap-⊗→⊆⟷ ⟩
      R ⊆ ⟦ ⟷[ C ] ⟧ R                       ↝⟨ unfold _ ⟩□
      R ⊆ ν ⟷[ C ] ∞                         □
  }

ext: agda

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Lib.Vec where

open import Common.Nat renaming (zero to Z; suc to S)
open import Lib.Fin
open import Common.Unit
import Common.List -- using (List ; [] ; _∷_)

data Vec (A : Set) :  Nat -> Set where
  _∷_ : forall {n} -> A -> Vec A n -> Vec A (S n)
  []   : Vec A Z

infixr 30 _++_

_++_ : {A : Set}{m n : Nat} -> Vec A m -> Vec A n -> Vec A (m + n)
[]        ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

snoc : {A : Set}{n : Nat} -> Vec A n -> A -> Vec A (S n)
snoc []        e = e ∷ []
snoc (x ∷ xs) e = x ∷ snoc xs e

length : {A : Set}{n : Nat} -> Vec A n -> Nat
length [] = Z
length (x ∷ xs) = 1 + length xs

length' : {A : Set}{n : Nat} -> Vec A n -> Nat
length' {n = n} _ = n

zipWith3 : ∀ {A B C D n} -> (A -> B -> C -> D) -> Vec A n -> Vec B n -> Vec C n -> Vec D n
zipWith3 f []        []        []        = []
zipWith3 f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z ∷ zipWith3 f xs ys zs

zipWith : ∀ {A B C n} -> (A -> B -> C) -> Vec A n -> Vec B n -> {u : Unit} -> Vec C n
zipWith _ [] [] = []
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys {u = unit}

_!_ : ∀ {A n} -> Vec A n -> Fin n -> A
(x ∷ xs) ! fz = x
(_ ∷ xs) ! fs n = xs ! n
[] ! ()

_[_]=_ : {A : Set}{n : Nat} -> Vec A n -> Fin n -> A -> Vec A n
(a ∷ as) [ fz ]= e = e ∷ as
(a ∷ as) [ fs n ]= e = a ∷ (as [ n ]= e)
[] [ () ]= e

map : ∀ {A B n}(f : A -> B)(xs : Vec A n) -> Vec B n
map f []        = []
map f (x ∷ xs) = f x ∷ map f xs

forgetL : {A : Set}{n : Nat} -> Vec A n -> Common.List.List A
forgetL [] = Common.List.[]
forgetL (x ∷ xs) = x Common.List.∷ forgetL xs

rem : {A : Set}(xs : Common.List.List A) -> Vec A (Common.List.length xs)
rem Common.List.[] = []
rem (x Common.List.∷ xs) = x ∷ rem xs

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --without-K #-}

module Agda.Builtin.Nat where

open import Agda.Builtin.Bool

data Nat : Set where
  zero : Nat
  suc  : (n : Nat) → Nat

{-# BUILTIN NATURAL Nat #-}

infix  4 _==_ _<_
infixl 6 _+_ _-_
infixl 7 _*_

_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)

{-# BUILTIN NATPLUS _+_ #-}

_-_ : Nat → Nat → Nat
n     - zero = n
zero  - suc m = zero
suc n - suc m = n - m

{-# BUILTIN NATMINUS _-_ #-}

_*_ : Nat → Nat → Nat
zero  * m = zero
suc n * m = m + n * m

{-# BUILTIN NATTIMES _*_ #-}

_==_ : Nat → Nat → Bool
zero  == zero  = true
suc n == suc m = n == m
_     == _     = false

{-# BUILTIN NATEQUALS _==_ #-}

_<_ : Nat → Nat → Bool
_     < zero  = false
zero  < suc _ = true
suc n < suc m = n < m

{-# BUILTIN NATLESS _<_ #-}

-- Helper function  div-helper  for Euclidean division.
---------------------------------------------------------------------------
--
-- div-helper computes n / 1+m via iteration on n.
--
--   n div (suc m) = div-helper 0 m n m
--
-- The state of the iterator has two accumulator variables:
--
--   k: The quotient, returned once n=0.  Initialized to 0.
--
--   j: A counter, initialized to the divisor m, decreased on each iteration step.
--      Once it reaches 0, the quotient k is increased and j reset to m,
--      starting the next countdown.
--
-- Under the precondition j ≤ m, the invariant is
--
--   div-helper k m n j = k + (n + m - j) div (1 + m)

div-helper : (k m n j : Nat) → Nat
div-helper k m  zero    j      = k
div-helper k m (suc n)  zero   = div-helper (suc k) m n m
div-helper k m (suc n) (suc j) = div-helper k       m n j

{-# BUILTIN NATDIVSUCAUX div-helper #-}

-- Proof of the invariant by induction on n.
--
--   clause 1: div-helper k m 0 j
--           = k                                        by definition
--           = k + (0 + m - j) div (1 + m)              since m - j < 1 + m
--
--   clause 2: div-helper k m (1 + n) 0
--           = div-helper (1 + k) m n m                 by definition
--           = 1 + k + (n + m - m) div (1 + m)          by induction hypothesis
--           = 1 + k +          n  div (1 + m)          by simplification
--           = k +   (n + (1 + m)) div (1 + m)          by expansion
--           = k + (1 + n + m - 0) div (1 + m)          by expansion
--
--   clause 3: div-helper k m (1 + n) (1 + j)
--           = div-helper k m n j                       by definition
--           = k + (n + m - j) div (1 + m)              by induction hypothesis
--           = k + ((1 + n) + m - (1 + j)) div (1 + m)  by expansion
--
-- Q.e.d.

-- Helper function  mod-helper  for the remainder computation.
---------------------------------------------------------------------------
--
-- (Analogous to div-helper.)
--
-- mod-helper computes n % 1+m via iteration on n.
--
--   n mod (suc m) = mod-helper 0 m n m
--
-- The invariant is:
--
--   m = k + j  ==>  mod-helper k m n j = (n + k) mod (1 + m).

mod-helper : (k m n j : Nat) → Nat
mod-helper k m  zero    j      = k
mod-helper k m (suc n)  zero   = mod-helper 0       m n m
mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j

{-# BUILTIN NATMODSUCAUX mod-helper #-}

-- Proof of the invariant by induction on n.
--
--   clause 1: mod-helper k m 0 j
--           = k                               by definition
--           = (0 + k) mod (1 + m)             since m = k + j, thus k < m
--
--   clause 2: mod-helper k m (1 + n) 0
--           = mod-helper 0 m n m              by definition
--           = (n + 0)       mod (1 + m)       by induction hypothesis
--           = (n + (1 + m)) mod (1 + m)       by expansion
--           = (1 + n) + k)  mod (1 + m)       since k = m (as l = 0)
--
--   clause 3: mod-helper k m (1 + n) (1 + j)
--           = mod-helper (1 + k) m n j        by definition
--           = (n + (1 + k)) mod (1 + m)       by induction hypothesis
--           = ((1 + n) + k) mod (1 + m)       by commutativity
--
-- Q.e.d.

max_stars_repo_name: caryoscelus/agda

max_issues_repo_name: caryoscelus/agda

max_forks_repo_name: caryoscelus/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Builtin.List
open import Agda.Builtin.Nat

infixl 6 _∷ʳ_

_∷ʳ_ : {A : Set} → List A → A → List A
[]        ∷ʳ x = x ∷ []
(hd ∷ tl) ∷ʳ x = hd ∷ tl ∷ʳ x

infixl 5 _∷ʳ′_

data InitLast {A : Set} : List A → Set where
  []    : InitLast []
  _∷ʳ′_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x)

initLast : {A : Set} (xs : List A) → InitLast xs
initLast []               = []
initLast (x ∷ xs)         with initLast xs
... | []       = [] ∷ʳ′ x
... | ys ∷ʳ′ y = (x ∷ ys) ∷ʳ′ y

f : (xs : List Nat) → Set
f xs with initLast xs
... | [] = {!!}
... | xs ∷ʳ′ x = {!!}

-- ^ Shadowing a variable that is bound implicitly in the `...` is allowed

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
open import Nat
open import Prelude
open import core
open import contexts

open import progress
open import htype-decidable
open import lemmas-complete

module complete-progress where

  -- as in progress, we define a datatype for the possible outcomes of
  -- progress for readability.
  data okc : (d : ihexp) (Δ : hctx) → Set where
    V : ∀{d Δ} → d val → okc d Δ
    S : ∀{d Δ} → Σ[ d' ∈ ihexp ] (d ↦ d') → okc d Δ

  complete-progress : {Δ : hctx} {d : ihexp} {τ : htyp} →
                       Δ , ∅ ⊢ d :: τ →
                       d dcomplete →
                       okc d Δ
  complete-progress wt comp with progress wt
  complete-progress wt comp | I x = abort (lem-ind-comp comp x)
  complete-progress wt comp | S x = S x
  complete-progress wt comp | BV (BVVal x) = V x
  complete-progress wt (DCCast comp x₂ ()) | BV (BVHoleCast x x₁)
  complete-progress (TACast wt x) (DCCast comp x₃ x₄) | BV (BVArrCast x₁ x₂) = abort (x₁ (complete-consistency x x₃ x₄))

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda