text:
open import LibraBFT.Impl.Consensus.MetricsSafetyRules
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Prelude                                   hiding (_++_)

module LibraBFT.Impl.Consensus.Properties.MetricsSafetyRules where

open Invariants

module performInitializeSpec
  (safetyRules : SafetyRules)
  (storage     : PersistentLivenessStorage)
  where

  record ContractOk (sr : SafetyRules) : Set where
    constructor mkContractOk
    field
      srPres    : Preserves SafetyRulesInv safetyRules sr
      lvNothing : sr ^∙ srPersistentStorage ∙ pssSafetyData ∙ sdLastVote ≡ nothing
  open ContractOk

  Contract : EitherD-Post ErrLog SafetyRules
  Contract (Left _)   = ⊤
  Contract (Right sr) = ContractOk sr

  module _ (sri : SafetyRulesInv safetyRules)
           (lvNothing : safetyRules ^∙ srPersistentStorage ∙ pssSafetyData ∙ sdLastVote ≡ nothing)
    where
    -- TODO-2: Requires refinement
    postulate
     contract' : EitherD-weakestPre (performInitialize-ed-abs safetyRules storage) Contract

    contract : Contract (performInitialize-abs safetyRules storage)
    contract rewrite performInitialize-abs-≡ safetyRules storage =
      EitherD-contract (performInitialize-ed-abs safetyRules storage) Contract contract'


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

module Fragment.Prelude where

open import Fragment.Tactic.Fragment using (fragment) public

open import Fragment.Equational.Theory.Bundles public
open import Fragment.Equational.Structures public

open import Fragment.Extensions.Semigroup using (SemigroupFrex) public
open import Fragment.Extensions.CSemigroup using (CSemigroupFrex) public

ext: agda

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module Cats.Category.Arrow where

open import Level
open import Relation.Binary using (IsEquivalence ; _Preserves₂_⟶_⟶_)

open import Cats.Category

module _ {lo la l≈} (C : Category lo la l≈) where

  infixr 9 _∘_
  infixr 4 _≈_

  private
    module C = Category C
    module ≈ = C.≈

  record Obj : Set (lo ⊔ la) where
    field
      Dom : C.Obj
      Cod : C.Obj
      arr : Dom C.⇒ Cod

  open Obj

  record _⇒_ (f g : Obj) : Set (la ⊔ l≈) where
    field
      dom : Dom f C.⇒ Dom g
      cod : Cod f C.⇒ Cod g
      commute : arr g C.∘ dom C.≈ cod C.∘ arr f

  open _⇒_

  record _≈_ {A B} (F G : A ⇒ B) : Set l≈ where
    field
      dom : dom F C.≈ dom G
      cod : cod F C.≈ cod G

  id : ∀ {A} → A ⇒ A
  id {record { Dom = Dom ; Cod = Cod ; arr = arr }}
      = record
      { dom = C.id
      ; cod = C.id
      ; commute = ≈.trans C.id-r (≈.sym C.id-l)
      }

  _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)
  _∘_ {F} {G} {H}
    record { dom = F-dom ; cod = F-cod ; commute = F-commute }
    record { dom = G-dom ; cod = G-cod ; commute = G-commute }
      = record
      { dom = F-dom C.∘ G-dom
      ; cod = F-cod C.∘ G-cod
      ; commute
          = begin
              arr H C.∘ F-dom C.∘ G-dom
            ≈⟨ C.unassoc ⟩
              (arr H C.∘ F-dom) C.∘ G-dom
            ≈⟨ C.∘-resp-l F-commute ⟩
              (F-cod C.∘ arr G) C.∘ G-dom
            ≈⟨ C.assoc ⟩
              F-cod C.∘ arr G C.∘ G-dom
            ≈⟨ C.∘-resp-r G-commute ⟩
              F-cod C.∘ G-cod C.∘ arr F
            ≈⟨ C.unassoc ⟩
              (F-cod C.∘ G-cod) C.∘ arr F
            ∎
      }
    where
      open C.≈-Reasoning

  equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
  equiv = record
      { refl = record { dom = ≈.refl ; cod = ≈.refl }
      ; sym = λ where
          record { dom = dom ; cod = cod } → record
            { dom = ≈.sym dom
            ; cod = ≈.sym cod
            }
      ; trans = λ where
          record { dom = dom₁ ; cod = cod₁ } record { dom = dom₂ ; cod = cod₂ }
            → record
            { dom = ≈.trans dom₁ dom₂
            ; cod = ≈.trans cod₁ cod₂
            }
      }

  ∘-resp : ∀ {A B C} → (_∘_ {A} {B} {C}) Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
  ∘-resp
    record { dom = dom-FG ; cod = cod-FG }
    record { dom = dom-HI ; cod = cod-HI }
      = record
      { dom = C.∘-resp dom-FG dom-HI
      ; cod = C.∘-resp cod-FG cod-HI
      }

  id-r : ∀ {A B} {F : A ⇒ B} → F ∘ id ≈ F
  id-r = record
      { dom = C.id-r
      ; cod = C.id-r
      }

  id-l : ∀ {A B} {F : A ⇒ B} → id ∘ F ≈ F
  id-l = record
      { dom = C.id-l
      ; cod = C.id-l
      }

  assoc : ∀ {A B C D} {F : C ⇒ D} {G : B ⇒ C} {H : A ⇒ B}
    → (F ∘ G) ∘ H ≈ F ∘ (G ∘ H)
  assoc = record
      { dom = C.assoc
      ; cod = C.assoc
      }

  _⃗ : Category (la ⊔ lo) (l≈ ⊔ la) l≈
  _⃗ = record
      { Obj = Obj
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = _∘_
      ; equiv = equiv
      ; ∘-resp = ∘-resp
      ; id-r = id-r
      ; id-l = id-l
      ; assoc = assoc
      }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module _ where

open import Agda.Builtin.Nat

module M (n : Nat) where

  postulate A : Set

module M₁ (m : Nat) where

  open module Mm = M m

  -- bar : M.A (m + 1)
  -- bar = m  -- Nat !=< M.A (m + 1)

postulate
  n : Nat

foo : M.A n
foo = n -- Nat !=< M.A n

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Categories.Category using () renaming (Category to Setoid-Category)
open import Categories.Category.Monoidal

module Categories.Category.Construction.EnrichedFunctors
  {o ℓ e} {V : Setoid-Category o ℓ e} (M : Monoidal V) where

-- The (enriched) functor category for a given pair of V-enriched categories

open import Level
open import Data.Product using (_,_; uncurry′)

open import Categories.Enriched.Category M
open import Categories.Enriched.Functor M renaming (id to idF)
open import Categories.Enriched.NaturalTransformation M renaming (id to idNT)
open import Categories.Functor.Bifunctor using (Bifunctor)

open NaturalTransformation using (_[_])

EnrichedFunctors : ∀ {c d} (C : Category c) (D : Category d) →
                   Setoid-Category (ℓ ⊔ e ⊔ c ⊔ d) (ℓ ⊔ e ⊔ c) (e ⊔ c)
EnrichedFunctors C D = record
  { Obj = Functor C D
  ; _⇒_ = NaturalTransformation
  ; _≈_ = λ α β → ∀ {X} → α [ X ] ≈ β [ X ]
  ; id  = idNT
  ; _∘_ = _∘ᵥ_
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = record
    { refl  = Equiv.refl
    ; sym   = λ α≈β → Equiv.sym α≈β
    ; trans = λ α≈β β≈γ → Equiv.trans α≈β β≈γ
    }
  ; ∘-resp-≈ = λ α₁≈β₁ α₂≈β₂ → ∘-resp-≈ α₁≈β₁ α₂≈β₂
  }
  where open Underlying D

-- Horizontal composition of natural transformations (aka the Godement
-- product) induces a composition functor over functor categories.
--
-- Note that all the equational reasoning happens in the underlying
-- (ordinary) categories!

⊚ : ∀ {c d e} {C : Category c} {D : Category d} {E : Category e} →
    Bifunctor (EnrichedFunctors D E) (EnrichedFunctors C D) (EnrichedFunctors C E)
⊚ {_} {_} {_} {_} {D} {E} = record
  { F₀ = uncurry′ _∘F_
  ; F₁ = uncurry′ _∘ₕ_
  ; identity = λ{ {F , G} {X} →
    begin
      (F $₁ D.id) ∘ E.id   ≈⟨ identityʳ ⟩
      F $₁ D.id            ≈⟨ identity F ⟩
      E.id                 ∎ }
  ; homomorphism = λ{ {_ , F₂} {G₁ , G₂} {H₁ , _} {α₁ , α₂} {β₁ , β₂} {X} →
    begin
      H₁ $₁ (β₂ [ X ] D.∘ α₂ [ X ]) ∘ β₁ [ F₂ $₀ X ] ∘ α₁ [ F₂ $₀ X ]
    ≈⟨ homomorphism H₁ ⟩∘⟨refl ⟩
      (H₁ $₁ β₂ [ X ] ∘ H₁ $₁ α₂ [ X ]) ∘ β₁ [ F₂ $₀ X ] ∘ α₁ [ F₂ $₀ X ]
    ≈⟨ ⟺ assoc ○ ∘-resp-≈ˡ assoc ⟩
      (H₁ $₁ β₂ [ X ] ∘ (H₁ $₁ α₂ [ X ] ∘ β₁ [ F₂ $₀ X ])) ∘ α₁ [ F₂ $₀ X ]
    ≈˘⟨ (refl⟩∘⟨ commute β₁ (α₂ [ X ])) ⟩∘⟨refl ⟩
      (H₁ $₁ β₂ [ X ] ∘ (β₁ [ G₂ $₀ X ] ∘ G₁ $₁ α₂ [ X ])) ∘ α₁ [ F₂ $₀ X ]
    ≈˘⟨ ⟺ assoc ○ ∘-resp-≈ˡ assoc ⟩
      (H₁ $₁ β₂ [ X ] ∘ β₁ [ G₂ $₀ X ]) ∘ G₁ $₁ α₂ [ X ] ∘ α₁ [ F₂ $₀ X ]
    ∎ }
  ; F-resp-≈ = λ{ {_} {F , _} (eq₁ , eq₂) → ∘-resp-≈ (F-resp-≈ F eq₂) eq₁ }
  }
  where
    module D = Underlying D
    module E = Underlying E
    open E hiding (id)
    open HomReasoning
    open UnderlyingFunctor hiding (F₀; F₁)
    open UnderlyingNT

    -- Aliases used to shorten some proof expressions

    infixr 14 _$₀_ _$₁_
    _$₀_ = UnderlyingFunctor.F₀
    _$₁_ = UnderlyingFunctor.F₁

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module RandomAccessList.General.Core where

open import Data.List
open import Data.Nat
open import Data.Vec
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_)

data General (A : Set) : ℕ → ℕ → ℕ → Set where
    [] : ∀ {a b n} → General A a b n
    ∺ : ∀ {v a a' b b' n}
        → Vec A v
        → a ⊓ v ≡ a'
        → b ⊔ b ≡ b'
        → General A a b n
        → General A a' b' n

--------------------------------------------------------------------------------
--  Beispiele
--------------------------------------------------------------------------------

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Theorems of ∨ connective.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Theorems.Disjunction ( n : ℕ ) where

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

open import Data.PropFormula.Syntax n
open import Data.PropFormula.Theorems.Classical n
open import Data.PropFormula.Properties n

open import Data.PropFormula.Theorems.Conjunction n using ( ∧-dmorgan₁ )
open import Data.PropFormula.Theorems.Implication n using ( vanDalen244e )

open import Function using ( _$_; _∘_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ )

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

-- Theorem.
∨-assoc₁
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ∨ (ψ ∨ γ)
  → Γ ⊢ (φ ∨ ψ) ∨ γ

-- Proof.
∨-assoc₁ {Γ}{φ}{ψ}{γ} =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₁ γ
          (∨-intro₁ ψ
            (assume φ)))
        (⊃-elim
          (⊃-intro
            (∨-elim {Γ = Γ , ψ ∨ γ}
              (∨-intro₁ γ
                (∨-intro₂ φ (assume {Γ = Γ , ψ ∨ γ} ψ)))
              (∨-intro₂ (φ ∨ ψ) (assume {Γ = Γ , ψ ∨ γ} γ))))
          (assume (ψ ∨ γ)))))
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-assoc₂
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ∨ ψ) ∨ γ
  → Γ ⊢ φ ∨ (ψ ∨ γ)

-- Proof.
∨-assoc₂ {Γ}{φ}{ψ}{γ} =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (⊃-elim
          (⊃-intro
            (∨-elim {Γ  = Γ , φ ∨ ψ}
              (∨-intro₁ (ψ ∨ γ)
                (assume {Γ = Γ , φ ∨ ψ} φ))
              (∨-intro₂ φ
                (∨-intro₁ γ
                  (assume {Γ = Γ , φ ∨ ψ} ψ)))))
          (assume (φ ∨ ψ)))
        (∨-intro₂ φ
          (∨-intro₂ ψ
            (assume γ)))))
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-assoc
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ∨ (ψ ∨ γ)) ⇔ ((φ ∨ ψ) ∨ γ)

-- Proof.
∨-assoc {φ = φ}{ψ}{γ} =
  ⇔-intro
    (∨-assoc₁ (assume (φ ∨ (ψ ∨ γ))))
    (∨-assoc₂ (assume (φ ∨ ψ ∨ γ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-comm
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ∨ ψ
  → Γ ⊢ ψ ∨ φ

-- Proof.
∨-comm {φ = φ}{ψ} =
  ⊃-elim $
    ⊃-intro
      (∨-elim
        (∨-intro₂ ψ
          (assume φ))
        (∨-intro₁ φ $
           assume ψ))
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-dist₁
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ∨ (ψ ∧ γ)
  → Γ ⊢ (φ ∨ ψ) ∧ (φ ∨ γ)

-- Proof.
∨-dist₁ {Γ}{φ}{ψ}{γ} =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∧-intro
          (∨-intro₁ ψ
            (assume φ))
          (∨-intro₁ γ
            (assume φ)))
        (∧-intro
          (∨-intro₂ φ
            (∧-proj₁
              (assume (ψ ∧ γ))))
          (∨-intro₂ φ
            (∧-proj₂
              (assume (ψ ∧ γ)))))))
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-dist₂
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ∨ ψ) ∧ (φ ∨ γ)
  → Γ ⊢ φ ∨ (ψ ∧ γ)

-- Proof.
∨-dist₂ {Γ}{φ}{ψ}{γ} Γ⊢⟪φ∨ψ⟫∧⟪φ∨γ⟫ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₁ (ψ ∧ γ)
          (assume φ))
        (⊃-elim
          (⊃-intro
            (∨-elim
              (∨-intro₁ (ψ ∧ γ)
                (assume {Γ = Γ , ψ} φ))
              (∨-intro₂ φ
                (∧-intro
                  (weaken γ
                    (assume ψ))
                  (assume {Γ = Γ , ψ} γ)))))
          (∧-proj₂
            (weaken ψ Γ⊢⟪φ∨ψ⟫∧⟪φ∨γ⟫)))))
    (∧-proj₁ Γ⊢⟪φ∨ψ⟫∧⟪φ∨γ⟫)
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-dist
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ∨ (ψ ∧ γ)) ⇔ ((φ ∨ ψ) ∧ (φ ∨ γ))

-- Proof.
∨-dist {φ = φ}{ψ}{γ} =
  ⇔-intro
    (∨-dist₁ (assume (φ ∨ (ψ ∧ γ))))
    (∨-dist₂ (assume (φ ∨ ψ ∧ (φ ∨ γ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-equiv
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ∨ ψ
  → Γ ⊢ ¬ (¬ φ ∧ ¬ ψ)
∨-to-¬¬∧¬ = ∨-equiv

-- Proof.
∨-equiv {Γ}{φ}{ψ} Γ⊢φ∨ψ =
  ¬-intro
    (⊃-elim
      (⊃-intro
        (∨-elim {Γ = Γ , ¬ φ ∧ ¬ ψ}
          (¬-elim
            (weaken φ
              (∧-proj₁
                (assume (¬ φ ∧ ¬ ψ))))
            (assume {Γ = Γ , ¬ φ ∧ ¬ ψ }  φ))
          (¬-elim
            (weaken ψ
              (∧-proj₂
                (assume (¬ φ ∧ ¬ ψ))))
            (assume {Γ = Γ , ¬ φ ∧ ¬ ψ}  ψ))))
      (weaken (¬ φ ∧ ¬ ψ) Γ⊢φ∨ψ))
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-dmorgan₁
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ (φ ∨ ψ)
  → Γ ⊢ ¬ φ ∧ ¬ ψ
¬∨-to-¬∧¬ = ∨-dmorgan₁

-- Proof.
∨-dmorgan₁ {Γ}{φ}{ψ} =
  ⊃-elim $
    ⊃-intro $
      ∧-intro
        (¬-intro $
          ¬-elim
            (weaken φ $
              assume (¬ (φ ∨ ψ)))
            (∨-intro₁ ψ $
              assume {Γ = Γ , ¬ (φ ∨ ψ)} φ))
        (¬-intro $
          ¬-elim
            (weaken ψ $
              assume (¬ (φ ∨ ψ)))
            (∨-intro₂ φ $
              assume {Γ = Γ , ¬ (φ ∨ ψ)} ψ))
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-dmorgan₂
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ φ ∧ ¬ ψ
  → Γ ⊢ ¬ (φ ∨ ψ)
¬∧¬-to-¬∨ = ∨-dmorgan₂

-- Proof.
∨-dmorgan₂ {φ = φ}{ψ} Γ⊢¬φ∧¬ψ  =
  ¬-intro
    (∨-elim
      (¬-elim
        (weaken φ
          (∧-proj₁ Γ⊢¬φ∧¬ψ ))
        (assume φ))
      (¬-elim
        (weaken ψ
          (∧-proj₂ Γ⊢¬φ∧¬ψ ))
        (assume ψ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-dmorgan
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ (φ ∨ ψ) ⇔ (¬ φ ∧ ¬ ψ)
¬∨-⇔-¬∧¬ = ∨-dmorgan

-- Proof.
∨-dmorgan {φ = φ}{ψ} =
  ⇔-intro
    (∨-dmorgan₁
      (assume (¬ (φ ∨ ψ))))
    (∨-dmorgan₂
      (assume (¬ φ ∧ ¬ ψ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
lem1
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ ¬ φ ∨ ¬ ¬ ψ
  → Γ ⊢ φ ∨ ψ
¬¬∨¬¬-to-∨ = lem1

-- Proof.
lem1 {φ = φ}{ψ} =
  ⊃-elim $
    ⊃-intro $
      ∨-elim
        (∨-intro₁ ψ $
          ⊃-elim vanDalen244e $ assume $ ¬ ¬ φ)
        (∨-intro₂ φ $
          ⊃-elim vanDalen244e $ assume $ ¬ ¬ ψ)
-------------------------------------------------------------------------- ∎

-- Theorem.
lem2
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ (φ ∨ ψ) ∧ ¬ ψ
  → Γ ⊢ φ

-- Proof.
lem2 {φ = φ}{ψ} Γ⊢⟪φ∨ψ⟫∧¬ψ =
  ⊃-elim
    (⊃-intro $
      (∨-elim
        (assume φ)
        (⊥-elim φ
          (¬-elim
            (weaken ψ (∧-proj₂ Γ⊢⟪φ∨ψ⟫∧¬ψ))
            (assume ψ)))))
    (∧-proj₁ Γ⊢⟪φ∨ψ⟫∧¬ψ)
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₀
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ∨ ψ → Γ ⊢ ¬ φ ∨ γ
  → Γ ⊢ ψ ∨ γ

-- Proof.
resolve₀ {Γ}{φ}{ψ}{γ} Γ⊢φ∨ψ Γ⊢¬φ∨γ =
 lem1 $
   ∧-dmorgan₁ $
     ¬-intro $
       ¬-elim
         (lem2 {Γ = Γ , ¬ ψ ∧ ¬ γ} $
           ∧-intro
             (weaken (¬ ψ ∧ ¬ γ) Γ⊢¬φ∨γ)
             (∧-proj₂ $ assume $ ¬ ψ ∧ ¬ γ))
         (lem2 $
           ∧-intro
             (weaken (¬ ψ ∧ ¬ γ) Γ⊢φ∨ψ)
             (∧-proj₁ $ assume $ ¬ ψ ∧ ¬ γ))
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₁
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ ψ ∨ φ → Γ ⊢ ¬ φ ∨ γ
  → Γ ⊢ ψ ∨ γ

-- Proof.
resolve₁ = resolve₀ ∘ ∨-comm
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₂
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ∨ ψ → Γ ⊢ γ ∨ ¬ φ
  → Γ ⊢ ψ ∨ γ

-- Proof.
resolve₂ Γ⊢φ∨ψ Γ⊢γ∨¬φ = resolve₀ Γ⊢φ∨ψ (∨-comm Γ⊢γ∨¬φ)
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₃
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ ψ ∨ φ → Γ ⊢ γ ∨ ¬ φ
  → Γ ⊢ ψ ∨ γ

-- Proof.
resolve₃ Γ⊢ψ∨φ Γ⊢γ∨¬φ = resolve₀ (∨-comm Γ⊢ψ∨φ) (∨-comm Γ⊢γ∨¬φ)
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₄
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ φ ∨ ψ → Γ ⊢ φ
  → Γ ⊢ ψ

-- Proof.
resolve₄ {φ = φ}{ψ} Γ⊢¬φ∨ψ Γ⊢φ =
 ⊃-elim
   (⊃-intro $
     ∨-elim
       (assume ψ)
       (assume ψ))
   (resolve₀
     (∨-intro₁ ψ Γ⊢φ)
     Γ⊢¬φ∨ψ)
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₅
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ψ ∨ ¬ φ
  → Γ ⊢ φ
  → Γ ⊢ ψ

-- Proof.
resolve₅ = resolve₄ ∘ ∨-comm
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₆
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ψ ∨ φ → Γ ⊢ ¬ φ
  → Γ ⊢ ψ

-- Proof.
resolve₆ {φ = φ}{ψ} Γ⊢ψ∨φ Γ⊢¬φ =
 ⊃-elim
   (⊃-intro $
     ∨-elim
       (assume ψ)
       (assume ψ))
   (resolve₀ (∨-comm Γ⊢ψ∨φ) (∨-intro₁ ψ Γ⊢¬φ))
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₇
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ∨ ψ → Γ ⊢ ¬ φ
  → Γ ⊢ ψ

-- Proof.
resolve₇ Γ⊢φ∨ψ Γ⊢¬φ = resolve₆ (∨-comm Γ⊢φ∨ψ) Γ⊢¬φ
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₈
  : ∀ {Γ} {φ}
  → Γ ⊢ φ → Γ ⊢ ¬ φ
  → Γ ⊢ ⊥

-- Proof.
resolve₈ Γ⊢φ Γ⊢¬φ = ¬-elim Γ⊢¬φ Γ⊢φ
-------------------------------------------------------------------------- ∎

-- Theorem.
resolve₉
  : ∀ {Γ} {φ}
  → Γ ⊢ ¬ φ → Γ ⊢ φ
  → Γ ⊢ ⊥

-- Proof.
resolve₉ = ¬-elim
-------------------------------------------------------------------------- ∎

-- Theorem.
subst⊢∨₁
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ⊃ γ
  → Γ ⊢ φ ∨ ψ
  → Γ ⊢ γ ∨ ψ

-- Proof.
subst⊢∨₁ {φ = φ}{ψ}{γ} Γ⊢φ⊃γ Γ⊢φ∨ψ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₁ ψ (⊃-elim (weaken φ Γ⊢φ⊃γ) (assume φ)))
        (∨-intro₂ γ (assume ψ))))
    Γ⊢φ∨ψ
-------------------------------------------------------------------------- ∎

-- Theorem.
subst⊢∨₂
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ ψ ⊃ γ
  → Γ ⊢ φ ∨ ψ
  → Γ ⊢ φ ∨ γ

-- Proof.
subst⊢∨₂ {φ = φ}{ψ}{γ} Γ⊢ψ⊃γ Γ⊢φ∨ψ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₁ γ (assume φ))
        (∨-intro₂ φ (⊃-elim (weaken ψ Γ⊢ψ⊃γ) (assume ψ)))))
    Γ⊢φ∨ψ
-------------------------------------------------------------------------- ∎

-- Theorem.
∨-to-¬⊃
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ∨ ψ
  → Γ ⊢ ¬ φ ⊃ ψ

-- Proof.
∨-to-¬⊃ {Γ}{φ}{ψ} Γ⊢φ∨ψ =
  ⊃-intro
    (⊃-elim
      (⊃-intro
        (∨-elim {Γ = Γ , ¬ φ}
          (⊥-elim ψ
            (¬-elim
              (weaken φ
                (assume (¬ φ)))
            (assume {Γ = Γ , ¬ φ} φ)))
          (assume {Γ = Γ , ¬ φ} ψ)))
      (weaken (¬ φ) Γ⊢φ∨ψ))
-------------------------------------------------------------------------- ∎

-- Theorem.
φ∨⊥-to-φ
 : ∀ {Γ} {φ}
 → Γ ⊢ φ ∨ ⊥
 → Γ ⊢ φ

-- Proof.
φ∨⊥-to-φ {φ = φ} Γ⊢φ∨⊥ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (assume φ)
        (⊥-elim φ (assume ⊥))))
    Γ⊢φ∨⊥
-------------------------------------------------------------------------- ∎

-- Theorem.
subst⊢∨₁≡
  : ∀ {Γ} {φ ψ γ}
  → φ ≡ γ
  → Γ ⊢ φ ∨ ψ
  → Γ ⊢ γ ∨ ψ

-- Proof.
subst⊢∨₁≡ {φ = φ}{ψ}{γ} φ≡γ Γ⊢φ∨ψ =
  ⊃-elim
    (⊃-intro
      (∨-elim
         (∨-intro₁ ψ (subst φ≡γ (assume φ)))
        (∨-intro₂ γ (assume ψ))))
    Γ⊢φ∨ψ
-------------------------------------------------------------------------- ∎

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


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

open import HoTT

module homotopy.elims.Lemmas where

fill-upper-right : ∀ {i j} {A : Type i} {B : A → Type j}
  {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ b₁₀' : B a₁₀} {b₁₁ : B a₁₁}
  (q₀₋ : b₀₀ == b₀₁ [ B ↓ p₀₋ ]) (q₋₀ : b₀₀ == b₁₀ [ B ↓ p₋₀ ])
  (q₋₁ : b₀₁ == b₁₁ [ B ↓ p₋₁ ]) (q₁₋ : b₁₀' == b₁₁ [ B ↓ p₁₋ ])
  → Σ (b₁₀ == b₁₀')
      (λ r → SquareOver B sq q₀₋ q₋₀ q₋₁ (r ◃ q₁₋))
fill-upper-right ids idp idp idp idp = (idp , ids)

fill-upper-right-unique : ∀ {i j} {A : Type i} {B : A → Type j}
  {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ b₁₀' : B a₁₀} {b₁₁ : B a₁₁}
  (q₀₋ : b₀₀ == b₀₁ [ B ↓ p₀₋ ]) (q₋₀ : b₀₀ == b₁₀ [ B ↓ p₋₀ ])
  (q₋₁ : b₀₁ == b₁₁ [ B ↓ p₋₁ ]) (q₁₋ : b₁₀' == b₁₁ [ B ↓ p₁₋ ])
  (r : b₁₀ == b₁₀')
  → SquareOver B sq q₀₋ q₋₀ q₋₁ (r ◃ q₁₋)
  → r == fst (fill-upper-right sq q₀₋ q₋₀ q₋₁ q₁₋)
fill-upper-right-unique {B = B} ids idp idp idp idp r sq' =
  ! (◃idp {B = B} r) ∙ ! (horiz-degen-path sq')

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
open import Common.Equality
open import Common.Prelude

NaN : Float
NaN = primFloatDiv 0.0 0.0

NaN≢-NaN : primFloatEquality NaN (primFloatNegate NaN) ≡ true
NaN≢-NaN = refl

NaN≢N-NaN : primFloatNumericalEquality NaN (primFloatNegate NaN) ≡ false
NaN≢N-NaN = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Category.Base where

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

private
  variable
    ℓ ℓ' : Level

-- Categories with hom-sets
record Category ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  -- no-eta-equality ; NOTE: need eta equality for `opop`
  field
    ob : Type ℓ
    Hom[_,_] : ob → ob → Type ℓ'
    id   : ∀ {x} → Hom[ x , x ]
    _⋆_  : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
    ⋆IdL : ∀ {x y} (f : Hom[ x , y ]) → id ⋆ f ≡ f
    ⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ id ≡ f
    ⋆Assoc : ∀ {x y z w} (f : Hom[ x , y ]) (g : Hom[ y , z ]) (h : Hom[ z , w ])
           → (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h)
    isSetHom : ∀ {x y} → isSet Hom[ x , y ]

  -- composition: alternative to diagramatic order
  _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ]
  g ∘ f = f ⋆ g

  infixr 9 _⋆_
  infixr 9 _∘_

open Category

-- Helpful syntax/notation
_[_,_] : (C : Category ℓ ℓ') → (x y : C .ob) → Type ℓ'
_[_,_] = Hom[_,_]

-- Needed to define this in order to be able to make the subsequence syntax declaration
seq' : ∀ (C : Category ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
seq' = _⋆_

infixl 15 seq'
syntax seq' C f g = f ⋆⟨ C ⟩ g

-- composition
comp' : ∀ (C : Category ℓ ℓ') {x y z} (g : C [ y , z ]) (f : C [ x , y ]) → C [ x , z ]
comp' = _∘_

infixr 16 comp'
syntax comp' C g f = g ∘⟨ C ⟩ f

-- Isomorphisms and paths in categories
record CatIso (C : Category ℓ ℓ') (x y : C .ob) : Type ℓ' where
  constructor catiso
  field
    mor : C [ x , y ]
    inv : C [ y , x ]
    sec : inv ⋆⟨ C ⟩ mor ≡ C .id
    ret : mor ⋆⟨ C ⟩ inv ≡ C .id

pathToIso : {C : Category ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso C x y
pathToIso {C = C} p = J (λ z _ → CatIso _ _ z) (catiso idx idx (C .⋆IdL idx) (C .⋆IdL idx)) p
  where
    idx = C .id

-- Univalent Categories
record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    univ : (x y : C .ob) → isEquiv (pathToIso {C = C} {x = x} {y = y})

  -- package up the univalence equivalence
  univEquiv : ∀ (x y : C .ob) → (x ≡ y) ≃ (CatIso _ x y)
  univEquiv x y = pathToIso , univ x y

  -- The function extracting paths from category-theoretic isomorphisms.
  CatIsoToPath : {x y : C .ob} (p : CatIso _ x y) → x ≡ y
  CatIsoToPath {x = x} {y = y} p =
    equivFun (invEquiv (univEquiv x y)) p

-- Opposite category
_^op : Category ℓ ℓ' → Category ℓ ℓ'
ob (C ^op)           = ob C
Hom[_,_] (C ^op) x y = C [ y , x ]
id (C ^op)           = id C
_⋆_ (C ^op) f g      = g ⋆⟨ C ⟩ f
⋆IdL (C ^op)         = C .⋆IdR
⋆IdR (C ^op)         = C .⋆IdL
⋆Assoc (C ^op) f g h = sym (C .⋆Assoc _ _ _)
isSetHom (C ^op)     = C .isSetHom


text:
{-# OPTIONS --without-K #-}
-- Two equivalent approached to define the advantage in
-- a (bit) guessing game
open import Data.Two
open import Data.Nat.NP hiding (_==_)
open import Data.Nat.Distance
open import Data.Product.NP

open import Function

open import Explore.Core
open import Explore.Properties
open import Explore.Summable
open import Explore.Sum
open import Explore.Product
open import Explore.Two

open import Relation.Binary.PropositionalEquality.NP

module Explore.GuessingGameFlipping
                 (R : Set)(sum : Sum R)(sum-ind : SumInd sum)(⅁ : 𝟚 → R → 𝟚) where
  open Operators
  X Y : R → 𝟚
  X = ⅁ 0₂
  Y = ⅁ 1₂
  R' = 𝟚 × R
  sum' : Sum R'
  sum' = 𝟚ˢ ×ˢ sum

  open FromSum    sum'    renaming (count to #'_)
  open FromSumInd sum-ind renaming (count to #_)

  G : R' → 𝟚
  G (b , r) = b == ⅁ b r

  1/2 : R' → 𝟚
  1/2 = fst

  -- TODO use the library
  lemma : ∀ X → sum (const 1) ≡ #(not ∘ X) + # X
  lemma X = sum-ind P refl (λ {a}{b} → part1 {a}{b}) part2
    where
      count = FromSum.count

      P = λ s → s (const 1) ≡ count s (not ∘ X) + count s X

      part1 : ∀ {s₀ s₁} → P s₀ → P s₁ → P (λ f → s₀ f + s₁ f)
      part1 {s₀} {s₁} Ps₀ Ps₁ rewrite Ps₀ | Ps₁ = +-interchange (count s₀ (not ∘ X)) (count s₀ X) (count s₁ (not ∘ X)) (count s₁ X)

      part2 : ∀ x → P (λ f → f x)
      part2 x with X x
      part2 x | 0₂ = refl
      part2 x | 1₂ = refl

  thm : dist (#' G) (#' 1/2) ≡ dist (# Y) (# X)
  thm = dist (#' G) (#' 1/2)
      ≡⟨ cong (dist (#' G)) helper ⟩
        dist (#' G) (#(not ∘ X) + # X)
      ≡⟨ refl ⟩ -- #' definition
        dist (# (_==_ 0₂ ∘ X) + # (_==_ 1₂ ∘ Y)) (# (not ∘ X) + # X)
      ≡⟨ refl ⟩ -- #' definition
        dist (# (not ∘ X) + # Y) (# (not ∘ X) + # X)
      ≡⟨ dist-x+ (# (not ∘ X)) (# Y) (# X) ⟩
        dist (# Y) (# X)
      ∎
    where
      open ≡-Reasoning

      helper = #' 1/2
             ≡⟨ refl ⟩
               sum (const 0) + sum (const 1)
             ≡⟨ cong (λ p → p + sum (const 1)) sum-zero ⟩
               sum (const 1)
             ≡⟨ lemma X ⟩
               # (not ∘ X) + # X
             ∎

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
{-# OPTIONS --profile=interactive #-}
open import Common.Prelude
open import Common.Equality

`1     = suc zero
`2     =     `1 +     `1
`4     =     `2 +     `2
`8     =     `4 +     `4
`16    =     `8 +     `8
`32    =    `16 +    `16
`64    =    `32 +    `32
`128   =    `64 +    `64
`256   =   `128 +   `128
`512   =   `256 +   `256
`1024  =   `512 +   `512
`2048  =  `1024 +  `1024
`4096  =  `2048 +  `2048
`8192  =  `4096 +  `4096
`16384 =  `8192 +  `8192
`32768 = `16384 + `16384
`65536 = `32768 + `32768

prf8 : `8 ≡ 8
prf8 = refl

prf65k : `65536 ≡ 65536
prf65k = refl

max_stars_repo_name: sseefried/agda


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Standard evaluation with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Denotation.Evaluation where

open import Nehemiah.Syntax.Type
open import Nehemiah.Syntax.Term
open import Nehemiah.Denotation.Value

open import Data.Integer
open import Structure.Bag.Nehemiah

import Parametric.Denotation.Evaluation Const ⟦_⟧Base as Evaluation

⟦_⟧Const : Evaluation.Structure
⟦ intlit-const n ⟧Const = n
⟦ add-const ⟧Const = λ m n → m + n
⟦ minus-const ⟧Const = λ n → - n
⟦ empty-const ⟧Const = emptyBag
⟦ insert-const ⟧Const = λ n b → singletonBag n ++ b
⟦ union-const ⟧Const = λ b₁ b₂ → b₁ ++ b₂
⟦ negate-const ⟧Const = λ b → negateBag b
⟦ flatmap-const ⟧Const = λ f b → flatmapBag f b
⟦ sum-const ⟧Const = λ b → sumBag b

open Evaluation.Structure ⟦_⟧Const public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Fun.Facts.Iso where

open import Cats.Category
open import Cats.Category.Cat using (_≈_)
open import Cats.Category.Fun using (Fun ; Trans ; ≈-intro ; ≈-elim)
open import Cats.Functor using (Functor)
open import Cats.Trans.Iso using (NatIso)

import Cats.Category.Constructions.Iso as Iso

open NatIso
open Trans
open Iso.Iso

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

  open Category (Fun C D) using (_≅_)

  ≈→≅ : F ≈ G → F ≅ G
  ≈→≅ i = record
    { forth = Forth i
    ; back = Back i
    ; back-forth = ≈-intro (back-forth (iso i))
    ; forth-back = ≈-intro (forth-back (iso i))
    }

  ≅→≈ : F ≅ G → F ≈ G
  ≅→≈ i = record
    { iso = λ {c} → record
      { forth = component (forth i) c
      ; back = component (back i) c
      ; back-forth = ≈-elim (back-forth i)
      ; forth-back = ≈-elim (forth-back i)
      }
    ; forth-natural = natural (forth i)
    }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
module PiFrac.NoRepeat where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import PiFrac.Syntax
open import PiFrac.Opsem
open import PiFrac.AuxLemmas
import PartialRevNoRepeat

-- Forward deterministic
deterministic : ∀ {st st₁ st₂} → st ↦ st₁ → st ↦ st₂ → st₁ ≡ st₂
deterministic (↦₁ {b = b₁}) (↦₁ {b = b₂}) with base-is-prop _ b₁ b₂
... | refl = refl
deterministic ↦₂ ↦₂ = refl
deterministic ↦₃ ↦₃ = refl
deterministic ↦₄ ↦₄ = refl
deterministic ↦₅ ↦₅ = refl
deterministic ↦₆ ↦₆ = refl
deterministic ↦₇ ↦₇ = refl
deterministic ↦₈ ↦₈ = refl
deterministic ↦₉ ↦₉ = refl
deterministic ↦₁₀ ↦₁₀ = refl
deterministic ↦₁₁ ↦₁₁ = refl
deterministic ↦₁₂ ↦₁₂ = refl
deterministic ↦η ↦η = refl
deterministic ↦ε₁ ↦ε₁ = refl
deterministic (↦ε₁ {eq = eq}) (↦ε₂ {neq = neq}) = ⊥-elim (neq eq)
deterministic (↦ε₂ {neq = neq}) (↦ε₁ {eq = eq}) = ⊥-elim (neq eq)
deterministic ↦ε₂ ↦ε₂ = refl

-- Backward deterministic
deterministicᵣₑᵥ : ∀ {st st₁ st₂} → st₁ ↦ st → st₂ ↦ st → st ≢ ⊠ → st₁ ≡ st₂
deterministicᵣₑᵥ {［ c ∣ _ ∣ κ ］} {⟨ c ∣ v ∣ κ ⟩} {⟨ c' ∣ v' ∣ κ' ⟩} ↦₁ r st≠⊠ with Lemma₁ r
... | refl , refl with Lemma₂ r
deterministicᵣₑᵥ {［ uniti₊l  ∣ _ ∣ κ ］} {⟨ _ ∣ x             ∣ κ ⟩} {⟨ _ ∣ x             ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ unite₊l  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ x        ∣ κ ⟩} {⟨ _ ∣ inj₂ x        ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap₊    ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap₊    ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ y        ∣ κ ⟩} {⟨ _ ∣ inj₂ y        ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩} ↦₁ () _ | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩} ↦₁ () _ | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ z        ∣ κ ⟩} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩} ↦₁ () _ | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ z        ∣ κ ⟩} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩} ↦₁ () _ | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ z        ∣ κ ⟩} {⟨ _ ∣ inj₂ z        ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ unite⋆l  ∣ _ ∣ κ ］} {⟨ _ ∣ (tt , v)      ∣ κ ⟩} {⟨ _ ∣ (tt , v)      ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ uniti⋆l  ∣ _ ∣ κ ］} {⟨ _ ∣ v             ∣ κ ⟩} {⟨ _ ∣ v             ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap⋆    ∣ _ ∣ κ ］} {⟨ _ ∣ (x , y)       ∣ κ ⟩} {⟨ _ ∣ (x , y)       ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl⋆  ∣ _ ∣ κ ］} {⟨ _ ∣ (x , (y , z)) ∣ κ ⟩} {⟨ _ ∣ (x , (y , z)) ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr⋆  ∣ _ ∣ κ ］} {⟨ _ ∣ ((x , y) , z) ∣ κ ⟩} {⟨ _ ∣ ((x , y) , z) ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ dist     ∣ _ ∣ κ ］} {⟨ _ ∣ (inj₁ x , z)  ∣ κ ⟩} {⟨ _ ∣ (inj₁ x , z)  ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ dist     ∣ _ ∣ κ ］} {⟨ _ ∣ (inj₂ y , z)  ∣ κ ⟩} {⟨ _ ∣ (inj₂ y , z)  ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ factor   ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ (x , z)  ∣ κ ⟩} {⟨ _ ∣ inj₁ (x , z)  ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ factor   ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ (y , z)  ∣ κ ⟩} {⟨ _ ∣ inj₂ (y , z)  ∣ κ ⟩} ↦₁ ↦₁ _ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap₊    ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ unite⋆l  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ uniti⋆l  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ swap⋆    ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ assocl⋆  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ assocr⋆  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ dist     ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ factor   ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ id↔      ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} (↦₁ {b = ()})
deterministicᵣₑᵥ {［ c₁ ⨾ c₂  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} (↦₁ {b = ()})
deterministicᵣₑᵥ {［ c₁ ⊕ c₂  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} (↦₁ {b = ()})
deterministicᵣₑᵥ {［ c₁ ⊗ c₂  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} (↦₁ {b = ()})
deterministicᵣₑᵥ {_} {_} {_} ↦₂ ↦₂ st≠⊠ = refl
deterministicᵣₑᵥ {_} {_} {_} ↦₃ ↦₃ st≠⊠ = refl
deterministicᵣₑᵥ {_} {_} {_} ↦₄ ↦₄ st≠⊠ = refl
deterministicᵣₑᵥ {_} {_} {_} ↦₅ ↦₅ st≠⊠ = refl
deterministicᵣₑᵥ {_} {_} {_} ↦₆ ↦₆ st≠⊠ = refl
deterministicᵣₑᵥ {_} {_} {_} ↦₇ ↦₇ st≠⊠ = refl
deterministicᵣₑᵥ {_} {_} {_} ↦₈ ↦₈ st≠⊠ = refl
deterministicᵣₑᵥ {_} {_} {_} ↦₉ ↦₉ st≠⊠ = refl
deterministicᵣₑᵥ {_} {_} {_} ↦₁₀ ↦₁₀ st≠⊠ = refl
deterministicᵣₑᵥ {.(［ _ ⊕ _ ∣ inj₁ _ ∣ _ ］)} {_} {⟨ c ∣ v ∣ κ ⟩} ↦₁₁ r st≠⊠ with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with Lemma₃ r
... | inj₂ (inj₂ refl) with Lemma₄ r
... | inj₁ ()
... | inj₂ ()
deterministicᵣₑᵥ {［ _ ⊕ _ ∣ inj₁ _ ∣ _ ］} {_} {_} ↦₁₁ ↦₁₁ st≠⊠ = refl
deterministicᵣₑᵥ {［ _ ⊕ _ ∣ inj₂ _ ∣ _ ］} {［ _ ∣ _ ∣ _ ⊕☐• _ ］} {⟨ c ∣ v ∣ κ ⟩} ↦₁₂ r st≠⊠ with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with Lemma₃ r
... | inj₂ (inj₂ refl) with Lemma₄ r
... | inj₁ ()
... | inj₂ ()
deterministicᵣₑᵥ {［ _ ⊕ _ ∣ inj₂ _ ∣ _ ］} {_} {_} ↦₁₂ ↦₁₂ st≠⊠ = refl
deterministicᵣₑᵥ {［ ηₓ v ∣ _ ∣ _ ］} {⟨ ηₓ v ∣ tt ∣ _ ⟩} {⟨ _ ∣ v' ∣ _ ⟩} ↦η r st≠⊠ with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with v'
... | tt = refl
deterministicᵣₑᵥ {［ εₓ v ∣ tt ∣ _ ］} {_} {_} (↦ε₁ {eq = refl}) (↦ε₁ {eq = refl}) st≠⊠ = refl
deterministicᵣₑᵥ {⊠} {⟨ εₓ v ∣ _ , ↻ ∣ _ ⟩} {_} ↦ε₂ ↦ε₂ st≠⊠ = ⊥-elim (st≠⊠ refl)

-- Non-repeating Lemma

⊠-is-stuck : ∀ {st} → st ≡ ⊠ → ∄[ st' ] (st ↦ st')
⊠-is-stuck refl = λ ()

open PartialRevNoRepeat (record { State = State
                                ; _↦_ = _↦_
                                ; is-fail = λ st → st ≡ ⊠
                                ; is-fail? = (λ { ⊠ → yes refl
                                                ; ⟨ _ ∣ _ ∣ _ ⟩ → no (λ ())
                                                ; ［ _ ∣ _ ∣ _ ］ → no (λ ())})
                                ; fail-is-stuck = ⊠-is-stuck
                                ; deterministic = deterministic
                                ; deterministicᵣₑᵥ = deterministicᵣₑᵥ}) public


text:
{-#  OPTIONS --type-in-type #-}
module ArgsWrongOrder where

open import AgdaPrelude

myFun : (a : Set) -> a -> Nat -> Nat
myFun _ x y = y

myApp = myFun _ Zero (Nil Nat)

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
{-# OPTIONS --prop #-}

data _≡_ {X : Set} (a : X) : X → Prop where
  refl : a ≡ a

postulate
  A : Set
  P : Prop
  p : P
  u : P → A

f : {x : A} (q : u p ≡ x) → P
f refl = p   -- works in 2.6.0.1

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

{-
  favonia:
  On 2017/03/23, after I added back Mayer-Vietoris, it seems
  difficult to type check everything in one round on travis,
  so parts of index.agda are moved here.

  favonia:
  On 2017/05/08, I further partition the results into multiple
  independent index[n].agda files because the garbage collection
  is not really working.
-}

module index2stage2 where

{- isomorphisms between different kinds of cohomology groups for finite CWs. -}
import cw.cohomology.AxiomaticIsoCellular

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Multidimensional.Data.Extra.Nat.Base where

open import Cubical.Data.Nat

sucn : (n : ℕ) → (ℕ → ℕ)
sucn n = iter n suc

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

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

module Definition01b where

postulate
  D   : Set
  _≡_ : D → D → Set

-- We test the translation of the definition of a unary function.
foo : D → D
foo d = d
{-# ATP definition foo #-}

postulate bar : ∀ d → d ≡ foo d
{-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

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

open import Numbers.ClassicalReals.RealField
open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Setoids.Orders
open import Sets.EquivalenceRelations
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Fields
open import Groups.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Sequences

module Numbers.ClassicalReals.Sequences (ℝ : RealField) where

open RealField ℝ
open Setoid S
open Equivalence eq
open Ring R
open Field F
open SetoidPartialOrder pOrder
open import Fields.Orders.LeastUpperBounds.Definition pOrder
open import Rings.Orders.Total.Lemmas orderedRing
open import Rings.Orders.Partial.Lemmas pOrderedRing
open Group additiveGroup
open PartiallyOrderedRing pOrderedRing
open SetoidTotalOrder (TotallyOrderedRing.total orderedRing)
open import Rings.InitialRing R
open import Fields.Orders.Lemmas oField
open import Rings.Lemmas R
open import Groups.Lemmas additiveGroup
open import Numbers.Intervals.Definition pOrderedRing
open import Numbers.Intervals.Arithmetic pOrderedRing
open import Fields.Lemmas F
open import Fields.Orders.Total.Definition F

orderedField : TotallyOrderedField pOrderedRing
orderedField = record { oRing = orderedRing }

open import Fields.Orders.Limits.Definition orderedField

StrictlyIncreasing : Sequence A → Set c
StrictlyIncreasing x = (n : ℕ) → (index x n) < (index x (succ n))

Increasing : Sequence A → Set (b ⊔ c)
Increasing x = (n : ℕ) → ((index x n) < (index x (succ n))) || ((index x n) ∼ (index x (succ n)))

sequencePredicate : (x : Sequence A) → A → Set b
sequencePredicate x a = Sg ℕ (λ n → index x n ∼ a)

sequenceSubset : (x : Sequence A) → subset S (sequencePredicate x)
sequenceSubset sequence {x} {y} x=y (n , sn=x) = n , transitive sn=x x=y

boundedSequenceBounds : (K : A) (x : Sequence A) → ((n : ℕ) → index x n < K) → UpperBound (sequenceSubset x) K
boundedSequenceBounds K x pr y (n , y=xn) = inl (<WellDefined y=xn reflexive (pr n))

increasingBoundedLimit : (x : Sequence A) → Increasing x → Bounded x → A
increasingBoundedLimit x increasing (K , kIsBound) with lub (sequenceSubset x) ((index x 0) , (0 , reflexive)) (K , boundedSequenceBounds K x kIsBound)
... | a , _ = a

increasingBoundedConverges : (x : Sequence A) → (increasing : Increasing x) → (bounded : Bounded x) → x ~> (increasingBoundedLimit x increasing bounded)
increasingBoundedConverges x increasing (K , prBound) with lub (sequenceSubset x) (Sequence.head x , (0 , reflexive)) (K , boundedSequenceBounds K x prBound)
... | lub , isLub = {!!}


text:
------------------------------------------------------------------------
-- Code related to the paper "Up-to Techniques using Sized Types"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

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

module README where

------------------------------------------------------------------------
-- Pointers to results from the paper

-- In order to more easily find code corresponding to results from the
-- paper, see the following module. Note that some of the code
-- referenced below is not discussed at all in the paper.

import README.Pointers-to-results-from-the-paper

------------------------------------------------------------------------
-- Some preliminaries

-- Overloaded "equational" reasoning combinators.

import Equational-reasoning

-- Unary and binary relations.

import Relation

------------------------------------------------------------------------
-- Containers

-- Indexed containers.

import Indexed-container

-- Container combinators.

import Indexed-container.Combinators

-- The delay monad defined as the greatest fixpoint of an indexed
-- container.

import Indexed-container.Delay-monad

------------------------------------------------------------------------
-- Up-to techniques

-- Up-to techniques, compatibility, size-preserving functions, and the
-- companion.

import Up-to

-- Closure properties for Compatible and Size-preserving.
--
-- (Some negative results in this module depend on code presented
-- further down.)

import Up-to.Closure

-- Up-to techniques via.

import Up-to.Via

------------------------------------------------------------------------
-- Labelled transition systems

-- Labelled transition systems (LTSs).

import Labelled-transition-system
import Labelled-transition-system.Equational-reasoning-instances

-- CCS.

import Labelled-transition-system.CCS

-- A labelled transition system for the delay monad.

import Labelled-transition-system.Delay-monad

-- An LTS from Section 6.2.5 of "Enhancements of the bisimulation
-- proof method" by Pous and Sangiorgi.

import Labelled-transition-system.6-2-5

------------------------------------------------------------------------
-- Similarity

-- The one-sided Step function, used to define similarity and the
-- two-sided Step function.

import Similarity.Step

-- A parametrised coinductive definition that can be used to define
-- various forms of similarity.

import Similarity.General

-- For more information about similarity, see "Similarity, continued"
-- below.

------------------------------------------------------------------------
-- Strong bisimilarity

-- The Step function, used to define strong and weak bisimilarity as
-- well as expansion.

import Bisimilarity.Step

-- A parametrised coinductive definition that can be used to define
-- strong and weak bisimilarity as well as expansion.

import Bisimilarity.General

-- A coinductive definition of (strong) bisimilarity.

import Bisimilarity
import Bisimilarity.Equational-reasoning-instances

-- The classical definition of (strong) bisimilarity.

import Bisimilarity.Classical
import Bisimilarity.Classical.Equational-reasoning-instances

-- A comparison of the two definitions of bisimilarity.

import Bisimilarity.Comparison

-- Some results related to strong bisimilarity for the delay monad.

import Bisimilarity.Delay-monad

-- Some results related to CCS, implemented without using a fixed form
-- of bisimilarity.

import Bisimilarity.CCS.General

-- Various results or examples related to CCS, implemented using the
-- coinductive definition of bisimilarity.

import Bisimilarity.CCS
import Bisimilarity.CCS.Examples
import Bisimilarity.CCS.Examples.Natural-numbers

-- Some of the results/examples above have also been implemented using
-- the classical definition of bisimilarity.

import Bisimilarity.CCS.Classical
import Bisimilarity.CCS.Examples.Classical

-- Up-to techniques for strong bisimilarity.

import Bisimilarity.Up-to
import Bisimilarity.Up-to.CCS
import Bisimilarity.Up-to.Counterexamples

-- Some results related to an LTS from Section 6.2.5 of "Enhancements
-- of the bisimulation proof method" by Pous and Sangiorgi,
-- implemented using the coinductive definition of bisimilarity.

import Bisimilarity.6-2-5

------------------------------------------------------------------------
-- Expansion

-- A coinductive definition of the expansion ordering.

import Expansion
import Expansion.Equational-reasoning-instances

-- Lemmas related to expansion and CCS.

import Expansion.CCS

-- Some results related to expansion for the delay monad.

import Expansion.Delay-monad

------------------------------------------------------------------------
-- Weak bisimilarity

-- A coinductive definition of weak bisimilarity.

import Bisimilarity.Weak
import Bisimilarity.Weak.Equational-reasoning-instances

-- An alternative (non-standard) coinductive definition of weak
-- bisimilarity.

import Bisimilarity.Weak.Alternative
import Bisimilarity.Weak.Alternative.Equational-reasoning-instances

-- An alternative (non-standard) classical definition of weak
-- bisimilarity.

import Bisimilarity.Weak.Alternative.Classical

-- A comparison of the two alternative definitions of weak
-- bisimilarity.

import Bisimilarity.Weak.Alternative.Comparison

-- The two coinductive definitions of weak bisimilarity are pointwise
-- logically equivalent.

import Bisimilarity.Weak.Equivalent

-- Lemmas related to weak bisimilarity and CCS.

import Bisimilarity.Weak.CCS

-- Examples/exercises related to CCS from "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.

import Bisimilarity.Weak.CCS.Examples

-- Some results about various forms of coinductively defined weak
-- bisimilarity for the delay monad.

import Bisimilarity.Weak.Delay-monad

-- Up-to techniques for the standard coinductive definition of weak
-- bisimilarity.

import Bisimilarity.Weak.Up-to
import Bisimilarity.Weak.Up-to.CCS

-- Up-to techniques for the delay monad and the alternative
-- coinductive definition of weak bisimilarity.

import Bisimilarity.Weak.Alternative.Up-to.Delay-monad

------------------------------------------------------------------------
-- Similarity, continued

-- A coinductive definition of (strong) similarity.

import Similarity
import Similarity.Equational-reasoning-instances

-- Lemmas related to strong similarity for CCS.

import Similarity.CCS

-- A coinductive definition of weak similarity.

import Similarity.Weak
import Similarity.Weak.Equational-reasoning-instances

-- An up-to technique for weak similarity.

import Similarity.Weak.Up-to

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
-- Length-indexed lists as a recursive family
-- From "Dependent Types at Work", section 3.1

module xx where

open import Level renaming (suc to lsuc)
open import Data.Nat hiding (_^_)
open import Data.Empty.Polymorphic
open import Data.Unit.Polymorphic
open import Data.Maybe hiding (map ; zip)
open import Data.Product hiding (map ; zip)

private
  variable
    m n : ℕ
    ℓ ℓ′ : Level
    A : Set ℓ
    B : Set ℓ′

-- Vec : Set ℓ → ℕ → Set ℓ
-- Vec A zero = ⊤
-- Vec A (suc n) = A × Vec A n

-- Generalize Vec

open import Function

iter : A → (A → A) → ℕ → A
iter z f zero    = z
iter z f (suc n) = f (iter z f n)

-- Is iter defined somewhere standard?

Vec : Set ℓ → ℕ → Set ℓ
Vec A = iter ⊤ (A ×_)

head : Vec A (suc n) → A
head (a , _) = a

tail : Vec A (suc n) → Vec A n
tail (_ , as) = as

map : (A → B) → Vec A n → Vec B n
map {n = zero } _ _ = tt
map {n = suc n} f (a , as) = f a , map {n = n} f as

zip : Vec A n → Vec B n → Vec (A × B) n
zip {n = zero } _ _ = tt
zip {n = suc n} (a , as) (b , bs) = (a , b) , zip {n = n} as bs

Fin : ℕ → Set
Fin zero    = ⊥
Fin (suc n) = Maybe (Fin n)

f5 : Fin 5
f5 = nothing
f4 : Fin 4
f4 = nothing
f3 : Fin 3
f3 = nothing
f2 : Fin 2
f2 = just nothing -- an element of the type
f1 : Fin 1
f1 = nothing
-- f0 : Fin 0
-- f0 = {!!} -- no solution found

_!_ : Vec A n → Fin n → A
_!_ {n = suc m} (a , _ ) nothing = a
_!_ {n = suc m} (_ , as) (just i) = as ! i

_!'_ : Vec A n → Fin n → A
_!'_ {n = suc m} (a , _)   nothing    = a
_!'_ {n = suc m} (_ , as) (just finm) = as !' finm

{-
(0 , 1 , 2 , tt) !                  nothing
(0 , 1 , 2 , tt) !             just nothing
(0 , 1 , 2 , tt) !       just (just nothing)
(0 , 1 , 2 , tt) ! just (just (just nothing))
-}

-- Perfect binary leaf tree
BTree : Set ℓ → ℕ → Set ℓ
BTree A = iter A (λ τ → τ × τ)

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

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

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


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Structures for homogeneous binary relations
------------------------------------------------------------------------

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

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

open import Relation.Binary.Core

module Relation.Binary.Structures
  {a ℓ} {A : Set a} -- The underlying set
  (_≈_ : Rel A ℓ)   -- The underlying equality relation
  where

open import Data.Product using (proj₁; proj₂; _,_)
open import Level using (Level; _⊔_)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Binary.Consequences
open import Relation.Binary.Definitions

private
  variable
    ℓ₂ : Level

------------------------------------------------------------------------
-- Equivalences
------------------------------------------------------------------------
-- Note all the following equivalences refer to the equality provided
-- as a module parameter at the top of this file.

record IsPartialEquivalence : Set (a ⊔ ℓ) where
  field
    sym   : Symmetric _≈_
    trans : Transitive _≈_

-- The preorders of this library are defined in terms of an underlying
-- equivalence relation, and hence equivalence relations are not
-- defined in terms of preorders.

-- To preserve backwards compatability, equivalence relations are
-- not defined in terms of their partial counterparts.

record IsEquivalence : Set (a ⊔ ℓ) where
  field
    refl  : Reflexive _≈_
    sym   : Symmetric _≈_
    trans : Transitive _≈_

  reflexive : _≡_ ⇒ _≈_
  reflexive P.refl = refl

  isPartialEquivalence : IsPartialEquivalence
  isPartialEquivalence = record
    { sym = sym
    ; trans = trans
    }

record IsDecEquivalence : Set (a ⊔ ℓ) where
  infix 4 _≟_
  field
    isEquivalence : IsEquivalence
    _≟_           : Decidable _≈_

  open IsEquivalence isEquivalence public

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

record IsPreorder (_∼_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence
    -- Reflexivity is expressed in terms of the underlying equality:
    reflexive     : _≈_ ⇒ _∼_
    trans         : Transitive _∼_

  module Eq = IsEquivalence isEquivalence

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

  ∼-respˡ-≈ : _∼_ Respectsˡ _≈_
  ∼-respˡ-≈ x≈y x∼z = trans (reflexive (Eq.sym x≈y)) x∼z

  ∼-respʳ-≈ : _∼_ Respectsʳ _≈_
  ∼-respʳ-≈ x≈y z∼x = trans z∼x (reflexive x≈y)

  ∼-resp-≈ : _∼_ Respects₂ _≈_
  ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈

------------------------------------------------------------------------
-- Partial orders
------------------------------------------------------------------------

record IsPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isPreorder : IsPreorder _≤_
    antisym    : Antisymmetric _≈_ _≤_

  open IsPreorder isPreorder public
    renaming
    ( ∼-respˡ-≈ to ≤-respˡ-≈
    ; ∼-respʳ-≈ to ≤-respʳ-≈
    ; ∼-resp-≈  to ≤-resp-≈
    )

record IsDecPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  infix 4 _≟_ _≤?_
  field
    isPartialOrder : IsPartialOrder _≤_
    _≟_            : Decidable _≈_
    _≤?_           : Decidable _≤_

  open IsPartialOrder isPartialOrder public
    hiding (module Eq)

  module Eq where

    isDecEquivalence : IsDecEquivalence
    isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = _≟_
      }

    open IsDecEquivalence isDecEquivalence public

record IsStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence
    irrefl        : Irreflexive _≈_ _<_
    trans         : Transitive _<_
    <-resp-≈      : _<_ Respects₂ _≈_

  module Eq = IsEquivalence isEquivalence

  asym : Asymmetric _<_
  asym {x} {y} = trans∧irr⟶asym Eq.refl trans irrefl {x = x} {y}

  <-respʳ-≈ : _<_ Respectsʳ _≈_
  <-respʳ-≈ = proj₁ <-resp-≈

  <-respˡ-≈ : _<_ Respectsˡ _≈_
  <-respˡ-≈ = proj₂ <-resp-≈

  asymmetric = asym
  {-# WARNING_ON_USAGE asymmetric
  "Warning: asymmetric was deprecated in v0.16.
  Please use asym instead."
  #-}

record IsDecStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  infix 4 _≟_ _<?_
  field
    isStrictPartialOrder : IsStrictPartialOrder _<_
    _≟_                  : Decidable _≈_
    _<?_                 : Decidable _<_

  private
    module SPO = IsStrictPartialOrder isStrictPartialOrder

  open SPO public hiding (module Eq)

  module Eq where

    isDecEquivalence : IsDecEquivalence
    isDecEquivalence = record
      { isEquivalence = SPO.isEquivalence
      ; _≟_           = _≟_
      }

    open IsDecEquivalence isDecEquivalence public

------------------------------------------------------------------------
-- Total orders
------------------------------------------------------------------------

record IsTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isPartialOrder : IsPartialOrder _≤_
    total          : Total _≤_

  open IsPartialOrder isPartialOrder public

record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  infix 4 _≟_ _≤?_
  field
    isTotalOrder : IsTotalOrder _≤_
    _≟_          : Decidable _≈_
    _≤?_         : Decidable _≤_

  open IsTotalOrder isTotalOrder public
    hiding (module Eq)

  isDecPartialOrder : IsDecPartialOrder _≤_
  isDecPartialOrder = record
    { isPartialOrder = isPartialOrder
    ; _≟_            = _≟_
    ; _≤?_           = _≤?_
    }

  module Eq where

    isDecEquivalence : IsDecEquivalence
    isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = _≟_
      }

    open IsDecEquivalence isDecEquivalence public

-- Note that these orders are decidable. The current implementation
-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
-- definition capturing these three properties implies decidability
-- as `Trichotomous` necessarily separates out the equality case.

record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence
    trans         : Transitive _<_
    compare       : Trichotomous _≈_ _<_

  infix 4 _≟_ _<?_

  _≟_ : Decidable _≈_
  _≟_ = tri⟶dec≈ compare

  _<?_ : Decidable _<_
  _<?_ = tri⟶dec< compare

  isDecEquivalence : IsDecEquivalence
  isDecEquivalence = record
    { isEquivalence = isEquivalence
    ; _≟_           = _≟_
    }

  module Eq = IsDecEquivalence isDecEquivalence

  isStrictPartialOrder : IsStrictPartialOrder _<_
  isStrictPartialOrder = record
    { isEquivalence = isEquivalence
    ; irrefl        = tri⟶irr compare
    ; trans         = trans
    ; <-resp-≈      = trans∧tri⟶resp≈ Eq.sym Eq.trans trans compare
    }

  isDecStrictPartialOrder : IsDecStrictPartialOrder _<_
  isDecStrictPartialOrder = record
    { isStrictPartialOrder = isStrictPartialOrder
    ; _≟_                  = _≟_
    ; _<?_                 = _<?_
    }

  open IsStrictPartialOrder isStrictPartialOrder public
    using (irrefl; asym; <-respʳ-≈; <-respˡ-≈; <-resp-≈)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Maybes where all the elements satisfy a given property
------------------------------------------------------------------------

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

module Data.Maybe.Relation.Unary.All where

open import Category.Applicative
open import Category.Monad
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Maybe.Relation.Unary.Any using (Any; just)
open import Data.Product as Prod using (_,_)
open import Function using (id; _∘′_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_; cong)
open import Relation.Unary
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec

------------------------------------------------------------------------
-- Definition

data All {a p} {A : Set a} (P : Pred A p) : Pred (Maybe A) (a ⊔ p) where
  just    : ∀ {x} → P x → All P (just x)
  nothing : All P nothing

------------------------------------------------------------------------
-- Basic operations

module _ {a p} {A : Set a} {P : Pred A p} where

  drop-just : ∀ {x} → All P (just x) → P x
  drop-just (just px) = px

  just-equivalence : ∀ {x} → P x ⇔ All P (just x)
  just-equivalence = equivalence just drop-just

  map : ∀ {q} {Q : Pred A q} → P ⊆ Q → All P ⊆ All Q
  map f (just px) = just (f px)
  map f nothing   = nothing

  fromAny : Any P ⊆ All P
  fromAny (just px) = just px

------------------------------------------------------------------------
-- (un/)zip(/With)

module _ {a p q r} {A : Set a} {P : Pred A p} {Q : Pred A q} {R : Pred A r} where

  zipWith : P ∩ Q ⊆ R → All P ∩ All Q ⊆ All R
  zipWith f (just px , just qx) = just (f (px , qx))
  zipWith f (nothing , nothing) = nothing

  unzipWith : P ⊆ Q ∩ R → All P ⊆ All Q ∩ All R
  unzipWith f (just px) = Prod.map just just (f px)
  unzipWith f nothing   = nothing , nothing

module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where

  zip : All P ∩ All Q ⊆ All (P ∩ Q)
  zip = zipWith id

  unzip : All (P ∩ Q) ⊆ All P ∩ All Q
  unzip = unzipWith id

------------------------------------------------------------------------
-- Traversable-like functions

module _ {a} p {A : Set a} {P : Pred A (a ⊔ p)} {F}
         (App : RawApplicative {a ⊔ p} F) where

  open RawApplicative App

  sequenceA : All (F ∘′ P) ⊆ F ∘′ All P
  sequenceA nothing   = pure nothing
  sequenceA (just px) = just <$> px

  mapA : ∀ {q} {Q : Pred A q} → (Q ⊆ F ∘′ P) → All Q ⊆ (F ∘′ All P)
  mapA f = sequenceA ∘′ map f

  forA : ∀ {q} {Q : Pred A q} {xs} → All Q xs → (Q ⊆ F ∘′ P) → F (All P xs)
  forA qxs f = mapA f qxs

module _ {a} p {A : Set a} {P : Pred A (a ⊔ p)} {M}
         (Mon : RawMonad {a ⊔ p} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM : All (M ∘′ P) ⊆ M ∘′ All P
  sequenceM = sequenceA p App

  mapM : ∀ {q} {Q : Pred A q} → (Q ⊆ M ∘′ P) → All Q ⊆ (M ∘′ All P)
  mapM = mapA p App

  forM : ∀ {q} {Q : Pred A q} {xs} → All Q xs → (Q ⊆ M ∘′ P) → M (All P xs)
  forM = forA p App

------------------------------------------------------------------------
-- Seeing All as a predicate transformer

module _ {a p} {A : Set a} {P : Pred A p} where

  dec : Decidable P → Decidable (All P)
  dec P-dec nothing  = yes nothing
  dec P-dec (just x) = Dec.map just-equivalence (P-dec x)

  universal : Universal P → Universal (All P)
  universal P-universal (just x) = just (P-universal x)
  universal P-universal nothing  = nothing

  irrelevant : Irrelevant P → Irrelevant (All P)
  irrelevant P-irrelevant (just p) (just q) = cong just (P-irrelevant p q)
  irrelevant P-irrelevant nothing  nothing  = P.refl

  satisfiable : Satisfiable (All P)
  satisfiable = nothing , nothing


text:
-- Andreas, 2017-03-30, issue #2524
-- compile abstract definitions to arbitrary Haskell code

module Issue2524 where

open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.String

{-# FOREIGN GHC import qualified Data.Text #-}

postulate
  NativeIO     : Set → Set
  nativeReturn : {A : Set} → A → NativeIO A
  _native>>=_  : {A B : Set} → NativeIO A → (A → NativeIO B) → NativeIO B

{-# BUILTIN IO NativeIO #-}
{-# COMPILE GHC NativeIO = type IO #-}
{-# COMPILE GHC nativeReturn = (\_ -> return :: a -> IO a) #-}
{-# COMPILE GHC _native>>=_ = (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}
{-# COMPILE JS nativeReturn =
    function(u0) { return function(u1) { return function(x) { return function(cb) { cb(x); }; }; }; } #-}
{-# COMPILE JS _native>>=_ =
  function(u0) { return function(u1) { return function(u2) { return function(u3) {
    return function(x) { return function(y) { return function(cb) {
      x(function (xx) { y(xx)(cb); });
  }; }; };
  }; }; }; }
#-}

postulate
  nativePutStrLn  : String → NativeIO ⊤
  primShowNat     : Nat → String

{-# COMPILE GHC nativePutStrLn = (\ s -> putStrLn (Data.Text.unpack s)) #-}
{-# COMPILE GHC primShowNat = Data.Text.pack . show #-}
{-# COMPILE JS nativePutStrLn = function (x) { return function(cb) { process.stdout.write(x + '\n'); cb(0); }; } #-}
{-# COMPILE JS primShowNat = agdaRTS.primShowInteger #-}

abstract
  record Pointer : Set where
    constructor mkPointer
    field thePointer : Nat
          otherInfo  : Nat

  newPointer : Pointer
  newPointer = mkPointer 5 17

  showPointer : Pointer → String
  showPointer p = primShowNat (Pointer.thePointer p)

{-# COMPILE GHC Pointer = type Integer #-}
{-# COMPILE GHC newPointer = 5 #-}
{-# COMPILE GHC showPointer = Data.Text.pack . show #-}
{-# COMPILE JS newPointer = 5 #-}
{-# COMPILE JS showPointer = function(x) { return x; } #-}

main : NativeIO ⊤
main = nativePutStrLn (showPointer newPointer)

max_stars_repo_name: shlevy/agda


text:
module Data.Lens.Proofs.LensLaws where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Agda.Primitive

-- First, define the lens laws

ViewSet : {a b : Set} -> (l : Lens a b) -> Set
ViewSet {a} {b} l = (v : b) (s : a) -> view l (set l v s) ≡ v

SetView : {a b : Set} -> (l : Lens a b) -> Set
SetView {a} {b} l = (s : a) -> set l (view l s) s ≡ s

SetSet : {a b : Set} -> (l : Lens a b) -> Set
SetSet {a} {b} l = (v1 v2 : b) (s : a) -> set l v2 (set l v1 s) ≡ set l v2 s

-- Define ValidLens as a lens for which the laws hold

data ValidLens (a b : Set) : Set₁ where
  CValidLens : (l : Lens a b) -> ViewSet l -> SetView l -> SetSet l -> ValidLens a b

toLens : ValidLens a b -> Lens a b
toLens (CValidLens l _ _ _) = l

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
record R {a} (A : Set a) : Set a where
  field
    some : A

module Works0 where

  works : ∀ {a}{A : Set a} {{r : R A}} -> A
  works = x
    where
      open R {{...}}
      x = some

-- If we add a dummy argument of type Set to "works" we fail, see module Fails
-- below.

-- But there is a chance it still works:

module Works where

  postulate
    works : ∀ {a}{A : Set a} -> A

  test : ∀ {a}{A : Set a} {{r : R A}} -> Set -> A
  test B = x
    where
      open R {{...}}
      x = some

-- Or, we could have an unsolved meta:

module Unsolved where

  postulate
    works : ∀ {a}{A : Set a} {r : R A} -> A

  test : ∀ {a}{A : Set a} {{r : R A}} -> Set -> A
  test B = x
    where
      open R {{...}}
      x = some
  -- unsolved at "x" in "test B = x":
  -- _r_45 : R (R .A)

-- This is the mysterious failure instance:

module Fails where

  fails : ∀ {a}{A : Set a} {{r : R A}} -> Set -> A
  fails B = x
    where
      open R {{...}}
      x = some
  -- No variable of type R (_A_54 .some B) was found in scope
  -- when checking that the expression x has type .A


text:
module _ where

module A where

  infix 2 _↑
  infix 1 _↓_

  data D : Set where
    ●   : D
    _↑  : D → D
    _↓_ : D → D → D

module B where

  data D : Set where
    _↓_ : D → D → D

open A
open B

rejected : A.D
rejected = ● ↑ ↓ ●


text:
-- Andreas, 2014-05-20, issue reported by Fabien Renaud

module Issue1125 where

f : {A- : Set} -> Set
f {A-} = A-

-- Should give a parse error now
-- since a comment is closed -} but none opened.

max_issues_repo_name: shlevy/agda


text:
-- Andreas, 2021-01-28 documenting #4702, reported by gallais

open import Agda.Builtin.Nat

case_of_ : {A B : Set} → A → (A → B) → B
case x of f = f x

-- Needed for making `plus` pass the termination checker.
-- Used to be automatic via `--auto-inline`, since 2.6.2 this flag
-- is off by default.

{-# INLINE case_of_ #-}

plus : Nat → Nat → Nat
plus m n = case m of λ
   { zero    → n
   ; (suc m) → suc (plus m n)
   }

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Numeral.Ordinal where

import      Lvl
open import Numeral.Natural
open import Syntax.Function
open import Type

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

-- Ordinal numbers up to a certain level as a type.
-- 𝟎 is the zero ordinal, the smallest ordinal number.
-- 𝐒 is the successor ordinal function, the smallest ordinal greater than the given argument.
-- lim is the limit ordinal function, the "limit" of the given sequence. The smallest ordinal greater than all values of the given sequence. Note that this is not the usual definition of a "limit ordinal" because `lim` allows arbitrary sequences, specifically those with a maximum, resulting in an equivalent to the successor ordinal `𝐒` (TODO: If this is the case, then 𝐒 is actually unnecessary? Just define it by (lim ∘ const)?
-- Note: Usually the indexing in a limit ordinal should be the class of ordinals before it, so this definition is probably unable to express all ordinals.
data Ordinal(T : Type{ℓ}) : Type{ℓ} where
  𝟎   : Ordinal(T)
  𝐒   : Ordinal(T) → Ordinal(T)
  lim : (T → Ordinal(T)) → Ordinal(T)

{-
data Ordinal' : (ℓ : Lvl.Level) → Typeω where
  𝟎   : Ordinal'(ℓ)
  𝐒   : Ordinal'(ℓ) → Ordinal'(ℓ)
  lim : (Ordinal'(ℓ) → Ordinal'(Lvl.𝐒(ℓ))) → Ordinal'(Lvl.𝐒(ℓ)) -- When the next ordinal have the current ordinal as its index

data Ordinal(T : Type{ℓ}) : Type{ℓ} where
  𝟎   : Ordinal(T)
  lim : (T → Ordinal(T)) → Ordinal(T) -- 𝐒 is expressable through lim

data Ordinal(T : Type{ℓ}) : Type{ℓ} where
  𝟎   : Ordinal(T)
  𝐒   : Ordinal(T) → Ordinal(T)
  lim : (f : T → Ordinal(T)) → ∃(IncreasingSubsequence(_<_)(f)) → Ordinal(T) -- This excludes the cases where f have a maximum, resulting in no intersection between 𝐒 and lim
-}

_+_ : Ordinal(T) → Ordinal(T) → Ordinal(T)
x + 𝟎     = x
x + 𝐒(y)  = 𝐒(x + y)
x + lim f = lim(y ↦ (x + f(y)))

_⋅_ : Ordinal(T) → Ordinal(T) → Ordinal(T)
x ⋅ 𝟎      = 𝟎
x ⋅ 𝐒(y)   = (x ⋅ y) + x
x ⋅ lim f  = lim(y ↦ (x ⋅ f(y)))

_^_ : Ordinal(T) → Ordinal(T) → Ordinal(T)
x ^ 𝟎     = x
x ^ 𝐒(y)  = (x ^ y) ⋅ x
x ^ lim f = lim(y ↦ (x ^ f(y)))

open import Logic.Propositional

private variable x y z x₁ x₂ y₁ y₂ z₁ z₂ : Ordinal(T)

module _ {T : Type{ℓ}} where
  open import Functional
  open import Logic.Propositional

  -- TODO: Not sure if this is correct
  data _<_ : Ordinal(T) → Ordinal(T) → Type{ℓ} where
    minimal : ∀{x} → (𝟎 < 𝐒(x))
    step    : ∀{x y} → (x < y) → (𝐒(x) < 𝐒(y))
    limitₗ  : ∀{f}{x} → (∀{i} → (f(i) < x)) → (lim f < 𝐒(x))
    limitᵣ  : ∀{i}{f}{x} → (x < 𝐒(f(i))) → (x < lim f)

  _>_ = swap(_<_)

  _≤_ : Ordinal(T) → Ordinal(T) → Type
  x ≤ y = x < 𝐒(y)

  _≥_ = swap(_≤_)

  _≡_ : Ordinal(T) → Ordinal(T) → Type
  x ≡ y = (y ≤ x) ∧ (x ≤ y)

  open import Numeral.Natural.Induction
  from-ℕ : ℕ → Ordinal(T)
  from-ℕ = ℕ-elim 𝟎 (const 𝐒)

  _+ₙ_ : Ordinal(T) → ℕ → Ordinal(T)
  _+ₙ_ x = ℕ-elim x (const 𝐒)

  private variable f g : T → Ordinal(T)
  private variable n : T

  [<]-limitₗ-inv : (lim f < 𝐒(x)) → (∀{n} → (f(n) < x))
  [<]-limitₗ-inv (limitₗ p) = p

  open import Logic.Predicate
  open import Type.Properties.Inhabited
  [<]-limitᵣ-inv : (x < lim f) → ∃(n ↦ (x < 𝐒(f(n))))
  [<]-limitᵣ-inv (limitᵣ{n} p) = [∃]-intro n ⦃ p ⦄

  [<]-lim-minimal : ⦃ ◊ T ⦄ → (𝟎 < lim f)
  [<]-lim-minimal = limitᵣ{i = [◊]-existence} minimal

  [<]-lim-maximum : (f(n) < lim f)
  [<]-of-step : (x < 𝐒(x))

  [<]-lim-maximum{f}{n} = limitᵣ{n} [<]-of-step

  [<]-without-step : (𝐒(x) < 𝐒(y)) → (x < y)
  [<]-without-step (step p) = p

  [<]-of-step {𝟎}     = minimal
  [<]-of-step {𝐒(x)}  = step [<]-of-step
  [<]-of-step {lim f} = limitₗ [<]-lim-maximum

  [<]-transitivity : (x < y) → (y < z) → (x < z)
  [<]-transitivity minimal     (step yz)          = minimal
  [<]-transitivity minimal     (limitᵣ {n}{f} yz) = limitᵣ {n}{f} minimal
  [<]-transitivity (step xy)   (step yz)          = step ([<]-transitivity xy yz)
  [<]-transitivity (step xy)   (limitᵣ yz)        = limitᵣ ([<]-transitivity (step xy) yz)
  [<]-transitivity (limitₗ xy) (step yz)          = limitₗ ([<]-transitivity xy yz)
  [<]-transitivity (limitₗ xy) (limitᵣ yz)        = limitᵣ (limitₗ ([<]-without-step([<]-transitivity (step xy) yz)))
  [<]-transitivity (limitᵣ xy) (limitₗ yz)        = [<]-transitivity xy (step yz)
  [<]-transitivity (limitᵣ xy) (limitᵣ yz)        = limitᵣ ([<]-transitivity (limitᵣ xy) yz)

  [<]-stepᵣ : (x < y) → (x < 𝐒(y))
  [<]-stepᵣ minimal    = minimal
  [<]-stepᵣ (step p)   = step ([<]-stepᵣ p)
  [<]-stepᵣ (limitₗ p) = limitₗ ([<]-stepᵣ p)
  [<]-stepᵣ (limitᵣ p) = [<]-transitivity p (step [<]-lim-maximum)

  [<]-to-[≤] : (x < y) → (x ≤ y)
  [<]-to-[≤] = [<]-stepᵣ

  [<]-irreflexivity : ¬(x < x)
  [<]-irreflexivity (step p)            = [<]-irreflexivity p
  [<]-irreflexivity (limitᵣ (limitₗ x)) = [<]-irreflexivity x

  [<]-asymmetry : (x < y) → (y < x) → ⊥
  [<]-asymmetry xy yx = [<]-irreflexivity([<]-transitivity xy yx)

  [<]-without-stepₗ : (𝐒(x) < y) → (x < y)
  [<]-without-stepₗ (step p)   = [<]-stepᵣ p
  [<]-without-stepₗ (limitᵣ p) = limitᵣ ([<]-without-stepₗ p)

  [<]-no-less-than-minimum : ¬(x < 𝟎)
  [<]-no-less-than-minimum ()

  [≤]-minimal : (𝟎 ≤ x)
  [≤]-minimal = minimal

  [≤]-step : (x ≤ y) → (𝐒(x) ≤ 𝐒(y))
  [≤]-step = step

  [≤]-reflexivity : (x ≤ x)
  [≤]-reflexivity = [<]-of-step

  [≡]-reflexivity : (x ≡ x)
  [≡]-reflexivity = [∧]-intro [≤]-reflexivity [≤]-reflexivity

  open import Logic.Propositional.Theorems
  [≡]-symmetry : (x ≡ y) → (y ≡ x)
  [≡]-symmetry = [∧]-symmetry

  [≡]-step : (x ≡ y) → (𝐒(x) ≡ 𝐒(y))
  [≡]-step = [∧]-map step step

  open import Relator.Equals renaming (_≡_ to _≡ₑ_)
  [<]-less-than-one : ⦃ ◊ T ⦄ → (x < 𝐒(𝟎)) → (x ≡ₑ 𝟎)
  [<]-less-than-one minimal = [≡]-intro
  [<]-less-than-one (limitₗ p) with () ← p{[◊]-existence}

  [<][≤]-semitransitivityₗ : ⦃ ◊ T ⦄ → (x ≤ y) → (y < z) → (x < z)
  [<][≤]-semitransitivityₗ {_}        {y}        {.(lim _)} xy                 (limitᵣ yz)  = limitᵣ ([<][≤]-semitransitivityₗ xy yz)
  [<][≤]-semitransitivityₗ {.𝟎}       {.𝟎}       {.(𝐒 _)}    minimal            minimal     = minimal
  [<][≤]-semitransitivityₗ {.𝟎}       {.(𝐒 _)}   {.(𝐒 _)}    minimal            (step yz)   = minimal
  [<][≤]-semitransitivityₗ {.𝟎}       {.(lim _)} {.(𝐒 _)}    minimal            (limitₗ x)  = minimal
  [<][≤]-semitransitivityₗ {.(𝐒 _)}   {.(𝐒 _)}   {.(𝐒 _)}    (step xy)          (step yz)   = step ([<][≤]-semitransitivityₗ xy yz)
  [<][≤]-semitransitivityₗ {.(𝐒 _)}   {.(lim _)} {.(𝐒 _)}    (step (limitᵣ xy)) (limitₗ yz) = step ([<][≤]-semitransitivityₗ xy yz)
  [<][≤]-semitransitivityₗ {.(lim _)} {.𝟎}       {.(𝐒 _)}    (limitₗ xy)        minimal     with () ← xy{[◊]-existence}
  [<][≤]-semitransitivityₗ {.(lim _)} {.(𝐒 _)}   {.(𝐒 _)}    (limitₗ xy)        (step yz)   = limitₗ ([<][≤]-semitransitivityₗ xy yz)
  [<][≤]-semitransitivityₗ {.(lim _)} {.(lim _)} {.(𝐒 _)}    (limitₗ xy)        (limitₗ yz) = limitₗ ([<][≤]-semitransitivityₗ ([∃]-proof([<]-limitᵣ-inv xy)) yz)

  [≤]-transitivity : ⦃ ◊ T ⦄ → (x ≤ y) → (y ≤ z) → (x ≤ z)
  [≤]-transitivity = [<][≤]-semitransitivityₗ

  [≡]-transitivity : ⦃ ◊ T ⦄ → (x ≡ y) → (y ≡ z) → (x ≡ z)
  [≡]-transitivity ([∧]-intro yx xy) ([∧]-intro zy yz) = [∧]-intro ([≤]-transitivity zy yx) ([≤]-transitivity xy yz)

  [<][≤]-semitransitivityᵣ : ⦃ ◊ T ⦄ → (x < y) → (y ≤ z) → (x < z)
  [<][≤]-semitransitivityᵣ {.𝟎}       {.(𝐒 𝟎)}       {.(𝐒 _)}   minimal (step minimal)         = minimal
  [<][≤]-semitransitivityᵣ {.𝟎}       {.(𝐒 (𝐒 _))}   {.(𝐒 _)}   minimal (step (step yz))       = minimal
  [<][≤]-semitransitivityᵣ {.𝟎}       {.(𝐒 (lim _))} {.(𝐒 _)}   minimal (step (limitₗ yz))     = minimal
  [<][≤]-semitransitivityᵣ {.𝟎}       {.(𝐒 _)}       {.(lim _)} minimal (step (limitᵣ yz))     = limitᵣ{[◊]-existence} minimal
  [<][≤]-semitransitivityᵣ {.(𝐒 _)}   {.(𝐒 _)}       {𝐒 z}      (step xy) (step yz)            = step ([<][≤]-semitransitivityᵣ xy yz)
  [<][≤]-semitransitivityᵣ {.(𝐒 _)}   {.(𝐒 _)}       {lim z}    (step xy) (step (limitᵣ yz))   = limitᵣ (step ([<][≤]-semitransitivityᵣ xy yz))
  [<][≤]-semitransitivityᵣ {.(lim _)} {.(𝐒 _)}       {𝐒 z}      (limitₗ xy) (step yz)          = limitₗ ([<][≤]-semitransitivityᵣ xy yz)
  [<][≤]-semitransitivityᵣ {.(lim _)} {.(𝐒 _)}       {lim z}    (limitₗ xy) (step (limitᵣ yz)) = limitᵣ ([<][≤]-semitransitivityᵣ (limitₗ xy) (step yz))
  [<][≤]-semitransitivityᵣ {x}        {.(lim _)}     {z}        (limitᵣ xy) (limitₗ yz)        = [<][≤]-semitransitivityᵣ xy (step yz)

  {-
  StrictlyIncreasingSubsequenceExistence : ∀{ℓ}{I : Type{ℓ}} → (I → Ordinal(T)) → Type
  StrictlyIncreasingSubsequenceExistence{I = I} (f) = ∃{Obj = ℕ → I}(g ↦ ∀{n} → (f(g(n)) < f(g(𝐒(n)))))

  -- TODO: Requires some kind of search for T
  StrictlyIncreasingSubsequenceExistence-to-no-maximum : StrictlyIncreasingSubsequenceExistence(f) → ¬ ∃(max ↦ ∀{x} → (f(x) < f(max)))
  StrictlyIncreasingSubsequenceExistence-to-no-maximum ([∃]-intro witness) ([∃]-intro witness₁) = [<]-asymmetry {!!} {!!}
  -}

  {- TODO: Maybe unprovable constructively
  [<]-classical : (x < y) ∨ ¬(x < y)
  [<]-classical {𝟎}     {𝟎}     = [∨]-introᵣ \()
  [<]-classical {𝟎}     {𝐒 y}   = [∨]-introₗ minimal
  [<]-classical {𝟎}     {lim y} = [∨]-introₗ (limitᵣ{𝟎} minimal)
  [<]-classical {𝐒 x}   {𝟎}     = [∨]-introᵣ \()
  [<]-classical {𝐒 x}   {𝐒 y}   = [∨]-elim2 step (_∘ [<]-without-step) ([<]-classical {x} {y})
  [<]-classical {𝐒 x}   {lim y} with [<]-classical {x} {lim y}
  ... | [∨]-introₗ p = {!!}
  ... | [∨]-introᵣ p = {!!}
  [<]-classical {lim x} {𝟎}     = [∨]-introᵣ \()
  [<]-classical {lim x} {𝐒 y}   with [<]-classical {lim x} {y}
  ... | [∨]-introₗ (limitₗ p)          = [∨]-introₗ (limitₗ ([<]-stepᵣ p))
  ... | [∨]-introₗ (limitᵣ (limitₗ p)) = [∨]-introₗ (limitₗ (limitᵣ ([<]-stepᵣ p)))
  ... | [∨]-introᵣ p = [∨]-introᵣ (p ∘ (q ↦ {![<]-limitₗ-inv q!}))
  [<]-classical {lim x} {lim y} = {!!}
  -}

  {- TODO: This is true when there is no maximum for f
  ∀{x} → ∃(y ↦ (x < y) ∧ (f(x) < f(y)))
  test : (x < lim f) → (𝐒(x) < lim f)
  test {𝟎} (limitᵣ minimal) = limitᵣ (step {!!})
  test {𝐒 x} (limitᵣ (step p)) = limitᵣ (step {!!})
  test {lim x} (limitᵣ (limitₗ x₁)) = {!!}
  -}

  {- TODO: Also unprovable constructively?
  f either have a maximum value or is unbounded (so, this would require some kind of search?)

  [<]-sequence-limit : ∀{n} → (f(n) < lim g) → ((∀{n} → (f(n) < lim g)) ∨ (f(n) ≡ x))

  [≤]-total : ⦃ ◊ T ⦄ → ((x ≤ y) ∨ (y ≤ x))
  [≤]-total {𝟎} {_} = [∨]-introₗ minimal
  [≤]-total {_} {𝟎} = [∨]-introᵣ minimal
  [≤]-total {𝐒 x} {𝐒 y} = [∨]-elim2 step step ([≤]-total {x} {y})
  [≤]-total {𝐒 x} {lim y} with [≤]-total {x} {lim y}
  ... | [∨]-introₗ minimal = [∨]-introₗ (step [<]-lim-minimal)
  ... | [∨]-introₗ (step (limitᵣ p)) = [∨]-introₗ (step (limitᵣ (step {!!})))
  ... | [∨]-introₗ (limitₗ p) = [∨]-introₗ (step (limitᵣ (limitₗ (\{n} → {![<]-limitᵣ-inv (p{n})!}))))
  ... | [∨]-introᵣ p = [∨]-introᵣ ([<]-stepᵣ p)
  [≤]-total {lim x} {𝐒 y} = {!!} -- [∨]-symmetry ([≤]-total {𝐒 y} {lim x})
  [≤]-total {lim x} {lim y} = {!!}
  -}

  {-
  [≤]-to-[<][≡] : ⦃ ◊ T ⦄ → (x ≤ y)  → ((x < y) ∨ (x ≡ y))
  [≤]-to-[<][≡] {𝟎}     {𝟎}     minimal    = [∨]-introᵣ ([∧]-intro minimal minimal)
  [≤]-to-[<][≡] {𝟎}     {𝐒 y}   minimal    = [∨]-introₗ minimal
  [≤]-to-[<][≡] {𝟎}     {lim y} minimal    = [∨]-introₗ [<]-lim-minimal
  [≤]-to-[<][≡] {𝐒 x}   {𝐒 y}   (step p)   = [∨]-elim2 step [≡]-step ([≤]-to-[<][≡] {x}{y} p)
  [≤]-to-[<][≡] {𝐒 x} {lim y} (step (limitᵣ p)) with [≤]-to-[<][≡] p
  ... | [∨]-introₗ pp = [∨]-introₗ (limitᵣ (step pp))
  ... | [∨]-introᵣ ([∧]-intro l r) = {!!}
  -- [∨]-introᵣ ([∧]-intro (limitₗ (\{n} → {!!})) (step (limitᵣ r)))
  -- [∨]-elim2 (limitᵣ ∘ step) (\([∧]-intro l r) → [∧]-intro (limitₗ {![<]-stepᵣ l!}) (step (limitᵣ r))) ([≤]-to-[<][≡] p)
  [≤]-to-[<][≡] {lim x} {𝟎}     (limitₗ p) = [∨]-introᵣ ([∧]-intro minimal (limitₗ p))
  [≤]-to-[<][≡] {lim x} {𝐒 y}   (limitₗ p) = {!!}
  [≤]-to-[<][≡] {lim x} {lim y} (limitₗ p) = {!!}

  [<]-trichotomy : ⦃ ◊ T ⦄ → ((x < y) ∨ (x ≡ y) ∨ (x > y))
  [<]-trichotomy {𝟎}     {𝟎}     = [∨]-introₗ ([∨]-introᵣ [≡]-reflexivity)
  [<]-trichotomy {𝟎}     {𝐒 y}   = [∨]-introₗ ([∨]-introₗ minimal)
  [<]-trichotomy {𝟎}     {lim y} = [∨]-introₗ ([∨]-introₗ [<]-lim-minimal)
  [<]-trichotomy {𝐒 x}   {𝟎}     = [∨]-introᵣ minimal
  [<]-trichotomy {lim x} {𝟎}     = [∨]-introᵣ [<]-lim-minimal
  [<]-trichotomy {𝐒 x}   {𝐒 y}   = [∨]-elim2 ([∨]-elim2 step [≡]-step) step ([<]-trichotomy {x}{y})
  [<]-trichotomy {𝐒 x}   {lim y} with [<]-trichotomy {x} {lim y}
  ... | [∨]-introₗ ([∨]-introᵣ ([∧]-intro p _)) = [∨]-introᵣ p
  ... | [∨]-introᵣ p                            = [∨]-introᵣ ([<]-stepᵣ p)
  ... | [∨]-introₗ ([∨]-introₗ (limitᵣ{n} p))   = {!!}
  [<]-trichotomy {lim x} {𝐒 y}   = {!!}
  [<]-trichotomy {lim x} {lim y} = {!!}
  -}

  lim-of-constant : ⦃ ◊ T ⦄ → (lim(const x) ≡ 𝐒(x))
  lim-of-constant = [∧]-intro (step (limitᵣ{[◊]-existence} [<]-of-step)) (limitₗ [<]-of-step)

  lim-of-sequence-with-maximum : ∀{max} → (∀{n} → (f(n) ≤ f(max))) → (lim f ≡ 𝐒(f(max)))
  lim-of-sequence-with-maximum{max = max} p = [∧]-intro (step (limitᵣ{max} [<]-of-step)) (limitₗ p)

  -- ∃(max ↦ (∀{n} → (f(n) ≤ f(max))) ∧ (lim f ≡ 𝐒(f(max)))) ∨ (∀{x} → (𝐒(f(x)) < lim f)) -- or maybe (∀{x y} → (f(x) + f(y) < lim f))

  lim-[≤]-function : (∀{x} → (f(x) ≤ g(x))) → (lim f ≤ lim g)
  lim-[≤]-function p = limitₗ(limitᵣ p)

  lim-function : (∀{x} → (f(x) ≡ g(x))) → (lim f ≡ lim g)
  lim-function p = [∧]-intro (lim-[≤]-function([∧]-elimₗ p)) (lim-[≤]-function([∧]-elimᵣ p))

  [+]-identityᵣ : ((x + 𝟎) ≡ x)
  [+]-identityᵣ = [≡]-reflexivity

  [+]-identityₗ : ((𝟎 + x) ≡ x)
  [+]-identityₗ {𝟎}     = [+]-identityᵣ
  [+]-identityₗ {𝐒 x}   = [≡]-step ([+]-identityₗ {x})
  [+]-identityₗ {lim x} = lim-function [+]-identityₗ

  [+]-associativity : (((x + y) + z) ≡ (x + (y + z)))
  [+]-associativity {x}{y}{𝟎}     = [≡]-reflexivity
  [+]-associativity {x}{y}{𝐒 z}   = [≡]-step ([+]-associativity {x}{y}{z})
  [+]-associativity {x}{y}{lim z} = lim-function ([+]-associativity {x}{y}{_})

  [+]ₗ-[<][≤]-semifunction : (x < y) → ((x + z) ≤ (y + z))
  [+]ₗ-[<][≤]-semifunction {z = 𝟎}     p = [<]-to-[≤] p
  [+]ₗ-[<][≤]-semifunction {z = 𝐒 z}   p = [≤]-step([+]ₗ-[<][≤]-semifunction {z = z} p)
  [+]ₗ-[<][≤]-semifunction {z = lim x} p = limitₗ (limitᵣ ([+]ₗ-[<][≤]-semifunction p))

  [+]ᵣ-[<]-function : ⦃ ◊ T ⦄ → (y < z) → ((x + y) < (x + z))
  [+]ᵣ-[<]-function (minimal {𝟎})     = [<]-of-step
  [+]ᵣ-[<]-function (minimal {𝐒 x})   = [<]-stepᵣ ([+]ᵣ-[<]-function minimal)
  [+]ᵣ-[<]-function (minimal {lim x}) = [<]-stepᵣ (limitᵣ{[◊]-existence} ([+]ᵣ-[<]-function minimal))
  [+]ᵣ-[<]-function (step p)   = step ([+]ᵣ-[<]-function p)
  [+]ᵣ-[<]-function (limitₗ p) = limitₗ ([+]ᵣ-[<]-function p)
  [+]ᵣ-[<]-function (limitᵣ p) = limitᵣ ([+]ᵣ-[<]-function p)

  {-
  [+]-operator : ⦃ ◊ T ⦄ → (x₁ ≡ x₂) → (y₁ ≡ y₂) → ((x₁ + y₁) ≡ (x₂ + y₂))
  [+]-operator ([∧]-intro pxl pxr) ([∧]-intro pyl pyr) = [∧]-intro {!!} {!!} where
    l : (x₁ ≡ x₂) → ((x₁ + y) ≡ (x₂ + y))
    l {𝟎}      {x₂} ([∧]-intro pl pr) = [∧]-intro {!!} {!!}
    l {𝐒 x₁}   {x₂} ([∧]-intro pl pr) = [∧]-intro {!!} {!!}
    l {lim x₁} {x₂} ([∧]-intro pl pr) = [∧]-intro {!!} {!!}

    r : (y₁ ≡ y₂) → ((x + y₁) ≡ (x + y₂))
    r ([∧]-intro pl pr) = [∧]-intro ([+]ᵣ-[<]-function pl) ([+]ᵣ-[<]-function pr)
  -}

  open import Structure.Relator.Ordering
  open        Structure.Relator.Ordering.Strict.Properties using (intro)

  Ordinal-accessibleₗ : ⦃ ◊ T ⦄ → Strict.Properties.Accessibleₗ(_<_)(x)
  Ordinal-accessibleₗ {n} = intro ⦃ proof{n} ⦄ where
    proof : ∀{y x} → ⦃ _ : (x < y) ⦄ → Strict.Properties.Accessibleₗ(_<_)(x)
    proof {_}        {𝟎}                          = intro ⦃ \ ⦃ ⦄ ⦄
    proof {𝐒 𝟎}      {lim y} ⦃ limitₗ p ⦄         with () ← p{[◊]-existence}
    proof {𝐒 x}      {𝐒 y}   ⦃ step p ⦄           = intro ⦃ \{z} ⦃ pz ⦄ → Strict.Properties.Accessibleₗ.proof (Ordinal-accessibleₗ {x}) ⦃ [<][≤]-semitransitivityₗ pz p ⦄ ⦄
    proof {𝐒(𝐒 x)}   {lim y} ⦃ limitₗ p ⦄         = intro ⦃ \{z} ⦃ pz ⦄ → Strict.Properties.Accessibleₗ.proof (Ordinal-accessibleₗ {𝐒 x}) ⦃ [<][≤]-semitransitivityₗ ([∃]-proof([<]-limitᵣ-inv pz)) p ⦄ ⦄
    proof {𝐒(lim x)} {lim y} ⦃ limitₗ p ⦄         = intro ⦃ \{z} ⦃ pz ⦄ → Strict.Properties.Accessibleₗ.proof (Ordinal-accessibleₗ {lim x}) ⦃ [<][≤]-semitransitivityₗ ([∃]-proof([<]-limitᵣ-inv pz)) p ⦄ ⦄
    proof {lim x}    {𝐒 y}   ⦃ limitᵣ(step p) ⦄   = intro ⦃ \{z} ⦃ pz ⦄ → Strict.Properties.Accessibleₗ.proof Ordinal-accessibleₗ ⦃ [<][≤]-semitransitivityₗ pz p ⦄ ⦄
    proof {lim x}    {lim y} ⦃ limitᵣ(limitₗ p) ⦄ = intro ⦃ \{z} ⦃ pz ⦄ → Strict.Properties.Accessibleₗ.proof Ordinal-accessibleₗ ⦃ [<][≤]-semitransitivityₗ ([∃]-proof([<]-limitᵣ-inv pz)) p ⦄ ⦄

module _ where
  open import Functional
  open import Function.Iteration
  open import Numeral.Natural.Induction

  private variable n : ℕ

  _⋅ₙ_ : Ordinal(ℕ) → ℕ → Ordinal(ℕ)
  _⋅ₙ_ x = ℕ-elim 𝟎 (const(lim ∘ (_+ₙ_)))

  ω : Ordinal(ℕ)
  ω = lim from-ℕ

  ω² : Ordinal(ℕ)
  ω² = lim(ω ⋅ₙ_)

  ω-[<]-correctness : from-ℕ(n) < ω
  ω-[<]-correctness {𝟎}    = limitᵣ{i = 𝟎}    minimal
  ω-[<]-correctness {𝐒(n)} = limitᵣ{i = 𝐒(n)} (step [<]-of-step)

  open import Relator.Equals renaming (_≡_ to _≡ₑ_)
  open import Relator.Equals.Proofs
  open import Type.Properties.Inhabited
  open import Structure.Relator

  private variable f : ℕ → Ordinal(ℕ)

  instance
    ℕ-inhabited : ◊ ℕ
    ℕ-inhabited = intro ⦃ 𝟎 ⦄

  strictly-increasing-sequence-when-zero : (∀{n} → (f(n) < f(𝐒(n)))) → (f(n) ≡ₑ 𝟎) → (n ≡ₑ 𝟎)
  strictly-increasing-sequence-when-zero {f = f}{n = 𝟎} ord p = [≡]-intro
  strictly-increasing-sequence-when-zero {f = f}{n = 𝐒 n} ord p with f(n) | ord{n}
  ... | 𝟎     | ord' with () ← [<]-irreflexivity (substitute₂ᵣ(_<_) p ord')
  ... | 𝐒 fn  | ord' with () ← [<]-asymmetry minimal (substitute₂ᵣ(_<_) p ord')
  ... | lim x | ord' with () ← [<]-asymmetry [<]-lim-minimal (substitute₂ᵣ(_<_) p ord')

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
record ∃ {A : Set} (B : A → Set) : Set where
  field
    fst : A
    snd : B fst

data ⊥ : Set where

infix 3 ¬_

¬_ : Set → Set
¬ P = P → ⊥

infixr 1 _⊎_

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

⊎-map : ∀ {A₁ A₂ B₁ B₂ : Set} →
        (A₁ → A₂) → (B₁ → B₂) → A₁ ⊎ B₁ → A₂ ⊎ B₂
⊎-map f g (inj₁ x) = inj₁ (f x)
⊎-map f g (inj₂ y) = inj₂ (g y)

record Raw-monad (M : Set → Set) : Set₁ where
  constructor mk
  infixl 5 _>>=_
  field
    return : ∀ {A} → A → M A
    _>>=_  : ∀ {A B} → M A → (A → M B) → M B

  map : ∀ {A B} → (A → B) → M A → M B
  map f x = x >>= λ x → return (f x)

open Raw-monad ⦃ … ⦄

-- Id is included in order to make run overloaded.

record Id (A : Set) : Set where
  field
    run : A

open Id

infix 3 ¬¬_

record ¬¬_ (A : Set) : Set where
  field
    run : ¬ ¬ A

open ¬¬_

instance

  double-negation-monad : Raw-monad ¬¬_
  run (Raw-monad.return double-negation-monad x)   = λ f → f x
  run (Raw-monad._>>=_  double-negation-monad x f) =
    λ ¬b → run x (λ a → run (f a) ¬b)

excluded-middle : {A : Set} → ¬¬ (A ⊎ ¬ A)
run excluded-middle ¬[a⊎¬a] = ¬[a⊎¬a] (inj₂ λ a → ¬[a⊎¬a] (inj₁ a))

postulate

  A    : Set
  P    : Set → Set
  _⇓_  : P A → A → Set
  _⇑   : P A → Set
  ¬⇓→⇑ : {x : P A} → ¬ (∃ λ y → x ⇓ y) → x ⇑

¬¬[⇓⊎⇑] : (x : P A) → ¬ ¬ ((∃ λ y → x ⇓ y) ⊎ x ⇑)
¬¬[⇓⊎⇑] x = run (map (⊎-map (λ x → x) ¬⇓→⇑) excluded-middle)


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

module Summary where

import Cubical.Data.Nat using (ℕ)
open import Cubical.Foundations.Prelude using (Lift; refl)
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Unit.Base using (Unit)
open import Cubical.Data.Sigma.Base

infix 1 _≅_
_≅_ = Iso

open import Number.Postulates
open import Number.Base
open import Number.Prettyprint

open ℕⁿ
open ℤᶻ
open ℚᶠ
open ℝʳ
open ℂᶜ

number-≅-Σ : ∀{p} → Number p ≅ NumberInterpretation p
number-≅-Σ = λ where
  .Iso.fun               → pop
  .Iso.inv      (x ,  p) → x ,, p
  .Iso.leftInv  (x ,, p) → refl
  .Iso.rightInv (x ,  p) → refl

iso00 : [ℕ]   ≅ Σ[ x ∈ Cubical.Data.Nat.ℕ ] Unit
iso01 : [ℕ⁺⁻] ≅ Σ[ x ∈ Cubical.Data.Nat.ℕ ] x  #ⁿ 0ⁿ
iso02 : [ℕ₀⁺] ≅ Σ[ x ∈ Cubical.Data.Nat.ℕ ] 0ⁿ ≤ⁿ x
iso03 : [ℕ⁺]  ≅ Σ[ x ∈ Cubical.Data.Nat.ℕ ] 0ⁿ <ⁿ x
iso04 : [ℕ₀⁻] ≅ Σ[ x ∈ Cubical.Data.Nat.ℕ ] x  ≤ⁿ 0ⁿ
iso05 : [ℤ]   ≅ Σ[ x ∈ ℤ.Carrier          ] Lift {j = ℤℓ'} Unit
iso06 : [ℤ⁺⁻] ≅ Σ[ x ∈ ℤ.Carrier          ] x  #ᶻ 0ᶻ
iso07 : [ℤ₀⁺] ≅ Σ[ x ∈ ℤ.Carrier          ] 0ᶻ ≤ᶻ x
iso08 : [ℤ⁺]  ≅ Σ[ x ∈ ℤ.Carrier          ] 0ᶻ <ᶻ x
iso09 : [ℤ⁻]  ≅ Σ[ x ∈ ℤ.Carrier          ] x  <ᶻ 0ᶻ
iso10 : [ℤ₀⁻] ≅ Σ[ x ∈ ℤ.Carrier          ] x  ≤ᶻ 0ᶻ
iso11 : [ℚ]   ≅ Σ[ x ∈ ℚ.Carrier          ] Lift {j = ℚℓ'} Unit
iso12 : [ℚ⁺⁻] ≅ Σ[ x ∈ ℚ.Carrier          ] x  #ᶠ 0ᶠ
iso13 : [ℚ₀⁺] ≅ Σ[ x ∈ ℚ.Carrier          ] 0ᶠ ≤ᶠ x
iso14 : [ℚ⁺]  ≅ Σ[ x ∈ ℚ.Carrier          ] 0ᶠ <ᶠ x
iso15 : [ℚ⁻]  ≅ Σ[ x ∈ ℚ.Carrier          ] x  <ᶠ 0ᶠ
iso16 : [ℚ₀⁻] ≅ Σ[ x ∈ ℚ.Carrier          ] x  ≤ᶠ 0ᶠ
iso17 : [ℝ]   ≅ Σ[ x ∈ ℝ.Carrier          ] Lift {j = ℝℓ'} Unit
iso18 : [ℝ⁺⁻] ≅ Σ[ x ∈ ℝ.Carrier          ] x  #ʳ 0ʳ
iso19 : [ℝ₀⁺] ≅ Σ[ x ∈ ℝ.Carrier          ] 0ʳ ≤ʳ x
iso20 : [ℝ⁺]  ≅ Σ[ x ∈ ℝ.Carrier          ] 0ʳ <ʳ x
iso21 : [ℝ⁻]  ≅ Σ[ x ∈ ℝ.Carrier          ] x  <ʳ 0ʳ
iso22 : [ℝ₀⁻] ≅ Σ[ x ∈ ℝ.Carrier          ] x  ≤ʳ 0ʳ
iso23 : [ℂ]   ≅ Σ[ x ∈ ℂ.Carrier          ] Lift {j = ℂℓ'} Unit
iso24 : [ℂ⁺⁻] ≅ Σ[ x ∈ ℂ.Carrier          ] x  #ᶜ 0ᶜ

iso00 = number-≅-Σ
iso01 = number-≅-Σ
iso02 = number-≅-Σ
iso03 = number-≅-Σ
iso04 = number-≅-Σ
iso05 = number-≅-Σ
iso06 = number-≅-Σ
iso07 = number-≅-Σ
iso08 = number-≅-Σ
iso09 = number-≅-Σ
iso10 = number-≅-Σ
iso11 = number-≅-Σ
iso12 = number-≅-Σ
iso13 = number-≅-Σ
iso14 = number-≅-Σ
iso15 = number-≅-Σ
iso16 = number-≅-Σ
iso17 = number-≅-Σ
iso18 = number-≅-Σ
iso19 = number-≅-Σ
iso20 = number-≅-Σ
iso21 = number-≅-Σ
iso22 = number-≅-Σ
iso23 = number-≅-Σ
iso24 = number-≅-Σ

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
open import Agda.Builtin.Equality

postulate
  A         : Set
  F G H I J : (A : Set₁) → (A → A → Set) → Set
  K         : ⦃ Set → Set → Set ⦄ → { Set → Set → Set } → Set

syntax F A (λ x y → B)               = y ⟨ A ∼ B ⟩₁ x
syntax G A (λ _ y → B)               = y ⟨ A ∼ B ⟩₂
syntax H A (λ x _ → B)               =   ⟨ B ∼ A ⟩₃ x
syntax I A (λ _ _ → B)               =   ⟨ B ∼ A ⟩₄
syntax J A (λ x y → B)               = x y ∶ A ↝ B
syntax K ⦃ λ A B → C ⦄ { λ D E → F } = A B C - D E F

_ : (P ⟨ (Set → Set) ∼ P (Q A) ⟩₁ Q) ≡ F (Set → Set) (λ F G → G (F A))
_ = refl

_ : (P ⟨ (Set → Set) ∼ P A ⟩₂) ≡ G (Set → Set) (λ _ G → G A)
_ = refl

_ : (⟨ Q A ∼ (Set → Set) ⟩₃ Q) ≡ H (Set → Set) (λ F _ → F A)
_ = refl

_ : (⟨ A ∼ (Set → Set) ⟩₄) ≡ I (Set → Set) (λ _ _ → A)
_ = refl

_ : (P Q ∶ (Set → Set) ↝ P (Q A)) ≡ J (Set → Set) (λ F G → F (G A))
_ = refl

_ : (x x x - x x x) ≡ K ⦃ λ _ x → x ⦄ { λ _ y → y }
_ = refl


text:
module Generic.Lib.Data.Sets where

open import Generic.Lib.Intro
open import Generic.Lib.Data.Nat
open import Generic.Lib.Data.Product
open import Generic.Lib.Data.Pow

infixl 6 _⊔ⁿ_

_⊔ⁿ_ : ∀ {n} -> Level ^ n -> Level -> Level
_⊔ⁿ_ = flip $ foldPow _ _⊔_

Sets : ∀ {n} -> (αs : Level ^ n) -> Set (mapPow lsuc αs ⊔ⁿ lzero)
Sets {0}      _       = ⊤
Sets {suc _} (α , αs) = Set α × Sets αs

FoldSets : ∀ {n β αs} -> Sets {n} αs -> Set β -> Set (αs ⊔ⁿ β)
FoldSets {0}      tt      B = B
FoldSets {suc _} (A , As) B = A -> FoldSets As B

HList : ∀ {n} {αs} -> Sets {n} αs -> Set (αs ⊔ⁿ lzero)
HList {0}      tt      = ⊤
HList {suc _} (A , As) = A × HList As

applyFoldSets : ∀ {n β αs} {As : Sets {n} αs} {B : Set β} -> FoldSets As B -> HList As -> B
applyFoldSets {0}     y  tt      = y
applyFoldSets {suc n} f (x , xs) = applyFoldSets (f x) xs

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module Prelude.List.Relations.Properties where

open import Agda.Primitive

open import Prelude.Equality
open import Prelude.Nat
open import Prelude.Empty
open import Prelude.Unit
open import Prelude.Product
open import Prelude.Number
open import Prelude.Decidable
open import Prelude.List.Base

open import Prelude.List.Relations.All
open import Prelude.List.Relations.Any

open import Prelude.Nat.Properties
open import Prelude.Variables

open import Prelude.Applicative

-- All --

module _ {a b} {A : Set a} {P Q : A → Set b} (f : ∀ {x} → P x → Q x) where
  mapAll : ∀ {xs} → All P xs → All Q xs
  mapAll [] = []
  mapAll (x ∷ xs) = f x ∷ mapAll xs

traverseAll : ∀ {a b} {A : Set a} {B : A → Set a} {F : Set a → Set b}
                {{AppF : Applicative F}} →
                (∀ x → F (B x)) → (xs : List A) → F (All B xs)
traverseAll f []       = pure []
traverseAll f (x ∷ xs) = ⦇ f x ∷ traverseAll f xs ⦈

module _ {a b} {A : Set a} {P : A → Set b} where

  -- Append

  infixr 5 _++All_
  _++All_ : ∀ {xs ys} → All P xs → All P ys → All P (xs ++ ys)
  []       ++All qs = qs
  (p ∷ ps) ++All qs = p ∷ ps ++All qs

-- Any --

module _ {a b} {A : Set a} {P Q : A → Set b} (f : ∀ {x} → P x → Q x) where
  mapAny : ∀ {xs} → Any P xs → Any Q xs
  mapAny (zero x) = zero (f x)
  mapAny (suc i)  = suc (mapAny i)

-- Literal overloading for Any
module _ {a b} {A : Set a} {P : A → Set b} where
  private
    AnyConstraint : List A → Nat → Set (a ⊔ b)
    AnyConstraint []        _      = ⊥′
    AnyConstraint (x ∷  _)  zero   = ⊤′ {a} × P x   -- hack to line up levels
    AnyConstraint (_ ∷ xs) (suc i) = AnyConstraint xs i

    natToIx : ∀ (xs : List A) n → {{_ : AnyConstraint xs n}} → Any P xs
    natToIx [] n {{}}
    natToIx (x ∷ xs)  zero {{_ , px}} = zero px
    natToIx (x ∷ xs) (suc n) = suc (natToIx xs n)

  instance
    NumberAny : ∀ {xs} → Number (Any P xs)
    Number.Constraint (NumberAny {xs}) = AnyConstraint xs
    fromNat {{NumberAny {xs}}} = natToIx xs

lookupAny : ∀ {a b} {A : Set a} {P Q : A → Set b} {xs} → All P xs → Any Q xs → Σ A (λ x → P x × Q x)
lookupAny (p ∷ ps) (zero q) = _ , p , q
lookupAny (p ∷ ps) (suc  i) = lookupAny ps i

lookup∈ : ∀ {a b} {A : Set a} {P : A → Set b} {xs x} → All P xs → x ∈ xs → P x
lookup∈ (p ∷ ps) (zero refl) = p
lookup∈ (p ∷ ps) (suc i)     = lookup∈ ps i

module _ {a b} {A : Set a} {P : A → Set b} {{EqP : ∀ {x} → Eq (P x)}} where

  private
    z' : ∀ {x xs} → P x → Any P (x ∷ xs)
    z' = zero

    zero-inj : ∀ {x} {xs : List A} {p q : P x} → Any.zero {xs = xs} p ≡ z' q → p ≡ q
    zero-inj refl = refl

    sucAny-inj : ∀ {x xs} {i j : Any P xs} → Any.suc {x = x} i ≡ Any.suc {x = x} j → i ≡ j
    sucAny-inj refl = refl

    cons-inj₁ : ∀ {x xs} {p q : P x} {ps qs : All P xs} → p All.∷ ps ≡ q ∷ qs → p ≡ q
    cons-inj₁ refl = refl

    cons-inj₂ : ∀ {x xs} {p q : P x} {ps qs : All P xs} → p All.∷ ps ≡ q ∷ qs → ps ≡ qs
    cons-inj₂ refl = refl

  instance
    EqAny : ∀ {xs} → Eq (Any P xs)
    _==_ {{EqAny}} (zero p) (zero q) = decEq₁ zero-inj   (p == q)
    _==_ {{EqAny}} (suc i)  (suc j)  = decEq₁ sucAny-inj (i == j)
    _==_ {{EqAny}} (zero _) (suc _)  = no λ ()
    _==_ {{EqAny}} (suc _)  (zero _) = no λ ()

    EqAll : ∀ {xs} → Eq (All P xs)
    _==_ {{EqAll}} []       []       = yes refl
    _==_ {{EqAll}} (x ∷ xs) (y ∷ ys) = decEq₂ cons-inj₁ cons-inj₂ (x == y) (xs == ys)

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


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

module Algebra.Linear.Structures where

open import Algebra.Structures.Field public
open import Algebra.Linear.Structures.VectorSpace public

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
module _ (A : Set) where

{-# POLARITY A #-}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
module Lvl.MultiFunctions where

open import Data
open import Data.Tuple
open import Data.Tuple.Raise
import      Data.Tuple.Raiseᵣ.Functions as Raise
open import Lvl

-- The maximum level of a tuple list of levels.
⨆ : ∀{n} → (Level ^ n) → Level
⨆ = Raise.foldᵣ(_⊔_) 𝟎