text:
module Oscar.Data.Term.Injectivity {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Data.Term FunctionName

open import Data.Fin
open import Data.Nat
open import Data.Vec
open import Relation.Binary.PropositionalEquality

Term-i-inj : ∀ {m} {𝑥₁ 𝑥₂ : Fin m} → i 𝑥₁ ≡ i 𝑥₂ → 𝑥₁ ≡ 𝑥₂
Term-i-inj refl = refl

Term-functionName-inj : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → fn₁ ≡ fn₂
Term-functionName-inj refl = refl

Term-functionArity-inj : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → N₁ ≡ N₂
Term-functionArity-inj refl = refl

Term-functionTerms-inj : ∀ {fn₁ fn₂} {n N} {ts₁ : Vec (Term n) N} {ts₂ : Vec (Term n) N} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → ts₁ ≡ ts₂
Term-functionTerms-inj refl = refl

Term-forkLeft-inj : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ fork r₁ ≡ l₂ fork r₂ → l₁ ≡ l₂
Term-forkLeft-inj refl = refl

Term-forkRight-inj : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ fork r₁ ≡ l₂ fork r₂ → r₁ ≡ r₂
Term-forkRight-inj refl = refl


text:
{-# OPTIONS --without-K --exact-split --rewriting --overlapping-instances #-}

open import lib.Basics
open import lib.NConnected
open import lib.NType2
open import lib.types.Truncation
open import lib.types.Sigma
open import lib.Equivalence
open import lib.types.Fin
open import lib.types.Coproduct

open import Graphs.Definition
open import Graphs.Properties

open import Coequalizers.Definition
open import Coequalizers.Misc
open import Groups.Definition
open import Coequalizers.PullbackStability
open import Coequalizers.PreserveEquivalence
open import Coequalizers.EdgeCoproduct
open import Graphs.SpanningTreeFinite
open import Graphs.SubTrees

open import Util.Misc
open import Util.DecEq

module NielsenSchreier {i : ULevel} where

{- We build towards the proof of the finite index Nielsen-Schreier theorem in several steps. -}

{- We will first show that subgroups of free higher groups are free higher groupoids. That is, we will show that
   for any family of types X over ⊤ / A, the total space Σ (⊤ / A) X is equivalent to the coequalizer of
   a graph. Moveover, we can give an explicit description of the graph. -}
module SubgroupsOfFreeHigherGroups (A : Type i) (X : (⊤ / A) → Type i) where
  instance
    {- Whenever we need a pair of maps (A × X fhg-base) ⇉ (X fhg-base) we will use the definition below. This
       applies in this module and wherever it is imported. -}
    higher-subgp-gph : Graph (A × X fhg-base) (X fhg-base)
    higher-subgp-gph = record { π₀ = snd ; π₁ = λ {(a , x) → transport X (quot a) x} }

  to-free-higher-gpd : Σ (⊤ / A) X ≃ (X fhg-base) / (A × X fhg-base)
  to-free-higher-gpd =
      Σ (⊤ / A) X
        ≃⟨ pb-equiv ⁻¹ ⟩ -- coequalizers are stable under pullback
      (Σ ⊤ (X ∘ c[_])) / (Σ A (X ∘ c[_] ∘ π₀))
        ≃⟨ Coeq-emap Σ₁-Unit (ide _) (λ _ → idp) (λ _ → idp) ⟩
      (X fhg-base) / (A × X fhg-base)
        ≃∎
      where
        open PullbackStability A ⊤ X -- contains definition of (Σ ⊤ (X ∘ c[_])) / (Σ A (X ∘ c[_] ∘ π₀))

{- We now show that subgroups of free groups are free groupoids. This is a 1-truncated version of
   the result above. -}
module SubGroupsOfFreeGroups (A : Type i) (X : ∥ ⊤ / A ∥₁ → Type i)
  ⦃ Xset : {z : ∥ ⊤ / A ∥₁} → is-set (X z) ⦄ where -- we now need to assume X is 0-truncated.
  open SubgroupsOfFreeHigherGroups A (X ∘ [_]) public -- also defines instance for (X fhg-base) / (A × X fhg-base)

  to-free-gpd : Σ ∥ ⊤ / A ∥₁ X ≃ ∥ X base / (A × X base) ∥₁
  to-free-gpd =
      Σ ∥ ⊤ / A ∥₁ X
        ≃⟨ Σ-emap-r (Trunc-elim λ z → ide _) ⟩
      Σ ∥ ⊤ / A ∥₁ X'
        ≃⟨ TruncRecType.flattening-Trunc _ ⟩
      ∥ Σ (⊤ / A) (X ∘ [_]) ∥₁
        ≃⟨ Trunc-emap to-free-higher-gpd ⟩
      ∥ X base / (A × X base) ∥₁
        ≃∎
      where
        X'-set : ∥ ⊤ / A ∥₁ → hSet i
        X'-set = Trunc-rec (λ z → ((X [ z ]) , Xset))

        X' = fst ∘ X'-set

        instance
          X-≃-gpd : {z : ∥ ⊤ / A ∥₁} → is-gpd (X z ≃ X' z)
          X-≃-gpd {z} = raise-level 0 (≃-level Xset (snd (X'-set z)))

{- A free groupoid with vertex set a definitionally finite set is merely equivalent
   to a free group. -}
strict-fin-free-gpd-is-free-gp :
  (n : ℕ) → (E : Type i) → (Edec : has-dec-eq E) →
  ⦃ gph : Graph E (Fin (S n)) ⦄ ⦃ conn : gph-is-connected gph ⦄ →
  ∥ Σ (Type i) (λ B → ∥ Coeq gph ∥₁ ≃ FreeGroup B) ∥
strict-fin-free-gpd-is-free-gp n E Edec =
  Trunc-fmap from-spanning-tree-fin (spanning-tree E Edec n)
  where
    from-spanning-tree-fin : SpanningTree E (Fin (S n)) (Fin n) (Fin (S n)) →
      Σ (Type i) (λ B → ∥ Fin (S n) / E ∥₁ ≃ FreeGroup B)
    from-spanning-tree-fin st =
      ¬E' , Trunc-emap eq
      where
        open SpanningTree st
        open ExtendSpanningTree E (Fin (S n)) (Fin n) (Fin (S n)) st
        open CoeqCoprodEquiv (Fin (S n)) (Fin n) ¬E'

        eq : Fin (S n) / E ≃ ⊤ / ¬E'
        eq =
          Fin (S n) / E
            ≃⟨ spantree-equiv ⟩
          Fin (S n) / ((Fin n) ⊔ ¬E')
            ≃⟨ edge-coproduct-expand ⟩
          (Fin (S n) / (Fin n)) / ¬E'
            ≃⟨ Coeq-emap (contr-equiv-Unit ⟨⟩) (ide _) (λ _ → idp) (λ _ → idp) ⟩
          ⊤ / ¬E'
            ≃∎

{- We generalise the above so that the vertex set only needs to be equivalent to a
   definitionally finite set. -}
fin-free-gpd-is-free-gp : (n : ℕ) → (E : Type i) → (Edec : has-dec-eq E) →
  (V : Type i) → (Vfin : V ≃ Fin (S n)) →
  ⦃ gph : Graph E V ⦄ ⦃ conn : gph-is-connected gph ⦄ →
  ∥ Σ (Type i) (λ B → ∥ Coeq gph ∥₁ ≃ FreeGroup B) ∥
fin-free-gpd-is-free-gp n E Edec V Vfin =
  Trunc-fmap (λ {(B , e) → B , (e ∘e Trunc-emap coeq-equiv)}) (strict-fin-free-gpd-is-free-gp n E Edec)
  where
    instance
      gph' : Graph E (Fin (S n))
      gph' = record { π₀ = (–> Vfin) ∘ π₀ ; π₁ = (–> Vfin) ∘ π₁ }

    coeq-equiv : (V / E) ≃ (Fin (S n) / E)
    coeq-equiv = Coeq-emap Vfin (ide E) (λ _ → idp) λ _ → idp

    instance
      conn' : gph-is-connected gph'
      conn' = equiv-preserves-level (Trunc-emap coeq-equiv )

{- We can now prove the finite index version of the Nielsen-Schreier theorem. -}
nielsen-schreier-finite-index :
  (A : Type i) (Adec : has-dec-eq A) -- we are given a type A with decidable equality
  (X : (FreeGroup A) → Type i) -- together with a covering space over the free group on A, that is a family of types X ...
  ⦃ conn : is-connected 0 (Σ (FreeGroup A) X) ⦄ -- such that the total space is connected
  (n : ℕ) (Xfin : X (base) ≃ Fin (S n)) → -- here we do the finite index case
  ∥ Σ (Type i) (λ B → Σ (FreeGroup A) X ≃ FreeGroup B) ∥ -- then the total space is a free group

nielsen-schreier-finite-index A Adec X n Xfin =
  Trunc-fmap (λ {(B , e) → B , e ∘e to-free-gpd}) -- we compose the two equivalences from earlier
             (fin-free-gpd-is-free-gp n (A × X base) (×-has-dec-eq Adec (equiv-preserves-dec-eq Xfin Fin-has-dec-eq)) (X base) Xfin)
               -- earlier we showed that free groupoids with finite vertex set are merely equivalent to free groups
  where
    open SubGroupsOfFreeGroups A X -- contains our proof that the subgroup is a free groupoid

    instance -- we use that X is a set and the free groupoid is connected
      Xset : {z : (FreeGroup A)} → is-set (X z)
      Xset {z} = Trunc-elim {P = λ z → is-set (X z)}
        (Coeq-elim (λ z → is-set (X [ z ]))
          (λ {unit → equiv-preserves-level (Xfin ⁻¹) ⦃ Fin-is-set ⦄}) λ _ → prop-has-all-paths-↓) z

      conn2 : is-connected 0 (X base / (A × X base))
      conn2 = equiv-preserves-level e
        where
          e : ∥ Σ (FreeGroup A) X ∥₀ ≃ ∥ X base / (A × X base) ∥₀
          e =
            ∥ Σ (FreeGroup A) X ∥₀
              ≃⟨ Trunc-emap (to-free-gpd ) ⟩
            ∥ ∥ X base / (A × X base) ∥₁ ∥₀
              ≃⟨ Trunc-fuse _ 0 1 ⟩
            ∥ X base / (A × X base) ∥₀
              ≃∎

ext: agda

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
{-# OPTIONS --without-K #-}
module TypeEquivalences where

open import Data.Empty
open import Data.Unit
open import Data.Unit.Core
open import Data.Nat renaming (_⊔_ to _⊔ℕ_)
open import Data.Sum renaming (map to _⊎→_)
open import Data.Product renaming (map to _×→_)
open import Function renaming (_∘_ to _○_)

-- explicit using to show how little of HoTT is needed
open import SimpleHoTT using (refl; ap; ap2)
open import Equivalences

------------------------------------------------------------------------------
-- Type Equivalences

-- for each type combinator, define two functions that are inverses, and
-- establish an equivalence.  These are all in the 'semantic space' with
-- respect to Pi combinators.

-- swap₊

swap₊ : {A B : Set} → A ⊎ B → B ⊎ A
swap₊ (inj₁ a) = inj₂ a
swap₊ (inj₂ b) = inj₁ b

swapswap₊ : {A B : Set} → swap₊ ○ swap₊ {A} {B} ∼ id
swapswap₊ (inj₁ a) = refl (inj₁ a)
swapswap₊ (inj₂ b) = refl (inj₂ b)

swap₊equiv : {A B : Set} → (A ⊎ B) ≃ (B ⊎ A)
swap₊equiv = (swap₊ , equiv₁ (mkqinv swap₊ swapswap₊ swapswap₊))

-- unite₊ and uniti₊

unite₊ : {A : Set} → ⊥ ⊎ A → A
unite₊ (inj₁ ())
unite₊ (inj₂ y) = y

uniti₊ : {A : Set} → A → ⊥ ⊎ A
uniti₊ a = inj₂ a

uniti₊∘unite₊ : {A : Set} → uniti₊ ○ unite₊ ∼ id {A = ⊥ ⊎ A}
uniti₊∘unite₊ (inj₁ ())
uniti₊∘unite₊ (inj₂ y) = refl (inj₂ y)

-- this is so easy, Agda can figure it out by itself (see below)
unite₊∙uniti₊ : {A : Set} → unite₊ ○ uniti₊ ∼ id {A = A}
unite₊∙uniti₊ = refl

unite₊equiv : {A : Set} → (⊥ ⊎ A) ≃ A
unite₊equiv = (unite₊ , mkisequiv uniti₊ refl uniti₊ uniti₊∘unite₊)

uniti₊equiv : {A : Set} → A ≃ (⊥ ⊎ A)
uniti₊equiv = uniti₊ , mkisequiv unite₊ uniti₊∘unite₊ unite₊ unite₊∙uniti₊

-- unite⋆ and uniti⋆

unite⋆ : {A : Set} → ⊤ × A → A
unite⋆ (tt , x) = x

uniti⋆ : {A : Set} → A → ⊤ × A
uniti⋆ x = tt , x

uniti⋆∘unite⋆ : {A : Set} → uniti⋆ ○ unite⋆ ∼ id {A = ⊤ × A}
uniti⋆∘unite⋆ (tt , x) = refl (tt , x)

unite⋆equiv : {A : Set} → (⊤ × A) ≃ A
unite⋆equiv = unite⋆ , mkisequiv uniti⋆ refl uniti⋆ uniti⋆∘unite⋆

uniti⋆equiv : {A : Set} → A ≃ (⊤ × A)
uniti⋆equiv = uniti⋆ , mkisequiv unite⋆ uniti⋆∘unite⋆ unite⋆ refl

-- swap⋆

swap⋆ : {A B : Set} → A × B → B × A
swap⋆ (a , b) = (b , a)

swapswap⋆ : {A B : Set} → swap⋆ ○ swap⋆ ∼ id {A = A × B}
swapswap⋆ (a , b) = refl (a , b)

swap⋆equiv : {A B : Set} → (A × B) ≃ (B × A)
swap⋆equiv = swap⋆ , mkisequiv swap⋆ swapswap⋆ swap⋆ swapswap⋆

-- assocl₊ and assocr₊

assocl₊ : {A B C : Set} → (A ⊎ (B ⊎ C)) → ((A ⊎ B) ⊎ C)
assocl₊ (inj₁ a) = inj₁ (inj₁ a)
assocl₊ (inj₂ (inj₁ b)) = inj₁ (inj₂ b)
assocl₊ (inj₂ (inj₂ c)) = inj₂ c

assocr₊ : {A B C : Set} → ((A ⊎ B) ⊎ C) → (A ⊎ (B ⊎ C))
assocr₊ (inj₁ (inj₁ a)) = inj₁ a
assocr₊ (inj₁ (inj₂ b)) = inj₂ (inj₁ b)
assocr₊ (inj₂ c) = inj₂ (inj₂ c)

assocl₊∘assocr₊ : {A B C : Set} → assocl₊ ○ assocr₊ ∼ id {A = ((A ⊎ B) ⊎ C)}
assocl₊∘assocr₊ (inj₁ (inj₁ a)) = refl (inj₁ (inj₁ a))
assocl₊∘assocr₊ (inj₁ (inj₂ b)) = refl (inj₁ (inj₂ b))
assocl₊∘assocr₊ (inj₂ c) = refl (inj₂ c)

assocr₊∘assocl₊ : {A B C : Set} → assocr₊ ○ assocl₊ ∼ id {A = (A ⊎ (B ⊎ C))}
assocr₊∘assocl₊ (inj₁ a) = refl (inj₁ a)
assocr₊∘assocl₊ (inj₂ (inj₁ b)) = refl (inj₂ (inj₁ b))
assocr₊∘assocl₊ (inj₂ (inj₂ c)) = refl (inj₂ (inj₂ c))

assocl₊equiv : {A B C : Set} → (A ⊎ (B ⊎ C)) ≃ ((A ⊎ B) ⊎ C)
assocl₊equiv =
  assocl₊ , mkisequiv assocr₊ assocl₊∘assocr₊ assocr₊ assocr₊∘assocl₊

assocr₊equiv : {A B C : Set} → ((A ⊎ B) ⊎ C) ≃ (A ⊎ (B ⊎ C))
assocr₊equiv =
  assocr₊ , mkisequiv assocl₊ assocr₊∘assocl₊ assocl₊ assocl₊∘assocr₊

-- assocl⋆ and assocr⋆

assocl⋆ : {A B C : Set} → (A × (B × C)) → ((A × B) × C)
assocl⋆ (a , (b , c)) = ((a , b) , c)

assocr⋆ : {A B C : Set} → ((A × B) × C) → (A × (B × C))
assocr⋆ ((a , b) , c) = (a , (b , c))

assocl⋆∘assocr⋆ : {A B C : Set} → assocl⋆ ○ assocr⋆ ∼ id {A = ((A × B) × C)}
assocl⋆∘assocr⋆ x = refl x

assocr⋆∘assocl⋆ : {A B C : Set} → assocr⋆ ○ assocl⋆ ∼ id {A = (A × (B × C))}
assocr⋆∘assocl⋆ x = refl x

assocl⋆equiv : {A B C : Set} → (A × (B × C)) ≃ ((A × B) × C)
assocl⋆equiv =
  assocl⋆ , mkisequiv assocr⋆ assocl⋆∘assocr⋆ assocr⋆ assocr⋆∘assocl⋆

assocr⋆equiv : {A B C : Set} → ((A × B) × C) ≃ (A × (B × C))
assocr⋆equiv =
  assocr⋆ , mkisequiv assocl⋆ assocr⋆∘assocl⋆ assocl⋆ assocl⋆∘assocr⋆

-- distz and factorz

distz : { A : Set} → (⊥ × A) → ⊥
distz (() , _)

factorz : {A : Set} → ⊥ → (⊥ × A)
factorz ()

distz∘factorz : {A : Set} → distz ○ factorz {A} ∼ id
distz∘factorz ()

factorz∘distz : {A : Set} → factorz {A} ○ distz ∼ id
factorz∘distz (() , proj₂)

distzequiv : {A : Set} → (⊥ × A) ≃ ⊥
distzequiv {A} =
  distz , mkisequiv factorz (distz∘factorz {A}) factorz factorz∘distz

factorzequiv : {A : Set} → ⊥ ≃ (⊥ × A)
factorzequiv {A} =
  factorz , mkisequiv distz factorz∘distz distz (distz∘factorz {A})

-- dist and factor

dist : {A B C : Set} → ((A ⊎ B) × C) → (A × C) ⊎ (B × C)
dist (inj₁ x , c) = inj₁ (x , c)
dist (inj₂ y , c) = inj₂ (y , c)

factor : {A B C : Set} → (A × C) ⊎ (B × C) → ((A ⊎ B) × C)
factor (inj₁ (a , c)) = inj₁ a , c
factor (inj₂ (b , c)) = inj₂ b , c

dist∘factor : {A B C : Set} → dist {A} {B} {C} ○ factor ∼ id
dist∘factor (inj₁ x) = refl (inj₁ x)
dist∘factor (inj₂ y) = refl (inj₂ y)

factor∘dist : {A B C : Set} → factor {A} {B} {C} ○ dist ∼ id
factor∘dist (inj₁ x , c) = refl (inj₁ x , c)
factor∘dist (inj₂ y , c) = refl (inj₂ y , c)

distequiv : {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C))
distequiv = dist , mkisequiv factor dist∘factor factor factor∘dist

factorequiv : {A B C : Set} →  ((A × C) ⊎ (B × C)) ≃ ((A ⊎ B) × C)
factorequiv = factor , (mkisequiv dist factor∘dist dist dist∘factor)

-- ⊕

_⊎∼_ : {A B C D : Set} {f : A → C} {finv : C → A} {g : B → D} {ginv : D → B} →
  (α : f ○ finv ∼ id) → (β : g ○ ginv ∼ id) →
  (f ⊎→ g) ○ (finv ⊎→ ginv) ∼ id {A = C ⊎ D}
_⊎∼_ α β (inj₁ x) = ap inj₁ (α x)
_⊎∼_ α β (inj₂ y) = ap inj₂ (β y)

path⊎ : {A B C D : Set} → A ≃ C → B ≃ D → (A ⊎ B) ≃ (C ⊎ D)
path⊎ (fp , eqp) (fq , eqq) =
  Data.Sum.map fp fq ,
  mkisequiv (P.g ⊎→ Q.g) (P.α ⊎∼ Q.α) (P.h ⊎→ Q.h) (P.β ⊎∼ Q.β)
  where module P = isequiv eqp
        module Q = isequiv eqq

-- ⊗

_×∼_ : {A B C D : Set} {f : A → C} {finv : C → A} {g : B → D} {ginv : D → B} →
  (α : f ○ finv ∼ id) → (β : g ○ ginv ∼ id) →
  (f ×→ g) ○ (finv ×→ ginv) ∼ id {A = C × D}
_×∼_ α β (x , y) = ap2 _,_ (α x) (β y)

path× : {A B C D : Set} → A ≃ C → B ≃ D → (A × B) ≃ (C × D)
path× {A} {B} {C} {D} (fp , eqp) (fq , eqq) =
  Data.Product.map fp fq ,
  mkisequiv
    (P.g ×→ Q.g)
    (_×∼_ {A} {B} {C} {D} {fp} {P.g} {fq} {Q.g} P.α Q.α)
    (P.h ×→ Q.h)
    (_×∼_ {C} {D} {A} {B} {P.h} {fp} {Q.h} {fq} P.β Q.β)
  where module P = isequiv eqp
        module Q = isequiv eqq

idequiv : {A : Set} → A ≃ A
idequiv = id≃

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module HyperPositive where

open import Prelude

infixr 4 _↬_
{-# NO_POSITIVITY_CHECK #-}
record _↬_ (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  inductive; constructor hyp
  field invoke : ((A ↬ B) → A) → B
open _↬_

open import Data.List using (List; _∷_; []; foldr)

module _ {a b} {A : Type a} {B : Type b} where
  XT = List (A × B) ↬ (A → List (A × B)) → List (A × B)
  YT = List (A × B) ↬ (A → List (A × B))

  yfld : List B → YT
  yfld = foldr f n
    where
    f : B → YT → YT
    f y yk .invoke xk x = (x , y) ∷ xk yk

    n : YT
    n .invoke _ _ = []

  xfld : List A → XT
  xfld = foldr f n
    where
    f : A → XT → XT
    f x xk yk = yk .invoke xk x

    n : XT
    n _ = []

  zip : List A → List B → List (A × B)
  zip xs ys = xfld xs (yfld ys)

open import Data.List using (_⋯_)
open import Data.List.Syntax

_ : zip (1 ⋯ 5) (11 ⋯ 15) ≡ [ 5 ][ (1 , 11) , (2 , 12) , (3 , 13) , (4 , 14) , (5 , 15) ]
_ = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Relation.Binary.Indexed

module Relation.Binary.Indexed.EqReasoning {𝒾} {I : Set 𝒾} {𝒸 ℓ} (S : Setoid I 𝒸 ℓ) where

open Setoid S
import Relation.Binary.Indexed.PreorderReasoning as PreR
open import Relation.Binary.Indexed.Extra using (Setoid⇒Preorder)
open PreR (Setoid⇒Preorder S) public
       renaming ( _∼⟨_⟩_  to _≈⟨_⟩_
                ; _≈⟨_⟩_  to _≡⟨_⟩_
                ; _≈⟨⟩_  to _≡⟨⟩_
                )

max_stars_repo_name: banacorn/categories

max_issues_repo_name: banacorn/categories

max_forks_repo_name: banacorn/categories


text:
module Cats.Category.Discrete {li} (I : Set li) where

open import Data.Unit using (⊤)
open import Level

open import Cats.Category.Base
open import Cats.Functor using (Functor)

Obj : Set li
Obj = I

data _⇒_ : Obj → Obj → Set where
  id : ∀ {A} → A ⇒ A

_∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C
id ∘ id = id

Discrete : Category li zero zero
Discrete = record
    { Obj = Obj
    ; _⇒_ = _⇒_
    ; _≈_ = λ _ _ → ⊤
    ; id = id
    ; _∘_ = _∘_
    ; equiv = _
    ; ∘-resp = _
    ; id-r = _
    ; id-l = _
    ; assoc = _
    }

functor : ∀ {lo la l≈} {C : Category lo la l≈}
  → (I → Category.Obj C)
  → Functor Discrete C
functor {C = C} f = record
    { fobj = f
    ; fmap = λ { id → C.id }
    ; fmap-resp = λ { {_} {_} {id} {id} _ → C.≈.refl }
    ; fmap-id = C.≈.refl
    ; fmap-∘ = λ { {f = id} {id} → C.id-l }
    }
  where
    module C = Category C

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


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

module Cubical.Categories.Sets where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Categories.Category

module _ ℓ where
  SET : Precategory (ℓ-suc ℓ) ℓ
  SET .ob = Σ (Type ℓ) isSet
  SET .hom (A , _) (B , _) = A → B
  SET .idn _  = λ x → x
  SET .seq f g = λ x → g (f x)
  SET .seq-λ f = refl
  SET .seq-ρ f = refl
  SET .seq-α f g h = refl

module _ {ℓ} where
  isSetExpIdeal : {A B : Type ℓ} → isSet B → isSet (A → B)
  isSetExpIdeal B/set = isOfHLevelPi 2 λ _ → B/set

  isSetLift : {A : Type ℓ} → isSet A → isSet (Lift {ℓ} {ℓ-suc ℓ} A)
  isSetLift = isOfHLevelLift 2

  instance
    SET-category : isCategory (SET ℓ)
    SET-category .homIsSet {_} {B , B/set} = isSetExpIdeal B/set

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
-- Building some simple tactics using the reflected type checking monad.
module _ where

open import Common.Reflection
open import Common.Prelude hiding (_>>=_)
open import Common.Equality
open import Agda.Builtin.Sigma

-- Some helpers --

quotegoal : (Type → Tactic) → Tactic
quotegoal tac hole =
  inferType hole >>= λ goal →
  reduce goal >>= λ goal →
  tac goal hole

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

replicateTC : {A : Set} → Nat → TC A → TC (List A)
replicateTC zero m = returnTC []
replicateTC (suc n) m = m >>= λ x → replicateTC n m >>= λ xs → returnTC (x ∷ xs)

mapTC! : ∀ {A : Set} → (A → TC ⊤) → List A → TC ⊤
mapTC! f [] = returnTC _
mapTC! f (x ∷ xs) = f x >>= λ _ → mapTC! f xs

mapTC!r : ∀ {A} → (A → TC ⊤) → List A → TC ⊤
mapTC!r f [] = returnTC _
mapTC!r f (x ∷ xs) = mapTC! f xs >>= λ _ → f x

visibleArity : QName → TC Nat
visibleArity q = getType q >>= λ t → returnTC (typeArity t)
  where
    typeArity : Type → Nat
    typeArity (pi (arg (argInfo visible _) _) (abs _ b)) = suc (typeArity b)
    typeArity (pi _ (abs _ b)) = typeArity b
    typeArity _ = 0

newMeta! : TC Term
newMeta! = newMeta unknown

absurdLam : Term
absurdLam = extLam (absurdClause
                      (("()" , arg (argInfo visible relevant) unknown) ∷ [])
                      (arg (argInfo visible relevant) absurd ∷ [])
                   ∷ []) []

-- Simple assumption tactic --

assumption-tac : Nat → Nat → Tactic
assumption-tac x 0 _ = typeError (strErr "No assumption matched" ∷ [])
assumption-tac x (suc n) hole =
  catchTC (unify hole (var x []))
          (assumption-tac (suc x) n hole)

macro
  assumption : Tactic
  assumption hole = getContext >>= λ Γ → assumption-tac 0 (length Γ) hole

test-assumption : ∀ {A B : Set} → A → B → A
test-assumption x y = assumption

test-assumption₂ : ∀ {A B : Set} → A → B → _
test-assumption₂ x y = assumption  -- will pick y

-- Solving a goal using only constructors --

tryConstructors : Nat → List QName → Tactic

constructors-tac : Nat → Type → Tactic
constructors-tac zero _ _ = typeError (strErr "Search depth exhausted" ∷ [])
constructors-tac (suc n) (def d vs) hole =
  getDefinition d >>= λ def →
  case def of λ
  { (dataDef _ cs) → tryConstructors n cs hole
  ; _              → returnTC _ }
constructors-tac _ (pi a b) hole = give absurdLam hole
constructors-tac _ _ hole = returnTC _

tryConstructors n []       hole = typeError (strErr "No matching constructor term" ∷ [])
tryConstructors n (c ∷ cs) hole =
  visibleArity c >>= λ ar →
  catchTC (replicateTC ar newMeta! >>= λ vs →
           unify hole (con c (map (arg (argInfo visible relevant)) vs)) >>= λ _ →
           mapTC!r (quotegoal (constructors-tac n)) vs)
          (tryConstructors n cs hole)

macro
  constructors : Tactic
  constructors = quotegoal (constructors-tac 10)

data Any {A : Set} (P : A → Set) : List A → Set where
  zero : ∀ {x xs} → P x      → Any P (x ∷ xs)
  suc  : ∀ {x xs} → Any P xs → Any P (x ∷ xs)

infix 1 _∈_
_∈_ : ∀ {A : Set} → A → List A → Set
x ∈ xs = Any (x ≡_) xs

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

test₁ : 3 ∈ 1 ∷ 2 ∷ 3 ∷ []
test₁ = constructors

test₂ : Dec (2 + 3 ≡ 5)
test₂ = constructors

test₃ : Dec (2 + 2 ≡ 5)
test₃ = constructors

data Singleton (n : Nat) : Set where
  it : (m : Nat) → m ≡ n → Singleton n

test₄ : Singleton 5
test₄ = constructors -- this works because we solve goals right to left (picking refl before m)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- Proofs of the map-iterate property and iterate fusion
------------------------------------------------------------------------

module MapIterate where

open import Codata.Musical.Notation
open import Codata.Musical.Stream as Stream
  using (Stream; map; zipWith; iterate; _≈_)
open Stream.Stream; open Stream._≈_
open import Data.Nat
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

private
  module SS {A : Set} = Setoid (Stream.setoid A)

-- The map-iterate property:

map-iterate :  {A : Set} (f : A → A) (x : A) →
               map f (iterate f x) ≈ iterate f (f x)
map-iterate f x = refl ∷ ♯ map-iterate f (f x)

-- An equality proof language.

infixr 5 _∷_
infix  4 _≈P_ _≈W_
infix  3 _∎
infixr 2 _≈⟨_⟩_

data _≈P_ {A : Set} : Stream A → Stream A → Set where
  _∷_          : ∀ (x : A) {xs ys}
                 (xs≈ys : ∞ (♭ xs ≈P ♭ ys)) → x ∷ xs ≈P x ∷ ys
  _≈⟨_⟩_       : ∀ (xs : Stream A) {ys zs}
                 (xs≈ys : xs ≈P ys) (ys≈zs : ys ≈P zs) → xs ≈P zs
  _∎           : (xs : Stream A) → xs ≈P xs
  zipWith-cong : ∀ (_∙_ : A → A → A) {xs₁ ys₁ xs₂ ys₂}
                 (xs₁≈ys₁ : xs₁ ≈P ys₁) (xs₂≈ys₂ : xs₂ ≈P ys₂) →
                 zipWith _∙_ xs₁ xs₂ ≈P zipWith _∙_ ys₁ ys₂

-- Completeness.

completeP : {A : Set} {xs ys : Stream A} → xs ≈ ys → xs ≈P ys
completeP (refl ∷ xs≈ys) = _ ∷ ♯ completeP (♭ xs≈ys)

-- Weak head normal forms.

data _≈W_ {A : Set} : Stream A → Stream A → Set where
  _∷_ : ∀ x {xs ys} (xs≈ys : ♭ xs ≈P ♭ ys) → x ∷ xs ≈W x ∷ ys

transW : {A : Set} {xs ys zs : Stream A} →
         xs ≈W ys → ys ≈W zs → xs ≈W zs
transW (x ∷ xs≈ys) (.x ∷ ys≈zs) = x ∷ (_ ≈⟨ xs≈ys ⟩ ys≈zs)

reflW : {A : Set} (xs : Stream A) → xs ≈W xs
reflW (x ∷ xs) = x ∷ (♭ xs ∎)

zipWith-congW : ∀ {A : Set} (_∙_ : A → A → A) {xs₁ ys₁ xs₂ ys₂} →
                xs₁ ≈W ys₁ → xs₂ ≈W ys₂ →
                zipWith _∙_ xs₁ xs₂ ≈W zipWith _∙_ ys₁ ys₂
zipWith-congW _∙_ (x₁ ∷ xs₁≈ys₁) (x₂ ∷ xs₂≈ys₂) =
  (x₁ ∙ x₂) ∷ zipWith-cong _∙_ xs₁≈ys₁ xs₂≈ys₂

whnf : {A : Set} {xs ys : Stream A} → xs ≈P ys → xs ≈W ys
whnf (x ∷ xs≈ys)           = x ∷ ♭ xs≈ys
whnf (xs ≈⟨ xs≈ys ⟩ ys≈zs) = transW (whnf xs≈ys) (whnf ys≈zs)
whnf (xs ∎)                = reflW xs
whnf (zipWith-cong _∙_ xs₁≈ys₁ xs₂≈ys₂) =
  zipWith-congW _∙_ (whnf xs₁≈ys₁) (whnf xs₂≈ys₂)

-- Soundness.

mutual

  soundW : {A : Set} {xs ys : Stream A} → xs ≈W ys → xs ≈ ys
  soundW (x ∷ xs≈ys) = refl ∷ ♯ soundP xs≈ys

  soundP : {A : Set} {xs ys : Stream A} → xs ≈P ys → xs ≈ ys
  soundP xs≈ys = soundW (whnf xs≈ys)

-- A small hack which enables me to write "by definition" below.

definition : {A : Set} {xs : Stream A} → xs ≈P xs
definition {xs = xs} = xs ∎

by : ∀ {A : Set} {x : A} {xs ys : ∞ (Stream A)} →
     ♭ xs ≈P ♭ ys → x ∷ xs ≈P x ∷ ys
by {x = x} ♭xs≈♭ys = x ∷ ♯ ♭xs≈♭ys

-- Iterate preserves equality.

iterate-cong : {A : Set} (f : A → A) {x y : A} →
               x ≡ y → iterate f x ≈P iterate f y
iterate-cong f {x} refl = iterate f x ∎

-- Iterate fusion.

iterate-fusion : {A B : Set} (h : A → B) (f₁ : A → A) (f₂ : B → B) →
                 ((x : A) → h (f₁ x) ≡ f₂ (h x)) →
                 (x : A) → map h (iterate f₁ x) ≈P iterate f₂ (h x)
iterate-fusion h f₁ f₂ hyp x =
  map h (iterate f₁ x)               ≈⟨ by definition ⟩
  h x ∷ ♯ map h (iterate f₁ (f₁ x))  ≈⟨ h x ∷ ♯ iterate-fusion h f₁ f₂ hyp (f₁ x) ⟩
  h x ∷ ♯ iterate f₂ (h (f₁ x))      ≈⟨ h x ∷ ♯ iterate-cong f₂ (hyp x) ⟩
  h x ∷ ♯ iterate f₂ (f₂ (h x))      ≈⟨ by definition ⟩
  iterate f₂ (h x)                   ∎

-- The equation given for fib in StreamProg has a unique solution.

fib-rhs : Stream ℕ → Stream ℕ
fib-rhs ns = 0 ∷ ♯ zipWith _+_ ns (1 ∷ ♯ ns)

fib-unique :
  ∀ ms ns → ms ≈ fib-rhs ms → ns ≈ fib-rhs ns → ms ≈P ns
fib-unique ms ns ms≈ ns≈ =
  ms         ≈⟨ completeP ms≈ ⟩
  fib-rhs ms ≈⟨ 0 ∷ ♯ zipWith-cong _+_ (fib-unique ms ns ms≈ ns≈)
                                       (1 ∷ ♯ fib-unique ms ns ms≈ ns≈) ⟩
  fib-rhs ns ≈⟨ completeP (SS.sym ns≈) ⟩
  ns         ∎

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


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

data ⊥ : Set where

bad : ⊥
bad = bad

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module plfa.working.Induction where

  import Relation.Binary.PropositionalEquality as Eq
  open Eq using (_≡_; refl; cong; sym)
  open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
  open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

  +-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
  +-assoc zero n p =
    begin
      (zero + n) + p
    ≡⟨⟩
      n + p
    ≡⟨⟩
      zero + (n + p)
    ∎
  +-assoc (suc m) n p =
    begin
      (suc m + n) + p
    ≡⟨⟩
      suc (m + n) + p
    ≡⟨⟩
      suc ((m + n) + p)
    ≡⟨ cong suc (+-assoc m n p) ⟩
      suc (m + (n + p))
    ≡⟨⟩
      suc m + (n + p)
    ∎

  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-identity zero =
    begin
      zero + zero
    ≡⟨⟩
      zero
    ∎
  +-identity (suc m) =
    begin
      (suc m) + zero
    ≡⟨⟩
      suc (m + zero)
    ≡⟨ cong suc (+-identity m) ⟩
      suc m
    ∎

  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
  +-suc zero n =
    begin
      zero + suc n
    ≡⟨⟩
      suc n
    ≡⟨⟩
      suc (zero + n)
    ∎
  +-suc (suc m) n =
    begin
      suc m + suc n
    ≡⟨⟩
      (suc m) + suc n
    ≡⟨ cong suc (+-suc m n) ⟩
      suc (suc m + n)
    ∎

  +-comm : ∀ (m n : ℕ) → m + n ≡ n + m
  +-comm m zero =
    begin
      m + zero
    ≡⟨ +-identity m ⟩
      m
    ≡⟨⟩
      zero + m
    ∎
  +-comm m (suc n) =
    begin
      m + suc n
    ≡⟨ +-suc m n ⟩
      suc (m + n)
    ≡⟨ cong suc (+-comm m n) ⟩
      suc (n + m)
    ≡⟨⟩
      suc n + m
    ∎


text:
{-# OPTIONS --sized-types --guardedness #-}

-- Note: This module is not meant to be imported.
module Js where

import Data
import Data.Boolean
import FFI.IO as FFI

main : FFI.IO Data.Unit
main = FFI.printStrLn("Okay")

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 _ where

record R : Set₁ where
  field x : Set

g : Set₁

module M (r : R) where
  open R r
  f = x

g = R


text:
module Examples.Syntax where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.String using (_++_)
open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; done; _∙_)
open import Luau.Syntax.ToString using (exprToString; blockToString)

f = var "f"
x = var "x"

ex1 : exprToString(f $ x) ≡
  "f(x)"
ex1 = refl

ex2 : blockToString(return nil ∙ done) ≡
  "return nil"
ex2 = refl

ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ done end ∙ return f ∙ done) ≡
  "local function f(x)\n" ++
  "  return x\n" ++
  "end\n" ++
  "return f"
ex3 = refl

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


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

open import HoTT
open import cw.CW
open import cw.FinCW
open import cw.FinBoundary
open import cohomology.Theory

module cw.cohomology.cochainequiv.HigherCoboundaryCommSquare (OT : OrdinaryTheory lzero)
  {n} (⊙fin-skel : ⊙FinSkeleton (S (S n))) where

open OrdinaryTheory OT
open import cw.cohomology.WedgeOfCells OT
open import cw.cohomology.reconstructed.HigherCoboundary OT ⊙⦉ ⊙fin-skel ⦊
open import cw.cohomology.cochainequiv.DualizedHigherBoundary OT ⊙fin-skel
open import cw.cohomology.cochainequiv.HigherCoboundary OT ⊙fin-skel

private
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel
  ac = ⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero

  ⊙fin-skel₋₁ = ⊙fcw-init ⊙fin-skel
  fin-skel₋₁ = ⊙FinSkeleton.skel ⊙fin-skel₋₁
  ac₋₁ = ⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel₋₁ lzero

abstract
  rephrase-dualized-higher-boundary-comm-sqr :
    CommSquareEquiv
      (λ g <I → Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁)))
      (_∘ᴳ fboundary-last fin-skel)
      (FreeAbGroup-extend (C2-abgroup 0))
      (FreeAbGroup-extend (C2-abgroup 0))
  rephrase-dualized-higher-boundary-comm-sqr =
    comm-sqr (λ g →
      equiv-adj'
        (GroupIso.f-equiv (FreeAbGroup-extend-iso (C2-abgroup 0)))
        (λ= λ <I → ! (rephrase-dualized-higher-boundary-in-degree g <I))) ,
    FreeAbGroup-extend-is-equiv (C2-abgroup 0) ,
    FreeAbGroup-extend-is-equiv (C2-abgroup 0)

  rephrase-cw-co∂-last-comm-sqr :
    CommSquareEquiv
      (λ g <I → Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁)))
      (GroupHom.f cw-co∂-last)
      (GroupIso.g (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel₋₁ ⦊ ac₋₁))
      (GroupIso.g (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel ⦊ ac))
  rephrase-cw-co∂-last-comm-sqr =
    comm-sqr (λ g →
      equiv-adj'
        (GroupIso.g-equiv (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel ⦊ ac))
        (λ= λ <I → ! (rephrase-cw-co∂-last-in-degree g <I))) ,
    (GroupIso.g-is-equiv (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel₋₁ ⦊ ac₋₁)) ,
    (GroupIso.g-is-equiv (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel ⦊ ac))

  higher-coboundary-comm-sqr :
    CommSquareEquiv
      (GroupHom.f cw-co∂-last)
      (_∘ᴳ fboundary-last fin-skel)
      (FreeAbGroup-extend (C2-abgroup 0) ∘ GroupIso.f (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel₋₁ ⦊ ac₋₁))
      (FreeAbGroup-extend (C2-abgroup 0) ∘ GroupIso.f (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel ⦊ ac))
  higher-coboundary-comm-sqr =
    CommSquareEquiv-∘v
      rephrase-dualized-higher-boundary-comm-sqr
      (CommSquareEquiv-inverse-v rephrase-cw-co∂-last-comm-sqr)

  higher-coboundary-comm-sqrᴳ :
    CommSquareEquivᴳ
      cw-co∂-last
      (pre∘ᴳ-hom (C2-abgroup 0) (fboundary-last fin-skel))
      (FreeAbGroup-extend-hom (C2-abgroup 0) ∘ᴳ GroupIso.f-hom (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel₋₁ ⦊ ac₋₁))
      (FreeAbGroup-extend-hom (C2-abgroup 0) ∘ᴳ GroupIso.f-hom (CXₙ/Xₙ₋₁-diag-β ⊙⦉ ⊙fin-skel ⦊ ac))
  higher-coboundary-comm-sqrᴳ =
    comm-sqrᴳ (fst higher-coboundary-comm-sqr □$_) , snd higher-coboundary-comm-sqr

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module CoinductiveAfterEvaluation where

open import Common.Coinduction

data Functor : Set where
  Id : Functor

_·_ : Functor → Set → Set
Id · A = A

data ν (F : Functor) : Set where
  inn : ∞ (F · ν F) → ν F

-- Evaluation is required to see that Id · ν Id is a coinductive type.

foo : ∀ F → F · ν F
foo Id = inn (♯ foo Id)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Dave.Algebra.Naturals.Definition where
  open import Dave.Equality public
  open import Dave.Structures.Monoid public

  data ℕ : Set where
    zero : ℕ
    suc : ℕ → ℕ

  one = suc zero
  two = suc one
  three = suc two
  four = suc three
  five = suc four
  six = suc five
  seven = suc six
  eight = suc seven
  nine = suc eight

  {-# BUILTIN NATURAL  ℕ #-}

  ℕ-suc-≡ : ∀ {m n : ℕ} → m ≡ n → suc m ≡ suc n
  ℕ-suc-≡ refl = refl


text:
module x07-747Negation-hc where

open import Relation.Binary.PropositionalEquality using (_≡_; cong; refl; subst; sym) -- added last
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; proj₁; proj₂)

------------------------------------------------------------------------------
-- NEGATION : defined as implying false
-- import Relation.Nullary using (¬_)
¬_ : Set → Set
¬ A = A → ⊥
infix 3 ¬_

-- if both ¬ A and A hold, then ⊥ holds
¬-elim : ∀ {A : Set}
  → ¬ A
  → A
    ---
  → ⊥
¬-elim ¬a a = ¬a a

-- double negation introduction (cannot be eliminated in intuitionistic logic)
¬¬-intro : ∀ {A : Set}
  → A
    -----
  → ¬ ¬ A
-- ¬¬-intro a     ¬a = ¬a a -- agda with auto split/fill to this
¬¬-intro    a = λ ¬a → ¬a a -- easier to understand with ¬ def using anon λ

-- triple negation elimination
¬¬¬-elim : ∀ {A : Set}
  → ¬ ¬ ¬ A
    -------
  → ¬ A
-- ¬¬¬-elim ¬¬¬a     a = ¬-elim ¬¬¬a (¬¬-intro a)
¬¬¬-elim    ¬¬¬a = λ a → ¬-elim ¬¬¬a (¬¬-intro a)

-- import Relation.Nullary.Negation using (contraposition)
-- one direction of the contrapositive
-- the other direction cannot be proved in intuitionistic logic
contraposition : ∀ {A B : Set}
  → (A → B)
    -----------
  → (¬ B → ¬ A)
-- contraposition a→b     ¬b     a = ¬b (a→b a)
contraposition    a→b = λ ¬b → λ a → ¬b (a→b a)

-- not-equal-to
_≢_ : ∀ {A : Set} → A → A → Set
x ≢ y  =  ¬ (x ≡ y)

_ : 1 ≢ 2
_ = λ ()

-- a first-order Peano axioms
peano : ∀ {m : ℕ} → zero ≢ suc m
peano ()

open import x05-842Isomorphism-hc using (extensionality)

-- two proofs of ⊥ → ⊥
-- they look different but are the same (assuming extensionality)
id : ⊥ → ⊥
id x = x

id′ : ⊥ → ⊥
id′ ()

id≡id′ : id ≡ id′
id≡id′ = extensionality (λ())

-- assuming extensionality, any two proofs of a negation are the same
assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
assimilation ¬x ¬x′ = extensionality λ x → ⊥-elim (¬x x)

-- BEGIN: Strict inequality (copied from 747Relations).
infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n
-- END: Strict inequality (copied from 747Relations).

-- NotFourLTThree
¬4<3 : ¬ (4 < 3)
¬4<3 (s<s (s<s (s<s ())))

-- < is irreflexive (never reflexive)
¬n<n : ∀ (n : ℕ) → ¬ (n < n)
-- ¬n<n (suc n)       (s<s n<n) = ¬n<n n n<n
¬n<n    (suc n) = λ { (s<s n<n) → ¬n<n n n<n }

-- 747/PLFA exercise: LTTrich (3 points)
-- Prove that strict inequality satisfies trichotomy : exactly one of the three possibilities holds.
data Trichotomy (m n : ℕ) : Set where
  is-< : m < n → ¬ m ≡ n → ¬ n < m → Trichotomy m n
  is-≡ : m ≡ n → ¬ m < n → ¬ n < m → Trichotomy m n
  is-> : n < m → ¬ m ≡ n → ¬ m < n → Trichotomy m n

open import x03-842Relations-hc-2 using (suc-injective; m≡n→sucm≡sucn)

inv-s<s : ∀ {m n : ℕ}
  → suc m < suc n
    -------------
  →     m <     n
inv-s<s (s<s m<n) = m<n

<-trichotomy : ∀ (m n : ℕ) → Trichotomy m n
<-trichotomy zero     zero   = is-≡ refl (λ ()) (λ ())
<-trichotomy zero    (suc n) = is-< z<s  (λ ()) (λ ())
<-trichotomy (suc m)  zero   = is-> z<s  (λ ()) (λ ())
<-trichotomy (suc m) (suc n) with <-trichotomy m n
... | is-< m<n ¬m≡n ¬n<m = is-< (s<s m<n)
                                (λ sucm≡sucn → ¬m≡n (suc-injective sucm≡sucn))
                                (λ sucn<sucm → ¬n<m (inv-s<s       sucn<sucm))
... | is-≡ m≡n ¬m<n ¬n<m = is-≡ (m≡n→sucm≡sucn m n m≡n)
                                (λ sucm<sucn → ¬m<n (inv-s<s       sucm<sucn))
                                (λ sucn<sucm → ¬n<m (inv-s<s       sucn<sucm))
... | is-> n<m ¬m≡n ¬m<n = is-> (s<s n<m)
                                (λ sucm≡sucn → ¬m≡n (suc-injective sucm≡sucn))
                                (λ sucm<sucn → ¬m<n (inv-s<s       sucm<sucn))

-- PLFA exercise: one of DeMorgan's Laws as isomorphism TODO
-- ⊎-dual-× : ∀ {A B : Set} → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
-- Expand negation as implies-false, then look in 747Relations
-- for a law of which this is a special case.

-- What about ¬ (A × B) ≃ (¬ A) ⊎ (¬ B)?
-- Answer: RHS implies LHS but converse cannot be proved in intuitionistic logic.

-- Intuitionistic vs classical logic.

-- The law of the excluded middle (LEM, or just em) cannot be proved in intuitionistic logic.
-- LEM can be added to intuitionistic logic to get classical logic.

-- postulate
--  em : ∀ {A : Set} → A ⊎ ¬ A

-- 'em-irrefutable' theorem of intuitionistic logic demonstrates
-- that 'em' does not give a contradiction?
em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
em-irrefutable = λ z → z (inj₂ (λ x → z (inj₁ x)))

-- PLFA exercise: classical equivalences TODO
-- Here are four other classical theorems that can be added and are consisstent in IT.
-- Prove each is logically equivalent to all the others.
-- It is NOT necessary to prove twenty implications, since implication is transitive.
-- There is a lot of choice as to how to proceed.

-- Excluded Middle
em = ∀ {A : Set} → A ⊎ ¬ A

-- Double Negation Elimination
dne = ∀ {A : Set} → ¬ ¬ A → A

-- Peirce’s Law
peirce = ∀ {A B : Set} → ((A → B) → A) → A

-- Implication as disjunction
iad = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B

-- De Morgan:
dem = ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B

-- End of classical five exercise.

-- Definition: a formula is stable if double negation holds for it.

Stable : Set → Set
Stable A = ¬ ¬ A → A

-- PLFA exercise: every negated formula is stable.
-- This is triple negation elimination.

-- PLFA exercise: the conjunction of two stable formulas is stable.
-- This is the version of DeMorgan's Law that is a special case, above.

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