text:
{-
Joseph Eremondi
Utrecht University Capita Selecta
UU# 4229924
July 22, 2015
-}

module RETypes where

open import Data.Char
open import Data.List
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Data.Product

--Tag for whether an RE can match the empty string or not
data Null? : Set where
  NonNull : Null?
  MaybeNull : Null?

--Equivalent of AND for Nullable
data NullTop : Null? -> Null? -> Null? -> Set where
  BothNullT : NullTop MaybeNull MaybeNull MaybeNull
  LeftNullT : NullTop MaybeNull NonNull NonNull
  RightNullT : NullTop NonNull MaybeNull NonNull
  BothNonNullT : NullTop NonNull NonNull NonNull

--Equivalent of OR for null
data NullBottom : Null? -> Null? -> Null? -> Set where
  BothNullB : NullBottom NonNull NonNull NonNull
  LeftNullB : NullBottom MaybeNull NonNull MaybeNull
  RightNullB : NullBottom NonNull MaybeNull MaybeNull
  BothNonNullB : NullBottom MaybeNull MaybeNull MaybeNull

--Standard definition of regular expressions
--plus nullable tags. Star can only accept non-nullable REs.
data RE : Null? -> Set where
  ε : RE MaybeNull
  ∅ : RE NonNull
  Lit : Char -> RE NonNull
  --Union is nullable if either input is nullable
  _+_ : {n1 n2 n3 : Null? }
    -> {nb : NullBottom n1 n2 n3}
    -> RE n1
    -> RE n2
    -> RE n3
  --Concatenation is nullable only if both inputs are nullable
  _·_ :  {n1 n2 n3 : Null? }
    -> {nt : NullTop n1 n2 n3}
    -> RE n1
    -> RE n2
    -> RE n3
  --Star always matches the empty string
  _* : RE NonNull -> RE MaybeNull

--Witness type, defining what it means for a word to match a regular expression
data REMatch : {n : Null?} -> List Char -> RE n -> Set where
  EmptyMatch : REMatch [] ε
  LitMatch : (c : Char) -> REMatch (c ∷ []) (Lit c)
  LeftPlusMatch :
    {n1 n2 n3 : Null? }
    -> {nb : NullBottom n1 n2 n3}
    -> {s : List Char} {r1 : RE n1}
    -> (r2 : RE n2)
    -> REMatch s r1
    -> REMatch {n3} s (_+_ {n1} {n2} {n3} {nb} r1 r2)
  RightPlusMatch :
    {n1 n2 n3 : Null? }
    -> {nb : NullBottom n1 n2 n3}
    -> {s : List Char} -> (r1 : RE n1) -> {r2 : RE n2}
    -> REMatch s r2
    -> REMatch {n3} s (_+_ {n1} {n2} {n3} {nb} r1 r2)
  ConcatMatch :
    {n1 n2 n3 : Null? }
    -> {nt : NullTop n1 n2 n3}
    -> {s1 s2 s3 : List Char} {spf : s1 ++ s2 ≡ s3} {r1 : RE n1} {r2 : RE n2}
    -> REMatch s1 r1
    -> REMatch s2 r2
    -> REMatch {n3} s3 (_·_ {n1} {n2} {n3} {nt} r1 r2)
  EmptyStarMatch : {r : RE NonNull} -> REMatch [] (r *)
  StarMatch :
    {s1 s2 s3 : List Char} {spf : (s1 ++ s2) ≡ s3} {r : RE NonNull}
    -> REMatch s1 r
    -> REMatch s2 (r *)
    -> REMatch s3 (r *)

extendRightNonNull : (s : List Char) -> (sRest : List Char) -> (∃ λ c -> ∃ λ t -> (s ≡ c ∷ t)) -> (∃ λ c1 -> ∃ λ t1 -> (s ++ sRest ≡ c1 ∷ t1))
extendRightNonNull .(c ∷ t) sRest (c , t , refl) = c , t ++ sRest , refl

extendLeftNonNull : (s : List Char) -> (sRest : List Char) -> (∃ λ c -> ∃ λ t -> (s ≡ c ∷ t)) -> (∃ λ c1 -> ∃ λ t1 -> (sRest ++ s ≡ c1 ∷ t1))
extendLeftNonNull .(t ∷ c) [] (t , c , refl) = t , c , refl
extendLeftNonNull .(t ∷ c) (x ∷ sRest) (t , c , refl)  = x , sRest ++ t ∷ c , refl

nullCorrect : (r : RE NonNull ) -> (s : List Char) -> REMatch s r -> ∃ λ c -> ∃ λ t -> (s ≡ c ∷ t)
nullCorrect .(Lit c) .(c ∷ []) (LitMatch c) = c , [] , refl
nullCorrect ._ s (LeftPlusMatch {nb = BothNullB} {r1 = r1} r2 match) = nullCorrect r1 s match
nullCorrect ._ s (RightPlusMatch {nb = BothNullB} r1 {r2 = r2} match) = nullCorrect r2 s match
nullCorrect (r1 · r2) s (ConcatMatch {nt = LeftNullT} {s2 = s2} match match₁) with nullCorrect r2 s2 match₁
nullCorrect (r1 · r2) .(s1 ++ c ∷ t) (ConcatMatch {.MaybeNull} {.NonNull} {.NonNull} {LeftNullT} {s1} {.(c ∷ t)} {.(s1 ++ c ∷ t)} {refl} match match₁) | c , t , refl = extendLeftNonNull (c ∷ t) s1 (c , t , refl)
nullCorrect (r1 · r2) ._ (ConcatMatch {nt = RightNullT} {s1 = s1} {spf = refl} match match₁) with nullCorrect r1 s1 match
nullCorrect (r1 · r2) .((c ∷ t) ++ s2) (ConcatMatch {.NonNull} {.MaybeNull} {.NonNull} {RightNullT} {.(c ∷ t)} {s2} {.((c ∷ t) ++ s2)} {refl} match match₁) | c , t , refl = extendRightNonNull (c ∷ t) s2 (c , t , refl)
nullCorrect (r1 · r2) s (ConcatMatch {nt = BothNonNullT} {s1 = s1} {s2 = s2} match match₁) with nullCorrect r1 s1 match
nullCorrect (r1 · r2) .(c ∷ t ++ s2) (ConcatMatch {.NonNull} {.NonNull} {.NonNull} {BothNonNullT} {.(c ∷ t)} {s2} {.(c ∷ t ++ s2)} {refl} match match₁) | c , t , refl = extendRightNonNull (c ∷ t) s2 (c , t , refl)

ext: agda

max_stars_repo_name: JoeyEremondi/agda-parikh

max_issues_repo_name: JoeyEremondi/agda-parikh

max_forks_repo_name: JoeyEremondi/agda-parikh


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Surjection
open import Oscar.Data.Proposequality

module Oscar.Class.Smap where

open import Oscar.Class.Hmap public

module Smap
  {𝔵₁ 𝔵₁'} {𝔛₁ : Ø 𝔵₁} {𝔛₁' : Ø 𝔵₁'}
  {𝔵₂ 𝔵₂'} {𝔛₂ : Ø 𝔵₂} {𝔛₂' : Ø 𝔵₂'}
  {𝔯₁₂} {𝔯₁₂'}
  (ℜ₁₂ : 𝔛₁ → 𝔛₂ → Ø 𝔯₁₂)
  (ℜ₁₂' : 𝔛₁' → 𝔛₂' → Ø 𝔯₁₂')
  (p₁ : 𝔛₁ → 𝔛₁')
  (p₂ : 𝔛₂ → 𝔛₂')
  where
  class = Hmap.class ℜ₁₂ (λ x y → ℜ₁₂' (p₁ x) (p₂ y))
  type = ∀ {x y} → ℜ₁₂ x y → ℜ₁₂' (p₁ x) (p₂ y)
  method : ⦃ _ : class ⦄ → type
  method = Hmap.method ℜ₁₂ (λ x y → ℜ₁₂' (p₁ x) (p₂ y)) _ _

module _
  {𝔵₁ 𝔯₁ 𝔵₂ 𝔯₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  {_∼₁_ : 𝔛₁ → 𝔛₁ → Ø 𝔯₁}
  (_∼₂_ : 𝔛₂ → 𝔛₂ → Ø 𝔯₂)
  (μ₁ μ₂ : Surjection.type 𝔛₁ 𝔛₂)
  where
  open Smap _∼₁_ _∼₂_ μ₁ μ₂
  smap⟦_/_/_⟧ : ⦃ _ : class ⦄ → type
  smap⟦_/_/_⟧ = smap

module ≡-Smap
  {𝔵₁ 𝔯₁ 𝔵₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (∼₁ : 𝔛₁ → 𝔛₁ → Ø 𝔯₁)
  (μ₁ μ₂ : Surjection.type 𝔛₁ 𝔛₂)
  = Smap ∼₁ _≡_ μ₁ μ₂

module _
  {𝔵₁ 𝔯₁ 𝔵₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  {_∼₁_ : 𝔛₁ → 𝔛₁ → Ø 𝔯₁}
  (μ₁ μ₂ : Surjection.type 𝔛₁ 𝔛₂)
  where
  open Smap _∼₁_ _≡_ μ₁ μ₂
  ≡-smap⟦_⟧ : ⦃ _ : class ⦄ → type
  ≡-smap⟦_⟧ = smap

module Smap!
  {𝔵₁ 𝔯₁ 𝔵₂ 𝔯₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (∼₁ : 𝔛₁ → 𝔛₁ → Ø 𝔯₁)
  (∼₂ : 𝔛₂ → 𝔛₂ → Ø 𝔯₂)
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  = Smap ∼₁ ∼₂ surjection surjection

module Smaparrow
  {𝔵₁ 𝔵₂ 𝔯 𝔭₁ 𝔭₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  (𝔓₁ : 𝔛₂ → Ø 𝔭₁)
  (𝔓₂ : 𝔛₂ → Ø 𝔭₂)
  (surjection₁ surjection₂ : Surjection.type 𝔛₁ 𝔛₂)
  = Smap ℜ (Arrow 𝔓₁ 𝔓₂) surjection₁ surjection₂

module _
  {𝔵₁ 𝔯 𝔭₁ 𝔭₂} {𝔛₁ : Ø 𝔵₁}
  {ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯}
  {𝔓₁ : 𝔛₁ → Ø 𝔭₁}
  {𝔓₂ : 𝔛₁ → Ø 𝔭₂}
  where
  smaparrow = Smaparrow.method ℜ 𝔓₁ 𝔓₂ ¡ ¡
  infixr 10 _◃_
  _◃_ = smaparrow
  smaparrow[]syntax = _◃_
  syntax smaparrow[]syntax 𝔛₂ x∼y fx = x∼y ◃[ 𝔛₂ ] fx

module Smaparrow!
  {𝔵₁ 𝔵₂ 𝔯 𝔭₁ 𝔭₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  (𝔓₁ : 𝔛₂ → Ø 𝔭₁)
  (𝔓₂ : 𝔛₂ → Ø 𝔭₂)
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  = Smaparrow ℜ 𝔓₁ 𝔓₂ surjection surjection

module Smaphomarrow
  {𝔵₁ 𝔯₁ 𝔵₂ 𝔯₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯₁)
  (𝔓 : 𝔛₂ → Ø 𝔯₂)
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  = Smaparrow ℜ 𝔓 𝔓 surjection surjection

module Smaphomarrow!
  {𝔵₁ 𝔯₁ 𝔵₂ 𝔯₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯₁)
  (𝔓 : 𝔛₂ → Ø 𝔯₂)
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  = Smaphomarrow ℜ 𝔓 surjection


text:
{-# OPTIONS --without-K #-}
module PathOperations where

open import Types

infixr 4 _·_
infix  9 _⁻¹

_⁻¹ : ∀ {a} {A : Set a} {x y : A} →
  x ≡ y → y ≡ x
_⁻¹ = J (λ x y _ → y ≡ x) (λ _ → refl) _ _

_·_ : ∀ {a} {A : Set a} {x y z : A} →
  x ≡ y → y ≡ z → x ≡ z
_·_ {z = z} = J (λ x y _ → y ≡ z → x ≡ z) (λ _ p′ → p′) _ _

tr : ∀ {a p} {A : Set a} (P : A → Set p) {x y : A} (p : x ≡ y) →
  P x → P y
tr P = J (λ x y _ → P x → P y) (λ _ x → x) _ _

ap : ∀ {a b} {A : Set a}  {B : Set b} {x y : A} (f : A → B) →
  x ≡ y → f x ≡ f y
ap f = J (λ x y _ → f x ≡ f y) (λ _ → refl) _ _

ap₂ : ∀ {a b c} {A : Set a}  {B : Set b} {C : Set c}
  {x x′ y y′} (f : A → B → C) (p : x ≡ x′) (q : y ≡ y′) →
  f x y ≡ f x′ y′
ap₂ f p q = ap (λ _ → f _ _) p · ap (f _) q

apd : ∀ {a b} {A : Set a} {B : A → Set b} {x y : A}
  (f : ∀ a → B a) (p : x ≡ y) →
  tr B p (f x) ≡ f y
apd {B = B} f = J
  (λ x y p → tr B p (f x) ≡ f y)
  (λ _ → refl) _ _

happly : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
  f ≡ g → ∀ x → f x ≡ g x
happly p x = ap (λ f → f x) p

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text: a = b module M where private

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Rational where

open import Cubical.HITs.Rational.Base public

-- open import Cubical.HITs.Rational.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation where

module Data where
      module Empty where open import Light.Implementation.Data.Empty public
      module Either where open import Light.Implementation.Data.Either public
      module Natural where open import Light.Implementation.Data.Natural public
      module Unit where open import Light.Implementation.Data.Unit public
      module Integer where open import Light.Implementation.Data.Integer public
      module Boolean where open import Light.Implementation.Data.Boolean public
      module Product where open import Light.Implementation.Data.Product public
      module These where open import Light.Implementation.Data.These public

module Relation where
      module Sets where open import Light.Implementation.Relation.Sets public
      module Boolean where open import Light.Implementation.Relation.Boolean public
      module Binary where
            module Equality where
                  module Propositional where
                        open import Light.Implementation.Relation.Binary.Equality.Propositional public
                        module Decidable where open import Light.Implementation.Relation.Binary.Equality.Propositional.Decidable public
      module Decidable where open import Light.Implementation.Relation.Decidable public

module Action where open import Light.Implementation.Action public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
-------------------------------------------------
-- Formalisation of the Z axioms of set theory.
-------------------------------------------------
module sv20.assign2.SetTheory.ZAxioms where

open import sv20.assign2.SetTheory.Logic

infix 1 ∃
infix 5 _⊆_ _⊂_
infix 5 _∈_ _∉_
infix 4 _≡_

-- The universe of discourse (pure sets) and the membership
-- relationship. (The letter 𝓢 is type by "\MCS")
postulate
  𝓢   : Set
  _∈_ : 𝓢 → 𝓢 → Set

-- Existential quantifier

data ∃ (A : 𝓢 → Set) : Set where
  _,_ : (t : 𝓢) → A t → ∃ A

-- Sugar syntax for the existential quantifier.

syntax ∃ (λ x → e) = ∃[ x ] e

-- Existential projections.

proj₁ : {A : 𝓢 → Set} → ∃ A → 𝓢
proj₁ (t , _) = t

proj₂ : (A : 𝓢 → Set) → (foo : ∃ A)  → A (proj₁ foo)
proj₂ A (_ , Ax) = Ax

-- Equivalence and non equivalence with some useful properties

data _≡_ (x : 𝓢) : 𝓢 → Set where
  refl : x ≡ x

_≢_ : 𝓢 → 𝓢 → Set
x ≢ y = ¬ x ≡ y

sym : (x y : 𝓢) → x ≡ y → y ≡ x
sym x .x refl = refl

cong : (f :  𝓢 → 𝓢) {x y : 𝓢} → x ≡ y → f x ≡ f y
cong f refl = refl

subs : (P : 𝓢 → Set) {x y : 𝓢} (p : x ≡ y) (h : P x) → P y
subs P {x} {.x} refl h = h

trans : {x y z : 𝓢} → x ≡ y →  y ≡ z → x ≡ z
trans refl refl = refl

-- Property concerning bi-implication, needed in a proof.
⇔-p₂ : (z : 𝓢) → {A B C : Set} →  A ⇔ (B ∧ C) → (C → B) → A ⇔ C
⇔-p₂ z (h₁ , h₂) h₃ = (λ a → ∧-proj₂ (h₁ a)) , (λ c → h₂ ((h₃ c) , c))

-- Definitions of subset and not-membership.

_⊆_ : 𝓢 → 𝓢 → Set
x ⊆ y = (t : 𝓢) → t ∈ x → t ∈ y

_∉_ : 𝓢 → 𝓢 → Set
x ∉ y = ¬ (x ∈ y)
-- {-# ATP definition _∉_ #-}

_⊂_ : 𝓢 → 𝓢 → Set
x ⊂ y = x ⊆ y ∧ x ≢ y

_⊂'_ : 𝓢 → 𝓢 → Set
x ⊂' y = x ⊆ y ∧ ∃ (λ z → z ∈ y ∧ z ∉ x)

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

-- ZFC's axioms
-- From (Suppes 1960, p. 56)

-- ext (Extensionality) : If two sets have exactly the same members,
-- they are equal.

-- empt (Empty Set Axiom) : There is a set having no
-- members. Allows us to define the empty set.

-- pair (Pairing Axiom) : For any sets y and z, there is a set having
-- as members just y and z. Allows to define a set which is just
-- the pair of any two sets.

-- pow (Power Set Axiom): For any x there is a set whose members are
-- exactly the subsets of x. Allows us to define the power set
-- operation.

-- sub (Subset Axiom, or Specification Axiom): This axiom asserts the
-- existence of a set B whose members are exactly those sets x in y
-- such that they satisfy certain property. Allows us to define
-- many operations like cartesian products and difference of sets.

-- uni (Union Axiom) : For any set x, there exists a set A whose
-- elements are exactly the members of x. Allows us to define the
-- union of two sets.

-- pem (Principle of the excluded middle) : To prove some things
-- not valid in intuitionistic logic and valid in classical logic. Taken
-- from the Standford Encyclopedia entry on Intuitionistic Logic.
-- (https://plato.stanford.edu/entries/logic-intuitionistic/).

-- The sum axioms allow us to define the union operation
-- over a family of sets.

postulate
  empt : ∃ (λ B → ∀ x → x ∉ B)
  ext  : (x y : 𝓢) → ∀ {z} → z ∈ x ⇔ z ∈ y → x ≡ y
  union : (x y : 𝓢) → ∃ (λ B → {z : 𝓢} → z ∈ B ⇔ z ∈ x ∨ z ∈ y)
  pair : (x y : 𝓢) → ∃ (λ B → {z : 𝓢} → z ∈ B ⇔ (z ≡ x ∨ z ≡ y))
  pow : (x : 𝓢) → ∃ (λ B → ∀ {y} → y ∈ B ⇔ y ⊆ x)
  sub  : (A : 𝓢 → Set) → (y : 𝓢) → ∃ (λ B → {z : 𝓢} → (z ∈ B ⇔ (z ∈ y ∧ A z)))
  pem : (A : Set) → A ∨ ¬ A
  sum : (A : 𝓢) → ∃ (λ C → (x : 𝓢) → x ∈ C ⇔ ∃ (λ B → x ∈ B ∧ B ∈ A))
-- {-# ATP axioms empt ext union pair pow #-}

-- sub not given to apia since it is an axiom schema and ATPs don't deal
-- with that.

-- pem isn't given either since ATP's use classical logic so it uses
-- this principle by default.

∅ : 𝓢
∅ = proj₁ empt
-- {-# ATP definition ∅ #-}

-- Axiom of regularity: Axiom that have two very intuitive consequences:
-- ∀ A (A ∉ A) and ¬ ∀ A,B (A∈B ∧ B∈A). From Suppes, p. 56 (1960).
postulate
  reg : (A : 𝓢) → A ≢ ∅ → ∃ (λ x → x ∈ A ∧ ∀ y → y ∈ x → y ∉ A)

-- References
--
-- Suppes, Patrick (1960). Axiomatic Set Theory.
-- The University Series in Undergraduate Mathematics.
-- D. Van Nostrand Company, inc.
--
-- Enderton, Herbert B. (1977). Elements of Set Theory.
-- Academic Press Inc.


text:
module Generic.Lib.Data.List where

open import Data.List.Base hiding ([]) renaming (fromMaybe to maybeToList) public
open List public

open import Generic.Lib.Intro
open import Generic.Lib.Equality.Propositional
open import Generic.Lib.Decidable
open import Generic.Lib.Category
open import Generic.Lib.Data.Nat
open import Generic.Lib.Data.Maybe
open import Generic.Lib.Data.Sum
open import Generic.Lib.Data.Product

import Data.List.Categorical as List

infix 4 _∈_

foldr₁ : ∀ {α} {A : Set α} -> (A -> A -> A) -> A -> List A -> A
foldr₁ f z  []          = z
foldr₁ f z (x ∷ [])     = x
foldr₁ f z (x ∷ y ∷ xs) = f x (foldr₁ f z (y ∷ xs))

mapInd : ∀ {α β} {A : Set α} {B : Set β} -> (ℕ -> A -> B) -> List A -> List B
mapInd f  []      = []
mapInd f (x ∷ xs) = f 0 x ∷ mapInd (f ∘ suc) xs

mapM : ∀ {α β} {A : Set α} {B : Set β} {M : Set β -> Set β} {{mMonad : RawMonad M}}
     -> (A -> M B) -> List A -> M (List B)
mapM {{mMonad}} = List.TraversableM.mapM mMonad

downFromTo : ℕ -> ℕ -> List ℕ
downFromTo n m = map (m +_) (downFrom (n ∸ m))

Any : ∀ {α β} {A : Set α} -> (A -> Set β) -> List A -> Set β
Any B  []      = ⊥
Any B (x ∷ []) = B x
Any B (x ∷ xs) = B x ⊎ Any B xs

_∈_ : ∀ {α} {A : Set α} -> A -> List A -> Set
x ∈ xs = Any (x ≡_) xs

here : ∀ {α β} {A : Set α} {B : A -> Set β} {x} xs -> B x -> Any B (x ∷ xs)
here  []      y = y
here (x ∷ xs) y = inj₁ y

phere : ∀ {α} {A : Set α} {x : A} xs -> x ∈ x ∷ xs
phere xs = here xs refl

there : ∀ {α β} {A : Set α} {B : A -> Set β} {x} xs -> Any B xs -> Any B (x ∷ xs)
there  []      ()
there (x ∷ xs) a  = inj₂ a

mapAny : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : A -> Set γ}
       -> ∀ xs -> (∀ {x} -> B x -> C x) -> Any B xs -> Any C xs
mapAny  []           g  ()
mapAny (x ∷ [])      g  y       = g y
mapAny (x ∷ x′ ∷ xs) g (inj₁ y) = inj₁ (g y)
mapAny (x ∷ x′ ∷ xs) g (inj₂ r) = inj₂ (mapAny (x′ ∷ xs) g r)

All : ∀ {α β} {A : Set α} -> (A -> Set β) -> List A -> Set β
All B  []      = ⊤
All B (x ∷ xs) = B x × All B xs

allToList : ∀ {α β} {A : Set α} {B : Set β} {xs : List A} -> All (const B) xs -> List B
allToList {xs = []}      tt      = []
allToList {xs = x ∷ xs} (y , ys) = y ∷ allToList ys

allIn : ∀ {α β} {A : Set α} {B : A -> Set β} -> ∀ xs -> (∀ {x} -> x ∈ xs -> B x) -> All B xs
allIn  []      g = tt
allIn (x ∷ xs) g = g (phere xs) , allIn xs (g ∘ there xs)

mapAll : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : A -> Set γ} {xs : List A}
       -> (∀ {x} -> B x -> C x) -> All B xs -> All C xs
mapAll {xs = []}     g  tt      = tt
mapAll {xs = x ∷ xs} g (y , ys) = g y , mapAll g ys

unmap : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : Set γ} {xs : List A}
      -> (∀ {x} -> B x -> C) -> All B xs -> List C
unmap g = allToList ∘ mapAll g

mapAllInd : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : A -> Set γ} {xs}
          -> (∀ {x} -> ℕ -> B x -> C x) -> All B xs -> All C xs
mapAllInd {xs = []}     g  tt      = tt
mapAllInd {xs = x ∷ xs} g (y , ys) = g 0 y , mapAllInd (g ∘ suc) ys

traverseAll : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : A -> Set γ} {xs : List A}
                {F : Set γ -> Set γ} {{fFunctor : RawFunctor F}} {{fApplicative : RawApplicative F}}
            -> (∀ {x} -> B x -> F (C x)) -> All B xs -> F (All C xs)
traverseAll {xs = []}     g  tt      = pure tt
traverseAll {xs = x ∷ xs} g (y , ys) = _,_ <$> g y <*> traverseAll g ys

splitList : ∀ {α β} {A : Set α} {B : A -> Set β} -> List (Σ A B) -> Σ (List A) (All B)
splitList  []            = [] , tt
splitList ((x , y) ∷ ps) = pmap (_∷_ x) (_,_ y) (splitList ps)

lookupAllConst : ∀ {α β} {A : Set α} {B : Set β} {{bEq : Eq B}} {xs : List A}
               -> B -> All (const B) xs -> Maybe (∃ (_∈ xs))
lookupAllConst {xs = []}     y  tt      = nothing
lookupAllConst {xs = x ∷ xs} y (z , ys) = if y == z
  then just (_ , phere xs)
  else second (there xs) <$> lookupAllConst y ys

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Optics.All
open import LibraBFT.Prelude

-- This module defines syntax and functionality modeling an RWST monad,
-- which we use to define an implementation.
-- TODO-2: this module is independent of any particular implementation
-- and arguably belongs somewhere more general, such as next to Optics.

module LibraBFT.Impl.Util.RWST (ℓ-State : Level) where

  ----------------
  -- RWST Monad --
  ----------------

  -- 'Fake' RWST monad; fake in the sense
  -- we use the free monoid on the writer (aka. lists)
  -- instad of requiring it to be a monoid in a separate
  -- argument.
  RWST-Raw : Set → Set → Set ℓ-State → {ℓ-Result : Level} → Set ℓ-Result → Set (ℓ-State ℓ⊔ ℓ-Result)
  RWST-Raw Ev Wr St R = Ev → St → (R × St × List Wr)

  -- Wrap it in a type; prevents spurious evaluation and
  -- obliges us to 'run' the monad.
  data RWST (Ev Wr : Set) (St : Set ℓ-State) {ℓ-Result : Level} : Set ℓ-Result → Set (ℓ-State ℓ⊔ ℓ-Result) where
    rwst : ∀ {R : Set ℓ-Result} → RWST-Raw Ev Wr St {ℓ-Result} R → RWST Ev Wr St R

  private
   variable
    Ev Wr : Set
    ℓ-A ℓ-B : Level
    A : Set ℓ-A
    B : Set ℓ-B
    St : Set ℓ-State

  RWST-run : RWST Ev Wr St A → Ev → St → (A × St × List Wr)
  RWST-run (rwst f) = f

  RWST-bind : RWST Ev Wr St A → (A → RWST Ev Wr St B) → RWST Ev Wr St B
  RWST-bind x f = rwst (λ ev st →
    let (a , st'  , wr₀) = RWST-run x     ev st
        (b , st'' , wr₁) = RWST-run (f a) ev st'
     in b , st'' , wr₀ ++ wr₁)

  RWST-return : A → RWST Ev Wr St A
  RWST-return x = rwst (λ _ st → x , st , [])

  -- Functorial Functionality

  RWST-map : (A → B) → RWST Ev Wr St A → RWST Ev Wr St B
  RWST-map f x = rwst (λ ev st →
    let (a , st' , wr) = RWST-run x ev st
     in f a , st' , wr)

  -- Provided Functionality

  get : RWST Ev Wr St {ℓ-State} St
  get = rwst (λ _ st → st , st , [])

  gets : (St → A) → RWST Ev Wr St A
  gets f = RWST-bind get (RWST-return ∘ f)

{- TODO-2: extend Lens to work with different levels and reinstate this

   Note that a preliminary exploration by @cwjnkins revealed this to
   be more painful than it's worth, at least until we have a
   compelling use case for St to be at a higher level.  In the
   meantime, we have defined use and modify' specifically for our
   state type, which is in Set; see LibraBFT.Impl.Util.Util.

  use : Lens St A → RWST Ev Wr St A
  use f = RWST-bind get (RWST-return ∘ (_^∙ f))
-}

  modify : (St → St) → RWST Ev Wr St Unit
  modify f = rwst (λ _ st → unit , f st , [])

{- TODO-2: extend Lens to work with different levels and reinstate this
   See comment above for use
  modify' : ∀ {A} → Lens St A → A → RWST Ev Wr St Unit
  modify' l val = modify λ x → x [ l := val ]
  syntax modify' l val = l ∙= val
-}

  put : St → RWST Ev Wr St Unit
  put s = modify (λ _ → s)

  tell : List Wr → RWST Ev Wr St Unit
  tell wrs = rwst (λ _ st → unit , st , wrs)

  tell1 : Wr → RWST Ev Wr St Unit
  tell1 wr = tell (wr ∷ [])

  ask : RWST Ev Wr St Ev
  ask = rwst (λ ev st → (ev , st , []))

  -- Easy to use do notation; i.e.;
  module RWST-do where
    infixl 1 _>>=_ _>>_
    _>>=_  : RWST Ev Wr St A → (A → RWST Ev Wr St B) → RWST Ev Wr St B
    _>>=_  = RWST-bind

    _>>_   : RWST Ev Wr St A → RWST Ev Wr St B → RWST Ev Wr St B
    x >> y = x >>= λ _ → y

    return : A → RWST Ev Wr St A
    return = RWST-return

    pure : A → RWST Ev Wr St A
    pure = return

    infixr 4 _<$>_
    _<$>_ : (A → B) → RWST Ev Wr St A → RWST Ev Wr St B
    _<$>_ = RWST-map

  private
    ex₀ : RWST ℕ Wr (Lift ℓ-State ℕ) ℕ
    ex₀ = do
       x₁ ← get
       x₂ ← ask
       return (lower x₁ + x₂)
       where open RWST-do

  -- Derived Functionality

  maybeMP : RWST Ev Wr St (Maybe A) → B → (A → RWST Ev Wr St B)
          → RWST Ev Wr St B
  maybeMP ma b f = do
    x ← ma
    case x of
      λ { (just r) → f r
        ; nothing  → return b
        }
    where open RWST-do

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Irrelevance {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.LogicalRelation
import Definition.LogicalRelation.Irrelevance as LR
open import Definition.LogicalRelation.Substitution

open import Tools.Product
open import Tools.Unit
import Tools.PropositionalEquality as PE

-- Irrelevance of valid substitutions with different derivations of contexts
irrelevanceSubst : ∀ {σ Γ Δ}
                   ([Γ] [Γ]′ : ⊩ᵛ Γ)
                   (⊢Δ ⊢Δ′ : ⊢ Δ)
                 → Δ ⊩ˢ σ ∷ Γ / [Γ]  / ⊢Δ
                 → Δ ⊩ˢ σ ∷ Γ / [Γ]′ / ⊢Δ′
irrelevanceSubst ε′ ε′ ⊢Δ ⊢Δ′ [σ] = tt
irrelevanceSubst ([Γ] ∙′ [A]) ([Γ]′ ∙′ [A]′) ⊢Δ ⊢Δ′ ([tailσ] , [headσ]) =
  let [tailσ]′ = irrelevanceSubst [Γ] [Γ]′ ⊢Δ ⊢Δ′ [tailσ]
  in  [tailσ]′
  ,   LR.irrelevanceTerm (proj₁ ([A] ⊢Δ [tailσ]))
                            (proj₁ ([A]′ ⊢Δ′ [tailσ]′))
                            [headσ]

-- Irrelevance of valid substitutions with different contexts
-- that are propositionally equal
irrelevanceSubst′ : ∀ {σ Γ Δ Δ′}
                    (eq : Δ PE.≡ Δ′)
                    ([Γ] [Γ]′ : ⊩ᵛ Γ)
                    (⊢Δ  : ⊢ Δ)
                    (⊢Δ′ : ⊢ Δ′)
                  → Δ  ⊩ˢ σ ∷ Γ / [Γ]  / ⊢Δ
                  → Δ′ ⊩ˢ σ ∷ Γ / [Γ]′ / ⊢Δ′
irrelevanceSubst′ PE.refl [Γ] [Γ]′ ⊢Δ ⊢Δ′ [σ] = irrelevanceSubst [Γ] [Γ]′ ⊢Δ ⊢Δ′ [σ]

-- Irrelevance of valid substitution equality
-- with different derivations of contexts
irrelevanceSubstEq : ∀ {σ σ′ Γ Δ}
                     ([Γ] [Γ]′ : ⊩ᵛ Γ)
                     (⊢Δ ⊢Δ′ : ⊢ Δ)
                     ([σ]  : Δ ⊩ˢ σ ∷ Γ / [Γ]  / ⊢Δ)
                     ([σ]′ : Δ ⊩ˢ σ ∷ Γ / [Γ]′ / ⊢Δ′)
                   → Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ]  / ⊢Δ  / [σ]
                   → Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ]′ / ⊢Δ′ / [σ]′
irrelevanceSubstEq ε′ ε′ ⊢Δ ⊢Δ′ [σ] [σ]′ [σ≡σ′] = tt
irrelevanceSubstEq ([Γ] ∙′ [A]) ([Γ]′ ∙′ [A]′) ⊢Δ ⊢Δ′ [σ] [σ]′ [σ≡σ′] =
  irrelevanceSubstEq [Γ] [Γ]′ ⊢Δ ⊢Δ′ (proj₁ [σ]) (proj₁ [σ]′) (proj₁ [σ≡σ′])
  , LR.irrelevanceEqTerm (proj₁ ([A] ⊢Δ  (proj₁ [σ])))
                            (proj₁ ([A]′ ⊢Δ′ (proj₁ [σ]′)))
                            (proj₂ [σ≡σ′])

-- Irrelevance of valid types with different derivations of contexts
irrelevance : ∀ {l A Γ}
              ([Γ] [Γ]′ : ⊩ᵛ Γ)
            → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
            → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]′
irrelevance [Γ] [Γ]′ [A] ⊢Δ [σ] =
  let [σ]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
  in  proj₁ ([A] ⊢Δ [σ]′)
   ,  λ [σ′] [σ≡σ′] → proj₂ ([A] ⊢Δ [σ]′)
                       (irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ′])
                       (irrelevanceSubstEq [Γ]′ [Γ] ⊢Δ ⊢Δ [σ] [σ]′ [σ≡σ′])

open import Definition.LogicalRelation.Properties

-- Irrelevance of valid types with different derivations of contexts
-- with lifting of eqaul types
irrelevanceLift : ∀ {l A F H Γ}
              ([Γ] : ⊩ᵛ Γ)
              ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
              ([H] : Γ ⊩ᵛ⟨ l ⟩ H / [Γ])
              ([F≡H] : Γ ⊩ᵛ⟨ l ⟩ F ≡ H / [Γ] / [F])
            → Γ ∙ F ⊩ᵛ⟨ l ⟩ A / (VPack _ _ (V∙ [Γ] [F]))
            → Γ ∙ H ⊩ᵛ⟨ l ⟩ A / (VPack _ _ (V∙ [Γ] [H]))
irrelevanceLift [Γ] [F] [H] [F≡H] [A] ⊢Δ ([tailσ] , [headσ]) =
  let [σ]′ = [tailσ] , convTerm₂ (proj₁ ([F] ⊢Δ [tailσ]))
                                 (proj₁ ([H] ⊢Δ [tailσ]))
                                 ([F≡H] ⊢Δ [tailσ]) [headσ]
  in  proj₁ ([A] ⊢Δ [σ]′)
  ,   (λ [σ′] x →
         let [σ′]′ = proj₁ [σ′] , convTerm₂ (proj₁ ([F] ⊢Δ (proj₁ [σ′])))
                                            (proj₁ ([H] ⊢Δ (proj₁ [σ′])))
                                            ([F≡H] ⊢Δ (proj₁ [σ′]))
                                            (proj₂ [σ′])
             [tailσ′] = proj₁ [σ′]
         in  proj₂ ([A] ⊢Δ [σ]′) [σ′]′
                   (proj₁ x , convEqTerm₂ (proj₁ ([F] ⊢Δ [tailσ]))
                                          (proj₁ ([H] ⊢Δ [tailσ]))
                                          ([F≡H] ⊢Δ [tailσ])
                                          (proj₂ x)))

-- Irrelevance of valid type equality with different derivations of
-- contexts and types
irrelevanceEq : ∀ {l l′ A B Γ}
                ([Γ] [Γ]′ : ⊩ᵛ Γ)
                ([A]  : Γ ⊩ᵛ⟨ l  ⟩ A / [Γ])
                ([A]′ : Γ ⊩ᵛ⟨ l′ ⟩ A / [Γ]′)
              → Γ ⊩ᵛ⟨ l  ⟩ A ≡ B / [Γ]  / [A]
              → Γ ⊩ᵛ⟨ l′ ⟩ A ≡ B / [Γ]′ / [A]′
irrelevanceEq [Γ] [Γ]′ [A] [A]′ [A≡B] ⊢Δ [σ] =
  let [σ]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
  in  LR.irrelevanceEq (proj₁ ([A] ⊢Δ [σ]′))
                       (proj₁ ([A]′ ⊢Δ [σ]))
                       ([A≡B] ⊢Δ [σ]′)

-- Irrelevance of valid terms with different derivations of contexts and types
irrelevanceTerm : ∀ {l l′ A t Γ}
                  ([Γ] [Γ]′ : ⊩ᵛ Γ)
                  ([A]  : Γ ⊩ᵛ⟨ l  ⟩ A / [Γ])
                  ([A]′ : Γ ⊩ᵛ⟨ l′ ⟩ A / [Γ]′)
                → Γ ⊩ᵛ⟨ l  ⟩ t ∷ A / [Γ]  / [A]
                → Γ ⊩ᵛ⟨ l′ ⟩ t ∷ A / [Γ]′ / [A]′
irrelevanceTerm [Γ] [Γ]′ [A] [A]′ [t] ⊢Δ [σ]′ =
  let [σ]   = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]′
      [σA]  = proj₁ ([A] ⊢Δ [σ])
      [σA]′ = proj₁ ([A]′ ⊢Δ [σ]′)
  in  LR.irrelevanceTerm [σA] [σA]′ (proj₁ ([t] ⊢Δ [σ]))
   ,  (λ [σ′] x → LR.irrelevanceEqTerm [σA] [σA]′ ((proj₂ ([t] ⊢Δ [σ]))
                    (irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ′])
                    (irrelevanceSubstEq [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]′ [σ] x)))

-- Irrelevance of valid terms with different derivations of
-- contexts and types which are propositionally equal
irrelevanceTerm′ : ∀ {l l′ A A′ t Γ}
                   (eq : A PE.≡ A′)
                   ([Γ] [Γ]′ : ⊩ᵛ Γ)
                   ([A]  : Γ ⊩ᵛ⟨ l  ⟩ A / [Γ])
                   ([A′] : Γ ⊩ᵛ⟨ l′ ⟩ A′ / [Γ]′)
                 → Γ ⊩ᵛ⟨ l  ⟩ t ∷ A / [Γ]  / [A]
                 → Γ ⊩ᵛ⟨ l′ ⟩ t ∷ A′ / [Γ]′ / [A′]
irrelevanceTerm′ {A = A} {t = t} PE.refl [Γ] [Γ]′ [A] [A]′ [t] =
  irrelevanceTerm {A = A} {t = t} [Γ] [Γ]′ [A] [A]′ [t]

-- Irrelevance of valid terms with different derivations of
-- contexts and types with a lifting of equal types
irrelevanceTermLift : ∀ {l A F H t Γ}
              ([Γ] : ⊩ᵛ Γ)
              ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
              ([H] : Γ ⊩ᵛ⟨ l ⟩ H / [Γ])
              ([F≡H] : Γ ⊩ᵛ⟨ l ⟩ F ≡ H / [Γ] / [F])
              ([A] : Γ ∙ F ⊩ᵛ⟨ l ⟩ A / (VPack _ _ (V∙ [Γ] [F])))
            → Γ ∙ F ⊩ᵛ⟨ l ⟩ t ∷ A / (VPack _ _ (V∙ [Γ] [F])) / [A]
            → Γ ∙ H ⊩ᵛ⟨ l ⟩ t ∷ A / (VPack _ _ (V∙ [Γ] [H]))
                           / irrelevanceLift {A = A} {F = F} {H = H}
                                             [Γ] [F] [H] [F≡H] [A]
irrelevanceTermLift [Γ] [F] [H] [F≡H] [A] [t] ⊢Δ ([tailσ] , [headσ]) =
  let [σ]′ = [tailσ] , convTerm₂ (proj₁ ([F] ⊢Δ [tailσ]))
                                 (proj₁ ([H] ⊢Δ [tailσ]))
                                 ([F≡H] ⊢Δ [tailσ]) [headσ]
  in  proj₁ ([t] ⊢Δ [σ]′)
  , (λ [σ′] x →
       let [σ′]′ = proj₁ [σ′] , convTerm₂ (proj₁ ([F] ⊢Δ (proj₁ [σ′])))
                                          (proj₁ ([H] ⊢Δ (proj₁ [σ′])))
                                          ([F≡H] ⊢Δ (proj₁ [σ′]))
                                          (proj₂ [σ′])
           [tailσ′] = proj₁ [σ′]
       in  proj₂ ([t] ⊢Δ [σ]′) [σ′]′
                 (proj₁ x , convEqTerm₂ (proj₁ ([F] ⊢Δ [tailσ]))
                                        (proj₁ ([H] ⊢Δ [tailσ]))
                                        ([F≡H] ⊢Δ [tailσ])
                                        (proj₂ x)))

-- Irrelevance of valid term equality with different derivations of
-- contexts and types
irrelevanceEqTerm : ∀ {l l′ A t u Γ}
                  ([Γ] [Γ]′ : ⊩ᵛ Γ)
                  ([A]  : Γ ⊩ᵛ⟨ l  ⟩ A / [Γ])
                  ([A]′ : Γ ⊩ᵛ⟨ l′ ⟩ A / [Γ]′)
                → Γ ⊩ᵛ⟨ l  ⟩ t ≡ u ∷ A / [Γ]  / [A]
                → Γ ⊩ᵛ⟨ l′ ⟩ t ≡ u ∷ A / [Γ]′ / [A]′
irrelevanceEqTerm {A = A} {t = t} {u = u} [Γ] [Γ]′ [A] [A]′ [t≡u] ⊢Δ [σ] =
  let [σ]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
  in  LR.irrelevanceEqTerm (proj₁ ([A] ⊢Δ [σ]′))
                           (proj₁ ([A]′ ⊢Δ [σ]))
                           ([t≡u] ⊢Δ [σ]′)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module Array.Base where

open import Data.Nat
open import Data.Nat.DivMod             --using (_div_ ; _mod_; _/_; m/n*n≤m)
open import Data.Nat.Divisibility
open import Data.Nat.Properties
open import Data.Vec
open import Data.Vec.Properties         using (lookup∘tabulate)
open import Data.Fin.Base               hiding (_<_; _+_)
open import Data.Fin.Properties         hiding (_≟_; <-cmp; ≤-trans; <-trans)
open import Function                    using (_$_; _∘_; case_of_)
open import Data.Product                using (Σ; _,_)
open import Relation.Binary.PropositionalEquality   --using (_≡_; _≢_; refl; subst; sym; cong; cong₂)
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Nullary            --using (Dec; yes; no)
open import Relation.Nullary.Decidable  --using (fromWitnessFalse; False)
open import Relation.Nullary.Negation   --using (contradiction)
open import Data.Sum                    using (inj₁; inj₂)
open import Data.Empty

infixr 5 _∷_
data Ix : (d : ℕ) → (s : Vec ℕ d) → Set where
  []   : Ix 0 []
  _∷_  : ∀ {d s x} → Fin x → (ix : Ix d s) → Ix (suc d) (x ∷ s)

ix-lookup : ∀ {d s} → Ix d s → (i : Fin d) → Fin (lookup s i)
ix-lookup [] ()
ix-lookup (x ∷ ix) zero = x
ix-lookup (x ∷ ix) (suc i) = ix-lookup ix i

ix-tabulate : ∀ {d s} → ((i : Fin d) → Fin (lookup s i)) → Ix d s
ix-tabulate {s = []} f = []
ix-tabulate {s = x ∷ s} f = f zero ∷ ix-tabulate (f ∘ suc)

ix→v : ∀ {d s} → Ix d s → Vec ℕ d
ix→v [] = []
ix→v (x ∷ xs) = toℕ x ∷ ix→v xs

--data Ar {a} (X : Set a) (d : ℕ) (s : Vec ℕ d) : Set a where
--  imap : (Ix d s → X) → Ar X d s
--
-- We used this type before `withReconstructed` was introduced, so that
-- we could obtain the shape of arrays at each imap.  Now we have switched
-- to the record that gives us η-equality.
--
--data Ar {a} (X : Set a) (d : ℕ) : (Vec ℕ d) → Set a where
--  imap : ∀ {s} → (Ix d s → X) → Ar X d s

record Ar {a} (X : Set a) (d : ℕ) (s : Vec ℕ d) : Set a where
  constructor imap
  field sel : Ix d s → X
open Ar public

unimap : ∀ {a}{X : Set a}{d s} → Ar X d s → Ix d s → X
unimap (imap x) = x

cst : ∀ {a}{X : Set a}{d s} → X → Ar X d s
cst x = imap λ _ → x

-- Promoting shapes into 1-dimensional array of integers
-- and back.
s→a : ∀ {n} → Vec ℕ n → Ar ℕ 1 (n ∷ [])
s→a s = imap (λ iv → lookup s $ ix-lookup iv zero )

a→s : ∀ {s} → Ar ℕ 1 (s ∷ []) → Vec ℕ s
a→s (imap x) = tabulate λ i → x (i ∷ [])

-- Here we define < on shape-like objects and demonstrate that
-- this relation is decideable.
_<s_ : ∀ {n} → Vec ℕ n → Vec ℕ n → Set
a <s b = ∀ i → lookup a i < lookup b i

-- XXX This might be just equality
_=s_ : ∀ {n} → Vec ℕ n → Vec ℕ n → Set
a =s b = ∀ i → lookup a i ≡ lookup b i

_<a_ : ∀ {d s} → Ar ℕ d s → Ar ℕ d s → Set
imap f <a imap g = ∀ iv → f iv < g iv

_≥a_ : ∀ {d s} → Ar ℕ d s → Ar ℕ d s → Set
imap f ≥a imap g = ∀ iv → f iv ≥ g iv

_=a_ : ∀ {a}{X : Set a}{d s} → Ar X d s → Ar X d s → Set a
imap f =a imap g = ∀ iv → f iv ≡ g iv

_=ix_ : ∀ {d s} → Ix d s → Ix d s → Set
iv =ix jv = ∀ i → ix-lookup iv i ≡ ix-lookup jv i

subst-ix : ∀ {n}{s s₁ : Vec ℕ n} → s =s s₁ → Ix n s → Ix n s₁
subst-ix {zero} {[]} {[]} pf []  = []
subst-ix {suc n} {x ∷ xs} {y ∷ ys} pf (i ∷ iv) rewrite (pf zero) = i ∷ subst-ix (pf ∘ suc) iv

subst-ar : ∀ {a}{X : Set a}{n}{s s₁ : Vec ℕ n} → s =s s₁ → Ar X n s → Ar X n s₁
subst-ar pf (imap f) = imap λ iv → f $ subst-ix (sym ∘ pf) iv

subst-ar-d : ∀ {a}{X : Set a}{n m}{s : Vec ℕ n}{s₁ : Vec ℕ m}
           → (n=m : n ≡ m)
           → s =s (subst (Vec ℕ) (sym n=m) s₁)
           → Ar X n s → Ar X m s₁
subst-ar-d refl pf a = subst-ar pf a

-- If we have an index, produce a pair containing an array representation
-- and the proof that the index is smaller than the shape.
ix→a : ∀ {d}{s : Vec ℕ d}
     → (ix : Ix d s)
     → Σ (Ar ℕ 1 (d ∷ [])) λ ax → ax <a (s→a s)
ix→a ix = imap (λ iv → toℕ $ ix-lookup ix (ix-lookup iv zero)) ,
          λ iv → toℕ<n (ix-lookup ix (ix-lookup iv zero))

-- XXX we can do this via imap/lookup if we want to, so that it
-- extracts to more efficient code.
infixl 10 _ix++_
_ix++_ : ∀ {n m s s₁}
       → (iv : Ix n s)
       → (jv : Ix m s₁)
       → Ix (n + m) (s ++ s₁)
_ix++_ {s = []}     {s₁} iv jv = jv
_ix++_ {s = s ∷ ss} {s₁} (i ∷ iv) jv = i ∷ iv ix++ jv

nest : ∀ {a}{X : Set a}{n m s s₁}
     →  Ar X (n + m) (s ++ s₁)
     →  Ar (Ar X m s₁) n s
nest (imap f) = imap (λ iv → imap (λ jv → f (iv ix++ jv)))

-- Take and drop for indices
take-ix-l : ∀ {n m} → (s : Vec ℕ n) (s₁ : Vec ℕ m)
          → Ix (n + m) (s ++ s₁)
          → Ix n s
take-ix-l []       s₁ ix = []
take-ix-l (s ∷ ss) s₁ (x ∷ ix) = x ∷ take-ix-l ss s₁ ix

take-ix-r : ∀ {n m} → (s : Vec ℕ n) (s₁ : Vec ℕ m)
          → Ix (n + m) (s ++ s₁)
          → Ix m s₁
take-ix-r [] s₁ ix = ix
take-ix-r (x ∷ s) s₁ (x₁ ∷ ix) = take-ix-r s s₁ ix

-- Flatten the first nesting of the Ar
flatten : ∀ {a}{X : Set a}{n m}{s : Vec ℕ n}{s₁ : Vec ℕ m}
        → Ar (Ar X m s₁) n s
        → Ar X (n + m) (s ++ s₁)
flatten (imap f) = imap λ iv → case f (take-ix-l _ _ iv) of λ where
                              (imap g) → g (take-ix-r _ _ iv)

prod : ∀ {n} → (Vec ℕ n) → ℕ
prod s = foldr _ _*_ 1 s

magic-fin : ∀ {a}{X : Set a} → Fin 0 → X
magic-fin ()

a*b≢0⇒a≢0 : ∀ {a b} → a * b ≢ 0 → a ≢ 0
a*b≢0⇒a≢0 {zero}    {b} 0≢0 0≡0 = 0≢0 0≡0
a*b≢0⇒a≢0 {(suc a)} {b} _       = λ ()

a*b≢0⇒b≢0 : ∀ {a b} → a * b ≢ 0 → b ≢ 0
a*b≢0⇒b≢0 {a} {b} rewrite (*-comm a b) = a*b≢0⇒a≢0

-- A basic fact about division that is not yet in the stdlib.
/-mono-x : ∀ {a b c} → a < b * c → (c≢0 : False (c ≟ 0))
         → (a / c) {≢0 = c≢0} < b
/-mono-x {a}{b}{c} a<b*c c≢0 with <-cmp ((a / c) {≢0 = c≢0}) b
/-mono-x {a} {b} {c} a<b*c c≢0 | tri< l< _ _ = l<
/-mono-x {a} {b} {c} a<b*c c≢0 | tri≈ _ l≡ _ = let
     a<a/c*c = subst (a <_) (cong₂ _*_ (sym l≡) refl) a<b*c
     a/c*c≤a = m/n*n≤m a c {≢0 = c≢0}
     a<a = ≤-trans a<a/c*c a/c*c≤a
   in contradiction a<a (n≮n a)
/-mono-x {a} {b} {suc c} a<b*c c≢0 | tri> _ _ l> = let
     b*c<a/c*c = *-monoˡ-< c l>
     a/c*c≤a = m/n*n≤m a (suc c) {≢0 = c≢0}
     b*c≤a = ≤-trans b*c<a/c*c a/c*c≤a
     a<a = <-trans a<b*c b*c≤a
   in contradiction a<a (n≮n a)

/-mono-f : ∀ {a b c} → a < b * c → (b≢0 : False (b ≟ 0))
         → (a / b) {≢0 = b≢0} < c
/-mono-f {b = b}{c} a<b*c ≢0 rewrite *-comm b c = /-mono-x a<b*c ≢0

divmod-thm : ∀ {a b m n}
           → (n≢0 : n ≢ 0)
           → a ≡ (m % n) {≢0 = fromWitnessFalse n≢0}
           → b ≡ (m / n) {≢0 = fromWitnessFalse n≢0} * n
             → m ≡ a + b
divmod-thm {n = zero} n≢0 _ _ = contradiction refl n≢0
divmod-thm {m = m}{n = suc n} n≢0 refl refl = m≡m%n+[m/n]*n m n

-- XXX currently this is not efficient way to convert between indices and
-- offsets, as we are doing it form left to right.  Computing in reverse
-- makes more sense.  Something for later.

off→idx : ∀ {n} → (sh : Vec ℕ n)
        → Ix 1 (prod sh ∷ [])
        → Ix n sh
off→idx [] iv = []
off→idx (s ∷ sh) iv with prod (s ∷ sh) ≟ 0
off→idx (s ∷ sh) iv | yes p rewrite p = magic-fin $ ix-lookup iv zero
off→idx (s ∷ sh) (off ∷ []) | no ¬p = let
                                         o = toℕ off
                                         tl = prod sh
                                         tl≢0 = fromWitnessFalse (a*b≢0⇒b≢0 {a = s} ¬p)
                                     in {- off / tl -} (fromℕ< (/-mono-x (toℕ<n off) tl≢0))
                                        {- rec call -} ∷ (off→idx sh ((o mod tl) {tl≢0} ∷ []))

module test-oi where
  open import Data.Fin using (#_)
  test-oi₁ : off→idx (10 ∷ 5 ∷ []) (# 40 ∷ []) ≡ (# 8) ∷ (# 0) ∷ []
  test-oi₁ = refl

-- [x , y] < [a , b] ⇒ rowmaj [x , y] < a*b ⇒ x*b+y < a*b
rm-thm : ∀ {a b} → (x : Fin a) → (b ≢ 0) → (y : Fin b) → ((toℕ y) + (toℕ x) * b  < (a * b))
rm-thm {a} {ℕ.zero}  x pf y = contradiction (refl {x = 0}) pf
rm-thm {ℕ.zero} {ℕ.suc b₁} () pf y
rm-thm {ℕ.suc a₁} {ℕ.suc b₁} x pf y = +-mono-≤ (toℕ<n y) $ *-monoˡ-≤ (ℕ.suc b₁) (≤-pred $ toℕ<n x)

v-rm-thm : ∀ {a b x y b≢0} → (toℕ $ fromℕ< (rm-thm {a = a} {b = b} x b≢0 y)) ≡ (toℕ y) + (toℕ x) * b
v-rm-thm {suc a} {suc b} {x} {y} {≢0} = toℕ-fromℕ< (rm-thm x ≢0 y)

Πs≡0⇒Fin0 : ∀ {n} → (s : Vec ℕ n)
          → (Ix n s) → (prod s ≡ 0)
          → Fin 0
Πs≡0⇒Fin0 (x ∷ s) (i ∷ iv) Πxs≡0 with  m*n≡0⇒m≡0∨n≡0 x Πxs≡0
Πs≡0⇒Fin0 (x ∷ s) (i ∷ iv) Πxs≡0 | inj₁ x≡0 rewrite x≡0 = i
Πs≡0⇒Fin0 (x ∷ s) (i ∷ iv) Πxs≡0 | inj₂ Πs≡0 = Πs≡0⇒Fin0 s iv Πs≡0

idx→off : ∀ {n} → (s : Vec ℕ n)
        → (iv : Ix n s)
        → Ix 1 (prod s ∷ [])
idx→off [] iv = zero ∷ iv
idx→off (s ∷ sh) (i ∷ iv) with prod (s ∷ sh) ≟ 0
idx→off (s ∷ sh) (i ∷ iv) | yes p rewrite p = magic-fin $ Πs≡0⇒Fin0 (s ∷ sh) (i ∷ iv) p
idx→off (s ∷ sh) (i ∷ iv) | no ¬p = fromℕ< (rm-thm i (a*b≢0⇒b≢0 {a = s} ¬p) (ix-lookup (idx→off sh iv) zero)) ∷ []

module test-io where
  open import Data.Fin using (#_)
  test-io₁ : idx→off (10 ∷ 5 ∷ []) (# 8 ∷ # 0 ∷ []) ≡ # 40 ∷ []
  test-io₁ = refl

mkempty : ∀ {a}{X : Set a}{n} → (s : Vec ℕ n) → (prod s ≡ 0) → Ar X n s
mkempty {X = X} {n = n} s Πs≡0 = imap empty
  where
    empty : _
    empty iv = magic-fin $ Πs≡0⇒Fin0 s iv Πs≡0

-- Fin fact:
Fin1≡0 : (x : Fin 1) → x ≡ zero
Fin1≡0 zero = refl

-- XXX This should be moved to Properties
io-oi : ∀ {n}{x : Vec _ n}{i : Fin (prod x)}
      → idx→off x (off→idx x (i ∷ [])) ≡ i ∷ []
io-oi {zero} {[]}{i} = cong (_∷ []) (sym (Fin1≡0 i))
io-oi {suc n} {x ∷ x₁}{i} with prod (x ∷ x₁) ≟ 0
... | yes p = ⊥-elim $ ¬Fin0 (subst Fin p i)
... | no ¬p with prod (x ∷ x₁) ≟ 0
io-oi {suc n} {x ∷ x₁} {i} | no ¬p | yes q = contradiction q ¬p
io-oi {suc n} {x ∷ x₁} {i} | no ¬p | no ¬q
  = cong (_∷ []) (toℕ-injective (trans (v-rm-thm {a = x} {b = prod x₁})
                                       (sym (divmod-thm
                                                 {a = toℕ (ix-lookup (idx→off x₁ (off→idx x₁ _)) zero)}
                                                 (a*b≢0⇒b≢0 {a = x} ¬p)
                                                 (trans (cong (λ x → toℕ (ix-lookup x zero))
                                                              (io-oi {x = x₁}))
                                                        mod⇒%)
                                                 (mono⇒/* {b = x} {c = prod x₁})))))
  where
    mono⇒/* : ∀ {b c}{i : Fin (b * c)}{≢0 : False (c ≟ 0)}
            → toℕ {n = b} (fromℕ< (/-mono-x (toℕ<n i) (≢0))) * c ≡ (toℕ i / c) {≢0} * c
    mono⇒/* {b} {c} {i} {≢0} = cong (_* c) (toℕ-fromℕ< (/-mono-x (toℕ<n i) ≢0))

    mod⇒% :  ∀ {n}{i : Fin n}{a}{≢0 : False (a ≟ 0)} → toℕ ((toℕ i mod a){≢0}) ≡ (toℕ i % a) {≢0}
    mod⇒% {n} {i} {suc a} = trans (toℕ-fromℕ< (m%n<n (toℕ i) a)) refl

m≡m+x⇒0≡x : ∀ {m x} → m ≡ m + x → 0 ≡ x
m≡m+x⇒0≡x {m}{x} m≡m+x = +-cancelˡ-≡ m (trans (+-identityʳ m) m≡m+x)

a*b≡0⇒b≢0⇒a≡0 : ∀ {a b} → a * b ≡ 0 → b ≢ 0 → a ≡ 0
a*b≡0⇒b≢0⇒a≡0 {a}{b} a*b≡0 b≢0 with (m*n≡0⇒m≡0∨n≡0 a a*b≡0)
a*b≡0⇒b≢0⇒a≡0 {a} {b} a*b≡0 b≢0 | inj₁ x = x
a*b≡0⇒b≢0⇒a≡0 {a} {b} a*b≡0 b≢0 | inj₂ y = contradiction y b≢0

-- m≤n⇒m%n≡m
m<n⇒m/n≡0 : ∀ {m n} → (m<n : m < n) → ∀ {≢0} → (m / n) {≢0} ≡ 0
m<n⇒m/n≡0 {m} {n@(suc n-1)} m<n = let
                      m%n≡m = m≤n⇒m%n≡m (≤-pred m<n)
                      m≡m%n+m/n*n = (m≡m%n+[m/n]*n m n-1)
                      m≡m+m/n*n = trans m≡m%n+m/n*n (cong₂ _+_ m%n≡m refl)
                      m/n*n≡0 = sym (m≡m+x⇒0≡x m≡m+m/n*n)
                      m/n≡0 = a*b≡0⇒b≢0⇒a≡0 {a = m / n} {b = n} m/n*n≡0 (m<n⇒n≢0 m<n)
                    in m/n≡0

b≡0+c≡a⇒b+c≡a : ∀ {a b c} → b ≡ 0 → c ≡ a → b + c ≡ a
b≡0+c≡a⇒b+c≡a refl refl = refl

a<c⇒c|b⇒[a+b]%c≡a : ∀ {a b c} → a < c → (c ∣ b) → ∀ {≢0} → ((a + b) % c) {≢0} ≡ a
a<c⇒c|b⇒[a+b]%c≡a {a} {b} {c@(suc c-1)} a<c c|b = trans (%-remove-+ʳ a c|b) (m≤n⇒m%n≡m (≤-pred a<c))

a<c⇒c|b⇒[a+b]mod[c]≡a : ∀ {b c} → (a : Fin c) → (c ∣ b) → ∀ {≢0} → ((toℕ a + b) mod c) {≢0} ≡ a
a<c⇒c|b⇒[a+b]mod[c]≡a {b} {suc c-1} a c|b {≢0} = toℕ-injective (trans (toℕ-fromℕ< _) (a<c⇒c|b⇒[a+b]%c≡a (toℕ<n a) c|b))

ixl-cong : ∀ {s}{i : Ix 1 (s ∷ [])} → (ix-lookup i zero) ∷ [] ≡ i
ixl-cong {i = i ∷ []} = refl

--rm-thm : ∀ {a b} → (x : Fin a) → (b ≢ 0) → (y : Fin b) → ((toℕ y) + (toℕ x) * b  < (a * b))
--v-rm-thm : ∀ {a b x y b≢0} → (toℕ $ fromℕ< (rm-thm {a = a} {b = b} x b≢0 y)) ≡ (toℕ y) + (toℕ x) * b
oi-io : ∀ {n}{x : Vec _ n}{iv : Ix n x}
      → off→idx x (idx→off x iv) ≡ iv
oi-io {x = []} {[]} = refl
oi-io {x = x ∷ xs} {i ∷ iv} with prod (x ∷ xs) ≟ 0
... | yes p = ⊥-elim $ ¬Fin0 $ Πs≡0⇒Fin0 (x ∷ xs) (i ∷ iv) p
... | no ¬p = cong₂ _∷_
                   -- Πiv + i * Πxs
                   (toℕ-injective (trans (toℕ-fromℕ< _)
                                         (trans (cong (_/ prod xs) (toℕ-fromℕ< _))
                                                (hlpr {n = prod xs}
                                                      {a = toℕ (ix-lookup (idx→off xs iv) zero)}
                                                      refl (toℕ<n _)))))
                   (trans (cong (off→idx xs)
                                (trans (cong (λ x → x mod (prod xs) ∷ []) (toℕ-fromℕ< _))
                                       (trans (cong (_∷ []) (a<c⇒c|b⇒[a+b]mod[c]≡a _ (n∣m*n (toℕ i) {n = (prod xs)})))
                                              ixl-cong)))
                          oi-io)
   where
     hlpr : ∀ {m n a x}{≢0} → a + m * n ≡ x → a < n → (x / n) {≢0} ≡ m
     hlpr {m} {n} {a} {x} {≢0} refl a<n = trans (+-distrib-/-∣ʳ {m = a} (m * n) {d = n} {≢0} (n∣m*n m))
                                                (b≡0+c≡a⇒b+c≡a (m<n⇒m/n≡0 a<n) (m*n/n≡m m n))

-- rewrite (v-rm-thm {a = x} {b = prod xs} {x = i} {y = (ix-lookup (idx→off xs iv) zero)} {b≢0 = (a*b≢0⇒b≢0 {a = x} ¬p)})

max_stars_repo_name: ashinkarov/agda-array

max_issues_repo_name: ashinkarov/agda-array

max_forks_repo_name: ashinkarov/agda-array


text:
module Everything where

import BoolMatcher
import Eq
import Prelude
import RegExps
import Setoids
import SimpleMatcher


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

module Data.Functor where

open import Prelude

record Functor ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    F : Type ℓ₁ → Type ℓ₂
    map : (A → B) → F A → F B

    identity : map {A = A} id ≡ id
    compose : (f : B → C) (g : A → B) → map (f ∘ g) ≡ map f ∘ map g

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module GUIgeneric.GUI  where

open import GUIgeneric.Prelude
open import GUIgeneric.GUIDefinitions

Frame : Set
Frame  = ComponentEls frame

logOn : Bool
logOn = true

log : {A : Set} → String → (f : Unit → IO GuiLev1Interface ∞ A) →
         IO GuiLev1Interface ∞ A
log s f = if logOn then (do (putStrLn s) λ x → f x) else f unit

module _ where
  FFIcomponents : {c : Component}(e :  ComponentEls c) → Set
  FFIcomponents {c} (add i e e' _) = FFIcomponents e × FFIcomponents e'
  FFIcomponents {frame} (createC tt) = FFIFrame
  FFIcomponents {atomicComp} (createC (button x)) = FFIButton
  FFIcomponents {atomicComp} (createC (txtbox y)) = FFITextCtrl

  ffiComponentsToFrame : (e : ComponentEls frame)(ffi : FFIcomponents e) → FFIFrame
  ffiComponentsToFrame (createC x) ffi = ffi
  ffiComponentsToFrame (add c'c e e₁ _) (ffie , ffie₁) = ffiComponentsToFrame e₁ ffie₁

  FFIcomponentsReduce : {c c' : Component}(e : ComponentEls c)(e' : ComponentEls c')
                      (ee' : e <c e')
                      (ff1 : FFIcomponents e')
                       → FFIcomponents e
  FFIcomponentsReduce e (add i .e e'' _) (addsub i' .e .e'' _) ffi1 = proj₁ ffi1
  FFIcomponentsReduce e (add i e' .e _) (addlift i' .e' .e _) ffi1 = proj₂ ffi1

  FFIcomponentsReduce+ : {c c' : Component}(e : ComponentEls c)(e' : ComponentEls c')
                      (ee' : e <=c+ e')
                      (ffi : FFIcomponents e')
                       → FFIcomponents e
  FFIcomponentsReduce+ e .e (in0= .e) ffi1 = ffi1
  FFIcomponentsReduce+ e e' (in2= .e e'₁ .e' x ee') ffi1 =
    FFIcomponentsReduce e e'₁ x (FFIcomponentsReduce+ e'₁ e' ee' ffi1)

  data SemiDec (A : Frame → Set) : Set where
    isEmpty     : ((f : Frame) → A f → ⊥) → SemiDec A
    posNonEmpty : SemiDec A

  data MethodsStruct : Set where
      fficom : MethodsStruct
      ⊥^     : MethodsStruct
      _⊎^_   : (m m' : MethodsStruct) → MethodsStruct
      _⊎^unoptimized_   : (m m' : MethodsStruct) → MethodsStruct

  mutual

    methodsStruct2Method : (g : Frame)(m : MethodsStruct)  → Set
    methodsStruct2Method g fficom = FFIcomponents g
    methodsStruct2Method g ⊥^ = ⊥
    methodsStruct2Method g (m ⊎^ m₁) = methodsStruct2Methodaux g m m₁
                                        (methodsUnivIsEmpty  m)
                                        (methodsUnivIsEmpty  m₁)
    methodsStruct2Method g (m ⊎^unoptimized m₁) = methodsStruct2Method g m ⊎ methodsStruct2Method g m₁

    methodsStruct2Methodaux :  (g : Frame) (m m' : MethodsStruct)
                           (s  : SemiDec (λ g → methodsStruct2Method g m))
                           (s' : SemiDec (λ g → methodsStruct2Method g m'))
                           → Set
    methodsStruct2Methodaux g m m' s (isEmpty s') = methodsStruct2Method g m
    methodsStruct2Methodaux g m m' (isEmpty x) posNonEmpty = methodsStruct2Method g m'
    methodsStruct2Methodaux g m m' posNonEmpty posNonEmpty = methodsStruct2Method g m ⊎ methodsStruct2Method g m'

    methodsUnivIsEmpty : (m : MethodsStruct) → SemiDec (λ g → methodsStruct2Method g m)
    methodsUnivIsEmpty  fficom = posNonEmpty
    methodsUnivIsEmpty  ⊥^ = isEmpty (λ g → λ ())
    methodsUnivIsEmpty  (m ⊎^ m₁) =
                methodsUnivIsEmptyaux  m m₁
                  (methodsUnivIsEmpty   m)
                  (methodsUnivIsEmpty  m₁)
    methodsUnivIsEmpty  (m ⊎^unoptimized m₁) = posNonEmpty

    methodsUnivIsEmptyaux :  (m m' : MethodsStruct)
                           (s  : SemiDec (λ g → methodsStruct2Method g m ))
                           (s' : SemiDec (λ g → methodsStruct2Method g m' ))
                           → SemiDec (λ g → methodsStruct2Methodaux g m m' s s')
    methodsUnivIsEmptyaux  m m' s (isEmpty s') = s
    methodsUnivIsEmptyaux  m m' (isEmpty x) posNonEmpty = posNonEmpty
    methodsUnivIsEmptyaux  m m' posNonEmpty posNonEmpty = posNonEmpty

  inj₁MUaux : (g : Frame) (m m' : MethodsStruct)
                   (s  : SemiDec (λ g → methodsStruct2Method g m ))
                   (s'  : SemiDec (λ g → methodsStruct2Method g m' ))
                   (u : methodsStruct2Method g m)
                   → methodsStruct2Methodaux g m m' s s'
  inj₁MUaux g m m' s (isEmpty x) u = u
  inj₁MUaux g m m' (isEmpty x) posNonEmpty u = ⊥-elim (x g u)
  inj₁MUaux g m m' posNonEmpty posNonEmpty u = inj₁ u

  inj₁MUoptimized : (g : Frame) (m m' : MethodsStruct)(u : methodsStruct2Method g m )-- (isOpt : Bool)
                   → methodsStruct2Method g (m ⊎^ m') --isOpt
  inj₁MUoptimized g m m' u = inj₁MUaux g m m'
                         (methodsUnivIsEmpty  m)
                         (methodsUnivIsEmpty  m') u

  inj₁MUUnoptimized : (g : Frame) (m m' : MethodsStruct)(u : methodsStruct2Method g m )-- (isOpt : Bool)
                   → methodsStruct2Method g (m ⊎^unoptimized m') --isOpt
  inj₁MUUnoptimized g m m' u = inj₁ u

  inj₂MUaux : (g : Frame) (m m' : MethodsStruct)
                   (s  : SemiDec (λ g → methodsStruct2Method g m))
                   (s'  : SemiDec (λ g → methodsStruct2Method g m' ))
                   (u : methodsStruct2Method g m')
                   → methodsStruct2Methodaux g m m' s s'
  inj₂MUaux g m m' s (isEmpty x) u = ⊥-elim (x g u)
  inj₂MUaux g m m' (isEmpty x) posNonEmpty u = u
  inj₂MUaux g m m' posNonEmpty posNonEmpty u = inj₂ u

  inj₂MUoptimized : (g : Frame) (m m' : MethodsStruct)(u : methodsStruct2Method g m' )
                   → methodsStruct2Method g (m ⊎^ m') --isOpt
  inj₂MUoptimized g m m' u = inj₂MUaux g m m'
                         (methodsUnivIsEmpty  m)
                         (methodsUnivIsEmpty  m') u

  inj₂MUUnoptimized : (g : Frame) (m m' : MethodsStruct)(u : methodsStruct2Method g m' )
                   → methodsStruct2Method g (m ⊎^unoptimized m') --isOpt
  inj₂MUUnoptimized g m m' u = inj₂ u

  methodStruct : {c : Component}(e : ComponentEls c) → MethodsStruct
  methodStruct (add c'c x x₁ optimized) = methodStruct x  ⊎^ methodStruct x₁
  methodStruct (add c'c x x₁ notOptimized) = methodStruct x  ⊎^unoptimized methodStruct x₁
  methodStruct {atomicComp} (createC (button s)) = fficom
  methodStruct {atomicComp} (createC (txtbox s)) = ⊥^
  methodStruct _  = ⊥^

  methods : {c : Component}(e : ComponentEls c)(g : Frame) → Set
  methods e g =  methodsStruct2Method g (methodStruct e)

  methodsG : (g : Frame) → Set
  methodsG g =  methods g g

  methodLift : {c c'' : Component}(e : ComponentEls c)(e'₁ : ComponentEls c'')
               (g : Frame) (x : e <c e'₁)  (m : methods e g )
                → methods e'₁ g
  methodLift e .(add i e e₁ optimized) g (addsub i .e e₁ optimized) m =
                 inj₁MUoptimized g
                   (methodStruct e)
                   (methodStruct e₁)
                m
  methodLift e .(add i e e₁ notOptimzed) g (addsub i .e e₁ notOptimzed) m =
               inj₁MUUnoptimized g
                   (methodStruct e)
                   (methodStruct e₁)
                m

  methodLift e .(add i e'₂ e optimized) g (addlift i e'₂ .e optimized) m =
                 inj₂MUoptimized g
                    (methodStruct e'₂)
                    (methodStruct e)
                 m

  methodLift e .(add i e'₂ e notOptimzed) g (addlift i e'₂ .e notOptimzed) m =
                inj₂MUUnoptimized g
                    (methodStruct e'₂)
                    (methodStruct e)
                 m

  methodLift+ : {c c' : Component}(e : ComponentEls c)(e' : ComponentEls c')
                (g : Frame)(ee' : e <=c+ e')
                (m : methods e g)
                → methods e' g
  methodLift+ e .e g (in0= .e) m = m
  methodLift+ e e' g (in2= .e e'₁ .e' x ee'') m =
    methodLift+ e'₁ e' g ee'' (methodLift e e'₁ g x m)

data returnType (f : Frame) : Set where
    noChange           :  returnType f
    changedAttributes  :  properties f  →  returnType f
    changedGUI
      :  (fNew : Frame)  →  (properties fNew) → returnType f

nextStateFrame : (f : Frame)(r : returnType f) → Frame
nextStateFrame f noChange = f
nextStateFrame f (changedAttributes x) = f
nextStateFrame f (changedGUI fNew x) = fNew

handlerInterface : Interfaceˢ
handlerInterface .Stateˢ       = Frame
handlerInterface .Methodˢ f    = methodsG f
handlerInterface .Resultˢ f m  = returnType f
handlerInterface .nextˢ f m r  = nextStateFrame f r

HandlerObject : ∀ i → Frame → Set
HandlerObject i g =
  IOObjectˢ  GuiLev1Interface  handlerInterface i g

StateAndGuiObj : Set
StateAndGuiObj = Σ[ g ∈ Frame ] (properties g) × (HandlerObject ∞ g)

StateAndFFIComp : Set
StateAndFFIComp = Σ[ g ∈ Frame ] FFIcomponents g

--
-- Step 3 : create object of type HandlerObject
--

SingleMVar : {A : Set} → (mvar : MVar A) → VarList
SingleMVar {A} mvar = addVar mvar []

initHandlerMVar : (l : VarList) (g : Frame)
                     (a : properties g)
                     (f : HandlerObject ∞ g)
              → IOˢ GuiLev2Interface ∞
                    (λ s → Σ[ mvar ∈ MVar StateAndGuiObj ]
                    s ≡ addVar mvar l  ) l
initHandlerMVar l g a f = doˢ (createVar {_}{StateAndGuiObj} (g , a , f)) λ mvar →
                         returnˢ (mvar , refl)

initFFIMVar : (g : Frame)
              → (comp : (FFIcomponents g))
              → IOˢ GuiLev2Interface ∞
                    (λ s → Σ[ mvar ∈ MVar StateAndFFIComp ]
                    s ≡ SingleMVar mvar  ) []
initFFIMVar g comp = doˢ (createVar {_}{StateAndFFIComp} (g , comp)) λ mvar →
                        returnˢ (mvar , refl)

module _ where
  frameToEnclosing : (e : ComponentEls frame)(ffi : FFIcomponents e) → FFIFrame
  frameToEnclosing (createC x) ffi = ffi
  frameToEnclosing (add i e e₁ _) (proj₃ , proj₄) = frameToEnclosing e₁ proj₄

  componentToEnclosingIndex : (c : Component) → Set
  componentToEnclosingIndex frame = ⊥
  componentToEnclosingIndex atomicComp = ⊤

  componentToEnclosings : (c : Component)(i : componentToEnclosingIndex c) → Set
  componentToEnclosings frame ()
  componentToEnclosings atomicComp tt = FFIFrame

  createComp : {c : Component}{s : GuiLev2State}(e : ComponentEls c)
                    (enclosings : (i : componentToEnclosingIndex c) → componentToEnclosings c i)
                        → (existingFrame : Maybe FFIFrame) → IOₚˢ GuiLev2Interface ∞ (FFIcomponents e) s s

  createComp {frame} (createC fr) enc (just ffiFrame) = returnˢ (refl , ffiFrame)
  createComp {frame} (createC fr) enc nothing =
     doˢ (level1C createWxFrame) λ frFFI → returnˢ (refl , frFFI)

  createComp {frame} (add buttonFrame e frameEl _) enc maybeFr =
      createComp frameEl enc maybeFr >>=ₚˢ λ frameComp →
      createComp e (λ x → frameToEnclosing frameEl frameComp) maybeFr >>=ₚˢ λ buttonComp →
      returnˢ (refl , buttonComp , frameComp)
  createComp {atomicComp} (createC (button x)) enc maybeFr =
    doˢ (level1C (createButton (enc tt) x)) λ bt →
    returnˢ (refl , bt)

  createComp {atomicComp} (createC (txtbox x)) enc maybeFr =
    doˢ (level1C (createTextCtrl (enc tt) x)) λ txt →
    returnˢ (refl , txt)

  createComp {atomicComp} (add () e e₁ _) x y

  createFrame : (g : Frame) → IOₚˢ GuiLev2Interface ∞ (FFIcomponents g) [] []
  createFrame g = createComp {frame} g (λ x → ⊥-elim x) nothing

  reCreateFrame : {s : GuiLev2State}(g : Frame)(f : FFIFrame) → IOₚˢ GuiLev2Interface ∞ (FFIcomponents g) s s
  reCreateFrame g fr = createComp {frame} g (λ x → ⊥-elim x) (just fr)

module _ where
  ButtonComp : Set
  ButtonComp = ComponentEls atomicComp

  button2Frame : (bt  : ButtonComp)(g   : Frame)(ffi : FFIcomponents g)
               (rel : bt <=c+ g) → FFIFrame
  button2Frame bt g ffi (in2= {c' = frame} .bt .(add c'c bt e _) .g (addsub c'c .bt e _) rel) = ffiComponentsToFrame e (FFIcomponentsReduce+ e g aux ffi)
                       where
                            aux : e <=c+ g
                            aux = in2= e (add c'c bt e _) g (addlift c'c bt e _) rel
  button2Frame bt g ffi (in2= {c' = atomicComp} .bt .(add _ bt e _) .g (addsub () .bt e _) rel)
  button2Frame bt g ffi (in2= .bt .(add _ e'₁ bt _) .g (addlift {frame} () e'₁ .bt _) (in2= .(add _ e'₁ bt _) e' .g x rel))
  button2Frame bt g ffi (in2= .bt .(add _ e'₁ bt _) .g (addlift {atomicComp} () e'₁ .bt _) (in2= .(add _ e'₁ bt _) e' .g x rel))

  buttonHandleraux2 : ∀{i} → (bt  : ButtonComp)
                         (g   : Frame)
                         (ffi : FFIcomponents g)
                         (rel : bt <=c+ g)
                         (m   : methods bt g)
                         (a  : properties g)
                         (obj : HandlerObject ∞ g)
                         (r    : returnType g)
                         (obj' : IOObjectˢ GuiLev1Interface handlerInterface ∞
                                (nextStateFrame g r))
                         → IO GuiLev1Interface i StateAndGuiObj
  buttonHandleraux2 bt g ffi rel m a obj noChange obj' = return (g , a , obj')
  buttonHandleraux2 bt g ffi rel m a obj (changedAttributes a') obj' =
                    log "Changing Attributes Directly" λ _ →
                    return (g , a' , obj')
  buttonHandleraux2 (createC x) g ffi rel m a obj (changedGUI gNew a') obj' =
                    log "Firing GUI change ----> SEND FIRE" λ _ →
                    do (fireCustomEvent (button2Frame (createC x) g ffi rel)) λ _ →
                    return (gNew , a' , obj')

  buttonHandleraux2 (add () bt bt₁ _) g ffi rel m a obj (changedGUI gNew a') obj'

  buttonHandleraux : ∀{i} → (bt  : ButtonComp)
                         (g   : Frame)
                         (ffi : FFIcomponents g)
                         (rel : bt <=c+ g)
                         (m   : methods bt g)
                         (gNew  : Frame)
                         (a  : properties gNew)
                         (obj : HandlerObject ∞ gNew)
                         (dec : Dec (g ≡ gNew))
                         → IO GuiLev1Interface i StateAndGuiObj
  buttonHandleraux bt g ffi rel m .g a obj (Dec.yes refl)
               = method obj (methodLift+ bt g g  rel m) >>= λ { (r , obj') →
                 buttonHandleraux2 bt g ffi rel m a obj r obj'}
  buttonHandleraux bt g ffi rel m gNew a obj (Dec.no ¬p)
              = log "ERROR: button handler is called for wrong GUI !!" λ _ →
                return (gNew , a , obj)

  buttonHandler : ∀{i} → (bt  : ButtonComp)
                         (g   : Frame)
                         (ffi : FFIcomponents g)
                         (rel : bt <=c+ g)
                         (m   : methods bt g)
                         (obj : StateAndGuiObj)
                         → IO GuiLev1Interface i StateAndGuiObj
  buttonHandler {i} bt g ffi rel m (gNew , a , obj) = buttonHandleraux {i} bt g ffi rel m gNew a obj (g ≟Comp gNew)

  setHandler : ∀{i} → (c : Component)
                      (cels : ComponentEls c)
                      (g : Frame)
                      (ffiComp : FFIcomponents g)
                      (rel : cels <=c+ g)
                      (mvar : MVar StateAndGuiObj)
                      (restList : VarList)
                      → IOˢ GuiLev2Interface i (λ s' → s' ≡ addVar mvar restList  × Unit)
                                                (addVar mvar restList)

  setHandler .frame (add buttonFrame cels cels₁ _) g ffi rel mvar restList =
    setHandler frame cels₁ g ffi
                (in2= cels₁ (add buttonFrame cels cels₁ _) g (addlift buttonFrame cels cels₁ _) rel)
                mvar restList >>=ₚˢ λ r →
    setHandler atomicComp cels g ffi (in2= cels (add buttonFrame cels cels₁ _) g (addsub buttonFrame cels cels₁ _) rel)  mvar restList >>=ₚˢ λ r →
    returnˢ (refl , _)

  setHandler frame (createC tt) g ffi rel  mvar restList = returnˢ (refl , _)

  setHandler atomicComp (createC (button x)) g ffi (in2= .(createC (button x)) e' .g x₁ rel)  mvar restList =
     doˢ (setButtonHandler (FFIcomponentsReduce (createC (button x)) e' x₁
                              (FFIcomponentsReduce+ e' g rel ffi)  )

         [ (λ obj → buttonHandler (createC (button x)) g ffi
                      (in2= (createC (button x)) e' g x₁ rel) ffi (varListProj₁ restList obj)
                     >>= (λ { (g' , obj') → return (varListUpdateProj₁ restList  ( g' , obj') obj)}))]) λ _ →

     returnˢ (refl , _)

  setHandler atomicComp (createC (txtbox x)) g ffi (in2= .(createC (txtbox x)) e' .g x₁ rel)  mvar restList =      returnˢ (refl , _)

  setHandlerG : ∀{i} → (g : Frame)
                      (ffiComp : FFIcomponents g)
                      (mvar : MVar StateAndGuiObj)
                      (restList : VarList)
                      → IOˢ GuiLev2Interface i (λ s → s ≡ addVar mvar restList × Unit) (addVar mvar restList)
  setHandlerG g ffi mvar restList = setHandler frame g g ffi (in0= g) mvar restList

  deleteComp : {c : Component}{s : GuiLev2State}(e : ComponentEls c)(ffi : FFIcomponents e)
                          → IOₚˢ GuiLev2Interface ∞ Unit s s

  deleteComp {frame} (createC fr) _ = returnˢ (refl , _)

  deleteComp {frame} (add x be frameEl _) (ffi , ffis) =
    deleteComp be ffi >>=ₚˢ λ _ →
    deleteComp frameEl ffis >>=ₚˢ λ r →
    returnˢ (refl , _)

  deleteComp {atomicComp} (createC (button x)) ffiButton =
    doˢ (level1C (deleteButton ffiButton)) λ _ →
    returnˢ (refl , _)

  deleteComp {atomicComp} (createC (txtbox y)) ffiTextCtrl =
    doˢ (level1C (deleteTextCtrl ffiTextCtrl)) λ _ →
    returnˢ (refl , _)

  deleteComp {atomicComp} (add () a b _) y

  setAttributes : {c : Component}(i : Size)(e : ComponentEls c)(a : properties e)
                      (ffi : FFIcomponents e)
                          → IO GuiLev1Interface i ⊤

  setAttributes {frame} i (createC fr) (a , b , c , d) x =
    log " setting properties for Frame " λ _ →
    do (setChildredLayout x a b c d) λ _ →
    return tt

  setAttributes {frame} i (add x be frameEl _) (a , as) (ffi , ffis) =

    setAttributes i be a ffi >>= λ _ →
    setAttributes i frameEl as ffis >>= λ r →
    return tt

  setAttributes {atomicComp} i (createC (button x)) propColor ffiButton =
    do (setAttribButton ffiButton propColor) λ _ →
    return tt

  setAttributes {atomicComp} i (createC (txtbox y)) propColor ffiTextCtrl =
    do (setAttribTextCtrl ffiTextCtrl propColor) λ _ →
    return tt

  setAttributes {atomicComp} i (add () a b _) y z

getFrameGen : (g : Frame)(cp : FFIcomponents g) → FFIFrame
getFrameGen (createC x) cp = cp
getFrameGen (add buttonFrame g g₁ _) (compg , compg₁) = getFrameGen g₁ compg₁

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
{-# OPTIONS --without-K --exact-split --safe #-}

open import Fragment.Equational.Theory

module Fragment.Equational.Model.Properties (Θ : Theory) where

open import Fragment.Equational.Model.Base Θ
open import Fragment.Equational.Model.Synthetic Θ
open import Fragment.Algebra.Homomorphism (Σ Θ)
open import Fragment.Algebra.Free (Σ Θ)
open import Fragment.Setoid.Morphism using (_↝_)

open import Level using (Level)
open import Function using (_∘_)

open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc; fromℕ)
open import Data.Vec using (Vec; []; _∷_; map)
open import Data.Product using (proj₁; proj₂)
open import Data.Vec.Relation.Binary.Pointwise.Inductive
  using (Pointwise; []; _∷_)

open import Relation.Binary using (Setoid)
import Relation.Binary.Reasoning.Setoid as Reasoning

private
  variable
    a ℓ : Level

module _ {n} (A : Model {a} {ℓ}) (θ : Env ∥ A ∥ₐ n) where

  private

    module S = Setoid ∥ A ∥/≈
    open Reasoning ∥ A ∥/≈

    mutual
      map-∣interp∣-cong : ∀ {m} {xs ys : Vec ∥ J n ∥ m}
                          → Pointwise ≈[ J n ] xs ys
                          → Pointwise ≈[ A ] (map ∣ inst ∥ A ∥ₐ θ ∣ xs)
                                             (map ∣ inst ∥ A ∥ₐ θ ∣ ys)
      map-∣interp∣-cong []       = []
      map-∣interp∣-cong (p ∷ ps) = ∣interp∣-cong p ∷ map-∣interp∣-cong ps

      ∣interp∣-cong : Congruent ≈[ J n ] ≈[ A ] ∣ inst ∥ A ∥ₐ θ ∣
      ∣interp∣-cong refl          = S.refl
      ∣interp∣-cong (sym p)       = S.sym (∣interp∣-cong p)
      ∣interp∣-cong (trans p q)   = S.trans (∣interp∣-cong p) (∣interp∣-cong q)
      ∣interp∣-cong (inherit p)   = ∣ inst ∥ A ∥ₐ θ ∣-cong p
      ∣interp∣-cong (cong f {xs = xs} {ys = ys} ps) = begin
          ∣ inst ∥ A ∥ₐ θ ∣ (term f xs)
        ≈⟨ S.sym (∣ inst ∥ A ∥ₐ θ ∣-hom f xs) ⟩
          A ⟦ f ⟧ (map ∣ inst ∥ A ∥ₐ θ ∣ xs)
        ≈⟨ (A ⟦ f ⟧-cong) (map-∣interp∣-cong ps) ⟩
          A ⟦ f ⟧ (map ∣ inst ∥ A ∥ₐ θ ∣ ys)
        ≈⟨ ∣ inst ∥ A ∥ₐ θ ∣-hom f ys ⟩
          ∣ inst ∥ A ∥ₐ θ ∣ (term f ys)
        ∎
      ∣interp∣-cong (axiom eq θ') = begin
          ∣ inst ∥ A ∥ₐ θ ∣ (∣ inst (F n) θ' ∣ lhs)
        ≈⟨ inst-assoc (F n) θ' (inst ∥ A ∥ₐ θ) {x = lhs} ⟩
          ∣ inst ∥ A ∥ₐ (∣ inst ∥ A ∥ₐ θ ∣ ∘ θ') ∣ lhs
        ≈⟨ ∥ A ∥ₐ-models eq _ ⟩
          ∣ inst ∥ A ∥ₐ (∣ inst ∥ A ∥ₐ θ ∣ ∘ θ') ∣ rhs
        ≈⟨ S.sym (inst-assoc (F n) θ' (inst ∥ A ∥ₐ θ) {x = rhs}) ⟩
          ∣ inst ∥ A ∥ₐ θ ∣ (∣ inst (F n) θ' ∣ rhs)
        ∎
        where lhs = proj₁ (Θ ⟦ eq ⟧ₑ)
              rhs = proj₂ (Θ ⟦ eq ⟧ₑ)

    ∣interp∣⃗ : ∥ J n ∥/≈ ↝ ∥ A ∥/≈
    ∣interp∣⃗ = record { ∣_∣      = ∣ inst ∥ A ∥ₐ θ ∣
                       ; ∣_∣-cong = ∣interp∣-cong
                       }

  interp : ∥ J n ∥ₐ ⟿ ∥ A ∥ₐ
  interp = record { ∣_∣⃗    = ∣interp∣⃗
                  ; ∣_∣-hom = ∣ inst ∥ A ∥ₐ θ ∣-hom
                  }

atomise : (n : ℕ) → ∥ J (suc n) ∥
atomise n = atom (dyn (fromℕ n))

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

raise : ∀ {n} → ∥ J n ∥ₐ ⟿ ∥ J (suc n) ∥ₐ
raise {n} = interp (J (suc n)) (λ k → atom (dyn (up k)))

step : ∀ {n} → ∥ J n ∥ₐ ⟿ ∥ J (suc n) ∥ₐ
step {n} = interp (J (suc n)) (λ k → atom (dyn (suc k)))

mutual

  map-step-raise : ∀ {n m} → (xs : Vec ∥ J n ∥ m)
                   → Pointwise ≈[ J (suc (suc n)) ]
                               (map ∣ step {suc n} ⊙ raise {n} ∣ xs)
                               (map ∣ raise {suc n} ⊙ step {n} ∣ xs)
  map-step-raise []       = []
  map-step-raise (x ∷ xs) = step-raise {x = x} ∷ map-step-raise xs

  step-raise : ∀ {n} → step {suc n} ⊙ raise {n} ≗ raise {suc n} ⊙ step {n}
  step-raise {n} {atom (dyn k)} = refl
  step-raise {n} {term f xs}    = begin
      ∣ step ⊙ raise ∣ (term f xs)
    ≈⟨ sym (∣ step ⊙ raise ∣-hom f xs) ⟩
      term f (map ∣ step ⊙ raise ∣ xs)
    ≈⟨ cong f (map-step-raise xs) ⟩
      term f (map ∣ raise ⊙ step ∣ xs)
    ≈⟨ ∣ raise ⊙ step ∣-hom f xs ⟩
      ∣ raise ⊙ step ∣ (term f xs)
    ∎
    where open Reasoning ∥ J (suc (suc n)) ∥/≈

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


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

open import HoTT

module groups.KernelCstImageCst {i j k}
  (G : Group i) (H : Group j) (K : Group k)
  (H-ab : is-abelian H) where

  private
    module H = Group H

  open import groups.KernelImage {G = G} {H = H} {K = K} cst-hom cst-hom H-ab

  Ker-cst-quot-Im-cst : Ker/Im ≃ᴳ H
  Ker-cst-quot-Im-cst = ≃-to-≃ᴳ (equiv to from to-from from-to) to-pres-comp where
    to : Ker/Im.El → H.El
    to = SetQuot-rec H.El-level to' to-rel where
      to' : Ker.El (cst-hom {G = H} {H = K}) → H.El
      to' ker = fst ker

      abstract
        to-rel : ∀ {h₁ h₂} → ker/im-rel' h₁ h₂ → h₁ == h₂
        to-rel {h₁} {h₂} = Trunc-rec (H.El-level _ _)
          λ{(_ , 0=h₁h₂⁻¹) → H.zero-diff-same h₁ h₂ (! 0=h₁h₂⁻¹)}

    from : H.El → Ker/Im.El
    from h = q[ h , idp ]

    abstract
      to-from : ∀ h → to (from h) == h
      to-from h = idp

      from-to : ∀ k/i → from (to k/i) == k/i
      from-to = SetQuot-elim (λ _ → =-preserves-set SetQuot-level)
        (λ _ → ap q[_] $ ker-El=-out idp)
        (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

      to-pres-comp : preserves-comp Ker/Im.comp H.comp to
      to-pres-comp = SetQuot-elim
        (λ _ → Π-is-set λ _ → =-preserves-set H.El-level)
        (λ _ → SetQuot-elim
          (λ _ → =-preserves-set H.El-level)
          (λ _ → idp)
          (λ _ → prop-has-all-paths-↓ (H.El-level _ _)))
        (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → H.El-level _ _))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

module HITs.PropositionalTruncation.Equivalence where

open import Prelude
open import Relation.Binary
open import HITs.PropositionalTruncation
open import HITs.PropositionalTruncation.Sugar

trunc-equivalence : ∀ {a} {A : Type a} → Equivalence A a → Equivalence A a
trunc-equivalence e .Equivalence._≋_ x y = ∥ Equivalence._≋_ e x y ∥
trunc-equivalence e .Equivalence.sym = _∥$∥_ (Equivalence.sym e)
trunc-equivalence e .Equivalence.refl = ∣ Equivalence.refl e ∣
trunc-equivalence e .Equivalence.trans xy yz = ⦇ (Equivalence.trans e) xy yz ⦈


text:
{-

Computable stuff constructed from the Combinatorics of Finite Sets

-}
{-# OPTIONS --safe #-}

module Cubical.Experiments.Combinatorics where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Bool
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Vec

open import Cubical.Data.SumFin renaming (Fin to Fin')
open import Cubical.Data.FinSet.Base
open import Cubical.Data.FinSet.Properties
open import Cubical.Data.FinSet.Constructors
open import Cubical.Data.FinSet.Cardinality
open import Cubical.Data.FinSet.DecidablePredicate
open import Cubical.Data.FinSet.Quotients

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidablePropositions
  hiding (DecProp) renaming (DecProp' to DecProp)
open import Cubical.Relation.Binary

open import Cubical.Functions.Embedding
open import Cubical.Functions.Surjection

private
  variable
    ℓ ℓ' ℓ'' : Level

-- convenient renaming

Fin : ℕ → FinSet ℓ-zero
Fin n = _ , isFinSetFin {n = n}

-- explicit numbers

s2 : card (_ , isFinSet≃ (Fin 2) (Fin 2)) ≡ 2
s2 = refl

s3 : card (_ , isFinSet≃ (Fin 3) (Fin 3)) ≡ 6
s3 = refl

a3,2 : card (_ , isFinSet↪ (Fin 2) (Fin 3)) ≡ 6
a3,2 = refl

2^4 : card (_ , isFinSet→ (Fin 4) (Fin 2)) ≡ 16
2^4 = refl

-- construct numerical functions from list
getFun : {n : ℕ} → Vec ℕ n → Fin n .fst → ℕ
getFun {n = n} ns = fun n ns
  where
    fun : (n : ℕ) → Vec ℕ n → Fin' n → ℕ
    fun 0 _ _ = 0
    fun (suc m) (n ∷ ns) (inl tt) = n
    fun (suc m) (n ∷ ns) (inr x) = fun m ns x

-- an example function
f = getFun (3 ∷ 1 ∷ 4 ∷ 1 ∷ 5 ∷ 9 ∷ 2 ∷ 6 ∷ [])

-- the total sum
s : sum (Fin _) f ≡ 31
s = refl

-- the total product
p : prod (Fin _) f ≡ 6480
p = refl

-- the maximal value
m : maxValue (Fin _) f ∣ fzero ∣ ≡ 9
m = refl

-- the number of numeral 1
n1 : card (_ , isFinSetFiberDisc (Fin _) ℕ discreteℕ f 1) ≡ 2
n1 = refl

-- a somewhat trivial equivalence relation making everything equivalent
R : {n : ℕ} → Fin n .fst → Fin n .fst → Type
R _ _ = Unit

isDecR : {n : ℕ} → (x y : Fin n .fst) → isDecProp (R {n = n} x y)
isDecR _ _ = true , idEquiv _

open BinaryRelation
open isEquivRel

isEquivRelR : {n : ℕ} → isEquivRel (R {n = n})
isEquivRelR {n = n} .reflexive _ = tt
isEquivRelR {n = n} .symmetric _ _ tt = tt
isEquivRelR {n = n} .transitive _ _ _ tt tt = tt

collapsed : (n : ℕ) → FinSet ℓ-zero
collapsed n = _ , isFinSetQuot (Fin n) R isEquivRelR isDecR

-- this number should be 1
≡1 : card (collapsed 2) ≡ 1
≡1 = refl

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module NoUniverseCheck where

data M : Set -> Set where
  return : forall {a}   -> a -> M a
  _>>=_  : forall {a b} -> M a -> (a -> M b) -> M b

record Cat : Set where
  field
    Obj : Set
    Mor : Obj -> Obj -> Set

data _≡_ {a : Set} (x : a) : a -> Set where
  refl : x ≡ x

CatOfCat : Cat
CatOfCat = record
  { Obj = Cat
  ; Mor = _≡_
  }

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via `Relation.Binary`.

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

module Relation.Binary.Definitions where

open import Agda.Builtin.Equality using (_≡_)

open import Data.Maybe.Base using (Maybe)
open import Data.Product using (_×_)
open import Data.Sum.Base using (_⊎_)
open import Function.Base using (_on_; flip)
open import Level
open import Relation.Binary.Core
open import Relation.Nullary using (Dec; ¬_)

private
  variable
    a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Definitions
------------------------------------------------------------------------

-- Reflexivity - defined without an underlying equality. It could
-- alternatively be defined as `_≈_ ⇒ _∼_` for some equality `_≈_`.

-- Confusingly the convention in the library is to use the name "refl"
-- for proofs of Reflexive and `reflexive` for proofs of type `_≈_ ⇒ _∼_`,
-- e.g. in the definition of `IsEquivalence` later in this file. This
-- convention is a legacy from the early days of the library.

Reflexive : Rel A ℓ → Set _
Reflexive _∼_ = ∀ {x} → x ∼ x

-- Generalised symmetry.

Sym : REL A B ℓ₁ → REL B A ℓ₂ → Set _
Sym P Q = P ⇒ flip Q

-- Symmetry.

Symmetric : Rel A ℓ → Set _
Symmetric _∼_ = Sym _∼_ _∼_

-- Generalised transitivity.

Trans : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k

-- A flipped variant of generalised transitivity.

TransFlip : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k

-- Transitivity.

Transitive : Rel A ℓ → Set _
Transitive _∼_ = Trans _∼_ _∼_ _∼_

-- Generalised antisymmetry

Antisym : REL A B ℓ₁ → REL B A ℓ₂ → REL A B ℓ₃ → Set _
Antisym R S E = ∀ {i j} → R i j → S j i → E i j

-- Antisymmetry.

Antisymmetric : Rel A ℓ₁ → Rel A ℓ₂ → Set _
Antisymmetric _≈_ _≤_ = Antisym _≤_ _≤_ _≈_

-- Irreflexivity - this is defined terms of the underlying equality.

Irreflexive : REL A B ℓ₁ → REL A B ℓ₂ → Set _
Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)

-- Asymmetry.

Asymmetric : Rel A ℓ → Set _
Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)

-- Generalised connex - exactly one of the two relations holds.

Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _
Connex P Q = ∀ x y → P x y ⊎ Q y x

-- Totality.

Total : Rel A ℓ → Set _
Total _∼_ = Connex _∼_ _∼_

-- Generalised trichotomy - exactly one of three types has a witness.

data Tri (A : Set a) (B : Set b) (C : Set c) : Set (a ⊔ b ⊔ c) where
  tri< : ( a :   A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
  tri≈ : (¬a : ¬ A) ( b :   B) (¬c : ¬ C) → Tri A B C
  tri> : (¬a : ¬ A) (¬b : ¬ B) ( c :   C) → Tri A B C

-- Trichotomy.

Trichotomous : Rel A ℓ₁ → Rel A ℓ₂ → Set _
Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y)
  where _>_ = flip _<_

-- Generalised maximum element.

Max : REL A B ℓ → B → Set _
Max _≤_ T = ∀ x → x ≤ T

-- Maximum element.

Maximum : Rel A ℓ → A → Set _
Maximum = Max

-- Generalised minimum element.

Min : REL A B ℓ → A → Set _
Min R = Max (flip R)

-- Minimum element.

Minimum : Rel A ℓ → A → Set _
Minimum = Min

-- Unary relations respecting a binary relation.

_⟶_Respects_ : (A → Set ℓ₁) → (B → Set ℓ₂) → REL A B ℓ₃ → Set _
P ⟶ Q Respects _∼_ = ∀ {x y} → x ∼ y → P x → Q y

-- Unary relation respects a binary relation.

_Respects_ : (A → Set ℓ₁) → Rel A ℓ₂ → Set _
P Respects _∼_ = P ⟶ P Respects _∼_

-- Right respecting - relatedness is preserved on the right by equality.

_Respectsʳ_ : REL A B ℓ₁ → Rel B ℓ₂ → Set _
_∼_ Respectsʳ _≈_ = ∀ {x} → (x ∼_) Respects _≈_

-- Left respecting - relatedness is preserved on the left by equality.

_Respectsˡ_ : REL A B ℓ₁ → Rel A ℓ₂ → Set _
P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_

-- Respecting - relatedness is preserved on both sides by equality

_Respects₂_ : Rel A ℓ₁ → Rel A ℓ₂ → Set _
P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_)

-- Substitutivity - any two related elements satisfy exactly the same
-- set of unary relations. Note that only the various derivatives
-- of propositional equality can satisfy this property.

Substitutive : Rel A ℓ₁ → (ℓ₂ : Level) → Set _
Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_

-- Decidability - it is possible to determine whether a given pair of
-- elements are related.

Decidable : REL A B ℓ → Set _
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

-- Weak decidability - it is sometimes possible to determine if a given
-- pair of elements are related.

WeaklyDecidable : REL A B ℓ → Set _
WeaklyDecidable _∼_ = ∀ x y → Maybe (x ∼ y)

-- Propositional equality is decidable for the type.

DecidableEquality : (A : Set a) → Set _
DecidableEquality A = Decidable {A = A} _≡_

-- Irrelevancy - all proofs that a given pair of elements are related
-- are indistinguishable.

Irrelevant : REL A B ℓ → Set _
Irrelevant _∼_ = ∀ {x y} (a b : x ∼ y) → a ≡ b

-- Recomputability - we can rebuild a relevant proof given an
-- irrelevant one.

Recomputable : REL A B ℓ → Set _
Recomputable _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y

-- Universal - all pairs of elements are related

Universal : REL A B ℓ → Set _
Universal _∼_ = ∀ x y → x ∼ y

-- Non-emptiness - at least one pair of elements are related.

record NonEmpty {A : Set a} {B : Set b}
                (T : REL A B ℓ) : Set (a ⊔ b ⊔ ℓ) where
  constructor nonEmpty
  field
    {x}   : A
    {y}   : B
    proof : T x y

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

-- Version 1.1

Conn = Connex
{-# WARNING_ON_USAGE Conn
"Warning: Conn was deprecated in v1.1.
Please use Connex instead."
#-}


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

open import lemmas-general
open import lemmas-env
open import lemmas-progress

open import results-checks
open import decidability
open import completeness
open import preservation
open import progress
open import finality
open import eval-checks

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


text:
-- Andreas, 2011-04-14
-- {-# OPTIONS -v tc.cover:20 -v tc.lhs.unify:20 #-}
module Issue291b where

open import Common.Coinduction
open import Common.Equality

data RUnit : Set where
  runit : ∞ RUnit -> RUnit

j : (u : RUnit) -> u ≡ runit (♯ u) -> Set
j u ()

-- needs to fail because of a non strongly rigid occurrence
-- ♯ does not count as a constructor, and that is good!


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers
------------------------------------------------------------------------

module Data.Nat where

open import Function
open import Function.Equality as F using (_⟨$⟩_)
open import Function.Injection using (_↣_)
open import Data.Sum
open import Data.Empty
import Level
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)

------------------------------------------------------------------------
-- The types

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}

infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_

data _≤_ : Rel ℕ Level.zero where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

_<_ : Rel ℕ Level.zero
m < n = suc m ≤ n

_≥_ : Rel ℕ Level.zero
m ≥ n = n ≤ m

_>_ : Rel ℕ Level.zero
m > n = n < m

_≰_ : Rel ℕ Level.zero
a ≰ b = ¬ a ≤ b

_≮_ : Rel ℕ Level.zero
a ≮ b = ¬ a < b

_≱_ : Rel ℕ Level.zero
a ≱ b = ¬ a ≥ b

_≯_ : Rel ℕ Level.zero
a ≯ b = ¬ a > b

-- The following, alternative definition of _≤_ is more suitable for
-- well-founded induction (see Induction.Nat).

infix 4 _≤′_ _<′_ _≥′_ _>′_

data _≤′_ (m : ℕ) : ℕ → Set where
  ≤′-refl :                         m ≤′ m
  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n

_<′_ : Rel ℕ Level.zero
m <′ n = suc m ≤′ n

_≥′_ : Rel ℕ Level.zero
m ≥′ n = n ≤′ m

_>′_ : Rel ℕ Level.zero
m >′ n = n <′ m

------------------------------------------------------------------------
-- A generalisation of the arithmetic operations

fold : {a : Set} → a → (a → a) → ℕ → a
fold z s zero    = z
fold z s (suc n) = s (fold z s n)

module GeneralisedArithmetic {a : Set} (0# : a) (1+ : a → a) where

  add : ℕ → a → a
  add n z = fold z 1+ n

  mul : (+ : a → a → a) → (ℕ → a → a)
  mul _+_ n x = fold 0# (λ s → x + s) n

------------------------------------------------------------------------
-- Arithmetic

pred : ℕ → ℕ
pred zero    = zero
pred (suc n) = n

infixl 7 _*_ _⊓_
infixl 6 _+_ _+⋎_ _∸_ _⊔_

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

{-# BUILTIN NATPLUS _+_ #-}

-- Argument-swapping addition. Used by Data.Vec._⋎_.

_+⋎_ : ℕ → ℕ → ℕ
zero  +⋎ n = n
suc m +⋎ n = suc (n +⋎ m)

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero  = m
zero  ∸ suc n = zero
suc m ∸ suc n = m ∸ n

{-# BUILTIN NATMINUS _∸_ #-}

_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + m * n

{-# BUILTIN NATTIMES _*_ #-}

-- Max.

_⊔_ : ℕ → ℕ → ℕ
zero  ⊔ n     = n
suc m ⊔ zero  = suc m
suc m ⊔ suc n = suc (m ⊔ n)

-- Min.

_⊓_ : ℕ → ℕ → ℕ
zero  ⊓ n     = zero
suc m ⊓ zero  = zero
suc m ⊓ suc n = suc (m ⊓ n)

-- Division by 2, rounded downwards.

⌊_/2⌋ : ℕ → ℕ
⌊ 0 /2⌋           = 0
⌊ 1 /2⌋           = 0
⌊ suc (suc n) /2⌋ = suc ⌊ n /2⌋

-- Division by 2, rounded upwards.

⌈_/2⌉ : ℕ → ℕ
⌈ n /2⌉ = ⌊ suc n /2⌋

------------------------------------------------------------------------
-- Queries

infix 4 _≟_

_≟_ : Decidable {A = ℕ} _≡_
zero  ≟ zero   = yes refl
suc m ≟ suc n  with m ≟ n
suc m ≟ suc .m | yes refl = yes refl
suc m ≟ suc n  | no prf   = no (prf ∘ PropEq.cong pred)
zero  ≟ suc n  = no λ()
suc m ≟ zero   = no λ()

≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
≤-pred (s≤s m≤n) = m≤n

_≤?_ : Decidable _≤_
zero  ≤? _     = yes z≤n
suc m ≤? zero  = no λ()
suc m ≤? suc n with m ≤? n
...            | yes m≤n = yes (s≤s m≤n)
...            | no  m≰n = no  (m≰n ∘ ≤-pred)

-- A comparison view. Taken from "View from the left"
-- (McBride/McKinna); details may differ.

data Ordering : Rel ℕ Level.zero where
  less    : ∀ m k → Ordering m (suc (m + k))
  equal   : ∀ m   → Ordering m m
  greater : ∀ m k → Ordering (suc (m + k)) m

compare : ∀ m n → Ordering m n
compare zero    zero    = equal   zero
compare (suc m) zero    = greater zero m
compare zero    (suc n) = less    zero n
compare (suc m) (suc n) with compare m n
compare (suc .m)           (suc .(suc m + k)) | less    m k = less    (suc m) k
compare (suc .m)           (suc .m)           | equal   m   = equal   (suc m)
compare (suc .(suc m + k)) (suc .m)           | greater m k = greater (suc m) k

-- If there is an injection from a type to ℕ, then the type has
-- decidable equality.

eq? : ∀ {a} {A : Set a} → A ↣ ℕ → Decidable {A = A} _≡_
eq? inj = Dec.via-injection inj _≟_

------------------------------------------------------------------------
-- Some properties

decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
  { Carrier         = ℕ
  ; _≈_             = _≡_
  ; _≤_             = _≤_
  ; isDecTotalOrder = record
      { isTotalOrder = record
          { isPartialOrder = record
              { isPreorder = record
                  { isEquivalence = PropEq.isEquivalence
                  ; reflexive     = refl′
                  ; trans         = trans
                  }
              ; antisym  = antisym
              }
          ; total = total
          }
      ; _≟_  = _≟_
      ; _≤?_ = _≤?_
      }
  }
  where
  refl′ : _≡_ ⇒ _≤_
  refl′ {zero}  refl = z≤n
  refl′ {suc m} refl = s≤s (refl′ refl)

  antisym : Antisymmetric _≡_ _≤_
  antisym z≤n       z≤n       = refl
  antisym (s≤s m≤n) (s≤s n≤m) with antisym m≤n n≤m
  ...                         | refl = refl

  trans : Transitive _≤_
  trans z≤n       _         = z≤n
  trans (s≤s m≤n) (s≤s n≤o) = s≤s (trans m≤n n≤o)

  total : Total _≤_
  total zero    _       = inj₁ z≤n
  total _       zero    = inj₂ z≤n
  total (suc m) (suc n) with total m n
  ...                   | inj₁ m≤n = inj₁ (s≤s m≤n)
  ...                   | inj₂ n≤m = inj₂ (s≤s n≤m)

import Relation.Binary.PartialOrderReasoning as POR
module ≤-Reasoning where
  open POR (DecTotalOrder.poset decTotalOrder) public
    renaming (_≈⟨_⟩_ to _≡⟨_⟩_)

  infixr 2 _<⟨_⟩_

  _<⟨_⟩_ : ∀ x {y z} → x < y → y IsRelatedTo z → suc x IsRelatedTo z
  x <⟨ x<y ⟩ y≤z = suc x ≤⟨ x<y ⟩ y≤z


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

open import lib.Base
open import lib.PathGroupoid
open import lib.PathOver
open import lib.cubical.Square

module lib.cubical.SquareOver where

SquareOver : ∀ {i j} {A : Type i} (B : A → Type j) {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  (q₀₋ : b₀₀ == b₀₁ [ B ↓ p₀₋ ]) (q₋₀ : b₀₀ == b₁₀ [ B ↓ p₋₀ ])
  (q₋₁ : b₀₁ == b₁₁ [ B ↓ p₋₁ ]) (q₁₋ : b₁₀ == b₁₁ [ B ↓ p₁₋ ])
  → Type j
SquareOver B ids = Square

apd-square : ∀ {i j} {A : Type i} {B : A → Type j} (f : Π A B)
  {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → SquareOver B sq (apd f p₀₋) (apd f p₋₀) (apd f p₋₁) (apd f p₁₋)
apd-square f ids = ids

↓-=-to-squareover : ∀ {i j} {A : Type i} {B : A → Type j}
  {f g : Π A B} {x y : A} {p : x == y}
  {u : f x == g x} {v : f y == g y}
  → u == v [ (λ z → f z == g z) ↓ p ]
  → SquareOver B vid-square u (apd f p) (apd g p) v
↓-=-to-squareover {p = idp} idp = hid-square

↓-=-from-squareover : ∀ {i j} {A : Type i} {B : A → Type j}
  {f g : Π A B} {x y : A} {p : x == y}
  {u : f x == g x} {v : f y == g y}
  → SquareOver B vid-square u (apd f p) (apd g p) v
  → u == v [ (λ z → f z == g z) ↓ p ]
↓-=-from-squareover {p = idp} sq = horiz-degen-path sq

squareover-cst-in : ∀ {i j} {A : Type i} {B : Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ b₀₁ b₁₀ b₁₁ : B}
  {q₀₋ : b₀₀ == b₀₁} {q₋₀ : b₀₀ == b₁₀} {q₋₁ : b₀₁ == b₁₁} {q₁₋ : b₁₀ == b₁₁}
  (sq' : Square q₀₋ q₋₀ q₋₁ q₁₋)
  → SquareOver (λ _ → B) sq
      (↓-cst-in q₀₋) (↓-cst-in q₋₀) (↓-cst-in q₋₁) (↓-cst-in q₁₋)
squareover-cst-in {sq = ids} sq' = sq'

↓↓-from-squareover : ∀ {i j k} {A : Type i} {B : A → Type j} {C : Type k}
  {x y : C → A} {u : (c : C) → B (x c)} {v : (c : C) → B (y c)}
  {p : (c : C) → x c == y c} {c₁ c₂ : C} {q : c₁ == c₂}
  {α : u c₁ == v c₁ [ B ↓ p c₁ ]} {β : u c₂ == v c₂ [ B ↓ p c₂ ]}
  → SquareOver B (natural-square p q)
               α (↓-ap-in _ _ (apd u q)) (↓-ap-in _ _ (apd v q)) β
  → α == β [ (λ c → u c == v c [ B ↓ p c ]) ↓ q ]
↓↓-from-squareover {q = idp} sq = lemma sq
  where
  lemma : ∀ {i j} {A : Type i} {B : A → Type j}
    {x y : A} {u : B x} {v : B y} {p : x == y}
    {α β : u == v [ B ↓ p ]}
    → SquareOver B hid-square α idp idp β
    → α == β
  lemma {p = idp} sq = horiz-degen-path sq

↓↓-to-squareover : ∀ {i j k} {A : Type i} {B : A → Type j} {C : Type k}
  {x y : C → A} {u : (c : C) → B (x c)} {v : (c : C) → B (y c)}
  {p : (c : C) → x c == y c} {c₁ c₂ : C} {q : c₁ == c₂}
  {α : u c₁ == v c₁ [ B ↓ p c₁ ]} {β : u c₂ == v c₂ [ B ↓ p c₂ ]}
  → α == β [ (λ c → u c == v c [ B ↓ p c ]) ↓ q ]
  → SquareOver B (natural-square p q)
               α (↓-ap-in _ _ (apd u q)) (↓-ap-in _ _ (apd v q)) β
↓↓-to-squareover {q = idp} r = lemma r
  where
  lemma : ∀ {i j} {A : Type i} {B : A → Type j}
    {x y : A} {u : B x} {v : B y} {p : x == y}
    {α β : u == v [ B ↓ p ]}
    → α == β
    → SquareOver B hid-square α idp idp β
  lemma {p = idp} r = horiz-degen-square r

infixr 80 _∙v↓⊡_ _∙h↓⊡_ _↓⊡v∙_ _↓⊡h∙_

_∙h↓⊡_ : ∀ {i j} {A : Type i} {B : A → Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  {q₀₋ q₀₋' : b₀₀ == b₀₁ [ B ↓ p₀₋ ]} {q₋₀ : b₀₀ == b₁₀ [ B ↓ p₋₀ ]}
  {q₋₁ : b₀₁ == b₁₁ [ B ↓ p₋₁ ]} {q₁₋ : b₁₀ == b₁₁ [ B ↓ p₁₋ ]}
  → q₀₋ == q₀₋'
  → SquareOver B sq q₀₋' q₋₀ q₋₁ q₁₋
  → SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋
_∙h↓⊡_ {sq = ids} = _∙h⊡_

_∙v↓⊡_ : ∀ {i j} {A : Type i} {B : A → Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  {q₀₋ : b₀₀ == b₀₁ [ B ↓ p₀₋ ]} {q₋₀ q₋₀' : b₀₀ == b₁₀ [ B ↓ p₋₀ ]}
  {q₋₁ : b₀₁ == b₁₁ [ B ↓ p₋₁ ]} {q₁₋ : b₁₀ == b₁₁ [ B ↓ p₁₋ ]}
  → q₋₀ == q₋₀'
  → SquareOver B sq q₀₋ q₋₀' q₋₁ q₁₋
  → SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋
_∙v↓⊡_ {sq = ids} = _∙v⊡_

_↓⊡v∙_ : ∀ {i j} {A : Type i} {B : A → Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  {q₀₋ : b₀₀ == b₀₁ [ B ↓ p₀₋ ]} {q₋₀ : b₀₀ == b₁₀ [ B ↓ p₋₀ ]}
  {q₋₁ q₋₁' : b₀₁ == b₁₁ [ B ↓ p₋₁ ]} {q₁₋ : b₁₀ == b₁₁ [ B ↓ p₁₋ ]}
  → SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋
  → q₋₁ == q₋₁'
  → SquareOver B sq q₀₋ q₋₀ q₋₁' q₁₋
_↓⊡v∙_ {sq = ids} = _⊡v∙_

_↓⊡h∙_ : ∀ {i j} {A : Type i} {B : A → Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  {q₀₋ : b₀₀ == b₀₁ [ B ↓ p₀₋ ]} {q₋₀ : b₀₀ == b₁₀ [ B ↓ p₋₀ ]}
  {q₋₁ : b₀₁ == b₁₁ [ B ↓ p₋₁ ]} {q₁₋ q₁₋' : b₁₀ == b₁₁ [ B ↓ p₁₋ ]}
  → SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋
  → q₁₋ == q₁₋'
  → SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋'
_↓⊡h∙_ {sq = ids} = _⊡h∙_


text:
module Star where

data Star {A : Set}(R : A -> A -> Set) : A -> A -> Set where
  rf   : {x : A} -> Star R x x
  _<>_ : forall {x y z} -> R x y -> Star R y z -> Star R x z


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

open import lib.Base
open import lib.Function
open import lib.PathFunctor
open import lib.PathGroupoid

open import lib.path-seq.Concat

module lib.path-seq.Split {i} {A : Type i} where

point-from-start : (n : ℕ) {a a' : A} (s : a =-= a') → A
point-from-start O {a} s = a
point-from-start (S n) {a = a} [] = a
point-from-start (S n) (p ◃∙ s) = point-from-start n s

drop : (n : ℕ) {a a' : A} (s : a =-= a') → point-from-start n s =-= a'
drop 0 s = s
drop (S n) [] = []
drop (S n) (p ◃∙ s) = drop n s

tail : {a a' : A} (s : a =-= a') → point-from-start 1 s =-= a'
tail = drop 1

private
  last1 : {a a' : A} (s : a =-= a') → A
  last1 {a = a} [] = a
  last1 {a = a} (p ◃∙ []) = a
  last1 (p ◃∙ s@(_ ◃∙ _)) = last1 s

  strip : {a a' : A} (s : a =-= a') → a =-= last1 s
  strip [] = []
  strip (p ◃∙ []) = []
  strip (p ◃∙ s@(_ ◃∙ _)) = p ◃∙ strip s

  point-from-end : (n : ℕ) {a a' : A} (s : a =-= a') → A
  point-from-end O {a} {a'} s = a'
  point-from-end (S n) s = point-from-end n (strip s)

!- : (n : ℕ) {a a' : A} (s : a =-= a') → a =-= point-from-end n s
!- O s = s
!- (S n) s = !- n (strip s)

take : (n : ℕ) {a a' : A} (s : a =-= a') → a =-= point-from-start n s
take O s = []
take (S n) [] = []
take (S n) (p ◃∙ s) = p ◃∙ take n s

private
  take-drop-split' : {a a' : A} (n : ℕ) (s : a =-= a')
    → s == take n s ∙∙ drop n s
  take-drop-split' O s = idp
  take-drop-split' (S n) [] = idp
  take-drop-split' (S n) (p ◃∙ s) = ap (λ v → p ◃∙ v) (take-drop-split' n s)

abstract
  take-drop-split : {a a' : A} (n : ℕ) (s : a =-= a')
    → ↯ s ◃∎ =ₛ ↯ (take n s) ◃∙ ↯ (drop n s) ◃∎
  take-drop-split n s = =ₛ-in $
    ↯ s
      =⟨ ap ↯ (take-drop-split' n s) ⟩
    ↯ (take n s ∙∙ drop n s)
      =⟨ ↯-∙∙ (take n s) (drop n s) ⟩
    ↯ (take n s) ∙ ↯ (drop n s) =∎

private
  split : {a a' : A} (s : a =-= a')
    → Σ A (λ a'' → Σ (a =-= a'') (λ _ → a'' == a'))
  split {a = a} [] = (a , ([] , idp))
  split {a = a} (p ◃∙ []) = (a , ([] , p))
  split (p ◃∙ s@(_ ◃∙ _)) =
    let (a'' , (t , q)) = split s
    in (a'' , (p ◃∙ t) , q)

  point-from-end' : (n : ℕ) {a a' : A} (s : a =-= a') → A
  point-from-end' n {a = a} [] = a
  point-from-end' O (p ◃∙ s) = point-from-end' O s
  point-from-end' (S n) (p ◃∙ s) = point-from-end' n (fst (snd (split (p ◃∙ s))))

#- : (n : ℕ) {a a' : A} (s : a =-= a') → point-from-end' n s =-= a'
#- n [] = []
#- O (p ◃∙ s) = #- O s
#- (S n) (p ◃∙ s) = let (a' , (t , q)) = split (p ◃∙ s) in #- n t ∙▹ q

infix 120 _!0 _!1 _!2 _!3 _!4 _!5
_!0 = !- 0
_!1 = !- 1
_!2 = !- 2
_!3 = !- 3
_!4 = !- 4
_!5 = !- 5

0! = drop 0
1! = drop 1
2! = drop 2
3! = drop 3
4! = drop 4
5! = drop 5

infix 120 _#0 _#1 _#2 _#3 _#4 _#5
_#0 = #- 0
_#1 = #- 1
_#2 = #- 2
_#3 = #- 3
_#4 = #- 4
_#5 = #- 5

0# = take 0
1# = take 1
2# = take 2
3# = take 3
4# = take 4
5# = take 5

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

module Note where

open import Data.Integer using (ℤ)
open import Data.Nat     using (ℕ; _*_)

open import Pitch        using (Pitch; transposePitch)

data Duration : Set where
  duration : ℕ → Duration

unduration : Duration → ℕ
unduration (duration d) = d

data Note : Set where
  tone : Duration → Pitch → Note
  rest : Duration         → Note

-- Note: If we inline duration here Agda can't figure out
-- that noteDuration (tone d _) = unduration d
noteDuration : Note → ℕ
noteDuration (tone d _) = unduration d
noteDuration (rest d)   = unduration d

transposeNote : ℤ → Note → Note
transposeNote k (tone d p) = tone d (transposePitch k p)
transposeNote k (rest d)   = rest d

-- duration in 16th notes
-- assume duration of a 16th note is 1
16th 8th qtr half whole : Duration
16th   = duration 1
8th    = duration 2
dqtr   = duration 3
qtr    = duration 4
half   = duration 8
dhalf  = duration 12
whole  = duration 16
dwhole = duration 24

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Group
open import Cubical.Data.Prod using (_,_)

open import Cubical.Data.Unit

import Cubical.Algebra.Monoid.Construct.Unit as ⊤Monoid
open ⊤Monoid public hiding (⊤-isMonoid; ⊤-Monoid)

inv : Op₁ ⊤
inv _ = tt

⊤-inverseˡ : LeftInverse tt inv _◯_
⊤-inverseˡ _ = refl

⊤-inverseʳ : RightInverse tt inv _◯_
⊤-inverseʳ _ = refl

⊤-inverse : Inverse tt inv _◯_
⊤-inverse = ⊤-inverseˡ , ⊤-inverseʳ

⊤-isGroup : IsGroup ⊤ _◯_ tt inv
⊤-isGroup = record
  { isMonoid = ⊤Monoid.⊤-isMonoid
  ; inverse  = ⊤-inverse
  }

⊤-Group : Group ℓ-zero
⊤-Group = record { isGroup = ⊤-isGroup }


text:
{-# OPTIONS --without-K  #-}
module algebra.semigroup.core where

open import level
open import equality.core
open import sum
open import hott.level

record IsSemigroup {i} (X : Set i) : Set i where
  field
    _*_ : X → X → X
    assoc : (x y z : X) → (x * y) * z ≡ x * (y * z)

    is-set : h 2 X

Semigroup : ∀ i → Set (lsuc i)
Semigroup i = Σ (Set i) IsSemigroup

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base