text:
------------------------------------------------------------------------
-- Properties of non-empty lists
------------------------------------------------------------------------

module Data.List.NonEmpty.Properties where

open import Algebra
open import Category.Monad
open import Data.Function
open import Data.Product
open import Data.List as List using (List; []; _∷_; _++_)
open RawMonad List.monad using () renaming (_>>=_ to _⋆>>=_)
private module LM {A} = Monoid (List.monoid A)
open import Data.List.NonEmpty as List⁺
open RawMonad List⁺.monad
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

η : ∀ {A} (xs : List⁺ A) → head xs ∷ tail xs ≡ List⁺.toList xs
η [ x ]    = refl
η (x ∷ xs) = refl

toList-fromList : ∀ {A} x (xs : List A) →
                  x ∷ xs ≡ List⁺.toList (List⁺.fromList x xs)
toList-fromList x []       = refl
toList-fromList x (y ∷ xs) = cong (_∷_ x) (toList-fromList y xs)

toList-⁺++ : ∀ {A} (xs : List⁺ A) ys →
             List⁺.toList xs ++ ys ≡
             List⁺.toList (xs ⁺++ ys)
toList-⁺++ [ x ]    ys = toList-fromList x ys
toList-⁺++ (x ∷ xs) ys = cong (_∷_ x) (toList-⁺++ xs ys)

toList-⁺++⁺ : ∀ {A} (xs ys : List⁺ A) →
              List⁺.toList xs ++ List⁺.toList ys ≡
              List⁺.toList (xs ⁺++⁺ ys)
toList-⁺++⁺ [ x ]    ys = refl
toList-⁺++⁺ (x ∷ xs) ys = cong (_∷_ x) (toList-⁺++⁺ xs ys)

toList->>= : ∀ {A B} (f : A → List⁺ B) (xs : List⁺ A) →
             (List⁺.toList xs ⋆>>= List⁺.toList ∘ f) ≡
             (List⁺.toList (xs >>= f))
toList->>= f [ x ]    = proj₂ LM.identity _
toList->>= f (x ∷ xs) = begin
  List⁺.toList (f x) ++ (List⁺.toList xs ⋆>>= List⁺.toList ∘ f) ≡⟨ cong (_++_ (List⁺.toList (f x))) (toList->>= f xs) ⟩
  List⁺.toList (f x) ++ List⁺.toList (xs >>= f)                 ≡⟨ toList-⁺++⁺ (f x) (xs >>= f) ⟩
  List⁺.toList (f x ⁺++⁺ (xs >>= f))                            ∎


text:
module Thesis.SIRelBigStep.DLang where

open import Thesis.SIRelBigStep.DSyntax public
open import Thesis.SIRelBigStep.DOpSem public
open import Thesis.SIRelBigStep.DLangDerive public

ext: agda

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Universes
------------------------------------------------------------------------

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

module Data.Universe where

open import Data.Product
open import Level

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

record Universe u e : Set (suc (u ⊔ e)) where
  field
    U : Set u       -- Codes.
    El : U → Set e  -- Decoding function.


text:
------------------------------------------------------------------------------
-- First-order logic theorems
------------------------------------------------------------------------------

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

-- This module contains some examples showing the use of the ATPs for
-- proving first-order logic theorems.

module FOL.TheoremsATP where

open import FOL.Base

------------------------------------------------------------------------------
-- We postulate some formulae and propositional functions.
postulate
  A     : Set
  A¹ B¹ : D → Set
  A²    : D → D → Set

-- The introduction and elimination rules for the quantifiers are theorems.
{-
      φ(x)
  -----------  ∀-intro
    ∀x.φ(x)

    ∀x.φ(x)
  -----------  ∀-elim
     φ(t)

      φ(t)
  -----------  ∃-intro
    ∃x.φ(x)

   ∃x.φ(x)   φ(x) → ψ
 ----------------------  ∃-elim
           ψ
-}

postulate
  ∀-intro : ((x : D) → A¹ x) → ∀ x → A¹ x
  ∀-intro' : ((x : D) → A¹ x) → ⋀ A¹
  ∀-elim  : (t : D) → (∀ x → A¹ x) → A¹ t
  ∀-elim' : (t : D) → ⋀ A¹ → A¹ t
  ∃-intro : (t : D) → A¹ t → ∃ A¹
  ∃-elim  : ∃ A¹ → ((x : D) → A¹ x → A) → A
{-# ATP prove ∀-intro #-}
{-# ATP prove ∀-intro' #-}
{-# ATP prove ∀-elim #-}
{-# ATP prove ∀-elim' #-}
{-# ATP prove ∃-intro #-}
{-# ATP prove ∃-elim #-}

-- Generalization of De Morgan's laws.
postulate
  gDM₁ : ¬ (∀ x → A¹ x) ↔ (∃[ x ] ¬ (A¹ x))
  gDM₂ : ¬ (∃ A¹)       ↔ (∀ x → ¬ (A¹ x))
  gDM₃ : (∀ x → A¹ x)   ↔ ¬ (∃[ x ] ¬ (A¹ x))
  gDM₄ : ∃ A¹           ↔ ¬ (∀ x → ¬ (A¹ x))
{-# ATP prove gDM₁ #-}
{-# ATP prove gDM₂ #-}
{-# ATP prove gDM₃ #-}
{-# ATP prove gDM₄ #-}

-- The order of quantifiers of the same sort is irrelevant.
postulate
  ∀-ord : (∀ x y → A² x y) ↔ (∀ y x → A² x y)
  ∃-ord : (∃[ x ] ∃[ y ] A² x y) ↔ (∃[ y ] ∃[ x ] A² x y)
{-# ATP prove ∀-ord #-}
{-# ATP prove ∃-ord #-}

-- Quantification over a variable that does not occur can be erased or
-- added.
postulate ∃-erase-add : (∃[ x ] A ∧ A¹ x) ↔ A ∧ (∃[ x ] A¹ x)
{-# ATP prove ∃-erase-add #-}

-- Distributes laws for the quantifiers.
postulate
  ∀-dist : (∀ x → A¹ x ∧ B¹ x) ↔ ((∀ x → A¹ x) ∧ (∀ x → B¹ x))
  ∃-dist : (∃[ x ] (A¹ x ∨ B¹ x)) ↔ (∃ A¹ ∨ ∃ B¹)
{-# ATP prove ∀-dist #-}
{-# ATP prove ∃-dist #-}

-- Interchange of quantifiers.
-- The related theorem ∀x∃y.Axy → ∃y∀x.Axy is not (classically) valid.
postulate ∃∀ : ∃[ x ] (∀ y → A² x y) → ∀ y → ∃[ x ] A² x y
{-# ATP prove ∃∀ #-}

-- ∃ in terms of ∀ and ¬.
postulate
  ∃→¬∀¬ : ∃[ x ] A¹ x → ¬ (∀ {x} → ¬ A¹ x)
  ∃¬→¬∀ : ∃[ x ] ¬ A¹ x → ¬ (∀ {x} → A¹ x)
{-# ATP prove ∃→¬∀¬ #-}
{-# ATP prove ∃¬→¬∀ #-}

-- ∀ in terms of ∃ and ¬.
postulate
  ∀→¬∃¬ : (∀ {x} → A¹ x) → ¬ (∃[ x ] ¬ A¹ x)
  ∀¬→¬∃ : (∀ {x} → ¬ A¹ x) → ¬ (∃[ x ] A¹ x)
{-# ATP prove ∀→¬∃¬ #-}
{-# ATP prove ∀¬→¬∃ #-}

-- Distribution of ∃ and ∨.
postulate ∃∨ : ∃[ x ](A¹ x ∨ B¹ x) → (∃[ x ] A¹ x) ∨ (∃[ x ] B¹ x)
{-# ATP prove ∃∨ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Logic
open import Structure.Setoid
open import Structure.Operator.Ring
open import Structure.OrderedField
open import Type

module Structure.OrderedField.AbsoluteValue
  {ℓ ℓₗ ℓₑ}
  {F : Type{ℓ}}
  ⦃ equiv : Equiv{ℓₑ}(F) ⦄
  (_+_ _⋅_ : F → F → F)
  (_≤_ : F → F → Stmt{ℓₗ})
  ⦃ ring : Ring(_+_)(_⋅_) ⦄ -- TODO: The definition does not require a ring, only some kind of total order compatible with an operation with an identity and an inverse
  -- ⦃ identity : Identity(_+_) ⦄
  -- ⦃ inverseFunction : InverseFunction(_+_)(−_) ⦄
  ⦃ ordered : Ordered(_+_)(_⋅_)(_≤_) ⦄
  where

open Ring(ring)
open Ordered(ordered)

import      Lvl
open import Data.Boolean
open import Data.Boolean.Proofs
import      Data.Either as Either
open import Functional
open import Logic.IntroInstances
open import Logic.Propositional
open import Structure.Function.Domain
open import Structure.Function.Ordering
open import Structure.Function
open import Structure.Operator
open import Structure.Operator.Proofs
open import Structure.Operator.Properties
open import Structure.Operator.Ring.Proofs
open import Structure.Relator.Properties
open import Syntax.Implication
open import Syntax.Transitivity

‖_‖ : F → F
‖ x ‖ = if Either.isRight(converseTotal(_≤_){𝟎}{x}) then (− x) else x

instance
  abs-function : Function(‖_‖)
  Function.congruence abs-function {x}{y} xy with converseTotal(_≤_){𝟎}{x} | converseTotal(_≤_){𝟎}{y}
  ... | Either.Left  p | Either.Left  q = xy
  ... | Either.Left  p | Either.Right q = antisymmetry(_≤_)(_≡_) (sub₂(_≡_)(_≤_) xy 🝖 q) p 🝖 antisymmetry(_≤_)(_≡_) ([↔]-to-[→] [≤]-flip-negative q) ([↔]-to-[→] [≤]-flip-positive(p 🝖 sub₂(_≡_)(_≤_) xy))
  ... | Either.Right p | Either.Left  q = antisymmetry(_≤_)(_≡_) ([↔]-to-[→] [≤]-flip-positive(q 🝖 sub₂(_≡_)(_≤_) (symmetry(_≡_) xy))) ([↔]-to-[→] [≤]-flip-negative p) 🝖 antisymmetry(_≤_)(_≡_) q (sub₂(_≡_)(_≤_) (symmetry(_≡_) xy) 🝖 p)
  ... | Either.Right p | Either.Right q = congruence₁(−_) xy

abs-positive : ∀{x} → (‖ x ‖ ≥ 𝟎)
abs-positive{x} = if-either-bool-intro {P = _≥ 𝟎} {x = x} {y = − x} id ([↔]-to-[→] [≤]-flip-negative) (converseTotal(_≤_){𝟎}{x})

abs-values : ∀{x} → (‖ x ‖ ≡ x) ∨ (‖ x ‖ ≡ − x)
abs-values{x} with converseTotal(_≤_){𝟎}{x}
... | [∨]-introₗ _ = [∨]-introₗ (reflexivity(_≡_))
... | [∨]-introᵣ _ = [∨]-introᵣ (reflexivity(_≡_))

abs-of-zero : (‖ 𝟎 ‖ ≡ 𝟎)
abs-of-zero with abs-values{𝟎}
... | Either.Left  p = p
... | Either.Right p = p 🝖 [−]-of-𝟎

abs-when-zero : ∀{x} → (‖ x ‖ ≡ 𝟎) ↔ (x ≡ 𝟎)
abs-when-zero{x} = [↔]-intro (p ↦ congruence₁(‖_‖) p 🝖 abs-of-zero) (p ↦ symmetry(_≡_) ([∨]-elim id (q ↦ p 🝖 symmetry(_≡_) ([↔]-to-[→] [−]-is-𝟎 (symmetry(_≡_) q 🝖 p))) abs-values) 🝖 p)

abs-of-negation : ∀{x} → (‖ − x ‖ ≡ ‖ x ‖)
abs-of-negation{x} with converseTotal(_≤_){𝟎}{x} | converseTotal(_≤_){𝟎}{− x}
... | [∨]-introₗ _   | [∨]-introᵣ _   = involution(−_)
... | [∨]-introᵣ _   | [∨]-introₗ _   = reflexivity(_≡_)
... | [∨]-introₗ zx  | [∨]-introₗ znx = antisymmetry(_≤_)(_≡_) (nxz 🝖 zx) (xz 🝖 znx) where
  nxz : (− x) ≤ 𝟎
  nxz = [↔]-to-[←] [≤]-flip-negative (zx 🝖 (sub₂(_≡_)(_≤_) $ symmetry(_≡_) $ involution(−_)))

  xz : x ≤ 𝟎
  xz = [↔]-to-[←] [≤]-flip-negative znx
... | [∨]-introᵣ xz | [∨]-introᵣ nxz  = antisymmetry(_≤_)(_≡_) (involution(−_) 🝖-subₗ (xz 🝖 znx)) (nxz 🝖 zx 🝖-subᵣ symmetry(_≡_) (involution(−_))) where
  znx : 𝟎 ≤ (− x)
  znx = [↔]-to-[→] [≤]-flip-negative xz

  zx : 𝟎 ≤ x
  zx = [↔]-to-[→] [≤]-flip-negative nxz 🝖 (sub₂(_≡_)(_≤_) $ involution(−_))

instance
  abs-idempotent : Idempotent(‖_‖)
  Idempotent.proof abs-idempotent {x} with abs-values{x}
  ... | Either.Left  p = congruence₁(‖_‖) p
  ... | Either.Right p = congruence₁(‖_‖) p 🝖 abs-of-negation

abs-order : ∀{x} → ((− ‖ x ‖) ≤ ‖ x ‖)
abs-order{x} = [↔]-to-[→] [≤]-flip-positive(abs-positive{x}) 🝖 abs-positive{x}

abs-order-pos : ∀{x} → (x ≤ ‖ x ‖)
abs-order-pos {x} with converseTotal(_≤_){𝟎}{x}
... | Either.Left  p = reflexivity(_≤_)
... | Either.Right p = p 🝖 [↔]-to-[→] [≤]-flip-negative p

abs-order-neg : ∀{x} → ((− x) ≤ ‖ x ‖)
abs-order-neg {x} with converseTotal(_≤_){𝟎}{x}
... | Either.Left  p = [↔]-to-[→] [≤]-flip-positive p 🝖 p
... | Either.Right p = reflexivity(_≤_)

abs-of-positive : ∀{x} → (𝟎 ≤ x) → (‖ x ‖ ≡ x)
abs-of-positive {x} ox = antisymmetry(_≤_)(_≡_) p abs-order-pos where
  p : ‖ x ‖ ≤ x
  p with converseTotal(_≤_){𝟎}{x}
  ... | Either.Left  _ = reflexivity(_≤_)
  ... | Either.Right _ = [↔]-to-[→] [≤]-flip-positive ox 🝖 ox
  -- Alternative 1:
  -- with abs-values{x}
  -- ... | Either.Left  p = p
  -- ... | Either.Right p = [↔]-to-[←] abs-when-zero xzero 🝖 symmetry(_≡_) xzero where
  --   xzero : (x ≡ 𝟎)
  --   xzero = antisymmetry(_≤_)(_≡_) ([↔]-to-[←] [≤]-flip-negative (abs-positive{x} 🝖 sub₂(_≡_)(_≤_) p)) ox
  -- Alternative 2: antisymmetry(_≤_)(_≡_) (sub₂(_≡_)(_≤_) p 🝖 [≤]-flip-positive ox 🝖 ox) (sub₂(_≡_)(_≤_) (symmetry(_≡_) (congruence₁(−_) p 🝖 [−−]-elim)) 🝖 abs-order{x})

abs-of-negative : ∀{x} → (x ≤ 𝟎) → (‖ x ‖ ≡ − x)
abs-of-negative {x} xo = antisymmetry(_≤_)(_≡_) p abs-order-neg where
  p : ‖ x ‖ ≤ (− x)
  p with converseTotal(_≤_){𝟎}{x}
  ... | Either.Left  _ = xo 🝖 [↔]-to-[→] [≤]-flip-negative xo
  ... | Either.Right _ = reflexivity(_≤_)
  -- Alternative 1:
  -- with abs-values{x}
  -- ... | Either.Right p = p
  -- ... | Either.Left  p = symmetry(_≡_) abs-of-negation 🝖 [↔]-to-[←] abs-when-zero xzero 🝖 symmetry(_≡_) xzero where
  --   xzero : (− x ≡ 𝟎)
  --   xzero = antisymmetry(_≤_)(_≡_) ([↔]-to-[←] [≤]-flip-negative (abs-positive{x} 🝖 sub₂(_≡_)(_≤_) p 🝖 sub₂(_≡_)(_≤_) (symmetry(_≡_) [−−]-elim))) ([↔]-to-[→] [≤]-flip-negative xo)

abs-triangle-inequality : ∀{x y} → (‖ x + y ‖ ≤ (‖ x ‖ + ‖ y ‖))
abs-triangle-inequality {x}{y} with converseTotal(_≤_){𝟎}{x + y}
... | Either.Left  p =
  (x + y)         🝖[ _≤_ ]-[ [≤][+]-preserve abs-order-pos abs-order-pos ]
  (‖ x ‖ + ‖ y ‖) 🝖-end
... | Either.Right p =
  −(x + y)        🝖[ _≡_ ]-[ [+]-negation-distribution ]-sub
  (− x) + (− y)   🝖[ _≤_ ]-[ [≤][+]-preserve abs-order-neg abs-order-neg ]
  (‖ x ‖ + ‖ y ‖) 🝖-end

-- TODO: True in rings? Only division rings? Maybe ≤ instead of ≡ is better because of zero divisors
-- abs-scaling : ∀{a x} → (‖ a ⋅ x ‖ ≡ (‖ a ‖ ⋅ ‖ x ‖))
-- abs-scaling{a}{x} with converseTotal(_≤_){𝟎}{a ⋅ x} | converseTotal(_≤_){𝟎}{a} | converseTotal(_≤_){𝟎}{x}
{-... | Either.Left  p =
  (a ⋅ x)         🝖[ _≡_ ]-[ {!!} ]
  (‖ a ‖ ⋅ ‖ x ‖) 🝖-end
... | Either.Right p = {!!}
-}

-- Distance
_𝄩_ : F → F → F
x 𝄩 y = ‖ x − y ‖

open import Structure.Function.Proofs
open import Structure.Operator.Proofs.Util

instance
  [𝄩]-binaryOperator : BinaryOperator(_𝄩_)
  [𝄩]-binaryOperator = [∘₂]-function {f = ‖_‖} ⦃ oper = [−]-binaryOperator ⦄

instance
  [𝄩]-commutativity : Commutativity(_𝄩_)
  Commutativity.proof [𝄩]-commutativity {x}{y} =
    ‖ x − y ‖    🝖-[ abs-of-negation ]-sym
    ‖ −(x − y) ‖ 🝖-[ congruence₁(‖_‖) [−]-negation-distribution ]
    ‖ y − x ‖    🝖-end

[𝄩]-triangle-inequality : ∀{x y z} → ((x 𝄩 z) ≤ ((x 𝄩 y) + (y 𝄩 z)))
[𝄩]-triangle-inequality {x}{y}{z} =
  x 𝄩 z                     🝖[ _≤_ ]-[]
  ‖ x − z ‖                 🝖[ _≡_ ]-[ congruence₁(‖_‖) (congruence₂ₗ(_−_) ⦃ [−]-binaryOperator ⦄ (z) (symmetry(_≡_) (identityᵣ(_+_)(𝟎)))) ]-sub
  ‖ (x + 𝟎) − z ‖           🝖[ _≡_ ]-[ congruence₁(‖_‖) (congruence₂ₗ(_−_) ⦃ [−]-binaryOperator ⦄ (z) (congruence₂ᵣ(_+_)(x) (symmetry(_≡_) (inverseFunctionₗ(_+_)(−_))))) ]-sub
  ‖ (x + ((− y) + y)) − z ‖ 🝖[ _≡_ ]-[ congruence₁(‖_‖) ((One.associate4-213-222 {_▫_ = _+_} {a = x}{− y}{y}{− z})) ]-sub
  ‖ (x + (− y)) + (y − z) ‖ 🝖[ _≤_ ]-[]
  ‖ (x − y) + (y − z) ‖     🝖[ _≤_ ]-[ abs-triangle-inequality ]
  (‖ x − y ‖) + (‖ y − z ‖) 🝖[ _≤_ ]-[]
  (x 𝄩 y) + (y 𝄩 z)          🝖-end

[𝄩]-self : ∀{x y} → (x 𝄩 y ≡ 𝟎) ↔ (x ≡ y)
[𝄩]-self {x}{y} = [↔]-intro l r where
  l =
    (x ≡ y)            ⇒-[ symmetry(_≡_) ∘ congruence₂ᵣ(_𝄩_)(x) ]
    (x 𝄩 y ≡ x 𝄩 x)     ⇒-[]
    (_     ≡ ‖ x − x ‖) ⇒-[ _🝖 congruence₁(‖_‖) (inverseFunctionᵣ(_+_)(−_)) ]
    (_     ≡ ‖ 𝟎 ‖)     ⇒-[ _🝖 abs-of-zero ]
    (_     ≡ 𝟎)         ⇒-end
  r =
    (x 𝄩 y ≡ 𝟎) ⇒-[ [↔]-to-[→] (abs-when-zero{x − y}) ]
    (x − y ≡ 𝟎) ⇒-[ [↔]-to-[→] [−]-difference-is-𝟎 ]
    (x ≡ y)     ⇒-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Data.Product using (∃; ∃-syntax; _×_; _,_)

open import DeBruijn
open import Parallel
open import Beta

par-diamond : ∀ {n} {M N N′ : Term n}
  →         M ⇉ N → M  ⇉ N′
    -----------------------
  → ∃[ L ] (N ⇉ L × N′ ⇉ L)
par-diamond (⇉-c {x = x}) ⇉-c = # x ,  ⇉-c , ⇉-c
par-diamond (⇉-ƛ p1) (⇉-ƛ p2)
    with par-diamond p1 p2
... | L′ , p3 , p4 =
      ƛ L′ , ⇉-ƛ p3 , ⇉-ƛ p4
par-diamond (⇉-ξ p1 p3) (⇉-ξ p2 p4)
    with par-diamond p1 p2
... | L₃ , p5 , p6
      with par-diamond p3 p4
...   | M₃ , p7 , p8 =
        L₃ · M₃ , ⇉-ξ p5 p7 , ⇉-ξ p6 p8
par-diamond (⇉-ξ (⇉-ƛ p1) p3) (⇉-β p2 p4)
    with par-diamond p1 p2
... | N₃ , p5 , p6
      with par-diamond p3 p4
...   | M₃ , p7 , p8 =
        N₃ [ M₃ ] , ⇉-β p5 p7 , sub-par p6 p8
par-diamond (⇉-β p1 p3) (⇉-ξ (⇉-ƛ p2) p4)
    with par-diamond p1 p2
... | N₃ , p5 , p6
      with par-diamond p3 p4
...   | M₃ , p7 , p8 =
        N₃ [ M₃ ] , sub-par p5  p7 , ⇉-β p6 p8
par-diamond (⇉-β p1 p3) (⇉-β p2 p4)
    with par-diamond p1 p2
... | N₃ , p5 , p6
      with par-diamond p3 p4
...   | M₃ , p7 , p8 =
        N₃ [ M₃ ] , sub-par p5 p7 , sub-par p6 p8

strip : ∀ {n} {M A B : Term n}
  →         M ⇉  A → M ⇉* B
    ------------------------
  → ∃[ N ] (A ⇉* N × B ⇉  N)
strip {A = A} M⇉A (M ∎) = A , (A ∎) , M⇉A
strip {A = A} M⇉A (M ⇉⟨　M⇉M′ ⟩ M′⇉*B)
    with par-diamond M⇉A M⇉M′
... | N , A⇉N , M′⇉N
      with strip M′⇉N M′⇉*B
...   | N′ , N⇉*N′              , B⇉N′ =
        N′ , (A ⇉⟨ A⇉N ⟩ N⇉*N′) , B⇉N′

par-confluence : ∀ {n} {M A B : Term n}
  →         M ⇉* A → M ⇉* B
    ------------------------
  → ∃[ N ] (A ⇉* N × B ⇉* N)
par-confluence {B = B} (M ∎) M⇉*B = B , M⇉*B , (B ∎)
par-confluence {B = B} (M ⇉⟨ M⇉A ⟩ A⇉*A′) M⇉*B
    with strip M⇉A M⇉*B
... | N , A⇉*N , B⇉N
      with par-confluence A⇉*A′ A⇉*N
...   | N′ , A′⇉*N′ , N⇉*N′ =
        N′ , A′⇉*N′ , (B ⇉⟨ B⇉N ⟩ N⇉*N′)

confluence : ∀ {n} {M A B : Term n}
  →         M —↠ A → M —↠ B
    ------------------------
  → ∃[ N ] (A —↠ N × B —↠ N)
confluence M—↠A M—↠B
    with par-confluence (betas-pars M—↠A) (betas-pars M—↠B)
... | N , A⇉*N , B⇉*N =
      N , pars-betas A⇉*N , pars-betas B⇉*N

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


text:
------------------------------------------------------------------------------
-- Mendelson's substitution
------------------------------------------------------------------------------

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

module FOT.FOL.MendelsonSubstI where

-- First-order logic with equality.
open import Common.FOL.FOL-Eq public

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

-- Mendelson's [2015] substitution (p. 93).

--   (A7) x = y ⇒ (A(x,x) ⇒ B(x,y)) (substitutivity of equality)

-- Using pattern matching.
mendelsonSubst : (A : D → D → Set) → ∀ {x y} → x ≡ y → A x x → A x y
mendelsonSubst A refl Axx = Axx

-- From `subst` to Mendelson substitution.
subst→mendelsonSubst : (A : D → D → Set) → ∀ {x y} → x ≡ y → A x x → A x y
subst→mendelsonSubst A {x} = subst (λ z → A x z)

-- From Mendelson substitution to `subst`.
mendelsonSubst→subst : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y
mendelsonSubst→subst A = mendelsonSubst (λ _ → A)

------------------------------------------------------------------------------
-- References

-- Mendelson, Elliott (2015). Introduction to Mathematical Logic. CRC
-- Press, 6th edition.


text:
------------------------------------------------------------------------
-- Code related to the delay monad
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

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

module README where

-- The concept referred to as the delay monad here is the monad
-- presented by Capretta in "General Recursion via Coinductive Types".

------------------------------------------------------------------------
-- The delay monad

-- The delay monad, defined coinductively.

import Delay-monad

-- A type used to index a combined definition of strong and weak
-- bisimilarity and expansion.

import Delay-monad.Bisimilarity.Kind

-- A combined definition of strong and weak bisimilarity and
-- expansion, along with various properties.

import Delay-monad.Bisimilarity

-- Strong bisimilarity for partially defined values, along with a
-- proof showing that this relation is pointwise isomorphic to path
-- equality.

import Delay-monad.Bisimilarity.For-all-sizes

-- A variant of weak bisimilarity that can be used to relate the
-- number of steps in two computations.

import Delay-monad.Quantitative-weak-bisimilarity

-- Termination.

import Delay-monad.Termination

-- Alternative definitions of weak bisimilarity.

import Delay-monad.Bisimilarity.Alternative

-- An observation about weak bisimilarity.

import Delay-monad.Bisimilarity.Observation

-- Some negative results related to weak bisimilarity and expansion.

import Delay-monad.Bisimilarity.Negative

-- An example showing that transitivity-like proofs that are not
-- size-preserving can sometimes be used in a compositional way.

import Delay-monad.Bisimilarity.Transitivity-constructor

-- A partial order.

import Delay-monad.Partial-order

-- Least upper bounds.

import Delay-monad.Least-upper-bound

-- The delay monad is a monad up to strong bisimilarity.

import Delay-monad.Monad

-- The "always true" predicate, □.

import Delay-monad.Always

-- A combinator for running two (independent) computations in
-- sequence.

import Delay-monad.Sequential

-- A combinator for running two computations in parallel.

import Delay-monad.Parallel

------------------------------------------------------------------------
-- A variant of the delay monad with a sized type parameter

-- The delay monad, defined coinductively, with a sized type
-- parameter.

import Delay-monad.Sized

-- A combined definition of strong and weak bisimilarity and
-- expansion, along with various properties.

import Delay-monad.Sized.Bisimilarity

-- Strong bisimilarity for partially defined values, along with a
-- proof showing that this relation is pointwise isomorphic to path
-- equality.

import Delay-monad.Sized.Bisimilarity.For-all-sizes

-- Termination.

import Delay-monad.Sized.Termination

-- Alternative definitions of weak bisimilarity.

import Delay-monad.Sized.Bisimilarity.Alternative

-- Some negative results related to weak bisimilarity and expansion.

import Delay-monad.Sized.Bisimilarity.Negative

-- A partial order.

import Delay-monad.Sized.Partial-order

-- Least upper bounds.

import Delay-monad.Sized.Least-upper-bound

-- A monad-like structure.

import Delay-monad.Sized.Monad

-- The "always true" predicate, □.

import Delay-monad.Sized.Always

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
{-

This file contains:

- Definition of type quotients (i.e. non-truncated quotients)

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.TypeQuotients.Base where

open import Cubical.Core.Primitives

-- Type quotients as a higher inductive type:
data _/ₜ_ {ℓ ℓ'} (A : Type ℓ) (R : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
  [_] : (a : A) → A /ₜ R
  eq/ : (a b : A) → (r : R a b) → [ a ] ≡ [ b ]

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
------------------------------------------------------------------------
-- Code related to the abstract "Type Theory with Weak J" by Thorsten
-- Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders
-- Danielsson, Simon Huber and Nicolai Kraus
--
-- The code is written by Nils Anders Danielsson
------------------------------------------------------------------------

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

module README.Weak-J where

-- For the equality between the two equalities, see proof₁≡proof₂.
--
-- For the main result about contractibility of the type of pairs
-- containing J functions and the corresponding β-rule, see
-- Equality-with-J-contractible.
--
-- Note that there are minor differences between the code and the
-- presentation in the abstract.

import Equality.Instances-related

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Data.Nat
open import Data.Fin using (Fin; #_; suc; zero)
open import Data.List as List hiding (null)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All
open import Data.Integer hiding (suc)
open import Data.Product hiding (map)
open import Data.Unit
open import Data.Star hiding (return ; _>>=_ ; map)
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning
open import Data.Empty

-- This file contains the syntax for the definitional interpreter for
-- MJ using scopes and frames, described in Section 5 of the paper.

-- The definitions are parameterized by a scope graph of size `k`, as
-- usual:

module MJSF.Syntax (k : ℕ) where

private
  Scope : Set
  Scope = Fin k

-- Return types, method parameters, and field types in MJ are given by
-- `VTy`:

data VTy : Set where
  void : VTy
  int : VTy
  ref : Scope → VTy

-- The scope graph library is parameterized by a single kind of type,
-- to be used for all declarations.  But there are three different
-- kinds of names (declarations) in MJ: value declarations (e.g., for
-- fields and method parameters); method declarations; and class
-- declarations.
--
-- We use the following type to "tag" and distinguish the various
-- kinds of declarations.

data Ty : Set where
  vᵗ : VTy → Ty
  mᵗ : List VTy → VTy → Ty
  cᵗ : Scope → Scope → Ty

-- We specialize the scopes-and-frames library to the size of our
-- scope graph, and the tagged type for declarations above:

open import ScopesFrames.ScopesFrames k Ty hiding (Scope)

-------------
-- HAS TAG --
-------------

-- As summarized above, declarations may be either value-typed,
-- method-typed, or class-typed.  We introduce some parameterized
-- predicates which only hold for a particular tag.  This is useful
-- for saying that some list of types `ts : List Ty` only contains
-- value types, and that a particular property holds for each of those
-- value types.  For example, the type `All (#v (λ _ → ⊤)) ts`
-- guarantees that `ts` contains only value types, and does not
-- constrain the value types further (due to the use of `⊤`).

data #v : (VTy → Set) → Ty → Set where
  #v' : ∀ {t p} → p t → #v p (vᵗ t)

data #m : (List VTy → VTy → Set) → Ty → Set where
  #m' : ∀ {ts rt p} → p ts rt → #m p (mᵗ ts rt)

data #c (sʳ : Scope) (p : Scope → Set) : Ty → Set where
  #c' : ∀ {s} → p s → #c sʳ p (cᵗ sʳ s)

module SyntaxG (g : Graph) where

  open UsesGraph g

  -------------------------------
  -- SUBTYPING AND INHERITANCE --
  -------------------------------

  -- As summarized in the paper, we define sub-typing in terms of
  -- inheritance edges between class scopes in the scope graph:

  _<:_ : Scope → Scope → Set
  _<:_ = _⟶_

  -- Scope graphs may be cyclic, and there is (in theory) nothing that
  -- prevents classes from mutually extending one another, thereby
  -- creating cyclic inheritance chains.  The following `Inherits`
  -- type witnesses that a given class scope has a finite set of
  -- inheritance steps.  This property is useful for defining object
  -- initialization in a way that lets Agda prove that object
  -- initialization takes finite time (i.e., no need for fuel).

  data Inherits : Scope → Scope → Set where
    obj   : ∀ s {ds sʳ} ⦃ shape : g s ≡ (ds , [ sʳ ]) ⦄ → Inherits s s
    super : ∀ {s ds sʳ sᵖ s'} ⦃ shape : g s ≡ (ds , sʳ ∷ sᵖ ∷ []) ⦄ → Inherits sᵖ s' → Inherits s s'

  ------------
  -- SYNTAX --
  ------------

  -- The expressions of MJ where the `s` in `Expr s t` is the lexical
  -- context scope:

  data Expr (s : Scope) : VTy → Set where
    call     :  ∀ {s' ts t} → Expr s (ref s') → -- receiver
                (s' ↦ (mᵗ ts t)) →              -- path to method declaration
                All (Expr s) ts →               -- argument list
                Expr s t
    get      :  ∀ {s' t} → Expr s (ref s') → (s' ↦ vᵗ t) → Expr s t
    var      :  ∀ {t} → (s ↦ vᵗ t) → Expr s t
    new      :  ∀ {sʳ s'} → s ↦ cᵗ sʳ s' → Expr s (ref s') -- path to class declaration
    null     :  ∀ {s'} → Expr s (ref s')
    num      :  ℤ → Expr s int
    iop      :  (ℤ → ℤ → ℤ) → (l r : Expr s int) → Expr s int
    upcast   :  ∀ {t' t} → t' <: t → Expr s (ref t') → Expr s (ref t)
    this     :  ∀ {s' self} → s ⟶ s' → self ∈ edgesOf s' → -- the `self` of objects is given by the lexical parent edge of a method
                Expr s (ref self)

  -- The statements of MJ where the `s` in `Stmt s t s'` is the
  -- lexical context scope before the statement `t` is the return type
  -- of the statement, and `s'` is the leixcal context scope after the
  -- statement.

  mutual
    data Stmt (s : Scope)(r : VTy) : Scope → Set where
      run   : ∀ {t'} → Expr s t' → Stmt s r s
      ifz   : ∀ {s' s'' : Scope} → Expr s int → Stmt s r s → Stmt s r s → Stmt s r s -- branches are blocks
      set   : ∀ {s' t'} → Expr s (ref s') → (s' ↦ vᵗ t') → Expr s t' → Stmt s r s
      loc   : ∀ (s' : Scope)(t' : VTy)⦃ shape : g s' ≡ ([ vᵗ t' ] , [ s ]) ⦄ → Stmt s r s' -- local variable scope `s'` is connected to lexical context scope `s`
      asgn  : ∀ {t'} → (s ↦ vᵗ t') → Expr s t' → Stmt s r s
      ret   : Expr s r → Stmt s r s
      block : ∀ {s'} → Stmts s r s' → Stmt s r s

    -- A block of statements is given by a sequence of statements
    -- whose scopes are lexically nested (if at all):

    Stmts : Scope → VTy → Scope → Set
    Stmts s r s' = Star (λ s s' → Stmt s r s') s s'

  -- Method bodies have a mandatory return expression, except for
  -- `void` typed method bodies:

  data Body (s : Scope) : VTy → Set where
    body      : ∀ {s' t} → Stmts s t s' → Expr s' t → Body s t
    body-void : ∀ {s'} → Stmts s void s' → Body s void

  -- A method defines the scope shape mandating that the method type
  -- parameters are declarations of the method body scope, and that
  -- the method body scope is connected to the scope of the class
  -- where they are defined.  The `s` in `Meth s ts t` is the scope of
  -- the surrounding class.

  data Meth (s : Scope) : List VTy → VTy → Set where
    meth  :  ∀ {ts rt}(s' : Scope)
             ⦃ shape : g s' ≡ (List.map vᵗ ts , [ s ]) ⦄ →
             Body s' rt →
             Meth s ts rt

  -- A class definition has an optional path to a super class; the
  -- only difference between a `class0` and a `class1` is that a
  -- `class1` has a path from the root scope `sʳ` to another class
  -- declaration, i.e., the super class.
  --
  -- The `sʳ` in `Class sʳ s` is the root scope (representing the
  -- class table), and the `s` is the scope of the defined class.
  --
  -- We distinguish three kinds of class members in MJ:
  --
  -- * Fields, typed by `fs`.
  --
  -- * Methods, typed by `ms`, where for each method type signature
  --   `mᵗ ts t` in `ms` there is a well-typed method `Meth s ts t`.
  --
  -- * Overriding methods, typed by `oms`, where for each method type
  --   signature `mᵗ ts t` in `oms` there is a path from the current
  --   class scope to a method declaration in a parent class scope,
  --   and a well-typed method `Meth s ts t` which overrides the
  --   method corresponding to that declaration.

  data Class (sʳ s : Scope) : Set where
    class1  :  ∀ {ms fs oms sᵖ} →
               sʳ ↦ (cᵗ sʳ sᵖ) →
               ⦃ shape  :  g s  ≡  (ms ++ fs ,  sʳ ∷ sᵖ ∷ []) ⦄ →
               All (#m (Meth s)) ms →
               All (#v (λ _ → ⊤)) fs →
               All (#m (λ ts rt → (s ↦ (mᵗ ts rt)) × Meth s ts rt )) oms → -- overrides
               Class sʳ s
    class0 : ∀ {ms fs oms} →
             ⦃ shape : g s ≡ (ms ++ fs , [ sʳ ]) ⦄ →
             All (#m (Meth s)) ms →   -- only methods
             All (#v (λ _ → ⊤)) fs →  -- only values
             All (#m (λ ts rt → (s ↦ (mᵗ ts rt)) × Meth s ts rt )) oms → -- overrides
             Class sʳ s

  -- A program consists of a sequence of well-typed class definitions
  -- and a main function to be evaluated in the context of the root
  -- scope.  The root scope has only class-typed declarations, and has
  -- no parent edges:

  data Program (sʳ : Scope)(a : VTy) : Set where
    program :
      ∀ cs ⦃ shape : g sʳ ≡ (cs , []) ⦄ →
        -- implementation of all the classes
        All (#c sʳ (λ s → Class sʳ s × ∃ λ s' → Inherits s s')) cs →
        -- main function
        Body sʳ a →
        Program sʳ a


text:
module Misc.PosBinary where  -- Positive Binary Numbers

open import Data.Nat
open import Data.List
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym)

open import Induction.WellFounded
open import Induction.Nat using (<-well-founded)

data Bin+ : Set where
  [] : Bin+
  1∷_ : Bin+ → Bin+
  2∷_ : Bin+ → Bin+

decimal : Bin+ → ℕ
decimal [] = 0
decimal (1∷ xs) = 1 + 2 * decimal xs
decimal (2∷ xs) = 2 + 2 * decimal xs

-- A even/odd view. Surprised that we don't have it in StdLib

data Div2 : ℕ → Set where
  even : ∀ n → Div2 (2 * n)
  odd  : ∀ n → Div2 (1 + 2 * n)

open import Data.Nat.Properties.Simple using (+-suc)
  -- +-suc : ∀ m n → m + suc n ≡ suc (m + n)
open import Data.Nat.Properties using (m≤′m+n)
  -- m≤′m+n : ∀ m n → m ≤′ m + n

_div2 : ∀ n → Div2 n
zero div2 = even 0
suc n div2 with n div2
suc .(n + (n + 0)) div2       | even n = odd n
suc .(suc (n + (n + 0))) div2 | odd n
      rewrite sym (+-suc n (n + zero)) = even (1 + n)

bin+' : (n : ℕ) → Acc _<′_ n → Bin+
bin+' n _ with n div2
bin+' .0 _                              | even zero = []
bin+' .(suc (m + suc (m + 0))) (acc rs) | even (suc m) =
   2∷ bin+' m (rs m (m≤′m+n (suc m) _))
bin+' .(suc (m + (m + 0)))     (acc rs) | odd m  =
   1∷ bin+' m (rs m (m≤′m+n (suc m) _))

bin+ : ℕ → Bin+
bin+ n = bin+' n (<-well-founded n)

{-  For reference.

bin' : (n : ℕ) → Acc _<′_ n → List ℕ
bin' n _ with n div2
bin' .0 (acc rs) | even 0 = []
bin' .(suc m + (suc m + 0)) (acc rs) | even (suc m) =
     0 ∷ bin' m (rs m (m≤′m+n (suc m) _))
bin' .(suc (m + (m + 0))) (acc rs)   | odd m =
     1 ∷ bin' m (rs m (m≤′m+n (suc m) _))

bin : ℕ → List ℕ
bin n = bin' n (<-well-founded n)
-}

lInv' : ∀ n → (ac : Acc _<′_ n) → decimal (bin+' n ac) ≡ n
lInv' n ac with n div2
lInv' .0 ac | even zero = refl
lInv' .(suc (m + suc (m + 0))) (acc rs) | even (suc m)
  rewrite lInv' m (rs m (m≤′m+n (suc m) (suc (m + zero))))
        | +-suc m (m + 0) = refl
lInv' .(suc (m + (m + 0))) (acc rs) | odd m
  rewrite lInv' m (rs m (m≤′m+n (suc m) (m + zero))) = refl

lInv : ∀ n → decimal (bin+ n) ≡ n
lInv n = lInv' n (<-well-founded n)

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module Tactic.Nat.Simpl where

open import Prelude hiding (abs)
open import Builtin.Reflection
open import Tactic.Reflection.Quote
open import Tactic.Reflection

open import Tactic.Nat.Reflect
open import Tactic.Nat.NF
open import Tactic.Nat.Exp
open import Tactic.Nat.Auto
open import Tactic.Nat.Auto.Lemmas
open import Tactic.Nat.Simpl.Lemmas

module _ {Atom : Set} {{_ : Eq Atom}} {{_ : Ord Atom}} where
  ExpEq : Exp Atom × Exp Atom → Env Atom → Set
  ExpEq (e₁ , e₂) ρ = ⟦ e₁ ⟧e ρ ≡ ⟦ e₂ ⟧e ρ

  CancelEq : Exp Atom × Exp Atom → Env Atom → Set
  CancelEq (e₁ , e₂) ρ = NFEqS (cancel (norm e₁) (norm e₂)) ρ

  ⟦_⟧h : List (Exp Atom × Exp Atom) → Env Atom → Set
  ⟦ [] ⟧h ρ = ⊥
  ⟦ h ∷ [] ⟧h ρ = ExpEq h ρ
  ⟦ h ∷ g  ⟧h ρ = ExpEq h ρ → ⟦ g ⟧h ρ

  ⟦_⟧hs : List (Exp Atom × Exp Atom) → Env Atom → Set
  ⟦ [] ⟧hs ρ = ⊥
  ⟦ h ∷ [] ⟧hs ρ = CancelEq h ρ
  ⟦ h ∷ g  ⟧hs ρ = CancelEq h ρ → ⟦ g ⟧hs ρ

  simplifyEq : ∀ eq (ρ : Env Atom) → CancelEq eq ρ → ExpEq eq ρ
  simplifyEq (e₁ , e₂) ρ H = liftNFEq e₁ e₂ ρ (cancel-sound (norm e₁) (norm e₂) ρ H)

  complicateEq : ∀ eq ρ → ExpEq eq ρ → CancelEq eq ρ
  complicateEq (e₁ , e₂) ρ H =
    cancel-complete (norm e₁) (norm e₂) ρ
    (unliftNFEq e₁ e₂ ρ H)

  simplifyH : ∀ goal ρ → ⟦ goal ⟧hs ρ → ⟦ goal ⟧h ρ
  simplifyH []            ρ ()
  simplifyH (h ∷ [])     ρ H = simplifyEq h ρ H
  simplifyH (h ∷ h₂ ∷ g) ρ H = λ H₁ → simplifyH (h₂ ∷ g) ρ $ H (complicateEq h ρ H₁)

simplify-tactic : {x y : Nat} → x ≡ y → Type → TC Term
simplify-tactic {x} {y} prf g = do
  `x   ← quoteTC x
  `y   ← quoteTC y
  `prf ← quoteTC prf
  let h = def₂ (quote _≡_) `x `y
      t = pi (vArg h) (abs "_" (weaken 1 g))
  just (goal , Γ) ← termToHyps t
    where nothing → typeError (strErr "Invalid goal" ∷ termErr t ∷ [])
  pure $ def (quote flip)
             $ vArg (def (quote simplifyH)
                    ( vArg (` goal)
                    ∷ vArg (quotedEnv Γ) ∷ [] ))
             ∷ vArg `prf ∷ []

assumed-tactic : {x y : Nat} → x ≡ y → Type → TC Term
assumed-tactic {x} {y} prf g = do
  `x   ← withNormalisation true $ quoteTC x
  `y   ← withNormalisation true $ quoteTC y
  `prf ← quoteTC prf
  let h = def (quote _≡_) (hArg unknown ∷ hArg (def₀ (quote Nat)) ∷ vArg `x ∷ vArg `y ∷ [])
  let t = pi (vArg h) (abs "_" (weaken 1 g))
  just (goal , Γ) ← termToHyps t
    where nothing → typeError (strErr "Invalid goal" ∷ termErr t ∷ [])
  pure $
    def (quote simplifyH) ( vArg (` goal)
                          ∷ vArg (quotedEnv Γ)
                          ∷ vArg (def (quote id) [])
                          ∷ vArg `prf ∷ [] )

macro
  follows-from : {x y : Nat} → x ≡ y → Tactic
  follows-from prf hole = do
    goal ← inferNormalisedType hole
    unify hole =<< assumed-tactic prf goal

  simplify : {x y : Nat} → x ≡ y → Tactic
  simplify prf hole = do
    goal ← inferNormalisedType hole
    unify hole =<< simplify-tactic prf goal

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Celeste where

open import Data.Nat using (ℕ; _⊔_; zero)
open import Data.String using (String)
open import Data.Vec using (Vec)
open import Data.Unsigned using (Unsigned)
open import Data.Signed using (Signed)
open import Data.Float using (Float)

private
  variable
    word-size : ℕ

mutual
  data Type : ℕ → Set where
    string : Type zero
    int8 : Type zero
    uint8 : Type zero
    int16 : Type zero
    uint16 : Type zero
    int32 : Type zero
    uint32 : Type zero
    int64 : Type zero
    uint64 : Type zero
    int128 : Type zero
    uint128 : Type zero
    int-word : Type zero
    uint-word : Type zero
    float32 : Type zero
    float64 : Type zero
    _×_ : {m n : ℕ} → Type m → Type n → Type (m ⊔ n)
    _⟶_ : {m n : ℕ} → Type m → Type n → Type (m ⊔ n)

  data Expr : {n : ℕ} → Type n → Set where
    str-lit : String → Expr string
    int8-lit : Signed 8 → Expr int8
    uint8-lit : Unsigned 8 → Expr uint8
    int16-lit : Signed 16 → Expr int16
    uint16-lit : Unsigned 16 → Expr uint16
    int32-lit : Signed 32 → Expr int32
    uint32-lit : Unsigned 32 → Expr uint32
    int64-lit : Signed 64 → Expr int64
    uint64-lit : Unsigned 64 → Expr uint64
    int128-lit : Signed 128 → Expr int128
    uint128-lit : Unsigned 128 → Expr uint128
    int-word-lit : Signed word-size → Expr int-word
    uint-word-lit : Unsigned word-size → Expr uint-word
    float32-lit : Float → Expr float32
    float64-lit : Float → Expr float64

max_stars_repo_name: brunoczim/Celeste

max_issues_repo_name: brunoczim/Celeste

max_forks_repo_name: brunoczim/Celeste


text:
------------------------------------------------------------------------
-- The parser equivalence proof language is sound
------------------------------------------------------------------------

module TotalParserCombinators.Congruence.Sound where

open import Category.Monad
open import Codata.Musical.Notation
open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
import Data.List.Categorical as ListMonad
open import Data.List.Relation.Binary.BagAndSetEquality
  renaming (_∼[_]_ to _List-∼[_]_)
open import Data.Maybe hiding (_>>=_)
open import Data.Product
open import Function
import Function.Related as Related
open import Level
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

open Related using (SK-sym)
open Related.EquationalReasoning
  renaming (_∼⟨_⟩_ to _∼⟨_⟩′_; _∎ to _∎′)
open RawMonad {f = zero} ListMonad.monad
  using () renaming (_⊛_ to _⊛′_; _>>=_ to _>>=′_)
private
  module BSOrd {k} {A : Set} = Preorder ([ k ]-Order A)

open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.CoinductiveEquality as CE
  using (_∼[_]c_; _∷_)
open import TotalParserCombinators.Congruence
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Lib using (return⋆)
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics using (_∼[_]_)

------------------------------------------------------------------------
-- Some lemmas

private

  ⊛flatten-lemma : ∀ {k} {R₁ R₂ : Set} {fs₁ fs₂ : List (R₁ → R₂)}
                   (xs₁ xs₂ : Maybe (List R₁)) →
                   fs₁ List-∼[ k ] fs₂ →
                   flatten xs₁ List-∼[ k ] flatten xs₂ →
                   fs₁ ⊛flatten xs₁ List-∼[ k ] fs₂ ⊛flatten xs₂
  ⊛flatten-lemma {k} {fs₁ = fs₁} {fs₂} xs₁ xs₂ fs₁≈fs₂ = helper xs₁ xs₂
    where
    helper : ∀ xs₁ xs₂ →
             flatten xs₁ List-∼[ k ] flatten xs₂ →
             fs₁ ⊛flatten xs₁ List-∼[ k ] fs₂ ⊛flatten xs₂
    helper nothing    nothing     []∼[]      = BSOrd.refl
    helper (just xs₁) (just xs₂) xs₁≈xs₂     = ⊛-cong fs₁≈fs₂ xs₁≈xs₂
    helper nothing    (just xs₂)  []≈xs₂ {x} =
      x ∈ []            ↔⟨ BSOrd.reflexive $ P.sym $
                             ListMonad.Applicative.right-zero fs₂ ⟩
      x ∈ (fs₂ ⊛′ [])   ∼⟨ ⊛-cong (BSOrd.refl {x = fs₂}) []≈xs₂ ⟩′
      x ∈ (fs₂ ⊛′ xs₂)  ∎′
    helper (just xs₁) nothing    xs₁∼[]  {x} =
      x ∈ (fs₁ ⊛′ xs₁)  ∼⟨ ⊛-cong (BSOrd.refl {x = fs₁}) xs₁∼[] ⟩′
      x ∈ (fs₁ ⊛′ [])   ↔⟨ BSOrd.reflexive $
                             ListMonad.Applicative.right-zero fs₁ ⟩
      x ∈ []            ∎′

  []-⊛flatten : ∀ {A B : Set} (xs : Maybe (List A)) →
                [] ⊛flatten xs List-∼[ bag ] [] {A = B}
  []-⊛flatten nothing   = BSOrd.refl
  []-⊛flatten (just xs) = BSOrd.refl

  bind-lemma : ∀ {k} {R₁ R₂ : Set} {xs₁ xs₂ : Maybe (List R₁)}
               (f₁ f₂ : Maybe (R₁ → List R₂)) →
               flatten xs₁ List-∼[ k ] flatten xs₂ →
               (∀ x → apply f₁ x List-∼[ k ] apply f₂ x) →
               bind xs₁ f₁ List-∼[ k ] bind xs₂ f₂
  bind-lemma {k} {xs₁ = xs₁} {xs₂} f₁ f₂ xs₁≈xs₂ = helper f₁ f₂
    where
    helper : ∀ f₁ f₂ →
             (∀ x → apply f₁ x List-∼[ k ] apply f₂ x) →
             bind xs₁ f₁ List-∼[ k ] bind xs₂ f₂
    helper nothing   nothing   []∼[]     = BSOrd.refl
    helper (just f₁) (just f₂) f₁≈f₂     = >>=-cong xs₁≈xs₂ f₁≈f₂
    helper nothing   (just f₂) []≈f₂ {x} =
      x ∈ []                           ∼⟨ BSOrd.reflexive $ P.sym $
                                             ListMonad.MonadProperties.right-zero (flatten xs₂) ⟩′
      x ∈ (flatten xs₂ >>=′ λ _ → [])  ∼⟨ >>=-cong (BSOrd.refl {x = flatten xs₂}) []≈f₂ ⟩′
      x ∈ (flatten xs₂ >>=′ f₂)        ∎′
    helper (just f₁) nothing   f₁∼[] {x} =
      x ∈ (flatten xs₁ >>=′ f₁)        ∼⟨ >>=-cong (BSOrd.refl {x = flatten xs₁}) f₁∼[] ⟩′
      x ∈ (flatten xs₁ >>=′ λ _ → [])  ∼⟨ BSOrd.reflexive $
                                            ListMonad.MonadProperties.right-zero (flatten xs₁) ⟩′
      x ∈ []                           ∎′

  bind-nothing : ∀ {A B : Set} (f : Maybe (A → List B)) →
                 bind nothing f List-∼[ bag ] []
  bind-nothing nothing  = BSOrd.refl
  bind-nothing (just f) = BSOrd.refl

------------------------------------------------------------------------
-- Equality is closed under initial-bag

initial-bag-cong :
  ∀ {k Tok R xs₁ xs₂} {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
  p₁ ∼[ k ]P p₂ → initial-bag p₁ List-∼[ k ] initial-bag p₂
initial-bag-cong (xs₁≈xs₂ ∷ Dp₁≈Dp₂)   = xs₁≈xs₂
initial-bag-cong (p ∎)                 = BSOrd.refl
initial-bag-cong (p₁ ∼⟨ p₁≈p₂ ⟩ p₂≈p₃) = _ ∼⟨ initial-bag-cong p₁≈p₂ ⟩′ initial-bag-cong p₂≈p₃
initial-bag-cong (p₁ ≅⟨ p₁≅p₂ ⟩ p₂≈p₃) = _ ↔⟨ initial-bag-cong p₁≅p₂ ⟩  initial-bag-cong p₂≈p₃
initial-bag-cong (sym p₁≈p₂)           = SK-sym (initial-bag-cong p₁≈p₂)
initial-bag-cong (return x₁≡x₂)        = BSOrd.reflexive $ P.cong [_] x₁≡x₂
initial-bag-cong fail                  = BSOrd.refl
initial-bag-cong token                 = BSOrd.refl
initial-bag-cong (p₁≈p₃ ∣ p₂≈p₄)       = ++-cong (initial-bag-cong p₁≈p₃) (initial-bag-cong p₂≈p₄)
initial-bag-cong (f₁≗f₂ <$> p₁≈p₂)     = map-cong f₁≗f₂ $ initial-bag-cong p₁≈p₂
initial-bag-cong (nonempty p₁≈p₂)      = BSOrd.refl

initial-bag-cong (cast {xs₁  = xs₁}  {xs₂  = xs₂}
                       {xs₁′ = xs₁′} {xs₂′ = xs₂′}
                       {xs₁≈xs₁′ = xs₁≈xs₁′} {xs₂≈xs₂′ = xs₂≈xs₂′}
                       p₁≈p₂) {x} =
  x ∈ xs₁′  ↔⟨ SK-sym xs₁≈xs₁′ ⟩
  x ∈ xs₁   ∼⟨ initial-bag-cong p₁≈p₂ ⟩′
  x ∈ xs₂   ↔⟨ xs₂≈xs₂′ ⟩
  x ∈ xs₂′  ∎′

initial-bag-cong ([ nothing          - _       ] p₁≈p₃ ⊛ p₂≈p₄)     = BSOrd.refl
initial-bag-cong ([ just (xs₁ , xs₂) - just _  ] p₁≈p₃ ⊛ p₂≈p₄)     = ⊛flatten-lemma xs₁ xs₂
                                                                        (initial-bag-cong p₁≈p₃) (initial-bag-cong p₂≈p₄)
initial-bag-cong ([ just (xs₁ , xs₂) - nothing ] p₁≈p₃ ⊛ p₂≈p₄) {x} =
  x ∈ [] ⊛flatten xs₁  ↔⟨ []-⊛flatten xs₁ ⟩
  x ∈ []               ↔⟨ SK-sym $ []-⊛flatten xs₂ ⟩
  x ∈ [] ⊛flatten xs₂  ∎′

initial-bag-cong ([ nothing        - _       ] p₁≈p₃ >>= p₂≈p₄)     = BSOrd.refl
initial-bag-cong ([ just (f₁ , f₂) - just _  ] p₁≈p₃ >>= p₂≈p₄)     = bind-lemma f₁ f₂
                                                                        (initial-bag-cong p₁≈p₃) (λ x → initial-bag-cong (p₂≈p₄ x))
initial-bag-cong ([ just (f₁ , f₂) - nothing ] p₁≈p₃ >>= p₂≈p₄) {x} =
  x ∈ bind nothing f₁  ↔⟨ bind-nothing f₁ ⟩
  x ∈ []               ↔⟨ SK-sym $ bind-nothing f₂ ⟩
  x ∈ bind nothing f₂  ∎′

------------------------------------------------------------------------
-- Equality is closed under D

D-cong : ∀ {k Tok R xs₁ xs₂}
           {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
         p₁ ∼[ k ]P p₂ → ∀ {t} → D t p₁ ∼[ k ]P D t p₂
D-cong (xs₁≈xs₂ ∷ Dp₁≈Dp₂)   {t} = ♭ (Dp₁≈Dp₂ t)
D-cong (p ∎)                 {t} = D t p ∎
D-cong (p₁ ∼⟨ p₁≈p₂ ⟩ p₂≈p₃) {t} = D t p₁ ∼⟨ D-cong p₁≈p₂ ⟩ D-cong p₂≈p₃
D-cong (p₁ ≅⟨ p₁≅p₂ ⟩ p₂≈p₃) {t} = D t p₁ ≅⟨ D-cong p₁≅p₂ ⟩ D-cong p₂≈p₃
D-cong (sym p₁≈p₂)               = _∼[_]P_.sym (D-cong p₁≈p₂)
D-cong (return x₁≡x₂)            = fail ∎
D-cong fail                      = fail ∎
D-cong token                 {t} = return t ∎
D-cong (p₁≈p₃ ∣ p₂≈p₄)           = D-cong p₁≈p₃ ∣ D-cong p₂≈p₄
D-cong (f₁≗f₂ <$> p₁≈p₂)         = f₁≗f₂ <$> D-cong p₁≈p₂
D-cong (nonempty p₁≈p₂)          = D-cong p₁≈p₂
D-cong (cast p₁≈p₂)              = D-cong p₁≈p₂

D-cong ([_-_]_⊛_ nothing nothing {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ ⊛ p₂)  ∼⟨ [ nothing - just (○ , ○) ] ♯ D-cong (♭ p₁≈p₃) ⊛ ♭ p₂≈p₄ ⟩
  D t (p₃ ⊛ p₄)  ∎
D-cong ([_-_]_⊛_ nothing (just (fs₁ , fs₂)) {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ ⊛ p₂)                                               ≅⟨ D.D-⊛ p₁ p₂ ⟩
    D t (♭ p₁) ⊛ ♭? p₂ ∣ return⋆ (flatten fs₁) ⊛ D t (♭? p₂)  ≅⟨ [ ○ - ◌ - ○ - ○ ] D t (♭ p₁) ∎ ⊛ (♭? p₂ ∎) ∣ (_ ∎) ⟩
  ♯ D t (♭ p₁) ⊛ ♭? p₂ ∣ return⋆ (flatten fs₁) ⊛ D t (♭? p₂)  ∼⟨ [ nothing - just (○ , ○) ] ♯ D-cong (♭ p₁≈p₃) ⊛ p₂≈p₄ ∣
                                                                 [ just (○ , ○) - just (○ , ○) ]
                                                                   Return⋆.cong (initial-bag-cong (♭ p₁≈p₃)) ⊛ D-cong p₂≈p₄ ⟩
  ♯ D t (♭ p₃) ⊛ ♭? p₄ ∣ return⋆ (flatten fs₂) ⊛ D t (♭? p₄)  ≅⟨ [ ◌ - ○ - ○ - ○ ] D t (♭ p₃) ∎ ⊛ (♭? p₄ ∎) ∣ (_ ∎) ⟩
    D t (♭ p₃) ⊛ ♭? p₄ ∣ return⋆ (flatten fs₂) ⊛ D t (♭? p₄)  ≅⟨ _∼[_]P_.sym $ D.D-⊛ p₃ p₄ ⟩
  D t (p₃ ⊛ p₄)                                               ∎
D-cong ([_-_]_⊛_ (just _) nothing {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ ⊛ p₂)                                   ≅⟨ D.D-⊛ p₁ p₂ ⟩
  D t (♭? p₁) ⊛ ♭ p₂ ∣ return⋆ [] ⊛   D t (♭ p₂)  ≅⟨ (D t (♭? p₁) ⊛ ♭ p₂ ∎) ∣
                                                     [ ○ - ○ - ○ - ◌ ] return⋆ [] ∎ ⊛ (D t (♭ p₂) ∎) ⟩
  D t (♭? p₁) ⊛ ♭ p₂ ∣ return⋆ [] ⊛ ♯ D t (♭ p₂)  ∼⟨ [ just (○ , ○) - just (○ , ○) ] D-cong p₁≈p₃ ⊛ ♭ p₂≈p₄ ∣
                                                     [ just (○ , ○) - nothing ] (return⋆ [] ∎) ⊛ ♯ D-cong (♭ p₂≈p₄) ⟩
  D t (♭? p₃) ⊛ ♭ p₄ ∣ return⋆ [] ⊛ ♯ D t (♭ p₄)  ≅⟨ (D t (♭? p₃) ⊛ ♭ p₄ ∎) ∣
                                                     [ ○ - ○ - ◌ - ○ ] return⋆ [] ∎ ⊛ (D t (♭ p₄) ∎) ⟩
  D t (♭? p₃) ⊛ ♭ p₄ ∣ return⋆ [] ⊛   D t (♭ p₄)  ≅⟨ _∼[_]P_.sym $ D.D-⊛ p₃ p₄ ⟩
  D t (p₃ ⊛ p₄)                                   ∎
D-cong ([_-_]_⊛_ (just _) (just (fs₁ , fs₂)) {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ ⊛ p₂)                                              ≅⟨ D.D-⊛ p₁ p₂ ⟩
  D t (♭? p₁) ⊛ ♭? p₂ ∣ return⋆ (flatten fs₁) ⊛ D t (♭? p₂)  ∼⟨ [ just (○ , ○) - just (○ , ○) ] D-cong p₁≈p₃ ⊛ p₂≈p₄ ∣
                                                                [ just (○ , ○) - just (○ , ○) ] Return⋆.cong (initial-bag-cong p₁≈p₃) ⊛
                                                                                D-cong p₂≈p₄ ⟩
  D t (♭? p₃) ⊛ ♭? p₄ ∣ return⋆ (flatten fs₂) ⊛ D t (♭? p₄)  ≅⟨ _∼[_]P_.sym $ D.D-⊛ p₃ p₄ ⟩
  D t (p₃ ⊛ p₄)                                              ∎

D-cong ([_-_]_>>=_ nothing nothing {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ >>= p₂)  ∼⟨ [ nothing - just (○ , ○) ] ♯ D-cong (♭ p₁≈p₃) >>= (♭ ∘ p₂≈p₄) ⟩
  D t (p₃ >>= p₄)  ∎
D-cong ([_-_]_>>=_ nothing (just (xs₁ , xs₂)) {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ >>= p₂)                                                         ≅⟨ D.D->>= p₁ p₂ ⟩
    D t (♭ p₁) >>= (♭? ∘ p₂) ∣ return⋆ (flatten xs₁) >>= (D t ∘ ♭? ∘ p₂)  ≅⟨ [ ○ - ◌ - ○ - ○ ] D t (♭ p₁) ∎ >>= (λ x → ♭? (p₂ x) ∎) ∣
                                                                             (_ ∎) ⟩
  ♯ D t (♭ p₁) >>= (♭? ∘ p₂) ∣ return⋆ (flatten xs₁) >>= (D t ∘ ♭? ∘ p₂)  ∼⟨ [ nothing - just (○ , ○) ] ♯ D-cong (♭ p₁≈p₃) >>= p₂≈p₄ ∣
                                                                             [ just (○ , ○) - just (○ , ○) ]
                                                                               Return⋆.cong (initial-bag-cong (♭ p₁≈p₃)) >>=
                                                                               (λ x → D-cong (p₂≈p₄ x)) ⟩
  ♯ D t (♭ p₃) >>= (♭? ∘ p₄) ∣ return⋆ (flatten xs₂) >>= (D t ∘ ♭? ∘ p₄)  ≅⟨ [ ◌ - ○ - ○ - ○ ] D t (♭ p₃) ∎ >>= (λ x → ♭? (p₄ x) ∎) ∣
                                                                             (_ ∎) ⟩
    D t (♭ p₃) >>= (♭? ∘ p₄) ∣ return⋆ (flatten xs₂) >>= (D t ∘ ♭? ∘ p₄)  ≅⟨ _∼[_]P_.sym $ D.D->>= p₃ p₄ ⟩
  D t (p₃ >>= p₄)                                                         ∎
D-cong ([_-_]_>>=_ (just _) nothing {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ >>= p₂)                                                     ≅⟨ D.D->>= p₁ p₂ ⟩
  D t (♭? p₁) >>= (♭ ∘ p₂) ∣ return⋆ [] >>= (D t ∘ ♭ ∘ p₂)            ≅⟨ (D t (♭? p₁) >>= (♭ ∘ p₂) ∎) ∣
                                                                         [ ○ - ○ - ○ - ◌ ] return⋆ [] ∎ >>= (λ x → D t (♭ (p₂ x)) ∎) ⟩
  D t (♭? p₁) >>= (♭ ∘ p₂) ∣ return⋆ [] >>= (λ x → ♯ D t (♭ (p₂ x)))  ∼⟨ [ just (○ , ○) - just (○ , ○) ] D-cong p₁≈p₃ >>= (♭ ∘ p₂≈p₄) ∣
                                                                         [ just (○ , ○) - nothing ] (return⋆ [] ∎) >>=
                                                                                (λ x → ♯ D-cong (♭ (p₂≈p₄ x))) ⟩
  D t (♭? p₃) >>= (♭ ∘ p₄) ∣ return⋆ [] >>= (λ x → ♯ D t (♭ (p₄ x)))  ≅⟨ (D t (♭? p₃) >>= (♭ ∘ p₄) ∎) ∣
                                                                         [ ○ - ○ - ◌ - ○ ] return⋆ [] ∎ >>= (λ x → D t (♭ (p₄ x)) ∎) ⟩
  D t (♭? p₃) >>= (♭ ∘ p₄) ∣ return⋆ [] >>= (D t ∘ ♭ ∘ p₄)            ≅⟨ _∼[_]P_.sym $ D.D->>= p₃ p₄ ⟩
  D t (p₃ >>= p₄)                                                     ∎
D-cong ([_-_]_>>=_ (just _) (just (xs₁ , xs₂)) {p₁} {p₂} {p₃} {p₄} p₁≈p₃ p₂≈p₄) {t} =
  D t (p₁ >>= p₂)                                                        ≅⟨ D.D->>= p₁ p₂ ⟩
  D t (♭? p₁) >>= (♭? ∘ p₂) ∣ return⋆ (flatten xs₁) >>= (D t ∘ ♭? ∘ p₂)  ∼⟨ [ just (○ , ○) - just (○ , ○) ] D-cong p₁≈p₃ >>= p₂≈p₄ ∣
                                                                            [ just (○ , ○) - just (○ , ○) ]
                                                                              Return⋆.cong (initial-bag-cong p₁≈p₃) >>=
                                                                              (λ x → D-cong (p₂≈p₄ x)) ⟩
  D t (♭? p₃) >>= (♭? ∘ p₄) ∣ return⋆ (flatten xs₂) >>= (D t ∘ ♭? ∘ p₄)  ≅⟨ _∼[_]P_.sym $ D.D->>= p₃ p₄ ⟩
  D t (p₃ >>= p₄)                                                        ∎

------------------------------------------------------------------------
-- Soundness

sound : ∀ {k Tok R xs₁ xs₂}
          {p₁ : Parser Tok R xs₁}
          {p₂ : Parser Tok R xs₂} →
        p₁ ∼[ k ]P p₂ → p₁ ∼[ k ] p₂
sound = CE.sound ∘ sound′
  where
  sound′ : ∀ {k Tok R xs₁ xs₂}
             {p₁ : Parser Tok R xs₁}
             {p₂ : Parser Tok R xs₂} →
           p₁ ∼[ k ]P p₂ → p₁ ∼[ k ]c p₂
  sound′ p₁≈p₂ = initial-bag-cong p₁≈p₂ ∷ λ t → ♯ sound′ (D-cong p₁≈p₂)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module _ where

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

variable
  f : Nat → Nat

-- Drops the argument to f!
foo : (n : Nat) → f n ≡ n → f (f n) ≡ n
foo n eq rewrite eq = eq

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K  #-}
module algebra.monoid.mset where

open import level
open import algebra.monoid.core
open import algebra.monoid.morphism
open import algebra.semigroup
open import equality.core
open import hott.level

module _ {i}(M : Set i) ⦃ mM : IsMonoid M ⦄ where
  open IsMonoid ⦃ ... ⦄
  record IsMSet {j} (X : Set j) : Set (i ⊔ j) where
    constructor mk-is-mset
    field
      _◂_ : M → X → X
      ◂-hom : (m₁ m₂ : M)(x : X) → (m₁ * m₂) ◂ x ≡ m₁ ◂ (m₂ ◂ x)
      ◂-id : (x : X) → e ◂ x ≡ x
      mset-level : h 2 X

  open IsMSet ⦃ ... ⦄

  module _ {j k}
           {X : Set j} ⦃ xM : IsMSet X ⦄
           {Y : Set k} ⦃ yM : IsMSet Y ⦄ where
    IsMSetMorphism : (X → Y) → Set (i ⊔ j ⊔ k)
    IsMSetMorphism f = (m : M)(x : X) → f (m ◂ x) ≡ m ◂ f x

    is-mset-morphism-level : h 2 Y → (f : X → Y)
      → h 1 (IsMSetMorphism f)
    is-mset-morphism-level hY f = Π-level λ m → Π-level λ x → hY _ _

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- Andreas, 2013-10-27

{-# OPTIONS --copatterns #-}

module Issue907a where

import Common.Level
open import Common.Prelude
open import Common.Product

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero

test : ∀ {A} → Σ Nat λ n → Vec A n
proj₁ test = zero
proj₂ test = []

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT
open import homotopy.SuspAdjointLoop
open import cohomology.WithCoefficients

module cohomology.SuspAdjointLoopIso where

module SuspAdjointLoopIso {i j} (X : Ptd i) (Y : Ptd j) where

  module ΣAΩ = SuspAdjointLoop X (⊙Ω Y)
  GSΣ = →Ω-group-structure (⊙Susp X) Y
  GSΩ = →Ω-group-structure X (⊙Ω Y)
  open GroupStructure

  comp-path : (p q : fst (⊙Ω (⊙Ω Y))) → ap2 _∙_ p q == p ∙ q
  comp-path p q = ap2-out _∙_ p q ∙ ap2 _∙_ (lemma p) (ap-idf q)
    where
    lemma : ∀ {i} {A : Type i} {x y : A} {p q : x == y} (α : p == q)
      → ap (λ r → r ∙ idp) α == ∙-unit-r p ∙ α ∙' ! (∙-unit-r q)
    lemma {p = idp} idp = idp

  pres-comp-inner : (H₁ H₂ : fst (⊙Susp X ⊙→ ⊙Ω Y))
    → ΣAΩ.R (comp GSΣ H₁ H₂) == comp GSΩ (ΣAΩ.R H₁) (ΣAΩ.R H₂)
  pres-comp-inner H₁ H₂ =
    transport
       (λ {(op , op-path) →
          ΣAΩ.R (comp GSΣ H₁ H₂) ==
          transport (λ b → Σ (fst X → _) (λ h → h (snd X) == b)) op-path
            (ΣAΩ.comp-lift (snd X) idp idp op (ΣAΩ.R H₁) (ΣAΩ.R H₂))})
       (pair= (λ= (λ p → λ= (comp-path p)))
              {b = idp} {b' = idp} (↓-app=cst-in snd-path))
       (ΣAΩ.pres-comp _∙_ H₁ H₂)
    where
    snd-path : idp == ap (λ f → f idp idp) (λ= (λ p → λ= (comp-path p))) ∙ idp
    snd-path =
      idp
        =⟨ ! (app=-β (comp-path idp) idp) ⟩
      app= (λ= (comp-path idp)) idp
        =⟨ ap (λ q → app= q idp) (! (app=-β (λ p → λ= (comp-path p)) idp)) ⟩
      app= (app= (λ= (λ p → λ= (comp-path p))) idp) idp
        =⟨ ∘-ap (λ z → z idp) (λ z → z idp) (λ= (λ p → λ= (comp-path p))) ⟩
      ap (λ f → f idp idp) (λ= (λ p → λ= (comp-path p)))
        =⟨ ! (∙-unit-r _) ⟩
      ap (λ f → f idp idp) (λ= (λ p → λ= (comp-path p))) ∙ idp ∎

  iso : →Ω-Group (⊙Susp X) Y ≃ᴳ →Ω-Group X (⊙Ω Y)
  iso = Trunc-Group-iso ΣAΩ.R pres-comp-inner (snd (ΣAΩ.eqv))

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


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

syntax Unit | U

type
  𝟙 : 0-ary

term
  unit : 𝟙

theory
  (𝟙η) u : 𝟙 |> u = unit
-}

module Unit.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Unit.Signature
open import Unit.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution U:Syn
open import SOAS.Metatheory.SecondOrder.Equality U:Syn

private
  variable
    α β γ τ : UT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ U) α Γ → (𝔐 ▷ U) α Γ → Set where
  𝟙η : ⁅ 𝟙 ⁆̣ ▹ ∅ ⊢ 𝔞 ≋ₐ unit

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import HoTT
open import homotopy.CoHSpace
open import cohomology.Theory

module cohomology.CoHSpace {i} (CT : CohomologyTheory i) (n : ℤ)
  {X : Ptd i} (CHSS : CoHSpaceStructure X) where

open CohomologyTheory CT
open CoHSpaceStructure CHSS
open import cohomology.Wedge CT n

abstract
  private
    lemma-l : CEl-fmap n ⊙coμ ∘ CEl-fmap n ⊙projl ∼ idf _
    lemma-l x =
        ∘-CEl-fmap n ⊙coμ ⊙projl x
      ∙ ap (λ f → CEl-fmap n f x) (⊙λ= ⊙unit-r)
      ∙ CEl-fmap-idf n x

    lemma-r : CEl-fmap n ⊙coμ ∘ CEl-fmap n ⊙projr ∼ idf _
    lemma-r x =
        ∘-CEl-fmap n ⊙coμ ⊙projr x
      ∙ ap (λ f → CEl-fmap n f x) (⊙λ= ⊙unit-l)
      ∙ CEl-fmap-idf n x

  C-fmap-coμ : ∀ x → CEl-fmap n ⊙coμ x == Group.comp (C n X) (CEl-fmap n ⊙winl x) (CEl-fmap n ⊙winr x)
  C-fmap-coμ x =
    CEl-fmap n ⊙coμ x
      =⟨ C-Wedge-out-η-comm-sqr X X (C-fmap n ⊙coμ) □$ᴳ x ⟩
    Group.comp (C n X)
      (CEl-fmap n ⊙coμ (CEl-fmap n ⊙projl (CEl-fmap n ⊙winl x)))
      (CEl-fmap n ⊙coμ (CEl-fmap n ⊙projr (CEl-fmap n ⊙winr x)))
      =⟨ ap2 (Group.comp (C n X)) (lemma-l (CEl-fmap n ⊙winl x)) (lemma-r (CEl-fmap n ⊙winr x)) ⟩
    Group.comp (C n X) (CEl-fmap n ⊙winl x) (CEl-fmap n ⊙winr x)
    =∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

--open import HoTT
open import homotopy.3x3.PushoutPushout
open import homotopy.3x3.Transpose
import homotopy.3x3.To as To
import homotopy.3x3.From as From
open import homotopy.3x3.Common

module homotopy.3x3.ToFrom {i} (d : Span^2 {i}) where

open Span^2 d
open M d hiding (Pushout^2)
open M (transpose d) using () renaming (A₀∙ to A∙₀; A₂∙ to A∙₂; A₄∙ to A∙₄;
                                        module F₁∙ to F∙₁; f₁∙ to f∙₁;
                                        module F₃∙ to F∙₃; f₃∙ to f∙₃;
                                        v-h-span to h-v-span)
open M using (Pushout^2)

open To d
open From d

open import homotopy.3x3.ToFromInit d
open import homotopy.3x3.ToFrom2 d
open import homotopy.3x3.ToFrom3 d

to-from-g-g : (c : A₂₂) → (to-from-g-l (f₁₂ c) , ↓-='-out (apd (to-from-r ∘ f∙₃) (glue c)) , ↓-='-out (apd (ap to ∘ ap from ∘ glue) (glue c))
                        =□□ ↓-='-out (apd glue (glue c)) , ↓-='-out (apd (to-from-l ∘ f∙₁) (glue c)) , to-from-g-r (f₃₂ c))
to-from-g-g c = coh _ lemma1 lemma3 _ _ (↓-='-out (apd glue (glue c))) lemma2
                    where
                open M2 c
                open M3 c

to-from-g-g' : (c : A₂₂) → to-from-g-l (f₁₂ c) == to-from-g-r (f₃₂ c) [ (λ c → (to-from-l (f∙₁ c) , glue c =□ ap to (ap from (glue c)) , to-from-r (f∙₃ c))) ↓ glue c ]
to-from-g-g' c = ↓-=□-in (to-from-g-g c)

module ToFromG = PushoutElim {d = span _ _ _ f₁₂ f₃₂} {P = λ c → (to-from-l (f∙₁ c) , glue c =□ ap to (ap from (glue c)) , to-from-r (f∙₃ c))}
                 to-from-g-l to-from-g-r to-from-g-g'

to-from-g : (c : A∙₂) → (to-from-l (f∙₁ c) , glue c =□ ap to (ap from (glue c)) , to-from-r (f∙₃ c))
to-from-g = ToFromG.f

to-from-g' : (c : A∙₂) → to-from-l (f∙₁ c) == to-from-r (f∙₃ c) [ (λ z → to (from z) == z) ↓ glue c ]
to-from-g' c = ↓-∘=idf-in to from (to-from-g c)

to-from : (x : Pushout^2 (transpose d)) → to (from x) == x
to-from = Pushout-elim to-from-l to-from-r to-from-g'

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module SubstantiveDischargeIsConsistent where

open import HasNegation
open import HasSubstantiveDischarge

record SubstantiveDischargeIsConsistent (+ : Set) (- : Set) ⦃ _ : HasNegation (-) ⦄ ⦃ _ : HasSubstantiveDischarge (+) (-) ⦄ : Set₁
 where
  field
    ≽-consistent : {+ : +} → { - : - } → + ≽ - → + ⋡ ~ -

open SubstantiveDischargeIsConsistent ⦃ … ⦄ public

{-# DISPLAY SubstantiveDischargeIsConsistent.≽-consistent _ = ≽-consistent #-}


text:
------------------------------------------------------------------------
-- Closure properties for h-levels
------------------------------------------------------------------------

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

-- Partly based on Voevodsky's work on so-called univalent
-- foundations.

open import Equality

module H-level.Closure
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq as Bijection hiding (id; _∘_)
open Derived-definitions-and-properties eq
import Equality.Decidable-UIP eq as DUIP
open import Equality.Decision-procedures eq
open import H-level eq
open import Logical-equivalence hiding (id; _∘_)
open import Nat eq as Nat
open import Prelude
open import Surjection eq as Surjection hiding (id; _∘_)

------------------------------------------------------------------------
-- The unit type

-- The unit type is contractible.

⊤-contractible : Contractible ⊤
⊤-contractible = (_ , λ _ → refl _)

-- A type is contractible iff it is in bijective correspondence with
-- the unit type.

contractible⇔↔⊤ : ∀ {a} {A : Type a} → Contractible A ⇔ (A ↔ ⊤)
contractible⇔↔⊤ = record
  { to   = flip contractible-isomorphic ⊤-contractible
  ; from = λ A↔⊤ → respects-surjection
                     (_↔_.surjection (Bijection.inverse A↔⊤))
                     0
                     ⊤-contractible
  }

------------------------------------------------------------------------
-- The empty type

abstract

  -- The empty type is not contractible.

  ¬-⊥-contractible : ∀ {ℓ} → ¬ Contractible (⊥ {ℓ = ℓ})
  ¬-⊥-contractible = ⊥-elim ∘ proj₁

  -- The empty type is propositional.

  ⊥-propositional : ∀ {ℓ} → Is-proposition (⊥ {ℓ = ℓ})
  ⊥-propositional x = ⊥-elim x

  -- Thus any uninhabited type is also propositional.

  uninhabited-propositional : ∀ {a} {A : Type a} →
                              ¬ A → Is-proposition A
  uninhabited-propositional ¬A =
    respects-surjection (_↔_.surjection $ ⊥↔uninhabited {ℓ = # 0} ¬A) 1
                        ⊥-propositional

------------------------------------------------------------------------
-- Booleans

abstract

  -- The booleans are not propositional.

  ¬-Bool-propositional : ¬ Is-proposition Bool
  ¬-Bool-propositional propositional =
    Bool.true≢false $
    propositional true false

  -- The booleans form a set.

  Bool-set : Is-set Bool
  Bool-set = DUIP.decidable⇒set Bool._≟_

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

abstract

  -- ℕ is not propositional.

  ¬-ℕ-propositional : ¬ Is-proposition ℕ
  ¬-ℕ-propositional ℕ-prop = 0≢+ $ ℕ-prop 0 1

  -- ℕ is a set.

  ℕ-set : Is-set ℕ
  ℕ-set = DUIP.decidable⇒set Nat._≟_

  -- Nat._≤_ is not a family of contractible types.

  ¬-≤-contractible : ¬ (∀ {m n} → Contractible (m Nat.≤ n))
  ¬-≤-contractible ≤-contr with proj₁ (≤-contr {m = 1} {n = 0})
  ... | ≤-refl′ 1≡0   = 0≢+ (sym 1≡0)
  ... | ≤-step′ _ +≡0 = 0≢+ (sym +≡0)

  -- Nat._≤_ is a family of propositions.

  ≤-propositional : ∀ {m n} → Is-proposition (m Nat.≤ n)
  ≤-propositional = irr
    where
    lemma : ∀ {m n k} → m ≡ n → m ≤ k → suc k ≡ n → ⊥₀
    lemma {m} {n} {k} m≡n m≤k 1+k≡n = <-irreflexive (
      suc n  ≡⟨ cong suc $ sym m≡n ⟩≤
      suc m  ≤⟨ suc≤suc m≤k ⟩
      suc k  ≡⟨ 1+k≡n ⟩≤
      n      ∎≤)

    cong-≤-step′ :
      ∀ {m n k₁ k₂}
        {p₁ : m ≤ k₁} {q₁ : suc k₁ ≡ n}
        {p₂ : m ≤ k₂} {q₂ : suc k₂ ≡ n} →
      (k₁≡k₂ : k₁ ≡ k₂) →
      subst (m ≤_) k₁≡k₂ p₁ ≡ p₂ →
      subst (λ k → suc k ≡ n) k₁≡k₂ q₁ ≡ q₂ →
      ≤-step′ p₁ q₁ ≡ ≤-step′ p₂ q₂
    cong-≤-step′ {p₁ = p₁} {q₁} {p₂} {q₂} k₁≡k₂ p-eq q-eq =
      cong (λ { (k , p , q) → ≤-step′ {k = k} p q })
        (Σ-≡,≡→≡
           k₁≡k₂
           (subst (λ k → _ ≤ k × suc k ≡ _) k₁≡k₂ (p₁ , q₁)             ≡⟨ push-subst-, _ _ ⟩
            (subst (_ ≤_) k₁≡k₂ p₁ , subst (λ k → suc k ≡ _) k₁≡k₂ q₁)  ≡⟨ cong₂ _,_ p-eq q-eq ⟩∎
            (p₂ , q₂)                                                   ∎))

    irr : ∀ {m n} → Is-proposition (m Nat.≤ n)
    irr (≤-refl′ q₁)    (≤-refl′ q₂)    = cong ≤-refl′ $ ℕ-set q₁ q₂
    irr (≤-refl′ q₁)    (≤-step′ p₂ q₂) = ⊥-elim (lemma q₁ p₂ q₂)
    irr (≤-step′ p₁ q₁) (≤-refl′ q₂)    = ⊥-elim (lemma q₂ p₁ q₁)

    irr {n = n} (≤-step′ {k = k₁} p₁ q₁)
                (≤-step′ {k = k₂} p₂ q₂) =
      cong-≤-step′ (cancel-suc (suc k₁  ≡⟨ q₁ ⟩
                                n       ≡⟨ sym q₂ ⟩∎
                                suc k₂  ∎))
                   (irr _ p₂)
                   (ℕ-set _ _)

  -- Nat.Distinct is not a family of contractible types.

  ¬-Distinct-contractible :
    ¬ (∀ m n → Contractible (Nat.Distinct m n))
  ¬-Distinct-contractible Distinct-contr =
    proj₁ (Distinct-contr 0 0)

  -- Distinct is a family of propositions.

  Distinct-propositional : ∀ m n → Is-proposition (Distinct m n)
  Distinct-propositional zero    zero    = ⊥-propositional
  Distinct-propositional zero    (suc n) = mono₁ 0 ⊤-contractible
  Distinct-propositional (suc m) zero    = mono₁ 0 ⊤-contractible
  Distinct-propositional (suc m) (suc n) = Distinct-propositional m n

------------------------------------------------------------------------
-- Π-types

-- Closure of contractibility under Π A is logically equivalent to
-- having extensional equality for functions from A.

Π-closure-contractible⇔extensionality :
  ∀ {a b} {A : Type a} →
  ({B : A → Type b} →
   (∀ x → Contractible (B x)) → Contractible ((x : A) → B x)) ⇔
  ({B : A → Type b} → Extensionality′ A B)
Π-closure-contractible⇔extensionality {b = b} {A} = record
  { to   = ⇒
  ; from = λ ext cB →
      ((λ x → proj₁ (cB x)) , λ f → ext λ x → proj₂ (cB x) (f x))
  }
  where
  ⇒ : ({B : A → Type b} →
       (∀ x → Contractible (B x)) → Contractible ((x : A) → B x)) →
      (∀ {B} → Extensionality′ A B)
  ⇒ closure {B} {f} {g} f≡g =
    f                                     ≡⟨ sym (cong (λ c → λ x → proj₁ (c x)) $
                                               proj₂ contractible (λ x → (f x , f≡g x))) ⟩
    (λ x → proj₁ (proj₁ contractible x))  ≡⟨ cong (λ c → λ x → proj₁ (c x)) $
                                               proj₂ contractible (λ x → (g x , refl (g x))) ⟩∎
    g                                     ∎
    where
    contractible : Contractible ((x : A) → Singleton (g x))
    contractible = closure (singleton-contractible ∘ g)

abstract

  -- Given (generalised) extensionality one can define an
  -- extensionality proof which is well-behaved.

  extensionality⇒well-behaved-extensionality :
    ∀ {a b} {A : Type a} →
    ({B : A → Type b} → Extensionality′ A B) →
    {B : A → Type b} → Well-behaved-extensionality A B
  extensionality⇒well-behaved-extensionality {A = A} ext {B} =
    (λ {_} → ext′) , λ f →
      ext′ (refl ∘ f)  ≡⟨ trans-symˡ _ ⟩∎
      refl f           ∎
    where
    ext′ : Extensionality′ A B
    ext′ = to (from ext)
      where open _⇔_ Π-closure-contractible⇔extensionality

-- A potential inverse of extensionality. (See Equivalence for a proof
-- which shows that this function has an inverse, assuming
-- extensionality.)

ext⁻¹ : ∀ {a b} {A : Type a} {B : A → Type b} {f g : (x : A) → B x} →
        f ≡ g → (∀ x → f x ≡ g x)
ext⁻¹ f≡g = λ x → cong (λ h → h x) f≡g

abstract

  -- "Evaluation rule" for ext⁻¹.

  ext⁻¹-refl : ∀ {a b} {A : Type a} {B : A → Type b}
               (f : (x : A) → B x) {x} →
               ext⁻¹ (refl f) x ≡ refl (f x)
  ext⁻¹-refl f {x} = cong-refl (λ h → h x)

  -- Given extensionality there is a (split) surjection from
  -- ∀ x → f x ≡ g x to f ≡ g.

  ext-surj : ∀ {a b} →
             Extensionality a b →
             {A : Type a} {B : A → Type b} {f g : (x : A) → B x} →
             (∀ x → f x ≡ g x) ↠ (f ≡ g)
  ext-surj {b = b} ext {A} {B} = record
    { logical-equivalence = record
      { to   = to
      ; from = ext⁻¹
      }
    ; right-inverse-of =
        elim (λ {f g} f≡g → to (ext⁻¹ f≡g) ≡ f≡g) λ h →
          proj₁ ext′ (ext⁻¹ (refl h))  ≡⟨ cong (proj₁ ext′) (proj₁ ext′ λ _ →
                                            ext⁻¹-refl h) ⟩
          proj₁ ext′ (refl ∘ h)        ≡⟨ proj₂ ext′ h ⟩∎
          refl h                       ∎
    }
    where
    ext′ : {B : A → Type b} → Well-behaved-extensionality A B
    ext′ = extensionality⇒well-behaved-extensionality (apply-ext ext)

    to : {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g
    to = proj₁ ext′

-- H-level′ is closed under Π A (assuming extensionality).

Π-closure′ :
  ∀ {a b} {A : Type a} {B : A → Type b} →
  Extensionality a b →
  ∀ n → (∀ x → H-level′ n (B x)) → H-level′ n ((x : A) → B x)
Π-closure′ ext zero =
  _⇔_.from Π-closure-contractible⇔extensionality (apply-ext ext)
Π-closure′ ext (suc n) = λ h f g →
  respects-surjection′ (ext-surj ext) n $
    Π-closure′ ext n (λ x → h x (f x) (g x))

-- H-level is closed under Π A (assuming extensionality).

Π-closure : ∀ {a b} {A : Type a} {B : A → Type b} →
            Extensionality a b →
            ∀ n → (∀ x → H-level n (B x)) → H-level n ((x : A) → B x)
Π-closure ext n h =
  _⇔_.from H-level⇔H-level′ $
  Π-closure′ ext n (λ x → _⇔_.to H-level⇔H-level′ (h x))

-- This also applies to the implicit function space.

implicit-Π-closure :
  ∀ {a b} {A : Type a} {B : A → Type b} →
  Extensionality a b →
  ∀ n → (∀ x → H-level n (B x)) → H-level n ({x : A} → B x)
implicit-Π-closure ext n =
  respects-surjection
    (_↔_.surjection $ Bijection.inverse implicit-Π↔Π) n ∘
  Π-closure ext n

abstract

  -- Negated types are propositional, assuming extensionality.

  ¬-propositional :
    ∀ {a} {A : Type a} →
    Extensionality a lzero →
    Is-proposition (¬ A)
  ¬-propositional ext = Π-closure ext 1 (λ _ → ⊥-propositional)

-- The type ∀ y → x ≡ y is a proposition (assuming extensionality).
--
-- This is Lemma 4.1 from van Doorn's "Constructing the Propositional
-- Truncation using Non-recursive HITs" (perhaps the proof is not
-- quite identical to van Doorn's).

Π≡-proposition :
  ∀ {a} {A : Type a} →
  Extensionality a a →
  (x : A) → Is-proposition (∀ y → x ≡ y)
Π≡-proposition {A = A} ext x =
  [inhabited⇒+]⇒+ 0 λ f →
  let prop : Is-proposition A
      prop u v =
        u  ≡⟨ sym (f u) ⟩
        x  ≡⟨ f v ⟩∎
        v  ∎
  in
  Π-closure ext 1 λ _ →
  mono₁ 1 prop

------------------------------------------------------------------------
-- Σ-types

-- H-level′ is closed under Σ.

Σ-closure′ :
  ∀ {a b} {A : Type a} {B : A → Type b} n →
  H-level′ n A → (∀ x → H-level′ n (B x)) → H-level′ n (Σ A B)
Σ-closure′ {A = A} {B} zero (x , irrA) hB =
  ((x , proj₁ (hB x)) , λ p →
     (x       , proj₁ (hB x))          ≡⟨ elim (λ {x y} _ → _≡_ {A = Σ A B} (x , proj₁ (hB x))
                                                                            (y , proj₁ (hB y)))
                                               (λ _ → refl _)
                                               (irrA (proj₁ p)) ⟩
     (proj₁ p , proj₁ (hB (proj₁ p)))  ≡⟨ cong (_,_ (proj₁ p)) (proj₂ (hB (proj₁ p)) (proj₂ p)) ⟩∎
     p                                 ∎)
Σ-closure′ {B = B} (suc n) hA hB = λ p₁ p₂ →
  respects-surjection′ (_↔_.surjection Σ-≡,≡↔≡) n $
    Σ-closure′ n (hA (proj₁ p₁) (proj₁ p₂))
      (λ pr₁p₁≡pr₁p₂ →
         hB (proj₁ p₂) (subst B pr₁p₁≡pr₁p₂ (proj₂ p₁)) (proj₂ p₂))

-- H-level is closed under Σ.

Σ-closure : ∀ {a b} {A : Type a} {B : A → Type b} n →
            H-level n A → (∀ x → H-level n (B x)) → H-level n (Σ A B)
Σ-closure n hA hB =
  _⇔_.from H-level⇔H-level′
    (Σ-closure′ n (_⇔_.to H-level⇔H-level′ hA)
                  (_⇔_.to H-level⇔H-level′ ∘ hB))

abstract

  -- In the case of contractibility the codomain only needs to have
  -- the right h-level (0) for a single index.

  Σ-closure-contractible :
    ∀ {a b} {A : Type a} {B : A → Type b} →
    (c : Contractible A) → Contractible (B (proj₁ c)) →
    Contractible (Σ A B)
  Σ-closure-contractible {B = B} cA (b , irrB) = Σ-closure 0 cA cB
    where
    cB : ∀ a → Contractible (B a)
    cB a =
      subst B (proj₂ cA a) b , λ b′ →

      subst B (proj₂ cA a) b                                ≡⟨ cong (subst B (proj₂ cA a)) $
                                                                irrB (subst B (sym $ proj₂ cA a) b′) ⟩
      subst B (proj₂ cA a) (subst B (sym $ proj₂ cA a) b′)  ≡⟨ subst-subst-sym _ _ _ ⟩∎

      b′                                                    ∎

  -- H-level is closed under _×_.

  ×-closure : ∀ {a b} {A : Type a} {B : Type b} n →
              H-level n A → H-level n B → H-level n (A × B)
  ×-closure n hA hB = Σ-closure n hA (const hB)

  -- If B a is inhabited for all a, and Σ A B has h-level n, then A
  -- also has h-level n.
  --
  -- One cannot, in general, replace ∀ a → B a with ∀ a → ∥ B a ∥ (see
  -- Circle.¬-generalised-proj₁-closure). However, this is possible if
  -- B is constant (see H-level.Truncation.Propositional.H-level-×₁).

  proj₁-closure :
    ∀ {a b} {A : Type a} {B : A → Type b} →
    (∀ a → B a) →
    ∀ n → H-level n (Σ A B) → H-level n A
  proj₁-closure {A = A} {B} inhabited = respects-surjection surj
    where
    surj : Σ A B ↠ A
    surj = record
      { logical-equivalence = record
        { to   = proj₁
        ; from = λ x → x , inhabited x
        }
      ; right-inverse-of = refl
      }

  -- If A is inhabited and A × B has h-level n, then B also has
  -- h-level n.

  proj₂-closure :
    ∀ {a b} {A : Type a} {B : Type b} →
    A →
    ∀ n → H-level n (A × B) → H-level n B
  proj₂-closure {A = A} {B} inhabited = respects-surjection surj
    where
    surj : A × B ↠ B
    surj = record
      { logical-equivalence = record
        { to   = proj₂
        ; from = λ x → inhabited , x
        }
      ; right-inverse-of = refl
      }

------------------------------------------------------------------------
-- Logical equivalences, split surjections and bijections

-- H-level n is closed under the type formers _⇔_, _↠_ and _↔_
-- (assuming extensionality).

⇔-closure :
  ∀ {a b} {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  ∀ n → H-level n A → H-level n B → H-level n (A ⇔ B)
⇔-closure {a} {b} ext n hA hB =
  respects-surjection
    (record
       { logical-equivalence = record
         { to   = _
         ; from = λ A⇔B → _⇔_.to A⇔B , _⇔_.from A⇔B
         }
       ; right-inverse-of = λ _ → refl _
       })
    n
    (×-closure n
       (Π-closure (lower-extensionality b a ext) n (λ _ → hB))
       (Π-closure (lower-extensionality a b ext) n (λ _ → hA)))

↠-closure :
  ∀ {a b} {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  ∀ n → H-level n A → H-level n B → H-level n (A ↠ B)
↠-closure {a} {b} ext n hA hB =
  respects-surjection
    (record
       { logical-equivalence = record
         { to   = _
         ; from = λ A↠B → _↠_.logical-equivalence A↠B ,
                          _↠_.right-inverse-of A↠B
         }
       ; right-inverse-of = λ _ → refl _
       })
    n
    (Σ-closure n (⇔-closure ext n hA hB) λ _ →
     Π-closure (lower-extensionality a a ext) n λ _ →
     ⇒≡ _ hB)

↔-closure :
  ∀ {a b} {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  ∀ n → H-level n A → H-level n B → H-level n (A ↔ B)
↔-closure {a} {b} ext n hA hB =
  respects-surjection
    (record
       { logical-equivalence = record
         { to   = _
         ; from = λ A↔B → _↔_.surjection A↔B ,
                          _↔_.left-inverse-of A↔B
         }
       ; right-inverse-of = λ _ → refl _
       })
    n
    (Σ-closure n (↠-closure ext n hA hB) λ _ →
     Π-closure (lower-extensionality b b ext) n λ _ →
     ⇒≡ _ hA)

------------------------------------------------------------------------
-- Lifted types

-- All H-levels are closed under lifting.

↑-closure : ∀ {a b} {A : Type a} n → H-level n A → H-level n (↑ b A)
↑-closure =
  respects-surjection (_↔_.surjection (Bijection.inverse ↑↔))

-- All H-levels are also closed under removal of lifting.

↑⁻¹-closure : ∀ {a b} {A : Type a} n → H-level n (↑ b A) → H-level n A
↑⁻¹-closure = respects-surjection (_↔_.surjection ↑↔)

------------------------------------------------------------------------
-- W-types

-- W-types are isomorphic to Σ-types containing W-types.

W-unfolding : ∀ {a b} {A : Type a} {B : A → Type b} →
              W A B ↔ ∃ λ (x : A) → B x → W A B
W-unfolding = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ w → headᵂ w , tailᵂ w
      ; from = uncurry sup
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = left-inverse-of
  }
  where
  left-inverse-of : (w : W _ _) → sup (headᵂ w) (tailᵂ w) ≡ w
  left-inverse-of (sup x f) = refl (sup x f)

abstract

  -- Equality between elements of a W-type can be proved using a pair
  -- of equalities (assuming extensionality).

  W-≡,≡↠≡ : ∀ {a b} {A : Type a} {B : A → Type b} →
            Extensionality b (a ⊔ b) →
            ∀ {x y} {f : B x → W A B} {g : B y → W A B} →
            (∃ λ (p : x ≡ y) → ∀ i → f i ≡ g (subst B p i)) ↠
            (sup x f ≡ sup y g)
  W-≡,≡↠≡ {a} {A = A} {B} ext {x} {y} {f} {g} =
    (∃ λ (p : x ≡ y) → ∀ i → f i ≡ g (subst B p i))        ↠⟨ Surjection.∃-cong lemma ⟩
    (∃ λ (p : x ≡ y) → subst (λ x → B x → W A B) p f ≡ g)  ↠⟨ _↔_.surjection Σ-≡,≡↔≡ ⟩
    (_≡_ {A = ∃ λ (x : A) → B x → W A B} (x , f) (y , g))  ↠⟨ ↠-≡ (_↔_.surjection (Bijection.inverse (W-unfolding {A = A} {B = B}))) ⟩□
    (sup x f ≡ sup y g)                                    □
    where
    lemma : (p : x ≡ y) →
            (∀ i → f i ≡ g (subst B p i)) ↠
            (subst (λ x → B x → W A B) p f ≡ g)
    lemma p = elim
      (λ {x y} p → (f : B x → W A B) (g : B y → W A B) →
                   (∀ i → f i ≡ g (subst B p i)) ↠
                   (subst (λ x → B x → W A B) p f ≡ g))
      (λ x f g →
         (∀ i → f i ≡ g (subst B (refl x) i))        ↠⟨ subst (λ h → (∀ i → f i ≡ g (h i)) ↠ (∀ i → f i ≡ g i))
                                                              (sym (apply-ext (lower-extensionality lzero a ext) (subst-refl B)))
                                                              Surjection.id ⟩
         (∀ i → f i ≡ g i)                           ↠⟨ ext-surj ext ⟩
         (f ≡ g)                                     ↠⟨ subst (λ h → (f ≡ g) ↠ (h ≡ g))
                                                              (sym $ subst-refl (λ x' → B x' → W A B) f)
                                                              Surjection.id ⟩□
         (subst (λ x → B x → W A B) (refl x) f ≡ g)  □)
      p f g

  -- H-level is not closed under W.

  ¬-W-closure-contractible : ∀ {a b} →
    ¬ (∀ {A : Type a} {B : A → Type b} →
       Contractible A → (∀ x → Contractible (B x)) →
       Contractible (W A B))
  ¬-W-closure-contractible closure =
    inhabited⇒W-empty (const (lift tt)) $
    proj₁ $
    closure (↑-closure 0 ⊤-contractible)
            (const (↑-closure 0 ⊤-contractible))

  ¬-W-closure : ∀ {a b} →
    ¬ (∀ {A : Type a} {B : A → Type b} n →
       H-level n A → (∀ x → H-level n (B x)) → H-level n (W A B))
  ¬-W-closure closure = ¬-W-closure-contractible (closure 0)

  -- However, all positive h-levels are closed under W (assuming
  -- extensionality).

  W-closure′ :
    ∀ {a b} {A : Type a} {B : A → Type b} →
    Extensionality b (a ⊔ b) →
    ∀ n → H-level′ (1 + n) A → H-level′ (1 + n) (W A B)
  W-closure′ {A = A} {B} ext n h = closure
    where
    closure : (x y : W A B) → H-level′ n (x ≡ y)
    closure (sup x f) (sup y g) =
      respects-surjection′ (W-≡,≡↠≡ ext) n $
        Σ-closure′ n (h x y) (λ _ →
          Π-closure′ ext n (λ i → closure (f _) (g _)))

  W-closure :
    ∀ {a b} {A : Type a} {B : A → Type b} →
    Extensionality b (a ⊔ b) →
    ∀ n → H-level (1 + n) A → H-level (1 + n) (W A B)
  W-closure ext n h =
    _⇔_.from H-level⇔H-level′
      (W-closure′ ext n (_⇔_.to H-level⇔H-level′ h))

------------------------------------------------------------------------
-- H-levels

abstract

  -- Contractible is /not/ a comonad in the category of types and
  -- functions, because map cannot be defined, but we can at least
  -- define the following functions.

  counit : ∀ {a} {A : Type a} → Contractible A → A
  counit = proj₁

  cojoin : ∀ {a} {A : Type a} →
           Extensionality a a →
           Contractible A → Contractible (Contractible A)
  cojoin {A = A} ext contr = contr₃
    where
    x : A
    x = proj₁ contr

    contr₁ : Contractible (∀ y → x ≡ y)
    contr₁ = Π-closure′ ext 0 (mono₁′ 0 contr x)

    contr₂ : (x : A) → Contractible (∀ y → x ≡ y)
    contr₂ x =
      subst (λ x → Contractible (∀ y → x ≡ y)) (proj₂ contr x) contr₁

    contr₃ : Contractible (∃ λ (x : A) → ∀ y → x ≡ y)
    contr₃ = Σ-closure 0 contr contr₂

  -- Contractible is not necessarily contractible.

  ¬-Contractible-contractible :
    ¬ ({A : Type} → Contractible (Contractible A))
  ¬-Contractible-contractible contr = proj₁ $ proj₁ $ contr {A = ⊥}

  -- Contractible is propositional (assuming extensionality).

  Contractible-propositional :
    ∀ {a} {A : Type a} →
    Extensionality a a →
    Is-proposition (Contractible A)
  Contractible-propositional ext =
    [inhabited⇒contractible]⇒propositional (cojoin ext)

  -- H-level′ is closed under λ P → For-iterated-equality n P A.

  H-level′-For-iterated-equality :
    ∀ {p A} {P : Type p → Type p} →
    Extensionality p p →
    ∀ m n →
    (∀ {A} → H-level′ m (P A)) →
    H-level′ m (For-iterated-equality n P A)
  H-level′-For-iterated-equality ext m zero    hyp = hyp
  H-level′-For-iterated-equality ext m (suc n) hyp =
    Π-closure′ ext m λ _ →
    Π-closure′ ext m λ _ →
    H-level′-For-iterated-equality ext m n hyp

  -- A variant of the previous result.

  H-level′-For-iterated-equality′ :
    ∀ {p A} {P : Type p → Type p} →
    Extensionality p p →
    ∀ m n {o} →
    H-level′ (n + o) A →
    (∀ {A} → H-level′ o A → H-level′ m (P A)) →
    H-level′ m (For-iterated-equality n P A)
  H-level′-For-iterated-equality′ ext m zero    hyp₁ hyp₂ = hyp₂ hyp₁
  H-level′-For-iterated-equality′ ext m (suc n) hyp₁ hyp₂ =
    Π-closure′ ext m λ _ →
    Π-closure′ ext m λ _ →
    H-level′-For-iterated-equality′ ext m n (hyp₁ _ _) hyp₂

  -- H-level is closed under λ P → For-iterated-equality n P A.

  H-level-For-iterated-equality :
    ∀ {p A} {P : Type p → Type p} →
    Extensionality p p →
    ∀ m n →
    (∀ {A} → H-level m (P A)) →
    H-level m (For-iterated-equality n P A)
  H-level-For-iterated-equality ext m n hyp =
    _⇔_.from H-level⇔H-level′ $
    H-level′-For-iterated-equality ext m n $
    _⇔_.to H-level⇔H-level′ hyp

  -- A variant of the previous result.

  H-level-For-iterated-equality′ :
    ∀ {p A} {P : Type p → Type p} →
    Extensionality p p →
    ∀ m n {o} →
    H-level (n + o) A →
    (∀ {A} → H-level o A → H-level m (P A)) →
    H-level m (For-iterated-equality n P A)
  H-level-For-iterated-equality′ ext m n hyp₁ hyp₂ =
    _⇔_.from (H-level⇔H-level′ {n = m}) $
    H-level′-For-iterated-equality′ ext m n
      (_⇔_.to H-level⇔H-level′ hyp₁)
      (_⇔_.to H-level⇔H-level′ ∘ hyp₂ ∘ _⇔_.from H-level⇔H-level′)

  -- H-level′ is pointwise propositional (assuming extensionality).

  H-level′-propositional :
    ∀ {a} → Extensionality a a →
    ∀ {A : Type a} n → Is-proposition (H-level′ n A)
  H-level′-propositional ext n =
    _⇔_.from (H-level⇔H-level′ {n = 1}) $
    H-level′-For-iterated-equality ext 1 n $
    _⇔_.to (H-level⇔H-level′ {n = 1}) $
    Contractible-propositional ext

  -- The property Is-proposition A is a proposition (assuming
  -- extensionality).
  --
  -- This result is proved in the HoTT book (first edition,
  -- Lemma 3.3.5).

  Is-proposition-propositional :
    ∀ {a} {A : Type a} → Extensionality a a →
    Is-proposition (Is-proposition A)
  Is-proposition-propositional ext = [inhabited⇒+]⇒+ 0 λ p →
    Π-closure ext 1 λ _ →
    Π-closure ext 1 λ _ →
    ⇒≡ 1 p

  -- All h-levels are propositional (assuming extensionality).

  H-level-propositional :
    ∀ {a} → Extensionality a a →
    ∀ {A : Type a} n → Is-proposition (H-level n A)
  H-level-propositional ext zero =
    Contractible-propositional ext
  H-level-propositional ext (suc zero) =
    Is-proposition-propositional ext
  H-level-propositional {A} ext (suc (suc n)) =
    implicit-Π-closure ext 1 λ x →
    implicit-Π-closure ext 1 λ y →
    H-level-propositional ext {A = x ≡ y} (suc n)

  -- Uniqueness-of-identity-proofs is pointwise propositional
  -- (assuming extensionality).

  UIP-propositional :
    ∀ {ℓ} → Extensionality (lsuc ℓ) ℓ →
    Is-proposition (Uniqueness-of-identity-proofs ℓ)
  UIP-propositional ext =
    implicit-Π-closure ext 1 λ A →
    H-level-propositional (lower-extensionality _ lzero ext) 2

------------------------------------------------------------------------
-- Binary sums

abstract

  -- Binary sums can be expressed using Σ and Bool (with large
  -- elimination).

  sum-as-pair : ∀ {a b} {A : Type a} {B : Type b} →
                (A ⊎ B) ↔ (∃ λ (x : Bool) → if x then ↑ b A else ↑ a B)
  sum-as-pair {a} {b} {A} {B} = record
    { surjection = record
      { logical-equivalence = record
        { to   = to
        ; from = from
        }
      ; right-inverse-of = to∘from
      }
    ; left-inverse-of = [ refl ∘ inj₁ {B = B} , refl ∘ inj₂ {A = A} ]
    }
    where
    to : A ⊎ B → (∃ λ (x : Bool) → if x then ↑ b A else ↑ a B)
    to = [ _,_ true ∘ lift , _,_ false ∘ lift ]

    from : (∃ λ (x : Bool) → if x then ↑ b A else ↑ a B) → A ⊎ B
    from (true  , x) = inj₁ $ lower x
    from (false , y) = inj₂ $ lower y

    to∘from : (y : ∃ λ x → if x then ↑ b A else ↑ a B) →
              to (from y) ≡ y
    to∘from (true  , x) = refl _
    to∘from (false , y) = refl _

  -- H-level is not closed under _⊎_.

  ¬-⊎-propositional : ∀ {a b} {A : Type a} {B : Type b} →
                      A → B → ¬ Is-proposition (A ⊎ B)
  ¬-⊎-propositional x y hA⊎B = ⊎.inj₁≢inj₂ $ hA⊎B (inj₁ x) (inj₂ y)

  ¬-⊎-closure : ∀ {a b} →
    ¬ (∀ {A : Type a} {B : Type b} n →
       H-level n A → H-level n B → H-level n (A ⊎ B))
  ¬-⊎-closure ⊎-closure =
    ¬-⊎-propositional (lift tt) (lift tt) $
    mono₁ 0 $
    ⊎-closure 0 (↑-closure 0 ⊤-contractible)
                (↑-closure 0 ⊤-contractible)

  -- However, all levels greater than or equal to 2 are closed under
  -- _⊎_.

  ⊎-closure :
    ∀ {a b} {A : Type a} {B : Type b} n →
    H-level (2 + n) A → H-level (2 + n) B → H-level (2 + n) (A ⊎ B)
  ⊎-closure {a} {b} {A} {B} n hA hB =
    respects-surjection
      (_↔_.surjection $ Bijection.inverse sum-as-pair)
      (2 + n)
      (Σ-closure (2 + n) Bool-2+n if-2+n)
    where
    Bool-2+n : H-level (2 + n) Bool
    Bool-2+n = mono (m≤m+n 2 n) Bool-set

    if-2+n : (x : Bool) → H-level (2 + n) (if x then ↑ b A else ↑ a B)
    if-2+n true  = respects-surjection
                     (_↔_.surjection $ Bijection.inverse ↑↔)
                     (2 + n) hA
    if-2+n false = respects-surjection
                     (_↔_.surjection $ Bijection.inverse ↑↔)
                     (2 + n) hB

  -- Furthermore, if A and B are propositions and mutually exclusive,
  -- then A ⊎ B is a proposition.

  ⊎-closure-propositional :
    ∀ {a b} {A : Type a} {B : Type b} →
    (A → B → ⊥₀) →
    Is-proposition A → Is-proposition B → Is-proposition (A ⊎ B)
  ⊎-closure-propositional A→B→⊥ A-prop B-prop = λ where
    (inj₁ a₁) (inj₁ a₂) → cong inj₁ (A-prop a₁ a₂)
    (inj₁ a₁) (inj₂ b₂) → ⊥-elim (A→B→⊥ a₁ b₂)
    (inj₂ b₁) (inj₁ a₂) → ⊥-elim (A→B→⊥ a₂ b₁)
    (inj₂ b₁) (inj₂ b₂) → cong inj₂ (B-prop b₁ b₂)

  -- All levels greater than or equal to 2 are also closed under
  -- Maybe.

  Maybe-closure :
    ∀ {a} {A : Type a} n →
    H-level (2 + n) A → H-level (2 + n) (Maybe A)
  Maybe-closure n h =
    ⊎-closure n (mono (zero≤ (2 + n)) ⊤-contractible) h

  -- T is pointwise propositional.

  T-propositional :
    ∀ {a b} {A : Type a} {B : Type b} →
    (x : A ⊎ B) → Is-proposition (T x)
  T-propositional (inj₁ _) = mono₁ 0 ⊤-contractible
  T-propositional (inj₂ _) = ⊥-propositional

  -- Furthermore Is-proposition is closed under Dec (assuming
  -- extensionality).

  Dec-closure-propositional :
    ∀ {a} {A : Type a} →
    Extensionality a lzero →
    Is-proposition A → Is-proposition (Dec A)
  Dec-closure-propositional {A = A} ext p = λ where
    (yes  a) (yes  a′) → cong yes $ p a a′
    (yes  a) (no  ¬a)  → ⊥-elim (¬a a)
    (no  ¬a) (yes  a)  → ⊥-elim (¬a a)
    (no  ¬a) (no  ¬a′) → cong no $ ¬-propositional ext ¬a ¬a′

  -- Is-proposition is also closed under _Xor_ (assuming
  -- extensionality).

  Xor-closure-propositional :
    ∀ {a b} {A : Type a} {B : Type b} →
    Extensionality (a ⊔ b) (# 0) →
    Is-proposition A → Is-proposition B →
    Is-proposition (A Xor B)
  Xor-closure-propositional {ℓa} {ℓb} {A} {B} ext pA pB = λ where
    (inj₁ (a , ¬b)) (inj₂ (¬a  , b))   → ⊥-elim (¬a a)
    (inj₂ (¬a , b)) (inj₁ (a   , ¬b))  → ⊥-elim (¬b b)
    (inj₁ (a , ¬b)) (inj₁ (a′  , ¬b′)) →
      cong₂ (λ x y → inj₁ (x , y))
        (pA a a′)
        (apply-ext (lower-extensionality ℓa _ ext) λ b → ⊥-elim (¬b b))
    (inj₂ (¬a , b)) (inj₂ (¬a′ , b′)) →
      cong₂ (λ x y → inj₂ (x , y))
        (apply-ext (lower-extensionality ℓb _ ext) λ a → ⊥-elim (¬a a))
        (pB b b′)

  -- However, H-level is not closed under _Xor_.

  ¬-Xor-closure-contractible : ∀ {a b} →
    ¬ ({A : Type a} {B : Type b} →
       Contractible A → Contractible B → Contractible (A Xor B))
  ¬-Xor-closure-contractible closure
    with proj₁ $ closure (↑-closure 0 ⊤-contractible)
                         (↑-closure 0 ⊤-contractible)
  ... | inj₁ (_ , ¬⊤) = ¬⊤ _
  ... | inj₂ (¬⊤ , _) = ¬⊤ _

  -- Alternative definition of ⊎-closure (for Type₀).

  module Alternative-proof where

    -- Is-set is closed under _⊎_, by an argument similar to the one
    -- Hedberg used to prove that decidable equality implies
    -- uniqueness of identity proofs.

    ⊎-closure-set : {A B : Type} →
                    Is-set A → Is-set B → Is-set (A ⊎ B)
    ⊎-closure-set {A} {B} A-set B-set = DUIP.constant⇒set c
      where
      c : (x y : A ⊎ B) → ∃ λ (f : x ≡ y → x ≡ y) → DUIP.Constant f
      c (inj₁ x) (inj₁ y) = (cong inj₁ ∘ ⊎.cancel-inj₁ , λ p q → cong (cong inj₁) $ A-set (⊎.cancel-inj₁ p) (⊎.cancel-inj₁ q))
      c (inj₂ x) (inj₂ y) = (cong inj₂ ∘ ⊎.cancel-inj₂ , λ p q → cong (cong inj₂) $ B-set (⊎.cancel-inj₂ p) (⊎.cancel-inj₂ q))
      c (inj₁ x) (inj₂ y) = (⊥-elim ∘ ⊎.inj₁≢inj₂       , λ _ → ⊥-elim ∘ ⊎.inj₁≢inj₂)
      c (inj₂ x) (inj₁ y) = (⊥-elim ∘ ⊎.inj₁≢inj₂ ∘ sym , λ _ → ⊥-elim ∘ ⊎.inj₁≢inj₂ ∘ sym)

    -- H-level is closed under _⊎_ for other levels greater than or equal
    -- to 2 too.

    ⊎-closure′ :
      ∀ {A B : Type} n →
      H-level (2 + n) A → H-level (2 + n) B → H-level (2 + n) (A ⊎ B)
    ⊎-closure′         zero    = ⊎-closure-set
    ⊎-closure′ {A} {B} (suc n) = clos
      where
      clos : H-level (3 + n) A → H-level (3 + n) B → H-level (3 + n) (A ⊎ B)
      clos hA hB {x = inj₁ x} {y = inj₁ y}         = respects-surjection (_↔_.surjection ≡↔inj₁≡inj₁) (2 + n) hA
      clos hA hB {x = inj₂ x} {y = inj₂ y}         = respects-surjection (_↔_.surjection ≡↔inj₂≡inj₂) (2 + n) hB
      clos hA hB {x = inj₁ x} {y = inj₂ y} {x = p} = ⊥-elim (⊎.inj₁≢inj₂ p)
      clos hA hB {x = inj₂ x} {y = inj₁ y} {x = p} = ⊥-elim (⊎.inj₁≢inj₂ (sym p))


text:
open import Coinduction using ( ∞ ; ♭ ; ♯_ )
open import Data.Bool using ( Bool ; true ; false )
open import Data.Empty using ( ⊥ ; ⊥-elim )
open import Data.Unit using ( ⊤ ; tt )
open import System.IO.Transducers.Lazy using
  ( _⇒_ ; inp ; out ; done ; choice ) renaming
  ( ⟦_⟧ to ⟦_⟧' ; _⟫_ to _⟫'_
  ; _[&]_ to _[&]'_ ; _⟨&⟩_ to _⟨&⟩'_ ; assoc to assoc' )
open import System.IO.Transducers.Session using ( Session ; I ; Σ ; Γ ; _/_ ; IsΣ ; ⟨_⟩ ; _&_ ; ¿ ; _⊕_ )
open import System.IO.Transducers.Trace using ( Trace ; [] ; _∷_ )

module System.IO.Transducers.Strict where

infixr 4 _⇛_
infixr 6 _⟫_
infixr 8 _[&]_ _⟨&⟩_

-- Strict tranducers are ones which perform input before any output

data Strict : ∀ {S T} → (S ⇒ T) → Set₁ where
  inp : ∀ {A V F T} P → (Strict (inp {A} {V} {F} {T} P))
  done : ∀ {S} → (Strict (done {S}))

-- Slightly annoyingly, _≡_ has different cardinalities
-- in different versions of the standard library.
-- Until 1.4 of agda-stdlib is more widely distributed,
-- we define a specialized version of _≡_ here.

data _≡_ (S : Session) : Session → Set₁ where
  refl : S ≡ S

-- S ⇛ T is the type of strict transducers regarded as functions

_⇛_ : Session → Session → Set₁
I     ⇛ T = I ≡ T
Σ V F ⇛ T = ∀ a → (♭ F a) ⇒ T

-- Identity transducer

id : ∀ {S} → S ⇛ S
id {I}     = refl
id {Σ V F} = λ a → out a done

-- Inclusion of strict in lazy transducers

ι : ∀ {S T} → (S ⇛ T) → (S ⇒ T)
ι {I}     refl = done
ι {Σ V F} P    = inp (♯ P)

-- Composition

_⟫_ : ∀ {S T U} → (S ⇛ T) → (T ⇛ U) → (S ⇛ U)
_⟫_ {I}             refl refl = refl
_⟫_ {Σ V F} {I}     P    refl = P
_⟫_ {Σ V F} {Σ W G} P    Q    = λ a → (P a ⟫' ι Q)

-- & on transducers

_[&]_ : ∀ {S T U V} → (S ⇛ T) → (U ⇛ V) → ((S & U) ⇛ (T & V))
_[&]_ {I}     refl Q = Q
_[&]_ {Σ V F} P    Q = λ a → (P a [&]' ι Q)

-- Associativity of &

assoc : ∀ {S T U} → ((S & (T & U)) ⇛ ((S & T) & U))
assoc {I}     {T} {U} = id {T & U}
assoc {Σ V F} {T} {U} = λ a → out a (assoc' {♭ F a})

-- Mediating morphism for &

_⟨&⟩_ : ∀ {S T U} → (S ⇛ T) → (S ⇛ U) → (S ⇛ T & U)
_⟨&⟩_ {I}     refl refl = refl
_⟨&⟩_ {Σ V F} P    Q    = λ a → (P a ⟨&⟩' Q a)

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io