text:
import cedille-options
open import general-util

module untyped-spans (options : cedille-options.options) {F : Set → Set} ⦃ monadF : monad F ⦄ where

open import ctxt
open import cedille-types
open import constants
open import conversion
open import free-vars
open import rename
open import spans options {F} ⦃ monadF ⦄
open import subst
open import syntax-util
open import to-string options
open import type-util
open import elab-util options

{-# TERMINATING #-}
untyped-term : ctxt → ex-tm → spanM term
untyped-type : ctxt → ex-tp → spanM type
untyped-kind : ctxt → ex-kd → spanM kind
untyped-tpkd : ctxt → ex-tk → spanM tpkd
untyped-arg : ctxt → ex-arg → spanM arg
untyped-args : ctxt → ex-args → spanM args
untyped-let : ctxt → ex-def → erased? → posinfo → posinfo → spanM (ctxt × var × tagged-val × (∀ {ed : exprd} → ⟦ ed ⟧ → ⟦ ed ⟧) × (term → term))
untyped-cases : ctxt → ex-cases → renamectxt → spanM cases
untyped-case : ctxt → ex-case → (siblings : ℕ) → (ℕ → err-m) → renamectxt → spanM (case × (ℕ → err-m) × maybe ℕ)

untyped-let Γ (ExDefTerm pi x Tₑ? t) e? fm to =
  maybe-map (untyped-type Γ) Tₑ? >>=? λ Tₑ?~ →
  untyped-term Γ t >>= λ t~ →
  elim-pair (compileFail-in Γ t~) λ tvs e →
  let Tₑ~ = maybe-else' Tₑ?~ (TpHole pi) id in
  [- Var-span (Γ , pi - x :` Tkt Tₑ~) pi x untyped tvs e -]
  return
    (ctxt-term-def pi localScope opacity-open x (just t~) Tₑ~ Γ ,
     pi % x ,
     binder-data Γ pi x (Tkt Tₑ~) e? (just t~) fm to ,
     (λ {ed} T' → [ Γ - t~ / (pi % x) ] T') ,
     (λ t' → LetTm e? x nothing t~ ([ Γ - Var x / (pi % x) ] t')))

untyped-let Γ (ExDefType pi x k T) e? fm to =
  untyped-kind Γ k >>= λ k~ →
  untyped-type Γ T >>= λ T~ →
  [- TpVar-span (Γ , pi - x :` Tkk k~) pi x untyped [] nothing -]
  return
    (ctxt-type-def pi localScope opacity-open x (just T~) k~ Γ ,
     pi % x ,
     binder-data Γ pi x (Tkk k~) e? (just T~) fm to ,
     (λ {ed} T' → [ Γ - T~ / (pi % x) ] T') ,
     (λ t' → LetTp x k~ T~ ([ Γ - TpVar x / (pi % x) ] t')))

untyped-term Γ (ExApp t e t') =
  [- App-span tt (term-start-pos t) (term-end-pos t') untyped [] nothing -]
  untyped-term Γ t >>= λ t~ →
  untyped-term Γ t' >>= λ t'~ →
  return (if e then t~ else App t~ t'~)

untyped-term Γ (ExAppTp t T) =
  [- AppTp-span tt (term-start-pos t) (type-end-pos T) untyped [] nothing -]
  untyped-type Γ T >>= λ T~ →
  untyped-term Γ t

untyped-term Γ (ExBeta pi t? t?') =
  maybe-map (λ {(PosTm t pi) → untyped-term Γ t}) t? >>=? λ t?~ →
  maybe-map (λ {(PosTm t pi) → untyped-term Γ t}) t?' >>=? λ t?'~ →
  [- Beta-span pi (term-end-pos (ExBeta pi t? t?')) untyped [] nothing -]
  return (maybe-else' t?'~ id-term id)

untyped-term Γ (ExChi pi T? t) =
  maybe-map (untyped-type Γ) T? >>=? λ T?~ →
  [- Chi-span Γ pi T?~ t untyped [] nothing -]
  untyped-term Γ t

untyped-term Γ (ExDelta pi T? t) =
  [- Delta-span pi t untyped [] nothing -]
  maybe-map (untyped-type Γ) T? >>=? λ T?~ →
  untyped-term Γ t >>= λ t~ →
  return id-term

untyped-term Γ (ExEpsilon pi lr -? t) =
  [- Epsilon-span pi lr -? t untyped [] nothing -]
  untyped-term Γ t

untyped-term Γ (ExHole pi) =
  [- hole-span Γ pi nothing untyped [] -]
  return (Hole pi)

untyped-term Γ (ExIotaPair pi t₁ t₂ Tₘ? pi') =
  let tv-f = λ {(ExGuide pi'' x Tₘ) →
               [ binder-data Γ pi'' x (Tkt (TpHole pi'')) ff nothing
                   (type-start-pos Tₘ) (type-end-pos Tₘ) ]} in
  [- IotaPair-span pi pi' untyped (maybe-else' Tₘ? [] tv-f) nothing -]
  untyped-term Γ t₁ >>= λ t₁~ →
  untyped-term Γ t₂ >>= λ t₂~ →
  maybe-map (λ {(ExGuide pi'' x Tₘ) →
    untyped-type (ctxt-term-decl pi'' x (TpHole pi'') Γ) Tₘ}) Tₘ? >>=? λ Tₘ?~ →
  return t₁~

untyped-term Γ (ExIotaProj t n pi) =
  [- IotaProj-span t pi untyped [] nothing -]
  untyped-term Γ t

untyped-term Γ (ExLam pi e pi' x tk? t) =
  (return tk? on-fail return (Tkt (TpHole pi')) >>=m untyped-tpkd Γ) >>= λ tk~ →
  untyped-term (Γ , pi' - x :` tk~) t >>= λ t~ →
  let eₖ? = tk? >>= λ _ → ifMaybej (tk-is-type tk~ && ~ e)
                             "λ-terms must bind a term, not a type (use Λ instead)"
      eₑ? = ifMaybej (e && is-free-in (pi' % x) (erase t~))
               "The Λ-bound variable occurs free in the erasure of the body" in
  [- var-span e (Γ , pi' - x :` tk~) pi' x untyped tk~ eₑ? -]
  [- Lam-span Γ untyped pi pi' e x tk~ t [] eₖ? -]
  return (if e then t~ else Lam ff x nothing ([ Γ - Var x / (pi' % x) ] t~))

untyped-term Γ (ExLet pi e? d t) =
  untyped-let Γ d e? (term-start-pos t) (term-end-pos t) >>= λ where
    (Γ' , x , tv , σ , f) →
      untyped-term Γ' t >>= λ t~ →
      [- punctuation-span "Parens (let)" pi (term-end-pos t) -]
      [- Let-span e? pi (term-end-pos t) untyped []
           (ifMaybej (e? && is-free-in x t~)
             (unqual-local x ^ "occurs free in the body of the term")) -]
      return (if is-free-in x t~ then f t~ else t~)

untyped-term Γ (ExOpen pi o pi' x t) =
  [- Var-span Γ pi' x untyped [ not-for-navigation ] nothing -]
  [- Open-span o pi x t untyped [] nothing -]
  untyped-term Γ t

untyped-term Γ (ExParens pi t pi') =
  [- punctuation-span "Parens (term)" pi pi' -]
  untyped-term Γ t

untyped-term Γ (ExPhi pi t₌ t₁ t₂ pi') =
  [- Phi-span pi pi' untyped [] nothing -]
  untyped-term Γ t₌ >>
  untyped-term Γ t₁ >>
  untyped-term Γ t₂

untyped-term Γ (ExRho pi ρ+? ρ<ns>? t₌ Tₘ? t) =
  [- Rho-span pi t₌ t untyped ρ+?
       (maybe-else' Tₘ? (inj₁ 1) λ {(ExGuide pi' x Tₘ) → inj₂ x}) [] nothing -]
  untyped-term Γ t₌ >>
  maybe-map (λ {(ExGuide pi' x Tₘ) →
                  untyped-type (ctxt-var-decl-loc pi' x Γ) Tₘ}) Tₘ? >>=? λ Tₘ?~ →
  untyped-term Γ t

untyped-term Γ (ExVarSigma pi t) =
  [- VarSigma-span pi t untyped [] nothing -]
  untyped-term Γ t

untyped-term Γ (ExTheta pi θ t ts) =
  [- Theta-span Γ pi θ t ts untyped [] nothing -]
  untyped-term Γ t >>= λ t~ →
  untyped-args Γ (map (λ {(Lterm e t) → ExTmArg e t}) ts) >>= λ as~ →
  return (recompose-apps (map Arg (erase-args as~)) t~)

untyped-term Γ (ExMu pi pi''' x t Tₘ? pi' ms pi'') =
  untyped-term Γ t >>= λ t~ →
  maybe-map (untyped-type Γ) Tₘ? >>=? λ Tₘ~? →
   [- Var-span Γ pi''' x untyped [] nothing -]
      let Γ' = ctxt-term-decl pi''' x (TpHole pi''') Γ
          ρ = renamectxt-single (pi''' % x) x
          tvs = [ binder-data Γ' pi''' x (Tkt (TpHole pi''')) ff nothing pi' pi'' ] in
      untyped-cases Γ' ms ρ >>= λ ms~ →
      -- Make sure we aren't matching upon a "False" datatype (e.g., one
      -- with no constructors) before any datatypes have been declared
      maybe-else' (head2 (trie-mappings (ctxt.μ Γ)))
        ([- Mu-span Γ pi pi'' Tₘ~? untyped tvs
              (just "No datatypes have been declared yet") -]
         return (Hole pi))
        λ where
          (Dₓ , ps , kᵢ , k , cs , eds , ecs) →
            [- Mu-span Γ pi pi'' Tₘ~? untyped tvs nothing -]
            return (Mu x t~ nothing (mk-data-info Dₓ Dₓ (params-to-args ps) [] ps kᵢ k cs cs eds ecs) ms~)
untyped-term Γ (ExSigma pi t? t Tₘ? pi' ms pi'') =
  untyped-term Γ t >>= λ t~ →
  maybe-map (untyped-type Γ) Tₘ? >>=? λ Tₘ~? →
      maybe-map (untyped-term Γ) t? >>=? λ t~? →
      let ρ = empty-renamectxt
          μ~ = t~?
          tvs = [] in
      untyped-cases Γ ms ρ >>= λ ms~ →
      -- Make sure we aren't matching upon a "False" datatype (e.g., one
      -- with no constructors) before any datatypes have been declared
      maybe-else' (head2 (trie-mappings (ctxt.μ Γ)))
        ([- Mu-span Γ pi pi'' Tₘ~? untyped tvs
              (just "No datatypes have been declared yet") -]
         return (Hole pi))
        λ where
          (Dₓ , ps , kᵢ , k , cs , eds , ecs) →
            [- Mu-span Γ pi pi'' Tₘ~? untyped tvs nothing -]
            return (Sigma μ~ t~ nothing (mk-data-info Dₓ Dₓ (params-to-args ps) [] ps kᵢ k cs cs eds ecs) ms~)

-- x
untyped-term Γ (ExVar pi x) =
  maybe-else' (ctxt-binds-term-var Γ x)
    ([- Var-span Γ pi x untyped [] (just "Not a term variable") -]
    return (Var x))
    λ {(qx , as) →
      [- Var-span Γ pi x untyped [] nothing -]
      return (recompose-apps (map Arg (erase-args as)) (Var qx))}

-- ∀/Π x : tk. T
untyped-type Γ (ExTpAbs pi e pi' x tk T) =
  untyped-tpkd Γ tk >>= λ tk~ →
  untyped-type (Γ , pi' - x :` tk~) T >>= λ T~ →
  let T~ = rename-var Γ (pi' % x) x T~ in
  [- punctuation-span "Forall" pi (posinfo-plus pi 1) -]
  [- var-span e (Γ , pi' - x :` tk~) pi' x untyped tk~ nothing -]
  [- TpQuant-span Γ e pi pi' x tk~ T untyped [] nothing -]
  return (TpAbs e x tk~ T~)

-- ι x : T₁. T₂
untyped-type Γ (ExTpIota pi pi' x T₁ T₂) =
  untyped-type Γ T₁ >>= λ T₁~ →
  untyped-type (Γ , pi' - x :` Tkt T₁~) T₂ >>= λ T₂~ →
  let T₂~ = rename-var Γ (pi' % x) x T₂~ in
  [- punctuation-span "Forall" pi (posinfo-plus pi 1) -]
  [- var-span ff (Γ , pi' - x :` Tkt T₁~) pi' x untyped (Tkt T₁~) nothing -]
  [- Iota-span Γ pi pi' x T₂~ T₂ untyped [] nothing -]
  return (TpIota x T₁~ T₂~)

-- {^ T ^} (generated by theta)
untyped-type Γ (ExTpNoSpans T pi) = untyped-type Γ T >>=spand return

-- [d] - T
untyped-type Γ (ExTpLet pi d T) =
  untyped-let Γ d ff (type-start-pos T) (type-end-pos T) >>= λ where
    (Γ' , x , tv , σ , f) →
      untyped-type Γ' T >>= λ T~ →
      [- punctuation-span "Parens (let)" pi (type-end-pos T) -]
      [- TpLet-span pi (type-end-pos T) untyped [ tv ] -]
      return (σ T~)

-- T · T'
untyped-type Γ (ExTpApp T T') =
  untyped-type Γ T >>= λ T~ →
  untyped-type Γ T' >>= λ T'~ →
  [- TpApp-span (type-start-pos T) (type-end-pos T) untyped [] nothing -]
  return (TpAppTp T~ T'~)

-- T t
untyped-type Γ (ExTpAppt T t) =
  untyped-type Γ T >>= λ T~ →
  untyped-term Γ t >>= λ t~ →
  [- TpAppt-span (type-start-pos T) (term-end-pos t) untyped [] nothing -]
  return (TpAppTm T~ t~)

-- T ➔/➾ T'
untyped-type Γ (ExTpArrow T e T') =
  untyped-type Γ T >>= λ T~ →
  untyped-type Γ T' >>= λ T'~ →
  [- TpArrow-span T T' untyped [] nothing -]
  return (TpAbs e ignored-var (Tkt T~) T'~)

-- { t₁ ≃ t₂ }
untyped-type Γ (ExTpEq pi t₁ t₂ pi') =
  untyped-term Γ t₁ >>= λ t₁~ →
  untyped-term Γ t₂ >>= λ t₂~ →
  [- punctuation-span "Parens (equation)" pi pi' -]
  [- TpEq-span pi pi' untyped [] nothing -]
  return (TpEq t₁~ t₂~)

-- ●
untyped-type Γ (ExTpHole pi) =
  [- tp-hole-span Γ pi nothing untyped [] -]
  return (TpHole pi)

-- λ x : tk. T
untyped-type Γ (ExTpLam pi pi' x tk T) =
  untyped-tpkd Γ tk >>= λ tk~ →
  untyped-type (Γ , pi' - x :` tk~) T >>= λ T~ →
  [- punctuation-span "Lambda (type)" pi (posinfo-plus pi 1) -]
  [- var-span ff (Γ , pi' - x :` tk~) pi' x untyped tk~ nothing -]
  [- TpLambda-span Γ pi pi' x tk~ T untyped [] nothing -]
  return (TpLam x tk~ (rename-var Γ (pi' % x) x T~))

-- (T)
untyped-type Γ (ExTpParens pi T pi') =
  [- punctuation-span "Parens (type)" pi pi' -]
  untyped-type Γ T

-- x
untyped-type Γ (ExTpVar pi x) =
  maybe-else' (ctxt-binds-type-var Γ x)
    ([- TpVar-span Γ pi x untyped [] (just "Undefined type variable") -]
     return (TpVar x))
    λ {(qx , as) →
      [- TpVar-span Γ pi x untyped [] nothing -]
      return (apps-type (TpVar qx) (erase-args-keep as))}

-- Π x : tk. k
untyped-kind Γ (ExKdAbs pi pi' x tk k) =
  untyped-tpkd Γ tk >>= λ tk~ →
  untyped-kind (Γ , pi' - x :` tk~) k >>= λ k~ →
  [- KdAbs-span Γ pi pi' x tk~ k untyped nothing -]
  [- var-span ff (Γ , pi' - x :` tk~) pi' x untyped tk~ nothing -]
  [- punctuation-span "Pi (kind)" pi (posinfo-plus pi 1) -]
  return (KdAbs x tk~ (rename-var Γ (pi' % x) x k~))

-- tk ➔ k
untyped-kind Γ (ExKdArrow tk k) =
  untyped-tpkd Γ tk >>= λ tk~ →
  untyped-kind Γ k >>= λ k~ →
  [- KdArrow-span tk k untyped nothing -]
  return (KdAbs ignored-var tk~ k~)

-- ●
untyped-kind Γ (ExKdHole pi) =
  [- kd-hole-span pi untyped -]
  return (KdHole pi)

-- (k)
untyped-kind Γ (ExKdParens pi k pi') =
  [- punctuation-span "Parens (kind)" pi pi' -]
  untyped-kind Γ k

-- ★
untyped-kind Γ (ExKdStar pi) =
  [- Star-span pi untyped nothing -]
  return KdStar

-- κ as...
untyped-kind Γ (ExKdVar pi κ as) =
  case ctxt-lookup-kind-var-def Γ κ of λ where
    nothing →
      [- KdVar-span Γ (pi , κ) (args-end-pos (posinfo-plus-str pi κ) as) [] untyped []
           (just "Undefined kind variable") -]
      return (KdHole pi)
    (just (ps , k)) →
      untyped-args Γ as >>= λ as~ →
      [- KdVar-span Γ (pi , κ)
           (args-end-pos (posinfo-plus-str pi κ) as)
           ps untyped (params-data Γ ps)
           (unless (length as =ℕ length ps)
             ("Expected " ^ ℕ-to-string (length ps) ^
              " argument" ^ (if length ps =ℕ 1 then "" else "s") ^
              ", but got " ^ ℕ-to-string (length as))) -]
      return (fst (subst-params-args' Γ ps as~ k))

untyped-arg Γ (ExTmArg ff t) = inj₁ <$> untyped-term Γ t
untyped-arg Γ (ExTmArg tt t) = (inj₂ ∘ inj₁) <$> untyped-term Γ t
untyped-arg Γ (ExTpArg T) = (inj₂ ∘ inj₂) <$> untyped-type Γ T

untyped-args Γ = sequenceA ∘ map (untyped-arg Γ)

untyped-tpkd Γ (ExTkt T) = Tkt <$> untyped-type Γ T
untyped-tpkd Γ (ExTkk k) = Tkk <$> untyped-kind Γ k

untyped-cases Γ ms ρ =
  let msₗ = length ms in
  foldl (λ m rec ms f → untyped-case Γ m msₗ f ρ >>= uncurry₂ λ m asₗ n? → rec (maybe-else' n? ms (λ n → set-nth n (just m) ms)) asₗ)
    (const ∘ return) ms (repeat (length ms) nothing) (λ _ → nothing) >>=r drop-nothing

untyped-case-args : ctxt → posinfo → ex-case-args → ex-tm → renamectxt → spanM (case-args × term)
untyped-case-args Γ pi cas t ρ =
  foldr {B = ctxt → renamectxt → 𝕃 tagged-val → (term → spanM ⊤) → spanM (case-args × term)}
    (λ {(ExCaseArg me pi x) rec Γ' ρ tvs sm →
      let tk = case me of λ {ExCaseArgTp → Tkk (KdHole pi-gen);
                             ExCaseArgTm → Tkt (TpHole pi-gen);
                             ExCaseArgEr → Tkt (TpHole pi-gen)} in
      rec
        (ctxt-tk-decl pi x tk Γ')
        (renamectxt-insert ρ (pi % x) x)
        (binder-data Γ' pi x tk (ex-case-arg-erased me) nothing
          (term-start-pos t) (term-end-pos t) :: tvs)
        (λ t →
          [- var-span (ex-case-arg-erased me) Γ' pi x untyped tk
            (when (ex-case-arg-erased me && is-free-in (pi % x) (erase t))
              "The bound variable occurs free in the erasure of the body (not allowed)") -]
          sm t) >>=c λ cas →
      return2 (case me of λ {ExCaseArgTm → CaseArg ff x nothing :: cas; _ → cas})})
    (λ Γ' ρ tvs sm →
      [- pattern-clause-span pi t (reverse tvs) -]
      untyped-term Γ' t >>= λ t~ →
      sm t~ >>
      return2 [] (subst-renamectxt Γ' ρ t~))
    cas Γ ρ [] λ _ → spanMok

untyped-case Γ (ExCase pi x cas t) csₗ asₗ ρ =
  untyped-case-args Γ pi cas t ρ >>=c λ cas~ t~ →
  case (qual-lookup Γ x) of λ where
    (just (qx , as , ctr-def ps T Cₗ cᵢ cₐ , loc)) →
      let c~ = Case qx cas~ t~ []
          eᵢ = "This constructor overlaps with " ^ x
          eₐ = unless (length cas~ =ℕ cₐ)
                 ("Expected " ^ ℕ-to-string cₐ ^
                  " arguments after erasure, but got " ^ ℕ-to-string (length cas~))
          eₗ = unless (Cₗ =ℕ csₗ)
                 ("Constructor's datatype has " ^ ℕ-to-string Cₗ ^
                  (if Cₗ =ℕ 1 then " constructor" else " constructors") ^
                  ", but expected " ^ ℕ-to-string csₗ) in
      [- Var-span Γ pi x untyped [] (asₗ cᵢ ||-maybe (eₐ ||-maybe eₗ)) -]
      return2 c~ ((λ cᵢ' → when (cᵢ =ℕ cᵢ') eᵢ) , (maybe-not (asₗ cᵢ) >> just cᵢ))
    _ →
      [- Var-span Γ pi x untyped [] (just $ "This is not a valid constructor name") -]
      return2 (Case x cas~ t~ []) (asₗ , nothing)


text:
module AlonzoPrelude where
  open import RTN public
  import RTP  -- magic module - Run Time Primitives

  Int : Set
  Int = RTP.Int

  Float : Set
  Float = RTP.Float

  String : Set
  String = RTP.String

  Char : Set
  Char = RTP.Char

  data True : Set where
    tt : True

{-
  record True : Set where

  tt : True
  tt = record{}
-}
  data False : Set where

  elim-False : {A : Set} -> False -> A
  elim-False ()

  -- _∘_ : {A,B,C:Set} -> (B -> C) -> (A -> B) -> A -> C
  -- f ∘ g = \x -> f (g x)

  id : {A : Set} -> A -> A
  id x = x

  infixr 90 _○_
  _○_ : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
  (f ○ g) x = f (g x)

  infixr 0 _$_
  _$_ : {A B : Set} -> (A -> B) -> A -> B
  f $ x = f x

  flip : {A B C : Set} -> (A -> B -> C) -> B -> A -> C
  flip f x y = f y x

  const : {A B : Set} -> A -> B -> A
  const x _ = x

  typeOf : {A : Set} -> A -> Set
  typeOf {A} _ = A

  data _×_ (A B : Set) : Set where
    <_,_> : A -> B -> A × B

  fst : {A B : Set} -> A × B -> A
  fst < x , y > = x

  snd : {A B : Set} -> A × B -> B
  snd < x , y > = y

{-
  infixr 10 _::_
  data List (A:Set) : Set where
    nil  : List A
    _::_ : A -> List A -> List A

  [_] : {A:Set} -> A -> List A
  [ x ] = x :: nil
-}
  {-# BUILTIN INTEGER Int    #-}
--  {-# BUILTIN STRING  String #-}
--   {-# BUILTIN FLOAT   Float  #-}
  {-# BUILTIN CHAR    Char   #-}

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.Block             as Block
import      LibraBFT.Impl.Execution.ExecutorTypes.StateComputeResult as StateComputeResult
import      LibraBFT.Impl.OBM.Crypto                                 as Crypto
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.ConsensusTypes.ExecutedBlock where

isNilBlock : ExecutedBlock → Bool
isNilBlock eb = Block.isNilBlock (eb ^∙ ebBlock)

blockInfo : ExecutedBlock → BlockInfo
blockInfo eb =
  Block.genBlockInfo
    (eb ^∙ ebBlock)
    (Crypto.obmHashVersion -- OBM-LBFT-DIFF - see SafetyRules.extensionCheck
      (eb ^∙ ebStateComputeResult ∙ scrObmNumLeaves))
    (eb ^∙ ebStateComputeResult ∙ scrObmNumLeaves)
    (eb ^∙ ebStateComputeResult ∙ scrEpochState)

maybeSignedVoteProposal : ExecutedBlock → MaybeSignedVoteProposal
maybeSignedVoteProposal self =
  MaybeSignedVoteProposal∙new
    (VoteProposal∙new (StateComputeResult.extensionProof (self ^∙ ebStateComputeResult))
                      (self ^∙ ebBlock)
                      (self ^∙ ebStateComputeResult ∙ scrEpochState))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bisimilarity for Covecs
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe --sized-types #-}

module Codata.Covec.Bisimilarity where

open import Level using (_⊔_)
open import Size
open import Codata.Thunk
open import Codata.Conat hiding (_⊔_)
open import Codata.Covec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)

data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) :
           ∀ m n (xs : Covec A ∞ m) (ys : Covec B ∞ n) → Set (r ⊔ a ⊔ b) where
  []  : Bisim R i zero zero [] []
  _∷_ : ∀ {x y m n xs ys} → R x y → Thunk^R (λ i → Bisim R i (m .force) (n .force)) i xs ys →
        Bisim R i (suc m) (suc n) (x ∷ xs) (y ∷ ys)

module _ {a r} {A : Set a} {R : A → A → Set r} where

 reflexive : Reflexive R → ∀ {i m} → Reflexive (Bisim R i m m)
 reflexive refl^R {i} {m} {[]}     = []
 reflexive refl^R {i} {m} {r ∷ rs} = refl^R ∷ λ where .force → reflexive refl^R

module _ {a b} {A : Set a} {B : Set b}
         {r} {P : A → B → Set r} {Q : B → A → Set r} where

 symmetric : Sym P Q → ∀ {i m n} → Sym (Bisim P i m n) (Bisim Q i n m)
 symmetric sym^PQ []       = []
 symmetric sym^PQ (p ∷ ps) = sym^PQ p ∷ λ where .force → symmetric sym^PQ (ps .force)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
         {r} {P : A → B → Set r} {Q : B → C → Set r} {R : A → C → Set r} where

 transitive : Trans P Q R → ∀ {i m n p} → Trans (Bisim P i m n) (Bisim Q i n p) (Bisim R i m p)
 transitive trans^PQR []       []       = []
 transitive trans^PQR (p ∷ ps) (q ∷ qs) =
   trans^PQR p q ∷ λ where .force → transitive trans^PQR (ps .force) (qs .force)

-- Pointwise Equality as a Bisimilarity
------------------------------------------------------------------------

module _ {ℓ} {A : Set ℓ} where

 infix 1 _,_⊢_≈_
 _,_⊢_≈_ : ∀ i m → Covec A ∞ m → Covec A ∞ m → Set ℓ
 _,_⊢_≈_ i m = Bisim _≡_ i m m

 refl : ∀ {i m} → Reflexive (i , m ⊢_≈_)
 refl = reflexive Eq.refl

 sym : ∀ {i m} → Symmetric (i , m ⊢_≈_)
 sym = symmetric Eq.sym

 trans : ∀ {i m} → Transitive (i , m ⊢_≈_)
 trans = transitive Eq.trans


text:
------------------------------------------------------------------------
-- Some omniscience principles
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Equality

module Omniscience {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Equality.Decision-procedures eq
open import Excluded-middle eq
open import Function-universe eq hiding (id; _∘_)
open import H-level eq
open import H-level.Closure eq
open import Nat eq

-- I don't know who first stated LPO and WLPO, or who first proved
-- various properties about these principles.

-- The limited principle of omniscience.

LPO : Type
LPO = (f : ℕ → Bool) → (∀ n → f n ≡ false) ⊎ (∃ λ n → f n ≡ true)

-- The weak limited principle of omniscience.

WLPO : Type
WLPO = (f : ℕ → Bool) → Dec (∀ n → f n ≡ false)

-- WLPO is propositional (assuming extensionality).

WLPO-propositional :
  Extensionality lzero lzero →
  Is-proposition WLPO
WLPO-propositional ext =
  Π-closure ext 1 λ f →
  Dec-closure-propositional ext
    (Π-closure ext 1 λ _ →
     Bool-set)

-- LPO implies WLPO.

LPO→WLPO : LPO → WLPO
LPO→WLPO LPO f =
  ⊎-map id
        (uncurry λ n fn≡true ∀n→fn≡false → Bool.true≢false (
           true   ≡⟨ sym fn≡true ⟩
           f n    ≡⟨ ∀n→fn≡false n ⟩∎
           false  ∎))
        (LPO f)

-- WLPO follows from excluded middle (assuming extensionality).
--
-- This follows from LPO→WLPO and LEM→LPO (see below), but this proof
-- is less complicated.

LEM→WLPO : Extensionality lzero lzero → Excluded-middle lzero → WLPO
LEM→WLPO ext em = λ _ → em (Π-closure ext 1 λ _ →
                            Bool-set)

mutual

  -- There is a propositional property that is logically equivalent to
  -- LPO (assuming extensionality).
  --
  -- I think that Escardo has proved some variant of this property. The
  -- proof below uses a technique suggested by Exercise 3.19 in the HoTT
  -- book.

  LPO⇔propositional :
    Extensionality lzero lzero →
    ∃ λ (P : Type) → Is-proposition P × (LPO ⇔ P)
  LPO⇔propositional ext =
    let P , P-prop , LPO⇔ = LPO⇔propositional′ ext in

      (∀ f → P f ⊎ ¬ P f)
    , (Π-closure ext 1 λ f →
       ⊎-closure-propositional
         (flip _$_) (P-prop f) (¬-propositional ext))
    , LPO⇔

  -- A variant of the previous property.

  LPO⇔propositional′ :
    Extensionality lzero lzero →
    ∃ λ (P : (ℕ → Bool) → Type) →
      (∀ f → Is-proposition (P f)) ×
      (LPO ⇔ ∀ f → P f ⊎ ¬ P f)
  LPO⇔propositional′ ext =
      P
    , P-prop
    , (((f : ℕ → Bool) → (∀ n → f n ≡ false) ⊎ (∃ λ n → f n ≡ true))  ↝⟨ (∀-cong _ λ _ →
                                                                            record { to = ≡false→¬P; from = ¬P→≡false }
                                                                              ⊎-cong
                                                                            record { to = ≡true→P; from = Σ-map id proj₁ }) ⟩
       ((f : ℕ → Bool) → ¬ P f ⊎ P f)                                 ↝⟨ (∀-cong _ λ _ → from-bijection ⊎-comm) ⟩□
       ((f : ℕ → Bool) → P f ⊎ ¬ P f)                                 □)
    where
    P = λ (f : ℕ → Bool) →
          ∃ λ n → f n ≡ true × ∀ {m} → m < n → f m ≡ false

    P-prop : ∀ f → Is-proposition (P f)
    P-prop f (n₁ , fn₁≡true , <n₁→≡false) (n₂ , fn₂≡true , <n₂→≡false) =
      Σ-≡,≡→≡
        (case n₁ <⊎≡⊎> n₂ of λ where
          (inj₁ n₁<n₂)        → ⊥-elim (Bool.true≢false (
                                  true   ≡⟨ sym fn₁≡true ⟩
                                  f n₁   ≡⟨ <n₂→≡false n₁<n₂ ⟩∎
                                  false  ∎))
          (inj₂ (inj₁ n₁≡n₂)) → n₁≡n₂
          (inj₂ (inj₂ n₁>n₂)) → ⊥-elim (Bool.true≢false (
                                  true   ≡⟨ sym fn₂≡true ⟩
                                  f n₂   ≡⟨ <n₁→≡false n₁>n₂ ⟩∎
                                  false  ∎)))
        (×-closure 1
           (Bool-set)
           (implicit-Π-closure ext 1 λ _ →
            Π-closure ext 1 λ _ →
            Bool-set)
           _ _)

    ¬P→≡false : ∀ {f} → ¬ (P f) → (∀ n → f n ≡ false)
    ¬P→≡false {f} ¬Pf =
      well-founded-elim _ λ n hyp →
        case inspect (f n) of λ where
          (false , fn≡false) → fn≡false
          (true  , fn≡true)  → ⊥-elim (¬Pf (n , fn≡true , hyp))

    ≡false→¬P : ∀ {f} → (∀ n → f n ≡ false) → ¬ (P f)
    ≡false→¬P {f} ≡false (n , ≡true , _) = Bool.true≢false (
      true   ≡⟨ sym ≡true ⟩
      f n    ≡⟨ ≡false n ⟩∎
      false  ∎)

    ≡true→P : ∀ {f} → (∃ λ n → f n ≡ true) → P f
    ≡true→P {f} (n , fn≡true) =
      helper (≤→≤↑ (zero≤ _)) (λ o<0 → ⊥-elim (≮0 _ o<0))
      where
      helper : ∀ {m} → m ≤↑ n → (∀ {o} → o < m → f o ≡ false) → P f
      helper {m} (≤↑-refl m≡n) <→≡false = n , fn≡true , λ {o} →
                                            o < n        ↝⟨ subst (o <_) (sym m≡n) ⟩
                                            o < m        ↝⟨ <→≡false ⟩□
                                            f o ≡ false  □
      helper {m} (≤↑-step m<n) <→≡false with inspect (f m)
      ... | true  , fm≡true  = m , fm≡true , <→≡false
      ... | false , fm≡false = helper m<n λ {o} o<1+m →
        case ≤→≤↑ o<1+m of λ where
          (≤↑-refl 1+o≡1+m) → f o    ≡⟨ cong f (cancel-suc 1+o≡1+m) ⟩
                              f m    ≡⟨ fm≡false ⟩∎
                              false  ∎
          (≤↑-step 1+o<1+m) → <→≡false (pred-mono (≤↑→≤ 1+o<1+m))

-- LPO follows from excluded middle (assuming extensionality).

LEM→LPO : Extensionality lzero lzero → Excluded-middle lzero → LPO
LEM→LPO ext =
  let P , P-prop , LPO⇔P = LPO⇔propositional′ ext in

  ({P : Type} → Is-proposition P → Dec P)  ↝⟨ _∘ P-prop ⟩
  (∀ f → P f ⊎ ¬ P f)                      ↝⟨ _⇔_.from LPO⇔P ⟩□
  LPO                                      □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --guardedness #-}

module is-lib.InfSys {𝓁} where
  open import is-lib.InfSys.Base {𝓁} public
  open import is-lib.InfSys.Induction {𝓁} public
  open import is-lib.InfSys.Coinduction {𝓁} public
  open import is-lib.InfSys.FlexCoinduction {𝓁} public
  open MetaRule public
  open FinMetaRule public
  open IS public

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module Issue121 where

id : Set → Set
id A = A

data Bool : Set where
  true  : Bool
  false : Bool

F : Bool → Set → Set
F true  = id
F false = id

G : Bool → Set → Set
G true = id
G false = λ A → A

data D : Set where
  nop : (b : Bool) → F b D → D
  bop : (b : Bool) → G b D → D

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Group | G

type
  * : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20
  neg  : *  ->  * | ⊖_ r40

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊖N⊕ᴸ) a |> add (neg (a), a) = unit
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = unit
-}

module Group.Signature where

open import SOAS.Context

open import SOAS.Common

open import SOAS.Syntax.Signature *T public
open import SOAS.Syntax.Build *T public

-- Operator symbols
data Gₒ : Set where
  unitₒ addₒ negₒ : Gₒ

-- Term signature
G:Sig : Signature Gₒ
G:Sig = sig λ
  {  unitₒ  → ⟼₀ *
  ;  addₒ   → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  negₒ   → (⊢₀ *) ⟼₁ *
  }

open Signature G:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
------------------------------------------------------------------------------
-- Properties stated in the Burstall's paper
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.SortList.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Program.SortList.Properties.Totality.BoolI
open import FOTC.Program.SortList.Properties.Totality.ListN-I
open import FOTC.Program.SortList.Properties.Totality.OrdList.FlattenI
open import FOTC.Program.SortList.Properties.Totality.OrdListI
open import FOTC.Program.SortList.Properties.Totality.OrdTreeI
open import FOTC.Program.SortList.Properties.Totality.TreeI
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- Induction on lit.
ind-lit : (A : D → Set) (f : D) → ∀ y₀ {xs} → ListN xs →
          A y₀ →
          (∀ {x} → N x → ∀ y → A y → A (f · x · y)) →
          A (lit f xs y₀)
ind-lit A f y₀ lnnil Ay₀ ih = subst A (sym (lit-[] f y₀)) Ay₀
ind-lit A f y₀ (lncons {i} {is} Ni LNis) Ay₀ ih =
  subst A
        (sym (lit-∷ f i is y₀))
        (ih Ni (lit f is y₀) (ind-lit A f y₀ LNis Ay₀ ih))

------------------------------------------------------------------------------
-- Burstall's lemma: If t is ordered then totree(i, t) is ordered.
toTree-OrdTree : ∀ {item t} → N item → Tree t → OrdTree t →
                 OrdTree (toTree · item · t)
toTree-OrdTree {item} Nitem tnil _ =
  ordTree (toTree · item · nil)
    ≡⟨ subst (λ x → ordTree (toTree · item · nil) ≡
                    ordTree x)
             (toTree-nil item)
             refl
    ⟩
  ordTree (tip item)
    ≡⟨ ordTree-tip item ⟩
  true ∎

toTree-OrdTree {item} Nitem (ttip {i} Ni) _ =
  case prf₁ prf₂ (x>y∨x≤y Ni Nitem)
  where
  prf₁ : i > item → OrdTree (toTree · item · tip i)
  prf₁ i>item =
    ordTree (toTree · item · tip i)
      ≡⟨ subst (λ t → ordTree (toTree · item · tip i) ≡ ordTree t)
               (toTree-tip item i)
               refl
      ⟩
    ordTree (if (le i item)
               then (node (tip i) item (tip item))
               else (node (tip item) i (tip i)))
      ≡⟨ subst (λ t → ordTree (if (le i item)
                                 then (node (tip i) item (tip item))
                                 else (node (tip item) i (tip i))) ≡
                      ordTree (if t
                                 then (node (tip i) item (tip item))
                                 else (node (tip item) i (tip i))))
               (x>y→x≰y Ni Nitem i>item)
                 refl
      ⟩
    ordTree (if false
               then (node (tip i) item (tip item))
               else (node (tip item) i (tip i)))
      ≡⟨ subst (λ t → ordTree (if false
                                 then (node (tip i) item (tip item))
                                 else (node (tip item) i (tip i))) ≡
                              ordTree t)
               (if-false (node (tip item) i (tip i)))
               refl
      ⟩
    ordTree (node (tip item) i (tip i))
      ≡⟨ ordTree-node (tip item) i (tip i) ⟩
    ordTree (tip item)
    && ordTree (tip i)
    && le-TreeItem (tip item) i
    && le-ItemTree i (tip i)
      ≡⟨ subst (λ t → ordTree (tip item)
                      && ordTree (tip i)
                      && le-TreeItem (tip item) i
                      && le-ItemTree i (tip i) ≡
                      t
                      && ordTree (tip i)
                      && le-TreeItem (tip item) i
                      && le-ItemTree i (tip i))
               (ordTree-tip item)
               refl
      ⟩
    true && ordTree (tip i) && le-TreeItem (tip item) i &&
    le-ItemTree i (tip i)
      ≡⟨ subst (λ t → true
                      && ordTree (tip i)
                      && le-TreeItem (tip item) i
                      && le-ItemTree i (tip i) ≡
                      true
                      && t
                      && le-TreeItem (tip item) i
                      && le-ItemTree i (tip i))
               (ordTree-tip i)
               refl
      ⟩
    true && true && le-TreeItem (tip item) i && le-ItemTree i (tip i)
      ≡⟨ subst (λ t → true && true && le-TreeItem (tip item) i &&
                      le-ItemTree i (tip i) ≡
                      true && true && t && le-ItemTree i (tip i))
               (le-TreeItem-tip item i)
               refl
      ⟩
    true && true && le item i && le-ItemTree i (tip i)
      ≡⟨ subst (λ t → true && true && le item i && le-ItemTree i (tip i) ≡
                      true && true && t && le-ItemTree i (tip i))
               (x<y→x≤y Nitem Ni i>item)
               refl
      ⟩
    true && true && true && le-ItemTree i (tip i)
      ≡⟨ subst (λ t → true && true && true && le-ItemTree i (tip i) ≡
                      true && true && true && t)
               (le-ItemTree-tip i i)
               refl
      ⟩
    true && true && true && le i i
      ≡⟨ subst (λ t → true && true && true && le i i ≡
                      true && true && true && t)
               (x≤x Ni)
               refl
      ⟩
    true && true && true && true
      ≡⟨ subst (λ t → true && true && true && true ≡ true && true && t)
               (t&&x≡x true)
               refl
      ⟩
    true && true && true
      ≡⟨ subst (λ t → true && true && true ≡ true && t)
               (t&&x≡x true)
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

  prf₂ : i ≤ item → OrdTree (toTree · item · tip i)
  prf₂ i≤item =
    ordTree (toTree · item · tip i)
      ≡⟨ subst (λ t → ordTree (toTree · item · tip i) ≡ ordTree t)
               (toTree-tip item i)
               refl
      ⟩
    ordTree (if (le i item)
               then (node (tip i) item (tip item))
               else (node (tip item) i (tip i)))
      ≡⟨ subst (λ t → ordTree (if (le i item)
                                 then (node (tip i) item (tip item))
                                 else (node (tip item) i (tip i))) ≡
                      ordTree (if t
                                 then (node (tip i) item (tip item))
                                 else (node (tip item) i (tip i))))
               i≤item
               refl
      ⟩
    ordTree (if true
               then (node (tip i) item (tip item))
               else (node (tip item) i (tip i)))
      ≡⟨ subst (λ t → ordTree (if true
                                 then (node (tip i) item (tip item))
                                 else (node (tip item) i (tip i))) ≡
                      ordTree t)
               (if-true (node (tip i) item (tip item)))
               refl
      ⟩
    ordTree (node (tip i) item (tip item))
      ≡⟨ ordTree-node (tip i) item (tip item) ⟩
    ordTree (tip i) && ordTree (tip item) && le-TreeItem (tip i) item &&
    le-ItemTree item (tip item)
      ≡⟨ subst (λ t → ordTree (tip i)             &&
                      ordTree (tip item)          &&
                      le-TreeItem (tip i) item     &&
                      le-ItemTree item (tip item)  ≡
                      t                           &&
                      ordTree (tip item)          &&
                      le-TreeItem (tip i) item     &&
                      le-ItemTree item (tip item))
               (ordTree-tip i)
               refl
      ⟩
    true && ordTree (tip item) && le-TreeItem (tip i) item &&
    le-ItemTree item (tip item)
      ≡⟨ subst (λ t → true                        &&
                      ordTree (tip item)          &&
                      le-TreeItem (tip i) item     &&
                      le-ItemTree item (tip item)  ≡
                      true                        &&
                      t                           &&
                      le-TreeItem (tip i) item     &&
                      le-ItemTree item (tip item))
               (ordTree-tip item)
               refl
      ⟩
    true && true && le-TreeItem (tip i) item && le-ItemTree item (tip item)
      ≡⟨ subst (λ t → true && true && le-TreeItem (tip i) item &&
                      le-ItemTree item (tip item) ≡
                      true && true && t && le-ItemTree item (tip item))
               (le-TreeItem-tip i item)
               refl
      ⟩
    true && true && le i item && le-ItemTree item (tip item)
      ≡⟨ subst (λ t → true && true && le i item && le-ItemTree item (tip item) ≡
                      true && true && t && le-ItemTree item (tip item))
               i≤item
               refl
      ⟩
    true && true && true && le-ItemTree item (tip item)
      ≡⟨ subst (λ t → true && true && true && le-ItemTree item (tip item) ≡
                      true && true && true && t)
               (le-ItemTree-tip item item)
               refl
      ⟩
    true && true && true && le item item
      ≡⟨ subst (λ t → true && true && true && le item item ≡
                      true && true && true && t)
               (x≤x Nitem)
               refl
      ⟩
    true && true && true && true
      ≡⟨ subst (λ t → true && true && true && true ≡ true && true && t)
               (t&&x≡x true)
               refl
      ⟩
    true && true && true
      ≡⟨ subst (λ t → true && true && true ≡ true && t) (t&&x≡x true) refl ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

toTree-OrdTree {item} Nitem (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) OTtnode =
  case prf₁ prf₂ (x>y∨x≤y Ni Nitem)
  where
  prf₁ : i > item → OrdTree (toTree · item · node t₁ i t₂)
  prf₁ i>item =
    ordTree (toTree · item · node t₁ i t₂)
      ≡⟨ subst (λ t → ordTree (toTree · item · node t₁ i t₂) ≡ ordTree t)
               (toTree-node item t₁ i t₂)
               refl
      ⟩
    ordTree (if (le i item)
               then (node t₁ i (toTree · item · t₂))
               else (node (toTree · item · t₁) i t₂))
      ≡⟨ subst (λ t → ordTree (if (le i item)
                                 then (node t₁ i (toTree · item · t₂))
                                 else (node (toTree · item · t₁) i t₂)) ≡
                      ordTree (if t
                                 then (node t₁ i (toTree · item · t₂))
                                 else (node (toTree · item · t₁) i t₂)))
               (x>y→x≰y Ni Nitem i>item)
               refl
      ⟩
    ordTree (if false
               then (node t₁ i (toTree · item · t₂))
               else (node (toTree · item · t₁) i t₂))
      ≡⟨ subst (λ t → ordTree (if false
                                 then (node t₁ i (toTree · item · t₂))
                                 else (node (toTree · item · t₁) i t₂)) ≡
                      ordTree t)
               (if-false (node (toTree · item · t₁) i t₂))
               refl
      ⟩
    ordTree (node (toTree · item · t₁) i t₂)
      ≡⟨ ordTree-node (toTree · item · t₁) i t₂ ⟩
    ordTree (toTree · item · t₁)      &&
    ordTree t₂                        &&
    le-TreeItem (toTree · item · t₁) i &&
    le-ItemTree i t₂
      ≡⟨ subst (λ t → ordTree (toTree · item · t₁)      &&
                      ordTree t₂                        &&
                      le-TreeItem (toTree · item · t₁) i &&
                      le-ItemTree i t₂                   ≡
                      t                                 &&
                      ordTree t₂                        &&
                      le-TreeItem (toTree · item · t₁) i &&
                      le-ItemTree i t₂)
               (toTree-OrdTree Nitem Tt₁
                               (leftSubTree-OrdTree Tt₁ Ni Tt₂ OTtnode))
               refl
      ⟩
    true && ordTree t₂ && le-TreeItem (toTree · item · t₁) i &&
    le-ItemTree i t₂
      ≡⟨ subst (λ t → true                              &&
                      ordTree t₂                        &&
                      le-TreeItem (toTree · item · t₁) i &&
                      le-ItemTree i t₂                   ≡
                      true                              &&
                      t                                 &&
                      le-TreeItem (toTree · item · t₁) i &&
                      le-ItemTree i t₂)
               (rightSubTree-OrdTree Tt₁ Ni Tt₂ OTtnode)
               refl
      ⟩
    true && true && le-TreeItem (toTree · item · t₁) i && le-ItemTree i t₂
      ≡⟨ subst (λ t → true                              &&
                      true                              &&
                      le-TreeItem (toTree · item · t₁) i &&
                      le-ItemTree i t₂                   ≡
                      true && true && t && le-ItemTree i t₂)
               (toTree-OrdTree-helper₁ Ni Nitem i>item Tt₁
                 ((&&-list₄-t₃
                   (ordTree-Bool Tt₁)
                   (ordTree-Bool Tt₂)
                   (le-TreeItem-Bool Tt₁ Ni)
                   (le-ItemTree-Bool Ni Tt₂)
                   (trans (sym (ordTree-node t₁ i t₂)) OTtnode))))
               refl
      ⟩
    true && true && true && le-ItemTree i t₂
      ≡⟨ subst (λ t → true && true && true && le-ItemTree i t₂ ≡
                      true && true && true && t)
               (&&-list₄-t₄
                 (ordTree-Bool Tt₁)
                 (ordTree-Bool Tt₂)
                 (le-TreeItem-Bool Tt₁ Ni)
                 (le-ItemTree-Bool Ni Tt₂)
                 (trans (sym (ordTree-node t₁ i t₂)) OTtnode))
               refl
      ⟩
    true && true && true && true
      ≡⟨ subst (λ t → true && true && true && true ≡ true && true && t)
               (t&&x≡x true)
               refl
      ⟩
    true && true && true
      ≡⟨ subst (λ t → true && true && true ≡ true && t) (t&&x≡x true) refl ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

  prf₂ : i ≤ item → OrdTree (toTree · item · node t₁ i t₂)
  prf₂ i≤item =
    ordTree (toTree · item · node t₁ i t₂)
      ≡⟨ subst (λ t → ordTree (toTree · item · node t₁ i t₂) ≡ ordTree t)
               (toTree-node item t₁ i t₂)
               refl
      ⟩
    ordTree (if (le i item)
               then (node t₁ i (toTree · item · t₂))
               else (node (toTree · item · t₁) i t₂))
      ≡⟨ subst (λ t → ordTree (if (le i item)
                                 then (node t₁ i (toTree · item · t₂))
                                 else (node (toTree · item · t₁) i t₂)) ≡
                      ordTree (if t
                                 then (node t₁ i (toTree · item · t₂))
                                 else (node (toTree · item · t₁) i t₂)))
               i≤item
               refl
      ⟩
    ordTree (if true
               then (node t₁ i (toTree · item · t₂))
               else (node (toTree · item · t₁) i t₂))
      ≡⟨ subst (λ t → ordTree (if true
                                 then (node t₁ i (toTree · item · t₂))
                                 else (node (toTree · item · t₁) i t₂)) ≡
                      ordTree t)
               (if-true (node t₁ i (toTree · item · t₂)))
               refl
      ⟩
    ordTree (node t₁ i (toTree · item · t₂))
      ≡⟨ ordTree-node t₁ i (toTree · item · t₂) ⟩
    ordTree t₁                     &&
    ordTree (toTree · item · t₂)   &&
    le-TreeItem t₁ i                &&
    le-ItemTree i (toTree · item · t₂)
      ≡⟨ subst (λ t → ordTree t₁                        &&
                      ordTree (toTree · item · t₂)      &&
                      le-TreeItem t₁ i                   &&
                      le-ItemTree i (toTree · item · t₂) ≡
                      t                                 &&
                      ordTree (toTree · item · t₂)      &&
                      le-TreeItem t₁ i                   &&
                      le-ItemTree i (toTree · item · t₂))
               (leftSubTree-OrdTree Tt₁ Ni Tt₂ OTtnode)
               refl
      ⟩
    true && ordTree (toTree · item · t₂) && le-TreeItem t₁ i &&
    le-ItemTree i (toTree · item · t₂)
      ≡⟨ subst (λ t → true                              &&
                      ordTree (toTree · item · t₂)      &&
                      le-TreeItem t₁ i                   &&
                      le-ItemTree i (toTree · item · t₂) ≡
                      true                              &&
                      t                                 &&
                      le-TreeItem t₁ i                   &&
                      le-ItemTree i (toTree · item · t₂))
               (toTree-OrdTree Nitem Tt₂
                 (rightSubTree-OrdTree Tt₁ Ni Tt₂ OTtnode))
               refl
      ⟩
    true && true && le-TreeItem t₁ i && le-ItemTree i (toTree · item · t₂)
      ≡⟨ subst (λ t → true                              &&
                      true                              &&
                      le-TreeItem t₁ i                   &&
                      le-ItemTree i (toTree · item · t₂) ≡
                      true                              &&
                      true                              &&
                      t                                 &&
                      le-ItemTree i (toTree · item · t₂))
               (&&-list₄-t₃
                 (ordTree-Bool Tt₁)
                 (ordTree-Bool Tt₂)
                 (le-TreeItem-Bool Tt₁ Ni)
                 (le-ItemTree-Bool Ni Tt₂)
                 (trans (sym (ordTree-node t₁ i t₂)) OTtnode))
               refl
      ⟩
    true && true && true && le-ItemTree i (toTree · item · t₂)
      ≡⟨ subst (λ t → true                              &&
                      true                              &&
                      true                              &&
                      le-ItemTree i (toTree · item · t₂) ≡
                      true && true && true && t)
               (toTree-OrdTree-helper₂ Ni Nitem i≤item Tt₂
                 ((&&-list₄-t₄
                   (ordTree-Bool Tt₁)
                     (ordTree-Bool Tt₂)
                     (le-TreeItem-Bool Tt₁ Ni)
                     (le-ItemTree-Bool Ni Tt₂)
                     (trans (sym (ordTree-node t₁ i t₂)) OTtnode))))
                 refl
      ⟩
    true && true && true && true
      ≡⟨ subst (λ t → true && true && true && true ≡ true && true && t)
               (t&&x≡x true)
               refl
      ⟩
    true && true && true
      ≡⟨ subst (λ t → true && true && true ≡ true && t) (t&&x≡x true) refl ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

------------------------------------------------------------------------------
-- Burstall's lemma: ord(maketree(is)).

-- makeTree-TreeOrd : ∀ {is} → ListN is → OrdTree (makeTree is)
-- makeTree-TreeOrd LNis =
--   ind-lit OrdTree toTree nil LNis ordTree-nil
--           (λ Nx y TOy → toTree-OrdTree Nx {!!} TOy)

makeTree-OrdTree : ∀ {is} → ListN is → OrdTree (makeTree is)
makeTree-OrdTree lnnil =
  ordTree (lit toTree [] nil)
    ≡⟨ subst (λ t → ordTree (lit toTree [] nil) ≡ ordTree t)
             (lit-[] toTree nil)
             refl
    ⟩
  ordTree nil
    ≡⟨ ordTree-nil ⟩
  true ∎

makeTree-OrdTree (lncons {i} {is} Ni Lis) =
  ordTree (lit toTree (i ∷ is) nil)
    ≡⟨ subst (λ t → ordTree (lit toTree (i ∷ is) nil) ≡ ordTree t)
             (lit-∷ toTree i is nil)
             refl
    ⟩
  ordTree (toTree · i · (lit toTree is nil))
    ≡⟨ toTree-OrdTree Ni (makeTree-Tree Lis) (makeTree-OrdTree Lis) ⟩
  true ∎

------------------------------------------------------------------------------
-- Burstall's lemma: If ord(is1) and ord(is2) and is1 ≤ is2 then
-- ord(concat(is1, is2)).
++-OrdList : ∀ {is js} → ListN is → ListN js → OrdList is → OrdList js →
             ≤-Lists is js → OrdList (is ++ js)

++-OrdList {js = js} lnnil LNjs LOis LOjs is≤js =
  subst OrdList (sym (++-leftIdentity js)) LOjs

++-OrdList {js = js} (lncons {i} {is} Ni LNis) LNjs LOi∷is LOjs i∷is≤js =
  subst OrdList (sym (++-∷ i is js)) lemma
  where
  lemma : OrdList (i ∷ is ++ js)
  lemma =
    ordList (i ∷ is ++ js)
      ≡⟨ ordList-∷ i (is ++ js) ⟩
    le-ItemList i (is ++ js) && ordList (is ++ js)
      ≡⟨ subst (λ t → le-ItemList i (is ++ js) && ordList (is ++ js) ≡
                      t && ordList (is ++ js))
               (++-OrdList-helper Ni LNis LNjs
                 (&&-list₂-t₁ (le-ItemList-Bool Ni LNis)
                              (ordList-Bool LNis)
                              (trans (sym (ordList-∷ i is)) LOi∷is))
                 (&&-list₂-t₁ (le-ItemList-Bool Ni LNjs)
                              (le-Lists-Bool LNis LNjs)
                              (trans (sym (le-Lists-∷ i is js)) i∷is≤js))
                 (&&-list₂-t₂ (le-ItemList-Bool Ni LNjs)
                              (le-Lists-Bool LNis LNjs)
                              (trans (sym (le-Lists-∷ i is js)) i∷is≤js))
               )
               refl
      ⟩
    true && ordList (is ++ js)
      ≡⟨ subst (λ t → true && ordList (is ++ js) ≡ true && t)
               (++-OrdList LNis LNjs (subList-OrdList Ni LNis LOi∷is) LOjs
                           (&&-list₂-t₂
                             (le-ItemList-Bool Ni LNjs)
                             (le-Lists-Bool LNis LNjs)
                             (trans (sym (le-Lists-∷ i is js)) i∷is≤js)))
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

------------------------------------------------------------------------------
-- Burstall's lemma: If t is ordered then (flatten t) is ordered.
flatten-OrdList : ∀ {t} → Tree t → OrdTree t → OrdList (flatten t)
flatten-OrdList tnil OTt =
  subst OrdList (sym flatten-nil) ordList-[]

flatten-OrdList (ttip {i} Ni) OTt =
  ordList (flatten (tip i))
    ≡⟨ subst (λ t → ordList (flatten (tip i)) ≡ ordList t)
             (flatten-tip i)
             refl
    ⟩
  ordList (i ∷ [])
    ≡⟨ ordList-∷ i [] ⟩
  le-ItemList i [] && ordList []
    ≡⟨ subst₂ (λ t₁ t₂ → le-ItemList i [] && ordList [] ≡ t₁ && t₂)
              (le-ItemList-[] i)
              ordList-[]
              refl
    ⟩
  true && true
    ≡⟨ t&&x≡x true ⟩
  true ∎

flatten-OrdList (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) OTt =
  ordList (flatten (node t₁ i t₂))
    ≡⟨ subst (λ t → ordList (flatten (node t₁ i t₂)) ≡ ordList t)
             (flatten-node t₁ i t₂)
             refl
    ⟩
  ordList (flatten t₁ ++ flatten t₂)
    ≡⟨ ++-OrdList (flatten-ListN Tt₁)
                  (flatten-ListN Tt₂)
                  (flatten-OrdList Tt₁ (leftSubTree-OrdTree Tt₁ Ni Tt₂ OTt))
                  (flatten-OrdList Tt₂ (rightSubTree-OrdTree Tt₁ Ni Tt₂ OTt))
                  (flatten-OrdList-helper Tt₁ Ni Tt₂ OTt)
    ⟩
  true ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Basic.Compiler.CorrectFrom where

open import Basic.AST
open import Basic.BigStep
open import Basic.Compiler.Code
open import Basic.Compiler.SplitCode
open import Utils.NatOrdLemmas
open import Utils.Decidable
open import Utils.Monoid

open import Data.Fin using (Fin; #_)
open import Data.Vec hiding (_∷ʳ_; _++_; [_]; _∈_; foldr)
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties
open import Data.Empty
open import Data.Bool renaming (not to notBool; if_then_else_ to ifBool_then_else)
open import Data.List hiding ([_])
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
import Level as L

open import Algebra
private
  module LM {a A} = Algebra.Monoid (Data.List.monoid {a} A)

open import Relation.Unary
open import Induction.Nat
open import Induction.WellFounded

{-
Lemma 3.22

This proof caused me considerable headache. First I started to prove it
by strctural recursion on the to-be-compiled statement, but then Agda complained
that it was not structurally recursive. And indeed it isn't.

In the "while-true" case, we start with a program derivation of the type:

  ⟨ 𝓒⟦ S ⟧ˢ ++ LOOP 𝓒⟦ b ⟧ᵉ 𝓒⟦ S ⟧ˢ ∷ [] , [] , s ⟩▷*⟨ [] , e , s' ⟩

And a statement with the following form:

  while b do S

Then we split this derivation into two parts:

  ⟨ 𝓒⟦ S ⟧ˢ , [] , s ⟩▷*⟨ [] , e'' , s'' ⟩
  ⟨ LOOP 𝓒⟦ b ⟧ᵉ 𝓒⟦ S ⟧ˢ ∷ [] , e'' , s'' ⟩▷*⟨ [] , e , s' ⟩

But now if we recurse on the second derivation, the corresponding statement will
be again "while b do S". Thus Agda will not be able to prove termination.

So I had to use well-founded induction. It is a standard library machinery that
allows us to do induction on a well-ordered set. Here's an introduction to how
it works:

http://blog.ezyang.com/2010/06/well-founded-recursion-in-agda/

We usually prefer to not use well-founded recursion, because it demands us proofs
of decreasing order even on cases where recursion is otherwise evidently structural, and
it also makes certain proofs rather difficult.
-}

-- Well-foundedness lemmas
------------------------------------------------------------

{-
We do well-founded recursion on the length of derivation sequences.
But we also have to prove that splitting a derivation sequence will
never produce empty sequences, or else the lenghts will not be strictly
decreasing.

To show this, we have to show that

  - compilation into abstract machine code never outputs
    an empty list of instructions

  - computation sequences starting with a non-empty instruction list are never empty

-}

∷ʳ-nonempty : ∀ {a}{A : Set a}(xs : List A) x → xs ∷ʳ x ≢ []
∷ʳ-nonempty [] x ()
∷ʳ-nonempty (x ∷ xs) x₁ ()

++-xs-empty : ∀ {a}{A : Set a}(xs : List A) {ys} → xs <> ys ≡ [] → xs ≡ []
++-xs-empty [] p = refl
++-xs-empty (x ∷ xs)  ()

{- Compiled statement are non-empty -}
𝓒ˢ-nonempty : ∀ {n}(S : St n) → 𝓒⟦ S ⟧ˢ ≢ []
𝓒ˢ-nonempty (x := x₁)             = ∷ʳ-nonempty 𝓒⟦ x₁ ⟧ᵉ (STORE x)
𝓒ˢ-nonempty (S , S₁)              = 𝓒ˢ-nonempty S ∘ ++-xs-empty 𝓒⟦ S ⟧ˢ
𝓒ˢ-nonempty (if x then S else S₁) = ∷ʳ-nonempty 𝓒⟦ x ⟧ᵉ (BRANCH 𝓒⟦ S ⟧ˢ 𝓒⟦ S₁ ⟧ˢ)
𝓒ˢ-nonempty (while x do S) ()
𝓒ˢ-nonempty skip ()

{- Compiled expressions are non-empty -}
𝓒-Exp-nonempty : ∀ {n t} (e : Exp n t) → 𝓒⟦ e ⟧ᵉ ≢ []
𝓒-Exp-nonempty (add e e₁)     = ∷ʳ-nonempty (𝓒⟦ e₁ ⟧ᵉ <> 𝓒⟦ e ⟧ᵉ) ADD
𝓒-Exp-nonempty (mul e e₁)     = ∷ʳ-nonempty (𝓒⟦ e₁ ⟧ᵉ <> 𝓒⟦ e ⟧ᵉ) MUL
𝓒-Exp-nonempty (sub e e₁)     = ∷ʳ-nonempty (𝓒⟦ e₁ ⟧ᵉ <> 𝓒⟦ e ⟧ᵉ) SUB
𝓒-Exp-nonempty (eq e e₁)      = ∷ʳ-nonempty (𝓒⟦ e₁ ⟧ᵉ <> 𝓒⟦ e ⟧ᵉ) EQ
𝓒-Exp-nonempty (lte e e₁)     = ∷ʳ-nonempty (𝓒⟦ e₁ ⟧ᵉ <> 𝓒⟦ e ⟧ᵉ) LTE
𝓒-Exp-nonempty (lt e e₁)      = ∷ʳ-nonempty (𝓒⟦ e₁ ⟧ᵉ <> 𝓒⟦ e ⟧ᵉ) LT
𝓒-Exp-nonempty (Exp.and e e₁) = ∷ʳ-nonempty (𝓒⟦ e₁ ⟧ᵉ <> 𝓒⟦ e ⟧ᵉ) AND
𝓒-Exp-nonempty (not e)        = ∷ʳ-nonempty 𝓒⟦ e ⟧ᵉ NOT
𝓒-Exp-nonempty (lit x) ()
𝓒-Exp-nonempty (var x) ()
𝓒-Exp-nonempty tt ()
𝓒-Exp-nonempty ff ()

{-Computations sequences for non-empty code are non-zero length -}
▷*-S-nonempty :
  ∀ {n S}{s s' : State n}{e e'} (p : ⟨ 𝓒⟦ S ⟧ˢ , e , s ⟩▷*⟨ [] , e' , s' ⟩)
  → ▷*-length p ≢ 0
▷*-S-nonempty{_}{S} p x with 𝓒ˢ-nonempty S | 𝓒⟦ S ⟧ˢ | inspect 𝓒⟦_⟧ˢ S
▷*-S-nonempty done x      | ¬empty | []     | [ remember ] = ¬empty remember
▷*-S-nonempty (() ∷ p) x₁ | ¬empty | []     | [ remember ]
▷*-S-nonempty (x₁ ∷ p) () | ¬empty | x ∷ cs | [ remember ]

{- misc ordering lemmas -}
a<′a+sb : ∀ a b → b ≢ 0 → a <′ a + b
a<′a+sb a zero x = ⊥-elim (x refl)
a<′a+sb a (suc b) x rewrite +-comm a (suc b) = ≤⇒≤′ $ a<sb+a a b

a<′b+sa : ∀ a b → a <′ b + suc a
a<′b+sa a zero    = ≤′-refl
a<′b+sa a (suc b) = ≤′-step (a<′b+sa a b)

≤′-weaken-l : ∀ {a b} c → a ≤′ b → a ≤′ c + b
≤′-weaken-l zero p = p
≤′-weaken-l (suc c) p = ≤′-step (≤′-weaken-l c p)

-- Correctness
------------------------------------------------------------

{-
This is a shorthand for the actual type of the theorem. We use this because
otherwise we'd have to write out the type three times in the following code.
-}
𝓒-correct-from-Ty : {_ : ℕ} → ℕ → Set
𝓒-correct-from-Ty {n} size =
    ∀ {S : St n} {e s s'}
    → (p : ⟨ 𝓒⟦ S ⟧ˢ , [] , s ⟩▷*⟨ [] , e , s' ⟩)
    → size ≡ ▷*-length p
    → ⟨ S , s ⟩⟱ s' × e ≡ []

𝓒-correct-from : ∀ {n} size → 𝓒-correct-from-Ty {n} size
𝓒-correct-from {n} = <-rec _ go where

  {-
  Note: we use ▷*-deterministic quite a few times below. We separately use
  ▷*-split to split the sequence and 𝓒-Exp to establish the contents of the stack
  after evaluating an expression, but these remain separate facts until we use
  determinism to prove that the first split sequence and 𝓒-Exp's resulting sequence
  are the same.

  We see 𝓒-Exp , ▷*-split and ▷*-deterministic chained together several times below.
  This is admittedly pretty ugly and it would be better to factor out this pattern
  and possibly include all the relevant information in the output of ▷*-split.
  -}

  {-
  "go" is the helper function for well-founded recursion. "<-rec" can be viewed as
  a sort of a fixpoint operator that demands a proof that the argument strictly decreases
  on every recursion. "size" is the size argument, and we recurse via the "recurse"
  argument.
  -}
  go : ∀ size → (∀ y → y <′ size → 𝓒-correct-from-Ty {n} y) → 𝓒-correct-from-Ty {n} size

  -- Assignment
  go size recurse {x := exp}{e}{s} p sizeEq
    with ▷*-split 𝓒⟦ exp ⟧ᵉ p | 𝓒-Exp-nat {e = []}{s = s} exp
  go size recurse {.x := exp} p sizeEq | s₁ , ._ , p1 , STORE x ∷ () ∷ p2 , eqn | exp'
  go size recurse {.x := exp} p sizeEq | s₁ , ._ , p1 , STORE x ∷ done , eqn | exp'
    with ▷*-deterministic p1 exp'
  ... | _ , eqe , eqs
    rewrite eqs
    with ∷-injective eqe
  ... | eq-cond , e≡[]
    rewrite nat-inj eq-cond
    = ass , e≡[]

  -- Skip
  go size recurse {skip} (NOOP ∷ done) sizeEq = skip , refl
  go size recurse {skip} (NOOP ∷ () ∷ p) sizeEq

  -- Sequencing
  go size recurse {S , S₁} p sizeEq
    with ▷*-split 𝓒⟦ S ⟧ˢ p
  ... | s'' , e'' , p1 , p2 , size+eq
    rewrite sizeEq | sym size+eq
    with recurse _ (a<′a+sb _ _ (▷*-S-nonempty {S = S₁} p2)) {S} p1 refl
  ... | p1' , e''≡[]
    rewrite e''≡[] | +-comm (▷*-length p1) (▷*-length p2)
    with recurse _ (a<′a+sb _ _ (▷*-S-nonempty {S = S} p1)) {S₁} p2 refl
  ... | p2' , e≡[] = (p1' , p2') , e≡[]

  -- If then else
  go size recurse {if b then S else S₁} {e}{s}{s'} p sizeEq
    with ▷*-split 𝓒⟦ b ⟧ᵉ p | 𝓒-Exp-bool {e = []}{s = s} b
  ... | s'' , ._ , p1 , BRANCH ∷ p2 , size+eq | b'
    with ▷*-deterministic p1 b'
  ... | _ , eqe , eqs
    rewrite eqs
    with ∷-injective eqe
  ... | eq-cond , e'≡[]
    rewrite bool-inj eq-cond | e'≡[] |
           proj₂ LM.identity (ifBool ⟦ b ⟧ᵉ s then 𝓒⟦ S ⟧ˢ else 𝓒⟦ S₁ ⟧ˢ)
           | sizeEq | sym size+eq
    with ⟦ b ⟧ᵉ s | inspect ⟦ b ⟧ᵉ s

  ... | true  | [ condTrue  ]
    = (if-true (≡true→T condTrue) (proj₁ rest)) , proj₂ rest
    where rest : ⟨ S , s ⟩⟱ s' × e ≡ []
          rest = recurse (▷*-length p2) (a<′b+sa (▷*-length p2) (▷*-length p1)) p2 refl

  ... | false | [ condFalse ]
    = (if-false (≡false→F condFalse) (proj₁ rest)) , proj₂ rest
    where rest : ⟨ S₁ , s ⟩⟱ s' × e ≡ []
          rest = recurse (▷*-length p2) (a<′b+sa (▷*-length p2) (▷*-length p1)) p2 refl

  -- While
  go size recurse {while b do S}{e}{s}{s'} (LOOP ∷ p) sizeEq
    with 𝓒-Exp-bool {e = []}{s = s} b | ▷*-split 𝓒⟦ b ⟧ᵉ p
  ... | b' | s'' , ._ , p1 , BRANCH ∷ p2 , size+eq
    with ▷*-deterministic p1 b'
  ... | _ , eqe , eqs
    rewrite eqs
    with ∷-injective eqe
  ... | eq-cond , e'≡[]
    rewrite bool-inj eq-cond | e'≡[] |
       proj₂ LM.identity (ifBool ⟦ b ⟧ᵉ s then 𝓒⟦ S ⟧ˢ ++ LOOP 𝓒⟦ b ⟧ᵉ 𝓒⟦ S ⟧ˢ ∷ [] else (NOOP ∷ []))
       | sym size+eq | sizeEq
    with ⟦ b ⟧ᵉ s | inspect ⟦ b ⟧ᵉ s

  {- Here we the proofs are a bit messed up by the two recursive calls with
     hideous hand-crafted proofs of size decrease. This is the sort of thing
     where Coq's solvers and tactics for arithmetic are really handy. Unfortunately
     we don't yet have those things in Agda, although there is some infrastructure
     already in place that could be used to create more automatization (like typeclasses
     and goal reflection)
   -}

  -- while-true
  ... | true  | [ condTrue  ] = 𝓒-while-true condTrue p2 refl
    where
      𝓒-while-true :
        ∀ {s s' : State n}{b e S}
        → ⟦ b ⟧ᵉ s ≡ true
        → (p3 : ⟨ 𝓒⟦ S ⟧ˢ ++ LOOP 𝓒⟦ b ⟧ᵉ 𝓒⟦ S ⟧ˢ ∷ [] , [] , s ⟩▷*⟨ [] , e , s' ⟩)
        → (▷*-length p3 ≡ ▷*-length p2)
        → (⟨ while b do S , s ⟩⟱ s') × e ≡ []
      𝓒-while-true {s}{s'}{b}{e}{S} condTrue p3 ≡len
        with ▷*-split 𝓒⟦ S ⟧ˢ p3
      ... | s'' , e'' , p1_new , p2_new , size+eq
        rewrite sym size+eq
        with recurse (▷*-length p1_new)
          (≤′-step
            (subst (λ x → suc (▷*-length p1_new) ≤′ ▷*-length p1 + suc x) ≡len
               (≤′-weaken-l (▷*-length p1)
                  (≤′-step (a<′a+sb (▷*-length p1_new) (▷*-length p2_new)
                    (▷*-S-nonempty {S = while b do S} p2_new))))))
          {S} p1_new refl

      ... | p1' , e''≡[]
        rewrite e''≡[]
        with recurse (▷*-length p2_new)
          (≤′-step (subst (λ x → suc (▷*-length p2_new) ≤′ ▷*-length p1 + suc x) ≡len
               (≤′-weaken-l (▷*-length p1)
                 (≤′-step (
                   subst
                     (λ x → ▷*-length p2_new <′ x)
                     (+-comm (▷*-length p2_new) (▷*-length p1_new))
                     (a<′a+sb
                         (▷*-length p2_new) (▷*-length p1_new)
                         (▷*-S-nonempty {S = S} p1_new)))))))
          {while b do S} p2_new refl
      ... | p2' , e≡[] = (while-true (≡true→T condTrue) p1' p2') , e≡[]

  -- while-false
  ... | false | [ condFalse ] = 𝓒-while-false condFalse p2
    where
      𝓒-while-false :
        ∀ {n}{s s' : State n}{e b S}
        → ⟦ b ⟧ᵉ s ≡ false
        → ⟨ NOOP ∷ [] , [] , s ⟩▷*⟨ [] , e , s' ⟩
        → (⟨ while b do S , s ⟩⟱ s' × e ≡ [])
      𝓒-while-false f (NOOP ∷ done) = (while-false (≡false→F f)) , refl
      𝓒-while-false f (NOOP ∷ () ∷ p)

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
{-# OPTIONS --type-in-type #-}

record ⊤ : Set where
  constructor tt

data ⊥ : Set where

data _==_ {A : Set} (x : A) : A → Set where
  refl : x == x

module _ (A : Set) (B : A → Set) where
  record Σ : Set where
    constructor _,_
    field
      π₁ : A
      π₂ : B π₁
  open Σ public
  syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

isContr : Set → Set
isContr A = Σ[ x ∶ A ] (∀ y → x == y)

Σ! : (A : Set) (B : A → Set) → Set
Σ! A B = isContr (Σ A B)

syntax Σ! A (λ x → B) = Σ![ x ∶ A ] B

_×_ : (A B : Set) → Set
A × B = Σ A λ _ → B

P : Set → Set
P A = A → Set

module _ {A : Set} where
  empty : P A
  empty = λ x → ⊥

  full : P A
  full = λ x → ⊤

  _∩_ : P A → P A → P A
  U ∩ V = λ x → (U x) × (V x)

  _⊆_ : P A → P A → Set
  U ⊆ V = ∀ x → U x → V x

  ⋃[_] : P (P A) → P A
  ⋃[_] S = λ x → Σ[ U ∶ P A ] S U × U x

record Topology (X : Set) : Set where
  field
    O : P (P X)

    empty-open : O empty
    full-open : O full
    inter-open : ∀ {U V} → O U → O V → O (U ∩ V)
    union-open : ∀ {S} → S ⊆ O → O ⋃[ S ]

record Equivalence {A : Set} (R : A → A → Set) : Set where
  field
    reflexivity : {x : A} → R x x
    !_ : {x y : A} → R x y → R y x
    _∙_ : {x y z : A} → R y z → R x y → R x z
  infixr 9 _∙_

instance
  ==-equiv : ∀ {A} → Equivalence (_==_ {A})
  ==-equiv = record { reflexivity = refl ; !_ = λ { {_} {._} refl → refl }; _∙_ = λ { {_} {._} {_} refl q → q } }

record Category : Set where
  field
    Ob : Set
    Hom : Ob → Ob → Set

    _~_ : ∀ {A B} → Hom A B → Hom A B → Set
    ~-equiv : ∀ {A B} → Equivalence (_~_ {A} {B})

    id : ∀ {A} → Hom A A
    _∘_ : ∀ {A B C} → Hom B C → Hom A B → Hom A C

    left-id : ∀ {A B} {f : Hom A B} → (id ∘ f) ~ f
    right-id : ∀ {A B} {f : Hom A B} → (f ∘ id) ~ f

    assoc : ∀ {A B C D} {f : Hom A B} {g : Hom B C} {h : Hom C D} → ((h ∘ g) ∘ f) ~ (h ∘ (g ∘ f))

  instance
    ~-equiv-instance = ~-equiv

    opposite : Category
    opposite =
      let open Equivalence {{...}} in
      record
      { Ob = Ob
      ; Hom = λ A B → Hom B A
      ; _~_ = _~_
      ; ~-equiv = ~-equiv
      ; id = id
      ; _∘_ = λ f g → g ∘ f
      ; left-id = λ {A} {B} → right-id
      ; right-id = λ {A} {B} → left-id
      ; assoc = λ {A} {B} {C} {D} {f} {g} {h} → ! assoc
      }

record Functor (C D : Category) : Set where
  module C = Category C
  module D = Category D

  field
    apply : C.Ob → D.Ob
    map : ∀ {A B} → C.Hom A B → D.Hom (apply A) (apply B)

    id-law : ∀ {A} → map (C.id {A}) D.~ D.id
    comp-law : ∀ {A B C} (f : C.Hom B C) (g : C.Hom A B) → map (f C.∘ g) D.~ (map f D.∘ map g)

instance
  open Equivalence {{...}}

  Types : Category
  Types =
    record
    { Ob = Set
    ; Hom = λ A B → A → B
    ; _~_ = λ f g → ∀ x → f x == g x
    ; ~-equiv = record
                   { reflexivity = λ x → refl
                   ; !_ = λ {f} {g} p x → ! p x
                   ; _∙_ = λ {f} {g} {h} p q r → p r ∙ q r
                   }
    ; id = λ {A} z → z
    ; _∘_ = λ {A} {B} {C} f g x → f (g x)
    ; left-id = λ {A} {B} {f} x → refl
    ; right-id = λ {A} {B} {f} x → refl
    ; assoc = λ x → refl
    }

module _ (X : Set) (T : Topology X) where
  private
    module T = Topology T

  instance
    OpenSets : Category
    OpenSets = record
      { Ob = Σ _ T.O
      ; Hom = λ U V → π₁ U ⊆ π₁ V
      ; _~_ = _==_
      ; ~-equiv = ==-equiv
      ; id = λ x z → z
      ; _∘_ = λ z z₁ x z₂ → z x (z₁ x z₂)
      ; left-id = refl
      ; right-id = refl
      ; assoc = refl
      }

  Presheaf : Set
  Presheaf = Functor (Category.opposite OpenSets) Types

  module _ (U : P X) (U-open : T.O U) where
    record Cover : Set where
      field
        Index : Set
        at : (i : Index) → P X
        at-open : (i : Index) → T.O (at i)
        at-subset : (i : Index) → at i ⊆ U
        covering : (x : X) → U x → Σ[ i ∶ Index ] at i x

    module _ (F : Presheaf) (<U> : Cover) where
      private
        module F = Functor F
        module <U> = Cover <U>

      Section : Set
      Section =
        ∀ i → F.apply (<U>.at i , <U>.at-open i)

      Coherence : Section → Set
      Coherence <s> =
        ∀ i j →
          let <U>ij = (<U>.at i ∩ <U>.at j) , (T.inter-open (<U>.at-open i) (<U>.at-open j) ) in
          F.map {<U>.at i , <U>.at-open i} {<U>ij} (λ _ → π₁) (<s> i)
            ==
          F.map {<U>.at j , <U>.at-open j} {<U>ij} (λ _ → π₂) (<s> j)

  Sheaf : Presheaf → Set
  Sheaf F =
    let module F = Functor F in
    (U : P X)
    (U-open : T.O U)
    (<U> : Cover U U-open)
    (<s> : Section U _ F <U>)
    (coh : Coherence U _  F <U> <s>)
      →
    let module <U> = Cover _ _ <U> in
      Σ![ s ∶ F.apply (U , U-open) ]
        (∀ i → F.map {U , U-open} (<U>.at-subset i) s == <s> i)

max_stars_repo_name: jonsterling/Agda-Sheaves

max_issues_repo_name: jonsterling/Agda-Sheaves

max_forks_repo_name: jonsterling/Agda-Sheaves


text:
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 _<_ #-}

div-helper : Nat → Nat → Nat → 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 #-}

mod-helper : Nat → Nat → Nat → 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 #-}


text:
{-# OPTIONS --safe #-}

module Definition.Conversion.Reduction where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Conversion

-- Weak head expansion of algorithmic equality of types.
reductionConv↑ : ∀ {A A′ B B′ r Γ}
               → Γ ⊢ A ⇒* A′ ^ r
               → Γ ⊢ B ⇒* B′ ^ r
               → Whnf A′
               → Whnf B′
               → Γ ⊢ A′ [conv↑] B′ ^ r
               → Γ ⊢ A  [conv↑] B ^ r
reductionConv↑ x x₁ x₂ x₃ ([↑] A″ B″ D D′ whnfA′ whnfB′ A′<>B′)
              rewrite whnfRed* D x₂ | whnfRed* D′ x₃ =
  [↑] A″ B″ x x₁ whnfA′ whnfB′ A′<>B′

-- Weak head expansion of algorithmic equality of terms.
reductionConv↑Term : ∀ {t t′ u u′ A B Γ l}
                   → Γ ⊢ A ⇒* B ^ [ ! , l ]
                   → Γ ⊢ t ⇒* t′ ∷ B ^ l
                   → Γ ⊢ u ⇒* u′ ∷ B ^ l
                   → Whnf B
                   → Whnf t′
                   → Whnf u′
                   → Γ ⊢ t′ [conv↑] u′ ∷ B ^ l
                   → Γ ⊢ t  [conv↑] u  ∷ A ^ l
reductionConv↑Term x x₁ x₂ x₃ x₄ x₅
                   ([↑]ₜ B₁ t″ u″ D d d′ whnfB whnft′ whnfu′ t<>u)
                   rewrite whnfRed* D x₃ | whnfRed*Term d x₄ | whnfRed*Term d′ x₅ =
  [↑]ₜ B₁ t″ u″ x x₁ x₂ whnfB whnft′ whnfu′ t<>u

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
open import Agda.Builtin.IO
open import Agda.Builtin.Size
open import Agda.Builtin.Unit

data D (i : Size) : Set where

{-# FOREIGN GHC
  data Empty i
  #-}

{-# COMPILE GHC D = data Empty () #-}

f : ∀ {i} → D i → D i
f ()

{-# COMPILE GHC f as f #-}

postulate
  return : {A : Set} → A → IO A

{-# COMPILE GHC return = \_ -> return #-}

main : IO ⊤
main = return _


text:
module Oscar.Class.Reflexive where

open import Oscar.Level
open import Oscar.Property.IsReflexive

record Reflexive {𝔬} (⋆ : Set 𝔬) ℓ : Set (𝔬 ⊔ lsuc ℓ) where
  field
    _≣_ : ⋆ → ⋆ → Set ℓ
    isReflexive : IsReflexive ⋆ _≣_

  open IsReflexive isReflexive public


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

open import Categories.Category using (Category; module Commutation)
open import Categories.Category.Monoidal.Core using (Monoidal)
open import Categories.Category.Monoidal.Braided using (Braided)

-- Braided monoidal categories satisfy the "four middle interchange"

module Categories.Category.Monoidal.Interchange.Braided
  {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (B : Braided M) where

open import Level using (_⊔_)
open import Data.Product using (_,_)

import Categories.Category.Construction.Core C as Core
import Categories.Category.Monoidal.Construction.Product as MonoidalProduct
open import Categories.Category.Monoidal.Braided.Properties as BraidedProps
  using (braiding-coherence; inv-Braided; inv-braiding-coherence)
open import Categories.Category.Monoidal.Interchange using (HasInterchange)
open import Categories.Category.Monoidal.Properties using (module Kelly's)
import Categories.Category.Monoidal.Reasoning as MonoidalReasoning
import Categories.Category.Monoidal.Utilities as MonoidalUtilities
open import Categories.Category.Product using (_⁂_; assocˡ)
open import Categories.Functor using (_∘F_)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (_≃_; niHelper)
open import Categories.Morphism.Reasoning C

open Category C
open Commutation C

private
  variable
    W W₁ W₂ X X₁ X₂ Y Y₁ Y₂ Z Z₁ Z₂ : Obj
    f g h i : X ⇒ Y

-- Braided monoidal categories have an interchange map.

open MonoidalReasoning M
open MonoidalUtilities M
open Braided B renaming (associator to α)
open Core.Shorthands            -- for idᵢ, _∘ᵢ_, ...
open Shorthands                 -- for λ⇒, ρ⇒, α⇒, ...
open BraidedProps.Shorthands B  -- for σ⇒, ...

-- The "four middle interchange" for braided tensor products.

swapInner : (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ≅ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z)
swapInner = α ⁻¹ ∘ᵢ idᵢ ⊗ᵢ (α ∘ᵢ σ ⊗ᵢ idᵢ ∘ᵢ α ⁻¹) ∘ᵢ α

module swapInner {W X Y Z} = _≅_ (swapInner {W} {X} {Y} {Z})
private
  i⇒ = swapInner.from
  i⇐ = swapInner.to

-- to shorten things, it is convenient to name some items that recur
-- swapˡ is the inner part of 'swapInner'
private
  swapˡ : X ⊗₀ (Y ⊗₀ Z) ⇒ Y ⊗₀ (X ⊗₀ Z)
  swapˡ = α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐

  swapˡ-act :  swapˡ ∘ g ⊗₁ (h ⊗₁ i) ≈ h ⊗₁ (g ⊗₁ i) ∘ swapˡ
  swapˡ-act {g = g} {h = h} {i = i} = begin
    (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ g ⊗₁ (h ⊗₁ i)    ≈⟨ pullʳ (pullʳ assoc-commute-to) ⟩
    α⇒ ∘ σ⇒ ⊗₁ id ∘ (g ⊗₁ h) ⊗₁ i ∘ α⇐      ≈⟨ refl⟩∘⟨ extendʳ (parallel (braiding.⇒.commute _) id-comm-sym) ⟩
    α⇒ ∘ (h ⊗₁ g) ⊗₁ i ∘ σ⇒ ⊗₁ id ∘ α⇐      ≈⟨ extendʳ assoc-commute-from ⟩
    h ⊗₁ (g ⊗₁ i) ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐      ∎

swapInner-natural : i⇒ ∘ (f ⊗₁ g) ⊗₁ (h ⊗₁ i) ≈ (f ⊗₁ h) ⊗₁ (g ⊗₁ i) ∘ i⇒
swapInner-natural {f = f} {g = g} {h = h} {i = i} = begin
    (α⇐ ∘ id ⊗₁ swapˡ ∘ α⇒) ∘ (f ⊗₁ g) ⊗₁ (h ⊗₁ i)  ≈⟨ pullʳ (pullʳ assoc-commute-from) ⟩
    α⇐ ∘ id ⊗₁ swapˡ ∘ f ⊗₁ g ⊗₁ (h ⊗₁ i) ∘ α⇒      ≈⟨ refl⟩∘⟨ extendʳ (parallel id-comm-sym swapˡ-act) ⟩
    α⇐ ∘ f ⊗₁ h ⊗₁ (g ⊗₁ i) ∘ id ⊗₁ swapˡ ∘ α⇒      ≈⟨ extendʳ assoc-commute-to ⟩
    (f ⊗₁ h) ⊗₁ (g ⊗₁ i) ∘ α⇐ ∘ id ⊗₁ swapˡ ∘ α⇒    ∎

swapInner-naturalIsomorphism : ⊗ ∘F (⊗ ⁂ ⊗) ≃ ⊗ ∘F MonoidalProduct.⊗ M M
swapInner-naturalIsomorphism = niHelper (record
  { η       = λ _ → i⇒
  ; η⁻¹     = λ _ → i⇐
  ; commute = λ _ → swapInner-natural
  ; iso     = λ _ → swapInner.iso
  })

-- Another version of the interchange that associates differently.
--
-- Why are there two versions and what's the difference? The domain
-- (X₁ ⊗ X₂) ⊗₀ (Y₁ ⊗ Y₂) and codomain (X₁ ⊗ Y₁) ⊗₀ (X₁ ⊗ Y₂) of the
-- interchange map are perfectly symmetric/balanced. But in order to
-- apply the braiding to the middle X₂ and Y₁, we need to
-- re-associate and that breaks the symmetry. We must first
-- re-associate the whole expression in one direction and then the
-- larger subterm in the other. This can be done in two ways,
-- associate to the right first, then to the left, resulting in X₁ ⊗
-- ((Y₂ ⊗₀ X₁) ⊗ Y₂), or vice versa, resulting in (X₁ ⊗ (Y₂ ⊗₀ X₁))
-- ⊗ Y₂. The choice is arbitrary and results in two distinct
-- interchange maps that behave the same way (as witnessed by
-- swapInner-coherent below).
--
-- Why define both? Because the proofs of some coherence laws become
-- easier when the core of the expression is associated in one
-- direction vs. the other. For example swapInner-unitˡ is easier to
-- prove for the second definition, while swapInner-unitʳ is easier
-- to prove for the first; swapInner-assoc uses both.

swapInner′ : (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ≅ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z)
swapInner′ = α ∘ᵢ (α ⁻¹ ∘ᵢ idᵢ ⊗ᵢ σ ∘ᵢ α) ⊗ᵢ idᵢ ∘ᵢ α ⁻¹

module swapInner′ {W X Y Z} = _≅_ (swapInner′ {W} {X} {Y} {Z})
private
  j⇒ = swapInner′.from
  j⇐ = swapInner′.to

  swapʳ : (X ⊗₀ Y) ⊗₀ Z ⇒ (X ⊗₀ Z) ⊗₀ Y
  swapʳ = α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒

-- Derived coherence laws.

swapInner-coherent : [ (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ⇒ (X₁ ⊗₀ Y₁) ⊗₀ (X₂ ⊗₀ Y₂) ]⟨
                       i⇒
                     ≈ j⇒
                     ⟩
swapInner-coherent = begin
    α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒                       ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
    α⇐ ∘ id ⊗₁ α⇒ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
    α⇐ ∘ id ⊗₁ α⇒ ∘ id ⊗₁ (σ⇒ ⊗₁ id) ∘ id ⊗₁ α⇐ ∘ α⇒          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ conjugate-from α (idᵢ ⊗ᵢ α) (⟺ pentagon) ⟩
    α⇐ ∘ id ⊗₁ α⇒ ∘ id ⊗₁ (σ⇒ ⊗₁ id) ∘ (α⇒ ∘ α⇒ ⊗₁ id) ∘ α⇐   ≈˘⟨ pullʳ (pullʳ (extendʳ (pushˡ assoc-commute-from))) ⟩
    (α⇐ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ (id ⊗₁ σ⇒) ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐   ≈⟨ pushʳ sym-assoc ⟩∘⟨refl ⟩
    ((α⇐ ∘ id ⊗₁ α⇒ ∘ α⇒) ∘ (id ⊗₁ σ⇒) ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐ ≈⟨ pushˡ (conjugate-from (α ⊗ᵢ idᵢ) α (assoc ○ pentagon)) ⟩∘⟨refl ⟩
    (α⇒ ∘ α⇐ ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐         ≈˘⟨ pushʳ (pushʳ (pushˡ split₁ˡ)) ⟩
    α⇒ ∘ α⇐ ⊗₁ id ∘ (id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐                 ≈˘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
    α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐                       ∎

private
  α-mid : ∀ {X} {Y} {Z} {W} → X ⊗₀ ((Y ⊗₀ Z) ⊗₀ W) ⇒ (X ⊗₀ Y) ⊗₀ (Z ⊗₀ W)
  α-mid = α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐

private
  serialize-assoc : α⇒ {X₁} {Y₁} {Z₁} ⊗₁ α⇒ {X₂} {Y₂} {Z₂} ≈ id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒
  serialize-assoc = begin
    α⇒ ⊗₁ α⇒                                           ≈⟨ serialize₂₁ ⟩
    id ⊗₁ α⇒ ∘ α⇒ ⊗₁ id                                ≈⟨ refl⟩∘⟨ (begin
      α⇒ ⊗₁ id                                             ≈⟨ switch-fromtoˡ α (switch-fromtoˡ (idᵢ ⊗ᵢ α) pentagon) ⟩
      α⇐ ∘ id ⊗₁ α⇐ ∘ α⇒ ∘ α⇒                             ≈˘⟨ refl⟩∘⟨ refl⟩⊗⟨ cancelˡ α.isoʳ ⟩∘⟨refl ⟩
      α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇐ ∘ α⇐) ∘ α⇒ ∘ α⇒                 ≈˘⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ pentagon-inv ⟩∘⟨refl ⟩
      α⇐ ∘ id ⊗₁ (α-mid ∘ id ⊗₁ α⇐) ∘ α⇒ ∘ α⇒             ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
      α⇐ ∘ id ⊗₁ α-mid ∘ id ⊗₁ (id ⊗₁ α⇐) ∘ α⇒ ∘ α⇒       ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩
      α⇐ ∘ id ⊗₁ α-mid ∘ α⇒ ∘ (id ⊗₁ id) ⊗₁ α⇐ ∘ α⇒       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
      α⇐ ∘ id ⊗₁ α-mid ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒               ∎) ⟩
    id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ α-mid ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒  ∎

swapInner-assoc : [ ((X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂)) ⊗₀ (Z₁ ⊗₀ Z₂) ⇒
                    (X₁ ⊗₀ (Y₁ ⊗₀ Z₁)) ⊗₀ (X₂ ⊗₀ (Y₂ ⊗₀ Z₂)) ]⟨
                    i⇒ ⊗₁ id    ⇒⟨ ((X₁ ⊗₀ Y₁) ⊗₀ (X₂ ⊗₀ Y₂)) ⊗₀ (Z₁ ⊗₀ Z₂) ⟩
                    i⇒          ⇒⟨ ((X₁ ⊗₀ Y₁) ⊗₀ Z₁) ⊗₀ ((X₂ ⊗₀ Y₂) ⊗₀ Z₂) ⟩
                    α⇒ ⊗₁ α⇒
                  ≈ α⇒          ⇒⟨ (X₁ ⊗₀ X₂) ⊗₀ ((Y₁ ⊗₀ Y₂) ⊗₀ (Z₁ ⊗₀ Z₂)) ⟩
                    id ⊗₁ i⇒    ⇒⟨ (X₁ ⊗₀ X₂) ⊗₀ ((Y₁ ⊗₀ Z₁) ⊗₀ (Y₂ ⊗₀ Z₂)) ⟩
                    i⇒
                  ⟩
swapInner-assoc = begin
    α⇒ ⊗₁ α⇒ ∘ i⇒ ∘ i⇒ ⊗₁ id                                   ≈⟨ serialize-assoc ⟩∘⟨refl ⟩
    (id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ α-mid ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒) ∘ i⇒ ∘ i⇒ ⊗₁ id  ≈˘⟨ pullˡ (pushˡ (⊗.identity ⟩⊗⟨refl ⟩∘⟨refl)) ⟩
    ((id ⊗₁ id) ⊗₁ α⇒ ∘ α⇐) ∘ (id ⊗₁ α-mid ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒) ∘ i⇒ ∘ i⇒ ⊗₁ id
                                                                  ≈⟨ ⟺ assoc-commute-to ⟩∘⟨ pullʳ (pullʳ (pushʳ (pushˡ (pushʳ (pushˡ split₂ˡ))))) ⟩
    (α⇐ ∘ id ⊗₁ (id ⊗₁ α⇒)) ∘ id ⊗₁ α-mid ∘ α⇒ ∘
    ((id ⊗₁ α⇐ ∘ α⇒) ∘ α⇐ ∘ id ⊗₁ α⇒) ∘
    (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘ i⇒ ⊗₁ id
                                                                  ≈⟨ pullʳ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ elimˡ (_≅_.isoˡ (α ⁻¹ ∘ᵢ idᵢ ⊗ᵢ α))) ⟩
    α⇐ ∘ id ⊗₁ (id ⊗₁ α⇒) ∘ id ⊗₁ α-mid ∘ α⇒ ∘
    (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
    i⇒ ⊗₁ id
                                                                  ≈⟨ refl⟩∘⟨ merge₂ sym-assoc ⟩∘⟨ pushʳ ((⟺ ⊗.identity ⟩⊗⟨refl) ⟩∘⟨refl ⟩∘⟨ split₁ˡ) ⟩
    α⇐ ∘ id ⊗₁ ((id ⊗₁ α⇒ ∘ α⇒) ∘ α⇐ ⊗₁ id ∘ α⇐) ∘
    (α⇒ ∘ (id ⊗₁ id) ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
    α⇐ ⊗₁ id ∘ (id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ⊗₁ id
                                                                  ≈⟨ refl⟩∘⟨ refl⟩⊗⟨
                                                                       extendʳ (pushˡ (switch-fromtoʳ (α ⊗ᵢ idᵢ) (assoc ○ pentagon))) ⟩∘⟨
                                                                       extendʳ assoc-commute-from ⟩∘⟨refl ⟩
    α⇐ ∘ id ⊗₁ ((α⇒ ∘ α⇒) ∘ (α⇐ ⊗₁ id ∘ α⇐ ⊗₁ id) ∘ α⇐) ∘
    (id ⊗₁ (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘ (α⇒ ∘ α⇒)) ∘ α⇐ ⊗₁ id ∘
    (id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ⊗₁ id
                                                                  ≈˘⟨ refl⟩∘⟨ refl⟩⊗⟨ pushʳ (refl⟩∘⟨ split₁ˡ ⟩∘⟨refl) ⟩∘⟨
                                                                       pushʳ (extendʳ (switch-fromtoʳ (α ⊗ᵢ idᵢ) (assoc ○ pentagon))) ⟩
    α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐) ∘
    id ⊗₁ (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘ id ⊗₁ α⇒ ∘ α⇒ ∘
    (id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ⊗₁ id
                                                                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩
    α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐) ∘
    id ⊗₁ (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘ id ⊗₁ α⇒ ∘ α⇒ ∘
    (id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐)) ⊗₁ id ∘ α⇒ ⊗₁ id
                                                                  ≈⟨ refl⟩∘⟨ merge₂ assoc²' ○ (refl⟩∘⟨ refl⟩∘⟨ assoc) ⟩∘⟨
                                                                       refl⟩∘⟨ extendʳ assoc-commute-from ⟩
    α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘
    id ⊗₁ α⇒ ∘
    id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ∘ α⇒ ∘ α⇒ ⊗₁ id
                                                                  ≈⟨ refl⟩∘⟨ merge₂ (assoc²' ○ (refl⟩∘⟨ refl⟩∘⟨ assoc²')) ⟩∘⟨
                                                                       refl⟩∘⟨ switch-fromtoˡ (idᵢ ⊗ᵢ α) pentagon ⟩
    α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
    id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ∘ id ⊗₁ α⇐ ∘ α⇒ ∘ α⇒
                                                                  ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
    α⇐ ∘ id ⊗₁
      (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
    id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ α⇒
                                                                  ≈⟨ refl⟩∘⟨ merge₂ assoc²' ○ (refl⟩∘⟨ refl⟩∘⟨ (assoc²' ○
                                                                      (refl⟩∘⟨ refl⟩∘⟨ assoc))) ⟩∘⟨ Equiv.refl ⟩
    α⇐ ∘ id ⊗₁ (α⇒ ∘
      α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘
      (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ α⇒
                                                                  ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pushʳ (begin
      α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘
      (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
                                                                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (pushˡ split₂ˡ) ⟩
      α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id) ∘ (id ⊗₁ α⇐ ∘ α⇒) ∘
      (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
                                                                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (extendʳ assoc-commute-to ○ (refl⟩∘⟨ sym-assoc)) ⟩
      α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id ∘ (α⇐ ∘ (id ⊗₁ α⇐ ∘ α⇒)) ∘
      (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
                                                                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○
                                                                         (conjugate-to α (α ⊗ᵢ idᵢ) (sym-assoc ○ pentagon-inv))) ⟩∘⟨refl ⟩
      α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id ∘ (α⇒ ⊗₁ id ∘ α⇐) ∘
      (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
                                                                  ≈˘⟨ refl⟩∘⟨ split₁ Equiv.refl ⟩∘⟨
                                                                          pushʳ (refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl) ⟩
      α⇒ ∘ ((α⇐ ∘ α⇐) ∘ id ⊗₁ σ⇒) ⊗₁ id ∘ α⇒ ⊗₁ id ∘ α⇐ ∘
      (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ (id ⊗₁ id) ∘ α⇐
                                                                  ≈⟨ refl⟩∘⟨ merge₁ assoc² ⟩∘⟨ extendʳ assoc-commute-to ⟩
      α⇒ ∘ (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘
      ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ⊗₁ id ∘ α⇐ ∘ α⇐
                                                                  ≈˘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
      α⇒ ∘ ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ⊗₁ id ∘
      α⇐ ∘ α⇐
                                                                  ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○ pentagon-inv) ⟩
      α⇒ ∘ ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ⊗₁ id ∘
      α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇐
                                                                  ≈⟨ refl⟩∘⟨ pullˡ (⟺ split₁ˡ ○ (assoc ⟩⊗⟨refl)) ⟩
      α⇒ ∘
      ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐) ⊗₁ id ∘
      α⇐ ∘ id ⊗₁ α⇐
                                                                  ≈⟨ refl⟩∘⟨ (begin
        (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐            ≈⟨ pushˡ (pushʳ sym-assoc) ⟩
        (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒ ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐            ≈⟨ (refl⟩∘⟨ extendʳ (pushʳ split₁ˡ)) ⟩
        (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒) ∘ (α⇒ ∘ α⇒ ⊗₁ id) ∘ (σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐    ≈⟨ pushʳ (switch-fromtoˡ (idᵢ ⊗ᵢ α) pentagon ⟩∘⟨ pushˡ split₁ˡ) ⟩
        ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒) ∘ (id ⊗₁ α⇐ ∘ α⇒ ∘ α⇒)) ∘
        (σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id ∘ α⇐                                         ≈⟨ pushˡ (sym-assoc ○ (pullˡ (pullʳ assoc ⟩∘⟨refl))) ⟩
        ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ id ⊗₁ α⇐) ∘ α⇒) ∘
        α⇒ ∘ (σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id ∘ α⇐                                   ≈⟨ pullʳ (refl⟩∘⟨ extendʳ assoc-commute-from) ⟩
        (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ id ⊗₁ α⇐) ∘ α⇒ ∘
        σ⇒ ⊗₁ (id ⊗₁ id) ∘ α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐                                   ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ ⟺ split₂ˡ) ⟩∘⟨ refl⟩∘⟨ (refl⟩⊗⟨ ⊗.identity ⟩∘⟨
           conjugate-from (idᵢ ⊗ᵢ (α ⁻¹)) (α ⁻¹) pentagon-inv) ⟩
        (α⇐ ∘ α⇐ ∘ id ⊗₁ (σ⇒ ∘ α⇐)) ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒            ≈˘⟨ extendʳ (sym-assoc ○ pentagon-inv) ⟩∘⟨refl ⟩
        (α⇐ ⊗₁ id ∘ (α⇐ ∘ id ⊗₁ α⇐) ∘ id ⊗₁ (σ⇒ ∘ α⇐)) ∘
        α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒                                           ≈˘⟨ (refl⟩∘⟨ pushʳ split₂ˡ) ⟩∘⟨refl ⟩
        (α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (α⇐ ∘ σ⇒ ∘ α⇐)) ∘
        α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒                                           ≈˘⟨ pushˡ ((refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (sym-assoc ○ hexagon₂ ○ assoc)) ⟩∘⟨refl) ⟩
        ((α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ σ⇒)) ∘ α⇒) ∘
        σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒                                                ≈⟨ pushˡ (pushʳ (pushʳ split₂ˡ)) ⟩∘⟨refl ⟩
        ((α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ σ⇒ ⊗₁ id) ∘ id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ∘
        σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒                                                ≈⟨ pushʳ (pushˡ split₂ˡ) ⟩∘⟨refl ⟩
        (((α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ σ⇒ ⊗₁ id) ∘ id ⊗₁ α⇐) ∘
          id ⊗₁ id ⊗₁ σ⇒ ∘ α⇒) ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒                      ≈⟨ ((pushˡ (pushʳ assoc-commute-to) ⟩∘⟨
                                                                                ⟺ assoc-commute-from) ○ (pullʳ sym-assoc)) ⟩∘⟨refl ⟩
        ((α⇐ ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id) ∘ ((α⇐ ∘ id ⊗₁ α⇐) ∘ α⇒) ∘
          (id ⊗₁ id) ⊗₁ σ⇒) ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒                         ≈⟨ pullˡ (⟺ split₁ˡ ⟩∘⟨
                                                                                conjugate-from α (idᵢ ⊗ᵢ α ∘ᵢ α) (⟺ (assoc ○ pentagon)))
                                                                                ⟩∘⟨refl ⟩
        (((α⇐ ∘ id ⊗₁ σ⇒) ⊗₁ id ∘ α⇒ ⊗₁ id ∘ α⇐) ∘ (id ⊗₁ id) ⊗₁ σ⇒) ∘
        σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒                                                ≈⟨ (pullˡ (⟺ split₁ˡ) ⟩∘⟨ ⊗.identity ⟩⊗⟨refl) ⟩∘⟨refl ⟩
        ((((α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ⊗₁ id ∘ α⇐) ∘ id ⊗₁ σ⇒) ∘
        σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒                                                ≈⟨ extend² (⟺ serialize₂₁ ○ serialize₁₂) ⟩
        ((((α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ⊗₁ id ∘ α⇐) ∘ σ⇒ ⊗₁ id) ∘
        id ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ α⇒                                                ≈˘⟨ pushʳ (refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity) ⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
        (((α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ⊗₁ id ∘ α⇐ ∘ σ⇒ ⊗₁ id ⊗₁ id) ∘
        (id ⊗₁ id) ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ α⇒                                        ≈⟨ pushʳ assoc-commute-to ⟩∘⟨ extendʳ (⟺ assoc-commute-to) ⟩
        ((((α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ⊗₁ id ∘ (σ⇒ ⊗₁ id) ⊗₁ id) ∘ α⇐) ∘
        α⇐ ∘ id ⊗₁ id ⊗₁ σ⇒ ∘ id ⊗₁ α⇒                                          ≈˘⟨ ((sym-assoc ○ sym-assoc) ⟩⊗⟨refl ○ split₁ˡ) ⟩∘⟨refl ⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩
        (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ⊗₁ id) ∘ α⇐) ∘
        α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒ ∘ α⇒)                                              ≈˘⟨ extend² (sym-assoc ○ pentagon-inv) ⟩
        (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ⊗₁ id) ∘ α⇐ ⊗₁ id) ∘
        (α⇐ ∘ id ⊗₁ α⇐) ∘ id ⊗₁ (id ⊗₁ σ⇒ ∘ α⇒)                                ≈˘⟨ split₁ˡ ⟩∘⟨ pushʳ split₂ˡ ⟩
        ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘
        α⇐ ∘ id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒)                                         ∎) ⟩⊗⟨refl ⟩∘⟨refl ⟩
      α⇒ ∘ (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘ α⇐ ∘
        id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒)) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇐               ≈⟨ (refl⟩∘⟨ pushˡ ((sym-assoc ⟩⊗⟨refl) ○ split₁ˡ)) ⟩
      α⇒ ∘ (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘ α⇐) ⊗₁ id ∘
      (id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒)) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇐                ≈⟨ (refl⟩∘⟨ split₁ˡ ⟩∘⟨ extendʳ (⟺ assoc-commute-to)) ○ pushʳ assoc ⟩
      (α⇒ ∘ (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id) ⊗₁ id) ∘
      α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ id ⊗₁ α⇐      ≈⟨ pushˡ assoc-commute-from ⟩
      ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ (id ⊗₁ id) ∘ α⇒ ∘
      α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ id ⊗₁ α⇐      ≈˘⟨ refl⟩∘⟨ pullʳ (pullʳ (refl⟩∘⟨ split₂ˡ)) ⟩
      ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ (id ⊗₁ id) ∘
      (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐)   ≈˘⟨ pullʳ (pullˡ (conjugate-from (α ∘ᵢ α ⊗ᵢ idᵢ) α pentagon)) ⟩
      (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ (id ⊗₁ id) ∘ α⇐) ∘
      id ⊗₁ α⇒ ∘ id ⊗₁ ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐)                ≈⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟩∘⟨ ⟺ split₂ˡ ⟩
      (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘ α⇐) ∘
      id ⊗₁ (α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐)                      ≡⟨⟩
      (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘ α⇐) ∘ id ⊗₁ j⇒   ≈˘⟨ switch-fromtoʳ α (switch-fromtoˡ α (⟺ hexagon₁))
                                                                                ⟩⊗⟨refl ⟩∘⟨refl ⟩∘⟨refl ⟩
      (σ⇒ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ j⇒
    ∎) ⟩∘⟨refl ⟩
    α⇐ ∘ id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ j⇒) ∘ α⇒ ∘ α⇒       ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
    α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ id ⊗₁ j⇒ ∘ α⇒ ∘ α⇒   ≈˘⟨ pullʳ (pullʳ (extendʳ assoc-commute-from)) ⟩
    (α⇐ ∘ id ⊗₁ swapˡ ∘ α⇒) ∘ (id ⊗₁ id) ⊗₁ j⇒ ∘ α⇒               ≡⟨⟩
    i⇒ ∘ (id ⊗₁ id) ⊗₁ j⇒ ∘ α⇒                                     ≈⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨ ⟺ swapInner-coherent ⟩∘⟨refl ⟩
    i⇒ ∘ id ⊗₁ i⇒ ∘ α⇒
  ∎

private
  mid-1-elim-coh : [ X ⊗₀ (unit ⊗₀ Y) ⇒ X ⊗₀ Y ]⟨ λ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ≈ id ⊗₁ λ⇒ ⟩
  mid-1-elim-coh = begin
    λ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐  ≈⟨ pullˡ (Kelly's.coherence₁ M) ⟩
    λ⇒ ⊗₁ id ∘ σ⇒ ⊗₁ id ∘ α⇐ ≈˘⟨  pushˡ split₁ˡ ⟩
    (λ⇒ ∘ σ⇒) ⊗₁ id ∘ α⇐     ≈⟨ braiding-coherence B ⟩⊗⟨refl ⟩∘⟨refl ⟩
    ρ⇒ ⊗₁ id ∘ α⇐             ≈˘⟨ switch-fromtoʳ α triangle ⟩
    id ⊗₁ λ⇒                  ∎

  Kelly₁′ :  [ unit ⊗₀ (X ⊗₀ Y) ⇒ X ⊗₀ Y ]⟨ λ⇒ ⊗₁ id ∘ α⇐ ≈ λ⇒ ⟩
  Kelly₁′ = ⟺ (switch-fromtoʳ α (Kelly's.coherence₁ M))

  Kelly₂′ : [  X ⊗₀ (Y ⊗₀ unit) ⇒ X ⊗₀ Y ]⟨ ρ⇒ ∘ α⇐ ≈ id ⊗₁ ρ⇒ ⟩
  Kelly₂′ = ⟺ (switch-fromtoʳ α (Kelly's.coherence₂ M))

  σ⁻¹-coherence : [ unit ⊗₀ X ⇒ X ]⟨ ρ⇒ ∘ σ⇒ ≈ λ⇒ ⟩
  σ⁻¹-coherence = inv-braiding-coherence (inv-Braided B)

swapInner-unitˡ : [ unit ⊗₀ (X ⊗₀ Y) ⇒ (X ⊗₀ Y) ]⟨
                    λ⇐ ⊗₁ id         ⇒⟨ (unit ⊗₀ unit) ⊗₀ (X ⊗₀ Y) ⟩
                    i⇒               ⇒⟨ (unit ⊗₀ X) ⊗₀ (unit ⊗₀ Y) ⟩
                    λ⇒ ⊗₁ λ⇒
                  ≈ λ⇒
                  ⟩
swapInner-unitˡ = begin
    λ⇒ ⊗₁ λ⇒ ∘ i⇒ ∘ λ⇐ ⊗₁ id      ≈⟨ refl⟩∘⟨ swapInner-coherent ⟩∘⟨ (Kelly's.coherence-inv₃ M ⟩⊗⟨refl) ⟩
    λ⇒ ⊗₁ λ⇒ ∘ j⇒ ∘ ρ⇐ ⊗₁ id      ≈⟨ pullˡ (pushˡ serialize₁₂) ⟩
    (λ⇒ ⊗₁ id ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ swapʳ ⊗₁ id ∘ α⇐) ∘ ρ⇐ ⊗₁ id
  ≈⟨ (refl⟩∘⟨ (begin
      id ⊗₁ λ⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐  ≈⟨ pullˡ triangle ⟩
      ρ⇒ ⊗₁ id ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐       ≈˘⟨ pushˡ split₁ˡ ⟩
      (ρ⇒ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐             ≈⟨ (pullˡ Kelly₂′ ⟩⊗⟨refl ⟩∘⟨refl) ⟩
      (id ⊗₁ ρ⇒ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐            ≈˘⟨ pushˡ split₂ˡ ⟩⊗⟨refl ⟩∘⟨refl ⟩
      (id ⊗₁ (ρ⇒ ∘ σ⇒) ∘ α⇒) ⊗₁ id ∘ α⇐                ≈⟨ (refl⟩⊗⟨ σ⁻¹-coherence ⟩∘⟨refl) ⟩⊗⟨refl ⟩∘⟨refl ⟩
      (id ⊗₁ λ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐                        ≈⟨ triangle ⟩⊗⟨refl ⟩∘⟨refl ⟩
      (ρ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐                             ≈˘⟨ assoc-commute-to ⟩
      α⇐ ∘ ρ⇒ ⊗₁ (id ⊗₁ id)
    ∎)) ⟩∘⟨refl ⟩
    (λ⇒ ⊗₁ id ∘ α⇐ ∘ ρ⇒ ⊗₁ (id ⊗₁ id)) ∘ ρ⇐ ⊗₁ id   ≈⟨ (sym-assoc ○ (Kelly₁′ ⟩∘⟨ refl⟩⊗⟨ ⊗.identity)) ⟩∘⟨refl ⟩
    (λ⇒ ∘ ρ⇒ ⊗₁ id) ∘ ρ⇐ ⊗₁ id                       ≈⟨ cancelʳ (_≅_.isoʳ (unitorʳ ⊗ᵢ idᵢ)) ⟩
    λ⇒
  ∎

swapInner-unitʳ : [ (X ⊗₀ Y) ⊗₀ unit ⇒ (X ⊗₀ Y) ]⟨
                    id ⊗₁ λ⇐         ⇒⟨ (X ⊗₀ Y) ⊗₀ (unit ⊗₀ unit) ⟩
                    i⇒               ⇒⟨ (X ⊗₀ unit) ⊗₀ (Y ⊗₀ unit) ⟩
                    ρ⇒ ⊗₁ ρ⇒
                  ≈ ρ⇒
                  ⟩
swapInner-unitʳ = begin
    ρ⇒ ⊗₁ ρ⇒ ∘ i⇒ ∘ id ⊗₁ λ⇐                                  ≡⟨⟩
    ρ⇒ ⊗₁ ρ⇒ ∘ (α⇐ ∘ id ⊗₁ swapˡ ∘ α⇒) ∘ id ⊗₁ λ⇐            ≈⟨ pullˡ (pushˡ serialize₂₁) ⟩
    (id ⊗₁ ρ⇒ ∘ ρ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ swapˡ ∘ α⇒) ∘ id ⊗₁ λ⇐ ≈⟨ (refl⟩∘⟨ (begin
      ρ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ swapˡ ∘ α⇒                                  ≈˘⟨ pushˡ (switch-fromtoʳ α triangle) ⟩
      id ⊗₁ λ⇒ ∘ id ⊗₁ swapˡ ∘ α⇒                                       ≈˘⟨ pushˡ split₂ˡ ⟩
      id ⊗₁ (λ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒                             ≈⟨ refl⟩⊗⟨ mid-1-elim-coh ⟩∘⟨refl ⟩
      id ⊗₁ (id ⊗₁ λ⇒) ∘ α⇒                                             ≈˘⟨ assoc-commute-from ⟩
      α⇒ ∘ (id ⊗₁ id) ⊗₁ λ⇒                                             ≈⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩
      α⇒ ∘ id ⊗₁ λ⇒                                                     ∎)) ⟩∘⟨refl ⟩
    (id ⊗₁ ρ⇒ ∘ α⇒ ∘ id ⊗₁ λ⇒) ∘ id ⊗₁ λ⇐                    ≈⟨ (sym-assoc ○ (Kelly's.coherence₂ M ⟩∘⟨refl )) ⟩∘⟨refl ⟩
    (ρ⇒ ∘ id ⊗₁ λ⇒) ∘ id ⊗₁ λ⇐                                ≈⟨ cancelʳ (_≅_.isoʳ (idᵢ ⊗ᵢ unitorˡ)) ⟩
    ρ⇒                                                         ∎

-- Two different ways of swapping things around are the same
private
  [23][14]ʳ : [ (X ⊗₀ Y) ⊗₀ (Z ⊗₀ W) ⇒ (Y ⊗₀ Z) ⊗₀ (X ⊗₀ W) ]⟨ α⇒ ∘ swapʳ ⊗₁ id ∘ (σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐ ≈ (α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐ ⟩
  [23][14]ʳ = begin
    (α⇒ ∘ swapʳ ⊗₁ id ∘ (σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐)  ≈˘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
    (α⇒ ∘ (swapʳ ∘ σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐)        ≈⟨ refl⟩∘⟨ pullʳ (assoc ○ hexagon₁) ⟩⊗⟨refl ⟩∘⟨refl ⟩
    (α⇒ ∘ (α⇐ ∘ α⇒ ∘ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐)       ≈⟨ refl⟩∘⟨ cancelˡ α.isoˡ ⟩⊗⟨refl ⟩∘⟨refl ⟩
    (α⇒ ∘ (σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐)                 ≈⟨ extendʳ (pushʳ split₁ˡ) ⟩
    ((α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐)           ∎

  [13][42]ˡ : [ (X ⊗₀ Y) ⊗₀ (Z ⊗₀ W) ⇒ (X ⊗₀ Z)  ⊗₀ (W ⊗₀ Y) ]⟨ α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒) ∘ id ⊗₁ swapˡ ∘ α⇒ ≈ (α⇐ ∘ id ⊗₁ α⇒) ∘ id ⊗₁ σ⇒ ∘ α⇒ ⟩
  [13][42]ˡ = begin
    α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒) ∘ id ⊗₁ swapˡ ∘ α⇒         ≈˘⟨  refl⟩∘⟨ pushˡ split₂ˡ ⟩
    α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (⟺ assoc ○ (pullˡ (assoc ○ hexagon₁))) ⟩∘⟨refl ⟩
    α⇐ ∘ id ⊗₁ ((α⇒ ∘ σ⇒ ∘ α⇒) ∘ α⇐) ∘ α⇒            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ (cancelʳ α.isoʳ) ⟩∘⟨refl ⟩
    α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒) ∘ α⇒                         ≈⟨ extendʳ (pushʳ split₂ˡ) ⟩
    (α⇐ ∘ id ⊗₁ α⇒) ∘ id ⊗₁ σ⇒ ∘ α⇒                  ∎

swapInner-braiding : [ (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ⇒ (Y ⊗₀ Z) ⊗₀ (W ⊗₀ X) ]⟨
                       i⇒         ⇒⟨ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z) ⟩
                       σ⇒ ⊗₁ σ⇒   ⇒⟨ (Y ⊗₀ W) ⊗₀ (Z ⊗₀ X) ⟩
                       i⇒
                     ≈ σ⇒
                     ⟩
swapInner-braiding = begin
    i⇒ ∘ σ⇒ ⊗₁ σ⇒ ∘ i⇒                                  ≡⟨⟩
    i⇒ ∘ σ⇒ ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ swapˡ ∘ α⇒              ≈⟨ swapInner-coherent ⟩∘⟨ pushˡ serialize₁₂ ⟩
    j⇒ ∘ σ⇒ ⊗₁ id ∘ id ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ swapˡ ∘ α⇒  ≈˘⟨ ((refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity) ⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl) ○ assoc ⟩
    ((α⇒ ∘ swapʳ ⊗₁ id ∘ α⇐) ∘ σ⇒ ⊗₁ (id ⊗₁ id)) ∘
    (id ⊗₁ id) ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ swapˡ ∘ α⇒           ≈⟨ pullʳ (pullʳ assoc-commute-to) ⟩∘⟨ extendʳ (⟺ assoc-commute-to) ⟩
    (α⇒ ∘ swapʳ ⊗₁ id ∘ (σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐) ∘
    α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒) ∘ id ⊗₁ swapˡ ∘ α⇒           ≈⟨ [23][14]ʳ ⟩∘⟨ [13][42]ˡ ⟩
    ((α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐) ∘ (α⇐ ∘ id ⊗₁ α⇒) ∘ id ⊗₁ σ⇒ ∘ α⇒  ≈˘⟨ extendʳ (pushʳ (pushʳ assoc)) ⟩
    (α⇒ ∘ σ⇒ ⊗₁ id) ∘ (α⇒ ⊗₁ id ∘ (α⇐ ∘ α⇐) ∘ id ⊗₁ α⇒) ∘ id ⊗₁ σ⇒ ∘ α⇒  ≈˘⟨ refl⟩∘⟨ switch-tofromˡ (α ⊗ᵢ idᵢ)
                                                                                (switch-tofromʳ (idᵢ ⊗ᵢ α) pentagon-inv) ⟩∘⟨refl ⟩
    (α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒               ≈⟨ pullʳ (sym-assoc ○ pullˡ hexagon₂) ⟩
    α⇒ ∘ ((α⇐ ∘ σ⇒) ∘ α⇐) ∘ α⇒                          ≈⟨ (refl⟩∘⟨ cancelʳ α.isoˡ) ⟩
    α⇒ ∘ (α⇐ ∘ σ⇒)                                       ≈⟨ cancelˡ α.isoʳ ⟩
    σ⇒                                                   ∎

-- Braided monoidal categories have an interchange.

hasInterchange : HasInterchange M
hasInterchange = record
  { swapInner  = swapInner
  ; natural    = swapInner-natural
  ; assoc      = swapInner-assoc
  ; unitˡ      = swapInner-unitˡ
  ; unitʳ      = swapInner-unitʳ
  }
open HasInterchange hasInterchange public using (naturalIso)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories