import SOAS.Families.Core

-- Various properties of context map operations
module SOAS.ContextMaps.Properties {T : Set}
  (open SOAS.Families.Core {T}) (𝒳 : Familyₛ) where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.ContextMaps.CategoryOfRenamings {T}
-- open import SOAS.ContextMaps.CategoryOfSubstitutions {T}
open import SOAS.ContextMaps.Combinators

open import Categories.Functor.Bifunctor
open import Categories.Object.Initial
open import Categories.Object.Coproduct
open import Categories.Category.Cocartesian
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (niHelper) renaming (refl to NI-refl)




private
  variable
    Γ Δ Θ Ξ : Ctx
    α : T

copair∘i₁ : {σ : Γ ~[ 𝒳 ]↝ Θ}{ς : Δ ~[ 𝒳 ]↝ Θ} (v : ℐ α Γ)
          → copair 𝒳 σ ς (∔.i₁ v) ≡ σ v
copair∘i₁ new = refl
copair∘i₁ {σ = σ} (old v) = copair∘i₁ {σ = σ ∘ old} v

copair∘i₂ : {σ : Γ ~[ 𝒳 ]↝ Θ}{ς : Δ ~[ 𝒳 ]↝ Θ} (v : ℐ α Δ)
          → copair 𝒳 σ ς (∔.i₂  {Γ} v) ≡ ς v
copair∘i₂ {Γ = ∅} v = refl
copair∘i₂ {Γ = α ∙ Γ} {σ = σ} v = copair∘i₂ {σ = σ ∘ old} v

f∘copair : (𝒳 {𝒴} : Familyₛ) (f : Θ ~[ 𝒳 ➔ 𝒴 ]↝ Ξ)(σ : Γ ~[ 𝒳 ]↝ Θ)(ς : Δ ~[ 𝒳 ]↝ Θ)
          (v : ℐ α (Γ ∔ Δ))
         → f (copair 𝒳 σ ς v) ≡ copair 𝒴 (f ∘ σ) (f ∘ ς) v
f∘copair {Γ = ∅} 𝒳 f σ ς v = refl
f∘copair {Γ = α ∙ Γ} 𝒳 f σ ς new = refl
f∘copair {Γ = α ∙ Γ} 𝒳 f σ ς (old v) = f∘copair 𝒳 f (σ ∘ old) ς v



-- module _ (𝒳ˢ : SubstitutionStructure 𝒳) where
--
--   open SubstitutionStructure 𝒳ˢ hiding (copair)
--
--   idm∘copair : (ρ : Γ ↝ Θ)(ϱ : Δ ↝ Θ)
--                (v : ℐ α (Γ ∔ Δ))
--              → copair 𝒳 (idm ∘ ρ) (idm ∘ ϱ) v ≡ idm (copair ℐ ρ ϱ v)
--   idm∘copair {∅} ρ ϱ v = refl
--   idm∘copair {α ∙ Γ} ρ ϱ new = refl
--   idm∘copair {α ∙ Γ} ρ ϱ (old v) = idm∘copair (ρ ∘ old) ϱ v
--   copair∘+₁ : {Γ₁ Γ₂ Δ₁ Δ₂ Θ : Ctx}{ρ : Γ₁ ↝ Γ₂}{ϱ : Δ₁ ↝ Δ₂}{σ : Γ₂ ~[ 𝒳 ]↝ Θ}{ς : Δ₂ ~[ 𝒳 ]↝ Θ}(v : ℐ α (Γ₁ ∔ Δ₁))
--             → copair 𝒳 σ ς ((ρ ∔.+₁ ϱ) v) ≡ copair 𝒳 (σ ∘ ρ) (ς ∘ ϱ) v
--   copair∘+₁ {Γ₁ = Γ₁}{Γ₂}{Δ₁}{Δ₂}{Θ}{ρ = ρ}{ϱ}{σ}{ς} v = begin
--         copair 𝒳 σ ς ((ρ ∔.+₁ ϱ) v)
--     ≡⟨⟩
--         copair 𝒳 σ ς (copair ℐ (∔.i₁ {Γ₂} ∘ ρ) (∔.i₂ {Γ₂} ∘ ϱ) v)
--     ≡⟨ f∘copair ℐ (copair 𝒳 σ ς) (∔.i₁ {Γ₂} ∘ ρ) (∔.i₂ {Γ₂} ∘ ϱ) v ⟩
--         copair 𝒳 (copair 𝒳 σ ς ∘ ∔.i₁ {Γ₂} ∘ ρ) (copair 𝒳 σ ς ∘ ∔.i₂ {Γ₂} ∘ ϱ) v
--     ≡⟨ 𝕊∔.[]-cong₂ 𝒳 𝒳ˢ (λ{ {v = v} → copair∘i₁ (ρ v) }) (λ{ {v = v} → copair∘i₂ {σ = σ} (ϱ v) }) {v = v} ⟩
--         copair 𝒳 (σ ∘ ρ) (ς ∘ ϱ) v
--     ∎ where open ≡-Reasoning


  --       copair 𝒳 σ ς ((ρ ∔.+₁ ϱ) v)
  --   ≡⟨⟩
  --       copair 𝒳 σ ς (copair ℐ (∔.i₁ {Γ₂} ∘ ρ) (∔.i₂ {Γ₂} ∘ ϱ) v)
  --   ≡⟨ f∘copair {Γ = {!   !}}{{!   !}}(copair 𝒳 σ ς) v ⟩
  --       copair 𝒳 (copair 𝒳 σ ς ∘ ∔.i₁ {Γ₂} ∘ ρ) (copair 𝒳 σ ς ∘ ∔.i₂ {Γ₂} ∘ ϱ) v
  --   ≡⟨ {!   !} ⟩
  --       copair 𝒳 (σ ∘ ρ) (ς ∘ ϱ) v
  --   ∎ where open ≡-Reasoning