text:
------------------------------------------------------------------------
-- Properties satisfied by total orders
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Props.TotalOrder (t : TotalOrder) where

open Relation.Binary.TotalOrder t
open import Relation.Binary.Consequences

decTotalOrder : Decidable _≈_ → DecTotalOrder
decTotalOrder ≟ = record
  { isDecTotalOrder = record
      { isTotalOrder = isTotalOrder
      ; _≟_          = ≟
      ; _≤?_         = total+dec⟶dec reflexive antisym total ≟
      }
  }

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module Slides where

import Background
import OpenTheory
import OpenTheory2
import ClosedTheory
import ClosedTheory2
import ClosedTheory3
import ClosedTheory4

ext: agda

max_stars_repo_name: larrytheliquid/generic-elim

max_issues_repo_name: larrytheliquid/generic-elim

max_forks_repo_name: larrytheliquid/generic-elim


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

open import Data.Nat using (ℕ)

module Categories.Category.Construction.Fin (n : ℕ) where

open import Level
open import Data.Fin.Properties

open import Categories.Category
open import Categories.Category.Construction.Thin 0ℓ (≤-poset n)

Fin : Category 0ℓ 0ℓ 0ℓ
Fin = Thin

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2016-12-09, issue #2331
-- Testcase from Nisse's application

open import Common.Size

data D (i : Size) : Set where
  c : (j : Size< i) → D i

postulate
  f : (i : Size) → ((j : Size< i) → D j → Set) → Set

module Mutual where
  mutual
    test : (i : Size) → D i → Set
    test  i (c j) = f j (helper i j)

    helper : (i : Size) (j : Size< i) (k : Size< j) → D k → Set
    helper i j k = test k

module Where where
  test : (i : Size) → D i → Set
  test i (c j) = f j helper
    where
    helper : (k : Size< j) → D k → Set
    helper k = test k

-- While k is an unusable size per se, in combination with the usable size j
-- (which comes from a inductive pattern match)
-- it should be fine to certify termination.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The torus, defined as a HIT
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- This module is based on the discussion of the torus in the HoTT
-- book.

-- The module is parametrised by a notion of equality. The higher
-- constructors of the HIT defining the torus use path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

module Torus
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Circle eq as Circle using (𝕊¹; base; loopᴾ)

private
  variable
    a p : Level
    A   : Type a
    P   : A → Type p

------------------------------------------------------------------------
-- The torus

mutual

  -- The torus.

  data T² : Type where
    base hub      : T²
    loop₁ᴾ loop₂ᴾ : base P.≡ base
    spokeᴾ        : (x : 𝕊¹) → rimᴾ x P.≡ hub

  private

    -- A synonym used to work around an Agda restriction.

    base′ = base

  -- A function used to define the spoke constructor.
  --
  -- Note that this function is defined using Circle.recᴾ, not
  -- Circle.rec.

  rimᴾ : 𝕊¹ → T²
  rimᴾ = Circle.recᴾ base loop₁₂₋₁₋₂ᴾ

  -- A loop.

  loop₁₂₋₁₋₂ᴾ : base′ P.≡ base′
  loop₁₂₋₁₋₂ᴾ =
    base  P.≡⟨ loop₁ᴾ ⟩
    base  P.≡⟨ loop₂ᴾ ⟩
    base  P.≡⟨ P.sym loop₁ᴾ ⟩
    base  P.≡⟨ P.sym loop₂ᴾ ⟩∎
    base  ∎

-- The constructors (and loop₁₂₋₁₋₂ᴾ) expressed using _≡_ instead of
-- paths.

loop₁ : base ≡ base
loop₁ = _↔_.from ≡↔≡ loop₁ᴾ

loop₂ : base ≡ base
loop₂ = _↔_.from ≡↔≡ loop₂ᴾ

loop₁₂₋₁₋₂ : base ≡ base
loop₁₂₋₁₋₂ = _↔_.from ≡↔≡ loop₁₂₋₁₋₂ᴾ

spoke : (x : 𝕊¹) → rimᴾ x ≡ hub
spoke = _↔_.from ≡↔≡ ∘ spokeᴾ

-- A variant of rimᴾ, defined using Circle.rec and loop₁₂₋₁₋₂.

rim : 𝕊¹ → T²
rim = Circle.rec base loop₁₂₋₁₋₂

-- The functions rim and rimᴾ are pointwise equal.

rim≡rimᴾ : ∀ x → rim x ≡ rimᴾ x
rim≡rimᴾ = Circle.elim
  _
  (refl _)
  (subst (λ x → rim x ≡ rimᴾ x) Circle.loop (refl _)           ≡⟨ subst-in-terms-of-trans-and-cong ⟩

   trans (sym (cong rim Circle.loop))
     (trans (refl _) (cong rimᴾ Circle.loop))                  ≡⟨ cong (trans _) $ trans-reflˡ _ ⟩

   trans (sym (cong rim Circle.loop)) (cong rimᴾ Circle.loop)  ≡⟨ cong₂ (trans ∘ sym) Circle.rec-loop lemma ⟩

   trans (sym loop₁₂₋₁₋₂) loop₁₂₋₁₋₂                           ≡⟨ trans-symˡ _ ⟩∎

   refl _                                                      ∎)
   where
   lemma =
     cong rimᴾ Circle.loop             ≡⟨ cong≡cong ⟩
     _↔_.from ≡↔≡ (P.cong rimᴾ loopᴾ)  ≡⟨⟩
     _↔_.from ≡↔≡ loop₁₂₋₁₋₂ᴾ          ≡⟨⟩
     loop₁₂₋₁₋₂                        ∎

------------------------------------------------------------------------
-- Eliminators expressed using paths

-- A dependent eliminator, expressed using paths.

record Elimᴾ₀ (P : T² → Type p) : Type p where
  no-eta-equality
  field
    baseʳ  : P base
    loop₁ʳ : P.[ (λ i → P (loop₁ᴾ i)) ] baseʳ ≡ baseʳ
    loop₂ʳ : P.[ (λ i → P (loop₂ᴾ i)) ] baseʳ ≡ baseʳ

  -- A dependent path.

  loop₁₂₋₁₋₂ʳ : P.[ (λ i → P (loop₁₂₋₁₋₂ᴾ i)) ] baseʳ ≡ baseʳ
  loop₁₂₋₁₋₂ʳ =
    baseʳ  P.≡⟨        loop₁ʳ ⟩[ P ]
    baseʳ  P.≡⟨        loop₂ʳ ⟩[ P ]
    baseʳ  P.≡⟨ P.hsym loop₁ʳ ⟩[ P ]
    baseʳ  P.≡⟨ P.hsym loop₂ʳ ⟩∎h
    baseʳ  ∎

  -- A special case of elimᴾ, used in the type of elimᴾ.

  elimᴾ-rimᴾ : (x : 𝕊¹) → P (rimᴾ x)
  elimᴾ-rimᴾ = Circle.elimᴾ (P ∘ rimᴾ) baseʳ loop₁₂₋₁₋₂ʳ

record Elimᴾ (P : T² → Type p) : Type p where
  no-eta-equality
  field
    elimᴾ₀ : Elimᴾ₀ P

  open Elimᴾ₀ elimᴾ₀ public

  field
    hubʳ   : P hub
    spokeʳ : (x : 𝕊¹) → P.[ (λ i → P (spokeᴾ x i)) ] elimᴾ-rimᴾ x ≡ hubʳ

elimᴾ : Elimᴾ P → (x : T²) → P x
elimᴾ {P = P} e = helper
  where
  module E = Elimᴾ e

  helper : (x : T²) → P x
  helper = λ where
    base                 → E.baseʳ
    hub                  → E.hubʳ
    (loop₁ᴾ i)           → E.loop₁ʳ i
    (loop₂ᴾ i)           → E.loop₂ʳ i
    (spokeᴾ base i)      → E.spokeʳ base i
    (spokeᴾ (loopᴾ j) i) → E.spokeʳ (loopᴾ j) i

-- The special case is a special case.

elimᴾ-rimᴾ≡elimᴾ-rimᴾ :
  (e : Elimᴾ P) (x : 𝕊¹) → elimᴾ e (rimᴾ x) ≡ Elimᴾ.elimᴾ-rimᴾ e x
elimᴾ-rimᴾ≡elimᴾ-rimᴾ _ = Circle.elimᴾ _ (refl _) (λ _ → refl _)

-- A non-dependent eliminator, expressed using paths.

Recᴾ : Type a → Type a
Recᴾ A = Elimᴾ (λ _ → A)

recᴾ : Recᴾ A → T² → A
recᴾ = elimᴾ

------------------------------------------------------------------------
-- Eliminators

-- A dependent eliminator.

record Elim (P : T² → Type p) : Type p where
  no-eta-equality
  field
    baseʳ  : P base
    loop₁ʳ : subst P loop₁ baseʳ ≡ baseʳ
    loop₂ʳ : subst P loop₂ baseʳ ≡ baseʳ

  -- An instance of Elimᴾ₀ P.

  elimᴾ₀ : Elimᴾ₀ P
  elimᴾ₀ = λ where
    .Elimᴾ₀.baseʳ  → baseʳ
    .Elimᴾ₀.loop₁ʳ → subst≡→[]≡ loop₁ʳ
    .Elimᴾ₀.loop₂ʳ → subst≡→[]≡ loop₂ʳ

  -- A special case of elim, used in the type of elim.

  elim-rimᴾ : (x : 𝕊¹) → P (rimᴾ x)
  elim-rimᴾ = Elimᴾ₀.elimᴾ-rimᴾ elimᴾ₀

  field
    hubʳ   : P hub
    spokeʳ : (x : 𝕊¹) → subst P (spoke x) (elim-rimᴾ x) ≡ hubʳ

  -- The eliminator.

  elim : (x : T²) → P x
  elim = elimᴾ λ where
    .Elimᴾ.elimᴾ₀ → elimᴾ₀
    .Elimᴾ.hubʳ   → hubʳ
    .Elimᴾ.spokeʳ → subst≡→[]≡ ∘ spokeʳ

  -- The special case is a special case.

  elim-rimᴾ≡elim-rimᴾ : (x : 𝕊¹) → elim (rimᴾ x) ≡ elim-rimᴾ x
  elim-rimᴾ≡elim-rimᴾ = elimᴾ-rimᴾ≡elimᴾ-rimᴾ _

  -- A variant of spokeʳ with a slightly different type.

  spokeʳ′ : (x : 𝕊¹) → subst P (spoke x) (elim (rimᴾ x)) ≡ hubʳ
  spokeʳ′ = Circle.elimᴾ _ (spokeʳ base) (λ i → spokeʳ (loopᴾ i))

  -- Computation rules.

  elim-loop₁ : dcong elim loop₁ ≡ loop₁ʳ
  elim-loop₁ = dcong-subst≡→[]≡ (refl _)

  elim-loop₂ : dcong elim loop₂ ≡ loop₂ʳ
  elim-loop₂ = dcong-subst≡→[]≡ (refl _)

  elim-spoke : (x : 𝕊¹) → dcong elim (spoke x) ≡ spokeʳ′ x
  elim-spoke = Circle.elimᴾ _
    (dcong-subst≡→[]≡ (refl _))
    (λ _ → dcong-subst≡→[]≡ (refl _))

-- A non-dependent eliminator.

record Rec (A : Type a) : Type a where
  no-eta-equality
  field
    baseʳ  : A
    loop₁ʳ : baseʳ ≡ baseʳ
    loop₂ʳ : baseʳ ≡ baseʳ

  -- An instance of Elimᴾ₀ P.

  elimᴾ₀ : Elimᴾ₀ (λ _ → A)
  elimᴾ₀ = λ where
    .Elimᴾ₀.baseʳ  → baseʳ
    .Elimᴾ₀.loop₁ʳ → _↔_.to ≡↔≡ loop₁ʳ
    .Elimᴾ₀.loop₂ʳ → _↔_.to ≡↔≡ loop₂ʳ

  -- A special case of recᴾ, used in the type of rec.

  rec-rimᴾ : 𝕊¹ → A
  rec-rimᴾ = Elimᴾ₀.elimᴾ-rimᴾ elimᴾ₀

  field
    hubʳ   : A
    spokeʳ : (x : 𝕊¹) → rec-rimᴾ x ≡ hubʳ

  -- The eliminator.

  rec : T² → A
  rec = recᴾ λ where
    .Elimᴾ.elimᴾ₀ → elimᴾ₀
    .Elimᴾ.hubʳ   → hubʳ
    .Elimᴾ.spokeʳ → _↔_.to ≡↔≡ ∘ spokeʳ

  -- The special case is a special case.

  rec-rimᴾ≡rec-rimᴾ : (x : 𝕊¹) → rec (rimᴾ x) ≡ rec-rimᴾ x
  rec-rimᴾ≡rec-rimᴾ = elimᴾ-rimᴾ≡elimᴾ-rimᴾ _

  -- A variant of spokeʳ with a slightly different type.

  spokeʳ′ : (x : 𝕊¹) → rec (rimᴾ x) ≡ hubʳ
  spokeʳ′ = Circle.elimᴾ _ (spokeʳ base) (λ i → spokeʳ (loopᴾ i))

  -- Computation rules.

  rec-loop₁ : cong rec loop₁ ≡ loop₁ʳ
  rec-loop₁ = cong-≡↔≡ (refl _)

  rec-loop₂ : cong rec loop₂ ≡ loop₂ʳ
  rec-loop₂ = cong-≡↔≡ (refl _)

  rec-spoke : (x : 𝕊¹) → cong rec (spoke x) ≡ spokeʳ′ x
  rec-spoke = Circle.elimᴾ _
    (cong-≡↔≡ (refl _))
    (λ _ → cong-≡↔≡ (refl _))

------------------------------------------------------------------------
-- Some lemmas

-- The remaining results are not taken from the HoTT book.

-- One can express loop₁₂₋₁₋₂ using loop₁ and loop₂.

loop₁₂₋₁₋₂≡ :
  loop₁₂₋₁₋₂ ≡ trans (trans loop₁ loop₂) (sym (trans loop₂ loop₁))
loop₁₂₋₁₋₂≡ =
  _↔_.from ≡↔≡ loop₁₂₋₁₋₂ᴾ                                        ≡⟨⟩

  _↔_.from ≡↔≡
    (P.trans loop₁ᴾ (P.trans loop₂ᴾ
                       (P.trans (P.sym loop₁ᴾ) (P.sym loop₂ᴾ))))  ≡⟨ sym trans≡trans ⟩

  trans loop₁
    (_↔_.from ≡↔≡ (P.trans loop₂ᴾ
                     (P.trans (P.sym loop₁ᴾ) (P.sym loop₂ᴾ))))    ≡⟨ cong (trans _) $ sym trans≡trans ⟩

  trans loop₁
    (trans loop₂
       (_↔_.from ≡↔≡ (P.trans (P.sym loop₁ᴾ) (P.sym loop₂ᴾ))))    ≡⟨ cong (λ eq → trans loop₁ (trans loop₂ eq)) $ sym trans≡trans ⟩

  trans loop₁
    (trans loop₂
       (trans (_↔_.from ≡↔≡ (P.sym loop₁ᴾ))
          (_↔_.from ≡↔≡ (P.sym loop₂ᴾ))))                         ≡⟨ cong₂ (λ p q → trans loop₁ (trans loop₂ (trans p q)))
                                                                       (sym sym≡sym)
                                                                       (sym sym≡sym) ⟩

  trans loop₁ (trans loop₂ (trans (sym loop₁) (sym loop₂)))       ≡⟨ sym $ trans-assoc _ _ _ ⟩

  trans (trans loop₁ loop₂) (trans (sym loop₁) (sym loop₂))       ≡⟨ cong (trans _) $ sym $ sym-trans _ _ ⟩∎

  trans (trans loop₁ loop₂) (sym (trans loop₂ loop₁))             ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Builtin.Float where

open import Prelude
open import Prelude.Equality.Unsafe

open import Agda.Builtin.Float
open Agda.Builtin.Float public using (Float)

natToFloat : Nat → Float
natToFloat = primNatToFloat

intToFloat : Int → Float
intToFloat (pos    x) = natToFloat x
intToFloat (negsuc x) = primFloatMinus -1.0 (natToFloat x)

instance
  EqFloat : Eq Float
  _==_ {{EqFloat}} x y with primFloatEquality x y
  ... | true  = yes unsafeEqual
  ... | false = no  unsafeNotEqual

data LessFloat (x y : Float) : Set where
  less-float : primFloatLess x y ≡ true → LessFloat x y

instance
  OrdFloat : Ord Float
  OrdFloat = defaultOrd cmpFloat
    where
      cmpFloat : ∀ x y → Comparison LessFloat x y
      cmpFloat x y with inspect (primFloatLess x y)
      ... | true  with≡ eq = less (less-float eq)
      ... | false with≡ _ with inspect (primFloatLess y x)
      ...   | true  with≡ eq = greater (less-float eq)
      ...   | false with≡ _  = equal unsafeEqual

  OrdLawsFloat : Ord/Laws Float
  Ord/Laws.super OrdLawsFloat    = it
  less-antirefl {{OrdLawsFloat}} (less-float eq) = unsafeNotEqual eq
  less-trans    {{OrdLawsFloat}} (less-float _) (less-float _) = less-float unsafeEqual

instance
  ShowFloat : Show Float
  ShowFloat = simpleShowInstance primShowFloat

instance
  NumFloat : Number Float
  Number.Constraint NumFloat _ = ⊤
  Number.fromNat    NumFloat x = primNatToFloat x

  SemiringFloat : Semiring Float
  Semiring.zro SemiringFloat = 0.0
  Semiring.one SemiringFloat = 1.0
  Semiring._+_ SemiringFloat = primFloatPlus
  Semiring._*_ SemiringFloat = primFloatTimes

  SubFloat : Subtractive Float
  Subtractive._-_    SubFloat = primFloatMinus
  Subtractive.negate SubFloat = primFloatNegate

  NegFloat : Negative Float
  Negative.Constraint NegFloat _ = ⊤
  Negative.fromNeg    NegFloat x = negate (primNatToFloat x)

  FracFloat : Fractional Float
  Fractional.Constraint FracFloat _ _ = ⊤
  Fractional._/_ FracFloat x y = primFloatDiv x y

floor   = primFloor
round   = primRound
ceiling = primCeiling
exp     = primExp
ln      = primLog
sin     = primSin
sqrt    = primFloatSqrt

π : Float
π = 3.141592653589793

cos : Float → Float
cos x = sin (π / 2.0 - x)

tan : Float → Float
tan x = sin x / cos x

log : Float → Float → Float
log base x = ln x / ln base

_**_ : Float → Float → Float
a ** x = exp (x * ln a)

NaN : Float
NaN = 0.0 / 0.0

Inf : Float
Inf = 1.0 / 0.0

-Inf : Float
-Inf = -1.0 / 0.0

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Tactic.Monoid.Proofs where

open import Prelude
open import Structure.Monoid.Laws

open import Tactic.Monoid.Exp

⟦_⟧_ : ∀ {a} {A : Set a} {{_ : Monoid A}} → Exp → (Nat → A) → A
⟦ var x  ⟧ ρ = ρ x
⟦ ε      ⟧ ρ = mempty
⟦ e ⊕ e₁ ⟧ ρ = ⟦ e ⟧ ρ <> ⟦ e₁ ⟧ ρ

⟦_⟧n_ : ∀ {a} {A : Set a} {{_ : Monoid A}} → List Nat → (Nat → A) → A
⟦ xs ⟧n ρ = mconcat (map ρ xs)

map/++ : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (xs ys : List A) → map f (xs ++ ys) ≡ map f xs ++ map f ys
map/++ f [] ys = refl
map/++ f (x ∷ xs) ys = f x ∷_ $≡ map/++ f xs ys

module _ {a} {A : Set a} {{Mon : Monoid A}} {{Laws : MonoidLaws A}} where

  mconcat/++ : (xs ys : List A) → mconcat (xs ++ ys) ≡ mconcat xs <> mconcat ys
  mconcat/++ [] ys = sym (idLeft _)
  mconcat/++ (x ∷ xs) ys = x <>_ $≡ mconcat/++ xs ys ⟨≡⟩ <>assoc x _ _

  sound : ∀ e (ρ : Nat → A) → ⟦ e ⟧ ρ ≡ ⟦ flatten e ⟧n ρ
  sound (var x) ρ = sym (idRight (ρ x))
  sound ε ρ = refl
  sound (e ⊕ e₁) ρ = _<>_ $≡ sound e ρ *≡ sound e₁ ρ ⟨≡⟩ʳ
                     mconcat $≡ map/++ ρ (flatten e) (flatten e₁) ⟨≡⟩
                     mconcat/++ (map ρ (flatten e)) _

  proof : ∀ e e₁ (ρ : Nat → A) → flatten e ≡ flatten e₁ → ⟦ e ⟧ ρ ≡ ⟦ e₁ ⟧ ρ
  proof e e₁ ρ nfeq = eraseEquality $ sound e ρ ⟨≡⟩ (⟦_⟧n ρ) $≡ nfeq ⟨≡⟩ʳ sound e₁ ρ


text:
------------------------------------------------------------------------------
-- Example of a partial function using the Bove-Capretta method
------------------------------------------------------------------------------

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

-- From: Ana Bove and Venanzio Capretta. Nested general recursion and
-- partiality in type theory. vol 2152 LNCS. 2001.

module FOT.FOTC.Program.Min.MinBC-SL where

open import Data.Nat renaming ( suc to succ )
open import Relation.Binary.PropositionalEquality

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

data minAcc : (ℕ → ℕ) → Set where
  minacc0 : (f : ℕ → ℕ) → f 0 ≡ 0 → minAcc f
  minacc1 : (f : ℕ → ℕ) → f 0 ≢ 0 → minAcc (λ n → f (succ n)) → minAcc f

min : (f : ℕ → ℕ) → minAcc f → ℕ
min f (minacc0 .f q)   = 0
min f (minacc1 .f q h) = succ (min (λ n → f (succ n)) h)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Logic
open import Logic.Classical
open import Structure.Setoid
open import Structure.OrderedField
open import Type

module Structure.Function.Metric
  {ℓF ℓₑF ℓ≤}
  {F : Type{ℓF}}
  ⦃ equiv-F : Equiv{ℓₑF}(F) ⦄
  {_+_}{_⋅_}
  {_≤_ : _ → _ → Type{ℓ≤}}
  ⦃ orderedField-F : OrderedField{F = F}(_+_)(_⋅_)(_≤_) ⦄
  ⦃ classical : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄
  where

open OrderedField(orderedField-F)

import      Lvl
open import Data.Boolean
open import Data.Boolean.Proofs
import      Data.Either as Either
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional as Fn
open import Logic.Propositional
open import Logic.Predicate
open import Relator.Ordering
open import Sets.PredicateSet renaming (_≡_ to _≡ₛ_)
open import Structure.Setoid.Uniqueness
open import Structure.Function.Ordering
open import Structure.Operator.Field
open import Structure.Operator.Monoid
open import Structure.Operator.Group
open import Structure.Operator.Proofs
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Ordering
open        Structure.Relator.Ordering.Weak.Properties
open import Structure.Relator.Properties
open import Syntax.Transitivity

F₊ = ∃(Positive)

module _ where
  record MetricSpace {ℓₘ ℓₑₘ} {M : Type{ℓₘ}} ⦃ equiv-M : Equiv{ℓₑₘ}(M) ⦄ (d : M → M → F) : Type{ℓF Lvl.⊔ ℓ≤ Lvl.⊔ ℓₘ Lvl.⊔ ℓₑₘ Lvl.⊔ ℓₑF} where
    field
      ⦃ distance-binary-operator ⦄ : BinaryOperator(d)
      self-distance : ∀{x y} → (d(x)(y) ≡ 𝟎) ↔ (x ≡ y)
      ⦃ distance-commutativity ⦄ : Commutativity(d)
      triangle-inequality : ∀{x y z} → (d(x)(z) ≤ (d(x)(y) + d(y)(z)))
      ⦃ non-negativity ⦄ : ∀{x y} → NonNegative(d(x)(y))
      {-
      non-negativity{x}{y} =
        ([≤]ₗ-of-[+] (
          𝟎
          d(x)(x)
          d(x)(y) + d(y)(x)
          d(x)(y) + d(x)(y)
          2 ⋅ d(x)(y)
        ))
      -}

    distance-to-self : ∀{x} → (d(x)(x) ≡ 𝟎)
    distance-to-self = [↔]-to-[←] self-distance (reflexivity(_≡_))

    Neighborhood : M → F₊ → PredSet(M)
    Neighborhood(p)([∃]-intro r)(q) = (d(p)(q) < r)

    Neighborhoods : ∀{ℓ} → M → PredSet(PredSet{ℓ}(M))
    Neighborhoods(p)(N) = ∃(r ↦ N ≡ₛ Neighborhood(p)(r))

    PuncturedNeighborhood : M → F₊ → PredSet(M)
    PuncturedNeighborhood(p)([∃]-intro r)(q) = (𝟎 < d(p)(q) < r)

    LimitPoint : ∀{ℓ} → PredSet{ℓ}(M) → PredSet(M)
    LimitPoint(E)(p) = ∀{r} → Overlapping(PuncturedNeighborhood(p)(r)) (E)

    IsolatedPoint : ∀{ℓ} → PredSet{ℓ}(M) → PredSet(M)
    IsolatedPoint(E)(p) = ∃(r ↦ Disjoint(PuncturedNeighborhood(p)(r)) (E))

    Interior : ∀{ℓ} → PredSet{ℓ}(M) → PredSet(M)
    Interior(E)(p) = ∃(r ↦ Neighborhood(p)(r) ⊆ E)

    Closed : ∀{ℓ} → PredSet(PredSet{ℓ}(M))
    Closed(E) = LimitPoint(E) ⊆ E

    Open : ∀{ℓ} → PredSet(PredSet{ℓ}(M))
    Open(E) = E ⊆ Interior(E)

    Perfect : ∀{ℓ} → PredSet(PredSet{ℓ}(M))
    Perfect(E) = LimitPoint(E) ≡ₛ E

    Bounded : ∀{ℓ} → PredSet(PredSet{ℓ}(M))
    Bounded(E) = ∃(p ↦ ∃(r ↦ E ⊆ Neighborhood(p)(r)))

    Discrete : ∀{ℓ} → PredSet(PredSet{ℓ}(M))
    Discrete(E) = E ⊆ IsolatedPoint(E)

    Closure : ∀{ℓ} → PredSet{ℓ}(M) → PredSet(M)
    Closure(E) = E ∪ LimitPoint(E)

    Dense : ∀{ℓ} → PredSet(PredSet{ℓ}(M))
    Dense(E) = ∀{p} → (p ∈ Closure(E))

    -- Compact

    Separated : ∀{ℓ₁ ℓ₂} → PredSet{ℓ₁}(M) → PredSet{ℓ₂}(M) → Stmt
    Separated(A)(B) = Disjoint(A)(Closure(B)) ∧ Disjoint(Closure(A))(B)

    Connected : ∀{ℓ} → PredSet{ℓ}(M) → Stmtω
    Connected(E) = ∀{ℓ₁ ℓ₂}{A : PredSet{ℓ₁}(M)}{B : PredSet{ℓ₂}(M)} → ((A ∪ B) ≡ₛ E) → Separated(A)(B) → ⊥

    -- Complete = Sequence.Cauchy ⊆ Sequence.Converging

    neighborhood-contains-center : ∀{p}{r} → (p ∈ Neighborhood(p)(r))
    neighborhood-contains-center {p}{[∃]-intro r ⦃ intro positive-r ⦄} =
      d(p)(p) 🝖-[ sub₂(_≡_)(_≤_) distance-to-self ]-sub
      𝟎       🝖-semiend
      r       🝖-end-from-[ positive-r ]

    -- TODO: Not always the case?
    -- subneighborhood-subradius : ∀{p₁ p₂}{r₁ r₂} → (Neighborhood(p₁)(r₁) ⊆ Neighborhood(p₂)(r₂)) → ([∃]-witness r₁ ≤ [∃]-witness r₂)

    subneighborhood-radius : ∀{p₁ p₂}{r₁ r₂} → (Neighborhood(p₁)(r₁) ⊆ Neighborhood(p₂)(r₂)) ← (d(p₂)(p₁) ≤ ([∃]-witness r₂ − [∃]-witness r₁))
    subneighborhood-radius {p₁} {p₂} {[∃]-intro r₁} {[∃]-intro r₂} p {q} qN₁ =
      d(p₂)(q)             🝖[ _≤_ ]-[ triangle-inequality ]-sub
      d(p₂)(p₁) + d(p₁)(q) 🝖[ _<_ ]-[ [<][+]-preserve-subₗ p qN₁ ]-super
      (r₂ − r₁) + r₁       🝖[ _≡_ ]-[ {!inverseOperₗ ? ?!} ] -- inverseOperatorᵣ(_+_)(_−_)
      r₂                   🝖-end
      {-where
        r₁r₂ : (r₁ ≤ r₂) -- TODO: This seems to be provable, but not used here
        r₁r₂ =
          r₁             🝖-[ {!!} ]
          d(p₁)(p₂) + r₁ 🝖-[ {!!} ]
          r₂             🝖-end
      -}

    subneighborhood-radius-on-same : ∀{p}{r₁ r₂} → (Neighborhood(p)(r₁) ⊆ Neighborhood(p)(r₂)) ← ([∃]-witness r₁ ≤ [∃]-witness r₂)
    subneighborhood-radius-on-same {p} {[∃]-intro r₁} {[∃]-intro r₂} r₁r₂ {x} xN₁ xN₂ = xN₁ (r₁r₂ 🝖 xN₂)

    interior-is-subset : ∀{ℓ}{E : PredSet{ℓ}(M)} → Interior(E) ⊆ E
    interior-is-subset {ℓ} {E} {x} ([∃]-intro ([∃]-intro r ⦃ intro positive-r ⦄) ⦃ N⊆E ⦄) =
      N⊆E {x} (p ↦ positive-r (
        r       🝖[ _≤_ ]-[ p ]-super
        d(x)(x) 🝖[ _≡_ ]-[ distance-to-self ]
        𝟎       🝖[ _≡_ ]-end
      ))

    neighborhood-interior-is-self : ∀{p}{r} → (Interior(Neighborhood(p)(r)) ≡ₛ Neighborhood(p)(r))
    ∃.witness (Tuple.left (neighborhood-interior-is-self {p} {r}) x) = r
    ∃.proof (Tuple.left (neighborhood-interior-is-self {p} {r} {x}) Nx) = {!!}
    Tuple.right (neighborhood-interior-is-self {p} {r}) = {!!}

    neighborhood-is-open : ∀{p}{r} → Open(Neighborhood(p)(r))

    interior-is-largest-subspace : ∀{ℓ₁ ℓ₂}{E : PredSet{ℓ₁}(M)}{Eₛ : PredSet{ℓ₂}(M)} → Open(Eₛ) → (Eₛ ⊆ E) → (Eₛ ⊆ Interior(E))

    nested-interior : ∀{ℓ}{E : PredSet{ℓ}(M)} → Interior(Interior(E)) ≡ₛ Interior(E)

    isolated-limit-eq : ∀{ℓ}{E : PredSet{ℓ}(M)} → (IsolatedPoint(E) ⊆ ∅ {Lvl.𝟎}) ↔ (E ⊆ LimitPoint(E))

    interior-closure-eq1 : ∀{ℓ}{E : PredSet{ℓ}(M)} → ((∁ Interior(E)) ≡ₛ Closure(∁ E))

    interior-closure-eq2 : ∀{ℓ}{E : PredSet{ℓ}(M)} → (Interior(∁ E) ≡ₛ (∁ Closure(E)))

    open-closed-eq1 : ∀{ℓ}{E : PredSet{ℓ}(M)} → (Open(E) ↔ Closed(∁ E))

    open-closed-eq2 : ∀{ℓ}{E : PredSet{ℓ}(M)} → (Open(∁ E) ↔ Closed(E))

    union-is-open : ∀{ℓ₁ ℓ₂}{A : PredSet{ℓ₁}(M)}{B : PredSet{ℓ₂}(M)} → Open(A) → Open(B) → Open(A ∪ B)

    intersection-is-open : ∀{ℓ₁ ℓ₂}{A : PredSet{ℓ₁}(M)}{B : PredSet{ℓ₂}(M)} → Open(A) → Open(B) → Open(A ∩ B)

    -- open-subsubspace : ∀{ℓ₁ ℓ₂}{Eₛ : PredSet{ℓ₁}(M)}{E : PredSet{ℓ₂}(M)} →

    separated-is-disjoint : ∀{ℓ₁ ℓ₂}{A : PredSet{ℓ₁}(M)}{B : PredSet{ℓ₂}(M)} → Separated(A)(B) → Disjoint(A)(B)

    unionₗ-is-connected : ∀{ℓ₁ ℓ₂}{A : PredSet{ℓ₁}(M)}{B : PredSet{ℓ₂}(M)} → Connected(A ∪ B) → Connected(A)

    unionᵣ-is-connected : ∀{ℓ₁ ℓ₂}{A : PredSet{ℓ₁}(M)}{B : PredSet{ℓ₂}(M)} → Connected(A ∪ B) → Connected(B)

    intersection-is-connected : ∀{ℓ₁ ℓ₂}{A : PredSet{ℓ₁}(M)}{B : PredSet{ℓ₂}(M)} → Connected(A) → Connected(B) → Connected(A ∩ B)

module Sequence {ℓ} {M : Type{ℓ}} ⦃ equiv-M : Equiv(M) ⦄ (d : M → M → F) where
  open import Numeral.Natural
  import      Numeral.Natural.Relation.Order as ℕ

  ConvergesTo : (ℕ → M) → M → Stmt
  ConvergesTo f(L) = ∃{Obj = F₊ → ℕ}(N ↦ ∀{ε : F₊}{n} → (n ℕ.≥ N(ε)) → (d(f(n))(L) < [∃]-witness ε))

  Converging : (ℕ → M) → Stmt
  Converging(f) = ∃(ConvergesTo(f))

  Diverging : (ℕ → M) → Stmt
  Diverging(f) = ∀{L} → ¬(ConvergesTo f(L))

  lim : (f : ℕ → M) → ⦃ Converging(f) ⦄ → M
  lim(f) ⦃ [∃]-intro L ⦄ = L

  Cauchy : (ℕ → M) → Stmt
  Cauchy(f) = ∃{Obj = F₊ → ℕ}(N ↦ ∀{ε : F₊}{a b} → (a ℕ.≥ N(ε)) → (b ℕ.≥ N(ε)) → (d(f(a))(f(b)) < [∃]-witness ε))

  Complete : Stmt
  Complete = Cauchy ⊆ Converging

  Bounded : (ℕ → M) → Stmt
  Bounded(f) = ∃(r ↦ ∃(p ↦ ∀{n} → (d(p)(f(n)) < r)))

  unique-converges-to : ∀{f} → Unique(ConvergesTo(f))

  converging-bounded : Converging ⊆ Bounded

  -- strictly-ordered-sequence-limit : ∀{f g : ℕ → M} → (∀{n} → (f(n) < g(n))) → (lim f < lim g)
  -- ordered-sequence-limit : ∀{f g : ℕ → M} → (∀{n} → (f(n) ≤ g(n))) → (lim f ≤ lim g)

  -- limit-point-converging-sequence : ∀{E}{p} → LimitPoint(E)(p) → ∃(f ↦ (ConvergesTo f(p)) ∧ (∀{x} → (f(x) ∈ E)))

  -- TODO: Apparently, this requires both axiom of choice and excluded middle? At least the (←)-direction?
  -- continuous-sequence-convergence-composition : (ContinuousOn f(p)) ↔ (∀{g} → (ConvergesTo g(p)) → (ConvergesTo(f ∘ g)(f(p))))

  {-
  module Series where
    ∑ : (ℕ → M) → ℕ → M
    ∑ f(𝟎)    = 𝟎
    ∑ f(𝐒(n)) = (∑ f(n)) + f(𝐒(n))

    ∑₂ : (ℕ → M) → (ℕ ⨯ ℕ) → M
    ∑₂ f(a , b) = ∑ (f ∘ (a +_))(b − a)

    ConvergesTo : (ℕ → M) → M → Stmt
    ConvergesTo f(L) = Sequence.ConvergesTo(∑ f)(L)

    Converging : (ℕ → M) → Stmt
    Converging(f) = ∃(ConvergesTo(f))

    Diverging : (ℕ → M) → Stmt
    Diverging(f) = ∀{L} → ¬(ConvergesTo f(L))

    ConvergesTo : (ℕ → M) → M → Stmt
    AbsolutelyConvergesTo f(L) = ConvergesTo (‖_‖ ∘ f)(L)

    AbsolutelyConverging : (ℕ → M) → Stmt
    AbsolutelyConverging(f) = ∃(AbsolutelyConvergesTo(f))

    AbsolutelyDiverging : (ℕ → M) → Stmt
    AbsolutelyDiverging(f) = ∀{L} → ¬(AbsolutelyConvergesTo f(L))

    ConditionallyConverging : (ℕ → M) → Stmt
    ConditionallyConverging(f) = AbsolutelyDiverging(f) ∧ Converging(f)

    sequence-of-converging-series-converges-to-0 : Converging(f) → (Sequence.ConvergesTo f(𝟎))

    convergence-by-ordering : (∀{n} → f(n) ≤ g(n)) → (Converging(f) ← Converging(g))
    divergence-by-ordering : (∀{n} → f(n) ≤ g(n)) → (Diverging(f) → Diverging(g))
    convergence-by-quotient : Sequence.Converging(n ↦ f(n) / g(n)) → (Converging(f) ↔ Converging(g))
  -}

module Analysis
  {ℓ₁ ℓ₂}
  {M₁ : Type{ℓ₁}} ⦃ equiv-M₁ : Equiv(M₁) ⦄ (d₁ : M₁ → M₁ → F)
  ⦃ space₁ : MetricSpace(d₁) ⦄
  {M₂ : Type{ℓ₂}} ⦃ equiv-M₂ : Equiv(M₂) ⦄ (d₂ : M₂ → M₂ → F)
  ⦃ space₂ : MetricSpace(d₂) ⦄
  where

  open MetricSpace

  Lim : ∀{ℓ}{E : PredSet{ℓ}(M₁)} → ((x : M₁) → ⦃ x ∈ E ⦄ → M₂) → M₁ → M₂ → Stmt
  Lim {E = E} f(p)(L) = ∃{Obj = F₊ → F₊}(δ ↦ ∀{ε : F₊}{x} → ⦃ ex : x ∈ E ⦄ → (p ∈ PuncturedNeighborhood(space₁)(x)(δ(ε))) → (L ∈ Neighborhood(space₂)(f(x) ⦃ ex ⦄)(ε)))

  lim : ∀{ℓ}{E : PredSet{ℓ}(M₁)} → (f : (x : M₁) → ⦃ x ∈ E ⦄ → M₂) → (p : M₁) → ⦃ ∃(Lim f(p)) ⦄ → M₂
  lim f(p) ⦃ [∃]-intro L ⦄ = L

  ContinuousOn : ∀{ℓ}{E : PredSet{ℓ}(M₁)} → ((x : M₁) → ⦃ x ∈ E ⦄ → M₂) → (p : M₁) → ⦃ p ∈ E ⦄ → Stmt
  ContinuousOn f(p) = Lim f(p) (f(p))

  Continuous : ∀{ℓ}{E : PredSet{ℓ}(M₁)} → ((x : M₁) → ⦃ x ∈ E ⦄ → M₂) → Stmt
  Continuous{E = E}(f) = ∀{p} → ⦃ ep : p ∈ E ⦄ → ContinuousOn f(p) ⦃ ep ⦄

  -- continuous-mapping-connected : Continuous(f) → Connected(E) → Connected(map f(E))

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:
module Positivity where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

data Tree : Set where
  node : List Tree -> Tree

data Loop (A : Set) : Set where
  loop : Loop (Loop A) -> Loop A

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

data PList (A : Set) : Set where
  leaf : A -> PList A
  succ : PList (A × A) -> PList A

data Bush (A : Set) : Set where
  nil  : Bush A
  cons : A -> Bush (Bush A) -> Bush A

F : Set -> Set
F A = A

data Ok : Set where
  ok : F Ok -> Ok

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Section10 where

open import Section9 public

-- 10. Conclusions
-- ===============
--
-- We have defined a calculus of proof trees for simply typed λ-calculus with explicit substitutions
-- and we have proved that this calculus is sound and complete with respect to Kripke
-- models.  A decision algorithm for convertibility based on the technique of “normalisation by
-- evaluation” has also been proven correct.
--
-- One application of the results for proof trees is the soundness and completeness for a
-- formulation of an implicitly-typed λ-calculus with explicit substitutions.
--
-- An important aspect of this work is that it has been carried out on a machine; actually,
-- the problem was partly chosen because it seemed possible to do the formalization in a nice
-- way using ALF.  It is often emphasised that a proof is machine checked, but this is the very
-- minimum one can ask of a proof system.  Another important aspect is that the system helps
-- you to develop your proof, and I feel that ALF is on the right way: this work was not done
-- first by pen and paper and then typed into the machine, but was from the very beginning
-- carried out in interaction with the system.
--
-- NOTE: The above paragraphs apply to Agda, as well.
--
--
-- Appendix
-- --------
--
-- (…)
--
--
-- Acknowledgement
-- ---------------
--
-- The author wants to thank the editor Olivier Danvy for having had the patience with delays
-- and still being supportive.  She is also grateful to Bernd Grobauer for help with improving
-- the presentation.  The comments of the anonymous referees have also been very valuable.
--
--
-- References
-- ----------
--
-- 1.  Abadi, M., Cardelli, L., Curien, P.-L., and Lévy, J.-J.
--     Explicit substitutions.
--     Journal of Functional Programming, 1(4) (1991) 375–416.
--
-- 2.  Berger, U.
--     Program extraction from normalization proofs.
--     In Proceedings of TLCA’93, LNCS, Vol. 664, Springer Verlag, Berlin, 1993, pp. 91–106.
--
-- 3.  Berger, U. and Schwichtenberg, H.
--     An inverse of the evaluation functional for typed λ-calculus.
--     In Proceedings of the 6th Annual IEEE Symposium on Logic in Comp. Sci., Amsterdam, 1991, pp. 203–211.
--
-- 4.  Coquand, Th.
--     Pattern matching with dependent types.
--     In Proceedings of the 1992 Workshop on Types for Proofs and Programs, B. Nordström, K. Petersson, and
--     G. Plotkin (Eds.).  Dept. of Comp. Sci. Chalmers Univ. of Technology and Göteborg Univ.
--     Available at (…), pp. 66–79.
--
-- 5.  Coquand, Th. and Dybjer, P.
--     Intuitionistic model constructions and normalisation proofs.
--     Math. Structures Comp. Sci., 7(1) (1997) 75–94.
--
-- 6.  Coquand, Th. and Gallier, J.
--     A proof of strong normalization for the theory of constructions using a Kripke-like interpretation.
--     In Proceedings of the First Workshop in Logical Frameworks, G. Huet and G. Plotkin (Eds.).
--     Available at (…), pp. 479–497.
--
-- 7.  Coquand, Th., Nordström, B., Smith, J., and von Sydow, B.
--     Type theory and programming.
--     EATCS, 52 (1994) 203–228.
--
-- 8.  Curien, P.-L.
--     An abstract framework for environment machines.
--     Theoretical Comp. Sci., 82 (1991) 389–402.
--
-- 9.  Friedman, H.
--     Equality between functionals.
--     In Logic Colloquium, Symposium on Logic, held at Boston, 1972–1973, LNCS, Vol. 453,
--     Springer-Verlag, Berlin, 1975, pp. 22–37.
--
-- 10. Gandy, R.O.
--     On the axiom of extensionality—Part I.
--     The Journal of symbolic logic, 21 (1956) 36–48.
--
-- 11. Kripke S.A.
--     Semantical analysis of intuitionistic logic I.
--     In Formal Systems and Recursive Functions, J.N. Crossley and M.A.E. Dummet (Eds.).
--     North-Holland, Amsterdam, 1965, pp. 92–130.
--
-- 12. Magnusson, L. and Nordström, B.
--     The ALF proof editor and its proof engine.
--     In Types for Proofs and Programs, LNCS, Vol. 806, Springer-Verlag, Berlin, 1994, pp. 213–237.
--
-- 13. Martin-Löf, P.
--     Substitution calculus.
--     Handwritten notes, Göteborg, 1992.
--
-- 14. Mitchell, J.C.
--     Type systems for programming languages.
--     In Handbook of Theoretical Comp. Sci., Volume B: Formal Models and Semantics, J. van Leeuwen (Ed.).
--     Elsevier and MIT Press, Amsterdam, 1990, pp. 365–458.
--
-- 15. Mitchell, J.C. and Moggi, E.
--     Kripke-style models for typed lambda calculus.
--     Annals for Pure and Applied Logic, 51 (1991) 99–124.
--
-- 16. Nordström, B., Petersson, K., and Smith, J.
--     Programming in Martin-Löf’s Type THeory. An Introduction.
--     Oxford University Press, Oxford, UK, 1990.
--
-- 17. Scott, D.S.
--     Relating theories lambda calculus.
--     In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism.
--     Academic Press, New York, 1980, pp. 403–450.
--
-- 18. Statman, R.
--     Logical relation and the typed λ-calculus.
--     Information and Control, 65 (1985) 85–97.
--
-- 19. Streicher, T.
--     Semantics of Type Theory.
--     Birkhäuser, Basel, 1991.
--
-- 20. Tasistro, A.
--     Formulation of Martin-Löf’s theory of types with explicit substitutions.
--     Licentiate thesis, Dept. of Comp. Sci. Chalmers Univ. of Technology and Göteborg Univ., 1993.

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
{-# OPTIONS --cubical-compatible #-}
module _ where

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  instance refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}  -- This should trigger a warning!


text:
open import Agda.Primitive
open import Agda.Builtin.List
open import Agda.Builtin.Equality

private
  variable
    a p : Level
    A : Set a
    P Q : A → Set p

data Any {a p} {A : Set a} (P : A → Set p) : List A → Set (a ⊔ p) where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

map : (∀ {x} → P x → Q x) → (∀ {xs} → Any P xs → Any Q xs)
map g (here px)   = here (g px)
map g (there pxs) = there (map g pxs)

postulate
  map-id : ∀ (f : ∀ {x} → P x → P x) → (∀ {x} (p : P x) → f p ≡ p) →
          ∀ {xs} → (p : Any P xs) → map f p ≡ p


text:
module Avionics.SafetyEnvelopes where

open import Data.Bool using (Bool; true; false; _∧_; _∨_)
open import Data.List using (List; []; _∷_; any; map; foldl; length)
open import Data.List.Relation.Unary.Any as Any using (Any)
open import Data.List.Relation.Unary.All as All using (All)
open import Data.Maybe using (Maybe; just; nothing; is-just; _>>=_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
    using (_≡_; _≢_; refl; cong; subst; sym)
open import Relation.Unary using (_∈_)
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Nullary.Decidable using (fromWitnessFalse)

open import Avionics.Real
    using (ℝ; _+_; _-_; _*_; _÷_; _^_; _<ᵇ_; _≤ᵇ_; _≤_; _<_; _<?_; _≤?_; _≟_;
           1/_;
           0ℝ; 1ℝ; 2ℝ; 1/2; _^2; √_; fromℕ)
--open import Avionics.Product using (_×_; ⟨_,_⟩; proj₁; proj₂)
open import Avionics.Probability using (Dist; NormalDist; ND; BiNormalDist)

sum : List ℝ → ℝ
sum = foldl _+_ 0ℝ

inside : NormalDist → ℝ → ℝ → Bool
inside nd z x = ((μ - z * σ) <ᵇ x) ∧ (x <ᵇ (μ + z * σ))
  where open NormalDist nd using (μ; σ)

mahalanobis1 : ℝ → ℝ → ℝ → ℝ
mahalanobis1 u v IV = √((u - v) * IV * (u - v))

inside' : NormalDist → ℝ → ℝ → Bool
inside' nd z x = mahalanobis1 μ x σ²-¹ <ᵇ z
  where open NormalDist nd using (μ; σ)
        σ²-¹ = 1/ (σ * σ)

mahalanobis2 : (ℝ × ℝ) → (ℝ × ℝ) → (ℝ × ℝ × ℝ × ℝ) → ℝ
--mahalanobis2 u v VI = ...
mahalanobis2 ⟨ u₁ , u₂ ⟩ ⟨ v₁ , v₂ ⟩
            ⟨ iv₁₁ , ⟨ iv₁₂ , ⟨ iv₂₁ , iv₂₂ ⟩ ⟩ ⟩ = √ ⟨u-v⟩IV⟨u-v⟩'
  where x₁ = u₁ - v₁
        x₂ = u₂ - v₂
        ⟨u-v⟩IV⟨u-v⟩' = (x₁ * x₁ * iv₁₁ + x₁ * x₂ * iv₁₂
                        + x₁ * x₂ * iv₂₁ + x₂ * x₂ * iv₂₂)

insideBiv : BiNormalDist → ℝ → (ℝ × ℝ) → Bool
insideBiv bnd z x = mahalanobis2 μ x Σ-¹ <ᵇ z
  where open BiNormalDist bnd using (μ; Σ-¹)

FlightState = (ℝ × ℝ)

record Model : Set where
  field
    -- Flight states
    SM : List FlightState
    -- Map from flight states to Normal Distributions
    fM : List (FlightState × (NormalDist × ℝ))
    -- Every flight state must be represented in the map fM
    .fMisMap₁ : All (λ θ → Any (λ θ,ND → proj₁ θ,ND ≡ θ) fM ) SM
    .fMisMap₂ : All (λ θ,ND → Any (λ θ → proj₁ θ,ND ≡ θ) SM ) fM
    .lenSM>0 : length SM ≢ 0
    --.lenfM>0 : length fM ≢ 0 -- this is the result of the bijection above and .lenSM>0

z-predictable' : List NormalDist → ℝ → ℝ → ℝ × Bool
z-predictable' nds z x = ⟨ x , any (λ nd → inside nd z x) nds ⟩

z-predictable : Model → ℝ → ℝ → ℝ × Bool
z-predictable M z x = z-predictable' (map (proj₁ ∘ proj₂) (Model.fM M)) z x

--

sample-z-predictable : List NormalDist → ℝ → ℝ → List ℝ → Maybe (ℝ × ℝ × Bool)
sample-z-predictable nds zμ zσ [] = nothing
sample-z-predictable nds zμ zσ (_ ∷ []) = nothing
sample-z-predictable nds zμ zσ xs@(_ ∷ _ ∷ _) = just ⟨ mean , ⟨ var_est , any inside'' nds ⟩ ⟩
  where
    n = fromℕ (length xs)

    mean = (sum xs ÷ n)
    var_est = (sum (map (λ{x →(x - mean)^2}) xs) ÷ (n - 1ℝ))

    inside'' : NormalDist → Bool
    inside'' nd = ((μ - zμ * σ) <ᵇ mean) ∧ (mean <ᵇ (μ + zμ * σ))
                ∧ (σ^2 - zσ * std[σ^2] <ᵇ var) ∧ (var <ᵇ σ^2 + zσ * std[σ^2])
      where open NormalDist nd using (μ; σ)
            σ^2 = σ ^2
            --Var[σ^2] = 2 * (σ^2)^2 / n
            std[σ^2] = (√ 2ℝ) * (σ^2 ÷ (√ n))

            -- Notice that the estimated variance here is computed assuming `μ`
            -- it's the mean of the distribution. This is so that Cramer-Rao
            -- lower bound can be applied to it
            var = (sum (map (λ{x →(x - μ)^2}) xs) ÷ n)

nonneg-cf : ℝ → ℝ × Bool
nonneg-cf x = ⟨ x , 0ℝ ≤ᵇ x ⟩

data StallClasses : Set where
  Stall NoStall Uncertain : StallClasses

P[stall]f⟨_|stall⟩_ : ℝ → List (ℝ × ℝ × Dist ℝ) → ℝ
P[stall]f⟨ x |stall⟩ pbs = sum (map unpack pbs)
  where
    unpack : ℝ × ℝ × Dist ℝ → ℝ
    unpack ⟨ P[θ] , ⟨ P[stall|θ] , dist ⟩ ⟩ = pdf x * P[θ] * P[stall|θ]
      where open Dist dist using (pdf)

f⟨_⟩_ : ℝ → List (ℝ × ℝ × Dist ℝ) → ℝ
f⟨ x ⟩ pbs = sum (map unpack pbs)
  where
    unpack : ℝ × ℝ × Dist ℝ → ℝ
    unpack ⟨ P[θ] , ⟨ _ , dist ⟩ ⟩ = pdf x * P[θ]
      where open Dist dist using (pdf)

-- There should be a proof showing that the resulting value will always be in the interval [0,1]
P[_|X=_]_ : StallClasses → ℝ → List (ℝ × ℝ × Dist ℝ) → Maybe ℝ
P[ Stall |X= x ] pbs with f⟨ x ⟩ pbs ≟ 0ℝ
... | yes _ = nothing
... | no _  = just (((P[stall]f⟨ x |stall⟩ pbs) ÷ (f⟨ x ⟩ pbs)))
P[ NoStall |X= x ] pbs with f⟨ x ⟩ pbs ≟ 0ℝ
... | yes _ = nothing
... | no _  = just (1ℝ - ((P[stall]f⟨ x |stall⟩ pbs) ÷ (f⟨ x ⟩ pbs)))
P[ Uncertain |X= _ ] _ = nothing

postulate
  -- TODO: Find out how to prove this!
  -- It probably requires to prove that P[Stall|X=x] + P[NoStall|X=x] ≡ 1
  Stall≡1-NoStall : ∀ {x pbs p}
                  → P[ Stall |X= x ] pbs ≡ just p
                  → P[ NoStall |X= x ] pbs ≡ just (1ℝ - p)
  NoStall≡1-Stall : ∀ {x pbs p}
                  → P[ NoStall |X= x ] pbs ≡ just p
                  → P[ Stall |X= x ] pbs ≡ just (1ℝ - p)

  -- Main assumptions
  --   * 0.5 < τ ≤ 1
  --   * 0 ≤ p ≤ 1
  -- Of course, these assumptions are never explicit in the code. But note
  -- that, only the first assumption can be broken by an user bad input. The
  -- second assumption stems for probability theory, yet not proven but
  -- should be true
  ≤p→¬≤1-p : ∀ {τ p}
           -- This first line are the assumptions. From them, the rest should follow
           → 1/2 < τ → τ ≤ 1ℝ   -- 0.5 < τ ≤ 1
           → 0ℝ ≤ p → p ≤ 1ℝ  -- 0 ≤ p ≤ 1
           → τ ≤ p
           → ¬ τ ≤ (1ℝ - p)
  ≤1-p→¬≤p : ∀ {τ p}
           → 1/2 < τ → τ ≤ 1ℝ  -- 0.5 < τ ≤ 1
           → 0ℝ ≤ p → p ≤ 1ℝ   -- 0 ≤ p ≤ 1
           → τ ≤ (1ℝ - p)
           → ¬ τ ≤ p

classify'' : List (ℝ × ℝ × Dist ℝ) → ℝ → ℝ → StallClasses
classify'' pbs τ x with P[ Stall |X= x ] pbs
...   | nothing = Uncertain
...   | just p with τ ≤? p | τ ≤? (1ℝ - p)
...            | yes _ | no  _ = Stall
...            | no _  | yes _ = NoStall
...            | _     | _     = Uncertain -- the only missing case is `no _ | no _`, `yes _ | yes _` is not possible

M→pbs : Model → List (ℝ × ℝ × Dist ℝ)
M→pbs M = map convert (Model.fM M)
  where
    n = fromℕ (length (Model.fM M))

    convert : (ℝ × ℝ) × (NormalDist × ℝ) → ℝ × ℝ × Dist ℝ
    convert ⟨ _ , ⟨ nd , P[stall|c] ⟩ ⟩ = ⟨ 1/ n , ⟨ P[stall|c] , dist ⟩ ⟩
      where open NormalDist nd using (dist)

classify : Model → ℝ → ℝ → StallClasses
classify M = classify'' (M→pbs M)

no-uncertain : StallClasses → Bool
no-uncertain Uncertain = false
no-uncertain _ = true

τ-confident : Model → ℝ → ℝ → Bool
τ-confident M τ = no-uncertain ∘ classify M τ

safety-envelope : Model → ℝ → ℝ → ℝ → Bool
safety-envelope M z τ x = proj₂ (z-predictable M z x)
                          ∧ τ-confident M τ x

max_stars_repo_name: helq/safety-envelopes-sentinels

max_issues_repo_name: helq/safety-envelopes-sentinels

max_forks_repo_name: helq/safety-envelopes-sentinels


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

open import Base
open import Coinduction

module CoindEquiv where

-- Coinductive equivalences
record _∼_ {i j} (A : Set i) (B : Set j) : Set (max i j) where
  constructor _,_,_
  field
    to : A → B
    from : B → A
    eq : ∞ ((a : A) (b : B) → ((to a ≡ b) ∼ (a ≡ from b)))

-- Identity
id-∼ : ∀ {i} (A : Set i) → A ∼ A
id-∼ A = (id A) , (id A) , ♯ (λ a b → id-∼ (a ≡ b))

-- Transitivity
trans-∼ : ∀ {i} {A B C : Set i} → A ∼ B → B ∼ C → A ∼ C
trans-∼ (to , from , eq) (to' , from' , eq') =
  ((to' ◯ to) , (from ◯ from') ,
    ♯ (λ a c → trans-∼ (♭ eq' (to a) c) (♭ eq a (from' c))) ) --(λ a c → ♯ trans-∼ (♭ (eq' (to a) c)) (♭ (eq a (from' c)))))

-- -- Left unity
-- left-unit-∼ : ∀ {i} {A B : Set i} (f : A ∼ B) → trans-∼ (id-∼ A) f ≡ f
-- left-unit-∼ f = {!!}

postulate
  !-≡ : ∀ {i} {A : Set i} {u v : A} → (u ≡ v) ≡ (v ≡ u)

-- Symmetry is harder
sym-∼ : ∀ {i} {A B : Set i} → A ∼ B → B ∼ A
sym-∼ (to , from , eq) = (from , to ,
  ♯ (λ b a → let (too , fromo , eqo) = sym-∼ (♭ eq a b) in ((! ◯ (too ◯ !)) , {!!} , {!!})))
--(λ a b → transport (λ u → ∞ (u ∼ (a ≡ to b))) !-≡ (transport (λ u → ∞ ((b ≡ from a) ∼ u)) !-≡ (♯ (sym-∼ (♭ (eq b a))))))) --♯ trans-∼ {!!} (trans-∼ (sym-∼ (♭ (eq b a))) {!!})))

-- Logical equivalence with the usual notion of equivalences

∼-to-≃ : ∀ {i j} {A : Set i} {B : Set j} → (A ∼ B → A ≃ B)
∼-to-≃ (to , from , eq) =
  (to , iso-is-eq to from (λ b → _∼_.from (♭ eq (from b) b) refl)
                          (λ a → ! (_∼_.to (♭ eq a (to a)) refl)))

≃-to-∼ : ∀ {i j} {A : Set i} {B : Set j} → (A ≃ B → A ∼ B)
≃-to-∼ e = (π₁ e) , (inverse e) ,
  ♯ (λ a b → ≃-to-∼ (equiv-compose
    (path-to-eq (ap (λ b → e ☆ a ≡ b) (! (inverse-right-inverse e b))))
    ((equiv-ap e a (inverse e b))⁻¹)))

-- Unfinished attempt to prove that this notion is coherent

∼-eq-raw : ∀ {i j} {A : Set i} {B : Set j}
  {f f' : A → B} (p : f ≡ f') {g g' : B → A} (q : g ≡ g')
  {eq : ∞ ((a : A) (b : B) → ((f a ≡ b) ∼ (a ≡ g b)))}
  {eq' : ∞ ((a : A) (b : B) → ((f' a ≡ b) ∼ (a ≡ g' b)))}
  (r : transport _ p (transport _ q eq) ≡ eq')
  → (f , g , eq) ≡ (f' , g' , eq')
∼-eq-raw refl refl refl = refl

-- ∼-eq : ∀ {i j} {A : Set i} {B : Set j}
--   {f f' : A → B} (p : (a : A) → f a ≡ f' a)
--   {g g' : B → A} (q : (b : B) → g b ≡ g' b)
--   {eq : (a : A) (b : B) → ∞ ((f a ≡ b) ∼ (a ≡ g b))}
--   {eq' : (a : A) (b : B) → ∞ ((f' a ≡ b) ∼ (a ≡ g' b))}
--   (r : (a : A) (b : B) →
--      transport (λ u → (u ≡ b) ∼ (a ≡ g' b)) (p a) (
--      transport (λ u → (f a ≡ b) ∼ (a ≡ u)) (q b) (♭ (eq a b)))
--      ≡ ♭ (eq' a b))
--   → (f , g , eq) ≡ (f' , g' , eq')
-- ∼-eq p q r = ∼-eq-raw (funext p) (funext q)
--   (funext (λ a → (funext (λ b → {!r a b!}))))

-- coherent : ∀ {i j} (A : Set i) (B : Set j) → ((A ≃ B) ≃ (A ∼ B))
-- coherent A B = (≃-to-∼ A B , iso-is-eq _ (∼-to-≃ A B)
--   (λ y → ∼-eq (λ a → refl _)
--               (λ b → happly (inverse-iso-is-eq (_∼_.to y) (_∼_.from y) _ _) b)
--               (λ a b → {!!}))
--   (λ e → Σ-eq (refl _) (π₁ (is-equiv-is-prop _ _ _))))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

module Definition.Typed.Consequences.Substitution where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.Typed.Weakening
open import Definition.Typed.Consequences.Syntactic
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Irrelevance
open import Definition.LogicalRelation.Fundamental

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Well-formed substitution of types.
substitution : ∀ {A rA Γ Δ σ} → Γ ⊢ A ^ rA → Δ ⊢ˢ σ ∷ Γ → ⊢ Δ → Δ ⊢ subst σ A ^ rA
substitution A σ ⊢Δ =
    let X = fundamental A
        [Γ] = proj₁ X
        [A] = proj₂ X
        Y = fundamentalSubst (wf A) ⊢Δ σ
        [Γ]′ = proj₁ Y
        [σ] = proj₂ Y
    in escape (proj₁ ([A] ⊢Δ (irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ])))

-- Well-formed substitution of type equality.
substitutionEq : ∀ {A B rA Γ Δ σ σ′}
               → Γ ⊢ A ≡ B ^ rA → Δ ⊢ˢ σ ≡ σ′ ∷ Γ → ⊢ Δ → Δ ⊢ subst σ A ≡ subst σ′ B ^ rA
substitutionEq A≡B σ ⊢Δ =
  let X = fundamentalEq A≡B
      [Γ] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [B] = proj₁ (proj₂ (proj₂ X))
      [A≡B] = proj₂ (proj₂ (proj₂ X))
      Y = fundamentalSubstEq (wfEq A≡B) ⊢Δ σ
      [Γ]′ = proj₁ Y
      [σ] = proj₁ (proj₂ Y)
      [σ′] = proj₁ (proj₂ (proj₂ Y))
      [σ≡σ′] = proj₂ (proj₂ (proj₂ Y))
      [σ]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
      [σ′]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ′]
      [σ≡σ′]′ = irrelevanceSubstEq [Γ]′ [Γ] ⊢Δ ⊢Δ [σ] [σ]′ [σ≡σ′]
  in  escapeEq (proj₁ ([A] ⊢Δ [σ]′))
                   (transEq (proj₁ ([A] ⊢Δ [σ]′)) (proj₁ ([B] ⊢Δ [σ]′))
                            (proj₁ ([B] ⊢Δ [σ′]′)) ([A≡B] ⊢Δ [σ]′)
                            (proj₂ ([B] ⊢Δ [σ]′) [σ′]′ [σ≡σ′]′))

-- Well-formed substitution of terms.
substitutionTerm : ∀ {t A rA Γ Δ σ}
               → Γ ⊢ t ∷ A ^ rA → Δ ⊢ˢ σ ∷ Γ → ⊢ Δ → Δ ⊢ subst σ t ∷ subst σ A ^ rA
substitutionTerm t σ ⊢Δ =
  let X = fundamentalTerm t
      [Γ] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [t] = proj₂ (proj₂ X)
      Y = fundamentalSubst (wfTerm t) ⊢Δ σ
      [Γ]′ = proj₁ Y
      [σ] = proj₂ Y
      [σ]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
  in escapeTerm (proj₁ ([A] ⊢Δ [σ]′)) (proj₁ ([t] ⊢Δ [σ]′))

-- Well-formed substitution of term equality.
substitutionEqTerm : ∀ {t u A rA Γ Δ σ σ′}
                   → Γ ⊢ t ≡ u ∷ A ^ rA → Δ ⊢ˢ σ ≡ σ′ ∷ Γ → ⊢ Δ
                   → Δ ⊢ subst σ t ≡ subst σ′ u ∷ subst σ A ^ rA
substitutionEqTerm t≡u σ≡σ′ ⊢Δ with fundamentalTermEq t≡u
substitutionEqTerm t≡u σ≡σ′ ⊢Δ | [Γ] , modelsTermEq [A] [t] [u] [t≡u] =
  let Y = fundamentalSubstEq (wfEqTerm t≡u) ⊢Δ σ≡σ′
      [Γ]′ = proj₁ Y
      [σ] = proj₁ (proj₂ Y)
      [σ′] = proj₁ (proj₂ (proj₂ Y))
      [σ≡σ′] = proj₂ (proj₂ (proj₂ Y))
      [σ]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
      [σ′]′ = irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ′]
      [σ≡σ′]′ = irrelevanceSubstEq [Γ]′ [Γ] ⊢Δ ⊢Δ [σ] [σ]′ [σ≡σ′]
  in  escapeTermEq (proj₁ ([A] ⊢Δ [σ]′))
                       (transEqTerm (proj₁ ([A] ⊢Δ [σ]′)) ([t≡u] ⊢Δ [σ]′)
                                    (proj₂ ([u] ⊢Δ [σ]′) [σ′]′ [σ≡σ′]′))

-- Reflexivity of well-formed substitution.
substRefl : ∀ {σ Γ Δ}
          → Δ ⊢ˢ σ ∷ Γ
          → Δ ⊢ˢ σ ≡ σ ∷ Γ
substRefl id = id
substRefl (σ , x) = substRefl σ , genRefl x

-- Weakening of well-formed substitution.
wkSubst′ : ∀ {ρ σ Γ Δ Δ′} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ) (⊢Δ′ : ⊢ Δ′)
           ([ρ] : ρ ∷ Δ′ ⊆ Δ)
           ([σ] : Δ ⊢ˢ σ ∷ Γ)
         → Δ′ ⊢ˢ ρ •ₛ σ ∷ Γ
wkSubst′ ε ⊢Δ ⊢Δ′ ρ id = id
wkSubst′ (_∙_ {Γ} {A} ⊢Γ ⊢A) ⊢Δ ⊢Δ′ ρ (tailσ , headσ) =
  wkSubst′ ⊢Γ ⊢Δ ⊢Δ′ ρ tailσ
  , PE.subst (λ x → _ ⊢ _ ∷ x ^ _) (wk-subst A) (wkTerm ρ ⊢Δ′ headσ)

-- Weakening of well-formed substitution by one.
wk1Subst′ : ∀ {F rF σ Γ Δ} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ)
            (⊢F : Δ ⊢ F ^ rF)
            ([σ] : Δ ⊢ˢ σ ∷ Γ)
          → (Δ ∙ F ^ rF) ⊢ˢ wk1Subst σ ∷ Γ
wk1Subst′ {F} {σ} {Γ} {Δ} ⊢Γ ⊢Δ ⊢F [σ] =
  wkSubst′ ⊢Γ ⊢Δ (⊢Δ ∙ ⊢F) (step id) [σ]

-- Lifting of well-formed substitution.
liftSubst′ : ∀ {F rF σ Γ Δ} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ)
             (⊢F  : Γ ⊢ F ^ rF)
             ([σ] : Δ ⊢ˢ σ ∷ Γ)
           → (Δ ∙ subst σ F ^ rF) ⊢ˢ liftSubst σ ∷ Γ ∙ F ^ rF
liftSubst′ {F} {rF} {σ} {Γ} {Δ} ⊢Γ ⊢Δ ⊢F [σ] =
  let ⊢Δ∙F = ⊢Δ ∙ substitution ⊢F [σ] ⊢Δ
  in  wkSubst′ ⊢Γ ⊢Δ ⊢Δ∙F (step id) [σ]
  ,   var ⊢Δ∙F (PE.subst (λ x → 0 ∷ x ^ rF ∈ (Δ ∙ subst σ F ^ rF))
                         (wk-subst F) here)

-- Well-formed identity substitution.
idSubst′ : ∀ {Γ} (⊢Γ : ⊢ Γ)
         → Γ ⊢ˢ idSubst ∷ Γ
idSubst′ ε = id
idSubst′ (_∙_ {Γ} {A} {rA} ⊢Γ ⊢A) =
  wk1Subst′ ⊢Γ ⊢Γ ⊢A (idSubst′ ⊢Γ)
  , PE.subst (λ x → Γ ∙ A ^ rA ⊢ _ ∷ x ^ rA) (wk1-tailId A) (var (⊢Γ ∙ ⊢A) here)

-- Well-formed substitution composition.
substComp′ : ∀ {σ σ′ Γ Δ Δ′} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ) (⊢Δ′ : ⊢ Δ′)
             ([σ] : Δ′ ⊢ˢ σ ∷ Δ)
             ([σ′] : Δ ⊢ˢ σ′ ∷ Γ)
           → Δ′ ⊢ˢ σ ₛ•ₛ σ′ ∷ Γ
substComp′ ε ⊢Δ ⊢Δ′ [σ] id = id
substComp′ (_∙_ {Γ} {A} {rA} ⊢Γ ⊢A) ⊢Δ ⊢Δ′ [σ] ([tailσ′] , [headσ′]) =
  substComp′ ⊢Γ ⊢Δ ⊢Δ′ [σ] [tailσ′]
  , PE.subst (λ x → _ ⊢ _ ∷ x ^ rA) (substCompEq A)
             (substitutionTerm [headσ′] [σ] ⊢Δ′)

-- Well-formed singleton substitution of terms.
singleSubst : ∀ {A t rA Γ} → Γ ⊢ t ∷ A ^ rA → Γ ⊢ˢ sgSubst t ∷ Γ ∙ A ^ rA
singleSubst {A} {rA = rA} t =
  let ⊢Γ = wfTerm t
  in  idSubst′ ⊢Γ , PE.subst (λ x → _ ⊢ _ ∷ x ^ rA) (PE.sym (subst-id A)) t

-- Well-formed singleton substitution of term equality.
singleSubstEq : ∀ {A t u rA Γ} → Γ ⊢ t ≡ u ∷ A ^ rA
              → Γ ⊢ˢ sgSubst t ≡ sgSubst u ∷ Γ ∙ A ^ rA
singleSubstEq {A} {rA = rA} t =
  let ⊢Γ = wfEqTerm t
  in  substRefl (idSubst′ ⊢Γ) , PE.subst (λ x → _ ⊢ _ ≡ _ ∷ x ^ rA) (PE.sym (subst-id A)) t

-- Well-formed singleton substitution of terms with lifting.
singleSubst↑ : ∀ {A t rA Γ} → Γ ∙ A ^ rA ⊢ t ∷ wk1 A ^ rA
             → Γ ∙ A ^ rA ⊢ˢ consSubst (wk1Subst idSubst) t ∷ Γ ∙ A ^ rA
singleSubst↑ {A} {rA = rA} t with wfTerm t
... | ⊢Γ ∙ ⊢A = wk1Subst′ ⊢Γ ⊢Γ ⊢A (idSubst′ ⊢Γ)
              , PE.subst (λ x → _ ∙ A ^ rA ⊢ _ ∷ x ^ _) (wk1-tailId A) t

-- Well-formed singleton substitution of term equality with lifting.
singleSubst↑Eq : ∀ {A rA t u Γ} → Γ ∙ A ^ rA ⊢ t ≡ u ∷ wk1 A ^ rA
              → Γ ∙ A ^ rA ⊢ˢ consSubst (wk1Subst idSubst) t ≡ consSubst (wk1Subst idSubst) u ∷ Γ ∙ A ^ rA
singleSubst↑Eq {A} {rA} t with wfEqTerm t
... | ⊢Γ ∙ ⊢A = substRefl (wk1Subst′ ⊢Γ ⊢Γ ⊢A (idSubst′ ⊢Γ))
              , PE.subst (λ x → _ ∙ A ^ rA ⊢ _ ≡ _ ∷ x ^ rA) (wk1-tailId A) t

-- Helper lemmas for single substitution

substType : ∀ {t F rF G rG Γ} → Γ ∙ F ^ rF ⊢ G ^ rG → Γ ⊢ t ∷ F ^ rF → Γ ⊢ G [ t ] ^ rG
substType {t} {F} {G} ⊢G ⊢t =
  let ⊢Γ = wfTerm ⊢t
  in  substitution ⊢G (singleSubst ⊢t) ⊢Γ

substTypeEq : ∀ {t u F rF G E rG Γ} → Γ ∙ F ^ rF ⊢ G ≡ E ^ rG
            → Γ ⊢ t ≡ u ∷ F ^ rF
            → Γ ⊢ G [ t ] ≡ E [ u ] ^ rG
substTypeEq {F = F} ⊢G ⊢t =
  let ⊢Γ = wfEqTerm ⊢t
  in  substitutionEq ⊢G (singleSubstEq ⊢t) ⊢Γ

substTerm : ∀ {F rF G rG t f Γ} → Γ ∙ F ^ rF ⊢ f ∷ G ^ rG
          → Γ ⊢ t ∷ F ^ rF
          → Γ ⊢ f [ t ] ∷ G [ t ] ^ rG
substTerm {F} {G} {t} {f} ⊢f ⊢t =
  let ⊢Γ = wfTerm ⊢t
  in  substitutionTerm ⊢f (singleSubst ⊢t) ⊢Γ

substTypeΠ : ∀ {t F rF lF lG G rΠ lΠ Γ} → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ rΠ , ι lΠ ] → Γ ⊢ t ∷ F ^ [ rF , ι lF ]
                                     → Γ ⊢ G [ t ] ^ [ rΠ , ι lG ]
substTypeΠ ΠFG t with syntacticΠ ΠFG
substTypeΠ ΠFG t | F , G = substType G t

subst↑Type : ∀ {t F rF G rG Γ}
           → Γ ∙ F ^ rF ⊢ G ^ rG
           → Γ ∙ F ^ rF ⊢ t ∷ wk1 F ^ rF
           → Γ ∙ F ^ rF ⊢ G [ t ]↑ ^ rG
subst↑Type ⊢G ⊢t = substitution ⊢G (singleSubst↑ ⊢t) (wfTerm ⊢t)

subst↑TypeEq : ∀ {t u F rF G E rG Γ}
             → Γ ∙ F ^ rF ⊢ G ≡ E ^ rG
             → Γ ∙ F ^ rF ⊢ t ≡ u ∷ wk1 F ^ rF
             → Γ ∙ F ^ rF ⊢ G [ t ]↑ ≡ E [ u ]↑ ^ rG
subst↑TypeEq ⊢G ⊢t = substitutionEq ⊢G (singleSubst↑Eq ⊢t) (wfEqTerm ⊢t)

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.Kleisli where

open import Level

open import Categories.Category
open import Categories.Functor using (Functor; module Functor)
open import Categories.NaturalTransformation hiding (id)
open import Categories.Monad
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level

Kleisli : {𝒞 : Category o ℓ e} → Monad 𝒞 → Category o ℓ e
Kleisli {𝒞 = 𝒞} M = record
  { Obj       = Obj
  ; _⇒_       = λ A B → (A ⇒ F₀ B)
  ; _≈_       = _≈_
  ; _∘_       = λ f g → (μ.η _ ∘ F₁ f) ∘ g
  ; id        = η.η _
  ; assoc     = assoc′
  ; sym-assoc = Equiv.sym assoc′
  ; identityˡ = identityˡ′
  ; identityʳ = identityʳ′
  ; identity² = identity²′
  ; equiv     = equiv
  ; ∘-resp-≈  = λ f≈h g≈i → ∘-resp-≈ (∘-resp-≈ʳ (F-resp-≈ f≈h)) g≈i
  }
  where
  module M = Monad M
  open M using (μ; η; F)
  open Functor F
  open Category 𝒞
  open HomReasoning
  open MR 𝒞

  -- shorthands to make the proofs nicer
  F≈ = F-resp-≈

  assoc′ : ∀ {A B C D} {f : A ⇒ F₀ B} {g : B ⇒ F₀ C} {h : C ⇒ F₀ D}
          → (μ.η D ∘ (F₁ ((μ.η D ∘ F₁ h) ∘ g))) ∘ f ≈ (μ.η D ∘ F₁ h) ∘ ((μ.η C ∘ F₁ g) ∘ f)
  assoc′ {A} {B} {C} {D} {f} {g} {h} =
      begin
        (μ.η D ∘ F₁ ((μ.η D ∘ F₁ h) ∘ g)) ∘ f            ≈⟨ assoc ⟩
        μ.η D ∘ (F₁ ((μ.η D ∘ F₁ h) ∘ g) ∘ f)            ≈⟨ refl⟩∘⟨ (F≈ assoc ⟩∘⟨refl ) ⟩
        μ.η D ∘ (F₁ (μ.η D ∘ (F₁ h ∘ g)) ∘ f)            ≈⟨ refl⟩∘⟨ (homomorphism ⟩∘⟨refl) ⟩
        μ.η D ∘ ((F₁ (μ.η D) ∘ F₁ (F₁ h ∘ g)) ∘ f)       ≈⟨ refl⟩∘⟨ assoc ○ ⟺ assoc ⟩
        (μ.η D ∘ F₁ (μ.η D)) ∘ (F₁ (F₁ h ∘ g) ∘ f)       ≈⟨ M.assoc ⟩∘⟨refl ○ assoc ⟩
        μ.η D ∘ (μ.η (F₀ D) ∘ (F₁ (F₁ h ∘ g) ∘ f))       ≈˘⟨ refl⟩∘⟨ assoc ⟩
        μ.η D ∘ ((μ.η (F₀ D) ∘ F₁ (F₁ h ∘ g)) ∘ f)       ≈⟨ refl⟩∘⟨ ( (refl⟩∘⟨ homomorphism) ⟩∘⟨refl) ⟩
        μ.η D ∘ ((μ.η (F₀ D) ∘ (F₁ (F₁ h) ∘ F₁ g)) ∘ f)  ≈˘⟨ refl⟩∘⟨ (assoc ⟩∘⟨refl) ⟩
        μ.η D ∘ (((μ.η (F₀ D) ∘ F₁ (F₁ h)) ∘ F₁ g) ∘ f)  ≈⟨ refl⟩∘⟨ ((μ.commute h ⟩∘⟨refl) ⟩∘⟨refl) ⟩
        μ.η D ∘ (((F₁ h ∘ μ.η C) ∘ F₁ g) ∘ f)            ≈⟨ refl⟩∘⟨ (assoc ⟩∘⟨refl) ⟩
        μ.η D ∘ ((F₁ h ∘ (μ.η C ∘ F₁ g)) ∘ f)            ≈⟨ refl⟩∘⟨ assoc ○ ⟺ assoc ⟩
        (μ.η D ∘ F₁ h) ∘ ((μ.η C ∘ F₁ g) ∘ f)
      ∎

  identityˡ′ : ∀ {A B} {f : A ⇒ F₀ B} → (μ.η B ∘ F₁ (η.η B)) ∘ f ≈ f
  identityˡ′ {A} {B} {f} = elimˡ M.identityˡ

  identityʳ′ : ∀ {A B} {f : A ⇒ F₀ B} → (μ.η B ∘ F₁ f) ∘ η.η A ≈ f
  identityʳ′ {A} {B} {f} =
      begin
        (μ.η B ∘ F₁ f) ∘ η.η A      ≈⟨ assoc ⟩
        μ.η B ∘ (F₁ f ∘ η.η A)      ≈˘⟨ refl⟩∘⟨ η.commute f ⟩
        μ.η B ∘ (η.η (F₀ B) ∘ f)    ≈˘⟨ assoc ⟩
        (μ.η B ∘ η.η (F₀ B)) ∘ f    ≈⟨ elimˡ M.identityʳ ⟩
        f
      ∎

  identity²′ : {A : Obj} → (μ.η A ∘ F₁ (η.η A)) ∘ η.η A ≈ η.η A
  identity²′ = elimˡ M.identityˡ

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


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

module Examples.Run where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Bool using (true; false)
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; val; bool; ~=; string)
open import Luau.Run using (run; return)

ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ val nil) ∙ done) ≡ return nil _)
ex1 = refl

ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (val (number 123.0)) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (number 123.0) _)
ex2 = refl

ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (val (number 1.0)) + (val (number 2.0))) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (number 3.0) _)
ex3 = refl

ex4 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (val (number 1.0)) < (val (number 2.0))) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (bool true) _)
ex4 = refl

ex5 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (val (string "foo")) ~= (val (string "bar"))) ∙ done end ∙ return (var "fn" $ val nil) ∙ done) ≡ return (bool true) _)
ex5 = refl

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
------------------------------------------------------------------------------
-- Properties for the bisimilarity relation
------------------------------------------------------------------------------

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

module FOTC.Relation.Binary.Bisimilarity.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Stream.Type
open import FOTC.Relation.Binary.Bisimilarity.Type

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, the
-- bisimilarity relation _≈_ on unbounded lists is also a pre-fixed
-- point of the bisimulation functional (see
-- FOTC.Relation.Binary.Bisimulation).

-- See Issue https://github.com/asr/apia/issues/81 .
≈-inB : D → D → Set
≈-inB xs ys = ∃[ x' ]  ∃[ xs' ] ∃[ ys' ]
                xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ xs' ≈ ys'
{-# ATP definition ≈-inB #-}

≈-in : ∀ {xs ys} →
       ∃[ x' ]  ∃[ xs' ] ∃[ ys' ]
         xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ xs' ≈ ys' →
       xs ≈ ys
≈-in h = ≈-coind ≈-inB h' h
  where
  postulate
    h' : ∀ {xs} {ys} → ≈-inB xs ys →
         ∃[ x' ] ∃[ xs' ] ∃[ ys' ] xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ ≈-inB xs' ys'
  {-# ATP prove h' #-}

-- See Issue https://github.com/asr/apia/issues/81 .
≈-reflB : D → D → Set
≈-reflB xs ys = xs ≡ ys ∧ Stream xs
{-# ATP definition ≈-reflB #-}

≈-refl : ∀ {xs} → Stream xs → xs ≈ xs
≈-refl {xs} Sxs = ≈-coind ≈-reflB h₁ h₂
  where
  postulate
    h₁ : ∀ {xs ys} → ≈-reflB xs ys →
         ∃[ x' ] ∃[ xs' ] ∃[ ys' ] xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ ≈-reflB xs' ys'
  {-# ATP prove h₁ #-}

  postulate h₂ : ≈-reflB xs xs
  {-# ATP prove h₂ #-}

-- See Issue https://github.com/asr/apia/issues/81 .
≈-symB : D → D → Set
≈-symB xs ys = ys ≈ xs
{-# ATP definition ≈-symB #-}

≈-sym : ∀ {xs ys} → xs ≈ ys → ys ≈ xs
≈-sym {xs} {ys} xs≈ys = ≈-coind ≈-symB h₁ h₂
  where
  postulate
    h₁ : ∀ {ys} {xs} → ≈-symB ys xs →
         ∃[ y' ] ∃[ ys' ] ∃[ xs' ] ys ≡ y' ∷ ys' ∧ xs ≡ y' ∷ xs' ∧ ≈-symB ys' xs'
  {-# ATP prove h₁ #-}

  postulate h₂ : ≈-symB ys xs
  {-# ATP prove h₂ #-}

-- See Issue https://github.com/asr/apia/issues/81 .
≈-transB : D → D → Set
≈-transB xs zs = ∃[ ys ] xs ≈ ys ∧ ys ≈ zs
{-# ATP definition ≈-transB #-}

≈-trans : ∀ {xs ys zs} → xs ≈ ys → ys ≈ zs → xs ≈ zs
≈-trans {xs} {ys} {zs} xs≈ys ys≈zs = ≈-coind ≈-transB h₁ h₂
  where
  postulate
    h₁ : ∀ {as} {cs} → ≈-transB as cs →
         ∃[ a' ] ∃[ as' ] ∃[ cs' ] as ≡ a' ∷ as' ∧ cs ≡ a' ∷ cs' ∧ ≈-transB as' cs'
  {-# ATP prove h₁ #-}

  postulate h₂ : ≈-transB xs zs
  {-# ATP prove h₂ #-}

postulate ∷-injective≈ : ∀ {x xs ys} → x ∷ xs ≈ x ∷ ys → xs ≈ ys
{-# ATP prove ∷-injective≈ #-}

postulate ∷-rightCong≈ : ∀ {x xs ys} → xs ≈ ys → x ∷ xs ≈ x ∷ ys
{-# ATP prove ∷-rightCong≈ ≈-in #-}


text:
open import Data.Nat hiding ( _+_; _*_; _⊔_; zero )
open import Algebra hiding (Zero)
open import Level using (Level; _⊔_)
open import Data.Product

module quad { c ℓ } ( ring : Ring c ℓ ) where
open Ring ring

data Nat4 : Set where
  One : Nat4
  Suc : Nat4 -> Nat4

variable
  a b d : Level
  A : Set a
  B : Set b
  C : Set c
  m n : Nat4

-- Indu:ctive definition of a Quad matrix
data Quad ( A : Set a ) : Nat4 → Set a where
  Zero : Quad A n
  Scalar : A → Quad A One
  Mtx : ( nw ne sw se : Quad A n ) → Quad A (Suc n)

-- Zero with explicit size
zeroQ : ( n : Nat4) → Quad A n
zeroQ n = Zero

oneQ : ∀ { n } → Quad Carrier n
oneQ {One} = Scalar 1#
oneQ {Suc n} = Mtx oneQ Zero
                   Zero oneQ

-- Equality

-- eq-Zero is only valid when m ≡ n
data EqQ {A : Set a} (_∼_ : A -> A -> Set d) :
                       (xs : Quad A m) (ys : Quad A n) → Set (a ⊔ d)
                       where

     eq-Zero : ∀ { n } → EqQ _∼_ (zeroQ n) (zeroQ n)

     eq-Scalar : { x y : A } ( x∼y : x ∼ y ) → EqQ _∼_ (Scalar x) (Scalar y)

     eq-Mtx  : { nw1 ne1 sw1 se1 : Quad A m } { nw2 ne2 sw2 se2 : Quad A n }
               ( nw : EqQ _∼_ nw1 nw2 ) ( ne : EqQ _∼_ ne1 ne2 )
               ( sw : EqQ _∼_ sw1 sw2 ) ( se : EqQ _∼_ se1 se2 ) →
               EqQ _∼_ (Mtx nw1 ne1 sw1 se1) (Mtx nw2 ne2 sw2 se2)

_=q_ : Quad Carrier n -> Quad Carrier n -> Set ( c ⊔ ℓ)
_=q_ = EqQ _≈_

-- Functions

mapq : ∀ { A B : Set } → ( A → B ) → Quad A n -> Quad B n
mapq f Zero = Zero
mapq f (Scalar x) = Scalar (f x)
mapq f (Mtx nw ne sw se) = Mtx (mapq f nw) (mapq f ne) (mapq f sw) (mapq f se)

-- Addition on Quads
_+q_ : ( x y : Quad Carrier n) → Quad Carrier n
Zero +q y = y
Scalar x +q Zero = Scalar x
Scalar x +q Scalar x₁ = Scalar (x + x₁)
Mtx x x₁ x₂ x₃ +q Zero = Mtx x x₁ x₂ x₃
Mtx x x₁ x₂ x₃ +q Mtx y y₁ y₂ y₃ = Mtx (x +q y) (x₁ +q y₁) (x₂ +q y₂) (x₃ +q y₃)

-- Multiplication

data Q' ( A : Set a) : Set a where
  Mtx' : ( nw ne sw se : A ) → Q' A

Q'toQuad : Q' (Quad A n) → Quad A (Suc n)
-- Q'toQuad (Mtx' Zero Zero Zero Zero) = Zero
Q'toQuad (Mtx' nw ne sw se) = Mtx nw ne sw se

zipQ' : ( A → B → C ) → Q' A → Q' B → Q' C
zipQ' _op_ (Mtx' nw ne sw se) (Mtx' nw₁ ne₁ sw₁ se₁) = Mtx' (nw op nw₁) (ne op ne₁)
                                                            (sw op sw₁) (se op se₁)

colExchange : Q' A → Q' A
colExchange (Mtx' nw ne sw se) = Mtx' ne nw se sw

prmDiagSqsh : Q' A → Q' A
prmDiagSqsh (Mtx' nw ne sw se) = Mtx' nw se nw se

offDiagSqsh : Q' A → Q' A
offDiagSqsh (Mtx' nw ne sw se) = Mtx' sw ne sw se

_*q_ : ( x y : Quad Carrier n) → Quad Carrier n
Zero *q y = Zero
Scalar x *q Zero = Zero
Scalar x *q Scalar x₁ = Scalar (x * x₁)
Mtx x x₁ x₂ x₃ *q Zero = Zero
Mtx x x₁ x₂ x₃ *q Mtx y y₁ y₂ y₃ =
      let X = Mtx' x x₁ x₂ x₃
          Y = Mtx' y y₁ y₂ y₃
      in Q'toQuad (zipQ' _+q_ (zipQ' _*q_ (colExchange X) (offDiagSqsh Y))
                              (zipQ' _*q_              X  (prmDiagSqsh Y)))

-- Example Quad

q1 : Quad ℕ (Suc One)
q1 = Mtx (Scalar 2) (Scalar 7) Zero Zero

q2 : Quad ℕ (Suc (Suc One))
q2 = Mtx q1 q1 Zero (Mtx (Scalar 1) Zero Zero (Scalar 1))

-- Proofs

quad-refl : { a : Quad Carrier n } → a =q a
quad-refl { n } { Zero } = eq-Zero
quad-refl { n } { (Scalar x) } = eq-Scalar refl
quad-refl { n } { (Mtx a a₁ a₂ a₃) } = eq-Mtx quad-refl quad-refl quad-refl quad-refl

quad-sym : { a b : Quad Carrier n } → a =q b → b =q a
quad-sym eq-Zero = eq-Zero
quad-sym (eq-Scalar x∼y) = eq-Scalar (sym x∼y)
quad-sym (eq-Mtx x x₁ x₂ x₃) = eq-Mtx (quad-sym x) (quad-sym x₁) (quad-sym x₂) (quad-sym x₃)

quad-zerol : ∀ { n } ( x : Quad Carrier n ) → ( Zero +q x ) =q x
quad-zerol x = quad-refl

quad-zeror : ∀ { n } ( x : Quad Carrier n ) → ( x +q Zero ) =q x
quad-zeror Zero = quad-refl
quad-zeror (Scalar x) = quad-refl
quad-zeror (Mtx x x₁ x₂ x₃) = quad-refl

-- Need a proof that Zero is left and right +q-identity
-- Should be some kind of (quad-zerol, quad-zeror)

quad-comm : ( a b : Quad Carrier n ) → ( a +q b) =q ( b +q a )
quad-comm Zero b = quad-sym (quad-zeror b)
quad-comm (Scalar x) Zero = quad-refl
quad-comm (Scalar x) (Scalar x₁) = eq-Scalar (+-comm x x₁)
quad-comm (Mtx a a₁ a₂ a₃) Zero = quad-refl
quad-comm (Mtx a a₁ a₂ a₃) (Mtx b b₁ b₂ b₃) = eq-Mtx (quad-comm a b) (quad-comm a₁ b₁)
                                                     (quad-comm a₂ b₂) (quad-comm a₃ b₃)

quad-assoc : ( a b c : Quad Carrier n ) → ((a +q b ) +q c ) =q ( a +q ( b +q c ))
quad-assoc Zero b c = quad-refl
quad-assoc (Scalar x) Zero c = quad-refl
quad-assoc (Scalar x) (Scalar x₁) Zero = quad-refl
quad-assoc (Scalar x) (Scalar x₁) (Scalar x₂) = eq-Scalar (+-assoc x x₁ x₂)
quad-assoc (Mtx a a₁ a₂ a₃) Zero c = quad-refl
quad-assoc (Mtx a a₁ a₂ a₃) (Mtx b b₁ b₂ b₃) Zero = quad-refl
quad-assoc (Mtx a a₁ a₂ a₃) (Mtx b b₁ b₂ b₃) (Mtx c c₁ c₂ c₃) = eq-Mtx (quad-assoc a  b  c ) (quad-assoc a₁ b₁ c₁)
                                                                       (quad-assoc a₂ b₂ c₂) (quad-assoc a₃ b₃ c₃)

quad-*-zerol : ( x : Quad Carrier n ) → ( Zero *q x ) =q Zero
quad-*-zerol x = eq-Zero

quad-*-zeror : ( x : Quad Carrier n ) → ( x *q Zero ) =q Zero
quad-*-zeror Zero = eq-Zero
quad-*-zeror (Scalar x) = eq-Zero
quad-*-zeror (Mtx x x₁ x₂ x₃) = eq-Zero

quad-onel : ( x : Quad Carrier n ) → ( oneQ *q x ) =q x

quad-onel-lemma : ( x : Quad Carrier n ) → ((oneQ *q x) +q Zero) =q x
quad-onel-lemma {One} Zero = eq-Zero
quad-onel-lemma {Suc n} Zero = eq-Zero
quad-onel-lemma (Scalar x) = eq-Scalar (*-identityˡ x)
quad-onel-lemma (Mtx x x₁ x₂ x₃) = eq-Mtx (quad-onel x) (quad-onel-lemma x₁) (quad-onel-lemma x₂) (quad-onel x₃)

quad-onel Zero = quad-*-zeror oneQ
quad-onel (Scalar x) = eq-Scalar (*-identityˡ x)
quad-onel (Mtx x x₁ x₂ x₃) = eq-Mtx (quad-onel x) (quad-onel-lemma x₁) (quad-onel-lemma x₂) (quad-onel x₃)


text:
-- Andreas, 2016-09-20, issue #2196 reported by mechvel
-- Test case by Ulf

-- {-# OPTIONS -v tc.lhs.dot:40 #-}

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

record _×_ (A B : Set) : Set where
  constructor _,_
  field fst : A
        snd : B
open _×_

EqP₁ : ∀ {A B} (p q : A × B) → Set
EqP₁ (x , y) (z , w) = (x ≡ z) × (y ≡ w)

EqP₂ : ∀ {A B} (p q : A × B) → Set
EqP₂ p q = (fst p ≡ fst q) × (snd p ≡ snd q)

works : {A : Set} (p q : A × A) → EqP₁ p q → Set₁
works (x , y) .(x , y) (refl , refl) = Set

test  : {A : Set} (p q : A × A) → EqP₂ p q → Set₁
test  (x , y) .(x , y) (refl , refl) = Set

-- ERROR WAS:
-- Failed to infer the value of dotted pattern
-- when checking that the pattern .(x , y) has type .A × .A


text:
{-

This file contains:

- The first Eilenberg–Mac Lane type as a HIT

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.EilenbergMacLane1.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Group.Base

private
  variable ℓ : Level

module _ (G : Group {ℓ}) where
  open Group G

  data EM₁ : Type ℓ where
    embase : EM₁
    emloop : Carrier → embase ≡ embase
    emcomp : (g h : Carrier)
           → PathP (λ j → embase ≡ emloop h j) (emloop g) (emloop (g + h))
    -- emsquash : ∀ (x y : EM₁) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s
    emsquash : isGroupoid EM₁

  {- The comp// constructor fills the square:

    emloop (g + h)
    [a]— — — >[c]
     ‖         ^
     ‖         | emloop h     ^
     ‖         |            j |
    [a]— — — >[b]          ∙ — >
       emloop g                i

    We use this to give another constructor-like construction:
  -}

  emloop-comp : (g h : Carrier) → emloop (g + h) ≡ emloop g ∙ emloop h
  emloop-comp g h i = compPath-unique refl (emloop g) (emloop h)
    (emloop (g + h) , emcomp g h)
    (emloop g ∙ emloop h , compPath-filler (emloop g) (emloop h)) i .fst

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.FGIdeal where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Powerset

open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Vec

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal using ()
            renaming (generatedIdeal to generatedIdealCommRing;
                      indInIdeal to ringIncInIdeal;
                      0FGIdeal to 0FGIdealCommRing)
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.CommAlgebra.Ideal

private
  variable
    ℓ : Level
    R : CommRing ℓ

generatedIdeal : {n : ℕ} (A : CommAlgebra R ℓ) → FinVec (fst A) n → IdealsIn A
generatedIdeal A = generatedIdealCommRing (CommAlgebra→CommRing A)

incInIdeal :   {n : ℕ} (A : CommAlgebra R ℓ)
              (U : FinVec ⟨ A ⟩ n) (i : Fin n) → U i ∈ fst (generatedIdeal A U)
incInIdeal A = ringIncInIdeal (CommAlgebra→CommRing A)

syntax generatedIdeal A V = ⟨ V ⟩[ A ]

module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
  open CommAlgebraStr (snd A)

  0FGIdeal : {n : ℕ} → ⟨ replicateFinVec n 0a ⟩[ A ] ≡ (0Ideal A)
  0FGIdeal = 0FGIdealCommRing (CommAlgebra→CommRing A)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --without-K  #-}
module algebra.monoid.morphism where

open import level
open import algebra.monoid.core
open import algebra.semigroup.morphism
open import equality.core
open import function.isomorphism
open import hott.level
open import sum

module _ {i}{j}
         {X : Set i}⦃ sX : IsMonoid X ⦄
         {Y : Set j}⦃ sY : IsMonoid Y ⦄ where
  open IsMonoid ⦃ ... ⦄

  record IsMonoidMorphism (f : X → Y) : Set (i ⊔ j) where
    constructor mk-is-monoid-morphism
    field
      sgrp-mor : IsSemigroupMorphism f
      id-pres : f e ≡ e

  is-monoid-morphism-struct-iso : (f : X → Y)
    → IsMonoidMorphism f ≅ (IsSemigroupMorphism f × (f e ≡ e))
  is-monoid-morphism-struct-iso f = record
    { to = λ mor → ( IsMonoidMorphism.sgrp-mor mor
                   , IsMonoidMorphism.id-pres mor )
    ; from = λ { (s , i) → mk-is-monoid-morphism s i }
    ; iso₁ = λ _ → refl
    ; iso₂ = λ _ → refl }

  is-monoid-morphism-level : (f : X → Y) → h 1 (IsMonoidMorphism f)
  is-monoid-morphism-level f =
    iso-level (sym≅ (is-monoid-morphism-struct-iso f))
    (×-level (is-semigroup-morphism-level f)
    (is-set _ _))

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-

  DUARel for the constant unit family

-}
{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Displayed.Unit where

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

open import Cubical.Data.Unit

open import Cubical.Displayed.Base
open import Cubical.Displayed.Constant

private
  variable
    ℓA ℓ≅A : Level

𝒮-Unit : UARel Unit ℓ-zero
𝒮-Unit .UARel._≅_ _ _ = Unit
𝒮-Unit .UARel.ua _ _ = invEquiv (isContr→≃Unit (isProp→isContrPath isPropUnit _ _))

𝒮ᴰ-Unit : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) → DUARel 𝒮-A (λ _ → Unit) ℓ-zero
𝒮ᴰ-Unit 𝒮-A = 𝒮ᴰ-const 𝒮-A 𝒮-Unit

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
------------------------------------------------------------------------
-- Compiler correctness
------------------------------------------------------------------------

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

module Lambda.Simplified.Delay-monad.Compiler-correctness where

import Equality.Propositional as E
open import Prelude
open import Prelude.Size

open import Monad E.equality-with-J
open import Vec.Function E.equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Monad

open import Lambda.Simplified.Compiler
open import Lambda.Simplified.Delay-monad.Interpreter
open import Lambda.Simplified.Delay-monad.Virtual-machine
open import Lambda.Simplified.Syntax
open import Lambda.Simplified.Virtual-machine

private
  module C = Closure Code
  module T = Closure Tm

-- Compiler correctness.

mutual

  ⟦⟧-correct :
    ∀ {i n} t {ρ : T.Env n} {c s}
      {k : T.Value → Delay (Maybe C.Value) ∞} →
    (∀ v → [ i ] exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈ k v) →
    [ i ] exec ⟨ comp t c , s , comp-env ρ ⟩ ≈ ⟦ t ⟧ ρ >>= k

  ⟦⟧-correct (var x) {ρ} {c} {s} {k} hyp =
    exec ⟨ var x ∷ c , s , comp-env ρ ⟩                 ≳⟨⟩
    exec ⟨ c , val (comp-val (ρ x)) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (ρ x) ⟩∼
    k (ρ x)                                             ∼⟨⟩
    ⟦ var x ⟧ ρ >>= k                                   ∎

  ⟦⟧-correct (ƛ t) {ρ} {c} {s} {k} hyp =
    exec ⟨ clo (comp t (ret ∷ [])) ∷ c , s , comp-env ρ ⟩   ≳⟨⟩
    exec ⟨ c , val (comp-val (T.ƛ t ρ)) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (T.ƛ t ρ) ⟩∼
    k (T.ƛ t ρ)                                             ∼⟨⟩
    ⟦ ƛ t ⟧ ρ >>= k                                         ∎

  ⟦⟧-correct (t₁ · t₂) {ρ} {c} {s} {k} hyp =
    exec ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩      ≈⟨ (⟦⟧-correct t₁ λ v₁ → ⟦⟧-correct t₂ λ v₂ → ∙-correct v₁ v₂ hyp) ⟩∼

    (⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂ >>= k)    ∼⟨ (⟦ t₁ ⟧ ρ ∎) >>=-cong (λ _ → associativity′ (⟦ t₂ ⟧ ρ) _ _) ⟩

    (⟦ t₁ ⟧ ρ >>= λ v₁ → (⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂) >>= k)  ∼⟨ associativity′ (⟦ t₁ ⟧ ρ) _ _ ⟩

    ⟦ t₁ · t₂ ⟧ ρ >>= k                                        ∎

  ∙-correct :
    ∀ {i n} v₁ v₂ {ρ : T.Env n} {c s}
      {k : T.Value → Delay (Maybe C.Value) ∞} →
    (∀ v → [ i ] exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈ k v) →
    [ i ] exec ⟨ app ∷ c
               , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
               , comp-env ρ
               ⟩ ≈
          v₁ ∙ v₂ >>= k
  ∙-correct (T.ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} hyp =
    exec ⟨ app ∷ c
         , val (comp-val v₂) ∷ val (comp-val (T.ƛ t₁ ρ₁)) ∷ s
         , comp-env ρ
         ⟩                                                     ≈⟨ later (λ { .force →

      exec ⟨ comp t₁ (ret ∷ [])
           , ret c (comp-env ρ) ∷ s
           , cons (comp-val v₂) (comp-env ρ₁)
           ⟩                                                        ≡⟨ E.cong (λ ρ′ →
                                                                                exec ⟨ comp t₁ (ret ∷ []) , ret c (comp-env ρ) ∷ s , ρ′ ⟩) $
                                                                              E.sym comp-cons ⟩
      exec ⟨ comp t₁ (ret ∷ [])
           , ret c (comp-env ρ) ∷ s
           , comp-env (cons v₂ ρ₁)
           ⟩                                                        ≈⟨ ⟦⟧-correct t₁ (λ v →

        exec ⟨ ret ∷ []
             , val (comp-val v) ∷ ret c (comp-env ρ) ∷ s
             , comp-env (cons v₂ ρ₁)
             ⟩                                                           ≳⟨⟩

        exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩                   ≈⟨ hyp v ⟩∎

        k v                                                              ∎) ⟩∼

      ⟦ t₁ ⟧ (cons v₂ ρ₁) >>= k                                     ∎ }) ⟩∎

    T.ƛ t₁ ρ₁ ∙ v₂ >>= k                                       ∎

-- Note that the equality that is used here is syntactic.

correct :
  ∀ t →
  exec ⟨ comp t [] , [] , nil ⟩ ≈
  ⟦ t ⟧ nil >>= λ v → return (just (comp-val v))
correct t =
  exec ⟨ comp t [] , [] , nil ⟩                     ≡⟨ E.cong (λ ρ → exec ⟨ comp t [] , [] , ρ ⟩) $ E.sym comp-nil ⟩
  exec ⟨ comp t [] , [] , comp-env nil ⟩            ≈⟨ ⟦⟧-correct t (λ v → return (just (comp-val v)) ∎) ⟩
  (⟦ t ⟧ nil >>= λ v → return (just (comp-val v)))  ∎

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module omega-automaton where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.List
open import Data.Maybe
-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary -- using (not_; Dec; yes; no)
open import Data.Empty

open import logic
open import automaton

open Automaton

ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q ) →  ℕ → ( ℕ → Σ )  → Q
ω-run Ω x zero s = x
ω-run Ω x (suc n) s = δ Ω (ω-run Ω x n s) ( s n )

--
-- accept as Buchi automaton
--
record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
    field
        from : ℕ
        stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x n S ) ≡ true

open Buchi

--  after sometimes, always p
--
--                       not p
--                   ------------>
--        <> [] p *                 <> [] p
--                   <-----------
--                       p

--
-- accept as Muller automaton
--
record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
    field
        next     : (n : ℕ ) → ℕ
        infinite : (x : Q) → (n : ℕ ) →  aend Ω ( ω-run Ω x (n + (next n)) S ) ≡ true

--  always sometimes p
--
--                       not p
--                   ------------>
--        [] <> p *                 [] <> p
--                   <-----------
--                       p

data  States3   : Set  where
   ts* : States3
   ts  : States3

transition3 : States3  → Bool  → States3
transition3 ts* true  = ts*
transition3 ts* false  = ts
transition3 ts true  = ts*
transition3 ts false  = ts

mark1 :  States3  → Bool
mark1 ts* = true
mark1 ts = false

ωa1 : Automaton States3 Bool
ωa1 = record {
        δ = transition3
     ;  aend = mark1
  }

true-seq :  ℕ → Bool
true-seq _ = true

false-seq :  ℕ → Bool
false-seq _ = false

flip-seq :  ℕ → Bool
flip-seq zero = false
flip-seq (suc n) = not ( flip-seq n )

lemma0 : Muller ωa1 flip-seq
lemma0 = record {
        next = λ n → suc (suc n)
      ; infinite = lemma01
   } where
        lemma01 :  (x : States3) (n : ℕ) →
           aend ωa1 (ω-run ωa1 x (n + suc (suc n)) flip-seq) ≡ true
        lemma01 = {!!}

lemma1 : Buchi ωa1 true-seq
lemma1 = record {
        from = zero
      ; stay = {!!}
   } where
      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} n true-seq ) ≡ true
      lem1 zero ()
      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} n true-seq
      lem1 (suc n) (s≤s z≤n) | ts* = {!!}
      lem1 (suc n) (s≤s z≤n) | ts = {!!}

ωa2 : Automaton States3 Bool
ωa2 = record {
        δ = transition3
     ;  aend = λ x → not ( mark1 x )
  }

flip-dec : (n : ℕ ) →  Dec (  flip-seq n   ≡ true )
flip-dec n with flip-seq n
flip-dec n | false = no  λ ()
flip-dec n | true = yes refl

flip-dec1 : (n : ℕ ) → flip-seq (suc n)  ≡ ( not ( flip-seq n ) )
flip-dec1 n = let open ≡-Reasoning in
          flip-seq (suc n )
       ≡⟨⟩
          ( not ( flip-seq n ) )
       ∎

flip-dec2 : (n : ℕ ) → not flip-seq (suc n)  ≡  flip-seq n
flip-dec2 n = {!!}

record flipProperty : Set where
    field
       flipP : (n : ℕ) →  ω-run ωa2 {!!} {!!} ≡ ω-run ωa2 {!!} {!!}

lemma2 : Muller ωa2 flip-seq
lemma2 = record {
          next = next
       ;  infinite = {!!}
   }  where
     next : ℕ → ℕ
     next = {!!}
     infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 {!!} ≡ true → aend ωa2 {!!} ≡ true
     infinite' = {!!}
     infinite : (n : ℕ) → aend ωa2 {!!} ≡ true
     infinite = {!!}

lemma3 : Buchi ωa1 false-seq  →  ⊥
lemma3 = {!!}

lemma4 : Muller ωa1 flip-seq  →  ⊥
lemma4 = {!!}

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
-- Andreas, 2019-05-03, issue #3742, reported by nad
--
-- Regression introduced in 2.5.2:
--
-- getConstInfo applied to abstract constructor D.c
-- in metaOccurs check throws funny "not in scope" error for D.c

record Σ (A : Set) (B : A → Set₁) : Set₁ where

mutual

  abstract

    data D (A : Set) : Set where
      c : D A

  F : Set → Set₁
  F A = Σ _ λ (_ : D A) → Set

-- Should succeed.


text:
------------------------------------------------------------------------
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Props.AbelianGroup (g : AbelianGroup) where

open AbelianGroup g
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Data.Function
open import Data.Product

private
  lemma : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
  lemma x y = begin
    x ∙ y ∙ x ⁻¹    ≈⟨ comm _ _ ⟨ ∙-pres-≈ ⟩ refl ⟩
    y ∙ x ∙ x ⁻¹    ≈⟨ assoc _ _ _ ⟩
    y ∙ (x ∙ x ⁻¹)  ≈⟨ refl ⟨ ∙-pres-≈ ⟩ proj₂ inverse _ ⟩
    y ∙ ε           ≈⟨ proj₂ identity _ ⟩
    y               ∎

-‿∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
-‿∙-comm x y = begin
  x ⁻¹ ∙ y ⁻¹                         ≈⟨ comm _ _ ⟩
  y ⁻¹ ∙ x ⁻¹                         ≈⟨ sym $ lem ⟨ ∙-pres-≈ ⟩ refl ⟩
  x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ∙ x ⁻¹  ≈⟨ lemma _ _ ⟩
  y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹               ≈⟨ lemma _ _ ⟩
  (x ∙ y) ⁻¹                          ∎
  where
  lem = begin
    x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹)  ≈⟨ sym $ assoc _ _ _ ⟩
    x ∙ (y ∙ (x ∙ y) ⁻¹) ∙ y ⁻¹  ≈⟨ sym $ assoc _ _ _ ⟨ ∙-pres-≈ ⟩ refl ⟩
    x ∙ y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹    ≈⟨ proj₂ inverse _ ⟨ ∙-pres-≈ ⟩ refl ⟩
    ε ∙ y ⁻¹                     ≈⟨ proj₁ identity _ ⟩
    y ⁻¹                         ∎

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2016-11-03, issue #2211
-- The occurs check did not take variables labeled as `UnusedArg`
-- on the left hand side into consideration.

-- {-# OPTIONS -v tc.check.term:40 #-}
-- {-# OPTIONS -v tc.meta:45 #-}
-- {-# OPTIONS -v tc.polarity:20 #-}

open import Agda.Builtin.Equality
open import Common.Nat

cong : ∀{A B : Set}(f : A → B) (x y : A) → x ≡ y → f x ≡ f y
cong _ _ _ refl = refl

data ⊥ : Set where

⊥-elim : ∀{A : Set} → ⊥ {- unused arg -} → A
⊥-elim ()

data Fin : Nat → Set where
  zero : {n : Nat} → Fin (suc n)
  suc  : {n : Nat} (i : Fin n) → Fin (suc n)

toNat : ∀ {n} → Fin n → Nat
toNat zero    = 0
toNat (suc i) = suc (toNat i)

tighten : ∀ n (x : Fin (suc n)) (neq : (toNat x ≡ n → ⊥) {- unused arg x-}) → Fin n
tighten zero    zero    neq = ⊥-elim (neq refl)
tighten (suc n) zero    neq = zero
tighten zero    (suc ())
tighten (suc n) (suc x) neq = suc (tighten n x (λ p → neq (cong suc _ _ p)))

tighten-correct : ∀ n (x : Fin (suc n)) (neq : toNat x ≡ n → ⊥) →
  toNat (tighten n x neq) ≡ toNat x
tighten-correct zero    zero    neq = ⊥-elim (neq refl)
tighten-correct (suc n) zero    neq = refl
tighten-correct zero    (suc ())
tighten-correct (suc n) (suc x) neq =
  cong suc _ _ (tighten-correct n x (λ p → neq (cong Nat.suc  _ _ p)))

-- ERROR WAS:
-- Cannot instantiate ... because it contains the variable neg ...

-- Should succeed.

{-
term _62 n x neq
     (toNat (tighten n x (λ p → neq (cong suc p)))) := suc
                                                       (toNat
                                                        (tighten n x (λ p → neq (cong suc p))))
term _62 n x neq (toNat x) := toNat (suc x)

after kill analysis
  metavar = _62
  kills   = [False,False,True,False]
  kills'  = [ru(False),ru(False),ru(True),ru(False)]
  oldType = (n₁ : Nat) (x₁ : Fin (suc n₁))
            (neq₁ : toNat (suc x₁) ≡ suc n₁ → ⊥) →
            Nat → Nat
  newType = (n₁ : Nat) → Fin (suc n₁) → Nat → Nat
actual killing
  new meta: _69
  kills   : [ru(False),ru(False),ru(True),ru(False)]
  inst    : _62 := _69 @3 n neq

term _69 n x (toNat (tighten n x (λ p → neq (cong suc p)))) := suc
                                                               (toNat
                                                                (tighten n x
                                                                 (λ p → neq (cong suc p))))

Here, the variable neq on the lhs was not considered eligible for occurrence on the rhs
since it is contained in an unused arg only.
-}


text:
-- Minimal implicational modal logic, PHOAS approach, initial encoding

module Pi.BoxMp where

open import Lib using (Nat; suc)

-- Types

infixr 0 _=>_
data Ty : Set where
  UNIT :             Ty
  _=>_ : Ty -> Ty -> Ty
  BOX  : Ty       -> Ty

-- Context and truth judgement with modal depth

Cx : Set1
Cx = Ty -> Nat -> Set

isTrue : Ty -> Nat -> Cx -> Set
isTrue a d tc = tc a d

-- Terms

module BoxMp where
  infixl 1 _$_
  data Tm (d : Nat) (tc : Cx) : Ty -> Set where
    var    : forall {a}      -> isTrue a d tc                 -> Tm d tc a
    lam'   : forall {a b}    -> (isTrue a d tc -> Tm d tc b)  -> Tm d tc (a => b)
    _$_    : forall {a b}    -> Tm d tc (a => b) -> Tm d tc a -> Tm d tc b
    box    : forall {a}      -> Tm (suc d) tc a               -> Tm d tc (BOX a)
    unbox' : forall {>d a b} -> Tm d tc (BOX a)  -> (isTrue a >d tc -> Tm d tc b) -> Tm d tc b

  lam'' : forall {d tc a b} -> (Tm d tc a -> Tm d tc b) -> Tm d tc (a => b)
  lam'' f = lam' \x -> f (var x)

  unbox'' : forall {d >d tc a b} -> Tm d tc (BOX a) -> (Tm >d tc a -> Tm d tc b) -> Tm d tc b
  unbox'' x f = unbox' x \y -> f (var y)

  syntax lam''   (\a -> b)    = lam a => b
  syntax unbox'' x' (\x -> y) = unbox x' as x => y

  Thm : Ty -> Set1
  Thm a = forall {d tc} -> Tm d tc a
open BoxMp public

-- Example theorems

rNec : forall {a} -> Thm a -> Thm (BOX a)
rNec x =
  box x

aK : forall {a b} -> Thm (BOX (a => b) => BOX a => BOX b)
aK =
  lam f' =>
    lam x' =>
      unbox f' as f =>
        unbox x' as x =>
          box (f $ x)

aT : forall {a} -> Thm (BOX a => a)
aT =
  lam x' =>
    unbox x' as x => x

a4 : forall {a} -> Thm (BOX a => BOX (BOX a))
a4 =
  lam x' =>
    unbox x' as x => box (box x)

t1 : forall {a} -> Thm (a => BOX (a => a))
t1 =
  lam _ => box (lam y => y)

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module Numeric.Nat.Properties where

open import Prelude hiding (less-antisym; less-antirefl; leq-antisym)
open import Prelude.Nat.Properties public
open import Tactic.Nat

--- Subtraction ---

sub-less : {a b : Nat} → a ≤ b → b - a + a ≡ b
sub-less {zero} _ = auto
sub-less {suc a} (diff! k) = auto

sub-underflow : (a b : Nat) → a ≤ b → a - b ≡ 0
sub-underflow a ._ (diff! k) = auto

sub-leq : (a b : Nat) → a - b ≤ a
sub-leq a b with compare a b
sub-leq a ._ | less    (diff! k) = diff a auto
sub-leq a .a | equal    refl     = diff a auto
sub-leq ._ b | greater (diff! k) = diff b auto

--- LessNat ---

fast-diff : {a b : Nat} → a < b → a < b
fast-diff {a} {b} a<b = diff (b - suc a) (eraseEquality $ by (sub-less {suc a} {b} (by a<b)))
{-# INLINE fast-diff #-}

infixr 0 _⟨<⟩_ _⟨≤⟩_

_⟨<⟩_ : ∀ {x y z} → LessNat x y → LessNat y z → LessNat x z
diff! a ⟨<⟩ diff! b = diff (suc (b + a)) auto

less-antirefl : ∀ {a b : Nat} → a < b → ¬ (a ≡ b)
less-antirefl (diff! k) eq = refute eq

less-not-geq : ∀ {a b : Nat} → a < b → b ≤ a → ⊥
less-not-geq (diff d eq) (diff! d₁) = refute eq

less-raa : {a b : Nat} → ¬ (suc a > b) → a < b
less-raa {a} {b} a≱b with compare a b
less-raa a≱b | less    a<b = a<b
less-raa a≱b | equal  refl = ⊥-elim (a≱b auto)
less-raa a≱b | greater a>b = ⊥-elim (a≱b (by a>b))

_⟨≤⟩_ : {a b c : Nat} → a ≤ b → b ≤ c → a ≤ c
diff! k ⟨≤⟩ diff! k₁ = auto

private
  leq-mul-r′ : ∀ a b → NonZero b → a ≤ a * b
  leq-mul-r′ _  zero ()
  leq-mul-r′ a (suc b) _ = auto

leq-mul-r : ∀ a b {{_ : NonZero b}} → a ≤ a * b
leq-mul-r a b = fast-diff (leq-mul-r′ _ b it)

-- Used for the well-founded induction over factorisation.
less-mul-l : {a b : Nat} → a > 1 → b > 1 → a < a * b
less-mul-l (diff! k) (diff! j) = auto

less-mul-r : {a b : Nat} → a > 1 → b > 1 → b < a * b
less-mul-r (diff! k) (diff! j) = auto

add-nonzero-l : ∀ a b {{_ : NonZero a}} → NonZero (a + b)
add-nonzero-l zero    b {{}}
add-nonzero-l (suc a) b = _

add-nonzero-r : ∀ a b {{_ : NonZero b}} → NonZero (a + b)
add-nonzero-r zero    zero {{}}
add-nonzero-r zero    (suc b) = _
add-nonzero-r (suc a) b       = _

mul-nonzero : ∀ a b {{nza : NonZero a}} {{nzb : NonZero b}} → NonZero (a * b)
mul-nonzero zero    b    {{nza = ()}}
mul-nonzero (suc a) zero {{nzb = ()}}
mul-nonzero (suc a) (suc b) = _

mul-nonzero-l : ∀ a b {{_ : NonZero (a * b)}} → NonZero a
mul-nonzero-l 0 _ {{}}
mul-nonzero-l (suc _) _ = _

mul-nonzero-r : ∀ a b {{_ : NonZero (a * b)}} → NonZero b
mul-nonzero-r a b {{nz}} = mul-nonzero-l b a {{transport NonZero auto nz}}

mul-unit-l : ∀ a b {{_ : NonZero b}} → a * b ≡ b → a ≡ 1
mul-unit-l 1 _ _ = refl
mul-unit-l 0 .0 {{}} refl
mul-unit-l (suc (suc a)) zero {{}} _
mul-unit-l (suc (suc a)) (suc b) ab=b = refute ab=b

mul-unit-r : ∀ a b {{_ : NonZero a}} → a * b ≡ a → b ≡ 1
mul-unit-r a b ab=a = mul-unit-l b a (mul-commute b a ⟨≡⟩ ab=a)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category

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

open import Level
open import Relation.Binary using (IsEquivalence; Setoid)

open Category C

Mono : ∀ {A B} → (f : A ⇒ B) → Set _
Mono {A} f = ∀ {C} → (g₁ g₂ : C ⇒ A) → f ∘ g₁ ≡ f ∘ g₂ → g₁ ≡ g₂

Epi : ∀ {B A} → (f : A ⇒ B) → Set _
Epi {B} f = ∀ {C} → (g₁ g₂ : B ⇒ C) → g₁ ∘ f ≡ g₂ ∘ f → g₁ ≡ g₂

record Iso {A B} (f : A ⇒ B) (g : B ⇒ A) : Set (o ⊔ ℓ ⊔ e) where
  field
    .isoˡ : g ∘ f ≡ id
    .isoʳ : f ∘ g ≡ id

infix 4 _≅_
record _≅_ (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    f : A ⇒ B
    g : B ⇒ A
    .iso : Iso f g
  .isoˡ : _
  isoˡ = Iso.isoˡ iso
  .isoʳ : _
  isoʳ = Iso.isoʳ iso

infix 4 _ⓘ_
_ⓘ_ : ∀ {X Y Z} → Y ≅ Z → X ≅ Y → X ≅ Z
G ⓘ F = record
  { f = G.f ∘ F.f
  ; g = F.g ∘ G.g
  ; iso = record
    { isoˡ =
      begin
        (F.g ∘ G.g) ∘ (G.f ∘ F.f)
      ↓⟨ assoc ⟩
        F.g ∘ (G.g ∘ (G.f ∘ F.f))
      ↑⟨ refl ⟩∘⟨ assoc ⟩
        F.g ∘ (G.g ∘ G.f) ∘ F.f
      ↓⟨ refl ⟩∘⟨ G.isoˡ ⟩∘⟨ refl ⟩
        F.g ∘ (id ∘ F.f)
      ↓⟨ refl ⟩∘⟨ identityˡ ⟩
        F.g ∘ F.f
      ↓⟨ F.isoˡ ⟩
        id
      ∎
    ; isoʳ =
      begin
        (G.f ∘ F.f) ∘ (F.g ∘ G.g)
      ↓⟨ assoc ⟩
        G.f ∘ (F.f ∘ (F.g ∘ G.g))
      ↑⟨ refl ⟩∘⟨ assoc ⟩
        G.f ∘ (F.f ∘ F.g) ∘ G.g
      ↓⟨ refl ⟩∘⟨ F.isoʳ ⟩∘⟨ refl ⟩
        G.f ∘ (id ∘ G.g)
      ↓⟨ refl ⟩∘⟨ identityˡ ⟩
        G.f ∘ G.g
      ↓⟨ G.isoʳ ⟩
        id
      ∎
    }
  }
  where
  module F = _≅_ F
  module G = _≅_ G
  open Iso
  open Equiv
  open HomReasoning

idⁱ : ∀ {A} → A ≅ A
idⁱ {A} = record
  { f = id
  ; g = id
  ; iso = record
    { isoˡ = identityˡ
    ; isoʳ = identityˡ
    }
  }

reverseⁱ : ∀ {A B} → A ≅ B → B ≅ A
reverseⁱ A≅B = record
  { f = A≅B.g
  ; g = A≅B.f
  ; iso = record
    { isoˡ = A≅B.isoʳ
    ; isoʳ = A≅B.isoˡ
    }
  }
  where
  module A≅B = _≅_ A≅B

≅-is-equivalence : IsEquivalence _≅_
≅-is-equivalence = record
  { refl = idⁱ
  ; sym = reverseⁱ
  ; trans = λ x y → y ⓘ x
  }

≅-setoid : Setoid o (o ⊔ ℓ ⊔ e)
≅-setoid = record
  { Carrier = Obj
  ; _≈_ = _≅_
  ; isEquivalence = ≅-is-equivalence
  }

-- equality of isos induced from arrow equality
-- could just use a pair, but this way is probably clearer

record _≡ⁱ_ {A B : Obj} (i j : A ≅ B) : Set (o ⊔ ℓ ⊔ e) where
  open _≅_
  field
    f-≡ : f i ≡ f j
    g-≡ : g i ≡ g j

.≡ⁱ-is-equivalence : ∀ {A B} → IsEquivalence (_≡ⁱ_ {A} {B})
≡ⁱ-is-equivalence = record
  { refl = record { f-≡ = refl; g-≡ = refl }
  ; sym = λ x → record { f-≡ = sym (f-≡ x); g-≡ = sym (g-≡ x) }
  ; trans = λ x y → record { f-≡ = trans (f-≡ x) (f-≡ y); g-≡ = trans (g-≡ x) (g-≡ y) }
  }
  where
  open Equiv
  open _≡ⁱ_

{-
≡ⁱ-setoid : ∀ {A B} → Setoid (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
≡ⁱ-setoid {A} {B} = record
  { Carrier = A ≅ B; _≈_ = _≡ⁱ_; isEquivalence = ≡ⁱ-is-equivalence }
-}

-- groupoid with only isos
Isos : Category o (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
Isos = record
  { Obj = Obj
  ; _⇒_ = _≅_
  ; _≡_ = _≡ⁱ_
  ; id = idⁱ
  ; _∘_ = _ⓘ_
  ; assoc = λ {A B C D f g h} → record { f-≡ = assoc; g-≡ = sym assoc }
  ; identityˡ = λ {A B f} → record { f-≡ = identityˡ; g-≡ = identityʳ }
  ; identityʳ = λ {A B f} → record { f-≡ = identityʳ; g-≡ = identityˡ }
  ; equiv = ≡ⁱ-is-equivalence
  ; ∘-resp-≡ = λ {A B C f h g i} f≡ⁱh g≡ⁱi → record
    { f-≡ = ∘-resp-≡ (f-≡ f≡ⁱh) (f-≡ g≡ⁱi)
    ; g-≡ = ∘-resp-≡ (g-≡ g≡ⁱi) (g-≡ f≡ⁱh)
    }
  }
  where
  open Equiv
  open _≡ⁱ_

-- heterogeneous equality of isos
open Heterogeneous Isos public using () renaming (_∼_ to _∼ⁱ_; ≡⇒∼ to ≡⇒∼ⁱ; ∼⇒≡ to ∼⇒≡ⁱ; refl to ∼ⁱ-refl; sym to ∼ⁱ-sym; trans to ~ⁱ-trans; ∘-resp-∼ to ∘-resp-∼ⁱ; ∘-resp-∼ˡ to ∘-resp-∼ⁱˡ; ∘-resp-∼ʳ to ∘-resp-∼ⁱʳ; domain-≣ to domain-≣ⁱ; codomain-≣ to codomain-≣ⁱ)

private
  f-∼′ : ∀ {A B} {i : A ≅ B} {A′ B′} {j : A′ ≅ B′} (eq : i ∼ⁱ j) → Heterogeneous._∼_ C (_≅_.f i) (_≅_.f j)
  f-∼′ (≡⇒∼ⁱ eq) = ≡⇒∼ (f-≡ eq)
    where
    open Heterogeneous C
    open _≡ⁱ_

  g-∼′ : ∀ {A B} {i : A ≅ B} {A′ B′} {j : A′ ≅ B′} (eq : i ∼ⁱ j) → Heterogeneous._∼_ C (_≅_.g i) (_≅_.g j)
  g-∼′ (≡⇒∼ⁱ eq) = ≡⇒∼ (g-≡ eq)
    where
    open Heterogeneous C
    open _≡ⁱ_

heqⁱ : ∀ {A B} (i : A ≅ B) {A′ B′} (j : A′ ≅ B′) → let open _≅_ in let open Heterogeneous C in f i ∼ f j → g i ∼ g j → i ∼ⁱ j
heqⁱ i j (Heterogeneous.≡⇒∼ eq-f) (Heterogeneous.≡⇒∼ eq-g)
  = ≡⇒∼ⁱ {f = i} {g = j} (record { f-≡ = eq-f; g-≡ = eq-g })

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Data.Pi.Base where

open import Level

Π : (A : Type a) (B : A → Type b) → Type _
Π A B = (x : A) → B x

∀′ : {A : Type a} (B : A → Type b) → Type _
∀′ {A = A} B = Π A B

infixr 4.5 ∀-syntax
∀-syntax : ∀ {a b} {A : Type a} (B : A → Type b) → Type (a ℓ⊔ b)
∀-syntax = ∀′

syntax ∀-syntax (λ x → e) = ∀[ x ] e

infixr 4.5 Π⦂-syntax
Π⦂-syntax : (A : Type a) (B : A → Type b) → Type (a ℓ⊔ b)
Π⦂-syntax = Π

syntax Π⦂-syntax t (λ x → e) = Π[ x ⦂ t ] e

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Thesis.IntChanges where

open import Data.Integer.Base
open import Relation.Binary.PropositionalEquality

open import Thesis.Changes
open import Theorem.Groups-Nehemiah

private
  intCh = ℤ
instance
  intCS : ChangeStructure ℤ
intCS = record
  { Ch = ℤ
  ; ch_from_to_ = λ dv v1 v2 → v1 + dv ≡ v2
  ; isCompChangeStructure = record
    { isChangeStructure = record
      { _⊕_ = _+_
      ; fromto→⊕ = λ dv v1 v2 v2≡v1+dv → v2≡v1+dv
      ; _⊝_ = _-_
      ; ⊝-fromto = λ a b → n+[m-n]=m {a} {b}
      }
    ; _⊚_ = λ da1 da2 → da1 + da2
    ; ⊚-fromto = i⊚-fromto
    }
  }
  where
    i⊚-fromto : (a1 a2 a3 : ℤ) (da1 da2 : intCh) →
      a1 + da1 ≡ a2 → a2 + da2 ≡ a3 → a1 + (da1 + da2) ≡ a3
    i⊚-fromto a1 a2 a3 da1 da2 a1+da1≡a2 a2+da2≡a3
      rewrite sym (associative-int a1 da1 da2) | a1+da1≡a2 = a2+da2≡a3

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 -v tc.lhs.unify:50 #-}
module Issue81 where

data ⊥ : Set where

data D : Set where
  d : D
  c : D

data E : Set where
  e : E

⌜_⌝ : E -> D
⌜ e ⌝ = c

data R : D -> E -> Set where
  Val : (v : E) -> R ⌜ v ⌝ v

foo : R d e -> ⊥
foo ()

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Primitive
open import Agda.Builtin.Sigma

variable
  ℓ₁ ℓ₂ : Level

is-universal-element : {X : Set ℓ₁} {A : X → Set ℓ₂} → Σ X A → Set (ℓ₁ ⊔ ℓ₂)
is-universal-element {ℓ₁} {ℓ₂} {X} {A} (x , a) = ∀ y → A y

fails : {X : Set ℓ₁} {A : X → Set ℓ₂} (x : X) (a : A x)
      → is-universal-element {A = _} (x , a) → (y : X) → A y -- a is yellow
fails {ℓ₁} {ℓ₂} {X = X} {A} x a u y = u y

works : ∀ {ℓ₁} {ℓ₂} {X : Set ℓ₁} {A : X → Set ℓ₂} (x : X) (a : A x)
      → is-universal-element {A = _} (x , a) → (y : X) → A y
works x a u y = u y