text:
module Prelude.Bool.Properties where

open import Prelude.Equality
open import Prelude.Bool
open import Prelude.Decidable
open import Prelude.Empty
open import Prelude.Variables

de-morg-neg-conj : (a b : Bool) → not (a && b) ≡ (not a || not b)
de-morg-neg-conj true true = refl
de-morg-neg-conj false true = refl
de-morg-neg-conj true false  = refl
de-morg-neg-conj false false  = refl

de-morg-neg-disj : (a b : Bool) → not (a || b) ≡ (not a && not b)
de-morg-neg-disj true true = refl
de-morg-neg-disj false true = refl
de-morg-neg-disj true false = refl
de-morg-neg-disj false false = refl

x||true : (x : Bool) → (x || true) ≡ true
x||true true = refl
x||true false = refl

x&&false : (x : Bool) → (x && false) ≡ false
x&&false true = refl
x&&false false = refl

IsTrue⇒≡ : IsTrue x → x ≡ true
IsTrue⇒≡ true = refl

IsFalse⇒≡ : IsFalse x → x ≡ false
IsFalse⇒≡ false = refl

not[x]≡false⇒x≡true : not x ≡ false → x ≡ true
not[x]≡false⇒x≡true {true} _ = refl
not[x]≡false⇒x≡true {false} ()

not[x]≡true⇒x≡false : not x ≡ true → x ≡ false
not[x]≡true⇒x≡false {true} ()
not[x]≡true⇒x≡false {false} _ = refl

-- Properties of ==? --
module _ {a} {A : Set a} {{EqA : Eq A}} where

  ==?-reflexive : (x : A) → (x ==? x) ≡ true
  ==?-reflexive x with  x == x
  ...| yes refl = refl
  ...| no notEq = ⊥-elim (notEq refl)

  ≡⇒==? : {x y : A} → (x ≡ y) → (x ==? y) ≡ true
  ≡⇒==? {x = x} {y = y} refl with x == y
  ...| yes refl = refl
  ...| no a≢b = ⊥-elim (a≢b refl)

  ≢⇒==? : {x y : A} → x ≢ y → (x ==? y) ≡ false
  ≢⇒==? {x = x} {y = y} x≢y with x == y
  ...| yes x≡y = ⊥-elim (x≢y x≡y)
  ...| no _ = refl

  ==?⇒≡ : {x y : A} → (x ==? y) ≡ true → x ≡ y
  ==?⇒≡ {x = x} {y = y} ==?≡true
    with x == y
  ...| yes x≡y = x≡y
  ...| no x≢y with (≢⇒==? x≢y) | ==?≡true
  ...| _ | ()

  ==?≡false⇒≢ : {a b : A} → (a ==? b) ≡ false → a ≢ b
  ==?≡false⇒≢ {a = a} {b = b} ==?≡false
    with a == b
  ...| no ¬eq = ¬eq
  ...| yes eq with ≡⇒==? | ==?≡false
  ...| _ | ()

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
module Integer where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Binary.PropositionalEquality

data ℤ₃ : Set where
  ℤ₊ : ℕ → ℤ₃
  ℤ₀ : ℤ₃
  ℤ₋ : ℕ → ℤ₃

ℤ₊-injective : ∀ {m n} → ℤ₊ m ≡ ℤ₊ n → m ≡ n
ℤ₊-injective refl = refl

ℤ₋-injective : ∀ {m n} → ℤ₋ m ≡ ℤ₋ n → m ≡ n
ℤ₋-injective refl = refl

data ℕ² : Set where
  _─_ : ℕ → ℕ → ℕ²

ℕ²-≡₊ : ∀ {a₊ a₋ b₊ b₋} → (a₊ ─ a₋) ≡ (b₊ ─ b₋) → a₊ ≡ b₊
ℕ²-≡₊ refl = refl

ℕ²-≡₋ : ∀ {a₊ a₋ b₊ b₋} → (a₊ ─ a₋) ≡ (b₊ ─ b₋) → a₋ ≡ b₋
ℕ²-≡₋ refl = refl

toℕ² : ℤ₃ → ℕ²
toℕ² (ℤ₊ n) = suc n ─ zero
toℕ² ℤ₀ = zero ─ zero
toℕ² (ℤ₋ n) = zero ─ suc n

toℤ₃ : ℕ² → ℤ₃
toℤ₃ (zero ─ zero) = ℤ₀
toℤ₃ (zero ─ suc n₋) = ℤ₋ n₋
toℤ₃ (suc n₊ ─ zero) = ℤ₊ n₊
toℤ₃ (suc n₊ ─ suc n₋) = toℤ₃ (n₊ ─ n₋)

data Dec (A : Set) : Set where
  yes : A → Dec A
  no : (A → ⊥) → Dec A

ℕ≡? : (m n : ℕ) → Dec (m ≡ n)
ℕ≡? zero zero = yes refl
ℕ≡? zero (suc n) = no (λ ())
ℕ≡? (suc m) zero = no (λ ())
ℕ≡? (suc m) (suc n) with ℕ≡? m n
... | yes m≡n = yes (cong suc m≡n)
... | no ¬m≡n = no λ sm≡sn → ¬m≡n (suc-injective sm≡sn)

ℤ₃≡? : (a b : ℤ₃) → Dec (a ≡ b)
ℤ₃≡? (ℤ₊ m) (ℤ₊ n) with ℕ≡? m n
... | yes m≡n = yes (cong ℤ₊ m≡n)
... | no ¬m≡n = no λ ℤ₊m≡ℤ₊n → ¬m≡n (ℤ₊-injective ℤ₊m≡ℤ₊n)
ℤ₃≡? (ℤ₊ _) ℤ₀ = no (λ ())
ℤ₃≡? (ℤ₊ _) (ℤ₋ _) = no (λ ())
ℤ₃≡? ℤ₀ (ℤ₊ _) = no (λ ())
ℤ₃≡? ℤ₀ ℤ₀ = yes refl
ℤ₃≡? ℤ₀ (ℤ₋ _) = no (λ ())
ℤ₃≡? (ℤ₋ _) (ℤ₊ _) = no (λ ())
ℤ₃≡? (ℤ₋ _) ℤ₀ = no (λ ())
ℤ₃≡? (ℤ₋ m) (ℤ₋ n) with ℕ≡? m n
... | yes m≡n = yes (cong ℤ₋ m≡n)
... | no ¬m≡n = no λ ℤ₋m≡ℤ₋n → ¬m≡n (ℤ₋-injective ℤ₋m≡ℤ₋n)

ℕ²≡? : (a b : ℕ²) → Dec (a ≡ b)
ℕ²≡? (a₊ ─ a₋) (b₊ ─ b₋) with ℕ≡? a₊ b₊
ℕ²≡? (a₊ ─ a₋) (b₊ ─ b₋) | yes refl with ℕ≡? a₋ b₋
ℕ²≡? (a₊ ─ a₋) (b₊ ─ b₋) | yes refl | yes refl =
  yes refl
ℕ²≡? (a₊ ─ a₋) (b₊ ─ b₋) | yes refl | no ¬a₋≡b₋ =
  no (λ a≡b → ¬a₋≡b₋ (ℕ²-≡₋ a≡b))
ℕ²≡? (a₊ ─ a₋) (b₊ ─ b₋) | no ¬a₊≡b₊ =
  no λ a≡b → ¬a₊≡b₊ (ℕ²-≡₊ a≡b)

_≃_ : ℕ² → ℕ² → Set
(a₊ ─ a₋) ≃ (b₊ ─ b₋) = a₊ + b₋ ≡ a₋ + b₊

≃? : (a b : ℕ²) → Dec (a ≃ b)
≃? (a₊ ─ a₋) (b₊ ─ b₋) = ℕ≡? (a₊ + b₋) (a₋ + b₊)

_+₂_ : ℕ² → ℕ² → ℕ²
(a₊ ─ a₋) +₂ (b₊ ─ b₋) = (a₊ + b₊) ─ (a₋ + b₋)

{-
≃-cong : {A : Set} {a b : ℕ²} (f : ℕ² → ℕ²) → a ≃ b → f a ≃ f b
≃-cong f a≃b = {!!}
-}

drop-neg : ℕ² → ℕ²
drop-neg (a₊ ─ _) = (a₊ ─ zero)

3-5≃2-4 : (3 ─ 5) ≃ (2 ─ 4)
3-5≃2-4 = refl

_+₃_ : ℤ₃ → ℤ₃ → ℤ₃
a +₃ b = toℤ₃ (toℕ² a +₂ toℕ² b)

ext: agda

max_stars_repo_name: iblech/agda-quotients

max_issues_repo_name: iblech/agda-quotients

max_forks_repo_name: iblech/agda-quotients


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

module Categories.Adjoint.Properties where

open import Level
open import Data.Product using (Σ; _,_; -,_; proj₂; uncurry)
open import Function using (_$_)

open import Categories.Adjoint using (_⊣_; Adjoint; Hom-NI′⇒Adjoint)
open import Categories.Adjoint.RAPL public
open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Product using (_⁂_; _⁂ⁿⁱ_)
open import Categories.Category.Construction.Comma using (CommaObj; Comma⇒; _↙_)
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Hom
open import Categories.Functor.Construction.Constant
open import Categories.Functor.Construction.LiftSetoids
open import Categories.Functor.Properties
open import Categories.Functor.Continuous
open import Categories.Functor.Cocontinuous
open import Categories.Functor.Bifunctor
open import Categories.Functor.Bifunctor.Properties
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_; _ⓘₕ_; _ⓘˡ_; module ≃)
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
open import Categories.Monad
open import Categories.Monad.Duality
open import Categories.Comonad
open import Categories.Morphism.Universal
open import Categories.Yoneda
import Categories.Yoneda.Properties as YP

import Categories.Diagram.Colimit as Col
import Categories.Diagram.Duality as Duality

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D E J : Category o ℓ e

-- if the left adjoint functor is a partial application of bifunctor, then it uniquely
-- determines a bifunctor compatible with the right adjoint functor.
module _ {C : Category o ℓ e}
         (L : Bifunctor C E D) {R : ∀ (X : Category.Obj E) → Functor D C}
         (LR : ∀ (X : Category.Obj E) → appʳ L X ⊣ R X) where
  private
    module C    = Category C
    module D    = Category D
    module E    = Category E
    module L    = Functor L
    module R X  = Functor (R X)
    module LR X = Adjoint (LR X)
    open C

    F′ : ∀ {A X B Y} f g → R.F₀ A X ⇒ R.F₀ B Y
    F′ {A} {X} {B} {Y} f g = LR.Ladjunct B (LR.counit.η A Y D.∘ L.F₁ (R.F₁ A g , f))
    --  R.F₁ B (LR.counit.η A Y) ∘ R.F₁ B (L.F₁ (R.F₁ A g , f)) ∘ LR.unit.η B (R.F₀ A X)

    commute′ : ∀ {A B X} (f : A E.⇒ B) → LR.counit.η A X D.∘ L.F₁ (F′ f D.id , E.id) D.≈ LR.counit.η B X D.∘ L.F₁ (C.id , f)
    commute′ {A} {B} {X} f = begin
      LR.counit.η A X D.∘ L.F₁ (F′ f D.id , E.id) ≈⟨ LR.RLadjunct≈id A ⟩
      LR.counit.η B X D.∘ L.F₁ (R.F₁ B D.id , f)  ≈⟨ refl ⟩∘⟨ L.F-resp-≈ (R.identity B , E.Equiv.refl) ⟩
      LR.counit.η B X D.∘ L.F₁ (C.id , f)         ∎
      where open D.HomReasoning

    open HomReasoning

    decompose₁ : ∀ {A B X Y} {f : A E.⇒ B} {g : X D.⇒ Y} → F′ f g ≈ R.F₁ A g ∘ F′ f D.id
    decompose₁ {A} {B} {X} {Y} {f} {g} = begin
      F′ f g
        ≈⟨ R.F-resp-≈ A (D.∘-resp-≈ʳ [ L ]-decompose₁) ⟩∘⟨refl ⟩
      R.F₁ A (LR.counit.η B Y D.∘ L.F₁ (R.F₁ B g , E.id) D.∘ L.F₁ (C.id , f)) ∘ LR.unit.η A (R.F₀ B X)
        ≈⟨ R.F-resp-≈ A (pullˡ (LR.counit.commute B g)) ⟩∘⟨refl ⟩
      R.F₁ A ((g D.∘ LR.counit.η B X) D.∘ L.F₁ (C.id , f)) ∘ LR.unit.η A (R.F₀ B X)
        ≈˘⟨ R.F-resp-≈ A (pushʳ (D.∘-resp-≈ʳ (L.F-resp-≈ (R.identity B , E.Equiv.refl)))) ⟩∘⟨refl ⟩
      R.F₁ A (g D.∘ LR.counit.η B X D.∘ L.F₁ (R.F₁ B D.id , f)) ∘ LR.unit.η A (R.F₀ B X)
        ≈⟨ R.homomorphism A ⟩∘⟨refl ⟩
      (R.F₁ A g ∘ R.F₁ A (LR.counit.η B X D.∘ L.F₁ (R.F₁ B D.id , f))) ∘ LR.unit.η A (R.F₀ B X)
        ≈⟨ assoc ⟩
      R.F₁ A g ∘ F′ f D.id
        ∎
      where open MR D

    decompose₂ : ∀ {A B X Y} {f : A E.⇒ B} {g : X D.⇒ Y} → F′ f g ≈ F′ f D.id ∘ R.F₁ B g
    decompose₂ {A} {B} {X} {Y} {f} {g} = begin
      F′ f g
        ≈⟨ R.F-resp-≈ A (D.∘-resp-≈ʳ [ L ]-decompose₂) ⟩∘⟨refl ⟩
      R.F₁ A (LR.counit.η B Y D.∘ L.F₁ (C.id , f) D.∘ L.F₁ (R.F₁ B g , E.id)) ∘ LR.unit.η A (R.F₀ B X)
        ≈˘⟨ R.F-resp-≈ A (pushˡ (D.∘-resp-≈ʳ (L.F-resp-≈ (R.identity B , E.Equiv.refl)))) ⟩∘⟨refl ⟩
      R.F₁ A ((LR.counit.η B Y D.∘ L.F₁ (R.F₁ B D.id , f)) D.∘ L.F₁ (R.F₁ B g , E.id)) ∘ LR.unit.η A (R.F₀ B X)
        ≈⟨ R.homomorphism A ⟩∘⟨refl ⟩
      (R.F₁ A (LR.counit.η B Y D.∘ L.F₁ (R.F₁ B D.id , f)) ∘ R.F₁ A (L.F₁ (R.F₁ B g , E.id))) ∘ LR.unit.η A (R.F₀ B X)
        ≈˘⟨ MR.pushʳ C (LR.unit.commute A (R.F₁ B g)) ⟩
      R.F₁ A (LR.counit.η B Y D.∘ L.F₁ (R.F₁ B D.id , f)) ∘ LR.unit.η A (R.F₀ B Y) ∘ R.F₁ B g
        ≈˘⟨ assoc ⟩
      F′ f D.id ∘ R.F₁ B g
        ∎
      where open MR D

    swap : ∀ {A B X Y} {f : A E.⇒ B} {g : X D.⇒ Y} → R.F₁ A g ∘ F′ f D.id ≈ F′ f D.id ∘ R.F₁ B g
    swap = trans (⟺ decompose₁) decompose₂

    commute″ : ∀ {X Y Z A} {f : Y E.⇒ Z} {g : X E.⇒ Y} → F′ (f E.∘ g) (D.id {A}) ≈ F′ g D.id ∘ F′ f D.id
    commute″ {X} {Y} {Z} {A} {f} {g} = begin
      F′ (f E.∘ g) D.id
        ≈⟨ R.F-resp-≈ X (D.∘-resp-≈ʳ (L.F-resp-≈ (R.identity Z , E.Equiv.refl))) ⟩∘⟨refl ⟩
      R.F₁ X (LR.counit.η Z A D.∘ L.F₁ (C.id , f E.∘ g)) ∘ LR.unit.η X (R.F₀ Z A)
        ≈⟨ R.F-resp-≈ X (D.∘-resp-≈ʳ (Functor.homomorphism (appˡ L (R.F₀ Z A)))) ⟩∘⟨refl ⟩
      R.F₁ X (LR.counit.η Z A D.∘ L.F₁ (C.id , f) D.∘ L.F₁ (C.id , g)) ∘ LR.unit.η X (R.F₀ Z A)
        ≈˘⟨ R.F-resp-≈ X (MR.pushˡ D (commute′ f)) ⟩∘⟨refl ⟩
      R.F₁ X ((LR.counit.η Y A D.∘ L.F₁ (F′ f D.id , E.id)) D.∘ L.F₁ (C.id , g)) ∘ LR.unit.η X (R.F₀ Z A)
        ≈˘⟨ R.F-resp-≈ X (MR.pushʳ D [ L ]-commute) ⟩∘⟨refl ⟩
      R.F₁ X (LR.counit.η Y A D.∘ L.F₁ (C.id , g) D.∘ L.F₁ (F′ f D.id , E.id)) ∘ LR.unit.η X (R.F₀ Z A)
        ≈˘⟨ R.F-resp-≈ X D.assoc ⟩∘⟨refl ⟩
      R.F₁ X ((LR.counit.η Y A D.∘ L.F₁ (C.id , g)) D.∘ L.F₁ (F′ f D.id , E.id)) ∘ LR.unit.η X (R.F₀ Z A)
        ≈⟨ R.homomorphism X ⟩∘⟨refl ⟩
      (R.F₁ X (LR.counit.η Y A D.∘ L.F₁ (C.id , g)) ∘ R.F₁ X (L.F₁ (F′ f D.id , E.id))) ∘ LR.unit.η X (R.F₀ Z A)
        ≈˘⟨ MR.pushʳ C (LR.unit.commute X (F′ f D.id)) ⟩
      R.F₁ X (LR.counit.η Y A D.∘ L.F₁ (C.id , g)) ∘ LR.unit.η X (R.F₀ Y A) ∘ F′ f D.id
        ≈˘⟨ R.F-resp-≈ X (D.∘-resp-≈ʳ (L.F-resp-≈ (R.identity Y , E.Equiv.refl))) ⟩∘⟨ refl ⟩∘⟨ refl ⟩
      R.F₁ X (LR.counit.η Y A D.∘ L.F₁ (R.F₁ Y D.id , g)) ∘ LR.unit.η X (R.F₀ Y A) ∘ F′ f D.id
        ≈˘⟨ assoc ⟩
      F′ g D.id ∘ F′ f D.id
        ∎

  induced-bifunctorʳ : Bifunctor E.op D C
  induced-bifunctorʳ = record
    { F₀           = uncurry R.F₀
    ; F₁           = uncurry F′
    ; identity     = λ where
      {e , d} →
        let open MR D
        in begin
          F′ E.id D.id
            ≈⟨ R.F-resp-≈ e (D.∘-resp-≈ʳ (L.F-resp-≈ (R.identity e , E.Equiv.refl))) ⟩∘⟨ refl ⟩
          R.F₁ e (LR.counit.η e d D.∘ L.F₁ (C.id , E.id)) ∘ LR.unit.η e (R.F₀ e d)
            ≈⟨ R.F-resp-≈ e (elimʳ L.identity) ⟩∘⟨ refl ⟩
          R.F₁ e (LR.counit.η e d) ∘ LR.unit.η e (R.F₀ e d)
            ≈⟨ LR.zag e ⟩
          C.id
            ∎
    ; homomorphism = λ where
      {A , X} {B , Y} {W , Z} {f , h} {g , i} →
        let open MR C
        in begin
          F′ (f E.∘ g) (i D.∘ h)
            ≈⟨ decompose₁ ⟩
          R.F₁ W (i D.∘ h) ∘ F′ (f E.∘ g) D.id
            ≈˘⟨ center⁻¹ (⟺ (R.homomorphism W)) (⟺ commute″) ⟩
          R.F₁ W i ∘ (R.F₁ W h ∘ F′ g D.id) ∘ F′ f D.id
            ≈˘⟨ center (⟺ swap) ⟩
          (R.F₁ W i ∘ F′ g D.id) ∘ R.F₁ B h ∘ F′ f D.id
            ≈˘⟨ decompose₁ ⟩∘⟨ decompose₁ ⟩
          F′ g i ∘ F′ f h
            ∎
    ; F-resp-≈     = λ where
      {A , X} {B , Y} (eq , eq′) →
        ∘-resp-≈ˡ (R.F-resp-≈ B (D.∘-resp-≈ʳ (L.F-resp-≈ (R.F-resp-≈ A eq′ , eq))))
    }

-- LAPC: left adjoint preserves colimits.
module _ {L : Functor C D} {R : Functor D C} (L⊣R : L ⊣ R) (F : Functor J C) where
  private
    module F = Functor F
    open Col

  lapc : Colimit F → Colimit (L ∘F F)
  lapc col = Duality.coLimit⇒Colimit D (rapl (Adjoint.op L⊣R) F.op (Duality.Colimit⇒coLimit C col))

-- adjoint functors induce monads and comonads
module _ {L : Functor C D} {R : Functor D C} (L⊣R : L ⊣ R) where
  private
    module C = Category C
    module D = Category D
    module L = Functor L
    module R = Functor R
    open Adjoint L⊣R

  rapl′ : ∀ {o ℓ e} → Continuous o ℓ e R
  rapl′ lim = rapl L⊣R _ lim , Mor.≅.refl C

  lapc′ : ∀ {o ℓ e} → Cocontinuous o ℓ e L
  lapc′ col = lapc L⊣R _ col , Mor.≅.refl D

  adjoint⇒monad : Monad C
  adjoint⇒monad = record
    { F         = R ∘F L
    ; η         = unit
    ; μ         = record
      { η           = μ′.η
      ; commute     = μ′.commute
      ; sym-commute = μ′.sym-commute
      }
    ; assoc     = [ R ]-resp-square (counit.commute _)
    ; sym-assoc = [ R ]-resp-square (counit.sym-commute _)
    ; identityˡ = λ {X} → begin
      μ′.η X ∘ R.F₁ (L.F₁ (unit.η X)) ≈⟨ [ R ]-resp-∘ zig ⟩
      R.F₁ D.id                       ≈⟨ R.identity ⟩
      C.id                            ∎
    ; identityʳ = zag
    }
    where open C
          open HomReasoning
          μ′ : NaturalTransformation (R ∘F (L ∘F R) ∘F L) (R ∘F Categories.Functor.id ∘F L)
          μ′ = R ∘ˡ counit ∘ʳ L
          module μ′ = NaturalTransformation μ′

module _ {L : Functor C D} {R : Functor D C} (L⊣R : L ⊣ R) where
  open Adjoint L⊣R

  adjoint⇒comonad : Comonad D
  adjoint⇒comonad = coMonad⇒Comonad D (adjoint⇒monad op)

-- adjoint functors are the same as universal morphisms
module _ {R : Functor D C} where
  private
    module C = Category C
    module D = Category D
    module R = Functor R

  adjoint⇒universalMorphisms : ∀ {L : Functor C D} → L ⊣ R → ∀ (X : C.Obj) → UniversalMorphism X R
  adjoint⇒universalMorphisms {L} L⊣R X = record
    { initial = record
      { ⊥        = record { f = unit.η X }
      ; !        =
        let open C.HomReasoning
        in record { commute = LRadjunct≈id ○ ⟺ C.identityʳ }
      ; !-unique = λ {A} g →
        let open D.HomReasoning
        in -, (begin
          Radjunct (f A)            ≈⟨ Radjunct-resp-≈ (C.Equiv.sym (C.Equiv.trans (commute g) (C.identityʳ {f = f A}))) ⟩
          Radjunct (Ladjunct (h g)) ≈⟨ RLadjunct≈id ⟩
          h g                       ∎)
      }
    }
    where module L = Functor L
          open Adjoint L⊣R
          open Comma⇒
          open CommaObj

  universalMophisms⇒adjoint : (∀ (X : C.Obj) → UniversalMorphism X R) → Σ (Functor C D) (λ L → L ⊣ R)
  universalMophisms⇒adjoint umors = L , record
    { unit   = ntHelper record
      { η       = λ c → f (umors.⊥ c)
      ; commute = λ i → let open C.HomReasoning in ⟺ (commute (⊥X⇒⊥Y i) ○ C.identityʳ )
      }
    ; counit = ntHelper record
      { η       = ε
      ; commute = λ {X Y} i →
        let open C.HomReasoning
            open MR C
        in proj₂ $ umors.!-unique₂ (R.F₀ X)
           {record { f = R.F₁ i }}
           (record
           { h       = ε Y D.∘ L₁ (R.F₁ i)
           ; commute = begin
             R.F₁ (ε Y D.∘ L₁ (R.F₁ i)) C.∘ f (⊥Rd X)          ≈⟨ R.homomorphism ⟩∘⟨refl ⟩
             (R.F₁ (ε Y) C.∘ R.F₁ (L₁ (R.F₁ i))) C.∘ f (⊥Rd X) ≈⟨ pullʳ (commute (⊥X⇒⊥Y (R.F₁ i)) ○ C.identityʳ) ⟩
             R.F₁ (ε Y) C.∘ f (⊥Rd Y) C.∘ R.F₁ i               ≈⟨ cancelˡ (commute (⊥Rd⇒id Y) ○ C.identityˡ) ⟩
             R.F₁ i                                            ≈˘⟨ C.identityʳ ⟩
             R.F₁ i C.∘ C.id                                   ∎
           })
           (record
           { h       = i D.∘ ε X
           ; commute = begin
             R.F₁ (i D.∘ ε X) C.∘ f (⊥Rd X)        ≈⟨ R.homomorphism ⟩∘⟨refl ⟩
             (R.F₁ i C.∘ R.F₁ (ε X)) C.∘ f (⊥Rd X) ≈⟨ cancelʳ (commute (⊥Rd⇒id X) ○ C.identityˡ) ⟩
             R.F₁ i                                ≈˘⟨ C.identityʳ ⟩
             R.F₁ i C.∘ C.id                       ∎
           })
      }
    ; zig    = λ {c} →
      let open C.HomReasoning
          open MR C
          α = f (umors.⊥ c)
      in proj₂ $ umors.!-unique₂ c
         {record { f = α }}
         (record
         { h       = ε (L₀ c) D.∘ L₁ α
         ; commute = begin
           R.F₁ (ε (L₀ c) D.∘ L₁ α) C.∘ α           ≈⟨ R.homomorphism ⟩∘⟨refl ⟩
           (R.F₁ (ε (L₀ c)) C.∘ R.F₁ (L₁ α)) C.∘ α  ≈⟨ pullʳ (commute (⊥X⇒⊥Y α) ○ C.identityʳ) ⟩
           R.F₁ (ε (L₀ c)) C.∘ f (⊥Rd (L₀ c)) C.∘ α ≈⟨ cancelˡ (commute (⊥Rd⇒id (L₀ c)) ○ C.identityˡ) ⟩
           α                                        ≈˘⟨ C.identityʳ ⟩
           α C.∘ C.id                               ∎
         })
         (record
         { h       = D.id
         ; commute = C.∘-resp-≈ˡ R.identity ○ id-comm-sym
         })
    ; zag    = λ {d} → C.Equiv.trans (commute (⊥Rd⇒id d)) C.identityˡ
    }
    where module umors X = UniversalMorphism (umors X)
          open CommaObj
          open Comma⇒

          commaObj∘g : ∀ {X Y} → X C.⇒ Y → CommaObj (const! X) R
          commaObj∘g {X} {Y} g = record { f = f (umors.⊥ Y) C.∘ g }

          ⊥X⇒⊥Y : ∀ {X Y} (g : X C.⇒ Y) → (X ↙ R) [ umors.⊥ X , commaObj∘g g ]
          ⊥X⇒⊥Y {X} {Y} g = umors.! X {commaObj∘g g}

          L₀ : ∀ X → D.Obj
          L₀ X         = β (umors.⊥ X)
          L₁ : ∀ {X Y} → X C.⇒ Y → β (umors.⊥ X) D.⇒ β (umors.⊥ Y)
          L₁ {X} {Y} g = h (⊥X⇒⊥Y g)
          L : Functor C D
          L            = record
            { F₀           = L₀
            ; F₁           = L₁
            ; identity     = λ {X} → proj₂ $ umors.!-unique X $
              record { commute = elimˡ R.identity ○ ⟺ C.identityʳ ○ ⟺ C.identityʳ }
            ; homomorphism = λ {X Y Z} {i j} → proj₂ $ umors.!-unique₂ X (umors.! X) $
              record { commute = begin
                R.F₁ (h (umors.! Y) D.∘ h (umors.! X)) C.∘ f (umors.⊥ X)
                  ≈⟨ (C.∘-resp-≈ˡ R.homomorphism) ○ C.assoc ⟩
                R.F₁ (h (umors.! Y)) C.∘ R.F₁ (h (umors.! X)) C.∘ f (umors.⊥ X)
                  ≈⟨ (C.∘-resp-≈ʳ (commute (⊥X⇒⊥Y i) ○ C.identityʳ)) ○ C.sym-assoc ⟩
                (R.F₁ (h (umors.! Y)) C.∘ f (umors.⊥ Y)) C.∘ i
                  ≈⟨ pushˡ (commute (⊥X⇒⊥Y j) ○ C.identityʳ) ⟩
                f (umors.⊥ Z) C.∘ j C.∘ i
                  ≈˘⟨ C.identityʳ ⟩
                (f (umors.⊥ Z) C.∘ j C.∘ i) C.∘ C.id
                  ∎ }
            ; F-resp-≈     = λ {X} eq → proj₂ $ umors.!-unique₂ X (umors.! X) $
              record { commute = commute (umors.! X) ○ C.∘-resp-≈ˡ (C.∘-resp-≈ʳ (⟺ eq)) }
            }
            where open C.HomReasoning
                  open MR C
          module L = Functor L

          ⊥Rd    : (d : D.Obj) → CommaObj (const! (R.F₀ d)) R
          ⊥Rd d    = umors.⊥ (R.F₀ d)
          ⊥Rd⇒id : (d : D.Obj) →  (R.F₀ d ↙ R) [ ⊥Rd d , record { f = C.id } ]
          ⊥Rd⇒id d = umors.! (R.F₀ d) {record { f = C.id }}
          ε      : ∀ d → L₀ (R.F₀ d) D.⇒ d
          ε d      = h (⊥Rd⇒id d)

-- adjoint functors of a functor are isomorphic
module _ (L : Functor C D) where
  open YP C

  R≃R′ : ∀ {R R′} → L ⊣ R → L ⊣ R′ → R ≃ R′
  R≃R′ {R} {R′} L⊣R L⊣R′ = yoneda-NI R R′ (unlift-≃ Hom[-,R-]≃Hom[-,R′-])
    where module ⊣₁ = Adjoint L⊣R
          module ⊣₂ = Adjoint L⊣R′
          Hom[-,R-]≃Hom[-,R′-] : ⊣₁.Hom[-,R-]′ ≃ ⊣₂.Hom[-,R-]′
          Hom[-,R-]≃Hom[-,R′-] = ≃.trans (≃.sym ⊣₁.Hom-NI) ⊣₂.Hom-NI

module _ {R : Functor D C} where

  L≃L′ : ∀ {L L′} → L ⊣ R → L′ ⊣ R → L ≃ L′
  L≃L′ L⊣R L′⊣R = NaturalIsomorphism.op L′≃Lᵒᵖ
    where module ⊣₁ = Adjoint L⊣R
          module ⊣₂ = Adjoint L′⊣R
          L′≃Lᵒᵖ = R≃R′ (Functor.op R) ⊣₂.op ⊣₁.op

-- adjoint functors are preserved by natural isomorphisms
module _ {L L′ : Functor C D} {R R′ : Functor D C} where
  private
    module C  = Category C
    module D  = Category D
    module L  = Functor L
    module L′ = Functor L′
    module R  = Functor R
    module R′ = Functor R′

  ⊣×≃⇒⊣ : L ⊣ R → L ≃ L′ → R ≃ R′ → L′ ⊣ R′
  ⊣×≃⇒⊣ L⊣R L≃L′ R≃R′ = Hom-NI′⇒Adjoint (≃.trans (LiftSetoids _ _  ⓘˡ Hom[L′-,-]≃Hom[L-,-])
                                        (≃.trans Hom-NI
                                                 (LiftSetoids _ _  ⓘˡ Hom[-,R-]≃Hom[-,R′-])))
    where open Adjoint L⊣R
          Hom[L′-,-]≃Hom[L-,-] : Hom[ D ][-,-] ∘F (L′.op ⁂ idF) ≃ Hom[ D ][-,-] ∘F (L.op ⁂ idF)
          Hom[L′-,-]≃Hom[L-,-] = Hom[ D ][-,-] ⓘˡ (NaturalIsomorphism.op L≃L′ ⁂ⁿⁱ ≃.refl)
          Hom[-,R-]≃Hom[-,R′-] : Hom[ C ][-,-] ∘F (idF ⁂ R) ≃ Hom[ C ][-,-] ∘F (idF ⁂ R′)
          Hom[-,R-]≃Hom[-,R′-] = Hom[ C ][-,-] ⓘˡ (≃.refl ⁂ⁿⁱ R≃R′)

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
------------------------------------------------------------------------
-- An example
------------------------------------------------------------------------

module RecursiveDescent.Hybrid.Mixfix.Example where

open import Data.Vec using ([]; _∷_; [_])
open import Data.List renaming ([_] to L[_])
open import Data.Product using (∃₂; ,_)
open import Data.Nat using (zero; suc)
open import Data.Fin using (#_)
open import Data.String
open import Data.Function using (_∘_)
open import Relation.Binary.PropositionalEquality

open import RecursiveDescent.Hybrid.Mixfix.Expr
open import RecursiveDescent.Hybrid.Mixfix.Fixity
import RecursiveDescent.Hybrid.Mixfix as Mixfix

------------------------------------------------------------------------
-- Operators

atom : Operator closed 0
atom = operator ("•" ∷ [])

• : Expr
• = ⟪ atom ∙ [] ⟫

parens : Operator closed 1
parens = operator ("(" ∷ ")" ∷ [])

⟦_⟧ : Expr -> Expr
⟦ e ⟧ = ⟪ parens ∙ [ e ] ⟫

plus : Operator (infx left) 0
plus = operator ("+" ∷ [])

_+_ : Expr -> Expr -> Expr
e₁ + e₂ = e₁ ⟨ plus ∙ [] ⟩ e₂

minus : Operator (infx left) 0
minus = operator ("-" ∷ [])

_-_ : Expr -> Expr -> Expr
e₁ - e₂ = e₁ ⟨ minus ∙ [] ⟩ e₂

times : Operator (infx left) 0
times = operator ("*" ∷ [])

_*_ : Expr -> Expr -> Expr
e₁ * e₂ = e₁ ⟨ times ∙ [] ⟩ e₂

comma : Operator (infx left) 0
comma = operator ("," ∷ [])

_,_ : Expr -> Expr -> Expr
e₁ , e₂ = e₁ ⟨ comma ∙ [] ⟩ e₂

wellTyped : Operator postfx 1
wellTyped = operator ("⊢" ∷ "∶" ∷ [])

_⊢_∶ : Expr -> Expr -> Expr
e₁ ⊢ e₂ ∶ = e₁ ⟨ wellTyped ∙ [ e₂ ] ⟫

------------------------------------------------------------------------
-- Precedence graph

prec : List (∃₂ Operator) -> PrecedenceGraph -> PrecedenceTree
prec ops = precedence (\fix -> gfilter (hasFixity fix) ops)

g : PrecedenceGraph
g = wt ∷ c ∷ pm ∷ t ∷ ap ∷ []
  where
  ap = prec ((, , atom) ∷ (, , parens) ∷ []) []
  t  = prec ((, , times) ∷ [])               (ap ∷ [])
  pm = prec ((, , plus) ∷ (, , minus) ∷ [])  (t ∷ ap ∷ [])
  c  = prec ((, , comma) ∷ [])               (pm ∷ t ∷ ap ∷ [])
  wt = prec ((, , wellTyped) ∷ [])           (c ∷ ap ∷ [])

------------------------------------------------------------------------
-- Some tests

test : String -> List Expr
test s = Mixfix.parseExpr g (map (fromList ∘ L[_]) (toList s))

-- Using an unoptimised type checker to run an inefficient parser can
-- take ages… The following examples have been converted into
-- postulates since I have not had the patience to wait long enough to
-- see whether the left- and right-hand sides actually match.

postulate
  ex₁ : test "•⊢•" ≡ []
  ex₂ : test "(•,•)⊢∶" ≡ []
  ex₃ : test "•⊢•∶" ≡ L[ • ⊢ • ∶ ]
  ex₄ : test "•,•+•*•⊢(•⊢•∶)∶" ≡
        L[ (• , (• + (• * •))) ⊢ ⟦ • ⊢ • ∶ ⟧ ∶ ]

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- Minimal propositional logic, PHOAS approach, initial encoding

module Pi.Mp where

-- Types

infixl 2 _&&_
infixl 1 _||_
infixr 0 _=>_
data Ty : Set where
  UNIT  :             Ty
  _=>_  : Ty -> Ty -> Ty
  _&&_  : Ty -> Ty -> Ty
  _||_  : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 _<=>_
_<=>_ : Ty -> Ty -> Ty
a <=> b = (a => b) && (b => a)

NOT : Ty -> Ty
NOT a = a => FALSE

TRUE : Ty
TRUE = FALSE => FALSE

-- Context and truth judgement

Cx : Set1
Cx = Ty -> Set

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

-- Terms

module Mp where
  infixl 1 _$_
  data Tm (tc : Cx) : Ty -> Set where
    var   : forall {a}     -> isTrue a tc               -> Tm tc a
    lam'  : forall {a b}   -> (isTrue a tc -> Tm tc b)  -> Tm tc (a => b)
    _$_   : forall {a b}   -> Tm tc (a => b) -> Tm tc a -> Tm tc b
    pair' : forall {a b}   -> Tm tc a        -> Tm tc b -> Tm tc (a && b)
    fst   : forall {a b}   -> Tm tc (a && b)            -> Tm tc a
    snd   : forall {a b}   -> Tm tc (a && b)            -> Tm tc b
    left  : forall {a b}   -> Tm tc a                   -> Tm tc (a || b)
    right : forall {a b}   -> Tm tc b                   -> Tm tc (a || b)
    case' : forall {a b c} -> Tm tc (a || b) -> (isTrue a tc -> Tm tc c) -> (isTrue b tc -> Tm tc c) -> Tm tc c

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

  case'' : forall {tc a b c} -> Tm tc (a || b) -> (Tm tc a -> Tm tc c) -> (Tm tc b -> Tm tc c) -> Tm tc c
  case'' xy f g = case' xy (\x -> f (var x)) (\y -> g (var y))

  syntax lam''  (\a -> b) = lam a => b
  syntax pair'  x y       = [ x , y ]
  syntax case'' xy (\x -> z1) (\y -> z2) = case xy of x => z1 or y => z2

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

-- Example theorems

c1 : forall {a b} -> Thm (a && b <=> b && a)
c1 =
  [ lam xy => [ snd xy , fst xy ]
  , lam yx => [ snd yx , fst yx ]
  ]

c2 : forall {a b} -> Thm (a || b <=> b || a)
c2 =
  [ lam xy =>
      case xy
        of x => right x
        or y => left y
  , lam yx =>
      case yx
        of y => right y
        or x => left x
  ]

i1 : forall {a} -> Thm (a && a <=> a)
i1 =
  [ lam xx => fst xx
  , lam x  => [ x , x ]
  ]

i2 : forall {a} -> Thm (a || a <=> a)
i2 =
  [ lam xx =>
      case xx
        of x => x
        or x => x
  , lam x => left x
  ]

l3 : forall {a} -> Thm ((a => a) <=> TRUE)
l3 =
  [ lam _ => lam nt => nt
  , lam _ => lam x => x
  ]

l1 : forall {a b c} -> Thm (a && (b && c) <=> (a && b) && c)
l1 =
  [ lam xyz =>
      (let yz = snd xyz in
        [ [ fst xyz , fst yz ] , snd yz ])
  , lam xyz =>
      (let xy = fst xyz in
        [ fst xy , [ snd xy , snd xyz ] ])
  ]

l2 : forall {a} -> Thm (a && TRUE <=> a)
l2 =
  [ lam xt => fst xt
  , lam x  => [ x , lam nt => nt ]
  ]

l4 : forall {a b c} -> Thm (a && (b || c) <=> (a && b) || (a && c))
l4 =
  [ lam xyz =>
      (let x = fst xyz in
        case snd xyz
          of y => left  [ x , y ]
          or z => right [ x , z ])
  , lam xyxz =>
      case xyxz
        of xy => [ fst xy , left  (snd xy) ]
        or xz => [ fst xz , right (snd xz) ]
  ]

l6 : forall {a b c} -> Thm (a || (b && c) <=> (a || b) && (a || c))
l6 =
  [ lam xyz =>
      case xyz
        of x  => [ left x , left x ]
        or yz => [ right (fst yz) , right (snd yz) ]
  , lam xyxz =>
      case fst xyxz
        of x => left x
        or y =>
          case snd xyxz
            of x => left x
            or z => right [ y , z ]
  ]

l7 : forall {a} -> Thm (a || TRUE <=> TRUE)
l7 =
  [ lam _ => lam nt => nt
  , lam t => right t
  ]

l9 : forall {a b c} -> Thm (a || (b || c) <=> (a || b) || c)
l9 =
  [ lam xyz =>
      case xyz
        of x  => left (left x)
        or yz =>
          case yz
            of y => left (right y)
            or z => right z
  , lam xyz =>
      case xyz
        of xy =>
          case xy
            of x => left x
            or y => right (left y)
        or z => right (right z)
  ]

l11 : forall {a b c} -> Thm ((a => (b && c)) <=> (a => b) && (a => c))
l11 =
  [ lam xyz =>
      [ lam x => fst (xyz $ x)
      , lam x => snd (xyz $ x)
      ]
  , lam xyxz =>
      lam x => [ fst xyxz $ x , snd xyxz $ x ]
  ]

l12 : forall {a} -> Thm ((a => TRUE) <=> TRUE)
l12 =
  [ lam _ => lam nt => nt
  , lam t => lam _  => t
  ]

l13 : forall {a b c} -> Thm ((a => (b => c)) <=> ((a && b) => c))
l13 =
  [ lam xyz =>
      lam xy => xyz $ fst xy $ snd xy
  , lam xyz =>
      lam x =>
        lam y => xyz $ [ x , y ]
  ]

l16 : forall {a b c} -> Thm (((a && b) => c) <=> (a => (b => c)))
l16 =
  [ lam xyz =>
      lam x =>
        lam y => xyz $ [ x , y ]
  , lam xyz =>
      lam xy => xyz $ fst xy $ snd xy
  ]

l17 : forall {a} -> Thm ((TRUE => a) <=> a)
l17 =
  [ lam tx => tx $ (lam nt => nt)
  , lam x  => lam _ => x
  ]

l19 : forall {a b c} -> Thm (((a || b) => c) <=> (a => c) && (b => c))
l19 =
  [ lam xyz =>
      [ lam x => xyz $ left x
      , lam y => xyz $ right y
      ]
  , lam xzyz =>
      lam xy =>
        case xy
          of x => fst xzyz $ x
          or y => snd xzyz $ y
  ]

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module Data.Num.Maximum where

open import Data.Num.Core

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra

open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤)
    renaming (zero to z; suc to s)

open import Data.Fin.Properties using (toℕ-fromℕ≤; bounded)
open import Data.Product

open import Function
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

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

Maximum : ∀ {b d o} → (xs : Numeral b d o) → Set
Maximum {b} {d} {o} xs = (ys : Numeral b d o) → ⟦ xs ⟧ ≥ ⟦ ys ⟧

-- Maximum-unique : ∀ {b d o}
--     → (max xs : Numeral b d o)
--     → Maximum max
--     → Maximum xs
--     → ⟦ max ⟧ ≡ ⟦ xs ⟧
-- Maximum-unique max xs max-max xs-max = IsPartialOrder.antisym isPartialOrder
--     (xs-max max)
--     (max-max xs)

Maximum-NullBase-Greatest : ∀ {d} {o}
    → (xs : Numeral 0 (suc d) o)
    → Greatest (lsd xs)
    → Maximum xs
Maximum-NullBase-Greatest {_} {o} (x ∙) greatest (y ∙) =
    greatest-of-all o x y greatest
Maximum-NullBase-Greatest {_} {o} (x ∙) greatest (y ∷ ys) =
    start
        Fin.toℕ y + o + ⟦ ys ⟧ * 0
    ≈⟨ toℕ-NullBase y ys ⟩
        Fin.toℕ y + o
    ≤⟨ greatest-of-all o x y greatest ⟩
        Fin.toℕ x + o
    □
Maximum-NullBase-Greatest {_} {o} (x ∷ xs) greatest (y ∙) =
    start
        Fin.toℕ y + o
    ≤⟨ greatest-of-all o x y greatest ⟩
        Fin.toℕ x + o
    ≈⟨ sym (toℕ-NullBase x xs) ⟩
        Fin.toℕ x + o + ⟦ xs ⟧ * 0
    □
Maximum-NullBase-Greatest {_} {o} (x ∷ xs) greatest (y ∷ ys) =
    start
        ⟦ y ∷ ys ⟧
    ≈⟨ toℕ-NullBase y ys ⟩
        Fin.toℕ y + o
    ≤⟨ greatest-of-all o x y greatest ⟩
        Fin.toℕ x + o
    ≈⟨ sym (toℕ-NullBase x xs) ⟩
        ⟦ x ∷ xs ⟧
    □

Maximum⇒Greatest-LSD : ∀ {b} {d} {o}
    → (xs : Numeral b d o)
    → Maximum xs
    → Greatest (lsd xs)
Maximum⇒Greatest-LSD xs max with Greatest? (lsd xs)
Maximum⇒Greatest-LSD xs max | yes greatest = greatest
Maximum⇒Greatest-LSD {b} {zero}      xs       max | no ¬greatest = NoDigits-explode xs
Maximum⇒Greatest-LSD {b} {suc d} {o} (x ∙)    max | no ¬greatest
    = contradiction p ¬p
    where
        ys : Numeral b (suc d) o
        ys = greatest-digit d ∙

        p : Digit-toℕ x o ≥ ⟦ ys ⟧
        p = max ys

        ¬p : Digit-toℕ x o ≱ ⟦ ys ⟧
        ¬p = <⇒≱ $
            start
                suc (Digit-toℕ x o)
            ≤⟨ +n-mono o (≤-pred (≤∧≢⇒< (bounded x) ¬greatest)) ⟩
                d + o
            ≈⟨ sym (greatest-digit-toℕ (Fin.fromℕ d) (greatest-digit-is-the-Greatest d)) ⟩
                Digit-toℕ (greatest-digit d) o
            ≈⟨ refl ⟩
                ⟦ ys ⟧
            □
Maximum⇒Greatest-LSD {b} {suc d} {o} (x ∷ xs) max | no ¬greatest
    = contradiction p ¬p
    where
        ys : Numeral b (suc d) o
        ys = greatest-digit d ∷ xs

        p : ⟦ x ∷ xs ⟧ ≥ ⟦ ys ⟧
        p = max ys

        ¬p : ⟦ x ∷ xs ⟧ ≱ ⟦ ys ⟧
        ¬p = <⇒≱ $ +n-mono (⟦ xs ⟧ * b) $
            start
                suc (Digit-toℕ x o)
            ≤⟨ +n-mono o (≤-pred (≤∧≢⇒< (bounded x) ¬greatest)) ⟩
                d + o
            ≈⟨ sym (greatest-digit-toℕ (Fin.fromℕ d) (greatest-digit-is-the-Greatest d)) ⟩
                (Digit-toℕ (greatest-digit d) o)
            □

Maximum-NullBase : ∀ {d} {o}
    → (xs : Numeral 0 (suc d) o)
    → Dec (Maximum xs)
Maximum-NullBase xs with Greatest? (lsd xs)
Maximum-NullBase xs | yes greatest = yes (Maximum-NullBase-Greatest xs greatest)
Maximum-NullBase xs | no ¬greatest = no (contraposition (Maximum⇒Greatest-LSD xs) ¬greatest)

Maximum-AllZeros : ∀ {b} → (xs : Numeral b 1 0) → Maximum xs
Maximum-AllZeros xs ys = reflexive $
    begin
        ⟦ ys ⟧
    ≡⟨ toℕ-AllZeros ys ⟩
        zero
    ≡⟨ sym (toℕ-AllZeros xs) ⟩
        ⟦ xs ⟧
    ∎

Maximum-Proper : ∀ {b d o}
    → (xs : Numeral (suc b) (suc d) o)
    → (proper : 2 ≤ suc (d + o))
    → ¬ (Maximum xs)
Maximum-Proper {b} {d} {o} xs proper claim = contradiction p ¬p
    where
        p : ⟦ xs ⟧ ≥ ⟦ greatest-digit d ∷ xs ⟧
        p = claim (greatest-digit d ∷ xs)
        ¬p : ⟦ xs ⟧ ≱ ⟦ greatest-digit d ∷ xs ⟧
        ¬p = <⇒≱ $
            start
                suc ⟦ xs ⟧
            ≈⟨ cong suc (sym (*-right-identity ⟦ xs ⟧)) ⟩
                suc (⟦ xs ⟧ * 1)
            ≤⟨ s≤s (n*-mono ⟦ xs ⟧ (s≤s z≤n)) ⟩
                suc (⟦ xs ⟧ * suc b)
            ≤⟨ +n-mono (⟦ xs ⟧ * suc b) (≤-pred proper) ⟩
                d + o + ⟦ xs ⟧ * suc b
            ≈⟨ cong
                (λ w → w + ⟦ xs ⟧ * suc b)
                (sym (greatest-digit-toℕ (Fin.fromℕ d) (greatest-digit-is-the-Greatest d)))
            ⟩
                ⟦ greatest-digit d ∷ xs ⟧
            □

Maximum? : ∀ {b d o}
    → (xs : Numeral b d o)
    → Dec (Maximum xs)
Maximum? {b} {d} {o} xs with numView b d o
Maximum? xs | NullBase d o = Maximum-NullBase xs
Maximum? xs | NoDigits b o = no (NoDigits-explode xs)
Maximum? xs | AllZeros b   = yes (Maximum-AllZeros xs)
Maximum? xs | Proper b d o proper = no (Maximum-Proper xs proper)

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module Esterel.Lang.CanFunction where

open import utility
  hiding (module ListSet)

open import Esterel.Lang
open import Esterel.Environment as Env
  using (Env ; _←_ ; Θ ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ) renaming (_≟ₛₜ_ to _≟ₛₜₛ_)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ) renaming (_≟ₛₜ_ to _≟ₛₜₛₕ_)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open import Function
  using (_∘_)
open import Relation.Nullary
  using (yes ; no)
open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Relation.Binary
  using (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl)
open import Data.Bool
  using (Bool ; not ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.List
  using (List ; [] ; _∷_ ; [_] ; _++_ ; map ; concatMap ; filter)
open import Data.List.Any
  using (Any ; any)
open import Data.Product
  using (_×_ ; _,_ ; _,′_ ; proj₁ ; proj₂)

import Data.Nat as Nat
open Nat using (ℕ ; zero ; suc)

module SigSet = utility.ListSet Nat._≟_
module ShrSet = utility.ListSet Nat._≟_
module CodeSet = utility.ListSet Code._≟_

-- hide this when importing CanFunction to avoid ambiguity from sn-calculus.agda
[S]-env : (S : Signal) → Env
[S]-env S = Θ SigMap.[ S ↦ Signal.unknown ] ShrMap.empty VarMap.empty

-- The speculative environment used in Canₛ rule and for existing signals in Canθ
[S]-env-absent : (S : Signal) → Env
[S]-env-absent S = Θ SigMap.[ S ↦ Signal.absent ] ShrMap.empty VarMap.empty

-- Helper environment for existing signals in Canθ
[S]-env-present : (S : Signal) → Env
[S]-env-present S = Θ SigMap.[ S ↦ Signal.present ] ShrMap.empty VarMap.empty

Can   : Term → Env → SigSet.ST × CodeSet.ST × ShrSet.ST
Canₛ  : Term → Env → SigSet.ST
Canₖ  : Term → Env → CodeSet.ST
Canₛₕ : Term → Env → ShrSet.ST

Canₛ p θ with Can p θ
... | Ss , _ , _ = Ss
Canₖ p θ with Can p θ
... | _ , ks , _ = ks
Canₛₕ p θ with Can p θ
... | _ , _ , ss = ss

Canθ   : SigMap.Map Signal.Status → ℕ → Term → Env → SigSet.ST × CodeSet.ST × ShrSet.ST
Canθₛ  : SigMap.Map Signal.Status → ℕ → Term → Env → SigSet.ST
Canθₖ  : SigMap.Map Signal.Status → ℕ → Term → Env → CodeSet.ST
Canθₛₕ : SigMap.Map Signal.Status → ℕ → Term → Env → ShrSet.ST

Canθₛ sigs S p θ = proj₁ (Canθ sigs S p θ)
Canθₖ sigs S p θ = proj₁ (proj₂ (Canθ sigs S p θ))
Canθₛₕ sigs S p θ = proj₂ (proj₂ (Canθ sigs S p θ))

Canθ [] S p θ = Can p θ
Canθ (nothing             ∷ sig') S p θ = Canθ sig' (suc S) p θ
Canθ (just Signal.present ∷ sig') S p θ = Canθ sig' (suc S) p (θ ← [S]-env-present (S ₛ))
Canθ (just Signal.absent  ∷ sig') S p θ = Canθ sig' (suc S) p (θ ← [S]-env-absent (S ₛ))
Canθ (just Signal.unknown ∷ sig') S p θ with
  any (Nat._≟_ S) (Canθₛ sig' (suc S) p (θ ← [S]-env (S ₛ)))
... | yes S∈can-p-θ←[S] = Canθ sig' (suc S) p (θ ← [S]-env (S ₛ))
... | no  S∉can-p-θ←[S] = Canθ sig' (suc S) p (θ ← [S]-env-absent (S ₛ))

Can nothin θ =
  [] ,′ [ Code.nothin ] ,′ []
Can pause θ =
  [] ,′ [ Code.pause ] ,′ []
Can (signl S p) θ =
  SigSet.set-remove (Canθₛ (Env.sig ([S]-env S)) 0 p θ) (Signal.unwrap S) ,′
                     Canθₖ (Env.sig ([S]-env S)) 0 p θ ,′
                     Canθₛₕ (Env.sig ([S]-env S)) 0 p θ
Can (present S ∣⇒ p ∣⇒ q) θ with (Env.Sig∈ S θ)
... | yes S∈ =
  if ⌊ Signal.present Signal.≟ₛₜ (Env.sig-stats{S} θ S∈) ⌋
  then Can p θ
  else
    if ⌊ Signal.absent Signal.≟ₛₜ Env.sig-stats{S} θ S∈ ⌋
    then Can q θ
    else Canₛ p θ ++ Canₛ q θ ,′ Canₖ p θ ++ Canₖ q θ ,′ Canₛₕ p θ ++ Canₛₕ q θ
... | no S∉ =
  Canₛ p θ ++ Canₛ q θ ,′ Canₖ p θ ++ Canₖ q θ ,′ Canₛₕ p θ ++ Canₛₕ q θ
Can (emit S) θ = [ (Signal.unwrap S) ] ,′ [ Code.nothin ] ,′ []
Can (p ∥ q) θ =
  Canₛ p θ ++ Canₛ q θ ,′
  concatMap (λ k → map (Code._⊔_ k) (Canₖ q θ)) (Canₖ p θ) ,′
  Canₛₕ p θ ++ Canₛₕ q θ
Can (loop p) θ = Can p θ
Can (loopˢ p q) θ = Can p θ
Can (p >> q) θ with any (Code._≟_ Code.nothin) (Canₖ p θ)
... | no  nothin∉ =
  Can p θ
... | yes nothin∈ =
  Canₛ p θ ++ Canₛ q θ ,′
  (CodeSet.set-remove (Canₖ p θ) Code.nothin) ++ Canₖ q θ ,′
  Canₛₕ p θ ++ Canₛₕ q θ
Can (suspend p S) θ = Can p θ
Can (trap p) θ =
  Canₛ p θ ,′ map Code.↓* (Canₖ p θ) ,′ Canₛₕ p θ
Can (exit n) θ =
  [] ,′ [ Code.exit n ] ,′ []
Can (shared s ≔ e in: p) θ =
  Canₛ p θ ,′
  Canₖ p θ ,′
  ShrSet.set-remove (Canₛₕ p θ) (SharedVar.unwrap s)
Can (s ⇐ e) θ =
  [] ,′ [ Code.nothin ] ,′ [ (SharedVar.unwrap s) ]
Can (var x ≔ e in: p) θ =
  Can p θ
Can (x ≔ e) θ =
  [] ,′ [ Code.nothin ] ,′ []
Can (if x ∣⇒ p ∣⇒ q) θ =
  Canₛ p θ ++ Canₛ q θ ,′ Canₖ p θ ++ Canₖ q θ ,′ Canₛₕ p θ ++ Canₛₕ q θ
Can (ρ⟨ (Θ sig' shr' var') , A ⟩· p) θ =
  SigSet.set-subtract (Canθₛ sig' 0 p θ)  (SigMap.keys sig') ,′
                       Canθₖ sig' 0 p θ ,′
  ShrSet.set-subtract (Canθₛₕ sig' 0 p θ) (ShrMap.keys shr')

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-

Groupoid quotients:

-}

{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.GroupoidQuotients.Properties where

open import Cubical.HITs.GroupoidQuotients.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary.Base

open import Cubical.HITs.PropositionalTruncation as PropTrunc using (∥_∥; ∣_∣; squash)
open import Cubical.HITs.SetTruncation as SetTrunc using (∥_∥₂; ∣_∣₂; squash₂)

-- Type quotients

private
  variable
    ℓA ℓR ℓ : Level
    A : Type ℓA
    R : A → A → Type ℓR
--    B : A // Rt → Type ℓ
--    C : A // Rt → A // Rt → Type ℓ

elimEq// : (Rt : BinaryRelation.isTrans R)
          {B : A // Rt → Type ℓ}
          (Bprop : (x : A // Rt) → isProp (B x))
          {x y : A // Rt}
          (eq : x ≡ y)
          (bx : B x)
          (by : B y) →
          PathP (λ i → B (eq i)) bx by
elimEq// Rt {B} Bprop {x = x} =
  J (λ y eq → ∀ bx by → PathP (λ i → B (eq i)) bx by) (λ bx by → Bprop x bx by)

elimProp : (Rt : BinaryRelation.isTrans R)
         → {B : A // Rt → Type ℓ}
         → ((x : A // Rt) → isProp (B x))
         → ((a : A) → B [ a ])
         → (x : A // Rt)
         → B x
elimProp Rt Bprop f [ x ] = f x
elimProp Rt Bprop f (eq// {a} {b} r i) = elimEq// Rt Bprop (eq// r) (f a) (f b) i
elimProp Rt Bprop f (comp// {a} {b} {c} r s i j) =
  isSet→isSetDep (λ x → isProp→isSet (Bprop x))
  (eq// r) (eq// (Rt a b c r s)) (λ j → [ a ]) (eq// s) (comp// r s)
  (λ i → elimEq// Rt Bprop (eq// r) (f a) (f b) i)
  (λ i → elimEq// Rt Bprop (eq// (Rt a b c r s)) (f a) (f c) i)
  (λ j → f a ) (λ j → elimEq// Rt Bprop (eq// s) (f b) (f c) j) i j
elimProp Rt Bprop f (squash// x y p q r s i j k) =
  isOfHLevel→isOfHLevelDep 3 (λ x → isSet→isGroupoid (isProp→isSet (Bprop x)))
  _ _ _ _ (λ j k → g (r j k)) (λ j k → g (s j k)) (squash// x y p q r s) i j k
  where
    g = elimProp Rt Bprop f

elimProp2 : (Rt : BinaryRelation.isTrans R)
          → {C : A // Rt → A // Rt → Type ℓ}
         → ((x y : A // Rt) → isProp (C x y))
         → ((a b : A) → C [ a ] [ b ])
         → (x y : A // Rt)
         → C x y
elimProp2 Rt Cprop f = elimProp Rt (λ x → isPropΠ (λ y → Cprop x y))
                                   (λ x → elimProp Rt (λ y → Cprop [ x ] y) (f x))

[]surjective : (Rt : BinaryRelation.isTrans R)
               → (x : A // Rt ) → ∃[ a ∈ A ] [ a ] ≡ x
[]surjective Rt = elimProp Rt (λ x → squash) (λ a → ∣ a , refl ∣)

elimSet : (Rt : BinaryRelation.isTrans R)
     → {B : A // Rt → Type ℓ}
     → ((x : A // Rt) → isSet (B x))
     → (f : (a : A) → B [ a ])
     → ({a b : A} (r : R a b) → PathP (λ i → B (eq// r i)) (f a) (f b))
     → (x : A // Rt)
     → B x
elimSet Rt Bset f feq [ a ] = f a
elimSet Rt Bset f feq (eq// r i) = feq r i
elimSet Rt Bset f feq (comp// {a} {b} {c} r s i j) =
  isSet→isSetDep Bset (eq// r) (eq// (Rt a b c r s)) (λ j → [ a ]) (eq// s) (comp// r s)
  (feq r) (feq (Rt a b c r s)) refl (feq s) i j
elimSet Rt Bset f feq (squash// x y p q r s i j k) =
  isOfHLevel→isOfHLevelDep 3 (λ x → isSet→isGroupoid (Bset x))
    _ _ _ _ (λ j k → g (r j k)) (λ j k → g (s j k)) (squash// x y p q r s) i j k
  where
    g = elimSet Rt Bset f feq

elim : (Rt : BinaryRelation.isTrans R)
     → {B : A // Rt → Type ℓ}
     → ((x : A // Rt) → isGroupoid (B x))
     → (f : (a : A) → B [ a ])
     → (feq : {a b : A} (r : R a b) → PathP (λ i → B (eq// r i)) (f a) (f b))
     → ({a b c : A} (r : R a b) (s : R b c)
           → SquareP (λ i j → B (comp// r s i j))
           (feq r) (feq (Rt a b c r s)) (λ j → f a) (feq s))
     → (x : A // Rt)
     → B x
elim Rt Bgpd f feq fcomp [ a ] = f a
elim Rt Bgpd f feq fcomp (eq// r i) = feq r i
elim Rt Bgpd f feq fcomp (comp// r s i j) = fcomp r s i j
elim Rt Bgpd f feq fcomp (squash// x y p q r s i j k) =
  isOfHLevel→isOfHLevelDep 3 Bgpd
    _ _ _ _ (λ j k → g (r j k)) (λ j k → g (s j k)) (squash// x y p q r s) i j k
  where
    g = elim Rt Bgpd f feq fcomp

rec : (Rt : BinaryRelation.isTrans R)
    → {B : Type ℓ}
    → isGroupoid B
    → (f : A → B)
    → (feq : {a b : A} (r : R a b) → f a ≡ f b)
    → ({a b c : A} (r : R a b) (s : R b c)
          → Square (feq r) (feq (Rt a b c r s)) refl (feq s))
    → (x : A // Rt)
    → B
rec Rt Bgpd = elim Rt (λ _ → Bgpd)

module BinarySetRelation {ℓA ℓR : Level} {A : Type ℓA} (R : Rel A A ℓR) where
  open BinaryRelation R

  isSetValued : Type (ℓ-max ℓA ℓR)
  isSetValued = (a b : A) → isSet (R a b)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
-- Andreas, 2016-10-09, re issue #2223

module Issue2223.Setoids where

open import Common.Level

record Setoid c ℓ : Set (lsuc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : Set c
    _≈_           : (x y : Carrier) → Set ℓ

_⟨_⟩_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
        A → (A → B → C) → B → C
x ⟨ f ⟩ y = f x y

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Foundations.Pointed.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' ℓA ℓB ℓC ℓD : Level

-- the default pointed Π-type: A is pointed, and B has a base point in the chosen fiber
Π∙ : (A : Pointed ℓ) (B : typ A → Type ℓ') (ptB : B (pt A)) → Type (ℓ-max ℓ ℓ')
Π∙ A B ptB = Σ[ f ∈ ((a : typ A) → B a) ] f (pt A) ≡ ptB

-- the unpointed Π-type becomes a pointed type if the fibers are all pointed
Πᵘ∙ : (A : Type ℓ) (B : A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Πᵘ∙ A B .fst = ∀ a → typ (B a)
Πᵘ∙ A B .snd a = pt (B a)

-- if the base and all fibers are pointed, we have the pointed pointed Π-type
Πᵖ∙ : (A : Pointed ℓ) (B : typ A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Πᵖ∙ A B .fst = Π∙ A (typ ∘ B) (pt (B (pt A)))
Πᵖ∙ A B  .snd .fst a = pt (B a)
Πᵖ∙ A B  .snd .snd = refl

-- the default pointed Σ-type is just the Σ-type, but as a pointed type
Σ∙ : (A : Pointed ℓ) (B : typ A → Type ℓ') (ptB : B (pt A)) → Pointed (ℓ-max ℓ ℓ')
Σ∙ A B ptB .fst = Σ[ a ∈ typ A ] B a
Σ∙ A B ptB .snd .fst = pt A
Σ∙ A B ptB .snd .snd = ptB

-- version if B is a family of pointed types
Σᵖ∙ : (A : Pointed ℓ) (B : typ A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Σᵖ∙ A B = Σ∙ A (typ ∘ B) (pt (B (pt A)))

_×∙_ : (A∙ : Pointed ℓ) (B∙ : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
(A∙ ×∙ B∙) .fst = (typ A∙) × (typ B∙)
(A∙ ×∙ B∙) .snd .fst = pt A∙
(A∙ ×∙ B∙) .snd .snd = pt B∙

-- composition of pointed maps
_∘∙_ : {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC}
       (g : B →∙ C) (f : A →∙ B) → (A →∙ C)
((g , g∙) ∘∙ (f , f∙)) .fst x = g (f  x)
((g , g∙) ∘∙ (f , f∙)) .snd = (cong g f∙) ∙ g∙

-- post composition
post∘∙ : ∀ {ℓX ℓ ℓ'} (X : Pointed ℓX) {A : Pointed ℓ} {B : Pointed ℓ'}
  → (A →∙ B) → ((X →∙ A ∙) →∙ (X →∙ B ∙))
post∘∙ X f .fst g = f ∘∙ g
post∘∙ X f .snd =
  ΣPathP
    ( (funExt λ _ → f .snd)
    , (sym (lUnit (f .snd)) ◁ λ i j → f .snd (i ∨ j)))

-- pointed identity
id∙ : (A : Pointed ℓA) → (A →∙ A)
id∙ A .fst x = x
id∙ A .snd = refl

-- constant pointed map
const∙ : (A : Pointed ℓA) (B : Pointed ℓB) → (A →∙ B)
const∙ _ B .fst _ = B .snd
const∙ _ B .snd = refl

-- left identity law for pointed maps
∘∙-idˡ : {A : Pointed ℓA} {B : Pointed ℓB} (f : A →∙ B) → f ∘∙ id∙ A ≡ f
∘∙-idˡ f = ΣPathP ( refl , (lUnit (f .snd)) ⁻¹ )

-- right identity law for pointed maps
∘∙-idʳ : {A : Pointed ℓA} {B : Pointed ℓB} (f : A →∙ B) → id∙ B ∘∙ f ≡ f
∘∙-idʳ f = ΣPathP ( refl , (rUnit (f .snd)) ⁻¹ )

-- associativity for composition of pointed maps
∘∙-assoc : {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC} {D : Pointed ℓD}
           (h : C →∙ D) (g : B →∙ C) (f : A →∙ B)
           → (h ∘∙ g) ∘∙ f ≡ h ∘∙ (g ∘∙ f)
∘∙-assoc (h , h∙) (g , g∙) (f , f∙) = ΣPathP (refl , q)
  where
    q : (cong (h ∘ g) f∙) ∙ (cong h g∙ ∙ h∙) ≡ cong h (cong g f∙ ∙ g∙) ∙ h∙
    q = ( (cong (h ∘ g) f∙) ∙ (cong h g∙ ∙ h∙)
        ≡⟨ refl ⟩
        (cong h (cong g f∙)) ∙ (cong h g∙ ∙ h∙)
        ≡⟨ assoc (cong h (cong g f∙)) (cong h g∙) h∙ ⟩
        (cong h (cong g f∙) ∙ cong h g∙) ∙ h∙
        ≡⟨ cong (λ p → p ∙ h∙) ((cong-∙ h (cong g f∙) g∙) ⁻¹) ⟩
        (cong h (cong g f∙ ∙ g∙) ∙ h∙) ∎ )

module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) where
  isInIm∙ : (x : typ B) → Type (ℓ-max ℓ ℓ')
  isInIm∙ x = Σ[ z ∈ typ A ] fst f z ≡ x

  isInKer∙ : (x : fst A) → Type ℓ'
  isInKer∙ x = fst f x ≡ snd B

pre∘∙equiv : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B C : Pointed ℓ'}
 → (B ≃∙ C) → Iso (A →∙ B) (A →∙ C)
pre∘∙equiv {A = A} {B = B} {C = C} eq = main
  where
  module _ {ℓ ℓ' : Level} (A : Pointed ℓ) (B C : Pointed ℓ')
           (eq : (B ≃∙ C)) where
    to : (A →∙ B) → (A →∙ C)
    to = ≃∙map eq ∘∙_

    from : (A →∙ C) → (A →∙ B)
    from = ≃∙map (invEquiv∙ eq) ∘∙_

  lem : {ℓ  : Level} {B : Pointed ℓ}
    → ≃∙map (invEquiv∙ {A = B} ((idEquiv (fst B)) , refl)) ≡ id∙ B
  lem = ΣPathP (refl , (sym (lUnit _)))

  J-lem : {ℓ ℓ' : Level} {A : Pointed ℓ} {B C : Pointed ℓ'}
             → (eq : (B ≃∙ C))
             → retract (to A B C eq) (from _ _ _ eq)
              × section (to A B C eq) (from _ _ _ eq)
  J-lem {A = A} {B = B} {C = C} =
    Equiv∙J (λ B eq → retract (to A B C eq) (from _ _ _ eq)
              × section (to A B C eq) (from _ _ _ eq))
            ((λ f → ((λ i → (lem i ∘∙ (id∙ C ∘∙ f)))
                  ∙ λ i → ∘∙-idʳ (∘∙-idʳ f i) i))
            , λ f → ((λ i → (id∙ C ∘∙ (lem i ∘∙ f)))
                  ∙ λ i → ∘∙-idʳ (∘∙-idʳ f i) i))

  main : Iso (A →∙ B) (A →∙ C)
  Iso.fun main = to A B C eq
  Iso.inv main = from A B C eq
  Iso.rightInv main = J-lem eq .snd
  Iso.leftInv main = J-lem eq .fst

post∘∙equiv : ∀ {ℓ ℓC} {A B : Pointed ℓ} {C : Pointed ℓC}
  → (A ≃∙ B) → Iso (A →∙ C) (B →∙ C)
post∘∙equiv {A = A} {B = B} {C = C} eq = main
  where
  module _ {ℓ ℓC : Level} (A B : Pointed ℓ) (C : Pointed ℓC)
           (eq : (A ≃∙ B)) where
    to : (A →∙ C) → (B →∙ C)
    to = _∘∙ ≃∙map (invEquiv∙ eq)

    from : (B →∙ C) → (A →∙ C)
    from = _∘∙ ≃∙map eq

  lem : {ℓ  : Level} {B : Pointed ℓ}
    → ≃∙map (invEquiv∙ {A = B} ((idEquiv (fst B)) , refl)) ≡ id∙ B
  lem = ΣPathP (refl , (sym (lUnit _)))

  J-lem : {ℓ ℓC : Level} {A B : Pointed ℓ} {C : Pointed ℓC}
             → (eq : (A ≃∙ B))
             → retract (to A B C eq) (from _ _ _ eq)
              × section (to A B C eq) (from _ _ _ eq)
  J-lem {B = B} {C = C} =
    Equiv∙J (λ A eq → retract (to A B C eq) (from _ _ _ eq)
              × section (to A B C eq) (from _ _ _ eq))
            ((λ f → ((λ i → (f ∘∙ lem i) ∘∙ id∙ B)
                  ∙ λ i → ∘∙-idˡ (∘∙-idˡ f i) i))
           , λ f → (λ i → (f ∘∙ id∙ B) ∘∙ lem i)
                  ∙ λ i → ∘∙-idˡ (∘∙-idˡ f i) i)

  main : Iso (A →∙ C) (B →∙ C)
  Iso.fun main = to A B C eq
  Iso.inv main = from A B C eq
  Iso.rightInv main = J-lem eq .snd
  Iso.leftInv main = J-lem eq .fst

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2013-09-17
module DoNotEtaContractFunIntoRecord where

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

postulate
  A : Set
  B : Set
  P : (B → A × B) → Set

goal : (x : A) → P (λ y → x , y)
goal x = {!!}

-- Goal should be displayed as
--   P (λ y → x , y)
-- rather than as
--   P (_,_ x)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.Types
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open        WithAbsVote

module LibraBFT.Concrete.Obligations.PreferredRound
  (𝓔 : EpochConfig)
  (𝓥 : VoteEvidence 𝓔)
  where
 open import LibraBFT.Abstract.Abstract UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Concrete.Intermediate               𝓔 𝓥

 ---------------------
 -- * PreferredRound * --
 ---------------------

 module _ {ℓ}(𝓢 : IntermediateSystemState ℓ) where
  open IntermediateSystemState 𝓢

 -- The PreferredRound rule is a little more involved to be expressed in terms
 -- of /HasBeenSent/: it needs two additional pieces which are introduced
 -- next.

 -- Cand-3-chain v carries the information for estabilishing
 -- that v.proposed will be part of a 3-chain if a QC containing v is formed.
 -- The difficulty is that we can't easily access the "grandparent" of a vote.
 -- Instead, we must explicitly state that it exists.
 --
 --                                candidate 3-chain
 --       +------------------------------------------------------+
 --       |                                                      |
 --       |       2-chain                                        |
 --       +----------------------------------+
 --  ⋯ <- v.grandparent <- q₁ <- v.parent <- q <- v.proposed  <- v
 --                                          ̭
 --                                          |
 --                                     The 'qc' defined below is an
 --                                     abstract view of q, above.
  record voteExtends (v : Vote) : Set where
    constructor mkVE
    field
      veBlock   : Block
      veId      : vBlockUID v ≡ bId    veBlock
      veRounds≡ : vRound    v ≡ bRound veBlock
  open voteExtends

  record Cand-3-chain-vote (v : Vote) : Set where
    field
      votesForB : voteExtends v
      qc        : QC
      qc←b      : Q qc ← B (veBlock votesForB)
      rc        : RecordChain (Q qc)
      n         : ℕ
      is-2chain : 𝕂-chain Contig (2 + n) rc
  open Cand-3-chain-vote public

  -- Returns the round of the head of the candidate 3-chain. In the diagram
  -- explaining Cand-3-chain-vote, this would be v.grandparent.round.
  Cand-3-chain-head-round : ∀{v} → Cand-3-chain-vote v → Round
  Cand-3-chain-head-round c3cand =
    getRound (kchainBlock (suc zero) (is-2chain c3cand))

  -- The preferred round rule states a fact about the /previous round/
  -- of a vote; that is, the round of the parent of the block
  -- being voted for; the implementation will have to
  -- show it can construct this parent.
  data VoteParentData-BlockExt : Record → Set where
    vpParent≡I : VoteParentData-BlockExt I
    vpParent≡Q : ∀{b q} → B b ← Q q → VoteParentData-BlockExt (Q q)

  -- TODO-2: it may be cleaner to specify this as a RC 2 vpParent vpQC,
  -- and we should consider it once we address the issue in
  -- Abstract.RecordChain (below the definition of transp-𝕂-chain)

  record VoteParentData (v : Vote) : Set where
    field
      vpExt        : voteExtends v
      vpParent     : Record
      vpExt'       : vpParent ← B (veBlock vpExt)
      vpMaybeBlock : VoteParentData-BlockExt vpParent
  open VoteParentData public

  -- The setup for PreferredRoundRule is like thta for VotesOnce.
  -- Given two votes by an honest author α:
  Type : Set ℓ
  Type = ∀{α v v'}
       → Meta-Honest-Member α
       → vMember v  ≡ α → HasBeenSent v
       → vMember v' ≡ α → HasBeenSent v'
       -- If v is a vote on a candidate 3-chain, that is, is a vote on a block
       -- that extends a 2-chain,
       → (c2 : Cand-3-chain-vote v)
       -- and the round of v is lower than that of v',
       → vRound v < vRound v'
       ------------------------------
       -- then α obeyed the preferred round rule:
       → Σ (VoteParentData v')
           (λ vp → Cand-3-chain-head-round c2 ≤ round (vpParent vp))

  private
   make-cand-3-chain : ∀{n α q}{rc : RecordChain (Q q)}
                     → (c3 : 𝕂-chain Contig (3 + n) rc)
                     → (v  : α ∈QC q)
                     → Cand-3-chain-vote (∈QC-Vote q v)
   make-cand-3-chain {q = q} (s-chain {suc (suc n)} {rc = rc} {b = b} ext₀@(Q←B h0 refl) _ ext₁@(B←Q h1 refl) c2) v
     with c2
   ...| (s-chain {q = q₀} _ _ _ (s-chain _ _ _ c))
       = record { votesForB = mkVE b (All-lookup (qVotes-C2 q) (Any-lookup-correct v))
                                      (trans (All-lookup (qVotes-C3 q) (Any-lookup-correct v)) h1)
                ; qc = q₀
                ; qc←b = ext₀
                ; rc = rc
                ; n  = n
                ; is-2chain = c2
                }

   -- It is important that the make-cand-3-chain lemma doesn't change the head of
   -- the 3-chain/cand-2-chain.
   make-cand-3-chain-lemma
     : ∀{n α q}{rc : RecordChain (Q q)}
     → (c3 : 𝕂-chain Contig (3 + n) rc)
     → (v  : α ∈QC q)
     → NonInjective-≡ bId ⊎ kchainBlock (suc zero) (is-2chain (make-cand-3-chain c3 v)) ≡ kchainBlock (suc (suc zero)) c3
   make-cand-3-chain-lemma {q = q} c3@(s-chain {suc (suc n)} {rc = rc} {b = b} ext₀@(Q←B h0 refl) _ ext₁@(B←Q h1 refl) c2) v
     with (veBlock (Cand-3-chain-vote.votesForB (make-cand-3-chain c3 v))) ≟Block b
   ...| no neq = inj₁ ((veBlock (Cand-3-chain-vote.votesForB (make-cand-3-chain c3 v)) , b)
                      , neq
                      , trans (sym (veId (votesForB (make-cand-3-chain c3 v))))
                              (All-lookup (qVotes-C2 q) (∈QC-Vote-correct q v)))
   ...| yes b≡
     with c2
   ...| (s-chain {q = q₀} _ _ _ (s-chain _ _ _ c)) rewrite b≡ = inj₂ refl

   vdParent-prevRound-lemma
      : ∀{α q}(rc : RecordChain (Q q))(va : α ∈QC q)
      → (vp : VoteParentData (∈QC-Vote q va))
      → NonInjective-≡ bId ⊎ (round (vpParent vp) ≡ prevRound rc)
   vdParent-prevRound-lemma {q = q} (step {r = B b} (step rc y) x@(B←Q refl refl)) va vp
     with b ≟Block (veBlock (vpExt vp))
   ...| no imp = inj₁ ( (b , veBlock (vpExt vp))
                      , (imp , id-B∨Q-inj (cong id-B∨Q (trans (sym (All-lookup (qVotes-C2 q) (∈QC-Vote-correct q va)))
                                                               (veId (vpExt vp))))))
   ...| yes refl
     with ←-inj y (vpExt' vp)
   ...| bSameId'
     with y | vpExt' vp
   ...| I←B y0 y1   | I←B e0 e1   = inj₂ refl
   ...| Q←B y0 refl | Q←B e0 refl
     with vpMaybeBlock vp
   ...| vpParent≡Q {b = bP} bP←qP
     with rc
   ...| step {r = B b'} rc' b←q
     with b' ≟Block bP
   ...| no  imp = inj₁ ((b' , bP) , imp , id-B∨Q-inj (lemmaS1-2 (eq-Q refl) b←q bP←qP))
   ...| yes refl
     with bP←qP | b←q
   ...| B←Q refl refl | B←Q refl refl = inj₂ refl

  -- Finally, we can prove the preferred round rule from the global version;
  proof : Type → PreferredRoundRule InSys
  proof glob-inv α hα {q} {q'} q∈sys q'∈sys c3 va rc' va' hyp
    with ∈QC⇒HasBeenSent q∈sys  hα va
       | ∈QC⇒HasBeenSent q'∈sys hα va'
  ...| sent-cv | sent-cv'
    with make-cand-3-chain c3  va | inspect
        (make-cand-3-chain c3) va
  ...| cand | [ R ]
    with glob-inv hα
           (sym (∈QC-Member q  va )) sent-cv
           (sym (∈QC-Member q' va')) sent-cv'
           cand hyp
  ...| va'Par , res
    with vdParent-prevRound-lemma rc' va' va'Par
  ...| inj₁ hb    = inj₁ hb
  ...| inj₂ final
    with make-cand-3-chain-lemma c3 va
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ xx = inj₂ (subst₂ _≤_
          (cong bRound (trans (cong (kchainBlock (suc zero) ∘ is-2chain) (sym R)) xx))
          final
          res)

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{- An adaptation of Edwin Brady and Kevin Hammond's paper Scrapping your inefficient engine ... -}
{-# OPTIONS --type-in-type #-}
module tests.Cat where

open import Prelude.Bool
open import Prelude.Bot
open import Prelude.IO
open import Prelude.Fin
open import Prelude.Eq
open import Prelude.Nat
open import Prelude.Product
open import Prelude.String
open import Prelude.Unit
open import Prelude.Vec

record Top : Set where
  constructor tt

data Ty : Set where
  TyUnit   : Ty
  TyBool   : Ty
  TyLift   : Set -> Ty
  TyHandle : Nat -> Ty

interpTy : Ty -> Set
interpTy TyUnit       = Unit
interpTy TyBool       = Bool
interpTy (TyLift A)   = A
interpTy (TyHandle n) = Fin n

data Purpose : Set where
  Reading : Purpose
  Writing : Purpose

getMode : Purpose -> String
getMode Reading = "r"
getMode Writing = "w"

data FileState : Set where
  Open   : Purpose -> FileState
  Closed : FileState

postulate
  EpicFile : Set

static[_] : {A : Set} → A → A
static[ x ] = x

{-# STATIC static[_] #-}

FileVec : Nat -> Set
FileVec n = Vec FileState n

data FileHandle : FileState -> Set where
  OpenFile   : ∀{p} -> EpicFile -> FileHandle (Open p)
  ClosedFile : FileHandle Closed

data Env : ∀{n} -> FileVec n -> Set where
  Empty  : Env []
  Extend : {n : Nat}{T : FileState}{G : FileVec n} -> (res : FileHandle T) -> Env G -> Env (T :: G)

addEnd : ∀{n T}{G : FileVec n} -> Env G -> FileHandle T -> Env (snoc G T)
addEnd Empty         fh = Extend fh Empty
addEnd (Extend x xs) fh = Extend x (addEnd xs fh)

updateEnv : ∀{n T}{G : FileVec n} -> Env G -> (i : Fin n) -> (fh : FileHandle T) -> Env (G [ i ]= T)
updateEnv (Extend x xs) fz     e = Extend e xs
updateEnv (Extend x xs) (fs n) e = Extend x (updateEnv xs n e)
updateEnv Empty         ()     e

bound : ∀{n : Nat} -> Fin (S n)
bound {Z}   = fz
bound {S n} = fs (bound {n})

_==P_ : Purpose -> Purpose -> Set
Reading ==P Reading = Top
Reading ==P Writing = Bot
Writing ==P Reading = Bot
Writing ==P Writing = Top

OpenH : ∀{n} -> Fin n -> Purpose -> FileVec n -> Set
OpenH fz p (Open p' :: as) = p ==P p'
OpenH fz p (Closed  :: as) = Bot
OpenH (fs i) p ( a  :: as) = OpenH i p as

getFile : ∀{n}{i : Fin n}{p : Purpose}{ts : FileVec n}{ope : OpenH i p ts} -> Env ts -> EpicFile
getFile {Z} {()} env
getFile {S y} {fz} (Extend (OpenFile y') y0) = y'
getFile {S y} {fz} {ope = ()} (Extend ClosedFile y')
getFile {S y} {fs y'} {ope = ope} (Extend res y0) = getFile {y} {y'} {ope = ope} y0

getPurpose : {n : Nat} -> Fin n -> FileVec n -> Purpose
getPurpose f ts with ts ! f
... | Open p = p
... | Closed = Reading -- Should not happen right?

FilePath : Set
FilePath = String

data File : ∀{n n'}  -> FileVec n -> FileVec n' -> Ty -> Set where
  ACTION  : ∀{a l}{ts : FileVec l}  -> IO (interpTy a) -> File ts ts a
  RETURN  : ∀{a l}{ts : FileVec l}  -> interpTy a -> File ts ts a
  WHILE   : ∀{l}{ts : FileVec l}    -> File ts ts TyBool -> File ts ts TyUnit -> File ts ts TyUnit
  IF      : ∀{a l}{ts : FileVec l}  -> Bool -> File ts ts a -> File ts ts a -> File ts ts a
  BIND    : ∀{a b l l' l''}{ts : FileVec l}{ts' : FileVec l'}{ts'' : FileVec l''}
         -> File ts ts' a -> (interpTy a -> File ts' ts'' b) -> File ts ts'' b
  OPEN    : ∀{l}{ts : FileVec l}
          -> (p : Purpose) -> (fd : FilePath) -> File ts (snoc ts (Open p)) (TyHandle (S l))
  CLOSE   : ∀ {l}{ts : FileVec l} -> (i : Fin l) -> {p : OpenH i (getPurpose i ts) ts} -> File ts (ts [ i ]= Closed) TyUnit
  GETLINE : ∀ {l}{ts : FileVec l} -> (i : Fin l) -> {p : OpenH i Reading ts} -> File ts ts (TyLift String)
  EOF     : ∀ {l}{ts : FileVec l} -> (i : Fin l) -> {p : OpenH i Reading ts} -> File ts ts TyBool
  PUTLINE : ∀ {l}{ts : FileVec l} -> (i : Fin l) -> (str : String) -> {p : OpenH i Writing ts} -> File ts ts TyUnit

postulate
  while  : IO Bool -> IO Unit -> IO Unit
  fopen  : FilePath -> String -> IO EpicFile
  fclose : EpicFile -> IO Unit
  fread  : EpicFile -> IO String
  feof   : EpicFile -> IO Bool
  fwrite : EpicFile -> String -> IO Unit

{-# COMPILED_EPIC while (add : Any, body : Any, u : Unit) -> Any = %while (add(u), body(u)) #-}
{-# COMPILED_EPIC fopen (fp : Any, mode : Any, u : Unit) -> Ptr = foreign Ptr "fopen" (mkString(fp) : String, mkString(mode) : String) #-}
{-# COMPILED_EPIC fclose (file : Ptr, u : Unit) -> Unit = foreign Int "fclose" (file : Ptr); unit #-}
{-# COMPILED_EPIC fread (file : Ptr, u : Unit) -> Any = frString(foreign String "freadStrChunk" (file : Ptr)) #-}
{-# COMPILED_EPIC feof (file : Ptr, u : Unit) -> Bool = foreign Int "feof" (file : Ptr) #-}
{-# COMPILED_EPIC fwrite (file : Ptr, str : Any, u : Unit) -> Unit =  foreign Unit "fputs" (mkString(str) : String, file : Ptr) #-}

fmap : {A B : Set} -> (A -> B) -> IO A -> IO B
fmap f io =
  x <- io ,
  return (f x)

data MIO (A : Set) : Set where
  Return : A -> MIO A
  ABind  : {B : Set} -> IO B -> (B -> MIO A) -> MIO A
  -- While  : MIO Bool -> MIO Unit -> MIO Unit

MBind : {A B : Set} -> MIO A -> (A -> MIO B) -> MIO B
MBind (Return x) f = f x
MBind (ABind io k) f = ABind io (λ x -> MBind (k x) f)
-- MBind (While b u) f  =

mmap : {A B : Set} -> (A -> B) -> MIO A -> MIO B
mmap f mio = MBind mio (λ x -> Return (f x))

runMIO : {A : Set} -> MIO A -> IO A
runMIO (Return x) = return x
runMIO (ABind io f) =
   x <- io ,
   runMIO (f x)

interp : ∀{n n' T}{ts : FileVec n}{ts' : FileVec n'} -> Env ts -> File ts ts' T -> MIO (Env ts' × interpTy T)
interp env (ACTION io) = ABind io (λ x -> Return (env , x))
interp env (RETURN val) = Return (env , val)
interp env (WHILE add body) =
    ABind (while (runMIO (mmap snd (interp env add))) (runMIO (mmap snd (interp env body)))) (λ _ ->
    Return (env , unit))
interp env (IF b t f) = if b then interp env t else interp env f
interp env (BIND code k) =
    MBind (interp env code) (λ v ->
    interp (fst v) (k (snd v)))
interp env (OPEN p fpath) =
    ABind (fopen fpath (getMode p)) (λ fh ->
    Return (addEnd env (OpenFile fh), bound))
interp env (CLOSE i {p = p}) =
    ABind (fclose (getFile {_} {i} {ope = p} env)) (\ _ ->
    Return (updateEnv env i ClosedFile , unit))
interp env (GETLINE i {p = p}) =
    ABind (fread (getFile {_} {i} {ope = p} env)) (λ x -> Return (env , x))
interp env (EOF i {p = p}) =

    ABind (feof (getFile {_} {i} {ope = p} env)) (\ e ->
    Return (env , e))
interp env (PUTLINE i str {p = p}) =
      ABind (fwrite (getFile {i = i} {ope = p} env) str) (λ _ ->
      ABind (fwrite (getFile {i = i} {ope = p} env) "\n") (λ x ->
      Return (env , unit)))

allClosed : (n : Nat) -> FileVec n
allClosed Z     = []
allClosed (S n) = Closed :: allClosed n

syntax BIND e (\ x -> f) = x := e % f
infixl 0 BIND

_%%_ : ∀{a b l l' l''}{ts : FileVec l}{ts' : FileVec l'}{ts'' : FileVec l''}
         -> File ts ts' a -> File ts' ts'' b -> File ts ts'' b
m %% k = BIND m (λ _ -> k)
infixr 0 _%%_

{-
cat : File [] (Closed :: []) TyUnit
cat = (
    fz := OPEN Reading "tests/Cat.out" %
    WHILE (b := EOF fz % RETURN (not b)) (
        str := GETLINE fz %
        ACTION (putStrLn str)
    ) %%
    CLOSE fz
 )

cont : Fin 1 -> File (Open Reading :: []) (Closed :: []) TyUnit
cont (fs ())
cont fz =  BIND (WHILE (BIND (EOF fz) (\b -> RETURN (not b)))
                       (BIND (GETLINE fz)
                             (\str -> ACTION (putStrLn str))
                       )
                )
                (λ x → CLOSE fz)

cat : File [] (Closed :: []) TyUnit
cat = BIND (OPEN Reading "hej")
            cont

-}

cont : Fin 1 -> File (Open Reading :: []) (Closed :: []) TyUnit
cont (fs ())
cont fz =
  WHILE ( b := EOF fz % RETURN (not b)) (
      str := GETLINE fz %
      ACTION (putStr str)
  ) %%
  CLOSE fz

cat : File [] (Closed :: []) TyUnit
cat = BIND (OPEN Reading "tests/Cat.out") cont

copy : File [] (Closed :: Closed :: []) TyUnit
copy =
  BIND (OPEN Reading "copy/input")  (λ _ →
  BIND (OPEN Writing "copy/output") (λ _ →
  BIND (WHILE (BIND (EOF fz) (λ b → RETURN (not b)))
       (BIND (GETLINE fz) (λ str → PUTLINE (fs fz) str))) (λ _ →
  BIND (CLOSE fz) (λ _ →
  CLOSE (fs fz)))))

runProg : {n : Nat} -> File [] (allClosed n) TyUnit -> IO Unit
runProg p = runMIO (mmap snd (interp Empty p))

{-# STATIC runProg #-}

main : IO Unit
main = runProg cat -- static[ runProg cat ]
-- main = runProg cat

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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

open import Relation.Binary
open import Prelude

module Data.List.Sort.MergeSort {e} {E : Type e} {r₁ r₂} (totalOrder : TotalOrder E r₁ r₂) where

open TotalOrder totalOrder hiding (refl)

open import Data.List.Sort.InsertionSort totalOrder using (insert; insert-sort)

open import Data.List
open import Data.List.Properties

open import TreeFold

open import Algebra
open import Relation.Nullary.Decidable.Properties using (from-reflects)
open import Path.Reasoning

mergeˡ :  E → (List E → List E) → List E → List E
mergeˡ x xs []       = x ∷ xs []
mergeˡ x xs (y ∷ ys) = if x ≤ᵇ y then x ∷ xs (y ∷ ys) else y ∷ mergeˡ x xs ys

_⋎_ : List E → List E → List E
_⋎_ = foldr mergeˡ id

merge-idʳ : ∀ xs → xs ⋎ [] ≡ xs
merge-idʳ [] = refl
merge-idʳ (x ∷ xs) = cong (x ∷_) (merge-idʳ xs)

merge-assoc : Associative _⋎_
merge-assoc []       ys zs = refl
merge-assoc (x ∷ xs) [] zs = cong (λ xs′ → mergeˡ x (xs′ ⋎_) zs) (merge-idʳ xs)
merge-assoc (x ∷ xs) (y ∷ ys) [] = merge-idʳ ((x ∷ xs) ⋎ (y ∷ ys)) ; cong ((x ∷ xs) ⋎_) (sym (merge-idʳ (y ∷ ys)))
merge-assoc (x ∷ xs) (y ∷ ys) (z ∷ zs)
  with merge-assoc xs (y ∷ ys) (z ∷ zs)
     | merge-assoc (x ∷ xs) ys (z ∷ zs)
     | merge-assoc (x ∷ xs) (y ∷ ys) zs
     | x ≤? y in x≤?y
     | y ≤? z in y≤?z
... | _ | _ | r | no x≰y | no y≰z rewrite y≤?z rewrite x≤?y =
  cong (z ∷_) r ;
  cong (bool′ _ _)
    (sym (from-reflects false (x ≤? z) (<⇒≱ (<-trans (≰⇒> y≰z) (≰⇒> x≰y)))))
... | _ | r | _ | no  x≰y | yes y≤z rewrite y≤?z rewrite x≤?y = cong (y ∷_) r
... | r | _ | _ | yes x≤y | yes y≤z rewrite y≤?z rewrite x≤?y =
  cong (bool′ _ _)
    (from-reflects true (x ≤? z) (≤-trans x≤y y≤z)) ;
  cong (x ∷_) r
merge-assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) | rx≤z | _ | rx≰z | yes x≤y | no y≰z with x ≤? z
... | no  x≰z rewrite x≤?y = cong (z ∷_) rx≰z
... | yes x≤z rewrite y≤?z = cong (x ∷_) rx≤z

merge-sort : List E → List E
merge-sort = treeFold _⋎_ [] ∘ map (_∷ [])

merge-insert : ∀ x xs → (x ∷ []) ⋎ xs ≡ insert x xs
merge-insert x [] = refl
merge-insert x (y ∷ xs) with x ≤ᵇ y
... | false = cong (y ∷_) (merge-insert x xs)
... | true  = refl

merge≡insert-sort : ∀ xs → merge-sort xs ≡ insert-sort xs
merge≡insert-sort xs =
  merge-sort xs                      ≡⟨⟩
  treeFold _⋎_ [] (map (_∷ []) xs)   ≡⟨ treeFoldHom _⋎_ [] merge-assoc (map (_∷ []) xs) ⟩
  foldr _⋎_ [] (map (_∷ []) xs)      ≡⟨ map-fusion _⋎_ [] (_∷ []) xs ⟩
  foldr (λ x → (x ∷ []) ⋎_) [] xs    ≡⟨ cong (λ f → foldr f [] xs) (funExt (funExt ∘ merge-insert)) ⟩
  foldr insert [] xs                 ≡⟨⟩
  insert-sort xs ∎

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
import Structure.Logic.Classical.NaturalDeduction

module Structure.Logic.Classical.NaturalDeduction.Proofs {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)

open import Functional hiding (Domain)

-- TODO: Move the ones which are constructive

[↔]-with-[∧]ₗ : ∀{a₁ a₂ b} → Proof(a₁ ⟷ a₂) → Proof((a₁ ∧ b) ⟷ (a₂ ∧ b))
[↔]-with-[∧]ₗ (proof) =
  ([↔].intro
    (a₂b ↦ [∧].intro (([↔].elimₗ proof) ([∧].elimₗ a₂b)) ([∧].elimᵣ a₂b))
    (a₁b ↦ [∧].intro (([↔].elimᵣ proof) ([∧].elimₗ a₁b)) ([∧].elimᵣ a₁b))
  )

[↔]-with-[∧]ᵣ : ∀{a b₁ b₂} → Proof(b₁ ⟷ b₂) → Proof((a ∧ b₁) ⟷ (a ∧ b₂))
[↔]-with-[∧]ᵣ (proof) =
  ([↔].intro
    (ab₂ ↦ [∧].intro ([∧].elimₗ ab₂) (([↔].elimₗ proof) ([∧].elimᵣ ab₂)))
    (ab₁ ↦ [∧].intro ([∧].elimₗ ab₁) (([↔].elimᵣ proof) ([∧].elimᵣ ab₁)))
  )

[↔]-with-[∧] : ∀{a₁ a₂ b₁ b₂} → Proof(a₁ ⟷ a₂) → Proof(b₁ ⟷ b₂) → Proof((a₁ ∧ b₁) ⟷ (a₂ ∧ b₂))
[↔]-with-[∧] (a₁a₂) (b₁b₂) =
  ([↔].intro
    (a₂b₂ ↦ [∧].intro (([↔].elimₗ a₁a₂) ([∧].elimₗ a₂b₂)) (([↔].elimₗ b₁b₂) ([∧].elimᵣ a₂b₂)))
    (a₁b₁ ↦ [∧].intro (([↔].elimᵣ a₁a₂) ([∧].elimₗ a₁b₁)) (([↔].elimᵣ b₁b₂) ([∧].elimᵣ a₁b₁)))
  )

[↔]-with-[∨]ₗ : ∀{a₁ a₂ b} → Proof(a₁ ⟷ a₂) → Proof((a₁ ∨ b) ⟷ (a₂ ∨ b))
[↔]-with-[∨]ₗ (proof) =
  ([↔].intro
    ([∨].elim([∨].introₗ ∘ ([↔].elimₗ proof)) [∨].introᵣ)
    ([∨].elim([∨].introₗ ∘ ([↔].elimᵣ proof)) [∨].introᵣ)
  )

[↔]-with-[∨]ᵣ : ∀{a b₁ b₂} → Proof(b₁ ⟷ b₂) → Proof((a ∨ b₁) ⟷ (a ∨ b₂))
[↔]-with-[∨]ᵣ (proof) =
  ([↔].intro
    ([∨].elim [∨].introₗ ([∨].introᵣ ∘ ([↔].elimₗ proof)))
    ([∨].elim [∨].introₗ ([∨].introᵣ ∘ ([↔].elimᵣ proof)))
  )

[↔]-with-[∨] : ∀{a₁ a₂ b₁ b₂} → Proof(a₁ ⟷ a₂) → Proof(b₁ ⟷ b₂) → Proof((a₁ ∨ b₁) ⟷ (a₂ ∨ b₂))
[↔]-with-[∨] (a₁a₂) (b₁b₂) =
  ([↔].intro
    ([∨].elim ([∨].introₗ ∘ ([↔].elimₗ a₁a₂)) ([∨].introᵣ ∘ ([↔].elimₗ b₁b₂)))
    ([∨].elim ([∨].introₗ ∘ ([↔].elimᵣ a₁a₂)) ([∨].introᵣ ∘ ([↔].elimᵣ b₁b₂)))
  )

[↔]-with-[∀] : ∀{f g} → (∀{x} → Proof(f(x) ⟷ g(x))) → Proof((∀ₗ f) ⟷ (∀ₗ g))
[↔]-with-[∀] (proof) =
  ([↔].intro
    (allg ↦ [∀].intro(\{x} → [↔].elimₗ (proof{x}) ([∀].elim(allg){x})))
    (allf ↦ [∀].intro(\{x} → [↔].elimᵣ (proof{x}) ([∀].elim(allf){x})))
  )

[↔]-with-[∃] : ∀{f g} → (∀{x} → Proof(f(x) ⟷ g(x))) → Proof((∃ₗ f) ⟷ (∃ₗ g))
[↔]-with-[∃] (proof) =
  ([↔].intro
    ([∃].elim(\{x} → gx ↦ [∃].intro{_}{x}([↔].elimₗ (proof{x}) (gx))))
    ([∃].elim(\{x} → fx ↦ [∃].intro{_}{x}([↔].elimᵣ (proof{x}) (fx))))
  )

-- [→]-with-[∀] : ∀{p f g} → (∀{x} → Proof(f(x) ⟶ g(x))) → Proof((∀ₗ f) ⟶ (∀ₗ g))
-- [→]-with-[∀] (proof) =

-- [→]-with-[∀] : ∀{p f g} → (∀{x} → Proof(f(x) ⟶ g(x))) → Proof(∀ₗ(x ↦ p(x) ⟶ f(x))) → Proof(∀ₗ(x ↦ p(x) ⟶ g(x)))
-- [→]-with-[∀] (proof) =

[∨][∧]-distributivityₗ : ∀{a b c} → Proof((a ∨ (b ∧ c)) ⟷ (a ∨ b)∧(a ∨ c))
[∨][∧]-distributivityₗ =
  ([↔].intro
    (a∨b∧a∨c ↦
      ([∨].elim
        (a ↦ [∨].introₗ a)
        (b ↦
          ([∨].elim
            (a ↦ [∨].introₗ a)
            (c ↦ [∨].introᵣ([∧].intro b c))
            ([∧].elimᵣ a∨b∧a∨c)
          )
        )
        ([∧].elimₗ a∨b∧a∨c)
      )
    )

    (a∨b∧c ↦
      ([∨].elim
        (a   ↦ [∧].intro([∨].introₗ a)([∨].introₗ a))
        (b∧c ↦ [∧].intro([∨].introᵣ([∧].elimₗ b∧c))([∨].introᵣ([∧].elimᵣ b∧c)))
        (a∨b∧c)
      )
    )
  )

[∨][∧]-distributivityᵣ : ∀{a b c} → Proof(((a ∧ b) ∨ c) ⟷ (a ∨ c)∧(b ∨ c))
[∨][∧]-distributivityᵣ =
  ([↔].intro
    (a∨c∧b∨c ↦
      ([∨].elim
        (a ↦
          ([∨].elim
            (b ↦ [∨].introₗ([∧].intro a b))
            (c ↦ [∨].introᵣ c)
            ([∧].elimᵣ a∨c∧b∨c)
          )
        )
        (c ↦ [∨].introᵣ c)
        ([∧].elimₗ a∨c∧b∨c)
      )
    )

    (a∧b∨c ↦
      ([∨].elim
        (a∧b ↦ [∧].intro([∨].introₗ([∧].elimₗ a∧b))([∨].introₗ([∧].elimᵣ a∧b)))
        (c   ↦ [∧].intro([∨].introᵣ c)([∨].introᵣ c))
        (a∧b∨c)
      )
    )
  )

[∧][∨]-distributivityₗ : ∀{a b c} → Proof((a ∧ (b ∨ c)) ⟷ (a ∧ b)∨(a ∧ c))
[∧][∨]-distributivityₗ =
  ([↔].intro
    (a∧b∨a∧c ↦
      ([∨].elim
        (a∧b ↦ [∧].intro([∧].elimₗ a∧b)([∨].introₗ([∧].elimᵣ a∧b)))
        (a∧c ↦ [∧].intro([∧].elimₗ a∧c)([∨].introᵣ([∧].elimᵣ a∧c)))
        (a∧b∨a∧c)
      )
    )

    (a∧b∨c ↦
      ([∨].elim
        (b ↦ [∨].introₗ([∧].intro([∧].elimₗ a∧b∨c)(b)))
        (c ↦ [∨].introᵣ([∧].intro([∧].elimₗ a∧b∨c)(c)))
        ([∧].elimᵣ a∧b∨c)
      )
    )
  )

[∧][∨]-distributivityᵣ : ∀{a b c} → Proof(((a ∨ b) ∧ c) ⟷ (a ∧ c)∨(b ∧ c))
[∧][∨]-distributivityᵣ =
  ([↔].intro
    (a∧c∨b∧c ↦
      ([∨].elim
        (a∧c ↦ [∧].intro([∨].introₗ([∧].elimₗ a∧c))([∧].elimᵣ a∧c))
        (b∧c ↦ [∧].intro([∨].introᵣ([∧].elimₗ b∧c))([∧].elimᵣ b∧c))
        (a∧c∨b∧c)
      )
    )

    (a∨b∧c ↦
      ([∨].elim
        (a ↦ [∨].introₗ([∧].intro(a)([∧].elimᵣ a∨b∧c)))
        (b ↦ [∨].introᵣ([∧].intro(b)([∧].elimᵣ a∨b∧c)))
        ([∧].elimₗ a∨b∧c)
      )
    )
  )

postulate [≡]-substitute-this-is-almost-trivial : ∀{φ : Domain → Formula}{a b} → Proof(((a ≡ b) ∧ φ(a)) ⟷ φ(b))

postulate [→][∧]-distributivityₗ : ∀{X Y Z} → Proof((X ⟶ (Y ∧ Z)) ⟷ ((X ⟶ Y) ∧ (X ⟶ Z)))

postulate [∀]-unrelatedₗ-[→] : ∀{P : Domain → Formula}{Q : Formula} → Proof(∀ₗ(x ↦ (P(x) ⟶ Q)) ⟷ (∃ₗ(x ↦ P(x)) ⟶ Q))

postulate [∀]-unrelatedᵣ-[→] : ∀{P : Formula}{Q : Domain → Formula} → Proof(∀ₗ(x ↦ (P ⟶ Q(x))) ⟷ (P ⟶ ∀ₗ(x ↦ Q(x))))

postulate [∃]-unrelatedₗ-[→] : ∀{P : Domain → Formula}{Q : Formula} → Proof(∃ₗ(x ↦ (P(x) ⟶ Q)) ⟷ (∀ₗ(x ↦ P(x)) ⟶ Q))

postulate [∃]-unrelatedᵣ-[→] : ∀{P : Formula}{Q : Domain → Formula} → Proof(∃ₗ(x ↦ (P ⟶ Q(x))) ⟷ (P ⟶ ∃ₗ(x ↦ Q(x))))

-- TODO: Is equivalence unprovable? I think so
Unique-unrelatedᵣ-[→]ᵣ : ∀{P : Formula}{Q : Domain → Formula} → Proof(Unique(x ↦ (P ⟶ Q(x))) ⟶ (P ⟶ Unique(x ↦ Q(x))))
Unique-unrelatedᵣ-[→]ᵣ {P}{Q} =
  [→].intro(uniquepq ↦ [→].intro(p ↦ [∀].intro(\{x} → [∀].intro(\{y} → [→].intro(qxqy ↦
    ([→].elim
      ([∀].elim([∀].elim uniquepq{x}){y})
      (([↔].elimᵣ [→][∧]-distributivityₗ) ([→].intro(p ↦ qxqy)))
    )
  )))))
  -- Proving these equivalent:
  -- ∀ₗ(x ↦ ∀ₗ(y ↦ (P ⟶ Q(x)) ∧ (P ⟶ Q(y)) ⟶ (x ≡ y))
  -- P ⟶ ∀ₗ(x ↦ ∀ₗ(y ↦ Q(x) ∧ Q(y) ⟶ (x ≡ y))
    -- test : Proof(∀ₗ(x ↦ ∀ₗ(y ↦ (P ⟶ Q(x)) ∧ (P ⟶ Q(y)) ⟶ (x ≡ y))) ⟷ ∀ₗ(x ↦ ∀ₗ(y ↦ (P ⟶ Q(x) ∧ Q(y)) ⟶ (x ≡ y))))
    -- test = ([↔]-with-[∀] ([↔]-with-[∀] ([→][∧]-distributivityₗ)))

-- TODO: Is left provable? Above left seems unprovable
[∃!]-unrelatedᵣ-[→]ᵣ : ∀{P : Formula}{Q : Domain → Formula} → Proof(∃ₗ!(x ↦ (P ⟶ Q(x))) ⟶ (P ⟶ ∃ₗ!(x ↦ Q(x))))
[∃!]-unrelatedᵣ-[→]ᵣ {P}{Q} =
  ([→].intro(proof ↦
    ([↔].elimₗ [→][∧]-distributivityₗ)
    ([∧].intro
      (([↔].elimᵣ [∃]-unrelatedᵣ-[→])    ([∧].elimₗ proof))
      (([→].elim Unique-unrelatedᵣ-[→]ᵣ) ([∧].elimᵣ proof))
    )
  ))

-- TODO: I think this is similar to the skolemization process of going from ∀∃ to ∃function∀
[∃]-fn-witness : ∀{P : Domain → Domain → Formula} → ⦃ _ : Proof(∀ₗ(x ↦ ∃ₗ(y ↦ P(x)(y)))) ⦄ → Domain → Domain
[∃]-fn-witness{P} ⦃ proof ⦄ (x) = [∃]-witness ⦃ [∀].elim(proof){x} ⦄

[∃]-fn-proof : ∀{P : Domain → Domain → Formula} → ⦃ p : Proof(∀ₗ(x ↦ ∃ₗ(y ↦ P(x)(y)))) ⦄ → Proof(∀ₗ(x ↦ P(x)([∃]-fn-witness{P} ⦃ p ⦄ (x))))
[∃]-fn-proof{P} ⦃ proof ⦄ =
  ([∀].intro(\{x} →
    [∃]-proof {P(x)} ⦃ [∀].elim proof{x} ⦄
  ))

[∃!]-fn-witness : ∀{P : Domain → Domain → Formula} → ⦃ _ : Proof(∀ₗ(x ↦ ∃ₗ!(y ↦ P(x)(y)))) ⦄ → Domain → Domain
[∃!]-fn-witness{P} ⦃ proof ⦄ (x) = [∃!]-witness ⦃ [∀].elim(proof){x} ⦄

{-
[∃!]-fn-proof : ∀{P : Domain → Domain → Formula} → ⦃ p : Proof(∀ₗ(x ↦ ∃ₗ!(y ↦ P(x)(y)))) ⦄ → Proof(∀ₗ(x ↦ P(x)([∃!]-fn-witness{P} ⦃ p ⦄ (x))))
[∃!]-fn-proof{P} ⦃ proof ⦄ =
  ([∀].intro(\{x} →
    [∃!]-proof {P(x)} ⦃ [∀].elim proof{x} ⦄
  ))
-}

[∃!]-fn-proof : ∀{P : Domain → Domain → Formula} → ⦃ p : Proof(∀ₗ(x ↦ ∃ₗ!(y ↦ P(x)(y)))) ⦄ → ∀{x} → Proof(P(x)([∃!]-fn-witness{P} ⦃ p ⦄ (x)))
[∃!]-fn-proof{P} ⦃ proof ⦄ {x} =
  [∃!]-proof {P(x)} ⦃ [∀].elim proof{x} ⦄

postulate [∃!]-fn-unique : ∀{P : Domain → Domain → Formula} → ⦃ p : Proof(∀ₗ(x ↦ ∃ₗ!(y ↦ P(x)(y)))) ⦄ → ∀{x} → Proof(∀ₗ(y ↦ P(x)(y) ⟶ (y ≡ [∃!]-fn-witness{P} ⦃ p ⦄ (x))))

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:
{-# OPTIONS --without-K #-}

-- Note that this is properly named, but it does depend on our version of
-- Equiv and TypeEquiv for a number of things.

module Data.SumProd.Properties where

open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming (map to map⊎)
open import Data.Product using (_×_; _,_) renaming (map to map×)

import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Function using (id; _∘_)

open import Equiv using (_∼_; sym∼)
open import TypeEquiv
  using (unite₊; uniti₊; swap₊; assocl₊; assocr₊;
         unite⋆; uniti⋆; unite⋆′; uniti⋆′; swap⋆; assocl⋆; assocr⋆;
         distz; distzr; factorz; factorzr;
         dist; factor; distl; factorl)

infixr 1 _⊎→_
infixr 4 _×→_

_⊎→_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
      (A → C) → (B → D) → (A ⊎ B → C ⊎ D)
_⊎→_ = map⊎

_×→_ : ∀ {a b p q}
        {A : Set a} {B : Set b} {P : Set p} {Q : Set q} →
      (A → B) → (P → Q) → (A × P) → (B × Q)
f ×→ g = λ { (x , y) → (f x , g y) }

------------------------------------------------------------------------------
-- Note that all these lemmas are "simple" in the sense that they
-- are all about map⊎ rather than [_,_]

distl-coh : {A B C D E F : Set} →
  {f : A → D} {g : B → E} {h : C → F} →
  distl ∘ (f ×→ (g ⊎→ h)) ∼ ((f ×→ g) ⊎→ (f ×→ h)) ∘ distl
distl-coh (a , inj₁ x) = P.refl
distl-coh (a , inj₂ y) = P.refl

factorl-coh : {A B C D E F : Set} →
  {f : A → D} {g : B → E} {h : C → F} →
  (f ×→ (g ⊎→ h)) ∘ factorl ∼ factorl ∘ ((f ×→ g) ⊎→ (f ×→ h))
factorl-coh (inj₁ (a , b)) = P.refl
factorl-coh (inj₂ (a , c)) = P.refl

dist-coh : {A B C D E F : Set} →
  {f : A → D} {g : B → E} {h : C → F} →
  dist ∘ ((f ⊎→ g) ×→ h) ∼ ((f ×→ h) ⊎→ (g ×→ h)) ∘ dist
dist-coh (inj₁ x , c) = P.refl
dist-coh (inj₂ y , c) = P.refl

factor-coh : {A B C D E F : Set} →
  {f : A → D} {g : B → E} {h : C → F} →
  ((f ⊎→ g) ×→ h) ∘ factor ∼ factor ∘ ((f ×→ h) ⊎→ (g ×→ h))
factor-coh (inj₁ x) = P.refl
factor-coh (inj₂ y) = P.refl

-- note how this is true without relying on ⊥ as input
distzr-coh : {A B : Set} → {f : A → B} → {g : ⊥ → ⊥} →
  distzr ∘ (f ×→ g) ∼ g ∘ distzr
distzr-coh _ = P.refl

-- but this is only true because of ⊥
factorzr-coh : {A B : Set} → {f : B → A} → {g : ⊥ → ⊥} →
  (f ×→ g) ∘ factorzr ∼ factorzr ∘ g
factorzr-coh ()

-- note how this is true without relying on ⊥ as input
distz-coh : {A B : Set} → {f : A → B} → {g : ⊥ → ⊥} →
  distz ∘ (g ×→ f) ∼ g ∘ distz
distz-coh _ = P.refl

-- but this is only true because of ⊥
factorz-coh : {A B : Set} → {f : B → A} → {g : ⊥ → ⊥} →
  (g ×→ f) ∘ factorz ∼ factorz ∘ g
factorz-coh ()

---------------------------------------------------------------
-- various coherence lemmas

-- These will be named for the action they perform on the
-- underlying type, rather than for the program they
-- represent.
A×[B⊎C]→[A×C]⊎[A×B] : {A B C : Set} →
  distl ∘ (id {A = A} ×→ swap₊ {B} {C}) ∼ swap₊ ∘ distl
A×[B⊎C]→[A×C]⊎[A×B] (x , inj₁ y) = P.refl
A×[B⊎C]→[A×C]⊎[A×B] (x , inj₂ y) = P.refl

[A×C]⊎[A×B]→A×[B⊎C] : {A B C : Set} →
  (id ×→ swap₊) ∘ factorl ∼ factorl ∘ swap₊ {A × C} {A × B}
[A×C]⊎[A×B]→A×[B⊎C] (inj₁ x) = P.refl
[A×C]⊎[A×B]→A×[B⊎C] (inj₂ y) = P.refl

[A⊎B]×C→[C×A]⊎[C×B] : {A B C : Set} →
  (swap⋆ ⊎→ swap⋆) ∘ dist ∼ distl ∘ swap⋆ {A ⊎ B} {C}
[A⊎B]×C→[C×A]⊎[C×B] (inj₁ x , z) = P.refl
[A⊎B]×C→[C×A]⊎[C×B] (inj₂ y , z) = P.refl

[C×A]⊎[C×B]→[A⊎B]×C : {A B C : Set} →
  factor ∘ (swap⋆ {C} {A} ⊎→ swap⋆ {C} {B}) ∼ swap⋆ ∘ factorl
[C×A]⊎[C×B]→[A⊎B]×C (inj₁ x) = P.refl
[C×A]⊎[C×B]→[A⊎B]×C (inj₂ y) = P.refl

-- × binds tighter than ⊎ (in the name)
[A⊎B⊎C]×D→[A×D⊎B×D]⊎C×D : {A B C D : Set} →
  (dist ⊎→ id) ∘ dist ∘ (assocl₊ {A} {B} {C} ×→ id {A = D}) ∼
  assocl₊ ∘ (id ⊎→ dist) ∘ dist
[A⊎B⊎C]×D→[A×D⊎B×D]⊎C×D (inj₁ x , d) = P.refl
[A⊎B⊎C]×D→[A×D⊎B×D]⊎C×D (inj₂ (inj₁ x) , d) = P.refl
[A⊎B⊎C]×D→[A×D⊎B×D]⊎C×D (inj₂ (inj₂ y) , d) = P.refl

[A×D⊎B×D]⊎C×D→[A⊎B⊎C]×D : {A B C D : Set} →
  (assocr₊ ×→ id) ∘ factor ∘ (factor {A} {B} {D} ⊎→ id {A = C × D}) ∼
  factor ∘ (id ⊎→ factor) ∘ assocr₊
[A×D⊎B×D]⊎C×D→[A⊎B⊎C]×D (inj₁ (inj₁ x)) = P.refl
[A×D⊎B×D]⊎C×D→[A⊎B⊎C]×D (inj₁ (inj₂ y)) = P.refl
[A×D⊎B×D]⊎C×D→[A⊎B⊎C]×D (inj₂ y) = P.refl

A×B×[C⊎D]→[A×B]×C⊎[A×B]×D : {A B C D : Set} →
  distl ∘ assocl⋆ {A} {B} {C ⊎ D} ∼ (assocl⋆ ⊎→ assocl⋆) ∘ distl ∘ (id ×→ distl)
A×B×[C⊎D]→[A×B]×C⊎[A×B]×D (a , b , inj₁ x) = P.refl
A×B×[C⊎D]→[A×B]×C⊎[A×B]×D (a , b , inj₂ y) = P.refl

[A×B]×C⊎[A×B]×D→A×B×[C⊎D] : {A B C D : Set} →
  assocr⋆ ∘ factorl {A × B} {C} {D} ∼ (id ×→ factorl) ∘ factorl ∘ (assocr⋆ ⊎→ assocr⋆)
[A×B]×C⊎[A×B]×D→A×B×[C⊎D] (inj₁ x) = P.refl
[A×B]×C⊎[A×B]×D→A×B×[C⊎D] (inj₂ y) = P.refl

-- in theory, this actually says that all ⊥ are equal!
-- the annotations can be inferred, but this makes it
-- clearer still
0×0→0 : distz {⊥} ∼ distzr {⊥}
0×0→0 (() , ())

0→0×0 : factorz {⊥} ∼ factorzr {⊥}
0→0×0 ()

0×[A⊎B]→0 : {A B : Set} →
  distz ∼ unite₊ ∘ (distz ⊎→ distz) ∘ distl {⊥} {A} {B}
0×[A⊎B]→0 (() , inj₁ _)
0×[A⊎B]→0 (_  , inj₂ _) = P.refl

0→0×[A⊎B] : {A B : Set} →
  factorz ∼ factorl {B = A} {B} ∘ (factorz ⊎→ factorz) ∘ uniti₊
0→0×[A⊎B] ()

0×1→0 : unite⋆′ {⊥} ∼ distz {⊤}
0×1→0 _ = P.refl

0→0×1 : uniti⋆′ {⊥} ∼ factorz {⊤}
0→0×1 ()

A×0→0 : {A : Set} → distzr {A} ∼ distz ∘ swap⋆
A×0→0 _ = P.refl

0→A×0 : {A : Set} → factorzr {A} ∼ swap⋆ ∘ factorz
0→A×0 ()

0×A×B→0 : {A B : Set} →
  distz ∼ distz ∘ (distz ×→ id) ∘ assocl⋆ {⊥} {A} {B}
0×A×B→0 _ = P.refl

0→0×A×B : {A B : Set} →
  factorz ∼ assocr⋆ {B = A} {B} ∘ (factorz ×→ id) ∘ factorz
0→0×A×B ()

A×0×B→0 : {A B : Set} →
  distzr ∘ (id ×→ distz) ∼ distz ∘ (distzr ×→ id) ∘ assocl⋆ {A} {⊥} {B}
A×0×B→0 _ = P.refl

0→A×0×B : {A B : Set} →
  (id ×→ factorz {B}) ∘ factorzr {A} ∼ assocr⋆ ∘ (factorzr ×→ id) ∘ factorz
0→A×0×B ()

A×[0+B]→A×B : {A B : Set} →
  (id {A = A} ×→ unite₊ {B}) ∼ unite₊ ∘ (distzr ⊎→ id) ∘ distl
A×[0+B]→A×B (_ , inj₁ ())
A×[0+B]→A×B (_ , inj₂ _) = P.refl

A×B→A×[0+B] : {A B : Set} →
  (id ×→ uniti₊) ∼ factorl ∘ (factorzr ⊎→ id) ∘ uniti₊ {A × B}
A×B→A×[0+B] (_ , _) = P.refl

1×[A⊎B]→A⊎B : {A B : Set} →
  unite⋆ ∼ (unite⋆ ⊎→ unite⋆) ∘ distl {⊤} {A} {B}
1×[A⊎B]→A⊎B (tt , inj₁ x) = P.refl
1×[A⊎B]→A⊎B (tt , inj₂ y) = P.refl

A⊎B→1×[A⊎B] : {A B : Set} →
  uniti⋆ ∼ factorl ∘ (uniti⋆ {A} ⊎→ uniti⋆ {B})
A⊎B→1×[A⊎B] (inj₁ x) = P.refl
A⊎B→1×[A⊎B] (inj₂ y) = P.refl

[A⊎B]×[C⊎D]→[[A×C⊎B×C]⊎A×D]⊎B×D : {A B C D : Set} →
  assocl₊ ∘ (dist ⊎→ dist) ∘ distl ∼
  (assocl₊ ⊎→ id) ∘ ((id ⊎→ swap₊) ⊎→ id) ∘
     (assocr₊ ⊎→ id) ∘ assocl₊ ∘ (distl ⊎→ distl) ∘ dist {A} {B} {C ⊎ D}
[A⊎B]×[C⊎D]→[[A×C⊎B×C]⊎A×D]⊎B×D (inj₁ x , inj₁ x₁) = P.refl
[A⊎B]×[C⊎D]→[[A×C⊎B×C]⊎A×D]⊎B×D (inj₁ x , inj₂ y) = P.refl
[A⊎B]×[C⊎D]→[[A×C⊎B×C]⊎A×D]⊎B×D (inj₂ y , inj₁ x) = P.refl
[A⊎B]×[C⊎D]→[[A×C⊎B×C]⊎A×D]⊎B×D (inj₂ y , inj₂ y₁) = P.refl

[[A×C⊎B×C]⊎A×D]⊎B×D→[A⊎B]×[C⊎D] : {A B C D : Set} →
  factorl ∘ (factor ⊎→ factor) ∘ assocr₊ ∼
  factor ∘ (factorl ⊎→ factorl) ∘ assocr₊ ∘(assocl₊ ⊎→ id) ∘
      ((id ⊎→ swap₊) ⊎→ id) ∘ (assocr₊ {A × C} ⊎→ id {A = B × D})
[[A×C⊎B×C]⊎A×D]⊎B×D→[A⊎B]×[C⊎D] (inj₁ (inj₁ (inj₁ (a , c)))) = P.refl
[[A×C⊎B×C]⊎A×D]⊎B×D→[A⊎B]×[C⊎D] (inj₁ (inj₁ (inj₂ (b , c)))) = P.refl
[[A×C⊎B×C]⊎A×D]⊎B×D→[A⊎B]×[C⊎D] (inj₁ (inj₂ (a , d))) = P.refl
[[A×C⊎B×C]⊎A×D]⊎B×D→[A⊎B]×[C⊎D] (inj₂ (b , d)) = P.refl

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

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

open Category C
open Equiv

open import Function using (flip)
open import Level
open import Function using (flip)
open import Categories.Support.PropositionalEquality

open import Categories.Square
open GlueSquares C

-- Borrowed from Dan Doel's definition of products
record Product (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where

  infix 10 ⟨_,_⟩

  field
    A×B : Obj
    π₁ : A×B ⇒ A
    π₂ : A×B ⇒ B
    ⟨_,_⟩ : ∀ {C} → (C ⇒ A) → (C ⇒ B) → (C ⇒ A×B)

    .commute₁ : ∀ {C} {f : C ⇒ A} {g : C ⇒ B} → π₁ ∘ ⟨ f , g ⟩ ≡ f
    .commute₂ : ∀ {C} {f : C ⇒ A} {g : C ⇒ B} → π₂ ∘ ⟨ f , g ⟩ ≡ g
    .universal : ∀ {C} {f : C ⇒ A} {g : C ⇒ B} {i : C ⇒ A×B}
               → π₁ ∘ i ≡ f → π₂ ∘ i ≡ g → ⟨ f , g ⟩ ≡ i

  .g-η : ∀ {C} {f : C ⇒ A×B} → ⟨ π₁ ∘ f , π₂ ∘ f ⟩ ≡ f
  g-η = universal refl refl

  .η : ⟨ π₁ , π₂ ⟩ ≡ id
  η = universal identityʳ identityʳ

  .⟨⟩-cong₂ : ∀ {C} → {f f′ : C ⇒ A} {g g′ : C ⇒ B} → f ≡ f′ → g ≡ g′ → ⟨ f , g ⟩ ≡ ⟨ f′ , g′ ⟩
  ⟨⟩-cong₂ f≡f′ g≡g′ =
    universal (trans commute₁ (sym f≡f′)) (trans commute₂ (sym g≡g′))

  .⟨⟩∘ : ∀ {C D} {f : C ⇒ A} {g : C ⇒ B} {q : D ⇒ C} → ⟨ f , g ⟩ ∘ q ≡ ⟨ f ∘ q , g ∘ q ⟩
  ⟨⟩∘ = sym (universal (pullˡ commute₁) (pullˡ commute₂))

import Categories.Morphisms
open Categories.Morphisms C

private
  module Lemmas {A B : Obj} where
    open Product {A} {B} renaming (⟨_,_⟩ to _⟨_,_⟩)

    repack : (p₁ p₂ : Product A B) → A×B p₁ ⇒ A×B p₂
    repack p₁ p₂ = p₂ ⟨ π₁ p₁ , π₂ p₁ ⟩

    .repack∘ : (p₁ p₂ p₃ : Product A B) → repack p₂ p₃ ∘ repack p₁ p₂ ≡ repack p₁ p₃
    repack∘ p₁ p₂ p₃ = sym (universal p₃
      (glueTrianglesʳ (commute₁ p₃) (commute₁ p₂))
      (glueTrianglesʳ (commute₂ p₃) (commute₂ p₂)))

    .repack≡id : (p : Product A B) → repack p p ≡ id
    repack≡id p = η p

    .repack-cancel : (p₁ p₂ : Product A B) → repack p₁ p₂ ∘ repack p₂ p₁ ≡ id
    repack-cancel p₁ p₂ = trans (repack∘ p₂ p₁ p₂) (repack≡id p₂)

up-to-iso : ∀ {A B} → (p₁ p₂ : Product A B) → Product.A×B p₁ ≅ Product.A×B p₂
up-to-iso p₁ p₂ = record
  { f = repack p₁ p₂
  ; g = repack p₂ p₁
  ; iso = record
    { isoˡ = repack-cancel p₂ p₁
    ; isoʳ = repack-cancel p₁ p₂
    }
  }
  where
  open Lemmas

transport-by-iso : ∀ {A B} → (p : Product A B) → ∀ {X} → Product.A×B p ≅ X → Product A B
transport-by-iso p {X} p≅X = record
  { A×B = X
  ; π₁ = p.π₁ ∘ g
  ; π₂ = p.π₂ ∘ g
  ; ⟨_,_⟩ = λ h₁ h₂ → f ∘ p ⟨ h₁ , h₂ ⟩
  ; commute₁ = trans (cancelInner isoˡ) p.commute₁
  ; commute₂ = trans (cancelInner isoˡ) p.commute₂
  ; universal = λ {_ l r i} pfˡ pfʳ → let open HomReasoning in
      begin
        f ∘ p ⟨ l , r ⟩
      ↑⟨ ∘-resp-≡ʳ (p.⟨⟩-cong₂ pfˡ pfʳ) ⟩
        f ∘ p ⟨ (p.π₁ ∘ g) ∘ i , (p.π₂ ∘ g) ∘ i ⟩
      ↓⟨ ∘-resp-≡ʳ (p.universal (sym assoc) (sym assoc)) ⟩
        f ∘ (g ∘ i)
      ↓⟨ cancelLeft isoʳ ⟩
        i
      ∎
  }
  where
  module p = Product p
  open Product using () renaming (⟨_,_⟩ to _⟨_,_⟩)
  open _≅_ p≅X

Reversible : ∀ {A B} → (p : Product A B) → Product B A
Reversible p = record
  { A×B = p.A×B
  ; π₁ = p.π₂
  ; π₂ = p.π₁
  ; ⟨_,_⟩ = flip p.⟨_,_⟩
  ; commute₁ = p.commute₂
  ; commute₂ = p.commute₁
  ; universal = flip p.universal
  }
  where module p = Product p

Commutative : ∀ {A B} (p₁ : Product A B) (p₂ : Product B A) → Product.A×B p₁ ≅ Product.A×B p₂
Commutative p₁ p₂ = up-to-iso p₁ (Reversible p₂)

Associable : ∀ {X Y Z} (p₁ : Product X Y) (p₂ : Product Y Z) (p₃ : Product X (Product.A×B p₂)) → Product (Product.A×B p₁) Z
Associable p₁ p₂ p₃ = record
  { A×B = A×B p₃
  ; π₁ = p₁ ⟨ π₁ p₃ , π₁ p₂ ∘ π₂ p₃ ⟩
  ; π₂ = π₂ p₂ ∘ π₂ p₃
  ; ⟨_,_⟩ = λ f g → p₃ ⟨ π₁ p₁ ∘ f , p₂ ⟨ π₂ p₁ ∘ f , g ⟩ ⟩
  ; commute₁ = λ {_ f g} → let open HomReasoning in begin
      p₁ ⟨ π₁ p₃ , π₁ p₂ ∘ π₂ p₃ ⟩ ∘ p₃ ⟨ π₁ p₁ ∘ f , p₂ ⟨ π₂ p₁ ∘ f , g ⟩ ⟩
    ↓⟨ ⟨⟩∘ p₁ ⟩
      p₁ ⟨ π₁ p₃ ∘ p₃ ⟨ π₁ p₁ ∘ f , _ ⟩ , (π₁ p₂ ∘ π₂ p₃) ∘ p₃ ⟨ _ , p₂ ⟨ π₂ p₁ ∘ f , g ⟩ ⟩ ⟩
    ↓⟨ ⟨⟩-cong₂ p₁ (commute₁ p₃) (glueTrianglesˡ (commute₁ p₂) (commute₂ p₃)) ⟩
      p₁ ⟨ π₁ p₁ ∘ f , π₂ p₁ ∘ f ⟩
    ↓⟨ g-η p₁ ⟩
      f
    ∎
  ; commute₂ = λ {_ f g} → glueTrianglesˡ (commute₂ p₂) (commute₂ p₃)
  ; universal = λ {D l r i} pfˡ pfʳ → let open HomReasoning in begin
      p₃ ⟨ π₁ p₁ ∘ l , p₂ ⟨ π₂ p₁ ∘ l , r ⟩ ⟩
    ↑⟨ ⟨⟩-cong₂ p₃ (∘-resp-≡ʳ pfˡ) (⟨⟩-cong₂ p₂ (∘-resp-≡ʳ pfˡ) pfʳ) ⟩
      p₃ ⟨ π₁ p₁ ∘ (p₁ ⟨ π₁ p₃ , _ ⟩ ∘ i) , p₂ ⟨ π₂ p₁ ∘ (p₁ ⟨ _ , π₁ p₂ ∘ π₂ p₃ ⟩ ∘ i) , (π₂ p₂ ∘ π₂ p₃) ∘ i ⟩ ⟩
    ↓⟨ ⟨⟩-cong₂ p₃ (pullˡ (commute₁ p₁)) (⟨⟩-cong₂ p₂ (pullˡ (commute₂ p₁)) refl) ⟩
      p₃ ⟨ π₁ p₃ ∘ i , p₂ ⟨ (π₁ p₂ ∘ π₂ p₃) ∘ i , (π₂ p₂ ∘ π₂ p₃) ∘ i ⟩ ⟩
    ↓⟨ ⟨⟩-cong₂ p₃ refl (universal p₂ (sym assoc) (sym assoc)) ⟩
      p₃ ⟨ π₁ p₃ ∘ i , π₂ p₃ ∘ i ⟩
    ↓⟨ g-η p₃ ⟩
      i
    ∎
  }
  where
  open Product renaming (⟨_,_⟩ to _⟨_,_⟩)

Associative : ∀ {X Y Z} (p₁ : Product X Y) (p₂ : Product Y Z) (p₃ : Product X (Product.A×B p₂)) (p₄ : Product (Product.A×B p₁) Z) → (Product.A×B p₃) ≅ (Product.A×B p₄)
Associative p₁ p₂ p₃ p₄ = up-to-iso (Associable p₁ p₂ p₃) p₄

open Lemmas public

Mobile : ∀ {A₁ B₁ A₂ B₂} (p : Product A₁ B₁) → A₁ ≅ A₂ → B₁ ≅ B₂ → Product A₂ B₂
Mobile p A₁≅A₂ B₁≅B₂ = record
  { A×B = p.A×B
  ; π₁ = f A₁≅A₂ ∘ p.π₁
  ; π₂ = f B₁≅B₂ ∘ p.π₂
  ; ⟨_,_⟩ = λ h k → p ⟨ g A₁≅A₂ ∘ h , g B₁≅B₂ ∘ k ⟩
  ; commute₁ = let open HomReasoning in begin
      (f A₁≅A₂ ∘ p.π₁) ∘ p ⟨ g A₁≅A₂ ∘ _ , g B₁≅B₂ ∘ _ ⟩
    ↓⟨ pullʳ p.commute₁ ⟩
      f A₁≅A₂ ∘ (g A₁≅A₂ ∘ _)
    ↓⟨ cancelLeft (isoʳ A₁≅A₂) ⟩
      _
    ∎
  ; commute₂ = let open HomReasoning in begin
      (f B₁≅B₂ ∘ p.π₂) ∘ p ⟨ g A₁≅A₂ ∘ _ , g B₁≅B₂ ∘ _ ⟩
    ↓⟨ pullʳ p.commute₂ ⟩
      f B₁≅B₂ ∘ (g B₁≅B₂ ∘ _)
    ↓⟨ cancelLeft (isoʳ B₁≅B₂) ⟩
      _
    ∎
  ; universal = λ pfˡ pfʳ → p.universal
                              (switch-fgˡ A₁≅A₂ (trans (sym assoc) pfˡ))
                              (switch-fgˡ B₁≅B₂ (trans (sym assoc) pfʳ))
  }
  where
  module p = Product p
  open Product renaming (⟨_,_⟩ to _⟨_,_⟩)
  open _≅_

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Issue280 where

data PreModel (C : Set) (M : C → Set) : Set → Set where
  model : (c : C) → PreModel C M (M c)

reflect : (C : Set)(M : C → Set) → PreModel C M C → C
reflect .(M c) M (model c) = c


text:
module Div where

data True : Set where
  trivial : True

data False : Set where

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

NonZero : Nat -> Set
NonZero  zero   = False
NonZero (suc _) = True

divHelp : Nat -> Nat -> Nat -> Nat
divHelp  zero    zero   c = suc zero
divHelp  zero   (suc y) c = zero
divHelp (suc x)  zero   c = suc (divHelp x c c)
divHelp (suc x) (suc y) c = divHelp x y c

div : (x y : Nat) -> NonZero y -> Nat
div  x       zero  ()
div  zero   (suc y) _ = zero
div (suc x) (suc y) _ = divHelp (suc x) (suc y) y

n1 = suc zero
n2 = suc n1
n3 = suc n2
n4 = suc n3
n5 = suc n4
n6 = suc n5
n7 = suc n6
n8 = suc n7
n9 = suc n8
n10 = suc n9
n11 = suc n10
n12 = suc n11


text:
{-# OPTIONS -v treeless.opt.final:20 -v 0 #-}
module Word where

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Word renaming (primWord64ToNat to toNat)
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.IO
open import Agda.Builtin.FromNat
open import Agda.Builtin.String
open import Agda.Builtin.Strict

instance
  NumWord : Number Word64
  Number.Constraint NumWord _ = ⊤
  fromNat {{NumWord}} n = primWord64FromNat n

  NumNat : Number Nat
  Number.Constraint NumNat _ = ⊤
  fromNat {{NumNat}} n = n

natOp : (Nat → Nat → Nat) → Word64 → Word64 → Word64
natOp f a b = fromNat (f (toNat a) (toNat b))
{-# INLINE natOp #-}

_^_ : Nat → Nat → Nat
a ^ zero = 1
a ^ suc n = a * a ^ n

2⁶⁴ : Nat
2⁶⁴ = 2 ^ 64
{-# STATIC 2⁶⁴ #-}

addWord : Word64 → Word64 → Word64
addWord = natOp _+_

subWord : Word64 → Word64 → Word64
subWord = natOp λ a b → a + 2⁶⁴ - b

mulWord : Word64 → Word64 → Word64
mulWord = natOp _*_

{-# INLINE addWord #-}
{-# INLINE subWord #-}
{-# INLINE mulWord #-}

-- div/mod

data ⊥ : Set where

NonZero : Nat → Set
NonZero zero    = ⊥
NonZero (suc _) = ⊤

div : (a b : Nat) {{nz : NonZero b}} → Nat
div a 0 {{}}
div a (suc b) = div-helper 0 b a b

mod : (a b : Nat) {{nz : NonZero b}} → Nat
mod a 0 {{}}
mod a (suc b) = mod-helper 0 b a b

{-# INLINE div #-}
{-# INLINE mod #-}

NonZeroWord : Word64 → Set
NonZeroWord a = NonZero (toNat a)

divWord : (a b : Word64) {{nz : NonZeroWord b}} → Word64
divWord a b = fromNat (div (toNat a) (toNat b))

modWord : (a b : Word64) {{nz : NonZeroWord b}} → Word64
modWord a b = fromNat (mod (toNat a) (toNat b))

{-# INLINE divWord #-}
{-# INLINE modWord #-}

-- Comparison --

eqWord : Word64 → Word64 → Bool
eqWord a b = toNat a == toNat b

ltWord : Word64 → Word64 → Bool
ltWord a b = toNat a < toNat b

{-# INLINE eqWord #-}
{-# INLINE ltWord #-}

postulate
  showWord : Word64 → String
  putStrLn : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC showWord = Data.Text.pack . show #-}
{-# COMPILE GHC putStrLn = Data.Text.IO.putStrLn #-}

{-# COMPILE JS showWord = function(x) { return x.toString(); } #-}
{-# COMPILE JS putStrLn = function (x) { return function(cb) { process.stdout.write(x + "\n"); cb(0); }; } #-}

2^63 : Word64
2^63 = addWord 1 (divWord (subWord 0 1) 2)

test : Word64
test = addWord (addWord 2^63 100)
               (addWord 2^63 1)

prf : test ≡ 101
prf = refl

prf' : eqWord test 101 ≡ true
prf' = refl

main : IO ⊤
main = putStrLn (showWord test)

-- Some checks for treeless optimisations

ltDouble : Word64 → Word64 → Bool
ltDouble x y = ltWord (mulWord 2 x) y

lt4x : Word64 → Word64 → Bool
lt4x x y = primForce (mulWord 2 x) ltDouble y


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

module Data.Sigma.Base where

open import Agda.Builtin.Sigma
  using (Σ; _,_; fst; snd)
  public
open import Level
open import Path

∃ : ∀ {a b} {A : Type a} (B : A → Type b) → Type (a ℓ⊔ b)
∃ {A = A} = Σ A

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

infixr 4.5 _×_
_×_ : (A : Type a) → (B : Type b) → Type (a ℓ⊔ b)
A × B = Σ A λ _ → B

curry : ∀ {A : Type a} {B : A → Type b} {C : Σ A B → Type c} →
          ((p : Σ A B) → C p) →
          ((x : A) → (y : B x) → C (x , y))
curry f x y = f (x , y)

uncurry : ∀ {A : Type a} {B : A → Type b} {C : Σ A B → Type c} →
            ((x : A) → (y : B x) → C (x , y)) →
            ((p : Σ A B) → C p)
uncurry f (x , y) = f x y

map-Σ : ∀ {p q} {P : A → Set p} {Q : B → Set q} →
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ A P → Σ B Q
map-Σ f g (x , y) = (f x , g y)

map₁ : (A → B) → A × C → B × C
map₁ f = map-Σ f (λ x → x)

map₁-Σ : ∀ {A : Set a} {B : Set b} {C : B → Set b}
       → (f : A → B) → Σ A (λ x → C (f x)) → Σ B C
map₁-Σ f (x , y) = f x , y

map₂ : ∀ {A : Set a} {B : A → Set b} {C : A → Set c} →
        (∀ {x} → B x → C x) → Σ A B → Σ A C
map₂ f = map-Σ (λ x → x) f

∃! : ∀ {a b} {A : Type a} → (A → Type b) → Type (a ℓ⊔ b)
∃! B = ∃ λ x → B x × (∀ {y} → B y → x ≡ y)

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

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

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

module Data.Unit.UniversePolymorphic where

open import Level

record ⊤ {ℓ} : Type ℓ where instance constructor tt


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.EquivCarac.Polyn-nPoly where

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

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.CommRing.Instances.UnivariatePoly
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly

open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.Poly0-A
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.Poly1-1Poly
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.An[Am[X]]-Anm[X]
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.AB-An[X]Bn[X]

open CommRingEquivs renaming (compCommRingEquiv to _∘-ecr_ ; invCommRingEquiv to inv-ecr)

private variable
  ℓ : Level

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

Equiv-Polyn-nPoly : (A' : CommRing ℓ) → (n : ℕ) → CommRingEquiv (PolyCommRing A' n) (nUnivariatePoly A' n)
Equiv-Polyn-nPoly A' zero = CRE-Poly0-A A'
Equiv-Polyn-nPoly A' (suc n) = inv-ecr _ _ (CRE-PolyN∘M-PolyN+M A' 1 n)
                               ∘-ecr (lift-equiv-poly _ _ (Equiv-Polyn-nPoly A' n) 1
                               ∘-ecr CRE-Poly1-Poly: (nUnivariatePoly A' n))

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical