text:
{-# OPTIONS --show-implicit #-}
module Exegesis where

module Superclasses where

  open import Agda.Primitive
  open import Agda.Builtin.Equality

  record Semigroup (A : Set) : Set where
    field
      _∙_ : A → A → A
      assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
      cong : ∀ w x y z → w ≡ y → x ≡ z → w ∙ x ≡ y ∙ z

  open Semigroup ⦃ … ⦄

  record Identity {A : Set} (_∙_ : A → A → A) : Set where
    field
      ε : A
      left-identity  : ∀ x → ε ∙ x ≡ x
      right-identity : ∀ x → x ∙ ε ≡ x

  open Identity ⦃ … ⦄

  record Monoid (A : Set) : Set where
    field
      ⦃ semigroup ⦄ : Semigroup A
      ⦃ identity ⦄  : Identity (_∙_ ⦃ semigroup ⦄)

  open Monoid ⦃ … ⦄

  foo : {A : Set} ⦃ m : Monoid A ⦄ → (x : A) → x ∙ ε ⦃ identity ⦄ ≡ x
  foo x = right-identity x

module StandardLibraryMethod where

  open import Agda.Primitive
  open import Agda.Builtin.Equality

  record Semigroup (A : Set) : Set where
    field
      _∙_ : A → A → A
      assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
      cong : ∀ w x y z → w ≡ y → x ≡ z → w ∙ x ≡ y ∙ z

  --open Semigroup ⦃ … ⦄

  record Identity (A : Set) (ε : A) (_∙_ : A → A → A) : Set where
    field
      left-identity  : ∀ x → ε ∙ x ≡ x
      right-identity : ∀ x → x ∙ ε ≡ x

  --open Identity ⦃ … ⦄

  record Monoid (A : Set) : Set where
    field
      s : Semigroup A

    open Semigroup s public

    field
      ε : A
      i : Identity A ε _∙_

    open Identity i public

  open Monoid ⦃ … ⦄

  foo : {A : Set} ⦃ m : Monoid A ⦄ → (x : A) → x ∙ ε ≡ x
  foo x = right-identity x -- right-identity x

module Cascade where

  open import Agda.Primitive
  open import Agda.Builtin.Equality

  record Semigroup (A : Set) : Set where
    field
      _∙_ : A → A → A
      assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
      cong : ∀ w x y z → w ≡ y → x ≡ z → w ∙ x ≡ y ∙ z

  open Semigroup ⦃ … ⦄

  record RawMonoid (A : Set) ⦃ _ : Semigroup A ⦄ : Set where
    no-eta-equality
    field
      ε : A

  open RawMonoid ⦃ … ⦄

  record Identity (A : Set) (ε : A) (_∙_ : A → A → A) : Set where
    field
      left-identity  : ∀ x → ε ∙ x ≡ x
      right-identity : ∀ x → x ∙ ε ≡ x

  open Identity ⦃ … ⦄

  foo : {A : Set} ⦃ _ : Semigroup A ⦄ ⦃ _ : RawMonoid A ⦄ ⦃ i : Identity A ε _∙_ ⦄ → (x : A) → x ∙ ε ≡ x
  foo ⦃ s ⦄ ⦃ rm ⦄ ⦃ i ⦄ x = right-identity ⦃ i ⦄ x

module Buncha where

  open import Agda.Primitive
  open import Agda.Builtin.Equality

  record Semigroup (A : Set) : Set where
    field
      _∙_ : A → A → A
      assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
      cong : ∀ w x y z → w ≡ y → x ≡ z → w ∙ x ≡ y ∙ z

  open Semigroup ⦃ … ⦄

  record RawMonoid (A : Set) : Set where
    field
      ε : A

  open RawMonoid ⦃ … ⦄

  record Identity {A : Set} (_∙_ : A → A → A) ⦃ _ : RawMonoid A ⦄ : Set where
    field
      left-identity  : ∀ x → ε ∙ x ≡ x
      right-identity : ∀ x → x ∙ ε ≡ x

  open Identity ⦃ … ⦄

  record Monoid (A : Set) : Set where
    field
      ⦃ semigroup ⦄ : Semigroup A
      ⦃ rawmonoid ⦄ : RawMonoid A
      ⦃ identity ⦄ : Identity {A} _∙_

  open Monoid ⦃ … ⦄

  foo : {A : Set} ⦃ _ : Semigroup A ⦄ ⦃ _ : RawMonoid A ⦄ ⦃ _ : Identity _∙_ ⦄ → (x : A) → x ∙ ε ≡ x
  foo x = right-identity x

  bar : {A : Set} ⦃ _ : Monoid A ⦄ → (x : A) → x ∙ ε ≡ x
  bar x = right-identity x

module SomethingThatWorks where

  open import Agda.Primitive
  open import Agda.Builtin.Equality

  record Equivalence (A : Set) : Set₁ where
    infix 4 _≈_
    field
      _≈_ : A → A → Set
      reflexive : ∀ x → x ≈ x
      symmetric : ∀ {x y} → x ≈ y → y ≈ x
      transitive : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z

  open Equivalence ⦃ … ⦄

  record Operator (A : Set) : Set where
    field
      _∙_ : A → A → A

  record Semigroup (A : Set) : Set₁ where
    field
      ⦃ operator ⦄ : Operator A
      ⦃ equivalence ⦄ : Equivalence A

    open Operator operator public
    field
      assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
      cong : ∀ w x y z → w ≡ y → x ≡ z → w ∙ x ≡ y ∙ z

  open Semigroup ⦃ … ⦄

  record IdentityElement (A : Set) : Set where
    field
      ε : A

  module ε where

    open IdentityElement ⦃ … ⦄ public

  record Identity {A : Set} (_∙_ : A → A → A) ⦃ _ : IdentityElement A ⦄ : Set where
    open ε
    field
      left-identity  : ∀ x → ε ∙ x ≡ x
      right-identity : ∀ x → x ∙ ε ≡ x

  open Identity ⦃ … ⦄

  record Monoid (A : Set) : Set₁ where
    field
      ⦃ semigroup ⦄ : Semigroup A
      ⦃ identityElement ⦄ : IdentityElement A
      ⦃ identity ⦄ : Identity {A} _∙_

  open Monoid ⦃ … ⦄

  bar : {A : Set} ⦃ _ : Monoid A ⦄ {B : Set} ⦃ _ : Monoid B ⦄ (open ε) → (x : A) → x ∙ ε ≡ x
  bar x = right-identity x

module SeparatingIsFromOught where

  open import Agda.Primitive
  open import Agda.Builtin.Equality

  record Equivalence (A : Set) : Set₁ where
    infix 4 _≈_
    field
      _≈_ : A → A → Set
      reflexive : ∀ x → x ≈ x
      symmetric : ∀ {x y} → x ≈ y → y ≈ x
      transitive : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z

  open Equivalence ⦃ … ⦄

  record Operator (A : Set) : Set where
    field
      _∙_ : A → A → A

  open Operator ⦃ … ⦄

  record IsSemigroup (A : Set) ⦃ _ : Operator A ⦄ ⦃ _ : Equivalence A ⦄ : Set where
    field
      assoc : ∀ (x : A) y z → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z)
      cong : ∀ (w : A) x y z → w ≈ y → x ≈ z → w ∙ x ≈ y ∙ z

  open IsSemigroup ⦃ … ⦄

  record Semigroup (A : Set) : Set₁ where
    field
      ⦃ operator ⦄ : Operator A
      ⦃ equivalence ⦄ : Equivalence A
      ⦃ isSemigroup ⦄ : IsSemigroup A

  open Semigroup ⦃ … ⦄
{-
  record IdentityElement (A : Set) : Set where
    field
      ε : A

  open IdentityElement ⦃ … ⦄
-}
  record IsIdentity (A : Set) ⦃ _ : Operator A ⦄ {-⦃ _ : IdentityElement A ⦄-} ⦃ _ : Equivalence A ⦄ : Set where

--  record IsIdentity {A : Set} (_∙_ : A → A → A) (ε : A) ⦃ _ : Equivalence A ⦄ : Set where
    field
      ε : A
      left-identity  : ∀ (x : A) → ε ∙ x ≈ x
      right-identity : ∀ (x : A) → x ∙ ε ≈ x

  open IsIdentity ⦃ … ⦄

  record Monoid (A : Set) : Set₁ where
    field
      ⦃ semigroup ⦄ : Semigroup A
      --⦃ identityElement ⦄ : IdentityElement A
      --ε : A
      --⦃ identity ⦄ : IsIdentity (_∙_ {A}) ε
--      ⦃ operator ⦄ : Operator A
      ⦃ identity ⦄ : IsIdentity A

  open Monoid ⦃ … ⦄

  bar : {A : Set} ⦃ m : Monoid A ⦄ {B : Set} ⦃ _ : Semigroup B ⦄ → (x : A) → x ∙ ε ≈ x
  bar x = right-identity x

  bar2 : {A : Set} ⦃ _ : Monoid A ⦄ → (x y : A) → (x ∙ ε) ∙ y ≈ x ∙ (ε ∙ y)
  bar2 x y = assoc x ε y

module FineControl where

  record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set₁ where
    field
      reflexive : ∀ x → x ≈ x
      symmetric : ∀ {x y} → x ≈ y → y ≈ x
      transitive : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z

  open IsEquivalence ⦃ … ⦄

  record Equivalence (A : Set) : Set₁ where
    infix 4 _≈_
    field
      _≈_ : A → A → Set
      ⦃ isEquivalence ⦄ : IsEquivalence _≈_

  open Equivalence ⦃ … ⦄

  record IsSemigroup {A : Set} (_∙_ : A → A → A) ⦃ _ : Equivalence A ⦄ : Set where
    field
      assoc : ∀ (x : A) y z → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z)
      cong : ∀ (w : A) x y z → w ≈ y → x ≈ z → w ∙ x ≈ y ∙ z

  open IsSemigroup ⦃ … ⦄

  record Semigroup (A : Set) : Set₁ where
    field
      ⦃ equivalence ⦄ : Equivalence A
      _∙_ : A → A → A
      ⦃ isSemigroup ⦄ : IsSemigroup _∙_

  open Semigroup ⦃ … ⦄

  record Identity (A : Set) : Set where
    field
      ε : A

  open Identity ⦃ … ⦄

--  record IsLeftIdentity {A B : Set} (_∙_ : A → B → B) ⦃ _ : Identity A ⦄ (ε : A) ⦃ _ : Equivalence B ⦄ : Set where
  record IsLeftIdentity {A B : Set} (_∙_ : A → B → B) ⦃ _ : Identity A ⦄ ⦃ _ : Equivalence B ⦄ : Set where
    field
      left-identity  : ∀ x → ε ∙ x ≈ x

  open IsLeftIdentity ⦃ … ⦄

--  record IsRightIdentity {A B : Set} (_∙_ : B → A → B) (ε : A) ⦃ _ : Equivalence B ⦄ : Set where
  record IsRightIdentity {A B : Set} (_∙_ : B → A → B) ⦃ _ : Identity A ⦄ ⦃ _ : Equivalence B ⦄ : Set where
    field
      right-identity : ∀ x → x ∙ ε ≈ x

  open IsRightIdentity ⦃ … ⦄

  record Monoid (A : Set) : Set₁ where
    field
      ⦃ semigroup ⦄ : Semigroup A
      --ε : A
      ⦃ identity ⦄ : Identity A
      ⦃ lidentity ⦄ : IsLeftIdentity {A = A} _∙_
      ⦃ ridentity ⦄ : IsRightIdentity {A = A} _∙_

  open Monoid ⦃ … ⦄

  bar : {A : Set} ⦃ m : Monoid A ⦄ → (x : A) → x ∙ ε ≈ x
  bar {A} x = right-identity {_∙_ = _∙_} x -- right-identity {_∙_ = _∙_} x

  bar' : {A : Set} ⦃ m : Monoid A ⦄ → (x : A) → x ∙ ε ≈ x
  bar' x = right-identity x

  bar2 : {A : Set} ⦃ _ : Monoid A ⦄ → (x y z : A) → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z)
  bar2 x y z = assoc x y z

module FineControl2 where

  record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set₁ where
    field
      reflexive : ∀ x → x ≈ x
      symmetric : ∀ {x y} → x ≈ y → y ≈ x
      transitive : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z

  open IsEquivalence ⦃ … ⦄

  record Equivalence (A : Set) : Set₁ where
    infix 4 _≈_
    field
      _≈_ : A → A → Set
      ⦃ isEquivalence ⦄ : IsEquivalence _≈_

  open Equivalence ⦃ … ⦄

  record IsSemigroup {A : Set} (_∙_ : A → A → A) ⦃ _ : Equivalence A ⦄ : Set where
    field
      assoc : ∀ (x : A) y z → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z)
      cong : ∀ (w : A) x y z → w ≈ y → x ≈ z → w ∙ x ≈ y ∙ z

  open IsSemigroup ⦃ … ⦄

  record Semigroup (A : Set) : Set₁ where
    field
      overlap ⦃ equivalence ⦄ : Equivalence A
      _∙_ : A → A → A
      ⦃ isSemigroup ⦄ : IsSemigroup _∙_

  open Semigroup ⦃ … ⦄

  record Identity (A : Set) : Set where
    field
      ε : A

  open Identity ⦃ … ⦄

--  record IsLeftIdentity {A B : Set} (_∙_ : A → B → B) (ε : A) ⦃ _ : Equivalence B ⦄ : Set where
--  record IsLeftIdentity {A B : Set} (_∙_ : A → B → B) : Set₁ where
  record IsLeftIdentity {A B : Set} (_∙_ : A → B → B) ⦃ _ : Identity A ⦄ ⦃ _ : Equivalence B ⦄ : Set₁ where
    field
      left-identity  : ∀ x → ε ∙ x ≈ x

  open IsLeftIdentity ⦃ … ⦄

--  record IsRightIdentity {A B : Set} (_∙_ : B → A → B) (ε : A) ⦃ _ : Equivalence B ⦄ : Set where
--  record IsRightIdentity {A B : Set} (_∙_ : B → A → B) : Set₁ where
  record IsRightIdentity {A B : Set} (_∙_ : B → A → B) ⦃ _ : Identity A ⦄ ⦃ _ : Equivalence B ⦄ : Set₁ where
    field
      right-identity : ∀ x → x ∙ ε ≈ x

--  open IsRightIdentity ⦃ … ⦄

  record Monoid (A : Set) : Set₁ where
    field
      ⦃ semigroup ⦄ : Semigroup A
      --ε : A
      ⦃ identity ⦄ : Identity A
      ⦃ lidentity ⦄ : IsLeftIdentity {A = A} _∙_
      ⦃ ridentity ⦄ : IsRightIdentity {A = A} _∙_

    open IsRightIdentity ridentity public

  open Monoid ⦃ … ⦄

  bar : {A : Set} ⦃ m : Monoid A ⦄ → (x : A) → x ∙ ε ≈ x
  bar {A} x = right-identity x -- right-identity {_∙_ = _∙_} x

  bar' : {A : Set} ⦃ m : Monoid A ⦄ → (x : A) → x ∙ ε ≈ x
  bar' x = right-identity x

  bar2 : {A : Set} ⦃ _ : Monoid A ⦄ → (x y z : A) → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z)
  bar2 x y z = assoc x y z


text:
----------------------------------------------------------------------------------
-- Types for parse trees
----------------------------------------------------------------------------------

module cedille-types where

open import lib
-- open import parse-tree

posinfo = string
alpha = string
alpha-bar-3 = string
alpha-range-1 = string
alpha-range-2 = string
bvar = string
bvar-bar-13 = string
fpth = string
fpth-bar-15 = string
fpth-bar-16 = string
fpth-bar-17 = string
fpth-plus-14 = string
fpth-star-18 = string
kvar = string
kvar-bar-19 = string
kvar-star-20 = string
num = string
num-plus-5 = string
numone = string
numone-range-4 = string
numpunct = string
numpunct-bar-10 = string
numpunct-bar-6 = string
numpunct-bar-7 = string
numpunct-bar-8 = string
numpunct-bar-9 = string
qkvar = string
qvar = string
var = string
var-bar-11 = string
var-star-12 = string

{-# FOREIGN GHC import qualified CedilleTypes #-}

data arg : Set
{-# COMPILE GHC arg = type CedilleTypes.Arg #-}
data args : Set
{-# COMPILE GHC args = type CedilleTypes.Args #-}
data opacity : Set
{-# COMPILE GHC opacity = type CedilleTypes.Opacity #-}
data cmd : Set
{-# COMPILE GHC cmd = type CedilleTypes.Cmd #-}
data cmds : Set
{-# COMPILE GHC cmds = type CedilleTypes.Cmds #-}
data decl : Set
{-# COMPILE GHC decl = type CedilleTypes.Decl #-}
data defDatatype : Set
{-# COMPILE GHC defDatatype = type CedilleTypes.DefDatatype #-}
data dataConst : Set
{-# COMPILE GHC dataConst = type CedilleTypes.DataConst #-}
data dataConsts : Set
{-# COMPILE GHC dataConsts = type CedilleTypes.DataConsts #-}
data defTermOrType : Set
{-# COMPILE GHC defTermOrType = type CedilleTypes.DefTermOrType #-}
data imports : Set
{-# COMPILE GHC imports = type CedilleTypes.Imports #-}
data imprt : Set
{-# COMPILE GHC imprt = type CedilleTypes.Imprt #-}
data kind : Set
{-# COMPILE GHC kind = type CedilleTypes.Kind #-}
data leftRight : Set
{-# COMPILE GHC leftRight = type CedilleTypes.LeftRight #-}
data liftingType : Set
{-# COMPILE GHC liftingType = type CedilleTypes.LiftingType #-}
data lterms : Set
{-# COMPILE GHC lterms = type CedilleTypes.Lterms #-}
data optType : Set
{-# COMPILE GHC optType = type CedilleTypes.OptType #-}
data maybeErased : Set
{-# COMPILE GHC maybeErased = type CedilleTypes.MaybeErased #-}
data maybeMinus : Set
{-# COMPILE GHC maybeMinus = type CedilleTypes.MaybeMinus #-}
data nums : Set
{-# COMPILE GHC nums = type CedilleTypes.Nums #-}
data optAs : Set
{-# COMPILE GHC optAs = type CedilleTypes.OptAs #-}
data optClass : Set
{-# COMPILE GHC optClass = type CedilleTypes.OptClass #-}
data optGuide : Set
{-# COMPILE GHC optGuide = type CedilleTypes.OptGuide #-}
data optPlus : Set
{-# COMPILE GHC optPlus = type CedilleTypes.OptPlus #-}
data optNums : Set
{-# COMPILE GHC optNums = type CedilleTypes.OptNums #-}
data optPublic : Set
{-# COMPILE GHC optPublic = type CedilleTypes.OptPublic #-}
data optTerm : Set
{-# COMPILE GHC optTerm = type CedilleTypes.OptTerm #-}
data params : Set
{-# COMPILE GHC params = type CedilleTypes.Params #-}
data start : Set
{-# COMPILE GHC start = type CedilleTypes.Start #-}
data term : Set
{-# COMPILE GHC term = type CedilleTypes.Term  #-}
data theta : Set
{-# COMPILE GHC theta = type CedilleTypes.Theta  #-}
data tk : Set
{-# COMPILE GHC tk = type CedilleTypes.Tk  #-}
data type : Set
{-# COMPILE GHC type = type CedilleTypes.Type  #-}
data vars : Set
{-# COMPILE GHC vars = type CedilleTypes.Vars  #-}
data cases : Set
{-# COMPILE GHC cases = type CedilleTypes.Cases  #-}
data varargs : Set
{-# COMPILE GHC varargs = type CedilleTypes.Varargs  #-}

data arg where
  TermArg : maybeErased → term → arg
  TypeArg : type → arg
{-# COMPILE GHC arg = data CedilleTypes.Arg (CedilleTypes.TermArg | CedilleTypes.TypeArg) #-}

data args where
  ArgsCons : arg → args → args
  ArgsNil : args
{-# COMPILE GHC args = data CedilleTypes.Args (CedilleTypes.ArgsCons | CedilleTypes.ArgsNil) #-}

data opacity where
  OpacOpaque : opacity
  OpacTrans : opacity
{-# COMPILE GHC opacity = data CedilleTypes.Opacity (CedilleTypes.OpacOpaque | CedilleTypes.OpacTrans) #-}

data cmd where
  DefKind : posinfo → kvar → params → kind → posinfo → cmd
  DefTermOrType : opacity → defTermOrType → posinfo → cmd
  DefDatatype   : defDatatype   → posinfo → cmd
  ImportCmd : imprt → cmd
{-# COMPILE GHC cmd = data CedilleTypes.Cmd (CedilleTypes.DefKind | CedilleTypes.DefTermOrType | CedilleTypes.DefDatatype |CedilleTypes.ImportCmd) #-}

data cmds where
  CmdsNext : cmd → cmds → cmds
  CmdsStart : cmds
{-# COMPILE GHC cmds = data CedilleTypes.Cmds (CedilleTypes.CmdsNext | CedilleTypes.CmdsStart) #-}

data decl where
  Decl : posinfo → posinfo → maybeErased → bvar → tk → posinfo → decl
{-# COMPILE GHC decl = data CedilleTypes.Decl (CedilleTypes.Decl) #-}

data defDatatype where
  Datatype : posinfo → posinfo → var → params → kind → dataConsts → posinfo → defDatatype
{-# COMPILE GHC defDatatype = data CedilleTypes.DefDatatype (CedilleTypes.Datatype) #-}

data dataConst where
  DataConst : posinfo → var → type → dataConst
{-# COMPILE GHC dataConst = data CedilleTypes.DataConst (CedilleTypes.DataConst) #-}

data dataConsts where
  DataNull : dataConsts
  DataCons : dataConst → dataConsts → dataConsts
{-# COMPILE GHC dataConsts = data CedilleTypes.DataConsts (CedilleTypes.DataNull | CedilleTypes.DataCons) #-}

data defTermOrType where
  DefTerm : posinfo → var → optType → term → defTermOrType
  DefType : posinfo → var → kind → type → defTermOrType
{-# COMPILE GHC defTermOrType = data CedilleTypes.DefTermOrType (CedilleTypes.DefTerm | CedilleTypes.DefType) #-}

data imports where
  ImportsNext : imprt → imports → imports
  ImportsStart : imports
{-# COMPILE GHC imports = data CedilleTypes.Imports (CedilleTypes.ImportsNext | CedilleTypes.ImportsStart) #-}

data imprt where
  Import : posinfo → optPublic → posinfo → fpth → optAs → args → posinfo → imprt
{-# COMPILE GHC imprt = data CedilleTypes.Imprt (CedilleTypes.Import) #-}

data kind where
  KndArrow : kind → kind → kind
  KndParens : posinfo → kind → posinfo → kind
  KndPi : posinfo → posinfo → bvar → tk → kind → kind
  KndTpArrow : type → kind → kind
  KndVar : posinfo → qkvar → args → kind
  Star : posinfo → kind
{-# COMPILE GHC kind = data CedilleTypes.Kind (CedilleTypes.KndArrow | CedilleTypes.KndParens | CedilleTypes.KndPi | CedilleTypes.KndTpArrow | CedilleTypes.KndVar | CedilleTypes.Star) #-}

data leftRight where
  Both : leftRight
  Left : leftRight
  Right : leftRight
{-# COMPILE GHC leftRight = data CedilleTypes.LeftRight (CedilleTypes.Both | CedilleTypes.Left | CedilleTypes.Right) #-}

data liftingType where
  LiftArrow : liftingType → liftingType → liftingType
  LiftParens : posinfo → liftingType → posinfo → liftingType
  LiftPi : posinfo → bvar → type → liftingType → liftingType
  LiftStar : posinfo → liftingType
  LiftTpArrow : type → liftingType → liftingType
{-# COMPILE GHC liftingType = data CedilleTypes.LiftingType (CedilleTypes.LiftArrow | CedilleTypes.LiftParens | CedilleTypes.LiftPi | CedilleTypes.LiftStar | CedilleTypes.LiftTpArrow) #-}

data lterms where
  LtermsCons : maybeErased → term → lterms → lterms
  LtermsNil : posinfo → lterms
{-# COMPILE GHC lterms = data CedilleTypes.Lterms (CedilleTypes.LtermsCons | CedilleTypes.LtermsNil) #-}

data optType where
  SomeType : type → optType
  NoType : optType
{-# COMPILE GHC optType = data CedilleTypes.OptType (CedilleTypes.SomeType | CedilleTypes.NoType) #-}

data maybeErased where
  Erased : maybeErased
  NotErased : maybeErased
{-# COMPILE GHC maybeErased = data CedilleTypes.MaybeErased (CedilleTypes.Erased | CedilleTypes.NotErased) #-}

data maybeMinus where
  EpsHanf : maybeMinus
  EpsHnf : maybeMinus
{-# COMPILE GHC maybeMinus = data CedilleTypes.MaybeMinus (CedilleTypes.EpsHanf | CedilleTypes.EpsHnf) #-}

data nums where
  NumsStart : num → nums
  NumsNext : num → nums → nums
{-# COMPILE GHC nums = data CedilleTypes.Nums (CedilleTypes.NumsStart | CedilleTypes.NumsNext) #-}

data optAs where
  NoOptAs : optAs
  SomeOptAs : posinfo → var → optAs
{-# COMPILE GHC optAs = data CedilleTypes.OptAs (CedilleTypes.NoOptAs | CedilleTypes.SomeOptAs) #-}

data optPublic where
  NotPublic : optPublic
  IsPublic : optPublic
{-# COMPILE GHC optPublic = data CedilleTypes.OptPublic (CedilleTypes.NotPublic | CedilleTypes.IsPublic) #-}

data optClass where
  NoClass : optClass
  SomeClass : tk → optClass
{-# COMPILE GHC optClass = data CedilleTypes.OptClass (CedilleTypes.NoClass | CedilleTypes.SomeClass) #-}

data optGuide where
  NoGuide : optGuide
  Guide : posinfo → var → type → optGuide
{-# COMPILE GHC optGuide = data CedilleTypes.OptGuide (CedilleTypes.NoGuide | CedilleTypes.Guide) #-}

data optPlus where
  RhoPlain : optPlus
  RhoPlus : optPlus
{-# COMPILE GHC optPlus = data CedilleTypes.OptPlus (CedilleTypes.RhoPlain | CedilleTypes.RhoPlus) #-}

data optNums where
  NoNums : optNums
  SomeNums : nums → optNums
{-# COMPILE GHC optNums = data CedilleTypes.OptNums (CedilleTypes.NoNums | CedilleTypes.SomeNums) #-}

data optTerm where
  NoTerm : optTerm
  SomeTerm : term → posinfo → optTerm
{-# COMPILE GHC optTerm = data CedilleTypes.OptTerm (CedilleTypes.NoTerm | CedilleTypes.SomeTerm) #-}

data params where
  ParamsCons : decl → params → params
  ParamsNil : params
{-# COMPILE GHC params = data CedilleTypes.Params (CedilleTypes.ParamsCons | CedilleTypes.ParamsNil) #-}

data start where
  File : posinfo → imports → posinfo → posinfo → qvar → params → cmds → posinfo → start
{-# COMPILE GHC start = data CedilleTypes.Start (CedilleTypes.File) #-}

data term where
  App : term → maybeErased → term → term
  AppTp : term → type → term
  Beta : posinfo → optTerm → optTerm → term
  Chi : posinfo → optType → term → term
  Delta : posinfo → optType → term → term
  Epsilon : posinfo → leftRight → maybeMinus → term → term
  Hole : posinfo → term
  IotaPair : posinfo → term → term → optGuide → posinfo → term
  IotaProj : term → num → posinfo → term
  Lam : posinfo → maybeErased → posinfo → bvar → optClass → term → term
  Let : posinfo → defTermOrType → term → term
  Open : posinfo → var → term → term
  Parens : posinfo → term → posinfo → term
  Phi : posinfo → term → term → term → posinfo → term
  Rho : posinfo → optPlus → optNums → term → optGuide → term → term
  Sigma : posinfo → term → term
  Theta : posinfo → theta → term → lterms → term
  Mu  : posinfo → bvar → term → optType → posinfo → cases → posinfo → term
  Mu' : posinfo → term → optType → posinfo → cases → posinfo → term
  Var : posinfo → qvar → term
{-# COMPILE GHC term = data CedilleTypes.Term (CedilleTypes.App | CedilleTypes.AppTp | CedilleTypes.Beta | CedilleTypes.Chi | CedilleTypes.Delta | CedilleTypes.Epsilon | CedilleTypes.Hole | CedilleTypes.IotaPair | CedilleTypes.IotaProj | CedilleTypes.Lam | CedilleTypes.Let | CedilleTypes.Open | CedilleTypes.Parens | CedilleTypes.Phi | CedilleTypes.Rho | CedilleTypes.Sigma | CedilleTypes.Theta | CedilleTypes.Mu | CedilleTypes.Mu' | CedilleTypes.Var) #-}

data cases where
  NoCase : cases
  SomeCase : posinfo → var → varargs → term → cases → cases
{-# COMPILE GHC cases = data CedilleTypes.Cases (CedilleTypes.NoCase | CedilleTypes.SomeCase) #-}

data varargs where
  NoVarargs : varargs
  NormalVararg : bvar → varargs → varargs
  ErasedVararg : bvar → varargs → varargs
  TypeVararg   : bvar → varargs → varargs
{-# COMPILE GHC varargs = data CedilleTypes.Varargs (CedilleTypes.NoVarargs | CedilleTypes.NormalVararg | CedilleTypes.ErasedVararg | CedilleTypes.TypeVararg ) #-}

data theta where
  Abstract : theta
  AbstractEq : theta
  AbstractVars : vars → theta
{-# COMPILE GHC theta = data CedilleTypes.Theta (CedilleTypes.Abstract | CedilleTypes.AbstractEq | CedilleTypes.AbstractVars) #-}

data tk where
  Tkk : kind → tk
  Tkt : type → tk
{-# COMPILE GHC tk = data CedilleTypes.Tk (CedilleTypes.Tkk | CedilleTypes.Tkt) #-}

data type where
  Abs : posinfo → maybeErased → posinfo → bvar → tk → type → type
  Iota : posinfo → posinfo → bvar → type → type → type
  Lft : posinfo → posinfo → var → term → liftingType → type
  NoSpans : type → posinfo → type
  TpLet : posinfo → defTermOrType → type → type
  TpApp : type → type → type
  TpAppt : type → term → type
  TpArrow : type → maybeErased → type → type
  TpEq : posinfo → term → term → posinfo → type
  TpHole : posinfo → type
  TpLambda : posinfo → posinfo → bvar → tk → type → type
  TpParens : posinfo → type → posinfo → type
  TpVar : posinfo → qvar → type
{-# COMPILE GHC type = data CedilleTypes.Type (CedilleTypes.Abs | CedilleTypes.Iota | CedilleTypes.Lft | CedilleTypes.NoSpans | CedilleTypes.TpLet | CedilleTypes.TpApp | CedilleTypes.TpAppt | CedilleTypes.TpArrow | CedilleTypes.TpEq | CedilleTypes.TpHole | CedilleTypes.TpLambda | CedilleTypes.TpParens | CedilleTypes.TpVar) #-}

data vars where
  VarsNext : var → vars → vars
  VarsStart : var → vars
{-# COMPILE GHC vars = data CedilleTypes.Vars (CedilleTypes.VarsNext | CedilleTypes.VarsStart) #-}

pattern Pi = NotErased
pattern All = Erased

-- embedded types:
aterm = term
atype = type
lliftingType = liftingType
lterm = term
ltype = type
pterm = term

ext: agda

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
{-# OPTIONS --warning=error #-}

-- Useless abstract

module Issue476b where

abstract
  data A : Set

data A where

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module RecordInParModule (a : Set) where

record Setoid : Set1 where
  field el : Set

postulate
  S : Setoid
  A : Setoid.el S

postulate X : Set

module M (x : X) where
  record R : Set where

module E {x : X} (r : M.R x) where
  open module M' = M.R x r

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Check that FOREIGN code can have nested pragmas.
module _ where

open import Common.Prelude

{-# FOREIGN GHC

{-# NOINLINE plusOne #-}
plusOne :: Integer -> Integer
plusOne n = n + 1

{-# INLINE plusTwo #-}
plusTwo :: Integer -> Integer
plusTwo = plusOne . plusOne

#-}

postulate
  plusOne : Nat → Nat

{-# COMPILE GHC plusOne = plusOne #-}


text:
module _ where

module M (A : _) where

  y = Set -- type of A is solved if this is removed

  x : Set
  x = A

-- WAS: yellow on type of A
-- SHOULD: succeed


text:
open import Prelude
open import Nat
open import dynamics-core
open import contexts
open import lemmas-disjointness

module contraction where
  -- in the same style as the proofs of exchange, this argument along with
  -- trasnport allows you to prove contraction for all the hypothetical
  -- judgements uniformly. we never explicitly use contraction anywhere, so
  -- we omit any of the specific instances for concision; they are entirely
  -- mechanical, as are the specific instances of exchange. one is shown
  -- below as an example.
  contract : {A : Set} {x : Nat} {τ : A} (Γ : A ctx) →
         ((Γ ,, (x , τ)) ,, (x , τ)) == (Γ ,, (x , τ))
  contract {A} {x} {τ} Γ = funext guts
    where
      guts : (y : Nat) → (Γ ,, (x , τ) ,, (x , τ)) y == (Γ ,, (x , τ)) y
      guts y with natEQ x y
      guts .x | Inl refl with Γ x
      guts .x | Inl refl | Some x₁ = refl
      guts .x | Inl refl | None with natEQ x x
      guts .x | Inl refl | None | Inl refl = refl
      guts .x | Inl refl | None | Inr x≠x = abort (x≠x refl)
      guts y | Inr x≠y with natEQ x y
      guts y | Inr x≠y | Inl refl = abort (x≠y refl)
      guts y | Inr x≠y | Inr x≠y' = refl

  contract-synth : ∀{Γ x τ e τ'} →
                   (Γ ,, (x , τ) ,, (x , τ)) ⊢ e => τ' →
                   (Γ ,, (x , τ)) ⊢ e => τ'
  contract-synth {Γ = Γ} {x = x} {τ = τ} {e = e} {τ' = τ'} =
    tr (λ qq → qq ⊢ e => τ') (contract {x = x} {τ = τ} Γ)

  -- as an aside, this also establishes the other direction which is rarely
  -- mentioned, since equality is symmetric
  elab-synth : ∀{Γ x τ e τ'} →
               (Γ ,, (x , τ)) ⊢ e => τ' →
               (Γ ,, (x , τ) ,, (x , τ)) ⊢ e => τ'
  elab-synth {Γ = Γ} {x = x} {τ = τ} {e = e} {τ' = τ'} =
    tr (λ qq → qq ⊢ e => τ') (! (contract {x = x} {τ = τ} Γ))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Numeral.Integer where

import      Lvl
open import Numeral.Natural      as ℕ using (ℕ)
import      Numeral.Natural.Oper as ℕ
open import Syntax.Number
open import Type

-- Integers
data ℤ : Type{Lvl.𝟎} where
  +ₙ_  : ℕ → ℤ -- Positive integers including zero from the naturals (0,1,..).
  −𝐒ₙ_ : ℕ → ℤ -- Negative integers from the naturals (..,−2,−1).

{-# BUILTIN INTEGER        ℤ  #-}
{-# BUILTIN INTEGERPOS     +ₙ_ #-}
{-# BUILTIN INTEGERNEGSUC −𝐒ₙ_ #-}

------------------------------------------
-- Constructors and deconstructors

-- Constructing negative number from ℕ
−ₙ_ : ℕ → ℤ
−ₙ (ℕ.𝟎)    = +ₙ ℕ.𝟎
−ₙ (ℕ.𝐒(x)) = −𝐒ₙ(x)

-- Intuitive constructor patterns
pattern 𝟎      = +ₙ(ℕ.𝟎)    -- Zero (0).
pattern +𝐒ₙ_ n = +ₙ(ℕ.𝐒(n)) -- Positive integers from the naturals (1,2,..).
pattern 𝟏      = +ₙ(ℕ.𝟏)    -- One (1).
pattern −𝟏     = −𝐒ₙ(ℕ.𝟎)   -- Negative one (−1).
{-# DISPLAY ℤ.+ₙ_ ℕ.𝟎  = 𝟎 #-}
{-# DISPLAY ℤ.+ₙ_ ℕ.𝟏  = 𝟏 #-}
{-# DISPLAY ℤ.−𝐒ₙ_ ℕ.𝟎 = −𝟏 #-}
{-# DISPLAY ℤ.+ₙ_(ℕ.𝐒(n)) = +𝐒ₙ_ n #-}

-- Absolute value
absₙ : ℤ → ℕ
absₙ(+ₙ x)   = x
absₙ(−𝐒ₙ(x)) = ℕ.𝐒(x)

-- Syntax
instance
  ℤ-InfiniteNegativeNumeral : InfiniteNegativeNumeral(ℤ)
  ℤ-InfiniteNegativeNumeral = InfiniteNegativeNumeral.intro(−ₙ_)

instance
  ℤ-InfiniteNumeral : InfiniteNumeral(ℤ)
  ℤ-InfiniteNumeral = InfiniteNumeral.intro(+ₙ_)

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:
-- Andreas, 2017-08-18, issue #2703, reported by davdar, testcase by gallais
-- Underapplied constructor triggers internal error

{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS -v tc.getConType:35 #-}

postulate
  A : Set

data Sg : A → Set where
  sg : ∀ t → Sg t  -- Target type depends on constructor argument

postulate
  cut : (∀ t → Sg t) → Set

bug : cut sg  -- Underapplied constructor
bug with A
bug | _ = _

-- Was: internal error in 2.5.3 RC1

-- Should succeed with unsolved meta.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue157b where

postulate
  A B : Set
  R   : A → B → Set
  err : ∀ {a b} → R a b → R b

max_stars_repo_name: masondesu/agda


text:
module Cats.Category.Cat where

open import Cats.Functor public using (Functor ; _∘_ ; id)

open import Data.Product using (_,_)
open import Data.Unit using (⊤ ; tt)
open import Level
open import Relation.Binary using
  (IsEquivalence ; _Preserves_⟶_ ; _Preserves₂_⟶_⟶_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Cats.Category
open import Cats.Category.Zero
open import Cats.Category.One
open import Cats.Trans.Iso as NatIso using (NatIso ; iso ; forth-natural)
open import Cats.Util.Simp using (simp!)

open Functor
open Category._≅_

_⇒_ : ∀ {lo la l≈ lo′ la′ l≈′}
  → Category lo la l≈ → Category lo′ la′ l≈′ → Set _
C ⇒ D = Functor C D

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  where

  infixr 4 _≈_

  _≈_ : (F G : C ⇒ D) → Set (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′)
  F ≈ G = NatIso F G

  equiv : IsEquivalence _≈_
  equiv = record
      { refl = NatIso.id
      ; sym = NatIso.sym
      ; trans = λ eq₁ eq₂ → eq₂ NatIso.∘ eq₁
      }

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  where

  ∘-resp : ∀ {lo″ la″ l≈″} {E : Category lo″ la″ l≈″}
    → {F G : D ⇒ E} {H I : C ⇒ D}
    → F ≈ G
    → H ≈ I
    → F ∘ H ≈ G ∘ I
  ∘-resp {E = E} {F} {G} {H} {I}
    record { iso = F≅G ; forth-natural = fnat-GH }
    record { iso = H≅I ; forth-natural = fnat-HI }
      = record
      { iso = E.≅.trans F≅G (fobj-resp G H≅I)
      ; forth-natural = λ {_} {_} {f} →
          begin
            (fmap G (forth H≅I) E.∘ forth F≅G) E.∘ fmap F (fmap H f)
          ≈⟨ simp! E ⟩
            fmap G (forth H≅I) E.∘ forth F≅G E.∘ fmap F (fmap H f)
          ≈⟨ E.∘-resp-r fnat-GH ⟩
            fmap G (forth H≅I) E.∘ fmap G (fmap H f) E.∘ forth F≅G
          ≈⟨ simp! E ⟩
            (fmap G (forth H≅I) E.∘ fmap G (fmap H f)) E.∘ forth F≅G
          ≈⟨ E.∘-resp-l (fmap-∘ G) ⟩
            fmap G (forth H≅I D.∘ fmap H f) E.∘ forth F≅G
          ≈⟨ E.∘-resp-l (fmap-resp G fnat-HI) ⟩
            fmap G (fmap I f D.∘ forth H≅I) E.∘ forth F≅G
          ≈⟨ E.∘-resp-l (E.≈.sym (fmap-∘ G)) ⟩
            (fmap G (fmap I f) E.∘ fmap G (forth H≅I)) E.∘ forth F≅G
          ≈⟨ simp! E ⟩
            fmap G (fmap I f) E.∘ fmap G (forth H≅I) E.∘ forth F≅G
          ∎
      }
    where
      module D = Category D
      module E = Category E
      open E.≈-Reasoning

  id-r : {F : C ⇒ D} → F ∘ id ≈ F
  id-r {F} = record
      { iso = D.≅.refl
      ; forth-natural = D.≈.trans D.id-l (D.≈.sym D.id-r)
      }
    where
      module D = Category D

  id-l : {F : C ⇒ D} → id ∘ F ≈ F
  id-l {F} = record
      { iso = D.≅.refl
      ; forth-natural = D.≈.trans D.id-l (D.≈.sym D.id-r)
      }
    where
      module D = Category D

  assoc : ∀ {lo″ la″ l≈″ lo‴ la‴ l≈‴}
    → {E : Category lo″ la″ l≈″} {X : Category lo‴ la‴ l≈‴}
    → (F : E ⇒ X) (G : D ⇒ E) (H : C ⇒ D)
    → (F ∘ G) ∘ H ≈ F ∘ (G ∘ H)
  assoc {E = E} {X} _ _ _ = record
      { iso = X.≅.refl
      ; forth-natural = X.≈.trans X.id-l (X.≈.sym X.id-r)
      }
    where
      module X = Category X

instance
  Cat : ∀ lo la l≈
    → Category (suc (lo ⊔ la ⊔ l≈)) (lo ⊔ la ⊔ l≈) (lo ⊔ la ⊔ l≈)
  Cat lo la l≈ = record
      { Obj = Category lo la l≈
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = _∘_
      ; equiv = equiv
      ; ∘-resp = ∘-resp
      ; id-r = id-r
      ; id-l = id-l
      ; assoc = λ {_} {_} {_} {_} {F} {G} {H} → assoc F G H
      }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
open import Peano using (ℕ; zero; succ; _+_; Rel)

module Semigroup where

  infix 4 _≡_

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

  record Semigroup {A : Set} (_◇_ : A → A → A) : Set where
    field
      associativity : ∀ x y z → (x ◇ y) ◇ z ≡ x ◇ (y ◇ z)

  record ℕ+-isSemigroup : Semigroup _+_ where
    field
      associativity : ∀ x y z → (x + y) + z ≡ x + (y + z)

max_stars_repo_name: cantsin/agda-experiments

max_issues_repo_name: cantsin/agda-experiments

max_forks_repo_name: cantsin/agda-experiments


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core

-- slice category (https://ncatlab.org/nlab/show/over+category)
-- TODO: Forgetful Functor from Slice to 𝒞
module Categories.Category.Slice {o ℓ e} (𝒞 : Category o ℓ e) where

open Category 𝒞
open HomReasoning

open import Level
open import Function using (_$_)
open import Relation.Binary using (Rel)

open import Categories.Morphism.Reasoning 𝒞

record SliceObj (X : Obj) : Set (o ⊔ ℓ) where
  constructor sliceobj
  field
    {Y} : Obj
    arr : Y ⇒ X

private
  variable
    A : Obj
    X Y Z : SliceObj A

record Slice⇒ {A : Obj} (X Y : SliceObj A) : Set (ℓ ⊔ e) where
  constructor slicearr
  module X = SliceObj X
  module Y = SliceObj Y
  field
    {h} : X.Y ⇒ Y.Y
    △   : Y.arr ∘ h ≈ X.arr

Slice : Obj → Category _ _ _
Slice A       = record
  { Obj       = SliceObj A
  ; _⇒_       = Slice⇒
  ; _≈_       = λ where
    (slicearr {f} _) (slicearr {g} _) → f ≈ g
  ; id        = slicearr identityʳ
  ; _∘_       = _∘′_
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = record -- must be expanded to get levels to work out
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  ; ∘-resp-≈  = ∘-resp-≈
  }
  where _∘′_ : Slice⇒ Y Z → Slice⇒ X Y → Slice⇒ X Z
        _∘′_ {Y = sliceobj y} {Z = sliceobj z} {X = sliceobj x} (slicearr {g} △) (slicearr {f} △′) = slicearr $ begin
          z ∘ g ∘ f ≈⟨ pullˡ △ ⟩
          y ∘ f     ≈⟨ △′ ⟩
          x         ∎

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Holes.Term where

open import Holes.Prelude

-- TODO: This logically ought to be abstract, but that breaks the `cong!` macro
-- because when it is abstract, `⌞ x ⌟ ≡ x` does not hold (at least
-- definitionally). Look into a way of fixing this.
⌞_⌟ : ∀ {a}{A : Set a} → A → A
⌞ x ⌟ = x

private
  -- Given a term, if it is a hole, returns the list of arguments given to it.
  -- Otherwise returns nothing.

  toHole : Term → Maybe (List (Arg Term))
  -- First three arguments are the parameters of `⌞_⌟`, respectively the universe
  -- level `a`, the set `A` and the explicit parameter (i.e. the thing in the
  -- hole). So these are ignored.
  toHole (def (quote ⌞_⌟) (_ ∷ _ ∷ _ ∷ args)) = just args
  toHole _ = nothing

-- A HoleyTerm is an Agda term that has a single 'hole' in it, where another
-- term fits

data HoleyTerm : Set where
  hole : (args : List (Arg Term)) → HoleyTerm
  var : (x : ℕ) (args : List (Arg HoleyTerm)) → HoleyTerm
  con : (c : Name) (args : List (Arg HoleyTerm)) → HoleyTerm
  def : (f : Name) (args : List (Arg HoleyTerm)) → HoleyTerm
  lam : (v : Visibility) (holeyAbs : Abs HoleyTerm) → HoleyTerm
  pi : (a : Arg HoleyTerm) (b : Abs HoleyTerm) → HoleyTerm
  agda-sort : (s : Sort) → HoleyTerm
  lit : (l : Literal) → HoleyTerm
  unknown : HoleyTerm
  meta : (x : Meta) (args : List (Arg HoleyTerm)) → HoleyTerm

data HoleyErr : Set where
  noHole : HoleyErr
  unsupportedTerm : Term → HoleyErr
  mismatchedHoleTerms : HoleyErr

printHoleyErr : Term → HoleyErr → List ErrorPart
printHoleyErr goalLhs noHole
  = strErr "LHS of goal type contains no hole:"
  ∷ termErr goalLhs
  ∷ []
printHoleyErr goalLhs (unsupportedTerm x)
  = strErr "Goal type's LHS"
  ∷ termErr goalLhs
  ∷ strErr "contains unsupported term"
  ∷ termErr x
  ∷ []
printHoleyErr goalLhs mismatched-hole-terms
  = strErr "Terms in different holes failed to unify with each other."
  ∷ strErr "Check that every hole has an identical term in it."
  ∷ strErr "Offending term:"
  ∷ termErr goalLhs
  ∷ []

private
  mapArglist : {A B : Set} → (A → B) → List (Arg A) → List (Arg B)
  mapArglist = map ∘ mapArg

-- Converts a HoleyTerm to a regular term by filling in the hole with some other
-- given term which is a function of the number of binders encountered on the
-- way to the hole.
--
-- Free variables inside the holey term are detected and modified using the
-- provided function, because otherwise they might interact wrongly with
-- surrounding terms in the result.

{-# TERMINATING #-}
fillHoley : (ℕ → ℕ) → ℕ → (ℕ → List (Arg Term) → Term) → HoleyTerm → Term
fillHoley freeVarMod binderDepth filler = go binderDepth
  where
  go : ℕ → HoleyTerm → Term
  go depth (hole args) = filler depth args
  go _ (lit l) = lit l
  go depth (var x args) =
    let freeVar = not (x <? depth)
    in var (if freeVar then freeVarMod x else x) (mapArglist (go depth) args)
  go depth (con c args) = con c (mapArglist (go depth) args)
  go depth (def f args) = def f (mapArglist (go depth) args)
  go depth (meta x args) = meta x (mapArglist (go depth) args)
  go depth (lam v (abs s holey)) = lam v (abs s (go depth holey))
  go depth (pi (arg v a) (abs s b)) =
    pi (arg v (go depth a))
       (abs s (go depth b))
  go _ (agda-sort s) = agda-sort s
  go _ unknown = unknown

-- Converts a HoleyTerm to a regular term which abstracts a variable that is
-- used to fill the hole.
--
-- The `suc` function is provided for `fillHoley`'s `freeVarMod` parameter.
-- This is because the binding level of any free variables in the given term
-- will need to be lifted over the new lambda that we're introducing. Otherwise
-- they'll end up referring to the new lambda's variables, which is wrong. Bound
-- variables inside the given term don't need to be changed.

holeyToLam : HoleyTerm → Term
holeyToLam holey = lam visible (abs "hole" (fillHoley suc 0 var holey))

-- Converts a HoleyTerm to a regular term by filling in the hole with a constant
-- other term.

fillHoley′ : (List (Arg Term) → Term) → HoleyTerm → Term
fillHoley′ filler = fillHoley id 0 (λ _ → filler)

private
  mapPair : ∀ {a b x y}{A : Set a}{B : Set b}{X : Set x}{Y : Set y} → (A → X) → (B → Y) → A × B → X × Y
  mapPair f g (x , y) = f x , g y

  pushArg : ∀ {A B : Set} → Arg (A × B) → A × Arg B
  pushArg (arg i (x , y)) = x , arg i y

  mutual
    argHelper : (List (Arg HoleyTerm) → HoleyTerm) → List (Arg Term) → Result HoleyErr (List Term × HoleyTerm)
    argHelper buildHoley
      = fmap (mapPair concat buildHoley ∘ unzip)
      ∘ traverse (fmap pushArg ∘ traverse termToHoleyHelper)

    {-# TERMINATING #-}
    termToHoleyHelper : Term → Result HoleyErr (List Term × HoleyTerm)
    termToHoleyHelper term with toHole term
    termToHoleyHelper term | just args = ok (term ∷ [] , hole args)
    termToHoleyHelper (lit l) | nothing = ok ([] , lit l)
    termToHoleyHelper (var x args) | nothing = argHelper (var x) args
    termToHoleyHelper (con c args) | nothing = argHelper (con c) args
    termToHoleyHelper (def f args) | nothing = argHelper (def f) args
    termToHoleyHelper (meta x args) | nothing = argHelper (meta x) args
    termToHoleyHelper (lam v (abs s t)) | nothing =
      mapPair id (λ h → lam v (abs s h)) <$> termToHoleyHelper t
    termToHoleyHelper (pi (arg v a) (abs s b)) | nothing =
      termToHoleyHelper a >>=² λ ts₁ a′ →
      termToHoleyHelper b >>=² λ ts₂ b′ →
      return (ts₁ ++ ts₂ , pi (arg v a′) (abs s b′))
    termToHoleyHelper unknown | nothing = ok ([] , unknown)
    termToHoleyHelper (agda-sort s) | nothing = ok ([] , agda-sort s)
    ... | _ = err (unsupportedTerm term)

-- If a term has a hole in it, specified by ⌞_⌟ around a subterm, returns a
-- HoleyTerm with the hole removed.

termToHoley : Term → Result HoleyErr HoleyTerm
termToHoley term = proj₂ <$> termToHoleyHelper term

-- A variant of `termToHoley` that also returns the term in the hole. If there
-- are multiple holes, returns all of the terms that are in them.

termToHoley′ : Term → Result HoleyErr (List Term × HoleyTerm)
termToHoley′ = termToHoleyHelper

private
  unifyAll : List Term → TC (Maybe Term)
  unifyAll [] = return nothing
  unifyAll (x ∷ xs) = traverse- (unify x) xs >> return (just x)

checkedTermToHoley : Term → RTC HoleyErr (Term × HoleyTerm)
checkedTermToHoley term =
  liftResult (termToHoley′ term) >>=² λ holeTerms holey →
  liftTC (unifyAll holeTerms)
    ⟨ catchRTC ⟩
  throw mismatchedHoleTerms >>= λ
  { nothing → return (fillHoley′ (λ _ → unknown) holey , hole [])
  ; (just holeTerm) → return (holeTerm , holey)
  }

-- A variant of `termToHoley` that also returns the term in the hole, and checks
-- that the holey term is valid by unifying it with the original term. The list
-- of error parts given is thrown as a type error if the term could not be
-- converted to a holey term. Also, if there are no holes, treats the entire
-- expression as a hole.

checkedTermToHoley′ : (HoleyErr → List ErrorPart) → Term → TC (Term × HoleyTerm)
checkedTermToHoley′ error =
  runRTC (typeError ∘ error) ∘ checkedTermToHoley

-- These macros are useful for debugging and testing

macro
  -- Given a holey term, expands to a function which accepts something to go in
  -- the hole.

  lambdaIntoHole : Term → Term → TC ⊤
  lambdaIntoHole term target =
    checkedTermToHoley′ (λ _ → strErr "Unsupported term for holiness or no hole:"
                                ∷ termErr term
                                ∷ []) term >>=² λ _ →
    unify target ∘ holeyToLam

  -- Given a holey term, expands to the quoted form of a function which accepts
  -- something to go in the hole.

  lambdaIntoHole′ : Term → Term → TC ⊤
  lambdaIntoHole′ term target =
    checkedTermToHoley′ (λ _ → strErr "Unsupported term for holiness or no hole:"
                                ∷ termErr term
                                ∷ []) term >>=² λ _ result →
    quoteTC (holeyToLam result) >>=
    unify target

  -- Quotes a holey term, reifying its abstract syntax tree.

  quoteHoley : Term → Term → TC ⊤
  quoteHoley term target =
    checkedTermToHoley′ (λ _ → strErr "Unsupported term for holiness or no hole:"
                                ∷ termErr term
                                ∷ []) term >>=² λ _ result →
    quoteTC result >>= unify target

  -- Quotes a holey term and also the term in the hole. Expanded type is always
  -- `Term × HoleyTerm`.

  quoteHoley′ : Term → Term → TC ⊤
  quoteHoley′ term target =
    checkedTermToHoley′ (λ _ → strErr "Unsupported term for holiness or no hole:"
                                ∷ termErr term
                                ∷ []) term >>=
    quoteTC >>= unify target

private
  module Tests where
    open PropEq using (_≡_; refl)

    data Fin : ℕ → Set where
      zero : ∀ {n} → Fin (suc n)
      suc : ∀ {n} → Fin n → Fin (suc n)

    eqTyped : ∀ {a}(A : Set a) → A → A → Set a
    eqTyped _ x y = x ≡ y

    syntax eqTyped A x y = x ≡[ A ] y

    -- Holes don't have to match the type of the bigger expression
    test1 : lambdaIntoHole (4 + 5 * length ⌞ 1 ∷ [] ⌟ + 7) ≡ λ hole → 4 + 5 * length hole + 7
    test1 = refl

    -- Holes can be around functions
    test2 : lambdaIntoHole (⌞ _+_ ⌟ 3 4) ≡[ ((ℕ → ℕ → ℕ) → ℕ) ] λ hole → hole 3 4
    test2 = refl

    -- Holey terms can contain free variables
    test3 : ∀ x y z → lambdaIntoHole (⌞ x + y ⌟ + z) ≡ λ hole → hole + z
    test3 x y z = refl

    -- Multiple holes are possible
    test4 : ∀ x y z → lambdaIntoHole (x + ⌞ y + z ⌟ * ⌞ y + z ⌟ + y * z) ≡ λ hole → x + hole * hole + y * z
    test4 x y z = refl

    -- Holes into Π types
    test5 : ∀ x y → lambdaIntoHole (Fin ⌞ x + y ⌟ → ℕ) ≡ λ hole → Fin hole → ℕ
    test5 x y = refl

    -- Constructors on the path
    test6 : (x y : ℕ) → lambdaIntoHole (ℕ.suc (x + ⌞ y ⌟ + y)) ≡ λ hole → suc (x + hole + y)
    test6 x y = refl


text:
-- Andreas, 2016-05-04 shrunk from the standard library

open import Common.Product

record ⊤ : Set where

IFun : Set → Set1
IFun I = I → I → Set → Set

------------------------------------------------------------------------
-- Indexed state monads

record RawIMonad {I : Set} (M : (i j : I) → Set → Set) : Set1 where
  field
    return : ∀ {i A} → A → M i i A
    _>>=_  : ∀ {i j k A B} → M i j A → (A → M j k B) → M i k B

record RawIMonadZero  {I : Set} (M : IFun I) : Set1 where
  field
    monad : RawIMonad M
    ∅     : ∀ {i j A} → M i j A

  open RawIMonad monad public

record RawIMonadPlus  {I : Set} (M : IFun I) : Set1 where
  field
    monadZero : RawIMonadZero M
    _∣_       : ∀ {i j A} → M i j A → M i j A → M i j A

  open RawIMonadZero monadZero public

RawMonad : (Set → Set) → Set1
RawMonad M = RawIMonad {I = ⊤} (λ _ _ → M)

RawMonadZero : (Set → Set) → Set1
RawMonadZero M = RawIMonadZero {I = ⊤} (λ _ _ → M)

RawMonadPlus : (Set → Set) → Set1
RawMonadPlus M = RawIMonadPlus {I = ⊤} (λ _ _ → M)

module RawMonad {M : Set → Set} (Mon : RawMonad M) where
  open RawIMonad Mon public

module RawMonadZero {M : Set → Set} (Mon : RawMonadZero M) where
  open RawIMonadZero Mon public

module RawMonadPlus {M : Set → Set} (Mon : RawMonadPlus M) where
  open RawIMonadPlus Mon public

IStateT : ∀  {I : Set} (S : I → Set) (M : Set → Set) (i j : I) (A : Set) → Set
IStateT S M i j A = S i → M (A × S j)

StateTIMonad : ∀ {I : Set} (S : I → Set) {M} →
               RawMonad M → RawIMonad (IStateT S M)
StateTIMonad S Mon = record
  { return = λ x s → return (x , s)
  ; _>>=_  = λ m f s → m s >>= λ as → let a , s' = as in f a s'
  }
  where open RawMonad Mon

StateTIMonadZero : ∀ {I : Set} (S : I → Set) {M} →
                   RawMonadZero M → RawIMonadZero (IStateT S M)
StateTIMonadZero S Mon = record
  { monad = StateTIMonad S (RawMonadZero.monad Mon)
  ; ∅     = λ s → ∅
  }
  where open RawMonadZero Mon

StateTIMonadPlus : ∀ {I : Set} (S : I → Set) {M} →
                   RawMonadPlus M → RawIMonadPlus (IStateT S M)
StateTIMonadPlus S Mon = record
  { monadZero = StateTIMonadZero S (RawIMonadPlus.monadZero Mon)
  ; _∣_       = λ m₁ m₂ s → m₁ s ∣ m₂ s
  }
  where open RawMonadPlus Mon

-- test = {!RawIMonadPlus.monadZero!}
-- test' = {! RawMonadPlus.monadZero !}


text:
module Structure.Logic.Constructive.Proofs where

open import Functional as Fn
open import Lang.Instance
open import Logic.Propositional as Logic using (_←_ ; _↔_)
open import Logic.Predicate     as Logic hiding (∀ₗ)
import      Lvl
import      Structure.Logic.Constructive.BoundedPredicate
import      Structure.Logic.Constructive.Predicate
import      Structure.Logic.Constructive.Propositional
open import Syntax.Function
open import Type

private variable ℓ ℓₗ ℓₘₗ ℓₒ ℓₚ : Lvl.Level
private variable Formula : Type{ℓₗ}
private variable Proof : Formula → Type{ℓₘₗ}
private variable Predicate : Type{ℓₚ}
private variable Domain : Type{ℓₒ}

module _ (Proof : Formula → Type{ℓₘₗ}) where
  open Structure.Logic.Constructive.Propositional(Proof)
  private variable X Y Z : Formula

  {-
  module _ ⦃ logic : ConstructiveLogic ⦄ where
    [⟵][⟶][∧]-[⟷]-equivalence : Proof(X ⟷ Y) ↔ (Proof(X ⟵ Y) Logic.∧ Proof(X ⟶ Y))
    [⟵][⟶][∧]-[⟷]-equivalence {X} {Y} = Logic.[↔]-intro
      (p ↦ ⟷.intro (⟵.elim(Logic.[∧]-elimₗ p)) (⟶.elim(Logic.[∧]-elimᵣ p)))
      (p ↦ Logic.[∧]-intro (⟵.intro (⟷.elimₗ p)) (⟶.intro (⟷.elimᵣ p)))
  -}

  [⟶]-redundancyₗ : ⦃ impl : ∃(Implication) ⦄ → Proof(X ⟶ (X ⟶ Y)) → Proof(X ⟶ Y)
  [⟶]-redundancyₗ = ⟶.intro ∘ swap apply₂ ∘ (⟶.elim ∘₂ ⟶.elim)

  [⟷]-reflexivity : ∀{_⟷_} → ⦃ Equivalence(_⟷_) ⦄ → Proof(X ⟷ X)
  [⟷]-reflexivity = ⟷.intro id id

  [⟵]-to-[⟶] : ⦃ con : ∃(Consequence) ⦄ → ∃(Implication)
  ∃.witness [⟵]-to-[⟶] = swap(_⟵_)
  Implication.intro (∃.proof [⟵]-to-[⟶]) = ⟵.intro
  Implication.elim  (∃.proof [⟵]-to-[⟶]) = ⟵.elim

  [⟶]-to-[⟵] : ⦃ impl : ∃(Implication) ⦄ → ∃(Consequence)
  ∃.witness [⟶]-to-[⟵] = swap(_⟶_)
  Consequence.intro (∃.proof [⟶]-to-[⟵]) = ⟶.intro
  Consequence.elim  (∃.proof [⟶]-to-[⟵]) = ⟶.elim

  [⟵][⟶][∧]-to-[⟷] : ⦃ con : ∃(Consequence) ⦄ → ⦃ impl : ∃(Implication) ⦄ → ⦃ or : ∃(Conjunction) ⦄ → ∃(Equivalence)
  ∃.witness [⟵][⟶][∧]-to-[⟷] X Y = (X ⟵ Y) ∧ (X ⟶ Y)
  Equivalence.intro (∃.proof [⟵][⟶][∧]-to-[⟷]) yx xy = ∧.intro (⟵.intro yx) (⟶.intro xy)
  Equivalence.elimₗ (∃.proof [⟵][⟶][∧]-to-[⟷])       = ⟵.elim ∘ ∧.elimₗ
  Equivalence.elimᵣ (∃.proof [⟵][⟶][∧]-to-[⟷])       = ⟶.elim ∘ ∧.elimᵣ

  [⟶][⟷]-to-[∧] : ⦃ impl : ∃(Implication) ⦄ → ⦃ eq : ∃(Equivalence) ⦄ → ∃(Conjunction)
  ∃.witness [⟶][⟷]-to-[∧] X Y = (X ⟶ Y) ⟷ X
  Conjunction.intro (∃.proof [⟶][⟷]-to-[∧]) x y = ⟷.intro (const(⟶.intro(const y))) (const x)
  Conjunction.elimₗ (∃.proof [⟶][⟷]-to-[∧]) xyx = ⟷.elimᵣ xyx (⟶.intro(swap apply₂(⟶.elim ∘ ⟷.elimₗ xyx)))
  Conjunction.elimᵣ (∃.proof [⟶][⟷]-to-[∧]) xyx = apply₂(⟷.elimᵣ xyx (⟶.intro(swap apply₂ (⟶.elim ∘ ⟷.elimₗ xyx)))) (⟶.elim ∘ (⟷.elimₗ xyx))

  [∨][⟷]-to-[⟶] : ⦃ or : ∃(Disjunction) ⦄ → ⦃ eq : ∃(Equivalence) ⦄ → ∃(Implication)
  ∃.witness [∨][⟷]-to-[⟶] X Y = (X ∨ Y) ⟷ Y
  Implication.intro (∃.proof [∨][⟷]-to-[⟶])       = ⟷.intro ∨.introᵣ ∘ swap ∨.elim id
  Implication.elim  (∃.proof [∨][⟷]-to-[⟶]) xyy x = ⟷.elimᵣ xyy (∨.introₗ x)

  [∧][⟷]-to-[⟶] : ⦃ and : ∃(Conjunction) ⦄ → ⦃ eq : ∃(Equivalence) ⦄ → ∃(Implication)
  ∃.witness [∧][⟷]-to-[⟶] X Y = (X ∧ Y) ⟷ X
  Implication.intro (∃.proof [∧][⟷]-to-[⟶]) xy    = ⟷.intro (x ↦ ∧.intro x (xy x)) ∧.elimₗ
  Implication.elim  (∃.proof [∧][⟷]-to-[⟶]) xyx x = ∧.elimᵣ(⟷.elimₗ xyx x)

  [¬][⊤]-to-[⊥] : ⦃ neg : ∃(Negation) ⦄ → ⦃ top : ∃(Top) ⦄ → ∃(Bottom)
  ∃.witness [¬][⊤]-to-[⊥] = ¬ ⊤
  Bottom.elim (∃.proof [¬][⊤]-to-[⊥]) = ¬.elim ⊤.intro

  [¬][⊥]-to-[⊤] : ⦃ neg : ∃(Negation) ⦄ → ⦃ bot : ∃(Bottom) ⦄ → ∃(Top)
  ∃.witness [¬][⊥]-to-[⊤] = ¬ ⊥
  Top.intro (∃.proof [¬][⊥]-to-[⊤]) = ¬.intro{Y = ⊥} ⊥.elim ⊥.elim

  [⟷]-to-[⊤] : Formula → ⦃ eq : ∃(Equivalence) ⦄ → ∃(Top)
  ∃.witness ([⟷]-to-[⊤] φ) = φ ⟷ φ
  Top.intro (∃.proof ([⟷]-to-[⊤] φ)) = [⟷]-reflexivity

  [⟷][⊥]-to-[¬] : ⦃ eq : ∃(Equivalence) ⦄ → ⦃ bot : ∃(Bottom) ⦄ → ∃(Negation)
  ∃.witness [⟷][⊥]-to-[¬] = _⟷ ⊥
  Negation.intro (∃.proof [⟷][⊥]-to-[¬]) xy xy⊥ = ⟷.intro ⊥.elim ((⟷.elimᵣ ∘ xy⊥) ∘ₛ xy)
  Negation.elim  (∃.proof [⟷][⊥]-to-[¬])        = ⊥.elim ∘₂ swap ⟷.elimᵣ

  [∨][⟷][⊥]-adequacy : ⦃ or : ∃(Disjunction) ⦄ → ⦃ eq : ∃(Equivalence) ⦄ → ⦃ bot : ∃(Bottom) ⦄ → Logic
  Logic.top         [∨][⟷][⊥]-adequacy = [⟷]-to-[⊤] ⊥
  Logic.implication [∨][⟷][⊥]-adequacy = [∨][⟷]-to-[⟶]
  Logic.negation    [∨][⟷][⊥]-adequacy = [⟷][⊥]-to-[¬]
  Logic.conjunction [∨][⟷][⊥]-adequacy = [⟶][⟷]-to-[∧] where instance _ = Logic.implication [∨][⟷][⊥]-adequacy
  Logic.consequence [∨][⟷][⊥]-adequacy = [⟶]-to-[⟵]    where instance _ = Logic.implication [∨][⟷][⊥]-adequacy

module _ (Proof : Formula → Type{ℓₘₗ}) where
  open Structure.Logic.Constructive.Propositional(Proof)
  private variable X Y Z : Formula

  open import Data.Tuple as Tuple using ()

  [⊤]-preserving-type : ⦃ top : ∃(Top) ⦄ → Proof(⊤) ↔ Logic.⊤
  Tuple.left  [⊤]-preserving-type = const ⊤.intro
  Tuple.right [⊤]-preserving-type = const Logic.[⊤]-intro

  [∧]-preserving-type : ⦃ and : ∃(Conjunction) ⦄ → Proof(X ∧ Y) ↔ (Proof(X) Logic.∧ Proof(Y))
  Tuple.left  [∧]-preserving-type (Logic.[∧]-intro x y) = ∧.intro x y
  Tuple.right [∧]-preserving-type xy                    = Logic.[∧]-intro (∧.elimₗ xy) (∧.elimᵣ xy)

  [∨]-preserving-type : ⦃ or : ∃(Disjunction) ⦄ → Proof(X ∨ Y) ← (Proof(X) Logic.∨ Proof(Y))
  [∨]-preserving-type = Logic.[∨]-elim ∨.introₗ ∨.introᵣ

  [⟶]-preserving-type : ⦃ impl : ∃(Implication) ⦄ → Proof(X ⟶ Y) ↔ (Proof(X) → Proof(Y))
  Tuple.left  [⟶]-preserving-type = ⟶.intro
  Tuple.right [⟶]-preserving-type = ⟶.elim

  [⟵]-preserving-type : ⦃ cons : ∃(Consequence) ⦄ → Proof(X ⟵ Y) ↔ (Proof(X) ← Proof(Y))
  Tuple.left  [⟵]-preserving-type = ⟵.intro
  Tuple.right [⟵]-preserving-type = ⟵.elim

  [⟷]-preserving-type : ⦃ eq : ∃(Equivalence) ⦄ → Proof(X ⟷ Y) ↔ (Proof(X) ↔ Proof(Y))
  Tuple.left  [⟷]-preserving-type xy = ⟷.intro (Logic.[↔]-to-[←] xy) (Logic.[↔]-to-[→] xy)
  Tuple.right [⟷]-preserving-type xy = Logic.[↔]-intro (⟷.elimₗ xy) (⟷.elimᵣ xy)

  {-
  module Test ⦃ logic : Logic ⦄ where
    pure : ∀{A : Formula} → Proof(A) → Proof(A)
    pure = id

    _<*>_ : ∀{A B : Formula} → Proof(A ⟶ B) → Proof(A) → Proof(B)
    _<*>_ = ⟶.elim

    test : ∀{A B} → Proof(A ⟶ (A ⟶ B)) → Proof(A) → Proof(B)
    test ab a = ⦇ ab a a ⦈

  module Test2 ⦃ logic : ConstructiveLogic ⦄ {Obj : Type{ℓ}} where
    private variable P : Obj → Formula

    module _ ⦃ all : ∃(Universal) ⦄ where
      pure : ∀{A : Formula} → Proof(A) → Proof(A)
      pure = id

      _<*>_ : ∀{P : Obj → Formula} → Proof(∀ₗ P) → (x : Obj) → Proof(P(x))
      _<*>_ = ∀ₗ.elim

      test : ∀{A : Obj → Obj → Formula} → Proof(∀ₗ(x ↦ ∀ₗ(y ↦ A x y))) → (x : Obj) → Proof(A x x)
      test a x  = ⦇ a x x ⦈
  -}

module _ where
  open import Data
  open import Data.Tuple
  open import Data.Either as Either
  open        Structure.Logic.Constructive.BoundedPredicate renaming (Logic to BoundedPredicateLogic)
  open        Structure.Logic.Constructive.Predicate        renaming (Logic to PredicateLogic)
  open        Structure.Logic.Constructive.Propositional    renaming (Logic to PropositionalLogic)

  instance
    typePropositionalLogic : PropositionalLogic{Formula = Type{ℓ}} id
    PropositionalLogic.bottom      typePropositionalLogic = [∃]-intro Empty     ⦃ record{elim = empty} ⦄
    PropositionalLogic.top         typePropositionalLogic = [∃]-intro Unit      ⦃ record{intro = <>} ⦄
    PropositionalLogic.implication typePropositionalLogic = [∃]-intro _→ᶠ_      ⦃ record{intro = _$_ ; elim = id} ⦄
    PropositionalLogic.conjunction typePropositionalLogic = [∃]-intro _⨯_       ⦃ record{intro = _,_ ; elimₗ = left ; elimᵣ = right} ⦄
    PropositionalLogic.disjunction typePropositionalLogic = [∃]-intro _‖_       ⦃ record{introₗ = Left ; introᵣ = Right ; elim = Either.map1} ⦄
    PropositionalLogic.consequence typePropositionalLogic = [∃]-intro _←ᶠ_      ⦃ record{intro = id ; elim = _$_} ⦄
    PropositionalLogic.equivalence typePropositionalLogic = [∃]-intro Logic._↔_ ⦃ record{intro = _,_ ; elimₗ = left ; elimᵣ = right} ⦄
    PropositionalLogic.negation    typePropositionalLogic = [∃]-intro Logic.¬_  ⦃ record{intro = Fn.swap(_∘ₛ_) ; elim = empty ∘₂ apply} ⦄

  instance
    typePredicateLogic : ∀{T : Type{ℓₒ}} → PredicateLogic{Formula = Type{ℓₒ Lvl.⊔ ℓₗ}} id {Predicate = T → Type{ℓₒ Lvl.⊔ ℓₗ}} {Domain = T} id
    PredicateLogic.universal   typePredicateLogic = [∃]-intro Logic.∀ₗ ⦃ record{intro = id ; elim = id} ⦄
    PredicateLogic.existential typePredicateLogic = [∃]-intro Logic.∃  ⦃ record{intro = \{_}{x} p → Logic.[∃]-intro x ⦃ p ⦄ ; elim = Logic.[∃]-elim} ⦄

  open import Type.Dependent

  instance
    typeBoundedPredicateLogic : ∀{T : Type{ℓₒ}} → BoundedPredicateLogic{Formula = Type{ℓₒ Lvl.⊔ ℓₗ}} id {Predicate = (x : T) → ∀{B : T → Type{ℓₒ Lvl.⊔ ℓₗ}} → B(x) → Type{ℓₒ Lvl.⊔ ℓₗ}} {Domain = T} id
    BoundedPredicateLogic.universal   typeBoundedPredicateLogic = [∃]-intro (\B P → ∀{x} → (bx : B(x)) → P(x){B}(bx)) ⦃ record{intro = \p bx → p bx ; elim = \p bx → p bx} ⦄
    BoundedPredicateLogic.existential typeBoundedPredicateLogic = [∃]-intro (\B P → Logic.∃(x ↦ Σ(B(x)) (P(x){B}))) ⦃ record{intro = \{_}{x} bx p → Logic.[∃]-intro x ⦃ intro bx p ⦄ ; elim = \p → Logic.[∃]-elim (\(intro bx px) → p bx px)} ⦄

  {- TODO: Maybe have some more assumptions
  boundedPredicateLogic-to-predicateLogic : ∀{Formula Domain Predicate : Type{ℓₒ}}{Proof : Formula → Type}{_$_} → BoundedPredicateLogic{Formula = Formula} Proof {Predicate = Predicate} {Domain = Domain} (_$_) → PredicateLogic{Formula = Formula} Proof {Predicate = (Domain → Formula) ⨯ Predicate} {Domain = Σ(Predicate ⨯ Domain) (\(P , x) → Proof((P $ x) {{!!}} {!!}))} {!!}
  PredicateLogic.propositional (boundedPredicateLogic-to-predicateLogic L) = BoundedPredicateLogic.propositional L
  ∃.witness (PredicateLogic.universal (boundedPredicateLogic-to-predicateLogic L)) (B , P) = ∃.witness (BoundedPredicateLogic.universal L) B P
  Universal.intro (∃.proof (PredicateLogic.universal (boundedPredicateLogic-to-predicateLogic L))) {B , P} p = BoundedUniversal.intro
                                                                                (∃.proof (BoundedPredicateLogic.universal L)) (\{x} pp → p{intro (P , x) {!!}})
  Universal.elim (∃.proof (PredicateLogic.universal (boundedPredicateLogic-to-predicateLogic L))) = {!!}
  ∃.witness (PredicateLogic.existential (boundedPredicateLogic-to-predicateLogic L)) (B , P) = ∃.witness (BoundedPredicateLogic.existential L) B P
  Existential.intro (∃.proof (PredicateLogic.existential (boundedPredicateLogic-to-predicateLogic L))) = {!!}
  Existential.elim (∃.proof (PredicateLogic.existential (boundedPredicateLogic-to-predicateLogic L))) = {!!}
  -}

  {- TODO: Seems to need a duplicate (Domain → Formula) in Predicate. Also, does not work with this generality
  boundedPredicateLogic-to-predicateLogic : ∀{_$_} → BoundedPredicateLogic{Formula = Formula} Proof {Predicate = Predicate} {Domain = Domain} (_$_) → PredicateLogic{Formula = Formula} Proof {Predicate = Predicate} {Domain = Σ((Domain → Formula) ⨯ Domain) (\(B , x) → Proof(B(x)))} (\P (intro(B , x) bx) → (P $ x) {B} bx)
  PredicateLogic.propositional (boundedPredicateLogic-to-predicateLogic L) = BoundedPredicateLogic.propositional L
  PredicateLogic.universal (boundedPredicateLogic-to-predicateLogic L) = [∃]-intro {!!} ⦃ record{intro = {!!} ; elim = {!!}} ⦄
  PredicateLogic.existential (boundedPredicateLogic-to-predicateLogic L) = [∃]-intro {!!} ⦃ record{intro = {!!} ; elim = {!!}} ⦄
  -}

  {-instance
    typeBoundedPredicateLogic : ∀{T : Type{ℓₒ}}{B : T → Type{ℓ}} → PredicateLogic{Formula = Type{ℓₒ Lvl.⊔ ℓₗ Lvl.⊔ ℓ}} id {Predicate = (x : T) → ⦃ B(x) ⦄ → Type{ℓₒ Lvl.⊔ ℓₗ Lvl.⊔ ℓ}} {Domain = Σ T B} (\f (intro x b) → f x ⦃ b ⦄)
    PredicateLogic.universal   (typeBoundedPredicateLogic {B = B}) = [∃]-intro (f ↦ (∀{x} ⦃ bx ⦄ → f(x) ⦃ bx ⦄)) ⦃ record{intro = \px → px ; elim = \{P} px {x} → px{Σ.left x} ⦃ Σ.right x ⦄} ⦄
    PredicateLogic.existential (typeBoundedPredicateLogic {B = B}) = [∃]-intro (f ↦ Logic.∃(x ↦ Σ(B(x)) (bx ↦ f x ⦃ bx ⦄)) ) ⦃ record{intro = {!!} ; elim = {!!}} ⦄
  -}

  import      Logic.Classical.DoubleNegated as DoubleNegated
  open import Logic.Names
  import      Logic.Propositional.Theorems as Logic
  instance
    doubleNegatedTypeLogic : PropositionalLogic{ℓₘₗ = Lvl.𝟎}(Logic.¬¬_)
    PropositionalLogic.bottom      doubleNegatedTypeLogic = Logic.[∃]-intro Logic.⊥     ⦃ record{elim = DoubleNegated.[⊥]-elim} ⦄
    PropositionalLogic.top         doubleNegatedTypeLogic = Logic.[∃]-intro Logic.⊤     ⦃ record{intro = DoubleNegated.[⊤]-intro} ⦄
    PropositionalLogic.implication doubleNegatedTypeLogic = Logic.[∃]-intro (_→ᶠ_)      ⦃ record{intro = DoubleNegated.[→]-intro ; elim = DoubleNegated.[→]-elim} ⦄
    PropositionalLogic.conjunction doubleNegatedTypeLogic = Logic.[∃]-intro (Logic._∧_) ⦃ record{intro = DoubleNegated.[∧]-intro ; elimₗ = DoubleNegated.[∧]-elimₗ ; elimᵣ = DoubleNegated.[∧]-elimᵣ} ⦄
    PropositionalLogic.disjunction doubleNegatedTypeLogic = Logic.[∃]-intro (Logic._∨_) ⦃ record{introₗ = DoubleNegated.[∨]-introₗ ; introᵣ = DoubleNegated.[∨]-introᵣ ; elim = DoubleNegated.[∨]-elim} ⦄
    PropositionalLogic.consequence doubleNegatedTypeLogic = Logic.[∃]-intro (Logic._←_) ⦃ record{intro = DoubleNegated.[←]-intro ; elim = DoubleNegated.[→]-elim} ⦄
    PropositionalLogic.equivalence doubleNegatedTypeLogic = Logic.[∃]-intro (Logic._↔_) ⦃ record{intro = DoubleNegated.[↔]-intro ; elimₗ = DoubleNegated.[↔]-elimₗ ; elimᵣ = DoubleNegated.[↔]-elimᵣ} ⦄
    PropositionalLogic.negation    doubleNegatedTypeLogic = Logic.[∃]-intro (Logic.¬_)  ⦃ record{intro = Fn.swap(_∘ₛ_) ; elim = const ∘₂ apply} ⦄

  open import Data.Boolean
  import      Data.Boolean.Operators
  open        Data.Boolean.Operators.Programming
  open import Data.Boolean.Stmt
  open import Data.Boolean.Stmt.Proofs
  instance
    booleanLogic : PropositionalLogic IsTrue
    PropositionalLogic.bottom      booleanLogic = [∃]-intro 𝐹    ⦃ record{elim = Logic.[⊥]-elim ∘ IsTrue.[𝐹]-elim} ⦄
    PropositionalLogic.top         booleanLogic = [∃]-intro 𝑇    ⦃ record{intro = IsTrue.[𝑇]-intro} ⦄
    PropositionalLogic.conjunction booleanLogic = [∃]-intro _&&_ ⦃ record{intro = IsTrue.[∧]-intro ; elimₗ = IsTrue.[∧]-elimₗ ; elimᵣ = IsTrue.[∧]-elimᵣ} ⦄
    PropositionalLogic.disjunction booleanLogic = [∃]-intro _||_ ⦃ record{introₗ = IsTrue.[∨]-introₗ ; introᵣ = IsTrue.[∨]-introᵣ ; elim = IsTrue.[∨]-elim} ⦄
    PropositionalLogic.negation    booleanLogic = [∃]-intro !    ⦃ record{intro = IsTrue.[!]-intro ; elim = IsTrue.[!]-elim} ⦄
    PropositionalLogic.implication booleanLogic = [∃]-intro _→?_ ⦃ record{intro = IsTrue.[→?]-intro ; elim = IsTrue.[→?]-elim} ⦄
    PropositionalLogic.consequence booleanLogic = [∃]-intro _←?_ ⦃ record{intro = IsTrue.[←?]-intro ; elim = IsTrue.[←?]-elim} ⦄
    PropositionalLogic.equivalence booleanLogic = [∃]-intro _==_ ⦃ record{intro = IsTrue.[==]-intro ; elimₗ = IsTrue.[==]-elimₗ ; elimᵣ = IsTrue.[==]-elimᵣ} ⦄

  booleanPredicateLogic : ∀{T : Type{ℓ}}{all exist : (T → Bool) → Bool} → (∀{P} → (∀{x} → IsTrue(P(x))) ↔ IsTrue(all P)) → (∀{P} → (Logic.∃(x ↦ IsTrue(P(x)))) ↔ IsTrue(exist P)) → PredicateLogic IsTrue {Domain = T} id
  PredicateLogic.universal   (booleanPredicateLogic {all = all} {exist = exist} all-eq exist-eq) = [∃]-intro all   ⦃ record{intro = Logic.[↔]-to-[→] all-eq ; elim = Logic.[↔]-to-[←] all-eq} ⦄
  PredicateLogic.existential (booleanPredicateLogic {all = all} {exist = exist} all-eq exist-eq) = [∃]-intro exist ⦃ record{intro = Logic.[↔]-to-[→] exist-eq ∘ (p ↦ [∃]-intro _ ⦃ p ⦄) ; elim = p ↦ ep ↦ p(Logic.[∃]-proof(Logic.[↔]-to-[←] exist-eq ep))} ⦄


text:
module Logic where

-- The true proposition.
data ⊤ : Set where
  obvious : ⊤ -- The proof of truth.

-- The false proposition.
data ⊥ : Set where
  -- There is nothing here so one can never prove false.

-- The AND of two statments.
data _∧_ (A B : Set)  : Set where
  -- The only way to construct a proof of A ∧ B is by pairing a a
  -- proof of A with a proof of and B.
  ⟨_,_⟩ : (a : A)  -- Proof of A
        → (b : B)  -- Proof of B
        → A ∧ B    -- Proof of A ∧ B

-- The OR of two statements.
data _∨_ (A B : Set) : Set where
  -- There are two ways of constructing a proof of A ∨ B.
  inl : (a : A) →  A ∨ B   -- From a proof of A by left introduction
  inr : (b : B) →  A ∨ B   -- From a proof of B by right introduction

-- The not of statement A
¬_ : (A : Set) → Set
¬ A = A → ⊥  -- Given a proof of A one should be able to get a proof
             -- of ⊥.

-- The statement A ↔ B are equivalent.
_↔_ : (A B : Set) → Set
A ↔ B = (A → B) -- If
           ∧    -- and
        (B → A) -- only if

infixr 1 _∧_
infixr 1 _∨_
infixr 0 _↔_
infix  2 ¬_

-- Function composition
_∘_   : {A B C : Set} → (B → C) → (A → B) → A → C
(f ∘ g) x = f (g x)

-- Double negation
doubleNegation : ∀ {A : Set} → A → ¬ (¬ A)
doubleNegation a negNegA = negNegA a

{-

doubleNegation' : ∀ {A : Set} → ¬ ( ¬ (¬ A)) → ¬ A

-}

deMorgan1 : ∀ (A B : Set) → ¬ (A ∨ B) → ¬ A ∧ ¬ B
deMorgan1 A B notAorB = ⟨ notAorB ∘ inl , notAorB ∘ inr ⟩

deMorgan2 : ∀ (A B : Set) → ¬ A ∧ ¬ B → ¬ (A ∨ B)
deMorgan2 A B ⟨ notA , notB ⟩ (inl a) = notA a
deMorgan2 A B ⟨ notA , notB ⟩ (inr b) = notB b

deMorgan : ∀ (A B : Set) → ¬ (A ∨ B) ↔ ¬ A ∧ ¬ B
deMorgan A B = ⟨ deMorgan1 A B , deMorgan2 A B ⟩

max_stars_repo_name: piyush-kurur/sample-code

max_issues_repo_name: piyush-kurur/sample-code

max_forks_repo_name: piyush-kurur/sample-code


text:
module Data.Option.Categorical where

import Lvl
import      Functional as Fn
open import Function.Equals
open import Data.Option
open import Data.Option.Functions
open import Data.Option.Proofs
open import Lang.Instance
open import Logic
open import Logic.Predicate
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
import      Structure.Category.Functor as Functor
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type
open import Type.Category

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

-- Option is a functor by using `map`.
instance
  map-functor : Functor{ℓ}(Option)
  Functor.map           ⦃ map-functor ⦄ = map
  Functor.map-function  ⦃ map-functor ⦄ = map-function
  Functor.op-preserving ⦃ map-functor ⦄ = map-preserves-[∘]
  Functor.id-preserving ⦃ map-functor ⦄ = map-preserves-id

-- Option is a monad by using `andThen`.
instance
  andThen-monad : Monad{ℓ}(Option)
  Monad.η            ⦃ andThen-monad ⦄ _ = Some
  Monad.ext          ⦃ andThen-monad ⦄   = Fn.swap _andThen_
  Monad.ext-function ⦃ andThen-monad ⦄ = andThen-function
  Monad.ext-inverse  ⦃ andThen-monad ⦄ = andThenᵣ-Some
  Dependent._⊜_.proof (Monad.ext-identity   ⦃ andThen-monad ⦄) = [≡]-intro
  Dependent._⊜_.proof (Monad.ext-distribute ⦃ andThen-monad ⦄ {f = f} {g}) {x} = andThen-associativity {f = g}{g = f}{o = x}

-- A monoid is constructed by lifting an associative binary operator using `or-combine`.
-- Essentially means that an additional value (None) is added to the type, and it becomes an identity by definition.
module _ {_▫_ : T → T → T} where
  instance
    or-combine-monoid : ⦃ assoc : Associativity(_▫_) ⦄ → Monoid(or-combine(_▫_) Fn.id Fn.id)
    Associativity.proof (Monoid.associativity or-combine-monoid) {None}   {None}   {None}   = [≡]-intro
    Associativity.proof (Monoid.associativity or-combine-monoid) {None}   {None}   {Some z} = [≡]-intro
    Associativity.proof (Monoid.associativity or-combine-monoid) {None}   {Some y} {None}   = [≡]-intro
    Associativity.proof (Monoid.associativity or-combine-monoid) {None}   {Some y} {Some z} = [≡]-intro
    Associativity.proof (Monoid.associativity or-combine-monoid) {Some x} {None}   {None}   = [≡]-intro
    Associativity.proof (Monoid.associativity or-combine-monoid) {Some x} {None}   {Some z} = [≡]-intro
    Associativity.proof (Monoid.associativity or-combine-monoid) {Some x} {Some y} {None}   = [≡]-intro
    Associativity.proof (Monoid.associativity or-combine-monoid) {Some x} {Some y} {Some z} = [≡]-with(Some) (associativity(_▫_))
    ∃.witness (Monoid.identity-existence or-combine-monoid) = None
    Identityₗ.proof (Identity.left  (∃.proof (Monoid.identity-existence or-combine-monoid))) {None}   = [≡]-intro
    Identityₗ.proof (Identity.left  (∃.proof (Monoid.identity-existence or-combine-monoid))) {Some x} = [≡]-intro
    Identityᵣ.proof (Identity.right (∃.proof (Monoid.identity-existence or-combine-monoid))) {None}   = [≡]-intro
    Identityᵣ.proof (Identity.right (∃.proof (Monoid.identity-existence or-combine-monoid))) {Some x} = [≡]-intro

module _ {_▫_ : T → T → T} where
  open Monoid ⦃ … ⦄ using (id)

  -- A monoid is still a monoid when lifting a binary operator using `and-combine`.
  instance
    and-combine-monoid : ⦃ monoid : Monoid(_▫_) ⦄ → Monoid(and-combine(_▫_))
    Associativity.proof (Monoid.associativity and-combine-monoid) {None}   {None}   {None}   = [≡]-intro
    Associativity.proof (Monoid.associativity and-combine-monoid) {None}   {None}   {Some z} = [≡]-intro
    Associativity.proof (Monoid.associativity and-combine-monoid) {None}   {Some y} {None}   = [≡]-intro
    Associativity.proof (Monoid.associativity and-combine-monoid) {None}   {Some y} {Some z} = [≡]-intro
    Associativity.proof (Monoid.associativity and-combine-monoid) {Some x} {None}   {None}   = [≡]-intro
    Associativity.proof (Monoid.associativity and-combine-monoid) {Some x} {None}   {Some z} = [≡]-intro
    Associativity.proof (Monoid.associativity and-combine-monoid) {Some x} {Some y} {None}   = [≡]-intro
    Associativity.proof (Monoid.associativity and-combine-monoid) {Some x} {Some y} {Some z} = [≡]-with(Some) (associativity(_▫_))
    ∃.witness (Monoid.identity-existence and-combine-monoid) = Some(id)
    Identityₗ.proof (Identity.left  (∃.proof (Monoid.identity-existence and-combine-monoid))) {None}   = [≡]-intro
    Identityₗ.proof (Identity.left  (∃.proof (Monoid.identity-existence and-combine-monoid))) {Some x} = [≡]-with(Some) (identityₗ(_▫_)(_))
    Identityᵣ.proof (Identity.right (∃.proof (Monoid.identity-existence and-combine-monoid))) {None}   = [≡]-intro
    Identityᵣ.proof (Identity.right (∃.proof (Monoid.identity-existence and-combine-monoid))) {Some x} = [≡]-with(Some) (identityᵣ(_▫_)(_))

  instance
    and-combine-absorberₗ : Absorberₗ(and-combine(_▫_))(None)
    Absorberₗ.proof and-combine-absorberₗ = [≡]-intro

  instance
    and-combine-absorberᵣ : Absorberᵣ(and-combine(_▫_))(None)
    Absorberᵣ.proof and-combine-absorberᵣ {None}   = [≡]-intro
    Absorberᵣ.proof and-combine-absorberᵣ {Some x} = [≡]-intro

  -- `and-combine` essentially adds an additional value (None) to the type, and it becomes an absorber by definition.
  instance
    and-combine-absorber : Absorber(and-combine(_▫_))(None)
    and-combine-absorber = intro


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Truncation.FromNegOne where

open import Cubical.HITs.Truncation.FromNegOne.Base public
open import Cubical.HITs.Truncation.FromNegOne.Properties public


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

import Level

open import Data.Empty using (⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Fin using (Fin; zero; suc)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Control.Category

module Dimension.PartialWeakening (E : Set) where

-- Partial weakenings from n to m are injective maps from Fin n to Fin m
-- that can raise exceptions in E.

data PWeak : (n m : ℕ) → Set where
  []   :                                   PWeak 0 0              -- empty
  _∷_  : ∀ {n m} (e : E) (f : PWeak n m) → PWeak (1 + n) m        -- partial
  lift : ∀ {n m}         (f : PWeak n m) → PWeak (1 + n) (1 + m)  -- new name
  weak : ∀ {n m}         (f : PWeak n m) → PWeak n (1 + m)        -- unused n.

-- Empty.

empty : ∀ {m} → PWeak 0 m
empty {m = 0}     = []
empty {m = suc m} = weak (empty {m = m})

-- Identity.

id : ∀ {n} → PWeak n n
id {n = 0}     = []
id {n = suc n} = lift (id {n = n})

-- Composition.

comp : ∀ {n m l} → PWeak n m → PWeak m l → PWeak n l
comp []        _       = empty
comp (e ∷ f)   g       = e ∷ comp f g
comp (lift f) (e ∷ g)  = e ∷ comp f g
comp (lift f) (lift g) = lift (comp f g)
comp (lift f) (weak g) = weak (comp (lift f) g)
comp (weak f) (e ∷ g)  = comp f g
comp (weak f) (lift g) = weak (comp f g)
comp (weak f) (weak g) = weak (comp (weak f) g)

module Laws where

  -- Empty is initial (i.e., equal to any (g : PWeak 0 m))

  abstract
    empty-extensional : ∀ {m} (g : PWeak 0 m) → g ≡ empty
    empty-extensional []       = refl
    empty-extensional (weak g) = cong weak (empty-extensional g)

  -- Empty is left dominant

  abstract
    empty-comp : ∀ {n m} (g : PWeak n m) → comp empty g ≡ empty
    empty-comp g = empty-extensional (comp empty g)
{-
    empty-comp [] = refl
    empty-comp (e ∷ g) = empty-comp g
    empty-comp (lift g) = cong weak (empty-comp g)
    empty-comp {n = zero } (weak g) = refl
    empty-comp {n = suc n} (weak g) = cong weak (empty-comp g)
-}
  -- Left identity.

  abstract
    left-id : ∀ {n m} (g : PWeak n m) → comp id g ≡ g
    left-id             []       = refl
    left-id             (e ∷ g)  = cong (_∷_ e) (left-id g)
    left-id             (lift g) = cong lift (left-id g)
    left-id {n = zero}  (weak g) = cong weak (sym (empty-extensional g))
    left-id {n = suc n} (weak g) = cong weak (left-id g)

  -- Right identity.

  abstract
    right-id : ∀ {n m} (g : PWeak n m) → comp g id ≡ g
    right-id             []       = refl
    right-id             (e ∷ g)  = cong (_∷_ e) (right-id g)
    right-id             (lift g) = cong lift (right-id g)
    right-id {n = zero } (weak g) = cong weak (right-id g)
    right-id {n = suc n} (weak g) = cong weak (right-id g)

  -- Associativity.

  abstract
    assoc : ∀ {n m l k} (f : PWeak n m) (g : PWeak m l) (h : PWeak l k) →
      comp (comp f g) h ≡ comp f (comp g h)
    assoc []        g        h       = empty-extensional _
    assoc (e ∷ f)   g        h       = cong (_∷_ e) (assoc f g h)
    assoc (lift f) (e ∷ g)   h       = cong (_∷_ e) (assoc f g h)
    assoc (lift f) (lift g) (e ∷ h)  = cong (_∷_ e) (assoc f g h)
    assoc (lift f) (lift g) (lift h) = cong lift (assoc f g h)
    assoc (lift f) (lift g) (weak h) = cong weak (assoc (lift f) (lift g) h)
    assoc (lift f) (weak g) (e ∷ h)  = assoc (lift f) g h
    assoc (lift f) (weak g) (lift h) = cong weak (assoc (lift f) g h)
    assoc (lift f) (weak g) (weak h) = cong weak (assoc (lift f) (weak g) h)
    assoc (weak f) (e ∷ g)   h       = assoc f g h
    assoc (weak f) (lift g) (e ∷ h)  = assoc f g h
    assoc (weak f) (lift g) (lift h) = cong weak (assoc f g h)
    assoc (weak f) (lift g) (weak h) = cong weak (assoc (weak f) (lift g) h)
    assoc (weak f) (weak g) (e ∷ h)  = assoc (weak f) g h
    assoc (weak f) (weak g) (lift h) = cong weak (assoc (weak f) g h)
    assoc (weak f) (weak g) (weak h) = cong weak (assoc (weak f) (weak g) h)

open Laws

-- PWeak is a category with initial object

SPWeak = λ n m → setoid (PWeak n m)

pWeakIsCategory : IsCategory SPWeak
pWeakIsCategory = record
  { ops  = record
    { id  = id
    ; _⟫_ = comp
    }
  ; laws = record
    { id-first = left-id _
    ; id-last  = right-id _
    ; ∘-assoc  = λ f → assoc f _ _
    ; ∘-cong   = cong₂ comp
    }
  }

emptyIsInitial : IsInitial SPWeak 0
emptyIsInitial = record
  { initial = empty
  ; initial-universal = empty-extensional _
  }

-- The category PWEAK

PWEAK : Category _ _ _
PWEAK = record { Hom = SPWeak; isCategory = pWeakIsCategory }

-- -}

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homomorphism proofs for multiplication over polynomials
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

open import Data.Nat.Base as ℕ          using (ℕ; suc; zero; _<′_; _≤′_; ≤′-step; ≤′-refl)
open import Data.Nat.Properties    using (≤′-trans)
open import Data.Nat.Induction
open import Data.Product           using (_×_; _,_; proj₁; proj₂; map₁)
open import Data.List.Kleene
open import Data.Vec               using (Vec)
open import Function
open import Induction.WellFounded
open import Relation.Unary

open Homomorphism homo hiding (_^_)

open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition homo
open import Tactic.RingSolver.Core.Polynomial.Base from
open import Tactic.RingSolver.Core.Polynomial.Reasoning to
open import Tactic.RingSolver.Core.Polynomial.Semantics homo
open import Algebra.Operations.Ring rawRing

reassoc : ∀ {y} x z → x * (y * z) ≈ y * (x * z)
reassoc {y} x z = sym (*-assoc x y z) ⟨ trans ⟩ ((≪* *-comm x y) ⟨ trans ⟩ *-assoc y x z)

mutual
  ⊠-step′-hom : ∀ {n} → (a : Acc _<′_ n) → (xs ys : Poly n) → ∀ ρ → ⟦ ⊠-step′ a xs ys ⟧ ρ ≈ ⟦ xs ⟧ ρ * ⟦ ys ⟧ ρ
  ⊠-step′-hom a (x ⊐ p) = ⊠-step-hom a x p

  ⊠-step-hom : ∀ {i n}
             → (a : Acc _<′_ n)
             → (xs : FlatPoly i)
             → (i≤n : i ≤′ n)
             → (ys : Poly n)
             → ∀ ρ → ⟦ ⊠-step a xs i≤n ys ⟧ ρ ≈ ⟦ xs ⊐ i≤n ⟧ ρ * ⟦ ys ⟧ ρ
  ⊠-step-hom a (Κ x) i≤n = ⊠-Κ-hom a x
  ⊠-step-hom a (⅀ xs) i≤n = ⊠-⅀-hom a xs i≤n

  ⊠-Κ-hom : ∀ {n}
          → (a : Acc _<′_ n)
          → ∀ x
          → (ys : Poly n)
          → ∀ ρ
          → ⟦ ⊠-Κ a x ys ⟧ ρ ≈ ⟦ x ⟧ᵣ * ⟦ ys ⟧ ρ
  ⊠-Κ-hom (acc _)  x (Κ y  ⊐ i≤n) ρ = *-homo x y
  ⊠-Κ-hom (acc wf) x (⅀ xs ⊐ i≤n) ρ =
    begin
      ⟦ ⊠-Κ-inj (wf _ i≤n) x xs ⊐↓ i≤n ⟧ ρ
    ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf _ i≤n) x xs) i≤n ρ ⟩
      ⅀?⟦ ⊠-Κ-inj (wf _ i≤n) x xs ⟧ (drop-1 i≤n ρ)
    ≈⟨ ⊠-Κ-inj-hom (wf _ i≤n) x xs (drop-1 i≤n ρ) ⟩
      ⟦ x ⟧ᵣ * ⅀⟦ xs ⟧ (drop-1 i≤n ρ)
    ∎

  ⊠-Κ-inj-hom : ∀ {n}
              → (a : Acc _<′_ n)
              → (x : Raw.Carrier)
              → (xs : Coeff n +)
              → ∀ ρ
              → ⅀?⟦ ⊠-Κ-inj a x xs ⟧ ρ ≈ ⟦ x ⟧ᵣ * ⅀⟦ xs ⟧ ρ
  ⊠-Κ-inj-hom {n} a x xs (ρ , Ρ) =
    poly-mapR
      ρ
      Ρ
      (⊠-Κ a x)
      (⟦ x ⟧ᵣ *_)
      (*-cong refl)
      reassoc
      (distribˡ ⟦ x ⟧ᵣ)
      (λ ys → ⊠-Κ-hom a x ys Ρ)
      (zeroʳ _)
      xs

  ⊠-⅀-hom : ∀ {i n}
          → (a : Acc _<′_ n)
          → (xs : Coeff i +)
          → (i<n : i <′ n)
          → (ys : Poly n)
          → ∀ ρ
          → ⟦ ⊠-⅀ a xs i<n ys ⟧ ρ ≈ ⅀⟦ xs ⟧ (drop-1 i<n ρ) * ⟦ ys ⟧ ρ
  ⊠-⅀-hom (acc wf) xs i<n (⅀ ys ⊐ j≤n) = ⊠-match-hom (acc wf) (inj-compare i<n j≤n) xs ys
  ⊠-⅀-hom (acc wf) xs i<n (Κ y  ⊐ _) ρ =
    begin
      ⟦ ⊠-Κ-inj (wf _ i<n) y xs ⊐↓ i<n ⟧ ρ
    ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf _ i<n) y xs) i<n ρ ⟩
      ⅀?⟦ ⊠-Κ-inj (wf _ i<n) y xs ⟧ (drop-1 i<n ρ)
    ≈⟨ ⊠-Κ-inj-hom (wf _ i<n) y xs (drop-1 i<n ρ) ⟩
      ⟦ y ⟧ᵣ * ⅀⟦ xs ⟧ (drop-1 i<n ρ)
    ≈⟨ *-comm _ _ ⟩
      ⅀⟦ xs ⟧ (drop-1 i<n ρ) * ⟦ y ⟧ᵣ
    ∎

  ⊠-⅀-inj-hom : ∀ {i k}
              → (a : Acc _<′_ k)
              → (i<k : i <′ k)
              → (xs : Coeff i +)
              → (ys : Poly k)
              → ∀ ρ
              → ⟦ ⊠-⅀-inj a i<k xs ys ⟧ ρ ≈ ⅀⟦ xs ⟧ (drop-1 i<k ρ) * ⟦ ys ⟧ ρ
  ⊠-⅀-inj-hom (acc wf) i<k x (⅀ ys ⊐ j≤k) = ⊠-match-hom (acc wf) (inj-compare i<k j≤k) x ys
  ⊠-⅀-inj-hom (acc wf) i<k x (Κ y ⊐ j≤k) ρ =
    begin
      ⟦ ⊠-Κ-inj (wf _ i<k) y x ⊐↓ i<k ⟧ ρ
    ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf _ i<k) y x) i<k ρ ⟩
      ⅀?⟦ ⊠-Κ-inj (wf _ i<k) y x ⟧ (drop-1 i<k ρ)
    ≈⟨ ⊠-Κ-inj-hom (wf _ i<k) y x (drop-1 i<k ρ) ⟩
      ⟦ y ⟧ᵣ * ⅀⟦ x ⟧ (drop-1 i<k ρ)
    ≈⟨ *-comm _ _ ⟩
      ⅀⟦ x ⟧ (drop-1 i<k ρ) * ⟦ y ⟧ᵣ
    ∎

  ⊠-match-hom : ∀ {i j n}
              → (a : Acc _<′_ n)
              → {i<n : i <′ n}
              → {j<n : j <′ n}
              → (ord : InjectionOrdering i<n j<n)
              → (xs : Coeff i +)
              → (ys : Coeff j +)
              → (Ρ : Vec Carrier n)
              → ⟦ ⊠-match a ord xs ys ⟧ Ρ
              ≈ ⅀⟦ xs ⟧ (drop-1 i<n Ρ) * ⅀⟦ ys ⟧ (drop-1 j<n Ρ)
  ⊠-match-hom {j = j} (acc wf) (inj-lt i≤j-1 j≤n) xs ys Ρ′ =
    let (ρ , Ρ) = drop-1 j≤n Ρ′
        xs′ = ⅀⟦ xs ⟧ (drop-1 (≤′-trans (≤′-step i≤j-1) j≤n) Ρ′)
    in
    begin
      ⟦ poly-map ( (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs)) ys ⊐↓ j≤n ⟧ Ρ′
    ≈⟨ ⊐↓-hom (poly-map ( (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs)) ys) j≤n Ρ′ ⟩
      ⅀?⟦ poly-map ( (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs)) ys ⟧ (ρ , Ρ)
    ≈⟨ poly-mapR ρ Ρ (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs)
                     (_ *_)
                     (*-cong refl)
                     reassoc
                     (distribˡ _)
                     (λ y → ⊠-⅀-inj-hom (wf _ j≤n) i≤j-1 xs y _)
                     (zeroʳ _) ys ⟩
       ⅀⟦ xs ⟧ (drop-1 i≤j-1 Ρ) * ⅀⟦ ys ⟧ (ρ , Ρ)
    ≈⟨ ≪* trans-join-coeffs-hom i≤j-1 j≤n xs Ρ′ ⟩
      xs′ * ⅀⟦ ys ⟧ (ρ , Ρ)
    ∎
  ⊠-match-hom (acc wf) (inj-gt i≤n j≤i-1) xs ys Ρ′ =
    let (ρ , Ρ) = drop-1 i≤n Ρ′
        ys′ = ⅀⟦ ys ⟧ (drop-1 (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n) Ρ′)
    in
    begin
      ⟦ poly-map ( (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys)) xs ⊐↓ i≤n ⟧ Ρ′
    ≈⟨ ⊐↓-hom (poly-map ( (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys)) xs) i≤n Ρ′ ⟩
      ⅀?⟦ poly-map ( (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys)) xs ⟧ (ρ , Ρ)
    ≈⟨ poly-mapR ρ Ρ (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys)
                     (_ *_)
                     (*-cong refl)
                     reassoc
                     (distribˡ _)
                     (λ x → ⊠-⅀-inj-hom (wf _ i≤n) j≤i-1 ys x _)
                     (zeroʳ _) xs ⟩
      ⅀⟦ ys ⟧ (drop-1 j≤i-1 Ρ) * ⅀⟦ xs ⟧ (ρ , Ρ)
    ≈⟨ ≪* trans-join-coeffs-hom j≤i-1 i≤n ys Ρ′ ⟩
      ys′ * ⅀⟦ xs ⟧ (ρ , Ρ)
    ≈⟨ *-comm ys′ _ ⟩
      ⅀⟦ xs ⟧ (ρ , Ρ) * ys′
    ∎
  ⊠-match-hom (acc wf) (inj-eq ij≤n) xs ys Ρ =
    begin
      ⟦ ⊠-coeffs (wf _ ij≤n) xs ys ⊐↓ ij≤n ⟧ Ρ
    ≈⟨ ⊐↓-hom (⊠-coeffs (wf _ ij≤n) xs ys) ij≤n Ρ ⟩
      ⅀?⟦ ⊠-coeffs (wf _ ij≤n) xs ys ⟧ (drop-1 ij≤n Ρ)
    ≈⟨ ⊠-coeffs-hom (wf _ ij≤n) xs ys (drop-1 ij≤n Ρ) ⟩
      ⅀⟦ xs ⟧ (drop-1 ij≤n Ρ) * ⅀⟦ ys ⟧ (drop-1 ij≤n Ρ)
    ∎

  ⊠-coeffs-hom : ∀ {n}
               → (a : Acc _<′_ n)
               → (xs ys : Coeff n +)
               → ∀ ρ → ⅀?⟦ ⊠-coeffs a xs ys ⟧ ρ ≈ ⅀⟦ xs ⟧ ρ * ⅀⟦ ys ⟧ ρ
  ⊠-coeffs-hom a xs (y ≠0 Δ j & []) (ρ , Ρ) =
    begin
      ⅀?⟦ poly-map (⊠-step′ a y) xs ⍓* j ⟧ (ρ , Ρ)
    ≈⟨ sym (pow′-hom j (poly-map (⊠-step′ a y) xs) ρ Ρ) ⟩
      ⅀?⟦ poly-map (⊠-step′ a y) xs ⟧ (ρ , Ρ) *⟨ ρ ⟩^ j
    ≈⟨ pow-mul-cong (poly-mapR ρ Ρ (⊠-step′ a y) (⟦ y ⟧ Ρ *_) (*-cong refl) reassoc (distribˡ _) (λ z → ⊠-step′-hom a y z Ρ) (zeroʳ _) xs) ρ j ⟩
      (⟦ y ⟧ Ρ * ⅀⟦ xs ⟧ (ρ , Ρ)) *⟨ ρ ⟩^ j
    ≈⟨ pow-opt _ ρ j ⟩
      (ρ ^ j) * (⟦ y ⟧ Ρ * ⅀⟦ xs ⟧ (ρ , Ρ))
    ≈⟨ sym (*-assoc _ _ _) ⟩
      (ρ ^ j) * ⟦ y ⟧ Ρ * ⅀⟦ xs ⟧ (ρ , Ρ)
    ≈⟨ *-comm _ _ ⟩
      ⅀⟦ xs ⟧ (ρ , Ρ) * ((ρ ^ j) * ⟦ y ⟧ Ρ)
    ≈⟨ *≫ sym (pow-opt _ ρ j) ⟩
      ⅀⟦ xs ⟧ (ρ , Ρ) * (⟦ y ⟧ Ρ *⟨ ρ ⟩^ j)
    ∎
  ⊠-coeffs-hom a xs (y ≠0 Δ j & ∹ ys) (ρ , Ρ) =
    let xs′ = ⅀⟦ xs ⟧ (ρ , Ρ)
        y′  = ⟦ y ⟧ Ρ
        ys′ = ⅀⟦ ys ⟧ (ρ , Ρ)
    in
    begin
      ⅀?⟦ para (⊠-cons a y ys) xs ⍓* j ⟧ (ρ , Ρ)
    ≈⟨ sym (pow′-hom j (para (⊠-cons a y ys) xs) ρ Ρ) ⟨ trans ⟩ pow-opt _ ρ j ⟩
      ρ ^ j * ⅀?⟦ para (⊠-cons a y ys) xs ⟧ (ρ , Ρ)
    ≈⟨ *≫ ⊠-cons-hom a y ys xs ρ Ρ ⟩
     ρ ^ j * (xs′ * (ρ * ys′ + y′))
    ≈⟨ sym (*-assoc _ _ _) ⟨ trans ⟩ (≪* *-comm _ _) ⟨ trans ⟩ *-assoc _ _ _ ⟨ trans ⟩ (*≫ sym (pow-opt _ ρ j))⟩
      xs′ * ((ρ * ys′ + y′) *⟨ ρ ⟩^ j)
    ∎

  ⊠-cons-hom : ∀ {n}
             → (a : Acc _<′_ n)
             → (y : Poly n)
             → (ys xs : Coeff n +)
             → (ρ : Carrier)
             → (Ρ : Vec Carrier n)
             → ⅀?⟦ para (⊠-cons a y ys) xs ⟧ (ρ , Ρ)
             ≈ ⅀⟦ xs ⟧ (ρ , Ρ) * (ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + ⟦ y ⟧ Ρ)
  -- ⊠-cons-hom a y [] xs ρ Ρ = {!!}
  ⊠-cons-hom a y ys xs ρ Ρ = poly-foldR ρ Ρ (⊠-cons a y ys) (flip _*_ (ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + ⟦ y ⟧ Ρ)) (flip *-cong refl) (λ x y → sym (*-assoc x y _)) step (zeroˡ _) xs
    where
    step = λ { (z ⊐ j≤n) {ys₁} zs ys≋zs →
      let x′  = ⟦ z ⊐ j≤n ⟧ Ρ
          xs′ = ⅀?⟦ zs ⟧ (ρ , Ρ)
          y′  = ⟦ y ⟧ Ρ
          ys′ = ⅀⟦ ys ⟧ (ρ , Ρ)
          step = λ y → ⊠-step-hom a z j≤n y Ρ
      in
      begin
        ρ * ⅀?⟦ ⊞-coeffs (poly-map ( (⊠-step a z j≤n)) ys) ys₁ ⟧ (ρ , Ρ) + ⟦ ⊠-step a z j≤n y ⟧ Ρ
      ≈⟨ (*≫ ⊞-coeffs-hom (poly-map (⊠-step a z j≤n) ys) _ (ρ , Ρ)) ⟨ +-cong ⟩ ⊠-step-hom a z j≤n y Ρ ⟩
        ρ * (⅀?⟦ poly-map (⊠-step a z j≤n) ys ⟧ (ρ , Ρ) + ⅀?⟦ ys₁ ⟧ (ρ , Ρ)) + x′ * y′
      ≈⟨ ≪+ *≫ (poly-mapR ρ Ρ (⊠-step a z j≤n) (x′ *_) (*-cong refl) reassoc (distribˡ _) step (zeroʳ _) ys ⟨ +-cong ⟩ ys≋zs) ⟩
        ρ * (x′ * ys′ + xs′ * (ρ * ys′ + y′)) + (x′ * y′)
      ≈⟨ ≪+ distribˡ _ _ _ ⟩
        ρ * (x′ * ys′) + ρ * (xs′ * (ρ * ys′ + y′)) + (x′ * y′)
      ≈⟨ (≪+ +-comm _ _) ⟨ trans ⟩ +-assoc _ _ _ ⟩
        ρ * (xs′ * (ρ * ys′ + y′)) + (ρ * (x′ * ys′) + (x′ * y′))
      ≈⟨ sym (*-assoc _ _ _) ⟨ +-cong ⟩ ((≪+ (sym (*-assoc _ _ _) ⟨ trans ⟩ (≪* *-comm _ _) ⟨ trans ⟩ *-assoc _ _ _)) ⟨ trans ⟩ sym (distribˡ _ _ _)) ⟩
        ρ * xs′ * (ρ * ys′ + y′) + x′ * (ρ * ys′ + y′)
      ≈⟨ sym (distribʳ _ _ _) ⟩
        (ρ * xs′ + x′) * (ρ * ys′ + y′)
      ∎ }

⊠-hom : ∀ {n} (xs ys : Poly n) →
        ∀ ρ → ⟦ xs ⊠ ys ⟧ ρ ≈ ⟦ xs ⟧ ρ * ⟦ ys ⟧ ρ
⊠-hom (xs ⊐ i≤n) = ⊠-step-hom (<′-wellFounded _) xs i≤n


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the heterogeneous suffix relation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Suffix.Heterogeneous.Properties where

open import Data.List as List
  using (List; []; _∷_; _++_; length; filter; replicate; reverse; reverseAcc)
open import Data.List.Relation.Binary.Pointwise as Pw
  using (Pointwise; []; _∷_; Pointwise-length)
open import Data.List.Relation.Binary.Suffix.Heterogeneous as Suffix
  using (Suffix; here; there; tail)
open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix
  using (Prefix)
open import Data.Nat
open import Data.Nat.Properties
open import Function using (_$_; flip)
open import Relation.Nullary using (Dec; yes; no; ¬_)
import Relation.Nullary.Decidable as Dec
open import Relation.Unary as U using (Pred)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary as B
  using (REL; Rel; Trans; Antisym; Irrelevant; _⇒_)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; sym; subst; subst₂)

import Data.List.Properties as Listₚ
import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefixₚ

------------------------------------------------------------------------
-- Suffix and Prefix are linked via reverse

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  fromPrefix : ∀ {as bs} → Prefix R as bs →
               Suffix R (reverse as) (reverse bs)
  fromPrefix {as} {bs} p with Prefix.toView p
  ... | Prefix._++_ {cs} rs ds =
    subst (Suffix R (reverse as))
      (sym (Listₚ.reverse-++-commute cs ds))
      (Suffix.fromView (reverse ds Suffix.++ Pw.reverse⁺ rs))

  fromPrefix-rev : ∀ {as bs} → Prefix R (reverse as) (reverse bs) →
                   Suffix R as bs
  fromPrefix-rev pre =
    subst₂ (Suffix R)
      (Listₚ.reverse-involutive _)
      (Listₚ.reverse-involutive _)
      (fromPrefix pre)

  toPrefix-rev : ∀ {as bs} → Suffix R as bs →
                 Prefix R (reverse as) (reverse bs)
  toPrefix-rev {as} {bs} s with Suffix.toView s
  ... | Suffix._++_ cs {ds} rs =
    subst (Prefix R (reverse as))
      (sym (Listₚ.reverse-++-commute cs ds))
      (Prefix.fromView (Pw.reverse⁺ rs Prefix.++ reverse cs))

  toPrefix : ∀ {as bs} → Suffix R (reverse as) (reverse bs) →
             Prefix R as bs
  toPrefix suf =
    subst₂ (Prefix R)
      (Listₚ.reverse-involutive _)
      (Listₚ.reverse-involutive _)
      (toPrefix-rev suf)

------------------------------------------------------------------------
-- length

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  length-mono : ∀ {as bs} → Suffix R as bs → length as ≤ length bs
  length-mono (here rs)   = ≤-reflexive (Pointwise-length rs)
  length-mono (there suf) = ≤-step (length-mono suf)

  S[as][bs]⇒∣as∣≢1+∣bs∣ : ∀ {as bs} → Suffix R as bs →
                          length as ≢ suc (length bs)
  S[as][bs]⇒∣as∣≢1+∣bs∣ suf eq = <⇒≱ (≤-reflexive (sym eq)) (length-mono suf)

------------------------------------------------------------------------
-- Pointwise conversion

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  fromPointwise : Pointwise R ⇒ Suffix R
  fromPointwise = here

  toPointwise : ∀ {as bs} → length as ≡ length bs →
                Suffix R as bs → Pointwise R as bs
  toPointwise eq (here rs)   = rs
  toPointwise eq (there suf) = contradiction eq (S[as][bs]⇒∣as∣≢1+∣bs∣ suf)

------------------------------------------------------------------------
-- Suffix as a partial order

module _ {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
         {R : REL A B r} {S : REL B C s} {T : REL A C t} where

  trans : Trans R S T → Trans (Suffix R) (Suffix S) (Suffix T)
  trans rs⇒t (here rs)    (here ss)       = here (Pw.transitive rs⇒t rs ss)
  trans rs⇒t (here rs)    (there ssuf)    = there (trans rs⇒t (here rs) ssuf)
  trans rs⇒t (there rsuf) ssuf            = trans rs⇒t rsuf (tail ssuf)

module _ {a b e r s} {A : Set a} {B : Set b}
         {R : REL A B r} {S : REL B A s} {E : REL A B e} where

  antisym : Antisym R S E → Antisym (Suffix R) (Suffix S) (Pointwise E)
  antisym rs⇒e rsuf ssuf = Pw.antisymmetric
    rs⇒e
    (toPointwise eq rsuf)
    (toPointwise (sym eq) ssuf)
    where eq = ≤-antisym (length-mono rsuf) (length-mono ssuf)

------------------------------------------------------------------------
-- _++_

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  ++⁺ : ∀ {as bs cs ds} → Suffix R as bs → Pointwise R cs ds →
        Suffix R (as ++ cs) (bs ++ ds)
  ++⁺ (here rs)   rs′ = here (Pw.++⁺ rs rs′)
  ++⁺ (there suf) rs′ = there (++⁺ suf rs′)

  ++⁻ : ∀ {as bs cs ds} → length cs ≡ length ds →
        Suffix R (as ++ cs) (bs ++ ds) → Pointwise R cs ds
  ++⁻ {_ ∷ _} {_}      {_}  {_}  eq suf         = ++⁻ eq (tail suf)
  ++⁻ {[]}    {[]}     {_}  {_}  eq suf         = toPointwise eq suf
  ++⁻ {[]}    {b ∷ bs} {_}  {_}  eq (there suf) = ++⁻ eq suf
  ++⁻ {[]}    {b ∷ bs} {cs} {ds} eq (here  rs)  = contradiction (sym eq) (<⇒≢ ds<cs)
    where
    open ≤-Reasoning
    ds<cs : length ds < length cs
    ds<cs = begin
      suc (length ds)             ≤⟨ s≤s (n≤m+n (length bs) (length ds)) ⟩
      suc (length bs + length ds) ≡⟨ sym $ Listₚ.length-++ (b ∷ bs) ⟩
      length (b ∷ bs ++ ds)       ≡⟨ sym $ Pointwise-length rs ⟩
      length cs                   ∎

------------------------------------------------------------------------
-- map

module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
         {R : REL C D r} where

  map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
         Suffix (λ a b → R (f a) (g b)) as bs →
         Suffix R (List.map f as) (List.map g bs)
  map⁺ f g (here rs)   = here (Pw.map⁺ f g rs)
  map⁺ f g (there suf) = there (map⁺ f g suf)

  map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
         Suffix R (List.map f as) (List.map g bs) →
         Suffix (λ a b → R (f a) (g b)) as bs
  map⁻ {as} {b ∷ bs} f g (here rs) = here (Pw.map⁻ f g rs)
  map⁻ {as} {b ∷ bs} f g (there suf) = there (map⁻ f g suf)
  map⁻ {x ∷ as} {[]} f g suf with length-mono suf
  ... | ()
  map⁻ {[]} {[]} f g suf = here []

------------------------------------------------------------------------
-- filter

module _ {a b r p q} {A : Set a} {B : Set b} {R : REL A B r}
         {P : Pred A p} {Q : Pred B q}
         (P? : U.Decidable P) (Q? : U.Decidable Q)
         (P⇒Q : ∀ {a b} → R a b → P a → Q b)
         (Q⇒P : ∀ {a b} → R a b → Q b → P a)
         where

  filter⁺ : ∀ {as bs} → Suffix R as bs →
            Suffix R (filter P? as) (filter Q? bs)
  filter⁺ (here rs) = here (Pw.filter⁺ P? Q? P⇒Q Q⇒P rs)
  filter⁺ (there {a} suf) with Q? a
  ... | yes q = there (filter⁺ suf)
  ... | no ¬q = filter⁺ suf

------------------------------------------------------------------------
-- replicate

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  replicate⁺ : ∀ {m n a b} → m ≤ n → R a b →
               Suffix R (replicate m a) (replicate n b)
  replicate⁺ {a = a} {b = b} m≤n r = repl (≤⇒≤′ m≤n)
    where
    repl : ∀ {m n} → m ≤′ n → Suffix R (replicate m a) (replicate n b)
    repl ≤′-refl       = here (Pw.replicate⁺ r _)
    repl (≤′-step m≤n) = there (repl m≤n)

------------------------------------------------------------------------
-- Irrelevant

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  irrelevant : Irrelevant R → Irrelevant (Suffix R)
  irrelevant irr (here  rs)   (here  rs₁)   = P.cong here $ Pw.irrelevant irr rs rs₁
  irrelevant irr (here  rs)   (there rsuf)  = contradiction (Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf)
  irrelevant irr (there rsuf) (here  rs)    = contradiction (Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf)
  irrelevant irr (there rsuf) (there rsuf₁) = P.cong there $ irrelevant irr rsuf rsuf₁

------------------------------------------------------------------------
-- Decidability

  suffix? : B.Decidable R → B.Decidable (Suffix R)
  suffix? R? as bs = Dec.map′ fromPrefix-rev toPrefix-rev
                   $ Prefixₚ.prefix? R? (reverse as) (reverse bs)


text:
{-# OPTIONS --universe-polymorphism #-}

{- This module is really a combination of copumpkin's Semigroup and
   CommutativeSemigroup modules, available on github at
   https://github.com/copumpkin/containers.git
-}
module Permutations where

open import Algebra
-- import Algebra.FunctionProperties as FunctionProperties

open import Data.Empty
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product
open import Data.Nat hiding (fold)
open import Data.Nat.Properties using (commutativeSemiring; i+j≡0⇒i≡0)
open import Data.Fin using (Fin; zero; suc; toℕ)
open import Data.Vec

open import Relation.Binary
open import Relation.Binary.PropositionalEquality renaming (setoid to ≡-setoid)
import Relation.Binary.EqReasoning as EqReasoning

open CommutativeSemiring commutativeSemiring using (+-identity; +-comm; distrib)
-- open import Containers.Semigroup

-- Full trees, representing associations
data Association : ℕ → Set where
  leaf : Association 1
  node : ∀ {m n} →
        (l : Association m) → (r : Association n) → Association (m + n)

leftA : ∀ {n} → Association (1 + n)
leftA {zero} = leaf
leftA {suc n} rewrite +-comm 1 n = node (leftA {n}) leaf

rightA : ∀ {n} → Association (1 + n)
rightA {zero} = leaf
rightA {suc n} = node leaf rightA

fold : ∀ {n} {a} {A : Set a} → Association n → (A → A → A) → Vec A n → A
fold leaf _∙_ (x ∷ xs) = x
fold (node {m} l r) _∙_ xs with splitAt m xs
...                        | ls , rs , pf = fold l _∙_ ls ∙ fold r _∙_ rs

foldl₁-fold : ∀ {n} {a} {A : Set a} (f : A → A → A) →
             (xs : Vec A (1 + n)) → foldl₁ f xs ≡ fold leftA f xs
foldl₁-fold {zero} f (x ∷ []) = refl
foldl₁-fold {suc n} f xs rewrite +-comm 1 n with splitAt (suc n) xs
foldl₁-fold {suc n} f .(ls ++ r ∷ []) | ls , r ∷ [] , refl
  rewrite sym (foldl₁-fold f ls) = foldl₁-snoc f r ls
  where
  foldl₁-snoc : ∀ {a} {A : Set a} {n} f x (xs : Vec A (1 + n)) →
                foldl₁ f (xs ++ x ∷ []) ≡ f (foldl₁ f xs) x
  foldl₁-snoc f x₀ (x₁ ∷ []) = refl
  foldl₁-snoc f x₀ (x₁ ∷ x ∷ xs) = foldl₁-snoc f x₀ (f x₁ x ∷ xs)

foldr-fold : ∀ {n} {a} {A : Set a} (f : A → A → A) z (xs : Vec A n) →
             foldr _ f z xs ≡ fold rightA f (xs ∷ʳ z)
foldr-fold f z [] = refl
foldr-fold f z (x ∷ xs) = cong (f x) (foldr-fold f z xs)

foldl-fold : ∀ {n} {a} {A : Set a} (f : A → A → A) z (xs : Vec A n) →
             foldl _ f z xs ≡ fold leftA f (z ∷ xs)
foldl-fold f z xs rewrite sym (foldl₁-fold f (z ∷ xs)) = refl

foldl-elim : ∀ {a b c} {A : Set a} {B : ℕ → Set b}
             (P : ∀ {n} → Vec A n → B n → Set c)
             {f : ∀ {n} → B n → A → B (1 + n)} {z : B 0}
           → P [] z
           → (∀ {n x′ z′} {xs′ : Vec A n} → P xs′ z′ → P (xs′ ∷ʳ x′) (f z′ x′))
           → ∀ {n} (xs : Vec A n) → P xs (foldl B f z xs)
foldl-elim P Pz Ps [] = Pz
foldl-elim {A} {B} P {f} {z} Pz Ps (x ∷ xs) =
  foldl-elim (λ xs′ → P (x ∷ xs′)) (Ps Pz) Ps xs

foldl-lemma : ∀ {a b} {A : Set a} {B : ℕ → Set b}
  {f : ∀ {n} → B n → A → B (suc n)} {z : B 0} {n} {x} (xs : Vec A n) →
  f (foldl B f z xs) x ≡ foldl B f z (xs ∷ʳ x)
foldl-lemma [] = refl
foldl-lemma {B = B} (y ∷ ys) = foldl-lemma {B = λ n → B (suc n)} ys

infixr 5 _∷_

data Permutation : ℕ → Set where
  []  : Permutation 0
  _∷_ : {n : ℕ} → (p : Fin (1 + n)) → (ps : Permutation n) → Permutation (1 + n)

max : ∀ {n} → Fin (suc n)
max {zero} = zero
max {suc n} = suc max

idP : ∀ {n} → Permutation n
idP {zero} = []
idP {suc n} = zero ∷ idP

reverseP : ∀ {n} → Permutation n
reverseP {zero} = []
reverseP {suc n} = max ∷ reverseP

insert : ∀ {n} {a} {A : Set a} → Vec A n → Fin (1 + n) → A → Vec A (1 + n)
insert xs zero a = a ∷ xs
insert [] (suc ()) a
insert (x ∷ xs) (suc i) a = x ∷ insert xs i a

permute : ∀ {n} {a} {A : Set a} → Permutation n → Vec A n → Vec A n
permute [] [] = []
permute (p ∷ ps) (x ∷ xs) = insert (permute ps xs) p x

idP-id : ∀ {n} {a} {A : Set a} (xs : Vec A n) → permute idP xs ≡ xs
idP-id [] = refl
idP-id (x ∷ xs) = cong (_∷_ x) (idP-id xs)

insert-max : ∀ {n} {a} {A : Set a} (ys : Vec A n) x → insert ys max x ≡ ys ∷ʳ x
insert-max [] x = refl
insert-max (y ∷ ys) x = cong (_∷_ y) (insert-max ys x)

reverse-∷ʳ : ∀ {n} {a} {A : Set a} (ys : Vec A n) x →
  reverse ys ∷ʳ x ≡ reverse (x ∷ ys)
reverse-∷ʳ {A = A} xs x =
  foldl-elim
    (λ xs b → b ∷ʳ x ≡ reverse (x ∷ xs))
    refl
    (λ {_} {_} {_} {xs} eq →
      trans (cong (_∷_ _) eq) (foldl-lemma {B = λ n -> Vec A (suc n)} xs))
    xs

reverseP-reverse : ∀ {n} {a} {A : Set a} (xs : Vec A n) →
  permute reverseP xs ≡ reverse xs
reverseP-reverse [] = refl
reverseP-reverse {suc n} {_} {A} (x ∷ xs) =
    begin
      insert (permute reverseP xs) max x
    ≈⟨ insert-max (permute reverseP xs) x ⟩
      permute reverseP xs ∷ʳ x
    ≈⟨ cong (λ q → q ∷ʳ x) (reverseP-reverse xs) ⟩
      reverse xs ∷ʳ x
    ≈⟨ reverse-∷ʳ xs x ⟩
      reverse (x ∷ xs)
    ∎
  where open EqReasoning (≡-setoid (Vec A (1 + n)))

remove : {n : ℕ} → {A : Set} → (i : Fin (suc n)) → Vec A (suc n) → Vec A n
remove {n} zero (x ∷ v) = v
remove {zero} (suc ()) _
remove {suc n} (suc i) (x ∷ v) = x ∷ remove i v

remove0 : {n : ℕ} {A : Set} → (v : Vec A (suc n)) →
  v ≡ (lookup zero v) ∷ remove zero v
remove0 (x ∷ v) = refl

{-
_◌_ : ∀ {n} → Permutation n → Permutation n → Permutation n
[] ◌ [] = []
(zero ∷ p₁) ◌ (q ∷ q₁) = q ∷ (p₁ ◌ q₁)
(suc p ∷ p₁) ◌ (zero ∷ q₁) = {!!}
(suc p ∷ p₁) ◌ (suc q ∷ q₁) = {!!}

perm◌perm : ∀ {n} {A : Set} → (p q : Permutation n) → (v : Vec A n) → permute q (permute p v) ≡ permute (p ◌ q) v
perm◌perm [] [] [] = refl
perm◌perm (zero ∷ p₁) (q ∷ q₁) (x ∷ v) = cong (λ y → insert y q x) (perm◌perm p₁ q₁ v)
perm◌perm (suc p ∷ p₁) (q ∷ q₁) (x ∷ v) with permute ((suc p) ∷ p₁) (x ∷ v)
perm◌perm (suc p ∷ p₁) (zero ∷ q₁) (x ∷ v) | y ∷ w = {!!}
perm◌perm (suc p ∷ p₁) (suc q ∷ q₁) (x ∷ v) | y ∷ w = {!!}

p1 : Permutation 5
p1 =  suc (suc zero) ∷ suc (suc zero)  ∷ zero ∷ suc zero ∷ zero ∷ []

p2 : Permutation 5
p2 = suc (suc (suc zero)) ∷ suc (suc (suc zero)) ∷ zero ∷ zero ∷ zero ∷ []

p3 : Permutation 5
p3 = suc (suc (suc (suc zero))) ∷ suc zero ∷ suc zero ∷ suc zero ∷ zero ∷ []

test1 : Vec (Fin 5) 5
test1 = permute p1 (tabulate {5} (λ x → x))

test2 : Vec (Fin 5 ) 5
test2 = permute p2 (tabulate (λ x → x))

test3 : Vec (Fin 5) 5
test3 = permute p1 (test2)

test4 : test3 ≡ permute p3 (tabulate (λ x → x))
test4 = refl
-}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual