text:
open import Prelude
open import dynamics-core

module lemmas-matching where
  -- arrow matching produces unique answers
  ▸arr-unicity : ∀{τ τ2 τ3} →
                 τ ▸arr τ2 →
                 τ ▸arr τ3 →
                 τ2 == τ3
  ▸arr-unicity MAHole MAHole = refl
  ▸arr-unicity MAArr MAArr   = refl

  -- only consistent types arrow match
  ▸arr-consist : ∀{τ1 τ2} →
                 τ1 ▸arr τ2 →
                 (τ1 ~ τ2)
  ▸arr-consist MAHole = TCHole2
  ▸arr-consist MAArr  = TCRefl

  -- if an arrow matches, then it's consistent with the
  -- least restrictive function type
  ▸arr-consist-hole : ∀{t t'} →
                      t ▸arr t' →
                      t ~ (⦇-⦈ ==> ⦇-⦈)
  ▸arr-consist-hole MAHole = TCHole2
  ▸arr-consist-hole MAArr  = TCArr TCHole1 TCHole1

  -- sum matching produces unique answers
  ▸sum-unicity : ∀{τ τ2 τ3} →
                 τ ▸sum τ2 →
                 τ ▸sum τ3 →
                 τ2 == τ3
  ▸sum-unicity MSHole MSHole = refl
  ▸sum-unicity MSSum MSSum   = refl

  -- only consistent types sum match
  ▸sum-consist : ∀{τ1 τ2} →
                 τ1 ▸sum τ2 →
                 (τ1 ~ τ2)
  ▸sum-consist MSHole = TCHole2
  ▸sum-consist MSSum  = TCRefl

  -- if a sum matches, then it's consistent with the
  -- least restrictive function type
  ▸sum-consist-hole : ∀{t t'} →
                      t ▸sum t' →
                      t ~ (⦇-⦈ ⊕ ⦇-⦈)
  ▸sum-consist-hole MSHole = TCHole2
  ▸sum-consist-hole MSSum  = TCSum TCHole1 TCHole1

  -- product matching produces unique answers
  ▸prod-unicity : ∀{τ τ2 τ3} →
                  τ ▸prod τ2 →
                  τ ▸prod τ3 →
                  τ2 == τ3
  ▸prod-unicity MPHole MPHole = refl
  ▸prod-unicity MPProd MPProd   = refl

  -- only consistent types product match
  ▸prod-consist : ∀{τ1 τ2} →
                  τ1 ▸prod τ2 →
                  (τ1 ~ τ2)
  ▸prod-consist MPHole = TCHole2
  ▸prod-consist MPProd = TCRefl

   -- if a sum matches, then it's consistent with the
  -- least restrictive function type
  ▸prod-consist-hole : ∀{t t'} →
                       t ▸prod t' →
                       t ~ (⦇-⦈ ⊠ ⦇-⦈)
  ▸prod-consist-hole MPHole = TCHole2
  ▸prod-consist-hole MPProd = TCProd TCHole1 TCHole1

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Haskell.Prim.Ord where

open import Agda.Builtin.Nat as Nat hiding (_==_; _<_)
open import Agda.Builtin.Char

open import Haskell.Prim
open import Haskell.Prim.Eq
open import Haskell.Prim.Bool
open import Haskell.Prim.Int
open import Haskell.Prim.Word
open import Haskell.Prim.Integer
open import Haskell.Prim.Double
open import Haskell.Prim.Tuple
open import Haskell.Prim.Monoid
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Either

--------------------------------------------------
-- Ordering

data Ordering : Set where
  LT EQ GT : Ordering

instance
  iEqOrdering : Eq Ordering
  iEqOrdering ._==_ LT LT = true
  iEqOrdering ._==_ EQ EQ = true
  iEqOrdering ._==_ GT GT = true
  iEqOrdering ._==_ _  _  = false

  iSemigroupOrdering : Semigroup Ordering
  iSemigroupOrdering ._<>_ LT _ = LT
  iSemigroupOrdering ._<>_ EQ o = o
  iSemigroupOrdering ._<>_ GT _ = GT

  iMonoidOrdering : Monoid Ordering
  iMonoidOrdering .mempty = EQ

--------------------------------------------------
-- Ord

record Ord (a : Set) : Set where
  field
    compare : a → a → Ordering
    _<_  : a → a → Bool
    _>_  : a → a → Bool
    _>=_ : a → a → Bool
    _<=_ : a → a → Bool
    max  : a → a → a
    min  : a → a → a
    overlap ⦃ super ⦄ : Eq a

  infix 4 _<_ _>_ _<=_ _>=_

open Ord ⦃ ... ⦄ public

{-# COMPILE AGDA2HS Ord existing-class #-}

ordFromCompare : ⦃ Eq a ⦄ → (a → a → Ordering) → Ord a
ordFromCompare cmp .compare = cmp
ordFromCompare cmp ._<_  x y = cmp x y == LT
ordFromCompare cmp ._>_  x y = cmp x y == GT
ordFromCompare cmp ._<=_ x y = cmp x y /= GT
ordFromCompare cmp ._>=_ x y = cmp x y /= LT
ordFromCompare cmp .max  x y = if cmp x y == LT then y else x
ordFromCompare cmp .min  x y = if cmp x y == GT then y else x

ordFromLessThan : ⦃ Eq a ⦄ → (a → a → Bool) → Ord a
ordFromLessThan _<_ .compare x y = if x < y then LT else if x == y then EQ else GT
ordFromLessThan _<_ ._<_  x y = x < y
ordFromLessThan _<_ ._>_  x y = y < x
ordFromLessThan _<_ ._<=_ x y = x < y || x == y
ordFromLessThan _<_ ._>=_ x y = y < x || x == y
ordFromLessThan _<_ .max  x y = if x < y then y else x
ordFromLessThan _<_ .min  x y = if y < x then y else x

ordFromLessEq : ⦃ Eq a ⦄ → (a → a → Bool) → Ord a
ordFromLessEq _<=_ .compare x y = if x == y then EQ else if x <= y then LT else GT
ordFromLessEq _<=_ ._<_  x y = x <= y && not (x == y)
ordFromLessEq _<=_ ._>_  x y = y <= x && not (x == y)
ordFromLessEq _<=_ ._<=_ x y = x <= y
ordFromLessEq _<=_ ._>=_ x y = y <= x
ordFromLessEq _<=_ .max  x y = if y <= x then x else y
ordFromLessEq _<=_ .min  x y = if x <= y then x else y

private
  compareFromLt : ⦃ Eq a ⦄ → (a → a → Bool) → a → a → Ordering
  compareFromLt _<_ x y = if x < y then LT else if x == y then EQ else GT

instance
  iOrdNat : Ord Nat
  iOrdNat = ordFromLessThan Nat._<_

  iOrdInteger : Ord Integer
  iOrdInteger = ordFromLessThan ltInteger

  iOrdInt : Ord Int
  iOrdInt = ordFromLessThan ltInt

  iOrdWord : Ord Word
  iOrdWord = ordFromLessThan ltWord

  iOrdDouble : Ord Double
  iOrdDouble = ordFromLessThan primFloatNumericalLess

  iOrdChar : Ord Char
  iOrdChar = ordFromLessThan λ x y → primCharToNat x < primCharToNat y

  iOrdBool : Ord Bool
  iOrdBool = ordFromCompare λ where
    false true  → LT
    true  false → GT
    _     _     → EQ

  iOrdTuple₀ : Ord (Tuple [])
  iOrdTuple₀ = ordFromCompare λ _ _ → EQ

  iOrdTuple : ∀ {as} → ⦃ Ord a ⦄ → ⦃ Ord (Tuple as) ⦄ → Ord (Tuple (a ∷ as))
  iOrdTuple = ordFromCompare λ where (x ∷ xs) (y ∷ ys) → compare x y <> compare xs ys

compareList : ⦃ Ord a ⦄ → List a → List a → Ordering
compareList []       []       = EQ
compareList []       (_ ∷ _)  = LT
compareList (_ ∷ _)  []       = GT
compareList (x ∷ xs) (y ∷ ys) = compare x y <> compareList xs ys

instance
  iOrdList : ⦃ Ord a ⦄ → Ord (List a)
  iOrdList = ordFromCompare compareList

  iOrdMaybe : ⦃ Ord a ⦄ → Ord (Maybe a)
  iOrdMaybe = ordFromCompare λ where
    Nothing  Nothing  → EQ
    Nothing  (Just _) → LT
    (Just _) Nothing  → GT
    (Just x) (Just y) → compare x y

  iOrdEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (Either a b)
  iOrdEither = ordFromCompare λ where
    (Left  x) (Left  y) → compare x y
    (Left  _) (Right _) → LT
    (Right _) (Left  _) → GT
    (Right x) (Right y) → compare x y

  iOrdOrdering : Ord Ordering
  iOrdOrdering = ordFromCompare λ where
    LT LT → EQ
    LT _  → LT
    _  LT → GT
    EQ EQ → EQ
    EQ GT → LT
    GT EQ → GT
    GT GT → EQ

ext: agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.UnivariateHIT.Polyn-nPoly where

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

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.DirectSumFun
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyHIT
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly

open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.Poly0-A
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.An[Am[X]]-Anm[X]
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.AB-An[X]Bn[X]

open CommRingEquivs renaming (compCommRingEquiv to _∘-ecr_ ; invCommRingEquiv to inv-ecr)

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- Definition

module equiv1 (A'@(A , Astr) : CommRing ℓ)
  where

  private
    PA = PolyCommRing A' 1
    PAstr = snd PA
    PA' = nUnivariatePolyHIT A' 1
    PA'str = snd PA'

  open CommRingStr

  directSense : fst (PolyCommRing A' 1) → fst (nUnivariatePolyHIT A' 1)
  directSense = DS-Rec-Set.f _ _ _ _
                (is-set PA'str)
                (0r PA'str)
                (λ { (n ∷ []) a → base n a})
                (_+_ PA'str)
                (+Assoc PA'str)
                (+IdR PA'str)
                (+Comm PA'str)
                (λ { (n ∷ []) → base-neutral _ })
                λ { (n ∷ []) a b  → base-add _ _ _}

  convSense : fst (nUnivariatePolyHIT A' 1) → fst (PolyCommRing A' 1)
  convSense = DS-Rec-Set.f _ _ _ _
               (is-set PAstr)
               (0r PAstr)
               (λ n a → base (n ∷ []) a)
               (_+_ PAstr)
               (+Assoc PAstr)
               (+IdR PAstr)
               (+Comm PAstr)
               (λ n → base-neutral _)
               λ _ _ _ → base-add _ _ _

  retr : (x : fst (PolyCommRing A' 1)) → convSense (directSense x) ≡ x
  retr = DS-Ind-Prop.f _ _ _ _ (λ _ → is-set PAstr _ _)
         refl
         (λ { (n ∷ []) a → refl})
         (λ {U V} ind-U ind-V → cong₂ (_+_ PAstr) ind-U ind-V)

  sect : (x : fst (nUnivariatePolyHIT A' 1)) → (directSense (convSense x) ≡ x)
  sect = DS-Ind-Prop.f _ _ _ _ (λ _ → is-set PA'str _ _)
         refl
         (λ n a → refl)
         (λ {U V} ind-U ind-V → cong₂ (_+_ PA'str) ind-U ind-V)

  converseSense-pres· : (x y : fst (PolyCommRing A' 1)) →
                        directSense (_·_ PAstr x y) ≡ _·_ PA'str (directSense x) (directSense y)
  converseSense-pres· = DS-Ind-Prop.f _ _ _ _
                        (λ _ → isPropΠ λ _ → is-set PA'str _ _)
                        (λ _ → refl)
                        (λ { (n ∷ []) a → DS-Ind-Prop.f _ _ _ _ (λ _ → is-set PA'str _ _)
                                           refl
                                           (λ { (m ∷ []) b → refl})
                                           λ {U V} ind-U ind-V → cong₂ (_+_ PA'str) ind-U ind-V})
                        λ {U V} ind-U ind-V y → cong₂ (_+_ PA'str) (ind-U y) (ind-V y)

  open Iso

  equivR : CommRingEquiv PA PA'
  fst equivR = isoToEquiv is
    where
    is : Iso (PA .fst) (PA' .fst)
    fun is = directSense
    inv is = convSense
    rightInv is = sect
    leftInv is = retr
  snd equivR = makeIsRingHom refl (λ _ _ → refl) converseSense-pres·

open equiv1

Equiv-Polyn-nPolyHIT : (A' : CommRing ℓ) → (n : ℕ) → CommRingEquiv (PolyCommRing A' n) (nUnivariatePolyHIT A' n)
Equiv-Polyn-nPolyHIT A' zero = CRE-Poly0-A A'
Equiv-Polyn-nPolyHIT A' (suc n) =       inv-ecr _ _ (CRE-PolyN∘M-PolyN+M A' 1 n)
                               ∘-ecr (lift-equiv-poly _ _ 1 (Equiv-Polyn-nPolyHIT A' n)
                               ∘-ecr equivR (nUnivariatePolyHIT A' n))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Data.Unit where

open import Agda.Builtin.Unit public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --experimental-irrelevance #-}
-- Andreas, 2011-04-15
-- {-# OPTIONS -v tc.data:20 #-}
module IrrelevantDataParameter where

postulate
  A : Set

data K .(a : A) : Set where
  c : K a

postulate
  a : A

data K' .(b : A) : Set where
  c : K' a
-- ok, since parameter irrelevant

-- 2011-09-09

postulate
  _×_ : ..(A B : Set) -> Set
  Lst : ..(A : Set) -> Set
  nl  : .(A : Set) -> Lst A
  cns : .(A : Set) -> A × Lst A -> Lst A
  -- cns' : .(A : Set) -> (a : A) -> (as : Lst A) -> Lst A -- not well-formed!

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Structure.Operator.Functions where

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

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ : Lvl.Level

module _ {A : Type{ℓ₁}} {X : Type{ℓ₂}} ⦃ equiv-X : Equiv{ℓₑ₁}(X) ⦄ {Y : Type{ℓ₃}} ⦃ equiv-Y : Equiv{ℓₑ₂}(Y) ⦄ where
  -- `a` is a element which yields the left identity element in the function `f`.
  -- (a ∈ kernelₗ(f)) means (f(a) = id).
  kernelₗ : ∀{_▫_ : X → Y → Y}{id : X} → ⦃ _ : Identityₗ(_▫_)(id) ⦄ → (A → X) → A → Stmt
  kernelₗ {_}{id} (f)(a) = (f(a) ≡ id)

  -- `a` is a element which yields the right identity element in the function `f`.
  -- (a ∈ kernelₗ(f)) means (f(a) = id).
  kernelᵣ : ∀{_▫_ : Y → X → Y}{id : X} → ⦃ _ : Identityᵣ(_▫_)(id) ⦄ → (A → X) → A → Stmt
  kernelᵣ {_}{id} (f)(a) = (f(a) ≡ id)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Relation.Binary.Core

module Heapsort.Impl1.Correctness.Order {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import Data.List
open import Function using (_∘_)
open import Heapsort.Impl1 _≤_ tot≤ trans≤
open import List.Sorted _≤_
open import OList _≤_
open import OList.Properties _≤_

theorem-heapsort-sorted : (xs : List A) → Sorted (forget (heapsort xs))
theorem-heapsort-sorted = lemma-olist-sorted ∘ heapsort

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Data.Option.Functions where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Either as Either using (_‖_)
open import Data.Option
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Type

private variable ℓ : Lvl.Level
private variable T A B T₁ T₂ T₃ : Type{ℓ}

-- Applies a function to the inner value of the option container.
-- A functor map for options.
map : (T₁ → T₂) → Option(T₁) → Option(T₂)
map f(Some x) = Some(f(x))
map f(None)   = None

-- Either the value inside the option container or the default value when it is none.
-- An option eliminator.
_or_ : Option(T) → T → T
_or_ (Some x) _   = x
_or_ None     def = def

-- Either transforming the value inside the option container or the default value when it is none.
-- An option eliminator.
partialMap : B → (A → B) → (Option(A) → B)
partialMap _   f (Some x) = f(x)
partialMap def _ None     = def

-- If the option have a value (is Some).
isSome : Option(T) → Bool
isSome (Some _) = 𝑇
isSome None     = 𝐹

-- If the option have no value (is None).
isNone : Option(T) → Bool
isNone (Some _) = 𝐹
isNone None     = 𝑇

-- Passes the inner value of the option to an option-valued function.
-- A monadic bind for options.
_andThen_ : Option(T₁) → (T₁ → Option(T₂)) → Option(T₂)
_andThen_ None     _ = None
_andThen_ (Some x) f = f(x)

-- Combines options of different types by applying the specified binary operator when both options have a value, and none otherwise.
and-combine : (T₁ → T₂ → T₃) → (Option(T₁) → Option(T₂) → Option(T₃))
and-combine (_▫_) (Some x) (Some y)  = Some(x ▫ y)
{-# CATCHALL #-}
and-combine _ _ _ = None

-- Combines options of different types by applying the specified binary operator when both options have a value, and the side functions when only the respective sides have a value. None otherwise.
or-combine : (T₁ → T₂ → T₃) → (T₁ → T₃) → (T₂ → T₃) → (Option(T₁) → Option(T₂) → Option(T₃))
or-combine(_▫_) l r None     None     = None
or-combine(_▫_) l r None     (Some y) = Some(r(y))
or-combine(_▫_) l r (Some x) None     = Some(l(x))
or-combine(_▫_) l r (Some x) (Some y) = Some(x ▫ y)

module Same where
  _orₗ_ : Option(T) → Option(T) → Option(T)
  _orₗ_ = or-combine(\x y → x) (\x → x) (\x → x)

  _orᵣ_ : Option(T) → Option(T) → Option(T)
  _orᵣ_ = or-combine(\x y → y) (\x → x) (\x → x)

  _andₗ_ : Option(T) → Option(T) → Option(T)
  _andₗ_ = and-combine(\x y → x)

  _andᵣ_ : Option(T) → Option(T) → Option(T)
  _andᵣ_ = and-combine(\x y → y)

module Different where
  _orₗ_ : Option(T₁) → Option(T₂) → Option(T₁ ‖ T₂)
  _orₗ_ = or-combine(\x y → Either.Left(x)) Either.Left Either.Right

  _orᵣ_ : Option(T₁) → Option(T₂) → Option(T₁ ‖ T₂)
  _orᵣ_ = or-combine(\x y → Either.Right(y)) Either.Left Either.Right

  _and_ : Option(T₁) → Option(T₂) → Option(T₁ ⨯ T₂)
  _and_ = and-combine(_,_)


text:
------------------------------------------------------------------------
-- Partiality algebra categories
------------------------------------------------------------------------

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

module Partiality-algebra.Category where

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

open import Bijection equality-with-J as Bijection using (_↔_)
open import Category equality-with-J as Category
open import Equality.Path.Isomorphisms.Univalence equality-with-paths
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Structure-identity-principle equality-with-J
open import Univalence-axiom equality-with-J

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

------------------------------------------------------------------------
-- Equality characterisation lemmas for Partiality-algebra-with

abstract

  -- An equality characterisation lemma for Partiality-algebra-with.

  equality-characterisation-Partiality-algebra-with₁ :
    ∀ {a p q} {A : Type a} {T : Type p}
      {P₁ P₂ : Partiality-algebra-with T q A} →
    let module P₁ = Partiality-algebra-with P₁
        module P₂ = Partiality-algebra-with P₂
    in
    (∃ λ (⊑≡⊑ : ∀ x y → (x P₁.⊑ y) ≡ (x P₂.⊑ y)) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡ P₂.⨆ (Σ-map id (≡⇒→ (⊑≡⊑ _ _) ∘_) s))
      ↔
    P₁ ≡ P₂
  equality-characterisation-Partiality-algebra-with₁
    {q = q} {A} {T} {P₁} {P₂} =

    (∃ λ (⊑≡⊑ : ∀ x y → (x P₁.⊑ y) ≡ (x P₂.⊑ y)) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡ P₂.⨆ (Σ-map id (≡⇒→ (⊑≡⊑ _ _) ∘_) s))              ↝⟨ ∃-cong (λ ⊑≡⊑ → ∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ s →
                                                                              ≡⇒↝ _ $ cong (λ (p : {f : ℕ → T} → _) →
                                                                                P₁.⨆ s ≡ P₂.⨆ (Σ-map id p s)) $
                                                                                (implicit-Π-closure ext 1 λ _ →
                                                                                Π-closure          ext 1 λ _ →
                                                                                Π-closure          ext 1 λ _ →
                                                                                P₂.⊑-propositional)
                                                                                (≡⇒→ (⊑≡⊑ _ _) ∘_)
                                                                                (λ {f} → ≡⇒→ (cong (λ _⊑_ → ∀ n → f n ⊑ f (suc n))
                                                                                (⟨ext⟩ (⟨ext⟩ ∘ ⊑≡⊑))))) ⟩
    (∃ λ (⊑≡⊑ : ∀ x y → (x P₁.⊑ y) ≡ (x P₂.⊑ y)) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             P₂.⨆ (Σ-map id
                         (λ {f} →
                            ≡⇒→ (cong (λ _⊑_ → ∀ n → f n ⊑ f (suc n))
                                      (⟨ext⟩ (⟨ext⟩ ∘ ⊑≡⊑))))
                         s))                                             ↝⟨ Σ-cong (∀-cong ext λ _ →
                                                                                Eq.extensionality-isomorphism bad-ext) (λ _ → F.id) ⟩
    (∃ λ (⊑≡⊑ : ∀ x → P₁._⊑_ x ≡ P₂._⊑_ x) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             P₂.⨆ (Σ-map id
                         (λ {f} →
                            ≡⇒→ (cong (λ _⊑_ → ∀ n → f n ⊑ f (suc n))
                                      (⟨ext⟩ ⊑≡⊑)))
                         s))                                             ↝⟨ Σ-cong (Eq.extensionality-isomorphism bad-ext) (λ _ → F.id) ⟩

    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             P₂.⨆ (Σ-map id
                         (λ {f} →
                            ≡⇒→ (cong (λ _⊑_ → ∀ n → f n ⊑ f (suc n))
                                      ⊑≡⊑))
                         s))                                             ↔⟨⟩

    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             P₂.⨆ ( proj₁ s
                  , ≡⇒→ (cong (λ _⊑_ →
                                 ∀ n → proj₁ s n ⊑ proj₁ s (suc n))
                              ⊑≡⊑)
                        (proj₂ s)
                  ))                                                     ↝⟨ ∃-cong (λ ⊑≡⊑ → ∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ →
                                                                              ≡⇒↝ _ $ cong (λ eq → _ ≡ P₂.⨆ (_ , ≡⇒→ eq _)) $ sym $
                                                                                cong-∘ _ _ ⊑≡⊑) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             P₂.⨆ ( proj₁ s
                  , ≡⇒→ (cong (uncurry λ _⊑_ (f : ℕ → T) →
                                         ∀ n → f n ⊑ f (suc n))
                              (cong (_, _) ⊑≡⊑))
                        (proj₂ s)
                  ))                                                     ↝⟨ ∃-cong (λ ⊑≡⊑ → ∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ →
                                                                              ≡⇒↝ _ $ cong (λ inc → _ ≡ P₂.⨆ (_ , inc)) $ sym $
                                                                                subst-in-terms-of-≡⇒↝ equivalence (cong (_, _) ⊑≡⊑) _ _) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             P₂.⨆ ( proj₁ s
                  , subst (uncurry λ _⊑_ (f : ℕ → T) →
                                     ∀ n → f n ⊑ f (suc n))
                          (cong (_, _) ⊑≡⊑)
                          (proj₂ s)
                  ))                                                     ↝⟨ ∃-cong (λ ⊑≡⊑ → ∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ →
                                                                              ≡⇒↝ _ $ cong (λ eq → _ ≡
                                                                                P₂.⨆ (_ , subst (uncurry λ _⊑_ (f : ℕ → T) →
                                                                                ∀ n → f n ⊑ f (suc n))
                                                                                eq _)) $ sym $
                                                                                Σ-≡,≡→≡-subst-const ⊑≡⊑ refl) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             P₂.⨆ ( proj₁ s
                  , subst (uncurry λ _⊑_ (f : ℕ → T) →
                                     ∀ n → f n ⊑ f (suc n))
                          (Σ-≡,≡→≡ ⊑≡⊑ (subst-const ⊑≡⊑))
                          (proj₂ s)
                  ))                                                     ↝⟨ ∃-cong (λ ⊑≡⊑ → ∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ →
                                                                              ≡⇒↝ _ $ cong (λ s → _ ≡ P₂.⨆ s) $ sym $
                                                                                push-subst-pair′ {y≡z = ⊑≡⊑} _ _ (subst-const ⊑≡⊑)) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             P₂.⨆ (subst (λ _⊑_ → ∃ λ f → ∀ n → f n ⊑ f (suc n))
                         ⊑≡⊑ s))                                         ↝⟨ ∃-cong (λ ⊑≡⊑ → ∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ →
                                                                              ≡⇒↝ _ $ cong (λ eq → _ ≡
                                                                                P₂.⨆ (subst (λ _⊑_ → ∃ λ f → ∀ n →
                                                                                f n ⊑ f (suc n)) eq _)) $
                                                                                sym $ sym-sym ⊑≡⊑) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             P₂.⨆ (subst (λ _⊑_ → ∃ λ f → ∀ n → f n ⊑ f (suc n))
                         (sym (sym ⊑≡⊑)) s))                             ↝⟨ ∃-cong (λ ⊑≡⊑ → ∃-cong λ _ → ∃-cong λ _ → ∀-cong ext λ _ →
                                                                              ≡⇒↝ _ $ cong (_ ≡_) $ sym $
                                                                                subst-→-domain _ (sym ⊑≡⊑)) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡
             subst (λ _⊑_ → ∃ (λ f → ∀ n → f n ⊑ f (suc n)) → T)
                   (sym ⊑≡⊑) P₂.⨆ s)                                     ↔⟨ ∃-cong (λ _ → ∃-cong λ _ →
                                                                              Eq.extensionality-isomorphism ext
                                                                                ×-cong
                                                                              Eq.extensionality-isomorphism ext) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       P₁.now ≡ P₂.now
         ×
       P₁.⨆ ≡ subst _ (sym ⊑≡⊑) P₂.⨆)                                    ↝⟨ ∃-cong (λ ⊑≡⊑ → ∃-cong λ _ → ∃-cong λ _ →
                                                                              ≡⇒↝ _ $ elim (λ ⊑≡⊑ → ∀ {⨆₁ ⨆₂} →
                                                                                (⨆₁ ≡ subst _ (sym ⊑≡⊑) ⨆₂) ≡
                                                                                (subst _ ⊑≡⊑ ⨆₁ ≡ ⨆₂))
                                                                                (λ _ → refl) ⊑≡⊑) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       P₁.never ≡ P₂.never
         ×
       P₁.now ≡ P₂.now
         ×
       subst _ ⊑≡⊑ P₁.⨆ ≡ P₂.⨆)                                          ↝⟨ ∃-cong (λ ⊑≡⊑ →
                                                                              ≡⇒↝ _ (cong (_≡ _) $ sym $ subst-const ⊑≡⊑)
                                                                                ×-cong
                                                                              ≡⇒↝ _ (cong (_≡ _) $ sym $ subst-const ⊑≡⊑)
                                                                                ×-cong
                                                                              F.id) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       subst _ ⊑≡⊑ P₁.never ≡ P₂.never
         ×
       subst _ ⊑≡⊑ P₁.now ≡ P₂.now
         ×
       subst _ ⊑≡⊑ P₁.⨆ ≡ P₂.⨆)                                          ↝⟨ ∃-cong (λ _ → ∃-cong λ _ → ≡×≡↔≡) ⟩

    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       subst _ ⊑≡⊑ P₁.never ≡ P₂.never
         ×
       (subst _ ⊑≡⊑ P₁.now , subst _ ⊑≡⊑ P₁.⨆) ≡
       (P₂.now , P₂.⨆))                                                  ↝⟨ ∃-cong (λ _ → ≡×≡↔≡) ⟩

    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       (subst _ ⊑≡⊑ P₁.never , subst _ ⊑≡⊑ P₁.now , subst _ ⊑≡⊑ P₁.⨆) ≡
       (P₂.never , P₂.now , P₂.⨆))                                       ↝⟨ ∃-cong (λ ⊑≡⊑ → ≡⇒↝ _ $ cong (λ x → (subst _ ⊑≡⊑ P₁.never , x) ≡ _) $
                                                                              sym $ push-subst-, {y≡z = ⊑≡⊑} _
                                                                                (λ _⊑_ → (∃ λ f → ∀ n → f n ⊑ f (suc n)) → _)) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       (subst _ ⊑≡⊑ P₁.never , subst _ ⊑≡⊑ (P₁.now , P₁.⨆)) ≡
       (P₂.never , P₂.now , P₂.⨆))                                       ↝⟨ ∃-cong (λ ⊑≡⊑ → ≡⇒↝ _ $ cong (_≡ _) $ sym $
                                                                              push-subst-, {y≡z = ⊑≡⊑} _ _) ⟩
    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       subst _ ⊑≡⊑ (P₁.never , P₁.now , P₁.⨆) ≡
       (P₂.never , P₂.now , P₂.⨆))                                       ↔⟨⟩

    (∃ λ (⊑≡⊑ : P₁._⊑_ ≡ P₂._⊑_) →
       subst _ ⊑≡⊑ (proj₂ (proj₁ (_↔_.to rearrange P₁))) ≡
       proj₂ (proj₁ (_↔_.to rearrange P₂)))                              ↝⟨ Bijection.Σ-≡,≡↔≡ ⟩

    proj₁ (_↔_.to rearrange P₁) ≡ proj₁ (_↔_.to rearrange P₂)            ↝⟨ ignore-propositional-component
                                                                              (×-closure 1 (implicit-Π-closure ext 1 λ _ →
                                                                                implicit-Π-closure ext 1 λ _ →
                                                                                Π-closure ext 1 λ _ →
                                                                                Π-closure ext 1 λ _ →
                                                                                P₂.T-is-set) $
                                                                               ×-closure 1 (H-level-propositional ext 2) $
                                                                               ×-closure 1 (Π-closure ext 1 λ _ →
                                                                                P₂.⊑-propositional) $
                                                                               ×-closure 1 (implicit-Π-closure ext 1 λ _ →
                                                                                implicit-Π-closure ext 1 λ _ →
                                                                                implicit-Π-closure ext 1 λ _ →
                                                                                Π-closure ext 1 λ _ →
                                                                                Π-closure ext 1 λ _ →
                                                                                P₂.⊑-propositional) $
                                                                               ×-closure 1 (Π-closure ext 1 λ _ →
                                                                                P₂.⊑-propositional) $
                                                                               ×-closure 1 (Π-closure ext 1 λ _ →
                                                                                Π-closure ext 1 λ _ →
                                                                                P₂.⊑-propositional) $
                                                                               ×-closure 1 (Π-closure ext 1 λ _ →
                                                                                Π-closure ext 1 λ _ →
                                                                                Π-closure ext 1 λ _ →
                                                                                P₂.⊑-propositional)
                                                                                (implicit-Π-closure ext 1 λ _ →
                                                                                implicit-Π-closure ext 1 λ _ →
                                                                                Is-proposition-propositional ext)) ⟩
    _↔_.to rearrange P₁ ≡ _↔_.to rearrange P₂                            ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ rearrange) ⟩□

    P₁ ≡ P₂                                                              □
    where
    module P₁ = Partiality-algebra-with P₁
    module P₂ = Partiality-algebra-with P₂

    rearrange :
      Partiality-algebra-with T q A
        ↔
      ∃ λ ((_⊑_ , never , _ , ⨆) :
           ∃ λ (_⊑_ : T → T → Type q) →
             T ×
             (A → T) ×
             ((∃ λ (f : ℕ → T) → ∀ n → f n ⊑ f (suc n)) → T)) →
        (∀ {x y} → x ⊑ y → y ⊑ x → x ≡ y)
          ×
        Is-set T
          ×
        (∀ x → x ⊑ x)
          ×
        (∀ {x y z} → x ⊑ y → y ⊑ z → x ⊑ z)
          ×
        (∀ x → never ⊑ x)
          ×
        (∀ s → ∀ n → proj₁ s n ⊑ ⨆ s)
          ×
        (∀ s ub → (∀ n → proj₁ s n ⊑ ub) → ⨆ s ⊑ ub)
          ×
        (∀ {x y} → Is-proposition (x ⊑ y))
    rearrange = record
      { surjection = record
        { logical-equivalence = record
          { to   = λ P → let open Partiality-algebra-with P in
                    ( _⊑_
                    , never
                    , now
                    , ⨆
                    )
                  , antisymmetry
                  , T-is-set-unused
                  , ⊑-refl
                  , ⊑-trans
                  , never⊑
                  , upper-bound
                  , least-upper-bound
                  , ⊑-propositional
          ; from = λ where
              ((LE , ne , n , l) , a , u , r , t , le , ub , lub , p) →
                record
                  { _⊑_               = LE
                  ; never             = ne
                  ; now               = n
                  ; ⨆                 = l
                  ; antisymmetry      = a
                  ; T-is-set-unused   = u
                  ; ⊑-refl            = r
                  ; ⊑-trans           = t
                  ; never⊑            = le
                  ; upper-bound       = ub
                  ; least-upper-bound = lub
                  ; ⊑-propositional   = p
                  }
          }
        ; right-inverse-of = λ _ → refl
        }
      ; left-inverse-of = λ _ → refl
      }

  -- Another equality characterisation lemma for
  -- Partiality-algebra-with.

  equality-characterisation-Partiality-algebra-with₂ :
    ∀ {a p q} {A : Type a} {T : Type p}
      {P₁ P₂ : Partiality-algebra-with T q A} →

    let module P₁ = Partiality-algebra-with P₁
        module P₂ = Partiality-algebra-with P₂
    in
    (∃ λ (⊑⇔⊑ : ∀ x y → x P₁.⊑ y ⇔ x P₂.⊑ y) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡ P₂.⨆ (Σ-map id (_⇔_.to (⊑⇔⊑ _ _) ∘_) s))
      ↔
    P₁ ≡ P₂
  equality-characterisation-Partiality-algebra-with₂
    {q = q} {A} {T} {P₁} {P₂} =

    (∃ λ (⊑⇔⊑ : ∀ x y → x P₁.⊑ y ⇔ x P₂.⊑ y) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡ P₂.⨆ (Σ-map id (_⇔_.to (⊑⇔⊑ _ _) ∘_) s))  ↝⟨ Σ-cong (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                             Eq.⇔↔≃ ext P₁.⊑-propositional P₂.⊑-propositional)
                                                                          (λ _ → F.id) ⟩
    (∃ λ (⊑≃⊑ : ∀ x y → (x P₁.⊑ y) ≃ (x P₂.⊑ y)) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡ P₂.⨆ (Σ-map id (_≃_.to (⊑≃⊑ _ _) ∘_) s))  ↝⟨ inverse $ Σ-cong
                                                                     (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                        ≡≃≃ (_≃_.to
                                                                               (Propositional-extensionality-is-univalence-for-propositions
                                                                                ext)
                                                                               prop-ext
                                                                               P₁.⊑-propositional
                                                                               P₂.⊑-propositional))
                                                                     (λ _ → F.id) ⟩
    (∃ λ (⊑≡⊑ : ∀ x y → (x P₁.⊑ y) ≡ (x P₂.⊑ y)) →
       P₁.never ≡ P₂.never
         ×
       (∀ x → P₁.now x ≡ P₂.now x)
         ×
       ∀ s → P₁.⨆ s ≡ P₂.⨆ (Σ-map id (≡⇒→ (⊑≡⊑ _ _) ∘_) s))     ↝⟨ equality-characterisation-Partiality-algebra-with₁ ⟩□

    P₁ ≡ P₂                                                     □
    where
    module P₁ = Partiality-algebra-with P₁
    module P₂ = Partiality-algebra-with P₂

------------------------------------------------------------------------
-- Partiality algebra categories

-- Partiality algebras (with fixed levels and types) form
-- precategories.

precategory :
  ∀ {a} p q (A : Type a) → Precategory (a ⊔ lsuc (p ⊔ q)) (a ⊔ p ⊔ q)
Precategory.precategory (precategory p q A) =
    Partiality-algebra p q A
  , (λ P Q → Morphism P Q , Morphism-set)
  , PA.id
  , PA._∘_
  , _↔_.to equality-characterisation-Morphism refl
  , _↔_.to equality-characterisation-Morphism refl
  , _↔_.to equality-characterisation-Morphism refl

-- A "standard notion of structure" built using
-- Partiality-algebra-with.

standard-notion-of-structure :
  ∀ {a} p q (A : Type a) →
  Standard-notion-of-structure _ _ (precategory-Set p ext)
standard-notion-of-structure p q A = record
  { P               = λ B → Partiality-algebra-with (proj₁ B) q A
  ; H               = Is-morphism-with
  ; H-prop          = λ { {p = P} {q = Q} _ →
                          Is-morphism-with-propositional P Q
                        }
  ; H-id            = λ { {p = P} →
                          proj₂ $
                            _↔_.to Morphism↔Morphism-as-Σ
                              (PA.id {P = ⟨ P ⟩})
                        }
  ; H-∘             = λ { {p = P} {q = Q} {r = R}
                          f-morphism g-morphism →
                          proj₂ $
                            _↔_.to Morphism↔Morphism-as-Σ
                              (_↔_.from
                                 (Morphism↔Morphism-as-Σ
                                    {P₁ = ⟨ Q ⟩} {P₂ = ⟨ R ⟩})
                                 (_ , g-morphism)
                                 PA.∘
                               _↔_.from
                                 (Morphism↔Morphism-as-Σ {P₁ = ⟨ P ⟩})
                                 (_ , f-morphism))
                        }
  ; H-antisymmetric = λ P Q id-morphism-P→Q id-morphism-Q→P →
      _↔_.to
        (equality-characterisation-Partiality-algebra-with₂)
        ( (λ x y → record { to   = proj₁ id-morphism-P→Q
                          ; from = proj₁ id-morphism-Q→P
                          })
        , proj₁ (proj₂ id-morphism-P→Q)
        , proj₁ (proj₂ (proj₂ id-morphism-P→Q))
        , proj₂ (proj₂ (proj₂ id-morphism-P→Q))
        )
  }

abstract

  -- The precategory obtained from the standard notion of structure is
  -- equal to the direct definition above.

  precategories-equal :
    ∀ {a p q} {A : Type a} →
    Standard-notion-of-structure.Str
      (standard-notion-of-structure p q A)
      ≡
    precategory p q A
  precategories-equal {p = p} {q} {A} =
    _↔_.to (equality-characterisation-Precategory ext univ univ)
      ( ≃Partiality-algebra
      , (λ _ _ → Eq.↔⇒≃ $ inverse $ Morphism↔Morphism-as-Σ)
      , (λ _ → refl)
      , (λ _ _ _ _ _ → refl)
      )
    where
    ≃Partiality-algebra :
      (∃ λ (T : Set p) → Partiality-algebra-with (proj₁ T) q A)
        ≃
      Partiality-algebra p q A
    ≃Partiality-algebra =
      (∃ λ (T : Set p) → Partiality-algebra-with (proj₁ T) q A)  ↔⟨ inverse Σ-assoc ⟩

      (∃ λ (T : Type p) →
         Is-set T × Partiality-algebra-with T q A)               ↔⟨ ∃-cong (λ _ → drop-⊤-left-× λ P → _⇔_.to contractible⇔↔⊤ $
                                                                      propositional⇒inhabited⇒contractible
                                                                        (H-level-propositional ext 2)
                                                                        (Partiality-algebra-with.T-is-set P)) ⟩
      (∃ λ (T : Type p) → Partiality-algebra-with T q A)         ↝⟨ Eq.↔⇒≃ record
                                                                      { surjection = record
                                                                        { logical-equivalence = record
                                                                          { to   = uncurry λ _ P → ⟨ P ⟩
                                                                          ; from = λ P → T P , partiality-algebra-with P
                                                                          }
                                                                        ; right-inverse-of = λ _ → refl
                                                                        }
                                                                      ; left-inverse-of = λ _ → refl
                                                                      } ⟩□
      Partiality-algebra p q A                                   □
      where
      open Partiality-algebra

-- Thus the precategory is a category.

category :
  ∀ {a} p q (A : Type a) →
  Category (a ⊔ lsuc (p ⊔ q)) (a ⊔ p ⊔ q)
Category.category (category p q A) =
    precategory _ _ A
  , subst (λ C → ∀ {P Q} → Eq.Is-equivalence
                             (Precategory.≡→≅ C {P} {Q}))
          precategories-equal
          (structure-identity-principle
             ext
             (category-Set _ ext (λ _ _ → univ))
             (standard-notion-of-structure p q A))

private

  precategory-category :
    ∀ {a p q} {A : Type a} →
    Category.precategory (category p q A) ≡ precategory p q A
  precategory-category = refl

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Agda.Builtin.Sigma

infix -100 This:_ this:_
data This:_ {a} {A : Set a} : A → Set where
  this:_ : ∀ x → This: x

macro
  runT : Tactic → Tactic
  runT m = m

  evalT : ∀ {a} {A : Set a} → TC A → Tactic
  evalT m hole = m >>= quoteTC >>= unify hole

-- The context on the rhs of each of the two functions below is the same, a single String

Γ : Telescope
Γ = ("s" , vArg (def (quote String) [])) ∷ []

context-Γ₀ : String → This: Γ
context-Γ₀ s = this: evalT getContext

module _ (S : String) where
  Γ' : Telescope
  Γ' = ("S" , vArg (def (quote String) [])) ∷ []

  context-Γ₁ : This: Γ'
  context-Γ₁ = this: evalT getContext

downMap : {A : Set} → (Nat → A) → Nat → List A
downMap f zero    = []
downMap f (suc n) = f n ∷ downMap f n

f-type : Term
f-type = def (quote String) []

f-tel : Nat → List (Σ String λ _ → Arg Type)
f-tel n = downMap (λ _ → "_" , vArg unknown) n

f-pats : Nat → List (Arg Pattern)
f-pats n = downMap (λ x → vArg (var x)) n

f-term : Nat → Term
f-term n = var n []

defineFresh : Nat → Nat → TC QName
defineFresh #pats #term =
  freshName "f" >>= λ f →
  define (vArg f) (funDef f-type (clause (f-tel #pats) (f-pats #pats) (f-term #term) ∷ [])) >>= λ _ →
  returnTC f

freshFun : Nat → Nat → TC Bool
freshFun #pats #term =
  catchTC (defineFresh #pats #term >>= λ _ → returnTC true)
          (returnTC false)

-- Check that the pattern list must be of length 0
-- and the context features 1 available variable.

define-Γ₀-0-0 : String → This: true
define-Γ₀-0-0 s = this: evalT (freshFun 0 0)

define-Γ₀-1-0 : String → This: false
define-Γ₀-1-0 s = this: evalT (freshFun 1 0)

define-Γ₀-1-1 : String → This: false
define-Γ₀-1-1 s = this: evalT (freshFun 0 1)

module _ (S : String) where
  define-Γ₁-0-0 : This: true
  define-Γ₁-0-0 = this: evalT (freshFun 0 0)

  define-Γ₁-0-1 : This: false
  define-Γ₁-0-1 = this: evalT (freshFun 0 1)

  define-Γ₁-1-0 : This: false
  define-Γ₁-1-0 = this: evalT (freshFun 1 0)

f₀ : String → String
f₀ s = runT λ hole → defineFresh 0 0 >>= λ f → unify hole (def f [])

f₁ : String → String
f₁ = λ s → runT λ hole → defineFresh 0 0 >>= λ f → unify hole (def f [])

f₂ : String → String
f₂ s = runT λ hole → defineFresh 0 0 >>= λ f → unify hole (def f [])
  where x = 0


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

-- The 'original' version of Lawvere Theory, based on
-- Nat^op and IOO functors. Contrast with the weak version at
-- https://ncatlab.org/nlab/show/Lawvere+theory
-- Unfortunately, many results on the weak version are not in
-- the literature, so doing that development would be new research.

module Categories.Theory.Lawvere where

open import Data.Nat using (ℕ)
open import Level

open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
import Categories.Category.Core as Cat
open import Categories.Category.Instance.Nat using (Nat; Natop-Cartesian)
open import Categories.Category.Instance.Setoids
open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-CartesianCategory)
open import Categories.Category.Unbundled using (Category)
open import Categories.Category.Unbundled.Properties using (pack′; unpack′)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Cartesian
open import Categories.Functor.Cartesian.Properties
open import Categories.Functor.IdentityOnObjects

private
  variable
    ℓ e o′ ℓ′ e′ ℓ″ e″ : Level

record LawvereTheory (ℓ e : Level) : Set (suc (ℓ ⊔ e)) where
  private
    𝒩 = Cat.Category.op Nat
  field
    L : Category ℕ ℓ e
  L′ : Cat.Category 0ℓ ℓ e
  L′ = pack′ L
  field
    T : Cartesian L′
  CartT : CartesianCategory 0ℓ ℓ e
  CartT = record { U = L′ ; cartesian = T }
  field
    I : IdentityOnObjects (unpack′ 𝒩) L
    CartF : IsCartesianF Natop-Cartesian CartT (IOO⇒Functor I)

record LT-Hom (T₁ : LawvereTheory ℓ e) (T₂ : LawvereTheory ℓ′ e′) : Set (ℓ ⊔ e ⊔ ℓ′ ⊔ e′) where
  private
    module T₁ = LawvereTheory T₁
    module T₂ = LawvereTheory T₂

  field
    cartF : CartesianF T₁.CartT T₂.CartT

  module cartF = CartesianF cartF using (F)

LT-id : {A : LawvereTheory ℓ e} → LT-Hom A A
LT-id = record { cartF = idF-CartesianF _ }

LT-∘ : {A : LawvereTheory ℓ e} {B : LawvereTheory ℓ′ e′} {C : LawvereTheory ℓ″ e″} →
       LT-Hom B C → LT-Hom A B → LT-Hom A C
LT-∘ G H = record { cartF = ∘-CartesianF (cartF G) (cartF H) }
  where open LT-Hom

-- A 'Model' will be taken to be in Setoids.
record Model (LT : LawvereTheory ℓ e) : Set (ℓ ⊔ e ⊔ suc (ℓ′ ⊔ e′)) where
  private
    module LT = LawvereTheory LT
  field
    cartF : CartesianF LT.CartT (Setoids-CartesianCategory ℓ′ e′)

  module cartF = CartesianF cartF

  mod : Functor LT.L′ (Setoids ℓ′ e′)
  mod = cartF.F

-- But we can have more general models 'in' a cartesian category
record ModelsOf_In_ (LT : LawvereTheory ℓ e) (𝒞 : CartesianCategory o′ ℓ′ e′) : Set (ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module LT = LawvereTheory LT using (L′; CartT)
    module CC = CartesianCategory 𝒞 using (U)
  field
    cartF : CartesianF LT.CartT 𝒞

  mod : Functor LT.L′ CC.U
  mod = CartesianF.F cartF

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module Magma where

open import Magma.Bundles public
open import Magma.Structures public
open import Magma.Definitions public


text:
-- Andreas, 2015-02-24, issue reported by g.x.allais
-- {-# OPTIONS -v interaction.give:100 #-}

record R : Set1 where
  field
    -v : Set

goal : R
goal = {!!}

-- refine here
-- WAS: error due to rendering or record as
--   record {-v = ?}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

ℤ is a Commutative Ring (using QuoInt)

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Instances.QuoInt where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing
open import Cubical.Data.Nat  using (ℕ ; zero ; suc)
open import Cubical.Data.Bool using (not)
open import Cubical.Data.Int.MoreInts.QuoInt
  renaming (ℤ to ℤType ; _+_ to _+ℤ_; _·_ to _·ℤ_; -_ to -ℤ_)

open CommRingStr

-- The missing additive inversion

+InvL' : ∀ n s → signed (not s) n +ℤ signed s n ≡ signed s zero
+InvL' zero _ = refl
+InvL' (suc n) spos = predℤ-+ʳ (neg n) (pos (suc n)) ∙ (λ i → neg n +ℤ predSucℤ (pos n) i) ∙ +InvL' n spos
+InvL' (suc n) sneg = sucℤ-+ʳ  (pos n) (neg (suc n)) ∙ (λ i → pos n +ℤ sucPredℤ (neg n) i) ∙ +InvL' n sneg

+InvL : (n : ℤType) → (-ℤ n) +ℤ n ≡ 0
+InvL (signed spos n) = +InvL' n spos
+InvL (signed sneg n) = +InvL' n sneg ∙ sym posneg
+InvL (posneg i) j =
  hcomp (λ k → λ
    { (i = i0) → 0
    ; (i = i1) → compPath-filler refl (sym posneg) k j
    ; (j = i0) → posneg i
    ; (j = i1) → posneg (i ∧ ~ k) })
  (posneg i)

+InvR : (n : ℤType) → n +ℤ (-ℤ n) ≡ 0
+InvR n = +-comm n (-ℤ n) ∙ +InvL n

ℤCommRing : CommRing ℓ-zero
ℤCommRing .fst = ℤType
ℤCommRing .snd .0r = 0
ℤCommRing .snd .1r = 1
ℤCommRing .snd ._+_ = _+ℤ_
ℤCommRing .snd ._·_ = _·ℤ_
ℤCommRing .snd .-_ = -ℤ_
ℤCommRing .snd .isCommRing = isCommRingℤ
  where
  abstract
    isCommRingℤ : IsCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_
    isCommRingℤ = makeIsCommRing
      isSetℤ +-assoc (+-zeroʳ _)
      +InvR +-comm ·-assoc
      ·-identityʳ (λ x y z → sym (·-distribˡ x y z)) ·-comm

max_stars_repo_name: gmagaf/cubical

max_issues_repo_name: gmagaf/cubical

max_forks_repo_name: gmagaf/cubical


text:
-- Intuitionistic propositional calculus.
-- Common syntax.

module IPC.Syntax.Common where

open import Common.Context public

-- Types, or propositions.

infixl 9 _∧_
infixl 8 _∨_
infixr 7 _▻_
data Ty : Set where
  α_  : Atom → Ty
  _▻_ : Ty → Ty → Ty
  _∧_ : Ty → Ty → Ty
  ⊤  : Ty
  ⊥  : Ty
  _∨_ : Ty → Ty → Ty

-- Additional useful types.

¬_ : Ty → Ty
¬ A = A ▻ ⊥

infix 7 _▻◅_
_▻◅_ : Ty → Ty → Ty
A ▻◅ B = (A ▻ B) ∧ (B ▻ A)

infixr 7 _▻⋯▻_
_▻⋯▻_ : Cx Ty → Ty → Ty
∅       ▻⋯▻ B = B
(Ξ , A) ▻⋯▻ B = Ξ ▻⋯▻ (A ▻ B)

infixr 7 _▻⋯▻⋆_
_▻⋯▻⋆_ : Cx Ty → Cx Ty → Ty
Γ ▻⋯▻⋆ ∅       = ⊤
Γ ▻⋯▻⋆ (Ξ , A) = (Γ ▻⋯▻⋆ Ξ) ∧ (Γ ▻⋯▻ A)

-- Inversion principles.

invα : ∀ {P P′} → α P ≡ α P′ → P ≡ P′
invα refl = refl

inv▻₁ : ∀ {A A′ B B′} → A ▻ B ≡ A′ ▻ B′ → A ≡ A′
inv▻₁ refl = refl

inv▻₂ : ∀ {A A′ B B′} → A ▻ B ≡ A′ ▻ B′ → B ≡ B′
inv▻₂ refl = refl

inv∧₁ : ∀ {A A′ B B′} → A ∧ B ≡ A′ ∧ B′ → A ≡ A′
inv∧₁ refl = refl

inv∧₂ : ∀ {A A′ B B′} → A ∧ B ≡ A′ ∧ B′ → B ≡ B′
inv∧₂ refl = refl

inv∨₁ : ∀ {A A′ B B′} → A ∨ B ≡ A′ ∨ B′ → A ≡ A′
inv∨₁ refl = refl

inv∨₂ : ∀ {A A′ B B′} → A ∨ B ≡ A′ ∨ B′ → B ≡ B′
inv∨₂ refl = refl

-- Decidable equality on types.

_≟ᵀ_ : (A A′ : Ty) → Dec (A ≡ A′)
(α P)   ≟ᵀ (α P′)    with P ≟ᵅ P′
(α P)   ≟ᵀ (α .P)    | yes refl = yes refl
(α P)   ≟ᵀ (α P′)    | no  P≢P′ = no (P≢P′ ∘ invα)
(α P)   ≟ᵀ (A′ ▻ B′) = no λ ()
(α P)   ≟ᵀ (A′ ∧ B′) = no λ ()
(α P)   ≟ᵀ ⊤        = no λ ()
(α P)   ≟ᵀ ⊥        = no λ ()
(α P)   ≟ᵀ (A′ ∨ B′) = no λ ()
(A ▻ B) ≟ᵀ (α P′)    = no λ ()
(A ▻ B) ≟ᵀ (A′ ▻ B′) with A ≟ᵀ A′ | B ≟ᵀ B′
(A ▻ B) ≟ᵀ (.A ▻ .B) | yes refl | yes refl = yes refl
(A ▻ B) ≟ᵀ (A′ ▻ B′) | no  A≢A′ | _        = no (A≢A′ ∘ inv▻₁)
(A ▻ B) ≟ᵀ (A′ ▻ B′) | _        | no  B≢B′ = no (B≢B′ ∘ inv▻₂)
(A ▻ B) ≟ᵀ (A′ ∧ B′) = no λ ()
(A ▻ B) ≟ᵀ ⊤        = no λ ()
(A ▻ B) ≟ᵀ ⊥        = no λ ()
(A ▻ B) ≟ᵀ (A′ ∨ B′) = no λ ()
(A ∧ B) ≟ᵀ (α P′)    = no λ ()
(A ∧ B) ≟ᵀ (A′ ▻ B′) = no λ ()
(A ∧ B) ≟ᵀ (A′ ∧ B′) with A ≟ᵀ A′ | B ≟ᵀ B′
(A ∧ B) ≟ᵀ (.A ∧ .B) | yes refl | yes refl = yes refl
(A ∧ B) ≟ᵀ (A′ ∧ B′) | no  A≢A′ | _        = no (A≢A′ ∘ inv∧₁)
(A ∧ B) ≟ᵀ (A′ ∧ B′) | _        | no  B≢B′ = no (B≢B′ ∘ inv∧₂)
(A ∧ B) ≟ᵀ ⊤        = no λ ()
(A ∧ B) ≟ᵀ ⊥        = no λ ()
(A ∧ B) ≟ᵀ (A′ ∨ B′) = no λ ()
⊤      ≟ᵀ (α P′)    = no λ ()
⊤      ≟ᵀ (A′ ▻ B′) = no λ ()
⊤      ≟ᵀ (A′ ∧ B′) = no λ ()
⊤      ≟ᵀ ⊤        = yes refl
⊤      ≟ᵀ ⊥        = no λ ()
⊤      ≟ᵀ (A′ ∨ B′) = no λ ()
⊥      ≟ᵀ (α P′)    = no λ ()
⊥      ≟ᵀ (A′ ▻ B′) = no λ ()
⊥      ≟ᵀ (A′ ∧ B′) = no λ ()
⊥      ≟ᵀ ⊤        = no λ ()
⊥      ≟ᵀ ⊥        = yes refl
⊥      ≟ᵀ (A′ ∨ B′) = no λ ()
(A ∨ B) ≟ᵀ (α P′)    = no λ ()
(A ∨ B) ≟ᵀ (A′ ▻ B′) = no λ ()
(A ∨ B) ≟ᵀ (A′ ∧ B′) = no λ ()
(A ∨ B) ≟ᵀ ⊤        = no λ ()
(A ∨ B) ≟ᵀ ⊥        = no λ ()
(A ∨ B) ≟ᵀ (A′ ∨ B′) with A ≟ᵀ A′ | B ≟ᵀ B′
(A ∨ B) ≟ᵀ (.A ∨ .B) | yes refl | yes refl = yes refl
(A ∨ B) ≟ᵀ (A′ ∨ B′) | no  A≢A′ | _        = no (A≢A′ ∘ inv∨₁)
(A ∨ B) ≟ᵀ (A′ ∨ B′) | _        | no  B≢B′ = no (B≢B′ ∘ inv∨₂)

open ContextEquality (_≟ᵀ_) public

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

module CoSig where

open import Data.Product as Prod
open import Data.Fin
open import Data.Unit
open import Data.Empty
open import Data.Sum
open import Data.Nat
open import Size
open import Function
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)

---- We don't use dependencies for now.

-- record CoSigDep (I : Set) : Set₁ where
--   field
--     ∥_∥ : I → Set
--     coar : {i : I} → ∥_∥ i → Set
--     sel : {i : I} (d : ∥_∥ i) → coar d → I
-- open CoSigDep public

-- Fam : Set → Set₁
-- Fam I = I → Set

-- -- | Extension of co-signature Δ, on objects
-- ⟪_⟫ : ∀{I} → CoSigDep I → Fam I → Fam I
-- ⟪ Δ ⟫ X i = (d : ∥ Δ ∥ i) → Σ[ u ∈ coar Δ d ] (X (sel Δ d u))

record CoSig : Set₁ where
  field
    ∥_∥ : Set
    coar : ∥_∥ → Set
open CoSig public

-- | Extension of co-signature Δ, on objects
⟪_⟫ : CoSig → Set → Set
--⟪ Δ ⟫ X = (d : ∥ Δ ∥) → Σ[ u ∈ coar Δ d ] X
⟪ Δ ⟫ X = (d : ∥ Δ ∥) → (coar Δ d) × X

-- | Extension of signature Σ, on morphisms
⟪_⟫₁ : (Δ : CoSig) {A B : Set} → (A → B) → ⟪ Δ ⟫ A → ⟪ Δ ⟫ B
⟪ Δ ⟫₁ f o d = Prod.map id f (o d)

-- | Lift ⟪ Δ ⟫ to relations
cosig-lift : {Δ : CoSig} {X : Set} (R : X → X → Set) (o₁ o₂ : ⟪ Δ ⟫ X) → Set
cosig-lift {Δ} _R_ o₁ o₂ =
  ∀ d → proj₁ (o₁ d) ≡ proj₁ (o₂ d) ×
        proj₂ (o₁ d) R proj₂ (o₂ d)

record CoSig-FP (Δ : CoSig) : Set where
  coinductive
  field destr : ⟪ Δ ⟫ (CoSig-FP Δ)
open CoSig-FP public

record Str {i : Size} (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    hd : A
    tl : ∀ {j : Size< i} → Str {j} A
open Str public

--- Example: Streams
Str-CoSig : Set → CoSig
Str-CoSig A = record
  { ∥_∥ = ⊤
  ; coar = λ _ → A
  }

Str' : Set → Set
Str' A = CoSig-FP (Str-CoSig A)

-- We can indeed extract a stream from stream implemented through cosignatures.
Str'-Str : ∀{A} → Str' A → Str A
hd (Str'-Str s) = proj₁ (destr s tt)
tl (Str'-Str s) = Str'-Str (proj₂ (destr s tt))

-- Example: Mealy machines
MM-CoSig : Set → Set → CoSig
MM-CoSig I O = record
  { ∥_∥ = I
  ; coar = λ _ → O
  }

MM : Set → Set → Set
MM I O = CoSig-FP (MM-CoSig I O)

-- Such a Mealy machine gives rise to a causal stream transformation.
MM-Causal : ∀{I O} → MM I O → ∀{i} → Str {i} I → Str {i} O
hd (MM-Causal m s) = proj₁ (destr m (hd s))
tl (MM-Causal m s) = MM-Causal (proj₂ (destr m (hd s))) (tl s)

--- Not quite Example: Streams with stop button
BStr-CoSig : Set → CoSig
BStr-CoSig A = record
  { ∥_∥ = ⊥ ⊎ ⊤
  ; coar = BStr-CoSig-coar
  }
  where
    BStr-CoSig-coar : ⊥ ⊎ ⊤ → Set
    BStr-CoSig-coar (inj₁ x) = ⊥-elim x
    BStr-CoSig-coar (inj₂ y) = A

BStr : Set → Set
BStr A = CoSig-FP (BStr-CoSig A)

st-ones : BStr ℕ
destr st-ones (inj₁ x) = ⊥-elim x
destr st-ones (inj₂ x) = (1 , st-ones)

-- Claim: This way of definining streams with a "stop button" renders
-- the button unusable. Thus, we only get streams back.
BStr-Str : ∀{A} → BStr A → Str A
hd (BStr-Str s) = proj₁ (destr s (inj₂ tt))
tl (BStr-Str s) = BStr-Str (proj₂ (destr s (inj₂ tt)))

Str-BStr : ∀{A} → Str A → BStr A
destr (Str-BStr s) (inj₁ x) = ⊥-elim x
destr (Str-BStr s) (inj₂ y) = (hd s , Str-BStr (tl s))

--- Example: Streams with stop button
BStr'-CoSig : Set → CoSig
BStr'-CoSig A = record
  { ∥_∥ = ⊤ ⊎ ⊤
  ; coar = BStr-CoSig-coar
  }
  where
    BStr-CoSig-coar : ⊤ ⊎ ⊤ → Set
    BStr-CoSig-coar (inj₁ x) = ⊥
    BStr-CoSig-coar (inj₂ y) = A

BStr' : Set → Set
BStr' A = CoSig-FP (BStr'-CoSig A)

-- Claim: This way of defining streams with a stop button makes any
-- such stream undefinable. Thus, the fixed point is trivial.
BStr'-triv : ∀{A} → BStr' A → ⊥
BStr'-triv s = proj₁ (destr s (inj₁ tt))

-- An extension of cosignatures that allow us to give a continuation
-- for the following states. This enables us to specify systems with,
-- for example, termination.
record CoSig₂ : Set₁ where
  field
    ∥_∥₂ : Set
    coar₂ : ∥_∥₂ → Set
    cont :  ∥_∥₂ → Set
open CoSig₂ public

-- | Extension of co-signature Δ, on objects
⟪_⟫₂ : CoSig₂ → Set → Set
⟪ Δ ⟫₂ X = (d : ∥ Δ ∥₂) → (coar₂ Δ d) × (cont Δ d → X)

record CoSig₂-FP (Δ : CoSig₂) : Set where
  coinductive
  field destr₂ : ⟪ Δ ⟫₂ (CoSig₂-FP Δ)
open CoSig₂-FP public

--- Example: Streams with stop button
BStr-CoSig₂ : Set → CoSig₂
BStr-CoSig₂ A = record
  { ∥_∥₂ = ⊤ ⊎ ⊤
  ; coar₂ = BStr-CoSig-coar
  ; cont = BStr-CoSig-cont
  }
  where
    BStr-CoSig-coar : ⊤ ⊎ ⊤ → Set
    BStr-CoSig-coar (inj₁ x) = ⊤
    BStr-CoSig-coar (inj₂ y) = A

    BStr-CoSig-cont : ⊤ ⊎ ⊤ → Set
    BStr-CoSig-cont (inj₁ x) = ⊥
    BStr-CoSig-cont (inj₂ y) = ⊤

BStr₂ : Set → Set
BStr₂ A = CoSig₂-FP (BStr-CoSig₂ A)

st-ones₂ : BStr₂ ℕ
destr₂ st-ones₂ (inj₁ tt) = (tt , ⊥-elim)
destr₂ st-ones₂ (inj₂ tt) = (1 , (λ _ → st-ones₂))

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

open import Categories.Category
open import Categories.Functor.Bifunctor

module Categories.Diagram.End {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where

private
  module C = Category C
  module D = Category D
  open D
  open HomReasoning
  variable
    A B : Obj
    f g : A ⇒ B

open import Level
open import Data.Product using (Σ; _,_)

open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation.Dinatural
open import Categories.Morphism.Reasoning D

open Functor F

record Wedge : Set (levelOfTerm F) where
  field
    E         : Obj
    dinatural : DinaturalTransformation (const E) F

  module dinatural = DinaturalTransformation dinatural

Wedge-∘ : (W : Wedge) → A ⇒ Wedge.E W → Wedge
Wedge-∘ {A = A} W f = record
  { E         = A
  ; dinatural = extranaturalʳ (λ X → dinatural.α X ∘ f)
                              (⟺ assoc ○ ∘-resp-≈ˡ (extranatural-commʳ dinatural) ○ assoc )
  }
  where open Wedge W

record End : Set (levelOfTerm F) where
  field
    wedge : Wedge

  module wedge = Wedge wedge
  open wedge public
  open Wedge

  field
    factor    : (W : Wedge) → E W ⇒ wedge.E
    universal : ∀ {W : Wedge} {A} → wedge.dinatural.α A ∘ factor W ≈ dinatural.α W A
    unique    : ∀ {W : Wedge} {g : E W ⇒ wedge.E} → (∀ {A} → wedge.dinatural.α A ∘ g ≈ dinatural.α W A) → factor W ≈ g

  η-id : factor wedge ≈ D.id
  η-id = unique identityʳ

  unique′ :(∀ {A} → wedge.dinatural.α A ∘ f ≈ wedge.dinatural.α A ∘ g) → f ≈ g
  unique′ {f = f} {g = g} eq = ⟺ (unique {W = Wedge-∘ wedge f} refl) ○ unique (⟺ eq)

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


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

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

open import LibraBFT.ImplShared.Consensus.Types

module LibraBFT.Impl.IO.OBM.ObmNeedFetch where

{-
The functions in this module are used when a node needs to catchup.

TODO-3: model catchup request/response in Agda.

In haskell, for each message received from the network (including messages to self),
each message is processed in a single thread that completes the processing
before then processing a subsequent message.

However, a node detects that it needs to catchup "in the middle" of that processing.
In Haskell we use unsafePerformIO to send a network request to other nodes asking
for "catchup" data.

The responses are received by a different thread that then feeds them to the waiting thread,
which then proceeds.
-}

postulate -- TODO-3: writeRequestReadResponseUNSAFE
  writeRequestReadResponseUNSAFE
    : ObmNeedFetch → Author → Author → BlockRetrievalRequest
    → BlockRetrievalResponse


text:
{- PROOF OF BOUNDING THEOREM -}

open import Preliminaries
open import Source
open import Complexity
open import Translation
open import Bounding-Lemmas

module Bounding where

  boundingRec : ∀ {τ} (v : [] Source.|- nat) (val-v : val v)
                      (e0 : [] Source.|- τ)
                      (e1 : (nat :: susp τ :: []) Source.|- τ)
                      (E : [] Complexity.|- nat)
                      (E0 : [] Complexity.|- || τ ||)
                      (E1 : (nat :: || τ || :: []) Complexity.|- || τ ||)
              → valBound v val-v E → expBound e0 E0
              → ((v' : [] Source.|- nat) (val-v' : val v') (E' :  [] Complexity.|- nat) → valBound v' val-v' E'
                → (r : [] Source.|- susp τ) (val-r : val r) (R :  [] Complexity.|- || τ ||) → valBound r val-r R
                → expBound (Source.subst e1 (Source.lem4 v' r)) (Complexity.subst E1 (Complexity.lem4 E' R)))
              → ((vbranch : [] Source.|- τ) (val-vbranch : val vbranch) (nbranch : Cost)
              → evals-rec-branch e0 e1 v vbranch nbranch
              → (plusC 1C (interp-Cost nbranch) ≤s l-proj (rec E (1C +C E0) (1C +C E1))
                × (valBound vbranch val-vbranch (r-proj (rec E (1C +C E0) (1C +C E1))))))
  boundingRec .z z-isval e0 e1 E E0 E1 vbound e0bound e1bound vbranch val-vbranch nbranch (evals-rec-z evals-branch) =
    (cong-+ refl-s (fst usee0bound ) trans l-proj-s) trans cong-lproj (rec-steps-z trans cong-rec vbound) ,
    weakeningVal' val-vbranch (snd usee0bound) (r-proj-s trans cong-rproj (rec-steps-z trans (cong-rec (vbound))))
    where usee0bound = (e0bound vbranch val-vbranch nbranch evals-branch)
  boundingRec .(suc v') (suc-isval v' val-v') e0 e1 E E0 E1 (E' , v'bound , sucE'≤E) e0bound e1bound vbranch val-vbranch nbranch (evals-rec-s evals-branch) =
    (cong-+ refl-s (fst usee1bound) trans l-proj-s) trans cong-lproj (rec-steps-s trans cong-rec sucE'≤E) ,
    weakeningVal' val-vbranch (snd usee1bound) (r-proj-s trans cong-rproj (rec-steps-s trans cong-rec sucE'≤E)) where
      IH = boundingRec v' val-v' e0 e1 E' E0 E1 v'bound e0bound e1bound
      usee1bound = e1bound v' val-v' E' v'bound
                         (delay (rec v' e0 e1)) (delay-isval _) (rec E' (1C +C E0) (1C +C E1) )
                         (λ { vr vvr ._ (rec-evals{n1 = n1} {n2 = n2} D D') →
                           let useIH = IH vr vvr n2 (transport (λ H → evals-rec-branch e0 e1 H vr n2) (! (fst (val-evals-inversion val-v' D))) D')
                            in (cong-+ (Eq0C-≤0 (snd (val-evals-inversion val-v' D))) refl-s trans +-unit-l) trans fst useIH , snd useIH } )
                         vbranch val-vbranch nbranch evals-branch

  boundingListRec : ∀ {τ τ'} (v : [] Source.|- list τ') (vv : val v)
                             (e0 : [] Source.|- τ)
                             (e1 : τ' :: list τ' :: susp τ :: [] Source.|- τ)
                             (E : [] Complexity.|- list ⟨⟨ τ' ⟩⟩)
                             (E0 : [] Complexity.|- || τ ||)
                             (E1 : ⟨⟨ τ' ⟩⟩ :: list ⟨⟨ τ' ⟩⟩ :: || τ || :: [] Complexity.|- || τ ||)
                             → valBound v vv E → expBound e0 E0
                             → ((h' : []  Source.|- τ') (vh' : val h') (H' : [] Complexity.|- ⟨⟨ τ' ⟩⟩)
                               → valBound h' vh' H'
                               → (v' : [] Source.|- list τ') (vv' : val v') (V' : [] Complexity.|- list ⟨⟨ τ' ⟩⟩)
                               → valBound v' vv' V'
                               → (r : [] Source.|- susp τ) (vr : val r) (R : [] Complexity.|- || τ ||)
                               → valBound r vr R
                               → expBound (Source.subst e1 (Source.lem5 h' v' r)) (Complexity.subst E1 (Complexity.lem5 H' V' R)))
                             → (vbranch : [] Source.|- τ)  (vvbranch : val vbranch) (nbranch : Cost)
                             → evals-listrec-branch e0 e1 v vbranch nbranch
                             → plusC 1C (interp-Cost nbranch) ≤s l-proj (listrec E (1C +C E0) (1C +C E1))
                               × valBound vbranch vvbranch (r-proj (listrec E (1C +C E0) (1C +C E1)))
  boundingListRec .nil nil-isval e0 e1 E E0 E1 vbv e0b e1b vbranch vvbranch n (evals-listrec-nil evals-branch) =
    ((cong-+ refl-s (fst usee0bound) trans l-proj-s) trans cong-lproj (listrec-steps-nil trans cong-listrec vbv)) ,
    weakeningVal' vvbranch (snd usee0bound) (r-proj-s trans cong-rproj (listrec-steps-nil trans cong-listrec vbv))
    where usee0bound = e0b vbranch vvbranch n evals-branch
  boundingListRec .(x ::s xs) (cons-isval x xs vv vv₁) e0 e1 E E0 E1 (h' , t' , (vbxh' , vbxst') , h'::t'≤sE)
    e0b e1b vbranch vvbranch nbranch (evals-listrec-cons evals-branch) =
      (cong-+ refl-s (fst usee1bound) trans l-proj-s) trans cong-lproj (listrec-steps-cons trans cong-listrec h'::t'≤sE) ,
      weakeningVal' vvbranch (snd usee1bound) (r-proj-s trans cong-rproj (listrec-steps-cons trans cong-listrec h'::t'≤sE))
      where
        IH = boundingListRec xs vv₁ e0 e1 t' E0 E1 vbxst' e0b e1b
        usee1bound = e1b x vv h' vbxh' xs vv₁ t' vbxst'
                     (delay (listrec xs e0 e1)) (delay-isval _) (listrec t' (1C +C E0) (1C +C E1))
                     (λ { vr vvr ._ (listrec-evals {_} {n2} D D') →
                     let useIH = IH vr vvr n2 (transport (λ H → evals-listrec-branch e0 e1 H vr n2) (! (fst (val-evals-inversion vv₁ D))) D')
                     in (cong-+ (Eq0C-≤0 (snd (val-evals-inversion vv₁ D))) refl-s trans +-unit-l) trans fst useIH , snd useIH } )
                     vbranch vvbranch nbranch evals-branch

  bounding : ∀{Γ τ} → (e : Γ Source.|- τ) → (Θ : Source.sctx [] Γ)
                       → (a : substVal Θ)
                       → (Θ' : Complexity.sctx [] ⟨⟨ Γ ⟩⟩c)
                       → substBound Θ a Θ'
                       → expBound (Source.subst e Θ) (Complexity.subst || e ||e Θ')
  bounding unit Θ a Θ' sb unit unit-isval 0c unit-evals = l-proj-s , <>
  bounding (var x) Θ a Θ' sb v vv c evals =
    inv1 (a x) evals trans l-proj-s ,
    weakeningVal' vv (transport-valBound (inv2 (a x) evals) (val-hprop (transport val (inv2 (a x) evals) (a x)) vv) _ (sb x)) r-proj-s
  bounding z Θ a Θ' sb .z z-isval .0c z-evals = l-proj-s , r-proj-s
  bounding (suc e) Θ a Θ' sb .(suc e₁) (suc-isval e₁ vv) n (s-evals evals) =
    fst IH trans l-proj-s ,
    (r-proj (Complexity.subst || e ||e Θ')) , (snd IH) , r-proj-s
    where
      IH = (bounding e Θ a Θ' sb _ vv _ evals)
  bounding (rec e e₁ e₂) Θ a Θ' sb e' val-e' ._ (rec-evals {v = v} arg-evals branch-evals) =
    cong-+ (fst IH1) (fst lemma) trans l-proj-s , weakeningVal' val-e' (snd lemma) r-proj-s
    where
      IH1 = bounding e Θ a Θ' sb _ (evals-val arg-evals) _ arg-evals
      lemma = boundingRec v (evals-val arg-evals) _
              (Source.subst e₂ (Source.s-extend (Source.s-extend Θ))) _ _ (Complexity.subst || e₂ ||e (Complexity.s-extend (Complexity.s-extend Θ')))
              (snd IH1)
              (bounding e₁ Θ a Θ' sb )
              (λ v' valv' E' valBoundv' r valr R valBoundR v'' valv'' c'' evals-rec →
              let IH3 = (bounding e₂ (Source.lem4' Θ v' r) (extend-substVal2 a valv' valr) (Complexity.lem4' Θ' E' R)
                        (extend-substBound2 sb valBoundv' valBoundR) v'' valv'' c'' (transport (λ x → evals x v'' c'')
                        (Source.subst-compose4 Θ v' r e₂) evals-rec))
              in (fst IH3 trans cong-refl (ap l-proj (! (Complexity.subst-compose4 Θ' E' R || e₂ ||e))) ,
                 weakeningVal' valv'' (snd IH3) (cong-rproj (cong-refl (! (Complexity.subst-compose4 Θ' E' R || e₂ ||e))))))
                 e' val-e' _ branch-evals
  bounding {τ = ρ ->s τ} (lam e) Θ a Θ' sb .(lam (Source.subst e (Source.s-extend Θ))) (lam-isval .(Source.subst e (Source.s-extend Θ))) .0c lam-evals =
    l-proj-s ,
    (λ v₁ vv₁ E1 valbound1 v vv n body-evals →
    let IH = bounding e (Source.lem3' Θ v₁) (extend-substVal a vv₁)
             (Complexity.lem3' Θ' E1) (extend-substBound sb valbound1)
             v vv n (transport (λ x → evals x v n) (Source.subst-compose Θ v₁ e) body-evals)
    in
      fst IH trans cong-lproj (cong-refl (! (Complexity.subst-compose Θ' E1 || e ||e)) trans lam-s trans cong-app r-proj-s) ,
      weakeningVal' vv (snd IH) (cong-rproj (cong-refl (! (Complexity.subst-compose Θ' E1 || e ||e)) trans lam-s trans cong-app r-proj-s)))
  bounding (app e1 e2) Θ a Θ' sb v val-v .((n0 +c n1) +c n)
           (app-evals {n0} {n1} {n} {τ2} {τ} {.(Source.subst e1 Θ)} {e1'} {.(Source.subst e2 Θ)} {v2} e1-evals e2-evals subst-evals) =
    cong-+ (cong-+ (fst IH1) (fst IH2)) (fst IH1a) trans l-proj-s ,
    weakeningVal' val-v (snd IH1a) r-proj-s
      where
        IH1 = (bounding e1 Θ a Θ' sb (lam e1') (lam-isval e1') n0 e1-evals)
        v2-val = evals-val e2-evals
        IH2 = (bounding e2 Θ a Θ' sb v2 v2-val n1 e2-evals)
        IH1a = snd IH1 v2 v2-val (r-proj (Complexity.subst || e2 ||e Θ')) (snd IH2) v val-v n subst-evals
  bounding {Γ} {τ1 ×s τ2} (prod e1 e2) Θ a Θ' sb .(prod e3 e4) (pair-isval e3 e4 val-e3 val-e4) .(n1 +c n2) (pair-evals {n1} {n2} evals-c1 evals-c2) =
    cong-+ (fst IH1) (fst IH2) trans l-proj-s ,
    weakeningVal' val-e3 (snd IH1) (l-proj-s trans cong-lproj r-proj-s) ,
      weakeningVal' val-e4 (snd IH2) (r-proj-s trans cong-rproj r-proj-s)
    where
      IH1 = (bounding e1 Θ a Θ' sb _ val-e3 _ evals-c1)
      IH2 = (bounding e2 Θ a Θ' sb _ val-e4 _ evals-c2)
  bounding (delay e) Θ a Θ' sb .(delay (Source.subst e Θ)) (delay-isval .(Source.subst e Θ)) .0c delay-evals =
    l-proj-s ,
    (λ v₁ vv n x →
    let IH = bounding e Θ a Θ' sb v₁ vv n x  in
    fst IH trans cong-lproj (r-proj-s trans refl-s) ,
    weakeningVal' vv (snd IH) (cong-rproj r-proj-s))
  bounding (force e) Θ a Θ' sb v vv ._ (force-evals {n1} {n2} {τ} {e'} {.v} {.(Source.subst e Θ)} evals evals₁) =
    (cong-+ (fst IH) (fst (snd IH v vv n2 evals₁)) trans l-proj-s) ,
    weakeningVal' vv (snd (snd IH v vv n2 evals₁)) r-proj-s
    where
      IH = (bounding e Θ a Θ' sb _ (delay-isval e') n1 evals)
  bounding {Γ} {τ} (split e0 e1) Θ a Θ' sb e' val-e' .(n1 +c n2) (split-evals {n1} {n2} {.τ} {τ1} {τ2} {.(Source.subst e0 Θ)} {v1} {v2} evals-in-c0 evals-in-c1) with evals-val evals-in-c0 | (bounding e0 Θ a Θ' sb (prod v1 v2) (evals-val evals-in-c0) _ evals-in-c0)
  ... | pair-isval ._ ._ val-v1 val-v2 | (IH11 , vb1 , vb2)
           = cong-+ IH11 (fst IH2) trans
             cong-+ refl-s (cong-lproj (cong-refl (! (Complexity.subst-compose3 Θ' || e1 ||e (l-proj (r-proj || e0 ||e)) (r-proj (r-proj || e0 ||e)))))) trans l-proj-s ,
             weakeningVal' val-e' (snd IH2)
             (cong-rproj (cong-refl
               (! (Complexity.subst-compose3 Θ' || e1 ||e (l-proj (r-proj || e0 ||e)) (r-proj (r-proj || e0 ||e))))) trans r-proj-s) where
           IH2 = bounding e1 (Source.lem4' Θ v1 v2)
                            (extend-substVal2 a val-v1 val-v2)
                            (Complexity.lem4' Θ' (l-proj (r-proj (Complexity.subst || e0 ||e Θ'))) (r-proj (r-proj (Complexity.subst || e0 ||e Θ'))))
                            (extend-substBound2 sb vb1 vb2)
                              e' val-e' n2 (transport (λ x → evals x e' n2) (Source.subst-compose3 Θ e1 v1 v2) evals-in-c1)
  bounding nil Θ a Θ' sb .nil nil-isval .0c nil-evals = l-proj-s , r-proj-s
  bounding (e ::s e₁) Θ a Θ' sb .(x ::s xs) (cons-isval x xs vv vv₁) ._ (cons-evals evals evals₁) =
           (cong-+ (fst IH1) (fst IH2) trans l-proj-s) ,
             (r-proj (Complexity.subst || e ||e Θ')) , r-proj (Complexity.subst || e₁ ||e Θ') , ((snd IH1 , snd IH2) , r-proj-s)
    where
      IH1 = (bounding e Θ a Θ' sb _ vv _ evals)
      IH2 = (bounding e₁ Θ a Θ' sb _ vv₁ _ evals₁)
  bounding (listrec e e₁ e₂) Θ a Θ' sb v vv ._ (listrec-evals {v = k} arg-evals branch-evals) =
    (cong-+ (fst IH1) (fst lemma) trans l-proj-s) , weakeningVal' vv (snd lemma) r-proj-s
    where
      IH1 = bounding e Θ a Θ' sb _ (evals-val arg-evals) _ arg-evals
      lemma = boundingListRec k (evals-val arg-evals) _
              (Source.subst e₂ (Source.s-extend (Source.s-extend (Source.s-extend Θ)))) _ _
              (Complexity.subst || e₂ ||e (Complexity.s-extend (Complexity.s-extend (Complexity.s-extend Θ'))))
              (snd IH1)
              (bounding e₁ Θ a Θ' sb)
              (λ h' vh' H' vbh'H' v' vv' V' vbv'V' r vr R vbrR v₁ vv₁ n x₂ →
              let IH3 = bounding e₂ (Source.lem5' Θ h' v' r) (extend-substVal3 a vh' vv' vr) (Complexity.lem5' Θ' H' V' R)
                        (extend-substBound3 sb vbh'H' vbv'V' vbrR) v₁ vv₁ n
                        (transport (λ x → evals x v₁ n) (Source.subst-compose5 Θ e₂ h' v' r) x₂)
              in
              fst IH3 trans cong-refl (ap l-proj (! (Complexity.subst-compose5 Θ' || e₂ ||e H' V' R))) ,
              weakeningVal' vv₁ (snd IH3) (cong-rproj (cong-refl (! (Complexity.subst-compose5 Θ' || e₂ ||e H' V' R)))))
              v vv _ branch-evals
  bounding true Θ a Θ' sb .true true-isval .0c true-evals = l-proj-s , r-proj-s
  bounding false Θ a Θ' sb .false false-isval .0c false-evals = l-proj-s , r-proj-s

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
------------------------------------------------------------------------------
-- Properties related with lists of natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.List.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.List
open import FOTC.Data.List

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

++-ListN : ∀ {ms ns} → ListN ms → ListN ns → ListN (ms ++ ns)
++-ListN {ns = ns} lnnil nsL = prf
  where postulate prf : ListN ([] ++ ns)
        {-# ATP prove prf #-}

++-ListN {ns = ns} (lncons {m} {ms} Nd LNms) LNns = prf (++-ListN LNms LNns)
  where postulate prf : ListN (ms ++ ns) → ListN ((m ∷ ms) ++ ns)
        {-# ATP prove prf #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Issue847 where

data ⊥ : Set where

bad : ⊥
bad = bad′
  where
  abstract
    bad′ : ⊥
    bad′ = bad


text:
open import Logic.Classical
open import Structure.Real

module Structure.Real.Abs {ℓ₁ ℓ₂ ℓₑ} {R} ⦃ R-equiv ⦄ (_+_) (_⋅_) (_≤_) ⦃ classical : ∀{ℓ}{P} → Classical{ℓ}(P) ⦄ ⦃ reals : RealTheory{ℓ₁}{ℓₑ}{ℓ₂} {R} ⦃ R-equiv ⦄ (_+_)(_⋅_)(_≤_) ⦄ where
open RealTheory(reals)

open import Data.Boolean
import      Lvl
open import Functional
open import Logic
open import Logic.Classical
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Operator.Field
open import Structure.Operator.Monoid
open import Structure.Operator.Group
open import Structure.Relator.Ordering
open        Structure.Relator.Ordering.Weak.Properties
open import Structure.Relator.Properties
open import Syntax.Type
open import Type

-- TODO: This file is probably redundant. Move this to Structure.Operator.OrderedField.Abs

-- TODO: Prove somewhere that: (P → ([∨]-elim x y (_ :of: (P ∨ Q)) ≡ x)) ∧ (Q → ([∨]-elim x y (_ :of: (P ∨ Q)) ≡ y)) because this is neccessary when proving the properties of abs

-- abs : R → R
-- abs(x) = if(decide{P = x ≤ 𝟎}) then (− x) else x


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

open import Categories.Category
open import Categories.Object.Zero

module Categories.Object.Kernel.Properties {o ℓ e} {𝒞 : Category o ℓ e} (𝒞-Zero : Zero 𝒞) where

open import Function using (_$_)

open import Categories.Diagram.Equalizer 𝒞
open import Categories.Diagram.Pullback 𝒞 renaming (glue to glue-pullback; up-to-iso to pullback-up-to-iso)
open import Categories.Diagram.Pullback.Properties 𝒞
open import Categories.Object.Kernel 𝒞-Zero
open import Categories.Object.Terminal 𝒞

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open HomReasoning
open Equiv

open Zero 𝒞-Zero

private
  variable
    A B : Obj
    f : A ⇒ B

-- We can express kernels as pullbacks along the morphism '! : ⊥ ⇒ A'.
Kernel⇒Pullback : Kernel f → Pullback f !
Kernel⇒Pullback {f = f} kernel = record
  { p₁ = kernel⇒
  ; p₂ = ¡
  ; isPullback = record
    { commute = commute
    ; universal = λ {C} {h₁} {h₂} eq → universal {h = h₁} $ begin
      f ∘ h₁ ≈⟨ eq ⟩
      ! ∘ h₂ ≈˘⟨ refl⟩∘⟨ ¡-unique h₂ ⟩
      zero⇒ ∎
    ; unique = λ {C} {h₁} {h₂} {i} k-eq h-eq → unique $ begin
      h₁ ≈˘⟨ k-eq ⟩
      kernel⇒ ∘ i ∎
    ; p₁∘universal≈h₁ = ⟺ factors
    ; p₂∘universal≈h₂ = ¡-unique₂ _ _
    }
  }
  where
    open Kernel kernel

-- All pullbacks along the morphism '! : ⊥ ⇒ A' are also kernels.
Pullback⇒Kernel : Pullback f ! → Kernel f
Pullback⇒Kernel {f = f} pullback = record
  { kernel⇒ = p₁
  ; isKernel = record
    { commute = begin
      f ∘ p₁ ≈⟨ commute ⟩
      ! ∘ p₂ ≈˘⟨ refl⟩∘⟨ ¡-unique p₂ ⟩
      zero⇒ ∎
    ; universal = λ eq → universal eq
    ; factors = ⟺ p₁∘universal≈h₁
    ; unique = λ eq → unique (⟺ eq) (⟺ (¡-unique _))
    }
  }
  where
    open Pullback pullback

-- We can also express kernels as the equalizer of 'f' and the zero morphism.
Kernel⇒Equalizer : Kernel f → Equalizer f zero⇒
Kernel⇒Equalizer {f = f} kernel = record
  { arr = kernel⇒
  ; isEqualizer = record
    { equality = begin
      f ∘ kernel⇒ ≈⟨ commute ⟩
      zero⇒       ≈⟨ pushʳ (¡-unique (¡ ∘ kernel⇒)) ⟩
      zero⇒ ∘ kernel⇒ ∎
    ; equalize = λ {_} {h} eq → universal (eq ○ pullʳ (⟺ (¡-unique (¡ ∘ h))))
    ; universal = factors
    ; unique = unique
    }
  }
  where
    open Kernel kernel

-- Furthermore, all equalizers of 'f' and the zero morphism are equalizers
Equalizer⇒Kernel : Equalizer f zero⇒ → Kernel f
Equalizer⇒Kernel {f = f} equalizer = record
  { kernel⇒ = arr
  ; isKernel = record
    { commute = begin
      f ∘ arr      ≈⟨ equality ⟩
      zero⇒ ∘ arr ≈⟨ pullʳ (⟺ (¡-unique (¡ ∘ arr))) ⟩
      zero⇒ ∎
    ; universal = λ {_} {h} eq → equalize (eq ○ pushʳ (¡-unique (¡ ∘ h)))
    ; factors = universal
    ; unique = unique
    }
  }
  where
    open Equalizer equalizer

module _ (K : Kernel f) where
  open Kernel K

  Kernel-Mono : Mono kernel⇒
  Kernel-Mono g₁ g₂ eq = begin
    g₁ ≈⟨ unique refl ⟩
    universal universal-∘ ≈˘⟨ unique eq ⟩
    g₂ ∎

module _ (has-kernels : ∀ {A B} → (f : A ⇒ B) → Kernel f) where

  -- The kernel of a kernel is isomorphic to the zero object.
  kernel²-zero : ∀ {A B} {f : A ⇒ B} → Kernel.kernel (has-kernels (Kernel.kernel⇒ (has-kernels f))) ≅ zero
  kernel²-zero {B = B} {f = f} = pullback-up-to-iso kernel-pullback (pullback-mono-mono !-Mono)
    where
      K : Kernel f
      K = has-kernels f

      module K = Kernel K

      K′ : Kernel K.kernel⇒
      K′ = has-kernels K.kernel⇒

      kernel-pullback : Pullback ! !
      kernel-pullback = Pullback-resp-≈ (glue-pullback (Kernel⇒Pullback K) (swap (Kernel⇒Pullback K′))) (!-unique (f ∘ !)) refl

      pullback-mono-mono : ∀ {A B} {f : A ⇒ B} → Mono f → Pullback f f
      pullback-mono-mono mono = record
        { p₁ = id
        ; p₂ = id
        ; isPullback = pullback-self-mono mono
        }

max_stars_repo_name: FintanH/agda-categories

max_issues_repo_name: FintanH/agda-categories

max_forks_repo_name: FintanH/agda-categories


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Non-canonical model equipment for Kripke-style semantics.

module BasicIS4.Equipment.KripkeDyadicNonCanonical where

open import BasicIS4.Syntax.Common public

module Syntax
    (_⊢_    : Cx² Ty Ty → Ty → Set)
    (mono²⊢ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ A → Π′ ⊢ A)
    (up      : ∀ {A Π} → Π ⊢ (□ A) → Π ⊢ (□ □ A))
    (down    : ∀ {A Π} → Π ⊢ (□ A) → Π ⊢ A)
    (lift    : ∀ {A Γ Δ} → (Γ ⁏ Δ) ⊢ A → (□⋆ Γ ⁏ Δ) ⊢ (□ A))
  where

  -- Worlds.

  Worldᶜ : Set
  Worldᶜ = Cx² Ty Ty

  -- Intuitionistic accessibility.

  infix 3 _≤ᶜ_
  _≤ᶜ_ : Worldᶜ → Worldᶜ → Set
  _≤ᶜ_ = _⊆²_

  refl≤ᶜ : ∀ {w} → w ≤ᶜ w
  refl≤ᶜ = refl⊆²

  trans≤ᶜ : ∀ {w w′ w″} → w ≤ᶜ w′ → w′ ≤ᶜ w″ → w ≤ᶜ w″
  trans≤ᶜ = trans⊆²

  bot≤ᶜ : ∀ {w} → ∅² ≤ᶜ w
  bot≤ᶜ = bot⊆²

  -- Not the canonical modal accessibility, based on the 4 axiom.

  infix 3 _Яᶜ_
  _Яᶜ_ : Worldᶜ → Worldᶜ → Set
  w Яᶜ w′ = ∀ {A} → w ⊢ (□ A) → w′ ⊢ (□ □ A)

  reflЯᶜ : ∀ {w} → w Яᶜ w
  reflЯᶜ = up

  transЯᶜ : ∀ {w w′ w″} → w Яᶜ w′ → w′ Яᶜ w″ → w Яᶜ w″
  transЯᶜ ζ ζ′ = down ∘ ζ′ ∘ ζ

  botЯᶜ : ∀ {w} → ∅² Яᶜ w
  botЯᶜ = mono²⊢ bot≤ᶜ ∘ up

  liftЯᶜ : ∀ {Γ Δ} → Γ ⁏ Δ Яᶜ □⋆ Γ ⁏ Δ
  liftЯᶜ = down ∘ lift ∘ up

  -- Composition of accessibility.

  infix 3 _≤⨾Яᶜ_
  _≤⨾Яᶜ_ : Worldᶜ → Worldᶜ → Set
  _≤⨾Яᶜ_ = _≤ᶜ_ ⨾ _Яᶜ_

  infix 3 _Я⨾≤ᶜ_
  _Я⨾≤ᶜ_ : Worldᶜ → Worldᶜ → Set
  _Я⨾≤ᶜ_ = _Яᶜ_ ⨾ _≤ᶜ_

  refl≤⨾Яᶜ : ∀ {w} → w ≤⨾Яᶜ w
  refl≤⨾Яᶜ {w} = w , (refl≤ᶜ , reflЯᶜ)

  reflЯ⨾≤ᶜ : ∀ {w} → w Я⨾≤ᶜ w
  reflЯ⨾≤ᶜ {w} = w , (reflЯᶜ , refl≤ᶜ)

  -- Persistence condition, after Iemhoff; included by Ono.
  --
  --   w′      v′  →           v′
  --   ◌───Я───●   →           ●
  --   │           →         ╱
  --   ≤  ξ,ζ      →       Я
  --   │           →     ╱
  --   ●           →   ●
  --   w           →   w

  ≤⨾Я→Яᶜ : ∀ {v′ w} → w ≤⨾Яᶜ v′ → w Яᶜ v′
  ≤⨾Я→Яᶜ (w′ , (ξ , ζ)) = ζ ∘ mono²⊢ ξ

  -- Brilliance condition, after Iemhoff.
  --
  --           v′  →           v′
  --           ●   →           ●
  --           │   →         ╱
  --      ζ,ξ  ≤   →       Я
  --           │   →     ╱
  --   ●───Я───◌   →   ●
  --   w       v   →   w

  Я⨾≤→Яᶜ : ∀ {w v′} → w Я⨾≤ᶜ v′ → w Яᶜ v′
  Я⨾≤→Яᶜ (v , (ζ , ξ)) = mono²⊢ ξ ∘ ζ

  -- Minor persistence condition, included by Božić and Došen.
  --
  --   w′      v′  →           v′
  --   ◌───Я───●   →           ●
  --   │           →           │
  --   ≤  ξ,ζ      →           ≤
  --   │           →           │
  --   ●           →   ●───Я───◌
  --   w           →   w       v
  --
  --                   w″  →                   w″
  --                   ●   →                   ●
  --                   │   →                   │
  --             ξ′,ζ′ ≤   →                   │
  --                   │   →                   │
  --           ●───R───◌   →                   ≤
  --           │       v′  →                   │
  --      ξ,ζ  ≤           →                   │
  --           │           →                   │
  --   ●───R───◌           →   ●───────R───────◌
  --   w       v           →   w               v″

  ≤⨾Я→Я⨾≤ᶜ : ∀ {v′ w} → w ≤⨾Яᶜ v′ → w Я⨾≤ᶜ v′
  ≤⨾Я→Я⨾≤ᶜ {v′} ξ,ζ = v′ , (≤⨾Я→Яᶜ ξ,ζ , refl≤ᶜ)

  transЯ⨾≤ᶜ : ∀ {w′ w w″} → w Я⨾≤ᶜ w′ → w′ Я⨾≤ᶜ w″ → w Я⨾≤ᶜ w″
  transЯ⨾≤ᶜ {w′} (v , (ζ , ξ)) (v′ , (ζ′ , ξ′)) = let v″ , (ζ″ , ξ″) = ≤⨾Я→Я⨾≤ᶜ (w′ , (ξ , ζ′))
                                                  in  v″ , (transЯᶜ ζ ζ″ , trans≤ᶜ ξ″ ξ′)

  ≤→Яᶜ : ∀ {v′ w} → w ≤ᶜ v′ → w Яᶜ v′
  ≤→Яᶜ {v′} ξ = ≤⨾Я→Яᶜ (v′ , (ξ , reflЯᶜ))

  -- Minor brilliance condition, included by Ewald and Alechina et al.
  --
  --           v′  →   w′      v′
  --           ●   →   ◌───Я───●
  --           │   →   │
  --      ζ,ξ  ≤   →   ≤
  --           │   →   │
  --   ●───Я───◌   →   ●
  --   w       v   →   w
  --
  --           v′      w″  →   v″              w″
  --           ◌───R───●   →   ◌───────R───────●
  --           │           →   │
  --           ≤  ξ′,ζ′    →   │
  --   v       │           →   │
  --   ◌───R───●           →   ≤
  --   │       w′          →   │
  --   ≤  ξ,ζ              →   │
  --   │                   →   │
  --   ●                   →   ●
  --   w                   →   w

  Я⨾≤→≤⨾Яᶜ : ∀ {w v′} → w Я⨾≤ᶜ v′ → w ≤⨾Яᶜ v′
  Я⨾≤→≤⨾Яᶜ {w} ζ,ξ = w , (refl≤ᶜ , Я⨾≤→Яᶜ ζ,ξ)

  trans≤⨾Яᶜ : ∀ {w′ w w″} → w ≤⨾Яᶜ w′ → w′ ≤⨾Яᶜ w″ → w ≤⨾Яᶜ w″
  trans≤⨾Яᶜ {w′} (v , (ξ , ζ)) (v′ , (ξ′ , ζ′)) = let v″ , (ξ″ , ζ″) = Я⨾≤→≤⨾Яᶜ (w′ , (ζ , ξ′))
                                                  in  v″ , (trans≤ᶜ ξ ξ″ , transЯᶜ ζ″ ζ′)

  ≤→Яᶜ′ : ∀ {w v′} → w ≤ᶜ v′ → w Яᶜ v′
  ≤→Яᶜ′ {w} ξ = Я⨾≤→Яᶜ (w , (reflЯᶜ , ξ))

  -- Infimum (greatest lower bound) of accessibility.
  --
  --   w′
  --   ●
  --   │
  --   ≤  ξ,ζ
  --   │
  --   ◌───R───●
  --   w       v

  infix 3 _≤⊓Яᶜ_
  _≤⊓Яᶜ_ : Worldᶜ → Worldᶜ → Set
  _≤⊓Яᶜ_ = _≤ᶜ_ ⊓ _Яᶜ_

  infix 3 _Я⊓≤ᶜ_
  _Я⊓≤ᶜ_ : Worldᶜ → Worldᶜ → Set
  _Я⊓≤ᶜ_ = _Яᶜ_ ⊓ _≤ᶜ_

  ≤⊓Я→Я⊓≤ᶜ : ∀ {w′ v} → w′ ≤⊓Яᶜ v → v Я⊓≤ᶜ w′
  ≤⊓Я→Я⊓≤ᶜ (w , (ξ , ζ)) = w , (ζ , ξ)

  Я⊓≤→≤⊓Яᶜ : ∀ {w′ v} → v Я⊓≤ᶜ w′ → w′ ≤⊓Яᶜ v
  Я⊓≤→≤⊓Яᶜ (w , (ζ , ξ)) = w , (ξ , ζ)

  -- Supremum (least upper bound) of accessibility.
  --
  --   w′      v′
  --   ●───R───◌
  --           │
  --      ξ,ζ  ≤
  --           │
  --           ●
  --           v

  infix 3 _≤⊔Яᶜ_
  _≤⊔Яᶜ_ : Worldᶜ → Worldᶜ → Set
  _≤⊔Яᶜ_ = _≤ᶜ_ ⊔ _Яᶜ_

  infix 3 _Я⊔≤ᶜ_
  _Я⊔≤ᶜ_ : Worldᶜ → Worldᶜ → Set
  _Я⊔≤ᶜ_ = _Яᶜ_ ⊔ _≤ᶜ_

  ≤⊔Я→Я⊔≤ᶜ : ∀ {w′ v} → w′ ≤⊔Яᶜ v → v Я⊔≤ᶜ w′
  ≤⊔Я→Я⊔≤ᶜ (v′ , (ξ , ζ)) = v′ , (ζ , ξ)

  Я⊔≤→≤⊔Яᶜ : ∀ {w′ v} → v Я⊔≤ᶜ w′ → w′ ≤⊔Яᶜ v
  Я⊔≤→≤⊔Яᶜ (v′ , (ζ , ξ)) = v′ , (ξ , ζ)

  -- Infimum-to-supremum condition, included by Ewald.
  --
  --   w′          →   w′      v′
  --   ●           →   ●───Я───◌
  --   │           →           │
  --   ≤  ξ,ζ      →           ≤
  --   │           →           │
  --   ◌───Я───●   →           ●
  --   w       v   →           v

  -- NOTE: This could be more precise.
  ≤⊓Я→≤⊔Яᶜ : ∀ {v w′} → w′ ≤⊓Яᶜ v → v ≤⊔Яᶜ w′
  ≤⊓Я→≤⊔Яᶜ {v} {w′} (w , (ξ , ζ)) =
    (w′ ⧺² v) , (weak⊆²⧺₂ , mono²⊢ (weak⊆²⧺₁ v) ∘ up)

  -- Supremum-to-infimum condition.
  --
  --   w′      v′  →   w′
  --   ●───Я───◌   →   ●
  --           │   →   │
  --      ξ,ζ  ≤   →   ≤
  --           │   →   │
  --           ●   →   ◌───Я───●
  --           v   →   w       v

  -- NOTE: This could be more precise.
  ≤⊔Я→≤⊓Яᶜ : ∀ {w′ v} → v ≤⊔Яᶜ w′ → w′ ≤⊓Яᶜ v
  ≤⊔Я→≤⊓Яᶜ (v′ , (ξ , ζ)) = ∅² , (bot≤ᶜ , botЯᶜ)


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

{-
  Helper routines most often used in reasoning with commutative squares,
  at the level of arrows in categories.

  Basic  : reasoning about identity
  Pulls  : use a ∘ b ≈ c as left-to-right rewrite
  Pushes : use c ≈ a ∘ b as a left-to-right rewrite
  IntroElim : introduce/eliminate an equivalent-to-id arrow
  Extend : 'extends' a commutative square with an equality on left/right/both
-}
module Categories.Morphism.Reasoning.Core {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Function renaming (id to idᶠ; _∘_ to _∙_)

open import Relation.Binary hiding (_⇒_)

open Category C

private
  variable
    X Y : Obj
    a a′ a″ b b′ b″ c c′ c″ : X ⇒ Y
    f g h i : X ⇒ Y

open HomReasoning

module Basic where
  id-unique : ∀ {o} {f : o ⇒ o} → (∀ g → g ∘ f ≈ g) → f ≈ id
  id-unique g∘f≈g = trans (sym identityˡ) (g∘f≈g id)

  id-comm : ∀ {a b} {f : a ⇒ b} → f ∘ id ≈ id ∘ f
  id-comm = trans identityʳ (sym identityˡ)

  id-comm-sym : ∀ {a b} {f : a ⇒ b} → id ∘ f ≈ f ∘ id
  id-comm-sym = trans identityˡ (sym identityʳ)

open Basic public

module Utils where
  assoc² : ((i ∘ h) ∘ g) ∘ f ≈ i ∘ (h ∘ (g ∘ f))
  assoc² = trans assoc assoc

  assoc²' : (i ∘ (h ∘ g)) ∘ f ≈ i ∘ (h ∘ (g ∘ f))
  assoc²' = trans assoc (∘-resp-≈ʳ assoc)

open Utils public

module Pulls (ab≡c : a ∘ b ≈ c) where

  pullʳ : (f ∘ a) ∘ b ≈ f ∘ c
  pullʳ {f = f} = begin
    (f ∘ a) ∘ b ≈⟨ assoc ⟩
    f ∘ (a ∘ b) ≈⟨ refl⟩∘⟨ ab≡c ⟩
    f ∘ c       ∎

  pullˡ : a ∘ b ∘ f ≈ c ∘ f
  pullˡ {f = f} = begin
    a ∘ b ∘ f   ≈⟨ sym assoc ⟩
    (a ∘ b) ∘ f ≈⟨ ab≡c ⟩∘⟨refl ⟩
    c ∘ f       ∎

open Pulls public

module Pushes (c≡ab : c ≈ a ∘ b) where
  pushʳ : f ∘ c ≈ (f ∘ a) ∘ b
  pushʳ {f = f} = begin
    f ∘ c       ≈⟨ refl⟩∘⟨ c≡ab ⟩
    f ∘ (a ∘ b) ≈˘⟨ assoc ⟩
    (f ∘ a) ∘ b ∎

  pushˡ : c ∘ f ≈ a ∘ (b ∘ f)
  pushˡ {f = f} = begin
    c ∘ f       ≈⟨ c≡ab ⟩∘⟨refl ⟩
    (a ∘ b) ∘ f ≈⟨ assoc ⟩
    a ∘ (b ∘ f) ∎

open Pushes public

module IntroElim (a≡id : a ≈ id) where
  elimʳ : f ∘ a ≈ f
  elimʳ {f = f} = begin
    f ∘ a  ≈⟨ refl⟩∘⟨ a≡id ⟩
    f ∘ id ≈⟨ identityʳ ⟩
    f      ∎

  introʳ : f ≈ f ∘ a
  introʳ = Equiv.sym elimʳ

  elimˡ : (a ∘ f) ≈ f
  elimˡ {f = f} = begin
    a ∘ f  ≈⟨ a≡id ⟩∘⟨refl ⟩
    id ∘ f ≈⟨ identityˡ ⟩
    f      ∎

  introˡ : f ≈ a ∘ f
  introˡ = Equiv.sym elimˡ

open IntroElim public

module Extends (s : CommutativeSquare f g h i) where
  extendˡ : CommutativeSquare f g (a ∘ h) (a ∘ i)
  extendˡ {a = a} = begin
    (a ∘ h) ∘ f ≈⟨ pullʳ s ⟩
    a ∘ i ∘ g   ≈˘⟨ assoc ⟩
    (a ∘ i) ∘ g ∎

  extendʳ : CommutativeSquare (f ∘ a) (g ∘ a) h i
  extendʳ {a = a} = begin
    h ∘ (f ∘ a) ≈⟨ pullˡ s ⟩
    (i ∘ g) ∘ a ≈⟨ assoc ⟩
    i ∘ (g ∘ a) ∎

  extend² : CommutativeSquare (f ∘ b) (g ∘ b) (a ∘ h) (a ∘ i)
  extend² {b = b} {a = a } = begin
    (a ∘ h) ∘ (f ∘ b) ≈⟨ pullʳ extendʳ ⟩
    a ∘ (i ∘ (g ∘ b)) ≈˘⟨ assoc ⟩
    (a ∘ i) ∘ (g ∘ b) ∎

open Extends public

-- essentially composition in the arrow category
{-
   A₁ -- c --> B₁
   |           |
   b′  comm    b
   |           |
   V           V
   A₂ -- c′ -> B₂
   |           |
   a′  comm    a
   |           |
   V           V
   A₃ -- c″ -> B₃

   then the whole diagram commutes
-}
glue : CommutativeSquare c′ a′ a c″ →
       CommutativeSquare c b′ b c′ →
       CommutativeSquare c (a′ ∘ b′) (a ∘ b) c″
glue {c′ = c′} {a′ = a′} {a = a} {c″ = c″} {c = c} {b′ = b′} {b = b} sq-a sq-b = begin
  (a ∘ b) ∘ c    ≈⟨ pullʳ sq-b ⟩
  a ∘ (c′ ∘ b′)  ≈⟨ pullˡ sq-a ⟩
  (c″ ∘ a′) ∘ b′ ≈⟨ assoc ⟩
  c″ ∘ (a′ ∘ b′) ∎

glue◃◽ : a ∘ c′ ≈ c″ → CommutativeSquare c b′ b c′ → CommutativeSquare c b′ (a ∘ b) c″
glue◃◽ {a = a} {c′ = c′} {c″ = c″} {c = c} {b′ = b′} {b = b} tri-a sq-b = begin
  (a ∘ b) ∘ c   ≈⟨ pullʳ sq-b ⟩
  a ∘ (c′ ∘ b′) ≈⟨ pullˡ tri-a ⟩
  c″ ∘ b′       ∎

glue◃◽′ : c ∘ c′ ≈ a′ → CommutativeSquare a b a′ b′ → CommutativeSquare (c′ ∘ a) b c b′
glue◃◽′ {c = c} {c′ = c′} {a′ = a′} {a = a} {b = b} {b′ = b′} tri sq = begin
  c ∘ c′ ∘ a ≈⟨ pullˡ tri ⟩
  a′ ∘ a     ≈⟨ sq ⟩
  b′ ∘ b     ∎

glue◽◃ : CommutativeSquare a b a′ b′ → b ∘ c ≈ c′ → CommutativeSquare (a ∘ c) c′ a′ b′
glue◽◃ {a = a} {b = b} {a′ = a′} {b′ = b′} {c = c} {c′ = c′} sq tri = begin
  a′ ∘ a ∘ c   ≈⟨ pullˡ sq ⟩
  (b′ ∘ b) ∘ c ≈⟨ pullʳ tri ⟩
  b′ ∘ c′      ∎

glue▹◽ : b ∘ a″ ≈ c → CommutativeSquare a b a′ b′ → CommutativeSquare (a ∘ a″) c a′ b′
glue▹◽ {b = b} {a″ = a″} {c = c} {a = a} {a′ = a′} {b′ = b′} tri sq = begin
  a′ ∘ a ∘ a″   ≈⟨ pullˡ sq ⟩
  (b′ ∘ b) ∘ a″ ≈⟨ pullʳ tri ⟩
  b′ ∘ c        ∎

-- essentially composition in the over category
glueTrianglesʳ : a ∘ b ≈ a′ → a′ ∘ b′ ≈ a″ → a ∘ (b ∘ b′) ≈ a″
glueTrianglesʳ {a = a} {b = b} {a′ = a′} {b′ = b′} {a″ = a″} a∘b≡a′ a′∘b′≡a″ = begin
  a ∘ (b ∘ b′) ≈⟨ pullˡ a∘b≡a′ ⟩
  a′ ∘ b′      ≈⟨ a′∘b′≡a″ ⟩
  a″           ∎

-- essentially composition in the under category
glueTrianglesˡ : a′ ∘ b′ ≈ b″ → a ∘ b ≈ b′ → (a′ ∘ a) ∘ b ≈ b″
glueTrianglesˡ {a′ = a′} {b′ = b′} {b″ = b″} {a = a} {b = b} a′∘b′≡b″ a∘b≡b′ = begin
  (a′ ∘ a) ∘ b ≈⟨ pullʳ a∘b≡b′ ⟩
  a′ ∘ b′      ≈⟨ a′∘b′≡b″ ⟩
  b″           ∎

module Cancellers (inv : h ∘ i ≈ id) where

  cancelʳ : (f ∘ h) ∘ i ≈ f
  cancelʳ {f = f} = begin
    (f ∘ h) ∘ i ≈⟨ pullʳ inv ⟩
    f ∘ id      ≈⟨ identityʳ ⟩
    f           ∎

  cancelˡ : h ∘ (i ∘ f) ≈ f
  cancelˡ {f = f} = begin
    h ∘ (i ∘ f) ≈⟨ pullˡ inv ⟩
    id ∘ f      ≈⟨ identityˡ ⟩
    f           ∎

  cancelInner : (f ∘ h) ∘ (i ∘ g) ≈ f ∘ g
  cancelInner {f = f} {g = g} = begin
    (f ∘ h) ∘ (i ∘ g) ≈⟨ pullˡ cancelʳ ⟩
    f ∘ g             ∎

open Cancellers public

center : g ∘ h ≈ a → (f ∘ g) ∘ h ∘ i ≈ f ∘ a ∘ i
center {g = g} {h = h} {a = a} {f = f} {i = i} eq = begin
  (f ∘ g) ∘ h ∘ i ≈⟨ assoc ⟩
  f ∘ g ∘ h ∘ i   ≈⟨ refl⟩∘⟨ pullˡ eq ⟩
  f ∘ a ∘ i       ∎

center⁻¹ : f ∘ g ≈ a → h ∘ i ≈ b →  f ∘ (g ∘ h) ∘ i ≈ a ∘ b
center⁻¹ {f = f} {g = g} {a = a} {h = h} {i = i} {b = b} eq eq′ = begin
  f ∘ (g ∘ h) ∘ i ≈⟨ refl⟩∘⟨ pullʳ eq′ ⟩
  f ∘ g ∘ b       ≈⟨ pullˡ eq ⟩
  a ∘ b           ∎

pull-last : h ∘ i ≈ a → (f ∘ g ∘ h) ∘ i ≈ f ∘ g ∘ a
pull-last {h = h} {i = i} {a = a} {f = f} {g = g} eq = begin
  (f ∘ g ∘ h) ∘ i ≈⟨ assoc ⟩
  f ∘ (g ∘ h) ∘ i ≈⟨ refl⟩∘⟨ pullʳ eq ⟩
  f ∘ g ∘ a       ∎

pull-first : f ∘ g ≈ a → f ∘ (g ∘ h) ∘ i ≈ a ∘ h ∘ i
pull-first {f = f} {g = g} {a = a} {h = h} {i = i} eq = begin
  f ∘ (g ∘ h) ∘ i ≈⟨ refl⟩∘⟨ assoc ⟩
  f ∘ g ∘ h ∘ i   ≈⟨ pullˡ eq ⟩
  a ∘ h ∘ i       ∎


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

module TreeFold.Indexed where

open import Prelude
open import Data.Binary using (𝔹; 0ᵇ; 1ᵇ_; 2ᵇ_; ⟦_⇓⟧; ⟦_⇑⟧; inc)
open import Data.Binary.Isomorphism
open import Data.Nat

private
  variable
    n m : ℕ
    t : Level
    N : ℕ → Type t
    ns : 𝔹

double : ℕ → ℕ
double n = n * 2

2^_*_ : ℕ → ℕ → ℕ
2^ zero  * m = m
2^ suc n * m = double (2^ n * m)

infixr 5 _1∷_ _2∷_
data Array (T : ℕ → Type a) : 𝔹 → Type a where
  []  : Array T 0ᵇ
  _1∷_ : T 1 → Array (T ∘ double) ns → Array T (1ᵇ ns)
  _2∷_ : T 2 → Array (T ∘ double) ns → Array T (2ᵇ ns)

cons : (∀ n → N n → N n → N (double n)) → N 1 → Array N ns → Array N (inc ns)
cons branch x [] = x 1∷ []
cons branch x (y 1∷ ys) = branch 1 x y 2∷ ys
cons branch x (y 2∷ ys) = x 1∷ cons (branch ∘ double) y ys

array-foldr : (N : ℕ → Type t) → (∀ n m → N (2^ n * 1) → N (2^ n * m) → N (2^ n * suc m)) → N 0 → Array N ns → N ⟦ ns ⇓⟧
array-foldr {ns = 0ᵇ}    N c b []        = b
array-foldr {ns = 2ᵇ ns} N c b (x 2∷ xs) = c 1 ⟦ ns ⇓⟧       x (array-foldr (N ∘ double) (c ∘ suc) b xs)
array-foldr {ns = 1ᵇ ns} N c b (x 1∷ xs) = c 0 (⟦ ns ⇓⟧ * 2) x (array-foldr (N ∘ double) (c ∘ suc) b xs)

open import Data.Vec
import Data.Nat.Properties as ℕ

double≡*2 : ∀ n → n + n ≡ n * 2
double≡*2 zero    = refl
double≡*2 (suc n) = cong suc (ℕ.+-suc n n ; cong suc (double≡*2 n))

module NonNorm {t} (N : ℕ → Type t) (f : ∀ p n m → N (2^ p * n) → N (2^ p * m) → N (2^ p * (n + m))) (z : N 0) where
  spine : Vec (N 1) n → Array (N ) ⟦ n ⇑⟧
  spine [] = []
  spine (x ∷ xs) = cons (λ n x y → subst N (double≡*2 n) (f 0 n n x y)) x (spine xs)

  unspine : Array N ns → N ⟦ ns ⇓⟧
  unspine = array-foldr N (λ n → f n 1) z

  treeFold : Vec (N 1) n → N n
  treeFold xs = subst N (𝔹-rightInv _) (unspine (spine xs))

pow-suc : ∀ n m → (2^ n * 1) + (2^ n * m) ≡ (2^ n * suc m)
pow-suc zero m = refl
pow-suc (suc n) m = sym (ℕ.+-*-distrib (2^ n * 1) (2^ n * m) 2) ; cong (_* 2) (pow-suc n m)

module _ {t} (N : ℕ → Type t) (f : ∀ {n m} → N n → N m → N (n + m)) (z : N 0) where
  spine : Vec (N 1) n → Array (N ) ⟦ n ⇑⟧
  spine [] = []
  spine (x ∷ xs) = cons (λ n x y → subst N (double≡*2 n) (f x y)) x (spine xs)

  unspine : Array N ns → N ⟦ ns ⇓⟧
  unspine = array-foldr N (λ n m xs ys → subst N (pow-suc n m) (f xs ys)) z

  treeFold : Vec (N 1) n → N n
  treeFold xs = subst N (𝔹-rightInv _) (unspine (spine xs))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Computability.Recursive where

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤)
open import Data.Bool using (Bool; false; true)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; pred)
open import Data.Product using (_×_)
open import Data.Fin using (Fin; zero; suc; punchIn; punchOut)
open import Data.Sum using (_⊎_)
open import Data.Vec using (Vec; _∷_; []; lookup) renaming (map to map-Vec)
open import Function using (Bijective)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Level renaming (zero to lzero; suc to lsuc)

variable
  n m : ℕ
  b : Bool

data RecFun : (use-mu : Bool) → ℕ → Set where
  Var : Fin n → RecFun b n
  Bind : Vec (RecFun b m) n → RecFun b n → RecFun b m
  Zero : RecFun b 0
  Suc : RecFun b 1
  Rec : RecFun b n → RecFun b (2 + n) → RecFun b (suc n)
  Mu : RecFun b (suc n) → RecFun true n

mutual
  eval-no-mu : Vec ℕ n → RecFun false n → ℕ
  eval-no-mu v (Var i) = lookup v i
  eval-no-mu v (Bind xs r) = eval-no-mu (eval-bindings v xs) r
  eval-no-mu v Zero = zero
  eval-no-mu (x ∷ []) Suc = suc x
  eval-no-mu (x ∷ v) (Rec base rec) = eval-no-mu-rec x v base rec

  eval-bindings : ∀{n m} → Vec ℕ m → Vec (RecFun false m) n → Vec ℕ n
  eval-bindings v [] = []
  eval-bindings v (x ∷ xs) = eval-no-mu v x ∷ eval-bindings v xs

  eval-no-mu-rec : ℕ → Vec ℕ n → RecFun false n → RecFun false (2 + n) → ℕ
  eval-no-mu-rec zero v base rec = eval-no-mu v base
  eval-no-mu-rec (suc k) v base rec = eval-no-mu (k ∷ result ∷ v) rec
    where result = eval-no-mu-rec k v base rec

postulate
  enum-RecFun : ∀ vars → ℕ → RecFun true vars
  enum-RecFun-Surj : ∀ vars → ℕ → Bijective {A = ℕ} {B = RecFun true vars} _≡_ _≡_ (enum-RecFun vars)

max_stars_repo_name: jesyspa/computability-in-agda

max_issues_repo_name: jesyspa/computability-in-agda

max_forks_repo_name: jesyspa/computability-in-agda


text:
module Experimental.Finite where

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

data Fin : ℕ → Set where
  Fin-S : ∀ {n} → Fin n → Fin (S n)
  Fin-Z : ∀ {n} → Fin (S n)

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt