text:
-- 2010-10-02, see issue 334

module TerminationInfiniteRecord where

record Empty : Set where
  inductive
  constructor empty
  field
    fromEmpty : Empty

elimEmpty : Empty -> Set
elimEmpty (empty e) = elimEmpty e

-- this no longer termination checks
-- and it should not, since it is translated to
-- elimEmpty e' = elimEmpty (fromEmpty e')

ext: agda

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Implications of nullary relations
------------------------------------------------------------------------

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

module Relation.Nullary.Implication where

open import Relation.Nullary
open import Data.Empty

-- Some properties which are preserved by _→_.

infixr 2 _→-dec_

_→-dec_ : ∀ {p q} {P : Set p} {Q : Set q} →
          Dec P → Dec Q → Dec (P → Q)
yes p →-dec no ¬q = no  (λ f → ¬q (f p))
yes p →-dec yes q = yes (λ _ → q)
no ¬p →-dec _     = yes (λ p → ⊥-elim (¬p p))


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

module LogicalFramework.UniversalQuantifier where

postulate D : Set

-- The universal quantifier type on D.
data ForAll (A : D → Set) : Set where
  dfun : ((t : D) → A t) → ForAll A

dapp : {A : D → Set}(t : D) → ForAll A → A t
dapp t (dfun f) = f t

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An alternative definition of mutually-defined lists and non-empty
-- lists, using the Kleene star and plus.
------------------------------------------------------------------------

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

module Data.List.Kleene where

------------------------------------------------------------------------
-- Types and basic operations

open import Data.List.Kleene.Base public


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Conversion
open import Definition.LogicalRelation.Substitution.Reduction
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.ProofIrrelevance
open import Definition.LogicalRelation.Substitution.MaybeEmbed
open import Definition.LogicalRelation.Substitution.Introductions.Nat
open import Definition.LogicalRelation.Substitution.Introductions.Natrec
open import Definition.LogicalRelation.Substitution.Introductions.Empty
open import Definition.LogicalRelation.Substitution.Introductions.Emptyrec
open import Definition.LogicalRelation.Substitution.Introductions.Universe
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.Sigma
open import Definition.LogicalRelation.Substitution.Introductions.Id
open import Definition.LogicalRelation.Substitution.Introductions.IdUPiPi
open import Definition.LogicalRelation.Substitution.Introductions.Cast
open import Definition.LogicalRelation.Substitution.Introductions.CastPi
open import Definition.LogicalRelation.Substitution.Introductions.Lambda
open import Definition.LogicalRelation.Substitution.Introductions.Application
open import Definition.LogicalRelation.Substitution.Introductions.Pair
open import Definition.LogicalRelation.Substitution.Introductions.Fst
open import Definition.LogicalRelation.Substitution.Introductions.Snd
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.Introductions.Transp
open import Definition.LogicalRelation.Fundamental.Variable
import Definition.LogicalRelation.Substitution.ProofIrrelevance as PI
import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Weakening

open import Tools.Product
open import Tools.Unit
open import Tools.Nat
import Tools.PropositionalEquality as PE

Idreflᵛ : ∀{Γ A l t}
  → ([Γ] : ⊩ᵛ Γ)
  → ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ^ [ ! , ι l ] / [Γ])
  → ([t] : Γ ⊩ᵛ⟨ ∞ ⟩ t ∷ A ^ [ ! , ι l ] / [Γ] / [A])
  → let [Id] = Idᵛ {A = A} {t = t} {u = t } [Γ] [A] [t] [t]
    in Γ ⊩ᵛ⟨ ∞ ⟩ Idrefl A t ∷ Id A t t ^ [ % , ι l ] / [Γ] / [Id]

Idreflᵛ {Γ} {A} {l} {t} [Γ] [A] [t]  =
  let [Id] = Idᵛ {A = A} {t = t} {u = t } [Γ] [A] [t] [t]
  in validityIrr {A = Id A t t} {t = Idrefl A t} [Γ] [Id] λ ⊢Δ [σ] → Idreflⱼ (escapeTerm (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ])))

castreflᵛ : ∀{Γ A t}
  → ([Γ] : ⊩ᵛ Γ)
  → ([UA] : Γ ⊩ᵛ⟨ ∞ ⟩ U ⁰ ^ [ ! , next ⁰ ] / [Γ])
  → ([A]ₜ : Γ ⊩ᵛ⟨ ∞ ⟩ A ∷ U ⁰ ^ [ ! , next ⁰ ] / [Γ] / [UA] )
  → ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ^ [ ! , ι ⁰ ] / [Γ])
  → ([t]ₜ : Γ ⊩ᵛ⟨ ∞ ⟩ t ∷ A ^ [ ! , ι ⁰ ] / [Γ] / [A])
  → let [Id] : Γ ⊩ᵛ⟨ ∞ ⟩ Id A t (cast ⁰ A A (Idrefl (U ⁰) A) t) ^ [ % , ι ⁰ ] / [Γ]
        [Id] = Idᵛ {A = A} {t = t} {u = cast ⁰ A A (Idrefl (U ⁰) A) t} [Γ] [A] [t]ₜ
                   (castᵗᵛ {A = A} {B = A} {t = t} {e = Idrefl (U ⁰) A} [Γ] [UA] [A]ₜ [A]ₜ [A] [A] [t]ₜ
                           (Idᵛ {A = U _} {t = A} {u = A} [Γ] [UA] [A]ₜ [A]ₜ)
                           (Idreflᵛ {A = U _} {t = A} [Γ] [UA] [A]ₜ))
    in Γ ⊩ᵛ⟨ ∞ ⟩ castrefl A t ∷ Id A t (cast ⁰ A A (Idrefl (U ⁰) A) t) ^ [ % , ι ⁰ ] / [Γ] / [Id]

castreflᵛ {Γ} {A} {t} [Γ] [UA] [A]ₜ [A] [t]ₜ =
  let [Id] : Γ ⊩ᵛ⟨ ∞ ⟩ Id A t (cast ⁰ A A (Idrefl (U ⁰) A) t) ^ [ % , ι ⁰ ] / [Γ]
      [Id] = Idᵛ {A = A} {t = t} {u = cast ⁰ A A (Idrefl (U ⁰) A) t} [Γ] [A] [t]ₜ
                 (castᵗᵛ {A = A} {B = A} {t = t} {e = Idrefl (U ⁰) A} [Γ] [UA] [A]ₜ [A]ₜ [A] [A] [t]ₜ
                 (Idᵛ {A = U _} {t = A} {u = A} [Γ] [UA] [A]ₜ [A]ₜ)
                 (Idreflᵛ {A = U _} {t = A} [Γ] [UA] [A]ₜ))
  in  validityIrr {A = Id A t (cast ⁰ A A (Idrefl (U ⁰) A) t)} {t = castrefl A t}
                  [Γ] [Id] λ ⊢Δ [σ] → castreflⱼ (escapeTerm (proj₁ ([UA] ⊢Δ [σ])) (proj₁ ([A]ₜ ⊢Δ [σ]))) (escapeTerm (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t]ₜ ⊢Δ [σ])))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-

This file contains:

- the coequalizer of sets as a HIT as performed in https://1lab.dev/Data.Set.Coequaliser.html

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.SetCoequalizer.Properties where

open import Cubical.HITs.SetCoequalizer.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Type ℓ
    B : Type ℓ'

-- Some helpful lemmas, similar to those in Cubical/HITs/SetQuotients/Properties.agda
elimProp : {f g : A → B} {C : SetCoequalizer f g → Type ℓ}
         → (Cprop : (x : SetCoequalizer f g) → isProp (C x))
         → (Cinc : (b : B) → C (inc b))
         → (x : SetCoequalizer f g) → C x
elimProp Cprop Cinc (inc x) = Cinc x
elimProp {f = f} {g = g} Cprop Cinc (coeq a i) =
  isProp→PathP (λ i → Cprop (coeq a i)) (Cinc (f a)) (Cinc (g a)) i
elimProp Cprop Cinc (squash x y p q i j) =
  isOfHLevel→isOfHLevelDep
    2 (λ x → isProp→isSet (Cprop x)) (g x) (g y) (cong g p) (cong g q) (squash x y p q) i j
  where
  g = elimProp Cprop Cinc

elimProp2 : {A' : Type ℓ} {B' : Type ℓ'} {f g : A → B} {f' g' : A' → B'}
            {C : SetCoequalizer f g → SetCoequalizer f' g' → Type (ℓ-max ℓ ℓ')}
          → (Cprop : (x : SetCoequalizer f g) → (y : SetCoequalizer f' g') → isProp (C x y))
          → (Cinc : (b : B) → (b' : B') → C (inc b) (inc b'))
          → (x : SetCoequalizer f g) → (y : SetCoequalizer f' g') → C x y
elimProp2 Cprop Cinc = elimProp (λ x → isPropΠ (λ y → Cprop x y))
                                (λ x → elimProp (λ y → Cprop (inc x) y) (Cinc x))

elimProp3 : {A' A'' : Type ℓ} {B' B'' : Type ℓ'} {f g : A → B} {f' g' : A' → B'}
            {f'' g'' : A'' → B''}
            {C : SetCoequalizer f g → SetCoequalizer f' g' → SetCoequalizer f'' g''
               → Type (ℓ-max ℓ ℓ')}
          → (Cprop : (x : SetCoequalizer f g)
                   → (y : SetCoequalizer f' g')
                   → (z : SetCoequalizer f'' g'')
                   → isProp (C x y z))
          → (Cinc : (b : B) → (b' : B') → (b'' : B'') → C (inc b) (inc b') (inc b''))
          → (x : SetCoequalizer f g) → (y : SetCoequalizer f' g') → (z : SetCoequalizer f'' g'')
          → C x y z
elimProp3 Cprop Cinc = elimProp (λ x → isPropΠ2 (λ y z → Cprop x y z))
                                (λ x → elimProp2 (λ y z → Cprop (inc x) y z) (Cinc x))

rec : {C : Type ℓ''} {f g : A → B}
    → (Cset : (x y : C) → (p q : x ≡ y) → p ≡ q)
    → (h : B → C)
    → (hcoeqs : (a : A) → h (f a) ≡ h (g a))
    → SetCoequalizer f g → C
rec Cset h hcoeqs (inc x) = h x
rec Cset h hcoeqs (coeq a i) = hcoeqs a i
rec Cset h hcoeqs (squash x y p q i j) =
    Cset (g x) (g y) (λ i → g (p i)) (λ i → g (q i)) i j
  where g = rec Cset h hcoeqs

rec2 : {A' : Type ℓ} {B' : Type ℓ'} {C : Type ℓ''} {f g : A → B} {f' g' : A' → B'}
     → (Cset : (x y : C) → (p q : x ≡ y) → p ≡ q)
     → (h : B → B' → C)
     → (hcoeqsl : (a : A) (b' : B') → h (f a) b' ≡ h (g a) b')
     → (hcoeqsr : (a' : A') (b : B) → h b (f' a') ≡ h b (g' a'))
     → SetCoequalizer f g → SetCoequalizer f' g' → C
rec2 Cset h hcoeqsl hcoeqsr =
  rec
    (isSetΠ (λ _ → Cset))
    (λ b → rec Cset (λ b' → h b b') (λ a' → hcoeqsr a' b))
    (λ a → funExt (elimProp (λ _ → Cset _ _) (λ b' → hcoeqsl a b')))

module UniversalProperty where
  {- The proof of the universal property of the coequalizer of sets.

  A ==f=g==> B --inc--> SetCoequalizer f g
              \         .
                \       .
                  h   ∃! inducedHom
                    \   .
                      \ .
                        C
  commuting diagram
  -}
  inducedHom : {C : Type ℓ''} {f g : A → B}
             → (Cset : (x y : C) → (p q : x ≡ y) → p ≡ q)
             → (h : B → C)
             → (hcoeq : (a : A) → h (f a) ≡ h (g a))
             → SetCoequalizer f g → C
  inducedHom Cset h hcoeq = rec Cset h hcoeq

  commutativity : {C : Type ℓ''} {f g : A → B}
                → (Cset : (x y : C) → (p q : x ≡ y) → p ≡ q)
                → (h : B → C)
                → (hcoeq : (a : A) → h (f a) ≡ h (g a))
                → ((b : B) → h b ≡ inducedHom Cset h hcoeq (inc b))
  commutativity Cset h hcoeq = λ b → refl

  uniqueness : {C : Type ℓ''}
             → (f g : A → B)
             → (Cset : (x y : C) → (p q : x ≡ y) → p ≡ q)
             → (h : B → C)
             → (hcoeq : (a : A) → h (f a) ≡ h (g a))
             → (i : SetCoequalizer f g → C)
             → (icommutativity : (b : B) → h b ≡ i (inc b))
             → (i ≡ inducedHom Cset h hcoeq)
  uniqueness f g Cset h hcoeq i icommutativity = λ j x → q x j
    where q : (x : SetCoequalizer f g) → i x ≡ inducedHom Cset h hcoeq x
          q = elimProp
                (λ _ → Cset _ _)
                (λ b → i (inc b) ≡⟨ sym (icommutativity b) ⟩
                      h b       ≡⟨ refl ⟩
                      inducedHom Cset h hcoeq (inc b) ∎)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Qualified imported constructors
module Issue262 where

open import Common.Prelude

z = Nat.zero

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2016-10-09, issue #2223

-- The level constraint solver needs to combine constraints
-- from different contexts and modules.
-- The parameter refinement broke this test case.

-- {-# OPTIONS -v tc.with.top:25 #-}
-- {-# OPTIONS -v tc.conv.nat:40 #-}
-- {-# OPTIONS -v tc.constr.add:45 #-}

open import Common.Level

module _ (a ℓ : Level) where

module Function where

  mutual
    X : Level
    X = _  -- Agda 2.5.1.1 solves this level meta

    X<=a : Set (X ⊔ a) → Set a
    X<=a A = A

    test : Set₁
    test with (lsuc ℓ)
    ... | _ = Set

      where
        a<=X : Set (X ⊔ a) → Set X
        a<=X A = A

-- Should solve all metas.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module PiLevel0 where

-- We refine the trivial relation used in level-(-2). We do not
-- identify all types: only those of the same "size". So between any
-- two types, there could be zero, one, or many identifications. If
-- there is more than one idenfication we force them to be the same;
-- so 'id' and 'not' at BOOL ⟷ BOOL are the same and U effectively
-- collapses to the set of natural numbers

open import Data.Unit using (⊤; tt)
open import Data.Nat using (ℕ)
open import Relation.Binary.Core using (IsEquivalence)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong₂; module ≡-Reasoning)

open import PiU using (U; ZERO; ONE; PLUS; TIMES; toℕ)

infix  30 _⟷_
infixr 50 _◎_

------------------------------------------------------------------------------
-- Level 0 of Pi

-- Abbreviation

size : U → ℕ
size = toℕ

-- Combinators

data _⟷_ : U → U → Set where
  unite₊l : {t : U} → PLUS ZERO t ⟷ t
  uniti₊l : {t : U} → t ⟷ PLUS ZERO t
  unite₊r : {t : U} → PLUS t ZERO ⟷ t
  uniti₊r : {t : U} → t ⟷ PLUS t ZERO
  swap₊   : {t₁ t₂ : U} → PLUS t₁ t₂ ⟷ PLUS t₂ t₁
  assocl₊ : {t₁ t₂ t₃ : U} → PLUS t₁ (PLUS t₂ t₃) ⟷ PLUS (PLUS t₁ t₂) t₃
  assocr₊ : {t₁ t₂ t₃ : U} → PLUS (PLUS t₁ t₂) t₃ ⟷ PLUS t₁ (PLUS t₂ t₃)
  unite⋆l  : {t : U} → TIMES ONE t ⟷ t
  uniti⋆l  : {t : U} → t ⟷ TIMES ONE t
  unite⋆r : {t : U} → TIMES t ONE ⟷ t
  uniti⋆r : {t : U} → t ⟷ TIMES t ONE
  swap⋆   : {t₁ t₂ : U} → TIMES t₁ t₂ ⟷ TIMES t₂ t₁
  assocl⋆ : {t₁ t₂ t₃ : U} → TIMES t₁ (TIMES t₂ t₃) ⟷ TIMES (TIMES t₁ t₂) t₃
  assocr⋆ : {t₁ t₂ t₃ : U} → TIMES (TIMES t₁ t₂) t₃ ⟷ TIMES t₁ (TIMES t₂ t₃)
  absorbr : {t : U} → TIMES ZERO t ⟷ ZERO
  absorbl : {t : U} → TIMES t ZERO ⟷ ZERO
  factorzr : {t : U} → ZERO ⟷ TIMES t ZERO
  factorzl : {t : U} → ZERO ⟷ TIMES ZERO t
  dist    : {t₁ t₂ t₃ : U} →
            TIMES (PLUS t₁ t₂) t₃ ⟷ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)
  factor  : {t₁ t₂ t₃ : U} →
            PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) ⟷ TIMES (PLUS t₁ t₂) t₃
  distl   : {t₁ t₂ t₃ : U } →
            TIMES t₁ (PLUS t₂ t₃) ⟷ PLUS (TIMES t₁ t₂) (TIMES t₁ t₃)
  factorl : {t₁ t₂ t₃ : U } →
            PLUS (TIMES t₁ t₂) (TIMES t₁ t₃) ⟷ TIMES t₁ (PLUS t₂ t₃)
  id⟷    : {t : U} → t ⟷ t
  _◎_     : {t₁ t₂ t₃ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (PLUS t₁ t₂ ⟷ PLUS t₃ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (TIMES t₁ t₂ ⟷ TIMES t₃ t₄)

-- At the next level we have a trivial equivalence that equates all
-- morphisms of the same type so for example id and not : BOOL ⟷ BOOL
-- are equated

triv≡ : {t₁ t₂ : U} → (f g : t₁ ⟷ t₂) → Set
triv≡ _ _ = ⊤

triv≡Equiv : {t₁ t₂ : U} → IsEquivalence (triv≡ {t₁} {t₂})
triv≡Equiv = record
  { refl = tt
  ; sym = λ _ → tt
  ; trans = λ _ _ → tt
  }

------------------------------------------------------------------------------
-- Every combinator has an inverse. There are actually many
-- syntactically different inverses but they are all equivalent.

! : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
! unite₊l   = uniti₊l
! uniti₊l   = unite₊l
! unite₊r   = uniti₊r
! uniti₊r   = unite₊r
! swap₊     = swap₊
! assocl₊   = assocr₊
! assocr₊   = assocl₊
! unite⋆l   = uniti⋆l
! uniti⋆l   = unite⋆l
! unite⋆r   = uniti⋆r
! uniti⋆r   = unite⋆r
! swap⋆     = swap⋆
! assocl⋆   = assocr⋆
! assocr⋆   = assocl⋆
! absorbl   = factorzr
! absorbr   = factorzl
! factorzl  = absorbr
! factorzr  = absorbl
! dist      = factor
! factor    = dist
! distl     = factorl
! factorl   = distl
! id⟷       = id⟷
! (c₁ ◎ c₂) = ! c₂ ◎ ! c₁
! (c₁ ⊕ c₂) = (! c₁) ⊕ (! c₂)
! (c₁ ⊗ c₂) = (! c₁) ⊗ (! c₂)

!! : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → triv≡ (! (! c)) c
!! = tt

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module BabyAgda where
data Nat : Set where
    zero : Nat
    suc : Nat -> Nat
    stuff : Nat

nonDependent : Nat -> Nat -> Nat
nonDependent a b = a

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

asdf : {A : Set} -> {B : Nat} -> {renameMe0 : Nat} -> Nat
asdf {_} {_} {zero} = zero
asdf {_} {_} {suc c} = dependent c


text:
-- Andreas, 2016-06-01, issue 1999

-- Bug in TypeChecking.Signature.applySection
-- If that function was not such horrible spaghetti code,
-- there would be less bugs like this.
-- Bug was: code for applying projection used ts instead of ts'

-- {-# OPTIONS -v tc.mod.apply:80 #-}

module Issue1999 where

import Common.Product as P using (_×_ ; proj₂)

module One (A : Set) where
  open P public

module Two (A : Set) where
  module M = One A

  myproj : A M.× A → A
  myproj p = M.proj₂ p

-- WAS: Internal error in Substitute (projection applied to lambda)
-- Should work.


text:
module DTGP.Rand where
open import Data.Nat
open import Relation.Nullary.Decidable
open import Data.Nat.DivMod renaming (_mod_ to _nmod_)
open import Data.Fin
open import Data.Product
open import DTGP.State public

postulate Int : Set
{-# BUILTIN INTEGER Int #-}

primitive
  primIntegerPlus     : Int → Int → Int
  primIntegerMinus    : Int → Int → Int
  primIntegerTimes    : Int → Int → Int
  primIntegerDiv      : Int → Int → Int  -- partial
  primIntegerMod      : Int → Int → Int  -- partial
  primIntegerAbs      : Int → ℕ
  primNatToInteger    : ℕ → Int

multiplier : Int
multiplier = primNatToInteger 25173

incrementer : Int
incrementer = primNatToInteger 13849

modulus : Int
modulus = primNatToInteger 65536

nextRand : ℕ → ℕ
nextRand nat =
  let n = primNatToInteger nat
      product = primIntegerTimes n multiplier
      sum = primIntegerPlus product incrementer
      remainder = primIntegerMod sum modulus
  in primIntegerAbs remainder

calcRand : ℕ → ℕ × ℕ
calcRand n with nextRand n
... | next = next , next

rand : State ℕ ℕ
rand = state calcRand

Rand : Set → Set
Rand A = State ℕ A

runRand :  ∀ {A} → Rand A → ℕ → A
runRand st seed = proj₁ (runState st seed)

primNatMod : (dividend divisor : ℕ) → ℕ
primNatMod dividend zero = zero
primNatMod dividend (suc n) =
  let x = primNatToInteger dividend
      y = primNatToInteger (suc n)
      z = primIntegerMod x y
      nat = primIntegerAbs z
  in nat

_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
_mod_ m n {p} = _nmod_ (primNatMod m n) n {p}

max_stars_repo_name: larrytheliquid/dtgp

max_issues_repo_name: larrytheliquid/dtgp

max_forks_repo_name: larrytheliquid/dtgp


text:
open import Agda.Builtin.Equality

postulate
   A : Set

Phantom : A → Set
Phantom _ = A

postulate
  rigid : A → A

mutual
  X : A → A → A → A
  X = _

  Y : (x y : A) → Phantom x
  Y = _

  -- This constraint triggers pruning of X in an attempt to remove the non-linearity.
  -- It doesn't get rid of the non-linearity but prunes x setting X x y z := Z y z,
  -- for a fresh meta Z.
  c₁ : (x y : A) → X x y y ≡ rigid y
  c₁ x y = refl

  -- Here we end up with Z y z == rigid (Y x y) which requires pruning x from Y. This
  -- fails due to the phantom dependency on x in the type of Y and the constraint is
  -- left unsolved. If we hadn't pruned x from X we could have solved this with
  -- X x y z := rigid (Y x y), turning the first constraint into rigid (Y x y) == rigid y,
  -- which is solved by Y x y := y.
  c₂ : (x y z : A) → X x y z ≡ rigid (Y x y)
  c₂ x y z =  refl


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

module Data.Empty where

open import Data.Empty.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- Andreas, 2021-04-14, #1154
-- Andreas, 2021-04-10, BNFC/bnfc#354
-- Make sure we do not "resurrect" superseded layout columns.

private private private
  A : Set                -- OK, stacking
        B : Set          -- Bad, should fail

-- Expected: Parse error after B


text:
------------------------------------------------------------------------
-- Lemmas related to expansion and CCS
------------------------------------------------------------------------

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

open import Prelude hiding (module W; step-→)

module Expansion.CCS {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import Prelude.Size

open import Function-universe equality-with-J hiding (id; _∘_)

import Bisimilarity.CCS as SL
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
import Expansion.Equational-reasoning-instances
open import Labelled-transition-system.CCS Name
open import Relation

open import Bisimilarity CCS as S using (_∼_)
open import Bisimilarity.Weak CCS as W using (_≈_; force)
open import Expansion CCS
import Labelled-transition-system.Equational-reasoning-instances CCS
  as Dummy

-- Some lemmas used to prove the congruence lemmas below as well as
-- similar results in Bisimilarity.Weak.CCS.

module Cong-lemmas
  ({R} R′ : Proc ∞ → Proc ∞ → Type ℓ)
  ⦃ _ : Reflexive R′ ⦄
  ⦃ _ : Convertible R R′ ⦄
  ⦃ _ : Convertible R′ R′ ⦄
  ⦃ _ : Transitive′ R′ _∼_ ⦄
  ⦃ _ : Transitive _∼_ R′ ⦄
  {_[_]↝_ : Proc ∞ → Label → Proc ∞ → Type ℓ}
  (right-to-left :
   ∀ {P Q} → R P Q →
   ∀ {Q′ μ} → Q [ μ ]⟶ Q′ → ∃ λ P′ → P [ μ ]↝ P′ × R′ P′ Q′)
  ⦃ _ : ∀ {μ} → Convertible _[ μ ]↝_ _[ μ ]↝_ ⦄
  ⦃ _ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]↝_ ⦄
  (↝→[]⇒ : ∀ {P Q a} → P [ name a ]↝ Q → P [ name a ]⇒ Q)
  ([]⇒→↝ : ∀ {P Q} → P [ τ ]⇒ Q → P [ τ ]↝ Q)
  (map-↝ :
    {F : Proc ∞ → Proc ∞} →
    (∀ {P P′ μ} → P [ μ ]⟶ P′ → F P [ μ ]⟶ F P′) →
    ∀ {P P′ μ} → P [ μ ]↝ P′ → F P [ μ ]↝ F P′)
  (map-↝′ :
    ∀ {μ} {F : Proc ∞ → Proc ∞} →
    (∀ {P P′ μ} → Silent μ → P [ μ ]⟶ P′ → F P [ μ ]⟶ F P′) →
    (∀ {P P′} → P [ μ ]⟶ P′ → F P [ μ ]⟶ F P′) →
    ∀ {P P′} → P [ μ ]↝ P′ → F P [ μ ]↝ F P′)
  (zip-↝ :
    {F : Proc ∞ → Proc ∞ → Proc ∞} →
    (∀ {P P′ Q μ} → P [ μ ]⟶ P′ → F P Q [ μ ]⟶ F P′ Q) →
    (∀ {P Q Q′ μ} → Q [ μ ]⟶ Q′ → F P Q [ μ ]⟶ F P Q′) →
    ∀ {μ₁ μ₂ μ₃} →
    (Silent μ₁ → Silent μ₂ → Silent μ₃) →
    (∀ {P P′ Q} → P [ μ₁ ]⟶ P′ → Silent μ₂ → F P Q [ μ₃ ]⟶ F P′ Q) →
    (∀ {P Q Q′} → Silent μ₁ → Q [ μ₂ ]⟶ Q′ → F P Q [ μ₃ ]⟶ F P Q′) →
    (∀ {P P′ Q Q′} →
     P [ μ₁ ]⟶ P′ → Q [ μ₂ ]⟶ Q′ → F P Q [ μ₃ ]⟶ F P′ Q′) →
    ∀ {P P′ Q Q′} →
    P [ μ₁ ]↝ P′ → Q [ μ₂ ]↝ Q′ → F P Q [ μ₃ ]↝ F P′ Q′)
  (!-lemma :
    (∀ {P Q μ} → P [ μ ]⇒ Q → ! P [ μ ]⇒ ! P ∣ Q) →
    ∀ {P Q μ} → P [ μ ]↝ Q →
    ∃ λ P′ → ((! P) [ μ ]↝ P′) × P′ ∼ ! P ∣ Q)
  where

  private

    infix -3 rl-result-↝

    rl-result-↝ : ∀ {P P′ Q′} μ → P [ μ ]↝ P′ → R′ P′ Q′ →
                  ∃ λ P′ → (P [ μ ]↝ P′) × R′ P′ Q′
    rl-result-↝ _ P↝P′ P′≳′Q′ = _ , P↝P′ , P′≳′Q′

    syntax rl-result-↝ μ P↝P′ P′≳′Q′ = P↝P′ ↝[ μ ] P′≳′Q′

  ∣-cong :
    (∀ {P P′ Q Q′} → R′ P P′ → R′ Q Q′ → R′ (P ∣ Q) (P′ ∣ Q′)) →
    ∀ {P₁ P₂ Q₁ Q₂ R₂ μ} →
    R P₁ P₂ → R Q₁ Q₂ → P₂ ∣ Q₂ [ μ ]⟶ R₂ →
    ∃ λ R₁ → ((P₁ ∣ Q₁) [ μ ]↝ R₁) × R′ R₁ R₂
  ∣-cong _∣-cong′_ P₁≳P₂ Q₁≳Q₂ = λ where
    (par-left  tr)  → Σ-map (_∣ _)
                        (Σ-map (map-↝ par-left)
                               (_∣-cong′ convert Q₁≳Q₂))
                        (right-to-left P₁≳P₂ tr)
    (par-right tr)  → Σ-map (_ ∣_)
                        (Σ-map (map-↝ par-right)
                               (convert P₁≳P₂ ∣-cong′_))
                        (right-to-left Q₁≳Q₂ tr)
    (par-τ tr₁ tr₂) → Σ-zip _∣_
                        (Σ-zip (zip-↝ par-left par-right
                                      (λ ()) (λ _ ()) (λ ())
                                      par-τ)
                               _∣-cong′_)
                        (right-to-left P₁≳P₂ tr₁)
                        (right-to-left Q₁≳Q₂ tr₂)

  ·-cong :
    ∀ {P₁ P₂ Q₂ μ μ′} →
    R′ (force P₁) (force P₂) → μ · P₂ [ μ′ ]⟶ Q₂ →
    ∃ λ Q₁ → ((μ · P₁) [ μ′ ]↝ Q₁) × R′ Q₁ Q₂
  ·-cong P₁≳P₂ action = _ , convert (⟶: action) , P₁≳P₂

  ⟨ν⟩-cong :
    (∀ {a P P′} → R′ P P′ → R′ (⟨ν a ⟩ P) (⟨ν a ⟩ P′)) →
    ∀ {a μ P P′ Q′} →
    R P P′ → ⟨ν a ⟩ P′ [ μ ]⟶ Q′ →
    ∃ λ Q → (⟨ν a ⟩ P [ μ ]↝ Q) × R′ Q Q′
  ⟨ν⟩-cong ⟨ν⟩-cong′ {a} {μ} {P} P≳P′
           (restriction {P′ = Q′} a∉μ P′⟶Q′) =
    case right-to-left P≳P′ P′⟶Q′ of λ where
      (Q , P↝Q , Q≳′Q′) →
        ⟨ν a ⟩ P   →⟨ map-↝′ (restriction ∘ ∉τ) (restriction a∉μ) P↝Q ⟩■
          ↝[ μ ]
        ⟨ν a ⟩ Q   ∼⟨ ⟨ν⟩-cong′ Q≳′Q′ ⟩■
        ⟨ν a ⟩ Q′

  !-cong-lemma₁ : ∀ {P Q μ} → P [ μ ]⇒ Q → ! P [ μ ]⇒ ! P ∣ Q
  !-cong-lemma₁ {P} {Q} {μ} = λ where
    (steps {q′ = Q′} done P⟶Q′ Q′⇒Q) →
      ! P       [ μ ]⇒⟨ replication (par-right P⟶Q′) ⟩
      ! P ∣ Q′  →⟨ map-⇒ par-right Q′⇒Q ⟩■
      ! P ∣ Q

    (steps {p′ = P″} {q′ = Q′}
           (step {q = P′} {μ = μ′} μ′s P⟶P′ P′⇒P″)
           P″⟶Q′ Q′⇒Q) →
      ! P       →⟨ ⟶→⇒ μ′s (replication (par-right P⟶P′)) ⟩
      ! P ∣ P′  →⟨ map-⇒ par-right P′⇒P″ ⟩
      ! P ∣ P″  [ μ ]⇒⟨ par-right P″⟶Q′ ⟩
      ! P ∣ Q′  →⟨ map-⇒ par-right Q′⇒Q ⟩■
      ! P ∣ Q

  !-cong-lemma₂ :
    ∀ {P Q₁ Q₂ a} →
    P [ name a ]⇒ Q₁ → P [ name (co a) ]⇒ Q₂ →
    ∃ λ R → ! P [ τ ]⇒ R × R ∼ (! P ∣ Q₁) ∣ Q₂
  !-cong-lemma₂ {P} {Q₁} {Q₂} {a} = λ where
    (steps {q′ = Q₁′} done P⟶Q₁′ Q₁′⇒Q₁)
      (steps {q′ = Q₂′} done P⟶Q₂′ Q₂′⇒Q₂) →
        _
      , (! P                [ τ ]⇒⟨ replication (par-τ (replication (par-right P⟶Q₁′)) P⟶Q₂′) ⟩
         (! P ∣ Q₁′) ∣ Q₂′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right Q₁′⇒Q₁) Q₂′⇒Q₂ ⟩■
         (! P ∣ Q₁) ∣ Q₂)
      , reflexive

    (steps {q′ = Q₁′} done P⟶Q₁′ Q₁′⇒Q₁)
      (steps {p′ = P₂″} {q′ = Q₂′}
             (step {q = P₂′} {μ = μ} μs P⟶P₂′ P₂′⇒P₂″)
             P₂″⟶Q₂′ Q₂′⇒Q₂) →
        _
      , (! P                →⟨ ⟶→⇒ μs (replication (par-right P⟶P₂′)) ⟩
         ! P ∣ P₂′          →⟨ map-⇒ par-right P₂′⇒P₂″ ⟩
         ! P ∣ P₂″          [ τ ]⇒⟨ par-τ (replication (par-right P⟶Q₁′)) P₂″⟶Q₂′ ⟩
         (! P ∣ Q₁′) ∣ Q₂′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right Q₁′⇒Q₁) Q₂′⇒Q₂ ⟩■
         (! P ∣ Q₁) ∣ Q₂)
      , reflexive

    (steps {p′ = P₁″} {q′ = Q₁′}
           (step {q = P₁′} {μ = μ} μs P⟶P₁′ P₁′⇒P₁″)
           P₁″⟶Q₁′ Q₁′⇒Q₁)
      (steps {q′ = Q₂′} done P⟶Q₂′ Q₂′⇒Q₂) →
        _
      , (! P                →⟨ ⟶→⇒ μs (replication (par-right P⟶P₁′)) ⟩
         ! P ∣ P₁′          →⟨ map-⇒ par-right P₁′⇒P₁″ ⟩
         ! P ∣ P₁″          [ τ ]⇒⟨ par-τ′ (sym $ co-involutive a) (replication (par-right P⟶Q₂′)) P₁″⟶Q₁′ ⟩
         (! P ∣ Q₂′) ∣ Q₁′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right Q₂′⇒Q₂) Q₁′⇒Q₁ ⟩■
         (! P ∣ Q₂) ∣ Q₁)
      , ((! P ∣ Q₂) ∣ Q₁  ∼⟨ SL.swap-rightmost ⟩■
         (! P ∣ Q₁) ∣ Q₂)

    (steps {p′ = P₁″} {q′ = Q₁′}
           (step {q = P₁′} {μ = μ₁} μ₁s P⟶P₁′ P₁′⇒P₁″)
           P₁″⟶Q₁′ Q₁′⇒Q₁)
      (steps {p′ = P₂″} {q′ = Q₂′}
             (step {q = P₂′} {μ = μ₂} μ₂s P⟶P₂′ P₂′⇒P₂″)
             P₂″⟶Q₂′ Q₂′⇒Q₂) →
        _
      , (! P                →⟨ ⟶→⇒ μ₂s (replication (par-right P⟶P₂′)) ⟩
         ! P ∣ P₂′          →⟨ ⟶→⇒ μ₁s (par-left (replication (par-right P⟶P₁′))) ⟩
         (! P ∣ P₁′) ∣ P₂′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right P₁′⇒P₁″) P₂′⇒P₂″ ⟩
         (! P ∣ P₁″) ∣ P₂″  [ τ ]⇒⟨ par-τ (par-right P₁″⟶Q₁′) P₂″⟶Q₂′ ⟩
         (! P ∣ Q₁′) ∣ Q₂′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right Q₁′⇒Q₁) Q₂′⇒Q₂ ⟩■
         (! P ∣ Q₁) ∣ Q₂)
      , reflexive

  !-cong :
    (∀ {P P′ Q Q′} → R′ P P′ → R′ Q Q′ → R′ (P ∣ Q) (P′ ∣ Q′)) →
    (∀ {P P′} → R′ P P′ → R′ (! P) (! P′)) →
    ∀ {P P′ Q′ μ} →
    R P P′ → ! P′ [ μ ]⟶ Q′ →
    ∃ λ Q → ((! P) [ μ ]↝ Q) × R′ Q Q′
  !-cong _∣-cong′_ !-cong′_ {P} {P′} {Q′} {μ} P≳P′ !P′⟶Q′ =
    case SL.6-1-3-2 !P′⟶Q′ of λ where

      (inj₁ (P″ , P′⟶P″ , Q′∼!P′∣P″)) →
        let Q , P↝Q  , Q≳′P″  = right-to-left P≳P′ P′⟶P″
            R , !P↝R , R∼!P∣Q = !-lemma !-cong-lemma₁ P↝Q
        in
          ! P        →⟨ !P↝R ⟩■
            ↝[ μ ]
          R          ∼⟨ R∼!P∣Q ⟩
          ! P ∣ Q    ∼′⟨ (!-cong′ (convert P≳P′)) ∣-cong′ Q≳′P″ ⟩
          ! P′ ∣ P″  ∼⟨ symmetric Q′∼!P′∣P″ ⟩■
          Q′

      (inj₂ (refl , P″ , P‴ , a , P′⟶P″ , P′⟶P‴ , Q′∼!P′∣P″∣P‴)) →
        let Q₁ , P↝Q₁ , Q₁≳′P″ = right-to-left P≳P′ P′⟶P″
            Q₂ , P↝Q₂ , Q₂≳′P‴ = right-to-left P≳P′ P′⟶P‴

            R , !P⇒R , R∼[!P∣Q₁]∣Q₂ =
              !-cong-lemma₂ (↝→[]⇒ P↝Q₁) (↝→[]⇒ P↝Q₂)
        in
          ! P               →⟨ []⇒→↝ !P⇒R ⟩■
            ↝[ τ ]
          R                 ∼⟨ R∼[!P∣Q₁]∣Q₂ ⟩
          (! P ∣ Q₁) ∣ Q₂   ∼′⟨ ((!-cong′ (convert P≳P′)) ∣-cong′ Q₁≳′P″) ∣-cong′ Q₂≳′P‴ ⟩
          (! P′ ∣ P″) ∣ P‴  ∼⟨ symmetric Q′∼!P′∣P″∣P‴ ⟩■
          Q′

  ⊕·-cong :
    ∀ {P Q Q′ S′ μ μ′} →
    R′ (force Q) (force Q′) → P ⊕ μ · Q′ [ μ′ ]⟶ S′ →
    ∃ λ S → ((P ⊕ μ · Q) [ μ′ ]↝ S) × R′ S S′
  ⊕·-cong {P} {Q} {Q′} {S′} {μ} {μ′} Q≳Q′ = λ where
    (sum-left P⟶S′) →
      P ⊕ μ · Q  →⟨ ⟶: sum-left P⟶S′ ⟩■
        ↝[ μ′ ]
      S′         ■

    (sum-right action) →
      P ⊕ μ · Q  →⟨ ⟶: sum-right action ⟩■
        ↝[ μ ]
      force Q    ∼⟨ Q≳Q′ ⟩■
      force Q′

  ·⊕·-cong :
    ∀ {μ₁ μ₂ P₁ P₁′ P₂ P₂′ S′ μ} →
    R′ (force P₁) (force P₁′) → R′ (force P₂) (force P₂′) →
    μ₁ · P₁′ ⊕ μ₂ · P₂′ [ μ ]⟶ S′ →
    ∃ λ S → ((μ₁ · P₁ ⊕ μ₂ · P₂) [ μ ]↝ S) × R′ S S′
  ·⊕·-cong {μ₁} {μ₂} {P₁} {P₁′} {P₂} {P₂′} P₁≳P₁′ P₂≳P₂′ = λ where
    (sum-left action) →
      μ₁ · P₁ ⊕ μ₂ · P₂  →⟨ ⟶: sum-left action ⟩■
        ↝[ μ₁ ]
      force P₁           ∼⟨ P₁≳P₁′ ⟩■
      force P₁′

    (sum-right action) →
      μ₁ · P₁ ⊕ μ₂ · P₂  →⟨ ⟶: sum-right action ⟩■
        ↝[ μ₂ ]
      force P₂           ∼⟨ P₂≳P₂′ ⟩■
      force P₂′

private
  module CL {i} =
    Cong-lemmas
      [ i ]_≳′_ right-to-left id id
      map-[]⇒ map-[]⇒′ (λ f g _ _ _ → zip-[]⇒ f g)
      (λ hyp P⇒Q → _ , hyp P⇒Q , reflexive)

mutual

  -- _∣_ preserves the expansion relation.

  infix 6 _∣-cong_ _∣-cong′_

  _∣-cong_ : ∀ {i P P′ Q Q′} →
             [ i ] P ≳ P′ → [ i ] Q ≳ Q′ → [ i ] P ∣ Q ≳ P′ ∣ Q′
  _∣-cong_ {i} P≳P′ Q≳Q′ =
    ⟨ lr P≳P′ Q≳Q′
    , CL.∣-cong _∣-cong′_ P≳P′ Q≳Q′
    ⟩
    where
    lr : ∀ {P P′ Q Q′ R μ} →
         [ i ] P ≳ P′ → [ i ] Q ≳ Q′ → P ∣ Q [ μ ]⟶ R →
         ∃ λ R′ → P′ ∣ Q′ [ μ ]⟶̂ R′ × [ i ] R ≳′ R′
    lr P≳P′ Q≳Q′ (par-left  tr)  = Σ-map (_∣ _)
                                         (Σ-map (map-⟶̂ par-left)
                                                (_∣-cong′ convert {a = ℓ} Q≳Q′))
                                     (left-to-right P≳P′ tr)
    lr P≳P′ Q≳Q′ (par-right tr)  = Σ-map (_ ∣_)
                                         (Σ-map (map-⟶̂ par-right)
                                                (convert {a = ℓ} P≳P′ ∣-cong′_))
                                     (left-to-right Q≳Q′ tr)
    lr P≳P′ Q≳Q′ (par-τ tr₁ tr₂) = Σ-zip _∣_
                                         (Σ-zip (zip-⟶̂ (λ ()) (λ _ ())
                                                       (λ ()) par-τ)
                                                _∣-cong′_)
                                     (left-to-right P≳P′ tr₁)
                                     (left-to-right Q≳Q′ tr₂)

  _∣-cong′_ : ∀ {i P P′ Q Q′} →
              [ i ] P ≳′ P′ → [ i ] Q ≳′ Q′ → [ i ] P ∣ Q ≳′ P′ ∣ Q′
  force (P≳P′ ∣-cong′ Q≳Q′) = force P≳P′ ∣-cong force Q≳Q′

-- _·_ preserves the expansion relation.

infix 12 _·-cong_ _·-cong′_

_·-cong_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ≳′ force P′ → [ i ] μ · P ≳ μ′ · P′
_·-cong_ {i} {μ} {P = P} {P′} refl P≳P′ = ⟨ lr , CL.·-cong P≳P′ ⟩
  where
  lr : ∀ {Q μ″} →
       μ · P [ μ″ ]⟶ Q →
       ∃ λ Q′ → μ · P′ [ μ″ ]⟶̂ Q′ × [ i ] Q ≳′ Q′
  lr action = _ , ⟶→⟶̂ action , P≳P′

_·-cong′_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ≳′ force P′ → [ i ] μ · P ≳′ μ′ · P′
force (μ≡μ′ ·-cong′ P≳P′) = μ≡μ′ ·-cong P≳P′

-- _∙_ preserves the expansion relation.

infix 12 _∙-cong_ _∙-cong′_

_∙-cong_ : ∀ {i μ μ′ P P′} →
           μ ≡ μ′ → [ i ] P ≳ P′ → [ i ] μ ∙ P ≳ μ′ ∙ P′
refl ∙-cong P≳P′ = refl ·-cong convert {a = ℓ} P≳P′

_∙-cong′_ : ∀ {i μ μ′ P P′} →
            μ ≡ μ′ → [ i ] P ≳′ P′ → [ i ] μ ∙ P ≳′ μ′ ∙ P′
force (μ≡μ′ ∙-cong′ P≳P′) = μ≡μ′ ∙-cong force P≳P′

-- _∙ turns equal actions into processes related by the expansion
-- relation.

infix 12 _∙-cong _∙-cong′

_∙-cong : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ≳ μ′ ∙
refl ∙-cong = reflexive

_∙-cong′ : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ≳′ μ′ ∙
refl ∙-cong′ = reflexive

mutual

  -- ⟨ν_⟩ preserves the expansion relation.

  ⟨ν_⟩-cong : ∀ {i a a′ P P′} →
              a ≡ a′ → [ i ] P ≳ P′ → [ i ] ⟨ν a ⟩ P ≳ ⟨ν a′ ⟩ P′
  ⟨ν_⟩-cong {i} {a} {P = P} {P′} refl P≳P′ =
    ⟨ lr
    , CL.⟨ν⟩-cong ⟨ν refl ⟩-cong′ P≳P′
    ⟩
    where
    lr : ∀ {Q μ} →
         ⟨ν a ⟩ P [ μ ]⟶ Q →
         ∃ λ Q′ → ⟨ν a ⟩ P′ [ μ ]⟶̂ Q′ × [ i ] Q ≳′ Q′
    lr {μ = μ} (restriction {P′ = Q} a∉μ P⟶Q)
      with left-to-right P≳P′ P⟶Q
    ... | Q′ , step P′⟶Q′ , Q≳′Q′ =
      ⟨ν a ⟩ Q   ∼⟨ ⟨ν refl ⟩-cong′ Q≳′Q′ ⟩■
      ⟨ν a ⟩ Q′
        ⟵̂[ μ ]   ←⟨ ⟶: restriction a∉μ P′⟶Q′ ⟩■
      ⟨ν a ⟩ P′

    ... | _ , done μs , Q≳′P′ =
      ⟨ν a ⟩ Q   ∼⟨ ⟨ν refl ⟩-cong′ Q≳′P′ ⟩■
      ⟨ν a ⟩ P′
        ⟵̂[ μ ]   ←⟨ ⟶̂: done μs ⟩■
      ⟨ν a ⟩ P′

  ⟨ν_⟩-cong′ : ∀ {i a a′ P P′} →
               a ≡ a′ → [ i ] P ≳′ P′ → [ i ] ⟨ν a ⟩ P ≳′ ⟨ν a′ ⟩ P′
  force (⟨ν a≡a′ ⟩-cong′ P≳P′) = ⟨ν a≡a′ ⟩-cong (force P≳P′)

mutual

  -- !_ preserves the expansion relation.

  infix 10 !-cong_ !-cong′_

  !-cong_ : ∀ {i P P′} →
            [ i ] P ≳ P′ → [ i ] ! P ≳ ! P′
  !-cong_ {i} {P} {P′} P≳P′ =
    ⟨ lr
    , CL.!-cong _∣-cong′_ !-cong′_ P≳P′
    ⟩
    where
    lr : ∀ {Q μ} →
         ! P [ μ ]⟶ Q →
         ∃ λ Q′ → ! P′ [ μ ]⟶̂ Q′ × [ i ] Q ≳′ Q′
    lr {Q} {μ} !P⟶Q = case SL.6-1-3-2 !P⟶Q of λ where

      (inj₁ (P″ , P⟶P″ , Q∼!P∣P″)) → case left-to-right P≳P′ P⟶P″ of λ where
        (_ , done s , P″≳′P′) → case silent≡τ s of λ where
          refl →
              _
            , (! P′  ■)
            , (Q          ∼⟨ Q∼!P∣P″ ⟩
               ! P  ∣ P″  ∼′⟨ !-cong′ (convert {a = ℓ} P≳P′) ∣-cong′ P″≳′P′ ⟩ S.∼:
               ! P′ ∣ P′  ∼⟨ SL.6-1-2 ⟩■
               ! P′)

        (Q′ , step P′⟶Q′ , P″≳′Q′) →
            _
          , (! P′ ∣ Q′  ←⟨ ⟶: replication (par-right P′⟶Q′) ⟩■
             ! P′)
          , (Q          ∼⟨ Q∼!P∣P″ ⟩
             ! P  ∣ P″  ∼⟨ !-cong′ (convert {a = ℓ} P≳P′) ∣-cong′ P″≳′Q′ ⟩■
             ! P′ ∣ Q′)

      (inj₂ (refl , P″ , P‴ , a , P⟶P″ , P⟶P‴ , Q≳!P∣P″∣P‴)) →
        case left-to-right P≳P′ P⟶P″ ,′
             left-to-right P≳P′ P⟶P‴ of λ where
          ((Q′ , step P′⟶Q′ , P″≳′Q′) ,
           (Q″ , step P′⟶Q″ , P‴≳′Q″)) →
              _
            , ((! P′ ∣ Q′) ∣ Q″  ←⟨ ⟶: replication (par-τ (replication (par-right P′⟶Q′)) P′⟶Q″) ⟩■
               ! P′)
            , (Q                 ∼⟨ Q≳!P∣P″∣P‴ ⟩
               (! P ∣ P″) ∣ P‴   ∼⟨ (!-cong′ (convert {a = ℓ} P≳P′) ∣-cong′ P″≳′Q′) ∣-cong′ P‴≳′Q″ ⟩■
               (! P′ ∣ Q′) ∣ Q″)

          ((_ , done () , _) , _)
          (_ , (_ , done () , _))

  !-cong′_ : ∀ {i P P′} → [ i ] P ≳′ P′ → [ i ] ! P ≳′ ! P′
  force (!-cong′ P≳P′) = !-cong (force P≳P′)

-- It is not necessarily the case that, if P expands P′, then P ⊕ Q is
-- weakly bisimilar to P′ ⊕ Q (assuming that Name is inhabited).
--
-- I based the counterexample on one in "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.

¬⊕-congˡ-≳≈ : Name → ¬ (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≈ P′ ⊕ Q)
¬⊕-congˡ-≳≈ x =
  (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≈ P′ ⊕ Q)  ↝⟨ _$ τa≳a ⟩
  τ ∙ (a ∙) ⊕ b ∙ ≈ a ∙ ⊕ b ∙             ↝⟨ τa⊕b≉a⊕b ⟩□
  ⊥                                       □
  where
  a = x , true
  b = x , false

  τa≳a : ∀ {a} → τ ∙ (a ∙) ≳ a ∙
  τa≳a {a} =
    ⟨ (λ where
        action →
          a ∙       ■
            ⟵̂[ τ ]
          a ∙       ■)
    , (λ where
        action →
          τ ∙ (a ∙)      →⟨ ⟶: action ⟩
          a ∙            →⟨ ⟶: action ⟩■
            ⇒[ name a ]
          ∅              ■)
    ⟩

  τa⊕b≉a⊕b : ¬ τ ∙ (a ∙) ⊕ b ∙ ≈ a ∙ ⊕ b ∙
  τa⊕b≉a⊕b τa⊕b≈a⊕b
    with W.left-to-right τa⊕b≈a⊕b (sum-left action)
  ... | _ , non-silent ¬s _ , _ = ⊥-elim (¬s _)
  ... | _ , silent _ (step () (sum-left  action) _) , _
  ... | _ , silent _ (step () (sum-right action) _) , _
  ... | _ , silent _ done , a≈′a⊕b
    with W.right-to-left (force a≈′a⊕b) (sum-right action)
  ...   | _ , silent () _ , _
  ...   | _ , non-silent _ (steps done () _) , _
  ...   | _ , non-silent _ (steps (step () action _) _ _) , _

-- It is not necessarily the case that, if Q expands Q′, then P ⊕ Q is
-- weakly bisimilar to P ⊕ Q′ (assuming that Name is inhabited).

¬⊕-congʳ-≳≈ : Name → ¬ (∀ {P Q Q′} → Q ≳ Q′ → P ⊕ Q ≈ P ⊕ Q′)
¬⊕-congʳ-≳≈ x ⊕-congʳ-≳≈ = ¬⊕-congˡ-≳≈ x ⊕-congˡ-≳≈
  where
  ⊕-congˡ-≳≈ : ∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≈ P′ ⊕ Q
  ⊕-congˡ-≳≈ {P} {P′} {Q} P≳P′ =
    P ⊕ Q   ∼⟨ SL.⊕-comm ⟩
    Q ⊕ P   ∼′⟨ ⊕-congʳ-≳≈ P≳P′ ⟩ S.∼:
    Q ⊕ P′  ∼⟨ SL.⊕-comm ⟩■
    P′ ⊕ Q

-- _⊕_ does not, in general, preserve the expansion relation in its
-- first argument (assuming that Name is inhabited).

¬⊕-congˡ : Name → ¬ (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≳ P′ ⊕ Q)
¬⊕-congˡ x =
  (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≳ P′ ⊕ Q)  ↝⟨ W.≳⇒≈ ∘_ ⟩
  (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≈ P′ ⊕ Q)  ↝⟨ ¬⊕-congˡ-≳≈ x ⟩□
  ⊥                                       □

-- _⊕_ does not, in general, preserve the expansion relation in its
-- second argument (assuming that Name is inhabited).

¬⊕-congʳ : Name → ¬ (∀ {P Q Q′} → Q ≳ Q′ → P ⊕ Q ≳ P ⊕ Q′)
¬⊕-congʳ x =
  (∀ {P Q Q′} → Q ≳ Q′ → P ⊕ Q ≳ P ⊕ Q′)  ↝⟨ W.≳⇒≈ ∘_ ⟩
  (∀ {P Q Q′} → Q ≳ Q′ → P ⊕ Q ≈ P ⊕ Q′)  ↝⟨ ¬⊕-congʳ-≳≈ x ⟩□
  ⊥                                       □

-- Some congruence lemmas for combinations of _⊕_ and _·_.

⊕·-cong : ∀ {i P μ Q Q′} →
          [ i ] force Q ≳′ force Q′ → [ i ] P ⊕ μ · Q ≳ P ⊕ μ · Q′
⊕·-cong {i} {P} {μ} {Q} {Q′} Q≳Q′ =
  ⟨ lr , CL.⊕·-cong Q≳Q′ ⟩
  where
  lr : ∀ {R μ′} →
       P ⊕ μ · Q [ μ′ ]⟶ R →
       ∃ λ R′ → P ⊕ μ · Q′ [ μ′ ]⟶̂ R′ × [ i ] R ≳′ R′
  lr {R} {μ′} = λ where
    (sum-left P⟶R) →
      R           ■
        ⟵̂[ μ′ ]   ←⟨ ⟶: sum-left P⟶R ⟩■
      P ⊕ μ · Q′

    (sum-right action) →
      force Q     ∼⟨ Q≳Q′ ⟩■
      force Q′
        ⟵̂[ μ ]    ←⟨ ⟶: sum-right action ⟩■
      P ⊕ μ · Q′

⊕·-cong′ : ∀ {i P μ Q Q′} →
           [ i ] force Q ≳′ force Q′ → [ i ] P ⊕ μ · Q ≳′ P ⊕ μ · Q′
force (⊕·-cong′ Q≳Q′) = ⊕·-cong Q≳Q′

·⊕-cong : ∀ {i P P′ μ Q} →
          [ i ] force P ≳′ force P′ → [ i ] μ · P ⊕ Q ≳ μ · P′ ⊕ Q
·⊕-cong {P = P} {P′} {μ} {Q} P≳P′ =
  μ · P ⊕ Q   ∼⟨ SL.⊕-comm ⟩
  Q ⊕ μ · P   ∼′⟨ ⊕·-cong P≳P′ ⟩ S.∼:
  Q ⊕ μ · P′  ∼⟨ SL.⊕-comm ⟩■
  μ · P′ ⊕ Q

·⊕-cong′ : ∀ {i P P′ μ Q} →
           [ i ] force P ≳′ force P′ → [ i ] μ · P ⊕ Q ≳′ μ · P′ ⊕ Q
force (·⊕-cong′ P≳P′) = ·⊕-cong P≳P′

infix 8 _·⊕·-cong_ _·⊕·-cong′_

_·⊕·-cong_ :
  ∀ {i μ₁ μ₂ P₁ P₁′ P₂ P₂′} →
  [ i ] force P₁ ≳′ force P₁′ → [ i ] force P₂ ≳′ force P₂′ →
  [ i ] μ₁ · P₁ ⊕ μ₂ · P₂ ≳ μ₁ · P₁′ ⊕ μ₂ · P₂′
_·⊕·-cong_ {i} {μ₁} {μ₂} {P₁} {P₁′} {P₂} {P₂′} P₁≳P₁′ P₂≳P₂′ =
  ⟨ lr , CL.·⊕·-cong P₁≳P₁′ P₂≳P₂′ ⟩
  where
  lr : ∀ {R μ} → μ₁ · P₁ ⊕ μ₂ · P₂ [ μ ]⟶ R →
       ∃ λ R′ → μ₁ · P₁′ ⊕ μ₂ · P₂′ [ μ ]⟶̂ R′ × [ i ] R ≳′ R′
  lr = λ where
    (sum-left action) →
      force P₁             ∼⟨ P₁≳P₁′ ⟩■
      force P₁′
        ⟵̂[ μ₁ ]            ←⟨ ⟶: sum-left action ⟩■
      μ₁ · P₁′ ⊕ μ₂ · P₂′

    (sum-right action) →
      force P₂             ∼⟨ P₂≳P₂′ ⟩■
      force P₂′
        ⟵̂[ μ₂ ]            ←⟨ ⟶: sum-right action ⟩■
      μ₁ · P₁′ ⊕ μ₂ · P₂′

_·⊕·-cong′_ :
  ∀ {i μ₁ μ₂ P₁ P₁′ P₂ P₂′} →
  [ i ] force P₁ ≳′ force P₁′ → [ i ] force P₂ ≳′ force P₂′ →
  [ i ] μ₁ · P₁ ⊕ μ₂ · P₂ ≳′ μ₁ · P₁′ ⊕ μ₂ · P₂′
force (P₁≳′P₁′ ·⊕·-cong′ P₂≳′P₂′) = P₁≳′P₁′ ·⊕·-cong P₂≳′P₂′

-- _[_] preserves the expansion relation for non-degenerate contexts.
-- (This result is related to Theorem 6.5.25 in "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.)

infix 5 _[_]-cong _[_]-cong′

_[_]-cong :
  ∀ {i n Ps Qs} {C : Context ∞ n} →
  Non-degenerate ∞ C → (∀ x → [ i ] Ps x ≳ Qs x) →
  [ i ] C [ Ps ] ≳ C [ Qs ]
hole     [ Ps≳Qs ]-cong = Ps≳Qs _
∅        [ Ps≳Qs ]-cong = reflexive
D₁ ∣ D₂  [ Ps≳Qs ]-cong = (D₁ [ Ps≳Qs ]-cong) ∣-cong (D₂ [ Ps≳Qs ]-cong)
action D [ Ps≳Qs ]-cong = refl ·-cong λ { .force → force D [ Ps≳Qs ]-cong }
⟨ν⟩ D    [ Ps≳Qs ]-cong = ⟨ν refl ⟩-cong (D [ Ps≳Qs ]-cong)
! D      [ Ps≳Qs ]-cong = !-cong (D [ Ps≳Qs ]-cong)
D₁ ⊕ D₂  [ Ps≳Qs ]-cong = ⊕-cong Ps≳Qs D₁ D₂
  where
  _[_]-cong′ :
    ∀ {i n Ps Qs} {C : Context ∞ n} →
    Non-degenerate′ ∞ C → (∀ x → [ i ] Ps x ≳ Qs x) →
    [ i ] C [ Ps ] ≳′ C [ Qs ]
  force (D [ Ps≳Qs ]-cong′) = force D [ Ps≳Qs ]-cong

  ⊕-cong :
    ∀ {i n Ps Qs} {C₁ C₂ : Context ∞ n} →
    (∀ x → [ i ] Ps x ≳ Qs x) →
    Non-degenerate-summand ∞ C₁ →
    Non-degenerate-summand ∞ C₂ →
    [ i ] (C₁ [ Ps ]) ⊕ (C₂ [ Ps ]) ≳ (C₁ [ Qs ]) ⊕ (C₂ [ Qs ])
  ⊕-cong {Ps = Ps} {Qs} Ps≳Qs = λ where
    (process P₁) (process P₂) →
      (context P₁ [ Ps ]) ⊕ (context P₂ [ Ps ])  ∼⟨ symmetric (SL.≡→∼ (context-[] P₁) SL.⊕-cong SL.≡→∼ (context-[] P₂)) ⟩
      P₁ ⊕ P₂                                    ∼⟨ SL.≡→∼ (context-[] P₁) SL.⊕-cong SL.≡→∼ (context-[] P₂) ⟩■
      (context P₁ [ Qs ]) ⊕ (context P₂ [ Qs ])

    (process P₁) (action {μ = μ₂} {C = C₂} D₂) →
      (context P₁ [ Ps ]) ⊕ μ₂ · (C₂ [ Ps ]′)  ∼⟨ symmetric (SL.≡→∼ (context-[] P₁)) SL.⊕-cong (_ ■) ⟩
      P₁ ⊕ μ₂ · (C₂ [ Ps ]′)                   ∼′⟨ ⊕·-cong (D₂ [ Ps≳Qs ]-cong′) ⟩ S.∼:
      P₁ ⊕ μ₂ · (C₂ [ Qs ]′)                   ∼⟨ SL.≡→∼ (context-[] P₁) SL.⊕-cong (_ ■) ⟩■
      (context P₁ [ Qs ]) ⊕ μ₂ · (C₂ [ Qs ]′)

    (action {μ = μ₁} {C = C₁} D₁) (process P₂) →
      μ₁ · (C₁ [ Ps ]′) ⊕ (context P₂ [ Ps ])  ∼⟨ (_ ■) SL.⊕-cong symmetric (SL.≡→∼ (context-[] P₂)) ⟩
      μ₁ · (C₁ [ Ps ]′) ⊕ P₂                   ∼′⟨ ·⊕-cong (D₁ [ Ps≳Qs ]-cong′) ⟩ S.∼:
      μ₁ · (C₁ [ Qs ]′) ⊕ P₂                   ∼⟨ (_ ■) SL.⊕-cong SL.≡→∼ (context-[] P₂) ⟩■
      μ₁ · (C₁ [ Qs ]′) ⊕ (context P₂ [ Qs ])

    (action {μ = μ₁} {C = C₁} D₁) (action {μ = μ₂} {C = C₂} D₂) →
      μ₁ · (C₁ [ Ps ]′) ⊕ μ₂ · (C₂ [ Ps ]′)  ∼⟨ (D₁ [ Ps≳Qs ]-cong′) ·⊕·-cong (D₂ [ Ps≳Qs ]-cong′) ⟩■
      μ₁ · (C₁ [ Qs ]′) ⊕ μ₂ · (C₂ [ Qs ]′)

_[_]-cong′ :
  ∀ {i n Ps Qs} {C : Context ∞ n} →
  Non-degenerate ∞ C → (∀ x → [ i ] Ps x ≳′ Qs x) →
  [ i ] C [ Ps ] ≳′ C [ Qs ]
force (C [ Ps≳Qs ]-cong′) = C [ (λ x → force (Ps≳Qs x)) ]-cong

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module BTree.Complete.Base {A : Set} where

open import BTree {A}
open import BTree.Equality {A}

data Perfect : BTree → Set where
  plf : Perfect leaf
  p≃ : {l r : BTree}
                   (x : A)
                   → l ≃ r
                   → Perfect (node x l r)

data _⋗_ : BTree → BTree → Set where
  ⋗lf : (x : A)
                   → node x leaf leaf ⋗ leaf
  ⋗nd : {l r' : BTree}
                   (x x' : A)
                   → (r l' : BTree)
                   → l ⋗ r'
                   → node x l r ⋗ node x' l' r'

data NearlyPerfect : BTree → Set where
  npr : {r : BTree}
                   (x : A)
                   (l : BTree)
                   → NearlyPerfect r
                   → NearlyPerfect (node x l r)
  np⋗ : {l r : BTree}
                   (x : A)
                   → l ⋗ r
                   → NearlyPerfect (node x l r)

data _⋘_ : BTree → BTree → Set where
  eq⋘ : {l r : BTree}
                   → l ≃ r
                   → l ⋘ r
  gt⋘ : {l r : BTree}
                   → NearlyPerfect l
                   → Perfect r
                   → l ⋗ r
                   → l ⋘ r

data _⋙_ : BTree → BTree → Set where
  ⋙gt : {l r : BTree}
                   → l ⋗ r
                   → l ⋙ r

data Complete : BTree → Set where
  leaf : Complete leaf
  left : {l r : BTree}
                   (x : A)
                   → Complete l
                   → Complete r
                   → l ⋘ r
                   → Complete (node x l r)
  right : {l r : BTree}
                   (x : A)
                   → Complete l
                   → Complete r
                   → l ⋙ r
                   → Complete (node x l r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Construct.Always where

open import Cubical.Core.Everything

open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Construct.Constant using (Const)
open import Cubical.Data.Unit.Polymorphic

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

Always : ∀ {a b ℓ} {A : Type a} {B : Type b} → REL A B ℓ
Always = Const (⊤ , isProp⊤)

------------------------------------------------------------------------
-- Properties

module _ {a} (A : Type a) ℓ where

  reflexive : Reflexive {A = A} {ℓ = ℓ} Always
  reflexive = _

  symmetric : Symmetric {A = A} {ℓ = ℓ} Always
  symmetric _ = _

  transitive : Transitive {A = A} {ℓ = ℓ} Always
  transitive _ _ = _

  isEquivalence : IsEquivalence {ℓ = ℓ} {A} Always
  isEquivalence = record {}

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


text:
module Prelude where

open import Data.Nat
open import Data.Unit
open import Data.Product

_^_ : Set → ℕ → Set
A ^ zero = ⊤
-- A ^ 1 = A
A ^ suc n = A × (A ^ n)

ℜⁿ : {A B : Set} → (A → B → Set) → (n : ℕ) → (A ^ n → B ^ n → Set)
ℜⁿ r zero = λ tt tt → ⊤
ℜⁿ r (suc n) = λ { (a , aⁿ) (b , bⁿ) → r a b × (ℜⁿ r n) aⁿ bⁿ }

𝔉ⁿ : {A B : Set} → (A → B) → (n : ℕ) → (A ^ n → B ^ n)
𝔉ⁿ f zero = λ tt → tt
𝔉ⁿ f (suc n) = λ { (a , aⁿ) → f a , 𝔉ⁿ f n aⁿ }

max_stars_repo_name: vikraman/agda-structures

max_issues_repo_name: vikraman/agda-structures

max_forks_repo_name: vikraman/agda-structures


text:
data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x

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

record Stream (A : Set) : Set where
  constructor stream
  field
    start : A
    next : A → A

open Stream

ℕ-stream : Stream ℕ
start ℕ-stream = zero
next ℕ-stream n = succ n

0th : {A : Set} → Stream A → A
0th s = start s

3rd : {A : Set} → Stream A → A
3rd s = next s (next s (next s (start s)))

_ : 0th ℕ-stream ≡ zero
_ = refl

_ : 3rd ℕ-stream ≡ succ (succ (succ zero))
_ = refl

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
-- Andreas, 2017-12-04, Re: issue #2862, reported by m0davis,
-- Make sure there is similar problem with functions.

open import Agda.Builtin.Equality

data Bool : Set where
  true false : Bool

val : Bool

module M where
  val = true  -- Should fail

  val≡true : val ≡ true
  val≡true = refl

val = false

data ⊥ : Set where

¬val≡true : val ≡ true → ⊥
¬val≡true ()

boom : ⊥
boom = ¬val≡true Z.val≡true


text:
------------------------------------------------------------------------------
-- Testing the η-expansion
------------------------------------------------------------------------------

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

module Eta2 where

postulate
  D   : Set
  ∃   : (A : D → Set) → Set
  _≡_ : D → D → Set

-- Due to η-contraction the Agda internal representation of foo and
-- bar are the same. We η-expand the internal types before the
-- translation to FOL.

postulate
  foo : ∀ d → ∃ (λ e → d ≡ e)
  bar : ∀ d → ∃ (_≡_ d)
{-# ATP prove foo #-}
{-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Day1 where

open import Data.String as String
open import Data.Maybe
open import Foreign.Haskell using (Unit)
open import Data.List as List
open import Data.Nat
import Data.Nat.Show as ℕs
open import Data.Char
open import Data.Vec as Vec renaming (_>>=_ to _VV=_ ; toList to VecToList)
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Nat.Properties
open import Data.Bool.Base
open import AocIO
open import AocUtil
open import AocVec

makePairs : {A : Set} → {N : ℕ } → Vec A (suc N) → Vec (A × A) N
makePairs (x ∷ y ∷ vs) = ( ( x , y )) ∷ makePairs (y ∷ vs)
makePairs (x ∷ []) = []

makeNPairs : {A : Set} → {M : ℕ} → (N : ℕ) → Vec A (N + M) → Vec (A × A) M
makeNPairs {M = M} N vs with (Vec.drop N vs)
... | ends rewrite (+-comm N M) with (Vec.take M vs)
... | starts =  Vec.zip starts ends

neighbours : {A : Set} → {N : ℕ} → Vec A N → Vec (A × A) N
neighbours [] = []
neighbours (x ∷ vs) with (dupFrontToBack (x ∷ vs))
... | dvs = makePairs dvs

halfwayNeighbours : {A : Set} → (N : ℕ) → Vec A (N + N) → Vec (A × A) (N + N)
halfwayNeighbours 0 [] = []
halfwayNeighbours (suc N) v with (dupFirstNToBack (suc N) v)
... | dupped with (makeNPairs (suc N) dupped)
... | pairs = pairs

parseDigits : List Char → Maybe (List ℕ)
parseDigits [] = Maybe.just []
parseDigits (c ∷ cs) with (toDigit c) | (parseDigits cs)
...                                    | (just n)   | (just ns) = just (n ∷ ns)
...                                    | _            | _             = nothing

onlyKeepPairs : List (ℕ × ℕ) → List (ℕ × ℕ)
onlyKeepPairs [] = []
onlyKeepPairs ((a , b) ∷ xs) with (a Data.Nat.≟ b)
... | yes p = (a , b) ∷ onlyKeepPairs xs
... | no ¬p = onlyKeepPairs xs

main2 : IO Unit
main2 = mainBuilder (readFileMain processFile)
     where
       processDigits : {M : ℕ} → Vec ℕ M → IO Unit
       processDigits vs with (neighbours vs)
       ... | neigh with (onlyKeepPairs (VecToList neigh))
       ... | pairs with (List.map  Σ.proj₁ pairs)
       ... | nums = putStrLn (toCostring (ℕs.show (List.sum nums)))
       processLine : List Char → IO Unit
       processLine ls with (parseDigits ls)
       ... | nothing = putStrLn (toCostring ("Failed to parse this line: " String.++ (String.fromList ls)))
       ... | just digs = processDigits (Vec.fromList digs)
       processFile : String → IO Unit
       processFile file-content with (lines (String.toList file-content))
       ... | file-lines with (List.map processLine file-lines)
       ... | ops = void (sequence-io-prim ops)

checkEvenVec : ∀ {a} {A : Set a} → {N : ℕ} → Vec A N → Maybe (Σ[ M ∈ ℕ ] M + M ≡ N)
checkEvenVec [] = just (0 , refl)
checkEvenVec (x ∷ []) = nothing
checkEvenVec { N = N} (x ∷ y ∷ vs) with (checkEvenVec vs)
... | nothing = nothing
... | just (M , p) with (cong suc (+-suc M M))
... | t rewrite p = just ((suc M) , t)

main : IO Unit
main = mainBuilder (readFileMain processFile)
      where
      processDigits : {N : ℕ} → Vec ℕ N → IO Unit
      processDigits vs with (checkEvenVec vs)
      ... | nothing = printString "Input has to have even length"
      ... | just (M , p) with (halfwayNeighbours M v)
        where
          v : Vec ℕ (M + M)
          v rewrite p = vs
      ... | half-neigh with (onlyKeepPairs (VecToList half-neigh))
      ... | pairs with (List.map Σ.proj₁ pairs)
      ... | nums = printString (ℕs.show (List.sum nums))
      processLine : List Char → IO Unit
      processLine ls with (parseDigits ls)
      ... | nothing = putStrLn (toCostring ("Failed to parse this line: " String.++ (String.fromList ls)))
      ... | just digs = processDigits (Vec.fromList digs)
      processFile : String → IO Unit
      processFile file-content with (lines (String.toList file-content))
      ... | file-lines with (List.map processLine file-lines)
      ... | ops = void (sequence-io-prim ops)


text:
module UnifyFin where

open import Data.Fin using (Fin; suc; zero)
open import Data.Nat using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂; cong; sym; trans)
open import Function using (_∘_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (∃; _,_; _×_)
open import Data.Empty using (⊥-elim)

thin : ∀ {n} -> (x : Fin (suc n)) (y : Fin n) -> Fin (suc n)
thin zero y = suc y
thin (suc x) zero = zero
thin (suc x) (suc y) = suc (thin x y)

p : ∀ {n} -> Fin (suc (suc n)) -> Fin (suc n)
p (suc x) = x
p zero = zero

module Thin where
  fact1 : ∀ {n} x y z -> thin {n} x y ≡ thin x z -> y ≡ z
  fact1 zero y .y refl = refl
  fact1 (suc x) zero zero r = refl
  fact1 (suc x) zero (suc z) ()
  fact1 (suc x) (suc y) zero ()
  fact1 (suc x) (suc y) (suc z) r = cong suc (fact1 x y z (cong p r))

  fact2 : ∀ {n} x y -> ¬ thin {n} x y ≡ x
  fact2 zero y ()
  fact2 (suc x) zero ()
  fact2 (suc x) (suc y) r = fact2 x y (cong p r)

  fact3 : ∀{n} x y -> ¬ x ≡ y -> ∃ λ y' -> thin {n} x y' ≡ y
  fact3 zero zero ne = ⊥-elim (ne refl)
  fact3 zero (suc y) _ = y , refl
  fact3 {zero} (suc ()) _ _
  fact3 {suc n} (suc x) zero ne = zero , refl
  fact3 {suc n} (suc x) (suc y) ne with y | fact3 x y (ne ∘ cong suc)
  ... | .(thin x y') | y' , refl = suc y' , refl

open import Data.Maybe
open import Category.Functor
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})

thick : ∀ {n} -> (x y : Fin (suc n)) -> Maybe (Fin n)
thick zero zero = nothing
thick zero (suc y) = just y
thick {zero} (suc ()) _
thick {suc _} (suc x) zero = just zero
thick {suc _} (suc x) (suc y) = suc <$> (thick x y)

open import Data.Sum

_≡Fin_ : ∀ {n} -> (x y : Fin n) -> Dec (x ≡ y)
zero ≡Fin zero = yes refl
zero ≡Fin suc y = no λ ()
suc x ≡Fin zero = no λ ()
suc {suc _} x ≡Fin suc y with x ≡Fin y
...              | yes r = yes (cong suc r)
...              | no r = no λ e -> r (cong p e)
suc {zero} () ≡Fin _

module Thick where
  half1 : ∀ {n} (x : Fin (suc n)) -> thick x x ≡ nothing
  half1 zero = refl
  half1 {suc _} (suc x) = cong (_<$>_ suc) (half1 x)
  half1 {zero} (suc ())

  half2 : ∀ {n} (x : Fin (suc n)) y -> ∀ y' -> thin x y' ≡ y -> thick x y ≡ just y'
  half2 zero zero y' ()
  half2 zero (suc y) .y refl = refl
  half2 {suc n} (suc x) zero zero refl = refl
  half2 {suc _} (suc _) zero (suc _) ()
  half2 {suc n} (suc x) (suc y) zero ()
  half2 {suc n} (suc x) (suc .(thin x y')) (suc y') refl with thick x (thin x y') | half2 x (thin x y') y' refl
  ...                                                       | .(just y')          | refl = refl
  half2 {zero} (suc ()) _ _ _

  fact1 : ∀ {n} (x : Fin (suc n)) y r
    -> thick x y ≡ r
    -> x ≡ y × r ≡ nothing ⊎ ∃ λ y' -> thin x y' ≡ y × r ≡ just y'
  fact1 x y .(thick x y) refl with x ≡Fin y
  fact1 x .x ._ refl | yes refl = inj₁ (refl , half1 x)
  ... | no el with Thin.fact3 x y el
  ...            | y' , thinxy'=y = inj₂ (y' , ( thinxy'=y , half2 x y y' thinxy'=y ))


text:
module SET where
  ----------------------------------------------------------------------------
  -- Auxiliary.
  ----------------------------------------------------------------------------
  data Fun (X Y : Set) : Set where
    fun : (X -> Y) -> Fun X Y

  {-
  Unop : Set -> Set
  Unop X = Fun X X

  Binop : Set -> Set
  Binop X = Fun X (Fun X X)
  -}

  -- We need to replace Pred X by its RHS (less readable!)

--  Pred : Set -> Set1
--  Pred X = X -> Set
--  Pow = Pred
--  Rel : Set -> Set1
--  Rel X = X -> X -> Set
  data Reflexive {X : Set} (R : X -> X -> Set) : Set where
    reflexive : ((x : X) -> R x x) -> Reflexive R

  data Symmetrical {X : Set} (R : X -> X -> Set) : Set where
    symmetrical : ( {x1 x2 : X} -> R x1 x2 -> R x2 x1) -> Symmetrical R
{-
  Transitive {X : Set}(R : X -> X -> Set) : Set
    = (x1 x2 x3 : X) |->  R x1 x2 -> R x2 x3 -> R x1 x3
  Compositional {X : Set}(R : X -> X -> Set) : Set
    = (x1 : X) |-> (x2 : X) |-> (x3 : X) |-> R x2 x3 -> R x1 x2 -> R x1 x3
-}
  data Substitutive {X : Set} (R : X -> X -> Set) : Set1 where
    substitutive : ( (P : X -> Set) -> {x1 x2 : X} -> R x1 x2 -> P x1 -> P x2)
                   -> Substitutive R
{-
  Collapsed (X : Set) : Set1
    = (P : X -> Set) -> (x1 x2 : X) |-> P x1 -> P x2
  id {X : Set} : X -> X
    = \x -> x
  cmp (|X |Y |Z : Set) : (Y -> Z) -> (X -> Y) -> X -> Z
    = \f -> \g -> \x -> f (g x)
  seq (|X |Y |Z : Set)(f : X -> Y)(g : Y -> Z) : X -> Z
    = cmp g f

  const (|X |Y : Set)(x : X)(y : Y) : X
    = x
  proj {X : Set}(Y : X -> Set)(x : X)(f : (x : X) -> Y x) : Y x
    = f x
  flip {X : Set}{Y : Set}{Z : Set}(f : X -> Y -> Z)(y : Y)(x : X) : Z
    = f x y
  FlipRel {X : Set}(R : X -> X -> Set)(x1 : X)(x2 : X) : Set
    = R x2 x1

  ----------------------------------------------------------------------------
  -- Product sets.
  ----------------------------------------------------------------------------
  Prod (X : Set)(Y : X -> Set) : Set
    = (x : X) -> Y x
  mapProd {X : Set}
          {Y1 : X -> Set}
          {Y2 : X -> Set}
          (f : (x : X) -> Y1 x -> Y2 x)
    : Prod X Y1  -> Prod X Y2
    = \g -> \x -> f x (g x)
  -- Fun(X : Set)(Y : Set) = X -> Y
  mapFun (|X1 |X2 |Y1 |Y2 : Set)
    : (X2 -> X1) -> (Y1 -> Y2) -> (X1 -> Y1) -> X2 -> Y2
    = \f -> \g -> \h -> \x ->
      g (h (f x))

  ----------------------------------------------------------------------------
  -- Identity proof sets.
  ----------------------------------------------------------------------------
  Id {X : Set} : X -> X -> Set
    = idata ref (x : X) : _ x x
  refId {X : Set} : Reflexive Id
    = \(x : X) -> ref@_  x

  elimId (|X : Set)
         (C : (x1 x2 : X)  |-> Id x1 x2 -> Set)
         (refC :  (x : X) -> C (refId x))
         (|x1 |x2 : X)
         (u : Id x1 x2) :
         C u
    = case u of { (ref x) -> refC x;}

  abstract whenId {X : Set}(C : X -> X -> Set)(c : (x : X) -> C x x)
    : (x1 x2 : X)  |-> Id x1 x2 -> C x1 x2
    = elimId (\x1 x2 |-> \(u : Id x1 x2) -> C x1 x2) c

  abstract substId {X : Set} : Substitutive Id
    = \(C : X -> Set) ->
      whenId (\x1 x2 -> C x1 -> C x2) (\x -> id)

  abstract mapId {X : Set}{Y : Set}(f : X -> Y)
    : (x1 x2 : X) |-> Id x1 x2 -> Id (f x1) (f x2)
    = whenId (\x1 x2 -> Id (f x1) (f x2)) (\(x : X) -> refId (f x))

  abstract symId {X : Set} : Symmetrical Id
    =  whenId (\(x1 x2 : X) ->  Id x2 x1) refId

  abstract cmpId {X : Set} : Compositional Id
    = let lem : (x y : X) |-> Id x y -> (z : X) |-> Id z x -> Id z y
            = whenId ( \(x y : _) -> (z : X) |-> Id z x -> Id z y)
                     ( \x -> \z |-> id)
      in  \(x1 x2 x3 : _) |->
          \(u : Id x2 x3) ->
          \(v : Id x1 x2) ->
          lem  u v

  abstract tranId {X : Set} : Transitive  Id
    = \(x1 x2 x3 : X) |->
      \(u : Id x1 x2) ->
      \(v : Id x2 x3) ->
      cmpId v u

  ----------------------------------------------------------------------------
  -- The empty set.
  ----------------------------------------------------------------------------
-}
  data Zero : Set where

{-
  abstract whenZero (X : Set)(z : Zero) : X
    = case z of { }
  elimZero (C : Zero -> Set)(z : Zero) : C z
    = case z of { }
  abstract collZero : Collapsed Zero
    = \(C : Zero -> Set) ->
      \(z1 z2 : Zero) |->
      \(c : C z1) ->
      case z1 of { }
  ----------------------------------------------------------------------------
  -- The singleton set.
  ----------------------------------------------------------------------------
-}
  data Unit : Set where
    unit : Unit
{-
  elUnit = tt
  elimUnit (C : Unit -> Set)(c_tt : C tt@_)(u : Unit) : C u
    = case u of { (tt) -> c_tt;}
  abstract collUnit : Collapsed Unit
    = \(C : Unit -> Set) ->
      \(u1 u2 : Unit) |->
      \(c : C u1) ->
      case u1 of { (tt) -> case u2 of { (tt) -> c;};}
  ----------------------------------------------------------------------------
  -- The successor set adds a new element.
  ----------------------------------------------------------------------------

  Succ (X : Set) : Set
    = data zer | suc (x : X)
  zerSucc {X : Set} : Succ X
    = zer@_
  sucSucc {X : Set}(x : X) : Succ X
    = suc@_ x
  elimSucc {X : Set}
           (C : Succ X -> Set)
           (c_z : C zer@_)
           (c_s : (x : X) -> C (suc@_ x))
           (x' : Succ X)
    : C x'
    = case x' of {
        (zer) -> c_z;
        (suc x) -> c_s x;}
  whenSucc (|X |Y : Set)(y_z : Y)(y_s : X -> Y)(x' : Succ X) : Y
    = case x' of {
        (zer) -> y_z;
        (suc x) -> y_s x;}
  mapSucc (|X |Y : Set)(f : X -> Y) : Succ X -> Succ Y
    = whenSucc zer@(Succ Y) (\(x : X) -> suc@_ (f x)) -- (Succ Y)

  ----------------------------------------------------------------------------
  -- The (binary) disjoint union.
  ----------------------------------------------------------------------------
  data Plus (X Y : Set) = inl (x : X) | inr (y : Y)

  elimPlus (|X |Y : Set)
           (C : Plus X Y -> Set)
           (c_lft : (x : X) -> C (inl@_ x))
           (c_rgt : (y : Y) -> C (inr@_ y))
           (xy : Plus X Y)
    : C xy
    = case xy of {
        (inl x) -> c_lft x;
        (inr y) -> c_rgt y;}
  when (|X |Y |Z : Set)(f : X -> Z)(g : Y -> Z) : Plus X Y -> Z
    = \xy -> case xy of {
        (inl x) -> f x;
        (inr y) -> g y;}
  whenPlus = when
  mapPlus (|X1 |X2 |Y1 |Y2 : Set)(f : X1 -> X2)(g : Y1 -> Y2)
    : Plus X1 Y1 -> Plus X2 Y2
    = when (\x1 -> inl (f x1)) (\y1 -> inr (g y1))
  swapPlus (|X |Y : Set) :  Plus X Y -> Plus Y X
    = when inr inl

  ----------------------------------------------------------------------------
  -- Dependent pairs.
  ----------------------------------------------------------------------------
  Sum (X : Set)(Y : X -> Set) : Set
    = sig{fst : X;
          snd : Y fst;}
  dep_pair {X : Set}{Y : X -> Set}(x : X)(y : Y x) : Sum X Y
    = struct {fst = x; snd = y;}
  dep_fst {X : Set}{Y : X -> Set}(xy : Sum X Y) : X
    = xy.fst
  dep_snd {X : Set}{Y : X -> Set}(xy : Sum X Y) : Y (dep_fst xy)
    = xy.snd
  dep_cur {X : Set}{Y : X -> Set}{Z : Set}(f : Sum X Y -> Z)
    : (x : X) |-> Y x -> Z
    = \x |-> \y ->  f (dep_pair  x  y)

  dep_uncur {X : Set}{Y : X -> Set}{Z : Set}
    : ((x : X) -> Y x -> Z) -> Sum X Y -> Z
    = \(f : (x : X) -> (x' : Y x) -> Z) -> \(xy : Sum X Y) -> f xy.fst xy.snd
  dep_curry {X : Set}
            {Y : X -> Set}
            (Z : Sum X Y -> Set)
            (f : (xy : Sum X Y) -> Z xy)
    : (x : X) ->  (y : Y x) -> Z (dep_pair x y)
    = \(x : X) -> \(y : Y x) -> f (dep_pair x y)

  dep_uncurry {X : Set}
              {Y : X -> Set}
              (Z : Sum X Y -> Set)
              (f : (x : X) ->
                  (y : Y x) ->
                  Z (dep_pair x y))
              (xy : Sum X Y)
    : Z xy
    = f xy.fst xy.snd
  mapSum {X : Set}{Y1 : X -> Set}{Y2 : X -> Set}(f : (x : X) -> Y1 x -> Y2 x)
    : Sum X Y1 -> Sum X Y2
    = \(p : Sum X Y1) -> dep_pair p.fst (f p.fst p.snd)

  elimSum = dep_uncurry
  ----------------------------------------------------------------------------
  -- Nondependent pairs (binary) cartesian product.
  ----------------------------------------------------------------------------
  Times (X : Set)(Y : Set) : Set
    = Sum X (\(x : X) -> Y)
  pair {X : Set}{Y : Set} : X -> Y -> Times X Y
    = \(x : X) ->
      \(y : Y) ->
      struct {
        fst = x;
        snd = y;}
  fst {X : Set}{Y : Set} : Times X Y -> X
    = \(xy : Times X Y) -> xy.fst
  snd {X : Set}{Y : Set} : Times X Y -> Y
    = \(xy : Times X Y) -> xy.snd
  pairfun {X : Set}{Y : Set}{Z : Set}(f : X -> Y)(g : X -> Z)(x : X)
    : Times Y Z
    = pair (f x) (g x)
  mapTimes {X1 : Set}{X2 : Set}{Y1 : Set}{Y2 : Set}
    : (f : X1 -> X2) -> (g : Y1 -> Y2) -> Times X1 Y1 -> Times X2 Y2
    = \(f : (x : X1) -> X2) ->
      \(g : (x : Y1) -> Y2) ->
      \(xy : Times X1 Y1) ->
      pair (f xy.fst) (g xy.snd)
  swapTimes {X : Set}{Y : Set} : Times X Y -> Times Y X
    = pairfun snd fst
  cur {X : Set}{Y : Set}{Z : Set}(f : Times X Y -> Z) : X -> Y -> Z
    = \(x : X) -> \(y : Y) -> f (pair |_ |_ x y)
  uncur {X : Set}{Y : Set}{Z : Set}(f : X -> Y -> Z) : Times X Y -> Z
    = \(xy : Times X Y) -> f xy.fst xy.snd
  curry {X : Set}
        {Y : Set}
        {Z : Times X Y -> Set}
        (f : (xy : Times X Y) -> Z xy)
    : (x : X) ->
       (y : Y) ->
       Z (pair |_ |_ x y)
    = \(x : X) ->
      \(y : Y) ->
      f (pair |_ |_ x y)

  uncurry {X : Set}
          {Y : Set}
          {Z : Times X Y -> Set}
          (f : (x : X) ->
              (y : Y) ->
              Z (pair |_ |_ x y))
    : (xy : Times X Y) -> Z xy
    = \(xy : Times X Y) -> f xy.fst xy.snd

  elimTimes = uncurry
  ----------------------------------------------------------------------------
  -- Natural numbers.
  ----------------------------------------------------------------------------
  Nat : Set
    = data zer | suc (m : Nat)
  zero : Nat
    = zer@_
  succ (x : Nat) : Nat
    = suc@_ x
  elimNat (C : Nat -> Set)
    : (c_z : C zer@_) ->
       (c_s : (x : Nat) -> C x -> C (suc@_ x)) ->
       (m : Nat) ->
       C m
    = \(c_z : C zer@_) ->
      \(c_s : (x : Nat) -> (x' : C x) -> C (suc@_ x)) ->
      \(m : Nat) ->
      case m of {
        (zer) -> c_z;
        (suc m') -> c_s m' (elimNat C c_z c_s m');}
  ----------------------------------------------------------------------------
  -- Linear universe of finite sets.
  ----------------------------------------------------------------------------
  Fin (m : Nat) : Set
    = case m of {
        (zer) -> Zero;
        (suc m') -> Succ (Fin m');}
  valFin (m : Nat) : Fin m -> Nat
    = \(n : Fin m) ->
      case m of {
        (zer) -> case n of { };
        (suc m') ->
          case n of {
            (zer) -> zer@_;
            (suc n') -> suc@_ (valFin m' n');};}
  zeroFin (m : Nat) : Fin (succ m)
    = zer@_
  succFin (m : Nat)(n : Fin m) : Fin (succ m)
    = suc@_ n
  ----------------------------------------------------------------------------
  -- Do these really belong here?
  ----------------------------------------------------------------------------
  HEAD (X : Set1)(m : Nat)(f : Fin (succ m) -> X) : X
    = f (zeroFin m)
  TAIL (X : Set1)(m : Nat)(f : Fin (succ m) -> X) : Fin m -> X
    = \(n : Fin m) -> f (succFin m n)
  ----------------------------------------------------------------------------
  -- Lists.
  ----------------------------------------------------------------------------
  List (X : Set) : Set
    = data nil | con (x : X) (xs : List X)
  nil {X : Set} : List X
    = nil@_
  con {X : Set}(x : X)(xs : List X) : List X
    = con@_ x xs
  elimList {X : Set}
           (C : List X -> Set)
           (c_nil : C (nil |_))
           (c_con : (x : X) -> (xs : List X) -> C xs -> C (con@_ x xs))
           (xs : List X)
    : C xs
    = case xs of {
        (nil) -> c_nil;
        (con x xs') -> c_con x xs' (elimList |_ C c_nil c_con xs');}
  ----------------------------------------------------------------------------
  -- Tuples are "dependently typed vectors".
  ----------------------------------------------------------------------------
  Nil : Set
    = data nil
  Con (X0 : Set)(X' : Set) : Set
    = data con (x : X0) (xs : X')
  Tuple (m : Nat)(X : Fin m -> Set) : Set
    = case m of {
        (zer) -> Nil;
        (suc m') -> Con (X zer@_) (Tuple m' (\(n : Fin m') -> X (suc@_ n)));}
  ----------------------------------------------------------------------------
  -- Vectors homogeneously typed tuples.
  ----------------------------------------------------------------------------
  Vec (X : Set)(m : Nat) : Set
    = Tuple m (\(n : Fin m) -> X)
  ----------------------------------------------------------------------------
  -- Monoidal expressions.
  ----------------------------------------------------------------------------
  Mon (X : Set) : Set
    = data unit | at (x : X) | mul (xs1 : Mon X) (xs2 : Mon X)
  ----------------------------------------------------------------------------
  -- Propositions.
  ----------------------------------------------------------------------------
  Imply (X : Set)(Y : Set) : Set
    = X -> Y
-}
  Absurd : Set
  Absurd = Zero
  Taut : Set
  Taut = Unit
{-
  Not (X : Set) : Set
    = X -> Absurd
  Exist {X : Set}(P : X -> Set) : Set
    = Sum X P
  Forall (X : Set)(P : X -> Set) : Set
    = (x : X) -> P x
  And (X : Set)(Y : Set) : Set
    = Times X Y
  Iff (X : Set)(Y : Set) : Set
    = And (Imply X Y) (Imply Y X)
  Or (X : Set)(Y : Set) : Set
    = Plus X Y
  Decidable (X : Set) : Set
    = Or X (Imply X Absurd)
  DecidablePred {X : Set}(P : X -> Set) : Set
    = (x : X) -> Decidable (P x)
  DecidableRel {X : Set}(R : X -> X -> Set) : Set
    = (x1 : X) -> (x2 : X) -> Decidable (R x1 x2)
  Least {X : Set}((<=) : X -> X -> Set)(P : X -> Set) : X -> Set
    = \(x : X) -> And (P x) ((x' : X) -> P x' -> (x <= x'))
  Greatest {X : Set}((<=) : X -> X -> Set)(P : X -> Set) : X -> Set
    = \(x : X) -> And (P x) ((x' : X) -> P x' -> (x' <= x))
  ----------------------------------------------------------------------------
  -- Booleans.
  ----------------------------------------------------------------------------
-}
  data Bool : Set where
    true  : Bool
    false : Bool
{-
  elimBool (C : Bool -> Set)(c_t : C true@_)(c_f : C false@_)(p : Bool)
    : C p
    = case p of {
        (true) -> c_t;
        (false) -> c_f;}
  whenBool (C : Set)(c_t : C)(c_f : C) : Bool -> C
    = elimBool (\(x : Bool) -> C) c_t c_f
  pred (X : Set) : Set
    = X -> Bool
-}
--  rel (X : Set) : Set
--    = X -> X -> Bool
  True : Bool -> Set
  True (true)  = Taut
  True (false) = Absurd
{-
  bool2set = True
  pred2Pred {X : Set} : pred X -> X -> Set
    = \(p : pred X) -> \(x : X) -> True (p x)
  rel2Rel {X : Set} : (X -> X -> Bool) -> X -> X -> Set
    = \(r : (X -> X -> Bool)) -> \(x : X) -> \(y : X) -> True (r x y)
  decTrue (p : Bool) : Decidable (True p)
    = case p of {
        (true) -> inl@_ tt;
        (false) -> inr@_ (id |_);}
  abstract dec_lem {P : Set}(decP : Decidable P)
    : Exist |_ (\(b : Bool) -> Iff (True b) P)
    = case decP of {
        (inl trueP) ->
          struct {
            fst = true@_;
            snd =
              struct {
                fst = const |_  |_ trueP;  -- (True true@_)
                snd = const |_ |_  tt;};};
        (inr notP) ->
          struct {
            fst = false@_;
            snd =
              struct {
                fst = whenZero P;
                snd = notP;};};}
  dec2bool : (P : Set) |-> (decP : Decidable P) -> Bool
    = \(P : Set) |-> \(decP : Decidable P) -> (dec_lem |_ decP).fst
  dec2bool_spec {P : Set}(decP : Decidable P)
    : Iff (True (dec2bool |_ decP)) P
    = (dec_lem |_ decP).snd

  abstract collTrue : (b : Bool) -> Collapsed (True b)
    = let aux (X : Set)(C : X -> Set)
            : (b : Bool) ->
               (f : True b -> X) ->
               (t1 : True b) |->
               (t2 : True b) |->
               C (f t1) -> C (f t2)
            = \(b : Bool) ->
              case b of {
                (true) ->
                  \(f : (x : True true@_) -> X) ->
                  \(t1 t2 : True true@_) |->
                  \(c : C (f t1)) ->
                  case t1 of { (tt) -> case t2 of { (tt) -> c;};};
                (false) ->
                  \(f : (x : True false@_) -> X) ->
                  \(t1 t2 : True false@_) |->
                  \(c : C (f t1)) ->
                  case t1 of { };}
      in   \(b : Bool) ->  \(P : True b -> Set) -> aux (True b) P b id

  bool2nat (p : Bool) : Nat
    = case p of {
        (true) -> succ zero;
        (false) -> zero;}
  ----------------------------------------------------------------------------
  -- Decidable subsets.
  ----------------------------------------------------------------------------
  Filter {X : Set}(p : pred X) : Set
    = Sum X (pred2Pred |_ p)
  ----------------------------------------------------------------------------
  -- Equality.
  ----------------------------------------------------------------------------
  -- "Deq" stands for "datoid equality" and represents exactly the data
  --  that has to be added to turn a set into a datoid.
  Deq (X : Set) : Set1
    = sig{eq : X -> X -> Bool;
          ref : (x : X) -> True (eq x x);
          subst :
            (C : X -> Set) -> (x1 x2 : X)|-> True (eq x1 x2) -> C x1 -> C x2;}
  -- The "Equality" type represents the data that has to be added to turna
  -- set into a setoid.
  Equality (X : Set) : Set1
    = sig{Equal : X -> X -> Set;
          ref  : Reflexive |_ Equal;
          sym  : Symmetrical |_ Equal;
          tran : Transitive |_ Equal;}
  -}
  data Datoid  : Set1 where
    datoid : (Elem : Set) ->
             (eq : Elem -> Elem -> Bool) ->
             (ref :  (x : Elem) -> True (eq x x)) ->
             (subst : Substitutive  (\x1 -> \x2 -> True (eq x1 x2))) ->
             Datoid

  pElem : Datoid -> Set
  pElem (datoid Elem _ _ _) = Elem

  {-
  ElD (X : Datoid) : Set
    = X.Elem
  eqD {X : Datoid} : ElD X -> ElD X -> Bool
    = X.eq
  EqD {X : Datoid}(x1 x2 : ElD X) : Set
    = True (X.eq x1 x2)

  Setoid : Set1
    = sig{Elem : Set;
          Equal : Elem -> Elem -> Set;
          ref : (x : Elem) -> Equal x x;
          sym : (x1 : Elem) |-> (x2 : Elem) |-> Equal x1 x2 -> Equal x2 x1;
          tran :
            (x1 : Elem) |->
            (x2 : Elem) |->
            (x3 : Elem) |->
            Equal x1 x2 -> Equal x2 x3 -> Equal x1 x3;}
  El (X : Setoid) : Set
    = X.Elem
  Eq {X : Setoid} : Rel (El X)
    = X.Equal

  NotEq {X : Setoid} : Rel (El X)
    = \x1-> \x2-> Not (Eq |X x1 x2)
  Respectable {X : Setoid}(P : El X -> Set) : Set
    = (x1 x2 : El X) |-> Eq |X x1 x2 -> P x1 -> P x2
  RspEq {X Y : Setoid}(f : El X -> El Y) : Set
    = (x1 x2 : El X)  |-> Eq |X x1 x2 -> Eq |Y (f x1) (f x2)
  RspEq2 (|X |Y |Z : Setoid)(f : El X -> El Y -> El Z)
    : Set
    = (x1 x2 :  X.Elem) |-> (y1 y2 :  Y.Elem) ->
      Eq |X x1 x2 ->
      Eq |Y y1 y2  ->
      Eq |Z (f x1 y1) (f x2 y2)
  D2S (Y : Datoid) : Setoid
    = struct {
        Elem = Y.Elem;
        Equal = \(x1 x2 : Elem) -> True (Y.eq x1 x2);
        ref = Y.ref;
        sym =
          \(x1 x2 : Elem) |->
          \(u : Equal x1 x2) ->
          Y.subst (\(x : Y.Elem) -> Equal x x1) |_ |_ u (ref x1);
        tran =
          \(x1 x2 x3 : Elem) |->
          \(u : Equal x1 x2) ->
          \(v : Equal x2 x3) ->
          Y.subst (Equal x1) |_ |_  v u;}

{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide
nd
hiding on
con "nil" as "[]" with symbolfont
con "con" infix as " : " with symbolfont
var "Forall" as "\"" with symbolfont
var "Exist" as "$" with symbolfont
var "And" infix as "&" with symbolfont
var "Or" infix as "Ú" with symbolfont
var "Iff" infix as "«" with symbolfont
var "Not" as "Ø" with symbolfont
var "Imply" infix as "É" with symbolfont
var "Taut" as "T" with symbolfont
var "Absurd" as "^" with symbolfont
var "El" mixfix as "|_|" with symbolfont
var "Eq" distfix3 as "==" with symbolfont
var "NotEq" distfix3 as "=|=" with symbolfont
var "True" mixfix as "|_|" with symbolfont
var "ElD" mixfix as "|_|" with symbolfont
var "EqD" distfix3 as "==" with symbolfont
var "Id" distfix3 as "=" with symbolfont
 #-}
-}


text:
module Membership where

open import OscarPrelude
open import Successor

record Membership {ℓ} (m : Set ℓ) (M : Set ℓ) : Set (⊹ ℓ)
 where
  field
    _∈_ : m → M → Set ℓ
    _∉_ : m → M → Set ℓ
    xor-membership : ∀ {x : m} {X : M} → x ∈ X ←⊗→ x ∉ X

open Membership ⦃ … ⦄ public

data _∈List_ {ℓ} {A : Set ℓ} (a : A) : List A → Set ℓ
 where
  zero : {as : List A} → a ∈List (a ∷ as)
  suc : {x : A} {as : List A} → a ∈List as → a ∈List (x ∷ as)

instance MembershipList : ∀ {ℓ} {A : Set ℓ} → Membership A $ List A
Membership._∈_ MembershipList = _∈List_
Membership._∉_ MembershipList x X = ¬ x ∈ X
Membership.xor-membership MembershipList = (λ x x₁ → x₁ x) , (λ x x₁ → x x₁)

instance SuccessorMembershipList : ∀ {ℓ} {A : Set ℓ} {a : A} {x : A} {as : List A} → Successor (a ∈ as) $ a ∈ (x List.∷ as)
Successor.⊹ SuccessorMembershipList = suc

_⊆_ : ∀ {ℓ} {m M : Set ℓ} ⦃ _ : Membership m M ⦄ → M → M → Set ℓ
_⊆_ {m = m} M₁ M₂ = ∀ {x : m} → x ∈ M₁ → x ∈ M₂


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Intersection of two binary relations
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Intersection where

open import Data.Product
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Function using (_∘_)
open import Level using (_⊔_)
open import Relation.Binary
open import Relation.Nullary using (yes; no)

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

_∩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
      REL A B ℓ₁ → REL A B ℓ₂ → REL A B (ℓ₁ ⊔ ℓ₂)
L ∩ R = λ i j → L i j × R i j

------------------------------------------------------------------------
-- Properties

module _ {a ℓ₁ ℓ₂} {A : Set a} (L : Rel A ℓ₁) (R : Rel A ℓ₂) where

  reflexive : Reflexive L → Reflexive R → Reflexive (L ∩ R)
  reflexive L-refl R-refl = L-refl , R-refl

  symmetric : Symmetric L → Symmetric R → Symmetric (L ∩ R)
  symmetric L-sym R-sym = map L-sym R-sym

  transitive : Transitive L → Transitive R → Transitive (L ∩ R)
  transitive L-trans R-trans = zip L-trans R-trans

  respects : ∀ {p} (P : A → Set p) →
             P Respects L ⊎ P Respects R → P Respects (L ∩ R)
  respects P resp (Lxy , Rxy) = [ (λ x → x Lxy) , (λ x → x Rxy) ] resp

  min : ∀ {⊤} → Minimum L ⊤ → Minimum R ⊤ → Minimum (L ∩ R) ⊤
  min L-min R-min = < L-min , R-min >

  max : ∀ {⊥} → Maximum L ⊥ → Maximum R ⊥ → Maximum (L ∩ R) ⊥
  max L-max R-max = < L-max , R-max >

module _ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b}
         (≈ : REL A B ℓ₁) {L : REL A B ℓ₂} {R : REL A B ℓ₃} where

  implies : (≈ ⇒ L) → (≈ ⇒ R) → ≈ ⇒ (L ∩ R)
  implies ≈⇒L ≈⇒R = < ≈⇒L , ≈⇒R >

module _ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b}
         (≈ : REL A B ℓ₁) (L : REL A B ℓ₂) (R : REL A B ℓ₃) where

  irreflexive : Irreflexive ≈ L ⊎ Irreflexive ≈ R → Irreflexive ≈ (L ∩ R)
  irreflexive irrefl x≈y (Lxy , Rxy) = [ (λ x → x x≈y Lxy) , (λ x → x x≈y Rxy) ] irrefl

module _ {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
         (≈ : Rel A ℓ₁) (L : Rel A ℓ₂) (R : Rel A ℓ₃) where

  respectsˡ : L Respectsˡ ≈ → R Respectsˡ ≈ → (L ∩ R) Respectsˡ ≈
  respectsˡ L-resp R-resp x≈y = map (L-resp x≈y) (R-resp x≈y)

  respectsʳ : L Respectsʳ ≈ → R Respectsʳ ≈ → (L ∩ R) Respectsʳ ≈
  respectsʳ L-resp R-resp x≈y = map (L-resp x≈y) (R-resp x≈y)

  respects₂ : L Respects₂ ≈ → R Respects₂ ≈ → (L ∩ R) Respects₂ ≈
  respects₂ (Lʳ , Lˡ) (Rʳ , Rˡ) = respectsʳ Lʳ Rʳ , respectsˡ Lˡ Rˡ

  antisymmetric : Antisymmetric ≈ L ⊎ Antisymmetric ≈ R → Antisymmetric ≈ (L ∩ R)
  antisymmetric (inj₁ L-antisym) (Lxy , _) (Lyx , _) = L-antisym Lxy Lyx
  antisymmetric (inj₂ R-antisym) (_ , Rxy) (_ , Ryx) = R-antisym Rxy Ryx

module _ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} {L : REL A B ℓ₁} {R : REL A B ℓ₂} where

  decidable : Decidable L → Decidable R → Decidable (L ∩ R)
  decidable L? R? x y with L? x y | R? x y
  ... | no ¬Lxy | _       = no (¬Lxy ∘ proj₁)
  ... | yes _   | no ¬Rxy = no (¬Rxy ∘ proj₂)
  ... | yes Lxy | yes Rxy = yes (Lxy , Rxy)

------------------------------------------------------------------------
-- Structures

module _ {a ℓ₁ ℓ₂} {A : Set a} {L : Rel A ℓ₁} {R : Rel A ℓ₂} where

  isEquivalence : IsEquivalence L → IsEquivalence R → IsEquivalence (L ∩ R)
  isEquivalence eqₗ eqᵣ = record
    { refl  = reflexive  L R Eqₗ.refl  Eqᵣ.refl
    ; sym   = symmetric  L R Eqₗ.sym   Eqᵣ.sym
    ; trans = transitive L R Eqₗ.trans Eqᵣ.trans
    }
    where module Eqₗ = IsEquivalence eqₗ; module Eqᵣ = IsEquivalence eqᵣ

  isDecEquivalence : IsDecEquivalence L → IsDecEquivalence R → IsDecEquivalence (L ∩ R)
  isDecEquivalence eqₗ eqᵣ = record
    { isEquivalence = isEquivalence Eqₗ.isEquivalence Eqᵣ.isEquivalence
    ; _≟_           = decidable Eqₗ._≟_ Eqᵣ._≟_
    }
    where module Eqₗ = IsDecEquivalence eqₗ; module Eqᵣ = IsDecEquivalence eqᵣ

module _ {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} {≈ : Rel A ℓ₁} {L : Rel A ℓ₂} {R : Rel A ℓ₃} where

  isPreorder : IsPreorder ≈ L → IsPreorder ≈ R → IsPreorder ≈ (L ∩ R)
  isPreorder Oₗ Oᵣ = record
    { isEquivalence = Oₗ.isEquivalence
    ; reflexive     = implies ≈ Oₗ.reflexive Oᵣ.reflexive
    ; trans         = transitive L R Oₗ.trans Oᵣ.trans
    }
    where module Oₗ = IsPreorder Oₗ; module Oᵣ = IsPreorder Oᵣ

  isPartialOrderˡ : IsPartialOrder ≈ L → IsPreorder ≈ R → IsPartialOrder ≈ (L ∩ R)
  isPartialOrderˡ Oₗ Oᵣ = record
    { isPreorder = isPreorder Oₗ.isPreorder Oᵣ
    ; antisym    = antisymmetric ≈ L R (inj₁ Oₗ.antisym)
    }
    where module Oₗ = IsPartialOrder Oₗ; module Oᵣ = IsPreorder Oᵣ

  isPartialOrderʳ : IsPreorder ≈ L → IsPartialOrder ≈ R → IsPartialOrder ≈ (L ∩ R)
  isPartialOrderʳ Oₗ Oᵣ = record
    { isPreorder = isPreorder Oₗ Oᵣ.isPreorder
    ; antisym    = antisymmetric ≈ L R (inj₂ Oᵣ.antisym)
    }
    where module Oₗ = IsPreorder Oₗ; module Oᵣ = IsPartialOrder Oᵣ

  isStrictPartialOrderˡ : IsStrictPartialOrder ≈ L →
                          Transitive R → R Respects₂ ≈ →
                          IsStrictPartialOrder ≈ (L ∩ R)
  isStrictPartialOrderˡ Oₗ transᵣ respᵣ = record
    { isEquivalence = Oₗ.isEquivalence
    ; irrefl        = irreflexive ≈ L R (inj₁ Oₗ.irrefl)
    ; trans         = transitive L R Oₗ.trans transᵣ
    ; <-resp-≈      = respects₂ ≈ L R Oₗ.<-resp-≈ respᵣ
    }
    where module Oₗ = IsStrictPartialOrder Oₗ

  isStrictPartialOrderʳ : Transitive L → L Respects₂ ≈ →
                          IsStrictPartialOrder ≈ R →
                          IsStrictPartialOrder ≈ (L ∩ R)
  isStrictPartialOrderʳ transₗ respₗ Oᵣ = record
    { isEquivalence = Oᵣ.isEquivalence
    ; irrefl        = irreflexive ≈ L R (inj₂ Oᵣ.irrefl)
    ; trans         = transitive L R transₗ Oᵣ.trans
    ; <-resp-≈      = respects₂ ≈ L R respₗ Oᵣ.<-resp-≈
    }
    where module Oᵣ = IsStrictPartialOrder Oᵣ


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

open import lib.Basics
open import lib.NType2
open import lib.types.Pi
open import lib.types.Group

{-
    The definition of G-sets.  Thanks to Daniel Grayson.
-}

module lib.types.GroupSet {i} where

  -- The right group action with respect to the group [grp].
  record GroupSetStructure (grp : Group i) {j} (El : Type j)
    (_ : is-set El) : Type (lmax i j) where
    constructor groupset-structure
    private
      module G = Group grp
      module GS = GroupStructure G.group-struct
    field
      act : El → G.El → El
      unit-r : ∀ x → act x GS.ident == x
      assoc : ∀ x g₁ g₂ → act (act x g₁) g₂ == act x (GS.comp g₁ g₂)

  -- The definition of a G-set.  A set [El] equipped with
  -- a right group action with respect to [grp].
  record GroupSet (grp : Group i) j : Type (lsucc (lmax i j)) where
    constructor groupset
    field
      El : Type j
      El-level : is-set El
      grpset-struct : GroupSetStructure grp El El-level
    open GroupSetStructure grpset-struct public
    El-is-set = El-level

  -- A helper function to establish equivalence between two G-sets.
  -- Many data are just props and this function do the coversion for them
  -- for you.  You only need to show the non-trivial parts.
  module _ {grp : Group i} {j} {El : Type j} {El-level : is-set El} where
    private
      module G = Group grp
      module GS = GroupStructure G.group-struct
    open GroupSetStructure
    private
      groupset-structure=' : ∀ {gss₁ gss₂ : GroupSetStructure grp El El-level}
        → (act= : act gss₁ == act gss₂)
        → unit-r gss₁ == unit-r gss₂
          [ (λ act → ∀ x → act x GS.ident == x) ↓ act= ]
        → assoc gss₁ == assoc gss₂
          [ (λ act → ∀ x g₁ g₂ →
              act (act x g₁) g₂ == act x (GS.comp g₁ g₂)) ↓ act= ]
        → gss₁ == gss₂
      groupset-structure=' {groupset-structure _ _ _} {groupset-structure ._ ._ ._}
        idp idp idp = idp

    groupset-structure= : ∀ {gss₁ gss₂ : GroupSetStructure grp El El-level}
      → (∀ x g → act gss₁ x g == act gss₂ x g)
      → gss₁ == gss₂
    groupset-structure= act= = groupset-structure='
      (λ= λ x → λ= λ g → act= x g)
      (prop-has-all-paths-↓ (Π-level λ _ → El-level _ _))
      (prop-has-all-paths-↓
        (Π-level λ _ → Π-level λ _ → Π-level λ _ → El-level _ _))

  module _ {grp : Group i} {j : ULevel} where
    private
      module G = Group grp
      module GS = GroupStructure G.group-struct
    open GroupSet {grp} {j}
    private
      groupset='' : ∀ {gs₁ gs₂ : GroupSet grp j}
        → (El= : El gs₁ == El gs₂)
        → (El-level : El-level gs₁ == El-level gs₂ [ is-set ↓ El= ])
        → grpset-struct gs₁ == grpset-struct gs₂
          [ uncurry (GroupSetStructure grp) ↓ pair= El= El-level ]
        → gs₁ == gs₂
      groupset='' {groupset _ _ _} {groupset ._ ._ ._} idp idp idp = idp

      groupset=' : ∀ {gs₁ gs₂ : GroupSet grp j}
        → (El= : El gs₁ == El gs₂)
        → (El-level : El-level gs₁ == El-level gs₂ [ is-set ↓ El= ])
        → (∀ {x₁} {x₂} (p : x₁ == x₂ [ idf _ ↓ El= ]) g
            → act gs₁ x₁ g == act gs₂ x₂ g [ idf _ ↓ El= ])
        → gs₁ == gs₂
      groupset=' {groupset _ _ _} {groupset ._ ._ _} idp idp act= =
        groupset='' idp idp (groupset-structure= λ x g → act= idp g)

    groupset= : ∀ {gs₁ gs₂ : GroupSet grp j}
      → (El≃ : El gs₁ ≃ El gs₂)
      → (∀ {x₁} {x₂}
          → –> El≃ x₁ == x₂
          → ∀ g → –> El≃ (act gs₁ x₁ g) == act gs₂ x₂ g)
      → gs₁ == gs₂
    groupset= El≃ act= =
      groupset='
        (ua El≃)
        (prop-has-all-paths-↓ is-set-is-prop)
        (λ x= g → ↓-idf-ua-in El≃ $ act= (↓-idf-ua-out El≃ x=) g)

  -- The GroupSet homomorphism.
  record GroupSetHom {grp : Group i} {j}
    (gset₁ gset₂ : GroupSet grp j) : Type (lmax i j) where
    constructor groupset-hom
    open GroupSet
    field
      f : El gset₁ → El gset₂
      pres-act : ∀ g x → f (act gset₁ x g) == act gset₂ (f x) g

  private
    groupset-hom=' : ∀ {grp : Group i} {j} {gset₁ gset₂ : GroupSet grp j}
      {gsh₁ gsh₂ : GroupSetHom gset₁ gset₂}
      → (f= : GroupSetHom.f gsh₁ == GroupSetHom.f gsh₂)
      → (GroupSetHom.pres-act gsh₁ == GroupSetHom.pres-act gsh₂
        [ (λ f → ∀ g x → f (GroupSet.act gset₁ x g) == GroupSet.act gset₂ (f x) g) ↓ f= ] )
      → gsh₁ == gsh₂
    groupset-hom=' idp idp = idp

  groupset-hom= : ∀ {grp : Group i} {j} {gset₁ gset₂ : GroupSet grp j}
    {gsh₁ gsh₂ : GroupSetHom gset₁ gset₂}
    → (∀ x → GroupSetHom.f gsh₁ x == GroupSetHom.f gsh₂ x)
    → gsh₁ == gsh₂
  groupset-hom= {gset₂ = gset₂} f= =
    groupset-hom='
      (λ= f=)
      (prop-has-all-paths-↓ $
        Π-level λ _ → Π-level λ _ → GroupSet.El-level gset₂ _ _)

  group-to-group-set : ∀ (grp : Group i) → GroupSet grp i
  group-to-group-set grp = record {
    El = G.El;
    El-level = G.El-level;
    grpset-struct = record {
      act = G.comp;
      unit-r = G.unit-r;
      assoc = G.assoc}}
    where module G = Group grp

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Sets.BoolSet.Proofs{ℓ₁} where

open import Data.Boolean
open import Data.Boolean.Proofs
open import Functional
open import Logic.Propositional
open import Sets.BoolSet{ℓ₁}
open import Type

module _ {ℓ₂}{T : Type{ℓ₂}} where
  [∈]-in-[∪] : ∀{a : T}{S₁ S₂ : BoolSet(T)} → (a ∈ S₁) → (a ∈ (S₁ ∪ S₂))
  [∈]-in-[∪] proof-a = [∨]-introₗ-[𝑇] proof-a

  [∈]-in-[∩] : ∀{a : T}{S₁ S₂ : BoolSet(T)} → (a ∈ S₁) → (a ∈ S₂) → (a ∈ (S₁ ∩ S₂))
  [∈]-in-[∩] proof-a₁ proof-a₂ = [∧]-intro-[𝑇] proof-a₁ proof-a₂

  [∈]-in-[∖] : ∀{a : T}{S₁ S₂ : BoolSet(T)} → (a ∈ S₁) → (a ∉ S₂) → (a ∈ (S₁ ∖ S₂))
  [∈]-in-[∖] proof-a₁ proof-a₂ = [∧]-intro-[𝑇] proof-a₁ proof-a₂

  [∈]-in-[∁] : ∀{a : T}{S : BoolSet(T)} → (a ∉ S) → (a ∈ (∁ S))
  [∈]-in-[∁] = id

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of relations to lists
------------------------------------------------------------------------

module Relation.Binary.List.Pointwise where

open import Function
open import Function.Inverse using (Inverse)
open import Data.Product hiding (map)
open import Data.List hiding (map)
open import Level
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec using (map′)
open import Relation.Binary renaming (Rel to Rel₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

infixr 5 _∷_

data Rel {a b ℓ} {A : Set a} {B : Set b}
         (_∼_ : REL A B ℓ) : List A → List B → Set (a ⊔ b ⊔ ℓ) where
  []  : Rel _∼_ [] []
  _∷_ : ∀ {x xs y ys} (x∼y : x ∼ y) (xs∼ys : Rel _∼_ xs ys) →
        Rel _∼_ (x ∷ xs) (y ∷ ys)

head : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} {x y xs ys} →
       Rel _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
head (x∼y ∷ xs∼ys) = x∼y

tail : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} {x y xs ys} →
       Rel _∼_ (x ∷ xs) (y ∷ ys) → Rel _∼_ xs ys
tail (x∼y ∷ xs∼ys) = xs∼ys

rec : ∀ {a b c ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ}
      (P : ∀ {xs ys} → Rel _∼_ xs ys → Set c) →
      (∀ {x y xs ys} {xs∼ys : Rel _∼_ xs ys} →
         (x∼y : x ∼ y) → P xs∼ys → P (x∼y ∷ xs∼ys)) →
      P [] →
      ∀ {xs ys} (xs∼ys : Rel _∼_ xs ys) → P xs∼ys
rec P c n []            = n
rec P c n (x∼y ∷ xs∼ys) = c x∼y (rec P c n xs∼ys)

map : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
        {_≈_ : REL A B ℓ₁} {_∼_ : REL A B ℓ₂} →
      _≈_ ⇒ _∼_ → Rel _≈_ ⇒ Rel _∼_
map ≈⇒∼ []            = []
map ≈⇒∼ (x≈y ∷ xs≈ys) = ≈⇒∼ x≈y ∷ map ≈⇒∼ xs≈ys

reflexive : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
              {_≈_ : REL A B ℓ₁} {_∼_ : REL A B ℓ₂} →
            _≈_ ⇒ _∼_ → Rel _≈_ ⇒ Rel _∼_
reflexive ≈⇒∼ []            = []
reflexive ≈⇒∼ (x≈y ∷ xs≈ys) = ≈⇒∼ x≈y ∷ reflexive ≈⇒∼ xs≈ys

refl : ∀ {a ℓ} {A : Set a} {_∼_ : Rel₂ A ℓ} →
       Reflexive _∼_ → Reflexive (Rel _∼_)
refl rfl {[]}     = []
refl rfl {x ∷ xs} = rfl ∷ refl rfl

symmetric : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
              {_≈_ : REL A B ℓ₁} {_∼_ : REL B A ℓ₂} →
            Sym _≈_ _∼_ → Sym (Rel _≈_) (Rel _∼_)
symmetric sym []            = []
symmetric sym (x∼y ∷ xs∼ys) = sym x∼y ∷ symmetric sym xs∼ys

transitive :
  ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c}
    {_≋_ : REL A B ℓ₁} {_≈_ : REL B C ℓ₂} {_∼_ : REL A C ℓ₃} →
  Trans _≋_ _≈_ _∼_ → Trans (Rel _≋_) (Rel _≈_) (Rel _∼_)
transitive trans []            []            = []
transitive trans (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) =
  trans x∼y y∼z ∷ transitive trans xs∼ys ys∼zs

antisymmetric : ∀ {a ℓ₁ ℓ₂} {A : Set a}
                  {_≈_ : Rel₂ A ℓ₁} {_≤_ : Rel₂ A ℓ₂} →
                Antisymmetric _≈_ _≤_ →
                Antisymmetric (Rel _≈_) (Rel _≤_)
antisymmetric antisym []            []            = []
antisymmetric antisym (x∼y ∷ xs∼ys) (y∼x ∷ ys∼xs) =
  antisym x∼y y∼x ∷ antisymmetric antisym xs∼ys ys∼xs

respects₂ : ∀ {a ℓ₁ ℓ₂} {A : Set a}
              {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} →
            _∼_ Respects₂ _≈_ → (Rel _∼_) Respects₂ (Rel _≈_)
respects₂ {_≈_ = _≈_} {_∼_} resp =
  (λ {xs} {ys} {zs} → resp¹ {xs} {ys} {zs}) ,
  (λ {xs} {ys} {zs} → resp² {xs} {ys} {zs})
  where
  resp¹ : ∀ {xs} → (Rel _∼_ xs) Respects (Rel _≈_)
  resp¹ []            []            = []
  resp¹ (x≈y ∷ xs≈ys) (z∼x ∷ zs∼xs) =
    proj₁ resp x≈y z∼x ∷ resp¹ xs≈ys zs∼xs

  resp² : ∀ {ys} → (flip (Rel _∼_) ys) Respects (Rel _≈_)
  resp² []            []            = []
  resp² (x≈y ∷ xs≈ys) (x∼z ∷ xs∼zs) =
    proj₂ resp x≈y x∼z ∷ resp² xs≈ys xs∼zs

decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} →
            Decidable _∼_ → Decidable (Rel _∼_)
decidable dec []       []       = yes []
decidable dec []       (y ∷ ys) = no (λ ())
decidable dec (x ∷ xs) []       = no (λ ())
decidable dec (x ∷ xs) (y ∷ ys) with dec x y
... | no ¬x∼y = no (¬x∼y ∘ head)
... | yes x∼y with decidable dec xs ys
...           | no ¬xs∼ys = no (¬xs∼ys ∘ tail)
...           | yes xs∼ys = yes (x∼y ∷ xs∼ys)

isEquivalence : ∀ {a ℓ} {A : Set a} {_≈_ : Rel₂ A ℓ} →
                IsEquivalence _≈_ → IsEquivalence (Rel _≈_)
isEquivalence eq = record
  { refl  = refl       Eq.refl
  ; sym   = symmetric  Eq.sym
  ; trans = transitive Eq.trans
  } where module Eq = IsEquivalence eq

isPreorder : ∀ {a ℓ₁ ℓ₂} {A : Set a}
               {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} →
             IsPreorder _≈_ _∼_ → IsPreorder (Rel _≈_) (Rel _∼_)
isPreorder pre = record
  { isEquivalence = isEquivalence Pre.isEquivalence
  ; reflexive     = reflexive     Pre.reflexive
  ; trans         = transitive    Pre.trans
  } where module Pre = IsPreorder pre

isDecEquivalence : ∀ {a ℓ} {A : Set a}
                     {_≈_ : Rel₂ A ℓ} → IsDecEquivalence _≈_ →
                   IsDecEquivalence (Rel _≈_)
isDecEquivalence eq = record
  { isEquivalence = isEquivalence DE.isEquivalence
  ; _≟_           = decidable     DE._≟_
  } where module DE = IsDecEquivalence eq

isPartialOrder : ∀ {a ℓ₁ ℓ₂} {A : Set a}
                   {_≈_ : Rel₂ A ℓ₁} {_≤_ : Rel₂ A ℓ₂} →
                 IsPartialOrder _≈_ _≤_ →
                 IsPartialOrder (Rel _≈_) (Rel _≤_)
isPartialOrder po = record
  { isPreorder = isPreorder    PO.isPreorder
  ; antisym    = antisymmetric PO.antisym
  } where module PO = IsPartialOrder po

preorder : ∀ {p₁ p₂ p₃} → Preorder p₁ p₂ p₃ → Preorder _ _ _
preorder p = record
  { isPreorder = isPreorder (Preorder.isPreorder p)
  }

setoid : ∀ {c ℓ} → Setoid c ℓ → Setoid _ _
setoid s = record
  { isEquivalence = isEquivalence (Setoid.isEquivalence s)
  }

decSetoid : ∀ {c ℓ} → DecSetoid c ℓ → DecSetoid _ _
decSetoid d = record
  { isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence d)
  }

poset : ∀ {c ℓ₁ ℓ₂} → Poset c ℓ₁ ℓ₂ → Poset _ _ _
poset p = record
  { isPartialOrder = isPartialOrder (Poset.isPartialOrder p)
  }

-- Rel _≡_ coincides with _≡_.

Rel≡⇒≡ : ∀ {a} {A : Set a} → Rel {A = A} _≡_ ⇒ _≡_
Rel≡⇒≡ []               = P.refl
Rel≡⇒≡ (P.refl ∷ xs∼ys) with Rel≡⇒≡ xs∼ys
Rel≡⇒≡ (P.refl ∷ xs∼ys) | P.refl = P.refl

≡⇒Rel≡ : ∀ {a} {A : Set a} → _≡_ ⇒ Rel {A = A} _≡_
≡⇒Rel≡ P.refl = refl P.refl

Rel↔≡ : ∀ {a} {A : Set a} →
        Inverse (setoid (P.setoid A)) (P.setoid (List A))
Rel↔≡ = record
  { to         = record { _⟨$⟩_ = id; cong = Rel≡⇒≡ }
  ; from       = record { _⟨$⟩_ = id; cong = ≡⇒Rel≡ }
  ; inverse-of = record
    { left-inverse-of  = λ _ → refl P.refl
    ; right-inverse-of = λ _ → P.refl
    }
  }

decidable-≡ : ∀ {a} {A : Set a} →
              Decidable {A = A} _≡_ → Decidable {A = List A} _≡_
decidable-≡ dec xs ys = Dec.map′ Rel≡⇒≡ ≡⇒Rel≡ (xs ≟ ys)
  where
  open DecSetoid (decSetoid (P.decSetoid dec))


text:
data ℕ : Set where
  ze : ℕ
  su : ℕ → ℕ

f : (ℕ → ℕ) → ℕ → ℕ
f g n = g n

syntax f g n = n , g

h : ℕ
h = ?