text:
module Min where

open import Data.Nat using (ℕ; zero; suc)
open import Algebra.Bundles using (CommutativeRing)
open import Algebra.Module.Bundles using (Module)
open import Data.Product using (Σ-syntax; ∃-syntax; _×_; proj₁; proj₂; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.Core using (Rel)
import Algebra.Module.Construct.Zero as Zero
import Algebra.Module.Construct.DirectProduct as Prod
import Algebra.Module.Construct.TensorUnit as Unit

module _
  {r ℓr} {CR : CommutativeRing r ℓr}
  {ma ℓma} (MA : Module CR ma ℓma)
  {mb ℓmb} (MB : Module CR mb ℓmb)
  where

  open import Linear MA MB

  module _
    {rel} (_<_ : Rel (CommutativeRing.Carrier CR) rel)
    (∥_∥ᴬ : A → R)
    (∥_∥ᴮ : B → R)
    (_÷_ : B → R → B)
    where

    _LimitOf_x→_ Limit-syntax : (L : B) (f : A → B) (c : A)→ Set _
    L LimitOf f x→ c = ∀ ε → ∃[ δ ] ∥ (f (c +ᴬ δ) -ᴮ L) ∥ᴮ < ∥ ε ∥ᴮ
    Limit-syntax = _LimitOf_x→_

    syntax Limit-syntax L (λ h → f) c = L LimitOf f ∶ h ⟶ c

    Diff' : (f : A → B) (x : A) (f' : A → A → B) → Set _
    Diff' f x f' = 0ᴮ LimitOf tmp dx ∶ dx ⟶ 0ᴬ
      where
        tmp : (dx : A) → B
        tmp dx = (f (x +ᴬ dx) -ᴮ f x -ᴮ f' x dx) ÷ ∥ dx ∥ᴬ

    Differentiable : (f : A → B) → A → Set _
    Differentiable f x =
      Σ[ f' ∈ (A → A → B) ]
          Linear (f' x)
        -- × ∀ dy → ∃[ dx ] (∥ ((f (x +ᴬ dx) -ᴮ f x) -ᴮ (f' x dx)) ∥ᴮ) < (∥ dy ∥ᴮ)

    D : {f : A → B} {x : A} (d : Differentiable f x) → A → B
    D {x = x} d = proj₁ d x

n-module : ∀ {a b} {S : CommutativeRing a b} → ℕ → Module S a b
n-module zero = Zero.⟨module⟩
n-module (suc n) = Prod.⟨module⟩ Unit.⟨module⟩ (n-module n)

open import Tactic.RingSolver

module Line {a b} (CR : CommutativeRing a b) where
  open CommutativeRing CR
  open import Relation.Binary.Reasoning.Setoid setoid

  open import Tactic.RingSolver.Core.AlmostCommutativeRing

  line : Carrier → Carrier → Carrier → Carrier
  line m b x = m * x + b

  x+y-x≈y : ∀ x y → (x + y) - x ≈ y
  x+y-x≈y x y =
    begin
      (x + y) - x
    ≈⟨ +-assoc x y (- x) ⟩
      x + (y - x)
    ≈⟨ +-cong refl (+-comm y (- x)) ⟩
      x + (- x + y)
    ≈⟨ sym (+-assoc x (- x) y) ⟩
      (x - x) + y
    ≈⟨ +-cong (proj₂ -‿inverse x) refl ⟩
      0# + y
    ≈⟨ +-identityˡ y ⟩
      y
    ∎

  x+y+z≈x+z+y : ∀ x y z → x + y + z ≈ x + z + y
  x+y+z≈x+z+y x y z =
    begin
      (x + y) + z
    ≈⟨ +-assoc x y z ⟩
      x + (y + z)
    ≈⟨ +-cong refl (+-comm y z) ⟩
      x + (z + y)
    ≈⟨ sym (+-assoc x z y) ⟩
      (x + z) + y
    ∎

  linear-diff : ∀ m b x dy → line m b (x + dy) - line m b x ≈ m * dy
  linear-diff m b x dy =
    begin
      m * (x + dy) + b - (m * x + b)
    ≈⟨ +-cong (+-cong (distribˡ m x dy) refl) refl ⟩
      m * x + m * dy + b - (m * x + b)
    ≈⟨ +-cong (x+y+z≈x+z+y (m * x) (m * dy) b) refl ⟩
      m * x + b + m * dy - (m * x + b)
    ≈⟨ x+y-x≈y (m * x + b) (m * dy) ⟩
      m * dy
    ∎

max_stars_repo_name: cspollard/diff

max_issues_repo_name: cspollard/diff

max_forks_repo_name: cspollard/diff


text:
{-

This file contains:

- Properties of groupoid truncations

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

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

open import Cubical.HITs.GroupoidTruncation.Base

private
  variable
    ℓ : Level
    A : Type ℓ

rec : ∀ {B : Type ℓ} → isGroupoid B → (A → B) → ∥ A ∥₃ → B
rec gB f ∣ x ∣₃ = f x
rec gB f (squash₃ x y p q r s i j k) =
  gB _ _ _ _ (λ m n → rec gB f (r m n)) (λ m n → rec gB f (s m n)) i j k

elim : {B : ∥ A ∥₃ → Type ℓ}
       (bG : (x : ∥ A ∥₃) → isGroupoid (B x))
       (f : (x : A) → B ∣ x ∣₃) (x : ∥ A ∥₃) → B x
elim bG f (∣ x ∣₃) = f x
elim bG f (squash₃ x y p q r s i j k) =
  isOfHLevel→isOfHLevelDep 3 bG _ _ _ _
    (λ j k → elim bG f (r j k)) (λ j k → elim bG f (s j k))
    (squash₃ x y p q r s)
    i j k

elim2 : {B : ∥ A ∥₃ → ∥ A ∥₃ → Type ℓ}
        (gB : ((x y : ∥ A ∥₃) → isGroupoid (B x y)))
        (g : (a b : A) → B ∣ a ∣₃ ∣ b ∣₃)
        (x y : ∥ A ∥₃) → B x y
elim2 gB g = elim (λ _ → isGroupoidΠ (λ _ → gB _ _))
                  (λ a → elim (λ _ → gB _ _) (g a))

elim3 : {B : (x y z : ∥ A ∥₃) → Type ℓ}
        (gB : ((x y z : ∥ A ∥₃) → isGroupoid (B x y z)))
        (g : (a b c : A) → B ∣ a ∣₃ ∣ b ∣₃ ∣ c ∣₃)
        (x y z : ∥ A ∥₃) → B x y z
elim3 gB g = elim2 (λ _ _ → isGroupoidΠ (λ _ → gB _ _ _))
                   (λ a b → elim (λ _ → gB _ _ _) (g a b))

groupoidTruncIsGroupoid : isGroupoid ∥ A ∥₃
groupoidTruncIsGroupoid a b p q r s = squash₃ a b p q r s

groupoidTruncIdempotent≃ : isGroupoid A → ∥ A ∥₃ ≃ A
groupoidTruncIdempotent≃ {A = A} hA = isoToEquiv f
  where
  f : Iso ∥ A ∥₃ A
  Iso.fun f = rec hA (idfun A)
  Iso.inv f x = ∣ x ∣₃
  Iso.rightInv f _ = refl
  Iso.leftInv f = elim (λ _ → isGroupoid→is2Groupoid groupoidTruncIsGroupoid _ _) (λ _ → refl)

groupoidTruncIdempotent : isGroupoid A → ∥ A ∥₃ ≡ A
groupoidTruncIdempotent hA = ua (groupoidTruncIdempotent≃ hA)

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Cubical.Codata.M.AsLimit.Coalg where

open import Cubical.Codata.M.AsLimit.Coalg.Base public


text:
module Oscar.Property.Extensionality where

open import Oscar.Level

record Extensionality
  {a} {A : Set a} {b} {B : A → Set b} {ℓ₁}
    (_≤₁_ : (x : A) → B x → Set ℓ₁)
  {c} {C : A → Set c} {d} {D : ∀ {x} → B x → Set d} {ℓ₂}
    (_≤₂_ : ∀ {x} → C x → ∀ {y : B x} → D y → Set ℓ₂)
    (μ₁ : (x : A) → C x)
    (μ₂ : ∀ {x} → (y : B x) → D y)
  : Set (a ⊔ ℓ₁ ⊔ b ⊔ ℓ₂) where
  field
    extensionality : ∀ {x} {y : B x} → x ≤₁ y → μ₁ x ≤₂ μ₂ y

open Extensionality ⦃ … ⦄ public

extension : ∀
    {a} {A : Set a}
    {b} {B : A → Set b}
    {ℓ₁} {_≤₁_ : (x : A) → B x → Set ℓ₁}
    {c} {C : A → Set c} {d} {D : ∀ {x} → B x → Set d} {ℓ₂}
  (_≤₂_ : ∀ {x} → C x → ∀ {y : B x} → D y → Set ℓ₂)
    {μ₁ : (x : A) → C x}
    {μ₂ : ∀ {x} → (y : B x) → D y}
  ⦃ _ : Extensionality _≤₁_ _≤₂_ μ₁ μ₂ ⦄
    {x} {y : B x}
  → x ≤₁ y → μ₁ x ≤₂ μ₂ y
extension _≤₂_ = extensionality {_≤₂_ = _≤₂_}


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

open import Base
open import Homotopy.Truncation
open import Integers

-- Formalization of 0-truncated groups
module Algebra.Groups where

-- A pregroup is a group whose carrier is not a required to be a set (but
-- without higher coherences)

record pregroup i : Set (suc i) where
  -- constructor pregroup
  field
    -- Stuff
    carrier : Set i  -- \|

    -- Structure
    _∙_ : carrier → carrier → carrier  -- \.
    e : carrier
    _′ : carrier → carrier  -- \'

    -- Properties
    assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
    right-unit : ∀ x → x ∙ e ≡ x
    left-unit : ∀ x → e ∙ x ≡ x
    right-inverse : ∀ x → x ∙ (x ′) ≡ e
    left-inverse : ∀ x → (x ′) ∙ x ≡ e

record group i : Set (suc i) where
  -- constructor group
  field
    pre : pregroup i
  open pregroup pre
  field
    set : is-set carrier
  open pregroup pre public

-- Group structure on [unit]
unit-group : ∀ {i} → group i
unit-group {i} = record
  { pre = record
    { carrier = unit
    ; _∙_ = λ _ _ → tt
    ; e = tt
    ; _′ = λ _ → tt
    ; assoc = λ _ _ _ → refl
    ; right-unit = λ _ → refl
    ; left-unit = λ _ → refl
    ; right-inverse = λ _ → refl
    ; left-inverse = λ _ → refl
    }
  ; set = unit-is-set
  }

postulate  -- Tedious because I have a terrible definition of groups
  unit-group-unique : ∀ {i} (G : group i) →
    let open group G in (c : is-contr carrier) → G ≡ unit-group

-- Every pregroup can be truncated to a group
π₀-pregroup : ∀ {i} → pregroup i → group i
π₀-pregroup pre = record
  { pre = record
    { carrier = carrier₀
    ; _∙_ = _•₀_
    ; e = e₀
    ; _′ = _′₀
    ; assoc = assoc₀
    ; right-unit = right-unit₀
    ; left-unit = left-unit₀
    ; right-inverse = right-inverse₀
    ; left-inverse = left-inverse₀
    }
  ; set = carrier₀-is-set
  } where

    open pregroup pre

    carrier₀ : Set _
    carrier₀ = π₀ carrier

    carrier₀-is-set : is-set carrier₀
    carrier₀-is-set = π₀-is-set carrier

    _•₀_ : carrier₀ → carrier₀ → carrier₀
    _•₀_ = π₀-extend-nondep ⦃ →-is-set $ carrier₀-is-set ⦄
              (λ x → π₀-extend-nondep ⦃ carrier₀-is-set ⦄
                (λ y → proj (x ∙ y)))

    e₀ : π₀ carrier
    e₀ = proj e

    _′₀ : carrier₀ → carrier₀
    _′₀ = π₀-extend-nondep ⦃ carrier₀-is-set ⦄ (λ x → proj (x ′))

    abstract
      assoc₀ : ∀ x y z → (x •₀ y) •₀ z ≡ x •₀ (y •₀ z)
      assoc₀ =
        (π₀-extend ⦃ λ _ → Π-is-set λ _ → Π-is-set λ _ → ≡-is-set carrier₀-is-set ⦄
          (λ x → π₀-extend ⦃ λ _ → Π-is-set λ _ → ≡-is-set carrier₀-is-set ⦄
            (λ y → π₀-extend ⦃ λ _ → ≡-is-set carrier₀-is-set ⦄
              (λ z → ap proj (assoc x y z)))))

    abstract
      right-unit₀ : ∀ x → x •₀ e₀ ≡ x
      right-unit₀ =
        (π₀-extend ⦃ λ _ → ≡-is-set carrier₀-is-set ⦄
          (ap proj ◯ right-unit))

    abstract
      left-unit₀ : ∀ x → e₀ •₀ x ≡ x
      left-unit₀ =
        (π₀-extend ⦃ λ _ → ≡-is-set carrier₀-is-set ⦄
          (ap proj ◯ left-unit))

    abstract
      right-inverse₀ : ∀ x → x •₀ (x ′₀) ≡ e₀
      right-inverse₀ =
        (π₀-extend ⦃ λ _ → ≡-is-set carrier₀-is-set ⦄
          (ap proj ◯ right-inverse))

    abstract
      left-inverse₀ : ∀ x → (x ′₀) •₀ x ≡ e₀
      left-inverse₀ =
        (π₀-extend ⦃ λ _ → ≡-is-set carrier₀-is-set ⦄
          (ap proj ◯ left-inverse))

-- Not used

-- is-group-morphism : ∀ {i j} (A : Group i) (B : Group j)
-- (f : ∣ g A ∣ → ∣ g B ∣)
--   → Set (max i j)
-- is-group-morphism A B f =
--   (x y : ∣ g A ∣) → f (_∙_ (g A) x y) ≡ _∙_ (g B) (f x) (f y)

-- _≈_ : ∀ {i j} (A : Group i) (B : Group j) → Set (max i j)
-- A ≈ B = Σ (∣ g A ∣ → ∣ g B ∣) (λ f → is-equiv f × is-group-morphism A B f)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-

Definition of the integers as a HIT ported from the redtt library:

  https://github.com/RedPRL/redtt/blob/master/library/cool/biinv-int.red

For the naive, but incorrect, way to define the integers as a HIT, see HITs.IsoInt

This file contains:
- definition of BiInvInt
- proof that Int ≡ BiInvInt
- [discreteBiInvInt] and [isSetBiInvInt]
- versions of the point constructors of BiInvInt which satisfy the path constructors judgmentally

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Ints.BiInvInt.Base where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Nat
open import Cubical.Data.Int

open import Cubical.Foundations.GroupoidLaws

open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.BiInvEquiv
open import Cubical.Foundations.HAEquiv
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties

open import Cubical.Relation.Nullary

data BiInvInt : Type₀ where
  zero : BiInvInt
  suc : BiInvInt -> BiInvInt

  -- suc is a bi-invertible equivalence:
  predr : BiInvInt -> BiInvInt
  suc-predr : ∀ z -> suc (predr z) ≡ z
  predl : BiInvInt -> BiInvInt
  predl-suc : ∀ z -> predl (suc z) ≡ z

suc-biinvequiv : BiInvEquiv BiInvInt BiInvInt
suc-biinvequiv = record { fun = suc ; invr = predr ; invr-rightInv = suc-predr
                                    ; invl = predl ; invl-leftInv  = predl-suc }

predr-suc : ∀ z -> predr (suc z) ≡ z
predr-suc = BiInvEquiv.invr-leftInv suc-biinvequiv

-- since we want to use suc-adj and pred-adj (defined below) later on, we will need the
--  definition of suc-predl taken from HAEquiv instead of from BiInvEquiv

suc-haequiv : HAEquiv BiInvInt BiInvInt
suc-haequiv = biInvEquiv→HAEquiv suc-biinvequiv

suc-predl : ∀ z -> suc (predl z) ≡ z
suc-predl = isHAEquiv.ret (snd suc-haequiv)

-- predr and predl (as well as suc-predr and suc-predl - up to a path) are indistinguishable,
--  so we can safely define 'pred' to just be predl

predl≡predr : ∀ z -> predl z ≡ predr z
predl≡predr z i = cong fst (isContr→isProp (isContr-section (biInvEquiv→Equiv-left suc-biinvequiv))
                                           (predl , suc-predl) (predr , suc-predr)) i z

suc-predl≡predr : ∀ z -> PathP (λ j → suc (predl≡predr z j) ≡ z) (suc-predl z) (suc-predr z)
suc-predl≡predr z i = cong snd (isContr→isProp (isContr-section (biInvEquiv→Equiv-left suc-biinvequiv))
                                               (predl , suc-predl) (predr , suc-predr)) i z

pred : BiInvInt -> BiInvInt
pred = predl

suc-pred = suc-predl
pred-suc = predl-suc

-- these paths from HAEquiv will be useful later
suc-adj  : ∀ z → (λ i → suc (pred-suc z i)) ≡ suc-pred (suc z)
pred-adj : ∀ z → (λ i → pred (suc-pred z i)) ≡ pred-suc (pred z)
suc-adj  z = isHAEquiv.com (snd suc-haequiv) z
pred-adj z = isHAEquiv.com-op (snd suc-haequiv) z

-- Int ≡ BiInvInt

fwd : Int -> BiInvInt
fwd (pos zero)       = zero
fwd (pos (suc n))    = suc (fwd (pos n))
fwd (negsuc zero)    = pred zero
fwd (negsuc (suc n)) = pred (fwd (negsuc n))

bwd : BiInvInt -> Int
bwd zero            = pos zero
bwd (suc z)         = sucInt (bwd z)
bwd (predr z)       = predInt (bwd z)
bwd (suc-predr z i) = sucPred (bwd z) i
bwd (predl z)       = predInt (bwd z)
bwd (predl-suc z i) = predSuc (bwd z) i

bwd-fwd : ∀ (x : Int) -> bwd (fwd x) ≡ x
bwd-fwd (pos zero)       = refl
bwd-fwd (pos (suc n))    = cong sucInt (bwd-fwd (pos n))
bwd-fwd (negsuc zero)    = refl
bwd-fwd (negsuc (suc n)) = cong predInt (bwd-fwd (negsuc n))

fwd-sucInt : ∀ (x : Int) → fwd (sucInt x) ≡ suc (fwd x)
fwd-sucInt (pos n)          = refl
fwd-sucInt (negsuc zero)    = sym (suc-pred (fwd (pos zero)))
fwd-sucInt (negsuc (suc n)) = sym (suc-pred (fwd (negsuc n)))

fwd-predInt : ∀ (x : Int) → fwd (predInt x) ≡ pred (fwd x)
fwd-predInt (pos zero)    = refl
fwd-predInt (pos (suc n)) = sym (predl-suc (fwd (pos n)))
fwd-predInt (negsuc n)    = refl

private
  sym-filler : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y)
                → Square {- (j = i0) -} refl
                         {- (i = i0) -} (sym p)
                         {- (i = i1) -} refl
                         {- (j = i1) -} p
  sym-filler {y = y} p i j = hcomp (λ k → λ { (j = i0) → y
                                            ; (i = i0) → p ((~ j) ∨ (~ k))
                                            ; (i = i1) → y
                                            ; (j = i1) → p (i ∨ (~ k)) }) y

fwd-sucPred : ∀ (x : Int)
              → Square {- (j = i0) -} (λ i → fwd (sucPred x i))
                       {- (i = i0) -} (fwd-sucInt (predInt x) ∙ (λ i → suc (fwd-predInt x i)))
                       {- (i = i1) -} (λ _ → fwd x)
                       {- (j = i1) -} (suc-pred (fwd x))

fwd-sucPred (pos zero) i j
  = hcomp (λ k → λ { (j = i0) → fwd (pos zero)
                   ; (i = i0) → rUnit (sym (suc-pred (fwd (pos zero)))) k j
                                -- because fwd-sucInt (predInt (pos zero)) ≡ sym (suc-pred (fwd (pos zero)))
                   ; (i = i1) → fwd (pos zero)
                   ; (j = i1) → suc-pred (fwd (pos zero)) i
                   })
          (sym-filler (suc-pred (fwd (pos zero))) i j)

fwd-sucPred (pos (suc n)) i j
  = hcomp (λ k → λ { (j = i0) → suc (fwd (pos n))
                   ; (i = i0) → lUnit (λ i → suc (sym (predl-suc (fwd (pos n))) i)) k j
                                -- because fwd-predInt (pos (suc n)) ≡ sym (predl-suc (fwd (pos n)))
                   ; (i = i1) → suc (fwd (pos n))
                   ; (j = i1) → suc-adj (fwd (pos n)) k i
                   })
          (suc (sym-filler (pred-suc (fwd (pos n))) i j))

fwd-sucPred (negsuc n) i j
  = hcomp (λ k → λ { (j = i0) → fwd (negsuc n)
                   ; (i = i0) → rUnit (sym (suc-pred (fwd (negsuc n)))) k j
                                -- because fwd-sucInt (predInt (negsuc n)) ≡ sym (suc-pred (fwd (negsuc n)))
                   ; (i = i1) → fwd (negsuc n)
                   ; (j = i1) → suc-pred (fwd (negsuc n)) i
                   })
          (sym-filler (suc-pred (fwd (negsuc n))) i j)

fwd-predSuc : ∀ (x : Int)
              → Square {- (j = i0) -} (λ i → fwd (predSuc x i))
                       {- (i = i0) -} (fwd-predInt (sucInt x) ∙ (λ i → pred (fwd-sucInt x i)))
                       {- (i = i1) -} (λ _ → fwd x)
                       {- (j = i1) -} (pred-suc (fwd x))

fwd-predSuc (pos n) i j
  = hcomp (λ k → λ { (j = i0) → fwd (pos n)
                   ; (i = i0) → rUnit (sym (pred-suc (fwd (pos n)))) k j
                                -- because fwd-predInt (sucInt (pos n)) ≡ sym (pred-suc (fwd (pos n)))
                   ; (i = i1) → fwd (pos n)
                   ; (j = i1) → pred-suc (fwd (pos n)) i
                   })
          (sym-filler (pred-suc (fwd (pos n))) i j)

fwd-predSuc (negsuc zero) i j
  = hcomp (λ k → λ { (j = i0) → fwd (negsuc zero)
                   ; (i = i0) → lUnit (λ i → pred (sym (suc-pred (fwd (pos zero))) i)) k j
                                -- because fwd-sucInt (negsuc zero) ≡ sym (suc-pred (fwd (pos zero)))
                   ; (i = i1) → fwd (negsuc zero)
                   ; (j = i1) → pred-adj (fwd (pos zero)) k i
                   })
          (pred (sym-filler (suc-pred (fwd (pos zero))) i j))

fwd-predSuc (negsuc (suc n)) i j
  = hcomp (λ k → λ { (j = i0) → fwd (negsuc (suc n))
                   ; (i = i0) → lUnit (λ i → pred (sym (suc-pred (fwd (negsuc n))) i)) k j
                                -- because fwd-sucInt (negsuc (suc n)) ≡ sym (suc-pred (fwd (negsuc n)))
                   ; (i = i1) → fwd (negsuc (suc n))
                   ; (j = i1) → pred-adj (fwd (negsuc n)) k i
                   })
          (pred (sym-filler (suc-pred (fwd (negsuc n))) i j))

fwd-bwd : ∀ (z : BiInvInt) -> fwd (bwd z) ≡ z
fwd-bwd zero      = refl
fwd-bwd (suc z)   = fwd-sucInt  (bwd z) ∙ (λ i → suc (fwd-bwd z i))
fwd-bwd (predr z) = fwd-predInt (bwd z) ∙ (λ i → predl≡predr (fwd-bwd z i) i)
fwd-bwd (predl z) = fwd-predInt (bwd z) ∙ (λ i → pred (fwd-bwd z i))
fwd-bwd (suc-predr z i) j
  = hcomp (λ k → λ { (j = i0) → fwd (sucPred (bwd z) i)
                   ; (i = i0) → (fwd-sucInt (predInt (bwd z))
                                 ∙ (λ i → suc (compPath-filler (fwd-predInt (bwd z))
                                                               (λ i' → predl≡predr (fwd-bwd z i') i')
                                                               k i))) j
                   ; (i = i1) → fwd-bwd z (j ∧ k)
                   ; (j = i1) → suc-predl≡predr (fwd-bwd z k) k i })
          (fwd-sucPred (bwd z) i j)
fwd-bwd (predl-suc z i) j
  = hcomp (λ k → λ { (j = i0) → fwd (predSuc (bwd z) i)
                   ; (i = i0) → (fwd-predInt (sucInt (bwd z))
                                 ∙ (λ i → pred (compPath-filler (fwd-sucInt (bwd z))
                                                                (λ i' → suc (fwd-bwd z i'))
                                                                k i))) j
                   ; (i = i1) → fwd-bwd z (j ∧ k)
                   ; (j = i1) → pred-suc (fwd-bwd z k) i })
          (fwd-predSuc (bwd z) i j)

Int≡BiInvInt : Int ≡ BiInvInt
Int≡BiInvInt = isoToPath (iso fwd bwd fwd-bwd bwd-fwd)

discreteBiInvInt : Discrete BiInvInt
discreteBiInvInt = subst Discrete Int≡BiInvInt discreteInt

isSetBiInvInt : isSet BiInvInt
isSetBiInvInt = subst isSet Int≡BiInvInt isSetInt

-- suc' is equal to suc (suc≡suc') but cancels pred *exactly* (see suc'-pred)

suc'ᵖ : (z : BiInvInt) -> Σ BiInvInt (suc z ≡_)
suc' = fst ∘ suc'ᵖ
suc≡suc' = snd ∘ suc'ᵖ

suc'ᵖ zero = suc zero , refl
suc'ᵖ (suc z) = suc (suc z) , refl
suc'ᵖ (predr z) = z , suc-predr z
suc'ᵖ (suc-predr z i) = let filler : I → I → BiInvInt
                            filler j i = hfill (λ j → λ { (i = i0) → suc (suc (predr z))
                                                        ; (i = i1) → suc≡suc' z j })
                                               (inS (suc (suc-predr z i))) j
                         in filler i1 i , λ j → filler j i
suc'ᵖ (predl z) = z , suc-predl z
suc'ᵖ (predl-suc z i) = let filler : I → I → BiInvInt
                            filler j i = hfill (λ j → λ { (i = i0) → suc-predl (suc z) j
                                                        ; (i = i1) → suc≡suc' z j })
                                               (inS (suc (predl-suc z i))) j
                         in filler i1 i , λ j → filler j i

private
  suc'-pred : ∀ z → suc' (pred z) ≡ z
  suc'-pred z = refl

-- pred' is equal to pred (pred≡pred') but cancels suc *exactly* (see pred'-suc)

predr'ᵖ : (z : BiInvInt) -> Σ BiInvInt (predr z ≡_)
predr' = fst ∘ predr'ᵖ
predr≡predr' = snd ∘ predr'ᵖ

predr'ᵖ zero = predr zero , refl
predr'ᵖ (suc z) = z , predr-suc z
predr'ᵖ (predr z) = predr (predr z) , refl
predr'ᵖ (suc-predr z i) = let filler : I → I → BiInvInt
                              filler j i = hfill (λ j → λ { (i = i0) → predr-suc (predr z) j
                                                          ; (i = i1) → predr≡predr' z j })
                                                 (inS (predr (suc-predr z i))) j
                           in filler i1 i , λ j → filler j i
predr'ᵖ (predl z) = predr (predl z) , refl
predr'ᵖ (predl-suc z i) = let filler : I → I → BiInvInt
                              filler j i = hfill (λ j → λ { (i = i0) → predr (predl (suc z))
                                                          ; (i = i1) → predr≡predr' z j })
                                                 (inS (predr (predl-suc z i))) j
                           in filler i1 i , λ j → filler j i

predl'ᵖ : (z : BiInvInt) -> Σ BiInvInt (predl z ≡_)
predl' = fst ∘ predl'ᵖ
predl≡predl' = snd ∘ predl'ᵖ

predl'ᵖ zero = predl zero , refl
predl'ᵖ (suc z) = z , predl-suc z
predl'ᵖ (predr z) = predl (predr z) , refl
predl'ᵖ (suc-predr z i) = let filler : I → I → BiInvInt
                              filler j i = hfill (λ j → λ { (i = i0) → predl-suc (predr z) j
                                                          ; (i = i1) → predl≡predl' z j })
                                                 (inS (predl (suc-predr z i))) j
                           in filler i1 i , λ j → filler j i
predl'ᵖ (predl z) = predl (predl z) , refl
predl'ᵖ (predl-suc z i) = let filler : I → I → BiInvInt
                              filler j i = hfill (λ j → λ { (i = i0) → predl (predl (suc z))
                                                          ; (i = i1) → predl≡predl' z j })
                                                 (inS (predl (predl-suc z i))) j
                           in filler i1 i , λ j → filler j i

private
  predr'-suc : ∀ z → predr' (suc z) ≡ z
  predr'-suc z = refl

  predl'-suc : ∀ z → predl' (suc z) ≡ z
  predl'-suc z = refl

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Numeral.Natural.Oper.Summation.Range.Proofs where

import      Lvl
open import Data.List
open import Data.List.Functions
open        Data.List.Functions.LongOper
open import Data.List.Proofs
open import Data.List.Equiv.Id
open import Data.List.Proofs.Length
open import Functional as Fn using (_$_ ; _∘_ ; const)
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Summation.Range
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals hiding (_≡_)
open import Relator.Equals.Proofs.Equiv
open import Structure.Function
open import Structure.Function.Multi
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

Range-empty : ∀{a} → (a ‥ a ≡ ∅)
Range-empty {𝟎} = [≡]-intro
Range-empty {𝐒 a} rewrite Range-empty {a} = [≡]-intro
{-# REWRITE Range-empty #-}

Range-reversed : ∀{a b} → ⦃ _ : (a ≥ b) ⦄ → (a ‥ b ≡ ∅)
Range-reversed {a}   {𝟎}   ⦃ min ⦄ = [≡]-intro
Range-reversed {𝐒 a} {𝐒 b} ⦃ succ p ⦄
  rewrite Range-reversed {a} {b} ⦃ p ⦄
  = [≡]-intro

Range-succ : ∀{a b} → (map 𝐒(a ‥ b) ≡ 𝐒(a) ‥ 𝐒(b))
Range-succ = [≡]-intro

Range-prepend : ∀{a b} → ⦃ _ : (a < b) ⦄ → (a ‥ b ≡ prepend a (𝐒(a) ‥ b))
Range-prepend {𝟎}   {𝐒 b} = [≡]-intro
Range-prepend {𝐒 a} {𝐒 b} ⦃ succ ab ⦄ rewrite Range-prepend {a} {b} ⦃ ab ⦄ = [≡]-intro

Range-postpend : ∀{a b} → ⦃ _ : (a < 𝐒(b)) ⦄ → (a ‥ 𝐒(b) ≡ postpend b (a ‥ b))
Range-postpend {𝟎}   {𝟎}   ⦃ [≤]-with-[𝐒] ⦄ = [≡]-intro
Range-postpend {𝟎}   {𝐒 b} ⦃ [≤]-with-[𝐒] ⦄  = congruence₁(prepend 𝟎) $
  map 𝐒(𝟎 ‥ 𝐒(b))                 🝖[ _≡_ ]-[ congruence₁(map 𝐒) (Range-postpend {𝟎}{b}) ]
  map 𝐒(postpend b (𝟎 ‥ b))       🝖[ _≡_ ]-[ map-postpend ]
  postpend (𝐒(b)) (map 𝐒(𝟎 ‥ b))  🝖-end
Range-postpend {𝐒 a} {𝐒 b} ⦃ succ 𝐒ab ⦄
  rewrite Range-postpend {a} {b} ⦃ 𝐒ab ⦄
  = map-postpend

Range-length : ∀{a b} → (length(a ‥ b) ≡ b −₀ a)
Range-length {𝟎} {𝟎} = [≡]-intro
Range-length {𝟎} {𝐒 b}
  rewrite length-map{f = 𝐒}{x = 𝟎 ‥ b}
  rewrite Range-length {𝟎} {b}
  = congruence₁(𝐒) [≡]-intro
Range-length {𝐒 a} {𝟎} = [≡]-intro
Range-length {𝐒 a} {𝐒 b}
  rewrite length-map{f = 𝐒}{x = a ‥ b}
  rewrite Range-length {a} {b}
  = [≡]-intro

Range-length-zero : ∀{b} → (length(𝟎 ‥ b) ≡ b)
Range-length-zero {b} = Range-length {𝟎}{b}

Range-singleton : ∀{a} → (a ‥ 𝐒(a) ≡ singleton(a))
Range-singleton {𝟎} = [≡]-intro
Range-singleton {𝐒 a}
  rewrite Range-singleton {a}
  = [≡]-intro
{-# REWRITE Range-singleton #-}

Range-concat : ∀{a b c} → ⦃ ab : (a ≤ b) ⦄ ⦃ bc : (b < c) ⦄ → ((a ‥ b) ++ (b ‥ c) ≡ a ‥ c)
Range-concat {𝟎} {𝟎}   {𝐒 c} ⦃ min ⦄ ⦃ succ bc ⦄ = [≡]-intro
Range-concat {𝟎} {𝐒 b} {𝐒 c} ⦃ min ⦄ ⦃ succ bc ⦄ = congruence₁ (prepend 0) $
  map 𝐒(𝟎 ‥ b) ++ map 𝐒 (b ‥ c) 🝖[ _≡_ ]-[ preserving₂(map 𝐒)(_++_)(_++_) {𝟎 ‥ b}{b ‥ c} ]-sym
  map 𝐒((𝟎 ‥ b) ++ (b ‥ c))     🝖[ _≡_ ]-[ congruence₁(map 𝐒) (Range-concat {𝟎} {b} {c}) ]
  map 𝐒(𝟎 ‥ c)                  🝖-end
  where instance _ = bc
Range-concat {𝐒 a} {𝐒 b} {𝐒 c} ⦃ succ ab ⦄ ⦃ succ bc ⦄ =
  map 𝐒(a ‥ b) ++ map 𝐒 (b ‥ c) 🝖[ _≡_ ]-[ preserving₂(map 𝐒)(_++_)(_++_) {a ‥ b}{b ‥ c} ]-sym
  map 𝐒((a ‥ b) ++ (b ‥ c))     🝖[ _≡_ ]-[ congruence₁(map 𝐒) (Range-concat {a} {b} {c}) ]
  map 𝐒(a ‥ c)                  🝖-end
  where
    instance _ = ab
    instance _ = bc

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Section9 where

open import Section8 public

-- 9. A decision algorithm for terms
-- =================================
--
-- The reduction defined above can be used for deciding if two well-typed terms are convertible
-- with each other or not: reduce the terms and check if the results are equal.  This algorithm
-- is implicit in Martin-Löf’s notes [13].
--
-- The decision algorithm is complete:

-- Theorem 11.
postulate
  thm₁₁ : ∀ {Γ A t₀ t₁} →
            Γ ⊢ t₀ ≊ t₁ ∷ A →
            Σ 𝕋 (λ t → Γ ⊢ t₀ ⇓ t ∷ A × Γ ⊢ t₁ ⇓ t ∷ A)

-- Proof:  By Lemma 14 and Lemma 12 we know that there exist proof trees `M, N` such
-- that `t₀` is equal to `M ⁻` and `t₁` is equal to `N ⁻`.  By Theorem 9 we get that `M ≅ N`.  We can
-- choose `nf M ⁻` for `t` since, by Lemma 8, `Γ ⊢ M ⁻ ⇓ nf M ⁻ ∷ A`, `Γ ⊢ N ⁻ ⇓ nf N ⁻ ∷ A`
-- and by Theorem 6 we have `nf M ≡ nf N` and hence that `nf M ⁻` and `nf N ⁻` are the
-- same.
--
-- This decision algorithm is correct, i.e.,

-- Theorem 12.
postulate
  thm₁₂ : ∀ {Γ A t} →
            (M N : Γ ⊢ A) → Γ ⊢ M ⁻ ⇓ t ∷ A → Γ ⊢ N ⁻ ⇓ t ∷ A →
            M ≅ N

-- Proof:  We have `nf M ⁻ ≡ nf N ⁻` since, by Lemma 8, `Γ ⊢ M ⁻ ⇓ nf M ⁻ ∷ A`
-- and `Γ ⊢ N ⁻ ⇓ nf N ⁻ ∷ A` and the reduction is deterministic.  By Corollary 2 we get
-- `M ≅ N`.

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
-- Andreas, 2019-12-03, issue #4205, reported by Smaug123,
-- first shrinking by Jesper Cockx

record R : Set₂ where
  field
    f : Set₁

postulate
  r : R

open R r

test : R
R.f test with Set₃
f test | _  = Set

-- WAS: internal error in getOriginalProjection

-- EXPECTED:
-- With clause pattern f is not an instance of its parent pattern R.f
-- when checking that the clause
-- R.f test with Set₃
-- f test | _ = Set
-- has type R

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Ints.Add.Invert where

open import Ints
open import Ints.Properties
open import Ints.Add.Comm
open import Nats.Add.Invert

open import Data.Empty
open import Relation.Nullary

open import Equality
open import Function

------------------------------------------------------------------------
-- internal stuffs

private

  nat→int′ : ∀ a b → -[1+ nsuc $ a :+: a ] ≡ -[1+ nsuc $ b :+: b ] → a ≡ b
  nat→int′ a b = nat-add-invert a b ∘ nat-add-invert-1 (a :+: a) (b :+: b) ∘ eq-neg-int-to-nat

  impossible : ∀ a b → ¬ (+ a + + a ≡ -[1+ b ] + -[1+ b ])
  impossible a b ()

  +-invert : ∀ a b → (a + a ≡ b + b) → a ≡ b
  +-invert  (+  a )  (+  b ) = eq-nat-to-int ∘ nat-add-invert a b ∘ eq-int-to-nat
  +-invert  (+  a ) -[1+ b ] = ⊥-elim ∘ impossible a b
  +-invert -[1+ a ]  (+  b ) = ⊥-elim ∘ impossible b a ∘ sym
  +-invert -[1+ a ] -[1+ b ] = eq-neg-nat-to-int ∘ nat→int′ a b

------------------------------------------------------------------------
-- public aliases

int-add-invert : ∀ a b → (a + a ≡ b + b) → a ≡ b
int-add-invert = +-invert


text:
-- {-# OPTIONS -v impossible:100 -v tc.lhs.imp:100 #-}
-- {-# OPTIONS -v impossible:100 -v tc.cover:20 #-}
{-# OPTIONS --copatterns #-}
module Copatterns where

open import Common.Equality

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

pair : {A B : Set} → A → B → A × B
fst (pair a b) = a
snd (pair a b) = b

swap : {A B : Set} → A × B → B × A
fst (swap p) = snd p
snd (swap p) = fst p

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
fst (swap3 t)       = snd (snd t)
fst (snd (swap3 t)) = fst (snd t)
snd (snd (swap3 t)) = fst t

-- should also work if we shuffle the clauses
swap4 : {A B C D : Set} → A × (B × (C × D)) → D × (C × (B × A))
fst (snd (swap4 t))       = fst (snd (snd t))
snd (snd (snd (swap4 t))) = fst t
fst (swap4 t)             = snd (snd (snd t))
fst (snd (snd (swap4 t))) = fst (snd t)

-- multiple clauses with abstractions

fswap3 : {A B C X : Set} → (X → A) × ((X → B) × C) → (X → C) × (X → (B × A))
fst (fswap3 t) x       = snd (snd t)
fst (snd (fswap3 t) y) = fst (snd t) y
snd (snd (fswap3 t) z) = fst t z

-- State monad example

-- The State newtype

record State (S A : Set) : Set where
  constructor state
  field
    runState : S → A × S
open State

-- The Monad type class

record Monad (M : Set → Set) : Set1 where
  constructor monad
  field
    return : {A : Set}   → A → M A
    _>>=_  : {A B : Set} → M A → (A → M B) → M B

module NoInstance where

-- State is an instance of Monad

  stateMonad : {S : Set} → Monad (State S)
  runState (Monad.return stateMonad a  ) s  = a , s
  runState (Monad._>>=_  stateMonad m k) s₀ =
    let a , s₁ = runState m s₀
    in  runState (k a) s₁

  module InstantiatedModule {S : Set} where

    open Monad (stateMonad {S})

    leftId : {A B : Set}(a : A)(k : A → State S B) →
      (return a >>= k) ≡ k a
    leftId a k = refl

    rightId : {A B : Set}(m : State S A) →
      (m >>= return) ≡ m
    rightId m = refl

    assoc : {A B C : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
      ((m >>= k) >>= l) ≡ (m >>= λ a → (k a >>= l))
    assoc m k l = refl

  module VisibleArgument where

    open Monad

    leftId : {A B S : Set}(a : A)(k : A → State S B) →
      (_>>=_ stateMonad (return stateMonad a) k) ≡ k a
    leftId a k = refl

    rightId : {A B S : Set}(m : State S A) →
      (_>>=_ stateMonad m (return stateMonad)) ≡ m
    rightId m = refl

    assoc : {A B C S : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
       (_>>=_ stateMonad (_>>=_ stateMonad m k) l) ≡
      (_>>=_ stateMonad m λ a → _>>=_ stateMonad (k a) l)
    assoc m k l = refl

  module HiddenArgument where

    return : ∀ {M}{dict : Monad M}{A : Set} → A → M A
    return {dict = dict} = Monad.return dict

    _>>=_ :  ∀ {M}{dict : Monad M}{A B : Set} → M A → (A → M B) → M B
    _>>=_ {dict = dict} = Monad._>>=_ dict

    leftId : {A B S : Set}(a : A)(k : A → State S B) →
      (_>>=_ {dict = stateMonad} (return {dict = stateMonad} a) k) ≡ k a
    leftId a k = refl

  {- LOTS OF YELLOW:

    leftId : {A B S : Set}(a : A)(k : A → State S B) → (return {dict = stateMonad {S}} a >>= k) ≡ k a
    leftId a k = refl

    rightId : {A B S : Set}(m : State S A) → (m >>= return) ≡ m
    rightId m = refl

    assoc : {A B C S : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
       ((m >>= k) >>= l) ≡ (m >>= λ a → k a >>= l)
    assoc m k l = refl
  -}

{- WORKS NOT YET
module InstanceArgument where

  open Monad {{...}}

  -- State is an instance of Monad

  -- TODO: this does not work with hidden argument yet
  stateMonad : {S : Set} → Monad (State S)
  runState (return {{stateMonad {S}}} a  ) s  = a , s
  runState (_>>=_  {{stateMonad {S}}} m k) s₀ =
    let a , s₁ = runState m s₀
    in  runState (k a) s₁

  _~_ : {S A : Set} → State S A → State S A → Set
  m ~ m' = ∀ {s} → runState m s ≡ runState m' s

  -- the following identities should also hold with _≡_
  -- but that would need a back-translation of copatterns to
  -- record expressions, which does not preserve SN for recursive cases
  leftId : {A B S : Set}(a : A)(k : A → State S B) → (return a >>= k) ≡ k a
  leftId a k = refl

  rightId : {A B S : Set}(m : State S A) → (m >>= return) ~ m
  rightId m = refl

  assoc : {A B C S : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
     ((m >>= k) >>= l) ~ (m >>= λ a → k a >>= l)
  assoc m k l = refl
-}

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --without-K #-}
module hott.level.closure.lift where

open import level
open import function.isomorphism.lift
open import hott.level.core
open import hott.level.closure.core

-- lifting preserves h-levels
↑-level : ∀ {i n} j {X : Set i}
        → h n X
        → h n (↑ j X)
↑-level j {X} = iso-level (lift-iso j X)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

open import Numbers.Naturals.Definition
open import LogicalFormulae
open import Groups.Definition
open import Groups.Orders.Partial.Definition
open import Setoids.Orders.Partial.Definition
open import Setoids.Setoids

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

module Groups.Orders.Archimedean {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {G : Group S _+_} {c : _} {_<_ : A → A → Set c} {pOrder : SetoidPartialOrder S _<_} (p : PartiallyOrderedGroup G pOrder) where

open Setoid S
open import Groups.Cyclic.Definition G
open Group G

Archimedean : Set (a ⊔ c)
Archimedean = (x y : A) → (0G < x) → (0G < y) → Sg ℕ (λ n → y < (positiveEltPower x n))


text:
open import Common.Prelude

_test_ : Nat → Nat → Nat
m test_ = m +_

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Agda.Primitive
open import Prelude
import GSeTT.Typed-Syntax
import Globular-TT.Syntax

{- Type theory for globular sets -}
module Globular-TT.Uniqueness-Derivations {l}
  (index : Set l) (rule : index → GSeTT.Typed-Syntax.Ctx × (Globular-TT.Syntax.Pre-Ty index)) (eqdec-index : eqdec index)  where

  open import Globular-TT.Syntax index
  open import Globular-TT.Rules index rule
  open import Globular-TT.Eqdec-syntax index eqdec-index

  lΓ≤n→n∉Γ : ∀ {Γ A} n → Γ ⊢C → C-length Γ ≤ n →  ¬ (n # A ∈ Γ)
  lΓ≤n→n∉Γ n (cc Γ⊢ Γ⊢A idp) Sl≤n (inl x) = lΓ≤n→n∉Γ n Γ⊢ (≤T (n≤Sn _) Sl≤n) x
  lΓ≤n→n∉Γ n (cc Γ⊢ Γ⊢A idp) Sl≤n (inr (idp , idp)) = Sn≰n _ Sl≤n

  lΓ∉Γ : ∀ {Γ A} → Γ ⊢C → ¬ (C-length Γ # A ∈ Γ)
  lΓ∉Γ Γ⊢ = lΓ≤n→n∉Γ _ Γ⊢ (n≤n _)

  has-all-paths-∈ : ∀ {Γ x A} → Γ ⊢C → has-all-paths (x # A ∈ Γ)
  has-all-paths-∈ {Γ ∙ y # B} {x} {A} (cc Γ⊢ γ⊢A idp) (inl x∈Γ) (inl x∈'Γ) = ap inl (has-all-paths-∈ Γ⊢ x∈Γ x∈'Γ)
  has-all-paths-∈ {Γ ∙ y # B} {x} {A} (cc Γ⊢ γ⊢A idp) (inr (p , q)) (inr (p' , q')) = inr= (,= (is-prop-has-all-paths (eqdec-is-set eqdecℕ _ _) p p') (is-prop-has-all-paths (eqdec-is-set eqdec-Ty _ _) q q'))
  has-all-paths-∈ {Γ ∙ y # B} {x} {A} (cc Γ⊢ γ⊢A idp) (inl x∈Γ) (inr (idp , idp)) = ⊥-elim (lΓ∉Γ Γ⊢ x∈Γ)
  has-all-paths-∈ {Γ ∙ y # B} {x} {A} (cc Γ⊢ γ⊢A idp) (inr (idp , idp)) (inl x∈Γ) = ⊥-elim (lΓ∉Γ Γ⊢ x∈Γ)

  has-all-paths-⊢C : ∀ {Γ} → has-all-paths (Γ ⊢C)
  has-all-paths-⊢T : ∀ {Γ A} → has-all-paths (Γ ⊢T A)
  has-all-paths-⊢t : ∀ {Γ A t} → has-all-paths (Γ ⊢t t # A)
  has-all-paths-⊢S : ∀ {Δ Γ γ} → has-all-paths (Δ ⊢S γ > Γ)

  has-all-paths-⊢C {⊘} ec ec = idp
  has-all-paths-⊢C {Γ ∙ x # A} (cc Γ⊢ Γ⊢A p) (cc Γ⊢' Γ⊢'A q) = ap³ cc (has-all-paths-⊢C Γ⊢ Γ⊢') (has-all-paths-⊢T Γ⊢A Γ⊢'A) (is-prop-has-all-paths (eqdec-is-set (eqdecℕ) _ _) p q)

  has-all-paths-⊢T {Γ} {∗} (ob Γ⊢) (ob Γ⊢') = ap ob (has-all-paths-⊢C Γ⊢ Γ⊢')
  has-all-paths-⊢T {Γ} {⇒ A t u} (ar Γ⊢A Γ⊢t:A Γ⊢u:A) (ar Γ⊢'A Γ⊢'t:A Γ⊢'u:A) = ap³ ar (has-all-paths-⊢T Γ⊢A Γ⊢'A) (has-all-paths-⊢t Γ⊢t:A Γ⊢'t:A) (has-all-paths-⊢t Γ⊢u:A Γ⊢'u:A)

  has-all-paths-⊢t {Γ} {A} {Var x} (var Γ⊢ x∈Γ) (var Γ⊢' x∈'Γ) = ap² var (has-all-paths-⊢C Γ⊢ Γ⊢') (has-all-paths-∈ Γ⊢ x∈Γ x∈'Γ)
  has-all-paths-⊢t {Γ} {A} {Tm-constructor i γ} (tm Ci⊢Ti Γ⊢γ p) (tm Ci⊢'Ti Γ⊢'γ p') = ap³ tm (has-all-paths-⊢T Ci⊢Ti Ci⊢'Ti) (has-all-paths-⊢S Γ⊢γ Γ⊢'γ) (is-prop-has-all-paths (eqdec-is-set eqdec-Ty _ _) p p')

  has-all-paths-⊢S {Δ} {Γ} {<>} (es Δ⊢) (es Δ⊢')= ap es (has-all-paths-⊢C Δ⊢ Δ⊢')
  has-all-paths-⊢S {Δ} {Γ} {< γ , x ↦ t >} (sc Δ⊢γ Γ+⊢ Δ⊢t p) (sc Δ⊢'γ Γ+⊢' Δ⊢'t q) = ap⁴ sc (has-all-paths-⊢S Δ⊢γ Δ⊢'γ) (has-all-paths-⊢C Γ+⊢ Γ+⊢') (has-all-paths-⊢t Δ⊢t Δ⊢'t) (is-prop-has-all-paths (eqdec-is-set (eqdecℕ) _ _) p q)

  is-prop-⊢C : ∀ Γ → is-prop (Γ ⊢C)
  is-prop-⊢T : ∀ Γ A → is-prop (Γ ⊢T A)
  is-prop-⊢t : ∀ Γ A t → is-prop (Γ ⊢t t # A)
  is-prop-⊢S : ∀ Δ Γ γ → is-prop (Δ ⊢S γ > Γ)

  is-prop-⊢C Γ = has-all-paths-is-prop has-all-paths-⊢C
  is-prop-⊢T Γ A = has-all-paths-is-prop has-all-paths-⊢T
  is-prop-⊢t Γ A t = has-all-paths-is-prop has-all-paths-⊢t
  is-prop-⊢S Γ Δ γ = has-all-paths-is-prop has-all-paths-⊢S

  unique-type : ∀ {Γ t u A B} → (Γ ⊢t t # A) → (Γ ⊢t u # B) →  t == u → A == B
  unique-type (var (cc Γ⊢ _ idp) (inl a)) (var _ (inl b)) idp = unique-type (var Γ⊢ a) (var Γ⊢ b) idp
  unique-type (var (cc Γ⊢ _ idp) (inr (idp , _))) (var _ (inl l∈Γ)) idp = ⊥-elim (lΓ∉Γ Γ⊢ l∈Γ)
  unique-type (var (cc Γ⊢ _ idp) (inl l∈Γ)) (var _ (inr (idp , _))) idp = ⊥-elim (lΓ∉Γ Γ⊢ l∈Γ)
  unique-type (var (cc Γ⊢ _ idp) (inr (idp , idp))) (var _ (inr (idp , idp))) _ = idp
  unique-type (tm _ _ p) (tm _ _ q) idp = p >> (q ^)

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Raw.Construct.Never where

open import Cubical.Core.Everything

open import Cubical.Relation.Binary.Raw
open import Cubical.Relation.Binary.Raw.Construct.Constant
open import Cubical.Data.Empty.Polymorphic using (⊥)

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

Never : ∀ {a ℓ} {A : Type a} → RawRel A ℓ
Never = Const ⊥


text:
open import Relation.Binary.Core

module TreeSort.Impl1  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import BTree {A}
open import Data.List
open import Data.Sum

insert : A → BTree → BTree
insert x leaf = node x leaf leaf
insert x (node y l r)
    with tot≤ x y
... | inj₁ x≤y = node y (insert x l) r
... | inj₂ y≤x = node y l (insert x r)

treeSort : List A → BTree
treeSort [] = leaf
treeSort (x ∷ xs) = insert x (treeSort xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------------
-- Using setoids for formalizing FOTC
------------------------------------------------------------------------------

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

{-

From Peter emails:

At that time I was considering an inductive data type D and an
inductively defined equality on D. But I think what we are doing now
is better.

For =: The reason is that with the propositional identity we have
identity elimination which lets us replace equals by equals. We cannot
do that in general if we have setoid equality.

For D: the reason why I prefer to postulate D is that we have no use
for the inductive structure of D, and this inductive structure would
make e g 0 + 0 different from 0. So in that case we need setoid
equality.

-}

module FOTC where

module Aczel-CA where
  -- From Peter's slides
  -- http://www.cse.chalmers.se/~peterd/slides/Amagasaki.pdf

  -- We add 3 to the fixities of the Agda standard library 0.8.1 (see
  -- Algebra.agda and Relation/Binary/Core.agda).
  infixl 9 _·_
  infix  7 _≐_

  data D : Set where
    K S : D
    _·_ : D → D → D

  -- The setoid equality.
  data _≐_ : D → D → Set where
    ≐-refl  : ∀ {x} → x ≐ x
    ≐-sym   : ∀ {x y} → x ≐ y → y ≐ x
    ≐-trans : ∀ {x y z} → x ≐ y → y ≐ z → x ≐ z
    ≐-cong  : ∀ {x x' y y'} → x ≐ y → x' ≐ y' → x · x' ≐ y · y'
    K-eq    : ∀ x y → K · x · y ≐ x
    S-eq    : ∀ x y z → S · x · y · z ≐ x · z · (y · z)

  -- The identity type.
  data _≡_ (x : D) : D → Set where
    refl : x ≡ x

  ----------------------------------------------------------------------------
  -- 14 May 2012: Using the inductive structure we cannot prove
  --
  -- K · x · y ≡ x,
  --
  -- we need the setoid equality.
  -- K-eq : ∀ {x y} → (K · x · y) ≡ x

  ----------------------------------------------------------------------------
  -- 14 May 2012. We cannot define the identity elimination using the
  -- setoid equality.
  --
  -- Adapted from Peter's email:

  -- Given
  postulate ≐-subst : (A : D → Set) → ∀ {x y} → x ≐ y → A x → A y

  -- we can proof

  ≐→≡ : ∀ {x y} → x ≐ y → x ≡ y
  ≐→≡ {x} h = ≐-subst (λ z → x ≡ z) h refl

  -- but this doesn't hold because "x ≡ y" (propositional equality)
  -- means identical expressions. We do NOT have K · x · y ≡ x.
  --
  -- The point is that ≐ is a non-trivial equivalence relation, and
  -- not all properties preserve it. However, all properties are
  -- preserved by ≡.

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

module FOTC where

  infixl 9 _·_  -- The symbol is '\cdot'.
  infix  7 _≐_

  data D : Set where
    _·_ : D → D → D
    lam fix : (D → D) → D
    true false if zero succ pred iszero : D

  -- The setoid equality.
  data _≐_ : D → D → Set where
    ≐-refl   : ∀ {x} → x ≐ x
    ≐-sym    : ∀ {x y} → x ≐ y → y ≐ x
    ≐-trans  : ∀ {x y z} → x ≐ y → y ≐ z → x ≐ z
    ≐-cong   : ∀ {x₁ x₂ y₁ y₂} → x₁ ≐ y₁ → x₂ ≐ y₂ → x₁ · x₂ ≐ y₁ · y₂
    if-true  : ∀ t t' → if · true · t · t' ≐ t
    if-false : ∀ t t' → if · false · t · t' ≐ t'
    pred-0   : pred · zero ≐ zero
    pred-S   : ∀ n → pred · (succ · n) ≐ n
    iszero-0 : iszero · zero ≐ true
    iszero-S : ∀ n → iszero · (succ · n) ≐ false
    beta     : ∀ f a → lam f · a ≐ f a
    fix-eq   : ∀ f → fix f ≐ f (fix f)

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

module LeibnizEquality where

  infixl 9 _·_
  infix  7 _≡_

  data D : Set where
    _·_ : D → D → D
    lam fix : (D → D) → D
    true false if zero succ pred iszero : D

  -- (Barthe et al. 2003, p. 262) use the Leibniz equality when
  -- they talk about setoids.

  -- Using the Leibniz equality (adapted from
  -- Agda/examples/lib/Logic/Leibniz.agda)

  _≡_ : D → D → Set₁
  x ≡ y = (A : D → Set) → A x → A y

  -- we can prove the setoids properties

  refl : ∀ x → x ≡ x
  refl x A Ax = Ax

  sym : ∀ {x y} → x ≡ y → y ≡ x
  sym {x} h A Ay = h (λ z → A z → A x) (λ Ax → Ax) Ay

  trans : ∀ x y z → x ≡ y → y ≡ z → x ≡ z
  trans x y z h₁ h₂ A Ax = h₂ A (h₁ A Ax)

  -- and the identity elimination

  subst : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y
  subst A h = h A

  -- and the congruency

  cong  : ∀ {x x' y y'} → x ≡ x' → y ≡ y' → x · y ≡ x' · y'
  cong {x} {x'} {y} {y'} h₁ h₂ A Axx' =
    h₂ (λ z → A (x' · z)) (h₁ (λ z → A (z · y)) Axx')

------------------------------------------------------------------------------
-- References
--
-- Barthe, Gilles, Capretta, Venanzio and Pons, Olivier
-- (2003). Setoids in type theory. Journal of Functional Programming
-- 13.2, pp. 261–293.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- Restricted hypotheses
------------------------------------------------------------------------

-- A restricted hypothesis is a hypothesis where both types are
-- sub/terms/ of either one of two given types.

open import RecursiveTypes.Syntax

module RecursiveTypes.Subterm.RestrictedHypothesis
         {n} (χ₁ χ₂ : Ty n) where

open import Category.Monad
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (module Inverse)
open import Data.List as List
open import Data.List.Relation.Unary.Any as Any
open import Data.List.Relation.Unary.Any.Properties
import Data.List.Categorical
import Data.List.Countdown as Countdown
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional.Properties
import Data.List.Membership.Setoid
open import Data.Product as Prod
open import Data.Sum as Sum
open import Level
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary.Construct.On as On
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)

open RawMonad (Data.List.Categorical.monad {ℓ = zero})

open import RecursiveTypes.Subterm as ST using (_⊑_; _∗)

------------------------------------------------------------------------
-- Restricted hypotheses

-- Types which are subterms of either χ₁ or χ₂.

Subterm : Ty n → Set
Subterm σ = σ ⊑ χ₁ ⊎ σ ⊑ χ₂

-- The Subterm predicate is anti-monotone.

anti-mono : ∀ {σ₁ σ₂} → σ₂ ⊑ σ₁ → Subterm σ₁ → Subterm σ₂
anti-mono σ₂⊑σ₁ = Sum.map (ST.trans σ₂⊑σ₁) (ST.trans σ₂⊑σ₁)

-- Hypotheses where both types are subterms.

RestrictedHyp : Set
RestrictedHyp = ∃ Subterm × ∃ Subterm

-- Computes the underlying hypothesis/es.

⟨_⟩ : RestrictedHyp → Hyp n
⟨_⟩ = Prod.map proj₁ proj₁

⟨_⟩⋆ : List RestrictedHyp → List (Hyp n)
⟨_⟩⋆ = List.map ⟨_⟩

-- Equality of restricted hypotheses (ignores the subterm proofs).

_≈_ : Rel RestrictedHyp zero
_≈_ = _≡_ on ⟨_⟩

-- List membership relation for restricted hypotheses.

open Data.List.Membership.Setoid
       (record { isEquivalence =
                   On.isEquivalence (⟨_⟩) PropEq.isEquivalence })
  using () renaming (_∈_ to _⟨∈⟩_)

------------------------------------------------------------------------
-- Computing all possible restricted hypotheses

-- Computes all the subterms of the given type.

subtermsOf : ∀ τ → (∀ {σ} → σ ⊑ τ → Subterm σ) → List (∃ Subterm)
subtermsOf τ f = List.map (Prod.map id f) (ST.subtermsOf τ)

subtermsOf-complete :
  ∀ {τ} (f : ∀ {σ} → σ ⊑ τ → Subterm σ) {σ} →
  σ ⊑ τ → ∃ λ σ⊑τ → (σ , f σ⊑τ) ∈ subtermsOf τ f
subtermsOf-complete f σ⊑τ =
  Prod.map id (λ ∈ → Inverse.to (map-∈↔ _) ⟨$⟩ (_ , ∈ , refl)) $
    ST.subtermsOf-complete σ⊑τ

subtermsOf²-complete :
  ∀ {σ₁ τ₁ σ₂ τ₂}
  (f : ∀ {σ} → σ ⊑ τ₁ → Subterm σ)
  (g : ∀ {σ} → σ ⊑ τ₂ → Subterm σ) →
  (σ₁⊑τ₁ : σ₁ ⊑ τ₁) (σ₂⊑τ₂ : σ₂ ⊑ τ₂) →
  ((σ₁ , f σ₁⊑τ₁) ≲ (σ₂ , g σ₂⊑τ₂)) ⟨∈⟩
    (subtermsOf τ₁ f ⊗ subtermsOf τ₂ g)
subtermsOf²-complete f g σ₁⊑τ₁ σ₂⊑τ₂ =
  Any.map (PropEq.cong $ Prod.map proj₁ proj₁) $
    Inverse.to ⊗-∈↔ ⟨$⟩
      ( proj₂ (subtermsOf-complete f σ₁⊑τ₁)
      , proj₂ (subtermsOf-complete g σ₂⊑τ₂)
      )

-- All subterms of χ₁.

⊑-χ₁ : List (∃ Subterm)
⊑-χ₁ = subtermsOf χ₁ inj₁

-- All subterms of χ₂.

⊑-χ₂ : List (∃ Subterm)
⊑-χ₂ = subtermsOf χ₂ inj₂

-- All possible restricted hypotheses.

restrictedHyps : List RestrictedHyp
restrictedHyps = (⊑-χ₁ ⊗ ⊑-χ₂) ++ (⊑-χ₂ ⊗ ⊑-χ₁) ++
                 (⊑-χ₁ ⊗ ⊑-χ₁) ++ (⊑-χ₂ ⊗ ⊑-χ₂)

complete : ∀ h → h ⟨∈⟩ restrictedHyps
complete ((σ , inj₁ σ⊑χ₁) ≲ (τ , inj₂ τ⊑χ₂)) =
  Inverse.to ++↔ ⟨$⟩ (inj₁ $
  subtermsOf²-complete inj₁ inj₂ σ⊑χ₁ τ⊑χ₂)
complete ((σ , inj₂ σ⊑χ₂) ≲ (τ , inj₁ τ⊑χ₁)) =
  Inverse.to (++↔ {xs = ⊑-χ₁ ⊗ ⊑-χ₂}) ⟨$⟩ (inj₂ $
  Inverse.to ++↔                      ⟨$⟩ (inj₁ $
  subtermsOf²-complete inj₂ inj₁ σ⊑χ₂ τ⊑χ₁))
complete ((σ , inj₁ σ⊑χ₁) ≲ (τ , inj₁ τ⊑χ₁)) =
  Inverse.to (++↔ {xs = ⊑-χ₁ ⊗ ⊑-χ₂}) ⟨$⟩ (inj₂ $
  Inverse.to (++↔ {xs = ⊑-χ₂ ⊗ ⊑-χ₁}) ⟨$⟩ (inj₂ $
  Inverse.to ++↔                      ⟨$⟩ (inj₁ $
  subtermsOf²-complete inj₁ inj₁ σ⊑χ₁ τ⊑χ₁)))
complete ((σ , inj₂ σ⊑χ₂) ≲ (τ , inj₂ τ⊑χ₂)) =
  Inverse.to (++↔ {xs = ⊑-χ₁ ⊗ ⊑-χ₂}) ⟨$⟩ (inj₂ $
  Inverse.to (++↔ {xs = ⊑-χ₂ ⊗ ⊑-χ₁}) ⟨$⟩ (inj₂ $
  Inverse.to (++↔ {xs = ⊑-χ₁ ⊗ ⊑-χ₁}) ⟨$⟩ (inj₂ $
  subtermsOf²-complete inj₂ inj₂ σ⊑χ₂ τ⊑χ₂)))

------------------------------------------------------------------------
-- A countdown structure for restricted hypotheses

-- Equality of restricted hypotheses can be decided.

_≟_ : Decidable (_≡_ {A = Hyp n})
( σ₁ ≲  σ₂) ≟ (τ₁ ≲ τ₂) with σ₁ ≡? τ₁ | σ₂ ≡? τ₂
(.τ₁ ≲ .τ₂) ≟ (τ₁ ≲ τ₂) | yes refl | yes refl = yes refl
... | no σ₁≢τ₁ | _ = no (σ₁≢τ₁ ∘ PropEq.cong proj₁)
... | _ | no σ₂≢τ₂ = no (σ₂≢τ₂ ∘ PropEq.cong proj₂)

isDecEquivalence : IsDecEquivalence _≈_
isDecEquivalence =
  On.isDecEquivalence ⟨_⟩ $
    DecSetoid.isDecEquivalence (PropEq.decSetoid _≟_)

-- The countdown data structure can be used to keep track of (an upper
-- bound of) the number of hypotheses which have not been inserted
-- into a given list of hypotheses yet.

private
  open module C =
    Countdown (record { isDecEquivalence = isDecEquivalence })
    public hiding (empty; emptyFromList)

-- An initialised countdown structure.

empty : [] ⊕ length restrictedHyps
empty = C.emptyFromList restrictedHyps complete

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
------------------------------------------------------------------------
-- Monads
------------------------------------------------------------------------

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

open import Equality

module Monad
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Function-universe eq using (inverse)

------------------------------------------------------------------------
-- Basic definitions

-- Raw monads and raw monad transformers.

open import Monad.Raw public

-- Monads.

record Monad {d c} (M : Type d → Type c) : Type (lsuc d ⊔ c) where
  constructor mk
  field
    ⦃ raw-monad ⦄  : Raw-monad M

    left-identity  : ∀ {A B} (x : A) (f : A → M B) →
                     return x >>= f ≡ f x
    right-identity : ∀ {A} (x : M A) →
                     x >>= return ≡ x
    associativity  : ∀ {A B C} →
                     (x : M A) (f : A → M B) (g : B → M C) →
                     x >>= (λ x → f x >>= g) ≡ x >>= f >>= g

  -- Monads are functors.

  map-id : ∀ {A} (x : M A) → map id x ≡ x
  map-id x =
    x >>= return ∘ id  ≡⟨⟩
    x >>= return       ≡⟨ right-identity _ ⟩∎
    x                  ∎

  map-∘ : Extensionality d c →
          ∀ {A B C} (f : B → C) (g : A → B) (x : M A) →
          map (f ∘ g) x ≡ map f (map g x)
  map-∘ ext f g x =
    x >>= return ∘ (f ∘ g)                     ≡⟨ cong (x >>=_) (apply-ext ext λ _ → sym $ left-identity _ _) ⟩
    x >>= (λ x → return (g x) >>= return ∘ f)  ≡⟨ associativity _ _ _ ⟩∎
    (x >>= return ∘ g) >>= return ∘ f          ∎

  -- More lemmas.

  map-return : ∀ {A B} (f : A → B) (x : A) →
               map {M = M} f (return x) ≡ return (f x)
  map-return f x =
    return x >>= return ∘ f  ≡⟨ left-identity _ _ ⟩∎
    return (f x)             ∎

  map->>= : ∀ {A B C} (f : B → C) (x : M A) (g : A → M B) →
            map f (x >>= g) ≡ x >>= map f ∘ g
  map->>= f x g =
    x >>= g >>= return ∘ f            ≡⟨ sym $ associativity _ _ _ ⟩
    x >>= (λ x → g x >>= return ∘ f)  ≡⟨⟩
    x >>= (λ x → map f (g x))         ≡⟨ refl _ ⟩∎
    x >>= map f ∘ g                   ∎

  >>=-map : Extensionality d c →
            ∀ {A B C} (f : A → B) (x : M A) (g : B → M C) →
            map f x >>= g ≡ x >>= g ∘ f
  >>=-map ext f x g =
    (x >>= return ∘ f) >>= g          ≡⟨ sym $ associativity _ _ _ ⟩
    x >>= (λ x → return (f x) >>= g)  ≡⟨ cong (x >>=_) (apply-ext ext λ _ → left-identity _ _) ⟩∎
    x >>= g ∘ f                       ∎

open Monad ⦃ … ⦄ public hiding (raw-monad)

-- Monad transformers.

record Monad-transformer
         {d c₁ c₂} (F : (Type d → Type c₁) → (Type d → Type c₂)) :
         Type (lsuc (c₁ ⊔ d) ⊔ c₂) where
  constructor mk
  field
    transform : ∀ {M}   ⦃ is-monad : Monad M ⦄ → Monad (F M)
    liftᵐ     : ∀ {M A} ⦃ is-monad : Monad M ⦄ → M A → F M A

    lift-return :
      ∀ {M A} ⦃ is-monad : Monad M ⦄ (x : A) →
      let module M = Raw-monad (Monad.raw-monad transform) in
      liftᵐ {M = M} (return x) ≡ M.return x

    lift->>= :
      ∀ {M A B} ⦃ is-monad : Monad M ⦄
      (x : M A) (f : A → M B) →
      let module M = Raw-monad (Monad.raw-monad transform) in
      liftᵐ (x >>= f) ≡ liftᵐ x M.>>= liftᵐ ∘ f

open Monad-transformer ⦃ … ⦄ public using (liftᵐ; lift-return; lift->>=)

------------------------------------------------------------------------
-- Preservation lemmas

-- If F and G are pointwise logically equivalent, then Raw-monad F and
-- Raw-monad G are logically equivalent.

⇔→raw⇔raw : ∀ {a f g} {F : Type a → Type f} {G : Type a → Type g} →
            (∀ x → F x ⇔ G x) → Raw-monad F ⇔ Raw-monad G
⇔→raw⇔raw {a} = λ F⇔G → record
  { to   = to F⇔G
  ; from = to (inverse ∘ F⇔G)
  }
  where
  to : ∀ {f g} {F : Type a → Type f} {G : Type a → Type g} →
       (∀ x → F x ⇔ G x) → Raw-monad F → Raw-monad G
  Raw-monad.return (to F⇔G F-monad) x =
    _⇔_.to (F⇔G _) (F.return x)
    where
    module F = Raw-monad F-monad

  Raw-monad._>>=_ (to F⇔G F-monad) x f =
    _⇔_.to (F⇔G _) (_⇔_.from (F⇔G _) x F.>>= λ x →
                    _⇔_.from (F⇔G _) (f x))
    where
    module F = Raw-monad F-monad

-- If F and G are pointwise isomorphic, then Raw-monad F and
-- Raw-monad G are isomorphic (assuming extensionality).

↔→raw↔raw : ∀ {a f g} →
            Extensionality (lsuc a ⊔ f ⊔ g) (lsuc a ⊔ f ⊔ g) →
            {F : Type a → Type f} {G : Type a → Type g} →
            (∀ x → F x ↔ G x) → Raw-monad F ↔ Raw-monad G
↔→raw↔raw {a} {f} {g} = λ ext F↔G → record
  { surjection = record
    { logical-equivalence = ⇔→raw⇔raw (_↔_.logical-equivalence ∘ F↔G)
    ; right-inverse-of    = to∘to (lower-extensionality f f ext)
                                  (inverse ∘ F↔G)
    }
  ; left-inverse-of = to∘to (lower-extensionality g g ext) F↔G
  }
  where
  to∘to :
    ∀ {f g} {F : Type a → Type f} {G : Type a → Type g} →
    Extensionality (lsuc a ⊔ f) (lsuc a ⊔ f) →
    (F↔G : ∀ x → F x ↔ G x) (F-monad : Raw-monad F) →
    let eq = ⇔→raw⇔raw (_↔_.logical-equivalence ∘ F↔G) in
    _⇔_.from eq (_⇔_.to eq F-monad) ≡ F-monad
  to∘to {f} ext F↔G (mk return _>>=_) = cong₂ mk
    (implicit-extensionality (lower-extensionality f (lsuc a) ext) λ _ →
     apply-ext (lower-extensionality _ (lsuc a) ext) λ x →

       _↔_.from (F↔G _) (_↔_.to (F↔G _) (return x))  ≡⟨ _↔_.left-inverse-of (F↔G _) _ ⟩∎
       return x                                      ∎)

    (implicit-extensionality (lower-extensionality f lzero    ext) λ _ →
     implicit-extensionality (lower-extensionality f (lsuc a) ext) λ _ →
     apply-ext (lower-extensionality (lsuc a) (lsuc a) ext) λ x →
     apply-ext (lower-extensionality (lsuc a) (lsuc a) ext) λ f →

       _↔_.from (F↔G _) (_↔_.to (F↔G _)
         (_↔_.from (F↔G _) (_↔_.to (F↔G _) x) >>= λ x →
          _↔_.from (F↔G _) (_↔_.to (F↔G _) (f x))))      ≡⟨ _↔_.left-inverse-of (F↔G _) _ ⟩

       (_↔_.from (F↔G _) (_↔_.to (F↔G _) x) >>= λ x →
        _↔_.from (F↔G _) (_↔_.to (F↔G _) (f x)))         ≡⟨ cong₂ _>>=_ (_↔_.left-inverse-of (F↔G _) _)
                                                                        (apply-ext (lower-extensionality _ (lsuc a) ext) λ _ →
                                                                         _↔_.left-inverse-of (F↔G _) _) ⟩∎
       x >>= f                                           ∎)

-- If F and G are pointwise isomorphic, then Monad F and Monad G are
-- logically equivalent (assuming extensionality).

↔→⇔ : ∀ {a f g} →
      Extensionality a (f ⊔ g) →
      {F : Type a → Type f} {G : Type a → Type g} →
      (∀ x → F x ↔ G x) → Monad F ⇔ Monad G
↔→⇔ {a} {f} {g} = λ ext F↔G → record
  { to   = to (lower-extensionality lzero g ext) F↔G
  ; from = to (lower-extensionality lzero f ext) (inverse ∘ F↔G)
  }
  where
  to : ∀ {f g} {F : Type a → Type f} {G : Type a → Type g} →
       Extensionality a f →
       (∀ x → F x ↔ G x) → Monad F → Monad G
  Monad.raw-monad (to ext F↔G F-monad) =
    _⇔_.to (⇔→raw⇔raw (_↔_.logical-equivalence ∘ F↔G)) F.raw-monad
    where
    module F = Monad F-monad

  Monad.left-identity (to ext F↔G F-monad) x f =
    _↔_.to (F↔G _)
      (_↔_.from (F↔G _) (_↔_.to (F↔G _) (FR.return x)) FR.>>= λ x →
       _↔_.from (F↔G _) (f x))                                        ≡⟨ cong (λ y → _↔_.to (F↔G _) (y FR.>>= _)) (_↔_.left-inverse-of (F↔G _) _) ⟩

    _↔_.to (F↔G _) (FR.return x FR.>>= λ x → _↔_.from (F↔G _) (f x))  ≡⟨ cong (_↔_.to (F↔G _)) (FM.left-identity _ _) ⟩

    _↔_.to (F↔G _) (_↔_.from (F↔G _) (f x))                           ≡⟨ _↔_.right-inverse-of (F↔G _) _ ⟩∎

    f x                                                               ∎
    where
    module FM = Monad F-monad
    module FR = Raw-monad FM.raw-monad

  Monad.right-identity (to ext F↔G F-monad) x =
    _↔_.to (F↔G _) (_↔_.from (F↔G _) x FR.>>= λ x →
                    _↔_.from (F↔G _) (_↔_.to (F↔G _) (FR.return x)))  ≡⟨ cong (λ g → _↔_.to (F↔G _) (_ FR.>>= g))
                                                                              (apply-ext ext λ _ → _↔_.left-inverse-of (F↔G _) _) ⟩
    _↔_.to (F↔G _) (_↔_.from (F↔G _) x FR.>>= FR.return)              ≡⟨ cong (_↔_.to (F↔G _)) (FM.right-identity _) ⟩

    _↔_.to (F↔G _) (_↔_.from (F↔G _) x)                               ≡⟨ _↔_.right-inverse-of (F↔G _) _ ⟩∎

    x                                                                 ∎
    where
    module FM = Monad F-monad
    module FR = Raw-monad FM.raw-monad

  Monad.associativity (to ext F↔G F-monad) x f g =
    _↔_.to (F↔G _)
      (_↔_.from (F↔G _) x FR.>>= λ x →
       _↔_.from (F↔G _) (_↔_.to (F↔G _)
         (_↔_.from (F↔G _) (f x) FR.>>= λ x → _↔_.from (F↔G _) (g x))))  ≡⟨ cong (λ g → _↔_.to (F↔G _) (_↔_.from (F↔G _) x FR.>>= g))
                                                                                (apply-ext ext λ _ → _↔_.left-inverse-of (F↔G _) _) ⟩
    _↔_.to (F↔G _)
      (_↔_.from (F↔G _) x FR.>>= λ x →
       _↔_.from (F↔G _) (f x) FR.>>= λ x → _↔_.from (F↔G _) (g x))       ≡⟨ cong (_↔_.to (F↔G _)) (FM.associativity _ _ _) ⟩

    _↔_.to (F↔G _)
      ((_↔_.from (F↔G _) x FR.>>= λ x →
        _↔_.from (F↔G _) (f x)) FR.>>= λ x →
       _↔_.from (F↔G _) (g x))                                           ≡⟨ cong (λ y → _↔_.to (F↔G _) (y FR.>>= _))
                                                                                (sym $ _↔_.left-inverse-of (F↔G _) _) ⟩∎
    _↔_.to (F↔G _)
      (_↔_.from (F↔G _) (_↔_.to (F↔G _)
         (_↔_.from (F↔G _) x FR.>>= λ x →
          _↔_.from (F↔G _) (f x))) FR.>>= λ x →
       _↔_.from (F↔G _) (g x))                                           ∎
    where
    module FM = Monad F-monad
    module FR = Raw-monad FM.raw-monad

------------------------------------------------------------------------
-- Identity monads

-- The identity monad.

identity-monad : ∀ {ℓ} → Monad {d = ℓ} id
Raw-monad.return (Monad.raw-monad identity-monad) x   = x
Raw-monad._>>=_  (Monad.raw-monad identity-monad) x f = f x
Monad.left-identity  identity-monad x f               = refl (f x)
Monad.right-identity identity-monad x                 = refl x
Monad.associativity  identity-monad x f g             = refl (g (f x))

-- The identity monad, defined using a wrapper type to make instance
-- resolution easier.

record Id {a} (A : Type a) : Type a where
  constructor wrap
  field
    run : A

open Id public

instance

  Id-raw-monad : ∀ {ℓ} → Raw-monad {d = ℓ} Id
  run (Raw-monad.return Id-raw-monad x)   = x
  run (Raw-monad._>>=_  Id-raw-monad x f) = run (f (run x))

  Id-monad : ∀ {ℓ} → Monad {d = ℓ} Id
  Monad.raw-monad      Id-monad       = Id-raw-monad
  Monad.left-identity  Id-monad x f   = cong wrap (refl (run (f x)))
  Monad.right-identity Id-monad x     = cong wrap (refl (run x))
  Monad.associativity  Id-monad x f g = cong wrap (refl (run (g (run (f (run x))))))

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Structure.Operator where

import Lvl
open import Functional using (_$_)
open import Lang.Instance
open import Logic.Predicate
open import Logic
open import Structure.Setoid
open import Structure.Function.Names
open import Structure.Function
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₒ ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₒ₄ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ ℓₗ₄ : Lvl.Level
private variable A₁ A₂ A₃ B : Type{ℓ}

module _
  ⦃ equiv-A₁ : Equiv{ℓₗ₁}(A₁) ⦄
  ⦃ equiv-A₂ : Equiv{ℓₗ₂}(A₂) ⦄
  ⦃ equiv-B : Equiv{ℓₗ₃}(B) ⦄
  (_▫_ : A₁ → A₂ → B)
  where

  -- The operator `_▫_` "(behaves like)/is a function" in the context of `_≡_` from the Equiv instance.
  -- `congruence` is the defining property of a binary operation.
  record BinaryOperator : Type{Lvl.of(A₁) Lvl.⊔ Lvl.of(A₂) Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓₗ₃} where
    constructor intro
    field congruence : Congruence₂(_▫_)

    instance
      left : ∀{x} → Function(_▫ x)
      left = intro(proof ↦ congruence proof (reflexivity(_≡_)))

    instance
      right : ∀{x} → Function(x ▫_)
      right = intro(proof ↦ congruence (reflexivity(_≡_)) proof)

    congruenceₗ : ∀{x₁ x₂}{y} → (x₁ ≡ x₂) → (x₁ ▫ y ≡ x₂ ▫ y)
    congruenceₗ = Function.congruence(left)

    congruenceᵣ : ∀{x}{y₁ y₂} → (y₁ ≡ y₂) → (x ▫ y₁ ≡ x ▫ y₂)
    congruenceᵣ = Function.congruence(right)

  [≡]-congruence2-left : ⦃ inst : BinaryOperator ⦄ → (x : _) → Function(_▫ x)
  [≡]-congruence2-left = x ↦ inst-fn(BinaryOperator.left) {x}

  [≡]-congruence2-right : ⦃ inst : BinaryOperator ⦄ → (x : _) → Function(x ▫_)
  [≡]-congruence2-right = x ↦ inst-fn(BinaryOperator.right) {x}

  congruence₂ = inst-fn BinaryOperator.congruence

  congruence₂ₗ : ⦃ inst : BinaryOperator ⦄ → (a : A₂) → ∀{x y : A₁} → (x ≡ y) → (x ▫ a ≡ y ▫ a)
  congruence₂ₗ _ = inst-fn BinaryOperator.congruenceₗ -- (congruence₁(_▫ a) ⦃ [≡]-congruence2-left ⦃ inst ⦄ a ⦄)

  congruence₂ᵣ : ⦃ inst : BinaryOperator ⦄ → (a : A₁) → ∀{x y : A₂} → (x ≡ y) → (a ▫ x ≡ a ▫ y)
  congruence₂ᵣ _ = inst-fn BinaryOperator.congruenceᵣ

  functions-to-binaryOperator : ⦃ l : ∀{y} → Function(_▫ y) ⦄ ⦃ r : ∀{x} → Function(x ▫_) ⦄ → BinaryOperator
  BinaryOperator.congruence functions-to-binaryOperator {x₁} {y₁} {x₂} {y₂} leq req =
    (x₁ ▫ x₂) 🝖[ _≡_ ]-[ congruence₁(_▫ x₂) leq ]
    (y₁ ▫ x₂) 🝖[ _≡_ ]-[ congruence₁(y₁ ▫_) req ]
    (y₁ ▫ y₂) 🝖-end

module _
  ⦃ equiv-A₁ : Equiv{ℓₗ₁}(A₁) ⦄
  ⦃ equiv-A₂ : Equiv{ℓₗ₂}(A₂) ⦄
  ⦃ equiv-A₃ : Equiv{ℓₗ₃}(A₃) ⦄
  ⦃ equiv-B : Equiv{ℓₗ₄}(B) ⦄
  (_▫_▫_ : A₁ → A₂ → A₃ → B)
  where

  record TrinaryOperator : Type{Lvl.of(A₁) Lvl.⊔ Lvl.of(A₂) Lvl.⊔ Lvl.of(A₃) Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓₗ₃ Lvl.⊔ ℓₗ₄} where
    constructor intro
    field congruence : Congruence₃(_▫_▫_)

  congruence₃ = inst-fn TrinaryOperator.congruence


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

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data ⊥ : Set where

record Σ {a} {b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

no : _≡_ {A = Σ Set (λ X → X)} (Nat , 0) (Nat , 1) → ⊥
no ()


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties for Conats
------------------------------------------------------------------------

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

module Codata.Conat.Properties where

open import Data.Nat
open import Codata.Thunk
open import Codata.Conat
open import Codata.Conat.Bisimilarity
open import Function
open import Relation.Nullary
open import Relation.Binary

sℕ≤s⁻¹ : ∀ {m n} → suc m ℕ≤ suc n → m ℕ≤ n .force
sℕ≤s⁻¹ (sℕ≤s p) = p

_ℕ≤?_ : Decidable _ℕ≤_
zero  ℕ≤? n       = yes zℕ≤n
suc m ℕ≤? zero    = no (λ ())
suc m ℕ≤? suc n with m ℕ≤? n .force
... | yes p = yes (sℕ≤s p)
... | no ¬p = no (¬p ∘′ sℕ≤s⁻¹)

0ℕ+-identity : ∀ {i n} → i ⊢ 0 ℕ+ n ≈ n
0ℕ+-identity = refl

+ℕ0-identity : ∀ {i n} → i ⊢ n +ℕ 0 ≈ n
+ℕ0-identity {n = zero}  = zero
+ℕ0-identity {n = suc n} = suc λ where .force → +ℕ0-identity


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Nat
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.Data.Prod

open import Cubical.Algebra
open import Cubical.Algebra.Properties
open import Cubical.Algebra.Monoid.Morphism

open import Cubical.Algebra.Semigroup.Properties as Semigroup using (isPropIsSemigroup)

open import Cubical.Relation.Binary.Reasoning.Equality
open import Cubical.Relation.Unary as Unary
open import Cubical.Relation.Binary as Binary

open import Cubical.Algebra.Monoid.MorphismProperties public
  using (MonoidPath; uaMonoid; carac-uaMonoid; Monoid≡; caracMonoid≡)

private
  variable
    ℓ : Level

isPropIsMonoid : ∀ {M : Type ℓ} {_•_ ε} → isProp (IsMonoid M _•_ ε)
isPropIsMonoid {_} {_} {_•_} {ε} (ismonoid aSemi aId) (ismonoid bSemi bId) =
  cong₂ ismonoid (isPropIsSemigroup aSemi bSemi) (isPropIdentity (IsSemigroup.is-set aSemi) _•_ ε aId bId)

module MonoidLemmas (M : Monoid ℓ) where
  open Monoid M

  ε-comm : ∀ x → x • ε ≡ ε • x
  ε-comm x = identityʳ x ∙ sym (identityˡ x)

  ^-zeroˡ : LeftZero ε _^_
  ^-zeroˡ zero    = refl
  ^-zeroˡ (suc n) = identityˡ (ε ^ n) ∙ ^-zeroˡ n

  ^-suc : ∀ x n → x ^ suc n ≡ x ^ n • x
  ^-suc x zero    = ε-comm x
  ^-suc x (suc n) =
    x ^ suc (suc n) ≡⟨⟩
    x • x ^ suc n   ≡⟨ cong (x •_) (^-suc x n) ⟩
    x • (x ^ n • x) ≡˘⟨ assoc x (x ^ n) x ⟩
    x • x ^ n • x   ≡⟨⟩
    x ^ suc n • x   ∎

  ^-plus : ∀ x → Homomorphic₂ (x ^_) _+_ _•_
  ^-plus x zero    n = sym (identityˡ (x ^ n))
  ^-plus x (suc m) n =
    x ^ (suc m + n)     ≡⟨⟩
    x • x ^ (m + n)     ≡⟨ cong (x •_) (^-plus x m n) ⟩
    x • (x ^ m • x ^ n) ≡˘⟨ assoc x (x ^ m) (x ^ n) ⟩
    x • x ^ m • x ^ n   ≡⟨⟩
    x ^ suc m • x ^ n   ∎

  infixl 10 _^′_
  _^′_ = Semigroup._^_ semigroup

  ^semi≡^ : ∀ x n → x ^′ n ≡ x ^ (ℕ₊₁→ℕ n)
  ^semi≡^ x one    = sym (identityʳ x)
  ^semi≡^ x (2+ n) = cong (x •_) (^semi≡^ x (1+ n))

-- Invertible elements
module Invertible (M : Monoid ℓ) where
  open Monoid M

  Inverses′ : RawRel ⟨ M ⟩ ℓ
  Inverses′ x y = (x • y ≡ ε) × (y • x ≡ ε)

  isPropInverses : Binary.isPropValued Inverses′
  isPropInverses _ _ = isPropProd (is-set _ _) (is-set _ _)

  Inverses : Rel ⟨ M ⟩ ℓ
  Inverses = Binary.fromRaw Inverses′ isPropInverses

  inv-unique′ : ∀ {x y z} → x • y ≡ ε → z • x ≡ ε → y ≡ z
  inv-unique′ {x} {y} {z} xy≡ε zx≡ε =
    y           ≡˘⟨ identityˡ y ⟩
    ε • y       ≡˘⟨ cong (_• y) zx≡ε ⟩
    (z • x) • y ≡⟨ assoc z x y ⟩
    z • (x • y) ≡⟨ cong (z •_) xy≡ε ⟩
    z • ε       ≡⟨ identityʳ z ⟩
    z           ∎

  inv-unique : ∀ {x y z} → ⟨ Inverses x y ⟩ → ⟨ Inverses x z ⟩ → y ≡ z
  inv-unique (xy≡ε , _) (_ , zx≡ε) = inv-unique′ xy≡ε zx≡ε

  Invertible′ : RawPred ⟨ M ⟩ ℓ
  Invertible′ x = Σ ⟨ M ⟩ (Inverses′ x)

  isPropInvertible : Unary.isPropValued Invertible′
  isPropInvertible x (y , x-y) (z , x-z) = ΣPathTransport→PathΣ (y , x-y) (z , x-z)
                                          (inv-unique x-y x-z , isPropInverses _ _ _ _)

  Invertible : Pred ⟨ M ⟩ ℓ
  Invertible = Unary.fromRaw Invertible′ isPropInvertible

  εInverses : ⟨ Inverses ε ε ⟩
  εInverses = identityˡ ε , identityˡ ε

  εInvertible : ε ∈ Invertible
  εInvertible = ε , εInverses

module Kernel {ℓ ℓ′} {M : Monoid ℓ} {N : Monoid ℓ′} (hom : MonoidHom M N)
  = Semigroup.Kernel (MonoidHom→SemigroupHom hom)


text:
-- Andreas, 2017-05-13, issue reported by nad

module Issue2579 where

open import Common.Bool

open import Issue2579.Import
import Issue2579.Instance Bool true  -- imports instances

theWrapped : {{w : Wrap Bool}} → Bool
theWrapped {{w}} = Wrap.wrapped w

test : Bool
test = theWrapped

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2013-03-22
-- cut down from  https://github.com/agda/agda-assoc-free/src/AssocFree/DList.agda
-- {-# OPTIONS -v tc.cover.splittree:10 -v tc.cc:30 #-}
module Issue827 where

open import Common.Equality

-- need to keep this record !
record List (A : Set) : Set where
  constructor list -- need to keep this constructor
  field bla : A

postulate
  _++_ : ∀ {A} → List A → List A → List A
  _∈_  : ∀ {A} (a : A) (as : List A) → Set
  _≪_ : ∀ {A} {a : A} {as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
  _≫_ : ∀ {A} {a : A} as {bs} → (a ∈ bs) → (a ∈ (as ++ bs))

-- Case on membership

data Case {A} a (as bs : List A) : Set where
  inj₁ : (a∈as : a ∈ as) → Case a as bs
  inj₂ : (a∈bs : a ∈ bs) → Case a as bs

-- Three-way case, used for proving associativity properties

data Case₃ {A} (a : A) as bs cs : Set where
  inj₁ : (a ∈ as) → Case₃ a as bs cs
  inj₂ : (a ∈ bs) → Case₃ a as bs cs
  inj₃ : (a ∈ cs) → Case₃ a as bs cs

-- Associating case₃ to the right gives case

case : ∀ {A} {a : A} {as bs cs} → Case₃ a as bs cs → Case a as (bs ++ cs)
case {cs = cs} (inj₂ a∈bs) = inj₂ (a∈bs ≪ cs)
case {bs = bs} (inj₃ a∈cs) = inj₂ (bs ≫ a∈cs)
case           (inj₁ a∈as) = inj₁ a∈as

works : ∀ {A} {a : A} {as bs cs : List A} {a∈bs : a ∈ bs} →
  case {as = as} (inj₂ a∈bs) ≡ inj₂ (a∈bs ≪ cs)
works = refl

-- Different order of clauses fails:

case′ : ∀ {A} {a : A} {as bs cs} → Case₃ a as bs cs → Case a as (bs ++ cs)
case′           (inj₁ a∈as) = inj₁ a∈as
case′ {cs = cs} (inj₂ a∈bs) = inj₂ (a∈bs ≪ cs)
case′ {bs = bs} (inj₃ a∈cs) = inj₂ (bs ≫ a∈cs)

fails : ∀ {A} {a : A} {as bs cs : List A} {a∈bs : a ∈ bs} →
  case′ {as = as} (inj₂ a∈bs) ≡ inj₂ (a∈bs ≪ cs)
fails = refl

-- There was a bug in the record pattern translation.
-- Solution: expand all catch-alls in position of a record
-- pattern split.  Then record pattern translation works fine.


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Constructions.Initial where

open import Data.Product using (proj₁ ; proj₂)
open import Level

open import Cats.Category.Base

import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Constructions.Unique as Unique

module Build {lo la l≈} (Cat : Category lo la l≈) where

  open Category Cat
  open Iso.Build Cat
  open Unique.Build Cat

  IsInitial : Obj → Set (lo ⊔ la ⊔ l≈)
  IsInitial ⊥ = ∀ X → ∃! ⊥ X

  record HasInitial : Set (lo ⊔ la ⊔ l≈) where
    field
      ⊥ : Obj
      isInitial : IsInitial ⊥

    ¡ : ∀ X → ⊥ ⇒ X
    ¡ X = ∃!′.arr (isInitial X)

    ¡-unique : ∀ {X} (f : ⊥ ⇒ X) → ¡ X ≈ f
    ¡-unique {X} f = ∃!′.unique (isInitial X) _

    ⊥⇒-unique : ∀ {X} (f g : ⊥ ⇒ X) → f ≈ g
    ⊥⇒-unique f g = ≈.trans (≈.sym (¡-unique f)) (¡-unique g)

    ⊥-unique : ∀ {X} → IsInitial X → X ≅ ⊥
    ⊥-unique {X} init = record
      { forth = init ⊥ .∃!′.arr
      ; back = ¡ X
      ; back-forth = ≈.trans (≈.sym (init X .∃!′.unique _)) (init X .∃!′.unique _)
      ; forth-back = ⊥⇒-unique _ _
      }

  initial-unique : ∀ {X Y} → IsInitial X → IsInitial Y → X ≅ Y
  initial-unique X-init Y-init
    = HasInitial.⊥-unique (record { isInitial = Y-init }) X-init

open Build public using (HasInitial)

private
  open module Build′ {lo la l≈} {C : Category lo la l≈}
    = Build C public using (IsInitial ; initial-unique)

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Functions.Definition
open import Boolean.Definition

open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Vectors

module Logic.PropositionalLogic where

data Propositions {a : _} (primitives : Set a) : Set a where
  ofPrimitive : primitives → Propositions primitives
  false : Propositions primitives
  implies : (a b : Propositions primitives) → Propositions primitives

prNot : {a : _} {pr : Set a} → Propositions pr → Propositions pr
prNot p = implies p false

impliesIsBigger : {a : _} {pr : Set a} {P Q : Propositions pr} → Q ≡ implies P Q → False
impliesIsBigger {P = P} {Q} ()

impliesInjectiveL : {a : _} {A : Set a} → {p q r : Propositions A} → implies p q ≡ implies r q → p ≡ r
impliesInjectiveL refl = refl

impliesInjectiveR : {a : _} {A : Set a} → {p q r : Propositions A} → implies p q ≡ implies p r → q ≡ r
impliesInjectiveR refl = refl

impliesInjective : {a : _} {A : Set a} → {p q r s : Propositions A} → implies p q ≡ implies r s → (p ≡ r) && (q ≡ s)
impliesInjective refl = refl ,, refl

record Valuation {a : _} (primitives : Set a) : Set a where
  field
    v : Propositions primitives → Bool
    vFalse : v false ≡ BoolFalse
    vImplicationF : {p q : Propositions primitives} → v p ≡ BoolTrue → v q ≡ BoolFalse → v (implies p q) ≡ BoolFalse
    vImplicationVacuous : {p q : Propositions primitives} → v p ≡ BoolFalse → v (implies p q) ≡ BoolTrue
    vImplicationT : {p q : Propositions primitives} → v q ≡ BoolTrue → v (implies p q) ≡ BoolTrue

-- Proposition 1a
valuationIsDetermined : {a : _} {pr : Set a} → (v1 v2 : Valuation pr) → ({x : pr} → Valuation.v v1 (ofPrimitive x) ≡ Valuation.v v2 (ofPrimitive x)) → {x : Propositions pr} → Valuation.v v1 x ≡ Valuation.v v2 x
valuationIsDetermined v1 v2 pr {ofPrimitive x} = pr
valuationIsDetermined v1 v2 pr {false} rewrite Valuation.vFalse v1 | Valuation.vFalse v2 = refl
valuationIsDetermined v1 v2 pr {implies x y} with valuationIsDetermined v1 v2 pr {x}
valuationIsDetermined v1 v2 pr {implies x y} | eqX with valuationIsDetermined v1 v2 pr {y}
... | eqY with inspect (Valuation.v v1 x)
valuationIsDetermined v1 v2 pr {implies x y} | eqX | eqY | BoolTrue with≡ p with inspect (Valuation.v v1 y)
valuationIsDetermined v1 v2 pr {implies x y} | eqX | eqY | BoolTrue with≡ p | BoolTrue with≡ q rewrite p | q | Valuation.vImplicationT v2 {p = x} {q = y} (equalityCommutative eqY) | Valuation.vImplicationT v1 {p = x} {q = y} q = refl
valuationIsDetermined v1 v2 pr {implies x y} | eqX | eqY | BoolTrue with≡ p | BoolFalse with≡ q rewrite p | q | Valuation.vImplicationF v1 p q | Valuation.vImplicationF v2 (equalityCommutative eqX) (equalityCommutative eqY) = refl
valuationIsDetermined v1 v2 pr {implies x y} | eqX | eqY | BoolFalse with≡ p rewrite p | Valuation.vImplicationVacuous v1 {q = y} p | Valuation.vImplicationVacuous v2 {q = y} (equalityCommutative eqX) = refl

extendValuationV : {a : _} {pr : Set a} → (w : pr → Bool) → Propositions pr → Bool
extendValuationV w (ofPrimitive x) = w x
extendValuationV w false = BoolFalse
extendValuationV w (implies x y) with extendValuationV w x
... | BoolTrue with extendValuationV w y
extendValuationV w (implies x y) | BoolTrue | BoolTrue = BoolTrue
... | BoolFalse = BoolFalse
extendValuationV w (implies x y) | BoolFalse = BoolTrue

extendValuation : {a : _} {pr : Set a} → (w : pr → Bool) → Valuation pr
Valuation.v (extendValuation w) = extendValuationV w
Valuation.vFalse (extendValuation w) = refl
Valuation.vImplicationF (extendValuation w) {p} {q} pT qF with Valuation.v (extendValuation w) p
Valuation.vImplicationF (extendValuation w) {p} {q} refl qF | BoolTrue with Valuation.v (extendValuation w) q
Valuation.vImplicationF (extendValuation w) {p} {q} refl () | BoolTrue | BoolTrue
Valuation.vImplicationF (extendValuation w) {p} {q} refl refl | BoolTrue | BoolFalse = refl
Valuation.vImplicationF (extendValuation w) {p} {q} () qF | BoolFalse
Valuation.vImplicationVacuous (extendValuation w) {p} {q} pF with Valuation.v (extendValuation w) p
Valuation.vImplicationVacuous (extendValuation w) {p} {q} () | BoolTrue
Valuation.vImplicationVacuous (extendValuation w) {p} {q} refl | BoolFalse = refl
Valuation.vImplicationT (extendValuation w) {p} {q} qT with Valuation.v (extendValuation w) p
Valuation.vImplicationT (extendValuation w) {p} {q} qT | BoolTrue with Valuation.v (extendValuation w) q
Valuation.vImplicationT (extendValuation w) {p} {q} refl | BoolTrue | BoolTrue = refl
Valuation.vImplicationT (extendValuation w) {p} {q} () | BoolTrue | BoolFalse
Valuation.vImplicationT (extendValuation w) {p} {q} qT | BoolFalse = refl

-- Proposition 1b
valuationsAreFree : {a : _} {pr : Set a} → (w : pr → Bool) → {x : pr} → Valuation.v (extendValuation w) (ofPrimitive x) ≡ w x
valuationsAreFree w = refl

Tautology : {a : _} {pr : Set a} (prop : Propositions pr) → Set a
Tautology {pr = pr} prop = (v : Valuation pr) → Valuation.v v prop ≡ BoolTrue

record IsSubset {a b : _} (sub : Set a) (super : Set b) : Set (a ⊔ b) where
  field
    ofElt : sub → super

mapProp : {a b : _} {pr1 : Set a} {pr2 : Set b} → (pr1 → pr2) → Propositions pr1 → Propositions pr2
mapProp f (ofPrimitive x) = ofPrimitive (f x)
mapProp f false = false
mapProp f (implies p q) = implies (mapProp f p) (mapProp f q)

inheritedValuation : {a b : _} {sub : Set a} {super : Set b} → (IsSubset sub super) → Valuation super → Valuation sub
Valuation.v (inheritedValuation isSub v) prop = Valuation.v v (mapProp (IsSubset.ofElt isSub) prop)
Valuation.vFalse (inheritedValuation isSub v) = Valuation.vFalse v
Valuation.vImplicationF (inheritedValuation isSub v) pT qF = Valuation.vImplicationF v pT qF
Valuation.vImplicationVacuous (inheritedValuation isSub v) pF = Valuation.vImplicationVacuous v pF
Valuation.vImplicationT (inheritedValuation isSub v) qT = Valuation.vImplicationT v qT

inheritedValuation' : {a b : _} {sub : Set a} {super : Set b} → (IsSubset sub (Propositions super)) → Valuation super → (x : sub) → Bool
inheritedValuation' subset v x = Valuation.v v (IsSubset.ofElt subset x)

Entails : {a b : _} {sub : Set a} {super : Set b} (S : IsSubset sub (Propositions super)) (P : Propositions super) → Set (a ⊔ b)
Entails {sub = sub} {super = super} S P = {v : Valuation super} → ({s : sub} → inheritedValuation' S v s ≡ BoolTrue) → Valuation.v v P ≡ BoolTrue

data ThreeElements : Set where
  One : ThreeElements
  Two : ThreeElements
  Three : ThreeElements

indexAxiom : {a : _} (A : Set a) → ThreeElements → Set a
indexAxiom A One = Propositions A && Propositions A
indexAxiom A Two = Propositions A & Propositions A & Propositions A
indexAxiom A Three = Propositions A

indexPropositionalAxioms : {a : _} {A : Set a} → Set a
indexPropositionalAxioms {A = A} = Sg ThreeElements (indexAxiom A)

-- An axiom system is simply a subset of a set of propositions.
propositionalAxioms : {a : _} {A : Set a} → IsSubset (indexPropositionalAxioms {A = A}) (Propositions A)
IsSubset.ofElt propositionalAxioms (One , (p ,, q)) = implies p (implies q p)
IsSubset.ofElt propositionalAxioms (Two , record { one = p ; two = q ; three = r }) = implies (implies p (implies q r)) (implies (implies p q) (implies p r))
IsSubset.ofElt propositionalAxioms (Three , p) = implies (prNot (prNot p)) p

record Selection {a : _} {A : Set a} {n : ℕ} (l : Vec A n) : Set a where
  field
    element : A
    position : ℕ
    pos<N : position <N n
    elementIsAt : vecIndex l position pos<N ≡ element

data Proof {a b c : _} {A : Set a} {axioms : Set b} (axiomsSubset : IsSubset axioms (Propositions A)) {givens : Set c} (givensSubset : IsSubset givens (Propositions A)) : (n : ℕ) → Set (a ⊔ b ⊔ c)
data ProofStep {a b c : _} {A : Set a} {axioms : Set b} (axiomsSubset : IsSubset axioms (Propositions A)) {givens : Set c} (givensSubset : IsSubset givens (Propositions A)) {n : ℕ} (proofSoFar : Proof {a} {b} {c} {A} {axioms} axiomsSubset {givens} givensSubset n) : Set (a ⊔ b ⊔ c)

toSteps : {a b c : _} {A : Set a} {axioms : Set b} {axiomsSubset : IsSubset axioms (Propositions A)} {givens : Set c} {givensSubset : IsSubset givens (Propositions A)} {n : ℕ} (pr : Proof {axioms = axioms} axiomsSubset {givens = givens} givensSubset n) → Vec (Propositions A) n

data ProofStep {a} {b} {c} {A} {axioms} axiomsSubset {givens} givensSubset proofSoFar where
  axiom : axioms → ProofStep axiomsSubset givensSubset proofSoFar
  given : givens → ProofStep axiomsSubset givensSubset proofSoFar
  modusPonens : (implication : Selection (toSteps proofSoFar)) → (argument : Selection (toSteps proofSoFar)) → (conclusion : Propositions A) → (Selection.element implication ≡ implies (Selection.element argument) conclusion) → ProofStep axiomsSubset givensSubset proofSoFar
data Proof {a} {b} {c} {A} {axioms} axiomsSubset {givens} givensSubset where
  empty : Proof axiomsSubset givensSubset 0
  nextStep : (n : ℕ) → (previous : Proof {axioms = axioms} axiomsSubset {givens = givens} givensSubset n) → ProofStep axiomsSubset givensSubset previous → Proof axiomsSubset givensSubset (succ n)

toSteps empty = []
toSteps {axiomsSubset = axiomsSubset} (nextStep n pr (axiom x)) = (IsSubset.ofElt axiomsSubset x) ,- toSteps pr
toSteps {givensSubset = givensSubset} (nextStep n pr (given x)) = IsSubset.ofElt givensSubset x ,- toSteps pr
toSteps (nextStep n pr (modusPonens implication argument conclusion x)) = conclusion ,- toSteps pr

record Proves {a b c : _} {A : Set a} {axioms : Set b} (axiomsSubset : IsSubset axioms (Propositions A)) {givens : Set c} (givensSubset : IsSubset givens (Propositions A)) (P : Propositions A) : Set (a ⊔ b ⊔ c) where
  field
    n : ℕ
    proof : Proof axiomsSubset givensSubset (succ n)
    ofStatement : vecIndex (toSteps proof) 0 (succIsPositive n) ≡ P

addSingletonSet : {a : _} → Set a → Set a
addSingletonSet A = True || A

interpretSingletonSet : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → IsSubset A B → (c : C) → (addSingletonSet A) → C || B
interpretSingletonSet A<B c (inl x) = inl c
interpretSingletonSet A<B _ (inr x) = inr (IsSubset.ofElt A<B x)

inrInjective : {a b : _} {A : Set a} {B : Set b} {b1 b2 : B} → inr {a = a} {A = A} b1 ≡ inr b2 → b1 ≡ b2
inrInjective refl = refl

singletonSubset : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → IsSubset A B → (c : C) → IsSubset (addSingletonSet A) (C || B)
IsSubset.ofElt (singletonSubset subs c) = interpretSingletonSet subs c

adjoinGiven : {a b : _} {A : Set a} {givens : Set b} (givensSubset : IsSubset givens A) (P : A) → IsSubset (addSingletonSet givens) A
IsSubset.ofElt (adjoinGiven record { ofElt = ofElt } P) (inl x) = P
IsSubset.ofElt (adjoinGiven record { ofElt = ofElt } _) (inr x) = ofElt x

vecIndexRefl : {a : _} {A : Set a} {n : ℕ} {v1 v2 : Vec A n} → {pos : ℕ} → {pos<N1 pos<N2 : pos <N n} → v1 ≡ v2 → vecIndex v1 pos pos<N1 ≡ vecIndex v2 pos pos<N2
vecIndexRefl {v1 = v1} {.v1} {pos} {pos<N1} {pos<N2} refl = refl

{-
proofRemainsValidOnAddingGivens : {a b c : _} {A : Set a} {axioms : Set b} {axiomsSubset : IsSubset axioms (Propositions A)} {givens : Set c} {givensSubset : IsSubset givens (Propositions A)} {n : ℕ} → {Q : Propositions A} → Proof axiomsSubset givensSubset n → Proof axiomsSubset (adjoinGiven givensSubset Q) n
pr' : {a b c : _} {A : Set a} {axioms : Set b} {axiomsSubset : IsSubset axioms (Propositions A)} {givens : Set c} {givensSubset : IsSubset givens (Propositions A)} {n : ℕ} → {Q : Propositions A} → (pr : Proof axiomsSubset givensSubset n) → toSteps pr ≡ toSteps (proofRemainsValidOnAddingGivens {Q = Q} pr)

pr' empty = refl
pr' (nextStep n pr (axiom x)) rewrite pr' pr = refl
pr' (nextStep n pr (given x)) rewrite pr' pr = refl
pr' (nextStep n pr (modusPonens implication argument conclusion x)) rewrite pr' pr = refl

proofRemainsValidOnAddingGivens {Q = Q} empty = empty
proofRemainsValidOnAddingGivens {Q = Q} (nextStep n pr (axiom x)) = nextStep n (proofRemainsValidOnAddingGivens pr) (axiom x)
proofRemainsValidOnAddingGivens {Q = Q} (nextStep n pr (given x)) = nextStep n (proofRemainsValidOnAddingGivens pr) (given (inr x))
proofRemainsValidOnAddingGivens {A = A} {axiomsSubset = axiomsSubset} {givensSubset = givensSubset} {Q = Q} (nextStep n pr (modusPonens implication argument conclusion x)) = nextStep n (proofRemainsValidOnAddingGivens pr) (modusPonens (record { element = Selection.element implication ; position = Selection.position implication ; pos<N = Selection.pos<N implication ; elementIsAt = lemma implication }) (record { element = Selection.element argument ; position = Selection.position argument ; pos<N = Selection.pos<N argument ; elementIsAt = lemma argument }) conclusion x)
  where
    lemma : (sel : Selection (toSteps pr)) → vecIndex (toSteps (proofRemainsValidOnAddingGivens pr)) (Selection.position sel) (Selection.pos<N sel) ≡ Selection.element sel
    lemma sel with proofRemainsValidOnAddingGivens {Q = Q} pr
    ... | nextStep n bl x = {!!}
-}

{-

proofImpliesProves : {a b c : _} {A : Set a} {axioms : Set b} {axiomsSubset : IsSubset axioms (Propositions A)} {givens : Set c} {givensSubset : IsSubset givens (Propositions A)} {n : ℕ} (0<n : 0 <N n) → (p : Proof axiomsSubset givensSubset n) → (pr : Propositions A) → vecIndex (toSteps p) 0 0<n ≡ pr → Proves axiomsSubset givensSubset pr
proofImpliesProves {n = zero} () p pr x
proofImpliesProves {n = succ n} _ p pr x = record { n = n ; proof = p ; ofStatement = transitivity (vecIndexRefl {v1 = toSteps p} refl) x }

deductionTheorem' : {a b c : _} {A : Set a} {axioms : Set b} {axiomsSubset : IsSubset axioms (Propositions A)} {givens : Set c} {givensSubset : IsSubset givens (Propositions A)} {n : ℕ} → {P Q : Propositions A} → Proves axiomsSubset givensSubset (implies P Q) → Proves axiomsSubset {givens = addSingletonSet givens} (adjoinGiven givensSubset P) Q
Proves.n (deductionTheorem' record { n = n ; proof = proof ; ofStatement = ofStatement }) = succ (succ n)
Proves.proof (deductionTheorem' {P = P} {Q = Q} record { n = n ; proof = proof ; ofStatement = ofStatement }) = nextStep (succ (succ n)) (nextStep (succ n) (proofRemainsValidOnAddingGivens proof) (given (inl record {}))) (modusPonens (record { element = implies P Q ; position = 1 ; pos<N = succPreservesInequality (succIsPositive _) ; elementIsAt = transitivity (equalityCommutative (vecIndexRefl (pr' proof))) ofStatement }) (record { element = P ; position = 0 ; pos<N = succIsPositive _ ; elementIsAt = refl }) Q refl)
Proves.ofStatement (deductionTheorem' record { n = n ; proof = proof ; ofStatement = ofStatement }) = refl

deductionTheorem : {a b c : _} {A : Set a} {givens : Set c} {givensSubset : IsSubset givens (Propositions A)} {n : ℕ} → {P Q : Propositions A} → Proves propositionalAxioms {givens = addSingletonSet givens} (adjoinGiven givensSubset P) Q → Proves propositionalAxioms givensSubset (implies P Q)
deductionTheorem {P = P} {Q} record { n = n ; proof = (nextStep .n proof (axiom x)) ; ofStatement = ofStatement } = {!!}
--... | bl = record { n = {!!} ; proof = nextStep (succ (succ (succ n))) (nextStep (succ (succ n)) (nextStep (succ n) {!deductionTheorem proof!} (axiom x)) (axiom (One , (Q ,, P)))) (modusPonens (record { element = implies Q (implies P Q) ; position = 0 ; pos<N = succIsPositive _ ; elementIsAt = refl }) (record { element = Q ; position = 1 ; pos<N = succPreservesInequality (succIsPositive _) ; elementIsAt = ofStatement }) (implies P Q) refl) ; ofStatement = {!!} }
deductionTheorem {P = P} {Q} record { n = n ; proof = (nextStep .n proof (given x)) ; ofStatement = ofStatement } = {!!}
deductionTheorem {P = P} {Q} record { n = n ; proof = (nextStep .n proof (modusPonens implication argument conclusion x)) ; ofStatement = ofStatement } = {!!}
{-
Proves.n (deductionTheorem {P = P} {Q} record { n = n ; proof = (nextStep .n proof (axiom x)) ; ofStatement = ofStatement }) = succ (succ (succ n))
Proves.proof (deductionTheorem {P = P} {Q} record { n = n ; proof = (nextStep .n proof (axiom x)) ; ofStatement = ofStatement }) = nextStep (succ (succ (succ n))) (nextStep (succ (succ n)) (nextStep (succ n) {!!} (axiom x)) (axiom (One , (Q ,, P)))) (modusPonens (record { element = implies Q (implies P Q) ; position = 0 ; pos<N = succIsPositive _ ; elementIsAt = refl }) (record { element = Q ; position = 1 ; pos<N = succPreservesInequality (succIsPositive _) ; elementIsAt = ofStatement }) (implies P Q) refl)
Proves.ofStatement (deductionTheorem {P = P} {Q} record { n = n ; proof = (nextStep .n proof (axiom x)) ; ofStatement = ofStatement }) = {!!}
deductionTheorem {P = P} {Q} record { n = n ; proof = (nextStep .n proof (given x)) ; ofStatement = ofStatement } = {!!}
deductionTheorem {P = P} {Q} record { n = n ; proof = (nextStep .n proof (modusPonens implication argument conclusion x)) ; ofStatement = ofStatement } = {!!}

-}

propositionalLogicSound : {a b c : _} {A : Set a} {givens : Set c} {givensSubset : IsSubset givens (Propositions A)} → {P : Propositions A} → Proves propositionalAxioms givensSubset P → Entails givensSubset P
Entails.entails (propositionalLogicSound {P = .(IsSubset.ofElt propositionalAxioms x)} record { n = .0 ; proof = (nextStep .0 empty (axiom x)) ; ofStatement = refl }) {v} values = propositionalAxiomsTautology x {v}
Entails.entails (propositionalLogicSound {P = P} record { n = .0 ; proof = (nextStep .0 empty (given x)) ; ofStatement = ofStatement }) {v} values rewrite equalityCommutative ofStatement = values {x}
Entails.entails (propositionalLogicSound {P = P} record { n = .0 ; proof = (nextStep .0 empty (modusPonens record { element = element ; position = zero ; pos<N = (le x₁ ()) ; elementIsAt = elementIsAt } argument conclusion x)) ; ofStatement = ofStatement }) {v} values
Entails.entails (propositionalLogicSound {P = P} record { n = .0 ; proof = (nextStep .0 empty (modusPonens record { element = element ; position = (succ position) ; pos<N = (le x₁ ()) ; elementIsAt = elementIsAt } argument conclusion x)) ; ofStatement = ofStatement }) {v} values
Entails.entails (propositionalLogicSound {P = P} record { n = .(succ n) ; proof = (nextStep .(succ n) (nextStep n proof y) x) ; ofStatement = ofStatement }) {v} values = {!!}

-}


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order

module Numbers.Naturals.WithK where

<NRefl : {a b : ℕ} → (p1 p2 : a <N b) → (p1 ≡ p2)
<NRefl {a} {.(succ (p1 +N a))} (le p1 refl) (le p2 proof2) = help p1=p2 proof2
  where
    p1=p2 : p1 ≡ p2
    p1=p2 = equalityCommutative (canSubtractFromEqualityRight {p2} {a} {p1} (succInjective proof2))
    help : (p1 ≡ p2) → (pr2 : succ (p2 +N a) ≡ succ (p1 +N a)) → le p1 refl ≡ le p2 pr2
    help refl refl = refl


text:
module bool-to-string where

open import bool
open import string

𝔹-to-string : 𝔹 → string
𝔹-to-string tt = "tt"
𝔹-to-string ff = "ff"

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
------------------------------------------------------------------------
-- The two semantical definitions of subtyping are equivalent
------------------------------------------------------------------------

module RecursiveTypes.Subtyping.Semantic.Equivalence where

open import Data.Nat
open import Codata.Musical.Notation
open import Function.Base

open import RecursiveTypes.Syntax
open import RecursiveTypes.Subtyping.Semantic.Inductive
open import RecursiveTypes.Subtyping.Semantic.Coinductive

mutual

  ≤∞⇒≤↓ : ∀ {n} {σ τ : Tree n} → σ ≤∞ τ → σ ≤↓ τ
  ≤∞⇒≤↓ le              zero    = ⊥
  ≤∞⇒≤↓ ⊥               (suc k) = ⊥
  ≤∞⇒≤↓ ⊤               (suc k) = ⊤
  ≤∞⇒≤↓ var             (suc k) = refl
  ≤∞⇒≤↓ (τ₁≤σ₁ ⟶ σ₂≤τ₂) (suc k) = ≤∞⇒≤↑ (♭ τ₁≤σ₁) k ⟶ ≤∞⇒≤↓ (♭ σ₂≤τ₂) k

  ≤∞⇒≤↑ : ∀ {n} {σ τ : Tree n} → σ ≤∞ τ → σ ≤↑ τ
  ≤∞⇒≤↑ le              zero    = ⊤
  ≤∞⇒≤↑ ⊥               (suc k) = ⊥
  ≤∞⇒≤↑ ⊤               (suc k) = ⊤
  ≤∞⇒≤↑ var             (suc k) = refl
  ≤∞⇒≤↑ (τ₁≤σ₁ ⟶ σ₂≤τ₂) (suc k) = ≤∞⇒≤↓ (♭ τ₁≤σ₁) k ⟶ ≤∞⇒≤↑ (♭ σ₂≤τ₂) k

domain : ∀ {n} {σ₁ σ₂ τ₁ τ₂ : FinTree n} →
         σ₁ ⟶ σ₂ ≤Fin τ₁ ⟶ τ₂ → σ₂ ≤Fin τ₂
domain refl            = refl
domain (τ₁≤σ₁ ⟶ σ₂≤τ₂) = σ₂≤τ₂

codomain : ∀ {n} {σ₁ σ₂ τ₁ τ₂ : FinTree n} →
           σ₁ ⟶ σ₂ ≤Fin τ₁ ⟶ τ₂ → τ₁ ≤Fin σ₁
codomain refl            = refl
codomain (τ₁≤σ₁ ⟶ σ₂≤τ₂) = τ₁≤σ₁

mutual

  ≤↑⇒≤∞ : ∀ {n} (σ τ : Tree n) → σ ≤↑ τ → σ ≤∞ τ
  ≤↑⇒≤∞ ⊥ _ le = ⊥
  ≤↑⇒≤∞ _ ⊤ le = ⊤
  ≤↑⇒≤∞ ⊤ ⊥ le with le 1
  ... | ()
  ≤↑⇒≤∞ ⊤ (var x) le with le 1
  ... | ()
  ≤↑⇒≤∞ ⊤ (σ ⟶ τ) le with le 1
  ... | ()
  ≤↑⇒≤∞ (var x) ⊥ le with le 1
  ... | ()
  ≤↑⇒≤∞ (var x) (var x′) le with le 1
  ≤↑⇒≤∞ (var x) (var .x) le | refl = var
  ≤↑⇒≤∞ (var x) (σ ⟶ τ) le with le 1
  ... | ()
  ≤↑⇒≤∞ (σ₁ ⟶ τ₁) ⊥ le with le 1
  ... | ()
  ≤↑⇒≤∞ (σ₁ ⟶ τ₁) (var x) le with le 1
  ... | ()
  ≤↑⇒≤∞ (σ₁ ⟶ τ₁) (σ₂ ⟶ τ₂) le =
    ♯ ≤↓⇒≤∞ (♭ σ₂) (♭ σ₁) (codomain ∘ le ∘ suc) ⟶
    ♯ ≤↑⇒≤∞ (♭ τ₁) (♭ τ₂) (domain   ∘ le ∘ suc)

  ≤↓⇒≤∞ : ∀ {n} (σ τ : Tree n) → σ ≤↓ τ → σ ≤∞ τ
  ≤↓⇒≤∞ ⊥ _ le = ⊥
  ≤↓⇒≤∞ _ ⊤ le = ⊤
  ≤↓⇒≤∞ ⊤ ⊥ le with le 1
  ... | ()
  ≤↓⇒≤∞ ⊤ (var x) le with le 1
  ... | ()
  ≤↓⇒≤∞ ⊤ (σ ⟶ τ) le with le 1
  ... | ()
  ≤↓⇒≤∞ (var x) ⊥ le with le 1
  ... | ()
  ≤↓⇒≤∞ (var x) (var x′) le with le 1
  ≤↓⇒≤∞ (var x) (var .x) le | refl = var
  ≤↓⇒≤∞ (var x) (σ ⟶ τ) le with le 1
  ... | ()
  ≤↓⇒≤∞ (σ₁ ⟶ τ₁) ⊥ le with le 1
  ... | ()
  ≤↓⇒≤∞ (σ₁ ⟶ τ₁) (var x) le with le 1
  ... | ()
  ≤↓⇒≤∞ (σ₁ ⟶ τ₁) (σ₂ ⟶ τ₂) le =
    ♯ ≤↑⇒≤∞ (♭ σ₂) (♭ σ₁) (codomain ∘ le ∘ suc) ⟶
    ♯ ≤↓⇒≤∞ (♭ τ₁) (♭ τ₂) (domain   ∘ le ∘ suc)

Ind⇒Coind : ∀ {n} {σ τ : Ty n} → σ ≤Ind τ → σ ≤Coind τ
Ind⇒Coind = ≤↓⇒≤∞ _ _

Coind⇒Ind : ∀ {n} {σ τ : Ty n} → σ ≤Coind τ → σ ≤Ind τ
Coind⇒Ind = ≤∞⇒≤↓


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

-- Based on (Vene, 2000).

module Functors where

infixr 1 _+_
infixr 2 _×_

data Bool : Set where
  false true : Bool

data _+_  (A B : Set) : Set where
  inl : A → A + B
  inr : B → A + B

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

-- The terminal object.
data ⊤ : Set where
   <> : ⊤

postulate
  -- The least fixed-point.

  -- Haskell definitions:

  -- data Mu f = In (f (Mu f))

  -- unIn :: Mu f → f (Mu f)
  -- unIn (In x) = x

  μ    : (Set → Set) → Set
  In   : {F : Set → Set} → F (μ F) → μ F
  unIn : {F : Set → Set} → μ F → F (μ F)

postulate
  -- The greatest fixed-point.

  -- Haskell definitions:

  -- data Nu f = Wrap (f (Nu f))

  -- out :: Nu f → (f (Nu f))
  -- out (Wrap x) = x

  ν    : (Set → Set) → Set
  Wrap : {F : Set → Set} → F (ν F) → ν F
  out  : {F : Set → Set} → ν F → F (ν F)

------------------------------------------------------------------------------
-- Functors

--  The identity functor (the functor for the empty and unit types).
IdF : Set → Set
IdF X = X

-- The (co)natural numbers functor.
NatF : Set → Set
NatF X = ⊤ + X

-- The (co)list functor.
ListF : Set → Set → Set
ListF A X = ⊤ + A × X

-- The stream functor.
StreamF : Set → Set → Set
StreamF A X = A × X

------------------------------------------------------------------------------
-- Types as least fixed-points

-- The empty type is a least fixed-point.
⊥ : Set
⊥ = μ IdF

-- The natural numbers type is a least fixed-point.
N : Set
N = μ NatF

-- The data constructors for the natural numbers.
zero : N
zero = In (inl <>)

succ : N → N
succ n = In (inr n)

-- The list type is a least fixed-point.
List : Set → Set
List A = μ (ListF A)

-- The data constructors for List.
nil : {A : Set} → List A
nil = In (inl <>)

cons : {A : Set} → A → List A → List A
cons x xs = In (inr (x , xs))

------------------------------------------------------------------------------
-- Types as greatest fixed-points

-- The unit type is a greatest fixed-point.
Unit : Set
Unit = ν IdF

-- Non-structural recursion
-- unit : Nu IdF
-- unit = Wrap IdF {!unit!}

-- The conat type is a greatest fixed-point.
Conat : Set
Conat = ν NatF

zeroC : Conat
zeroC = Wrap (inl <>)

succC : Conat → Conat
succC cn = Wrap (inr cn)

-- Non-structural recursion for the definition of ∞C.
-- ∞C : Conat
-- ∞C = succC {!∞C!}

-- The pred function is the conat destructor.
pred : Conat → ⊤ + Conat
pred cn with out cn
... | inl _ = inl <>
... | inr x = inr x

-- The colist type is a greatest fixed-point.
Colist : Set → Set
Colist A = ν (ListF A)

-- The colist data constructors.
nilCL : {A : Set} → Colist A
nilCL = Wrap (inl <>)

consCL : {A : Set} → A → Colist A → Colist A
consCL x xs = Wrap (inr (x , xs))

-- The colist destructors.
nullCL : {A : Set} → Colist A → Bool
nullCL xs with out xs
... | inl _ = true
... | inr _ = false

-- headCL : {A : Set} → Colist A → A
-- headCL {A} xs with out (ListF A) xs
-- ... | inl t       =  -- Impossible
-- ... | inr (x , _) = x

-- tailCL : {A : Set} → Colist A → Colist A
-- tailCL {A} xs with out (ListF A) xs
-- ... | inl t         =  -- Impossible
-- ... | inr (_ , xs') = xs'

-- The stream type is a greatest fixed-point.
Stream : Set → Set
Stream A = ν (StreamF A)

-- The stream data constructor.
consS : {A : Set} → A → Stream A → Stream A
consS x xs = Wrap (x , xs)

-- The stream destructors.
headS : {A : Set} → Stream A → A
headS xs with out xs
... | x , _ = x

tailS : {A : Set} → Stream A → Stream A
tailS xs with out xs
... | _ , xs' = xs'

-- From (Leclerc and Paulin-Mohring 1994, p. 195).
--
-- TODO (07 January 2014): Agda doesn't accept the definition of
-- Stream-build.
{-# TERMINATING #-}
Stream-build :
  {A X : Set} →
  (X → StreamF A X) →
  X → Stream A
Stream-build h x with h x
... | a , x' = Wrap (a , Stream-build h x')

-- From (Giménez, 1995, p. 40).
--
-- TODO (07 January 2014): Agda doesn't accept the definition of
-- Stream-corec.
{-# TERMINATING #-}
Stream-corec :
  {A X : Set} →
  (X → (A × (Stream A + X))) →
  X → Stream A
Stream-corec h x with h x
... | a , inl xs = Wrap (a , xs)
... | a , inr x' = Wrap (a , (Stream-corec h x'))

------------------------------------------------------------------------------
-- References
--
-- Giménez, E. (1995). Codifying guarded definitions with recursive
-- schemes. In: Types for Proofs and Programs (TYPES ’94). Ed. by
-- Dybjer, P., Nordström, B. and Smith, J. Vol. 996. LNCS. Springer,
-- pp. 39–59.
--
-- Leclerc, F. and Paulin-Mohring, C. (1994). Programming with Streams
-- in Coq. A case study : the Sieve of Eratosthenes. In: Types for
-- Proofs and Programs (TYPES ’93). Ed. by Barendregt, H. and Nipkow,
-- T. Vol. 806. LNCS. Springer, pp. 191–212.
--
-- Vene, Varmo (2000). Categorical programming with inductive and
-- coinductive types. PhD thesis. Faculty of Mathematics: University
-- of Tartu.