module A201605.AbelChapmanExtended.OPE where

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong)

open import A201605.AbelChapmanExtended.Syntax




data _⊇_ : (Γ Γ′ : Cx) → Set where
  id   : ∀ {Γ}                → Γ        ⊇ Γ
  weak : ∀ {Γ Γ′ a} → Γ′ ⊇ Γ → (Γ′ , a) ⊇ Γ
  lift : ∀ {Γ Γ′ a} → Γ′ ⊇ Γ → (Γ′ , a) ⊇ (Γ , a)


_•_ : ∀ {Γ Γ′ Γ″} → Γ″ ⊇ Γ′ → Γ′ ⊇ Γ → Γ″ ⊇ Γ
id      • η      = η
weak η′ • η      = weak (η′ • η)
lift η′ • id     = lift η′
lift η′ • weak η = weak (η′ • η)
lift η′ • lift η = lift (η′ • η)


η•id : ∀ {Γ Γ′} (η : Γ′ ⊇ Γ) → η • id ≡ η
η•id id       = refl
η•id (weak η) = cong weak (η•id η)
η•id (lift η) = refl

id•η : ∀ {Γ Γ′} (η : Γ′ ⊇ Γ) → id • η ≡ η
id•η id       = refl
id•η (weak η) = refl
id•η (lift η) = cong lift (id•η η)

•assoc : ∀ {Γ‴ Γ″ Γ′ Γ} (η″ : Γ‴ ⊇ Γ″) (η′ : Γ″ ⊇ Γ′) (η : Γ′ ⊇ Γ) →
         (η″ • η′) • η ≡ η″ • (η′ • η)
•assoc id        η′        η        = refl
•assoc (weak η″) η′        η        = cong weak (•assoc η″ η′ η)
•assoc (lift η″) id        η        = refl
•assoc (lift η″) (weak η′) η        = cong weak (•assoc η″ η′ η)
•assoc (lift η″) (lift η′) id       = refl
•assoc (lift η″) (lift η′) (weak η) = cong weak (•assoc η″ η′ η)
•assoc (lift η″) (lift η′) (lift η) = cong lift (•assoc η″ η′ η)




-- module NonStandardLibrary where
--   open import Categories.Category using (Category)
--   open import Function using (flip)
--   open import Relation.Binary.PropositionalEquality using (sym ; cong₂ ; isEquivalence)

--   OPE : Category _ _ _
--   OPE = record
--     { Obj       = Cx
--     ; _⇒_      = _⊇_
--     ; _≡_       = _≡_
--     ; _∘_       = flip _•_
--     ; id        = id
--     ; assoc     = λ {_} {_} {_} {_} {η″} {η′} {η} → sym (•assoc η″ η′ η)
--     ; identityˡ = λ {_} {_} {η} → η•id η
--     ; identityʳ = λ {_} {_} {η} → id•η η
--     ; equiv     = isEquivalence
--     ; ∘-resp-≡  = cong₂ (flip _•_)
--     }