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

-- Verbatim dual of Categories.Category.Construction.Kleisli
module Categories.Category.Construction.CoKleisli where

open import Level

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

private
  variable
    o ℓ e : Level

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

  -- useful lemma
  trihom : {X Y Z W : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} {h : Z ⇒ W} → F₁ (h ∘ g ∘ f) ≈ F₁ h ∘ F₁ g ∘ F₁ f
  trihom {X} {Y} {Z} {W} {f} {g} {h} = begin
   F₁ (h ∘ g ∘ f)     ≈⟨ homomorphism ⟩
   F₁ h ∘ F₁ (g ∘ f)  ≈⟨ refl⟩∘⟨ homomorphism ⟩
   F₁ h ∘ F₁ g ∘ F₁ f ∎
  -- shorthands to make the proofs nicer
  F≈ = F-resp-≈

  assoc′ : {A B C D : Obj} {f : F₀ A ⇒ B} {g : F₀ B ⇒ C} {h : F₀ C ⇒ D} → (h ∘ F₁ g ∘ δ.η B) ∘ F₁ f ∘ δ.η A ≈ h ∘ F₁ (g ∘ F₁ f ∘ δ.η A) ∘ δ.η A
  assoc′ {A} {B} {C} {D} {f} {g} {h} =
      begin
        (h ∘ F₁ g ∘ δ.η B) ∘ (F₁ f ∘ δ.η A)             ≈⟨ assoc²' ⟩
        h ∘ (F₁ g ∘ (δ.η B ∘ (F₁ f ∘ δ.η A)))           ≈⟨ ((refl⟩∘⟨ (refl⟩∘⟨ sym assoc))) ⟩
        h ∘ (F₁ g ∘ ((δ.η B ∘ F₁ f) ∘ δ.η A))           ≈⟨ ((refl⟩∘⟨ (refl⟩∘⟨ pushˡ (δ.commute f)))) ⟩
        h ∘ (F₁ g ∘ (F₁ (F₁ f) ∘ (δ.η (F₀ A) ∘ δ.η A))) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨  pushʳ (Comonad.assoc M)) ⟩
        h ∘ (F₁ g ∘ ((F₁ (F₁ f) ∘ F₁ (δ.η A)) ∘ δ.η A)) ≈⟨ pull-center (sym trihom) ⟩
        h ∘ (F₁ (g ∘ (F₁ f ∘ δ.η A)) ∘ δ.η A)
      ∎

  identityˡ′ : ∀ {A B : Obj} {f : F₀ A ⇒ B} → ε.η B ∘ F₁ f ∘ δ.η A ≈ f
  identityˡ′ {A} {B} {f} =
    begin
      ε.η B ∘ F₁ f ∘ δ.η A     ≈⟨ pullˡ (ε.commute f) ⟩
      (f ∘ ε.η (F₀ A)) ∘ δ.η A ≈⟨ trans (pullʳ (Comonad.identityʳ M)) identityʳ ⟩
      f
    ∎

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

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


text:
import Data.Integer as Integer
open Integer using (ℤ)

module NumberTheory.ModularArithmetic (m : ℤ) where

open import Algebra.Structures

open Integer hiding (+_; _-_) -- using (_+_; _*_; -_; +0)
open import Data.Integer.GCD
open import Data.Integer.Properties hiding (*-1-isMonoid; *-1-isCommutativeMonoid; +-*-isCommutativeRing)
open import Data.Integer.Tactic.RingSolver
open import Data.Product

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

_≈_ : Rel ℤ _
x ≈ y = ∃ λ k → k * m + x ≡ y

refl : Reflexive _≈_
refl {x} = +0 , (begin
  +0 * m + x
    ≡⟨ ≡.cong (_+ x) (*-zeroˡ m) ⟩
  +0 + x
    ≡⟨ +-identityˡ x ⟩
  x
    ∎)
  where
    open ≡.≡-Reasoning

sym : Symmetric _≈_
sym {x} {y} (k , p) = (- k) , (begin
  - k * m + y
    ≡˘⟨ ≡.cong₂ _+_ (neg-distribˡ-* k m) (neg-involutive y) ⟩
  - (k * m) + - - y
    ≡˘⟨ neg-distrib-+ (k * m) (- y) ⟩
  - (k * m + - y)
    ≡⟨ ≡.cong -_ (begin
      k * m + - y
        ≡˘⟨ +-identityʳ _ ⟩
      k * m + - y + +0
        ≡˘⟨ ≡.cong (k * m + - y +_) (+-inverseʳ x) ⟩
      k * m + - y + (x + - x)
        ≡˘⟨ +-assoc (k * m + - y) x (- x) ⟩
      k * m + - y + x + - x
        ≡⟨ ≡.cong (_+ - x) (begin
          k  * m + - y + x
            ≡⟨ +-assoc (k * m) (- y) x ⟩
          k * m + (- y + x)
            ≡⟨ ≡.cong (k * m +_) (+-comm (- y) x) ⟩
          k * m + (x + - y)
            ≡˘⟨ +-assoc (k * m) x (- y) ⟩
          k * m + x + - y
            ≡⟨ ≡.cong (_+ - y) p ⟩
          y + - y
            ≡⟨ +-inverseʳ y ⟩
          +0
            ∎) ⟩
      +0 + - x
        ≡⟨ +-identityˡ (- x) ⟩
      - x
        ∎) ⟩
  - - x
    ≡⟨ neg-involutive x ⟩
  x
    ∎)
  where
    open ≡.≡-Reasoning

trans : Transitive _≈_
trans {x} {y} {z} (j , p) (k , q) = k + j , (begin
  (k + j) * m + x
    ≡⟨ ≡.cong (_+ x) (*-distribʳ-+ (m) k j) ⟩
  k * m + j * m + x
    ≡⟨ +-assoc (k * m) (j * m) x ⟩
  k * m + (j * m + x)
    ≡⟨ ≡.cong (_+_ (k * m)) p ⟩
  k * m + y
    ≡⟨ q ⟩
  z
    ∎)
  where
    open ≡.≡-Reasoning

≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
  { refl = refl
  ; sym = sym
  ; trans = trans
  }

open IsEquivalence ≈-isEquivalence public using (reflexive)

setoid : Setoid _ _
setoid = record { isEquivalence = ≈-isEquivalence }

open import Algebra.Definitions _≈_

+-cong : Congruent₂ _+_
+-cong {x} {y} {u} {v} (j , p) (k , q) = j + k , (begin
  (j + k) * m + (x + u)
    ≡⟨ ≡.cong (_+ (x + u)) (*-distribʳ-+ m j k) ⟩
  j * m + k * m + (x + u)
    ≡˘⟨ +-assoc (j * m + k * m) x u ⟩
  j * m + k * m + x + u
    ≡⟨ ≡.cong (_+ u) (begin
    j * m + k * m + x
      ≡⟨ +-assoc (j * m) (k * m) x ⟩
    j * m + (k * m + x)
      ≡⟨ ≡.cong (j * m +_) (+-comm (k * m) x) ⟩
    j * m + (x + k * m)
      ≡˘⟨ +-assoc (j * m) x (k * m) ⟩
    j * m + x + k * m
      ∎) ⟩
  j * m + x + k * m + u
    ≡⟨ +-assoc (j * m + x) (k * m) u ⟩
  j * m + x + (k * m + u)
    ≡⟨ ≡.cong₂ _+_ p q ⟩
  y + v
    ∎)
  where
    open ≡.≡-Reasoning

*-cong : Congruent₂ _*_
*-cong {x} {y} {u} {v} (j , p) (k , q) = j * m * k + j * u + x * k , (begin
  (j * m * k + j * u + x * k) * m + x * u
    ≡⟨ ≡.cong (_+ x * u) (begin
    (j * m * k + j * u + x * k) * m
      ≡⟨ *-distribʳ-+ m (j * m * k + j * u) (x * k) ⟩
    (j * m * k + j * u) * m + (x * k) * m
      ≡⟨ ≡.cong₂ _+_ (*-distribʳ-+ m (j * m * k) (j * u)) (*-assoc x k m) ⟩
    j * m * k * m + j * u * m + x * (k * m)
      ≡⟨ ≡.cong (_+ x * (k * m)) (begin
      j * m * k * m + (j * u) * m
        ≡⟨ ≡.cong (_+ j * u * m) (*-assoc (j * m) k m) ⟩
      j * m * (k * m) + j * u * m
        ≡⟨ ≡.cong (j * m * (k * m) +_) (begin
        j * u * m
          ≡⟨ *-assoc j u m ⟩
        j * (u * m)
          ≡⟨ ≡.cong (j *_) (*-comm u m) ⟩
        j * (m * u)
          ≡˘⟨ *-assoc j m u ⟩
        j * m * u
          ∎) ⟩
      (j * m) * (k * m) + (j * m) * u
        ∎) ⟩
    j * m * (k * m) + j * m * u + x * (k * m)
      ∎) ⟩
  (j * m) * (k * m) + (j * m) * u + x * (k * m) + x * u
    ≡⟨ +-assoc ((j * m) * (k * m) + (j * m) * u) (x * (k * m)) (x * u) ⟩
  (j * m) * (k * m) + (j * m) * u + (x * (k * m) + x * u)
    ≡˘⟨ ≡.cong₂ _+_ (*-distribˡ-+ (j * m) (k * m) u) (*-distribˡ-+ x (k * m) u) ⟩
  (j * m) * (k * m + u) + x * (k * m + u)
    ≡˘⟨ *-distribʳ-+ (k * m + u) (j * m) x ⟩
  (j * m + x) * (k * m + u)
    ≡⟨ ≡.cong₂ _*_ p q ⟩
  y * v
    ∎)
  where
    open ≡.≡-Reasoning

neg-cong : Congruent₁ -_
neg-cong {x} {y} (k , p) = - k , (begin
  - k * m + - x
    ≡˘⟨ ≡.cong (_+ - x) (neg-distribˡ-* k m) ⟩
  - (k * m) + - x
    ≡˘⟨ neg-distrib-+ (k * m) x ⟩
  - (k * m + x)
    ≡⟨ ≡.cong -_ p ⟩
  - y
    ∎)
  where
    open ≡.≡-Reasoning

+-0-isAbelianGroup : IsAbelianGroup _≈_ _+_ +0 -_
+-0-isAbelianGroup = record
  { isGroup = record
    { isMonoid = record
      { isSemigroup = record
        { isMagma = record
          { isEquivalence = ≈-isEquivalence
          ; ∙-cong = +-cong
          }
        ; assoc = λ x y z → reflexive (+-assoc x y z)
        }
      ; identity = (λ x → reflexive (+-identityˡ x)) , λ x → reflexive (+-identityʳ x)
      }
    ; inverse = (λ x → reflexive (+-inverseˡ x)) , λ x → reflexive(+-inverseʳ x)
    ; ⁻¹-cong = neg-cong
    }
  ; comm = λ x y → reflexive (+-comm x y)
  }

*-1-isCommutativeMonoid : IsCommutativeMonoid _≈_ _*_ (Integer.+ 1)
*-1-isCommutativeMonoid = record
  { isMonoid = record
    { isSemigroup = record
      { isMagma = record
        { isEquivalence = ≈-isEquivalence
        ; ∙-cong = *-cong
        }
      ; assoc = λ x y z → reflexive (*-assoc x y z)
      }
    ; identity = (λ x → reflexive (*-identityˡ x)) , λ x → reflexive (*-identityʳ x )
    }
  ; comm = λ x y → reflexive (*-comm x y)
  }

open IsCommutativeMonoid *-1-isCommutativeMonoid using () renaming (isMonoid to *-1-isMonoid)

+-*-isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ +0 (Integer.+ 1)
+-*-isCommutativeRing = record
  { isRing = record
    { +-isAbelianGroup = +-0-isAbelianGroup
    ; *-isMonoid = *-1-isMonoid
    ; distrib = (λ x y z → reflexive (*-distribˡ-+ x y z)) , λ x y z → reflexive (*-distribʳ-+ x y z)
    ; zero = (λ x → reflexive (*-zeroˡ x)) , λ x → reflexive (*-zeroʳ x)
    }
  ; *-comm = λ x y → reflexive (*-comm x y)
  }

ext: agda

max_stars_repo_name: Taneb/antlion

max_issues_repo_name: Taneb/antlion

max_forks_repo_name: Taneb/antlion


text:
{-# OPTIONS -v tc.lhs.unify:80 #-}
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

postulate
  A : Set
  a : A

record Foo : Set where
  constructor foo
  field anA : A

test : (f : A → A) (x : Foo) → foo (f a) ≡ x → A
test f .(foo (f a)) refl = a

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Highlighting where

Set-one : Set₂
Set-one = Set₁

record R (A : Set) : Set-one where
  constructor con

  field X : Set

  F : Set → Set → Set
  F A B = B

  field P : F A X → Set

  -- highlighting of non-terminating definition
  Q : F A X → Set
  Q = Q

postulate P : _

open import Highlighting.M

data D (A : Set) : Set-one where
  d : let X = D in X A

postulate _+_ _×_ : Set → Set → Set

infixl 4 _×_ _+_
  -- Issue #2140: the operators should be highlighted also in the
  -- fixity declaration.

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
------------------------------------------------------------------------
-- Integers, defined using a quotient type
------------------------------------------------------------------------

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

import Equality.Path as P

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

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

open import Prelude as P hiding (suc; _*_; _^_) renaming (_+_ to _⊕_)

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Equivalence-relation equality-with-J
open import Erased.Cubical eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import Group equality-with-J as G using (Group; Abelian; _≃ᴳ_)
open import Group.Cyclic eq as C using (Generated-by; Cyclic)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq using (∣_∣)
import Integer equality-with-J as Data
import Nat equality-with-J as Nat
open import Quotient eq as Q hiding (elim; rec)
open import Univalence-axiom equality-with-J

private
  variable
    m m₁ m₂ n n₁ n₂ : ℕ
    a               : Level
    A               : Type a
    i j p q         : A

------------------------------------------------------------------------
-- The relation used to define the integers.

-- Two pairs of natural numbers are related if they have the same
-- difference.

Same-difference : ℕ × ℕ → ℕ × ℕ → Type
Same-difference (m₁ , n₁) (m₂ , n₂) = m₁ ⊕ n₂ ≡ n₁ ⊕ m₂

-- The relation is pointwise propositional.

Same-difference-propositional :
  Is-proposition (Same-difference p q)
Same-difference-propositional = ℕ-set

-- The relation is an equivalence relation.

Same-difference-is-equivalence-relation :
  Is-equivalence-relation Same-difference
Same-difference-is-equivalence-relation = record
  { reflexive  = λ { {m , n} →
                     m ⊕ n  ≡⟨ Nat.+-comm m ⟩∎
                     n ⊕ m  ∎
                   }
  ; symmetric  = λ { {m₁ , n₁} {m₂ , n₂} hyp →
                     m₂ ⊕ n₁  ≡⟨ Nat.+-comm m₂ ⟩
                     n₁ ⊕ m₂  ≡⟨ sym hyp ⟩
                     m₁ ⊕ n₂  ≡⟨ Nat.+-comm m₁ ⟩∎
                     n₂ ⊕ m₁  ∎
                   }
  ; transitive = λ { {m₁ , n₁} {m₂ , n₂} {m₃ , n₃} hyp₁ hyp₂ →
                     Nat.+-cancellativeʳ (
                       m₁ ⊕ n₃ ⊕ m₂    ≡⟨ sym $ Nat.+-assoc m₁ ⟩
                       m₁ ⊕ (n₃ ⊕ m₂)  ≡⟨ cong (m₁ ⊕_) $ Nat.+-comm n₃ ⟩
                       m₁ ⊕ (m₂ ⊕ n₃)  ≡⟨ cong (m₁ ⊕_) hyp₂ ⟩
                       m₁ ⊕ (n₂ ⊕ m₃)  ≡⟨ Nat.+-assoc m₁ ⟩
                       m₁ ⊕ n₂ ⊕ m₃    ≡⟨ cong (_⊕ m₃) hyp₁ ⟩
                       n₁ ⊕ m₂ ⊕ m₃    ≡⟨ sym $ Nat.+-assoc n₁ ⟩
                       n₁ ⊕ (m₂ ⊕ m₃)  ≡⟨ cong (n₁ ⊕_) $ Nat.+-comm m₂ ⟩
                       n₁ ⊕ (m₃ ⊕ m₂)  ≡⟨ Nat.+-assoc n₁ ⟩∎
                       n₁ ⊕ m₃ ⊕ m₂    ∎)
                   }
  }

-- It is decidable whether the relation holds.

Same-difference-decidable : ∀ p → Dec (Same-difference p q)
Same-difference-decidable _ = _ Nat.≟ _

------------------------------------------------------------------------
-- Integers

-- Integers.

ℤ : Type
ℤ = (ℕ × ℕ) / Same-difference

-- The integers form a set.

ℤ-set : Is-set ℤ
ℤ-set = /-is-set

-- Turns natural numbers into the corresponding integers.

infix 8 +_

+_ : ℕ → ℤ
+ n = [ (n , 0) ]

-- Turns natural numbers into the corresponding negative integers.

-[_] : ℕ → ℤ
-[ n ] = [ (0 , n) ]

------------------------------------------------------------------------
-- A lemma

-- Increasing both sides of a pair by one does not affect the value of
-- the corresponding integer.

[]≡[suc,suc] : _≡_ {A = ℤ} [ (m , n) ] [ (P.suc m , P.suc n) ]
[]≡[suc,suc] {m = m} {n = n} = []-respects-relation
  (m ⊕ P.suc n  ≡⟨ sym $ Nat.suc+≡+suc m ⟩
   P.suc m ⊕ n  ≡⟨ Nat.+-comm (P.suc m) ⟩∎
   n ⊕ P.suc m  ∎)

------------------------------------------------------------------------
-- A one-to-one correspondence between two definitions of integers

-- There is a bijection between this variant of integers and the one
-- in Integer.

ℤ↔ℤ : ℤ ↔ Data.ℤ
ℤ↔ℤ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to-lemma₁ : m₁ ⊕ P.suc n₂ ≡ m₂ →
              (Data.+ m₁) ≡ Data.+ m₂ +-[1+ n₂ ]
  to-lemma₁ {m₁ = m₁} {n₂ = n₂} {m₂ = zero} hyp =
    ⊥-elim $
    Nat.0≢+
      (zero             ≡⟨ sym hyp ⟩
       m₁ ⊕ P.suc n₂    ≡⟨ sym $ Nat.suc+≡+suc m₁ ⟩∎
       P.suc (m₁ ⊕ n₂)  ∎)
  to-lemma₁ {m₁ = m₁} {n₂ = zero} {m₂ = P.suc m₂} hyp =
    cong (Data.+_) $
    Nat.cancel-suc
      (P.suc m₁  ≡⟨ Nat.+-comm 1 ⟩
       m₁ ⊕ 1    ≡⟨ hyp ⟩∎
       P.suc m₂  ∎)
  to-lemma₁ {m₁ = m₁} {n₂ = P.suc n₂} {m₂ = P.suc m₂} hyp =
    to-lemma₁ $
    Nat.cancel-suc
      (P.suc (m₁ ⊕ P.suc n₂)  ≡⟨ Nat.suc+≡+suc m₁ ⟩
       m₁ ⊕ P.suc (P.suc n₂)  ≡⟨ hyp ⟩∎
       P.suc m₂               ∎)

  to-lemma₂ : m₁ ⊕ zero ≡ P.suc n₁ ⊕ m₂ →
              Data.+ m₁ +-[1+ n₁ ] ≡ Data.+ m₂
  to-lemma₂ {m₁ = zero} hyp =
    ⊥-elim $ Nat.0≢+ hyp
  to-lemma₂ {m₁ = P.suc m₁} {n₁ = zero} {m₂ = m₂} hyp =
    cong (Data.+_) $
    Nat.cancel-suc
      (P.suc m₁      ≡⟨ sym Nat.+-right-identity ⟩
       P.suc m₁ ⊕ 0  ≡⟨ hyp ⟩∎
       P.suc m₂      ∎)
  to-lemma₂ {m₁ = P.suc m₁} {n₁ = P.suc n₁} hyp =
    to-lemma₂ (Nat.cancel-suc hyp)

  to-lemma₃ :
    ∀ m₁ n₁ m₂ n₂ →
    m₁ ⊕ P.suc n₂ ≡ P.suc n₁ ⊕ m₂ →
    Data.+ m₁ +-[1+ n₁ ] ≡ Data.+ m₂ +-[1+ n₂ ]
  to-lemma₃ (P.suc m₁) (P.suc n₁) m₂ n₂ hyp =
    to-lemma₃ m₁ n₁ m₂ n₂ (Nat.cancel-suc hyp)
  to-lemma₃ m₁ n₁ (P.suc m₂) (P.suc n₂) hyp =
    to-lemma₃ m₁ n₁ m₂ n₂ $
    Nat.cancel-suc
      (P.suc (m₁ ⊕ P.suc n₂)  ≡⟨ Nat.suc+≡+suc m₁ ⟩
       m₁ ⊕ P.suc (P.suc n₂)  ≡⟨ hyp ⟩
       P.suc n₁ ⊕ P.suc m₂    ≡⟨ cong P.suc $ sym $ Nat.suc+≡+suc n₁ ⟩∎
       P.suc (P.suc n₁ ⊕ m₂)  ∎)
  to-lemma₃ zero n₁ zero n₂ hyp =
    cong Data.-[1+_] $
    Nat.cancel-suc
      (P.suc n₁      ≡⟨ sym Nat.+-right-identity ⟩
       P.suc n₁ ⊕ 0  ≡⟨ sym hyp ⟩∎
       P.suc n₂      ∎)
  to-lemma₃ (P.suc m₁) zero (P.suc m₂) zero hyp =
    cong (Data.+_) $
    Nat.cancel-suc $
      (P.suc m₁  ≡⟨ Nat.+-comm 1 ⟩
       m₁ ⊕ 1    ≡⟨ Nat.cancel-suc hyp ⟩∎
       P.suc m₂  ∎)
  to-lemma₃ (P.suc m₁) zero zero n₂ hyp =
    ⊥-elim $ Nat.0≢+
      (0                ≡⟨ sym $ Nat.cancel-suc hyp ⟩
       m₁ ⊕ P.suc n₂    ≡⟨ sym $ Nat.suc+≡+suc m₁ ⟩∎
       P.suc (m₁ ⊕ n₂)  ∎)
  to-lemma₃ zero n₁ (P.suc m₂) zero hyp =
    ⊥-elim $ Nat.0≢+
      (0                ≡⟨ Nat.cancel-suc hyp ⟩
       n₁ ⊕ P.suc m₂    ≡⟨ sym $ Nat.suc+≡+suc n₁ ⟩∎
       P.suc (n₁ ⊕ m₂)  ∎)

  to-lemma :
    ∀ m₁ n₁ m₂ n₂ →
    Same-difference (m₁ , n₁) (m₂ , n₂) →
    Data.+ m₁ Data.- Data.+ n₁ ≡
    Data.+ m₂ Data.- Data.+ n₂
  to-lemma m₁ zero m₂ zero hyp =
    Data.+ (m₁ ⊕ 0)  ≡⟨ cong Data.+_ hyp ⟩
    Data.+ m₂        ≡⟨ cong Data.+_ (sym Nat.+-right-identity) ⟩∎
    Data.+ (m₂ ⊕ 0)  ∎
  to-lemma m₁ zero m₂ (P.suc n₂) hyp =
    Data.+ (m₁ ⊕ 0)       ≡⟨ cong Data.+_ Nat.+-right-identity ⟩
    Data.+ m₁             ≡⟨ to-lemma₁ hyp ⟩∎
    Data.+ m₂ +-[1+ n₂ ]  ∎
  to-lemma m₁ (P.suc n₁) m₂ zero hyp =
    Data.+ m₁ +-[1+ n₁ ]  ≡⟨ to-lemma₂ hyp ⟩
    Data.+ m₂             ≡⟨ cong Data.+_ (sym Nat.+-right-identity) ⟩∎
    Data.+ (m₂ ⊕ 0)       ∎
  to-lemma m₁ (P.suc n₁) m₂ (P.suc n₂) hyp =
    Data.+ m₁ +-[1+ n₁ ]  ≡⟨ to-lemma₃ _ _ _ _ hyp ⟩∎
    Data.+ m₂ +-[1+ n₂ ]  ∎

  to : ℤ → Data.ℤ
  to = Q.rec λ where
    .[]ʳ (m , n) → Data.+ m Data.- Data.+ n

    .[]-respects-relationʳ {x = m₁ , n₁} {y = m₂ , n₂} →
      to-lemma m₁ n₁ m₂ n₂

    .is-setʳ → Data.ℤ-set

  from : Data.ℤ → ℤ
  from (Data.+ n)    = + n
  from Data.-[1+ n ] = [ (0 , P.suc n) ]

  to∘from : ∀ i → to (from i) ≡ i
  to∘from (Data.+ n) =
    to (from (Data.+ n))      ≡⟨⟩
    Data.+ (n ⊕ 0)            ≡⟨ cong Data.+_ Nat.+-right-identity ⟩∎
    Data.+ n                  ∎
  to∘from Data.-[1+ n ] =
    to (from Data.-[1+ n ])  ≡⟨⟩
    Data.-[1+ n ]            ∎

  from-+_+-[1+_] :
    ∀ m n → from (Data.+ m +-[1+ n ]) ≡ [ (m , P.suc n) ]
  from-+ zero    +-[1+ n ]       = refl _
  from-+ P.suc m +-[1+ zero ]    = []≡[suc,suc]
  from-+ P.suc m +-[1+ P.suc n ] =
    from (Data.+ P.suc m +-[1+ P.suc n ])  ≡⟨⟩
    from (Data.+ m +-[1+ n ])              ≡⟨ from-+ m +-[1+ n ] ⟩
    [ (m , P.suc n) ]                      ≡⟨ []≡[suc,suc] ⟩∎
    [ (P.suc m , P.suc (P.suc n)) ]        ∎

  from∘to : ∀ i → from (to i) ≡ i
  from∘to = Q.elim-prop λ where
    .[]ʳ (m , zero) →
      from (to (+ m))  ≡⟨⟩
      + (m ⊕ 0)        ≡⟨ cong +_ Nat.+-right-identity ⟩∎
      + m              ∎
    .[]ʳ (m , P.suc n) →
      from (to [ (m , P.suc n) ])  ≡⟨⟩
      from (Data.+ m +-[1+ n ])    ≡⟨ from-+ m +-[1+ n ] ⟩∎
      [ (m , P.suc n) ]            ∎
    .is-propositionʳ _ → ℤ-set

-- The bijection is homomorphic with respect to +_/Data.+_.

ℤ↔ℤ-+ : _↔_.to ℤ↔ℤ (+ n) ≡ Data.+ n
ℤ↔ℤ-+ {n = n} =
  Data.+ (n ⊕ 0)  ≡⟨ cong Data.+_ Nat.+-right-identity ⟩∎
  Data.+ n        ∎

-- The bijection is homomorphic with respect to -[_]/Data.-[_].

ℤ↔ℤ--[] : _↔_.to ℤ↔ℤ -[ n ] ≡ Data.-[ n ]
ℤ↔ℤ--[] {n = zero}    = Data.+ 0  ∎
ℤ↔ℤ--[] {n = P.suc n} = Data.-[1+ n ]  ∎

------------------------------------------------------------------------
-- An eliminator and a recursor with poor computational behaviour

module _ where

  private

    -- An eliminator for integers. This eliminator is not exported,
    -- because it is basically just the eliminator for quotients.

    elim :
      (P : ℤ → Type p) →
      (∀ i → Is-set (P i)) →
      (f : ∀ m n → P [ (m , n) ]) →
      (∀ {p q} (s : Same-difference p q) →
       subst P ([]-respects-relation s) (uncurry f p) ≡ uncurry f q) →
      ∀ i → P i
    elim _ P-set f resp = Q.elim λ where
      .[]ʳ                   → uncurry f
      .[]-respects-relationʳ → resp
      .is-setʳ               → P-set

    -- The following computation rule holds by definition.

    elim-[] :
      (P : ℤ → Type p) →
      (P-set : ∀ i → Is-set (P i)) →
      (f : ∀ m n → P [ (m , n) ]) →
      (resp : ∀ {p q} (s : Same-difference p q) →
              subst P ([]-respects-relation s) (uncurry f p) ≡
              uncurry f q) →
      elim P P-set f resp [ (m , n) ] ≡ f m n
    elim-[] _ _ _ _ = refl _

private

  -- A helper function used in the implementation of elim.

  elim′ :
    (P : ℤ → Type p) →
    (∀ n → P (_↔_.from ℤ↔ℤ (Data.+ n))) →
    (∀ n → P (_↔_.from ℤ↔ℤ Data.-[1+ n ])) →
    ∀ i → P (_↔_.from ℤ↔ℤ i)
  elim′ _ p n (Data.+ m)    = p m
  elim′ _ p n Data.-[1+ m ] = n m

-- An eliminator for integers.
--
-- Note that the motive does not have to be a family of sets, and
-- that the function does not need to respect the relation
-- Same-difference.

elim :
  (P : ℤ → Type p) →
  (∀ m n → P [ (m , n) ]) →
  ∀ i → P i
elim P f i =                       $⟨ elim′ P (λ n → f n 0) (λ n → f 0 (P.suc n)) (_↔_.to ℤ↔ℤ i) ⟩
  P (_↔_.from ℤ↔ℤ (_↔_.to ℤ↔ℤ i))  ↝⟨ subst P (_↔_.left-inverse-of ℤ↔ℤ i) ⟩□
  P i                              □

mutual

  -- A "computation" rule for elim.
  --
  -- Here the function is required to respect Same-difference. Note that
  -- this "computation" rule does not (at the time of writing) in
  -- general hold by definition.

  elim-[] :
    {P : ℤ → Type p}
    (f : ∀ m n → P [ (m , n) ]) →
    (∀ {p q} (s : Same-difference p q) →
     subst P ([]-respects-relation s) (uncurry f p) ≡ uncurry f q) →
    elim P f [ (m , n) ] ≡ f m n
  elim-[] f hyp = elim-[]′ f (λ _ _ → hyp _)

  -- A variant of the computation rule in which the requirement to
  -- respect Same-difference has been replaced by a more specific
  -- condition.

  elim-[]′ :
    {P : ℤ → Type p}
    (f : ∀ m n → P [ (m , n) ]) →
    (∀ m n → subst P []≡[suc,suc] (f m n) ≡ f (P.suc m) (P.suc n)) →
    elim P f [ (m , n) ] ≡ f m n
  elim-[]′ {m = m} {n = zero} {P = P} f hyp =
    elim P f [ (m , 0) ]                                  ≡⟨⟩
    subst P (cong +_ Nat.+-right-identity) (f (m ⊕ 0) 0)  ≡⟨ sym $ subst-∘ _ _ _ ⟩
    subst (P ∘ +_) Nat.+-right-identity (f (m ⊕ 0) 0)     ≡⟨ elim¹ (λ eq → subst (P ∘ +_) eq (f _ _) ≡ f _ _) (subst-refl _ _) _ ⟩∎
    f m 0                                                 ∎

  elim-[]′ {m = m} {n = P.suc n} {P = P} f hyp =
    elim P f [ (m , P.suc n) ]                                          ≡⟨⟩

    subst P (_↔_.left-inverse-of ℤ↔ℤ [ (m , P.suc n) ]) $
      elim′ P (λ n → f n 0) (λ n → f 0 (P.suc n)) (Data.+ m +-[1+ n ])  ≡⟨ lemma m n ⟩∎

    f m (P.suc n)                                                       ∎
    where
    lemma :
      ∀ m n →
      subst P (_↔_.left-inverse-of ℤ↔ℤ [ (m , P.suc n) ])
        (elim′ P (λ n → f n 0) (λ n → f 0 (P.suc n))
           (Data.+ m +-[1+ n ])) ≡
      f m (P.suc n)
    lemma zero n =
      subst P (refl _) (f 0 (P.suc n))  ≡⟨ subst-refl _ _ ⟩∎
      f 0 (P.suc n)                     ∎
    lemma (P.suc m) zero =
      subst P []≡[suc,suc] (f m 0)  ≡⟨ hyp _ _ ⟩∎
      f (P.suc m) 1                 ∎
    lemma (P.suc m) (P.suc n) =
      subst P
        (trans (_↔_.left-inverse-of ℤ↔ℤ [ (m , P.suc n) ])
           []≡[suc,suc])
        (elim′ P (λ n → f n 0) (λ n → f 0 (P.suc n))
           (Data.+ m +-[1+ n ]))                              ≡⟨ sym $ subst-subst _ _ _ _ ⟩

      subst P []≡[suc,suc]
        (subst P (_↔_.left-inverse-of ℤ↔ℤ [ (m , P.suc n) ])
           (elim′ P (λ n → f n 0) (λ n → f 0 (P.suc n))
              (Data.+ m +-[1+ n ])))                          ≡⟨ cong (subst P ([]-respects-relation _)) $
                                                                 lemma m n ⟩

      subst P []≡[suc,suc] (f m (P.suc n))                    ≡⟨ hyp _ _ ⟩∎

      f (P.suc m) (P.suc (P.suc n))                           ∎

private

  -- A helper function used in the implementation of rec.

  rec′ : (ℕ → A) → (ℕ → A) → Data.ℤ → A
  rec′ p n (Data.+ m)    = p m
  rec′ p n Data.-[1+ m ] = n m

-- A recursor for integers.

rec : (ℕ → ℕ → A) → ℤ → A
rec {A = A} f =
  ℤ       ↔⟨ ℤ↔ℤ ⟩
  Data.ℤ  ↝⟨ rec′ (λ n → f n 0) (λ n → f 0 (P.suc n)) ⟩□
  A       □

-- The recursor could have been defined in terms of the eliminator.
--
-- The recursor is not defined in terms of the eliminator in this way
-- because (in at least some cases) this would lead to different
-- computational behaviour.

rec≡elim : (f : ℕ → ℕ → A) → rec f i ≡ elim (const _) f i
rec≡elim {i = i} f =
  rec f i                                                               ≡⟨⟩

  rec′ (λ n → f n 0) (λ n → f 0 (P.suc n)) (_↔_.to ℤ↔ℤ i)               ≡⟨ lemma (_↔_.to ℤ↔ℤ i) ⟩

  elim′ (const _) (λ n → f n 0) (λ n → f 0 (P.suc n)) (_↔_.to ℤ↔ℤ i)    ≡⟨ sym $ subst-const _ ⟩

  subst (const _) (_↔_.left-inverse-of ℤ↔ℤ i) $
    elim′ (const _) (λ n → f n 0) (λ n → f 0 (P.suc n)) (_↔_.to ℤ↔ℤ i)  ≡⟨⟩

  elim (const _) f i                                                    ∎
  where
  lemma :
    ∀ i →
    rec′ (λ n → f n 0) (λ n → f 0 (P.suc n)) i ≡
    elim′ (const _) (λ n → f n 0) (λ n → f 0 (P.suc n)) i
  lemma (Data.+ _)    = refl _
  lemma Data.-[1+ _ ] = refl _

-- A "computation" rule for rec.
--
-- Note that this "computation" rule does not (at the time of writing)
-- in general hold by definition.

rec-[] :
  (f : ℕ → ℕ → A) →
  (∀ {p q} → Same-difference p q → uncurry f p ≡ uncurry f q) →
  rec f [ (m , n) ] ≡ f m n
rec-[] {m = m} {n = n} f hyp =
  rec f [ (m , n) ]                                         ≡⟨ rec≡elim f ⟩
  elim (const _) f [ (m , n) ]                              ≡⟨ elim-[] f (λ {p q} s →
    subst (const _) ([]-respects-relation s) (uncurry f p)       ≡⟨ subst-const _ ⟩
    uncurry f p                                                  ≡⟨ hyp s ⟩∎
    uncurry f q                                                  ∎) ⟩∎
  f m n                                                     ∎

------------------------------------------------------------------------
-- Negation, addition and subtraction

-- A helper function that can be used to define unary operators on
-- integers.

unary-operator :
  (f : ℕ × ℕ → ℕ × ℕ) →
  (∀ {i j} →
   Same-difference i j →
   Same-difference (f i) (f j)) →
  ℤ → ℤ
unary-operator f resp = Q.rec λ where
  .[]ʳ i                   → [ f i ]
  .[]-respects-relationʳ s → []-respects-relation (resp s)
  .is-setʳ                 → ℤ-set

private

  -- A computation rule for unary-operator.
  --
  -- The function is not defined using the recursor above, but rather
  -- the quotient eliminator, to ensure that this computation rule
  -- holds by definition.

  unary-operator-[] :
    (f : ℕ × ℕ → ℕ × ℕ) →
    (resp : ∀ {i j} →
            Same-difference i j →
            Same-difference (f i) (f j)) →
    ∀ i → unary-operator f resp [ i ] ≡ [ f i ]
  unary-operator-[] _ _ _ = refl _

-- A helper function that can be used to define binary operators on
-- integers.

binary-operator :
  (f : ℕ × ℕ → ℕ × ℕ → ℕ × ℕ) →
  (∀ {i₁ i₂ j₁ j₂} →
   Same-difference i₁ i₂ →
   Same-difference j₁ j₂ →
   Same-difference (f i₁ j₁) (f i₂ j₂)) →
  ℤ → ℤ → ℤ
binary-operator f resp = Q.rec λ where
  .[]ʳ i → Q.rec λ where
    .[]ʳ j → [ f i j ]

    .[]-respects-relationʳ s →
      []-respects-relation (resp (Nat.+-comm (proj₁ i)) s)

    .is-setʳ → ℤ-set

  .[]-respects-relationʳ s → ⟨ext⟩ $ Q.elim-prop λ where
    .[]ʳ i → []-respects-relation (resp s (Nat.+-comm (proj₁ i)))

    .is-propositionʳ _ → +⇒≡ {n = 1} ℤ-set

  .is-setʳ →
    Π-closure ext 2 λ _ →
    ℤ-set

private

  -- A computation rule for binary-operator.
  --
  -- The function is not defined using the recursor above, but rather
  -- the quotient eliminator, to ensure that this computation rule
  -- holds by definition.

  binary-operator-[] :
    (f : ℕ × ℕ → ℕ × ℕ → ℕ × ℕ) →
    (resp : ∀ {i₁ i₂ j₁ j₂} →
            Same-difference i₁ i₂ →
            Same-difference j₁ j₂ →
            Same-difference (f i₁ j₁) (f i₂ j₂)) →
    ∀ i j → binary-operator f resp [ i ] [ j ] ≡ [ f i j ]
  binary-operator-[] _ _ _ _ = refl _

-- Negation.

infix 8 -_

-_ : ℤ → ℤ
-_ = unary-operator swap sym

-- Addition.

infixl 6 _+_

_+_ : ℤ → ℤ → ℤ
_+_ = binary-operator
  (Σ-zip _⊕_ _⊕_)
  (λ { {k₁ , k₂} {ℓ₁ , ℓ₂} {m₁ , m₂} {n₁ , n₂} hyp₁ hyp₂ →
       (k₁ ⊕ m₁) ⊕ (ℓ₂ ⊕ n₂)  ≡⟨ lemma k₁ ⟩
       (k₁ ⊕ ℓ₂) ⊕ (m₁ ⊕ n₂)  ≡⟨ cong₂ _⊕_ hyp₁ hyp₂ ⟩
       (k₂ ⊕ ℓ₁) ⊕ (m₂ ⊕ n₁)  ≡⟨ lemma k₂ ⟩∎
       (k₂ ⊕ m₂) ⊕ (ℓ₁ ⊕ n₁)  ∎
     })
  where
  lemma : ∀ _ {_ _ _} → _
  lemma a {b} {c} {d} =
    (a ⊕ b) ⊕ (c ⊕ d)  ≡⟨ sym $ Nat.+-assoc a ⟩
    a ⊕ (b ⊕ (c ⊕ d))  ≡⟨ cong (a ⊕_) $ Nat.+-assoc b ⟩
    a ⊕ ((b ⊕ c) ⊕ d)  ≡⟨ cong ((a ⊕_) ∘ (_⊕ d)) $ Nat.+-comm b ⟩
    a ⊕ ((c ⊕ b) ⊕ d)  ≡⟨ cong (a ⊕_) $ sym $ Nat.+-assoc c ⟩
    a ⊕ (c ⊕ (b ⊕ d))  ≡⟨ Nat.+-assoc a ⟩∎
    (a ⊕ c) ⊕ (b ⊕ d)  ∎

-- Subtraction.

infixl 6 _-_

_-_ : ℤ → ℤ → ℤ
i - j = i + - j

-- The implementation of negation given here matches the one in
-- Integer.

-₁≡-₁ : ∀ i → - (_↔_.from ℤ↔ℤ i) ≡ _↔_.from ℤ↔ℤ (Data.- i)
-₁≡-₁ (Data.+ zero)      = -[ 0 ]        ∎
-₁≡-₁ (Data.+ (P.suc n)) = -[ P.suc n ]  ∎
-₁≡-₁ Data.-[1+ n ]      = + P.suc n     ∎

-- A lemma used in the implementation of +≡+.

++-[1+]≡++-[1+] : + m + -[ P.suc n ] ≡ _↔_.from ℤ↔ℤ (Data.+ m +-[1+ n ])
++-[1+]≡++-[1+] {m = zero}    {n = n}       = refl _
++-[1+]≡++-[1+] {m = P.suc m} {n = zero}    =
  [ (P.suc (m ⊕ 0) , 1) ]  ≡⟨ cong (Q.[_] ∘ (_, 1) ∘ P.suc) Nat.+-right-identity ⟩
  [ (P.suc m , 1) ]        ≡⟨ sym []≡[suc,suc] ⟩∎
  [ (m , 0) ]              ∎
++-[1+]≡++-[1+] {m = P.suc m} {n = P.suc n} =
  + P.suc m + -[ P.suc (P.suc n) ]               ≡⟨ sym []≡[suc,suc] ⟩
  + m + -[ P.suc n ]                             ≡⟨ ++-[1+]≡++-[1+] ⟩
  _↔_.from ℤ↔ℤ (Data.+ m +-[1+ n ])              ≡⟨⟩
  _↔_.from ℤ↔ℤ (Data.+ P.suc m +-[1+ P.suc n ])  ∎

-- The implementation of addition given here matches the one in
-- Integer.

+≡+ :
  ∀ i →
  (_↔_.from ℤ↔ℤ i) + (_↔_.from ℤ↔ℤ j) ≡ _↔_.from ℤ↔ℤ (i Data.+ j)
+≡+ {j = Data.+ n}      (Data.+ m) = + (m ⊕ n)  ∎
+≡+ {j = Data.-[1+ n ]} (Data.+ m) = ++-[1+]≡++-[1+]

+≡+ {j = Data.+ n} Data.-[1+ m ] =
  -[ P.suc m ] + + n                 ≡⟨ []-respects-relation (
      n ⊕ P.suc m                         ≡⟨ Nat.+-comm n ⟩
      P.suc m ⊕ n                         ≡⟨ sym $ cong₂ _⊕_ (Nat.+-right-identity {n = P.suc m}) Nat.+-right-identity ⟩∎
      P.suc m ⊕ 0 ⊕ (n ⊕ 0)               ∎) ⟩
  + n + -[ P.suc m ]                 ≡⟨ ++-[1+]≡++-[1+] ⟩∎
  _↔_.from ℤ↔ℤ (Data.+ n +-[1+ m ])  ∎

+≡+ {j = Data.-[1+ n ]} Data.-[1+ m ] =
  -[ P.suc m ⊕ P.suc n ]      ≡⟨ cong (-[_] ∘ P.suc) $ sym $ Nat.suc+≡+suc _ ⟩∎
  -[ P.suc (P.suc (m ⊕ n)) ]  ∎

-- The implementation of subtraction given here matches the one in
-- Integer.

-≡- :
  ∀ i j →
  (_↔_.from ℤ↔ℤ i) - (_↔_.from ℤ↔ℤ j) ≡ _↔_.from ℤ↔ℤ (i Data.- j)
-≡- i j =
  (_↔_.from ℤ↔ℤ i) - (_↔_.from ℤ↔ℤ j)       ≡⟨⟩
  (_↔_.from ℤ↔ℤ i) + - (_↔_.from ℤ↔ℤ j)     ≡⟨ cong (λ j → _↔_.from ℤ↔ℤ i + j) $ -₁≡-₁ j ⟩
  _↔_.from ℤ↔ℤ i + _↔_.from ℤ↔ℤ (Data.- j)  ≡⟨ +≡+ i ⟩
  _↔_.from ℤ↔ℤ (i Data.+ Data.- j)          ≡⟨⟩
  _↔_.from ℤ↔ℤ (i Data.- j)                 ∎

------------------------------------------------------------------------
-- Some lemmas related to equality

-- The Same-difference relation is pointwise equivalent to equality
-- under [_] (assuming propositional extensionality).

Same-difference≃[]≡[] :
  Propositional-extensionality lzero →
  Same-difference i j ≃ ([ i ] ≡ [ j ])
Same-difference≃[]≡[] prop-ext =
  related≃[equal]
    prop-ext
    Same-difference-is-equivalence-relation
    (λ {p} → Same-difference-propositional {p = p})

-- Non-negative integers are not equal to negative integers.

+≢-[1+] : + m ≢ -[ P.suc n ]
+≢-[1+] {m = m} {n = n} =
  Stable-¬
    [ + m ≡ -[ P.suc n ]                     ↔⟨⟩
      [ (m , 0) ] ≡ [ (0 , P.suc n) ]        ↔⟨ inverse $ Same-difference≃[]≡[] prop-ext ⟩
      Same-difference (m , 0) (0 , P.suc n)  ↔⟨⟩
      m ⊕ P.suc n ≡ 0                        ↝⟨ trans (Nat.suc+≡+suc m) ⟩
      P.suc (m ⊕ n) ≡ 0                      ↝⟨ Nat.0≢+ ∘ sym ⟩□
      ⊥                                      □
    ]

-- Non-positive integers are not equal to positive integers.

+[1+]≢- : + P.suc m ≢ -[ n ]
+[1+]≢- {m = m} {n = n} =
  Stable-¬
    [ + P.suc m ≡ -[ n ]                     ↔⟨⟩
      [ (P.suc m , 0) ] ≡ [ (0 , n) ]        ↔⟨ inverse $ Same-difference≃[]≡[] prop-ext ⟩
      Same-difference (P.suc m , 0) (0 , n)  ↔⟨⟩
      P.suc m ⊕ n ≡ 0                        ↝⟨ Nat.0≢+ ∘ sym ⟩□
      ⊥                                      □
    ]

-- The +_ "constructor" is cancellative (assuming propositional
-- extensionality).

+-cancellative :
  Propositional-extensionality lzero →
  + m ≡ + n → m ≡ n
+-cancellative {m = m} {n = n} prop-ext =
  + m ≡ + n                  ↔⟨⟩
  [ (m , 0) ] ≡ [ (n , 0) ]  ↔⟨ inverse $ Same-difference≃[]≡[] prop-ext ⟩
  m ⊕ 0 ≡ 0 ⊕ n              ↝⟨ trans (sym Nat.+-right-identity) ⟩□
  m ≡ n                      □

-- The -[_] "constructor" is cancellative (assuming propositional
-- extensionality).

-[]-cancellative :
  Propositional-extensionality lzero →
  -[ m ] ≡ -[ n ] → m ≡ n
-[]-cancellative {m = m} {n = n} prop-ext =
  -[ m ] ≡ -[ n ]  ↝⟨ cong (-_) ⟩
  + m ≡ + n        ↝⟨ +-cancellative prop-ext ⟩□
  m ≡ n            □

-- Equality of integers is decidable (assuming propositional
-- extensionality).

infix 4 [_]_≟_

[_]_≟_ :
  Propositional-extensionality lzero →
  Decidable-equality ℤ
[_]_≟_ prop-ext = Q.elim-prop λ where
  .[]ʳ i → Q.elim-prop λ where
     .[]ʳ _ →
       ⊎-map (_≃_.to $ Same-difference≃[]≡[] prop-ext)
             (_∘ _≃_.from (Same-difference≃[]≡[] prop-ext))
             (Same-difference-decidable i)
     .is-propositionʳ _ →
       Dec-closure-propositional ext ℤ-set
  .is-propositionʳ _ →
    Π-closure ext 1 λ _ →
    Dec-closure-propositional ext ℤ-set

-- Erased equality of integers is decidable.

infix 4 _≟_

_≟_ : Decidable-erased-equality ℤ
_≟_ = Q.elim-prop λ where
  .[]ʳ i → Q.elim-prop λ where
     .[]ʳ _ →
       Dec-Erased-map
         (from-equivalence $ Same-difference≃[]≡[] prop-ext) $
       Dec→Dec-Erased $
       Same-difference-decidable i
     .is-propositionʳ _ →
       Is-proposition-Dec-Erased ext ℤ-set
  .is-propositionʳ _ →
    Π-closure ext 1 λ _ →
    Is-proposition-Dec-Erased ext ℤ-set

------------------------------------------------------------------------
-- The successor and predecessor functions

-- The successor function.

suc : ℤ → ℤ
suc = Q.rec λ where
  .[]ʳ (m , n) → [ (P.suc m , n) ]

  .[]-respects-relationʳ {x = m₁ , m₂} {y = n₁ , n₂} hyp →
    []-respects-relation
      (P.suc (m₁ ⊕ n₂)  ≡⟨ cong P.suc hyp ⟩
       P.suc (m₂ ⊕ n₁)  ≡⟨ Nat.suc+≡+suc _ ⟩∎
       m₂ ⊕ P.suc n₁    ∎ )

  .is-setʳ → ℤ-set

-- The function suc adds one to its input.

suc≡1+ : ∀ i → suc i ≡ + 1 + i
suc≡1+ = elim _ λ _ _ → refl _

-- The predecessor function.

pred : ℤ → ℤ
pred = Q.rec λ where
  .[]ʳ (m , n) → [ (m , P.suc n) ]

  .[]-respects-relationʳ {x = m₁ , m₂} {y = n₁ , n₂} hyp →
    []-respects-relation
      (m₁ ⊕ P.suc n₂    ≡⟨ sym $ Nat.suc+≡+suc _ ⟩
       P.suc (m₁ ⊕ n₂)  ≡⟨ cong P.suc hyp ⟩∎
       P.suc (m₂ ⊕ n₁)  ∎)

  .is-setʳ → ℤ-set

-- The function pred subtracts one from its input.

pred≡-1+ : ∀ i → pred i ≡ -[ 1 ] + i
pred≡-1+ = elim _ λ _ _ → refl _

-- An equivalence between ℤ and ℤ corresponding to the successor
-- function.

successor : ℤ ≃ ℤ
successor = Eq.↔→≃
  suc
  pred
  (elim _ λ m _ → []-respects-relation (cong P.suc (Nat.+-comm m)))
  (elim _ λ m _ → []-respects-relation (cong P.suc (Nat.+-comm m)))

------------------------------------------------------------------------
-- Positive, negative

-- The property of being positive.

Positive : ℤ → Type
Positive = Data.Positive ∘ _↔_.to ℤ↔ℤ

-- Positive is propositional.

Positive-propositional : ∀ i → Is-proposition (Positive i)
Positive-propositional _ = Data.Positive-propositional

-- The property of being negative.

Negative : ℤ → Type
Negative = Data.Negative ∘ _↔_.to ℤ↔ℤ

-- Negative is propositional.

Negative-propositional : ∀ i → Is-proposition (Negative i)
Negative-propositional _ = Data.Negative-propositional

-- No integer is both positive and negative.

¬+- : ∀ i → Positive i → Negative i → ⊥₀
¬+- _ = Data.¬+-

-- No integer is both positive and equal to zero.

¬+0 : Positive i → i ≡ + 0 → ⊥₀
¬+0 pos ≡0 = Data.¬+0 pos (_↔_.from-to ℤ↔ℤ (sym ≡0))

-- No integer is both negative and equal to zero.

¬-0 : Negative i → i ≡ + 0 → ⊥₀
¬-0 neg ≡0 = Data.¬-0 neg (_↔_.from-to ℤ↔ℤ (sym ≡0))

-- One can decide if an integer is negative, zero or positive.

-⊎0⊎+ : ∀ i → Negative i ⊎ i ≡ + 0 ⊎ Positive i
-⊎0⊎+ i =
  ⊎-map id (⊎-map (sym ∘ _↔_.to-from ℤ↔ℤ) id)
    (Data.-⊎0⊎+ $ _↔_.to ℤ↔ℤ i)

-- If i and j are positive, then i + j is positive.

>0→>0→+>0 : ∀ i j → Positive i → Positive j → Positive (i + j)
>0→>0→+>0 i j i+ j+ =                                                   $⟨ Data.>0→>0→+>0 (_↔_.to ℤ↔ℤ i) (_↔_.to ℤ↔ℤ j) i+ j+ ⟩

  Data.Positive (_↔_.to ℤ↔ℤ i Data.+ _↔_.to ℤ↔ℤ j)                      ↝⟨ subst Data.Positive $
                                                                           sym $ _↔_.from-to ℤ↔ℤ $ sym $ +≡+ (_↔_.to ℤ↔ℤ i) ⟩
  Data.Positive (_↔_.to ℤ↔ℤ (_↔_.from ℤ↔ℤ (_↔_.to ℤ↔ℤ i) +
                             _↔_.from ℤ↔ℤ (_↔_.to ℤ↔ℤ j)))              ↔⟨⟩

  Positive (_↔_.from ℤ↔ℤ (_↔_.to ℤ↔ℤ i) + _↔_.from ℤ↔ℤ (_↔_.to ℤ↔ℤ j))  ↝⟨ subst Positive $
                                                                           cong₂ _+_
                                                                             (_↔_.left-inverse-of ℤ↔ℤ i)
                                                                             (_↔_.left-inverse-of ℤ↔ℤ j) ⟩□
  Positive (i + j)                                                      □

-- If i and j are negative, then i + j is negative.

<0→<0→+<0 : ∀ i j → Negative i → Negative j → Negative (i + j)
<0→<0→+<0 i j i- j- =                                                   $⟨ Data.<0→<0→+<0 (_↔_.to ℤ↔ℤ i) (_↔_.to ℤ↔ℤ j) i- j- ⟩

  Data.Negative (_↔_.to ℤ↔ℤ i Data.+ _↔_.to ℤ↔ℤ j)                      ↝⟨ subst Data.Negative $
                                                                           sym $ _↔_.from-to ℤ↔ℤ $ sym $ +≡+ (_↔_.to ℤ↔ℤ i) ⟩
  Data.Negative (_↔_.to ℤ↔ℤ (_↔_.from ℤ↔ℤ (_↔_.to ℤ↔ℤ i) +
                             _↔_.from ℤ↔ℤ (_↔_.to ℤ↔ℤ j)))              ↔⟨⟩

  Negative (_↔_.from ℤ↔ℤ (_↔_.to ℤ↔ℤ i) + _↔_.from ℤ↔ℤ (_↔_.to ℤ↔ℤ j))  ↝⟨ subst Negative $
                                                                           cong₂ _+_
                                                                             (_↔_.left-inverse-of ℤ↔ℤ i)
                                                                             (_↔_.left-inverse-of ℤ↔ℤ j) ⟩□
  Negative (i + j)                                                      □

------------------------------------------------------------------------
-- The group of integers

-- The group of integers.

ℤ-group : Group lzero
ℤ-group .Group.Carrier        = ℤ
ℤ-group .Group.Carrier-is-set = ℤ-set
ℤ-group .Group._∘_            = _+_
ℤ-group .Group.id             = + 0
ℤ-group .Group._⁻¹            = -_
ℤ-group .Group.assoc          =
  elim _ λ m₁ n₁ → elim _ λ _ _ → elim _ λ _ _ →
  cong [_] $ cong₂ _,_
    (Nat.+-assoc m₁)
    (Nat.+-assoc n₁)
ℤ-group .Group.left-identity =
  elim _ λ _ _ → refl _
ℤ-group .Group.right-identity =
  elim _ λ _ _ →
  cong [_] $ cong₂ _,_
        Nat.+-right-identity
        Nat.+-right-identity
ℤ-group .Group.left-inverse =
  elim _ λ _ n →
  []-respects-relation (cong (_⊕ 0) $ Nat.+-comm n)
ℤ-group .Group.right-inverse =
  elim _ λ m _ →
  []-respects-relation (cong (_⊕ 0) $ Nat.+-comm m)

-- ℤ-group is isomorphic to Data.ℤ-group.

ℤ≃ᴳℤ : ℤ-group ≃ᴳ Data.ℤ-group
ℤ≃ᴳℤ = G.≃ᴳ-sym λ where
  .G.Homomorphic.related         → Eq.↔⇒≃ (inverse ℤ↔ℤ)
  .G.Homomorphic.homomorphic i _ → sym (+≡+ i)

-- ℤ-group is equal to Data.ℤ-group (assuming univalence).

ℤ≡ℤ :
  Univalence lzero →
  ℤ-group ≡ Data.ℤ-group
ℤ≡ℤ univ = _≃_.to (G.≃ᴳ≃≡ ext univ) ℤ≃ᴳℤ

-- The group of integers is generated by + 1.

ℤ-generated-by-1 : Generated-by ℤ-group (+ 1)
ℤ-generated-by-1 =
  C.≃ᴳ→Generated-by→Generated-by
    (G.≃ᴳ-sym ℤ≃ᴳℤ)
    C.ℤ-generated-by-1

-- The group of integers is cyclic.

ℤ-cyclic : Cyclic ℤ-group
ℤ-cyclic = ∣ _ , ℤ-generated-by-1 ∣

-- The group of integers is abelian.

ℤ-abelian : Abelian ℤ-group
ℤ-abelian = C.Cyclic→Abelian ℤ-group ℤ-cyclic

-- The direct product of the group of integers and the group of
-- integers is not cyclic.

ℤ×ℤ-not-cyclic : ¬ Cyclic (ℤ-group G.× ℤ-group)
ℤ×ℤ-not-cyclic =
  Cyclic (ℤ-group G.× ℤ-group)            ↝⟨ C.≃ᴳ→Cyclic→Cyclic (G.↝-× ℤ≃ᴳℤ ℤ≃ᴳℤ) ⟩
  Cyclic (Data.ℤ-group G.× Data.ℤ-group)  ↝⟨ C.ℤ×ℤ-not-cyclic ⟩□
  ⊥                                       □

-- The group of integers is not isomorphic to the direct product of
-- the group of integers and the group of integers.

ℤ≄ᴳℤ×ℤ : ¬ ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)
ℤ≄ᴳℤ×ℤ =
  ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)                 ↝⟨ G.↝ᴳ-trans (G.≃ᴳ-sym ℤ≃ᴳℤ) ∘ flip G.↝ᴳ-trans (G.↝-× ℤ≃ᴳℤ ℤ≃ᴳℤ) ⟩
  Data.ℤ-group ≃ᴳ (Data.ℤ-group G.× Data.ℤ-group)  ↝⟨ C.ℤ≄ᴳℤ×ℤ ⟩□
  ⊥                                                □

-- The group of integers is not equal to the direct product of the
-- group of integers and the group of integers.

ℤ≢ℤ×ℤ : ℤ-group ≢ (ℤ-group G.× ℤ-group)
ℤ≢ℤ×ℤ =
  ℤ-group ≡ (ℤ-group G.× ℤ-group)   ↝⟨ flip (subst (ℤ-group ≃ᴳ_)) G.↝ᴳ-refl ⟩
  ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)  ↝⟨ ℤ≄ᴳℤ×ℤ ⟩□
  ⊥                                 □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Reported by guillaume.brunerie, Sep 18, 2013
-- Andreas, 2013-10-27  issue submitted by Guilliaume Brunerie

{-# OPTIONS --copatterns #-}

module Issue907 where

-- Globular types as a coinductive record

record Glob : Set1 where
  coinductive
  field
    Ob : Set
    Hom : (a b : Ob) → Glob
open Glob public

Glob-corec : {A : Set1} (Ob* : A → Set)
  (Hom* : (x : A) (a b : Ob* x) → A) → (A → Glob)
Ob  (Glob-corec Ob* Hom* x)     = Ob* x
Hom (Glob-corec Ob* Hom* x) a b = Glob-corec Ob* Hom* (Hom* x a b)

-- For the second equation to type-check,
-- we need to reduce with the first equation!

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Oscar.Category.CategoryAction where

open import Oscar.Category.Action
open import Oscar.Category.Category
open import Oscar.Category.SemigroupoidAction
open import Oscar.Category.Setoid
open import Oscar.Level

module _ {𝔊𝔬 𝔊𝔪 𝔊𝔮} (category : Category 𝔊𝔬 𝔊𝔪 𝔊𝔮) where
  open Category category

  module _ {𝔄𝔬 𝔄𝔮} (action : Action ⋆ 𝔄𝔬 𝔄𝔮) where
    open Action action

    record IsCategoryAction
      (_◂_ : ∀ {x y} → x ↦ y → ↥ x → ↥ y)
      : Set (𝔊𝔬 ⊔ 𝔊𝔪 ⊔ 𝔊𝔮 ⊔ 𝔄𝔬 ⊔ 𝔄𝔮) where
      field ⦃ isSemigroupoidAction ⦄ : IsSemigroupoidAction semigroupoid action _◂_
      field identity : ∀ {x} → (s : ↥ x) → ε ◂ s ≋ s

open IsCategoryAction ⦃ … ⦄ public

record CategoryAction 𝔊𝔬 𝔊𝔪 𝔊𝔮 𝔄𝔬 𝔄𝔮 : Set (lsuc (𝔊𝔬 ⊔ 𝔊𝔪 ⊔ 𝔊𝔮 ⊔ 𝔄𝔬 ⊔ 𝔄𝔮)) where
  constructor [_/_]
  field category : Category 𝔊𝔬 𝔊𝔪 𝔊𝔮
  open Category category public

  field action : Action ⋆ 𝔄𝔬 𝔄𝔮
  open Action action public

  field _◂_ : ∀ {x y} → x ↦ y → ↥ x → ↥ y
  field ⦃ isCategoryAction ⦄ : IsCategoryAction category action _◂_

  semgroupoidAction : SemigroupoidAction _ _ _ _ _
  SemigroupoidAction.semigroupoid semgroupoidAction = semigroupoid
  SemigroupoidAction.action semgroupoidAction = action
  SemigroupoidAction._◂_ semgroupoidAction = _◂_


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Morphisms between algebraic structures
------------------------------------------------------------------------

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

module Algebra.Morphism where

open import Relation.Binary
open import Algebra
open import Algebra.FunctionProperties
import Algebra.Properties.Group as GroupP
open import Function
open import Level
import Relation.Binary.Reasoning.Setoid as EqR

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

module Definitions {f t ℓ}
                   (From : Set f) (To : Set t) (_≈_ : Rel To ℓ) where
  Morphism : Set _
  Morphism = From → To

  Homomorphic₀ : Morphism → From → To → Set _
  Homomorphic₀ ⟦_⟧ ∙ ∘ = ⟦ ∙ ⟧ ≈ ∘

  Homomorphic₁ : Morphism → Fun₁ From → Op₁ To → Set _
  Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ (∘ ⟦ x ⟧)

  Homomorphic₂ : Morphism → Fun₂ From → Op₂ To → Set _
  Homomorphic₂ ⟦_⟧ _∙_ _∘_ =
    ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)

------------------------------------------------------------------------
-- Structure homomorphisms

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : Semigroup c₁ ℓ₁)
         (To   : Semigroup c₂ ℓ₂) where

  private
    module F = Semigroup From
    module T = Semigroup To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsSemigroupMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
      ∙-homo  : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_

  syntax IsSemigroupMorphism From To F = F Is From -Semigroup⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : Monoid c₁ ℓ₁)
         (To   : Monoid c₂ ℓ₂) where

  private
    module F = Monoid From
    module T = Monoid To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsMonoidMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      sm-homo : IsSemigroupMorphism F.semigroup T.semigroup ⟦_⟧
      ε-homo  : Homomorphic₀ ⟦_⟧ F.ε T.ε

    open IsSemigroupMorphism sm-homo public

  syntax IsMonoidMorphism From To F = F Is From -Monoid⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : CommutativeMonoid c₁ ℓ₁)
         (To   : CommutativeMonoid c₂ ℓ₂) where

  private
    module F = CommutativeMonoid From
    module T = CommutativeMonoid To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧

    open IsMonoidMorphism mn-homo public

  syntax IsCommutativeMonoidMorphism From To F = F Is From -CommutativeMonoid⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : IdempotentCommutativeMonoid c₁ ℓ₁)
         (To   : IdempotentCommutativeMonoid c₂ ℓ₂) where

  private
    module F = IdempotentCommutativeMonoid From
    module T = IdempotentCommutativeMonoid To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsIdempotentCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧

    open IsMonoidMorphism mn-homo public

    isCommutativeMonoidMorphism :
      IsCommutativeMonoidMorphism F.commutativeMonoid T.commutativeMonoid ⟦_⟧
    isCommutativeMonoidMorphism = record { mn-homo = mn-homo }

  syntax IsIdempotentCommutativeMonoidMorphism From To F = F Is From -IdempotentCommutativeMonoid⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : Group c₁ ℓ₁)
         (To   : Group c₂ ℓ₂) where

  private
    module F = Group From
    module T = Group To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsGroupMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧

    open IsMonoidMorphism mn-homo public

    ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
    ⁻¹-homo x = let open EqR T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin
      ⟦ x F.⁻¹ ⟧ T.∙ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (x F.⁻¹) x) ⟩
      ⟦ x F.⁻¹ F.∙ x ⟧     ≈⟨ ⟦⟧-cong (F.inverseˡ x) ⟩
      ⟦ F.ε ⟧              ≈⟨ ε-homo ⟩
      T.ε ∎

  syntax IsGroupMorphism From To F = F Is From -Group⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : AbelianGroup c₁ ℓ₁)
         (To   : AbelianGroup c₂ ℓ₂) where

  private
    module F = AbelianGroup From
    module T = AbelianGroup To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsAbelianGroupMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      gp-homo : IsGroupMorphism F.group T.group ⟦_⟧

    open IsGroupMorphism gp-homo public

  syntax IsAbelianGroupMorphism From To F = F Is From -AbelianGroup⟶ To

module _ {c₁ ℓ₁ c₂ ℓ₂}
         (From : Ring c₁ ℓ₁)
         (To   : Ring c₂ ℓ₂) where

  private
    module F = Ring From
    module T = Ring To
  open Definitions F.Carrier T.Carrier T._≈_

  record IsRingMorphism (⟦_⟧ : Morphism) :
         Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
    field
      +-abgp-homo : ⟦_⟧ Is F.+-abelianGroup -AbelianGroup⟶ T.+-abelianGroup
      *-mn-homo   : ⟦_⟧ Is F.*-monoid -Monoid⟶ T.*-monoid

  syntax IsRingMorphism From To F = F Is From -Ring⟶ To


text:
module Function.Equals.Proofs where

import      Lvl
open import Data
import      Functional
import      Function.Equals
open import Logic.Predicate
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Function
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Syntax.Type
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓₑ ℓᵤ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ : Lvl.Level

module Dependent where
  open        Functional using (id)
  open import Functional.Dependent
  open        Function.Equals.Dependent

  module _ {A : Type{ℓ₁}} {B : A → Type{ℓ₂}} ⦃ equiv-B : ∀{a} → Equiv{ℓₑ₂}(B(a)) ⦄ where
    [⊜]-identityₗ : Identityₗ {T₂ = (a : A) → B(a)} (_∘_)(id)
    _⊜_.proof (Identityₗ.proof [⊜]-identityₗ) {x} = reflexivity(_≡_) ⦃ Equiv.reflexivity equiv-B ⦄

  module _ {A : Type{ℓ₁}} {B : Type{ℓ₂}} {C : B → Type{ℓ₂}} ⦃ equiv-C : ∀{b} → Equiv{ℓₑ₃}(C(b)) ⦄ where
    [⊜][∘]ₗ-function-raw : ∀{f₁ f₂ : (b : B) → C(b)}{g : A → B} → (f₁ ⊜ f₂) → ((f₁ ∘ g) ⊜ (f₂ ∘ g))
    [⊜][∘]ₗ-function-raw {g = g} (intro feq) = intro(\{x} → feq{g(x)})

  module _ {A : Type{ℓ₁}} {B : A → Type{ℓ₂}} {C : (a : A) → B(a) → Type{ℓ₃}} ⦃ equiv-C : ∀{a}{b} → Equiv{ℓₑ₃}(C(a)(b)) ⦄ where
    [⊜][∘ₛ]ₗ-function-raw : ∀{f₁ f₂ : (a : A) → (b : B(a)) → C(a)(b)}{g : (a : A) → B(a)} → (f₁ ⊜ f₂) → ((f₁ ∘ₛ g) ⊜ (f₂ ∘ₛ g))
    [⊜][∘ₛ]ₗ-function-raw {g = g} (intro feq) = intro(\{x} → _⊜_.proof (feq{x}) {g(x)})

  -- module _ {A : Type{ℓ₁}} {B : Type{ℓ₂}} {C : B → Type{ℓ₃}} ⦃ _ : Equiv(B) ⦄ ⦃ equiv-C : ∀{b} → Equiv(C(b)) ⦄ {f₁ f₂ : (b : B) → C(b)} ⦃ _ : Function(f₂) ⦄ where (TODO: Requires Function to be able to take a dependent function)
    -- [⊜][∘]-binaryOperator-raw : (f₁ ⊜ f₂) → ∀{g₁ g₂ : A → B} → (g₁ ⊜ g₂) → (f₁ ∘ g₁ ⊜ f₂ ∘ g₂)
    -- [⊜][∘]-binaryOperator-raw feq (intro geq) = [⊜][∘]ₗ-function-raw feq 🝖 (intro(congruence₁(f₂) (geq)))

open Functional
open Function.Equals

private variable A B C D A₁ A₂ B₁ B₂ : Type{ℓ}

-- TODO: Rename all these so that they mention (_∘_)
module _ ⦃ _ : let _ = A in Equiv{ℓₑ₂}(B) ⦄ where
  [⊜]-identityₗ : Identityₗ {T₂ = A → B} (_∘_)(id)
  _⊜_.proof(Identityₗ.proof([⊜]-identityₗ)) = reflexivity(_≡_)

  [⊜]-identityᵣ : Identityᵣ {T₁ = A → B} (_∘_)(id)
  _⊜_.proof(Identityᵣ.proof([⊜]-identityᵣ)) = reflexivity(_≡_)

module _ ⦃ _ : Equiv{ℓₑ}(A) ⦄ where
  [⊜]-identity : Identity {T = A → A} (_∘_)(id)
  [⊜]-identity = intro ⦃ left = [⊜]-identityₗ ⦄ ⦃ right = [⊜]-identityᵣ ⦄

module _ ⦃ _ : let _ = A ; _ = B ; _ = C ; _ = D in Equiv{ℓₑ₄}(D) ⦄ where
  [⊜]-associativity : Names.AssociativityPattern {T₁ = C → D} {T₂ = B → C} {T₃ = A → B} (_∘_)(_∘_)(_∘_)(_∘_)
  _⊜_.proof ([⊜]-associativity {f} {g} {h}) {x} = reflexivity(_≡_)

module _ ⦃ _ : Equiv{ℓₑ₁}(Empty{ℓₑ}) ⦄ where
  [⊜]-emptyₗ : ∀{f g : A → Empty{ℓₑ}} → (f ⊜ g)
  [⊜]-emptyₗ {f = f} = intro(\{x} → empty(f(x)))

module _ ⦃ _ : Equiv{ℓₑ}(A) ⦄ where
  [⊜]-emptyᵣ : ∀{f g : Empty{ℓₑ} → A} → (f ⊜ g)
  [⊜]-emptyᵣ = intro(\{})

module _ ⦃ _ : Equiv{ℓₑ}(Unit{ℓᵤ}) ⦄ where
  [⊜]-unitₗ : ∀{f g : A → Unit{ℓᵤ}} → (f ⊜ g)
  [⊜]-unitₗ = intro(reflexivity(_≡_))

module _ ⦃ _ : let _ = A ; _ = B ; _ = C in Equiv{ℓₑ₃}(C) ⦄ where
  [⊜][∘]ₗ-function-raw : ∀{f₁ f₂ : B → C}{g : A → B} → (f₁ ⊜ f₂) → ((f₁ ∘ g) ⊜ (f₂ ∘ g))
  [⊜][∘]ₗ-function-raw {g = g} (intro feq) = intro(\{x} → feq{g(x)})

module _ ⦃ _ : let _ = A in Equiv{ℓₑ₂}(B) ⦄ ⦃ _ : Equiv{ℓₑ₃}(C) ⦄ {f₁ f₂ : B → C} ⦃ func₂ : Function(f₂) ⦄ {g₁ g₂ : A → B} where
  [⊜][∘]-binaryOperator-raw : (f₁ ⊜ f₂) → (g₁ ⊜ g₂) → (f₁ ∘ g₁ ⊜ f₂ ∘ g₂)
  [⊜][∘]-binaryOperator-raw feq (intro geq) = [⊜][∘]ₗ-function-raw feq 🝖 (intro(congruence₁(f₂) (geq)))

module _ ⦃ _ : let _ = A in Equiv{ℓₑ₂}(B) ⦄ ⦃ _ : Equiv{ℓₑ₃}(C) ⦄ ⦃ function : ∀{f : B → C} → Function(f) ⦄ where
  instance
    [⊜][∘]-binaryOperator : BinaryOperator(_∘_ {X = A}{Y = B}{Z = C})
    BinaryOperator.congruence [⊜][∘]-binaryOperator = [⊜][∘]-binaryOperator-raw

module _ ⦃ _ : let _ = A in Equiv{ℓₑ₂}(B) ⦄ where
  [⊜]-abstract : ∀{a b : B} → (a ≡ b) → ((x ↦ a) ⊜ ((x ↦ b) :of: (A → B)))
  [⊜]-abstract {a} {b} x = intro x

  [⊜]-apply : ∀{f g : A → B} → (f ⊜ g) → (∀{x} → (f(x) ≡ g(x)))
  [⊜]-apply (intro proof) = proof

-- TODO: Is this correct?
-- [⊜]-not-all : ∀{ℓ₁ ℓ₂}{T₁ : Type{ℓ₁}}{T₂ : Type{ℓ₂}} → (∀{f g : T₁ → T₂} → (f ⊜ g)) → IsEmpty(T₁)
-- [⊜]-not-all{_}{_} {_} {_}{_} = intro(\{})

{- TODO: What assumptions? Unprovable?
module _
  {ℓ} -- {ℓ₁}{ℓ₂}{ℓ₃}{ℓ₄}
  {A : Type{ℓ}} ⦃ _ : Equiv(A) ⦄
  {B : Type{ℓ}} ⦃ _ : Equiv(B) ⦄
  {C : Type{ℓ}} ⦃ eq-c : Equiv(C) ⦄
  {D : Type{ℓ}} ⦃ eq-d : Equiv(D) ⦄
  {f : (A → B) → (C → D)}
  ⦃ fn : ∀{ab} → Function {T₁ = C} ⦃ eq-c ⦄ {T₂ = D} ⦃ eq-d ⦄ (f(ab)) ⦄
  where

  instance
    [⊜]-function : Function {T₁ = A → B} ⦃ [⊜]-equiv ⦄ {T₂ = C → D} ⦃ [⊜]-equiv ⦄ (f)
    _⊜_.proof (Function.congruence ([⊜]-function) {g} {h} (intro eq)) {x} = {!!}
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Definition.Conversion.Conversion where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.RedSteps
open import Definition.Typed.Properties
open import Definition.Conversion
open import Definition.Conversion.Stability
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Equality
open import Definition.Typed.Consequences.Reduction

open import Tools.Product
import Tools.PropositionalEquality as PE

mutual

  -- Conversion of algorithmic equality.
  convConv↑Term : ∀ {t u A B Γ Δ l}
                → ⊢ Γ ≡ Δ
                → Γ ⊢ A ≡ B ^ [ ! , l ]
                → Γ ⊢ t [conv↑] u ∷ A ^ l
                → Δ ⊢ t [conv↑] u ∷ B ^ l
  convConv↑Term Γ≡Δ A≡B ([↑]ₜ B₁ t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    let _ , ⊢B = syntacticEq A≡B
        B′ , whnfB′ , D′ = whNorm ⊢B
        B₁≡B′ = trans (sym (subset* D)) (trans A≡B (subset* (red D′)))
    in  [↑]ₜ B′ t′ u′ (stabilityRed* Γ≡Δ (red D′))
             (stabilityRed*Term Γ≡Δ (conv* d B₁≡B′))
             (stabilityRed*Term Γ≡Δ (conv* d′ B₁≡B′)) whnfB′ whnft′ whnfu′
             (convConv↓Term Γ≡Δ B₁≡B′ whnfB′ t<>u)

  -- Conversion of algorithmic equality with terms and types in WHNF.
  convConv↓Term : ∀ {t u A B Γ Δ l}
                → ⊢ Γ ≡ Δ
                → Γ ⊢ A ≡ B ^ [ ! , l ]
                → Whnf B
                → Γ ⊢ t [conv↓] u ∷ A ^ l
                → Δ ⊢ t [conv↓] u ∷ B ^ l
  convConv↓Term Γ≡Δ A≡B whnfB (ℕ-ins x) rewrite ℕ≡A A≡B whnfB =
    ℕ-ins (stability~↓! Γ≡Δ x)
  convConv↓Term Γ≡Δ A≡B whnfB (ne x) rewrite U≡A-whnf A≡B whnfB = ne (stability~↓! Γ≡Δ x)
  convConv↓Term Γ≡Δ A≡B whnfB (ne-ins t u x x₁) with ne≡A x A≡B whnfB
  convConv↓Term Γ≡Δ A≡B whnfB (ne-ins t u x x₁) | B , neB , PE.refl =
    ne-ins (stabilityTerm Γ≡Δ (conv t A≡B)) (stabilityTerm Γ≡Δ (conv u A≡B))
           neB (stability~↓! Γ≡Δ x₁)
  convConv↓Term Γ≡Δ A≡B whnfB (zero-refl x) rewrite ℕ≡A A≡B whnfB =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  zero-refl ⊢Δ
  convConv↓Term Γ≡Δ A≡B whnfB (suc-cong x) rewrite ℕ≡A A≡B whnfB =
    suc-cong (stabilityConv↑Term Γ≡Δ x)
  convConv↓Term Γ≡Δ A≡B whnfB (η-eq l< l<' x x₁ x₂ y y₁ x₃) with Π≡A A≡B whnfB
  convConv↓Term Γ≡Δ A≡B whnfB (η-eq l< l<' x x₁ x₂ y y₁ x₃) | F′ , G′ , PE.refl =
    let F≡F′ , rF≡rF′ , _ , _ , G≡G′ = injectivity A≡B
        ⊢F , ⊢F′ = syntacticEq F≡F′
    in  η-eq l< l<'
             (stability Γ≡Δ ⊢F′) (stabilityTerm Γ≡Δ (conv x₁ A≡B))
             (stabilityTerm Γ≡Δ (conv x₂ A≡B)) y y₁
             (convConv↑Term (Γ≡Δ ∙ F≡F′) G≡G′ x₃)
  convConv↓Term Γ≡Δ A≡B whnfB (U-refl x x₁) rewrite U≡A-whnf A≡B whnfB =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ in U-refl x ⊢Δ
  convConv↓Term Γ≡Δ A≡B whnfB (ℕ-refl x) rewrite U≡A-whnf A≡B whnfB =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ in ℕ-refl ⊢Δ
  convConv↓Term Γ≡Δ A≡B whnfB (Empty-refl x _) rewrite U≡A-whnf A≡B whnfB =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ in Empty-refl x ⊢Δ
  convConv↓Term Γ≡Δ A≡B whnfB (Π-cong lΠ rF lF lG l< l<' x x₁ x₂) rewrite U≡A-whnf A≡B whnfB =
    Π-cong lΠ rF lF lG l< l<' (stability Γ≡Δ x) (stabilityConv↑Term Γ≡Δ x₁) (stabilityConv↑Term (Γ≡Δ ∙ refl x) x₂)
  convConv↓Term Γ≡Δ A≡B whnfB (∃-cong lΠ x x₁ x₂) rewrite U≡A-whnf A≡B whnfB =
    ∃-cong lΠ (stability Γ≡Δ x) (stabilityConv↑Term Γ≡Δ x₁) (stabilityConv↑Term (Γ≡Δ ∙ refl x) x₂)

-- Conversion of algorithmic equality with the same context.
convConvTerm : ∀ {t u A B Γ l}
              → Γ ⊢ t [conv↑] u ∷ A ^ l
              → Γ ⊢ A ≡ B ^ [ ! , l ]
              → Γ ⊢ t [conv↑] u ∷ B ^ l
convConvTerm t<>u A≡B = convConv↑Term (reflConEq (wfEq A≡B)) A≡B t<>u

conv~↑% : ∀ {t u A B Γ l}
              -- → ⊢ Γ ≡ Δ
              → Γ ⊢ t ~ u ↑% A ^ l
              → Γ ⊢ A ≡ B ^ [ % , l ]
              → Γ ⊢ t ~ u ↑% B ^ l
conv~↑% (%~↑ ⊢k ⊢l) e = %~↑ (conv ⊢k e) (conv ⊢l e)
--(stabilityTerm ⊢Γ≡Δ (conv ⊢k e)) (stabilityTerm ⊢Γ≡Δ (conv ⊢l e))

convConvTerm%! : ∀ {t u A B Γ r l}
              → Γ ⊢ t [genconv↑] u ∷ A ^ [ r , l ]
              → Γ ⊢ A ≡ B ^ [ r , l ]
              → Γ ⊢ t [genconv↑] u ∷ B ^ [ r , l ]
convConvTerm%! {r = !} = convConvTerm
convConvTerm%! {r = %} = conv~↑%

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module ShouldBeAppliedToTheDatatypeParameters where

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

mutual

  F : Nat -> Set
  F zero    = Nat
  F (suc n) = Foo (F n)

  data Foo (A : Set) : Set where
    fooI1 : F (suc zero)


text:
record ⊤ : Set where constructor tt
data ⊥ : Set where

open import Agda.Builtin.Size

record Delay (F : Size → Set) (i : Size) : Set where
  coinductive
  field force : {j : Size< i} → F j
open Delay public

data Stream (A : Set) (i : Size) : Set where
 _∷_ : A → Delay (Stream A) i → Stream A i

concat : Stream ⊤ ∞ → Delay (Stream ⊥) ∞
concat (xs ∷ xss) = concat (force xss)

head : Stream ⊥ ∞ → ⊥
head (x ∷ xs) = x

units : ∀ {i} → Stream ⊤ i
units = tt ∷ λ where .force → units

false : ⊥
false = head (force (concat units))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2015-07-01 polarity needs to be computed for abstract defs.
-- See also issue 1599 for the same problem with positivity.

-- {-# OPTIONS -v tc.pos:10 -v tc.polarity:20 #-}

open import Common.Size
open import Common.Prelude

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

abstract
  E : Bool → Size → Set
  E true  i = D i
  E false i = D i

  cast : ∀{i b} → E b i → E b (↑ i)
  cast x = x

-- should succeed


text:
module List.Permutation.Pair.Properties (A : Set) where

open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import List.Permutation.Base.Preorder A
open import List.Permutation.Pair A
open import Data.List
open import Data.Product
open import Relation.Binary.PreorderReasoning ∼-preorder
open import Algebra
open import Algebra.Structures

lemma≈∼ : {xs ys zs : List A} → xs ≈ (ys , zs) → xs ∼ (ys ++ zs)
lemma≈∼ (≈[]l zs) = refl∼
lemma≈∼ (≈[]r ys) rewrite ((proj₂ (IsMonoid.identity (Monoid.isMonoid (monoid A)))) ys) = refl∼
lemma≈∼ (≈xr {ys = ys} xs∼ys,zs') = ∼x /head (lemma++/l {xs = ys} /head) (lemma≈∼ xs∼ys,zs')
lemma≈∼ (≈xl xs∼ys',zs) = ∼x /head /head (lemma≈∼ xs∼ys',zs)

lemma≈ : {xs ys zs ws ys' zs' : List A} → xs ≈ (ys , zs) → ys ∼ ys' → zs ∼ zs' → ws ≈ (ys' , zs') → xs ∼ ws
lemma≈ {xs} {ys} {zs} {ws} {ys'} {zs'} xs∼ys,zs ys∼ys' zs∼zs' ws∼ys',zs'
  =  begin
        xs
        ∼⟨ lemma≈∼ xs∼ys,zs  ⟩
        ys ++ zs
        ∼⟨ lemma++∼ ys∼ys' zs∼zs'  ⟩
        ys' ++ zs'
        ∼⟨ sym∼ (lemma≈∼ ws∼ys',zs')  ⟩
        ws
      ∎

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --allow-unsolved-metas #-}
module _ where

open import Agda.Builtin.Bool

postulate
  P : Set → Set

record R : Set1 where
  constructor con
  field
    A : Set
    B : Set

data D : Set1 where
  con : Set → Set → D

snd : D → Set
snd (con A B) = B

-- Eliminating from an under-applied constructor shouldn't result in a
-- crash.

F : Bool → Set₁
F = {!!}

bar : let x : F true; x = R.con Bool in P (x .R.B)
bar = {!!} -- P (con Bool .R.B)

bar2 : let x : F true; x = D.con Bool in P (snd x)
bar2 = {!!} -- P (snd (con Bool))

-- These still show meta numbers because they refer to blocked
-- typechecking problems.
-- Reify could try harder to look at meta instantiations.
bar3 : let x : F true; x = D.con Bool in P (snd (x x))
bar3 = {!!} -- P (snd _23)

bar4 : let x : F true; x = (x : Bool) → Bool in P (x true)
bar4 = {!!} -- P _32

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
{-# OPTIONS --without-K --erased-cubical --no-import-sorts #-}

module Soundness where

open import Prelude

open import Instruments
open import MakeTracks using (makeTrackList)
open import Motif using (motif; levels)
open import SUtil

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

macro
  getDef : Name → Term → TC ⊤
  getDef n h = do
    d ← getDefinition n
    t ← quoteTC d
    unify h t

record Line : Type where
  constructor line
  field
    lhs : List Name
    rhs : List Name
open Line

Proof : Type
Proof = List Line

-- Get only visible constructor names
getNamesP : List (Arg Pattern) → List Name
getNamesP []       = []
getNamesP (arg (arg-info v m)         (Pattern.dot t) ∷ ps)     = getNamesP ps
getNamesP (arg (arg-info v m)         (Pattern.var x₁) ∷ ps)    = getNamesP ps
getNamesP (arg (arg-info v m)         (Pattern.lit l) ∷ ps)     = getNamesP ps
getNamesP (arg (arg-info v m)         (Pattern.proj f) ∷ ps)    = getNamesP ps
getNamesP (arg (arg-info v m)         (Pattern.absurd x₁) ∷ ps) = getNamesP ps
getNamesP (arg (arg-info hidden m)    (Pattern.con n _) ∷ ps)   = getNamesP ps
getNamesP (arg (arg-info instance′ m) (Pattern.con n _) ∷ ps)   = getNamesP ps
getNamesP (arg (arg-info visible m)   (Pattern.con n _) ∷ ps)   = n ∷ getNamesP ps

{-# TERMINATING #-}
getNamesT  : Term → List Name
getNamesAT : Arg Term → List Name

getNamesT (con n args)      = n ∷ concatMap getNamesAT args
getNamesT (def n args)      = n ∷ concatMap getNamesAT args
getNamesT (var x₁ args)     = concatMap getNamesAT args
getNamesT (pat-lam cs args) = concatMap getNamesAT args
getNamesT (lam v t)         = []
getNamesT (pi a b)          = []
getNamesT (agda-sort s)     = []
getNamesT (lit l)           = []
getNamesT (meta x₁ x₂)      = []
getNamesT unknown           = []

getNamesAT (arg i t) = getNamesT t

getNamesC : Clause → Line
getNamesC (Clause.clause tel ps t)      = line (getNamesP ps) (getNamesT t)
getNamesC (Clause.absurd-clause tel ps) = line (getNamesP ps) []

getNamesD : Definition → List Line
getNamesD (function cs)       = map getNamesC cs
getNamesD (data-type pars cs) = []
getNamesD (record-type c fs)  = []
getNamesD (data-cons d)       = []
getNamesD axiom               = []
getNamesD prim-fun            = []

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

data TopLevel : Type where
  s↑   : TopLevel
  s↓   : TopLevel
  sc↑  : TopLevel
  sc↓  : TopLevel
  sct↑ : TopLevel
  sct↓ : TopLevel

topLevelName : TopLevel → Name
topLevelName s↑ = quote soundness~↑
topLevelName s↓ = quote soundness~↓
topLevelName sc↑ = quote soundnessConv↑
topLevelName sc↓ = quote soundnessConv↓
topLevelName sct↑ = quote soundnessConv↑Term
topLevelName sct↓ = quote soundnessConv↓Term

isTopLevel : Name → Maybe TopLevel
isTopLevel n =
  if      n == quote soundness~↑ then just s↑
  else if n == quote soundness~↓ then just s↓
  else if n == quote soundnessConv↑ then just sc↑
  else if n == quote soundnessConv↓ then just sc↓
  else if n == quote soundnessConv↑Term then just sct↑
  else if n == quote soundnessConv↓Term then just sct↓
  else nothing

topLevelDef : TopLevel → Definition
topLevelDef s↑   = getDef soundness~↑
topLevelDef s↓   = getDef soundness~↓
topLevelDef sc↑  = getDef soundnessConv↑
topLevelDef sc↓  = getDef soundnessConv↓
topLevelDef sct↑ = getDef soundnessConv↑Term
topLevelDef sct↓ = getDef soundnessConv↓Term

topLevelProof : TopLevel → Proof
topLevelProof = getNamesD ∘ topLevelDef

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

-- Number of tracks to create
tracks : ℕ
tracks = 4

{-# TERMINATING #-}
-- First argument n is current level (0 is bottom level; no recursive calls allowed)
-- Second argument m is exponent for doubling speed (2^m)
proof→notes : ℕ → ℕ → TopLevel → List (List Note)
line→notes  : ℕ → ℕ → Line → List (List Note)
names→notes : ℕ → ℕ → List Name → List (List Note)

-- starts with proof name
proof→notes n m t =
  zipFull (2ⁿSpeed m (motif (topLevelName t)) ∷ [])
  (concatMap (line→notes n m) (topLevelProof t))

-- just use rhs for now
line→notes n m (line lhs rhs) = names→notes n m rhs

names→notes _    m []         = [] ∷ []
names→notes zero m ns@(_ ∷ _) = 2ⁿSpeed m (concatMap motif ns) ∷ []
names→notes (suc k) m (n ∷ ns) with isTopLevel n
... | just t  = proof→notes k (suc m) t ++ names→notes (suc k) m ns
... | nothing = (2ⁿSpeed m (motif n) ∷ []) ++ names→notes (suc k) m ns

proof→notesTop : ℕ → TopLevel → List (List Note)
proof→notesTop level = proof→notes level 0

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

instruments : Vec InstrumentNumber-1 maxChannels
instruments =
  drawbarOrgan ∷ -- 1
  piano ∷ -- 2
  electricPiano1 ∷ -- 3
  churchOrgan ∷ -- 4
  piano ∷ -- 5
  piano ∷ -- 6
  piano ∷ -- 7
  piano ∷ -- 8
  piano ∷ -- 9
  drums ∷ -- 10 (percussion)
  piano ∷ -- 11
  piano ∷ -- 12
  piano ∷ -- 13
  piano ∷ -- 14
  piano ∷ -- 15
  piano ∷ -- 16
  []

music : Vec (List Note) tracks
music = foldIntoVector (proof→notesTop levels s↑)

tempo : ℕ
tempo = 160

soundTracks : List MidiTrack
soundTracks = makeTrackList instruments tempo music

max_stars_repo_name: halfaya/Music

max_issues_repo_name: halfaya/Music

max_forks_repo_name: halfaya/Music


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

------------------------------------------------------------------------
-- A terminating parser data type and the accompanying interpreter
------------------------------------------------------------------------

-- This code is based on "Parallel Parsing Processes" by Koen
-- Claessen.

module Parallel where

open import Parallel.Index

open import Data.Product renaming (_,_ to pair)
open import Data.Bool
open import Data.Nat
open import Data.Product.Record using (_,_)
import Data.List as List
open List using (List; []; _∷_; _++_)
import Data.Vec as Vec
open Vec using (Vec; []; _∷_) renaming (_++_ to _<+>_)
open import Category.Monad.State
open import Data.Function
open import Data.Maybe
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl)

------------------------------------------------------------------------
-- Parser monad

P : Set -> (Set -> Set)
P tok = StateT (List tok) List

------------------------------------------------------------------------
-- Basic parsers (no CPS)

private
 module Base where

  -- returnPlus below takes a _vector_ of immediate results, since
  -- otherwise the returnPlus/returnPlus case of _∣_ would not type
  -- check. (Its type would have to be changed.)
  --
  -- (The vector could just as well have been a list, if it were not
  -- for the unused module IncorrectBind below. However, documenting
  -- that this list is never empty is not a bad thing, and does not
  -- cost much.)

  codata Parser (tok r : Set) : Index -> Set where
    symbolBind : forall {i : tok -> Index} ->
                 ((c : tok) -> Parser tok r (i c)) -> Parser tok r 0I
    fail       : Parser tok r 0I
    returnPlus : forall {e d n} ->
                 Vec r (suc n) -> Parser tok r (e , d) ->
                 Parser tok r (true , suc d)

  -- Note that the type of this return function is not suitable if you
  -- want to state the monad laws (since (true , 1) is not a zero in
  -- the monoid which is used here). The return function defined below
  -- has a more suitable type, though.

  return : forall {tok r} -> r -> Parser tok r (true , 1)
  return x = returnPlus (Vec.[_] x) fail

  cast : forall {tok i₁ i₂ r} ->
         i₁ ≡ i₂ -> Parser tok r i₁ -> Parser tok r i₂
  cast refl p = p

  infixl 0 _∣_

  _∣_ : forall {tok r i₁ i₂} ->
        Parser tok r i₁ -> Parser tok r i₂ -> Parser tok r (i₁ ∣I i₂)
  fail              ∣ p₂                ~ p₂
  returnPlus xs p₁  ∣ fail              ~ returnPlus xs p₁
  symbolBind f₁     ∣ fail              ~ symbolBind f₁
  symbolBind f₁     ∣ symbolBind f₂     ~ symbolBind (\c -> f₁ c ∣ f₂ c)
  symbolBind f₁     ∣ returnPlus xs p₂  ~ returnPlus xs (symbolBind f₁ ∣ p₂)
  returnPlus xs p₁  ∣ symbolBind f₂     ~ returnPlus xs (symbolBind f₂ ∣ p₁)
  returnPlus xs₁ p₁ ∣ returnPlus xs₂ p₂ ~ returnPlus (xs₁ <+> xs₂) (p₁ ∣ p₂)

  -- parse is structurally recursive over the following lexicographic
  -- measure:
  --
  -- ⑴ The input string.
  -- ⑵ The Distance index.

  parse : forall {tok r e d} ->
          Parser tok r (e , d) -> P tok r
  parse (symbolBind f)    (c ∷ s) = parse (f c) s
  parse (symbolBind f)    []      = []
  parse fail              _       = []
  parse (returnPlus xs p) s       =
    List.map (\x -> pair x s) (Vec.toList xs) ++ parse p s

  -- It may be interesting to note that it is hard to define bind
  -- directly. Note that the module Incorrect is not used for
  -- anything; bind is defined further down using CPS.

  private
   module IncorrectBind where

    -- choice ≈ foldr₁ _∣_.

    choice : forall {tok r i n} ->
             Vec (Parser tok r i) (suc n) -> Parser tok r i
    choice {i = i} =
      Vec.foldr₁ (\p₁ p₂ -> cast (∣-idempotent i) (p₁ ∣ p₂))
      where open IndexSemiring

    -- This function is used to state the type of bind.

    bind-index : forall {tok r i} ->
                 Parser tok r i -> Index -> Index
    bind-index (symbolBind f)    _ = 0I
    bind-index fail              _ = 0I
    bind-index (returnPlus xs p) i = i

    open IndexSemiring

    bind-index-lemma : forall {tok r i₁} (p : Parser tok r i₁) i₂ ->
                       i₂ ∣I bind-index p i₂ ≡ i₂
    bind-index-lemma (symbolBind f)    i = proj₂ +-identity i
    bind-index-lemma fail              i = proj₂ +-identity i
    bind-index-lemma (returnPlus xs p) i = ∣-idempotent i

    -- Note that bind has a non-trivial type. This is not a
    -- fundamental problem, though. The big problem is that bind is
    -- not productive (in general). The recursive call p >>= g in the
    -- last line is not guarded if, for instance, g = const fail, in
    -- which case we have (ignoring some casts)
    --
    --   returnPlus xs p >>= g  =  p >>= g.
    --
    -- If furthermore p = returnPlus xs p, then we have a real
    -- problem.

    _>>=_ : forall {tok r₁ r₂ i₁ i₂} ->
            (p₁ : Parser tok r₁ i₁) -> (r₁ -> Parser tok r₂ i₂) ->
            Parser tok r₂ (bind-index p₁ i₂)
    symbolBind f    >>= g ~ symbolBind (\c -> f c >>= g)
    fail            >>= g ~ fail
    returnPlus xs p >>= g ~ cast (bind-index-lemma p _)
                                 (choice (Vec.map g xs) ∣ p >>= g)

------------------------------------------------------------------------
-- CPS transformation

-- The code below manually applies the continuation-passing monad
-- transformer to the Base parser above to improve the efficiency of
-- left-nested uses of bind. (And, in light of Base.Incorrect._>>=_,
-- to enable a well-founded definition of bind.)

data Parser (tok : Set) (i : Index) (r : Set) : Set1 where
  parser : (forall {i' r'} ->
            (r -> Base.Parser tok r' i') ->
            Base.Parser tok r' (i ·I i')) ->
           Parser tok i r

private

  unP : forall {tok r i r' i'} ->
        Parser tok i r ->
        (r -> Base.Parser tok r' i') ->
        Base.Parser tok r' (i ·I i')
  unP (parser p) = p

symbol : forall {tok} -> Parser tok 0I tok
symbol = parser Base.symbolBind

fail : forall {tok r} -> Parser tok 0I r
fail = parser \k -> Base.fail

-- A problematic variant of fail. See Parallel.Lib.

problematic : forall {tok r} -> r -> Parser tok 0I r
problematic x = parser (\k -> helper (k x))
  where
  helper : forall {tok r' i'} ->
           Base.Parser tok r' i' -> Base.Parser tok r' 0I
  helper (Base.symbolBind _)   = Base.fail
  helper Base.fail             = Base.fail
  helper (Base.returnPlus _ _) = Base.fail

return : forall {tok r} -> r -> Parser tok 1I r
return x = parser \k -> k x

-- Note that _>>=_ cannot easily be given a dependent type (where the
-- second argument has type (x : r₁) -> Parser tok r₂ (i₂ x)). What
-- would the type of the result of _>>=_ be? The type would depend on
-- the input string, which is not an argument to _>>=_.
--
-- Note also that the variant _!>>=_ from Parser/RecursiveDescent.Coinductive
-- cannot (?) be implemented, since the continuation given to p cannot
-- be dependently typed.

infixl 1 _>>=_

_>>=_ : forall {tok r₁ r₂ i₁ i₂} ->
        Parser tok i₁ r₁ -> (r₁ -> Parser tok i₂ r₂) ->
        Parser tok (i₁ ·I i₂) r₂
_>>=_ {i₁ = i₁} {i₂} (parser p) f = parser
  \{i₃} k -> Base.cast (sym $ *-assoc i₁ i₂ i₃)
                       (p \x -> unP (f x) k)
  where open IndexSemiring

infixl 0 _∣_

_∣_ : forall {tok r i₁ i₂} ->
      Parser tok i₁         r ->
      Parser tok i₂         r ->
      Parser tok (i₁ ∣I i₂) r
_∣_ {i₁ = i₁} {i₂ = i₂} (parser p₁) (parser p₂) =
  parser \{i₃} k ->
    Base.cast (sym $ proj₂ distrib i₃ i₁ i₂)
              (Base._∣_ (p₁ k) (p₂ k))
  where open IndexSemiring

-- Since _>>=_ has a non-dependent type it is hard to define sat
-- without using the underlying parsers in Base, and hence sat is
-- provided here.

sat : forall {tok r} ->
      (tok -> Maybe r) -> Parser tok 0I r
sat {tok} {r} p = parser \k -> Base.symbolBind (\c -> ok k (p c))
  where
  okIndex : Index -> Maybe r -> Index
  okIndex i' nothing  = 0I
  okIndex i' (just _) = i'

  ok : forall {r' i'} ->
       (r -> Base.Parser tok r' i') ->
       (x : Maybe r) -> Base.Parser tok r' (okIndex i' x)
  ok k nothing  = Base.fail
  ok k (just x) = k x

parse : forall {tok r i} ->
        Parser tok i r -> P tok r
parse (parser p) = Base.parse (p Base.return)

-- A variant which only returns parses which leave no remaining input.

parse-complete : forall {tok r i} ->
                 Parser tok i r -> List tok -> List r
parse-complete p s =
  List.map proj₁ (List.filter (List.null ∘ proj₂) (parse p s))

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --no-qualified-instances #-}

module NoQualifiedInstances-AnonymousInstance where

postulate
  A : Set
  f : {{A}} → A

postulate instance _ : A

test : A
test = f


text:
open import Structure.Setoid
open import Structure.Category
open import Type

module Structure.Category.Monoid
  {ℓₒ ℓₘ ℓₑ}
  {Obj : Type{ℓₒ}}
  {Morphism : Obj → Obj → Type{ℓₘ}}
  ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}(Morphism x y) ⦄
  (cat : Category(Morphism))
  where

open import Logic.Predicate
open import Structure.Categorical.Properties
open import Structure.Operator.Monoid
open import Structure.Operator.Properties

open Category(cat)

-- A monoid constructed from a category for a specific object.
monoid : ∀{x} → Monoid(_∘_ {x = x})
Monoid.binary-operator monoid = binaryOperator
Associativity.proof (Monoid.associativity monoid) = Morphism.associativity(_∘_)
∃.witness (Monoid.identity-existence monoid) = id
Identityₗ.proof (Identity.left  (∃.proof (Monoid.identity-existence monoid))) = Morphism.identityₗ(_∘_)(id)
Identityᵣ.proof (Identity.right (∃.proof (Monoid.identity-existence monoid))) = Morphism.identityᵣ(_∘_)(id)


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

open import lib.Basics
open import lib.NConnected
open import lib.types.Bool
open import lib.types.Lift
open import lib.types.Nat
open import lib.types.Pointed
open import lib.types.TLevel
open import lib.types.Suspension

module lib.types.IteratedSuspension where

⊙Susp^ : ∀ {i} (n : ℕ) → Ptd i → Ptd i
⊙Susp^ O X = X
⊙Susp^ (S n) X = ⊙Susp (⊙Susp^ n X)

⊙Susp^-conn : ∀ {i} (n : ℕ) {X : Ptd i} {m : ℕ₋₂}
  → is-connected m (fst X) → is-connected (⟨ n ⟩₋₂ +2+ m) (fst (⊙Susp^ n X))
⊙Susp^-conn O cX = cX
⊙Susp^-conn (S n) cX = Susp-conn (⊙Susp^-conn n cX)

⊙Susp^-+ : ∀ {i} (m n : ℕ) {X : Ptd i}
  → ⊙Susp^ m (⊙Susp^ n X) == ⊙Susp^ (m + n) X
⊙Susp^-+ O n = idp
⊙Susp^-+ (S m) n = ap ⊙Susp (⊙Susp^-+ m n)

⊙susp^-fmap : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → fst (X ⊙→ Y) → fst (⊙Susp^ n X ⊙→ ⊙Susp^ n Y)
⊙susp^-fmap O f = f
⊙susp^-fmap (S n) f = ⊙susp-fmap (⊙susp^-fmap n f)

⊙susp^-fmap-idf : ∀ {i} (n : ℕ) (X : Ptd i)
  → ⊙susp^-fmap n (⊙idf X) == ⊙idf (⊙Susp^ n X)
⊙susp^-fmap-idf O X = idp
⊙susp^-fmap-idf (S n) X =
  ap ⊙susp-fmap (⊙susp^-fmap-idf n X) ∙ ⊙susp-fmap-idf (⊙Susp^ n X)

⊙susp^-fmap-cst : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → ⊙susp^-fmap n (⊙cst {X = X} {Y = Y}) == ⊙cst
⊙susp^-fmap-cst O = idp
⊙susp^-fmap-cst (S n) = ap ⊙susp-fmap (⊙susp^-fmap-cst n)
                           ∙ (⊙susp-fmap-cst {X = ⊙Susp^ n _})

⊙susp^-fmap-∘ : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
  → ⊙susp^-fmap n (g ⊙∘ f) == ⊙susp^-fmap n g ⊙∘ ⊙susp^-fmap n f
⊙susp^-fmap-∘ O g f = idp
⊙susp^-fmap-∘ (S n) g f =
  ap ⊙susp-fmap (⊙susp^-fmap-∘ n g f)
  ∙ ⊙susp-fmap-∘ (⊙susp^-fmap n g) (⊙susp^-fmap n f)

⊙Sphere : (n : ℕ) → Ptd₀
⊙Sphere n = ⊙Susp^ n ⊙Bool

Sphere : (n : ℕ) → Type₀
Sphere n = fst (⊙Sphere n)

-- favonia: [S¹] has its own elim rules in Circle.agda.
⊙S⁰ = ⊙Sphere 0
⊙S¹ = ⊙Sphere 1
⊙S² = ⊙Sphere 2
⊙S³ = ⊙Sphere 3
S⁰ = Sphere 0
S¹ = Sphere 1
S² = Sphere 2
S³ = Sphere 3

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
{-# OPTIONS --without-K #-}
module HoTT.Exercises.Chapter2 where

open import HoTT.Base

module Exercise1 {i} {A : 𝒰 i} where
  module _ {x y z : A} (p : x == y) (q : y == z) where
    -- Induction over p
    _∙₁_ : x == z
    _∙₁_ = =-ind D d p z q where
      D : (x y : A) → x == y → 𝒰 i
      D x y p = (z : A) → (q : y == z) → x == z
      d : (x : A) → D x x refl
      d x z q = q

    -- Induction over q
    _∙₂_ : x == z
    _∙₂_ = =-ind D d q x p where
      D : (y z : A) → y == z → 𝒰 i
      D y z q = (x : A) → (p : x == y) → x == z
      d : (y : A) → D y y refl
      d y x p = p

    -- Induction over p then q
    _∙₃_ : x == z
    _∙₃_ = =-ind D d p z q where
      E : (x z : A) → (q : x == z) → 𝒰 i
      E x z q = x == z
      e : (x : A) → E x x refl
      e x = refl
      D : (x y : A) → x == y → 𝒰 i
      D x y p = (z : A) → (q : y == z) → x == z
      d : (x : A) → D x x refl
      d x z q = =-ind E e q

  module _ {x y z : A} (p : x == y) (q : y == z) where
    prop₁₌₂ : p ∙₁ q == p ∙₂ q
    prop₁₌₂ = =-ind D d p z q where
      E : (y z : A) → y == z → 𝒰 i
      E y z q = refl ∙₁ q == refl ∙₂ q
      e : (y : A) → E y y refl
      e y = refl
      D : (x y : A) → x == y → 𝒰 i
      D x y p = (z : A) → (q : y == z) → p ∙₁ q == p ∙₂ q
      d : (x : A) → D x x refl
      d x z q = =-ind E e q

    prop₂₌₃ : p ∙₂ q == p ∙₃ q
    prop₂₌₃ = =-ind D d p z q where
      E : (y z : A) → y == z → 𝒰 i
      E y z q = refl ∙₂ q == refl ∙₃ q
      e : (y : A) → E y y refl
      e y = refl
      D : (x y : A) → x == y → 𝒰 i
      D x y p = (z : A) → (q : y == z) → p ∙₂ q == p ∙₃ q
      d : (x : A) → D x x refl
      d x z q = =-ind E e q

    prop₁₌₃ : p ∙₁ q == p ∙₃ q
    prop₁₌₃ = =-ind D d p z q where
      E : (y z : A) → y == z → 𝒰 i
      E y z q = refl ∙₁ q == refl ∙₃ q
      e : (y : A) → E y y refl
      e y = refl
      D : (x y : A) → x == y → 𝒰 i
      D x y p = (z : A) → (q : y == z) → p ∙₁ q == p ∙₃ q
      d : (x : A) → D x x refl
      d x z q = =-ind E e q

module Exercise2 {i} {A : 𝒰 i} {x y z : A} {p : x == y} {q : y == z} where
  open Exercise1

  _ : prop₁₌₂ p q ∙ prop₂₌₃ p q == prop₁₌₃ p q
  _ = =-ind D d p z q where
    E : (y z : A) → y == z → 𝒰 i
    E y z q = prop₁₌₂ refl q ∙ prop₂₌₃ refl q == prop₁₌₃ refl q
    e : (y : A) → E y y refl
    e y = refl
    D : (x y : A) → x == y → 𝒰 i
    D x y p = (z : A) → (q : y == z) → prop₁₌₂ p q ∙ prop₂₌₃ p q == prop₁₌₃ p q
    d : (x : A) → D x x refl
    d x z q = =-ind E e q

module Exercise3 {i} {A : 𝒰 i} where
  open Exercise1 using (_∙₁_)

  -- Induction over q then p
  _∙₄_ : {x y z : A} → x == y → y == z → x == z
  _∙₄_ {x} {y} {z} p q = =-ind D d q x p where
    E : (x y : A) → (p : x == y) → 𝒰 i
    E x y _ = x == y
    e : (x : A) → E x x refl
    e x = refl
    D : (y z : A) → y == z → 𝒰 i
    D y z q = (x : A) → (p : x == y) → x == z
    d : (y : A) → D y y refl
    d y x p = =-ind E e p

  prop₁₌₄ : {x y z : A} (p : x == y) (q : y == z) → p ∙₁ q == p ∙₄ q
  prop₁₌₄ {x} {y} {z} p q = =-ind D d p z q where
    E : (y z : A) → y == z → 𝒰 i
    E y z q = refl ∙₁ q == refl ∙₄ q
    e : (y : A) → E y y refl
    e y = refl
    D : (x y : A) → x == y → 𝒰 i
    D x y p = (z : A) → (q : y == z) → p ∙₁ q == p ∙₄ q
    d : (x : A) → D x x refl
    d x z q = =-ind E e q

module Exercise4 {i} (A : 𝒰 i) where
  n-path : ℕ → 𝒰 i
  n-path = ℕ-rec A (λ n P → Σ[ x ∶ P ] (Σ[ y ∶ P ] (x == y)))

module Exercise5 {i} {A B : 𝒰 i} {x y : A} {p : x == y} {f : A → B} where
  open import HoTT.Identity
  open import HoTT.Equivalence

  _ : f x == f y ≃ transport _ p (f x) == f y
  _ = g , qinv→isequiv (h , η , ε)
    where
    -- 2.3.6
    g : f x == f y → transport _ p (f x) == f y
    g = transportconst p (f x) ∙_
    -- 2.3.7
    h : transport _ p (f x) == f y → f x == f y
    h = transportconst p (f x) ⁻¹ ∙_
    η : (h ∘ g) ~ id
    η q = assoc ∙ (invₗ ∙ᵣ q ∙ unitₗ ⁻¹)
    ε : (g ∘ h) ~ id
    ε q = assoc ∙ (invᵣ ∙ᵣ q ∙ unitₗ ⁻¹)

module Exercise6 {i} {A : 𝒰 i} {x y z : A} {p : x == y} where
  open import HoTT.Equivalence
  open import HoTT.Identity

  _ : y == z ≃ x == z
  _ = f , qinv→isequiv (g , η , ε)
    where
    f = p ∙_
    g = p ⁻¹ ∙_
    η : g ∘ f ~ id
    η q = assoc ∙ (invₗ ∙ᵣ q ∙ unitₗ ⁻¹)
    ε : f ∘ g ~ id
    ε q = assoc ∙ (invᵣ ∙ᵣ q ∙ unitₗ ⁻¹)

module Exercise7 {i j k l} {A : 𝒰 i} {A' : 𝒰 j} {B : A → 𝒰 k} {B' : A' → 𝒰 l}
                 {g : A → A'} {h : {x : A} → B x → B' (g x)} where
  open import HoTT.Identity
  open import HoTT.Identity.Sigma

  prop : {x y : Σ A B} (p : pr₁ x == pr₁ y) (q : transport B p (pr₂ x) == (pr₂ y)) →
         ap (λ x → g (pr₁ x) , h (pr₂ x)) (pair⁼ {x = x} {y} (p , q)) ==
         pair⁼ (ap g p , transport-ap B' g p (h (pr₂ x)) ∙ transport-∘ h p (pr₂ x) ∙ ap h q)
  prop {x = _ , _} {_ , _} refl refl = refl

module Exercise8 {i j k l} {A : 𝒰 i} {B : 𝒰 j} {A' : 𝒰 k} {B' : 𝒰 l}
                 {g : A → A'} {h : B → B'} where
  open import HoTT.Identity.Coproduct

  private variable x y : A + B

  f : A + B → A' + B'
  f = +-rec (inl ∘ g) (inr ∘ h)

  ap-gh : (p : x =+ y) → f x =+ f y
  ap-gh {inl _} {inl _} (lift p) = lift (ap g p)
  ap-gh {inl _} {inr _} ()
  ap-gh {inr _} {inl _} ()
  ap-gh {inr _} {inr _} (lift p) = lift (ap h p)

  prop : (p : x =+ y) → ap f (=+-intro p) == =+-intro (ap-gh p)
  prop {inl _} {inl _} (lift refl) = refl
  prop {inl _} {inr _} ()
  prop {inr _} {inl _} ()
  prop {inr _} {inr _} (lift refl) = refl

module Exercise9 {i j k} {A : 𝒰 i} {B : 𝒰 j} where
  open import HoTT.Equivalence
  open import HoTT.Identity.Pi

  prop₁ : {X : 𝒰 k} → (A + B → X) ≃ (A → X) × (B → X)
  prop₁ {X} = f , qinv→isequiv (g , β , α)
    where
    f : (A + B → X) → (A → X) × (B → X)
    f h = h ∘ inl , h ∘ inr
    g : (A → X) × (B → X) → (A + B → X)
    g (h , _) (inl a) = h a
    g (_ , h) (inr b) = h b
    α : f ∘ g ~ id
    α (_ , _) = refl
    β : g ∘ f ~ id
    β _ = funext λ{(inl _) → refl ; (inr _) → refl}

  prop₂ : {P : A + B → 𝒰 k} →
          ((x : A + B) → P x) ≃ ((a : A) → P (inl a)) × ((b : B) → P (inr b))
  prop₂ {P} = f , qinv→isequiv (g , β , α)
    where
    f : ((x : A + B) → P x) → ((a : A) → P (inl a)) × ((b : B) → P (inr b))
    f h = (h ∘ inl) , h ∘ inr
    g : ((a : A) → P (inl a)) × ((b : B) → P (inr b)) → ((x : A + B) → P x)
    g (h , _) (inl a) = h a
    g (_ , h) (inr b) = h b
    α : f ∘ g ~ id
    α (_ , _) = refl
    β : g ∘ f ~ id
    β _ = funext λ{(inl _) → refl ; (inr _) → refl}

module Exercise10 {i j k} {A : 𝒰 i} {B : A → 𝒰 j} {C : Σ A B → 𝒰 k}
  where
  open import HoTT.Equivalence

  _ : Σ[ x ∶ A ] Σ[ y ∶ B x ] C (x , y) ≃ Σ[ p ∶ Σ A B ] C p
  _ = f , qinv→isequiv (g , η , ε)
    where
    f : Σ[ x ∶ A ] Σ[ y ∶ B x ] C (x , y) → Σ[ p ∶ Σ A B ] C p
    f (x , y , z) = (x , y) , z
    g : Σ[ p ∶ Σ A B ] C p → Σ[ x ∶ A ] Σ[ y ∶ B x ] C (x , y)
    g ((x , y) , z) = x , y , z
    η : g ∘ f ~ id
    η (_ , _ , _) = refl
    ε : f ∘ g ~ id
    ε ((_ , _) , _) = refl

import HoTT.Exercises.Chapter2.Exercise11

import HoTT.Exercises.Chapter2.Exercise12

module Exercise13
  where
  open import HoTT.Equivalence
  open import HoTT.Equivalence.Proposition
  open import HoTT.Identity.Pi
  open import HoTT.Identity.Sigma

  not : 𝟐 → 𝟐
  not = 𝟐-rec 1₂ 0₂

  -- There are two possibilities for 𝟐 ≃ 𝟐, id and not. In our
  -- equivalence (𝟐 ≃ 𝟐) ≃ 𝟐, we associate `id` with 0₂, and `not`
  -- with 1₂. For some f : 𝟐 ≃ 𝟐, we have f 0₂ = 0₂ when f is id,
  -- and f 0₂ = 1₂ when f is not, so we can use f 0₂ in the forward
  -- direction.
  _ : (𝟐 ≃ 𝟐) ≃ 𝟐
  _ = to , qinv→isequiv (from , β , α)
    where
    to : 𝟐 ≃ 𝟐 → 𝟐
    to (f , _) = f 0₂
    from : 𝟐 → 𝟐 ≃ 𝟐
    from 0₂ = id , qinv→isequiv (id , (λ _ → refl) , λ _ → refl)
    from 1₂ = not , qinv→isequiv (not , 𝟐-ind _ refl refl , 𝟐-ind _ refl refl)
    -- The first homotopy is easy, we just do 𝟐-induction on the
    -- input to determine whether we have `id` or `not`. Once we
    -- know that, it is just a matter of showing 0₂ = 0₂ or 1₂ = 1₂,
    -- both of which are true by reflection.
    α : to ∘ from ~ id
    α = 𝟐-ind _ refl refl
    -- The second homotopy is much trickier since we have to show
    -- that these two complex structures are the same. The approach
    -- we use is to induct on the four possibilities for f 0₂ and
    -- f 1₂ (0₂ 0₂, 0₂ 1₂, 1₂ 0₂, or 1₂ 1₂). In the induction goals,
    -- we require proofs that the boolean we induct on is equal
    -- to f 0₂ or f 1₂ respectively. These proofs can be used
    -- directly for the case where f = id or f = not. The other two
    -- cases are impossible unless 0₂ = 1₂, and we can use the
    -- proofs together with the equivalence inverse function and
    -- homotopy to show the desired behavior of f.
    β : from ∘ to ~ id
    β (f , e) =
      pair⁼ (𝟐-ind (λ x → x == f 0₂ → pr₁ (from x) == f)
        (λ p → 𝟐-ind (λ x → x == f 1₂ → id == f)
          (λ q → funext (𝟐-ind _ p (η 1₂ ⁻¹ ∙ ap g (q ⁻¹ ∙ p) ∙ η 0₂ ∙ q)))
          (λ q → funext (𝟐-ind _ p q))
          (f 1₂) refl)
        (λ p → 𝟐-ind (λ x → x == f 1₂ → not == f)
          (λ q → funext (𝟐-ind _ p q))
          (λ q → funext (𝟐-ind _ p (η 0₂ ⁻¹ ∙ ap g (p ⁻¹ ∙ q) ∙ η 1₂ ∙ q)))
          (f 1₂) refl)
        (f 0₂) refl , isequiv-prop _ _)
      where open qinv (isequiv→qinv e)

module Exercise14 {i} {A : 𝒰 i} {x : A}
  where
  -- In chapter 1 exercise 14, we showed that we couldn't use path
  -- induction to prove (x : A) → (p : x = x) → p = reflₓ since,
  -- given q : x = y, q = reflₓ is not well-typed (reflₓ : x = x,
  -- while q : x = y). However, using the equality reflection rule
  -- we have x ≡ y, so we can say reflₓ : x = y. Therefore, we can
  -- define
  --
  --   C : (x s : A) → x = y → 𝒰
  --   C x y q :≡ q = reflₓ
  --
  --   c : (x : A) → C x x reflₓ
  --   c x :≡ refl {reflₓ}
  --
  -- Using path induction we have ind₌ C c x x p : p = reflₓ. By
  -- applying the equality reflection rule again, we arrive at the
  -- desired definitional equality, p ≡ reflₓ.

module Exercise15 {i j} {A : 𝒰 i} {B : A → 𝒰 j} {x y : A} {p : x == y} {u : B x}
  where
  _ : transport _ p == transport id (ap B p)
  _ = =-ind (λ _ _ p → transport _ p == transport id (ap B p)) (λ _ → refl) p

module Exercise16 {i} {j} {A : 𝒰 i} {B : A → 𝒰 j} (f g : Π A B) where
  open import HoTT.Identity
  open import HoTT.Identity.Sigma
  open import HoTT.Identity.Pi using (funext)
  open import HoTT.Equivalence

  =Π-equiv : f == g ≃ f ~ g
  =Π-equiv = happly , qinv→isequiv (funext' , η , ε)
    where
    -- Define funext' in such a way that funext (happly refl) ≡
    -- funext (λ x. refl) can cancel.
    funext' : {g : Π A B} → f ~ g → f == g
    funext' α = funext α ∙ funext (λ _ → refl) ⁻¹
    η : funext' ∘ happly ~ id
    η refl = invᵣ
    ε : happly ∘ funext' ~ id
    ε α = transport P p (ap happly invᵣ)
      where
      P : Π[ x ∶ A ] Σ[ y ∶ B x ] f x == y → 𝒰 _
      P h = let α = pr₂ ∘ h in happly (funext' α) == α
      -- The trick here is to use funext to simultaneously show
      -- that λ x. (f x , refl) = λ x. (g x , α x). Then, we can
      -- transport a path made by canceling the funext with its
      -- inverse to get the desired equality.
      p : (λ x → f x , refl) == (λ x → g x , α x)
      p = funext λ x → pair⁼ (α x , =-ind (λ _ _ p → transport _ p refl == p) (λ _ → refl) (α x))

module Exercise17 {i} where
  open import HoTT.Equivalence
  open import HoTT.Equivalence.Proposition
  open import HoTT.Identity.Product
  open import HoTT.Identity.Sigma
  open import HoTT.Identity.Universe
  open import HoTT.Identity.Pi

  variable
    A A' B B' : 𝒰 i
    P : A → 𝒰 i
    P' : A' → 𝒰 i

  prop : (_◆_ : 𝒰 i → 𝒰 i → 𝒰 i) → A == A' → B == B' → (A ◆ B) ≃ (A' ◆ B')
  prop {A} {A'} {B} {B'} (_◆_) p q =
    transport (λ{ (A' , B') → A ◆ B ≃ A' ◆ B' })
      (×-pair⁼ {x = A , B} {y = A' , B'} (p , q)) reflₑ

  module _ (e₁ : A ≃ A') (e₂ : B ≃ B')
    where
    open Iso (eqv→iso e₁) renaming (f to f₁ ; g to g₁ ; η to η₁ ; ε to ε₁)
    open Iso (eqv→iso e₂) renaming (f to f₂ ; g to g₂ ; η to η₂ ; ε to ε₂)

    -- (i) Proof without using univalence
    prop-×' : A × B ≃ A' × B'
    prop-×' = let open Iso in iso→eqv λ where
      .f (a , b) → f₁ a , f₂ b
      .g (a' , b') → g₁ a' , g₂ b'
      .η (a , b) → ×-pair⁼ (η₁ a , η₂ b)
      .ε (a' , b') → ×-pair⁼ (ε₁ a' , ε₂ b')

    -- (ii) Proof using univalence (for general operator)
    prop-× = prop _×_ (ua e₁) (ua e₂)

    -- (iii) Proof for non-dependent type formers (→, +)
    prop-→ = prop (λ A B → A → B) (ua e₁) (ua e₂)
    prop-+ = prop _+_ (ua e₁) (ua e₂)

  -- Proof that (i) and (ii) are equal
  propᵢ₌ᵢᵢ : (e₁ : A ≃ A') (e₂ : B ≃ B') → prop-×' e₁ e₂ == prop-× e₁ e₂
  propᵢ₌ᵢᵢ e₁ e₂ = ap² prop-×' (=𝒰-β e₁ ⁻¹) (=𝒰-β e₂ ⁻¹) ∙ lemma
    where
    lemma : prop-×' (idtoeqv (ua e₁)) (idtoeqv (ua e₂)) == prop-× e₁ e₂
    lemma rewrite ua e₁ rewrite ua e₂ =
      pair⁼ (funext (λ{ (a , b) → refl }) , isequiv-prop _ _)

  module _ (e₁ : A ≃ A') (e₂ : (x : A') → transport (λ A' → A' → 𝒰 i) (ua e₁) P x ≃ P' x)
    where
    prop-dep : (_◆_ : (A : 𝒰 i) → (A → 𝒰 i) → 𝒰 i) → (A ◆ P) ≃ (A' ◆ P')
    prop-dep _◆_ = transport (λ{ (A' , P') → A ◆ P ≃ A' ◆ P' })
      (pair⁼ {x = A , P} {y = A' , P'} (ua e₁ , funext (ua ∘ e₂))) reflₑ

    -- (iii) Proof for dependent type formers (Σ, Π)
    prop-Σ = prop-dep Σ
    prop-Π = prop-dep Π

module Exercise18 {i} {A : 𝒰 i} {B : A → 𝒰 i} {f g : Π A B} {H : f ~ g}
                  {x y : A} {p : x == y}
  where
  -- We first induct on p, changing our goal to
  --
  --   ap (transport refl) (H x) ∙ apd g refl = apd f refl ∙ H y
  --
  -- This reduces to
  --
  --   ap id (H x) ∙ refl = refl ∙ H x
  --
  -- Now, we just need one final induction on H x, after which our goal
  -- reduces to refl : refl = refl.
  _ : ap (transport _ p) (H x) ∙ apd g p == apd f p ∙ H y
  _ = =-ind' (λ y p → ap (transport _ p) (H x) ∙ apd g p == apd f p ∙ H y)
    (=-ind' (λ _ Hₓ → ap id Hₓ ∙ refl == refl ∙ Hₓ) refl (H x)) p

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
------------------------------------------------------------------------------
-- Well-founded relation on trees
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Mirror.TreeR where

open import FOTC.Base
open import FOTC.Data.List.WF-Relation.LT-Cons
open import FOTC.Program.Mirror.Type

------------------------------------------------------------------------------
-- Well-founded relation on trees.

-- A well-founded relation for rose trees is the lexicographical order
--
-- (t : ts) < (t' : ts') = t < t' or t ≡ t' and ts < ts'.
--
-- It seems we would not to use the first conjunct in the mirror
-- example.
TreeR : D → D → Set
TreeR t₁ t₂ = ∃[ d ] ∃[ ts₁ ] ∃[ ts₂ ]
                 t₁ ≡ node d ts₁
                 ∧ t₂ ≡ node d ts₂
                 ∧ LTC ts₁ ts₂

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- This file contains several ways to define localisation
-- and proves them all to be equivalent

{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Experiments.LocalisationDefs where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.Transport
open import Cubical.Functions.FunExtEquiv

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Vec
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

open Iso

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

record isMultClosedSubset (R' : CommRing {ℓ}) (S' : ℙ (R' .fst)) : Type ℓ where
 constructor
   multclosedsubset
 field
   containsOne : (R' .snd .CommRingStr.1r) ∈ S'
   multClosed : ∀ {s t} → s ∈ S' → t ∈ S' → (R' .snd .CommRingStr._·_ s t) ∈ S'

module _ (R' : CommRing {ℓ}) (S' : ℙ (R' .fst)) (SMultClosedSubset : isMultClosedSubset R' S') where
 open isMultClosedSubset
 private R = R' .fst
 open CommRingStr (R' .snd)
 open Theory (CommRing→Ring R')

 S = Σ[ s ∈ R ] (s ∈ S')

 -- HIT definition
 data S⁻¹R : Type ℓ where
  _/ₗ_ : R → S → S⁻¹R
  zd : (r₁ r₂ : R) (s s₁ s₂ : S)
     → fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁
     → r₁ /ₗ s₁ ≡ r₂ /ₗ s₂
  trunc : isSet S⁻¹R

 infixr 5 _/ₗ_

 module Elim {ℓ'} {B : S⁻¹R → Type ℓ'}
     (_/*_ : (r : R) (s : S) → B (r /ₗ s))
     (zd* : (r₁ r₂ : R) (s s₁ s₂  : S)
          → (p : fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁)
          → PathP (λ i → B (zd r₁ r₂ s s₁ s₂ p i))  (r₁ /* s₁) (r₂ /* s₂))
     (trunc* : (q : S⁻¹R) → isSet (B q)) where

  f : (q : S⁻¹R) → B q
  f (r /ₗ s) = r /* s
  f (zd r₁ r₂ s s₁ s₂ p i) = zd* r₁ r₂ s s₁ s₂ p i
  f (trunc q₁ q₂ x y i j) = isOfHLevel→isOfHLevelDep 2 trunc*  (f q₁) (f q₂) (cong f x) (cong f y)
                                                      (trunc q₁ q₂ x y) i j

 module ElimProp {ℓ'} {B : S⁻¹R → Type ℓ'} (Bprop : {q : S⁻¹R} → isProp (B q))
                 (_/*_ : (r : R) → (s : S) → B (r /ₗ s)) where

  f : (q : S⁻¹R) → B q
  f = Elim.f _/*_ (λ r₁ r₂ s s₁ s₂ p
    → toPathP (Bprop (transp (λ i → B (zd r₁ r₂ s s₁ s₂ p i)) i0 (r₁ /* s₁))
              (r₂ /* s₂)))
             λ q → isProp→isSet Bprop

 module Rec {ℓ'} {B : Type ℓ'} (BType : isSet B)
     (_/*_ : R → S → B)
     (zd* : (r₁ r₂ : R) (s s₁ s₂ : S)
          → (p : fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁)
          → r₁ /* s₁ ≡ r₂ /* s₂)
     where

  f : S⁻¹R → B
  f = Elim.f _/*_ zd* (λ _ → BType)

 -- approach using set quotients
 _≈_ : R × S → R × S → Type ℓ
 (r₁ , s₁) ≈ (r₂ , s₂) = ∃[ s ∈ S ] (fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁)

 S⁻¹R/ = (R × S) / _≈_

 -- proving equivalence of the two types
 φ : S⁻¹R/ → S⁻¹R
 φ = SQ.rec trunc (λ (r , s) → r /ₗ s) β
  where
  α : ((r₁ , s₁) (r₂ , s₂) : R × S) → Σ[ s ∈ S ] (fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁)
    → r₁ /ₗ s₁ ≡ r₂ /ₗ s₂
  α _ _ (s , p) = zd _ _ s _ _ p

  β : ((r₁ , s₁) (r₂ , s₂) : R × S) → ∃[ s ∈ S ] (fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁)
    → r₁ /ₗ s₁ ≡ r₂ /ₗ s₂
  β _ _ = PT.rec (trunc _ _) (α _ _)

 ψ : S⁻¹R → S⁻¹R/
 ψ (r /ₗ s) = [ r , s ]
 ψ (zd r₁ r₂ s s₁ s₂ p i) = eq/ (r₁ , s₁) (r₂ , s₂) ∣ s , p ∣ i
 ψ (trunc x y p q i j) = squash/ (ψ x) (ψ y) (cong ψ p) (cong ψ q) i j

 η : section φ ψ
 η = ElimProp.f (trunc _ _) λ _ _ → refl

 ε : retract φ ψ
 ε = elimProp (λ _ → squash/ _ _) λ _ → refl

 S⁻¹R/≃S⁻¹R : S⁻¹R/ ≃ S⁻¹R
 S⁻¹R/≃S⁻¹R = isoToEquiv (iso φ ψ η ε)

 -- Set quotients but with Σ, this is the type used in Algebra.Localisation.Base
 -- as this is easiest to use
 _≈'_ : R × S → R × S → Type ℓ
 (r₁ , s₁) ≈' (r₂ , s₂) = Σ[ s ∈ S ] (fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁)

 S⁻¹R/' = (R × S) / _≈'_

 S⁻¹R/'≃S⁻¹R/ : S⁻¹R/' ≃ S⁻¹R/
 S⁻¹R/'≃S⁻¹R/ = SQ.truncRelEquiv

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Andreas, 2018-06-09, issue #2513, parsing attributes

postulate
  fail : ∀ @0 A → A → A

-- Should fail.


text:
-- Andreas, 2018-10-27, issue #3327
--
-- Test that {-# NO_UNIVERSE_CHECK #-} pragma only applies to the following definition.

module _ where

-- The following pragma should only apply to the following definition,
-- but due to a bug is actually applying to the rest of the module.

{-# NO_UNIVERSE_CHECK #-}
data ⊥ : Set where

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

-- This passes only with {-# NO_UNIVERSE_CHECK #-}:

record Type : Set where
  constructor inn
  field out : Set
open Type

-- The rest is Hurken's paradox.

⊥′ : Type
⊥′ = inn ((A : Type) → out A)

_⇒_ : (A B : Type) → Type
inn A ⇒ inn B = inn (A → B)

Π : (A : Type) (B : out A → Type) → Type
Π A B = inn ((x : out A) → out (B x))

¬_ : Type → Type
¬ A = A ⇒ ⊥′

P : Type → Type
P A = inn (out A → Type)

U : Type
U = inn ((X : Type) → out ((P (P X) ⇒ X) ⇒ P (P X)))

τ : out (P (P U) ⇒ U)
τ t = λ X f p → t λ x → p (f (x X f))

σ : out (U ⇒ P (P U))
σ s pu = s U (λ t → τ t) pu

Δ : out (P U)
Δ = λ y → ¬ (Π (P U) λ p → σ y p ⇒ p (τ (σ y)))

Ω : out U
Ω X t px = τ (λ p → Π U λ x → σ x p ⇒ p x) X t px

D : Type
D = Π (P U) λ p → σ Ω p ⇒ p (τ (σ Ω))

lem₁ : out (Π (P U) λ p → (Π U λ x → σ x p ⇒ p x) ⇒ p Ω)
lem₁ p H1 = H1 Ω λ x → H1 (τ (σ x))

lem₂ : out (¬ D)
lem₂ d A = lem₁ Δ (λ x H2 H3 → H3 Δ H2 λ p → H3 λ y → p (τ (σ y))) d A

lem₃ : out D
lem₃ p = lem₁ λ y → p (τ (σ y))

loop : out ⊥′
loop = λ A → lem₂ lem₃ A

absurd : ⊥
absurd = loop (inn ⊥)