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

module AgdaFeatureNeedHiddenVariableTypeConstructorWrapper where

Unwrapped : {A : Set} → (A → Set) → Set₁
Unwrapped B = ∀ {x} → B x → Set

record Unindexed : Set₁ where
  field
    {A} : Set
    {B} : A → Set
    unwrap : Unwrapped B

record Indexed {A : Set} (B : A → Set) : Set₁ where
  field
    unwrap : Unwrapped B

record Generic (A : Set₁) : Set₁ where
  field
    unwrap : A

record Foo (F : Set₁) : Set₁ where
  field
    foo : F → Set

open Foo {{...}}

postulate
  A : Set
  B : A → Set
  unwrapped : Unwrapped B
  indexed : Indexed B
  unindexed : Unindexed
  generic : Generic (Unwrapped B)

postulate

  instance FooUnwrapped : Foo (Unwrapped B)
  instance FooIndexed : Foo (Indexed B)
  instance FooUnindexed : Foo Unindexed
  instance FooGeneric : Foo (Generic (Unwrapped B))

test-unwrapped-lambda-unhide-works : Set
test-unwrapped-lambda-unhide-works = foo (λ {_} → unwrapped)

test-unwrapped-help-instance-works : Set
test-unwrapped-help-instance-works = foo {F = ∀ {_} → _} unwrapped

test-unindexed-works : Set
test-unindexed-works = foo unindexed

test-indexed-works : Set
test-indexed-works = foo indexed

test-generic-works : Set
test-generic-works = foo generic

test-unwrapped-fails : Set
test-unwrapped-fails = {!foo unwrapped!}
{-
No instance of type Foo (B _x_48 → Set) was found in scope.
when checking that unwrapped is a valid argument to a function of
type {F : Set₁} {{r : Foo F}} → F → Set
-}

-- tests for unwrapping

unwrap-test-generic : Unwrapped B
unwrap-test-generic = let instance _ = generic in let open Generic ⦃ … ⦄ in unwrap {A = Unwrapped _}

unwrap-test-index : Unwrapped B
unwrap-test-index = let instance _ = indexed in let open Indexed ⦃ … ⦄ in unwrap


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------

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

module Relation.Binary.Indexed.Heterogeneous where

open import Function
open import Level using (suc; _⊔_)
open import Relation.Binary using (_⇒_)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)

------------------------------------------------------------------------
-- Publically export core definitions

open import Relation.Binary.Indexed.Heterogeneous.Core public

------------------------------------------------------------------------
-- Equivalences

record IsIndexedEquivalence {i a ℓ} {I : Set i} (A : I → Set a)
                            (_≈_ : IRel A ℓ) : Set (i ⊔ a ⊔ ℓ) where
  field
    refl  : Reflexive  A _≈_
    sym   : Symmetric  A _≈_
    trans : Transitive A _≈_

  reflexive : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈_ {i}
  reflexive P.refl = refl

record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : I → Set c
    _≈_           : IRel Carrier ℓ
    isEquivalence : IsIndexedEquivalence Carrier _≈_

  open IsIndexedEquivalence isEquivalence public

------------------------------------------------------------------------
-- Preorders

record IsIndexedPreorder {i a ℓ₁ ℓ₂} {I : Set i} (A : I → Set a)
                         (_≈_ : IRel A ℓ₁) (_∼_ : IRel A ℓ₂) :
                         Set (i ⊔ a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isEquivalence : IsIndexedEquivalence A _≈_
    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _∼_
    trans         : Transitive A _∼_

  module Eq = IsIndexedEquivalence isEquivalence

  refl : Reflexive A _∼_
  refl = reflexive Eq.refl

record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
                       Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _∼_
  field
    Carrier    : I → Set c
    _≈_        : IRel Carrier ℓ₁  -- The underlying equality.
    _∼_        : IRel Carrier ℓ₂  -- The relation.
    isPreorder : IsIndexedPreorder Carrier _≈_ _∼_

  open IsIndexedPreorder isPreorder public

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.17

REL = IREL
{-# WARNING_ON_USAGE REL
"Warning: REL was deprecated in v0.17.
Please use IREL instead."
#-}
Rel = IRel
{-# WARNING_ON_USAGE Rel
"Warning: Rel was deprecated in v0.17.
Please use IRel instead."
#-}
Setoid = IndexedSetoid
{-# WARNING_ON_USAGE Setoid
"Warning: Setoid was deprecated in v0.17.
Please use IndexedSetoid instead."
#-}
IsEquivalence = IsIndexedEquivalence
{-# WARNING_ON_USAGE IsEquivalence
"Warning: IsEquivalence was deprecated in v0.17.
Please use IsIndexedEquivalence instead."
#-}

ext: agda


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

-- From the technical manual of TPTP
-- (http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml)

-- ... variables start with upper case letters, ... predicates and
-- functors either start with lower case and contain alphanumerics and
-- underscore ...

module Issue1.Functions where

postulate
  D : Set
  NAME : D → Set
  nAME : D → Set

postulate foo : ∀ a → NAME a
{-# ATP axiom foo #-}

-- This conjecture should not be proved.
postulate bar : ∀ a → nAME a
{-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
open import Agda.Builtin.Maybe
open import Agda.Builtin.Char
open import Agda.Builtin.String
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

_ : primStringUncons "abcd" ≡ just ('a', "bcd")
_ = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --rewriting --confluence-check #-}
module Issue4333.N1 where

open import Issue4333.M
{-# REWRITE p₁ #-}

b₁' : B a₁'
b₁' = b

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.UnivariateList.Poly1-1Poly where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec renaming ( [] to <> ; _∷_ to _::_)
open import Cubical.Data.Vec.OperationsNat

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Polynomials.UnivariateList.Base renaming (Poly to Poly:)
open import Cubical.Algebra.Polynomials.UnivariateList.Properties
open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyList
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly

private variable
  ℓ : Level

module Equiv-Poly1-Poly:
  (Acr@(A , Astr) : CommRing ℓ) where

  private
    PA = PolyCommRing Acr 1
    PAstr = snd PA
    PA: = UnivariatePolyList Acr
    PA:str = snd PA:

  open PolyMod Acr using (ElimProp)
  open PolyModTheory Acr
    using ( prod-Xn ; prod-Xn-sum ; prod-Xn-∷ ; prod-Xn-prod)
    renaming
    (prod-Xn-0P to prod-Xn-0P:)

  open CommRingStr
  open RingTheory

-- Notation P, Q, R... for Poly 1
-- x, y, w... for Poly:
-- a,b,c... for A

-----------------------------------------------------------------------------
-- direct

  trad-base : (v : Vec ℕ 1) → A → Poly: Acr
  trad-base (n :: <>) a = prod-Xn n (a ∷ [])

  trad-base-neutral : (v : Vec ℕ 1) → trad-base v (0r Astr) ≡ []
  trad-base-neutral (n :: <>) = cong (prod-Xn n) drop0 ∙ prod-Xn-0P: n

  trad-base-add : (v : Vec ℕ 1) → (a b : A) → _+_ PA:str (trad-base v a) (trad-base v b) ≡ trad-base v (_+_ Astr a b)
  trad-base-add (n :: <>) a b = prod-Xn-sum n (a ∷ []) (b ∷ [])

  Poly1→Poly: : Poly Acr 1 → Poly: Acr
  Poly1→Poly: = DS-Rec-Set.f _ _ _ _ (is-set PA:str)
                 []
                 trad-base
                 (_+_ PA:str)
                 (+Assoc PA:str)
                 (+IdR PA:str)
                 (+Comm PA:str)
                 trad-base-neutral
                 trad-base-add

  Poly1→Poly:-pres+ : (P Q : Poly Acr 1) → Poly1→Poly: (_+_ PAstr P Q) ≡ _+_ PA:str (Poly1→Poly: P) (Poly1→Poly: Q)
  Poly1→Poly:-pres+ P Q = refl

-----------------------------------------------------------------------------
-- converse

  Poly:→Poly1-int : (n : ℕ) → Poly: Acr → Poly Acr 1
  Poly:→Poly1-int n [] = 0r PAstr
  Poly:→Poly1-int n (a ∷ x) = _+_ PAstr (base (n :: <>) a) (Poly:→Poly1-int (suc n) x)
  Poly:→Poly1-int n (drop0 i) = ((cong (λ X → _+_ PAstr X (0r PAstr)) (base-neutral (n :: <>))) ∙ (+IdR PAstr _)) i

  Poly:→Poly1 : Poly: Acr → Poly Acr 1
  Poly:→Poly1 x = Poly:→Poly1-int 0 x

  Poly:→Poly1-int-pres+ : (x y : Poly: Acr) → (n : ℕ) →
                              Poly:→Poly1-int n (_+_ PA:str x y) ≡ _+_ PAstr (Poly:→Poly1-int n x) (Poly:→Poly1-int n y)
  Poly:→Poly1-int-pres+ = ElimProp _
                           (λ y n → cong (Poly:→Poly1-int n) (+IdL PA:str y) ∙ sym (+IdL PAstr _))
                           (λ a x ind-x → ElimProp _
                                           (λ n → sym (+IdR PAstr (Poly:→Poly1-int n (a ∷ x))))
                                           (λ b y ind-y n → sym (+ShufflePairs (CommRing→Ring PA) _ _ _ _
                                                                ∙ cong₂ (_+_ PAstr) (base-add _ _ _) (sym (ind-x y (suc n)))))
                                           (isPropΠ (λ _ → is-set PAstr _ _)))
                           (isPropΠ2 (λ _ _ → is-set PAstr _ _))

  Poly:→Poly1-pres+ : (x y : Poly: Acr) → Poly:→Poly1 (_+_ PA:str x y) ≡ _+_ PAstr (Poly:→Poly1 x) (Poly:→Poly1 y)
  Poly:→Poly1-pres+ x y = Poly:→Poly1-int-pres+ x y 0

-----------------------------------------------------------------------------
-- section

  e-sect-int : (x : Poly: Acr) → (n : ℕ) → Poly1→Poly: (Poly:→Poly1-int n x) ≡ prod-Xn n x
  e-sect-int = ElimProp _
               (λ n → sym (prod-Xn-0P: n))
               (λ a x ind-x n → cong (λ X → _+_ PA:str (prod-Xn n (a ∷ [])) X) (ind-x (suc n))
                                 ∙ prod-Xn-∷ n a x)
               (isPropΠ (λ _ → is-set PA:str _ _))

  e-sect : (x : Poly: Acr) → Poly1→Poly: (Poly:→Poly1 x) ≡ x
  e-sect x = e-sect-int x 0

-----------------------------------------------------------------------------
-- retraction

  idde : (m n : ℕ) → (a : A) → Poly:→Poly1-int n (prod-Xn m (a ∷ [])) ≡ base ((n +n m) :: <>) a
  idde zero n a = +IdR PAstr (base (n :: <>) a)
                  ∙ cong (λ X → base (X :: <>) a) (sym (+-zero n))
  idde (suc m) n a = cong (λ X → _+_ PAstr X (Poly:→Poly1-int (suc n) (prod-Xn m (a ∷ [])))) (base-neutral (n :: <>))
                     ∙ +IdL PAstr (Poly:→Poly1-int (suc n) (prod-Xn m (a ∷ [])))
                     ∙ idde m (suc n) a
                     ∙ cong (λ X → base (X :: <>) a) (sym (+-suc n m))

  idde-v : (v : Vec ℕ 1) → (a : A) → Poly:→Poly1-int 0 (trad-base v a) ≡ base v a
  idde-v (n :: <>) a = (idde n 0 a)

  e-retr : (P : Poly Acr 1) → Poly:→Poly1 (Poly1→Poly: P) ≡ P
  e-retr = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
           refl
           (λ v a → idde-v v a)
           λ {P Q} ind-P ind-Q → cong Poly:→Poly1 (Poly1→Poly:-pres+ P Q)
                                 ∙ Poly:→Poly1-pres+ (Poly1→Poly: P) (Poly1→Poly: Q)
                                 ∙ cong₂ (_+_ PAstr) ind-P ind-Q

-----------------------------------------------------------------------------
-- Ring morphism

  Poly1→Poly:-pres1 : Poly1→Poly: (1r PAstr) ≡ 1r PA:str
  Poly1→Poly:-pres1 = refl

  trad-base-prod : (v v' : Vec ℕ 1) → (a a' : A) → trad-base (v +n-vec v') (Astr ._·_ a a') ≡
                                                      _·_ PA:str (trad-base v a) (trad-base v' a')
  trad-base-prod (k :: <>) (l :: <>) a a' = sym ((prod-Xn-prod k l [ a ]  [ a' ]) ∙ cong (λ X → prod-Xn (k +n l) [ X ]) (+IdR Astr _))

  Poly1→Poly:-pres· : (P Q : Poly Acr 1) → Poly1→Poly: (_·_ PAstr P Q) ≡ _·_ PA:str (Poly1→Poly: P) (Poly1→Poly: Q)
  Poly1→Poly:-pres· = DS-Ind-Prop.f _ _ _ _ (λ _ → isPropΠ λ _ → is-set PA:str _ _)
                        (λ Q → refl)
                        (λ v a → DS-Ind-Prop.f _ _ _ _ (λ _ → is-set PA:str _ _)
                                  (sym (0RightAnnihilates (CommRing→Ring PA:) _))
                                  (λ v' a' → trad-base-prod v v' a a')
                                  λ {U V} ind-U ind-V → (cong₂ (_+_ PA:str) ind-U ind-V)
                                                          ∙ sym (·DistR+ PA:str _ _ _))
                        λ {U V} ind-U ind-V Q → (cong₂ (_+_ PA:str) (ind-U Q) (ind-V Q))
                                                 ∙ sym (·DistL+ PA:str _ _ _)

-----------------------------------------------------------------------------
-- Ring Equivalences

module _ (Acr : CommRing ℓ) where

  open Equiv-Poly1-Poly: Acr

  CRE-Poly1-Poly: : CommRingEquiv (PolyCommRing Acr 1) (UnivariatePolyList Acr)
  fst CRE-Poly1-Poly: = isoToEquiv is
    where
    is : Iso _ _
    Iso.fun is = Poly1→Poly:
    Iso.inv is = Poly:→Poly1
    Iso.rightInv is = e-sect
    Iso.leftInv is = e-retr
  snd CRE-Poly1-Poly: = makeIsRingHom
                        Poly1→Poly:-pres1
                        Poly1→Poly:-pres+
                        Poly1→Poly:-pres·

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------------
-- Testing the translation of universal quantified propositional functions
------------------------------------------------------------------------------

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

module PropositionalFunction where

postulate D : Set

postulate id₁ : {A : D → Set}{x : D} → A x → A x
{-# ATP prove id₁ #-}

postulate id₂ : {A : D → D → Set}{x y : D} → A x y → A x y
{-# ATP prove id₂ #-}


text:
--------------------------------------------------------------------------------
-- This file generates the environment that the interpreter starts with. In
-- particular, it contains the grammar that is loaded initially.
--------------------------------------------------------------------------------

module Bootstrap.InitEnv where

open import Class.Map
open import Data.Char.Ranges
open import Data.List using (dropWhile; takeWhile)
open import Data.SimpleMap
open import Data.String using (fromList; toList)

open import Prelude
open import Prelude.Strings

open import Parse.Escape
open import Bootstrap.SimpleInductive

private
  nameSymbols : List Char
  nameSymbols = "$='-/!@&^"

  nameInits : List Char
  nameInits = letters ++ "_"

  nameTails : List Char
  nameTails = nameInits ++ nameSymbols ++ digits

  parseConstrToNonTerminals : String → List String
  parseConstrToNonTerminals = (map fromList) ∘ parseConstrToNonTerminals' ∘ toList
    where
      parseConstrToNonTerminals' : List Char → List (List Char)
      parseConstrToNonTerminals' =
        takeEven ∘ (map concat) ∘ (splitMulti "_") ∘ groupEscaped -- don't split on escaped underscores!
        -- this also ignores ignored non-terminals automatically

  grammar : List (List Char)
  grammar =
    "space'$" ∷ "space'$=newline=_space'_" ∷ "space'$=space=_space'_" ∷
    "space$=newline=_space'_" ∷ "space$=space=_space'_" ∷

    "index'$" ∷ map (λ c → "index'$" ++ [ c ] ++ "_index'_") digits ++
    map (λ c → "index$" ++ [ c ] ++ "_index'_") digits ++
    "var$_string_" ∷ "var$_index_" ∷

    "sort$=ast=" ∷ "sort$=sq=" ∷
    "const$Char" ∷

    "term$_var_" ∷
    "term$_sort_" ∷
    "term$=Kappa=_const_" ∷
    "term$=pi=^space^_term_" ∷
    "term$=psi=^space^_term_" ∷
    "term$=beta=^space^_term_^space^_term_" ∷
    "term$=delta=^space^_term_^space^_term_" ∷
    "term$=sigma=^space^_term_" ∷
    "term$=lsquare=^space'^_term_^space^_term_^space'^=rsquare=" ∷
    "term$=langle=^space'^_term_^space^_term_^space'^=rangle=" ∷
    "term$=rho=^space^_term_^space^_string_^space'^=dot=^space'^_term_^space^_term_" ∷
    "term$=forall=^space^_string_^space'^=colon=^space'^_term_^space^_term_" ∷
    "term$=Pi=^space^_string_^space'^=colon=^space'^_term_^space^_term_" ∷
    "term$=iota=^space^_string_^space'^=colon=^space'^_term_^space^_term_" ∷
    "term$=lambda=^space^_string_^space'^=colon=^space'^_term_^space^_term_" ∷
    "term$=Lambda=^space^_string_^space'^=colon=^space'^_term_^space^_term_" ∷
    "term$=lbrace=^space'^_term_^space'^=comma=^space'^_term_^space^_string_^space'^=dot=^space'^_term_^space'^=rbrace=" ∷
    "term$=phi=^space^_term_^space^_term_^space^_term_" ∷
    "term$=equal=^space^_term_^space^_term_" ∷
    "term$=omega=^space^_term_" ∷ -- this is M
    "term$=mu=^space^_term_^space^_term_" ∷
    "term$=epsilon=^space^_term_" ∷
    "term$=zeta=EvalStmt^space^_term_" ∷
    "term$=zeta=ShellCmd^space^_term_^space^_term_" ∷
    "term$=zeta=CheckTerm^space^_term_^space^_term_" ∷
    "term$=zeta=Parse^space^_term_^space^_term_^space^_term_" ∷
    "term$=zeta=Normalize^space^_term_" ∷
    "term$=zeta=HeadNormalize^space^_term_" ∷
    "term$=zeta=InferType^space^_term_" ∷
    "term$=zeta=CatchErr^space^_term_^space^_term_" ∷ -- this is not actually in PrimMeta
    "term$=kappa=_char_" ∷ -- this constructs a Char
    "term$=gamma=^space^_term_^space^_term_" ∷ -- charEq

    "lettail$=dot=" ∷ "lettail$=colon=^space'^_term_^space'^=dot=" ∷

    "stmt'$let^space^_string_^space'^=colon==equal=^space'^_term_^space'^_lettail_" ∷
    "stmt'$ass^space^_string_^space'^=colon=^space'^_term_^space'^=dot=" ∷
    "stmt'$seteval^space^_term_^space^_string_^space^_string_^space'^=dot=" ∷
    "stmt'$import^space^_string_^space'^=dot=" ∷
    "stmt'$" ∷
    "stmt$^space'^_stmt'_" ∷
    []

  sortGrammar : List (List Char) → SimpleMap (List Char) (List (List Char))
  sortGrammar G = mapSnd (map (dropHeadIfAny ∘ dropWhile (¬? ∘ _≟ '$'))) $
    mapFromList (takeWhile (¬? ∘ _≟ '$')) G

  toInductiveData : String → String → List String → InductiveData
  toInductiveData namespace name constrs =
    (namespace + "$" + name
    , map (λ c → (namespace + "$" + name + "$" + c , map (toConstrData' name) (parseConstrToNonTerminals c)))
          constrs)
    where
      toConstrData' : String → String → ConstrData'
      toConstrData' self l = if self ≣ l then Self else Other (namespace + "$" + l)

  stringData : InductiveData
  stringData =
    ("init$string"
    , ("init$string$cons" , (Other "ΚChar" ∷ Self ∷ [])) ∷ ("init$string$nil" , []) ∷ []) -- capital kappa

  stringListData : InductiveData
  stringListData =
    ("init$stringList" ,
    ("init$stringList$nil" , []) ∷ ("init$stringList$cons" , (Other "init$string" ∷ Self ∷ [])) ∷ [])

  termListData : InductiveData
  termListData =
    ("init$termList"
    , ("init$termList$nil" , []) ∷ ("init$termList$cons" , (Other "init$term" ∷ Self ∷ [])) ∷ [])

  metaResultData : InductiveData
  metaResultData =
    ("init$metaResult"
    , ("init$metaResult$pair" , (Other "init$stringList" ∷ Other "init$termList" ∷ [])) ∷ [])

  charDataConstructor : Char → String → String
  charDataConstructor c prefix =
    "let " + prefix + fromList (escapeChar c) + " := κ" + show c + "."

  nameInitConstrs : List String
  nameInitConstrs = map (flip charDataConstructor "init$nameInitChar$") nameInits

  nameTailConstrs : List String
  nameTailConstrs = map (flip charDataConstructor "init$nameTailChar$") nameTails

  initEnvConstrs : List InductiveData
  initEnvConstrs = stringData ∷
    (map
      (λ { (name , rule) → toInductiveData "init" (fromList name) (map fromList rule) }) $
      sortGrammar grammar)

  otherInit : List String
  otherInit =
    map simpleInductive (stringListData ∷ termListData ∷ metaResultData ∷ [])
    ++ "let init$string$_nameInitChar__string'_ := init$string$cons."
    ∷ "let init$string'$_nameTailChar__string'_ := init$string$cons."
    ∷ "let init$string'$ := init$string$nil."
    ∷ "let init$product := λ A : * λ B : * ∀ X : * Π _ : Π _ : A Π _ : B X X."
    ∷ "let init$pair := λ A : * λ B : * λ a : A λ b : B Λ X : * λ p : Π _ : A Π _ : B X [[p a] b]."
    ∷ "let eval := λ s : init$stmt ζEvalStmt s." ∷ "seteval eval init stmt." ∷ []

  grammarWithChars : List (List Char)
  grammarWithChars = grammar ++
    map ("nameTailChar$" ++_) (map escapeChar nameTails) ++
    map ("nameInitChar$" ++_) (map escapeChar nameInits) ++
    "char$!!" ∷
    "string'$_nameTailChar__string'_" ∷ "string'$" ∷
    "string$_nameInitChar__string'_" ∷
    "var$_string_" ∷ "var$_index_" ∷ []

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

initEnv : String
initEnv = "let init$char := ΚChar." + Data.String.concat
  (map simpleInductive initEnvConstrs ++ nameInitConstrs ++ nameTailConstrs ++ otherInit)

-- a map from non-terminals to their possible expansions
parseRuleMap : SimpleMap (List Char) (List (List Char))
parseRuleMap = from-just $ sequence $ map (λ { (fst , snd) → do
  snd' ← sequence (map (λ x → translate $ fst ++ "$" ++ x) snd)
  return (fst , reverse snd') }) $ sortGrammar grammarWithChars

coreGrammarGenerator : List (List Char)
coreGrammarGenerator = from-just $ sequence $ map translate grammarWithChars

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

open import HoTT
open import cw.CW
open import homotopy.SphereEndomorphism
open import homotopy.PinSn
open import groups.CoefficientExtensionality

module cw.DegreeBySquashing {i} where

  module DegreeAboveOne {n : ℕ} (skel : Skeleton {i} (S (S n)))
    (dec : has-cells-with-dec-eq skel)
    -- the cells at the upper and lower dimensions
    (upper : cells-last skel)
    (lower : cells-last (cw-init skel))
    where

    private
      lower-skel = cw-init skel
      lower-dec = init-has-cells-with-dec-eq skel dec
      lower-cells = cells-last lower-skel
      lower-cells-has-dec-eq = cells-last-has-dec-eq lower-skel lower-dec

    -- squash the lower CW complex except one of its cells [lower]
    cw-squash-lower-to-Sphere : ⟦ lower-skel ⟧ → Sphere (S n)
    cw-squash-lower-to-Sphere = Attached-rec (λ _ → north) squash-hubs squash-spokes where
      -- squash cells except [lower]
      squash-hubs : lower-cells → Sphere (S n)
      squash-hubs c with lower-cells-has-dec-eq c lower
      ... | (inl _) = south
      ... | (inr _) = north
      -- squash cells except [lower]
      squash-spokes : (c : lower-cells) → Sphere n
        → north == squash-hubs c
      squash-spokes c s with lower-cells-has-dec-eq c lower
      ... | (inl _) = merid s
      ... | (inr _) = idp

    degree-map : Sphere (S n) → Sphere (S n)
    degree-map = cw-squash-lower-to-Sphere ∘ attaching-last skel upper

    degree-map' : ℤ-group →ᴳ ℤ-group
    degree-map' = –>ᴳ (πS-SphereS-iso-ℤ n)
               ∘ᴳ Trunc-rec →ᴳ-level (πS-fmap n)
                    (⊙SphereS-endo-in n [ degree-map ])
               ∘ᴳ <–ᴳ (πS-SphereS-iso-ℤ n)

    degree' : ℤ → ℤ
    degree' = GroupHom.f degree-map'

    degree : ℤ
    degree = degree' 1

  module DegreeAtOne (skel : Skeleton {i} 1)
    (dec : has-cells-with-dec-eq skel)
    -- the cells at the upper and lower dimensions
    (line : cells-last skel)
    (point : cells-last (cw-init skel)) where

    private
      points-dec-eq = cells-nth-has-dec-eq (inr ltS) skel dec
      endpoint = attaching-last skel

    -- Maybe [true] can or should be mapped to [-1]. Not sure.
    degree : ℤ
    degree with points-dec-eq (endpoint line true) point
    degree | inl _ = 1
    degree | inr _ with points-dec-eq (endpoint line false) point
    degree | inr _ | inl _ = -1
    degree | inr _ | inr _ = 0

  degree-last : ∀ {n} (skel : Skeleton {i} (S n))
    → has-cells-with-dec-eq skel
    → cells-last skel → cells-last (cw-init skel) → ℤ
  degree-last {n = O} = DegreeAtOne.degree
  degree-last {n = S _} = DegreeAboveOne.degree

  degree-nth : ∀ {m n} (Sm≤n : S m ≤ n) (skel : Skeleton {i} n)
    → has-cells-with-dec-eq skel
    → cells-nth Sm≤n skel → cells-last (cw-init (cw-take Sm≤n skel)) → ℤ
  degree-nth Sm≤n skel dec = degree-last (cw-take Sm≤n skel) (take-has-cells-with-dec-eq Sm≤n skel dec)

  has-degrees-with-finite-support : ∀ {n} (skel : Skeleton {i} n)
    → has-cells-with-dec-eq skel → Type i
  has-degrees-with-finite-support {n = O} _ _ = Lift ⊤
  has-degrees-with-finite-support {n = S n} skel dec =
    has-degrees-with-finite-support (cw-init skel) (init-has-cells-with-dec-eq skel dec) ×
    ∀ upper → has-finite-support (cells-nth-has-dec-eq (inr ltS) skel dec) (degree-last skel dec upper)

  init-has-degrees-with-finite-support : ∀ {n} (skel : Skeleton {i} (S n)) dec
    → has-degrees-with-finite-support skel dec
    → has-degrees-with-finite-support (cw-init skel) (init-has-cells-with-dec-eq skel dec)
  init-has-degrees-with-finite-support skel dec fin-sup = fst fin-sup

  take-has-degrees-with-finite-support : ∀ {m n} (m≤n : m ≤ n) (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    → has-degrees-with-finite-support (cw-take m≤n skel) (take-has-cells-with-dec-eq m≤n skel dec)
  take-has-degrees-with-finite-support (inl idp) skel dec fin-sup = fin-sup
  take-has-degrees-with-finite-support (inr ltS) skel dec fin-sup =
    init-has-degrees-with-finite-support skel dec fin-sup
  take-has-degrees-with-finite-support (inr (ltSR lt)) skel dec fin-sup =
    take-has-degrees-with-finite-support (inr lt) (cw-init skel)
      (init-has-cells-with-dec-eq skel dec)
      (init-has-degrees-with-finite-support skel dec fin-sup)

  degree-last-has-finite-support : ∀ {n} (skel : Skeleton {i} (S n)) dec
    → has-degrees-with-finite-support skel dec
    → ∀ upper → has-finite-support
        (cells-last-has-dec-eq (cw-init skel) (init-has-cells-with-dec-eq skel dec))
        (degree-last skel dec upper)
  degree-last-has-finite-support skel dec fin-sup = snd fin-sup

  degree-nth-has-finite-support : ∀ {m n} (Sm≤n : S m ≤ n) (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    → ∀ upper → has-finite-support
        (cells-last-has-dec-eq
          (cw-init (cw-take Sm≤n skel))
          (init-has-cells-with-dec-eq (cw-take Sm≤n skel) (take-has-cells-with-dec-eq Sm≤n skel dec)))
        (degree-nth Sm≤n skel dec upper)
  degree-nth-has-finite-support Sm≤n skel dec fin-sup =
    degree-last-has-finite-support (cw-take Sm≤n skel)
      (take-has-cells-with-dec-eq Sm≤n skel dec)
      (take-has-degrees-with-finite-support Sm≤n skel dec fin-sup)

  -- the following are named [boundary'] because it is not extended to the free groups

  boundary'-last : ∀ {n} (skel : Skeleton {i} (S n)) dec
    → has-degrees-with-finite-support skel dec
    → cells-last skel → FreeAbGroup.El (cells-last (cw-init skel))
  boundary'-last skel dec fin-sup upper = fst ((snd fin-sup) upper)

  boundary'-nth : ∀ {m n} (Sm≤n : S m ≤ n) (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    → cells-nth Sm≤n skel → FreeAbGroup.El (cells-last (cw-init (cw-take Sm≤n skel)))
  boundary'-nth Sm≤n skel dec fin-sup =
    boundary'-last (cw-take Sm≤n skel)
      (take-has-cells-with-dec-eq Sm≤n skel dec)
      (take-has-degrees-with-finite-support Sm≤n skel dec fin-sup)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Monoidal.Instance.Rels where

-- The category of relations is cartesian and (by self-duality) co-cartesian.
-- Perhaps slightly counter-intuitively if you're used to categories which act
-- like Sets, the product acts on objects as the disjoint union.

open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
import Data.Product as ×
open × using (_,_)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function using (case_of_; flip)
open import Level using (Lift; lift)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Categories.Category.Cartesian using (Cartesian; module CartesianMonoidal)
open import Categories.Category.Core using (Category)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Instance.Rels using (Rels)

module _ {o ℓ} where

  Rels-Cartesian : Cartesian (Rels o ℓ)
  Rels-Cartesian = record
    { terminal = record
      { ⊤ = ⊥
      ; ⊤-is-terminal = record
        { ! = λ { _ (lift ()) }
        ; !-unique = λ _ → (λ { {_} {lift ()} }) , (λ { {_} {lift ()} })
        }
      }
    ; products = record
      { product = λ {A} {B} → record
        { A×B = A ⊎ B
        ; π₁ = [ (λ x y → Lift ℓ (x ≡ y) ) , (λ _ _ → ⊥) ]′
        ; π₂ = [ (λ _ _ → ⊥) , (λ x y → Lift ℓ (x ≡ y)) ]′
        ; ⟨_,_⟩ = λ L R c → [ L c , R c ]′
        ; project₁ = (λ { (inj₁ x , r , lift refl) → r})
          , λ r → inj₁ _ , r , lift refl
        ; project₂ = (λ { (inj₂ _ , r , lift refl) → r })
          , (λ r → inj₂ _ , r , lift refl)
        ; unique =
            λ { (p , q) (p′ , q′) → (λ { {_} {inj₁ a} r → case (q {_} {a} r) of λ { (inj₁ .a , s , lift refl) → s}
                                       ; {_} {inj₂ b} r → case (q′ {_} {b} r) of λ { (inj₂ .b , s , lift refl) → s} })
                                   , λ { {_} {inj₁ a} hxa → p (inj₁ a , hxa , lift refl)
                                       ; {_} {inj₂ b} hxb → p′ (inj₂ b , hxb , lift refl) } }
        }
      }
    }

  module Rels-CartesianMonoidal = CartesianMonoidal _ Rels-Cartesian
  open Rels-CartesianMonoidal renaming (monoidal to Rels-Monoidal) public

  -- because Rels is dual to itself, the proof that it is cocartesian resembles the proof that it's cartesian
  -- Rels is not self-dual 'on the nose', so we can't use duality proper.
  Rels-Cocartesian : Cocartesian (Rels o ℓ)
  Rels-Cocartesian = record
    { initial = record
      { ⊥ = ⊥
      ; ⊥-is-initial = record
        { ! = λ ()
        ; !-unique = λ _ → (λ { {()} }) , (λ { {()} })
        }
      }
    ; coproducts = record
      { coproduct = λ {A} {B} → record
        { A+B = A ⊎ B
        ; i₁ = λ a → [ (λ a′ → Lift ℓ (a ≡ a′)) , (λ _ → ⊥) ]′
        ; i₂ = λ b → [ (λ _ → ⊥) , (λ b′ → Lift ℓ (b ≡ b′)) ]′
        ; [_,_] = λ L R a+b c → [ flip L c , flip R c ]′ a+b
        ; inject₁ = (λ { (inj₁ x , lift refl , fxy) → fxy})
          , λ r → inj₁ _ , lift refl , r
        ; inject₂ = (λ { (inj₂ _ , lift refl , r) → r })
          , (λ r → inj₂ _ , lift refl , r)
        ; unique = λ { (p , q) (p′ , q′) → (λ { {inj₁ a} r → case (q {a} r) of λ { (inj₁ .a , lift refl , s) → s}
                                              ; {inj₂ b} r → case (q′ {b} r) of λ { (inj₂ .b , lift refl , s) → s} })
                                          , λ { {inj₁ a} hxa → p (inj₁ a , lift refl , hxa)
                                              ; {inj₂ b} hxb → p′ (inj₂ b , lift refl , hxb) } }
        }
      }
    }

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: andrejbauer/agda-categories

max_forks_repo_name: andrejbauer/agda-categories


text:
module Common.MAlonzo where

open import Common.Prelude
open import Common.Coinduction

postulate
  putStrLn : ∞ String → IO Unit

{-# COMPILED putStrLn putStrLn #-}

main = putStrLn (♯ "This is a dummy main routine.")

mainPrint : String → _
mainPrint s = putStrLn (♯ s)

postulate
  natToString : Nat → String

{-# COMPILED natToString show #-}

mainPrintNat : Nat → _
mainPrintNat n = putStrLn (♯ (natToString n))

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Relations between properties of functions, such as associativity and
-- commutativity
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total)

module Algebra.FunctionProperties.Consequences
  {a ℓ} (S : Setoid a ℓ) where

open Setoid S renaming (Carrier to A)

open import Algebra.FunctionProperties _≈_
open import Data.Sum using (inj₁; inj₂)
open import Data.Product using (_,_)
import Relation.Binary.Consequences as Bin
open import Relation.Binary.Reasoning.Setoid S
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- Re-export core properties

open import Algebra.FunctionProperties.Consequences.Core public

------------------------------------------------------------------------
-- Magma-like structures

module _ {_•_ : Op₂ A} (comm : Commutative _•_) where

  comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ →  RightCancellative _•_
  comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x (begin
    x • y ≈⟨ comm x y ⟩
    y • x ≈⟨ eq ⟩
    z • x ≈⟨ comm z x ⟩
    x • z ∎)

  comm+cancelʳ⇒cancelˡ : RightCancellative _•_ → LeftCancellative _•_
  comm+cancelʳ⇒cancelˡ cancelʳ x {y} {z} eq = cancelʳ y z (begin
    y • x ≈⟨ comm y x ⟩
    x • y ≈⟨ eq ⟩
    x • z ≈⟨ comm x z ⟩
    z • x ∎)

------------------------------------------------------------------------
-- Monoid-like structures

module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where

  comm+idˡ⇒idʳ : LeftIdentity e _•_ → RightIdentity e _•_
  comm+idˡ⇒idʳ idˡ x = begin
    x • e ≈⟨ comm x e ⟩
    e • x ≈⟨ idˡ x ⟩
    x     ∎

  comm+idʳ⇒idˡ : RightIdentity e _•_ → LeftIdentity e _•_
  comm+idʳ⇒idˡ idʳ x = begin
    e • x ≈⟨ comm e x ⟩
    x • e ≈⟨ idʳ x ⟩
    x     ∎

  comm+zeˡ⇒zeʳ : LeftZero e _•_ → RightZero e _•_
  comm+zeˡ⇒zeʳ zeˡ x = begin
    x • e ≈⟨ comm x e ⟩
    e • x ≈⟨ zeˡ x ⟩
    e     ∎

  comm+zeʳ⇒zeˡ : RightZero e _•_ → LeftZero e _•_
  comm+zeʳ⇒zeˡ zeʳ x = begin
    e • x ≈⟨ comm e x ⟩
    x • e ≈⟨ zeʳ x ⟩
    e     ∎

------------------------------------------------------------------------
-- Group-like structures

module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _•_) where

  comm+invˡ⇒invʳ : LeftInverse e _⁻¹ _•_ → RightInverse e _⁻¹ _•_
  comm+invˡ⇒invʳ invˡ x = begin
    x • (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩
    (x ⁻¹) • x ≈⟨ invˡ x ⟩
    e          ∎

  comm+invʳ⇒invˡ : RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_
  comm+invʳ⇒invˡ invʳ x = begin
    (x ⁻¹) • x ≈⟨ comm (x ⁻¹) x ⟩
    x • (x ⁻¹) ≈⟨ invʳ x ⟩
    e          ∎

module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _•_) where

  assoc+id+invʳ⇒invˡ-unique : Associative _•_ →
                              Identity e _•_ → RightInverse e _⁻¹ _•_ →
                              ∀ x y → (x • y) ≈ e → x ≈ (y ⁻¹)
  assoc+id+invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
    x                ≈⟨ sym (idʳ x) ⟩
    x • e            ≈⟨ cong refl (sym (invʳ y)) ⟩
    x • (y • (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
    (x • y) • (y ⁻¹) ≈⟨ cong eq refl ⟩
    e • (y ⁻¹)       ≈⟨ idˡ (y ⁻¹) ⟩
    y ⁻¹             ∎

  assoc+id+invˡ⇒invʳ-unique : Associative _•_ →
                              Identity e _•_ → LeftInverse e _⁻¹ _•_ →
                              ∀ x y → (x • y) ≈ e → y ≈ (x ⁻¹)
  assoc+id+invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
    y                ≈⟨ sym (idˡ y) ⟩
    e • y            ≈⟨ cong (sym (invˡ x)) refl ⟩
    ((x ⁻¹) • x) • y ≈⟨ assoc (x ⁻¹) x y ⟩
    (x ⁻¹) • (x • y) ≈⟨ cong refl eq ⟩
    (x ⁻¹) • e       ≈⟨ idʳ (x ⁻¹) ⟩
    x ⁻¹             ∎

----------------------------------------------------------------------
-- Bisemigroup-like structures

module _ {_•_ _◦_ : Op₂ A}
         (◦-cong : Congruent₂ _◦_)
         (•-comm : Commutative _•_)
         where

  comm+distrˡ⇒distrʳ :  _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_
  comm+distrˡ⇒distrʳ distrˡ x y z = begin
    (y ◦ z) • x       ≈⟨ •-comm (y ◦ z) x ⟩
    x • (y ◦ z)       ≈⟨ distrˡ x y z ⟩
    (x • y) ◦ (x • z) ≈⟨ ◦-cong (•-comm x y) (•-comm x z) ⟩
    (y • x) ◦ (z • x) ∎

  comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_
  comm+distrʳ⇒distrˡ distrˡ x y z = begin
    x • (y ◦ z)       ≈⟨ •-comm x (y ◦ z) ⟩
    (y ◦ z) • x       ≈⟨ distrˡ x y z ⟩
    (y • x) ◦ (z • x) ≈⟨ ◦-cong (•-comm y x) (•-comm z x) ⟩
    (x • y) ◦ (x • z) ∎

  comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≈ ((x ◦ y) • (x ◦ z)))
  comm⇒sym[distribˡ] x {y} {z} prf = begin
    x ◦ (z • y)       ≈⟨ ◦-cong refl (•-comm z y) ⟩
    x ◦ (y • z)       ≈⟨ prf ⟩
    (x ◦ y) • (x ◦ z) ≈⟨ •-comm (x ◦ y) (x ◦ z) ⟩
    (x ◦ z) • (x ◦ y) ∎

----------------------------------------------------------------------
-- Ring-like structures

module _ {_+_ _*_ : Op₂ A}
         {_⁻¹ : Op₁ A} {0# : A}
         (+-cong : Congruent₂ _+_)
         (*-cong : Congruent₂ _*_)
         where

  assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
                                RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
                                LeftZero 0# _*_
  assoc+distribʳ+idʳ+invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ  x = begin
    0# * x                                 ≈⟨ sym (idʳ _) ⟩
    (0# * x) + 0#                          ≈⟨ +-cong refl (sym (invʳ _)) ⟩
    (0# * x) + ((0# * x)  + ((0# * x)⁻¹))  ≈⟨ sym (+-assoc _ _ _) ⟩
    ((0# * x) +  (0# * x)) + ((0# * x)⁻¹)  ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ⟩
    ((0# + 0#) * x) + ((0# * x)⁻¹)         ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩
    (0# * x) + ((0# * x)⁻¹)                ≈⟨ invʳ _ ⟩
    0#                                     ∎

  assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
                                RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
                                RightZero 0# _*_
  assoc+distribˡ+idʳ+invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ  x = begin
     x * 0#                                ≈⟨ sym (idʳ _) ⟩
     (x * 0#) + 0#                         ≈⟨ +-cong refl (sym (invʳ _)) ⟩
     (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹))  ≈⟨ sym (+-assoc _ _ _) ⟩
     ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹)  ≈⟨ +-cong (sym (distribˡ _ _ _)) refl ⟩
     (x * (0# + 0#)) + ((x * 0#)⁻¹)        ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩
     ((x * 0#) + ((x * 0#)⁻¹))             ≈⟨ invʳ _ ⟩
     0#                                    ∎

------------------------------------------------------------------------
-- Without Loss of Generality

module _ {p} {f : Op₂ A} {P : Pred A p}
         (≈-subst : Substitutive _≈_ p)
         (comm : Commutative f)
         where

  subst+comm⇒sym : Symmetric (λ a b → P (f a b))
  subst+comm⇒sym = ≈-subst P (comm _ _)

  wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ →
         (∀ a b → a R b → P (f a b)) →
         ∀ a b → P (f a b)
  wlog r-total = Bin.wlog r-total subst+comm⇒sym


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

open import prelude renaming (_≟Nat_ to _≟_)

-- Copied pretty much verbatim

Var = Nat

data Term : Set where
  var : Var → Term
  fun : Term → Term
  _$_ : Term → Term → Term
  true : Term
  false : Term
  if_then_else_end : Term → Term → Term → Term

data VarHeaded : Term → Set
data Value : Term → Set

data VarHeaded where
  var : (x : Var) → VarHeaded(var x)
  _$_ : ∀ {t} → VarHeaded(t) → (u : Term) → VarHeaded(t $ u)
  if_then_else_end : ∀ {t₀} → VarHeaded(t₀) → (t₁ t₂ : Term) → VarHeaded(if t₀ then t₁ else t₂ end)

data Value where
  var : (x : Var) → Value(var x)
  fun : (t : Term) → Value(fun t)
  _$_ : ∀ {t} → VarHeaded(t) → (u : Term) → Value(t $ u)
  if_then_else_end : ∀ {t₀} → VarHeaded(t₀) → (t₁ t₂ : Term) → Value(if t₀ then t₁ else t₂ end)
  true : Value true
  false :  Value false

-- Substitution

shift : Var → Var → Term → Term
shift c d (var x) = if (c ≤? x) (var (d + x)) (var x)
shift c d (fun t) = fun (shift (1 + c) d t)
shift c d (t₁ $ t₂) = (shift c d t₁) $ (shift c d t₂)
shift c d true = true
shift c d false = false
shift c d if t₀ then t₁ else t₂ end = if shift c d t₀ then shift c d t₁ else shift c d t₂ end

[_↦_]_ : Var → Term → Term → Term
[ x ↦ s ] var y = if (x ≟ y) (shift 0 x s) (if (x ≤? y) (var (y - 1)) (var y))
[ x ↦ s ] fun t = fun ([ (1 + x) ↦ s ] t)
[ x ↦ s ] (t₁ $ t₂) = ([ x ↦ s ] t₁) $ ([ x ↦ s ] t₂)
[ x ↦ s ] true = true
[ x ↦ s ] false = false
[ x ↦ s ] if t₀ then t₁ else t₂ end = if [ x ↦ s ] t₀ then [ x ↦ s ] t₁ else [ x ↦ s ] t₂ end

-- Reduction

data _⟶_ : Term → Term → Set where

  E─IfTrue : ∀ {t₂ t₃} →

    -----------------------------------
    if true then t₂ else t₃ end ⟶ t₂

  E─IfFalse : ∀ {t₂ t₃} →

    -----------------------------------
    if false then t₂ else t₃ end ⟶ t₃

  E─IfCong : ∀ {t₁ t₁′ t₂ t₃} →

    (t₁ ⟶ t₁′) →
    ----------------------------------------------------------
    (if t₁ then t₂ else t₃ end ⟶ if t₁′ then t₂ else t₃ end)

  E─App1 : ∀ {t₁ t₁′ t₂} →

     (t₁ ⟶ t₁′) →
     ------------------------
     (t₁ $ t₂) ⟶ (t₁′ $ t₂)

  E─App2 : ∀ {t₁ t₂ t₂′} →

     (t₂ ⟶ t₂′) →
     ------------------------
     (t₁ $ t₂) ⟶ (t₁ $ t₂′)

  E─AppAbs : ∀ {t₁ t₂} →

     ---------------------------------
     (fun t₁ $ t₂) ⟶ ([ 0 ↦ t₂ ] t₁)

data Redex  : Term → Set where

  redex : ∀ {t t′} →

    t ⟶ t′ →
    --------
    Redex(t)

-- Types

data Type : Set where
  bool : Type
  _⇒_ : Type → Type → Type

data Context : Set where
  ε : Context
  _,_ : Context → Type → Context

data _∋_⦂_ : Context → Nat → Type → Set where

  zero : ∀ {Γ S} → (Γ , S) ∋ zero ⦂ S
  suc : ∀ {Γ S T n} → (Γ ∋ n ⦂ T) → (Γ , S) ∋ suc n ⦂ T

data _⊢_⦂_ : Context → Term → Type → Set where

  T-True : ∀ {Γ} →

    -----------
    Γ ⊢ true ⦂ bool

  T-False : ∀ {Γ} →

    -----------
    Γ ⊢ false ⦂ bool

  T-If : ∀ {Γ t₁ t₂ t₃ T} →

    Γ ⊢ t₁ ⦂ bool →
    Γ ⊢ t₂ ⦂ T →
    Γ ⊢ t₃ ⦂ T →
    -----------------------------
    Γ ⊢ if t₁ then t₂ else t₃ end ⦂ T

  T-Var : ∀ {Γ n T} →

    Γ ∋ n ⦂ T →
    ------------------------
    Γ ⊢ var n ⦂ T

  T-Abs : ∀ {Γ t T₁ T₂} →

    (Γ , T₁) ⊢ t ⦂ T₂ →
    -----------------------
    Γ ⊢ (fun t) ⦂ (T₁ ⇒ T₂)

  T-App : ∀ {Γ t₁ t₂ T₁₁ T₁₂} →

    Γ ⊢ t₁ ⦂ (T₁₁ ⇒ T₁₂) →
    Γ ⊢ t₂ ⦂ T₁₁ →
    -----------------------
    Γ ⊢ (t₁ $ t₂) ⦂ T₁₂

-- Proving that well-typed terms stay well-typed

# : Context → Nat
# ε = 0
# (Γ , x) = 1 + # Γ

_,,_ : Context → Context → Context
Γ ,, ε = Γ
Γ ,, (Δ , T) = (Γ ,, Δ) , T

T-Eq : ∀ {Γ s S T} → (Γ ⊢ s ⦂ S) → (S ≡ T) → (Γ ⊢ s ⦂ T)
T-Eq p refl = p

hit : ∀ {Γ Δ S T} → (((Γ , S) ,, Δ) ∋ # Δ ⦂ T) → (S ≡ T)
hit {Δ = ε} zero = refl
hit {Δ = Δ , R} (suc p) = hit p

left : ∀ {Γ Δ S T n} → (# Δ < n) → (((Γ , S) ,, Δ) ∋ n ⦂ T) → ((Γ ,, Δ) ∋ (n - 1) ⦂ T)
left {n = zero} p q = CONTRADICTION (p zero)
left {Δ = ε} {n = suc n} p (suc q) = q
left {Δ = Δ , R} {n = suc zero} p (suc q) = CONTRADICTION (p (suc zero))
left {Δ = Δ , R} {n = suc (suc n)} p (suc q) = suc (left (λ a → p (suc a)) q)

right : ∀ {Γ Δ S T n} → (n < # Δ) → (((Γ , S) ,, Δ) ∋ n ⦂ T) → ((Γ ,, Δ) ∋ n ⦂ T)
right {Δ = ε} p q = CONTRADICTION (p zero)
right {Δ = Δ , R} p zero = zero
right {Δ = Δ , R} p (suc q) = suc (right (λ z → p (suc z)) q)

this : ∀ {Γ T} n Δ Ξ → (# Ξ ≤ n) → ((Γ ,, Ξ) ∋ n ⦂ T) → (((Γ ,, Δ) ,, Ξ) ∋ (# Δ + n) ⦂ T)
this n ε ε p q = q
this n (Δ , R) ε p q = suc (this n Δ ε p q)
this (suc n) Δ (Ξ , S) (suc p) (suc q) = suc (this n Δ Ξ p q)

that : ∀ {Γ T} n Δ Ξ → (n < # Ξ) → ((Γ ,, Ξ) ∋ n ⦂ T) → (((Γ ,, Δ) ,, Ξ) ∋ n ⦂ T)
that n Δ ε p q = CONTRADICTION (p zero)
that zero Δ (Ξ , S) p zero = zero
that (suc n) Δ (Ξ , S) p (suc q) = suc (that n Δ Ξ (λ z → p (suc z)) q)

preservation-shift : ∀ {Γ s S} Δ Ξ → ((Γ ,, Ξ) ⊢ s ⦂ S) → (((Γ ,, Δ) ,, Ξ) ⊢ shift (# Ξ) (# Δ) s ⦂ S)
preservation-shift Δ Ξ T-True = T-True
preservation-shift Δ Ξ T-False = T-False
preservation-shift Δ Ξ (T-If p p₁ p₂) = T-If (preservation-shift Δ Ξ p) (preservation-shift Δ Ξ p₁)
                                          (preservation-shift Δ Ξ p₂)
preservation-shift {Γ} {var n} {S} Δ Ξ (T-Var p) = helper (# Ξ ≤? n) where

  helper : (q : Dec(# Ξ ≤ n)) → ((Γ ,, Δ) ,, Ξ) ⊢ if q (var (# Δ + n)) (var n) ⦂ S
  helper (yes q) = T-Var (this n Δ Ξ q p)
  helper (no q)  = T-Var (that n Δ Ξ q p)

preservation-shift Δ Ξ (T-Abs p) = T-Abs (preservation-shift Δ (Ξ , _) p)
preservation-shift Δ Ξ (T-App p p₁) = T-App (preservation-shift Δ Ξ p) (preservation-shift Δ Ξ p₁)

preservation-substitution : ∀ {Γ s t S T} → (Γ ⊢ s ⦂ S) → (Δ : Context) → (((Γ , S) ,, Δ) ⊢ t ⦂ T) → ((Γ ,, Δ) ⊢ [ # Δ ↦ s ] t ⦂ T)
preservation-substitution {Γ} {s} {t} {S} {T} p Δ (T-Var {n = n} q) = helper (# Δ ≟ n) (# Δ ≤? n) where

  helper : (p : Dec(# Δ ≡ n)) → (q : Dec(# Δ ≤ n)) → (Γ ,, Δ) ⊢ if p (shift 0 (# Δ) s) (if q (var (n - 1)) (var n)) ⦂ T
  helper (yes refl) _ = T-Eq (preservation-shift Δ ε p) (hit q)
  helper (no a) (yes b) = T-Var (left (λ c → a (asym b c)) q)
  helper (no a) (no b) = T-Var (right b q)

preservation-substitution p Δ T-True = T-True
preservation-substitution p Δ T-False = T-False
preservation-substitution p Δ (T-If q q₁ q₂) = T-If (preservation-substitution p Δ q)
                                                 (preservation-substitution p Δ q₁)
                                                 (preservation-substitution p Δ q₂)
preservation-substitution p Δ (T-Abs q) = T-Abs (preservation-substitution p (Δ , _) q)
preservation-substitution p Δ (T-App q q₁) = T-App (preservation-substitution p Δ q)
                                               (preservation-substitution p Δ q₁)

preservation : ∀ {Γ t t′ T} → (Γ ⊢ t ⦂ T) → (t ⟶ t′) → (Γ ⊢ t′ ⦂ T)
preservation (T-If p₁ p₂ p₃) E─IfTrue = p₂
preservation (T-If p₁ p₂ p₃) E─IfFalse = p₃
preservation (T-If p₁ p₂ p₃) (E─IfCong q) = T-If (preservation p₁ q) p₂ p₃
preservation (T-App p₁ p₂) (E─App1 q) = T-App (preservation p₁ q) p₂
preservation (T-App p₁ p₂) (E─App2 q) = T-App p₁ (preservation p₂ q)
preservation (T-App (T-Abs p₁) p₂) E─AppAbs = preservation-substitution p₂ ε p₁

-- Proving that every term is a value or a redex

data ValueOrRedex : Term → Set where

  value : ∀ {t} →

    (Value(t)) →
    ---------------
    ValueOrRedex(t)

  redex : ∀ {t t′} →

    t ⟶ t′ →
    ---------------
    ValueOrRedex(t)

progress : ∀ {Γ t T} → (Γ ⊢ t ⦂ T) → ValueOrRedex(t)
progress T-True = value true
progress T-False = value false
progress (T-If p₁ p₂ p₃) = helper (progress p₁) p₁ where

  helper : ∀ {Γ t₀ t₁ t₂} → ValueOrRedex(t₀) → (Γ ⊢ t₀ ⦂ bool) → ValueOrRedex(if t₀ then t₁ else t₂ end)
  helper (value true) p = redex E─IfTrue
  helper (value false) p = redex E─IfFalse
  helper (value (var x)) p = value (if var x then _ else _ end)
  helper (value (if t₃ then t₄ else t₅ end)) p = value if if t₃ then t₄ else t₅ end then _ else _ end
  helper (value (t₁ $ t₂)) p = value if (t₁ $ t₂) then _ else _ end
  helper (redex r) p = redex (E─IfCong r)

progress (T-Var {n = n} p) = value (var n)
progress (T-Abs {t = t} p) = value (fun t)
progress (T-App p₁ p₂) = helper (progress p₁) p₁ where

  helper : ∀ {Γ t₁ t₂ T₁₁ T₁₂} → ValueOrRedex(t₁) → (Γ ⊢ t₁ ⦂ (T₁₁ ⇒ T₁₂)) → ValueOrRedex(t₁ $ t₂)
  helper (value (var x)) p = value (var x $ _)
  helper (value (fun t)) p = redex E─AppAbs
  helper (value (t₃ $ t₄)) p = value ((t₃ $ t₄) $ _)
  helper (value (if t₃ then t₄ else t₅ end)) p = value (if t₃ then t₄ else t₅ end $ _)
  helper (redex r) p = redex (E─App1 r)

-- Interpreter

data _⟶*_ : Term → Term → Set where

  done : ∀ {t} →

    --------
    t ⟶* t

  redex : ∀ {t t′ t″} →

    t ⟶ t′ →
    t′ ⟶* t″ →
    ----------
    t ⟶* t″

-- An interpreter result

data Result  : Term → Set where

  result : ∀ {t t′} →

    t ⟶* t′ →
    Value(t′) →
    ---------
    Result(t)

-- The interpreter just calls `progress` until it is a value.
-- This might bot terminate!

{-# NON_TERMINATING #-}
interp : ∀ {Γ t T} → (Γ ⊢ t ⦂ T) → Result(t)
interp p = helper₂ p (progress p) where

  helper₁ : ∀ {t t′} → (t ⟶ t′) → Result(t′) → Result(t)
  helper₁ r (result s v) = result (redex r s) v

  helper₂ : ∀ {Γ t T} → (Γ ⊢ t ⦂ T) → ValueOrRedex(t) → Result(t)
  helper₂ p (value v) = result done v
  helper₂ p (redex r) = helper₁ r (interp (preservation p r))

max_stars_repo_name: asajeffrey/tapl

max_issues_repo_name: asajeffrey/tapl

max_forks_repo_name: asajeffrey/tapl


text:
module PublicWithoutOpen2 where

import Imports.A public


text:
open import Oscar.Prelude
open import Oscar.Data.¶

module Oscar.Data.Fin where

data ¶⟨<_⟩ : ¶ → Ø₀ where
  ∅ : ∀ {n} → ¶⟨< ↑ n ⟩
  ↑_ : ∀ {n} → ¶⟨< n ⟩ → ¶⟨< ↑ n ⟩

Fin = ¶⟨<_⟩

module Fin = ¶⟨<_⟩


text:
-- Tests for withNormalisation

module _ where

open import Agda.Builtin.Reflection
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Unit
open import Agda.Builtin.List

infixl 4 _>>=_
_>>=_ = bindTC

F : Bool → Set
F false = Nat
F true  = Bool

data D (b : Bool) : Set where

_&&_ : Bool → Bool → Bool
true  && x = x
false && _ = false

postulate
  reflected : ∀ {a} {A : Set a} → Term → A

pattern vArg x = arg (arg-info visible relevant) x

useReflected : Term → Term → TC ⊤
useReflected hole goal =
  quoteTC goal >>= λ `goal →
  unify hole (def (quote reflected) (vArg `goal ∷ []))

macro
  error : Term → TC ⊤
  error hole =
    inferType hole >>= λ goal → typeError (termErr goal ∷ [])

  reflect : Term → TC ⊤
  reflect hole = inferType hole >>= useReflected hole

  reflectN : Term → TC ⊤
  reflectN hole = withNormalisation true (inferType hole) >>= useReflected hole

test₁ : D (true && false)
test₁ = reflect

test₂ : D (true && false)
test₂ = reflectN

pattern `D x = def (quote D) (vArg x ∷ [])
pattern `true = con (quote true) []
pattern `false = con (quote false) []
pattern _`&&_ x y = def (quote _&&_) (vArg x ∷ vArg y ∷ [])

check₁ : test₁ ≡ reflected (`D (`true `&& `false))
check₁ = refl

check₂ : test₂ ≡ reflected (`D `false)
check₂ = refl


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

module Cubical.Algebra.Group.Semidirect where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphism
open import Cubical.Algebra.Group.Notation
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Action
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' : Level

module _  where

  semidirectProd : (G : Group {ℓ}) (H : Group {ℓ'}) (Act : GroupAction H G) → Group {ℓ-max ℓ ℓ'}
  semidirectProd G H Act = makeGroup-left {A = sd-carrier} sd-0 _+sd_ -sd_ sd-set sd-assoc sd-lId sd-lCancel
    where
      open ActionNotationα Act
      open ActionLemmas Act
      open GroupNotationG G
      open GroupNotationᴴ H
      -- sd stands for semidirect
      sd-carrier = ⟨ G ⟩ × ⟨ H ⟩
      sd-0 = 0ᴳ , 0ᴴ

      module _ ((g , h) : sd-carrier) where
        -sd_ = (-ᴴ h) α (-ᴳ g) , -ᴴ h

        _+sd_ = λ (g' , h') → g +ᴳ (h α g') , h +ᴴ h'

      abstract
        sd-set = isSetΣ setᴳ (λ _ → setᴴ)
        sd-lId = λ ((g , h) : sd-carrier) → ΣPathP (lIdᴳ (0ᴴ α g) ∙ (α-id g) , lIdᴴ h)
        sd-lCancel = λ ((g , h) : sd-carrier) → ΣPathP ((sym (α-hom (-ᴴ h) (-ᴳ g) g) ∙∙ cong ((-ᴴ h) α_) (lCancelᴳ g) ∙∙ actOnUnit (-ᴴ h)) , lCancelᴴ h)

        sd-assoc = λ (a , x) (b , y) (c , z) → ΣPathP ((a +ᴳ (x α (b  +ᴳ (y α c)))
                                    ≡⟨ cong (a +ᴳ_) (α-hom x b (y α c)) ⟩
                                a +ᴳ ((x α b) +ᴳ (x α (y α c)))
                                    ≡⟨ assocᴳ a (x α b) (x α (y α c)) ⟩
                                (a +ᴳ (x α b)) +ᴳ (x α (y α c))
                                    ≡⟨ cong ((a +ᴳ (x α b)) +ᴳ_) (sym (α-assoc x y c)) ⟩
                                (a +ᴳ (x α b)) +ᴳ ((x +ᴴ y) α c) ∎) , assocᴴ x y z)

  -- this syntax declaration is the reason we can't unify semidirectProd with
  -- the projections module
  syntax semidirectProd G H α = G ⋊⟨ α ⟩ H

module _ {G : Group {ℓ}} {H : Group {ℓ'}} (Act : GroupAction H G) where
  open ActionNotationα Act
  open ActionLemmas Act
  open GroupNotationG G
  open GroupNotationᴴ H

  π₁ : ⟨ G ⋊⟨ Act ⟩ H ⟩ → ⟨ G ⟩
  π₁ = fst

  ι₁ : GroupHom G (G ⋊⟨ Act ⟩ H)
  ι₁ = grouphom (λ g → g , 0ᴴ) λ g g' → ΣPathP (cong (g +ᴳ_) (sym (α-id g')), sym (lIdᴴ 0ᴴ))

  π₂ : GroupHom (G ⋊⟨ Act ⟩ H) H
  -- π₂ = grouphom snd λ _ _ → refl
  π₂ = grouphom snd λ (g , h) (g' , h') → refl {x = h +ᴴ h'}

  ι₂ : GroupHom H (G ⋊⟨ Act ⟩ H)
  ι₂ = grouphom (λ h → 0ᴳ , h) λ h h' → ΣPathP (sym (actOnUnit h) ∙ sym (lIdᴳ (h α 0ᴳ)) , refl)

  π₂-hasSec : isGroupSplitEpi ι₂ π₂
  π₂-hasSec = GroupMorphismExt (λ _ → refl)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- The delay monad is a monad up to strong bisimilarity
------------------------------------------------------------------------

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

module Delay-monad.Monad where

open import Equality.Propositional
open import Prelude
open import Prelude.Size

open import Conat equality-with-J as Conat using (zero; suc; force)
open import Monad equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity as B

------------------------------------------------------------------------
-- Map, join and bind

-- A universe-polymorphic variant of map.

map′ : ∀ {i a b} {A : Type a} {B : Type b} →
       (A → B) → Delay A i → Delay B i
map′ f (now   x) = now (f x)
map′ f (later x) = later λ { .force → map′ f (force x) }

-- Join.

join : ∀ {i a} {A : Type a} →
       Delay (Delay A i) i → Delay A i
join (now   x) = x
join (later x) = later λ { .force → join (force x) }

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : ∀ {i a b} {A : Type a} {B : Type b} →
         Delay A i → (A → Delay B i) → Delay B i
x >>=′ f = join (map′ f x)

instance

  -- A raw monad instance.

  delay-raw-monad : ∀ {a i} → Raw-monad (λ (A : Type a) → Delay A i)
  Raw-monad.return delay-raw-monad = now
  Raw-monad._>>=_  delay-raw-monad = _>>=′_

------------------------------------------------------------------------
-- Monad laws

left-identity′ :
  ∀ {a b} {A : Type a} {B : Type b} x (f : A → Delay B ∞) →
  return x >>=′ f ∼ f x
left-identity′ x f = reflexive (f x)

right-identity′ : ∀ {a i} {A : Type a} (x : Delay A ∞) →
                  [ i ] x >>= return ∼ x
right-identity′ (now   x) = now
right-identity′ (later x) = later λ { .force →
                              right-identity′ (force x) }

associativity′ :
  ∀ {a b c i} {A : Type a} {B : Type b} {C : Type c} →
  (x : Delay A ∞) (f : A → Delay B ∞) (g : B → Delay C ∞) →
  [ i ] x >>=′ (λ x → f x >>=′ g) ∼ x >>=′ f >>=′ g
associativity′ (now   x) f g = reflexive (f x >>=′ g)
associativity′ (later x) f g = later λ { .force →
                                 associativity′ (force x) f g }

-- The delay monad is a monad (assuming extensionality).

delay-monad :
  ∀ {a} → B.Extensionality a → Monad (λ (A : Type a) → Delay A ∞)
Monad.raw-monad      (delay-monad ext)       = delay-raw-monad
Monad.left-identity  (delay-monad ext) x f   = ext (left-identity′ x f)
Monad.right-identity (delay-monad ext) x     = ext (right-identity′ x)
Monad.associativity  (delay-monad ext) x f g = ext (associativity′ x f g)

------------------------------------------------------------------------
-- The functions map′, join and _>>=′_ preserve strong and weak
-- bisimilarity and expansion

map-cong : ∀ {k i a b} {A : Type a} {B : Type b}
           (f : A → B) {x y : Delay A ∞} →
           [ i ] x ⟨ k ⟩ y → [ i ] map′ f x ⟨ k ⟩ map′ f y
map-cong f now        = now
map-cong f (later  p) = later λ { .force → map-cong f (force p) }
map-cong f (laterˡ p) = laterˡ (map-cong f p)
map-cong f (laterʳ p) = laterʳ (map-cong f p)

join-cong : ∀ {k i a} {A : Type a} {x y : Delay (Delay A ∞) ∞} →
            [ i ] x ⟨ k ⟩ y → [ i ] join x ⟨ k ⟩ join y
join-cong now        = reflexive _
join-cong (later  p) = later λ { .force → join-cong (force p) }
join-cong (laterˡ p) = laterˡ (join-cong p)
join-cong (laterʳ p) = laterʳ (join-cong p)

infixl 5 _>>=-cong_

_>>=-cong_ :
  ∀ {k i a b} {A : Type a} {B : Type b}
    {x y : Delay A ∞} {f g : A → Delay B ∞} →
  [ i ] x ⟨ k ⟩ y → (∀ z → [ i ] f z ⟨ k ⟩ g z) →
  [ i ] x >>=′ f ⟨ k ⟩ y >>=′ g
now      >>=-cong  q = q _
later  p >>=-cong  q = later λ { .force → force p >>=-cong q }
laterˡ p >>=-cong  q = laterˡ (p >>=-cong q)
laterʳ p >>=-cong  q = laterʳ (p >>=-cong q)

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

-- The function map′ can be expressed using _>>=′_ and now.

map∼>>=-now :
  ∀ {i a b} {A : Type a} {B : Type b} {f : A → B} (x : Delay A ∞) →
  [ i ] map′ f x ∼ x >>=′ now ∘ f
map∼>>=-now (now x)   = now
map∼>>=-now (later x) = later λ { .force → map∼>>=-now (x .force) }

------------------------------------------------------------------------
-- Some lemmas relating monadic combinators to steps

-- Use of map′ does not affect the number of steps in the computation.

steps-map′ :
  ∀ {i a b} {A : Type a} {B : Type b} {f : A → B}
  (x : Delay A ∞) →
  Conat.[ i ] steps (map′ f x) ∼ steps x
steps-map′ (now x)   = zero
steps-map′ (later x) = suc λ { .force → steps-map′ (x .force) }

-- Use of _⟨$⟩_ does not affect the number of steps in the
-- computation.

steps-⟨$⟩ :
  ∀ {i ℓ} {A B : Type ℓ} {f : A → B}
  (x : Delay A ∞) →
  Conat.[ i ] steps (f ⟨$⟩ x) ∼ steps x
steps-⟨$⟩ (now x)   = zero
steps-⟨$⟩ (later x) = suc λ { .force → steps-⟨$⟩ (x .force) }

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
module _ where

open import Agda.Builtin.Equality

module _ (Ty : Set) where

  data Cxt : Set where
    sg : (A : Ty) → Cxt
    _∙_ : (Γ₁ Γ₂ : Cxt) → Cxt

  postulate Sub : Cxt → Cxt → Set

  variable Γ Δ : Cxt

  data Var (A : Ty) : Cxt → Set where
    •   : Var A (sg A)
    inl : (x : Var A Γ) → Var A (Γ ∙ Δ)

postulate
  T : ∀ {a} {A : Set a} → A → Set

  bla : T Γ

check-bla : {Ty : Set} {Γ : Cxt Ty} → T Γ
check-bla = bla


text:
module _ where

open import Common.Prelude

data Vec (A : Set) : Nat → Set where
  [] : Vec A 0
  _∷_ : ∀ {@0 n} → A → Vec A n → Vec A (suc n)

sum : ∀ {@0 n} → Vec Nat n → Nat
sum (x ∷ xs) = x + sum xs
sum [] = 0

foldl : ∀ {A} {B : Nat → Set} → (∀ {@0 n} → B n → A → B (suc n)) → B 0 → ∀ {@0 n} → Vec A n → B n
foldl {B = B} f z (x ∷ xs) = foldl {B = λ n → B (suc n)} f (f z x) xs
foldl f z [] = z

reverse : ∀ {A} {@0 n} → Vec A n → Vec A n
reverse = foldl {B = Vec _} (λ xs x → x ∷ xs) []

downFrom : ∀ n → Vec Nat n
downFrom zero = []
downFrom (suc n) = n ∷ downFrom n

main : IO Unit
main = printNat (sum (reverse (downFrom 100000)))

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
{-# OPTIONS --safe --without-K #-}
------------------------------------------------------------------------
-- Group objects in a cartesian category.
------------------------------------------------------------------------

open import Categories.Category
open import Categories.Category.Cartesian

module Categories.Object.Group {o ℓ e} {𝒞 : Category o ℓ e} (C : Cartesian 𝒞) where

open import Level

open import Categories.Category.BinaryProducts 𝒞 using (BinaryProducts)
open import Categories.Category.Cartesian.Monoidal
open import Categories.Object.Monoid (CartesianMonoidal.monoidal C)
open import Categories.Object.Terminal 𝒞

open Category 𝒞
open Cartesian C
module Π = BinaryProducts products
open BinaryProducts products using (_×_; _⁂_; ⟨_,_⟩)
open Terminal terminal

record IsGroup (G : Obj) : Set (ℓ ⊔ e) where
  -- any group object is also a monoid object
  field
    isMonoid : IsMonoid G

  open IsMonoid isMonoid public

  field
    -- inverse operation
    ι : G ⇒ G
    -- ι is in fact an inverse
    inverseˡ : η ∘ ! ≈ μ ∘ ⟨ ι , id ⟩
    inverseʳ : η ∘ ! ≈ μ ∘ ⟨ id , ι ⟩

record Group : Set (o ⊔ ℓ ⊔ e) where
  field
    Carrier : Obj
    isGroup : IsGroup Carrier

  open IsGroup isGroup public

  monoid : Monoid
  monoid = record { isMonoid = isMonoid }

open Group

record Group⇒ (G H : Group) : Set (ℓ ⊔ e) where
  field
    arr : Carrier G ⇒ Carrier H
    preserves-μ : arr ∘ μ G ≈ μ H ∘ (arr ⁂ arr)
    preserves-η : arr ∘ η G ≈ η H
    preserves-ι : arr ∘ ι G ≈ ι H ∘ arr

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --disable-positivity-check #-}

module univ where

import Logic.ChainReasoning
module Chain {A : Set}
             ( _==_ : A -> A -> Set)
             (refl : {x : A} -> x == x)
             (trans : {x y z : A} -> x == y -> y == z -> x == z) =
             Logic.ChainReasoning.Mono.Homogenous _==_ (\x -> refl) (\x y z -> trans)

data N1 : Set where
  T : N1

data N0 : Set where

data Sigma (A:Set)(B : A -> Set) : Set where
 Pair : (x:A) -> B x -> Sigma A B

rel : Set -> Set1

rel A = A -> A -> Set

pred : Set -> Set1

pred A = A -> Set

Refl : {A:Set} -> rel A -> Set
Refl {A} R = {x : A} -> R x x

Sym : {A:Set} -> rel A -> Set
Sym {A} R = {x y : A} -> R x y -> R y x

Trans : {A:Set} -> rel A -> Set
Trans {A} R = {x y z : A} -> R x y -> R y z -> R x z

Map : (A:Set) -> rel A -> (B:Set) -> rel B -> pred (A -> B)
Map A _R_ B _S_ f = {x y : A} -> x R y -> f x S f y

postulate
  N : Set
  _=N_ : rel N
  refN : Refl _=N_
  symN : Sym _=N_
  transN : Trans _=N_

-- mutual inductive recursive definition of S and the functions _=S_, El, eq, and all the
-- proofs on these functions

mutual

  infix 40 _==_ _=S_
  infixr 80 _<<_

  data S : Set where
    nat : S
    pi  : (A:S) -> (f:El A -> S) -> Map (El A) _==_ S _=S_ f -> S

  _=S'_ : rel S
  nat       =S' nat       = N1
  nat       =S' pi A f pf = N0
  pi _ _ _  =S' nat       = N0
  pi A F pF =S' pi B G pG =
      Sigma (A =S B) \ A=B -> (x : El B) -> F (A=B << x) =S G x

  data _=S_ (A B : S) : Set where
    eqS : A =S' B -> A =S B

  El' : S -> Set
  El' nat = N
  El' (pi A F pF) =
   Sigma ((x : El A) -> El (F x))
         \f -> {x y : El A}(x=y : x == y) ->
               f x == pF x=y << f y

  data El (A : S) : Set where
    el : El' A -> El A

  _=='_ : {A : S} -> rel (El A)
  _=='_ {nat} (el x) (el y) = x =N y
  _=='_ {pi A F pF} (el (Pair f pf)) (el (Pair g pg)) =
        (x : El A) -> f x == g x

  data _==_ {A : S}(x y : El A) : Set where
    eq : x ==' y -> x == y

  _<<_ : {A B : S} -> A =S B -> El B -> El A
  _<<_ {nat} {nat} p x = x
  _<<_ {pi A F pF} {pi B G pG} (eqS (Pair A=B F=G)) (el (Pair g pg)) =
    el (Pair f (\{x}{y} -> pf x y))
    where
      B=A = symS A=B

      F=Gc : (x : El A) -> F x =S G (B=A << x)
      F=Gc x =
        transS (transS refS (symS (pF (castlem A=B (symS A=B) x))))
        (F=G (symS A=B << x))

--         chain> F x
--            === F (A=B << B=A << x)  by symS (pF (castlem A=B B=A x))
--            === G (B=A << x)         by F=G (B=A << x)
--         where
--           open module C = Chain _=S_ refS transS

      f : (x : El A) -> El (F x)
      f x = F=Gc x << g (B=A << x)

      pf : (x y : El A)(p : x == y) -> f x == pF p << f y
      pf x y x=y = trans fx=ccgy ccgy=cfy
        where
          cx = B=A << x
          cy = B=A << y

          cx=cy : cx == cy
          cx=cy = p<< B=A x=y

          cgy : El (G cx)
          cgy = pG cx=cy << g cy

          gx=gy : g cx == cgy
          gx=gy = pg cx=cy

          ccgy : El (F x)
          ccgy = F=Gc x << cgy

          fx=ccgy : f x == ccgy
          fx=ccgy = p<< (F=Gc x) gx=gy

          cfy : El (F x)
          cfy = pF x=y << f y

          ccgy=cfy : ccgy == cfy
          ccgy=cfy = castlem2 (F=Gc x) (pF x=y)
                              (pG cx=cy) (F=Gc y)
                              (g cy)

  p<< : {A B : S}(A=B : A =S B) -> Map (El B) _==_ (El A) _==_ (_<<_ A=B)
  p<< {nat}{nat} _ x=y = x=y
  p<< {pi A F pF} {pi B G pG} (eqS (Pair A=B F=G))
        {el (Pair f pf)} {el (Pair g pg)} (eq f=g) = eq cf=cg
    where
      open module C = Logic.ChainReasoning.Mono.Homogenous _=S_ (\x -> refS) (\x y z -> transS)
      B=A = symS A=B

      F=Gc : (x : El A) -> F x =S G (B=A << x)
      F=Gc x =
        chain> F x
           === F (A=B << B=A << x)  by symS (pF (castlem A=B B=A x))
           === G (B=A << x)         by F=G _

      cf=cg : (x : El A) -> F=Gc x << f (B=A << x)
                         == F=Gc x << g (B=A << x)
      cf=cg x = p<< (F=Gc x) (f=g (B=A << x))

  p<< {nat}      {pi _ _ _} (eqS ()) _
  p<< {pi _ _ _} {nat}      (eqS ()) _

  refS : Refl _=S_
  refS {nat}       = eqS T
  refS {pi A F pF} = eqS (Pair refS \(x : El A) -> pF (castref refS x))

  transS : Trans _=S_
  transS {nat}{nat}{nat} p q = p
  transS {nat}{nat}{pi _ _ _}      _      (eqS ())
  transS {nat}{pi _ _ _}{_}       (eqS ()) _
  transS {pi _ _ _}{nat}{_}       (eqS ()) _
  transS {pi _ _ _}{pi _ _ _}{nat} _      (eqS ())
  transS {pi A F pF}{pi B G pG}{pi C H pH}
         (eqS (Pair A=B F=G)) (eqS (Pair B=C G=H)) =
         eqS (Pair A=C F=H)
    where
      open module C = Chain _=S_ refS transS
      A=C = transS A=B B=C
      F=H : (x : El C) -> F (A=C << x) =S H x
      F=H x =
        chain> F (A=C << x)
           === F (A=B << B=C << x) by symS (pF (casttrans A=B B=C A=C x))
           === G (B=C << x)        by F=G (B=C << x)
           === H x                 by G=H x

  symS : Sym _=S_
  symS {nat}{nat} p                 = p
  symS {pi _ _ _}{nat} (eqS ())
  symS {nat}{pi _ _ _} (eqS ())
  symS {pi A F pF}{pi B G pg} (eqS (Pair A=B F=G)) = eqS (Pair B=A G=F)
    where
      open module C = Chain _=S_ refS transS
      B=A = symS A=B
      G=F : (x : El A) -> G (B=A << x) =S F x
      G=F x =
        chain> G (B=A << x)
           === F (A=B << B=A << x) by symS (F=G (B=A << x))
           === F x                 by pF (castlem A=B B=A x)

  pfi : {A B : S}(p q : A =S B)(x : El B) -> p << x == q << x
  pfi {nat}{nat} _ _ x = ref
  pfi {nat}{pi _ _ _} (eqS ()) _ _
  pfi {pi _ _ _}{nat} (eqS ()) _ _
  pfi {pi A F pF}{pi B G pG} (eqS (Pair A=B1 F=G1)) (eqS (Pair A=B2 F=G2))
      (el (Pair f pf)) = eq f1=f2
    where
      B=A1 = symS A=B1
      B=A2 = symS A=B2

      f1=f2 : (x : El A) -> _ << f (B=A1 << x) == _ << f (B=A2 << x)
      f1=f2 x =
        chain> _ << f (B=A1 << x)
           === _ << _ << f (B=A2 << x) by p<< _ lem2
           === _ << f (B=A2 << x)      by casttrans _ _ _ _
        where
          open module C = Chain _==_ (ref {F x}) (trans {F x})
          lem1 : B=A1 << x == B=A2 << x
          lem1 = pfi B=A1 B=A2 x

          lem2 : f (B=A1 << x) == _ << f (B=A2 << x)
          lem2 = pf lem1

  castref : {A : S}(p : A =S A)(x : El A) -> p << x == x
  castref {nat} p x = ref
  castref {pi A F pF} (eqS (Pair A=A F=F)) (el (Pair f pf)) = eq cf=f
    where
      A=A' = symS A=A
      cf=f : (x : El A) -> _ << f (A=A' << x) == f x
      cf=f x =
        chain> Fx=Fcx << f (A=A' << x)
           === Fx=Fcx << _ << f x by p<< Fx=Fcx lem2
           === refS << f x        by casttrans _ _ _ (f x)
           === f x                by castref _ (f x)
        where
          Fx=Fcx = _
          open module C = Chain _==_ (ref {F x}) (trans {F x})
          lem1 : A=A' << x == x
          lem1 = castref A=A' x

          lem2 : f (A=A' << x) == _ << f x
          lem2 = pf lem1

  casttrans : {A B C : S}(A=B : A =S B)(B=C : B =S C)(A=C : A =S C)(x : El C) ->
               A=B << B=C << x == A=C << x
  casttrans {nat}{nat}{nat} _ _ _ x = ref
  casttrans {nat}{nat}{pi _ _ _}      _      (eqS ()) _ _
  casttrans {nat}{pi _ _ _}{_}       (eqS ()) _ _ _
  casttrans {pi _ _ _}{nat}{_}       (eqS ()) _ _ _
  casttrans {pi _ _ _}{pi _ _ _}{nat} _      (eqS ()) _ _
  casttrans {pi A F pF}{pi B G pG}{pi C H pH}
            (eqS (Pair A=B F=G))(eqS (Pair B=C G=H))(eqS (Pair A=C F=H))
            (el (Pair h ph)) = eq prf
    where
      B=A = symS A=B
      C=B = symS B=C
      C=A = symS A=C

      prf : (x : El A) -> _ << _ << h (C=B << B=A << x) == _ << h (C=A << x)
      prf x =
        chain> Fx=Gcx << Gcx=Hccx << h (C=B << B=A << x)
           === Fx=Hccx << h (C=B << B=A << x) by casttrans _ _ _ _
           === Fx=Hccx << _ << h (C=A << x) by p<< _ (ph (casttrans C=B B=A C=A x))
           === Fx=Hcx << h (C=A << x)  by casttrans _ _ _ _
        where
          Fx=Gcx   = _
          Gcx=Hccx = _
          Fx=Hccx  = transS (lemF=Gc A=B pF pG F=G _)
                            (lemF=Gc B=C pG pH G=H _)
          Fx=Hcx   = _
          open module C = Chain _==_ (ref {F x}) (trans {F x})

  lemF=Gc : {A B : S}(A=B : A =S B)
            {F : El A -> S}(pF : Map (El A) _==_ S _=S_ F)
            {G : El B -> S}(pG : Map (El B) _==_ S _=S_ G)
            (F=G : (x : El B) -> F (A=B << x) =S G x)
            (x : El A) -> F x =S G (symS A=B << x)
  lemF=Gc A=B {F} pF {G} pG F=G x =
    chain> F x
       === F (A=B << B=A << x)  by symS (pF (castlem A=B B=A x))
       === G (B=A << x)         by F=G _
    where
      open module C = Chain _=S_ refS transS
      B=A = symS A=B

  castlem : {A B : S}(p : A =S B)(q : B =S A)(x : El A) ->
            p << q << x == x
  castlem {A}{B} p q x =
    chain> p << q << x
       === refS << x  by casttrans p q refS x
       === x          by castref refS x
    where open module C = Chain _==_ (ref {A}) (trans {A})

  castlem2 : {A B B' C : S}(A=B : A =S B)(A=B' : A =S B')(B=C : B =S C)(B'=C : B' =S C)
             (x : El C) ->
             A=B << B=C << x == A=B' << B'=C << x
  castlem2 {A} p p' q q' x =
    chain> p << q       << x
       === transS p  q  << x  by casttrans _ _ _ x
       === transS p' q' << x  by pfi _ _ _
       === p' << q'     << x  by sym (casttrans _ _ _ x)
    where open module C = Chain _==_ (ref {A}) (trans {A})

  ref : {A:S} -> Refl {El A} _==_
  ref {nat}      {el n}           = eq refN
  ref {pi A F pF}{el (Pair f pf)} = eq f=f
    where
      f=f : (x : El A) -> f x == f x
      f=f x = ref

  trans : {A:S} -> Trans {El A} _==_
  trans {nat}{el x}{el y}{el z} (eq p) (eq q) = eq (transN p q)
  trans {pi A F pF}{el (Pair f pf)}{el (Pair g pg)}{el (Pair h ph)}
        (eq f=g)(eq g=h) = eq f=h
    where
      f=h : (x : El A) -> f x == h x
      f=h x = trans (f=g x) (g=h x)

  sym : {A:S} -> Sym {El A} _==_
  sym {nat}{el x}{el y} (eq p)  = eq (symN p)
  sym {pi A F pF}{el (Pair f pf)}{el (Pair g pg)}
        (eq f=g) = eq g=f
    where
      g=f : (x : El A) -> g x == f x
      g=f x = sym (f=g x)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module _ where

open import utility

open import Function using (_∘_)
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction
  using (Canₛ ; Canₛₕ)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; module SigMap ; module ShrMap ; module VarMap ; []env ; sig-stats ; Dom)
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Context.Properties
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open import Relation.Nullary
  using (¬_ ; yes ; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl)
open import Data.Empty
  using (⊥ ; ⊥-elim)
import Data.FiniteMap
open import Data.List
  using (List ; _∷_ ; [] ; _++_)
open import Data.List.All as All
  using (All ; _∷_ ; [])
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; proj₁ ; proj₂ ; _×_ ; _,′_ ; ∃ )
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Relation.Binary.PropositionalEquality
open import Esterel.Lang.Binding
-- open import coherence
open import blocked
open import sn-calculus
open import par-swap
open import calculus

open _≐_⟦_⟧e
open _≐_⟦_⟧c

open EvaluationContext1
open Context1

open import Data.Maybe

sn≡ₑ-context : ∀ p q C ->
             (∀ p BVp FVp -> CorrectBinding p BVp FVp -> CB (C ⟦ p ⟧c)) ->
             p sn≡ₑ q -> (C ⟦ p ⟧c) sn≡ₑ (C ⟦ q ⟧c)
sn≡ₑ-context p q C CBfill (rstp psn⟶q) = rstp (Context-sn⟶⟦⟧ C psn⟶q)
sn≡ₑ-context p q C CBfill (rsym{p = .q}{BV = BV} {FV} psn≡ₑq CBq) with sn≡ₑ-context q p C CBfill psn≡ₑq
... | C⟦q⟧csn≡ₑC⟦p⟧c = rsym C⟦q⟧csn≡ₑC⟦p⟧c (CBfill q BV FV CBq)
sn≡ₑ-context p .p C _ rref = rref
sn≡ₑ-context p q C CBfill (rtrn{r = r} psn≡ₑr rsn≡ₑq) with
    sn≡ₑ-context p r C CBfill psn≡ₑr | sn≡ₑ-context r q C CBfill rsn≡ₑq
... | C⟦p⟧csn≡ₑC⟦r⟧c | C⟦r⟧csn≡ₑC⟦q⟧c = rtrn {r = C ⟦ r ⟧c} C⟦p⟧csn≡ₑC⟦r⟧c C⟦r⟧csn≡ₑC⟦q⟧c

sn≡ₑ-sn⟶* : ∀ {p q} -> p sn⟶* q -> p sn≡ₑ q
sn≡ₑ-sn⟶* rrefl = rref
sn≡ₑ-sn⟶* (rstep psn⟶q psn⟶*q) = rtrn (rstp psn⟶q) (sn≡ₑ-sn⟶* psn⟶*q)

≡ₑ-context :
  ∀ {p q} -> ∀ C1 C2 ->
   (∀ {r r′ BVp FVp} -> CorrectBinding r BVp FVp -> r′ ≐ C2 ⟦ r ⟧c -> CB r′) ->
   p ≡ₑ q # C1 ->
   p ≡ₑ q # (C2 ++ C1)
≡ₑ-context C C′ CBfill ≡ₑrefl = ≡ₑrefl
≡ₑ-context C C′ CBfill (≡ₑtran p≡ₑr r≡ₑq)
  with ≡ₑ-context C C′ CBfill p≡ₑr
... | p≡ₑr#C
  with ≡ₑ-context C C′ CBfill r≡ₑq
... | r≡ₑq#C = ≡ₑtran p≡ₑr#C r≡ₑq#C
≡ₑ-context C C′ CBfill (≡ₑsymm{q = q} CBq p≡ₑq)
  with ≡ₑ-context C C′ CBfill p≡ₑq
... | q≡ₑp#C = ≡ₑsymm (CBfill CBq (++-is-nesting C′ C _)) q≡ₑp#C
≡ₑ-context C1 C2 CBfill (≡ₑctxt{_}{C''} C′⟦p⟧≐C′⟦p⟧c C′⟦q⟧≐C′⟦q⟧c p≡ₑq)
  with ≡ₑ-context (C1 ++ C'') C2  wrapCBfill p≡ₑq where
      wrapCBfill : ∀ {r r′ BVp FVp} ->
        CorrectBinding r BVp FVp ->
        r′ ≐ C2 ⟦ r ⟧c ->
        CB r′
      wrapCBfill{r} CB C′⟦r⟧c = CBfill CB C′⟦r⟧c
... | p≡ₑq#[C′++C++C''] rewrite sym (++-assoc C2 C1 C'')
  =  ≡ₑctxt C′⟦p⟧≐C′⟦p⟧c C′⟦q⟧≐C′⟦q⟧c p≡ₑq#[C′++C++C'']
≡ₑ-context C C′ CBfill (≡ₑstep p⟶₁q)
  = ≡ₑstep p⟶₁q

θ-present-signals : Env → List Signal
θ-present-signals θ = Data.List.mapMaybe (f ∘ _ₛ) DomS
  where
    DomS = (fst (Env.Dom θ))
    f : Signal → Maybe Signal
    f S with (Env.Sig∈ S θ)
    ... | (no S∈) = nothing
    ... | (yes S∈) with sig-stats{S} θ S∈
    ... | Signal.present = just S
    ... | Signal.absent = nothing
    ... | Signal.unknown = nothing

get-signals : Term → List Signal
get-signals nothin = []
get-signals pause = []
get-signals (signl S p) = []
get-signals (present S ∣⇒ p ∣⇒ p₁) = []
get-signals (emit S) = []
get-signals (p ∥ p₁) = []
get-signals (loop p) = []
get-signals (loopˢ p q) = []
get-signals (p >> p₁) = []
get-signals (suspend p S) = []
get-signals (trap p) = []
get-signals (exit x) = []
get-signals (shared s ≔ e in: p) = []
get-signals (s ⇐ e) = []
get-signals (var x ≔ e in: p) = []
get-signals (x ≔ e) = []
get-signals (if x ∣⇒ p ∣⇒ p₁) = []
get-signals (ρ⟨ θ , A ⟩· p) = θ-present-signals θ

data eval-result : Set where
   output : List Signal → eval-result

data non-constructive : Env → Term → Set where
  nc : ∀{p θ} → (Σ (Env × Term) λ {(θq , q) → (ρ⟨ θ , GO ⟩· p) sn≡ₑ (ρ⟨ θq , GO ⟩· q) × (manifests-as-non-constructive θq GO q)})
              → non-constructive θ p

data evalsn≡ₑ : Term → Env → eval-result → Set where
   evalsn-complete : ∀{p q θ θq} →
     (ρθ·p≡q : (ρ⟨ θ , GO ⟩· p) sn≡ₑ (ρ⟨ θq , GO ⟩· q)) →
     (complete-q : complete (ρ⟨ θq , GO ⟩· q)) →
     evalsn≡ₑ p θ (output (get-signals (ρ⟨ θq , GO ⟩· q)))

data eval∥R∪sn≡ₑ : Term → Env → eval-result → Set where
   eval∥R∪sn-complete : ∀{p q θ θq} →
     (ρθ·p≡q : (ρ⟨ θ , GO ⟩· p) ∥R∪sn≡ₑ (ρ⟨ θq , GO ⟩· q)) →
     (complete-q : complete (ρ⟨ θq , GO ⟩· q)) →
     eval∥R∪sn≡ₑ p θ (output (get-signals (ρ⟨ θq , GO ⟩· q)))

data eval≡ₑ : Term → Env → eval-result → Set where
   eval-complete : ∀{p q θ θq} →
     (ρθ·p≡q : (ρ⟨ θ , GO ⟩· p) ≡ₑ (ρ⟨ θq , GO ⟩· q) # []) →
     (complete-q : complete (ρ⟨ θq , GO ⟩· q)) →
     eval≡ₑ p θ (output (get-signals (ρ⟨ θq , GO ⟩· q)))

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
-- The comonad named Store by Russel O'Connor.
-- See his WGP 2011 paper.

{-# OPTIONS --copatterns #-}

module Control.Comonad.Store where

open import Function using (id) renaming (_∘′_ to _∘_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
open ≡-Reasoning

open import Axiom.FunctionExtensionality
open import Util.Equality

open import Control.Functor
open import Control.Functor.NaturalTransformation
open import Control.Comonad

-- The Store comonad.

record Store (I O : Set) : Set where
  constructor store
  field
    peek : I → O
    pos  : I

  extract : O
  extract = peek pos

{- not in scope: store
  extend′ : ∀ {B} → (Store I O → B) → Store I B
  extend′ f = store (f ∘ store peek) pos
-}

  extend′ : ∀ {B} → (Store I O → B) → Store I B
  pos  (extend′ f) = pos
  peek (extend′ f) = f ∘ s
    where
      s : I → Store I O
      peek (s i) = peek
      pos  (s i) = i

storeIsComonad : ∀ I → IsComonad (Store I)
storeIsComonad I = record
  { extract  = extract
  ; extend   = extend
  ; extend-β = refl
  ; extend-η = refl
  ; extend-∘ = refl
  }
  where
    extract : ∀ {O} → Store I O → O
    extract (store v i) = v i

    extend : ∀ {A B} → (Store I A → B) → Store I A → Store I B
    extend f (store v i) = store (f ∘ store v) i

    extend-β : ∀ {A B} (f : Store I A → B) → extract ∘ extend f ≡ f
    extend-β f = refl

StoreC : ∀ I → Comonad
StoreC I = comonad (Store I) (storeIsComonad I)

-- Functoriality,

storeIsFunctor : ∀ I → IsFunctor (Store I)
storeIsFunctor I = IsComonad.isFunctor (storeIsComonad I)

StoreF : (I : Set) → Functor
StoreF I = functor (Store I) (storeIsFunctor I)

idLens : ∀ {I} → I → Store I I
idLens = store id

-- Van Laarhoven presentation

record LStore (I O : Set) : Set₁ where
  -- constructor lstore
  field
    modifier : (FF : Functor) → let open Functor FF in
               (I → F I) → F O

  -- Laws.

  -- 0. Free theorem.
  field
    modifier-free : {FF GG : Functor} (N : NatTrans FF GG) →
      let open Functor FF using () renaming (F   to F) in
      let open Functor GG using () renaming (F   to G) in
      let open NatTrans N using () renaming (eta to η) in
      (f : I → F I) →

        η (modifier FF f) ≡ modifier GG (η ∘ f)

  -- 1. Identity

  -- modifier-id :

-- Converting between store comonads.

storeToLStore : ∀ {I O} → Store I O → LStore I O
storeToLStore {I = I} {O = O} (store v i) = record
  { modifier      = modifier
  ; modifier-free = modifier-free
  }
  where
    modifier : (FF : Functor) → let open Functor FF in
               (I → F I) → F O
    modifier FF f = map v (f i)
      where open Functor FF

    modifier-free : {FF GG : Functor} (N : NatTrans FF GG) →
      let open Functor FF using () renaming (F   to F) in
      let open Functor GG using () renaming (F   to G) in
      let open NatTrans N using () renaming (eta to η) in
      (f : I → F I) →

        η (modifier FF f) ≡ modifier GG (η ∘ f)

    modifier-free {FF = FF}{GG = GG} N f = begin
        η (modifier FF f)   ≡⟨⟩
        (η ∘ mapF v) (f i)  ≡⟨ app-≡ (f i) (naturality _) ⟩
        (mapG v ∘ η) (f i)  ≡⟨⟩
        modifier GG (η ∘ f) ∎

      where
        open Functor FF using () renaming (F to F; map to mapF; map-id to mapF-id; map-∘ to mapF-∘)
        open Functor GG using () renaming (F to G; map to mapG; map-id to mapG-id; map-∘ to mapG-∘)
        open NatTrans N using (naturality) renaming (eta to η)

lstoreToStore : ∀ {I O} → LStore I O → Store I O
lstoreToStore {I = I} {O = O} l = LStore.modifier l (StoreF I) idLens

-- Isomorphism.

storeId : ∀ {I O} (s : Store I O) → lstoreToStore (storeToLStore s) ≡ s
storeId {I = I}{O = O} (store v i) = begin
  lstoreToStore (storeToLStore (store v i))                      ≡⟨⟩
  LStore.modifier (storeToLStore (store v i)) (StoreF I) idLens  ≡⟨⟩
  Functor.map (StoreF I) v (idLens i)                            ≡⟨⟩
  Functor.map (StoreF I) v (store id i)                          ≡⟨⟩
  store (v ∘ id) i                                               ≡⟨⟩
  store v i ∎

-- -- BAD IDEA: the proof of modifier-free should not be compared with ≡

-- lstoreId : ∀ {I O} (l : LStore I O) → storeToLStore (lstoreToStore l) ≡ l
-- lstoreId {I = I}{O = O} l = begin
--    storeToLStore (lstoreToStore l)             ≡⟨⟩
--    storeToLStore (modifier (StoreF I) idLens)  ≡⟨⟩
--    storeToLStore (modifier (StoreF I) idLens)  ≡⟨ {!!} ⟩
--    l                                           ∎
--   where open LStore l

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
module z04-lists where

open import bool
open import eq
open import nat
open import nat-thms
open import product-thms using (keep)
open import logic -- needed for filter-idem

{-
-- p 75

'data' : datatype declaration
'𝕃'    : name of type being declared
{ℓ}    : level
A      : element type (polymorphic)

𝕃 is a type level function
- takes a type (bound to 'A') - at level ℓ
- returns a type - at level same level ℓ
-}

data  𝕃 {ℓ} (A : Set ℓ) : Set ℓ where
  []   :                      𝕃 A
  _::_ : (x : A) (xs : 𝕃 A) → 𝕃 A

-- from lists.agda

[_] : ∀ {ℓ} {A : Set ℓ} → A → 𝕃 A
[ x ] = x :: []

-- p 77

length : ∀ {ℓ} {A : Set ℓ } → 𝕃 A → ℕ
length       []  = 0
length (x :: xs) = suc (length xs)

-- 78

_++_ : ∀ {ℓ} {A : Set ℓ} → 𝕃 A → 𝕃 A → 𝕃 A
[]        ++ ys =             ys
(x :: xs) ++ ys = x :: (xs ++ ys)

-- 79

map : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'}  → (A → B) → 𝕃 A → 𝕃 B
map f       []  = []
map f (x :: xs) = f x :: map f xs

-- 80

filter : ∀ {ℓ} {A : Set ℓ} → (A → 𝔹) → 𝕃 A → 𝕃 A
filter p       []  = []
filter p (x :: xs) = if p x then x :: r else r
 where
  r = filter p xs

-- p 81

remove : ∀ {ℓ} {A : Set ℓ} (eq : A → A → 𝔹) (a : A) (l : 𝕃 A) → 𝕃 A
remove eq a l = filter (λ x → ~ (eq a x)) l

-- p 82

data maybe {ℓ} (A : Set ℓ) : Set ℓ where
  just    : A → maybe A
  nothing :     maybe A

nth : ∀ {ℓ} {A : Set ℓ} → ℕ → 𝕃 A → maybe A
nth _             []  = nothing
nth 0       (x :: xs) = just x
nth (suc n) (x :: xs) = nth n xs

-- p 83

-- inefficient
sreverse : ∀ {ℓ} {A : Set ℓ} → 𝕃 A → 𝕃 A
sreverse      []  = []
sreverse (h :: t) = sreverse t ++ [ h ]

reverse-helper : ∀ {ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A → 𝕃 A
reverse-helper h       []  = h
reverse-helper h (x :: xs) = reverse-helper (x :: h) xs

reverse : ∀ {ℓ} {A : Set ℓ} → 𝕃 A → 𝕃 A
reverse l = reverse-helper [] l

------------------------------------------------------------------------------
-- p 84 Reasong about List Operations

length-++ : ∀ {ℓ}{A : Set ℓ} (l1 l2 : 𝕃 A)
          → length (l1 ++ l2) ≡ length l1 + length l2
length-++ [] l2 -- length ([] ++ l2) ≡ length [] + length l2
                -- length        l2  ≡             length l2
  = refl
length-++ (x :: xs) l2 --      length ((x :: xs) ++ l2)  ≡      length (x :: xs) + length l2
                       -- suc (length       (xs  ++ l2)) ≡ suc (length       xs  + length l2)
                       --                 |
  rewrite              -- IH              ≡
                       --                 v
    length-++ xs l2    -- suc (length  xs +  length l2)  ≡ suc (length       xs  + length l2)
  = refl

-- p 86

++-assoc : ∀ {ℓ} {A : Set ℓ} (l1 l2 l3 : 𝕃 A)
         → (l1 ++  l2) ++ l3
         ≡  l1 ++ (l2  ++ l3)
++-assoc [] l2 l3                  -- (([] ++ l2) ++ l3) ≡ ([] ++ (l2 ++ l3))
                                   --        (l2  ++ l3) ≡        (l2 ++ l3)
  = refl
++-assoc (x :: xs) l2 l3 -- (((x ::   xs) ++ l2) ++ l3)   ≡ ((x ::  xs) ++ (l2 ++ l3))
                         --   (x :: ((xs  ++ l2) ++ l3))  ≡  (x :: (xs  ++ (l2 ++ l3)))
  rewrite                -- IH               v
    ++-assoc xs l2 l3    --   (x ::  (xs ++ (l2  ++ l3))) ≡  (x :: (xs  ++ (l2 ++ l3)))
  = refl

{-
------------------------------------------------------------------------------
-- p 87 - WITH

for
- any type A (of any level),
- any predicate p on A
- any list of A
the length of the list after filtering l with p
<=
length of l
-}

length-filter : ∀ {ℓ} {A : Set ℓ} (p : A → 𝔹) (l : 𝕃 A)
              → length (filter p l) ≤ length l ≡ tt

-- proof case-splits input list

length-filter p      []         -- length (filter p []) ≤ length [] ≡ tt
                                --                   0  ≤         0 ≡ tt
  = refl

-- Consider cases where predicate returns tt or ff.
-- The predicate return value is NOT an input to length-filter.
-- WITH : extend pattern on left side with an additional pattern, here : | tt     and   | ff

length-filter p (x :: l) with p x
length-filter p (x :: l) | tt   --    length (filter p l)  <      length l
                                -- || length (filter p l) =ℕ      length l  ≡ tt
  = length-filter p l           -- IH
length-filter p (x :: l) | ff   --    length (filter p l)  < suc (length l)
  =                             -- || length (filter p l) =ℕ suc (length l) ≡ tt
  ≤-trans {length (filter p l)}
          (length-filter p l)   -- IH
          (≤-suc (length l))    -- ≤-suc proves length l ≤ suc (length l)

{- this is to see the goal for the non-nil case
lf : ∀ {ℓ} {A : Set ℓ} (p : A → 𝔹) (l : 𝕃 A)
   → length (filter p l) ≤ length l ≡ tt
lf p      []  = refl
lf p (x :: l) -- length                  (filter p (x :: l))                ≤      length (x :: l) ≡ tt
              -- length (if p x then x :: filter p       l else filter p l) ≤ suc (length       l) ≡ tt
  = {!!}

------------------------------------------------------------------------------
-- p 90 KEEP (called INSPECT in Agda standard library)

filtering a list twice using same predicate gives the same result as filtering it once

cannot use WITH because Agda only applies the p ≡ tt to the goal once, not the next iteration
(see page 92 for more details)

'with keep (p x)' : make additional variable (here p') available
-}

filter-idem : ∀ {ℓ} {A : Set ℓ} (p : A → 𝔹) (l : 𝕃 A)
            → (filter p (filter p l)) ≡ (filter p l)
filter-idem p []            -- filter p (filter p []) ≡ filter p []
                            --                    []  ≡          []
  = refl
{-
filter-idem p (x :: l)           -- filter p (filter p (x :: l)) ≡ filter p (x :: l)
                                 --
                                 -- filter p (if p x then x :: filter p l else filter p l)
                                 -- ≡ if p x then x :: filter p l else filter p l
  = {!!}
-}
filter-idem p (x :: l) with keep (p x)

filter-idem p (x :: l) | tt , p' -- filter p (if p x then x :: filter p l else filter p l)
                                 -- ≡ if p x then x :: filter p l else filter p l

  rewrite
    -- agda does not instantiate 'p x' in goal
    -- must explicit use it below to change 'p x' to 'tt' (or 'ff' further below)

    p'                           -- filter p (if tt then x :: filter p l else filter p l)
                                 -- ≡ if tt then x :: filter p l else filter p l
                                 --
                                 --   if p x then x :: filter p (filter p l) else filter p (filter p l)
                                 -- ≡ (x :: filter p l)

  -- use it again to eliminate the if

  | p'                           --   if tt  then x :: filter p (filter p l) else filter p (filter p l)
                                 -- ≡ (x :: filter p l)
                                 --
                                 --   (x :: filter p (filter p l)) ≡ (x :: filter p l)

  | filter-idem p l              --   (x :: filter p l) ≡ (x :: filter p l)
  = refl

filter-idem p (x :: l) | ff , p' -- filter p (if p x then x :: filter p l else filter p l)
                                 -- ≡ if p x then x :: filter p l else filter p l

  rewrite p'                     -- filter p (if ff then x :: filter p l else filter p l)
                                 -- ≡ if ff  then x :: filter p l else filter p l
                                 --
                                 -- filter p (filter p l) ≡ filter p l
  = filter-idem p l

{-
------------------------------------------------------------------------------
-- p 93

reverse-helper args
- reverse of the list processed so far
- rest of list to be reversed

tricky to figure out what general property of reverse-helper to prove
-length of reverse-helper h l is sum of lengths of h and l
-}

length-reverse-helper
  : ∀ {ℓ} {A : Set ℓ} (h l : 𝕃 A)
  → length (reverse-helper h l) ≡ length h + length l

length-reverse-helper h []                     -- length (reverse-helper h []) ≡ length h + length []
                                               -- length h                     ≡ length h + 0
  rewrite
    +comm (length h) 0                         -- length h                     ≡ length h
  -- also can do via
  -- rewrite +0 (length h) = refl
  = refl
length-reverse-helper h (x :: xs)
                                               -- length (reverse-helper h (x :: xs)) ≡ length h + length (x :: xs)
                                               -- length (reverse-helper (x :: h) xs) ≡ length h + suc (length xs)
  rewrite
    length-reverse-helper (x :: h) xs -- IH    --          suc (length h + length xs) ≡ length h + suc (length xs)
  | +suc (length h) (length xs)                --          suc (length h + length xs) ≡ suc (length h + length xs)
  = refl

length-reverse : ∀ {ℓ} {A : Set ℓ} (l : 𝕃 A)
               → length (reverse l) ≡ length l
length-reverse l = length-reverse-helper [] l

{-
------------------------------------------------------------------------------
-- p 95  conclusion : WITH     and    KEEP (aka INSPECT)

-- p 96 EXERCISES

-- 1
-}

-------------------------
-- NOT TRUE
-- 1a : ∀ {ℓ} {A : Set ℓ} (l1 l2 : 𝕃 A) → l1 ++ l2 ≡ l2 ++ l1

-------------------------
-- NOT TRUE
-- 1b : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (l : 𝕃 A) → length (map f l) ≡ suc (length l)

-------------------------
-- 1c: TRUE

repeat : ∀ {ℓ} {A : Set ℓ} → ℕ → A → 𝕃 A
repeat 0 a = []
repeat (suc n) a = a :: (repeat n a)

1c : ∀ {ℓ} {A : Set ℓ} {p : A → 𝔹} {a : A} (n : ℕ)
   → p a ≡ ff
   → filter p (repeat n a) ≡ []
1c 0 prop            -- filter p (repeat zero a) ≡ []
                     --                       [] ≡ []
  = refl
1c (suc n) prop      -- filter p (repeat (suc n) a) ≡ []
                     -- if p a then a :: filter p (repeat n a) else filter p (repeat n a) ≡ []
  rewrite
    prop             -- if ff  then a :: filter p (repeat n a) else filter p (repeat n a) ≡ []
                     --                                             filter p (repeat n a) ≡ []
  = 1c n prop -- IH

-------------------------
-- NOT TRUE
-- 1d : ∀ {ℓ} {A : Set ℓ} (l : 𝕃 A) → is-empty l ≡ tt → is-empty (reverse l) ≡ ff

-------------------------
-- TRUE
1e : ∀ {ℓ} {A : Set ℓ} (p : A -> 𝔹) (l1 l2 : 𝕃 A)
   → filter p (l1 ++          l2)
   ≡ filter p  l1 ++ filter p l2
1e p       []  l2               -- filter p ([] ++ l2) ≡ (filter p [] ++ filter p l2)
                                -- filter p        l2  ≡  filter p                l2
  = refl
1e p (x :: xs) l2 with keep (p x)
1e p (x :: xs) l2 | tt , p' --     if p x then x :: filter p (xs ++ l2) else filter p (xs ++ l2)
                            -- ≡ ((if p x then x :: filter p xs else filter p xs) ++ filter p l2)
  rewrite
    p'                      --     if tt  then x :: filter p (xs ++ l2) else filter p (xs ++ l2)
                            -- ≡ ((if tt  then x :: filter p xs else filter p xs) ++ filter p l2)
                            --
                            --   (x ::  filter p (xs ++          l2))
                            -- ≡ (x :: (filter p  xs ++ filter p l2))

  | 1e p xs l2              --   (x :: (filter p  xs ++ filter p l2))
                            -- ≡ (x :: (filter p  xs ++ filter p l2))
  = refl
1e p (x :: xs) l2 | ff , p' --     if p x then x :: filter p (xs ++ l2) else filter p (xs ++ l2)
                            -- ≡ ((if p x then x :: filter p xs else filter p xs) ++ filter p l2)
  rewrite
    p'                      --     if ff  then x :: filter p (xs ++ l2) else filter p (xs ++ l2)
                            -- ≡ ((if ff  then x :: filter p xs else filter p xs) ++ filter p l2)
                            --
                            -- filter p (xs ++ l2) ≡ (filter p xs ++ filter p l2)
  = 1e p xs l2              -- IH

--------------------------------------------------
-- 2

-------------------------
-- 2a [] : 𝕃 Set  (𝕃 _A_277)

-------------------------
2b : ∀ {ℓ} {A : Set ℓ} → 𝕃 A → ℕ
2b       []  = 0
2b (x :: xs) = suc (2b xs)

-------------------------
-- Note: 2ci does not explicitly give ℓ
-- Note: some other answers are probably OK - did not check
2c : ∀ {ℓ} {A : Set ℓ} {B : Set ℓ} {C : Set ℓ}
   → (A → B)
   → (B → C)
   → 𝕃 A
   → 𝕃 C
2c f g x = map g (map f x)

--------------------------------------------------
-- 3

takeWhile : ∀ {ℓ} {A : Set ℓ} → (A → 𝔹) -> 𝕃 A → 𝕃 A
takeWhile p       []  = []
takeWhile p (x :: xs) = if p x then x :: takeWhile p xs else takeWhile p xs

--------------------------------------------------
-- 4

4twr : ∀ {ℓ} {A : Set ℓ} {p : A → 𝔹} {a : A} (n : ℕ)
     → p a ≡ tt
     → takeWhile p (repeat n a) ≡ repeat n a
4twr  zero p               -- takeWhile p₁ (repeat zero a) ≡ repeat zero a
                           --                           [] ≡ []
  = refl
4twr {l} {A} {pred} {a} (suc n) p -- takeWhile p₁ (repeat (suc n) a) ≡ repeat (suc n) a
                                  --   if p₁ a then a :: takeWhile p₁ (repeat n a) else takeWhile p₁ (repeat n a)
                                  -- ≡             (a ::               repeat n a)
  rewrite
    p                             --   if tt   then a :: takeWhile p₁ (repeat n a) else takeWhile p₁ (repeat n a)
                                  -- ≡             (a ::               repeat n a)
                                  --               (a :: takeWhile p₁ (repeat n a))
                                  -- ≡             (a ::               repeat n a)
  | 4twr {l} {A} {pred} {a} n p   --               (a ::               repeat n a) ≡ (a :: repeat n a)
  = refl

--------------------------------------------------
-- 5

take    : ∀ {ℓ} {A : Set ℓ} → ℕ → 𝕃 A → 𝕃 A
take         0         _  = []
take         _        []  = []
take    (suc n) (x :: xs) = x :: take n xs

--------------------------------------------------
-- 6

nthTail : ∀ {ℓ} {A : Set ℓ} → ℕ → 𝕃 A → 𝕃 A
nthTail      0        xs  = xs
nthTail      _        []  = []
nthTail (suc n) (x :: xs) = nthTail n xs
{-
6tn : ∀ {ℓ} {A : Set ℓ} {a : A} (n : ℕ) (l : 𝕃 A)
    → take n l ++ nthTail n l ≡ l
6tn  zero   l              -- (take zero l ++ nthTail zero l) ≡ l
                           --                             l  ≡ l
  = refl
6tn {ℓ} {A} {a} (suc n) l  -- (take (suc n) l ++ nthTail (suc n) l) ≡ l
  rewrite
    6tn {ℓ} {A} {a} n l
  = {!!}
-}

6tn : ∀ {ℓ} {A : Set ℓ} {a : A} (n : ℕ) (l : 𝕃 A)
    → take n l ++ nthTail n l ≡ l
6tn               zero        []  --       (take zero      []      ++ nthTail   zero        []) ≡ []
                                  --                                                        []  ≡ []
  = refl
6tn             (suc n)       []  --       (take (suc n)       []  ++ nthTail (suc n)       [])  ≡ []
                                  --                                                        []   ≡ []
  = refl
6tn               zero  (x :: xs) --       (take   zero  (x :: xs) ++ nthTail   zero  (x :: xs)) ≡ (x :: xs)
                                  -- (x :: xs)  ≡ (x :: xs)
  = refl
6tn {ℓ} {A} {a} (suc n) (x :: xs) --       (take (suc n) (x :: xs) ++ nthTail (suc n) (x :: xs)) ≡ (x :: xs)
                                  -- (x :: (take      n        xs  ++ nthTail      n        xs)) ≡ (x :: xs)
  rewrite
    6tn {ℓ} {A} {a} n xs          -- (x :: xs)                                                   ≡ (x :: xs)
  = refl

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

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

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


text:
-- {-# OPTIONS -v tc.proj.like:10 #-}
-- {-# OPTIONS -v tc.conv:10 #-}
open import Common.Level

module ProjectionLikeAndModules (A : Set) (a : A) where

record ⊤ : Set where
  constructor tt

data Wrap (W : Set) : Set where
  wrap : W → Wrap W

data Bool : Set where
  true false : Bool

-- postulate

-- `or' should be projection like in the module parameters
if : Bool → {ℓ : Level} {B : Set ℓ} → B → B → B
if true  a b = a
if false a b = b

postulate
  u v : ⊤
  P : {ℓ : Level} {C : Set ℓ} (c : C) -> Set

test : (y : Bool)
  -> P (if y (wrap u) (wrap tt))
  -> P (if y (wrap tt) (wrap v))
test y h = h

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Conversion.hs:536