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

module dom-eq where
  -- main definition: two contexts are domain-equal when they produce (Some
  -- x) on the same indices. note that the context need not map indices to
  -- even the same type of contents; this is just a property about the
  -- domains. the proofs that follow establish that this property is
  -- respected in the appropriate ways by the context maniupulation
  -- operators we use in the other judgements.
  dom-eq : {A B : Set} → A ctx → B ctx → Set
  dom-eq {A} {B} C1 C2 = ((n : Nat) → Σ[ x ∈ A ]( C1 n == Some x) → (Σ[ y ∈ B ](C2 n == Some y)))×
                         ((n : Nat) → Σ[ y ∈ B ]( C2 n == Some y) → (Σ[ x ∈ A ](C1 n == Some x)))

  -- the empty context has the same domain as itself
  dom-∅ : {A B : Set} → dom-eq (λ _ → None {A}) (λ _ → None {B})
  dom-∅ {A} {B} = (λ n x → abort (somenotnone (! (π2 x)))) , (λ n x → abort (somenotnone (! (π2 x))))

  -- the singleton contexts formed with any contents but the same index has
  -- the same domain
  dom-single : {A B : Set} (x : Nat) {a : A} {b : B} → dom-eq (■ (x , a)) (■ (x , b))
  dom-single {A} {B} x {α} {β} = (λ n x₁ → β , (ap1 (λ qq → (■ (qq , β)) n) (! (lem-dom-eq x₁)) · x∈■ _ _)) ,
                             (λ n x₁ → α , (ap1 (λ qq → (■ (qq , α)) n) (! (lem-dom-eq x₁)) · x∈■ _ _))

  -- if two disjoint contexts each share a domain with two others, those
  -- are also disjoint.
  dom-eq-disj : {A B : Set} {Δ1 Δ2 : A ctx} {H1 H2 : B ctx} →
              H1 ## H2 →
              dom-eq Δ1 H1 →
              dom-eq Δ2 H2 →
              Δ1 ## Δ2
  dom-eq-disj {A} {B} {Δ1} {Δ2} {H1} {H2} (d1 , d2) (de1 , de2) (de3 , de4) = guts1 , guts2
    where
      guts1 : (n : Nat) → dom Δ1 n → n # Δ2
      guts1 n dom1 with ctxindirect H2 n
      guts1 n dom1 | Inl x = abort (somenotnone (! (π2 x) · d1 n (de1 n dom1)))
      guts1 n dom1 | Inr x with ctxindirect Δ2 n
      guts1 n dom1 | Inr x₁ | Inl x = abort (somenotnone (! (π2 (de3 n x)) · x₁))
      guts1 n dom1 | Inr x₁ | Inr x = x

      guts2 : (n : Nat) → dom Δ2 n → n # Δ1
      guts2 n dom2 with ctxindirect H1 n
      guts2 n dom2 | Inl x = abort (somenotnone (! (π2 x) · d2 n (de3 n dom2)))
      guts2 n dom2 | Inr x with ctxindirect Δ1 n
      guts2 n dom2 | Inr x₁ | Inl x = abort (somenotnone (! (π2 (de1 n x)) · x₁))
      guts2 n dom2 | Inr x₁ | Inr x = x

  -- if two sets share a domain with disjoint sets, then their union shares
  -- a domain with the union
  dom-union : {A B : Set} {Δ1 Δ2 : A ctx} {H1 H2 : B ctx} →
              H1 ## H2 →
              dom-eq Δ1 H1 →
              dom-eq Δ2 H2 →
              dom-eq (Δ1 ∪ Δ2) (H1 ∪ H2)
  dom-union {A} {B} {Δ1} {Δ2} {H1} {H2} disj (p1 , p2) (p3 , p4) = guts1 , guts2
    where
      guts1 : (n : Nat) →
                 Σ[ x ∈ A ] ((Δ1 ∪ Δ2) n == Some x) →
                 Σ[ y ∈ B ] ((H1 ∪ H2) n == Some y)
      guts1 n (x , eq) with ctxindirect Δ1 n
      guts1 n (x₁ , eq) | Inl x with p1 n x
      ... | q1 , q2 = q1 , x∈∪l H1 H2 n q1 q2
      guts1 n (x₁ , eq) | Inr x with p3 n (_ , lem-dom-union-apt1 {Δ1 = Δ1} {Δ2 = Δ2} x eq)
      ... | q1 , q2 =  q1 , x∈∪r H1 H2 n q1 q2 (π2 disj n (q1 , q2))

      guts2 : (n : Nat) →
                 Σ[ y ∈ B ] ((H1 ∪ H2) n == Some y) →
                 Σ[ x ∈ A ] ((Δ1 ∪ Δ2) n == Some x)
      guts2 n (x , eq) with ctxindirect H1 n
      guts2 n (x₁ , eq) | Inl x with p2 n x
      ... | q1 , q2 = q1 , x∈∪l Δ1 Δ2 n q1 q2
      guts2 n (x₁ , eq) | Inr x with p4 n (_ , lem-dom-union-apt2 {Δ1 = H2} {Δ2 = H1} x (tr (λ qq → qq n == Some x₁) (∪comm H1 H2 disj) eq))
      ... | q1 , q2 with ##-comm (dom-eq-disj disj (p1 , p2) (p3 , p4))
      ... | π3 , π4 = q1 , x∈∪r Δ1 Δ2 n q1 q2 (π3 n (q1 , q2))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

   Copyright (c) 2020 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 LibraBFT.Prelude

-- To enable reasoning about algorithms that concatenate
-- ByteStrings and pass the result to a cryptographic hash
-- function (as LibraBFT does), it is critical to have an
-- injective bitstring concat function ('bs-concat', below).
--
-- To see why, suppose we hash a data structure that contains two
-- fields of type ByteString by passing its fields to a hash
-- function like this:
--
-- > h : String -> String -> Hash
-- > h a b = hash (concat [a , b])
--
-- This function is /NOT/ collision resistant:
--
-- > h "xx" "x" == hash (concat ["xx" , "x"])
-- >            == hash "xxx"
-- >            == hash (concat ["x" , "xx"]) == h "x" "xx"
--
-- We cannot solve the problem simply by using an arbitrary field
-- separator, because an arbitrary ByteString might contain the
-- separator.  For example, if we define:
--
-- > h a b = hash (concat [ a , ";" , b ])
--
-- Then, we still have:
--
-- > h "x;x" "x" == h "x" "x;x"
--
-- Two possible approaches to defining an injective `concat`
-- function are:
--
-- 1) Use some length-prefixed encoding where we know the size of
-- each field. This approach will work in practice but we won't
-- be able to prove its injectivity for arbitrary ByteStrings in
-- Agda: Regardless of how many bytes we reserve for size
-- information, there are some inputs that require more.
--
-- 2) Encoding the arguments' list structure in the result of
-- concat; inverting the concat function then becomes parsing a
-- list of values. This approach is analogous to:
--
-- > concat : List ByteString -> BitString
-- > concat = serialize . toJSON
--
-- We take the second approach.
module LibraBFT.Base.ByteString where

  -- A BitString is a list of bits
  BitString : Set
  BitString = List Bool

  -- A ByteString is a list of bytes
  ByteString : Set
  ByteString = List (Vec Bool 8)

  _≟ByteString_ : (bs1 bs2 : ByteString) → Dec (bs1 ≡ bs2)
  _≟ByteString_ = List-≡-dec (Vec-≡-dec _≟Bool_)

  -- Concatenates ByteString prepending '11' to each byte.
  toBitString-pad' : ByteString → BitString
  toBitString-pad' = concat ∘ List-map (λ v → true ∷ true ∷ Vec-toList v)

  -- Concatenates a ByteString distinguishing an empty list from a non-empty list
  toBitString-pad : ByteString → BitString
  toBitString-pad []       = false ∷ false ∷ []
  toBitString-pad (b ∷ bs) = true  ∷ false ∷ Vec-toList b ++ toBitString-pad' bs

  -- Here's our injective concat function for ByteString
  bs-concat : List ByteString -> BitString
  bs-concat = concat ∘ List-map toBitString-pad

  -----------------------
  -- Injectivity Proof --
  -----------------------

  -- The proof is straightforward once we figure out the core reasoning principle:
  -- Any non-injective cases would be some variation on:
  --
  --         bs-concat ([a] ∷ c) ≡ bs-concat ([b₀ , b₁] ∷ d)
  --
  --    <==> toBitString-pad [a] ++ bs-concat c ≡ toBitString-pad [b₀ , b₁] ++ bs-concat d
  --
  --    <==> 1 1 a₀ ⋯ a₇ ++ bs-concat c ≡ 1 1 b₀₀ ⋯ b₀₇ 1 0 b₁₀ ⋯ b₁₇ ++ bs-concat d
  --
  --         { ++ is injective for same-length prefixes }
  --
  --    <==> aᵢ ≡ b₀ᵢ × bs-concat c ≡ 1 0 b₁₀ ⋯ b₁₇ ++ bs-concat d
  --
  --         { impossible,  bs-concat c is either empty or starts with 11 }
  --
  --    <==> ⊥
  --
  -- The actual Agda is a little more involved; but this covers the intuition.

  -- Appending two lists of the same length is injective.
  ++-len-injective : ∀{a}{A : Set a}(xs₀ ys₀ : List A){xs₁ ys₁ : List A}
               → length xs₀ ≡ length ys₀
               → xs₀ ++ xs₁ ≡ ys₀ ++ ys₁
               → xs₀ ≡ ys₀ × xs₁ ≡ ys₁
  ++-len-injective [] [] len hyp = refl , hyp
  ++-len-injective (x ∷ xs0) (y ∷ ys0) len hyp
    = let x≡y , tails≡ = ∷-injective hyp
          a , b = ++-len-injective xs0 ys0 (suc-injective len) tails≡
       in cong₂ _∷_ x≡y a , b

  Vec-toList-length : ∀{a n}{A : Set a}(x : Vec A n) → length (Vec-toList x) ≡ n
  Vec-toList-length []       = refl
  Vec-toList-length (_ ∷ xs) = cong suc (Vec-toList-length xs)

  Vec-toList-inj : ∀{a n}{A : Set a}{x y : Vec A n}
                 → Vec-toList x ≡ Vec-toList y → x ≡ y
  Vec-toList-inj {x = []}     {[]}     hyp = refl
  Vec-toList-inj {x = x ∷ xs} {y ∷ ys} hyp
    = let x≡y , xs≡ys = ∷-injective hyp
       in cong₂ _∷_ x≡y (Vec-toList-inj xs≡ys)

  -- In general, _++_ is not injective.  However, we can
  -- characterize it universally with a /Prefix/ property.
  data _≺_ {a}{A : Set a} : List A → List A → Set where
    z≺n : ∀{xs}      → [] ≺ xs
    s≺s : ∀{x xs ys} → xs ≺ ys → (x ∷ xs) ≺ (x ∷ ys)

  -- Returns the tail of ys; after dropping the prefix xs.
  ≺-drop : ∀{a}{A : Set a}{xs ys : List A} → xs ≺ ys → List A
  ≺-drop {ys = ys} z≺n = ys
  ≺-drop (s≺s a)       = ≺-drop a

  ++-≺ : ∀{a}{A : Set a}(xs ws : List A){ys zs : List A}
       → xs ++ ys ≡ ws ++ zs
       → Σ (xs ≺ ws) (λ prf → ≺-drop prf ++ zs ≡ ys)
       ⊎ Σ (ws ≺ xs) (λ prf → ≺-drop prf ++ ys ≡ zs)
  ++-≺ [] ys hyp = inj₁ (z≺n , sym hyp)
  ++-≺ (x ∷ xs) [] hyp = inj₂ (z≺n , hyp)
  ++-≺ (x ∷ xs) (y ∷ ys) hyp
    with ∷-injective hyp
  ...| refl , xs≡ys
    with ++-≺ xs ys xs≡ys
  ...| inj₁ (ok , prf) = inj₁ (s≺s ok , prf)
  ...| inj₂ (ok , prf) = inj₂ (s≺s ok , prf)

  ≺-respects-++-len
    : ∀{a}{A : Set a}(xs₀ ys₀ : List A){xs₁ ys₁ : List A}
    → (p : (xs₀ ++ xs₁) ≺ (ys₀ ++ ys₁))
    → length xs₀ ≡ length ys₀
    → xs₀ ≡ ys₀ × Σ (xs₁ ≺ ys₁) (λ p' → ≺-drop p ≡ ≺-drop p')
  ≺-respects-++-len [] [] prf hyp = refl , (prf , refl)
  ≺-respects-++-len (x ∷ xs) (.x ∷ ys) (s≺s prf) hyp
    with ≺-respects-++-len xs ys prf (suc-injective hyp)
  ...| xs≡ys , res , ok = cong (x ∷_) xs≡ys , res , ok

  bs-concat-[]⊎tf : ∀ as {bs} → true ∷ true ∷ bs ≢ bs-concat as
  bs-concat-[]⊎tf ([] ∷ as) ()
  bs-concat-[]⊎tf ((_ ∷ _) ∷ as) ()

  toBitString-pad'-≺
    : ∀{a b}
    → (a≺bbs : toBitString-pad' a ≺ toBitString-pad' b)
    → a ≡ b ⊎ ∃[ tail ] (≺-drop a≺bbs ≡ true ∷ true ∷ tail)
  toBitString-pad'-≺ {[]} {[]} prf     = inj₁ refl
  toBitString-pad'-≺ {[]} {x ∷ bs} z≺n = inj₂ (Vec-toList x ++ toBitString-pad' bs , refl)
  toBitString-pad'-≺ {a ∷ as} {b ∷ bs} (s≺s (s≺s prf))
    with ≺-respects-++-len (Vec-toList a) (Vec-toList b) prf
                           (trans (Vec-toList-length a) (sym (Vec-toList-length b)))
  ...| a≡b , prf' , drop≡
    with toBitString-pad'-≺ {as} {bs} prf'
  ...| inj₁ ok = inj₁ (cong₂ _∷_ (Vec-toList-inj a≡b) ok)
  ...| inj₂ ok = inj₂ (proj₁ ok , trans drop≡ (proj₂ ok))

  toBitString-pad-≺
    : ∀{a b}
    → (a≺bbs : toBitString-pad a ≺ toBitString-pad b)
    → a ≡ b ⊎ ∃[ tail ] (≺-drop a≺bbs ≡ true ∷ true ∷ tail)
  toBitString-pad-≺ {[]}    {[]} prf = inj₁ refl
  toBitString-pad-≺ {a ∷ as} {b ∷ bs} (s≺s (s≺s prf))
    with ≺-respects-++-len (Vec-toList a) (Vec-toList b) prf
                           (trans (Vec-toList-length a) (sym (Vec-toList-length b)))
  ...| a≡b , prf' , drop≡
    with toBitString-pad'-≺ {as} {bs} prf'
  ...| inj₁ ok = inj₁ (cong₂ _∷_ (Vec-toList-inj a≡b) ok)
  ...| inj₂ ok = inj₂ (proj₁ ok , trans drop≡ (proj₂ ok))

  bs-concat-inj : ∀ bs₁ bs₂ → bs-concat bs₁ ≡ bs-concat bs₂ → bs₁ ≡ bs₂
  bs-concat-inj [] [] hyp = refl
  bs-concat-inj ([] ∷ as) [] ()
  bs-concat-inj [] ([] ∷ bs) ()
  bs-concat-inj [] ((_ ∷ _) ∷ bs) ()
  bs-concat-inj ((_ ∷ _) ∷ as) [] ()
  bs-concat-inj (a ∷ as) (b ∷ bs) hyp -- TODO-1: Eliminate catchall warning or explain why we don't.
    with ++-≺ (toBitString-pad a) (toBitString-pad b) hyp
  ...| inj₁ (a≺b , prf)
    with toBitString-pad-≺ a≺b
  ...| inj₁ refl = cong (a ∷_) (bs-concat-inj as bs (proj₂ (++-len-injective (toBitString-pad a) _ refl hyp)))
  ...| inj₂ (tail , aux) rewrite aux = ⊥-elim (bs-concat-[]⊎tf as prf)
  bs-concat-inj (a ∷ as) (b ∷ bs) hyp
     | inj₂ (b≺a , prf)
    with toBitString-pad-≺ b≺a
  ...| inj₁ refl = cong (a ∷_) (bs-concat-inj as bs (proj₂ (++-len-injective (toBitString-pad a) _ refl hyp)))
  ...| inj₂ (tail , aux) rewrite aux  = ⊥-elim (bs-concat-[]⊎tf bs prf)

ext: agda

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:
------------------------------------------------------------------------
-- Information orderings
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --sized-types #-}

open import Prelude hiding (module W)

module Delay-monad.Alternative.Partial-order {a} {A : Type a} where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths

open import Delay-monad.Alternative
open import Delay-monad.Alternative.Equivalence
open import Delay-monad.Alternative.Termination
import Delay-monad.Partial-order as PO
import Delay-monad.Termination as T

infix 4 _⊑_

-- Information orderings.

_⊑_ : Delay A → Delay A → Type a
x ⊑ y = ∀ z → x ⇓ z → y ⇓ z

_∥⊑∥_ : Delay A → Delay A → Type a
x ∥⊑∥ y = ∀ z → x ∥⇓∥ z → y ∥⇓∥ z

-- The two ordering relations are logically equivalent (if A is a
-- set).

⊑⇔∥⊑∥ : Is-set A → ∀ x y → x ⊑ y ⇔ x ∥⊑∥ y
⊑⇔∥⊑∥ A-set x y =
  ∀-cong _ λ _ → →-cong _ (⇓⇔∥⇓∥ A-set x) (⇓⇔∥⇓∥ A-set y)

-- The ordering relation _⊑_ is pointwise logically equivalent (via
-- Delay⇔Delay) to the ordering relation defined in
-- Delay-monad.Partial-order.

⊑⇔⊑ : ∀ x y →
      x ⊑ y ⇔ _⇔_.to Delay⇔Delay x PO.⊑ _⇔_.to Delay⇔Delay y
⊑⇔⊑ x y =
  x ⊑ y                                                              ↝⟨ F.id ⟩
  (∀ z → x ⇓ z → y ⇓ z)                                              ↝⟨ ∀-cong _ (λ _ → →-cong _ (⇓⇔⇓ x) (⇓⇔⇓ y)) ⟩
  (∀ z → _⇔_.to Delay⇔Delay x  T.⇓ z → _⇔_.to Delay⇔Delay y  T.⇓ z)  ↝⟨ inverse $ ∀-cong _ (λ _ → →-cong _ (_↔_.logical-equivalence PO.⇓↔⇓)
                                                                                (_↔_.logical-equivalence PO.⇓↔⇓)) ⟩
  (∀ z → _⇔_.to Delay⇔Delay x PO.⇓ z → _⇔_.to Delay⇔Delay y PO.⇓ z)  ↝⟨ inverse PO.⊑⇔⇓→⇓ ⟩□
  _⇔_.to Delay⇔Delay x PO.⊑ _⇔_.to Delay⇔Delay y                     □

⊑⇔⊑′ : ∀ {x y} →
       x PO.⊑ y ⇔ _⇔_.from Delay⇔Delay x ⊑ _⇔_.from Delay⇔Delay y
⊑⇔⊑′ {x} {y} =
  x PO.⊑ y                                                         ↝⟨ PO.⊑⇔⇓→⇓ ⟩
  (∀ z → x PO.⇓ z → y PO.⇓ z)                                      ↝⟨ ∀-cong _ (λ _ → →-cong _ (_↔_.logical-equivalence PO.⇓↔⇓)
                                                                                (_↔_.logical-equivalence PO.⇓↔⇓))  ⟩
  (∀ z → x  T.⇓ z → y  T.⇓ z)                                      ↝⟨ ∀-cong _ (λ _ → →-cong _ ⇓⇔⇓′ ⇓⇔⇓′) ⟩
  (∀ z → _⇔_.from Delay⇔Delay x ⇓ z → _⇔_.from Delay⇔Delay y ⇓ z)  ↝⟨ F.id ⟩□
  _⇔_.from Delay⇔Delay x ⊑ _⇔_.from Delay⇔Delay y                  □

-- The ordering relation _∥⊑∥_ is pointwise propositional.

∥⊑∥-propositional : ∀ x y → Is-proposition (x ∥⊑∥ y)
∥⊑∥-propositional _ _ =
  Π-closure ext 1 λ _ →
  Π-closure ext 1 λ _ →
  truncation-is-proposition

-- The ordering relation _∥⊑∥_ is reflexive.

∥⊑∥-reflexive : ∀ x → x ∥⊑∥ x
∥⊑∥-reflexive _ = λ _ → id

-- The ordering relation _∥⊑∥_ is transitive.

∥⊑∥-transitive : ∀ x y z → x ∥⊑∥ y → y ∥⊑∥ z → x ∥⊑∥ z
∥⊑∥-transitive _ _ _ p q = λ z → q z ∘ p z

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


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

open import Categories.Category

module Categories.Object.Initial {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level

record Initial : Set (o ⊔ ℓ ⊔ e) where
  field
    ⊥ : Obj
    ! : ∀ {A} → (⊥ ⇒ A)
    .!-unique : ∀ {A} → (f : ⊥ ⇒ A) → ! ≡ f

  .!-unique₂ : ∀ {A} → (f g : ⊥ ⇒ A) → f ≡ g
  !-unique₂ f g =
      begin
        f
      ↑⟨ !-unique f ⟩
        !
      ↓⟨ !-unique g ⟩
        g
      ∎
    where
    open HomReasoning

  .⊥-id : (f : ⊥ ⇒ ⊥) → f ≡ id
  ⊥-id f = !-unique₂ f id

import Categories.Morphisms
open Categories.Morphisms C
open Initial

.to-⊥-is-Epi : ∀ {A : Obj} {i : Initial} → (f : A ⇒ ⊥ i) → Epi f
to-⊥-is-Epi {_} {i} f = helper
  where
    helper : ∀ {C : Obj} → (g h : ⊥ i ⇒ C) → g ∘ f ≡ h ∘ f → g ≡ h
    helper g h _ = !-unique₂ i g h

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


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

module Calf.Types.Nat where

open import Calf.Prelude
open import Calf.Metalanguage
open import Data.Nat using (ℕ; zero; suc) public

nat : tp pos
nat = U (meta ℕ)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

open import Cubical.Core.Everything

open import Cubical.Algebra.Base
open import Cubical.Algebra.Structures
open import Cubical.Relation.Binary
open import Cubical.Foundations.Function

open import Cubical.Classes

------------------------------------------------------------------------
-- Bundles with 1 binary operation
------------------------------------------------------------------------

record Magma c : Type (ℓ-suc c) where
  constructor mkmagma
  infix 7 _•_ -- No association - forces parentheses
  field
    Carrier : Type c
    _•_     : Op₂ Carrier
    isMagma : IsMagma Carrier _•_

  open IsMagma isMagma public

instance
  MagmaCoerce : ∀ {c} → Coerce (Magma c)
  MagmaCoerce = record { coerce = Magma.Carrier }

record Semigroup c : Type (ℓ-suc c) where
  constructor mksemigroup
  infixl 7 _•_
  field
    Carrier     : Type c
    _•_         : Op₂ Carrier
    isSemigroup : IsSemigroup Carrier _•_

  open IsSemigroup isSemigroup public

  magma : Magma c
  magma = record { isMagma = isMagma }

instance
  SemigroupCoerce : ∀ {c} → Coerce (Semigroup c)
  SemigroupCoerce = record { coerce = Semigroup.Carrier }

  Semigroup→Magma : ∀ {c} → Cast (Semigroup c) (Magma c)
  Semigroup→Magma = record { cast = Semigroup.magma }

record Band c : Type (ℓ-suc c) where
  constructor mkband
  infixl 7 _•_
  field
    Carrier : Type c
    _•_     : Op₂ Carrier
    isBand  : IsBand Carrier _•_

  open IsBand isBand public

  semigroup : Semigroup c
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup public using (magma)

instance
  BandCoerce : ∀ {c} → Coerce (Band c)
  BandCoerce = record { coerce = Band.Carrier }

  Cast-Band→Semigroup : ∀ {c} → Cast (Band c) (Semigroup c)
  Cast-Band→Semigroup = record { cast = Band.semigroup }

  Cast-Band→Magma : ∀ {c} → Cast (Band c) (Magma c)
  Cast-Band→Magma = record { cast = Band.magma }

record CommutativeSemigroup c : Type (ℓ-suc c) where
  constructor mkcommsemigroup
  infixl 7 _•_
  field
    Carrier                 : Type c
    _•_                     : Op₂ Carrier
    isCommutativeSemigroup  : IsCommutativeSemigroup Carrier _•_

  open IsCommutativeSemigroup isCommutativeSemigroup public

  semigroup : Semigroup c
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup public using (magma)

instance
  CommSemigroupCoerce : ∀ {c} → Coerce (CommutativeSemigroup c)
  CommSemigroupCoerce = record { coerce = CommutativeSemigroup.Carrier }

  Cast-CommSemigroup→Semigroup : ∀ {c} → Cast (CommutativeSemigroup c) (Semigroup c)
  Cast-CommSemigroup→Semigroup = record { cast = CommutativeSemigroup.semigroup }

  Cast-CommSemigroup→Magma : ∀ {c} → Cast (CommutativeSemigroup c) (Magma c)
  Cast-CommSemigroup→Magma = record { cast = CommutativeSemigroup.magma }

record Semilattice c : Type (ℓ-suc c) where
  constructor mksemilattice
  infixr 7 _•_
  field
    Carrier       : Type c
    _•_           : Op₂ Carrier
    isSemilattice : IsSemilattice Carrier _•_

  open IsSemilattice isSemilattice public

  band : Band c
  band = record { isBand = isBand }

  open Band band public using (magma; semigroup)

instance
  SemilatticeCoerce : ∀ {c} → Coerce (Semilattice c)
  SemilatticeCoerce = record { coerce = Semilattice.Carrier }

record SelectiveMagma c : Type (ℓ-suc c) where
  constructor mkselmagma
  infixl 7 _•_
  field
    Carrier          : Type c
    _•_              : Op₂ Carrier
    isSelectiveMagma : IsSelectiveMagma Carrier _•_

  open IsSelectiveMagma isSelectiveMagma public

  magma : Magma c
  magma = record { isMagma = isMagma }

instance
  SelectiveMagmaCoerce : ∀ {c} → Coerce (SelectiveMagma c)
  SelectiveMagmaCoerce = record { coerce = SelectiveMagma.Carrier }

------------------------------------------------------------------------
-- Bundles with 1 binary operation & 1 element
------------------------------------------------------------------------

record Monoid c : Type (ℓ-suc c) where
  constructor mkmonoid
  infixl 7 _•_
  field
    Carrier  : Type c
    _•_      : Op₂ Carrier
    ε        : Carrier
    isMonoid : IsMonoid Carrier _•_ ε

  open IsMonoid isMonoid public

  semigroup : Semigroup _
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup public using (magma)

instance
  MonoidCoerce : ∀ {c} → Coerce (Monoid c)
  MonoidCoerce = record { coerce = Monoid.Carrier }

record CommutativeMonoid c : Type (ℓ-suc c) where
  constructor mkcommmonoid
  infixl 7 _•_
  field
    Carrier             : Type c
    _•_                 : Op₂ Carrier
    ε                   : Carrier
    isCommutativeMonoid : IsCommutativeMonoid Carrier _•_ ε

  open IsCommutativeMonoid isCommutativeMonoid public

  monoid : Monoid _
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid public using (magma; semigroup)

  commutativeSemigroup : CommutativeSemigroup _
  commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }

instance
  CommMonoidCoerce : ∀ {c} → Coerce (CommutativeMonoid c)
  CommMonoidCoerce = record { coerce = CommutativeMonoid.Carrier }

record IdempotentCommutativeMonoid c : Type (ℓ-suc c) where
  constructor mkidemcommmonoid
  infixl 7 _•_
  field
    Carrier                       : Type c
    _•_                           : Op₂ Carrier
    ε                             : Carrier
    isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid Carrier _•_ ε

  open IsIdempotentCommutativeMonoid isIdempotentCommutativeMonoid public

  commutativeMonoid : CommutativeMonoid _
  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }

  open CommutativeMonoid commutativeMonoid public
    using (magma; semigroup; monoid)

instance
  IdemCommMonoidCoerce : ∀ {c} → Coerce (IdempotentCommutativeMonoid c)
  IdemCommMonoidCoerce = record { coerce = IdempotentCommutativeMonoid.Carrier }

-- Idempotent commutative monoids are also known as bounded lattices.
-- Note that the BoundedLattice necessarily uses the notation inherited
-- from monoids rather than lattices.

BoundedLattice = IdempotentCommutativeMonoid
pattern mkboundedlattice = mkidemcommmonoid

module BoundedLattice {c} (idemCommMonoid : IdempotentCommutativeMonoid c) =
       IdempotentCommutativeMonoid idemCommMonoid

------------------------------------------------------------------------
-- Bundles with 1 binary operation, 1 unary operation & 1 element
------------------------------------------------------------------------

record Group c : Type (ℓ-suc c) where
  constructor mkgroup
  infix  8 _⁻¹
  infixl 7 _•_
  field
    Carrier : Type c
    _•_     : Op₂ Carrier
    ε       : Carrier
    _⁻¹     : Op₁ Carrier
    isGroup : IsGroup Carrier _•_ ε _⁻¹

  open IsGroup isGroup public

  monoid : Monoid _
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid public using (magma; semigroup)

instance
  GroupCoerce : ∀ {c} → Coerce (Group c)
  GroupCoerce = record { coerce = Group.Carrier }

record AbelianGroup c : Type (ℓ-suc c) where
  constructor mkabgroup
  infix  8 -_
  infixl 7 _+_
  field
    Carrier        : Type c
    _+_            : Op₂ Carrier
    ε              : Carrier
    -_             : Op₁ Carrier
    isAbelianGroup : IsAbelianGroup Carrier _+_ ε -_

  open IsAbelianGroup isAbelianGroup public

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

  open Group group public
    using (magma; semigroup; monoid)

  commutativeMonoid : CommutativeMonoid _
  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }

  open CommutativeMonoid commutativeMonoid public
    using (commutativeSemigroup)

instance
  AbelianGroupCoerce : ∀ {c} → Coerce (AbelianGroup c)
  AbelianGroupCoerce = record { coerce = AbelianGroup.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations
------------------------------------------------------------------------

record Lattice c : Type (ℓ-suc c) where
  constructor mklattice
  infixr 7 _⋀_
  infixr 6 _⋁_
  field
    Carrier   : Type c
    _⋀_       : Op₂ Carrier
    _⋁_       : Op₂ Carrier
    isLattice : IsLattice Carrier _⋀_ _⋁_

  open IsLattice isLattice public

instance
  LatticeCoerce : ∀ {c} → Coerce (Lattice c)
  LatticeCoerce = record { coerce = Lattice.Carrier }

record DistributiveLattice c : Type (ℓ-suc c) where
  constructor mkdistrlattice
  infixr 7 _⋀_
  infixr 6 _⋁_
  field
    Carrier               : Type c
    _⋀_                   : Op₂ Carrier
    _⋁_                   : Op₂ Carrier
    isDistributiveLattice : IsDistributiveLattice Carrier _⋀_ _⋁_

  open IsDistributiveLattice isDistributiveLattice public

  lattice : Lattice _
  lattice = record { isLattice = isLattice }

instance
  DistrLatticeCoerce : ∀ {c} → Coerce (DistributiveLattice c)
  DistrLatticeCoerce = record { coerce = DistributiveLattice.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations & 1 element
------------------------------------------------------------------------

record NearSemiring c : Type (ℓ-suc c) where
  constructor mknearsemiring
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier        : Type c
    _+_            : Op₂ Carrier
    _*_            : Op₂ Carrier
    0#             : Carrier
    isNearSemiring : IsNearSemiring Carrier _+_ _*_ 0#

  open IsNearSemiring isNearSemiring public

  +-monoid : Monoid _
  +-monoid = record { isMonoid = +-isMonoid }

  open Monoid +-monoid public
    using () renaming
    ( magma     to +-magma
    ; semigroup to +-semigroup
    )

  *-semigroup : Semigroup _
  *-semigroup = record { isSemigroup = *-isSemigroup }

  open Semigroup *-semigroup public
    using () renaming
    ( magma to *-magma )

instance
  NearSemiringCoerce : ∀ {c} → Coerce (NearSemiring c)
  NearSemiringCoerce = record { coerce = NearSemiring.Carrier }

record SemiringWithoutOne c : Type (ℓ-suc c) where
  constructor mksemiringwo1
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier              : Type c
    _+_                  : Op₂ Carrier
    _*_                  : Op₂ Carrier
    0#                   : Carrier
    isSemiringWithoutOne : IsSemiringWithoutOne Carrier _+_ _*_ 0#

  open IsSemiringWithoutOne isSemiringWithoutOne public

  nearSemiring : NearSemiring _
  nearSemiring = record { isNearSemiring = isNearSemiring }

  open NearSemiring nearSemiring public
    using
    ( +-magma; +-semigroup; +-monoid
    ; *-magma; *-semigroup
    )

  +-commutativeMonoid : CommutativeMonoid _
  +-commutativeMonoid = record { isCommutativeMonoid = +-isCommutativeMonoid }

  open CommutativeMonoid +-commutativeMonoid public
    using () renaming (commutativeSemigroup to +-commutativeSemigroup)

instance
  SemiringW1Coerce : ∀ {c} → Coerce (SemiringWithoutOne c)
  SemiringW1Coerce = record { coerce = SemiringWithoutOne.Carrier }

record CommutativeSemiringWithoutOne c : Type (ℓ-suc c) where
  constructor mkcommsemiringwo1
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier                         : Type c
    _+_                             : Op₂ Carrier
    _*_                             : Op₂ Carrier
    0#                              : Carrier
    isCommutativeSemiringWithoutOne :
      IsCommutativeSemiringWithoutOne Carrier _+_ _*_ 0#

  open IsCommutativeSemiringWithoutOne
         isCommutativeSemiringWithoutOne public

  semiringWithoutOne : SemiringWithoutOne _
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

  open SemiringWithoutOne semiringWithoutOne public
    using
    ( +-magma; +-semigroup; +-commutativeSemigroup
    ; *-magma; *-semigroup
    ; +-monoid; +-commutativeMonoid
    ; nearSemiring
    )

instance
  CommSemiringW1Coerce : ∀ {c} → Coerce (CommutativeSemiringWithoutOne c)
  CommSemiringW1Coerce = record { coerce = CommutativeSemiringWithoutOne.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations & 2 elements
------------------------------------------------------------------------

record SemiringWithoutAnnihilatingZero c : Type (ℓ-suc c) where
  constructor mksemiringwoa0
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier                           : Type c
    _+_                               : Op₂ Carrier
    _*_                               : Op₂ Carrier
    0#                                : Carrier
    1#                                : Carrier
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero Carrier _+_ _*_ 0# 1#

  open IsSemiringWithoutAnnihilatingZero
         isSemiringWithoutAnnihilatingZero public

  +-commutativeMonoid : CommutativeMonoid _
  +-commutativeMonoid =
    record { isCommutativeMonoid = +-isCommutativeMonoid }

  open CommutativeMonoid +-commutativeMonoid public
    using () renaming
    ( magma                to +-magma
    ; semigroup            to +-semigroup
    ; commutativeSemigroup to +-commutativeSemigroup
    ; monoid               to +-monoid
    )

  *-monoid : Monoid _
  *-monoid = record { isMonoid = *-isMonoid }

  open Monoid *-monoid public
    using ()
    renaming
    ( magma     to *-magma
    ; semigroup to *-semigroup
    )

instance
  SemiringWA0Coerce : ∀ {c} → Coerce (SemiringWithoutAnnihilatingZero c)
  SemiringWA0Coerce = record { coerce = SemiringWithoutAnnihilatingZero.Carrier }

record Semiring c : Type (ℓ-suc c) where
  constructor mksemiring
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier    : Type c
    _+_        : Op₂ Carrier
    _*_        : Op₂ Carrier
    0#         : Carrier
    1#         : Carrier
    isSemiring : IsSemiring Carrier _+_ _*_ 0# 1#

  open IsSemiring isSemiring public

  semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _
  semiringWithoutAnnihilatingZero = record
    { isSemiringWithoutAnnihilatingZero =
        isSemiringWithoutAnnihilatingZero
    }

  open SemiringWithoutAnnihilatingZero
         semiringWithoutAnnihilatingZero public
    using
    ( +-magma;  +-semigroup; +-commutativeSemigroup
    ; *-magma;  *-semigroup
    ; +-monoid; +-commutativeMonoid
    ; *-monoid
    )

  semiringWithoutOne : SemiringWithoutOne _
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

  open SemiringWithoutOne semiringWithoutOne public
    using (nearSemiring)

instance
  SemiringCoerce : ∀ {c} → Coerce (Semiring c)
  SemiringCoerce = record { coerce = Semiring.Carrier }

record CommutativeSemiring c : Type (ℓ-suc c) where
  constructor mkcommsemiring
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier               : Type c
    _+_                   : Op₂ Carrier
    _*_                   : Op₂ Carrier
    0#                    : Carrier
    1#                    : Carrier
    isCommutativeSemiring : IsCommutativeSemiring Carrier _+_ _*_ 0# 1#

  open IsCommutativeSemiring isCommutativeSemiring public

  semiring : Semiring _
  semiring = record { isSemiring = isSemiring }

  open Semiring semiring public
    using
    ( +-magma; +-semigroup; +-commutativeSemigroup
    ; *-magma; *-semigroup
    ; +-monoid; +-commutativeMonoid
    ; *-monoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero
    )

  *-commutativeSemigroup : CommutativeSemigroup _
  *-commutativeSemigroup = record
    { isCommutativeSemigroup = *-isCommutativeSemigroup
    }

  *-commutativeMonoid : CommutativeMonoid _
  *-commutativeMonoid = record
    { isCommutativeMonoid = *-isCommutativeMonoid
    }

  commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _
  commutativeSemiringWithoutOne = record
    { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
    }

instance
  CommSemiringCoerce : ∀ {c} → Coerce (CommutativeSemiring c)
  CommSemiringCoerce = record { coerce = CommutativeSemiring.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations, 1 unary operation & 2 elements
------------------------------------------------------------------------

record Ring c : Type (ℓ-suc c) where
  constructor mkring
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier : Type c
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    isRing  : IsRing Carrier _+_ _*_ -_ 0# 1#

  open IsRing isRing public

  +-abelianGroup : AbelianGroup _
  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }

  semiring : Semiring _
  semiring = record { isSemiring = isSemiring }

  open Semiring semiring public
    using
    ( +-magma; +-semigroup; +-commutativeSemigroup
    ; *-magma; *-semigroup
    ; +-monoid ; +-commutativeMonoid
    ; *-monoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero
    )

  open AbelianGroup +-abelianGroup public
    using () renaming (group to +-group)

instance
  RingCoerce : ∀ {c} → Coerce (Ring c)
  RingCoerce = record { coerce = Ring.Carrier }

record CommutativeRing c : Type (ℓ-suc c) where
  constructor mkcommring
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier           : Type c
    _+_               : Op₂ Carrier
    _*_               : Op₂ Carrier
    -_                : Op₁ Carrier
    0#                : Carrier
    1#                : Carrier
    isCommutativeRing : IsCommutativeRing Carrier _+_ _*_ -_ 0# 1#

  open IsCommutativeRing isCommutativeRing public

  ring : Ring _
  ring = record { isRing = isRing }

  commutativeSemiring : CommutativeSemiring _
  commutativeSemiring =
    record { isCommutativeSemiring = isCommutativeSemiring }

  open Ring ring public using (+-group; +-abelianGroup)
  open CommutativeSemiring commutativeSemiring public
    using
    ( +-magma; +-semigroup; +-commutativeSemigroup
    ; *-magma; *-semigroup; *-commutativeSemigroup
    ; +-monoid; +-commutativeMonoid
    ; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne
    )

instance
  CommRingCoerce : ∀ {c} → Coerce (CommutativeRing c)
  CommRingCoerce = record { coerce = CommutativeRing.Carrier }

record BooleanAlgebra c : Type (ℓ-suc c) where
  constructor mkbooleanalgebra
  infix  8 ¬_
  infixr 7 _⋀_
  infixr 6 _⋁_
  field
    Carrier          : Type c
    _⋀_              : Op₂ Carrier
    _⋁_              : Op₂ Carrier
    ¬_               : Op₁ Carrier
    ⊤                : Carrier
    ⊥                : Carrier
    isBooleanAlgebra : IsBooleanAlgebra Carrier _⋀_ _⋁_ ¬_ ⊤ ⊥

  open IsBooleanAlgebra isBooleanAlgebra public

  distributiveLattice : DistributiveLattice _
  distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }

  open DistributiveLattice distributiveLattice public
    using (lattice)

instance
  BooleanCoerce : ∀ {c} → Coerce (BooleanAlgebra c)
  BooleanCoerce = record { coerce = BooleanAlgebra.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations, 1 unary operation & 2 elements
------------------------------------------------------------------------

record DivisionRing c ℓ : Type (ℓ-suc (ℓ-max c ℓ)) where
  constructor mkdivring
  infix  9 _⁻¹
  infix  8 -_
  infixr 7 _*_
  infixr 6 _+_
  field
    Carrier        : Type c
    Invertible     : Carrier → Type ℓ
    _+_            : Op₂ Carrier
    _*_            : Op₂ Carrier
    0#             : Carrier
    1#             : Carrier
    -_             : Op₁ Carrier
    _⁻¹            : Σ Carrier Invertible → Carrier
    isDivisionRing : IsDivisionRing Carrier Invertible _+_ _*_ -_ _⁻¹ 0# 1#

  open IsDivisionRing isDivisionRing public

  ring : Ring _
  ring = record { isRing = isRing }

  open Ring ring public using (+-group; +-abelianGroup)

instance
  DivisionRingCoerce : ∀ {c ℓ} → Coerce (DivisionRing c ℓ)
  DivisionRingCoerce = record { coerce = DivisionRing.Carrier }

record Field c ℓ : Type (ℓ-suc (ℓ-max c ℓ)) where
  constructor mkfield
  infix  9 _⁻¹
  infix  8 -_
  infixr 7 _*_
  infixr 6 _+_
  field
    Carrier    : Type c
    Invertible : Carrier → Type ℓ
    _+_        : Op₂ Carrier
    _*_        : Op₂ Carrier
    0#         : Carrier
    1#         : Carrier
    -_         : Op₁ Carrier
    _⁻¹        : Σ Carrier Invertible → Carrier
    isField    : IsField Carrier Invertible _+_ _*_ -_ _⁻¹ 0# 1#

  open IsField isField public

  divisionRing : DivisionRing _ _
  divisionRing = record { isDivisionRing = isDivisionRing }

  open DivisionRing divisionRing public using (ring; +-group; +-abelianGroup)

  commutativeRing : CommutativeRing _
  commutativeRing = record { isCommutativeRing = isCommutativeRing }

  open CommutativeRing commutativeRing public
      using
      ( commutativeSemiring
      ; +-magma; +-semigroup; +-commutativeSemigroup
      ; *-magma; *-semigroup; *-commutativeSemigroup
      ; +-monoid; +-commutativeMonoid
      ; *-monoid; *-commutativeMonoid
      ; nearSemiring; semiringWithoutOne
      ; semiringWithoutAnnihilatingZero; semiring
      ; commutativeSemiringWithoutOne
      )

instance
  FieldCoerce : ∀ {c ℓ} → Coerce (Field c ℓ)
  FieldCoerce = record { coerce = Field.Carrier }


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

module Relation.Binary.Indexed where

import Relation.Binary as B

open import Relation.Binary.Indexed.Core public

-- By "instantiating" an indexed setoid one gets an ordinary setoid.

_at_ : ∀ {i s₁ s₂} {I : Set i} → Setoid I s₁ s₂ → I → B.Setoid _ _
S at i = record
  { Carrier       = S.Carrier i
  ; _≈_           = S._≈_
  ; isEquivalence = record
    { refl  = S.refl
    ; sym   = S.sym
    ; trans = S.trans
    }
  } where module S = Setoid S

------------------------------------------------------------------------
-- Simple properties of indexed binary relations

-- Generalised implication.

infixr 4 _=[_]⇒_

_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} →
          B.Rel A ℓ₁ → ((x : A) → B x) → Rel B ℓ₂ → Set _
P =[ f ]⇒ Q = ∀ {i j} → P i j → Q (f i) (f j)


text:
module plfa.Naturals where

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

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

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

infixl 6 _+_

-- @practice: exercise `seven` start
_ : 7 ≡ suc (suc (suc (suc (suc (suc (suc zero))))))
_ = refl
-- @practice: exercise `seven` end

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩
    5
  ∎

-- @practice: exercise `+-example` start

_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc ( suc ( 1 + 4 ))
  ≡⟨⟩
    suc ( suc ( suc ( 0 + 4 )))
  ≡⟨⟩
    suc ( suc ( suc 4 ))
  ≡⟨⟩
    7
  ∎

-- @practice: exercise `+-example` end

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

infixl 7 _*_

_ =
  begin
    2 * 3
  ≡⟨⟩
    3 + ( 1 * 3 )
  ≡⟨⟩
    3 + ( 3 + ( 0 * 3 ))
  ≡⟨⟩
    3 + (3 + 0)
  ≡⟨⟩
    6
  ∎

-- @practice: exercise `*-example` start
_ =
  begin
    3 * 4
  ≡⟨⟩
    4 + ( 2 * 4)
  ≡⟨⟩
    4 + ( 4 + (1 * 4))
  ≡⟨⟩
    4 + ( 4 + (4 + (0 * 4)))
  ≡⟨⟩
    4 + (4 + (4 + 0))
  ≡⟨⟩
    12
  ∎
-- @practice: exercise `*-example` end

-- @recommend: exercise `_^_` start
_^_ : ℕ → ℕ → ℕ
m ^ zero = 1
m ^ (suc n) = m * (m ^ n)

infixl 8 _^_

_ : 3 ^ 4 ≡ 81
_ = refl
-- @recommend: exercise `_^_` end

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

infixl 6 _∸_

_ =
  begin
    3 ∸ 2
  ≡⟨⟩
    2 ∸ 1
  ≡⟨⟩
    1 ∸ 0
  ≡⟨⟩
    1
  ∎

_ =
  begin
    2 ∸ 3
  ≡⟨⟩
    1 ∸ 2
  ≡⟨⟩
    0 ∸ 1
  ≡⟨⟩
    0
  ∎

-- @recommend: exercise `∸-examples` start
_ =
  begin
    5 ∸ 3
  ≡⟨⟩
    4 ∸ 2
  ≡⟨⟩
    3 ∸ 1
  ≡⟨⟩
    2 ∸ 0
  ≡⟨⟩
    2
  ∎

_ =
  begin
    2 ∸ 5
  ≡⟨⟩
    1 ∸ 4
  ≡⟨⟩
    0 ∸ 3
  ≡⟨⟩
    0
  ∎
-- @recommend: exercise `∸-examples` end

-- infixl 6 _+_ _∸_
-- infixl 7 _⋆_
-- infixl indicates an operator associates to the left
-- infixr indicates an operator associates to the right
-- infix indicates that parentheses are always required

-- C-c + C-l convert `?` to `{}#`
-- C-c + C-f jump to next hole
-- C-c + C-c pattern variables to case
-- C-c + C-, the target type and the context
-- C-c + C-. the target type and the context and the inferred type
-- C-c + C-r recommendation
-- C-c + C-SPA fill up the hole
-- C-c + C-a auto fill up the holes

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

-- @stretch: exercise `Bin` start

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc (m O) = m I
inc (m I) = (inc m) O
inc ⟨⟩ = ⟨⟩ I

-- inc unit test start

_ =
  begin
    inc (⟨⟩)
  ≡⟨⟩
    ⟨⟩ I
  ∎

_ =
  begin
    inc (⟨⟩ I)
  ≡⟨⟩
    ⟨⟩ I O
  ∎

_ =
  begin
    inc (⟨⟩ I O)
  ≡⟨⟩
    ⟨⟩ I I
  ∎

_ =
  begin
    inc (⟨⟩ I O I I)
  ≡⟨⟩
    (inc (⟨⟩ I O I)) O
  ≡⟨⟩
    ( (inc (⟨⟩ I O)) O ) O
  ≡⟨⟩
    ((⟨⟩ I I) O ) O
  ≡⟨⟩
    ⟨⟩ I I O O
  ∎

-- inc unit test end

to : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)

from : Bin -> ℕ
from (m O) = 2 * (from m)
from (m I) = 2 * (from m) + 1
from ⟨⟩ = 0

-- from & to unit test start

_ : (to 11) ≡ (⟨⟩ I O I I)
_ = refl

_ : (from (⟨⟩ I O I I)) ≡ 11
_ = refl

_ : (to 0) ≡ (⟨⟩ O)
_ = refl

_ : (to 1) ≡ (⟨⟩ I)
_ = refl

_ : (from (⟨⟩ I)) ≡ 1
_ = refl

_ : (from (⟨⟩ O)) ≡ 0
_ = refl

-- from & to unit test end

-- @stretch: exercise `Bin` end

-- import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

max_stars_repo_name: lonelyhentai/workspace

max_issues_repo_name: lonelyhentai/workspace

max_forks_repo_name: lonelyhentai/workspace


text:
{-
  A simple stack language example. Illustrating that one
  wants dependent elimination of inductive families.
-}

module StackLanguage where

open import Lib.Nat
open import Lib.Vec
open import Lib.Id

data Prog (A : Set) : Nat -> Set where
  init : Prog A 0
  push : forall {n} -> A -> Prog A n -> Prog A (suc n)
  pop  : forall {n} -> Prog A (suc n) -> Prog A n

⟦_⟧ : forall {A n} -> Prog A n -> Vec A n
⟦ init     ⟧ = ε
⟦ push x p ⟧ = x ► ⟦ p ⟧
⟦ pop p    ⟧ with ⟦ p ⟧
...             | x ► xs = xs

reify : forall {A n} -> Vec A n -> Prog A n
reify ε        = init
reify (x ► xs) = push x (reify xs)

normalise : forall {A n} -> Prog A n -> Prog A n
normalise p = reify ⟦ p ⟧

_≅_ : forall {A n} -> Prog A n -> Prog A n -> Set
p₁ ≅ p₂ = ⟦ p₁ ⟧ == ⟦ p₂ ⟧

sound : forall {A n} -> (p : Prog A n) -> normalise p ≅ p
sound init       = refl
sound (push x p) = cong (_►_ x) (sound p)
sound (pop p)    with ⟦ p ⟧ | sound p
...           | x ► xs | ih with ⟦ reify xs ⟧
sound (pop p) | x ► xs | refl  | .xs = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Base
open import Homotopy.Truncation

module Homotopy.Connected {i} where

is-connected : ℕ₋₂ → Set i → Set i
is-connected n A = is-contr (τ n A)

is-connected-is-prop : (n : ℕ₋₂) {A : Set i} → is-prop (is-connected n A)
is-connected-is-prop n = is-contr-is-prop

has-connected-fibers : {A B : Set i} → ℕ₋₂ → (A → B) → Set i
has-connected-fibers n f = ∀ x → is-connected n (hfiber f x)

module _ (n : ℕ₋₂) (A : Set i) where

  private
    τ-to-ττ : τ n A → τ n (τ (S n) A)
    τ-to-ττ = τ-extend-nondep (proj ◯ proj)

    τ-is-truncated-S : is-truncated (S n) (τ n A)
    τ-is-truncated-S = truncated-is-truncated-S n (τ-is-truncated n A)

    ττ-to-τ : τ n (τ (S n) A) → τ n A
    ττ-to-τ = τ-extend-nondep (τ-extend-nondep proj)

    τ-inv-ττ : (x : τ n A) → ττ-to-τ (τ-to-ττ x) ≡ x
    τ-inv-ττ = τ-extend ⦃ λ _ → ≡-is-truncated n (τ-is-truncated n A) ⦄
                 (λ _ → refl)

    ττ-inv-τ : (x : τ n (τ (S n) A)) → τ-to-ττ (ττ-to-τ x) ≡ x
    ττ-inv-τ = τ-extend ⦃ λ _ → ≡-is-truncated n (τ-is-truncated n _) ⦄
                 (τ-extend ⦃ λ _ → truncated-is-truncated-S n
                                     (≡-is-truncated n
                                       (τ-is-truncated n _)) ⦄
                   (λ _ → refl))

  τ-equiv-ττ : τ n A ≃ τ n (τ (S n) A)
  τ-equiv-ττ = (τ-to-ττ , iso-is-eq _ ττ-to-τ ττ-inv-τ τ-inv-ττ)

  ττ-equiv-τ : τ n (τ (S n) A) ≃ τ n A
  ττ-equiv-τ = (ττ-to-τ , iso-is-eq _ τ-to-ττ τ-inv-ττ ττ-inv-τ)

abstract
  contr-is-connected : (n : ℕ₋₂) {A : Set i}
    → (is-contr A → is-connected n A)
  contr-is-connected n (x , p) =
    (proj x , τ-extend ⦃ λ _ → ≡-is-truncated n (τ-is-truncated n _) ⦄
                (λ _ → ap proj (contr-has-all-paths (x , p) _ _)))

  connected-S-is-connected : (n : ℕ₋₂) {A : Set i}
    → (is-connected (S n) A → is-connected n A)
  connected-S-is-connected n p =
    equiv-types-truncated _ (ττ-equiv-τ n _) (contr-is-connected n p)

app-is-inj : ∀ {j} {A : Set i} {B : Set j} {n : ℕ₋₂} {f g : A → B} (x₀ : A)
  → (is-connected n A → is-truncated n B → f x₀ ≡ g x₀ → f ≡ g)
app-is-inj x₀ p q e = equiv-is-inj (τ-extend-equiv _ _ _) _ _
                                   (funext (contr-has-section p (proj x₀) e))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Structure.Operator.Ring where

import      Lvl
open import Logic
open import Logic.Predicate
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Operator
open import Structure.Operator.Group using (Group ; CommutativeGroup)
open import Structure.Operator.Monoid using (Monoid)
open import Structure.Operator.Properties hiding (distributivityₗ ; distributivityᵣ ; commutativity)
open import Syntax.Function
open import Type

-- TODO: Rg, Rng, Rig

private
  module Impl {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (𝟎 : T) where
    record NonZero (x : T) : Stmt{ℓₑ} where
      constructor intro
      field proof : (x ≢ 𝟎)

-- An algebraic structure over two operators, in which the first one is a commutative group, and the second one is associative and distributes over the first one.
-- Also called: Rg.
record Rng {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ [+]-commutative-group ⦄  : CommutativeGroup (_+_)
    ⦃ [⋅]-binary-operator ⦄    : BinaryOperator(_⋅_)
    ⦃ [⋅]-associativity ⦄      : Associativity(_⋅_)
    ⦃ [⋅][+]-distributivityₗ ⦄ : Distributivityₗ(_⋅_)(_+_)
    ⦃ [⋅][+]-distributivityᵣ ⦄ : Distributivityᵣ(_⋅_)(_+_)

  open CommutativeGroup([+]-commutative-group)
    using ()
    renaming(
      group               to [+]-group ;
      commutativity       to [+]-commutativity ;
      monoid              to [+]-monoid ;
      binary-operator     to [+]-binary-operator ;
      associativity       to [+]-associativity ;
      identity-existence  to [+]-identity-existence ;
      identity-existenceₗ to [+]-identity-existenceₗ ;
      identity-existenceᵣ to [+]-identity-existenceᵣ ;
      id                  to 𝟎 ;
      identity            to [+]-identity ;
      identityₗ           to [+]-identityₗ ;
      identityᵣ           to [+]-identityᵣ ;
      inverse-existence   to [+]-inverse-existence ;
      inv                 to −_ ;
      inv-function        to [−]-function ;
      inverse             to [+]-inverse ;
      inverseₗ            to [+]-inverseₗ ;
      inverseᵣ            to [+]-inverseᵣ
    ) public
  open Impl(𝟎) public

  _−_ : T → T → T
  x − y = x + (− y)

  ZeroDivisorₗ : T → Stmt
  ZeroDivisorₗ(a) = ∃(x ↦ (x ≢ 𝟎) ∧ (a ⋅ x ≡ 𝟎))

  ZeroDivisorᵣ : T → Stmt
  ZeroDivisorᵣ(a) = ∃(x ↦ (x ≢ 𝟎) ∧ (x ⋅ a ≡ 𝟎))

  ZeroDivisor : T → Stmt
  ZeroDivisor(a) = ∃(x ↦ (x ≢ 𝟎) ∧ ((a ⋅ x ≡ 𝟎) ∧ (x ⋅ a ≡ 𝟎)))

record RngObject {ℓ ℓₑ} : Stmt{Lvl.𝐒(ℓ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {T} : Type{ℓ}
    ⦃ equiv ⦄ : Equiv{ℓₑ}(T)
    _+_ : T → T → T
    _⋅_ : T → T → T
    ⦃ rng ⦄ : Rng(_+_)(_⋅_)
  open Rng(rng) public

record Unity {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) ⦃ rng : Rng(_+_)(_⋅_) ⦄ : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  open Rng(rng)
  field
    ⦃ [⋅]-identity-existence ⦄ : ∃(Identity(_⋅_))

  [⋅]-monoid : Monoid(_⋅_)
  [⋅]-monoid = record{}

  open Monoid([⋅]-monoid)
    using ()
    renaming(
      id                 to 𝟏 ;
      identity           to [⋅]-identity ;
      identityₗ          to [⋅]-identityₗ ;
      identityᵣ          to [⋅]-identityᵣ
    ) public

  DistinctIdentities = NonZero(𝟏)

-- Rng with unity.
-- Also called: Rig.
record Ring {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ rng ⦄   : Rng(_+_)(_⋅_)
    ⦃ unity ⦄ : Unity(_+_)(_⋅_)
  open Rng(rng) public
  open Unity(unity) public

record RingObject {ℓ ℓₑ} : Stmt{Lvl.𝐒(ℓ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {T} : Type{ℓ}
    ⦃ equiv ⦄ : Equiv{ℓₑ}(T)
    _+_ : T → T → T
    _⋅_ : T → T → T
    ⦃ ring ⦄ : Ring(_+_)(_⋅_)
  open Ring(ring) public

record Division {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) ⦃ rng : Rng(_+_)(_⋅_) ⦄ ⦃ unity : Unity(_+_)(_⋅_) ⦄ : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  open Rng(rng)
  open Unity(unity)
  field
    ⅟ : (x : T) → ⦃ NonZero(x) ⦄ → T
    [⋅]-inverseₗ : ∀{x} → ⦃ non-zero : NonZero(x) ⦄ → (x ⋅ (⅟ x) ≡ 𝟏)
    [⋅]-inverseᵣ : ∀{x} → ⦃ non-zero : NonZero(x) ⦄ → ((⅟ x) ⋅ x ≡ 𝟏)

  _/_ : T → (y : T) → ⦃ NonZero(y) ⦄ → T
  x / y = x ⋅ (⅟ y)

-- Ring with division.
-- Also called: Ring.
record DivisionRing {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ ring ⦄     : Ring(_+_)(_⋅_)
    ⦃ division ⦄ : Division(_+_)(_⋅_)
  open Ring    (ring)     public
  open Division(division) public

record DivisionRingObject {ℓ ℓₑ} : Stmt{Lvl.𝐒(ℓ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {T} : Type{ℓ}
    ⦃ equiv ⦄ : Equiv{ℓₑ}(T)
    _+_ : T → T → T
    _⋅_ : T → T → T
    ⦃ divisionRing ⦄ : DivisionRing(_+_)(_⋅_)
  open DivisionRing(divisionRing) public

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda