text:
------------------------------------------------------------------------
-- Strict ω-continuous functions
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

module Partiality-algebra.Strict-omega-continuous where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J hiding (_∘_)
open import H-level.Closure equality-with-J
open import Monad equality-with-J

open import Partiality-algebra as PA
open import Partiality-algebra.Monotone
open import Partiality-algebra.Omega-continuous

-- Definition of strict ω-continuous functions.

record [_⟶_]⊥
         {a₁ p₁ q₁} {A₁ : Type a₁} (P₁ : Partiality-algebra p₁ q₁ A₁)
         {a₂ p₂ q₂} {A₂ : Type a₂} (P₂ : Partiality-algebra p₂ q₂ A₂) :
         Type (p₁ ⊔ p₂ ⊔ q₁ ⊔ q₂) where
  private
    module P₁ = Partiality-algebra P₁
    module P₂ = Partiality-algebra P₂

  field
    ω-continuous-function : [ P₁ ⟶ P₂ ]

  open [_⟶_] ω-continuous-function public

  field
    strict : function P₁.never ≡ P₂.never

open [_⟶_]⊥

-- Identity.

id⊥ : ∀ {a p q} {A : Type a} {P : Partiality-algebra p q A} →
      [ P ⟶ P ]⊥
ω-continuous-function id⊥ = idω
strict                id⊥ = refl

-- Composition.

infixr 40 _∘⊥_

_∘⊥_ :
  ∀ {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
    {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂}
    {a₃ p₃ q₃} {A₃ : Type a₃} {P₃ : Partiality-algebra p₃ q₃ A₃} →
  [ P₂ ⟶ P₃ ]⊥ → [ P₁ ⟶ P₂ ]⊥ → [ P₁ ⟶ P₃ ]⊥
ω-continuous-function (f ∘⊥ g) =
  ω-continuous-function f ∘ω ω-continuous-function g

strict (_∘⊥_ {P₁ = P₁} {P₂ = P₂} {P₃ = P₃} f g) =
  function f (function g P₁.never)  ≡⟨ cong (function f) (strict g) ⟩
  function f P₂.never               ≡⟨ strict f ⟩∎
  P₃.never                          ∎
  where
  module P₁ = Partiality-algebra P₁
  module P₂ = Partiality-algebra P₂
  module P₃ = Partiality-algebra P₃

-- Equality characterisation lemma for strict ω-continuous functions.

equality-characterisation-strict :
  ∀ {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
    {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂}
    {f g : [ P₁ ⟶ P₂ ]⊥} →
  (∀ x → function f x ≡ function g x) ↔ f ≡ g
equality-characterisation-strict {P₁ = P₁} {P₂ = P₂} {f} {g} =
  (∀ x → function f x ≡ function g x)                ↝⟨ equality-characterisation-continuous ⟩
  ω-continuous-function f ≡ ω-continuous-function g  ↝⟨ ignore-propositional-component P₂.T-is-set ⟩
  _↔_.to rearrange f ≡ _↔_.to rearrange g            ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ rearrange) ⟩□
  f ≡ g                                              □
  where
  module P₁ = Partiality-algebra P₁
  module P₂ = Partiality-algebra P₂

  rearrange :
    [ P₁ ⟶ P₂ ]⊥
      ↔
    ∃ λ (h : [ P₁ ⟶ P₂ ]) → [_⟶_].function h P₁.never ≡ P₂.never
  rearrange = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ f → ω-continuous-function f , strict f
        ; from = uncurry λ f c → record { ω-continuous-function = f
                                        ; strict                = c
                                        }
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    }
    where
    open Partiality-algebra

-- Composition is associative.

∘⊥-assoc :
  ∀ {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
    {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂}
    {a₃ p₃ q₃} {A₃ : Type a₃} {P₃ : Partiality-algebra p₃ q₃ A₃}
    {a₄ p₄ q₄} {A₄ : Type a₄} {P₄ : Partiality-algebra p₄ q₄ A₄}
  (f : [ P₃ ⟶ P₄ ]⊥) (g : [ P₂ ⟶ P₃ ]⊥) (h : [ P₁ ⟶ P₂ ]⊥) →
  f ∘⊥ (g ∘⊥ h) ≡ (f ∘⊥ g) ∘⊥ h
∘⊥-assoc _ _ _ =
  _↔_.to equality-characterisation-strict λ _ → refl

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
open import FRP.LTL.Time using ( Time ; _,_ )
open import FRP.LTL.Time.Bound using
  ( Time∞ ; _≼_ ; _≺_ ; fin ; +∞ ; +∞-top ; t≺+∞ ; ≼-refl ; _≼-trans_
  ; ≡-impl-≼ ; ≺-impl-≼ ; _≺-trans_ ; _≺-transʳ_ ; ≺-impl-⋡ ; t≺t+1 )
open import FRP.LTL.Util using ( irrelevant ; ⊥-elim )
open import Relation.Unary using ( _∈_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym )

module FRP.LTL.Time.Interval where

infixr 2 _⊑_ _~_
infixr 4 _,_ _⌢_∵_

-- Semi-open intervals, with possibly infinite bounds

-- Previous versions of Interval used ≼ rather than ≺
-- (that is, empty intervals were supported) but
-- MSet has been written to avoid requiring empty intervals.

data Interval : Set where
  [_⟩ : ∀ {s t} → .(s ≺ t) → Interval

lb : Interval → Time∞
lb ([_⟩ {s} {t} s≺t) = s

ub : Interval → Time∞
ub ([_⟩ {s} {t} s≺t) = t

.lb≺ub : ∀ i → (lb i ≺ ub i)
lb≺ub [ s≺t ⟩ = irrelevant s≺t

-- Semantics of intervals

data Int∞ (i : Interval) (t : Time∞) : Set where
  _,_ : .(lb i ≼ t) → .(t ≺ ub i) → (t ∈ Int∞ i)

Int : Interval → Time → Set
Int i t = fin t ∈ Int∞ i

.lb≼ : ∀ {t i} → (t ∈ Int i) → (lb i ≼ fin t)
lb≼ (s≼t , t≺u) = irrelevant s≼t

.≺ub : ∀ {t i} → (t ∈ Int i) → (fin t ≺ ub i)
≺ub (s≼t , t≺u) = irrelevant t≺u

-- Ordering on intervals

data _⊑_ (i j : Interval) : Set where
  _,_ : .(lb j ≼ lb i) → .(ub i ≼ ub j) → (i ⊑ j)

⊑-refl : ∀ {i} → (i ⊑ i)
⊑-refl = (≼-refl , ≼-refl)

_⊑-trans_ : ∀ {i j k} → (i ⊑ j) → (j ⊑ k) → (i ⊑ k)
(sj≼si , ui≼uj) ⊑-trans (sk≼sj , uj≼uk) =
  (sk≼sj ≼-trans sj≼si , ui≼uj ≼-trans uj≼uk)

.⊑-impl-≼ : ∀ {i j} → (i ⊑ j) → (ub i ≼ ub j)
⊑-impl-≼ (lj≼li , ui≼uj) = irrelevant ui≼uj

.⊑-impl-≽ : ∀ {i j} → (i ⊑ j) → (lb j ≼ lb i)
⊑-impl-≽ (lj≼li , ui≼uj) = irrelevant lj≼li

-- When do two intervals abut?

_~_ : Interval → Interval → Set
i ~ j = ub i ≡ lb j

-- Concatenation of intervals

_⌢_∵_ : ∀ i j → (i ~ j) → Interval
i ⌢ j ∵ i~j = [ lb≺ub i ≺-trans ≡-impl-≼ i~j ≺-transʳ lb≺ub j ⟩

⌢-inj₁ : ∀ i j i~j → (i ⊑ (i ⌢ j ∵ i~j))
⌢-inj₁ [ s≺t ⟩ [ t≺u ⟩ refl = (≼-refl , ≺-impl-≼ t≺u)

⌢-inj₂ : ∀ i j i~j → (j ⊑ (i ⌢ j ∵ i~j))
⌢-inj₂ [ s≺t ⟩ [ t≺u ⟩ refl = (≺-impl-≼ s≺t , ≼-refl)

-- Up-closure of a time

↑ : Time → Interval
↑ t = [ t≺+∞ {t} ⟩

-- Singleton interval

sing : Time → Interval
sing t = [ t≺t+1 {t} ⟩

ext: agda

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
------------------------------------------------------------------------
-- Laws related to _>>=_
------------------------------------------------------------------------

module TotalParserCombinators.Laws.Monad where

open import Algebra
open import Category.Monad
open import Codata.Musical.Notation
open import Data.List
open import Data.List.Categorical
  using () renaming (module MonadProperties to ListMonad)
import Data.List.Relation.Binary.BagAndSetEquality as BSEq
open import Function
open import Level

private
  module BagMonoid {k} {A : Set} =
    CommutativeMonoid (BSEq.commutativeMonoid k A)
  open RawMonad {f = zero} Data.List.Categorical.monad
    using () renaming (_>>=_ to _>>=′_)

open import TotalParserCombinators.Derivative
open import TotalParserCombinators.Congruence as Eq
  hiding (return; fail) renaming (_∣_ to _∣′_)
import TotalParserCombinators.Laws.AdditiveMonoid as AdditiveMonoid
open import TotalParserCombinators.Laws.Derivative as Derivative
open import TotalParserCombinators.Laws.ReturnStar as Return⋆
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- _>>=_, return, _∣_ and fail form a monad with a zero and a plus

-- If the laws below are combined with the additive monoid laws this
-- means that we have something which resembles an idempotent semiring
-- (if we restrict ourselves to language equivalence).

-- The zero laws are proved elsewhere.

open Derivative public
  using () renaming (left-zero->>=  to left-zero;
                     right-zero->>= to right-zero)

left-distributive : ∀ {Tok R₁ R₂ xs} {f g : R₁ → List R₂}
                    (p₁ : Parser Tok R₁ xs)
                    (p₂ : (x : R₁) → Parser Tok R₂ (f x))
                    (p₃ : (x : R₁) → Parser Tok R₂ (g x)) →
                    p₁ >>= (λ x → p₂ x ∣ p₃ x) ≅P p₁ >>= p₂ ∣ p₁ >>= p₃
left-distributive {xs = xs} {f} {g} p₁ p₂ p₃ =
  BSEq.>>=-left-distributive xs {f = f} ∷ λ t → ♯ (
    D t (p₁ >>= (λ x → p₂ x ∣ p₃ x))                       ≅⟨ D->>= p₁ (λ x → p₂ x ∣ p₃ x) ⟩

    D t p₁ >>= (λ x → p₂ x ∣ p₃ x) ∣
    return⋆ xs >>= (λ x → D t (p₂ x) ∣ D t (p₃ x))         ≅⟨ left-distributive (D t p₁) p₂ p₃ ∣′
                                                              left-distributive (return⋆ xs)
                                                                (λ x → D t (p₂ x)) (λ x → D t (p₃ x)) ⟩
    (D t p₁ >>= p₂ ∣ D t p₁ >>= p₃) ∣
    (return⋆ xs >>= (λ x → D t (p₂ x)) ∣
     return⋆ xs >>= (λ x → D t (p₃ x)))                    ≅⟨ AdditiveMonoid.swap
                                                               (D t p₁ >>= p₂) (D t p₁ >>= p₃)
                                                               (return⋆ xs >>= (λ x → D t (p₂ x)))
                                                               (return⋆ xs >>= (λ x → D t (p₃ x))) ⟩
    (D t p₁ >>= p₂ ∣ return⋆ xs >>= (λ x → D t (p₂ x))) ∣
    (D t p₁ >>= p₃ ∣ return⋆ xs >>= (λ x → D t (p₃ x)))    ≅⟨ sym (D->>= p₁ p₂ ∣′ D->>= p₁ p₃) ⟩

    D t (p₁ >>= p₂) ∣ D t (p₁ >>= p₃)                      ∎)

right-distributive : ∀ {Tok R₁ R₂ xs₁ xs₂} {f : R₁ → List R₂}
                     (p₁ : Parser Tok R₁ xs₁)
                     (p₂ : Parser Tok R₁ xs₂)
                     (p₃ : (x : R₁) → Parser Tok R₂ (f x)) →
                     (p₁ ∣ p₂) >>= p₃ ≅P p₁ >>= p₃ ∣ p₂ >>= p₃
right-distributive {xs₁ = xs₁} {xs₂} {f} p₁ p₂ p₃ =
  BagMonoid.reflexive (ListMonad.right-distributive xs₁ xs₂ f) ∷ λ t → ♯ (
    D t ((p₁ ∣ p₂) >>= p₃)                                  ≅⟨ D->>= (p₁ ∣ p₂) p₃ ⟩

    (D t p₁ ∣ D t p₂) >>= p₃ ∣
    return⋆ (xs₁ ++ xs₂) >>= (λ x → D t (p₃ x))             ≅⟨ ((D t p₁ ∣ D t p₂) >>= p₃ ∎) ∣′
                                                               [ ○ - ○ - ○ - ○ ] Return⋆.distrib-∣ xs₁ xs₂ >>=
                                                                                (λ x → D t (p₃ x) ∎) ⟩
    (D t p₁ ∣ D t p₂) >>= p₃ ∣
    (return⋆ xs₁ ∣ return⋆ xs₂) >>= (λ x → D t (p₃ x))      ≅⟨ right-distributive (D t p₁) (D t p₂) p₃ ∣′
                                                               right-distributive (return⋆ xs₁) (return⋆ xs₂)
                                                                                (λ x → D t (p₃ x)) ⟩
    ((D t p₁ >>= p₃) ∣ (D t p₂ >>= p₃)) ∣
    (return⋆ xs₁ >>= (λ x → D t (p₃ x)) ∣
     return⋆ xs₂ >>= (λ x → D t (p₃ x)))                    ≅⟨ AdditiveMonoid.swap
                                                                 (D t p₁ >>= p₃) (D t p₂ >>= p₃)
                                                                 (return⋆ xs₁ >>= (λ x → D t (p₃ x)))
                                                                 (return⋆ xs₂ >>= (λ x → D t (p₃ x))) ⟩
    (D t p₁ >>= p₃ ∣ return⋆ xs₁ >>= (λ x → D t (p₃ x))) ∣
    (D t p₂ >>= p₃ ∣ return⋆ xs₂ >>= (λ x → D t (p₃ x)))    ≅⟨ sym (D->>= p₁ p₃ ∣′ D->>= p₂ p₃) ⟩

    D t (p₁ >>= p₃) ∣ D t (p₂ >>= p₃)                       ∎)

left-identity : ∀ {Tok R₁ R₂} {f : R₁ → List R₂}
                (x : R₁) (p : (x : R₁) → Parser Tok R₂ (f x)) →
                return x >>= p ≅P p x
left-identity {f = f} x p =
  BagMonoid.reflexive (ListMonad.left-identity x f) ∷ λ t → ♯ (
    D t (return x >>= p)                              ≅⟨ D->>= (return x) p ⟩
    fail >>= p ∣ return⋆ [ x ] >>= (λ x → D t (p x))  ≅⟨ left-zero p ∣′
                                                         [ ○ - ○ - ○ - ○ ] AdditiveMonoid.right-identity (return x) >>=
                                                                           (λ x → D t (p x) ∎) ⟩
    fail ∣ return x >>= (λ x → D t (p x))             ≅⟨ AdditiveMonoid.left-identity (return x >>= (λ x → D t (p x))) ⟩
    return x >>= (λ x → D t (p x))                    ≅⟨ left-identity x (λ x → D t (p x)) ⟩
    D t (p x)                                         ∎)

right-identity : ∀ {Tok R xs}
                 (p : Parser Tok R xs) → p >>= return ≅P p
right-identity {xs = xs} p =
  BagMonoid.reflexive (ListMonad.right-identity xs) ∷ λ t → ♯ (
    D t (p >>= return)                              ≅⟨ D->>= p return ⟩
    D t p >>= return ∣ return⋆ xs >>= (λ _ → fail)  ≅⟨ right-identity (D t p) ∣′ right-zero (return⋆ xs) ⟩
    D t p            ∣ fail                         ≅⟨ AdditiveMonoid.right-identity (D t p) ⟩
    D t p                                           ∎)

associative : ∀ {Tok R₁ R₂ R₃ xs}
                {f : R₁ → List R₂} {g : R₂ → List R₃}
              (p₁ : Parser Tok R₁ xs)
              (p₂ : (x : R₁) → Parser Tok R₂ (f x))
              (p₃ : (x : R₂) → Parser Tok R₃ (g x)) →
              p₁ >>= (λ x → p₂ x >>= p₃) ≅P p₁ >>= p₂ >>= p₃
associative {xs = xs} {f} {g} p₁ p₂ p₃ =
  BagMonoid.reflexive (ListMonad.associative xs f g) ∷ λ t → ♯ (
    D t (p₁ >>= λ x → p₂ x >>= p₃)                               ≅⟨ D->>= p₁ (λ x → p₂ x >>= p₃) ⟩

    D t p₁ >>= (λ x → p₂ x >>= p₃) ∣
    return⋆ xs >>= (λ x → D t (p₂ x >>= p₃))                     ≅⟨ associative (D t p₁) p₂ p₃ ∣′
                                                                    [ ○ - ○ - ○ - ○ ] return⋆ xs ∎ >>= (λ x → D->>= (p₂ x) p₃) ⟩
    D t p₁ >>= p₂ >>= p₃ ∣
    return⋆ xs >>=
      (λ x → D t (p₂ x) >>= p₃ ∣
             return⋆ (f x) >>= λ x → D t (p₃ x))                 ≅⟨ (D t p₁ >>= p₂ >>= p₃ ∎) ∣′
                                                                    left-distributive (return⋆ xs)
                                                                                (λ x → D t (p₂ x) >>= p₃)
                                                                                (λ x → return⋆ (f x) >>= (λ x → D t (p₃ x))) ⟩
    D t p₁ >>= p₂ >>= p₃ ∣
    (return⋆ xs >>= (λ x → D t (p₂ x) >>= p₃) ∣
     return⋆ xs >>= (λ x → return⋆ (f x) >>= λ x → D t (p₃ x)))  ≅⟨ (D t p₁ >>= p₂ >>= p₃ ∎) ∣′
                                                                    (associative (return⋆ xs) (λ x → D t (p₂ x)) p₃ ∣′
                                                                     associative (return⋆ xs) (return⋆ ∘ f) (λ x → D t (p₃ x))) ⟩
    D t p₁ >>= p₂ >>= p₃ ∣
    (return⋆ xs >>= (λ x → D t (p₂ x)) >>= p₃ ∣
     return⋆ xs >>= (return⋆ ∘ f) >>= λ x → D t (p₃ x))          ≅⟨ sym $ AdditiveMonoid.associative
                                                                            (D t p₁ >>= p₂ >>= p₃)
                                                                            (return⋆ xs >>= (λ x → D t (p₂ x)) >>= p₃)
                                                                            (return⋆ xs >>= (return⋆ ∘ f) >>= (λ x → D t (p₃ x))) ⟩
    D t p₁ >>= p₂ >>= p₃ ∣
    return⋆ xs >>= (λ x → D t (p₂ x)) >>= p₃ ∣
    return⋆ xs >>= (return⋆ ∘ f) >>= (λ x → D t (p₃ x))          ≅⟨ sym (right-distributive
                                                                           (D t p₁ >>= p₂)
                                                                           (return⋆ xs >>= (λ x → D t (p₂ x)))
                                                                           p₃) ∣′
                                                                    [ ○ - ○ - ○ - ○ ] sym (Return⋆.distrib->>= xs f) >>=
                                                                                (λ x → D t (p₃ x) ∎) ⟩
    (D t p₁ >>= p₂ ∣
     return⋆ xs >>= (λ x → D t (p₂ x))) >>= p₃ ∣
    return⋆ (xs >>=′ f) >>= (λ x → D t (p₃ x))                   ≅⟨ [ ○ - ○ - ○ - ○ ] sym (D->>= p₁ p₂) >>= (λ x → p₃ x ∎) ∣′
                                                                    (return⋆ (xs >>=′ f) >>= (λ x → D t (p₃ x)) ∎) ⟩
    D t (p₁ >>= p₂) >>= p₃ ∣
    return⋆ (xs >>=′ f) >>= (λ x → D t (p₃ x))                   ≅⟨ sym $ D->>= (p₁ >>= p₂) p₃ ⟩

    D t (p₁ >>= p₂ >>= p₃)                                       ∎)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --cubical --no-import-sorts  #-}

module MoreAlgebra where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)

open import Utils

hPropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
hPropRel A B ℓ' = A → B → hProp ℓ'

module Definitions where
  -- NOTE: one needs these "all-lowercase constructors" to make use of copatterns

  _Preserves_⟶_ : ∀{Aℓ Bℓ ℓ ℓ'} {A : Type Aℓ} {B : Type Bℓ} → (A → B) → Rel A A ℓ → Rel B B ℓ' → Set _
  f Preserves P ⟶ Q = ∀{x y} → P x y → Q (f x) (f y)

  _Reflects_⟶_ : ∀{Aℓ Bℓ ℓ ℓ'} {A : Type Aℓ} {B : Type Bℓ} → (A → B) → Rel A A ℓ → Rel B B ℓ' → Set _
  f Reflects P ⟶ Q = ∀{x y} → Q (f x) (f y) → P x y

  -- https://en.wikipedia.org/wiki/Complete_partial_order
  --   A partially ordered set is a directed-complete partial order (dcpo) if each of its directed subsets has a supremum.
  --   A subset of a partial order is directed if it is non-empty and every pair of elements has an upper bound in the subset.
  --   In the literature, dcpos sometimes also appear under the label up-complete poset.

  -- https://ncatlab.org/nlab/show/dcpo
  --   A DCPO, or directed-complete partial order, is a poset with all directed joins.
  --   Often a DCPO is required to have a bottom element ⊥\bot; then it is called a pointed DCPO or a CPO (but this term is ambiguous).

  -- In this chapter we develop the theory of directed-complete partial orders (dcpo), namely
  -- partially ordered sets in which only certain joins are required to exist.
  --
  -- ...
  --
  -- 3.1 Dcpos
  --
  -- We start by defining partial orders. By a binary relation R on a set X , we mean a map X → X → HProp, as in Definition 2.7.1.
  -- We can specify which universe the binary relation lands in by saying that R is HPropᵢ-valued or is a relation in universe i if R : X → X → HPropᵢ.
  --
  -- Definition 3.1.1. A binary relation R on a set X is
  --
  -- 1. reflexive     if (∀ x       : X)   R x x;
  -- 2. irreflexive   if (∀ x       : X) ¬ R x x;
  -- 3. symmetric     if (∀ x, y    : X)   R x y ⇒ R y x;
  -- 4. antisymmetric if (∀ x, y    : X)   R x y ⇒ R y x ⇒ x = y;
  -- 5. transitive    if (∀ x, y, z : X)   R x y ⇒ R y z ⇒ R x z;
  -- 6. cotransitive  if (∀ x, y, z : X)   R x y ⇒ (R x z) ∨ (R z y).
  --
  -- Remark 3.1.2. Cotransitivity is also known as weak linearity [91, Definition 11.2.7] or the approximate splitting principle [84].
  --
  -- Definition 3.1.3.
  --
  -- A preorder, denoted by ≤, is a reflexive transitive relation.
  -- A partial order is an antisymmetric preorder.

  -- Definition 4.1.4.
  -- - An apartness relation, denoted by #, is an irreflexive symmetric cotransitive relation.
  -- - A strict partial order, denoted by <, is an irreflexive transitive cotransitive relation.

  IsIrrefl : {ℓ ℓ' : Level} {A : Type ℓ} → (R : Rel A A ℓ') → Type (ℓ-max ℓ ℓ')
  IsIrrefl {A = A} R = (a : A) → ¬(R a a)

  IsCotrans : {ℓ ℓ' : Level} {A : Type ℓ} → (R : Rel A A ℓ') → Type (ℓ-max ℓ ℓ')
  IsCotrans {A = A} R = (a b : A) → R a b → (∀(x : A) → (R a x) ⊎ (R x b))

  -- NOTE: see Cubical.Algebra.Poset
  IsSymᵖ : {ℓ ℓ' : Level} {A : Type ℓ} → (R : hPropRel A A ℓ') → Type (ℓ-max ℓ ℓ')
  IsSymᵖ {A = A} R = (a b : A) → [ R a b ] → [ R b a ]

  IsIrreflᵖ : {ℓ ℓ' : Level} {A : Type ℓ} → (R : hPropRel A A ℓ') → Type (ℓ-max ℓ ℓ')
  IsIrreflᵖ {A = A} R = (a : A) → [ ¬ᵖ(R a a) ]

  IsCotransᵖ : {ℓ ℓ' : Level} {A : Type ℓ} → (R : hPropRel A A ℓ') → Type (ℓ-max ℓ ℓ')
  IsCotransᵖ {A = A} R = (a b : A) → [ R a b ] → (∀(x : A) → [ (R a x) ⊔ (R x b) ])

  {- NOTE: formulating the properties on witnesses with `[_]` is similar to the previous Propositions-as-types formalism
           but it is not the way to proceed with hProps
           the idea is, to produce an hProp again
           e.g. from `Cubical.Algebra.Poset`
             isTransitive : {A : Type ℓ₀} → Order ℓ₁ A → hProp (ℓ-max ℓ₀ ℓ₁)
             isTransitive {ℓ₀ = ℓ₀} {ℓ₁ = ℓ₁} {A = X} _⊑_ = φ , φ-prop
               where
                 φ      : Type (ℓ-max ℓ₀ ℓ₁)
                 φ      = ((x y z : X) → [ x ⊑ y ⇒ y ⊑ z ⇒ x ⊑ z ])
                 φ-prop : isProp φ
                 φ-prop = isPropΠ3 λ x y z → snd (x ⊑ y ⇒ y ⊑ z ⇒ x ⊑ z)
  -}
  IsTransᵖ : {ℓ ℓ' : Level} {A : Type ℓ} → (R : hPropRel A A ℓ') → Type (ℓ-max ℓ ℓ')
  IsTransᵖ {A = A} R = (a b c : A)  → [ R a b ] → [ R b c ] → [ R a c ]

  -- NOTE: this is starting with a lower-case, because `hProp (ℓ-max ℓ ℓ')` is not a type but an element
  isTransᵖ : {ℓ ℓ' : Level} {A : Type ℓ} → (R : hPropRel A A ℓ') → hProp (ℓ-max ℓ ℓ')
  isTransᵖ {ℓ} {ℓ'} {A = A} R = φ , φ-prop
    where
      φ : Type (ℓ-max ℓ ℓ')
      φ = (a b c : A) → [ R a b ⇒ R b c ⇒ R a c ]
      φ-prop : isProp φ
      φ-prop = isPropΠ3 λ a b c → snd (R a b ⇒ R b c ⇒ R a c)

  isIrreflᵖ : {ℓ ℓ' : Level} {A : Type ℓ} → (R : hPropRel A A ℓ') → hProp (ℓ-max ℓ ℓ')
  isIrreflᵖ {ℓ} {ℓ'} {A = A} R = φ , φ-prop
    where
      φ : Type (ℓ-max ℓ ℓ')
      φ = (a : A) → [ ¬ᵖ (R a a) ]
      φ-prop : isProp φ
      φ-prop = isPropΠ λ a → snd (¬ᵖ (R a a))

  isCotransᵖ : {ℓ ℓ' : Level} {A : Type ℓ} → (R : hPropRel A A ℓ') → hProp (ℓ-max ℓ ℓ')
  isCotransᵖ {ℓ} {ℓ'} {A = A} R = φ , φ-prop
    where
      φ : Type (ℓ-max ℓ ℓ')
      φ = (a b : A) → [ R a b ⇒ (∀[ x ∶ A ] (R a x) ⊔ (R x b)) ]
      φ-prop : isProp φ
      φ-prop = isPropΠ2 λ a b → snd (R a b ⇒ (∀[ x ∶ A ] (R a x) ⊔ (R x b)))

  record IsApartnessRel {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') : Type (ℓ-max ℓ ℓ') where
    field
      isIrrefl  : IsIrrefl R
      isSym     : BinaryRelation.isSym R
      isCotrans : IsCotrans R

  record IsApartnessRelᵖ {ℓ ℓ' : Level} {A : Type ℓ} (R : hPropRel A A ℓ') : Type (ℓ-max ℓ ℓ') where
    field
      isIrrefl  : IsIrreflᵖ R
      isSym     : IsSymᵖ R
      isCotrans : IsCotransᵖ R

  record IsStrictPartialOrder {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') : Type (ℓ-max ℓ ℓ') where
    constructor isstrictpartialorder
    field
      isIrrefl  : IsIrrefl R
      isTrans   : BinaryRelation.isTrans R
      isCotrans : IsCotrans R

  record IsStrictPartialOrderᵖ {ℓ ℓ' : Level} {A : Type ℓ} (R : hPropRel A A ℓ') : Type (ℓ-max ℓ ℓ') where
    constructor isstrictpartialorderᵖ
    field
      isIrrefl  : IsIrreflᵖ R
      isTrans   : IsTransᵖ R
      isCotrans : IsCotransᵖ R

  {- NOTE: here again, the previous-way-interpretation would be to put witnesses into the struct with `[_]`
           but with hProps, we would have `isStrictPartialOrder : hProp`
           and use `[ isStrictPartialOrder ]` as the witness type
           with hProps we would need to make heavy use of `Cubical.Foundations.HLevels`
             isProp×, isProp×2, isProp×3
           to show the record's `isProp`
           do we have pathes on records? in order to use `isProp` on records?
             yes, with record constructors
  -}
  record [IsStrictPartialOrder] {ℓ ℓ' : Level} {A : Type ℓ} (R : hPropRel A A ℓ') : Type (ℓ-max ℓ ℓ') where
    constructor isstrictpartialorderᵖ
    field
      isIrrefl  : [ isIrreflᵖ  R ]
      isTrans   : [ isTransᵖ   R ]
      isCotrans : [ isCotransᵖ R ]

  isStrictParialOrder : {ℓ ℓ' : Level} {A : Type ℓ} (R : hPropRel A A ℓ') → hProp (ℓ-max ℓ ℓ')
  isStrictParialOrder R = [IsStrictPartialOrder] R , φ-prop where
    φ-prop :      isProp ([IsStrictPartialOrder] R)
    φ-prop (isstrictpartialorderᵖ isIrrefl₀ isTrans₀ isCotrans₀)
           (isstrictpartialorderᵖ isIrrefl₁ isTrans₁ isCotrans₁) =
      λ i → isstrictpartialorderᵖ (isProp[] (isIrreflᵖ  R) isIrrefl₀  isIrrefl₁  i)
                                  (isProp[] (isTransᵖ   R) isTrans₀   isTrans₁   i)
                                  (isProp[] (isCotransᵖ R) isCotrans₀ isCotrans₁ i)

  record IsPreorder {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') : Type (ℓ-max ℓ ℓ') where
    constructor ispreorder
    field
      isRefl    : BinaryRelation.isRefl R
      isTrans   : BinaryRelation.isTrans R

  -- NOTE: there is already
  --       isAntisym : {A : Type ℓ₀} → isSet A → Order ℓ₁ A → hProp (ℓ-max ℓ₀ ℓ₁)
  --       in Cubical.Algebra.Poset. Can we use this?
  -- import Cubical.Algebra.Poset

  IsAntisym : {ℓ ℓ' : Level} {A : Type ℓ} → (R : Rel A A ℓ') → Type (ℓ-max ℓ ℓ')
  IsAntisym {A = A} R = ∀ a b → R a b → R b a → a ≡ b

  record IsPartialOrder {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') : Type (ℓ-max ℓ ℓ') where
    constructor ispartialorder
    field
      isRefl    : BinaryRelation.isRefl R
      isAntisym : IsAntisym R
      isTrans   : BinaryRelation.isTrans R

  _#'_ : ∀{X : Type ℓ} {_<_ : Rel X X ℓ'} → Rel X X ℓ'
  _#'_ {_<_ = _<_} x y = (x < y) ⊎ (y < x)

  _≤'_ : ∀{X : Type ℓ} {_<_ : Rel X X ℓ'} → Rel X X ℓ'
  _≤'_ {_<_ = _<_} x y = ¬ (y < x)

-- NOTE: there is `Properties` and `Consequences`
--       the difference somehow is, that we do want to open `Consequences` directly
--       but we do not want to open `Properties` directly, because it might have a name clash
--       e.g. there is `Properties.Group` which clashes with `Cubical.Algebra.Group.Group` when opening `Properties`
--       but it is totally fine to open `Properties.Group` directly because it does not export a `Group`
-- TODO: check whether this matches the wording of the (old) standard library
module Consequences where
  open Definitions

  -- Lemma 4.1.7.
  -- Given a strict partial order < on a set X:
  -- 1. we have an apartness relation defined by
  --    x # y := (x < y) ∨ (y < x), and

  #'-isApartnessRel : ∀{X : Type ℓ} {_<_ : Rel X X ℓ'} → (isSPO : IsStrictPartialOrder _<_) → IsApartnessRel (_#'_ {_<_ = _<_})
  #'-isApartnessRel {X = X} {_<_ = _<_} isSPO =
    let (isstrictpartialorder <-irrefl <-trans <-cotrans) = isSPO
    in λ where
      .IsApartnessRel.isIrrefl a (inl a<a) → <-irrefl _ a<a
      .IsApartnessRel.isIrrefl a (inr a<a) → <-irrefl _ a<a
      .IsApartnessRel.isSym    a b p → ⊎-swap p
      .IsApartnessRel.isCotrans a b (inl a<b) x → case (<-cotrans _ _ a<b x) of λ where -- case x of f = f x
        (inl a<x) → inl (inl a<x)
        (inr x<b) → inr (inl x<b)
      .IsApartnessRel.isCotrans a b (inr b<a) x → case (<-cotrans _ _ b<a x) of λ where
        (inl b<x) → inr (inr b<x)
        (inr x<a) → inl (inr x<a)

  -- variant without copatterns: "just" move the `λ where` "into" the record
  #'-isApartnessRel' : ∀{X : Type ℓ} {_<_ : Rel X X ℓ'} → {IsStrictPartialOrder _<_} → IsApartnessRel (_#'_ {_<_ = _<_})
  #'-isApartnessRel' {X = X} {_<_ = _<_} {isSPO} =
    let (isstrictpartialorder <-irrefl <-trans <-cotrans) = isSPO
    in record
      { isIrrefl  = λ where a (inl a<a) → <-irrefl _ a<a
                            a (inr a<a) → <-irrefl _ a<a
      ; isSym     = λ where a b p → ⊎-swap p
      ; isCotrans = λ where
        a b (inl a<b) x → case (<-cotrans _ _ a<b x) of λ where
          (inl a<x) → inl (inl a<x)
          (inr x<b) → inr (inl x<b)
        a b (inr b<a) x → case (<-cotrans _ _ b<a x) of λ where
          (inl b<x) → inr (inr b<x)
          (inr x<a) → inl (inr x<a)
      }

  -- 2. we have a preorder defined by
  --    x ≤ y := ¬(y < x).

  ≤-isPreorder' : ∀{X : Type ℓ} {_<_ : Rel X X ℓ'} → {IsStrictPartialOrder _<_} → IsPreorder (_≤'_ {_<_ = _<_})
  ≤-isPreorder' {X = X} {_<_ = _<_} {isSPO} =
    let (isstrictpartialorder <-irrefl <-trans <-cotrans) = isSPO
    in λ where
     .IsPreorder.isRefl → <-irrefl
     .IsPreorder.isTrans a b c ¬b<a ¬c<b c<a → case (<-cotrans _ _ c<a b) of λ where
       (inl c<b) → ¬c<b c<b
       (inr b<a) → ¬b<a b<a

  module _
    {X : Type ℓ} (_<_ : Rel X X ℓ')
    (isSPO : IsStrictPartialOrder _<_)
    (<-isProp : ∀ x y → isProp (x < y))
    (let _#_ = _#'_ {_<_ = _<_})
    (let (isstrictpartialorder <-irrefl <-trans <-cotrans) = isSPO)
    where
    -- open IsStrictPartialOrder isSPO

    #-from-<-isProp : ∀ x y → isProp (x # y)
    #-from-<-isProp x y (inl x<y₁) (inl x<y₂) = cong inl (<-isProp x y x<y₁ x<y₂)
    -- NOTE: ⊥-elim could not resolve the level here and needed some hint on `A`
    #-from-<-isProp x y (inl x<y ) (inr y<x ) = ⊥-elim {A = λ _ → inl x<y ≡ inr y<x} (<-irrefl y (<-trans y x y y<x x<y))
    #-from-<-isProp x y (inr y<x ) (inl x<y ) = ⊥-elim {A = λ _ → inr y<x ≡ inl x<y} (<-irrefl y (<-trans y x y y<x x<y))
    #-from-<-isProp x y (inr y<x₁) (inr y<x₂) = cong inr (<-isProp y x y<x₁ y<x₂)

module Properties where

  module _ where
    open import Cubical.Algebra.Group
    -- import Cubical.Algebra.Group.Properties

    module GroupProperties (G : Group {ℓ}) where
      open Group G
      private
        simplR = GroupLemmas.simplR G

      invUniqueL : {g h : Carrier} → g + h ≡ 0g → g ≡ - h
      invUniqueL {g} {h} p = simplR h (p ∙ sym (invl h))

      -- ported from `Algebra.Properties.Group`
      right-helper : ∀ x y → y ≡ - x + (x + y)
      right-helper x y = (
        y               ≡⟨ sym (snd (identity y)) ⟩
        0g          + y ≡⟨ cong₂ _+_ (sym (snd (inverse x))) refl  ⟩
        ((- x) + x) + y ≡⟨ sym (assoc (- x) x y) ⟩
        (- x) + (x + y) ∎)

      -- alternative:
      --   follows from uniqueness of -
      --     (a + -a) ≡ 0
      --     ∃! b . a + b = 0
      --   show that a is an additive inverse of - a then it must be THE additive inverse of - a and has to be called - - a which is a by uniqueness
      -involutive : ∀ x → - - x ≡ x
      -involutive x = (
        (- (- x))             ≡⟨ sym (fst (identity _)) ⟩
        (- (- x)) + 0g        ≡⟨ cong₂ _+_ refl (sym (snd (inverse _))) ⟩
        (- (- x)) + (- x + x) ≡⟨ sym (right-helper (- x) x) ⟩
        x                    ∎)

  module _ where
    open import Cubical.Algebra.Ring
    module RingProperties (R : Ring {ℓ}) where
      open Ring R
      open Cubical.Algebra.Ring.Theory R

      -- NOTE: a few facts about rings that might be collected from elsewhere
      a+b-b≡a : ∀ a b → a ≡ (a + b) - b
      a+b-b≡a a b = let P = sym (fst (+-inv b))
                        Q = sym (fst (+-identity a))
                        R = transport (λ i → a ≡ a + P i) Q
                        S = transport (λ i → a ≡ (+-assoc a b (- b)) i ) R
                    in S

      -- NOTE: this is called `simplL` and `simplL` in `Cubical.Algebra.Group.Properties.GroupLemmas`
      +-preserves-≡ : ∀{a b} → ∀ c → a ≡ b → a + c ≡ b + c
      +-preserves-≡ c a≡b i = a≡b i + c

      +-preserves-≡-l : ∀{a b} → ∀ c → a ≡ b → c + a ≡ c + b
      +-preserves-≡-l c a≡b i = c + a≡b i

      a+b≡0→a≡-b : ∀{a b} → a + b ≡ 0r → a ≡ - b
      a+b≡0→a≡-b {a} {b} a+b≡0 = transport
        (λ i →
          let RHS = snd (+-identity (- b))
              LHS₁ : a + (b + - b) ≡ a + 0r
              LHS₁ = +-preserves-≡-l a (fst (+-inv b))
              LHS₂ : (a + b) - b ≡ a
              LHS₂ = transport (λ j →  (+-assoc a b (- b)) j ≡ fst (+-identity a) j) LHS₁
              in  LHS₂ i ≡ RHS i
        ) (+-preserves-≡ (- b) a+b≡0)

      -- NOTE: there is already
      -- -commutesWithRight-· : (x y : R) →  x · (- y) ≡ - (x · y)

      a·-b≡-a·b : ∀ a b → a · (- b) ≡ - (a · b)
      a·-b≡-a·b a b =
        let P : a · 0r ≡ 0r
            P = 0-rightNullifies a
            Q : a · (- b + b) ≡ 0r
            Q = transport (λ i →  a · snd (+-inv b) (~ i) ≡ 0r) P
            R : a · (- b) + a · b ≡ 0r
            R = transport (λ i → ·-rdist-+ a (- b) b i ≡ 0r) Q
        in a+b≡0→a≡-b R

      a·b-a·c≡a·[b-c] : ∀ a b c → a · b - (a · c) ≡ a · (b - c)
      a·b-a·c≡a·[b-c] a b c =
        let P : a · b + a · (- c) ≡ a · (b + - c)
            P = sym (·-rdist-+ a b (- c))
            Q : a · b - a · c ≡ a · (b + - c)
            Q = transport (λ i →  a · b + a·-b≡-a·b a c i ≡ a · (b + - c) ) P
        in  Q

  -- exports
  module Group = GroupProperties
  module Ring  = RingProperties

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
open import Coinduction using ( ♯_ )
open import Data.Maybe using ( Maybe ; just ; nothing ; maybe )
open import Data.Nat using ( ℕ ; _+_ )
open import Data.Integer using ( ℤ ; +_ ; _⊖_ )
open import System.IO.Transducers using ( inp ; out ; done ; _⇒_ ; Inp_⇒_ ; C⟦_⟧ ; _⟨¿⟩_ )
open import System.IO.Transducers.Trace using ( [] ; _∷_ )
open import System.IO.Transducers.Session using ( ⟨_⟩ ; _&_ ; ¡ ; ¿ )
open import System.IO.Transducers.Stateful using ( loop )

module System.IO.Examples.Transducers where

add : ⟨ ℕ ⟩ & ⟨ ℕ ⟩ ⇒ ⟨ ℕ ⟩
add = inp (♯ λ x → inp (♯ λ y → out (x + y) done))

-- runAdd == 8 ∷ []
runAdd = C⟦ add ⟧ ( 3 ∷ 5 ∷ [] )

nat? : ¡ ⟨ ℤ ⟩ ⇒ ¿ ⟨ ℕ ⟩ & ¡ ⟨ ℤ ⟩
nat? = inp (♯ rest) where
  rest : Inp ¡ ⟨ ℤ ⟩ ⇒ ¿ ⟨ ℕ ⟩ & ¡ ⟨ ℤ ⟩
  rest nothing      = out nothing (out nothing done)
  rest (just (+ n)) = out (just n) done
  rest (just x)     = out nothing (out (just x) done)

-- runNat? == ( just 5 ∷ just (+ 7) ∷ just (0 ⊖ 3) ∷ just (+ 8) ∷ nothing ∷ [])
runNat? = C⟦ nat? ⟧ ( just (+ 5) ∷ just (+ 7) ∷ just (0 ⊖ 3) ∷ just (+ 8) ∷ nothing ∷ [])

nat! : ¡ ⟨ ℤ ⟩ ⇒ ¡ ⟨ ℕ ⟩ & ¡ ⟨ ℤ ⟩
nat! = loop {⟨ ℕ ⟩} nat?

-- runNat! == ( just 5 ∷ just 7 ∷ nothing ∷ just (0 ⊖ 3) ∷ just (+ 8) ∷ nothing ∷ [])
runNat! = C⟦ nat! ⟧ ( just (+ 5) ∷ just (+ 7) ∷ just (0 ⊖ 3) ∷ just (+ 8) ∷ nothing ∷ [])

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
module Structure.Operator.Field where

import      Lvl
open import Logic
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Operator.Properties
open import Structure.Operator.Ring
open import Type

record Field {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  field
    ⦃ divisionRing ⦄      : DivisionRing(_+_)(_⋅_)
    ⦃ [⋅]-commutativity ⦄ : Commutativity(_⋅_)

  open DivisionRing(divisionRing) public

  field
     -- Note: This excludes the trivial ring and is unprovable from the other field axioms, and models where this is true are always "trivial/singleton rings".
    ⦃ distinct-identities ⦄ : DistinctIdentities

record FieldObject {ℓ ℓₑ} : Stmt{Lvl.𝐒(ℓ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {T} : Type{ℓ}
    ⦃ equiv ⦄ : Equiv{ℓₑ}(T)
    _+_ : T → T → T
    _⋅_ : T → T → T
    ⦃ structure ⦄ : Field(_+_)(_⋅_)
  open Field(structure) public

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:
{-# OPTIONS --without-K --safe #-}

-- Bundled version of a Cartesian Category
module Categories.Category.Cartesian.Bundle where

open import Level

open import Categories.Category.Core using (Category)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
open import Categories.Category.Monoidal using (MonoidalCategory)

record CartesianCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U         : Category o ℓ e  -- U for underlying
    cartesian : Cartesian U

  open Category U public
  open Cartesian cartesian public

  monoidalCategory : MonoidalCategory o ℓ e
  monoidalCategory = record
    { U        = U
    ; monoidal = CartesianMonoidal.monoidal cartesian
    }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Weakening {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkEq; wkTerm; wkEqTerm)
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Weakening of neutrals in WHNF

wkTermNe : ∀ {ρ Γ Δ k A} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
         → Γ ⊩neNf k ∷ A → Δ ⊩neNf U.wk ρ k ∷ U.wk ρ A
wkTermNe {ρ} [ρ] ⊢Δ (neNfₜ neK ⊢k k≡k) =
  neNfₜ (wkNeutral ρ neK) (T.wkTerm [ρ] ⊢Δ ⊢k) (~-wk [ρ] ⊢Δ k≡k)

wkEqTermNe : ∀ {ρ Γ Δ k k′ A} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
           → Γ ⊩neNf k ≡ k′ ∷ A → Δ ⊩neNf U.wk ρ k ≡ U.wk ρ k′ ∷ U.wk ρ A
wkEqTermNe {ρ} [ρ] ⊢Δ (neNfₜ₌ neK neM k≡m) =
  neNfₜ₌ (wkNeutral ρ neK) (wkNeutral ρ neM) (~-wk [ρ] ⊢Δ k≡m)

-- Weakening of reducible natural numbers

mutual
  wkTermℕ : ∀ {ρ Γ Δ n} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
          → Γ ⊩ℕ n ∷ℕ → Δ ⊩ℕ U.wk ρ n ∷ℕ
  wkTermℕ {ρ} [ρ] ⊢Δ (ℕₜ n d n≡n prop) =
    ℕₜ (U.wk ρ n) (wkRed:*:Term [ρ] ⊢Δ d)
       (≅ₜ-wk [ρ] ⊢Δ n≡n)
       (wkNatural-prop [ρ] ⊢Δ prop)

  wkNatural-prop : ∀ {ρ Γ Δ n} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
                 → Natural-prop Γ n
                 → Natural-prop Δ (U.wk ρ n)
  wkNatural-prop ρ ⊢Δ (sucᵣ n) = sucᵣ (wkTermℕ ρ ⊢Δ n)
  wkNatural-prop ρ ⊢Δ zeroᵣ = zeroᵣ
  wkNatural-prop ρ ⊢Δ (ne nf) = ne (wkTermNe ρ ⊢Δ nf)

mutual
  wkEqTermℕ : ∀ {ρ Γ Δ t u} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
            → Γ ⊩ℕ t ≡ u ∷ℕ
            → Δ ⊩ℕ U.wk ρ t ≡ U.wk ρ u ∷ℕ
  wkEqTermℕ {ρ} [ρ] ⊢Δ (ℕₜ₌ k k′ d d′ t≡u prop) =
    ℕₜ₌ (U.wk ρ k) (U.wk ρ k′) (wkRed:*:Term [ρ] ⊢Δ d)
        (wkRed:*:Term [ρ] ⊢Δ d′) (≅ₜ-wk [ρ] ⊢Δ t≡u)
        (wk[Natural]-prop [ρ] ⊢Δ prop)

  wk[Natural]-prop : ∀ {ρ Γ Δ n n′} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
                   → [Natural]-prop Γ n n′
                   → [Natural]-prop Δ (U.wk ρ n) (U.wk ρ n′)
  wk[Natural]-prop ρ ⊢Δ (sucᵣ [n≡n′]) = sucᵣ (wkEqTermℕ ρ ⊢Δ [n≡n′])
  wk[Natural]-prop ρ ⊢Δ zeroᵣ = zeroᵣ
  wk[Natural]-prop ρ ⊢Δ (ne x) = ne (wkEqTermNe ρ ⊢Δ x)

-- Empty
wkTermEmpty : ∀ {ρ Γ Δ n} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
  → Γ ⊩Empty n ∷Empty → Δ ⊩Empty U.wk ρ n ∷Empty
wkTermEmpty {ρ} [ρ] ⊢Δ (Emptyₜ n d n≡n (ne prop)) =
  Emptyₜ (U.wk ρ n) (wkRed:*:Term [ρ] ⊢Δ d)
     (≅ₜ-wk [ρ] ⊢Δ n≡n)
     (ne (wkTermNe [ρ] ⊢Δ prop))

wk[Empty]-prop : ∀ {ρ Γ Δ n n′} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
  → [Empty]-prop Γ n n′
  → [Empty]-prop Δ (U.wk ρ n) (U.wk ρ n′)
wk[Empty]-prop ρ ⊢Δ (ne x) = ne (wkEqTermNe ρ ⊢Δ x)

wkEqTermEmpty : ∀ {ρ Γ Δ t u} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
  → Γ ⊩Empty t ≡ u ∷Empty
  → Δ ⊩Empty U.wk ρ t ≡ U.wk ρ u ∷Empty
wkEqTermEmpty {ρ} [ρ] ⊢Δ (Emptyₜ₌ k k′ d d′ t≡u prop) =
  Emptyₜ₌ (U.wk ρ k) (U.wk ρ k′) (wkRed:*:Term [ρ] ⊢Δ d)
      (wkRed:*:Term [ρ] ⊢Δ d′) (≅ₜ-wk [ρ] ⊢Δ t≡u)
      (wk[Empty]-prop [ρ] ⊢Δ prop)

-- Unit
wkTermUnit : ∀ {ρ Γ Δ n} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
           → Γ ⊩Unit n ∷Unit → Δ ⊩Unit U.wk ρ n ∷Unit
wkTermUnit {ρ} [ρ] ⊢Δ (Unitₜ n d prop) =
  Unitₜ (U.wk ρ n) (wkRed:*:Term [ρ] ⊢Δ d) (wkWhnf ρ prop)

wkEqTermUnit : ∀ {ρ Γ Δ t u} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
          → Γ ⊩Unit t ≡ u ∷Unit
          → Δ ⊩Unit U.wk ρ t ≡ U.wk ρ u ∷Unit
wkEqTermUnit {ρ} [ρ] ⊢Δ (Unitₜ₌ ⊢t ⊢u) =
  Unitₜ₌ (T.wkTerm [ρ] ⊢Δ ⊢t) (T.wkTerm [ρ] ⊢Δ ⊢u)

-- Weakening of the logical relation

wk : ∀ {ρ Γ Δ A l} → ρ ∷ Δ ⊆ Γ → ⊢ Δ → Γ ⊩⟨ l ⟩ A → Δ ⊩⟨ l ⟩ U.wk ρ A
wk ρ ⊢Δ (Uᵣ′ l′ l< ⊢Γ) = Uᵣ′ l′ l< ⊢Δ
wk ρ ⊢Δ (ℕᵣ D) = ℕᵣ (wkRed:*: ρ ⊢Δ D)
wk ρ ⊢Δ (Emptyᵣ D) = Emptyᵣ (wkRed:*: ρ ⊢Δ D)
wk ρ ⊢Δ (Unitᵣ D) = Unitᵣ (wkRed:*: ρ ⊢Δ D)
wk {ρ} [ρ] ⊢Δ (ne′ K D neK K≡K) =
  ne′ (U.wk ρ K) (wkRed:*: [ρ] ⊢Δ D) (wkNeutral ρ neK) (~-wk [ρ] ⊢Δ K≡K)
wk {ρ} {Γ} {Δ} {A} {l} [ρ] ⊢Δ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  let ⊢ρF = T.wk [ρ] ⊢Δ ⊢F
      [F]′ : ∀ {ρ ρ′ E} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
           → E ⊩⟨ l ⟩ U.wk ρ (U.wk ρ′ F)
      [F]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E = irrelevance′
                              (PE.sym (wk-comp ρ ρ′ F))
                              ([F] ([ρ] •ₜ [ρ′]) ⊢E)
      [a]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ a ∷ U.wk (ρ • ρ′) F / [F] ([ρ] •ₜ [ρ′]) ⊢E
      [a]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E [a] = irrelevanceTerm′ (wk-comp ρ ρ′ F)
                                          ([F]′ [ρ] [ρ′] ⊢E) ([F] ([ρ] •ₜ [ρ′]) ⊢E) [a]
      [G]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ U.wk (lift (ρ • ρ′)) G [ a ]
      [G]′ η η′ ⊢E [a] = [G] (η •ₜ η′) ⊢E ([a]′ η η′ ⊢E [a])
  in  Πᵣ′ (U.wk ρ F) (U.wk (lift ρ) G) (T.wkRed:*: [ρ] ⊢Δ D) ⊢ρF
           (T.wk (lift [ρ]) (⊢Δ ∙ ⊢ρF) ⊢G)
           (≅-wk [ρ] ⊢Δ A≡A)
           (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] → irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                        ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] [b] [a≡b] →
              let [a≡b]′ = irrelevanceEqTerm′ (wk-comp ρ₁ ρ F)
                                              ([F]′ [ρ₁] [ρ] ⊢Δ₁)
                                              ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                              [a≡b]
              in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                                  (wk-comp-subst ρ₁ ρ G)
                                  ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                  (irrelevance′
                                            (wk-comp-subst ρ₁ ρ G)
                                            ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
                                  (G-ext ([ρ₁] •ₜ [ρ]) ⊢Δ₁
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [b])
                                         [a≡b]′))
wk {ρ} {Γ} {Δ} {A} {l} [ρ] ⊢Δ (Σᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  let ⊢ρF = T.wk [ρ] ⊢Δ ⊢F
      [F]′ : ∀ {ρ ρ′ E} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
           → E ⊩⟨ l ⟩ U.wk ρ (U.wk ρ′ F)
      [F]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E = irrelevance′
                              (PE.sym (wk-comp ρ ρ′ F))
                              ([F] ([ρ] •ₜ [ρ′]) ⊢E)
      [a]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ a ∷ U.wk (ρ • ρ′) F / [F] ([ρ] •ₜ [ρ′]) ⊢E
      [a]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E [a] = irrelevanceTerm′ (wk-comp ρ ρ′ F)
                                          ([F]′ [ρ] [ρ′] ⊢E) ([F] ([ρ] •ₜ [ρ′]) ⊢E) [a]
      [G]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ U.wk (lift (ρ • ρ′)) G [ a ]
      [G]′ η η′ ⊢E [a] = [G] (η •ₜ η′) ⊢E ([a]′ η η′ ⊢E [a])
  in  Σᵣ′ (U.wk ρ F) (U.wk (lift ρ) G) (T.wkRed:*: [ρ] ⊢Δ D) ⊢ρF
           (T.wk (lift [ρ]) (⊢Δ ∙ ⊢ρF) ⊢G)
           (≅-wk [ρ] ⊢Δ A≡A)
           (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] → irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                        ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] [b] [a≡b] →
              let [a≡b]′ = irrelevanceEqTerm′ (wk-comp ρ₁ ρ F)
                                              ([F]′ [ρ₁] [ρ] ⊢Δ₁)
                                              ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                              [a≡b]
              in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                                  (wk-comp-subst ρ₁ ρ G)
                                  ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                  (irrelevance′
                                            (wk-comp-subst ρ₁ ρ G)
                                            ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
                                  (G-ext ([ρ₁] •ₜ [ρ]) ⊢Δ₁
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [b])
                                         [a≡b]′))
wk ρ ⊢Δ (emb 0<1 x) = emb 0<1 (wk ρ ⊢Δ x)

wkEq : ∀ {ρ Γ Δ A B l} → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
       ([A] : Γ ⊩⟨ l ⟩ A)
     → Γ ⊩⟨ l ⟩ A ≡ B / [A]
     → Δ ⊩⟨ l ⟩ U.wk ρ A ≡ U.wk ρ B / wk [ρ] ⊢Δ [A]
wkEq ρ ⊢Δ (Uᵣ′ _ _ _) PE.refl = PE.refl
wkEq ρ ⊢Δ (ℕᵣ D) A≡B = wkRed* ρ ⊢Δ A≡B
wkEq ρ ⊢Δ (Emptyᵣ D) A≡B = wkRed* ρ ⊢Δ A≡B
wkEq ρ ⊢Δ (Unitᵣ D) A≡B = wkRed* ρ ⊢Δ A≡B
wkEq {ρ} [ρ] ⊢Δ (ne′ _ _ _ _) (ne₌ M D′ neM K≡M) =
  ne₌ (U.wk ρ M) (wkRed:*: [ρ] ⊢Δ D′)
      (wkNeutral ρ neM) (~-wk [ρ] ⊢Δ K≡M)
wkEq {ρ} [ρ] ⊢Δ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  B₌ (U.wk ρ F′) (U.wk (lift ρ) G′) (T.wkRed* [ρ] ⊢Δ D′) (≅-wk [ρ] ⊢Δ A≡B)
     (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevanceEq″ (PE.sym (wk-comp ρ₁ ρ F))
                                 (PE.sym (wk-comp ρ₁ ρ F′))
                                 ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                 (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                               ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                 ([F≡F′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
        let [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F)
                                    (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                                  ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁) [a]
        in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                            (wk-comp-subst ρ₁ ρ G′)
                            ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′)
                            (irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                          ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
                            ([G≡G′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkEq {ρ} [ρ] ⊢Δ (Σᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  B₌ (U.wk ρ F′) (U.wk (lift ρ) G′) (T.wkRed* [ρ] ⊢Δ D′) (≅-wk [ρ] ⊢Δ A≡B)
     (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevanceEq″ (PE.sym (wk-comp ρ₁ ρ F))
                                 (PE.sym (wk-comp ρ₁ ρ F′))
                                 ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                 (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                               ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                 ([F≡F′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
        let [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F)
                                    (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                                  ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁) [a]
        in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                            (wk-comp-subst ρ₁ ρ G′)
                            ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′)
                            (irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                          ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
                            ([G≡G′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkEq ρ ⊢Δ (emb 0<1 x) A≡B = wkEq ρ ⊢Δ x A≡B

wkTerm : ∀ {ρ Γ Δ A t l} ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
         ([A] : Γ ⊩⟨ l ⟩ A)
       → Γ ⊩⟨ l ⟩ t ∷ A / [A]
       → Δ ⊩⟨ l ⟩ U.wk ρ t ∷ U.wk ρ A / wk [ρ] ⊢Δ [A]
wkTerm {ρ} [ρ] ⊢Δ (Uᵣ′ .⁰ 0<1 ⊢Γ) (Uₜ A d typeA A≡A [t]) =
  Uₜ (U.wk ρ A) (wkRed:*:Term [ρ] ⊢Δ d)
     (wkType ρ typeA) (≅ₜ-wk [ρ] ⊢Δ A≡A) (wk [ρ] ⊢Δ [t])
wkTerm ρ ⊢Δ (ℕᵣ D) [t] = wkTermℕ ρ ⊢Δ [t]
wkTerm ρ ⊢Δ (Emptyᵣ D) [t] = wkTermEmpty ρ ⊢Δ [t]
wkTerm ρ ⊢Δ (Unitᵣ D) [t] = wkTermUnit ρ ⊢Δ [t]
wkTerm {ρ} [ρ] ⊢Δ (ne′ K D neK K≡K) (neₜ k d nf) =
  neₜ (U.wk ρ k) (wkRed:*:Term [ρ] ⊢Δ d) (wkTermNe [ρ] ⊢Δ nf)
wkTerm {ρ} [ρ] ⊢Δ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  Πₜ (U.wk ρ f) (wkRed:*:Term [ρ] ⊢Δ d) (wkFunction ρ funcF)
     (≅ₜ-wk [ρ] ⊢Δ f≡f)
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] [b] [a≡b] →
        let F-compEq = wk-comp ρ₁ ρ F
            G-compEq = wk-comp-subst ρ₁ ρ G
            [F]₁ = [F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁
            [F]₂ = irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) [F]₁
            [a]′ = irrelevanceTerm′ F-compEq [F]₂ [F]₁ [a]
            [b]′ = irrelevanceTerm′ F-compEq [F]₂ [F]₁ [b]
            [G]₁ = [G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′
            [G]₂ = irrelevance′ G-compEq [G]₁
            [a≡b]′ = irrelevanceEqTerm′ F-compEq [F]₂ [F]₁ [a≡b]
        in  irrelevanceEqTerm″ (PE.cong (λ x → x ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                (PE.cong (λ x → x ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                G-compEq
                                [G]₁ [G]₂
                                ([f] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′ [b]′ [a≡b]′))
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
        let [F]₁ = [F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁
            [F]₂ = irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) [F]₁
            [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F) [F]₂ [F]₁ [a]
            [G]₁ = [G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′
            [G]₂ = irrelevance′ (wk-comp-subst ρ₁ ρ G) [G]₁
        in  irrelevanceTerm″ (wk-comp-subst ρ₁ ρ G)
                              (PE.cong (λ x → x ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                              [G]₁ [G]₂ ([f]₁ ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkTerm {ρ} [ρ] ⊢Δ [A]@(Σᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                  (Σₜ p d pProd p≅p [fst] [snd]) =
  let [ρF] = irrelevance′ (PE.sym (wk-comp id ρ F)) ([F] [ρ] (wf (T.wk [ρ] ⊢Δ ⊢F)))
      [ρfst] = wkTerm [ρ] ⊢Δ ([F] id (wf ⊢F)) [fst]
      [ρfst]′ = (irrelevanceTerm′
                  (PE.begin
                    U.wk ρ (U.wk id F)
                  PE.≡⟨ PE.cong (U.wk ρ) (wk-id F) ⟩
                    U.wk ρ F
                  PE.≡⟨ PE.sym (wk-id (U.wk ρ F)) ⟩
                    U.wk id (U.wk ρ F)
                  PE.∎)
                  (wk [ρ] ⊢Δ ([F] id (wf ⊢F)))
                  [ρF]
                  [ρfst])
      [ρsnd] = wkTerm [ρ] ⊢Δ ([G] id (wf ⊢F) [fst]) [snd]
      [ρG]′ = (irrelevance′ (wk-comp-subst id ρ G)
       ([G] [ρ] (wf (T.wk [ρ] ⊢Δ ⊢F))
        (irrelevanceTerm′ (wk-comp id ρ F)
         [ρF]
         ([F] [ρ] (wf (T.wk [ρ] ⊢Δ ⊢F)))
         [ρfst]′)))
      [ρsnd]′ = irrelevanceTerm′
                  (PE.begin
                    U.wk ρ (U.wk (lift id) G [ fst p ])
                  PE.≡⟨ PE.cong (λ x → U.wk ρ (x [ fst p ])) (wk-lift-id G) ⟩
                    U.wk ρ (G [ fst p ])
                  PE.≡⟨ wk-β G ⟩
                    (U.wk (lift ρ) G) [ fst (U.wk ρ p) ]
                  PE.≡⟨ PE.cong (λ x → x [ fst (U.wk ρ p) ]) (PE.sym (wk-lift-id (U.wk (lift ρ) G))) ⟩
                    (U.wk (lift id) (U.wk (lift ρ) G)) [ fst (U.wk ρ p) ]
                  PE.∎)
                  (wk [ρ] ⊢Δ ([G] id (wf ⊢F) [fst])) [ρG]′
                  [ρsnd]
  in  Σₜ (U.wk ρ p) (wkRed:*:Term [ρ] ⊢Δ d) (wkProduct ρ pProd) (≅ₜ-wk [ρ] ⊢Δ p≅p)
         [ρfst]′ [ρsnd]′
wkTerm ρ ⊢Δ (emb 0<1 x) t = wkTerm ρ ⊢Δ x t

wkEqTerm : ∀ {ρ Γ Δ A t u l} ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
           ([A] : Γ ⊩⟨ l ⟩ A)
         → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
         → Δ ⊩⟨ l ⟩ U.wk ρ t ≡ U.wk ρ u ∷ U.wk ρ A / wk [ρ] ⊢Δ [A]
wkEqTerm {ρ} [ρ] ⊢Δ (Uᵣ′ .⁰ 0<1 ⊢Γ) (Uₜ₌ A B d d′ typeA typeB A≡B [t] [u] [t≡u]) =
  Uₜ₌ (U.wk ρ A) (U.wk ρ B) (wkRed:*:Term [ρ] ⊢Δ d) (wkRed:*:Term [ρ] ⊢Δ d′)
      (wkType ρ typeA) (wkType ρ typeB) (≅ₜ-wk [ρ] ⊢Δ A≡B)
      (wk [ρ] ⊢Δ [t]) (wk [ρ] ⊢Δ [u]) (wkEq [ρ] ⊢Δ [t] [t≡u])
wkEqTerm ρ ⊢Δ (ℕᵣ D) [t≡u] = wkEqTermℕ ρ ⊢Δ [t≡u]
wkEqTerm ρ ⊢Δ (Emptyᵣ D) [t≡u] = wkEqTermEmpty ρ ⊢Δ [t≡u]
wkEqTerm ρ ⊢Δ (Unitᵣ D) [t≡u] = wkEqTermUnit ρ ⊢Δ [t≡u]
wkEqTerm {ρ} [ρ] ⊢Δ (ne′ K D neK K≡K) (neₜ₌ k m d d′ nf) =
  neₜ₌ (U.wk ρ k) (U.wk ρ m)
       (wkRed:*:Term [ρ] ⊢Δ d) (wkRed:*:Term [ρ] ⊢Δ d′)
       (wkEqTermNe [ρ] ⊢Δ nf)
wkEqTerm {ρ} [ρ] ⊢Δ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                    (Πₜ₌ f g d d′ funcF funcG f≡g [t] [u] [f≡g]) =
  let [A] = Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
  in  Πₜ₌ (U.wk ρ f) (U.wk ρ g) (wkRed:*:Term [ρ] ⊢Δ d) (wkRed:*:Term [ρ] ⊢Δ d′)
          (wkFunction ρ funcF) (wkFunction ρ funcG)
          (≅ₜ-wk [ρ] ⊢Δ f≡g) (wkTerm [ρ] ⊢Δ [A] [t]) (wkTerm [ρ] ⊢Δ [A] [u])
          (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
             let [F]₁ = [F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁
                 [F]₂ = irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) [F]₁
                 [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F) [F]₂ [F]₁ [a]
                 [G]₁ = [G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′
                 [G]₂ = irrelevance′ (wk-comp-subst ρ₁ ρ G) [G]₁
             in  irrelevanceEqTerm″ (PE.cong (λ y → y ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                     (PE.cong (λ y → y ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                     (wk-comp-subst ρ₁ ρ G)
                                     [G]₁ [G]₂
                                     ([f≡g] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkEqTerm {ρ} [ρ] ⊢Δ [A]@(Σᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                    (Σₜ₌ p r d d′ pProd rProd p≅r [t] [u] [fstp] [fstr] [fst≡] [snd≡]) =
  let [A] = Σᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
      ⊢Γ = wf ⊢F
      ρidF≡idρF = PE.begin
                    U.wk ρ (U.wk id F)
                  PE.≡⟨ PE.cong (U.wk ρ) (wk-id F) ⟩
                    U.wk ρ F
                  PE.≡⟨ PE.sym (wk-id (U.wk ρ F)) ⟩
                    U.wk id (U.wk ρ F)
                  PE.∎
      [ρF] = irrelevance′ (PE.sym (wk-comp id ρ F)) ([F] [ρ] (wf (T.wk [ρ] ⊢Δ ⊢F)))
      [ρfstp] = wkTerm [ρ] ⊢Δ ([F] id ⊢Γ) [fstp]
      [ρfstp]′ = irrelevanceTerm′
                  ρidF≡idρF
                  (wk [ρ] ⊢Δ ([F] id ⊢Γ)) [ρF]
                  [ρfstp]
      [ρfstr] = wkTerm [ρ] ⊢Δ ([F] id ⊢Γ) [fstr]
      [ρfstr]′ = irrelevanceTerm′
                  ρidF≡idρF
                  (wk [ρ] ⊢Δ ([F] id ⊢Γ)) [ρF]
                  [ρfstr]
      [ρfst≡] = wkEqTerm [ρ] ⊢Δ ([F] id ⊢Γ) [fst≡]
      [ρfst≡]′ = irrelevanceEqTerm′
                   ρidF≡idρF
                   (wk [ρ] ⊢Δ ([F] id ⊢Γ)) [ρF]
                   [ρfst≡]
      [ρsnd≡] = wkEqTerm [ρ] ⊢Δ ([G] id ⊢Γ [fstp]) [snd≡]
      [ρG]′ = (irrelevance′ (wk-comp-subst id ρ G)
       ([G] [ρ] (wf (T.wk [ρ] ⊢Δ ⊢F))
        (irrelevanceTerm′ (wk-comp id ρ F)
         [ρF]
         ([F] [ρ] (wf (T.wk [ρ] ⊢Δ ⊢F)))
         [ρfstp]′)))
      [ρsnd≡]′ = irrelevanceEqTerm′
                  (PE.begin
                    U.wk ρ (U.wk (lift id) G [ fst p ])
                  PE.≡⟨ PE.cong (λ x → U.wk ρ (x [ fst p ])) (wk-lift-id G) ⟩
                    U.wk ρ (G [ fst p ])
                  PE.≡⟨ wk-β G ⟩
                    (U.wk (lift ρ) G) [ fst (U.wk ρ p) ]
                  PE.≡⟨ PE.cong (λ x → x [ fst (U.wk ρ p) ]) (PE.sym (wk-lift-id (U.wk (lift ρ) G))) ⟩
                    (U.wk (lift id) (U.wk (lift ρ) G)) [ fst (U.wk ρ p) ]
                  PE.∎)
                  (wk [ρ] ⊢Δ ([G] id (wf ⊢F) [fstp])) [ρG]′
                  [ρsnd≡]
  in  Σₜ₌ (U.wk ρ p) (U.wk ρ r) (wkRed:*:Term [ρ] ⊢Δ d) (wkRed:*:Term [ρ] ⊢Δ d′)
          (wkProduct ρ pProd) (wkProduct ρ rProd)
          (≅ₜ-wk [ρ] ⊢Δ p≅r) (wkTerm [ρ] ⊢Δ [A] [t]) (wkTerm [ρ] ⊢Δ [A] [u])
          [ρfstp]′ [ρfstr]′ [ρfst≡]′ [ρsnd≡]′
wkEqTerm ρ ⊢Δ (emb 0<1 x) t≡u = wkEqTerm ρ ⊢Δ x t≡u


text:
module FlexInterpreter where

data Ty : Set where
  nat : Ty
  arr : Ty -> Ty -> Ty

data Exp : Ty -> Set where
  zero : Exp nat
  suc  : Exp (arr nat nat)
  pred : Exp (arr nat nat)
  app  : {a b : Ty} -> Exp (arr a b) -> Exp a -> Exp b

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

Sem : Ty -> Set
Sem nat = Nat
Sem (arr a b) = Sem a -> Sem b

eval : {a : Ty} -> Exp a -> Sem a
eval zero = zero
eval suc  = suc
eval pred zero = zero
eval pred (suc n) = n
eval (app f e) = eval f (eval e)

max_stars_repo_name: dagit/agda

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
-- Ordinals as defined in the HoTT book.

{-# OPTIONS --without-K --safe #-}
module Ordinal.HoTT where

open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Induction.WellFounded using (Acc ; acc ; WellFounded)
open import Level using (Level ; _⊔_ ; 0ℓ) renaming (suc to lsuc)
open import Relation.Binary using (Rel ; IsEquivalence ; Transitive)

private
  variable
    α β γ ρ ε : Level
    A B C : Set α

record _↔_ (A : Set α) (B : Set β) : Set (α ⊔ β) where
  field
    forth : A → B
    back : B → A

open _↔_ public

IsExtensional : ∀ {α} {A : Set α} (_≈_ : Rel A ε) (_<_ : Rel A ρ) → Set (α ⊔ ε ⊔ ρ)
IsExtensional _≈_ _<_ = ∀ {a b} → (∀ c → (c < a) ↔ (c < b)) → a ≈ b

record IsOrdinal (A : Set α) ε ρ : Set (α ⊔ lsuc (ε ⊔ ρ)) where
  field
    _≈_ : Rel A ε
    ≈-equiv : IsEquivalence _≈_
    _<_ : Rel A ρ
    <-wf : WellFounded _<_
    <-ext : IsExtensional _≈_ _<_
    <-trans : Transitive _<_

  open IsEquivalence ≈-equiv public using () renaming
    ( refl to ≈-refl
    ; sym to ≈-sym
    ; trans to ≈-trans)

open IsOrdinal public

record Ordinal α ε ρ : Set (lsuc (α ⊔ ε ⊔ ρ)) where
  field
    _↓ : Set α
    isOrdinal : IsOrdinal _↓ ε ρ

open Ordinal public

zero : Ordinal 0ℓ 0ℓ 0ℓ
zero = record
  { _↓ = ⊤
  ; isOrdinal = record
    { _≈_ = λ _ _ → ⊤
    ; ≈-equiv = _
    ; _<_ = λ _ _ → ⊥
    ; <-wf = λ _ → acc λ y ()
    ; <-ext = _
    ; <-trans = λ()
    }
  }

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Part2_Agda_in_a_Nutshell where

{-
https://serokell.io/blog/agda-in-nutshell

Danya Rogozin
Monday, November 26th, 2018

Theorem proving in Agda based on a constructive logical framework.
Dependently typed programming and theorem proving in Agda.
Example use of Agda in the formalisation of algebra.

------------------------------------------------------------------------------
General

dependently typed : based on variant of Martin-Löf type theory.

Martin-Löf is constructive, so Agda doesn’t have default features for writing classical
(in contrast to HOL or Isabelle).

Agda : proof-assistant based on propositions-as-types.

------------------------------------------------------------------------------
Types in Agda

datatypes introduced via GADTs
-}

data Writers    : Set where Wilde Shelley Byron Sartre Camus                    : Writers
data Literature : Set where DorianGrey Alastor ChildeHarold LaNausée L’Étranger : Literature

data ℕ : Set where
  zero :     ℕ
  suc  : ℕ → ℕ

{-
Parameterized and indexed datatypes

see: https://agda.readthedocs.io/en/latest/language/data-types.html#indexed-datatypes

parameterized datatype
- depends on parameter that should remain the same in the types of constructors
-}

data List (A : Set) : Set where
  Nil  :              List A
  Cons : A → List A → List A

-- can have indexes that could differ from constructor to constructor

-- Vec is parameterized by A and indexed by ℕ.
data Vec (A : Set) : ℕ → Set where
  Nil  :                         Vec A  zero
  -- n is an implicit argument of the constructor.
  -- Cons is an example of a dependent function.
  Cons : {n : ℕ} → A → Vec A n → Vec A (suc n)

-- defines types of finite cardinality
-- Fin is a datatype indexed by a natural number.
data Fin : ℕ → Set where
  -- zero reflects an empty set which is an element of any finite set
  zero : {n : ℕ} →         Fin (suc n)
  -- suc applies the finite set i and yields a new finite set, larger than i on one element.
  suc  : {n : ℕ} → Fin n → Fin (suc n)

-- Vec and Fin in Agda are examples of dependent types,
-- types that depend on values (e.g., natural numbers), not only on types.

------------------------------------------------------------------------------
-- Functions

bookToWriter : Literature → Writers
bookToWriter DorianGrey   = Wilde
bookToWriter Alastor      = Shelley
bookToWriter ChildeHarold = Byron
bookToWriter LaNausée     = Sartre
bookToWriter L’Étranger   = Camus

-- A dependent function is a function that
--   takes a term a of type A and
--   returns some result of type B, where a may appear in B

-- Here types A and B are explicit arguments.
const₁ : (A B : Set) → A → B → A
const₁ A B x y = x

-- may take them implicitly:
const₂ : {A B : Set} → A → B → A
const₂ x y = x

data Ireland : Set where Dublin : Ireland
data England : Set where London : England
data France  : Set where Paris  : France

WriterToCountry : Writers → Set
WriterToCountry Wilde   = Ireland
WriterToCountry Shelley = England
WriterToCountry Byron   = England
WriterToCountry Sartre  = France
WriterToCountry Camus   = France

WriterToCity : (w : Writers) → WriterToCountry w
WriterToCity    Wilde   = Dublin
WriterToCity    Shelley = London
WriterToCity    Byron   = London
WriterToCity    Sartre  = Paris
WriterToCity    Camus   = Paris

{-
WriterToCity is a dependent function, because the type of the result depends on the argument.
The type of a dependent function is called a Π-type.

Generally, given function P: A → Set,
then Π-type is a type of the function that assigns
to every term t : A
some object of type P t.

In Agda : (t : A) → P t for some {A : Set} {P : A → Set} in context.

Logically Π-type encodes intuitionistic universal quantifier.

P is a predicate and
some function of a type (t : A) → P t
is a proof that
for each t : A the property P has established.

------------------------------------------------------------------------------
Dependent pairs : Σ-type

inductive predicate on two lists:
-}

data IsReverse {A : Set} : (xs ys : List A) → Set where
  ReverseNil  : IsReverse [] []
  ReverseCons : (x : A) (xs ys : List A)
              → IsReverse xs ys
              → IsReverse (x ∷ xs) (ys ++ [ x ])
{-
IsReverse xs ys denotes that the list ys is equal to reversed xs.

IsReverse is a datatype parameterized over a type A and
indexed over two lists of elements of type A.

prove theorem : for all list xs there exists list ys such that ys is a reversed list xs,
i.e., produce a dependent pair, where
  the first projection of this pair is some list ys and
  the second one is a proof that ys is reversed list xs.

Use the dependent pair type to prove existence:
-}

theoremReverse₁ : {A : Set} (xs : List A) → Σ (List A) (λ ys → IsReverse xs ys)
theoremReverse₁ [] = [] , ReverseNil
theoremReverse₁ (z ∷ zs) =
    let ys      = proj₁ (theoremReverse₁ zs) in
    let ysProof = proj₂ (theoremReverse₁ zs) in
    ys ++ [ x ] , ReverseCons z zs ys ysProof
{-
Read the theoremReverse₁ signature as
  let A be type and
  xs be a list with elements of the type A,
  then there exists list ys, such that ys is the reversed list xs.

proved by induction on xs and build ys for every case.
Base case: if xs is empty,
  then we present an empty list as the desired list ys and
  ReverseNil is a proof that ys is equal to reversed list xs, because both of them are empty.
Inductive step : xs is a non-empty
  List zs is smaller than z :: zs,
  so apply induction hypothesis to zs and
  show that :: preserves the desired property using the ReverseCons constructor.

Generally, Σ-type is defined in Agda:
-}
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst -- apply B to arg from first field
{-
Defined for arbitrary universes (see below).

logical point of view : Σ A B
  there exists some element of a type A, such that this element satisfies property B
i.e. Σ-type encodes constructive existential quantifier.

To prove the existence of some object with desired property constructively,
present the particular object and prove that object satisfies the property.

------------------------------------------------------------------------------
Universes

Hierarchy of types : initiated by Bertrand Russell.

Basic types (e.g., Nat, Bool) have a type called Set (i.e., Set₁)

Universe polymorphism enables defining functions that can be called on types of arbitrary levels. E.g.,
-}
s : {A B C : Set} → (A → B → C) → (A → B) → A → C
s f g x = f x (g x)

-- indicate that types A, B, C are types of arbitrary level a:
s₁ : {a : Level} {A B C : Set a} → (A → B → C) → (A → B) → A → C
s₁ f g x = f x (g x)

-- generalize s further, because A, B and C in s₁ belong to the same level above,
-- but these types may generally belong to different levels :
s₂ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c}
    → (A → B → C) → (A → B) → A → C
s₂ f g x = f x (g x)

-- most general version of s : a universe polymorphic dependent function

S : {a b c : Level} {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c}
   → (f : (x : A) → (y : B x) → C x y) → (g : (x : A) → B x)
   → (x : A) → C x (g x)
S f g x = f x (g x)

------------------------------------------------------------------------------
-- Records

record Person : Set where
  field
    name    : String
    country : String
    age     : Int

------------------------------------------------------------------------------
-- Typeclasses are introduced in Agda as records. E.g.,

record Functor {a} (F : Set a → Set a) : Set (suc a) where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

-- Instances may be declared either
-- by constructing a record explicitly:
instance
  ListFunctor₁ : Functor List
  ListFunctor₁ = record { fmap = map }
-- or by using copatterns:
instance
  ListFunctor₂ : Functor List
  fmap {{ListFunctor₂}} = map

------------------------------------------------------------------------------
-- Propositional equality

-- The identity type is a datatype that reflects equality of terms in predicate logic.

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

-- examples using propositional equality:

-- proof of distributivity of natural number multiplication over addition
*-+-distr : ∀ a b c → (b + c) * a ≡ b * a + c * a
*-+-distr a zero c = refl
*-+-distr a (suc b) c =
    begin
    (suc b + c) * a     ≡⟨ refl ⟩
    a + (b + c) * a     ≡⟨ cong (_+_ a) (*-+-distr a b c) ⟩
    a + (b * a + c * a) ≡⟨ sym (+-assoc a (b * a) (c * a)) ⟩
    suc b * a + c * a
    ∎

-- Proved by induction on b.
-- When b equals zero, the equality holds trivially.
-- Otherwise, equality is proved using the induction hypothesis.

{-
------------------------------------------------------------------------------
Algebraic example

A ring is an algebraic system
⟨R, +, ⋅, −, 0⟩
, where
R is a non-empty set,
0 ∈ R,
+, ⋅ are binary operations on R
 and
− is a unary operation on R
 such that:
1. ∀a,b,c ∈ R, (a+b)+c=a+(b+c);
2. ∀a,b ∈ R, a+b=b+a;
3. ∀a ∈ R, −a + a = 0;
4. ∀a ∈ R, a + 0 = a;
5. ∀a,b,c ∈ R, (a+b)⋅c=(a⋅c)+(b⋅c);
6. ∀a,b,c ∈ R, a⋅(b+c)=(a⋅b)+(a⋅c).
-}

record Ring (R : Set) : Set₁ where
  constructor mkRing
  infixr 7 _·_
  infixr 6 _+_
  field
      θ   : R
      -_  : R → R
      _+_ : R → R → R
      _·_ : R → R → R

      +-assoc       : (a b c : R) → (a + b) + c ≡ a + (b + c)
      +-commute     : (a b : R)   → a + b ≡ b + a
      +-inv₁        : (a : R)     → - a + a ≡ θ
      +-θ           : (a : R)     → a + θ ≡ a
      ·-distr-right : (a b c : R) → (a + b) · c ≡ (a · c) + (b · c)
      ·-distr-left  : (a b c : R) → a · (b + c) ≡ (a · b) + (a · c)
open Ring {{...}} public

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
open import Agda.Primitive

variable
  ℓ : Level
  A : Set ℓ

postulate
  w/e : ∀ {a} {A : Set a} → A

  Sub : {a : Level} (A : Set a) → (Set → A) → Set

  hcomp-equivFillerSub : Sub A (λ { _ → w/e {_} {_} })

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Cubical.HITs.Sn.Base public
open import Cubical.HITs.Sn.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Luau.Run where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Luau.Heap using (Heap; ∅)
open import Luau.Syntax using (Block; return; _∙_; done)
open import Luau.OpSem using (_⊢_⟶*_⊣_; refl; step)
open import Luau.Value using (val)
open import Properties.Step using (stepᴮ; step; return; done; error)
open import Luau.RuntimeError using (RuntimeErrorᴮ)

data RunResult {a} (H : Heap a) (B : Block a) : Set where
  return : ∀ V {B′ H′} → (H ⊢ B ⟶* (return (val V) ∙ B′) ⊣ H′) → RunResult H B
  done : ∀ {H′} → (H ⊢ B ⟶* done ⊣ H′) → RunResult H B
  error : ∀ {B′ H′} → (RuntimeErrorᴮ H′ B′) → (H ⊢ B ⟶* B′ ⊣ H′) → RunResult H B

{-# TERMINATING #-}
run′ : ∀ {a} H B → RunResult {a} H B
run′ H B with stepᴮ H B
run′ H B | step H′ B′ D with run′ H′ B′
run′ H B | step H′ B′ D | return V D′  = return V (step D D′)
run′ H B | step H′ B′ D | done D′ = done (step D D′)
run′ H B | step H′ B′ D | error E D′ = error E (step D D′)
run′ H _ | return V refl = return V refl
run′ H _ | done refl = done refl
run′ H B | error E = error E refl

run : ∀ {a} B → RunResult {a} ∅ B
run = run′ ∅


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

-- Definition of Pi with fractionals

module PiFrac2 where

-- From the standard library:
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂)

-- The basic types we add:
open import Singleton

infix  80 ●_ 𝟙/●_
infixr 70 _×ᵤ_
infixr 60 _+ᵤ_
infixr 50 _⊚_

------------------------------------------------------------------------------
-- Pi with fractionals

-- The following are all mutually dependent:

data 𝕌 : Set                               -- 𝕌niverse of types
⟦_⟧ : (A : 𝕌) → Set                        -- denotation of types
data _⟷_ : 𝕌 → 𝕌 → Set                     -- type equivalences
eval : {A B : 𝕌} → (A ⟷ B) → ⟦ A ⟧ → ⟦ B ⟧ -- evaluating an equivalence

data 𝕌 where
  𝟘       : 𝕌
  𝟙       : 𝕌
  _+ᵤ_    : 𝕌 → 𝕌 → 𝕌
  _×ᵤ_    : 𝕌 → 𝕌 → 𝕌
  ●_   : {A : 𝕌} → ⟦ A ⟧ → 𝕌
  𝟙/●_ : {A : 𝕌} → ⟦ A ⟧ → 𝕌

⟦ 𝟘 ⟧ = ⊥
⟦ 𝟙 ⟧ = ⊤
⟦ t₁ +ᵤ t₂ ⟧ = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ t₁ ×ᵤ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧
⟦ ● v ⟧ = Singleton _ v
⟦ 𝟙/● v ⟧ = Recip _ v

data _⟷_ where
  unite₊l : {t : 𝕌} → 𝟘 +ᵤ t ⟷ t
  uniti₊l : {t : 𝕌} → t ⟷ 𝟘 +ᵤ t
  unite₊r : {t : 𝕌} → t +ᵤ 𝟘 ⟷ t
  uniti₊r : {t : 𝕌} → t ⟷ t +ᵤ 𝟘
  swap₊   : {t₁ t₂ : 𝕌} → t₁ +ᵤ t₂ ⟷ t₂ +ᵤ t₁
  assocl₊ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤ (t₂ +ᵤ t₃) ⟷ (t₁ +ᵤ t₂) +ᵤ t₃
  assocr₊ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) +ᵤ t₃ ⟷ t₁ +ᵤ (t₂ +ᵤ t₃)
  unite⋆l : {t : 𝕌} → 𝟙 ×ᵤ t ⟷ t
  uniti⋆l : {t : 𝕌} → t ⟷ 𝟙 ×ᵤ t
  unite⋆r : {t : 𝕌} → t ×ᵤ 𝟙 ⟷ t
  uniti⋆r : {t : 𝕌} → t ⟷ t ×ᵤ 𝟙
  swap⋆   : {t₁ t₂ : 𝕌} → t₁ ×ᵤ t₂ ⟷ t₂ ×ᵤ t₁
  assocl⋆ : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ ×ᵤ t₃) ⟷ (t₁ ×ᵤ t₂) ×ᵤ t₃
  assocr⋆ : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₂) ×ᵤ t₃ ⟷ t₁ ×ᵤ (t₂ ×ᵤ t₃)
  absorbr : {t : 𝕌} → 𝟘 ×ᵤ t ⟷ 𝟘
  absorbl : {t : 𝕌} → t ×ᵤ 𝟘 ⟷ 𝟘
  factorzr : {t : 𝕌} → 𝟘 ⟷ t ×ᵤ 𝟘
  factorzl : {t : 𝕌} → 𝟘 ⟷ 𝟘 ×ᵤ t
  dist    : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) ×ᵤ t₃ ⟷ (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃)
  factor  : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃) ⟷ (t₁ +ᵤ t₂) ×ᵤ t₃
  distl   : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ +ᵤ t₃) ⟷ (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃)
  factorl : {t₁ t₂ t₃ : 𝕌 } → (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃) ⟷ t₁ ×ᵤ (t₂ +ᵤ t₃)
  id⟷     : {t : 𝕌} → t ⟷ t
  _⊚_     : {t₁ t₂ t₃ : 𝕌} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ +ᵤ t₂ ⟷ t₃ +ᵤ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ ×ᵤ t₂ ⟷ t₃ ×ᵤ t₄)
  -- new operations on Singleton
{--
  lift : {t₁ t₂ : 𝕌} → {v₁ : ⟦ t₁ ⟧} →
           (c : t₁ ⟷ t₂) →
           ((● v₁) ⟷ (● (eval c v₁)))
  tensorl : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            ●_ {A = t₁ ×ᵤ t₂} (v₁ , v₂) ⟷ ● v₁ ×ᵤ ● v₂
  tensorr : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            ● v₁ ×ᵤ ● v₂ ⟷ ●_ {A = t₁ ×ᵤ t₂} (v₁ , v₂)
  plusll : {t₁ t₂ : 𝕌} {v : ⟦ t₁ ⟧} →
            ●_ {A = t₁ +ᵤ t₂} (inj₁ v) ⟷ ● v
  pluslr : {t₁ t₂ : 𝕌} {v : ⟦ t₁ ⟧} →
             ● v ⟷ ●_ {A = t₁ +ᵤ t₂} (inj₁ v)
  plusrl : {t₁ t₂ : 𝕌} {v : ⟦ t₂ ⟧} →
            ●_ {A = t₁ +ᵤ t₂} (inj₂ v) ⟷ ● v
  plusrr : {t₁ t₂ : 𝕌} {v : ⟦ t₂ ⟧} →
             ● v ⟷ ●_ {A = t₁ +ᵤ t₂} (inj₂ v)
  fracl : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            𝟙/●_ {A = t₁ ×ᵤ t₂} (v₁ , v₂) ⟷ 𝟙/● v₁ ×ᵤ 𝟙/● v₂
  fracr : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            𝟙/● v₁ ×ᵤ 𝟙/● v₂ ⟷ 𝟙/●_ {A = t₁ ×ᵤ t₂} (v₁ , v₂)
--}
  -- fractionals
  η : {t : 𝕌} → (v : ⟦ t ⟧) → 𝟙 ⟷ ● v ×ᵤ 𝟙/● v
  ε : {t : 𝕌} → (v : ⟦ t ⟧) → ● v ×ᵤ 𝟙/● v ⟷ 𝟙
  -- double lift prop eq
{--
  ll : ∀ {t : 𝕌} {v : ⟦ t ⟧} {w : ⟦ ● v ⟧} →
        ●_ {A = ● v} w  ⟷ ● v
  == : ∀ {t₁ t₂ : 𝕌} {v : ⟦ t₁ ⟧} {w w' : ⟦ t₂ ⟧} →
       (● v ⟷ ● w) → (w ≡ w') → (● v ⟷ ● w')
--}

eval unite₊l (inj₂ v) = v
eval uniti₊l v  = inj₂ v
eval unite₊r (inj₁ v) = v
eval uniti₊r v  = inj₁ v
eval swap₊ (inj₁ v) = inj₂ v
eval swap₊ (inj₂ v) = inj₁ v
eval assocl₊ (inj₁ v) = inj₁ (inj₁ v)
eval assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
eval assocl₊ (inj₂ (inj₂ v)) = inj₂ v
eval assocr₊ (inj₁ (inj₁ v)) = inj₁ v
eval assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
eval assocr₊ (inj₂ v) = inj₂ (inj₂ v)
eval unite⋆l (tt , v) = v
eval uniti⋆l v = (tt , v)
eval unite⋆r (v , tt) = v
eval uniti⋆r v = (v , tt)
eval swap⋆ (v₁ , v₂)          = (v₂ , v₁)
eval assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
eval assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
eval absorbl ()
eval absorbr ()
eval factorzl ()
eval factorzr ()
eval dist (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
eval dist (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
eval factor (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
eval factor (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)
eval distl (v , inj₁ v₁) = inj₁ (v , v₁)
eval distl (v , inj₂ v₂) = inj₂ (v , v₂)
eval factorl (inj₁ (v , v₁)) = (v , inj₁ v₁)
eval factorl (inj₂ (v , v₂)) = (v , inj₂ v₂)
eval id⟷ v = v
eval (c₁ ⊚ c₂) v = eval c₂ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₁ v) = inj₁ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₂ v) = inj₂ (eval c₂ v)
eval (c₁ ⊗ c₂) (v₁ , v₂) = (eval c₁ v₁ , eval c₂ v₂)
{--
eval (lift c) (w , v≡w) = eval c w , cong (eval c) v≡w
eval tensorl ((w₁ , w₂) , vp≡wp) =
  (w₁ , cong proj₁ vp≡wp) , (w₂ , cong proj₂ vp≡wp)
eval tensorr ((w₁ , p₁) , (w₂ , p₂)) =
  (w₁ , w₂) , cong₂ _,_ p₁ p₂
--}
eval (η v) tt = (v , refl) , λ _ → tt
eval (ε v) (p , f) = f p
{--
eval (plusll {v = .w₁}) (inj₁ w₁ , refl) = w₁ , refl
eval pluslr (v₁ , refl) = inj₁ v₁ , refl
eval (plusrl {v = .w₂}) (inj₂ w₂ , refl) = w₂ , refl
eval plusrr (v₂ , refl) = inj₂ v₂ , refl
eval (fracl {v₁ = v₁} {v₂ = v₂}) f = (λ _ → f ((v₁ , v₂) , refl)) , (λ _ → f ((v₁ , v₂) , refl))
eval fracr (f₁ , f₂) ((w₁ , w₂) , refl) = let _ = f₁ (w₁ , refl) ; _ = f₂ (w₂ , refl) in tt
eval (ll {t} {v} {.w}) (w , refl) = v , refl
eval (== c eq) s₁ = let (w₂ , p) = eval c s₁ in w₂ , trans (sym eq) p
--}

-- monad/comonad pair

{--

focus : {t : 𝕌} → (v : ⟦ t ⟧) → Singleton ⟦ t ⟧ v
focus v = (v , refl)

unfocus : {t : 𝕌} {v : ⟦ t ⟧} → Singleton ⟦ t ⟧ v → ⟦ t ⟧
unfocus (v , refl) = v

open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; subst)

------------------------------------------------------------------------------
-- Useful for examples

infixr 2  _⟷⟨_⟩_
infix  3  _□

_⟷⟨_⟩_ : (t₁ : 𝕌) {t₂ : 𝕌} {t₃ : 𝕌} →
          (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
_ ⟷⟨ α ⟩ β = α ⊚ β

_□ : (t : 𝕌) → {t : 𝕌} → (t ⟷ t)
_□ t = id⟷

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

𝔹 : 𝕌
𝔹 = 𝟙 +ᵤ 𝟙

𝔹² : 𝕌
𝔹² = 𝔹 ×ᵤ 𝔹

𝔽 𝕋 : ⟦ 𝔹 ⟧
𝔽 = inj₁ tt
𝕋 = inj₂ tt

not : ⟦ 𝔹 ⟧ → ⟦ 𝔹 ⟧
not (inj₁ tt) = inj₂ tt
not (inj₂ tt) = inj₁ tt

-- this version might look more contrived that the fully expanded
-- one via pattern matching, but it generalizes better.
controlled : ∀ {A} → (⟦ A ⟧ → ⟦ A ⟧) → ⟦ 𝔹 ⟧ × ⟦ A ⟧ → ⟦ 𝔹 ⟧ × ⟦ A ⟧
controlled f (b , a) = (b , [ (λ _ → a) , (λ _ → f a) ]′ b)
-- controlled f (inj₁ tt , a) = (inj₁ tt , a  )
-- controlled f (inj₂ tt , a) = (inj₂ tt , f a)

------------------------------------------------------------------------------
-- Examples

zigzag : ∀ b → ●_ {𝔹} b ⟷ ● b
zigzag b =
  uniti⋆l ⊚                -- ONE * POINTED TWO
  (η b ⊗ id⟷) ⊚          -- (POINTED TWO * RECIP TWO) * POINTED TWO
  assocr⋆ ⊚                -- POINTED TWO * (RECIP TWO * POINTED TWO)
  (id⟷ ⊗ swap⋆) ⊚         -- POINTED TWO * (POINTED TWO * RECIP TWO)
  (id⟷ ⊗ ε b) ⊚           -- POINTED TWO * ONE
  unite⋆r

test1 = eval (zigzag 𝔽) (𝔽 , refl)      -- (⇑ #f refl)
-- test2 = eval (zigzag 𝔽) (𝕋 , refl)   -- typechecks if given proof #f=#t
-- test3 = eval (zigzag 𝕋) (𝔽 , refl)   -- typechecks if given proof #f=#t
test4 = eval (zigzag 𝕋) (𝕋 , refl)      -- (⇑ #t refl)

zigzagU : ⟦ 𝔹 ⟧ → ⟦ 𝔹 ⟧
zigzagU b = unfocus (eval (zigzag b) (focus b))

-- Conventional PI examples

NOT : 𝔹 ⟷ 𝔹
NOT = swap₊

NEG1 NEG2 NEG3 NEG4 NEG5 : 𝔹 ⟷ 𝔹
NEG1 = swap₊
NEG2 = id⟷ ⊚ NOT
NEG3 = NOT ⊚ NOT ⊚ NOT
NEG4 = NOT ⊚ id⟷
NEG5 = uniti⋆l ⊚ swap⋆ ⊚ (NOT ⊗ id⟷) ⊚ swap⋆ ⊚ unite⋆l
NEG6 = uniti⋆r ⊚ (NOT ⊗ id⟷) ⊚ unite⋆r -- same as above, but shorter

CNOT : 𝔹² ⟷ 𝔹²
CNOT =
  𝔹 ×ᵤ 𝔹                ⟷⟨ id⟷ ⟩
  (x +ᵤ y) ×ᵤ 𝔹         ⟷⟨ dist ⟩
  (x ×ᵤ 𝔹) +ᵤ (y ×ᵤ 𝔹)  ⟷⟨ id⟷ ⊕ (id⟷ ⊗ NOT) ⟩
  (x ×ᵤ 𝔹) +ᵤ (y ×ᵤ 𝔹)  ⟷⟨ factor ⟩
  (x +ᵤ y) ×ᵤ 𝔹         ⟷⟨ id⟷ ⟩
  𝔹 ×ᵤ 𝔹 □
  where x = 𝟙; y = 𝟙

TOFFOLI : 𝔹 ×ᵤ 𝔹² ⟷ 𝔹 ×ᵤ 𝔹²
TOFFOLI =
  𝔹 ×ᵤ 𝔹²                 ⟷⟨ id⟷ ⟩
  (x +ᵤ y) ×ᵤ 𝔹²          ⟷⟨ dist ⟩
  (x ×ᵤ 𝔹²) +ᵤ (y ×ᵤ 𝔹²)  ⟷⟨ id⟷ ⊕ (id⟷ ⊗ CNOT) ⟩
  (x ×ᵤ 𝔹²) +ᵤ (y ×ᵤ 𝔹²)  ⟷⟨ factor ⟩
  (x +ᵤ y) ×ᵤ 𝔹²          ⟷⟨ id⟷ ⟩
  𝔹 ×ᵤ 𝔹² □
  where x = 𝟙; y = 𝟙

PERES : (𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹 ⟷ (𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹
PERES = (id⟷ ⊗ NOT) ⊚ assocr⋆ ⊚ (id⟷ ⊗ swap⋆) ⊚
        TOFFOLI ⊚
        (id⟷ ⊗ (NOT ⊗ id⟷)) ⊚
        TOFFOLI ⊚
        (id⟷ ⊗ swap⋆) ⊚ (id⟷ ⊗ (NOT ⊗ id⟷)) ⊚
        TOFFOLI ⊚
        (id⟷ ⊗ (NOT ⊗ id⟷)) ⊚ assocl⋆

SWAP12 SWAP23 SWAP13 ROTL ROTR : 𝟙 +ᵤ 𝟙 +ᵤ 𝟙 ⟷ 𝟙 +ᵤ 𝟙 +ᵤ 𝟙
SWAP12 = assocl₊ ⊚ (swap₊ ⊕ id⟷) ⊚ assocr₊
SWAP23 = id⟷ ⊕ swap₊
SWAP13 = SWAP23 ⊚ SWAP12 ⊚ SWAP23
ROTR   = SWAP12 ⊚ SWAP23
ROTL   = SWAP13 ⊚ SWAP23

t3 : ∀ {b₁ b₂} →
     ● (𝔽 , (b₁ , b₂)) ⟷
     ● (𝔽 , (b₁ , b₂))
t3 = lift TOFFOLI

{--
The following do not typecheck. Good

t4 : ● (𝔹 ×ᵤ 𝔹²) [ 𝕋 , (𝔽 , 𝔽) ] ⟷
     ● (𝔹 ×ᵤ 𝔹²) [ 𝕋 , (𝔽 , 𝕋) ]
t4 = lift TOFFOLI

t5 : ∀ {b₁ b₂} →
     ● (𝔹 ×ᵤ 𝔹²) [ b₁ , (𝔽 , b₂) ] ⟷
     ● (𝔹 ×ᵤ 𝔹²) [ b₁ , (𝔽 , b₂) ]
t5 = lift TOFFOLI
--}

t6 : ∀ {b} →
     ● (𝕋 , (𝕋 , b)) ⟷
     ● (𝕋 , (𝕋 , eval NOT b))
t6 = lift TOFFOLI

-- Ancilla examples from literature

-- Fig. 2 in Ricercar

CONTROLLED : {A : 𝕌} → (A ⟷ A) → 𝔹 ×ᵤ A ⟷ 𝔹 ×ᵤ A
CONTROLLED c = dist ⊚ (id⟷ ⊕ (id⟷ ⊗ c)) ⊚ factor

fig2a : 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ⟷
        𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹
fig2a = CONTROLLED (CONTROLLED (CONTROLLED NOT))

-- first write the circuit with the additional ancilla

fig2b' : ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹) ⟷ ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹)
fig2b' =
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (id⟷ ⊗ CONTROLLED (CONTROLLED NOT))  -- first ccnot
  ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷)                        -- move it back
  ⊚
  (assocl⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (id⟷ ⊗ swap⋆) ⊚
  (id⟷ ⊗ CONTROLLED (CONTROLLED NOT))  -- second ccnot
  ⊚
  (id⟷ ⊗ swap⋆) ⊚
  assocl⋆ ⊚
  (assocr⋆ ⊗ id⟷)                      -- move it back
  ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (id⟷ ⊗ CONTROLLED (CONTROLLED NOT))  -- third ccnot
  ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷)                        -- move it back

-- then prove a theorem that specifies its semantics

fig2b'≡ : (a b c d : ⟦ 𝔹 ⟧) →
          proj₂ (eval fig2b' ((a , b , c , d) , 𝔽)) ≡ 𝔽
fig2b'≡ a         (inj₁ tt) c d = refl
fig2b'≡ (inj₁ tt) (inj₂ tt) c d = refl
fig2b'≡ (inj₂ tt) (inj₂ tt) c d = refl

-- generalize above?  Method:
-- for 'dist' to evaluate, need to split on b first
--   in first case, split on e (same reason)
--   in second case, split on a (same reason)
--     split on e
--     split on e
foo : (a b c d e : ⟦ 𝔹 ⟧) →
          proj₂ (eval fig2b' ((a , b , c , d) , e)) ≡ e
foo a         (inj₁ x) c d (inj₁ x₁) = refl
foo a         (inj₁ x) c d (inj₂ y)  = refl
foo (inj₁ x)  (inj₂ y) c d (inj₁ x₁) = refl
foo (inj₁ x)  (inj₂ y) c d (inj₂ y₁) = refl
foo (inj₂ y₁) (inj₂ y) c d (inj₁ x)  = refl
foo (inj₂ y₁) (inj₂ y) c d (inj₂ y₂) = refl

postulate
  -- boring...
  tensor4 : ∀ {a b c d e} →
          (●_ {𝔹} a ×ᵤ ●_ {𝔹} b ×ᵤ ●_ {𝔹} c ×ᵤ ●_ {𝔹} d) ×ᵤ ●_ {𝔹} e ⟷
          ●_ {(𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹} ((a , b , c , d) , e)
  itensor4 : ∀ {a b c d e} →
          ●_ {(𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹} ((a , b , c , d) , e) ⟷
          (● a ×ᵤ ● b ×ᵤ ● c ×ᵤ ● d)  ×ᵤ ● e

-- now lift it

fig2b : ∀ {a b c d e} →
        let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
        in
           ● a ×ᵤ ● b ×ᵤ ● c ×ᵤ ● d ⟷
           ● x ×ᵤ ● y ×ᵤ ● z ×ᵤ ● w
fig2b {a} {b} {c} {d} {e} =
  let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
  in    uniti⋆r ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝟙[e]
        (id⟷ ⊗ η e) ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × (●𝔹[e] x ●1/𝔹[e])
        assocl⋆ ⊚
        -- ((●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝔹[e) x ●1/𝔹[e]
        (tensor4 ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (a,b,c,d),e ] x ●1/𝔹[e]
        (lift fig2b' ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (x,y,z,w),e ] x ●1/𝔹[e]
        (((== id⟷ (cong (λ H → ((x , y , z , w)) , H) (foo a b c d e))) ⊗ id⟷)) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (x,y,z,w),e ] x ●1/𝔹[e]
        (itensor4 ⊗ id⟷) ⊚
         -- ((●𝔹[x] × ●𝔹[y] × ●𝔹[z] × ●𝔹[w]) × ●𝔹[e]) x ●1/𝔹[e]
        assocr⋆ ⊚
        (id⟷ ⊗ ε e) ⊚
        unite⋆r

-- This is mostly to show that == is really 'subst' in hiding.
fig2b₂ : ∀ {a b c d e} →
        let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
        in
           ● a ×ᵤ ● b ×ᵤ ● c ×ᵤ ● d ⟷
           ● x ×ᵤ ● y ×ᵤ ● z ×ᵤ ● w
fig2b₂ {a} {b} {c} {d} {e} =
  let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
  in    uniti⋆r ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝟙[e]
        (id⟷ ⊗ η e) ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × (●𝔹[e] x ●1/𝔹[e])
        assocl⋆ ⊚
        -- ((●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝔹[e) x ●1/𝔹[e]
        (tensor4 ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (a,b,c,d),e ] x ●1/𝔹[e]
        (lift fig2b' ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (x,y,z,w),e ] x ●1/𝔹[e]
        (itensor4 ⊗ id⟷) ⊚
         -- ((●𝔹[x] × ●𝔹[y] × ●𝔹[z] × ●𝔹[w]) × ●𝔹[e]) x ●1/𝔹[e]
        assocr⋆ ⊚
        (id⟷ ⊗ (subst (λ ee → ● ee ×ᵤ 𝟙/● e ⟷ 𝟙) (sym (foo a b c d e)) (ε e))) ⊚
        unite⋆r

open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)

open import Data.Product using (Σ; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_; subst)

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

dual : {A B : 𝕌} → (f : A ⟷ B) → (v : ⟦ A ⟧ ) →
                   (𝟙/● (eval f v) ⟷ 𝟙/● v)
dual f v = uniti⋆l ⊚ (η v ⊗ id⟷) ⊚ ((lift f ⊗ id⟷) ⊗ id⟷) ⊚
  assocr⋆ ⊚ (id⟷ ⊗ swap⋆) ⊚ assocl⋆ ⊚ (ε (eval f v) ⊗ id⟷) ⊚ unite⋆l

-- name, coname
name : {A B : 𝕌} → (f : A ⟷ B) → (v : ⟦ A ⟧ ) → 𝟙 ⟷ ● (eval f v) ×ᵤ 𝟙/● v
name f v = η v ⊚ (lift f ⊗ id⟷)

coname : {A B : 𝕌} → (f : A ⟷ B) → (v : ⟦ A ⟧ ) → ● v ×ᵤ 𝟙/● (eval f v) ⟷ 𝟙
coname f v = (lift f ⊗ id⟷) ⊚ ε (eval f v)

-- and 'trace' reveals something neat: we can't choose just any random 'a' and 'c'
-- to start with, but we need that make a coherence choice of a and c !!
trace : {A B C : 𝕌} (a : ⟦ A ⟧ ) → (f : A ×ᵤ C ⟷ B ×ᵤ C) →
  (coh : Σ ⟦ C ⟧ (λ c → proj₂ (eval f (a , c)) ≡ c)) →
  ● a ⟷ ● (proj₁ (eval f (a , proj₁ coh)))
trace {A} {B} {C} a f (c , choice) =
  uniti⋆r ⊚        -- A ×ᵤ 1
  (id⟷ ⊗ η c) ⊚   -- A ×ᵤ (C ×ᵤ 1/C)
  assocl⋆ ⊚       -- (A ×ᵤ C) ×ᵤ 1/C
  (tensorr ⊗ id⟷) ⊚ -- bring in the ●
  (lift f ⊗ id⟷) ⊚ -- (B ×ᵤ C) ×ᵤ 1/C
  (tensorl ⊗ id⟷) ⊚ -- bring out the ●
  assocr⋆ ⊚          -- B ×ᵤ (C ×ᵤ 1/C)
  (id⟷ ⊗ (subst fixer choice id⟷ ⊚ ε c)) ⊚ -- B ×ᵤ 1
  unite⋆r
  where
    fixer : ⟦ C ⟧ → Set
    fixer d = (● (proj₂ (eval f (a , c))) ×ᵤ 𝟙/● d) ⟷ (● d ×ᵤ 𝟙/● d)

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

-- Example in Sec. 4.3 from Abramsky's paper
-- http://www.cs.ox.ac.uk/files/341/calco05.pdf

q : {A1 A2 A3 A4 B1 B2 B3 B4 : 𝕌} →
  (f1 : A1 ⟷ B2) →
  (f2 : A2 ⟷ B4) →
  (f3 : A3 ⟷ B3) →
  (f4 : A4 ⟷ B1) →
  A1 ×ᵤ (A2 ×ᵤ (A3 ×ᵤ A4)) ⟷ B1 ×ᵤ (B2 ×ᵤ (B3 ×ᵤ B4))
q {A1} {A2} {A3} {A4} {B1} {B2} {B3} {B4} f1 f2 f3 f4 =
  (A1 ×ᵤ A2 ×ᵤ A3 ×ᵤ A4)     ⟷⟨ f1 ⊗ (f2 ⊗ (f3 ⊗ f4)) ⟩
  (B2 ×ᵤ B4 ×ᵤ B3 ×ᵤ B1)     ⟷⟨ assocl⋆ ⟩
  (B2 ×ᵤ B4) ×ᵤ (B3 ×ᵤ B1)   ⟷⟨ swap⋆ ⟩
  (B3 ×ᵤ B1) ×ᵤ (B2 ×ᵤ B4)   ⟷⟨ swap⋆ ⊗ id⟷ ⟩
  (B1 ×ᵤ B3) ×ᵤ (B2 ×ᵤ B4)   ⟷⟨ assocr⋆ ⊚ (id⟷ ⊗ assocl⋆) ⟩
  B1 ×ᵤ ((B3 ×ᵤ B2) ×ᵤ B4)   ⟷⟨ id⟷ ⊗ ((swap⋆ ⊗ id⟷) ⊚ assocr⋆) ⟩
  B1 ×ᵤ (B2 ×ᵤ (B3 ×ᵤ B4)) □

q' : {A1 U2 U3 U4 B1 : 𝕌} →
  (f1 : A1 ⟷ U2) →
  (f2 : U2 ⟷ U4) →
  (f3 : U3 ⟷ U3) →
  (f4 : U4 ⟷ B1) → (v : ⟦ A1 ⟧) (u3 : ⟦ U3 ⟧)  → (u3-fix : eval f3 u3 ≡ u3) →
  let u2 = eval f1 v in
  let u4 = eval f2 u2 in
  ● v ⟷ ● (proj₁ (eval (q f1 f2 f3 f4) (v , u2 , u3 , u4)))
q' f1 f2 f3 f4 v u3 u3fix =
  trace v (q f1 f2 f3 f4) (( u2 , ( u3 , u4 ) ), cong₂ _,_ refl (cong₂ _,_ u3fix refl))
  where
    u2 = eval f1 v
    u3′ = eval f3 u3
    u4 = eval f2 u2

-- The point is that q' acts in a very particular way:
q'-closed-form : {A1 U2 U3 U4 B1 : 𝕌} →
  (f1 : A1 ⟷ U2) →
  (f2 : U2 ⟷ U4) →
  (f3 : U3 ⟷ U3) →
  (f4 : U4 ⟷ B1) → (u3 : ⟦ U3 ⟧) (u3-fix : eval f3 u3 ≡ u3) → (v : ⟦ A1 ⟧) →
  proj₁ (eval (q' f1 f2 f3 f4 v u3 u3-fix) (v , refl)) ≡ eval (f1 ⊚ f2 ⊚ f4) v
q'-closed-form f1 f2 f3 f4 u3 u3fix v = refl

---------------------------------------------------------------------------------
-- I think the examples below are 'obsolete', in the sense that the one above
-- is more faithful to the original, and more general too.  Delete?
p : {A1 A2 A3 A4 : 𝕌} →
    (A1 ×ᵤ A2) ×ᵤ (A3 ×ᵤ A4) ⟷ (A2 ×ᵤ A4) ×ᵤ (A3 ×ᵤ A1)
p = (swap⋆ ⊗ swap⋆) ⊚
       assocr⋆ ⊚ (id⟷ ⊗ assocl⋆) ⊚ (id⟷ ⊗ (swap⋆ ⊗ id⟷)) ⊚
       (id⟷ ⊗ assocr⋆) ⊚ assocl⋆ ⊚ (id⟷ ⊗ swap⋆)

p' : {A1 A2 A3 A4 : 𝕌} →
    ((A1 ×ᵤ A2) ×ᵤ A4) ×ᵤ A3 ⟷ ((A2 ×ᵤ A4) ×ᵤ A1) ×ᵤ A3
p' = assocr⋆ ⊚ (id⟷ ⊗ swap⋆) ⊚ p ⊚ (id⟷ ⊗ swap⋆) ⊚ assocl⋆

p2 : 𝔹 ×ᵤ (𝔹 ×ᵤ (𝔹 ×ᵤ 𝔹)) ⟷ 𝔹 ×ᵤ (𝔹 ×ᵤ (𝔹 ×ᵤ 𝔹))
p2 = assocl⋆ ⊚ (swap⋆ ⊗ swap⋆) ⊚
       assocr⋆ ⊚ (id⟷ ⊗ assocl⋆) ⊚ (id⟷ ⊗ (swap⋆ ⊗ id⟷)) ⊚
       (id⟷ ⊗ assocr⋆) ⊚ assocl⋆ ⊚ (id⟷ ⊗ swap⋆) ⊚ assocr⋆

p2' : (v : ⟦ 𝔹 ⟧) →
      ● v ⟷ ● (proj₁ (proj₁ (eval p ((v , v) , (v , v)))))
p2' v = trace v p2 ((v , (v , v)) , refl)

---------------------------------------------------------------------------------
-- Examples inspired by compact closed categories and fractional numbers.

-- Intuition:
-- 1/A x B is a space transformer; takes A space and returns B space
-- denote space transformers as A ⊸ B

-- Best we can do:
-- we need Singletons, so |a ⊸ b| is 1 component of a function.

_⊸_ : {A : 𝕌} → (a : ⟦ A ⟧) → {B : 𝕌} → (b : ⟦ B ⟧) → 𝕌
_⊸_ {A} a {B} b = 𝟙/● a ×ᵤ ● b

id⊸ : {A : 𝕌} {a : ⟦ A ⟧} → (a ⊸ a) ⟷ 𝟙
id⊸ {A} {a} =
  (𝟙/● a ×ᵤ ● a) ⟷⟨ swap⋆ ⟩
  (● a ×ᵤ 𝟙/● a) ⟷⟨ ε a ⟩
  𝟙 □

comp⊸ : {A B C : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} {c : ⟦ C ⟧} →
        (a ⊸ b) ×ᵤ (b ⊸ c) ⟷ (a ⊸ c)
comp⊸ {A} {B} {C} {a} {b} {c} =
  (𝟙/● a ×ᵤ ● b) ×ᵤ (𝟙/● b ×ᵤ ● c) ⟷⟨ assocr⋆ ⟩
  𝟙/● a ×ᵤ (● b ×ᵤ (𝟙/● b ×ᵤ ● c)) ⟷⟨ id⟷ ⊗ assocl⋆ ⟩
  𝟙/● a ×ᵤ (● b ×ᵤ 𝟙/● b) ×ᵤ ● c   ⟷⟨ id⟷ ⊗ (ε b ⊗ id⟷) ⟩
  𝟙/● a ×ᵤ (𝟙 ×ᵤ ● c)                          ⟷⟨ id⟷ ⊗ unite⋆l ⟩
  𝟙/● a ×ᵤ ● c □

app : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} → (a ⊸ b) ×ᵤ ● a ⟷ ● b
app {A} {B} {a} {b} =
  (𝟙/● a ×ᵤ ● b) ×ᵤ ● a ⟷⟨ swap⋆ ⊗ id⟷ ⟩
  (● b ×ᵤ 𝟙/● a) ×ᵤ ● a ⟷⟨ assocr⋆ ⊚ (id⟷ ⊗ (swap⋆ ⊚ ε a)) ⟩
  ● b ×ᵤ 𝟙                          ⟷⟨ unite⋆r ⟩
  ● b □

-- B/A × D/C ⟷ B × D / A × C
dist×/ : {A B C D : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} {c : ⟦ C ⟧} {d : ⟦ D ⟧}
       → (a ⊸ b) ×ᵤ (c ⊸ d) ⟷ ((a , c) ⊸ (b , d))
dist×/ {A} {B} {C} {D} {a} {b} {c} {d} =
  (𝟙/● a ×ᵤ ● b) ×ᵤ (𝟙/● c ×ᵤ ● d) ⟷⟨ assocr⋆ ⊚ (id⟷ ⊗ assocl⋆) ⟩
  (𝟙/● a ×ᵤ (● b ×ᵤ 𝟙/● c) ×ᵤ ● d) ⟷⟨ id⟷ ⊗ (swap⋆ ⊗ id⟷) ⟩
  (𝟙/● a ×ᵤ (𝟙/● c ×ᵤ ● b) ×ᵤ ● d) ⟷⟨ (id⟷ ⊗ assocr⋆) ⊚ assocl⋆ ⟩
  (𝟙/● a ×ᵤ 𝟙/● c) ×ᵤ (● b ×ᵤ ● d) ⟷⟨ fracr ⊗ tensorr ⟩
  (𝟙/●_ {A ×ᵤ C} (a , c)) ×ᵤ (●_ {B ×ᵤ D} (b , d)) □

-- 1/A x 1/B <-> 1 / (A x B)
rev× : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧}
     → (a ⊸ tt) ×ᵤ (b ⊸ tt) ⟷ ((a , b) ⊸ tt)
rev× {A} {B} {a} {b} =
  (𝟙/● a ×ᵤ ● tt) ×ᵤ (𝟙/● b ×ᵤ ● tt) ⟷⟨ dist×/ ⟩
  (𝟙/● (a , b) ×ᵤ ● (tt , tt)) ⟷⟨ id⟷ ⊗ lift unite⋆l ⟩
  (𝟙/●_ {A ×ᵤ B} (a , b) ×ᵤ ● tt) □

{--
trivial : ● 𝟙 [ tt ] ⟷ 𝟙
trivial = {!!}
--}

-- (A <-> B) -> (1/A <-> 1/B)
--rev : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧}
--     → ● A [ a ] ⟷ ● B [ b ] → (b ⊸ tt) ⟷ (a ⊸ tt)
--  (𝟙/● A [ a ] ×ᵤ ● 𝟙 [ tt ]) ⟷⟨ {!!} ⟩
--  (𝟙/● B [ b ] ×ᵤ ● 𝟙 [ tt ]) □

rev : {A B : 𝕌} {a : ⟦ A ⟧}
     → (f : A ⟷ B) → (𝟙/● (eval f a) ⟷ 𝟙/● a)
rev {A} {B} {a} f = dual f a

-- A <-> 1 / (1/A)
revrev : {A : 𝕌} {a : ⟦ A ⟧} {a⋆ : ⟦ 𝟙/● a ⟧} →
         ● a ⟷ 𝟙/● a⋆
revrev {A} {a} {a⋆} =
  ● a ⟷⟨ uniti⋆r ⟩
  ● a ×ᵤ 𝟙 ⟷⟨ {!id⟷ ⊗ η a⋆!} ⟩
  ● a ×ᵤ (𝟙/● a ×ᵤ 𝟙/● a⋆) ⟷⟨ {!!} ⟩
  𝟙/● a⋆ □

-- this is strange
-- A/C + B/C <-> (A + B) / C
-- factor+/l : {A B C : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} {c : ⟦ C ⟧}
--           → (c ⊸ a) +ᵤ (c ⊸ b) ⟷ (_⊸_ {C} c {A +ᵤ B} (inj₁ a))
-- factor+/l {A} {B} {C} {a} {b} {c} =
--   (𝟙/● C [ c ] ×ᵤ ● A [ a ] +ᵤ 𝟙/● C [ c ] ×ᵤ ● B [ b ]) ⟷⟨ factorl ⟩
--   (𝟙/● C [ c ] ×ᵤ (● A [ a ] +ᵤ ● B [ b ])) ⟷⟨ id⟷ ⊗ {!!} ⟩
--   (𝟙/● C [ c ] ×ᵤ ● A +ᵤ B [ inj₁ a ]) □

-- same issue here with the +
-- A/B + C/D <-> (A x D + B x C) / (B x D)

-- SAT solver Sec. 5 from https://www.cs.indiana.edu/~sabry/papers/rational.pdf

-- can we do this?
-- curry⊸ : {A B C : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} {c : ⟦ C ⟧}
--        → (● A [ a ] ×ᵤ (b ⊸ c)) ⟷ (a ⊸ {!!}) -- what do we put here?
-- curry⊸ {A} {B} {C} {a} {b} {c} = {!!}

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

--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Analysis where

open import Data.List       using (List; []; _∷_; map)

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

open import Harmony
open import Music
open import Note
open import Pitch

-- test of analysis

accompF : List Pitch
accompF = f 4 ∷ a 4 ∷ c 5 ∷ []

xx = pitchClassListToSet (map pitchToClass accompF)
--yy = showPitchClassSet xx

zz : xx ≡ IV-maj
zz = refl

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
open import Everything

{-
open import Oscar.Prelude
open import Oscar.Class.HasEquivalence
open import Oscar.Class.Symmetrical
open import Oscar.Data.Term
open import Oscar.Data.Substitunction
open import Oscar.Data.Surjcollation
open import Oscar.Data.Surjextenscollation
open import Oscar.Data.Proposequality
import Oscar.Class.HasEquivalence.ExtensionṖroperty
import Oscar.Class.HasEquivalence.Ṗroperty
import Oscar.Class.Symmetrical.ExtensionalUnifies
import Oscar.Class.Symmetrical.Unifies
import Oscar.Property.Setoid.Proposequality -- FIXME see _∼⁰_ below; comment this out to observe confusing error messages
import Oscar.Property.Functor.SubstitunctionExtensionTerm
import Oscar.Class.Surjection.⋆
-}

module Test.SymmetricalSubstitunction {𝔭} (𝔓 : Ø 𝔭) (ℓ : Ł) where
  open Term 𝔓 using () renaming (
    Term to 𝑩;
    Terms to 𝑩')
  open Substitunction 𝔓 using () renaming (
    Substitunction to 𝑪)

  infix 18 _∼⁰_
  _∼⁰_ = ≡-surjcollation⟦ 𝑪 ⟧ --  ≡-Unifies₀⟦ 𝑪 ⟧ -- FIXME gives a confusing error message
  -- _∼⁰_ = ≡-SymUnifies₀⟦ 𝑪 ⟧ -- FIXME gives a more useful error message

  open Surjextenscollation 𝑪 _≡̇_ renaming (_⟹_ to _∼¹_)

  fact1⋆ : ∀ {𝓃} (𝓈 𝓉 : 𝑩 𝓃) → 𝓈 ∼⁰ 𝓉 ≈ 𝓉 ∼⁰ 𝓈
  fact1⋆ 𝓈 𝓉 = symmetrical 𝓈 𝓉
  -- fact1⋆ 𝓈 𝓉 = symmetrical ⦃ r = Oscar.Class.Symmetrical.Unifies.𝓢ymmetricalUnifies₀ ⦃ ! ⦄ ⦃ ! ⦄ ⦃ Oscar.Property.Setoid.Proposequality.𝓢ymmetryProposequality ⦄ ⦄ 𝓈 𝓉 -- FIXME I wish Agda would tell us that this is how the instances were resolved

  fact1⋆s : ∀ {N 𝓃} (𝓈 𝓉 : 𝑩' N 𝓃) → 𝓈 ∼⁰ 𝓉 ≈ 𝓉 ∼⁰ 𝓈
  fact1⋆s 𝓈 𝓉 = symmetrical 𝓈 𝓉

  fact1 : ∀ {𝓃} (𝓈 𝓉 : 𝑩 𝓃) → 𝓈 ∼¹ 𝓉 ≈ 𝓉 ∼¹ 𝓈
  fact1 𝓈 𝓉 = symmetrical 𝓈 𝓉

  fact1s : ∀ {N 𝓃} (𝓈 𝓉 : 𝑩' N 𝓃) → 𝓈 ∼¹ 𝓉 ≈ 𝓉 ∼¹ 𝓈
  fact1s 𝓈 𝓉 = symmetrical 𝓈 𝓉