text:
{-# OPTIONS --safe #-}
{-
Constructions of "sets" in the cumulative hierarchy. Including:
- the empty set
- unions
- ω
- replacement
- separation
-}

module Cubical.HITs.CumulativeHierarchy.Constructions where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure
open import Cubical.Functions.Embedding
open import Cubical.Functions.Logic as L
open import Cubical.Data.Sum hiding (elim)
open import Cubical.Data.Sigma
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.Sum as ⊎ using (_⊎_)
open import Cubical.Data.Bool
open import Cubical.Data.Unit
open import Cubical.Data.Empty as E hiding (elim)
open import Cubical.HITs.PropositionalTruncation as P hiding (elim; elim2)

open import Cubical.HITs.CumulativeHierarchy.Base
open import Cubical.HITs.CumulativeHierarchy.Properties
import Cubical.HITs.PropositionalTruncation.Monad as PropMonad

private
  variable
    ℓ ℓ' : Level

------------
-- Structures for building specific sets by giving encodings and decodings for their membership
-----------

record SetStructure ℓ : Type (ℓ-suc ℓ) where
  field
    X : Type ℓ
    ix : X → V ℓ
  resSet : V ℓ
  resSet = sett X ix

record SetPackage ℓ ℓ' : Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) where
  field
    structure : SetStructure ℓ
  open SetStructure structure hiding (resSet)
  open SetStructure structure using (resSet) public
  field
    ∈-rep : V ℓ → hProp ℓ'
    unpack : (x : X) → ⟨ ∈-rep (ix x) ⟩
    repack : {y : V ℓ} → ⟨ ∈-rep y ⟩ → ∥ fiber ix y ∥₁

  open PropMonad
  classification : ⟨ ∀[ y ] (y ∈ₛ resSet ⇔ ∈-rep y) ⟩
  classification y = intoClassifier , fromClassifier where
    intoClassifier : ⟨ y ∈ₛ resSet ⟩ → ⟨ ∈-rep y ⟩
    intoClassifier (yi , yr) = proof (∈-rep y) by do
      (x , ix) ← ∈∈ₛ {b = resSet} .snd (yi , yr)
      return (subst (fst ∘ ∈-rep) ix (unpack x))
    fromClassifier : ⟨ ∈-rep y ⟩ → ⟨ y ∈ₛ resSet ⟩
    fromClassifier yr = ∈∈ₛ {b = resSet} .fst (repack {y = y} yr)

------------
-- Specific constructions
-----------
open SetPackage using (structure; ∈-rep; unpack; repack)

module EmptySet where
  EmptyStructure : SetStructure ℓ
  SetStructure.X EmptyStructure = Lift E.⊥
  SetStructure.ix EmptyStructure ()

  EmptyPackage : SetPackage ℓ ℓ-zero
  structure EmptyPackage = EmptyStructure
  ∈-rep EmptyPackage _ = L.⊥
  unpack EmptyPackage ()
  repack EmptyPackage ()

  ∅ : V ℓ
  ∅ = SetStructure.resSet EmptyStructure

  ∅-empty : ⟨ ∀[ b ∶ V ℓ ] ¬ (b ∈ₛ ∅) ⟩
  ∅-empty b = SetPackage.classification EmptyPackage b .fst
open EmptySet using (∅; ∅-empty) public

module UnionSet (S : V ℓ) where
  UnionStructure : SetStructure ℓ
  SetStructure.X UnionStructure = Σ[ r ∈ ⟪ S ⟫ ] ⟪ ⟪ S ⟫↪ r ⟫
  SetStructure.ix UnionStructure (r , i) = ⟪ ⟪ S ⟫↪ r ⟫↪ i

  UNION : V ℓ
  UNION = SetStructure.resSet UnionStructure

  UnionPackage : SetPackage _ (ℓ-suc ℓ)
  structure UnionPackage = UnionStructure
  ∈-rep UnionPackage y = ∃[ v ] (v ∈ₛ S) ⊓ (y ∈ₛ v)
  unpack UnionPackage (vi , yi) = ∣ ⟪ S ⟫↪ vi , ∈ₛ⟪ S ⟫↪ vi , ∈ₛ⟪ ⟪ S ⟫↪ vi ⟫↪ yi ∣₁
  repack UnionPackage {y = y} = P.rec squash₁ go where
    go : Σ[ v ∈ V _ ] ⟨ v ∈ₛ S ⟩ ⊓′ ⟨ y ∈ₛ v ⟩ → ∥ fiber _ y ∥₁
    go (v , (vi , vS) , xv) = ∣ repFiber≃fiber _ _ .fst ((vi , key .fst) , key .snd) ∣₁ where
      path : v ≡ ⟪ S ⟫↪ vi
      path = sym (equivFun identityPrinciple vS)
      key : Σ[ i ∈ ⟪ ⟪ S ⟫↪ vi ⟫ ] ⟪ ⟪ S ⟫↪ vi ⟫↪ i ≊ y
      key = subst (λ v → Σ[ ix ∈ ⟪ v ⟫ ] ⟪ v ⟫↪ ix ≊ y) path xv

  union-ax : ⟨ ∀[ u ] (u ∈ₛ UNION ⇔ (∃[ v ] (v ∈ₛ S) ⊓ (u ∈ₛ v))) ⟩
  union-ax = classification where
    open SetPackage UnionPackage using (classification)
open UnionSet renaming (UNION to infixr 9 ⋃_) using (union-ax) public

module PairingSet (a b : V ℓ) where
  PairingStructure : SetStructure ℓ
  SetStructure.X PairingStructure = Lift Bool
  SetStructure.ix PairingStructure (lift false) = a
  SetStructure.ix PairingStructure (lift true) = b

  open PropMonad
  PairingPackage : SetPackage _ (ℓ-suc ℓ)
  structure PairingPackage = PairingStructure
  ∈-rep PairingPackage d = (d ≡ₕ a) ⊔ (d ≡ₕ b)
  unpack PairingPackage (lift false) = L.inl refl
  unpack PairingPackage (lift true) = L.inr refl
  repack PairingPackage {y = y} = _>>= λ where
    (_⊎_.inl ya) → ∣ lift false , sym ya ∣₁
    (_⊎_.inr yb) → ∣ lift true , sym yb ∣₁

  PAIR : V ℓ
  PAIR = SetStructure.resSet PairingStructure

  pairing-ax : ⟨ ∀[ d ] (d ∈ₛ PAIR ⇔ (d ≡ₕ a) ⊔ (d ≡ₕ b)) ⟩
  pairing-ax = classification where
    open SetPackage PairingPackage using (classification)
-- pairing TODO: notation?
open PairingSet renaming (PAIR to infix 12 ⁅_,_⁆) using (pairing-ax) public

module SingletonSet (a : V ℓ) where
  SingletonStructure : SetStructure ℓ
  SetStructure.X SingletonStructure = Lift Unit
  SetStructure.ix SingletonStructure (lift tt) = a

  SingletonPackage : SetPackage _ (ℓ-suc ℓ)
  structure SingletonPackage = SingletonStructure
  ∈-rep SingletonPackage d = d ≡ₕ a
  unpack SingletonPackage _ = refl
  repack SingletonPackage ya = ∣ lift tt , sym ya ∣₁

  SINGL : V ℓ
  SINGL = SetStructure.resSet SingletonStructure
open SingletonSet renaming (SINGL to infix 10 ⁅_⁆s) public

-- small unions
_∪_ : (a b : V ℓ) → V ℓ
a ∪ b = ⋃ ⁅ a , b ⁆

module InfinitySet {ℓ} where
  sucV : V ℓ → V ℓ
  sucV N = N ∪ ⁅ N ⁆s

  #_ : ℕ → V ℓ
  # zero = ∅
  # suc n = sucV (# n)

  ωStructure : SetStructure ℓ
  SetStructure.X ωStructure = Lift ℕ
  SetStructure.ix ωStructure = #_ ∘ lower

  ω : V ℓ
  ω = SetStructure.resSet ωStructure

  open PropMonad
  ωPackage : SetPackage _ (ℓ-suc ℓ)
  structure ωPackage = ωStructure
  ∈-rep ωPackage d = (d ≡ₕ ∅) ⊔ (∃[ v ] (d ≡ₕ sucV v) ⊓ (v ∈ₛ ω))
  unpack ωPackage (lift zero) = L.inl refl
  unpack ωPackage (lift (suc n)) = L.inr ∣ # n , refl , ∈∈ₛ {b = ω} .fst ∣ lift n , refl ∣₁ ∣₁
  repack ωPackage {y = y} = ⊔-elim (y ≡ₕ ∅) ∥ _ ∥ₚ (λ _ → ∥ fiber _ y ∥ₚ)
    (λ e → ∣ lift zero , sym e ∣₁)
    (λ m → do (v , yv , vr) ← m
              (lift n , eq) ← ∈∈ₛ {b = ω} .snd vr
              ∣ lift (suc n) , sym (subst (λ v → y ≡ (v ∪ ⁅ v ⁆s)) (sym eq) yv) ∣₁
    )

  infinity-ax : ⟨ ∀[ y ] (y ∈ₛ ω ⇔ (y ≡ₕ ∅) ⊔ (∃[ v ] (y ≡ₕ sucV v) ⊓ (v ∈ₛ ω))) ⟩
  infinity-ax = classification where
    open SetPackage ωPackage using (classification)

  ω-empty : ⟨ ∅ ∈ₛ ω ⟩
  ω-empty = infinity-ax ∅ .snd (L.inl refl)

  ω-next : ⟨ ∀[ x ∶ V ℓ ] x ∈ₛ ω ⇒ sucV x ∈ₛ ω ⟩
  ω-next x x∈ω = infinity-ax (sucV x) .snd (L.inr ∣ x , refl , x∈ω ∣₁)

  #-in-ω : ∀ n → ⟨ # n ∈ₛ ω ⟩
  #-in-ω zero = ω-empty
  #-in-ω (suc n) = ω-next (# n) (#-in-ω n)

open InfinitySet using (ω; ω-empty; ω-next; infinity-ax) public

module ReplacementSet (r : V ℓ → V ℓ) (a : V ℓ) where
  ReplacementStructure : SetStructure ℓ
  SetStructure.X ReplacementStructure = ⟪ a ⟫
  SetStructure.ix ReplacementStructure = r ∘ ⟪ a ⟫↪

  REPLACED : V ℓ
  REPLACED = SetStructure.resSet ReplacementStructure

  open PropMonad
  ReplacementPackage : SetPackage _ (ℓ-suc ℓ)
  structure ReplacementPackage = ReplacementStructure
  ∈-rep ReplacementPackage y = ∃[ z ] (z ∈ₛ a) ⊓ (y ≡ₕ r z)
  unpack ReplacementPackage ⟪a⟫ = ∣ ⟪ a ⟫↪ ⟪a⟫ , (∈ₛ⟪ a ⟫↪ ⟪a⟫) , refl ∣₁
  repack ReplacementPackage {y = y} m = do
    (z , (a , za) , yr) ← m
    ∣ a , cong r (equivFun identityPrinciple za) ∙ sym yr ∣₁

  replacement-ax : ⟨ ∀[ y ] (y ∈ₛ REPLACED ⇔ (∃[ z ] (z ∈ₛ a) ⊓ (y ≡ₕ r z))) ⟩
  replacement-ax y = classification y where
    open SetPackage ReplacementPackage using (classification)
open ReplacementSet renaming (REPLACED to infix 12 ⁅_∣_⁆) using (replacement-ax) public

module SeparationSet (a : V ℓ) (ϕ : V ℓ → hProp ℓ) where
  SeparationStructure : SetStructure ℓ
  SetStructure.X SeparationStructure = Σ[ x ∈ ⟪ a ⟫ ] ⟨ ϕ (⟪ a ⟫↪ x) ⟩
  SetStructure.ix SeparationStructure = ⟪ a ⟫↪ ∘ fst

  SeparationPackage : SetPackage _ ℓ
  structure SeparationPackage = SeparationStructure
  ∈-rep SeparationPackage y = (y ∈ₛ a) ⊓ ϕ y
  unpack SeparationPackage (⟪a⟫ , phi) = (∈ₛ⟪ a ⟫↪ ⟪a⟫) , phi
  repack SeparationPackage ((⟪a⟫ , ya) , phi) =
    ∣ (⟪a⟫ , subst (fst ∘ ϕ) (sym (equivFun identityPrinciple ya)) phi)
      , equivFun identityPrinciple ya ∣₁

  SEPAREE : V ℓ
  SEPAREE = SetStructure.resSet SeparationStructure

  separation-ax : ⟨ ∀[ y ] (y ∈ₛ SEPAREE ⇔ (y ∈ₛ a) ⊓ ϕ y) ⟩
  separation-ax y = classification y .fst , classification y .snd where
    open SetPackage SeparationPackage using (classification)
open SeparationSet renaming (SEPAREE to infix 12 ⁅_∶_⁆) using (separation-ax) public

module Examples where
  open InfinitySet

  the1 : V ℓ-zero
  the1 = # 1

  1-ok? : ∥ Bool ∥₁
  1-ok? = do
    prf ← infinity-ax the1 .fst (#-in-ω 1)
    case prf of λ { (⊎.inl _) → ∣ false ∣₁ ; (⊎.inr _) → ∣ true ∣₁ }
    where
    open PropMonad
  test : 1-ok? ≡ ∣ true ∣₁
  test = refl

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module A1 where

open import Data.Empty using (⊥)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
open import Data.Unit using (⊤; tt)
open import Data.Bool using (Bool; false; true; _xor_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; Σ; Σ-syntax)
open import Data.Nat using (ℕ; suc; _+_; _*_)
open import Data.List using (List; []; _++_)
open import Data.Vec using (Vec; []; _∷_) renaming (_++_ to _++V_)

------------------------------------------------------------------------------
-- Ch. 1
-- Theme: for each type, recursion principle and induction principle

------------------------------------------------------------------------------
-- Sec. 1.9
-- ℕ

recℕ : ∀ {ℓ} → (C : Set ℓ) → C → (ℕ → C → C) → ℕ → C
recℕ C z f 0 = z
recℕ C z f (suc n) = f n (recℕ C z f n)

indℕ : ∀ {ℓ} → (C : ℕ → Set ℓ) → C 0 → ((n : ℕ) → C n → C (suc n)) → (n : ℕ) → C n
indℕ C z f 0 = z
indℕ C z f (suc n) = f n (indℕ C z f n)

-- Many examples in L.agda

------------------------------------------------------------------------------
-- Sec. 1.7
-- Empty type

-- Ex falso quodlibet

rec⊥ : ∀ {ℓ} → (C : Set ℓ) → ⊥ → C
rec⊥ C ()

ind⊥ : ∀ {ℓ} → (C : ⊥ → Set ℓ) → (v : ⊥) → C v
ind⊥ C ()

-- Examples

⊥→1≡2 : ⊥ → (1 ≡ 2)
⊥→1≡2 = rec⊥ (1 ≡ 2)

⊥→⊤≡⊥ : ⊥ → ⊤
⊥→⊤≡⊥ = rec⊥ ⊤

⊥→⊤≡⊥' : ⊥ → ⊤
⊥→⊤≡⊥' = ind⊥ (λ v → ⊤)

------------------------------------------------------------------------------
-- Sec. 1.5
-- Unit type

rec⊤ : ∀ {ℓ} → (C : Set ℓ) → C → ⊤ → C
rec⊤ C c tt = c

ind⊤ : ∀ {ℓ} → (C : ⊤ → Set ℓ) → C tt → (u : ⊤) → C u
ind⊤ C c tt = c

-- Example

singleton⊤ : (u : ⊤) → (u ≡ tt)
singleton⊤ = ind⊤ (λ u → u ≡ tt) refl

------------------------------------------------------------------------------
-- Sec. 1.8
-- Booleans

recBool : ∀ {ℓ} → (C : Set ℓ) → C → C → Bool → C
recBool C el th false = el
recBool C el th true = th

indBool : ∀ {ℓ} → (C : Bool → Set ℓ) → C false → C true → (b : Bool) → C b
indBool C el th false = el
indBool C el th true = th

-- Example

bool2 : (b : Bool) → (b ≡ false) ⊎ (b ≡ true)
bool2 = indBool
          (λ b → (b ≡ false) ⊎ (b ≡ true))
          (inj₁ refl)
          (inj₂ refl)

------------------------------------------------------------------------------
-- Sec. 1.5
-- Product types

rec× : ∀ {ℓ₁ ℓ₂ ℓ₃} → {A : Set ℓ₁} {B : Set ℓ₂} →
      (C : Set ℓ₃) → (A → B → C) → A × B → C
rec× C g (a , b) = g a b

ind× : ∀ {ℓ₁ ℓ₂ ℓ₃} → {A : Set ℓ₁} {B : Set ℓ₂} → (C : A × B → Set ℓ₃) →
       ((a : A) → (b : B) → C (a , b)) → (p : A × B) → C p
ind× C g ( a , b ) = g a b

-- Examples

fst : {A B : Set} → A × B → A
fst {A} {B} = rec× A (λ a b → a)

snd : {A B : Set} → A × B → B
snd {A} {B} = rec× B (λ a b → b)

surj-pair : ∀ {A B} → (p : A × B) → (fst p , snd p) ≡ p
surj-pair = ind×
              (λ p → (fst p , snd p) ≡ p)
              (λ a b → refl)

-- IMPORTANT:
--
-- TO PROVE ANY PROPERTY OF SOMETHING OF TYPE A × B, IT IS SUFFICIENT
-- TO PROVE IT FOR CANONICAL VALUES OF THAT TYPE, i.e. FOR (a , b)
--

_Product_ : (A : Set) → (B : Set) → Set
A Product B = (z : Bool) → recBool Set A B z

pair : {A B : Set} → A → B → A Product B
pair {A} {B} a b = indBool (λ z → recBool Set A B z) a b

------------------------------------------------------------------------------
-- Sigma types (dependent pair type)

recΣ : ∀ {ℓ₁ ℓ₂ ℓ₃} → {A : Set ℓ₁} {B : A → Set ℓ₂} → (C : Set ℓ₃) →
       ((a : A) → B a → C) → Σ A B → C
recΣ C g (a , b) = g a b

indΣ : ∀ {ℓ₁ ℓ₂ ℓ₃} → {A : Set ℓ₁} {B : A → Set ℓ₂} → (C : Σ A B → Set ℓ₃) →
        ((a : A) → (b : B a) → C (a , b)) → (p : Σ A B) → C p
indΣ C g ( a , b ) = g a b

-- Examples

dfst : {A : Set} {B : A → Set} → Σ A B → A
dfst {A} {B} = recΣ A (λ a b → a)

dsnd : {A : Set} {B : A → Set} → (p : Σ A B) → B (dfst p)
dsnd {A} {B} = indΣ
                 (λ p → B (dfst p))
                 (λ a b → b)

ac : {A B : Set} {R : A → B → Set} →
     ((x : A) → (Σ[ y ∈ B ] (R x y))) →
     (Σ[ f ∈ (A → B) ] ((x : A) → R x (f x)))
ac g = (λ x → dfst (g x)) , (λ x → dsnd (g x))

{-- In English :-)

If for all x, exists y, such that x R y, then
exists f such that for all x, x R f(x)

... this is one type-theoretic "axiom of choice"

--}

Magma : Set₁
Magma = Σ[ A ∈ Set ] (A → A → A)

m₁ m₂ m₃ m₄ m₅ : Magma
m₁ = (ℕ , _+_)
m₂ = (ℕ , _*_)
m₃ = (Bool , _xor_)
m₄ = (List Bool , _++_)
m₅ = (⊥ , λ ())

PointedMagma : Set₁
PointedMagma = Σ[ A ∈ Set ] ((A → A → A) × A)

pm₁ pm₂ pm₃ pm₄ : PointedMagma
pm₁ = (ℕ , _+_ , 0)
pm₂ = (ℕ , _*_ , 1)
pm₃ = (Bool , _xor_ , false)
pm₄ = (List Bool , _++_ , [])

------------------------------------------------------------------------------
-- Sum types (coproducts)

rec⊎ : ∀ {ℓ₁ ℓ₂ ℓ₃} → {A : Set ℓ₁} {B : Set ℓ₂} →
       (C : Set ℓ₃) → (A → C) → (B → C) → (A ⊎ B → C)
rec⊎ C f g (inj₁ a) = f a
rec⊎ C f g (inj₂ b) = g b

ind⊎ : ∀ {ℓ₁ ℓ₂ ℓ₃} → {A : Set ℓ₁} {B : Set ℓ₂} → (C : A ⊎ B → Set ℓ₃) →
        ((a : A) → C (inj₁ a)) → ((b : B) → C (inj₂ b)) → ((x : A ⊎ B) → C x)
ind⊎ C f g (inj₁ a) = f a
ind⊎ C f g (inj₂ b) = g b

-- Examples

_Union_ : (A : Set) → (B : Set) → Set
A Union B = Σ[ b ∈ Bool ] (recBool Set A B b)

inLeft : {A B : Set} → A → A Union B
inLeft a = (false , a)

inRight : {A B : Set} → B → A Union B
inRight b = (true , b)

------------------------------------------------------------------------------
-- Induction principle for vectors

indVec : {A : Set} → (C : {n : ℕ} → Vec A n → Set) →
         C [] →
         ({m : ℕ} → (x : A) → (xs : Vec A m) → C xs → C (x ∷ xs)) →
         ({n : ℕ} → (xs : Vec A n) → C xs)
indVec C cnil ccons [] = cnil
indVec C cnil ccons (x ∷ xs) = ccons x xs (indVec C cnil ccons xs)

-- Example

[]++v≡v : ∀ {A n} → (v : Vec A n) → [] ++V v ≡ v
[]++v≡v {A} {n} = indVec
                    (λ v → [] ++V v ≡ v)
                    refl
                    (λ x xs p → refl)
postulate
  n+0≡n : ∀ {n} → n + 0 ≡ n

v++[]≡v : ∀ {n} {A : Set} → (v : Vec A n) →
        (subst (λ n -> Vec A n) n+0≡n (v ++V [])) ≡ v
v++[]≡v {A} {n} = {!!}

------------------------------------------------------------------------------
-- Obvious omission from list of types

-- No induction principle for functions

------------------------------------------------------------------------------
-- Propositions as types

¬ : Set → Set
¬ A = A → ⊥

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

ext: agda

max_stars_repo_name: andmkent/misc-HoTT

max_issues_repo_name: andmkent/misc-HoTT

max_forks_repo_name: andmkent/misc-HoTT


text:
module x02-842Induction-hc where

import Relation.Binary.PropositionalEquality as Eq
open   Eq using (_≡_; refl; cong; sym)
open   Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

-- associativity

_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 + 4) + 5  ≡⟨⟩
         7  + 5  ≡⟨⟩
    12           ≡⟨⟩
    3 +  9       ≡⟨⟩
    3 + (4 + 5)
  ∎

+-identityᴸ : ∀ (m : ℕ) → zero + m ≡ m
+-identityᴸ m = refl -- via def/eq

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ   zero  = refl
+-identityʳ (suc m)         -- suc  m + zero  ≡ suc m
                            -- suc (m + zero) ≡ suc m
  rewrite +-identityʳ m     -- suc  m         ≡ suc m
  = refl

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc   zero  n p = refl
+-assoc (suc m) n p         -- suc  m +  n + p   ≡ suc  m + (n + p)
                            -- suc (m +  n + p)  ≡ suc (m + (n + p))
  rewrite +-assoc m n p     -- suc (m + (n + p)) ≡ suc (m + (n + p))
  = refl

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc   zero  n = refl
+-suc (suc m) n             -- suc  (m + suc n)  ≡ suc (suc (m + n))
  rewrite +-suc m n         -- suc (suc (m + n)) ≡ suc (suc (m + n))
  = refl

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm zero n               -- zero + n          ≡ n + zero
                            --        n          ≡ n + zero
  rewrite +-identityʳ n     --        n          ≡ n
  = refl
+-comm (suc m)   zero       -- suc  m + zero     ≡ zero + suc m
                            -- suc (m + zero)    ≡ suc m
  rewrite +-identityʳ m     -- suc  m            ≡ suc m
  = refl
+-comm (suc m) (suc n)      -- suc  m + suc n    ≡ suc  n + suc m
                            -- suc (m + suc n)   ≡ suc (n + suc m)
  rewrite
    +-suc m n               -- suc (suc (m + n)) ≡ suc (n + suc m)
  | +-suc n m               -- suc (suc (m + n)) ≡ suc (suc (n + m))
  | +-comm m n              -- suc (suc (n + m)) ≡ suc (suc (n + m))
  = refl

-- without using induction/recursion
+-swap : ∀ (m n p : ℕ) → (m + n) + p ≡ n + (m + p)
+-swap   zero  n p = refl
+-swap (suc m) n p          -- suc  m +  n + p   ≡ n + (suc  m + p)
                            -- suc (m +  n + p)  ≡ n + suc  (m + p)
  rewrite
    +-suc n (m + p)         -- suc (m +  n + p)  ≡ suc (n + (m + p))
  | +-comm m n              -- suc (n +  m + p)  ≡ suc (n + (m + p))
  | +-assoc n m p           -- suc (n + (m + p)) ≡ suc (n + (m + p))
  = refl

-- addition distributes over multiplication
*-+-rdistrib : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-+-rdistrib   zero  n p = refl
*-+-rdistrib (suc m) n p       --     (suc m + n) * p ≡ suc m * p + n * p
                               --     p + (m + n) * p ≡ p + m * p + n * p
  rewrite
    *-+-rdistrib m n p         -- p + (m * p + n * p) ≡ p + m * p + n * p
  | +-assoc p (m * p) (n * p)  -- p + (m * p + n * p) ≡ p + (m * p + n * p)
  = refl

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc   zero  n p = refl
*-assoc (suc m) n p            --       suc m * n * p ≡ suc m * (n * p)
                               --     (n + m * n) * p ≡ n * p + m * (n * p)
  rewrite
    *-+-rdistrib n (m * n) p   -- n * p + m *  n * p  ≡ n * p + m * (n * p)
  | *-assoc m n p              -- n * p + m * (n * p) ≡ n * p + m * (n * p)
  = refl

*0 : ∀ (n : ℕ) → n * zero ≡ zero
*0    zero = refl
*0 (suc n) = *0 n

*-suc : ∀ (m n : ℕ) → m * suc n ≡ m + (m * n)
*-suc   zero  n = refl
*-suc (suc m) n                --         suc m * suc n ≡ suc  m +  suc m * n
                               -- suc (n + m  * suc n)  ≡ suc (m + (n + m * n))
  rewrite
    *-suc m n                  -- suc (n + (m + m * n)) ≡ suc (m + (n + m * n))
  | sym (+-assoc n m (m * n))  -- suc (n +  m + m * n)  ≡ suc (m + (n + m * n))
  | +-comm n m                 -- suc (m +  n + m * n)  ≡ suc (m + (n + m * n))
  | +-assoc m n (m * n)        -- suc (m + (n + m * n)) ≡ suc (m + (n + m * n))
  = refl

*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm   zero  n rewrite *0 n = refl
*-comm (suc m) n               -- suc m * n ≡ n * suc m
                               -- n + m * n ≡ n * suc m
  rewrite
    *-suc n m                  -- n + m * n ≡ n + n * m
  | *-comm m n                 -- n + n * m ≡ n + n * m
  = refl

0∸n≡0 : ∀ (m : ℕ) → zero ∸ m ≡ zero
0∸n≡0   zero  = refl
0∸n≡0 (suc m) rewrite 0∸n≡0 m = refl

-- form of associativity for monus
∸-+-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc   zero     n    p    --  zero ∸ n ∸ p ≡ zero ∸ (n + p)
  rewrite
    0∸n≡0 n                    --         0 ∸ p ≡ 0    ∸ (n + p)
  | 0∸n≡0 p                    --             0 ≡ 0    ∸ (n + p)
  | 0∸n≡0 (n + p)              --             0 ≡ 0
  = refl
∸-+-assoc      m  zero    p    --   m      ∸ p  ≡ m ∸      p
  = refl
∸-+-assoc      m     n zero    --   m ∸  n      ≡ m ∸ (n + zero)
  rewrite +-identityʳ n        --   m ∸  n      ≡ m ∸  n
  = refl
∸-+-assoc (suc m) (suc n) p    --   m ∸  n ∸ p  ≡ m ∸ (n + p)
  rewrite ∸-+-assoc m n p      --   m ∸ (n + p) ≡ m ∸ (n + p)
  = refl

------------------------------------------------------------------------------
-- properties of binary representation

-- BEGIN copied from 842Naturals

data Bin-ℕ : Set where
  bits : Bin-ℕ
  _x0 : Bin-ℕ → Bin-ℕ
  _x1 : Bin-ℕ → Bin-ℕ

dbl : ℕ → ℕ
dbl zero = zero
dbl (suc n) = suc (suc (dbl n))

inc : Bin-ℕ → Bin-ℕ
inc  bits  =  bits x1
inc (m x0) =     m x1
inc (m x1) = inc m x0

tob : ℕ → Bin-ℕ
tob   zero   = bits
tob (suc m)  = inc (tob m)

fromb : Bin-ℕ → ℕ
fromb  bits  = 0
fromb (n x0) =      dbl (fromb n)
fromb (n x1) = suc (dbl (fromb n))

_bin-+_ : Bin-ℕ → Bin-ℕ → Bin-ℕ
bl      bin-+   bits  =       bl
bits    bin-+  br     =                br
(bl x0) bin-+ (br x0) =      (bl bin-+ br) x0
(bl x0) bin-+ (br x1) =      (bl bin-+ br) x1
(bl x1) bin-+ (br x0) =      (bl bin-+ br) x1
(bl x1) bin-+ (br x1) = inc ((bl bin-+ br) x1)

-- END copied from 842Naturals

dblb : Bin-ℕ → Bin-ℕ
dblb b = b x0

_ : dblb (tob 3) ≡ tob  6
_ = refl
_ : dblb (tob 7) ≡ tob 14
_ = refl
_ : dblb (tob 9) ≡ tob 18
_ = refl

from∘inc : ∀ (b : Bin-ℕ) → fromb (inc b) ≡ suc (fromb b)
from∘inc  bits  = refl
from∘inc (b x0) = refl
from∘inc (b x1)            --          fromb (inc (b x1)) ≡      suc      (fromb (b x1))
                           --     dbl (fromb (inc  b))    ≡ suc (suc (dbl (fromb  b)))
  rewrite from∘inc b       -- suc (suc (dbl (fromb b)))   ≡ suc (suc (dbl (fromb  b)))
  = refl

from∘tob : ∀ (m : ℕ) → fromb (tob m) ≡ m
from∘tob   zero  = refl
from∘tob (suc m)           -- fromb (tob (suc m)) ≡ suc m
                           -- fromb (inc (tob m)) ≡ suc m
  rewrite
    from∘inc (tob m)       -- suc (fromb (tob m)) ≡ suc m
  | from∘tob      m        -- suc             m   ≡ suc m
  = refl

-- The property ∀ (m : Bin-ℕ) → tob (fromb m) ≡ m cannot be proved.
-- Because there are two representations of zero.
-- The following restriction can be proved:

to/from-corr : ∀ (b : Bin-ℕ) (n : ℕ) → b ≡ tob n → fromb b ≡ n --  TODO
to/from-corr b n b≡tn = {!!}

dblb∘inc : ∀ (b : Bin-ℕ) → dblb (inc b) ≡ inc (inc (dblb b))
dblb∘inc  bits  = refl
dblb∘inc (b x0)             -- dblb (inc (b x0)) ≡ inc (inc (dblb (b     x0)))
                            --      dblb (b x1)  ≡               ((b x1) x0)
  rewrite dblb∘inc b        --       ((b x1) x0) ≡               ((b x1) x0)
  = refl
dblb∘inc (b x1)             -- dblb (inc (b x1)) ≡ inc (inc (dblb (b x1)))
                            -- dblb (inc  b x0)  ≡    ((inc b x0) x0)
  rewrite dblb∘inc b        --   ((inc b x0) x0) ≡ ((inc b x0) x0)
  = refl
{-
-- more BIN properties to prove

-- not sure this can be proved because of multiple representations of zero
to∘dbl : ∀ (m : ℕ) → tob (dbl m) ≡ dblb (tob m) -- TODO -- not sure if provable because of zero
to∘dbl   zero               -- tob (dbl zero) ≡ dblb (tob zero)
                            --           bits ≡ dblb bits
  = {!!}
to∘dbl (suc m)              --       tob (dbl (suc m)) ≡ dblb (tob (suc m))
                            -- inc (inc (tob (dbl m))) ≡ dblb (inc (tob m))
  rewrite to∘dbl m          --     (inc (tob m) x0)    ≡ (inc (tob m) x0)
  = refl

from∘dblb : ∀ (b : Bin-ℕ) → fromb (dblb b) ≡ dbl (fromb b)
from∘dblb b = refl

-- bit version of second case for unary addition: suc m + n = suc (m + n)
-- useful in the next proof
-- hint: use induction on both parameters
bin-+-linc : ∀ (b1 b2 : Bin-ℕ) → (inc b1) bin-+ b2 ≡ inc (b1  bin-+ b2) -- TODO
bin-+-linc   b1   bits = refl
bin-+-linc bits (b2 x0) = {!!}
bin-+-linc bits (b2 x1) = {!!}
bin-+-linc (b1 x0) b2  = {!!}
bin-+-linc (b1 x1) b2  = {!!}

-- 842 exercise: PlusUnaryBinary (2 points)
-- This theorem relates unary and binary addition.

to∘+ : ∀ (m n : ℕ) → tob (m + n) ≡ tob m bin-+ tob n --  TODO
to∘+ m n = {!!}
-}

{-
The follwing theorems can be found in:
import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)

-- Unicode

    ∀  U+2200  FOR ALL (\forall, \all)
    ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)
    ′  U+2032  PRIME (\')
    ″  U+2033  DOUBLE PRIME (\')
    ‴  U+2034  TRIPLE PRIME (\')
    ⁗  U+2057  QUADRUPLE PRIME (\')
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
-- Instance arguments in records.
module Issue509 where

-- The instance version of _
⋯ : {A : Set} {{ x : A }} → A
⋯ {{ x }} = x

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

record T (n : ℕ) : Set where
  field
    nextPrime : ℕ

T₁ : T (suc zero)
T₁ = record { nextPrime = suc (suc zero) }

T₂ : T (suc (suc zero))
T₂ = record { nextPrime = suc (suc (suc zero)) }

data Param : ℕ → Set where
  param : ∀ n → Param (suc n)

record R : Set where
  constructor r
  field
    {impl} : ℕ
    {{ inst }} : T impl
    p : Param impl
    s : ℕ

-- The inst field should be an instance meta here
testA : R
testA = record { p = param zero; s = suc (suc zero) }

-- So, pretty much this:
testB : R
testB = record { impl = _; inst = ⋯; p = param zero; s = suc (suc zero) }

-- Or using the construcor
testC : R
testC = r { _ } {{ ⋯ }} (param zero) (suc (suc zero))

-- Omitting the fields also works when using the constructor (of course)
testD : R
testD = r (param zero) (suc (suc zero))

-- Note that {{ _ }} means explicitly giving the instance argument and saying
-- it should be an ordinary meta. Going the other way would be {⋯}.

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import lib.Basics
open import lib.NConnected

open import Graphs.Definition
open import Coequalizers.Definition

{- We will consider two properties of graphs: if they are trees and if they are connected,
   both are defined in terms of the geometric realisation (coequalizer). -}
module Graphs.Properties where

{- A graph is a tree if its coequalizer is contractible. -}
is-tree : {i j : ULevel} {E : Type i} {V : Type j} ( gph : Graph E V ) → Type (lmax i j)
is-tree gph = is-contr (Coeq gph)

{- A graph is connected if its coequalizer is connected. -}
gph-is-connected : {i j : ULevel} {E : Type i} {V : Type j} (gph : Graph E V) → Type (lmax i j)
gph-is-connected gph = is-connected 0 (Coeq gph)

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Integers, basic types and operations
------------------------------------------------------------------------

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

module Data.Integer.Base where

open import Data.Nat.Base as ℕ
  using (ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Sign as Sign using (Sign) renaming (_*_ to _S*_)
open import Function
open import Relation.Nullary using (¬_)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_)

infix  8 -_
infixl 7 _*_ _⊓_
infixl 6 _+_ _-_ _⊖_ _⊔_
infix  4 _≤_ _≥_ _<_ _>_ _≰_ _≱_ _≮_ _≯_

------------------------------------------------------------------------
-- The types

open import Agda.Builtin.Int public
  using ()
  renaming
  ( Int to ℤ
  ; pos    to +_      -- "+ n"      stands for "n"
  ; negsuc to -[1+_]  -- "-[1+ n ]" stands for "- (1 + n)"
  )

------------------------------------------------------------------------
-- Conversions

-- Absolute value.

∣_∣ : ℤ → ℕ
∣ + n      ∣ = n
∣ -[1+ n ] ∣ = ℕ.suc n

-- Gives the sign. For zero the sign is arbitrarily chosen to be +.

sign : ℤ → Sign
sign (+ _)    = Sign.+
sign -[1+ _ ] = Sign.-

------------------------------------------------------------------------
-- A view of integers as sign + absolute value

infix 5 _◂_ _◃_

_◃_ : Sign → ℕ → ℤ
_      ◃ ℕ.zero  = + ℕ.zero
Sign.+ ◃ n       = + n
Sign.- ◃ ℕ.suc n = -[1+ n ]

data SignAbs : ℤ → Set where
  _◂_ : (s : Sign) (n : ℕ) → SignAbs (s ◃ n)

signAbs : ∀ i → SignAbs i
signAbs (+ ℕ.zero)    = Sign.+ ◂ ℕ.zero
signAbs (+ (ℕ.suc n)) = Sign.+ ◂ ℕ.suc n
signAbs (-[1+ n ])    = Sign.- ◂ ℕ.suc n

------------------------------------------------------------------------
-- Arithmetic

-- Negation.

-_ : ℤ → ℤ
- (+ ℕ.suc n) = -[1+ n ]
- (+ ℕ.zero)  = + ℕ.zero
- -[1+ n ]    = + ℕ.suc n

-- Subtraction of natural numbers.

_⊖_ : ℕ → ℕ → ℤ
m       ⊖ ℕ.zero  = + m
ℕ.zero  ⊖ ℕ.suc n = -[1+ n ]
ℕ.suc m ⊖ ℕ.suc n = m ⊖ n

-- Addition.

_+_ : ℤ → ℤ → ℤ
-[1+ m ] + -[1+ n ] = -[1+ ℕ.suc (m ℕ+ n) ]
-[1+ m ] + +    n   = n ⊖ ℕ.suc m
+    m   + -[1+ n ] = m ⊖ ℕ.suc n
+    m   + +    n   = + (m ℕ+ n)

-- Subtraction.

_-_ : ℤ → ℤ → ℤ
i - j = i + (- j)

-- Successor.

suc : ℤ → ℤ
suc i = (+ 1) + i

-- Predecessor.

pred : ℤ → ℤ
pred i = (- + 1) + i

-- Multiplication.

_*_ : ℤ → ℤ → ℤ
i * j = sign i S* sign j ◃ ∣ i ∣ ℕ* ∣ j ∣

-- Maximum.

_⊔_ : ℤ → ℤ → ℤ
-[1+ m ] ⊔ -[1+ n ] = -[1+ ℕ._⊓_ m n ]
-[1+ m ] ⊔ +    n   = + n
+    m   ⊔ -[1+ n ] = + m
+    m   ⊔ +    n   = + (ℕ._⊔_ m n)

-- Minimum.

_⊓_ : ℤ → ℤ → ℤ
-[1+ m ] ⊓ -[1+ n ] = -[1+ ℕ._⊔_ m n ]
-[1+ m ] ⊓ +    n   = -[1+ m ]
+    m   ⊓ -[1+ n ] = -[1+ n ]
+    m   ⊓ +    n   = + (ℕ._⊓_ m n)

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

data _≤_ : ℤ → ℤ → Set where
  -≤+ : ∀ {m n} → -[1+ m ] ≤ + n
  -≤- : ∀ {m n} → (n≤m : n ℕ.≤ m) → -[1+ m ] ≤ -[1+ n ]
  +≤+ : ∀ {m n} → (m≤n : m ℕ.≤ n) → + m ≤ + n

_≥_ : Rel ℤ _
x ≥ y = y ≤ x

_<_ : Rel ℤ _
x < y = suc x ≤ y

_>_ : Rel ℤ _
x > y = y < x

_≰_ : Rel ℤ _
x ≰ y = ¬ (x ≤ y)

_≱_ : Rel ℤ _
x ≱ y = ¬ (x ≥ y)

_≮_ : Rel ℤ _
x ≮ y = ¬ (x < y)

_≯_ : Rel ℤ _
x ≯ y = ¬ (x > y)


text:
module DeBruijnExSubst where

open import Prelude -- using (_∘_)       -- composition, identity
open import Data.Maybe
open import Logic.Identity renaming (subst to subst≡)
import Logic.ChainReasoning
module Chain = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans)
open Chain

open import DeBruijn

-- untyped de Bruijn terms
data LamE (A : Set) : Set where
    varE  : A -> LamE A
    appE  : LamE A -> LamE A -> LamE A
    absE  : LamE (Maybe A) -> LamE A
    flatE : LamE (LamE A) -> LamE A

-- functoriality of LamE
lamE : {A B : Set} -> (A -> B) -> LamE A -> LamE B
lamE f (varE a)     = varE (f a)
lamE f (appE t1 t2) = appE (lamE f t1) (lamE f t2)
lamE f (absE r)     = absE (lamE (fmap f) r)
lamE f (flatE r)    = flatE (lamE (lamE f) r)

{- from TCS 05 paper
eval' : {A B : Set} -> (A -> B) -> LamE A -> Lam B
eval' f (varE a)     = var (f a)
eval' f (appE t1 t2) = app (eval' f t1) (eval' f t2)
eval' f (absE r)     = abs (eval' (fmap f) r)
eval' f (flatE r)    = subst id (eval' (eval' f) r)

eval : {A : Set} -> LamE A -> Lam A
eval = eval' id
-}

eval : {A : Set} -> LamE A -> Lam A
eval (varE a)     = var a
eval (appE t1 t2) = app (eval t1) (eval t2)
eval (absE r)     = abs (eval r)
eval (flatE r)    = subst eval (eval r)

evalNAT : {A B : Set}(f : A -> B) -> (t : LamE A) ->
  eval (lamE f t) ≡ lam f (eval t)
evalNAT f (varE a)     = refl
evalNAT f (appE t1 t2) =
  chain> eval (lamE f (appE t1 t2))
     === eval (appE (lamE f t1) (lamE f t2))
       by refl
     === app (eval (lamE f t1)) (eval (lamE f t2))
       by refl
     === app (lam f (eval t1))  (eval (lamE f t2))
       by cong (\ x -> app x (eval (lamE f t2))) (evalNAT f t1)
     === app (lam f (eval t1))  (lam f (eval t2))
       by cong (\ x -> app (lam f (eval t1)) x)  (evalNAT f t2)
     === lam f (app (eval t1) (eval t2))
       by refl
     === lam f (eval (appE t1 t2))
       by refl
evalNAT f (absE r) =
  chain> eval (lamE f (absE r))
     === eval (absE (lamE (fmap f) r))   by  refl
     === abs (eval (lamE (fmap f) r))    by  refl
     === abs (lam (fmap f) (eval r))     by  cong abs (evalNAT (fmap f) r)
     === lam f (abs (eval r))            by  refl
     === lam f (eval (absE r))           by  refl
evalNAT f (flatE r) =
  chain> eval (lamE f (flatE r))
     === eval (flatE (lamE (lamE f) r))
       by refl
     === subst eval (eval (lamE (lamE f) r))
       by refl
     === subst eval (lam (lamE f) (eval r))
       by cong (subst eval) (evalNAT (lamE f) r)
     === subst (eval ∘ lamE f) (eval r)
       by substLaw1 (lamE f) eval (eval r)
     === subst (lam f ∘ eval) (eval r)
       by substExt _ _ (evalNAT f) (eval r)
     === lam f (subst eval (eval r))
       by substLaw2 f eval (eval r)
     === lam f (eval (flatE r))
       by refl

evalNATcor : {A : Set}(ee : LamE (LamE A)) ->
  subst id (eval (lamE eval ee)) ≡ eval (flatE ee)
evalNATcor ee =
  chain> subst id (eval (lamE eval ee))
     === subst id (lam eval (eval ee))  by  cong (subst id) (evalNAT eval ee)
     === subst eval (eval ee)           by  substLaw1 eval id (eval ee)
     === eval (flatE ee)                by  refl


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

open import Sets.EquivalenceRelations
open import LogicalFormulae
open import Orders.Total.Definition
open import Orders.Partial.Definition
open import Setoids.Setoids
open import Functions.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Setoids.Orders.Partial.Definition where

record SetoidPartialOrder {a b c : _} {A : Set a} (S : Setoid {a} {b} A) (_<_ : Rel {a} {c} A) : Set (a ⊔ b ⊔ c) where
  open Setoid S
  field
    <WellDefined : {a b c d : A} → (a ∼ b) → (c ∼ d) → a < c → b < d
    irreflexive : {x : A} → (x < x) → False
    <Transitive : {a b c : A} → (a < b) → (b < c) → (a < c)
  _<=_ : Rel {a} {b ⊔ c} A
  a <= b = (a < b) || (a ∼ b)
  <=Transitive : {a b c : A} → (a <= b) → (b <= c) → (a <= c)
  <=Transitive (inl a<b) (inl b<c) = inl (<Transitive a<b b<c)
  <=Transitive (inl a<b) (inr b=c) = inl (<WellDefined (Equivalence.reflexive eq) b=c a<b)
  <=Transitive (inr a=b) (inl b<c) = inl (<WellDefined (Equivalence.symmetric eq a=b) (Equivalence.reflexive eq) b<c)
  <=Transitive (inr a=b) (inr b=c) = inr (Equivalence.transitive eq a=b b=c)

partialOrderToSetoidPartialOrder : {a b : _} {A : Set a} (P : PartialOrder {a} A {b}) → SetoidPartialOrder (reflSetoid A) (PartialOrder._<_ P)
SetoidPartialOrder.<WellDefined (partialOrderToSetoidPartialOrder P) a=b c=d a<c rewrite a=b | c=d = a<c
SetoidPartialOrder.irreflexive (partialOrderToSetoidPartialOrder P) = PartialOrder.irreflexive P
SetoidPartialOrder.<Transitive (partialOrderToSetoidPartialOrder P) = PartialOrder.<Transitive P


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

module Cubical.Data.Nat.Lower where

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport

open import Cubical.Data.Bool
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Unit

open import Cubical.Relation.Nullary

isMonotone : (ℕ → Bool) → Type
isMonotone f = ∀ n → f n ≥ f (suc n)

isPropIsMonotone : ∀ f → isProp (isMonotone f)
isPropIsMonotone f = isPropΠ λ n → isProp≥ (f n) (f (suc n))

isPropDepIsMonotone : isPropDep isMonotone
isPropDepIsMonotone = isOfHLevel→isOfHLevelDep 1 isPropIsMonotone {_}

Monotone : Type
Monotone = Σ _ isMonotone

isSetMonotone : isSet Monotone
isSetMonotone = isSetΣ (isSet→ isSetBool) (isProp→isSet ∘ isPropIsMonotone)

private
  variable
    ℓ : Level
    m n : Monotone

private
  mz : ℕ → Bool
  mz _ = false

  ms : (ℕ → Bool) → (ℕ → Bool)
  ms _ zero = true
  ms f (suc m) = f m

  msm : ∀{f} → isMonotone f → isMonotone (ms f)
  msm _ zero = _
  msm mf (suc m) = mf m

  mp : (ℕ → Bool) → (ℕ → Bool)
  mp f k = f (suc k)

  ms-mp : ∀ f → f 0 ≡ true → ms (mp f) ≡ f
  ms-mp f p i 0 = p (~ i)
  ms-mp f p i (suc k) = f (suc k)

  mz-lemma : ∀ f → isMonotone f → f 0 ≡ false → ∀ k → false ≡ f k
  mz-lemma f  _ p zero = sym p
  mz-lemma f mf p (suc k)
    with f 1
      | inspect f 1
      | subst (_≥ f 1) p (mf 0)
  ... | false | [ q ]ᵢ | _ = mz-lemma (mp f) (mf ∘ suc) q k

msuc : Monotone → Monotone
msuc m .fst = ms (fst m)
msuc m .snd = msm (snd m)

mpred : Monotone → Monotone
mpred f .fst k = f .fst (suc k)
mpred f .snd k = f .snd (suc k)

data MView : (ℕ → Bool) → Type where
  mzv : MView mz
  msv : ∀ n → MView (ms n)

mview : ∀ f → isMonotone f → MView f
mview f mf with f 0 | inspect f 0
... |  true | [ p ]ᵢ = subst MView (ms-mp f p) (msv (mp f))
... | false | [ p ]ᵢ = subst MView (funExt (mz-lemma f mf p)) mzv

∞ : Monotone
∞ .fst _ = true
∞ .snd _ = _

Detached : (ℕ → Bool) → Type
Detached p = Σ[ n ∈ ℕ ] Bool→Type (p n)

Lower : Monotone → Type
Lower m = Detached (fst m)

Detached-ext
  : ∀{p : ℕ → Bool} (k l : Detached p) → k .fst ≡ l .fst → k ≡ l
Detached-ext {p} (k , q) (l , r) s
  = ΣPathP (s , isPropDep∘ p isPropDep-Bool→Type q r s)

Lower∞≃ℕ : Lower ∞ ≃ ℕ
Lower∞≃ℕ = isoToEquiv λ where
    .fun → fst
    .inv n → n , _
    .rightInv _ → refl
    .leftInv _ → refl
  where open Iso

private
  apart : ℕ → ℕ → Type
  apart zero zero = ⊥
  apart (suc m) (suc n) = apart m n
  apart _ _ = Unit

  ≢→apart : (i j : ℕ) → ¬ i ≡ j → apart i j
  ≢→apart zero zero ¬p = ¬p refl
  ≢→apart (suc i) (suc j) ¬p = ≢→apart i j (¬p ∘ cong suc)
  ≢→apart zero (suc _) _ = _
  ≢→apart (suc _) zero _ = _

  apart→≢ : (i j : ℕ) → apart i j → ¬ i ≡ j
  apart→≢ (suc _) zero _ = snotz
  apart→≢ zero (suc _) _ = znots
  apart→≢ (suc i) (suc j) i#j = apart→≢ i j i#j ∘ cong predℕ

  isPropApart : ∀ i j → isProp (apart i j)
  isPropApart 0 0 = isProp⊥
  isPropApart (suc i) (suc j) = isPropApart i j
  isPropApart 0 (suc _) = isPropUnit
  isPropApart (suc _) 0 = isPropUnit

_#_ : ∀{P : ℕ → Type ℓ} → Σ ℕ P → Σ ℕ P → Type
u # v = apart (fst u) (fst v)

_#?_ : ∀{P : ℕ → Type ℓ} → (u v : Σ ℕ P) → (u # v) ⊎ (fst u ≡ fst v)
u #? v = decide (fst u) (fst v) where
  decide : (m n : ℕ) → apart m n ⊎ (m ≡ n)
  decide zero zero = inr refl
  decide zero (suc _) = inl _
  decide (suc _) zero = inl _
  decide (suc m) (suc n) = map (idfun _) (cong suc) (decide m n)

#→≢ : ∀{P : ℕ → Type ℓ} (u v : Σ ℕ P) → u # v → ¬ u ≡ v
#→≢ u v d = apart→≢ (fst u) (fst v) d ∘ cong fst

isProp# : ∀{P : ℕ → Type ℓ} (u v : Σ ℕ P) → isProp (u # v)
isProp# u v = isPropApart (fst u) (fst v)

isProp#Depᵣ : ∀{P : ℕ → Type ℓ} (v : Σ ℕ P) → isPropDep (λ u → u # v)
isProp#Depᵣ v = isOfHLevel→isOfHLevelDep 1 (λ u → isProp# u v) {_} {_}

≢→# : ∀{p} (u v : Detached p) → ¬ u ≡ v → u # v
≢→# u v ¬p = ≢→apart (fst u) (fst v) (¬p ∘ Detached-ext u v)

dzero : ∀{f} → Detached (ms f)
dzero = zero , _

dsuc : ∀{f} → Detached f → Detached (ms f)
dsuc (l , p) = suc l , p

module Untangle
    {α β}
    (f : Detached (ms α) → Detached (ms β))
    (g : Detached (ms β) → Detached (ms α))
    (rinv : section f g)
    (linv : retract f g)
  where

  default : ∀{γ} → (v d : Detached (ms γ)) → v # d → Detached γ
  default (suc l , p) _ _ = l , p
  default (0 , _) (suc l , p) _ = l , p

  #-f : ∀ u v → u # v → f u # f v
  #-f u v u#v with f u #? f v
  ... | inl fu#fv = fu#fv
  ... | inr fu≡fv = Empty.rec (#→≢ u v u#v u≡v)
    where
    u≡v : u ≡ v
    u≡v = sym (linv u)
       ∙∙ cong g (Detached-ext (f u) (f v) fu≡fv)
       ∙∙ linv v

  #-g : ∀ u v → u # v → g u # g v
  #-g u v u#v with g u #? g v
  ... | inl gu#gv = gu#gv
  ... | inr gu≡gv = Empty.rec (#→≢ u v u#v u≡v)
    where
    u≡v : u ≡ v
    u≡v = sym (rinv u)
       ∙∙ cong f (Detached-ext (g u) (g v) gu≡gv)
       ∙∙ rinv v

  f- : Detached α → Detached β
  f- v = default (f (dsuc v)) (f dzero) (#-f (dsuc v) dzero _)

  g- : Detached β → Detached α
  g- v = default (g (dsuc v)) (g dzero) (#-g (dsuc v) dzero _)

  g-f-z : ∀ v u → g dzero ≡ dsuc v → g (dsuc u) ≡ dzero → g- u ≡ v
  g-f-z v u r s with g (dsuc u) | g dzero | #-g (dsuc u) dzero _
  ... | zero , _ | suc k , q | #gf
    = Detached-ext (k , q) v (cong (predℕ ∘ fst) r)
  ... | w@(suc k , _) | _ | #gf = Empty.rec (snotz (cong fst s))

  g-f-s : ∀ v u → g (dsuc u) ≡ dsuc v → g- u ≡ v
  g-f-s v u r with g (dsuc u) | #-g (dsuc u) dzero _
  ... | suc k , q | #gf = Detached-ext (k , q) v (cong (predℕ ∘ fst) r)
  ... |  zero , _ | #gf = Empty.rec (znots (cong fst r))

  g-f- : ∀(v : Detached α) → g- (f- v) ≡ v
  g-f- v with f (dsuc v) | linv (dsuc v) | #-f (dsuc v) dzero _
  g-f- v | suc j , p | r | #f = g-f-s v (j , p) r
  ... | zero , _ | r | #f with f dzero | linv dzero
  ... | suc j , p | s = g-f-z v (j , p) r s

  f-g-z : ∀ v u → f dzero ≡ dsuc v → f (dsuc u) ≡ dzero → f- u ≡ v
  f-g-z v u r s with f (dsuc u) | f dzero | #-f (dsuc u) dzero _
  ... | zero , _ | suc k , q | #fg
    = Detached-ext (k , q) v (cong (predℕ ∘ fst) r)
  ... | (suc _ , _) | _ | _ = Empty.rec (snotz (cong fst s))

  f-g-s : ∀ v u → f (dsuc u) ≡ dsuc v → f- u ≡ v
  f-g-s v u r with f (dsuc u) | #-f (dsuc u) dzero _
  ... | suc k , q | _ = Detached-ext (k , q) v (cong (predℕ ∘ fst) r)
  ... |  zero , _ | _ = Empty.rec (znots (cong fst r))

  f-g- : ∀ v → f- (g- v) ≡ v
  f-g- v with g (dsuc v) | rinv (dsuc v) | #-g (dsuc v) dzero _
  ... | suc j , q | r | _ = f-g-s v (j , q) r
  ... | zero , _ | r | _ with g dzero | rinv dzero
  ... | suc k , q | s = f-g-z v (k , q) r s

  open Iso
  iso- : Iso (Detached α) (Detached β)
  iso- .fun = f-
  iso- .inv = g-
  iso- .rightInv = f-g-
  iso- .leftInv = g-f-

iso-pred
  : ∀{α β}
  → Iso (Detached (ms α)) (Detached (ms β))
  → Iso (Detached α) (Detached β)
iso-pred i = Untangle.iso- fun inv rightInv leftInv
  where open Iso i

isInjectiveLower : Lower m ≡ Lower n → m ≡ n
isInjectiveLower {m} {n} P =
  curry ΣPathP
    (lemma (m .fst) (n .fst) (m .snd) (n .snd) (pathToIso P))
    (isPropDepIsMonotone (m .snd) (n .snd) _)
  where
  lemma
    : ∀ α β → isMonotone α → isMonotone β
    → Iso (Detached α) (Detached β)
    → α ≡ β
  lemma α β mα mβ I i k with mview α mα | mview β mβ
  ... | mzv | mzv = mz k
  lemma α β mα mβ I i 0 | msv _ | msv _
    = true
  lemma α β mα mβ I i (suc k) | msv α' | msv β'
    = lemma α' β' (mα ∘ suc) (mβ ∘ suc) (iso-pred I) i k
  lemma α β mα mβ I i k | mzv | msv β'
    = Empty.rec {A = α k ≡ β k} (Iso.inv I dzero .snd) i
  lemma α β mα mβ I i k | msv _ | mzv
    = Empty.rec {A = α k ≡ β k} (Iso.fun I dzero .snd) i


text:
------------------------------------------------------------------------
-- An observation about weak bisimilarity
------------------------------------------------------------------------

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

module Delay-monad.Bisimilarity.Observation where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Function-universe equality-with-J as F hiding (_∘_)
open import H-level.Closure equality-with-J

------------------------------------------------------------------------
-- The D type

mutual

  -- A mixed inductive-coinductive type.

  data D (i : Size) : Type where
    -- Output a boolean and continue. Note that this constructor is
    -- inductive.
    put : Bool → D i → D i

    -- Wait. The intention is that finite delay should not be
    -- "observable" (as captured by weak bisimilarity).
    later : D′ i → D i

  record D′ (i : Size) : Type where
    coinductive
    field
      force : {j : Size< i} → D j

open D′ public

private
  variable
    b b′  : Bool
    n     : ℕ
    i     : Size
    x y z : D ∞
    x′ y′ : D′ ∞

-- Making put inductive is a bit strange, because one can construct a
-- coinductive variant of it by using later.

put′ : Bool → D′ i → D i
put′ b x = later λ { .force → put b (x .force) }

------------------------------------------------------------------------
-- Weak bisimilarity

-- The output relation: x [ n ]≡ b means that x can output at least n
-- times, and the n-th output is b.

data _[_]≡_ : D ∞ → ℕ → Bool → Type where
  put-zero : put b x [ zero ]≡ b
  put-suc  : x [ n ]≡ b → put b′ x [ suc n ]≡ b
  later    : x′ .force [ n ]≡ b → later x′ [ n ]≡ b

-- The output relation is propositional.

[]≡-propositional : Is-proposition (x [ n ]≡ b)
[]≡-propositional {b = true}  put-zero put-zero = refl
[]≡-propositional {b = false} put-zero put-zero = refl
[]≡-propositional (put-suc p) (put-suc q) =
  cong put-suc ([]≡-propositional p q)
[]≡-propositional (later p) (later q) =
  cong later ([]≡-propositional p q)

-- Weak bisimilarity. Two computations are weakly bisimilar if the
-- output relation cannot distinguish between them.

_≈_ : D ∞ → D ∞ → Type
x ≈ y = ∀ {n b} → x [ n ]≡ b ⇔ y [ n ]≡ b

-- Weak bisimilarity is propositional (assuming extensionality).

≈-propositional :
  Extensionality lzero lzero →
  Is-proposition (x ≈ y)
≈-propositional ext =
  implicit-Π-closure ext 1 λ _ →
  implicit-Π-closure ext 1 λ _ →
  ⇔-closure ext 1 []≡-propositional []≡-propositional

-- The put constructor and the function put′ are closely related.

put≈put′ : put b (x′ .force) ≈ put′ b x′
put≈put′ ._⇔_.to   q         = later q
put≈put′ ._⇔_.from (later q) = q

-- Weak bisimilarity is an equivalence relation.

reflexive-≈ : x ≈ x
reflexive-≈ = F.id

symmetric-≈ : x ≈ y → y ≈ x
symmetric-≈ x≈y = F.inverse x≈y

transitive-≈ : x ≈ y → y ≈ z → x ≈ z
transitive-≈ x≈y y≈z = y≈z F.∘ x≈y

-- The later constructor can be removed to the left and to the right.

laterˡ⁻¹ : later x′ ≈ y → x′ .force ≈ y
laterˡ⁻¹ p ._⇔_.to   q = _⇔_.to p (later q)
laterˡ⁻¹ p ._⇔_.from q with _⇔_.from p q
…                      | later q′ = q′

laterʳ⁻¹ : x ≈ later y′ → x ≈ y′ .force
laterʳ⁻¹ = symmetric-≈ ∘ laterˡ⁻¹ ∘ symmetric-≈

later⁻¹ : later x′ ≈ later y′ → x′ .force ≈ y′ .force
later⁻¹ = laterˡ⁻¹ ∘ laterʳ⁻¹

-- The put constructor can be removed if it is removed on both sides
-- at the same time.

put⁻¹ : put b x ≈ put b′ y → x ≈ y
put⁻¹ p ._⇔_.to   q with _⇔_.to p (put-suc q)
…                   | put-suc q′ = q′
put⁻¹ p ._⇔_.from q with _⇔_.from p (put-suc q)
…                   | put-suc q′ = q′

------------------------------------------------------------------------
-- Not weak bisimilarity

module Not-weak-bisimilarity where

  mutual

    infix 4 [_]_≈_ [_]_≈′_

    -- After having seen the definition of weak bisimilarity in
    -- Delay-monad.Bisimilarity one might believe that weak
    -- bisimilarity for D can be defined in the following way:

    data [_]_≈_ (i : Size) : D ∞ → D ∞ → Type where
      put    : [ i ] x ≈ y → [ i ] put b x ≈ put b y
      later  : [ i ] x′ .force ≈′ y′ .force → [ i ] later x′ ≈ later y′
      laterˡ : [ i ] x′ .force ≈ y → [ i ] later x′ ≈ y
      laterʳ : [ i ] x ≈ y′ .force → [ i ] x ≈ later y′

    record [_]_≈′_ (i : Size) (x y : D ∞) : Type where
      coinductive
      field
        force : {j : Size< i} → [ j ] x ≈ y

  open [_]_≈′_ public

  -- The relation [ i ]_≈_ is reflexive and symmetric.

  reflexive-[]≈ : [ i ] x ≈ x
  reflexive-[]≈ {x = put _ _} = put reflexive-[]≈
  reflexive-[]≈ {x = later _} = later λ { .force → reflexive-[]≈ }

  symmetric-[]≈ : [ i ] x ≈ y → [ i ] y ≈ x
  symmetric-[]≈ (put p)    = put (symmetric-[]≈ p)
  symmetric-[]≈ (later p)  = later λ { .force →
                               symmetric-[]≈ (p .force) }
  symmetric-[]≈ (laterˡ p) = laterʳ (symmetric-[]≈ p)
  symmetric-[]≈ (laterʳ p) = laterˡ (symmetric-[]≈ p)

  -- However, the relation [ ∞ ]_≈_ is not transitive.

  ¬-transitive-≈ :
    ¬ (∀ {x y z} → [ ∞ ] x ≈ y → [ ∞ ] y ≈ z → [ ∞ ] x ≈ z)
  ¬-transitive-≈ trans = x≉z x≈z
    where
    x̲ : D i
    x̲ = later λ { .force → put true (put true x̲) }

    y̲ : D i
    y̲ = later λ { .force → put true y̲ }

    z̲ : D i
    z̲ = put true (later λ { .force → put true z̲ })

    x≈y : [ i ] x̲ ≈ y̲
    x≈y = later λ { .force → put (laterʳ (put x≈y)) }

    y≈z : [ i ] y̲ ≈ z̲
    y≈z = laterˡ (put (later λ { .force → put y≈z }))

    x≉z : ¬ [ ∞ ] x̲ ≈ z̲
    x≉z (laterˡ (put (laterʳ (put p)))) = x≉z p

    x≈z : [ ∞ ] x̲ ≈ z̲
    x≈z = trans x≈y y≈z

  -- Thus the two relations _≈_ and [ ∞ ]_≈_ are not pointwise
  -- logically equivalent.

  ¬≈⇔[]≈ : ¬ (∀ {x y} → x ≈ y ⇔ [ ∞ ] x ≈ y)
  ¬≈⇔[]≈ =
    (∀ {x y} → x ≈ y ⇔ [ ∞ ] x ≈ y)                        ↝⟨ (λ hyp x≈y y≈z → _⇔_.to hyp (transitive-≈ (_⇔_.from hyp x≈y) (_⇔_.from hyp y≈z))) ⟩
    (∀ {x y z} → [ ∞ ] x ≈ y → [ ∞ ] y ≈ z → [ ∞ ] x ≈ z)  ↝⟨ ¬-transitive-≈ ⟩□
    ⊥                                                      □

  -- The relation [ ∞ ]_≈_ is contained in _≈_.

  []≈→≈ : [ ∞ ] x ≈ y → x ≈ y
  []≈→≈ = λ p → record { to = ≈→→ p; from = ≈→→ (symmetric-[]≈ p) }
    where
    ≈→→ : [ ∞ ] x ≈ y → x [ n ]≡ b → y [ n ]≡ b
    ≈→→ (put p)    put-zero    = put-zero
    ≈→→ (put p)    (put-suc q) = put-suc (≈→→ p q)
    ≈→→ (later p)  (later q)   = later (≈→→ (p .force) q)
    ≈→→ (laterˡ p) (later q)   = ≈→→ p q
    ≈→→ (laterʳ p) q           = later (≈→→ p q)

  -- The relation _≈_ is not contained in [ ∞ ]_≈_.

  ¬≈→[]≈ : ¬ (∀ {x y} → x ≈ y → [ ∞ ] x ≈ y)
  ¬≈→[]≈ =
    (∀ {x y} → x ≈ y → [ ∞ ] x ≈ y)  ↝⟨ (λ hyp → record { to = hyp; from = []≈→≈ }) ⟩
    (∀ {x y} → x ≈ y ⇔ [ ∞ ] x ≈ y)  ↝⟨ ¬≈⇔[]≈ ⟩□
    ⊥                                □

------------------------------------------------------------------------
-- An alternative definition of weak bisimilarity

mutual

  infix 4 [_]_≈_ [_]_≈′_

  -- The problem with Not-weak-bisimilarity.[_]_≈_ is that its put
  -- constructor is inductive. The put constructor of D is inductive,
  -- but as noted above (put′, put≈put′) this is a bit strange, and it
  -- might make more sense to make put coinductive.
  --
  -- The following definition of weak bisimilarity uses a coinductive
  -- put constructor.

  data [_]_≈_ (i : Size) : D ∞ → D ∞ → Type where
    put    : [ i ] x ≈′ y → [ i ] put b x ≈ put b y
    later  : [ i ] x′ .force ≈′ y′ .force → [ i ] later x′ ≈ later y′
    laterˡ : [ i ] x′ .force ≈ y → [ i ] later x′ ≈ y
    laterʳ : [ i ] x ≈ y′ .force → [ i ] x ≈ later y′

  record [_]_≈′_ (i : Size) (x y : D ∞) : Type where
    coinductive
    field
      force : {j : Size< i} → [ j ] x ≈ y

open [_]_≈′_ public

-- The relation [ ∞ ]_≈_ is not propositional.

¬-≈[]-propositional : ¬ (∀ {x y} → Is-proposition ([ ∞ ] x ≈ y))
¬-≈[]-propositional =
  (∀ {x y} → Is-proposition ([ ∞ ] x ≈ y))  ↝⟨ (λ prop → prop _ _) ⟩
  proof₁ ≡ proof₂                           ↝⟨ (λ ()) ⟩□
  ⊥                                         □
  where
  never : D i
  never = later λ { .force → never }

  proof₁ : ∀ {i} → [ i ] never ≈ never
  proof₁ = later λ { .force → proof₁ }

  proof₂ : ∀ {i} → [ i ] never ≈ never
  proof₂ = laterˡ proof₁

-- The relation [ i ]_≈_ is reflexive and symmetric.

reflexive-[]≈ : [ i ] x ≈ x
reflexive-[]≈ {x = put _ _} = put   λ { .force → reflexive-[]≈ }
reflexive-[]≈ {x = later _} = later λ { .force → reflexive-[]≈ }

symmetric-[]≈ : [ i ] x ≈ y → [ i ] y ≈ x
symmetric-[]≈ (put p)    = put   λ { .force → symmetric-[]≈ (p .force) }
symmetric-[]≈ (later p)  = later λ { .force → symmetric-[]≈ (p .force) }
symmetric-[]≈ (laterˡ p) = laterʳ (symmetric-[]≈ p)
symmetric-[]≈ (laterʳ p) = laterˡ (symmetric-[]≈ p)

-- The two relations _≈_ and [ ∞ ]_≈_ are pointwise logically
-- equivalent.

≈⇔[]≈ : x ≈ y ⇔ [ ∞ ] x ≈ y
≈⇔[]≈ = record
  { to   = to _ _
  ; from = λ p → record { to = from p; from = from (symmetric-[]≈ p) }
  }
  where
  from : [ ∞ ] x ≈ y → x [ n ]≡ b → y [ n ]≡ b
  from (put p)    put-zero    = put-zero
  from (put p)    (put-suc q) = put-suc (from (p .force) q)
  from (later p)  (later q)   = later (from (p .force) q)
  from (laterˡ p) (later q)   = from p q
  from (laterʳ p) q           = later (from p q)

  mutual

    to : ∀ x y → x ≈ y → [ i ] x ≈ y
    to (put b x) y         p = symmetric-[]≈ (to′ (symmetric-≈ p)
                                                  (_⇔_.to p put-zero))
    to x         (put b y) p = to′ p (_⇔_.from p put-zero)
    to (later x) (later y) p = later λ { .force → to _ _ (later⁻¹ p) }

    to′ : x ≈ put b y → x [ zero ]≡ b → [ i ] x ≈ put b y
    to′ p put-zero  = put λ { .force → to _ _ (put⁻¹ p) }
    to′ p (later q) = laterˡ (to′ (laterˡ⁻¹ p) q)

-- The relation [ ∞ ]_≈_ is transitive.

transitive-[]≈ : [ ∞ ] x ≈ y → [ ∞ ] y ≈ z → [ ∞ ] x ≈ z
transitive-[]≈ p q =
  _⇔_.to ≈⇔[]≈ (transitive-≈ (_⇔_.from ≈⇔[]≈ p) (_⇔_.from ≈⇔[]≈ q))

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
open import FRP.JS.String using ( String )
open import FRP.JS.Time using ( Time )

module FRP.JS.Date where

postulate
  Date : Set
  fromTime : Time → Date
  toTime : Date → Time
  toString : Date → String
  toUTCString : Date → String

{-# COMPILED_JS fromTime require("agda-frp-time").date #-}
{-# COMPILED_JS toTime function(d) { return d.getTime(); } #-}
{-# COMPILED_JS toString function(d) { return d.toString(); } #-}
{-# COMPILED_JS toUTCString function(d) { return d.toUTCString(); } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym)

module AKS.Nat.Combinatorial where

open import AKS.Nat.Base using (ℕ; _+_; _∸_; _*_; _≤_)
open ℕ
open import AKS.Nat.Properties using (*-identityʳ)
open import AKS.Nat.Properties using (0≤n; ≤-refl; m≤m+n; *-mono-≤; module ≤-Reasoning)
open import AKS.Nat.Properties using (<-irrefl; *-mono-<)
open import AKS.Nat.Divisibility using (_/_)
open ≤-Reasoning

_C_ : ℕ → ℕ → ℕ
n C zero = 1
zero C suc k = 0
suc n C suc k = n C k + n C (suc k)

_! : ℕ → ℕ
zero ! = 1
suc n ! = suc n * n !

1≤n! : ∀ n → 1 ≤ n !
1≤n! zero = ≤-refl
1≤n! (suc n) = begin
  1 ≤⟨ 1≤n! n ⟩
  n ! ≤⟨ m≤m+n ⟩
  n ! + n * n ! ≡⟨ refl ⟩
  (1 + n) ! ∎

n≤n! : ∀ n → n ≤ n !
n≤n! zero = 0≤n
n≤n! (suc n) = begin
  suc n ≡⟨ sym (*-identityʳ (suc n)) ⟩
  suc n * 1 ≤⟨ *-mono-≤ (≤-refl {suc n}) (1≤n! n) ⟩
  (1 + n) ! ∎

_C′_ : ℕ → ℕ → ℕ
n C′ k = (n ! / (k ! * (n ∸ k) !)) {≢⇒¬≟ den≢0}
  where
  den≢0 : k ! * (n ∸ k) ! ≢ 0
  den≢0 den≡0 = <-irrefl (sym den≡0) (*-mono-< (1≤n! k) (1≤n! (n ∸ k)))

nC′0≡1 : ∀ {n} → n C′ 0 ≡ 1
nC′0≡1 {n} = lemma num≡dem
  where
  num≡dem : n ! ≡ (0 ! * (n ∸ 0) !)
  num≡dem = sym (+-identityʳ (n !))
  lemma : ∀ {num dem} .{dem≢0} → num ≡ dem → (num / dem) {dem≢0} ≡ 1
  lemma {num} {_} {dem≢0} refl = n/n≡1 num {dem≢0}

-- 0C′n≡0 : ∀ {k} → 0 C′ k ≡ 0
-- 0C′n≡0 {k} = {!0/n≡0 (k ! * (0 ∸ k) !) {?}!}

-- lem : ∀ {n k} → n C k ≡ n C′ k
-- lem {n} {zero} = sym (nC′0≡1 {n})
-- lem {zero} {suc k} = {!refl!}
-- lem {suc n} {suc k} with lem {n} {k} | lem {n} {suc k}
-- ... | p₁ | p₂ = {!!}

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


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

module Lecture6 where

import Lecture5
open Lecture5 public

-- Section 6.1 Contractible types

is-contr : {i : Level} → UU i → UU i
is-contr A = Sigma A (λ a → (x : A) → Id a x)

center : {i : Level} {A : UU i} → is-contr A → A
center (dpair c C) = c

-- We make sure that the contraction is coherent in a straightforward way
contraction : {i : Level} {A : UU i} (H : is-contr A) →
  (const A A (center H) ~ id)
contraction (dpair c C) x = concat _ (inv (C c)) (C x)

coh-contraction : {i : Level} {A : UU i} (H : is-contr A) →
  Id (contraction H (center H)) refl
coh-contraction (dpair c C) = left-inv (C c)

ev-pt : {i j : Level} (A : UU i) (a : A) (B : A → UU j) → ((x : A) → B x) → B a
ev-pt A a B f = f a

sing-ind-is-contr : {i j : Level} (A : UU i) (H : is-contr A) (B : A → UU j) →
  B (center H) → (x : A) → B x
sing-ind-is-contr A H B b x = tr B (contraction H x) b

sing-comp-is-contr : {i j : Level} (A : UU i) (H : is-contr A) (B : A → UU j) →
  (((ev-pt A (center H) B) ∘ (sing-ind-is-contr A H B)) ~ id)
sing-comp-is-contr A H B b =
  ap (λ (ω : Id (center H) (center H)) → tr B ω b) (coh-contraction H)

is-sing-is-contr : {i j : Level} (A : UU i) (H : is-contr A) (B : A → UU j) →
  sec (ev-pt A (center H) B)
is-sing-is-contr A H B =
  dpair (sing-ind-is-contr A H B) (sing-comp-is-contr A H B)

is-sing : {i : Level} (A : UU i) → A → UU (lsuc i)
is-sing {i} A a = (B : A → UU i) → sec (ev-pt A a B)

is-contr-is-sing : {i : Level} (A : UU i) (a : A) →
  is-sing A a → is-contr A
is-contr-is-sing A a S = dpair a (pr1 (S (λ y → Id a y)) refl)

is-sing-unit : is-sing unit star
is-sing-unit B = dpair ind-unit (λ b → refl)

is-contr-unit : is-contr unit
is-contr-unit = is-contr-is-sing unit star (is-sing-unit)

is-sing-total-path : {i : Level} (A : UU i) (a : A) →
  is-sing (Σ A (λ x → Id a x)) (dpair a refl)
is-sing-total-path A a B = dpair (ind-Σ ∘ (ind-Id _)) (λ b → refl)

is-contr-total-path : {i : Level} (A : UU i) (a : A) →
  is-contr (Σ A (λ x → Id a x))
is-contr-total-path A a = is-contr-is-sing _ _ (is-sing-total-path A a)

-- Section 6.2 Contractible maps

fib : {i j : Level} {A : UU i} {B : UU j} (f : A → B) (b : B) → UU (i ⊔ j)
fib f b = Σ _ (λ x → Id (f x) b)

is-contr-map : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
is-contr-map f = (y : _) → is-contr (fib f y)

-- Our goal is to show that contractible maps are equivalences.
-- First we construct the inverse of a contractible map.
inv-is-contr-map : {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  is-contr-map f → B → A
inv-is-contr-map H y = pr1 (center (H y))

-- Then we show that the inverse is a section.
issec-is-contr-map : {i j : Level} {A : UU i} {B : UU j} {f : A → B}
  (H : is-contr-map f) → (f ∘ (inv-is-contr-map H)) ~ id
issec-is-contr-map H y = pr2 (center (H y))

-- Then we show that the inverse is also a retraction.
isretr-is-contr-map : {i j : Level} {A : UU i} {B : UU j} {f : A → B}
  (H : is-contr-map f) → ((inv-is-contr-map H) ∘ f) ~ id
isretr-is-contr-map {_} {_} {A} {B} {f} H x =
  ap {_} {_} {fib f (f x)} {A} pr1
    {dpair (inv-is-contr-map H (f x)) (issec-is-contr-map H (f x))}
    {dpair x refl}
    ( concat (center (H (f x)))
             (inv (contraction (H (f x))
               (dpair (inv-is-contr-map H (f x)) (issec-is-contr-map H (f x)))))
             (contraction (H (f x)) (dpair x refl)))

-- Finally we put it all together to show that contractible maps are equivalences.
is-equiv-is-contr-map : {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  is-contr-map f → is-equiv f
is-equiv-is-contr-map H =
  pair
    (dpair (inv-is-contr-map H) (issec-is-contr-map H))
    (dpair (inv-is-contr-map H) (isretr-is-contr-map H))

-- Section 6.3 Equivalences are contractible maps

htpy-nat : {i j : Level} {A : UU i} {B : UU j} {f g : A → B} (H : f ~ g)
  {x y : A} (p : Id x y) →
  Id (concat _ (H x) (ap g p)) (concat _ (ap f p) (H y))
htpy-nat H refl = right-unit (H _)

-- Should left-unwhisk and right-unwhisk be moved to Lecture 4? That's where they most naturally fit.
left-unwhisk : {i : Level} {A : UU i} {x y z : A} (p : Id x y) {q r : Id y z} →
  Id (concat _ p q) (concat _ p r) → Id q r
left-unwhisk refl s = concat _ (inv (left-unit _)) (concat _ s (left-unit _))

right-unwhisk : {i : Level} {A : UU i} {x y z : A} {p q : Id x y}
  (r : Id y z) → Id (concat _ p r) (concat _ q r) → Id p q
right-unwhisk refl s = concat _ (inv (right-unit _)) (concat _ s (right-unit _))

htpy-red : {i : Level} {A : UU i} {f : A → A} (H : f ~ id) →
  (x : A) → Id (H (f x)) (ap f (H x))
htpy-red {_} {A} {f} H x = right-unwhisk (H x)
  (concat (concat (f x) (H (f x)) (ap id (H x)))
    (ap (concat (f x) (H (f x))) (inv (ap-id (H x)))) (htpy-nat H (H x)))

center-is-invertible : {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  is-invertible f → (y : B) → fib f y
center-is-invertible {i} {j} {A} {B} {f}
  (dpair g (dpair issec isretr)) y =
    (dpair (g y)
      (concat _
        (inv (ap (f ∘ g) (issec y)))
        (concat _ (ap f (isretr (g y))) (issec y))))

mv-left : {i : Level} {A : UU i} {x y z : A}
  (p : Id x y) {q : Id y z} {r : Id x z} →
  Id (concat _ p q) r → Id q (concat _ (inv p) r)
mv-left refl s = s

square : {i : Level} {A : UU i} {x y1 y2 z : A}
  (p1 : Id x y1) (q1 : Id y1 z) (p2 : Id x y2) (q2 : Id y2 z) → UU i
square p q p' q' = Id (concat _ p q) (concat _ p' q')

sq-left-whisk : {i : Level} {A : UU i} {x y1 y2 z : A} {p1 p1' : Id x y1}
  (s : Id p1 p1') {q1 : Id y1 z} {p2 : Id x y2} {q2 : Id y2 z} →
  square p1 q1 p2 q2 → square p1' q1 p2 q2
sq-left-whisk refl sq = sq

sq-top-whisk : {i : Level} {A : UU i} {x y1 y2 z : A}
  {p1 : Id x y1} {q1 : Id y1 z}
  {p2 p2' : Id x y2} (s : Id p2 p2') {q2 : Id y2 z} →
  square p1 q1 p2 q2 → square p1 q1 p2' q2
sq-top-whisk refl sq = sq

contraction-is-invertible : {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  (I : is-invertible f) → (y : B) → (t : fib f y) →
  Id (center-is-invertible I y) t
contraction-is-invertible {i} {j} {A} {B} {f}
  (dpair g (dpair issec isretr)) y (dpair x refl) =
  eq-pair (dpair
    (isretr x)
    (concat _
      (tr-fib (isretr x) (f x)
        (pr2 (center-is-invertible
          (dpair g (dpair issec isretr))
          (f x))))
      (inv (mv-left (ap f (isretr x))
        (concat _ (right-unit (ap f (isretr x)))
        (mv-left (ap (f ∘ g) (issec y))
        (sq-left-whisk {_} {_} {f(g(f(g(f x))))} {f(g(f x))} {f(g(f x))} {f x}
          {issec (f(g(f x)))} {ap (f ∘ g) (issec (f x))}
          (htpy-red issec (f x)) {ap f (isretr x)} {ap f (isretr (g (f x)))}
          {issec (f x)}
          (sq-top-whisk {_} {_} {f(g(f(g(f x))))} {f(g(f x))} {f(g(f x))} {f x}
            {issec (f(g(f x)))} {_} {_} {_}
            (concat _ (ap-comp f (g ∘ f) (isretr x))
            (inv (ap (ap f) (htpy-red isretr x))))
            (htpy-nat (htpy-right-whisk issec f) (isretr x))))))))))

is-contr-map-is-invertible : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-invertible f → is-contr-map f
is-contr-map-is-invertible {i} {j} {A} {B} {f} I y =
    dpair (center-is-invertible I y) (contraction-is-invertible I y)

is-contr-map-is-equiv : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-equiv f → is-contr-map f
is-contr-map-is-equiv = is-contr-map-is-invertible ∘ is-invertible-is-equiv

is-contr-total-path' : {i : Level} (A : UU i) (a : A) →
  is-contr (Σ A (λ x → Id x a))
is-contr-total-path' A a = is-contr-map-is-equiv (is-equiv-id _) a

-- Exercises

-- Exercise 6.1
is-prop-is-contr : {i : Level} {A : UU i} → is-contr A → (x y : A) → is-contr (Id x y)
is-prop-is-contr {i} {A} C =
  sing-ind-is-contr A C
    (λ x → ((y : A) → is-contr (Id x y)))
    (λ y → dpair
           (contraction C y)
           (ind-Id
             (λ z (p : Id (center C) z) → Id (contraction C z) p)
             (coh-contraction C)
             y))

-- Exercise 6.2
is-contr-retract-of : {i j : Level} {A : UU i} (B : UU j) → A retract-of B → is-contr B → is-contr A
is-contr-retract-of B (dpair i (dpair r isretr)) C =
  dpair
    (r (center C))
    (λ x → concat (r (i x)) (ap r (contraction C (i x))) (isretr x))

-- Exercise 6.3

is-equiv-const-is-contr : {i : Level} {A : UU i} → is-contr A → is-equiv (const A unit star)
is-equiv-const-is-contr {i} {A} H = pair (dpair (ind-unit (center H)) (ind-unit refl)) (dpair (const unit A (center H)) (contraction H))

is-contr-is-equiv-const : {i : Level} {A : UU i} → is-equiv (const A unit star) → is-contr A
is-contr-is-equiv-const (dpair (dpair g issec) (dpair h isretr)) = dpair (h star) isretr

is-contr-is-equiv : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → is-equiv f → is-contr B → is-contr A
is-contr-is-equiv f Ef C =
  is-contr-is-equiv-const
    (is-equiv-comp (λ x → refl) Ef (is-equiv-const-is-contr C))

is-contr-is-equiv' : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → is-equiv f → is-contr A → is-contr B
is-contr-is-equiv' f Ef C = is-contr-is-equiv (inv-is-equiv Ef) (is-equiv-inv-is-equiv Ef) C

is-equiv-is-contr : {i j : Level} {A : UU i} {B : UU j} (f : A → B) →
  is-contr A → is-contr B → is-equiv f
is-equiv-is-contr {i} {j} {A} {B} f CA CB =
  pair
    (dpair
      (const B A (center CA))
      (sing-ind-is-contr B CB _ (inv (contraction CB (f (center CA))))))
    (dpair (const B A (center CA)) (contraction CA))


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

open import Algebra.Construct.DirectProduct

module Construct.DirectProduct where

open import Algebra
import Algebra.Construct.DirectProduct as DirectProduct
open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Level using (Level; _⊔_)

private
  variable
    a b ℓ₁ ℓ₂ : Level

------------------------------------------------------------------------
-- Raw bundles

rawQuasigroup : RawQuasigroup a ℓ₁ → RawQuasigroup b ℓ₂ → RawQuasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawQuasigroup M N = record
  { Carrier = M.Carrier × N.Carrier
  ; _≈_     = Pointwise M._≈_ N._≈_
  ; _∙_     = zip M._∙_ N._∙_
  ; _\\_    = zip M._\\_ N._\\_
  ; _//_    = zip M._//_ N._//_
  } where module M = RawQuasigroup M; module N = RawQuasigroup N

rawLoop : RawLoop a ℓ₁ → RawLoop b ℓ₂ → RawLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawLoop M N = record
  { Carrier = M.Carrier × N.Carrier
  ; _≈_     = Pointwise M._≈_ N._≈_
  ; _∙_     = zip M._∙_ N._∙_
  ; _\\_    = zip M._\\_ N._\\_
  ; _//_    = zip M._//_ N._//_
  ; ε       = M.ε , N.ε
  } where module M = RawLoop M; module N = RawLoop N

------------------------------------------------------------------------
-- Bundles

unitalMagma : UnitalMagma a ℓ₁ → UnitalMagma b ℓ₂ → UnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
unitalMagma M N = record
  { ε = M.ε , N.ε
  ; isUnitalMagma = record
    { isMagma = Magma.isMagma (magma M.magma N.magma)
    ; identity = (M.identityˡ , N.identityˡ <*>_)
               , (M.identityʳ , N.identityʳ <*>_)
    }
  } where module M = UnitalMagma M; module N = UnitalMagma N

invertibleMagma : InvertibleMagma a ℓ₁ → InvertibleMagma b ℓ₂ → InvertibleMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
invertibleMagma M N = record
  { _⁻¹ = map M._⁻¹ N._⁻¹
  ; isInvertibleMagma = record
    { isMagma = Magma.isMagma (magma M.magma N.magma)
    ; inverse = (λ x → (M.inverseˡ , N.inverseˡ) <*> x)
                , (λ x → (M.inverseʳ , N.inverseʳ) <*> x)
    }
  } where module M = InvertibleMagma M; module N = InvertibleMagma N

invertibleUnitalMagma : InvertibleUnitalMagma a ℓ₁ → InvertibleUnitalMagma b ℓ₂ → InvertibleUnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
invertibleUnitalMagma M N = record
  { ε = M.ε , N.ε
  ; isInvertibleUnitalMagma = record
    { isInvertibleMagma = InvertibleMagma.isInvertibleMagma (invertibleMagma M.invertibleMagma N.invertibleMagma)
    ; identity = (M.identityˡ , N.identityˡ <*>_)
               , (M.identityʳ , N.identityʳ <*>_)
    }
  } where module M = InvertibleUnitalMagma M; module N = InvertibleUnitalMagma N


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

open import Base

module Homotopy.PullbackDef where

record pullback-diag (i : Level) : Set (suc i) where
  constructor diag_,_,_,_,_
  field
    A : Set i
    B : Set i
    C : Set i
    f : A → C
    g : B → C

pullback-diag-raw-eq : ∀ {i} {A A' : Set i} (p : A ≡ A')
  {B B' : Set i} (q : B ≡ B') {C C' : Set i} (r : C ≡ C')
  {f : A → C} {f' : A' → C'} (s : f' ◯ (transport _ p) ≡ transport _ r ◯ f)
  {g : B → C} {g' : B' → C'} (t : transport _ r ◯ g ≡ g' ◯ (transport _ q))
  → (diag A , B , C , f , g) ≡ (diag A' , B' , C' , f' , g')
pullback-diag-raw-eq refl refl refl refl refl = refl

pullback-diag-eq : ∀ {i} {A A' : Set i} (p : A ≃ A')
  {B B' : Set i} (q : B ≃ B') {C C' : Set i} (r : C ≃ C')
  {f : A → C} {f' : A' → C'} (s : (a : A) → f' ((π₁ p) a) ≡ (π₁ r) (f a))
  {g : B → C} {g' : B' → C'} (t : (b : B) → (π₁ r) (g b) ≡ g' ((π₁ q) b))
  → (diag A , B , C , f , g) ≡ (diag A' , B' , C' , f' , g')
pullback-diag-eq p q r {f} {f'} s {g} {g'} t = pullback-diag-raw-eq
  (eq-to-path p)
  (eq-to-path q)
  (eq-to-path r)
  (funext (λ a → ap f' (trans-id-eq-to-path p a)
                     ∘ (s a ∘ ! (trans-id-eq-to-path r (f a)))))
  (funext (λ b → trans-id-eq-to-path r (g b)
                     ∘ (t b ∘ ap g' (! (trans-id-eq-to-path q b)))))

module Pullback {i} (D : pullback-diag i) where

  open pullback-diag D

  record pullback : Set i where
    constructor _,_,_
    field
      a : A
      b : B
      h : f a ≡ g b

  pullback-eq : {a a' : A} (p : a ≡ a') {b b' : B} (q : b ≡ b')
    {h : f a ≡ g b} {h' : f a' ≡ g b'} (r : h ∘ ap g q ≡ ap f p ∘ h')
    → (a , b , h) ≡ (a' , b' , h')
  pullback-eq refl refl r =
    ap (λ u → _ , _ , u) (! (refl-right-unit _) ∘ r)

open Pullback public

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Module shadowing using generated modules for records and datatypes
module Issue260b where

module R where
record R : Set where

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module UniDB.Subst.StarPrime where

open import UniDB.Subst.Core
open import UniDB.Morph.StarPrime
open import UniDB.Morph.Depth

module _
  {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
  {Ξ : MOR} {{lkTΞ : Lk T Ξ}}
  where

  mutual
    instance
      iLkStar* : Lk T (Star* Ξ)
      lk {{iLkStar*}} refl     i = vr i
      lk {{iLkStar*}} (incl ξ) i = lk ξ i

      iLkStar₁ : Lk T (Star+ Ξ)
      lk {{iLkStar₁}} (step ξs ξ) i = ap {T} (depth ξ 0) (lk ξs i)

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
-- Basic intuitionistic propositional calculus, without ∨ or ⊥.
-- Hilbert-style formalisation of syntax.
-- Nested terms.

module BasicIPC.Syntax.Hilbert where

open import BasicIPC.Syntax.Common public

-- Derivations.

infix 3 _⊢_
data _⊢_ (Γ : Cx Ty) : Ty → Set where
  var   : ∀ {A}     → A ∈ Γ → Γ ⊢ A
  app   : ∀ {A B}   → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
  ci    : ∀ {A}     → Γ ⊢ A ▻ A
  ck    : ∀ {A B}   → Γ ⊢ A ▻ B ▻ A
  cs    : ∀ {A B C} → Γ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
  cpair : ∀ {A B}   → Γ ⊢ A ▻ B ▻ A ∧ B
  cfst  : ∀ {A B}   → Γ ⊢ A ∧ B ▻ A
  csnd  : ∀ {A B}   → Γ ⊢ A ∧ B ▻ B
  unit  : Γ ⊢ ⊤

infix 3 _⊢⋆_
_⊢⋆_ : Cx Ty → Cx Ty → Set
Γ ⊢⋆ ∅     = 𝟙
Γ ⊢⋆ Ξ , A = Γ ⊢⋆ Ξ × Γ ⊢ A

-- Monotonicity with respect to context inclusion.

mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
mono⊢ η (var i)   = var (mono∈ η i)
mono⊢ η (app t u) = app (mono⊢ η t) (mono⊢ η u)
mono⊢ η ci        = ci
mono⊢ η ck        = ck
mono⊢ η cs        = cs
mono⊢ η cpair     = cpair
mono⊢ η cfst      = cfst
mono⊢ η csnd      = csnd
mono⊢ η unit      = unit

mono⊢⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ Ξ → Γ′ ⊢⋆ Ξ
mono⊢⋆ {∅}     η ∙        = ∙
mono⊢⋆ {Ξ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Shorthand for variables.

v₀ : ∀ {A Γ} → Γ , A ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ} → Γ , A , B ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ} → Γ , A , B , C ⊢ A
v₂ = var i₂

-- Reflexivity.

refl⊢⋆ : ∀ {Γ} → Γ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

-- Deduction theorem.

lam : ∀ {A B Γ} → Γ , A ⊢ B → Γ ⊢ A ▻ B
lam (var top)     = ci
lam (var (pop i)) = app ck (var i)
lam (app t u)     = app (app cs (lam t)) (lam u)
lam ci            = app ck ci
lam ck            = app ck ck
lam cs            = app ck cs
lam cpair         = app ck cpair
lam cfst          = app ck cfst
lam csnd          = app ck csnd
lam unit          = app ck unit

lam⋆ : ∀ {Ξ Γ A} → Γ ⧺ Ξ ⊢ A → Γ ⊢ Ξ ▻⋯▻ A
lam⋆ {∅}     = I
lam⋆ {Ξ , B} = lam⋆ {Ξ} ∘ lam

lam⋆₀ : ∀ {Γ A} → Γ ⊢ A → ∅ ⊢ Γ ▻⋯▻ A
lam⋆₀ {∅}     = I
lam⋆₀ {Γ , B} = lam⋆₀ ∘ lam

-- Detachment theorem.

det : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ , A ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

det⋆ : ∀ {Ξ Γ A} → Γ ⊢ Ξ ▻⋯▻ A → Γ ⧺ Ξ ⊢ A
det⋆ {∅}     = I
det⋆ {Ξ , B} = det ∘ det⋆ {Ξ}

det⋆₀ : ∀ {Γ A} → ∅ ⊢ Γ ▻⋯▻ A → Γ ⊢ A
det⋆₀ {∅}     = I
det⋆₀ {Γ , B} = det ∘ det⋆₀

-- Cut and multicut.

cut : ∀ {A B Γ} → Γ ⊢ A → Γ , A ⊢ B → Γ ⊢ B
cut t u = app (lam u) t

multicut : ∀ {Ξ A Γ} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

-- Transitivity.

trans⊢⋆ : ∀ {Γ″ Γ′ Γ} → Γ ⊢⋆ Γ′ → Γ′ ⊢⋆ Γ″ → Γ ⊢⋆ Γ″
trans⊢⋆ {∅}      ts ∙        = ∙
trans⊢⋆ {Γ″ , A} ts (us , u) = trans⊢⋆ ts us , multicut ts u

-- Contraction.

ccont : ∀ {A B Γ} → Γ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ} → Γ , A , A ⊢ B → Γ , A ⊢ B
cont t = det (app ccont (lam (lam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ} → Γ , A , B ⊢ C → Γ , B , A ⊢ C
exch t = det (det (app cexch (lam (lam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C Γ} → Γ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ} → Γ , B ⊢ C → Γ , A ⊢ B → Γ , A ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

-- Useful theorems in functional form.

pair : ∀ {A B Γ} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
pair t u = app (app cpair t) u

fst : ∀ {A B Γ} → Γ ⊢ A ∧ B → Γ ⊢ A
fst t = app cfst t

snd : ∀ {A B Γ} → Γ ⊢ A ∧ B → Γ ⊢ B
snd t = app csnd t

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ → Γ , A ⊢ B → Γ′ ⊢ A → Γ ⧺ Γ′ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

-- Convertibility.

data _⋙_ {Γ : Cx Ty} : ∀ {A} → Γ ⊢ A → Γ ⊢ A → Set where
  refl⋙     : ∀ {A} → {t : Γ ⊢ A}
                     → t ⋙ t

  trans⋙    : ∀ {A} → {t t′ t″ : Γ ⊢ A}
                     → t ⋙ t′ → t′ ⋙ t″
                     → t ⋙ t″

  sym⋙      : ∀ {A} → {t t′ : Γ ⊢ A}
                     → t ⋙ t′
                     → t′ ⋙ t

  congapp⋙  : ∀ {A B} → {t t′ : Γ ⊢ A ▻ B} → {u u′ : Γ ⊢ A}
                       → t ⋙ t′ → u ⋙ u′
                       → app t u ⋙ app t′ u′

  congi⋙    : ∀ {A} → {t t′ : Γ ⊢ A}
                     → t ⋙ t′
                     → app ci t ⋙ app ci t′

  congk⋙    : ∀ {A B} → {t t′ : Γ ⊢ A} → {u u′ : Γ ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app ck t) u ⋙ app (app ck t′) u′

  congs⋙    : ∀ {A B C} → {t t′ : Γ ⊢ A ▻ B ▻ C} → {u u′ : Γ ⊢ A ▻ B} → {v v′ : Γ ⊢ A}
                         → t ⋙ t′ → u ⋙ u′ → v ⋙ v′
                         → app (app (app cs t) u) v ⋙ app (app (app cs t′) u′) v′

  congpair⋙ : ∀ {A B} → {t t′ : Γ ⊢ A} → {u u′ : Γ ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app cpair t) u ⋙ app (app cpair t′) u′

  congfst⋙  : ∀ {A B} → {t t′ : Γ ⊢ A ∧ B}
                       → t ⋙ t′
                       → app cfst t ⋙ app cfst t′

  congsnd⋙  : ∀ {A B} → {t t′ : Γ ⊢ A ∧ B}
                       → t ⋙ t′
                       → app csnd t ⋙ app csnd t′

  -- TODO: Verify this.
  beta▻ₖ⋙   : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                       → app (app ck t) u ⋙ t

  -- TODO: Verify this.
  beta▻ₛ⋙   : ∀ {A B C} → {t : Γ ⊢ A ▻ B ▻ C} → {u : Γ ⊢ A ▻ B} → {v : Γ ⊢ A}
                         → app (app (app cs t) u) v ⋙ app (app t v) (app u v)

  -- TODO: What about eta for ▻?
  beta∧₁⋙   : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                       → app cfst (app (app cpair t) u) ⋙ t

  beta∧₂⋙   : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                       → app csnd (app (app cpair t) u) ⋙ u

  eta∧⋙     : ∀ {A B} → {t : Γ ⊢ A ∧ B}
                       → t ⋙ app (app cpair (app cfst t)) (app csnd t)

  eta⊤⋙    : ∀ {t : Γ ⊢ ⊤} → t ⋙ unit

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- Small parser combinator library used by Mixfix.Acyclic.Grammar
------------------------------------------------------------------------

-- Note that while Mixfix.Acyclic.Lib and Mixfix.Cyclic.Lib may appear
-- to be very similar, there are some important differences:
--
-- • Mixfix.Cyclic.Lib._⊛∞_ accepts delayed parsers,
--   Mixfix.Acyclic.Lib._⊛_ does not.
--
-- • There is a translation from the parsers in Mixfix.Acyclic.Lib to
--   the /simplified/ parsers in
--   StructurallyRecursiveDescentParsing.Simplified; no such
--   translation is defined for the parsers in Mixfix.Cyclic.Lib. Note
--   that the depth-first backend in
--   StructurallyRecursiveDescentParsing.DepthFirst only handles
--   simplified parsers.

module Mixfix.Acyclic.Lib where

open import Algebra
open import Codata.Musical.Notation
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.NonEmpty using (List⁺; _∷_; [_]; _∷⁺_; _⁺∷ʳ_)
import Data.List.Properties
private module LM {A : Set} = Monoid (Data.List.Properties.++-monoid A)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Product
import Data.String.Properties as String
open import Relation.Binary
open DecSetoid String.≡-decSetoid using (_≟_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong)

import StructurallyRecursiveDescentParsing.Simplified as Simplified
open Simplified hiding (⟦_⟧)
open import StructurallyRecursiveDescentParsing.Simplified.Semantics
  as Sem hiding (cast∈; sound; complete)
open import Mixfix.Operator using (NamePart)

------------------------------------------------------------------------
-- Programs

-- Agda's termination checker only accepts corecursive definitions if
-- they are /syntactically/ guarded by constructors. The following
-- small language of "parser programs" reifies a selection of parser
-- combinators as /constructors/. These constructors are then used in
-- Mixfix.Acyclic.Grammar in order to ensure that Agda accepts the
-- grammars defined there.

infix  55 _+
infixl 50 _⊛_ _<$>_
infixl  5 _∣_
infixr  5 _∥_

data ParserProg : Set → Set1 where
  fail      : ∀ {R} → ParserProg R
  _∣_       : ∀ {R}
              (p₁ : ParserProg R)
              (p₂ : ParserProg R) →
                    ParserProg R
  _⊛_       : ∀ {R₁ R₂}
              (p₁ : ParserProg (R₁ → R₂))
              (p₂ : ParserProg R₁) →
                    ParserProg R₂
  _<$>_     : ∀ {R₁ R₂} (f : R₁ → R₂)
              (p : ParserProg R₁) →
                   ParserProg R₂
  _+        : ∀ {R} (p : ParserProg R) →
                         ParserProg (List⁺ R)
  _between_ : ∀ {R n}
              (p : ∞ (ParserProg R)) (toks : Vec NamePart (1 + n)) →
              ParserProg (Vec R n)
  _∥_       : ∀ {I i} {R : I → Set}
              (p₁ : ParserProg (R i))
              (p₂ : ParserProg (∃ R)) →
                    ParserProg (∃ R)

-- Parses a given token.

tok : NamePart → Parser NamePart false NamePart
tok tok = token !>>= λ tok′ → ♯ ok tok′
  module TheToken where
  okIndex : NamePart → Bool
  okIndex tok′ with tok ≟ tok′
  ... | yes _ = true
  ... | no  _ = false

  ok : (tok′ : NamePart) → Parser NamePart (okIndex tok′) NamePart
  ok tok′ with tok ≟ tok′
  ... | yes _ = return tok′
  ... | no  _ = fail

-- Interprets the parser programs as parsers.

private
  infix 10 ♯′_

  ♯′_ : {A : Set₁} → A → ∞ A
  ♯′ x = ♯ x

⟦_⟧ : ∀ {R} → ParserProg R → Parser NamePart false R
⟦ fail                    ⟧ = fail
⟦ p₁ ∣ p₂                 ⟧ = ⟦ p₁ ⟧ ∣ ⟦ p₂ ⟧
⟦ p₁ ⊛ p₂                 ⟧ = ⟦ p₁ ⟧ !>>= λ f → ♯ ⟦ f <$> p₂ ⟧
⟦ f <$> p                 ⟧ = ⟦ p  ⟧ !>>= λ x → ♯′ return (f x)
⟦ p +                     ⟧ = ⟦ p  ⟧ !>>= λ x → ♯
                              (⟦ _∷⁺_ x <$> p + ⟧ ∣ return [ x ])
⟦ p between (t ∷ [])      ⟧ = tok t !>>= λ _ → ♯′ return []
⟦ p between (t ∷ t′ ∷ ts) ⟧ = tok t !>>= λ _ → ♯
                              ⟦ _∷_ <$> ♭ p ⊛ (p between (t′ ∷ ts)) ⟧
⟦ p₁ ∥ p₂                 ⟧ = (⟦ p₁ ⟧ !>>= λ x → ♯′ return (-, x)) ∣
                              ⟦ p₂ ⟧

------------------------------------------------------------------------
-- Semantics of the programs

module Semantics where

  -- This definition may seem unnecessary: why not simply define
  --
  --   x ∈⟦ p ⟧· s  =  x ∈ ⟦ p ⟧ · s?
  --
  -- One reason is that it is hard for Agda to infer the value of p
  -- from ⟦ p ⟧ (note that ⟦_⟧ is a function which evaluates). By
  -- using the definition below this problem is avoided. A more
  -- important reason may be that the definition below ensures that
  -- the details of ⟦_⟧ do not need to be understood.

  infix  60 <$>_
  infixl 50 _⊛_
  infix  4  _∈⟦_⟧·_

  data _∈⟦_⟧·_ : ∀ {R} → R → ParserProg R → List NamePart → Set₁ where
    ∣ˡ         : ∀ {R x s}
                   {p₁ : ParserProg R} {p₂ : ParserProg R}
                 (x∈p₁ : x ∈⟦ p₁ ⟧· s) → x ∈⟦ p₁ ∣ p₂ ⟧· s
    ∣ʳ         : ∀ {R x s}
                   {p₁ : ParserProg R} {p₂ : ParserProg R}
                 (x∈p₂ : x ∈⟦ p₂ ⟧· s) → x ∈⟦ p₁ ∣ p₂ ⟧· s
    _⊛_        : ∀ {s₁ s₂ R₁ R₂ f x}
                   {p₁ : ParserProg (R₁ → R₂)}
                   {p₂ : ParserProg R₁}
                 (f∈p₁ : f ∈⟦ p₁ ⟧· s₁)
                 (x∈p₂ : x ∈⟦ p₂ ⟧· s₂) →
                 f x ∈⟦ p₁ ⊛ p₂ ⟧· s₁ ++ s₂
    <$>_       : ∀ {s R₁ R₂ x} {f : R₁ → R₂} {p : ParserProg R₁}
                 (x∈p : x ∈⟦ p ⟧· s) → f x ∈⟦ f <$> p ⟧· s
    +-[]       : ∀ {R x s} {p : ParserProg R}
                 (x∈p : x ∈⟦ p ⟧· s) → [ x ] ∈⟦ p + ⟧· s
    +-∷        : ∀ {R x s₁ s₂ xs} {p : ParserProg R}
                 (x∈p : x ∈⟦ p ⟧· s₁) (xs∈p : xs ∈⟦ p + ⟧· s₂) →
                 x ∷⁺ xs ∈⟦ p + ⟧· s₁ ++ s₂
    between-[] : ∀ {R t} {p : ∞ (ParserProg R)} →
                 [] ∈⟦ p between (t ∷ []) ⟧· t ∷ []
    between-∷  : ∀ {R n t x xs s₁ s₂}
                   {p : ∞ (ParserProg R)} {ts : Vec NamePart (suc n)}
                 (x∈p : x ∈⟦ ♭ p ⟧· s₁)
                 (xs∈⋯ : xs ∈⟦ p between ts ⟧· s₂) →
                 x ∷ xs ∈⟦ p between (t ∷ ts) ⟧· t ∷ s₁ ++ s₂
    ∥ˡ         : ∀ {I i} {R : I → Set} {x s}
                   {p₁ : ParserProg (R i)}
                   {p₂ : ParserProg (∃ R)}
                 (x∈p₁ : x ∈⟦ p₁ ⟧· s) → (-, x) ∈⟦ p₁ ∥ p₂ ⟧· s
    ∥ʳ         : ∀ {I i} {R : I → Set} {x s}
                   {p₁ : ParserProg (R i)}
                   {p₂ : ParserProg (∃ R)}
                 (x∈p₂ : x ∈⟦ p₂ ⟧· s) → x ∈⟦ p₁ ∥ p₂ ⟧· s

  -- The semantics is correct. (Note that this proof only establishes
  -- language equivalence, not parser equivalence; see
  -- TotalParserCombinators.Semantics.)

  private

    drop-[] : ∀ {R s x} {p : Parser NamePart false R} →
              x ∈ p · s ++ [] → x ∈ p · s
    drop-[] = Sem.cast∈ refl refl (proj₂ LM.identity _)

    add-[] : ∀ {R s x} {p : ParserProg R} →
             x ∈⟦ p ⟧· s → x ∈⟦ p ⟧· s ++ []
    add-[] {s = s} x∈p rewrite proj₂ LM.identity s = x∈p

  ⊛-complete : ∀ {s₁ s₂ R₁ R₂ f x}
               (p₁ : ParserProg (R₁ → R₂)) {p₂ : ParserProg R₁} →
               f ∈ ⟦ p₁ ⟧ · s₁ → x ∈ ⟦ p₂ ⟧ · s₂ →
               f x ∈ ⟦ p₁ ⊛ p₂ ⟧ · s₁ ++ s₂
  ⊛-complete _ f∈p₁ x∈p₂ = f∈p₁ !>>= drop-[] (x∈p₂ !>>= return)

  tok-sound : ∀ {t t′ s} →
              t′ ∈ tok t · s →
              t ≡ t′ × s ≡ t′ ∷ []
  tok-sound {t} (_!>>=_ {x = t″} token t′∈) with t ≟ t″
  tok-sound (token !>>= return) | yes t≈t″ = (t≈t″ , refl)
  tok-sound (token !>>= ())     | no  t≉t″

  tok-complete : ∀ {t} → t ∈ tok t · t ∷ []
  tok-complete {t} = token !>>= ok-lemma
    where
    ok-lemma : t ∈ TheToken.ok t t · []
    ok-lemma with t ≟ t
    ... | yes refl = return
    ... | no  t≢t  with t≢t refl
    ...   | ()

  sound : ∀ {R x s} {p : ParserProg R} →
          x ∈⟦ p ⟧· s → x ∈ ⟦ p ⟧ · s
  sound (∣ˡ x∈p₁)                 = ∣ˡ       (sound x∈p₁)
  sound (∣ʳ x∈p₂)                 = ∣ʳ false (sound x∈p₂)
  sound (_⊛_ {p₁ = p₁} f∈p₁ x∈p₂) = ⊛-complete p₁ (sound f∈p₁) (sound x∈p₂)
  sound (<$> x∈p)                 = drop-[] (sound x∈p !>>= return)
  sound (+-[] x∈p)                = drop-[] (sound x∈p !>>= ∣ʳ false return)
  sound (+-∷ x∈p xs∈p)            = sound x∈p !>>= ∣ˡ (drop-[] (sound xs∈p !>>= return))
  sound (∥ˡ x∈p₁)                 = drop-[] (∣ˡ {x = (-, _)} (sound x∈p₁ !>>= return))
  sound (∥ʳ x∈p₂)                 = ∣ʳ false (sound x∈p₂)
  sound between-[]                = tok-complete !>>= return
  sound (between-∷ {s₁ = s₁} {p = p} {ts = _ ∷ _} x∈p xs∈⋯) =
    tok-complete !>>=
    ⊛-complete (_ <$> ♭ p) (drop-[] {s = s₁} (sound x∈p !>>= return)) (sound xs∈⋯)

  complete : ∀ {R x s} (p : ParserProg R) →
             x ∈ ⟦ p ⟧ · s → x ∈⟦ p ⟧· s
  complete fail      ()

  complete (p₁ ∣ p₂) (∣ˡ        x∈p₁) = ∣ˡ (complete p₁ x∈p₁)
  complete (p₁ ∣ p₂) (∣ʳ .false x∈p₂) = ∣ʳ (complete p₂ x∈p₂)

  complete (p₁ ⊛ p₂) (f∈p₁ !>>= (y∈p₂ !>>= return)) =
    complete p₁ f∈p₁ ⊛ add-[] (complete p₂ y∈p₂)

  complete (f <$> p) (x∈p !>>= return) = add-[] (<$> complete p x∈p)

  complete (p +) (x∈p !>>= ∣ˡ (xs∈p+ !>>= return)) = +-∷ (complete p x∈p) (add-[] (complete (p +) xs∈p+))
  complete (p +) (x∈p !>>= ∣ʳ .false return)       = add-[] (+-[] (complete p x∈p))

  complete (p between (t ∷ [])) (t∈ !>>= return) with tok-sound t∈
  ... | (refl , refl) = between-[]
  complete (p between (t ∷ t′ ∷ ts))
           (t∈ !>>= (x∈p !>>= return !>>= (xs∈ !>>= return))) with tok-sound t∈
  ... | (refl , refl) =
    between-∷ (add-[] (complete (♭ p) x∈p))
              (add-[] (complete (p between (t′ ∷ ts)) xs∈))

  complete (p₁ ∥ p₂) (∣ˡ (x∈p₁ !>>= return)) = add-[] (∥ˡ (complete p₁ x∈p₁))
  complete (p₁ ∥ p₂) (∣ʳ .false x∈p₂)        = ∥ʳ (complete p₂ x∈p₂)

------------------------------------------------------------------------
-- A variant of the semantics

-- The alternative semantics defined below may be slightly harder to
-- understand, but it is (language) equivalent to the one above, and
-- it simplifies the proof in Mixfix.Acyclic.Show.

module Semantics-⊕ where

  infix  60 <$>_
  infixl 50 _⊛_
  infix  4  _⊕_∈⟦_⟧·_

  data _⊕_∈⟦_⟧·_ : ∀ {R} →
                   R → List NamePart → ParserProg R → List NamePart → Set1 where
    ∣ˡ         : ∀ {R x s s₁}
                   {p₁ : ParserProg R} {p₂ : ParserProg R}
                 (x∈p₁ : x ⊕ s₁ ∈⟦ p₁ ⟧· s) → x ⊕ s₁ ∈⟦ p₁ ∣ p₂ ⟧· s
    ∣ʳ         : ∀ {R x s s₁}
                   {p₁ : ParserProg R} {p₂ : ParserProg R}
                 (x∈p₂ : x ⊕ s₁ ∈⟦ p₂ ⟧· s) → x ⊕ s₁ ∈⟦ p₁ ∣ p₂ ⟧· s
    _⊛_        : ∀ {s s₁ s₂ R₁ R₂ f x}
                   {p₁ : ParserProg (R₁ → R₂)} {p₂ : ParserProg R₁}
                 (f∈p₁ : f ⊕ s₁ ∈⟦ p₁ ⟧· s) (x∈p₂ : x ⊕ s₂ ∈⟦ p₂ ⟧· s₁) →
                 f x ⊕ s₂ ∈⟦ p₁ ⊛ p₂ ⟧· s
    <$>_       : ∀ {s s′ R₁ R₂ x} {f : R₁ → R₂} {p : ParserProg R₁}
                 (x∈p : x ⊕ s′ ∈⟦ p ⟧· s) → f x ⊕ s′ ∈⟦ f <$> p ⟧· s
    +-[]       : ∀ {R x s s₁} {p : ParserProg R}
                 (x∈p : x ⊕ s₁ ∈⟦ p ⟧· s) → [ x ] ⊕ s₁ ∈⟦ p + ⟧· s
    +-∷        : ∀ {R x s s₁ s₂ xs} {p : ParserProg R}
                 (x∈p : x ⊕ s₁ ∈⟦ p ⟧· s) (xs∈p : xs ⊕ s₂ ∈⟦ p + ⟧· s₁) →
                 x ∷⁺ xs ⊕ s₂ ∈⟦ p + ⟧· s
    between-[] : ∀ {R t s} {p : ∞ (ParserProg R)} →
                 [] ⊕ s ∈⟦ p between (t ∷ []) ⟧· t ∷ s
    between-∷  : ∀ {R n t x xs s s₁ s₂}
                   {p : ∞ (ParserProg R)} {ts : Vec NamePart (suc n)}
                 (x∈p : x ⊕ s₁ ∈⟦ ♭ p ⟧· s)
                 (xs∈⋯ : xs ⊕ s₂ ∈⟦ p between ts ⟧· s₁) →
                 x ∷ xs ⊕ s₂ ∈⟦ p between (t ∷ ts) ⟧· t ∷ s
    ∥ˡ         : ∀ {I i} {R : I → Set} {x s s′}
                   {p₁ : ParserProg (R i)}
                   {p₂ : ParserProg (∃ R)}
                 (x∈p₁ : x ⊕ s′ ∈⟦ p₁ ⟧· s) →
                 (-, x) ⊕ s′ ∈⟦ p₁ ∥ p₂ ⟧· s
    ∥ʳ         : ∀ {I i} {R : I → Set} {s s′ i′} {x : R i′}
                   {p₁ : ParserProg (R i)}
                   {p₂ : ParserProg (∃ R)}
                 (x∈p₂ : (-, x) ⊕ s′ ∈⟦ p₂ ⟧· s) →
                 (-, x) ⊕ s′ ∈⟦ p₁ ∥ p₂ ⟧· s

  -- The semantics is correct.

  ⊛-complete : ∀ {s s₁ s₂ R₁ R₂ f x}
               (p₁ : ParserProg (R₁ → R₂)) {p₂ : ParserProg R₁} →
               f ⊕ s₁ ∈ ⟦ p₁ ⟧ · s → x ⊕ s₂ ∈ ⟦ p₂ ⟧ · s₁ →
               f x ⊕ s₂ ∈ ⟦ p₁ ⊛ p₂ ⟧ · s
  ⊛-complete _ f∈p₁ x∈p₂ = f∈p₁ !>>= (x∈p₂ !>>= return)

  tok-sound : ∀ {t t′ s₁ s} →
              t′ ⊕ s₁ ∈ tok t · s →
              t ≡ t′ × s ≡ t′ ∷ s₁
  tok-sound     ∈ with Sem.⊕-sound′ ∈
  tok-sound     ∈ | (s         , refl , ∈′) with Semantics.tok-sound ∈′
  tok-sound {t} ∈ | (.(t ∷ []) , refl , ∈′) | (refl , refl) = (refl , refl)

  tok-complete : ∀ {t s} → t ⊕ s ∈ tok t · t ∷ s
  tok-complete = Sem.⊕-complete′ (_ , refl , Semantics.tok-complete)

  sound : ∀ {R x s s′} {p : ParserProg R} →
          x ⊕ s′ ∈⟦ p ⟧· s → x ⊕ s′ ∈ ⟦ p ⟧ · s
  sound (∣ˡ x∈p₁)                 = ∣ˡ       (sound x∈p₁)
  sound (∣ʳ x∈p₂)                 = ∣ʳ false (sound x∈p₂)
  sound (_⊛_ {p₁ = p₁} f∈p₁ x∈p₂) = ⊛-complete p₁ (sound f∈p₁) (sound x∈p₂)
  sound (<$> x∈p)                 = sound x∈p !>>= return
  sound (+-[] x∈p)                = sound x∈p !>>= ∣ʳ false return
  sound (+-∷ x∈p xs∈p)            = sound x∈p !>>= ∣ˡ (sound xs∈p !>>= return)
  sound (∥ˡ x∈p₁)                 = ∣ˡ (sound x∈p₁ !>>= return)
  sound (∥ʳ x∈p₂)                 = ∣ʳ false (sound x∈p₂)
  sound between-[]                = tok-complete !>>= return
  sound (between-∷ {p = p} {ts = _ ∷ _} x∈p xs∈⋯) =
    tok-complete !>>=
    ⊛-complete (_ <$> ♭ p) (sound x∈p !>>= return) (sound xs∈⋯)

  complete : ∀ {R x s s′} (p : ParserProg R) →
             x ⊕ s′ ∈ ⟦ p ⟧ · s → x ⊕ s′ ∈⟦ p ⟧· s
  complete fail      ()

  complete (p₁ ∣ p₂) (∣ˡ        x∈p₁) = ∣ˡ (complete p₁ x∈p₁)
  complete (p₁ ∣ p₂) (∣ʳ .false x∈p₂) = ∣ʳ (complete p₂ x∈p₂)

  complete (p₁ ⊛ p₂) (f∈p₁ !>>= (y∈p₂ !>>= return)) =
    complete p₁ f∈p₁ ⊛ complete p₂ y∈p₂

  complete (f <$> p) (x∈p !>>= return) = <$> complete p x∈p

  complete (p +) (x∈p !>>= ∣ˡ (xs∈p+ !>>= return)) = +-∷  (complete p x∈p) (complete (p +) xs∈p+)
  complete (p +) (x∈p !>>= ∣ʳ .false return)       = +-[] (complete p x∈p)

  complete (p between (t ∷ [])) (t∈ !>>= return) with tok-sound t∈
  ... | (refl , refl) = between-[]
  complete (p between (t ∷ t′ ∷ ts))
           (t∈ !>>= (x∈p !>>= return !>>= (xs∈ !>>= return))) with tok-sound t∈
  ... | (refl , refl) =
    between-∷ (complete (♭ p) x∈p) (complete (p between (t′ ∷ ts)) xs∈)

  complete (p₁ ∥ p₂) (∣ˡ (x∈p₁ !>>= return)) = ∥ˡ (complete p₁ x∈p₁)
  complete (p₁ ∥ p₂) (∣ʳ .false x∈p₂)        = ∥ʳ (complete p₂ x∈p₂)

  -- Some lemmas.

  +-∷ʳ : ∀ {R x s s₁ s₂ xs} {p : ParserProg R} →
         xs ⊕ s₁ ∈⟦ p + ⟧· s → x ⊕ s₂ ∈⟦ p ⟧· s₁ →
         xs ⁺∷ʳ x ⊕ s₂ ∈⟦ p + ⟧· s
  +-∷ʳ {xs = _ ∷ ._} (+-[] x∈p)     y∈p = +-∷ x∈p (+-[] y∈p)
  +-∷ʳ {xs = _ ∷ ._} (+-∷ x∈p xs∈p) y∈p = +-∷ x∈p (+-∷ʳ xs∈p y∈p)

  cast∈ : ∀ {R x₁ x₂ s s′} {p : ParserProg R} →
          x₁ ≡ x₂ → x₁ ⊕ s′ ∈⟦ p ⟧· s → x₂ ⊕ s′ ∈⟦ p ⟧· s
  cast∈ refl x∈p = x∈p

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A Categorical view of the Sum type (Left-biased)
------------------------------------------------------------------------

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

open import Level

module Data.Sum.Categorical.Left {a} (A : Set a) (b : Level) where

open import Data.Sum
open import Category.Functor
open import Category.Applicative
open import Category.Monad
import Function.Identity.Categorical as Id
open import Function

-- To minimize the universe level of the RawFunctor, we require that elements of
-- B are "lifted" to a copy of B at a higher universe level (a ⊔ b). See the
-- examples for how this is done.

------------------------------------------------------------------------
-- Left-biased monad instance for _⊎_

Sumₗ : Set (a ⊔ b) → Set (a ⊔ b)
Sumₗ B = A ⊎ B

functor : RawFunctor Sumₗ
functor = record { _<$>_ = map₂ }

applicative : RawApplicative Sumₗ
applicative = record
  { pure = inj₂
  ; _⊛_ = [ const ∘ inj₁ , map₂ ]′
  }

-- The monad instance also requires some mucking about with universe levels.
monadT : RawMonadT (_∘′ Sumₗ)
monadT M = record
  { return = M.pure ∘ inj₂
  ; _>>=_  = λ ma f → ma M.>>= [ M.pure ∘′ inj₁ , f ]′
  } where module M = RawMonad M

monad : RawMonad Sumₗ
monad = monadT Id.monad

------------------------------------------------------------------------
-- Get access to other monadic functions

module _ {F} (App : RawApplicative {a ⊔ b} F) where

  open RawApplicative App

  sequenceA : ∀ {A} → Sumₗ (F A) → F (Sumₗ A)
  sequenceA (inj₁ a) = pure (inj₁ a)
  sequenceA (inj₂ x) = inj₂ <$> x

  mapA : ∀ {A B} → (A → F B) → Sumₗ A → F (Sumₗ B)
  mapA f = sequenceA ∘ map₂ f

  forA : ∀ {A B} → Sumₗ A → (A → F B) → F (Sumₗ B)
  forA = flip mapA

module _ {M} (Mon : RawMonad {a ⊔ b} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM : ∀ {A} → Sumₗ (M A) → M (Sumₗ A)
  sequenceM = sequenceA App

  mapM : ∀ {A B} → (A → M B) → Sumₗ A → M (Sumₗ B)
  mapM = mapA App

  forM : ∀ {A B} → Sumₗ A → (A → M B) → M (Sumₗ B)
  forM = forA App


text: {-# REWRITE #-}


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module SAT-solver where

import 14-univalence
open 14-univalence public

{- The literates are atomic propositions or negations thereof. We simply use
   the natural numbers to encode the atomic propositions, and we use the
   booleans to tell whether it should be negated or not. -}

Literate = ℕ × bool

neg-Literate : Literate → Literate
neg-Literate (pair n b) = pair n (neg-𝟚 b)

zero-true-Literate : Literate
zero-true-Literate = pair zero-ℕ true

truth-value-Literate : (ℕ → bool) → Literate → bool
truth-value-Literate f (pair n true) = f n
truth-value-Literate f (pair n false) = neg-𝟚 (f n)

bool-Eq-ℕ : ℕ → ℕ → bool
bool-Eq-ℕ zero-ℕ zero-ℕ = true
bool-Eq-ℕ zero-ℕ (succ-ℕ n) = false
bool-Eq-ℕ (succ-ℕ m) zero-ℕ = false
bool-Eq-ℕ (succ-ℕ m) (succ-ℕ n) = bool-Eq-ℕ m n

bool-Eq-𝟚 : bool → bool → bool
bool-Eq-𝟚 true true = true
bool-Eq-𝟚 true false = false
bool-Eq-𝟚 false true = false
bool-Eq-𝟚 false false = true

bool-Eq-Literate : Literate → Literate → bool
bool-Eq-Literate (pair m x) (pair n y) =
  conjunction-𝟚 (bool-Eq-ℕ m n) (bool-Eq-𝟚 x y)

{- Clauses are finite disjunctions of literates. We simply encode them using
   lists of literates. -}

Clause = list Literate

clause-Literate : Literate → Clause
clause-Literate l = cons l nil

is-literate-Clause : Clause → UU lzero
is-literate-Clause c = Σ Literate (λ l → Id (clause-Literate l) c)

zero-true-Clause = clause-Literate zero-true-Literate

truth-value-Clause : (ℕ → bool) → Clause → bool
truth-value-Clause f nil = false
truth-value-Clause f (cons l c) =
  disjunction-𝟚 (truth-value-Literate f l) (truth-value-Clause f c)

contains-Clause : Literate → Clause → bool
contains-Clause l nil = false
contains-Clause l (cons l' c) =
  disjunction-𝟚 (bool-Eq-Literate l l') (contains-Clause l c)

if-then-else : {l : Level} {A : UU l} → bool → A → A → A
if-then-else true x y = x
if-then-else false x y = y

if-then-else-dep :
  {l1 l2 : Level} {A : UU l1} (B : A → UU l2)
  (b : bool) {x y : A} (u : Id b true → B x) (v : Id b false → B y) →
  B (if-then-else b x y)
if-then-else-dep B true u v = u refl
if-then-else-dep B false u v = v refl

{- We write a function that simplifies a clause in the following way:
    * simplified clauses do not contain any literate more than once.
    * if a simplified clause contains a literate and its negation, then it is
      of the form l ∨ ¬l. -}

simplify-Clause : Clause → Clause
simplify-Clause nil = nil
simplify-Clause (cons l c) =
  if-then-else
    ( contains-Clause (neg-Literate l) c)
    ( cons l (cons (neg-Literate l) nil))
    ( if-then-else
      ( contains-Clause l c)
      ( simplify-Clause c)
      ( cons l (simplify-Clause c)))

is-satisfiable-Clause : Clause → UU lzero
is-satisfiable-Clause c = Σ (ℕ → bool) (λ f → Id (truth-value-Clause f c) true)

{- We show that any non-empty disjunctive clause is satisfiable. -}

right-true-law-disjunction-𝟚 : (b : bool) → Id (disjunction-𝟚 b true) true
right-true-law-disjunction-𝟚 true = refl
right-true-law-disjunction-𝟚 false = refl

left-true-law-disjunction-𝟚 : (b : bool) → Id (disjunction-𝟚 true b) true
left-true-law-disjunction-𝟚 true = refl
left-true-law-disjunction-𝟚 false = refl

is-satisfiable-cons-Clause :
  ( l : Literate) (c : Clause) → is-satisfiable-Clause (cons l c)
is-satisfiable-cons-Clause (pair n true) c =
  pair
    ( const ℕ bool true)
    ( left-true-law-disjunction-𝟚 (truth-value-Clause (const ℕ bool true) c))
is-satisfiable-cons-Clause (pair n false) c =
  pair
    ( const ℕ bool false)
    ( left-true-law-disjunction-𝟚 (truth-value-Clause (const ℕ bool false) c))

{- Formulas in conjunctive normal form are finite conjunctions of clauses, as
   defined above. Therefore we encode them as lists of clauses. -}

CNF = list Clause

truth-value-CNF : (ℕ → bool) → CNF → bool
truth-value-CNF f nil = true
truth-value-CNF f (cons c φ) =
  conjunction-𝟚 (truth-value-Clause f c) (truth-value-CNF f φ)

{- A formula φ is in conjunctive normal form is said to be satisfiable if there
   is a map ℕ → bool which evaluates φ to true. -}

is-satisfiable-CNF : CNF → UU lzero
is-satisfiable-CNF φ = Σ (ℕ → bool) (λ f → Id (truth-value-CNF f φ) true)

contains-CNF : (l : Literate) (φ : CNF) → bool
contains-CNF l nil = false
contains-CNF l (cons c φ) =
  disjunction-𝟚 (contains-Clause l c) (contains-CNF l φ)

contains

simplify-CNF : CNF → CNF
simplify-CNF nil = nil
simplify-CNF (cons c φ) = cons (simplify-Clause c) (simplify-CNF φ)

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
open import Data.Product using ( _,_ )
open import Data.Unit using ( ⊤ ; tt )
open import FRP.LTL.ISet.Core using ( ISet ; [_] ; _,_ )

module FRP.LTL.ISet.Unit where

T : ISet
T = [ (λ i → ⊤) , (λ i j i~j t → (tt , tt)) , (λ i j i⊑j t → tt) ]

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl