text:
module STLC2.Kovacs.Completeness where

open import STLC2.Kovacs.Normalisation public
open import STLC2.Kovacs.Convertibility public

-- TODO: Remove this
postulate
  █ : ∀ {ℓ} → {X : Set ℓ} → X

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

-- (_≈_)
mutual
  infix 3 _≫_
  _≫_ : ∀ {A Γ} → Γ ⊢ A → Γ ⊩ A → Set

  _≫_ {⎵}      {Γ} M N = M ∼ embⁿᶠ N

  _≫_ {A ⇒ B} {Γ} M f = ∀ {Γ′} → (η : Γ′ ⊇ Γ)
                                → {N : Γ′ ⊢ A} {∂a : Γ′ ∂⊩ A}
                                → N ∂≫ ∂a
                                → ren η M ∙ N ∂≫ f η ∂a

  _≫_ {A ⩕ B}  {Γ} M s = π₁ M ∂≫ proj₁ s × π₂ M ∂≫ proj₂ s

  _≫_ {⫪}     {Γ} M s = ⊤

  _≫_ {⫫}     {Γ} M s = ⊥

  _≫_ {A ⩖ B}  {Γ} M s = elim⊎ s (λ ∂a → Σ (Γ ⊢ A) (λ M₁ → M₁ ∂≫ ∂a))
                                 (λ ∂b → Σ (Γ ⊢ B) (λ M₂ → M₂ ∂≫ ∂b))

  infix 3 _∂≫_
  _∂≫_ : ∀ {Γ A} → Γ ⊢ A → Γ ∂⊩ A → Set

  _∂≫_ {Γ} {A} M ∂a
    = ∀ {Γ′ C} → (η : Γ′ ⊇ Γ)
               → {N : Γ′ ⊢ C}
               → {Nⁿᶠ : Γ′ ⊢ⁿᶠ C}
               → (f : ∀ {Γ″} → (η′ : Γ″ ⊇ Γ′)
                              → {a : Γ″ ⊩ A}
                              → ren (η ○ η′) M ≫ a
                              → ren η′ N ∼ embⁿᶠ (renⁿᶠ η′ Nⁿᶠ))
               → N ∼ embⁿᶠ Nⁿᶠ

-- (_≈ᶜ_)
infix 3 _∂≫⋆_
data _∂≫⋆_ : ∀ {Γ Ξ} → Γ ⊢⋆ Ξ → Γ ∂⊩⋆ Ξ → Set
  where
    ∅   : ∀ {Γ} → ∅ {Γ} ∂≫⋆ ∅

    _,_ : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ∂⊩⋆ Ξ}
                    → (χ : σ ∂≫⋆ ρ)
                    → {M : Γ ⊢ A} {∂a : Γ ∂⊩ A}
                    → (∂q : M ∂≫ ∂a)
                    → σ , M ∂≫⋆ ρ , ∂a

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

-- (_∼◾≈_)
mutual
  coe≫ : ∀ {A Γ} → {M₁ M₂ : Γ ⊢ A}
                 → M₁ ∼ M₂ → {a : Γ ⊩ A} → M₁ ≫ a
                 → M₂ ≫ a
  coe≫ {⎵}      p {N}      q = p ⁻¹ ⦙ q
  coe≫ {A ⇒ B} p {f}      g = λ η {N} {∂a} ∂q →
                                 ∂coe≫ {∂a = λ η′ f′ → f η ∂a η′ f′}
                                       (ren∼ η p ∙∼ (refl∼ {M = N}))
                                       (g η {N} {∂a} ∂q)
  coe≫ {A ⩕ B}  p {s}      q = ∂coe≫ {∂a = proj₁ s} (π₁∼ p) (proj₁ q) ,
                               ∂coe≫ {∂a = proj₂ s} (π₂∼ p) (proj₂ q)
  coe≫ {⫪}     p {s}      q = tt
  coe≫ {⫫}     p {s}      q = elim⊥ s
  coe≫ {A ⩖ B}  p {inj₁ a} q = q
  coe≫ {A ⩖ B}  p {inj₂ b} q = q

  ∂coe≫ : ∀ {A Γ} → {M₁ M₂ : Γ ⊢ A} {∂a : Γ ∂⊩ A}
                  → M₁ ∼ M₂ → M₁ ∂≫ ∂a
                  → M₂ ∂≫ ∂a

  ∂coe≫ p ∂q
    = λ η {N} {Nⁿᶠ} f →
        ∂q η {N} {Nⁿᶠ} (λ η′ {a} q →
          f η′ (coe≫ (ren∼ (η ○ η′) p)
                     q))

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

-- (≈ₑ)
mutual
  acc≫ : ∀ {A Γ Γ′} → (η : Γ′ ⊇ Γ)
                    → {M : Γ ⊢ A} {a : Γ ⊩ A}
                    → M ≫ a
                    → ren η M ≫ acc η a
  acc≫ {⎵}      η {M} {N}      p         = coe ((λ N′ → ren η M ∼ N′)
                                                & natembⁿᶠ η N ⁻¹)
                                               (ren∼ η p)
  acc≫ {A ⇒ B} η {M} {f}      g         η′ {N} {∂a}
                                         rewrite ren○ η′ η M ⁻¹
                                         = g (η ○ η′) {N} {∂a}
  acc≫ {A ⩕ B}  η {M} {s}      q         = ∂acc≫ η {π₁ M} {proj₁ s} (proj₁ q)
                                         , ∂acc≫ η {π₂ M} {proj₂ s} (proj₂ q)
  acc≫ {⫪}     η {M} {s}      q         = tt
  acc≫ {⫫}     η {M} {s}      q         = elim⊥ s
  acc≫ {A ⩖ B}  η {M} {inj₁ a} (M₁ , ∂a) = ren η M₁ , ∂acc≫ η {M₁} {a} ∂a
  acc≫ {A ⩖ B}  η {M} {inj₂ b} (M₂ , ∂b) = ren η M₂ , ∂acc≫ η {M₂} {b} ∂b

  ∂acc≫ : ∀ {A Γ Γ′} → (η : Γ′ ⊇ Γ)
                     → {M : Γ ⊢ A} {∂a : Γ ∂⊩ A}
                     → M ∂≫ ∂a
                     → ren η M ∂≫ ∂acc η ∂a

  ∂acc≫ η {M} ∂q
    = λ η′ {N} {Nⁿᶠ} f →
        ∂q (η ○ η′) {N} {Nⁿᶠ} (λ η″ q →
          f η″ (coe≫ (coe (_∼_ & ((λ η‴ → ren η‴ M) & assoc○ η″ η′ η ⁻¹)
                               ⊗ ren○ (η′ ○ η″) η M)
                          refl∼)
                     q))

-- (≈ᶜₑ)
-- NOTE: _⬖≫_ = ∂acc≫⋆
_⬖≫_ : ∀ {Γ Γ′ Ξ} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ∂⊩⋆ Ξ}
                  → (χ : σ ∂≫⋆ ρ) (η : Γ′ ⊇ Γ)
                  → σ ◐ η ∂≫⋆ ρ ⬖ η
∅                 ⬖≫ η = ∅
_,_ χ {M} {∂a} ∂q ⬖≫ η = χ ⬖≫ η , ∂acc≫ η {M} {∂a} ∂q

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

return≫ : ∀ {A Γ} → {M : Γ ⊢ A} {a : Γ ⊩ A}
                  → M ≫ a → M ∂≫ return a

return≫ {M = M} {a} q
  = λ η {N} {Nⁿᶠ} f →
      coe (_∼_ & idren N
               ⊗ embⁿᶠ & idrenⁿᶠ Nⁿᶠ)
          (f idₑ {acc η a}
                 (coe≫ (coe ((λ η′ → ren η M ∼ ren η′ M)
                             & (rid○ η ⁻¹))
                            refl∼)
                       (acc≫ η {M} {a} q)))

bind≫ : ∀ {A C Γ} → {M : Γ ⊢ A} {∂a : Γ ∂⊩ A}
                     {N : Γ ⊢ C} {∂c : Γ ∂⊩ C}
                  → M ∂≫ ∂a → (∀ {Γ′} → (η : Γ′ ⊇ Γ)
                                        → {a : Γ′ ⊩ A}
                                        → ren η M ≫ a
                                        → ren η N ∂≫ ∂acc η ∂c)
                  → N ∂≫ ∂c

bind≫ {M = M} {∂a} {N} {∂c} ∂q f
  = λ η {N′} {Nⁿᶠ′} f′ →
      ∂q η {N′} {Nⁿᶠ′} (λ η′ {a} q →
        f (η ○ η′) {a} q idₑ {ren η′ N′} {renⁿᶠ η′ Nⁿᶠ′} (λ η″ {c} q′ →
          coe (_∼_ & ren○ η″ η′ N′
                   ⊗ embⁿᶠ & renⁿᶠ○ η″ η′ Nⁿᶠ′)
              (f′ (η′ ○ η″) (coe≫ (coe (_∼_ & ren○ (idₑ ○ η″) (η ○ η′) N
                                            ⊗ (λ η‴ → ren η‴ N)
                                              & ( (λ η‴ → (η ○ η′) ○ η‴)
                                                  & lid○ η″
                                                ⦙ assoc○ η″ η′ η
                                                ))
                                       refl∼)
                                  q′))))

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

-- (∈≈)
get≫ : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ∂⊩⋆ Ξ}
                 → σ ∂≫⋆ ρ → (i : Ξ ∋ A)
                 → getₛ σ i ∂≫ getᵥ ρ i
get≫ (χ , p) zero    = p
get≫ (χ , p) (suc i) = get≫ χ i

-- (Tm≈)
eval≫ : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ∂⊩⋆ Ξ}
                 → σ ∂≫⋆ ρ → (M : Ξ ⊢ A)
                 → sub σ M ∂≫ eval ρ M

eval≫ {σ = σ} {ρ} χ (𝓋 i)
  = get≫ χ i

eval≫ {σ = σ} {ρ} χ (ƛ M)
  = return≫ {M = ƛ (sub (liftₛ σ) M)}
            {a = λ {Γ′} η ∂a → eval (ρ ⬖ η , ∂a) M}
            (λ {Γ′} η {N} {∂a} ∂q →
              ∂coe≫ {∂a = eval (ρ ⬖ η , ∂a) M}
                    (coe (((ƛ (ren (liftₑ η) (sub (liftₛ σ) M)) ∙ N) ∼_)
                          & ( sub◑ (idₛ , N) (liftₑ η) (sub (liftₛ σ) M) ⁻¹
                            ⦙ sub● (liftₑ η ◑ (idₛ , N)) (liftₛ σ) M ⁻¹
                            ⦙ (λ σ′ → sub (σ′ , N) M)
                              & ( comp●◑ (η ◑ idₛ , N) (wkₑ idₑ) σ
                                ⦙ (σ ●_) & lid◑ (η ◑ idₛ)
                                ⦙ comp●◑ idₛ η σ ⁻¹
                                ⦙ rid● (σ ◐ η)
                                )
                            ))
                         (red⇒ (ren (liftₑ η) (sub (liftₛ σ) M)) N) ⁻¹)
                    (eval≫ (_,_ (χ ⬖≫ η) {∂a = ∂a} (∂q)) M))

eval≫ {σ = σ} {ρ} χ (M ∙ N)
  = bind≫ {M  = sub σ M}
          {∂a = eval ρ M}
          {N  = sub σ M ∙ sub σ N}
          {∂c = eval ρ M ∂!∙ eval ρ N}
          (eval≫ χ M)
          (λ η {f} g →
            ∂coe≫ {∂a = eval (ρ ⬖ η) M ∂!∙ eval (ρ ⬖ η) N}
                  (coe (_∼_ & ((λ M′ → M′ ∙ ren η (sub σ N))
                               & ( (λ η′ → ren η′ (sub σ M))
                                   & (rid○ η ⁻¹)
                                 ⦙ ren○ idₑ η (sub σ M)
                                 ))
                            ⊗ refl)
                       refl∼)
                  (g idₑ {∂a = ∂acc η (eval ρ N)}
                         (∂coe≫ {∂a = eval (ρ ⬖ η) N}
                                (≡→∼ (sub◐ η σ N))
                                (eval≫ (χ ⬖≫ η) N))))

eval≫ {σ = σ} {ρ} χ (M , N)
  = return≫ {M = sub σ M , sub σ N}
            {a = eval ρ M , eval ρ N}
            ( ∂coe≫ {∂a = eval ρ M}
                    (red⩕₁ (sub σ M) (sub σ N) ⁻¹)
                    (eval≫ χ M)
            , ∂coe≫ {∂a = eval ρ N}
                    (red⩕₂ (sub σ M) (sub σ N) ⁻¹)
                    (eval≫ χ N)
            )

eval≫ {σ = σ} {ρ} χ (π₁ M)
  = bind≫ {M  = sub σ M}
          {∂a = eval ρ M}
          {N  = π₁ (sub σ M)}
          {∂c = ∂!π₁ (eval ρ M)}
          (eval≫ χ M)
          (λ η q → proj₁ q)

eval≫ {σ = σ} {ρ} χ (π₂ M)
  = bind≫ {M  = sub σ M}
          {∂a = eval ρ M}
          {N  = π₂ (sub σ M)}
          {∂c = ∂!π₂ (eval ρ M)}
          (eval≫ χ M)
          (λ η q → proj₂ q)

eval≫ {σ = σ} {ρ} χ τ
  = return≫ {M = τ} tt

eval≫ {σ = σ} {ρ} χ (φ M)
  = bind≫ {M  = sub σ M}
          {∂a = eval ρ M}
          {N  = φ (sub σ M)}
          {∂c = ∂!φ (eval ρ M)}
          (eval≫ χ M)
          (λ η q → elim⊥ q)

eval≫ {σ = σ} {ρ} χ (ι₁ M)
  = return≫ {M = ι₁ (sub σ M)}
            {a = inj₁ (eval ρ M)}
            (sub σ M , eval≫ χ M)

eval≫ {σ = σ} {ρ} χ (ι₂ M)
  = return≫ {M = ι₂ (sub σ M)}
            {a = inj₂ (eval ρ M)}
            (sub σ M , eval≫ χ M)

eval≫ {σ = σ} {ρ} χ (M ⁇ N₁ ∥ N₂)
  = bind≫ {M  = sub σ M}
          {∂a = eval ρ M}
          {N  = sub σ M ⁇ sub (liftₛ σ) N₁
                        ∥ sub (liftₛ σ) N₂}
          {∂c = eval ρ M ∂!⁇ (λ η ∂a → eval (ρ ⬖ η , ∂a) N₁)
                         ∂!∥ (λ η ∂b → eval (ρ ⬖ η , ∂b) N₂)}
          (eval≫ χ M)
          (λ { η {inj₁ ∂a} (M₁ , ∂q) →
                 λ η′ {N} {Nⁿᶠ} f →
                   ∂q η′ {N} {Nⁿᶠ} (λ η″ {a} q →
                     █)
             ; η {inj₂ ∂b} (M₂ , ∂q) →
                 λ η′ {N} {Nⁿᶠ} f →
                   ∂q η′ {N} {Nⁿᶠ} (λ η″ {a} q →
                     █)
             })

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

mutual
  -- (q≈)
  reify≫ : ∀ {A Γ} → {M : Γ ⊢ A} {a : Γ ∂⊩ A}
                   → (∂q : M ∂≫ a)
                   → M ∼ embⁿᶠ (reify a)

  reify≫ {⎵} {M = M} {∂a} ∂q
    = ∂q idₑ {M} {reify ∂a} (λ η {N} p →
        █)

  reify≫ {A ⇒ B} {M = M} {∂a} ∂q
    = ∂q idₑ {M} {reify ∂a} (λ η {f} g →
        █)

  reify≫ {A ⩕ B} {M = M} {∂a} ∂q
    = ∂q idₑ {M} {reify ∂a} (λ η {s} q →
        █)

  reify≫ {⫪} {M = M} {∂a} ∂q
    = ∂q idₑ {M} {reify ∂a} (λ η {s} q →
        coe ((λ M′ → ren η M ∼ M′)
             & natembⁿᶠ η (∂a idₑ (λ η′ s′ → τ)) ⁻¹)
            (ren∼ {M₁ = M}
                  {M₂ = embⁿᶠ (∂a idₑ (λ η′ s′ → τ))}
                  η
                  █))

  reify≫ {⫫} {M = M} {∂a} ∂q
    = ∂q idₑ {M} {reify ∂a} (λ η {s} q →
        █)

  reify≫ {A ⩖ B} {M = M} {∂a} ∂q
    = ∂q idₑ {M} {reify ∂a} (λ η {s} q →
        █)

  -- (u≈)
  reflect≫ : ∀ {A Γ} → (M : Γ ⊢ⁿᵉ A)
                     → embⁿᵉ M ∂≫ reflect M

  reflect≫ {⎵} M
    = return≫ {M = embⁿᵉ M}
              {a = ne M}
              refl∼

  reflect≫ {A ⇒ B} M
    = return≫ {M = embⁿᵉ M}
              {a = λ η ∂a → reflect (renⁿᵉ η M ∙ reify ∂a)}
              (λ η {N} {∂a} ∂q →
                ∂coe≫ {∂a = ∂acc η (reflect M) ∂!∙ ∂a}
                      (≡→∼ (natembⁿᵉ η M ⁻¹) ∙∼ reify≫ ∂q ⁻¹)
                      (reflect≫ (renⁿᵉ η M ∙ reify ∂a)))

  reflect≫ {A ⩕ B} M
    = return≫ {M = embⁿᵉ M}
              {a = reflect (π₁ M) , reflect (π₂ M)}
              (reflect≫ (π₁ M) , reflect≫ (π₂ M))

  reflect≫ {⫪} M
    = return≫ {M = embⁿᵉ M}
              {a = tt}
              tt

  reflect≫ {⫫} M
    = λ η {N} {Nⁿᶠ} f →
        coe (_∼_ & idren N
                 ⊗ embⁿᶠ & idrenⁿᶠ Nⁿᶠ)
            (f idₑ {█} █)

  reflect≫ {A ⩖ B} M
    = λ η {N} {Nⁿᶠ} f →
        coe (_∼_ & idren N
                 ⊗ embⁿᶠ & idrenⁿᶠ Nⁿᶠ)
            (f idₑ {█} █)

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

-- (uᶜ≈)
id≫⋆ : ∀ {Γ} → idₛ {Γ} ∂≫⋆ idᵥ
id≫⋆ {∅}     = ∅
id≫⋆ {Γ , A} = id≫⋆ ⬖≫ wkₑ idₑ , reflect≫ 0

complete : ∀ {Γ A} → (M : Γ ⊢ A)
                   → M ∼ embⁿᶠ (nf M)
complete M = coe ((_∼ embⁿᶠ (reify (eval idᵥ M))) & idsub M)
                 (reify≫ (eval≫ id≫⋆ M))

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
-- Andreas, 2010-09-24

module ParseForallAbsurd where

parseFails : forall () -> Set1
parseFails x = Set
-- this does no longer give the error message
-- "absurd lambda cannot have a body"

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Data.Unit
open import Data.Integer as ℤ using (ℤ)
open import Data.List
open import Data.List.Relation.Unary.All as List

module quantifierIn-output where

private
  VEHICLE_PROJECT_FILE = "TODO_projectFile"

emptyList : List ℤ
emptyList = []

abstract
  empty : List.All (λ (x : ℤ) → ⊤) emptyList
  empty = checkProperty record
    { projectFile  = VEHICLE_PROJECT_FILE
    ; propertyUUID = "TODO_propertyUUID"
    }

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: wenkokke/vehicle


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

open import lib.Base
open import lib.PathGroupoid
open import lib.Relation

module lib.NType where

module _ {i} where

  {- Definition of contractible types and truncation levels -}

  -- We define `has-level' as a record, so that it does not unfold when
  -- applied to (S n), in order for instance arguments to work correctly
  -- (idea by Dan Licata)
  record has-level (n : ℕ₋₂) (A : Type i) : Type i

  has-level-aux : ℕ₋₂ → (Type i → Type i)
  has-level-aux ⟨-2⟩ A = Σ A (λ x → ((y : A) → x == y))
  has-level-aux (S n) A = (x y : A) → has-level n (x == y)

  record has-level n A where
    -- Agda notices that the record is recursive, so we need to specify that we want eta-equality
    inductive
    eta-equality
    constructor has-level-in
    field
      has-level-apply : has-level-aux n A
  open has-level public

  instance
    has-level-apply-instance : {A : Type i} {n : ℕ₋₂} {x y : A} {{p : has-level (S n) A}} → has-level n (x == y)
    has-level-apply-instance {x = x} {y} {{p}} = has-level-apply p x y

  is-contr = has-level -2
  is-prop = has-level -1
  is-set  = has-level 0

  contr-center : {A : Type i} (p : is-contr A) → A
  contr-center p = fst (has-level-apply p)

  contr-path : {A : Type i} (p : is-contr A) (y : A) → contr-center p == y
  contr-path p y = snd (has-level-apply p) y

  prop-path : {A : Type i} (p : is-prop A) (x y : A) → x == y
  prop-path p x y = contr-center (has-level-apply p x y)

  {- To be a mere proposition, it is sufficient that all points are equal -}

  has-all-paths : Type i → Type i
  has-all-paths A = (x y : A) → x == y

  abstract
    all-paths-is-prop : {A : Type i} → (has-all-paths A → is-prop A)
    all-paths-is-prop {A} c = has-level-in (λ x y → has-level-in (c x y , canon-path)) where

      canon-path : {x y : A} (p : x == y) → c x y == p
      canon-path {.y} {y} idp =
        c y y               =⟨ lemma (! (c y y)) ⟩
        (! (c y y)) ∙ c y y =⟨ !-inv-l (c y y) ⟩
        idp =∎  where

        lemma : {x y : A} (p : x == y) → c x y == p ∙ c y y
        lemma idp = idp

  {- Truncation levels are cumulative -}
  raise-level : {A : Type i} (n : ℕ₋₂)
    → (has-level n A → has-level (S n) A)
  raise-level ⟨-2⟩ q =
    all-paths-is-prop (λ x y → ! (contr-path q x) ∙ contr-path q y)
  raise-level (S n) q =
    has-level-in (λ x y → raise-level n (has-level-apply q x y))

  {- Having decidable equality is stronger that being a set -}

  has-dec-onesided-eq : {A : Type i} → A → Type i
  has-dec-onesided-eq x = ∀ y → Dec (x == y)

  has-dec-eq : Type i → Type i
  has-dec-eq A = (x : A) → has-dec-onesided-eq x

  abstract
    -- XXX naming
    dec-onesided-eq-is-prop : {A : Type i} (x : A)
      → has-dec-onesided-eq x → (∀ y → is-prop (x == y))
    dec-onesided-eq-is-prop {A} x d y = all-paths-is-prop UIP where

      T : {y : A} → x == y → Type i
      T {y} p with d x | d y
      T {y} p | inr _  | _      = Lift ⊥
      T {y} p | inl _  | inr _  = Lift ⊥
      T {y} p | inl dx | inl dy = ! dx ∙ dy == p

      lemma : {y : A} → (p : x == y) → T p
      lemma idp with d x
      lemma idp | inl r  = !-inv-l r
      lemma idp | inr r⊥ = lift (r⊥ idp)

      UIP : {y : A} (p q : x == y) → p == q
      UIP idp q with d x | lemma q
      UIP idp q | inl r  | s = ! (!-inv-l r) ∙' s
      UIP idp q | inr r⊥ | _ = Empty-elim (r⊥ idp)

    dec-eq-is-set : {A : Type i} → has-dec-eq A → is-set A
    dec-eq-is-set d = has-level-in (λ x y → dec-onesided-eq-is-prop x (d x) y)

  {- Relationships between levels -}

  module _ {A : Type i} where
    abstract
      contr-has-all-paths : {{_ : is-contr A}} → has-all-paths A
      contr-has-all-paths {{c}} x y = ! (contr-path c x) ∙ contr-path c y

      prop-has-all-paths : {{_ : is-prop A}} → has-all-paths A
      prop-has-all-paths {{c}} x y = prop-path c x y

      inhab-prop-is-contr : A → {{_ : is-prop A}} → is-contr A
      inhab-prop-is-contr x₀ {{p}} = has-level-in (x₀ , λ y → prop-path p x₀ y)

      inhab-to-contr-is-prop : (A → is-contr A) → is-prop A
      inhab-to-contr-is-prop c = all-paths-is-prop $
        λ x y → ! (contr-path (c x) x) ∙ contr-path (c x) y

      inhab-to-prop-is-prop : (A → is-prop A) → is-prop A
      inhab-to-prop-is-prop c = has-level-in (λ x y → has-level-apply (c x) x y)

      contr-has-level : {n : ℕ₋₂} → (is-contr A → has-level n A)
      contr-has-level {n = ⟨-2⟩} p = p
      contr-has-level {n = S n} p = raise-level n (contr-has-level p)

      prop-has-level-S : {n : ℕ₋₂} → (is-prop A → has-level (S n) A)
      prop-has-level-S {n = ⟨-2⟩} p = p
      prop-has-level-S {n = S n} p = raise-level (S n) (prop-has-level-S p)

      set-has-level-SS : {n : ℕ₋₂} → (is-set A → has-level (S (S n)) A)
      set-has-level-SS {n = ⟨-2⟩} p = p
      set-has-level-SS {n = S n} p = raise-level (S (S n)) (set-has-level-SS p)

      contr-is-prop : is-contr A → is-prop A
      contr-is-prop = contr-has-level

      contr-is-set : is-contr A → is-set A
      contr-is-set = contr-has-level

      prop-is-set : is-prop A → is-set A
      prop-is-set = prop-has-level-S

      =-preserves-contr : {x y : A} → is-contr A → is-contr (x == y)
      =-preserves-contr p = has-level-in (contr-has-all-paths {{p}} _ _ , unique-path) where
          unique-path : {u v : A} (q : u == v)
            → contr-has-all-paths {{p}} u v == q
          unique-path idp = !-inv-l (contr-path p _)

    {- If [A] has level [n], then so does [x == y] for [x y : A] -}
    instance
      =-preserves-level : {n : ℕ₋₂} {x y : A}
        → has-level n A → has-level n (x == y)
      =-preserves-level {⟨-2⟩} = =-preserves-contr
      =-preserves-level {S n} {x} {y} p = raise-level n (has-level-apply p x y)

    {- The type of paths from a fixed point is contractible -}
    instance
      pathfrom-is-contr : (x : A) → is-contr (Σ A (λ t → x == t))
      pathfrom-is-contr x = has-level-in ((x , idp) , pathfrom-unique-path) where
        pathfrom-unique-path : {u : A} (pp : Σ A (λ t → u == t)) → (u , idp) == pp
        pathfrom-unique-path (u , idp) = idp

    {- The type of paths to a fixed point is contractible -}
    instance
      pathto-is-contr : (x : A) → is-contr (Σ A (λ t → t == x))
      pathto-is-contr x = has-level-in ((x , idp) , pathto-unique-path) where
        pathto-unique-path : {u : A} (pp : Σ A (λ t → t == u)) → (u , idp) == pp
        pathto-unique-path (u , idp) = idp

    {-
    If [B] is a fibration over a contractible type [A], then any point in any
    fiber of [B] gives a section
    -}
    contr-has-section : ∀ {j} {A : Type i} {B : A → Type j}
      → (is-contr A → (x : A) → (u : B x) → Π A B)
    contr-has-section {B = B} p x₀ y₀ t = transport B (! (contr-path p x₀) ∙ contr-path p t) y₀

{- Subtypes -}

-- TODO: replace them by records, with the second field an instance field

module _ {i} (A : Type i) where
  SubtypeProp : ∀ j → Type (lmax i (lsucc j))
  SubtypeProp j = Σ (A → Type j) (λ P → ∀ a → is-prop (P a))

module SubtypeProp {i j} {A : Type i} (P : SubtypeProp A j) where
  prop = fst P
  level = snd P

module _ {i j} {A : Type i} (P : SubtypeProp A j) where
  private
    module P = SubtypeProp P

  Subtype : Type (lmax i j)
  Subtype = Σ A P.prop

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import HoTT
open import cw.CW
open import cw.FinCW
open import cw.FinBoundary
open import cohomology.Theory

module cw.cohomology.cochainequiv.DualizedHigherBoundary (OT : OrdinaryTheory lzero)
  {n} (⊙fin-skel : ⊙FinSkeleton (S (S n))) where

open OrdinaryTheory OT

private
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel

  fin-skel₋₁ = AttachedFinSkeleton.skel fin-skel
  I₋₁ = AttachedFinSkeleton.numCells fin-skel₋₁

  module FAG   = FreeAbelianGroup (Fin I)
  module FAG₋₁ = FreeAbelianGroup (Fin I₋₁)

  open FAG   renaming (FreeAbGroup to G)   using ()
  open FAG₋₁ renaming (FreeAbGroup to G₋₁) using ()

abstract
  rephrase-dualized-higher-boundary-in-degree : ∀ (g : Fin I₋₁ → Group.El (C2 0)) <I
    → GroupIso.g (FAG.Freeness.extend-iso (C2-abgroup 0))
        (GroupIso.f (FAG₋₁.Freeness.extend-iso (C2-abgroup 0)) g ∘ᴳ fboundary-last fin-skel) <I
    == Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁))
  rephrase-dualized-higher-boundary-in-degree g <I =
    γ.f (GroupHom.f (fboundary-last fin-skel) (FAG.insert <I))
      =⟨ ap γ.f $ app= (is-equiv.g-f (snd (FAG.Freeness.extend-equiv G₋₁)) (fboundary'-last fin-skel)) <I ⟩
    γ.f (G₋₁.sum (λ <I₋₁ → G₋₁.exp (FAG₋₁.insert <I₋₁) (deg <I₋₁)))
      =⟨ γ.pres-sum (λ <I₋₁ → G₋₁.exp (FAG₋₁.insert <I₋₁) (deg <I₋₁)) ⟩
    C⁰2.sum (λ <I₋₁ → γ.f (G₋₁.exp (FAG₋₁.insert <I₋₁) (deg <I₋₁)))
      =⟨ ap C⁰2.sum (λ= $ λ <I₋₁ → γ.pres-exp (FAG₋₁.insert <I₋₁) (deg <I₋₁)) ⟩
    C⁰2.sum (λ <I₋₁ → C⁰2.exp (γ.f (FAG₋₁.insert <I₋₁)) (deg <I₋₁))
      =⟨ ap C⁰2.sum
          (λ= λ <I₋₁ → ap (λ g → C⁰2.exp g (deg <I₋₁)) $
            app= (is-equiv.g-f (snd (FAG₋₁.Freeness.extend-equiv C⁰2)) g) <I₋₁) ⟩
    C⁰2.sum (λ <I₋₁ → C⁰2.exp (g <I₋₁) (deg <I₋₁))
      =∎
    where
      deg : Fin I₋₁ → ℤ
      deg <I₋₁ = fdegree-last fin-skel <I <I₋₁
      C⁰2 : AbGroup lzero
      C⁰2 = C2-abgroup 0
      module C⁰2 = AbGroup C⁰2
      γ : G₋₁.grp →ᴳ C⁰2.grp
      γ = FAG₋₁.Freeness.extend C⁰2 g
      module γ = GroupHom γ

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import Common.Prelude

pattern [_] x = x ∷ []
pattern tail {x} xs = x ∷ xs

length : ∀ {A} → List A → Nat
length [] = 0
length [ _ ] = 1
length (tail [ _ ]) = 2
length (tail (tail xs)) = 2 + length xs

data Vec (A : Set) : Nat → Set where
  nil : Vec A 0
  cons : ∀ n → A → Vec A n → Vec A (suc n)

pattern _∷v_ {n} x xs = cons n x xs

map : ∀ {A B n} → (A → B) → Vec A n → Vec B n
map f nil = nil
map f (x ∷v xs) = f x ∷v map f xs

data SomeVec (A : Set) : Set where
  someVec : ∀ n → Vec A n → SomeVec A

pattern some {n} xs = someVec n xs

null : ∀ {A} → SomeVec A → Bool
null (some nil)      = true
null (some (_ ∷v _)) = false  -- check that the hidden arg can be instantiated to a dot pattern

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module hott.core.univalence  where

open import hott.core.universe
open import hott.functions
open import hott.core.equality
open import hott.core.sigma

-- The core idea of univalence is to "identify" isomorphic types as
-- equal. Of course the normal definition of isomorphism is that there
-- should be a map from A to B that is witnesses the equivalence of the
-- two type. This is captured by the following record.
record _≃_  {a b : Level}(A : Type a)(B : Type b) : Type (a ⊔ b) where

  constructor IdentifyTypesVia
  field
    equiv     : (A → B)  -- The equivalence
    left-inv  : (B → A)  -- its left inverse
    right-inv : (B → A)  -- and its right inverse

    -- The proofs of the fact that the left and right inverses are actually
    -- left and right inverses.
    left-inv∘equiv~idA  : left-inv ∘ equiv ~ id
    iso∘right-equiv~idB : equiv    ∘ right-inv ~ id

-- Of course a type should be equivalent to itself via identity.
A≃A : {ℓ : Level}{A : Type ℓ} → A ≃ A
A≃A {ℓ} {A} = IdentifyTypesVia id id id (λ _ →  refl) (λ _ → refl)

-- Equal types are equivalent.
≡→≃ : {ℓ : Level}{A B : Type ℓ} → A ≡ B → A ≃ B
≡→≃ refl = A≃A

-- For the converse we need the univalence. However Univalence says
-- something. Not only can we infer A ≡ B from A ≃ B via the postulate
-- ua, this map together with ≡→≃ gives an equivalence of types.
module Univalence {ℓ : Level}{A B : Type ℓ} where

  -- The main axiom is to identify A ≃ B with A ≡ B
  postulate ua : A ≃ B → A ≡ B

  -- Now we are ready for the univalence axiom.
  UnivalenceAxiom : (A ≃ B) ≃ (A ≡ B)
  UnivalenceAxiom = IdentifyTypesVia ua ≡→≃ ≡→≃ linv-prf rinv-prf
    where postulate rinv-prf :  ua ∘ ≡→≃ ~ id
          postulate linv-prf :  ≡→≃ ∘ ua ~ id

  -- The next function helps in clean use of the univalence
  -- axioms in equational reasoning.
  --
  --
  -- begin ...
  --       ≡    B by univalence
  --       ...
  --
  -- provided an appropriate instance of A ≃ B is available in the
  -- vicinity.
  --
  univalence : ⦃ a≃b : A ≃ B ⦄ → A ≡ B
  univalence ⦃ a≃b ⦄ = ua a≃b

open Univalence public

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
-- The category Ab of abelian groups
{-# OPTIONS --safe #-}

module Cubical.Categories.Instances.AbGroups where

open import Cubical.Algebra.AbGroup.Base
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Categories.Category.Base
open import Cubical.Foundations.Prelude

module _ {ℓ : Level} where
  open Category

  AbGroupCategory : Category (ℓ-suc ℓ) ℓ
  AbGroupCategory .ob = AbGroup ℓ
  AbGroupCategory .Hom[_,_] = AbGroupHom
  AbGroupCategory .id = idGroupHom
  AbGroupCategory ._⋆_ = compGroupHom
  AbGroupCategory .⋆IdL f = GroupHom≡ refl
  AbGroupCategory .⋆IdR f = GroupHom≡ refl
  AbGroupCategory .⋆Assoc f g h = GroupHom≡ refl
  AbGroupCategory .isSetHom = isSetGroupHom

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------
-- A total parser combinator library
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

module TotalParserCombinators where

-- Check out TotalRecognisers for an introduction to the ideas used
-- below in the simplified setting of recognisers (as opposed to
-- parsers).

import TotalRecognisers

-- The parser type, and its semantics.

import TotalParserCombinators.Parser
import TotalParserCombinators.Semantics

-- Forcing of parsers (can be used for inspection/debugging purposes).

import TotalParserCombinators.Force

-- Some lemmas about initial bags.

import TotalParserCombinators.InitialBag

-- A small library of derived parser combinators.

import TotalParserCombinators.Lib

-- A Brzozowski derivative operator for parsers.

import TotalParserCombinators.Derivative

-- A breadth-first backend, based on the derivative operator.

import TotalParserCombinators.BreadthFirst

-- An alternative, coinductive definition of equality (and related
-- orderings) between parsers.

import TotalParserCombinators.CoinductiveEquality

-- Language equivalence and parser equivalence are both congruences.
-- The various orderings are compatible preorders.

import TotalParserCombinators.Congruence
import TotalParserCombinators.Congruence.Sound

-- However, it is possible to construct combinators which do not
-- preserve equality.

import TotalParserCombinators.NotACongruence

-- Proofs of various laws, for instance the monad laws.

import TotalParserCombinators.Laws

-- A proof showing that all functions of type List Bool → List R can
-- be realised using parser combinators (for any R, assuming that bag
-- equality is used for the lists of results).

import TotalParserCombinators.ExpressiveStrength

-- Definitions of asymmetric choice, and and not. Note that no
-- extension of the library is required to define these combinators,
-- which make use of a general operator which lifts initial bag
-- operations to parsers. This operator is defined using the
-- breadth-first backend's derivative operator.

import TotalParserCombinators.Pointwise
import TotalParserCombinators.AsymmetricChoice
import TotalParserCombinators.And
import TotalParserCombinators.Not

-- A lookahead operator cannot be defined.

import TotalParserCombinators.NoLookahead

-- An alternative semantics.

import TotalParserCombinators.Semantics.Continuation

-- Simplification of parsers.

import TotalParserCombinators.Simplification

-- Definition of unambiguity.

import TotalParserCombinators.Unambiguity

-- An example: a left recursive expression grammar.

import TotalParserCombinators.Examples.Expression

-- Recognisers defined on top of the parsers, and a variant of the
-- left recursive expression grammar mentioned above.

import TotalParserCombinators.Recogniser
import TotalParserCombinators.Recogniser.Expression

-- Another example: parsing PBM image files.

import TotalParserCombinators.Examples.PBM

-- An extended example: mixfix operator parsing.

import Mixfix

-- For code related to the paper "Structurally Recursive Descent
-- Parsing", developed together with Ulf Norell, see the following
-- module:

import StructurallyRecursiveDescentParsing

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{- Reported by Nils Anders Danielsson, 2011-07-06

From the release notes for Agda 2.2.10:

  "Projections now preserve sizes, both in patterns and expressions."

However, the following code is rejected:
-}

module SubTermAndProjections where

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

open _×_

postulate
 i : {A : Set} → A → A

data I : Set where
  c1 : I → I
  c2 : I → I → I

data D : I → Set where
  d : (j : I × I)  → D (c1 (proj₁ j)) → D (proj₂ j) → D (c2 (c1 (proj₁ j)) (proj₂ j))

f : ∀ i → D i → Set
f .(c2 (c1 (proj₁ j)) (proj₂ j)) (d j l r) = f (c1 (proj₁ j)) (i l)

{- Is this intentional? I guess the issue here is the subterm relation
rather than the sizes. Should we modify the subterm relation?
-}
-- Andreas, 2011-07-07 this should termination check.


text:
open import Agda.Primitive using (_⊔_)
open import Categories.Category
open import Categories.Functor
open import Categories.Monad.Relative

module SecondOrder.RelativeKleisli
         {o l e o' l' e'}
         {𝒞 : Category o l e}
         {𝒟 : Category o' l' e'}
         {J : Functor 𝒞 𝒟}
         (M : Monad J)
       where

  Kleisli : Category o l' e'
  Kleisli =
    let open Category in
    let open Functor in
    record
      { Obj = Obj 𝒞
      ; _⇒_ = λ A B →  𝒟 [ F₀ J A , Monad.F₀ M B ]
      ; _≈_ = _≈_ 𝒟
      ; id = Monad.unit M
      ; _∘_ = λ f g → _∘_ 𝒟 (Monad.extend M f) g
      ; assoc = λ {A} {B} {C} {D} {f} {g} {h}
                → Equiv.trans 𝒟 (∘-resp-≈ˡ 𝒟 (Monad.assoc M)) (assoc 𝒟)
      ; sym-assoc = λ {A} {B} {C} {D} {f} {g} {h}
                    → Equiv.sym 𝒟 (Equiv.trans 𝒟 (∘-resp-≈ˡ 𝒟 (Monad.assoc M)) (assoc 𝒟))
      ; identityˡ = λ {A} {B} {f}
                    → Equiv.trans 𝒟 (∘-resp-≈ˡ 𝒟 (Monad.identityˡ M)) (identityˡ 𝒟)
      ; identityʳ = λ {A} {B} {f}
                    → Monad.identityʳ M
      ; identity² = λ {A} → Equiv.trans 𝒟 ((∘-resp-≈ˡ 𝒟 (Monad.identityˡ M))) (identityˡ 𝒟)
      ; equiv = equiv 𝒟
      ; ∘-resp-≈ = λ p₁ p₂ → ∘-resp-≈ 𝒟 (Monad.extend-≈ M p₁) p₂
      }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module TakeDropDec where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List using (List; []; _∷_)
open import Data.List.All using (All; []; _∷_)
open import Data.Bool using (Bool; true; false; T)
open import Data.Unit using (⊤; tt)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using ()
open import Function using (_∘_)

module TakeDrop {A : Set} {P : A → Set} (P? : ∀ (x : A) → Dec (P x)) where

  takeWhile : List A → List A
  takeWhile []                   =  []
  takeWhile (x ∷ xs) with P? x
  ...                   | yes _  =  x ∷ takeWhile xs
  ...                   | no  _  =  []

  dropWhile : List A → List A
  dropWhile []                   =  []
  dropWhile (x ∷ xs) with P? x
  ...                   | yes _  =  dropWhile xs
  ...                   | no  _  =  x ∷ xs

  Head : (A → Set) → List A → Set
  Head P []        =  ⊥
  Head P (x ∷ xs)  =  P x

  takeWhile-lemma : ∀ (xs : List A) → All P (takeWhile xs)
  takeWhile-lemma []                    =  []
  takeWhile-lemma (x ∷ xs) with P? x
  ...                         | yes px  =  px ∷ takeWhile-lemma xs
  ...                         | no  _   =  []

  dropWhile-lemma : ∀ (xs : List A) → ¬ Head P (dropWhile xs)
  dropWhile-lemma []                     =  λ()
  dropWhile-lemma (x ∷ xs) with P? x
  ...                         | yes _    =  dropWhile-lemma xs
  ...                         | no  ¬px  =  ¬px

open TakeDrop
open import Data.Nat using (ℕ; zero; suc; _≟_)

_ : takeWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (0 ∷ 0 ∷ [])
_ = refl

_ : dropWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (1 ∷ [])
_ = refl


text:
module PLRTree.Compound {A : Set}  where

open import PLRTree {A}

data Compound : PLRTree → Set where
  compound : {t : Tag}{x : A}{l r : PLRTree} → Compound (node t x l r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Class.Monoid where

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

record Monoid {a} (M : Set a) : Set (suc a) where
  infixl 6 _+_
  field
    mzero : M
    _+_ : M -> M -> M

open Monoid {{...}} public

concat : ∀ {a} {M : Set a} {{_ : Monoid M}} -> List M -> M
concat [] = mzero
concat (x ∷ l) = x + concat l

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
module Oscar.Data.Nat where

open import Agda.Builtin.Nat public using (Nat; zero; suc)


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

open import Categories.Category

module Categories.Category.Slice.Properties {o ℓ e} (C : Category o ℓ e) where

open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.Functor
open import Categories.Object.Product
open import Categories.Diagram.Pullback
open import Categories.Morphism.Reasoning C
open import Categories.Object.Terminal C
import Categories.Category.Slice as S

private
  module C = Category C

module _ {A : C.Obj} where
  open S C
  open Category (Slice A)
  open SliceObj
  open Slice⇒
  open C.HomReasoning

  product⇒pullback : ∀ {X Y : Obj} → Product (Slice A) X Y → Pullback C (arr X) (arr Y)
  product⇒pullback p = record
    { p₁              = h π₁
    ; p₂              = h π₂
    ; commute         = △ π₁ ○ ⟺ (△ π₂)
    ; universal       = λ eq → h ⟨ slicearr eq , slicearr refl ⟩
    ; unique          = λ {_ _ _ _ eq} eq′ eq″ → ⟺ (unique {h = slicearr (pushˡ (⟺ (△ π₁)) ○ C.∘-resp-≈ʳ eq′ ○ eq)} eq′ eq″)
    ; p₁∘universal≈h₁ = project₁
    ; p₂∘universal≈h₂ = project₂
    }
    where open Product (Slice A) p

  pullback⇒product : ∀ {X Y : Obj} → Pullback C (arr X) (arr Y) → Product (Slice A) X Y
  pullback⇒product {X} {Y} p = record
    { A×B      = sliceobj (arr Y C.∘ p₂)
    ; π₁       = slicearr commute
    ; π₂       = slicearr refl
    ; ⟨_,_⟩    = λ f g → slicearr (pullʳ (p₂∘universal≈h₂ {eq = △ f ○ ⟺ (△ g)}) ○ △ g)
    ; project₁ = p₁∘universal≈h₁
    ; project₂ = p₂∘universal≈h₂
    ; unique   = λ eq eq′ → ⟺ (unique eq eq′)
    }
    where open Pullback p

module _ (t : Terminal) where
  open S C
  open Terminal t
  open Category (Slice ⊤)
  open SliceObj
  open Slice⇒
  open C.HomReasoning

  lift : ∀ {A B : C.Obj} (f : A C.⇒ B) → Slice⇒ (sliceobj (! {A})) (sliceobj (! {B}))
  lift f = slicearr {h = f} !-unique₂

  pullback⇒product′ : ∀ {X Y : Obj} → Pullback C (arr X) (arr Y) → Product (Slice ⊤) X Y
  pullback⇒product′ {X} {Y} p = record
    { A×B      = sliceobj !
    ; π₁       = slicearr {h = p₁} !-unique₂
    ; π₂       = slicearr {h = p₂} !-unique₂
    ; ⟨_,_⟩    = λ f g → slicearr {h = universal (△ f ○ ⟺ (△ g))} !-unique₂
    ; project₁ = p₁∘universal≈h₁
    ; project₂ = p₂∘universal≈h₂
    ; unique   = λ eq eq′ → ⟺ (unique eq eq′)
    }
    where open Pullback p

-- slice of slice
module _ {A B} (f : A C.⇒ B) where
  private
    C/B : Category _ _ _
    C/B = S.Slice C B
    module C/B = Category C/B

    C/A : Category _ _ _
    C/A = S.Slice C A
    module C/A = Category C/A

    open C.HomReasoning

  slice-slice⇒slice : Functor (S.Slice C/B (S.sliceobj f)) C/A
  slice-slice⇒slice = record
    { F₀           = λ { (S.sliceobj (S.slicearr {h} △)) → S.sliceobj h }
    ; F₁           = λ { (S.slicearr △) → S.slicearr △ }
    ; identity     = refl
    ; homomorphism = refl
    ; F-resp-≈     = λ eq → eq
    }

  slice⇒slice-slice : Functor C/A (S.Slice C/B (S.sliceobj f))
  slice⇒slice-slice = record
    { F₀           = λ { (S.sliceobj arr) → S.sliceobj (S.slicearr {h = arr} refl) }
    ; F₁           = λ { (S.slicearr △) → S.slicearr {h = S.slicearr (pullʳ △)} △ }
    ; identity     = refl
    ; homomorphism = refl
    ; F-resp-≈     = λ eq → eq
    }

  slice-slice≃slice : StrongEquivalence C/A (S.Slice C/B (S.sliceobj f))
  slice-slice≃slice = record
    { F            = slice⇒slice-slice
    ; G            = slice-slice⇒slice
    ; weak-inverse = record
      { F∘G≈id = record
        { F⇒G = record
          { η           = λ { (S.sliceobj (S.slicearr △)) → S.slicearr {h = S.slicearr (C.identityʳ ○ ⟺ △)} C.identityʳ }
          ; commute     = λ _ → id-comm-sym
          ; sym-commute = λ _ → id-comm
          }
        ; F⇐G           = record
          { η           = λ { (S.sliceobj (S.slicearr △)) → S.slicearr {h = S.slicearr (C.identityʳ ○ △)} C.identityʳ }
          ; commute     = λ _ → id-comm-sym
          ; sym-commute = λ _ → id-comm
          }
        ; iso = λ _ → record
          { isoˡ = C.identity²
          ; isoʳ = C.identity²
          }
        }
      ; G∘F≈id = record
        { F⇒G = record
          { η           = λ { (S.sliceobj arr) → S.slicearr C.identityʳ }
          ; commute     = λ _ → id-comm-sym
          ; sym-commute = λ _ → id-comm
          }
        ; F⇐G           = record
          { η           = λ { (S.sliceobj arr) → S.slicearr C.identityʳ }
          ; commute     = λ _ → id-comm-sym
          ; sym-commute = λ _ → id-comm
          }
        ; iso = λ _ → record
          { isoˡ = C.identity²
          ; isoʳ = C.identity²
          }
        }
      }
    }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Generic.Lib.Prelude where

open import Generic.Lib.Intro                  public
open import Generic.Lib.Equality.Propositional public
open import Generic.Lib.Equality.Coerce        public
open import Generic.Lib.Equality.Heteroindexed public
open import Generic.Lib.Equality.Congn         public
open import Generic.Lib.Decidable              public
open import Generic.Lib.Category               public
open import Generic.Lib.Data.Nat               public
open import Generic.Lib.Data.String            public
open import Generic.Lib.Data.Maybe             public
open import Generic.Lib.Data.Sum               public
open import Generic.Lib.Data.Product           public
open import Generic.Lib.Data.List              public
open import Generic.Lib.Data.Pow               public
open import Generic.Lib.Data.Sets              public
open import Generic.Lib.Reflection.Core        public
open import Generic.Lib.Reflection.Fold        public

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the pointwise lifting of a predicate to a binary tree
------------------------------------------------------------------------

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

module Data.Tree.Binary.Relation.Unary.All.Properties where

open import Level
open import Data.Tree.Binary as Tree using (Tree; leaf; node)
open import Data.Tree.Binary.Relation.Unary.All
open import Relation.Unary

private
  variable
    a b p q : Level
    A : Set a
    B : Set b

module _ {P : B → Set p} where

  map⁺ : (f : A → B) → ∀[ All (f ⊢ P) ⇒ Tree.map f ⊢ All P ]
  map⁺ f leaf         = leaf
  map⁺ f (node l m r) = node (map⁺ f l) m (map⁺ f r)


text:
{-# OPTIONS --guarded #-}
module _ where

primitive
  primLockUniv : _

postulate
  A B : primLockUniv
  c : A → B
  foo : (@tick x y : B) → Set

bar : (@tick x y : A) → Set
bar x y = foo (c x) (c y)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Core definition of divisibility
------------------------------------------------------------------------

-- The definition of divisibility is split out from
-- `Data.Nat.Divisibility` to avoid a dependency cycle with
-- `Data.Nat.DivMod`.

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

module Data.Nat.Divisibility.Core where

open import Data.Nat.Base using (ℕ; _*_)
open import Data.Nat.Properties
open import Level using (0ℓ)
open import Relation.Nullary using (¬_)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym)

------------------------------------------------------------------------
-- Definition
--
-- m ∣ n is inhabited iff m divides n. Some sources, like Hardy and
-- Wright's "An Introduction to the Theory of Numbers", require m to
-- be non-zero. However, some things become a bit nicer if m is
-- allowed to be zero. For instance, _∣_ becomes a partial order, and
-- the gcd of 0 and 0 becomes defined.

infix 4 _∣_ _∤_

record _∣_ (m n : ℕ) : Set where
  constructor divides
  field quotient : ℕ
        equality : n ≡ quotient * m
open _∣_ using (quotient) public

_∤_ : Rel ℕ 0ℓ
m ∤ n = ¬ (m ∣ n)


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

-- We do not parameterize this module since we do not have access to _+_ or _*_
-- for the fields that we want (real numbers)
open import Level using (Level)

open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open ≡-Reasoning

open import Data.Nat using (ℕ) renaming (_+_ to _+ᴺ_)
open import Data.Nat.Properties
open import Data.Vec using (Vec; []; _∷_; _++_; take; drop; map; replicate)
open import Data.Vec.Properties

open import Function using (id)

open import FLA.Algebra.Structures
open import FLA.Algebra.Properties.Field
open import FLA.Algebra.LinearAlgebra
open import FLA.Algebra.LinearAlgebra.Properties

module FLA.Algebra.LinearMap where

private
  variable
    ℓ : Level
    A : Set ℓ
    m n p q : ℕ

-- A linear map from one vector field to another
record _⊸_ {ℓ : Level} {A : Set ℓ} ⦃ F : Field A ⦄ (m n : ℕ) : Set ℓ where
  field
    f : (Vec A m → Vec A n)

    -- Additivity
    f[u+v]≡f[u]+f[v] : (u v : Vec A m) → f (u +ⱽ v) ≡ f u +ⱽ f v

    -- Homogeneity
    f[c*v]≡c*f[v] : (c : A) → (v : Vec A m) → f (c ∘ⱽ v) ≡ c ∘ⱽ (f v)

infixr 1 _⊸_

-- A convenient syntax if a particular set needs to be specified.
_—_⊸_ : {ℓ : Level} (m : ℕ) (A : Set ℓ) (n : ℕ) ⦃ F : Field A ⦄ → Set ℓ
m — A ⊸ n  = _⊸_ {A = A} m n
infixr 1 _—_⊸_

module _ ⦃ F : Field A ⦄ where
  open Field F
  open _⊸_

  _·ˡᵐ_ : m ⊸ n → Vec A m → Vec A n
  _·ˡᵐ_ LM = f LM

  private
    +ˡᵐ-linearity : (g h : m ⊸ n) → (u v x y : Vec A m)
                  → g ·ˡᵐ (u +ⱽ v) +ⱽ h ·ˡᵐ (x +ⱽ y) ≡
                     g ·ˡᵐ u +ⱽ h ·ˡᵐ x +ⱽ (g ·ˡᵐ v +ⱽ h ·ˡᵐ y)
    +ˡᵐ-linearity g h u v x y rewrite
        f[u+v]≡f[u]+f[v] g u v
      | f[u+v]≡f[u]+f[v] h x y
      | (+ⱽ-assoc (g ·ˡᵐ u) (g ·ˡᵐ v) (h ·ˡᵐ x +ⱽ h ·ˡᵐ y))
      | sym (+ⱽ-assoc (g ·ˡᵐ v) (h ·ˡᵐ x) (h ·ˡᵐ y))
      | +ⱽ-comm (g ·ˡᵐ v) (h ·ˡᵐ x)
      | (+ⱽ-assoc (h ·ˡᵐ x) (g ·ˡᵐ v) (h ·ˡᵐ y))
      | sym (+ⱽ-assoc (g ·ˡᵐ u) (h ·ˡᵐ x) (g ·ˡᵐ v +ⱽ h ·ˡᵐ y))
      = refl

    +-homogeneity : (g h : m ⊸ n) → (c : A) (u v : Vec A m)
                  → g ·ˡᵐ (c ∘ⱽ u) +ⱽ h ·ˡᵐ (c ∘ⱽ v) ≡
                     c ∘ⱽ (g ·ˡᵐ u +ⱽ h ·ˡᵐ v)
    +-homogeneity g h c u v rewrite
          f[c*v]≡c*f[v] g c u
        | f[c*v]≡c*f[v] h c v
        | sym (∘ⱽ-distr-+ⱽ c (g ·ˡᵐ u) (h ·ˡᵐ v))
        = refl

  _+ˡᵐ_ : m ⊸ n → m ⊸ n → m ⊸ n
  g +ˡᵐ h = record
    { f = λ v → g ·ˡᵐ v +ⱽ h ·ˡᵐ v
    ; f[u+v]≡f[u]+f[v] = λ u v → +ˡᵐ-linearity g h u v u v
    ; f[c*v]≡c*f[v] = λ c v → +-homogeneity g h c v v
    }

  _-ˡᵐ_ : m ⊸ n → m ⊸ n → m ⊸ n
  g -ˡᵐ h = record
    { f = λ v → g ·ˡᵐ v -ⱽ h ·ˡᵐ v
    ; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]' g h
    ; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]' g h
    }
    where
      f[u+v]≡f[u]+f[v]' : (g h : m ⊸ n) → (u v : Vec A m)
                        → g ·ˡᵐ (u +ⱽ v) -ⱽ h ·ˡᵐ (u +ⱽ v) ≡
                           g ·ˡᵐ u -ⱽ h ·ˡᵐ u +ⱽ (g ·ˡᵐ v -ⱽ h ·ˡᵐ v)
      f[u+v]≡f[u]+f[v]' g h u v = begin
          g ·ˡᵐ (u +ⱽ v) -ⱽ h ·ˡᵐ (u +ⱽ v)
        ≡⟨ cong (g ·ˡᵐ (u +ⱽ v) +ⱽ_) (-ⱽ≡-1ᶠ∘ⱽ (h ·ˡᵐ (u +ⱽ v))) ⟩
          g ·ˡᵐ (u +ⱽ v) +ⱽ (- 1ᶠ) ∘ⱽ (h ·ˡᵐ (u +ⱽ v))
        ≡⟨ cong (λ x → g ·ˡᵐ (u +ⱽ v) +ⱽ (- 1ᶠ) ∘ⱽ x) (f[u+v]≡f[u]+f[v] h u v) ⟩
          g ·ˡᵐ (u +ⱽ v) +ⱽ (- 1ᶠ) ∘ⱽ (h ·ˡᵐ u +ⱽ h ·ˡᵐ v)
        ≡⟨ cong (g ·ˡᵐ (u +ⱽ v) +ⱽ_) (∘ⱽ-distr-+ⱽ (- 1ᶠ) (h ·ˡᵐ u) (h ·ˡᵐ v)) ⟩
          g ·ˡᵐ (u +ⱽ v) +ⱽ ((- 1ᶠ) ∘ⱽ h ·ˡᵐ u +ⱽ (- 1ᶠ) ∘ⱽ h ·ˡᵐ v)
        ≡⟨ cong₂ (λ x y → g ·ˡᵐ (u +ⱽ v) +ⱽ (x +ⱽ y))
                 (sym (f[c*v]≡c*f[v] h (- 1ᶠ) u))
                 (sym (f[c*v]≡c*f[v] h (- 1ᶠ) v)) ⟩
          g ·ˡᵐ (u +ⱽ v) +ⱽ (h ·ˡᵐ ((- 1ᶠ) ∘ⱽ u) +ⱽ h ·ˡᵐ ((- 1ᶠ) ∘ⱽ v))
        ≡⟨ cong (g ·ˡᵐ (u +ⱽ v) +ⱽ_)
                (sym (f[u+v]≡f[u]+f[v] h ((- 1ᶠ) ∘ⱽ u) ((- 1ᶠ) ∘ⱽ v))) ⟩
          g ·ˡᵐ (u +ⱽ v) +ⱽ (h ·ˡᵐ ((- 1ᶠ) ∘ⱽ u +ⱽ (- 1ᶠ) ∘ⱽ v))
        ≡⟨ +ˡᵐ-linearity g h u v ((- 1ᶠ) ∘ⱽ u) ((- 1ᶠ) ∘ⱽ v) ⟩
          g ·ˡᵐ u +ⱽ h ·ˡᵐ ((- 1ᶠ) ∘ⱽ u) +ⱽ (g ·ˡᵐ v +ⱽ h ·ˡᵐ ((- 1ᶠ) ∘ⱽ v))
        ≡⟨ cong₂ (λ x y → g ·ˡᵐ u +ⱽ x +ⱽ (g ·ˡᵐ v +ⱽ y))
          (trans (f[c*v]≡c*f[v] h ((- 1ᶠ)) u) (sym (-ⱽ≡-1ᶠ∘ⱽ (h ·ˡᵐ u))))
          (trans (f[c*v]≡c*f[v] h ((- 1ᶠ)) v) (sym (-ⱽ≡-1ᶠ∘ⱽ (h ·ˡᵐ v)))) ⟩
          g ·ˡᵐ u -ⱽ h ·ˡᵐ u +ⱽ (g ·ˡᵐ v -ⱽ h ·ˡᵐ v)
        ∎

      f[c*v]≡c*f[v]' : (g h : m ⊸ n) → (c : A) (v : Vec A m)
                     → g ·ˡᵐ (c ∘ⱽ v) -ⱽ h ·ˡᵐ (c ∘ⱽ v) ≡
                        c ∘ⱽ (g ·ˡᵐ v -ⱽ h ·ˡᵐ v)
      f[c*v]≡c*f[v]' g h c v = begin
          g ·ˡᵐ (c ∘ⱽ v) -ⱽ h ·ˡᵐ (c ∘ⱽ v)
        ≡⟨ cong (g ·ˡᵐ (c ∘ⱽ v) +ⱽ_)
          (trans (-ⱽ≡-1ᶠ∘ⱽ (h ·ˡᵐ (c ∘ⱽ v)))
                 (sym (f[c*v]≡c*f[v] h (- 1ᶠ) (c ∘ⱽ v)))) ⟩
          g ·ˡᵐ (c ∘ⱽ v) +ⱽ h ·ˡᵐ ((- 1ᶠ) ∘ⱽ (c ∘ⱽ v))
        ≡⟨ cong (λ x → g ·ˡᵐ (c ∘ⱽ v) +ⱽ h ·ˡᵐ x) (∘ⱽ-comm (- 1ᶠ) c v) ⟩
          g ·ˡᵐ (c ∘ⱽ v) +ⱽ h ·ˡᵐ (c ∘ⱽ ((- 1ᶠ) ∘ⱽ v))
        ≡⟨ +-homogeneity g h c v ((- 1ᶠ) ∘ⱽ v) ⟩
          c ∘ⱽ (g ·ˡᵐ v +ⱽ h ·ˡᵐ ((- 1ᶠ) ∘ⱽ v))
        ≡⟨ cong (λ x → c ∘ⱽ (g ·ˡᵐ v +ⱽ x))
                (trans (f[c*v]≡c*f[v] h (- 1ᶠ) v) (sym (-ⱽ≡-1ᶠ∘ⱽ (h ·ˡᵐ v)))) ⟩
          c ∘ⱽ (g ·ˡᵐ v -ⱽ h ·ˡᵐ v)
        ∎

  _*ˡᵐ_ : n ⊸ p → m ⊸ n → m ⊸ p
  g *ˡᵐ h = record
    { f = λ v → g ·ˡᵐ (h ·ˡᵐ v)
    ; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]' g h
    ; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]' g h
    }
    where
      f[u+v]≡f[u]+f[v]' : (g : n ⊸ p) (h : m ⊸ n)
                        → (u v : Vec A m)
                        → g ·ˡᵐ (h ·ˡᵐ (u +ⱽ v)) ≡
                           g ·ˡᵐ (h ·ˡᵐ u) +ⱽ g ·ˡᵐ (h ·ˡᵐ v)
      f[u+v]≡f[u]+f[v]' g h u v rewrite
          f[u+v]≡f[u]+f[v] h u v
        | f[u+v]≡f[u]+f[v] g (f h u) (f h v)
        = refl

      f[c*v]≡c*f[v]' : (g : n ⊸ p) (h : m ⊸ n)
                     → (c : A) (v : Vec A m)
                     → g ·ˡᵐ (h ·ˡᵐ (c ∘ⱽ v)) ≡ c ∘ⱽ g ·ˡᵐ (h ·ˡᵐ v)
      f[c*v]≡c*f[v]' g h c v rewrite
          f[c*v]≡c*f[v] h c v
        | f[c*v]≡c*f[v] g c (h ·ˡᵐ v)
        = refl

  -- vertical stack forward operator
  _—ˡᵐ_ : p ⊸ m → p ⊸ n → p ⊸ (m +ᴺ n)
  T —ˡᵐ B =
    record
      { f = λ v →  T ·ˡᵐ v ++ B ·ˡᵐ v
      ; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]' T B
      ; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]' T B
      }
    where
      f[u+v]≡f[u]+f[v]' : (T : p ⊸ m) (B : p ⊸ n)
                        → (u v : Vec A p)
                        → T ·ˡᵐ (u +ⱽ v) ++ B ·ˡᵐ (u +ⱽ v) ≡
                          (T ·ˡᵐ u ++ B ·ˡᵐ u) +ⱽ (T ·ˡᵐ v ++ B ·ˡᵐ v)
      f[u+v]≡f[u]+f[v]' T B u v rewrite
          f[u+v]≡f[u]+f[v] T u v
        | f[u+v]≡f[u]+f[v] B u v
        | +ⱽ-flip-++ (T ·ˡᵐ u) (T ·ˡᵐ v) (B ·ˡᵐ u) (B ·ˡᵐ v)
        = refl

      f[c*v]≡c*f[v]' : (T : p ⊸ m) (B : p ⊸ n)
                     → (c : A) → (v : Vec A p)
                     → T ·ˡᵐ (c ∘ⱽ v) ++ B ·ˡᵐ (c ∘ⱽ v) ≡
                        c ∘ⱽ (T ·ˡᵐ v ++ B ·ˡᵐ v)
      f[c*v]≡c*f[v]' T B c v rewrite
          f[c*v]≡c*f[v] T c v
        | f[c*v]≡c*f[v] B c v
        | ∘ⱽ-distr-++ c (T ·ˡᵐ v) (B ·ˡᵐ v)
        = refl

  -- horizontal stack forward operator
  _|ˡᵐ_ : m ⊸ p → n ⊸ p → (m +ᴺ n) ⊸ p
  _|ˡᵐ_ {m} {n} {p} T B =
    record
      { f = λ v → T ·ˡᵐ (take m v) +ⱽ B ·ˡᵐ (drop m v)
      ; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]' T B
      ; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]' T B
      }
      where
        f[u+v]≡f[u]+f[v]' : {m n p : ℕ}
                          → (T : m ⊸ p) (B : n ⊸ p)
                          → (u v : Vec A (m +ᴺ n))
                          → T ·ˡᵐ take m (u +ⱽ v) +ⱽ B ·ˡᵐ drop m (u +ⱽ v) ≡
                             T ·ˡᵐ take m u +ⱽ B ·ˡᵐ drop m u +ⱽ
                             (T ·ˡᵐ take m v +ⱽ B ·ˡᵐ drop m v)
        f[u+v]≡f[u]+f[v]' {m} T B u v = begin
            T ·ˡᵐ (take m (u +ⱽ v)) +ⱽ B ·ˡᵐ (drop m (u +ⱽ v))
          ≡⟨ cong₂ (λ x y → T ·ˡᵐ x +ⱽ B ·ˡᵐ y)
                   (take-distr-zipWith _+_ u v) (drop-distr-zipWith _+_ u v)⟩
            T ·ˡᵐ (take m u +ⱽ take m v) +ⱽ B ·ˡᵐ (drop m u +ⱽ drop m v)
          ≡⟨ cong₂ _+ⱽ_ (f[u+v]≡f[u]+f[v] T (take m u) (take m v))
                        (f[u+v]≡f[u]+f[v] B (drop m u) (drop m v)) ⟩
            T ·ˡᵐ take m u +ⱽ T ·ˡᵐ take m v +ⱽ
            (B ·ˡᵐ drop m u +ⱽ B ·ˡᵐ drop m v)
          ≡⟨ sym (+ⱽ-assoc (T ·ˡᵐ take m u +ⱽ T ·ˡᵐ take m v)
                           (B ·ˡᵐ drop m u) (B ·ˡᵐ drop m v)) ⟩
            T ·ˡᵐ take m u +ⱽ T ·ˡᵐ take m v +ⱽ B ·ˡᵐ drop m u +ⱽ
            B ·ˡᵐ drop m v
          ≡⟨ cong (_+ⱽ B ·ˡᵐ drop m v) (+ⱽ-assoc (T ·ˡᵐ take m u)
                                                 (T ·ˡᵐ take m v)
                                                 (B ·ˡᵐ drop m u)) ⟩
            T ·ˡᵐ take m u +ⱽ (T ·ˡᵐ take m v +ⱽ B ·ˡᵐ drop m u) +ⱽ
            B ·ˡᵐ drop m v
          ≡⟨ cong (λ x → (T ·ˡᵐ take m u +ⱽ x) +ⱽ B ·ˡᵐ drop m v)
                  (+ⱽ-comm (T ·ˡᵐ take m v) (B ·ˡᵐ drop m u)) ⟩
            (T ·ˡᵐ take m u +ⱽ ((B ·ˡᵐ drop m u +ⱽ T ·ˡᵐ take m v))) +ⱽ
            B ·ˡᵐ drop m v
          ≡⟨ cong (_+ⱽ B ·ˡᵐ drop m v) (sym (+ⱽ-assoc (T ·ˡᵐ take m u)
                                                      (B ·ˡᵐ drop m u)
                                                      (T ·ˡᵐ take m v))) ⟩
            (T ·ˡᵐ take m u +ⱽ B ·ˡᵐ drop m u +ⱽ T ·ˡᵐ take m v) +ⱽ
            B ·ˡᵐ drop m v
          ≡⟨ +ⱽ-assoc (T ·ˡᵐ take m u +ⱽ B ·ˡᵐ drop m u)
                      (T ·ˡᵐ take m v) (B ·ˡᵐ drop m v) ⟩
            T ·ˡᵐ take m u +ⱽ B ·ˡᵐ drop m u +ⱽ
            (T ·ˡᵐ take m v +ⱽ B ·ˡᵐ drop m v)
          ∎

        f[c*v]≡c*f[v]' : {m n p : ℕ}
                       → (T : m ⊸ p) → (B : n ⊸ p)
                       → (c : A) (v : Vec A (m +ᴺ n))
                       → T ·ˡᵐ take m (c ∘ⱽ v) +ⱽ B ·ˡᵐ drop m (c ∘ⱽ v) ≡
                          c ∘ⱽ (T ·ˡᵐ take m v +ⱽ B ·ˡᵐ drop m v)
        f[c*v]≡c*f[v]' {m} T B c v = begin
            T ·ˡᵐ take m (c ∘ⱽ v) +ⱽ B ·ˡᵐ drop m (c ∘ⱽ v)
          ≡⟨ cong₂ (λ x y → T ·ˡᵐ x +ⱽ B ·ˡᵐ y) (take-distr-map (c *_) m v)
                                                 (drop-distr-map (c *_) m v) ⟩
            T ·ˡᵐ (c ∘ⱽ take m v) +ⱽ B ·ˡᵐ (c ∘ⱽ drop m v)
          ≡⟨ cong₂ _+ⱽ_ (f[c*v]≡c*f[v] T c (take m v))
                        (f[c*v]≡c*f[v] B c (drop m v)) ⟩
            c ∘ⱽ (T ·ˡᵐ take m v) +ⱽ c ∘ⱽ (B ·ˡᵐ drop m v)
          ≡⟨ sym (∘ⱽ-distr-+ⱽ c (T ·ˡᵐ take m v) (B ·ˡᵐ drop m v)) ⟩
            c ∘ⱽ (T ·ˡᵐ take m v +ⱽ B ·ˡᵐ drop m v)
          ∎

  -- block diagonal forward and adjoint operator
  _/ˡᵐ_ : m ⊸ n → p ⊸ q → (m +ᴺ p) ⊸ (n +ᴺ q)
  _/ˡᵐ_ {m} {n} {p} {q} T B =
    record
      { f = λ v → T ·ˡᵐ (take m v) ++ B ·ˡᵐ (drop m v)
      ; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]' T B
      ; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]' T B
      }
      where
        f[u+v]≡f[u]+f[v]' : {m n p q : ℕ}
                          → (T : m ⊸ n) (B : p ⊸ q)
                          → (u v : Vec A (m +ᴺ p))
                          → T ·ˡᵐ (take m (u +ⱽ v)) ++ B ·ˡᵐ (drop m (u +ⱽ v)) ≡
                             (T ·ˡᵐ (take m u) ++ B ·ˡᵐ (drop m u)) +ⱽ
                             (T ·ˡᵐ (take m v) ++ B ·ˡᵐ (drop m v))
        f[u+v]≡f[u]+f[v]' {m} T B u v =
          begin
              T ·ˡᵐ take m (u +ⱽ v) ++ B ·ˡᵐ drop m (u +ⱽ v)
            ≡⟨ cong₂ (λ x y → T ·ˡᵐ x ++ B ·ˡᵐ y)
                     (take-distr-zipWith _+_ u v) (drop-distr-zipWith _+_ u v)⟩
              T ·ˡᵐ (take m u +ⱽ take m v) ++ B ·ˡᵐ (drop m u +ⱽ drop m v)
            ≡⟨ cong₂ _++_ (f[u+v]≡f[u]+f[v] T (take m u) (take m v))
                          (f[u+v]≡f[u]+f[v] B (drop m u) (drop m v)) ⟩
              (T ·ˡᵐ take m u +ⱽ T ·ˡᵐ take m v) ++
              (B ·ˡᵐ drop m u +ⱽ B ·ˡᵐ drop m v)
            ≡⟨ sym (+ⱽ-flip-++ (T ·ˡᵐ take m u) (T ·ˡᵐ take m v)
                               (B ·ˡᵐ drop m u) (B ·ˡᵐ drop m v)) ⟩
              (T ·ˡᵐ take m u ++ B ·ˡᵐ drop m u) +ⱽ
              (T ·ˡᵐ take m v ++ B ·ˡᵐ drop m v)
          ∎

        f[c*v]≡c*f[v]' : {m n p q : ℕ}
                       → (T : m ⊸ n) (B : p ⊸ q)
                       → (c : A) (v : Vec A (m +ᴺ p))
                       → T ·ˡᵐ (take m (c ∘ⱽ v)) ++ B ·ˡᵐ (drop m (c ∘ⱽ v)) ≡
                          c ∘ⱽ (T ·ˡᵐ (take m v) ++ B ·ˡᵐ (drop m v))
        f[c*v]≡c*f[v]' {m} T B c v =
          begin
              T ·ˡᵐ take m (c ∘ⱽ v) ++ B ·ˡᵐ drop m (c ∘ⱽ v)
            ≡⟨ cong₂ (λ x y → T ·ˡᵐ x ++ B ·ˡᵐ y) (take-distr-map (c *_) m v)
                                                   (drop-distr-map (c *_) m v) ⟩
              T ·ˡᵐ (c ∘ⱽ take m v) ++ B ·ˡᵐ (c ∘ⱽ (drop m v))
            ≡⟨ cong₂ _++_ (f[c*v]≡c*f[v] T c (take m v))
                          (f[c*v]≡c*f[v] B c (drop m v)) ⟩
              c ∘ⱽ (T ·ˡᵐ take m v) ++ c ∘ⱽ (B ·ˡᵐ drop m v)
            ≡⟨ sym (∘ⱽ-distr-++ c (T ·ˡᵐ take m v) (B ·ˡᵐ drop m v)) ⟩
              c ∘ⱽ (T ·ˡᵐ take m v ++ B ·ˡᵐ drop m v)
          ∎

  -- Multiply by a constant
  _∘ˡᵐ_ : A → n ⊸ m → n ⊸ m
  c ∘ˡᵐ m =
    record
      { f = λ v → c ∘ⱽ m ·ˡᵐ v
      ; f[u+v]≡f[u]+f[v] = λ u v → trans (cong (c ∘ⱽ_) (f[u+v]≡f[u]+f[v] m u v))
                                         (∘ⱽ-distr-+ⱽ c (m ·ˡᵐ u) (m ·ˡᵐ v))
      ; f[c*v]≡c*f[v] = λ c₁ v → trans (cong (c ∘ⱽ_) (f[c*v]≡c*f[v] m c₁ v))
                                       (∘ⱽ-comm c c₁ (f m v))
      }

  -- Choose 20 since function application is assumed higher than almost anything
  infixr 20 _·ˡᵐ_

  infixl 2 _—ˡᵐ_
  infixl 3 _|ˡᵐ_
  infixl 4 _/ˡᵐ_
  infixl 6 _+ˡᵐ_
  infixl 6 _-ˡᵐ_
  infixl 7 _*ˡᵐ_
  infixl 10 _∘ˡᵐ_

-- Example LinearMap values ---------------------------------------------------

module _ ⦃ F : Field A ⦄ where
  open Field F

  idₗₘ : n ⊸ n
  idₗₘ = record
    { f = id
    ; f[u+v]≡f[u]+f[v] = λ u v → refl
    ; f[c*v]≡c*f[v] = λ c v → refl
    }

  diagₗₘ : Vec A n → n ⊸ n
  diagₗₘ d = record
    { f = d *ⱽ_
    ; f[u+v]≡f[u]+f[v] = *ⱽ-distr-+ⱽ d
    ; f[c*v]≡c*f[v] = λ c v → *ⱽ∘ⱽ≡∘ⱽ*ⱽ c d v
    }

  1ₗₘ : n ⊸ m
  1ₗₘ = record
    { f = λ v → replicate (sum v)
    ; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]
    ; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]
    }
    where
      f[u+v]≡f[u]+f[v] : (u v : Vec A n)
                       → replicate (sum (u +ⱽ v)) ≡
                          replicate (sum u) +ⱽ replicate (sum v)
      f[u+v]≡f[u]+f[v] u v = begin
        replicate (sum (u +ⱽ v))      ≡⟨ cong replicate (sum-distr-+ⱽ u v) ⟩
        replicate ((sum u) + (sum v)) ≡⟨ replicate-distr-+ (sum u) (sum v) ⟩
        replicate (sum u) +ⱽ replicate (sum v) ∎

      f[c*v]≡c*f[v] : (c : A) (v : Vec A n)
                    → replicate (sum (c ∘ⱽ v)) ≡ c ∘ⱽ replicate (sum v)
      f[c*v]≡c*f[v] c v = begin
        replicate (sum (c ∘ⱽ v)) ≡⟨ cong replicate (sum[c∘ⱽv]≡c*sum[v] c v) ⟩
        replicate (c * sum v)    ≡⟨ replicate[a*b]≡a∘ⱽreplicate[b] c (sum v) ⟩
        c ∘ⱽ replicate (sum v)   ∎

  -- This could be defined as 0ᶠ ∘ˡᵐ allonesₗₘ, but then that would make
  -- some later proofs more difficult, since they would then have more than
  -- just replicate 0ᶠ to replace zerosₗₘ with.
  0ₗₘ : n ⊸ m
  0ₗₘ =  record
    { f = λ v → replicate 0ᶠ
    ; f[u+v]≡f[u]+f[v] = λ u v → sym (trans (zipWith-replicate _+_ 0ᶠ 0ᶠ)
                                             (cong replicate 0ᶠ+0ᶠ≡0ᶠ))
    ; f[c*v]≡c*f[v] = λ c v → sym (c∘ⱽ0ᶠⱽ≡0ᶠⱽ c)
    }

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:
-- Occurs when different mixfix patterns use similar names.
module Issue147b where

data X : Set where
  f  : X -> X
  f_ : X -> X
  x  : X

bad : X -> X
bad (f x) = x
bad _     = x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bisimilarity for M-types
------------------------------------------------------------------------

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

module Codata.M.Bisimilarity where

open import Level
open import Size
open import Codata.Thunk
open import Codata.M
open import Data.Container.Core
open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_)
open import Data.Product using (_,_)
open import Function
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

data Bisim {s p} (C : Container s p) (i : Size) : Rel (M C ∞) (s ⊔ p) where
  inf : ∀ {t u} → Pointwise C (Thunk^R (Bisim C) i) t u → Bisim C i (inf t) (inf u)

module _ {s p} {C : Container s p} where

  -- unfortunately the proofs are a lot nicer if we do not use the combinators
  -- C.refl, C.sym and C.trans

  refl : ∀ {i} → Reflexive (Bisim C i)
  refl {x = inf t} = inf (P.refl , λ where p .force → refl)

  sym : ∀ {i} → Symmetric (Bisim C i)
  sym  (inf (P.refl , f)) = inf (P.refl , λ where p .force → sym (f p .force))

  trans : ∀ {i} → Transitive (Bisim C i)
  trans (inf (P.refl , f)) (inf (P.refl , g)) =
    inf (P.refl , λ where p .force → trans (f p .force) (g p .force))

  isEquivalence : ∀ {i} → IsEquivalence (Bisim C i)
  isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }

  setoid : {i : Size} → Setoid (s ⊔ p) (s ⊔ p)
  setoid {i} = record
    { isEquivalence = isEquivalence {i}
    }


text:
------------------------------------------------------------------------
-- Least upper bounds
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Delay-monad.Least-upper-bound where

open import Equality.Propositional
open import Prelude hiding (_⊔_)
open import Prelude.Size

open import Nat equality-with-J

open import Delay-monad
open import Delay-monad.Partial-order

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

  -- Least upper bounds (if they exist).

  infix 10 _⊔_

  _⊔_ : ∀ {i} → Delay A i → Delay A i → Delay A i
  now x   ⊔ _       = now x
  later x ⊔ now y   = now y
  later x ⊔ later y = later λ { .force → force x ⊔ force y }

  -- The computation x ⊔ y is smaller than or equal to every upper
  -- bound of x and y.

  ⊔-least-upper-bound : ∀ {i x y z} →
                        [ i ] x ⊑ z → [ i ] y ⊑ z → [ i ] x ⊔ y ⊑ z
  ⊔-least-upper-bound               now        _ = now
  ⊔-least-upper-bound               (laterʳ p) q = laterʳ (⊔-least-upper-bound p (laterʳ⁻¹ q))
  ⊔-least-upper-bound {y = now y}   (laterˡ _) q = q
  ⊔-least-upper-bound {y = later y} (laterˡ p) q = laterˡ λ { .force →
                                                     ⊔-least-upper-bound (force p) (laterˡ⁻¹ q) }

  -- If x and y have a lower bound, then this is also a lower bound of
  -- x ⊔ y.

  ⊔-lower-bound : ∀ {i x y z} → [ i ] z ⊑ x → [ i ] z ⊑ y → [ i ] z ⊑ x ⊔ y
  ⊔-lower-bound               now        _ = now
  ⊔-lower-bound               (laterˡ p) q = laterˡ λ { .force →
                                               ⊔-lower-bound (force p) (laterˡ⁻¹ q) }
  ⊔-lower-bound {y = now y}   (laterʳ _) q = q
  ⊔-lower-bound {y = later y} (laterʳ p) q = laterʳ (⊔-lower-bound p (laterʳ⁻¹ q))

  -- If x and y have an upper bound, then x ⊔ y is an upper bound
  -- of y.

  ⊔-upper-boundʳ : ∀ {i x y z} →
                   [ i ] x ⊑ z → [ i ] y ⊑ z → [ i ] y ⊑ x ⊔ y
  ⊔-upper-boundʳ               now        q = q
  ⊔-upper-boundʳ               (laterʳ p) q = ⊔-upper-boundʳ p (laterʳ⁻¹ q)
  ⊔-upper-boundʳ {y = now y}   (laterˡ _) _ = now
  ⊔-upper-boundʳ {y = later y} (laterˡ p) q =
    later-cong λ { .force → ⊔-upper-boundʳ (force p) (laterˡ⁻¹ q) }

  -- If x and y have an upper bound, then x ⊔ y is an upper bound
  -- of x.

  ⊔-upper-boundˡ : ∀ {i x y z} →
                   [ i ] x ⊑ z → [ i ] y ⊑ z → [ i ] x ⊑ x ⊔ y
  ⊔-upper-boundˡ               now        q = now
  ⊔-upper-boundˡ               (laterʳ p) q = ⊔-upper-boundˡ p (laterʳ⁻¹ q)
  ⊔-upper-boundˡ {y = later y} (laterˡ p) q = later-cong λ { .force →
                                                ⊔-upper-boundˡ (force p) (laterˡ⁻¹ q) }
  ⊔-upper-boundˡ {y = now y}   (laterˡ p) q = laterˡ λ { .force →
                                                ⊔-upper-boundʳ q (force p) }

  -- A variant of the lower/upper bound lemmas.

  ⊔-lower-upper-bound : ∀ {i x y z} →
                        x ⊑ y → [ i ] y ⊑ z → [ i ] y ⊑ x ⊔ z
  ⊔-lower-upper-bound               now        _            = now
  ⊔-lower-upper-bound               (laterʳ p) q            = laterˡ λ { .force →
                                                                ⊔-lower-upper-bound p (laterˡ⁻¹ q) }
  ⊔-lower-upper-bound               (laterˡ p) (laterʳ q)   = laterʳ (⊔-lower-upper-bound (force p) q)
  ⊔-lower-upper-bound {z = now z}   (laterˡ _) q            = q
  ⊔-lower-upper-bound {z = later z} (laterˡ p) (laterˡ q)   = later-cong λ { .force →
                                                                ⊔-lower-upper-bound
                                                                  (laterʳ⁻¹ (force p))
                                                                  (laterʳ⁻¹ (force q)) }

  -- If x terminates, then x ⊔ y also terminates.

  ⊔-⇓ˡ : ∀ {i x y} {z : A} →
         Terminates i x z → ∃ λ z′ → Terminates i (x ⊔ y) z′
  ⊔-⇓ˡ               now        = _ , now
  ⊔-⇓ˡ {y = now y}   (laterʳ p) = _ , now
  ⊔-⇓ˡ {y = later y} (laterʳ p) = Σ-map id laterʳ (⊔-⇓ˡ p)

  -- If y terminates, then x ⊔ y also terminates.

  ⊔-⇓ʳ : ∀ {i} x {y} {z : A} →
         Terminates i y z → ∃ λ z′ → Terminates i (x ⊔ y) z′
  ⊔-⇓ʳ (now x)   _          = _ , now
  ⊔-⇓ʳ (later x) now        = _ , now
  ⊔-⇓ʳ (later x) (laterʳ p) = Σ-map id laterʳ (⊔-⇓ʳ (force x) p)

-- Increasing sequences.

Increasing-sequence : ∀ {a} → Type a → Type a
Increasing-sequence A =
  ∃ λ (f : ℕ → Delay A ∞) → ∀ n → f n ⊑ f (suc n)

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

  -- The tail of an increasing sequence.

  tailˢ : Increasing-sequence A → Increasing-sequence A
  tailˢ = Σ-map (_∘ suc) (_∘ suc)

  -- Later sequence elements are larger.

  later-larger : (s : Increasing-sequence A) →
                 ∀ {m n} → m ≤ n → proj₁ s m ⊑ proj₁ s n
  later-larger s (≤-refl′ refl)   = reflexive _
  later-larger s (≤-step′ p refl) =
    transitive (later-larger s p) (proj₂ s _)

  -- Least upper bounds of increasing sequences.

  ⨆ : ∀ {i} → Increasing-sequence A → Delay A i
  ⨆ s = proj₁ s 0 ⊔ later λ { .force → ⨆ (tailˢ s) }

  -- ⨆ s is smaller than or equal to every upper bound of s.

  ⨆-least-upper-bound :
    ∀ {i} (s : Increasing-sequence A) ub →
    (∀ n → [ i ] proj₁ s n ⊑ ub) → [ i ] ⨆ s ⊑ ub
  ⨆-least-upper-bound s ub is-ub =
    ⊔-least-upper-bound
      (is-ub 0)
      (laterˡ λ { .force →
         ⨆-least-upper-bound (tailˢ s) ub (is-ub ∘ suc) })

  -- If every element in s terminates with a given value, then ⨆ s
  -- terminates with the same value.

  ⨆-⇓ : ∀ {i x} (s : Increasing-sequence A) →
        (∀ n → proj₁ s n ⇓ x) → Terminates i (⨆ s) x
  ⨆-⇓ s s-⇓ =
    ⊑now→⇓→⇓ (⨆-least-upper-bound s _ (λ n → symmetric (s-⇓ n)))
             (proj₂ (⊔-⇓ˡ (s-⇓ 0)))

  -- If s has a lower bound, then this is also a lower bound of ⨆ s.

  ⨆-lower-bound : ∀ {i} (s : Increasing-sequence A) lb →
                  (∀ n → lb ⊑ proj₁ s n) → [ i ] lb ⊑ ⨆ s
  ⨆-lower-bound s (now x)    is-lb = ⨆-⇓ s is-lb
  ⨆-lower-bound s (later lb) is-lb =
    ⊔-lower-bound
      (is-lb 0)
      (later-cong λ { .force →
         ⨆-lower-bound (tailˢ s) (force lb) λ n →
           laterˡ⁻¹ (transitive (is-lb n) (proj₂ s n)) })

  -- ⨆ s is an upper bound of s.

  ⨆-upper-bound : ∀ {i} (s : Increasing-sequence A) →
                  ∀ n → [ i ] proj₁ s n ⊑ ⨆ s
  ⨆-upper-bound s zero    = ⨆-lower-bound s (proj₁ s 0)
                              (λ n → later-larger s (zero≤ n))
  ⨆-upper-bound s (suc n) = ⊔-lower-upper-bound
                              (later-larger s (zero≤ (suc n)))
                              (laterʳ (⨆-upper-bound (tailˢ s) n))

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
module Normalize where

open import Data.List
open import Data.Product

open import PiLevel0

-- We are going to use all the coherence as follows; make the right
-- hand side canonical and rewrite the left hand side to the right
-- hand side. Brute force below cannot work!

-- Use the same structure as
-- https://agda.github.io/agda-stdlib/Algebra.Monoid-solver.html ??

{-# NO_TERMINATION_CHECK #-}
normalize : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₁ ⟷ t₂)
normalize unite₊ = {!!}
normalize uniti₊ = {!!}
normalize swap₊ = {!!}
normalize assocl₊ = {!!}
normalize assocr₊ = {!!}
normalize unite⋆ = {!!}
normalize uniti⋆ = {!!}
normalize swap⋆ = {!!}
normalize assocl⋆ = {!!}
normalize assocr⋆ = {!!}
normalize absorbr = {!!}
normalize absorbl = {!!}
normalize factorzr = {!!}
normalize factorzl = {!!}
normalize dist = {!!}
normalize factor = {!!}
normalize id⟷ = {!!}
normalize (c ◎ id⟷) = normalize c
normalize (unite₊ ◎ c₁) = {!!}
normalize (uniti₊ ◎ c₁) = {!!}
normalize (swap₊ ◎ c₁) = {!!}
normalize (assocl₊ ◎ c₁) = {!!}
normalize (assocr₊ ◎ c₁) = {!!}
normalize (unite⋆ ◎ c₁) = {!!}
normalize (uniti⋆ ◎ c₁) = {!!}
normalize (swap⋆ ◎ c₁) = {!!}
normalize (assocl⋆ ◎ c₁) = {!!}
normalize (assocr⋆ ◎ c₁) = {!!}
normalize (absorbr ◎ c₁) = {!!}
normalize (absorbl ◎ c₁) = {!!}
normalize (factorzr ◎ c₁) = {!!}
normalize (factorzl ◎ c₁) = {!!}
normalize (dist ◎ c₁) = {!!}
normalize (factor ◎ c₁) = {!!}
normalize (id⟷ ◎ c₁) = normalize c₁
normalize ((c ◎ c₁) ◎ c₂) = normalize (c ◎ (c₁ ◎ c₂))
normalize ((c ⊕ c₁) ◎ c₂) = {!!}
normalize ((c ⊗ c₁) ◎ c₂) = {!!}
normalize (c ⊕ unite₊) = {!!}
normalize (c ⊕ uniti₊) = {!!}
normalize (c ⊕ swap₊) = {!!}
normalize (c ⊕ assocl₊) = {!!}
normalize (c ⊕ assocr₊) = {!!}
normalize (c ⊕ unite⋆) = {!!}
normalize (c ⊕ uniti⋆) = {!!}
normalize (c ⊕ swap⋆) = {!!}
normalize (c ⊕ assocl⋆) = {!!}
normalize (c ⊕ assocr⋆) = {!!}
normalize (c ⊕ absorbr) = {!!}
normalize (c ⊕ absorbl) = {!!}
normalize (c ⊕ factorzr) = {!!}
normalize (c ⊕ factorzl) = {!!}
normalize (c ⊕ dist) = {!!}
normalize (c ⊕ factor) = {!!}
normalize (c ⊕ id⟷) = {!!}
normalize (c ⊕ c₁ ◎ c₂) = {!!}
normalize (c ⊕ (c₁ ⊕ c₂)) = {!!}
normalize (c ⊕ (c₁ ⊗ c₂)) = {!!}
normalize (c ⊗ c₁) = {!!}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Prelude.Maybe where

open import Prelude.Unit
open import Prelude.Empty
open import Prelude.Function
open import Prelude.Functor
open import Prelude.Applicative
open import Prelude.Monad
open import Prelude.Equality
open import Prelude.Decidable

data Maybe {a} (A : Set a) : Set a where
  nothing : Maybe A
  just    : A → Maybe A

{-# FOREIGN GHC type AgdaMaybe l = Maybe #-}
{-# COMPILE GHC Maybe = data MAlonzo.Code.Prelude.Maybe.AgdaMaybe (Nothing | Just) #-}

maybe : ∀ {a b} {A : Set a} {B : Set b} → B → (A → B) → Maybe A → B
maybe z f nothing  = z
maybe z f (just x) = f x
{-# INLINE maybe #-}

fromMaybe : ∀ {a} {A : Set a} → A → Maybe A → A
fromMaybe z = maybe z id
{-# INLINE fromMaybe #-}

IsJust : ∀ {a} {A : Set a} → Maybe A → Set
IsJust = maybe ⊥ (const ⊤)

FromJust : ∀ {a} {A : Set a} → Maybe A → Set a
FromJust {A = A} = maybe ⊤′ (const A)

fromJust : ∀ {a} {A : Set a} (m : Maybe A) → FromJust m
fromJust nothing  = _
fromJust (just x) = x

maybeYes : ∀ {a} {A : Set a} → Dec A → Maybe A
maybeYes (yes x) = just x
maybeYes (no _)  = nothing

--- Equality ---

just-inj : ∀ {a} {A : Set a} {x y : A} → just x ≡ just y → x ≡ y
just-inj refl = refl

instance
  EqMaybe : ∀ {a} {A : Set a} {{EqA : Eq A}} → Eq (Maybe A)
  _==_ {{EqMaybe}} nothing nothing  = yes refl
  _==_ {{EqMaybe}} nothing (just x) = no λ ()
  _==_ {{EqMaybe}} (just x) nothing = no λ ()
  _==_ {{EqMaybe}} (just x) (just y) with x == y
  ... | yes eq  = yes (just $≡ eq)
  ... | no  neq = no (λ eq → neq (just-inj eq))

--- Monad ---

instance
  FunctorMaybe : ∀ {a} → Functor (Maybe {a})
  fmap {{FunctorMaybe}} f m = maybe nothing (just ∘ f) m

  ApplicativeMaybe : ∀ {a} → Applicative (Maybe {a})
  pure  {{ApplicativeMaybe}} = just
  _<*>_ {{ApplicativeMaybe}} mf mx = maybe nothing (λ f → fmap f mx) mf

  MonadMaybe : ∀ {a} → Monad {a} Maybe
  _>>=_  {{MonadMaybe}} m f = maybe nothing f m

  FunctorMaybe′ : ∀ {a b} → Functor′ {a} {b} Maybe
  fmap′ {{FunctorMaybe′}} f m = maybe nothing (just ∘ f) m

  ApplicativeMaybe′ : ∀ {a b} → Applicative′ {a} {b} Maybe
  _<*>′_ {{ApplicativeMaybe′}} (just f) (just x) = just (f x)
  _<*>′_ {{ApplicativeMaybe′}}  _        _       = nothing

  MonadMaybe′ : ∀ {a b} → Monad′ {a} {b} Maybe
  _>>=′_ {{MonadMaybe′}} m f = maybe nothing f m

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Properties where

-- Properties valid of all Functors
open import Level
open import Data.Product using (proj₁; proj₂; _,_)
open import Function.Surjection using (Surjective)
open import Function.Equivalence using (Equivalence)
open import Function.Equality hiding (_∘_)

open import Categories.Category
open import Categories.Functor.Core
open import Categories.Functor
open import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as Reas
open import Categories.Morphism.IsoEquiv as IsoEquiv
open import Categories.Morphism.Isomorphism

open import Relation.Binary using (_Preserves_⟶_)

private
  variable
    o ℓ e : Level
    C D : Category o ℓ e

-- a series of [ Functor ]-respects-Thing combinators (with respects -> resp)

module _ (F : Functor C D) where
  private
    module C = Category C
    module D = Category D
    module IsoC = IsoEquiv C
    module IsoD = IsoEquiv D
  open C hiding (_∘_)
  open Functor F

  private
    variable
      A B E : Obj
      f g h i : A ⇒ B

  [_]-resp-∘ : C [ C [ f ∘ g ] ≈ h ] → D [ D [ F₁ f ∘ F₁ g ] ≈ F₁ h ]
  [_]-resp-∘ {f = f} {g = g} {h = h} eq = begin
    F₁ f ∘ F₁ g      ≈˘⟨ homomorphism ⟩
    F₁ (C [ f ∘ g ]) ≈⟨ F-resp-≈ eq ⟩
    F₁ h             ∎
    where open D
          open D.HomReasoning

  [_]-resp-square : C.CommutativeSquare f g h i →
                    D.CommutativeSquare (F₁ f) (F₁ g) (F₁ h) (F₁ i)
  [_]-resp-square {f = f} {g = g} {h = h} {i = i} sq = begin
    F₁ h ∘ F₁ f      ≈˘⟨ homomorphism ⟩
    F₁ (C [ h ∘ f ]) ≈⟨ F-resp-≈ sq ⟩
    F₁ (C [ i ∘ g ]) ≈⟨ homomorphism ⟩
    F₁ i ∘ F₁ g       ∎
    where open D
          open D.HomReasoning

  [_]-resp-Iso : Iso C f g → Iso D (F₁ f) (F₁ g)
  [_]-resp-Iso {f = f} {g = g} iso = record
    { isoˡ = begin
      F₁ g ∘ F₁ f      ≈⟨ [ isoˡ ]-resp-∘ ⟩
      F₁ C.id          ≈⟨ identity ⟩
      D.id             ∎
    ; isoʳ = begin
      F₁ f ∘ F₁ g      ≈⟨ [ isoʳ ]-resp-∘ ⟩
      F₁ C.id          ≈⟨ identity ⟩
      D.id             ∎
    }
    where open Iso iso
          open D
          open D.HomReasoning

  [_]-resp-≅ : F₀ Preserves _≅_ C ⟶ _≅_ D
  [_]-resp-≅ i≅j = record
    { from       = F₁ from
    ; to         = F₁ to
    ; iso        = [ iso ]-resp-Iso
    }
    where open _≅_ i≅j

  [_]-resp-≃ : ∀ {f g :  _≅_ C A B} → f IsoC.≃ g → [ f ]-resp-≅ IsoD.≃ [ g ]-resp-≅
  [_]-resp-≃ ⌞ eq ⌟ = ⌞ F-resp-≈ eq ⌟

  homomorphismᵢ : ∀ {f : _≅_ C B E} {g : _≅_ C A B} → [ _∘ᵢ_ C f g ]-resp-≅ IsoD.≃ (_∘ᵢ_ D [ f ]-resp-≅ [ g ]-resp-≅ )
  homomorphismᵢ = ⌞ homomorphism ⌟

  -- Uses a strong version of Essential Surjectivity.
  EssSurj×Full×Faithful⇒Invertible : EssentiallySurjective F → Full F → Faithful F → Functor D C
  EssSurj×Full×Faithful⇒Invertible surj full faith = record
    { F₀ = λ d → proj₁ (surj d)
    ; F₁ = λ {A} {B} f →
      let (a , sa) = surj A in
      let (b , sb) = surj B in
      let module S = Surjective (full {a} {b}) in
      S.from ⟨$⟩ (_≅_.to sb) ∘ f ∘ (_≅_.from sa)
    ; identity = λ {A} →
      let (a , sa) = surj A in begin
      from full ⟨$⟩  _≅_.to sa ∘ D.id ∘ _≅_.from sa ≈⟨ cong (from full) (D.∘-resp-≈ʳ D.identityˡ D.HomReasoning.○ _≅_.isoˡ sa) ⟩
      from full ⟨$⟩ D.id                            ≈˘⟨ cong (from full) identity ⟩
      from full ⟨$⟩ F₁ C.id                         ≈⟨ faith _ _ (right-inverse-of full (F₁ C.id)) ⟩
      C.id ∎
    ; homomorphism = λ {X} {Y} {Z} {f} {g} →
      let (x , sx) = surj X in
      let (y , sy) = surj Y in
      let (z , sz) = surj Z in
      let open Morphism._≅_ in faith _ _ (E.begin
      F₁ (from full ⟨$⟩ to sz ∘ (g ∘ f) ∘ from sx)                                    E.≈⟨ right-inverse-of full _ ⟩
      (to sz ∘ (g ∘ f) ∘ from sx)                                                    E.≈⟨ D.∘-resp-≈ʳ (D.∘-resp-≈ˡ (D.∘-resp-≈ʳ (introˡ (isoʳ sy)))) ⟩
      (to sz ∘ (g ∘ (from sy ∘ to sy) ∘ f) ∘ from sx)                                E.≈˘⟨ D.assoc ⟩
      (to sz ∘ g ∘ ((from sy ∘ to sy) ∘ f)) ∘ from sx                                E.≈⟨ D.∘-resp-≈ˡ (D.∘-resp-≈ʳ (D.∘-resp-≈ʳ D.assoc)) ⟩
      (to sz ∘ g ∘ (from sy ∘ (to sy ∘ f))) ∘ from sx                                E.≈˘⟨ D.∘-resp-≈ˡ D.assoc ⟩
      ((to sz ∘ g) ∘ (from sy ∘ (to sy ∘ f))) ∘ from sx                              E.≈˘⟨ D.∘-resp-≈ˡ D.assoc ⟩
      (((to sz ∘ g) ∘ from sy) ∘ (to sy ∘ f)) ∘ from sx                              E.≈⟨ D.assoc ⟩
      ((to sz ∘ g) ∘ from sy) ∘ ((to sy ∘ f) ∘ from sx)                              E.≈⟨ D.∘-resp-≈ D.assoc D.assoc  ⟩
      (to sz ∘ g ∘ from sy) ∘ (to sy ∘ f ∘ from sx)                                  E.≈˘⟨ D.∘-resp-≈ (right-inverse-of full _) (right-inverse-of full _) ⟩
      F₁ (from full ⟨$⟩ to sz ∘ g ∘ from sy) ∘ F₁ (from full ⟨$⟩ to sy ∘ f ∘ from sx)  E.≈˘⟨ homomorphism ⟩
      F₁ ((from full ⟨$⟩ to sz ∘ g ∘ from sy) C.∘ (from full ⟨$⟩ to sy ∘ f ∘ from sx)) E.∎)
    ; F-resp-≈ = λ f≈g → cong (from full) (D.∘-resp-≈ʳ (D.∘-resp-≈ˡ f≈g))
    }
    where
    open Morphism D
    open Reas D
    open Category D
    open Surjective
    open C.HomReasoning
    module E = D.HomReasoning

-- Functor Composition is Associative and the unit laws are found in
-- NaturalTransformation.NaturalIsomorphism, reified as associator, unitorˡ and unitorʳ.

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module Experiment.Expr.Expr where

open import Data.Fin
open import Data.Empty
open import Level
open import Data.Bool
open import Data.Nat hiding (_⊔_)
open import Data.Product
open import Data.List as List hiding (or; and)

data Expr {v} (V : Set v) : Set v where
  var : V -> Expr V
  or and : Expr V -> Expr V -> Expr V
  neg : Expr V -> Expr V

foldExpr : ∀ {a v} {V : Set v} {A : Set a} →
           (V → A) → (A → A → A) → (A → A → A) → (A → A) →
           Expr V → A
foldExpr v o a n (var v′)    = v v′
foldExpr v o a n (or e₁ e₂)  = o (foldExpr v o a n e₁) (foldExpr v o a n e₂)
foldExpr v o a n (and e₁ e₂) = a (foldExpr v o a n e₁) (foldExpr v o a n e₂)
foldExpr v o a n (neg e)     = n (foldExpr v o a n e)

evalExpr : ∀ {v} {V : Set v} → (V → Bool) → Expr V → Bool
evalExpr v = foldExpr v _∨_ _∧_ not

data Sign : Set where
  pos : Sign
  neg : Sign

Literal : ∀ {a} → Set a → Set a
Literal V = Sign × V

data NNF {v} (V : Set v) : Set v where
  lit : Literal V → NNF V
  and or : NNF V → NNF V → NNF V

data GExpr {v t₁ t₂ tₙ} (T₁ : Set t₁) (T₂ : Set t₂) (Tₙ : Set tₙ) (V : Set v)
  : Set (v ⊔ t₁ ⊔ t₂ ⊔ tₙ) where
  var : (v : V) → GExpr T₁ T₂ Tₙ V
  op₁ : T₁ → (e : GExpr T₁ T₂ Tₙ V) → GExpr T₁ T₂ Tₙ V
  op₂ : T₂ → (e₁ e₂ :  GExpr T₁ T₂ Tₙ V) → GExpr T₁ T₂ Tₙ V
  opₙ : Tₙ → (es : List (GExpr T₁ T₂ Tₙ V)) → GExpr T₁ T₂ Tₙ V

data AndOr : Set where
  and : AndOr
  or : AndOr

data Neg : Set where
  neg : Neg

ExprAndOrNeg : ℕ → Set
ExprAndOrNeg n = GExpr AndOr Neg ⊥ (Fin n)

evalAndOr : AndOr → Bool → Bool → Bool
evalAndOr and = _∧_
evalAndOr or  = _∨_

module _ {v t₁ t₂ tₙ a} {V : Set v} {T₁ : Set t₁}
         {T₂ : Set t₂} {Tₙ : Set tₙ} {A : Set a}
         (var* : V → A) (op₁* : T₁ → A → A) (op₂* : T₂ → A → A → A)
         (opₙ* : Tₙ → List A → A) where
  foldGExpr : GExpr T₁ T₂ Tₙ V → A
  foldGExpr (var v) = var* v
  foldGExpr (op₁ t₁ e) = op₁* t₁ (foldGExpr e)
  foldGExpr (op₂ t₂ e₁ e₂) = op₂* t₂ (foldGExpr e₁) (foldGExpr e₂)
  foldGExpr (opₙ tₙ es) = opₙ* tₙ (List.map foldGExpr es)


text:
module UniDB.Subst.Sum where

open import UniDB.Subst.Core
open import UniDB.Morph.Sum

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

module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}}
  (X : STX) {{wkX : Wk X}} {{apTX : Ap T X}} {{apRelTX : ApRel T X}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
  (Ζ : MOR) {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}}
  where

  ap-inl : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (x : X γ₁) →
    ap {T} {X} {Sum Ξ Ζ} (inl ξ) x ≡ ap {T} ξ x
  ap-inl ξ = ap-rel≅ {T} (≃-to-≅` lem)
    where
      lem : (δ : Dom) → [ T ] inl {Ξ} {Ζ} ξ ↑ δ ≃ ξ ↑ δ
      lk≃ (lem δ) i rewrite inl-↑ Ξ Ζ ξ δ = refl

  ap-inr : {γ₁ γ₂ : Dom} (ζ : Ζ γ₁ γ₂) (x : X γ₁) →
    ap {T} {X} {Sum Ξ Ζ} (inr ζ) x ≡ ap {T} ζ x
  ap-inr ζ = ap-rel≅ {T} (≃-to-≅` lem)
    where
      lem : (δ : Dom) → [ T ] inr {Ξ} {Ζ} ζ ↑ δ ≃ ζ ↑ δ
      lk≃ (lem δ) i rewrite inr-↑ Ξ Ζ ζ δ = refl

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
open import Prelude
open import Reflection renaming (Term to AgTerm; Type to AgType)
open import Data.String using (String)

open import RW.Language.RTerm
open import RW.Language.RTermUtils
open import RW.Language.FinTerm
open import RW.Language.GoalGuesser 1

open import RW.Strategy

module RW.RW (db : TStratDB) where

  open import RW.Utils.Monads
  open import RW.Utils.Error
  open Monad {{...}}
  open IsError {{...}}

  ------------------
  -- Housekeeping --
  ------------------

  -- We need to bring our instances into scope explicitely,
  -- to make Agda happy.
  private
    instance
      ErrErr   = IsError-StratErr
      ErrMonad = MonadError

    unarg : {A : Set} → Arg A → A
    unarg (arg _ x) = x

  -- We need to translate types to FinTerms, so we know how many variables
  -- we're expecting to guess from instantiation.
  Ag2RTypeFin : AgType → ∃ FinTerm
  Ag2RTypeFin = R2FinType ∘ lift-ivar ∘ η ∘ Ag2RType

  -- TODO: fix the duality: "number of ivar's lifted to ovar's vs. parameters we need to guess"

  make-RWData : Name → AgTerm → List (Arg AgType) → Err StratErr RWData
  make-RWData act goal ctx with η (Ag2RTerm goal) | Ag2RTypeFin (type act) | map (Ag2RType ∘ unarg) ctx
  ...| g' | tyℕ , ty | ctx' with forceBinary g' | forceBinary (typeResult ty)
  ...| just g | just a = return (rw-data g tyℕ a ctx')
  ...| just _ | nothing = throwError (Custom "Something strange happened with the action")
  ...| nothing | just _ = throwError (Custom "Something strange happened with the goal")
  ...| nothing | nothing = throwError (Custom "My brain just exploded.")

  -- Given a goal and a list of actions to apply to such goal, return
  -- a list l₁ ⋯ lₙ such that ∀ 0 < i ≤ n . tyᵢ : p1 lᵢ → p1 lᵢ₊₁
  Ag2RTypeFin* : RTerm ⊥ → List AgType → Maybe (List (RBinApp ⊥ × ∃ (RBinApp ∘ Fin)))
  Ag2RTypeFin* (rapp n (g₁ ∷ g₂ ∷ [])) tys
    =            mapM (return ∘ Ag2RTypeFin) tys
    >>=          mapM (λ v → forceBinary (typeResult (p2 v)) >>= (return ∘ (_,_ $ p1 v)))
    >>= λ tys' → (divideGoal (n , g₁ , g₂) tys' >>= assemble)
    >>= λ gs   → return (zip gs tys')
    where
      assemble : {A : Set} → List (RTerm A) → Maybe (List (RBinApp A))
      assemble (x1 ∷ x2 ∷ []) = just ((n , x1 , x2) ∷ [])
      assemble (x1 ∷ x2 ∷ l)  = assemble (x2 ∷ l) >>= return ∘ (_∷_ (n , x1 , x2))
      assemble _              = nothing
  Ag2RTypeFin* _ _ = nothing

  -- Produces a list of RWData, one for each 'guessed' step.
  make-RWData* : List Name → AgTerm → List (Arg AgType) → Err StratErr (List RWData)
  make-RWData* acts goal ctx with Ag2RTerm goal | map type acts | map (Ag2RType ∘ unarg) ctx
  ...| g' | tys | ctx' with Ag2RTypeFin* g' tys
  ...| nothing = throwError (Custom "Are you sure you can apply those steps?")
  ...| just r  = i2 (map (λ x → rw-data (p1 x) (p1 (p2 x)) (p2 (p2 x)) ctx') r)

  postulate
    RW-error : ∀{a}{A : Set a} → String → A

  RWerr : Name → RWData → Err StratErr (RWData × UData × RTerm ⊥)
  RWerr act d
    =   runUStrats d
    >>= λ u → runTStrats db d act u
    >>= λ v → return (d , u , v)

  -- A variant with less information, more suitable to be map'ed.
  RWerr-less : Name → RWData → Err StratErr (RTerm ⊥)
  RWerr-less act d = RWerr act d >>= return ∘ p2 ∘ p2

  ----------------
  -- By Tactics --
  ----------------

  -- Standard debugging version.
  by' : Name → List (Arg AgType) → AgTerm → (RWData × UData × RTerm ⊥)
  by' act ctx goal with runErr (make-RWData act goal ctx >>= RWerr act)
  ...| i1 err  = RW-error err
  ...| i2 term = term

  -- This function is only beeing used to pass the context
  -- given by the 'tactic' keyword around.
  by : Name → List (Arg AgType) → AgTerm → AgTerm
  by act ctx goal = R2AgTerm ∘ p2 ∘ p2 $ (by' act ctx goal)

  -- Handling multiple actions, naive way.
  -- by+ is pretty much foldM (<|>) error (by ⋯),
  -- where (<|>) is the usual alternative from Error Monad.
  by+ : List Name → List (Arg AgType) → AgTerm → AgTerm
  by+ [] _ _ = RW-error "No suitable action"
  by+ (a ∷ as) ctx goal with runErr (make-RWData a goal ctx >>= RWerr a)
  ...| i1 _ = by+ as ctx goal
  ...| i2 t = R2AgTerm ∘ p2 ∘ p2 $ t

  join-tr : Name → List (RTerm ⊥) → RTerm ⊥
  join-tr _  []      = ivar 0
  join-tr tr (x ∷ l) = foldr (λ h r → rapp (rdef tr) (r ∷ h ∷ [])) x l

  -- Handling multiple goals.
  by*-err : Name → List Name → List (Arg AgType) → AgTerm → Err StratErr AgTerm
  by*-err tr acts ctx goal
    =   make-RWData* acts goal ctx
    >>= λ l → mapM (uncurry RWerr-less) (zip acts l)
    >>= return ∘ R2AgTerm ∘ join-tr tr
    where
      unzip : {A B : Set} → List (A × B) → List A × List B
      unzip [] = [] , []
      unzip ((a , b) ∷ l) with unzip l
      ...| la , lb = a ∷ la , b ∷ lb

  by*-tactic : Set
  by*-tactic = List Name → List (Arg AgType) → AgTerm → AgTerm

  by* : Name → by*-tactic
  by* tr acts ctx goal with runErr (by*-err tr acts ctx goal)
  ...| i1 err = RW-error err
  ...| i2 res = res

  ------------------------------
  -- Adding Tries to the cake --
  ------------------------------

  -- The proper way to handle multiple actions.

  open import RW.Data.RTrie

  module Auto
    (bt    : RTrie)                 -- which trie to use,
    (newHd : RTermName → RTermName) -- given the goal head, how to build the head for the action.
    where

    open import RW.Language.RTermTrie

    our-strategy : RTermName → Name → UData → Err StratErr (RTerm ⊥)
    our-strategy goal
      = maybe
        TStrat.how
        (const $ const $ i1 no-strat)
      $ filter-db db
      where
        no-strat : StratErr
        no-strat = NoTStrat goal (newHd goal)

        filter-db : TStratDB → Maybe TStrat
        filter-db [] = nothing
        filter-db (s ∷ ss) with TStrat.when s goal (newHd goal)
        ...| false = filter-db ss
        ...| true  = just s

    auto-internal : List (Arg AgType) → AgTerm → Err StratErr AgTerm
    auto-internal _ goal with forceBinary $ Ag2RTerm goal
    ...| nothing = i1 $ Custom "non-binary goal"
    ...| just (hd , g₁ , g₂)
      = let
        options = search-action (newHd hd) (hd , g₁ , g₂) bt
        strat   = uncurry $ our-strategy hd
        err     = Custom "No option was succesful"
      in try-all strat err options >>= return ∘ R2AgTerm

    auto : List (Arg AgType) → AgTerm → AgTerm
    auto ctx goal with runErr (auto-internal ctx goal)
    ...| i1 err = RW-error err
    ...| i2 r   = r

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


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

module Cardinality.Finite.SplitEnumerable.Inductive where

open import Data.List public
open import Data.List.Membership
open import Prelude

ℰ! : Type a → Type a
ℰ! A = Σ[ xs ⦂ List A ] ((x : A) → x ∈ xs)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

open import Cubical.Core.Everything
open import Cubical.Relation.Binary.Raw

module Cubical.Relation.Binary.Reasoning.Equivalence {c ℓ} {A : Type c} (E : Equivalence A ℓ) where

open Equivalence E

------------------------------------------------------------------------
-- Reasoning combinators

open import Cubical.Relation.Binary.Reasoning.PartialEquivalence partialEquivalence public
  hiding (_∎⟨_⟩)
open import Cubical.Relation.Binary.Reasoning.Base.Single _≈_ isPreorder public
  using (_∎)


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

open import HoTT
open import homotopy.OneSkeleton

module homotopy.ConstantToSetFactorization
  {i j} {A : Type i} {B : Type j} (B-is-set : is-set B)
  (f : A → B) (f-is-const : ∀ a₁ a₂ → f a₁ == f a₂) where

  private
    Skel : Type i
    Skel = Trunc ⟨0⟩ (OneSkeleton f)

    abstract
      Skel-has-all-paths : has-all-paths Skel
      Skel-has-all-paths =
        Trunc-elim (λ _ → Π-is-set λ _ → =-preserves-set Trunc-level)
          (OneSkeleton-elim {P = λ s₁ → ∀ [s₂] → [ s₁ ] == [s₂]}
            (λ a₁ → Trunc-elim (λ _ → =-preserves-set Trunc-level)
              (OneSkeleton-elim {P = λ s₂ → [ point a₁ ] == [ s₂ ]}
                (λ a₂ → ap [_] $ link a₁ a₂ $ f-is-const a₁ a₂)
                (λ _ _ _ → prop-has-all-paths-↓ (Trunc-level {n = ⟨0⟩} _ _))))
            (λ a₁ a₂ p → ↓-cst→app-in λ s₂ →
              prop-has-all-paths-↓ (Trunc-level {n = ⟨0⟩} _ _)))

    Skel-is-prop : is-prop Skel
    Skel-is-prop = all-paths-is-prop Skel-has-all-paths

  cst-extend : Trunc ⟨-1⟩ A → B
  cst-extend = Trunc-rec B-is-set OneSkeleton-lift
             ∘ Trunc-rec Skel-is-prop ([_] ∘ point)

  -- The beta rule.
  -- This is definitionally true, so you don't need it.
  cst-extend-β : cst-extend ∘ [_] == f
  cst-extend-β = idp

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda