text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.FunctorAlgebras where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
open import Cubical.Foundations.Univalence

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation.Base

open _≅_

private
  variable ℓC ℓC' : Level

module _ {C : Category ℓC ℓC'} (F : Functor C C) where

  open Category
  open Functor

  IsAlgebra : ob C → Type ℓC'
  IsAlgebra x = C [ F-ob F x , x ]

  record Algebra : Type (ℓ-max ℓC ℓC') where
    constructor algebra
    field
      carrier : ob C
      str : IsAlgebra carrier
  open Algebra

  IsAlgebraHom : (algA algB : Algebra) → C [ carrier algA , carrier algB ] → Type ℓC'
  IsAlgebraHom algA algB f = (f ∘⟨ C ⟩ str algA) ≡ (str algB ∘⟨ C ⟩ F-hom F f)

  record AlgebraHom (algA algB : Algebra) : Type ℓC' where
    constructor algebraHom
    field
      carrierHom : C [ carrier algA , carrier algB ]
      strHom : IsAlgebraHom algA algB carrierHom
  open AlgebraHom

  RepAlgebraHom : (algA algB : Algebra) → Type ℓC'
  RepAlgebraHom algA algB = Σ[ f ∈ C [ carrier algA , carrier algB ] ] IsAlgebraHom algA algB f

  isoRepAlgebraHom : (algA algB : Algebra) → AlgebraHom algA algB ≅ RepAlgebraHom algA algB
  fun (isoRepAlgebraHom algA algB) (algebraHom f isalgF) = f , isalgF
  inv (isoRepAlgebraHom algA algB) (f , isalgF) = algebraHom f isalgF
  rightInv (isoRepAlgebraHom algA algB) (f , isalgF) = refl
  leftInv (isoRepAlgebraHom algA algB) (algebraHom f isalgF)= refl

  pathRepAlgebraHom : (algA algB : Algebra) → AlgebraHom algA algB ≡ RepAlgebraHom algA algB
  pathRepAlgebraHom algA algB = ua (isoToEquiv (isoRepAlgebraHom algA algB))

  AlgebraHom≡ : {algA algB : Algebra} {algF algG : AlgebraHom algA algB}
    → (carrierHom algF ≡ carrierHom algG) → algF ≡ algG
  carrierHom (AlgebraHom≡ {algA} {algB} {algF} {algG} p i) = p i
  strHom (AlgebraHom≡ {algA} {algB} {algF} {algG} p i) = idfun
    (PathP (λ j → (p j ∘⟨ C ⟩ str algA) ≡ (str algB ∘⟨ C ⟩ F-hom F (p j)))
      (strHom algF)
      (strHom algG)
    )
    (fst (idfun (isContr _) (isOfHLevelPathP' 0
        (isOfHLevelPath' 1 (isSetHom C) _ _)
      (strHom algF) (strHom algG))))
    i

  idAlgebraHom : {algA : Algebra} → AlgebraHom algA algA
  carrierHom (idAlgebraHom {algA}) = id C
  strHom (idAlgebraHom {algA}) =
    ⋆IdR C (str algA) ∙∙ sym (⋆IdL C (str algA)) ∙∙ cong (λ φ → φ ⋆⟨ C ⟩ str algA) (sym (F-id F))

  seqAlgebraHom : {algA algB algC : Algebra}
    (algF : AlgebraHom algA algB) (algG : AlgebraHom algB algC)
    → AlgebraHom algA algC
  carrierHom (seqAlgebraHom {algA} {algB} {algC} algF algG) = carrierHom algF ⋆⟨ C ⟩ carrierHom algG
  strHom (seqAlgebraHom {algA} {algB} {algC} algF algG) =
    str algA ⋆⟨ C ⟩ (carrierHom algF ⋆⟨ C ⟩ carrierHom algG)
      ≡⟨ sym (⋆Assoc C (str algA) (carrierHom algF) (carrierHom algG)) ⟩
    (str algA ⋆⟨ C ⟩ carrierHom algF) ⋆⟨ C ⟩ carrierHom algG
      ≡⟨ cong (λ φ → φ ⋆⟨ C ⟩ carrierHom algG) (strHom algF) ⟩
    (F-hom F (carrierHom algF) ⋆⟨ C ⟩ str algB) ⋆⟨ C ⟩ carrierHom algG
      ≡⟨ ⋆Assoc C (F-hom F (carrierHom algF)) (str algB) (carrierHom algG) ⟩
    F-hom F (carrierHom algF) ⋆⟨ C ⟩ (str algB ⋆⟨ C ⟩ carrierHom algG)
      ≡⟨ cong (λ φ → F-hom F (carrierHom algF) ⋆⟨ C ⟩ φ) (strHom algG) ⟩
    F-hom F (carrierHom algF) ⋆⟨ C ⟩ (F-hom F (carrierHom algG) ⋆⟨ C ⟩ str algC)
      ≡⟨ sym (⋆Assoc C (F-hom F (carrierHom algF)) (F-hom F (carrierHom algG)) (str algC)) ⟩
    (F-hom F (carrierHom algF) ⋆⟨ C ⟩ F-hom F (carrierHom algG)) ⋆⟨ C ⟩ str algC
      ≡⟨ cong (λ φ → φ ⋆⟨ C ⟩ str algC) (sym (F-seq F (carrierHom algF) (carrierHom algG))) ⟩
    F-hom F (carrierHom algF ⋆⟨ C ⟩ carrierHom algG) ⋆⟨ C ⟩ str algC ∎

  AlgebrasCategory : Category (ℓ-max ℓC ℓC') ℓC'
  ob AlgebrasCategory = Algebra
  Hom[_,_] AlgebrasCategory = AlgebraHom
  id AlgebrasCategory = idAlgebraHom
  _⋆_ AlgebrasCategory = seqAlgebraHom
  ⋆IdL AlgebrasCategory algF = AlgebraHom≡ (⋆IdL C (carrierHom algF))
  ⋆IdR AlgebrasCategory algF = AlgebraHom≡ (⋆IdR C (carrierHom algF))
  ⋆Assoc AlgebrasCategory algF algG algH =
    AlgebraHom≡ (⋆Assoc C (carrierHom algF) (carrierHom algG) (carrierHom algH))
  isSetHom AlgebrasCategory = subst isSet (sym (pathRepAlgebraHom _ _))
    (isSetΣ (isSetHom C) (λ f → isProp→isSet (isSetHom C _ _)))

  ForgetAlgebra : Functor AlgebrasCategory C
  F-ob ForgetAlgebra = carrier
  F-hom ForgetAlgebra = carrierHom
  F-id ForgetAlgebra = refl
  F-seq ForgetAlgebra algF algG = refl

module _ {C : Category ℓC ℓC'} {F G : Functor C C} (τ : NatTrans F G) where

  private
    module C = Category C
  open Functor
  open NatTrans
  open AlgebraHom

  AlgebrasFunctor : Functor (AlgebrasCategory G) (AlgebrasCategory F)
  F-ob AlgebrasFunctor (algebra a α) = algebra a (α C.∘ N-ob τ a)
  carrierHom (F-hom AlgebrasFunctor (algebraHom f isalgF)) = f
  strHom (F-hom AlgebrasFunctor {algebra a α} {algebra b β} (algebraHom f isalgF)) =
    (N-ob τ a C.⋆ α) C.⋆ f
      ≡⟨ C.⋆Assoc (N-ob τ a) α f ⟩
    N-ob τ a C.⋆ (α C.⋆ f)
      ≡⟨ cong (N-ob τ a C.⋆_) isalgF ⟩
    N-ob τ a C.⋆ (F-hom G f C.⋆ β)
      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
    (N-ob τ a C.⋆ F-hom G f) C.⋆ β
      ≡⟨ cong (C._⋆ β) (sym (N-hom τ f)) ⟩
    (F-hom F f C.⋆ N-ob τ b) C.⋆ β
      ≡⟨ C.⋆Assoc _ _ _ ⟩
    F-hom F f C.⋆ (N-ob τ b C.⋆ β) ∎
  F-id AlgebrasFunctor = AlgebraHom≡ F refl
  F-seq AlgebrasFunctor algΦ algΨ = AlgebraHom≡ F refl

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Prelude where

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

open import Agda.Primitive public
  using (Level ; _⊔_)
  renaming (lzero to ℓ₀)

id : ∀ {ℓ} → {X : Set ℓ}
           → X → X
id x = x

_◎_ : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {P : X → Set ℓ′} {Q : ∀ {x} → P x → Set ℓ″}
                  → (g : ∀ {x} → (y : P x) → Q y) (f : (x : X) → P x) (x : X)
                  → Q (f x)
(g ◎ f) x = g (f x)

const : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′}
                 → X → Y → X
const x y = x

flip : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : X → Y → Set ℓ″}
                   → (f : (x : X) (y : Y) → Z x y) (y : Y) (x : X)
                   → Z x y
flip f y x = f x y

_∘_ : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″}
                  → (g : Y → Z) (f : X → Y)
                  → X → Z
g ∘ f = g ◎ f

_⨾_ : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″}
                  → (f : X → Y) (g : Y → Z)
                  → X → Z
_⨾_ = flip _∘_

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

open import Agda.Builtin.Equality public
  using (_≡_ ; refl)

_⁻¹≡ : ∀ {ℓ} → {X : Set ℓ} {x₁ x₂ : X}
             → x₁ ≡ x₂ → x₂ ≡ x₁
refl ⁻¹≡ = refl

_⦙≡_ : ∀ {ℓ} → {X : Set ℓ} {x₁ x₂ x₃ : X}
             → x₁ ≡ x₂ → x₂ ≡ x₃ → x₁ ≡ x₃
refl ⦙≡ refl = refl

record PER {ℓ}
           (X : Set ℓ)
           (_≈_ : X → X → Set ℓ)
         : Set ℓ where
  infix  9 _⁻¹
  infixr 4 _⦙_
  field
    _⁻¹ : ∀ {x₁ x₂} → x₁ ≈ x₂
                    → x₂ ≈ x₁

    _⦙_ : ∀ {x₁ x₂ x₃} → x₁ ≈ x₂ → x₂ ≈ x₃
                       → x₁ ≈ x₃

open PER {{…}} public

instance
  per≡ : ∀ {ℓ} {X : Set ℓ} → PER X _≡_
  per≡ =
    record
      { _⁻¹ = _⁻¹≡
      ; _⦙_ = _⦙≡_
      }

infixl 9 _&_
_&_ : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′} {x₁ x₂ : X}
               → (f : X → Y) → x₁ ≡ x₂
               → f x₁ ≡ f x₂
f & refl = refl

infixl 8 _⊗_
_⊗_ : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′} {f₁ f₂ : X → Y} {x₁ x₂ : X}
               → f₁ ≡ f₂ → x₁ ≡ x₂
               → f₁ x₁ ≡ f₂ x₂
refl ⊗ refl = refl

case_of_ : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′}
                    → X → (X → Y) → Y
case x of f = f x

coe : ∀ {ℓ} → {X Y : Set ℓ}
            → X ≡ Y → X → Y
coe refl x = x

postulate
  fext! : ∀ {ℓ ℓ′} → {X : Set ℓ} {P : X → Set ℓ′} {f₁ f₂ : (x : X) → P x}
                   → ((x : X) → f₁ x ≡ f₂ x)
                   → f₁ ≡ f₂

  fext¡ : ∀ {ℓ ℓ′} → {X : Set ℓ} {P : X → Set ℓ′} {f₁ f₂ : {x : X} → P x}
                   → ({x : X} → f₁ {x} ≡ f₂ {x})
                   → (λ {x} → f₁ {x}) ≡ (λ {x} → f₂ {x})

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

open import Agda.Builtin.Unit public
  using (⊤ ; tt)

data ⊥ : Set where

elim⊥ : ∀ {ℓ} → {X : Set ℓ}
               → ⊥ → X
elim⊥ ()

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ X = X → ⊥

Π : ∀ {ℓ ℓ′} → Set ℓ → Set ℓ′ → Set (ℓ ⊔ ℓ′)
Π X Y = X → Y

infixl 6 _,_
record Σ {ℓ ℓ′}
         (X : Set ℓ) (P : X → Set ℓ′)
       : Set (ℓ ⊔ ℓ′) where
  instance
    constructor _,_
  field
    proj₁ : X

    proj₂ : P proj₁

open Σ public

infixl 5 _⁏_
pattern _⁏_ x y = x , y

infixl 2 _×_
_×_ : ∀ {ℓ ℓ′} → Set ℓ → Set ℓ′ → Set (ℓ ⊔ ℓ′)
X × Y = Σ X (λ x → Y)

mapΣ : ∀ {ℓ ℓ′ ℓ″ ℓ‴} → {X : Set ℓ} {Y : Set ℓ′} {P : X → Set ℓ″} {Q : Y → Set ℓ‴}
                      → (f : X → Y) (g : ∀ {x} → P x → Q (f x)) → Σ X P
                      → Σ Y Q
mapΣ f g (x , y) = f x , g y

caseΣ : ∀ {ℓ ℓ′ ℓ″ ℓ‴} → {X : Set ℓ} {Y : Set ℓ′} {P : X → Set ℓ″} {Q : Y → Set ℓ‴}
                       → Σ X P → (f : X → Y) (g : ∀ {x} → P x → Q (f x))
                       → Σ Y Q
caseΣ p f g = mapΣ f g p

infixl 1 _⊎_
data _⊎_ {ℓ ℓ′}
         (X : Set ℓ) (Y : Set ℓ′)
       : Set (ℓ ⊔ ℓ′) where
  inj₁ : (x : X) → X ⊎ Y
  inj₂ : (y : Y) → X ⊎ Y

elim⊎ : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″}
                    → X ⊎ Y → (X → Z) → (Y → Z)
                    → Z
elim⊎ (inj₁ x) f g = f x
elim⊎ (inj₂ y) f g = g y

map⊎ : ∀ {ℓ ℓ′ ℓ″ ℓ‴} → {X : Set ℓ} {Y : Set ℓ′} {Z₁ : Set ℓ″} {Z₂ : Set ℓ‴}
                      → (X → Z₁) → (Y → Z₂) → X ⊎ Y
                      → Z₁ ⊎ Z₂
map⊎ f g s = elim⊎ s (inj₁ ∘ f) (inj₂ ∘ g)

case⊎ : ∀ {ℓ ℓ′ ℓ″ ℓ‴} → {X : Set ℓ} {Y : Set ℓ′} {Z₁ : Set ℓ″} {Z₂ : Set ℓ‴}
                       → X ⊎ Y → (X → Z₁) → (Y → Z₂)
                       → Z₁ ⊎ Z₂
case⊎ s f g = map⊎ f g s

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

open import Agda.Builtin.Bool public
  using (Bool ; false ; true)

if_then_else_ : ∀ {ℓ} → {X : Set ℓ}
                      → Bool → X → X
                      → X
if_then_else_ true  t f = t
if_then_else_ false t f = f

not : Bool → Bool
not true  = false
not false = true

and : Bool → Bool → Bool
and true  b = b
and false b = false

or : Bool → Bool → Bool
or true  b = true
or false b = b

xor : Bool → Bool → Bool
xor true  b = not b
xor false b = b

data True : Bool → Set
  where
    instance
      yes : True true

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

open import Agda.Builtin.Nat public
  using (Nat ; zero ; suc)
open import Agda.Builtin.FromNat public
  using (Number ; fromNat)

instance
  numNat : Number Nat
  numNat =
    record
      { Constraint = λ n → ⊤
      ; fromNat    = λ n → n
      }

_>?_ : Nat → Nat → Bool
zero  >? k     = false
suc n >? zero  = true
suc n >? suc k = n >? k

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

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

    suc  : ∀ {n} → Fin n
                 → Fin (suc n)

Nat→Fin : ∀ {n} → (k : Nat) {{_ : True (n >? k)}}
                 → Fin n
Nat→Fin {n = zero}  k       {{()}}
Nat→Fin {n = suc n} zero    {{is-true}} = zero
Nat→Fin {n = suc n} (suc k) {{p}}       = suc (Nat→Fin k {{p}})

instance
  numFin : ∀ {n} → Number (Fin n)
  numFin {n} =
    record
      { Constraint = λ k → True (n >? k)
      ; fromNat    = Nat→Fin
      }

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
-- Andreas, 2013-11-23
-- checking that postulates are allowed in new-style mutual blocks

open import Common.Prelude

-- new style mutual block

even : Nat → Bool

postulate
  odd : Nat → Bool

even zero    = true
even (suc n) = odd n

-- No error

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Data.Num.Bijective where

open import Data.Nat
open import Data.Fin as Fin using (Fin; #_; fromℕ≤)
open import Data.Fin.Extra
open import Data.Fin.Properties using (bounded)
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open import Level using () renaming (suc to lsuc)
open import Function
open import Relation.Nullary.Negation
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as PropEq

infixr 5 _∷_

-- For a system to be bijective wrt ℕ:
--  * base ≥ 1
--  * digits = {1 .. base}
data Bij : ℕ → Set where
    -- from the terminal object, which represents 0
    ∙ : ∀ {b}           -- base
        → Bij (suc b)   -- base ≥ 1

    -- successors
    _∷_ : ∀ {b}
        → Fin b         -- digit = {1 .. b}
        → Bij b → Bij b

infixr 9 _/_
-- syntax sugar for chaining digits with ℕ
_/_ : ∀ {b} → (n : ℕ)
    → {lower-bound : True (suc zero ≤? n)}      -- digit ≥ 1
    → {upper-bound : True (n        ≤? b)}      -- digit ≤ base
    → Bij b → Bij b
_/_ {b} zero    {()} {ub} ns
_/_ {b} (suc n) {lb} {ub} ns = (# n) {b} {ub} ∷ ns

module _/_-Examples where

    零 : Bij 2
    零 = ∙

    一 : Bij 2
    一 = 1 / ∙

    八 : Bij 3
    八 = 2 / 2 / ∙

八 : Bij 3
八 = 2 / 2 / ∙

open import Data.Nat.DM
open import Data.Nat.Properties using (≰⇒>)
open import Relation.Binary

-- a digit at its largest
full : ∀ {b} (x : Fin (suc b)) → Dec (Fin.toℕ {suc b} x ≡ b)
full {b} x = Fin.toℕ x ≟ b

-- a digit at its largest (for ℕ)
full-ℕ : ∀ b n → Dec (n ≡ b)
full-ℕ b n = n ≟ b

------------------------------------------------------------------------
-- Digit
------------------------------------------------------------------------

digit-toℕ : ∀ {b} → Fin b → ℕ
digit-toℕ x = suc (Fin.toℕ x)

digit+1-lemma : ∀ a b → a < suc b → a ≢ b → a < b
digit+1-lemma zero    zero    a<1+b a≢b = contradiction refl a≢b
digit+1-lemma zero    (suc b) a<1+b a≢b = s≤s z≤n
digit+1-lemma (suc a) zero    (s≤s ()) a≢b
digit+1-lemma (suc a) (suc b) (s≤s a<1+b) a≢b = s≤s (digit+1-lemma a b a<1+b (λ z → a≢b (cong suc z)))

digit+1 : ∀ {b} → (x : Fin (suc b)) → Fin.toℕ x ≢ b → Fin (suc b)
digit+1 {b} x ¬p = fromℕ≤ {digit-toℕ x} (s≤s (digit+1-lemma (Fin.toℕ x) b (bounded x) ¬p))

------------------------------------------------------------------------
-- Bij
------------------------------------------------------------------------

1+ : ∀ {b} → Bij (suc b) → Bij (suc b)
1+     ∙        = Fin.zero ∷ ∙
1+ {b} (x ∷ xs) with full x
1+ {b} (x ∷ xs) | yes p = Fin.zero ∷ 1+ xs
1+ {b} (x ∷ xs) | no ¬p = digit+1 x ¬p ∷ xs

n+ : ∀ {b} → ℕ → Bij (suc b) → Bij (suc b)
n+ zero    xs = xs
n+ (suc n) xs = 1+ (n+ n xs)

------------------------------------------------------------------------
-- From and to ℕ
------------------------------------------------------------------------

toℕ : ∀ {b} → Bij b → ℕ
toℕ ∙              = zero
toℕ {b} (x ∷ xs) = digit-toℕ x + (toℕ xs * b)

fromℕ : ∀ {b} → ℕ → Bij (suc b)
fromℕ zero    = ∙
fromℕ (suc n) = 1+ (fromℕ n)

------------------------------------------------------------------------
-- Functions on Bij
------------------------------------------------------------------------

-- infixl 6 _⊹_
--
-- _⊹_ : ∀ {b} → Bij b → Bij b → Bij b
-- _⊹_         ∙       ys        = ys
-- _⊹_         xs       ∙        = xs
-- _⊹_ {zero} (() ∷ xs) (y ∷ ys)
-- _⊹_ {suc b} (x ∷ xs) (y ∷ ys) with (suc (Fin.toℕ x + Fin.toℕ y)) divMod (suc b)
-- _⊹_ {suc b} (x ∷ xs) (y ∷ ys) | result quotient remainder property div-eq mod-eq =
--     remainder ∷ n+ quotient (xs ⊹ ys)

-- old base = suc b
-- new base = suc (suc b)
increase-base : ∀ {b} → Bij (suc b) → Bij (suc (suc b))
increase-base {b} ∙        = ∙
increase-base {b} (x ∷ xs) with fromℕ {suc b} (toℕ (increase-base xs) * suc b)
    | inspect (λ ws → fromℕ {suc b} (toℕ ws * suc b)) (increase-base xs)
increase-base {b} (x ∷ xs) | ∙      | [ eq ] = Fin.inject₁ x ∷ ∙
increase-base {b} (x ∷ xs) | y ∷ ys | [ eq ]
    with suc (Fin.toℕ x + Fin.toℕ y) divMod (suc (suc b))
increase-base {b} (x ∷ xs) | y ∷ ys | [ eq ]
    | result quotient remainder property div-eq mod-eq =
    remainder ∷ n+ quotient ys

-- old base = suc (suc b)
-- new base = suc b
decrease-base : ∀ {b} → Bij (suc (suc b)) → Bij (suc b)
decrease-base {b} ∙ = ∙
decrease-base {b} (x ∷ xs) with fromℕ {b} (toℕ (decrease-base xs) * suc (suc b))
              | inspect (λ ws → fromℕ {b} (toℕ ws * suc (suc b))) (decrease-base xs)
decrease-base {b} (x ∷ xs) | ∙      | [ eq ] with full x
decrease-base {b} (x ∷ xs) | ∙      | [ eq ] | yes p = Fin.zero ∷ Fin.zero ∷ ∙
decrease-base {b} (x ∷ xs) | ∙      | [ eq ] | no ¬p = inject-1 x ¬p ∷ ∙
decrease-base {b} (x ∷ xs) | y ∷ ys | [ eq ] with (suc (Fin.toℕ x + Fin.toℕ y)) divMod (suc b)
decrease-base (x ∷ xs) | y ∷ ys | [ eq ] | result quotient remainder property div-eq mod-eq
    = remainder ∷ n+ quotient ys

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module z-06 where

open import Data.Nat                              using (ℕ; zero; suc; _+_; _*_; _<?_; _<_; ≤-pred)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import      Relation.Binary.PropositionalEquality.Core as PE

{-
------------------------------------------------------------------------------
-- 267 p 6.2.2 Shortcuts.

C-c C-l       typecheck and highlight the current file
C-c C-,       get information about the hole under the cursor
C-c C-.       show inferred type for proposed term for a hole
C-c C-space   give a solution
C-c C-c       case analysis on a variable
C-c C-r       refine the hole
C-c C-a       automatic fill
C-c C-n       which normalizes a term (useful to test computations)
middle click  definition of the term

SYMBOLS

∧ \and
⊤ \top
→ \to
∀ \all
Π \Pi
λ \Gl
∨ \or
⊥ \bot
¬ \neg
∃ \ex
Σ \Sigma
≡ \equiv
ℕ \bN
× \times
≤ \le
∈ \in
⊎ \uplus
∷ \::
∎ \qed
x₁ \_1
x¹ \^1

------------------------------------------------------------------------------
-- p 268 6.2.3 The standard library.

default path /usr/share/agda-stdlib

Data.Empty    empty type (⊥)
Data.Unit     unit type (⊤)
Data.Bool     booleans
Data.Nat      natural numbers (ℕ)
Data.List     lists
Data.Vec      vectors (lists of given length)
Data.Fin      types with finite number of elements
Data.Integer  integers
Data.Float    floating point numbers
Data.Bin      binary natural numbers
Data.Rational rational numbers
Data.String   strings
Data.Maybe    option types
Data.AVL      balanced binary search trees

Data.Sum                               sum types (⊎, ∨)
Data.Product                           product types (×, ∧, ∃, Σ)
Relation.Nullary                       negation (¬)
Relation.Binary.PropositionalEquality  equality (≡)

------------------------------------------------------------------------------
-- p 277 6.3.4 Postulates.

for axioms (no proof)
avoide as much as possible
e.g, to work in classical logic, assume law of excluded middle with

postulate
  lem : (A : Set) → ¬ A ⊎ A

postulates do not compute:
- applying 'lem' to type A, will not reduce to ¬ A or A (as expected for a coproduct)
see section 6.5.6

------------------------------------------------------------------------------
-- p 277 6.3.5 Records.
-}

-- implementation of pairs using records
record Pair (A B : Set) : Set where
  constructor mkPair
  field
    fst : A
    snd : B

make-pair : {A B : Set} → A → B → Pair A B
make-pair a b = record { fst = a ; snd = b }

make-pair' : {A B : Set} → A → B → Pair A B
make-pair' a b = mkPair a b

proj1 : {A B : Set} → Pair A B → A
proj1 p = Pair.fst p

------------------------------------------------------------------------------
-- p 278 6.4 Inductive types: data
-- p 278 6.4.1 Natural numbers

{-
data ℕ : Set where
  zero :     ℕ -- base case
  suc  : ℕ → ℕ -- inductive case
-}

pred : ℕ → ℕ
pred  zero   = zero
pred (suc n) = n

_+'_ : ℕ → ℕ → ℕ
zero    +' n =          n
(suc m) +' n = suc (m +' n)
infixl 6  _+'_

_∸'_ : ℕ → ℕ → ℕ
zero  ∸'     n = zero
suc m ∸' zero  = suc m
suc m ∸' suc n = m ∸' n

_*'_ : ℕ → ℕ → ℕ
zero  *' n = zero
suc m *' n = (m *' n) + n

{-
_mod'_ :  ℕ → ℕ → ℕ
m mod' n with m <? n
m mod' n | yes _ = m
m mod' n | no  _ = (m ∸' n) mod' n
-}
-- TODO : what is going on here?
-- mod' :  ℕ → ℕ → ℕ
-- mod' m n with m <? n
-- ... | x = {!!}
{-
------------------------------------------------------------------------------
-- p 280 Empty pattern matching.

there is no case to pattern match on elements of this type
use on types with no elements, e.g.,
-}
data ⊥'  : Set where

-- given an element of type ⊥ then "produce" anything
-- uses pattern : () -- means that no such pattern can happen
⊥'-elim : {A : Set} → ⊥' → A
⊥'-elim ()

{-
since A is arbitrary, no way, in proof, to exhibit one.
Do not have to.
'()'  states no cases to handle, so done

Useful in negation and other less obvious ways of constructing empty inductive types.
E.g., the type zero ≡ suc zero of equalities between 0 and 1 is also an empty inductive type.
-}

{-
------------------------------------------------------------------------------
-- p 281 Anonymous pattern matching.
-}
-- curly brackets before args, cases separated by semicolons:
-- e.g.,

pred' : ℕ → ℕ
pred' = λ { zero → zero ; (suc n) → n }

{-
------------------------------------------------------------------------------
-- p 281  6.4.3 The induction principle.

pattern matching corresponds to the presence of a recurrence or induction principle

e.g.,
f : → A
f  zero   = t
f (suc n) = u' -- u' might be 'n' or result of recursive call f n

recurrence principle expresses this as
-}

rec : {A : Set} → A → (ℕ → A → A) → ℕ → A
rec t u  zero   = t
rec t u (suc n) = u n (rec t u n)

-- same with differenct var names
recℕ : {A : Set} → A → (ℕ → A → A) → ℕ → A
recℕ a n→a→a   zero  = a
recℕ a n→a→a (suc n) = n→a→a n (recℕ a n→a→a n)

{-
Same as "recursor" for including nats to simply typed λ-calculus in section 4.3.6.

Any function of type ℕ → A defined using pattern matching can be redefined using this function.
This recurrence function encapsulates the expressive power of pattern matching.
e.g.,
-}

pred'' : ℕ → ℕ
pred'' = rec zero (λ n _ → n)

_ : pred'' 2 ≡ rec zero (λ n _ → n) 2
_ = refl
_ :            rec zero (λ n _ → n) 2 ≡ 1
_ = refl
_ : pred'' 2                          ≡ 1
_ = refl

{-
logical : recurrence principle corresponds to elimination rule, so aka "eliminator"

Pattern matching in Agda is more powerful
- can be used to define functions whose return type depends on argument

means must consider functions of the form

f : (n : ℕ) -> P n    -- P : ℕ → Set
f  zero   = t         --   : P zero
f (suc n) = u n (f n) --   : P (suc n)

corresponding dependent variant of the recurrence principle is called the induction principle:
-}

rec' : (P : ℕ → Set)
     → P zero
     → ((n : ℕ) → P n → P (suc n))
     → (n : ℕ)
     → P n
rec' P Pz Ps  zero   = Pz
rec' P Pz Ps (suc n) = Ps n (rec' P Pz Ps n)

{-
reading type as a logical formula, it says the recurrence principle over natural numbers:

    P (0) ⇒ (∀n ∈ ℕ.P (n) ⇒ P (n + 1)) ⇒ ∀n ∈ ℕ.P (n)
-}

-- proof using recursion
+-zero' :    (n : ℕ) → n + zero ≡ n
+-zero'  zero   = refl
+-zero' (suc n) =                                  PE.cong suc (+-zero' n)

-- proof using dependent induction principle
+-zero'' :   (n : ℕ) → n + zero ≡ n
+-zero'' = rec' (λ n → n + zero ≡ n) refl (λ n p → PE.cong suc p)

_ : +-zero'' 2 ≡ refl
_ = refl
_ : rec' (λ n →             n + zero ≡ n) refl (λ n p → PE.cong suc p) ≡
          λ n → rec' (λ z → z + zero ≡ z) refl (λ n   → PE.cong (λ z → suc z)) n
_ = refl

------------------------------------------------------------------------------
-- p 282 Booleans

data Bool : Set where
  false : Bool
  true  : Bool

-- induction principle for booleans
Bool-rec : (P : Bool → Set) → P false → P true → (b : Bool) → P b
Bool-rec P Pf Pt false = Pf
Bool-rec P Pf Pt true  = Pt

------------------------------------------------------------------------------
-- p 283 Lists Data.List

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

length : {A : Set} → List A → ℕ
length      []  = 0
length (_ ∷ xs) = 1 + length xs

_++_ : {A : Set} → List A → List A → List A
[]       ++ l =            l
(x ∷ xs) ++ l = x ∷ (xs ++ l)

List-rec
  : {A : Set}
  → (P : List A → Set)
  → P []
  → ((x : A) → (xs : List A) → P xs → P (x ∷ xs))
  → (xs : List A)
  → P xs
List-rec P Pe Pc      []  = Pe
List-rec P Pe Pc (x ∷ xs) = Pc x xs (List-rec P Pe Pc xs)

------------------------------------------------------------------------------
-- p 284 6.4.7 Vectors.

data Vec (A : Set) : ℕ → Set where
  []  :                         Vec A  zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

{-
------------------------------------------------------------------------------
-- p 284 Dependent types.

type Vec A n depends on term n : a defining feature of dependent types.
-}

-- also, functions whose result type depends on argument, e.g.,
replicate : {A : Set} → A → (n : ℕ) → Vec A n
replicate x  zero   = []
replicate x (suc n) = x ∷ replicate x n

------------------------------------------------------------------------------
-- p 285 Dependent pattern matching.

-- since input is type Vec A (suc n), infers never applied to empty
head : {n : ℕ} {A : Set} → Vec A (suc n) → A
head (x ∷ xs) = x

------------------------------------------------------------------------------
-- p 285 Convertibility.

-- Agda is able to compare types up to β-reduction on terms (zero + n reduces to n):
-- - never distinguishes between two β-convertible terms

_++'_ : {m n : ℕ} {A : Set}
      → Vec A m → Vec A n → Vec A (m + n)
[]       ++' l = l                        -- Vec A (zero + n) ≡ Vec A n
(x ∷ xs) ++' l = x ∷ (xs ++' l)

------------------------------------------------------------------------------
-- p 285 Induction principle for Vec-rec

-- induction principle for vectors
Vec-rec : {A : Set}
        → (P : {n : ℕ} → Vec A n → Set)
        → P []
        → ({n : ℕ} → (x : A) → (xs : Vec A n) → P xs → P (x ∷ xs))
        → {n : ℕ}
        → (xs : Vec A n)
        → P xs
Vec-rec P Pe Pc      []  = Pe
Vec-rec P Pe Pc (x ∷ xs) = Pc x xs (Vec-rec P Pe Pc xs)

------------------------------------------------------------------------------
-- p 285 Indices instead of parameters.

-- general : can always encode a parameter as an index
-- recommended using parameters whenever possible (Agda handles them more efficiently)

-- use an index for type A (instead of a parameter)
data VecI : Set → ℕ → Set where
  []  : {A : Set} → VecI A zero
  _∷_ : {A : Set} {n : ℕ} (x : A) (xs : VecI A n) → VecI A (suc n)

-- induction principle for index VecI
VecI-rec : (P : {A : Set} {n : ℕ} → VecI A n → Set)
         → ({A : Set} → P {A} [])
         → ({A : Set} {n : ℕ} (x : A) (xs : VecI A n) → P xs → P (x ∷ xs))
         → {A : Set}
         → {n : ℕ}
         → (xs : VecI A n)
         → P xs
VecI-rec P Pe Pc      []  = Pe
VecI-rec P Pe Pc (x ∷ xs) = Pc x xs (VecI-rec P Pe Pc xs)

------------------------------------------------------------------------------
-- p 286 6.4.8 Finite sets.

-- has n elements
data Fin' : ℕ → Set where
  fzero' : {n : ℕ} →          Fin' (suc n)
  fsuc'  : {n : ℕ} → Fin' n → Fin' (suc n)

{-
Fin n is collection of ℕ restricted to Fin n = {0,...,n − 1}

above type corresponds to inductive set-theoretic definition:

    Fin      0  = ∅
    Fin (n + 1) = {0} ∪ {i + 1 | i ∈ Fin n}
-}

finToℕ : {n : ℕ} → Fin' n → ℕ
finToℕ  fzero'   = zero
finToℕ (fsuc' i) = suc (finToℕ i)

------------------------------------------------------------------------------
-- p 286 Vector lookup using Fin

-- Fin n typically used to index

-- type ensures index in bounds
lookup : {n : ℕ} {A : Set} → Fin' n → Vec A n → A
lookup  fzero'   (x ∷ xs) = x
lookup (fsuc' i) (x ∷ xs) = lookup i xs

-- where index can be out of bounds
open import Data.Maybe
lookup' : ℕ → {A : Set} {n : ℕ} → Vec A n → Maybe A
lookup'  zero       []  = nothing
lookup'  zero   (x ∷ l) = just x
lookup' (suc i)     []  = nothing
lookup' (suc i) (x ∷ l) = lookup' i l

-- another option : add proof of i < n
lookupP : {i n : ℕ} {A : Set}
        → i < n
        → Vec A n
        → A
lookupP     {i}       {.0}  ()     []
lookupP  {zero} {.(suc _)} i<n (x ∷ l) = x
lookupP {suc i} {.(suc _)} i<n (x ∷ l) = lookupP (≤-pred i<n) l

{-
------------------------------------------------------------------------------
-- p 287 6.5 Inductive types: logic

Use inductive types to implement types used as logical formulas,
though the Curry-Howard correspondence.

What follows is a dictionary between the two.

------------------------------------------------------------------------------
-- 6.5.1 Implication : corresponds to arrow (→) in types
-}

-- constant function
-- classical formula   A ⇒ B ⇒ A  proved by
K : {A B : Set} → A → B → A
K x y = x

-- composition
-- classical formula     (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C  proved by
S : {A B C : Set} → (A → B → C) → (A → B) → A → C
S g f x = g x (f x)

{-
------------------------------------------------------------------------------
-- 6.5.2 Product : corresponds to conjunction
defined in Data.Product
-}

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

-- aka fst
proj₁ : {A B : Set} → A × B → A
proj₁ (a , b) = a

-- aka snd
proj₂ : {A B : Set} → A × B → B
proj₂ (a , b) = b

-- proof of A ∧ B ⇒ B ∧ A (commutativity of conjunction)
×-comm : {A B : Set} → A × B → B × A
×-comm (a , b) = (b , a)

-- proof of curryfication
×-→ : {A B C : Set} → (A × B → C) → (A → B → C)
×-→ f x y = f (x , y)
-- and
→-× : {A B C : Set} → (A → B → C) → (A × B → C)
→-× f (x , y) = f x y

{-
introduction rule for conjunction:
    Γ ⊢ A    Γ ⊢ B
    -------------- (∧I)
    Γ ⊢ A      ∧ B

general : when logical connectives are defined with inductive types,
- CONSTRUCTORS CORRESPOND TO INTRODUCTION RULES

------------------------------------------------------------------------------
Induction principle : ELIMINATION RULE CORRESPONDS TO THE ASSOCIATED INDUCTION PRINCIPLE
-}

-- for case where P does not depend on its arg
×-rec : {A B : Set}
  → (P : Set)
  → (A → B → P)
  → A × B → P
×-rec P Pp (x , y) = Pp x y
{-
corresponds to elimination rule for conjunction:
    Γ, A,B ⊢ P      Γ ⊢ A ∧ B
    ------------------------- (∧E)
               Γ ⊢ P
if the premises are true then the conclusion is also true
-}
-- dependent induction principle
-- corresponds to the elimination rule in dependent types
-- see 8.3.3
×-ind : {A B : Set}
  → (P : A × B → Set)
  → ((x : A) → (y : B) → P (x , y))
  → (p : A × B) → P p
×-ind P Pp (x , y) = Pp x y

{-
------------------------------------------------------------------------------
-- p 289 6.5.3 Unit type : corresponds to truth
Data.Unit
-}

data ⊤ : Set where
  tt : ⊤ -- constructor is introduction rule

{-
    ----- (⊤I)
    Γ ⊢ ⊤
-}

-- induction principle
⊤-rec
  : (P : ⊤ → Set)
  → P tt
  → (t : ⊤)
  → P t
⊤-rec P Ptt tt = Ptt

{-
know from logic there is no elimination rule associated with truth

but can write rule that corresponds to induction principle:

    Γ ⊢ P    Γ ⊢ ⊤
    --------------- (⊤E)
         Γ ⊢ P

not interesting from a logical point of view:
if P holds and ⊤ holds
then can deduce that P holds, which was already known

------------------------------------------------------------------------------
-- 6.5.4 Empty type : corresponds to falsity
Data.Empty
-}

data ⊥ : Set where
  -- no constructor, so no introduction rule

-- dependent induction principle
⊥-d-elim : (P : ⊥ → Set) → (x : ⊥) → P x
⊥-d-elim P ()

-- non-dependent variant of this principle
⊥-elim : (P : Set) → ⊥ → P
⊥-elim P () -- () is the empty pattern in Agda
            -- indicates there are no cases to handle when matching on a value of type

{-
corresponds to explosion principle, which is the associated elimination rule

    Γ ⊢ ⊥
    ---- (⊥E)
    Γ ⊢ P

------------------------------------------------------------------------------
6.5.5 Negation
Relation.Nullary
-}

¬ : Set → Set
¬ A = A → ⊥

-- e.g., A ⇒ ¬¬A  proved:
nni : {A : Set} → A → ¬ (¬ A)
nni A ¬A = ¬A A

{-
------------------------------------------------------------------------------
p 290 6.5.6 Coproduct : corresponds to disjunction
Data.Sum
-}
data _⊎_ (A : Set) (B : Set) : Set where
  inj₁ : A → A ⊎ B -- called injection of A into A ⊎ B
  inj₂ : B → A ⊎ B -- ditto               B

{-
The two constructors correspond to the two introduction rules
    Γ ⊢ A
    --------- (∨ᴸI)
    Γ ⊢ A ∨ B

    Γ ⊢     B
    --------- (∨ᴿI)
    Γ ⊢ A ∨ B
-}

-- commutativity of disjunction
⊎-comm : (A B : Set) → A ⊎ B → B ⊎ A
⊎-comm A B (inj₁ x) = inj₂ x
⊎-comm A B (inj₂ y) = inj₁ y
{-
-- proof of (A ∨ ¬A) ⇒ ¬¬A ⇒ A
lem-raa : {A : Set}
  → A ⊎ ¬ A
  → ¬ (¬ A)
  → A
lem-raa (inj₁  a) _ = a
lem-raa (inj₂ ¬a) k = ⊥-elim (k ¬a) -- ⊥ !=< Set
-}
-- induction principle
⊎-rec : {A B : Set}
  → (P : A ⊎ B → Set)
  → ((x : A) → P (inj₁ x))
  → ((y : B) → P (inj₂ y))
  → (u : A ⊎ B)
  → P u
⊎-rec P P₁ P₂ (inj₁ x) = P₁ x
⊎-rec P P₁ P₂ (inj₂ y) = P₂ y
{-
non-dependent induction principle corresponds to the elimination rule
    Γ, A ⊢ P    Γ, B ⊢ P    Γ ⊢ A ∨ B
    ----------------------------- (∨E)
                   Γ ⊢ P

------------------------------------------------------------------------------
Decidable types : A type A is decidable when it is known whether it is inhabited or not
i.e. a proof of A ∨ ¬A

could define predicate: Dec A is a proof that A is decidable
-}
Dec' : Set → Set
Dec' A = A ⊎ ¬ A -- by definition of the disjunction
{-
Agda convention
  write yes/no instead of inj₁/inj₂
because it answers the question: is A provable?

defined in Relation.Nullary as

-- p 291
A type A is decidable when
-}
data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

{-
logic of Agda is intuitionistic
therefore A ∨ ¬A not provable for any type A, and not every type is decidable

it can be proved that no type is not decidable (see 2.3.5 and 6.6.8)
-}

nndec : (A : Set) → ¬ (¬ (Dec A))
nndec A n = n (no (λ a → n (yes a)))

{-
------------------------------------------------------------------------------
-- p 291 6.5.7 Π-types : corresponds to universal quantification

dependent types : types that depend on terms

some connectives support dependent generalizations

e.g., generalization of function types
  A → B
to dependent function types
  (x : A) → B
where x might occur in B.
the type B of the returned value depends on arg x

e.g.,

replicate : {A : Set} → A → (n : ℕ) → Vec A n

Dependent function types are also called Π-types

often written

    Π(x : A).B

can be define as (note: there is builtin notation in Agda)
-}
data Π {A : Set} (A : Set) (B : A → Set) : Set where
  Λ : ((a : A) → B a) → Π A B

{-
an element of Π A B is a dependent function

    (x : A) → B x

bound universal quantification bounded (the type A over which the variable ranges)

   corresponds to

    ∀x ∈ A.B(x)

proof of that formula corresponds to a function which
- to every x in A
- associates a proof of B(x)

why Agda allows the notation
    ∀ x → B x
for the above type (leaves A implicit)

Exercise 6.5.7.1.
Show that the type
     Π Bool (λ { false → A ; true → B })
is isomorphic to
     A × B

------------------------------------------------------------------------------
-- p 292 6.5.8 Σ-types : corresponds to bounded existential quantification
Data.Product
-}

-- dependent variant of product types : a : A , b : B a
data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → B a → Σ A B

-- actual Agda def is done using a record

dproj₁ : {A : Set} {B : A → Set} → Σ A B → A
dproj₁ (a , b) = a

dproj₂ : {A : Set} {B : A → Set} → (s : Σ A B) → B (dproj₁ s)
dproj₂ (a , b) = b

{-
Logical interpretation

type

    Σ A B

is bounded existential quantification

    ∃x ∈ A.B(x)

set theoretic interpretation corresponds to constructing sets by comprehension

    {x ∈ A | B(x)}

the set of elements x of A such that B(x) is satisfied

e.g., in set theory
- given a function f : A → B
- its image Im(f) is the subset of B consisting of elements in the image of f.

formally defined

     Im(f) = {y ∈ B | ∃x ∈ A.f (x) = y}

translated to with two Σ types
- one for the comprehension
- one for the universal quantification
-}
Im : {A B : Set} (f : A → B) → Set
Im {A} {B} f = Σ B (λ y → Σ A (λ x → f x ≡ y))

-- e.g., can show that every function f : A → B has a right inverse (or section)
-- g : Im(f) → A
sec : {A B : Set} (f : A → B) → Im f → A
sec f (y , (x , p)) = x

{-
------------------------------------------------------------------------------
-- p 293 : the axiom of choice

for every relation R ⊆ A × B satisfying ∀x ∈ A.∃y ∈ B.(x, y) ∈ R
there is a function f : A → B such that ∀x ∈ A.(x, f (x)) ∈ R

section 6.5.9 defined type Rel A B
corresponding to relations between types A and B

using Rel, can prov axiom of choice
-}
-- AC : {A B : Set} (R : Rel A B) -- TODO
--   → ((x : A) → Σ B (λ y → R x y))
--   → Σ (A → B) (λ f → ∀ x → R x (f x))
-- AC R f = (λ x → proj₁ (f x)) , (λ x → proj₂ (f x))
{-
the arg that corresponds to the proof of (6.1), is constructive
a function which to every element x of type A
associates a pair of an element y of B
and a proof that (x, y) belongs to the relation.

By projecting it on the first component,
necessary function f is obtained (associates an element of B to each element of A)

use the second component to prove that it satisfies the required property

the "classical" variant of the axiom of choice
does not have access to the proof of (6.1) -- it only knows its existence.

another description is thus
where the double negation has killed the contents of the proof, see section 2.5.9

postulate CAC : {A B : Set} (R : Rel A B)
  → ¬ ¬ ((x : A) → Σ B (λ y → R x y))
  → ¬ ¬ Σ (A → B) (λ f → ∀ x → R x (f x))
see 9.3.4.

------------------------------------------------------------------------------
-- p 293 : 6.5.9 Predicates

In classical logic, the set Bool of booleans is the set of truth values:
- a predicate on a set A can either be false or true
- modeled as a function A → Bool

In Agda/intuitionistic logic
- not so much interested in truth value of predicate
- but rather in its proofs
- so the role of truth values is now played by Set

predicate P on a type A is term of type

  A → Set

which to every element x of A associates the type of proofs of P x

------------------------------------------------------------------------------
-- p 294 Relations
Relation.Binary

In classical mathematics, a relation R on a set A is a subset of A × A (see A.1)

x of A is in relation with an element y when (x, y) ∈ R

relation on A can also be encoded as a function : A × A → 𝔹
or, curryfication,                              : A → A → 𝔹

in this representation, x is in relation with y when R(x, y) = 1

In Agda/intuitionistic
- relations between types A and B as type Rel A
- obtained by replacing the set 𝔹 of truth values with Set in the above description:
-}
Rel : Set → Set₁
Rel A = A → A → Set

-- e.g.
-- _≤_ : type Rel ℕ
-- _≡_ : type Rel A

{-
------------------------------------------------------------------------------
Inductive predicates (predicates defined by induction)
-}

data isEven : ℕ → Set where
  even-z : isEven zero                               --    0 is even
  even-s : {n : ℕ} → isEven n → isEven (suc (suc n)) -- if n is even then n + 2 is even
{-
corresponds to def of set E ⊆ N of even numbers
as the smallest set of numbers such that
    0 ∈ E
and
    n ∈ E ⇒ n+2 ∈ E
-}
data _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ}                 →  zero ≤     n
  s≤s : {m n : ℕ} (m≤n : m ≤ n) → suc m ≤ suc n
{-
smallest relation on ℕ such that
     0 ≤ 0
and
     m ≤ n implies m+1 ≤ n+1

inductive predicate definitions enable reasoning by induction over those predicates/relations
-}

≤-refl : {n : ℕ} → (n ≤ n)
≤-refl  {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

-- p 295

≤-trans : {m n p : ℕ} → (m ≤ n) → (n ≤ p) → (m ≤ p)
≤-trans      z≤n       n≤p  = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

{-
inductive defs good because of Agda's support for
reasoning by induction (and dependent pattern matching)
leading to simpler proofs

other defs possible

-- base on classical equivalence, for m, n ∈ N, m ≤ n ⇔ ∃m' ∈ N.m + m' = n
_≤'_ : ℕ → ℕ → Set
m ≤' n = Σ (λ m' → m + m' ≡eq n)

another:
-}
le : ℕ → ℕ → Bool
le   zero       n  = true
le (suc m)   zero  = false
le (suc m) (suc n) = le m n

_≤'_ : ℕ → ℕ → Set
m ≤' n = le m n ≡ true

{-
EXERCISE : show reflexivity and transitivity with the alternate formalizations

involved example
implicational fragment of intuitionistic natural deduction is formalized in section 7.2
the relation Γ ⊢ A
between a context Γ and a type A
which is true when the sequent is provable
is defined inductively

------------------------------------------------------------------------------
-- p 295 6.6 Equality
Relation.Binary.PropositionalEquality

-- typed equality : compare elements of same type
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x -- only way to be equal is to be the same

------------------------------------------------------------------------------
6.6.1 Equality and pattern matching

example proof with equality : successor function on natural numbers is injective
- for every natural numbers m and n
- m + 1 = n + 1 ⇒ m = n
-}

-- p 296

suc-injective : {m n : ℕ} → suc m ≡ suc n → m ≡ n
-- suc-injective {m} {n} p  -- Goal: m ≡ n;   p : suc m ≡ suc n
                            -- case split on p : it can ONLY be refl
                            -- therefore m is equal to n
                            -- so agda provide .m - not really an arg - something equal to m
suc-injective {m} {.m} refl --       m ≡ m
  = refl

{-
------------------------------------------------------------------------------
-- p 296 6.6.2 Main properties of equality: reflexive, congruence, symmetric, transitive
-}

sym : {A : Set} {x y : A}
  → x ≡ y
  → y ≡ x
sym refl = refl

trans : {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
  → x ≡ z
trans refl refl = refl

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

-- substitutivity : enables transporting the elements of a type along an equality
{-
subst : {A : Set} (P : A → Set) → {x y : A}
  →   x ≡ y
  → P x
  → P     y
subst P refl p = p
-}
-- https://stackoverflow.com/a/27789403
subst : ∀ {a p} {A : Set a} (P : A → Set p) {x y : A}
      → x ≡ y → P x → P y
subst P refl p = p

-- coercion : enables converting an element of type to another equal type
coe : {A B : Set}
  → A ≡ B
  → A
  → B
coe p x = subst (λ A → A) p x

-- see 9.1

{-
------------------------------------------------------------------------------
-- p 296 6.6.3 Half of even numbers : example every even number has a half
using proof strategy from 2.3

traditional notation : show  ∀n ∈ N. isEven(n) ⇒ ∃m ∈ ℕ.m + m = n
-}

+-suc : ∀ (m n : ℕ)
      →      m + suc n
      ≡ suc (m +     n)
+-suc  zero   n = refl
+-suc (suc m) n = cong suc (+-suc m n)

-- even-half : {n : ℕ}
--   → isEven n
--   → Σ (λ m → m + m ≡ n) -- TODO (m : ℕ) → Set !=< Set
-- even-half  even-z = zero , refl
-- even-half (even-s e) with even-half e
-- even-half (even-s e) | m , p =
--   suc m , cong suc (trans (+-suc m m) (cong suc p))

{-
second case : by induction have m such that m + m = n
need to construct a half for n + 2: m + 1
show that it is a half via

    (m + 1) + (m + 1) =  (m + (m  + 1)) + 1   by definition of addition
                      = ((m +  m) + 1)  + 1   by +-suc
                      =       (n  + 1)  + 1   since m + m = n

implemented using transitivity of equality and
fact that it is a congruence (m + 1 = n + 1 from m = n)
also use auxiliary lemma m + (n + 1) = (m + n) + 1
-}

{-
------------------------------------------------------------------------------
-- p 297 6.6.4 Reasoning
-}

--import      Relation.Binary.PropositionalEquality as Eq
--open        Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

infix  3 _∎
infixr 2 _≡⟨⟩_ _≡⟨_⟩_
infix  1 begin_

begin_ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → x ≡ y
begin_ x≡y = x≡y

_≡⟨⟩_ : ∀ {ℓ} {A : Set ℓ} (x {y} : A) → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y

_≡⟨_⟩_ : {A : Set} (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

_∎ : ∀ {ℓ} {A : Set ℓ} (x : A) → x ≡ x
_∎ _ = refl

+-zero : ∀ (n : ℕ) → n + zero ≡ n
+-zero   zero  = refl
+-zero (suc n) rewrite +-zero n = refl

+-comm : (m n : ℕ) → m + n ≡ n + m
+-comm m zero    = +-zero m
+-comm m (suc n) =
  begin
    (m + suc n) ≡⟨ +-suc m n ⟩             -- m + (n + 1) = (m + n) + 1 -- by +-suc
    suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩ -- = (n + m) + 1 -- by induction hypothesis
    suc (n + m)
  ∎

-- p 297
-- another proof using properties of equality
+-comm' : (m n : ℕ) → m + n ≡ n + m
+-comm' m   zero  = +-zero m
+-comm' m (suc n) = trans (+-suc m n) (cong suc (+-comm m n))

{-
------------------------------------------------------------------------------
-- p 298 6.6.5 Definitional equality

two terms which are convertible (i.e. re duce to a common term) are considered to be EQUAL.

not ≡, but equality internal to Agda, referred to as definitional equality
- cannot distinguish between two definitionally equal terms
- e.g., zero + n is definitionally equal to n (because addition defined that way)
- definitional equality implies equality by refl:
-}

+-zero''' : (n : ℕ) → zero + n ≡ n
+-zero''' n = refl

-- n + zero and n are not definitionally equal (because def of addition)
-- but can be proved
+-0 : (n : ℕ) → n + zero ≡ n
+-0  zero   = refl
+-0 (suc n) = cong suc (+-zero n)

-- implies structure of definitions is important (and an art form)

------------------------------------------------------------------------------
-- p 298 6.6.6 More properties with equality

-- zero is NOT the successor of any NAT
zero-suc : {n : ℕ} → zero ≡ suc n → ⊥
zero-suc ()

+-assoc : (m n o : ℕ) → (m + n) + o ≡ m + (n + o)
+-assoc  zero   n o = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)

-- p 299
*-+-dist-r : (m n o : ℕ)
           → (m + n) * o ≡ m * o + n * o
*-+-dist-r  zero   n o = refl
*-+-dist-r (suc m) n o
  rewrite
    +-comm n o
  | *-+-dist-r m n o
  | +-assoc o (m * o) (n * o)
  = refl

*-assoc : (m n o : ℕ) → (m * n) * o ≡ m * (n * o)
*-assoc  zero   n o = refl
*-assoc (suc m) n o
  rewrite
    *-+-dist-r n (m * n) o
  | *-assoc m n o
  = refl

------------------------------------------------------------------------------
-- p 299 Lists

++-empty' : {A : Set}
          → (l : List A)
          → [] ++ l ≡ l
++-empty' l = refl

empty-++ : {A : Set}
          → (l : List A)
          → l ++ [] ≡ l
empty-++     []  = refl
empty-++ (x ∷ l) = cong (x ∷_) (empty-++ l)

++-assoc : {A : Set}
         → (l1 l2 l3 : List A)
         → ((l1 ++ l2) ++ l3) ≡ (l1 ++ (l2 ++ l3))
++-assoc      []  l2 l3 = refl
++-assoc (x ∷ l1) l2 l3 = cong (x ∷_) (++-assoc l1 l2 l3)

-- TODO DOES NOT COMPILE: Set₁ != Set
-- ++-not-comm : ¬ ({A : Set} → (l1 l2 : List A)
--                  → (l1 ++ l2) ≡ (l2 ++ l1))
-- ++-not-comm f with f (1 ∷ []) (2 ∷ [])
-- ... | ()

++-length : {A : Set}
          → (l1 l2 : List A)
          → length (l1 ++ l2) ≡ length l1 + length l2
++-length      []  l2 = refl
++-length (x ∷ l1) l2 = cong (1 +_) (++-length l1 l2)

-- p 300

-- adds element to end of list
snoc : {A : Set} → List A → A → List A
snoc     []  x = x ∷ []
snoc (y ∷ l) x = y ∷ (snoc l x)

-- reverse a list
rev : {A : Set} → List A → List A
rev     []  = []
rev (x ∷ l) = snoc (rev l) x

-- reversing a list with x as the last element will prodice a list with x as the first element
rev-snoc : {A : Set}
         → (l : List A) → (x : A)
         → rev (snoc l x) ≡ x ∷ (rev l)
rev-snoc     []  x = refl
rev-snoc (y ∷ l) x = cong (λ l → snoc l y) (rev-snoc l x)

-- reverse twice
rev-rev : {A : Set}
        → (l : List A)
        → rev (rev l) ≡ l
rev-rev     []  = refl
rev-rev (x ∷ l) = trans (rev-snoc (rev l) x)
                        (cong (x ∷_) (rev-rev l))

--------------------------------------------------
-- p 300 6.6.7 The J rule.

-- equality
data _≡'_ {A : Set} : A → A → Set where
  refl' : {x : A} → x ≡' x

-- has associated induction principle :  J rule:
-- to prove P depending on equality proof p,
-- - prove it when this proof is refl
J : {A : Set} {x y : A}
    (p : x ≡' y)
    (P : (x y : A) → x ≡' y → Set)
    (r : (x : A)   → P x x refl')
  → P x y p
J {A} {x} {.x} refl' P r = r x

{-
section 6.6 shows that definition usually taken in Agda is different
(it uses a parameter instead of an index for the first argument of type A),
so that the resulting induction principle is a variant:
-}

J' : {A : Set}
     (x : A)
     (P : (y : A) → x ≡' y → Set)
     (r : P x refl')
     (y : A)
     (p : x ≡' y)
   → P y p
J' x P r .x refl' = r

{-
--------------------------------------------------
p 301 6.6.8 Decidable equality.

A type A is decidable when either A or ¬A is provable.

Write Dec A for the type of proofs of decidability of A
- yes p, where p is a proof of  A, or
- no  q, where q is a proof of ¬A

A relation on a type A is decidable when
- the type R x y is decidable
- for every elements x and y of type A.
-}

-- in Relation.Binary
-- term of type Decidable R is proof that relation R is decidable
Decidable : {A : Set} (R : A → A → Set) → Set
Decidable {A} R = (x y : A) → Dec (R x y)

{-
A type A has decidable equality when equality relation _≡_ on A is decidable.
- means there is a function/algorithm able to determine,
  given two elements of A,
  whether they are equal or not
- return a PROOF (not a boolean)
-}

_≟_ : Decidable {A = Bool} _≡_
false ≟ false = yes refl
true  ≟ true  = yes refl
false ≟ true  = no (λ ())
true  ≟ false = no (λ ())

_≟ℕ_ : Decidable {A = ℕ} _≡_
zero  ≟ℕ zero  = yes refl
zero  ≟ℕ suc n = no(λ())
suc m ≟ℕ zero  = no(λ())
suc m ≟ℕ suc n with m ≟ℕ n
... | yes refl = yes refl
... | no  ¬p   = no (λ p → ¬p (suc-injective p))

{-
--------------------------------------------------
p 301 6.6.9 Heterogeneous equality : enables comparing (seemingly) distinct types

due to McBride [McB00]

p 302

e.g., show concatenation of vectors is associative

    (l1 ++ l2) ++ l3 ≡ l1 ++ (l2 ++ l3) , where lengths are m, n and o

equality ≡ only used on terms of same type
- but types above are
- left   Vec A ((m + n) + o)
- right  Vec A (m + (n + o))

the two types are propositionally equal, can prove

   Vec A ((m + n) + o) ≡ Vec A (m + (n + o))

by

  cong (Vec A) (+-assoc m n o)

but the two types are not definitionally equal (required to compare terms with ≡)

PROOF WITH STANDARD EQUALITY.

To compare vecs, use above propositional equality
and'coe' to cast one of the members to the same type as other.
   term
      coe (cong (Vec A) (+-assoc m n o))
has type
      Vec A ((m + n) + o) → Vec A (m + (n + o))
-}

-- lemma : if l and l’ are propositional equal vectors,
-- up to propositional equality of their types as above,
-- then x : l and x : l’ are also propositionally equal:
∷-cong : {A : Set} → {m n : ℕ} {l1 : Vec A m} {l2 : Vec A n}
       → (x : A)
       → (p : m ≡ n)
       → coe (PE.cong (Vec A) p) l1 ≡ l2
       → coe (PE.cong (Vec A) (PE.cong suc p)) (x ∷ l1) ≡ x ∷ l2
∷-cong x refl refl = refl

-- TODO this needs Vec ++ (only List ++ in scope)
-- ++-assoc' : {A : Set} {m n o : ℕ}
--           → (l1 : Vec A m)
--           → (l2 : Vec A n)
--           → (l3 : Vec A o)
--           → coe (PE.cong (Vec A) (+-assoc m n o))
--                 ((l1 ++ l2) ++ l3) ≡ l1 ++ (l2 ++ l3)
-- ++-assoc'                          []  l2 l3 = refl
-- ++-assoc' {_} {suc m} {n} {o} (x ∷ l1) l2 l3 = ∷-cong x (+-assoc m n o) (++-assoc' l1 l2 l3)

{-
p 303 Proof with heterogeneous equality - TODO

------------------------------------------------------------------------------
p 303 6.7 Proving programs in practice

correctness means it agrees with a specification

correctness properties
- absence of errors : uses funs with args in correct domain (e.g., no divide by zero)
- invariants : properties always satisfied during execution
- functional properties : computes expected output on any given input

p 304 6.7.1 Extrinsic vs intrinsic proofs

extrinsic : first write program then prove properties about it (from "outside") e.g., sort : List ℕ →     List ℕ
intrinsic : incorporate properties in types                                     e.g., sort : List ℕ → SortList ℕ

example: length of concat of two lists is sum of their lengths
-}
-- extrinsic proof
++-length' : {A : Set}
           → (l1 l2 : List A)
           → length (l1 ++ l2) ≡ length l1 + length l2
++-length'      []  l2 = refl
++-length' (x ∷ l1) l2 = PE.cong suc (++-length' l1 l2)

-- intrinsic
_V++_ : {m n : ℕ} {A : Set} → Vec A m → Vec A n → Vec A (m + n)
[]      V++ l  = l
(x ∷ l) V++ l' = x ∷ (l V++ l')

------------------------------------------------------------------------------
-- p 305 6.7.2 Insertion sort

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

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

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


text:
module TrustMe where

open import Data.String
open import Data.String.Unsafe
open import Data.Unit.Polymorphic using (⊤)
open import IO
import IO.Primitive as Prim
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

-- Check that trustMe works.

testTrustMe : IO ⊤
testTrustMe with "apa" ≟ "apa"
... | yes refl = putStrLn "Yes!"
... | no  _    = putStrLn "No."

main : Prim.IO ⊤
main = run testTrustMe

max_forks_repo_name: shlevy/agda


text:
-- Mapping of Haskell types to Agda Types
module Foreign.Haskell.Types where

open import Prelude
open import Builtin.Float

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

HSUnit = ⊤
HSBool = Bool
HSInteger = Int

HSList = List

HSChar = Char
HSString = HSList HSChar
HSText = String

postulate
  HSFloat : Set
  HSFloat=>Float : HSFloat → Float
  lossyFloat=>HSFloat : Float → HSFloat

  HSInt : Set
  HSInt=>Int : HSInt → Int
  lossyInt=>HSInt : Int → HSInt

{-# COMPILE GHC HSFloat = type Float #-}
{-# COMPILE GHC HSFloat=>Float = GHC.Float.float2Double #-}
{-# COMPILE GHC lossyFloat=>HSFloat = GHC.Float.double2Float #-}
{-# COMPILE GHC HSInt = type Int #-}
{-# COMPILE GHC HSInt=>Int = toInteger #-}
{-# COMPILE GHC lossyInt=>HSInt = fromInteger #-}

{-# FOREIGN GHC type AgdaTuple a b c d = (c, d) #-}

data HSTuple {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  _,_ : A → B → HSTuple A B
{-# COMPILE GHC HSTuple = data MAlonzo.Code.Foreign.Haskell.Types.AgdaTuple ((,)) #-}

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
open import Prelude

module Implicits.Resolution.Termination.Lemmas
  where

open import Induction.WellFounded
open import Induction.Nat
open import Data.Fin.Substitution
open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties
open import Relation.Binary using (module DecTotalOrder)
open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl)
open import Extensions.Nat

open import Implicits.Resolution.Termination.Lemmas.SizeMeasures public
-- open import Implicits.Resolution.Termination.Lemmas.Stack public


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

open import Groups.Definition
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Rings.Definition
open import Rings.Orders.Partial.Definition

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

module Rings.Orders.Total.Definition {n m : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} where

open Ring R
open Group additiveGroup
open Setoid S

record TotallyOrderedRing {p : _} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S _<_} (pRing : PartiallyOrderedRing R pOrder) : Set (lsuc n ⊔ m ⊔ p) where
  field
    total : SetoidTotalOrder pOrder
  open SetoidPartialOrder pOrder


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

open import HoTT
open import cohomology.FunctionOver
open import cohomology.FlipPushout

module cohomology.CofiberSequence {i} where

{- Lemma: pushing flip-susp through susp-fmap -}
flip-susp-fmap : {A B : Type i} (f : A → B)
  → ∀ σ → flip-susp (susp-fmap f σ) == susp-fmap f (flip-susp σ)
flip-susp-fmap f = Suspension-elim idp idp $ λ y → ↓-='-in $
  ap-∘ (susp-fmap f) flip-susp (merid y)
  ∙ ap (ap (susp-fmap f)) (FlipSusp.merid-β y)
  ∙ ap-! (susp-fmap f) (merid y)
  ∙ ap ! (SuspFmap.merid-β f y)
  ∙ ! (FlipSusp.merid-β (f y))
  ∙ ! (ap (ap flip-susp) (SuspFmap.merid-β f y))
  ∙ ∘-ap flip-susp (susp-fmap f) (merid y)

{- Useful abbreviations -}
module _ {X Y : Ptd i} (f : fst (X ⊙→ Y)) where

  ⊙Cof² = ⊙Cof (⊙cfcod' f)
  ⊙cfcod² = ⊙cfcod' (⊙cfcod' f)
  cfcod² = fst ⊙cfcod²
  ⊙Cof³ = ⊙Cof ⊙cfcod²
  ⊙cfcod³ = ⊙cfcod' ⊙cfcod²
  cfcod³ = fst ⊙cfcod³

{- For [f : X → Y], the cofiber space [Cof(cfcod f)] is equivalent to
 - [Suspension X]. This is essentially an application of the two pushouts
 - lemma:
 -
 -       f
 -   X ––––> Y ––––––––––––––> ∙
 -   |       |                 |
 -   |       |cfcod f          |
 -   v       v                 v
 -   ∙ ––> Cof f ––––––––––> Cof² f
 -                cfcod² f
 -
 - The map [cfcod² f : Cof f → Cof² f] becomes [ext-glue : Cof f → ΣX],
 - and the map [ext-glue : Cof² f → ΣY] becomes [susp-fmap f : ΣX → ΣY].
 -}
module Cof² {X Y : Ptd i} (f : fst (X ⊙→ Y)) where

  module Equiv {X Y : Ptd i} (f : fst (X ⊙→ Y)) where

    module Into = CofiberRec {f = cfcod' (fst f)} {C = fst (⊙Susp X)}
      south ext-glue (λ _ → idp)

    into = Into.f

    ⊙into : fst (⊙Cof² f ⊙→ ⊙Susp X)
    ⊙into = (into , ! (merid (snd X)))

    module Out = SuspensionRec {C = fst (⊙Cof² f)}
      (cfcod cfbase) cfbase
      (λ x → ap cfcod (cfglue x) ∙ ! (cfglue (fst f x)))

    out = Out.f

    into-out : ∀ σ → into (out σ) == σ
    into-out = Suspension-elim idp idp
      (λ x → ↓-∘=idf-in into out $
        ap (ap into) (Out.merid-β x)
        ∙ ap-∙ into (ap cfcod (cfglue x)) (! (cfglue (fst f x)))
        ∙ ap (λ w → ap into (ap cfcod (cfglue x)) ∙ w)
             (ap-! into (cfglue (fst f x)) ∙ ap ! (Into.glue-β (fst f x)))
        ∙ ∙-unit-r _
        ∙ ∘-ap into cfcod (cfglue x) ∙ ExtGlue.glue-β x)

    out-into : ∀ κ → out (into κ) == κ
    out-into = Cofiber-elim {f = cfcod' (fst f)}
      idp
      (Cofiber-elim {f = fst f} idp cfglue
        (λ x → ↓-='-from-square $
          (ap-∘ out ext-glue (cfglue x)
           ∙ ap (ap out) (ExtGlue.glue-β x) ∙ Out.merid-β x)
          ∙v⊡ (vid-square {p = ap cfcod (cfglue x)}
               ⊡h rt-square (cfglue (fst f x)))
          ⊡v∙ ∙-unit-r _))
      (λ y → ↓-∘=idf-from-square out into $
         ap (ap out) (Into.glue-β y) ∙v⊡ connection)

    eq = equiv into out into-out out-into

    space-path : ⊙Cof² f == ⊙Susp X
    space-path = ⊙ua (⊙≃-in eq (! (merid (snd X))))

  cfcod²-over : cfcod² f == ext-glue
                [ (λ U → fst (⊙Cof f) → fst U) ↓ Equiv.space-path f ]
  cfcod²-over = ↓-cst2-in _ _ $ codomain-over-equiv (cfcod² f) _

  cfcod³-over : ext-glue == flip-susp ∘ susp-fmap (fst f)
                [ (λ U → fst U → fst (⊙Susp Y)) ↓ Equiv.space-path f ]
  cfcod³-over = ↓-cst2-in _ _ $
    domain!-over-equiv ext-glue _ ▹ λ= lemma
    where
    lemma : (σ : fst (⊙Susp X))
      → ext-glue (Equiv.out f σ) == flip-susp (susp-fmap (fst f) σ)
    lemma = Suspension-elim idp idp
      (λ x → ↓-='-in $
        ap-∘ flip-susp (susp-fmap (fst f)) (merid x)
        ∙ ap (ap flip-susp) (SuspFmap.merid-β (fst f) x)
        ∙ FlipSusp.merid-β (fst f x)
        ∙ ! (ap-∘ ext-glue (Equiv.out f) (merid x)
             ∙ ap (ap ext-glue) (Equiv.Out.merid-β f x)
             ∙ ap-∙ ext-glue (ap cfcod (cfglue x))
                             (! (cfglue (fst f x)))
             ∙ (∘-ap ext-glue cfcod (cfglue x)
                ∙ ap-cst south (cfglue x))
               ∙2
               (ap-! ext-glue (cfglue (fst f x))
                ∙ ap ! (ExtGlue.glue-β (fst f x)))))

  open Equiv f public

cofiber-sequence : {X Y : Ptd i} (f : fst (X ⊙→ Y)) → Path
  {A = Σ (Ptd i × Ptd i)
         (λ {(U , V) → (fst (⊙Cof f) → fst U) × (fst U → fst V)})}
  ((⊙Cof² f , ⊙Cof³ f) , cfcod² f , cfcod³ f)
  ((⊙Susp X , ⊙Susp Y) , ext-glue , susp-fmap (fst f))
cofiber-sequence {X} {Y} f =
    ap (λ {(Z , g) → ((⊙Cof² f , Z) , cfcod² f , g)})
       (pair= (Cof².space-path (⊙cfcod' f)) (Cof².cfcod²-over (⊙cfcod' f)))
  ∙ ap (λ {(Z , g , h) → ((Z , ⊙Susp Y) , g , h)})
       (pair= (Cof².space-path f)
         (↓-×-in (Cof².cfcod²-over f) (Cof².cfcod³-over f)))
  ∙ ap (λ {(Z , g) → ((⊙Susp X , Z) , ext-glue , g)})
       (pair= (flip-⊙pushout-path (suspension-⊙span Y))
              (↓-cst2-in _ _ $ codomain!-over-equiv _ _))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- Andreas, 2016-06-20
-- Issue #436 fixed by Ulf's instantiating parameters sprint
-- (Agda meeting April 2016 Strathclyde)

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

foo : {A : Set} (x y : A) -> x == y -> A
foo x y = \ { eq → {!eq!} } -- load and do C-c C-c in the shed

-- Should work now (and is justified by new semantics).

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe --warning=error --without-K #-}
-- These are explicitly with-K, because we currently encode an element of Zn as
-- a natural together with a proof that it is small.

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Semirings.Definition
open import Orders.Total.Definition
open import Numbers.Modulo.Definition
open import Numbers.Modulo.ModuloFunction
open import Numbers.Naturals.Order.Lemmas

module Numbers.Modulo.Addition where
open TotalOrder ℕTotalOrder

_+n_ : {n : ℕ} .(pr : 0 <N n) → ℤn n pr → ℤn n pr → ℤn n pr
_+n_ {n} pr a b = record { x = mod n pr (ℤn.x a +N ℤn.x b) ; xLess = mod<N pr _ }

plusZnIdentityRight : {n : ℕ} → .(pr : 0 <N n) → (a : ℤn n pr) → (_+n_ pr a record { x = 0 ; xLess = pr }) ≡ a
plusZnIdentityRight 0<n record { x = x ; xLess = xLess } rewrite Semiring.sumZeroRight ℕSemiring x = equalityZn (modIsMod 0<n x (<NProp xLess))

plusZnIdentityLeft : {n : ℕ} → .(pr : 0 <N n) → (a : ℤn n pr) → _+n_ pr (record { x = 0 ; xLess = pr }) a ≡ a
plusZnIdentityLeft 0<n record { x = x ; xLess = xLess } = equalityZn (modIsMod 0<n x (<NProp xLess))

plusZnCommutative : {n : ℕ} → .(pr : 0 <N n) → (a b : ℤn n pr) → _+n_ pr a b ≡ _+n_ pr b a
plusZnCommutative {n} 0<n a b = equalityZn (applyEquality (mod n 0<n) (Semiring.commutative ℕSemiring (ℤn.x a) _))

plusZnAssociative' : {n : ℕ} → .(pr : 0 <N n) → {a b c : ℕ} → (a <N n) → (b <N n) → (c <N n) → mod n pr ((mod n pr (a +N b)) +N c) ≡ mod n pr (a +N (mod n pr (b +N c)))
plusZnAssociative' 0<n {a} {b} {c} a<n b<n c<n with modAddition 0<n a<n b<n
plusZnAssociative' {n} 0<n {a} {b} {c} a<n b<n c<n | inl a+b=mod with modAddition 0<n b<n c<n
... | inl b+c=mod rewrite equalityCommutative (a+b=mod) | equalityCommutative (b+c=mod) = applyEquality (mod _ 0<n) (equalityCommutative (Semiring.+Associative ℕSemiring a b c))
... | inr b+c=n+mod rewrite equalityCommutative (a+b=mod) | equalityCommutative (modAnd+n 0<n (a +N mod _ 0<n (b +N c))) | Semiring.+Associative ℕSemiring n a (mod _ 0<n (b +N c)) | Semiring.commutative ℕSemiring n a | equalityCommutative (Semiring.+Associative ℕSemiring a n (mod _ 0<n (b +N c))) | equalityCommutative b+c=n+mod = applyEquality (mod _ 0<n) (equalityCommutative (Semiring.+Associative ℕSemiring a b c))
plusZnAssociative' 0<n {a} {b} {c} a<n b<n c<n | inr a+b=n+mod with modAddition 0<n b<n c<n
plusZnAssociative' {n} 0<n {a} {b} {c} a<n b<n c<n | inr a+b=n+mod | inl b+c=mod rewrite equalityCommutative b+c=mod | equalityCommutative (modAnd+n 0<n (mod _ 0<n (a +N b) +N c)) | Semiring.+Associative ℕSemiring n (mod _ 0<n (a +N b)) c | equalityCommutative a+b=n+mod = applyEquality (mod _ 0<n) (equalityCommutative (Semiring.+Associative ℕSemiring a b c))
plusZnAssociative' {n} 0<n {a} {b} {c} a<n b<n c<n | inr a+b=n+mod | inr b+c=n+mod rewrite equalityCommutative (modAnd+n 0<n ((mod _ 0<n (a +N b)) +N c)) | equalityCommutative (modAnd+n 0<n (a +N mod _ 0<n (b +N c))) | Semiring.+Associative ℕSemiring n (mod _ 0<n (a +N b)) c | equalityCommutative (a+b=n+mod) | Semiring.commutative ℕSemiring a (mod n 0<n (b +N c)) | Semiring.+Associative ℕSemiring n (mod n 0<n (b +N c)) a | equalityCommutative b+c=n+mod | Semiring.commutative ℕSemiring (b +N c) a = applyEquality (mod _ 0<n) (equalityCommutative (Semiring.+Associative ℕSemiring a b c))

plusZnAssociative : {n : ℕ} → .(pr : 0 <N n) → (a b c : ℤn n pr) → _+n_ pr (_+n_ pr a b) c ≡ _+n_ pr a (_+n_ pr b c)
plusZnAssociative {succ n} 0<sn record { x = a ; xLess = aLess } record { x = b ; xLess = bLess } record { x = c ; xLess = cLess } = equalityZn t
  where
    ma = mod (succ n) 0<sn a
    mb = mod (succ n) 0<sn b
    mc = mod (succ n) 0<sn c
    v : mod (succ n) 0<sn ((mod (succ n) 0<sn (ma +N mb)) +N mc) ≡ mod (succ n) 0<sn (ma +N mod (succ n) 0<sn (mb +N mc))
    v = plusZnAssociative' 0<sn (mod<N 0<sn a) (mod<N 0<sn b) (mod<N 0<sn c)
    u : mod (succ n) 0<sn ((mod (succ n) 0<sn (mod (succ n) 0<sn a +N (mod (succ n) 0<sn b))) +N c) ≡ mod (succ n) 0<sn (a +N mod (succ n) 0<sn ((mod (succ n) 0<sn b) +N (mod (succ n) 0<sn c)))
    u rewrite equalityCommutative (modIsMod 0<sn c (<NProp cLess)) | equalityCommutative (modIsMod 0<sn a (<NProp aLess)) | modIdempotent 0<sn a | modIdempotent 0<sn c = v
    t : mod (succ n) 0<sn (mod (succ n) 0<sn (a +N b) +N c) ≡ mod (succ n) 0<sn (a +N mod (succ n) 0<sn (b +N c))
    t rewrite modExtracts {succ n} 0<sn a b | modExtracts {succ n} 0<sn b c = u


text:
module Prelude where

infixr 90 _∘_
infixr 0 _$_

id : {A : Set} -> A -> A
id x = x

_∘_ : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
(f ∘ g) x = f (g x)

_$_ : {A B : Set} -> (A -> B) -> A -> B
f $ x = f x

flip : {A B C : Set} -> (A -> B -> C) -> B -> A -> C
flip f x y = f y x

const : {A B : Set} -> A -> B -> A
const x _ = x

typeOf : {A : Set} -> A -> Set
typeOf {A} _ = A

typeOf1 : {A : Set1} -> A -> Set1
typeOf1 {A} _ = A


text:
{-# OPTIONS --without-K #-}
module HoTT.Sigma.Transport where

open import HoTT.Base
open import HoTT.Identity
open import HoTT.Identity.Sigma

Σ-transport : ∀ {i j k} {A : 𝒰 i} {P : A → 𝒰 j} {Q : (Σ A λ x → P x) → 𝒰 k} {x y : A} →
              (p : x == y) (uz : Σ (P x) λ u → Q (x , u)) →
              transport (λ x → Σ (P x) λ u → Q (x , u)) p uz ==
                transport _ p (pr₁ uz) , transport Q (pair⁼ (p , refl)) (pr₂ uz)
Σ-transport refl (u , z) = refl

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
-- Andreas, 2015-01-19  Forced constructor arguments should not
-- give rise to unification constraints.

-- Andreas, 2015-02-27  Forcing analysis is too fragile to have
-- such a huge impact.  The problem has to be addressed by
-- putting heterogeneous unification on a solid foundation.

-- Jesper, 2015-12-18   The new unifier now correctly rejects this example.

-- {-# OPTIONS -v tc.lhs.unify:15 #-}
-- {-# OPTIONS -v tc.force:10 #-}

open import Common.Equality
open import Common.Prelude

data HEq (A : Set) (a : A) : (B : Set) (b : B) → Set1 where
  refl : HEq A a A a

-- Abstracting over suc disables forcing [Issue 1427]
module M (s : Nat → Nat) where

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

open M suc

inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → HEq (Fin n) i (Fin m) j → n ≡ m
inj-Fin-≅ {i = zero}  {zero  } refl = refl  -- Expected to fail, as n /= m
inj-Fin-≅ {i = zero}  {suc  j} ()
inj-Fin-≅ {i = suc i} {zero  } ()
inj-Fin-≅ {i = suc i} {suc .i} refl = refl  -- Expected to fail, as n /= m

-- This should not be accepted, as the direct attempt also fails:

-- inj-Fin-≅' : ∀ {n m} {i : Fin n} {j : Fin m} → HEq (Fin n) i (Fin m) j → n ≡ m
-- inj-Fin-≅' refl = refl


text:
open import Relation.Binary.Core

module BBSTree.Properties  {A : Set}
                     (_≤_ : A → A → Set)
                     (trans≤ : Transitive _≤_) where

open import BBSTree _≤_
open import Bound.Total A
open import Bound.Total.Order.Properties _≤_ trans≤
open import List.Order.Simple _≤_
open import List.Order.Simple.Properties _≤_ trans≤
open import List.Sorted _≤_

lemma-bbst-*≤ : {b : Bound}(x : A) → (t : BBSTree b (val x)) → flatten t *≤ x
lemma-bbst-*≤ x (bslf _) = lenx
lemma-bbst-*≤ x (bsnd {x = y} b≤y y≤x l r) = lemma-++-*≤ (lemma-LeB≤ y≤x) (lemma-bbst-*≤ y l) (lemma-bbst-*≤ x r)

lemma-bbst-≤* : {b : Bound}(x : A) → (t : BBSTree (val x) b) → x ≤* flatten t
lemma-bbst-≤* x (bslf _) = genx
lemma-bbst-≤* x (bsnd {x = y} x≤y y≤t l r) = lemma-≤*-++ (lemma-LeB≤ x≤y) (lemma-bbst-≤* x l) (lemma-bbst-≤* y r)

lemma-bbst-sorted : {b t : Bound}(t : BBSTree b t) → Sorted (flatten t)
lemma-bbst-sorted (bslf _) = nils
lemma-bbst-sorted (bsnd {x = x} b≤x x≤t l r) = lemma-sorted++ (lemma-bbst-*≤ x l) (lemma-bbst-≤* x r) (lemma-bbst-sorted l) (lemma-bbst-sorted r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import hott.core
open import hott.core.theorems
open import hott.functions

-- An important theorem in topology is to show the 2-dimensional loop
-- space is abelian. To avoid notational clutter we parameterize the
-- common variables as module parameters.

module hott.topology.loopspace.eckmann-hilton {ℓ : Level}{A : Type ℓ}{a : A}
       where

  -- Let us give a name to the trivial loop at a
  reflₐ : a ≡ a
  reflₐ = refl {ℓ}{A}{a}

  open import hott.topology.loopspace

  -- Eckmann-Hilton : (α β : Ω² (A , a)) → α ∙ β ≡ β ∙ α

  -- This uses the wiskering technique. Consider the following paths
  --    ____ p₀ ___   ____ p₁ ____
  --   /           \ /            \
  --  a₀    α₀     a₁      α₁     a₁
  --   \           / \            /
  --    --- q₀ ----   ---- q₁ ----
  --
  -- The 2-dimensional α₀ and α₀ paths cannot be composed in general
  -- as the end point of α₀ (i.e. q₀) is not the starting point of α₁
  -- (i.e. p₁). However, because the paths are 2-dimenional paths we
  -- can compose them horizontally which we denote by ⋆. We
  -- encapsulate this composition inside a module called wiskering.
  --

  module wiskering {x y : A}{p q : x ≡ y} where
    _∙ᵣ_ : {z : A} (α : p ≡ q)(r : y ≡ z) → p ∙ r ≡ q ∙ r
    α ∙ᵣ refl = p∙refl≡p p ∙ α ∙ p≡p∙refl q

    _∙ₗ_ : {w : A}(r : w ≡ x)(β : p ≡ q) → r ∙ p ≡ r ∙ q
    refl ∙ₗ β = refl∙p≡p p ∙ β ∙ p≡refl∙p q

  open wiskering

--------   Lemmas on wiskering ------------------------------------

  -- The next two lemma specialises the wiskering when one of the
  -- paths is refl.
  α∙ᵣrefl≡α : (α : reflₐ ≡ reflₐ) → α ∙ᵣ reflₐ ≡ α
  α∙ᵣrefl≡α α =
    begin α ∙ᵣ refl ≡ refl ∙ α ∙ refl by  definition
                    ≡ α ∙ refl        by  applying flip _∙_ refl
                                      on refl∙p≡p α
                    ≡ α by p∙refl≡p α
    ∎

  refl∙ₗβ≡β : (β : reflₐ ≡ reflₐ) → reflₐ ∙ₗ β ≡ β
  refl∙ₗβ≡β β =
    begin refl ∙ₗ β ≡ refl ∙ β ∙ refl by definition
                    ≡ β ∙ refl        by applying flip _∙_ refl
                                      on refl∙p≡p β
                    ≡ β by p∙refl≡p β
    ∎

---------- End of lemma on wiskering -----------------------------

  -- With wiskering we can now define two different horizontal
  -- composition of higher order paths.
  module horizontal {a₀ a₁ a₂ : A}{p q : a₀ ≡ a₁}{r s : a₁ ≡ a₂} where

    _⋆_  : (α : p ≡ q)
         → (β : r ≡ s)
         → p ∙ r ≡ q ∙ s -- α₀ ⋆ α₁

    α ⋆ β = (α ∙ᵣ r) ∙ (q ∙ₗ β)

    _⋆′_ : (α : p ≡ q)
         → (β : r ≡ s)
         → p ∙ r ≡ q ∙ s

    α ⋆′ β = (p ∙ₗ β) ∙ (α ∙ᵣ s)

  open horizontal

  -- The shows that either ways of horizontal composition gives the
  -- same higher homotopy. Here we need to induct on all α β an
  ⋆≡⋆′ : {p : a ≡ a}{r : a ≡ a}
         (α : p ≡ reflₐ) (β : reflₐ ≡ r )
        → α ⋆ β ≡ α ⋆′ β
  ⋆≡⋆′ refl refl = refl

  -- The specialisation of the above lemma for elements in the second
  -- loop space.
  ⋆≡⋆′-refl : {α β : Ω² (A , a)} → α ⋆ β ≡ α ⋆′ β
  ⋆≡⋆′-refl {α} {β} = ⋆≡⋆′ α β

  -- When every path is refl horizontal compositions α ⋆ β and α ⋆′ β
  -- reduce to α ∙ β and β ∙ α respectively. The proofs are given at
  -- the end.
  α⋆β≡α∙β : {α β : Ω² (A , a)} → α ⋆ β ≡ α ∙ β
  α⋆′β≡β∙α : {α β : Ω² (A , a)} → α ⋆′ β ≡ β ∙ α

  -- From which we get the Eckmann-Hilton theorem.
  Eckmann-Hilton : (α β : Ω² (A , a)) → α ∙ β ≡ β ∙ α
  Eckmann-Hilton α β = begin α ∙ β ≡ α ⋆  β by α⋆β≡α∙β ⁻¹
                                   ≡ α ⋆′ β by ⋆≡⋆′-refl
                                   ≡ β ∙ α  by α⋆′β≡β∙α

  -- Proofs.
  α⋆β≡α∙β {α}{β} =
    begin α ⋆ β ≡ (α ∙ᵣ refl) ∙ (refl ∙ₗ β)
                     by definition
                ≡ (α ∙ᵣ refl) ∙ β
                     by applying _∙_ (α ∙ᵣ refl) on refl∙ₗβ≡β β
                ≡ α ∙ β
                     by applying flip _∙_ β on α∙ᵣrefl≡α α
    ∎
  α⋆′β≡β∙α {α}{β} =
    begin α ⋆′ β ≡ (refl ∙ₗ β) ∙ (α ∙ᵣ refl)
                         by definition
                 ≡ (refl ∙ₗ β) ∙ α
                         by applying _∙_ (refl ∙ₗ β) on α∙ᵣrefl≡α α
                 ≡ β ∙ α
                         by applying flip _∙_ α on refl∙ₗβ≡β β
    ∎

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
module Issue512 where

open import Common.Equality

data A : Set where
  a b : A

proof : a ≡ a
proof = refl

f : A → A → A
f x y rewrite proof = {!!}

-- gave error below (now complains about LEVELZERO instead of STRING):
-- No binding for builtin thing STRING, use {-# BUILTIN STRING name #-} to bind it to 'name'
-- when checking that the type of the generated with function
-- (w : A) → _≡_ {"Max []"} {A} w w → (x y : A) → A is well-formed

-- Andreas, 2014-05-17: After fixing 1110, there is no error any more,
-- just an unsolved meta.


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

open import Tutorials.Monday-Complete
module Tutorials.Tuesday where

-----------
-- Pi and Sigma types
-----------

module Product where
  -- The open keyword opens a given module in the current namespace
  -- By default all of the public names of the module are opened
  -- The using keyword limits the imported definitions to those explicitly listed
  open Fin
  open Vec using (Vec; []; _∷_)
  open Simple using (¬_)

  variable
    P Q : A → Set

  -- Pi types: dependent function types
  -- For every x of type A, the predicate P x holds
  Π : (A : Set) → (Pred A) → Set
  Π A P = (x : A) → P x

  infix 5 _,_
  -- Sigma types: dependent product types, existential types
  -- For this x of type A, the predicate P x holds
  record Σ (A : Set) (P : Pred A) : Set where
    -- In the type P fst, fst refers to a previously introduced field
    constructor _,_
    field
      fst : A
      snd : P fst

  open Σ public

  -- By depending on a boolean we can use pi types to represent product types
  Π-× : Set → Set → Set
  Π-× A B = Π Bool λ where
    true  → A
    false → B

  -- By depending on a boolean we can use sigma types to represent sum types
  Σ-⊎ : Set → Set → Set
  Σ-⊎ A B = Σ Bool λ where
    true  → A
    false → B

  -- Use pi types to recover function types
  Π-→ : Set → Set → Set
  Π-→ A B = Π A λ where
    _     → B

  -- Use sigma types to recover product types
  Σ-× : Set → Set → Set
  Σ-× A B = Σ A λ where
    _     → B

  infix 5 _×_
  _×_ : Set → Set → Set
  _×_ = Σ-×

  -- 1) If we can transform the witness and
  -- 2) transform the predicate as per the transformation on the witness
  -- ⇒) then we can transform a sigma type
  map : (f : A → B) → (∀ {x} → P x → Q (f x)) → (Σ A P → Σ B Q)
  map f g (x , y) = (f x , g y)

  -- The syntax keyword introduces notation that can include binders
  infix 4 Σ-syntax
  Σ-syntax : (A : Set) → (A → Set) → Set
  Σ-syntax = Σ
  syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

  ¬∘ : Pred A → Pred A
  ¬∘ P = ¬_ ∘ P

  -- These can be proven regardless of A

  ¬∃⇒∀¬ : ¬ (Σ A P) → Π A (¬∘ P)
  ¬∃⇒∀¬ = {!!}

  ∃¬⇒¬∀ : Σ A (¬∘ P) → ¬ Π A P
  ∃¬⇒¬∀ = {!!}

  ∀¬⇒¬∃ : Π A (¬∘ P) → ¬ Σ A P
  ∀¬⇒¬∃ = {!!}

  -- Works in classical, not in constructive mathematics
  postulate ¬∀⇒∃¬ : ¬ Π A P → Σ A (¬∘ P)

  -- Show that ≤ is antisymmetric
  ≤-≡ : n ≤ m → m ≤ n → n ≡ m
  ≤-≡ x y = {!!}

  -- By using n ≤ m instead of Fin m we can mention n in the output
  take : Vec A m → n ≤ m → Vec A n
  take xs lte = {!!}

  Fin-to-≤ : (i : Fin m) → to-ℕ i < m
  Fin-to-≤ i = {!!}

  -- Proof combining sigma types and equality
  ≤-to-Fin : n < m → Fin m
  ≤-to-Fin lt = {!!}

  Fin-≤-inv : (i : Fin m) → ≤-to-Fin (Fin-to-≤ i) ≡ i
  Fin-≤-inv i = {!!}

  ≤-Fin-inv : (lt : Σ[ n ∈ ℕ ] n < m)
            → (to-ℕ (≤-to-Fin (snd lt)) , Fin-to-≤ (≤-to-Fin (snd lt))) ≡ lt
  ≤-Fin-inv lt = {!!}

max_stars_repo_name: poncev/agda-bcam

max_issues_repo_name: poncev/agda-bcam

max_forks_repo_name: poncev/agda-bcam


text:
{-# OPTIONS --no-termination-check #-}

module AC where

import Nat
import Bool
import List
import Fin
import Logic
import Vec
import EqProof

open Nat hiding (_<_) renaming (_==_ to _=Nat=_)
open Bool
open List hiding (module Eq)
open Fin renaming (_==_ to _=Fin=_)
open Logic
open Vec

infix 20 _○_
infix 10 _≡_

ForAll : {A : Set}(n : Nat) -> (Vec n A -> Set) -> Set
ForAll      zero   F = F ε
ForAll {A} (suc n) F = (x : A) -> ForAll _ \xs -> F (x ∷ xs)

apply : {n : Nat}{A : Set}(F : Vec n A -> Set) -> ForAll n F -> (xs : Vec n A) -> F xs
apply {zero}  F t (vec vnil)         = t
apply {suc n} F f (vec (vcons x xs)) = apply _ (f x) xs

lambda : {n : Nat}{A : Set}(F : Vec n A -> Set) -> ((xs : Vec n A) -> F xs) -> ForAll n F
lambda {zero } F f = f ε
lambda {suc n} F f = \x -> lambda _ (\xs -> f (x ∷ xs))

data Expr (n : Nat) : Set where
  zro : Expr n
  var : Fin n -> Expr n
  _○_ : Expr n -> Expr n -> Expr n

data Theorem (n : Nat) : Set where
  _≡_ : Expr n -> Expr n -> Theorem n

theorem : (n : Nat) -> ({m : Nat} -> ForAll {Expr m} n \_ -> Theorem m) -> Theorem n
theorem n thm = apply _ thm (map var (fzeroToN-1 n))

module Provable where

  NF : Nat -> Set
  NF n = List (Fin n)

  infix 12 _⊕_

  _⊕_ : {n : Nat} -> NF n -> NF n -> NF n
  []      ⊕ ys              = ys
  x :: xs ⊕ []              = x :: xs
  x :: xs ⊕ y :: ys = if   x < y
                      then x :: (xs ⊕ y :: ys)
                      else y :: (x :: xs ⊕ ys)

  normalise : {n : Nat} -> Expr n -> NF n
  normalise  zro    = []
  normalise (var n) = n :: []
  normalise (a ○ b) = normalise a ⊕ normalise b

  infix 30 _↓

  _↓ : {n : Nat} -> NF n -> Expr n
  (i :: is) ↓ = var i ○ is ↓
  []        ↓ = zro

  infix 10 _=Expr=_ _=NF=_

  _=NF=_ : {n : Nat} -> NF n -> NF n -> Bool
  _=NF=_ = ListEq._==_
    where
      module ListEq = List.Eq _=Fin=_

  substNF : {n : Nat}{xs ys : NF n}(P : NF n -> Set) -> IsTrue (xs =NF= ys) -> P xs -> P ys
  substNF = List.Subst.subst _=Fin=_ (subst {_})

  _=Expr=_ : {n : Nat} -> Expr n -> Expr n -> Bool
  a =Expr= b = normalise a =NF= normalise b

  provable : {n : Nat} -> Theorem n -> Bool
  provable (a ≡ b) = a =Expr= b

module Semantics
  {A     : Set}
  (_==_  : A -> A -> Set)
  (_*_   : A -> A -> A)
  (one   : A)
  (refl  : {x : A} -> x == x)
  (sym   : {x y : A} -> x == y -> y == x)
  (trans : {x y z : A} -> x == y -> y == z -> x == z)
  (idL   : {x : A} -> (one * x) == x)
  (idR   : {x : A} -> (x * one) == x)
  (comm  : {x y : A} -> (x * y) == (y * x))
  (assoc : {x y z : A} -> (x * (y * z)) == ((x * y) * z))
  (congL : {x y z : A} -> y == z -> (x * y) == (x * z))
  (congR : {x y z : A} -> x == y -> (x * z) == (y * z))
  where

  open Provable

  module EqP = EqProof _==_ refl trans
  open EqP

  expr[_] : {n : Nat} -> Expr n -> Vec n A -> A
  expr[ zro   ] ρ = one
  expr[ var i ] ρ = ρ ! i
  expr[ a ○ b ] ρ = expr[ a ] ρ * expr[ b ] ρ

  eq[_] : {n : Nat} -> Theorem n -> Vec n A -> Set
  eq[ a ≡ b ] ρ = expr[ a ] ρ == expr[ b ] ρ

  data CantProve (A : Set) : Set where
    no-proof : CantProve A

  Prf : {n : Nat} -> Theorem n -> Bool -> Set
  Prf thm true  = ForAll _ \ρ -> eq[ thm ] ρ
  Prf thm false = CantProve (Prf thm true)

  Proof : {n : Nat} -> Theorem n -> Set
  Proof thm = Prf thm (provable thm)

  lem0 : {n : Nat} -> (xs ys : NF n) -> (ρ : Vec n A) ->
         eq[ xs ↓ ○ ys ↓ ≡ (xs ⊕ ys) ↓ ] ρ
  lem0 []        ys        ρ = idL
  lem0 (x :: xs) []        ρ = idR
  lem0 (x :: xs) (y :: ys) ρ = if' x < y then less else more
    where
      lhs     = (var x ○ xs ↓) ○ (var y ○ ys ↓)
      lbranch = x :: (xs ⊕ y :: ys)
      rbranch = y :: (x :: xs ⊕ ys)

      P = \z -> eq[ lhs ≡ (if z then lbranch else rbranch) ↓ ] ρ

      less : IsTrue (x < y) -> _
      less x<y = BoolEq.subst {true}{x < y} P x<y
                  (spine (lem0 xs (y :: ys) ρ))
        where
          spine : forall {x' xs' y' ys' zs} h -> _
          spine {x'}{xs'}{y'}{ys'}{zs} h =
            eqProof> (x' * xs') * (y' * ys')
                 === x' * (xs' * (y' * ys'))  by  sym assoc
                 === x' * zs              by  congL h

      more : IsFalse (x < y) -> _
      more x>=y = BoolEq.subst {false}{x < y} P x>=y
                    (spine (lem0 (x :: xs) ys ρ))
        where
          spine : forall {x' xs' y' ys' zs} h -> _
          spine {x'}{xs'}{y'}{ys'}{zs} h =
            eqProof> (x' * xs') * (y' * ys')
                 === (y' * ys') * (x' * xs')  by  comm
                 === y' * (ys' * (x' * xs'))  by  sym assoc
                 === y' * ((x' * xs') * ys')  by  congL comm
                 === y' * zs              by  congL h

  lem1 : {n : Nat} -> (e : Expr n) -> (ρ : Vec n A) -> eq[ e ≡ normalise e ↓ ] ρ
  lem1  zro    ρ = refl
  lem1 (var i) ρ = sym idR
  lem1 (a ○ b) ρ = trans step1 (trans step2 step3)
    where
      step1 : eq[ a ○ b ≡ normalise a ↓ ○ b ] ρ
      step1 = congR (lem1 a ρ)

      step2 : eq[ normalise a ↓ ○ b ≡ normalise a ↓ ○ normalise b ↓ ] ρ
      step2 = congL (lem1 b ρ)

      step3 : eq[ normalise a ↓ ○ normalise b ↓ ≡ (normalise a ⊕ normalise b) ↓ ] ρ
      step3 = lem0 (normalise a) (normalise b) ρ

  lem2 : {n : Nat} -> (xs ys : NF n) -> (ρ : Vec n A) -> IsTrue (xs =NF= ys) -> eq[ xs ↓ ≡ ys ↓ ] ρ
  lem2 xs ys ρ eq = substNF {_}{xs}{ys} (\z -> eq[ xs ↓ ≡ z ↓ ] ρ) eq refl

  prove : {n : Nat} -> (thm : Theorem n) -> Proof thm
  prove thm = proof (provable thm) thm (\h -> h)
    where
      proof : {n : Nat}(valid : Bool)(thm : Theorem n) -> (IsTrue valid -> IsTrue (provable thm)) -> Prf thm valid
      proof false  _      _       = no-proof
      proof true  (a ≡ b) isValid = lambda eq[ a ≡ b ] \ρ ->
          trans (step-a ρ) (trans (step-ab ρ) (step-b ρ))
        where
          step-a : forall ρ -> eq[ a ≡ normalise a ↓ ] ρ
          step-a ρ = lem1 a ρ

          step-b : forall ρ -> eq[ normalise b ↓ ≡ b ] ρ
          step-b ρ = sym (lem1 b ρ)

          step-ab : forall ρ -> eq[ normalise a ↓ ≡ normalise b ↓ ] ρ
          step-ab ρ = lem2 (normalise a) (normalise b) ρ (isValid tt)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --type-in-type #-}

module _ where

Set' : ∀ i → Set _
Set' i = Set i

postulate
  A : Set
  a : A
  T : Set → Set
  comp : (P : A → Set) (g : (a : A) → P a) → P a
  foo : ∀ i (Q : A → Set' i) → T (comp _ Q)
  -- (no issue if Set' is replaced by Set)

bar : T {!_!} -- Try to give _
bar = foo _ _

-- WAS:
-- A !=< Agda.Primitive.Level of type Set
-- when checking that the expression _ has type Set
-- SHOULD: succeed (with unsolved meta)


text:
-- New NO_POSITIVITY_CHECK pragma for data definitions and mutual
-- blocks

-- Skipping a single data definition in an abstract block.
abstract
  {-# NO_POSITIVITY_CHECK #-}
  data D : Set where
    lam : (D → D) → D


text:
-- Andreas, 2017-03-23, issue #2510
-- Error message in case of --no-pattern-matching

{-# OPTIONS --no-pattern-matching #-}

test : Set
test x = x

-- Expected error:
-- Cannot eliminate type Set with pattern x (did you supply too many arguments?)


text:
record ⊤ : Set where

abstract
  a : ⊤
  a = {!!}


text:
------------------------------------------------------------------------------
-- From ListP as the least fixed-point to ListP using data
------------------------------------------------------------------------------

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

-- We want to represent the polymorphic total lists data type
--
-- data ListP (A : D → Set) : D → Set where
--   lnil  : ListP A []
--   lcons : ∀ {x xs} → A x → ListP A xs → ListP A (x ∷ xs)
--
-- using the representation of ListP as the least fixed-point.

module LFPs.ListP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.Type
open import FOTC.Data.Nat.UnaryNumbers

------------------------------------------------------------------------------
-- ListP is a least fixed-point of a functor

-- The functor.
-- ListPF : (D → Set) → (D → Set) → D → Set
-- ListPF A B xs = xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] A x' ∧ xs ≡ x' ∷ xs' ∧ B xs')

-- ListP is the least fixed-point of ListPF.
postulate
  ListP : (D → Set) → D → Set

  -- ListP is a pre-fixed point of ListPF.
  --
  -- Peter: It corresponds to the introduction rules.
  ListP-in :
    (A : D → Set) →
    ∀ {xs} → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] A x' ∧ xs ≡ x' ∷ xs' ∧ ListP A xs') →
    ListP A xs

  -- ListP is the least pre-fixed point of ListPF.
  --
  -- Peter: It corresponds to the elimination rule of an inductively
  -- defined predicate.
  ListP-ind :
    (A B : D → Set) →
    (∀ {xs} → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] A x' ∧ xs ≡ x' ∷ xs' ∧ B xs') → B xs) →
    ∀ {xs} → ListP A xs → B xs

------------------------------------------------------------------------------
-- The data constructors of ListP.
lnil  : (A : D → Set) → ListP A []
lnil A = ListP-in A (inj₁ refl)

lcons : (A : D → Set) → ∀ {x xs} → A x → ListP A xs → ListP A (x ∷ xs)
lcons A {n} {ns} An LPns = ListP-in A (inj₂ (n , ns , An , refl , LPns))

------------------------------------------------------------------------------
-- The induction principle for ListP.
ListP-ind' : (A B : D → Set) →
             B [] →
             (∀ x {xs} → A x → B xs → B (x ∷ xs)) →
             ∀ {xs} → ListP A xs → B xs
ListP-ind' A B B[] is = ListP-ind A B prf
  where
  prf : ∀ {xs} →
        xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] A x' ∧ xs ≡ x' ∷ xs' ∧ B xs') →
        B xs
  prf (inj₁ xs≡[])                        = subst B (sym xs≡[]) B[]
  prf (inj₂ (x' , xs' , Ax' , h₁ , Bxs')) = subst B (sym h₁) (is x' Ax' Bxs')

------------------------------------------------------------------------------
-- Examples

-- "Heterogeneous" total lists
xs : D
xs = 0' ∷ true ∷ 1' ∷ false ∷ []

List : D → Set
List = ListP (λ d → d ≡ d)

xs-ListP : List xs
xs-ListP =
  lcons A refl (lcons A refl (lcons A refl (lcons A refl (lnil A))))
  where
  A : D → Set
  A d = d ≡ d

-- Total lists of total natural numbers
ys : D
ys = 0' ∷ 1' ∷ 2' ∷ []

ListN : D → Set
ListN = ListP N

ys-ListP : ListN ys
ys-ListP =
  lcons N nzero (lcons N (nsucc nzero) (lcons N (nsucc (nsucc nzero)) (lnil N)))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- 2011-08-22 Andreas (reported and fixed by Dominique Devriese)
{-# OPTIONS --no-universe-polymorphism #-}
module Issue427 where

data ⊥ : Set where

postulate f : {I : ⊥} (B : _) → ⊥

data A : Set where a : {x y : ⊥} → A

test : A → Set
test (a {x = x} {y = y}) with f {_}
test (a {x = x} {y = y}) | _ = A
{- old error message:
  ⊥ should be a function type, but it isn't
  when checking that {y} are valid arguments to a function of type ⊥
-}
-- new error message should be: Unresolved metas


text:
module InstanceArgumentsSections where

postulate  A : Set

module Basic where
  record B : Set where
    field bA : A

  open B {{...}}

  bA' : {{_ : B}} → A
  bA' = bA

module Parameterised (a : A) where
  record C : Set where
    field cA : A

  open C {{...}}

  cA' : {{_ : C}} → A
  cA' = cA

module RecordFromParameterised where
  postulate a : A

  open Parameterised a
  open C {{...}}

  cA'' : {{_ : C}} → A
  cA'' = cA

module RecordFromParameterisedInParameterised (a : A) where

  open Parameterised a
  open C {{...}}

  cA'' : {{_ : C}} → A
  cA'' = cA

module RecordFromParameterised' (a : A) where

  open Parameterised
  open C {{...}}

  cA'' : {{_ : C a}} → A
  cA'' = cA {a}

module AppliedRecord (a : A) where
  open Parameterised

  D : Set
  D = C a

  module D = C
  open D {{...}}

  dA' : {{_ : D}} → A
  dA' = cA {a}


text:
open import Algebra.Bundles using (Group)

module GGT.Group.Facts
  {a b ℓ}
  (G : Group a ℓ)
  where

open import Relation.Unary using (Pred)
open import Relation.Binary
open import GGT.Group.Structures
open import Algebra.Bundles using (Group)
open import Algebra.Properties.Group G
open Group G
open import Relation.Binary.Reasoning.Setoid setoid

⁻¹-anti-homo-- : ∀ (x y : Carrier) → (x - y)⁻¹ ≈ y - x
⁻¹-anti-homo-- x y = begin
                      (x - y)⁻¹ ≡⟨⟩
                      (x ∙ y ⁻¹)⁻¹ ≈⟨ ⁻¹-anti-homo-∙ _ _ ⟩
                      (y ⁻¹) ⁻¹ ∙ x ⁻¹ ≈⟨ ∙-congʳ (⁻¹-involutive _) ⟩
                      y ∙ x ⁻¹ ≡⟨⟩
                      y - x ∎

subgroup⁻¹-closed : {P : Pred Carrier b } →
                        IsSubGroup G P →
                        ∀ x → P x → P (x ⁻¹)
subgroup⁻¹-closed iss x px =
  -- e - x = x ⁻¹ →  P e - x → P x ⁻¹
  r (identityˡ (x ⁻¹)) (∙-⁻¹-closed ε∈ px)
  where open IsSubGroup iss

-- -----
-- (Right) Coset Relation is Equivalenc
cosetRelRefl : {P : Pred Carrier b } →
               (iss : IsSubGroup G P) → Reflexive (IsSubGroup._∼_ iss)
cosetRelRefl iss {x} = r (sym (inverseʳ x)) ε∈ where open IsSubGroup iss
-- (e = x - x) → P e → P x - x
cosetRelSym : {P : Pred Carrier b } →
              (iss : IsSubGroup G P) → Symmetric (IsSubGroup._∼_ iss)

cosetRelSym iss {x} {y} x∼y = r u≈y-x Pu where
-- P e → P (x - y) → P (y - x)
  open IsSubGroup iss
  u≈y-x = begin
            ε - (x - y) ≡⟨⟩
            ε ∙ (x - y)⁻¹ ≈⟨ identityˡ ((x - y)⁻¹) ⟩
            (x - y)⁻¹ ≈⟨ ⁻¹-anti-homo-- _ _ ⟩
            y - x ∎
  Pu = ∙-⁻¹-closed ε∈ x∼y

cosetRelTrans : {P : Pred Carrier b } →
                (iss : IsSubGroup G P) → Transitive (IsSubGroup._∼_ iss)
cosetRelTrans iss {x} {y} {z} x∼y y∼z =
  r x-y-[z-y]≈x-z Pu where
    open IsSubGroup iss
    -- P z - y
    z∼y = cosetRelSym iss y∼z
    x-y-[z-y]≈x-z = begin
                      (x - y) - (z - y) ≡⟨⟩
                      (x - y) ∙ (z - y) ⁻¹ ≈⟨ ∙-congˡ (⁻¹-anti-homo-- z y) ⟩
                      (x - y) ∙ (y - z) ≡⟨⟩
                      (x ∙ y ⁻¹) ∙ (y ∙ z ⁻¹)  ≈⟨ assoc x (y ⁻¹) (y ∙ z ⁻¹) ⟩
                      x ∙ (y ⁻¹ ∙ (y ∙ z ⁻¹))  ≈˘⟨ ∙-congˡ (assoc (y ⁻¹) y (z ⁻¹)) ⟩
                      x ∙ ((y ⁻¹ ∙ y) ∙ z ⁻¹)  ≈⟨ ∙-congˡ (∙-congʳ (inverseˡ _)) ⟩
                      x ∙ (ε ∙ z ⁻¹) ≈⟨ ∙-congˡ (identityˡ _) ⟩
                      x ∙ z ⁻¹ ≡⟨⟩
                      x - z ∎
    Pu = ∙-⁻¹-closed {x - y} {z - y} x∼y z∼y

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt