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

module PiLevel1 where

open import Data.Unit using (⊤; tt)
open import Relation.Binary.Core using (IsEquivalence)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym; [_])

open import PiU using (U; ZERO; ONE; PLUS; TIMES)
open import PiLevel0
  -- hiding triv≡ certainly; we are replacing it with _⇔_
  using (_⟷_; !;
         unite₊l; uniti₊l; unite₊r; uniti₊r; swap₊; assocl₊; assocr₊;
         unite⋆l; uniti⋆l; unite⋆r; uniti⋆r; swap⋆; assocl⋆; assocr⋆;
         absorbr; absorbl; factorzr; factorzl;
         dist; factor; distl; factorl;
         id⟷; _◎_; _⊕_; _⊗_)

------------------------------------------------------------------------------
-- Level 1: instead of using triv≡ to reason about equivalence of
-- combinators, we use the following 2-combinators

infix  30 _⇔_

data _⇔_ : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₁ ⟷ t₂) → Set where
  assoc◎l : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
          (c₁ ◎ (c₂ ◎ c₃)) ⇔ ((c₁ ◎ c₂) ◎ c₃)
  assoc◎r : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
          ((c₁ ◎ c₂) ◎ c₃) ⇔ (c₁ ◎ (c₂ ◎ c₃))
  assocl⊕l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          ((c₁ ⊕ (c₂ ⊕ c₃)) ◎ assocl₊) ⇔ (assocl₊ ◎ ((c₁ ⊕ c₂) ⊕ c₃))
  assocl⊕r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          (assocl₊ ◎ ((c₁ ⊕ c₂) ⊕ c₃)) ⇔ ((c₁ ⊕ (c₂ ⊕ c₃)) ◎ assocl₊)
  assocl⊗l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          ((c₁ ⊗ (c₂ ⊗ c₃)) ◎ assocl⋆) ⇔ (assocl⋆ ◎ ((c₁ ⊗ c₂) ⊗ c₃))
  assocl⊗r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          (assocl⋆ ◎ ((c₁ ⊗ c₂) ⊗ c₃)) ⇔ ((c₁ ⊗ (c₂ ⊗ c₃)) ◎ assocl⋆)
  assocr⊕r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          (((c₁ ⊕ c₂) ⊕ c₃) ◎ assocr₊) ⇔ (assocr₊ ◎ (c₁ ⊕ (c₂ ⊕ c₃)))
  assocr⊗l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
           (assocr⋆ ◎ (c₁ ⊗ (c₂ ⊗ c₃))) ⇔ (((c₁ ⊗ c₂) ⊗ c₃) ◎ assocr⋆)
  assocr⊗r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          (((c₁ ⊗ c₂) ⊗ c₃) ◎ assocr⋆) ⇔ (assocr⋆ ◎ (c₁ ⊗ (c₂ ⊗ c₃)))
  assocr⊕l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
           (assocr₊ ◎ (c₁ ⊕ (c₂ ⊕ c₃))) ⇔ (((c₁ ⊕ c₂) ⊕ c₃) ◎ assocr₊)
  dist⇔l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {a : t₁ ⟷ t₂} {b : t₃ ⟷ t₄} {c : t₅ ⟷ t₆} →
      ((a ⊕ b) ⊗ c) ◎ dist ⇔ dist ◎ ((a ⊗ c) ⊕ (b ⊗ c))
  dist⇔r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {a : t₁ ⟷ t₂} {b : t₃ ⟷ t₄} {c : t₅ ⟷ t₆} →
      dist ◎ ((a ⊗ c) ⊕ (b ⊗ c)) ⇔ ((a ⊕ b) ⊗ c) ◎ dist
  distl⇔l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {a : t₁ ⟷ t₂} {b : t₃ ⟷ t₄} {c : t₅ ⟷ t₆} →
      (a ⊗ (b ⊕ c)) ◎ distl ⇔ distl ◎ ((a ⊗ b) ⊕ (a ⊗ c))
  distl⇔r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {a : t₁ ⟷ t₂} {b : t₃ ⟷ t₄} {c : t₅ ⟷ t₆} →
      distl ◎ ((a ⊗ b) ⊕ (a ⊗ c)) ⇔ (a ⊗ (b ⊕ c)) ◎ distl
  factor⇔l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {a : t₁ ⟷ t₂} {b : t₃ ⟷ t₄} {c : t₅ ⟷ t₆} →
       ((a ⊗ c) ⊕ (b ⊗ c)) ◎ factor ⇔ factor ◎ ((a ⊕ b) ⊗ c)
  factor⇔r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {a : t₁ ⟷ t₂} {b : t₃ ⟷ t₄} {c : t₅ ⟷ t₆} →
       factor ◎ ((a ⊕ b) ⊗ c) ⇔ ((a ⊗ c) ⊕ (b ⊗ c)) ◎ factor
  factorl⇔l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {a : t₁ ⟷ t₂} {b : t₃ ⟷ t₄} {c : t₅ ⟷ t₆} →
       ((a ⊗ b) ⊕ (a ⊗ c)) ◎ factorl ⇔ factorl ◎ (a ⊗ (b ⊕ c))
  factorl⇔r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {a : t₁ ⟷ t₂} {b : t₃ ⟷ t₄} {c : t₅ ⟷ t₆} →
       factorl ◎ (a ⊗ (b ⊕ c)) ⇔ ((a ⊗ b) ⊕ (a ⊗ c)) ◎ factorl
  idl◎l   : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (id⟷ ◎ c) ⇔ c
  idl◎r   : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ⇔ id⟷ ◎ c
  idr◎l   : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (c ◎ id⟷) ⇔ c
  idr◎r   : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ⇔ (c ◎ id⟷)
  linv◎l  : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (c ◎ ! c) ⇔ id⟷
  linv◎r  : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → id⟷ ⇔ (c ◎ ! c)
  rinv◎l  : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (! c ◎ c) ⇔ id⟷
  rinv◎r  : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → id⟷ ⇔ (! c ◎ c)
  unite₊l⇔l : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          (unite₊l ◎ c₂) ⇔ ((c₁ ⊕ c₂) ◎ unite₊l)
  unite₊l⇔r : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          ((c₁ ⊕ c₂) ◎ unite₊l) ⇔ (unite₊l ◎ c₂)
  uniti₊l⇔l : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          (uniti₊l ◎ (c₁ ⊕ c₂)) ⇔ (c₂ ◎ uniti₊l)
  uniti₊l⇔r : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          (c₂ ◎ uniti₊l) ⇔ (uniti₊l ◎ (c₁ ⊕ c₂))
  unite₊r⇔l : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          (unite₊r ◎ c₂) ⇔ ((c₂ ⊕ c₁) ◎ unite₊r)
  unite₊r⇔r : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          ((c₂ ⊕ c₁) ◎ unite₊r) ⇔ (unite₊r ◎ c₂)
  uniti₊r⇔l : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          (uniti₊r ◎ (c₂ ⊕ c₁)) ⇔ (c₂ ◎ uniti₊r)
  uniti₊r⇔r : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          (c₂ ◎ uniti₊r) ⇔ (uniti₊r ◎ (c₂ ⊕ c₁))
  swapl₊⇔ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} →
          (swap₊ ◎ (c₁ ⊕ c₂)) ⇔ ((c₂ ⊕ c₁) ◎ swap₊)
  swapr₊⇔ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} →
          ((c₂ ⊕ c₁) ◎ swap₊) ⇔ (swap₊ ◎ (c₁ ⊕ c₂))
  unitel⋆⇔l : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          (unite⋆l ◎ c₂) ⇔ ((c₁ ⊗ c₂) ◎ unite⋆l)
  uniter⋆⇔l : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          ((c₁ ⊗ c₂) ◎ unite⋆l) ⇔ (unite⋆l ◎ c₂)
  unitil⋆⇔l : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          (uniti⋆l ◎ (c₁ ⊗ c₂)) ⇔ (c₂ ◎ uniti⋆l)
  unitir⋆⇔l : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          (c₂ ◎ uniti⋆l) ⇔ (uniti⋆l ◎ (c₁ ⊗ c₂))
  unitel⋆⇔r : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          (unite⋆r ◎ c₂) ⇔ ((c₂ ⊗ c₁) ◎ unite⋆r)
  uniter⋆⇔r : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          ((c₂ ⊗ c₁) ◎ unite⋆r) ⇔ (unite⋆r ◎ c₂)
  unitil⋆⇔r : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          (uniti⋆r ◎ (c₂ ⊗ c₁)) ⇔ (c₂ ◎ uniti⋆r)
  unitir⋆⇔r : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          (c₂ ◎ uniti⋆r) ⇔ (uniti⋆r ◎ (c₂ ⊗ c₁))
  swapl⋆⇔ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} →
          (swap⋆ ◎ (c₁ ⊗ c₂)) ⇔ ((c₂ ⊗ c₁) ◎ swap⋆)
  swapr⋆⇔ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} →
          ((c₂ ⊗ c₁) ◎ swap⋆) ⇔ (swap⋆ ◎ (c₁ ⊗ c₂))
  id⇔     : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ⇔ c
  trans⇔  : {t₁ t₂ : U} {c₁ c₂ c₃ : t₁ ⟷ t₂} →
         (c₁ ⇔ c₂) → (c₂ ⇔ c₃) → (c₁ ⇔ c₃)
  _⊡_  : {t₁ t₂ t₃ : U}
         {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₁ ⟷ t₂} {c₄ : t₂ ⟷ t₃} →
         (c₁ ⇔ c₃) → (c₂ ⇔ c₄) → (c₁ ◎ c₂) ⇔ (c₃ ◎ c₄)
  resp⊕⇔  : {t₁ t₂ t₃ t₄ : U}
         {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₁ ⟷ t₂} {c₄ : t₃ ⟷ t₄} →
         (c₁ ⇔ c₃) → (c₂ ⇔ c₄) → (c₁ ⊕ c₂) ⇔ (c₃ ⊕ c₄)
  resp⊗⇔  : {t₁ t₂ t₃ t₄ : U}
         {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₁ ⟷ t₂} {c₄ : t₃ ⟷ t₄} →
         (c₁ ⇔ c₃) → (c₂ ⇔ c₄) → (c₁ ⊗ c₂) ⇔ (c₃ ⊗ c₄)
  -- below are the combinators added for the RigCategory structure
  id⟷⊕id⟷⇔ : {t₁ t₂ : U} → (id⟷ {t₁} ⊕ id⟷ {t₂}) ⇔ id⟷
  split⊕-id⟷ : {t₁ t₂ : U} → (id⟷ {PLUS t₁ t₂}) ⇔ (id⟷ ⊕ id⟷)
  hom⊕◎⇔ : {t₁ t₂ t₃ t₄ t₅ t₆ : U} {c₁ : t₅ ⟷ t₁} {c₂ : t₆ ⟷ t₂}
        {c₃ : t₁ ⟷ t₃} {c₄ : t₂ ⟷ t₄} →
        ((c₁ ◎ c₃) ⊕ (c₂ ◎ c₄)) ⇔ ((c₁ ⊕ c₂) ◎ (c₃ ⊕ c₄))
  hom◎⊕⇔ : {t₁ t₂ t₃ t₄ t₅ t₆ : U} {c₁ : t₅ ⟷ t₁} {c₂ : t₆ ⟷ t₂}
        {c₃ : t₁ ⟷ t₃} {c₄ : t₂ ⟷ t₄} →
         ((c₁ ⊕ c₂) ◎ (c₃ ⊕ c₄)) ⇔ ((c₁ ◎ c₃) ⊕ (c₂ ◎ c₄))
  id⟷⊗id⟷⇔ : {t₁ t₂ : U} → (id⟷ {t₁} ⊗ id⟷ {t₂}) ⇔ id⟷
  split⊗-id⟷ : {t₁ t₂ : U} → (id⟷ {TIMES t₁ t₂}) ⇔ (id⟷ ⊗ id⟷)
  hom⊗◎⇔ : {t₁ t₂ t₃ t₄ t₅ t₆ : U} {c₁ : t₅ ⟷ t₁} {c₂ : t₆ ⟷ t₂}
        {c₃ : t₁ ⟷ t₃} {c₄ : t₂ ⟷ t₄} →
        ((c₁ ◎ c₃) ⊗ (c₂ ◎ c₄)) ⇔ ((c₁ ⊗ c₂) ◎ (c₃ ⊗ c₄))
  hom◎⊗⇔ : {t₁ t₂ t₃ t₄ t₅ t₆ : U} {c₁ : t₅ ⟷ t₁} {c₂ : t₆ ⟷ t₂}
        {c₃ : t₁ ⟷ t₃} {c₄ : t₂ ⟷ t₄} →
         ((c₁ ⊗ c₂) ◎ (c₃ ⊗ c₄)) ⇔ ((c₁ ◎ c₃) ⊗ (c₂ ◎ c₄))
  -- associativity triangle
  triangle⊕l : {t₁ t₂ : U} →
    (unite₊r {t₁} ⊕ id⟷ {t₂}) ⇔ assocr₊ ◎ (id⟷ ⊕ unite₊l)
  triangle⊕r : {t₁ t₂ : U} →
    assocr₊ ◎ (id⟷ {t₁} ⊕ unite₊l {t₂}) ⇔ (unite₊r ⊕ id⟷)
  triangle⊗l : {t₁ t₂ : U} →
    ((unite⋆r {t₁}) ⊗ id⟷ {t₂}) ⇔ assocr⋆ ◎ (id⟷ ⊗ unite⋆l)
  triangle⊗r : {t₁ t₂ : U} →
    (assocr⋆ ◎ (id⟷ {t₁} ⊗ unite⋆l {t₂})) ⇔ (unite⋆r ⊗ id⟷)
  pentagon⊕l : {t₁ t₂ t₃ t₄ : U} →
    assocr₊ ◎ (assocr₊ {t₁} {t₂} {PLUS t₃ t₄}) ⇔
    ((assocr₊ ⊕ id⟷) ◎ assocr₊) ◎ (id⟷ ⊕ assocr₊)
  pentagon⊕r : {t₁ t₂ t₃ t₄ : U} →
    ((assocr₊ {t₁} {t₂} {t₃} ⊕ id⟷ {t₄}) ◎ assocr₊) ◎ (id⟷ ⊕ assocr₊) ⇔
    assocr₊ ◎ assocr₊
  pentagon⊗l : {t₁ t₂ t₃ t₄ : U} →
    assocr⋆ ◎ (assocr⋆ {t₁} {t₂} {TIMES t₃ t₄}) ⇔
    ((assocr⋆ ⊗ id⟷) ◎ assocr⋆) ◎ (id⟷ ⊗ assocr⋆)
  pentagon⊗r : {t₁ t₂ t₃ t₄ : U} →
    ((assocr⋆ {t₁} {t₂} {t₃} ⊗ id⟷ {t₄}) ◎ assocr⋆) ◎ (id⟷ ⊗ assocr⋆) ⇔
    assocr⋆ ◎ assocr⋆
  -- from the braiding
  -- unit coherence
  unite₊l-coh-l : {t₁ : U} → unite₊l {t₁} ⇔ swap₊ ◎ unite₊r
  unite₊l-coh-r : {t₁ : U} → swap₊ ◎ unite₊r ⇔ unite₊l {t₁}
  unite⋆l-coh-l : {t₁ : U} → unite⋆l {t₁} ⇔ swap⋆ ◎ unite⋆r
  unite⋆l-coh-r : {t₁ : U} → swap⋆ ◎ unite⋆r ⇔ unite⋆l {t₁}
  hexagonr⊕l : {t₁ t₂ t₃ : U} →
    (assocr₊ ◎ swap₊) ◎ assocr₊ {t₁} {t₂} {t₃} ⇔
    ((swap₊ ⊕ id⟷) ◎ assocr₊) ◎ (id⟷ ⊕ swap₊)
  hexagonr⊕r : {t₁ t₂ t₃ : U} →
    ((swap₊ ⊕ id⟷) ◎ assocr₊) ◎ (id⟷ ⊕ swap₊) ⇔
    (assocr₊ ◎ swap₊) ◎ assocr₊ {t₁} {t₂} {t₃}
  hexagonl⊕l : {t₁ t₂ t₃ : U} →
    (assocl₊ ◎ swap₊) ◎ assocl₊ {t₁} {t₂} {t₃} ⇔
    ((id⟷ ⊕ swap₊) ◎ assocl₊) ◎ (swap₊ ⊕ id⟷)
  hexagonl⊕r : {t₁ t₂ t₃ : U} →
    ((id⟷ ⊕ swap₊) ◎ assocl₊) ◎ (swap₊ ⊕ id⟷) ⇔
    (assocl₊ ◎ swap₊) ◎ assocl₊ {t₁} {t₂} {t₃}
  hexagonr⊗l : {t₁ t₂ t₃ : U} →
    (assocr⋆ ◎ swap⋆) ◎ assocr⋆ {t₁} {t₂} {t₃} ⇔
    ((swap⋆ ⊗ id⟷) ◎ assocr⋆) ◎ (id⟷ ⊗ swap⋆)
  hexagonr⊗r : {t₁ t₂ t₃ : U} →
    ((swap⋆ ⊗ id⟷) ◎ assocr⋆) ◎ (id⟷ ⊗ swap⋆) ⇔
    (assocr⋆ ◎ swap⋆) ◎ assocr⋆ {t₁} {t₂} {t₃}
  hexagonl⊗l : {t₁ t₂ t₃ : U} →
    (assocl⋆ ◎ swap⋆) ◎ assocl⋆ {t₁} {t₂} {t₃} ⇔
    ((id⟷ ⊗ swap⋆) ◎ assocl⋆) ◎ (swap⋆ ⊗ id⟷)
  hexagonl⊗r : {t₁ t₂ t₃ : U} →
    ((id⟷ ⊗ swap⋆) ◎ assocl⋆) ◎ (swap⋆ ⊗ id⟷) ⇔
    (assocl⋆ ◎ swap⋆) ◎ assocl⋆ {t₁} {t₂} {t₃}
  absorbl⇔l : {t₁ t₂ : U} {c₁ : t₁ ⟷ t₂} →
    (c₁ ⊗ id⟷ {ZERO}) ◎ absorbl ⇔ absorbl ◎ id⟷ {ZERO}
  absorbl⇔r : {t₁ t₂ : U} {c₁ : t₁ ⟷ t₂} →
    absorbl ◎ id⟷ {ZERO} ⇔ (c₁ ⊗ id⟷ {ZERO}) ◎ absorbl
  absorbr⇔l : {t₁ t₂ : U} {c₁ : t₁ ⟷ t₂} →
    (id⟷ {ZERO} ⊗ c₁) ◎ absorbr ⇔ absorbr ◎ id⟷ {ZERO}
  absorbr⇔r : {t₁ t₂ : U} {c₁ : t₁ ⟷ t₂} →
    absorbr ◎ id⟷ {ZERO} ⇔ (id⟷ {ZERO} ⊗ c₁) ◎ absorbr
  factorzl⇔l : {t₁ t₂ : U} {c₁ : t₁ ⟷ t₂} →
    id⟷ ◎ factorzl ⇔ factorzl ◎ (id⟷ ⊗ c₁)
  factorzl⇔r : {t₁ t₂ : U} {c₁ : t₁ ⟷ t₂} →
    factorzl ◎ (id⟷ {ZERO} ⊗ c₁) ⇔ id⟷ {ZERO} ◎ factorzl
  factorzr⇔l : {t₁ t₂ : U} {c₁ : t₁ ⟷ t₂} →
    id⟷ ◎ factorzr ⇔ factorzr ◎ (c₁ ⊗ id⟷)
  factorzr⇔r : {t₁ t₂ : U} {c₁ : t₁ ⟷ t₂} →
    factorzr ◎ (c₁ ⊗ id⟷) ⇔ id⟷ ◎ factorzr
  -- from the coherence conditions of RigCategory
  swap₊distl⇔l : {t₁ t₂ t₃ : U} →
    (id⟷ {t₁} ⊗ swap₊ {t₂} {t₃}) ◎ distl ⇔ distl ◎ swap₊
  swap₊distl⇔r : {t₁ t₂ t₃ : U} →
    distl ◎ swap₊ ⇔ (id⟷ {t₁} ⊗ swap₊ {t₂} {t₃}) ◎ distl
  dist-swap⋆⇔l : {t₁ t₂ t₃ : U} →
    dist {t₁} {t₂} {t₃} ◎ (swap⋆ ⊕ swap⋆) ⇔ swap⋆ ◎ distl
  dist-swap⋆⇔r : {t₁ t₂ t₃ : U} →
    swap⋆ ◎ distl {t₁} {t₂} {t₃} ⇔ dist ◎ (swap⋆ ⊕ swap⋆)
  assocl₊-dist-dist⇔l : {t₁ t₂ t₃ t₄ : U} →
    ((assocl₊ {t₁} {t₂} {t₃} ⊗ id⟷ {t₄}) ◎ dist) ◎ (dist ⊕ id⟷) ⇔
    (dist ◎ (id⟷ ⊕ dist)) ◎ assocl₊
  assocl₊-dist-dist⇔r : {t₁ t₂ t₃ t₄ : U} →
    (dist {t₁} ◎ (id⟷ ⊕ dist {t₂} {t₃} {t₄})) ◎ assocl₊ ⇔
    ((assocl₊ ⊗ id⟷) ◎ dist) ◎ (dist ⊕ id⟷)
  assocl⋆-distl⇔l : {t₁ t₂ t₃ t₄ : U} →
    assocl⋆ {t₁} {t₂} ◎ distl {TIMES t₁ t₂} {t₃} {t₄} ⇔
    ((id⟷ ⊗ distl) ◎ distl) ◎ (assocl⋆ ⊕ assocl⋆)
  assocl⋆-distl⇔r : {t₁ t₂ t₃ t₄ : U} →
    ((id⟷ ⊗ distl) ◎ distl) ◎ (assocl⋆ ⊕ assocl⋆) ⇔
    assocl⋆ {t₁} {t₂} ◎ distl {TIMES t₁ t₂} {t₃} {t₄}
  absorbr0-absorbl0⇔ : absorbr {ZERO} ⇔ absorbl {ZERO}
  absorbl0-absorbr0⇔ : absorbl {ZERO} ⇔ absorbr {ZERO}
  absorbr⇔distl-absorb-unite : {t₁ t₂ : U} →
    absorbr ⇔ (distl {t₂ = t₁} {t₂} ◎ (absorbr ⊕ absorbr)) ◎ unite₊l
  distl-absorb-unite⇔absorbr : {t₁ t₂ : U} →
    (distl {t₂ = t₁} {t₂} ◎ (absorbr ⊕ absorbr)) ◎ unite₊l ⇔ absorbr
  unite⋆r0-absorbr1⇔ : unite⋆r ⇔ absorbr
  absorbr1-unite⋆r-⇔ : absorbr ⇔ unite⋆r
  absorbl≡swap⋆◎absorbr : {t₁ : U} → absorbl {t₁} ⇔ swap⋆ ◎ absorbr
  swap⋆◎absorbr≡absorbl : {t₁ : U} → swap⋆ ◎ absorbr ⇔ absorbl {t₁}
  absorbr⇔[assocl⋆◎[absorbr⊗id⟷]]◎absorbr : {t₁ t₂ : U} →
    absorbr ⇔ (assocl⋆ {ZERO} {t₁} {t₂} ◎ (absorbr ⊗ id⟷)) ◎ absorbr
  [assocl⋆◎[absorbr⊗id⟷]]◎absorbr⇔absorbr : {t₁ t₂ : U} →
    (assocl⋆ {ZERO} {t₁} {t₂} ◎ (absorbr ⊗ id⟷)) ◎ absorbr ⇔ absorbr
  [id⟷⊗absorbr]◎absorbl⇔assocl⋆◎[absorbl⊗id⟷]◎absorbr : {t₁ t₂ : U} →
    (id⟷ ⊗ absorbr {t₂}) ◎ absorbl {t₁} ⇔
    (assocl⋆ ◎ (absorbl ⊗ id⟷)) ◎ absorbr
  assocl⋆◎[absorbl⊗id⟷]◎absorbr⇔[id⟷⊗absorbr]◎absorbl : {t₁ t₂ : U} →
    (assocl⋆ ◎ (absorbl ⊗ id⟷)) ◎ absorbr ⇔
    (id⟷ ⊗ absorbr {t₂}) ◎ absorbl {t₁}
  elim⊥-A[0⊕B]⇔l : {t₁ t₂ : U} →
     (id⟷ {t₁} ⊗ unite₊l {t₂}) ⇔
     (distl ◎ (absorbl ⊕ id⟷)) ◎ unite₊l
  elim⊥-A[0⊕B]⇔r : {t₁ t₂ : U} →
     (distl ◎ (absorbl ⊕ id⟷)) ◎ unite₊l ⇔ (id⟷ {t₁} ⊗ unite₊l {t₂})
  elim⊥-1[A⊕B]⇔l : {t₁ t₂ : U} →
    unite⋆l ⇔
    distl ◎ (unite⋆l {t₁} ⊕ unite⋆l {t₂})
  elim⊥-1[A⊕B]⇔r : {t₁ t₂ : U} →
    distl ◎ (unite⋆l {t₁} ⊕ unite⋆l {t₂}) ⇔ unite⋆l
  fully-distribute⇔l : {t₁ t₂ t₃ t₄ : U} →
    (distl ◎ (dist {t₁} {t₂} {t₃} ⊕ dist {t₁} {t₂} {t₄})) ◎ assocl₊ ⇔
      ((((dist ◎ (distl ⊕ distl)) ◎ assocl₊) ◎ (assocr₊ ⊕ id⟷)) ◎
         ((id⟷ ⊕ swap₊) ⊕ id⟷)) ◎ (assocl₊ ⊕ id⟷)
  fully-distribute⇔r : {t₁ t₂ t₃ t₄ : U} →
    ((((dist ◎ (distl ⊕ distl)) ◎ assocl₊) ◎ (assocr₊ ⊕ id⟷)) ◎
       ((id⟷ ⊕ swap₊) ⊕ id⟷)) ◎ (assocl₊ ⊕ id⟷) ⇔
    (distl ◎ (dist {t₁} {t₂} {t₃} ⊕ dist {t₁} {t₂} {t₄})) ◎ assocl₊

-- At the next level we have a trivial equivalence that equates all
-- 2-morphisms of the same type.

triv≡ : {t₁ t₂ : U} {f g : t₁ ⟷ t₂} → (α β : f ⇔ g) → Set
triv≡ _ _ = ⊤

triv≡Equiv : {t₁ t₂ : U} {f₁ f₂ : t₁ ⟷ t₂} →
             IsEquivalence (triv≡ {t₁} {t₂} {f₁} {f₂})
triv≡Equiv = record
  { refl = tt
  ; sym = λ _ → tt
  ; trans = λ _ _ → tt
  }

------------------------------------------------------------------------------
-- Inverses for 2paths

2! : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} → (c₁ ⇔ c₂) → (c₂ ⇔ c₁)
2! assoc◎l = assoc◎r
2! assoc◎r = assoc◎l
2! assocl⊕l = assocl⊕r
2! assocl⊕r = assocl⊕l
2! assocl⊗l = assocl⊗r
2! assocl⊗r = assocl⊗l
2! assocr⊕r = assocr⊕l
2! assocr⊕l = assocr⊕r
2! assocr⊗r = assocr⊗l
2! assocr⊗l = assocr⊗r
2! dist⇔l = dist⇔r
2! dist⇔r = dist⇔l
2! distl⇔l = distl⇔r
2! distl⇔r = distl⇔l
2! factor⇔l = factor⇔r
2! factor⇔r = factor⇔l
2! factorl⇔l = factorl⇔r
2! factorl⇔r = factorl⇔l
2! idl◎l = idl◎r
2! idl◎r = idl◎l
2! idr◎l = idr◎r
2! idr◎r = idr◎l
2! linv◎l = linv◎r
2! linv◎r = linv◎l
2! rinv◎l = rinv◎r
2! rinv◎r = rinv◎l
2! unite₊l⇔l = unite₊l⇔r
2! unite₊l⇔r = unite₊l⇔l
2! uniti₊l⇔l = uniti₊l⇔r
2! uniti₊l⇔r = uniti₊l⇔l
2! unite₊r⇔l = unite₊r⇔r
2! unite₊r⇔r = unite₊r⇔l
2! uniti₊r⇔l = uniti₊r⇔r
2! uniti₊r⇔r = uniti₊r⇔l
2! swapl₊⇔ = swapr₊⇔
2! swapr₊⇔ = swapl₊⇔
2! unitel⋆⇔l = uniter⋆⇔l
2! uniter⋆⇔l = unitel⋆⇔l
2! unitil⋆⇔l = unitir⋆⇔l
2! unitir⋆⇔l = unitil⋆⇔l
2! unitel⋆⇔r = uniter⋆⇔r
2! uniter⋆⇔r = unitel⋆⇔r
2! unitil⋆⇔r = unitir⋆⇔r
2! unitir⋆⇔r = unitil⋆⇔r
2! swapl⋆⇔ = swapr⋆⇔
2! swapr⋆⇔ = swapl⋆⇔
2! id⇔ = id⇔
2! (α ⊡ β) = (2! α) ⊡ (2! β)
2! (trans⇔ α β) = trans⇔ (2! β) (2! α)
2! (resp⊕⇔ α β) = resp⊕⇔ (2! α) (2! β)
2! (resp⊗⇔ α β) = resp⊗⇔ (2! α) (2! β)
2! id⟷⊕id⟷⇔ = split⊕-id⟷
2! split⊕-id⟷ = id⟷⊕id⟷⇔
2! hom⊕◎⇔ = hom◎⊕⇔
2! hom◎⊕⇔ = hom⊕◎⇔
2! id⟷⊗id⟷⇔ = split⊗-id⟷
2! split⊗-id⟷ = id⟷⊗id⟷⇔
2! hom⊗◎⇔ = hom◎⊗⇔
2! hom◎⊗⇔ = hom⊗◎⇔
2! triangle⊕l = triangle⊕r
2! triangle⊕r = triangle⊕l
2! triangle⊗l = triangle⊗r
2! triangle⊗r = triangle⊗l
2! pentagon⊕l = pentagon⊕r
2! pentagon⊕r = pentagon⊕l
2! pentagon⊗l = pentagon⊗r
2! pentagon⊗r = pentagon⊗l
2! unite₊l-coh-l = unite₊l-coh-r
2! unite₊l-coh-r = unite₊l-coh-l
2! unite⋆l-coh-l = unite⋆l-coh-r
2! unite⋆l-coh-r = unite⋆l-coh-l
2! hexagonr⊕l = hexagonr⊕r
2! hexagonr⊕r = hexagonr⊕l
2! hexagonl⊕l = hexagonl⊕r
2! hexagonl⊕r = hexagonl⊕l
2! hexagonr⊗l = hexagonr⊗r
2! hexagonr⊗r = hexagonr⊗l
2! hexagonl⊗l = hexagonl⊗r
2! hexagonl⊗r = hexagonl⊗l
2! absorbl⇔l = absorbl⇔r
2! absorbl⇔r = absorbl⇔l
2! absorbr⇔l = absorbr⇔r
2! absorbr⇔r = absorbr⇔l
2! factorzl⇔l = factorzl⇔r
2! factorzl⇔r = factorzl⇔l
2! factorzr⇔l = factorzr⇔r
2! factorzr⇔r = factorzr⇔l
2! swap₊distl⇔l = swap₊distl⇔r
2! swap₊distl⇔r = swap₊distl⇔l
2! dist-swap⋆⇔l = dist-swap⋆⇔r
2! dist-swap⋆⇔r = dist-swap⋆⇔l
2! assocl₊-dist-dist⇔l = assocl₊-dist-dist⇔r
2! assocl₊-dist-dist⇔r = assocl₊-dist-dist⇔l
2! assocl⋆-distl⇔l = assocl⋆-distl⇔r
2! assocl⋆-distl⇔r = assocl⋆-distl⇔l
2! absorbr0-absorbl0⇔ = absorbl0-absorbr0⇔
2! absorbl0-absorbr0⇔ = absorbr0-absorbl0⇔
2! absorbr⇔distl-absorb-unite = distl-absorb-unite⇔absorbr
2! distl-absorb-unite⇔absorbr = absorbr⇔distl-absorb-unite
2! unite⋆r0-absorbr1⇔ = absorbr1-unite⋆r-⇔
2! absorbr1-unite⋆r-⇔ = unite⋆r0-absorbr1⇔
2! absorbl≡swap⋆◎absorbr = swap⋆◎absorbr≡absorbl
2! swap⋆◎absorbr≡absorbl = absorbl≡swap⋆◎absorbr
2! absorbr⇔[assocl⋆◎[absorbr⊗id⟷]]◎absorbr =
    [assocl⋆◎[absorbr⊗id⟷]]◎absorbr⇔absorbr
2!  [assocl⋆◎[absorbr⊗id⟷]]◎absorbr⇔absorbr =
    absorbr⇔[assocl⋆◎[absorbr⊗id⟷]]◎absorbr
2! [id⟷⊗absorbr]◎absorbl⇔assocl⋆◎[absorbl⊗id⟷]◎absorbr =
    assocl⋆◎[absorbl⊗id⟷]◎absorbr⇔[id⟷⊗absorbr]◎absorbl
2! assocl⋆◎[absorbl⊗id⟷]◎absorbr⇔[id⟷⊗absorbr]◎absorbl =
    [id⟷⊗absorbr]◎absorbl⇔assocl⋆◎[absorbl⊗id⟷]◎absorbr
2! elim⊥-A[0⊕B]⇔l = elim⊥-A[0⊕B]⇔r
2! elim⊥-A[0⊕B]⇔r = elim⊥-A[0⊕B]⇔l
2! elim⊥-1[A⊕B]⇔l = elim⊥-1[A⊕B]⇔r
2! elim⊥-1[A⊕B]⇔r = elim⊥-1[A⊕B]⇔l
2! fully-distribute⇔l = fully-distribute⇔r
2! fully-distribute⇔r = fully-distribute⇔l

2!! : {t₁ t₂ : U} {f g : t₁ ⟷ t₂} {α : f ⇔ g} → triv≡ (2! (2! α)) α
2!! = tt

-- This makes _⇔_ an equivalence relation...

⇔Equiv : {t₁ t₂ : U} → IsEquivalence (_⇔_ {t₁} {t₂})
⇔Equiv = record
  { refl = id⇔
  ; sym = 2!
  ; trans = trans⇔
  }

------------------------------------------------------------------------------

-- Unit coherence has two versions, but one is derivable
-- from the other.  As it turns out, one of our examples
-- needs the 'flipped' version.

unite₊r-coh-r : {t₁ : U} → swap₊ ◎ unite₊l ⇔ unite₊r {t₁}
unite₊r-coh-r =
  trans⇔ (id⇔ ⊡ unite₊l-coh-l) (
  trans⇔ assoc◎l ((
  trans⇔ (linv◎l ⊡ id⇔) idl◎l ) ) )

------------------------------------------------------------------------------

-- It is often useful to have that reversing c twice is ⇔ c rather than ≡
-- Unfortunately, it needs a 'proof', which is quite dull, though
-- it does have 3 non-trivial cases.
!!⇔id : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (! (! c)) ⇔ c
!!⇔id {c = unite₊l} = id⇔
!!⇔id {c = uniti₊l} = id⇔
!!⇔id {c = unite₊r} = id⇔
!!⇔id {c = uniti₊r} = id⇔
!!⇔id {c = swap₊} = id⇔
!!⇔id {c = assocl₊} = id⇔
!!⇔id {c = assocr₊} = id⇔
!!⇔id {c = unite⋆l} = id⇔
!!⇔id {c = uniti⋆l} = id⇔
!!⇔id {c = unite⋆r} = id⇔
!!⇔id {c = uniti⋆r} = id⇔
!!⇔id {c = swap⋆} = id⇔
!!⇔id {c = assocl⋆} = id⇔
!!⇔id {c = assocr⋆} = id⇔
!!⇔id {c = absorbr} = id⇔
!!⇔id {c = absorbl} = id⇔
!!⇔id {c = factorzr} = id⇔
!!⇔id {c = factorzl} = id⇔
!!⇔id {c = dist} = id⇔
!!⇔id {c = factor} = id⇔
!!⇔id {c = distl} = id⇔
!!⇔id {c = factorl} = id⇔
!!⇔id {c = id⟷} = id⇔
!!⇔id {c = c ◎ c₁} = !!⇔id ⊡ !!⇔id
!!⇔id {c = c ⊕ c₁} = resp⊕⇔ !!⇔id !!⇔id
!!⇔id {c = c ⊗ c₁} = resp⊗⇔ !!⇔id !!⇔id

-------------
mutual
  eval₁ : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} (ce : c₁ ⇔ c₂) → (t₁ ⟷ t₂)
  eval₁ (assoc◎l {c₁ = c₁} {c₂} {c₃}) = (c₁ ◎ c₂) ◎ c₃
  eval₁ (assoc◎r {c₁ = c₁} {c₂} {c₃}) = c₁ ◎ (c₂ ◎ c₃)
  eval₁ (assocl⊕l {c₁ = c₁} {c₂} {c₃}) = assocl₊ ◎ ((c₁ ⊕ c₂) ⊕ c₃)
  eval₁ (assocl⊕r {c₁ = c₁} {c₂} {c₃}) = (c₁ ⊕ (c₂ ⊕ c₃)) ◎ assocl₊
  eval₁ (assocl⊗l {c₁ = c₁} {c₂} {c₃}) = assocl⋆ ◎ ((c₁ ⊗ c₂) ⊗ c₃)
  eval₁ (assocl⊗r {c₁ = c₁} {c₂} {c₃}) = (c₁ ⊗ (c₂ ⊗ c₃)) ◎ assocl⋆
  eval₁ (assocr⊕r {c₁ = c₁} {c₂} {c₃}) = assocr₊ ◎ (c₁ ⊕ (c₂ ⊕ c₃))
  eval₁ (assocr⊗l {c₁ = c₁} {c₂} {c₃}) = ((c₁ ⊗ c₂) ⊗ c₃) ◎ assocr⋆
  eval₁ (assocr⊗r {c₁ = c₁} {c₂} {c₃}) = assocr⋆ ◎(c₁ ⊗ (c₂ ⊗ c₃))
  eval₁ (assocr⊕l {c₁ = c₁} {c₂} {c₃}) = ((c₁ ⊕ c₂) ⊕ c₃) ◎ assocr₊
  eval₁ (dist⇔l {a = c₁} {c₂} {c₃}) = dist ◎ ((c₁ ⊗ c₃) ⊕ (c₂ ⊗ c₃))
  eval₁ (dist⇔r {a = c₁} {c₂} {c₃}) = ((c₁ ⊕ c₂) ⊗ c₃) ◎ dist
  eval₁ (distl⇔l {a = c₁} {c₂} {c₃}) = distl ◎ ((c₁ ⊗ c₂) ⊕ (c₁ ⊗ c₃))
  eval₁ (distl⇔r {a = c₁} {c₂} {c₃}) = (c₁ ⊗ (c₂ ⊕ c₃)) ◎ distl
  eval₁ (factor⇔l {a = c₁} {c₂} {c₃}) = factor ◎ ((c₁ ⊕ c₂) ⊗ c₃)
  eval₁ (factor⇔r {a = c₁} {c₂} {c₃}) = ((c₁ ⊗ c₃) ⊕ (c₂ ⊗ c₃)) ◎ factor
  eval₁ (factorl⇔l {a = c₁} {c₂} {c₃}) = factorl ◎ (c₁ ⊗ (c₂ ⊕ c₃))
  eval₁ (factorl⇔r {a = c₁} {c₂} {c₃}) = ((c₁ ⊗ c₂) ⊕ (c₁ ⊗ c₃)) ◎ factorl
  eval₁ (idl◎l {c = c}) = c
  eval₁ (idl◎r {c = c}) = id⟷ ◎ c
  eval₁ (idr◎l {c = c}) = c
  eval₁ (idr◎r {c = c}) = c ◎ id⟷
  eval₁ (linv◎l {c = c}) = id⟷
  eval₁ (linv◎r {c = c}) = c ◎ ! c
  eval₁ (rinv◎l {c = c}) = id⟷
  eval₁ (rinv◎r {c = c}) = ! c ◎ c
  eval₁ (unite₊l⇔l {c₁ = c₁} {c₂}) = (c₁ ⊕ c₂) ◎ unite₊l
  eval₁ (unite₊l⇔r {c₁ = c₁} {c₂}) = unite₊l ◎ c₂
  eval₁ (uniti₊l⇔l {c₁ = c₁} {c₂}) = c₂ ◎ uniti₊l
  eval₁ (uniti₊l⇔r {c₁ = c₁} {c₂}) = uniti₊l ◎ (c₁ ⊕ c₂)
  eval₁ (unite₊r⇔l {c₁ = c₁} {c₂}) = (c₂ ⊕ c₁) ◎ unite₊r
  eval₁ (unite₊r⇔r {c₁ = c₁} {c₂}) = unite₊r ◎ c₂
  eval₁ (uniti₊r⇔l {c₁ = c₁} {c₂}) = c₂ ◎ uniti₊r
  eval₁ (uniti₊r⇔r {c₁ = c₁} {c₂}) = uniti₊r ◎ (c₂ ⊕ c₁)
  eval₁ (swapl₊⇔  {c₁ = c₁} {c₂}) = (c₂ ⊕ c₁) ◎ swap₊
  eval₁ (swapr₊⇔  {c₁ = c₁} {c₂}) = swap₊ ◎ (c₁ ⊕ c₂)
  eval₁ (unitel⋆⇔l {c₁ = c₁} {c₂}) = (c₁ ⊗ c₂) ◎ unite⋆l
  eval₁ (uniter⋆⇔l {c₁ = c₁} {c₂}) = unite⋆l ◎ c₂
  eval₁ (unitil⋆⇔l {c₁ = c₁} {c₂}) = c₂ ◎ uniti⋆l
  eval₁ (unitir⋆⇔l {c₁ = c₁} {c₂}) = uniti⋆l ◎ (c₁ ⊗ c₂)
  eval₁ (unitel⋆⇔r {c₁ = c₁} {c₂}) = (c₂ ⊗ c₁) ◎ unite⋆r
  eval₁ (uniter⋆⇔r {c₁ = c₁} {c₂}) = unite⋆r ◎ c₂
  eval₁ (unitil⋆⇔r {c₁ = c₁} {c₂}) = c₂ ◎ uniti⋆r
  eval₁ (unitir⋆⇔r {c₁ = c₁} {c₂}) = uniti⋆r ◎ (c₂ ⊗ c₁)
  eval₁ (swapl⋆⇔ {c₁ = c₁} {c₂}) = (c₂ ⊗ c₁) ◎ swap⋆
  eval₁ (swapr⋆⇔ {c₁ = c₁} {c₂}) = swap⋆ ◎ (c₁ ⊗ c₂)
  eval₁ (id⇔ {c = c}) = c
  eval₁ (trans⇔ {t₁} {t₂} {c₁} {c₂} {c₃} ce ce₁) with eval₁ ce | exact ce
  ... | cc | refl =  eval₁ {c₁ = cc} {c₃} ce₁
  eval₁ (_⊡_ {c₁ = c₁} {c₂} {c₃} {c₄} ce₀ ce₁) =
    let r₀ = eval₁ ce₀ in
    let r₁ = eval₁ ce₁ in
    r₀ ◎ r₁
  eval₁ (resp⊕⇔ ce₀ ce₁) =
    let r₀ = eval₁ ce₀ in
    let r₁ = eval₁ ce₁ in
    r₀ ⊕ r₁
  eval₁ (resp⊗⇔ ce₀ ce₁) =
    let r₀ = eval₁ ce₀ in
    let r₁ = eval₁ ce₁ in
    r₀ ⊗ r₁
  eval₁ id⟷⊕id⟷⇔ = id⟷
  eval₁ split⊕-id⟷ = id⟷ ⊕ id⟷
  eval₁ (hom⊕◎⇔ {c₁ = c₁} {c₂} {c₃} {c₄}) = (c₁ ⊕ c₂) ◎ (c₃ ⊕ c₄)
  eval₁ (hom◎⊕⇔ {c₁ = c₁} {c₂} {c₃} {c₄}) = (c₁ ◎ c₃) ⊕ (c₂ ◎ c₄)
  eval₁ id⟷⊗id⟷⇔ = id⟷
  eval₁ split⊗-id⟷ = id⟷ ⊗ id⟷
  eval₁ (hom⊗◎⇔ {c₁ = c₁} {c₂} {c₃} {c₄}) = (c₁ ⊗ c₂) ◎ (c₃ ⊗ c₄)
  eval₁ (hom◎⊗⇔ {c₁ = c₁} {c₂} {c₃} {c₄}) = (c₁ ◎ c₃) ⊗ (c₂ ◎ c₄)
  eval₁ triangle⊕l = assocr₊ ◎ (id⟷ ⊕ unite₊l)
  eval₁ triangle⊕r = unite₊r ⊕ id⟷
  eval₁ triangle⊗l = assocr⋆ ◎ (id⟷ ⊗ unite⋆l)
  eval₁ triangle⊗r = unite⋆r ⊗ id⟷
  eval₁ pentagon⊕l = ((assocr₊ ⊕ id⟷) ◎ assocr₊) ◎ (id⟷ ⊕ assocr₊)
  eval₁ pentagon⊕r = assocr₊ ◎ assocr₊
  eval₁ pentagon⊗l = ((assocr⋆ ⊗ id⟷) ◎ assocr⋆) ◎ (id⟷ ⊗ assocr⋆)
  eval₁ pentagon⊗r = assocr⋆ ◎ assocr⋆
  eval₁ unite₊l-coh-l = swap₊ ◎ unite₊r
  eval₁ unite₊l-coh-r = unite₊l
  eval₁ unite⋆l-coh-l = swap⋆ ◎ unite⋆r
  eval₁ unite⋆l-coh-r = unite⋆l
  eval₁ hexagonr⊕l = ((swap₊ ⊕ id⟷) ◎ assocr₊) ◎ (id⟷ ⊕ swap₊)
  eval₁ hexagonr⊕r = (assocr₊ ◎ swap₊) ◎ assocr₊
  eval₁ hexagonl⊕l = ((id⟷ ⊕ swap₊) ◎ assocl₊) ◎ (swap₊ ⊕ id⟷)
  eval₁ hexagonl⊕r = (assocl₊ ◎ swap₊) ◎ assocl₊
  eval₁ hexagonr⊗l = ((swap⋆ ⊗ id⟷) ◎ assocr⋆) ◎ (id⟷ ⊗ swap⋆)
  eval₁ hexagonr⊗r = (assocr⋆ ◎ swap⋆) ◎ assocr⋆
  eval₁ hexagonl⊗l = ((id⟷ ⊗ swap⋆) ◎ assocl⋆) ◎ (swap⋆ ⊗ id⟷)
  eval₁ hexagonl⊗r = (assocl⋆ ◎ swap⋆) ◎ assocl⋆
  eval₁ absorbl⇔l = absorbl ◎ id⟷
  eval₁ (absorbl⇔r {c₁ = c₁}) = (c₁ ⊗ id⟷) ◎ absorbl
  eval₁ absorbr⇔l = absorbr ◎ id⟷
  eval₁ (absorbr⇔r {c₁ = c₁}) = (id⟷ ⊗ c₁) ◎ absorbr
  eval₁ (factorzl⇔l {c₁ = c₁}) = factorzl ◎ (id⟷ ⊗ c₁)
  eval₁ (factorzl⇔r {c₁ = c₁}) = id⟷ ◎ factorzl
  eval₁ (factorzr⇔l {c₁ = c₁}) = factorzr ◎ (c₁ ⊗ id⟷)
  eval₁ (factorzr⇔r {c₁ = c₁}) = id⟷ ◎ factorzr
  eval₁ swap₊distl⇔l = distl ◎ swap₊
  eval₁ swap₊distl⇔r = (id⟷ ⊗ swap₊) ◎ distl
  eval₁ dist-swap⋆⇔l = swap⋆ ◎ distl
  eval₁ dist-swap⋆⇔r = dist ◎ (swap⋆ ⊕ swap⋆)
  eval₁ assocl₊-dist-dist⇔l = (dist ◎ (id⟷ ⊕ dist)) ◎ assocl₊
  eval₁ assocl₊-dist-dist⇔r = ((assocl₊ ⊗ id⟷) ◎ dist) ◎ (dist ⊕ id⟷)
  eval₁ assocl⋆-distl⇔l = ((id⟷ ⊗ distl) ◎ distl) ◎ (assocl⋆ ⊕ assocl⋆)
  eval₁ assocl⋆-distl⇔r = assocl⋆ ◎ distl
  eval₁ absorbr0-absorbl0⇔ = absorbl
  eval₁ absorbl0-absorbr0⇔ = absorbr
  eval₁ absorbr⇔distl-absorb-unite = (distl ◎ (absorbr ⊕ absorbr)) ◎ unite₊l
  eval₁ distl-absorb-unite⇔absorbr = absorbr
  eval₁ unite⋆r0-absorbr1⇔ = absorbr
  eval₁ absorbr1-unite⋆r-⇔ = unite⋆r
  eval₁ absorbl≡swap⋆◎absorbr = swap⋆ ◎ absorbr
  eval₁ swap⋆◎absorbr≡absorbl = absorbl
  eval₁ absorbr⇔[assocl⋆◎[absorbr⊗id⟷]]◎absorbr = (assocl⋆ ◎ (absorbr ⊗ id⟷)) ◎ absorbr
  eval₁ [assocl⋆◎[absorbr⊗id⟷]]◎absorbr⇔absorbr = absorbr
  eval₁ [id⟷⊗absorbr]◎absorbl⇔assocl⋆◎[absorbl⊗id⟷]◎absorbr = (assocl⋆ ◎ (absorbl ⊗ id⟷)) ◎ absorbr
  eval₁ assocl⋆◎[absorbl⊗id⟷]◎absorbr⇔[id⟷⊗absorbr]◎absorbl = (id⟷ ⊗ absorbr) ◎ absorbl
  eval₁ elim⊥-A[0⊕B]⇔l = (distl ◎ (absorbl ⊕ id⟷)) ◎ unite₊l
  eval₁ elim⊥-A[0⊕B]⇔r = id⟷ ⊗ unite₊l
  eval₁ elim⊥-1[A⊕B]⇔l = distl ◎ (unite⋆l ⊕ unite⋆l)
  eval₁ elim⊥-1[A⊕B]⇔r = unite⋆l
  eval₁ fully-distribute⇔l = ((((dist ◎ (distl ⊕ distl)) ◎ assocl₊) ◎ (assocr₊ ⊕ id⟷)) ◎
                                ((id⟷ ⊕ swap₊) ⊕ id⟷))
                               ◎ (assocl₊ ⊕ id⟷)
  eval₁ fully-distribute⇔r = (distl ◎ (dist ⊕ dist)) ◎ assocl₊

  exact : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} (ce : c₁ ⇔ c₂) → eval₁ ce ≡ c₂
  exact assoc◎l = refl
  exact assoc◎r = refl
  exact assocl⊕l = refl
  exact assocl⊕r = refl
  exact assocl⊗l = refl
  exact assocl⊗r = refl
  exact assocr⊕r = refl
  exact assocr⊗l = refl
  exact assocr⊗r = refl
  exact assocr⊕l = refl
  exact dist⇔l = refl
  exact dist⇔r = refl
  exact distl⇔l = refl
  exact distl⇔r = refl
  exact factor⇔l = refl
  exact factor⇔r = refl
  exact factorl⇔l = refl
  exact factorl⇔r = refl
  exact idl◎l = refl
  exact idl◎r = refl
  exact idr◎l = refl
  exact idr◎r = refl
  exact linv◎l = refl
  exact linv◎r = refl
  exact rinv◎l = refl
  exact rinv◎r = refl
  exact unite₊l⇔l = refl
  exact unite₊l⇔r = refl
  exact uniti₊l⇔l = refl
  exact uniti₊l⇔r = refl
  exact unite₊r⇔l = refl
  exact unite₊r⇔r = refl
  exact uniti₊r⇔l = refl
  exact uniti₊r⇔r = refl
  exact swapl₊⇔ = refl
  exact swapr₊⇔ = refl
  exact unitel⋆⇔l = refl
  exact uniter⋆⇔l = refl
  exact unitil⋆⇔l = refl
  exact unitir⋆⇔l = refl
  exact unitel⋆⇔r = refl
  exact uniter⋆⇔r = refl
  exact unitil⋆⇔r = refl
  exact unitir⋆⇔r = refl
  exact swapl⋆⇔ = refl
  exact swapr⋆⇔ = refl
  exact id⇔ = refl
  exact (trans⇔ ce ce₁) rewrite exact ce | exact ce₁ = refl
  exact (ce ⊡ ce₁) rewrite exact ce | exact ce₁ = refl
  exact (resp⊕⇔ ce ce₁) rewrite exact ce | exact ce₁ = refl
  exact (resp⊗⇔ ce ce₁) rewrite exact ce | exact ce₁ = refl
  exact id⟷⊕id⟷⇔ = refl
  exact split⊕-id⟷ = refl
  exact hom⊕◎⇔ = refl
  exact hom◎⊕⇔ = refl
  exact id⟷⊗id⟷⇔ = refl
  exact split⊗-id⟷ = refl
  exact hom⊗◎⇔ = refl
  exact hom◎⊗⇔ = refl
  exact triangle⊕l = refl
  exact triangle⊕r = refl
  exact triangle⊗l = refl
  exact triangle⊗r = refl
  exact pentagon⊕l = refl
  exact pentagon⊕r = refl
  exact pentagon⊗l = refl
  exact pentagon⊗r = refl
  exact unite₊l-coh-l = refl
  exact unite₊l-coh-r = refl
  exact unite⋆l-coh-l = refl
  exact unite⋆l-coh-r = refl
  exact hexagonr⊕l = refl
  exact hexagonr⊕r = refl
  exact hexagonl⊕l = refl
  exact hexagonl⊕r = refl
  exact hexagonr⊗l = refl
  exact hexagonr⊗r = refl
  exact hexagonl⊗l = refl
  exact hexagonl⊗r = refl
  exact absorbl⇔l = refl
  exact absorbl⇔r = refl
  exact absorbr⇔l = refl
  exact absorbr⇔r = refl
  exact factorzl⇔l = refl
  exact factorzl⇔r = refl
  exact factorzr⇔l = refl
  exact factorzr⇔r = refl
  exact swap₊distl⇔l = refl
  exact swap₊distl⇔r = refl
  exact dist-swap⋆⇔l = refl
  exact dist-swap⋆⇔r = refl
  exact assocl₊-dist-dist⇔l = refl
  exact assocl₊-dist-dist⇔r = refl
  exact assocl⋆-distl⇔l = refl
  exact assocl⋆-distl⇔r = refl
  exact absorbr0-absorbl0⇔ = refl
  exact absorbl0-absorbr0⇔ = refl
  exact absorbr⇔distl-absorb-unite = refl
  exact distl-absorb-unite⇔absorbr = refl
  exact unite⋆r0-absorbr1⇔ = refl
  exact absorbr1-unite⋆r-⇔ = refl
  exact absorbl≡swap⋆◎absorbr = refl
  exact swap⋆◎absorbr≡absorbl = refl
  exact absorbr⇔[assocl⋆◎[absorbr⊗id⟷]]◎absorbr = refl
  exact [assocl⋆◎[absorbr⊗id⟷]]◎absorbr⇔absorbr = refl
  exact [id⟷⊗absorbr]◎absorbl⇔assocl⋆◎[absorbl⊗id⟷]◎absorbr = refl
  exact assocl⋆◎[absorbl⊗id⟷]◎absorbr⇔[id⟷⊗absorbr]◎absorbl = refl
  exact elim⊥-A[0⊕B]⇔l = refl
  exact elim⊥-A[0⊕B]⇔r = refl
  exact elim⊥-1[A⊕B]⇔l = refl
  exact elim⊥-1[A⊕B]⇔r = refl
  exact fully-distribute⇔l = refl
  exact fully-distribute⇔r = refl

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

{- *** Definition 5.3 and Lemma 5.5 are taken from the library ***
   *** Corollary 6.8 is too trivial a consequence of -}

{- ConnectednessAlt and the last submodule of Connection are the
   only modules importing real truncation types from the library.
   Except for that, Univalence is the only additional assumption
   to Agda-style MLTT we work with. -}
module Universe.index where

{- General utility funcions and type constructors for
   the pseudo-universe of types of fixed truncation level. -}
import Universe.Utility.General
import Universe.Utility.TruncUniverse

{- Pointed types.
   Corresponds to section 4 plus some lemmata of section 5,
   which are used in multiple modules and thus belong here. -}
-- *** Definitions 4.1, 4.3, 4.5, 4.6 and Lemmata 4.5, 4.7, 5.1, 5.4 ***
import Universe.Utility.Pointed

{- Homotopically complicated types.
   Corresponds to section 5 sans the initial lemma.
   Concludes with the main theorem that the n-types
   in the n-th universe from a strict n-type.
   Hierarchy and Trunc.* are mutually independent. -}
{- *** Lemmata 5.2, 5.7, 5.8(*), Theorems 5.9, 5.11, and Corollary 5.6 ***
       (*) a slightly weaker version -}
import Universe.Hierarchy

{- Connectedness constructions
   Corresponds to section 6 and 7.
   The first three modules develop a framework of
   truncations internal to MLTT+Univalence without truncations.
   Connection contains the main result of section 6.
   ConnectednessAlt is independent from the first four modules
   and presents a provably equivalent definition of n-connectedness
   using only propositional truncation (as remarked in the article
   and mentioned in an exercise in the HoTT book). -}

--- *** Definition 6.2, Lemma 6.6
import Universe.Trunc.Universal

--- *** Definition 6.4, Lemma 6.7 ***
import Universe.Trunc.Basics

--- *** Lemmata 6.9, 6.10
import Universe.Trunc.TypeConstructors

--- *** Definitions 6.11, 6.13, Lemmata 6.12, 6.14, 6.15
import Universe.Trunc.Connection
import Universe.Trunc.ConnectednessAlt

ext: agda

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
module +-example where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
open import Naturals using (suc; _+_)

+-example : 3 + 4 ≡ 7
+-example =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc (suc (1 + 4))
  ≡⟨⟩
    suc (suc (suc (0 + 4)))
  ≡⟨⟩
    suc (suc (suc 4))
  ≡⟨⟩
    7
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors where all elements satisfy a given property
------------------------------------------------------------------------

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

module Data.Vec.Relation.Unary.All where

open import Data.Nat.Base using (zero; suc)
open import Data.Fin.Base using (Fin; zero; suc)
open import Data.Product as Prod using (_×_; _,_; uncurry; <_,_>)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Function using (_∘_)
open import Level using (Level; _⊔_)
open import Relation.Nullary hiding (Irrelevant)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary
open import Relation.Binary.PropositionalEquality as P using (subst)

private
  variable
    a b c p q r : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- All P xs means that all elements in xs satisfy P.

infixr 5 _∷_

data All {a} {A : Set a} (P : Pred A p) : ∀ {n} → Vec A n → Set (p ⊔ a) where
  []  : All P []
  _∷_ : ∀ {n x} {xs : Vec A n} (px : P x) (pxs : All P xs) → All P (x ∷ xs)

------------------------------------------------------------------------
-- Operations on All

module _ {P : Pred A p} where

  head : ∀ {n x} {xs : Vec A n} → All P (x ∷ xs) → P x
  head (px ∷ pxs) = px

  tail : ∀ {n x} {xs : Vec A n} → All P (x ∷ xs) → All P xs
  tail (px ∷ pxs) = pxs

  uncons : ∀ {n x} {xs : Vec A n} → All P (x ∷ xs) → P x × All P xs
  uncons = < head , tail >

  lookup : ∀ {n} {xs : Vec A n} (i : Fin n) →
           All P xs → P (Vec.lookup xs i)
  lookup zero    (px ∷ pxs) = px
  lookup (suc i) (px ∷ pxs) = lookup i pxs

  tabulate : ∀ {n xs} → (∀ i → P (Vec.lookup xs i)) → All P {n} xs
  tabulate {xs = []}    pxs = []
  tabulate {xs = _ ∷ _} pxs = pxs zero ∷ tabulate (pxs ∘ suc)

module _ {P : Pred A p} {Q : Pred A q} where

  map : ∀ {n} → P ⊆ Q → All P {n} ⊆ All Q {n}
  map g []         = []
  map g (px ∷ pxs) = g px ∷ map g pxs

  zip : ∀ {n} → All P ∩ All Q ⊆ All (P ∩ Q) {n}
  zip ([] , [])             = []
  zip (px ∷ pxs , qx ∷ qxs) = (px , qx) ∷ zip (pxs , qxs)

  unzip : ∀ {n} → All (P ∩ Q) {n} ⊆ All P ∩ All Q
  unzip []           = [] , []
  unzip (pqx ∷ pqxs) = Prod.zip _∷_ _∷_ pqx (unzip pqxs)

module _ {P : Pred A p} {Q : Pred B q} {R : Pred C r} where

  zipWith : ∀ {_⊕_ : A → B → C} →
            (∀ {x y} → P x → Q y → R (x ⊕ y)) →
            ∀ {n xs ys} → All P {n} xs → All Q {n} ys →
            All R {n} (Vec.zipWith _⊕_ xs ys)
  zipWith _⊕_ {xs = []}     {[]}     []         []         = []
  zipWith _⊕_ {xs = x ∷ xs} {y ∷ ys} (px ∷ pxs) (qy ∷ qys) =
    px ⊕ qy ∷ zipWith _⊕_ pxs qys

------------------------------------------------------------------------
-- Properties of predicates preserved by All

module _ {P : Pred A p} where

  all : ∀ {n} → Decidable P → Decidable (All P {n})
  all P? []       = yes []
  all P? (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×-dec all P? xs)

  universal : Universal P → ∀ {n} → Universal (All P {n})
  universal u []       = []
  universal u (x ∷ xs) = u x ∷ universal u xs

  irrelevant : Irrelevant P → ∀ {n} → Irrelevant (All P {n})
  irrelevant irr []           []           = P.refl
  irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
    P.cong₂ _∷_ (irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)

  satisfiable : Satisfiable P → ∀ {n} → Satisfiable (All P {n})
  satisfiable (x , p) {zero}  = [] , []
  satisfiable (x , p) {suc n} = Prod.map (x ∷_) (p ∷_) (satisfiable (x , p))


text:
-- Andreas, 2015-07-22  Fixed bug in test for empty type of sizes

{-# OPTIONS --copatterns #-}

open import Common.Size

record U (i : Size) : Set where
  coinductive
  field out : (j : Size< i) → U j
open U

fixU : {A : Size → Set} (let C = λ i → A i → U i)
  → ∀ i (f : ∀ i → (∀ (j : Size< i) → C j) → C i) → C i
out (fixU i f a) j = out (f i {!λ (j : Size< i) → fixU j f!} a) j

-- Giving should succeed (even if termination checking might not succeed yet)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/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
-}

module Dijkstra.Syntax where

open import Dijkstra.EitherD
open import Dijkstra.EitherLike
open import Dijkstra.RWS
open import Haskell.Prelude
open import Optics.All

{-
Within a "Dijkstra-fied" monad `M`, `if` and `ifD` are semantically interchangeable.

The difference is in how proof obligations are generated
- with the *D variants generating new weakestPre obligations for each case.

In some cases, this is helpful for structuring proofs, while in other cases it is
unnecessary and introduces more structure to the proof without adding any benefit.

A rule of thumb is that, if the "scrutinee" (whatever we are doing case analysis on,
i.e., the first argument) is the value provided via >>= (bind) by a previous code block,
then we already have a weakestPre proof obligation, so introducing additional ones via the
*D variants only creates more work and provides no additional benefit.
-}

record MonadIfD {ℓ₁ ℓ₂ ℓ₃ : Level} (M : Set ℓ₁ → Set ℓ₂) : Set (ℓ₂ ℓ⊔ ℓ+1 ℓ₁ ℓ⊔ ℓ+1 ℓ₃) where
  infix 1 ifD‖_
  field
    ⦃ monad ⦄ : Monad M
    ifD‖_ : ∀ {A : Set ℓ₁} → Guards{ℓ₂}{ℓ₃} (M A) → M A

open MonadIfD ⦃ ... ⦄ public

module _ {ℓ₁ ℓ₂ ℓ₃} {M : Set ℓ₁ → Set ℓ₂} where

  private
    variable
      A : Set ℓ₁
      B : Set ℓ₃

  infix 0 ifD_then_else_
  ifD_then_else_ : ⦃ _ : MonadIfD{ℓ₃ = ℓ₃} M ⦄ ⦃ _ : ToBool B ⦄ → B → (c₁ c₂ : M A) → M A
  ifD b then c₁ else c₂ =
    ifD‖ b ≔ c₁
       ‖ otherwise≔ c₂

whenD : ∀ {ℓ₂ ℓ₃} {M : Set → Set ℓ₂} {B : Set ℓ₃} ⦃ _ : MonadIfD{ℓ0}{ℓ₂}{ℓ₃} M ⦄ ⦃ _ : ToBool B ⦄ → B → M Unit → M Unit
whenD b f = ifD b then f else pure unit

module _ {ℓ₁ ℓ₂} {M : Set ℓ₁ → Set ℓ₂} where
  private
    variable A B : Set ℓ₁

  ifMD : ⦃ mi : MonadIfD{ℓ₃ = ℓ₁} M ⦄ ⦃ _ : ToBool B ⦄ → M B → (c₁ c₂ : M A) → M A
  ifMD{B = B} ⦃ mi ⦄ m c₁ c₂ = do
    x ← m
    ifD x then c₁ else c₂

record MonadMaybeD {ℓ₁ ℓ₂ : Level} (M : Set ℓ₁ → Set ℓ₂) : Set (ℓ₂ ℓ⊔ ℓ+1 ℓ₁) where
  field
    ⦃ monad ⦄ : Monad M
    maybeD : ∀ {A B : Set ℓ₁} → M B → (A → M B) → Maybe A → M B

open MonadMaybeD ⦃ ... ⦄ public

infix 0 caseMD_of_
caseMD_of_ : ∀ {ℓ₁ ℓ₂} {M : Set ℓ₁ → Set ℓ₂} ⦃ _ : MonadMaybeD M ⦄ {A B : Set ℓ₁} → Maybe A → (Maybe A → M B) → M B
caseMD m of f = maybeD (f nothing) (f ∘ just) m

record MonadEitherD {ℓ₁ ℓ₂ : Level} (M : Set ℓ₁ → Set ℓ₂) : Set (ℓ₂ ℓ⊔ ℓ+1 ℓ₁) where
  field
    ⦃ monad ⦄ : Monad M
    eitherD : ∀ {E A B : Set ℓ₁} → (E → M B) → (A → M B) → Either E A → M B

open MonadEitherD ⦃ ... ⦄ public hiding (eitherD)

eitherD
  : ∀ {ℓ₁ ℓ₂ ℓ₃} {M : Set ℓ₁ → Set ℓ₂} ⦃ med : MonadEitherD M ⦄ →
    ∀ {EL : Set ℓ₁ → Set ℓ₁ → Set ℓ₃} ⦃ _ : EitherLike EL ⦄ →
    ∀ {E A B : Set ℓ₁} → (E → M B) → (A → M B) → EL E A → M B
eitherD ⦃ med = med ⦄ f₁ f₂ e =
  MonadEitherD.eitherD med f₁ f₂ (toEither e)

infix 0 case⊎D_of_
case⊎D_of_
  : ∀ {ℓ₁ ℓ₂ ℓ₃} {M : Set ℓ₁ → Set ℓ₂} ⦃ _ : MonadEitherD M ⦄ →
    ∀ {EL : Set ℓ₁ → Set ℓ₁ → Set ℓ₃} ⦃ _ : EitherLike EL ⦄ →
    ∀ {E A B : Set ℓ₁} → EL E A → (EL E A → M B) → M B
case⊎D e of f = eitherD (f ∘ fromEither ∘ Left) (f ∘ fromEither ∘ Right) e


text:
open import Agda.Builtin.Nat

foo : Nat → Nat
foo x = bar x
  where
    bar : Nat → Nat
    bar y = {!x!}

-- WAS: Splitting on x produces the following garbage:
-- foo : Nat → Nat
-- foo x = bar x
--   where
--     bar : Nat → Nat
--     bar y = {!!}
--     bar y = {!!}

-- SHOULD: raise an error


text:
module Numeral.Natural.Relation.Divisibility.Proofs where

import Lvl
open import Data
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Logic.Predicate.Theorems
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Function
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Multiplication
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Classical
open import Numeral.Natural.Relation.Order.Proofs
open import Numeral.Natural.Relation.Order.Existence using ([≤]-equivalence)
open import Numeral.Natural.Relation.Order.Existence.Proofs using ()
open import Numeral.Natural.Relation.Divisibility
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Operator
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Structure.Relator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type
open import Type.Properties.MereProposition

{-
div-elim-test : ∀{ℓ ℓ₁}{A : Type{ℓ₁}}{f : A → ℕ}{g : ℕ → ℕ}{P : ∀{y x} → (f(y) ∣ x) → Type{ℓ}} → (∀{y} → P(Div𝟎{f y})) → (∀{y x}{p : f y ∣ g x} → P(p) → P(Div𝐒 p)) → (∀{y x}{p : f(y) ∣ g x} → P(p))
div-elim-test {f = f}{g = g}              z s {y}{x}{p = p} with g(x)
... | 𝟎 = {!p!}
... | 𝐒 a = {!p!}
-- div-elim-test               z s {p = Div𝟎}   = z
-- div-elim-test{f = f}{P = P} z s {p = Div𝐒 p} = s(div-elim-test{f = f}{P = P} z s {p = p})
-}

{-
Even-mereProposition : ∀{n} → MereProposition(Even(n))
Even-mereProposition = intro proof where
  proof : ∀{n}{p q : Even n} → (p ≡ q)
  proof {𝟎}       {Even0}   {Even0}   = [≡]-intro
  proof {𝐒(𝐒(n))} {Even𝐒 p} {Even𝐒 q} = [≡]-with(Even𝐒) (proof {n} {p} {q})

Odd-mereProposition : ∀{n} → MereProposition(Odd(n))
Odd-mereProposition = intro proof where
  proof : ∀{n}{p q : Odd n} → (p ≡ q)
  proof {𝐒(𝟎)}    {Odd0}   {Odd0}   = [≡]-intro
  proof {𝐒(𝐒(n))} {Odd𝐒 p} {Odd𝐒 q} = [≡]-with(Odd𝐒) (proof {n} {p} {q})
-}

{-

div-elim-test : ∀{f : ℕ → ℕ}{ℓ}{P : ∀{y x} → (f y ∣ x) → Type{ℓ}} → (∀{y} → P(Div𝟎{f y})) → (∀{y x}{p : f y ∣ x} → P(p) → P(Div𝐒 p)) → (∀{y x}{p : f y ∣ x} → P(p))
div-elim-test        z s {p = Div𝟎}   = z
div-elim-test{f = f}{P = P} z s {p = Div𝐒 p} = s(div-elim-test{f = f}{P = P} z s {p = p})

divides-mereProposition : ∀{d n} → MereProposition(𝐒(d) ∣ n)
divides-mereProposition = intro proof where
  proof : ∀{d n}{p q : (𝐒(d) ∣ n)} → (p ≡ q)
  proof {d} {.𝟎} {Div𝟎} {Div𝟎} = [≡]-intro
  proof {d} {.(𝐒 d + _)} {Div𝐒 p} {q} = {!div-elim-test{P = Div𝐒 p ≡_} ? ? {?}!}
  --proof{d}{n}{p}{q} = div-elim {P = \q → ∀{p} → (p ≡ q)} (\{y}{p} → {!div-elim {P = _≡ Div𝟎} ? ? {p = p}!}) {!!} {p = q}
  -- div-elim{P = {!!}} (div-elim {!!} {!!} {p = p}) (div-elim {!!} {!!} {p = p}) {p = q}

  {-
  test : ∀{y x} → (y ∣ x) → ∃{Obj = ℕ ⨯ ℕ}(Tuple.uncurry(_∣_))
  test {y}{.𝟎} Div𝟎     = [∃]-intro (y , 𝟎) ⦃ Div𝟎 ⦄
  test         (Div𝐒 p) = [∃]-intro _       ⦃ p ⦄
  -}
-}

DivN : ∀{y : ℕ} → (n : ℕ) → (y ∣ (y ⋅ n))
DivN {y}(𝟎)    = Div𝟎
DivN {y}(𝐒(n)) = Div𝐒(DivN{y}(n))

divides-quotient : ∀{x y} → (y ∣ x) → ℕ
divides-quotient = divides-elim 𝟎 𝐒

divides-quotient-correctness : ∀{x y}{yx : (y ∣ x)} → (y ⋅ (divides-quotient yx) ≡ x)
divides-quotient-correctness        {yx = Div𝟎}    = [≡]-intro
divides-quotient-correctness {_}{y} {yx = Div𝐒 yx} = congruence₂ᵣ(_+_)(y) (divides-quotient-correctness {yx = yx})

divides-[⋅]-existence : ∀{x y} → ∃(n ↦ y ⋅ n ≡ x) ↔ (y ∣ x)
divides-[⋅]-existence = [↔]-intro l r where
  l : ∀{x y} → (y ∣ x) → (∃(n ↦ y ⋅ n ≡ x))
  l yx = [∃]-intro (divides-quotient yx) ⦃ divides-quotient-correctness {yx = yx} ⦄

  r : ∀{x y} → (∃(n ↦ y ⋅ n ≡ x)) → (y ∣ x)
  r {x}{y} ([∃]-intro n ⦃ y⋅n≡x ⦄) = [≡]-substitutionᵣ y⋅n≡x {y ∣_} (DivN{y}(n))

divides-[⋅]-existence₊ : ∀{x y} → (y ∣ 𝐒(x)) → ∃(n ↦ y ⋅ 𝐒(n) ≡ 𝐒(x))
divides-[⋅]-existence₊ {x}{y} p with [↔]-to-[←] (divides-[⋅]-existence{𝐒(x)}{y}) p
... | [∃]-intro (𝐒(n)) = [∃]-intro n

instance
  divides-transitivity : Transitivity(_∣_)
  Transitivity.proof (divides-transitivity) {a}{b}{c} (a-div-b) (b-div-c) with ([↔]-to-[←] divides-[⋅]-existence a-div-b , [↔]-to-[←] divides-[⋅]-existence b-div-c)
  ... | (([∃]-intro (n₁) ⦃ a⋅n₁≡b ⦄),([∃]-intro (n₂) ⦃ b⋅n₂≡c ⦄)) =
    ([↔]-to-[→] divides-[⋅]-existence
      ([∃]-intro
        (n₁ ⋅ n₂)
        ⦃
          (symmetry(_≡_) (associativity(_⋅_) {a}{n₁}{n₂}))
          🝖 ([≡]-with(expr ↦ expr ⋅ n₂) (a⋅n₁≡b))
          🝖 (b⋅n₂≡c)
        ⦄
      )
    )

divides-with-[+] : ∀{a b c} → (a ∣ b) → (a ∣ c) → (a ∣ (b + c))
divides-with-[+] {a}{b}{c} (a-div-b) (a-div-c) with ([↔]-to-[←] divides-[⋅]-existence a-div-b , [↔]-to-[←] divides-[⋅]-existence a-div-c)
... | (([∃]-intro (n₁) ⦃ a⋅n₁≡b ⦄),([∃]-intro (n₂) ⦃ a⋅n₂≡c ⦄)) =
  ([↔]-to-[→] divides-[⋅]-existence
    ([∃]-intro
      (n₁ + n₂)
      ⦃
        (distributivityₗ(_⋅_)(_+_) {a}{n₁}{n₂})
        🝖 ([≡]-with-op(_+_)
          (a⋅n₁≡b)
          (a⋅n₂≡c)
        )
      ⦄
    )
  )

divides-with-[−₀] : ∀{a b c} → (a ∣ b) → (a ∣ c) → (a ∣ (b −₀ c))
divides-with-[−₀] {a}{b}{c} (a-div-b) (a-div-c) with ([↔]-to-[←] divides-[⋅]-existence a-div-b , [↔]-to-[←] divides-[⋅]-existence a-div-c)
... | (([∃]-intro (n₁) ⦃ a⋅n₁≡b ⦄),([∃]-intro (n₂) ⦃ a⋅n₂≡c ⦄)) =
  ([↔]-to-[→] divides-[⋅]-existence
    ([∃]-intro
      (n₁ −₀ n₂)
      ⦃
        (distributivityₗ(_⋅_)(_−₀_) {a}{n₁}{n₂})
        🝖 ([≡]-with-op(_−₀_)
          (a⋅n₁≡b)
          (a⋅n₂≡c)
        )
      ⦄
    )
  )

divides-without-[+] : ∀{a b c} → (a ∣ (b + c)) → ((a ∣ b) ↔ (a ∣ c))
divides-without-[+] {a}{b}{c} abc = [↔]-intro (l abc) (r abc) where
  l : ∀{a b c} → (a ∣ (b + c)) → (a ∣ b) ← (a ∣ c)
  l{a}{b}{c} abc ac = [≡]-substitutionᵣ ([−₀]ₗ[+]ᵣ-nullify{b}{c}) {expr ↦ (a ∣ expr)} (divides-with-[−₀] {a}{b + c}{c} abc ac)

  r : ∀{a b c} → (a ∣ (b + c)) → (a ∣ b) → (a ∣ c)
  r{a}{b}{c} abc ab = l {a}{c}{b} ([≡]-substitutionᵣ (commutativity(_+_) {b}{c}) {expr ↦ a ∣ expr} abc) ab

divides-with-[𝄩] : ∀{a b c} → (a ∣ b) → (a ∣ c) → (a ∣ (b 𝄩 c))
divides-with-[𝄩] {a} ab ac
 with [∃]-intro n₁ ⦃ p ⦄ ← [↔]-to-[←] divides-[⋅]-existence ab
 with [∃]-intro n₂ ⦃ q ⦄ ← [↔]-to-[←] divides-[⋅]-existence ac
 = [↔]-to-[→] divides-[⋅]-existence ([∃]-intro (n₁ 𝄩 n₂) ⦃ distributivityₗ(_⋅_)(_𝄩_) {a}{n₁}{n₂} 🝖 congruence₂(_𝄩_) p q ⦄)

-- instance
--   divides-with-fn : ∀{a b} → (a ∣ b) → ∀{f : ℕ → ℕ} → {_ : ∀{x y : ℕ} → ∃{ℕ → ℕ}(\g → f(x ⋅ y) ≡ f(x) ⋅ g(y))} → ((f(a)) ∣ (f(b)))
--   divides-with-fn {a}{b} (a-div-b) {f} ⦃ f-prop ⦄

instance
  [1]-divides : ∀{n} → (1 ∣ n)
  [1]-divides {𝟎}    = Div𝟎
  [1]-divides {𝐒(n)} =
    [≡]-substitutionₗ
      (commutativity(_+_) {n}{1})
      {expr ↦ (1 ∣ expr)}
      (Div𝐒([1]-divides{n}))

-- TODO: Rename these reflexivity proofs
instance
  divides-reflexivity : ∀{n} → (n ∣ n)
  divides-reflexivity = Div𝐒(Div𝟎)

instance
  divides-reflexivity-instance : Reflexivity(_∣_)
  divides-reflexivity-instance = intro divides-reflexivity

instance
  [0]-divides-[0] : (0 ∣ 0)
  [0]-divides-[0] = Div𝟎

[0]-only-divides-[0] : ∀{n} → (0 ∣ n) → (n ≡ 0)
[0]-only-divides-[0] {𝟎} _ = [≡]-intro
[0]-only-divides-[0] {𝐒(n)} proof with () ← [∃]-proof([↔]-to-[←] divides-[⋅]-existence proof)

[0]-divides-not : ∀{n} → ¬(0 ∣ 𝐒(n))
[0]-divides-not (0divSn) = [𝐒]-not-0([0]-only-divides-[0] 0divSn)

divides-not-[1] : ∀{n} → ¬((n + 2) ∣ 1)
divides-not-[1] ()

[1]-only-divides-[1] : ∀{n} → (n ∣ 1) → (n ≡ 1)
[1]-only-divides-[1] {𝟎}       ndiv1 = [⊥]-elim ([0]-divides-not ndiv1)
[1]-only-divides-[1] {𝐒(𝟎)}    ndiv1 = [≡]-intro
[1]-only-divides-[1] {𝐒(𝐒(n))} ()

divides-with-[⋅] : ∀{a b c} → ((a ∣ b) ∨ (a ∣ c)) → (a ∣ (b ⋅ c))
divides-with-[⋅] {a}{b}{c} = [∨]-elim (l{a}{b}{c}) (r{a}{b}{c}) where
  l : ∀{a b c} → (a ∣ b) → (a ∣ (b ⋅ c))
  l Div𝟎 = Div𝟎
  l {a}{a}{c} (Div𝐒 Div𝟎) = DivN{a} c
  l {a} {.(a + x)} {c} (Div𝐒 {.a} {x} ab@(Div𝐒 _)) = [≡]-substitutionₗ (distributivityᵣ(_⋅_)(_+_) {a}{x}{c}) {a ∣_} (divides-with-[+] (l {a}{a}{c} (Div𝐒 Div𝟎)) (l {a}{x}{c} ab))

  r : ∀{a b c} → (a ∣ c) → (a ∣ (b ⋅ c))
  r {a}{b}{c} ac = [≡]-substitutionᵣ (commutativity(_⋅_) {c}{b}) {a ∣_} (l {a}{c}{b} ac)

divides-upper-limit : ∀{a b} → (a ∣ 𝐒(b)) → (a ≤ 𝐒(b))
divides-upper-limit {𝟎}   {_} (proof) = [⊥]-elim ([0]-divides-not (proof))
divides-upper-limit {𝐒(a)}{b} (proof) = ([↔]-to-[→] [≤]-equivalence) (existence2) where
  existence1 : ∃(n ↦ 𝐒(a) + (𝐒(a) ⋅ n) ≡ 𝐒(b))
  existence1 = divides-[⋅]-existence₊(proof)

  existence2 : ∃(n ↦ 𝐒(a) + n ≡ 𝐒(b))
  existence2 = [∃]-intro(𝐒(a) ⋅ [∃]-witness(existence1)) ⦃ [∃]-proof(existence1) ⦄

divides-not-lower-limit : ∀{a b} → (a > 𝐒(b)) → (a ∤ 𝐒(b))
divides-not-lower-limit {a}{b} = (contrapositiveᵣ (divides-upper-limit {a}{b})) ∘ [>]-to-[≰]

Div𝐏 : ∀{x y : ℕ} → (y ∣ (y + x)) → (y ∣ x)
Div𝐏 {x}{y} proof = [↔]-to-[→] (divides-without-[+] {y}{y}{x} proof) (divides-reflexivity)

Div𝐏-monus : ∀{x y : ℕ} → (y ∣ x) → (y ∣ (x −₀ y))
Div𝐏-monus Div𝟎 = Div𝟎
Div𝐏-monus {.(y + x)}{y} (Div𝐒 {_}{x} yx) = [≡]-substitutionₗ ([−₀]ₗ[+]ₗ-nullify {y}{x}) {y ∣_} yx

divides-with-[⋅]ₗ-both : ∀{x y z} → (x ∣ y) → (z ⋅ x ∣ z ⋅ y)
divides-with-[⋅]ₗ-both {x} {.0}       {z} Div𝟎 = Div𝟎
divides-with-[⋅]ₗ-both {x} {.(x + _)} {z} (Div𝐒 {_}{y} xy) rewrite distributivityₗ(_⋅_)(_+_) {z}{x}{y} = Div𝐒 (divides-with-[⋅]ₗ-both {x}{y}{z} xy)

divides-with-[⋅]ᵣ-both : ∀{x y z} → (x ∣ y) → (x ⋅ z ∣ y ⋅ z)
divides-with-[⋅]ᵣ-both {x} {.0}       {z} Div𝟎 = Div𝟎
divides-with-[⋅]ᵣ-both {x} {.(x + _)} {z} (Div𝐒 {_}{y} xy) rewrite distributivityᵣ(_⋅_)(_+_) {x}{y}{z} = Div𝐒 (divides-with-[⋅]ᵣ-both {x}{y}{z} xy)

divides-with-[⋅]-both : ∀{x₁ y₁ x₂ y₂} → (x₁ ∣ y₁) → (x₂ ∣ y₂) → (x₁ ⋅ x₂ ∣ y₁ ⋅ y₂)
divides-with-[⋅]-both {x₁}{y₁}{x₂}{y₂} xy1 xy2
  with [∃]-intro n₁ ⦃ [≡]-intro ⦄ ← [↔]-to-[←] divides-[⋅]-existence xy1
  with [∃]-intro n₂ ⦃ [≡]-intro ⦄ ← [↔]-to-[←] divides-[⋅]-existence xy2
  = [↔]-to-[→] divides-[⋅]-existence ([∃]-intro (n₁ ⋅ n₂) ⦃ One.associate-commute4 {_▫_ = _⋅_} {a = x₁}{x₂}{n₁}{n₂} (commutativity(_⋅_) {x₂}{n₁}) ⦄)

divides-with-[^] : ∀{a b n} → (a ∣ b) → ((a ^ n) ∣ (b ^ n))
divides-with-[^] {n = 𝟎}   _  = Div𝐒 Div𝟎
divides-with-[^] {n = 𝐒 n} ab = divides-with-[⋅]-both ab (divides-with-[^] {n = n} ab)

divides-withᵣ-[^] : ∀{a b n} → ⦃ pos : Positive(n) ⦄ → (a ∣ b) → (a ∣ (b ^ n))
divides-withᵣ-[^] {a}{b}{𝐒 n} ab = divides-with-[⋅] {a}{b}{b ^ n} ([∨]-introₗ ab)

divides-without-[⋅]ᵣ-both : ∀{x y z} → (x ⋅ 𝐒(z) ∣ y ⋅ 𝐒(z)) → (x ∣ y)
divides-without-[⋅]ᵣ-both {x}{y}{z} p
  with [∃]-intro n ⦃ peq ⦄ ← [↔]-to-[←] divides-[⋅]-existence p
  = [↔]-to-[→] divides-[⋅]-existence ([∃]-intro n ⦃ [⋅]-cancellationᵣ{𝐒(z)} (symmetry(_≡_) (One.commuteᵣ-assocₗ{_▫_ = _⋅_}{x}{𝐒(z)}{n}) 🝖 peq) ⦄)

divides-without-[⋅]ₗ-both : ∀{x y z} → (𝐒(z) ⋅ x ∣ 𝐒(z) ⋅ y) → (x ∣ y)
divides-without-[⋅]ₗ-both {x}{y}{z} p = divides-without-[⋅]ᵣ-both {x}{y}{z} (substitute₂(_∣_) (commutativity(_⋅_) {𝐒(z)}{x}) (commutativity(_⋅_) {𝐒(z)}{y}) p)

divides-without-[⋅]ᵣ-both' : ∀{x y z} → (z > 0) → (x ⋅ z ∣ y ⋅ z) → (x ∣ y)
divides-without-[⋅]ᵣ-both' {x}{y}{𝐒(z)} _ = divides-without-[⋅]ᵣ-both {x}{y}{z}

divides-without-[⋅]ₗ-both' : ∀{x y z} → (z > 0) → (z ⋅ x ∣ z ⋅ y) → (x ∣ y)
divides-without-[⋅]ₗ-both' {x}{y}{𝐒(z)} _ = divides-without-[⋅]ₗ-both {x}{y}{z}

divides-factorial : ∀{n x} → (𝐒(x) ≤ n) → (𝐒(x) ∣ (n !))
divides-factorial {.(𝐒 y)}{.x} (succ {x}{y} xy) with [≥]-or-[<] {x}{y}
... | [∨]-introₗ yx with [≡]-intro ← antisymmetry(_≤_)(_≡_) xy yx = divides-with-[⋅] {𝐒(x)}{𝐒(x)}{x !} ([∨]-introₗ(reflexivity(_∣_)))
... | [∨]-introᵣ sxy = divides-with-[⋅] {𝐒(x)}{𝐒(y)}{y !} ([∨]-introᵣ(divides-factorial{y}{x} sxy))

instance
  divides-antisymmetry : Antisymmetry(_∣_)(_≡_)
  Antisymmetry.proof divides-antisymmetry {𝟎} {𝟎}     ab ba = [≡]-intro
  Antisymmetry.proof divides-antisymmetry {𝟎} {𝐒 b}   ab ba with () ← [0]-divides-not ab
  Antisymmetry.proof divides-antisymmetry {𝐒 a} {𝟎}   ab ba with () ← [0]-divides-not ba
  Antisymmetry.proof divides-antisymmetry {𝐒 a} {𝐒 b} ab ba = antisymmetry(_≤_)(_≡_) (divides-upper-limit ab) (divides-upper-limit ba)

divides-quotient-positive : ∀{d n}{dn : (d ∣ 𝐒(n))} → (divides-quotient dn ≥ 1)
divides-quotient-positive {𝟎}   {n}        {dn = dn}      with () ← [0]-divides-not dn
divides-quotient-positive {𝐒 d} {.(d + _)} {dn = Div𝐒 dn} = succ _≤_.min

divides-quotient-composite : ∀{d n} → (d ≥ 2) → (d < n) → ∀{dn : (d ∣ n)} → (divides-quotient dn ≥ 2)
divides-quotient-composite l g {Div𝐒 {x = 𝟎}   dn} with () ← irreflexivity(_<_) g
divides-quotient-composite l g {Div𝐒 {x = 𝐒 x} dn} = succ (divides-quotient-positive {dn = dn})

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Nat
open import Prelude
open import List
open import contexts
open import judgemental-erase
open import lemmas-matching
open import moveerase
open import sensibility
open import statics-core
open import synth-unicity

module statics-checks where
  -- these three judmgements lift the action semantics judgements to relate
  -- an expression and a list of pair-wise composable actions to the
  -- expression that's produced by tracing through the action semantics for
  -- each element in that list.
  --
  -- we do this just by appealing to the original judgement with
  -- constraints on the terms to enforce composability.
  --
  -- in all three cases, we assert that the empty list of actions
  -- constitutes a reflexivity step, so when you run out of actions to
  -- preform you have to be where you wanted to be.
  --
  -- note that the only difference between the types for each judgement and
  -- the original action semantics is that the action is now a list of
  -- actions.
  data runtype : (t : ztyp) (Lα : List action) (t' : ztyp) → Set where
     DoRefl : {t : ztyp} →
              runtype t [] t
     DoType : {t : ztyp} {α : action} {t' t'' : ztyp}
              {L : List action} →
              t + α +> t' →
              runtype t' L t'' →
              runtype t (α :: L) t''

  data runsynth : (Γ : tctx) (e : zexp) (t1 : htyp) (Lα : List action)
                  (e' : zexp) (t2 : htyp) → Set where
     DoRefl  : {Γ : tctx} {e : zexp} {t : htyp} →
               runsynth Γ e t [] e t
     DoSynth : {Γ : tctx} {e : zexp} {t : htyp} {α : action} {e' e'' : zexp} {t' t'' : htyp}
               {L : List action} →
               Γ ⊢ e => t ~ α ~> e' => t' →
               runsynth Γ e' t' L e'' t'' →
               runsynth Γ e t (α :: L) e'' t''

  data runana : (Γ : tctx) (e : zexp) (Lα : List action) (e' : zexp) (t : htyp) → Set where
     DoRefl : {Γ : tctx} {e : zexp} {t : htyp} →
              runana Γ e [] e t
     DoAna  : {Γ : tctx} {e : zexp} {α : action} {e' e'' : zexp} {t : htyp}
              {L : List action} →
              Γ ⊢ e ~ α ~> e' ⇐ t →
              runana Γ e' L e'' t →
              runana Γ e (α :: L) e'' t

  -- all three run judgements lift to the list monoid as expected. these
  -- theorems are simple because the structure of lists is simple, but they
  -- amount a reasoning principle about the composition of action sequences
  -- by letting you split lists in (nearly) arbitrary places and argue
  -- about the consequences of the splits before composing them together.
  runtype++ : ∀{t t' t'' L1 L2 } →
              runtype t  L1 t' →
              runtype t' L2 t'' →
              runtype t (L1 ++ L2) t''
  runtype++ DoRefl d2 = d2
  runtype++ (DoType x d1) d2 = DoType x (runtype++ d1 d2)

  runsynth++ : ∀{Γ e t L1 e' t' L2 e'' t''} →
               runsynth Γ e t L1 e' t' →
               runsynth Γ e' t' L2 e'' t'' →
               runsynth Γ e t (L1 ++ L2) e'' t''
  runsynth++ DoRefl d2 = d2
  runsynth++ (DoSynth x d1) d2 = DoSynth x (runsynth++ d1 d2)

  runana++ : ∀{Γ e t L1 e' L2 e''} →
             runana Γ e  L1 e' t →
             runana Γ e' L2 e'' t →
             runana Γ e (L1 ++ L2) e'' t
  runana++ DoRefl d2 = d2
  runana++ (DoAna x d1) d2 = DoAna x (runana++ d1 d2)

  -- the following collection of lemmas asserts that the various runs
  -- interoperate nicely. in many cases, these amount to observing
  -- something like congruence: if a subterm is related to something by one
  -- of the judgements, it can be replaced by the thing to which it is
  -- related in a larger context without disrupting that larger
  -- context.
  --
  -- taken together, this is a little messier than a proper congruence,
  -- because the action semantics demand well-typedness at each step, and
  -- therefore there are enough premises to each lemma to supply to the
  -- action semantics rules.
  --
  -- therefore, these amount to a checksum on the zipper actions under the
  -- lifing of the action semantics to the list monoid.
  --
  -- they only check the zipper actions they happen to be include, however,
  -- which is driven by the particular lists we use in the proofs of
  -- contructability and reachability, which may or may not be all of
  -- them. additionally, the lemmas given here are what is needed for these
  -- proofs, not anything that's more general.

    -- type zippers
  ziplem-tmarr1 : ∀{t1 t1' t2 L} →
                  runtype t1' L t1 →
                  runtype (t1' ==>₁ t2) L (t1 ==>₁ t2)
  ziplem-tmarr1 DoRefl = DoRefl
  ziplem-tmarr1 (DoType x L') = DoType (TMArrZip1 x) (ziplem-tmarr1 L')

  ziplem-tmarr2 : ∀{t1 t2 t2' L} →
                  runtype t2' L t2 →
                  runtype (t1 ==>₂ t2') L (t1 ==>₂ t2)
  ziplem-tmarr2 DoRefl = DoRefl
  ziplem-tmarr2 (DoType x L') = DoType (TMArrZip2 x) (ziplem-tmarr2 L')

  ziplem-tmplus1 : ∀{t1 t1' t2 L} →
                   runtype t1' L t1 →
                   runtype (t1' ⊕₁ t2) L (t1 ⊕₁ t2)
  ziplem-tmplus1 DoRefl = DoRefl
  ziplem-tmplus1 (DoType x L') = DoType (TMPlusZip1 x) (ziplem-tmplus1 L')

  ziplem-tmplus2 : ∀{t1 t2 t2' L} →
                   runtype t2' L t2 →
                   runtype (t1 ⊕₂ t2') L (t1 ⊕₂ t2)
  ziplem-tmplus2 DoRefl = DoRefl
  ziplem-tmplus2 (DoType x L') = DoType (TMPlusZip2 x) (ziplem-tmplus2 L')

  ziplem-tmprod1 : ∀{t1 t1' t2 L} →
                   runtype t1' L t1 →
                   runtype (t1' ⊠₁ t2) L (t1 ⊠₁ t2)
  ziplem-tmprod1 DoRefl = DoRefl
  ziplem-tmprod1 (DoType x L') = DoType (TMProdZip1 x) (ziplem-tmprod1 L')

  ziplem-tmprod2 : ∀{t1 t2 t2' L} →
                   runtype t2' L t2 →
                   runtype (t1 ⊠₂ t2') L (t1 ⊠₂ t2)
  ziplem-tmprod2 DoRefl = DoRefl
  ziplem-tmprod2 (DoType x L') = DoType (TMProdZip2 x) (ziplem-tmprod2 L')

    -- expression zippers
  ziplem-asc1 : ∀{Γ t L e e'} →
                runana Γ e L e' t →
                runsynth Γ (e ·:₁ t) t L (e' ·:₁ t) t
  ziplem-asc1 DoRefl = DoRefl
  ziplem-asc1 (DoAna a r) = DoSynth (SAZipAsc1 a) (ziplem-asc1 r)

  ziplem-asc2 : ∀{Γ t L t' t◆ t'◆ u} →
                erase-t t t◆ →
                erase-t t' t'◆ →
                runtype t L t' →
                runsynth Γ (⦇-⦈[ u ] ·:₂ t) t◆ L (⦇-⦈[ u ] ·:₂ t') t'◆
  ziplem-asc2 {Γ} er er' rt with erase-t◆ er | erase-t◆ er'
  ... | refl | refl = ziplem-asc2' {Γ = Γ} rt
   where
     ziplem-asc2' : ∀{t L t' Γ u} →
                    runtype t L t' →
                    runsynth Γ (⦇-⦈[ u ] ·:₂ t) (t ◆t) L (⦇-⦈[ u ] ·:₂ t') (t' ◆t)
     ziplem-asc2' DoRefl = DoRefl
     ziplem-asc2' (DoType x rt) =
       DoSynth (SAZipAsc2 x (◆erase-t _ _ refl) (◆erase-t _ _ refl) (ASubsume SEHole TCHole1))
               (ziplem-asc2' rt)

  ziplem-lam : ∀{Γ x e t t1 t2 L e'} →
               x # Γ →
               t ▸arr (t1 ==> t2) →
               runana (Γ ,, (x , t1)) e L e' t2 →
               runana Γ (·λ x e) L (·λ x e') t
  ziplem-lam a m DoRefl = DoRefl
  ziplem-lam a m (DoAna x₁ d) = DoAna (AAZipLam a m x₁) (ziplem-lam a m d)

  ziplem-halflam1 : ∀{Γ u t1 t1' t1◆ t1'◆ x l} →
                    x # Γ →
                    erase-t t1 t1◆ →
                    erase-t t1' t1'◆ →
                    runtype t1 l t1' →
                    runsynth Γ (·λ x ·[ t1 ]₁ ⦇-⦈[ u ]) (t1◆ ==> ⦇-⦈) l
                      (·λ x ·[ t1' ]₁ ⦇-⦈[ u ]) (t1'◆ ==> ⦇-⦈)
  ziplem-halflam1 apt et et' DoRefl
    with eraset-det et et'
  ... | refl = DoRefl
  ziplem-halflam1 apt et et' (DoType x rt) =
    DoSynth (SAZipLam1 apt et (rel◆t _) x SEHole SEHole)
            (ziplem-halflam1 apt (rel◆t _) et' rt)

  ziplem-halflam2 : ∀{Γ e e' e◆ t1 t2 t2' x L} →
                    x # Γ →
                    erase-e e e◆ →
                    (Γ ,, (x , t1)) ⊢ e◆ => t2 →
                    runsynth (Γ ,, (x , t1)) e t2 L e' t2' →
                    runsynth Γ (·λ x ·[ t1 ]₂ e) (t1 ==> t2) L
                      (·λ x ·[ t1 ]₂ e') (t1 ==> t2')
  ziplem-halflam2 apt ee wt DoRefl = DoRefl
  ziplem-halflam2 apt ee wt (DoSynth x rs) =
    DoSynth (SAZipLam2 apt ee wt x)
            (ziplem-halflam2 apt (rel◆ _) (actsense-synth ee (rel◆ _) x wt) rs)

  ziplem-plus1 : ∀{Γ e L e' f} →
                 runana Γ e L e' num →
                 runsynth Γ (e ·+₁ f) num L (e' ·+₁ f) num
  ziplem-plus1 DoRefl = DoRefl
  ziplem-plus1 (DoAna x d) = DoSynth (SAZipPlus1 x) (ziplem-plus1 d)

  ziplem-plus2 : ∀{Γ e L e' f} →
                 runana Γ e L e' num →
                 runsynth Γ (f ·+₂ e) num L (f ·+₂ e') num
  ziplem-plus2 DoRefl = DoRefl
  ziplem-plus2 (DoAna x d) = DoSynth (SAZipPlus2 x) (ziplem-plus2 d)

  ziplem-ap2 : ∀{Γ e L e' t t' f tf} →
               Γ ⊢ f => t' →
               t' ▸arr (t ==> tf) →
               runana Γ e L e' t →
               runsynth Γ (f ∘₂ e) tf L (f ∘₂ e') tf
  ziplem-ap2 wt m DoRefl = DoRefl
  ziplem-ap2 wt m (DoAna x d) = DoSynth (SAZipApAna m wt x) (ziplem-ap2 wt m d)

  ziplem-nehole-a : ∀{Γ e e' L t t' u} →
                    (Γ ⊢ e ◆e => t) →
                    runsynth Γ e t L e' t' →
                    runsynth Γ ⦇⌜ e ⌟⦈[ u ] ⦇-⦈ L ⦇⌜ e' ⌟⦈[ u ] ⦇-⦈
  ziplem-nehole-a wt DoRefl = DoRefl
  ziplem-nehole-a wt (DoSynth {e = e} x d) =
    DoSynth (SAZipNEHole (rel◆ e) wt x)
            (ziplem-nehole-a (actsense-synth (rel◆ e) (rel◆ _) x wt) d)

  ziplem-nehole-b : ∀{Γ e e' L t t' t'' u} →
                    (Γ ⊢ e ◆e => t) →
                    (t'' ~ t') →
                    runsynth Γ e t L e' t' →
                    runana Γ ⦇⌜ e ⌟⦈[ u ] L ⦇⌜ e' ⌟⦈[ u ] t''
  ziplem-nehole-b wt c DoRefl = DoRefl
  ziplem-nehole-b wt c (DoSynth x rs) =
    DoAna (AASubsume (erase-in-hole (rel◆ _)) (SNEHole wt) (SAZipNEHole (rel◆ _) wt x) TCHole1)
          (ziplem-nehole-b (actsense-synth (rel◆ _) (rel◆ _) x wt) c rs)

  -- because the point of the reachability theorems is to show that we
  -- didn't forget to define any of the action semantic cases, it's
  -- important that theorems include the fact that the witness only uses
  -- move -- otherwise, you could cheat by just prepending [ del ] to the
  -- list produced by constructability. constructability does also use
  -- some, but not all, of the possible movements, so this would no longer
  -- demonstrate the property we really want. to that end, we define a
  -- predicate on lists that they contain only (move _) and that the
  -- various things above that produce the lists we use have this property.

  -- predicate
  data movements : List action → Set where
    AM:: : {L : List action} {δ : direction} →
           movements L →
           movements ((move δ) :: L)
    AM[] : movements []

  -- movements breaks over the list monoid, as expected
  movements++ : {l1 l2 : List action} →
                movements l1 →
                movements l2 →
                movements (l1 ++ l2)
  movements++ (AM:: m1) m2 = AM:: (movements++ m1 m2)
  movements++ AM[] m2 = m2

  -- these are zipper lemmas that are specific to list of movement
  -- actions. they are not true for general actions, but because
  -- reachability is restricted to movements, we get some milage out of
  -- them anyway.
  endpoints : ∀{Γ e t L e' t'} →
              Γ ⊢ (e ◆e) => t →
              runsynth Γ e t L e' t' →
              movements L →
              t == t'
  endpoints _ DoRefl AM[] = refl
  endpoints wt (DoSynth x rs) (AM:: mv)
    with endpoints (actsense-synth (rel◆ _) (rel◆ _) x wt) rs mv
  ... | refl = π2 (moveerase-synth (rel◆ _) wt x)

  ziplem-moves-asc2 : ∀{ Γ l t t' e t◆} →
                      movements l →
                      erase-t t t◆ →
                      Γ ⊢ e <= t◆ →
                      runtype t l t' →
                      runsynth Γ (e ·:₂ t) t◆ l (e ·:₂ t') t◆
  ziplem-moves-asc2 _ _ _ DoRefl = DoRefl
  ziplem-moves-asc2 (AM:: m) er wt (DoType x rt) with moveeraset' er x
  ... | er' =  DoSynth (SAZipAsc2 x er' er wt) (ziplem-moves-asc2 m er' wt rt)

  synthana-moves : ∀{t t' l e e' Γ} →
                   Γ ⊢ e ◆e => t' →
                   movements l →
                   t ~ t' →
                   runsynth Γ e t' l e' t' →
                   runana Γ e l e' t
  synthana-moves _ _ _ DoRefl = DoRefl
  synthana-moves wt (AM:: m) c (DoSynth x rs) with π2 (moveerase-synth (rel◆ _) wt x)
  ... | refl =
    DoAna (AASubsume (rel◆ _) wt x c)
          (synthana-moves (actsense-synth (rel◆ _) (rel◆ _) x wt) m c rs)

  ziplem-moves-halflam1 : ∀{Γ e t1 t1' t1◆ t1'◆ t2 t2' x l} →
                          x # Γ →
                          erase-t t1 t1◆ →
                          erase-t t1' t1'◆ →
                          movements l →
                          runtype t1 l t1' →
                          (Γ ,, (x , t1◆)) ⊢ e => t2 →
                          (Γ ,, (x , t1'◆)) ⊢ e => t2' →
                          runsynth Γ (·λ x ·[ t1 ]₁ e) (t1◆ ==> t2) l
                          (·λ x ·[ t1' ]₁ e) (t1'◆ ==> t2')
  ziplem-moves-halflam1 apt et et' AM[] DoRefl wt1 wt2
    with eraset-det et et'
  ... | refl with synthunicity wt1 wt2
  ... | refl = DoRefl
  ziplem-moves-halflam1 apt et et' (AM:: mv) (DoType x rt) wt1 wt2
    with erase-t◆ et | erase-t◆ et'
  ... | refl | refl with moveeraset x
  ... | qq rewrite qq with ziplem-moves-halflam1 apt (rel◆t _) (rel◆t _) mv rt wt1 wt2
  ... | ww = DoSynth (SAZipLam1 apt et (rel◆t _) x wt1 wt1) ww

  ziplem-moves-ap1 : ∀{Γ l e1 e1' e2 t t' tx} →
                     Γ ⊢ e1 ◆e => t →
                     t ▸arr (tx ==> t') →
                     Γ ⊢ e2 <= tx →
                     movements l →
                     runsynth Γ e1 t l e1' t →
                     runsynth Γ (e1 ∘₁ e2) t' l (e1' ∘₁ e2) t'
  ziplem-moves-ap1 _ _ _ _ DoRefl = DoRefl
  ziplem-moves-ap1 wt1 mch wt2 (AM:: m) (DoSynth x rs) with π2 (moveerase-synth (rel◆ _) wt1 x)
  ... | refl =
    DoSynth (SAZipApArr mch (rel◆ _) wt1 x wt2)
    (ziplem-moves-ap1 (actsense-synth (rel◆ _) (rel◆ _) x wt1) mch wt2 m rs)

  -- zip lemmas for sums
  ziplem-inl : ∀{t t1 t2 Γ e L e'} →
               t ▸sum (t1 ⊕ t2) →
               runana Γ e L e' t1 →
               runana Γ (inl e) L (inl e') t
  ziplem-inl m DoRefl = DoRefl
  ziplem-inl m (DoAna x r) = DoAna (AAZipInl m x) (ziplem-inl m r)

  ziplem-inr : ∀{t t1 t2 Γ e L e'} →
               t ▸sum (t1 ⊕ t2) →
               runana Γ e L e' t2 →
               runana Γ (inr e) L (inr e') t
  ziplem-inr m DoRefl = DoRefl
  ziplem-inr m (DoAna x r) = DoAna (AAZipInr m x) (ziplem-inr m r)

  ziplem-case1a : ∀{x Γ y e e◆ t0 t+ e' e1 e2 L t1 t2 t} →
                  x # Γ →
                  y # Γ →
                  erase-e e e◆ →
                  Γ ⊢ e◆ => t0 →
                  runsynth Γ e t0 L e' t+ →
                  t+ ▸sum (t1 ⊕ t2) →
                  (Γ ,, (x , t1)) ⊢ e1 <= t →
                  (Γ ,, (y , t2)) ⊢ e2 <= t →
                  movements L →
                  runana Γ (case₁ e x e1 y e2) L (case₁ e' x e1 y e2) t
  ziplem-case1a x# y# er wt0 DoRefl m wt1 wt2 mv = DoRefl
  ziplem-case1a x# y# er wt0 (DoSynth α rs) m wt1 wt2 (AM:: mv)
    with endpoints (actsense-synth er (rel◆ _) α wt0) rs mv
  ... | refl with (π2 (moveerase-synth er wt0 α))
  ... | refl =
    DoAna (AAZipCase1 x# y# er wt0 α m wt1 wt2)
          (ziplem-case1a x# y# (eq-er-trans (π1 (moveerase-synth er wt0 α)) er)
                         wt0 rs m wt1 wt2 mv)

  ziplem-case1b : ∀{Γ e e' t L t' x y t0 e◆ u u1 u2} →
                  x # Γ →
                  y # Γ →
                  erase-e e e◆ →
                  Γ ⊢ e◆ => t →
                  runsynth Γ e t L e' t' →
                  runana Γ (case₁ ⦇⌜ e ⌟⦈[ u ] x ⦇-⦈[ u1 ] y ⦇-⦈[ u2 ]) L
                           (case₁ ⦇⌜ e' ⌟⦈[ u ] x ⦇-⦈[ u1 ] y ⦇-⦈[ u2 ]) t0
  ziplem-case1b _ _ _ _ DoRefl = DoRefl
  ziplem-case1b x# y# er wt (DoSynth x₁ rs) =
    DoAna (AAZipCase1 x# y# (erase-in-hole er) (SNEHole wt) (SAZipNEHole er wt x₁)
          MSHole (ASubsume SEHole TCHole1) (ASubsume SEHole TCHole1))
          (ziplem-case1b x# y# (rel◆ _) (actsense-synth er (rel◆ _) x₁ wt) rs)

  ziplem-case2 : ∀{t t+ t1 t2 Γ x y e e1 e1' e2 l} →
                 x # Γ →
                 y # Γ →
                 Γ ⊢ e => t+ →
                 (Γ ,, (y , t2)) ⊢ e2 <= t →
                 t+ ▸sum (t1 ⊕ t2) →
                 runana (Γ ,, (x , t1)) e1 l e1' t →
                 runana Γ (case₂ e x e1 y e2) l (case₂ e x e1' y e2) t
  ziplem-case2 x# y# wt1 wt2 m DoRefl = DoRefl
  ziplem-case2 x# y# wt1 wt2 m (DoAna x₁ ra) =
    DoAna (AAZipCase2 x# y# wt1 m x₁)
          (ziplem-case2 x# y# wt1 wt2 m ra)

  ziplem-case3  : ∀{t t+ t1 t2 Γ x y e e1 e2 e2' l} →
                  x # Γ →
                  y # Γ →
                  Γ ⊢ e => t+ →
                  (Γ ,, (x , t1)) ⊢ e1 <= t →
                  t+ ▸sum (t1 ⊕ t2) →
                  runana (Γ ,, (y , t2)) e2 l e2' t →
                  runana Γ (case₃ e x e1 y e2) l (case₃ e x e1 y e2') t
  ziplem-case3 x# y# wt1 wt2 m DoRefl = DoRefl
  ziplem-case3 x# y# wt1 wt2 m (DoAna x₁ ra) =
    DoAna (AAZipCase3 x# y# wt1 m x₁)
          (ziplem-case3 x# y# wt1 wt2 m ra)

  -- zip lemma for products
  ziplem-pair1 : ∀ {t1 t1' t2 Γ e1 e1◆ l e1' e2} →
                 erase-e e1 e1◆ →
                 Γ ⊢ e1◆ => t1 →
                 runsynth Γ e1 t1 l e1' t1' →
                 Γ ⊢ e2 => t2 →
                 runsynth Γ ⟨ e1 , e2 ⟩₁ (t1 ⊠ t2) l ⟨ e1' , e2 ⟩₁ (t1' ⊠ t2)
  ziplem-pair1 er wt1 DoRefl wt2 = DoRefl
  ziplem-pair1 er wt1 (DoSynth x rs) wt2 =
    DoSynth (SAZipPair1 er wt1 x wt2)
            (ziplem-pair1 (rel◆ _) (actsense-synth er (rel◆ _) x wt1) rs wt2)

  ziplem-pair2 : ∀ {t1 t2 t2' Γ e1 e2 e2◆ l e2'} →
                 Γ ⊢ e1 => t1 →
                 erase-e e2 e2◆ →
                 Γ ⊢ e2◆ => t2 →
                 runsynth Γ e2 t2 l e2' t2' →
                 runsynth Γ ⟨ e1 , e2 ⟩₂ (t1 ⊠ t2) l ⟨ e1 , e2' ⟩₂ (t1 ⊠ t2')
  ziplem-pair2 wt1 er wt2 DoRefl = DoRefl
  ziplem-pair2 wt1 er wt2 (DoSynth x rs) =
    DoSynth (SAZipPair2 wt1 er wt2 x)
            (ziplem-pair2 wt1 (rel◆ _) (actsense-synth er (rel◆ _) x wt2) rs)

  ziplem-moves-fst : ∀ {t× t×' t1 t1' t2 t2' Γ e e◆ l e'} →
                   t× ▸prod (t1 ⊠ t2) →
                   t×' ▸prod (t1' ⊠ t2') →
                   erase-e e e◆ →
                   Γ ⊢ e◆ => t× →
                   movements l →
                   runsynth Γ e t× l e' t×' →
                   runsynth Γ (fst e) t1 l (fst e') t1'
  ziplem-moves-fst pr pr' er wt m DoRefl with ▸prod-unicity pr pr'
  ... | refl = DoRefl
  ziplem-moves-fst pr pr' er wt (AM:: m) (DoSynth x rs)
    with endpoints (actsense-synth er (rel◆ _) x wt) rs m
  ... | refl with moveerase-synth er wt x
  ... | q , refl with ▸prod-unicity pr pr'
  ... | refl =
    DoSynth (SAZipFst pr pr' er wt x)
            (ziplem-moves-fst pr pr' (eq-er-trans q er) wt m rs)

  ziplem-moves-snd : ∀ {t× t×' t1 t1' t2 t2' Γ e e◆ l e'} →
                   t× ▸prod (t1 ⊠ t2) →
                   t×' ▸prod (t1' ⊠ t2') →
                   erase-e e e◆ →
                   Γ ⊢ e◆ => t× →
                   movements l →
                   runsynth Γ e t× l e' t×' →
                   runsynth Γ (snd e) t2 l (snd e') t2'
  ziplem-moves-snd pr pr' er wt m DoRefl with ▸prod-unicity pr pr'
  ... | refl = DoRefl
  ziplem-moves-snd pr pr' er wt (AM:: m) (DoSynth x rs)
    with endpoints (actsense-synth er (rel◆ _) x wt) rs m
  ... | refl with moveerase-synth er wt x
  ... | q , refl with ▸prod-unicity pr pr'
  ... | refl =
    DoSynth (SAZipSnd pr pr' er wt x)
            (ziplem-moves-snd pr pr' (eq-er-trans q er) wt m rs)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module SubstantiveDischargeIsReflexive where

open import HasSubstantiveDischarge

record SubstantiveDischargeIsReflexive (A : Set) ⦃ _ : HasSubstantiveDischarge A A ⦄ : Set₁
 where
  field
    ≽-reflexive : (x : A) → x ≽ x

{-
record SubstantiveDischargeIsReflexive (A : Set) : Set₁
 where
  field
    overlap ⦃ hasSubstantiveDischarge ⦄ : HasSubstantiveDischarge A A
    ≽-reflexive : (x : A) → x ≽ x
-}
open SubstantiveDischargeIsReflexive ⦃ … ⦄ public
{-
record SubstantiveDischargeIsReflexive (A : Set) ⦃ _ : HasSubstantiveDischarge A A ⦄ : Set₁
 where
  field
    ≽-reflexive : {x : A} → x ≽ x

open SubstantiveDischargeIsReflexive ⦃ … ⦄
-}
{-# DISPLAY SubstantiveDischargeIsReflexive.≽-reflexive _ = ≽-reflexive #-}


text:
-- Andreas, 2017-10-09, issue #2576
-- Duplicate definition should be reported as such,
-- not as "Missing type signature."

data ⊥ : Set where
data ⊥ where

-- Error was: Missing type signature for ⊥
-- Error was: Duplicate definition of module ⊥ (fixed 2019-07-07)

-- Expected error: Multiple definitions of ⊥

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to Fin, and operations making use of these
-- properties (or other properties not available in Data.Fin)
------------------------------------------------------------------------

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

module Data.Fin.Properties where

open import Algebra.FunctionProperties using (Involutive)
open import Category.Applicative using (RawApplicative)
open import Category.Functor using (RawFunctor)
open import Data.Empty using (⊥-elim)
open import Data.Fin.Base
open import Data.Nat as ℕ using (ℕ; zero; suc; s≤s; z≤n; _∸_)
  renaming
  ( _≤_ to _ℕ≤_
  ; _<_ to _ℕ<_
  ; _+_ to _ℕ+_
  )
import Data.Nat.Properties as ℕₚ
open import Data.Unit using (tt)
open import Data.Product using (∃; ∃₂; ∄; _×_; _,_; map; proj₁)
open import Function using (_∘_; id)
open import Function.Injection using (_↣_)
open import Relation.Binary as B hiding (Decidable)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; sym; trans; cong; subst; module ≡-Reasoning)
open import Relation.Nullary using (¬_)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Unary as U using (U; Pred; Decidable; _⊆_)
open import Relation.Unary.Properties using (U?)

------------------------------------------------------------------------
-- Fin

¬Fin0 : ¬ Fin 0
¬Fin0 ()

------------------------------------------------------------------------
-- Properties of _≡_

suc-injective : ∀ {o} {m n : Fin o} → Fin.suc m ≡ suc n → m ≡ n
suc-injective refl = refl

infix 4 _≟_

_≟_ : ∀ {n} → B.Decidable {A = Fin n} _≡_
zero  ≟ zero  = yes refl
zero  ≟ suc y = no λ()
suc x ≟ zero  = no λ()
suc x ≟ suc y with x ≟ y
... | yes x≡y = yes (cong suc x≡y)
... | no  x≢y = no  (x≢y ∘ suc-injective)

preorder : ℕ → Preorder _ _ _
preorder n = P.preorder (Fin n)

setoid : ℕ → Setoid _ _
setoid n = P.setoid (Fin n)

isDecEquivalence : ∀ {n} → IsDecEquivalence (_≡_ {A = Fin n})
isDecEquivalence = record
  { isEquivalence = P.isEquivalence
  ; _≟_           = _≟_
  }

decSetoid : ℕ → DecSetoid _ _
decSetoid n = record
  { Carrier          = Fin n
  ; _≈_              = _≡_
  ; isDecEquivalence = isDecEquivalence
  }

------------------------------------------------------------------------
-- toℕ

toℕ-injective : ∀ {n} {i j : Fin n} → toℕ i ≡ toℕ j → i ≡ j
toℕ-injective {zero}  {}      {}      _
toℕ-injective {suc n} {zero}  {zero}  eq = refl
toℕ-injective {suc n} {zero}  {suc j} ()
toℕ-injective {suc n} {suc i} {zero}  ()
toℕ-injective {suc n} {suc i} {suc j} eq =
  cong suc (toℕ-injective (cong ℕ.pred eq))

toℕ-strengthen : ∀ {n} (i : Fin n) → toℕ (strengthen i) ≡ toℕ i
toℕ-strengthen zero    = refl
toℕ-strengthen (suc i) = cong suc (toℕ-strengthen i)

toℕ-raise : ∀ {m} n (i : Fin m) → toℕ (raise n i) ≡ n ℕ+ toℕ i
toℕ-raise zero    i = refl
toℕ-raise (suc n) i = cong suc (toℕ-raise n i)

toℕ<n : ∀ {n} (i : Fin n) → toℕ i ℕ< n
toℕ<n zero    = s≤s z≤n
toℕ<n (suc i) = s≤s (toℕ<n i)

toℕ≤pred[n] : ∀ {n} (i : Fin n) → toℕ i ℕ≤ ℕ.pred n
toℕ≤pred[n] zero                 = z≤n
toℕ≤pred[n] (suc {n = zero}  ())
toℕ≤pred[n] (suc {n = suc n} i)  = s≤s (toℕ≤pred[n] i)

-- A simpler implementation of toℕ≤pred[n],
-- however, with a different reduction behavior.
-- If no one needs the reduction behavior of toℕ≤pred[n],
-- it can be removed in favor of toℕ≤pred[n]′.
toℕ≤pred[n]′ : ∀ {n} (i : Fin n) → toℕ i ℕ≤ ℕ.pred n
toℕ≤pred[n]′ i = ℕₚ.<⇒≤pred (toℕ<n i)

------------------------------------------------------------------------
-- fromℕ

toℕ-fromℕ : ∀ n → toℕ (fromℕ n) ≡ n
toℕ-fromℕ zero    = refl
toℕ-fromℕ (suc n) = cong suc (toℕ-fromℕ n)

fromℕ-toℕ : ∀ {n} (i : Fin n) → fromℕ (toℕ i) ≡ strengthen i
fromℕ-toℕ zero    = refl
fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)

------------------------------------------------------------------------
-- fromℕ≤

fromℕ≤-toℕ : ∀ {m} (i : Fin m) (i<m : toℕ i ℕ< m) → fromℕ≤ i<m ≡ i
fromℕ≤-toℕ zero    (s≤s z≤n)       = refl
fromℕ≤-toℕ (suc i) (s≤s (s≤s m≤n)) = cong suc (fromℕ≤-toℕ i (s≤s m≤n))

toℕ-fromℕ≤ : ∀ {m n} (m<n : m ℕ< n) → toℕ (fromℕ≤ m<n) ≡ m
toℕ-fromℕ≤ (s≤s z≤n)       = refl
toℕ-fromℕ≤ (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ≤ (s≤s m<n))

-- fromℕ is a special case of fromℕ≤.
fromℕ-def : ∀ n → fromℕ n ≡ fromℕ≤ ℕₚ.≤-refl
fromℕ-def zero    = refl
fromℕ-def (suc n) = cong suc (fromℕ-def n)

------------------------------------------------------------------------
-- fromℕ≤″

fromℕ≤≡fromℕ≤″ : ∀ {m n} (m<n : m ℕ< n) (m<″n : m ℕ.<″ n) →
                  fromℕ≤ m<n ≡ fromℕ≤″ m m<″n
fromℕ≤≡fromℕ≤″ (s≤s z≤n)       (ℕ.less-than-or-equal refl) = refl
fromℕ≤≡fromℕ≤″ (s≤s (s≤s m<n)) (ℕ.less-than-or-equal refl) =
  cong suc (fromℕ≤≡fromℕ≤″ (s≤s m<n) (ℕ.less-than-or-equal refl))

toℕ-fromℕ≤″ : ∀ {m n} (m<n : m ℕ.<″ n) → toℕ (fromℕ≤″ m m<n) ≡ m
toℕ-fromℕ≤″ {m} {n} m<n = begin
  toℕ (fromℕ≤″ m m<n)  ≡⟨ cong toℕ (sym (fromℕ≤≡fromℕ≤″ _ m<n)) ⟩
  toℕ (fromℕ≤ _)       ≡⟨ toℕ-fromℕ≤ (ℕₚ.≤″⇒≤ m<n) ⟩
  m ∎
  where open ≡-Reasoning

------------------------------------------------------------------------
-- cast

toℕ-cast : ∀ {m n} .(eq : m ≡ n) (k : Fin m) → toℕ (cast eq k) ≡ toℕ k
toℕ-cast {n = zero}  () zero
toℕ-cast {n = suc n} eq zero    = refl
toℕ-cast {n = zero}  () (suc k)
toℕ-cast {n = suc n} eq (suc k) = cong suc (toℕ-cast (cong ℕ.pred eq) k)

------------------------------------------------------------------------
-- Properties of _≤_

-- Relational properties
≤-reflexive : ∀ {n} → _≡_ ⇒ (_≤_ {n})
≤-reflexive refl = ℕₚ.≤-refl

≤-refl : ∀ {n} → Reflexive (_≤_ {n})
≤-refl = ≤-reflexive refl

≤-trans : ∀ {n} → Transitive (_≤_ {n})
≤-trans = ℕₚ.≤-trans

≤-antisym : ∀ {n} → Antisymmetric _≡_ (_≤_ {n})
≤-antisym x≤y y≤x = toℕ-injective (ℕₚ.≤-antisym x≤y y≤x)

≤-total : ∀ {n} → Total (_≤_ {n})
≤-total x y = ℕₚ.≤-total (toℕ x) (toℕ y)

infix 4 _≤?_ _<?_

_≤?_ : ∀ {n} → B.Decidable (_≤_ {n})
a ≤? b = toℕ a ℕ.≤? toℕ b

_<?_ : ∀ {n} → B.Decidable (_<_ {n})
m <? n = suc (toℕ m) ℕ.≤? toℕ n

≤-isPreorder : ∀ {n} → IsPreorder _≡_ (_≤_ {n})
≤-isPreorder = record
  { isEquivalence = P.isEquivalence
  ; reflexive     = ≤-reflexive
  ; trans         = ≤-trans
  }

≤-preorder : ℕ → Preorder _ _ _
≤-preorder n = record
  { isPreorder = ≤-isPreorder {n}
  }

≤-isPartialOrder : ∀ {n} → IsPartialOrder _≡_ (_≤_ {n})
≤-isPartialOrder = record
  { isPreorder = ≤-isPreorder
  ; antisym    = ≤-antisym
  }

≤-poset : ℕ → Poset _ _ _
≤-poset n = record
  { isPartialOrder = ≤-isPartialOrder {n}
  }

≤-isTotalOrder : ∀ {n} → IsTotalOrder _≡_ (_≤_ {n})
≤-isTotalOrder = record
  { isPartialOrder = ≤-isPartialOrder
  ; total          = ≤-total
  }

≤-totalOrder : ℕ → TotalOrder _ _ _
≤-totalOrder n = record
  { isTotalOrder = ≤-isTotalOrder {n}
  }

≤-isDecTotalOrder : ∀ {n} → IsDecTotalOrder _≡_ (_≤_ {n})
≤-isDecTotalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  ; _≟_          = _≟_
  ; _≤?_         = _≤?_
  }

≤-decTotalOrder : ℕ → DecTotalOrder _ _ _
≤-decTotalOrder n = record
  { isDecTotalOrder = ≤-isDecTotalOrder {n}
  }

-- Other properties
≤-irrelevant : ∀ {n} → Irrelevant (_≤_ {n})
≤-irrelevant = ℕₚ.≤-irrelevant

------------------------------------------------------------------------
-- Properties of _<_

-- Relational properties
<-irrefl : ∀ {n} → Irreflexive _≡_ (_<_ {n})
<-irrefl refl = ℕₚ.<-irrefl refl

<-asym : ∀ {n} → Asymmetric (_<_ {n})
<-asym = ℕₚ.<-asym

<-trans : ∀ {n} → Transitive (_<_ {n})
<-trans = ℕₚ.<-trans

<-cmp : ∀ {n} → Trichotomous _≡_ (_<_ {n})
<-cmp zero    zero    = tri≈ (λ())     refl  (λ())
<-cmp zero    (suc j) = tri< (s≤s z≤n) (λ()) (λ())
<-cmp (suc i) zero    = tri> (λ())     (λ()) (s≤s z≤n)
<-cmp (suc i) (suc j) with <-cmp i j
... | tri< i<j i≢j j≮i = tri< (s≤s i<j)         (i≢j ∘ suc-injective) (j≮i ∘ ℕₚ.≤-pred)
... | tri> i≮j i≢j j<i = tri> (i≮j ∘ ℕₚ.≤-pred) (i≢j ∘ suc-injective) (s≤s j<i)
... | tri≈ i≮j i≡j j≮i = tri≈ (i≮j ∘ ℕₚ.≤-pred) (cong suc i≡j)        (j≮i ∘ ℕₚ.≤-pred)

<-respˡ-≡ : ∀ {n} → (_<_ {n}) Respectsˡ _≡_
<-respˡ-≡ refl x≤y = x≤y

<-respʳ-≡ : ∀ {n} → (_<_ {n}) Respectsʳ _≡_
<-respʳ-≡ refl x≤y = x≤y

<-resp₂-≡ : ∀ {n} → (_<_ {n}) Respects₂ _≡_
<-resp₂-≡ = <-respʳ-≡ , <-respˡ-≡

<-isStrictPartialOrder : ∀ {n} → IsStrictPartialOrder _≡_ (_<_ {n})
<-isStrictPartialOrder = record
  { isEquivalence = P.isEquivalence
  ; irrefl        = <-irrefl
  ; trans         = <-trans
  ; <-resp-≈      = <-resp₂-≡
  }

<-strictPartialOrder : ℕ → StrictPartialOrder _ _ _
<-strictPartialOrder n = record
  { isStrictPartialOrder = <-isStrictPartialOrder {n}
  }

<-isStrictTotalOrder : ∀ {n} → IsStrictTotalOrder _≡_ (_<_ {n})
<-isStrictTotalOrder = record
  { isEquivalence = P.isEquivalence
  ; trans         = <-trans
  ; compare       = <-cmp
  }

<-strictTotalOrder : ℕ → StrictTotalOrder _ _ _
<-strictTotalOrder n = record
  { isStrictTotalOrder = <-isStrictTotalOrder {n}
  }

-- Other properties
<-irrelevant : ∀ {n} → Irrelevant (_<_ {n})
<-irrelevant = ℕₚ.<-irrelevant

<⇒≢ : ∀ {n} {i j : Fin n} → i < j → i ≢ j
<⇒≢ i<i refl = ℕₚ.n≮n _ i<i

≤∧≢⇒< : ∀ {n} {i j : Fin n} → i ≤ j → i ≢ j → i < j
≤∧≢⇒< {i = zero}  {zero}  _         0≢0     = contradiction refl 0≢0
≤∧≢⇒< {i = zero}  {suc j} _         _       = s≤s z≤n
≤∧≢⇒< {i = suc i} {zero}  ()
≤∧≢⇒< {i = suc i} {suc j} (s≤s i≤j) 1+i≢1+j =
  s≤s (≤∧≢⇒< i≤j (1+i≢1+j ∘ (cong suc)))

------------------------------------------------------------------------
-- inject

toℕ-inject : ∀ {n} {i : Fin n} (j : Fin′ i) →
             toℕ (inject j) ≡ toℕ j
toℕ-inject {i = zero}  ()
toℕ-inject {i = suc i} zero    = refl
toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j)

------------------------------------------------------------------------
-- inject+

toℕ-inject+ : ∀ {m} n (i : Fin m) → toℕ i ≡ toℕ (inject+ n i)
toℕ-inject+ n zero    = refl
toℕ-inject+ n (suc i) = cong suc (toℕ-inject+ n i)

------------------------------------------------------------------------
-- inject₁

inject₁-injective : ∀ {n} {i j : Fin n} → inject₁ i ≡ inject₁ j → i ≡ j
inject₁-injective {i = zero}  {zero}  i≡j = refl
inject₁-injective {i = zero}  {suc j} ()
inject₁-injective {i = suc i} {zero}  ()
inject₁-injective {i = suc i} {suc j} i≡j =
  cong suc (inject₁-injective (suc-injective i≡j))

toℕ-inject₁ : ∀ {n} (i : Fin n) → toℕ (inject₁ i) ≡ toℕ i
toℕ-inject₁ zero    = refl
toℕ-inject₁ (suc i) = cong suc (toℕ-inject₁ i)

toℕ-inject₁-≢ : ∀ {n}(i : Fin n) → n ≢ toℕ (inject₁ i)
toℕ-inject₁-≢ zero = λ ()
toℕ-inject₁-≢ (suc i) = λ p → toℕ-inject₁-≢ i (ℕₚ.suc-injective p)

------------------------------------------------------------------------
-- inject₁ and lower₁

inject₁-lower₁ : ∀ {n} (i : Fin (suc n)) (n≢i : n ≢ toℕ i) →
                 inject₁ (lower₁ i n≢i) ≡ i
inject₁-lower₁ {zero}  zero     0≢0     = contradiction refl 0≢0
inject₁-lower₁ {zero}  (suc ()) _
inject₁-lower₁ {suc n} zero     _       = refl
inject₁-lower₁ {suc n} (suc i)  n+1≢i+1 =
  cong suc (inject₁-lower₁ i  (n+1≢i+1 ∘ cong suc))

lower₁-inject₁′ : ∀ {n} (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) →
                  lower₁ (inject₁ i) n≢i ≡ i
lower₁-inject₁′ zero    _       = refl
lower₁-inject₁′ (suc i) n+1≢i+1 =
  cong suc (lower₁-inject₁′ i (n+1≢i+1 ∘ cong suc))

lower₁-inject₁ : ∀ {n} (i : Fin n) →
                 lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i
lower₁-inject₁ i = lower₁-inject₁′ i (toℕ-inject₁-≢ i)

lower₁-irrelevant : ∀ {n} (i : Fin (suc n)) n≢i₁ n≢i₂ →
             lower₁ {n} i n≢i₁ ≡ lower₁ {n} i n≢i₂
lower₁-irrelevant {zero}  zero     0≢0 _ = contradiction refl 0≢0
lower₁-irrelevant {zero}  (suc ()) _   _
lower₁-irrelevant {suc n} zero     _   _ = refl
lower₁-irrelevant {suc n} (suc i)  _   _ =
  cong suc (lower₁-irrelevant i _ _)

------------------------------------------------------------------------
-- inject≤

toℕ-inject≤ : ∀ {m n} (i : Fin m) (le : m ℕ≤ n) →
                toℕ (inject≤ i le) ≡ toℕ i
toℕ-inject≤ zero    (s≤s le) = refl
toℕ-inject≤ (suc i) (s≤s le) = cong suc (toℕ-inject≤ i le)

inject≤-refl : ∀ {n} (i : Fin n) (n≤n : n ℕ≤ n) → inject≤ i n≤n ≡ i
inject≤-refl zero    (s≤s _  ) = refl
inject≤-refl (suc i) (s≤s n≤n) = cong suc (inject≤-refl i n≤n)

------------------------------------------------------------------------
-- _≺_

≺⇒<′ : _≺_ ⇒ ℕ._<′_
≺⇒<′ (n ≻toℕ i) = ℕₚ.≤⇒≤′ (toℕ<n i)

<′⇒≺ : ℕ._<′_ ⇒ _≺_
<′⇒≺ {n} ℕ.≤′-refl = subst (_≺ suc n) (toℕ-fromℕ n)
                              (suc n ≻toℕ fromℕ n)
<′⇒≺ (ℕ.≤′-step m≤′n) with <′⇒≺ m≤′n
... | n ≻toℕ i = subst (_≺ suc n) (toℕ-inject₁ i) (suc n ≻toℕ _)

------------------------------------------------------------------------
-- pred

<⇒≤pred : ∀ {n} {i j : Fin n} → j < i → j ≤ pred i
<⇒≤pred {i = zero}  {_}     ()
<⇒≤pred {i = suc i} {zero}  j<i       = z≤n
<⇒≤pred {i = suc i} {suc j} (s≤s j<i) =
  subst (_ ℕ≤_) (sym (toℕ-inject₁ i)) j<i

------------------------------------------------------------------------
-- ℕ-

toℕ‿ℕ- : ∀ n i → toℕ (n ℕ- i) ≡ n ∸ toℕ i
toℕ‿ℕ- n       zero     = toℕ-fromℕ n
toℕ‿ℕ- zero    (suc ())
toℕ‿ℕ- (suc n) (suc i)  = toℕ‿ℕ- n i

------------------------------------------------------------------------
-- ℕ-ℕ

nℕ-ℕi≤n : ∀ n i → n ℕ-ℕ i ℕ≤ n
nℕ-ℕi≤n n       zero     = ℕₚ.≤-refl
nℕ-ℕi≤n zero    (suc ())
nℕ-ℕi≤n (suc n) (suc i)  = begin
  n ℕ-ℕ i  ≤⟨ nℕ-ℕi≤n n i ⟩
  n        ≤⟨ ℕₚ.n≤1+n n ⟩
  suc n    ∎
  where open ℕₚ.≤-Reasoning

------------------------------------------------------------------------
-- punchIn

punchIn-injective : ∀ {m} i (j k : Fin m) →
                    punchIn i j ≡ punchIn i k → j ≡ k
punchIn-injective zero    _       _       refl      = refl
punchIn-injective (suc i) zero    zero    _         = refl
punchIn-injective (suc i) zero    (suc k) ()
punchIn-injective (suc i) (suc j) zero    ()
punchIn-injective (suc i) (suc j) (suc k) ↑j+1≡↑k+1 =
  cong suc (punchIn-injective i j k (suc-injective ↑j+1≡↑k+1))

punchInᵢ≢i : ∀ {m} i (j : Fin m) → punchIn i j ≢ i
punchInᵢ≢i zero    _    ()
punchInᵢ≢i (suc i) zero ()
punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective

------------------------------------------------------------------------
-- punchOut

-- A version of 'cong' for 'punchOut' in which the inequality argument can be
-- changed out arbitrarily (reflecting the proof-irrelevance of that argument).

punchOut-cong : ∀ {n} (i : Fin (suc n)) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} → j ≡ k → punchOut i≢j ≡ punchOut i≢k
punchOut-cong zero {zero} {i≢j = 0≢0} = contradiction refl 0≢0
punchOut-cong zero {suc j} {zero} {i≢k = 0≢0} = contradiction refl 0≢0
punchOut-cong zero {suc j} {suc k} = suc-injective
punchOut-cong {zero} (suc ())
punchOut-cong {suc n} (suc i) {zero} {zero} _ = refl
punchOut-cong {suc n} (suc i) {zero} {suc k} ()
punchOut-cong {suc n} (suc i) {suc j} {zero} ()
punchOut-cong {suc n} (suc i) {suc j} {suc k} = cong suc ∘ punchOut-cong i ∘ suc-injective

-- An alternative to 'punchOut-cong' in the which the new inequality argument is
-- specific. Useful for enabling the omission of that argument during equational
-- reasoning.

punchOut-cong′ : ∀ {n} (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) → punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)
punchOut-cong′ i q = punchOut-cong i q

punchOut-injective : ∀ {m} {i j k : Fin (suc m)}
                     (i≢j : i ≢ j) (i≢k : i ≢ k) →
                     punchOut i≢j ≡ punchOut i≢k → j ≡ k
punchOut-injective {_}     {zero}   {zero}  {_}     0≢0 _   _     = contradiction refl 0≢0
punchOut-injective {_}     {zero}   {_}     {zero}  _   0≢0 _     = contradiction refl 0≢0
punchOut-injective {_}     {zero}   {suc j} {suc k} _   _   pⱼ≡pₖ = cong suc pⱼ≡pₖ
punchOut-injective {zero}  {suc ()}
punchOut-injective {suc n} {suc i}  {zero}  {zero}  _   _    _    = refl
punchOut-injective {suc n} {suc i}  {zero}  {suc k} _   _   ()
punchOut-injective {suc n} {suc i}  {suc j} {zero}  _   _   ()
punchOut-injective {suc n} {suc i}  {suc j} {suc k} i≢j i≢k pⱼ≡pₖ =
  cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ))

punchIn-punchOut : ∀ {m} {i j : Fin (suc m)} (i≢j : i ≢ j) →
                   punchIn i (punchOut i≢j) ≡ j
punchIn-punchOut {_}     {zero}   {zero}  0≢0 = contradiction refl 0≢0
punchIn-punchOut {_}     {zero}   {suc j} _   = refl
punchIn-punchOut {zero}  {suc ()}
punchIn-punchOut {suc m} {suc i}  {zero}  i≢j = refl
punchIn-punchOut {suc m} {suc i}  {suc j} i≢j =
  cong suc (punchIn-punchOut (i≢j ∘ cong suc))

punchOut-punchIn : ∀ {n} i {j : Fin n} → punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j
punchOut-punchIn zero {j} = refl
punchOut-punchIn (suc i) {zero} = refl
punchOut-punchIn (suc i) {suc j} = cong suc (begin
  punchOut (punchInᵢ≢i i j ∘ suc-injective ∘ sym ∘ cong suc)  ≡⟨ punchOut-cong i refl ⟩
  punchOut (punchInᵢ≢i i j ∘ sym)                             ≡⟨ punchOut-punchIn i ⟩
  j                                                           ∎)
  where open ≡-Reasoning

------------------------------------------------------------------------
-- _+′_

infixl 6 _+′_

_+′_ : ∀ {m n} (i : Fin m) (j : Fin n) → Fin (ℕ.pred m ℕ+ n)
i +′ j = inject≤ (i + j) (ℕₚ.+-mono-≤ (toℕ≤pred[n] i) ℕₚ.≤-refl)

------------------------------------------------------------------------
-- Quantification

∀-cons : ∀ {n p} {P : Pred (Fin (suc n)) p} →
         P zero → (∀ i → P (suc i)) → (∀ i → P i)
∀-cons z s zero    = z
∀-cons z s (suc i) = s i

decFinSubset : ∀ {n p q} {P : Pred (Fin n) p} {Q : Pred (Fin n) q} →
               Decidable Q → (∀ {f} → Q f → Dec (P f)) → Dec (Q ⊆ P)
decFinSubset {zero}  {_}     {_} _  _  = yes λ{}
decFinSubset {suc n} {P = P} {Q} Q? P? with decFinSubset (Q? ∘ suc) P?
... | no ¬q⟶p = no (λ q⟶p → ¬q⟶p (q⟶p))
... | yes q⟶p with Q? zero
...   | no ¬q₀ = yes (∀-cons {P = Q U.⇒ P} (⊥-elim ∘ ¬q₀) (λ _ → q⟶p) _)
...   | yes q₀ with P? q₀
...     | no ¬p₀ = no (λ q⟶p → ¬p₀ (q⟶p q₀))
...     | yes p₀ = yes (∀-cons {P = Q U.⇒ P} (λ _ → p₀) (λ _ → q⟶p) _)

any? : ∀ {n p} {P : Fin n → Set p} → Decidable P → Dec (∃ P)
any? {zero}  {_} P? = no λ { (() , _) }
any? {suc n} {P} P? with P? zero | any? (P? ∘ suc)
... | yes P₀ | _              = yes (_ , P₀)
... | no  _  | yes (_ , P₁₊ᵢ) = yes (_ , P₁₊ᵢ)
... | no ¬P₀ | no ¬P₁₊ᵢ       = no λ
  { (zero  , P₀)   → ¬P₀ P₀
  ; (suc f , P₁₊ᵢ) → ¬P₁₊ᵢ (_ , P₁₊ᵢ)
  }

all? : ∀ {n p} {P : Pred (Fin n) p} →
       Decidable P → Dec (∀ f → P f)
all? P? with decFinSubset U? (λ {f} _ → P? f)
... | yes ∀p = yes (λ f → ∀p tt)
... | no ¬∀p = no  (λ ∀p → ¬∀p (λ _ → ∀p _))

-- If a decidable predicate P over a finite set is sometimes false,
-- then we can find the smallest value for which this is the case.

¬∀⟶∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
                 ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
¬∀⟶∃¬-smallest zero    P P? ¬∀P = contradiction (λ()) ¬∀P
¬∀⟶∃¬-smallest (suc n) P P? ¬∀P with P? zero
... | no ¬P₀ = (zero , ¬P₀ , λ ())
... | yes P₀ = map suc (map id (∀-cons P₀))
  (¬∀⟶∃¬-smallest n (P ∘ suc) (P? ∘ suc) (¬∀P ∘ (∀-cons P₀)))

-- When P is a decidable predicate over a finite set the following
-- lemma can be proved.

¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
          ¬ (∀ i → P i) → (∃ λ i → ¬ P i)
¬∀⟶∃¬ n P P? ¬P = map id proj₁ (¬∀⟶∃¬-smallest n P P? ¬P)

-- The pigeonhole principle.

pigeonhole : ∀ {m n} → m ℕ.< n → (f : Fin n → Fin m) →
             ∃₂ λ i j → i ≢ j × f i ≡ f j
pigeonhole (s≤s z≤n)       f = contradiction (f zero) λ()
pigeonhole (s≤s (s≤s m≤n)) f with any? (λ k → f zero ≟ f (suc k))
... | yes (j , f₀≡fⱼ) = zero , suc j , (λ()) , f₀≡fⱼ
... | no  f₀≢fₖ with pigeonhole (s≤s m≤n) (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
...   | (i , j , i≢j , fᵢ≡fⱼ) =
  suc i , suc j , i≢j ∘ suc-injective ,
  punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ

------------------------------------------------------------------------
-- Categorical

module _ {f} {F : Set f → Set f} (RA : RawApplicative F) where

  open RawApplicative RA

  sequence : ∀ {n} {P : Pred (Fin n) f} →
             (∀ i → F (P i)) → F (∀ i → P i)
  sequence {zero}  ∀iPi = pure λ()
  sequence {suc n} ∀iPi = ∀-cons <$> ∀iPi zero ⊛ sequence (∀iPi ∘ suc)

module _ {f} {F : Set f → Set f} (RF : RawFunctor F) where

  open RawFunctor RF

  sequence⁻¹ : ∀ {A : Set f} {P : Pred A f} →
               F (∀ i → P i) → (∀ i → F (P i))
  sequence⁻¹ F∀iPi i = (λ f → f i) <$> F∀iPi

------------------------------------------------------------------------
-- If there is an injection from a type to a finite set, then the type
-- has decidable equality.

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

  eq? : ∀ {n} → A ↣ Fin n → B.Decidable {A = A} _≡_
  eq? inj = Dec.via-injection inj _≟_

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

cmp              = <-cmp
{-# WARNING_ON_USAGE cmp
"Warning: cmp was deprecated in v0.15.
Please use <-cmp instead."
#-}
strictTotalOrder = <-strictTotalOrder
{-# WARNING_ON_USAGE strictTotalOrder
"Warning: strictTotalOrder was deprecated in v0.15.
Please use <-strictTotalOrder instead."
#-}

-- Version 0.16

to-from = toℕ-fromℕ
{-# WARNING_ON_USAGE to-from
"Warning: to-from was deprecated in v0.16.
Please use toℕ-fromℕ instead."
#-}
from-to          = fromℕ-toℕ
{-# WARNING_ON_USAGE from-to
"Warning: from-to was deprecated in v0.16.
Please use fromℕ-toℕ instead."
#-}
bounded = toℕ<n
{-# WARNING_ON_USAGE bounded
"Warning: bounded was deprecated in v0.16.
Please use toℕ<n instead."
#-}
prop-toℕ-≤ = toℕ≤pred[n]
{-# WARNING_ON_USAGE prop-toℕ-≤
"Warning: prop-toℕ-≤ was deprecated in v0.16.
Please use toℕ≤pred[n] instead."
#-}
prop-toℕ-≤′ = toℕ≤pred[n]′
{-# WARNING_ON_USAGE prop-toℕ-≤′
"Warning: prop-toℕ-≤′ was deprecated in v0.16.
Please use toℕ≤pred[n]′ instead."
#-}
inject-lemma = toℕ-inject
{-# WARNING_ON_USAGE inject-lemma
"Warning: inject-lemma was deprecated in v0.16.
Please use toℕ-inject instead."
#-}
inject+-lemma = toℕ-inject+
{-# WARNING_ON_USAGE inject+-lemma
"Warning: inject+-lemma was deprecated in v0.16.
Please use toℕ-inject+ instead."
#-}
inject₁-lemma = toℕ-inject₁
{-# WARNING_ON_USAGE inject₁-lemma
"Warning: inject₁-lemma was deprecated in v0.16.
Please use toℕ-inject₁ instead."
#-}
inject≤-lemma = toℕ-inject≤
{-# WARNING_ON_USAGE inject≤-lemma
"Warning: inject≤-lemma was deprecated in v0.16.
Please use toℕ-inject≤ instead."
#-}

-- Version 0.17

≤+≢⇒< = ≤∧≢⇒<
{-# WARNING_ON_USAGE ≤+≢⇒<
"Warning: ≤+≢⇒< was deprecated in v0.17.
Please use ≤∧≢⇒< instead."
#-}

-- Version 1.0

≤-irrelevance = ≤-irrelevant
{-# WARNING_ON_USAGE ≤-irrelevance
"Warning: ≤-irrelevance was deprecated in v1.0.
Please use ≤-irrelevant instead."
#-}
<-irrelevance = <-irrelevant
{-# WARNING_ON_USAGE <-irrelevance
"Warning: <-irrelevance was deprecated in v1.0.
Please use <-irrelevant instead."
#-}


text:
{-# OPTIONS --cubical #-}
open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Sigma

data S1 : Set where
  base : S1
  loop : base ≡ base

data Torus : Set where
  point : Torus
  line1 : point ≡ point
  line2 : point ≡ point
  square : PathP (λ i → line1 i ≡ line1 i) line2 line2

t2c : Torus → Σ S1 \ _ → S1
t2c point = ( base , base )
t2c (line1 i) = ( loop i , base )
t2c (line2 i) = ( base , loop i )
t2c (square i1 i2) = ( loop i1 , loop i2 )


text:
------------------------------------------------------------------------------
-- Issue in the translation
------------------------------------------------------------------------------

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

module Issue10 where

postulate
  D  : Set
  P' : D → Set

postulate foo : ∀ d → P' d → P' d
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
open import Agda.Primitive
open import Agda.Builtin.Nat

Type : (i : Level) -> Set (lsuc i)
Type i = Set i

postulate
  P : (i : Level) (A : Type i) → A → Type i

postulate
  lemma : (a : Nat) -> P _ _ a

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.ListedFiniteSet.Properties where

open import Cubical.Foundations.Prelude

open import Cubical.HITs.ListedFiniteSet.Base

private
  variable
    A : Type₀

_++_ : ∀ (xs ys : LFSet A) → LFSet A
[]                  ++ ys = ys
(x ∷ xs)            ++ ys = x ∷ (xs ++ ys)
---------------------------------------------
dup x xs i          ++ ys = proof i
   where
     proof :
     -- Need:  (x ∷ x ∷ xs) ++ ys ≡ (x ∷ xs) ++ ys
     -- which reduces to:
               x ∷ x ∷ (xs ++ ys) ≡ x ∷ (xs ++ ys)
     proof = dup x (xs ++ ys)
comm x y xs i       ++ ys = comm x y (xs ++ ys) i
trunc xs zs p q i j ++ ys
  = trunc (xs ++ ys) (zs ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j

assoc-++ : ∀ (xs : LFSet A) ys zs → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
assoc-++ []       ys zs = refl
assoc-++ (x ∷ xs) ys zs
  = cong (x ∷_) (assoc-++ xs ys zs)
------------------------------------
assoc-++ (dup x xs i) ys zs j
  = dup x (assoc-++ xs ys zs j) i
assoc-++ (comm x y xs i) ys zs j
  = comm x y (assoc-++ xs ys zs j) i
assoc-++ (trunc xs xs' p q i k) ys zs j
  = trunc (assoc-++ xs ys zs j) (assoc-++ xs' ys zs j)
          (cong (\ xs -> assoc-++ xs ys zs j) p) (cong (\ xs -> assoc-++ xs ys zs j) q) i k

max_stars_repo_name: mchristianl/cubical

max_issues_repo_name: mchristianl/cubical

max_forks_repo_name: aljungstrom/cubical