text:
------------------------------------------------------------------------
-- Eliminators and initiality
------------------------------------------------------------------------

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

module Partiality-algebra.Eliminators where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (T)

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

open import Partiality-algebra as PA hiding (id; _∘_)

------------------------------------------------------------------------
-- Eliminators

-- I (NAD) have tried to follow the spirit of the rules for HITs
-- specified in the HoTT-Agda library
-- (https://github.com/HoTT/HoTT-Agda/blob/master/core/lib/types/HIT_README.txt).
-- However, at the time of writing those rules don't apply to indexed
-- types.

-- A specification of a given partiality algebra's eliminator
-- arguments (for given motive sizes).

record Arguments {a p′ q′} {A : Type a} p q
                 (PA : Partiality-algebra p′ q′ A) :
                 Type (a ⊔ lsuc (p ⊔ q) ⊔ p′ ⊔ q′) where

  open Partiality-algebra PA

  -- Predicate transformer related to increasing sequences.

  Inc : (P : T → Type p)
        (Q : ∀ {x y} → P x → P y → x ⊑ y → Type q) →
        Increasing-sequence → Type (p ⊔ q)
  Inc P Q s =
    ∃ λ (p : ∀ n → P (s [ n ])) →
      ∀ n → Q (p n) (p (suc n)) (increasing s n)

  field
    P  : T → Type p
    Q  : ∀ {x y} → P x → P y → x ⊑ y → Type q
    pe : P never
    po : ∀ x → P (now x)
    pl : ∀ s (pq : Inc P Q s) → P (⨆ s)
    pa : ∀ {x y} (x⊑y : x ⊑ y) (x⊒y : x ⊒ y)
         (p-x : P x) (p-y : P y)
         (q-x⊑y : Q p-x p-y x⊑y) (q-x⊒y : Q p-y p-x x⊒y) →
         subst P (antisymmetry x⊑y x⊒y) p-x ≡ p-y
    pp : ∀ {x} → Is-set (P x)
    qr : ∀ x (p : P x) → Q p p (⊑-refl x)
    qt : ∀ {x y z} (x⊑y : x ⊑ y) (y⊑z : y ⊑ z) →
         (px : P x) (py : P y) (pz : P z) →
         Q px py x⊑y → Q py pz y⊑z → Q px pz (⊑-trans x⊑y y⊑z)
    qe : ∀ x (p : P x) → Q pe p (never⊑ x)
    qu : ∀ s (pq : Inc P Q s) n →
         Q (proj₁ pq n) (pl s pq) (upper-bound s n)
    ql : ∀ s ub is-ub (pq : Inc P Q s) (pu : P ub)
         (qu : ∀ n → Q (proj₁ pq n) pu (is-ub n)) →
         Q (pl s pq) pu (least-upper-bound s ub is-ub)
    qp : ∀ {x y} (p-x : P x) (p-y : P y) (x⊑y : x ⊑ y) →
         Is-proposition (Q p-x p-y x⊑y)

-- A specification of a given partiality algebra's eliminators.

record Eliminators {a p q p′ q′} {A : Type a}
                   {PA : Partiality-algebra p′ q′ A}
                   (args : Arguments p q PA) :
                   Type (a ⊔ p ⊔ q ⊔ p′ ⊔ q′) where
  open Partiality-algebra PA
  open Arguments args

  field
    ⊥-rec : (x : T) → P x
    ⊑-rec : ∀ {x y} (x⊑y : x ⊑ y) → Q (⊥-rec x) (⊥-rec y) x⊑y

  inc-rec : (s : Increasing-sequence) → Inc P Q s
  inc-rec = λ { (s , inc) → ( (λ n → ⊥-rec (s   n))
                            , (λ n → ⊑-rec (inc n))
                            ) }

  field

    -- Some "computation" rules.

    ⊥-rec-never : ⊥-rec never ≡ pe
    ⊥-rec-now   : ∀ x → ⊥-rec (now x) ≡ po x
    ⊥-rec-⨆     : ∀ s → ⊥-rec (⨆ s) ≡ pl s (inc-rec s)

-- A specification of the elimination principle for a given partiality
-- algebra (for motives of certain sizes).

Elimination-principle :
  ∀ {a p′ q′} {A : Type a} →
  ∀ p q → Partiality-algebra p′ q′ A → Type (a ⊔ lsuc (p ⊔ q) ⊔ p′ ⊔ q′)
Elimination-principle p q P =
  (args : Arguments p q P) → Eliminators args

------------------------------------------------------------------------
-- Initiality

-- The statement that a given partiality algebra is homotopy-initial.

Initial : ∀ {a p q} p′ q′ {A : Type a} → Partiality-algebra p q A →
          Type (a ⊔ p ⊔ q ⊔ lsuc (p′ ⊔ q′))
Initial p′ q′ {A} P =
  (P′ : Partiality-algebra p′ q′ A) → Contractible (Morphism P P′)

-- If a partiality algebra is initial at certain sizes, then it is
-- also initial at smaller sizes.

lower-initiality :
  ∀ {a p q p₁ q₁} p₂ q₂ {A : Type a}
  (P : Partiality-algebra p q A)
  (initial : Initial (p₁ ⊔ p₂) (q₁ ⊔ q₂) P) →
  Initial p₁ q₁ P
lower-initiality {p₁ = p₁} {q₁} p₂ q₂ {A} P initial P′ =
  Σ-map lower-morphism lemma (initial P″)
  where
  open Partiality-algebra P′

  P″ : Partiality-algebra (p₁ ⊔ p₂) (q₁ ⊔ q₂) A
  P″ = record
    { T                       = ↑ p₂ T
    ; partiality-algebra-with = record
      { _⊑_               = λ x y → ↑ q₂ (lower x ⊑ lower y)
      ; never             = lift never
      ; now               = lift ∘ now
      ; ⨆                 = lift ∘ ⨆ ∘ Σ-map (lower ∘_) (lower ∘_)
      ; antisymmetry      = λ x⊑y y⊑x →
                              cong lift (antisymmetry (lower x⊑y)
                                                      (lower y⊑x))
      ; T-is-set-unused   = λ _ _ → ↑-closure 2 T-is-set _ _
      ; ⊑-refl            = lift ∘ ⊑-refl ∘ lower
      ; ⊑-trans           = λ x⊑y y⊑z →
                              lift (⊑-trans (lower x⊑y)
                                            (lower y⊑z))
      ; never⊑            = lift ∘ never⊑ ∘ lower
      ; upper-bound       = λ _ → lift ∘ upper-bound _
      ; least-upper-bound = λ _ _ →
                              lift ∘
                              least-upper-bound _ _ ∘
                              (lower ∘_)
      ; ⊑-propositional   = ↑-closure 1 ⊑-propositional
      }
    }

  lower-morphism : Morphism P P″ → Morphism P P′
  lower-morphism m = record
    { function     = lower ∘ function
    ; monotone     = lower ∘ monotone
    ; strict       = cong lower strict
    ; now-to-now   = cong lower ∘ now-to-now
    ; ω-continuous = cong lower ∘ ω-continuous
    }
    where
    open Morphism m

  lift-morphism : Morphism P P′ → Morphism P P″
  lift-morphism m = record
    { function     = lift ∘ function
    ; monotone     = lift ∘ monotone
    ; strict       = cong lift strict
    ; now-to-now   = cong lift ∘ now-to-now
    ; ω-continuous = cong lift ∘ ω-continuous
    }
    where
    open Morphism m

  lemma : {m : Morphism P P″} →
          (∀ m′ → m ≡ m′) →
          (∀ m′ → lower-morphism m ≡ m′)
  lemma {m} hyp m′ = _↔_.to equality-characterisation-Morphism
    (lower ∘ Morphism.function m  ≡⟨ cong ((lower ∘_) ∘ Morphism.function) (hyp (lift-morphism m′)) ⟩∎
     Morphism.function m′         ∎)

------------------------------------------------------------------------
-- Specifying the partiality monad using eliminators is logically
-- equivalent (at the meta-level) to specifying it using initiality

-- Any partiality algebra with eliminators (at certain sizes) is
-- initial (at the same sizes).

eliminators→initiality :
  ∀ {a p q p′ q′} {A : Type a} →
  (P : Partiality-algebra p′ q′ A) →
  Elimination-principle p q P →
  Initial p q P
eliminators→initiality {p = p} {q} P elims P′ = morphism , unique
  where
  module P  = Partiality-algebra P
  module P′ = Partiality-algebra P′

  args : Arguments p q P
  args = record
    { P  = λ _ → P′.T
    ; Q  = λ x y _ → x P′.⊑ y
    ; pe = P′.never
    ; po = P′.now
    ; pl = λ _ → P′.⨆
    ; pa = λ x⊑y y⊑x u v u⊑v v⊑u →
             let eq = Partiality-algebra.antisymmetry P x⊑y y⊑x in

             subst (const P′.T) eq u  ≡⟨ subst-const eq ⟩
             u                        ≡⟨ P′.antisymmetry u⊑v v⊑u ⟩∎
             v                        ∎
    ; pp = P′.T-is-set
    ; qr = λ _ → P′.⊑-refl
    ; qt = λ _ _ _ _ _ → P′.⊑-trans
    ; qe = λ _ → P′.never⊑
    ; qu = λ _ → P′.upper-bound
    ; ql = λ _ _ _ → P′.least-upper-bound
    ; qp = λ _ _ _ → P′.⊑-propositional
    }

  module E = Eliminators (elims args)

  morphism : Morphism P P′
  morphism = record
    { function     = E.⊥-rec
    ; monotone     = E.⊑-rec
    ; strict       = E.⊥-rec-never
    ; now-to-now   = E.⊥-rec-now
    ; ω-continuous = E.⊥-rec-⨆
    }

  open Morphism

  function-unique : (f : Morphism P P′) →
                    E.⊥-rec ≡ function f
  function-unique f = sym $ ⟨ext⟩ $ Eliminators.⊥-rec (elims (record
    { Q  = λ _ _ _ → ↑ _ ⊤
    ; pe = function f P.never  ≡⟨ strict f ⟩
           P′.never            ≡⟨ sym $ E.⊥-rec-never ⟩∎
           E.⊥-rec P.never     ∎
    ; po = λ x →
             function f (P.now x)  ≡⟨ now-to-now f x ⟩
             P′.now x              ≡⟨ sym $ E.⊥-rec-now x ⟩∎
             E.⊥-rec (P.now x)     ∎
    ; pl = λ s hyp →
             function f (P.⨆ s)            ≡⟨ ω-continuous f s ⟩
             P′.⨆ (sequence-function f s)  ≡⟨ cong P′.⨆ $ _↔_.to P′.equality-characterisation-increasing (proj₁ hyp) ⟩
             P′.⨆ (E.inc-rec s)            ≡⟨ sym $ E.⊥-rec-⨆ s ⟩
             E.⊥-rec (P.⨆ s)               ∎
    ; pa = λ _ _ _ _ _ _ → P′.T-is-set _ _
    ; pp = λ _ _ → mono₁ 1 P′.T-is-set _ _
    ; qp = λ _ _ _ _ _ → refl
    }))

  unique : ∀ f → morphism ≡ f
  unique f =
    _↔_.to equality-characterisation-Morphism (function-unique f)

-- Any partiality algebra with initiality (at certain sufficiently
-- large sizes) has eliminators (at certain sizes).

initiality→eliminators :
  ∀ {a p q p′ q′} {A : Type a} {P : Partiality-algebra p′ q′ A}
  (initial : Initial (p ⊔ p′) (q ⊔ q′) P) →
  Elimination-principle p q P
initiality→eliminators {p = p} {q} {p′} {q′} {A} {PA} initial args =
  record
    { ⊥-rec       = ⊥-rec
    ; ⊑-rec       = ⊑-rec
    ; ⊥-rec-never = ⊥-rec-never
    ; ⊥-rec-now   = ⊥-rec-now
    ; ⊥-rec-⨆     = ⊥-rec-⨆
    }
  where
  open Partiality-algebra PA

  open Arguments args

  private

    -- A partiality algebra with ∃ P as the carrier type.

    ∃PA : Partiality-algebra (p ⊔ p′) (q ⊔ q′) A
    ∃PA = record
      { T                       = ∃ P
      ; partiality-algebra-with = record
        { _⊑_               = λ { (_ , p) (_ , q) → ∃ (Q p q) }
        ; never             = never , pe
        ; now               = λ x → now x , po x
        ; ⨆                 = λ s → ⨆ (Σ-map (proj₁ ∘_) (proj₁ ∘_) s)
                                  , pl _ ( proj₂ ∘ proj₁ s
                                         , proj₂ ∘ proj₂ s
                                         )
        ; antisymmetry      = λ { {x = (x , p)} {y = (y , q)}
                                  (x⊑y , Qx⊑y) (y⊑x , Qy⊑x) →
                                  Σ-≡,≡→≡
                                    (antisymmetry x⊑y y⊑x)
                                    (pa x⊑y y⊑x p q Qx⊑y Qy⊑x)
                                }
        ; T-is-set-unused   = Σ-closure 2 T-is-set (λ _ → pp)
        ; ⊑-refl            = λ _ → _ , qr _ _
        ; ⊑-trans           = Σ-zip ⊑-trans (qt _ _ _ _ _)
        ; never⊑            = λ _ → _ , qe _ _
        ; upper-bound       = λ _ _ → upper-bound _ _ , qu _ _ _
        ; least-upper-bound = λ _ _ ⊑qs →
                                  least-upper-bound _ _ (proj₁ ∘ ⊑qs)
                                , ql _ _ _ _ _ (proj₂ ∘ ⊑qs)
        ; ⊑-propositional   = Σ-closure 1 ⊑-propositional λ _ → qp _ _ _
        }
      }

    -- Initiality gives us a morphism from PA to ∃PA.

    eliminator-morphism : Morphism PA ∃PA
    eliminator-morphism = proj₁ (initial ∃PA)

    open Morphism eliminator-morphism

    -- We can construct a morphism from ∃PA to PA directly.

    proj₁-morphism : Morphism ∃PA PA
    proj₁-morphism = record
      { function     = proj₁
      ; monotone     = proj₁
      ; strict       = refl
      ; now-to-now   = λ _ → refl
      ; ω-continuous = λ _ → refl
      }

    -- By composing the two morphisms we get an endomorphism on PA.

    id′ : Morphism PA PA
    id′ = proj₁-morphism PA.∘ eliminator-morphism

    -- Due to initiality this morphism must be equal to id.

    id′≡id : id′ ≡ PA.id
    id′≡id =
      let m , unique = lower-initiality p q PA initial PA in

      id′    ≡⟨ sym $ unique id′ ⟩
      m      ≡⟨ unique PA.id ⟩∎
      PA.id  ∎

    abstract

      -- This provides us with a key lemma used to define the
      -- eliminators.

      lemma : ∀ x → proj₁ (function x) ≡ x
      lemma x = cong (λ m → Morphism.function m x) id′≡id

    -- As an aside this means that there is a split surjection from
    -- ∃ P to T.

    ↠T : ∃ P ↠ T
    ↠T = record
      { logical-equivalence = record
        { to   = Morphism.function proj₁-morphism
        ; from = function
        }
      ; right-inverse-of = lemma
      }

  -- The eliminators.

  ⊥-rec : ∀ x → P x
  ⊥-rec x =                 $⟨ proj₂ (function x) ⟩
    P (proj₁ (function x))  ↝⟨ subst P (lemma x) ⟩□
    P x                     □

  ⊑-rec : ∀ {x y} (x⊑y : x ⊑ y) → Q (⊥-rec x) (⊥-rec y) x⊑y
  ⊑-rec {x} {y} x⊑y =                                                   $⟨ proj₂ (monotone x⊑y) ⟩
    Q (proj₂ (function x)) (proj₂ (function y)) (proj₁ (monotone x⊑y))  ↝⟨ subst Q′ $
                                                                             Σ-≡,≡→≡ (cong₂ _,_ (lemma x) (lemma y)) (
        subst (λ xy → P (proj₁ xy) × P (proj₂ xy) ×
                      proj₁ xy ⊑ proj₂ xy)
              (cong₂ _,_ (lemma x) (lemma y))
              ( proj₂ (function x)
              , proj₂ (function y)
              , proj₁ (monotone x⊑y)
              )                                                                 ≡⟨ push-subst-, {y≡z = cong₂ _,_ (lemma x) (lemma y)}
                                                                                (λ xy → P (proj₁ xy))
                                                                                (λ xy → P (proj₂ xy) × proj₁ xy ⊑ proj₂ xy)
                                                                                {p = ( proj₂ (function x)
                                                                                , proj₂ (function y)
                                                                                , proj₁ (monotone x⊑y)
                                                                                )} ⟩
        ( subst (λ xy → P (proj₁ xy))
                (cong₂ _,_ (lemma x) (lemma y))
                (proj₂ (function x))
        , subst (λ xy → P (proj₂ xy) × proj₁ xy ⊑ proj₂ xy)
                (cong₂ _,_ (lemma x) (lemma y))
                ( proj₂ (function y)
                , proj₁ (monotone x⊑y)
                )
        )                                                                       ≡⟨ cong₂ _,_
                                                                                (subst-∘ P proj₁ (cong₂ _,_ (lemma x) (lemma y))
                                                                                {p = proj₂ (function x)})
                                                                                (push-subst-, {y≡z = cong₂ _,_ (lemma x) (lemma y)}
                                                                                (λ xy → P (proj₂ xy))
                                                                                (λ xy → proj₁ xy ⊑ proj₂ xy)
                                                                                {p = ( proj₂ (function y)
                                                                                , proj₁ (monotone x⊑y)
                                                                                )}) ⟩
        ( subst P (cong proj₁ $ cong₂ _,_ (lemma x) (lemma y))
                (proj₂ (function x))
        , subst (λ xy → P (proj₂ xy))
                (cong₂ _,_ (lemma x) (lemma y))
                (proj₂ (function y))
        , subst (λ xy → proj₁ xy ⊑ proj₂ xy)
                (cong₂ _,_ (lemma x) (lemma y))
                (proj₁ (monotone x⊑y))
        )                                                                       ≡⟨ cong₂ _,_
                                                                                (cong (λ p → subst P p (proj₂ (function x))) $
                                                                                cong-proj₁-cong₂-, (lemma x) (lemma y))
                                                                                (cong₂ _,_
                                                                                (subst-∘ P proj₂ (cong₂ _,_ (lemma x) (lemma y))
                                                                                {p = proj₂ (function y)})
                                                                                (⊑-propositional _ _)) ⟩
        ( subst P (lemma x) (proj₂ (function x))
        , subst P (cong proj₂ $ cong₂ _,_ (lemma x) (lemma y))
                (proj₂ (function y))
        , x⊑y
        )                                                                       ≡⟨ cong (λ p → ⊥-rec x , subst P p (proj₂ (function y)) , x⊑y) $
                                                                                cong-proj₂-cong₂-, (lemma x) (lemma y) ⟩∎
        (⊥-rec x , ⊥-rec y , x⊑y)                                               ∎) ⟩□

    Q (⊥-rec x) (⊥-rec y) x⊑y                                           □
    where
    Q′ :
      (∃ λ xy → P (proj₁ xy) × P (proj₂ xy) × proj₁ xy ⊑ proj₂ xy) →
      Type q
    Q′ (_ , px , py , x⊑y) = Q px py x⊑y

  inc-rec : ∀ s → Inc P Q s
  inc-rec (s , inc) = ⊥-rec ∘ s , ⊑-rec ∘ inc

  -- "Computation" rules.

  private

    -- A lemma.

    ⊥-rec-lemma′ :
      ∀ {a b} {A : Type a} {B : A → Type b} {x y : Σ A B} →
      Is-set A →
      x ≡ y → (p : proj₁ x ≡ proj₁ y) →
      subst B p (proj₂ x) ≡ proj₂ y
    ⊥-rec-lemma′ {B = B} A-set =
      elim (λ {x y} _ → (p : proj₁ x ≡ proj₁ y) →
                        subst B p (proj₂ x) ≡ proj₂ y)
           (λ { (_ , x₂) p →
                subst B p x₂     ≡⟨ cong (λ p → subst B p _) $ A-set p refl ⟩
                subst B refl x₂  ≡⟨⟩
                x₂               ∎
              })

    -- A specific instance of the lemma above.

    ⊥-rec-lemma : ∀ {x y} → function x ≡ (x , y) → ⊥-rec x ≡ y
    ⊥-rec-lemma {x} {y} eq =
      ⊥-rec x                                 ≡⟨⟩
      subst P (lemma x) (proj₂ (function x))  ≡⟨ ⊥-rec-lemma′ T-is-set eq (lemma x) ⟩∎
      y                                       ∎

  ⊥-rec-never : ⊥-rec never ≡ pe
  ⊥-rec-never = ⊥-rec-lemma strict

  ⊥-rec-now : ∀ x → ⊥-rec (now x) ≡ po x
  ⊥-rec-now x = ⊥-rec-lemma (now-to-now x)

  ⊥-rec-⨆ : ∀ s → ⊥-rec (⨆ s) ≡ pl s (inc-rec s)
  ⊥-rec-⨆ s = ⊥-rec-lemma
    (function (⨆ s)                                           ≡⟨ ω-continuous s ⟩

     ⨆ (Σ-map (proj₁ ∘_) (proj₁ ∘_) (sequence-function s)) ,
     pl _ ( proj₂ ∘ proj₁ (sequence-function s)
          , proj₂ ∘ proj₂ (sequence-function s)
          )                                                   ≡⟨⟩

     ⨆ ( proj₁ ∘ function ∘ proj₁ s
       , proj₁ ∘ monotone ∘ proj₂ s
       ) ,
     pl _ ( proj₂ ∘ function ∘ proj₁ s
          , proj₂ ∘ monotone ∘ proj₂ s
          )                                                   ≡⟨ Σ-≡,≡→≡ (cong ⨆ lemma₁) lemma₂ ⟩

     ⨆ s , pl s ( ⊥-rec ∘ proj₁ s
                , ⊑-rec ∘ proj₂ s
                )                                             ≡⟨⟩

     ⨆ s , pl s (inc-rec s)                                   ∎)
     where
     lemma₁ =
       ( proj₁ ∘ function ∘ proj₁ s
       , proj₁ ∘ monotone ∘ proj₂ s
       )                             ≡⟨ _↔_.to equality-characterisation-increasing (λ n →
                                          lemma (s [ n ])) ⟩∎
       s                             ∎

     lemma₂ =
       subst P (cong ⨆ lemma₁)
         (pl _ ( proj₂ ∘ function ∘ proj₁ s
               , proj₂ ∘ monotone ∘ proj₂ s
               ))                                         ≡⟨ sym $ subst-∘ P ⨆ lemma₁ ⟩

       subst (P ∘ ⨆) lemma₁
         (pl _ ( proj₂ ∘ function ∘ proj₁ s
               , proj₂ ∘ monotone ∘ proj₂ s
               ))                                         ≡⟨ elim
                                                               (λ {s′ s} eq → ∀ {i′ i} →
                                                                              subst (λ s → ∀ n → P (s [ n ])) eq (proj₁ i′) ≡ proj₁ i →
                                                                              subst (P ∘ ⨆) eq (pl s′ i′) ≡ pl s i)
                                                               (λ s {i′ i} eq →
                                                                  pl s i′  ≡⟨ cong (pl s) (Σ-≡,≡→≡ eq (⟨ext⟩ λ _ → qp _ _ _ _ _)) ⟩∎
                                                                  pl s i   ∎)
                                                               lemma₁
                                                               (⟨ext⟩ λ n →
           let lemma₃ =
                 cong _[ n ] lemma₁                               ≡⟨ sym $ cong-∘ (_$ n) proj₁ lemma₁ ⟩
                 cong (_$ n) (cong proj₁ lemma₁)                  ≡⟨ cong (cong (_$ n)) $ proj₁-Σ-≡,≡→≡ (⟨ext⟩ (lemma ∘ proj₁ s)) _ ⟩
                 cong (_$ n) (⟨ext⟩ (lemma ∘ proj₁ s))            ≡⟨ cong-ext (lemma ∘ proj₁ s) ⟩∎
                 lemma (s [ n ])                                  ∎
           in
           subst (λ s → ∀ n → P (s [ n ])) lemma₁
                 (proj₂ ∘ function ∘ proj₁ s) n                   ≡⟨ sym $ push-subst-application lemma₁ (λ s n → P (s [ n ])) ⟩

           subst (λ s → P (s [ n ])) lemma₁
                 (proj₂ (function (s [ n ])))                     ≡⟨ subst-∘ P _[ n ] lemma₁ ⟩

           subst P (cong _[ n ] lemma₁)
                 (proj₂ (function (s [ n ])))                     ≡⟨ cong (λ eq → subst P eq (proj₂ (function (s [ n ])))) lemma₃ ⟩∎

           subst P (lemma (s [ n ]))
                 (proj₂ (function (s [ n ])))                     ∎) ⟩

       pl s ( (λ n → subst P (lemma (s [ n ]))
                           (proj₂ (function (s [ n ]))))
            , ⊑-rec ∘ proj₂ s
            )                                             ≡⟨⟩

       pl s ( ⊥-rec ∘ proj₁ s
            , ⊑-rec ∘ proj₂ s
            )                                             ∎

-- For any partiality algebra (with certain levels) initiality (at
-- possibly larger levels) is logically equivalent to having
-- eliminators (at the same possibly larger levels).

initiality⇔eliminators :
  ∀ {a p q p′ q′} {A : Type a} →
  (P : Partiality-algebra p′ q′ A) →
  Initial (p ⊔ p′) (q ⊔ q′) P
    ⇔
  Elimination-principle (p ⊔ p′) (q ⊔ q′) P
initiality⇔eliminators P = record
  { to   = initiality→eliminators
  ; from = eliminators→initiality P
  }

-- For any partiality algebra initiality at all levels is logically
-- equivalent (at the meta-level) to having eliminators at all levels.

∀initiality→∀eliminators :
  ∀ {a p q} {A : Type a} →
  (P : Partiality-algebra p q A) →
  (∀ p q → Initial p q P) →
  (∀ p q → Elimination-principle p q P)
∀initiality→∀eliminators {p = p′} {q = q′} P initial p q =
  initiality→eliminators (initial (p ⊔ p′) (q ⊔ q′))

∀eliminators→∀initiality :
  ∀ {a p q} {A : Type a} →
  (P : Partiality-algebra p q A) →
  (∀ p q → Elimination-principle p q P) →
  (∀ p q → Initial p q P)
∀eliminators→∀initiality P elim p q =
  eliminators→initiality P (elim p q)

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
{-# OPTIONS --universe-polymorphism #-}

module Categories.NaturalIsomorphism where

open import Level
open import Relation.Binary using (IsEquivalence)

open import Categories.Support.PropositionalEquality
open import Categories.Support.Equivalence
open import Categories.Category
open import Categories.Functor hiding (id) renaming (_∘_ to _∘F_; _≡_ to _≡F_; equiv to equivF)
open import Categories.NaturalTransformation.Core hiding (_≡_; equiv; setoid)
open import Categories.NaturalTransformation using (_∘ˡ_; _∘ʳ_)
import Categories.Morphisms as Morphisms
open import Categories.Functor.Properties using (module FunctorsAlways)

record NaturalIsomorphism {o ℓ e o′ ℓ′ e′}
                          {C : Category o ℓ e}
                          {D : Category o′ ℓ′ e′}
                          (F G : Functor C D) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private module C = Category C
  private module D = Category D
  private module F = Functor F
  private module G = Functor G
  open F
  open G renaming (F₀ to G₀; F₁ to G₁)

  field
    F⇒G : NaturalTransformation F G
    F⇐G : NaturalTransformation G F

  module ⇒ = NaturalTransformation F⇒G
  module ⇐ = NaturalTransformation F⇐G

  open Morphisms D

  field
    .iso : ∀ X → Iso (⇒.η X) (⇐.η X)

equiv : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → IsEquivalence (NaturalIsomorphism {C = C} {D})
equiv {C = C} {D} = record
  { refl = record
    { F⇒G = id
    ; F⇐G = id
    ; iso = λ _ → record
      { isoˡ = D.identityˡ
      ; isoʳ = D.identityˡ
      }
    }
  ; sym = λ X → let module X Z = Morphisms.Iso (NaturalIsomorphism.iso X Z) in record
    { F⇒G = NaturalIsomorphism.F⇐G X
    ; F⇐G = NaturalIsomorphism.F⇒G X
    ; iso = λ Y → record
      { isoˡ = X.isoʳ Y
      ; isoʳ = X.isoˡ Y
      }
    }
  ; trans = trans′
  }
  where
  module C = Category C
  module D = Category D
  open D hiding (id)

  trans′ : {x y z : Functor C D} → NaturalIsomorphism x y → NaturalIsomorphism y z → NaturalIsomorphism x z
  trans′ X Y = record
    { F⇒G = F⇒G′
    ; F⇐G = F⇐G′
    ; iso = iso′
    }
    where
    F⇒G′ = NaturalIsomorphism.F⇒G Y ∘₁ NaturalIsomorphism.F⇒G X
    F⇐G′ = NaturalIsomorphism.F⇐G X ∘₁ NaturalIsomorphism.F⇐G Y

    .iso′ : (X : C.Obj) → _
    iso′ Z = record
      { isoˡ = isoˡ′
      ; isoʳ = isoʳ′
      }
      where
      open NaturalIsomorphism
      open NaturalTransformation
      module Y Z = Morphisms.Iso (iso Y Z)
      module X Z = Morphisms.Iso (iso X Z)

      isoˡ′ : (η (F⇐G X) Z ∘ η (F⇐G Y) Z) ∘ (η (F⇒G Y) Z ∘ η (F⇒G X) Z) ≡ D.id
      isoˡ′ = begin
                (η (F⇐G X) Z ∘ η (F⇐G Y) Z) ∘ (η (F⇒G Y) Z ∘ η (F⇒G X) Z)
              ↓⟨ D.assoc ⟩
                η (F⇐G X) Z ∘ (η (F⇐G Y) Z ∘ (η (F⇒G Y) Z ∘ η (F⇒G X) Z))
              ↑⟨ D.∘-resp-≡ʳ D.assoc ⟩
                η (F⇐G X) Z ∘ ((η (F⇐G Y) Z ∘ η (F⇒G Y) Z) ∘ η (F⇒G X) Z)
              ↓⟨ D.∘-resp-≡ʳ (D.∘-resp-≡ˡ (Y.isoˡ Z)) ⟩
                η (F⇐G X) Z ∘ (D.id ∘ η (F⇒G X) Z)
              ↓⟨ D.∘-resp-≡ʳ D.identityˡ ⟩
                η (F⇐G X) Z ∘ η (F⇒G X) Z
              ↓⟨ X.isoˡ Z ⟩
                D.id
              ∎
        where
        open D.HomReasoning

      isoʳ′ : (η (F⇒G Y) Z ∘ η (F⇒G X) Z) ∘ (η (F⇐G X) Z ∘ η (F⇐G Y) Z) ≡ D.id
      isoʳ′ = begin
                (η (F⇒G Y) Z ∘ η (F⇒G X) Z) ∘ (η (F⇐G X) Z ∘ η (F⇐G Y) Z)
              ↓⟨ D.assoc ⟩
                η (F⇒G Y) Z ∘ (η (F⇒G X) Z ∘ (η (F⇐G X) Z ∘ η (F⇐G Y) Z))
              ↑⟨ D.∘-resp-≡ʳ D.assoc ⟩
                η (F⇒G Y) Z ∘ ((η (F⇒G X) Z ∘ η (F⇐G X) Z) ∘ η (F⇐G Y) Z)
              ↓⟨ D.∘-resp-≡ʳ (D.∘-resp-≡ˡ (X.isoʳ Z)) ⟩
                η (F⇒G Y) Z ∘ (D.id ∘ η (F⇐G Y) Z)
              ↓⟨ D.∘-resp-≡ʳ D.identityˡ ⟩
                η (F⇒G Y) Z ∘ η (F⇐G Y) Z
              ↓⟨ Y.isoʳ Z ⟩
                D.id
              ∎
        where
        open D.HomReasoning

setoid : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → Setoid _ _
setoid {C = C} {D} = record
  { Carrier = Functor C D
  ; _≈_ = NaturalIsomorphism
  ; isEquivalence = equiv {C = C} {D}
  }

_ⓘˡ_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
     → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
     → {F G : Functor C D}
     → (H : Functor D E) → (η : NaturalIsomorphism F G) → NaturalIsomorphism (H ∘F F) (H ∘F G)
_ⓘˡ_ {C = C} {D} {E} {F} {G} H η = record
  { F⇒G = H ∘ˡ η.F⇒G
  ; F⇐G = H ∘ˡ η.F⇐G
  ; iso = λ X → FunctorsAlways.resp-Iso H (η.iso X)
  }
  where
  module η = NaturalIsomorphism η

_ⓘʳ_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
     → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
     → {F G : Functor C D}
     → (η : NaturalIsomorphism F G) → (K : Functor E C) → NaturalIsomorphism (F ∘F K) (G ∘F K)
η ⓘʳ K = record
  { F⇒G = η.F⇒G ∘ʳ K
  ; F⇐G = η.F⇐G ∘ʳ K
  ; iso = λ X → η.iso (K.F₀ X)
  }
  where
  module η = NaturalIsomorphism η
  module K = Functor K

-- try ≡→iso again, but via first de-embedding some helpers, as that seems to make things
-- go 'weird' in combination with irrelevance
private
  _©_ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D} →
       NaturalTransformation F G → (x : Category.Obj C) → D [ Functor.F₀ F x , Functor.F₀ G x ]
  _©_ = NaturalTransformation.η

  my-sym : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (F G : Functor C D) → F ≡F G → G ≡F F
  my-sym {D = D} _ _ F≡G X = Heterogeneous.sym D (F≡G X)

  oneway : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (F G : Functor C D) →
    F ≡F G → NaturalTransformation F G
  oneway {C = C} {D} F G F≡G =
    record
    { η = my-η
    ; commute = my-commute
    }
    where
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
    open Heterogeneous D
    same-Objs : ∀ A → F.F₀ A ≣ G.F₀ A
    same-Objs A = domain-≣ (F≡G (C.id {A}))
    my-η : ∀ X → D [ F.F₀ X , G.F₀ X ]
    my-η X = ≣-subst (λ x → D [ F.F₀ X , x ]) (same-Objs X) D.id

    .my-commute : ∀ {X Y} (f : C [ X , Y ]) → D [ D [ my-η Y ∘ F.F₁ f ] ≡ D [ G.F₁ f ∘ my-η X ] ]
    my-commute {X} {Y} f with helper₃
      where
      helper₁ : D [ my-η Y ∘ F.F₁ f ] ∼ F.F₁ f
      helper₁ with F.F₀ Y | G.F₀ Y | same-Objs Y | F.F₁ f
      helper₁ | _ | ._ | ≣-refl | f′ = ≡⇒∼ D.identityˡ
      helper₂ : G.F₁ f ∼ D [ G.F₁ f ∘ my-η X ]
      helper₂ with F.F₀ X | G.F₀ X | same-Objs X | G.F₁ f
      helper₂ | _ | ._ | ≣-refl | f′ = ≡⇒∼ (D.Equiv.sym D.identityʳ)
      helper₃ : D [ my-η Y ∘ F.F₁ f ] ∼ D [ G.F₁ f ∘ my-η X ]
      helper₃ = trans helper₁ (trans (F≡G f) helper₂)
    my-commute f | Heterogeneous.≡⇒∼ pf = irr pf

≡→iso : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (F G : Functor C D) → F ≡F G → NaturalIsomorphism F G
≡→iso {C = C} {D} F G F≡G =
  record
  { F⇒G = oneway F G F≡G
  ; F⇐G = oneway G F (my-sym F G F≡G)
  ; iso = λ X → record
    { isoˡ = my-iso G F (my-sym F G F≡G) F≡G X
    ; isoʳ = my-iso F G F≡G (my-sym F G F≡G) X
    }
  }
  where
  module C = Category C
  module D = Category D
  open Heterogeneous D

  .my-iso : (F G : Functor C D) (F≡G : F ≡F G) (G≡F : G ≡F F) (x : C.Obj) → D [ D [ oneway F G F≡G © x ∘ oneway G F G≡F © x ] ≡ D.id ]
  my-iso F G F≡G G≡F x = func (F.F₀ x) (G.F₀ x) (domain-≣ (F≡G (C.id {x}))) (domain-≣ (G≡F (C.id {x})))
    where
    module F = Functor F
    module G = Functor G
    -- hand-written function that "with" cannot properly abstract on its own, it gets itself all confused.
    func : (w z : D.Obj) (zz : w ≣ z ) (ww : z ≣ w) →
        ≣-subst (D._⇒_ w) zz (D.id {w}) D.∘ ≣-subst (D._⇒_ z) ww (D.id {z}) D.≡ D.id
    func w .w ≣-refl ≣-refl = D.identityʳ

ext: agda

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --sized-types #-}

module SizedTypesVarSwap where

open import Common.Size renaming (↑_ to _^)

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {size ^}
  suc  : {size : Size} -> Nat {size} -> Nat {size ^}

bad : {i j : Size} -> Nat {i} -> Nat {j} -> Nat {∞}
bad (suc x) y = bad (suc y) x
bad zero y = y

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Sessions.Semantics.Communication {E : Set} (delay : E) where

open import Prelude
open import Data.List.Relation.Ternary.Interleaving
open import Data.List.Relation.Ternary.Interleaving.Propositional
open import Data.List.Relation.Equality.Propositional
open import Data.List.Properties
import Data.List as L

open import Relation.Unary hiding (Empty; _∈_)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Ternary.Separation.Construct.Market
open import Relation.Ternary.Separation.Construct.Product
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad

open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Monad.Error
open import Relation.Ternary.Separation.Monad.State

open import Sessions.Syntax.Types
open import Sessions.Syntax.Values
open import Sessions.Syntax.Expr
open import Sessions.Semantics.Commands
open import Sessions.Semantics.Runtime delay

{- A specification of the update we are performing -}
_≔_ : ∀ {x} {ys} {zs} → [ endp x ] ⊎ ys ≣ zs → SType → RCtx
_≔_ {zs = x ∷ zs}         (to-right s) α  = x ∷ s ≔ α
_≔_ {zs = chan l r ∷ zs}  (divide lr s) α = chan α r ∷ zs
_≔_ {zs = chan l r ∷ zs}  (divide rl s) α = chan l α ∷ zs
_≔_ {zs = .(endp _) ∷ zs} (to-left s) α   = endp α ∷ zs

{- Type of actions on a link -}
private
  Action : ∀ (from to : SType) → Pt RCtx 0ℓ
  Action from to P Φ = ∀ {τ} → (end : End from τ) → (Channel τ ─✴ Except E (P ✴ Channel (end ≔ₑ to))) Φ

module _ where
  open ExceptMonad {A = RCtx} E
  open Monads.Monad except-monad
  open Monads using (str)

  {- Takes an endpointer and the channel list and updates it using a link action -}
  act : ∀ {P α xs ds} →
        (ptr : [ endp α ] ⊎ ds ≣ xs) →
        ∀[ Action α β P
           ⇒ Channels' xs
           ─✴ Except E (Empty ([ endp β ] ⊎ ds ≣ (ptr ≔ β)) ✴ P ✴ Channels' (ptr ≔ β)) ]

  -- the pointer points to a channel where one end is already closed
  app (act {xs = x ∷ xs} (to-left ptr) f) (ch :⟨ τ ⟩: chs) σ with ⊎-unassoc σ τ
  ... | _ , τ₁ , τ₂ = do
    px ×⟨ τ₄ ⟩ (ch' ×⟨ τ₅ ⟩ chs) ← mapM (app (f (-, to-left [])) ch τ₁ &⟨ τ₂ ⟩ chs) ✴-assocᵣ
    return (emp (to-left ptr) ×⟨ ⊎-idˡ ⟩ px ×⟨ τ₄ ⟩ cons (ch' ×⟨ τ₅ ⟩ chs))

  -- the pointer points to the left side of a channel in the state
  app (act {xs = x ∷ xs} (divide lr ptr) f) (ch :⟨ τ ⟩: chs) σ with ⊎-unassoc σ τ
  ... | _ , τ₂ , τ₃ = do
    px ×⟨ τ₄ ⟩ chs ← mapM (app (f (ending lr)) ch τ₂ &⟨ τ₃ ⟩ chs) ✴-assocᵣ
    return (emp (divide lr ptr) ×⟨ ⊎-idˡ ⟩ px ×⟨ τ₄ ⟩ cons chs)

  -- the pointer points to the right side of a channel in the state
  app (act {xs = x ∷ xs} (divide rl ptr) f) (ch :⟨ τ ⟩: chs) σ with ⊎-unassoc σ τ
  ... | _ , τ₂ , τ₃ = do
    px ×⟨ τ₄ ⟩ (ch' ×⟨ τ₅ ⟩ chs) ← mapM (app (f (ending rl)) ch τ₂ &⟨ τ₃ ⟩ chs) ✴-assocᵣ
    return (emp (divide rl ptr) ×⟨ ⊎-idˡ ⟩ px ×⟨ τ₄ ⟩ cons (ch' ×⟨ τ₅ ⟩ chs))

  -- the pointer points to some channel further down the list
  app (act {xs = x ∷ xs} (to-right ptr) f) (ch :⟨ τ ⟩: chs) σ with ⊎-unassoc σ (⊎-comm τ)
  ... | _ , τ₁ , τ₂ = do
    emp ptr ×⟨ τ₃ ⟩ rhs ← mapM (app (act ptr f) chs τ₁ &⟨ τ₂ ⟩ ch) ✴-assocᵣ
    let px ×⟨ τ₄ ⟩ chs' = ✴-assocᵣ rhs
    return (emp (to-right ptr) ×⟨ τ₃ ⟩ (px ×⟨ τ₄ ⟩ cons (✴-swap chs')))

module _ where
  open StateWithErr {C = RCtx} E
  open Monads.Monad {{...}}

  {- Updating a single link based on a pointer to one of its endpoints -}
  operate : ∀ {P} → ∀[ Action α β P ⇒ Endptr α ─✴ State? Channels (P ✴ Endptr β) ]
  app (app (operate f) refl σ₁) (lift chs k) (offerᵣ σ₂) with ⊎-assoc σ₂ k
  ... | _ , σ₃ , σ₄ with ⊎-assoc (⊎-comm σ₁) σ₃
  ... | _ , σ₅ , σ₆ with ⊎-unassoc σ₆ (⊎-comm σ₄)
  ... | _ , σ₇ , σ₈ with app (act σ₅ f) chs σ₇
  ... | error _ = error delay
  ... | partial (inj₂ (emp ptr' ×⟨ σ ⟩ (px ×⟨ τ ⟩ chs'))) with ⊎-id⁻ˡ σ
  ... | refl with ⊎-unassoc ptr' σ₈
  ... | _ , τ₁ , τ₂ with ⊎-unassoc τ₁ τ
  ... | _ , τ₃ , τ₄ with ⊎-assoc (⊎-comm τ₄) τ₂
  ... | _ , τ₅ , eureka =
    partial (inj₂ (inj (px ×⟨ ⊎-comm τ₃ ⟩ refl) ×⟨ offerᵣ eureka ⟩ lift chs' (⊎-comm τ₅)))

  {- Getting a value from a ready-to-receive endpoint -}
  receive? : ∀[ Endptr (a ¿ β) ⇒ State? Channels (Val a ✴ Endptr β) ]
  receive? ptr = app (operate (λ end → wandit (chan-receive end))) ptr ⊎-idˡ

  {- Putting a value in a ready-to-send endpoint -}
  send! : ∀[ Endptr (a ! β) ⇒ Val a ─✴ State? Channels (Endptr β) ]
  app (send! {a = a} ptr) v σ = do
    empty ×⟨ σ ⟩ ptr ← app (operate sender) ptr (⊎-comm σ)
    case ⊎-id⁻ˡ σ of λ where
      refl → return ptr
    where
      sender : Action (a ! γ) γ Emp _
      app (sender e) ch σ =
        let ch' = app (chan-send e ch) v (⊎-comm σ)
        in ✓ (empty ×⟨ ⊎-idˡ ⟩ ch')

  newChan : ε[ State? Channels (Endptr α ✴ Endptr (α ⁻¹)) ]
  app newChan (lift chs k) σ with ⊎-id⁻ˡ σ
  ... | refl = ✓ (
   (inj (refl ×⟨ divide lr ⊎-idˡ ⟩ refl))
      ×⟨ offerᵣ ⊎-∙ ⟩
   lift (cons (emptyChannel ×⟨ ⊎-idˡ ⟩ chs)) (⊎-∙ₗ k))

  closeChan : ∀[ Endptr end ⇒ State? Channels Emp ]
  app (closeChan refl) (lift chs k) (offerᵣ σ) =
    let
      _ , σ₂ , σ₃ = ⊎-assoc σ k
      chs' = close'em σ₂ chs
    in ✓ (inj empty ×⟨ ⊎-idˡ ⟩ lift chs' σ₃)
    where
      -- This is really cool:
      -- The pointer, in the form of the splitting of the store, contains all the necessary information
      -- for the shape of the underlying buffer.
      -- Depending on the shape of the splitting, we know, just by dependent pattern matching,
      -- whether the channel is two- or onesided
      close'em : ∀ {ds xs} → (ptr : [ endp end ] ⊎ ds ≣ xs) → ∀[ Channels' xs ⇒ Channels' ds ]

      close'em (divide lr ptr) (twosided (link refl (emp ×⟨ τ ⟩ bᵣ)) :⟨ σ ⟩: chs) with ⊎-id⁻ˡ ptr | ⊎-id⁻ˡ τ
      ... | refl | refl = cons (onesided bᵣ ×⟨ σ ⟩ chs)

      close'em (divide rl ptr) (twosided (link eq (bₗ ×⟨ τ ⟩ emp)) :⟨ σ ⟩: chs) with ⊎-id⁻ˡ ptr | ⊎-id⁻ʳ τ
      ... | refl | refl with dual-end (sym eq)
      ... | refl = cons (onesided bₗ ×⟨ σ ⟩ chs)

      close'em (to-left ptr) (cons (onesided emp ×⟨ σ ⟩ chs)) with ⊎-id⁻ˡ ptr | ⊎-id⁻ˡ σ
      ... | refl | refl = chs

      close'em (to-right ptr)  (ch :⟨ σ ⟩: chs) =
        let chs' = close'em ptr chs
        in cons (ch ×⟨ σ ⟩ chs')


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

open import Data.Product
open import Data.List using (List; []; _∷_; _∷ʳ_; _++_)
open import Data.List.Properties using (∷-injective)

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

open import Common

module Trace {ℙ : Set} (message : Message ℙ)
  where

open import Action message public
open import SessionType message

Trace : Set
Trace = List Action

--| CO-TRACES |--

co-trace : Trace -> Trace
co-trace = Data.List.map co-action

co-trace-involution : (φ : Trace) -> co-trace (co-trace φ) ≡ φ
co-trace-involution [] = refl
co-trace-involution (α ∷ φ) rewrite co-action-involution α | co-trace-involution φ = refl

co-trace-++ : (φ ψ : Trace) -> co-trace (φ ++ ψ) ≡ co-trace φ ++ co-trace ψ
co-trace-++ []      _ = refl
co-trace-++ (α ∷ φ) ψ = cong (co-action α ∷_) (co-trace-++ φ ψ)

co-trace-injective : ∀{φ ψ} -> co-trace φ ≡ co-trace ψ -> φ ≡ ψ
co-trace-injective {[]} {[]} eq = refl
co-trace-injective {x ∷ φ} {x₁ ∷ ψ} eq with ∷-injective eq
... | eq1 , eq2 rewrite co-action-injective eq1 | co-trace-injective eq2 = refl

--| PREFIX RELATION |--

data _⊑_ : Trace -> Trace -> Set where
  none : ∀{φ}     -> [] ⊑ φ
  some : ∀{φ ψ α} -> φ ⊑ ψ -> (α ∷ φ) ⊑ (α ∷ ψ)

⊑-refl : (φ : Trace) -> φ ⊑ φ
⊑-refl [] = none
⊑-refl (_ ∷ φ) = some (⊑-refl φ)

⊑-tran : ∀{φ ψ χ} -> φ ⊑ ψ -> ψ ⊑ χ -> φ ⊑ χ
⊑-tran none _ = none
⊑-tran (some le1) (some le2) = some (⊑-tran le1 le2)

⊑-++ : ∀{φ χ} -> φ ⊑ (φ ++ χ)
⊑-++ {[]} = none
⊑-++ {_ ∷ φ} = some (⊑-++ {φ})

⊑-precong-++ : ∀{φ ψ χ} -> ψ ⊑ χ -> (φ ++ ψ) ⊑ (φ ++ χ)
⊑-precong-++ {[]} le = le
⊑-precong-++ {_ ∷ _} le = some (⊑-precong-++ le)

⊑-co-trace : ∀{φ ψ} -> φ ⊑ ψ -> co-trace φ ⊑ co-trace ψ
⊑-co-trace none = none
⊑-co-trace (some le) = some (⊑-co-trace le)

⊑-trace : ∀{φ ψ} -> ψ ⊑ φ -> ∃[ φ' ] (φ ≡ ψ ++ φ')
⊑-trace {φ} none = φ , refl
⊑-trace {α ∷ φ} (some le) with ⊑-trace le
... | φ' , eq rewrite eq = φ' , refl

absurd-++-≡ : ∀{φ ψ : Trace}{α} -> (φ ++ α ∷ ψ) ≢ []
absurd-++-≡ {[]} ()
absurd-++-≡ {_ ∷ _} ()

absurd-++-⊑ : ∀{φ α ψ} -> ¬ (φ ++ α ∷ ψ) ⊑ []
absurd-++-⊑ {[]} ()
absurd-++-⊑ {_ ∷ _} ()

--| STRICT PREFIX RELATION |--

data _⊏_ : Trace -> Trace -> Set where
  none : ∀{α φ} -> [] ⊏ (α ∷ φ)
  some : ∀{φ ψ α} -> φ ⊏ ψ -> (α ∷ φ) ⊏ (α ∷ ψ)

⊏-irreflexive : ∀{φ} -> ¬ φ ⊏ φ
⊏-irreflexive (some lt) = ⊏-irreflexive lt

⊏-++ : ∀{φ ψ α} -> φ ⊏ (φ ++ (ψ ∷ʳ α))
⊏-++ {[]} {[]} = none
⊏-++ {[]} {_ ∷ _} = none
⊏-++ {_ ∷ φ} = some (⊏-++ {φ})

⊏->≢ : ∀{φ ψ} -> φ ⊏ ψ -> φ ≢ ψ
⊏->≢ (some lt) refl = ⊏-irreflexive lt

⊏->⊑ : ∀{φ ψ} -> φ ⊏ ψ -> φ ⊑ ψ
⊏->⊑ none = none
⊏->⊑ (some lt) = some (⊏->⊑ lt)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
open import Level hiding ( suc ; zero )
open import Algebra
module sym5a where

open import Symmetric
open import Data.Unit using (⊤ ; tt )
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function hiding (flip)
open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
open import Data.Nat.Properties
open import Relation.Nullary
open import Data.Empty
open import Data.Product

open import Gutil
open import Putil
open import Solvable using (solvable)
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

open import Data.Fin hiding (_<_ ; _≤_  ; lift )
open import Data.Fin.Permutation  hiding (_∘ₚ_)

infixr  200 _∘ₚ_
_∘ₚ_ = Data.Fin.Permutation._∘ₚ_

open import Data.List  hiding ( [_] )
open import nat
open import fin
open import logic

open _∧_

¬sym5solvable : ¬ ( solvable (Symmetric 5) )
¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (any3de (dervied-length sol) 3rot 0<3 0<4 ) ) where
--
--    dba       1320      d → b → a → d
--    (dba)⁻¹   3021      a → b → d → a
--    aec       21430
--    (aec)⁻¹   41032
--    [ dba , aec ] = (abd)(cea)(dba)(aec) = abc
--      so commutator always contains abc, dba and aec

     open ≡-Reasoning

     open solvable
     open Solvable ( Symmetric 5)
     end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →  x =p= pid
     end5 x der = end sol x der

     0<4 : 0 < 4
     0<4 = s≤s z≤n

     0<3 : 0 < 3
     0<3 = s≤s z≤n

     --- 1 ∷ 2 ∷ 0 ∷ []      abc
     3rot : Permutation 3 3
     3rot = pid {3} ∘ₚ pins (n≤ 2)

     save2 : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) →  Permutation  5 5
     save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4)

     -- Permutation 5 5 include any Permutation 3 3
     any3 : {i j : ℕ }  → Permutation 3 3  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
     any3 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 )

     any3cong : {i j : ℕ }  → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → any3 x i<3 j<4  =p= any3 y i<3 j<4
     any3cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )}
         (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl

     open _=p=_

     -- derving n includes any Permutation 3 3,
     any3de : {i j : ℕ } → (n : ℕ) → (abc : Permutation 3 3) →  (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) → deriving n (any3 abc i<3 j<4)
     any3de {i} {j} zero abc i<3 j<4 = Level.lift tt
     any3de {i} {j} (suc n) abc i<3 j<4 = ccong abc-from-comm (comm (any3de n (abc  ∘ₚ abc) i<3 j0<4 ) (any3de n (abc  ∘ₚ abc) i0<3 j<4 ))  where
         i0 : ℕ
         i0 = ?
         j0 : ℕ
         j0 = ?
         i0<3 : i0 ≤ 3
         i0<3 = {!!}
         j0<4 : j0 ≤ 4
         j0<4 = {!!}
         abc-from-comm : [ any3 (abc  ∘ₚ abc) i<3 j0<4  , any3 (abc  ∘ₚ abc) i0<3 j<4 ] =p= any3 abc i<3 j<4
         abc-from-comm = {!!}

     abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
     abc i<3 j<4 = any3 3rot i<3 j<4

     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
     counter-example eq with ←pleq _ _ eq
     ...  | ()

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
-- Andreas, 2016-02-11, bug reported by sanzhiyan

module Issue610-module-alias-with where

import Common.Level
open import Common.Equality

data ⊥ : Set where
record ⊤ : Set where

data A : Set₁ where
  set : .Set → A

module M .(x : Set) where

  .out : _
  out = x

.ack : A → Set
ack (set x) = M.out x

hah : set ⊤ ≡ set ⊥
hah = refl

.moo : ⊥
moo with cong ack hah
moo | q = subst (λ x → x) q _

-- Expected error:
-- .(⊥) !=< ⊥ of type Set
-- when checking that the expression subst (λ x → x) q _ has type ⊥

baa : .⊥ → ⊥
baa ()

yoink : ⊥
yoink = baa moo


text:
{-

        Agda Implementors' Meeting VI

                  Göteborg
             May 24 - 30, 2007

                Hello Agda!

                Ulf Norell

-}

-- Something which is rather useful is the ability to pattern match
-- on intermediate computations. That's where the with-construct comes
-- in.

module TestWith where

-- open import Nat
open import PreludeNat hiding(_==_; even; odd)
open import PreludeShow

{-

  Basic idea

-}

-- The basic principle is that you can add argument to your
-- function on the fly. For instance,

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A -> Maybe A

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

compare : (n m : Nat) -> Maybe (n == m)
compare  zero   zero   = just refl
compare (suc _) zero   = nothing
compare  zero  (suc _) = nothing
compare (suc n)(suc m) with compare n m
compare (suc n)(suc .n) | just refl = just refl
compare (suc n)(suc m)  | nothing   = nothing

-- To add more than one argument separate by |
silly : Nat -> Nat
silly zero = zero
silly (suc n) with n | n
silly (suc n) | zero | suc m = m  -- the values of the extra argument are
                                  -- not taken into consideration
silly (suc n) | _    | _     = n

{-

  The parity example

-}

-- This is a cute example of what you can do with with.

data Parity : Nat -> Set where
  even : (k : Nat) -> Parity (k * 2)
  odd  : (k : Nat) -> Parity (1 + k * 2)

parity : (n : Nat) -> Parity n
parity zero = even 0
parity (suc n) with parity n
parity (suc .(    k * 2)) | even k = odd k
parity (suc .(1 + k * 2)) | odd  k = even (suc k)

half : Nat -> Nat
half n with parity n
half .(    k * 2) | even k = k
half .(1 + k * 2) | odd  k = k

mainS = showNat (half 44)
{-

  What's next?

-}

-- Move on to: Modules.agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Cubical.Categories.Abelian where

open import Cubical.Categories.Abelian.Base public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Categories.Product where

open import Prelude hiding (_×_)
open import Categories

module _ {ℓ₁ ℓ₂} (C : Category ℓ₁ ℓ₂) where
  open Category C

  module _ (X Y : Ob) where
    record Product : Type (ℓ₁ ℓ⊔ ℓ₂) where
      field
        obj : Ob
        proj₁ : C [ obj , X ]
        proj₂ : C [ obj , Y ]
        ump : (f : C [ Z , X ]) (g : C [ Z , Y ]) →
              ∃![ f×g ] ((C [ proj₁ ∘ f×g ] ≡ f) Prelude.× (C [ proj₂ ∘ f×g ] ≡ g))
      _P[_×_] : ∀ {Z} → (π₁ : C [ Z , X ]) (π₂ : C [ Z , Y ]) →
                C [ Z , obj ]
      _P[_×_] π₁ π₂ = fst (ump π₁ π₂)

  record HasProducts : Type (ℓ₁ ℓ⊔ ℓ₂) where
    field product : (X Y : Ob) → Product X Y

    _×_ : Ob → Ob → Ob
    A × B = Product.obj (product A B)

    module _ {A A′ B B′ : Ob} where
      open Product using (_P[_×_])
      open Product (product A B) hiding (_P[_×_])

      _|×|_ : C [ A , A′ ] → C [ B , B′ ] → C [ Product.obj (product A B) , Product.obj (product A′ B′) ]
      f |×| g = product A′ B′ P[ C [ f ∘ proj₁ ] × C [ g ∘ proj₂ ] ]

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-

This file contains:

- Definition of groupoid quotients

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.GroupoidQuotients.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Relation.Binary.Base

-- Groupoid quotients as a higher inductive type:
-- For the definition, only transitivity is needed
data _//_ {ℓ ℓ'} (A : Type ℓ) {R : A → A → Type ℓ'}
          (Rt : BinaryRelation.isTrans R) : Type (ℓ-max ℓ ℓ') where
  [_] : (a : A) → A // Rt
  eq// : {a b : A} → (r : R a b) → [ a ] ≡ [ b ]
  comp// : {a b c : A} → (r : R a b) → (s : R b c)
          → PathP (λ j → [ a ] ≡ eq// s j) (eq// r) (eq// (Rt a b c r s))
  squash// : ∀ (x y : A // Rt) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s

{- The comp// constructor fills the square:

  eq// (Rt a b c r s)
    [a]— — — >[c]
     ‖         ^
     ‖         | eq// s   ^
     ‖         |        j |
    [a]— — — >[b]         ∙ — >
       eq// r               i

  We use this to give another constructor-like construction:
-}

comp'// : {ℓ ℓ' : Level} (A : Type ℓ) {R : A → A → Type ℓ'}
          (Rt : BinaryRelation.isTrans R)
          {a b c : A} → (r : R a b) → (s : R b c)
          → eq// {Rt = Rt} (Rt a b c r s) ≡ eq// r ∙ eq// s
comp'// A Rt r s i = compPath-unique refl (eq// r) (eq// s)
  (eq// {Rt = Rt} (Rt _ _ _ r s) , comp// r s)
  (eq// r ∙ eq// s , compPath-filler (eq// r) (eq// s)) i .fst

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module Bee2.Crypto.Belt where

open import Data.ByteString
open import Data.ByteVec
open import Data.Nat using (ℕ)
open import Data.Product using (_,_)
open import Agda.Builtin.TrustMe using (primTrustMe)

import Bee2.Crypto.Defs
open Bee2.Crypto.Defs
open Bee2.Crypto.Defs using (Hash) public

{-# FOREIGN GHC import qualified Bee2.Crypto.Belt    #-}
{-# FOREIGN GHC import qualified Data.ByteString    #-}

Password = ByteString Strict
Salt = ByteString Strict
Key = ByteVec {Strict} 32
Header = ByteVec {Strict} 16
Kek = ByteVec {Strict} 32

{-# FOREIGN GHC import qualified Bee2.Crypto.Belt    #-}
postulate
  primBeltPBKDF : ByteString Strict → SizeT → ByteString Strict → ByteString Strict
  primBeltHash : ByteString Strict → ByteString Strict

{-# COMPILE GHC primBeltPBKDF =
    ( Bee2.Crypto.Belt.beltPBKDF'bs ) #-}
{-# COMPILE GHC primBeltHash =
    ( Bee2.Crypto.Belt.beltHash'bs ) #-}

beltPBKDF : Password → ℕ → Salt → Kek
beltPBKDF p n s = (primBeltPBKDF p (SizeFromℕ n) s) , primTrustMe

beltHash : ByteString Strict → Hash
beltHash bs = primBeltHash bs , primTrustMe


text:
module Structure.Sets.Operator where

open import Data.Boolean
open import Data.Boolean.Stmt
open import Functional
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Function
open import Structure.Relator
open import Structure.Setoid using (Equiv) renaming (_≡_ to _≡ₛ_ ; _≢_ to _≢ₛ_)
import      Structure.Sets.Names as Names
open import Structure.Sets.Relator using (SubsetRelation)
open import Type

private variable ℓ ℓₗ ℓₗ₁ ℓₗ₂ ℓᵣ ℓᵣₑₗ ℓₒ ℓₛ : Lvl.Level
private variable A B C S S₁ S₂ Sₒ Sᵢ Sₗ Sᵣ E E₁ E₂ Eₗ Eᵣ I O : Type{ℓ}
private variable _∈_ _∈ₒ_ _∈ᵢ_ : E → S → Stmt{ℓₗ}
private variable _∈ₗ_ : E → Sₗ → Stmt{ℓₗ}
private variable _∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}
private variable _⊆_ : Sₗ → Sᵣ → Stmt{ℓᵣ}

private variable ⦃ equiv-I ⦄ : Equiv{ℓₗ}(I)
private variable ⦃ equiv-E ⦄ : Equiv{ℓₗ}(E)
private variable ⦃ equiv-Eₗ ⦄ : Equiv{ℓₗ}(Eₗ)
private variable ⦃ equiv-Eᵣ ⦄ : Equiv{ℓₗ}(Eᵣ)
private variable ⦃ equiv-O ⦄ : Equiv{ℓₗ}(O)
private variable ⦃ sub ⦄ : SubsetRelation(_∈ₗ_)(_∈ᵣ_)(_⊆_)

module _ (_∈_ : E → S → Stmt{ℓₗ}) where
  record EmptySet(∅ : S) : Type{Lvl.of(E) Lvl.⊔ ℓₗ} where
    constructor intro
    field membership : Names.EmptyMembership(_∈_)(∅)

  record UniversalSet(𝐔 : S) : Type{Lvl.of(E) Lvl.⊔ ℓₗ} where
    constructor intro
    field membership : Names.UniversalMembership(_∈_)(𝐔)

  module _ ⦃ equiv-I : Equiv{ℓₗ₁}(I) ⦄ ⦃ equiv-E : Equiv{ℓₗ₂}(E) ⦄ where
    record ImageFunction(⊶ : (f : I → E) → ⦃ func : Function(f) ⦄ → S) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(I) Lvl.⊔ ℓₗ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
      constructor intro
      field membership : Names.ImageMembership(_∈_)(⊶)

  module _ ⦃ equiv-E : Equiv{ℓₗ₁}(E) ⦄ {O : Type{ℓ}} ⦃ equiv-O : Equiv{ℓₗ₂}(O) ⦄ where
    record FiberFunction(fiber : (f : E → O) → ⦃ func : Function(f) ⦄ → (O → S)) : Type{Lvl.of(E) Lvl.⊔ ℓ Lvl.⊔ ℓₗ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
      constructor intro
      field membership : Names.FiberMembership(_∈_)(fiber)

  module _ ⦃ equiv-E : Equiv{ℓₗ}(E) ⦄ where
    record SingletonFunction(singleton : E → S) : Type{Lvl.of(E) Lvl.⊔ ℓₗ} where
      constructor intro
      field membership : Names.SingletonMembership(_∈_)(singleton)

    record PairFunction(pair : E → E → S) : Type{Lvl.of(E) Lvl.⊔ ℓₗ} where
      constructor intro
      field membership : Names.PairMembership(_∈_)(pair)

    record ComprehensionFunction(comp : (P : E → Stmt{ℓ}) ⦃ unaryRelator : UnaryRelator(P) ⦄ → S) : Type{Lvl.of(E) Lvl.⊔ ℓₗ Lvl.⊔ Lvl.𝐒(ℓ)} where
      constructor intro
      field membership : Names.ComprehensionMembership(_∈_)(comp)

module _ (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}) where
  record ComplementOperator(∁ : Sₗ → Sᵣ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ} where
    constructor intro
    field membership : Names.ComplementMembership(_∈ₗ_)(_∈ᵣ_)(∁)

  module _ ⦃ equiv-E : Equiv{ℓₗ}(E) ⦄ where
    record AddOperator(add : E → Sₗ → Sᵣ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ} where
      constructor intro
      field membership : Names.AddMembership(_∈ₗ_)(_∈ᵣ_)(add)

    record RemoveOperator(remove : E → Sₗ → Sᵣ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ} where
      constructor intro
      field membership : Names.RemoveMembership(_∈ₗ_)(_∈ᵣ_)(remove)

    record FilterFunction(filter : (P : E → Stmt{ℓ}) ⦃ unaryRelator : UnaryRelator(P) ⦄ → (Sₗ → Sᵣ)) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ Lvl.𝐒(ℓ)} where
      constructor intro
      field membership : Names.FilterMembership(_∈ₗ_)(_∈ᵣ_)(filter)

  record BooleanFilterFunction(boolFilter : (E → Bool) → (Sₗ → Sᵣ)) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ} where
    constructor intro
    field membership : Names.BooleanFilterMembership(_∈ₗ_)(_∈ᵣ_)(boolFilter)

  record IndexedBigUnionOperator(⋃ᵢ : (I → Sₗ) → Sᵣ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ Lvl.of(I)} where
    constructor intro
    field membership : Names.IndexedBigUnionMembership(_∈ₗ_)(_∈ᵣ_)(⋃ᵢ)

  record IndexedBigIntersectionOperator(⋂ᵢ : (I → Sₗ) → Sᵣ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ Lvl.of(I)} where
    constructor intro
    field membership : Names.IndexedBigIntersectionMembership(_∈ₗ_)(_∈ᵣ_)(⋂ᵢ)

module _ (_∈ₗ_ : Eₗ → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : Eᵣ → Sᵣ → Stmt{ℓᵣ}) where
  module _ ⦃ equiv-Eₗ : Equiv{ℓₗ₁}(Eₗ) ⦄ ⦃ equiv-Eᵣ : Equiv{ℓₗ₂}(Eᵣ) ⦄ where
    record MapFunction(map : (f : Eₗ → Eᵣ) ⦃ func : Function(f) ⦄ → (Sₗ → Sᵣ)) : Type{Lvl.of(Eₗ) Lvl.⊔ Lvl.of(Eᵣ) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
      constructor intro
      field membership : Names.MapMembership(_∈ₗ_)(_∈ᵣ_)(map)

    record UnmapFunction(unmap : (f : Eₗ → Eᵣ) ⦃ func : Function(f) ⦄ → (Sᵣ → Sₗ)) : Type{Lvl.of(Eₗ) Lvl.⊔ Lvl.of(Eᵣ) Lvl.⊔ Lvl.of(Sᵣ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
      constructor intro
      field membership : Names.UnmapMembership(_∈ₗ_)(_∈ᵣ_)(unmap)

module _ (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}) (_∈ₒ_ : E → Sₒ → Stmt{ℓₒ}) where
  record UnionOperator(_∪_ : Sₗ → Sᵣ → Sₒ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ Lvl.of(Sᵣ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ ℓₒ} where
    constructor intro
    field membership : Names.UnionMembership(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)(_∪_)

  record IntersectionOperator(_∩_ : Sₗ → Sᵣ → Sₒ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ Lvl.of(Sᵣ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ ℓₒ} where
    constructor intro
    field membership : Names.IntersectMembership(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)(_∩_)

  record WithoutOperator(_∖_ : Sₗ → Sᵣ → Sₒ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ Lvl.of(Sᵣ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ ℓₒ} where
    constructor intro
    field membership : Names.WithoutMembership(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)(_∖_)

module _ (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : E → Sᵣ → Stmt{ℓᵣ}) (_∈ₒ_ : Sₗ → Sₒ → Stmt{ℓₒ}) {_⊆_ : Sₗ → Sᵣ → Stmt{ℓₛ}} ⦃ sub : SubsetRelation(_∈ₗ_)(_∈ᵣ_)(_⊆_) ⦄ where
  record PowerFunction(℘ : Sᵣ → Sₒ) : Type{Lvl.of(Sₗ) Lvl.⊔ Lvl.of(Sᵣ) Lvl.⊔ ℓₛ Lvl.⊔ ℓₒ} where
    constructor intro
    field membership : Names.PowerMembership(_∈ₒ_)(_⊆_)(℘)

module _ (_∈ₗ_ : E → Sₗ → Stmt{ℓₗ}) (_∈ᵣ_ : Sₗ → Sᵣ → Stmt{ℓᵣ}) (_∈ₒ_ : E → Sₒ → Stmt{ℓₒ}) where
  record BigUnionOperator(⋃ : Sᵣ → Sₒ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ Lvl.of(Sᵣ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ ℓₒ} where
    constructor intro
    field membership : Names.BigUnionMembership(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)(⋃)

  record BigIntersectionOperator(⋂ : Sᵣ → Sₒ) : Type{Lvl.of(E) Lvl.⊔ Lvl.of(Sₗ) Lvl.⊔ Lvl.of(Sᵣ) Lvl.⊔ ℓₗ Lvl.⊔ ℓᵣ Lvl.⊔ ℓₒ} where
    constructor intro
    field membership : Names.BigIntersectionMembership(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)(⋂)

module _ ⦃ p : ∃(EmptySet(_∈_)) ⦄ where
  open ∃(p) using () renaming (witness to ∅) public
  open EmptySet([∃]-proof p) using () renaming (membership to [∅]-membership) public

module _ ⦃ p : ∃(UniversalSet(_∈_)) ⦄ where
  open ∃(p) using () renaming (witness to 𝐔) public
  open UniversalSet([∃]-proof p) using () renaming (membership to [𝐔]-membership) public

module _ ⦃ p : ∃(ImageFunction(_∈_) ⦃ equiv-I ⦄ ⦃ equiv-E ⦄) ⦄ where
  open ∃(p) using () renaming (witness to ⊶) public
  open ImageFunction([∃]-proof p) using () renaming (membership to [⊶]-membership) public

module _ ⦃ p : ∃(FiberFunction(_∈_) ⦃ equiv-E ⦄ ⦃ equiv-O ⦄) ⦄ where
  open ∃(p) using () renaming (witness to fiber) public
  open FiberFunction([∃]-proof p) using () renaming (membership to Fiber-membership) public

module _ ⦃ p : ∃(SingletonFunction(_∈_) ⦃ equiv-E ⦄) ⦄ where
  open ∃(p) using () renaming (witness to singleton) public
  open SingletonFunction([∃]-proof p) using () renaming (membership to Singleton-membership) public

module _ ⦃ p : ∃(PairFunction(_∈_) ⦃ equiv-E ⦄) ⦄ where
  open ∃(p) using () renaming (witness to pair) public
  open PairFunction([∃]-proof p) using () renaming (membership to Pair-membership) public

module _ ⦃ p : ∃(ComplementOperator(_∈ₗ_)(_∈ᵣ_)) ⦄ where
  open ∃(p) using () renaming (witness to ∁) public
  open ComplementOperator([∃]-proof p) using () renaming (membership to [∁]-membership) public

module _ ⦃ p : ∃(AddOperator(_∈ₗ_)(_∈ᵣ_) ⦃ equiv-E ⦄) ⦄ where
  open ∃(p) using () renaming (witness to add) public
  open AddOperator([∃]-proof p) using () renaming (membership to Add-membership) public

module _ ⦃ p : ∃(RemoveOperator(_∈ₗ_)(_∈ᵣ_) ⦃ equiv-E ⦄) ⦄ where
  open ∃(p) using () renaming (witness to remove) public
  open RemoveOperator([∃]-proof p) using () renaming (membership to Remove-membership) public

module _ ⦃ p : ∃(FilterFunction(_∈ₗ_)(_∈ᵣ_) ⦃ equiv-E ⦄ {ℓ}) ⦄ where
  open ∃(p) using () renaming (witness to filter) public
  open FilterFunction([∃]-proof p) using () renaming (membership to Filter-membership) public

module _ ⦃ p : ∃(BooleanFilterFunction(_∈ₗ_)(_∈ᵣ_)) ⦄ where
  open ∃(p) using () renaming (witness to boolFilter) public
  open BooleanFilterFunction([∃]-proof p) using () renaming (membership to BooleanFilter-membership) public

module _ ⦃ p : ∃(IndexedBigUnionOperator(_∈ₗ_)(_∈ᵣ_) {I = I}) ⦄ where
  open ∃(p) using () renaming (witness to ⋃ᵢ) public
  open IndexedBigUnionOperator([∃]-proof p) using () renaming (membership to [⋃ᵢ]-membership) public

module _ ⦃ p : ∃(IndexedBigIntersectionOperator(_∈ₗ_)(_∈ᵣ_) {I = I}) ⦄ where
  open ∃(p) using () renaming (witness to ⋂ᵢ) public
  open IndexedBigIntersectionOperator([∃]-proof p) using () renaming (membership to [⋂ᵢ]-membership) public

module _ ⦃ p : ∃(MapFunction(_∈ₗ_)(_∈ᵣ_) ⦃ equiv-Eₗ ⦄ ⦃ equiv-Eᵣ ⦄) ⦄ where
  open ∃(p) using () renaming (witness to map) public
  open MapFunction([∃]-proof p) using () renaming (membership to Map-membership) public

module _ ⦃ p : ∃(UnmapFunction(_∈ₗ_)(_∈ᵣ_) ⦃ equiv-Eₗ ⦄ ⦃ equiv-Eᵣ ⦄) ⦄ where
  open ∃(p) using () renaming (witness to unmap) public
  open UnmapFunction([∃]-proof p) using () renaming (membership to Unmap-membership) public

module _ ⦃ p : ∃(UnionOperator(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)) ⦄ where
  open ∃(p) using () renaming (witness to _∪_) public
  open UnionOperator([∃]-proof p) using () renaming (membership to [∪]-membership) public

module _ ⦃ p : ∃(IntersectionOperator(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)) ⦄ where
  open ∃(p) using () renaming (witness to _∩_) public
  open IntersectionOperator([∃]-proof p) using () renaming (membership to [∩]-membership) public

module _ ⦃ p : ∃(WithoutOperator(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)) ⦄ where
  open ∃(p) using () renaming (witness to _∖_) public
  open WithoutOperator([∃]-proof p) using () renaming (membership to [∖]-membership) public

module _ ⦃ p : ∃(PowerFunction(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_) ⦃ sub ⦄) ⦄ where
  open ∃(p) using () renaming (witness to ℘) public
  open PowerFunction([∃]-proof p) using () renaming (membership to [℘]-membership) public

module _ ⦃ p : ∃(BigUnionOperator(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)) ⦄ where
  open ∃(p) using () renaming (witness to ⋃) public
  open BigUnionOperator([∃]-proof p) using () renaming (membership to [⋃]-membership) public

module _ ⦃ p : ∃(BigIntersectionOperator(_∈ₗ_)(_∈ᵣ_)(_∈ₒ_)) ⦄ where
  open ∃(p) using () renaming (witness to ⋂) public
  open BigIntersectionOperator([∃]-proof p) using () renaming (membership to [⋂]-membership) 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:
module Base.Change.Sums where

open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Level

open import Base.Ascription
open import Base.Change.Algebra
open import Base.Change.Equivalence
open import Base.Change.Equivalence.Realizers
open import Postulate.Extensionality

module SumChanges ℓ {X Y : Set ℓ} {{CX : ChangeAlgebra X}} {{CY : ChangeAlgebra Y}} where
  open ≡-Reasoning

  -- This is an indexed datatype, so it has two constructors per argument. But
  -- erasure would probably not be smart enough to notice.

  -- Should we rewrite this as two separate datatypes?
  data SumChange : X ⊎ Y → Set ℓ where
    ch₁ : ∀ {x} → (dx : Δ x) → SumChange (inj₁ x)
    rp₁₂ : ∀ {x} → (y : Y) → SumChange (inj₁ x)
    ch₂ : ∀ {y} → (dy : Δ y) → SumChange (inj₂ y)
    rp₂₁ : ∀ {y} → (x : X) → SumChange (inj₂ y)

  _⊕_ : (v : X ⊎ Y) → SumChange v → X ⊎ Y
  inj₁ x ⊕ ch₁ dx = inj₁ (x ⊞ dx)
  inj₂ y ⊕ ch₂ dy = inj₂ (y ⊞ dy)
  inj₁ x ⊕ rp₁₂ y = inj₂ y
  inj₂ y ⊕ rp₂₁ x = inj₁ x

  _⊝_ : ∀ (v₂ v₁ : X ⊎ Y) → SumChange v₁
  inj₁ x₂ ⊝ inj₁ x₁ = ch₁ (x₂ ⊟ x₁)
  inj₂ y₂ ⊝ inj₂ y₁ = ch₂ (y₂ ⊟ y₁)
  inj₂ y₂ ⊝ inj₁ x₁ = rp₁₂ y₂
  inj₁ x₂ ⊝ inj₂ y₁ = rp₂₁ x₂

  s-nil : (v : X ⊎ Y) → SumChange v
  s-nil (inj₁ x) = ch₁ (nil x)
  s-nil (inj₂ y) = ch₂ (nil y)

  s-update-diff : ∀ (u v : X ⊎ Y) → v ⊕ (u ⊝ v) ≡ u
  s-update-diff (inj₁ x₂) (inj₁ x₁) = cong inj₁ (update-diff x₂ x₁)
  s-update-diff (inj₂ y₂) (inj₂ y₁) = cong inj₂ (update-diff y₂ y₁)
  s-update-diff (inj₁ x₂) (inj₂ y₁) = refl
  s-update-diff (inj₂ y₂) (inj₁ x₁) = refl

  s-update-nil : ∀ v → v ⊕ (s-nil v) ≡ v
  s-update-nil (inj₁ x) = cong inj₁ (update-nil x)
  s-update-nil (inj₂ y) = cong inj₂ (update-nil y)

  instance
    changeAlgebraSums : ChangeAlgebra (X ⊎ Y)
    changeAlgebraSums = record
      { Change = SumChange
      ; update = _⊕_
      ; diff = _⊝_
      ; nil = s-nil
      ; isChangeAlgebra = record
        { update-diff = s-update-diff
        ; update-nil = s-update-nil
        }
      }

  inj₁′ : Δ (inj₁ as (X → (X ⊎ Y)))
  inj₁′ = nil inj₁

  inj₁′-realizer : RawChange (inj₁ as (X → (X ⊎ Y)))
  inj₁′-realizer x dx = ch₁ dx

  inj₁′Derivative : IsDerivative (inj₁ as (X → (X ⊎ Y))) inj₁′-realizer
  inj₁′Derivative x dx = refl

  inj₁′-realizer-correct : ∀ a da → apply inj₁′ a da ≙₍ inj₁ a as (X ⊎ Y) ₎ inj₁′-realizer a da
  inj₁′-realizer-correct a da = diff-update

  inj₁′-faster-w-proof : equiv-raw-change-to-change-ResType inj₁ inj₁′-realizer
  inj₁′-faster-w-proof = equiv-raw-change-to-change inj₁ inj₁′ inj₁′-realizer inj₁′-realizer-correct
  inj₁′-faster : Δ inj₁
  inj₁′-faster = proj₁ inj₁′-faster-w-proof

  inj₂′ : Δ (inj₂ as (Y → (X ⊎ Y)))
  inj₂′ = nil inj₂

  inj₂′-realizer : RawChange (inj₂ as (Y → (X ⊎ Y)))
  inj₂′-realizer y dy = ch₂ dy

  inj₂′Derivative : IsDerivative (inj₂ as (Y → (X ⊎ Y))) inj₂′-realizer
  inj₂′Derivative y dy = refl

  inj₂′-realizer-correct : ∀ b db → apply inj₂′ b db ≙₍ inj₂ b as (X ⊎ Y) ₎ inj₂′-realizer b db
  inj₂′-realizer-correct b db = diff-update

  inj₂′-faster-w-proof : equiv-raw-change-to-change-ResType inj₂ inj₂′-realizer
  inj₂′-faster-w-proof = equiv-raw-change-to-change inj₂ inj₂′ inj₂′-realizer inj₂′-realizer-correct
  inj₂′-faster : Δ inj₂
  inj₂′-faster = proj₁ inj₂′-faster-w-proof

  module _ {Z : Set ℓ} {{CZ : ChangeAlgebra Z}} where
    -- Elimination form for sums. This is a less dependently-typed version of
    -- [_,_].
    match : (X → Z) → (Y → Z) → X ⊎ Y → Z
    match f g (inj₁ x) = f x
    match f g (inj₂ y) = g y

    match′ : Δ match
    match′ = nil match

    match′-realizer : (f : X → Z) → Δ f → (g : Y → Z) → Δ g → (s : X ⊎ Y) → Δ s → Δ (match f g s)
    match′-realizer f df g dg (inj₁ x) (ch₁ dx) = apply df x dx
    match′-realizer f df g dg (inj₁ x) (rp₁₂ y) = ((g ⊞ dg) y) ⊟ (f x)
    match′-realizer f df g dg (inj₂ y) (rp₂₁ x) = ((f ⊞ df) x) ⊟ (g y)
    match′-realizer f df g dg (inj₂ y) (ch₂ dy) = apply dg y dy

    match′-realizer-correct :
      (f : X → Z) → (df : Δ f) → (g : Y → Z) → (dg : Δ g) → (s : X ⊎ Y) → (ds : Δ s) →
      apply (apply (apply match′ f df) g dg) s ds ≙₍ match f g s ₎ match′-realizer f df g dg s ds
    match′-realizer-correct f df g dg (inj₁ x) (ch₁ dx) = ≙-incrementalization f df x dx
    match′-realizer-correct f df g dg (inj₁ x) (rp₁₂ y) = ≙-refl
    match′-realizer-correct f df g dg (inj₂ y) (ch₂ dy) = ≙-incrementalization g dg y dy
    match′-realizer-correct f df g dg (inj₂ y) (rp₂₁ x) = ≙-refl

    -- We need a ternary variant of the lemma here.
    match′-faster-w-proof : equiv-raw-change-to-change-ternary-ResType match match′-realizer
    match′-faster-w-proof = equiv-raw-change-to-change-ternary match match′ match′-realizer match′-realizer-correct

    match′-faster : Δ match
    match′-faster = proj₁ match′-faster-w-proof

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Product.Relation.Binary.Lex.Strict directly.
------------------------------------------------------------------------

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

module Data.Product.Relation.Lex.Strict where

open import Data.Product.Relation.Binary.Lex.Strict public


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

open import Categories.Category

module Categories.Functor.Hom.Properties.Covariant {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Function.Equality using (Π)
open import Relation.Binary using (Setoid)

open import Categories.Category.Construction.Cones
open import Categories.Category.Instance.Setoids
open import Categories.Diagram.Cone.Properties
open import Categories.Diagram.Limit
open import Categories.Functor
open import Categories.Functor.Limits
open import Categories.Functor.Hom

import Categories.Morphism.Reasoning as MR

private
  variable
    o′ ℓ′ e′ : Level
    J : Category o′ ℓ′ e′
  module C = Category C

open Category C
open Hom C
open Π

-- Hom functor preserves limits in C
module _ (W : Obj) {F : Functor J C} (lim : Limit F) where
  private
    module F   = Functor F
    module lim = Limit lim
    open lim
    HomF : Functor J (Setoids ℓ e)
    HomF = Hom[ W ,-] ∘F F
    open HomReasoning
    open MR C

    ⊤ : Cone HomF
    ⊤ = F-map-Coneˡ Hom[ W ,-] limit

    module _ (K : Cone HomF) where
      private
        module K = Cone _ K

      KW : Setoid.Carrier (Cone.N K) → Cone F
      KW x = record
        { N    = W
        ; apex = record
          { ψ       = λ X → K.ψ X ⟨$⟩ x
          ; commute = λ f → ⟺ (∘-resp-≈ʳ identityʳ) ○ K.commute f (Setoid.refl K.N)
          }
        }

      ! : Cones HomF [ K , ⊤ ]
      ! = record
        { arr     = record
          { _⟨$⟩_ = λ x → rep (KW x)
          ; cong  = λ {x y} eq → ψ-≈⇒rep-≈ F W (Cone.apex (KW x)) (Cone.apex (KW y)) lim
                                              (λ A → cong (K.ψ A) eq)
          }
        ; commute = λ {X} {x y} eq → begin
          proj X ∘ rep (KW x) ∘ C.id ≈⟨ refl⟩∘⟨ C.identityʳ ⟩
          proj X ∘ rep (KW x)        ≈⟨ lim.commute ⟩
          K.ψ X ⟨$⟩ x                ≈⟨ cong (K.ψ X) eq ⟩
          K.ψ X ⟨$⟩ y                ∎
        }

    !-unique : ∀ {K : Cone HomF} (f : Cones HomF [ K , ⊤ ]) → Cones HomF [ ! K ≈ f ]
    !-unique {K} f {x} {y} x≈y = begin
      rep (KW K x) ≈⟨ terminal.!-unique f′ ⟩
      f.arr ⟨$⟩ x  ≈⟨ cong f.arr x≈y ⟩
      f.arr ⟨$⟩ y  ∎
      where module K = Cone _ K
            module f = Cone⇒ _ f

            f′ : Cones F [ KW K x , limit ]
            f′ = record
              { arr     = f.arr ⟨$⟩ x
              ; commute = ⟺ (∘-resp-≈ʳ C.identityʳ) ○ f.commute (Setoid.refl K.N)
              }

  hom-resp-limit : Limit HomF
  hom-resp-limit = record
    { terminal = record
      { ⊤             = ⊤
      ; ⊤-is-terminal = record
        { !        = ! _
        ; !-unique = !-unique
        }
      }
    }

Hom-Continuous : ∀ X o′ ℓ′ e′ → Continuous o′ ℓ′ e′ Hom[ X ,-]
Hom-Continuous X _ _ _ L = terminal.⊤-is-terminal
  where open Limit (hom-resp-limit X L)

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:
module Issue947 where

A : Set₁
A = Set
  where

B : Set₁
B = Set
  module _ where

C : Set₁
C = Set
  module M where

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Module.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open import Cubical.Algebra.Ring
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Group

open Iso

private
  variable
    ℓ ℓ' : Level

record IsLeftModule (R : Ring ℓ) {M : Type ℓ'}
  (0m : M)
  (_+_ : M → M → M)
  (-_ : M → M)
  (_⋆_ : ⟨ R ⟩ → M → M) : Type (ℓ-max ℓ ℓ') where

  open RingStr (snd R) using (_·_; 1r) renaming (_+_ to _+r_)

  field
    +IsAbGroup : IsAbGroup 0m _+_ -_
    ⋆Assoc : (r s : ⟨ R ⟩) (x : M) → (r · s) ⋆ x ≡ r ⋆ (s ⋆ x)
    ⋆DistR+ : (r : ⟨ R ⟩) (x y : M) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y)
    ⋆DistL+ : (r s : ⟨ R ⟩) (x : M) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x)
    ⋆IdL   : (x : M) → 1r ⋆ x ≡ x

  open IsAbGroup +IsAbGroup public
    renaming
    ( isSemigroup to +IsSemigroup
    ; isMonoid    to +IsMonoid
    ; isGroup     to +IsGroup
    )

unquoteDecl IsLeftModuleIsoΣ = declareRecordIsoΣ IsLeftModuleIsoΣ (quote IsLeftModule)

record LeftModuleStr (R : Ring ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where

  field
    0m             : A
    _+_            : A → A → A
    -_             : A → A
    _⋆_            : ⟨ R ⟩ → A → A
    isLeftModule   : IsLeftModule R 0m _+_ -_ _⋆_

  open IsLeftModule isLeftModule public

LeftModule : (R : Ring ℓ) → ∀ ℓ' → Type (ℓ-max ℓ (ℓ-suc ℓ'))
LeftModule R ℓ' = Σ[ A ∈ Type ℓ' ] LeftModuleStr R A

module _ {R : Ring ℓ} where

  module _ (M : LeftModule R ℓ') where
    LeftModule→AbGroup : AbGroup ℓ'
    LeftModule→AbGroup .fst = M .fst
    LeftModule→AbGroup .snd .AbGroupStr.0g = _
    LeftModule→AbGroup .snd .AbGroupStr._+_ = _
    LeftModule→AbGroup .snd .AbGroupStr.-_  = _
    LeftModule→AbGroup .snd .AbGroupStr.isAbGroup =
      IsLeftModule.+IsAbGroup (M .snd .LeftModuleStr.isLeftModule)

  isSetLeftModule : (M : LeftModule R ℓ') → isSet ⟨ M ⟩
  isSetLeftModule M = isSetAbGroup (LeftModule→AbGroup M)

  open RingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·s_)

  module _  {M : Type ℓ'} {0m : M}
           {_+_ : M → M → M} { -_ : M → M} {_⋆_ : ⟨ R ⟩ → M → M}
                  (isSet-M : isSet M)
                  (+Assoc  :  (x y z : M) → x + (y + z) ≡ (x + y) + z)
                  (+IdR    : (x : M) → x + 0m ≡ x)
                  (+InvR   : (x : M) → x + (- x) ≡ 0m)
                  (+Comm   : (x y : M) → x + y ≡ y + x)
                  (⋆Assoc  : (r s : ⟨ R ⟩) (x : M) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
                  (⋆DistR+ : (r : ⟨ R ⟩) (x y : M) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
                  (⋆DistL+ : (r s : ⟨ R ⟩) (x : M) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
                  (⋆IdL    : (x : M) → 1r ⋆ x ≡ x)
    where

    makeIsLeftModule : IsLeftModule R 0m _+_ -_ _⋆_
    makeIsLeftModule .IsLeftModule.+IsAbGroup = makeIsAbGroup isSet-M +Assoc +IdR +InvR +Comm
    makeIsLeftModule .IsLeftModule.⋆Assoc = ⋆Assoc
    makeIsLeftModule .IsLeftModule.⋆DistR+ = ⋆DistR+
    makeIsLeftModule .IsLeftModule.⋆DistL+ = ⋆DistL+
    makeIsLeftModule .IsLeftModule.⋆IdL = ⋆IdL

record IsLeftModuleHom {R : Ring ℓ} {A B : Type ℓ'}
  (M : LeftModuleStr R A) (f : A → B) (N : LeftModuleStr R B)
  : Type (ℓ-max ℓ ℓ')
  where

  -- Shorter qualified names
  private
    module M = LeftModuleStr M
    module N = LeftModuleStr N

  field
    pres0 : f M.0m ≡ N.0m
    pres+ : (x y : A) → f (x M.+ y) ≡ f x N.+ f y
    pres- : (x : A) → f (M.- x) ≡ N.- (f x)
    pres⋆ : (r : ⟨ R ⟩) (y : A) → f (r M.⋆ y) ≡ r N.⋆ f y

LeftModuleHom : {R : Ring ℓ} (M N : LeftModule R ℓ') → Type (ℓ-max ℓ ℓ')
LeftModuleHom M N = Σ[ f ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsLeftModuleHom (M .snd) f (N .snd)

IsLeftModuleEquiv : {R : Ring ℓ} {A B : Type ℓ'}
  (M : LeftModuleStr R A) (e : A ≃ B) (N : LeftModuleStr R B)
  → Type (ℓ-max ℓ ℓ')
IsLeftModuleEquiv M e N = IsLeftModuleHom M (e .fst) N

LeftModuleEquiv : {R : Ring ℓ} (M N : LeftModule R ℓ') → Type (ℓ-max ℓ ℓ')
LeftModuleEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsLeftModuleEquiv (M .snd) e (N .snd)

isPropIsLeftModule : (R : Ring ℓ) {M : Type ℓ'}
  (0m : M)
  (_+_ : M → M → M)
  (-_ : M → M)
  (_⋆_ : ⟨ R ⟩ → M → M)
  → isProp (IsLeftModule R 0m _+_ -_ _⋆_)
isPropIsLeftModule R _ _ _ _ =
  isOfHLevelRetractFromIso 1 IsLeftModuleIsoΣ
    (isPropΣ (isPropIsAbGroup _ _ _)
      (λ ab →
        isProp× (isPropΠ3 λ _ _ _ → ab .is-set _ _)
          (isProp× (isPropΠ3 λ _ _ _ → ab .is-set _ _)
            (isProp× (isPropΠ3 λ _ _ _ → ab .is-set _ _)
              (isPropΠ λ _ → ab .is-set _ _)))))
  where
  open IsAbGroup

𝒮ᴰ-LeftModule : (R : Ring ℓ) → DUARel (𝒮-Univ ℓ') (LeftModuleStr R) (ℓ-max ℓ ℓ')
𝒮ᴰ-LeftModule R =
  𝒮ᴰ-Record (𝒮-Univ _) (IsLeftModuleEquiv {R = R})
    (fields:
      data[ 0m ∣ autoDUARel _ _ ∣ pres0 ]
      data[ _+_ ∣ autoDUARel _ _ ∣ pres+ ]
      data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
      data[ _⋆_ ∣ autoDUARel _ _ ∣ pres⋆ ]
      prop[ isLeftModule ∣ (λ _ _ → isPropIsLeftModule _ _ _ _ _) ])
  where
  open LeftModuleStr
  open IsLeftModuleHom

LeftModulePath : {R : Ring ℓ} (M N : LeftModule R ℓ') → (LeftModuleEquiv M N) ≃ (M ≡ N)
LeftModulePath {R = R} = ∫ (𝒮ᴰ-LeftModule R) .UARel.ua


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

open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Data.Nat using (ℕ; suc; zero)
open import Data.Empty using (⊥)
open import Data.Vec using (Vec)
                     renaming ([] to []ⱽ; _∷_ to _∷ⱽ_)

module FLA.Data.Vec+.Base where

private
  variable
    ℓ : Level
    A : Set ℓ
    n : ℕ

-- TODO: Can this be replaced with something like the List⁺ definition so that
-- the proofs from Vec can be transferred? This definition is convenient because
-- the size is correct (it is not n - 1).
data Vec⁺ (A : Set ℓ) : ℕ → Set ℓ where
  [_] : A → Vec⁺ A 1
  _∷_ : ∀ {n} (x : A) (xs : Vec⁺ A n) → Vec⁺ A (suc n)

infixr 5 _∷_

-- Want to prove that is it not possible to construct an empty vector
emptyVecImpossible : Vec⁺ A 0 → ⊥
emptyVecImpossible = λ ()

Vec⁺→Vec : Vec⁺ A n → Vec A n
Vec⁺→Vec [ v ] = v ∷ⱽ []ⱽ
Vec⁺→Vec (v ∷ vs⁺) = v ∷ⱽ Vec⁺→Vec vs⁺

Vec⁺→n≢0 : Vec⁺ A n → n ≢ 0
Vec⁺→n≢0 {ℓ} {A} {suc n} v = suc≢0
  where
    suc≢0 : {n : ℕ} → suc n ≢ 0
    suc≢0 {zero} ()
    suc≢0 {suc n} = λ ()

-- Closer maybe but still buggered
-- Vec→Vec⁺ : ∀ {ℓ} → {A : Set ℓ} {n : ℕ} → (n ≢ 0) → Vec A n → Vec⁺ A n
-- Vec→Vec⁺ {ℓ} {A} {0} p []ⱽ = ⊥-elim (p refl)
-- Vec→Vec⁺ {ℓ} {A} {1} p (x ∷ⱽ []ⱽ) = [ x ]
-- Vec→Vec⁺ {ℓ} {A} {suc n} p (x ∷ⱽ xs) = x ∷ (Vec→Vec⁺ {!!} xs)

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


text:
{-

This file contains:
  - The inductive construction of James.

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.James.Inductive.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Nat

open import Cubical.HITs.SequentialColimit

private
  variable
    ℓ : Level

module _
  (X∙@(X , x₀) : Pointed ℓ) where

  -- The family 𝕁ames n is equivalence to Brunerie's J n

  data 𝕁ames : ℕ → Type ℓ where
    [] : 𝕁ames 0
    _∷_   : {n : ℕ} → X → 𝕁ames n → 𝕁ames (1 + n)
    incl  : {n : ℕ} → 𝕁ames n → 𝕁ames (1 + n)
    incl∷ : {n : ℕ} → (x : X)(xs : 𝕁ames n) → incl (x ∷ xs) ≡ x ∷ incl xs
    unit  : {n : ℕ} → (xs : 𝕁ames n) → incl xs ≡ x₀ ∷ xs
    coh   : {n : ℕ} → (xs : 𝕁ames n) → PathP (λ i → incl (unit xs i) ≡ x₀ ∷ incl xs) (unit (incl xs)) (incl∷ x₀ xs)

  -- The direct system defined by 𝕁ames

  open Sequence

  𝕁amesSeq : Sequence ℓ
  𝕁amesSeq .space = 𝕁ames
  𝕁amesSeq .map   = incl

  -- The 𝕁ames∞ wanted is the direct colimit of 𝕁ames n

  𝕁ames∞ : Type ℓ
  𝕁ames∞ = Lim→ 𝕁amesSeq


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

module Note where

open import Data.Integer using (ℤ)
open import Data.Nat     using (ℕ; _+_; _*_; ⌊_/2⌋)
open import Function     using (_∘_)

open import Pitch        using (Pitch; transposePitch)
open import Interval     using (Upi; Opi; transposePitchInterval)

Duration : Set
Duration = ℕ

data Note : Set where
  tone : Duration → Pitch → Note
  rest : Duration         → Note

noteDuration : Note → ℕ
noteDuration (tone d _) = d
noteDuration (rest d)   = d

liftPitch : (Pitch → Pitch) → Note → Note
liftPitch f (tone d p) = tone d (f p)
liftPitch f (rest d)   = rest d

transposeNote : ℤ → Note → Note
transposeNote = liftPitch ∘ transposePitch

transposeNoteInterval : Opi → Note → Note
transposeNoteInterval = liftPitch ∘ transposePitchInterval

-- rounds down
doubleSpeed : Note → Note
doubleSpeed (tone d p) = tone (⌊_/2⌋ d) p
doubleSpeed (rest d)   = rest (⌊_/2⌋ d)

slowDown : ℕ → Note → Note
slowDown k (tone d p) = tone (d * k) p
slowDown k (rest d)   = rest (d * k)

-- duration in 16th notes
-- assume duration of a 16th note is 1
16th 8th d8th qtr dqtr half whole : Duration
16th   = 1
8th    = 2
d8th   = 3
qtr    = 4
dqtr   = 6
half   = 8
dhalf  = 12
whole  = 16
dwhole = 24

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
------------------------------------------------------------------------
-- A solution to a problem posed by Venanzio Capretta
------------------------------------------------------------------------

module VenanziosProblem where

open import Codata.Musical.Notation
open import Codata.Musical.Stream as Stream
  using (Stream; _⋎_; evens; odds; _≈_)
open Stream.Stream; open Stream._≈_
open import Data.Nat
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

private
  module S {A : Set} = Setoid (Stream.setoid A)

------------------------------------------------------------------------
-- Problem formulation

-- The problem concerns functions satisfying a certain equation:

rhs : {A : Set} → (Stream A → Stream A) → Stream A → Stream A
rhs φ s = s ⋎ φ (evens (φ s))

SatisfiesEquation : {A : Set} → (Stream A → Stream A) → Set
SatisfiesEquation φ = ∀ s → φ s ≈ rhs φ s

-- The statement of the problem:

Statement : Set₁
Statement = {A : Set} {φ₁ φ₂ : Stream A → Stream A} →
            SatisfiesEquation φ₁ → SatisfiesEquation φ₂ →
            ∀ s → φ₁ s ≈ φ₂ s

------------------------------------------------------------------------
-- Solution

module Solution {A : Set} where

  infixr 5 _∷_
  infix  4 _∣_∣_≈P_ _∣_∣_≈W_
  infix  3 _∎
  infixr 2 _≈⟨_⟩_

  -- Let us first define a small language of equality proofs.
  --
  -- m ∣ n ∣ xs ≈P ys means that xs and ys, which are streams
  -- generated in chunks of size 1 + m, where the outer chunk has size
  -- n, are equal.

  mutual

    -- Weak head normal forms of programs.

    data _∣_∣_≈W_ : ℕ → ℕ → Stream A → Stream A → Set where
      reset : ∀ {xs₁ xs₂ m} (xs₁≈xs₂ : ∞ (m ∣ suc m ∣ xs₁ ≈P xs₂)) →
              m ∣ 0 ∣ xs₁ ≈W xs₂
      _∷_   : ∀ x {xs₁ xs₂ m n} (xs₁≈xs₂ : m ∣ n ∣ ♭ xs₁ ≈W ♭ xs₂) →
              m ∣ suc n ∣ x ∷ xs₁ ≈W x ∷ xs₂

    -- Programs.

    data _∣_∣_≈P_ : ℕ → ℕ → Stream A → Stream A → Set where

      -- WHNFs are programs.
      ↑          : ∀ {m n xs₁ xs₂} (xs₁≈xs₂ : m ∣ n ∣ xs₁ ≈W xs₂) →
                   m ∣ n ∣ xs₁ ≈P xs₂

      -- Various congruences.
      _∷_        : ∀ x {xs₁ xs₂ m n} (xs₁≈xs₂ : m ∣ n ∣ ♭ xs₁ ≈P ♭ xs₂) →
                   m ∣ suc n ∣ x ∷ xs₁ ≈P x ∷ xs₂
      _⋎-cong_   : ∀ {xs₁ xs₂ ys₁ ys₂}
                   (xs₁≈xs₂ : 1 ∣ 1 ∣ xs₁ ≈P xs₂)
                   (ys₁≈ys₂ : 0 ∣ 1 ∣ ys₁ ≈P ys₂) →
                   1 ∣ 2 ∣ xs₁ ⋎ ys₁ ≈P xs₂ ⋎ ys₂
      evens-cong : ∀ {xs₁ xs₂}
                   (xs₁≈xs₂ : 1 ∣ 1 ∣ xs₁ ≈P xs₂) →
                   0 ∣ 1 ∣ evens xs₁ ≈P evens xs₂
      odds-cong  : ∀ {xs₁ xs₂}
                   (xs₁≈xs₂ : 1 ∣ 2 ∣ xs₁ ≈P xs₂) →
                   0 ∣ 1 ∣ odds xs₁ ≈P odds xs₂

      -- Equational reasoning.
      _≈⟨_⟩_     : ∀ xs₁ {xs₂ xs₃ m n}
                   (xs₁≈xs₂ : m ∣ n ∣ xs₁ ≈P xs₂)
                   (xs₂≈xs₃ : m ∣ n ∣ xs₂ ≈P xs₃) →
                   m ∣ n ∣ xs₁ ≈P xs₃
      _∎         : ∀ {n m} xs → m ∣ n ∣ xs ≈P xs

      -- If we have already produced 1 + n elements of the last chunk,
      -- then it is safe to pretend that we have only produced n
      -- elements.
      shift      : ∀ {n m xs₁ xs₂} (xs₁≈xs₂ : m ∣ suc n ∣ xs₁ ≈P xs₂) →
                   m ∣ n ∣ xs₁ ≈P xs₂

      -- A variation of the statement we want to prove.
      goal′      : ∀ {φ₁ φ₂ xs₁ xs₂}
                   (s₁ : SatisfiesEquation φ₁)
                   (s₂ : SatisfiesEquation φ₂)
                   (xs₁≈xs₂ : 0 ∣ 1 ∣ xs₁ ≈P xs₂) →
                   1 ∣ 1 ∣ rhs φ₁ xs₁ ≈P rhs φ₂ xs₂

  -- The equality language is complete.

  completeW : ∀ {n m xs ys} → xs ≈ ys → m ∣ n ∣ xs ≈W ys
  completeW {zero}  xs≈ys            = reset (♯ ↑ (completeW xs≈ys))
  completeW {suc n} (P.refl ∷ xs≈ys) = _ ∷ completeW (♭ xs≈ys)

  -- If we can prove that the equality language is sound, then the
  -- following lemma implies the intended result.

  goal : ∀ {φ₁ φ₂ xs₁ xs₂}
         (s₁ : SatisfiesEquation φ₁) (s₂ : SatisfiesEquation φ₂) →
         0 ∣ 1 ∣ xs₁ ≈P xs₂ → 1 ∣ 1 ∣ φ₁ xs₁ ≈P φ₂ xs₂
  goal {φ₁} {φ₂} {xs₁} {xs₂} s₁ s₂ xs₁≈xs₂ =
    φ₁ xs₁      ≈⟨ ↑ (completeW (s₁ xs₁)) ⟩
    rhs φ₁ xs₁  ≈⟨ goal′ s₁ s₂ xs₁≈xs₂ ⟩
    rhs φ₂ xs₂  ≈⟨ ↑ (completeW (S.sym (s₂ xs₂))) ⟩
    φ₂ xs₂      ∎

  -- Some lemmas about weak head normal forms.

  evens-congW : {xs₁ xs₂ : Stream A} →
                1 ∣ 1 ∣ xs₁ ≈W xs₂ → 0 ∣ 1 ∣ evens xs₁ ≈W evens xs₂
  evens-congW (x ∷ reset xs₁≈xs₂) =
    x ∷ reset (♯ odds-cong (♭ xs₁≈xs₂))

  reflW : ∀ xs {m} n → m ∣ n ∣ xs ≈W xs
  reflW xs       zero    = reset (♯ (xs ∎))
  reflW (x ∷ xs) (suc n) = x ∷ reflW (♭ xs) n

  transW : ∀ {xs ys zs m n} →
           m ∣ n ∣ xs ≈W ys → m ∣ n ∣ ys ≈W zs → m ∣ n ∣ xs ≈W zs
  transW (x ∷ xs≈ys)   (.x ∷ ys≈zs)  = x ∷ transW xs≈ys ys≈zs
  transW (reset xs≈ys) (reset ys≈zs) =
    reset (♯ (_ ≈⟨ ♭ xs≈ys ⟩ ♭ ys≈zs))

  shiftW : ∀ n {m xs₁ xs₂} →
           m ∣ suc n ∣ xs₁ ≈W xs₂ → m ∣ n ∣ xs₁ ≈W xs₂
  shiftW zero    (x ∷ reset xs₁≈xs₂) = reset (♯ (x ∷ shift (♭ xs₁≈xs₂)))
  shiftW (suc n) (x ∷       xs₁≈xs₂) = x ∷ shiftW n xs₁≈xs₂

  -- Every program can be transformed into WHNF.

  whnf : ∀ {xs ys m n} → m ∣ n ∣ xs ≈P ys → m ∣ n ∣ xs ≈W ys
  whnf (↑ xs≈ys) = xs≈ys

  whnf (x ∷ xs₁≈xs₂) = x ∷ whnf xs₁≈xs₂

  whnf (xs₁≈xs₂ ⋎-cong ys₁≈ys₂) with whnf xs₁≈xs₂ | whnf ys₁≈ys₂
  ... | x ∷ reset xs₁≈xs₂′ | y ∷ reset ys₁≈ys₂′ =
    x ∷ y ∷ reset (♯ (shift (♭ xs₁≈xs₂′) ⋎-cong ♭ ys₁≈ys₂′))

  whnf (evens-cong xs₁≈xs₂) = evens-congW (whnf xs₁≈xs₂)

  whnf (odds-cong xs₁≈xs₂) with whnf xs₁≈xs₂
  ... | x ∷ xs₁≈xs₂′ = evens-congW xs₁≈xs₂′

  whnf (xs₁ ≈⟨ xs₁≈xs₂ ⟩ xs₂≈xs₃) = transW (whnf xs₁≈xs₂) (whnf xs₂≈xs₃)
  whnf (xs ∎)                     = reflW xs _

  whnf (shift xs₁≈xs₂) = shiftW _ (whnf xs₁≈xs₂)

  whnf (goal′ s₁ s₂ xs₁≈xs₂) with whnf xs₁≈xs₂
  ... | (x ∷ reset xs₁≈xs₂′) =
    x ∷ reset (♯ (goal s₁ s₂ (evens-cong (goal s₁ s₂ xs₁≈xs₂))
                    ⋎-cong
                  ♭ xs₁≈xs₂′))

  -- Soundness follows by a corecursive repetition of the whnf
  -- procedure.

  ⟦_⟧W : ∀ {xs ys m n} → m ∣ n ∣ xs ≈W ys → xs ≈ ys
  ⟦ reset ys≈zs ⟧W with whnf (♭ ys≈zs)
  ... | x ∷ ys≈zs′ = P.refl ∷ ♯ ⟦ ys≈zs′ ⟧W
  ⟦ x ∷ ys≈zs   ⟧W = P.refl ∷ ♯ ⟦ ys≈zs ⟧W

  ⟦_⟧P : ∀ {xs ys m n} → m ∣ n ∣ xs ≈P ys → xs ≈ ys
  ⟦ xs≈ys ⟧P = ⟦ whnf xs≈ys ⟧W

-- Wrapping up.

solution : Statement
solution s₁ s₂ s = ⟦ goal s₁ s₂ (s ∎) ⟧P
  where open Solution

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


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

open import HoTT
open import groups.KernelImage

module groups.KernelImageEmap where

module _ {i₀ i₁ j₀ j₁ k₀ k₁}
  {G₀ : Group i₀} {H₀ : Group j₀} {K₀ : Group k₀}
  {G₁ : Group i₁} {H₁ : Group j₁} {K₁ : Group k₁}
  {ψ₀ : H₀ →ᴳ K₀} {φ₀ : G₀ →ᴳ H₀} (H₀-ab : is-abelian H₀)
  {ψ₁ : H₁ →ᴳ K₁} {φ₁ : G₁ →ᴳ H₁} (H₁-ab : is-abelian H₁)
  {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
  (ψ₀∼ψ₁ : CommSquareᴳ ψ₀ ψ₁ ξH ξK)
  (φ₀∼φ₁ : CommSquareᴳ φ₀ φ₁ ξG ξH)
  where

  module ξG = GroupHom ξG
  module ξH = GroupHom ξH
  module ξK = GroupHom ξK
  module ψ₀ = GroupHom ψ₀
  module ψ₁ = GroupHom ψ₁
  module φ₀ = GroupHom φ₀
  module φ₁ = GroupHom φ₁

  private
    f : Ker/Im.El ψ₀ φ₀ H₀-ab → Ker/Im.El ψ₁ φ₁ H₁-ab
    f = SetQuot-rec to pres-rel
      where
        abstract
          ξh-in-Ker : ∀ h (ψ₀h=0 : ψ₀.f h == Group.ident K₀)
            → ψ₁.f (ξH.f h) == Group.ident K₁
          ξh-in-Ker h ψ₀h=0 = (! $ ψ₀∼ψ₁ □$ᴳ h) ∙ ap ξK.f ψ₀h=0 ∙ ξK.pres-ident

        to : Ker.El ψ₀ → Ker/Im.El ψ₁ φ₁ H₁-ab
        to (h , ψ₀h=0) = q[ ξH.f h , ξh-in-Ker h ψ₀h=0 ]

        abstract
          pres-rel : ∀ {h h'}
            → ker/im-rel ψ₀ φ₀ H₀-ab h h'
            → to h == to h'
          pres-rel {(h , _)} {(h' , _)} = Trunc-rec
            λ{(g , φg=h-h') → quot-rel
              [ ξG.f g , (! $ φ₀∼φ₁ □$ᴳ g) ∙ ap ξH.f φg=h-h' ∙ ξH.pres-diff h h' ]}

    abstract
      f-is-hom : preserves-comp (Ker/Im.comp ψ₀ φ₀ H₀-ab) (Ker/Im.comp ψ₁ φ₁ H₁-ab) f
      f-is-hom = SetQuot-elim
        (λ{(h , _) → SetQuot-elim
          (λ{(h' , _) → ap q[_] (Ker.El=-out ψ₁ (ξH.pres-comp h h'))})
          (λ _ → prop-has-all-paths-↓)})
        (λ _ → prop-has-all-paths-↓)

  Ker/Im-fmap : Ker/Im ψ₀ φ₀ H₀-ab →ᴳ Ker/Im ψ₁ φ₁ H₁-ab
  Ker/Im-fmap = group-hom f f-is-hom

module _ {i₀ i₁ j₀ j₁ k₀ k₁}
  {G₀ : Group i₀} {H₀ : Group j₀} {K₀ : Group k₀}
  {G₁ : Group i₁} {H₁ : Group j₁} {K₁ : Group k₁}
  {ψ₀ : H₀ →ᴳ K₀} {φ₀ : G₀ →ᴳ H₀} (H₀-ab : is-abelian H₀)
  {ψ₁ : H₁ →ᴳ K₁} {φ₁ : G₁ →ᴳ H₁} (H₁-ab : is-abelian H₁)
  {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
  (ψ₀∼ψ₁ : CommSquareᴳ ψ₀ ψ₁ ξH ξK)
  (φ₀∼φ₁ : CommSquareᴳ φ₀ φ₁ ξG ξH)
  (ξG-ise : is-equiv (GroupHom.f ξG))
  (ξH-ise : is-equiv (GroupHom.f ξH))
  (ξK-ise : is-equiv (GroupHom.f ξK))
  where

  private
    to : Ker/Im.El ψ₀ φ₀ H₀-ab → Ker/Im.El ψ₁ φ₁ H₁-ab
    to = GroupHom.f (Ker/Im-fmap H₀-ab H₁-ab ψ₀∼ψ₁ φ₀∼φ₁)

    from : Ker/Im.El ψ₁ φ₁ H₁-ab → Ker/Im.El ψ₀ φ₀ H₀-ab
    from = GroupHom.f (Ker/Im-fmap H₁-ab H₀-ab (CommSquareᴳ-inverse-v ψ₀∼ψ₁ ξH-ise ξK-ise) (CommSquareᴳ-inverse-v φ₀∼φ₁ ξG-ise ξH-ise))

    abstract
      to-from : ∀ x → to (from x) == x
      to-from = SetQuot-elim
        {{=-preserves-level ⟨⟩}}
        (λ{(h , _) → ap q[_] $ Ker.El=-out ψ₁ $ is-equiv.f-g ξH-ise h})
        (λ {h} {h'} _ → prop-has-all-paths-↓ {{has-level-apply SetQuot-is-set (to (from q[ h' ])) q[ h' ]}})

      from-to : ∀ x → from (to x) == x
      from-to = SetQuot-elim
        {{=-preserves-level ⟨⟩}}
        (λ{(h , _) → ap q[_] $ Ker.El=-out ψ₀ $ is-equiv.g-f ξH-ise h})
        (λ {h} {h'} _ → prop-has-all-paths-↓ {{has-level-apply SetQuot-is-set (from (to q[ h' ])) q[ h' ]}})

  Ker/Im-emap : Ker/Im ψ₀ φ₀ H₀-ab ≃ᴳ Ker/Im ψ₁ φ₁ H₁-ab
  Ker/Im-emap = Ker/Im-fmap H₀-ab H₁-ab ψ₀∼ψ₁ φ₀∼φ₁ ,
    is-eq to from to-from from-to

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module WErrorOverride where

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}
{-# BUILTIN IO IO #-}

infixl 1 _>>=_

postulate
  return : {A : Set} → A → IO A
  _>>=_  : {A : Set} {B : Set} → IO A → (A → IO B) → IO B

{-# COMPILED return (\_ -> return)    #-}
{-# COMPILED _>>=_  (\_ _ -> (>>=)) #-}

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

-- An error should be raised if one tries to do something like this:

data PartialBool : Set where
  true : PartialBool

{-# COMPILED_DATA PartialBool Bool True #-}

-- However one can override such behaviour by passing the flag
-- --ghc-flag=-Wwarn to Agda upon compilation.

main = return true


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Unary.All.Properties directly.
------------------------------------------------------------------------

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

module Data.Vec.All.Properties where

open import Data.Vec.Relation.Unary.All.Properties public


text:
{-# OPTIONS --prop --rewriting #-}

module Examples where

-- Sequential
import Examples.Id
import Examples.Gcd
import Examples.Queue

-- Parallel
import Examples.TreeSum
import Examples.Exp2

-- Hybrid
import Examples.Sorting

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

open import HoTT
import homotopy.ConstantToSetExtendsToProp as ConstExt
open import homotopy.RibbonCover

module homotopy.GroupSetsRepresentCovers {i} (X : Ptd i)
  {{_ : is-connected 0 (de⊙ X)}} where

  open Cover

  private
    A : Type i
    A = de⊙ X
    a₁ : A
    a₁ = pt X

  -- A covering space constructed from a G-set.
  grpset-to-cover : ∀ {j} → GroupSet (πS 0 X) j → Cover A (lmax i j)
  grpset-to-cover gs = Ribbon-cover X gs

  -- Covering spaces to G-sets.
  cover-to-grpset-struct : ∀ {j} (cov : Cover A j)
    → GroupSetStructure (πS 0 X) (Fiber cov a₁)
  cover-to-grpset-struct cov = record
    { act = cover-trace cov
    ; unit-r = cover-trace-idp₀ cov
    ; assoc = cover-paste cov
    }

  cover-to-grpset : ∀ {j} → Cover A j → GroupSet (πS 0 X) j
  cover-to-grpset cov = record
    { El = Fiber cov a₁
    ; grpset-struct = cover-to-grpset-struct cov
    }

  -- This is derivable from connectedness condition.
  module _ where
    abstract
      [base-path] : ∀ {a₂ : A} → Trunc -1 (a₁ == a₂)
      [base-path] {a₂} =
        –> (Trunc=-equiv [ a₁ ] [ a₂ ]) (contr-has-all-paths [ a₁ ] [ a₂ ])

  -- Part 1: Show that the synthesized cover (ribbon) is fiberwisely
  --         equivalent to the original fiber.
  private
    module _ {j} (cov : Cover A j) where

      -- Suppose that we get the path, we can compute the ribbon easily.
      fiber+path-to-ribbon : ∀ {a₂} (a↑ : Fiber cov a₂) (p : a₁ == a₂)
        → Ribbon X (cover-to-grpset cov) a₂
      fiber+path-to-ribbon {a₂} a↑ p =
        trace (cover-trace cov a↑ [ ! p ]) [ p ]

      abstract
        -- Our construction is "constant" with respect to paths.
        fiber+path-to-ribbon-is-path-irrelevant :
          ∀ {a₂} (a↑ : Fiber cov a₂) (p₁ p₂ : a₁ == a₂)
          → fiber+path-to-ribbon a↑ p₁ == fiber+path-to-ribbon a↑ p₂
        fiber+path-to-ribbon-is-path-irrelevant a↑ p idp =
          trace (cover-trace cov a↑ [ ! p ]) [ p ]
            =⟨ paste a↑ [ ! p ] [ p ] ⟩
          trace a↑ [ ! p ∙ p ]
            =⟨ !₀-inv-l [ p ] |in-ctx trace a↑ ⟩
          trace a↑ idp₀
            ∎

      module FiberAndPathToRibbon {a₂} (a↑ : Fiber cov a₂)
        = ConstExt
          (fiber+path-to-ribbon a↑)
          (fiber+path-to-ribbon-is-path-irrelevant a↑)

      fiber+path₋₁-to-ribbon : ∀ {a₂} (a↑ : Cover.Fiber cov a₂)
        → Trunc -1 (a₁ == a₂) → Ribbon X (cover-to-grpset cov) a₂
      fiber+path₋₁-to-ribbon a↑ = FiberAndPathToRibbon.ext a↑

  -- So the conversion from fiber to ribbon is done.
  fiber-to-ribbon : ∀ {j} (cov : Cover A j)
    → {a₂ : A} (a↑ : Cover.Fiber cov a₂)
    → Ribbon X (cover-to-grpset cov) a₂
  fiber-to-ribbon cov a↑ = fiber+path₋₁-to-ribbon cov a↑ [base-path]

  -- The other direction is easy.
  ribbon-to-fiber : ∀ {j} (cov : Cover A j) {a₂}
    → Ribbon X (cover-to-grpset cov) a₂ → Cover.Fiber cov a₂
  ribbon-to-fiber cov {a₂} r =
    Ribbon-rec (cover-trace cov) (cover-paste cov) r

  private
    -- Some routine computations.
    abstract
      ribbon-to-fiber-to-ribbon : ∀ {j} (cov : Cover A j) {a₂}
        → (r : Ribbon X (cover-to-grpset cov) a₂)
        → fiber-to-ribbon cov (ribbon-to-fiber cov r) == r
      ribbon-to-fiber-to-ribbon cov {a₂} = Ribbon-elim
        {P = λ r → fiber-to-ribbon cov (ribbon-to-fiber cov r) == r}
        (λ a↑ p → Trunc-elim
          -- All ugly things will go away when bp = proj bp′
          {{λ bp → has-level-apply Ribbon-is-set
                    (fiber+path₋₁-to-ribbon cov (cover-trace cov a↑ p) bp)
                    (trace a↑ p)}}
          (lemma a↑ p)
          [base-path])
        (λ _ _ _ → prop-has-all-paths-↓)
        where
          abstract
            lemma : ∀ {a₂} (a↑ : Cover.Fiber cov a₁) (p : a₁ =₀ a₂) (bp : a₁ == a₂)
              → trace {X = X} {gs = cover-to-grpset cov}
                  (cover-trace cov (cover-trace cov a↑ p) [ ! bp ]) [ bp ]
              == trace {X = X} {gs = cover-to-grpset cov} a↑ p
            lemma a↑ p idp =
              trace (cover-trace cov a↑ p) idp₀
                =⟨ paste a↑ p idp₀ ⟩
              trace a↑ (p ∙₀ idp₀)
                =⟨ ap (trace a↑) $ ∙₀-unit-r p ⟩
              trace a↑ p
                ∎

      fiber-to-ribbon-to-fiber : ∀ {j} (cov : Cover A j) {a₂}
        → (a↑ : Cover.Fiber cov a₂)
        → ribbon-to-fiber cov (fiber-to-ribbon cov {a₂} a↑) == a↑
      fiber-to-ribbon-to-fiber cov {a₂} a↑ = Trunc-elim
        -- All ugly things will go away when bp = proj bp′
        {{λ bp → has-level-apply (Cover.Fiber-is-set cov)
                  (ribbon-to-fiber cov
                    (fiber+path₋₁-to-ribbon cov a↑ bp))
                  a↑}}
        (lemma a↑)
        [base-path]
        where
          abstract
            lemma : ∀ {a₂} (a↑ : Cover.Fiber cov a₂) (bp : a₁ == a₂)
              → cover-trace cov (cover-trace cov a↑ [ ! bp ]) [ bp ]
              == a↑
            lemma a↑ idp = idp

  cover-to-grpset-to-cover : ∀ {j} (cov : Cover A (lmax i j))
    → grpset-to-cover (cover-to-grpset cov) == cov
  cover-to-grpset-to-cover cov = cover= λ _ →
    ribbon-to-fiber cov , is-eq
      (ribbon-to-fiber cov)
      (fiber-to-ribbon cov)
      (fiber-to-ribbon-to-fiber cov)
      (ribbon-to-fiber-to-ribbon cov)

  -- The second direction : grpset -> covering -> grpset

  -- Part 2.1: The fiber over the point a is the carrier.
  ribbon-a₁-to-El : ∀ {j} {gs : GroupSet (πS 0 X) j}
    → Ribbon X gs a₁ → GroupSet.El gs
  ribbon-a₁-to-El {j} {gs} = let open GroupSet gs in
    Ribbon-rec act assoc

  ribbon-a₁-to-El-equiv : ∀ {j} {gs : GroupSet (πS 0 X) j}
    → Ribbon X gs a₁ ≃ GroupSet.El gs
  ribbon-a₁-to-El-equiv {j} {gs} = let open GroupSet gs in
    ribbon-a₁-to-El , is-eq _
      (λ r → trace r idp₀)
      (λ a↑ → unit-r a↑)
      (Ribbon-elim
        {P = λ r → trace (ribbon-a₁-to-El r) idp₀ == r}
        (λ y p →
          trace (act y p) idp₀
            =⟨ paste y p idp₀ ⟩
          trace y (p ∙₀ idp₀)
            =⟨ ap (trace y) $ ∙₀-unit-r p ⟩
          trace y p
            ∎)
        (λ _ _ _ → prop-has-all-paths-↓))

  grpset-to-cover-to-grpset : ∀ {j} (gs : GroupSet (πS 0 X) (lmax i j))
    → cover-to-grpset (grpset-to-cover gs) == gs
  grpset-to-cover-to-grpset gs =
    groupset=
      ribbon-a₁-to-El-equiv
      (λ {x₁}{x₂} x= → Trunc-elim λ g →
        ribbon-a₁-to-El (transport (Ribbon X gs) g x₁)
          =⟨ ap (λ x → ribbon-a₁-to-El (transport (Ribbon X gs) g x))
                $ ! $ <–-inv-l ribbon-a₁-to-El-equiv x₁ ⟩
        ribbon-a₁-to-El (transport (Ribbon X gs) g (trace (ribbon-a₁-to-El x₁) idp₀))
          =⟨ ap (λ x → ribbon-a₁-to-El (transport (Ribbon X gs) g (trace x idp₀))) x= ⟩
        ribbon-a₁-to-El (transport (Ribbon X gs) g (trace x₂ idp₀))
          =⟨ ap ribbon-a₁-to-El $ transp-trace g x₂ idp₀ ⟩
        GroupSet.act gs x₂ [ g ]
          ∎)

  -- Finally...
  grpset-equiv-cover : ∀ {j}
    → GroupSet (πS 0 X) (lmax i j) ≃ Cover A (lmax i j)
  grpset-equiv-cover {j} =
    grpset-to-cover , is-eq
      _
      (λ c → cover-to-grpset c)
      (λ c → cover-to-grpset-to-cover {lmax i j} c)
      (grpset-to-cover-to-grpset {lmax i j})

  -- The path-set cover is represented by the fundamental group itself
  path-set-repr-by-π1 : cover-to-grpset (path-set-cover X)
    == group-to-group-set (πS 0 X)
  path-set-repr-by-π1 = groupset= (ide _)
    (λ {x₁} p g → (transp₀-cst=₀idf g x₁ ∙ ∙₀'=∙₀ x₁ g) ∙' ap (_∙₀ g) p)