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

module Categories.Category.Instance.Properties.Posets where

open import Level using (_⊔_; Lift; lift)
open import Data.Unit using (⊤; tt)
open import Data.Product as Prod using (_,_; <_,_>) renaming (_×_ to _|×|_)
open import Function using (flip)
open import Relation.Binary using (IsPartialOrder; Poset)
open import Relation.Binary.OrderMorphism
  using (id; _∘_) renaming (_⇒-Poset_ to _⇒_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Categories.Category
import Categories.Category.CartesianClosed as CCC
import Categories.Category.CartesianClosed.Canonical as Canonical
open import Categories.Category.Instance.Posets
open import Categories.Functor using (Functor; Endofunctor)
open import Categories.Utils.Product

open Poset renaming (_≈_ to ₍_₎_≈_; _≤_ to ₍_₎_≤_)
open _⇒_

-- The pointwise partial order on order preserving maps.
--
-- (See the Exponential module below for the definition of the
-- exponential/hom object based on this order.)

module Pointwise {a₁ a₂ a₃ b₁ b₂ b₃} {A : Poset a₁ a₂ a₃} {B : Poset b₁ b₂ b₃}
  where

  infix 4 _≤°_

  _≤°_ : (f g : A ⇒ B) → Set (a₁ ⊔ b₃)
  f ≤° g = ∀ {x} → ₍ B ₎ fun f x ≤ fun g x

  ≤°-isPartialOrder : IsPartialOrder _≗_ _≤°_
  ≤°-isPartialOrder = record
    { isPreorder      = record
      { isEquivalence = ≗-isEquivalence
      ; reflexive     = λ f≗g → reflexive B f≗g
      ; trans         = λ f≤g g≤h → trans B f≤g g≤h
      }
    ; antisym         = λ f≤g g≤f → antisym B f≤g g≤f
    }

  module ≤° = IsPartialOrder ≤°-isPartialOrder

open Pointwise

-- Poset has a duality involution: the poset obtained by reversing the
-- partial order is again a poset.

module Opposite where

  -- NOTE: we flip the direction of the underlying equality _≈_ as
  -- well, so that |op (op A) ≡ A| definitionally.

  op : ∀ {a₁ a₂ a₃} → Poset a₁ a₂ a₃ → Poset a₁ a₂ a₃
  op A = record
    { Carrier           = Carrier A
    ; _≈_               = flip ₍ A ₎_≈_
    ; _≤_               = flip ₍ A ₎_≤_
    ; isPartialOrder    = record
      { isPreorder      = record
        { isEquivalence = record
          { refl        = Eq.refl A
          ; sym         = Eq.sym A
          ; trans       = flip (Eq.trans A)
          }
        ; reflexive     = reflexive A
        ; trans         = flip (trans A)
        }
      ; antisym         = antisym A
      }
    }

  module _ {a₁ a₂ a₃} {A : Poset a₁ a₂ a₃} where

    op-involutive : op (op A) ≡ A
    op-involutive = ≡.refl

    module _ {b₁ b₂ b₃} {B : Poset b₁ b₂ b₃} where

      op₁ : A ⇒ B → op A ⇒ op B
      op₁ f = record { fun = fun f ; monotone = monotone f }

      op₂ : {f g : A ⇒ B} → f ≤° g → op₁ g ≤° op₁ f
      op₂ f≤g = f≤g

  -- op induces an endofunctor on Posets

  op-functor : ∀ {a₁ a₂ a₃} → Endofunctor (Posets a₁ a₂ a₃)
  op-functor = record
    { F₀           = op
    ; F₁           = op₁
    ; identity     = λ {A}       → Eq.refl A
    ; homomorphism = λ {_ _ C}   → Eq.refl C
    ; F-resp-≈     = λ {_ B} x≈y → Eq.sym B x≈y
    }

  module op {a₁ a₂ a₃} = Functor (op-functor {a₁} {a₂} {a₃})

-- The category of posets has terminal objects.

module Terminals where

  unit : ∀ a₁ a₂ a₃ → Poset a₁ a₂ a₃
  unit a₁ a₂ a₃ = record
    { Carrier = Lift a₁ ⊤
    ; _≈_     = λ _ _ → Lift a₂ ⊤
    ; _≤_     = λ _ _ → Lift a₃ ⊤
    }

  module _ {a₁ a₂ a₃ b₁ b₂ b₃} {B : Poset b₁ b₂ b₃} where

    ! : B ⇒ unit a₁ a₂ a₃
    ! = _

    !-unique : (f : B ⇒ unit a₁ a₂ a₃) → ! ≗ f
    !-unique f = _

open Terminals

-- The category of posets has products.

module Products where

  infixr 2 _×_

  _×_ : ∀ {a₁ a₂ a₃ b₁ b₂ b₃} →
        Poset a₁ a₂ a₃ → Poset b₁ b₂ b₃ → Poset (a₁ ⊔ b₁) (a₂ ⊔ b₂) (a₃ ⊔ b₃)
  A × B = record
    { Carrier           = Carrier A |×| Carrier B
    ; _≈_               = ₍ A ₎_≈_ -< _|×|_ >- ₍ B ₎_≈_
    ; _≤_               = ₍ A ₎_≤_ -< _|×|_ >- ₍ B ₎_≤_
    ; isPartialOrder    = record
      { isPreorder      = record
        { isEquivalence = record
          { refl        = Eq.refl A , Eq.refl B
          ; sym         = Prod.map (Eq.sym A) (Eq.sym B)
          ; trans       = Prod.zip (Eq.trans A) (Eq.trans B)
          }
        ; reflexive     = Prod.map (reflexive A) (reflexive B)
        ; trans         = Prod.zip (trans A) (trans B)
        }
      ; antisym         = Prod.zip (antisym A) (antisym B)
      }
    }

  module _ {a₁ a₂ a₃ b₁ b₂ b₃} {A : Poset a₁ a₂ a₃} {B : Poset b₁ b₂ b₃} where

    π₁ : (A × B) ⇒ A
    π₁ = record { fun = Prod.proj₁ ; monotone = Prod.proj₁ }

    π₂ : (A × B) ⇒ B
    π₂ = record { fun = Prod.proj₂ ; monotone = Prod.proj₂ }

    module _ {c₁ c₂ c₃} {C : Poset c₁ c₂ c₃} where

      infix 11 ⟨_,_⟩

      ⟨_,_⟩ : C ⇒ A → C ⇒ B → C ⇒ (A × B)
      ⟨ f , g ⟩ = record
        { fun      = < fun f , fun g >
        ; monotone = < monotone f , monotone g >
        }

      π₁-comp  : {f : C ⇒ A} {g : C ⇒ B} → π₁ ∘ ⟨ f , g ⟩ ≗ f
      π₁-comp = Eq.refl A

      π₂-comp  : {f : C ⇒ A} {g : C ⇒ B} → π₂ ∘ ⟨ f , g ⟩ ≗ g
      π₂-comp = Eq.refl B

      ⟨,⟩-unique : {f : C ⇒ A} {g : C ⇒ B} {h : C ⇒ (A × B)} →
                   π₁ ∘ h ≗ f → π₂ ∘ h ≗ g → ⟨ f , g ⟩ ≗ h
      ⟨,⟩-unique hyp₁ hyp₂ {x} = Eq.sym A hyp₁ , Eq.sym B hyp₂

  infixr 2 _×₁_

  _×₁_ : ∀ {a₁ a₂ a₃ b₁ b₂ b₃ c₁ c₂ c₃ d₁ d₂ d₃}
         {A : Poset a₁ a₂ a₃} {B : Poset b₁ b₂ b₃}
         {C : Poset c₁ c₂ c₃} {D : Poset d₁ d₂ d₃} →
         A ⇒ C → B ⇒ D → (A × B) ⇒ (C × D)
  f ×₁ g = ⟨ f ∘ π₁ , g ∘ π₂ ⟩

open Products

-- The category of posets has exponential objects.
--
-- It's easier to define exponentials with respect to the *canonical*
-- product.  The more generic version can then be given by appealing
-- to uniqueness (up to iso) of products.

module Exponentials where

  -- Use arrow rather than exponential notation for readability.

  infixr 9 _⇨_

  _⇨_ : ∀ {a₁ a₂ a₃ b₁ b₂ b₃} → Poset a₁ a₂ a₃ → Poset b₁ b₂ b₃ →
        Poset (a₁ ⊔ a₃ ⊔ b₁ ⊔ b₃) (a₁ ⊔ b₂) (a₁ ⊔ b₃)
  A ⇨ B = record
    { Carrier           = A ⇒ B
    ; _≈_               = _≗_
    ; _≤_               = _≤°_
    ; isPartialOrder    = ≤°-isPartialOrder
    }

  module _ {a₁ a₂ a₃ b₁ b₂ b₃} {A : Poset a₁ a₂ a₃} {B : Poset b₁ b₂ b₃} where

    eval : (A ⇨ B × A) ⇒ B
    eval = record
      { fun      = λ{ (f , x) → fun f x }
      ; monotone = λ{ {f , _} (f≤g , x≤y) → trans B (monotone f x≤y) f≤g }
      }

    module _ {c₁ c₂ c₃} {C : Poset c₁ c₂ c₃} where

      curry : (C × A) ⇒ B → C ⇒ (A ⇨ B)
      curry f = record
        { fun        = λ x → record
          { fun      = Prod.curry (fun f) x
          ; monotone = Prod.curry (monotone f) (refl C)
          }
        ; monotone   = λ x≤y → monotone f (x≤y , refl A)
        }

      eval-comp : {f : (C × A) ⇒ B} → eval ∘ (curry f ×₁ id) ≗ f
      eval-comp = Eq.refl B

      curry-resp-≗ : {f g : (C × A) ⇒ B} → f ≗ g → curry f ≗ curry g
      curry-resp-≗ hyp = hyp

      curry-unique : {f : C ⇒ (A ⇨ B)} {g : (C × A) ⇒ B} →
                     eval ∘ (f ×₁ id) ≗ g → f ≗ curry g
      curry-unique hyp = hyp

open Exponentials

-- The category of posets is cartesian closed.

Posets-CanonicallyCCC : ∀ {a} → Canonical.CartesianClosed (Posets a a a)
Posets-CanonicallyCCC = record
  { !            = !
  ; π₁           = π₁
  ; π₂           = π₂
  ; ⟨_,_⟩        = ⟨_,_⟩
  ; !-unique     = !-unique
  ; π₁-comp      = λ {_ _ f _ g}   → π₁-comp {f = f} {g}
  ; π₂-comp      = λ {_ _ f _ g}   → π₂-comp {f = f} {g}
  ; ⟨,⟩-unique   = λ {_ _ f _ h g} → ⟨,⟩-unique {f = f} {g} {h}
  ; eval         = eval
  ; curry        = curry
  ; eval-comp    = λ {_ _ _ f}   → eval-comp {f = f}
  ; curry-resp-≈ = λ {_ _ _ f g} → curry-resp-≗ {f = f} {g}
  ; curry-unique = λ {_ _ _ f g} → curry-unique {f = f} {g}
  }

module CanonicallyCartesianClosed {a} =
  Canonical.CartesianClosed (Posets-CanonicallyCCC {a})

Posets-CCC : ∀ {a} → CCC.CartesianClosed (Posets a a a)
Posets-CCC = Canonical.Equivalence.fromCanonical _ Posets-CanonicallyCCC

module CartesianClosed {a} = CCC.CartesianClosed (Posets-CCC {a})

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
------------------------------------------------------------------------------
-- Totality properties respect to Bool
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.BoolI where

open import FOTC.Base
open import FOTC.Data.Bool.Type
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Program.SortList.SortList

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

le-ItemList-Bool : ∀ {item is} → N item → ListN is → Bool (le-ItemList item is)
le-ItemList-Bool {item} Nitem lnnil = subst Bool (sym (le-ItemList-[] item)) btrue
le-ItemList-Bool {item} Nitem (lncons {i} {is} Ni Lis) =
  subst Bool
        (sym (le-ItemList-∷ item i is))
        (&&-Bool (le-Bool Nitem Ni) (le-ItemList-Bool Nitem Lis))

-- See the ATP version.
postulate le-Lists-Bool : ∀ {is js} → ListN is → ListN js → Bool (le-Lists is js)

-- See the ATP version.
postulate ordList-Bool : ∀ {is} → ListN is → Bool (ordList is)

le-ItemTree-Bool : ∀ {item t} → N item → Tree t →
                  Bool (le-ItemTree item t)
le-ItemTree-Bool {item} _ tnil = subst Bool (sym (le-ItemTree-nil item)) btrue
le-ItemTree-Bool {item} Nitem (ttip {i} Ni) =
  subst Bool (sym (le-ItemTree-tip item i)) (le-Bool Nitem Ni)
le-ItemTree-Bool {item} Nitem  (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) =
    subst Bool
          (sym (le-ItemTree-node item t₁ i t₂))
          (&&-Bool (le-ItemTree-Bool Nitem Tt₁) (le-ItemTree-Bool Nitem Tt₂))

le-TreeItem-Bool : ∀ {t item} → Tree t → N item → Bool (le-TreeItem t item)
le-TreeItem-Bool {item = item} tnil _ =
  subst Bool (sym (le-TreeItem-nil item)) btrue
le-TreeItem-Bool {item = item} (ttip {i} Ni) Nitem =
  subst Bool (sym (le-TreeItem-tip i item)) (le-Bool Ni Nitem)
le-TreeItem-Bool {item = item} (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) Nitem =
  subst Bool
        (sym (le-TreeItem-node t₁ i t₂ item))
        (&&-Bool (le-TreeItem-Bool Tt₁ Nitem) (le-TreeItem-Bool Tt₂ Nitem))

ordTree-Bool : ∀ {t} → Tree t → Bool (ordTree t)
ordTree-Bool tnil          = subst Bool (sym ordTree-nil) btrue
ordTree-Bool (ttip {i} Ni) = subst Bool (sym (ordTree-tip i)) btrue
ordTree-Bool (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) =
  subst Bool
        (sym (ordTree-node t₁ i t₂))
        (&&-Bool (ordTree-Bool Tt₁)
                 (&&-Bool (ordTree-Bool Tt₂)
                          (&&-Bool (le-TreeItem-Bool Tt₁ Ni)
                                   (le-ItemTree-Bool Ni Tt₂))))

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Issue279 where

record Unit : Set where
  constructor tt

open Unit tt  -- this no longer brings tt into scope

test : Unit
test = tt

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED.
------------------------------------------------------------------------

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

-- Disabled to prevent warnings from deprecated monoid solver
{-# OPTIONS --warn=noUserWarning #-}

module Data.List.Solver where

{-# WARNING_ON_IMPORT
"Data.List.Solver was deprecated in v1.3.
Use the new reflective Tactic.MonoidSolver instead."
#-}

import Algebra.Solver.Monoid as Solver
open import Data.List.Properties using (++-monoid)

------------------------------------------------------------------------
-- A module for automatically solving propositional equivalences
-- containing _++_

module ++-Solver {a} {A : Set a} =
  Solver (++-monoid A) renaming (id to nil)


text:
open import Common.Prelude
open import Common.Reflection

postulate
  X Y : Set

isX : QName → Bool
isX (quote X) = true
isX _ = false

main : IO Unit
main = putStrLn ((if isX (quote X) then "yes" else "no") +S+
                 (if isX (quote Y) then "yes" else "no"))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.TypePrecategory where

open import Cubical.Foundations.Prelude

open import Cubical.Categories.Category.Precategory

open Precategory

-- TYPE precategory has types as objects
module _ ℓ where
  TYPE : Precategory (ℓ-suc ℓ) ℓ
  TYPE .ob           = Type ℓ
  TYPE .Hom[_,_] A B = A → B
  TYPE .id           = λ x → x
  TYPE ._⋆_ f g      = λ x → g (f x)
  TYPE .⋆IdL f       = refl
  TYPE .⋆IdR f       = refl
  TYPE .⋆Assoc f g h = refl

max_stars_repo_name: FernandoLarrain/cubical


text:
open import Type

module Graph.Category {ℓ₁ ℓ₂} {V : Type{ℓ₁}} where

open import Data.Tuple as Tuple using ()
open import Functional
open import Logic.Propositional
import      Lvl
open import Graph{ℓ₁}{ℓ₂}(V)
open import Graph.Walk{ℓ₁}{ℓ₂}{V}
open import Graph.Walk.Proofs{ℓ₁}{ℓ₂}{V}
open import Relator.Equals
open import Relator.Equals.Proofs
open import Relator.Equals.Proofs.Equiv
open import Structure.Category
import      Structure.Categorical.Names as Names
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Transitivity

module _ (_⟶_ : Graph) where
  private variable a b c d : V
  private variable e e₁ e₂ e₃ : a ⟶ b
  private variable w w₁ w₂ w₃ : Walk(_⟶_) a b

  Walk-transitivity-raw-identityₗ-raw : (Walk-transitivity-raw at w ≡ w)
  Walk-transitivity-raw-identityₗ-raw = [≡]-intro

  Walk-transitivity-raw-identityᵣ-raw : (Walk-transitivity-raw w at ≡ w)
  Walk-transitivity-raw-identityᵣ-raw {a}{.a} {Walk.at}                  = [≡]-intro
  Walk-transitivity-raw-identityᵣ-raw {a}{c}  {Walk.prepend {b = b} e w} = congruence₁(prepend e) (Walk-transitivity-raw-identityᵣ-raw {b}{c} {w})

  Walk-transitivity-raw-associativity-raw : Names.Morphism.Associativity{Obj = V}(\{w} → Walk-transitivity-raw{_⟶_ = _⟶_}{z = w})
  Walk-transitivity-raw-associativity-raw {a}{b}{c}{d}  {Walk.at}          {w₂}{w₃} = [≡]-intro
  Walk-transitivity-raw-associativity-raw {a}{b}{c}{d}  {Walk.prepend e w₁}{w₂}{w₃} = congruence₁(prepend e) (Walk-transitivity-raw-associativity-raw {a}{b}{c}{_} {w₁}{w₂}{w₃})

  instance
    Walk-transitivity-raw-identityₗ : Morphism.Identityₗ{Obj = V}(\{w} → Walk-transitivity-raw{z = w})(at)
    Walk-transitivity-raw-identityₗ = Morphism.intro Walk-transitivity-raw-identityₗ-raw

  instance
    Walk-transitivity-raw-identityᵣ : Morphism.Identityᵣ{Obj = V}(\{w} → Walk-transitivity-raw{z = w})(at)
    Walk-transitivity-raw-identityᵣ = Morphism.intro Walk-transitivity-raw-identityᵣ-raw

  instance
    Walk-transitivity-raw-identity : Morphism.Identity{Obj = V}(\{w} → Walk-transitivity-raw{_⟶_ = _⟶_}{z = w})(at)
    Walk-transitivity-raw-identity = [∧]-intro Walk-transitivity-raw-identityₗ Walk-transitivity-raw-identityᵣ

  -- The category arising from a graph by its vertices and walks.
  -- Note that `Walk` is defined so that every sequence of edges have an unique walk. For example `ReflexitiveTransitiveClosure` (a relation equivalent to a walk) would not work.
  free-category : Category(Walk(_⟶_))
  Category._∘_ free-category = swap(transitivity(Walk(_⟶_)))
  Category.id  free-category = reflexivity(Walk(_⟶_))
  BinaryOperator.congruence (Category.binaryOperator free-category) [≡]-intro [≡]-intro = [≡]-intro
  Morphism.Associativity.proof (Category.associativity free-category) {a}{b}{c}{d} {w₁}{w₂}{w₃} = symmetry(_≡_) (Walk-transitivity-raw-associativity-raw {d}{c}{b}{a} {w₃}{w₂}{w₁})
  Morphism.Identityₗ.proof (Tuple.left  (Category.identity free-category)) = Walk-transitivity-raw-identityᵣ-raw
  Morphism.Identityᵣ.proof (Tuple.right (Category.identity free-category)) = Walk-transitivity-raw-identityₗ-raw

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --universe-polymorphism #-}
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}
-- {-# OPTIONS --verbose tc.term.args.ifs:15 #-}
-- {-# OPTIONS --verbose tc.checkArgs:15 #-}

module 12-constraintFamilies where

open import Level
open import Function
open import Data.Unit
open import Data.List
open import Data.Product hiding (map)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

record ConstrainedFunctor {c} (Constraint : Set → Set c)
  (f : (A : Set) → Set) : Set (suc c) where
  field
    fmap : ∀ {A B : Set} → {{cA : Constraint A}} → {{cB : Constraint B}} →
      (A → B) → f A → f B

listConstrainedFunctor : ConstrainedFunctor (const ⊤) List
listConstrainedFunctor = record { fmap = map }

postulate
  sort : {A : Set} → {{ordA : ∃ λ (_<_ : A → A → Set) → IsStrictTotalOrder {A = A} _≡_ _<_}} →
         List A → List A

⋯ : ∀ {a} {A : Set a} {{a : A}} → A
⋯ {{a}} = a

sortedListConstrainedFunctor : ConstrainedFunctor (λ A → ∃ λ (_<_ : A → A → Set) → IsStrictTotalOrder _≡_ _<_) List
sortedListConstrainedFunctor = record { fmap = λ {{x}} {{y}} → map' {{x}} {{y}} } where
  map' : {A B : Set} → {{ordA : ∃ λ (_<_ : A → A → Set) → (IsStrictTotalOrder _≡_ _<_)}} →
         {{ordB : ∃ λ (_<_ : B → B → Set) → (IsStrictTotalOrder _≡_ _<_)}} →
         (A → B) → List A → List B
  map' f = sort ∘′ map f

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --without-K #-}
module NTypes.Nat where

open import NTypes
open import PathOperations
open import PathStructure.Nat
open import Types

ℕ-isSet : isSet ℕ
ℕ-isSet = ind
  (λ m → (n : ℕ) (p q : m ≡ n) → p ≡ q)
  (λ m-1 r → ind (λ n → (p q : suc m-1 ≡ n) → p ≡ q)
    (λ n-1 r′ p′ q′
      → split-eq p′ ⁻¹
      · ap (ap suc)
        (r _
          (merge-path m-1 n-1
            (tr (F (suc m-1)) p′ (F-lemma (suc m-1))))
          (merge-path m-1 n-1
            (tr (F (suc m-1)) q′ (F-lemma (suc m-1)))))
      · split-eq q′
      )
    (λ p q → 0-elim (split-path _ _ p)))
  (ind (λ n → (p q : 0 ≡ n) → p ≡ q)
    (λ _ _ p q → 0-elim (split-path _ _ p))
    (λ     p q → split-eq p ⁻¹ · split-eq q))
  where
  split-eq : {x y : ℕ} → _
  split-eq {x} {y} = π₂ (π₂ (π₂ (split-merge-eq {x} {y})))

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


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

open import Algebra

module Data.FingerTree.Measures
  {r m}
  (ℳ : Monoid r m)
  where

open import Level using (_⊔_)

open Monoid ℳ renaming (Carrier to 𝓡)
open import Data.List as List using (List; _∷_; [])
open import Data.Product
open import Function

-- | A measure.
record σ {a} (Σ : Set a) : Set (a ⊔ r) where field μ : Σ → 𝓡
open σ ⦃ ... ⦄
{-# DISPLAY σ.μ _ = μ #-}

instance
  σ-List : ∀ {a} {Σ : Set a} → ⦃ _ : σ Σ ⦄ → σ (List Σ)
  μ ⦃ σ-List ⦄ = List.foldr (_∙_ ∘ μ) ε

-- A "fiber" (I think) from the μ function.
--
-- μ⟨ Σ ⟩≈ 𝓂 means "There exists a Σ such that μ Σ ≈ 𝓂"
infixl 2 _⇑[_]
record μ⟨_⟩≈_ {a} (Σ : Set a) ⦃ _ : σ Σ ⦄ (𝓂 : 𝓡) : Set (a ⊔ r ⊔ m) where
  constructor _⇑[_]
  field
    𝓢 : Σ
    .𝒻 : μ 𝓢 ≈ 𝓂
open μ⟨_⟩≈_ public

-- Construct a measured value without any transformations of the measure.
infixl 2 _⇑
_⇑ : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ (𝓢 : Σ) → μ⟨ Σ ⟩≈ μ 𝓢
𝓢 (x ⇑) = x
𝒻 (x ⇑) = refl
{-# INLINE _⇑ #-}

-- These combinators allow for a kind of easoning syntax over the measures.
-- The first is used like so:
--
--   xs ≈[ assoc _ _ _ ]
--
-- Which will have the type:
--
--   μ⟨ Σ ⟩≈ x ∙ y ∙ z → μ⟨ Σ ⟩≈ (x ∙ y) ∙ z
--
-- The second does the same:
--
--   xs ≈[ assoc _ _ _ ]′
--
-- However, when used in a chain, it typechecks after the ones used to its
-- left. This means you can call the solver on the left.
--
--   xs ≈[ ℳ ↯ ] ≈[ assoc _ _ _ ]′
infixl 2 _≈[_] ≈-rev
_≈[_] : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ {x : 𝓡} → μ⟨ Σ ⟩≈ x → ∀ {y} → .(x ≈ y) → μ⟨ Σ ⟩≈ y
𝓢 (xs ≈[ y≈z ]) = 𝓢 xs
𝒻 (xs ≈[ y≈z ]) = trans (𝒻 xs) y≈z
{-# INLINE _≈[_] #-}

≈-rev : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ {x : 𝓡} → ∀ {y} → .(x ≈ y) → μ⟨ Σ ⟩≈ x → μ⟨ Σ ⟩≈ y
𝓢 (≈-rev y≈z xs) = 𝓢 xs
𝒻 (≈-rev y≈z xs) = trans (𝒻 xs) y≈z
{-# INLINE ≈-rev #-}

syntax ≈-rev y≈z x↦y = x↦y ≈[ y≈z ]′

infixr 2 ≈-right
≈-right : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ {x : 𝓡} → μ⟨ Σ ⟩≈ x → ∀ {y} → .(x ≈ y) → μ⟨ Σ ⟩≈ y
≈-right (x ⇑[ x≈y ]) y≈z = x ⇑[ trans x≈y y≈z ]

syntax ≈-right x x≈ = [ x≈ ]≈ x

infixr 1 _↤_
-- A memoized application of μ
record ⟪_⟫ {a} (Σ : Set a) ⦃ _ : σ Σ ⦄ : Set (a ⊔ r ⊔ m) where
  constructor _↤_
  field
    𝔐 : 𝓡
    𝓕 : μ⟨ Σ ⟩≈ 𝔐
open ⟪_⟫ public

-- Construct the memoized version
⟪_⇓⟫ : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → Σ → ⟪ Σ ⟫
𝔐 ⟪ x ⇓⟫ = μ x
𝓕 ⟪ x ⇓⟫ = x ⇑

instance
  σ-⟪⟫ : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → σ ⟪ Σ ⟫
  μ ⦃ σ-⟪⟫ ⦄ = 𝔐

open import Algebra.FunctionProperties _≈_

-- This section allows us to use the do-notation to clean up proofs.
-- First, we construct arguments:
infixl 2 arg-syntax
record Arg {a} (Σ : Set a) ⦃ _ : σ Σ ⦄ (𝓂 : 𝓡) (f : 𝓡 → 𝓡) : Set (m ⊔ r ⊔ a) where
  constructor arg-syntax
  field
    .⟨f⟩ : Congruent₁ f
    arg : μ⟨ Σ ⟩≈ 𝓂
open Arg

syntax arg-syntax (λ sz → e₁) xs = xs [ e₁ ⟿ sz ]
-- This syntax is meant to be used like so:
--
--   do x ← xs [ a ∙> (s <∙ b) ⟿ s ]
--
-- And it means "the size of the variable I'm binding here will be stored in this
-- part of the expression". See, for example, the listToTree function:
--
--   listToTree [] = empty ⇑
--   listToTree (x ∷ xs) = [ ℳ ↯ ]≈ do
--     ys ← listToTree xs [ μ x ∙> s ⟿ s ]
--     x ◂ ys
--
infixl 1 _>>=_
_>>=_ : ∀ {a b} {Σ₁ : Set a} {Σ₂ : Set b} ⦃ _ : σ Σ₁ ⦄ ⦃ _ : σ Σ₂ ⦄ {𝓂 f}
      → Arg Σ₁ 𝓂 f
      → ((x : Σ₁) → .⦃ x≈ : μ x ≈ 𝓂 ⦄ → μ⟨ Σ₂ ⟩≈ f (μ x))
      → μ⟨ Σ₂ ⟩≈ f 𝓂
arg-syntax cng xs >>= k = k (𝓢 xs) ⦃ 𝒻 xs ⦄ ≈[ cng (𝒻 xs) ]
{-# INLINE _>>=_ #-}

-- Inside the lambda generated by do notation, we can only pass one argument.
-- So, to provide the proof (if needed)
_≈?_ : ∀ x y → ⦃ x≈y : x ≈ y ⦄ → x ≈ y
_≈?_ _ _ ⦃ x≈y ⦄ = x≈y

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Everything

module Test.ProblemWithSym where

module _ {a} {A : ¶ → Set a} where

  private AList = Descender⟨ A ⟩

  instance

    test-works : Transassociativity.class (flip AList) Proposequality transitivity
    test-works .⋆ f g h = symmetry (transassociativity h g f)

    test-fails : Transassociativity.class (flip AList) Proposequality transitivity
    test-fails .⋆ f g h = symmetry (transassociativity h g f) -- FIXME this was problematic when using a version of symmetry which did not include a negative argument in .⋆ It deserves explanation.

    test-hole : Transassociativity.class (flip AList) Proposequality transitivity
    test-hole .⋆ f g h = symmetry {!!}


text:
module Ag01 where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

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

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

_*_ : ℕ → ℕ → ℕ
zero *  n = zero
suc m * n = n + (m * n)

_ : 3 * 4 ≡ 12
_ = refl

_^_ : ℕ → ℕ → ℕ
m ^ 0       = 1
m ^ (suc n) = m * (m ^ n)

_ : 3 ^ 4 ≡ 81
_ = refl

_∸_ : ℕ → ℕ → ℕ
m ∸ zero = m
zero ∸ suc n = zero
suc m ∸ suc n = m ∸ n

infixl 6 _+_ _∸_
infixl 7 _*_

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

inc : Bin → Bin
inc nil    = nil
inc (x1 b) = x0 (inc b)
inc (x0 b) = x1 b

_ : inc (x0 nil) ≡ (x1 nil)
_ = refl

_ : inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
_ = refl

to : ℕ → Bin
to zero = x0 nil
to (suc m) = inc (to m)

from : Bin → ℕ
from nil      = zero
from (x1 b)   = suc (2 * (from b))
from (x0 b)   = 2 * (from b)

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
module Kind (Gnd : Set)(U : Set)(T : U -> Set) where

open import Basics
open import Pr
open import Nom

data Kind : Set where
  Ty    : Gnd -> Kind
  _|>_  : Kind -> Kind -> Kind
  Pi    : (u : U) -> (T u -> Kind) -> Kind

infixr 60 _|>_


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

module Miscellaneous.FiniteMultiset where

import      Lvl
open import Data.List using (List)
import      Data.List.Functions as List
open import Data.List.Relation.Permutation
open import Functional as Fn
open import Type.Cubical
open import Type.Cubical.Quotient
open import Type
open import Type.Identity

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}
private variable x y z : T

FiniteMultiset : Type{ℓ} → Type
FiniteMultiset(T) = Quotient(_permutes_ {T = T})

pattern ∅ = class List.∅

add : T → FiniteMultiset(T) → FiniteMultiset(T)
add x = Quotient-recursion (class ∘ (x List.⊰_)) (class-extensionalityₗ ∘ prepend)

_∪•_ : FiniteMultiset(T) → T → FiniteMultiset(T)
_∪•_ = Fn.swap add
infixr 1000 _∪•_

open import Data.Boolean
open import Data.List.Relation.Membership as List using (use ; skip)
open import Numeral.Natural
open import Relator.Equals.Proofs.Equivalence
open import Type.Cubical.Path.Equality

private variable l : FiniteMultiset(T)

count : (T → Bool) → FiniteMultiset(T) → ℕ
count f = Quotient-function(List.count f) ⦃ Proofs.permutes-countᵣ-function ⦄

satisfiesAny : (T → Bool) → FiniteMultiset(T) → Bool
satisfiesAny f = Quotient-function(List.satisfiesAny f) ⦃ Proofs.permutes-satisfiesAny-functionᵣ ⦄

-- _∈_ : T → FiniteMultiset(T) → Type
-- _∈_ x = Quotient-function (List._∈_ x) ⦃ {!!} ⦄


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

open import Categories.Category

module Categories.Diagram.Duality {o ℓ e} (C : Category o ℓ e) where

open Category C

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

open import Categories.Functor
open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation.Dinatural

open import Categories.Object.Initial
open import Categories.Object.Terminal
open import Categories.Object.Duality
open import Categories.Diagram.Equalizer op
open import Categories.Diagram.Coequalizer C
open import Categories.Diagram.Pullback op
open import Categories.Diagram.Pushout C
open import Categories.Diagram.Cone as Cone
open import Categories.Diagram.Cocone as Cocone
open import Categories.Diagram.End as End
open import Categories.Diagram.Coend as Coend
open import Categories.Diagram.Limit as Limit
open import Categories.Diagram.Colimit as Colimit
open import Categories.Category.Construction.Cocones using (Cocones)

private
  variable
    o′ ℓ′ e′ : Level
    D J : Category o′ ℓ′ e′
    A B : Obj
    f g : A ⇒ B

Coequalizer⇒coEqualizer : Coequalizer f g → Equalizer f g
Coequalizer⇒coEqualizer coe = record
  { arr       = arr
  ; equality  = equality
  ; equalize  = coequalize
  ; universal = universal
  ; unique    = unique
  }
  where open Coequalizer coe

coEqualizer⇒Coequalizer : Equalizer f g → Coequalizer f g
coEqualizer⇒Coequalizer e = record
  { arr        = arr
  ; equality   = equality
  ; coequalize = equalize
  ; universal  = universal
  ; unique     = unique
  }
  where open Equalizer e

coPullback⇒Pushout : Pullback f g → Pushout f g
coPullback⇒Pushout p = record
  { i₁              = p₁
  ; i₂              = p₂
  ; commute         = commute
  ; universal       = universal
  ; unique          = unique
  ; universal∘i₁≈h₁ = p₁∘universal≈h₁
  ; universal∘i₂≈h₂ = p₂∘universal≈h₂
  }
  where open Pullback p

Pushout⇒coPullback : Pushout f g → Pullback f g
Pushout⇒coPullback p = record
  { p₁              = i₁
  ; p₂              = i₂
  ; isPullback = record
    { commute         = commute
    ; universal       = universal
    ; unique          = unique
    ; p₁∘universal≈h₁ = universal∘i₁≈h₁
    ; p₂∘universal≈h₂ = universal∘i₂≈h₂
    }
  }
  where open Pushout p

module _ {F : Functor J C} where
  open Functor F renaming (op to Fop)

  coApex⇒Coapex : ∀ X → Apex Fop X → Coapex F X
  coApex⇒Coapex X apex = record
      { ψ       = ψ
      ; commute = commute
      }
    where open Cone.Apex apex

  coCone⇒Cocone : Cone Fop → Cocone F
  coCone⇒Cocone c = record
    { coapex = coApex⇒Coapex _ apex
    }
    where open Cone.Cone c

  Coapex⇒coApex : ∀ X → Coapex F X → Apex Fop X
  Coapex⇒coApex X coapex = record
      { ψ       = ψ
      ; commute = commute
      }
    where open Cocone.Coapex coapex

  Cocone⇒coCone : Cocone F → Cone Fop
  Cocone⇒coCone c = record
    { apex = Coapex⇒coApex _ coapex
    }
    where open Cocone.Cocone c

  coCone⇒⇒Cocone⇒ : ∀ {K K′} → Cone⇒ Fop K K′ → Cocone⇒ F (coCone⇒Cocone K′) (coCone⇒Cocone K)
  coCone⇒⇒Cocone⇒ f = record
    { arr     = arr
    ; commute = commute
    }
    where open Cone⇒ f

  Cocone⇒⇒coCone⇒ : ∀ {K K′} → Cocone⇒ F K K′ → Cone⇒ Fop (Cocone⇒coCone K′) (Cocone⇒coCone K)
  Cocone⇒⇒coCone⇒ f = record
    { arr     = arr
    ; commute = commute
    }
    where open Cocone⇒ f

  coLimit⇒Colimit : Limit Fop → Colimit F
  coLimit⇒Colimit lim = record
    { initial = op⊤⇒⊥ (Cocones F) $ record
      { ⊤             = coCone⇒Cocone ⊤
      ; ⊤-is-terminal = record
        { !        = coCone⇒⇒Cocone⇒ !
        ; !-unique = λ f → !-unique (Cocone⇒⇒coCone⇒ f)
        }
      }
    }
    where open Limit.Limit lim
          open Terminal terminal

  Colimit⇒coLimit : Colimit F → Limit Fop
  Colimit⇒coLimit colim = record
    { terminal = record
      { ⊤             = Cocone⇒coCone ⊥
      ; ⊤-is-terminal = record
        { !        = Cocone⇒⇒coCone⇒ !
        ; !-unique = λ f → !-unique (coCone⇒⇒Cocone⇒ f)
        }
      }
    }
    where open Colimit.Colimit colim
          open Initial initial

module _ {F : Bifunctor (Category.op D) D C} where
  open HomReasoning
  open Functor F renaming (op to Fop)

  coWedge⇒Cowedge : Wedge Fop → Cowedge F
  coWedge⇒Cowedge W = record
    { E         = E
    ; dinatural = DinaturalTransformation.op dinatural
    }
    where open Wedge W

  Cowedge⇒coWedge : Cowedge F → Wedge Fop
  Cowedge⇒coWedge W = record
    { E         = E
    ; dinatural = DinaturalTransformation.op dinatural
    }
    where open Cowedge W

  coEnd⇒Coend : End Fop → Coend F
  coEnd⇒Coend e = record
    { cowedge   = coWedge⇒Cowedge wedge
    ; factor    = λ W → factor (Cowedge⇒coWedge W)
    ; universal = universal
    ; unique    = unique
    }
    where open End.End e

  Coend⇒coEnd : Coend F → End Fop
  Coend⇒coEnd e = record
    { wedge     = Cowedge⇒coWedge cowedge
    ; factor    = λ W → factor (coWedge⇒Cowedge W)
    ; universal = universal
    ; unique    = unique
    }
    where open Coend.Coend e

module DiagramDualityConversionProperties where
  private
    Coequalizer⇔coEqualizer : ∀ (coequalizer : Coequalizer f g) →
      coEqualizer⇒Coequalizer (Coequalizer⇒coEqualizer coequalizer) ≡ coequalizer
    Coequalizer⇔coEqualizer _ = refl

    coPullback⇔Pushout : ∀ (coPullback : Pullback f g) →
      Pushout⇒coPullback (coPullback⇒Pushout coPullback) ≡ coPullback
    coPullback⇔Pushout _ = refl

    module _ {F : Functor J C} where
      open Functor F renaming (op to Fop)

      coApex⇔Coapex : ∀ X → (coApex : Apex Fop X) →
                        Coapex⇒coApex X (coApex⇒Coapex X coApex) ≡ coApex
      coApex⇔Coapex _ _ = refl

      coCone⇔Cocone : ∀ (coCone : Cone Fop) →
                        Cocone⇒coCone (coCone⇒Cocone coCone) ≡ coCone
      coCone⇔Cocone _ = refl

      coCone⇒⇔Cocone⇒ : ∀ {K K′} → (coCone⇒ : Cone⇒ Fop K K′) →
                        Cocone⇒⇒coCone⇒ (coCone⇒⇒Cocone⇒ coCone⇒) ≡ coCone⇒
      coCone⇒⇔Cocone⇒ _ = refl

      coLimit⇔Colimit : ∀ (coLimit : Limit Fop) →
                        Colimit⇒coLimit (coLimit⇒Colimit coLimit) ≡ coLimit
      coLimit⇔Colimit _ = refl

    module _ {F : Bifunctor (Category.op D) D C} where
      open Functor F renaming (op to Fop)

      coWedge⇔Cowedge : ∀ (coWedge : Wedge Fop) →
                        Cowedge⇒coWedge (coWedge⇒Cowedge coWedge) ≡ coWedge
      coWedge⇔Cowedge _ = refl

      coEnd⇔Coend : ∀ (coEnd : End Fop) →
                    Coend⇒coEnd (coEnd⇒Coend coEnd) ≡ coEnd
      coEnd⇔Coend _ = refl


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

module Data.Binary.Base where

open import Prelude
import Data.Nat as ℕ

infixr 5 1ᵇ∷_ 2ᵇ∷_
data 𝔹 : Type₀ where
  [] : 𝔹
  1ᵇ∷_ : 𝔹 → 𝔹
  2ᵇ∷_ : 𝔹 → 𝔹

inc : 𝔹 → 𝔹
inc [] = 1ᵇ∷ []
inc (1ᵇ∷ xs) = 2ᵇ∷ xs
inc (2ᵇ∷ xs) = 1ᵇ∷ inc xs

⟦_⇑⟧ : ℕ → 𝔹
⟦ zero  ⇑⟧ = []
⟦ suc n ⇑⟧ = inc ⟦ n ⇑⟧

⟦_⇓⟧ : 𝔹 → ℕ
⟦ [] ⇓⟧ = 0
⟦ 1ᵇ∷ xs ⇓⟧ = 1 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2
⟦ 2ᵇ∷ xs ⇓⟧ = 2 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2

add₁ : 𝔹 → 𝔹 → 𝔹
add₂ : 𝔹 → 𝔹 → 𝔹

add₁ [] ys = inc ys
add₁ xs [] = inc xs
add₁ (1ᵇ∷ xs) (1ᵇ∷ ys) = 1ᵇ∷ add₁ xs ys
add₁ (1ᵇ∷ xs) (2ᵇ∷ ys) = 2ᵇ∷ add₁ xs ys
add₁ (2ᵇ∷ xs) (1ᵇ∷ ys) = 2ᵇ∷ add₁ xs ys
add₁ (2ᵇ∷ xs) (2ᵇ∷ ys) = 1ᵇ∷ add₂ xs ys

add₂ [] [] = 2ᵇ∷ []
add₂ [] (1ᵇ∷ ys) = 1ᵇ∷ inc ys
add₂ [] (2ᵇ∷ ys) = 2ᵇ∷ inc ys
add₂ (1ᵇ∷ xs) [] = 1ᵇ∷ inc xs
add₂ (2ᵇ∷ xs) [] = 2ᵇ∷ inc xs
add₂ (1ᵇ∷ xs) (1ᵇ∷ ys) = 2ᵇ∷ add₁ xs ys
add₂ (1ᵇ∷ xs) (2ᵇ∷ ys) = 1ᵇ∷ add₂ xs ys
add₂ (2ᵇ∷ xs) (1ᵇ∷ ys) = 1ᵇ∷ add₂ xs ys
add₂ (2ᵇ∷ xs) (2ᵇ∷ ys) = 2ᵇ∷ add₂ xs ys

infixl 6 _+_
_+_ : 𝔹 → 𝔹 → 𝔹
[] + ys = ys
xs + [] = xs
(1ᵇ∷ xs) + (1ᵇ∷ ys) = 2ᵇ∷ xs + ys
(1ᵇ∷ xs) + (2ᵇ∷ ys) = 1ᵇ∷ add₁ xs ys
(2ᵇ∷ xs) + (1ᵇ∷ ys) = 1ᵇ∷ add₁ xs ys
(2ᵇ∷ xs) + (2ᵇ∷ ys) = 2ᵇ∷ add₁ xs ys

double : 𝔹 → 𝔹
double [] = []
double (1ᵇ∷ xs) = 2ᵇ∷ double xs
double (2ᵇ∷ xs) = 2ᵇ∷ 1ᵇ∷ xs

infixl 7 _*_
_*_ : 𝔹 → 𝔹 → 𝔹
xs * [] = []
xs * (1ᵇ∷ ys) = go xs
  where
  go : 𝔹 → 𝔹
  go [] = []
  go (1ᵇ∷ xs) = 1ᵇ∷ ys + go xs
  go (2ᵇ∷ xs) = 2ᵇ∷ double ys + go xs
xs * (2ᵇ∷ ys) = go xs
  where
  go : 𝔹 → 𝔹
  go [] = []
  go (1ᵇ∷ xs) = 2ᵇ∷ ys + go xs
  go (2ᵇ∷ xs) = 2ᵇ∷ (1ᵇ∷ ys) + go xs

dec′ : 𝔹 → 𝔹
dec : 𝔹 → 𝔹

dec′ [] = []
dec′ (1ᵇ∷ xs) = 2ᵇ∷ dec′ xs
dec′ (2ᵇ∷ xs) = 2ᵇ∷ 1ᵇ∷ xs

dec [] = []
dec (2ᵇ∷ xs) = 1ᵇ∷ xs
dec (1ᵇ∷ xs) = dec′ xs

sub₄ : (𝔹 → 𝔹) → (𝔹 → 𝔹) → 𝔹 → 𝔹 → 𝔹
sub₃ : (𝔹 → 𝔹) → (𝔹 → 𝔹) → 𝔹 → 𝔹 → 𝔹

sub₄ o k []           ys       = []
sub₄ o k (1ᵇ∷ xs)     (1ᵇ∷ ys) = sub₄ (o ∘ k) 2ᵇ∷_ xs ys
sub₄ o k (2ᵇ∷ xs)     (2ᵇ∷ ys) = sub₄ (o ∘ k) 2ᵇ∷_ xs ys
sub₄ o k (1ᵇ∷ xs)     (2ᵇ∷ ys) = sub₄ o (k ∘ 1ᵇ∷_) xs ys
sub₄ o k (2ᵇ∷ xs)     (1ᵇ∷ ys) = sub₃ o (k ∘ 1ᵇ∷_) xs ys
sub₄ o k (1ᵇ∷ [])     []       = o []
sub₄ o k (1ᵇ∷ 1ᵇ∷ xs) []       = o (k (1ᵇ∷ (dec′ xs)))
sub₄ o k (1ᵇ∷ 2ᵇ∷ xs) []       = o (k (1ᵇ∷ (1ᵇ∷ xs)))
sub₄ o k (2ᵇ∷ xs)     []       = o (k (dec′ xs))

sub₃ o k []       []       = o []
sub₃ o k []       (1ᵇ∷ ys) = []
sub₃ o k []       (2ᵇ∷ ys) = []
sub₃ o k (1ᵇ∷ xs) []       = o (k (dec′ xs))
sub₃ o k (2ᵇ∷ xs) []       = o (k (1ᵇ∷ xs))
sub₃ o k (1ᵇ∷ xs) (1ᵇ∷ ys) = sub₃ o (k ∘ 1ᵇ∷_) xs ys
sub₃ o k (2ᵇ∷ xs) (2ᵇ∷ ys) = sub₃ o (k ∘ 1ᵇ∷_) xs ys
sub₃ o k (1ᵇ∷ xs) (2ᵇ∷ ys) = sub₄ (o ∘ k) 2ᵇ∷_ xs ys
sub₃ o k (2ᵇ∷ xs) (1ᵇ∷ ys) = sub₃ (o ∘ k) 2ᵇ∷_ xs ys

sub₂ : (𝔹 → 𝔹) → 𝔹 → 𝔹 → 𝔹
sub₂ k []       ys       = []
sub₂ k (1ᵇ∷ xs) []       = k (dec′ xs)
sub₂ k (2ᵇ∷ xs) []       = k (1ᵇ∷ xs)
sub₂ k (1ᵇ∷ xs) (1ᵇ∷ ys) = sub₂ (1ᵇ∷_ ∘ k) xs ys
sub₂ k (2ᵇ∷ xs) (2ᵇ∷ ys) = sub₂ (1ᵇ∷_ ∘ k) xs ys
sub₂ k (1ᵇ∷ xs) (2ᵇ∷ ys) = sub₄ k 2ᵇ∷_ xs ys
sub₂ k (2ᵇ∷ xs) (1ᵇ∷ ys) = sub₃ k 2ᵇ∷_ xs ys

sub₁ : (𝔹 → 𝔹) → 𝔹 → 𝔹 → 𝔹
sub₁ k  xs      []       = k xs
sub₁ k []       (1ᵇ∷ ys) = []
sub₁ k []       (2ᵇ∷ ys) = []
sub₁ k (1ᵇ∷ xs) (1ᵇ∷ ys) = sub₃ k 2ᵇ∷_ xs ys
sub₁ k (2ᵇ∷ xs) (2ᵇ∷ ys) = sub₃ k 2ᵇ∷_ xs ys
sub₁ k (2ᵇ∷ xs) (1ᵇ∷ ys) = sub₁ (1ᵇ∷_ ∘ k) xs ys
sub₁ k (1ᵇ∷ xs) (2ᵇ∷ ys) = sub₂ (1ᵇ∷_ ∘ k) xs ys

infixl 6 _-_
_-_ : 𝔹 → 𝔹 → 𝔹
_-_ = sub₁ id

_≡ᵇ_ : 𝔹 → 𝔹 → Bool
[] ≡ᵇ [] = true
[] ≡ᵇ (1ᵇ∷ ys) = false
[] ≡ᵇ (2ᵇ∷ ys) = false
(1ᵇ∷ xs) ≡ᵇ [] = false
(1ᵇ∷ xs) ≡ᵇ (1ᵇ∷ ys) = xs ≡ᵇ ys
(1ᵇ∷ xs) ≡ᵇ (2ᵇ∷ ys) = false
(2ᵇ∷ xs) ≡ᵇ [] = false
(2ᵇ∷ xs) ≡ᵇ (1ᵇ∷ ys) = false
(2ᵇ∷ xs) ≡ᵇ (2ᵇ∷ ys) = xs ≡ᵇ ys

-- testers : ℕ → Type₀
-- testers n = bins n n ≡ nats n n
--   where
--   open import Data.List
--   open import Data.List.Syntax
--   open import Data.List.Sugar
--   import Agda.Builtin.Nat as Nat

--   upTo : (ℕ → A) → ℕ → List A
--   upTo f zero = []
--   upTo f (suc n) = f zero List.∷ upTo (f ∘ suc) n

--   bins : ℕ → ℕ → List 𝔹
--   bins ns ms = do
--     n ← upTo id ns
--     m ← upTo id ms
--     pure (⟦ n ⇑⟧ - ⟦ m ⇑⟧)

--   nats : ℕ → ℕ → List 𝔹
--   nats ns ms = do
--     n ← upTo id ns
--     m ← upTo id ms
--     pure ⟦ n Nat.- m ⇑⟧

-- _ : testers 100
-- _ = refl

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- 2011-11-24 Andreas, James
{-# OPTIONS --copatterns #-}
module CopatternWithoutFieldName where

record R : Set2 where
  field
    f : Set1
open R

test : (f : R -> Set1) -> R
test f = bla where
  bla : R
  f bla = Set
-- not a copattern, since f not a field name


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Rose trees
------------------------------------------------------------------------

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

module Data.Tree.Rose where

open import Level using (Level)
open import Size
open import Data.List.Base as List using (List; []; _∷_)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
import Data.Nat.Properties as ℕₚ
open import Data.List.Extrema.Nat
open import Function.Base using (_∘_)

private
  variable
    a b : Level
    A : Set a
    B : Set b
    i : Size

------------------------------------------------------------------------
-- Type and basic constructions

data Rose (A : Set a) : Size → Set a where
  node : (a : A) (ts : List (Rose A i)) → Rose A (↑ i)

leaf : A → Rose A ∞
leaf a = node a []

------------------------------------------------------------------------
-- Transforming rose trees

map : (A → B) → Rose A i → Rose B i
map f (node a ts) = node (f a) (List.map (map f) ts)

------------------------------------------------------------------------
-- Reducing rose trees

foldr : (A → List B → B) → Rose A i → B
foldr n (node a ts) = n a (List.map (foldr n) ts)

depth : Rose A i → ℕ
depth (node a ts) = suc (max 0 (List.map depth ts))


text:
postulate
  A   : Set
  x   : A
  f   : A → A → A
  _●_ : A → A → A

infix 20 _●_

syntax f x y = x ○ y

doesn't-parse : A
doesn't-parse = x ○ x ● x

-- Default fixity for syntax is no longer -666, but 20 as for normal operators.


text:
data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Zero : Nat → Set where
  instance
    isZero : Zero zero

data NonZero : Nat → Set where
  instance
    isSuc : ∀ {n : Nat} → NonZero (suc n)

pred : ∀ t {{_ : NonZero t}} → Nat
pred ._ {{isSuc {n}}} = n

test : Nat
test = pred (suc zero)

data Test (x : Nat) : Set where
  here  : {{_ : Zero x}} → Test x
  there : {{nz : NonZero x}} → Test (pred x) → Test x

broken : Test (suc zero)
broken = there here


text:
{-

Defines groups and adds some smart constructors

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Data.Sigma
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Semigroup

private
  variable
    ℓ : Level

record IsGroup {G : Type ℓ}
               (1g : G) (_·_ : G → G → G) (inv : G → G) : Type ℓ where

  constructor isgroup

  field
    isMonoid  : IsMonoid 1g _·_
    inverse   : (x : G) → (x · inv x ≡ 1g) × (inv x · x ≡ 1g)

  open IsMonoid isMonoid public

  infixl 6 _-_

  -- Useful notation for additive groups
  _-_ : G → G → G
  x - y = x · inv y

  invl : (x : G) → inv x · x ≡ 1g
  invl x = inverse x .snd

  invr : (x : G) → x · inv x ≡ 1g
  invr x = inverse x .fst

record GroupStr (G : Type ℓ) : Type ℓ where

  constructor groupstr

  field
    1g      : G
    _·_     : G → G → G
    inv     : G → G
    isGroup : IsGroup 1g _·_ inv

  infixr 7 _·_

  open IsGroup isGroup public

Group : ∀ ℓ → Type (ℓ-suc ℓ)
Group ℓ = TypeWithStr ℓ GroupStr

Group₀ : Type₁
Group₀ = Group ℓ-zero

group : (G : Type ℓ) (1g : G) (_·_ : G → G → G) (inv : G → G) (h : IsGroup 1g _·_ inv) → Group ℓ
group G 1g _·_ inv h = G , groupstr 1g _·_ inv h

isSetGroup : (G : Group ℓ) → isSet ⟨ G ⟩
isSetGroup G = GroupStr.isGroup (snd G) .IsGroup.isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

makeIsGroup : {G : Type ℓ} {e : G} {_·_ : G → G → G} { inv : G → G}
              (is-setG : isSet G)
              (assoc : (x y z : G) → x · (y · z) ≡ (x · y) · z)
              (rid : (x : G) → x · e ≡ x)
              (lid : (x : G) → e · x ≡ x)
              (rinv : (x : G) → x · inv x ≡ e)
              (linv : (x : G) → inv x · x ≡ e)
            → IsGroup e _·_ inv
IsGroup.isMonoid (makeIsGroup is-setG assoc rid lid rinv linv) = makeIsMonoid is-setG assoc rid lid
IsGroup.inverse (makeIsGroup is-setG assoc rid lid rinv linv) = λ x → rinv x , linv x

makeGroup : {G : Type ℓ} (e : G) (_·_ : G → G → G) (inv : G → G)
            (is-setG : isSet G)
            (assoc : (x y z : G) → x · (y · z) ≡ (x · y) · z)
            (rid : (x : G) → x · e ≡ x)
            (lid : (x : G) → e · x ≡ x)
            (rinv : (x : G) → x · inv x ≡ e)
            (linv : (x : G) → inv x · x ≡ e)
          → Group ℓ
makeGroup e _·_ inv is-setG assoc rid lid rinv linv = _ , helper
  where
  helper : GroupStr _
  GroupStr.1g helper = e
  GroupStr._·_ helper = _·_
  GroupStr.inv helper = inv
  GroupStr.isGroup helper = makeIsGroup is-setG assoc rid lid rinv linv

makeGroup-right : {A : Type ℓ}
  → (1g : A)
  → (_·_ : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (assoc : ∀ a b c → a · (b · c) ≡ (a · b) · c)
  → (rUnit : ∀ a → a · 1g ≡ a)
  → (rCancel : ∀ a → a · inv a ≡ 1g)
  → Group ℓ
makeGroup-right 1g _·_ inv set assoc rUnit rCancel =
  makeGroup 1g _·_ inv set assoc rUnit lUnit rCancel lCancel
  where
    abstract
      lCancel : ∀ a → inv a · a ≡ 1g
      lCancel a =
        inv a · a
          ≡⟨ sym (rUnit _)  ⟩
        (inv a · a) · 1g
          ≡⟨ cong (_·_ _) (sym (rCancel (inv a))) ⟩
        (inv a · a) · (inv a · (inv (inv a)))
          ≡⟨ assoc _ _ _ ⟩
        ((inv a · a) · (inv a)) · (inv (inv a))
          ≡⟨ cong (λ □ → □ · _) (sym (assoc _ _ _)) ⟩
        (inv a · (a · inv a)) · (inv (inv a))
          ≡⟨ cong (λ □ → (inv a · □) · (inv (inv a))) (rCancel a) ⟩
        (inv a · 1g) · (inv (inv a))
          ≡⟨ cong (λ □ → □ · (inv (inv a))) (rUnit (inv a)) ⟩
        inv a · (inv (inv a))
          ≡⟨ rCancel (inv a) ⟩
        1g
          ∎

      lUnit : ∀ a → 1g · a ≡ a
      lUnit a =
        1g · a
          ≡⟨ cong (λ b → b · a) (sym (rCancel a)) ⟩
        (a · inv a) · a
          ≡⟨ sym (assoc _ _ _) ⟩
        a · (inv a · a)
          ≡⟨ cong (a ·_) (lCancel a) ⟩
        a · 1g
          ≡⟨ rUnit a ⟩
        a
          ∎

makeGroup-left : {A : Type ℓ}
  → (1g : A)
  → (_·_ : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (assoc : ∀ a b c → a · (b · c) ≡ (a · b) · c)
  → (lUnit : ∀ a → 1g · a ≡ a)
  → (lCancel : ∀ a → (inv a) · a ≡ 1g)
  → Group ℓ
makeGroup-left 1g _·_ inv set assoc lUnit lCancel =
  makeGroup 1g _·_ inv set assoc rUnit lUnit rCancel lCancel
  where
    abstract
      rCancel : ∀ a → a · inv a ≡ 1g
      rCancel a =
        a · inv a
          ≡⟨ sym (lUnit _)  ⟩
        1g · (a · inv a)
          ≡⟨ cong (λ b → b · (a · inv a)) (sym (lCancel (inv a))) ⟩
        (inv (inv a) · inv a) · (a · inv a)
          ≡⟨ sym (assoc (inv (inv a)) (inv a) _) ⟩
        inv (inv a) · (inv a · (a · inv a))
          ≡⟨ cong (inv (inv a) ·_) (assoc (inv a) a (inv a)) ⟩
        (inv (inv a)) · ((inv a · a) · (inv a))
          ≡⟨ cong (λ b → (inv (inv a)) · (b · (inv a))) (lCancel a) ⟩
        inv (inv a) · (1g · inv a)
          ≡⟨ cong (inv (inv a) ·_) (lUnit (inv a)) ⟩
        inv (inv a) · inv a
          ≡⟨ lCancel (inv a) ⟩
        1g
          ∎

      rUnit : ∀ a → a · 1g ≡ a
      rUnit a =
        a · 1g
          ≡⟨ cong (a ·_) (sym (lCancel a)) ⟩
        a · (inv a · a)
          ≡⟨ assoc a (inv a) a ⟩
        (a · inv a) · a
          ≡⟨ cong (λ b → b · a) (rCancel a) ⟩
        1g · a
          ≡⟨ lUnit a ⟩
        a
          ∎

max_stars_repo_name: jespercockx/cubical

max_issues_repo_name: jespercockx/cubical

max_forks_repo_name: jespercockx/cubical


text:
----------------------------------------------------------------
-- This file contains the definition natural transformations. --
----------------------------------------------------------------
module Category.NatTrans where

open import Level

open import Category.Category public
open import Category.Funct public
open import Category.CatEq public

record NatTrans {l₁ l₂ : Level}
                {ℂ₁ : Cat {l₁}}
                {ℂ₂ : Cat {l₂}}
                (F G : Functor ℂ₁ ℂ₂) : Set (l₁ ⊔ l₂) where
  field
    -- The family of components.
    η : (A : Obj ℂ₁) → el (Hom ℂ₂ (omap F A) (omap G A))

    -- The natural transformation law.
    η-ax : ∀{A B}{f : el (Hom ℂ₁ A B)} → comm-square {ℂ = ℂ₂} (appT (fmap F) f) (η B) (η A) (appT (fmap G) f)

open NatTrans public

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Data.Bool as Bool using (Bool; false; true; if_then_else_; not)
open import Data.String using (String)
open import Data.Nat using (ℕ; _+_; _≟_; suc; _>_; _<_; _∸_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.List as l using (List; filter; map; take; foldl; length; []; _∷_)
open import Data.List.Properties
-- open import Data.List.Extrema using (max)
open import Data.Maybe using (to-witness)
open import Data.Fin using (fromℕ; _-_; zero; Fin)
open import Data.Fin.Properties using (≤-totalOrder)
open import Data.Product as Prod using (∃; ∃₂; _×_; _,_; Σ)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning
open import Level using (Level)
open import Data.Vec as v using (Vec; fromList; toList; last; length; []; _∷_; [_]; _∷ʳ_; _++_; lookup; head; initLast; filter; map)
open import Data.Vec.Bounded as vb using ([]; _∷_; fromVec; filter; Vec≤)
open import Agda.Builtin.Nat public
  using () renaming (_==_ to _≡ᵇ_)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; _≗_; cong₂; inspect; [_])
open import Data.Nat.Properties using (+-comm)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (does)
open import Data.Vec.Bounded.Base using (padRight; ≤-cast)
import Data.Nat.Properties as ℕₚ
open import Relation.Nullary.Decidable.Core using (dec-false)
open import Function using (_∘_)
open import Data.List.Extrema ℕₚ.≤-totalOrder
open import Data.Empty using (⊥)

-- TODO add to std-lib
open import Relation.Nullary

dec-¬ : ∀ {a} {P : Set a} → Dec P → Dec (¬ P)
dec-¬ (yes p) = no λ prf → prf p
dec-¬ (no ¬p) = yes ¬p

-- TODO switch to Vec init?
allButLast : ∀ {a} {A : Set a} → List A → List A
allButLast []           = l.[]
allButLast (_ ∷ [])     = l.[]
allButLast (x ∷ x₁ ∷ l) = x l.∷ (allButLast (x₁ l.∷ l))

allButLast-∷ʳ : ∀ {a} {A : Set a} {l : List A} {x} → allButLast (l l.∷ʳ x) ≡ l
allButLast-∷ʳ {l = []}         = refl
allButLast-∷ʳ {l = _ ∷ []}     = refl
allButLast-∷ʳ {l = x ∷ x₁ ∷ l} = cong (x l.∷_) (allButLast-∷ʳ {l = x₁ l.∷ l})

filter' : {A : Set} → (A → Bool) → List A → List A
filter' p []               = l.[]
filter' p (x ∷ xs) with (p x)
...                | true  = x l.∷ filter' p xs
...                | false = filter' p xs

record Todo : Set where
  field
    text      : String
    completed : Bool
    id        : ℕ

-- can't define this for (List any) since (last []) must be defined for each carrier type
TodoListLast : List Todo → Todo
TodoListLast []          = record {}
TodoListLast (x ∷ [])    = x
TodoListLast (_ ∷ y ∷ l) = TodoListLast (y l.∷ l)

AddTodo : List Todo → String → List Todo
AddTodo todos text =
  todos l.∷ʳ
  record
    { id        = 1
    ; completed = false
    ; text      = text
    }

-- AddTodo is well-defined
AddTodoAddsNewListItem :
  (todos : List Todo) (text : String) →
    l.length (AddTodo todos text) ≡ l.length todos + 1
AddTodoAddsNewListItem todos text = length-++ todos

AddTodoSetsNewCompletedToFalse :
  (todos : List Todo) (text : String) →
    Todo.completed (TodoListLast (AddTodo todos text)) ≡ false
AddTodoSetsNewCompletedToFalse []          text = refl
AddTodoSetsNewCompletedToFalse (_ ∷ [])    text = refl
AddTodoSetsNewCompletedToFalse (_ ∷ _ ∷ l) text = AddTodoSetsNewCompletedToFalse (_ l.∷ l) text

-- TODO can't prove this until AddTodo definition changed
AddTodoSetsNewIdToNonExistingId :
  (todos : List Todo) (text : String) →
    l.length (l.filter (λ todo → dec-¬ (Todo.id todo ≟ Todo.id (TodoListLast (AddTodo todos text)))) (AddTodo todos text)) ≡ 1
AddTodoSetsNewIdToNonExistingId todos text = {!   !}

AddTodoSetsNewTextToText :
  (todos : List Todo) (text : String) →
    Todo.text (TodoListLast (AddTodo todos text)) ≡ text
AddTodoSetsNewTextToText []          text = refl
AddTodoSetsNewTextToText (_ ∷ [])    text = refl
AddTodoSetsNewTextToText (_ ∷ _ ∷ l) text = AddTodoSetsNewTextToText (_ l.∷ l) text

AddTodoDoesntChangeOtherTodos :
  (todos : List Todo) (text : String) →
    l.length todos > 0 →
      allButLast (AddTodo todos text) ≡ todos
AddTodoDoesntChangeOtherTodos (x l.∷ xs) text _<_ = allButLast-∷ʳ
-- END AddTodo is well-defined

-- TODO text1 ≠ text2
AddTodo-not-comm :
  (todos : List Todo) →
    (text1 : String) →
      (text2 : String) →
  (AddTodo (AddTodo todos text1) text2 ≢ AddTodo (AddTodo todos text2) text1)
AddTodo-not-comm todos text1 text2 = {!   !}

-- {-# COMPILE JS AddTodo =
--   function (todos) {
--     return function (text) {
--       return [
--         ...todos,
--         {
--           id: todos.reduce((maxId, todo) => Math.max(todo.id, maxId), -1) + 1,
--           completed: false,
--           text: text
--         }
--       ]
--     }
--   }
-- #-}

DeleteTodo : (List Todo) → ℕ → (List Todo)
DeleteTodo todos id = l.filter (λ todo → dec-¬ (Todo.id todo ≟ id)) todos

DeleteTodo' : (List Todo) → ℕ → (List Todo)
DeleteTodo' todos id = filter' (λ todo → not (Todo.id todo ≡ᵇ id)) todos

DeleteTodo'RemoveTodoWithId :
  (todos : List Todo) (id : ℕ) →
    filter' (λ todo → Todo.id todo ≡ᵇ id) (DeleteTodo' todos id) ≡ l.[]
DeleteTodo'RemoveTodoWithId []       id = refl
DeleteTodo'RemoveTodoWithId (x ∷ xs) id with (Todo.id x ≡ᵇ id) | inspect (_≡ᵇ id) (Todo.id x)
... | true  | P.[ eq ]                  = DeleteTodo'RemoveTodoWithId xs id
... | false | P.[ eq ] rewrite eq       = DeleteTodo'RemoveTodoWithId xs id

-- TODO this one needs Todo to specify that it can only have one unique id
DeleteTodo'Removes1Element :
  (todos : List Todo) (id : ℕ) →
    l.length (DeleteTodo' todos id) ≡ l.length todos ∸ 1
DeleteTodo'Removes1Element []       id = refl
DeleteTodo'Removes1Element (x ∷ xs) id with (Todo.id x ≡ᵇ id) | inspect (_≡ᵇ id) (Todo.id x)
... | true  | P.[ eq ] rewrite eq = {!   !} -- DeleteTodo'Removes1Element xs id
... | false | P.[ eq ] rewrite eq = {!   !}

DeleteTodoDoesntChangeOtherTodos :
  (todos : List Todo) (id : ℕ) →
    DeleteTodo todos id ≡ l.filter (λ todo → dec-¬ (Todo.id todo ≟ id)) todos
DeleteTodoDoesntChangeOtherTodos todos id = refl
-- END DeleteTodo is well-defined

DeleteTodo-idem :
  (todos : List Todo) (id : ℕ) →
    DeleteTodo (DeleteTodo todos id) id ≡ DeleteTodo todos id
DeleteTodo-idem todos id = filter-idem (λ e → dec-¬ (Todo.id e ≟ id)) todos

-- {-# COMPILE JS DeleteTodo =
--   function (todos) {
--     return function (id) {
--       return todos.filter(function (todo) {
--         return todo.id !== id
--       });
--     }
--   }
-- #-}

-- EditTodo: can't use updateAt since id doesn't necessarily correspond to Vec index
EditTodo : (List Todo) → ℕ → String → (List Todo)
EditTodo todos id text =
  l.map (λ todo →
    if (⌊ Todo.id todo ≟ id ⌋)
    then record todo { text = text }
    else todo)
    todos

EditTodo' : (List Todo) → ℕ → String → (List Todo)
EditTodo' todos id text =
  l.map (λ todo →
    if (Todo.id todo ≡ᵇ id)
    then record todo { text = text }
    else todo)
    todos

-- EditTodo is well-defined
-- EditTodoChangesText :
--   (todos : List Todo) (id : ℕ) (text : String) →
--     l.map Todo.text (l.filter (λ todo → Todo.id todo ≟ id) (EditTodo todos id text)) ≡ l.[ text ]
-- EditTodoChangesText todos id text = {!   !}

-- -- TODO not necessarily true
-- EditTodo'ChangesText :
--   (todos : List Todo) (id : ℕ) (text : String) →
--     l.map Todo.text (EditTodo' (filter' (λ todo → Todo.id todo ≡ᵇ id) todos) id text) ≡ l.map Todo.text (filter' (λ todo → Todo.id todo ≡ᵇ id) todos)
-- EditTodo'ChangesText []       id text = refl
-- EditTodo'ChangesText (x ∷ xs) id text with (Todo.id x ≡ᵇ id) | inspect (_≡ᵇ id) (Todo.id x)
-- ... | true  | P.[ eq ] rewrite eq = {!   !} -- cong (Todo.text x l.∷_) (EditTodo'ChangesText xs id text)
-- ... | false | P.[ eq ] rewrite eq = EditTodo'ChangesText xs id text

EditTodo'DoesntChangeId :
  (todos : List Todo) (id : ℕ) (text : String) →
    l.map Todo.id (EditTodo' todos id text) ≡ l.map Todo.id todos
EditTodo'DoesntChangeId []       id text = refl
EditTodo'DoesntChangeId (x ∷ xs) id text with (Todo.id x ≡ᵇ id)
... | true  = cong ((Todo.id x) l.∷_) (EditTodo'DoesntChangeId xs id text)
... | false = cong ((Todo.id x) l.∷_) (EditTodo'DoesntChangeId xs id text)

EditTodo'DoesntChangeCompleted :
  (todos : List Todo) (id : ℕ) (text : String) →
    l.map Todo.completed (EditTodo' todos id text) ≡ l.map Todo.completed todos
EditTodo'DoesntChangeCompleted []       id text = refl
EditTodo'DoesntChangeCompleted (x ∷ xs) id text with (Todo.id x ≡ᵇ id)
... | true  = cong ((Todo.completed x) l.∷_) (EditTodo'DoesntChangeCompleted xs id text)
... | false = cong ((Todo.completed x) l.∷_) (EditTodo'DoesntChangeCompleted xs id text)

EditTodo'DoesntChangeOtherTodos :
  (todos : List Todo) (id : ℕ) (text : String) →
    filter' (λ todo → not (Todo.id todo ≡ᵇ id)) (EditTodo' todos id text) ≡ filter' (λ todo → not (Todo.id todo ≡ᵇ id)) todos
EditTodo'DoesntChangeOtherTodos []       id text = refl
EditTodo'DoesntChangeOtherTodos (x ∷ xs) id text with (Todo.id x ≡ᵇ id) | inspect (_≡ᵇ id) (Todo.id x)
... | true  | P.[ eq ] rewrite eq = EditTodo'DoesntChangeOtherTodos xs id text
... | false | P.[ eq ] rewrite eq = cong (x l.∷_) (EditTodo'DoesntChangeOtherTodos xs id text)

EditTodoLengthUnchanged :
  (todos : List Todo) (id' : ℕ) (text : String) →
    l.length (EditTodo todos id' text) ≡ l.length todos
EditTodoLengthUnchanged todos id' text = length-map (λ todo → if (⌊ Todo.id todo ≟ id' ⌋) then record todo { text = text } else todo) todos
-- END EditTodo is well-defined

EditTodo'-idem :
  (todos : List Todo) (id : ℕ) (text : String) →
    EditTodo' (EditTodo' todos id text) id text ≡ EditTodo' todos id text
EditTodo'-idem []       id text = refl
EditTodo'-idem (x ∷ xs) id text with (Todo.id x ≡ᵇ id) | inspect (_≡ᵇ id) (Todo.id x)
... | true  | P.[ eq ] rewrite eq = cong (record x { text = text } List.∷_) (EditTodo'-idem xs id text)
... | false | P.[ eq ] rewrite eq = cong (x List.∷_) (EditTodo'-idem xs id text)

-- {-# COMPILE JS EditTodo =
--   function (todos) {
--     return function (id) {
--       return function (text) {
--         return todos.map(function (todo) {
--           if (todo.id === id) {
--             todo.text = text;
--           }

--           return todo;
--         });
--       }
--     }
--   }
-- #-}

CompleteTodo : (List Todo) → ℕ → (List Todo)
CompleteTodo todos id =
  l.map (λ todo →
    if (⌊ Todo.id todo ≟ id ⌋)
    then record todo { completed = true }
    else todo)
    todos

CompleteTodo' : (List Todo) → ℕ → (List Todo)
CompleteTodo' todos id =
  l.map (λ todo →
    if (Todo.id todo ≡ᵇ id)
    then record todo { completed = true }
    else todo)
    todos

-- CompleteTodo is well-defined
-- TODO don't know if there is only one instance of Todo with that id
CompleteTodo'ChangesCompleted :
  (todos : List Todo) (id : ℕ) →
    l.map Todo.completed (filter' (λ todo → Todo.id todo ≡ᵇ id) (CompleteTodo' todos id)) ≡ l.map (λ todo → true) (filter' (λ todo → Todo.id todo ≡ᵇ id) todos)
CompleteTodo'ChangesCompleted []       id = refl
CompleteTodo'ChangesCompleted (x ∷ xs) id with Todo.id x ≡ᵇ id | inspect (_≡ᵇ id) (Todo.id x)
... | true  | P.[ eq ] rewrite eq = cong (true l.∷_) (CompleteTodo'ChangesCompleted xs id)
... | false | P.[ eq ] rewrite eq = CompleteTodo'ChangesCompleted xs id

CompleteTodoDoesntChangeIds :
  (todos : List Todo) (id : ℕ) →
    l.map Todo.id (CompleteTodo todos id) ≡ l.map Todo.id todos
CompleteTodoDoesntChangeIds []       id = refl
CompleteTodoDoesntChangeIds (x ∷ []) id = cong (l._∷ l.[]) (helper x id)
  where
    helper :
      (x : Todo) (id : ℕ) →
        Todo.id (if ⌊ Todo.id x ≟ id ⌋ then record { text = Todo.text x ; completed = true ; id = Todo.id x } else x) ≡ Todo.id x
    helper x id with (⌊ Todo.id x ≟ id ⌋)
    ...         | true  = refl
    ...         | false = refl
CompleteTodoDoesntChangeIds (x ∷ xs) id =
  begin
    l.map Todo.id (CompleteTodo (x l.∷ xs) id)
  ≡⟨⟩
    (l.map Todo.id (CompleteTodo l.[ x ] id)) l.++ l.map Todo.id (CompleteTodo xs id)
  ≡⟨ cong (l._++ l.map Todo.id (CompleteTodo xs id)) (CompleteTodoDoesntChangeIds (x l.∷ l.[]) id) ⟩
    l.map Todo.id (l.[ x ]) l.++ l.map Todo.id (CompleteTodo xs id)
  ≡⟨⟩
    l.[ Todo.id x ] l.++ l.map Todo.id (CompleteTodo xs id)
  ≡⟨⟩
    Todo.id x l.∷ l.map Todo.id (CompleteTodo xs id)
  ≡⟨ cong (Todo.id x l.∷_) (CompleteTodoDoesntChangeIds xs id) ⟩
    Todo.id x l.∷ l.map Todo.id xs
  ≡⟨⟩
    l.map Todo.id (x l.∷ xs)
  ∎

CompleteTodoDoesntChangeText :
  (todos : List Todo) (id : ℕ) →
    l.map Todo.text (CompleteTodo todos id) ≡ l.map Todo.text todos
CompleteTodoDoesntChangeText []       id = refl
CompleteTodoDoesntChangeText (x ∷ []) id = cong (l._∷ l.[]) (helper x id)
  where
    helper :
      (x : Todo) (id : ℕ) →
        Todo.text (if ⌊ Todo.id x ≟ id ⌋ then record { text = Todo.text x ; completed = true ; id = Todo.id x } else x) ≡ Todo.text x
    helper x id with (⌊ Todo.id x ≟ id ⌋)
    ...         | true  = refl
    ...         | false = refl
CompleteTodoDoesntChangeText (x ∷ xs) id =
  begin
    l.map Todo.text (CompleteTodo (x l.∷ xs) id)
  ≡⟨⟩
    (l.map Todo.text (CompleteTodo l.[ x ] id)) l.++ l.map Todo.text (CompleteTodo xs id)
  ≡⟨ cong (l._++ l.map Todo.text (CompleteTodo xs id)) (CompleteTodoDoesntChangeText (x l.∷ l.[]) id) ⟩
    l.map Todo.text (l.[ x ]) l.++ l.map Todo.text (CompleteTodo xs id)
  ≡⟨⟩
    l.[ Todo.text x ] l.++ l.map Todo.text (CompleteTodo xs id)
  ≡⟨⟩
    Todo.text x l.∷ l.map Todo.text (CompleteTodo xs id)
  ≡⟨ cong (Todo.text x l.∷_) (CompleteTodoDoesntChangeText xs id) ⟩
    Todo.text x l.∷ l.map Todo.text xs
  ≡⟨⟩
    l.map Todo.text (x l.∷ xs)
  ∎

CompleteTodo'DoesntChangeOthersCompleted :
  (todos : List Todo) (id : ℕ) →
    l.map Todo.completed (CompleteTodo' (filter' (λ todo → not (Todo.id todo ≡ᵇ id)) todos) id) ≡ l.map Todo.completed (filter' (λ todo → not (Todo.id todo ≡ᵇ id)) todos)
CompleteTodo'DoesntChangeOthersCompleted []       id = refl
CompleteTodo'DoesntChangeOthersCompleted (x ∷ xs) id with Todo.id x ≡ᵇ id | inspect (_≡ᵇ id) (Todo.id x)
... | true  | P.[ eq ] rewrite eq = CompleteTodo'DoesntChangeOthersCompleted xs id --
... | false | P.[ eq ] rewrite eq = cong (Todo.completed x l.∷_) (CompleteTodo'DoesntChangeOthersCompleted xs id)

CompleteTodoLengthUnchanged :
  (todos : List Todo) (id : ℕ) →
    l.length (CompleteTodo todos id) ≡ l.length todos
CompleteTodoLengthUnchanged todos id = length-map (λ todo → if (⌊ Todo.id todo ≟ id ⌋) then record todo { completed = true } else todo) todos
-- END CompleteTodo is well-defined

CompleteTodo'-idem :
  (todos : List Todo) (id : ℕ) →
    CompleteTodo' (CompleteTodo' todos id) id ≡ CompleteTodo' todos id
CompleteTodo'-idem []       id = refl
CompleteTodo'-idem (x ∷ xs) id with Todo.id x ≡ᵇ id | inspect (_≡ᵇ id) (Todo.id x)
... | true  | P.[ eq ] rewrite eq = cong (record x { completed = true } l.∷_) (CompleteTodo'-idem xs id)
... | false | P.[ eq ] rewrite eq = cong (x l.∷_) (CompleteTodo'-idem xs id)

-- {-# COMPILE JS CompleteTodo =
--   function (todos) {
--     return function (id) {
--       return todos.map(function (todo) {
--         if (todo.id === id) {
--           todo.completed = true;
--         }

--         return todo;
--       });
--     }
--   }
-- #-}

CompleteAllTodos : List Todo → List Todo
CompleteAllTodos todos =
  l.map (λ todo →
    record todo { completed = true })
    todos

-- CompleteAllTodos is well-defined
CompleteAllTodosAllCompleted :
  (todos : List Todo) →
    l.filter (λ todo → (Todo.completed todo) Bool.≟ false) (CompleteAllTodos todos) ≡ l.[]
CompleteAllTodosAllCompleted []       = refl
CompleteAllTodosAllCompleted (x ∷ xs) = CompleteAllTodosAllCompleted xs

CompleteAllTodosDoesntChangeIds :
  (todos : List Todo) →
    l.map Todo.id (CompleteAllTodos todos) ≡ l.map Todo.id todos
CompleteAllTodosDoesntChangeIds []       = refl
CompleteAllTodosDoesntChangeIds (x ∷ []) = cong (l._∷ l.[]) (helper x)
  where
    helper :
      (x : Todo) →
        Todo.id (record x { completed = true }) ≡ Todo.id x
    helper x = refl
CompleteAllTodosDoesntChangeIds (x ∷ xs) =
  begin
    l.map Todo.id (CompleteAllTodos (x l.∷ xs))
  ≡⟨⟩
    (l.map Todo.id (CompleteAllTodos l.[ x ])) l.++ l.map Todo.id (CompleteAllTodos xs)
  ≡⟨ cong (l._++ l.map Todo.id (CompleteAllTodos xs)) (CompleteAllTodosDoesntChangeIds (x l.∷ l.[])) ⟩
    l.map Todo.id (l.[ x ]) l.++ l.map Todo.id (CompleteAllTodos xs)
  ≡⟨⟩
    l.[ Todo.id x ] l.++ l.map Todo.id (CompleteAllTodos xs)
  ≡⟨⟩
    Todo.id x l.∷ l.map Todo.id (CompleteAllTodos xs)
  ≡⟨ cong (Todo.id x l.∷_) (CompleteAllTodosDoesntChangeIds xs) ⟩
    Todo.id x l.∷ l.map Todo.id xs
  ≡⟨⟩
    l.map Todo.id (x l.∷ xs)
  ∎

CompleteAllTodosDoesntChangeText :
  (todos : List Todo) →
    l.map Todo.text (CompleteAllTodos todos) ≡ l.map Todo.text todos
CompleteAllTodosDoesntChangeText []       = refl
CompleteAllTodosDoesntChangeText (x ∷ []) = cong (l._∷ l.[]) (helper x)
  where
    helper :
      (x : Todo) →
        Todo.text (record x { completed = true }) ≡ Todo.text x
    helper x = refl
CompleteAllTodosDoesntChangeText (x ∷ xs) =
  begin
    l.map Todo.text (CompleteAllTodos (x l.∷ xs))
  ≡⟨⟩
    (l.map Todo.text (CompleteAllTodos l.[ x ])) l.++ l.map Todo.text (CompleteAllTodos xs)
  ≡⟨ cong (l._++ l.map Todo.text (CompleteAllTodos xs)) (CompleteAllTodosDoesntChangeText (x l.∷ l.[])) ⟩
    l.map Todo.text (l.[ x ]) l.++ l.map Todo.text (CompleteAllTodos xs)
  ≡⟨⟩
    l.[ Todo.text x ] l.++ l.map Todo.text (CompleteAllTodos xs)
  ≡⟨⟩
    Todo.text x l.∷ l.map Todo.text (CompleteAllTodos xs)
  ≡⟨ cong (Todo.text x l.∷_) (CompleteAllTodosDoesntChangeText xs) ⟩
    Todo.text x l.∷ l.map Todo.text xs
  ≡⟨⟩
    l.map Todo.text (x l.∷ xs)
  ∎

CompleteAllTodosLengthUnchanged :
  (todos : List Todo) →
    l.length (CompleteAllTodos todos) ≡ l.length todos
CompleteAllTodosLengthUnchanged todos = length-map (λ todo → record todo { completed = true }) todos
-- END CompleteAllTodos is well-defined

-- CompleteAllTodos-idem

-- {-# COMPILE JS CompleteAllTodos =
--   function (todos) {
--     return todos.map(function(todo) {
--       todo.completed = true;
--       return todo;
--     });
--   }
-- #-}

ClearCompleted : (List Todo) → (List Todo)
ClearCompleted todos =
  (l.filter (λ todo → dec-¬ ((Todo.completed todo) Bool.≟ true)) todos)

-- ClearCompleted is well-defined
ClearCompletedRemovesOnlyCompleted :
  (todos : List Todo) →
    l.map Todo.completed (ClearCompleted todos) ≡ l.map Todo.completed (l.filter (λ todo → dec-¬ ((Todo.completed todo) Bool.≟ true)) todos)
ClearCompletedRemovesOnlyCompleted todos = refl

ClearCompletedDoesntChangeCompleted :
  (todos : List Todo) →
    l.map Todo.completed (ClearCompleted todos) ≡ l.map Todo.completed (l.filter (λ todo → dec-¬ ((Todo.completed todo) Bool.≟ true)) todos)
ClearCompletedDoesntChangeCompleted todos = refl

ClearCompletedDoesntChangeIds :
  (todos : List Todo) →
    l.map Todo.id (ClearCompleted todos) ≡ l.map Todo.id (l.filter (λ todo → dec-¬ ((Todo.completed todo) Bool.≟ true)) todos)
ClearCompletedDoesntChangeIds todos = refl

ClearCompletedDoesntChangeText :
  (todos : List Todo) →
    l.map Todo.text (ClearCompleted todos) ≡ l.map Todo.text (l.filter (λ todo → dec-¬ ((Todo.completed todo) Bool.≟ true)) todos)
ClearCompletedDoesntChangeText todos = refl
-- END ClearCompleted is well-defined

ClearCompleted-idem :
  (todos : List Todo) →
    ClearCompleted (ClearCompleted todos) ≡ ClearCompleted todos
ClearCompleted-idem todos = filter-idem (λ e → dec-¬ (Todo.completed e Bool.≟ true)) todos

-- {-# COMPILE JS ClearCompleted =
--   function (todos) {
--     return todos.filter(function(todo) {
--       return !todo.completed;
--     });
--   }
-- #-}

-- interactions
-- AddTodo-AddTodo
-- DeleteTodo-DeleteTodo
-- AddTodo-DeleteTodo
-- DeleteTodo-AddTodo
-- EditTodo-EditTodo
-- AddTodo-EditTodo
-- EditTodo-AddTodo
-- ...

max_stars_repo_name: frankymacster/redux

max_issues_repo_name: frankymacster/redux

max_forks_repo_name: frankymacster/redux


text:
module aux where

open import Data.Nat
open import Level renaming (zero to lzero)
open import Data.Fin
open import Data.Fin.Properties
open import Data.Fin.Subset renaming (∣_∣ to ∣_∣ˢ)
open import Data.Fin.Subset.Properties
open import Data.Vec
open import Data.Bool
open import Data.Bool.Properties
open import Data.Product
open import Data.Sum
open import Relation.Unary hiding (_∈_ ; _⊆_)
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Nullary.Sum
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open import Data.Empty renaming (⊥ to ⊥')

postulate
  ext : {A : Set}{B : A → Set}{f : (x : A) → B x} {g : (x : A) → B x} →
    (∀ x → f x ≡ g x) → f ≡ g

sum-eq : {A B : Set} {x y : A} → (inj₁{B = B} x) ≡ (inj₁{B = B} y) → x ≡ y
sum-eq {A} {B} {x} {.x} refl = refl

in-subset-eq : {n : ℕ} {x : Fin n} {s : Subset n} → (l l' : x ∈ s) → l ≡ l'
in-subset-eq {.(ℕ.suc _)} {.zero} here here = refl
in-subset-eq {.(ℕ.suc _)} {.(Fin.suc _)} (there l) (there l') = cong there (in-subset-eq l l')

dec-manipulate : {n : ℕ} {A : Set} → (dec : (a a' : A) → Dec (a ≡ a')) → ((a a' : A ⊎ Fin 1) → Dec (a ≡ a'))
dec-manipulate {n} {A} dec (inj₁ x) (inj₁ x₁)
  with dec x x₁
...  | yes p = yes (cong inj₁ p)
...  | no ¬p = no λ x₂ → contradiction (sum-eq x₂) ¬p
dec-manipulate {n} {A} dec (inj₁ x) (inj₂ y) = no λ ()
dec-manipulate {n} {A} dec (inj₂ y) (inj₁ x) = no λ ()
dec-manipulate {n} {A} dec (inj₂ zero) (inj₂ zero) = yes (cong inj₂ refl)

f-manipulate : {n : ℕ} {A : Set} {s : Subset n} → ((l : Fin n) → l ∈ s → A) → (Fin n → (A ⊎ Fin 1))
f-manipulate {n} {A} {s} f l
  with l ∈? s
...  | yes p = inj₁ (f l p)
...  | no ¬p = inj₂ zero

f-equal : {n : ℕ} {A : Set} {dec : (a a' : A) → Dec (a ≡ a')} → (f f' : (l : Fin n) → A) → Dec (f ≡ f')
f-equal {n} {A} {dec} f f'
  with all?{n} λ x → dec (f x) (f' x)
...  | yes p = yes (ext p)
...  | no ¬p = no λ x → contradiction (cong-app x) ¬p

f-manipulate-eq⇒f-eq : {n : ℕ} {A : Set} {s : Subset n} {f f' : (l : Fin n) → l ∈ s → A} → (f-manipulate f) ≡ (f-manipulate f') → f ≡ f'
f-manipulate-eq⇒f-eq {n} {A} {s} {f} {f'} eq
  with (cong-app eq)
...  | eq' = ext (λ x → ext (ϱ x))
     where ϱ : (l : Fin n) → (i : l ∈ s) → f l i ≡ f' l i
           ϱ l i
             with (eq' l)
           ...  | eq''
                with l ∈? s
           ...     | yes p rewrite (in-subset-eq i p) = sum-eq eq''
           ...     | no ¬p = contradiction i ¬p

f-eq⇒f-manipulate-eq : {n : ℕ} {A : Set} {s : Subset n} {f f' : (l : Fin n) → l ∈ s → A} → f ≡ f' → (f-manipulate f) ≡ (f-manipulate f')
f-eq⇒f-manipulate-eq {n} {A} {s} {f} {f'} eq
  with (cong-app eq)
...  | eq' = ext (λ x → ϱ x)
     where ϱ : (l : Fin n) → (f-manipulate f l) ≡ (f-manipulate f' l)
           ϱ l
             with (eq' l)
           ...  | eq''
                 with l ∈? s
           ...      | yes p = cong inj₁ ((cong-app eq'') p)
           ...      | no ¬p = refl

_≡ᶠ?_ : {n : ℕ} {s : Subset n} {A : Set} {dec : (a a' : A) → Dec (a ≡ a')} (f f' : (l : Fin n) → s Data.Vec.[ l ]= inside → A) → Dec (f ≡ f')
_≡ᶠ?_ {n} {s} {A} {dec} f f'
  with (f-equal{dec = dec-manipulate{n} dec} (f-manipulate f) (f-manipulate f'))
...     | yes p = yes (f-manipulate-eq⇒f-eq p)
...     | no ¬p = no (contraposition f-eq⇒f-manipulate-eq ¬p)

x∷xs≡y∷ys⇒x≡y : {n : ℕ} {xs ys : Subset n} {x y : Bool} → (x ∷ xs) ≡ (y ∷ ys) → x ≡ y
x∷xs≡y∷ys⇒x≡y {n} {xs} {.xs} {x} {.x} refl = refl

x∷xs≡y∷ys⇒xs≡ys : {n : ℕ} {xs ys : Subset n} {x y : Bool} → (x ∷ xs) ≡ (y ∷ ys) → xs ≡ ys
x∷xs≡y∷ys⇒xs≡ys {n} {xs} {.xs} {x} {.x} refl = refl

_≡ˢ?_ : {n : ℕ} → (s s' : Subset n) → Dec (s ≡ s')
_≡ˢ?_ {zero} [] [] = yes refl
_≡ˢ?_ {suc n} (x ∷ s) (x₁ ∷ s')
  with _≡ˢ?_ {n} s s' | x Data.Bool.Properties.≟ x₁
...  | yes p | yes p' rewrite p | p' = yes refl
...  | yes p | no ¬p' rewrite p = no λ x₂ → contradiction (x∷xs≡y∷ys⇒x≡y x₂) ¬p'
...  | no ¬p | _ = no (λ x₂ → contradiction (x∷xs≡y∷ys⇒xs≡ys x₂) ¬p)

empty-subset-outside : {n : ℕ} → (x : Fin n) → ¬ (⊥ [ x ]= inside)
empty-subset-outside {.(ℕ.suc _)} zero ()
empty-subset-outside {.(ℕ.suc _)} (Fin.suc x) (there ins) = empty-subset-outside x ins

x∈[l]⇒x≡l : {n : ℕ} {x l : Fin n} → x ∈ ⁅ l ⁆ → x ≡ l
x∈[l]⇒x≡l {.(ℕ.suc _)} {zero} {zero} ins = refl
x∈[l]⇒x≡l {.(ℕ.suc _)} {Fin.suc x} {zero} (there ins) = contradiction ins (empty-subset-outside x)
x∈[l]⇒x≡l {.(ℕ.suc _)} {Fin.suc x} {Fin.suc l} (there ins) = cong Fin.suc (x∈[l]⇒x≡l ins)

l∈L⇒[l]⊆L : {n : ℕ} {l : Fin n} {L : Subset n} → l ∈ L → ⁅ l ⁆ ⊆ L
l∈L⇒[l]⊆L {n} {l} {L} ins x rewrite (x∈[l]⇒x≡l x) = ins

[l]⊆L⇒l∈L : {n : ℕ} {l : Fin n} {L : Subset n} → ⁅ l ⁆ ⊆ L → l ∈ L
[l]⊆L⇒l∈L {n} {l} {L} sub = sub (x∈⁅x⁆ l)

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
module Issue2486 where

open import Common.Prelude
open import Issue2486.Import
open import Issue2486.ImportB
open import Issue2486.HaskellB

f : MyList String → String
f [] = "sdf"
f (x :: _) = x

xs : MyList String
xs = "sdfg" :: []

postulate
  toBList : ∀ {A} → MyList A → BList A
  fromBList : ∀ {A} → BList A → MyList A

{-# COMPILE GHC toBList   = \ _ xs -> xs #-}
{-# COMPILE GHC fromBList = \ _ xs -> xs #-}

{-# FOREIGN GHC import qualified MAlonzo.Code.Issue2486.HaskellB as B #-}

data Test : Set where
  Con : BBool → Test
{-# COMPILE GHC Test = data B.Test ( B.Con ) #-}

{-
ff : BBool
ff = BTrue
-}

main : IO Unit
main =
  putStrLn (f (fromBList (toBList xs)))


text:
{-# OPTIONS -v treeless.opt:20 #-}
-- Tests for case-on-case simplification.
module _ where

open import Common.Prelude
open import Common.Integer

data Cmp : Set where
  less equal greater : Cmp

isLess : Cmp → Bool
isLess less = true
isLess equal = false
isLess greater = false
{-# INLINE isLess #-}

postulate _-_ : Integer → Integer → Integer
{-# COMPILED _-_ (-) #-}
{-# COMPILED_UHC _-_ UHC.Agda.Builtins.primIntegerMinus #-}
{-# COMPILED_JS _-_ function(x) { return function(y) { return agdaRTS.uprimIntegerMinus(x, y); }; } #-}

compareInt : Integer → Integer → Cmp
compareInt a b with a - b
... | pos 0       = equal
... | pos (suc _) = greater
... | negsuc _    = less
{-# INLINE compareInt #-}

_<_ : Integer → Integer → Bool
a < b = isLess (compareInt a b)
{-# INLINE _<_ #-}

cmp : Integer → Integer → String
cmp a b with a < b
... | true  = "less"
... | false = "not less"

fancyCase : Nat → Cmp → Nat
fancyCase 0 _ = 0
fancyCase (suc (suc (suc n))) greater = n
fancyCase (suc (suc (suc _))) equal = 4
fancyCase 1 _ = 1
fancyCase 2 _ = 2
fancyCase (suc n) less = n

main : IO Unit
main = putStrLn (cmp (pos 31) (negsuc 5)) ,,
       putStrLn (cmp (pos 5) (pos 5)) ,,
       putStrLn (cmp (negsuc 4) (negsuc 2))

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
-- Andreas, AIM XIII, 2011-04-07
-- {-# OPTIONS -v tc.rec.proj:50 #-}
module DependentIrrelevance where

open import Common.Irrelevance

ElimSq = {A : Set}(P : Squash A -> Set)
         (ih : .(a : A) -> P (squash a)) ->
         (a- : Squash A) -> P a-
elimSq : ElimSq
elimSq P ih (squash a) = ih a

elimSq' : ElimSq
elimSq' P ih a- = ih (Squash.unsquash a-)

ElimSq' = {A : Set}(P : Squash A -> Set)
          (ih : forall .a -> P (squash a)) ->
          (a- : Squash A) -> P a-

record Union (A : Set)(B : .A -> Set) : Set where
  field
    .index : A
    elem   : B index

makeUnion : {A : Set}{B : .A -> Set}.(index : A)(elem : B index) -> Union A B
makeUnion i e = record { index = i ; elem = e }

{- extended parsing examples (do not work yet)

postulate
  A : Set
  P : .A -> Set
  a : A

f1 : _
f1 = λ .x -> P x

f2 : .A -> A
f2 = λ x -> a

postulate
  g   : forall .x -> P x
  f   : (.x : A) -> P x
  f'  : .(x : A) -> P x
  f'' : forall .x .(y : A) -> P x
  g1  : forall .(x y : A) -> P x
  g2  : forall (.x .y : A) -> P x
  g3  : forall {.x .y : A} -> P x
  g4  : forall x1 {.x2} .{x3 x4} {.x y} -> P x

-}


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

-- Properties valid of all Functors
open import Level
open import Data.Product using (proj₁; proj₂; _,_; _×_; Σ)
open import Function.Surjection using (Surjective)
open import Function.Equivalence using (Equivalence)
open import Function.Equality using (Π; _⟶_; _⟨$⟩_; cong)
open import Relation.Binary using (_Preserves_⟶_)
open import Relation.Nullary

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

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

Contravariant : ∀ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Set _
Contravariant C D = Functor (Category.op C) D

Faithful : Functor C D → Set _
Faithful {C = C} {D = D} F = ∀ {X Y} → (f g : C [ X , Y ]) → D [ F₁ f ≈ F₁ g ] → C [ f ≈ g ]
  where open Functor F

Full : Functor C D → Set _
Full {C = C} {D = D} F = ∀ {X Y} → Surjective {To = D.hom-setoid {F₀ X} {F₀ Y}} G
  where
    module C = Category C
    module D = Category D
    open Functor F
    G : ∀ {X Y} → (C.hom-setoid {X} {Y}) ⟶ D.hom-setoid {F₀ X} {F₀ Y}
    G = record { _⟨$⟩_ = F₁ ; cong = F-resp-≈ }

FullyFaithful : Functor C D → Set _
FullyFaithful F = Full F × Faithful F

-- Note that this is a constructive version of Essentially Surjective, which is
-- quite a strong assumption.
EssentiallySurjective : Functor C D → Set _
EssentiallySurjective {C = C} {D = D} F = (d : Category.Obj D) → Σ C.Obj (λ c → Functor.F₀ F c ≅ d)
  where
  open Morphism D
  module C = Category C

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

module _ (F : Functor C D) where
  private
    module C = Category C using (Obj; _∘_; _⇒_; id; module HomReasoning)
    module D = Category D
    module IsoC = IsoEquiv C
    module IsoD = IsoEquiv D
  open C hiding (_∘_)
  open Functor F
  open Morphism

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

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

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

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

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

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

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

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

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

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module RandomAccessList.Standard where

open import RandomAccessList.Standard.Core
open import RandomAccessList.Standard.Core.Properties
open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf)
import BuildingBlock.BinaryLeafTree as BLT

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Fin using (Fin; fromℕ≤; reduce≥; toℕ)
import      Data.Fin as Fin
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Nat.Etc
open import Data.Product as Prod
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; trans; sym; inspect)
open PropEq.≡-Reasoning

--------------------------------------------------------------------------------
-- Operations

consₙ : ∀ {n A} → BinaryLeafTree A n → 0-1-RAL A n → 0-1-RAL A n
consₙ a []        = a 1∷ []
consₙ a (  0∷ xs) = a 1∷ xs
consₙ a (x 1∷ xs) =   0∷ (consₙ (Node a x) xs)

cons : ∀ {A} → A → 0-1-RAL A 0 → 0-1-RAL A 0
cons a xs = consₙ (Leaf a) xs

headₙ :  ∀ {n A} → (xs : 0-1-RAL A n) → ⟦ xs ⟧ ≢ 0 → BinaryLeafTree A n
headₙ {n} {A} [] p = ⊥-elim (p (⟦[]⟧≡0 ([] {A} {n}) refl))
headₙ (  0∷ xs)  p = proj₁ (BLT.split (headₙ xs (contraposition (trans (⟦0∷xs⟧≡⟦xs⟧ xs)) p)))
headₙ (x 1∷ xs)  p = x

head : ∀ {A} → (xs : 0-1-RAL A 0) → ⟦ xs ⟧ ≢ 0 → A
head xs p = BLT.head (headₙ xs p)

tailₙ : ∀ {n A} → (xs : 0-1-RAL A n) → ⟦ xs ⟧ ≢ 0 → 0-1-RAL A n
tailₙ {n} {A} [] p = ⊥-elim (p (⟦[]⟧≡0 ([] {A} {n}) refl))
tailₙ (  0∷ xs)  p = proj₂ (BLT.split (headₙ xs (contraposition (trans (⟦0∷xs⟧≡⟦xs⟧ xs)) p))) 1∷ tailₙ xs (contraposition (trans (⟦0∷xs⟧≡⟦xs⟧ xs)) p)
tailₙ (x 1∷ xs)  p = 0∷ xs

tail : ∀ {A} → (xs : 0-1-RAL A 0) → ⟦ xs ⟧ ≢ 0 → 0-1-RAL A 0
tail = tailₙ

--------------------------------------------------------------------------------
-- Searching

transportFin : ∀ {a b} → a ≡ b → Fin a → Fin b
transportFin refl i = i

splitIndex : ∀ {n A} → (x : BinaryLeafTree A n) → (xs : 0-1-RAL A (suc n)) → ⟦ x 1∷ xs ⟧ ≡ (2 ^ n) + ⟦ xs ⟧
splitIndex {n} x xs =
    begin
        2 ^ n * suc (2 * ⟦ xs ⟧ₙ)
    ≡⟨ +-*-suc (2 ^ n) (2 * ⟦ xs ⟧ₙ) ⟩
        2 ^ n + 2 ^ n * (2 * ⟦ xs ⟧ₙ)
    ≡⟨ cong (_+_ (2 ^ n)) (sym (*-assoc (2 ^ n) 2 ⟦ xs ⟧ₙ)) ⟩
        2 ^ n + 2 ^ n * 2 * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ w → 2 ^ n + w * ⟦ xs ⟧ₙ) (*-comm (2 ^ n) 2) ⟩
        2 ^ n + (2 * 2 ^ n) * ⟦ xs ⟧ₙ
    ∎

elemAt : ∀ {n A} → (xs : 0-1-RAL A n) → Fin ⟦ xs ⟧ → A
elemAt {zero}  (     []) ()
elemAt {suc n} {A} ( []) i  = elemAt {n} ([] {n = n}) (transportFin (⟦[]⟧≡⟦[]⟧ {n} {A}) i)
elemAt         (  0∷ xs) i  with ⟦ 0∷ xs ⟧ | inspect ⟦_⟧ (0∷ xs)
elemAt         (  0∷ xs) () | zero  | _
elemAt {n}     (  0∷ xs) i  | suc z | PropEq.[ eq ] = elemAt xs (transportFin (trans (sym eq) (⟦0∷xs⟧≡⟦xs⟧ xs)) i)
elemAt {n}     (x 1∷ xs) i  with (2 ^ n) ≤? toℕ i
elemAt {n}     (x 1∷ xs) i  | yes p rewrite splitIndex x xs = elemAt xs (reduce≥ i p)
elemAt         (x 1∷ xs) i  | no ¬p = BLT.elemAt x (fromℕ≤ (BLT.¬a≤b⇒b<a ¬p))

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module LearnYouAn2 where

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

_+_ : ℕ → ℕ → ℕ

zero + n     = n
(suc n) + n′ = suc (n + n′)

data _even : ℕ → Set where
  ZERO : zero even
  STEP : ∀ x → x even → (suc (suc x)) even

-- To prove four is even
proof₁ : suc (suc (suc (suc zero))) even
proof₁ = STEP (suc (suc zero)) (STEP zero ZERO)

proof₂′ : (A : Set) → A → A
proof₂′ _ a = a

proof₂ : ℕ → ℕ
proof₂ = proof₂′ ℕ

max_stars_repo_name: shouya/thinking-dumps

max_issues_repo_name: shouya/thinking-dumps

max_forks_repo_name: shouya/thinking-dumps


text:
-- Andreas, 2019-08-10

record R : Set₁ where
  indutive
  field A : Set

-- The error message is strange:

-- This declaration is illegal in a record before the last field
-- when scope checking the declaration
--   record R where
--     indutive
--     field A : Set

max_stars_repo_name: cruhland/agda


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

module Categories where

open import Prelude
open import Cubical.Foundations.HLevels

record PreCategory ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  no-eta-equality
  field
    Ob    : Type ℓ₁
    Hom   : Ob → Ob → Type ℓ₂
    Id    : ∀ {X} → Hom X X
    Comp  : ∀ {X Y Z} → Hom Y Z → Hom X Y → Hom X Z
    assoc-Comp : ∀  {W X Y Z}
                    (f : Hom Y Z)
                    (g : Hom X Y)
                    (h : Hom W X) →
                    Comp f (Comp g h) ≡ Comp (Comp f g) h
    Comp-Id  : ∀ {X Y} (f : Hom X Y) → Comp f Id ≡ f
    Id-Comp  : ∀ {X Y} (f : Hom X Y) → Comp Id f ≡ f
    Hom-Set  : ∀ {X Y} → isSet (Hom X Y)

  infixr 0 _⟶_
  _⟶_ = Hom

  infixl 0 _⟵_
  _⟵_ = flip Hom

  infixr 9 _·_
  _·_ = Comp

  variable
    X Y Z : Ob

  infix 4 _≅_
  _≅_ : Ob → Ob → Type _

  Isomorphism : (X ⟶ Y) → Type ℓ₂
  Isomorphism {X} {Y} f = Σ[ g ⦂ Y ⟶ X ] × (g · f ≡ Id) × (f · g ≡ Id)

  X ≅ Y = Σ (X ⟶ Y) Isomorphism

  Domain : (X ⟶ Y) → Ob
  Domain {X} {Y} _ = X

  Codomain : (X ⟶ Y) → Ob
  Codomain {X} {Y} _ = Y

  module _ {X Y : Ob} where
    Monic : (X ⟶ Y) → Type _
    Monic f = ∀ {Z} → (g₁ g₂ : Z ⟶ X) → f · g₁ ≡ f · g₂ → g₁ ≡ g₂

    Epic : (X ⟶ Y) → Type _
    Epic f = ∀ {Z} → (g₁ g₂ : Y ⟶ Z) → g₁ · f ≡ g₂ · f → g₁ ≡ g₂

  IsInitial : Ob → Type _
  IsInitial I = ∀ {X} → isContr (I ⟶ X)

  IsTerminal : Ob → Type _
  IsTerminal T = ∀ {X} → isContr (X ⟶ T)

  Initial = ∃ x × IsInitial x
  Terminal = ∃ x × IsTerminal x

  refl-≅ : X ≅ X
  refl-≅ .fst = Id
  refl-≅ .snd .fst = Id
  refl-≅ .snd .snd .fst = Comp-Id Id
  refl-≅ .snd .snd .snd = Comp-Id Id

  sym-≅ : X ≅ Y → Y ≅ X
  sym-≅ X≅Y .fst = X≅Y .snd .fst
  sym-≅ X≅Y .snd .fst = X≅Y .fst
  sym-≅ X≅Y .snd .snd .fst = X≅Y .snd .snd .snd
  sym-≅ X≅Y .snd .snd .snd = X≅Y .snd .snd .fst

  open import Path.Reasoning

  trans-≅ : X ≅ Y → Y ≅ Z → X ≅ Z
  trans-≅ X≅Y Y≅Z .fst = Y≅Z .fst · X≅Y .fst
  trans-≅ X≅Y Y≅Z .snd .fst = X≅Y .snd .fst · Y≅Z .snd .fst
  trans-≅ X≅Y Y≅Z .snd .snd .fst =
    (X≅Y .snd .fst · Y≅Z .snd .fst) · (Y≅Z .fst · X≅Y .fst) ≡⟨ assoc-Comp _ _ _ ⟩
    ((X≅Y .snd .fst · Y≅Z .snd .fst) · Y≅Z .fst) · X≅Y .fst ≡˘⟨ cong (_· X≅Y .fst) (assoc-Comp _ _ _) ⟩
    (X≅Y .snd .fst · (Y≅Z .snd .fst · Y≅Z .fst)) · X≅Y .fst ≡⟨ cong (λ yz → (X≅Y .snd .fst · yz) · X≅Y .fst) (Y≅Z .snd .snd .fst) ⟩
    (X≅Y .snd .fst · Id) · X≅Y .fst ≡⟨ cong (_· X≅Y .fst) (Comp-Id (X≅Y .snd .fst)) ⟩
    X≅Y .snd .fst · X≅Y .fst ≡⟨ X≅Y .snd .snd .fst ⟩
    Id ∎
  trans-≅ X≅Y Y≅Z .snd .snd .snd =
    (Y≅Z .fst · X≅Y .fst) · (X≅Y .snd .fst · Y≅Z .snd .fst) ≡⟨ assoc-Comp _ _ _ ⟩
    ((Y≅Z .fst · X≅Y .fst) · X≅Y .snd .fst) · Y≅Z .snd .fst ≡˘⟨ cong (_· Y≅Z .snd .fst) (assoc-Comp _ _ _) ⟩
    (Y≅Z .fst · (X≅Y .fst · X≅Y .snd .fst)) · Y≅Z .snd .fst ≡⟨ cong (λ xy → (Y≅Z .fst · xy) · Y≅Z .snd .fst) (X≅Y .snd .snd .snd) ⟩
    (Y≅Z .fst · Id) · Y≅Z .snd .fst ≡⟨ cong (_· Y≅Z .snd .fst) (Comp-Id _) ⟩
    Y≅Z .fst · Y≅Z .snd .fst ≡⟨ Y≅Z .snd .snd .snd ⟩
    Id ∎

  idToIso : X ≡ Y → X ≅ Y
  idToIso {X} {Y} X≡Y = subst (X ≅_) X≡Y refl-≅

  ≅-set : isSet (X ≅ Y)
  ≅-set = isOfHLevelΣ 2 Hom-Set
    λ _ → isOfHLevelΣ 2 Hom-Set
    λ _ → isOfHLevelΣ 2 (isOfHLevelSuc 2 Hom-Set _ _)
    λ _ → isOfHLevelSuc 2 Hom-Set _ _

record Category ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  no-eta-equality
  field
    preCategory : PreCategory ℓ₁ ℓ₂
  open PreCategory preCategory public
  field
    univalent : {X Y : Ob} → (X ≡ Y) ≃ (X ≅ Y)

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

  _[_,_] : Ob → Ob → Type ℓ₂
  _[_,_] = Hom
  {-# INLINE _[_,_] #-}

  _[_∘_] : (Y ⟶ Z) → (X ⟶ Y) → (X ⟶ Z)
  _[_∘_] = Comp
  {-# INLINE _[_∘_] #-}

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module hott.types.theorems where

open import hott.types.nat.theorems public

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
-- Issue #1130, test generation of helper function

-- {-# OPTIONS -v tc.with:40 #-}

id : (A : Set) → A → A
id A = {!id′!}
 -- C-c C-h produces:       id′ : ∀ {A} → A
 -- when it should produce: id′ : ∀ {A} → A → A

f : (A : Set) (B : A → Set) (a : A) → B a
f A B a = {!g A a!}
  -- Before: ∀ {A} {B : A → Set} A₁ (a : A₁) → B a
  -- After:  ∀ A (a : A) {B : A → Set} → B a
  -- Andreas, 2019-10-12:  ∀ {A} {B : A → Set} (a : A) → B a

open import Agda.Builtin.Bool

if_then_else : ∀{a} {A : Set a} (b : Bool) (t e : A) → A
if true  then t else e = t
if false then t else e = e

-- Andreas, 2019-10-12, issue #1050: Prevent unnecessary normalization.

id₂ : (A B : Set) → if true then A else B → if false then B else A
id₂ A B x = {!id₂′ x!}
  -- C-c C-h produces
  -- id₂′ : ∀ {A} {B} (x : if true then A else B) →
  --        if false then B else A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue117 where

Set′ = Set

record ⊤ : Set′ where
data   ⊥ : Set′ where


text:
module PiNF-semantics where

open import Data.Nat hiding (_⊔_; suc; _+_; _*_)
open import Data.Vec
open import Level
open import Algebra.Structures

open import PiNF-algebra

------------------------------------------------------------------------------
-- Define module over a ring (the types bot, top, disjoint union, and product
-- do form a ring as shown in the type-iso library)

R-module : ℕ → Set → Set
R-module dim c = Vec c dim

-- The only element of (R-module 0) is the zero vector

zeroV : ∀ {A : Set} → R-module 0 A
zeroV = []

-- (R-module 1 A) is isomorphic to A

v-R1 : ∀ {A : Set} → A → R-module 1 A
v-R1 a = [ a ]

R1-v : ∀ {A : Set} → R-module 1 A → A
R1-v (a ∷ []) = a

--

module MR (C : CommutativeSemiringWithoutAnnihilatingZero Level.zero Level.zero) where

  open Data.Nat using (ℕ; zero; suc; _+_; _*_)
  open Data.Vec using ([]; _∷_; map; _++_)
  open CommutativeSemiringWithoutAnnihilatingZero
    using (Carrier; _≈_; 0#; 1#)
    renaming (_+_ to _+r_; _*_ to _*r_)

{--
  zeroV : ∀ {b : Set} → R-module b 0
  zeroV = []

  tensorV : {b₁ b₂ : Set } {m₁ m₂ : ℕ} →
            R-module b₁ m₁ → R-module b₂ m₂ →
            R-module (b₁ × b₂) (m₁ * m₂)
  tensorV [] _ = []
  tensorV (x ∷ xs) ys = (map (λ y → (x , y)) ys) ++ (tensorV xs ys)

  addV : {n : ℕ} → R-module (Carrier C) n → R-module (Carrier C) n
                 → R-module (Carrier C) n
  addV x y = Data.Vec.zipWith (_+r_ C) x y

--}

open MR

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Primitive

record Graph ℓv ℓe : Set (lsuc (ℓv ⊔ ℓe)) where
  field
    Obj : Set ℓv
    Hom : Obj → Obj → Set ℓe

open Graph public

postulate
  t : Nat → Nat → Bool

ωGr : Graph lzero lzero
Obj ωGr = Nat
Hom ωGr m n with t m n
... | true = {!!} -- if n ≡ (suc m)
... | false = {!!} -- otherwise

foo : ∀ m n → Hom ωGr m n → {!!}
foo m n f with t m n
... | z = {!!}

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≥_; _≤_; z≤n; s≤s)
open import Function.Equivalence using (_⇔_)
open import Relation.Binary.PropositionalEquality using (→-to-⟶)

postulate
  adjoint : ∀ {x y z} → x + y ≥ z ⇔ x ≥ z ∸ y
  unit : ∀ {x y} → x ≥ (x + y) ∸ y
  apply : ∀ {x y} → (x ∸ y) + y ≥ x


text:
module _ where

open import Agda.Builtin.Nat renaming (Nat to Nombre)
open import Agda.Builtin.Equality
open import Agda.Builtin.String
open import Agda.Builtin.Reflection

check₁ : primShowQName (quote Nombre) ≡ "Agda.Builtin.Nat.Nat"
check₁ = refl

check₂ : primShowQName (quote Agda.Builtin.Nat.Nat) ≡ "Agda.Builtin.Nat.Nat"
check₂ = refl


text:
open import FRP.JS.Nat using ( ℕ ; _+_ ; _≤_ ; _<_ ; _≟_ )
open import FRP.JS.True using ( True ; False )

module FRP.JS.Nat.Properties where

postulate
  ≤-impl-≯ : ∀ {m n} → True (m ≤ n) → False (n < m)
  ≤≠-impl-< : ∀ {m n} → True (m ≤ n) → False (m ≟ n) → True (m < n)
  <-impl-s≤ : ∀ {m n} → True (m < n) → True (1 + m ≤ n)
  ≤-bot : ∀ {n} → True (0 ≤ n)

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module _ where

open import Agda.Builtin.Reflection
open import Agda.Builtin.Equality

module M where
  open import Agda.Builtin.Nat renaming (Nat to Nombre)
  a = quote Nombre

fail : M.a ≡ quote Name
fail = refl

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --safe --without-K #-}
open import Generics.Prelude
open import Generics.Telescope
open import Generics.Desc
open import Generics.All

module Generics.Accessibility
  {P I ℓ} (A : Indexed P I ℓ)
  {n} (D : DataDesc P I n)
  (let A′ = uncurry P I A)
  (split : ∀ {pi} → A′ pi → ⟦ D ⟧Data A′ pi)
  {p} where

  -- | Accessibility predicate for datatype A at value x
  data Acc {i} (x : A′ (p , i)) : Setω where
    acc : AllDataω Acc D (split x) → Acc x

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007

                   Agda

                Ulf Norell

-}

-- Records are labeled sigma types.

module Records where

open import Nat
open import Bool

{-

  A very simple record.

-}

record Point : Set where
  field
    x : Nat
    y : Nat

-- A record can be seen as a one constructor datatype. In this case:
data Point' : Set where
  mkPoint : (x : Nat)(y : Nat) -> Point'

-- There are a few differences, though:

-- To construct a record you use the syntax record { ..; x = e; .. }
origin : Point
origin = record { x = 0; y = 0 }

-- instead of
origin' : Point'
origin' = mkPoint 0 0

-- What's more interesting is that you get projection functions
-- for free when you declare a record. More precisely, you get a module
-- parameterised over a record, containing functions corresponding to the
-- fields. In the Point example you get:
{-
  module Point (p : Point) where
    x : Nat
    y : Nat
-}

-- So Point.x : Point -> Nat is the projection function for the field x.
getX : Point -> Nat
getX = Point.x

-- A nifty thing with having the projection functions in a module is that
-- you can apply the module to a record value, in effect opening the record.
sum : Point -> Nat
sum p = x + y
  where
   open module Pp = Point p

-- The final difference between records and datatypes is that we have
-- η-equality on records.

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

η-Point : (p : Point) -> p == record { x = Point.x p; y = Point.y p }
η-Point p = refl

{-

  The empty record

-}

-- One interesting benefit of this is that we get a unit type with
-- η-equality.
record True : Set where

tt : True
tt = record{}

-- Now, since any element of True is equal to tt, metavariables of
-- type True will simply disappear. The following cute example exploits
-- this:

data False : Set where

NonZero : Nat -> Set
NonZero zero    = False
NonZero (suc _) = True

-- We make the proof that m is non-zero implicit.

_/_ : (n m : Nat){p : NonZero m} -> Nat
(n / zero) {}
zero  / suc m = zero
suc n / suc m = div (suc n) (suc m) m
  where
    div : Nat -> Nat -> Nat -> Nat
    div  zero    zero   c = suc zero
    div  zero   (suc y) c = zero
    div (suc x)  zero   c = suc (div x c c)
    div (suc x) (suc y) c = div x y c

-- Now, as long as we're dividing by things which are obviously
-- NonZero we can completely ignore the proof.

five = 17 / 3

{-

  A dependent record

-}

-- Of course, records can be dependent, and have parameters.
record ∃ {A : Set}(P : A -> Set) : Set where
  field
    witness : A
    proof   : P witness


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Sigma.Base where

open import Cubical.Core.Primitives public

-- Σ-types are defined in Core/Primitives as they are needed for Glue types.

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module FMSB where

data Nat : Set where
  ze : Nat
  su : Nat -> Nat

data Lam (X : Nat -> Set)(n : Nat) : Set where
  var : X n -> Lam X n
  app : Lam X n -> Lam X n -> Lam X n
  lam : Lam X (su n) -> Lam X n

_->>_ : {I : Set}(X Y : I -> Set) -> Set
X ->> Y = {i : _} -> X i -> Y i

fmsub : {X Y : Nat -> Set} -> (X ->> Lam Y) -> Lam X ->> Lam Y
fmsub sb (var x)   = sb x
fmsub sb (app f s) = app (fmsub sb f) (fmsub sb s)
fmsub sb (lam b)   = lam (fmsub sb b)

data Fin : Nat -> Set where
  ze : {n : Nat} -> Fin (su n)
  su : {n : Nat} -> Fin n -> Fin (su n)

D : (Nat -> Set) -> Nat -> Set
D F n = F (su n)

weak : {F : Nat -> Set} -> (Fin ->> F) -> (F ->> D F) ->
       {m n : Nat}-> (Fin m -> F n) -> D Fin m -> D F n
weak v w f ze      = v ze
weak v w f (su x)  = w (f x)

_+_ : Nat -> Nat -> Nat
ze    + y = y
su x  + y = su (x + y)

_!+_ : (Nat -> Set) -> Nat -> (Nat -> Set)
F !+ n = \ m -> F (m + n)

weaks : {F : Nat -> Set} -> (Fin ->> F) -> (F ->> D F) ->
        {m n : Nat}-> (Fin m -> F n) -> (Fin !+ m) ->> (F !+ n)
weaks v w f {ze}    = f
weaks v w f {su i}  = weak v w (weaks v w f {i})

jing : {m n : Nat} -> Lam Fin (m + n) -> Lam (Fin !+ n) m
jing (var x) = var x
jing (app f s) = app (jing f) (jing s)
jing (lam t) = lam (jing t)

gnij : {m n : Nat} -> Lam (Fin !+ n) m -> Lam Fin (m + n)
gnij (var x) = var x
gnij (app f s) = app (gnij f) (gnij s)
gnij (lam t) = lam (gnij t)

ren : {m n : Nat} -> (Fin m -> Fin n) -> Lam Fin m -> Lam Fin n
ren f t = gnij (fmsub (\ {i} x -> var (weaks (\ z -> z) su f {i} x)) {ze} (jing t))

sub : {m n : Nat} -> (Fin m -> Lam Fin n) -> Lam Fin m -> Lam Fin n
sub {m}{n} f t = gnij {ze} (fmsub (\ {i} x -> jing {i} (weaks {Lam Fin} var (ren su) f {i} x)) (jing {ze} t))

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
{-# OPTIONS --guardedness #-}

module Iterator where

import      Lvl
open import Data.Option as Option using (Option ; Some ; None)
open import Data.Tuple  as Tuple  using (_⨯_ ; _,_)
open import Type

private variable ℓ : Lvl.Level
private variable T A B : Type{ℓ}
private variable a x init : T
private variable f : A → B

-- A finite/infinite sequence.
record Iterator (T : Type{ℓ}) : Type{ℓ} where
  coinductive
  field
    next : Option(T ⨯ Iterator(T))

open Iterator

empty : Iterator(T)
next empty = None

singleton : T → Iterator(T)
next(singleton x) = Some(x , empty)

prepend : T → Iterator(T) -> Iterator(T)
next(prepend x i) = Some(x , i)

import Data.Option.Functions as Option

head : Iterator(T) → Option(T)
head i = Option.map Tuple.left (next(i))

tail : Iterator(T) → Option(Iterator(T))
tail i = Option.map Tuple.right (next(i))

open import Functional

tail₀ : Iterator(T) → Iterator(T)
tail₀ = (Option._or empty) ∘ tail

open import Numeral.Natural
open import Numeral.Natural.Induction

index : ℕ → Iterator(T) → Option(T)
index n      i with next(i)
index _      _ | None        = None
index 𝟎      _ | Some(x , r) = Some x
index (𝐒(k)) _ | Some(x , r) = index k r

repeat : T → Iterator(T)
next(repeat(x)) = Some(x , repeat(x))

map : (A → B) → (Iterator(A) → Iterator(B))
next(map f(i)) with next(i)
... | None        = None
... | Some(x , r) = Some(f(x) , map f(r))
-- Option.map (Tuple.map f (map f)) (next i)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda