text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Reflexivity
open import Oscar.Class.Smap
open import Oscar.Class.Surjextensionality
open import Oscar.Class.Surjidentity
open import Oscar.Class.Surjtranscommutativity
open import Oscar.Class.HasEquivalence
open import Oscar.Class.Transitivity
open import Oscar.Class.Thickandthin
open import Oscar.Class.IsPrefunctor
open import Oscar.Class.IsFunctor
open import Oscar.Data.Maybe
open import Oscar.Data.¶
open import Oscar.Data.Fin
open import Oscar.Data.Proposequality
open import Oscar.Data.Substitunction
open import Oscar.Data.Term
open import Oscar.Data.Substitist
open import Oscar.Data.Descender
import Oscar.Property.Setoid.Proposextensequality
import Oscar.Property.Functor.SubstitunctionExtensionTerm
import Oscar.Property.Category.AListProposequality
import Oscar.Property.Category.ExtensionProposextensequality
import Oscar.Property.Thickandthin.FinFinProposequalityMaybeProposequality
import Oscar.Class.HasEquivalence.Substitunction
import Oscar.Class.Surjection.⋆

module Oscar.Property.Functor.SubstitistProposequalitySubstitunctionProposextensequality where

module _ {𝔭} {𝔓 : Ø 𝔭} where

  open Substitunction 𝔓
  open Term 𝔓
  open Substitist 𝔓

  _for_ : ∀ {n} (t' : Term n) (x : Fin (↑ n)) → Fin (↑ n) → Term n
  (t for x) y = maybe′ ε t (check[ Maybe ] x y)

  instance

    𝓢urjectivitySubstitist,Substitunction : Smap.class Substitist Substitunction ¡ ¡
    𝓢urjectivitySubstitist,Substitunction .⋆ _ _ ∅ = i
    𝓢urjectivitySubstitist,Substitunction .⋆ _ _ ((x , t) , σ) = 𝓢urjectivitySubstitist,Substitunction .⋆ _ _ σ ∙ (t for x)

    𝓢urjextensionalitySubstitist,Substitunction : Surjextensionality.class Substitist Proposequality Substitunction _≈_ ¡ smap
    𝓢urjextensionalitySubstitist,Substitunction .⋆ _ _ _ _ ∅ _ = ∅

    𝓢urjtranscommutativitySubstitist,Substitunction : Surjtranscommutativity.class Substitist Substitunction _≈_ smap transitivity transitivity
    𝓢urjtranscommutativitySubstitist,Substitunction .⋆ ∅ _ _ = ∅
    𝓢urjtranscommutativitySubstitist,Substitunction .⋆ ((π₀ , π₁) , f) g =
      let _⟪∙⟫′_ = flip (𝓢urjtranscommutativitySubstitist,Substitunction .⋆) in -- kludge for Agda's termination checker

        (
            § g ⟪∙⟫ §[ Substitunction ] f
          ∙
            ⟪ g ⟪∙⟫′ f ⟫[ Proposextensequality ]
        )
      ∘
        π₁ for π₀

    IsPrefunctorSubstitist,Substitunction : IsPrefunctor Substitist Proposequality transitivity Substitunction _≈_ transitivity smap
    IsPrefunctorSubstitist,Substitunction = ∁

    𝓢urjidentitySubstitist,Substitunction : Surjidentity.class Substitist Substitunction _≈_ smap ε ε
    𝓢urjidentitySubstitist,Substitunction .⋆ _ = ∅

    IsFunctorSubstitist,Substitunction : IsFunctor Substitist Proposequality ε transitivity Substitunction _≈_ ε transitivity smap
    IsFunctorSubstitist,Substitunction = ∁


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

module Substream (A : Set) where

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PE
open import PropsAsTypes
open import Stream

open Bisim A
open ~-Reasoning

mutual
  record Sel : Set where
    coinductive
    field out : Selμ

  data Selμ : Set where
    pres  : Sel → Selμ
    drop  : Selμ → Selμ

open Sel public

filterμ  : Selμ → Stream A → Stream A
filter   : Sel → Stream A → Stream A

filter x = filterμ (x .out)

filterμ (pres x) s .hd  = s .hd
filterμ (pres x) s .tl  = filter x (s .tl)
filterμ (drop u) s      = filterμ u (s .tl)

_≤[_]_ : Stream A → Sel → Stream A → Prop
s ≤[ x ] t = s ~ filter x t

_≤μ[_]_ : Stream A → Selμ → Stream A → Prop
s ≤μ[ u ] t = s ~ filterμ u t

_≤'_ : Stream A → Stream A → Prop
s ≤' t = ∃[ x ∈ Sel ] (s ≤[ x ] t)

_•_   : Sel → Sel → Sel
_•μ_  : Selμ → Selμ → Selμ

(x • y) .out = (x .out) •μ (y .out)

(pres x')  •μ (pres y')  = pres (x' • y')
(drop u')  •μ (pres y')  = drop (u' •μ (y' .out))
u          •μ (drop v')  = drop (u •μ v')

filter-hom   : ∀ x y s → filter (y • x) s ~ filter y (filter x s)
filterμ-hom  : ∀ u v s → filterμ (v •μ u) s ~ filterμ v (filterμ u s)

filter-hom x y s = filterμ-hom (x .out) (y .out) s

filterμ-hom (pres x) (pres y)  s .hd≡  = refl
filterμ-hom (pres x) (pres y)  s .tl~  = filter-hom x y (s .tl)
filterμ-hom (pres x) (drop v)  s       = filterμ-hom (x .out) v (s .tl)
filterμ-hom (drop u) (pres x)  s       = filterμ-hom u (pres x) (s .tl)
filterμ-hom (drop u) (drop v)  s       = filterμ-hom u (drop v) (s .tl)

filter-resp~   : ∀{s t} (x : Sel)  → s ~ t → filter x s ~ filter x t
filterμ-resp~  : ∀{s t} (u : Selμ) → s ~ t → filterμ u s ~ filterμ u t

filter-resp~ x p = filterμ-resp~ (x .out) p

filterμ-resp~ (pres x)  p .hd≡  = p .hd≡
filterμ-resp~ (pres x)  p .tl~  = filter-resp~ x (p .tl~)
filterμ-resp~ (drop u)  p       = filterμ-resp~ u (p .tl~)

≤-witness-trans : ∀{r s t} {x y} → r ≤[ x ] s → s ≤[ y ] t → r ≤[ x • y ] t
≤-witness-trans {r} {s} {t} {x} {y} p q =
  begin
    r
  ~⟨ p ⟩
    filter x s
  ~⟨ filter-resp~ x q ⟩
    filter x (filter y t)
  ~⟨ S.sym (filter-hom y x t) ⟩
    filter (x • y) t
  ∎
  where
    module S = Setoid stream-setoid

≤'-trans : ∀{r s t} → r ≤' s → s ≤' t → r ≤' t
≤'-trans = ∃₂-elim  (λ x y p q →
                    ∃-intro (x • y) (≤-witness-trans {x = x} {y} p q))

mutual
  record _≤_ (s t : Stream A) : Prop where
    coinductive
    field out≤ : s ≤μ t

  data _≤μ_ (s t : Stream A) : Prop where
    match : (s .hd ≡ t .hd) → (s .tl ≤ t .tl) → s ≤μ t
    skip  : (s ≤μ t .tl) → s ≤μ t

open _≤_ public

witness   : {s t : Stream A} → s ≤ t → Sel
witnessμ  : {s t : Stream A} → s ≤μ t → Selμ

witness p .out = witnessμ (p .out≤)

witnessμ (match _ t≤)  = pres (witness t≤)
witnessμ (skip u)      = drop (witnessμ u)

≤-implies-witnessed≤    : ∀{s t} → (p : s ≤ t) → s ≤[ witness p ] t
≤μ-implies-witnessed≤μ  : ∀{s t} → (p : s ≤μ t) → s ≤μ[ witnessμ p ] t

≤-implies-witnessed≤ {s} {t} p = ≤μ-implies-witnessed≤μ (p .out≤)

≤μ-implies-witnessed≤μ (match h≡ t≤) .hd≡  = h≡
≤μ-implies-witnessed≤μ (match h≡ t≤) .tl~  = ≤-implies-witnessed≤ t≤
≤μ-implies-witnessed≤μ (skip q)            = ≤μ-implies-witnessed≤μ q

≤-implies-≤' : _≤_ ⊑ _≤'_
≤-implies-≤' p = ∃-intro (witness p) (≤-implies-witnessed≤ p)

witnessed≤-implies-≤    : ∀{s t} (x : Sel) → s ≤[ x ] t → s ≤ t
witnessed≤μ-implies-≤μ  : ∀{s t} (u : Selμ) → s ≤μ[ u ] t → s ≤μ t

witnessed≤-implies-≤ x p .out≤ = witnessed≤μ-implies-≤μ (x .out) p

witnessed≤μ-implies-≤μ (pres x) p  = match (p .hd≡) (witnessed≤-implies-≤ x (p .tl~))
witnessed≤μ-implies-≤μ (drop u) p  = skip (witnessed≤μ-implies-≤μ u p)

≤'-implies-≤ : _≤'_ ⊑ _≤_
≤'-implies-≤ = ∃-elim witnessed≤-implies-≤

≤-and-≤'-equivalent : ∀ {s t} → s ≤ t ⇔ s ≤' t
≤-and-≤'-equivalent = equivalence ≤-implies-≤' ≤'-implies-≤

≤-trans : ∀{r s t} → r ≤ s → s ≤ t → r ≤ t
≤-trans p q = ≤'-implies-≤ (≤'-trans (≤-implies-≤' p) (≤-implies-≤' q))

ext: agda

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Structure.Category.Functor.Functors.Proofs where

import      Functional as Fn
import      Function.Equals
open        Function.Equals.Dependent
open import Function.Equals.Proofs
open import Logic.Predicate
open import Logic.Propositional
import      Lvl
open import Relator.Equals.Proofs.Equivalence
open import Structure.Category
open import Structure.Category.Functor
open import Structure.Category.Functor.Equiv
open import Structure.Category.Functor.Functors
open import Structure.Category.Morphism.IdTransport
open import Structure.Category.NaturalTransformation
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓₒ ℓₘ ℓₑ : Lvl.Level
private variable A B C : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}

open CategoryObject
open Category ⦃ … ⦄
open Functor ⦃ … ⦄

module _ where
  open Wrapped

  -- TODO: Prove transport-of-congruenced-bifunctor
  [∘ᶠᵘⁿᶜᵗᵒʳ]-binaryOperator : BinaryOperator(_∘ᶠᵘⁿᶜᵗᵒʳ_ {A = A}{B = B}{C = C})
  _≡ᶠᵘⁿᶜᵗᵒʳ_.functor-proof (BinaryOperator.congruence ([∘ᶠᵘⁿᶜᵗᵒʳ]-binaryOperator {A = A} {B = B} {C = C}) {[∃]-intro F₁} {[∃]-intro F₂} {[∃]-intro G₁} {[∃]-intro G₂} (intro fp₁ mp₁) (intro fp₂ mp₂)) = congruence₂(Fn._∘_) ⦃ [⊜][∘]-binaryOperator ⦃ function = [≡]-function ⦄ ⦄ fp₁ fp₂ where
    instance _ = [≡]-equiv {T = Object(B)}
    instance _ = [≡]-equiv {T = Object(C)}
  NaturalTransformation.natural (_≡ᶠᵘⁿᶜᵗᵒʳ_.map-proof (BinaryOperator.congruence ([∘ᶠᵘⁿᶜᵗᵒʳ]-binaryOperator {A = A} {B = B} {C = C}) {[∃]-intro F₁}{[∃]-intro F₂} {[∃]-intro G₁}{[∃]-intro G₂} (intro fp₁ mp₁) (intro fp₂ mp₂))) {x}{y} {f} = anything {-
    transport C (_⊜_.proof (congruence₂(Fn._∘_) ⦃ [⊜][∘]-binaryOperator ⦃ function = [≡]-function _ ⦄ ⦄ fp₁ fp₂)) ∘ map(map f)      🝖-[ {!x₂ y₂!} ]
    map(map f) ∘ transport C ([≡]-with-op (Object C) (λ v v₁ → {!v!}) (_⊜_.proof fp₁) (_⊜_.proof fp₂)) 🝖-[ {!!} ]
    map(map f) ∘ transport C (_⊜_.proof (congruence₂(Fn._∘_) ⦃ [⊜][∘]-binaryOperator ⦃ function = [≡]-function _ ⦄ ⦄ fp₁ fp₂)) 🝖-end-}
    where
      postulate anything : ∀{ℓ}{a : Type{ℓ}} → a
      open module MorphismEquivB {x}{y} = Equiv(morphism-equiv B {x}{y}) using () renaming (_≡_ to _≡B_)
      open module MorphismEquivC {x}{y} = Equiv(morphism-equiv C {x}{y}) using () renaming (_≡_ to _≡C_)
      instance _ = category A
      instance _ = category B
      instance _ = category C
      instance _ = [≡]-equiv {T = Object B}
      instance _ = [≡]-equiv {T = Object C}
      -- [≡]-with-op

  instance
    [∘ᶠᵘⁿᶜᵗᵒʳ]-identityₗ : Morphism.Identityₗ {Obj = CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}} (\{A} → _∘ᶠᵘⁿᶜᵗᵒʳ_ {A = A})(idᶠᵘⁿᶜᵗᵒʳ)
    _≡ᶠᵘⁿᶜᵗᵒʳ_.functor-proof (Morphism.Identityₗ.proof ([∘ᶠᵘⁿᶜᵗᵒʳ]-identityₗ) {y = B}) = reflexivity(_⊜_) where
      instance _ = [≡]-equiv {T = Object(B)}
    NaturalTransformation.natural (_≡ᶠᵘⁿᶜᵗᵒʳ_.map-proof (Morphism.Identityₗ.proof [∘ᶠᵘⁿᶜᵗᵒʳ]-identityₗ {A} {B} {[∃]-intro F})) {x} {y} {f} =
      id ∘ map f 🝖-[ Morphism.identityₗ(_∘_)(id) ]
      map f      🝖-[ Morphism.identityᵣ(_∘_)(id) ]-sym
      map f ∘ id 🝖-end
      where
        open module MorphismEquivB {x}{y} = Equiv(morphism-equiv B {x}{y}) using () renaming (_≡_ to _≡B_)
        instance _ = category A
        instance _ = category B

  instance
    [∘ᶠᵘⁿᶜᵗᵒʳ]-identityᵣ : Morphism.Identityᵣ {Obj = CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}} (\{A} → _∘ᶠᵘⁿᶜᵗᵒʳ_ {A = A})(idᶠᵘⁿᶜᵗᵒʳ)
    _≡ᶠᵘⁿᶜᵗᵒʳ_.functor-proof (Morphism.Identityᵣ.proof ([∘ᶠᵘⁿᶜᵗᵒʳ]-identityᵣ) {y = B}) = reflexivity(_⊜_) where
      instance _ = [≡]-equiv {T = Object(B)}
    NaturalTransformation.natural (_≡ᶠᵘⁿᶜᵗᵒʳ_.map-proof (Morphism.Identityᵣ.proof [∘ᶠᵘⁿᶜᵗᵒʳ]-identityᵣ {A} {B} {[∃]-intro F})) {x} {y} {f} =
      id ∘ map f 🝖-[ Morphism.identityₗ(_∘_)(id) ]
      map f      🝖-[ Morphism.identityᵣ(_∘_)(id) ]-sym
      map f ∘ id 🝖-end
      where
        open module MorphismEquivB {x}{y} = Equiv(morphism-equiv B {x}{y}) using () renaming (_≡_ to _≡B_)
        instance _ = category A
        instance _ = category B

  instance
    [∘ᶠᵘⁿᶜᵗᵒʳ]-identity : Morphism.Identity {Obj = CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}} (\{A} → _∘ᶠᵘⁿᶜᵗᵒʳ_ {A = A})(idᶠᵘⁿᶜᵗᵒʳ)
    [∘ᶠᵘⁿᶜᵗᵒʳ]-identity = [∧]-intro [∘ᶠᵘⁿᶜᵗᵒʳ]-identityₗ [∘ᶠᵘⁿᶜᵗᵒʳ]-identityᵣ

  instance
    [∘ᶠᵘⁿᶜᵗᵒʳ]-associativity : Morphism.Associativity {Obj = CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}} (\{A B C} → _∘ᶠᵘⁿᶜᵗᵒʳ_ {A = A}{B = B}{C = C})
    _≡ᶠᵘⁿᶜᵗᵒʳ_.functor-proof (Morphism.Associativity.proof [∘ᶠᵘⁿᶜᵗᵒʳ]-associativity {w = D}) = reflexivity(_⊜_) where
      instance _ = [≡]-equiv {T = Object(D)}
    NaturalTransformation.natural (_≡ᶠᵘⁿᶜᵗᵒʳ_.map-proof (Morphism.Associativity.proof [∘ᶠᵘⁿᶜᵗᵒʳ]-associativity {A}{B}{C}{D} {[∃]-intro F}{[∃]-intro G}{[∃]-intro H})) {x}{y}{f} =
      id ∘ map(map(map f)) 🝖-[ Morphism.identityₗ(_∘_)(id) ]
      map(map(map f))      🝖-[ Morphism.identityᵣ(_∘_)(id) ]-sym
      map(map(map f)) ∘ id 🝖-end
      where
        open module MorphismEquivₗ {x}{y} = Equiv(morphism-equiv D {x}{y}) using () renaming (_≡_ to _≡D_)
        instance _ = category A
        instance _ = category B
        instance _ = category C
        instance _ = category D

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:
-- Andreas, 2015-06-28, issue reported by Nisse

{-# OPTIONS -vtc.pos.occ:20 #-} -- KEEP!, this triggered the __IMPOSSIBLE__

-- {-# OPTIONS -vtc.pos.occ:70 -v tc.rec:80 --show-implicit #-}

data ⊥ : Set where

F : ⊥ → Set
F ()

record R (i : ⊥) : Set₁ where
  constructor c
  field
    P Q : F i → Set

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Syntax/Translation/InternalToAbstract.hs:874

-- The error is triggered by the use of prettyTCM in
-- Agda.TypeChecking.Positivity.getOccurrences.

-- tel = (_ : Prop) (_ : Prop) -- WRONG
-- perm = id
-- ps = (c x x : R @0) _
-- body = λ x _y _z -> x _z
-- type = F @1 → Set


text:
open import Agda.Builtin.Nat

f : Nat
f with zero
... | n with (suc n)
... | m = m

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
data Li : (a : Set) -> Set where
  Ni : {a : Set} -> Li a
  Co : {a : Set} -> a -> Li a -> Li a

{-# BUILTIN NATURAL name #-}

t : Li (Set 2) -> Set 1
t li = Set 1

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
------------------------------------------------------------------------
-- Recognisers form a Kleene algebra
------------------------------------------------------------------------

module TotalRecognisers.LeftRecursion.KleeneAlgebra (Tok : Set) where

open import Algebra
import Algebra.Properties.BooleanAlgebra
open import Codata.Musical.Notation
open import Data.Bool hiding (_∧_; _≤_)
import Data.Bool.Properties as Bool
private
  module BoolCS = CommutativeSemiring Bool.∨-∧-commutativeSemiring
  module BoolBA = Algebra.Properties.BooleanAlgebra
                    Bool.∨-∧-booleanAlgebra
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq using (_⇔_; equivalence)
open import Data.List
open import Data.List.Properties
private
  module ListMonoid {A : Set} = Monoid (++-monoid A)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product as Prod
open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; _≗_)
open import Relation.Nullary

import TotalRecognisers.LeftRecursion
open TotalRecognisers.LeftRecursion Tok hiding (left-zero)
import TotalRecognisers.LeftRecursion.Lib
open TotalRecognisers.LeftRecursion.Lib Tok
open ⊙ using (_⊙′_)
open KleeneStar₂

------------------------------------------------------------------------
-- The relation _≤_ is a partial order with respect to _≈_

module PartialOrder where

  reflexive : ∀ {n} {p : P n} → p ≤ p
  reflexive = id

  trans : ∀ {n₁ n₂ n₃} {p₁ : P n₁} {p₂ : P n₂} {p₃ : P n₃} →
          p₁ ≤ p₂ → p₂ ≤ p₃ → p₁ ≤ p₃
  trans p₁≤p₂ p₂≤p₃ = p₂≤p₃ ∘ p₁≤p₂

  antisym : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
            p₁ ≤ p₂ → p₂ ≤ p₁ → p₁ ≈ p₂
  antisym p₁≤p₂ p₂≤p₁ = equivalence p₁≤p₂ p₂≤p₁

------------------------------------------------------------------------
-- The relation _≈_ is an equality, i.e. a congruential equivalence
-- relation

module Equivalence where

  reflexive : ∀ {n} {p : P n} → p ≈ p
  reflexive = Eq.id

  sym : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} → p₁ ≈ p₂ → p₂ ≈ p₁
  sym p₁≈p₂ = Eq.sym p₁≈p₂

  trans : ∀ {n₁ n₂ n₃} {p₁ : P n₁} {p₂ : P n₂} {p₃ : P n₃} →
          p₁ ≈ p₂ → p₂ ≈ p₃ → p₁ ≈ p₃
  trans p₁≈p₂ p₂≈p₃ = Eq._∘_ p₂≈p₃ p₁≈p₂

♭♯-cong : ∀ {n₁ n₂} b₁ b₂ {p₁ : P n₁} {p₂ : P n₂} →
          p₁ ≈ p₂ → ♭? (♯? {b₁} p₁) ≈ ♭? (♯? {b₂} p₂)
♭♯-cong b₁ b₂ {p₁} {p₂} rewrite ♭?♯? b₁ {p = p₁} | ♭?♯? b₂ {p = p₂} = id

fail-cong : fail ≈ fail
fail-cong = Equivalence.reflexive

empty-cong : empty ≈ empty
empty-cong = Equivalence.reflexive

sat-cong : {f₁ f₂ : Tok → Bool} → f₁ ≗ f₂ → sat f₁ ≈ sat f₂
sat-cong f₁≗f₂ = equivalence (helper f₁≗f₂) (helper (P.sym ∘ f₁≗f₂))
  where
  helper : {f₁ f₂ : Tok → Bool} → f₁ ≗ f₂ → sat f₁ ≤ sat f₂
  helper f₁≗f₂ (sat ok) = sat (P.subst T (f₁≗f₂ _) ok)

∣-cong : ∀ {n₁ n₂ n₃ n₄}
           {p₁ : P n₁} {p₂ : P n₂} {p₃ : P n₃} {p₄ : P n₄} →
         p₁ ≈′ p₃ → p₂ ≈′ p₄ → p₁ ∣ p₂ ≈′ p₃ ∣ p₄
∣-cong (refl ∷ rest₁) (refl ∷ rest₂) =
  refl ∷ λ t → ♯ ∣-cong (♭ (rest₁ t)) (♭ (rest₂ t))

·-cong : ∀ {n₁ n₂ n₃ n₄}
           {p₁ : ∞⟨ n₂ ⟩P n₁} {p₂ : ∞⟨ n₁ ⟩P n₂}
           {p₃ : ∞⟨ n₄ ⟩P n₃} {p₄ : ∞⟨ n₃ ⟩P n₄} →
         ♭? p₁ ≈ ♭? p₃ → ♭? p₂ ≈ ♭? p₄ → p₁ · p₂ ≈ p₃ · p₄
·-cong p₁≈p₃ p₂≈p₄ =
  Eq.Equivalence.from ≈⇔≤≥ ⟨$⟩
    Prod.zip helper helper
             (Eq.Equivalence.to ≈⇔≤≥ ⟨$⟩ p₁≈p₃)
             (Eq.Equivalence.to ≈⇔≤≥ ⟨$⟩ p₂≈p₄)
  where
  helper : ∀ {n₁ n₂ n₃ n₄}
             {p₁ : ∞⟨ n₂ ⟩P n₁} {p₂ : ∞⟨ n₁ ⟩P n₂}
             {p₃ : ∞⟨ n₄ ⟩P n₃} {p₄ : ∞⟨ n₃ ⟩P n₄} →
           ♭? p₁ ≤ ♭? p₃ → ♭? p₂ ≤ ♭? p₄ → p₁ · p₂ ≤ p₃ · p₄
  helper ₁≤₃ ₂≤₄ (∈p₁ · ∈p₂) = ₁≤₃ ∈p₁ · ₂≤₄ ∈p₂

⊙-cong : ∀ {n₁ n₂ n₃ n₄}
           {p₁ : P n₁} {p₂ : P n₂} {p₃ : P n₃} {p₄ : P n₄} →
         p₁ ≈ p₃ → p₂ ≈ p₄ → p₁ ⊙ p₂ ≈ p₃ ⊙ p₄
⊙-cong {n₁} {n₂} {n₃} {n₄} ₁≈₃ ₂≈₄ =
  ·-cong (♭♯-cong n₂ n₄ ₁≈₃) (♭♯-cong n₁ n₃ ₂≈₄)

nonempty-cong : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
                p₁ ≈′ p₂ → nonempty p₁ ≈′ nonempty p₂
nonempty-cong (_ ∷ rest) = refl ∷ rest

cast-cong : ∀ {n₁ n₂ n₁′ n₂′}
              {p₁ : P n₁} {p₂ : P n₂}
              {eq₁ : n₁ ≡ n₁′} {eq₂ : n₂ ≡ n₂′} →
            p₁ ≈′ p₂ → cast eq₁ p₁ ≈′ cast eq₂ p₂
cast-cong {eq₁ = refl} {refl} (init ∷ rest) = init ∷ rest

⋆-cong : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
         p₁ ≈ p₂ → p₁ ⋆ ≈ p₂ ⋆
⋆-cong p₁≈p₂ = Eq.Equivalence.from ≈⇔≤≥ ⟨$⟩
                 Prod.map helper helper
                   (Eq.Equivalence.to ≈⇔≤≥ ⟨$⟩ p₁≈p₂)
  where
  helper : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} →
           p₁ ≤ p₂ → p₁ ⋆ ≤ p₂ ⋆
  helper p₁≤p₂ (∣-left  empty)                 = ∣-left empty
  helper p₁≤p₂ (∣-right (nonempty ∈p₁ · ∈p₁⋆)) =
    ∣-right {p₁ = empty} (nonempty (p₁≤p₂ ∈p₁) · helper p₁≤p₂ ∈p₁⋆)

^-cong : ∀ {n₁ n₂ i₁ i₂} {p₁ : P n₁} {p₂ : P n₂} →
         p₁ ≈ p₂ → i₁ ≡ i₂ → p₁ ^ i₁ ≈ p₂ ^ i₂
^-cong {i₁ = i} p₁≈p₂ refl =
  Eq.Equivalence.from ≈⇔≤≥ ⟨$⟩
    Prod.map (helper i) (helper i)
             (Eq.Equivalence.to ≈⇔≤≥ ⟨$⟩ p₁≈p₂)
  where
  helper : ∀ {n₁ n₂} {p₁ : P n₁} {p₂ : P n₂} i →
           p₁ ≤ p₂ → p₁ ^ i ≤ p₂ ^ i
  helper           zero    p₁≤p₂ empty   = empty
  helper {n₁} {n₂} (suc i) p₁≤p₂ ∈p₁⊙p₁ⁱ
    with ⊙.sound ⟨ n₁ ^ i ⟩-nullable ∈p₁⊙p₁ⁱ
  ... | ∈p₁ ⊙′ ∈p₁ⁱ = ⊙.complete (p₁≤p₂ ∈p₁) (helper i p₁≤p₂ ∈p₁ⁱ)

------------------------------------------------------------------------
-- A variant of _≤_

infix 4 _≲_

-- If _∣_ is viewed as the join operation of a join-semilattice, then
-- the following definition of order is natural.

_≲_ : ∀ {n₁ n₂} → P n₁ → P n₂ → Set
p₁ ≲ p₂ = p₁ ∣ p₂ ≈ p₂

-- The order above coincides with _≤_.

≤⇔≲ : ∀ {n₁ n₂} (p₁ : P n₁) (p₂ : P n₂) → p₁ ≤ p₂ ⇔ p₁ ≲ p₂
≤⇔≲ {n₁} p₁ p₂ =
  equivalence
    (λ (p₁≤p₂ : p₁ ≤ p₂) {_} →
       equivalence (helper p₁≤p₂) (∣-right {n₁ = n₁}))
    (λ (p₁≲p₂ : p₁ ≲ p₂) s∈p₁ → Eq.Equivalence.to p₁≲p₂ ⟨$⟩ ∣-left s∈p₁)
  where
  helper : p₁ ≤ p₂ → p₁ ∣ p₂ ≤ p₂
  helper p₁≤p₂ (∣-left  s∈p₁) = p₁≤p₂ s∈p₁
  helper p₁≤p₂ (∣-right s∈p₂) = s∈p₂

------------------------------------------------------------------------
-- Recognisers form a *-continuous Kleene algebra

-- The definition of *-continuous Kleene algebras used here is the one
-- given by Kozen in "On Kleene Algebras and Closed Semirings", except
-- for the presence of the recogniser indices. Kozen used the order
-- _≲_ in his definition, but as shown above this order is equivalent
-- to _≤_.

-- Additive idempotent commutative monoid. (One of the identity lemmas
-- could be omitted.)

∣-commutative : ∀ {n₁ n₂} (p₁ : P n₁) (p₂ : P n₂) → p₁ ∣ p₂ ≈′ p₂ ∣ p₁
∣-commutative {n₁} {n₂} p₁ p₂ =
  BoolCS.+-comm n₁ n₂ ∷ λ t → ♯ ∣-commutative (D t p₁) (D t p₂)

fail-left-identity : ∀ {n} (p : P n) → fail ∣ p ≈′ p
fail-left-identity p = refl ∷ λ t → ♯ fail-left-identity (D t p)

fail-right-identity : ∀ {n} (p : P n) → p ∣ fail ≈′ p
fail-right-identity {n} p =
  proj₂ BoolCS.+-identity n ∷ λ t → ♯ fail-right-identity (D t p)

∣-associative : ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
                p₁ ∣ (p₂ ∣ p₃) ≈′ (p₁ ∣ p₂) ∣ p₃
∣-associative {n₁} {n₂} {n₃} p₁ p₂ p₃ =
  P.sym (BoolCS.+-assoc n₁ n₂ n₃) ∷ λ t →
    ♯ ∣-associative (D t p₁) (D t p₂) (D t p₃)

∣-idempotent : ∀ {n} (p : P n) → p ∣ p ≈′ p
∣-idempotent {n} p =
  BoolBA.∨-idempotent n ∷ λ t → ♯ ∣-idempotent (D t p)

-- Multiplicative monoid.

empty-left-identity : ∀ {n} (p : P n) → empty ⊙ p ≈ p
empty-left-identity {n} p =
  equivalence helper (λ s∈p → ⊙.complete empty s∈p)
  where
  helper : empty ⊙ p ≤ p
  helper ∈empty⊙p with ⊙.sound n ∈empty⊙p
  ... | empty ⊙′ s∈p = s∈p

empty-right-identity : ∀ {n} (p : P n) → p ⊙ empty ≈ p
empty-right-identity {n} p =
  equivalence
    helper
    (λ s∈p → cast∈ (proj₂ ListMonoid.identity _) refl
                   (⊙.complete s∈p empty))
  where
  helper : ∀ {s} → s ∈ p ⊙ empty → s ∈ p
  helper ∈p⊙empty with ⊙.sound true ∈p⊙empty
  helper ∈p⊙empty | ∈p ⊙′ empty =
    cast∈ (P.sym (proj₂ ListMonoid.identity _)) refl ∈p

·-associative : ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
                p₁ ⊙ (p₂ ⊙ p₃) ≈ (p₁ ⊙ p₂) ⊙ p₃
·-associative {n₁} {n₂} {n₃} p₁ p₂ p₃ = equivalence helper₁ helper₂
  where
  helper₁ : p₁ ⊙ (p₂ ⊙ p₃) ≤ (p₁ ⊙ p₂) ⊙ p₃
  helper₁ ∈⊙⊙ with ⊙.sound (n₂ ∧ n₃) ∈⊙⊙
  ... | _⊙′_ {s₁ = s₁} ∈p₁ ∈⊙ with ⊙.sound n₃ ∈⊙
  ...   | ∈p₂ ⊙′ ∈p₃ =
    cast∈ (ListMonoid.assoc s₁ _ _) refl $
      ⊙.complete (⊙.complete ∈p₁ ∈p₂) ∈p₃

  helper₂ : (p₁ ⊙ p₂) ⊙ p₃ ≤ p₁ ⊙ (p₂ ⊙ p₃)
  helper₂ ∈⊙⊙ with ⊙.sound n₃ ∈⊙⊙
  ... | ∈⊙ ⊙′ ∈p₃ with ⊙.sound n₂ ∈⊙
  ...   | _⊙′_ {s₁ = s₁} ∈p₁ ∈p₂ =
    cast∈ (P.sym $ ListMonoid.assoc s₁ _ _) refl $
      ⊙.complete ∈p₁ (⊙.complete ∈p₂ ∈p₃)

-- Distributivity.

left-distributive :
  ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
  p₁ ⊙ (p₂ ∣ p₃) ≈ p₁ ⊙ p₂ ∣ p₁ ⊙ p₃
left-distributive {n₁} {n₂} {n₃} p₁ p₂ p₃ = equivalence helper₁ helper₂
  where
  helper₁ : p₁ ⊙ (p₂ ∣ p₃) ≤ p₁ ⊙ p₂ ∣ p₁ ⊙ p₃
  helper₁ ∈⊙∣ with ⊙.sound (n₂ ∨ n₃) ∈⊙∣
  ... | ∈p₁ ⊙′ ∣-left  ∈p₂ = ∣-left $ ⊙.complete ∈p₁ ∈p₂
  ... | ∈p₁ ⊙′ ∣-right ∈p₃ = ∣-right {n₁ = n₁ ∧ n₂} $ ⊙.complete ∈p₁ ∈p₃

  helper₂ : p₁ ⊙ p₂ ∣ p₁ ⊙ p₃ ≤ p₁ ⊙ (p₂ ∣ p₃)
  helper₂ (∣-left ∈⊙) with ⊙.sound n₂ ∈⊙
  ... | ∈p₁ ⊙′ ∈p₂ = ⊙.complete ∈p₁ (∣-left ∈p₂)
  helper₂ (∣-right ∈⊙) with ⊙.sound n₃ ∈⊙
  ... | ∈p₁ ⊙′ ∈p₃ = ⊙.complete ∈p₁ (∣-right {n₁ = n₂} ∈p₃)

right-distributive :
  ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
  (p₁ ∣ p₂) ⊙ p₃ ≈ p₁ ⊙ p₃ ∣ p₂ ⊙ p₃
right-distributive {n₁} {n₂} {n₃} p₁ p₂ p₃ = equivalence helper₁ helper₂
  where
  helper₁ : (p₁ ∣ p₂) ⊙ p₃ ≤ p₁ ⊙ p₃ ∣ p₂ ⊙ p₃
  helper₁ ∈∣⊙ with ⊙.sound n₃ ∈∣⊙
  ... | ∣-left  ∈p₁ ⊙′ ∈p₃ = ∣-left $ ⊙.complete ∈p₁ ∈p₃
  ... | ∣-right ∈p₂ ⊙′ ∈p₃ = ∣-right {n₁ = n₁ ∧ n₃} $ ⊙.complete ∈p₂ ∈p₃

  helper₂ : p₁ ⊙ p₃ ∣ p₂ ⊙ p₃ ≤ (p₁ ∣ p₂) ⊙ p₃
  helper₂ (∣-left ∈⊙) with ⊙.sound n₃ ∈⊙
  ... | ∈p₁ ⊙′ ∈p₃ = ⊙.complete (∣-left ∈p₁) ∈p₃
  helper₂ (∣-right ∈⊙) with ⊙.sound n₃ ∈⊙
  ... | ∈p₂ ⊙′ ∈p₃ = ⊙.complete (∣-right {n₁ = n₁} ∈p₂) ∈p₃

-- Zero.

left-zero : ∀ {n} (p : P n) → fail ⊙ p ≈ fail
left-zero {n} p = equivalence helper (λ ())
  where
  helper : fail ⊙ p ≤ fail
  helper ∈fail⊙ with ⊙.sound n ∈fail⊙
  ... | () ⊙′ _

right-zero : ∀ {n} (p : P n) → p ⊙ fail ≈ fail
right-zero {n} p = equivalence helper (λ ())
  where
  helper : p ⊙ fail ≤ fail
  helper ∈⊙fail with ⊙.sound false ∈⊙fail
  ... | _ ⊙′ ()

-- *-continuity.

*-continuity-upper-bound :
  ∀ {n₁ n₂ n₃} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) →
  ∀ i → p₁ ⊙ p₂ ^ i ⊙ p₃ ≤ p₁ ⊙ p₂ ⋆ ⊙ p₃
*-continuity-upper-bound {n₁} {n₂} {n₃} _ _ _ i ∈⊙ⁱ⊙
  with ⊙.sound n₃ ∈⊙ⁱ⊙
... | ∈⊙ⁱ ⊙′ ∈p₃ with ⊙.sound ⟨ n₂ ^ i ⟩-nullable ∈⊙ⁱ
...   | ∈p₁ ⊙′ ∈p₂ⁱ = ⊙.complete (⊙.complete ∈p₁ (^≤⋆ i ∈p₂ⁱ)) ∈p₃

*-continuity-least-upper-bound :
  ∀ {n₁ n₂ n₃ n} (p₁ : P n₁) (p₂ : P n₂) (p₃ : P n₃) (p : P n) →
  (∀ i → p₁ ⊙ p₂ ^ i ⊙ p₃ ≤ p) → p₁ ⊙ p₂ ⋆ ⊙ p₃ ≤ p
*-continuity-least-upper-bound {n₁} {n₂} {n₃} {n} p₁ p₂ p₃ p ub =
  helper ∘ _⟨$⟩_ (Eq.Equivalence.from $ ·-associative p₁ (p₂ ⋆) p₃)
  where
  helper : p₁ ⊙ (p₂ ⋆ ⊙ p₃) ≤ p
  helper ∈⊙⋆⊙ with ⊙.sound (true ∧ n₃) ∈⊙⋆⊙
  ... | _⊙′_ {s₁ = s₁} ∈p₁ ∈⋆⊙ with ⊙.sound n₃ ∈⋆⊙
  ...   | ∈p₂⋆ ⊙′ ∈p₃ with ⋆≤^ ∈p₂⋆
  ...     | (i , ∈p₂ⁱ) =
    cast∈ (ListMonoid.assoc s₁ _ _) refl $
      ub i $ ⊙.complete (⊙.complete ∈p₁ ∈p₂ⁱ) ∈p₃

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-
   FP Lunch, Nottingham
   July 27, 2007
   Conor McBride
-}

module Binary where

data Bit : Set where
  O : Bit
  I : Bit

infixl 80 _◃_

data Pos : Set where
  ◃I  : Pos
  _◃_ : Pos -> Bit -> Pos

bsuc : Pos -> Pos
bsuc ◃I      = ◃I ◃ O
bsuc (n ◃ O) = n ◃ I
bsuc (n ◃ I) = bsuc n ◃ O

data Peano : Pos -> Set where
  pI   : Peano ◃I
  psuc : {n : Pos} -> Peano n -> Peano (bsuc n)

pdouble : {n : Pos} -> Peano n -> Peano (n ◃ O)
pdouble pI       = psuc pI
pdouble (psuc p) = psuc (psuc (pdouble p))

peano : (n : Pos) -> Peano n
peano ◃I      = pI
peano (n ◃ O) = pdouble (peano n)
peano (n ◃ I) = psuc (pdouble (peano n))

-- Slow addition (yay!)
_+_ : Pos -> Pos -> Pos
_+_ n m = peano n ⊕ m
  where
    _⊕_ : {n : Pos} -> Peano n -> Pos -> Pos
    pI     ⊕ m = bsuc m
    psuc p ⊕ m = bsuc (p ⊕ m)

infixl 60 _+_
infix  40 _==_

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

test : (◃I ◃ I ◃ O ◃ O ◃ O) == (◃I ◃ I ◃ O ◃ I) + (◃I ◃ O ◃ I ◃ I)
test = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Chain
    {A : Set}(_==_ : A -> A -> Set)
    (refl : (x : A) -> x == x)
    (trans : (x y z : A) -> x == y -> y == z -> x == z)
  where

infix  2 chain>_
infixl 2 _===_by_
infix  1 _qed

private
  data _≃_ (x y : A) : Set where
    prf : x == y -> x ≃ y

chain>_ : (x : A) -> x ≃ x
chain> x = prf (refl x)

_===_by_ : {x y : A} -> x ≃ y -> (z : A) -> y == z -> x ≃ z
prf p === z by q = prf (trans _ _ _ p q)

_qed : {x y : A} -> x ≃ y -> x == y
prf p qed = p

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Languages.FILL.Syntax where

open import level
open import bool
open import nat
open import unit
open import empty
open import list
open import eq
open import sum

open import Utils.HaskellTypes
open import Utils.HaskellFunctions
open import Languages.FILL.TypeSyntax

True : Set
True = ⊤{lzero}

False : Set
False = ⊥{lzero}

Name : Set
Name = ℕ

name-in : ∀{A : Set} → (A → A → 𝔹) → A → 𝕃 A → Set
name-in eq x ctx with list-member eq x ctx
name-in _ x ctx | tt = True
name-in _ x ctx | ff = False

-- Bound Variable Labels:
data VLabel : Set where
  LPV : VLabel         -- Let-Bound Left Pattern Variable
  RPV : VLabel         -- Let-Bound Right Pattern Variable
  BV  : VLabel         -- λ-Bound Variable

_vl-eq_ : VLabel → VLabel → 𝔹
LPV vl-eq LPV = tt
RPV vl-eq RPV = tt
BV vl-eq BV = tt
_ vl-eq _ = ff

data Pattern : Set where
  PTriv : Pattern
  PTensor : String → String → Pattern
  PPar : String → String → Pattern

data Term : Set where
  Triv : Term
  Void : Term
  FVar : String → Term
  BVar : Name → String → VLabel → Term
  Let : Term → Type → Pattern → Term → Term
  Lam : String → Type → Term → Term
  App : Term → Term → Term
  Tensor : Term → Term → Term
  Par : Term → Term → Term

open-t : Name → VLabel → Term → Term → Term
open-t x l u (BVar y ys l') with x =ℕ y | l vl-eq l'
... | tt | tt = u
... | _  | _  = BVar y ys l'
open-t x BV u (Let t₁ y z t₂) = Let (open-t x BV u t₁) y z (open-t x BV u t₂)
open-t x l u (Let t₁ a p t₂) = Let (open-t (suc x) l u t₁) a p (open-t (suc x) l u t₂)
open-t x BV u (Lam ys a t) = Lam ys a (open-t (suc x) BV u t)
open-t x l u (Lam ys a t) = Lam ys a (open-t x l u t)
open-t x l u (App t₁ t₂) = App (open-t x l u t₁) (open-t x l u t₂)
open-t x l u (Tensor t₁ t₂) = Tensor (open-t x l u t₁) (open-t x l u t₂)
open-t x l u (Par t₁ t₂) = Par (open-t x l u t₁) (open-t x l u t₂)
open-t _ _ _ t = t

close-t : Name → String → VLabel → String → Term → Term
close-t x xs l y (FVar z) with y str-eq z
... | tt = BVar x xs l
... | ff = FVar z
close-t x xs l y (Let t₁ ty p t₂) = Let (close-t x xs l y t₁) ty p (close-t x xs l y t₂)
close-t x xs l y (Lam ys a t) = Lam ys a (close-t x xs l y t)
close-t x xs l y (App t₁ t₂) = App (close-t x xs l y t₁) (close-t x xs l y t₂)
close-t x xs l y (Tensor t₁ t₂) = Tensor (close-t x xs l y t₁) (close-t x xs l y t₂)
close-t x xs l y (Par t₁ t₂) = Par (close-t x xs l y t₁) (close-t x xs l y t₂)
close-t _ _ _ _ t = t

data LC : Term → Set where
  Triv : LC Triv
  Void : LC Void
  FVar : ∀{x : String} → LC (FVar x)
  Lam : ∀{ns : 𝕃 String}{t : Term}{a : Type}{y : String}
      → LC t
      → (∀{x : String}
           → (name-in _str-eq_ x ns → False)
           → LC (open-t 0 BV (FVar x) t))
      → LC (Lam y a t)
  LetTriv : ∀{t₁ : Term}{a : Type}{t₂ : Term}
      → LC t₁
      → LC t₂
      → LC (Let t₁ a PTriv t₂)
  LetTensor : ∀{ns : 𝕃 String}{t₁ : Term}{a : Type}{t₂ : Term}{s₁ s₂ : String}
      → LC t₁
      → LC t₂
      → (∀{x y : String}
           → (name-in _str-eq_ x ns → False)
           → (name-in _str-eq_ y ns → False)
           → LC (open-t 0 LPV (FVar x) (open-t 0 RPV (FVar y) t₂)))
      → LC (Let t₁ a (PTensor s₁ s₂) t₂)
  LetPar : ∀{ns : 𝕃 String}{t₁ : Term}{a : Type}{t₂ : Term}{s₁ s₂ : String}
      → LC t₁
      → LC t₂
      → (∀{x y : String}
           → (name-in _str-eq_ x ns → False)
           → (name-in _str-eq_ y ns → False)
           → LC (open-t 0 LPV (FVar x) (open-t 0 RPV (FVar y) t₂)))
      → LC (Let t₁ a (PPar s₁ s₂) t₂)
  App : ∀{t₁ t₂ : Term}
      → LC t₁
      → LC t₂
      → LC (App t₁ t₂)
  Tensor : ∀{t₁ t₂ : Term}
      → LC t₁
      → LC t₂
      → LC (Tensor t₁ t₂)
  Par : ∀{t₁ t₂ : Term}
      → LC t₁
      → LC t₂
      → LC (Par t₁ t₂)

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions {{eqrel : EqRelSet}} where

open import Definition.LogicalRelation.Substitution.Introductions.Application public
open import Definition.LogicalRelation.Substitution.Introductions.Lambda public
open import Definition.LogicalRelation.Substitution.Introductions.Nat public
open import Definition.LogicalRelation.Substitution.Introductions.Natrec public
open import Definition.LogicalRelation.Substitution.Introductions.Pi public
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst public
open import Definition.LogicalRelation.Substitution.Introductions.Universe public

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
open import Agda.Builtin.Equality

cong : ∀{a b} {A : Set a} {B : Set b} (f : A → B) {x y : A} (eq : x ≡ y) → f x ≡ f y
cong f refl = refl

record Category : Set₂ where
  field
    Ob  : Set₁
    _⇒_ : Ob → Ob → Set
    _∘_ : ∀ {O P Q} → P ⇒ Q → O ⇒ P → O ⇒ Q

  -- Moving this out of the record fixes the problem.
  idem : {X : Ob} → X ⇒ X → Set₁
  idem {X} f = f ∘ f ≡ f → Set

Sets : Category
Sets = record
    { Ob = Set
    ; _⇒_ = {!!}
    ; _∘_ = λ f g x → f (g x)
    }
open Category Sets

postulate
  Y : Ob
  f : Y ⇒ Y

idem-f : idem {X = _} f  -- Solving the _ fixes the problem
idem-f ff≡f
  with ffx≡fx ← cong {!!} ff≡f
  = Y


text:
-- Andreas, 2012-01-11, bug reported by Adam Gundry
module Issue551 where

data Bool : Set where
  true false : Bool

data _≡_ {A : Set}(a : A) : A → Set where
  refl : a ≡ a

cong : {A B : Set}(f : A → B){a a' : A} → a ≡ a' → f a ≡ f a'
cong f refl = refl

implicit : {A : Set}{{a : A}} -> A
implicit {{a}} = a

record PackBool : Set where
  constructor pack
  field unpack : Bool
open PackBool

data IrrBool : Set where
  irr : .(b : PackBool) -> IrrBool

p : irr (pack true) ≡ irr (pack false)
p = refl

-- The following should fail:

unirr : IrrBool -> PackBool
unirr (irr x) = implicit
-- unirr (irr x) = x gives an error message (as well it should)
-- but using instance arguments circumvents the check.

q : true ≡ false
q = cong (λ x → unpack (unirr x)) p

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Issue936 where

-- The highlighting generated for this file should not contain
-- any references to Agda.Primitive.


text:
-- Andreas, 2017-01-18, issue #57
-- reported by Nisse 2008-03-26

data Unit : Set where
  unit : Unit

foo : Unit → Unit
foo m with m
foo _ | x@unit with x
foo _ | x@unit | _ = x

test : Unit → Unit
test m with m
test _ | x@unit with x
... | _ = x


text:
------------------------------------------------------------------------
-- Rational numbers
------------------------------------------------------------------------

module Data.Rational where

open import Data.Bool.Properties
open import Data.Function
open import Data.Integer hiding (suc) renaming (_*_ to _ℤ*_)
open import Data.Integer.Divisibility as ℤDiv using (Coprime)
import Data.Integer.Properties as ℤ
open import Data.Nat.Divisibility as ℕDiv using (_∣_)
import Data.Nat.Coprimality as C
open import Data.Nat as ℕ renaming (_*_ to _ℕ*_)
open import Relation.Nullary.Decidable
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
open ≡-Reasoning

------------------------------------------------------------------------
-- The definition

-- Rational numbers in reduced form.

record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ
    isCoprime     : True (C.coprime? ∣ numerator ∣ (suc denominator-1))

  denominator : ℤ
  denominator = + suc denominator-1

  coprime : Coprime numerator denominator
  coprime = witnessToTruth isCoprime

-- Constructs rational numbers. The arguments have to be in reduced
-- form.

infixl 7 _÷_

_÷_ : (numerator : ℤ) (denominator : ℕ)
      {coprime : True (C.coprime? ∣ numerator ∣ denominator)}
      {≢0 : False (ℕ._≟_ denominator 0)} →
      ℚ
(n ÷ zero) {≢0 = ()}
(n ÷ suc d) {c} =
  record { numerator = n; denominator-1 = d; isCoprime = c }

private

  -- Note that the implicit arguments do not need to be given for
  -- concrete inputs:

  0/1 : ℚ
  0/1 = + 0 ÷ 1

  -½ : ℚ
  -½ = - + 1 ÷ 2

------------------------------------------------------------------------
-- Equality

-- Equality of rational numbers.

infix 4 _≃_

_≃_ : Rel ℚ
p ≃ q = P.numerator ℤ* Q.denominator ≡
        Q.numerator ℤ* P.denominator
  where module P = ℚ p; module Q = ℚ q

-- _≃_ coincides with propositional equality.

≡⇒≃ : _≡_ ⇒ _≃_
≡⇒≃ refl = refl

≃⇒≡ : _≃_ ⇒ _≡_
≃⇒≡ {p} {q} = helper P.numerator P.denominator-1 P.isCoprime
                     Q.numerator Q.denominator-1 Q.isCoprime
  where
  module P = ℚ p; module Q = ℚ q

  helper : ∀ n₁ d₁ c₁ n₂ d₂ c₂ →
           n₁ ℤ* + suc d₂ ≡ n₂ ℤ* + suc d₁ →
           (n₁ ÷ suc d₁) {c₁} ≡ (n₂ ÷ suc d₂) {c₂}
  helper n₁ d₁ c₁ n₂ d₂ c₂ eq
    with Poset.antisym ℕDiv.poset 1+d₁∣1+d₂ 1+d₂∣1+d₁
    where
    1+d₁∣1+d₂ : suc d₁ ∣ suc d₂
    1+d₁∣1+d₂ = ℤDiv.coprime-divisor (+ suc d₁) n₁ (+ suc d₂)
                  (C.sym $ witnessToTruth c₁) $
                  ℕDiv.divides ∣ n₂ ∣ (begin
                    ∣ n₁ ℤ* + suc d₂ ∣  ≡⟨ cong ∣_∣ eq ⟩
                    ∣ n₂ ℤ* + suc d₁ ∣  ≡⟨ ℤ.abs-*-commute n₂ (+ suc d₁) ⟩
                    ∣ n₂ ∣ ℕ* suc d₁    ∎)

    1+d₂∣1+d₁ : suc d₂ ∣ suc d₁
    1+d₂∣1+d₁ = ℤDiv.coprime-divisor (+ suc d₂) n₂ (+ suc d₁)
                  (C.sym $ witnessToTruth c₂) $
                  ℕDiv.divides ∣ n₁ ∣ (begin
                    ∣ n₂ ℤ* + suc d₁ ∣  ≡⟨ cong ∣_∣ (PropEq.sym eq) ⟩
                    ∣ n₁ ℤ* + suc d₂ ∣  ≡⟨ ℤ.abs-*-commute n₁ (+ suc d₂) ⟩
                    ∣ n₁ ∣ ℕ* suc d₂    ∎)

  helper n₁ d c₁ n₂ .d c₂ eq | refl with ℤ.cancel-*-right
                                           n₁ n₂ (+ suc d) (λ ()) eq
  helper n  d c₁ .n .d c₂ eq | refl | refl with proof-irrelevance c₁ c₂
  helper n  d c  .n .d .c eq | refl | refl | refl = refl

max_issues_repo_name: larrytheliquid/Lemmachine


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

open import lib.Basics
open import lib.types.Group
open import lib.types.Unit
open import lib.groups.SubgroupProp
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism
open import lib.groups.Lift

module lib.groups.Unit where

Unit-group-structure : GroupStructure Unit
Unit-group-structure = record
  { ident = unit
  ; inv = λ _ → unit
  ; comp = λ _ _ → unit
  ; unit-l = λ _ → idp
  ; assoc = λ _ _ _ → idp
  ; inv-l = λ _ → idp
  }

Unit-group : Group lzero
Unit-group = group _ Unit-is-set Unit-group-structure

0ᴳ = Unit-group

abstract
  Unit-group-is-trivial : is-trivialᴳ Unit-group
  Unit-group-is-trivial = λ _ → idp

  iso-Unit-is-trivial : ∀ {i} {G : Group i} → G ≃ᴳ Unit-group → is-trivialᴳ G
  iso-Unit-is-trivial G-iso-0 = iso-preserves'-trivial G-iso-0 Unit-group-is-trivial

0ᴳ-is-trivial = Unit-group-is-trivial
iso-0ᴳ-is-trivial = iso-Unit-is-trivial

trivial-iso-Unit : ∀ {i} {G : Group i} → is-trivialᴳ G → G ≃ᴳ Unit-group
trivial-iso-Unit {G = G} G-triv = group-hom (λ _ → tt) (λ _ _ → idp) ,
  is-eq _ (λ _ → Group.ident G) (λ _ → idp) (λ _ → ! (G-triv _))

trivial-iso-0ᴳ = trivial-iso-Unit

{- the following should be replaced by [is-trivial] completely -}

abstract
  contr-iso-Unit : ∀ {i} (G : Group i) → is-contr (Group.El G) → G ≃ᴳ Unit-group
  contr-iso-Unit G pA = ≃-to-≃ᴳ (contr-equiv-Unit pA) (λ _ _ → idp)
contr-iso-0ᴳ = contr-iso-Unit

Unit-group-is-abelian : is-abelian 0ᴳ
Unit-group-is-abelian _ _ = idp

0ᴳ-is-abelian = Unit-group-is-abelian

Unit-abgroup : AbGroup₀
Unit-abgroup = Unit-group , Unit-group-is-abelian

0ᴳ-abgroup = Unit-abgroup

abstract
  hom₁-Unit-is-trivial : ∀ {i} (G : AbGroup i) → is-trivialᴳ (hom-group Unit-group G)
  hom₁-Unit-is-trivial G φ = group-hom= $ λ= λ _ → GroupHom.pres-ident φ

hom₁-0ᴳ-is-trivial = hom₁-Unit-is-trivial

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

plus : Nat → Nat → Nat
plus zero b = b
plus (suc a) b = suc (plus a b)

infixl 6 _+_
_+_ = plus

{-# DISPLAY suc n = 1 + n #-}
{-# DISPLAY plus a b = a + b #-}

postulate
  T : {A : Set} → A → Set

test₁ : ∀ a b → T (plus (suc a) b)
test₁ a b = {!!}

data Vec (A : Set) : Nat → Set where
  []  : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

data List A : Set where
  []  : List A
  _∷_ : A → List A → List A

infixr 4 _∷_

[_] : ∀ {A} → A → Vec A (suc zero)
[ x ] = x ∷  []

{-# DISPLAY Vec._∷_ x Vec.[] = [ x ] #-}

test₂ : (n : Nat) → T (n Vec.∷ [])
test₂ n = {!!}

append : ∀ {A : Set} {n m} → Vec A n → Vec A m → Vec A (n + m)
append []       ys = ys
append (x ∷ xs) ys = x ∷ append xs ys

infixr 4 _++_
_++_ = append

{-# DISPLAY append xs ys = xs ++ ys #-}
{-# DISPLAY append xs (y Vec.∷ ys) = xs ++ [ y ] ++ ys #-}

test₃ : ∀ {n} (xs ys : Vec Nat n) → T (append xs (n ∷ ys))
test₃ {n} xs ys = {!!}


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Reducibility {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped hiding (_∷_)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties

open import Tools.Nat
open import Tools.Product

private
  variable
    n : Nat
    Γ : Con Term n

-- Valid types are reducible.
reducibleᵛ : ∀ {A l}
             ([Γ] : ⊩ᵛ Γ)
           → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
           → Γ ⊩⟨ l ⟩ A
reducibleᵛ [Γ] [A] =
  let ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevance′ (subst-id _) (proj₁ ([A] ⊢Γ [id]))

-- Valid type equality is reducible.
reducibleEqᵛ : ∀ {A B l}
               ([Γ] : ⊩ᵛ Γ)
               ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
             → Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A]
             → Γ ⊩⟨ l ⟩ A ≡ B / reducibleᵛ [Γ] [A]
reducibleEqᵛ {A = A} [Γ] [A] [A≡B] =
  let [σA] = reducibleᵛ {A = A} [Γ] [A]
      ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevanceEq″ (subst-id _) (subst-id _)
                      (proj₁ ([A] ⊢Γ [id])) [σA] ([A≡B] ⊢Γ [id])

-- Valid terms are reducible.
reducibleTermᵛ : ∀ {t A l}
                 ([Γ] : ⊩ᵛ Γ)
                 ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
               → Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A]
               → Γ ⊩⟨ l ⟩ t ∷ A / reducibleᵛ [Γ] [A]
reducibleTermᵛ {A = A} [Γ] [A] [t] =
  let [σA] = reducibleᵛ {A = A} [Γ] [A]
      ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevanceTerm″ (subst-id _) (subst-id _)
                        (proj₁ ([A] ⊢Γ [id])) [σA] (proj₁ ([t] ⊢Γ [id]))

-- Valid term equality is reducible.
reducibleEqTermᵛ : ∀ {t u A l}
                   ([Γ] : ⊩ᵛ Γ)
                   ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
                 → Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A]
                 → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / reducibleᵛ [Γ] [A]
reducibleEqTermᵛ {A = A} [Γ] [A] [t≡u] =
  let [σA] = reducibleᵛ {A = A} [Γ] [A]
      ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevanceEqTerm″ (subst-id _) (subst-id _) (subst-id _)
                          (proj₁ ([A] ⊢Γ [id])) [σA] ([t≡u] ⊢Γ [id])

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.Properties.Comma where

open import Level
open import Data.Product using (Σ; _,_; proj₁; proj₂; zip; map; swap; <_,_>; -,_)

open import Categories.Category
open import Categories.Category.Instance.One
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Construction.Constant using (const; constNat)
open import Categories.NaturalTransformation using (module NaturalTransformation)
open import Categories.Category.Construction.Comma
open import Categories.Category.Product renaming (Product to _×_)
open import Categories.Category.Construction.Functors renaming (Functors to [_⇒_])
open import Categories.NaturalTransformation renaming (id to idN)

import Categories.Category.Slice as Sl
import Categories.Morphism.Reasoning as Reas

private
  variable
    o ℓ e o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃ : Level
    C D E : Category o ℓ e

-- There's a projection functor down onto the A and B Categories
module _ {A : Category o₁ ℓ₁ e₁}  {B : Category o₂ ℓ₂ e₂} {C : Category o₃ ℓ₃ e₃} where
  open CommaObj
  open Comma⇒
  private
    module A = Category A
    module EA = A.Equiv
    module B = Category B
    module EB = B.Equiv
    module C = Category C

  module _ (S : Functor B C) (T : Functor A C) where
    private
      module S = Functor S
      module T = Functor T

    S↓T⇒A×B : Functor (S ↓ T) (A × B)
    S↓T⇒A×B = record
      { F₀           = < β , α >
      ; F₁           = < h , g >
      ; identity     = EA.refl , EB.refl
      ; homomorphism = EA.refl , EB.refl
      ; F-resp-≈     = swap
      }

    induced-nat : NaturalTransformation (S ∘F Dom S T) (T ∘F Cod S T)
    induced-nat = record
      { η           = f
      ; commute     = λ i → C.Equiv.sym (commute i)
      ; sym-commute = commute
      }

    module _ (S′ : Functor D B) (T′ : Functor E A) where
      private
        module S′ = Functor S′
        module T′ = Functor T′

      compose-F : Functor (S ∘F S′ ↓ T ∘F T′) (S ↓ T)
      compose-F = record
        { F₀           = λ X → record
          { f = f X
          }
        ; F₁           = λ i → record
          { g       = S′.F₁ (g i)
          ; h       = T′.F₁ (h i)
          ; commute = commute i
          }
        ; identity     = S′.identity , T′.identity
        ; homomorphism = S′.homomorphism , T′.homomorphism
        ; F-resp-≈     = map S′.F-resp-≈ T′.F-resp-≈
        }

    module _ (S′ : Functor D B) where
      private
        module S′ = Functor S′

      compose-Fˡ : Functor (S ∘F S′ ↓ T) (S ↓ T)
      compose-Fˡ = record
        { F₀           = λ X → record
          { f = f X
          }
        ; F₁           = λ i → record
          { g       = S′.F₁ (g i)
          ; h       = h i
          ; commute = commute i
          }
        ; identity     = S′.identity , A.Equiv.refl
        ; homomorphism = S′.homomorphism , A.Equiv.refl
        ; F-resp-≈     = map S′.F-resp-≈ λ eq → eq
        }

    module _ (T′ : Functor E A) where
      private
        module T′ = Functor T′

      compose-Fʳ : Functor (S ↓ T ∘F T′) (S ↓ T)
      compose-Fʳ = record
        { F₀           = λ X → record
          { f = f X
          }
        ; F₁           = λ i → record
          { g       = g i
          ; h       = T′.F₁ (h i)
          ; commute = commute i
          }
        ; identity     = B.Equiv.refl , T′.identity
        ; homomorphism = B.Equiv.refl , T′.homomorphism
        ; F-resp-≈     = map (λ eq → eq) T′.F-resp-≈
        }

  module _ {S S′ : Functor B C} {T T′ : Functor A C} (γ : NaturalTransformation S′ S) (δ : NaturalTransformation T T′) where
    private
      module S′ = Functor S′
      module T′ = Functor T′
      module γ  = NaturalTransformation γ
      module δ  = NaturalTransformation δ
      module S = Functor S
      module T = Functor T
      open C
      open HomReasoning
      open Reas C

    -- functors between Comma categories along natural transformations
    along-nat : Functor (S ↓ T) (S′ ↓ T′)
    along-nat = record
      { F₀           = λ X → record
        { f = δ.η (β X) ∘ f X ∘ γ.η (α X)
        }
      ; F₁           = λ {X Y} i → record
        { g       = g i
        ; h       = h i
        ; commute = begin
          T′.F₁ (h i) ∘ δ.η (β X) ∘ f X ∘ γ.η (α X)   ≈⟨ sym-assoc ⟩
          (T′.F₁ (h i) ∘ δ.η (β X)) ∘ f X ∘ γ.η (α X) ≈˘⟨ center⁻¹ (δ.commute (h i)) refl ⟩
          δ.η (β Y) ∘ (T.F₁ (h i) ∘ f X) ∘ γ.η (α X)  ≈⟨ refl⟩∘⟨ pushˡ (commute i) ⟩
          δ.η (β Y) ∘ f Y ∘ S.F₁ (g i) ∘ γ.η (α X)    ≈˘⟨ pull-last (γ.commute (g i)) ⟩
          (δ.η (β Y) ∘ f Y ∘ γ.η (α Y)) ∘ S′.F₁ (g i) ∎
        }
      ; identity     = B.Equiv.refl , A.Equiv.refl
      ; homomorphism = B.Equiv.refl , A.Equiv.refl
      ; F-resp-≈     = λ eq → eq
      }

  along-natʳ : ∀ {T T′ : Functor A C} (S : Functor B C) (δ : NaturalTransformation T T′) → Functor (S ↓ T) (S ↓ T′)
  along-natʳ S = along-nat idN

  along-natˡ : ∀ {S S′ : Functor B C} (γ : NaturalTransformation S′ S) (T : Functor A C) → Functor (S ↓ T) (S′ ↓ T)
  along-natˡ γ T = along-nat γ idN

-- There's an induced functor from Functors category to Functors over Comma categories
module _ {A : Category o₁ ℓ₁ e₁} {B : Category o₂ ℓ₂ e₂} {C : Category o₃ ℓ₃ e₃} where
  open CommaObj
  open Comma⇒
  open Category C
  open Functor
  open HomReasoning
  open Reas C

  induced : {s₁ d₁ : Functor A C} {s₂ d₂ : Functor B C} →
            ((Category.op [ A ⇒ C ] × [ B ⇒ C ]) [ (s₁ , s₂) , (d₁ , d₂) ]) → Functor (s₁ ↓ s₂) (d₁ ↓ d₂)
  induced {s₁ = s₁} {d₁ = d₁} {s₂} {d₂} (m₁ , m₂) = record
    { F₀ = λ o → record
      { α = α o
      ; β = β o
      ; f = m₂.η (β o) ∘ f o ∘ m₁.η (α o)
      }
    ; F₁ = λ {o₁} {o₂} a → record
      { g = g a
      ; h = h a
      ; commute = begin
        F₁ d₂ (h a) ∘ m₂.η (β o₁) ∘ f o₁ ∘ m₁.η (α o₁)   ≈˘⟨ pushˡ (m₂.commute (h a)) ⟩
        (m₂.η (β o₂) ∘ F₁ s₂ (h a)) ∘ f o₁ ∘ m₁.η (α o₁) ≈⟨ pullˡ (pullʳ (commute a)) ⟩
        (m₂.η (β o₂) ∘ f o₂ ∘ F₁ s₁ (g a)) ∘ m₁.η (α o₁) ≈˘⟨ extendˡ (extendˡ (m₁.commute (g a))) ⟩
        (m₂.η (β o₂) ∘ f o₂ ∘ m₁.η (α o₂)) ∘ F₁ d₁ (g a) ∎
      }
    ; identity = A.Equiv.refl , B.Equiv.refl
    ; homomorphism = A.Equiv.refl , B.Equiv.refl
    ; F-resp-≈ = λ f≈g → f≈g
    }
    where
    module A = Category A
    module B = Category B
    module m₁ = NaturalTransformation m₁
    module m₂ = NaturalTransformation m₂

module _ (F : Functor C D) where
  private
    module D = Category D

  along-natˡ′ : ∀ {A B} (f : A D.⇒ B) → Functor (B ↙ F) (A ↙ F)
  along-natˡ′ f = along-natˡ (constNat f) F

  along-natʳ′ : ∀ {A B} (f : A D.⇒ B) → Functor (F ↘ A) (F ↘ B)
  along-natʳ′ f = along-natʳ F (constNat f)

module _ {C : Category o ℓ e} where
  open Category C
  open Sl C
  open SliceObj
  open Slice⇒
  open HomReasoning
  open CommaObj
  open Comma⇒
  open Reas C

  slice⇒comma : ∀ X → Functor (Slice X) (idF {C = C} ↓ const {C = One {o} {ℓ} {e}} X)
  slice⇒comma X = record
    { F₀           = λ X → record { f = arr X }
    ; F₁           = λ f → record { commute = identityˡ ○ ⟺ (△ f) }
    ; identity     = refl , _
    ; homomorphism = refl , _
    ; F-resp-≈     = λ eq → eq , _
    }

  comma⇒slice : ∀ X → Functor (idF {C = C} ↓ const {C = One {o} {ℓ} {e}} X) (Slice X)
  comma⇒slice X = record
    { F₀           = λ X → Sl.sliceobj (f X)
    ; F₁           = λ g → Sl.slicearr (⟺ (commute g) ○ identityˡ)
    ; identity     = refl
    ; homomorphism = refl
    ; F-resp-≈     = proj₁
    }

  comma-slice-equiv : ∀ X → StrongEquivalence (Slice X) (idF {C = C} ↓ const {C = One {o} {ℓ} {e}} X)
  comma-slice-equiv X = record
    { F            = slice⇒comma X
    ; G            = comma⇒slice X
    ; weak-inverse = record
      { F∘G≈id = record
        { F⇒G = record
          { η           = λ _ → record { commute = id-comm-sym }
          ; commute     = λ _ → id-comm-sym , _
          ; sym-commute = λ _ → id-comm , _
          }
        ; F⇐G = record
          { η           = λ _ → record { commute = id-comm-sym }
          ; commute     = λ _ → id-comm-sym , _
          ; sym-commute = λ _ → id-comm , _
          }
        ; iso = λ Y → record
          { isoˡ = identityˡ , _
          ; isoʳ = identityˡ , _
          }
        }
      ; G∘F≈id = record
        { F⇒G = record
          { η           = λ _ → Sl.slicearr identityʳ
          ; commute     = λ _ → id-comm-sym
          ; sym-commute = λ _ → id-comm
          }
        ; F⇐G = record
          { η           = λ _ → Sl.slicearr identityʳ
          ; commute     = λ _ → id-comm-sym
          ; sym-commute = λ _ → id-comm
          }
        ; iso = λ _ → record
          { isoˡ = identityˡ
          ; isoʳ = identityˡ
          }
        }
      }
    }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module FlatUnderscore where

postulate
  A : Set
  f : (@♭ X : A → Set) → ∀ a → X a
  @♭ B : A → Set

-- The undescore should be solved to B.
g : ∀ a → B a
g = f _


text:
{-# OPTIONS --safe --no-qualified-instances #-}
module CF.Syntax where

open import Level

open import Data.Integer
open import Data.Bool
open import Data.String
open import Data.Product
open import Data.List hiding (null)
open import Data.List.Relation.Unary.All

open import Relation.Unary hiding (_⊢_)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Binary.Structures using (IsPreorder)
open import Relation.Binary.PropositionalEquality using (isEquivalence; refl)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad.Possibly
open import Relation.Ternary.Monad.Weakening
open import Relation.Ternary.Data.Bigstar hiding ([_])

open import CF.Types
open import CF.Contexts.Lexical

open import Relation.Ternary.Construct.Product using (fst; snd)

open import Relation.Ternary.Data.Allstar Ty

data BinOp : Ty → Ty → Ty → Set where
  add sub mul div xor : BinOp int int int
  eq ne lt ge gt le   : BinOp int int bool

data Exp : Ty → Pred Ctx 0ℓ where
  unit       : ε[ Exp void ]
  num        : ℤ → ε[ Exp int ]
  bool       : Bool → ε[ Exp bool ]
  ifthenelse : ∀[ Exp bool ✴ Exp a ✴ Exp a ⇒ Exp a ]
  var'       : ∀[ Var a ⇒ Exp a ]
  bop        : BinOp a b c → ∀[ Exp a ✴ Exp b ⇒ Exp c ]

pattern var  = var' vars

module Statements (Block : Ty → Pred Ctx 0ℓ) where

  data Statement (r : Ty) : Pred Ctx 0ℓ where
    asgn          : ∀[ Var a ✴ Exp a ⇒ Statement r ]
    run           : ∀[ Exp a ⇒ Statement r ]
    ifthenelse    : ∀[ Exp bool ✴ Statement r ✴ Statement r ⇒ Statement r ]
    while         : ∀[ Exp bool ✴ Statement r ⇒ Statement r ]
    block         : ∀[ Block r ⇒ Statement r ]

mutual
  Stmt = Statements.Statement Block

  data Block (r : Ty) : Pred Ctx 0ℓ where
    local : ∀[ Exp a ✴ [ a ] ⊢ (Block r) ⇒ Block r ]
    cons  : ∀[ Stmt r ✴ Block r ⇒ Block r ]
    emp   : ε[ Block r ]

-- make constructors visible
open Statements Block public

infixr 5 _⍮⟨_⟩_
pattern _⍮⟨_⟩_ s σ b = cons (s ∙⟨ σ ⟩ b)
pattern _≔⟨_⟩_ e σ b = local (e ∙⟨ σ ⟩ b)


text:
-- Andreas, 2019-11-06, issue #4173, reported and testcase by nad.
-- Allow pattern matching on erased arguments in erased context.

-- {-# OPTIONS -v tc.cover.split:60 #-}

open import Agda.Builtin.Bool

@0 F : @0 Bool → Set₁
F true  = Set
F false = Set

-- Should succeed.

@0 G : @0 Bool → Set₁
G x = {! x !}  -- splitting on x should also succeed


text:
module Class.Monad where

open import Class.Functor
open import Data.Unit.Polymorphic
open import Category.Monad renaming (RawMonad to Monad) public

open Monad {{...}} using (return; _>>=_; _=<<_; _>>_) public

module _ {a} {M : Set a → Set a} {{m : Monad M}} where

  instance
    _ = Monad.rawIApplicative m
    monadFunctor = Monad.rawFunctor m

  void : ∀ {A} → M A → M ⊤
  void x = x >> return tt

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

open import Agda.Primitive
open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules

{- Categorical structure of the type theory for globular sets -}
module GSeTT.CwF-structure where

  {- cut-admissibility : action of substitutions preserves derivability -}
  []T : ∀ {Γ A Δ γ} → Γ ⊢T A → Δ ⊢S γ > Γ → Δ ⊢T (A [ γ ]Pre-Ty)
  []t : ∀ {Γ A t Δ γ} → Γ ⊢t t # A → Δ ⊢S γ > Γ → Δ ⊢t (t [ γ ]Pre-Tm) # (A [ γ ]Pre-Ty)

  []T (ob Γ⊢) Δ⊢γ:Γ = ob (Δ⊢γ:Γ→Δ⊢ Δ⊢γ:Γ)
  []T (ar Γ⊢t:A Γ⊢u:A) Δ⊢γ:Γ = ar ([]t Γ⊢t:A Δ⊢γ:Γ) ([]t Γ⊢u:A Δ⊢γ:Γ)
  []t {Γ = (Γ :: _)} {t = Var x} (var Γ+⊢@(cc Γ⊢ _ idp) (inl x∈Γ)) Δ⊢γ+:Γ+@(sc Δ⊢γ:Γ _ _ idp) with (eqdecℕ x (length Γ))
  ...                                                                                | inl idp = ⊥-elim (lΓ∉Γ Γ⊢ x∈Γ)
  ...                                                                                | inr _ = trT (wk[]T (Γ⊢t:A→Γ⊢A (var Γ⊢ x∈Γ)) Δ⊢γ+:Γ+ ^) ([]t (var Γ⊢ x∈Γ) Δ⊢γ:Γ)
  []t {Γ = (Γ :: _)} {t = Var x} (var Γ+⊢@(cc Γ⊢ Γ⊢A idp) (inr (idp , idp))) Δ⊢γ+:Γ+@(sc Δ⊢γ:Γ x₁ Δ⊢t:A[γ] idp) with (eqdecℕ x (length Γ))
  ...                                                                                | inl _ = trT (wk[]T Γ⊢A Δ⊢γ+:Γ+ ^) Δ⊢t:A[γ]
  ...                                                                                | inr x≠x = ⊥-elim (x≠x idp)

  {- action of identity on types and terms is trivial (true on syntax) -}
  [id]T : ∀ Γ A → (A [ Pre-id Γ ]Pre-Ty) == A
  [id]t : ∀ Γ t → (t [ Pre-id Γ ]Pre-Tm) == t

  [id]T Γ ∗ = idp
  [id]T Γ (⇒ A t u) = ⇒= ([id]T Γ A) ([id]t Γ t) ([id]t Γ u)
  [id]t nil (Var x) = idp
  [id]t (Γ :: (y , B)) (Var x) with (eqdecℕ x y)
  ...                              | inl x=y = Var= (x=y ^)
  ...                              | inr _ = [id]t Γ (Var x)

  {- identity is well-formed -}
  Γ⊢id:Γ : ∀ {Γ} → Γ ⊢C → Γ ⊢S Pre-id Γ > Γ
  Γ⊢id:Γ ec = es ec
  Γ⊢id:Γ Γ,x:A⊢@(cc Γ⊢ Γ⊢A idp) = sc (wkS (Γ⊢id:Γ Γ⊢) Γ,x:A⊢) Γ,x:A⊢ (var Γ,x:A⊢ (inr (idp , [id]T _ _))) idp

  {- action of substitutions on types and terms respects composition -}
  [∘]T : ∀ {Γ Δ Θ A γ δ} → Γ ⊢T A → Δ ⊢S γ > Γ → Θ ⊢S δ > Δ → ((A [ γ ]Pre-Ty) [ δ ]Pre-Ty) == (A [ γ ∘ δ ]Pre-Ty)
  [∘]t : ∀ {Γ Δ Θ A t γ δ} → Γ ⊢t t # A → Δ ⊢S γ > Γ → Θ ⊢S δ > Δ → ((t [ γ ]Pre-Tm) [ δ ]Pre-Tm) == (t [ γ ∘ δ ]Pre-Tm)

  [∘]T (ob _) _ _ = idp
  [∘]T (ar Γ⊢t:A Γ⊢u:A) Δ⊢γ:Γ Θ⊢δ:Δ = ⇒= ([∘]T (Γ⊢t:A→Γ⊢A Γ⊢t:A) Δ⊢γ:Γ Θ⊢δ:Δ) ([∘]t Γ⊢t:A Δ⊢γ:Γ Θ⊢δ:Δ) ([∘]t Γ⊢u:A Δ⊢γ:Γ Θ⊢δ:Δ)
  [∘]t (var {x = x} Γ⊢ x∈Γ) (sc {x = y} Δ⊢γ:Γ _ Δ⊢t:A[γ] idp) Θ⊢δ:Δ with (eqdecℕ x y )
  ... | inl idp = idp
  [∘]t (var Γ,y:A⊢ (inr (idp , idp))) (sc Δ⊢γ:Γ _ Δ⊢t:A[γ] idp) Θ⊢δ:Δ | inr x≠x = ⊥-elim (x≠x idp)
  [∘]t (var (cc Γ⊢ _ _) (inl x∈Γ)) (sc Δ⊢γ:Γ _ Δ⊢t:A[γ] idp) Θ⊢δ:Δ | inr _ = [∘]t (var Γ⊢ x∈Γ) Δ⊢γ:Γ Θ⊢δ:Δ

  {- composition of well-formed substitutions is well-formed -}
  ∘-admissibility : ∀ {Γ Δ Θ γ δ} → Δ ⊢S γ > Γ → Θ ⊢S δ > Δ → Θ ⊢S (γ ∘ δ) > Γ
  ∘-admissibility (es Δ⊢) Θ⊢δ:Δ = es (Δ⊢γ:Γ→Δ⊢ Θ⊢δ:Δ)
  ∘-admissibility (sc Δ⊢γ:Γ Γ,x:A⊢@(cc _ Γ⊢A _) Δ⊢t:A[γ] idp) Θ⊢δ:Δ = sc (∘-admissibility Δ⊢γ:Γ Θ⊢δ:Δ) Γ,x:A⊢ (trT ([∘]T Γ⊢A Δ⊢γ:Γ Θ⊢δ:Δ) ([]t Δ⊢t:A[γ] Θ⊢δ:Δ)) idp

  {- composition is associative, this is true only for well-formed substitutions -}
  ∘-associativity : ∀ {Γ Δ Θ Ξ γ δ θ} → Δ ⊢S γ > Γ → Θ ⊢S δ > Δ → Ξ ⊢S θ > Θ → ((γ ∘ δ) ∘ θ) == (γ ∘ (δ ∘ θ))
  ∘-associativity (es _) _ _ = idp
  ∘-associativity (sc Δ⊢γ:Γ _ Δ⊢t:A[γ] idp) Θ⊢δ:Δ Ξ⊢θ:Θ = ::= (∘-associativity Δ⊢γ:Γ Θ⊢δ:Δ Ξ⊢θ:Θ) (×= idp ([∘]t Δ⊢t:A[γ] Θ⊢δ:Δ Ξ⊢θ:Θ))

  {- Left unitality of composition -}

  -- To prove right-unitality, we need a analoguous of wk[]T and wk[]t for substitutions
  -- Composing if θ is a subst without x, acting (γ :: (x , u)) on it is same as acting just γ on it
  wk[]S : ∀ {Γ Δ γ x u B Θ θ} → Γ ⊢S θ > Θ → Δ ⊢S (γ :: (x , u)) > (Γ :: (x , B)) → (θ ∘ (γ :: (x , u))) == (θ ∘ γ)
  wk[]S (es _) _ = idp
  wk[]S (sc Γ⊢θ:Θ _ Γ⊢t:A[θ] idp) Δ⊢γ+:Γ+ = ::= (wk[]S Γ⊢θ:Θ Δ⊢γ+:Γ+) (×= idp (wk[]t Γ⊢t:A[θ] Δ⊢γ+:Γ+))

  ∘-left-unit : ∀{Γ Δ γ} → Δ ⊢S γ > Γ → (Pre-id Γ ∘ γ) == γ
  ∘-left-unit (es _) = idp
  ∘-left-unit Δ⊢γ+:Γ+@(sc {x = x} Δ⊢γ:Γ (cc Γ⊢ _ _) _ idp) with (eqdecℕ x x)
  ...                                                 | inl _ = ::= (wk[]S (Γ⊢id:Γ Γ⊢) Δ⊢γ+:Γ+ >> ∘-left-unit Δ⊢γ:Γ) idp
  ...                                                 | inr x≠x = ⊥-elim (x≠x idp)

 {- Right unitality of composition (true on syntax)-}
  ∘-right-unit : ∀ {Δ γ} →  (γ ∘ Pre-id Δ) == γ
  ∘-right-unit {Δ} {nil} = idp
  ∘-right-unit {Δ} {γ :: (y , t)} = ::= ∘-right-unit (×= idp ([id]t Δ t))

  {- Structure of CwF -}
  Γ,x:A⊢π:Γ : ∀ {Γ x A} → (Γ :: (x , A)) ⊢C → (Γ :: (x , A)) ⊢S Pre-π Γ x A > Γ
  Γ,x:A⊢π:Γ Γ,x:A⊢@(cc Γ⊢ _ _) = wkS (Γ⊢id:Γ Γ⊢) Γ,x:A⊢

  -- TODO : complete the CwF structure

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
{- With Agda's current sized types, we have a size ∞ with ∞ < ∞. That's
   obviously troublesome if we want to interpret sizes as ordinals and < as the
   less-than relation, and indeed we can use this rule to prove false (in
   multiple different ways).

   This file is an experiment to see whether we could still work with a system
   that doesn't have this rule.
-}

{-# OPTIONS --postfix-projections #-}
module irreflexive-lt where

open import Size

postulate
  𝟘 : Size

data Size≲ : (j : Size) → Set where
  ≲∞ : (i : Size) → Size≲ ∞
  <→≲ : ∀ {j} (i : Size< j) → Size≲ j

from≲ : ∀ {j} → Size≲ j → Size
from≲ (≲∞ i) = i
from≲ (<→≲ i) = i

∞′ : Size≲ ∞
∞′ = ≲∞ ∞

--------------------------------------------------------------------------------
-- Natural numbers

data ℕ (i : Size) : Set where
  zero : ℕ i
  suc : (j : Size< i) → ℕ j → ℕ i

-- Using the successor at size ∞ becomes nontrivial. The following is NOT
-- allowed since we use (∞ : Size< ∞).
-- suc₀ : ℕ ∞ → ℕ ∞
-- suc₀ n = suc ∞ n

-- Workaround: superfluous pattern matching.
suc₁ : ℕ ∞ → ℕ ∞
suc₁ zero = suc 𝟘 zero
suc₁ (suc j x) = suc (↑ j) (suc j x)

-- Case analysis
caseℕ : {T : Set} → (i : Size) → ℕ i → T → ((j : Size< i) → ℕ j → T) → T
caseℕ i zero z s = z
caseℕ i (suc j n) z s = s j n

-- Dependent elimination (with size-based termination).
indℕ : (P : (i : Size) → ℕ i → Set)
  → ((i : Size) → P i zero)
  → ((i : Size) (j : Size< i) (n : ℕ j) → P j n → P i (suc j n))
  → (i : Size) (n : ℕ i) → P i n
indℕ P Z S i zero = Z i
indℕ P Z S i (suc j n) = S i j n (indℕ P Z S j n)

--------------------------------------------------------------------------------
-- Streams

record 𝕊 (A : Set) (i : Size) : Set where
  coinductive
  field
    head : A
    tail : (j : Size< i) → 𝕊 A j

open 𝕊

variable
  A B : Set

-- Again, we CANNOT use tail at ∞ directly since this uses (∞ : Size< ∞).
-- tail₀ : 𝕊 ∞ → 𝕊 ∞
-- tail₀ xs = tail xs ∞

-- Workaround: The equivalent of the 'superfluous pattern matching' workaround
-- for suc.
tail₁ : 𝕊 A ∞ → 𝕊 A ∞
tail₁ xs .head = head {i = 𝟘} (tail xs 𝟘) -- [1]
tail₁ xs .tail j = tail (tail xs (↑ j)) j

-- [1] Without the implicit argument, this doesn't typecheck. Apparently the
-- size argument to head gets eagerly instantiated to ∞ or something.

replicate : (i : Size) → A → 𝕊 A i
replicate i a .head = a
replicate i a .tail j = replicate j a

map𝕊 : (A → B) → (i : Size) → 𝕊 A i → 𝕊 B i
map𝕊 f i xs .head = f (head xs)
map𝕊 f i xs .tail j = map𝕊 f j (tail xs j)

--------------------------------------------------------------------------------
-- Rose trees

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

mapList : (A → B) → List A → List B
mapList f [] = []
mapList f (x ∷ xs) = f x ∷ mapList f xs

data Tree (A : Set) (i : Size) : Set where
  leaf : A → Tree A i
  node : (j : Size< i) → List (Tree A j) → Tree A i

mapTree : (A → B) → (i : Size) → Tree A i → Tree B i
mapTree f i (leaf x) = leaf (f x)
mapTree f i (node j cs) = node j (mapList (mapTree f j) cs)

--------------------------------------------------------------------------------
-- Potentially infinite lists

mutual
  data CoList (A : Set) (i : Size) : Set where
    [] : CoList A i
    _∷_ : A → CoList′ A i → CoList A i

  record CoList′ (A : Set) (i : Size) : Set where
    coinductive
    field
      force : (j : Size< i) → CoList A j

open CoList′

open import Data.Product using (∃-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; inspect ; [_])
open import Relation.Binary.HeterogeneousEquality using (_≅_ ; refl)

postulate
  force-parametric : ∀ {A i} (xs : CoList′ A i) (j j′ : Size< i)
    → xs .force j ≅ xs .force j′

  size-parametric : ∀ {T : Size< ∞ → Set} (f : (i : Size< ∞) → T i)
    → (j j′ : Size< ∞)
    → f j ≅ f j′

mutual
  data _≈_ {A i j} : CoList A i → CoList A j → Set where
    [] : [] ≈ []
    _∷_ : ∀ {x y xs ys}
      → x ≡ y
      → xs ≈′ ys
      → (x ∷ xs) ≈ (y ∷ ys)

  record _≈′_ {A i j} (xs : CoList′ A i) (ys : CoList′ A j) : Set where
    coinductive
    field
      force : (k : Size< i) (l : Size< j) → xs .force k ≈ ys .force l

open _≈′_

force∞ : CoList′ A ∞ → CoList A ∞
force∞ {A} xs with xs .force 𝟘
... | [] = []
... | y ∷ ys = y ∷ ys′
  where
    ys′ : CoList′ A ∞
    ys′ .force i with xs .force (↑ i)
    ... | [] = []
    ... | z ∷ zs = zs .force i

𝕊→CoList : (i : Size) → 𝕊 A i → CoList A i
𝕊→CoList i xs = head xs ∷ λ { .force j → 𝕊→CoList j (tail xs j) }

-- Radical thought: Just kill ∞ altogether and work with (∀ i → CoList A i) and
-- (∃ i → List A i) directly. How much less useful does that make the system?
--
-- Perhaps we can auto-derive the iso (∃ i → List A i) ≅ List A.

-- Radical thought: What if we only provide the Thunk type from the stdlib? Can
-- we recover all other coinductive types from that?

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Data.List.Functions where

import      Lvl
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.List
open import Data.Option as Option using (Option)
import      Data.Option.Functions as Option
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Numeral.Finite
open import Numeral.Natural
open import Type

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

infixl 1000 _++_

open import Data.List.Functions.Positional public

-- The list of the successive application of `tail` on a list.
-- For a list `l`, the range of `n ↦ (tail ^ n)(l)` as a list.
-- Example:
--   tails []      = [[]]
--   tails [a]     = [[a] , []]
--   tails [a,b]   = [[a,b] , [b] , []]
--   tails [a,b,c] = [[a,b,c] , [b,c] , [c] , []]
-- Note: `∀{l} → (tails l = accumulateIterate (length l) tail l)`.
tails : List(T) → List(List(T))
tails ∅       = singleton(∅)
tails (x ⊰ l) = (x ⊰ l) ⊰ tails l

-- Applies a binary operator to each element in the list starting with the initial element.
-- Example:
--   foldₗ(▫)(init)[]          = init
--   foldₗ(▫)(init)[a]         = init▫a
--   foldₗ(▫)(init)[a,b]       = (init▫a)▫b
--   foldₗ(▫)(init)[a,b,c,d,e] = ((((init▫a)▫b)▫c)▫d)▫e
foldₗ : (Result → T → Result) → Result → List(T) → Result
foldₗ _   result ∅          = result
foldₗ _▫_ result (elem ⊰ l) = foldₗ _▫_ (result ▫ elem) l

-- Applies a binary operator to each element in the list starting with the initial element.
-- Example:
--   foldᵣ(▫)(init)[]          = init
--   foldᵣ(▫)(init)[a]         = a▫init
--   foldᵣ(▫)(init)[a,b]       = a▫(b▫init)
--   foldᵣ(▫)(init)[a,b,c,d,e] = a▫(b▫(c▫(d▫(e▫init))))
foldᵣ : (T → Result → Result) → Result → List(T) → Result
foldᵣ _   init ∅          = init
foldᵣ _▫_ init (elem ⊰ l) = elem ▫ (foldᵣ _▫_ init l)

-- Applies a binary operator to each element in the list starting with the initial element.
-- Example:
--   foldᵣ-init(▫)(init)[]          = init
--   foldᵣ-init(▫)(init)[a]         = init▫a
--   foldᵣ-init(▫)(init)[a,b]       = init▫(a▫b)
--   foldᵣ-init(▫)(init)[a,b,c,d,e] = init▫(a▫(b▫(c▫(d▫e))))
-- Same as (reduceOrᵣ (_▫_) (a) (a⊰l)) except that
-- this allows matching out one element when
-- there is only a first element as the head
--  and an _arbitrary_ list as the tail.
-- Also, this dIffers from foldᵣ in the following way:
--   foldᵣ      (_▫_) (1) [2,3] = 2 ▫ (3 ▫ 1)
--   foldᵣ-init (_▫_) (1) [2,3] = 1 ▫ (2 ▫ 3)
-- Also: foldᵣ-init(▫)(init)(l++[last]) = foldᵣ(▫)(last)(init⊰l)
foldᵣ-init : (T → T → T) → T → List(T) → T
foldᵣ-init _   init ∅          = init
foldᵣ-init _▫_ init (elem ⊰ l) = init ▫ (foldᵣ-init _▫_ elem l)

-- If the list is empty, use the result, else like foldₗ
-- Example:
--   reduceOrₗ(▫)(result)[]          = result
--   reduceOrₗ(▫)(result)[a]         = a
--   reduceOrₗ(▫)(result)[a,b]       = a▫b
--   reduceOrₗ(▫)(result)[a,b,c]     = (a▫b)▫c
--   reduceOrₗ(▫)(result)[a,b,c,d,e] = (((a▫b)▫c)▫d)▫e
reduceOrₗ : (T → T → T) → T → List(T) → T
reduceOrₗ _   result ∅          = result
reduceOrₗ _▫_ result (elem ⊰ l) = foldₗ _▫_ elem l

-- If the list is empty, use the result, else like foldᵣ
-- Example:
--   reduceOrᵣ(▫)(result)[]          = result
--   reduceOrᵣ(▫)(result)[a]         = a
--   reduceOrᵣ(▫)(result)[a,b]       = a▫b
--   reduceOrᵣ(▫)(result)[a,b,c]     = a▫(b▫c)
--   reduceOrᵣ(▫)(result)[a,b,c,d,e] = a▫(b▫(c▫(d▫e)))
reduceOrᵣ : (T → T → T) → T → List(T) → T
reduceOrᵣ _   init ∅          = init
reduceOrᵣ _▫_ init (elem ⊰ l) = foldᵣ-init _▫_ elem l

-- Accumulates the results of every step in `foldₗ` into a list.
-- Example:
--   accumulateFoldₗ(_▫_) result []        = [result]
--   accumulateFoldₗ(_▫_) result [a]       = [result▫a]
--   accumulateFoldₗ(_▫_) result [a,b]     = [result▫a , (result▫a)▫b]
--   accumulateFoldₗ(_▫_) result [a,b,c]   = [result▫a , (result▫a)▫b , ((result▫a)▫b)▫c]
--   accumulateFoldₗ(_▫_) result [a,b,c,d] = [result▫a , (result▫a)▫b , ((result▫a)▫b)▫c , (((result▫a)▫b)▫c)▫d]
accumulateFoldₗ : (Result → T → Result) → Result → List(T) → List(Result)
accumulateFoldₗ(_▫_) result ∅       = singleton(result)
accumulateFoldₗ(_▫_) result (x ⊰ l) = result ⊰ accumulateFoldₗ(_▫_) (result ▫ x) l

-- Accumulates the results of every step in `reduceₗ` into a list.
-- Example:
--   accumulateReduceₗ(_▫_) []        = []
--   accumulateReduceₗ(_▫_) [a]       = [a]
--   accumulateReduceₗ(_▫_) [a,b]     = [a , a▫b]
--   accumulateReduceₗ(_▫_) [a,b,c]   = [a , a▫b , (a▫b)▫c]
--   accumulateReduceₗ(_▫_) [a,b,c,d] = [a , a▫b , (a▫b)▫c , ((a▫b)▫c)▫d]
accumulateReduceₗ : (T → T → T) → List(T) → List(T)
accumulateReduceₗ(_▫_) ∅       = ∅
accumulateReduceₗ(_▫_) (x ⊰ l) = accumulateFoldₗ(_▫_) x l

-- Accumulates the results of every step in `_^_` into a list.
-- Example:
--   accumulateIterate₀ 0 f(x) = []
--   accumulateIterate₀ 1 f(x) = [x]
--   accumulateIterate₀ 2 f(x) = [x , f(x)]
--   accumulateIterate₀ 3 f(x) = [x , f(x) , f(f(x))]
--   accumulateIterate₀ 4 f(x) = [x , f(x) , f(f(x)) , f(f(f(x)))]
accumulateIterate₀ : ℕ → (T → T) → (T → List(T))
accumulateIterate₀ 𝟎      f(x) = ∅
accumulateIterate₀ (𝐒(n)) f(x) = x ⊰ accumulateIterate₀ n f (f(x))

-- Accumulates the results of every step in `_^_` into a list.
-- Example:
--   accumulateIterate 0 f(x) = [x]
--   accumulateIterate 1 f(x) = [x , f(x)]
--   accumulateIterate 2 f(x) = [x , f(x) , f(f(x))]
--   accumulateIterate 3 f(x) = [x , f(x) , f(f(x)) , f(f(f(x)))]
--   accumulateIterate 4 f(x) = [x , f(x) , f(f(x)) , f(f(f(x))) , f(f(f(f(x))))]
accumulateIterate : ℕ → (T → T) → (T → List(T))
accumulateIterate n = accumulateIterate₀(𝐒(n))

-- List concatenation.
-- Concatenates (joins/glues) two lists together.
-- Examples:
--   [] ++ [] = []
--   [a] ++ [b] = [a,b]
--   [a,b,c] ++ [d,e,f] = [a,b,c,d,e,f]
_++_ : List(T) → List(T) → List(T)
_++_ = swap(foldᵣ (_⊰_))

-- Concatenates multiple lists together.
-- Examples:
--   concat [[a,b,c] , [d,e] , [f] , [g,h]]
--   = [a,b,c] ++ [d,e] ++ [f] ++ [g,h] =
--   = [a,b,c,d,e,f,g,h]
concat : List(List(T)) → List(T)
concat = foldᵣ(_++_) ∅

-- Postpends an element to a list, inserting it to the end of the list.
-- Examples:
--   postpend a []      = [a]
--   postpend b [a]     = [a,b]
--   postpend c [a,b]   = [a,b,c]
--   postpend d [a,b,c] = [a,b,c,d]
postpend : T → List(T) → List(T)
postpend a ∅       = a ⊰ ∅
postpend a (x ⊰ l) = x ⊰ postpend a l

-- Inserts an element to a list, inserting it at the given position of the list.
-- If the given position is out of range, then the element is postpended to the list.
-- Examples:
--   insert 2 x []        = [x]
--   insert 2 x [a]       = [a,x]
--   insert 2 x [a,b]     = [a,b,x]
--   insert 2 x [a,b,c]   = [a,b,x,c]
--   insert 2 x [a,b,c,d] = [a,b,x,c,d]
insert : ℕ → T → List(T) → List(T)
insert 𝟎                = _⊰_
insert (𝐒(_)) a ∅       = singleton a
insert (𝐒(i)) a (x ⊰ l) = x ⊰ insert i a l

module LongOper where
  pattern empty = ∅
  pattern prepend elem list = elem ⊰ list

-- Applies a function on each element in the list
-- Examples:
--   map f[]      = []
--   map f[a]     = [f(a)]
--   map f[a,b]   = [f(a),f(b)]
--   map f[a,b,c] = [f(a),f(b),f(c)]
map : (A → B) → (List(A) → List(B))
map _ ∅ = ∅
map f (x ⊰ l) = f(x) ⊰ (map f l)

-- Filters the list while mapping it
mapFilter : (A → Option(B)) → (List(A) → List(B))
mapFilter _ ∅ = ∅
mapFilter f (x ⊰ l) with f(x)
... | Option.Some(y) = y ⊰ (mapFilter f l)
... | Option.None    = mapFilter f l

-- Maps every element to a list in the given list and then concatenates the resulting list.
-- Note: Functionally equivalent to: `concat ∘₂ map`.
-- Example: `concatMap(x ↦ [x , x + 1 , x + 2]) [10,20,30,40] = [10,11,12 , 20,21,22 , 30,31,32 , 40,41,42]`
-- Alternative implementation:
--   concatMap f ∅ = ∅
--   concatMap f (x ⊰ l) = f(x) ++ concatMap f l
concatMap : (A → List(B)) → (List(A) → List(B))
concatMap f = foldᵣ((_++_) ∘ f) ∅

-- The nth element in the list
-- Examples:
-- • `index₀ 0 [a,b,c] = Some a`
-- • `index₀ 1 [a,b,c] = Some b`
-- • `index₀ 2 [a,b,c] = Some c`
-- • `index₀ 3 [a,b,c] = None`
-- • `index₀ 4 [a,b,c] = None`
index₀ : ℕ → List(T) → Option(T)
index₀ _      ∅       = Option.None
index₀ 𝟎      (x ⊰ _) = Option.Some(x)
index₀ (𝐒(n)) (_ ⊰ l) = index₀ n l

-- The sublist with the first n elements in the list.
-- Also called: "take" in the Haskell standard library.
-- Example:
-- • `initial 0 [1,2,3] = []`
-- • `initial 1 [1,2,3] = [1]`
-- • `initial 2 [1,2,3] = [1,2]`
-- • `initial 3 [1,2,3] = [1,2,3]`
-- • `initial 4 [1,2,3] = [1,2,3]`
-- • `initial 5 [1,2,3] = [1,2,3]`
initial : ℕ → List(T) → List(T)
initial _      ∅       = ∅
initial 𝟎      (_ ⊰ _) = ∅
initial (𝐒(n)) (x ⊰ l) = x ⊰ (initial n l)

-- The sublist without the first n elements in the list
-- Example:
-- • `skip 0 [1,2,3] = [1,2,3]`
-- • `skip 1 [1,2,3] = [2,3]`
-- • `skip 2 [1,2,3] = [3]`
-- • `skip 3 [1,2,3] = []`
-- • `skip 4 [1,2,3] = []`
-- • `skip 5 [1,2,3] = []`
skip : ℕ → List(T) → List(T)
skip _      ∅         = ∅
skip 𝟎      l@(_ ⊰ _) = l
skip (𝐒(n)) (x ⊰ l)   = skip n l

-- TODO: Maybe rename this to "extractFirst"?
-- Extracts the first element from the list if there is one.
-- Example: `splitFirst [1,2,3] = Some(1 , [2,3])`
splitFirst : List(T) → Option(T ⨯ List(T))
splitFirst ∅       = Option.None
splitFirst (x ⊰ l) = Option.Some(x , l)

-- Extracts the last element from the list if there is one.
-- Example: `splitLast [1,2,3] = Some([1,2] , 3)`
splitLast : List(T) → Option(List(T) ⨯ T)
splitLast ∅           = Option.None
splitLast (x ⊰ ∅)     = Option.Some(∅ , x)
splitLast (x ⊰ y ⊰ l) = Option.map (Tuple.mapLeft (x ⊰_)) (splitLast (y ⊰ l))

-- Split a list into two sublist parts at the specified index.
-- The first list's length is the specified index.
-- The second list starts at the specified index.
-- Example:
--   splitAt 0 [a,b,c,d] = ([] , [a,b,c,d])
--   splitAt 1 [a,b,c,d] = ([a] , [b,c,d])
--   splitAt 2 [a,b,c,d] = ([a,b] , [c,d])
--   splitAt 3 [a,b,c,d] = ([a,b,c] , [d])
--   splitAt 4 [a,b,c,d] = ([a,b,c,d] , [])
--   splitAt 5 [a,b,c,d] = ([a,b,c,d] , [])
splitAt : ℕ → List(T) → (List(T) ⨯ List(T))
splitAt 𝟎     l       = (∅ , l)
splitAt (𝐒 n) ∅       = (∅ , ∅)
splitAt (𝐒 n) (x ⊰ l) = Tuple.mapLeft (x ⊰_) (splitAt n l)

-- All ordered sublist partitions of the specified list with only two parts.
--
splits₂ : List(T) → List(List(T) ⨯ List(T))
splits₂ l = (∅ , l) ⊰ f ∅ l where
  f : List(T) → List(T) → List(List(T) ⨯ List(T))
  f _ ∅       = ∅
  f a (x ⊰ b) = (postpend x a , b) ⊰ f (postpend x a) b

-- Length of the list (number of elements in the list).
-- Examples:
-- • `length []      = 0`
-- • `length [a]     = 1`
-- • `length [a,b]   = 2`
-- • `length [a,b,c] = 3`
-- • `length [b,c,a] = 3`
-- • `length [c,a,b] = 3`
-- • `length [b,a,c] = 3`
-- • `length [a,c,b] = 3`
-- • `length [b,a,c] = 3`
length : List(T) → ℕ
length = foldᵣ (const 𝐒) 0

-- The nth element in the list as a total function.
index : (l : List(T)) → 𝕟(length(l)) → T
index ∅       ()
index (x ⊰ l) 𝟎     = x
index (x ⊰ l) (𝐒 n) = index l n

-- The sublist with the last n elements in the list
-- last : ℕ → List(T) → List(T)
-- last n l = skip(length(l) −₀ ) l

-- TODO: Generalize
mapWindow2ₗ : (T → T → T) → List(T) → List(T)
mapWindow2ₗ f (x₁ ⊰ x₂ ⊰ l) = (f x₁ x₂) ⊰ (mapWindow2ₗ f (x₂ ⊰ l))
{-# CATCHALL #-}
mapWindow2ₗ _ _ = ∅

_orₗ_ : List(T) → List(T) → List(T)
_orₗ_ ∅ default      = default
_orₗ_ (l @(_ ⊰ _)) _ = l

-- Reverse the order of the elements in the list.
-- Example: `reverse [a,b,c,d] = [d,c,b,a]`.
reverse : List(T) → List(T)
reverse ∅ = ∅
reverse (x ⊰ l) = postpend x (reverse l)

import Function.Iteration as Function

-- The list with a list concatenated (repeated) n times.
-- Example: `[a,b,c] ++^ 4 = [a,b,c] ++ [a,b,c] ++ [a,b,c] ++ [a,b,c] = [a,b,c , a,b,c , a,b,c , a,b,c]`.
_++^_ : List(T) → ℕ → List(T)
_++^_ l n = Function.repeatᵣ n (_++_) l ∅

-- The list with an element repeated n times
-- Example: `repeat a 4 = [a,a,a,a]`.
repeat : T → ℕ → List(T)
repeat = (_++^_) ∘ singleton

-- Whether at least one element in the list satisfies the given boolean predicate function.
-- Note: `∀{pred}{l} → (satisfiesAny pred l = foldᵣ((_||_) ∘ pred) 𝐹 l)`. They are functionally equivalent but the difference is that this exits early when something false is found which is good for performance.
satisfiesAny : (T → Bool) → List(T) → Bool
satisfiesAny pred ∅       = 𝐹
satisfiesAny pred (x ⊰ l) with pred(x)
... | 𝑇 = 𝑇
... | 𝐹 = satisfiesAny(pred)(l)

-- Whether all elements in the list satisfies the given boolean predicate function.
-- Note: `∀{pred}{l} → (satisfiesAll pred l = foldᵣ((_&&_) ∘ pred) 𝑇 l)`. They are functionally equivalent but the difference is that this exits early when something false is found which is good for performance.
satisfiesAll : (T → Bool) → List(T) → Bool
satisfiesAll pred ∅       = 𝑇
satisfiesAll pred (x ⊰ l) with pred(x)
... | 𝑇 = satisfiesAll(pred)(l)
... | 𝐹 = 𝐹

satisfiesAll₂ : (T → T → Bool) → (T → Bool) → (T → Bool) → (List(T) → List(T) → Bool)
satisfiesAll₂(_▫_) l r ∅          ∅          = 𝑇
satisfiesAll₂(_▫_) l r l₁@(_ ⊰ _) ∅          = satisfiesAll l l₁
satisfiesAll₂(_▫_) l r ∅          l₂@(_ ⊰ _) = satisfiesAll r l₂
satisfiesAll₂(_▫_) l r (x₁ ⊰ l₁)  (x₂ ⊰ l₂)  = (x₁ ▫ x₂) && satisfiesAll₂(_▫_) l r l₁ l₂
{-satisfiesAll₂(_▫_) l r (x₁ ⊰ l₁)  (x₂ ⊰ l₂)  with (x₁ ▫ x₂)
... | 𝑇 = satisfiesAll₂(_▫_) l r l₁ l₂
... | 𝐹 = 𝐹-}

-- TODO
-- List-apply : ∀{L : List(Type{ℓ})} → (foldᵣ (_⨯_) (Out) (L)) → ∀{Out : Type{ℓ}} → (foldᵣ (_→ᶠ_) (Out) (L)) → Out
-- List-apply(∅)           (f) = f
-- List-apply(head ⊰ rest) (f) = List-apply(rest) (f(head))

-- fn-to-list : ∀{L : List(Type{ℓ})}{Out : Type{ℓ}} → (foldᵣ (_→ᶠ_) (Out) (L)) → (List(Type{ℓ}) → Out)
-- fn-to-list{∅} =

-- Replacing the nth element in the list.
-- Example: `modifyAt 2 f [a,b,c,d] = [a,b,f(c),d]`.
modifyAt : ℕ → (T → T) → List(T) → List(T)
modifyAt _      f ∅       = ∅
modifyAt 𝟎      f (x ⊰ l) = f(x) ⊰ l
modifyAt (𝐒(n)) f (x ⊰ l) = x ⊰ modifyAt n f l

-- Example: `replaceAt 2 x [a,b,c,d] = [a,b,x,d]`.
replaceAt : ℕ → T → List(T) → List(T)
replaceAt n = modifyAt n ∘ const

-- The list without the nth element in the list
-- Example: `withoutIndex 2 [a,b,c,d] = [a,b,d]`.
withoutIndex : ℕ → List(T) → List(T)
withoutIndex _       ∅       = ∅
withoutIndex 𝟎       (_ ⊰ l) = l
withoutIndex (𝐒(n))  (x ⊰ l) = x ⊰ withoutIndex(n)(l)

-- Example: `swapIndex 1 3 [a,b,c,d,e,f] = [a,d,c,b,e,f]`.
swapIndex : ℕ → ℕ → List(T) → List(T)
swapIndex _      _      ∅      = ∅
swapIndex 𝟎      𝟎      (x ⊰ l) = (x ⊰ l)
swapIndex (𝐒(a)) 𝟎      (x ⊰ l) = Option.map(_⊰ replaceAt a x l) (index₀ a l) Option.or (x ⊰ l)
swapIndex 𝟎      (𝐒(b)) (x ⊰ l) = Option.map(_⊰ replaceAt b x l) (index₀ b l) Option.or (x ⊰ l)
swapIndex (𝐒(a)) (𝐒(b)) (x ⊰ l) = x ⊰ swapIndex a b l

-- The given list with only the elements that satisfy the given predicate (without the elements that do not satisfy the given predicate).
-- Example: `filter(_<? 10) [0,10,11,1,2,12,3,13,14,4,5] = [0,1,2,3,4,5]`.
filter : (T → Bool) → List(T) → List(T)
filter f(∅)     = ∅
filter f(x ⊰ l) = (if f(x) then (x ⊰_) else id) (filter f(l))

-- Finds the first element that satisfies the given predicate in the given list.
find : (T → Bool) → List(T) → Option(T)
find f(∅)     = Option.None
find f(x ⊰ l) with f(x)
... | 𝑇 = Option.Some(x)
... | 𝐹 = find f(l)

-- Finds and extracts the first element satisfying the given predicate.
-- Example: `extractFirst(_> 2) [0,1,2,3,4,5] = Some(3 , [0,1,2,4,5])`.
extractFirstBy : (T → Bool) → List(T) → Option(T ⨯ List(T))
extractFirstBy f(∅)     = Option.None
extractFirstBy f(x ⊰ l) with f(x)
... | 𝑇 = Option.Some(x , l)
... | 𝐹 = Option.map(Tuple.mapRight(x ⊰_)) (extractFirstBy f(l))

-- The number of elements satisfying the given predicate in the given list.
count : (T → Bool) → List(T) → ℕ
count f(∅)     = 𝟎
count f(x ⊰ l) = (if f(x) then 𝐒 else id) (count f(l))

-- Whether the given list is the empty list.
isEmpty : List(T) → Bool
isEmpty(∅)     = 𝑇
isEmpty(_ ⊰ _) = 𝐹

-- Separates a list into 2 lists of almost equal length putting every other element into different lists.
-- Example:
--   separate₂ []          = ([]      , [])
--   separate₂ [a]         = ([a]     , [])
--   separate₂ [a,b]       = ([a]     , [b])
--   separate₂ [a,b,c]     = ([a,c]   , [b])
--   separate₂ [a,b,c,d]   = ([a,c]   , [b,d])
--   separate₂ [a,b,c,d,e] = ([a,c,e] , [b,d])
separate₂ : List(T) → (List(T) ⨯ List(T))
separate₂ ∅           = (∅ , ∅)
separate₂ (x ⊰ ∅)     = (singleton x , ∅)
separate₂ (x ⊰ y ⊰ l) = Tuple.map (x ⊰_) (y ⊰_) (separate₂ l)

-- Example:
--   interleave [[0,1,2],[10,11,12,13,14],[100,101]] = [0,10,100 , 1,11,101 , 2,12 , 13 , 14]
-- Termination:
--   Terminates because the argument in the recursion `map tail ls` shrinks every list until they all become empty, and when all lists are empty, the function branches to the other trivially terminating case.
{-# TERMINATING #-}
interleave : List(List(T)) → List(T)
interleave ls with satisfiesAll isEmpty ls
... | 𝑇 = ∅
... | 𝐹 = foldᵣ (Option.partialMap id (_⊰_) ∘ first) (interleave(map tail ls)) ls

-- Note: This is similiar to a function called `zipWith` in the Haskell standard library.
-- TODO: Generalize like https://stackoverflow.com/questions/39991581/how-can-i-implement-generalized-zipn-and-unzipn-in-haskell
map₂ : (A₁ → A₂ → B) → (List(A₁) → List(B)) → (List(A₂) → List(B)) → (List(A₁) → List(A₂) → List(B))
map₂ f g₁ g₂ ∅          ∅          = ∅
map₂ f g₁ g₂ ∅          l₂@(_ ⊰ _) = g₂ l₂
map₂ f g₁ g₂ l₁@(_ ⊰ _) ∅          = g₁ l₁
map₂ f g₁ g₂ (x₁ ⊰ l₁)  (x₂ ⊰ l₂)  = f x₁ x₂ ⊰ map₂ f g₁ g₂ l₁ l₂

-- Rotates to the left.
-- Example:
--   rotateₗ 3 [a,b,c,d,e]
--   = rotateₗ 2 [b,c,d,e,a]
--   = rotateₗ 1 [c,d,e,a,b]
--   = rotateₗ 0 [d,e,a,b,c]
--   = [d,e,a,b,c]
rotateₗ : ℕ → List(T) → List(T)
rotateₗ 𝟎      l       = l
rotateₗ (𝐒(n)) ∅       = ∅
rotateₗ (𝐒(n)) (x ⊰ l) = postpend x (rotateₗ n l)

rotateᵣ : ℕ → List(T) → List(T)
rotateᵣ n l with splitLast l
... | Option.None        = ∅
... | Option.Some(r , x) = x ⊰ r

-- Examples:
--   every n [] = []
--   every 0  [0,1,2,3,4,5,6,7,8] = []
--   every 1  [0,1,2,3,4,5,6,7,8] = [0,1,2,3,4,5,6,7,8]
--   every 2  [0,1,2,3,4,5,6,7,8] = [0,2,4,6,8]
--   every 3  [0,1,2,3,4,5,6,7,8] = [0,3,6]
--   every 4  [0,1,2,3,4,5,6,7,8] = [0,4,8]
--   every 5  [0,1,2,3,4,5,6,7,8] = [0,5]
--   every 6  [0,1,2,3,4,5,6,7,8] = [0,6]
--   every 7  [0,1,2,3,4,5,6,7,8] = [0,7]
--   every 8  [0,1,2,3,4,5,6,7,8] = [0,8]
--   every 9  [0,1,2,3,4,5,6,7,8] = [0]
--   every 10 [0,1,2,3,4,5,6,7,8] = [0]
-- Alternative implementations:
-- • every n l = map head (accumulateIterate₀ (length(n) ⌈/₀⌉ n) (skip n) l)
--   every 0         _       = ∅
--   every 1         l       = l
--   every (𝐒(𝐒(n))) ∅       = ∅
-- • every (𝐒(𝐒(n))) (x ⊰ l) = x ⊰ every (𝐒(𝐒(n))) (skip (𝐒(n)) l)
every : ℕ → List(T) → List(T)
every 𝟎      = const ∅
every (𝐒(n)) = impl 𝟎 where
  -- TODO: Is it possible to prove stuff about `every` when `impl` is hidden in a where clause? `impl` essentially contains a counter, so an alternative implementation would be having `every` having two arguments.
  impl : ℕ → List(T) → List(T)
  impl _     ∅       = ∅
  impl 𝟎     (x ⊰ l) = x ⊰ impl n l
  impl (𝐒 k) (x ⊰ l) = impl k l

-- Examples:
--   separate 0  [0,1,2,3,4,5,6,7,8] = []
--   separate 1  [0,1,2,3,4,5,6,7,8] = [[0,1,2,3,4,5,6,7,8]]
--   separate 2  [0,1,2,3,4,5,6,7,8] = [[0,2,4,6,8],[1,3,5,7]]
--   separate 3  [0,1,2,3,4,5,6,7,8] = [[0,3,6],[1,4,7],[2,5,8]]
--   separate 4  [0,1,2,3,4,5,6,7,8] = [[0,4,8],[1,5],[2,6],[3,7]]
--   separate 5  [0,1,2,3,4,5,6,7,8] = [[0,5],[1,6],[2,7],[3,8],[4]]
--   separate 6  [0,1,2,3,4,5,6,7,8] = [[0,6],[1,7],[2,8],[3],[4],[5]]
--   separate 7  [0,1,2,3,4,5,6,7,8] = [[0,7],[1,8],[2],[3],[4],[5],[6]]
--   separate 8  [0,1,2,3,4,5,6,7,8] = [[0,8],[1],[2],[3],[4],[5],[6],[7]]
--   separate 9  [0,1,2,3,4,5,6,7,8] = [[0],[1],[2],[3],[4],[5],[6],[7],[8]]
--   separate 10 [0,1,2,3,4,5,6,7,8] = [[0],[1],[2],[3],[4],[5],[6],[7],[8],[]]
--   separate 11 [0,1,2,3,4,5,6,7,8] = [[0],[1],[2],[3],[4],[5],[6],[7],[8],[],[]]
separate : ℕ → List(T) → List(List(T))
separate n l = map (every n) (accumulateIterate₀ n tail l)

insertIn : T → (l : List(T)) → 𝕟₌(length l) → List(T)
insertIn a l       𝟎      = a ⊰ l
insertIn a ∅       (𝐒(_)) = singleton a
insertIn a (x ⊰ l) (𝐒(i)) = x ⊰ insertIn a l i


text:
{-# OPTIONS --universe-polymorphism --no-positivity-check #-}

module Alg-IIR where

data Level : Set where
      zero : Level
      suc  : Level -> Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}

max : Level -> Level -> Level
max  zero    m      = m
max (suc n)  zero   = suc n
max (suc n) (suc m) = suc (max n m)

{-# BUILTIN LEVELMAX max #-}

_o_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f o g = λ x → f (g x)
infixl 50 _o_

record Sg {a b : Level}(S : Set a)(T : S -> Set b) : Set (max a b) where
  constructor _,_
  field
    fst : S
    snd : T fst

infixr 40 _,_

record Lifted {l : Level} (A : Set l) : Set (suc l) where
  constructor lif
  field
    fil : A

open Lifted

lift : {i : Level} -> Set i -> Set (suc i)
lift x =  Lifted x

unl : {l r : Level}{A : Set l}{P : Lifted A -> Set r} ->
      ((a : A) -> P (lif a)) -> (a : Lifted A) -> P a
unl p a = p (fil a)

mutual
  data IRD (I : Set1)(J : I -> Set1) : Set1 where
    var : I -> IRD I J
    con : Set -> IRD I J
    _*_ : (S : IRD I J) -> (Deco S -> IRD I J) -> IRD I J
    _>_ : (S : Set) -> (S -> IRD I J) -> IRD I J

  Deco : forall {I J} -> IRD I J -> Set1
  Deco {I}{J} (var i) = J i
  Deco (con A) = lift A -- grr
  Deco (S * T) = Sg (Deco S) \ s -> Deco (T s)
  Deco (S > T) = (s : S) -> Deco (T s)

_-:>_ : forall {a b c}{I : Set a} -> (I -> Set b) -> (I -> Set c)
        -> Set (max a (max b c))
_-:>_ {I = I} S T = (i : I) -> S i -> T i

mutual
  Func : forall {I J} -> IRD I J -> (X : I -> Set)(d : X -:> J) -> Set
  Func (var i) X d = X i
  Func (con A) X d = A
  Func (S * T) X d = Sg (Func S X d) \ s -> Func (T (deco S X d s)) X d
  Func (S > T) X d = (s : S) -> Func (T s) X d

  deco : forall {I J} -> (D : IRD I J) -> (X : I -> Set)(d : X -:> J) ->
           Func D X d -> Deco D
  deco (var i) X d x = d i x
  deco (con A) X d a = lif a
  deco (S * T) X d (s , t) = s' , t' where
    s' = deco S X d s
    t' = deco (T s') X d t
  deco (S > T) X d f = \ s -> deco (T s) X d (f s)

mutual
  data DATA {I J}(F : I -> IRD I J)(d : (Deco o F) -:> J)(i : I) : Set where
    <_> : Func (F i) (DATA F d) decode -> DATA F d i

  decode : forall {I J}{F : I -> IRD I J}{d : (Deco o F) -:> J} ->
           DATA F d -:> J
  decode {I}{J}{F}{d} i < xs > = d i (deco (F i) (DATA F d) decode xs)

data MyTags : Set where
  zz ss : MyTags

[_/_] : forall {l}{P : MyTags -> Set l} -> P zz -> P ss -> (t : MyTags) -> P t
[ z / s ] zz = z
[ z / s ] ss = s

record One {a} : Set a where
  constructor <>

NAT : One {suc zero} -> IRD One \ _ -> One
NAT _ = con MyTags * unl [ con One / var _ ]

Nat : Set
Nat = DATA NAT _ _

myze : Nat
myze = < zz , _ >

mysu : Nat -> Nat
mysu n = < ss , n >

data Two : Set where
  tt ff : Two

not : Two -> Two
not tt = ff
not ff = tt

_&&_ : Two -> Two -> Two
tt && b = b
ff && b = ff

_=N=_ : Nat -> Nat -> Two
< zz , _ > =N= < zz , _ > = tt
< zz , _ > =N= < ss , _ > = ff
< ss , _ > =N= < zz , _ > = ff
< ss , m > =N= < ss , n > = m =N= n

data Zero : Set where

So : Two -> Set
So tt = One
So ff = Zero

FREL :  One {suc zero} -> IRD One \ _ -> Lifted (Nat -> Two)
FREL _ = con MyTags * unl
           [ con One
           / (var _ * unl \ f -> con Nat * unl \ x -> con (So (f x)))
           ]

frel : Deco o FREL -:> \ _ -> Lifted (Nat -> Two)
frel _ (lif zz , _)                  = lif \ _ -> tt
frel _ (lif ss , lif f , lif x , p)  = lif \ y -> not (y =N= x) && f y

Frel : Set
Frel = DATA FREL frel _

good : Frel
good = < ss , < ss , < ss , < zz , _ > ,
         myze , _ > ,
         mysu myze , _ > ,
         mysu (mysu myze) , _ >

{-
bad : Frel
bad =  < ss , < ss , < ss , < zz , _ > ,
         myze , _ > ,
         mysu myze , _ > ,
         myze , {!!} >
-}

UNI :  One {suc zero} -> IRD One \ _ -> Set
UNI _ =  con MyTags * unl
           [ con One
           / (var _ * \ S -> S > \ _ -> var _)
           ]

uni : Deco o UNI -:> \ _ -> Set
uni i (lif zz , _) = Nat
uni i (lif ss , S , T) = (s : S) -> T s


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

open import Level
open import Categories.Category using () renaming (Category to Setoid-Category)
open import Categories.Category.Monoidal using (Monoidal)

module Categories.Pseudofunctor.Instance.EnrichedUnderlying
  {o ℓ e} {V : Setoid-Category o ℓ e} (M : Monoidal V) (v : Level) where

-- The "forgetful" functor from V-enriched categories to their
-- underlying Setoid-categories.

open import Data.Product as Prod using (_,_)

open import Categories.Bicategory.Instance.Cats
open import Categories.Bicategory.Instance.EnrichedCats M
open import Categories.Enriched.Category M
open import Categories.Enriched.Functor M
open import Categories.Enriched.NaturalTransformation M
import Categories.Morphism.Reasoning as MorphismReasoning
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
open import Categories.Pseudofunctor using (Pseudofunctor)

private
  module V = Setoid-Category V
  module UnderlyingReasoning {c} (C : Category c) where
    open Underlying C public hiding (id)
    open HomReasoning public
    open MorphismReasoning (Underlying C) public
  open NaturalTransformation using (_[_])

  -- Aliases used to shorten some proof expressions

  module UF = UnderlyingFunctor
  infixr 14 _$₀_ _$₁_
  _$₀_ = UF.F₀
  _$₁_ = UF.F₁

-- The "forgetful" pseudofunctor mapping a V-enriched category to its
-- underlying Setoid-category.
--
-- Note that all the equational reasoning happens in the underlying
-- (ordinary) categories!

EnrichedUnderlying : Pseudofunctor (EnrichedCats v) (Cats v ℓ e)
EnrichedUnderlying = record
  { P₀ = Underlying
  ; P₁ = record
    { F₀ = UnderlyingFunctor
    ; F₁ = UnderlyingNT
    ; identity     = V.Equiv.refl
    ; homomorphism = V.Equiv.refl
    ; F-resp-≈     = λ eq → eq
    }
  ; P-identity = λ {C} →
    let module C = Underlying C
        open UnderlyingReasoning C
    in niHelper record
      { η = λ _ → ntHelper record
        { η       = λ _ → C.id
        ; commute = λ f → begin
            C.id ∘ f              ≈⟨ identityˡ ⟩
            f                     ≈˘⟨ identityʳ ○ V.identityˡ ⟩
            (V.id V.∘ f) ∘ C.id   ∎
        }
      ; η⁻¹ = λ _ → ntHelper record
        { η       = λ _ → C.id
        ; commute = λ f → begin
            C.id ∘ (V.id V.∘ f)   ≈⟨ identityˡ ○ V.identityˡ ⟩
            f                     ≈˘⟨ identityʳ ⟩
            f ∘ C.id              ∎
        }
      ; commute = λ _ → V.Equiv.refl
      ; iso     = λ _ → record { isoˡ = C.identityˡ ; isoʳ = C.identityʳ }
      }
  ; P-homomorphism = λ {C D E} →
    let module C = Underlying C
        module D = Underlying D
        module E = Underlying E
        open UnderlyingReasoning E
    in niHelper record
      { η = λ{ (F , G) → ntHelper record
        { η       = λ _ → E.id
        ; commute = λ f → begin
            E.id ∘ F $₁ G $₁ f     ≈⟨ id-comm-sym ⟩
            F $₁ G $₁ f ∘ E.id     ≈˘⟨ V.assoc ⟩∘⟨refl ⟩
            (F ∘F G) $₁ f ∘ E.id   ∎
        } }
      ; η⁻¹ = λ{ (F , G) → ntHelper record
        { η       = λ _ → E.id
        ; commute = λ f → begin
            E.id ∘ (F ∘F G) $₁ f   ≈⟨ id-comm-sym ⟩
            (F ∘F G) $₁ f ∘ E.id   ≈⟨ V.assoc ⟩∘⟨refl ⟩
            F $₁ G $₁ f ∘ E.id     ∎
        } }
      ; commute = λ _ → id-comm-sym
      ; iso     = λ _ → record { isoˡ = E.identityˡ ; isoʳ = E.identityʳ }
      }
  ; unitaryˡ = λ {_ D} →
    let module D = Underlying D
        open UnderlyingReasoning D
    in begin
      D.id ∘ D.id ∘ (V.id V.∘ D.id) ∘ D.id   ≈⟨ identityˡ ○ identityˡ ⟩
      (V.id V.∘ D.id) ∘ D.id                 ≈⟨ identityʳ ○ V.identityˡ ⟩
      D.id                                   ∎
  ; unitaryʳ = λ {C D F X} →
    let module C = Underlying C
        module D = Underlying D
        open UnderlyingReasoning D
    in begin
      D.id ∘ D.id ∘ F $₁ C.id ∘ D.id   ≈⟨ identityˡ ○ identityˡ ○ identityʳ ⟩
      F $₁ C.id                        ≈⟨ UF.identity F ⟩
      D.id                             ∎
  ; assoc = λ {_ B C D F G H X} →
    let module B = Underlying B
        module C = Underlying C
        module D = Underlying D
        open UnderlyingReasoning D
    in ∘-resp-≈ʳ (begin
      D.id ∘ (H ∘F G) $₁ B.id ∘ D.id   ≈⟨ refl⟩∘⟨ V.assoc ⟩∘⟨refl ⟩
      D.id ∘ H $₁ G $₁ B.id ∘ D.id     ≈⟨ refl⟩∘⟨ UF.F-resp-≈ H
                                                    (UF.identity G) ⟩∘⟨refl ⟩
      D.id ∘ H $₁ C.id ∘ D.id          ≈⟨ id-comm-sym ⟩
      (H $₁ C.id ∘ D.id) ∘ D.id        ∎)
  }


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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.Properties.VoteData as VoteDataProps
import      LibraBFT.Impl.Consensus.ConsensusTypes.VoteData            as VoteData
open import LibraBFT.Impl.Consensus.ConsensusTypes.QuorumCert          as QuorumCert
import      LibraBFT.Impl.Types.LedgerInfoWithSignatures               as LedgerInfoWithSignatures
import      LibraBFT.Impl.Types.Properties.LedgerInfoWithSignatures    as LedgerInfoWithSignaturesProps
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Hash
open import Util.KVMap                                                 as Map
open import Util.Prelude

module LibraBFT.Impl.Consensus.ConsensusTypes.Properties.QuorumCert (self : QuorumCert) (vv : ValidatorVerifier) where
  voteHash = hashVD (self ^∙ qcVoteData)

  record rnd≡0Props : Set where
    field
        par≡cert : self ^∙ qcParentBlock    ≡ self ^∙ qcCertifiedBlock
        cert≡li  : self ^∙ qcCertifiedBlock ≡ self ^∙ qcLedgerInfo ∙ liwsLedgerInfo ∙ liCommitInfo
        noSigs   : Map.kvm-size (self ^∙ qcLedgerInfo ∙ liwsSignatures) ≡ 0
  open rnd≡0Props

  record rnd≢0Props : Set where
    field
      sigProp : LedgerInfoWithSignatures.verifySignatures (self ^∙ qcLedgerInfo) vv ≡ Right unit
      vdProp  : VoteDataProps.Contract (self ^∙ qcVoteData)
  open rnd≢0Props

  ParentProps : Dec (self ^∙ qcCertifiedBlock ∙ biRound ≡ 0) → Set
  ParentProps (yes _) = rnd≡0Props
  ParentProps (no  _) = rnd≢0Props

  record Contract : Set where
    field
      lihash≡ : self ^∙ qcSignedLedgerInfo ∙ liwsLedgerInfo ∙ liConsensusDataHash ≡ voteHash
      rnd≟0   : Dec (self ^∙ qcCertifiedBlock ∙ biRound ≡ 0)
      parProp : ParentProps rnd≟0
  open Contract

  contract : ∀ (r : Either ErrLog Unit) → r ≡ Right unit
           → QuorumCert.verify self vv ≡ r
           → Contract
  contract (Left fakeErr)
     with (self ^∙ qcSignedLedgerInfo ∙ liwsLedgerInfo ∙ liConsensusDataHash) ≟Hash
          (hashVD (self ^∙ qcVoteData))
  ...| no neq = λ ()
  ...| yes refl
     with self ^∙ qcCertifiedBlock ∙ biRound ≟ 0
  ...| yes refl
     with (self ^∙ qcParentBlock) ≟-BlockInfo (self ^∙ qcCertifiedBlock)
  ...| no neq = λ ()
  ...| yes refl
     with (self ^∙ qcCertifiedBlock) ≟-BlockInfo (self ^∙ qcLedgerInfo ∙ liwsLedgerInfo ∙ liCommitInfo)
  ...| no neq = λ ()
  ...| yes refl
     with Map.kvm-size (self ^∙ qcLedgerInfo ∙ liwsSignatures) ≟ 0
  ...| yes noSigs = λ ()

  contract (Right unit)
     with (self ^∙ qcSignedLedgerInfo ∙ liwsLedgerInfo ∙ liConsensusDataHash) ≟Hash (hashVD (self ^∙ qcVoteData))
  ...| no neq = λ _ ()
  ...| yes refl
     with self ^∙ qcCertifiedBlock ∙ biRound ≟ 0
  ...| yes refl
     with (self ^∙ qcParentBlock) ≟-BlockInfo (self ^∙ qcCertifiedBlock)
  ...| no neq = λ _ ()
  ...| yes refl
     with (self ^∙ qcCertifiedBlock) ≟-BlockInfo (self ^∙ qcLedgerInfo ∙ liwsLedgerInfo ∙ liCommitInfo)
  ...| no neq = λ _ ()
  ...| yes refl
     with Map.kvm-size (self ^∙ qcLedgerInfo ∙ liwsSignatures) ≟ 0
  ...| yes noSigs = λ _ _ →
         record { lihash≡ = refl
                ; rnd≟0 = yes refl
                ; parProp = record { par≡cert = refl
                                   ; cert≡li = refl
                                   ; noSigs = noSigs } }
  contract (Right unit)
     | yes refl
     | no neq
     with  LedgerInfoWithSignatures.verifySignatures (self ^∙ qcLedgerInfo)  vv | inspect
          (LedgerInfoWithSignatures.verifySignatures (self ^∙ qcLedgerInfo)) vv
  ...| Left  err  | [ R ] = λ _ ()
  ...| Right unit | [ R ]
     with VoteData.verify (self ^∙ qcVoteData) | inspect
          VoteData.verify (self ^∙ qcVoteData)
  ...| Left err   | _ = λ _ ()
  ...| Right unit | [ R' ] = λ _ _ →
         record { lihash≡ = refl
                ; rnd≟0 = no neq
                ; parProp = record { sigProp = R
                                   ; vdProp = VoteDataProps.contract (self ^∙ qcVoteData) R' } }