text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Monoid.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Function
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.Algebra.Semigroup hiding (⟨_⟩)

open Iso

private
  variable
    ℓ : Level

record IsMonoid {A : Type ℓ} (ε : A) (_·_ : A → A → A) : Type ℓ where
  constructor ismonoid

  field
    isSemigroup : IsSemigroup _·_
    identity    : (x : A) → (x · ε ≡ x) × (ε · x ≡ x)

  open IsSemigroup isSemigroup public

  lid : (x : A) → ε · x ≡ x
  lid x = identity x .snd

  rid : (x : A) → x · ε ≡ x
  rid x = identity x .fst

record Monoid : Type (ℓ-suc ℓ) where
  constructor monoid

  field
    Carrier  : Type ℓ
    ε        : Carrier
    _·_      : Carrier → Carrier → Carrier
    isMonoid : IsMonoid ε _·_

  infixl 7 _·_

  open IsMonoid isMonoid public

  -- semigrp : Semigroup
  -- semigrp = record { isSemigroup = isSemigroup }

  -- open Semigroup semigrp public

-- Extractor for the carrier type
⟨_⟩ : Monoid → Type ℓ
⟨_⟩ = Monoid.Carrier

η-isMonoid : {A : Type ℓ} {ε : A} {_∙_ :  A → A → A} (b : IsMonoid ε _∙_)
          → ismonoid (IsMonoid.isSemigroup b) (IsMonoid.identity b) ≡ b
IsMonoid.isSemigroup (η-isMonoid b i) = IsMonoid.isSemigroup b
IsMonoid.identity (η-isMonoid b i) = IsMonoid.identity b

-- Easier to use constructors

makeIsMonoid : {M : Type ℓ} {ε : M} {_·_ : M → M → M}
               (is-setM : isSet M)
               (assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
               (rid : (x : M) → x · ε ≡ x)
               (lid : (x : M) → ε · x ≡ x)
             → IsMonoid ε _·_
IsMonoid.isSemigroup (makeIsMonoid is-setM assoc rid lid) = issemigroup is-setM assoc
IsMonoid.identity (makeIsMonoid is-setM assoc rid lid) = λ x → rid x , lid x

makeMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M)
             (is-setM : isSet M)
             (assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
             (rid : (x : M) → x · ε ≡ x)
             (lid : (x : M) → ε · x ≡ x)
           → Monoid
makeMonoid ε _·_ is-setM assoc rid lid =
  monoid _ ε _·_ (makeIsMonoid is-setM assoc rid lid)

record MonoidEquiv (M N : Monoid {ℓ}) : Type ℓ where

  constructor monoidiso

  private
    module M = Monoid M
    module N = Monoid N

  field
    e     : ⟨ M ⟩ ≃ ⟨ N ⟩
    presε : equivFun e M.ε ≡ N.ε
    isHom : (x y : ⟨ M ⟩) → equivFun e (x M.· y) ≡ equivFun e x N.· equivFun e y

module MonoidΣTheory {ℓ} where

  RawMonoidStructure : Type ℓ → Type ℓ
  RawMonoidStructure X = X × (X → X → X)

  RawMonoidEquivStr = AutoEquivStr RawMonoidStructure

  rawMonoidUnivalentStr : UnivalentStr _ RawMonoidEquivStr
  rawMonoidUnivalentStr = autoUnivalentStr RawMonoidStructure

  MonoidAxioms : (M : Type ℓ) → RawMonoidStructure M → Type ℓ
  MonoidAxioms M (e , _·_) = IsSemigroup _·_
                            × ((x : M) → (x · e ≡ x) × (e · x ≡ x))

  MonoidStructure : Type ℓ → Type ℓ
  MonoidStructure = AxiomsStructure RawMonoidStructure MonoidAxioms

  MonoidΣ : Type (ℓ-suc ℓ)
  MonoidΣ = TypeWithStr ℓ MonoidStructure

  isPropMonoidAxioms : (M : Type ℓ) (s : RawMonoidStructure M) → isProp (MonoidAxioms M s)
  isPropMonoidAxioms M (e , _·_) =
    isPropΣ (isPropIsSemigroup _·_)
            λ α → isPropΠ λ _ → isProp× (IsSemigroup.is-set α _ _) (IsSemigroup.is-set α _ _)

  MonoidEquivStr : StrEquiv MonoidStructure ℓ
  MonoidEquivStr = AxiomsEquivStr RawMonoidEquivStr MonoidAxioms

  MonoidAxiomsIsoIsMonoid : {M : Type ℓ} (s : RawMonoidStructure M)
    → Iso (MonoidAxioms M s) (IsMonoid (s .fst) (s .snd))
  fun (MonoidAxiomsIsoIsMonoid s) (x , y)        = ismonoid x y
  inv (MonoidAxiomsIsoIsMonoid s) a = (IsMonoid.isSemigroup a) , IsMonoid.identity a
  rightInv (MonoidAxiomsIsoIsMonoid s) b         = η-isMonoid b
  leftInv (MonoidAxiomsIsoIsMonoid s) _          = refl

  MonoidAxioms≡IsMonoid : {M : Type ℓ} (s : RawMonoidStructure M)
    → MonoidAxioms M s ≡ IsMonoid (s .fst) (s .snd)
  MonoidAxioms≡IsMonoid s = isoToPath (MonoidAxiomsIsoIsMonoid s)
  open Monoid
  Monoid→MonoidΣ : Monoid → MonoidΣ
  Monoid→MonoidΣ M =
    ⟨ M ⟩ , ((ε M) , _·_ M) , MonoidAxiomsIsoIsMonoid ((ε M) , _·_ M) .inv (isMonoid M)

  MonoidΣ→Monoid : MonoidΣ → Monoid
  MonoidΣ→Monoid (M , (ε , _·_) , isMonoidΣ) =
    monoid M ε _·_ (MonoidAxiomsIsoIsMonoid (ε , _·_) .fun isMonoidΣ)

  MonoidIsoMonoidΣ : Iso Monoid MonoidΣ
  MonoidIsoMonoidΣ =
    iso Monoid→MonoidΣ MonoidΣ→Monoid (λ _ → refl) helper
    where
    helper : _
    Carrier (helper a i) = ⟨ a ⟩
    ε (helper a i) = ε a
    _·_ (helper a i) = _·_ a
    isMonoid (helper a i) = η-isMonoid (isMonoid a) i

  monoidUnivalentStr : UnivalentStr MonoidStructure MonoidEquivStr
  monoidUnivalentStr = axiomsUnivalentStr _ isPropMonoidAxioms rawMonoidUnivalentStr

  MonoidΣPath : (M N : MonoidΣ) → (M ≃[ MonoidEquivStr ] N) ≃ (M ≡ N)
  MonoidΣPath = SIP monoidUnivalentStr

  MonoidEquivΣ : (M N : Monoid) → Type ℓ
  MonoidEquivΣ M N = Monoid→MonoidΣ M ≃[ MonoidEquivStr ] Monoid→MonoidΣ N

  MonoidIsoΣPath : {M N : Monoid} → Iso (MonoidEquiv M N) (MonoidEquivΣ M N)
  fun MonoidIsoΣPath (monoidiso e h1 h2) = (e , h1 , h2)
  inv MonoidIsoΣPath (e , h1 , h2)       = monoidiso e h1 h2
  rightInv MonoidIsoΣPath _              = refl
  leftInv MonoidIsoΣPath _               = refl

  MonoidPath : (M N : Monoid) → (MonoidEquiv M N) ≃ (M ≡ N)
  MonoidPath M N =
    MonoidEquiv M N                       ≃⟨ isoToEquiv MonoidIsoΣPath ⟩
    MonoidEquivΣ M N                      ≃⟨ MonoidΣPath _ _ ⟩
    Monoid→MonoidΣ M ≡ Monoid→MonoidΣ N ≃⟨ isoToEquiv (invIso (congIso MonoidIsoMonoidΣ)) ⟩
    M ≡ N ■

  RawMonoidΣ : Type (ℓ-suc ℓ)
  RawMonoidΣ = TypeWithStr ℓ RawMonoidStructure

  Monoid→RawMonoidΣ : Monoid → RawMonoidΣ
  Monoid→RawMonoidΣ A = ⟨ A ⟩ , (ε A) , (_·_ A)

  InducedMonoid : (M : Monoid) (N : RawMonoidΣ) (e : M .Monoid.Carrier ≃ N .fst)
                 → RawMonoidEquivStr (Monoid→RawMonoidΣ M) N e → Monoid
  InducedMonoid M N e r =
    MonoidΣ→Monoid (transferAxioms rawMonoidUnivalentStr (Monoid→MonoidΣ M) N (e , r))

  InducedMonoidPath : (M : Monoid {ℓ}) (N : RawMonoidΣ) (e : M .Monoid.Carrier ≃ N .fst)
                      (E : RawMonoidEquivStr (Monoid→RawMonoidΣ M) N e)
                    → M ≡ InducedMonoid M N e E
  InducedMonoidPath M N e E =
    MonoidPath M (InducedMonoid M N e E) .fst (monoidiso e (E .fst) (E .snd))

-- We now extract the important results from the above module

isPropIsMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M) → isProp (IsMonoid ε _·_)
isPropIsMonoid ε _·_ =
  subst isProp (MonoidΣTheory.MonoidAxioms≡IsMonoid (ε , _·_))
        (MonoidΣTheory.isPropMonoidAxioms _ (ε , _·_))

MonoidPath : (M N : Monoid {ℓ}) → (MonoidEquiv M N) ≃ (M ≡ N)
MonoidPath = MonoidΣTheory.MonoidPath

InducedMonoid : (M : Monoid {ℓ}) (N : MonoidΣTheory.RawMonoidΣ) (e : M .Monoid.Carrier ≃ N .fst)
              → MonoidΣTheory.RawMonoidEquivStr (MonoidΣTheory.Monoid→RawMonoidΣ M) N e
              → Monoid
InducedMonoid = MonoidΣTheory.InducedMonoid

InducedMonoidPath : (M : Monoid {ℓ}) (N : MonoidΣTheory.RawMonoidΣ) (e : M .Monoid.Carrier ≃ N .fst)
                    (E : MonoidΣTheory.RawMonoidEquivStr (MonoidΣTheory.Monoid→RawMonoidΣ M) N e)
                  → M ≡ InducedMonoid M N e E
InducedMonoidPath = MonoidΣTheory.InducedMonoidPath

module MonoidTheory {ℓ} (M' : Monoid {ℓ}) where

  open Monoid M' renaming ( Carrier to M )

  -- Added for its use in groups
  -- If there exists a inverse of an element it is unique
  inv-lemma : (x y z : M) → y · x ≡ ε → x · z ≡ ε → y ≡ z
  inv-lemma x y z left-inverse right-inverse =
    y           ≡⟨ sym (rid y) ⟩
    y · ε       ≡⟨ cong (λ - → y · -) (sym right-inverse) ⟩
    y · (x · z) ≡⟨ assoc y x z ⟩
    (y · x) · z ≡⟨ cong (λ - → - · z) left-inverse ⟩
    ε · z       ≡⟨ lid z ⟩
    z ∎

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module _ where

  data Nat : Set where
    zero : Nat
    suc : Nat → Nat
  {-# BUILTIN NATURAL Nat #-}

  _+_ : (m n : Nat) → Nat
  zero + n = n
  suc m + n = suc (m + n)

  data Th : (m n : Nat) → Set where
    os : ∀ {m n} → Th m n → Th (suc m) (suc n)

  Fin : Nat → Set
  Fin = Th (suc zero)

  infixl 6 _++_
  infix 4 _≈M_

  postulate
    U : Set
    RCtx : Nat → Set
    _++_ : ∀ {m n} → RCtx m → RCtx n → RCtx (n + m)
    El : U → RCtx (suc zero)
    _≈M_ : ∀ {n} (Δ0 Δ1 : RCtx n) → Set

  infix 4 _⊢l-var_

  data _⊢l-var_ : ∀ {n} (Δi : RCtx n) (i : Fin n) → Set where
    os : ∀ {n} {e : Th zero n} {Δ Δπ π} (iq : Δπ ≈M (Δ ++ El π)) →
         Δπ ⊢l-var os e

  ⊢l-var-sub : ∀ {n Δ} {i : Fin n} → Δ ⊢l-var i → Set
  ⊢l-var-sub (os iq) = Nat

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Examples.Sorting.Sequential.Comparable where

open import Calf.CostMonoid
open import Calf.CostMonoids

costMonoid = ℕ-CostMonoid

open import Data.Nat using (ℕ)
open CostMonoid costMonoid using (ℂ)

fromℕ : ℕ → ℂ
fromℕ n = n

open import Examples.Sorting.Comparable costMonoid fromℕ public

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Type.Properties.Homotopy where

open import Functional
import      Lvl
open import Numeral.Natural
open import Structure.Setoid
open import Type
open import Type.Dependent
open import Syntax.Function

private variable ℓ ℓ₁ ℓ₂ ℓₑ : Lvl.Level
private variable T A B : Type{ℓ}
private variable n : ℕ

module _ {ℓ} ⦃ equiv : ∀{T : Type{ℓ}} → Equiv{ℓ}(T) ⦄ where -- TODO: Maybe the requirements can be relaxed to a tower of equivalences?
  module Names where
    HomotopyLevel : ℕ → (A : Type{ℓ}) → Type
    HomotopyLevel(𝟎)      (A) = Σ(A)(x ↦ ∀{y} → (y ≡ x))
    HomotopyLevel(𝐒(𝟎))   (A) = ∀{x y : A} → (x ≡ y)
    HomotopyLevel(𝐒(𝐒(n)))(A) = ∀{x y : A} → HomotopyLevel(𝐒(n))(x ≡ y)

    Truncation = HomotopyLevel ∘ 𝐒 ∘ 𝐒

  record HomotopyLevel(n : ℕ) (A : Type{ℓ}) : Type{ℓ} where
    constructor intro
    field proof : Names.HomotopyLevel(n)(A)

  Truncation = HomotopyLevel ∘ 𝐒 ∘ 𝐒

-- TODO: Where should this be stated?
-- ExcludedMiddle : (A : Type{ℓ}) ⦃ equiv-A : Equiv{ℓₑ}(A) ⦄ → Stmt
-- ExcludedMiddle(A) = MereProposition(A) → (IsUnit(A) ∨ IsEmpty(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:
open import Common.Prelude

_test_test_ : Nat → Nat → Nat → Nat
m test_test n = λ i → m + i + n


text:
-- A brief Agda tutorial.
-- Martín Escardó, 7 Sep 2012 (updated to be compatible with Agda 2.4.2 2 Oct 2014).
--
-- Agda is a computer-implemented dialect of Martin-Löf type theory.
-- It can both check and run proofs.
--
-- Propositions are types (also called sets, indicated by the keyword
-- Set), and their witnesses or proofs are programs.
--
-- If one ignores this view/encoding of propositions, Agda is simply a
-- strongly typed, pure, functional programming language with
-- dependent types and other kinds of fancy types.
--
-- All programs normalize in Agda.
---
-- Gödel's system T is included in Agda, but Platek-Scott-Plotkin's
-- PCF is not.  But Agda is much more expressive than system T: it
-- defines many more functions ℕ → ℕ, for example, and encodes much
-- higher ordinals.

-- The Agda wiki http://wiki.portal.chalmers.se/agda/agda.php tells
-- you how to install Agda and get started with editing.
--
-- I recommend the tutorial paper
---    http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf,
-- among others available at
--     http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Documentation
--
-- See also the standard library
--     http://www.cse.chalmers.se/~nad/listings/lib-0.6/README.html
-- which we will not use in this tutorial.

module EscardoTutorial where

-- An inductive definition:

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

-- This notation uses unicode UTF-8. To enter unicode characters in emacs in Agda mode, see
-- http://wiki.portal.chalmers.se/agda/agda.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode
-- (usually LaTeX syntax works).

-- Could instead write the following, which is equivalent with a
-- different notation, using ascii characters only:

data N : Set where
 zero : N
 succ : N -> N
 one  : N

-- But we will use the first definition. (Later we may prove that ℕ
-- and N are isomorphic, as an exercise.)

-- Our first function, inductively defined:

_+_ : ℕ → ℕ → ℕ
x + zero = x
x + succ y = succ(x + y)

-- We can define a simple-recursion combinator:

rec : (X : Set) → X → (X → X) → (ℕ → X)
rec X x f zero = x
rec X x f (succ n) = f(rec X x f n)

-- Or the primitive-recursion combinator:

prim-rec : (X : Set) → X → (ℕ → X → X) → ℕ → X
prim-rec X x f zero = x
prim-rec X x f (succ n) = f n (prim-rec X x f n)

-- Addition can then be instead defined as:

_+₁_ : ℕ → ℕ → ℕ
x +₁ y = rec ℕ x succ y

-- We are using a subscript to indicate a different version. An
-- identifier is a sequence of unicode (UTF-8 encoding) characters not
-- containing white space or reserved characters @.(){};_.
--
-- Quoting from the agda wiki,
-- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.LexicalMatters:
--
-- Furthermore, the following set of reserved words cannot be used as name parts.
--
-- ->         :         =        ?        \           |          →         ∀   --     λ
-- abstract   data      forall   hiding   import      in         infix     infixl   infixr
-- let        module    mutual   open     postulate   primitive  private   public   record
-- renaming   rewrite   using    where    with
-- Prop       Set[0–9]* [0–9]+
--
-- This means that strings like x:A and A→B are valid names. To write
-- the type signature and the function type, white space have to be
-- inserted: x : A, and A → B.
--

-- To illustrate some features, another equivalent definition is this:

rec₁ : (X : Set) → X → (X → X) → (ℕ → X)
rec₁ X x f = h
 where
  h : ℕ → X
  h zero = x
  h (succ n) = f(h n)

-- Indentation matters.

-- The parameter X of the definition of rec/rec₁ may be made implicit,
-- and this is sensible:

rec₂ : {X : Set} → X → (X → X) → (ℕ → X)
rec₂ {X} x f = h
 where
  h : ℕ → X
  h zero = x
  h (succ n) = f(h n)

-- Now we can define addition omitting the type ℕ:

_+₂_ : ℕ → ℕ → ℕ
x +₂ y = rec₂ x succ y

-- Agda then infers (by unification) that this is the only possibly
-- choice for the implicit argument.

-- In cases when the inference fails, or when you want to implicitly
-- supply the implicit parameter for emphasis, you can write:

_+₃_ : ℕ → ℕ → ℕ
x +₃ y = rec₂ {ℕ} x succ y

-- You can also write:

_+₄_ : ℕ → ℕ → ℕ
_+₄_ x y = rec₂ {ℕ} x succ y

-- or even, using η-contraction:

_+₅_ : ℕ → ℕ → ℕ
_+₅_ x = rec₂ {ℕ} x succ

-- or:

_+₆_ : ℕ → ℕ → ℕ
_+₆_ = λ x → rec₂ {ℕ} x succ

-- or, using only ascii characters:

_+₇_ : ℕ → ℕ → ℕ
_+₇_ = \x -> rec₂ {ℕ} x succ

-- I prefer the original definition.

-- You can also declare an associativity and precedence for (the
-- various versions of) _+_ if you wish (valid from now on):

infixl 5 _+_

-- Since we are discussing syntax, let also do:

-- {-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN NATURAL N #-}

-- This allows you to write e.g. 0 to mean zero and 3 to mean
-- Succ(Succ(Succ zero)).

-- So far we have a few definitions. We want to prove something about
-- them.

-- Agda uses the Brouwer-Heyting-Kolmogorov-Curry-Howard
-- representation of propositions as types.
--
-- Types are called sets in Agda syntax, with the keyword "Set".
-- (And in the early accounts by Martin-Löf too.)
--
-- So a proposition is a set.
--
--    * A set may be empty: this represents "false".
--
--    * Or it may have an element: any inhabited set represents "true".
--
-- So a proposition may be true in many ways: an element of its
-- representing set is called a "witness" or a "realizer" or "a
-- proof".
--
--
-- A predicate on a type X is a function A : X → Set.
-- For each element x : X it gives a set A x representing a
-- proposition.
--
--
-- * The BHKCH intepretation of implication:
--
--     A realizer of the proposition "A implies B" is a function that
--     given any realizer of A produces a realizer of B.
--
--     Thus, the function type (A → B), built-in in Martin-Löf theory
--     and in Agda, codes implication.
--
--
-- * The BHKCH intepretation of universal quantification:
--
--     A realizer of "for all x in X, A x" is a function that
--     transforms any x in X into a realizer of A x.
--
--     The interpretation of universal quantification is given by
--     dependent products, again built-in in Martin-Löf theory and in
--     Agda.
--
--     In Martin-Löf type theory, it is written Π.  In Agda, the
--     notation (x : X) → A x is used, where A : X → Set.
--
--     It is the type of functions that map any x : X to an element y : A x.
--     Notice that the type of the output depends on the input.
--
--     Agda allows you to write ∀(x : X) → A x to mean (x : X) → A x.
--     When types can be inferred by Agda, you can also write ∀ x → A x.
--
-- * The BHKCH intepretation of existential quantification:
--
--     A realizer of "there is x in X s.t. A x" is a pair (x , a)
--     where x is in X and a is a realizer of A x.
--
--     In Martin-Löf type theory, Σ is used to define the
--     interpretation of existential quantification.
--
--     In Agda we need to (inductively) define it ourselves:

data Σ {X : Set} (A : X → Set) : Set where
     _,_ : (x₀ : X) → A x₀ → Σ \(x : X) → A x

-- Read Σ \(x : X) → A x as the sum of the sets A x for x : X.  Agda
-- is "intensional", but it uses the η rule.  So Σ \(x : X) → A x is
-- the same as Σ {X} A, because A is the same thing as \(x : X) → A x,
-- and because X can be inferred now, as it is given in the definition
-- \(x : X) → A x.

π₀ : {X : Set} {A : X → Set} → (Σ \(x : X) → A x) → X
π₀(x , a) = x

π₁ : {X : Set} {A : X → Set} → (z : Σ \(x : X) → A x) → A(π₀ z)
π₁(x , a) = a

-- Martin-Löf instead works with the following elimination rule, which
-- is a dependently type version of "uncurrying":

Σ-elim : {X : Set} → {Y : X → Set} →
         {A : (Σ \(x : X) → Y x) → Set}

   → (∀(x : X) → ∀(y : Y x) → A(x , y))
   → ∀(t : (Σ \(x : X) → Y x)) → A t

Σ-elim f(x , y) = f x y

-- Notice that Σ-elim defines the projections:

π₀' : {X : Set} {A : X → Set} → (Σ \(x : X) → A x) → X
π₀' = Σ-elim (λ x a → x)

π₁' : {X : Set} {A : X → Set} → (z : Σ \(x : X) → A x) → A(π₀ z)
π₁' = Σ-elim (λ x a → a)

-- The converse holds if we assume "surjective-pairing", a form of the
-- η-rule for sums. Now this may be confusing: the way we defined Σ
-- using "data" doesn't give you that. But if you define Σ using a
-- record, then you do get that. See
-- http://www.cs.bham.ac.uk/~mhe/agda/SetsAndFunctions.html

-- Cartesian products are a special case of dependent sums, where Y
-- doesn't depend on x : X, which represent conjunctions in the BHKCH
-- interpretation of logic:

_×_ : Set → Set → Set
X × Y = Σ \(x : X) → Y

-- It is also useful to introduce ∃-notation:

∃ : {X : Set} → (A : X → Set) → Set
∃ = Σ

-- We have developed enough material to be able to formulate and prove
-- our first theorem: the Axiom of Choice:

AC : {X Y : Set} {A : X → Y → Set} →

 (∀(x : X) → ∃ \(y : Y) → A x y) → ∃ \(f : X → Y) → ∀(x : X) → A x (f x)

AC g = (λ x → π₀(g x)) , (λ x → π₁(g x))

-- We have a dependently typed version as well (not to be confused
-- with dependent choice, which I will discuss later), with the same
-- proof:

AC' : {X : Set} {Y : X → Set} {A : (x : X) → Y x → Set} →

 (∀(x : X) → ∃ \(y : Y x) → A x y) → ∃ \(f : ((x : X) → Y x)) → ∀(x : X) → A x (f x)

AC' g = ((λ x → π₀(g x)) , (λ x → π₁(g x)))

-- I find the following use of an implicit argument useful in order
-- to achieve a notation close to Martin-Löf's.

Π : {X : Set} → (Y : X → Set) → Set
Π {X} Y = (x : X) → Y x

-- For example the axiom of choice becomes less surprising when we
-- realize that it amounts to

AC-in-ML-notation : {X : Set} {Y : X → Set} {A : (x : X) → Y x → Set} →

 (Π \(x : X) → Σ \(y : Y x) → A x y) → Σ \(f : ((x : X) → Y x)) → Π \(x : X) → A x (f x)

AC-in-ML-notation g = ((λ x → π₀(g x)) , (λ x → π₁(g x)))

-- (The axiom of choice usually fails in a topos, but the above always
-- holds. In fact, the function AC-in-ML-notation is a
-- (pointwise) isomorphism. Exercise: define its inverse in Agda.)

-- Let's return to the natural numbers.
-- We can also write an induction combinator:

induction : {A : ℕ → Set} →

 A zero → (∀(k : ℕ) → A k → A(succ k)) → ∀(n : ℕ) → A n

induction base step 0 = base
induction base step (succ n) = step n (induction base step n)

-- Notice that the realizer of the principle of induction has the same
-- definition as primitive recursion. Only the types are different:
-- that of primitive recursion is less general, and that of induction
-- is the dependent-type generalization.

prim-rec' : {X : Set} → X → (ℕ → X → X) → ℕ → X
prim-rec' = induction

-- The empty type, representing the false proposition.

data ∅ : Set where
 -- no constructors given

-- The "elimintation rule of false", or "ex-falso quod libet", or the
-- function from the empty set to any set:

from-∅ : {X : Set} → ∅ → X
from-∅ ()

-- This is our first encounter of "()" patterns. They assert that a
-- case is impossible (and Agda checks that), or that no constructor
-- is available to perform a match. All uses of () can be reduced to
-- from-∅, but sometimes it is clearer to use the "()" pattern.

-- The type with one element, giving one way of representing the true
-- proposition:

data ① : Set where
 * : ①

-- This is something like the terminal object:

to-① : {X : Set} → X → ①
to-① x = *

-- * The BHKCH intepretation of disjunction is the binary co-product,
--   inductively defined. It is natural to use the symbol "+" to
--   denote the co-product, but in Agda there is no overloading other than
--   constructors defined in (different) "data" definitions. So let's
--   use "⨄" as in the standard library

data _⨄_ (X₀ X₁ : Set) : Set where
 in₀ : X₀ → X₀ ⨄ X₁
 in₁ : X₁ → X₀ ⨄ X₁

-- These constructors correspond to the introduction rules of disjunction.
-- Definition by cases corresponds to the elimination rule:

cases : {X₀ X₁ Y : Set} → (X₀ → Y) → (X₁ → Y) → (X₀ ⨄ X₁ → Y)
cases f₀ f₁ (in₀ x₀) = f₀ x₀
cases f₀ f₁ (in₁ x₁) = f₁ x₁

-- See Bove & Dybjer's paper "Dependent types at work" for
-- a dependently typed version of this:
-- http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
-- Alternatively, work it out yourself as an exercise.

-- Binary co-products can be alternatively defined from sums and the
-- booleans in the presence of the "universe" Set.
--
-- First define the set of binary digits (the booleans with another
-- notation and perspective):

data ② : Set where
 ₀ : ②
 ₁ : ②

-- This amounts to if-then-else:

②-cases : {X : Set} → X → X → ② → X
②-cases x₀ x₁ ₀ = x₀
②-cases x₀ x₁ ₁ = x₁

-- Here is the dependently-typed version:

dep-②-cases : {X : ② → Set} → X ₀ → X ₁ → ((i : ②) → X i)
dep-②-cases x₀ x₁ ₀ = x₀
dep-②-cases x₀ x₁ ₁ = x₁

-- The following has the same definition but a different type:

②-Cases : Set → Set → ② → Set
②-Cases X₀ X₁ ₀ = X₀
②-Cases X₀ X₁ ₁ = X₁

-- Agda has universe polymorphism, but I won't mention it in this
-- tutorial. It requires to rewrite all code we have written and we
-- will write in this tutorial, everytime with a parameter for a
-- universe level. Explore the standard library to see how this works.

_⨄'_ : Set → Set → Set
X₀ ⨄' X₁ = Σ \(i : ②) → ②-Cases X₀ X₁ i

in₀' : {X₀ X₁ : Set} → X₀ → X₀ ⨄' X₁
in₀' x₀ = (₀ , x₀)

in₁' : {X₀ X₁ : Set} → X₁ → X₀ ⨄' X₁
in₁' x₁ = (₁ , x₁)

cases' : {X₀ X₁ Y : Set} → (X₀ → Y) → (X₁ → Y) → (X₀ ⨄' X₁ → Y)
cases' {X₀} {X₁} {Y} f₀ f₁ = h
 where
  Y' : X₀ ⨄' X₁ → Set
  Y' z = Y

  f : (i : ②) → (x : ②-Cases X₀ X₁ i) → Y'(i , x)
  f = dep-②-cases f₀ f₁

  g : (z : X₀ ⨄' X₁) → Y' z
  g = Σ-elim {②} {②-Cases X₀ X₁} {Y'} f

  h : X₀ ⨄' X₁ → Y
  h = g

-- * The BHKCH intepretation of equality:
--
--     Howards idea: x = y is interpreted by a type that is empty if x
--     and y are equal, and has precisely one element if not.
--
--     In set theory (classical or constructive), this can be written
--     { z ∈ 1 | x = y }, where 1 is a singleton, say {0}.
--
--     But notice that this cannot be written down in Martin-Löf's
--     type theory, and already presuposes a notion of equality to be
--     available.
--
--     Martin-Löf's idea: inductively define this type. This is the
--     so-called identity type, which is complicated and hence we will
--     look at it later.

-- Using the universe Set, one can easily define equality on the
-- natural numbers by induction and show that the Martin-Löf induction
-- priciple J holds for this notion of equality on ℕ.

-- Notice that we use four stacked bars to denote the equality type on
-- the type ℕ. Later we will use three to denote the equality type, or
-- identity type, for any type (and in particular ℕ again).

infix 3 _≣_

_≣_ : ℕ → ℕ → Set
0 ≣ 0 = ①
(succ m) ≣ 0 = ∅
0 ≣ (succ n) = ∅
(succ m) ≣ (succ n) = m ≣ n

Reflℕ : ∀ n → n ≣ n
Reflℕ 0 = *
Reflℕ (succ n) = IH
 -- Notice that we needed to inhabit the set ((succ m) ≣ (succ n))
 -- in this case, but we instead inhabited the set (m ≣ n) using IH.
 -- This works because, by definition, ((succ m) ≣ (succ n)) is (m ≣ n).
 where
  IH : n ≣ n
  IH = Reflℕ n

-- We next show that _≣_ is the least reflexive relation on ℕ:

weak-Jℕ : (A : ℕ → ℕ → Set) → (∀ n → A n n) →  ∀ m n → m ≣ n → A m n
weak-Jℕ A φ 0 0 * = φ 0
weak-Jℕ A φ 0 (succ n) ()
weak-Jℕ A φ (succ m) 0 ()
weak-Jℕ A φ (succ m) (succ n) e = weak-Jℕ A' φ' m n e
 where
  A' : ℕ → ℕ → Set
  A' m n = A (succ m) (succ n)
  φ' : ∀ n → A' n n
  φ' n = φ(succ n)

-- If you don't like "()" patterns, you can use the function from-∅
-- (defined above using "()" patterns):

weak-Jℕ' : (A : ℕ → ℕ → Set) → (∀ n → A n n) →  ∀ m n → m ≣ n → A m n
weak-Jℕ' A φ 0 0 * = φ 0
weak-Jℕ' A φ 0 (succ n) e = from-∅ e
weak-Jℕ' A φ (succ m) 0 e = from-∅ e
weak-Jℕ' A φ (succ m) (succ n) e =
 weak-Jℕ' (λ m n → A(succ m)(succ n)) (λ n → φ(succ n)) m n e

-- There is a stronger, dependent(ly typed) version of weak-Jℕ:

Jℕ : (A : (m n : ℕ) → m ≣ n → Set)

   → (∀ n → A n n (Reflℕ n)) →  ∀ m n → ∀(e : m ≣ n) → A m n e

Jℕ A φ 0 0 * = φ 0
Jℕ A φ 0 (succ n) ()
Jℕ A φ (succ m) 0 ()
Jℕ A φ (succ m) (succ n) e =
 Jℕ (λ m n → A (succ m) (succ n)) (λ n → φ(succ n)) m n e

-- Of course we could have defined instead the weak version from the
-- strong one:

weak-Jℕ'' : (A : (m n : ℕ) → Set) → (∀ n → A n n) →  ∀ m n → m ≣ n → A m n
weak-Jℕ'' A = Jℕ (λ m n e → A m n)

-- Jℕ can be regarded as an induction principle for equality on the
-- type ℕ. Several properties of ≣ can be proved using J without
-- reference to the inductive structure of the the type ℕ, and often
-- its weak version suffices.

symℕ : (x y : ℕ) → x ≣ y → y ≣ x
symℕ = weak-Jℕ A φ
 where
  A : (x y : ℕ) → Set
  A x y = y ≣ x
  φ : (x : ℕ) → x ≣ x
  φ = Reflℕ

transℕ : (x y z : ℕ) → x ≣ y → y ≣ z → x ≣ z
transℕ x y z r s =  transℕ' x y r z s
 where
  transℕ' : (x y : ℕ) → x ≣ y → (z : ℕ) → y ≣ z → x ≣ z
  transℕ' = weak-Jℕ A φ
   where
    A : (x y : ℕ) → Set
    A x y = ∀(z : ℕ) → y ≣ z → x ≣ z
    φ : (x : ℕ) → A x x
    φ x z s = s

substℕ : (P : ℕ → Set) → (x y : ℕ) → x ≣ y → P x → P y
substℕ P = weak-Jℕ A φ
 where
  A : (x y : ℕ) → Set
  A x y = P x → P y
  φ : (x : ℕ) → A x x
  φ x p = p

-- Transitivity can be proved using substitution:

sym-transℕ : (x y z : ℕ) → x ≣ y → x ≣ z → y ≣ z
sym-transℕ x y z = rearrange z x y
 where
  rearrange : (z x y : ℕ) → x ≣ y → x ≣ z → y ≣ z
  rearrange z = substℕ (λ x → x ≣ z)

transℕ' : (x y z : ℕ) → x ≣ y → y ≣ z → x ≣ z
transℕ' x y z r s = sym-transℕ y x z (symℕ x y r) s

congℕ→ℕ : (f : ℕ → ℕ) → (x x' : ℕ) → x ≣ x' → f x ≣ f x'
congℕ→ℕ f = weak-Jℕ (λ x x' → f x ≣ f x') (λ x → Reflℕ(f x))

-- As another example, we show that addition is commutative:

zero-is-left-neutral : ∀ n → 0 + n ≣ n
zero-is-left-neutral 0 = *
zero-is-left-neutral (succ n) = IH
             -- We need to inhabit the type (0 + succ n ≣ succ n).
             -- Expanding the definitions,
             --   (0 + succ n ≣ succ n) =
             --   (succ(0 + n) ≣ succ n) =
             --   (0 + n ≣ n).
             -- Here "=" is definitional equality, silently applied by Agda.
 where
  IH : 0 + n ≣ n
  IH = zero-is-left-neutral n

-- Equivalently:

zero-is-left-neutral' : ∀ n → 0 + n ≣ n
zero-is-left-neutral' = induction base step
 where
  base : ①
  base = *
  step : ∀ n → 0 + n ≣ n → 0 + n ≣ n
  step n e = e

-- This with the following shows that, of course, it is equivalent to
-- define addition by induction on the first argument. The proof is by
-- induction on the second argument, following the definition of _+_.

addition-on-first : ∀ m n → (succ m) + n ≣ succ(m + n)
addition-on-first m 0 = Reflℕ m
addition-on-first m (succ n) = IH
 where
  IH : succ m + n ≣ succ(m + n)
  IH = addition-on-first m n

-- Because the situation is symmetric, we can choose any of the two
-- arguments to perform the induction in the following theorem:

addition-commutative : ∀ m n → m + n ≣ n + m
addition-commutative 0 n = zero-is-left-neutral n
addition-commutative (succ m) n = lemma
 where
  IH : m + n ≣ n + m
  IH = addition-commutative m n
  claim : succ(m + n) ≣ succ(n + m)
  claim = congℕ→ℕ succ (m + n) (n + m) IH
  lemma : succ m + n ≣ succ (n + m)
  lemma = transℕ (succ m + n) (succ(m + n)) (succ (n + m))
                 (addition-on-first m n) claim

-- Exercise. Prove the Peano axioms that are not covered above.

-- The above theorem "Jℕ" motivates Martin-Löf's inductive definition
-- of the identity type for any type X:

data _≡_ {X : Set} : X → X → Set where
 refl : {x : X} → x ≡ x

-- Martin-Löf's notation is the following:

Id : (X : Set) → X → X → Set
Id X x y  =  x ≡ y

Refl : (X : Set) → (x : X) → Id X x x
Refl X x = refl {X} {x}

-- The induction principle is as for equality on ℕ defined earlier:

J : {X : Set} → (A : (x x' : X) → x ≡ x' → Set)

   → (∀(x : X) → A x x refl) →  ∀{x x' : X} → ∀(r : x ≡ x') → A x x' r

J A f {x} refl = f x

-- In Agda, one can prove the unique-of-identity proofs principle K by
-- pattern matching:

K : {X : Set} → ∀{x x' : X} → ∀(r s : x ≡ x') → r ≡ s
K refl refl = refl

-- This is not provable in intensional Martin-Löf type theory (Hofmann
-- & Streicher's groupoid interpretation paper).
--
-- However, it is known that the following is provable in MLTT:

pseudo-K : {X : Set} → ∀{x x' : X} → ∀(r : x ≡ x') → (x , refl) ≡ (x' , r)
pseudo-K {X} = J {X} A (λ x → refl)
 where
  A : ∀(x x' : X) → x ≡ x' → Set
  A x x' r = _≡_ {Σ \(x' : X) → x ≡ x'} (x , refl) (x' , r)

-- It has been shown that types with decidable equality, such as ℕ and
-- the booleans, satisfy the K-rule. Moreover, for ℕ it can be easily
-- proved by induction (exercise, which we may eventually do).

-- Conor McBride proved that having the K-rule is equivalent to having
-- pattern matching over refl, which Agda does. But this can be
-- disabled in Agda using the pragma {-# OPTIONS --without-K #-}.
-- Without this pragma, many definitions by pattern matching,
-- including that of J, are accepted, but that of K, and other
-- definitions that require K, are not.

-- Exercise: formulate and prove sym, subst, trans, cong, generalizing
-- the above development for ℕ. Define a weak version of J from J, and
-- use this in your proofs.

-- The propositional "axiom of function extensionality" is

Extensionality : Set₁
Extensionality =
 ∀(X Y : Set) → ∀(f g : X → Y) → (∀(x : X) → f x ≡ g x) → f ≡ g

-- Here we have used the second universe. The first is Set = Set₀.  We
-- have Set₀ : Set₁, Set₁ : Set₂, and so on. The "small" sets (or
-- types) live in Set₀. The large set Extensionality lives in Set₁
-- because it quantifies over elements of Set₀.

-- It is neither possible to show that the set Extensionality is
-- inhabited or that it is empty. That is, the extensionality axiom is
-- independent of MLTT. We can, if we wish, postulate it, or rather
-- postulate an inhabitant:

postulate ext : Extensionality

-- But then ext behaves like a constant, with no computation rules for
-- it. Reduction gets stuck when it encounters this case.

-- The principle of excluded middle is independent of MLTT.

EM : Set₁
EM = ∀(X : Set) → X ⨄ (X → ∅)

-- Notice that (X → ∅) represents negation because ∅ represents false.
-- Notice also that the independence of EM follows from that of
-- Extensionality if we don't have the above postulate.

-- It would be good, too good, to have an inhabitant of EM without
-- violating the computational character of MLTT. It would solve
-- Hilbert's decision problem for large fragments of mathematics,
-- including Peano arithmetic. It would amount to an algorithm for
-- deciding whether a proposition has a realizer, or its negation has
-- a realizer, and would also give the corresponding realizer. As is
-- well known, this is not possible, and this is why EM cannot be
-- inhabited in MLTT.

-- This is not to say that EM is false in MLTT.
-- In fact the set (EM → ∅) cannot be inhabited in MLTT either. This
-- is because MLTT is compatible with classical mathematics (like
-- Bishop mathematics). Set theory, say ZF with an inaccessible
-- cardinal modeling the universe, or with a stack of inaccessible
-- cardinals modelling a hierarchy of universes, can be used to give a
-- model of MLTT in which EM is inhabited (by simply using the
-- principle of excluded middle of ZF, whose consistency is not
-- disputed, even by constructive mathematicians).

-- The negation of EM is also consistent, because recursive models
-- of MLTT, in which an inhabitant of EM needs to be given by an
-- algorithm, exist, so that EM is empty and hence (EM → ∅) is
-- inhabited in such models. There are also (classical and
-- constructive) models in which all functions are continuous. In
-- those models, (EM → ∅) has an inhabitant too.

-- So it is very inaccurate to say that excluded middle "doesn't hold"
-- in Martin-Löf type theory.  What we have is that EM is independent
-- of MLTT. Independence is a meta-theoretical property, which cannot
-- be written down in MLTT itself, of course. Formalized versions of
-- the assertions "all functions are computable" and "all functions
-- are continuous" are also independent. In constructive mathematics
-- in the style of Bishop or Martin-Löf, in which compatibility with
-- classical and computational mathematics is desired, it is very easy
-- to find independent statements, as there are plenty of theorems
-- that hold classically but have no computable realizers (EM is one).

-- To be continued.

Jℕeq : (A : (m n : ℕ) → m ≣ n → Set) → (φ : (∀ n → A n n (Reflℕ n))) →  ∀ m
     → Jℕ A φ m m (Reflℕ m) ≡ φ m
Jℕeq A φ zero = refl
Jℕeq A φ (succ m) = Jℕeq (λ m n → A (succ m) (succ n)) (λ n → φ(succ n)) m

Jℕeq17 : (A : (m n : ℕ) → m ≣ n → Set) → (φ : (∀ n → A n n (Reflℕ n)))
     → Jℕ A φ 17 17 (Reflℕ 17) ≡ φ 17
Jℕeq17 A φ = refl

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

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

module Definition11 where

open import Common.FOL

-- We test the translation of a definition which Agda η-reduces.

P : D → Set
P d = ∃ λ e → d ≡ e
{-# ATP definition P #-}

postulate bar : ∀ {d} → P d → ∃ λ e → e ≡ d
{-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --no-syntactic-equality #-}

open import Agda.Primitive

variable
  ℓ : Level
  A : Set ℓ
  P : A → Set ℓ

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRingSolver.EvalHom where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Int.Base hiding (_+_ ; _·_ ; -_)
open import Cubical.Data.FinData
open import Cubical.Data.Vec
open import Cubical.Data.Bool
open import Cubical.Relation.Nullary.Base

open import Cubical.Algebra.CommRingSolver.Utility
open import Cubical.Algebra.CommRingSolver.RawAlgebra
open import Cubical.Algebra.CommRingSolver.IntAsRawRing
open import Cubical.Algebra.CommRingSolver.HornerForms
open import Cubical.Algebra.CommRingSolver.HornerEval
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring

private
  variable
    ℓ : Level

module HomomorphismProperties (R : CommRing ℓ) where
  private
    νR = CommRing→RawℤAlgebra R
  open CommRingStr (snd R)
  open RingTheory (CommRing→Ring R)
  open IteratedHornerOperations νR

  EvalHom+0 : {n : ℕ} (P : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
      → eval (0ₕ +ₕ P) xs ≡ eval P xs
  EvalHom+0 {n = ℕ.zero} (const x) [] = cong (scalar R) (+Ridℤ x)
  EvalHom+0 {n = ℕ.suc _} P xs = refl

  Eval0H : {n : ℕ} (xs : Vec ⟨ νR ⟩ n)
         → eval {A = νR} 0ₕ xs ≡ 0r
  Eval0H  [] = refl
  Eval0H (x ∷ xs) = refl

  Eval1ₕ : {n : ℕ} (xs : Vec ⟨ νR ⟩ n)
         → eval {A = νR} 1ₕ xs ≡ 1r
  Eval1ₕ [] = refl
  Eval1ₕ (x ∷ xs) =
    eval 1ₕ (x ∷ xs)                             ≡⟨ refl ⟩
    eval (0H ·X+ 1ₕ) (x ∷ xs)                    ≡⟨ combineCasesEval R 0H 1ₕ x xs ⟩
    eval {A = νR} 0H (x ∷ xs) · x + eval 1ₕ xs   ≡⟨ cong (λ u → u · x + eval 1ₕ xs)
                                                                   (Eval0H (x ∷ xs)) ⟩
    0r · x + eval 1ₕ xs                          ≡⟨ cong (λ u → 0r · x + u)
                                                        (Eval1ₕ xs) ⟩
    0r · x + 1r                                  ≡⟨ cong (λ u → u + 1r)
                                                         (0LeftAnnihilates _) ⟩
    0r + 1r                                      ≡⟨ +IdL _ ⟩
    1r ∎

  -EvalDist :
    {n : ℕ} (P : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval (-ₕ P) xs ≡ - eval P xs
  -EvalDist (const x) []   = -DistScalar R x
  -EvalDist 0H  xs =
    eval (-ₕ 0H) xs  ≡⟨ Eval0H xs ⟩
    0r               ≡⟨ sym 0Selfinverse ⟩
    - 0r             ≡⟨ cong -_ (sym (Eval0H xs)) ⟩
    - eval 0H xs     ∎
  -EvalDist (P ·X+ Q) (x ∷ xs) =
      eval (-ₕ (P ·X+ Q)) (x ∷ xs)
    ≡⟨ refl ⟩
      eval ((-ₕ P) ·X+ (-ₕ Q)) (x ∷ xs)
    ≡⟨ combineCasesEval R (-ₕ P) (-ₕ Q) x xs ⟩
      (eval (-ₕ P) (x ∷ xs)) · x + eval (-ₕ Q) xs
    ≡⟨ cong (λ u → u · x + eval (-ₕ Q) xs) (-EvalDist P _) ⟩
      (- eval P (x ∷ xs)) · x + eval (-ₕ Q) xs
    ≡⟨ cong (λ u → (- eval P (x ∷ xs)) · x + u) (-EvalDist Q _) ⟩
      (- eval P (x ∷ xs)) · x + - eval Q xs
    ≡[ i ]⟨ -DistL· (eval P (x ∷ xs)) x i +  - eval Q xs ⟩
      - ((eval P (x ∷ xs)) · x) + (- eval Q xs)
    ≡⟨ -Dist _ _ ⟩
      - ((eval P (x ∷ xs)) · x + eval Q xs)
    ≡[ i ]⟨ - combineCasesEval R P Q x xs (~ i) ⟩
      - eval (P ·X+ Q) (x ∷ xs) ∎

  combineCases+ : {n : ℕ} (P Q : IteratedHornerForms νR (ℕ.suc n))
                  (r s : IteratedHornerForms νR n)
                  (x : fst R) (xs : Vec (fst R) n)
                  → eval ((P ·X+ r) +ₕ (Q ·X+ s)) (x ∷ xs)
                  ≡ eval ((P +ₕ Q) ·X+ (r +ₕ s)) (x ∷ xs)
  combineCases+ {n = n} P Q r s x xs with (isZero νR (P +ₕ Q) and isZero νR (r +ₕ s)) ≟ true
  ... | yes p = compute+ₕEvalBothZero R n P Q r s x xs p
  ... | no p = compute+ₕEvalNotBothZero R n P Q r s x xs (¬true→false _ p)

  +Homeval :
    {n : ℕ} (P Q : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval (P +ₕ Q) xs ≡ (eval P xs) + (eval Q xs)
  +Homeval (const x) (const y) [] = +HomScalar R x y
  +Homeval 0H Q xs =
    eval (0H +ₕ Q) xs            ≡⟨ refl ⟩
    eval Q xs                    ≡⟨ sym (+IdL _) ⟩
    0r + eval Q xs               ≡⟨ cong (λ u → u + eval Q xs) (sym (Eval0H xs)) ⟩
    eval 0H xs + eval Q xs ∎
  +Homeval (P ·X+ Q) 0H xs =
    eval ((P ·X+ Q) +ₕ 0H) xs                    ≡⟨ refl ⟩
    eval (P ·X+ Q) xs                            ≡⟨ sym (+IdR _) ⟩
    eval (P ·X+ Q) xs + 0r
   ≡⟨ cong (λ u → eval (P ·X+ Q) xs + u) (sym (Eval0H xs)) ⟩
    eval (P ·X+ Q) xs + eval 0H xs ∎
  +Homeval (P ·X+ Q) (S ·X+ T) (x ∷ xs) =
    eval ((P ·X+ Q) +ₕ (S ·X+ T)) (x ∷ xs)
   ≡⟨ combineCases+ P S Q T x xs ⟩
    eval ((P +ₕ S) ·X+ (Q +ₕ T)) (x ∷ xs)
   ≡⟨ combineCasesEval R (P +ₕ S) (Q +ₕ T) x xs ⟩
    (eval (P +ₕ S) (x ∷ xs)) · x + eval (Q +ₕ T) xs
   ≡⟨ cong (λ u → (eval (P +ₕ S) (x ∷ xs)) · x + u) (+Homeval Q T xs) ⟩
    (eval (P +ₕ S) (x ∷ xs)) · x + (eval Q xs + eval T xs)
   ≡⟨ cong (λ u → u · x + (eval Q xs + eval T xs)) (+Homeval P S (x ∷ xs)) ⟩
    (eval P (x ∷ xs) + eval S (x ∷ xs)) · x
    + (eval Q xs + eval T xs)
   ≡⟨ cong (λ u → u + (eval Q xs + eval T xs)) (·DistL+ _ _ _) ⟩
    (eval P (x ∷ xs)) · x + (eval S (x ∷ xs)) · x
    + (eval Q xs + eval T xs)
   ≡⟨ +ShufflePairs _ _ _ _ ⟩
    ((eval P (x ∷ xs)) · x + eval Q xs)
    + ((eval S (x ∷ xs)) · x + eval T xs)
   ≡[ i ]⟨ combineCasesEval R P Q x xs (~ i) + combineCasesEval R S T x xs (~ i) ⟩
    eval (P ·X+ Q) (x ∷ xs)
    + eval (S ·X+ T) (x ∷ xs) ∎

  ⋆Homeval : {n : ℕ}
             (r : IteratedHornerForms νR n)
             (P : IteratedHornerForms νR (ℕ.suc n)) (x : ⟨ νR ⟩) (xs : Vec ⟨ νR ⟩ n)
           → eval (r ⋆ P) (x ∷ xs) ≡ eval r xs · eval P (x ∷ xs)

  ⋆0LeftAnnihilates :
    {n : ℕ} (P : IteratedHornerForms νR (ℕ.suc n)) (xs : Vec ⟨ νR ⟩ (ℕ.suc n))
    → eval (0ₕ ⋆ P) xs ≡ 0r
  ⋆0LeftAnnihilates 0H xs = Eval0H xs
  ⋆0LeftAnnihilates {n = ℕ.zero} (P ·X+ Q) (x ∷ xs) = refl
  ⋆0LeftAnnihilates {n = ℕ.suc _} (P ·X+ Q) (x ∷ xs) = refl

  ⋆isZeroLeftAnnihilates :
    {n : ℕ} (r : IteratedHornerForms νR n)
            (P : IteratedHornerForms νR (ℕ.suc n))
    (xs : Vec ⟨ νR ⟩ (ℕ.suc n))
    → isZero νR r ≡ true
    → eval (r ⋆ P) xs ≡ 0r
  ⋆isZeroLeftAnnihilates r P xs isZero-r = evalIsZero R (r ⋆ P) xs (isZeroPresLeft⋆ r P isZero-r)

  ·0LeftAnnihilates :
    {n : ℕ} (P : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval (0ₕ ·ₕ P) xs ≡ 0r
  ·0LeftAnnihilates (const x) xs =
    eval (const _) xs ≡⟨ Eval0H xs ⟩ 0r ∎
  ·0LeftAnnihilates 0H xs = Eval0H xs
  ·0LeftAnnihilates (P ·X+ P₁) xs = Eval0H xs

  ·isZeroLeftAnnihilates :
    {n : ℕ} (P Q : IteratedHornerForms νR n)
    (xs : Vec (fst R) n)
    → isZero νR P ≡ true
    → eval (P ·ₕ Q) xs ≡ 0r
  ·isZeroLeftAnnihilates P Q xs isZeroP = evalIsZero R (P ·ₕ Q) xs (isZeroPresLeft·ₕ P Q isZeroP)

  ·Homeval : {n : ℕ} (P Q : IteratedHornerForms νR n) (xs : Vec ⟨ νR ⟩ n)
    → eval (P ·ₕ Q) xs ≡ (eval P xs) · (eval Q xs)

  combineCases⋆ : {n : ℕ} (x : fst R) (xs : Vec (fst R) n)
                → (r : IteratedHornerForms νR n)
                → (P : IteratedHornerForms νR (ℕ.suc n))
                → (Q : IteratedHornerForms νR n)
                → eval (r ⋆ (P ·X+ Q)) (x ∷ xs) ≡ eval ((r ⋆ P) ·X+ (r ·ₕ Q)) (x ∷ xs)
  combineCases⋆ x xs r P Q with isZero νR r ≟ true
  ... | yes p =
    eval (r ⋆ (P ·X+ Q)) (x ∷ xs)                ≡⟨ ⋆isZeroLeftAnnihilates r (P ·X+ Q) (x ∷ xs) p ⟩
    0r                                           ≡⟨ someCalculation R ⟩
    0r · x + 0r                                  ≡⟨ step1 ⟩
    eval (r ⋆ P) (x ∷ xs) · x + eval (r ·ₕ Q) xs  ≡⟨ sym (combineCasesEval R (r ⋆ P) (r ·ₕ Q) x xs) ⟩
    eval ((r ⋆ P) ·X+ (r ·ₕ Q)) (x ∷ xs) ∎
    where
      step1 : 0r · x + 0r ≡ eval (r ⋆ P) (x ∷ xs) · x + eval (r ·ₕ Q) xs
      step1 i = ⋆isZeroLeftAnnihilates r P (x ∷ xs) p (~ i) · x + ·isZeroLeftAnnihilates r Q xs p (~ i)
  ... | no p with isZero νR r
  ...           | true = byAbsurdity (p refl)
  ...           | false = refl

  ⋆Homeval r 0H x xs =
    eval (r ⋆ 0H) (x ∷ xs)                ≡⟨ refl ⟩
    0r                                    ≡⟨ sym (0RightAnnihilates _) ⟩
    eval r xs · 0r                        ≡⟨ refl ⟩
    eval r xs · eval {A = νR} 0H (x ∷ xs) ∎
  ⋆Homeval r (P ·X+ Q) x xs =
      eval (r ⋆ (P ·X+ Q)) (x ∷ xs)                ≡⟨ combineCases⋆ x xs r P Q ⟩
      eval ((r ⋆ P) ·X+ (r ·ₕ Q)) (x ∷ xs)
    ≡⟨ combineCasesEval R (r ⋆ P) (r ·ₕ Q) x xs ⟩
      (eval (r ⋆ P) (x ∷ xs)) · x + eval (r ·ₕ Q) xs
    ≡⟨ cong (λ u → u · x + eval (r ·ₕ Q) xs) (⋆Homeval r P x xs) ⟩
      (eval r xs · eval P (x ∷ xs)) · x + eval (r ·ₕ Q) xs
    ≡⟨ cong (λ u → (eval r xs · eval P (x ∷ xs)) · x + u) (·Homeval r Q xs) ⟩
      (eval r xs · eval P (x ∷ xs)) · x + eval r xs · eval Q xs
    ≡⟨ cong (λ u → u  + eval r xs · eval Q xs) (sym (·Assoc _ _ _)) ⟩
      eval r xs · (eval P (x ∷ xs) · x) + eval r xs · eval Q xs
    ≡⟨ sym (·DistR+ _ _ _) ⟩
      eval r xs · ((eval P (x ∷ xs) · x) + eval Q xs)
    ≡[ i ]⟨ eval r xs · combineCasesEval R P Q x xs (~ i) ⟩
      eval r xs · eval (P ·X+ Q) (x ∷ xs) ∎

  lemmaForCombineCases· :
    {n : ℕ} (Q : IteratedHornerForms νR n) (P S : IteratedHornerForms νR (ℕ.suc n))
    (xs : Vec (fst R) (ℕ.suc n))
    →  isZero νR (P ·ₕ S) ≡ true
    → eval ((P ·X+ Q) ·ₕ S) xs ≡ eval (Q ⋆ S) xs
  lemmaForCombineCases· Q P S xs isZeroProd with isZero νR (P ·ₕ S)
  ... | true = refl
  ... | false = byBoolAbsurdity isZeroProd

  combineCases· :
    {n : ℕ} (Q : IteratedHornerForms νR n) (P S : IteratedHornerForms νR (ℕ.suc n))
    (xs : Vec (fst R) (ℕ.suc n))
    → eval ((P ·X+ Q) ·ₕ S) xs ≡ eval (((P ·ₕ S) ·X+ 0ₕ) +ₕ (Q ⋆ S)) xs
  combineCases· Q P S (x ∷ xs) with isZero νR (P ·ₕ S) ≟ true
  ... | yes p =
        eval ((P ·X+ Q) ·ₕ S) (x ∷ xs)                          ≡⟨ lemmaForCombineCases· Q P S (x ∷ xs) p ⟩
        eval (Q ⋆ S) (x ∷ xs)                                   ≡⟨ sym (+IdL _) ⟩
        0r + eval (Q ⋆ S) (x ∷ xs)                              ≡⟨ step1 ⟩
        eval ((P ·ₕ S) ·X+ 0ₕ) (x ∷ xs) + eval (Q ⋆ S) (x ∷ xs)  ≡⟨ step2 ⟩
        eval (((P ·ₕ S) ·X+ 0ₕ) +ₕ (Q ⋆ S)) (x ∷ xs)             ∎
        where
          lemma =
            eval ((P ·ₕ S) ·X+ 0ₕ) (x ∷ xs)          ≡⟨ combineCasesEval R (P ·ₕ S) 0ₕ x xs ⟩
            eval (P ·ₕ S) (x ∷ xs) · x + eval 0ₕ xs  ≡[ i ]⟨ evalIsZero R (P ·ₕ S) (x ∷ xs) p i · x + Eval0H xs i ⟩
            0r · x + 0r                             ≡⟨ sym (someCalculation R) ⟩
            0r                                      ∎
          step1 : _ ≡ _
          step1 i = lemma (~ i) + eval (Q ⋆ S) (x ∷ xs)
          step2 = sym (+Homeval ((P ·ₕ S) ·X+ 0ₕ) (Q ⋆ S) (x ∷ xs))
  ... | no p with isZero νR (P ·ₕ S)
  ...           | true = byAbsurdity (p refl)
  ...           | false = refl

  ·Homeval (const x) (const y) [] = ·HomScalar R x y
  ·Homeval 0H Q xs =
    eval (0H ·ₕ Q) xs       ≡⟨ Eval0H xs ⟩
    0r                     ≡⟨ sym (0LeftAnnihilates _) ⟩
    0r · eval Q xs         ≡⟨ cong (λ u → u · eval Q xs) (sym (Eval0H xs)) ⟩
    eval 0H xs · eval Q xs ∎
  ·Homeval (P ·X+ Q) S (x ∷ xs) =
      eval ((P ·X+ Q) ·ₕ S) (x ∷ xs)
    ≡⟨ combineCases· Q P S (x ∷ xs) ⟩
      eval (((P ·ₕ S) ·X+ 0ₕ) +ₕ (Q ⋆ S)) (x ∷ xs)
    ≡⟨ +Homeval ((P ·ₕ S) ·X+ 0ₕ) (Q ⋆ S) (x ∷ xs) ⟩
      eval ((P ·ₕ S) ·X+ 0ₕ) (x ∷ xs) + eval (Q ⋆ S) (x ∷ xs)
    ≡⟨ cong (λ u → u + eval (Q ⋆ S) (x ∷ xs)) (combineCasesEval R (P ·ₕ S) 0ₕ x xs) ⟩
      (eval (P ·ₕ S) (x ∷ xs) · x + eval 0ₕ xs) + eval (Q ⋆ S) (x ∷ xs)
    ≡⟨ cong (λ u → u + eval (Q ⋆ S) (x ∷ xs))
          ((eval (P ·ₕ S) (x ∷ xs) · x + eval 0ₕ xs)
         ≡⟨ cong (λ u → eval (P ·ₕ S) (x ∷ xs) · x + u) (Eval0H xs) ⟩
           (eval (P ·ₕ S) (x ∷ xs) · x + 0r)
         ≡⟨ +IdR _ ⟩
           (eval (P ·ₕ S) (x ∷ xs) · x)
         ≡⟨ cong (λ u → u · x) (·Homeval P S (x ∷ xs)) ⟩
           ((eval P (x ∷ xs) · eval S (x ∷ xs)) · x)
         ≡⟨ sym (·Assoc _ _ _) ⟩
           (eval P (x ∷ xs) · (eval S (x ∷ xs) · x))
         ≡⟨ cong (λ u → eval P (x ∷ xs) · u) (·Comm _ _) ⟩
           (eval P (x ∷ xs) · (x · eval S (x ∷ xs)))
         ≡⟨ ·Assoc _ _ _ ⟩
           (eval P (x ∷ xs) · x) · eval S (x ∷ xs)
          ∎) ⟩
      (eval P (x ∷ xs) · x) · eval S (x ∷ xs) + eval (Q ⋆ S) (x ∷ xs)
    ≡⟨ cong (λ u → (eval P (x ∷ xs) · x) · eval S (x ∷ xs) + u)
            (⋆Homeval Q S x xs) ⟩
      (eval P (x ∷ xs) · x) · eval S (x ∷ xs) + eval Q xs · eval S (x ∷ xs)
    ≡⟨ sym (·DistL+ _ _ _) ⟩
      ((eval P (x ∷ xs) · x) + eval Q xs) · eval S (x ∷ xs)
    ≡⟨ cong (λ u → u · eval S (x ∷ xs)) (sym (combineCasesEval R P Q x xs)) ⟩
      eval (P ·X+ Q) (x ∷ xs) · eval S (x ∷ xs) ∎

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Applicative with law

{-# OPTIONS --without-K --safe #-}
module Experiment.Applicative where

open import Data.Product as Prod
open import Data.Unit
open import Function.Base
open import Relation.Binary.PropositionalEquality

record Functor (F : Set → Set) : Set₁ where
  field
    fmap    : ∀ {A B} → (A → B) → F A → F B
  field
    fmap-id : ∀ {A} (x : F A) → fmap id x ≡ x
    fmap-∘  : ∀ {A B C} (f : B → C) (g : A → B) (x : F A) →
              fmap f (fmap g x) ≡ fmap (f ∘′ g) x
    fmap-cong : ∀ {A B} {f g : A → B} {x : F A} →
                (∀ v → f v ≡ g v) → fmap f x ≡ fmap g x

  _<$>_ : ∀ {A B} → (A → B) → F A → F B
  _<$>_ = fmap

×-assoc : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A × B) × C → A × (B × C)
×-assoc ((x , y) , z) = x , (y , z)

×-assoc⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → A × (B × C) → (A × B) × C
×-assoc⁻¹ (x , (y , z)) = (x , y) , z

app : ∀ {a} {b} {A : Set a} {B : Set b} → (A → B) × A → B
app = uncurry _$′_

record Applicative (F : Set → Set) : Set₁ where
  infixl 5 _<*>_
  field
    functor : Functor F
    unit    : F ⊤
    _<,>_   : ∀ {A B} → F A → F B → F (A × B)
  open Functor functor public

  field
    natural : ∀ {A B C D} (f : A → C) (g : B → D) (fx : F A) (fy : F B) →
              fmap f fx <,> fmap g fy ≡ fmap (Prod.map f g) (fx <,> fy)
    assoc : ∀ {A B C} (fx : F A) (fy : F B) (fz : F C) →
            fmap ×-assoc ((fx <,> fy) <,> fz) ≡ (fx <,> (fy <,> fz))
    unitˡ : ∀ {B} (fy : F B) → fmap proj₂ (unit <,> fy) ≡ fy
    unitʳ : ∀ {A} (fx : F A) → fmap proj₁ (fx <,> unit) ≡ fx

  pure : ∀ {A} → A → F A
  pure {A} x = fmap (λ _ → x) unit

  _<*>_ : ∀ {A B} → F (A → B) → F A → F B
  _<*>_ ff fx = fmap app (ff <,> fx)

  liftA2 : ∀ {A B C} → (A → B → C) → F A → F B → F C
  liftA2 f fx fy = fmap (uncurry f) (fx <,> fy)

  natural₁ : ∀ {A B C} (f : A → C) (fx : F A) (fy : F B) →
             fmap f fx <,> fy ≡ fmap (Prod.map₁ f) (fx <,> fy)
  natural₁ f fx fy = begin
    fmap f fx <,> fy               ≡⟨ cong (fmap f fx <,>_) $ sym $ fmap-id fy ⟩
    fmap f fx <,> fmap id fy       ≡⟨ natural f id fx fy ⟩
    fmap (Prod.map₁ f) (fx <,> fy) ∎
    where open ≡-Reasoning

  natural₂ : ∀ {A B D} (g : B → D) (fx : F A) (fy : F B) →
             fx <,> fmap g fy ≡ fmap (Prod.map₂ g) (fx <,> fy)
  natural₂ g fx fy = begin
    fx <,> fmap g fy               ≡⟨ cong (_<,> fmap g fy) $ sym $ fmap-id fx ⟩
    fmap id fx <,> fmap g fy       ≡⟨ natural id g fx fy ⟩
    fmap (Prod.map₂ g) (fx <,> fy) ∎
    where open ≡-Reasoning

  assoc⁻¹ : ∀ {A B C} (fx : F A) (fy : F B) (fz : F C) →
            fmap ×-assoc⁻¹ (fx <,> (fy <,> fz)) ≡ (fx <,> fy) <,> fz
  assoc⁻¹ fx fy fz = begin
    fmap ×-assoc⁻¹ (fx <,> (fy <,> fz))
      ≡⟨ sym $ cong (fmap ×-assoc⁻¹) (assoc fx fy fz) ⟩
    fmap ×-assoc⁻¹ (fmap ×-assoc ((fx <,> fy) <,> fz))
      ≡⟨ fmap-∘ ×-assoc⁻¹ ×-assoc ((fx <,> fy) <,> fz) ⟩
    fmap (×-assoc⁻¹ ∘′ ×-assoc) ((fx <,> fy) <,> fz)
      ≡⟨⟩
    fmap id ((fx <,> fy) <,> fz)
      ≡⟨ fmap-id ((fx <,> fy) <,> fz) ⟩
    (fx <,> fy) <,> fz
      ∎
    where open ≡-Reasoning

  unit-pure : unit ≡ pure tt
  unit-pure = begin
    unit                 ≡⟨ sym $ fmap-id unit ⟩
    fmap id unit         ≡⟨ refl ⟩
    fmap (λ _ → tt) unit ∎
    where open ≡-Reasoning

  fmap-pure : ∀ {A B} (f : A → B) (x : A) → fmap f (pure x) ≡ pure (f x)
  fmap-pure f x = begin
    fmap f (fmap (λ _ → x) unit) ≡⟨ fmap-∘ f (λ _ → x) unit ⟩
    fmap (λ _ → f x) unit        ∎
    where open ≡-Reasoning

  unitˡʳ : ∀ {A} (fx : F A) → fmap proj₂ (unit <,> fx) ≡ fmap proj₁ (fx <,> unit)
  unitˡʳ fx = trans (unitˡ fx) (sym $ unitʳ fx)

  unitˡ′ : ∀ {B} (fy : F B) → unit <,> fy ≡ fmap (tt ,_) fy
  unitˡ′ fy = begin
    unit <,> fy
      ≡⟨ sym $ fmap-id (unit <,> fy) ⟩
    fmap id (unit <,> fy)
      ≡⟨ fmap-cong (λ _ → refl) ⟩
    fmap ((tt ,_) ∘′ proj₂) (unit <,> fy)
      ≡⟨ sym $ fmap-∘ (tt ,_) proj₂ (unit <,> fy) ⟩
    fmap (tt ,_) (fmap proj₂ (unit <,> fy))
      ≡⟨ cong (fmap (tt ,_)) (unitˡ fy) ⟩
    fmap (tt ,_) fy
      ∎
    where open ≡-Reasoning

  unitʳ′ : ∀ {A} (fx : F A) → fx <,> unit ≡ fmap (_, tt) fx
  unitʳ′ fx = begin
    fx <,> unit
      ≡⟨ sym $ fmap-id (fx <,> unit) ⟩
    fmap id (fx <,> unit)
      ≡⟨⟩
    fmap ((_, tt) ∘′ proj₁) (fx <,> unit)
      ≡⟨ sym $ fmap-∘ (_, tt) proj₁ (fx <,> unit) ⟩
    fmap (_, tt) (fmap proj₁ (fx <,> unit))
      ≡⟨ cong (fmap (_, tt)) (unitʳ fx) ⟩
    fmap (_, tt) fx
      ∎
    where open ≡-Reasoning

  <,>-pureˡ : ∀ {A B} (x : A) (fy : F B) → pure x <,> fy ≡ fmap (x ,_) fy
  <,>-pureˡ x fy = begin
    fmap (λ _ → x) unit <,> fy
      ≡⟨ natural₁ (λ _ → x) unit fy ⟩
    fmap (Prod.map₁ (λ _ → x)) (unit <,> fy)
      ≡⟨ cong (fmap (Prod.map₁ (λ _ → x))) (unitˡ′ fy) ⟩
    fmap (Prod.map₁ (λ _ → x)) (fmap (tt ,_) fy)
      ≡⟨ fmap-∘ (Prod.map₁ (λ _ → x)) (tt ,_) fy ⟩
    fmap (Prod.map₁ (λ _ → x) ∘′ (tt ,_)) fy
      ≡⟨⟩
    fmap (x ,_) fy
      ∎
    where open ≡-Reasoning

  <,>-pureʳ : ∀ {A B} (fx : F A) (y : B) → fx <,> pure y ≡ fmap (_, y) fx
  <,>-pureʳ fx y = begin
    fx <,> fmap (λ _ → y) unit
      ≡⟨ natural₂ (λ _ → y) fx unit ⟩
    fmap (Prod.map₂ (λ _ → y)) (fx <,> unit)
      ≡⟨ cong (fmap (Prod.map₂ (λ _ → y))) (unitʳ′ fx) ⟩
    fmap (Prod.map₂ (λ _ → y)) (fmap (_, tt) fx)
      ≡⟨ fmap-∘ (Prod.map₂ (λ _ → y)) (_, tt) fx ⟩
    fmap (Prod.map₂ (λ _ → y) ∘′ (_, tt)) fx
      ≡⟨⟩
    fmap (_, y) fx ∎
    where open ≡-Reasoning

  pure-<,> : ∀ {A B} (x : A) (y : B) → pure x <,> pure y ≡ pure (x , y)
  pure-<,> x y = begin
    pure x <,> pure y    ≡⟨ <,>-pureˡ x (pure y) ⟩
    fmap (x ,_) (pure y) ≡⟨ fmap-pure (x ,_) y ⟩
    pure (x , y)         ∎
    where open ≡-Reasoning

  <*>-fmap : ∀ {A B} (f : A → B) (fx : F A) → pure f <*> fx ≡ fmap f fx
  <*>-fmap f fx = begin
    fmap app (pure f <,> fx)  ≡⟨ cong (fmap app) $ <,>-pureˡ f fx ⟩
    fmap app (fmap (f ,_) fx) ≡⟨ fmap-∘ app (f ,_) fx ⟩
    fmap (app ∘′ (f ,_)) fx   ≡⟨⟩
    fmap f fx                 ∎
    where open ≡-Reasoning

  <*>-identity : ∀ {A} (v : F A) → pure id <*> v ≡ v
  <*>-identity v = begin
   fmap (uncurry _$′_) (pure id <,> v)  ≡⟨ cong (fmap (uncurry _$′_)) $ <,>-pureˡ id v ⟩
   fmap (uncurry _$′_) (fmap (id ,_) v) ≡⟨ fmap-∘ (uncurry _$′_) (id ,_) v ⟩
   fmap (uncurry _$′_ ∘′ (id ,_)) v     ≡⟨ fmap-cong (λ _ → refl) ⟩
   fmap id v                            ≡⟨ fmap-id v ⟩
   v                                    ∎
   where open ≡-Reasoning

  <*>-composition : ∀ {A B C} (u : F (A → C)) (v : F (B → A)) (w : F B) →
                    pure _∘′_ <*> u <*> v <*> w ≡ u <*> (v <*> w)
  <*>-composition u v w = begin
    pure _∘′_ <*> u <*> v <*> w
      ≡⟨ cong (λ t → t <*> v <*> w) $ <*>-fmap _∘′_ u ⟩
    fmap _∘′_ u <*> v <*> w
      ≡⟨⟩
    fmap app (fmap _∘′_ u <,> v) <*> w
      ≡⟨⟩
    fmap app (fmap app (fmap _∘′_ u <,> v) <,> w)
      ≡⟨ cong (λ t → fmap app (fmap app t <,> w)) $ natural₁ _∘′_ u v ⟩
    fmap app (fmap app (fmap (Prod.map₁ _∘′_) (u <,> v)) <,> w)
      ≡⟨ cong (fmap app) $ natural₁ app (fmap (Prod.map₁ _∘′_) (u <,> v)) w ⟩
    fmap app (fmap (Prod.map₁ app) (fmap (Prod.map₁ _∘′_) (u <,> v) <,> w))
      ≡⟨ fmap-∘ app (Prod.map₁ app) _ ⟩
    fmap (app ∘′ Prod.map₁ app) (fmap (Prod.map₁ _∘′_) (u <,> v) <,> w)
      ≡⟨ cong (fmap (app ∘′ Prod.map₁ app)) $ natural₁ (Prod.map₁ _∘′_) (u <,> v) w ⟩
    fmap (app ∘′ Prod.map₁ app) (fmap (Prod.map₁ (Prod.map₁ _∘′_)) ((u <,> v) <,> w))
      ≡⟨ fmap-∘ (app ∘′ Prod.map₁ app) (Prod.map₁ (Prod.map₁ _∘′_)) _ ⟩
    fmap (app ∘′ Prod.map₁ app ∘′ Prod.map₁ (Prod.map₁ _∘′_)) ((u <,> v) <,> w)
      ≡⟨ fmap-cong (λ _ → refl) ⟩
    fmap (app ∘′ Prod.map₂ app ∘′ ×-assoc) ((u <,> v) <,> w)
      ≡⟨ sym $ fmap-∘ (app ∘′ Prod.map₂ app) ×-assoc ((u <,> v) <,> w) ⟩
    fmap (app ∘′ Prod.map₂ app) (fmap ×-assoc ((u <,> v) <,> w))
      ≡⟨ cong (fmap (app ∘′ Prod.map₂ app)) (assoc u v w) ⟩
    fmap (app ∘′ Prod.map₂ app) (u <,> (v <,> w))
      ≡⟨ sym $ fmap-∘ app (Prod.map₂ app) (u <,> (v <,> w)) ⟩
    fmap app (fmap (Prod.map₂ app) (u <,> (v <,> w)))
      ≡⟨ sym $ cong (fmap app) $ natural₂ app u (v <,> w) ⟩
    fmap app (u <,> fmap app (v <,> w))
      ≡⟨⟩
    u <*> (v <*> w)
      ∎
    where open ≡-Reasoning

  <*>-homomorphism : ∀ {A B} (f : A → B) (x : A) → pure f <*> pure x ≡ pure (f x)
  <*>-homomorphism f x = begin
    pure f <*> pure x ≡⟨ <*>-fmap f (pure x) ⟩
    fmap f (pure x)   ≡⟨ fmap-pure f x ⟩
    pure (f x)        ∎
    where open ≡-Reasoning

  <*>-interchange : ∀ {A B} (u : F (A → B)) (y : A) →
    u <*> pure y ≡ pure (_$ y) <*> u
  <*>-interchange u y = begin
    u <*> pure y             ≡⟨⟩
    fmap app (u <,> pure y)  ≡⟨ cong (fmap app) (<,>-pureʳ u y) ⟩
    fmap app (fmap (_, y) u) ≡⟨ fmap-∘ app (_, y) u ⟩
    fmap (app ∘′ (_, y)) u   ≡⟨⟩
    fmap (_$ y) u            ≡⟨ sym $ <*>-fmap (_$ y) u ⟩
    pure (_$ y) <*> u        ∎
    where open ≡-Reasoning

  liftA2-defn : ∀ {A B C} (f : A → B → C) (fx : F A) (fy : F B) →
    liftA2 f fx fy ≡ pure f <*> fx <*> fy
  liftA2-defn f fx fy = begin
    fmap (uncurry f) (fx <,> fy)              ≡⟨⟩
    fmap (app ∘′ Prod.map₁ f) (fx <,> fy)     ≡⟨ sym $ fmap-∘ app (Prod.map₁ f) (fx <,> fy) ⟩
    fmap app (fmap (Prod.map₁ f) (fx <,> fy)) ≡⟨ cong (fmap app) $ sym $ natural₁ f fx fy ⟩
    fmap app (fmap f fx <,> fy)               ≡⟨⟩
    fmap f fx <*> fy                          ≡⟨ sym $ cong (_<*> fy) $ <*>-fmap f fx ⟩
    pure f <*> fx <*> fy                      ∎
    where open ≡-Reasoning

  liftA2-cong : ∀ {A B C} {f g : A → B → C} {fx : F A} {fy : F B} →
    (∀ x y → f x y ≡ g x y) → liftA2 f fx fy ≡ liftA2 g fx fy
  liftA2-cong {_} {_} {_} {f} {g} {fx} {gx} f≡g = fmap-cong λ v → f≡g (proj₁ v) (proj₂ v)

  <*>-defn : ∀ {A B} (ff : F (A → B)) (fx : F A) → ff <*> fx ≡ liftA2 _$′_ ff fx
  <*>-defn ff fx = refl

  -- liftA2 f fx fy = pure f <*> fx <*> fy
{-
forall x y. p (q x y) = f x . g y
it follows from the above that

liftA2 p (liftA2 q u v) = liftA2 f u . liftA2 g v
-}

record ApplicativeViaAp (F : Set → Set) : Set₁ where
  infixl 5 _<*>_
  field
    functor : Functor F
    pure    : ∀ {A} → A → F A
    _<*>_   : ∀ {A B} → F (A → B) → F A → F B
  open Functor functor public
  field
    identity     : ∀ {A} (fx : F A) → pure id <*> fx ≡ fx
    composition  : ∀ {A B C} (u : F (A → C)) (v : F (B → A)) (w : F B) →
                   pure _∘′_ <*> u <*> v <*> w ≡ u <*> (v <*> w)
    homomorphism : ∀ {A B} (f : A → B) (x : A) → pure f <*> pure x ≡ pure (f x)
    interchange  : ∀ {A B} (u : F (A → B)) (y : A) →
                   u <*> pure y ≡ pure (_$ y) <*> u
    <*>-fmap     : ∀ {A B} (f : A → B) (fx : F A) → pure f <*> fx ≡ fmap f fx

  _<,>_ : ∀ {A B} → F A → F B → F (A × B)
  fx <,> fy = pure _,_ <*> fx <*> fy

  liftA2 : ∀ {A B C} → (A → B → C) → F A → F B → F C
  liftA2 f fx fy = fmap (uncurry f) (fx <,> fy)

  unit : F ⊤
  unit = pure tt
{-
  <,>-natural : ∀ {A B C D} (f : A → C) (g : B → D) (fx : F A) (fy : F B) →
    fmap f fx <,> fmap g fy ≡ fmap (Prod.map f g) (fx <,> fy)
  <,>-natural f g fx fy = begin
    pure _,_ <*> fmap f fx <*> fmap g fy
      ≡⟨ cong (_<*> fmap g fy) $ <*>-fmap _,_ (fmap f fx) ⟩
    fmap _,_ (fmap f fx) <*> fmap g fy
      ≡⟨ cong (_<*> fmap g fy) $ fmap-∘ _,_ f fx ⟩
    fmap (_,_ ∘′ f) fx <*> fmap g fy
      ≡⟨ {!   !} ⟩
    fmap (Prod.map f g) (fmap _,_ fx <*> fy)
      ≡⟨ sym $ cong (λ t → fmap (Prod.map f g) (t <*> fy)) $ <*>-fmap _,_ fx ⟩
    fmap (Prod.map f g) (pure _,_ <*> fx <*> fy)
      ∎
    where open ≡-Reasoning

  liftA2-defn : ∀ {A B C} (f : A → B → C) (fx : F A) (fy : F B) →
    liftA2 f fx fy ≡ pure f <*> fx <*> fy
  liftA2-defn f fx fy = {!   !}
-}
record Monad (F : Set → Set) : Set₁ where
  infixl 5 _>>=_
  field
    functor : Functor F
    return  : ∀ {A} → A → F A
    join    : ∀ {A} → F (F A) → F A

  open Functor functor public
  field
    assoc          : ∀ {A} (fffx : F (F (F A))) → join (fmap join fffx) ≡ join (join fffx)
    identityˡ      : ∀ {A} (fx : F A) → join (fmap return fx) ≡ fx
    identityʳ      : ∀ {A} (fx : F A) → join (return fx) ≡ fx
    join-natural   : ∀ {A B} (f : A → B) (ffx : F (F A)) →
                     join (fmap (fmap f) ffx) ≡ fmap f (join ffx)
    return-natural : ∀ {A B} (f : A → B) (x : A) → return (f x) ≡ fmap f (return x)

  _>>=_ : ∀ {A B} → F A → (A → F B) → F B
  _>>=_ m k = join (fmap k m)

  _=<<_ : ∀ {A B} → (A → F B) → F A → F B
  _=<<_ = flip _>>=_

  liftM : ∀ {A B} → (A → B) → F A → F B
  liftM f fx = fx >>= λ x → return (f x)

  ap : ∀ {A B} → F (A → B) → F A → F B
  ap ff fx = ff >>= λ f → fmap f fx

  pair : ∀ {A B} → F A → F B → F (A × B)
  pair fx fy = fx >>= λ x → fmap (λ y → x , y) fy

  unitM : F ⊤
  unitM = return tt

  liftM-is-fmap : ∀ {A B} (f : A → B) (fx : F A) → liftM f fx ≡ fmap f fx
  liftM-is-fmap f fx = begin
    join (fmap (λ x → return (f x)) fx) ≡⟨ sym $ cong join $ fmap-∘ return f fx ⟩
    join (fmap return (fmap f fx))      ≡⟨ identityˡ (fmap f fx) ⟩
    fmap f fx                           ∎
    where open ≡-Reasoning

  >>=-cong : ∀ {A B} {f g : A → F B} {fx : F A} →
    (∀ x → f x ≡ g x) → fx >>= f ≡ fx >>= g
  >>=-cong f≡g = cong join (fmap-cong f≡g)

  fmap-lemma : ∀ {A B C} (f : A → B) (fx : F A) (k : B → F C) →
    fmap f fx >>= k ≡ fx >>= λ x → k (f x)
  fmap-lemma f fx k = begin
    fmap f fx >>= k                  ≡⟨⟩
    join (fmap k (fmap f fx))        ≡⟨ cong join (fmap-∘ k f fx) ⟩
    join (fmap (λ x → (k (f x))) fx) ∎
    where open ≡-Reasoning

  liftM-lemma : ∀ {A B C} (f : A → B) (fx : F A) (k : B → F C) →
    liftM f fx >>= k ≡ fx >>= λ x → k (f x)
  liftM-lemma f fx k = begin
    liftM f fx >>= k       ≡⟨ cong (_>>= k) $ liftM-is-fmap f fx ⟩
    fmap f fx >>= k        ≡⟨ fmap-lemma f fx k ⟩
    fx >>= (λ x → k (f x)) ∎
    where open ≡-Reasoning

{-
kleisli-assoc
-}
{-
  kleisli-identityˡ : ∀ {A B : Set} (f : A → F B) (x : A) → join (fmap return (f x)) ≡ f x
  kleisli-identityˡ f x = identityˡ (f x)

  kleisli-identityʳ : ∀ {A B : Set} (f : A → F B) (x : A) → join (fmap f (return x)) ≡ f x
  kleisli-identityʳ f x = >>=-identityˡ f x
-}

  fmap-return : ∀ {A B} (f : A → B) (x : A) → fmap f (return x) ≡ return (f x)
  fmap-return f x = sym $ return-natural f x

  >>=-identityˡ : ∀ {A B} (a : A) (k : A → F B) → return a >>= k ≡ k a
  >>=-identityˡ a k = begin
    join (fmap k (return a)) ≡⟨ cong join $ fmap-return k a ⟩
    join (return (k a))      ≡⟨ identityʳ (k a) ⟩
    k a                      ∎
    where open ≡-Reasoning

  >>=-identityʳ : ∀ {A} (m : F A) → m >>= return ≡ m
  >>=-identityʳ m = identityˡ m

  >>=-assoc : ∀ {A B C} (m : F A) (k : A → F B) (h : B → F C) →
              m >>= (λ x → k x >>= h) ≡ (m >>= k) >>= h
  >>=-assoc m k h = begin
    m >>= (λ x → k x >>= h)
      ≡⟨⟩
    join (fmap (λ x → join (fmap h (k x))) m)
      ≡⟨ sym $ cong join $ fmap-∘ join (fmap h ∘′ k) m ⟩
    join (fmap join (fmap (fmap h ∘′ k) m))
      ≡⟨ assoc (fmap (fmap h ∘′ k) m) ⟩
    join (join (fmap (fmap h ∘′ k) m))
      ≡⟨ cong join (begin
      join (fmap (fmap h ∘′ k) m)     ≡⟨ sym $ cong join $ fmap-∘ (fmap h) k m ⟩
      join (fmap (fmap h) (fmap k m)) ≡⟨ join-natural h (fmap k m) ⟩
      fmap h (join (fmap k m))        ∎ ) ⟩
    join (fmap h (join (fmap k m)))
      ≡⟨⟩
    (m >>= k) >>= h
      ∎
    where open ≡-Reasoning

  fmap->>= : ∀ {A B C} (f : B → C) (m : F A) (k : A → F B) →
             fmap f (m >>= k) ≡ m >>= (λ x → fmap f (k x))
  fmap->>= f m k = begin
    fmap f (m >>= k)                ≡⟨⟩
    fmap f (join (fmap k m))        ≡⟨ sym $ join-natural f (fmap k m) ⟩
    join (fmap (fmap f) (fmap k m)) ≡⟨ cong join $ fmap-∘ (fmap f) k m ⟩
    join (fmap (fmap f ∘′ k) m)     ≡⟨⟩
    m >>= (λ x → fmap f (k x))      ∎
    where open ≡-Reasoning

  fmap-move : ∀ {A B C D} (f : C → D) (g : A → B → C) (m1 : F A) (m2 : F B) →
         fmap f (m1 >>= λ x → fmap (g x) m2) ≡ m1 >>= (λ x → fmap (f ∘′ g x) m2)
  fmap-move f g m1 m2 = begin
    fmap f (m1 >>= λ x → fmap (g x) m2)   ≡⟨ fmap->>= f m1 (λ x → fmap (g x) m2) ⟩
    m1 >>= (λ x → fmap f (fmap (g x) m2)) ≡⟨ >>=-cong (λ x → fmap-∘ f (g x) m2) ⟩
    m1 >>= (λ x → fmap (f ∘′ g x) m2)     ∎
    where open ≡-Reasoning
{-
  applicative : Applicative F
  applicative = record
    { functor = functor
    ; unit    = unitM
    ; _<,>_   = pair
    ; natural = λ f g fx fy → begin
      pair (fmap f fx) (fmap g fy)
        ≡⟨⟩
      fmap f fx >>= (λ x → fmap (λ y → x , y) (fmap g fy))
        ≡⟨ fmap-lemma f fx _ ⟩
      fx >>= (λ x → fmap (λ y → f x , y) (fmap g fy) )
        ≡⟨ >>=-cong (λ x → fmap-∘ (f x ,_) g fy) ⟩
      fx >>= (λ x → fmap (λ y → f x , g y) fy)
        ≡⟨⟩
      fx >>= (λ x → fmap (λ y → Prod.map f g (x , y) ) fy )
        ≡⟨ sym $ fmap-move (Prod.map f g) _,_ fx fy ⟩
      fmap (Prod.map f g) (fx >>= λ x → fmap (λ y → x , y) fy)
        ≡⟨⟩
      fmap (Prod.map f g) (pair fx fy)
        ∎
    ; assoc   = λ fx fy fz →
      fmap ×-assoc (pair (pair fx fy) fz)
        ≡⟨⟩
      fmap ×-assoc ((fx >>= λ x → fmap (x ,_) fy) >>= λ xy → fmap (xy ,_) fz)
        ≡⟨ {! sym $ >>=-assoc fx   !} ⟩
      fx >>= (λ x → fy >>= λ y → fmap (λ z → x , (y , z)) fz)
        ≡⟨ sym $ >>=-cong (λ x → fmap-move (x ,_) _,_ fy fz) ⟩
      fx >>= (λ x → fmap (x ,_) (fy >>= λ y → fmap (y ,_) fz))
        ≡⟨⟩
      pair fx (pair fy fz)
        ∎
    ; unitˡ   = {!   !}
    ; unitʳ   = {!   !}
    }
    where open ≡-Reasoning
-}


text:
------------------------------------------------------------------------------
-- FOTC version of a nested recursive function
------------------------------------------------------------------------------

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

-- From: Ana Bove and Venanzio Capretta. Nested general recursion and
-- partiality in type theory. Vol. 2152 of LNCS. 2001.

module FOT.FOTC.Program.Nest.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Data.Nat.Type
open import FOTC.Program.Nest.Nest

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

nestCong : ∀ {m n} → m ≡ n → nest m ≡ nest n
nestCong refl = refl

nest-x≡0 : ∀ {n} → N n → nest n ≡ zero
nest-x≡0 nzero = nest-0
nest-x≡0 (nsucc {n} Nn) =
  nest (succ₁ n) ≡⟨ nest-S n ⟩
  nest (nest n)  ≡⟨ nestCong (nest-x≡0 Nn) ⟩
  nest zero      ≡⟨ nest-0 ⟩
  zero           ∎

nest-N : ∀ {n} → N n → N (nest n)
nest-N Nn = subst N (sym (nest-x≡0 Nn)) nzero

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import HoTT
open import homotopy.Bouquet

{-
Various lemmas that will be used in cohomology.DisjointlyPointedSet.
Many of them, for example the choice lemma about coproducts, should be
put into core/.
-}

module homotopy.DisjointlyPointedSet where

module _ {i} where

  is-separable : (X : Ptd i) → Type i
  is-separable X = has-dec-onesided-eq (pt X)

  abstract
    is-separable-is-prop : {X : Ptd i}
      → is-prop (is-separable X)
    is-separable-is-prop = has-dec-onesided-eq-is-prop

  MinusPoint : (X : Ptd i) → Type i
  MinusPoint X = Σ (de⊙ X) (pt X ≠_)

  MinusPoint-prop : (X : Ptd i) → SubtypeProp (de⊙ X) i
  MinusPoint-prop X = (pt X ≠_) , ⟨⟩

  abstract
    MinusPoint-has-dec-eq : {X : Ptd i}
      → has-dec-eq (de⊙ X)
      → has-dec-eq (MinusPoint X)
    MinusPoint-has-dec-eq {X} X-dec =
      Subtype-has-dec-eq (MinusPoint-prop X) X-dec

  unite-pt : (X : Ptd i) → (⊤ ⊔ MinusPoint X → de⊙ X)
  unite-pt X (inl _) = pt X
  unite-pt X (inr (x , _)) = x

  separate-pt : {X : Ptd i}
    → is-separable X
    → (de⊙ X → ⊤ ⊔ (Σ (de⊙ X) (pt X ≠_)))
  separate-pt dec x with dec x
  separate-pt dec x | inl _  = inl unit
  separate-pt dec x | inr ¬p = inr (x , ¬p)

  has-disjoint-pt : (X : Ptd i) → Type i
  has-disjoint-pt X = is-equiv (unite-pt X)

  separable-has-disjoint-pt : {X : Ptd i}
    → is-separable X → has-disjoint-pt X
  separable-has-disjoint-pt {X} dec =
    is-eq _ (separate-pt dec) unite-sep sep-unite where
      abstract
        sep-unite : ∀ x → separate-pt dec (unite-pt X x) == x
        sep-unite (inl _) with dec (pt X)
        sep-unite (inl _) | inl _  = idp
        sep-unite (inl _) | inr ¬p = ⊥-rec (¬p idp)
        sep-unite (inr (x , ¬p)) with dec x
        sep-unite (inr (x , ¬p)) | inl p   = ⊥-rec (¬p p)
        sep-unite (inr (x , ¬p)) | inr ¬p' = ap inr $ pair= idp (prop-has-all-paths ¬p' ¬p)

        unite-sep : ∀ x → unite-pt X (separate-pt dec x) == x
        unite-sep x with dec x
        unite-sep x | inl p = p
        unite-sep x | inr ¬p = idp

  disjoint-pt-is-separable : {X : Ptd i}
    → has-disjoint-pt X → is-separable X
  disjoint-pt-is-separable unite-ise x with unite.g x | unite.f-g x
    where module unite = is-equiv unite-ise
  disjoint-pt-is-separable unite-ise x | inl unit       | p   = inl p
  disjoint-pt-is-separable unite-ise x | inr (y , pt≠y) | y=x = inr λ pt=x → pt≠y (pt=x ∙ ! y=x)

  separable-unite-equiv : ∀ {X}
    → is-separable X
    → (⊤ ⊔ MinusPoint X ≃ de⊙ X)
  separable-unite-equiv dX = _ , separable-has-disjoint-pt dX

module _ {i j k} n (A : Type i) (B : Type j) where
  {- Hmm. Where should we put this lemma? -}
  abstract
    ⊔-has-choice-implies-inr-has-choice : has-choice n (A ⊔ B) k → has-choice n B k
    ⊔-has-choice-implies-inr-has-choice ⊔-ac W =
      transport is-equiv (λ= lemma₃)
        (snd lemma₂ ∘ise ⊔-ac W' ∘ise is-equiv-inverse (snd (Trunc-emap lemma₁))) where
          W' : A ⊔ B → Type k
          W' (inl _) = Lift {j = k} ⊤
          W' (inr b) = W b

          lemma₁ : Π (A ⊔ B) W' ≃ Π B W
          lemma₁ = equiv to from to-from from-to where
            to : Π (A ⊔ B) W' → Π B W
            to f b = f (inr b)

            from : Π B W → Π (A ⊔ B) W'
            from f (inl a) = lift tt
            from f (inr b) = f b

            abstract
              to-from : ∀ f → to (from f) == f
              to-from f = λ= λ b → idp

              from-to : ∀ f → from (to f) == f
              from-to f = λ= λ{(inl a) → idp; (inr b) → idp}

          lemma₂ : Π (A ⊔ B) (Trunc n ∘ W') ≃ Π B (Trunc n ∘ W)
          lemma₂ = equiv to from to-from from-to where
            to : Π (A ⊔ B) (Trunc n ∘ W') → Π B (Trunc n ∘ W)
            to f b = f (inr b)

            from : Π B (Trunc n ∘ W) → Π (A ⊔ B) (Trunc n ∘ W')
            from f (inl a) = [ lift tt ]
            from f (inr b) = f b

            abstract
              to-from : ∀ f → to (from f) == f
              to-from f = λ= λ b → idp

              from-to : ∀ f → from (to f) == f
              from-to f = λ= λ{
                (inl a) → Trunc-elim
                  {P = λ t → [ lift tt ] == t}
                  (λ _ → idp) (f (inl a));
                (inr b) → idp}

          lemma₃ : ∀ f → –> lemma₂ (unchoose (<– (Trunc-emap lemma₁) f)) == unchoose f
          lemma₃ = Trunc-elim
            {P = λ f → –> lemma₂ (unchoose (<– (Trunc-emap lemma₁) f)) == unchoose f}
            (λ f → λ= λ b → idp)

module _ {i j} {n} {X : Ptd i} (X-sep : is-separable X) where
  abstract
    MinusPoint-has-choice : has-choice n (de⊙ X) j → has-choice n (MinusPoint X) j
    MinusPoint-has-choice X-ac =
      ⊔-has-choice-implies-inr-has-choice n ⊤ (MinusPoint X) $
        transport! (λ A → has-choice n A j) (ua (_ , separable-has-disjoint-pt X-sep)) X-ac

module _ {i} {X : Ptd i} (X-sep : is-separable X) where

  Bouquet-equiv-X : Bouquet (MinusPoint X) 0 ≃ de⊙ X
  Bouquet-equiv-X = equiv to from to-from from-to where
    from : de⊙ X → BigWedge {A = MinusPoint X} (λ _ → ⊙Bool)
    from x with X-sep x
    from x | inl p  = bwbase
    from x | inr ¬p = bwin (x , ¬p) false

    module To = BigWedgeRec {A = MinusPoint X} {X = λ _ → ⊙Bool}
      (pt X) (λ{_ true → pt X; (x , _) false → x}) (λ _ → idp)
    to = To.f

    abstract
      from-to : ∀ x → from (to x) == x
      from-to = BigWedge-elim base* in* glue* where
        base* : from (pt X) == bwbase
        base* with X-sep (pt X)
        base* | inl _  = idp
        base* | inr ¬p = ⊥-rec (¬p idp)

        in* : (wp : MinusPoint X) (b : Bool)
          → from (to (bwin wp b)) == bwin wp b
        in* wp true with X-sep (pt X)
        in* wp true | inl _ = bwglue wp
        in* wp true | inr pt≠pt = ⊥-rec (pt≠pt idp)
        in* (x , pt≠x) false with X-sep x
        in* (x , pt≠x) false | inl pt=x = ⊥-rec (pt≠x pt=x)
        in* (x , pt≠x) false | inr pt≠'x =
          ap (λ ¬p → bwin (x , ¬p) false) $ prop-has-all-paths pt≠'x pt≠x

        glue* : (wp : MinusPoint X)
          → base* == in* wp true [ (λ x → from (to x) == x) ↓ bwglue wp ]
        glue* wp = ↓-∘=idf-from-square from to $ ap (ap from) (To.glue-β wp) ∙v⊡ square where
          square : Square base* idp (bwglue wp) (in* wp true)
          square with X-sep (pt X)
          square | inl _ = br-square (bwglue wp)
          square | inr ¬p = ⊥-rec (¬p idp)

      to-from : ∀ x → to (from x) == x
      to-from x with X-sep x
      to-from x | inl pt=x = pt=x
      to-from x | inr pt≠x = idp

  Bouquet-⊙equiv-X : ⊙Bouquet (MinusPoint X) 0 ⊙≃ X
  Bouquet-⊙equiv-X = ≃-to-⊙≃ Bouquet-equiv-X idp

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- Normalisation by evaluation
------------------------------------------------------------------------

import Axiom.Extensionality.Propositional as E
import Level
open import Data.Universe

-- The code makes use of the assumption that propositional equality of
-- functions is extensional.

module README.DependentlyTyped.NBE
  (Uni₀ : Universe Level.zero Level.zero)
  (ext : E.Extensionality Level.zero Level.zero)
  where

open import Data.Empty
open import Data.Product renaming (curry to c)
open import deBruijn.Substitution.Data
open import Function hiding (_∋_) renaming (const to k)
import README.DependentlyTyped.NormalForm as NF
open NF Uni₀ renaming ([_] to [_]n)
import README.DependentlyTyped.Term as Term; open Term Uni₀
import README.DependentlyTyped.Term.Substitution as S; open S Uni₀
import Relation.Binary.PropositionalEquality as P
open import Relation.Nullary using (¬_)

open P.≡-Reasoning

-- The values that are used by the NBE algorithm.

import README.DependentlyTyped.NBE.Value as Value
open Value Uni₀ public

-- Weakening for the values.

import README.DependentlyTyped.NBE.Weakening as Weakening
open Weakening Uni₀ ext public

-- Application.

infix 9 [_]_·̌_

[_]_·̌_ : ∀ {Γ sp₁ sp₂} σ →
         V̌alue Γ (π sp₁ sp₂ , σ) → (v : V̌alue Γ (fst σ)) →
         V̌alue Γ (snd σ /̂ ŝub ⟦̌ v ⟧)
[ _ ] f ·̌ v = proj₁ f ε v

abstract

  -- Lifting can be expressed using žero.

  ∘̂-ŵk-▻̂-žero : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) σ →
                ρ̂ ∘̂ ŵk ▻̂[ σ ] ⟦ žero _ (proj₂ σ /̂I ρ̂) ⟧n ≅-⇨̂ ρ̂ ↑̂ σ
  ∘̂-ŵk-▻̂-žero ρ̂ σ = begin
    [ ρ̂ ∘̂ ŵk ▻̂ ⟦ žero _ _ ⟧n ]  ≡⟨ ▻̂-cong P.refl P.refl (ňeutral-to-normal-identity _ (var zero)) ⟩
    [ ρ̂ ∘̂ ŵk ▻̂ ⟦ var zero ⟧  ]  ≡⟨ P.refl ⟩
    [ ρ̂ ↑̂                    ]  ∎

mutual

  -- Evaluation.

  eval : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
         Γ ⊢ σ → Sub V̌al ρ̂ → V̌alue Δ (σ /̂ ρ̂)
  eval (var x)   ρ = x /∋ ρ
  eval (ƛ t)     ρ = (eval[ƛ t ] ρ) , eval[ƛ t ] ρ well-behaved
  eval (t₁ · t₂) ρ = eval[ t₁ · t₂ ] ρ

  -- Some abbreviations.

  eval[ƛ_] : ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ} →
             Γ ▻ σ ⊢ τ → Sub V̌al ρ̂ → V̌alue-π Δ _ _ (IType-π σ τ /̂I ρ̂)
  eval[ƛ t ] ρ Γ₊ v = eval t (V̌al-subst.wk-subst₊ Γ₊ ρ ▻ v)

  eval[_·_] : ∀ {Γ Δ sp₁ sp₂ σ} {ρ̂ : Γ ⇨̂ Δ} →
              Γ ⊢ (π sp₁ sp₂ , σ) → (t₂ : Γ ⊢ fst σ) → Sub V̌al ρ̂ →
              V̌alue Δ (snd σ /̂ ŝub ⟦ t₂ ⟧ ∘̂ ρ̂)
  eval[_·_] {σ = σ} t₁ t₂ ρ =
    cast ([ σ /I ρ ] eval t₁ ρ ·̌ eval t₂ ρ)
    where
    cast = P.subst (λ v → V̌alue _ (snd σ /̂ ⟦ ρ ⟧⇨ ↑̂ /̂ ŝub v))
                   (≅-Value-⇒-≡ $ P.sym $ eval-lemma t₂ ρ)

  abstract

    -- The ƛ case is well-behaved.

    eval[ƛ_]_well-behaved :
      ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ} (t : Γ ▻ σ ⊢ τ) (ρ : Sub V̌al ρ̂) →
      W̌ell-behaved _ _ (IType-π σ τ /I ρ) (eval[ƛ t ] ρ)
    eval[ƛ_]_well-behaved {σ = σ} {τ = τ} t ρ Γ₊ v =
      let υ  = IType-π σ τ /I ρ in begin
      [ (⟦̌ υ ∣ eval[ƛ t ] ρ ⟧-π /̂Val ŵk₊ Γ₊) ˢ ⟦̌ v ⟧ ]  ≡⟨ ˢ-cong (/̂Val-cong (P.sym $ eval-lemma-ƛ t ρ) P.refl) P.refl ⟩
      [ (c ⟦ t ⟧ /̂Val ⟦ ρ ⟧⇨ ∘̂ ŵk₊ Γ₊) ˢ ⟦̌ v ⟧       ]  ≡⟨ P.refl ⟩
      [ ⟦ t ⟧ /̂Val (⟦ ρ ⟧⇨ ∘̂ ŵk₊ Γ₊ ▻̂ ⟦̌ v ⟧)         ]  ≡⟨ eval-lemma t _ ⟩
      [ ⟦̌ eval t (V̌al-subst.wk-subst₊ Γ₊ ρ ▻ v) ⟧    ]  ∎

    -- An unfolding lemma.

    eval-· :
      ∀ {Γ Δ sp₁ sp₂ σ} {ρ̂ : Γ ⇨̂ Δ}
      (t₁ : Γ ⊢ π sp₁ sp₂ , σ) (t₂ : Γ ⊢ fst σ) (ρ : Sub V̌al ρ̂) →
      eval[ t₁ · t₂ ] ρ ≅-V̌alue [ σ /I ρ ] eval t₁ ρ ·̌ eval t₂ ρ
    eval-· {σ = σ} t₁ t₂ ρ =
      drop-subst-V̌alue (λ v → snd σ /̂ ⟦ ρ ⟧⇨ ↑̂ /̂ ŝub v)
                       (≅-Value-⇒-≡ $ P.sym $ eval-lemma t₂ ρ)

    -- The evaluator is correct (with respect to the standard
    -- semantics).

    eval-lemma : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (t : Γ ⊢ σ) (ρ : Sub V̌al ρ̂) →
                 ⟦ t ⟧ /Val ρ ≅-Value ⟦̌ eval t ρ ⟧
    eval-lemma (var x)             ρ = V̌al-subst./̂∋-⟦⟧⇨ x ρ
    eval-lemma (ƛ t)               ρ = eval-lemma-ƛ t ρ
    eval-lemma (_·_ {σ = σ} t₁ t₂) ρ = begin
      [ ⟦ t₁ · t₂ ⟧ /Val ρ                           ]  ≡⟨ P.refl ⟩
      [ (⟦ t₁ ⟧ /Val ρ) ˢ (⟦ t₂ ⟧ /Val ρ)            ]  ≡⟨ ˢ-cong (eval-lemma t₁ ρ) (eval-lemma t₂ ρ) ⟩
      [ ⟦̌_⟧ {σ = σ /I ρ} (eval t₁ ρ) ˢ ⟦̌ eval t₂ ρ ⟧ ]  ≡⟨ proj₂ (eval t₁ ρ) ε (eval t₂ ρ) ⟩
      [ ⟦̌ [ σ /I ρ ] eval t₁ ρ ·̌ eval t₂ ρ ⟧         ]  ≡⟨ ⟦̌⟧-cong (P.sym $ eval-· t₁ t₂ ρ) ⟩
      [ ⟦̌ eval[ t₁ · t₂ ] ρ ⟧                        ]  ∎

    private

      eval-lemma-ƛ :
        ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ} (t : Γ ▻ σ ⊢ τ) (ρ : Sub V̌al ρ̂) →
        ⟦ ƛ t ⟧ /Val ρ ≅-Value ⟦̌ IType-π σ τ /I ρ ∣ eval[ƛ t ] ρ ⟧-π
      eval-lemma-ƛ {σ = σ} {τ = τ} t ρ =
        let υ  = IType-π σ τ /I ρ
            ρ↑ = V̌al-subst.wk-subst₊ (σ / ρ ◅ ε) ρ ▻ v̌ar ⊙ zero

        in begin
        [ c ⟦ t ⟧ /Val ρ          ]  ≡⟨ P.refl ⟩
        [ c (⟦ t ⟧ /̂Val ⟦ ρ ⟧⇨ ↑̂) ]  ≡⟨ curry-cong $ /̂Val-cong (P.refl {x = [ ⟦ t ⟧ ]})
                                                                         (P.sym $ ∘̂-ŵk-▻̂-žero ⟦ ρ ⟧⇨ _) ⟩
        [ c (⟦ t ⟧ /Val ρ↑)       ]  ≡⟨ curry-cong (eval-lemma t ρ↑) ⟩
        [ c ⟦̌ eval t ρ↑ ⟧         ]  ≡⟨ P.sym $ unfold-⟦̌∣⟧-π υ (eval[ƛ t ] ρ) ⟩
        [ ⟦̌ υ ∣ eval[ƛ t ] ρ ⟧-π  ]  ∎

-- Normalisation.

normalise : ∀ {Γ σ} → Γ ⊢ σ → Γ ⊢ σ ⟨ no ⟩
normalise t = řeify _ (eval t V̌al-subst.id)

-- Normalisation is semantics-preserving.

normalise-lemma : ∀ {Γ σ} (t : Γ ⊢ σ) → ⟦ t ⟧ ≅-Value ⟦ normalise t ⟧n
normalise-lemma t = eval-lemma t V̌al-subst.id

-- Some congruence lemmas.

·̌-cong :
  ∀ {Γ₁ sp₁₁ sp₂₁ σ₁}
    {f₁ : V̌alue Γ₁ (π sp₁₁ sp₂₁ , σ₁)} {v₁ : V̌alue Γ₁ (fst σ₁)}
    {Γ₂ sp₁₂ sp₂₂ σ₂}
    {f₂ : V̌alue Γ₂ (π sp₁₂ sp₂₂ , σ₂)} {v₂ : V̌alue Γ₂ (fst σ₂)} →
  σ₁ ≅-IType σ₂ → _≅-V̌alue_ {σ₁ = -, σ₁} f₁ {σ₂ = -, σ₂} f₂ →
  v₁ ≅-V̌alue v₂ →
  [ σ₁ ] f₁ ·̌ v₁ ≅-V̌alue [ σ₂ ] f₂ ·̌ v₂
·̌-cong P.refl P.refl P.refl = P.refl

eval-cong :
  ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {t₁ : Γ₁ ⊢ σ₁} {ρ₁ : Sub V̌al ρ̂₁}
    {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {t₂ : Γ₂ ⊢ σ₂} {ρ₂ : Sub V̌al ρ̂₂} →
  t₁ ≅-⊢ t₂ → ρ₁ ≅-⇨ ρ₂ → eval t₁ ρ₁ ≅-V̌alue eval t₂ ρ₂
eval-cong P.refl P.refl = P.refl

normalise-cong :
  ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁}
    {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
  t₁ ≅-⊢ t₂ → normalise t₁ ≅-⊢n normalise t₂
normalise-cong P.refl = P.refl

abstract

  -- Note that we can /not/ prove that normalise takes semantically
  -- equal terms to identical normal forms, assuming extensionality
  -- and the existence of a universe code which decodes to an empty
  -- type:

  normal-forms-not-unique :
    E.Extensionality Level.zero Level.zero →
    (∃ λ (bot : U₀) → ¬ El₀ bot) →
    ¬ (∀ {Γ σ} (t₁ t₂ : Γ ⊢ σ) →
       ⟦ t₁ ⟧ ≅-Value ⟦ t₂ ⟧ → normalise t₁ ≅-⊢n normalise t₂)
  normal-forms-not-unique ext (bot , empty) hyp = ⊥-elim (x₁≇x₂ x₁≅x₂)
    where
    Γ : Ctxt
    Γ = ε ▻ (⋆ , _) ▻ (⋆ , _) ▻ (el , k bot)

    x₁ : Γ ∋ (⋆ , _)
    x₁ = suc (suc zero)

    x₂ : Γ ∋ (⋆ , _)
    x₂ = suc zero

    x₁≇x₂ : ¬ (ne ⋆ (var x₁) ≅-⊢n ne ⋆ (var x₂))
    x₁≇x₂ ()

    ⟦x₁⟧≡⟦x₂⟧ : ⟦ var x₁ ⟧ ≅-Value ⟦ var x₂ ⟧
    ⟦x₁⟧≡⟦x₂⟧ = P.cong [_] (ext λ γ → ⊥-elim $ empty $ proj₂ γ)

    norm-x₁≅norm-x₂ : normalise (var x₁) ≅-⊢n normalise (var x₂)
    norm-x₁≅norm-x₂ = hyp (var x₁) (var x₂) ⟦x₁⟧≡⟦x₂⟧

    lemma : (x : Γ ∋ (⋆ , _)) → normalise (var x) ≅-⊢n ne ⋆ (var x)
    lemma x = begin
      [ normalise (var x)        ]n  ≡⟨ P.refl ⟩
      [ ne ⋆ (x /∋ V̌al-subst.id) ]n  ≡⟨ ne-cong $ ≅-Value-⋆-⇒-≅-⊢n $ V̌al-subst./∋-id x ⟩
      [ ne ⋆ (var x)             ]n  ∎

    x₁≅x₂ : ne ⋆ (var x₁) ≅-⊢n ne ⋆ (var x₂)
    x₁≅x₂ = begin
      [ ne ⋆ (var x₁)      ]n  ≡⟨ P.sym $ lemma x₁ ⟩
      [ normalise (var x₁) ]n  ≡⟨ norm-x₁≅norm-x₂ ⟩
      [ normalise (var x₂) ]n  ≡⟨ lemma x₂ ⟩
      [ ne ⋆ (var x₂)      ]n  ∎

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Showing natural numbers
------------------------------------------------------------------------

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

module Data.Nat.Show where

open import Data.Nat
open import Relation.Nullary.Decidable using (True)
open import Data.String.Base as String using (String)
open import Data.Digit
open import Data.Product using (proj₁)
open import Function
open import Data.List.Base

-- showInBase b n is a string containing the representation of n in
-- base b.

showInBase : (base : ℕ)
             {base≥2 : True (2 ≤? base)}
             {base≤16 : True (base ≤? 16)} →
             ℕ → String
showInBase base {base≥2} {base≤16} n =
  String.fromList $
  map (showDigit {base≤16 = base≤16}) $
  reverse $
  proj₁ $ toDigits base {base≥2 = base≥2} n

-- show n is a string containing the decimal expansion of n (starting
-- with the most significant digit).

show : ℕ → String
show = showInBase 10


text:
module Issue641 where
Foo : Set
Foo = Set


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Group.Subgroup where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

open import Cubical.Algebra
open import Cubical.Algebra.Group.Morphism
open import Cubical.Algebra.Monoid.Submonoid

open import Cubical.Relation.Unary
open import Cubical.Relation.Unary.Subtype

open import Cubical.HITs.PropositionalTruncation

record IsSubgroup {c ℓ} (G : Group c) (Member : Pred ⟨ G ⟩ ℓ) : Type (ℓ-max c ℓ) where
  constructor issubgroup

  private module G = Group G

  field
    preservesOp : G._•_ Preserves₂ Member
    preservesInv : G._⁻¹ Preserves Member
    preservesId : G.ε ∈ Member

  isSubmonoid : IsSubmonoid G.monoid Member
  isSubmonoid = record
    { preservesOp = preservesOp
    ; preservesId = preservesId
    }

  open IsSubmonoid isSubmonoid hiding (preservesOp; preservesId; _^_) public

  _⁻¹ : Op₁ Carrier
  (x , subx) ⁻¹ = x G.⁻¹ , preservesInv subx

  inverseˡ : LeftInverse ε _⁻¹ _•_
  inverseˡ _ = ΣPathTransport→PathΣ _ _ (G.inverseˡ _ , isProp[ Member ] _ _ _)

  inverseʳ : RightInverse ε _⁻¹ _•_
  inverseʳ _ = ΣPathTransport→PathΣ _ _ (G.inverseʳ _ , isProp[ Member ] _ _ _)

  inverse : Inverse ε _⁻¹ _•_
  inverse = inverseˡ , inverseʳ

  isGroup : IsGroup Carrier _•_ ε _⁻¹
  isGroup = record
    { isMonoid = isMonoid
    ; inverse = inverse
    }

  group : Group _
  group = record { isGroup = isGroup }

  open Group group using
    ( _^_
    ; _/_
    ; _/ˡ_
    ; inv-uniqueˡ
    ; inv-uniqueʳ
    ; cancelˡ
    ; cancelʳ
    ) public

record Subgroup {c} (G : Group c) ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  constructor mksubgroup

  private module G = Group G

  field
    Member : Pred ⟨ G ⟩ ℓ
    isSubgroup : IsSubgroup G Member

  open IsSubgroup isSubgroup public

  submonoid : Submonoid G.monoid ℓ
  submonoid = record { isSubmonoid = isSubmonoid }

  open Submonoid submonoid using (submagma; subsemigroup)

instance
  SubgroupCarrier : ∀ {c ℓ} {G : Group c} → HasCarrier (Subgroup G ℓ) _
  SubgroupCarrier = record { ⟨_⟩ = Subgroup.Carrier }

private
  variable
    c ℓ : Level
    G : Group c

module _ {G : Group c} where
  open Group G

  ε-isSubgroup : IsSubgroup G ｛ ε ｝
  ε-isSubgroup = record
    { preservesOp = map2 λ p q → cong₂ _•_ p q ∙ identityʳ ε
    ; preservesInv = map λ p → cong _⁻¹ p ∙ cancelʳ ε (inverseˡ ε ∙ sym (identityʳ ε))
    ; preservesId = ∣ refl ∣
    }

  ε-subgroup : Subgroup G _
  ε-subgroup = record { isSubgroup = ε-isSubgroup }

  U-isSubgroup : IsSubgroup G U
  U-isSubgroup = record {} -- trivial

  U-subgroup : Subgroup G _
  U-subgroup = record { isSubgroup = U-isSubgroup }

IsNormal : Subgroup G ℓ → Type _
IsNormal {G = G} N =
  ∀ ((n , _) : ⟨ N ⟩) (g : ⟨ G ⟩) → g • n • g ⁻¹ ∈ Subgroup.Member N
  where
    open Group G

NormalSubgroup : Group c → (ℓ : Level) → Type _
NormalSubgroup G ℓ = Σ (Subgroup G ℓ) IsNormal


text:
-- An ATP definition must be used with functions.

-- This error is detected by Syntax.Translation.ConcreteToAbstract.

module ATPBadDefinition1 where

data Bool : Set where
  false true : Bool

{-# ATP definition false #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
-- Andreas, 2017-01-20, issue #2329

-- Neutral sizes cannot be used by the size solver,
-- thus, should be handled by coerceSize.

-- {-# OPTIONS -v tc:10 #-}
-- {-# OPTIONS -v tc.conv.coerce:20 #-}
-- {-# OPTIONS -v tc.size:20 #-}
-- {-# OPTIONS -v tc.size.solve:50 #-}

open import Agda.Builtin.Size

record R (i : Size) : Set where
  field
    j : Size< i

postulate
  f : ∀ i → R i

works : ∀ i → R i
R.j (works i) = R.j {i} (f i)

test : ∀ i → R i
R.j (test i) = R.j (f i)

-- Error WAS:
-- Unsolved constraint:
-- ↑ R.j (f i) =< i : Size

max_forks_repo_name: Agda-zh/agda


text:
module VecMap where

open import Prelude

map : forall {A B n} -> (A -> B) -> Vec A n -> Vec B n
map f xs = {!!}

max_stars_repo_name: carlostome/martin

max_issues_repo_name: carlostome/martin

max_forks_repo_name: carlostome/martin


text:
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_)

open import IMP
open import OperationalSemantics
open import Hoare

wp : ∀{l} → com → assn {l} → assn {l}
wp c Q s = ∀ t → ⦅ c , s ⦆⇒ t → Q t

fatto : ∀{P Q : assn} {c}
      → ⊨[ P ] c [ Q ]
      → (∀ s → P s → wp c Q s)
fatto = λ z s z₁ t → z z₁

fatto-converse : ∀{P Q : assn} {c}
      → (∀ s → P s → wp c Q s)
      → ⊨[ P ] c [ Q ]
fatto-converse = (λ z {s} {t} z₁ → z s z₁ t)

wp-hoare : ∀ c {l} {Q : assn {l}}
  → ⊢[ wp c Q ] c [ Q ]
wp-hoare SKIP = Conseq (λ s z → z s Skip) Skip (λ s z → z)
wp-hoare (x ::= a) = Conseq (λ s wpe → wpe (s [ x ::= aval a s ]) Loc) Loc (λ s r → r)
wp-hoare (c :: c₁) = Comp (Conseq (λ s z x x₁ x₂ x₃ → z x₂ (Comp x₁ x₃)) (wp-hoare c) (λ s z → z)) (wp-hoare c₁)
wp-hoare (IF x THEN c ELSE c₁) = If (Conseq (λ s z x x₁ → proj₁ z x (IfTrue (proj₂ z) x₁)) (wp-hoare c) (λ s z → z))
                                    (Conseq (λ s z x x₁ → proj₁ z x (IfFalse (proj₂ z) x₁)) (wp-hoare c₁) (λ s z → z))
wp-hoare (WHILE b DO c) =
  Conseq (λ s x → x)
         (While (Conseq (λ s z x x₁ x₂ x₃ → proj₁ z x₂ (WhileTrue (proj₂ z) x₁ x₃))
                        (wp-hoare c)
                        (λ s z → z)))
         (λ s z → proj₁ z s (WhileFalse (proj₂ z)))

completeness : ∀ c {P Q : assn}
  → ⊨[ P ] c [ Q ]
  → ⊢[ P ] c [ Q ]
completeness c cc = Conseq (fatto cc) (wp-hoare c) (λ r x → x)

max_stars_repo_name: iwilare/imp-semantics

max_issues_repo_name: iwilare/imp-semantics

max_forks_repo_name: iwilare/imp-semantics


text:
{-# OPTIONS --type-in-type #-}

module DescFix where

open import DescTT

aux : (C : Desc)(D : Desc)(P : Mu C -> Set)(x : [| D |] (Mu C)) -> Set
aux C id          P (con y) = P (con y) * aux C C P y
aux C (const K)   P k       = Unit
aux C (prod D D') P (s , t) = aux C D P s * aux C D' P t
aux C (sigma S T) P (s , t) = aux C (T s) P t
aux C (pi S T)    P f       = (s : S) -> aux C (T s) P (f s)

gen : (C : Desc)(D : Desc)(P : Mu C -> Set)
  (rec : (y : [| C |] Mu C) -> aux C C P y -> P (con y))
  (x : [| D |] Mu C) -> aux C D P x
gen C id          P rec (con x) = rec x (gen C C P rec x) , gen C C P rec x
gen C (const K)   P rec k       = Void
gen C (prod D D') P rec (s , t) = gen C D P rec s , gen C D' P rec t
gen C (sigma S T) P rec (s , t) = gen C (T s) P rec t
gen C (pi S T)    P rec f       = \ s -> gen C (T s) P rec (f s)

fix : (D : Desc)(P : Mu D -> Set)
  (rec : (y : [| D |] Mu D) -> aux D D P y -> P (con y))
  (x : Mu D) -> P x
fix D P rec (con x) = rec x (gen D D P rec x)

plus : Nat -> Nat -> Nat
plus (con (Ze , Void)) n = n
plus (con (Suc , m)) n = suc (plus m n)

fib : Nat -> Nat
fib = fix NatD (\ _ -> Nat) help
  where
    help : (m : [| NatD |] Nat) -> aux NatD NatD (\ _ -> Nat) m -> Nat
    help (Ze , x) a = suc ze
    help (Suc , con (Ze , _)) a = suc ze
    help (Suc , con (Suc , con n)) (fib-n , (fib-sn , a)) = plus fib-n fib-sn

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
-- Andreas, 2014-09-23
-- Syntax declaration for overloaded constructor.

-- {-# OPTIONS -v scope.operators:50 #-}

syntax c x = ⟦ x ⟧

data D1 : Set where
  c : D1

data D2 : Set where
  c : D1 → D2

test : D2
test = ⟦ c ⟧

-- Should work.


text:
-- P: (vcd) <E[send c v]> | <F[recv d]>  --> (vcd) <E[c]> | <F[(d,v)]>

-- P: (vcd) <E[close c]> | <F[wait d]>  --> (vcd) <E[()]> | <F[()]>
module Properties.StepCloseWait where

open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All
open import Data.Product
open import Data.Sum

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel
open import Values
open import Session
open import Schedule

open import ProcessSyntax
open import ProcessRun

open import Properties.Base

mkclose : ∀ {Φ} → Expr (TUnit ∷ Φ) TUnit → Expr (TChan send! ∷ Φ) TUnit
mkclose = λ e → letbind (left (split-all-right _)) (close (here [])) e

mkwait : ∀ {Φ} → Expr (TUnit ∷ Φ) TUnit → Expr (TChan send? ∷ Φ) TUnit
mkwait = λ e → letbind (left (split-all-right _)) (wait (here [])) e

module General where

  mklhs : ∀ {Φ Φ₁ Φ₂}
    → Split Φ Φ₁ Φ₂
    → Expr (TUnit ∷ Φ₁) TUnit
    → Expr (TUnit ∷ Φ₂) TUnit
    → Proc Φ
  mklhs sp e f =
    res (delay send!)
        (par (left (rght sp))
             (exp (mkclose e)) (exp (mkwait f)))

  mkrhs : ∀ {Φ Φ₁ Φ₂}
    → Split Φ Φ₁ Φ₂
    → Expr (TUnit ∷ Φ₁) TUnit
    → Expr (TUnit ∷ Φ₂) TUnit
    → Proc Φ
  mkrhs sp e f =
    par sp (exp (letbind (split-all-right _) (unit []) e))
           (exp (letbind (split-all-right _) (unit []) f))

  -- obviously true, but requires a nasty inductive proof
  postulate
    weaken2-ident : ∀ {G Φ} (ϱ : VEnv G Φ) → weaken2-venv [] [] ϱ ≡ ϱ

  postulate
    weaken1-ident : ∀ {G Φ} (ϱ : VEnv G Φ) → weaken1-venv [] ϱ ≡ ϱ

  reductionT : Set
  reductionT =
    ∀ { Φ Φ₁ Φ₂ }
    (sp : Split Φ Φ₁ Φ₂)
    (ϱ : VEnv [] Φ)
    (p : ∃ λ ϱ₁ → ∃ λ ϱ₂ →
           split-env sp (lift-venv ϱ) ≡ (((nothing ∷ []) , (nothing ∷ [])) , (ss-both ss-[]) , ϱ₁ , ϱ₂))
    (e : Expr (TUnit ∷ Φ₁) TUnit)
    (f : Expr (TUnit ∷ Φ₂) TUnit) →
    let lhs = (runProc [] (mklhs sp e f) ϱ) in
    let rhs = (runProc [] (mkrhs sp e f) ϱ) in
    one-step lhs ≡
    (Closed , nothing ∷ proj₁ rhs , lift-threadpool (proj₂ rhs))

  reduction : reductionT
  reduction{Φ}{Φ₁}{Φ₂} sp ϱ p e f
    with ssplit-refl-left-inactive []
  ... | G' , ina-G' , ss-GG'
    with split-env-lemma-2 sp ϱ
  ... | ϱ₁ , ϱ₂ , spe== , sp==
    rewrite spe== | sp==
    with ssplit-compose{just (send! , POSNEG) ∷ []} (ss-posneg ss-[]) (ss-left ss-[])
  ... | ssc
    rewrite split-env-right-lemma ϱ₁
    with ssplit-compose{just (send! , POSNEG) ∷ []} (ss-left ss-[]) (ss-left ss-[])
  ... | ssc-ll
    rewrite split-env-right-lemma ϱ₂
    with ssplit-compose2 (ss-both ss-[]) (ss-both ss-[])
  ... | ssc2
    rewrite weaken2-ident (lift-venv ϱ₁)
          | split-rotate-lemma {Φ₁}
          | split-rotate-lemma {Φ₂}
          | split-env-right-lemma0 ϱ₁
          | split-env-right-lemma0 ϱ₂
          | weaken2-ident ϱ₁
          | weaken1-ident (lift-venv ϱ₂)
          | weaken1-ident ϱ₂
    = refl

module ClosedWithContext where
  mklhs : Expr (TUnit ∷ []) TUnit
    → Expr (TUnit ∷ []) TUnit
    → Proc []
  mklhs e f =
    res (delay send!)
        (par (left (rght []))
             (exp (mkclose e)) (exp (mkwait f)))

  mkrhs : Expr (TUnit ∷ []) TUnit
    → Expr (TUnit ∷ []) TUnit
    → Proc []
  mkrhs e f =
    par [] (exp (letbind [] (unit []) e))
           (exp (letbind [] (unit []) f))

  reduction :
    (e f : Expr (TUnit ∷ []) TUnit) →
    let lhs = (runProc [] (mklhs e f) (vnil []-inactive)) in
    let rhs = (runProc [] (mkrhs e f) (vnil []-inactive)) in
    one-step lhs ≡
    (Closed , nothing ∷ proj₁ rhs , lift-threadpool (proj₂ rhs))
  reduction e f
    with ssplit-refl-left-inactive []
  ... | G' , ina-G' , ss-GG'
    = refl

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
module Prelude.Level where

open import Agda.Primitive public
  using    (Level)
  renaming (lzero to zero; lsuc to suc; _⊔_ to max)

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Everything

module Test.Symmetrical where

  test-𝓢ymmetrical𝓢ymmetry : ∀
    {𝔬} {𝔒 : Ø 𝔬}
    {ℓ} {_∼_ : 𝔒 → 𝔒 → Ø ℓ}
    ⦃ _ : Symmetry.class _∼_ ⦄
    → Symmetry.type _∼_
  -- test-𝓢ymmetrical𝓢ymmetry = symmetrical _ _ -- FIXME no longer works after 𝓢ymmetrical𝓢ymmetry was "rationalised"
  test-𝓢ymmetrical𝓢ymmetry {𝔒 = 𝔒} = symmetrical {𝔄 = 𝔒} _ _

  test-𝓢ymmetrical𝓢ymmetry-alternate : ∀
    {𝔬} {𝔒 : Ø 𝔬}
    {ℓ} {_∼_ : 𝔒 → 𝔒 → Ø ℓ}
    ⦃ _ : Symmetry.class _∼_ ⦄
    → Symmetry.type _∼_
  test-𝓢ymmetrical𝓢ymmetry-alternate {x = x} = symmetrical x _

  lhs-test1 : ∀ {𝔬} {𝔒 : Ø 𝔬}
    {ℓ} {_∼_ : 𝔒 → 𝔒 → Ø ℓ}
    ⦃ _ : Symmetry.class _∼_ ⦄
    {_∼'_ : 𝔒 → 𝔒 → Ø ℓ}
    ⦃ _ : Symmetry.class _∼'_ ⦄
    → ∀ x y → _
  lhs-test1 {_∼_ = _∼_} = symmetrical⟦ _∼_ / (λ x y → x → y) ⟧

  module OverlappingInstances
    {𝔞} {𝔄 : Ø 𝔞}
    {𝔟} {𝔅 : Ø 𝔟}
    {ℓ} {_↦_ : 𝔅 → 𝔅 → Ø ℓ}
        {_↦'_ : 𝔅 → 𝔅 → Ø ℓ}
    {_∼1_ : 𝔄 → 𝔄 → 𝔅}
    {_∼2_ : 𝔄 → 𝔄 → 𝔅}
    ⦃ _ : Symmetrical _∼1_ _↦_ ⦄
    ⦃ _ : Symmetrical _∼1_ _↦'_ ⦄
    ⦃ _ : Symmetrical _∼2_ _↦_ ⦄
    ⦃ _ : Symmetrical _∼2_ _↦'_ ⦄
    (x y : 𝔄)
    where

    test1 = symmetrical {_∼_ = _∼1_} {_↦_ = _↦_} x y

    test2 : (x ∼1 y) ↦ (y ∼1 x)
    test2 = symmetrical⟦ _ / _↦_ ⟧ x y

    test2a : (x ∼1 y) ↦ (y ∼1 x)
    test2a = symmetrical x y

    test3 = symmetrical⟦ _∼1_ / _↦_ ⟧ x y

  lhs-test2a : ∀
    {𝔞} {𝔄 : Ø 𝔞}
    {𝔟} {𝔅 : Ø 𝔟}
    (_∼_ : 𝔄 → 𝔄 → 𝔅)
    {ℓ} (_↦_ : 𝔅 → 𝔅 → Ø ℓ)
    ⦃ _ : Symmetrical _∼_ _↦_ ⦄
    → ∀ (x y : 𝔄) → _ ↦ _
  lhs-test2a _∼_ _↦_ x y =
    symmetrical x y -- works
    -- symmetrical⟦ _∼_ / _↦_ ⟧ x y -- works
    -- symmetrical⟦ _ / _↦_ ⟧ x y -- works
    -- symmetrical⟦ _∼_ / _ ⟧ x y -- works

  open import Oscar.Data.Proposequality
  lhs-test2a' : ∀
    {𝔞} {𝔄 : Ø 𝔞}
    {𝔟} {𝔅 : Ø 𝔟}
    (_∼_ : 𝔄 → 𝔄 → 𝔅) {_∼'_ : 𝔄 → 𝔄 → 𝔅}
    {ℓ} (_↦_ : 𝔅 → 𝔅 → Ø ℓ) {_↦'_ : 𝔅 → 𝔅 → Ø ℓ}
    ⦃ _ : Symmetrical _∼_ _↦_ ⦄
    ⦃ _ : Symmetrical _∼'_ _↦_ ⦄
    ⦃ _ : Symmetrical _∼_ _↦'_ ⦄
    ⦃ _ : Symmetrical _∼'_ _↦'_ ⦄
    → ∀ (x y : 𝔄) → -- _
                    _ ↦ _
                    -- (x ∼ y) ↦ (y ∼ x)
  lhs-test2a' _∼_ _↦_ x y =
    symmetrical⟦ _∼_ / _ ⟧ x y
    -- symmetrical x y -- fails, as expected
    -- symmetrical⟦ _ / _ ⟧ x y -- fails, as expected
    -- symmetrical⟦ _ / _↦_ ⟧ x y -- fails, as expected

  lhs-test2a'' : ∀
    {𝔞} {𝔄 : Ø 𝔞}
    {𝔟} {𝔅 : Ø 𝔟}
    (_∼_ : 𝔄 → 𝔄 → 𝔅) {_∼'_ : 𝔄 → 𝔄 → 𝔅}
    {ℓ} (_↦_ : 𝔅 → 𝔅 → Ø ℓ) {_↦'_ : 𝔅 → 𝔅 → Ø ℓ}
    ⦃ _ : Symmetrical _∼_ _↦_ ⦄
    ⦃ _ : Symmetrical _∼'_ _↦_ ⦄
    ⦃ _ : Symmetrical _∼_ _↦'_ ⦄
    ⦃ _ : Symmetrical _∼'_ _↦'_ ⦄
    → ∀ (x y : 𝔄) → -- _
                    -- _ ↦ _
                    (x ∼ y) ↦ (y ∼ x)
  lhs-test2a'' _∼_ _↦_ x y =
    symmetrical {_∼_ = _∼_} x y
    -- symmetrical'' {_↦_ = _↦_} x y
    -- symmetrical'' {_∼_ = _∼_} {_↦_ = _↦_} x y
    -- symmetrical'' x y