Pi.Syntax.Pi+.NonIndexed

{-# OPTIONS --without-K --exact-split --rewriting #-}

open import lib.Base
open import lib.NType
open import Pi.Common.Extra

module Pi.Syntax.Pi+.NonIndexed where

-- Types

data U : Set where
  O I : U
  _+_ : U → U → U

infixr 40 _+_
infix 30 _⟷₁_
infixr 50 _◎_ _⊕_

-- 1-combinators

data _⟷₁_  : U → U → Set where
  unite₊l : {t : U} → O + t ⟷₁ t
  uniti₊l : {t : U} → t ⟷₁ O + t
  swap₊   : {t₁ t₂ : U} → t₁ + t₂ ⟷₁ t₂ + t₁
  assocl₊ : {t₁ t₂ t₃ : U} → t₁ + (t₂ + t₃) ⟷₁ (t₁ + t₂) + t₃
  assocr₊ : {t₁ t₂ t₃ : U} → (t₁ + t₂) + t₃ ⟷₁ t₁ + (t₂ + t₃)
  id⟷₁     : {t : U} → t ⟷₁ t
  _◎_     : {t₁ t₂ t₃ : U} → (t₁ ⟷₁ t₂) → (t₂ ⟷₁ t₃) → (t₁ ⟷₁ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : U} → (t₁ ⟷₁ t₃) → (t₂ ⟷₁ t₄) → (t₁ + t₂ ⟷₁ t₃ + t₄)

-- Equational reasoning

infixr 10 _⟷₁⟨_⟩_
infix  15 _⟷₁∎

_⟷₁⟨_⟩_ : ∀ {t₂ t₃ : U} → (t₁ : U) → (t₁ ⟷₁ t₂) → (t₂ ⟷₁ t₃) → (t₁ ⟷₁ t₃)
_ ⟷₁⟨ c₁ ⟩ c₂ = c₁ ◎ c₂

_⟷₁∎ : (t : U) → t ⟷₁ t
_⟷₁∎ t = id⟷₁

-- Coherence

unite₊r : {t : U} → t + O ⟷₁ t
unite₊r = swap₊ ◎ unite₊l

uniti₊r : {t : U} → t ⟷₁ t + O
uniti₊r = uniti₊l ◎ swap₊

!⟷₁ : {t₁ t₂ : U} → t₁ ⟷₁ t₂ → t₂ ⟷₁ t₁
!⟷₁ unite₊l = uniti₊l
!⟷₁ uniti₊l = unite₊l
!⟷₁ swap₊ = swap₊
!⟷₁ assocl₊ = assocr₊
!⟷₁ assocr₊ = assocl₊
!⟷₁ id⟷₁ = id⟷₁
!⟷₁ (c₁ ◎ c₂) = !⟷₁ c₂ ◎ !⟷₁ c₁
!⟷₁ (c₁ ⊕ c₂) = !⟷₁ c₁ ⊕ !⟷₁ c₂

-- 2-combinators

data _⟷₂_ : {X Y : U} → X ⟷₁ Y → X ⟷₁ Y → Set where
  assoc◎l : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷₁ t₂} {c₂ : t₂ ⟷₁ t₃} {c₃ : t₃ ⟷₁ t₄} →
          (c₁ ◎ (c₂ ◎ c₃)) ⟷₂ ((c₁ ◎ c₂) ◎ c₃)
  assoc◎r : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷₁ t₂} {c₂ : t₂ ⟷₁ t₃} {c₃ : t₃ ⟷₁ t₄} →
          ((c₁ ◎ c₂) ◎ c₃) ⟷₂ (c₁ ◎ (c₂ ◎ c₃))
  assocl₊l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷₁ t₂} {c₂ : t₃ ⟷₁ t₄} {c₃ : t₅ ⟷₁ t₆} →
          ((c₁ ⊕ (c₂ ⊕ c₃)) ◎ assocl₊) ⟷₂ (assocl₊ ◎ ((c₁ ⊕ c₂) ⊕ c₃))
  assocl₊r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷₁ t₂} {c₂ : t₃ ⟷₁ t₄} {c₃ : t₅ ⟷₁ t₆} →
          (assocl₊ ◎ ((c₁ ⊕ c₂) ⊕ c₃)) ⟷₂ ((c₁ ⊕ (c₂ ⊕ c₃)) ◎ assocl₊)
  assocr₊r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷₁ t₂} {c₂ : t₃ ⟷₁ t₄} {c₃ : t₅ ⟷₁ t₆} →
          (((c₁ ⊕ c₂) ⊕ c₃) ◎ assocr₊) ⟷₂ (assocr₊ ◎ (c₁ ⊕ (c₂ ⊕ c₃)))
  assocr₊l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷₁ t₂} {c₂ : t₃ ⟷₁ t₄} {c₃ : t₅ ⟷₁ t₆} →
           (assocr₊ ◎ (c₁ ⊕ (c₂ ⊕ c₃))) ⟷₂ (((c₁ ⊕ c₂) ⊕ c₃) ◎ assocr₊)
  idl◎l   : {t₁ t₂ : U} {c : t₁ ⟷₁ t₂} → (id⟷₁ ◎ c) ⟷₂ c
  idl◎r   : {t₁ t₂ : U} {c : t₁ ⟷₁ t₂} → c ⟷₂ id⟷₁ ◎ c
  idr◎l   : {t₁ t₂ : U} {c : t₁ ⟷₁ t₂} → (c ◎ id⟷₁) ⟷₂ c
  idr◎r   : {t₁ t₂ : U} {c : t₁ ⟷₁ t₂} → c ⟷₂ (c ◎ id⟷₁)
  linv◎l  : {t₁ t₂ : U} {c : t₁ ⟷₁ t₂} → (c ◎ !⟷₁ c) ⟷₂ id⟷₁
  linv◎r  : {t₁ t₂ : U} {c : t₁ ⟷₁ t₂} → id⟷₁ ⟷₂ (c ◎ !⟷₁ c)
  rinv◎l  : {t₁ t₂ : U} {c : t₁ ⟷₁ t₂} → (!⟷₁ c ◎ c) ⟷₂ id⟷₁
  rinv◎r  : {t₁ t₂ : U} {c : t₁ ⟷₁ t₂} → id⟷₁ ⟷₂ (!⟷₁ c ◎ c)
  unite₊l⟷₂l : {t₁ t₂ : U} {c₁ : O ⟷₁ O} {c₂ : t₁ ⟷₁ t₂} →
          (unite₊l ◎ c₂) ⟷₂ ((c₁ ⊕ c₂) ◎ unite₊l)
  unite₊l⟷₂r : {t₁ t₂ : U} {c₁ : O ⟷₁ O} {c₂ : t₁ ⟷₁ t₂} →
          ((c₁ ⊕ c₂) ◎ unite₊l) ⟷₂ (unite₊l ◎ c₂)
  uniti₊l⟷₂l : {t₁ t₂ : U} {c₁ : O ⟷₁ O} {c₂ : t₁ ⟷₁ t₂} →
          (uniti₊l ◎ (c₁ ⊕ c₂)) ⟷₂ (c₂ ◎ uniti₊l)
  uniti₊l⟷₂r : {t₁ t₂ : U} {c₁ : O ⟷₁ O} {c₂ : t₁ ⟷₁ t₂} →
          (c₂ ◎ uniti₊l) ⟷₂ (uniti₊l ◎ (c₁ ⊕ c₂))
  swapl₊⟷₂ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷₁ t₂} {c₂ : t₃ ⟷₁ t₄} →
          (swap₊ ◎ (c₁ ⊕ c₂)) ⟷₂ ((c₂ ⊕ c₁) ◎ swap₊)
  swapr₊⟷₂ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷₁ t₂} {c₂ : t₃ ⟷₁ t₄} →
          ((c₂ ⊕ c₁) ◎ swap₊) ⟷₂ (swap₊ ◎ (c₁ ⊕ c₂))
  id⟷₂     : {t₁ t₂ : U} {c : t₁ ⟷₁ t₂} → c ⟷₂ c
  trans⟷₂  : {t₁ t₂ : U} {c₁ c₂ c₃ : t₁ ⟷₁ t₂} →
         (c₁ ⟷₂ c₂) → (c₂ ⟷₂ c₃) → (c₁ ⟷₂ c₃)
  _⊡_  : {t₁ t₂ t₃ : U}
         {c₁ : t₁ ⟷₁ t₂} {c₂ : t₂ ⟷₁ t₃} {c₃ : t₁ ⟷₁ t₂} {c₄ : t₂ ⟷₁ t₃} →
         (c₁ ⟷₂ c₃) → (c₂ ⟷₂ c₄) → (c₁ ◎ c₂) ⟷₂ (c₃ ◎ c₄)
  resp⊕⟷₂  : {t₁ t₂ t₃ t₄ : U}
         {c₁ : t₁ ⟷₁ t₂} {c₂ : t₃ ⟷₁ t₄} {c₃ : t₁ ⟷₁ t₂} {c₄ : t₃ ⟷₁ t₄} →
         (c₁ ⟷₂ c₃) → (c₂ ⟷₂ c₄) → (c₁ ⊕ c₂) ⟷₂ (c₃ ⊕ c₄)
  id⟷₁⊕id⟷₁⟷₂ : {t₁ t₂ : U} → (id⟷₁ {t₁} ⊕ id⟷₁ {t₂}) ⟷₂ id⟷₁
  split⊕-id⟷₁ : {t₁ t₂ : U} → (id⟷₁ {t₁ + t₂}) ⟷₂ (id⟷₁ ⊕ id⟷₁)
  hom⊕◎⟷₂ : {t₁ t₂ t₃ t₄ t₅ t₆ : U} {c₁ : t₅ ⟷₁ t₁} {c₂ : t₆ ⟷₁ t₂}
        {c₃ : t₁ ⟷₁ t₃} {c₄ : t₂ ⟷₁ t₄} →
        ((c₁ ◎ c₃) ⊕ (c₂ ◎ c₄)) ⟷₂ ((c₁ ⊕ c₂) ◎ (c₃ ⊕ c₄))
  hom◎⊕⟷₂ : {t₁ t₂ t₃ t₄ t₅ t₆ : U} {c₁ : t₅ ⟷₁ t₁} {c₂ : t₆ ⟷₁ t₂}
        {c₃ : t₁ ⟷₁ t₃} {c₄ : t₂ ⟷₁ t₄} →
         ((c₁ ⊕ c₂) ◎ (c₃ ⊕ c₄)) ⟷₂ ((c₁ ◎ c₃) ⊕ (c₂ ◎ c₄))
  -- associativity triangle
  triangle₊l : {t₁ t₂ : U} →
    (unite₊r {t₁} ⊕ id⟷₁ {t₂}) ⟷₂ assocr₊ ◎ (id⟷₁ ⊕ unite₊l)
  triangle₊r : {t₁ t₂ : U} →
    assocr₊ ◎ (id⟷₁ {t₁} ⊕ unite₊l {t₂}) ⟷₂ unite₊r ⊕ id⟷₁
  pentagon₊l : {t₁ t₂ t₃ t₄ : U} →
    assocr₊ ◎ (assocr₊ {t₁} {t₂} {t₃ + t₄}) ⟷₂
    ((assocr₊ ⊕ id⟷₁) ◎ assocr₊) ◎ (id⟷₁ ⊕ assocr₊)
  pentagon₊r : {t₁ t₂ t₃ t₄ : U} →
    ((assocr₊ {t₁} {t₂} {t₃} ⊕ id⟷₁ {t₄}) ◎ assocr₊) ◎ (id⟷₁ ⊕ assocr₊) ⟷₂
    assocr₊ ◎ assocr₊
  -- unit coherence
  unite₊l-coh-l : {t₁ : U} → unite₊l {t₁} ⟷₂ swap₊ ◎ unite₊r
  unite₊l-coh-r : {t₁ : U} → swap₊ ◎ unite₊r ⟷₂ unite₊l {t₁}
  hexagonr₊l : {t₁ t₂ t₃ : U} →
    (assocr₊ ◎ swap₊) ◎ assocr₊ {t₁} {t₂} {t₃} ⟷₂
    ((swap₊ ⊕ id⟷₁) ◎ assocr₊) ◎ (id⟷₁ ⊕ swap₊)
  hexagonr₊r : {t₁ t₂ t₃ : U} →
    ((swap₊ ⊕ id⟷₁) ◎ assocr₊) ◎ (id⟷₁ ⊕ swap₊) ⟷₂
    (assocr₊ ◎ swap₊) ◎ assocr₊ {t₁} {t₂} {t₃}
  hexagonl₊l : {t₁ t₂ t₃ : U} →
    (assocl₊ ◎ swap₊) ◎ assocl₊ {t₁} {t₂} {t₃} ⟷₂
    ((id⟷₁ ⊕ swap₊) ◎ assocl₊) ◎ (swap₊ ⊕ id⟷₁)
  hexagonl₊r : {t₁ t₂ t₃ : U} →
    ((id⟷₁ ⊕ swap₊) ◎ assocl₊) ◎ (swap₊ ⊕ id⟷₁) ⟷₂
    (assocl₊ ◎ swap₊) ◎ assocl₊ {t₁} {t₂} {t₃}

-- Braiding compatible with unitors (redundant; provable from above
-- axioms. See for example Thm. 10 in "On MacLane's Conditions for
-- Coherence of Natural Associativities, Commutativities, etc.
-- Kelly 1964)
unit-braid : unite₊l {O} ⟷₂ swap₊ ◎ unite₊l
unit-braid = TODO! -- see above comment

braid-unit : swap₊ ◎ unite₊l ⟷₂ unite₊l {O}
braid-unit = TODO! -- see above comment

-- Equational reasoning

infixr 10 _⟷₂⟨_⟩_
infix  15 _⟷₂∎

_⟷₂⟨_⟩_ : ∀ {t₁ t₂ : U} (c₁ : t₁ ⟷₁ t₂) {c₂ c₃ : t₁ ⟷₁ t₂} →
         (c₁ ⟷₂ c₂) → (c₂ ⟷₂ c₃) → (c₁ ⟷₂ c₃)
_ ⟷₂⟨ β ⟩ γ = trans⟷₂ β γ

_⟷₂∎ : ∀ {t₁ t₂ : U} (c : t₁ ⟷₁ t₂) → c ⟷₂ c
_ ⟷₂∎ = id⟷₂

-- Coherence

!⟷₁!⟷₁ : {t₁ t₂ : U} → (c : t₁ ⟷₁ t₂) → (!⟷₁ (!⟷₁ c) ⟷₂ c)
!⟷₁!⟷₁ unite₊l = id⟷₂
!⟷₁!⟷₁ uniti₊l = id⟷₂
!⟷₁!⟷₁ swap₊ = id⟷₂
!⟷₁!⟷₁ assocl₊ = id⟷₂
!⟷₁!⟷₁ assocr₊ = id⟷₂
!⟷₁!⟷₁ id⟷₁ = id⟷₂
!⟷₁!⟷₁ (c ◎ c₁) = !⟷₁!⟷₁ c ⊡ !⟷₁!⟷₁ c₁
!⟷₁!⟷₁ (c ⊕ c₁) = resp⊕⟷₂ (!⟷₁!⟷₁ c) (!⟷₁!⟷₁ c₁)

!⟷₂ : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷₁ t₂} → (α : c₁ ⟷₂ c₂) → (c₂ ⟷₂ c₁)
!⟷₂ assoc◎l = assoc◎r
!⟷₂ assoc◎r = assoc◎l
!⟷₂ assocl₊l = assocl₊r
!⟷₂ assocl₊r = assocl₊l
!⟷₂ assocr₊r = assocr₊l
!⟷₂ assocr₊l = assocr₊r
!⟷₂ idl◎l = idl◎r
!⟷₂ idl◎r = idl◎l
!⟷₂ idr◎l = idr◎r
!⟷₂ idr◎r = idr◎l
!⟷₂ linv◎l = linv◎r
!⟷₂ linv◎r = linv◎l
!⟷₂ rinv◎l = rinv◎r
!⟷₂ rinv◎r = rinv◎l
!⟷₂ unite₊l⟷₂l = unite₊l⟷₂r
!⟷₂ unite₊l⟷₂r = unite₊l⟷₂l
!⟷₂ uniti₊l⟷₂l = uniti₊l⟷₂r
!⟷₂ uniti₊l⟷₂r = uniti₊l⟷₂l
!⟷₂ swapl₊⟷₂ = swapr₊⟷₂
!⟷₂ swapr₊⟷₂ = swapl₊⟷₂
!⟷₂ id⟷₂ = id⟷₂
!⟷₂ (trans⟷₂ c c₁) = trans⟷₂ (!⟷₂ c₁) (!⟷₂ c)
!⟷₂ (c ⊡ c₁) = !⟷₂ c ⊡ !⟷₂ c₁
!⟷₂ (resp⊕⟷₂ c c₁) = resp⊕⟷₂ (!⟷₂ c) (!⟷₂ c₁)
!⟷₂ id⟷₁⊕id⟷₁⟷₂ = split⊕-id⟷₁
!⟷₂ split⊕-id⟷₁ = id⟷₁⊕id⟷₁⟷₂
!⟷₂ hom⊕◎⟷₂ = hom◎⊕⟷₂
!⟷₂ hom◎⊕⟷₂ = hom⊕◎⟷₂
!⟷₂ triangle₊l = triangle₊r
!⟷₂ triangle₊r = triangle₊l
!⟷₂ pentagon₊l = pentagon₊r
!⟷₂ pentagon₊r = pentagon₊l
!⟷₂ unite₊l-coh-l = unite₊l-coh-r
!⟷₂ unite₊l-coh-r = unite₊l-coh-l
!⟷₂ hexagonr₊l = hexagonr₊r
!⟷₂ hexagonr₊r = hexagonr₊l
!⟷₂ hexagonl₊l = hexagonl₊r
!⟷₂ hexagonl₊r = hexagonl₊l
-- !⟷₂ unit-braid = braid-unit
-- !⟷₂ braid-unit = unit-braid

!⟷₁⟷₂ : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷₁ t₂} → (α : c₁ ⟷₂ c₂) → (!⟷₁ c₁ ⟷₂ !⟷₁ c₂)
!⟷₁⟷₂ assoc◎l = assoc◎r
!⟷₁⟷₂ assoc◎r = assoc◎l
!⟷₁⟷₂ assocl₊l = assocr₊l
!⟷₁⟷₂ assocl₊r = assocr₊r
!⟷₁⟷₂ assocr₊r = assocl₊r
!⟷₁⟷₂ assocr₊l = assocl₊l
!⟷₁⟷₂ idl◎l = idr◎l
!⟷₁⟷₂ idl◎r = idr◎r
!⟷₁⟷₂ idr◎l = idl◎l
!⟷₁⟷₂ idr◎r = idl◎r
!⟷₁⟷₂ linv◎l = rinv◎l
!⟷₁⟷₂ linv◎r = rinv◎r
!⟷₁⟷₂ rinv◎l = linv◎l
!⟷₁⟷₂ rinv◎r = linv◎r
!⟷₁⟷₂ unite₊l⟷₂l = uniti₊l⟷₂r
!⟷₁⟷₂ unite₊l⟷₂r = uniti₊l⟷₂l
!⟷₁⟷₂ uniti₊l⟷₂l = unite₊l⟷₂r
!⟷₁⟷₂ uniti₊l⟷₂r = unite₊l⟷₂l
!⟷₁⟷₂ swapl₊⟷₂ = swapr₊⟷₂
!⟷₁⟷₂ swapr₊⟷₂ = swapl₊⟷₂
!⟷₁⟷₂ id⟷₂ = id⟷₂
!⟷₁⟷₂ (trans⟷₂ α β) = trans⟷₂ (!⟷₁⟷₂ α) (!⟷₁⟷₂ β)
!⟷₁⟷₂ (α ⊡ β) = !⟷₁⟷₂ β ⊡ !⟷₁⟷₂ α
!⟷₁⟷₂ (resp⊕⟷₂ α β) = resp⊕⟷₂ (!⟷₁⟷₂ α) (!⟷₁⟷₂ β)
!⟷₁⟷₂ id⟷₁⊕id⟷₁⟷₂ = id⟷₁⊕id⟷₁⟷₂
!⟷₁⟷₂ split⊕-id⟷₁ = split⊕-id⟷₁
!⟷₁⟷₂ hom⊕◎⟷₂ = hom⊕◎⟷₂
!⟷₁⟷₂ hom◎⊕⟷₂ = hom◎⊕⟷₂
!⟷₁⟷₂ triangle₊l =
  ((uniti₊l ◎ swap₊) ⊕ id⟷₁)
    ⟷₂⟨ TODO- ⟩ -- same as Indexed
  ((id⟷₁ ⊕ uniti₊l) ◎ assocl₊) ⟷₂∎
!⟷₁⟷₂ triangle₊r =
  ((id⟷₁ ⊕ uniti₊l) ◎ assocl₊)
    ⟷₂⟨ TODO- ⟩ -- same as Indexed
  ((uniti₊l ◎ swap₊) ⊕ id⟷₁) ⟷₂∎
!⟷₁⟷₂ pentagon₊l = TODO- -- same as Indexed
!⟷₁⟷₂ pentagon₊r = TODO- -- same as Indexed
!⟷₁⟷₂ unite₊l-coh-l = TODO- -- same as Indexed
!⟷₁⟷₂ unite₊l-coh-r = TODO- -- same as Indexed
!⟷₁⟷₂ hexagonr₊l = trans⟷₂ (trans⟷₂ assoc◎l hexagonl₊l) assoc◎r
!⟷₁⟷₂ hexagonr₊r = trans⟷₂ (trans⟷₂ assoc◎l hexagonl₊r) assoc◎r
!⟷₁⟷₂ hexagonl₊l = trans⟷₂ (trans⟷₂ assoc◎l hexagonr₊l) assoc◎r
!⟷₁⟷₂ hexagonl₊r = trans⟷₂ (trans⟷₂ assoc◎l hexagonr₊r) assoc◎r

-- 3-combinators trivial

data _⟷₃_ : {X Y : U} {p q : X ⟷₁ Y} → (p ⟷₂ q) → (p ⟷₂ q) → Set where
  trunc : {X Y : U} {p q : X ⟷₁ Y} (α β : p ⟷₂ q) → α ⟷₃ β

--