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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Nat
open import Cubical.Data.NatPlusOne

open import Cubical.Algebra
open import Cubical.Algebra.Properties
open import Cubical.Algebra.Semigroup.Properties using (isPropIsSemigroup)

open import Cubical.Relation.Binary.Reasoning.Equality

private
  variable
    ??? : Level

isPropIsBand : ??? {B : Type ???} {_???_} ??? isProp (IsBand B _???_)
isPropIsBand {_} {_} {_???_} (isband aSemigroup aIdem) (isband bSemigroup bIdem) =
  cong??? isband (isPropIsSemigroup aSemigroup bSemigroup) (isPropIdempotent (IsSemigroup.is-set aSemigroup) _???_ aIdem bIdem)

module BandLemmas (S : Band ???) where
  open Band S

  ^-id : ??? x n ??? x ^ n ??? x
  ^-id x one          = refl
  ^-id x (2+ zero)    = idem x
  ^-id x (2+ (suc n)) =
    x ??? (x ??? x ^ 1+ n) ???????? assoc x x (x ^ 1+ n) ???
    x ??? x ??? x ^ 1+ n   ?????? cong (_??? x ^ 1+ n) (idem x) ???
    x ??? x ^ 1+ n       ?????? ^-id x (2+ n) ???
    x                  ???

open BandLemmas public

ext: agda


text:
module _ where

data Unit : Set where
  unit : Unit

module M (_ : Unit) where

  record R₁ (A : Set) : Set₁ where
    no-eta-equality

    postulate
      x : A

  open R₁ ⦃ … ⦄ public

  record R₂ (A : Set) : Set₁ where
    field
      instance
        r₁ : R₁ A

  open R₂ ⦃ … ⦄

open M unit

postulate
  A : Set

instance
  postulate
    m : R₁ A

a : A
a = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- 2014-04-06 Andreas, issue reported by Andres Sicard-Ramirez

-- {-# OPTIONS --termination-depth=100 -v term.matrices:40 #-}

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

-- The following function is accepted by the termination checker in
-- Agda-2.3.2.2, but it is rejected by the termination checker in
-- the current development version. (The function was adapted from Lee,
-- Jones, and Ben-Amram, POPL '01).
p : ℕ → ℕ → ℕ → ℕ
p m n        (succ r) = p m r n
p m (succ n) zero     = p zero n m
p m zero     zero     = m


text:
module Oscar.Class.Monoid where

open import Oscar.Data.Equality
open import Oscar.Level

record Monoid {a} {A : Set a} {b} (_↠_ : A → A → Set b) : Set (a ⊔ b) where
  field
    ε : ∀ {m} → m ↠ m
    _◇_ : ∀ {l m n} → m ↠ n → l ↠ m → l ↠ n
    ◇-left-identity : ∀ {m n} → (f : m ↠ n) → ε ◇ f ≡ f
    ◇-right-identity : ∀ {m n} → (f : m ↠ n) → f ◇ ε ≡ f
    ◇-associativity : ∀ {k l m n} (f : k ↠ l) (g : l ↠ m) (h : m ↠ n) → h ◇ (g ◇ f) ≡ (h ◇ g) ◇ f

open Monoid ⦃ … ⦄ public


text:
-- {-# OPTIONS --sized-types #-} Option obsolete since 2014-04-12.

module SizedTypesLeqInfty where

open import Common.Size
data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {↑ size}
  suc  : {size : Size} -> Nat {size} -> Nat {↑ size}

weak : {i : Size} -> Nat {i} -> Nat {∞}
weak x = x


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

open import lib.Basics
open import lib.types.Group
open import lib.types.Pi
open import lib.NType2
open import lib.types.Paths
open import lib.types.EilenbergMacLane1.Core

module lib.types.EilenbergMacLane1.FunElim where

module _ {i} {G : Group i} where

  private
    module G = Group G

  module EM₁Level₁FunElim {j k} {B : EM₁ G → Type j} {C : EM₁ G → Type k}
    {{C-level : has-level 1 (C embase)}}
    (embase* : B embase → C embase)
    (emloop* : ∀ g b → transport C (emloop g) (embase* b) == embase* (transport B (emloop g) b))
    (emloop-comp* : ∀ g₁ g₂ b →
      emloop* (G.comp g₁ g₂) b ◃∙
      ap (λ p → embase* (transport B p b)) (emloop-comp g₁ g₂) ◃∙
      ap embase* (transp-∙ (emloop g₁) (emloop g₂) b) ◃∎
      =ₛ
      ap (λ p → transport C p (embase* b)) (emloop-comp g₁ g₂) ◃∙
      transp-∙ (emloop g₁) (emloop g₂) (embase* b) ◃∙
      ap (transport C (emloop g₂)) (emloop* g₁ b) ◃∙
      emloop* g₂ (transport B (emloop g₁) b) ◃∎)
    where

    emloop** : ∀ g → embase* == embase* [ (λ x → B x → C x) ↓ emloop g ]
    emloop** g = ↓-→-from-transp (λ= (emloop* g))

    private
      emloop-comp** : ∀ g₁ g₂ →
        emloop** (G.comp g₁ g₂) == emloop** g₁ ∙ᵈ emloop** g₂
          [ (λ p → embase* == embase* [ (λ x → B x → C x) ↓ p ]) ↓ emloop-comp g₁ g₂ ]
      emloop-comp** g₁ g₂ = step₁ ▹ step₂
        where
        intermediate' : ∀ b →
          transport C (emloop g₁ ∙ emloop g₂) (embase* b) ==
          embase* (transport B (emloop g₁ ∙ emloop g₂) b)
        intermediate' =
          comp-transp {B = B} {C = C}
                      {u = embase*} {u' = embase*} {u'' = embase*}
                      (emloop g₁) (emloop g₂)
                      (λ= (emloop* g₁)) (λ= (emloop* g₂))
        intermediate : embase* == embase* [ (λ x → B x → C x) ↓ emloop g₁ ∙ emloop g₂ ]
        intermediate = ↓-→-from-transp (λ= intermediate')
        step₁'' : ∀ b →
          app= (λ= (emloop* (G.comp g₁ g₂))) b ◃∙
          app= (ap (λ p → embase* ∘ transport B p) (emloop-comp g₁ g₂)) b ◃∎
          =ₛ
          app= (ap (λ p → transport C p ∘ embase*) (emloop-comp g₁ g₂)) b ◃∙
          app= (λ= intermediate') b ◃∎
        step₁'' b =
          app= (λ= (emloop* (G.comp g₁ g₂))) b ◃∙
          app= (ap (λ p → embase* ∘ transport B p) (emloop-comp g₁ g₂)) b ◃∎
            =ₛ₁⟨ 0 & 1 & app=-β (emloop* (G.comp g₁ g₂)) b ⟩
          emloop* (G.comp g₁ g₂) b ◃∙
          app= (ap (λ p → embase* ∘ transport B p) (emloop-comp g₁ g₂)) b ◃∎
            =ₛ₁⟨ 1 & 1 & ∘-ap (_$ b) (λ p → embase* ∘ transport B p) (emloop-comp g₁ g₂) ⟩
          emloop* (G.comp g₁ g₂) b ◃∙
          ap (λ p → embase* (transport B p b)) (emloop-comp g₁ g₂) ◃∎
            =ₛ⟨ post-rotate-in {p = _ ◃∙ _ ◃∎} (emloop-comp* g₁ g₂ b) ⟩
          ap (λ p → transport C p (embase* b)) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (embase* b) ◃∙
          ap (transport C (emloop g₂)) (emloop* g₁ b) ◃∙
          emloop* g₂ (transport B (emloop g₁) b) ◃∙
          ! (ap embase* (transp-∙ (emloop g₁) (emloop g₂) b)) ◃∎
            =ₛ₁⟨ 2 & 1 & ap (ap (transport C (emloop g₂))) (! (app=-β (emloop* g₁) b)) ⟩
          ap (λ p → transport C p (embase* b)) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (embase* b) ◃∙
          ap (transport C (emloop g₂)) (app= (λ= (emloop* g₁)) b) ◃∙
          emloop* g₂ (transport B (emloop g₁) b) ◃∙
          ! (ap embase* (transp-∙ (emloop g₁) (emloop g₂) b)) ◃∎
            =ₛ₁⟨ 3 & 1 & ! (app=-β (emloop* g₂) (transport B (emloop g₁) b)) ⟩
          ap (λ p → transport C p (embase* b)) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (embase* b) ◃∙
          ap (transport C (emloop g₂)) (app= (λ= (emloop* g₁)) b) ◃∙
          app= (λ= (emloop* g₂)) (transport B (emloop g₁) b) ◃∙
          ! (ap embase* (transp-∙ (emloop g₁) (emloop g₂) b)) ◃∎
            =ₛ⟨ 1 & 4 & contract ⟩
          ap (λ p → transport C p (embase* b)) (emloop-comp g₁ g₂) ◃∙
          intermediate' b ◃∎
            =ₛ₁⟨ 0 & 1 & ap-∘ (_$ b) (λ p → transport C p ∘ embase*) (emloop-comp g₁ g₂) ⟩
          app= (ap (λ p → transport C p ∘ embase*) (emloop-comp g₁ g₂)) b ◃∙
          intermediate' b ◃∎
            =ₛ₁⟨ 1 & 1 & ! (app=-β intermediate' b) ⟩
          app= (ap (λ p → transport C p ∘ embase*) (emloop-comp g₁ g₂)) b ◃∙
          app= (λ= intermediate') b ◃∎ ∎ₛ
        step₁' :
          λ= (emloop* (G.comp g₁ g₂)) ∙
          ap (λ p → embase* ∘ transport B p) (emloop-comp g₁ g₂)
          ==
          ap (λ p → transport C p ∘ embase*) (emloop-comp g₁ g₂) ∙
          λ= intermediate'
        step₁' =
          –>-is-inj (app=-equiv {A = B embase} {P = λ _ → C embase}
                                {f = transport C (emloop (G.comp g₁ g₂)) ∘ embase*}
                                {g = embase* ∘ transport B (emloop g₁ ∙ emloop g₂)})
                     _ _ $
          λ= $ λ b →
          app= (λ= (emloop* (G.comp g₁ g₂)) ∙
                ap (λ p → embase* ∘ transport B p) (emloop-comp g₁ g₂)) b
            =⟨ ap-∙ (_$ b) (λ= (emloop* (G.comp g₁ g₂)))
                           (ap (λ p → embase* ∘ transport B p) (emloop-comp g₁ g₂)) ⟩
          app= (λ= (emloop* (G.comp g₁ g₂))) b ∙
          app= (ap (λ p → embase* ∘ transport B p) (emloop-comp g₁ g₂)) b
            =⟨ =ₛ-out (step₁'' b) ⟩
          app= (ap (λ p → transport C p ∘ embase*) (emloop-comp g₁ g₂)) b ∙
          app= (λ= intermediate') b
            =⟨ ∙-ap (_$ b) (ap (λ p → transport C p ∘ embase*) (emloop-comp g₁ g₂))
                           (λ= intermediate') ⟩
          app= (ap (λ p → transport C p ∘ embase*) (emloop-comp g₁ g₂) ∙
                λ= intermediate') b =∎
        step₁ : emloop** (G.comp g₁ g₂) == intermediate
                  [ (λ p → embase* == embase* [ (λ x → B x → C x) ↓ p ]) ↓ emloop-comp g₁ g₂ ]
        step₁ =
          ap↓ ↓-→-from-transp $
          ↓-='-in $
          ∙'=∙ (λ= (emloop* (G.comp g₁ g₂)))
               (ap (λ p → embase* ∘ transport B p) (emloop-comp g₁ g₂)) ∙
          step₁'
        step₂ : intermediate == emloop** g₁ ∙ᵈ emloop** g₂
        step₂ = ↓-→-from-transp-∙ᵈ {B = B} {C = C} {p = emloop g₁} {q = emloop g₂}
                                   {u = embase*} {u' = embase*} {u'' = embase*}
                                   (λ= (emloop* g₁)) (λ= (emloop* g₂))

      module M =
        EM₁Level₁Elim
          {P = λ x → B x → C x}
          {{EM₁-prop-elim {P = λ x → has-level 1 (B x → C x)}
                          {{λ x → has-level-is-prop}}
                          (Π-level {B = λ _ → C embase} (λ _ → C-level))}}
          embase*
          emloop**
          emloop-comp**

      open M public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{- SAMPLE PROGRAMS IN SOURCE LANGUAGE -}

{-# OPTIONS --no-termination-check #-}

open import Preliminaries
open import Source

module Samples where

  {- dbl (n : nat) : nat = 2 * n -}
  dbl : ∀ {Γ} → Γ |- (nat ->s nat)
  dbl = lam (rec (var i0) z (suc (suc (force (var (iS i0))))))

  {- add (m n : nat) : nat = m + n -}
  add : ∀ {Γ} → Γ |- (nat ->s (nat ->s nat))
  add = lam (lam (rec (var (iS i0)) (var i0) (suc (force (var (iS i0))))))

  {- mult (m n : nat) : nat = m * n -}
  mult : ∀ {Γ} → Γ |- (nat ->s (nat ->s nat))
  mult = lam (lam (rec (var (iS i0)) z (app (app add (var (iS (iS i0)))) (force (var (iS i0))))))

  -- hack : instead of having bool case analysis just do natural number recursion and return 1/0

  {- iszero (n : nat) : nat = z -> 1 | _ -> 0 -}
  isz : ∀ {Γ} → Γ |- (nat ->s nat)
  isz = lam (rec (var i0) (suc z) z)

  {- leq (m n : nat) : nat = m ≤ n -}
  leq : ∀ {Γ} → Γ |- (nat ->s (nat ->s nat))
  leq = lam (lam (rec (var (iS i0))
          (app isz (var (iS i0)))
          (rec (var (iS (iS (iS i0)))) (suc z) (force (var (iS i0))))))

  {- len (l : list τ) : nat = [] -> z | x :: xs -> 1 + len xs -}
  len : ∀ {Γ τ} → Γ |- (list τ ->s nat)
  len = lam (listrec (var i0) z (suc (force (var (iS (iS i0))))))

  {- insert (l : list nat) (el : nat) : list nat = [] -> [el] | x :: xs -> (leq el x -> el :: x :: xs | x :: (insert el xs)) -}
  insert : ∀ {Γ} → Γ |- (list nat ->s (nat ->s list nat))
  insert = lam (lam (listrec (var (iS i0))
             (var i0 ::s nil)
             (rec (app (app leq (var (iS (iS (iS i0))))) (var i0))
               (var i0 ::s force (var (iS (iS i0))))
               (var (iS (iS (iS (iS (iS i0))))) ::s var (iS (iS (iS (iS (iS (iS i0))))))))))

  {- insertion sort (l : list nat) : list nat = [] -> [] | x :: xs -> insert x (isort xs) -}
  isort : ∀ {Γ} → Γ |- (list nat ->s list nat)
  isort = lam (listrec (var i0) nil (app (app insert (force (var (iS (iS i0))))) (var i0)))

  {- halve (l : list nat) : (list nat * list nat) = splits a list in half -}
  halve : ∀ {Γ} → Γ |- (list nat ->s (list nat ×s list nat))
  halve = lam (listrec (var i0)
            (prod nil nil)
            (listrec (var (iS i0))
              (prod (var i0 ::s nil) nil)
              (prod (var (iS (iS (iS i0))) ::s split (force (var (iS (iS i0)))) (var i0)) (var i0 ::s split (force (var (iS (iS i0)))) (var (iS i0))))))

  {- merge (l1 l2 : list nat) : list nat =
       match l1 with
       [] -> l2
       x :: xs ->
         match l2 with
           [] -> x :: xs
           y :: ys ->
             x <= y -> x :: merge xs l2
             _ -> y :: merge l1 ys -}
  merge : ∀ {Γ} → Γ |- ((list nat ×s list nat) ->s list nat)
  merge = lam (listrec (split (var i0) (var i0))
            (split (var i0) (var (iS i0)))
            (listrec (split (var (iS (iS (iS i0)))) (var (iS i0)))
              (split (var (iS (iS (iS i0)))) (var i0))
              (rec (app (app leq (var (iS (iS (iS i0))))) (var i0))
                (var (iS (iS (iS i0))) ::s force (var (iS (iS (iS (iS (iS i0)))))))
                (var i0 ::s app merge (prod (split (var (iS (iS (iS (iS (iS (iS (iS (iS i0))))))))) (var (iS i0))) (var (iS (iS (iS i0)))))))))

  {- mergesort (l : list nat) : list nat -}
  msort : ∀ {Γ} → Γ |- (list nat ->s list nat)
  msort = lam (listrec (var i0)
            nil
            (listrec (var (iS i0))
              (var i0 ::s nil)
              (app merge (prod
                (app msort (split (app halve (var (iS (iS (iS (iS (iS (iS i0)))))))) (var i0)))
                (app msort (split (app halve (var (iS (iS (iS (iS (iS (iS i0)))))))) (var (iS i0))))))))

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


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

open import Cubical.Core.Everything

module Cubical.Relation.Binary.Raw.Bundles {c : Level} (Carrier : Type c) where

open import Cubical.Foundations.Prelude using (isSet)

open import Cubical.Relation.Nullary using (¬_)
open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Binary.Raw.Definitions
open import Cubical.Relation.Binary.Raw.Structures

------------------------------------------------------------------------
-- Preorders
------------------------------------------------------------------------

record Preorder ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _∼_
  field
    _∼_        : RawRel Carrier ℓ
    isPreorder : IsPreorder _∼_

  open IsPreorder isPreorder public

------------------------------------------------------------------------
-- Equivalences
------------------------------------------------------------------------

record PartialEquivalence ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  field
    _≈_                  : RawRel Carrier ℓ
    isPartialEquivalence : IsPartialEquivalence _≈_

  open IsPartialEquivalence isPartialEquivalence public

  _≉_ : RawRel Carrier _
  x ≉ y = ¬ (x ≈ y)

record Equivalence ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _≈_
  field
    _≈_           : RawRel Carrier ℓ
    isEquivalence : IsEquivalence _≈_

  open IsEquivalence isEquivalence public

  partialEquivalence : PartialEquivalence ℓ
  partialEquivalence = record
    { isPartialEquivalence = isPartialEquivalence
    }

  open PartialEquivalence partialEquivalence public using (_≉_)

  preorder : Preorder ℓ
  preorder = record
    { isPreorder = isPreorder
    }

record DecEquivalence ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _≈_
  field
    _≈_              : RawRel Carrier ℓ
    isDecEquivalence : IsDecEquivalence _≈_

  open IsDecEquivalence isDecEquivalence public

  equivalence : Equivalence ℓ
  equivalence = record
    { isEquivalence = isEquivalence
    }

  open Equivalence equivalence public using (partialEquivalence; _≉_)

------------------------------------------------------------------------
-- Partial orders
------------------------------------------------------------------------

record PartialOrder ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _≤_
  field
    _≤_            : RawRel Carrier ℓ
    isPartialOrder : IsPartialOrder _≤_

  open IsPartialOrder isPartialOrder public

  preorder : Preorder ℓ
  preorder = record
    { isPreorder = isPreorder
    }

record DecPartialOrder ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _≤_
  field
    _≤_               : RawRel Carrier ℓ
    isDecPartialOrder : IsDecPartialOrder _≤_

  open IsDecPartialOrder isDecPartialOrder public

  partialOrder : PartialOrder ℓ
  partialOrder = record
    { isPartialOrder = isPartialOrder
    }

  open PartialOrder partialOrder public using (preorder)

record StrictPartialOrder ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _<_
  field
    _<_                  : RawRel Carrier ℓ
    isStrictPartialOrder : IsStrictPartialOrder _<_

  open IsStrictPartialOrder isStrictPartialOrder public

record DecStrictPartialOrder ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _<_
  field
    _<_                     : RawRel Carrier ℓ
    isDecStrictPartialOrder : IsDecStrictPartialOrder _<_

  open IsDecStrictPartialOrder isDecStrictPartialOrder public

  strictPartialOrder : StrictPartialOrder ℓ
  strictPartialOrder = record
    { isStrictPartialOrder = isStrictPartialOrder
    }

------------------------------------------------------------------------
-- Total orders
------------------------------------------------------------------------

record TotalOrder ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _≤_
  field
    _≤_          : RawRel Carrier ℓ
    isTotalOrder : IsTotalOrder _≤_

  open IsTotalOrder isTotalOrder public

  partialOrder : PartialOrder ℓ
  partialOrder = record
    { isPartialOrder = isPartialOrder
    }

  open PartialOrder partialOrder public using (preorder)

record DecTotalOrder ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _≤_
  field
    _≤_             : RawRel Carrier ℓ
    isDecTotalOrder : IsDecTotalOrder _≤_

  open IsDecTotalOrder isDecTotalOrder public

  totalOrder : TotalOrder ℓ
  totalOrder = record
    { isTotalOrder = isTotalOrder
    }

  open TotalOrder totalOrder public using (partialOrder; preorder)

  decPartialOrder : DecPartialOrder ℓ
  decPartialOrder = record
    { isDecPartialOrder = isDecPartialOrder
    }

-- Note that these orders are decidable. The current implementation
-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
-- definition capturing these three properties implies decidability
-- as `Trichotomous` necessarily separates out the equality case.

record StrictTotalOrder ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  infix 4 _<_
  field
    _<_                : RawRel Carrier ℓ
    isStrictTotalOrder : IsStrictTotalOrder _<_

  open IsStrictTotalOrder isStrictTotalOrder public

  strictPartialOrder : StrictPartialOrder ℓ
  strictPartialOrder = record
    { isStrictPartialOrder = isStrictPartialOrder
    }


text:
{-# OPTIONS --safe --warning=error --without-K --guardedness #-}

open import Setoids.Setoids
open import Rings.Definition
open import Rings.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Semirings.Definition

module Fields.CauchyCompletion.Approximation {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open PartiallyOrderedRing pRing
open Ring R
open Group additiveGroup
open Field F

open import Fields.Lemmas F
open import Fields.Orders.Lemmas {F = F} record { oRing = order }
open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.AbsoluteValue order
open import Rings.Orders.Partial.Lemmas pRing
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Addition order F
open import Fields.CauchyCompletion.Comparison order F
open import Rings.InitialRing R
open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })

abstract

  chain : {a b : A} (c : CauchyCompletion) → (a r<C c) → (c <Cr b) → a < b
  chain {a} {b} c record { e = betweenAC ; 0<e = 0<betweenAC ; N = Nac ; pr = prAC } record { e = betweenCB ; 0<e = 0<betweenCB ; N = Nb ; property = prBC } = SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenAC a)) (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder (prAC (succ Nac +N Nb) (le Nb (applyEquality succ (Semiring.commutative ℕSemiring Nb Nac)))) (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenCB (index (Sequence.tail (CauchyCompletion.elts c)) (Nac +N Nb))))))) (prBC (succ Nac +N Nb) (le Nac refl))

  private
    approxLemma : (a : CauchyCompletion) (e e/2 : A) → (0G < e) → (e/2 + e/2 ∼ e) → (m N : ℕ) → abs ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N)) < e/2 → (e/2 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) N + e)
    approxLemma a e e/2 0<e prE/2 m N ans with totality 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N))
    approxLemma a e e/2 0<e prE/2 m N ans | inl (inl x) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) groupIsAbelian (orderRespectsAddition ans (index (CauchyCompletion.elts a) N))
    ... | bl = <WellDefined groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) prE/2)) (orderRespectsAddition bl e/2)
    approxLemma a e e/2 0<e prE/2 m N ans | inl (inr x) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) (identLeft) (orderRespectsAddition x (index (CauchyCompletion.elts a) N))
    ... | bl = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (ringAddInequalities bl (halfLess e/2 e 0<e prE/2))
    approxLemma a e e/2 0<e prE/2 m N ans | inr x with transferToRight additiveGroup (Equivalence.symmetric eq x)
    ... | bl = <WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bl)) groupIsAbelian (orderRespectsAddition (halfLess e/2 e 0<e prE/2) (index (CauchyCompletion.elts a) N))

approximateAboveCrude : (a : CauchyCompletion) → A
approximateAboveCrude a with CauchyCompletion.converges a 1R (0<1 (charNot2ImpliesNontrivial R charNot2))
... | N , conv = (((index (CauchyCompletion.elts a) (succ N)) + 1R) + 1R) + 1R

abstract
  approximateAboveCrudeIsAbove : (a : CauchyCompletion) → a <Cr (approximateAboveCrude a)
  approximateAboveCrudeIsAbove a with CauchyCompletion.converges a 1R (0<1 (charNot2ImpliesNontrivial R charNot2))
  ... | N , conv = record { e = 1R ; 0<e = 0<1 (charNot2ImpliesNontrivial R charNot2) ; N = N ; property = ans }
    where
      ans : (m : ℕ) → (N <N m) → (1R + index (CauchyCompletion.elts a) m) < (((index (CauchyCompletion.elts a) (succ N) + 1R) + 1R) + 1R)
      ans m N<m with conv {m} {succ N} N<m (le 0 refl)
      ... | bl with totality 0G (index (CauchyCompletion.elts a) m + inverse (index (CauchyCompletion.elts a) (succ N)))
      ans m N<m | bl | inl (inl 0<am-aN) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) (Equivalence.reflexive eq) (orderRespectsAddition bl (index (CauchyCompletion.elts a) (succ N)))
      ... | am<1+an = <WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) identLeft) groupIsAbelian) (Equivalence.transitive eq (+WellDefined groupIsAbelian (Equivalence.reflexive eq)) +Associative) (ringAddInequalities am<1+an (orderRespectsAddition (0<1 (charNot2ImpliesNontrivial R charNot2)) 1R))
      ans m N<m | bl | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
      ... | am<aN = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder am<aN (<WellDefined (Equivalence.reflexive eq) (+Associative) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (0<1 (charNot2ImpliesNontrivial R charNot2)) (0<1 (charNot2ImpliesNontrivial R charNot2)))) (index (CauchyCompletion.elts a) (succ N)))))) 1R)
      ans m N<m | bl | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (+WellDefined identLeft (Equivalence.reflexive eq)) identLeft) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (Equivalence.reflexive eq)) +Associative)) (orderRespectsAddition (ringAddInequalities (0<1 (charNot2ImpliesNontrivial R charNot2)) (0<1 (charNot2ImpliesNontrivial R charNot2))) (1R + (index (CauchyCompletion.elts a) m)))

rationalApproximatelyAbove : (a : CauchyCompletion) → (e : A) → (0G < e) → A
rationalApproximatelyAbove a e 0<e with halve charNot2 e
... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
... | 0<e/2 with halve charNot2 e/2
... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
... | N , cauchyBeyondN = index (CauchyCompletion.elts a) (succ N) + e/2

abstract
  rationalApproximatelyAboveIsAbove : (a : CauchyCompletion) (e : A) → (0<e : 0G < e) → a <Cr (rationalApproximatelyAbove a e 0<e)
  rationalApproximatelyAboveIsAbove a e 0<e with halve charNot2 e
  ... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
  ... | 0<e/2 with halve charNot2 e/2
  ... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
  ... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
  ... | N , cauchyBeyondN with halve charNot2 e/4
  ... | e/8 , prE/8 with halvePositive e/8 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/8) 0<e/4)
  ... | 0<e/8 with CauchyCompletion.converges a e/8 0<e/8
  ... | N2 , cauchyBeyondN2 = record { e = e/8 ; 0<e = 0<e/8 ; N = N +N N2 ; property = ans2 }
    where
      ans2 : (m : ℕ) → N +N N2 <N m → (e/8 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N) + e/2)
      ans2 m <m with cauchyBeyondN {m} {succ N} (inequalityShrinkLeft <m) (le 0 refl)
      ... | absam-aN<e/4 with totality 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) (succ N)))
      ans2 m <m | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.<Transitive pOrder (<WellDefined groupIsAbelian (Equivalence.transitive eq groupIsAbelian  +Associative) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) (Equivalence.reflexive eq) (orderRespectsAddition am-aN<e/4 (index (CauchyCompletion.elts a) (succ N)))) e/8)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)) (index (CauchyCompletion.elts a) (succ N))))
      ans2 m <m | -[am-aN]<e/4 | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft)) (Equivalence.reflexive eq) (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _) (ringSwapNegatives' -[am-aN]<e/4)) (e/4 + e/8))
      ... | e/8<am-aN+e/4+e/8 = SetoidPartialOrder.<Transitive pOrder (orderRespectsAddition e/8<am-aN+e/4+e/8 (index (CauchyCompletion.elts a) m)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (ringAddInequalities (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities am-aN<0 (<WellDefined groupIsAbelian prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)))) am<aN))
        where
          am<aN : (index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N))
          am<aN = <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) groupIsAbelian)) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invRight) identRight)) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
      ans2 m <m | absam-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (orderRespectsAddition {b = e/2} (SetoidPartialOrder.<Transitive pOrder (halfLess e/8 e/4 0<e/4 prE/8) (halfLess e/4 e/2 0<e/2 prE/4)) (index (CauchyCompletion.elts a) m))

  rationalApproximatelyAboveIsNear : (a : CauchyCompletion) (e : A) → (0<e : 0G < e) → (injection (rationalApproximatelyAbove a e 0<e) +C (-C a)) <C (injection e)
  rationalApproximatelyAboveIsNear a e 0<e with halve charNot2 e
  ... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
  ... | 0<e/2 with halve charNot2 e/2
  ... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
  ... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
  ... | N , cauchyBeyondN with halve charNot2 e/4
  ... | e/8 , prE/8 with halvePositive e/8 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/8) 0<e/4)
  ... | 0<e/8 with CauchyCompletion.converges a e/8 0<e/8
  ... | N8 , cauchyBeyondN8 with halve charNot2 e/8
  ... | e/16 , prE/16 with halvePositive e/16 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/16) 0<e/8)
  ... | 0<e/16 = record { i = (e/2 + e/4) + e/8 ; a<i = record { e = e/8 ; 0<e = 0<e/8 ; N = N +N N8 ; property = ans } ; i<b = record { e = e/16 ; 0<e = 0<e/16 ; N = 0 ; pr = t' } }
    where
      t' : (m : ℕ) → (0 <N m) → (((e/2 + e/4) + e/8) + e/16) < index (constSequence e) m
      t' m 0<m rewrite indexAndConst e m = <WellDefined (Equivalence.reflexive eq) prE/2 (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) prE/4) (<WellDefined +Associative (Equivalence.symmetric eq +Associative) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/8 (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (halfLess e/16 e/8 0<e/8 prE/16) e/8))) (e/2 + e/4)))))
      ans : (m : ℕ) → (N +N N8) <N m → (e/8 + index (apply _+_ (constSequence (index (CauchyCompletion.elts a) (succ N) + e/2)) (map inverse (CauchyCompletion.elts a))) m) < ((e/2 + e/4) + e/8)
      ans m N<m rewrite indexAndApply (constSequence (index (CauchyCompletion.elts a) (succ N) + e/2)) (map inverse (CauchyCompletion.elts a)) _+_ {m} | indexAndConst (index (CauchyCompletion.elts a) (succ N) + e/2) m | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) = <WellDefined groupIsAbelian (+WellDefined groupIsAbelian (Equivalence.reflexive eq)) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq groupIsAbelian (Equivalence.reflexive eq)) (Equivalence.reflexive eq) q) e/8)
        where
          am : A
          am = index (CauchyCompletion.elts a) m
          aN : A
          aN = index (CauchyCompletion.elts a) (succ N)
          t : abs (am + inverse aN) < e/4
          t = cauchyBeyondN {m} {succ N} (inequalityShrinkLeft N<m) (le 0 refl)
          r : ((inverse am) + aN) < e/4
          r with t
          ... | f with totality 0G (am + inverse aN)
          r | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) (lemm2' _ 0<am-aN)) 0<e/4
          r | f | inl (inr x) = <WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) f
          r | am-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq 0=am-aN) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (invIdent additiveGroup)) (inverseWellDefined additiveGroup 0=am-aN)) (inverseWellDefined additiveGroup groupIsAbelian)) (invContravariant additiveGroup)) (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) am-aN<e/4
          q : ((inverse (index (CauchyCompletion.elts a) m)) + (index (CauchyCompletion.elts a) (succ N) + e/2)) < (e/4 + e/2)
          q = <WellDefined (Equivalence.symmetric eq +Associative) (Equivalence.reflexive eq) (orderRespectsAddition r e/2)

  approximateAbove : (a : CauchyCompletion) → (ε : A) → (0G < ε) → Sg A (λ b → (a <Cr b) && (injection b +C (-C a)) <C (injection ε))
  approximateAbove a e 0<e = rationalApproximatelyAbove a e 0<e , (rationalApproximatelyAboveIsAbove a e 0<e ,, rationalApproximatelyAboveIsNear a e 0<e)

  approximateBelow : (a : CauchyCompletion) → (ε : A) → (0G < ε) → Sg A (λ b → (b r<C a) && (a +C (-C injection b)) <C (injection ε))
  approximateBelow a e 0<e with approximateAbove (-C a) e 0<e
  ... | x , (record { e = deltaXAnd-A ; 0<e = 0<deltaXA ; N = NdeltaXA ; property = prDeltaXA } ,, record { i = rationalNear ; a<i = record { e = bound ; 0<e = 0<bound ; N = N ; property = prBound } ; i<b = record { e = bound2 ; 0<e = 0<bound2 ; N = N2 ; pr = prBound2 } }) = inverse x , (record { e = deltaXAnd-A ; 0<e = 0<deltaXA ; N = NdeltaXA ; pr = λ m N<m → <WellDefined (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (cancel {m} (CauchyCompletion.elts a))) identRight)))))) (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invRight (Equivalence.reflexive eq)) identLeft)) (orderRespectsAddition (prDeltaXA m N<m) (inverse x + (index (CauchyCompletion.elts a) m))) } ,, record { i = rationalNear ; a<i = record { e = bound ; 0<e = 0<bound ; N = N ; property = pr1 } ; i<b = record { e = bound2 ; 0<e = 0<bound2 ; N = N2 ; pr = prBound2 } })
    where
      cancel : {m : ℕ} (a : Sequence A) → (index (map inverse a) m) + (index a m) ∼ 0G
      cancel {m} a rewrite equalityCommutative (mapAndIndex a inverse m) = invLeft
      pr1 : (m : ℕ) → (N <N m) → (bound + index (apply _+_ (CauchyCompletion.elts a) (map inverse (constSequence (inverse x)))) m) < rationalNear
      pr1 m N<m with prBound m N<m
      ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (constSequence (inverse x))) _+_ {m} | equalityCommutative (mapAndIndex (constSequence (inverse x)) inverse m) | indexAndConst x m | indexAndApply (constSequence x) (map inverse (map inverse (CauchyCompletion.elts a))) _+_ {m} | indexAndConst x m | equalityCommutative (mapAndIndex (map inverse (CauchyCompletion.elts a)) inverse m) | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) | indexAndConst (inverse x) m = <WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (invTwice additiveGroup _) (Equivalence.symmetric eq (invTwice additiveGroup _))))) (Equivalence.reflexive eq) bl

  boundModulus : (a : CauchyCompletion) → Sg A (λ b → Sg ℕ (λ N → (m : ℕ) → (N <N m) → (abs (index (CauchyCompletion.elts a) m)) < b))
  boundModulus a with approximateBelow a 1R (0<1 (charNot2ImpliesNontrivial R charNot2))
  ... | below , (below<a ,, a-below<e) with approximateAbove a 1R (0<1 (charNot2ImpliesNontrivial R charNot2))
  ... | above , (a<above ,, above-a<e) with totality 0R below
  boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) with totality 0R above
  boundModulus a | below , (record { e = belowBound ; 0<e = 0<belowBound ; N = Nbelow ; pr = prBelow } ,, a-below<e) | above , (record { e = bound ; 0<e = 0<bound ; N = N ; property = ans } ,, above-a<e) | inl (inl 0<below) | inl (inl 0<above) = above , ((N +N Nbelow) , λ m N<m → SetoidPartialOrder.<Transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
    where
      res : (m : ℕ) → ((N +N Nbelow) <N m) → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
      res m N<m with totality 0R (index (CauchyCompletion.elts a) m)
      res m N<m | inl (inl _) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
      res m N<m | inl (inr am<0) = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder 0<below (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<belowBound below)) (prBelow m (inequalityShrinkRight N<m))) am<0)))
      res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound
  boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inl (inr above<0) = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder 0<below (SetoidPartialOrder.<Transitive pOrder (chain a below<a a<above) above<0)))
  boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inr 0=above = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder 0<below (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (chain a below<a a<above))))
  boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) with totality 0R above
  boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) with totality (inverse below) above
  boundModulus a | below , (record { e = boundBelow ; 0<e = 0<boundBelow ; N = N ; pr = prBoundBelow } ,, a-below<e) | above , (record { e = boundAbove ; 0<e = 0<boundAbove ; N = Nabove ; property = prBoundAbove } ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inl -bel<ab) = above , ((N +N Nabove) , ans)
    where
      ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
      ans m N<m with totality 0G (index (CauchyCompletion.elts a) m)
      ans m N<m | inl (inl 0<am) = SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
      ans m N<m | inl (inr am<0) = SetoidPartialOrder.<Transitive pOrder (ringSwapNegatives' (prBoundBelow m (inequalityShrinkLeft N<m))) (SetoidPartialOrder.<Transitive pOrder (ringSwapNegatives' (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below))) -bel<ab)
      ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
  boundModulus a | below , (record { e = boundBelow ; 0<e = 0<boundBelow ; N = N ; pr = prBoundBelow } ,, a-below<e) | above , (record { e = boundAbove ; 0<e = 0<boundAbove ; N = Nabove ; property = prBoundAbove } ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inr ab<-bel) = inverse below , ((N +N Nabove) , ans)
    where
      ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < (inverse below)
      ans m N<m with totality 0G (index (CauchyCompletion.elts a) m)
      ans m N<m | inl (inl 0<am) = SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) ab<-bel
      ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
      ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 below below<0)
  boundModulus a | below , (record { e = boundBelow ; 0<e = 0<boundBelow ; N = N ; pr = prBoundBelow } ,, a-below<e) | above , (record { e = boundAbove ; 0<e = 0<boundAbove ; N = Nabove ; property = prBoundAbove } ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inr -bel=ab = above , ((N +N Nabove) , ans)
    where
      ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
      ans m N<m with totality 0G (index (CauchyCompletion.elts a) m)
      ans m N<m | inl (inl 0<am) = SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
      ans m N<m | inl (inr am<0) = <WellDefined (Equivalence.reflexive eq) (-bel=ab) (ringSwapNegatives' (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m))))
      ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
  boundModulus a | below , (record { e = boundBelow ; 0<e = 0<boundBelow ; N = N ; pr = prBoundBelow } ,, a-below<e) | above , (record { e = boundAbove ; 0<e = 0<boundAbove ; N = Nabove ; property = prBoundAbove } ,, above-a<e) | inl (inr below<0) | inl (inr above<0) = inverse below , ((N +N Nabove) , ans)
    where
      ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
      ans m N<m with totality 0R (index (CauchyCompletion.elts a) m)
      ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<am (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
      ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
      ans m N<m | inr 0=am = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=am) (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
  boundModulus a | below , (record { e = boundBelow ; 0<e = 0<boundBelow ; N = N ; pr = prBoundBelow } ,, a-below<e) | above , (record { e = boundAbove ; 0<e = 0<boundAbove ; N = Nabove ; property = prBoundAbove } ,, above-a<e) | inl (inr below<0) | inr 0=above = inverse below , ((N +N Nabove) , ans)
    where
      ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
      ans m N<m with totality 0R (index (CauchyCompletion.elts a) m)
      ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (SetoidPartialOrder.<Transitive pOrder 0<am (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))))))
      ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
      ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 _ below<0)
  boundModulus a | below , (record { e = boundBelow ; 0<e = boundBelowDiff ; N = Nb ; pr = ansBelow } ,, a-below<e) | above , (record { e = bound ; 0<e = 0<bound ; N = N ; property = ans } ,, above-a<e) | inr 0=below = above , ((N +N Nb) , λ m N<m → SetoidPartialOrder.<Transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
    where
      res : (m : ℕ) → (N +N Nb) <N m → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
      res m N<m with totality 0R (index (CauchyCompletion.elts a) m)
      res m N<m | inl (inl 0<am) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
      res m N<m | inl (inr am<0) = exFalso (irreflexive (<WellDefined (Equivalence.symmetric eq 0=below) (Equivalence.reflexive eq) (SetoidPartialOrder.<Transitive pOrder (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition boundBelowDiff below)) (ansBelow m (inequalityShrinkRight N<m))) am<0)))
      res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound


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

module Motif where

open import Prelude

open import SUtil using (lookup)

open import Yamanote using (counterp)

import Definition.Conversion
import Definition.Conversion.Whnf
import Definition.Typed
import Definition.Untyped
import Definition.Typed.Consequences.InverseUniv
import Definition.Typed.Consequences.NeTypeEq
import Definition.Typed.Consequences.Syntactic
import Definition.Typed.Properties
import Relation.Binary.PropositionalEquality.Core

-- Number of levels of recursion
levels : ℕ
levels = 2

-- Factor to slow down base melody
multiplier : ℕ
multiplier = 2 ^ levels

-- slowed down prime, etc forms
p i r ri : List Note → List Note
p = map (slowDown multiplier)
i = inversion ∘ p
r = retrograde ∘ p
ri = retrograde ∘ i

w : Pitch → List Note
w n = slowDown multiplier (tone half n) ∷ []

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

-- Hexachords from P10 of ICFP 2020 micro-opera.
i20p10a i20p10b i20coda : List Note

i20p10a =
  tone 8th  (b♭ 4) ∷
  tone 8th  (b♭ 4) ∷
  tone 8th  (a  4) ∷
  tone 8th  (g  4) ∷
  tone qtr  (c  5) ∷
  tone qtr  (d  5) ∷
  tone half (c♯ 5) ∷
  []

i20p10b =
  tone qtr  (b  4) ∷
  tone 9    (e  5) ∷
  tone 8th  (f♯ 4) ∷
  tone 8th  (f  4) ∷
  tone 8th  (d♯ 4) ∷
  tone half (g♯ 5) ∷
  []

i20coda =
  tone 8th   (a 5) ∷
  tone 8th   (f 5) ∷
  tone 8th   (f 5) ∷
  tone 8th   (a 5) ∷
  tone 8th   (c 6) ∷
  tone whole (f 6) ∷
  []

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

-- first 8 notes of Yamanote counterpoint transposed to F
yamanoteCP : List Note
yamanoteCP = map (transposeNote (-[1+ 7 ]) ∘ slowDown 2) (take 8 counterp)

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

soundness : List (Name × List Note)
soundness =
  (quote soundness~↑ , p i20p10a) ∷
  (quote soundness~↓ , i i20p10a) ∷
  (quote soundnessConv↑ , p subject) ∷
  (quote soundnessConv↓ , i subject) ∷
  (quote soundnessConv↑Term , p yamanoteCP) ∷
  (quote soundnessConv↓Term , i yamanoteCP) ∷
  []

conversion : List (Name × List Note)
conversion =
  (quote Definition.Conversion.Whnf.ne~↓ , ri canonsubject) ∷
  (quote Definition.Conversion.[~] , r canonsubject) ∷
  (quote Definition.Conversion.[↑] , p canonsubject) ∷
  (quote Definition.Conversion.[↑] , i canonsubject) ∷

  (quote Definition.Conversion._⊢_[conv↓]_.Empty-refl , p b4) ∷
  (quote Definition.Conversion._⊢_[conv↓]_.U-refl , i b4) ∷
  (quote Definition.Conversion._⊢_[conv↓]_.Unit-refl , r b4) ∷
  (quote Definition.Conversion._⊢_[conv↓]_.ne , ri b4) ∷
  (quote Definition.Conversion._⊢_[conv↓]_.Π-cong , p b5) ∷
  (quote Definition.Conversion._⊢_[conv↓]_.Σ-cong , i b5) ∷
  (quote Definition.Conversion._⊢_[conv↓]_.ℕ-refl , r b5) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.Empty-ins , ri b5) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.Unit-ins , p b6) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.ne-ins , i b6) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.suc-cong , r b6) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.univ , ri b6) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.zero-refl , p b7) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.Σ-η , i b7) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.η-eq , r b7) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.η-unit , ri b7) ∷
  (quote Definition.Conversion._⊢_[conv↓]_∷_.ℕ-ins , p b8) ∷

  (quote Definition.Conversion._⊢_~_↑_.Emptyrec-cong , i b8) ∷
  (quote Definition.Conversion._⊢_~_↑_.app-cong , r b8) ∷
  (quote Definition.Conversion._⊢_~_↑_.fst-cong , ri b8) ∷
  (quote Definition.Conversion._⊢_~_↑_.natrec-cong , p b9) ∷
  (quote Definition.Conversion._⊢_~_↑_.snd-cong , i b9) ∷
  (quote Definition.Conversion._⊢_~_↑_.var-refl , r b9) ∷
  []

typed : List (Name × List Note)
typed =
  (quote Definition.Typed.Consequences.InverseUniv.inverseUnivEq , ri b9) ∷
  (quote Definition.Typed.Consequences.NeTypeEq.neTypeEq , p b10) ∷
  (quote Definition.Typed.Consequences.Syntactic.syntacticEqTerm , i b10) ∷
  (quote Definition.Typed.Consequences.Syntactic.syntacticTerm , r b10) ∷
  (quote Definition.Typed.Consequences.Syntactic.syntacticΠ , ri b10) ∷
  (quote Definition.Typed.Consequences.Syntactic.syntacticΣ , p b1) ∷
  (quote Definition.Typed.Properties.subset* , i b1) ∷
  (quote Definition.Typed.Properties.subset*Term , r b1) ∷
  (quote Definition.Typed._⊢_.Emptyⱼ , ri b1) ∷
  (quote Definition.Typed._⊢_.Unitⱼ , p b2) ∷
  (quote Definition.Typed._⊢_.Uⱼ , i b2) ∷
  (quote Definition.Typed._⊢_.ℕⱼ , r b2) ∷
  (quote Definition.Typed._⊢_∷_.zeroⱼ , ri b2) ∷
  (quote Definition.Typed._⊢_≡_.refl , p b3) ∷
  (quote Definition.Typed._⊢_≡_.sym , i b3) ∷
  (quote Definition.Typed._⊢_≡_.trans , r b3) ∷
  (quote Definition.Typed._⊢_≡_.univ , ri b3) ∷
  (quote Definition.Typed._⊢_≡_.Π-cong , w (c 6)) ∷
  (quote Definition.Typed._⊢_≡_.Σ-cong , w (d 6)) ∷
  (quote Definition.Typed._⊢_≡_∷_.Emptyrec-cong , w (e 6)) ∷
  (quote Definition.Typed._⊢_≡_∷_.app-cong , w (f 6)) ∷
  (quote Definition.Typed._⊢_≡_∷_.conv , w (g 6)) ∷
  (quote Definition.Typed._⊢_≡_∷_.fst-cong , w (a 6)) ∷
  (quote Definition.Typed._⊢_≡_∷_.natrec-cong , w (b 6)) ∷
  (quote Definition.Typed._⊢_≡_∷_.refl , w (c 7)) ∷
  (quote Definition.Typed._⊢_≡_∷_.snd-cong , w (d 7)) ∷
  (quote Definition.Typed._⊢_≡_∷_.suc-cong , w (e 7)) ∷
  (quote Definition.Typed._⊢_≡_∷_.sym , w (f 7)) ∷
  (quote Definition.Typed._⊢_≡_∷_.trans , w (g 7)) ∷
  (quote Definition.Typed._⊢_≡_∷_.Σ-η , w (a 7)) ∷
  (quote Definition.Typed._⊢_≡_∷_.η-eq , w (b 7)) ∷
  (quote Definition.Typed._⊢_≡_∷_.η-unit , w (c 8)) ∷
  []

untyped : List (Name × List Note)
untyped =
  (quote Definition.Untyped.Con._∙_ , w (d 8)) ∷
  (quote Definition.Untyped.Empty , w (e 8)) ∷
  (quote Definition.Untyped.Term.var , w (f 8)) ∷
  (quote Definition.Untyped.U , w (g 8)) ∷
  (quote Definition.Untyped.Unit , w (a 8)) ∷
  (quote Definition.Untyped._[_] , w (b 8)) ∷
  (quote Definition.Untyped._[_]↑ , w (c 3)) ∷
  (quote Definition.Untyped._∘_ , w (d 3)) ∷
  (quote Definition.Untyped._▹▹_ , w (e 3)) ∷
  (quote Definition.Untyped.fst , w (f 3)) ∷
  (quote Definition.Untyped.snd , w (g 3)) ∷
  (quote Definition.Untyped.suc , w (a 3)) ∷
  (quote Definition.Untyped.wk1 , w (b 3)) ∷
  (quote Definition.Untyped.zero , w (c 4)) ∷
  (quote Definition.Untyped.Π_▹_ , w (d 4)) ∷
  (quote Definition.Untyped.Σ_▹_ , w (e 4)) ∷
  (quote Definition.Untyped.ℕ , w (f 4)) ∷
  []

misc : List (Name × List Note)
misc =
  (quote Fin , w (c 2)) ∷
  (quote Fin.zero , w (d 2)) ∷
  (quote Relation.Binary.PropositionalEquality.Core.subst , w (e 2)) ∷
  (quote fst , w (f 2)) ∷
  (quote lzero , w (g 2)) ∷
  (quote snd , w (a 2)) ∷
  (quote ℕ.suc , w (b 2)) ∷
  []

motives : List (Name × List Note)
motives = soundness ++ conversion ++ typed ++ untyped ++ misc

motif : Name → List Note
motif = lookup motives

max_stars_repo_name: halfaya/Music

max_issues_repo_name: halfaya/Music

max_forks_repo_name: halfaya/Music


text:
module FileIOEffect where

open import Effect
import IO.Primitive as IO
open import Data.String using (String)
open import Data.Bool using (Bool ; if_then_else_ ; false ; true)
open import Data.Unit using (⊤ ; tt)
open import Category.Monad using (RawMonad)
open import Level using (zero)
open import Data.List using (List ; _∷_ ; [])
open import Data.List.All using (All ; lookup ; _∷_ ; [])
open import Data.List.Any using (here ; there)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Membership-equality using (_∈_)
open import Data.Product using (Σ ; _,_ ; _×_)

data FileIOState : Set where
  opened closed : FileIOState

data FileHandle : Set where
  FH : String → FileHandle

data FileIOEff : Effect zero where
  `openFile  : String → FileIOEff Bool ⊤ λ ok → if ok then FileHandle else ⊤
  `closeFile : FileIOEff ⊤ FileHandle λ h → ⊤

-- Should we really use this now?
FileIO : EFFECT zero
FileIO = mkEff ⊤ FileIOEff

IOMonad : RawMonad IO.IO
IOMonad = record { return = IO.return ; _>>=_ = IO._>>=_ {zero} {zero}}

myOpClose : ∀ {m} → String → EffM m ⊤ (FileIO ∷ []) λ _ → (FileIO ∷ [])
myOpClose file = effect (here refl) (`openFile file) >>= λ
  { true → effect (here refl) `closeFile
  ; false → return tt}

main : IO.IO ⊤
main = run IO.IO (record { return = IO.return ; _>>=_ = IO._>>=_ }) (myOpClose ".gitignore") myEnv
  where
    FileIOHandler : Handler IO.IO FileIOEff
    FileIOHandler v (`openFile x) k = k true (FH x)
    FileIOHandler (FH x) `closeFile k = k tt tt
    myEnv : Env IO.IO (FileIO ∷ [])
    myEnv = (FileIOHandler , tt) ∷ []

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
{-
  This file contains cospans, cones, pullbacks and maps of cones in precategories.
-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Pullback where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Categories.Category

open Precategory

private
  variable
    ℓ ℓ' : Level

record Cospan (C : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  constructor cospan
  field
    l r vertex : Precategory.ob C
    s₁ : C [ l , vertex ]
    s₂ : C [ r , vertex ]

record Cone {C : Precategory ℓ ℓ'} (cspn : Cospan C) (c : ob C) : Type (ℓ-max ℓ ℓ') where
  constructor cone
  field
    p₁ : C [ c , (Cospan.l cspn)]
    p₂ : C [ c , (Cospan.r cspn)]
    sq : p₁ ⋆⟨ C ⟩ (Cospan.s₁ cspn) ≡ p₂ ⋆⟨ C ⟩ (Cospan.s₂ cspn)

record Pullback {C : Precategory ℓ ℓ'} (cspn : Cospan C) : Type (ℓ-max ℓ ℓ') where
  constructor pullback
  field
    pbOb : ob C
    pbCn : Cone cspn pbOb
    universal : ∀ {c' : ob C} (cn' : Cone cspn c')
              → ∃![ f ∈ C [ c' , pbOb ] ] Σ[ q ∈ Cone.p₁ cn' ≡ f ⋆⟨ C ⟩ (Cone.p₁ pbCn) ] (Cone.p₂ cn' ≡ f ⋆⟨ C ⟩ (Cone.p₂ pbCn))

-- extend a cone on c by a morphism c'→c using precomposition
coneMap : {C : Precategory ℓ ℓ'} {cspn : Cospan C} {c c' : ob C} (cn : Cone cspn c) (f : C [ c' , c ]) → Cone cspn c'
coneMap {C = C} {cospan _ _ _ s₁ s₂} (cone p₁ p₂ sq) f =
  cone (f ⋆⟨ C ⟩ p₁)  (f ⋆⟨ C ⟩ p₂) ((C .⋆Assoc f p₁ s₁) ∙∙ lPrecatWhisker {C = C} f (p₁ ⋆⟨ C ⟩ s₁) (p₂ ⋆⟨ C ⟩ s₂) sq ∙∙ sym (C .⋆Assoc f p₂ s₂))


text:
module Algebra.Theorems where

open import Algebra
open import Reasoning

+pre-idempotence : ∀ {A} {x : Graph A} -> x + x + ε ≡ x
+pre-idempotence {_} {x} =
  begin
    (x + x) + ε             ≡⟨ L (L (symmetry *right-identity)) ⟩
    (x * ε + x) + ε         ≡⟨ L (R (symmetry *right-identity)) ⟩
    (x * ε + x * ε) + ε     ≡⟨ R (symmetry *right-identity)     ⟩
    (x * ε + x * ε) + ε * ε ≡⟨ symmetry decomposition           ⟩
    (x * ε) * ε             ≡⟨ *right-identity                  ⟩
    x * ε                   ≡⟨ *right-identity                  ⟩
    x
  ∎

+identity : ∀ {A} {x : Graph A} -> x + ε ≡ x
+identity {_} {x} =
  begin
    x + ε                   ≡⟨ symmetry +pre-idempotence       ⟩
    ((x + ε) + (x + ε)) + ε ≡⟨ L +associativity                ⟩
    (((x + ε) + x) + ε) + ε ≡⟨ L (L (symmetry +associativity)) ⟩
    ((x + (ε + x)) + ε) + ε ≡⟨ L (L (R +commutativity))        ⟩
    ((x + (x + ε)) + ε) + ε ≡⟨ L (L +associativity)            ⟩
    (((x + x) + ε) + ε) + ε ≡⟨ L (symmetry +associativity)     ⟩
    ((x + x) + (ε + ε)) + ε ≡⟨ symmetry +associativity         ⟩
    (x + x) + ((ε + ε) + ε) ≡⟨ R +pre-idempotence              ⟩
    (x + x) + ε             ≡⟨ +pre-idempotence                ⟩
    x
  ∎

+idempotence : ∀ {A} {x : Graph A} -> x + x ≡ x
+idempotence = transitivity (symmetry +identity) +pre-idempotence

saturation : ∀ {A} {x : Graph A} -> x * x * x ≡ x * x
saturation {_} {x} =
  begin
    (x * x) * x             ≡⟨ decomposition  ⟩
    (x * x + x * x) + x * x ≡⟨ L +idempotence ⟩
    x * x + x * x           ≡⟨ +idempotence   ⟩
    x * x
  ∎

absorption : ∀ {A} {x y : Graph A} -> x * y + x + y ≡ x * y
absorption {_} {x} {y} =
  begin
    (x * y + x) + y         ≡⟨ L (R (symmetry *right-identity)) ⟩
    (x * y + x * ε) + y     ≡⟨ R (symmetry *right-identity)     ⟩
    (x * y + x * ε) + y * ε ≡⟨ symmetry decomposition           ⟩
    (x * y) * ε             ≡⟨ *right-identity                  ⟩
    x * y
  ∎

-- Subgraph relation
⊆reflexivity : ∀ {A} {x : Graph A} -> x ⊆ x
⊆reflexivity = +idempotence

⊆antisymmetry : ∀ {A} {x y : Graph A} -> x ⊆ y -> y ⊆ x -> x ≡ y
⊆antisymmetry p q = symmetry q      -- x = y + x
                 >> +commutativity  --     y + x = x + y
                 >> p               --             x + y = y

⊆transitivity : ∀ {A} {x y z : Graph A} -> x ⊆ y -> y ⊆ z -> x ⊆ z
⊆transitivity p q = symmetry
    (symmetry q              -- z = y + z
  >> L (symmetry p)          --     y + z = (x + y) + z
  >> symmetry +associativity --             (x + y) + z = x + (y + z)
  >> R q)                    --                           x + (y + z) = x + z

⊆least-element : ∀ {A} {x : Graph A} -> ε ⊆ x
⊆least-element = +commutativity >> +identity

⊆overlay : ∀ {A} {x y : Graph A} -> x ⊆ (x + y)
⊆overlay = +associativity >> L +idempotence

⊆connect : ∀ {A} {x y : Graph A} -> (x + y) ⊆ (x * y)
⊆connect = +commutativity >> +associativity >> absorption

⊆left-overlay-monotony : ∀ {A} {x y z : Graph A} -> x ⊆ y -> (x + z) ⊆ (y + z)
⊆left-overlay-monotony {_} {x} {y} {z} p =
  begin
    (x + z) + (y + z) ≡⟨ symmetry +associativity     ⟩
    x + (z + (y + z)) ≡⟨ R +commutativity            ⟩
    x + ((y + z) + z) ≡⟨ R (symmetry +associativity) ⟩
    x + (y + (z + z)) ≡⟨ R (R +idempotence)          ⟩
    x + (y + z)       ≡⟨ +associativity              ⟩
    (x + y) + z       ≡⟨ L p                         ⟩
    y + z
  ∎

⊆right-overlay-monotony : ∀ {A} {x y z : Graph A} -> x ⊆ y -> (z + x) ⊆ (z + y)
⊆right-overlay-monotony {_} {x} {y} {z} p =
  begin
    (z + x) + (z + y) ≡⟨ +associativity          ⟩
    ((z + x) + z) + y ≡⟨ L +commutativity        ⟩
    (z + (z + x)) + y ≡⟨ L +associativity        ⟩
    ((z + z) + x) + y ≡⟨ L (L +idempotence)      ⟩
    (z + x) + y       ≡⟨ symmetry +associativity ⟩
    z + (x + y)       ≡⟨ R p                     ⟩
    z + y
  ∎

⊆left-connect-monotony : ∀ {A} {x y z : Graph A} -> x ⊆ y -> (x * z) ⊆ (y * z)
⊆left-connect-monotony {_} {x} {y} {z} p =
  begin
    (x * z) + (y * z) ≡⟨ symmetry right-distributivity ⟩
    (x + y) * z       ≡⟨ L p                           ⟩
    y * z
  ∎

⊆right-connect-monotony : ∀ {A} {x y z : Graph A} -> x ⊆ y -> (z * x) ⊆ (z * y)
⊆right-connect-monotony {_} {x} {y} {z} p =
  begin
    (z * x) + (z * y) ≡⟨ symmetry left-distributivity ⟩
    z * (x + y)       ≡⟨ R p                          ⟩
    z * y
  ∎

⊆left-monotony : ∀ {A} {op : BinaryOperator} {x y z : Graph A} -> x ⊆ y -> apply op x z ⊆ apply op y z
⊆left-monotony {_} {+op} {x} {y} {z} p = ⊆left-overlay-monotony p
⊆left-monotony {_} {*op} {x} {y} {z} p = ⊆left-connect-monotony p

⊆right-monotony : ∀ {A} {op : BinaryOperator} {x y z : Graph A} -> x ⊆ y -> apply op z x ⊆ apply op z y
⊆right-monotony {_} {+op} {x} {y} {z} p = ⊆right-overlay-monotony p
⊆right-monotony {_} {*op} {x} {y} {z} p = ⊆right-connect-monotony p

max_stars_repo_name: asr/alga

max_issues_repo_name: asr/alga

max_forks_repo_name: asr/alga


text:
{-# OPTIONS --cubical #-}
module Multidimensional.Data.Dir.Base where

open import Cubical.Core.Primitives

-- "Direction" type for determining direction in spatial structures.
-- We interpret ↓ as 0 and ↑ as 1 when used in numerals in
-- numerical types.
data Dir : Type₀ where
  ↓ : Dir
  ↑ : Dir

caseDir : ∀ {ℓ} → {A : Type ℓ} → (ad au : A) → Dir → A
caseDir ad au ↓ = ad
caseDir ad au ↑ = au

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


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.Prelude
open import LibraBFT.Abstract.Types.EpochConfig
open        WithAbsVote

-- This module provides a convenient way for modules in other namespaces to import
-- everything from Abstract.

module LibraBFT.Abstract.Abstract
  (UID    : Set)
  (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁))
  (NodeId : Set)
  (𝓔  : EpochConfig UID NodeId)
  (𝓥  : VoteEvidence UID NodeId 𝓔)
  where
    open import LibraBFT.Abstract.Types                   UID        NodeId 𝓔    public
    open import LibraBFT.Abstract.RecordChain             UID _≟UID_ NodeId 𝓔 𝓥 public
    open import LibraBFT.Abstract.RecordChain.Assumptions UID _≟UID_ NodeId 𝓔 𝓥 public
    open import LibraBFT.Abstract.Records                 UID _≟UID_ NodeId 𝓔 𝓥 public
    open import LibraBFT.Abstract.Records.Extends         UID _≟UID_ NodeId 𝓔 𝓥 public
    open import LibraBFT.Abstract.Properties              UID _≟UID_ NodeId 𝓔 𝓥 public
    open import LibraBFT.Abstract.System                  UID _≟UID_ NodeId 𝓔 𝓥 public

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module Nats.Multiply.Distrib where

open import Nats
open import Equality
open import Function

open import Nats.Multiply.Comm
open import Nats.Add.Assoc
open import Nats.Add.Comm

------------------------------------------------------------------------
-- internal stuffs

private

  a*1+b=a+a*b : ∀ a b → a * suc b ≡ a + a * b
  a*1+b=a+a*b a b
    rewrite nat-multiply-comm a $ suc b
          | nat-multiply-comm a b
            = refl

  a*c+b*c=/a+b/*c : ∀ a b c → a * c + b * c ≡ (a + b) * c
  a*c+b*c=/a+b/*c a b    zero
    rewrite nat-multiply-comm a 0
          | nat-multiply-comm b 0
          | nat-multiply-comm (a + b) 0
            = refl
  a*c+b*c=/a+b/*c a b sc@(suc c)
    rewrite nat-add-comm a b
          | a*1+b=a+a*b a c
          | nat-add-assoc a (a * c) (b * sc)
          | nat-add-comm a $ a * c + b * sc
          | a*1+b=a+a*b b c
          | nat-multiply-comm (b + a) sc
          | nat-add-assoc b a $ c * (b + a)
          | nat-add-comm a $ c * (b + a)
          | sym $ nat-add-assoc b (c * (b + a)) a
          | nat-multiply-comm c $ b + a
          | sym $ a*c+b*c=/a+b/*c b a c
          | sym $ nat-add-assoc (a * c) b (b * c)
          | nat-add-comm (b * c) (a * c)
          | sym $ nat-add-assoc b (b * c) (a * c)
          | sym $ nat-add-assoc b (a * c) (b * c)
          | nat-add-comm b $ a * c
            = refl

------------------------------------------------------------------------
-- public aliases

nat-multiply-distrib : ∀ a b c → a * c + b * c ≡ (a + b) * c
nat-multiply-distrib = a*c+b*c=/a+b/*c


text:
module Categories.CoProducts where

open import Data.Sum hiding ([_,_])
open import Library hiding (_+_ ; _,_)
open import Categories

record CoProd {l m}(C : Cat {l}{m}) : Set (m ⊔ l) where
  open Cat C
  field _+_   : Obj -> Obj -> Obj
        inl   : ∀{A B} -> Hom A (A + B)
        inr   : ∀{A B} -> Hom B (A + B)
        [_,_] : ∀{A B C} -> Hom A C -> Hom B C -> Hom (A + B) C
        law1  : ∀{A B C}(f : Hom A C)(g : Hom B C) →
                comp [ f , g ] inl ≅ f
        law2  : ∀{A B C}(f : Hom A C)(g : Hom B C) →
                comp [ f , g ] inr ≅ g
        law3  : ∀{A B C}(f : Hom A C)(g : Hom B C)
                (h : Hom (A + B) C) →
                comp h inl ≅ f → comp h inr ≅ g → h ≅ [ f , g ]

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module Prelude.Number where

open import Agda.Builtin.FromNat public
open import Agda.Builtin.FromNeg public

NoNumConstraint : ∀ {a} {A : Set a} → Number A → Set a
NoNumConstraint Num = ∀ {n} → Number.Constraint Num n

NoNegConstraint : ∀ {a} {A : Set a} → Negative A → Set a
NoNegConstraint Neg = ∀ {n} → Negative.Constraint Neg n

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

module Cubical.Structures.Group.Morphism where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Structures.Group.Base

private
  variable
    ℓ ℓ' : Level

-- The following definition of GroupHom and GroupEquiv are level-wise heterogeneous.
-- This allows for example to deduce that G ≡ F from a chain of isomorphisms
-- G ≃ H ≃ F, even if H does not lie in the same level as G and F.

isGroupHom : (G : Group {ℓ}) (H : Group {ℓ'}) (f : ⟨ G ⟩ → ⟨ H ⟩) → Type _
isGroupHom G H f = (x y : ⟨ G ⟩) → f (x G.+ y) ≡ (f x H.+ f y) where
  module G = Group G
  module H = Group H

record GroupHom (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  constructor grouphom

  field
    fun : ⟨ G ⟩ → ⟨ H ⟩
    isHom : isGroupHom G H fun

record GroupEquiv (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  constructor groupequiv

  field
    eq : ⟨ G ⟩ ≃ ⟨ H ⟩
    isHom : isGroupHom G H (equivFun eq)

  hom : GroupHom G H
  hom = grouphom (equivFun eq) isHom

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
module Prelude.Equality where

open import Prelude.Decidable

open import Agda.Builtin.Equality public

record Eq {a} (A : Set a) : Set a where
  infix 4 _==_
  field
    _==_ : (x y : A) → Dec (x ≡ y)

open Eq {{...}} public

sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

infixr 0 _⟨≡⟩_ _⟨≡⟩ʳ_ _ʳ⟨≡⟩_ _ʳ⟨≡⟩ʳ_

trans : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl eq = eq

_⟨≡⟩_ = trans

_⟨≡⟩ʳ_ : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → z ≡ y → x ≡ z
eq ⟨≡⟩ʳ refl = eq

_ʳ⟨≡⟩_ : ∀ {a} {A : Set a} {x y z : A} → y ≡ x → y ≡ z → x ≡ z
refl ʳ⟨≡⟩ eq = eq

_ʳ⟨≡⟩ʳ_ : ∀ {a} {A : Set a} {x y z : A} → y ≡ x → z ≡ y → x ≡ z
refl ʳ⟨≡⟩ʳ refl = refl

infixl 4 cong _*≡_
syntax cong f eq = f $≡ eq
cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

_*≡_ : ∀ {a b} {A : Set a} {B : Set b} {f g : A → B} {x y} → f ≡ g → x ≡ y → f x ≡ g y
refl *≡ refl = refl

cong₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) {x₁ x₂ y₁ y₂} →
        x₁ ≡ x₂ → y₁ ≡ y₂ → f x₁ y₁ ≡ f x₂ y₂
cong₂ f refl refl = refl

transport : ∀ {a b} {A : Set a} (B : A → Set b) {x y} → x ≡ y → B x → B y
transport B refl bx = bx

transport₂ : ∀ {a b c} {A : Set a} {B : Set b} (C : A → B → Set c) {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → C x₁ y₁ → C x₂ y₂
transport₂ C refl refl cxy = cxy

-- Decidable equality helpers --

decEq₁ : ∀ {a b} {A : Set a} {B : Set b} {f : A → B} → (∀ {x y} → f x ≡ f y → x ≡ y) →
           ∀ {x y} → Dec (x ≡ y) → Dec (f x ≡ f y)
decEq₁ f-inj (yes refl) = yes refl
decEq₁ f-inj (no  neq)  = no λ eq → neq (f-inj eq)

decEq₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} {f : A → B → C} →
           (∀ {x y z w} → f x y ≡ f z w → x ≡ z) →
           (∀ {x y z w} → f x y ≡ f z w → y ≡ w) →
           ∀ {x y z w} → Dec (x ≡ y) → Dec (z ≡ w) → Dec (f x z ≡ f y w)
decEq₂ f-inj₁ f-inj₂ (no neq)    _         = no λ eq → neq (f-inj₁ eq)
decEq₂ f-inj₁ f-inj₂  _         (no neq)   = no λ eq → neq (f-inj₂ eq)
decEq₂ f-inj₁ f-inj₂ (yes refl) (yes refl) = yes refl

{-# INLINE decEq₁ #-}
{-# INLINE decEq₂ #-}

-- Equality reasoning --

infixr 0 eqReasoningStep eqReasoningStepʳ
infix  1 _∎

-- Giving the proofs in the reverse order means the values of x and y
-- are inferred before checking the x ≡ y proof. This leads to significant
-- performance improvements in some cases.

syntax eqReasoningStep x q p = x ≡⟨ p ⟩ q
eqReasoningStep : ∀ {a} {A : Set a} (x : A) {y z} → y ≡ z → x ≡ y → x ≡ z
x ≡⟨ refl ⟩ p = p

syntax eqReasoningStepʳ x q p = x ≡⟨ p ⟩ʳ q
eqReasoningStepʳ : ∀ {a} {A : Set a} (x : A) {y z} → y ≡ z → y ≡ x → x ≡ z
x ≡⟨ refl ⟩ʳ p = p

_∎ : ∀ {a} {A : Set a} (x : A) → x ≡ x
x ∎ = refl

-- Instances --

instance
  EqEq : ∀ {a} {A : Set a} {x y : A} → Eq (x ≡ y)
  _==_ {{EqEq}} refl refl = yes refl

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
data HasUniqueValues (A : Set) : List A → Set
 where
  [] : HasUniqueValues A []
  _∷_ : {x : A} → {xs : List A} → x ∉ xs → (uxs : HasUniqueValues A xs) → HasUniqueValues A (x ∷ xs)

record AList (A : Set) (B : Set) : Set
 where
  field
    domain : List A
    uniquedomain : HasUniqueValues A domain
    range : ∀ {x : A} → x ∈ domain → B

open AList

record Unifiable (F : Set) (T : Set) (U₁ U₂ : Set) (σ : (T → F) → F → F) : Set₁ where
  field
    _≈u≈_ : (φ₁ φ₂ : F) → Set
    unifier : (φ₁ φ₂ : F) → φ₁ ≈u≈ φ₂ → (F → F) × (F → F)
    unifier-law : (φ₁ φ₂ : F) → (=u= : φ₁ ≈u≈ φ₂) → (let u = unifier φ₁ φ₂ =u=) → (fst u) φ₁ ≡ (snd u) φ₂

mutual
  data FTerm : 𝕃 VariableName → Set
   where
    variable : (𝑥 : VariableName) → FTerm (𝕃⟦ 𝑥 ⟧)
    function : (𝑓 : FunctionName) → ..{𝑥s : 𝕃 VariableName} {arity : Nat} → (τs : FTerms 𝑥s arity) → FTerm 𝑥s

  data FTerms : 𝕃 VariableName → Nat → Set
   where
    [] : FTerms ∅ zero
    _∷_ : ∀ ..{𝑥s' 𝑥s : 𝕃 VariableName} → FTerm 𝑥s' → {n : Nat} → FTerms 𝑥s n → FTerms (union {m = VariableName} 𝑥s' 𝑥s) (⊹ n)

instance MembershipVariableNameFTerm : ∀ {𝑥s} → Membership VariableName (FTerm 𝑥s)
MembershipVariableNameFTerm = {!!}

record TotalIntersection {ℓ} (m : Set ℓ) (M : Set ℓ) ⦃ _ : Membership m M ⦄ : Set ℓ
 where
  field
    intersection : M → M → M
    intersectionLaw1 : ∀ {x : m} {X₁ X₂ : M} → x ∈ intersection X₁ X₂ → x ∈ X₁
    intersectionLaw2 : ∀ {x : m} {X₁ X₂ : M} → x ∈ intersection X₁ X₂ → x ∈ X₂
    intersectionLaw3 : ∀ {x : m} {X₁ X₂ : M} → x ∈ X₁ × x ∈ X₂ → x ∈ intersection X₁ X₂

open TotalIntersection ⦃ … ⦄

{-# DISPLAY TotalIntersection.intersection _ = intersection #-}

instance Intersection𝕃 : ∀ {ℓ} {A : Set ℓ} ⦃ _ : Eq A ⦄ → TotalIntersection A (𝕃 A)
Intersection𝕃 = {!!}

mutual
  subst : AList VariableName (∃ FTerm) → ∃ FTerm → ∃ FTerm
  subst x t@(.(✓ ∅) , variable 𝑥) with 𝑥 ∈? domain x
  … | yes x∈D = range x x∈D
  … | no x∉D = t
  subst x (fst₁ , function 𝑓 {𝑥s = 𝑥s} {arity = a} τs) with substs x a (𝑥s , τs)
  subst x (fst₁ , function 𝑓 {.fst₁} {arity₁} τs) | fst₂ , snd₁ = fst₂ , (function 𝑓 snd₁)

  substs : AList VariableName (∃ FTerm) → (a : Nat) → ∃ (flip FTerms a) → ∃ (flip FTerms a)
  substs x .0 (.∅ , []) = ∅ , []
  substs x .(suc _) (._ , (x₁ ∷ snd₁)) with {!subst x (_ , x₁)!}
  substs x .(suc _) (._ , (x₁ ∷ snd₁)) | sb = {!!}

-- indexed by the number of function symbols contained
data DTerm : Nat → Set
 where
  variable : (𝑥 : VariableName) → DTerm zero
  function : (𝑓 : FunctionName) → {arity : Nat} → (τs : Vec (∃ DTerm) arity) → DTerm (suc (sum (fst <$> vecToList τs)))

mutual
  substD : VariableName → ∃ DTerm → {n : Nat} → DTerm n → ∃ DTerm
  substD x x₁ (variable 𝑥) = ifYes 𝑥 ≟ x then x₁ else _ , variable 𝑥
  substD x x₁ (function 𝑓 τs) with substsD x x₁ τs
  substD x x₁ (function 𝑓 τs) | ss = suc (sum (fst <$> vecToList ss)) , function 𝑓 {_} ss

  substsD : VariableName → ∃ DTerm → {n : Nat} → Vec (Σ Nat DTerm) n → Vec (Σ Nat DTerm) n
  substsD x x₁ [] = []
  substsD x x₁ (x₂ ∷ x₃) with substD x x₁ (snd x₂) | substsD x x₁ x₃
  substsD x x₁ (x₂ ∷ x₃) | fst₁ , snd₁ | sss = (fst₁ , snd₁) ∷ sss

data HDTerm : Set where
  ⟨_⟩ : {n : Nat} → DTerm n → HDTerm

substituteD : (AList VariableName HDTerm) → HDTerm → HDTerm
substituteD = {!!}

amgu : HDTerm → HDTerm → (AList VariableName HDTerm) → Maybe (AList VariableName HDTerm)
amgu ⟨ variable 𝑥 ⟩ ⟨ variable 𝑥₁ ⟩ f = {!!}
amgu ⟨ variable 𝑥 ⟩ ⟨ function 𝑓 τs ⟩ f = {!!}
amgu ⟨ function 𝑓 τs ⟩ ⟨ variable 𝑥 ⟩ f = {!!}
amgu ⟨ function 𝑓 τs₁ ⟩ ⟨ function 𝑓₁ τs ⟩ f = {!!}

{-
data AList : 𝕃 VariableName → Set
 where
  [] : AList ∅
  _∷_ :
-}
record JohnUnification {𝑥s₁} (τ₁ : FTerm 𝑥s₁) {𝑥s₂} (τ₂ : FTerm 𝑥s₂) (_ : intersection {m = VariableName} 𝑥s₁ 𝑥s₂ ≡ ∅) : Set where
  field
    u₁ u₂ : AList VariableName (∃ FTerm)
    unification-law₁ : fst (subst u₁ (𝑥s₁ , τ₁)) ≡ fst (subst u₂ (𝑥s₂ , τ₂))
    unification-law₂ : snd (subst u₁ (𝑥s₁ , τ₁)) ≡ transport FTerm (sym unification-law₁) (snd (subst u₂ (𝑥s₂ , τ₂)))

record UnificationEquation (𝑥s : 𝕃 VariableName) : Set
 where
  field
    {lhs-terms} : 𝕃 VariableName
    lhs : FTerm lhs-terms
    {rhs-terms} : 𝕃 VariableName
    rhs : FTerm rhs-terms
    lhs∪rhs-terms : 𝑥s ≡ union {m = VariableName} lhs-terms rhs-terms

open UnificationEquation

number-of-variables-that-occur-more-than-once : ∀ {n-eqn} → Vec (∃ λ 𝑥s → UnificationEquation 𝑥s) n-eqn → Nat
number-of-variables-that-occur-more-than-once {zero} [] = 0
number-of-variables-that-occur-more-than-once {suc n-eqn} x = {!!}

number-of-function-symbols : ∀ {𝑥s} → FTerm 𝑥s → Nat
number-of-function-symbols = {!!}

record UnificationProblem (n-var n-lhs n-eqn : Nat) : Set
 where
  field
    equations : Vec (∃ λ 𝑥s → UnificationEquation 𝑥s) n-eqn
    n-var-law : number-of-variables-that-occur-more-than-once equations ≤ n-var
    n-lhs-law : (sum ∘ vecToList $ number-of-function-symbols ∘ lhs ∘ snd <$> equations) ≤ n-lhs

instance MembershipUnificationEquationUnificationProblem : ∀ {n-var n-lhs n-eqn 𝑥s} → Membership (UnificationEquation 𝑥s) (UnificationProblem n-var n-lhs n-eqn)
MembershipUnificationEquationUnificationProblem = {!!}

instance MembershipVariableNameUnificationProblem : ∀ {n-var n-lhs n-eqn} → Membership VariableName (UnificationProblem n-var n-lhs n-eqn)
MembershipVariableNameUnificationProblem = {!!}

deletable : ∀ {𝑥s} → UnificationEquation 𝑥s → Set
deletable = {!!}

deletable? : ∀ {𝑥s} → (eq : UnificationEquation 𝑥s) → Dec (deletable eq)
deletable? = {!!}

u-deletable? : ∀ {n-var n-lhs n-eqn} (up : UnificationProblem n-var n-lhs n-eqn) → Dec (∃ λ 𝑥s → ∃ λ (εq : UnificationEquation 𝑥s) → deletable εq × εq ∈ up)
u-deletable? {n-var} {n-lhs} {zero} up = no {!!}
u-deletable? {n-var} {n-lhs} {suc n-eqn} up = {!!}

deleteRule : ∀ {n-var n-lhs n-eqn} {up : UnificationProblem n-var n-lhs (suc n-eqn)} {𝑥s} {εq : UnificationEquation 𝑥s} → deletable εq → εq ∈ up → UnificationProblem n-var n-lhs n-eqn
deleteRule = {!!}

decomposable : ∀ {𝑥s} → UnificationEquation 𝑥s → Set
decomposable = {!!}

decomposable? : ∀ {𝑥s} → (eq : UnificationEquation 𝑥s) → Dec (decomposable eq)
decomposable? = {!!}

u-decomposable? : ∀ {n-var n-lhs n-eqn} (up : UnificationProblem n-var (suc n-lhs) n-eqn) → Dec (∃ λ 𝑥s → ∃ λ (εq : UnificationEquation 𝑥s) → decomposable εq × εq ∈ up)
u-decomposable? = {!!}

decomposeRule : ∀ {n-var n-lhs n-eqn} {up : UnificationProblem n-var (suc n-lhs) n-eqn} {𝑥s} {εq : UnificationEquation 𝑥s} → decomposable εq → εq ∈ up → UnificationProblem n-var n-lhs n-eqn
decomposeRule = {!!}

swapable : ∀ {𝑥s} → UnificationEquation 𝑥s → Set
swapable = {!!}

swapable? : ∀ {𝑥s} → (eq : UnificationEquation 𝑥s) → Dec (swapable eq)
swapable? = {!!}

u-swapable? : ∀ {n-var n-lhs n-eqn} (up : UnificationProblem n-var (suc n-lhs) n-eqn) → Dec (∃ λ 𝑥s → ∃ λ (εq : UnificationEquation 𝑥s) → swapable εq × εq ∈ up)
u-swapable? = {!!}

swapRule : ∀ {n-var n-lhs n-eqn} {up : UnificationProblem n-var (suc n-lhs) n-eqn} {𝑥s} {εq : UnificationEquation 𝑥s} → swapable εq → εq ∈ up → UnificationProblem n-var n-lhs n-eqn
swapRule = {!!}

eliminatable : ∀ {n-var n-lhs n-eqn} {up : UnificationProblem n-var n-lhs n-eqn} {𝑥s} {εq : UnificationEquation 𝑥s} → (εq∈up : εq ∈ up) → Set
eliminatable = {!!}

u-eliminatable? : ∀ {n-var n-lhs n-eqn} (up : UnificationProblem (suc n-var) n-lhs n-eqn) → Dec (∃ λ 𝑥s → ∃ λ (εq : UnificationEquation 𝑥s) → ∃ λ (εq∈up : εq ∈ up) → eliminatable {up = up} {εq = εq} εq∈up)
u-eliminatable? = {!!}

eliminateRule : ∀ {n-var n-lhs n-eqn} {up : UnificationProblem (suc n-var) n-lhs n-eqn} {𝑥s} {εq : UnificationEquation 𝑥s} → {εq∈up : εq ∈ up} → eliminatable {up = up} {εq = εq} εq∈up → UnificationProblem n-var n-lhs n-eqn
eliminateRule = {!!}

conflictable : ∀ {𝑥s} → UnificationEquation 𝑥s → Set
conflictable = {!!}

conflictable? : ∀ {𝑥s} → (εq : UnificationEquation 𝑥s) → Dec (conflictable εq)
conflictable? = {!!}

u-conflictable? : ∀ {n-var n-lhs n-eqn} (up : UnificationProblem n-var n-lhs n-eqn) → Dec (∃ λ 𝑥s → ∃ λ (εq : UnificationEquation 𝑥s) → conflictable εq × εq ∈ up)
u-conflictable? = {!!}

checkable : ∀ {𝑥s} → UnificationEquation 𝑥s → Set
checkable = {!!}

checkable? : ∀ {𝑥s} → (εq : UnificationEquation 𝑥s) → Dec (checkable εq)
checkable? = {!!}

u-checkable? : ∀ {n-var n-lhs n-eqn} (up : UnificationProblem n-var n-lhs n-eqn) → Dec (∃ λ 𝑥s → ∃ λ (εq : UnificationEquation 𝑥s) → checkable εq × εq ∈ up)
u-checkable? = {!!}

postulate
  substituteFormula : (VariableName → Term) → Formula → Formula

record Unifier' : Set
 where
  field
    unifier-left unifier-right : VariableName → Term

open Unifier'

record _Unifies_and_ (υ : Unifier') (φ₁ φ₂ : Formula) : Set
 where
  field
    unification-law : substituteFormula (unifier-left υ) φ₁ ≡ substituteFormula (unifier-right υ) φ₂


text:
{-# OPTIONS --experimental-irrelevance #-}

record NonStrict (A : Set) : Set where
  constructor [_]
  field
    ..! : A

open NonStrict

map-ns : {A B : Set} (f : A → B) → NonStrict A → NonStrict B
map-ns f [ x ] = [ f x ]

open import Agda.Builtin.Nat

data Vec (A : Set) : NonStrict Nat → Set where
  []  : Vec A [ 0 ]
  _∷_ : .{n : Nat} → A → Vec A [ n ] → Vec A [ suc n ]

map : ∀ {A B} .{n} (f : A → B) → Vec A [ n ] → Vec B [ n ]
map f [] = []
map f (x ∷ xs) = (f x) ∷ (map f xs)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
data Nat : Set where
  zero : Nat
  suc : (n : Nat) → Nat

test₁ : (n : Nat) → Nat
test₁ n with zero
... | x = {!x!}

data Tree : Set where
  leaf : Tree
  node : Tree → Tree → Tree

test₂ : (n : Tree) → Tree
test₂ n₁ with leaf
... | n = {!n!}


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Sub | S

type
  L : 0-ary
  T : 0-ary

term
  vr : L  ->  T
  sb : L.T  T  ->  T

theory
  (C) x y : T |> sb (a. x[], y[]) = x[]
  (L) x : T |> sb (a. vr(a), x[]) = x[]
  (R) a : L  x : L.T |> sb (b. x[b], vr(a[])) = x[a[]]
  (A) x : (L,L).T  y : L.T  z : T |> sb (a. sb (b. x[a,b], y[a]), z[]) = sb (b. sb (a. x[a, b], z[]), sb (a. y[a], z[]))
-}

module Sub.Signature where

open import SOAS.Context

-- Type declaration
data ST : Set where
  L : ST
  T : ST

open import SOAS.Syntax.Signature ST public
open import SOAS.Syntax.Build ST public

-- Operator symbols
data Sₒ : Set where
  vrₒ sbₒ : Sₒ

-- Term signature
S:Sig : Signature Sₒ
S:Sig = sig λ
  {  vrₒ  → (⊢₀ L) ⟼₁ T
  ;  sbₒ  → (L ⊢₁ T) , (⊢₀ T) ⟼₂ T
  }

open Signature S:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- Andreas, 2017-05-24, issue #2590
-- Making variables visible by case splitting in with-clauses

-- {-# OPTIONS -v interaction.case:20 #-}
-- {-# OPTIONS -v reify:100 #-}
-- {-# OPTIONS -v tc.display:100 #-}

open import Agda.Builtin.Nat

test1 : {x : Nat} → Nat
test1 with Set
... | q = {!.x!}  -- C-c C-c

-- Expected result:
-- test1 {x} | q = ?

data Any (x : Nat) : Set where
  any : Any x

postulate
  zonk : ∀{x} → Any x → Nat

test2 : {x y : Nat} → Any y → Nat
test2 p with zonk p
... | q = {!.y!} -- C-c C-c

-- Expected result:
-- test2 {y = y} p | q = ?

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- Fixpoint combinators
------------------------------------------------------------------------

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

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

module Partiality-algebra.Fixpoints where

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

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

open import Partiality-algebra.Monotone
open import Partiality-algebra.Omega-continuous
import Partiality-algebra.Properties as PAP

open [_⟶_]⊑

-- The development below, up to fix-is-least, is (very similar to)
-- Kleene's fixed-point theorem.

private
 module Fix₀ {a p q} {A : Type a} {P : Partiality-algebra p q A} where

  open Partiality-algebra P
  open PAP P

  -- Repeated composition of a monotone function with itself.

  comp : [ P ⟶ P ]⊑ → ℕ → [ P ⟶ P ]⊑
  comp f zero    = id⊑
  comp f (suc n) = f ∘⊑ comp f n

  -- Pre-composition with the function is equal to post-composition
  -- with the function.

  pre≡post : ∀ f n → comp f n ∘⊑ f ≡ f ∘⊑ comp f n
  pre≡post f zero    = f  ∎
  pre≡post f (suc n) =
    (f ∘⊑ comp f n) ∘⊑ f  ≡⟨ ∘⊑-assoc f (comp f n) ⟩
    f ∘⊑ (comp f n ∘⊑ f)  ≡⟨ cong (f ∘⊑_) $ pre≡post f n ⟩∎
    f ∘⊑ (f ∘⊑ comp f n)  ∎

  -- Repeated application of a monotone function to never.

  app : [ P ⟶ P ]⊑ → ℕ → T
  app f n = function (comp f n) never

  -- An increasing sequence consisting of repeated applications of the
  -- given monotone function to never.

  fix-sequence : [ P ⟶ P ]⊑ → Increasing-sequence
  fix-sequence f = app f , fix-sequence-increasing
    where
    abstract
      fix-sequence-increasing :
        ∀ n → function (comp f n) never ⊑ function (f ∘⊑ comp f n) never
      fix-sequence-increasing n =
        function (comp f n) never               ⊑⟨ monotone (comp f n) (never⊑ (function f never)) ⟩
        function (comp f n) (function f never)  ⊑⟨⟩
        function (comp f n ∘⊑ f) never          ≡⟨ cong (λ g → function g never) $ pre≡post f n ⟩⊑
        function (f ∘⊑ comp f n) never          ■

  -- Taking the tail of this sequence amounts to the same thing as
  -- applying the function to each element in the sequence.

  tailˢ-fix-sequence :
    (f : [ P ⟶ P ]⊑) →
    tailˢ (fix-sequence f) ≡ [ f $ fix-sequence f ]-inc
  tailˢ-fix-sequence f =
    _↔_.to equality-characterisation-increasing λ _ → refl

  -- The sequence has the same least upper bound as the sequence you get
  -- if you apply the function to each element of the sequence.

  ⨆-fix-sequence :
    (f : [ P ⟶ P ]⊑) →
    ⨆ (fix-sequence f) ≡ ⨆ [ f $ fix-sequence f ]-inc
  ⨆-fix-sequence f =
    ⨆ (fix-sequence f)            ≡⟨ sym $ ⨆tail≡⨆ _ ⟩
    ⨆ (tailˢ (fix-sequence f))    ≡⟨ cong ⨆ (tailˢ-fix-sequence f) ⟩∎
    ⨆ [ f $ fix-sequence f ]-inc  ∎

  -- A fixpoint combinator.

  fix : [ P ⟶ P ]⊑ → T
  fix f = ⨆ (fix-sequence f)

  -- The fixpoint combinator produces fixpoints for ω-continuous
  -- arguments.

  fix-is-fixpoint-combinator :
    (fω : [ P ⟶ P ]) →
    let f : [ P ⟶ P ]⊑
        f = [_⟶_].monotone-function fω
    in fix f ≡ function f (fix f)
  fix-is-fixpoint-combinator fω =
    fix f                            ≡⟨⟩
    ⨆ (fix-sequence f)               ≡⟨ ⨆-fix-sequence f ⟩
    ⨆ [ f $ fix-sequence f ]-inc     ≡⟨ sym $ [_⟶_].ω-continuous fω _ ⟩
    function f (⨆ (fix-sequence f))  ≡⟨⟩
    function f (fix f)               ∎
    where
    f : [ P ⟶ P ]⊑
    f = [_⟶_].monotone-function fω

  -- The result of the fixpoint combinator is smaller than or equal to
  -- every post-fixpoint.

  fix-is-least :
    (f : [ P ⟶ P ]⊑) →
    ∀ x → function f x ⊑ x → fix f ⊑ x
  fix-is-least f x fx⊑x = least-upper-bound _ _ lemma
    where
    lemma : ∀ n → function (comp f n) never ⊑ x
    lemma zero    = never⊑ x
    lemma (suc n) =
      function (f ∘⊑ comp f n) never          ⊑⟨⟩
      function f (function (comp f n) never)  ⊑⟨ monotone f (lemma n) ⟩
      function f x                            ⊑⟨ fx⊑x ⟩■
      x                                       ■

  -- A restricted homomorphism property.

  comp-∘ : ∀ f n → comp (f ∘⊑ f) n ≡ comp f n ∘⊑ comp f n
  comp-∘ f zero    = id⊑  ∎
  comp-∘ f (suc n) =
    (f ∘⊑ f) ∘⊑ comp (f ∘⊑ f) n         ≡⟨ cong ((f ∘⊑ f) ∘⊑_) (comp-∘ f n) ⟩
    (f ∘⊑ f) ∘⊑ (comp f n ∘⊑ comp f n)  ≡⟨ lemma f f (comp f n) _ ⟩
    f ∘⊑ ((f ∘⊑ comp f n) ∘⊑ comp f n)  ≡⟨ cong ((_∘⊑ comp f n) ∘ (f ∘⊑_)) $ sym $ pre≡post f n ⟩
    f ∘⊑ ((comp f n ∘⊑ f) ∘⊑ comp f n)  ≡⟨ sym $ lemma f (comp f n) f _ ⟩∎
    (f ∘⊑ comp f n) ∘⊑ (f ∘⊑ comp f n)  ∎
    where
    lemma : (f g h k : [ P ⟶ P ]⊑) →
            (f ∘⊑ g) ∘⊑ (h ∘⊑ k) ≡ f ∘⊑ ((g ∘⊑ h) ∘⊑ k)
    lemma f g h k =
      (f ∘⊑ g) ∘⊑ (h ∘⊑ k)  ≡⟨ ∘⊑-assoc f g ⟩
      f ∘⊑ (g ∘⊑ (h ∘⊑ k))  ≡⟨ cong (f ∘⊑_) $ ∘⊑-assoc g h ⟩∎
      f ∘⊑ ((g ∘⊑ h) ∘⊑ k)  ∎

  -- The function comp f is homomorphic with respect to _+_/_∘⊑_.

  comp-+∘ : ∀ f m {n} → comp f (m + n) ≡ comp f m ∘⊑ comp f n
  comp-+∘ f zero    {n} = comp f n  ∎
  comp-+∘ f (suc m) {n} =
    f ∘⊑ comp f (m + n)          ≡⟨ cong (f ∘⊑_) $ comp-+∘ f m ⟩
    f ∘⊑ (comp f m ∘⊑ comp f n)  ≡⟨ ∘⊑-assoc f (comp f m) ⟩∎
    (f ∘⊑ comp f m) ∘⊑ comp f n  ∎

  -- Taking steps that are "twice as large" does not affect the end
  -- result.

  fix-∘ : (f : [ P ⟶ P ]⊑) → fix (f ∘⊑ f) ≡ fix f
  fix-∘ f = antisymmetry
    (least-upper-bound _ _ λ n →
       function (comp (f ∘⊑ f) n) never       ≡⟨ cong (λ f → function f never) $ comp-∘ f n ⟩⊑
       function (comp f n ∘⊑ comp f n) never  ≡⟨ cong (λ f → function f never) $ sym $ comp-+∘ f n ⟩⊑
       function (comp f (n + n)) never        ⊑⟨ upper-bound (fix-sequence f) (n + n) ⟩■
       ⨆ (fix-sequence f)                     ■)
    (⨆-mono λ n →
       function (comp f n) never                        ⊑⟨ monotone (comp f n) (never⊑ _) ⟩
       function (comp f n) (function (comp f n) never)  ⊑⟨⟩
       function (comp f n ∘⊑ comp f n) never            ≡⟨ cong (λ f → function f never) $ sym $ comp-∘ f n ⟩⊑
       function (comp (f ∘⊑ f) n) never                 ■)

open Fix₀

-- N-ary Scott induction.

module N-ary
  (open Partiality-algebra)
  {a p q r} n
  (As : Fin n → Type a)
  (Ps : ∀ i → Partiality-algebra p q (As i))
  (P : (∀ i → T (Ps i)) → Type r)
  (P⊥ : P (λ i → never (Ps i)))
  (P⨆ : (ss : ∀ i → Increasing-sequence (Ps i)) →
        (∀ n → P (λ i → _[_] (Ps i) (ss i) n)) →
        P (λ i → ⨆ (Ps i) (ss i)))
  (fs : ∀ i → [ Ps i ⟶ Ps i ]⊑)
  where

  -- Generalised.

  fix-induction′ :
    (∀ n → P (λ i → app (fs i) n) → P (λ i → app (fs i) (suc n))) →
    P (fix ∘ fs)
  fix-induction′ step =                       $⟨ lemma ⟩
    (∀ n → P (λ i → app (fs i) n))            ↝⟨ P⨆ _ ⟩
    P (λ i → ⨆ (Ps i) (fix-sequence (fs i)))  ↝⟨ id ⟩□
    P (fix ∘ fs)                              □
    where
    lemma : ∀ n → P (λ i → function (comp (fs i) n) (never (Ps i)))
    lemma zero    = P⊥
    lemma (suc n) =                             $⟨ lemma n ⟩
      P (λ i → app (fs i) n)                    ↝⟨ step n ⟩□
      P (λ i → function (fs i) (app (fs i) n))  □

  -- Basic.

  fix-induction :
    (∀ xs → P xs → P (λ i → function (fs i) (xs i))) →
    P (fix ∘ fs)
  fix-induction step =
    fix-induction′ (λ n → step (λ i → app (fs i) n))

open N-ary public

module Fix {a p q} {A : Type a} {P : Partiality-algebra p q A} where

  open Partiality-algebra P

  -- Unary Scott induction.

  fix-induction₁ :
    ∀ {r}
    (Q : T → Type r) →
    Q never →
    (∀ s → (∀ n → Q (s [ n ])) → Q (⨆ s)) →
    (f : [ P ⟶ P ]⊑) →
    (∀ x → Q x → Q (function f x)) →
    Q (fix f)
  fix-induction₁ Q Q⊥ Q⨆ f step =
    fix-induction
      1
      [ const A ,        ⊥-elim    ]
      [ const P , (λ i → ⊥-elim i) ]
      (Q ∘ (_$ fzero))
      Q⊥
      (Q⨆ ∘ (_$ fzero))
      [ const f , (λ x → ⊥-elim x) ]
      (step ∘ (_$ fzero))

  open Fix₀ {P = P} public

open Fix public

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


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

module sets.nat.algebra where

open import equality.core
open import algebra.monoid.core
open import sets.nat.core
open import sets.nat.properties

+-monoid : Monoid _
+-monoid = record
  { carrier = ℕ
  ; is-mon = record
    { id = λ _ → 0
    ; _∘_ = _+_
    ; left-unit = +-left-unit
    ; right-unit = +-right-unit
    ; associativity = λ x y z → +-associativity z y x } }

*-monoid : Monoid _
*-monoid = record
  { carrier = ℕ
  ; is-mon = record
    { id = λ _ → 1
    ; _∘_ = _*_
    ; left-unit = *-left-unit
    ; right-unit = *-right-unit
    ; associativity = λ x y z → *-associativity z y x } }

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module List.Permutation.Base.Bag (A : Set) where

open import Data.List
open import Data.List.Any as Any
open import Data.List.Any.BagAndSetEquality
open import Data.List.Any.Properties
open import Data.Sum renaming (_⊎_ to _∨_)
open import Function
open import Function.Inverse hiding (sym ; _∘_ ; id)
open import Function.Related as Related hiding (_∼[_]_)
open import List.Permutation.Base A
import Relation.Binary.EqReasoning as EqR
open import Relation.Binary.PropositionalEquality as P hiding (sym)

open Any.Membership-≡
open EqR ([ bag ]-Equality A)
open Related.EquationalReasoning renaming (_∎ to _□)

infix 4 _≈-bag_

_≈-bag_ : ∀ {a} {A : Set a} → List A → List A → Set a
xs ≈-bag ys = xs ∼[ bag ] ys

sym-≈-bag : {xs ys : List A} → xs ≈-bag ys → ys ≈-bag xs
sym-≈-bag {xs} {ys} xs≈ys {z} = record
  { to         = Inverse.from xs≈ys
  ; from       = Inverse.to xs≈ys
  ; inverse-of = record
    { left-inverse-of  = Inverse.right-inverse-of xs≈ys
    ; right-inverse-of = Inverse.left-inverse-of xs≈ys
    }
  }

refl-≈-bag : {xs : List A} → xs ≈-bag xs
refl-≈-bag {xs} = begin xs ∎

∨↔ : ∀{a b}{A : Set a}{B : Set b} → (A ∨ B) ↔ (B ∨ A)
∨↔ = record
  { to         = P.→-to-⟶ ∨→
  ; from       = P.→-to-⟶ ∨→
  ; inverse-of = record
    { left-inverse-of  = v→∘v→
    ; right-inverse-of = v→∘v→
    }
  }
  where
  ∨→ : ∀{a b}{A : Set a}{B : Set b} → (A ∨ B) → (B ∨ A)
  ∨→ (inj₁ x) = inj₂ x
  ∨→ (inj₂ x) = inj₁ x

  v→∘v→ : ∀{a b}{A : Set a}{B : Set b}(a∨b : A ∨ B) → ∨→ (∨→ a∨b) ≡ a∨b
  v→∘v→ (inj₁ _) = refl
  v→∘v→ (inj₂ _) = refl

xy≈-bag-yx : {x y : A} → x ∷ y ∷ [] ≈-bag y ∷ x ∷ []
xy≈-bag-yx {x} {y} {z} =
  z ∈ x ∷ y ∷ [] ↔⟨ sym $ ++↔ {xs = x ∷ []} {ys = y ∷ []} ⟩
  (z ∈ x ∷ [] ∨ z ∈ y ∷ []) ↔⟨ ∨↔ ⟩
  (z ∈ y ∷ [] ∨ z ∈ x ∷ []) ↔⟨ ++↔ ⟩
  z ∈ y ∷ x ∷ [] □

lemma-/-≈-bag : {y : A}{xs ys : List A} → xs / y ⟶ ys → xs ≈-bag (y ∷ ys)
lemma-/-≈-bag /head = refl-≈-bag
lemma-/-≈-bag (/tail {x} {y} {xs} {ys} xs/y⟶ys) = begin
  x ∷ xs ≈⟨ ∷-cong refl (lemma-/-≈-bag xs/y⟶ys) ⟩
  x ∷ y ∷ ys ≈⟨ ++-cong xy≈-bag-yx refl-≈-bag ⟩
  y ∷ x ∷ ys ∎

lemma-∼-≈-bag : {xs ys : List A} → xs ∼ ys → xs ≈-bag ys
lemma-∼-≈-bag ∼[] = refl-≈-bag
lemma-∼-≈-bag (∼x {x} {xs} {ys} {xs'} {ys'} xs/x⟶xs' ys/x⟶ys' xs'∼ys') = begin
  xs ≈⟨ lemma-/-≈-bag xs/x⟶xs' ⟩
  x ∷ xs' ≈⟨ ∷-cong refl (lemma-∼-≈-bag xs'∼ys') ⟩
  x ∷ ys' ≈⟨ sym-≈-bag (lemma-/-≈-bag ys/x⟶ys') ⟩
  ys ∎

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module DataRecordInductive where

module NotMutual where

  record Nil (A : Set) : Set where
    constructor []

  record Cons (A X : Set) : Set where
    constructor _∷_
    field head : A
          tail : X
  open Cons

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

  -- works
  module Constr where

    map : {A B : Set} → (A → B) → List A → List B
    map f (nil   [])      = nil []
    map f (cons (x ∷ xs)) = cons (f x ∷ map f xs)

  -- works, since projections are size preserving
  module Proj where

    map : {A B : Set} → (A → B) → List A → List B
    map f (nil   _) = nil []
    map f (cons  p) = cons (f (head p) ∷ map f (tail p))

module Mutual where

  mutual

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

    record Nil (A : Set) : Set where
      constructor []

    -- since Cons is inductive, we are not creating colists
    record Cons (A : Set) : Set where
      inductive
      constructor _∷_
      field head : A
            tail : List A

  open Cons

  -- works
  module Constr where

    map : {A B : Set} → (A → B) → List A → List B
    map f (nil   [])      = nil []
    map f (cons (x ∷ xs)) = cons (f x ∷ map f xs)

  -- works, since projections of an inductive record are size-preserving
  module Proj where

    map : {A B : Set} → (A → B) → List A → List B
    map f (nil   _) = nil []
    map f (cons  p) = cons (f (head p) ∷ map f (tail p))


text:
module Tactic.Monoid.Reflect where

open import Prelude
open import Tactic.Reflection
open import Tactic.Reflection.Match

open import Control.Monad.Zero
open import Control.Monad.State
open import Container.Traversable

open import Tactic.Monoid.Exp
open import Tactic.Reflection.Parse renaming (parseEqn to parseEq)

private
  data ExpF (A : Set) : Set where
    eVar  : Nat → ExpF A
    eZero : ExpF A
    ePlus : A → A → ExpF A

  instance
    FunctorExpF : Functor ExpF
    fmap {{FunctorExpF}} _ (eVar i) = eVar i
    fmap {{FunctorExpF}} _ eZero = eZero
    fmap {{FunctorExpF}} f (ePlus x y) = ePlus (f x) (f y)

    TraversableExpF : Traversable ExpF
    traverse {{TraversableExpF}} f (eVar i)    = pure (eVar i)
    traverse {{TraversableExpF}} f eZero       = pure eZero
    traverse {{TraversableExpF}} f (ePlus x y) = ⦇ ePlus (f x) (f y) ⦈

  mkExp : ExpF Exp → Exp
  mkExp (eVar i)    = var i
  mkExp eZero       = ε
  mkExp (ePlus x y) = x ⊕ y

module _ (match : Term → Maybe (ExpF Term)) where
  parseEqn : Term → ParseTerm TC (Exp × Exp)
  parseEqn v = parseEq eVar match mkExp v

  parseGoal : Term → TC ((Exp × Exp) × List Term)
  parseGoal v = runParse (parseEqn v)

private
  match<> : ∀ {a} {A : Set a} → Monoid A → TC (Term → Maybe (Vec Term 2))
  match<> {A = A} dict = do
    `A    ← quoteTC A
    `plus ← quoteTC (Monoid._<>_ dict)
    extendContext (vArg `A) $
      extendContext (vArg $ weaken 1 `A) $
      match 2 <$> normalise (safeApply (weaken 2 `plus) (vArg (safe (var 0 []) _) ∷
                                                         vArg (safe (var 1 []) _) ∷ []))

  matchEmpty : ∀ {a} {A : Set a} → Monoid A → TC (Term → Bool)
  matchEmpty dict = do
    v ← quoteTC (Monoid.mempty dict)
    pure (isYes ∘ (v ==_))

monoidMatcher : ∀ {a} {A : Set a} → Monoid A → TC (Term → Maybe (ExpF Term))
monoidMatcher dict = withNormalisation true $ do
  isZ ← matchEmpty dict
  isP ← match<> dict
  pure λ v →
       guard! (isZ v) (pure eZero) <|> do
         x ∷ y ∷ [] ←  isP v
         pure (ePlus x y)

private
  lookupEnv : ∀ {a} {A : Set a} {{_ : Monoid A}} → List A → Nat → A
  lookupEnv xs i = maybe mempty id (index xs i)

  quoteList : List Term → Term
  quoteList = foldr (λ x xs → con₂ (quote List._∷_) x xs) (con₀ (quote List.[]))

quoteEnv : Term → List Term → Term
quoteEnv dict xs = def (quote lookupEnv) (iArg dict ∷ vArg (quoteList xs) ∷ [])