text:
module Singleton where

open import Level
open import Data.Unit
open import Data.Product
open import Function
open import Relation.Binary
open import Function.Inverse
open import Function.Equality as FE
open import Relation.Binary.PropositionalEquality as P

open import Pi using (⟦_⟧; _⟷_ )

embed₁ : Set → Set
embed₁ b = Σ b (λ _ → ⊤)

B-to-Σ⊤ : {B : Set} → B → embed₁ B
B-to-Σ⊤ v = (v , tt)

Σ⊤-to-B : {B : Set} → embed₁ B → B
Σ⊤-to-B (v , _) = v

BΣ₁ : ∀ {b} → Inverse (P.setoid b) (P.setoid (embed₁ b))
BΣ₁ = record {
        to = record { _⟨$⟩_ = B-to-Σ⊤; cong = P.cong B-to-Σ⊤  }
      ; from = record { _⟨$⟩_ = Σ⊤-to-B; cong = P.cong Σ⊤-to-B }
      ; inverse-of = record { left-inverse-of = λ _ → refl
                               ; right-inverse-of = λ x → refl } }

data Singleton {c : Level} {A : Set c} : A → Set c where
  singleton : (x : A) -> Singleton x

-- That a Singleton type is a setoid is not needed, but here is the proof anyways.
data _∼_ {c : Level} {A : Set c} {v : A} (x : Singleton v) (y : Singleton v) : Set c where
    uniq : x ∼ y

∼Equiv : {c : Level} {A : Set c} {v : A} → IsEquivalence {_} {_} {Singleton v}  _∼_
∼Equiv {v = v } = record {
                    refl = uniq
                  ; sym = λ _ →  uniq
                  ; trans = λ _ _ → uniq }

SingSetoid : {c c : Level} → (A : Setoid c c) → (Setoid.Carrier A) → Setoid c c
SingSetoid A v = record {
                   Carrier = Singleton v
                 ; _≈_ = _∼_
                 ; isEquivalence = ∼Equiv }

-- We can map a type to its Σ of Singletons and back.
embed₂ : Set → Set
embed₂ b = Σ b Singleton

B-to-ΣS : {B : Set} → B → embed₂ B
B-to-ΣS v = (v , singleton v)

ΣS-to-B : {B : Set} → embed₂ B → B
ΣS-to-B x = proj₁ x

right-inverse : ∀ {c} {b : Set c} → (x : Σ b (Singleton {A = b})) → (proj₁ x , singleton (proj₁ x)) ≡ x
right-inverse (v , singleton .v) = refl

BΣ₂ : ∀ {b} → Inverse (P.setoid b) (P.setoid (embed₂ b))
BΣ₂ =  record {
         to = record { _⟨$⟩_ = B-to-ΣS; cong = P.cong B-to-ΣS }
       ; from = record { _⟨$⟩_ = ΣS-to-B; cong = P.cong ΣS-to-B }
       ; inverse-of = record { left-inverse-of = λ x → refl
                             ; right-inverse-of = right-inverse } }

-- A generalized idea of a permutation: a bijection between any two types
Permutation : Set → Set -> Set
Permutation a b = Inverse (P.setoid a) (P.setoid b)

-- Now, what we really want is to interpret Pi combinators as
-- permutations.  We need a refined version of embed₂ which
-- allows us to use a permutation to transport things.

embed₃ : {l : Level} → (S T : Setoid l l) → Inverse S T → Setoid l l
embed₃ S T f = record {
                 Carrier = Σ A (λ b → Singleton (to f ⟨$⟩ b))
               ; _≈_ = _≡_
               ; isEquivalence = P.isEquivalence }
               where open Inverse {From = S} {T}
                     A = Setoid.Carrier S

ext: agda

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --copatterns #-}

module HighlightCopattern where

record WrapSet : Set₂ where
  field
    wrapped : Set₁
open WrapSet

my : WrapSet
wrapped my = Set    -- 'wrapped' should be highlighted in projection color

proj : WrapSet → Set₁
proj w = wrapped w  -- 'wrapped' should be highlighted in projection color

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where

open Lattice L
open import Algebra.Structures
open import Algebra.FunctionProperties _≈_
import Algebra.Properties.Semilattice as SL
open import Relation.Binary
import Relation.Binary.Lattice as R
open import Relation.Binary.Reasoning.Setoid  setoid
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Data.Product using (_,_; swap)

------------------------------------------------------------------------
-- Every lattice contains two semilattices.

∧-idempotent : Idempotent _∧_
∧-idempotent x = begin
  x ∧ x            ≈⟨ refl ⟨ ∧-cong ⟩ sym (∨-absorbs-∧ _ _) ⟩
  x ∧ (x ∨ x ∧ x)  ≈⟨ ∧-absorbs-∨ _ _ ⟩
  x                ∎

∨-idempotent : Idempotent _∨_
∨-idempotent x = begin
  x ∨ x      ≈⟨ refl ⟨ ∨-cong ⟩ sym (∧-idempotent _) ⟩
  x ∨ x ∧ x  ≈⟨ ∨-absorbs-∧ _ _ ⟩
  x          ∎

∧-isSemilattice : IsSemilattice _≈_ _∧_
∧-isSemilattice = record
  { isBand = record
    { isSemigroup = record
      { isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = ∧-cong
        }
      ; assoc         = ∧-assoc
      }
    ; idem = ∧-idempotent
    }
  ; comm   = ∧-comm
  }

∧-semilattice : Semilattice l₁ l₂
∧-semilattice = record { isSemilattice = ∧-isSemilattice }

∨-isSemilattice : IsSemilattice _≈_ _∨_
∨-isSemilattice = record
  { isBand = record
    { isSemigroup = record
      { isMagma = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = ∨-cong
        }
      ; assoc         = ∨-assoc
      }
    ; idem = ∨-idempotent
    }
  ; comm   = ∨-comm
  }

∨-semilattice : Semilattice l₁ l₂
∨-semilattice = record { isSemilattice = ∨-isSemilattice }

open SL ∧-semilattice public using (poset)
open Poset poset using (_≤_; isPartialOrder)

------------------------------------------------------------------------
-- The dual construction is also a lattice.

∧-∨-isLattice : IsLattice _≈_ _∧_ _∨_
∧-∨-isLattice = record
  { isEquivalence = isEquivalence
  ; ∨-comm        = ∧-comm
  ; ∨-assoc       = ∧-assoc
  ; ∨-cong        = ∧-cong
  ; ∧-comm        = ∨-comm
  ; ∧-assoc       = ∨-assoc
  ; ∧-cong        = ∨-cong
  ; absorptive    = swap absorptive
  }

∧-∨-lattice : Lattice _ _
∧-∨-lattice = record { isLattice = ∧-∨-isLattice }

------------------------------------------------------------------------
-- Every algebraic lattice can be turned into an order-theoretic one.

isOrderTheoreticLattice : R.IsLattice _≈_ _≤_ _∨_ _∧_
isOrderTheoreticLattice = record
  { isPartialOrder = isPartialOrder
  ; supremum       = supremum
  ; infimum        = infimum
  }
  where
  ∧-meetSemilattice = SL.orderTheoreticMeetSemilattice ∧-semilattice
  ∨-joinSemilattice = SL.orderTheoreticJoinSemilattice ∨-semilattice
  open R.MeetSemilattice ∧-meetSemilattice using (infimum)
  open R.JoinSemilattice ∨-joinSemilattice using ()
    renaming (supremum to supremum′; _≤_ to _≤′_)

  -- An alternative but equivalent interpretation of the order _≤_.

  sound : ∀ {x y} → x ≤′ y → x ≤ y
  sound {x} {y} y≈y∨x = sym $ begin
    x ∧ y        ≈⟨ ∧-congˡ y≈y∨x ⟩
    x ∧ (y ∨ x)  ≈⟨ ∧-congˡ (∨-comm y x) ⟩
    x ∧ (x ∨ y)  ≈⟨ ∧-absorbs-∨ x y ⟩
    x            ∎

  complete : ∀ {x y} → x ≤ y → x ≤′ y
  complete {x} {y} x≈x∧y = sym $ begin
    y ∨ x        ≈⟨ ∨-congˡ x≈x∧y ⟩
    y ∨ (x ∧ y)  ≈⟨ ∨-congˡ (∧-comm x y) ⟩
    y ∨ (y ∧ x)  ≈⟨ ∨-absorbs-∧ y x ⟩
    y            ∎

  supremum : R.Supremum _≤_ _∨_
  supremum x y =
    let x∨y≥x , x∨y≥y , greatest = supremum′ x y
    in sound x∨y≥x , sound x∨y≥y ,
       λ z x≤z y≤z → sound (greatest z (complete x≤z) (complete y≤z))

orderTheoreticLattice : R.Lattice _ _ _
orderTheoreticLattice = record { isLattice = isOrderTheoreticLattice }

------------------------------------------------------------------------
-- One can replace the underlying equality with an equivalent one.

replace-equality : {_≈′_ : Rel Carrier l₂} →
                   (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → Lattice _ _
replace-equality {_≈′_} ≈⇔≈′ = record
  { _≈_       = _≈′_
  ; _∧_       = _∧_
  ; _∨_       = _∨_
  ; isLattice = record
    { isEquivalence = record
      { refl  = to ⟨$⟩ refl
      ; sym   = λ x≈y → to ⟨$⟩ sym (from ⟨$⟩ x≈y)
      ; trans = λ x≈y y≈z → to ⟨$⟩ trans (from ⟨$⟩ x≈y) (from ⟨$⟩ y≈z)
      }
    ; ∨-comm     = λ x y → to ⟨$⟩ ∨-comm x y
    ; ∨-assoc    = λ x y z → to ⟨$⟩ ∨-assoc x y z
    ; ∨-cong     = λ x≈y u≈v → to ⟨$⟩ ∨-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
    ; ∧-comm     = λ x y → to ⟨$⟩ ∧-comm x y
    ; ∧-assoc    = λ x y z → to ⟨$⟩ ∧-assoc x y z
    ; ∧-cong     = λ x≈y u≈v → to ⟨$⟩ ∧-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
    ; absorptive = (λ x y → to ⟨$⟩ ∨-absorbs-∧ x y)
                 , (λ x y → to ⟨$⟩ ∧-absorbs-∨ x y)
    }
  } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})


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

module Categories.Object.Subobject.Properties where

open import Level
open import Data.Product
open import Data.Unit
open import Function using (_$_)

open import Relation.Binary using (_=[_]⇒_)
open import Relation.Binary.Bundles
open import Relation.Binary.OrderMorphism

open import Categories.Category
open import Categories.Functor
open import Categories.Functor.Presheaf
open import Categories.Category.Slice
open import Categories.Object.Subobject
open import Categories.Diagram.Pullback renaming (glue to glue-pullback)
open import Categories.Diagram.Pullback.Properties
open import Categories.Category.Instance.Posets
open import Categories.Category.Instance.Setoids
open import Categories.Adjoint.Instance.PosetCore
import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
open import Categories.Morphism.Notation

module _ {o ℓ e} {𝒞 : Category o ℓ e} (has-pullbacks : ∀ {A B X} → (f : 𝒞 [ A , X ]) → (g : 𝒞 [ B , X ]) → Pullback 𝒞 f g) where
  private
    module 𝒞 = Category 𝒞

  open 𝒞.HomReasoning
  open 𝒞.Equiv

  open Mor 𝒞
  open MR 𝒞
  open _↣_

  -- The Subobject functor, into the category of posets
  Subₚ : Presheaf 𝒞 (Posets (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) (ℓ ⊔ e))
  Subₚ = record
    { F₀ = Subobjects 𝒞
    ; F₁ = λ f → record
      { fun = morphism f
      ; monotone = λ {(α , m) (β , n)} h → monotone f {(α , m)} {β , n} h
      }
    ; identity = λ {A} {(α , m)} →
      let pid = has-pullbacks 𝒞.id (mor m)
      in record
        { from = record
          { h = Pullback.p₂ pid
          ; △ = ⟺ (Pullback.commute pid) ○ 𝒞.identityˡ
          }
        ; to = record
          { h = Pullback.universal pid id-comm-sym
          ; △ = Pullback.p₁∘universal≈h₁ pid
          }
        ; iso = record
          { isoˡ = pullback-identity 𝒞 pid
          ; isoʳ = Pullback.p₂∘universal≈h₂ pid
          }
        }
    ; homomorphism = λ {X} {Y} {Z} {f} {g} {(α , m)} →
      let pfg = has-pullbacks (𝒞 [ f ∘ g ]) (mor m)
          pf = has-pullbacks f (mor m)
          pg = has-pullbacks g (Pullback.p₁ pf)
          iso = up-to-iso 𝒞 pfg (glue-pullback 𝒞 pf pg)
          module iso = _≅_ iso
      in record
        { from = record
          { h = iso.from
          ; △ = Pullback.p₁∘universal≈h₁ pg
          }
        ; to = record
          { h = iso.to
          ; △ = Pullback.p₁∘universal≈h₁ pfg
          }
        ; iso = record
          { isoˡ = iso.isoˡ
          ; isoʳ = iso.isoʳ
          }
        }
    ; F-resp-≈ = λ {A B f g} eq {(α , m)} →
      let pf = has-pullbacks f (mor m)
          pg = has-pullbacks g (mor m)
          iso = up-to-iso 𝒞 pf (pullback-resp-≈ 𝒞 pg (sym eq) refl)
          module iso = _≅_ iso
      in record
        { from = record
          { h = iso.from
          ; △ = Pullback.p₁∘universal≈h₁ pg
          }
        ; to = record
          { h = iso.to
          ; △ = Pullback.p₁∘universal≈h₁ pf
          }
        ; iso = record
          { isoˡ = iso.isoˡ
          ; isoʳ = iso.isoʳ
          }
        }
    }
    where
      morphism : ∀ {A B} → (f : 𝒞 [ B , A ]) → Σ[ α ∈ 𝒞.Obj ] (α ↣ A) → Σ[ β ∈ 𝒞.Obj ] (β ↣ B)
      morphism f (α , m) =
        let pb = has-pullbacks f (mor m)
        in Pullback.P pb , record
          { mor = Pullback.p₁ pb
          ; mono = Pullback-resp-Mono 𝒞 pb (mono m)
          }

      monotone : ∀ {A B} (f : 𝒞 [ B , A ]) → Poset._≤_ (Subobjects 𝒞 A) =[ morphism f ]⇒ Poset._≤_ (Subobjects 𝒞 B)
      monotone f {(α , m)} {(β , n)} h =
        let pm = has-pullbacks f (mor m)
            pn = has-pullbacks f (mor n)
        in record
          { h = Pullback.universal pn $ begin
              𝒞 [ f ∘ Pullback.p₁ pm ] ≈⟨ Pullback.commute pm ⟩
              𝒞 [ mor m ∘ Pullback.p₂ pm ] ≈⟨ pushˡ (⟺ (Slice⇒.△ h)) ⟩
              𝒞 [ mor n ∘ 𝒞 [ Slice⇒.h h ∘ Pullback.p₂ pm ] ] ∎
          ; △ = Pullback.p₁∘universal≈h₁ pn
          }

  -- The subobject functor as a presheaf on Setoids.
  -- This is just Subₚ composed with the 'Core'
  Sub : Presheaf 𝒞 (Setoids (o ⊔ ℓ ⊔ e) (ℓ ⊔ e))
  Sub =  Core ∘F Subₚ

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text: module Issue2217.M where

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.Core where

open import Function.Base using (_on_)
open import Level using (Level; _⊔_; suc)

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

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

-- Heterogeneous binary relations

REL : Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
REL A B ℓ = A → B → Set ℓ

-- Homogeneous binary relations

Rel : Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Rel A ℓ = REL A A ℓ

------------------------------------------------------------------------
-- Relationships between relations
------------------------------------------------------------------------

infixr 4 _⇒_ _=[_]⇒_

-- Implication/containment - could also be written _⊆_.

_⇒_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _
P ⇒ Q = ∀ {x y} → P x y → Q x y

-- Generalised implication - if P ≡ Q it can be read as "f preserves P".

_=[_]⇒_ : Rel A ℓ₁ → (A → B) → Rel B ℓ₂ → Set _
P =[ f ]⇒ Q = P ⇒ (Q on f)

-- A synonym for _=[_]⇒_.

_Preserves_⟶_ : (A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _
f Preserves P ⟶ Q = P =[ f ]⇒ Q

-- A binary variant of _Preserves_⟶_.

_Preserves₂_⟶_⟶_ : (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
_∙_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y u v} → P x y → Q u v → R (x ∙ u) (y ∙ v)


text:
module equational where

open import lib

postulate
  A : Set
  a : A
  b : A
  c : A
  d : A
  f : A → A
  g : A → A
  h : A → A → A
  p : a ≡ b
  q : b ≡ c
  r : f a ≡ a
  s : h a a ≡ a
  t : ∀ x → f (g x) ≡ g (f x)
  u : ∀ {x} → f x ≡ x → g (g x) ≡ x  -- {x} means x is implicit, so you do not need to write it when you call u
  v : ∀ x → h x d ≡ x

L0 : c ≡ c
L0 = refl

L1 : c ≡ a
L1 rewrite p | q = refl

L2 : h (f a) (f (f a)) ≡ a
L2 rewrite r | r = s

L3 : f b ≡ b
L3 rewrite sym p = r

L4 : h (h d d) d ≡ d
L4 rewrite s | v d = v d

L5 : f (g (g a)) ≡ a
L5 rewrite t ( g a) | t a | r | u r  = refl

L6 : f (g (f (g a))) ≡ g (g (f (f a)))
L6 rewrite t a | r | u r | r | u r  = refl

L7 : ∀ x → f (f (f x)) ≡ x → f (f (f (f (f x)))) ≡ x → f x ≡ x
L7 x y z rewrite y | z | r  = y


text:
module libbijection where

open import Level renaming ( zero to Zero ; suc to Suc )
open import Data.Nat
open import Data.Maybe
open import Data.List hiding ([_] ; sum )
open import Data.Nat.Properties
open import Relation.Nullary
open import Data.Empty
open import Data.Unit hiding ( _≤_ )
open import  Relation.Binary.Core hiding (_⇔_)
open import  Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality
open import Function.Inverse hiding (sym)
open import Function.Bijection renaming (Bijection to Bijection1)
open import Function.Equality hiding (cong)

open import logic
open import nat

-- record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
--    field
--        fun←  :  S → R
--        fun→  :  R → S
--        fiso← : (x : R)  → fun← ( fun→ x )  ≡ x
--        fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x
--
-- injection :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
-- injection R S f = (x y : R) → f x ≡ f y → x ≡ y

open Bijection

b→injection1 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection S R (fun← b)
b→injection1 R S b x y eq = trans (  sym ( fiso→ b x ) ) (trans (  cong (λ k → fun→ b k ) eq ) ( fiso→ b y  ))

--
-- injection as an uniquneness of bijection
--
b→injection0 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection R S (fun→ b)
b→injection0 R S b x y eq = begin
          x
        ≡⟨ sym ( fiso← b x ) ⟩
          fun← b ( fun→ b x )
        ≡⟨ cong (λ k → fun← b k ) eq ⟩
          fun← b ( fun→ b y )
        ≡⟨  fiso← b y  ⟩
          y
        ∎  where open ≡-Reasoning

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

≡-Setoid :  {n : Level} (R : Set n) → Setoid n n
≡-Setoid R = record {
      Carrier = R
    ; _≈_ = _≡_
    ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }
  }

libBijection :  {n m : Level} (R : Set n) (S : Set m) → Bijection R S  → Bijection1 (≡-Setoid R) (≡-Setoid S)
libBijection R S b = record {
     to = record { _⟨$⟩_   = λ x → fun→ b x ; cong = λ i=j → cong (fun→ b) i=j }
   ; bijective  = record {
         injective = λ {x} {y} eq → b→injection0 R S b x y eq
       ; surjective = record { from = record { _⟨$⟩_   = λ x → fun← b x ; cong = λ i=j → cong (fun← b) i=j }
          ; right-inverse-of = λ x → fiso→ b x }
      }
  }

fromBijection1 :  {n m : Level} (R : Set n) (S : Set m) → Bijection1 (≡-Setoid R) (≡-Setoid S) → Bijection R S
fromBijection1 R S b = record {
      fun←  = Π._⟨$⟩_ (Surjective.from (Bijective.surjective (Bijection1.bijective b)))
    ; fun→  = Π._⟨$⟩_ (Bijection1.to b)
    ; fiso← = λ x → Bijective.injective (Bijection1.bijective b) (fb1 x)
    ; fiso→ =  Surjective.right-inverse-of  (Bijective.surjective (Bijection1.bijective b))
  } where
      --  fun← b x ≡ fun← b y → x ≡ y
      --  fun← (fun→ ( fun← x ))  ≡  fun← x
      --  fun→ ( fun← x )  ≡ x
     fb1 : (x : R) → Π._⟨$⟩_ (Bijection1.to b) (Surjective.from (Bijective.surjective (Bijection1.bijective b)) ⟨$⟩ (Bijection1.to b ⟨$⟩ x))  ≡ Π._⟨$⟩_ (Bijection1.to b) x
     fb1 x = begin
          Π._⟨$⟩_ (Bijection1.to b) (Surjective.from (Bijective.surjective (Bijection1.bijective b)) ⟨$⟩ (Bijection1.to b ⟨$⟩ x))
             ≡⟨ Surjective.right-inverse-of  (Bijective.surjective (Bijection1.bijective b)) _ ⟩
          Π._⟨$⟩_ (Bijection1.to b) x ∎ where open ≡-Reasoning

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
{-

A parameterized family of structures S can be combined into a single structure:
X ↦ (a : A) → S a X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Parameterized where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Functions.FunExtEquiv
open import Cubical.Foundations.SIP

module _ {ℓ ℓ₁ ℓ₂} (A : Type ℓ) where

  ParamStructure : (S : A → Type ℓ₁ → Type ℓ₂)
    → Type ℓ₁ → Type (ℓ-max ℓ ℓ₂)
  ParamStructure S X = (a : A) → S a X

  ParamEquivStr : {S : A → Type ℓ₁ → Type ℓ₂} {ℓ₃ : Level}
    → (∀ a → StrEquiv (S a) ℓ₃) → StrEquiv (ParamStructure S) (ℓ-max ℓ ℓ₃)
  ParamEquivStr ι (X , l) (Y , m) e = ∀ a → ι a (X , l a) (Y , m a) e

  ParamUnivalentStr : {S : A → Type ℓ₁ → Type ℓ₂} {ℓ₃ : Level}
    (ι : ∀ a → StrEquiv (S a) ℓ₃) (θ : ∀ a → UnivalentStr (S a) (ι a))
    → UnivalentStr (ParamStructure S) (ParamEquivStr ι)
  ParamUnivalentStr ι θ e = compEquiv (equivPi λ a → θ a e) funExtEquiv

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


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

import Tutorials.Monday-Complete as Mon
import Tutorials.Tuesday-Complete as Tue
import Tutorials.Wednesday-Complete as Wed
open Mon using (⊤; tt; ℕ; zero; suc)
open Mon.Simple using (_⊎_; inl; inr)
open Tue.Product using (Σ; _,_; fst; snd; _×_)

module Tutorials.Thursday where

variable
  A B C S : Set

-- Things that we skipped so far
--------------------------------

module WithAbstraction where
  open Mon using (Bool; true; false; Pred; _≡_; refl; _+_; subst; +-comm)
  open Mon.List using (List; []; _∷_)

  -- With abstraction
  -- You can use "with abstraction" to pattern match on intermediary computations
  -- These can be nested, or executed simultaneously

  filter : (A → Bool) → List A → List A
  filter f [] = []
  filter f (x ∷ xs) with f x
  filter f (x ∷ xs) | true = x ∷ filter f xs
  filter f (x ∷ xs) | false = filter f xs

  -- Alternative notation
  filter′ : (A → Bool) → List A → List A
  filter′ f [] = []
  filter′ f (x ∷ xs) with f x
  ...                | true = x ∷ filter′ f xs
  ...                | false = filter′ f xs

  -- The goal type and the type of the arguments are generalised over the value of the scrutinee
  thm : {P : Pred ℕ} (n m : ℕ) → P (n + m) → P (m + n)
  -- 1) Here (p : P (n + m)) and (eq : n + m ≡ m + n)
  -- thm n m p with +-comm n m
  -- thm n m p | eq = {!!}
  -- 2) Here (p : P x) and (eq : x ≡ m + n)
  -- thm n m p with n + m | +-comm n m
  -- thm n m p | x | eq = {!!}
  -- 3) Pattern matching we get (p : P (m + n)), the dot signifies that the argument is uniquely determined
  thm n m p with n + m | +-comm n m
  thm n m p | .(m + n) | refl = p

  -- This is such a common formula that there is special syntax for it
  thm′ : {P : Pred ℕ} (n m : ℕ) → P (n + m) → P (m + n)
  thm′ n m p rewrite +-comm n m = p

  -- We could use subst to be more explicit about *where* the rewrite happens
  thm′′ : {P : Pred ℕ} (n m : ℕ) → P (n + m) → P (m + n)
  thm′′ {P} n m p = subst {P = P} (+-comm n m) p

-- A little on coinductive types
--------------------------------

-- Stolen from https://github.com/pigworker/CS410-17/blob/master/lectures/Lec6Done.agda

ListT : Set → Set → Set
ListT X B = ⊤ ⊎ (X × B)

module List where
  data List (A : Set) : Set where
    [] : List A
    _∷_ : A → List A → List A

  mkList : ListT A (List A) → List A
  mkList x = {!!}

  foldr : (ListT A B → B) → List A → B
  foldr alg xs = {!!}

  list-id : List A → List A
  list-id = {!!}

  incr : ListT A ℕ → ℕ
  incr x = {!!}

  length : List A → ℕ
  length = {!!}

module CoList where
  record CoList (A : Set) : Set where
    coinductive
    field
      next : ListT A (CoList A)

  open CoList

  [] : CoList A
  [] = {!!}

  _∷_ : A → CoList A → CoList A
  (x ∷ xs) = {!!}

  unfoldr : (S → ListT A S) → S → CoList A
  unfoldr coalg s = {!!}

  colist-id : CoList A → CoList A
  colist-id = {!!}

  repeat : A → CoList A
  repeat = {!!}

  take : ℕ → CoList A → List.List A
  take n xs = {!!}

module Stream where
  record Stream (A : Set) : Set where
    coinductive
    field
      head : A
      tail : Stream A

  open Stream

  forever : A → Stream A
  forever x = {!!}

  unfold : (S → A × S) → S → Stream A
  unfold coalg s = {!!}

---------------------------------------------
-- If you are interested in more
-- Documentation for Agda: https://agda.readthedocs.io/en/v2.6.0.1/index.html
-- Programming Language Foundations in Agda: https://plfa.github.io/
-- Lots of other nice tutorials online
-- The standard library: https://agda.github.io/agda-stdlib/

max_stars_repo_name: poncev/agda-bcam

max_issues_repo_name: poncev/agda-bcam

max_forks_repo_name: poncev/agda-bcam


text:
{- Copyright © 1992–2002 The University of Glasgow
Copyright © 2015 Benjamin Barenblat

Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
this file except in compliance with the License.  You may obtain a copy of the
License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed
under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
CONDITIONS OF ANY KIND, either express or implied.  See the License for the
specific language governing permissions and limitations under the License. -}

module B.Prelude.Functor where

import Category.Monad as Monad
import Category.Functor
import Data.List
import Data.Maybe
open import Function using (_∘_)

open Category.Functor
  using (RawFunctor)
  public

open Category.Functor.RawFunctor ⦃...⦄
  using (_<$>_)
  public

instance
  Functor-List : ∀ {ℓ} → RawFunctor (Data.List.List {ℓ})
  Functor-List = Monad.RawMonad.rawFunctor Data.List.monad

  Functor-Maybe : ∀ {ℓ} → RawFunctor (Data.Maybe.Maybe {ℓ})
  Functor-Maybe = Monad.RawMonad.rawFunctor Data.Maybe.monad

  Functor-Function : ∀ {ℓ} {r : Set ℓ} → RawFunctor {ℓ} (λ s → (r → s))
  Functor-Function {r} =
    -- I could say _<$>_ = _∘_ here, but that makes type checking much more
    -- challenging.
    record { _<$>_ = λ f g → f ∘ g }

  -- TODO: Do proper instance for dependent pairs

max_stars_repo_name: bbarenblat/B

max_issues_repo_name: bbarenblat/B

max_forks_repo_name: bbarenblat/B


text:
{-# OPTIONS --show-implicit #-}

module BottomUp where

open import Foundation.Primitive
open import Foundation.Bottom
open import Foundation.Equivalence

open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit

module NegEquiv {ℓ'} (⊥ : Set ℓ') ⦃ _ : ∀ {b} → IsBottom ⊥ b ⦄ where

  _≉_ : ∀ {a} {A : Set a} {ℓ} ⦃ _ : Equivalence A ℓ ⦄ → A → A → Set (ℓ ⊔ ℓ')
  x ≉ y = x ≈ y → ⊥

module Data-⊥ where

  data Data⊥ : Set where

  instance bottom-rule : ∀ {b} → IsBottom Data⊥ b
  IsBottom.⊥-elim (bottom-rule {b}) () {B}

module IsDecisive-Module {ℓ'} (⊥ : Set ℓ') ⦃ _ : ∀ {b} → IsBottom ⊥ b ⦄ where

  open NegEquiv ⊥

  record IsDecisive a
                    (Decision : (A : Set a) → Set a)
                    (yes-c : {A : Set a} → A → Decision A)
                    (no-c : {A : Set a} → (A → ⊥) → Decision A)
                    ℓ
                    ⦃ equiv-decision : {A : Set a} → Equivalence (Decision A) ℓ ⦄
                    : Set (ℓ ⊔ ⟰ a ⊔ ℓ') where
    field
      yes-correct : {A : Set a} → (dec : Decision A) → (x : A) → yes-c x ≈ dec
      no-correct : {A : Set a} → (dec : Decision A) → (x : A → ⊥) → no-c x ≈ dec
      yes-no-incompat : {A : Set a} (x : A) (nx : A → ⊥) → yes-c x ≉ no-c nx

  open IsDecisive ⦃ … ⦄ public

record ⊤′ {a} : Set a where
  instance constructor tt

module Data-Decision {ℓ} (⊥ : Set ℓ) ⦃ _ : ∀ {b} → IsBottom ⊥ b ⦄ where

  data Decision {a} (A : Set a) : Set (a ⊔ ℓ) where
    yes : A → Decision A
    no : (A → ⊥) → Decision A

  open IsDecisive-Module ⊥

  instance dec-equiv : ∀ {a} {A : Set a} → Equivalence (Decision {a} A) a
  (dec-equiv {a} {A} Equivalence.≈ yes x₁) (yes x₂) = ⊤′
  (dec-equiv {a} {A} Equivalence.≈ yes x₁) (no x₂) = ⊥-elim (x₂ x₁)
  (dec-equiv {a} {A} Equivalence.≈ no x₁) (yes x₂) = ⊥-elim (x₁ x₂)
  (dec-equiv {a} {A} Equivalence.≈ no x₁) (no x₂) = ⊤′
  IsEquivalence.reflexivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (yes x₁) = tt
  IsEquivalence.reflexivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (no x₁) = tt
  IsEquivalence.symmetry (Equivalence.isEquivalence (dec-equiv {a} {A})) (yes x₁) (yes x₂) x₃ = x₃
  IsEquivalence.symmetry (Equivalence.isEquivalence (dec-equiv {a} {A})) (yes x₁) (no x₂) x₃ = x₃
  IsEquivalence.symmetry (Equivalence.isEquivalence (dec-equiv {a} {A})) (no x₁) (yes x₂) x₃ = x₃
  IsEquivalence.symmetry (Equivalence.isEquivalence (dec-equiv {a} {A})) (no x₁) (no x₂) x₃ = x₃
  IsEquivalence.transitivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (yes x₁) (yes x₂) (yes x₃) x₄ x₅ = tt
  IsEquivalence.transitivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (yes x₁) (yes x₂) (no x₃) x₄ x₅ = ⊥-elim (x₃ x₂)
  IsEquivalence.transitivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (yes x₁) (no x₂) (yes x₃) x₄ x₅ = tt
  IsEquivalence.transitivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (yes x₁) (no x₂) (no x₃) x₄ x₅ = ⊥-elim (x₂ x₁)
  IsEquivalence.transitivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (no x₁) (yes x₂) (yes x₃) x₄ x₅ = ⊥-elim (x₁ x₂)
  IsEquivalence.transitivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (no x₁) (yes x₂) (no x₃) x₄ x₅ = tt
  IsEquivalence.transitivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (no x₁) (no x₂) (yes x₃) x₄ x₅ = ⊥-elim (x₂ x₃)
  IsEquivalence.transitivity (Equivalence.isEquivalence (dec-equiv {a} {A})) (no x₁) (no x₂) (no x₃) x₄ x₅ = tt

  instance dec-instance : ∀ {a} → IsDecisive (a ⊔ ℓ) (Decision {a ⊔ ℓ}) yes no (a ⊔ ℓ)
  IsDecisive-Module.IsDecisive.yes-correct (dec-instance {a}) {A} (yes x₁) x₂ = tt
  IsDecisive-Module.IsDecisive.yes-correct (dec-instance {a}) {A} (no x₁) x₂ = ⊥-elim (x₁ x₂)
  IsDecisive-Module.IsDecisive.no-correct (dec-instance {a}) {A} (yes x₁) x₂ = ⊥-elim (x₂ x₁)
  IsDecisive-Module.IsDecisive.no-correct (dec-instance {a}) {A} (no x₁) x₂ = tt
  IsDecisive-Module.IsDecisive.yes-no-incompat (dec-instance {a}) x₁ nx x₂ = nx x₁

open Data-⊥

-- module DecisionModule (⊥ : Set) ⦃ _ : ∀ {a} {b} → IsBottom ⊥ a b ⦄ where

--   record IsDecidableEquivalence {a} {A : Set a} {ℓ} (_≈_ : A → A → Set ℓ) : Set (a ⊔ ℓ) where
--     infix 4 _≈?_
--     field
--       isEquivalence : IsEquivalence _≈_
--       _≈?_ : (x y : A) → Decision (x ≈ y)

--   record DecidableEquivalence {a} (A : Set a) ℓ : Set (lsuc (a ⊔ ℓ)) where
--     field
--       ⦃ equivalence ⦄ : Equivalence A ℓ
--     --open Equivalence equivalence
--     infix 4 _≈?_
--     field
--       _≈?_ : (x y : A) → Decision (x ≈ y)

--   open DecidableEquivalence ⦃ … ⦄ public

--   record DecidableEquivalence' {a} (A : Set a) : Set (lsuc a) where
--     field
--       ⦃ equivalence ⦄ : Equivalence A a
--     infix 4 _≈?_
--     field
--       _≈?_ : (x y : A) → Decision (x ≈ y)

-- data ⊥-fake : Set where
--   faker : ⊥-fake

-- ⊥fake-rule : ∀ {a} {A : Set a} → (A → ⊥-fake) → A → ∀ {b} {B : Set b} → B
-- ⊥fake-rule x x₁ with x x₁
-- ⊥fake-rule x x₁ | faker = {!!}

-- open DecisionModule ⊥

-- data Tree (A : Set) : Set where
--   value : A → Tree A
--   leaf : Tree A
--   branch : Tree A → Tree A → Tree A

-- substitute₁List : ∀ {a} {A : Set a} ⦃ _ : DecidableEquivalence A a ⦄ → A → A → List A → List A
-- substitute₁List x₁ y [] = []
-- substitute₁List x₁ y (x₂ ∷ xs) with x₁ ≈? x₂
-- substitute₁List x₁ y (x₂ ∷ xs) | yes x₃ = y ∷ substitute₁List x₁ y xs
-- substitute₁List x₁ y (x₂ ∷ xs) | no x₃ = x₂ ∷ substitute₁List x₁ y xs

-- open import Agda.Builtin.Nat
-- open import Agda.Builtin.Bool

-- instance EquivalenceNat : Equivalence Nat lzero
-- (EquivalenceNat Equivalence.≈ x) x₁ = (x == x₁) ≡ true
-- IsEquivalence.reflexivity (Equivalence.isEquivalence EquivalenceNat) = isrefl where
--   isrefl : ∀ x → (x == x) ≡ true
--   isrefl zero = refl
--   isrefl (suc x) = isrefl x
-- IsEquivalence.symmetry (Equivalence.isEquivalence EquivalenceNat) = issym where
--   issym : (x y : Nat) →
--             EquivalenceNat .Equivalence._≈_ x y →
--             EquivalenceNat .Equivalence._≈_ y x
--   issym zero zero x₁ = refl
--   issym zero (suc y) x₁ = x₁
--   issym (suc x) zero x₁ = x₁
--   issym (suc x) (suc y) x₁ = issym x y x₁
-- IsEquivalence.transitivity (Equivalence.isEquivalence EquivalenceNat) = {!!}

-- instance DecidableEquivalenceNat : DecidableEquivalence Nat lzero
-- DecisionModule.DecidableEquivalence.equivalence DecidableEquivalenceNat = EquivalenceNat
-- (DecidableEquivalenceNat DecisionModule.DecidableEquivalence.≈? zero) zero = yes refl
-- (DecidableEquivalenceNat DecisionModule.DecidableEquivalence.≈? zero) (suc y) = no (λ x → {!!})
-- (DecidableEquivalenceNat DecisionModule.DecidableEquivalence.≈? suc x) zero = {!!}
-- (DecidableEquivalenceNat DecisionModule.DecidableEquivalence.≈? suc x) (suc y) = {!!}

-- {-
-- $&[{}(=*)+]!#
-- ~%7531902468`
-- ;,.
-- :<>
-- -}


text:
{- Example by Guillaume Brunerie, 17-11-2015 -}

{-# OPTIONS --rewriting --cubical-compatible #-}

open import Agda.Primitive

postulate
  _↦_ : ∀ {i} {A : Set i} → A → A → Set i
  idr : ∀ {i} {A : Set i} {a : A} → a ↦ a
{-# BUILTIN REWRITE _↦_ #-}

infixr 3 _==_

data _==_ {i} {A : Set i} (a : A) : A → Set i where
  idp : a == a

PathOver : ∀ {i j} {A : Set i} (B : A → Set j)
  {x y : A} (p : x == y) (u : B x) (v : B y) → Set j
PathOver B idp u v = (u == v)

syntax PathOver B p u v =
  u == v [ B ↓ p ]

postulate
  PathOver-rewr : ∀ {i j} {A : Set i} {B : Set j} {x y : A} (p : x == y) (u v : B) →
    (PathOver (λ _ → B) p u v) ↦ (u == v)
  {-# REWRITE PathOver-rewr #-}

ap : ∀ {i j} {A : Set i} {B : A → Set j} (f : (a : A) → B a) {x y : A}
  → (p : x == y) → PathOver B p (f x) (f y)
ap f idp = idp

module _ {i j k} {A : Set i} {B : Set j} {C : Set k} (g : B → C) (f : A → B) where

  ∘ap : {x y : A} (p : x == y) →
    ap g (ap f p) ↦ ap (λ x → g (f x)) p
  ∘ap idp = idr
  {-# REWRITE ∘ap #-}

  ap∘ : {x y : A} (p : x == y) →
    ap (λ x → g (f x)) p ↦ ap g (ap f p)
  ap∘ p = idr


text:
-- Andreas, 2014-09-03
-- Test explanation of local shadowed by import.

module _ where

module M where

  A = Set1

test : (A : Set) → let open M in {!A!}
test A = Set

-- The A exported by M is in competition with the local A.
-- Ambiguous name should be reported.


text:
module Transducer where

open import Data.Unit
open import Data.Product
open import Data.Sum
open import Data.List

_* = List

-- | Finite and infinite sequences (constructively useful variant)
record Seq (A : Set) : Set where
  coinductive
  field
    out : (A ⊎ ⊤) × Seq A
open Seq

-- | Functor that allows us to capture transducer as coalgebras.
F : (A B : Set) → Set → Set
F A B X = A → B * × X

-- | Interpretation of transducers as maps between sequences, i.e., corecursion.
⟦_⟧ : ∀{A B X} → (δ : X → F A B X) → X → (Seq A → Seq B)
out (⟦_⟧ {B = B} {X} δ x s) with out s
... | (inj₁ a , t) =
  let (w , y) = δ x a
  in cont y w
  where
    cont : X → B * → (B ⊎ ⊤) × Seq B
    cont y [] = (inj₂ tt , ⟦ δ ⟧ y t)
    proj₁ (cont y (b ∷ bs)) = inj₁ b
    out (proj₂ (cont y (b ∷ bs))) = cont y bs
... | (inj₂ tt , y) = (inj₂ tt , ⟦ δ ⟧ x y)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

open import Cubical.Algebra.Module.Base public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------------
-- Test the consistency of FOTC.Base
------------------------------------------------------------------------------

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

-- In the module FOTC.Base we declare Agda postulates as first-order
-- logic axioms. We test if it is possible to prove an unprovable
-- theorem from these axioms.

module FOTC.Base.Consistency.Axioms where

open import FOTC.Base

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

postulate impossible : ∀ d e → d ≡ e
{-# ATP prove impossible #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Slice where

open import Logic.Relations
open import Logic.Equivalence
open import Logic.Base
open import Category

module SliceCat (ℂ : Cat)(Γ : Category.Obj ℂ) where

  open module CC = Category.Category ℂ

  record SlObj : Set1 where
    field
      dom : Obj
      arr : dom ─→ Γ

  record _Sl→_ (f f' : SlObj) : Set where
    field
      h : (SlObj.dom f) ─→ (SlObj.dom f')
      π : (SlObj.arr f') ∘ h == (SlObj.arr f)

  SlId : {f : SlObj} -> f Sl→ f
  SlId = record
    { h = id
    ; π = idRight
    }

  _o_ : {f f' f'' : SlObj} -> f' Sl→ f'' -> f Sl→ f' -> f Sl→ f''
  _o_ {F} {F'} {F''} F₁ F₂ =
    let f   = SlObj.arr F   in
    let f'  = SlObj.arr F'  in
    let f'' = SlObj.arr F'' in
    let h'  = _Sl→_.h F₁     in
    let h   = _Sl→_.h F₂     in
    record
      { h = (_Sl→_.h F₁) ∘ (_Sl→_.h F₂)
      -- Proof of f'' ∘ (h' ∘ h) == f
      ; π = trans (trans (sym assoc)
                         (congL (_Sl→_.π F₁)))
                  (_Sl→_.π F₂)
      }

  SlRel : {A B : SlObj} -> Rel (A Sl→ B)
  SlRel f f' = (_Sl→_.h f) == (_Sl→_.h f')

  SlRefl : {A B : SlObj} -> Reflexive {A Sl→ B} SlRel
  SlRefl = refl

  SlSym : {A B : SlObj} -> Symmetric {A Sl→ B} SlRel
  SlSym = sym

  SlTrans : {A B : SlObj} -> Transitive {A Sl→ B} SlRel
  SlTrans = trans

  SlEq : {A B : SlObj} -> Equivalence (A Sl→ B)
  SlEq {A} {B} = record
    { _==_  = SlRel {A} {B}
    ; refl  = \{f     : A Sl→ B} -> SlRefl  {A}{B}{f}
    ; sym   = \{f g   : A Sl→ B} -> SlSym   {A}{B}{f}{g}
    ; trans = \{f g h : A Sl→ B} -> SlTrans {A}{B}{f}{g}{h}
    }

  SlCong : {A B C : SlObj}{f f' : B Sl→ C}{g g' : A Sl→ B} ->
    SlRel f f' -> SlRel g g' -> SlRel (f o g) (f' o g')
  SlCong = cong

  SlIdLeft : {A B : SlObj}{f : A Sl→ B} -> SlRel (SlId o f) f
  SlIdLeft = idLeft

  SlIdRight : {A B : SlObj}{f : A Sl→ B} -> SlRel (f o SlId) f
  SlIdRight = idRight

  SlAssoc : {A B C D : SlObj}{f : C Sl→ D}{g : B Sl→ C}{h : A Sl→ B} ->
    SlRel ((f o g) o h) (f o (g o h))
  SlAssoc = assoc

  Slice : Cat
  Slice = record
    { Obj     = SlObj
    ; _─→_    = _Sl→_
    ; id      = SlId
    ; _∘_     = _o_
    ; Eq      = SlEq
    ; cong    = \{A B C : SlObj}{f f' : B Sl→ C}{g g' : A Sl→ B} -> SlCong {A}{B}{C}{f}{f'}{g}{g'}
    ; idLeft  = \{A B : SlObj}{f : A Sl→ B} -> SlIdLeft {A} {B} {f}
    ; idRight = \{A B : SlObj}{f : A Sl→ B} -> SlIdRight {A} {B} {f}
    ; assoc   = \{A B C D : SlObj}{f : C Sl→ D}{g : B Sl→ C}{h : A Sl→ B} ->
        SlAssoc {A}{B}{C}{D}{f}{g}{h}
    }

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Algebra.Structures.Bundles.Field where

open import Algebra
open import Level using (suc; _⊔_)
open import Relation.Binary using (Rel)

open import Algebra.Structures.Field

record Field c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Carrier -> Carrier -> Carrier
    _*_     : Carrier -> Carrier -> Carrier
    0#      : Carrier
    1#      : Carrier
    -_      : Carrier -> Carrier
    _⁻¹      : MultiplicativeInverse _≈_ 0#
    isField : IsField _≈_ _+_ _*_ 0# 1# -_ _⁻¹

  open IsField isField public

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Naturals
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Groups.Homomorphisms.Lemmas2 {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ : A → A → A} (G : Group S _+A_) where

imageGroup : {c d : _} {B : Set c} {T : Setoid {c} {d} B} {_+B_ : B → B → B} → (f : A → B) → SetoidSurjection S T f → ({x y : A} → Setoid._∼_ T (f (x +A y)) ((f x) +B (f y))) → ({x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x +B y) (m +B n)) → Group T _+B_
Group.+WellDefined (imageGroup f surj respects+ wd) {m} {n} {x} {y} = wd
Group.0G (imageGroup f surj respects+ wd) = f (Group.0G G)
Group.inverse (imageGroup f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) b with surjective {b}
Group.inverse (imageGroup f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) b | a , fa=b = f (Group.inverse G a)
Group.+Associative (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {a} {b} {c} with surjective {a}
... | x , fx=a with surjective {b}
... | y , fy=b with surjective {c}
... | z , fz=c = transitive (wd (symmetric fx=a) (transitive (wd (symmetric fy=b) (symmetric fz=c)) (symmetric respects+))) (transitive (transitive (symmetric respects+) (transitive (wellDefined (Group.+Associative G)) respects+)) (wd (transitive respects+ (wd fx=a fy=b)) fz=c))
  where
    open Setoid T
    open Equivalence eq
Group.identRight (imageGroup {T = T} f record { wellDefined = wd ; surjective = surjective } respects+ bWd) {b} with surjective {b}
... | a , fa=b = transitive (bWd (symmetric fa=b) reflexive) (transitive (symmetric respects+) (transitive (wd (Group.identRight G)) fa=b))
  where
    open Setoid T
    open Equivalence eq
Group.identLeft (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} with surjective {b}
... | a , fa=b = transitive (wd reflexive (symmetric fa=b)) (transitive (symmetric respects+) (transitive (wellDefined (Group.identLeft G)) fa=b))
  where
    open Setoid T
    open Equivalence eq
Group.invLeft (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} with surjective {b}
Group.invLeft (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} | a , fa=b = transitive (wd reflexive (symmetric fa=b)) (transitive (symmetric respects+) (wellDefined (Group.invLeft G)))
  where
    open Setoid T
    open Equivalence eq
Group.invRight (imageGroup f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} with surjective {b}
Group.invRight (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} | a , fa=b = transitive (wd (symmetric fa=b) reflexive) (transitive (symmetric respects+) (wellDefined (Group.invRight G)))
  where
    open Setoid T
    open Equivalence eq

homToImageGroup : {c d : _} {B : Set c} {T : Setoid {c} {d} B} {_+B_ : B → B → B} → (f : A → B) → (surj : SetoidSurjection S T f) → (respects+ : {x y : A} → Setoid._∼_ T (f (x +A y)) ((f x) +B (f y))) → (wd : {x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x +B y) (m +B n)) → GroupHom G (imageGroup f surj respects+ wd) f
GroupHom.groupHom (homToImageGroup f surj respects+ wd) = respects+
GroupHom.wellDefined (homToImageGroup f surj respects+ wd) = SetoidSurjection.wellDefined surj


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List using (List; []; _∷_; takeWhile; dropWhile)
open import Data.List.All using (All; []; _∷_)
open import Data.Bool using (Bool; true; false; T)
open import Data.Unit using (⊤; tt)
open import Relation.Nullary using (¬_)
open import Function using (_∘_)

module TakeDropBool (A : Set) (P : A → Bool) where

  Head : ∀ {A : Set} → (A → Bool) → List A → Set
  Head P []       =  ⊥
  Head P (c ∷ s)  =  T (P c)

  data Book (x : A) (b : Bool) : Set where
    book : P x ≡ b → Book x b

  boo : ∀ (x : A) → Book x (P x)
  boo x = book refl

  dropWhile-lemma : ∀ (s : List A) → ¬ Head P (dropWhile P s)
  dropWhile-lemma []                                         =  λ()
  dropWhile-lemma (c ∷ s) with P c    | boo c
  ...                        | true   | _                    =  dropWhile-lemma s
  ...                        | false  | book eq  rewrite eq  =  λ()

  takeWhile-lemma : ∀ (s : List A) → All (T ∘ P) (takeWhile P s)
  takeWhile-lemma []                                         =  []
  takeWhile-lemma (c ∷ s) with P c    | boo c
  ...                        | false  | _                    =  []
  ...                        | true   | book eq rewrite eq   =  {! tt!} ∷ takeWhile-lemma s

{-  Hole 0
Goal: T (P c)
————————————————————————————————————————————————————————————
s  : List A
eq : P c ≡ true
c  : A
P  : A → Bool
A  : Set
-}


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

open import HoTT
open import homotopy.DisjointlyPointedSet

module groups.DisjointlyPointedSet where

  diff-and-separate : ∀ {i j} {X : Ptd i} (G : Group j)
    → (de⊙ X → Group.El G) → Group.El G × (MinusPoint X → Group.El G)
  diff-and-separate {X = X} G f =
    f (pt X) , λ x- → Group.diff G (f (fst x-)) (f (pt X))

  shift-and-unite : ∀ {i j} {X : Ptd i} (G : Group j)
    → is-separable X
    → Group.El G × (MinusPoint X → Group.El G) → (de⊙ X → Group.El G)
  shift-and-unite {X = X} G X-sep p x with X-sep x
  ... | inl _ = fst p
  ... | inr pt≠x = Group.comp G (snd p (x , pt≠x)) (fst p)

  diff-and-separate-hom : ∀ {i j} {X : Ptd i} (G : AbGroup j)
    →  Πᴳ (de⊙ X) (λ _ → AbGroup.grp G)
    →ᴳ AbGroup.grp G ×ᴳ Πᴳ (MinusPoint X) (λ _ → AbGroup.grp G)
  diff-and-separate-hom {X = X} G = group-hom (diff-and-separate grp) lemma where
    open AbGroup G
    abstract
      lemma : preserves-comp
                (Group.comp (Πᴳ (de⊙ X) (λ _ → AbGroup.grp G)))
                (Group.comp (AbGroup.grp G ×ᴳ Πᴳ (MinusPoint X) (λ _ → AbGroup.grp G)))
                (diff-and-separate grp)
      lemma f₀ f₁ = pair×= idp
        (λ= λ x- → diff-comp (f₀ (fst x-)) (f₁ (fst x-)) (f₀ (pt X)) (f₁ (pt X)))

  diff-and-separate-is-equiv : ∀ {i j} {X : Ptd i} (G : Group j)
    → is-separable X → is-equiv (diff-and-separate {X = X} G)
  diff-and-separate-is-equiv {X = X} G X-sep = is-eq to from to-from (λ= ∘ from-to)
    where
      open Group G
      to = diff-and-separate {X = X} G
      from = shift-and-unite {X = X} G X-sep

      abstract
        fst-to-from : ∀ p → fst (to (from p)) == fst p
        fst-to-from _ with X-sep (pt X)
        ... | inl _ = idp
        ... | inr pt≠pt = ⊥-rec (pt≠pt idp)

        snd-to-from : ∀ p x → snd (to (from p)) x == snd p x
        snd-to-from p x with X-sep (fst x)
        ... | inl pt=x = ⊥-rec (snd x pt=x)
        ... | inr pt≠x with X-sep (pt X)
        ...   | inl _ = assoc (snd p (fst x , pt≠x)) (fst p) (inv (fst p))
                      ∙ ap (comp (snd p (fst x , pt≠x))) (inv-r (fst p))
                      ∙ unit-r (snd p (fst x , pt≠x))
                      ∙ ap (λ neq → snd p (fst x , neq)) (prop-has-all-paths _ _)
        ...   | inr pt≠pt = ⊥-rec (pt≠pt idp)

        to-from : ∀ p → to (from p) == p
        to-from p = pair×= (fst-to-from p) (λ= (snd-to-from p))

        from-to : ∀ f x → from (to f) x == f x
        from-to f x with X-sep x
        ... | inl idp = idp
        ... | inr _ = assoc (f x) (inv (f (pt X))) (f (pt X))
                    ∙ ap (comp (f x)) (inv-l (f (pt X)))
                    ∙ unit-r (f x)

  diff-and-separate-iso : ∀ {i j} {X : Ptd i} (G : AbGroup j)
    → is-separable X
    →  Πᴳ (de⊙ X) (λ _ → AbGroup.grp G)
    ≃ᴳ AbGroup.grp G ×ᴳ Πᴳ (MinusPoint X) (λ _ → AbGroup.grp G)
  diff-and-separate-iso G X-sep =
    diff-and-separate-hom G , diff-and-separate-is-equiv (AbGroup.grp G) X-sep

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- See also test/Succeed/InlineCompiled.agda
module _ where

id : {A : Set} → A → A
id x = x
{-# INLINE id #-}

-- this is pointless and should generate a warning in the info buffer
{-# COMPILE GHC id = \ _ x -> x #-}


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

open import lib.Basics
open import lib.NConnected
open import lib.types.TLevel
open import lib.NType2
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Pointed
open import lib.types.LoopSpace
open import lib.types.Truncation
open import lib.types.PathSet

module lib.types.Cover where

{-
  The definition of covering spaces.
-}
record Cover {i} (A : Type i) j : Type (lmax i (lsucc j)) where
  constructor cover
  field
    Fiber : A → Type j
    Fiber-level : ∀ a → is-set (Fiber a)
  Fiber-is-set = Fiber-level
  TotalSpace = Σ A Fiber

-- Basic lemmas
module _ {i} {A : Type i} {j} where

  open Cover

  -- Equality between covers.
  private
    cover=′ : {c₁ c₂ : Cover A j} → Fiber c₁ == Fiber c₂ → c₁ == c₂
    cover=′ {cover f _} {cover .f _} idp = ap (cover f) $
      prop-has-all-paths (Π-is-prop λ _ → is-set-is-prop) _ _

  cover= : {c₁ c₂ : Cover A j} → (∀ a → Fiber c₁ a ≃ Fiber c₂ a)
    → c₁ == c₂
  cover= F≃ = cover=′ (λ= λ a → ua $ F≃ a)

  -- The definition of universality in terms of connectedness.
  is-universal : Cover A j → Type (lmax i j)
  is-universal cov = is-connected 1 $ TotalSpace cov

  -- In terms of connectedness
  UniversalCover : Type (lmax i (lsucc j))
  UniversalCover = Σ (Cover A j) is-universal

-- Theorem: A covering space keeps higher homotopy groups.
module _ {i} (A∙ : Ptd i)
  {j} (c : Cover (fst A∙) j)
  (a↑ : Cover.Fiber c (snd A∙)) where

  open Cover c
  private
    F = Cover.Fiber c
    F-level = Cover.Fiber-level c
    A = fst A∙
    a = snd A∙

  private
    -- The projection map with one end free (in order to apply J).
    to′ : ∀ {p⇑ : _==_ {A = Σ A F} (a , a↑) (a , a↑)}
        → idp == p⇑ → idp == fst= p⇑
    to′ idp=p⇑ = ap fst= idp=p⇑

    -- The projection map from Ω²(Σ A F) to Ω²(A).
    to : Ω^ 2 ⊙[ Σ A F , (a , a↑) ] → Ω^ 2 A∙
    to p²⇑ = to′ {p⇑ = idp} p²⇑

    -- Auxiliary synthesized path for injection.
    idp=p↑ : ∀ {p : a == a} {p↑ : a↑ == a↑ [ F ↓ p ]}
             → (idp=p : idp == p)
             → idp == p↑
               [ (λ p → a↑ == a↑ [ F ↓ p ]) ↓ idp=p ]
    idp=p↑ idp = prop-has-all-paths (F-level a _ _) _ _

    -- The injection map with some ends free (in order to apply J).
    from′ : ∀ {p : a == a} {p↑ : a↑ == a↑ [ F ↓ p ]}
            → (idp=p : idp == p)
            → idp == p↑ -- aux
              [ (λ p → a↑ == a↑ [ F ↓ p ]) ↓ idp=p ]
            → idp == pair= p p↑
    from′ idp=p idp=p↑ = pair== idp=p idp=p↑

    -- The injection map from Ω²(A) to Ω²(Σ A F).
    from : Ω^ 2 A∙ → Ω^ 2 ⊙[ Σ A F , (a , a↑) ]
    from p² = from′ {p = idp} {p↑ = idp} p² (idp=p↑ p²)

    -- Injection is left-inverse to projection (with some ends free).
    from′-to′ : ∀ {p⇑ : _==_ {A = Σ A F} (a , a↑) (a , a↑)}
                → (idp=p⇑ : idp == p⇑)
                → (idp=snd=p⇑ : idp == snd= p⇑ -- aux
                  [ (λ p → a↑ == a↑ [ F ↓ p ]) ↓ to′ idp=p⇑ ])
                → from′ (to′ idp=p⇑) idp=snd=p⇑ == idp=p⇑
                  [ (λ p⇑ → idp == p⇑) ↓ ! (pair=-η p⇑) ]
    from′-to′ idp idp=snd=p⇑ = ap (from′ idp)
      $ contr-has-all-paths (F-level a _ _ _ _) _ _

    -- Injection is left-inverse to projection.
    from-to : ∀ p²⇑ → from (to p²⇑) == p²⇑
    from-to p²⇑ = from′-to′ {p⇑ = idp} p²⇑ (idp=p↑ (to′ p²⇑))

    -- Injection is right-inverse to projection (with some ends free).
    to′-from′ : ∀ {p : a == a} {p↑ : a↑ == a↑ [ F ↓ p ]}
                → (idp=p : idp == p)
                → (idp=p↑ : idp == p↑ -- aux
                  [ (λ p → a↑ == a↑ [ F ↓ p ]) ↓ idp=p ])
                → to′ (from′ idp=p idp=p↑) == idp=p
                  [ (λ p → idp == p) ↓ fst=-β p p↑ ]
    to′-from′ idp idp = idp

    -- Injection is right-inverse to projection.
    to-from : ∀ p² → to (from p²) == p²
    to-from p² = to′-from′ p² (idp=p↑ p²)

  -- The theorem.
  Ω²ΣAFiber≃Ω²A : Ω^ 2 (Σ A F , (a , a↑)) ≃ Ω^ 2 A∙
  Ω²ΣAFiber≃Ω²A = to , is-eq to from to-from from-to

-- A natural way to construct a G-set from covering spaces.
module _ {i} {A : Type i} where
  open Cover

  cover-trace : ∀ {j} (cov : Cover A j) {a₁ a₂}
    → Fiber cov a₁ → a₁ =₀ a₂
    → Fiber cov a₂
  cover-trace cov a↑ p =
    transport₀ (Fiber cov) (Fiber-is-set cov _) p a↑

  abstract
    cover-trace-idp₀ : ∀ {j} (cov : Cover A j) {a₁}
      → (a↑ : Fiber cov a₁)
      → cover-trace cov a↑ idp₀ == a↑
    cover-trace-idp₀ cov a↑ = idp

    cover-paste : ∀ {j} (cov : Cover A j) {a₁ a₂}
      → (a↑ : Fiber cov a₁)
      → (loop : a₁ =₀ a₁)
      → (p : a₁ =₀ a₂)
      → cover-trace cov (cover-trace cov a↑ loop) p
      == cover-trace cov a↑ (loop ∙₀ p)
    cover-paste cov a↑ loop p = ! $ trans₀-∙₀ (Fiber-is-set cov) loop p a↑

-- Path sets form a covering space
module _ {i} (A∙ : Ptd i) where
  path-set-cover : Cover (fst A∙) i
  path-set-cover = record
    { Fiber = λ a → snd A∙ =₀ a
    ; Fiber-level = λ a → Trunc-level
    }

-- Cover morphisms
CoverHom : ∀ {i} {A : Type i} {j₁ j₂}
  → (cov1 : Cover A j₁)
  → (cov2 : Cover A j₂)
  → Type (lmax i (lmax j₁ j₂))
CoverHom (cover F₁ _) (cover F₂ _) = ∀ a → F₁ a → F₂ a

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

open import Cubical.Algebra.Semilattice.Base public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bijections
------------------------------------------------------------------------

module Function.Bijection where

open import Data.Product
open import Level
open import Relation.Binary
open import Function.Equality as F
  using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
open import Function.Injection   as Inj  hiding (id; _∘_)
open import Function.Surjection  as Surj hiding (id; _∘_)
open import Function.LeftInverse as Left hiding (id; _∘_)

-- Bijective functions.

record Bijective {f₁ f₂ t₁ t₂}
                 {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
                 (to : From ⟶ To) :
                 Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    injective  : Injective  to
    surjective : Surjective to

  open Surjective surjective public

  left-inverse-of : from LeftInverseOf to
  left-inverse-of x = injective (right-inverse-of (to ⟨$⟩ x))

-- The set of all bijections between two setoids.

record Bijection {f₁ f₂ t₁ t₂}
                 (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
                 Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    to        : From ⟶ To
    bijective : Bijective to

  open Bijective bijective public

  injection : Injection From To
  injection = record
    { to        = to
    ; injective = injective
    }

  surjection : Surjection From To
  surjection = record
    { to         = to
    ; surjective = surjective
    }

  open Surjection surjection public
    using (equivalence; right-inverse; from-to)

  left-inverse : LeftInverse From To
  left-inverse = record
    { to              = to
    ; from            = from
    ; left-inverse-of = left-inverse-of
    }

  open LeftInverse left-inverse public using (to-from)

-- Identity and composition. (Note that these proofs are superfluous,
-- given that Bijection is equivalent to Function.Inverse.Inverse.)

id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → Bijection S S
id {S = S} = record
  { to        = F.id
  ; bijective = record
    { injective  =  Injection.injective   (Inj.id {S = S})
    ; surjective = Surjection.surjective (Surj.id {S = S})
    }
  }

infixr 9 _∘_

_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
        {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
      Bijection M T → Bijection F M → Bijection F T
f ∘ g = record
  { to        = to f ⟪∘⟫ to g
  ; bijective = record
    { injective  =  Injection.injective   (Inj._∘_  (injection f)  (injection g))
    ; surjective = Surjection.surjective (Surj._∘_ (surjection f) (surjection g))
    }
  } where open Bijection


text:
------------------------------------------------------------------------------
-- From inductive PA to Mendelson's axioms
------------------------------------------------------------------------------

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

-- From the definition of PA using Agda data types and primitive
-- recursive functions for addition and multiplication, we can prove the
-- Mendelson's axioms [1].

-- N.B. We make the recursion in the first argument for _+_ and _*_.

-- S₁. m = n → m = o → n = o
-- S₂. m = n → succ m = succ n
-- S₃. 0 ≠ succ n
-- S₄. succ m = succ n → m = n
-- S₅. 0 + n = n
-- S₆. succ m + n = succ (m + n)
-- S₇. 0 * n = 0
-- S₈. succ m * n = (m * n) + m
-- S₉. P(0) → (∀n.P(n) → P(succ n)) → ∀n.P(n), for any wf P(n) of PA.

-- [1]. Elliott Mendelson. Introduction to mathematical
--      logic. Chapman& Hall, 4th edition, 1997, p. 155.

module PA.Inductive2Mendelson where

open import PA.Inductive.Base

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

S₁ :  ∀ {m n o} → m ≡ n → m ≡ o → n ≡ o
S₁ refl refl = refl

S₂ : ∀ {m n} → m ≡ n → succ m ≡ succ n
S₂ refl = refl

S₃ : ∀ {n} → zero ≢ succ n
S₃ ()

S₄ : ∀ {m n} → succ m ≡ succ n → m ≡ n
S₄ refl = refl

S₅ : ∀ n → zero + n ≡ n
S₅ n = refl

S₆ : ∀ m n → succ m + n ≡ succ (m + n)
S₆ m n = refl

S₇ : ∀ n → zero * n ≡ zero
S₇ n = refl

S₈ : ∀ m n → succ m * n ≡ n + m * n
S₈ m n = refl

S₉ : (A : ℕ → Set) → A zero → (∀ n → A n → A (succ n)) → ∀ n → A n
S₉ = ℕ-ind


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

module Data.Binary.Operations.Addition where

open import Data.Binary.Definitions
open import Data.Binary.Operations.Unary

add : Bit → 𝔹⁺ → 𝔹⁺ → 𝔹⁺
add c (x ∷ xs) (y ∷ ys) = sumᵇ c x y ∷ add (carryᵇ c x y) xs ys
add O 1ᵇ ys = inc⁺⁺ ys
add O (O ∷ xs) 1ᵇ = I ∷ xs
add O (I ∷ xs) 1ᵇ = O ∷ inc⁺⁺ xs
add I 1ᵇ 1ᵇ = I ∷ 1ᵇ
add I 1ᵇ (y ∷ ys) = y ∷ inc⁺⁺ ys
add I (x ∷ xs) 1ᵇ = x ∷ inc⁺⁺ xs

_+_ : 𝔹 → 𝔹 → 𝔹
0ᵇ + ys = ys
(0< xs) + 0ᵇ = 0< xs
(0< xs) + (0< ys) = 0< add O xs ys

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
module SortDependingOnIndex where

open import Common.Level

data Bad : (l : Level) → Set l where