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

-- We can use a propositional equality parametrized on Set instead of
-- using two "different" equalities on D and M.

module LogicalFramework.SetEquality where

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Relation/Binary/Core.agda).
infix 7 _≡D_ _≡M_

------------------------------------------------------------------------------
-- Domain universe D
postulate
  D : Set

-- Propositional equality on D.
data _≡D_ (x : D) : D → Set where
  refl : x ≡D x

≡D-thm : ∀ {d e} → d ≡D e → e ≡D d
≡D-thm refl = refl

------------------------------------------------------------------------------
-- Domain universe M

data M : Set where
  zero :     M
  succ : M → M

-- Propositional equality on M.
data _≡M_ (n : M) : M → Set where
  refl : n ≡M n

≡M-thm : ∀ {m n} → m ≡M n → n ≡M m
≡M-thm refl = refl

------------------------------------------------------------------------------
-- Propositional equality on Set.

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

≡-thm₁ : ∀ {d e : D} → d ≡ e → e ≡ d
≡-thm₁ refl = refl

≡-thm₂ : ∀ {m n : M} → m ≡ n → n ≡ m
≡-thm₂ refl = refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module L.Base.Coproduct.Properties where

-- There are no properties yet.

ext: agda

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
postulate
  I  : Set
  U  : I → Set
  El : ∀ {i} → U i → Set

infixr 4 _,_

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ

∃ : ∀ {A : Set} → (A → Set) → Set
∃ = Σ _

mutual

  infixl 5 _▻_

  data Ctxt : Set where
    _▻_ : (Γ : Ctxt) → Type Γ → Ctxt

  Type : Ctxt → Set
  Type Γ = ∃ λ i → Env Γ → U i

  Env : Ctxt → Set
  Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (proj₂ σ γ)

mutual

  data Ctxt⁺ (Γ : Ctxt) : Set where
    _▻_ : (Γ⁺ : Ctxt⁺ Γ) → Type (Γ ++ Γ⁺) → Ctxt⁺ Γ

  infixl 5 _++_

  _++_ : (Γ : Ctxt) → Ctxt⁺ Γ → Ctxt
  Γ ++ (Γ⁺ ▻ σ) = (Γ ++ Γ⁺) ▻ σ

data P : (Γ : Ctxt) → Type Γ → Set where
  c : ∀ {Γ σ τ} → P (Γ ▻ σ) τ

f : ∀ {Γ} → Ctxt⁺ Γ → Set₁
f {Γ} (Γ⁺ ▻ σ) = Set
  where
  g : ∀ τ → P (Γ ++ Γ⁺ ▻ σ) τ → Set₁
  g _ c = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Binary where

data Bit : Set where
  O : Bit
  I : Bit

infixl 80 _<<_

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

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

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

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

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

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

infixl 60 _+_
infix  40 _==_

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

{-
test : (<<I << I << O << O << O) == (<<I << I << O << I) + (<<I << O << I << I)
test = refl
-}

{-
simple : (<<I << O) == (<<I) + (<<I)
simple = refl
-}

{-
t : Peano _
t = peano (<<I)
-}

{-
t : Pos
t = bsuc (<<I)
-}

{-
t : Pos
t = peano (<<I << O) <+> (<<I << I)
-- t = psuc pI <+> (<<I)
  where
    _<+>_ : {n : Pos} -> Peano n -> Pos -> Pos
    pI     <+> m = bsuc m
    psuc p <+> m = bsuc (p <+> m)
-}

t1 : Pos
t1 = (<<I << O) + (<<I << O)

t2 : (<<I) + (<<I) == (<<I) + (<<I)
t2 = refl

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
-- Sets represented by unary predicates (Like restricted comprehension)
-- Similiar to BoolSet, but instead using the builtin constructive logic with levels.
module Sets.PredicateSet where

import      Lvl
open import Data hiding (Empty)
open import Data.Boolean
open import Data.Boolean.Stmt
open import Functional
open import Function.Proofs
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
-- open import Relator.Equals.Proofs.Equiv
open import Structure.Setoid using (Equiv) renaming (_≡_ to _≡ₛ_)
open import Data.Any
open import Structure.Function.Domain
open import Type

module _ where
  -- A set of objects of a certain type.
  -- This is represented by a predicate.
  -- Note: This is only a "set" within a certain type, so everything PredSet(T) is actually a subset of T (if T were a set (the set of all objects with type T)). Or in other words: PredSet(T) is supposed to represent the set {x. x: T}, and then (S ∈ PredSet(T)) essentially means that S when interpreted as a set of objects is a subset of {x. x: T}.
  PredSet : ∀{ℓ ℓₒ} → Type{ℓₒ} → Type{Lvl.𝐒(ℓ) Lvl.⊔ ℓₒ}
  PredSet{ℓ}{ℓₒ} (T) = (T → Stmt{ℓ})

  private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓₒ ℓₑ : Lvl.Level
  private variable T A B : Type{ℓₒ}

  -- The statement of whether an element is in a set
  -- TODO: Maybe define this using a equivalence relation instead? (Alternatively a Setoid: x ∈ S = ∃(y ↦ (x ≡_T y) ∧ S(y)))
  _∈_ : T → PredSet{ℓ}(T) → Stmt
  _∈_ = apply -- (x ∈ S) = S(x)

  _∉_ : T → PredSet{ℓ}(T) → Stmt
  _∉_ = (¬_) ∘₂ (_∈_) -- (x ∉ S) = ¬(x ∈ S)

  _∋_ : PredSet{ℓ}(T) → T → Stmt
  _∋_ = swap(_∈_) -- (S ∋ x) = (x ∈ S)

  _∌_ : PredSet{ℓ}(T) → T → Stmt
  _∌_ = (¬_) ∘₂ (_∋_) -- (S ∌ x) = ¬(S ∋ x)

  module BoundedQuantifiers {T : Type{ℓₒ}} where
    ∀ₛ : PredSet{ℓ}(T) → (T → Stmt{ℓ₁}) → Stmt{ℓ Lvl.⊔ ℓ₁ Lvl.⊔ ℓₒ}
    ∀ₛ(S) P = ∀{elem : T} → (elem ∈ S) → P(elem)

    ∃ₛ : PredSet{ℓ}(T) → (T → Stmt{ℓ₁}) → Stmt{ℓ Lvl.⊔ ℓ₁ Lvl.⊔ ℓₒ}
    ∃ₛ(S) P = ∃(elem ↦ (elem ∈ S) ∧ P(elem))

  -- An empty set
  ∅ : PredSet{ℓ}(T)
  ∅ = const(Data.Empty)

  -- An universal set
  -- Note: It is only within a certain type, so 𝐔{T} is not actually a subset of everything. It is the greatest subset of subsets of T.
  𝐔 : PredSet{ℓ}(T)
  𝐔 = const(Unit)

  -- A singleton set (a set with only one element)
  •_ : ⦃ Equiv{ℓₑ}(T) ⦄ → T → PredSet(T)
  •_ = (_≡ₛ_)

  -- An union of two sets
  _∪_ : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → PredSet(T)
  _∪_ S₁ S₂ x = (S₁(x) ∨ S₂(x))

  -- An union of a set and a singleton set
  _∪•_ : ∀{ℓ}{T : Type{ℓ}} → PredSet{ℓ₁}(T) → Type{ℓ} → PredSet(T)
  _∪•_ S P x = (S(x) ∨ P)

  -- An intersection of two sets
  _∩_ : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → PredSet(T)
  _∩_ S₁ S₂ x = (S₁(x) ∧ S₂(x))

  -- A complement of a set
  ∁_ : PredSet{ℓ}(T) → PredSet(T)
  ∁_ = (¬_) ∘_ -- ∁_ S x = (¬ S(x))

  _∖_ : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → PredSet(T)
  _∖_ S₁ S₂ = (S₁ ∩ (∁ S₂))

  filter : (T → Bool) → PredSet{ℓ}(T) → PredSet(T)
  filter f S x = (S(x) ∧ IsTrue(f(x)))

  -- TODO: Maybe move these to a separate "Relations" file?

  -- A statement of whether a set is a subset of a set
  _⊆_ : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → Stmt
  _⊆_ S₁ S₂ = (∀{x} → (x ∈ S₁) → (x ∈ S₂))

  -- A statement of whether a set is a superset of a set
  _⊇_ : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → Stmt
  _⊇_ S₁ S₂ = (∀{x} → (x ∈ S₁) ← (x ∈ S₂))

  -- A statement of whether a set is equivalent to a set
  _≡_ : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → Stmt
  _≡_ S₁ S₂ = (∀{x} → (x ∈ S₁) ↔ (x ∈ S₂))

  Empty : PredSet{ℓ}(T) → Stmt
  Empty(S) = ∀{x} → ¬(x ∈ S)

  NonEmpty : PredSet{ℓ}(T) → Stmt
  NonEmpty(S) = ∃(_∈ S)

  Disjoint : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → Stmt
  Disjoint S₁ S₂ = ((S₁ ∩ S₂) ⊆ (∅ {Lvl.𝟎}))

  Overlapping : PredSet{ℓ₁}(T) → PredSet{ℓ₂}(T) → Stmt
  Overlapping S₁ S₂ = ∃(S₁ ∩ S₂)

  ⋃_ : PredSet{ℓ₁}(PredSet{ℓ₂}(T)) → PredSet(T)
  ⋃_ S x = ∃(s ↦ (s ∈ S) ∧ (x ∈ s))

  ⋂_ : PredSet{ℓ₁}(PredSet{ℓ₂}(T)) → PredSet(T)
  ⋂_ S x = ∀{s} → (s ∈ S) → (x ∈ s)

  ℘ : PredSet{ℓ₁}(T) → PredSet(PredSet{ℓ₁}(T))
  ℘ S x = x ⊆ S

  unapply : ⦃ Equiv{ℓₑ}(B) ⦄ → (f : A → B) → B → PredSet(A)
  unapply f(y) x = f(x) ≡ₛ y

  map : ⦃ Equiv{ℓₑ}(B) ⦄ → (f : A → B) → PredSet{ℓ}(A) → PredSet(B)
  map f(S) y = Overlapping(S)(unapply f(y))

  unmap : (f : A → B) → PredSet{ℓ}(B) → PredSet(A)
  unmap f(y) x = f(x) ∈ y

  ⊶ : ⦃ Equiv{ℓₑ}(B) ⦄ → (f : A → B) → PredSet(B)
  ⊶ f y = ∃(unapply f(y))

  module _ where -- TODO: These proofs should be generalized somewhere else?
    open import Structure.Relator.Equivalence
    open import Structure.Relator.Properties

    private variable S a b c a₁ a₂ b₁ b₂ : PredSet{ℓ}(T)
    private variable S₁ : PredSet{ℓ₁}(T)
    private variable S₂ : PredSet{ℓ₂}(T)

    instance
      [≡]-reflexivity : Reflexivity(_≡_ {ℓ₁}{ℓ₂}{T})
      Reflexivity.proof [≡]-reflexivity = [↔]-reflexivity

    instance
      [≡]-symmetry : Symmetry(_≡_ {ℓ₁}{ℓ₂}{T})
      Symmetry.proof [≡]-symmetry {x} {y} xy = [↔]-symmetry xy

    instance
      [≡]-transitivity : Transitivity(_≡_ {ℓ₁}{ℓ₂}{T})
      Transitivity.proof [≡]-transitivity {x} {y} {z} xy yz = [↔]-transitivity xy yz

    instance
      [≡]-equivalence : Equivalence(_≡_ {ℓ₁}{ℓ₂}{T})
      [≡]-equivalence = intro

    {- TODO: Cannot be an instance of Equiv because of level issues, but see a solution in ExtensionalPredicateSet
    instance
      [≡]-equiv : Equiv(PredSet{ℓ}(T))
      Equiv._≡_ [≡]-equiv = {!_≡_!}
      Equiv.equivalence [≡]-equiv = {![≡]-equivalence!}
    -}

    [≡]-to-[⊆] : (S₁ ≡ S₂) → (S₁ ⊆ S₂)
    [≡]-to-[⊆] S₁S₂ {x} = [↔]-to-[→] (S₁S₂{x})

    [≡]-to-[⊇] : (S₁ ≡ S₂) → (S₁ ⊇ S₂)
    [≡]-to-[⊇] S₁S₂ {x} = [↔]-to-[←] (S₁S₂{x})

    [⊆]-of-[∪]ₗ : (S₁ ⊆ (S₁ ∪ S₂))
    [⊆]-of-[∪]ₗ = [∨]-introₗ

    [⊆]-of-[∪]ᵣ : (S₂ ⊆ (S₁ ∪ S₂))
    [⊆]-of-[∪]ᵣ = [∨]-introᵣ

    [∪]-of-subset : (S₁ ⊆ S₂) → ((S₁ ∪ S₂) ≡ S₂)
    [∪]-of-subset S₁S₂ = [↔]-intro [∨]-introᵣ ([∨]-elim S₁S₂ id)

    [⊆]-min : (∅ {ℓ} ⊆ S)
    [⊆]-min = empty

    [⊆]-max : (S ⊆ 𝐔 {ℓ})
    [⊆]-max = const <>

    [∅]-containment : ∀{x : T} → ¬(x ∈ ∅ {ℓ})
    [∅]-containment = empty

    [𝐔]-containment : ∀{x : T} → (x ∈ 𝐔 {ℓ})
    [𝐔]-containment = <>

    map-containmentₗ : ⦃ equiv-B : Equiv{ℓₑ}(B) ⦄ → ∀{x : A}{f : A → B} → (f(x) ∈ map ⦃ equiv-B ⦄ f(S)) ← (x ∈ S)
    map-containmentₗ {x = x} = (xS ↦ [∃]-intro x ⦃ [↔]-intro xS (reflexivity(_≡ₛ_)) ⦄)

    -- map-containmentᵣ : ⦃ _ : Relation(S) ⦄ → ∀{f : A → B} → ⦃ _ : Injective(f) ⦄ → ∀{x : A} → (f(x) ∈ map f(S)) → (x ∈ S)
    -- map-containmentᵣ {x = x} = ([∃]-intro a ⦃ [∧]-intro p q ⦄) ↦ {!!}

    [⋂]-of-[∅] : ((⋂_ {ℓ₁}{ℓ₂} ∅) ≡ 𝐔 {ℓ₃}{ℓ₄}{T})
    [⋂]-of-[∅] = [↔]-intro (const empty) (const <>)

    [⋂]-of-[𝐔] : ((⋂_ {ℓ₁}{ℓ₂} 𝐔) ≡ ∅ {ℓ₂}{ℓ₃}{T})
    [⋂]-of-[𝐔] {ℓ₁}{ℓ₂}{ℓ₃}{T} = [↔]-intro empty (inters ↦ inters([𝐔]-containment{x = ∅ {ℓ₂}{ℓ₃}{T}}))

    [⋃]-of-[∅] : ((⋃_ {ℓ₁}{ℓ₂} ∅) ≡ ∅ {ℓ₁}{ℓ₃}{T})
    [⋃]-of-[∅] = [↔]-intro empty (([∃]-intro s ⦃ [∧]-intro p _ ⦄) ↦ p)

    [⋃]-of-[𝐔] : ((⋃_ {ℓ₁}{ℓ₂} 𝐔) ≡ 𝐔 {ℓ₃}{ℓ₄}{T})
    [⋃]-of-[𝐔] {ℓ₁}{ℓ₂}{ℓ₃}{T} = [↔]-intro (const ([∃]-intro 𝐔 ⦃ [↔]-intro <> <> ⦄)) (const <>)

    LvlUp-set-equality : (Lvl.Up{ℓ} ∘ S ≡ S)
    LvlUp-set-equality = [↔]-intro Lvl.up Lvl.Up.obj

    -- Disjoint-irreflexivity : ⦃ _ : NonEmpty(_) ⦄ → Irreflexivity(Disjoint{ℓ₁}{ℓ₂}{T})
    -- Irreflexivity.proof Disjoint-irreflexivity p = {!!}

    -- TODO: Duplicated in SetLike
    -- SetType : PredSet{ℓ}(T) → Stmt
    -- SetType(s) = ∃(_∈ s)

    {-
    choice : ∀{S : PredSet{ℓ₁}(PredSet{ℓ₂}(T))} → ∃{Obj = SetType(S) → SetType(⋃ S)}(f ↦ ∀{([∃]-intro x) : SetType(S)} → ([∃]-witness(f([∃]-intro x)) ∈ x))
    ∃.witness (∃.witness (choice {S = S}) ([∃]-intro f ⦃ proof ⦄)) = {!!}
    ∃.proof   (∃.witness (choice {S = S}) ([∃]-intro f ⦃ proof ⦄)) = {!!}
    ∃.proof              (choice {S = S}) {[∃]-intro f ⦃ proof ⦄}  = {!!}
    -}

    [∪]-subset : (a ⊆ c) → (b ⊆ c) → ((a ∪ b) ⊆ c)
    [∪]-subset ac bc = [∨]-elim ac bc

    [∪]-subset2 : (a₁ ⊆ a₂) → (b₁ ⊆ b₂) → ((a₁ ∪ b₁) ⊆ (a₂ ∪ b₂))
    [∪]-subset2 aa bb = [∨]-elim2 aa bb

    [∖][∪]-is-[∪]ᵣ : (((a ∖ b) ∪ b) ⊆ (a ∪ b))
    [∖][∪]-is-[∪]ᵣ {a = A}{b = B}{x = x} = [∨]-elim ([∨]-introₗ ∘ [∧]-elimₗ) [∨]-introᵣ

    open import Logic.Classical
    [∖][∪]-is-[∪] : ⦃ ∀{x} → Classical(b(x)) ⦄ → (((a ∖ b) ∪ b) ≡ (a ∪ b))
    [∖][∪]-is-[∪] {b = B}{a = A}{x = x} = [↔]-intro
      ([∨]-elim (Ax ↦ [∨]-elim2 ([∧]-intro Ax) id ([∨]-symmetry(excluded-middle(B(x))))) [∨]-introᵣ)
      ([∖][∪]-is-[∪]ᵣ {a = A}{b = B})

    [∪][∖]-invertᵣ-[⊆] : (a ⊆ (b ∪ c)) → ((a ∖ c) ⊆ b)
    [∪][∖]-invertᵣ-[⊆] abc ([∧]-intro a nc) = [∨]-elim id ([⊥]-elim ∘ nc) (abc a)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

module Number.Structures where

private
  variable
    ℓ ℓ' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base -- Rel

-- open import Data.Nat.Base using (ℕ) renaming (_≤_ to _≤ₙ_)
open import Cubical.Data.Nat using (ℕ; zero; suc) renaming (_+_ to _+ₙ_)
open import Cubical.Data.Nat.Order renaming (zero-≤ to z≤n; suc-≤-suc to s≤s; _≤_ to _≤ₙ_; _<_ to _<ₙ_)

open import Cubical.Data.Unit.Base -- Unit
open import Cubical.Data.Empty -- ⊥
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
open import Cubical.Data.Maybe.Base

import MoreAlgebra
open MoreAlgebra.Definitions

import Algebra.Structures

-- ℕ ℤ ℚ ℝ ℂ and ℚ₀⁺ ℝ₀⁺ ...
-- ring without additive inverse
-- see Algebra.Structures.IsCommutativeSemiring
record IsRCommSemiring {F : Type ℓ} (_#_ : Rel F F ℓ') (0f 1f : F) (_+_ _·_ : F → F → F) : Type (ℓ-max ℓ ℓ') where
  field
    isApartnessRel : IsApartnessRel _#_
    -- TODO: properties

  open IsApartnessRel isApartnessRel public
    renaming
      ( isIrrefl  to #-irrefl
      ; isSym     to #-sym
      ; isCotrans to #-cotrans )

-- ℤ ℚ ℝ ℂ
-- see Algebra.Structures.IsCommutativeRing
record IsRCommRing {F : Type ℓ} (_#_ : Rel F F ℓ') (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) : Type (ℓ-max ℓ ℓ') where
  field
    isRCommSemiring : IsRCommSemiring _#_ 0f 1f _+_ _·_

  open IsRCommSemiring isRCommSemiring public

-- ℚ ℝ ℂ
record IsRField {F : Type ℓ} (_#_ : Rel F F ℓ') (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_⁻¹ : (x : F) → {{ x # 0f }} → F) : Type (ℓ-max ℓ ℓ') where
  field
    isRCommRing : IsRCommRing _#_ 0f 1f _+_ _·_ -_
    +-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
    +-comm  : ∀ x y   →       x + y ≡ y + x
    distrib : ∀ x y z → (x + y) · z ≡ (x · z) + (y · z)
    ⁻¹-preserves-#0 : ∀ x → (p : x # 0f) → _⁻¹ x {{p}} # 0f
    -preserves-#  : ∀ x y → x # y  → (- x) # (- y)
    -preserves-#0 : ∀ x   → x # 0f → (- x) #    0f
    ·-#0-#0-implies-#0 : ∀ a b → a  # 0f →  b # 0f → (a · b) #    0f
    1#0 : 1f # 0f
    -- TODO: properties

  open IsRCommRing isRCommRing public

-- Finₖ ℕ ℤ ℚ ℝ and ℚ₀⁺ ℚ⁺ ℝ₀⁺ ℝ⁺ ...
record IsRLattice {F : Type ℓ} (_<_ _≤_ _#_ : Rel F F ℓ') (min max : F → F → F) : Type (ℓ-max ℓ ℓ') where
  field
    isPartialOrder : IsPartialOrder _≤_
    glb      : ∀ x y z → z ≤ min x y → z ≤ x × z ≤ y
    glb-back : ∀ x y z → z ≤ x × z ≤ y → z ≤ min x y
    lub      : ∀ x y z → max x y ≤ z → x ≤ z × y ≤ z
    lub-back : ∀ x y z → x ≤ z × y ≤ z → max x y ≤ z

    -- TODO: derived properties
    <-implies-# : ∀ x y → x < y → x # y
    ≤-#-implies-< : ∀ x y → x ≤ y → x # y → x < y
    #-sym : ∀ x y → x # y → y # x
    max-sym : ∀ x y → max x y ≡ max y x
    max-id : ∀ x → max x x ≡ x

  open IsPartialOrder isPartialOrder public

-- ℕ ℤ ℚ ℝ and ℚ₀⁺ ℚ⁺ ℝ₀⁺ ℝ⁺ ...
-- ring without additive inverse
record IsROrderedCommSemiring {F : Type ℓ} (_<_ _≤_ _#_ : Rel F F ℓ') (min max : F → F → F) (0f 1f : F) (_+_ _·_ : F → F → F) : Type (ℓ-max ℓ ℓ') where
  field
    isRLattice : IsRLattice _<_ _≤_ _#_ min max
    isRCommSemiring : IsRCommSemiring _#_ 0f 1f _+_ _·_
    -- TODO: properties
    -- TODO: the following can be derived
    0<1 : 0f < 1f
    +-0<-0<-implies-0< : ∀ a b → 0f <  a → 0f <  b →    0f   < (a + b)
    +-0<-0≤-implies-0< : ∀ a b → 0f <  a → 0f ≤  b →    0f   < (a + b)
    +-0≤-0<-implies-0< : ∀ a b → 0f ≤  a → 0f <  b →    0f   < (a + b)
    +-0≤-0≤-implies-0≤ : ∀ a b → 0f ≤  a → 0f ≤  b →    0f   ≤ (a + b)
    +-<0-<0-implies-<0 : ∀ a b →  a < 0f →  b < 0f → (a + b) <    0f
    +-<0-≤0-implies-<0 : ∀ a b →  a < 0f →  b ≤ 0f → (a + b) <    0f
    +-≤0-<0-implies-<0 : ∀ a b →  a ≤ 0f →  b < 0f → (a + b) <    0f
    +-≤0-≤0-implies-≤0 : ∀ a b →  a ≤ 0f →  b ≤ 0f → (a + b) ≤    0f

    ·-#0-#0-implies-#0 : ∀ a b → a  # 0f →  b # 0f → (a · b) #    0f
    ·-#0-0<-implies-#0 : ∀ a b → a  # 0f → 0f < b  → (a · b) #    0f
    ·-#0-<0-implies-#0 : ∀ a b → a  # 0f →  b < 0f → (a · b) #    0f
    ·-0≤-0≤-implies-0≤ : ∀ a b → 0f ≤  a → 0f ≤ b  →    0f   ≤ (a · b)
    ·-0≤-0<-implies-0≤ : ∀ a b → 0f ≤  a → 0f < b  →    0f   ≤ (a · b)
    ·-0≤-<0-implies-≤0 : ∀ a b → 0f ≤  a →  b < 0f → (a · b) ≤    0f
    ·-0≤-≤0-implies-≤0 : ∀ a b → 0f ≤  a →  b ≤ 0f → (a · b) ≤    0f
    ·-0<-#0-implies-#0 : ∀ a b → 0f <  a →  b # 0f → (a · b) #    0f
    ·-0<-0≤-implies-0≤ : ∀ a b → 0f <  a → 0f ≤ b  →    0f   ≤ (a · b)
    ·-0<-0<-implies-0< : ∀ a b → 0f <  a → 0f < b  →    0f   < (a · b)
    ·-0<-<0-implies-<0 : ∀ a b → 0f <  a →  b < 0f → (a · b) <    0f
    ·-0<-≤0-implies-≤0 : ∀ a b → 0f <  a →  b ≤ 0f → (a · b) ≤    0f
    ·-<0-#0-implies-#0 : ∀ a b → a  < 0f →  b # 0f → (a · b) #    0f
    ·-<0-0≤-implies-≤0 : ∀ a b → a  < 0f → 0f ≤ b  → (a · b) ≤    0f
    ·-<0-0<-implies-<0 : ∀ a b → a  < 0f → 0f < b  → (a · b) <    0f
    ·-<0-<0-implies-0< : ∀ a b → a  < 0f →  b < 0f →    0f   < (a · b)
    ·-<0-≤0-implies-0≤ : ∀ a b → a  < 0f →  b ≤ 0f →    0f   ≤ (a · b)
    ·-≤0-0≤-implies-≤0 : ∀ a b → a  ≤ 0f → 0f ≤ b  → (a · b) ≤    0f
    ·-≤0-0<-implies-≤0 : ∀ a b → a  ≤ 0f → 0f < b  → (a · b) ≤    0f
    ·-≤0-<0-implies-0≤ : ∀ a b → a  ≤ 0f →  b < 0f →    0f   ≤ (a · b)
    ·-≤0-≤0-implies-0≤ : ∀ a b → a  ≤ 0f →  b ≤ 0f →    0f   ≤ (a · b)

    0≤-#0-implies-0< : ∀ x → 0f ≤ x → x # 0f → 0f < x

    {-
    ·-#0-#0-implies-#0 : ∀ a b → a  # 0f → b  # 0f → (a · b) #    0f
    ·-#0-0<-implies-#0 : ∀ a b → a  # 0f → 0f < b  → (a · b) #    0f
    ·-0≤-0≤-implies-0≤ : ∀ a b → 0f ≤ a  → 0f ≤ b  →    0f   ≤ (a · b)
    ·-0≤-0<-implies-0≤ : ∀ a b → 0f ≤ a  → 0f < b  →    0f   ≤ (a · b)
    ·-0≤-≤0-implies-≤0 : ∀ a b → 0f ≤ a  → b  ≤ 0f → (a · b) ≤    0f
    ·-0<-#0-implies-#0 : ∀ a b → 0f < a  → b  # 0f → (a · b) #    0f
    ·-0<-0≤-implies-0≤ : ∀ a b → 0f < a  → 0f ≤ b  →    0f   ≤ (a · b)
    ·-0<-0<-implies-0< : ∀ a b → 0f < a  → 0f < b  →    0f   < (a · b)
    ·-0<-≤0-implies-≤0 : ∀ a b → 0f < a  → b  ≤ 0f → (a · b) ≤    0f
    ·-≤0-0≤-implies-≤0 : ∀ a b → a  ≤ 0f → 0f ≤ b  → (a · b) ≤    0f
    ·-≤0-0<-implies-≤0 : ∀ a b → a  ≤ 0f → 0f < b  → (a · b) ≤    0f
    ·-≤0-≤0-implies-0≤ : ∀ a b → a  ≤ 0f → b  ≤ 0f →    0f   ≤ (a · b)
    -}

  open IsRLattice isRLattice public

-- ℤ ℚ ℝ
record IsROrderedCommRing {F : Type ℓ} (_<_ _≤_ _#_ : Rel F F ℓ') (min max : F → F → F) (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) : Type (ℓ-max ℓ ℓ') where
  field
    isROrderedCommSemiring : IsROrderedCommSemiring _<_ _≤_ _#_ min max 0f 1f _+_ _·_
    isRCommRing : IsRCommRing _#_ 0f 1f _+_ _·_ -_
    0≡-0 : 0f ≡ - 0f
    -flips-<  : ∀ x y → x  < y  → (- y) < (- x)
    -flips-<0 : ∀ x   → x  < 0f →    0f < (- x)
    -flips-0< : ∀ x   → 0f < x  → (- x) <    0f
    -flips-≤  : ∀ x y → x  ≤ y  → (- y) ≤ (- x)
    -flips-≤0 : ∀ x   → x  ≤ 0f →    0f ≤ (- x)
    -flips-0≤ : ∀ x   → 0f ≤ x  → (- x) ≤    0f
    -preserves-#  : ∀ x y → x # y  → (- x) # (- y)
    -preserves-#0 : ∀ x   → x # 0f → (- x) #    0f
    -- TODO: properties

  open IsROrderedCommSemiring isROrderedCommSemiring public

-- Remark 6.7.7. As we define absolute values by | x | = max(x, -x), as is common in constructive analysis,
-- if x has a locator, then so does | x |, and we use this fact in the proof of the above theorem.

-- Remark 4.1.9.
--
-- 1. From the fact that (A, ≤, min, max) is a lattice, it does not follow that
-- for every x and y,
--
--   max(x, y) = x  ∨  max(x, y) = y,
--
-- which would hold in a linear order.
-- However, in Lemma 6.7.1 we characterize max as
--
--   z < max(x, y) ⇔ z < x ∨ z < y,
--
-- and similarly for min.

{- from: https://isabelle.in.tum.de/doc/tutorial.pdf "8.4.5 The Numeric Type Classes"

  Absolute Value.

  The absolute value function `abs` is available for all ordered rings, including types int, rat and real.
  It satisfies many properties, such as the following:

    | x * y | ≡ | x | * | y |         (abs_mult)

    | a | ≤ b ⇔ (a ≤ b) ∧ (- a) ≤ b   (abs_le_iff)

    | a + b | ≤ | a | + | b |         (abs_triangle_ineq)
-}

-- also see https://en.wikipedia.org/wiki/Ordered_ring#Basic_properties

record IsAbsOrderedCommRing {F : Type ℓ} (_<_ _≤_ _#_ : Rel F F ℓ') (min max : F → F → F) (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (abs : F → F) : Type (ℓ-max ℓ ℓ') where
  field
    abs0≡0          :         abs 0f ≡ 0f
    abs-preserves-· : ∀ x y → abs (x · y) ≡ abs x · abs y
    triangle-ineq   : ∀ x y → abs (x + y) ≤ (abs x + abs y)
    -- -trichotomy     : ∀ x → (x ≡ 0f) ⊎ (0f < x) ⊎ (0f < (- x))
    abs-≤           : ∀ x y → abs x ≤ y → (x ≤ y) × ((- x) ≤ y)
    abs-≤-back      : ∀ x y → (x ≤ y) × ((- x) ≤ y) → abs x ≤ y
    0≤abs           : ∀ x   → 0f ≤ abs x

-- ℚ ℝ
record IsROrderedField {F : Type ℓ} (_<_ _≤_ _#_ : Rel F F ℓ') (min max : F → F → F) (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_⁻¹ : (x : F) → {{ x # 0f }} → F) : Type (ℓ-max ℓ ℓ') where
  field
    isROrderedCommRing : IsROrderedCommRing _<_ _≤_ _#_ min max 0f 1f _+_ _·_ -_
    isRField           : IsRField _#_ 0f 1f _+_ _·_ -_ _⁻¹
    -- TODO: properties

  open IsROrderedCommRing isROrderedCommRing hiding
    ( -preserves-#
    ; -preserves-#0
    ) public
  open IsRField isRField hiding
    ( ·-#0-#0-implies-#0
    ) public

  field
    ⁻¹-preserves-<0 : ∀ x → (x < 0f) → (p : x # 0f) → _⁻¹ x {{p}} < 0f
    ⁻¹-preserves-0< : ∀ x → (0f < x) → (p : x # 0f) → 0f < _⁻¹ x {{p}}

-- ℚ₀⁺ ℚ₀⁻ ℝ₀⁺ ℝ₀⁻
{-
record IsROrderedSemifield {F : Type ℓ} (_<_ _≤_ _#_ : Rel F F ℓ') (min max : F → F → F) (0f 1f : F) (_+_ _·_ : F → F → F) (_⁻¹ : (x : F) → {{ x < 0f }} → F) : Type (ℓ-max ℓ ℓ') where
  field
    isROrderedCommSemiring : IsROrderedCommSemiring _<_ _≤_ _#_ min max 0f 1f _+_ _·_
    -- TODO: properties
    #0-implies-0< : ∀ x → 0f # x → 0f < x
    positivity : ∀ x → 0f ≤ x
  open IsROrderedCommSemiring isROrderedCommSemiring public
-}

-- ℚ⁺ ℚ⁻ ℝ⁺ ℝ⁻
{-
record IsROrderedSemifieldWithoutZero {F : Type ℓ} (_<_ _≤_ _#_ : Rel F F ℓ') (min max : F → F → F) (0f 1f : F) (_+_ _·_ : F → F → F) (_⁻¹ : (x : F) → F) : Type (ℓ-max ℓ ℓ') where
  field
    isRLattice : IsRLattice _<_ _≤_ _#_ min max
    -- isGroup : IsGroup 1f _·_ _⁻¹
    +-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
    +-comm  : ∀ x y → x + y ≡ y + x
    distrib : ∀ x y z → (x + y) · z ≡ (x · z) + (y · z)
    -- TODO: properties
  open IsRLattice isRLattice public

-}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{-# OPTIONS --without-K #-}
module Chapter3.Formalization where

-- Sets and n-types
-- ----------------

open import Data.Unit
open import Data.Empty
open import Data.Nat
open import Data.Sum
open import Relation.Nullary using (¬_)
open import Data.Bool
open import Data.Product

open import Basics
open import Relation.Equivalence.Univalence
open import Relation.Equality
open import Relation.Equality.Extensionality
open import Relation.Path.Operation

isSet : ∀ {a} → Set a → Set a
isSet A = (x y : A) (p q : x ≡ y) → p ≡ q

-- The only possible inhabitants of ⊤ is tt which means everything
-- is reflexivity.
is-1-set : isSet ⊤
is-1-set tt tt refl refl = refl

-- Ex falso quodlibet strikes again
is-0-set : isSet ⊥
is-0-set ()

hasDecEq : ∀ {i} → Set i → Set i
hasDecEq A = (x y : A) → (x ≡ y) ⊎ ¬ (x ≡ y)

decEqIsSet : ∀ {i}{A : Set i} → hasDecEq A → isSet A
decEqIsSet {A} d x y = {!   !} -- TBD: Hedberg's Theorem

-- Natural numbers are also a set because every equality type is decidable.
-- Boy, it's a pain in the ass proving that, though.
is-ℕ-set : isSet ℕ
is-ℕ-set = decEqIsSet hasDecEq-ℕ where
  hasDecEq-ℕ : hasDecEq ℕ
  hasDecEq-ℕ zero zero = inj₁ refl
  hasDecEq-ℕ zero (suc y) = inj₂ (λ ())
  hasDecEq-ℕ (suc x) zero = inj₂ (λ ())
  hasDecEq-ℕ (suc x) (suc y) with hasDecEq-ℕ x y
  hasDecEq-ℕ (suc x) (suc y) | inj₁ x₁ = inj₁ (ap {f = suc} x₁)
  hasDecEq-ℕ (suc x) (suc y) | inj₂ pnot = inj₂ (λ p → pnot (ap {f = remark} p)) where
    remark : ℕ → ℕ
    remark zero = 42
    remark (suc n) = n

is-×-set : ∀ {a b}{A : Set a}{B : Set b} → isSet A → isSet B → isSet (A × B)
is-×-set SA SB x y p q = {!   !}

is-1-type : ∀ {a} → Set a → Set a
is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s

3-1-8 : ∀ {a}{A : Set a} → isSet A → is-1-type A
3-1-8 f x y p q r s = {! apd r  !}
  where
    g : (q : x ≡ y) → (p ≡ q)
    g q = f x y p q

3-1-9 : ¬ (isSet Set)
3-1-9 x = {!   !} where
  f : Bool → Bool
  f false = true
  f true = false

  contra : ¬ (false ≡ true)
  contra ()

  lem : IsEquiv f
  lem = record
    { from = f
    ; iso₁ = λ x → mlem {x}
    ; iso₂ = λ x → mlem {x}
    } where
    mlem : ∀ {x : Bool} → f (f x) ≡ x
    mlem {false} = refl
    mlem {true} = refl

not-double-neg : ∀ {A : Set} → (¬ (¬ A) → A) → ⊥
not-double-neg f = {!  !} where
  e : Bool ≃ Bool
  e = e-equiv , record { from = e-equiv ; iso₁ = λ x → helper {x} ; iso₂ = λ x → helper {x} } where
    e-equiv : Bool → Bool
    e-equiv true = false
    e-equiv false = true

    helper : ∀ {x : Bool} → e-equiv (e-equiv x) ≡ x
    helper {true} = refl
    helper {false} = refl

  -- 3-2-4 : (x : Bool) → ¬ (e x ≡ x)
  -- 3-2-4 = ?

  p : Bool ≡ Bool
  p = {! ua e  !}

not-lem : ∀ {A : Set} → ¬ (A ⊎ (¬ A))
not-lem {A} (inj₁ x) = not-double-neg (λ _ → x)
not-lem {A} (inj₂ w) = not-double-neg (λ x → ⊥-elim (x w))

-- This defines "mere propositions"
-- If all elements of P are connected by a path, then p contains no
-- higher homotopy.
--
-- "The adjective “mere” emphasizes that although any type may be regarded as a
-- proposition (which we prove by giving an inhabitant of it), a type that is a
-- mere proposition cannot usefully be regarded as any more than a proposition:
-- there is no additional information contained in a witness of its truth."
isProp : ∀ {a} → Set a → Set a
isProp P = (x y : P) → (x ≡ y)

top-is-prop : isProp ⊤
top-is-prop tt tt = refl

3-3-3 : ∀ {a b}{P : Set a}{Q : Set b} → (p : isProp P)(q : isProp Q) → (f : P → Q) → (g : Q → P) → P ≃ Q
3-3-3 p q f g = f , record
                      { from = g
                      ; iso₁ = λ x → p (g (f x)) x
                      ; iso₂ = λ y → q (f (g y)) y
                      }

3-3-2 : ∀ {a}{P : Set a} → (p : isProp P) → (x₀ : P) → P ≃ ⊤
3-3-2 {_}{P} p x₀ = 3-3-3 p (top-is-prop) f g where
  f : P → ⊤
  f x = tt

  g : ⊤ → P
  g u = x₀

isProp-isSet : ∀ {a}{A : Set a} → isProp A → isSet A
isProp-isSet {_}{A} f x y p q = lem p ∙ lem q ⁻¹ where
  g : (y : A) → x ≡ y
  g y = f x y

  -- Read bottom-to-top
  lem : (p : x ≡ y) → p ≡ (g x ⁻¹ ∙ g y)
  lem p = (ap {f = (λ z → z ∙ p)} (back-and-there-again {p = (g x)}) ⁻¹) -- we have p = g(x)−1   g(y) = q.
        ∙ (assoc (g x ⁻¹) (g x) p ⁻¹) -- and after a little convincing
        ∙ ap {f = (λ z → (g x ⁻¹) ∙ z)} -- which is to say that p = g(y)⁻¹ ∙ g(z)
          ( (2-11-2 x p (g x) ⁻¹) -- Hence by Lemma 2.11.2, we have g(y) ∙ p = g(z)
          ∙ (apd {f = g} p) -- we have apd(p) : p(g(y)) = g(z).
          ) -- Then for any y,z : A and p : y = z

isProp-is-prop : ∀ {a}{A : Set a} → isProp (isProp A)
isProp-is-prop f g = funext λ x →
                     funext λ y → isProp-isSet f _ _ (f x y) (g x y)

isSet-is-prop : ∀ {a}{A : Set a} → isProp (isSet A)
isSet-is-prop f g = funext λ x →
                    funext λ y →
                    funext λ p →
                    funext λ q → isProp-isSet (f x y) _ _ (f x y p q) (g x y p q)

3-5-1 : ∀ {a}{A : Set a} → (P : A → Set) → ({x : A} → isProp (P x)) → (u v : Σ[ x ∈ A ] P x) → (proj₁ u ≡ proj₁ v) → u ≡ v
3-5-1 P x u v p = {!   !}

3-6-1 : ∀ {a b}{A : Set a}{B : Set b} → (isProp A) → (isProp B) → isProp (A × B)
3-6-1 PA PB px py = {!   !}

3-6-2 : ∀ {a b}{A : Set a}{B : A → Set b}{x : A} → (isProp (B x)) → isProp ((x : A) → B x)
3-6-2 PPI f g = funext λ x → {! f x ≡ g x  !}

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


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

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

data D (A : Set) : Set where
  c c' : D A

postulate rew : c {Bool} ≡ c' {Bool}

{-# REWRITE rew #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Relation.Binary.PropositionalEquality

record Group : Set₁ where
  field
    X : Set
    _·_ : X → X → X
    e : X
    i : X → X
    assoc  : (x y z : X) → (x · y) · z ≡ x · (y · z)
    unit-l : (x : X) → e · x ≡ x
    unit-r : (x : X) → x · e ≡ x
    inv-l  : (x : X) → i x · x ≡ e
    inv-r  : (x : X) → x · i x ≡ e

inv-u-l : {G : Group} → (x x' y : Group.X) → (x Group.· y) ≡ Group.e → (x' Group.· y) ≡ Group.e → x ≡ x'
inv-u-l x x' y p q = ?

max_stars_repo_name: erwinkn/program-eq-proof

max_issues_repo_name: erwinkn/program-eq-proof

max_forks_repo_name: erwinkn/program-eq-proof


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Direct-Sum.Properties where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup

open import Cubical.Algebra.Direct-Sum.Base

private variable
  ℓ ℓ' : Level

module _ (Idx : Type ℓ) (P : Idx → Type ℓ') (AGP : (r : Idx) → AbGroupStr (P r)) where

  inv : ⊕ Idx P AGP → ⊕ Idx P AGP
  inv = DS-Rec-Set.f Idx P AGP (⊕ Idx P AGP) trunc
           -- elements
           neutral
           (λ r a → base r (AbGroupStr.-_ (AGP r) a))
           (λ xs ys → xs add ys)
           -- eq group
           (λ xs ys zs → addAssoc xs ys zs)
           (λ xs → addRid xs)
           (λ xs ys → addComm xs ys)
           -- eq base
           (λ r → let open AbGroupStr (AGP r) in
                   let open GroupTheory (P r , AbGroupStr→GroupStr (AGP r)) in
                   (cong (base r) inv1g) ∙ (base-neutral r))
           (λ r a b → let open AbGroupStr (AGP r) in
                       let open GroupTheory (P r , AbGroupStr→GroupStr (AGP r)) in
                       ((base r (- a) add base r (- b))   ≡⟨ (base-add r (- a) (- b)) ⟩
                       base r ((- a) + (- b))             ≡⟨ (cong (base r) (sym (invDistr b a))) ⟩
                       base r (- (b + a))                 ≡⟨ cong (base r) (cong (-_) (comm b a)) ⟩
                       base r (- (a + b)) ∎))

  rinv : (z : ⊕ Idx P AGP) → z add (inv z) ≡ neutral
  rinv = DS-Ind-Prop.f Idx P AGP (λ z → z add (inv z) ≡ neutral) (λ _ → trunc _ _)
         -- elements
         (addRid neutral)
         (λ r a → let open AbGroupStr (AGP r) in
                        ((base r a add base r (- a)) ≡⟨ base-add r a (- a) ⟩
                        base r (a + - a)             ≡⟨ cong (base r) (invr a) ⟩
                        base r 0g                    ≡⟨ base-neutral r ⟩
                        neutral ∎))
         (λ {x} {y} p q →
                        (((x add y) add ((inv x) add (inv y)))   ≡⟨ cong (λ X → X add ((inv x) add (inv y))) (addComm x y) ⟩
                        ((y add x) add (inv x add inv y))        ≡⟨ sym (addAssoc y x (inv x add inv y)) ⟩
                        (y add (x add (inv x add inv y)))        ≡⟨ cong (λ X → y add X) (addAssoc x (inv x) (inv y)) ⟩
                        (y add ((x add inv x) add inv y))        ≡⟨ cong (λ X → y add (X add (inv y))) (p) ⟩
                        (y add (neutral add inv y))              ≡⟨ cong (λ X → y add X) (addComm neutral (inv y)) ⟩
                        (y add (inv y add neutral))              ≡⟨ cong (λ X → y add X) (addRid (inv y)) ⟩
                        (y add inv y)                            ≡⟨ q ⟩
                        neutral ∎))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module Structure.Setoid.Uniqueness.Proofs where

import      Lvl
open import Functional
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid.Uniqueness
open import Structure.Setoid
open import Structure.Function.Domain
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable A B : Type{ℓ}
private variable P : A → Type{ℓ}

module _ ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ {f : A → B} where
  Uniqueness-Injectivity : (∀{y : B} → Unique(x ↦ y ≡ f(x))) ↔ Injective(f)
  Uniqueness-Injectivity = [↔]-intro l r where
    l : (∀{y : B} → Unique(x ↦ y ≡ f(x))) ← Injective(f)
    l inj {y} {x₁}{x₂} (y≡fx₁) (y≡fx₂) = injective _ ⦃ inj ⦄ {x₁}{x₂} (symmetry(_≡_) (y≡fx₁) 🝖 (y≡fx₂))

    r : (∀{y : B} → Unique(x ↦ y ≡ f(x))) → Injective(f)
    Injective.proof(r unique) {x₁}{x₂} (fx₁≡fx₂) = unique {f(x₁)}{x₁}{x₂} (reflexivity(_≡_)) (fx₁≡fx₂)


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFlattening
open import lib.types.Span
open import lib.types.Unit

-- Wedge of two pointed types is defined as a particular case of pushout

module lib.types.Wedge where

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

  wedge-span : Span
  wedge-span = span (fst X) (fst Y) Unit (λ _ → snd X) (λ _ → snd Y)

  Wedge : Type (lmax i j)
  Wedge = Pushout wedge-span

  _∨_ = Wedge

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  winl : fst X → X ∨ Y
  winl x = left x

  winr : fst Y → X ∨ Y
  winr y = right y

  wglue : winl (snd X) == winr (snd Y)
  wglue = glue tt

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

  ⊙Wedge : Ptd (lmax i j)
  ⊙Wedge = ⊙[ Wedge X Y , winl (snd X) ]

  _⊙∨_ = ⊙Wedge

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  ⊙winl : fst (X ⊙→ X ⊙∨ Y)
  ⊙winl = (winl , idp)

  ⊙winr : fst (Y ⊙→ X ⊙∨ Y)
  ⊙winr = (winr , ! wglue)

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  module WedgeElim {k} {P : X ∨ Y → Type k}
    (winl* : (x : fst X) → P (winl x)) (winr* : (y : fst Y) → P (winr y))
    (wglue* : winl* (snd X) == winr* (snd Y) [ P ↓ wglue ]) where

    private
      module M = PushoutElim winl* winr* (λ _ → wglue*)

    f = M.f
    glue-β = M.glue-β unit

  open WedgeElim public using () renaming (f to Wedge-elim)

  module WedgeRec {k} {C : Type k} (winl* : fst X → C) (winr* : fst Y → C)
    (wglue* : winl* (snd X) == winr* (snd Y)) where

    private
      module M = PushoutRec {d = wedge-span X Y} winl* winr* (λ _ → wglue*)

    f = M.f
    glue-β = M.glue-β unit

add-wglue : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → fst (X ⊙⊔ Y) → X ∨ Y
add-wglue (inl x) = winl x
add-wglue (inr y) = winr y

⊙add-wglue : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → fst (X ⊙⊔ Y ⊙→ X ⊙∨ Y)
⊙add-wglue = (add-wglue , idp)

module Fold {i} {X : Ptd i} =
  WedgeRec {X = X} {Y = X} (λ x → x) (λ x → x) idp

fold = Fold.f

⊙fold : ∀ {i} {X : Ptd i} → fst (X ⊙∨ X ⊙→ X)
⊙fold = (fold , idp)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
-- {-# OPTIONS -v impossible:100 -v tc.lhs.imp:100 #-}
-- {-# OPTIONS -v impossible:100 -v tc.cover:20 #-}
-- {-# OPTIONS --copatterns #-} -- Andreas, 2015-08-26 on by default.
module Issue957 where

open import Common.Equality

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

pair : {A B : Set} → A → B → A × B
fst (pair a b) = ?
snd (pair a b) = ?

swap : {A B : Set} → A × B → B × A
fst (swap p) = ?
snd (swap p) = ?

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
fst (swap3 t)       = ?
fst (snd (swap3 t)) = ?
snd (snd (swap3 t)) = ?

-- should also work if we shuffle the clauses
swap4 : {A B C D : Set} → A × (B × (C × D)) → D × (C × (B × A))
fst (snd (swap4 t))       = ?
snd (snd (snd (swap4 t))) = ?
fst (swap4 t)             = ?
fst (snd (snd (swap4 t))) = ?

-- multiple clauses with abstractions

fswap3 : {A B C X : Set} → (X → A) × ((X → B) × C) → (X → C) × (X → (B × A))
fst (fswap3 t) x       = ?
fst (snd (fswap3 t) y) = ?
snd (snd (fswap3 t) z) = ?

-- State monad example

-- The State newtype

record State (S A : Set) : Set where
  constructor state
  field
    runState : S → A × S
open State

-- The Monad type class

record Monad (M : Set → Set) : Set1 where
  constructor monad
  field
    return : {A : Set}   → A → M A
    _>>=_  : {A B : Set} → M A → (A → M B) → M B

module InstanceArgument where

  open Monad {{...}}

  -- State is an instance of Monad

  instance
    stateMonad : {S : Set} → Monad (State S)
    runState (return {{stateMonad}} a  ) s  = ?
    runState (_>>=_  {{stateMonad}} m k) s₀ = ?


text:
module Logic where

open import Type renaming (Type to Stmt ; Typeω to Stmtω) public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Equality.Setoid directly.
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid)

module Data.List.Relation.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where

open import Data.List.Relation.Binary.Equality.Setoid S public


text:
------------------------------------------------------------------------
-- A variant of Coherently with an erased field
------------------------------------------------------------------------

{-# OPTIONS --cubical --guardedness #-}

import Equality.Path as P

module Lens.Non-dependent.Higher.Coherently.Coinductive.Erased
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

import Equality.Path.Univalence as EPU
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as B using (_↔_)
import Bijection P.equality-with-J as PB
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence P.equality-with-J as PEq
open import Equivalence.Erased equality-with-J as EEq using (_≃ᴱ_)
open import Function-universe equality-with-J hiding (_∘_)
import Function-universe P.equality-with-J as PF
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹; ∥∥¹ᴱ→∥∥¹)
open import H-level.Truncation.Propositional.One-step.Erased eq as OE
  using (∥_∥¹ᴱ)
open import Univalence-axiom equality-with-J
import Univalence-axiom P.equality-with-J as PU

open import Lens.Non-dependent.Higher.Coherently.Coinductive eq as C
  using (Coherently)

private
  variable
    a b ℓ p p₁ p₂ : Level
    A A₁ A₂ B C   : Type a
    x y           : A
    f             : A → B

-- A variant of
-- Lens.Non-dependent.Higher.Coherently.Coinductive.Coherently with an
-- erased "coherent" field.

record Coherentlyᴱ
         {A : Type a} {B : Type b}
         (P : {A : Type a} → (A → B) → Type p)
         (@0 step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ᴱ → B)
         (f : A → B) : Type p where
  coinductive
  field
    property    : P f
    @0 coherent : Coherentlyᴱ P step (step f property)

open Coherentlyᴱ public

-- A preservation lemma for Coherentlyᴱ. (See also Coherentlyᴱ-cong
-- below.)

@0 Coherentlyᴱ-cong′ :
  {P : {A : Type a} → (A → B) → Type p}
  {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ᴱ → B} →
  Univalence a →
  (A₁≃A₂ : A₁ ≃ A₂) →
  Coherentlyᴱ P step (f ∘ _≃_.to A₁≃A₂) ≃ Coherentlyᴱ P step f
Coherentlyᴱ-cong′ {f = f} {P = P} {step = step} univ A₁≃A₂ =
  ≃-elim₁ univ
    (λ A₁≃A₂ →
       Coherentlyᴱ P step (f ∘ _≃_.to A₁≃A₂) ≃
       Coherentlyᴱ P step f)
    Eq.id
    A₁≃A₂

-- Coherently can be converted to Coherentlyᴱ in a certain way
-- (assuming univalence).

Coherently→Coherentlyᴱ :
  {P : {A : Type a} → (A → B) → Type p}
  {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B} →
  @0 Univalence a →
  Coherently P step f → Coherentlyᴱ P (λ f p → step f p ∘ ∥∥¹ᴱ→∥∥¹) f
Coherently→Coherentlyᴱ _    c .property = c .C.property
Coherently→Coherentlyᴱ univ c .coherent =
  Coherently→Coherentlyᴱ univ
    (_≃_.from (C.Coherently-cong′ univ O.∥∥¹ᴱ≃∥∥¹)
       (c .C.coherent))

-- In erased contexts Coherently and Coherentlyᴱ are, in a certain
-- sense, logically equivalent (assuming univalence).

@0 Coherentlyᴱ⇔Coherently :
  {P : {A : Type a} → (A → B) → Type p}
  {step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ → B} →
  Univalence a →
  Coherentlyᴱ P (λ f p → step f p ∘ ∥∥¹ᴱ→∥∥¹) f ⇔ Coherently P step f
Coherentlyᴱ⇔Coherently univ ._⇔_.from = Coherently→Coherentlyᴱ univ

Coherentlyᴱ⇔Coherently univ ._⇔_.to c .C.property = c .property
Coherentlyᴱ⇔Coherently univ ._⇔_.to c .C.coherent =
  Coherentlyᴱ⇔Coherently univ ._⇔_.to
    (_≃_.to (Coherentlyᴱ-cong′ univ O.∥∥¹ᴱ≃∥∥¹)
       (c .coherent))

private

  -- A preservation lemma for Coherentlyᴱ.
  --
  -- The lemma does not use the univalence argument, instead it uses
  -- EPU.univ (and EPU.≃⇒≡) directly.

  Coherentlyᴱ-cong-≡ :
    Block "Coherentlyᴱ-cong-≡" →
    {A : Type a}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ᴱ → B}
    {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ᴱ → B}
    {f : A → B} →
    Univalence p →
    (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f) →
    ({A : Type a} (f : A → B) (x : P₂ f) →
     step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x) →
    Coherentlyᴱ P₁ step₁ f P.≡ Coherentlyᴱ P₂ step₂ f
  Coherentlyᴱ-cong-≡
    {a = a} {B = B} {p = p} ⊠ {P₁ = P₁} {P₂ = P₂}
    {step₁ = step₁} {step₂ = step₂} {f = f} _ P₁≃P₂′ step₁≡step₂ =

    P.cong (λ ((P , step) :
              ∃ λ (P : (A : Type a) → (A → B) → Type p) →
                  {A : Type a} (f : A → B) → P A f → ∥ A ∥¹ᴱ → B) →
             Coherentlyᴱ (P _) step f) $

    Σ-≡,≡→≡′

      (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) →
       EPU.≃⇒≡ (P₁≃P₂ f))

      (P.implicit-extensionality P.ext λ A → P.⟨ext⟩ λ f →
         P.subst (λ P → {A : Type a} (f : A → B) → P A f → ∥ A ∥¹ᴱ → B)
           (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) →
            EPU.≃⇒≡ (P₁≃P₂ f))
           step₁ f                                                       P.≡⟨ P.trans (P.cong (_$ f) $ P.sym $
                                                                                P.push-subst-implicit-application
                                                                                (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) → EPU.≃⇒≡ (P₁≃P₂ f))
                                                                                (λ P A → (f : A → B) → P A f → ∥ A ∥¹ᴱ → B)
                                                                                {f = const _} {g = step₁}) $
                                                                              P.sym $ P.push-subst-application
                                                                                (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) → EPU.≃⇒≡ (P₁≃P₂ f))
                                                                                (λ P f → P A f → ∥ A ∥¹ᴱ → B)
                                                                                {f = const f} {g = step₁} ⟩
         P.subst (λ P → P A f → ∥ A ∥¹ᴱ → B)
           (P.⟨ext⟩ λ A → P.⟨ext⟩ λ (f : A → B) →
            EPU.≃⇒≡ (P₁≃P₂ f))
           (step₁ f)                                                     P.≡⟨⟩

         P.subst (λ P → P → ∥ A ∥¹ᴱ → B)
           (EPU.≃⇒≡ (P₁≃P₂ f))
           (step₁ f)                                                     P.≡⟨ P.sym $
                                                                              PU.transport-theorem
                                                                                (λ P → P → ∥ A ∥¹ᴱ → B)
                                                                                (PF.→-cong₁ _)
                                                                                (λ _ → P.refl)
                                                                                EPU.univ
                                                                                (P₁≃P₂ f)
                                                                                (step₁ f) ⟩
         PF.→-cong₁ _ (P₁≃P₂ f) (step₁ f)                                P.≡⟨⟩

         step₁ f ∘ PEq._≃_.from (P₁≃P₂ f)                                P.≡⟨ P.⟨ext⟩ (_↔_.to ≡↔≡ ∘ step₁≡step₂ f) ⟩∎

         step₂ f                                                         ∎)
    where
    P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f PEq.≃ P₂ f
    P₁≃P₂ f = _↔_.to ≃↔≃ (P₁≃P₂′ f)

    Σ-≡,≡→≡′ :
      {P : A → Type b} {p₁ p₂ : Σ A P} →
      (p : proj₁ p₁ P.≡ proj₁ p₂) →
      P.subst P p (proj₂ p₁) P.≡ proj₂ p₂ →
      p₁ P.≡ p₂
    Σ-≡,≡→≡′ {P = P} {p₁ = _ , y₁} {p₂ = _ , y₂} p q i =
      p i , lemma i
      where
      lemma : P.[ (λ i → P (p i)) ] y₁ ≡ y₂
      lemma = PB._↔_.from (P.heterogeneous↔homogeneous _) q

  -- A "computation rule".

  to-Coherentlyᴱ-cong-≡-property :
    (bl : Block "Coherentlyᴱ-cong-≡")
    {A : Type a} {B : Type b}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ᴱ → B}
    {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ᴱ → B}
    {f : A → B}
    (univ : Univalence p)
    (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f)
    (step₁≡step₂ :
       {A : Type a} (f : A → B) (x : P₂ f) →
       step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x)
    (c : Coherentlyᴱ P₁ step₁ f) →
    PU.≡⇒→ (Coherentlyᴱ-cong-≡ bl univ P₁≃P₂ step₁≡step₂) c .property
      P.≡
    _≃_.to (P₁≃P₂ f) (c .property)
  to-Coherentlyᴱ-cong-≡-property
    ⊠ {P₁ = P₁} {P₂ = P₂} {f = f} _ P₁≃P₂ step₁≡step₂ c =

    P.transport (λ _ → P₂ f) P.0̲
      (_≃_.to (P₁≃P₂ f) (P.transport (λ _ → P₁ f) P.0̲ (c .property)))  P.≡⟨ P.cong (_$ _≃_.to (P₁≃P₂ f)
                                                                                (P.transport (λ _ → P₁ f) P.0̲ (c .property))) $
                                                                            P.transport-refl P.0̲ ⟩

    _≃_.to (P₁≃P₂ f) (P.transport (λ _ → P₁ f) P.0̲ (c .property))      P.≡⟨ P.cong (λ g → _≃_.to (P₁≃P₂ f) (g (c .property))) $
                                                                            P.transport-refl P.0̲ ⟩∎
    _≃_.to (P₁≃P₂ f) (c .property)                                     ∎

  -- Another "computation rule".

  from-Coherentlyᴱ-cong-≡-property :
    (bl : Block "Coherentlyᴱ-cong-≡")
    {A : Type a} {B : Type b}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ᴱ → B}
    {step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ᴱ → B}
    {f : A → B}
    (univ : Univalence p)
    (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ P₂ f)
    (step₁≡step₂ :
       {A : Type a} (f : A → B) (x : P₂ f) →
       step₁ f (_≃_.from (P₁≃P₂ f) x) ≡ step₂ f x)
    (c : Coherentlyᴱ P₂ step₂ f) →
    PEq._≃_.from
      (PU.≡⇒≃ (Coherentlyᴱ-cong-≡ bl {step₁ = step₁} univ
                 P₁≃P₂ step₁≡step₂))
      c .property P.≡
    _≃_.from (P₁≃P₂ f) (c .property)
  from-Coherentlyᴱ-cong-≡-property
    ⊠ {P₁ = P₁} {P₂ = P₂} {f = f} _ P₁≃P₂ step₁≡step₂ c =

    P.transport (λ _ → P₁ f) P.0̲
      (_≃_.from (P₁≃P₂ f) (P.transport (λ _ → P₂ f) P.0̲ (c .property)))  P.≡⟨ P.cong (_$ _≃_.from (P₁≃P₂ f)
                                                                                (P.transport (λ _ → P₂ f) P.0̲ (c .property))) $
                                                                              P.transport-refl P.0̲ ⟩

    _≃_.from (P₁≃P₂ f) (P.transport (λ _ → P₂ f) P.0̲ (c .property))      P.≡⟨ P.cong (λ g → _≃_.from (P₁≃P₂ f) (g (c .property))) $
                                                                              P.transport-refl P.0̲ ⟩∎
    _≃_.from (P₁≃P₂ f) (c .property)                                     ∎

  -- A preservation lemma for Coherentlyᴱ.
  --
  -- The two directions of this equivalence compute the property
  -- fields in certain ways, see the "unit tests" below.
  --
  -- Note that P₁ and P₂ have to target the same universe. A more
  -- general result is given below (Coherentlyᴱ-cong).

  Coherentlyᴱ-cong-≃ᴱ :
    {A : Type a}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {@0 step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ᴱ → B}
    {@0 step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ᴱ → B}
    {f : A → B} →
    @0 Univalence p →
    (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ᴱ P₂ f) →
    @0 ({A : Type a} (f : A → B) (x : P₂ f) →
        step₁ f (_≃ᴱ_.from (P₁≃P₂ f) x) ≡ step₂ f x) →
    Coherentlyᴱ P₁ step₁ f ≃ᴱ Coherentlyᴱ P₂ step₂ f
  Coherentlyᴱ-cong-≃ᴱ
    {P₁ = P₁} {P₂ = P₂} {step₁ = step₁} {step₂ = step₂} {f = f}
    univ P₁≃P₂ step₁≡step₂ =

    block λ bl →
    EEq.[≃]→≃ᴱ
      (EEq.[proofs]
         (Eq.with-other-inverse
            (Eq.with-other-function
               (equiv bl)
               (to bl)
               (_↔_.from ≡↔≡ ∘ ≡to bl))
            (from bl)
            (_↔_.from ≡↔≡ ∘ ≡from bl)))

    where

    @0 equiv :
      Block "Coherentlyᴱ-cong-≡" →
      Coherentlyᴱ P₁ step₁ f ≃ Coherentlyᴱ P₂ step₂ f
    equiv bl =
      _↔_.from ≃↔≃ $ PU.≡⇒≃ $
      Coherentlyᴱ-cong-≡ bl univ (EEq.≃ᴱ→≃ ∘ P₁≃P₂) step₁≡step₂

    to :
      Block "Coherentlyᴱ-cong-≡" →
      Coherentlyᴱ P₁ step₁ f → Coherentlyᴱ P₂ step₂ f
    to _  c .property = _≃ᴱ_.to (P₁≃P₂ f) (c .property)
    to bl c .coherent =
      P.subst
        (Coherentlyᴱ P₂ step₂)
        (P.cong (step₂ f) $
         to-Coherentlyᴱ-cong-≡-property
           bl univ (EEq.≃ᴱ→≃ ∘ P₁≃P₂) step₁≡step₂ c) $
      _≃_.to (equiv bl) c .coherent

    @0 ≡to : ∀ bl c → _≃_.to (equiv bl) c P.≡ to bl c
    ≡to bl c i .property = to-Coherentlyᴱ-cong-≡-property
                             bl univ (EEq.≃ᴱ→≃ ∘ P₁≃P₂) step₁≡step₂ c i
    ≡to bl c i .coherent = lemma i
      where
      lemma :
        P.[ (λ i → Coherentlyᴱ P₂ step₂
                     (step₂ f (to-Coherentlyᴱ-cong-≡-property
                                 bl univ (EEq.≃ᴱ→≃ ∘ P₁≃P₂)
                                 step₁≡step₂ c i))) ]
          _≃_.to (equiv bl) c .coherent ≡
          P.subst
            (Coherentlyᴱ P₂ step₂)
            (P.cong (step₂ f) $
             to-Coherentlyᴱ-cong-≡-property
               bl univ (EEq.≃ᴱ→≃ ∘ P₁≃P₂) step₁≡step₂ c)
            (_≃_.to (equiv bl) c .coherent)
      lemma =
        PB._↔_.from (P.heterogeneous↔homogeneous _) P.refl

    from :
      Block "Coherentlyᴱ-cong-≡" →
      Coherentlyᴱ P₂ step₂ f → Coherentlyᴱ P₁ step₁ f
    from _  c .property = _≃ᴱ_.from (P₁≃P₂ f) (c .property)
    from bl c .coherent =
      P.subst
        (Coherentlyᴱ P₁ step₁)
        (P.cong (step₁ f) $
         from-Coherentlyᴱ-cong-≡-property
           bl univ (EEq.≃ᴱ→≃ ∘ P₁≃P₂) step₁≡step₂ c) $
      _≃_.from (equiv bl) c .coherent

    @0 ≡from : ∀ bl c → _≃_.from (equiv bl) c P.≡ from bl c
    ≡from bl c i .property = from-Coherentlyᴱ-cong-≡-property
                               bl univ (EEq.≃ᴱ→≃ ∘ P₁≃P₂)
                               step₁≡step₂ c i
    ≡from bl c i .coherent = lemma i
      where
      lemma :
        P.[ (λ i → Coherentlyᴱ P₁ step₁
                     (step₁ f (from-Coherentlyᴱ-cong-≡-property
                                 bl univ (EEq.≃ᴱ→≃ ∘ P₁≃P₂)
                                 step₁≡step₂ c i))) ]
          _≃_.from (equiv bl) c .coherent ≡
          P.subst
            (Coherentlyᴱ P₁ step₁)
            (P.cong (step₁ f) $
             from-Coherentlyᴱ-cong-≡-property
               bl univ (EEq.≃ᴱ→≃ ∘ P₁≃P₂) step₁≡step₂ c)
            (_≃_.from (equiv bl) c .coherent)
      lemma =
        PB._↔_.from (P.heterogeneous↔homogeneous _) P.refl

  -- Unit tests that ensure that Coherentlyᴱ-cong-≃ᴱ computes the
  -- property fields in certain ways.

  module _
    {A : Type a}
    {P₁ P₂ : {A : Type a} → (A → B) → Type p}
    {@0 step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ᴱ → B}
    {@0 step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ᴱ → B}
    {f : A → B}
    {@0 univ : Univalence p}
    {P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ᴱ P₂ f}
    {@0 step₁≡step₂ :
       {A : Type a} (f : A → B) (x : P₂ f) →
       step₁ f (_≃ᴱ_.from (P₁≃P₂ f) x) ≡ step₂ f x}
    where

    _ :
      {c : Coherentlyᴱ P₁ step₁ f} →
      _≃ᴱ_.to (Coherentlyᴱ-cong-≃ᴱ univ P₁≃P₂ step₁≡step₂) c .property ≡
      _≃ᴱ_.to (P₁≃P₂ f) (c .property)
    _ = refl _

    _ :
      {c : Coherentlyᴱ P₂ step₂ f} →
      _≃ᴱ_.from (Coherentlyᴱ-cong-≃ᴱ {step₁ = step₁} univ
                   P₁≃P₂ step₁≡step₂)
        c .property ≡
      _≃ᴱ_.from (P₁≃P₂ f) (c .property)
    _ = refl _

  -- A lemma involving Coherentlyᴱ and ↑.

  Coherentlyᴱ-↑ :
    {A : Type a}
    {P : {A : Type a} → (A → B) → Type p}
    {@0 step : {A : Type a} (f : A → B) → P f → ∥ A ∥¹ᴱ → B}
    {f : A → B} →
    Coherentlyᴱ (↑ ℓ ∘ P) ((_∘ lower) ∘ step) f ≃
    Coherentlyᴱ P step f
  Coherentlyᴱ-↑ {ℓ = ℓ} {P = P} {step = step} =
    Eq.↔→≃
      to
      from
      (_↔_.from ≡↔≡ ∘ to-from)
      (_↔_.from ≡↔≡ ∘ from-to)
    where
    to :
      Coherentlyᴱ (↑ ℓ ∘ P) ((_∘ lower) ∘ step) f →
      Coherentlyᴱ P step f
    to c .property = lower (c .property)
    to c .coherent = to (c .coherent)

    from :
      Coherentlyᴱ P step f →
      Coherentlyᴱ (↑ ℓ ∘ P) ((_∘ lower) ∘ step) f
    from c .property = lift (c .property)
    from c .coherent = from (c .coherent)

    to-from :
      (c : Coherentlyᴱ P step f) →
      to (from c) P.≡ c
    to-from c i .property = c .property
    to-from c i .coherent = to-from (c .coherent) i

    from-to :
      (c : Coherentlyᴱ (↑ ℓ ∘ P) ((_∘ lower) ∘ step) f) →
      from (to c) P.≡ c
    from-to c i .property = c .property
    from-to c i .coherent = from-to (c .coherent) i

-- A preservation lemma for Coherentlyᴱ.
--
-- The two directions of this equivalence compute the property
-- fields in certain ways, see the "unit tests" below.

Coherentlyᴱ-cong :
  {A : Type a}
  {P₁ : {A : Type a} → (A → B) → Type p₁}
  {P₂ : {A : Type a} → (A → B) → Type p₂}
  {@0 step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ᴱ → B}
  {@0 step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ᴱ → B}
  {f : A → B} →
  @0 Univalence (p₁ ⊔ p₂) →
  (P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ᴱ P₂ f) →
  @0 ({A : Type a} (f : A → B) (x : P₂ f) →
      step₁ f (_≃ᴱ_.from (P₁≃P₂ f) x) ≡ step₂ f x) →
  Coherentlyᴱ P₁ step₁ f ≃ᴱ Coherentlyᴱ P₂ step₂ f
Coherentlyᴱ-cong
  {p₁ = p₁} {p₂ = p₂}
  {P₁ = P₁} {P₂ = P₂} {step₁ = step₁} {step₂ = step₂} {f = f}
  univ P₁≃P₂ step₁≡step₂ =

  Coherentlyᴱ P₁ step₁ f                          ↔⟨ inverse Coherentlyᴱ-↑ ⟩

  Coherentlyᴱ (↑ p₂ ∘ P₁) ((_∘ lower) ∘ step₁) f  ↝⟨ Coherentlyᴱ-cong-≃ᴱ
                                                       univ
                                                       (λ f →
    ↑ p₂ (P₁ f)                                           ↔⟨ B.↑↔ ⟩
    P₁ f                                                  ↝⟨ P₁≃P₂ f ⟩
    P₂ f                                                  ↔⟨ inverse B.↑↔ ⟩□
    ↑ p₁ (P₂ f)                                           □)
                                                       ((_∘ lower) ∘ step₁≡step₂) ⟩

  Coherentlyᴱ (↑ p₁ ∘ P₂) ((_∘ lower) ∘ step₂) f  ↔⟨ Coherentlyᴱ-↑ ⟩□

  Coherentlyᴱ P₂ step₂ f                          □

-- Unit tests that ensure that Coherentlyᴱ-cong computes the property
-- fields in certain ways.

module _
  {A : Type a}
  {P₁ : {A : Type a} → (A → B) → Type p₁}
  {P₂ : {A : Type a} → (A → B) → Type p₂}
  {@0 step₁ : {A : Type a} (f : A → B) → P₁ f → ∥ A ∥¹ᴱ → B}
  {@0 step₂ : {A : Type a} (f : A → B) → P₂ f → ∥ A ∥¹ᴱ → B}
  {f : A → B}
  {@0 univ : Univalence (p₁ ⊔ p₂)}
  {P₁≃P₂ : {A : Type a} (f : A → B) → P₁ f ≃ᴱ P₂ f}
  {@0 step₁≡step₂ :
     {A : Type a} (f : A → B) (x : P₂ f) →
     step₁ f (_≃ᴱ_.from (P₁≃P₂ f) x) ≡ step₂ f x}
  where

  _ :
    {c : Coherentlyᴱ P₁ step₁ f} →
    _≃ᴱ_.to (Coherentlyᴱ-cong univ P₁≃P₂ step₁≡step₂) c .property ≡
    _≃ᴱ_.to (P₁≃P₂ f) (c .property)
  _ = refl _

  _ :
    {c : Coherentlyᴱ P₂ step₂ f} →
    _≃ᴱ_.from (Coherentlyᴱ-cong {step₁ = step₁} univ P₁≃P₂ step₁≡step₂)
      c .property ≡
    _≃ᴱ_.from (P₁≃P₂ f) (c .property)
  _ = refl _

-- A "computation rule".

subst-Coherentlyᴱ-property :
  ∀ {B : Type b} {P : C → {A : Type a} → (A → B) → Type p}
    {@0 step : (c : C) {A : Type a} (f : A → B) → P c f → ∥ A ∥¹ᴱ → B}
    {f : C → A → B} {eq : x ≡ y} {c} →
  subst (λ x → Coherentlyᴱ (P x) (step x) (f x)) eq c .property ≡
  subst (λ x → P x (f x)) eq (c .property)
subst-Coherentlyᴱ-property
  {P = P} {step = step} {f = f} {eq = eq} {c = c} =
  elim¹
    (λ eq →
       subst (λ x → Coherentlyᴱ (P x) (step x) (f x)) eq c .property ≡
       subst (λ x → P x (f x)) eq (c .property))
    (subst (λ x → Coherentlyᴱ (P x) (step x) (f x)) (refl _) c .property  ≡⟨ cong property $ subst-refl _ _ ⟩
     c .property                                                          ≡⟨ sym $ subst-refl _ _ ⟩∎
     subst (λ x → P x (f x)) (refl _) (c .property)                       ∎)
    eq

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
postulate
  F    : (Set → Set) → Set
  !_   : Set → Set
  !_,_ : Set → Set → Set
  X    : Set

syntax F (λ X → A) = X , A

infix 1 F
infix 2 !_

Foo : Set
Foo = ! X , X

-- This expression can be parsed in exactly one way. However, Agda
-- rejects it:
--
--   Expected variable name in binding position
--
-- The error is thrown from pure code in rebuildBinding, and this
-- action circumvents the parser logic.
--
-- The error was introduced in the fix for Issue 1129, and the problem
-- raised in Issue 1129 was introduced in a fix for Issue 1108
-- ("Operator parser performance").


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

open import Algebra
open import Prelude
open import HITs.PropositionalTruncation
open import HITs.PropositionalTruncation.Sugar

module Algebra.Construct.Cayley {a} (mon : Monoid a) where

open Monoid mon

𝒞 : Type a
𝒞 = Σ[ f ⦂ (𝑆 → 𝑆) ] × ∀ x → ∥ f ε ∙ x ≡ f x ∥

⟦_⇓⟧ : 𝒞 → 𝑆
⟦ x ⇓⟧ = x .fst ε

⟦_⇑⟧ : 𝑆 → 𝒞
⟦ x ⇑⟧ .fst y = x ∙ y
⟦ x ⇑⟧ .snd y = ∣ cong (_∙ y) (∙ε x) ∣

ⓔ : 𝒞
ⓔ .fst x = x
ⓔ .snd x = ∣ ε∙ x ∣

open import Relation.Binary
open import HITs.PropositionalTruncation.Equivalence
open import Relation.Binary.Equivalence.Reasoning (trunc-equivalence (≡-equivalence {A = 𝑆}))

_⊙_ : 𝒞 → 𝒞 → 𝒞
(x ⊙ y) .fst z = x .fst (y .fst z)
(x ⊙ y) .snd z =
  x .fst (y .fst ε) ∙ z     ≋˘⟨ cong (_∙ z) ∥$∥ (x .snd (y .fst ε)) ⟩
  x .fst ε ∙ y .fst ε ∙ z   ≡⟨ assoc (x .fst ε) (y .fst ε) z ⟩
  x .fst ε ∙ (y .fst ε ∙ z) ≋⟨ cong (x .fst ε ∙_) ∥$∥ (y .snd z)  ⟩
  x .fst ε ∙ y .fst z       ≋⟨ x .snd (y .fst z) ⟩
  x .fst (y .fst z) ∎

⊙-assoc : Associative _⊙_
⊙-assoc x y z i .fst k = x .fst (y .fst (z .fst k))
⊙-assoc x y z i .snd k = squash (((x ⊙ y) ⊙ z) .snd k) ((x ⊙ (y ⊙ z)) .snd k) i

ⓔ⊙ : ∀ x → ⓔ ⊙ x ≡ x
ⓔ⊙ x i .fst y = x .fst y
ⓔ⊙ x i .snd y = squash ((ⓔ ⊙ x) .snd y) (x .snd y) i

⊙ⓔ : ∀ x → x ⊙ ⓔ ≡ x
⊙ⓔ x i .fst y = x .fst y
⊙ⓔ x i .snd y = squash ((x ⊙ ⓔ) .snd y) (x .snd y) i

cayleyMonoid : Monoid a
Monoid.𝑆 cayleyMonoid = 𝒞
Monoid._∙_ cayleyMonoid = _⊙_
Monoid.ε cayleyMonoid = ⓔ
Monoid.assoc cayleyMonoid = ⊙-assoc
Monoid.ε∙ cayleyMonoid = ⓔ⊙
Monoid.∙ε cayleyMonoid = ⊙ⓔ

open import Data.Sigma.Properties

module _ (sIsSet : isSet 𝑆) where
  𝒞-leftInv-fst : ∀ x y → ⟦ ⟦ x ⇓⟧ ⇑⟧ .fst y ≡ x .fst y
  𝒞-leftInv-fst x y = rec (sIsSet (x .fst ε ∙ y) (x .fst y)) id (x .snd y)

  𝒞-leftInv : ∀ x → ⟦ ⟦ x ⇓⟧ ⇑⟧ ≡ x
  𝒞-leftInv x = Σ≡Prop (λ f xs ys → funExt λ x → squash (xs x) (ys x)) (funExt (𝒞-leftInv-fst x))

  𝒞-iso : 𝒞 ⇔ 𝑆
  fun 𝒞-iso = ⟦_⇓⟧
  inv 𝒞-iso = ⟦_⇑⟧
  rightInv 𝒞-iso = ∙ε
  leftInv 𝒞-iso = 𝒞-leftInv

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Agda program using the Iowa Agda library
{-# OPTIONS --termination-depth=2 #-}

module PROOF-gamelength
  where

open import eq
open import bool
open import nat
open import nat-thms
open import list
open import nondet
open import nondet-thms

---------------------------------------------------------------------------
-- Translated Curry operations:

data Move : Set where
   L : Move
   R : Move

solve2 : ℕ → ℕ → ND (𝕃 Move)
solve2 zero    zero    = Val []
solve2 (suc x) zero    = mapND (_::_ L) (solve2 x zero)
solve2 zero    (suc y) = mapND (_::_ R) (solve2 zero y)
solve2 (suc z) (suc u) = (mapND (_::_ L) (solve2 z (suc u)))
                      ?? (mapND (_::_ R) (solve2 (suc z) u))

len : {a : Set} → 𝕃 a → ℕ
len [] = zero
len (x :: y) = suc (len y)

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

-- Theorem: the length of every solution is the sum of the input arguments
gamelength : (x : ℕ) → (y : ℕ)
              → (solve2 x y) satisfy (λ xs → length xs =ℕ x + y) ≡ tt
gamelength zero zero = refl
gamelength zero (suc y)
 rewrite
    satisfy-mapND (_::_ R) (solve2 zero y) (λ xs → length xs =ℕ zero + suc y)
  | gamelength zero y = refl
gamelength (suc x) zero
 rewrite
   satisfy-mapND (_::_ L) (solve2 x zero) (λ xs → length xs =ℕ suc x + zero)
 | gamelength x zero = refl
gamelength (suc x) (suc y)
 rewrite
  satisfy-mapND (_::_ L) (solve2 x (suc y)) (λ xs → length xs =ℕ suc x + suc y)
 | satisfy-mapND (_::_ R) (solve2 (suc x) y) (λ xs → length xs =ℕ suc x + suc y)
 | gamelength x (suc y)
 | +suc x y
 | gamelength (suc x) y
 = refl

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

max_stars_repo_name: phlummox/curry-tools

max_issues_repo_name: phlummox/curry-tools

max_forks_repo_name: phlummox/curry-tools


text:
module Equality where

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Product using (_×_; _,_; ∃-syntax; proj₁; proj₂)
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ)

--
-- Relation
--

record Relation (R : Set → Set) (A : Set) : Set where
  field
    relate : A × A → Bool
    to-witness : ∀ x → relate x ≡ true → R A
    from-witness : R A → ∃[ x ] (relate x ≡ true)
    to-from-witness : ∀ x d → x ≡ (proj₁ ∘ from-witness) (to-witness x d)

  Related : A × A → Set
  Related (x , y) = R A × relate (x , y) ≡ true

-- Properties

IsReflexive : ∀ R A (rel : Relation R A) → Set
IsReflexive R A rel = ∀ x → Related (x , x)
  where open Relation rel

IsSymmetric : ∀ R A (rel : Relation R A) → Set
IsSymmetric R A rel = ∀ x y → Related (x , y) → Related (y , x)
  where open Relation rel

IsTransitive : ∀ R A (rel : Relation R A) → Set
IsTransitive R A rel = ∀ x y z → Related (x , y) → Related (y , z) → Related (x , z)
  where open Relation rel

--
-- Equality
--

record Equality (E : Set → Set) (A : Set) : Set where
  field
    rel : Relation E A
    isReflexive  : IsReflexive  E A rel
    isSymmetric  : IsSymmetric  E A rel
    isTransitive : IsTransitive E A rel

--
-- SMT Equality
--

postulate
  -- datatype
  EqualitySMT : ∀ A → A → A → Set

  -- instances
  equalitySMT-Bool : Equality EqualitySMT Bool
  equalitySMT-ℕ    : Equality EqualitySMT ℕ

  -- eq-smt : (A : Set) (x y : A) → Bool

--
-- Propositional Equality
--

postulate
  eq-prop : ∀ (A : Set) (x y : A) → Bool

data EqualityProp : ∀ A → A → A → Set where
  injection-SMT :
    ∀ (A : Set) (equ : Equality EqualitySMT A) x y →
      Relation.Related EqualitySMT (x , y) →
      Relation.Related EqualityProp (x , y)
  -- extensional :
  --   ∀ (A B : Set) f g →
  --     (∀ x → EqualityProp


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic definitions for Characters
------------------------------------------------------------------------

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

module Data.Char.Base where

------------------------------------------------------------------------
-- Re-export the type, and renamed primitives

open import Agda.Builtin.Char public using ( Char )
  renaming
  -- testing
  ( primIsLower    to isLower
  ; primIsDigit    to isDigit
  ; primIsAlpha    to isAlpha
  ; primIsSpace    to isSpace
  ; primIsAscii    to isAscii
  ; primIsLatin1   to isLatin1
  ; primIsPrint    to isPrint
  ; primIsHexDigit to isHexDigit
  -- transforming
  ; primToUpper to toUpper
  ; primToLower to toLower
  -- converting
  ; primCharToNat to toNat
  ; primNatToChar to fromNat
  )

open import Agda.Builtin.String public using ()
  renaming ( primShowChar to show )


text:
open import Nat
open import Prelude
open import List
open import core
open import contexts

module lemmas-freevars where
  mutual
    -- if e successfully type-checks via analysis, under a context which
    -- can only bind x in the final position, then the free vars of e, with
    -- the context's last binder removed, cannot contain x.
    rff-lemma-ana : ∀{Γ x x' e τ₁ τ₂} → x # Γ → (Γ ,, (x' , τ₁)) ⊢ e <= τ₂ → x inList remove-from-free' x' e → ⊥
    rff-lemma-ana {_} {x} {x'} {e} h₁ h₂ h₃ with   natEQ x x'
    rff-lemma-ana {Γ} {x} {x'} {e} h₁ h₂ h₃      | Inl x==x'  = remove-all-not-in natEQ (free-vars e) x' (tr ( λ y → y inList remove-all natEQ (free-vars e) x') x==x' h₃)
    rff-lemma-ana {Γ} {x} {x'} {e} {τ₁} h₁ h₂ h₃ | Inr x≠x'   = a∉l→a∉remove-all-l-a' natEQ (fv-lemma-ana (lem-none-union {Γ = Γ} {τ₁} (flip x≠x') h₁) h₂) h₃

    -- as above
    rff-lemma-syn : ∀{Γ x x' e τ₁ τ₂} → x # Γ → (Γ ,, (x' , τ₁)) ⊢ e => τ₂ → x inList remove-from-free' x' e → ⊥
    rff-lemma-syn {Γ} {x} {x'} {e} h₁ h₂ h₃ with   natEQ x x'
    rff-lemma-syn {Γ} {x} {x'} {e} h₁ h₂ h₃      | Inl x==x'  = remove-all-not-in natEQ (free-vars e) x' (tr ( λ y → y inList remove-all natEQ (free-vars e) x') x==x' h₃)
    rff-lemma-syn {Γ} {x} {x'} {e} {τ₁} h₁ h₂ h₃ | Inr x≠x'   = a∉l→a∉remove-all-l-a' natEQ (fv-lemma-syn (lem-none-union {Γ = Γ} {τ₁} (flip x≠x') h₁) h₂) h₃

    -- if e analysizes against type under a context that doesn't mention x,
    -- x is not in free vars of e
    fv-lemma-ana : ∀{Γ x e τ} → x # Γ → Γ ⊢ e <= τ → x inList (free-vars e) → ⊥
    fv-lemma-ana h₁ (ASubsume x₁ x₂) = fv-lemma-syn h₁ x₁
    fv-lemma-ana {Γ} h₁ (ALam x₂ x₃ h₂) = rff-lemma-ana {Γ} h₁ h₂

    -- if e synthesizes a type under a context that doesn't mention x, x is
    -- not in free vars of e
    fv-lemma-syn : ∀{Γ x e τ} → x # Γ → Γ ⊢ e => τ → x inList (free-vars e) → ⊥
    fv-lemma-syn apt SConst ()
    fv-lemma-syn apt (SAsc x₁) = fv-lemma-ana apt x₁
    fv-lemma-syn apt (SVar x₂) InH = somenotnone (! x₂ · apt)
    fv-lemma-syn apt (SVar x₂) (InT ())
    fv-lemma-syn apt (SAp {e1 = e1} x₁ wt x₂ x₃) xin
      with inList++ {l1 = free-vars e1} natEQ xin
    ... | Inl x₄ = fv-lemma-syn apt wt x₄
    ... | Inr x₄ = fv-lemma-ana apt x₃ x₄
    fv-lemma-syn apt SEHole ()
    fv-lemma-syn apt (SNEHole x₁ wt) = fv-lemma-syn apt wt
    fv-lemma-syn {Γ} apt (SLam x₂ wt) xin = rff-lemma-syn {Γ} apt wt xin
    fv-lemma-syn apt (SFst wt x₁) = fv-lemma-syn apt wt
    fv-lemma-syn apt (SSnd wt x₁) = fv-lemma-syn apt wt
    fv-lemma-syn apt (SPair {e1 = e1} x₁ wt wt₁) xin
      with inList++ {l1 = free-vars e1} natEQ xin
    ... | Inl y = fv-lemma-syn apt wt y
    ... | Inr y = fv-lemma-syn apt wt₁ y

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
------------------------------------------------------------------------
-- A definitional interpreter that is instrumented with information
-- about the stack size of the compiled program
------------------------------------------------------------------------

open import Prelude

import Lambda.Syntax

module Lambda.Interpreter.Stack-sizes
  {Name : Type}
  (open Lambda.Syntax Name)
  (def : Name → Tm 1)
  where

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

open import Colist E.equality-with-J as C
open import Conat E.equality-with-J as Conat using (infinity)
open import Function-universe E.equality-with-J hiding (id; _∘_)
open import Monad E.equality-with-J
open import Nat E.equality-with-J
open import Vec.Data E.equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity as D using (later; force)

open import Upper-bounds

open import Lambda.Compiler def
open import Lambda.Delay-crash as DC hiding (crash)
open import Lambda.Delay-crash-trace as DCT hiding (tell)
import Lambda.Interpreter def as I

open Closure Tm
open Delay-crash-trace using (tell)

------------------------------------------------------------------------
-- The interpreter

-- A stack size change function used in the interpreter's call case.

δ : In-tail-context → ℕ → ℕ
δ tc = if tc then pred else id

infix 10 [_,_]_∙_

mutual

  -- The semantics instrumented with stack size changes (functions of
  -- type ℕ → ℕ). The semantics takes an argument of type
  -- In-tail-context, so that it can produce annotations matching
  -- those produced by the compiler + virtual machine.

  ⟦_⟧ :
    ∀ {i n} →
    Tm n → Env n → In-tail-context →
    Delay-crash-trace (ℕ → ℕ) Value i
  ⟦ var x ⟧       ρ _  = tell suc (return (index ρ x))
  ⟦ lam t ⟧       ρ _  = tell suc (return (lam t ρ))
  ⟦ t₁ · t₂ ⟧     ρ _  = do v₁ ← ⟦ t₁ ⟧ ρ false
                            v₂ ← ⟦ t₂ ⟧ ρ false
                            [ pred , pred ] v₁ ∙ v₂
  ⟦ call f t ⟧    ρ tc = do v ← ⟦ t ⟧ ρ false
                            [ δ tc , δ (not tc) ] lam (def f) [] ∙ v
  ⟦ con b ⟧       ρ _  = tell suc (return (con b))
  ⟦ if t₁ t₂ t₃ ⟧ ρ tc = do v₁ ← ⟦ t₁ ⟧ ρ false
                            ⟦if⟧ v₁ t₂ t₃ ρ tc

  [_,_]_∙_ :
    ∀ {i} →
    (ℕ → ℕ) → (ℕ → ℕ) →
    Value → Value → Delay-crash-trace (ℕ → ℕ) Value i
  [ f₁ , f₂ ] lam t₁ ρ ∙ v₂ = later f₁ λ { .force → do
                                v ← ⟦ t₁ ⟧ (v₂ ∷ ρ) true
                                tell f₂ (return v) }
  [ _  , _  ] con _    ∙ _  = crash

  ⟦if⟧ :
    ∀ {i n} →
    Value → Tm n → Tm n → Env n → In-tail-context →
    Delay-crash-trace (ℕ → ℕ) Value i
  ⟦if⟧ (lam _ _)   _  _  _ _  = crash
  ⟦if⟧ (con true)  t₂ t₃ ρ tc = tell pred (⟦ t₂ ⟧ ρ tc)
  ⟦if⟧ (con false) t₂ t₃ ρ tc = tell pred (⟦ t₃ ⟧ ρ tc)

-- The numbers produced by a given computation, for a given initial
-- number. The initial number is the first element in the output.

numbers : ∀ {A i} → Delay-crash-trace (ℕ → ℕ) A i → ℕ → Colist ℕ i
numbers x n = scanl (λ m f → f m) n (trace x)

-- The stack sizes, for an empty initial stack, with false as the
-- In-tail-context argument.
--
-- Note that this colist is not guaranteed to match the one generated
-- by the virtual machine exactly. However, they are guaranteed to
-- have the same least upper bound.

stack-sizes : ∀ {i} → Tm 0 → Colist ℕ i
stack-sizes t = numbers (⟦ t ⟧ [] false) 0

------------------------------------------------------------------------
-- The semantics given above gives the same (uninstrumented) result as
-- the one in Lambda.Interpreter

mutual

  -- The instrumented and the uninstrumented semantics yield strongly
  -- bisimilar results.

  ⟦⟧∼⟦⟧ :
    ∀ {i n} (t : Tm n) {ρ : Env n} tc →
    D.[ i ] delay-crash (⟦ t ⟧ ρ tc) ∼ I.⟦ t ⟧ ρ
  ⟦⟧∼⟦⟧ (var x) _ = D.reflexive _

  ⟦⟧∼⟦⟧ (lam t) _ = D.reflexive _

  ⟦⟧∼⟦⟧ (t₁ · t₂) {ρ} _ =
    delay-crash
      (⟦ t₁ ⟧ ρ false >>= λ v₁ → ⟦ t₂ ⟧ ρ false >>= λ v₂ →
       [ pred , pred ] v₁ ∙ v₂)                              D.∼⟨ delay-crash->>= (⟦ t₁ ⟧ _ _) ⟩

    (delay-crash (⟦ t₁ ⟧ ρ false) >>= λ v₁ →
     delay-crash (⟦ t₂ ⟧ ρ false >>= λ v₂ →
                  [ pred , pred ] v₁ ∙ v₂))                  D.∼⟨ ((delay-crash (⟦ t₁ ⟧ _ _) D.∎) DC.>>=-cong λ _ →
                                                                   delay-crash->>= (⟦ t₂ ⟧ _ _)) ⟩
    (delay-crash (⟦ t₁ ⟧ ρ false) >>= λ v₁ →
     delay-crash (⟦ t₂ ⟧ ρ false) >>= λ v₂ →
     delay-crash ([ pred , pred ] v₁ ∙ v₂))                  D.∼⟨ (⟦⟧∼⟦⟧ t₁ _ DC.>>=-cong λ v₁ → ⟦⟧∼⟦⟧ t₂ _ DC.>>=-cong λ _ → ∙∼∙ pred v₁) ⟩∼

    (I.⟦ t₁ ⟧ ρ >>= λ v₁ → I.⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ I.∙ v₂)  D.∎

  ⟦⟧∼⟦⟧ (call f t) {ρ} tc =
    delay-crash (⟦ t ⟧ ρ false >>= λ v →
                 [ _ , _ ] lam (def f) [] ∙ v)       D.∼⟨ delay-crash->>= (⟦ t ⟧ _ _) ⟩

    (delay-crash (⟦ t ⟧ ρ false) >>= λ v →
     delay-crash ([ δ tc , _ ] lam (def f) [] ∙ v))  D.∼⟨ (⟦⟧∼⟦⟧ t _ DC.>>=-cong λ _ → ∙∼∙ (δ tc) (lam (def f) [])) ⟩∼

    (I.⟦ t ⟧ ρ >>= λ v → lam (def f) [] I.∙ v)       D.∎

  ⟦⟧∼⟦⟧ (con b) _ = D.reflexive _

  ⟦⟧∼⟦⟧ (if t₁ t₂ t₃) {ρ} tc =
    (delay-crash (⟦ t₁ ⟧ ρ false >>= λ v₁ → ⟦if⟧ v₁ t₂ t₃ ρ tc))  D.∼⟨ delay-crash->>= (⟦ t₁ ⟧ _ _) ⟩

    (delay-crash (⟦ t₁ ⟧ ρ false) >>= λ v₁ →
     delay-crash (⟦if⟧ v₁ t₂ t₃ ρ tc))                            D.∼⟨ (⟦⟧∼⟦⟧ t₁ _ DC.>>=-cong λ v₁ → ⟦if⟧∼⟦if⟧ v₁ t₂ t₃ _) ⟩∼

    (I.⟦ t₁ ⟧ ρ >>= λ v₁ → I.⟦if⟧ v₁ t₂ t₃ ρ)                     D.∎

  ∙∼∙ :
    ∀ {i} f₁ {f₂} (v₁ {v₂} : Value) →
    D.[ i ] delay-crash ([ f₁ , f₂ ] v₁ ∙ v₂) ∼ v₁ I.∙ v₂
  ∙∼∙ f₁ {f₂} (lam t₁ ρ) {v₂} = later λ { .force →
    delay-crash (⟦ t₁ ⟧ (v₂ ∷ ρ) true >>= tell f₂ ∘ return)  D.∼⟨ delay-crash->>= (⟦ t₁ ⟧ _ _) ⟩

    delay-crash (⟦ t₁ ⟧ (v₂ ∷ ρ) true) >>=
    delay-crash ∘ tell f₂ ∘ return                           D.∼⟨ ((delay-crash (⟦ t₁ ⟧ _ _) D.∎) DC.>>=-cong λ _ → D.reflexive _) ⟩

    delay-crash (⟦ t₁ ⟧ (v₂ ∷ ρ) true) >>= return            D.∼⟨ DC.right-identity _ ⟩

    delay-crash (⟦ t₁ ⟧ (v₂ ∷ ρ) true)                       D.∼⟨ ⟦⟧∼⟦⟧ t₁ _ ⟩∼

    I.⟦ t₁ ⟧ (v₂ ∷ ρ)                                        D.∎ }

  ∙∼∙ _ (con _) = D.reflexive _

  ⟦if⟧∼⟦if⟧ :
    ∀ {i n} v₁ (t₂ t₃ : Tm n) {ρ} tc →
    D.[ i ] delay-crash (⟦if⟧ v₁ t₂ t₃ ρ tc) ∼ I.⟦if⟧ v₁ t₂ t₃ ρ
  ⟦if⟧∼⟦if⟧ (lam _ _)   _  _  _ = D.reflexive _
  ⟦if⟧∼⟦if⟧ (con true)  t₂ t₃ _ = ⟦⟧∼⟦⟧ t₂ _
  ⟦if⟧∼⟦if⟧ (con false) t₂ t₃ _ = ⟦⟧∼⟦⟧ t₃ _

------------------------------------------------------------------------
-- A lemma

-- The function numbers preserves strong bisimilarity.

numbers-cong :
  ∀ {i A} {x y : Delay-crash-trace (ℕ → ℕ) A ∞} {n} →
  DCT.[ i ] x ∼ y → C.[ i ] numbers x n ∼ numbers y n
numbers-cong = scanl-cong ∘ trace-cong

------------------------------------------------------------------------
-- An example: An analysis of the semantics of Ω

-- The semantics of Ω is the non-terminating computation never.

Ω-loops : ∀ {i} → D.[ i ] delay-crash (⟦ Ω ⟧ [] false) ∼ never
Ω-loops =
  delay-crash (⟦ Ω ⟧ [] false)  D.∼⟨ ⟦⟧∼⟦⟧ Ω false ⟩
  I.⟦ Ω ⟧ []                    D.∼⟨ I.Ω-loops ⟩
  never                         D.∎

-- A colist used in an analysis of the stack space usage of Ω.

Ω-sizes : ∀ {i} → ℕ → Colist ℕ i
Ω-sizes n =
  n ∷′ 1 + n ∷′ 2 + n ∷ λ { .force → Ω-sizes (1 + n) }

private

  -- An abbreviation.

  cong₃ :
    ∀ {i x y z} {xs ys : Colist′ ℕ ∞} →
    C.[ i ] force xs ∼′ force ys →
    C.[ i ] x ∷′ y ∷′ z ∷ xs ∼ x ∷′ y ∷′ z ∷ ys
  cong₃ p = E.refl ∷ λ { .force → E.refl ∷ λ { .force → E.refl ∷ p }}

-- The colist Ω-sizes n has the same upper bounds as nats-from n.

Ω-sizes≂nats-from : ∀ {i} n → [ i ] Ω-sizes n ≂ nats-from n
Ω-sizes≂nats-from n =
  Ω-sizes n                               ∼⟨ (cong₃ λ { .force → C.reflexive-∼ _ }) ⟩≂
  n ∷′ 1 + n ∷′ 2 + n ∷′ Ω-sizes (suc n)  ≂⟨ cons′-≂ (_⇔_.from ≂′⇔≂″ λ { .force →
                                             consˡ-≂ (inj₁ (here ≤-refl)) (
                                             consˡ-≂ (inj₁ (there (here ≤-refl))) (
                                             Ω-sizes≂nats-from (suc n))) }) ⟩∼
  n ∷′ nats-from (suc n)                  C.∼⟨ C.symmetric-∼ ∷∼∷′ ⟩
  nats-from n                             C.∎

-- The least upper bound of Ω-sizes 0 is infinity.

lub-Ω-sizes-0-infinity :
  LUB (Ω-sizes 0) infinity
lub-Ω-sizes-0-infinity =      $⟨ lub-nats-infinity ⟩
  LUB nats          infinity  ↝⟨ LUB-∼ nats∼nats-from-0 (Conat.reflexive-∼ _) ⟩
  LUB (nats-from 0) infinity  ↝⟨ LUB-≂ (symmetric-≂ (Ω-sizes≂nats-from 0)) ⟩□
  LUB (Ω-sizes 0)   infinity  □

-- When Ω is interpreted (starting with an empty stack) the stack
-- sizes that are encountered match the sizes in the colist Ω-sizes 0.

stack-sizes-Ω∼Ω-sizes-0 :
  ∀ {i} → C.[ i ] stack-sizes Ω ∼ Ω-sizes 0
stack-sizes-Ω∼Ω-sizes-0 =
  stack-sizes Ω                                                     C.∼⟨⟩

  numbers (⟦ Ω ⟧ [] false) 0                                        C.∼⟨ (E.refl ∷ λ { .force → E.refl ∷ λ { .force → E.refl ∷ λ { .force →
                                                                          C.reflexive-∼ _ }}}) ⟩
  0 ∷′ 1 ∷′ 2 ∷′ numbers (⟦ ω-body ⟧ (lam ω-body [] ∷ []) true >>=
                          tell pred ∘ return) 1                     C.∼⟨ (cong₃ λ { .force → lemma 1 }) ⟩

  0 ∷′ 1 ∷′ 2 ∷′ Ω-sizes 1                                          C.∼⟨ (cong₃ λ { .force → C.reflexive-∼ _ }) ⟩

  Ω-sizes 0                                                         C.∎
  where
  lemma :
    ∀ {i} n {k : Value → Delay-crash-trace (ℕ → ℕ) Value ∞} →
    C.[ i ] numbers (⟦ ω-body ⟧ (lam ω-body [] ∷ []) true >>= k) n ∼
            Ω-sizes n
  lemma n {k} =
    numbers (⟦ ω-body ⟧ (lam ω-body [] ∷ []) true >>= k) n                C.∼⟨⟩

    numbers (tell suc (tell suc
               ([ pred , pred ] lam ω-body [] ∙ lam ω-body []) >>= k)) n  C.∼⟨ (E.refl ∷ λ { .force → E.refl ∷ λ { .force → E.refl ∷ λ { .force →
                                                                                C.reflexive-∼ _ }}}) ⟩
    n ∷′ 1 + n ∷′ 2 + n ∷′
    numbers (⟦ ω-body ⟧ (lam ω-body [] ∷ []) true >>=
             tell pred ∘ return >>= k) (1 + n)                            C.∼⟨ (cong₃ λ { .force → C.symmetric-∼ $ numbers-cong $
                                                                                DCT.associativity (⟦ ω-body ⟧ (lam _ _ ∷ []) true) _ _ }) ⟩
    n ∷′ 1 + n ∷′ 2 + n ∷′
    numbers (⟦ ω-body ⟧ (lam ω-body [] ∷ []) true >>= λ v →
             tell pred (return v) >>= k) (1 + n)                          C.∼⟨ (cong₃ λ { .force → lemma (1 + n) }) ⟩

    n ∷′ 1 + n ∷′ 2 + n ∷′ Ω-sizes (1 + n)                                C.∼⟨ (cong₃ λ { .force → C.reflexive-∼ _ }) ⟩

    Ω-sizes n                                                             C.∎

-- The computation Ω requires unbounded space.

Ω-requires-unbounded-space : LUB (stack-sizes Ω) infinity
Ω-requires-unbounded-space =
  LUB-∼ (C.symmetric-∼ stack-sizes-Ω∼Ω-sizes-0)
        (Conat.reflexive-∼ _)
        lub-Ω-sizes-0-infinity

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
------------------------------------------------------------------------------
-- The FOTC natural numbers type
------------------------------------------------------------------------------

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

-- N.B. This module is re-exported by FOTC.Data.Nat.

module FOTC.Data.Nat.Type where

open import FOTC.Base

------------------------------------------------------------------------------
-- The FOTC natural numbers type (inductive predicate for the total
-- natural numbers).
data N : D → Set where
  nzero : N zero
  nsucc : ∀ {n} → N n → N (succ₁ n)
{-# ATP axioms nzero nsucc #-}

-- Induction principle.
N-ind : (A : D → Set) →
        A zero →
        (∀ {n} → A n → A (succ₁ n)) →
        ∀ {n} → N n → A n
N-ind A A0 h nzero      = A0
N-ind A A0 h (nsucc Nn) = h (N-ind A A0 h Nn)


text:
{-# OPTIONS --type-in-type #-}  -- yes, there will be some cheating in this lecture

module Lec3Start where

open import Lec1Done
open import Lec2Done

postulate
  extensionality : {S : Set}{T : S -> Set}
                   (f g : (x : S) -> T x) ->
                   ((x : S) -> f x == g x) ->
                   f == g

record Category : Set where
  field

    -- two types of thing
    Obj  : Set                  -- "objects"
    _~>_ : Obj -> Obj -> Set    -- "arrows" or "morphisms"
                                -- or "homomorphisms"

    -- two operations
    id~>        : {T : Obj} ->      T ~> T
    _>~>_       : {R S T : Obj} ->  R ~> S  ->  S ~> T  ->  R ~> T

    -- three laws
    law-id~>>~> : {S T : Obj}     (f : S ~> T) ->
                    (id~> >~> f) == f
    law->~>id~> : {S T : Obj}     (f : S ~> T) ->
                    (f >~> id~>) == f
    law->~>>~>  : {Q R S T : Obj} (f : Q ~> R)(g : R ~> S)(h : S ~> T) ->
                    ((f >~> g) >~> h) == (f >~> (g >~> h))

-- Sets and functions are the classic example of a category.
{-+}
SET : Category
SET = {!!}
{+-}

-- A PREORDER is a category where there is at most one arrow between
-- any two objects. (So arrows are unique.)
{-+}
NAT->= : Category
NAT->= = {!!} where
  unique : (m n : Nat)(p q : m >= n) -> p == q
  unique m n p q = {!!}
{+-}

-- A MONOID is a category with Obj = One.
-- The values in the monoid are the *arrows*.
{-+}
ONE-Nat : Category
ONE-Nat = {!!}
{+-}

{-+}
eqUnique : {X : Set}{x y : X}(p q : x == y) -> p == q
eqUnique p q = {!!}

-- A DISCRETE category is one where the only arrows are the identities.
DISCRETE : (X : Set) -> Category
DISCRETE X = {!!}
{+-}

module FUNCTOR where
  open Category

  record _=>_ (C D : Category) : Set where  -- "Functor from C to D"
    field
      -- two actions
      F-Obj : Obj C -> Obj D
      F-map : {S T : Obj C} -> _~>_ C S T -> _~>_ D (F-Obj S) (F-Obj T)

      -- two laws
      F-map-id~> : {T : Obj C} -> F-map (id~> C {T}) == id~> D {F-Obj T}
      F-map->~>  : {R S T : Obj C}(f : _~>_ C R S)(g : _~>_ C S T) ->
                     F-map (_>~>_ C f g) == _>~>_ D (F-map f) (F-map g)

open FUNCTOR

{-+}
VEC : Nat -> SET => SET
VEC n = {!!}
{+-}

{-+}
VTAKE : Set -> NAT->= => SET
VTAKE X = {!!}
{+-}

{-+}
ADD : Nat -> NAT->= => NAT->=
ADD d = {!!}
{+-}

{-+}
CATEGORY : Category
CATEGORY = {!!}
{+-}

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

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

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


text:
module Stack where

open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; zero; suc)

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

module V1 where
    {-
    This first version introduces the Stack abstract data type.
    -}

    data Stack (A : Set) : Set where
        ∅    : Stack A
        _>>_ : A → Stack A → Stack A

    infixr 50 _>>_

    push : ∀ {A} → A → Stack A → Stack A
    push a s = a >> s

    peek : ∀ {A} → (S : Stack A) → A
    -- May be absurd can be used here but how?
    peek (a >> _) = a

    pop : ∀ {A} → (S : Stack A) → Stack A
    -- May be absurd can be used here but how?
    pop (a >> s) = s

    module Example where
        _ : Stack Bool
        _ = true >> false >> ∅

    module Laws where
        law1 : ∀ {A} (a : A) (s : Stack A) -> peek (push a s) ≡ a
        law1 a s =
            begin
               peek (push a s)
               ≡⟨⟩
               peek (a >> s)
               ≡⟨⟩
               a
            ∎

        law2 : ∀ {A} {a : A} {s : Stack A} → pop (push a s) ≡ s
        law2 = refl

module V2 where
    {-
    This second version introduces the expression as constraint in the type definition.
    This prevents incomplete pattern matching for peek and pop.

    For this purpose we first design empty? predicate and then we use it in the type definition
    of peek and pop.
    -}

    data Stack (A : Set) : Set where
        ∅    : Stack A
        _>>_ : A → Stack A → Stack A

    infixr 50 _>>_

    empty? : ∀ {A} → Stack A → Bool
    empty? ∅ = true
    empty? _ = false

    push : ∀ {A} → A → Stack A → Stack A
    push a s = a >> s

    peek : ∀ {A} → (S : Stack A) -> {empty? S ≡ false} → A
    peek (a >> _) = a

    pop : ∀ {A} → (S : Stack A) -> {empty? S ≡ false} → Stack A
    pop (a >> s) = s

    module Example where
        _ : Stack Bool
        _ = pop (push true ∅) {refl}

    module Laws where
        law1 : ∀ {A} {a : A} {s : Stack A} → peek (push a s) {refl} ≡ a
        law1 = refl

        law2 : ∀ {A} {a : A} {s : Stack A} → pop (push a s) {refl} ≡ s
        law2 = refl

module V3 where
    {-
    In this third version we use a GADT for the Stack data representation.
    A Kind then is design on purpose and a phantom type is used for the
    association between the stack and the kind.
    -}

    data Kind : Set where
        Empty    : Kind
        NotEmpty : Kind

    data Stack (A : Set) : Kind → Set where
        ∅    : Stack A Empty
        _>>_ : ∀ {B} → A → Stack A B → Stack A NotEmpty

    infixr 50 _>>_

    push : ∀ {A B} → A → Stack A B → Stack A NotEmpty
    push a s = a >> s

    peek : ∀ {A} → Stack A NotEmpty → A
    peek (a >> _) = a

    {-
    B is in the ouput only! => No constraint with the input.
    Writing such pop function is impossible as is.

    pop : ∀ {A B} → Stack A NotEmpty → Stack A B
    pop (_ >> s) = s
    -}

    module Example where
        _ : Stack Bool NotEmpty
        _ = push true ∅

    module Laws where
        law1 : ∀ {A B} {a : A} {s : Stack A B} → peek (push a s) ≡ a
        law1 = refl

        -- law2 cannot be expressed ...

module V4 where
    {-
    In this fourth version we slightly review the NotEmpty construction.
    This opens the opportunity to express the pop function since a
    dependency can by modeled in the corresponding type definition.
    -}
    data Kind : Set where
        Empty    : Kind
        NotEmpty : Kind → Kind

    data Stack (A : Set) : Kind → Set where
        ∅  : Stack A Empty
        _>>_ : ∀ {B} → A → Stack A B → Stack A (NotEmpty B)

    infixr 50 _>>_

    push : ∀ {A B} → A → Stack A B → Stack A (NotEmpty B)
    push a s = a >> s

    peek : ∀ {A B} → Stack A (NotEmpty B) → A
    peek (a >> _) = a

    pop : ∀ {A B} → Stack A (NotEmpty B) → Stack A B
    pop (_ >> s) = s

    module Example where
        _ : Stack Bool (NotEmpty Empty)
        _ = push true ∅

    module Laws where
        law1 : ∀ {A B} {a : A} {s : Stack A B} → peek (push a s) ≡ a
        law1 = refl

        law2 : ∀ {A B} {a : A} {s : Stack A B} → pop (push a s) ≡ s
        law2 = refl

module V5 where
    {-
    In this last version we show that previous Kind definiton is isomorphic
    with the Natural.
    -}

    data Stack (A : Set) : ℕ → Set where
        ∅  : Stack A 0
        _>>_ : ∀ {B} → A → Stack A B → Stack A (suc B)

    infixr 50 _>>_

    push : ∀ {A B} → A → Stack A B → Stack A (suc B)
    push a s = a >> s

    peek : ∀ {A B} → Stack A (suc B) → A
    peek (a >> _) = a

    pop : ∀ {A B} → Stack A (suc B) → Stack A B
    pop (_ >> s) = s

    module Example where
        _ : Stack Bool 1
        _ = push true ∅

    module Laws where
        law1 : ∀ {A B} {a : A} {s : Stack A B} → peek (push a s) ≡ a
        law1 = refl

        law2 : ∀ {A B} {a : A} {s : Stack A B} → pop (push a s) ≡ s
        law2 = refl

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


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

module Cubical.Codata.M.AsLimit.M.Properties where

open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Cubical.Data.Nat as ℕ using (ℕ ; suc ; _+_ )
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv using (_≃_)
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv

open import Cubical.Functions.Embedding

open import Cubical.Codata.M.AsLimit.helper
open import Cubical.Codata.M.AsLimit.M.Base
open import Cubical.Codata.M.AsLimit.Container

-- in-fun and out-fun are inverse

open Iso

in-inverse-out : ∀ {ℓ} {S : Container ℓ} → (in-fun {S = S} ∘ out-fun {S = S}) ≡ idfun (M S)
in-inverse-out {S = S} = subst (λ inv → in-fun {S = S} ∘ inv ≡ idfun (M S)) idpath def where
  -- substituting refl makes type-checking work a lot faster, but introduces a transport
  -- TODO (2020-05-23): revisit this at some point to see if it's still needed in future versions of agda
  def : (in-fun {S = S} ∘ inv (shift-iso S)) ≡ idfun (M S)
  def = funExt (rightInv (shift-iso S))
  idpath : inv (shift-iso S) ≡ out-fun {S = S}
  idpath = refl

out-inverse-in : ∀ {ℓ} {S : Container ℓ} → (out-fun {S = S} ∘ in-fun {S = S}) ≡ idfun (P₀ S (M S))
out-inverse-in {S = S} = subst (λ fun → out-fun {S = S} ∘ fun ≡ idfun (P₀ S (M S))) idpath def where
  def : (out-fun {S = S} ∘ fun (shift-iso S)) ≡ idfun (P₀ S (M S))
  def = funExt (leftInv (shift-iso S))
  idpath : fun (shift-iso S) ≡ in-fun {S = S}
  idpath = refl

in-out-id : ∀ {ℓ} {S : Container ℓ} -> ∀ {x y : M S} → (in-fun (out-fun x) ≡ in-fun (out-fun y)) ≡ (x ≡ y)
in-out-id {x = x} {y} i = (in-inverse-out i x) ≡ (in-inverse-out i y)

-- constructor properties

in-inj : ∀ {ℓ} {S : Container ℓ} {Z : Type ℓ} → ∀ {f g : Z → P₀ S (M S)} → (in-fun ∘ f ≡ in-fun ∘ g) ≡ (f ≡ g)
in-inj {ℓ} {S = S} {Z = Z} {f = f} {g = g} = iso→fun-Injection-Path {ℓ = ℓ} {A = P₀ S (M S)} {B = M S} {C = Z} (shift-iso S) {f = f} {g = g}

out-inj : ∀ {ℓ} {S : Container ℓ} {Z : Type ℓ} → ∀ {f g : Z → M S} → (out-fun ∘ f ≡ out-fun ∘ g) ≡ (f ≡ g)
out-inj {ℓ} {S = S} {Z = Z} {f = f} {g = g} = iso→inv-Injection-Path {ℓ = ℓ} {A = P₀ S (M S)} {B = M S} {C = Z} (shift-iso S) {f = f} {g = g}

in-inj-x : ∀ {ℓ} {S : Container ℓ} → ∀ {x y : P₀ S (M S)} → (in-fun x ≡ in-fun y) ≡ (x ≡ y)
in-inj-x {ℓ} {S = S} {x = x} {y} = iso→fun-Injection-Path-x (shift-iso S) {x} {y}

out-inj-x : ∀ {ℓ} {S : Container ℓ} → ∀ {x y : M S} → (out-fun x ≡ out-fun y) ≡ (x ≡ y)
out-inj-x {ℓ} {S = S} {x = x} {y} = iso→inv-Injection-Path-x (shift-iso S) {x} {y}

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Ring.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring.Base

private
  variable
    ℓ : Level

{-
  some basic calculations (used for example in QuotientRing.agda),
  that should become obsolete or subject to change once we have a
  ring solver (see https://github.com/agda/cubical/issues/297)
-}
module RingTheory (R' : Ring ℓ) where

  open RingStr (snd R')
  private R = ⟨ R' ⟩
  implicitInverse : (x y : R)
                 → x + y ≡ 0r
                 → y ≡ - x
  implicitInverse x y p =
    y               ≡⟨ sym (+Lid y) ⟩
    0r + y          ≡⟨ cong (λ u → u + y) (sym (+Linv x)) ⟩
    (- x + x) + y   ≡⟨ sym (+Assoc _ _ _) ⟩
    (- x) + (x + y) ≡⟨ cong (λ u → (- x) + u) p ⟩
    (- x) + 0r      ≡⟨ +Rid _ ⟩
    - x             ∎

  equalByDifference : (x y : R)
                      → x - y ≡ 0r
                      → x ≡ y
  equalByDifference x y p =
    x               ≡⟨ sym (+Rid _) ⟩
    x + 0r          ≡⟨ cong (λ u → x + u) (sym (+Linv y)) ⟩
    x + ((- y) + y) ≡⟨ +Assoc _ _ _ ⟩
    (x - y) + y     ≡⟨ cong (λ u → u + y) p ⟩
    0r + y          ≡⟨ +Lid _ ⟩
    y               ∎

  0Selfinverse : - 0r ≡ 0r
  0Selfinverse = sym (implicitInverse _ _ (+Rid 0r))

  0Idempotent : 0r + 0r ≡ 0r
  0Idempotent = +Lid 0r

  +Idempotency→0 : (x : R) → x ≡ x + x → x ≡ 0r
  +Idempotency→0 x p =
    x               ≡⟨ sym (+Rid x) ⟩
    x + 0r          ≡⟨ cong (λ u → x + u) (sym (+Rinv _)) ⟩
    x + (x + (- x)) ≡⟨ +Assoc _ _ _ ⟩
    (x + x) + (- x) ≡⟨ cong (λ u → u + (- x)) (sym p) ⟩
    x + (- x)       ≡⟨ +Rinv _ ⟩
    0r              ∎

  -Idempotent : (x : R) → -(- x) ≡ x
  -Idempotent x =  - (- x)   ≡⟨ sym (implicitInverse (- x) x (+Linv _)) ⟩
                   x ∎

  0RightAnnihilates : (x : R) → x · 0r ≡ 0r
  0RightAnnihilates x =
              let x·0-is-idempotent : x · 0r ≡ x · 0r + x · 0r
                  x·0-is-idempotent =
                    x · 0r               ≡⟨ cong (λ u → x · u) (sym 0Idempotent) ⟩
                    x · (0r + 0r)        ≡⟨ ·Rdist+ _ _ _ ⟩
                    (x · 0r) + (x · 0r)  ∎
              in (+Idempotency→0 _ x·0-is-idempotent)

  0LeftAnnihilates : (x : R) → 0r · x ≡ 0r
  0LeftAnnihilates x =
              let 0·x-is-idempotent : 0r · x ≡ 0r · x + 0r · x
                  0·x-is-idempotent =
                    0r · x               ≡⟨ cong (λ u → u · x) (sym 0Idempotent) ⟩
                    (0r + 0r) · x        ≡⟨ ·Ldist+ _ _ _ ⟩
                    (0r · x) + (0r · x)  ∎
              in +Idempotency→0 _ 0·x-is-idempotent

  -DistR· : (x y : R) →  x · (- y) ≡ - (x · y)
  -DistR· x y = implicitInverse (x · y) (x · (- y))

                               (x · y + x · (- y)     ≡⟨ sym (·Rdist+ _ _ _) ⟩
                               x · (y + (- y))        ≡⟨ cong (λ u → x · u) (+Rinv y) ⟩
                               x · 0r                 ≡⟨ 0RightAnnihilates x ⟩
                               0r ∎)

  -DistL· : (x y : R) →  (- x) · y ≡ - (x · y)
  -DistL· x y = implicitInverse (x · y) ((- x) · y)

                              (x · y + (- x) · y     ≡⟨ sym (·Ldist+ _ _ _) ⟩
                              (x - x) · y            ≡⟨ cong (λ u → u · y) (+Rinv x) ⟩
                              0r · y                 ≡⟨ 0LeftAnnihilates y ⟩
                              0r ∎)

  -Swap· : (x y : R) → (- x) · y ≡ x · (- y)
  -Swap· _ _ = -DistL· _ _ ∙ sym (-DistR· _ _)

  -IsMult-1 : (x : R) → - x ≡ (- 1r) · x
  -IsMult-1 _ = sym (·Lid _) ∙ sym (-Swap· _ _)

  -Dist : (x y : R) → (- x) + (- y) ≡ - (x + y)
  -Dist x y =
    implicitInverse _ _
         ((x + y) + ((- x) + (- y)) ≡⟨ sym (+Assoc _ _ _) ⟩
          x + (y + ((- x) + (- y))) ≡⟨ cong
                                         (λ u → x + (y + u))
                                         (+Comm _ _) ⟩
          x + (y + ((- y) + (- x))) ≡⟨ cong (λ u → x + u) (+Assoc _ _ _) ⟩
          x + ((y + (- y)) + (- x)) ≡⟨ cong (λ u → x + (u + (- x)))
                                            (+Rinv _) ⟩
          x + (0r + (- x))           ≡⟨ cong (λ u → x + u) (+Lid _) ⟩
          x + (- x)                 ≡⟨ +Rinv _ ⟩
          0r ∎)

  translatedDifference : (x a b : R) → a - b ≡ (x + a) - (x + b)
  translatedDifference x a b =
              a - b                       ≡⟨ cong (λ u → a + u)
                                                  (sym (+Lid _)) ⟩
              (a + (0r + (- b)))          ≡⟨ cong (λ u → a + (u + (- b)))
                                                  (sym (+Rinv _)) ⟩
              (a + ((x + (- x)) + (- b))) ≡⟨ cong (λ u → a + u)
                                                  (sym (+Assoc _ _ _)) ⟩
              (a + (x + ((- x) + (- b)))) ≡⟨ (+Assoc _ _ _) ⟩
              ((a + x) + ((- x) + (- b))) ≡⟨ cong (λ u → u + ((- x) + (- b)))
                                                  (+Comm _ _) ⟩
              ((x + a) + ((- x) + (- b))) ≡⟨ cong (λ u → (x + a) + u)
                                                  (-Dist _ _) ⟩
              ((x + a) - (x + b)) ∎

  +Assoc-comm1 : (x y z : R) → x + (y + z) ≡ y + (x + z)
  +Assoc-comm1 x y z = +Assoc x y z ∙∙ cong (λ x → x + z) (+Comm x y) ∙∙ sym (+Assoc y x z)

  +Assoc-comm2 : (x y z : R) → x + (y + z) ≡ z + (y + x)
  +Assoc-comm2 x y z = +Assoc-comm1 x y z ∙∙ cong (λ x → y + x) (+Comm x z) ∙∙ +Assoc-comm1 y z x

  +ShufflePairs : (a b c d : R)
                → (a + b) + (c + d) ≡ (a + c) + (b + d)
  +ShufflePairs a b c d =
    (a + b) + (c + d) ≡⟨ +Assoc _ _ _ ⟩
    ((a + b) + c) + d ≡⟨ cong (λ u → u + d) (sym (+Assoc _ _ _)) ⟩
    (a + (b + c)) + d ≡⟨ cong (λ u → (a + u) + d) (+Comm _ _) ⟩
    (a + (c + b)) + d ≡⟨ cong (λ u → u + d) (+Assoc _ _ _) ⟩
    ((a + c) + b) + d ≡⟨ sym (+Assoc _ _ _) ⟩
    (a + c) + (b + d) ∎

  ·-assoc2 : (x y z w : R) → (x · y) · (z · w) ≡ x · (y · z) · w
  ·-assoc2 x y z w = ·Assoc (x · y) z w ∙ cong (_· w) (sym (·Assoc x y z))

module RingHoms where
  open IsRingHom

  idRingHom : (R : Ring ℓ) → RingHom R R
  fst (idRingHom R) = idfun (fst R)
  snd (idRingHom R) = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)

  compRingHom : {R S T : Ring ℓ} → RingHom R S → RingHom S T → RingHom R T
  fst (compRingHom f g) x = g .fst (f .fst x)
  snd (compRingHom f g) = makeIsRingHom (cong (g .fst) (pres1 (snd f)) ∙ pres1 (snd g))
                                        (λ x y → cong (g .fst) (pres+ (snd f) _ _) ∙ pres+ (snd g) _ _)
                                        (λ x y → cong (g .fst) (pres· (snd f) _ _) ∙ pres· (snd g) _ _)

  compIdRingHom : {R S : Ring ℓ} (φ : RingHom R S) → compRingHom (idRingHom R) φ ≡ φ
  compIdRingHom φ = RingHom≡ refl

  idCompRingHom : {R S : Ring ℓ} (φ : RingHom R S) → compRingHom φ (idRingHom S) ≡ φ
  idCompRingHom φ = RingHom≡ refl

  compAssocRingHom : {R S T U : Ring ℓ} (φ : RingHom R S) (ψ : RingHom S T) (χ : RingHom T U) →
                     compRingHom (compRingHom φ ψ) χ ≡ compRingHom φ (compRingHom ψ χ)
  compAssocRingHom _ _ _ = RingHom≡ refl

module RingHomTheory {R S : Ring ℓ} (φ : RingHom R S) where
  open RingTheory ⦃...⦄
  open RingStr ⦃...⦄
  open IsRingHom (φ .snd)
  private
    instance
      _ = R
      _ = S
      _ = snd R
      _ = snd S
    f = fst φ

  ker≡0→inj : ({x : ⟨ R ⟩} → f x ≡ 0r → x ≡ 0r)
            → ({x y : ⟨ R ⟩} → f x ≡ f y → x ≡ y)
  ker≡0→inj ker≡0 {x} {y} p = equalByDifference _ _ (ker≡0 path)
   where
   path : f (x - y) ≡ 0r
   path = f (x - y)     ≡⟨ pres+ _ _ ⟩
          f x + f (- y) ≡⟨ cong (f x +_) (pres- _) ⟩
          f x - f y     ≡⟨ cong (_- f y) p ⟩
          f y - f y     ≡⟨ +Rinv _ ⟩
          0r            ∎


text:
module Issue3295.Incomplete2 where

open import Agda.Builtin.Nat

{-# NON_COVERING #-}
g : Nat → Nat
g zero = zero

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda