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

{--

Make a version of this file with plain PI and ℕ as a model

Make another version with PI+NEG+FRAC (meadow style) and ℚ as a model

Keep extending; add imaginary numbers and try ℂ as a model

then add square roots and try algebraic numbers as a model

An orthogonal direction is to try other models that are not numbers: in
particular groupoid-based models like we started in F2.agda and F2a.agda

--}

module HP where

-- Pi as a higher-order inductive type

open import Agda.Prim
open import Data.Empty
open import Data.Unit
open import Data.Unit.Core
open import Data.Maybe hiding (map)
open import Data.Nat renaming (_⊔_ to _⊔ℕ_)
open import Data.Integer hiding (_⊔_)
open import Data.Sum renaming (map to _⊎→_)
open import Data.Product renaming (map to _×→_)
open import Data.List
open import Data.Rational hiding (_≃_)
open import Function renaming (_∘_ to _○_)

infixr 8  _∘_   -- path composition
infix  4  _≡_   -- propositional equality
infix  4  _∼_   -- homotopy between two functions
infix  4  _≃_   -- type of equivalences
infix  2  _∎      -- equational reasoning
infixr 2  _≡⟨_⟩_  -- equational reasoning
infix  2  _∎≃      -- equational reasoning for equivalences
infixr 2  _≃⟨_⟩_   -- equational reasoning for equivalences

------------------------------------------------------------------------------
-- Identity types and path induction principles

-- Our own version of refl that makes 'a' explicit

data _≡_ {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where
  refl : (a : A) → (a ≡ a)

pathInd : ∀ {u ℓ} → {A : Set u} →
          (C : {x y : A} → x ≡ y → Set ℓ) →
          (c : (x : A) → C (refl x)) →
          ({x y : A} (p : x ≡ y) → C p)
pathInd C c (refl x) = c x

basedPathInd : {A : Set} → (a : A) → (C : (x : A) → (a ≡ x) → Set) →
  C a (refl a) → ((x : A) (p : a ≡ x) → C x p)
basedPathInd a C c .a (refl .a) = c

------------------------------------------------------------------------------
-- Ch. 2

-- Lemma 2.1.1

! : ∀ {u} → {A : Set u} {x y : A} → (x ≡ y) → (y ≡ x)
! = pathInd (λ {x} {y} _ → y ≡ x) refl

-- Lemma 2.1.2

_∘_ : ∀ {u} → {A : Set u} → {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_∘_ {u} {A} {x} {y} {z} p q =
  pathInd
    (λ {x} {y} p → ((z : A) → (q : y ≡ z) → (x ≡ z)))
    (λ x z q → pathInd (λ {x} {z} _ → x ≡ z) refl {x} {z} q)
    {x} {y} p z q

-- Lemma 2.1.4

-- p ≡ p ∘ refl

unitTransR : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ p ∘ refl y)
unitTransR {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ p ∘ (refl y))
    (λ x → refl (refl x))
    {x} {y} p

-- p ≡ refl ∘ p

unitTransL : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ refl x ∘ p)
unitTransL {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ (refl x) ∘ p)
    (λ x → refl (refl x))
    {x} {y} p

-- ! p ∘ p ≡ refl

invTransL : {A : Set} {x y : A} → (p : x ≡ y) → (! p ∘ p ≡ refl y)
invTransL {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ! p ∘ p ≡ refl y)
    (λ x → refl (refl x))
    {x} {y} p

-- p ∘ ! p ≡ refl

invTransR : ∀ {ℓ} {A : Set ℓ} {x y : A} → (p : x ≡ y) → (p ∘ ! p ≡ refl x)
invTransR {ℓ} {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ∘ ! p ≡ refl x)
    (λ x → refl (refl x))
    {x} {y} p

-- ! (! p) ≡ p

invId : {A : Set} {x y : A} → (p : x ≡ y) → (! (! p) ≡ p)
invId {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ! (! p) ≡ p)
    (λ x → refl (refl x))
    {x} {y} p

-- p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r

assocP : {A : Set} {x y z w : A} → (p : x ≡ y) → (q : y ≡ z) → (r : z ≡ w) →
         (p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r)
assocP {A} {x} {y} {z} {w} p q r =
  pathInd
    (λ {x} {y} p → (z : A) → (w : A) → (q : y ≡ z) → (r : z ≡ w) →
      p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r)
    (λ x z w q r →
      pathInd
        (λ {x} {z} q → (w : A) → (r : z ≡ w) →
          (refl x) ∘ (q ∘ r) ≡ ((refl x) ∘ q) ∘ r)
        (λ x w r →
          pathInd
            (λ {x} {w} r →
              (refl x) ∘ ((refl x) ∘ r) ≡
              ((refl x) ∘ (refl x)) ∘ r)
            (λ x → (refl (refl x)))
            {x} {w} r)
        {x} {z} q w r)
    {x} {y} p z w q r

-- ! (p ∘ q) ≡ ! q ∘ ! p

invComp : {A : Set} {x y z : A} → (p : x ≡ y) → (q : y ≡ z) →
          ! (p ∘ q) ≡ ! q ∘ ! p
invComp {A} {x} {y} {z} p q =
  pathInd
    (λ {x} {y} p → (z : A) → (q : y ≡ z) → ! (p ∘ q) ≡ ! q ∘ ! p)
    (λ x z q →
      pathInd
        (λ {x} {z} q → ! (refl x ∘ q) ≡ ! q ∘ ! (refl x))
        (λ x → refl (refl x))
        {x} {z} q)
    {x} {y} p z q

-- Introduce equational reasoning syntax to simplify proofs

_≡⟨_⟩_ : ∀ {u} → {A : Set u} (x : A) {y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_ ≡⟨ p ⟩ q = p ∘ q

bydef : ∀ {u} → {A : Set u} {x : A} → (x ≡ x)
bydef {u} {A} {x} = refl x

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

------------------------------------------------------------------------------
-- Functions are functors

-- Lemma 2.2.1
-- computation rule: ap f (refl x) = refl (f x)

ap : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {x y : A} →
     (f : A → B) → (x ≡ y) → (f x ≡ f y)
ap f p =
  pathInd
    (λ {x} {y} _ → f x ≡ f y)
    (λ x → refl (f x))
    p

ap₂ : ∀ {ℓ ℓ' ℓ''} → {A : Set ℓ} {B : Set ℓ'} {C : Set ℓ''}
     {x₁ y₁ : A} {x₂ y₂ : B} →
     (f : A → B → C) → (x₁ ≡ y₁) → (x₂ ≡ y₂) → (f x₁ x₂  ≡ f y₁ y₂)
ap₂ {ℓ} {ℓ'} {ℓ''} {A} {B} {C} {x₁} {y₁} {x₂} {y₂} f p₁ p₂ =
  pathInd -- on p₁
    (λ {x₁} {y₁} p₁ → f x₁ x₂ ≡ f y₁ y₂)
    (λ x →
      pathInd -- on p₂
        (λ {x₂} {y₂} p₂ → f x x₂ ≡ f x y₂)
        (λ y → refl (f x y))
        {x₂} {y₂} p₂)
    {x₁} {y₁} p₁

-- Lemma 2.2.2

-- f (p ∘ q) ≡ f p ∘ f q

apfTrans : ∀ {u} → {A B : Set u} {x y z : A} →
  (f : A → B) → (p : x ≡ y) → (q : y ≡ z) → ap f (p ∘ q) ≡ (ap f p) ∘ (ap f q)
apfTrans {u} {A} {B} {x} {y} {z} f p q =
  pathInd {u}
    (λ {x} {y} p → (z : A) → (q : y ≡ z) →
      ap f (p ∘ q) ≡ (ap f p) ∘ (ap f q))
    (λ x z q →
      pathInd {u}
        (λ {x} {z} q →
          ap f (refl x ∘ q) ≡ (ap f (refl x)) ∘ (ap f q))
        (λ x → refl (refl (f x)))
        {x} {z} q)
    {x} {y} p z q

-- f (! p) ≡ ! (f p)

apfInv : ∀ {u} → {A B : Set u} {x y : A} → (f : A → B) → (p : x ≡ y) →
         ap f (! p) ≡ ! (ap f p)
apfInv f p =
  pathInd
    (λ p → ap f (! p) ≡ ! (ap f p))
    (λ x → refl (ap f (refl x)))
    p

-- g (f p) ≡ (g ○ f) p

apfComp : {A B C : Set} {x y : A} → (f : A → B) → (g : B → C) → (p : x ≡ y) →
          ap g (ap f p) ≡ ap (g ○ f) p
apfComp {A} {B} {C} {x} {y} f g p =
  pathInd
    (λ {x} {y} p → ap g (ap f p) ≡ ap (g ○ f) p)
    (λ x → refl (ap g (ap f (refl x))))
    {x} {y} p

-- id p ≡ p

apfId : {A : Set} {x y : A} → (p : x ≡ y) → ap id p ≡ p
apfId {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ap id p ≡ p)
    (λ x → refl (refl x))
    {x} {y} p

-- Transport

-- Lemma 2.3.1

transport : ∀ {ℓ ℓ'} → {A : Set ℓ} {x y : A} →
  (P : A → Set ℓ') → (p : x ≡ y) → P x → P y
transport {x = x} {y} P p =
  pathInd
    (λ {x'} {y'} _ → (P x' → P y'))
    (λ _ → id)
    {x} {y} p

-- Lemma 2.3.10

transport-f : ∀ {ℓ ℓ' ℓ''} → {A : Set ℓ} {B : Set ℓ'} {x y : A} →
  (f : A → B) → (P : B → Set ℓ'') →
  (p : x ≡ y) → (u : P (f x)) →
  transport (P ○ f) p u ≡ transport P (ap f p) u
transport-f {ℓ} {ℓ'} {ℓ''} {A} {B} {x} {y} f P p u =
  pathInd -- on p
    (λ {x} {y} p → (u : P (f x)) →
      transport (P ○ f) p u ≡ transport P (ap f p) u)
    (λ x u → refl u)
    {x} {y} p u

-- Lemma 2.11.2

transportIdR : {A : Set} {a y z : A} → (p : y ≡ z) → (q : a ≡ y) →
  transport (λ x → a ≡ x) p q ≡ q ∘ p
transportIdR {A} {a} {y} {z} p q =
  pathInd
    (λ {y} {z} p → (q : a ≡ y) → transport (λ x → a ≡ x) p q ≡ q ∘ p)
    (λ y q → transport (λ x → a ≡ x) (refl y) q
               ≡⟨ bydef ⟩
             q
               ≡⟨ unitTransR q ⟩
             q ∘ refl y ∎)
    {y} {z} p q

transportIdL : {A : Set} {a y z : A} → (p : y ≡ z) → (q : y ≡ a) →
  transport (λ x → x ≡ a) p q ≡ ! p ∘ q
transportIdL {A} {a} {y} {z} p q =
  pathInd
    (λ {y} {z} p → (q : y ≡ a) → transport (λ x → x ≡ a) p q ≡ ! p ∘ q)
    (λ y q → transport (λ x → x ≡ a) (refl y) q
               ≡⟨ bydef ⟩
             q
               ≡⟨ unitTransL q ⟩
             ! (refl y) ∘ q ∎)
    {y} {z} p q

transportIdRefl : {A : Set} {y z : A} → (p : y ≡ z) → (q : y ≡ y) →
  transport (λ x → x ≡ x) p q ≡ ! p ∘ q ∘ p
transportIdRefl {A} {y} {z} p q =
  pathInd
    (λ {y} {z} p → (q : y ≡ y) → transport (λ x → x ≡ x) p q ≡ ! p ∘ q ∘ p)
    (λ y q → transport (λ x → x ≡ x) (refl y) q
               ≡⟨ bydef ⟩
             q
               ≡⟨ unitTransR q ⟩
             q ∘ refl y
               ≡⟨ unitTransL (q ∘ refl y) ⟩
             ! (refl y) ∘ q ∘ refl y ∎)
    {y} {z} p q

-- Thm 2.11.3

transportId : {A B : Set} {y z : A} → (f g : A → B) →
  (p : y ≡ z) → (q : f y ≡ g y) →
  transport (λ x → f x ≡ g x) p q ≡ ! (ap f p) ∘ q ∘ (ap g p)
transportId {A} {B} {y} {z} f g p q =
  pathInd
    (λ {y} {z} p → (q : f y ≡ g y) →
      transport (λ x → f x ≡ g x) p q ≡ ! (ap f p) ∘ q ∘ (ap g p))
    (λ y q → q
               ≡⟨ unitTransR q ⟩
             q ∘ refl (g y)
               ≡⟨ unitTransL (q ∘ refl (g y)) ⟩
             refl (f y) ∘ q ∘ refl (g y) ∎)
    {y} {z} p q

-------------------------------------------------------------------------------
-- Homotopies and equivalences

_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
      (f g : (x : A) → P x) → Set (_⊔_ ℓ ℓ')
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x

-- Quasi-inverses

record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (_⊔_ ℓ ℓ') where
  constructor mkqinv
  field
    g : B → A
    α : (f ○ g) ∼ id
    β : (g ○ f) ∼ id

-- Example 2.4.7

idqinv : ∀ {ℓ} → {A : Set ℓ} → qinv {ℓ} {ℓ} {A} {A} id
idqinv = record {
           g = id ;
           α = λ b → refl b ;
           β = λ a → refl a
         }

-- Equivalences

record isequiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (_⊔_ ℓ ℓ') where
  constructor mkisequiv
  field
    g : B → A
    α : (f ○ g) ∼ id
    h : B → A
    β : (h ○ f) ∼ id

equiv₁ : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → qinv f → isequiv f
equiv₁ (mkqinv qg qα qβ) = mkisequiv qg qα qg qβ

equiv₂ : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → isequiv f → qinv f
equiv₂ {f = f} (mkisequiv ig iα ih iβ) =
  record {
    g = ig ;
    α = iα ;
    β = λ x → ig (f x)
                ≡⟨ ! (iβ (ig (f x))) ⟩
              ih (f (ig (f x)))
                ≡⟨ ap ih (iα (f x)) ⟩
              ih (f x)
                ≡⟨ iβ x ⟩
              x ∎
  }

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (_⊔_ ℓ ℓ')
A ≃ B = Σ (A → B) isequiv

id≃ : ∀ {ℓ} {A : Set ℓ} → A ≃ A
id≃ = (id , equiv₁ idqinv)

sym≃ :  ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A ≃ B) → B ≃ A
sym≃ (A→B , equiv) with equiv₂ equiv
... | mkqinv g α β = g , equiv₁ (mkqinv A→B β α)

trans≃ : {A B C : Set} → A ≃ B → B ≃ C → A ≃ C
trans≃ (f , feq) (g , geq) with equiv₂ feq | equiv₂ geq
... | mkqinv ff fα fβ | mkqinv gg gα gβ =
  (g ○ f , equiv₁ (mkqinv
                    (ff ○ gg)
                    (λ c → g (f (ff (gg c)))
                             ≡⟨ ap g (fα (gg c)) ⟩
                           g (gg c)
                             ≡⟨ gα c ⟩
                           c ∎)
                    (λ a → ff (gg (g (f a)))
                             ≡⟨ ap ff (gβ (f a)) ⟩
                           ff (f a)
                             ≡⟨ fβ a ⟩
                           a ∎)))

-- identities are equivalences

idtoeqv : {A B : Set} → (A ≡ B) → (A ≃ B)
idtoeqv {A} {B} p =
  pathInd
    (λ {A'} {B'} _ → A' ≃ B')
    (λ _ → id≃)
    {A} {B} p

-- equivalences are injective

_⋆_ : {A B : Set} → (A ≃ B) → (x : A) → B
(f , _) ⋆ x = f x

inj≃ : {A B : Set} → (eq : A ≃ B) → (x y : A) → (eq ⋆ x ≡ eq ⋆ y → x ≡ y)
inj≃ (f , mkisequiv g α h β) x y p = ! (β x) ∘ (ap h p ∘ β y)

-- equivalences for coproducts (Sec. 2.12)

indCP : {A B : Set} → (C : A ⊎ B → Set) →
        ((a : A) → C (inj₁ a)) → ((b : B) → C (inj₂ b)) → ((x : A ⊎ B) → C x)
indCP C f g (inj₁ a) = f a
indCP C f g (inj₂ b) = g b

code : {A B : Set} → (a₀ : A) → A ⊎ B → Set
code a₀ (inj₁ a) = a₀ ≡ a
code a₀ (inj₂ b) = ⊥

encode : {A B : Set} → (a₀ : A) → (x : A ⊎ B) → (p : inj₁ a₀ ≡ x) → code a₀ x
encode {A} {B} a₀ x p = transport (code a₀) p (refl a₀)

decode : {A B : Set} → (a₀ : A) → (x : A ⊎ B) → (c : code a₀ x) → inj₁ a₀ ≡ x
decode a₀ (inj₁ a) c = ap inj₁ c
decode a₀ (inj₂ b) ()

codeqinv : {A B : Set} {a₀ : A} {x : A ⊎ B} → qinv (encode a₀ x)
codeqinv {A} {B} {a₀} {x} = record {
  g = decode a₀ x ;
  α = indCP
        (λ x → (c : code a₀ x) → encode a₀ x (decode a₀ x c) ≡ c)
        (λ a c → encode a₀ (inj₁ a) (decode a₀ (inj₁ a) c)
                   ≡⟨ bydef ⟩
                 encode a₀ (inj₁ a) (ap inj₁ c)
                   ≡⟨ bydef ⟩
                 transport (code a₀) (ap inj₁ c) (refl a₀)
                   ≡⟨ ! (transport-f inj₁ (code a₀) c (refl a₀)) ⟩
                 transport (λ a → code {A} {B} a₀ (inj₁ a)) c (refl a₀)
                   ≡⟨ bydef ⟩
                 transport (λ a → a₀ ≡ a) c (refl a₀)
                   ≡⟨ transportIdR c (refl a₀) ⟩
                 (refl a₀) ∘ c
                   ≡⟨ ! (unitTransL c) ⟩
                 c ∎)
        (λ b ())
        x ;
  β = λ p → basedPathInd
              (inj₁ a₀)
              (λ x p → decode a₀ x (encode a₀ x p) ≡ p)
              (decode a₀ (inj₁ a₀)
                (encode {A} {B} a₀ (inj₁ a₀) (refl (inj₁ a₀)))
                 ≡⟨ bydef ⟩
              (decode a₀ (inj₁ a₀)
                (transport (code {A} {B} a₀) (refl (inj₁ a₀)) (refl a₀)))
                 ≡⟨ bydef ⟩
              (decode a₀ (inj₁ a₀) (refl a₀))
                 ≡⟨ bydef ⟩
              (ap inj₁ (refl a₀))
                 ≡⟨ bydef ⟩
               refl (inj₁ a₀) ∎)
              x p }

thm2-12-5 : {A B : Set} → (a₀ : A) → (x : A ⊎ B) → (inj₁ a₀ ≡ x) ≃ code a₀ x
thm2-12-5 {A} {B} a₀ x = (encode a₀ x , equiv₁ codeqinv)

inj₁₁path : {A B : Set} → (a₁ a₂ : A) →
          (inj₁ {A = A} {B = B} a₁ ≡ inj₁ a₂) ≃ (a₁ ≡ a₂)
inj₁₁path a₁ a₂ = thm2-12-5 a₁ (inj₁ a₂)

inj₁₂path : {A B : Set} → (a : A) (b : B) → (inj₁ a ≡ inj₂ b) ≃ ⊥
inj₁₂path a b = thm2-12-5 a (inj₂ b)

-- Abbreviations for equivalence compositions

_≃⟨_⟩_ : (A : Set) {B C : Set} → (A ≃ B) → (B ≃ C) → (A ≃ C)
_ ≃⟨ p ⟩ q = trans≃ p q

_∎≃ : {ℓ : Level} {A : Set ℓ} → A ≃ A
_∎≃ {ℓ} {A} = id≃ {ℓ} {A}

------------------------------------------------------------------------------
-- Type equivalences

-- unite₊ and uniti₊

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

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

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

unite₊∙uniti₊ : {A : Set} → unite₊ ○ uniti₊ ∼ id {A = A}
unite₊∙uniti₊ = refl

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

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

-- swap₊

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

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

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

-- assocl₊ and assocr₊

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

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

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

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

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

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

-- unite⋆ and uniti⋆

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

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

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

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

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

-- swap⋆

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

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

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

-- assocl⋆ and assocr⋆

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

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

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

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

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

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

-- distz and factorz

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

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

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

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

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

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

-- dist and factor

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

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

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

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

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

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

-- congruence

-- ⊕

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

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

-- ⊗

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

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

------------------------------------------------------------------------------
-- Pi as a higher-order inductive type

module PI where

  -- hidden

  private
    data FT* : Set where
      ZERO*  : FT*
      ONE*   : FT*
      PLUS*  : FT* → FT* → FT*
      TIMES* : FT* → FT* → FT*
      NEG*   : FT* → FT*
      RECIP* : FT* → FT*

  -- exported

  FT : Set
  FT = FT*

  ZERO : FT
  ZERO = ZERO*

  ONE : FT
  ONE = ONE*

  PLUS : FT → FT → FT
  PLUS = PLUS*

  TIMES : FT → FT → FT
  TIMES = TIMES*

  NEG : FT → FT
  NEG = NEG*

  RECIP : FT → FT
  RECIP = RECIP*

  postulate
    -- additive structure
    unite₊≡  : { b : FT } → PLUS ZERO b ≡ b
    uniti₊≡  : { b : FT } → b ≡ PLUS ZERO b
    swap₊≡   : { b₁ b₂ : FT } → PLUS b₁ b₂ ≡ PLUS b₂ b₁
    assocl₊≡ : { b₁ b₂ b₃ : FT } → PLUS b₁ (PLUS b₂ b₃) ≡ PLUS (PLUS b₁ b₂) b₃
    assocr₊≡ : { b₁ b₂ b₃ : FT } → PLUS (PLUS b₁ b₂) b₃ ≡ PLUS b₁ (PLUS b₂ b₃)
    -- multiplicative structure
    unite⋆≡  : { b : FT } → TIMES ONE b ≡ b
    uniti⋆≡  : { b : FT } → b ≡ TIMES ONE b
    swap⋆≡   : { b₁ b₂ : FT } → TIMES b₁ b₂ ≡ TIMES b₂ b₁
    assocl⋆≡ : { b₁ b₂ b₃ : FT } →
               TIMES b₁ (TIMES b₂ b₃) ≡ TIMES (TIMES b₁ b₂) b₃
    assocr⋆≡ : { b₁ b₂ b₃ : FT } →
               TIMES (TIMES b₁ b₂) b₃ ≡ TIMES b₁ (TIMES b₂ b₃)
    -- distributivity
    distz≡   : { b : FT } → TIMES ZERO b ≡ ZERO
    factorz≡ : { b : FT } → ZERO ≡ TIMES ZERO b
    dist≡    : { b₁ b₂ b₃ : FT } →
              TIMES (PLUS b₁ b₂) b₃ ≡ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
    factor≡  : { b₁ b₂ b₃ : FT } →
              PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ≡ TIMES (PLUS b₁ b₂) b₃
    -- negatives and fractionals
    η₊       : { b : FT } → ZERO ≡ PLUS (NEG b) b
    ε₊       : { b : FT } → PLUS (NEG b) b ≡ ZERO
    refe⋆    : { b : FT } → RECIP (RECIP b) ≡ b
    refi⋆    : { b : FT } → b ≡ RECIP (RECIP b)
    rile⋆    : { b : FT } → TIMES b (TIMES b (RECIP b)) ≡ b
    rili⋆    : { b : FT } → b ≡ TIMES b (TIMES b (RECIP b))
    -- no need to postulate congruence; it will be provable

  -- Any function mapping PI to a type C must produce one of the following
  -- records that shows how both points and paths are mapped

  record PIR {ℓ : Level} (C : Set ℓ) : Set (lsuc ℓ) where
    field
      czero     : C
      cone      : C
      cplus     : C → C → C
      ctimes    : C → C → C
      cneg      : C → C
      crecip    : C → C
      cunite₊≡  : { c : C } → cplus czero c ≡ c
      cuniti₊≡  : { c : C } → c ≡ cplus czero c
      cswap₊≡   : { c₁ c₂ : C } → cplus c₁ c₂ ≡ cplus c₂ c₁
      cassocl₊≡ : { c₁ c₂ c₃ : C } →
                  cplus c₁ (cplus c₂ c₃) ≡ cplus (cplus c₁ c₂) c₃
      cassocr₊≡ : { c₁ c₂ c₃ : C } →
                  cplus (cplus c₁ c₂) c₃ ≡ cplus c₁ (cplus c₂ c₃)
      cunite⋆≡  : { c : C } → ctimes cone c ≡ c
      cuniti⋆≡  : { c : C } → c ≡ ctimes cone c
      cswap⋆≡   : { c₁ c₂ : C } → ctimes c₁ c₂ ≡ ctimes c₂ c₁
      cassocl⋆≡ : { c₁ c₂ c₃ : C } →
                  ctimes c₁ (ctimes c₂ c₃) ≡ ctimes (ctimes c₁ c₂) c₃
      cassocr⋆≡ : { c₁ c₂ c₃ : C } →
                  ctimes (ctimes c₁ c₂) c₃ ≡ ctimes c₁ (ctimes c₂ c₃)
      cdistz≡   : { c : C } → ctimes czero c ≡ czero
      cfactorz≡ : { c : C } → czero ≡ ctimes czero c
      cdist≡    : { c₁ c₂ c₃ : C } →
                  ctimes (cplus c₁ c₂) c₃ ≡ cplus (ctimes c₁ c₃) (ctimes c₂ c₃)
      cfactor≡  : { c₁ c₂ c₃ : C } →
                  cplus (ctimes c₁ c₃) (ctimes c₂ c₃) ≡ ctimes (cplus c₁ c₂) c₃
      cη₊       : { c : C } → czero ≡ cplus (cneg c) c
      cε₊       : { c : C } → cplus (cneg c) c ≡ czero
      crefe⋆    : { c : C } → crecip (crecip c) ≡ c
      crefi⋆    : { c : C } → c ≡ crecip (crecip c)
      crile⋆    : { c : C } → ctimes c (ctimes c (crecip c)) ≡ c
      crili⋆    : { c : C } → c ≡ ctimes c (ctimes c (crecip c))

  open PIR

  -- recursion principle for PI: given a target type C and a target record as
  -- above that has appropriate points and paths, recPI shows how points are
  -- mapped to points; the postulates assert that paths are transported as
  -- expected

  recPI : {ℓ : Level} {C : Set ℓ} → (PIR C) → FT → C
  recPI pir ZERO*          = czero pir
  recPI pir ONE*           = cone pir
  recPI pir (PLUS* B₁ B₂)  = cplus pir (recPI pir B₁) (recPI pir B₂)
  recPI pir (TIMES* B₁ B₂) = ctimes pir (recPI pir B₁) (recPI pir B₂)
  recPI pir (NEG* B)       = cneg pir (recPI pir B)
  recPI pir (RECIP* B)     = crecip pir (recPI pir B)

  postulate
    βreccunite₊≡  : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b : FT} → ap (recPI pir) (unite₊≡ {b}) ≡ cunite₊≡ pir
    βreccuniti₊≡  : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b : FT} → ap (recPI pir) (uniti₊≡ {b}) ≡ cuniti₊≡ pir
    βreccswap₊≡   : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b₁ b₂ : FT} → ap (recPI pir) (swap₊≡ {b₁} {b₂}) ≡ cswap₊≡ pir
    βreccassocl₊≡ : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b₁ b₂ b₃ : FT} → ap (recPI pir) (assocl₊≡ {b₁} {b₂} {b₃}) ≡
      cassocl₊≡ pir
    βreccassocr₊≡ : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b₁ b₂ b₃ : FT} → ap (recPI pir) (assocr₊≡ {b₁} {b₂} {b₃}) ≡
      cassocr₊≡ pir
    βreccunite⋆≡  : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b : FT} → ap (recPI pir) (unite⋆≡ {b}) ≡ cunite⋆≡ pir
    βreccuniti⋆≡  : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b : FT} → ap (recPI pir) (uniti⋆≡ {b}) ≡ cuniti⋆≡ pir
    βreccswap⋆≡   : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b₁ b₂ : FT} → ap (recPI pir) (swap⋆≡ {b₁} {b₂}) ≡ cswap⋆≡ pir
    βreccassocl⋆≡ : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b₁ b₂ b₃ : FT} → ap (recPI pir) (assocl⋆≡ {b₁} {b₂} {b₃}) ≡
      cassocl⋆≡ pir
    βreccassocr⋆≡ : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b₁ b₂ b₃ : FT} → ap (recPI pir) (assocr⋆≡ {b₁} {b₂} {b₃}) ≡
      cassocr⋆≡ pir
    βreccdistz≡   : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b : FT} → ap (recPI pir) (distz≡ {b}) ≡ cdistz≡ pir
    βreccfactorz≡ : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b : FT} → ap (recPI pir) (factorz≡ {b}) ≡ cfactorz≡ pir
    βreccdist≡    : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b₁ b₂ b₃ : FT} → ap (recPI pir) (dist≡ {b₁} {b₂} {b₃}) ≡
      cdist≡ pir
    βreccfactor≡  : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      {b₁ b₂ b₃ : FT} → ap (recPI pir) (factor≡ {b₁} {b₂} {b₃}) ≡
      cfactor≡ pir
    βreccη₊       : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      { b : FT } → ap (recPI pir) (η₊ {b}) ≡ cη₊ pir
    βreccε₊       : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      { b : FT } → ap (recPI pir) (ε₊ {b}) ≡ cε₊ pir
    βreccrefe⋆    : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      { b : FT } → ap (recPI pir) (refe⋆ {b}) ≡ crefe⋆ pir
    βreccrefi⋆    : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      { b : FT } → ap (recPI pir) (refi⋆ {b}) ≡ crefi⋆ pir
    βreccrile⋆    : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      { b : FT } → ap (recPI pir) (rile⋆ {b}) ≡ crile⋆ pir
    βreccrili⋆    : {ℓ : Level} {C : Set ℓ} → (pir : PIR C) →
      { b : FT } → ap (recPI pir) (rili⋆ {b}) ≡ crili⋆ pir

open PI public

------------------------------------------------------------------------------
-- Semantics I
-- The rationals are a model of PI

{--
unitPlus : (n : ℕ) -> (n + 0) ≡ n
unitPlus 0       = refl 0
unitPlus (suc m) = ap suc (unitPlus m)

sPlus : (n m : ℕ) -> suc (n + m) ≡ (n + suc m)
sPlus 0 m       = refl (suc m)
sPlus (suc n) m = ap suc (sPlus n m)

commPlus : (m n : ℕ) -> (m + n) ≡ (n + m)
commPlus 0 n       = ! (unitPlus n)
commPlus (suc m) n = (ap suc (commPlus m n)) ∘ (sPlus n m)

assocPlus : (m n o : ℕ) ->((m + n) + o) ≡ (m + (n + o))
assocPlus 0 n o       = refl (n + o)
assocPlus (suc m) n o = ap suc (assocPlus m n o)

--

unitMult : (i : ℕ) → 1 * i ≡ i
unitMult 0       = refl 0
unitMult (suc i) = ap suc (unitMult i)

mulSuc : (m n : ℕ) → m * suc n ≡ m + m * n
mulSuc 0 n       = refl 0
mulSuc (suc m) n = ap (λ x → suc n + x) (mulSuc m n) ∘
                   ap suc (! (assocPlus n m (m * n))) ∘
                   ap (λ x → suc (x + m * n)) (commPlus n m) ∘
                   ap suc (assocPlus m n (m * n))

annMult : (i : ℕ) → i * 0 ≡ 0
annMult 0       = refl 0
annMult (suc i) = annMult i

commMult : (i j : ℕ) → i * j ≡ j * i
commMult 0 j       = ! (annMult j)
commMult (suc i) j = ap (λ x → j + x) (commMult i j) ∘
                     (! (mulSuc j i))

distrib : (i j k : ℕ) → (j + k) * i ≡ j * i + k * i
distrib i 0 k       = refl (k * i)
distrib i (suc j) k = ap (_+_ i) (distrib i j k) ∘
                      (! (assocPlus i (j * i) (k * i)))

assocMult : (i j k : ℕ) → (i * j) * k ≡ i * (j * k)
assocMult 0 j k       = refl 0
assocMult (suc i) j k = distrib k j (i * j) ∘
                        ap (λ x → j * k + x) (assocMult i j k)
--}

--

toℚ : FT → ℚ
toℚ b = recPI (record {
          czero     = + 0 ÷ 1 ;
          cone      = + 1 ÷ 1 ;
          cplus     = {!!} ; --_+_ ;
          ctimes    = {!!} ; --_*_ ;
          cneg      = {!!} ;
          crecip    = {!!} ;
          cunite₊≡  = {!!} ; --λ {c} → refl c ;
          cuniti₊≡  = {!!} ; --λ {c} → refl c ;
          cswap₊≡   = {!!} ; --λ {a b} → commPlus a b ;
          cassocl₊≡ = {!!} ; --λ {a b c} → ! (assocPlus a b c) ;
          cassocr₊≡ = {!!} ; --λ {a b c} → assocPlus a b c ;
          cunite⋆≡  = {!!} ; --λ {a} → unitMult a ;
          cuniti⋆≡  = {!!} ; --λ {a} → ! (unitMult a) ;
          cswap⋆≡   = {!!} ; --λ {a b} → commMult a b  ;
          cassocl⋆≡ = {!!} ; --λ {a b c} → ! (assocMult a b c) ;
          cassocr⋆≡ = {!!} ; --λ {a b c} → assocMult a b c ;
          cdistz≡   = {!!} ; --refl 0  ;
          cfactorz≡ = {!!} ; --refl 0 ;
          cdist≡    = {!!} ; --λ {a b c} → distrib c a b ;
          cfactor≡  = {!!} ; --λ {a b c} → ! (distrib c a b) ;
          cη₊       = {!!} ;
          cε₊       = {!!} ;
          crefe⋆    = {!!} ;
          crefi⋆    = {!!} ;
          crile⋆    = {!!} ;
          crili⋆    = {!!}
        }) b

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module is-free where

open import lib

open import cedille-types
open import ctxt-types
open import syntax-util
open import general-util

are-free-e = 𝔹
check-erased = tt
skip-erased = ff

are-free-in-t : Set → Set₁
are-free-in-t T = ∀{A} → are-free-e → trie A → T → 𝔹

are-free-in-term : are-free-in-t term
are-free-in-type : are-free-in-t type
are-free-in-kind : are-free-in-t kind
are-free-in-optClass : are-free-in-t optClass
-- are-free-in-optType : are-free-in-t optType
are-free-in-optTerm : are-free-in-t optTerm
are-free-in-optGuide : are-free-in-t optGuide
are-free-in-tk : are-free-in-t tk
are-free-in-liftingType : are-free-in-t liftingType
are-free-in-optType : are-free-in-t optType
are-free-in-args : are-free-in-t args
are-free-in-cases : are-free-in-t cases
are-free-in-varargs : are-free-in-t varargs

are-free-in-term ce x (App t Erased t') = are-free-in-term ce x t || (ce && are-free-in-term ce x t')
are-free-in-term ce x (App t NotErased t') = are-free-in-term ce x t || are-free-in-term ce x t'
are-free-in-term ce x (AppTp t tp) = are-free-in-term ce x t || (ce && are-free-in-type ce x tp)
are-free-in-term ce x (Hole x₁) = ff
are-free-in-term ce x (Lam _ b _ x' oc t) =
  (ce && are-free-in-optClass ce x oc)
  || are-free-in-term ce (trie-remove x x') t
are-free-in-term ce x (Let _ (DefTerm _ x' m t) t') =
  (ce && are-free-in-optType ce x m)
  || (are-free-in-term ce x t)
  || are-free-in-term ce (trie-remove x x') t'
are-free-in-term ce x (Let _ (DefType _ x' k t) t') =
  (ce && (are-free-in-kind ce x k || are-free-in-type ce x t))
  || are-free-in-term ce (trie-remove x x') t'
are-free-in-term ce x (Open _ _ t) = are-free-in-term ce x t -- return the same answer as the erasure of (Open ...)
are-free-in-term ce x (Parens x₁ t x₂) = are-free-in-term ce x t
are-free-in-term ce x (Var _ "_") = ff
are-free-in-term ce x (Var _ x') = trie-contains x x'
are-free-in-term ce x (Beta _ ot ot') = are-free-in-optTerm ce x ot' || (ce && are-free-in-optTerm ce x ot)
are-free-in-term ce x (IotaPair _ t1 t2 ot _) = are-free-in-term ce x t1 || (ce && (are-free-in-term ce x t2 || are-free-in-optGuide ce x ot))
are-free-in-term ce x (IotaProj t n _) = are-free-in-term ce x t
are-free-in-term ce x (Epsilon _ _ _ t) = are-free-in-term ce x t
are-free-in-term ce x (Sigma _ t) = are-free-in-term ce x t
are-free-in-term ce x (Phi _ t t₁ t₂ _) = (ce && are-free-in-term ce x t) || (ce && are-free-in-term ce x t₁) || are-free-in-term ce x t₂
are-free-in-term ce x (Rho _ _ _ t ot t') = (ce && (are-free-in-term ce x t || are-free-in-optGuide ce x ot)) || are-free-in-term ce x t'
are-free-in-term ce x (Chi _ T t') = (ce && are-free-in-optType ce x T) || are-free-in-term ce x t'
are-free-in-term ce x (Delta _ T t') = ce && (are-free-in-optType ce x T || are-free-in-term ce x t')
are-free-in-term ce x (Theta _ _ t ls) = are-free-in-term ce x t || are-free-in-lterms ce x ls
  where are-free-in-lterms : ∀{A} → are-free-e → trie A → lterms → 𝔹
        are-free-in-lterms ce x (LtermsNil _) = ff
        are-free-in-lterms ce x (LtermsCons Erased t ls) = (ce && are-free-in-term ce x t) || are-free-in-lterms ce x ls
        are-free-in-lterms ce x (LtermsCons NotErased t ls) = are-free-in-term ce x t || are-free-in-lterms ce x ls
are-free-in-term ce x (Mu _ x' t ot _ cs _) = (ce && are-free-in-optType ce x ot) || are-free-in-term ce (trie-remove x x') t || are-free-in-cases ce x cs
are-free-in-term ce x (Mu' _   t ot _ cs _) = (ce && are-free-in-optType ce x ot) || are-free-in-term ce x t || are-free-in-cases ce x cs

are-free-in-cases _ _  NoCase                    = ff
are-free-in-cases ce x (SomeCase _ c varargs t cs) = are-free-in-varargs ce x varargs || are-free-in-term ce x t || are-free-in-cases ce x cs

are-free-in-varargs ce x NoVarargs              = ff
are-free-in-varargs ce x (NormalVararg x' args) = trie-contains x x'         || are-free-in-varargs ce x args
are-free-in-varargs ce x (ErasedVararg x' args) = (ce && trie-contains x x') || are-free-in-varargs ce x args
are-free-in-varargs ce x (TypeVararg   x' args) = (ce && trie-contains x x') || are-free-in-varargs ce x args

{-# TERMINATING #-}
are-free-in-type ce x (Abs _ _ _ x' atk t) = are-free-in-tk ce x atk || are-free-in-type ce (trie-remove x x') t
are-free-in-type ce x (TpLambda _ _ x' atk t) = are-free-in-tk ce x atk || are-free-in-type ce (trie-remove x x') t
are-free-in-type ce x (Iota _ _ x' m t) = are-free-in-type ce x m || are-free-in-type ce (trie-remove x x') t
are-free-in-type ce x (Lft _ _ X t l) = are-free-in-liftingType ce x l || are-free-in-term ce (trie-remove x X) t
are-free-in-type ce x (TpApp t t') = are-free-in-type ce x t || are-free-in-type ce x t'
are-free-in-type ce x (TpAppt t t') = are-free-in-type ce x t || are-free-in-term ce x t'
are-free-in-type ce x (TpArrow t _ t') = are-free-in-type ce x t || are-free-in-type ce x t'
are-free-in-type ce x (TpEq _ t t' _) = are-free-in-term ce x t || are-free-in-term ce x t'
are-free-in-type ce x (TpParens x₁ t x₂) = are-free-in-type ce x t
are-free-in-type ce x (TpVar _ "_") = ff
are-free-in-type ce x (TpVar _ x') = trie-contains x x'
are-free-in-type ce x (NoSpans t _) = are-free-in-type ce x t
are-free-in-type ce x (TpHole _) = ff
are-free-in-type ce x (TpLet _ (DefTerm _ x' m t) T) =
  (ce && are-free-in-optType ce x m)
  || (are-free-in-term ce x t)
  || are-free-in-type ce (trie-remove x x') T
are-free-in-type ce x (TpLet _ (DefType _ x' k T) T') =
  (ce && (are-free-in-kind ce x k || are-free-in-type ce x T))
  || are-free-in-type ce (trie-remove x x') T'

are-free-in-kind ce x (KndArrow k k') = are-free-in-kind ce x k || are-free-in-kind ce x k'
are-free-in-kind ce x (KndParens x₁ k x₂) = are-free-in-kind ce x k
are-free-in-kind ce x (KndPi _ _ x' atk k) = are-free-in-tk ce x atk || are-free-in-kind ce (trie-remove x x') k
are-free-in-kind ce x (KndTpArrow t k) = are-free-in-type ce x t || are-free-in-kind ce x k
are-free-in-kind ce x (KndVar _ x' ys) = trie-contains x x' || are-free-in-args ce x ys
are-free-in-kind ce x (Star x₁) = ff

are-free-in-args ce x (ArgsCons (TermArg _ y) ys) = are-free-in-term ce x y || are-free-in-args ce x ys
are-free-in-args ce x (ArgsCons (TypeArg y) ys) = are-free-in-type ce x y || are-free-in-args ce x ys
are-free-in-args ce x ArgsNil = ff

are-free-in-optClass ce x NoClass = ff
are-free-in-optClass ce x (SomeClass atk) = are-free-in-tk ce x atk

are-free-in-optType ce x NoType = ff
are-free-in-optType ce x (SomeType t) = are-free-in-type ce x t

are-free-in-optTerm ce x NoTerm = ff
are-free-in-optTerm ce x (SomeTerm t _) = are-free-in-term ce x t

are-free-in-optGuide ce x NoGuide = ff
are-free-in-optGuide ce x (Guide _ v tp) = are-free-in-type ce (trie-remove x v) tp

are-free-in-tk ce x (Tkt t) = are-free-in-type ce x t
are-free-in-tk ce x (Tkk k) = are-free-in-kind ce x k

are-free-in-liftingType ce x (LiftArrow l l') = are-free-in-liftingType ce x l || are-free-in-liftingType ce x l'
are-free-in-liftingType ce x (LiftParens x₁ l x₂) = are-free-in-liftingType ce x l
are-free-in-liftingType ce x (LiftPi _ x' t l) =
  are-free-in-type ce x t || are-free-in-liftingType ce (trie-remove x x') l
are-free-in-liftingType ce x (LiftStar x₁) = ff
are-free-in-liftingType ce x (LiftTpArrow t l) = are-free-in-type ce x t || are-free-in-liftingType ce x l

are-free-in : {ed : exprd} → are-free-e → stringset → ⟦ ed ⟧ → 𝔹
are-free-in{TERM} e x t = are-free-in-term e x t
are-free-in{ARG} e x (TermArg _ t) = are-free-in-term e x t
are-free-in{TYPE} e x t = are-free-in-type e x t
are-free-in{ARG} e x (TypeArg t) = are-free-in-type e x t
are-free-in{KIND} e x t = are-free-in-kind e x t
are-free-in{TK} e x t = are-free-in-tk e x t
are-free-in{LIFTINGTYPE} e x t = are-free-in-liftingType e x t
are-free-in{QUALIF} e x (x' , as) = trie-contains x x' || are-free-in-args e x as

is-free-in : {ed : exprd} → are-free-e → var → ⟦ ed ⟧ → 𝔹
is-free-in{TERM} e x t = are-free-in-term e (stringset-singleton x) t
is-free-in{ARG} e x (TermArg _ t) = are-free-in-term e (stringset-singleton x) t
is-free-in{TYPE} e x t = are-free-in-type e (stringset-singleton x) t
is-free-in{ARG} e x (TypeArg t) = are-free-in-type e (stringset-singleton x) t
is-free-in{KIND} e x t = are-free-in-kind e (stringset-singleton x) t
is-free-in{LIFTINGTYPE} e x t = are-free-in-liftingType e (stringset-singleton x) t
is-free-in{QUALIF} e x (x' , as) = x =string x' || are-free-in-args e (stringset-singleton x) as
is-free-in{TK} e x t = are-free-in-tk e (stringset-singleton x) t

abs-tk : maybeErased → var → tk → type → type
abs-tk me x (Tkk k) tp = Abs posinfo-gen Erased posinfo-gen x (Tkk k) tp
abs-tk me x (Tkt tp') tp with are-free-in check-erased (stringset-singleton x) tp
abs-tk me x (Tkt tp') tp | tt = Abs posinfo-gen me posinfo-gen x (Tkt tp') tp
abs-tk me x (Tkt tp') tp | ff = TpArrow tp' me tp

absk-tk : var → tk → kind → kind
absk-tk x atk k with are-free-in check-erased (stringset-singleton x) k
absk-tk x atk k | tt = KndPi posinfo-gen posinfo-gen x atk k
absk-tk x (Tkt tp) k | ff = KndTpArrow tp k
absk-tk x (Tkk k') k | ff = KndArrow k' k

data abs  : Set where
  mk-abs : maybeErased → var → tk → (var-free-in-body : 𝔹) → type → abs

to-abs : type → maybe abs
to-abs (Abs _ me _ x atk tp) = just (mk-abs me x atk (are-free-in check-erased (stringset-singleton x) tp) tp)
to-abs (TpArrow tp1 me tp2) = just (mk-abs me dummy-var (Tkt tp1) ff tp2)
to-abs _ = nothing

record is-tpabs : Set where
  constructor mk-tpabs
  field
    is-tpabs-e?   : maybeErased
    is-tpabs-var  : var
    is-tpabs-kind : kind
    is-tpabs-body : type
open is-tpabs public

is-tpabs? = type ∨ is-tpabs

pattern yes-tpabs e? x k tp = inj₂ (mk-tpabs e? x k tp)
pattern not-tpabs tp = inj₁ tp

to-is-tpabs : type → is-tpabs?
to-is-tpabs tp with to-abs tp
... | nothing =
  not-tpabs tp
... | just (mk-abs _ _ (Tkt _) _ _)
  = not-tpabs tp
... | just (mk-abs e? x (Tkk k) var-free-in-body tp') =
  yes-tpabs e? x k tp'

data absk  : Set where
  mk-absk : var → tk → (var-free-in-body : 𝔹) → kind → absk

to-absk : kind → maybe absk
to-absk (KndPi _ _ x atk k) = just (mk-absk x atk (are-free-in check-erased (stringset-singleton x) k) k)
to-absk (KndArrow k1 k2) = just (mk-absk dummy-var (Tkk k1) ff k2)
to-absk (KndTpArrow tp k) = just (mk-absk dummy-var (Tkt tp) ff k)
to-absk _ = nothing

record is-tmabs : Set where
  constructor mk-tmabs
  field
    is-tmabs-binder : maybeErased
    is-tmabs-var    : var
    is-tmabs-dom    : type
    is-tmabs-var-in-body : 𝔹
    is-tmabs-cod    : type
open is-tmabs public

is-tmabs? = type ∨ is-tmabs

pattern yes-tmabs e? x dom occurs cod = inj₂ (mk-tmabs e? x dom occurs cod)
pattern not-tmabs tp = inj₁ tp

to-is-tmabs : type → is-tmabs?
to-is-tmabs (Abs _ e? _ x (Tkt dom) cod) =
  yes-tmabs e? x dom (is-free-in check-erased x cod) cod
to-is-tmabs (TpArrow dom e? cod) =
  yes-tmabs e? "_" dom ff cod
to-is-tmabs tp = not-tmabs tp

from-is-tmabs : is-tmabs → type
from-is-tmabs (mk-tmabs b x dom occ cod) =
  Abs posinfo-gen b posinfo-gen x (Tkt dom) cod

ext: agda

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
open import AEff
open import EffectAnnotations
open import Types hiding (``)

open import Relation.Binary.PropositionalEquality hiding ([_] ; Extensionality)
--open ≡-Reasoning

module Renamings where

-- SET OF RENAMINGS BETWEEN CONTEXTS

Ren : Ctx → Ctx → Set
Ren Γ Γ' = {X : VType} → X ∈ Γ → X ∈ Γ'

-- IDENTITY, COMPOSITION, AND EXCHANGE RENAMINGS

id-ren : {Γ : Ctx} → Ren Γ Γ
id-ren {X} x = x

comp-ren : {Γ Γ' Γ'' : Ctx} → Ren Γ' Γ'' → Ren Γ Γ' → Ren Γ Γ''
comp-ren f g x = f (g x)

exchange : {Γ : Ctx} {X Y : VType} → Ren (Γ ∷ X ∷ Y) (Γ ∷ Y ∷ X)
exchange Hd = Tl Hd
exchange (Tl Hd) = Hd
exchange (Tl (Tl x)) = Tl (Tl x)

-- WEAKENING OF RENAMINGS

wk₁ : {Γ : Ctx} {X : VType} → Ren Γ (Γ ∷ X)
wk₁ = Tl

wk₂ : {Γ Γ' : Ctx} {X : VType} → Ren Γ Γ' → Ren (Γ ∷ X) (Γ' ∷ X)
wk₂ f Hd = Hd
wk₂ f (Tl v) = Tl (f v)

wk₃ : {Γ : Ctx} {X Y Z : VType} → Ren (Γ ∷ Y ∷ Z) (Γ ∷ X ∷ Y ∷ Z)
wk₃ Hd = Hd
wk₃ (Tl Hd) = Tl Hd
wk₃ (Tl (Tl x)) = Tl (Tl (Tl x))

-- ACTION OF RENAMING ON WELL-TYPED VALUES AND COMPUTATIONS

mutual

  V-rename : {X : VType} {Γ Γ' : Ctx} → Ren Γ Γ' → Γ ⊢V⦂ X → Γ' ⊢V⦂ X
  V-rename f (` x) = ` f x
  V-rename f (`` c) = `` c
  V-rename f (ƛ M) = ƛ (M-rename (wk₂ f) M)
  V-rename f ⟨ V ⟩ = ⟨ V-rename f V ⟩

  M-rename : {C : CType} {Γ Γ' : Ctx} → Ren Γ Γ' → Γ ⊢M⦂ C → Γ' ⊢M⦂ C
  M-rename f (return V) =
    return (V-rename f V)
  M-rename f (let= M `in N) =
    let= M-rename f M `in M-rename (wk₂ f) N
  M-rename f (letrec M `in N) =
    letrec M-rename (wk₂ (wk₂ f)) M `in M-rename (wk₂ f) N
  M-rename f (V · W) =
    V-rename f V · V-rename f W
  M-rename f (↑ op p V M) =
    ↑ op p (V-rename f V) (M-rename f M)
  M-rename f (↓ op V M) =
    ↓ op (V-rename f V) (M-rename f M)
  M-rename f (promise op ∣ p ↦ M `in N) =
    promise op ∣ p ↦ M-rename (wk₂ f) M `in M-rename (wk₂ f) N
  M-rename f (await V until M) =
    await (V-rename f V) until (M-rename (wk₂ f) M)
  M-rename f (coerce p q M) =
    coerce p q (M-rename f M)

-- ACTION OF RENAMING ON WELL-TYPED PROCESSES

P-rename : {o : O} {PP : PType o} {Γ Γ' : Ctx} → Ren Γ Γ' → Γ ⊢P⦂ PP → Γ' ⊢P⦂ PP
P-rename f (run M) =
  run (M-rename f M)
P-rename f (P ∥ Q) =
  P-rename f P ∥ P-rename f Q
P-rename f (↑ op p V P) =
  ↑ op p (V-rename f V) (P-rename f P)
P-rename f (↓ op V P) =
  ↓ op (V-rename f V) (P-rename f P)

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda


text:
module Numeral.Natural.Oper.Proofs.Multiplication where

open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Classical
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Operator
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Syntax.Transitivity

instance
  [⋅][−₀]-distributivityᵣ : Distributivityᵣ(_⋅_)(_−₀_)
  Distributivityᵣ.proof([⋅][−₀]-distributivityᵣ) {x}{y}{z} = p{x}{y}{z} where
    p : ∀{x y z : ℕ} → ((x −₀ y) ⋅ z) ≡ (x ⋅ z) −₀ (y ⋅ z)
    p {x} {y} {𝟎} = [≡]-intro
    p {x} {y} {𝐒 z} with [≥]-or-[<] {x}{y}
    ... | [∨]-introₗ gt =
      (x −₀ y) ⋅ 𝐒(z)                 🝖[ _≡_ ]-[]
      (x −₀ y) + ((x −₀ y) ⋅ z)       🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(x −₀ y) (p {x}{y}{z}) ]
      (x −₀ y) + ((x ⋅ z) −₀ (y ⋅ z)) 🝖[ _≡_ ]-[ [+][−₀]-almost-associativity {x −₀ y} ([≤]-with-[⋅]ᵣ {c = z} gt) ]-sym
      ((x −₀ y) + (x ⋅ z)) −₀ (y ⋅ z) 🝖[ _≡_ ]-[ congruence₂ₗ(_−₀_)(y ⋅ z) (commutativity(_+_) {x −₀ y}{x ⋅ z}) ]
      ((x ⋅ z) + (x −₀ y)) −₀ (y ⋅ z) 🝖[ _≡_ ]-[ congruence₂ₗ(_−₀_)(y ⋅ z) ([+][−₀]-almost-associativity {x ⋅ z} gt) ]-sym
      (((x ⋅ z) + x) −₀ y) −₀ (y ⋅ z) 🝖[ _≡_ ]-[ congruence₂ₗ(_−₀_)(y ⋅ z) (congruence₂ₗ(_−₀_)(y) (commutativity(_+_) {x ⋅ z}{x})) ]
      ((x + (x ⋅ z)) −₀ y) −₀ (y ⋅ z) 🝖[ _≡_ ]-[ [−₀][−₀]-to-[−₀][+] {x + (x ⋅ z)}{y}{y ⋅ z} ]
      (x + (x ⋅ z)) −₀ (y + (y ⋅ z))  🝖[ _≡_ ]-[]
      (x ⋅ 𝐒(z)) −₀ (y ⋅ 𝐒(z))        🝖-end
    ... | [∨]-introᵣ lt =
      (x −₀ y) ⋅ 𝐒(z)                🝖[ _≡_ ]-[ congruence₂ₗ(_⋅_)(𝐒(z)) ([↔]-to-[→] [−₀]-when-0 (sub₂(_<_)(_≤_) lt)) ]
      𝟎 ⋅ 𝐒(z)                       🝖[ _≡_ ]-[ absorberₗ(_⋅_)(𝟎) {𝐒(z)} ]
      𝟎                              🝖[ _≡_ ]-[ [↔]-to-[→] [−₀]-when-0 ([≤]-with-[+] ⦃ sub₂(_<_)(_≤_) lt ⦄ ⦃ [≤]-with-[⋅]ᵣ {c = z} (sub₂(_<_)(_≤_) lt) ⦄) ]-sym
      (x + (x ⋅ z)) −₀ (y + (y ⋅ z)) 🝖-end

-- TODO: This is a specialized distributivity-equivalence-by-commutativity
instance
  [⋅][−₀]-distributivityₗ : Distributivityₗ(_⋅_)(_−₀_)
  Distributivityₗ.proof([⋅][−₀]-distributivityₗ) {x}{y}{z} = p{x}{y}{z} where
    p : ∀{x y z : ℕ} → (x ⋅ (y −₀ z)) ≡ (x ⋅ y) −₀ (x ⋅ z)
    p{x}{y}{z} =
      x ⋅ (y −₀ z)       🝖[ _≡_ ]-[ commutativity(_⋅_) {x}{y −₀ z} ]
      (y −₀ z) ⋅ x       🝖[ _≡_ ]-[ distributivityᵣ(_⋅_)(_−₀_) {y}{z}{x} ]
      (y ⋅ x) −₀ (z ⋅ x) 🝖[ _≡_ ]-[ congruence₂(_−₀_) (commutativity(_⋅_) {y}{x}) (commutativity(_⋅_) {z}{x}) ]
      (x ⋅ y) −₀ (x ⋅ z) 🝖-end

[⋅]-cancellationₗ : ∀{x} → ⦃ pos : Positive(x) ⦄ → (Names.CancellationOnₗ(_⋅_)(x))
[⋅]-cancellationₗ {𝐒 a}{b}{c} p with [<]-trichotomy {b}{c}
... | [∨]-introₗ ([∨]-introₗ lt) with () ← [<]-to-[≢] ([<]-with-[⋅]ₗ {a = a} lt) p
... | [∨]-introₗ ([∨]-introᵣ eq) = eq
... | [∨]-introᵣ gt              with () ← [>]-to-[≢] ([<]-with-[⋅]ₗ {a = a} gt) p

[⋅]-cancellationᵣ : ∀{x} → ⦃ pos : Positive(x) ⦄ → (Names.CancellationOnᵣ(_⋅_)(x))
[⋅]-cancellationᵣ {𝐒 c}{a}{b} p with [<]-trichotomy {a}{b}
... | [∨]-introₗ ([∨]-introₗ lt) with () ← [<]-to-[≢] ([<]-with-[⋅]ᵣ {c = c} lt) p
... | [∨]-introₗ ([∨]-introᵣ eq) = eq
... | [∨]-introᵣ gt              with () ← [>]-to-[≢] ([<]-with-[⋅]ᵣ {c = c} gt) p

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 --warning=error #-}

open import Sets.EquivalenceRelations
open import Setoids.Setoids
open import Groups.FreeGroup.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Decidable.Sets
open import Numbers.Naturals.Order
open import LogicalFormulae
open import Semirings.Definition
open import Functions.Definition
open import Groups.Isomorphisms.Definition
open import Boolean.Definition
open import Boolean.Lemmas

module Groups.FreeGroup.Parity {a : _} {A : Set a} (decA : DecidableSet A) where

open import Groups.FreeGroup.Word decA
open import Groups.FreeGroup.Group decA

C2 : Group (reflSetoid Bool) xor
Group.+WellDefined C2 refl refl = refl
Group.0G C2 = BoolFalse
Group.inverse C2 = id
Group.+Associative C2 {BoolTrue} {BoolTrue} {BoolTrue} = refl
Group.+Associative C2 {BoolTrue} {BoolTrue} {BoolFalse} = refl
Group.+Associative C2 {BoolTrue} {BoolFalse} {z} = refl
Group.+Associative C2 {BoolFalse} {y} {z} = refl
Group.identRight C2 {BoolTrue} = refl
Group.identRight C2 {BoolFalse} = refl
Group.identLeft C2 {x} = refl
Group.invLeft C2 {BoolTrue} = refl
Group.invLeft C2 {BoolFalse} = refl
Group.invRight C2 {BoolTrue} = refl
Group.invRight C2 {BoolFalse} = refl

parity : (x : A) → ReducedWord → Bool
parity x empty = BoolFalse
parity x (prependLetter (ofLetter y) w _) with decA x y
parity x (prependLetter (ofLetter y) w _) | inl _ = not (parity x w)
parity x (prependLetter (ofLetter y) w _) | inr _ = parity x w
parity x (prependLetter (ofInv y) w _) with decA x y
parity x (prependLetter (ofInv y) w _) | inl _ = not (parity x w)
parity x (prependLetter (ofInv y) w _) | inr _ = parity x w

private
  parityPrepend : (a : A) (w : ReducedWord) (l : A) → ((a ≡ l) → False) → parity a (prepend w (ofLetter l)) ≡ parity a w
  parityPrepend a empty l notEq with decA a l
  parityPrepend a empty l notEq | inl x = exFalso (notEq x)
  parityPrepend a empty l notEq | inr x = refl
  parityPrepend a (prependLetter (ofLetter r) w x) l notEq with decA a l
  parityPrepend a (prependLetter (ofLetter r) w x) l notEq | inl m = exFalso (notEq m)
  parityPrepend a (prependLetter (ofLetter r) w x) l notEq | inr _ = refl
  parityPrepend a (prependLetter (ofInv r) w x) l notEq with decA a r
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r with decA l r
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inl l=r = exFalso (notEq (transitivity a=r (equalityCommutative l=r)))
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with decA a l
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inl a=l = exFalso (notEq a=l)
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with decA a r
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inl x₁ = refl
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inr bad = exFalso (bad a=r)
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r with decA l r
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl x₁ = refl
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with decA a l
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inl a=l = exFalso (notEq a=l)
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with decA a r
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inl a=r = exFalso (a!=r a=r)
  parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inr x₁ = refl

  parityPrepend' : (a : A) (w : ReducedWord) (l : A) → ((a ≡ l) → False) → parity a (prepend w (ofInv l)) ≡ parity a w
  parityPrepend' a empty l notEq with decA a l
  parityPrepend' a empty l notEq | inl x = exFalso (notEq x)
  parityPrepend' a empty l notEq | inr x = refl
  parityPrepend' a (prependLetter (ofLetter r) w x) l notEq with decA l r
  parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inl m with decA a r
  ... | inl a=r = exFalso (notEq (transitivity a=r (equalityCommutative m)))
  ... | inr a!=r = refl
  parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inr l!=r with decA a l
  ... | inl a=l = exFalso (notEq a=l)
  ... | inr a!=l = refl
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq with decA a r
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r with decA l r
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inl l=r = exFalso (notEq (transitivity a=r (equalityCommutative l=r)))
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with decA a l
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inl a=l = exFalso (notEq a=l)
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with decA a r
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inl x₁ = refl
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inr bad = exFalso (bad a=r)
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r with decA l r
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r with decA a l
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r | inl a=l = exFalso (notEq a=l)
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r | inr a!=l with decA a r
  ... | inl a=r = exFalso (a!=r a=r)
  ... | inr _ = refl
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with decA a l
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inl a=l = exFalso (notEq a=l)
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with decA a r
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inl a=r = exFalso (a!=r a=r)
  parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inr x₁ = refl

  parityPrepend'' : (a : A) (w : ReducedWord) → parity a (prepend w (ofLetter a)) ≡ not (parity a w)
  parityPrepend'' a empty with decA a a
  ... | inl _ = refl
  ... | inr bad = exFalso (bad refl)
  parityPrepend'' a (prependLetter (ofLetter l) w x) with decA a a
  parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ with decA a l
  parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ | inl a=l = refl
  parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ | inr a!=l = refl
  parityPrepend'' a (prependLetter (ofLetter l) w x) | inr bad = exFalso (bad refl)
  parityPrepend'' a (prependLetter (ofInv l) w x) with decA a l
  ... | inl a=l = equalityCommutative (notNot (parity a w))
  parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l with decA a a
  parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l | inl _ with decA a l
  ... | inl a=l = exFalso (a!=l a=l)
  ... | inr _ = refl
  parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l | inr bad = exFalso (bad refl)

  parityPrepend''' : (a : A) (w : ReducedWord) → parity a (prepend w (ofInv a)) ≡ not (parity a w)
  parityPrepend''' a empty with decA a a
  ... | inl _ = refl
  ... | inr bad = exFalso (bad refl)
  parityPrepend''' a (prependLetter (ofLetter l) w x) with decA a l
  ... | inl a=l = equalityCommutative (notNot _)
  parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l with decA a a
  ... | inl _ with decA a l
  parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l | inl _ | inl a=l = exFalso (a!=l a=l)
  parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l | inl _ | inr _ = refl
  parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l | inr bad = exFalso (bad refl)
  parityPrepend''' a (prependLetter (ofInv l) w x) with decA a a
  parityPrepend''' a (prependLetter (ofInv l) w x) | inl _ with decA a l
  ... | inl a=l = refl
  ... | inr a!=l = refl
  parityPrepend''' a (prependLetter (ofInv l) w x) | inr bad = exFalso (bad refl)

  parityHomIsHom : (a : A) → (x y : ReducedWord) → parity a (_+W_ x y) ≡ xor (parity a x) (parity a y)
  parityHomIsHom a empty y = refl
  parityHomIsHom a (prependLetter (ofLetter l) x _) y with decA a l
  parityHomIsHom a (prependLetter (ofLetter .a) x _) y | inl refl = transitivity (parityPrepend'' a (x +W y)) (transitivity (applyEquality not (parityHomIsHom a x y)) (notXor (parity a x) (parity a y)))
  parityHomIsHom a (prependLetter (ofLetter l) x _) y | inr a!=l = transitivity (parityPrepend a (_+W_ x y) l a!=l) (parityHomIsHom a x y)
  parityHomIsHom a (prependLetter (ofInv l) x _) y with decA a l
  parityHomIsHom a (prependLetter (ofInv .a) x _) y | inl refl = transitivity (parityPrepend''' a (x +W y)) (transitivity (applyEquality not (parityHomIsHom a x y)) (notXor (parity a x) (parity a y)))
  parityHomIsHom a (prependLetter (ofInv l) x _) y | inr a!=l = transitivity (parityPrepend' a (x +W y) l a!=l) (parityHomIsHom a x y)

parityHom : (x : A) → GroupHom (freeGroup) C2 (parity x)
GroupHom.groupHom (parityHom x) {y} {z} = parityHomIsHom x y z
GroupHom.wellDefined (parityHom x) refl = refl


text:
module _ where

postulate
  A : Set
  _,_ : A → A → A

module M where
  module Mx (x : A) where
    module M where
      module My (y : A) where
        f : A
        f = x , y

postulate
  a b c : A

module M′  = M
module Ma  = M′.Mx.M a
module Mab = Ma.My b

g : A
g =  Mab.f

-- Original bug report --

record I (A : Set) : Set where
  field
    i : A → A
  record R (A : Set) : Set where
    field
      f : A → A
  open R public

module C (A : Set) where
  I₀ : I A
  I₀ = record { i = λ x → x }

  open I I₀

  r : (B : Set) → R B
  r B = record { f = λ x → x }

  g1 : (B : Set) → B → B
  g1 B = f′
    where
      open R (r B) renaming (f to f′)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Base

module Spaces.LoopSpaceDecidableWedgeCircles {i} (A : Set i) (eq : has-dec-eq A)
  where

open import Spaces.WedgeCircles A renaming (wedge-circles to WA; base to baseWA)
open import Algebra.FreeGroup A renaming (freegroup to FA)
open import Algebra.FreeGroupProps A
open import Algebra.FreeGroupAsReducedWords A eq
open import Spaces.FlatteningLoopSpaceWedgeCircles A (dec-eq-is-set eq)

-- We can now prove that [tot-cover] is contractible using [CA-rec]
-- (because [CA-rec] means that [tot-cover] is the Cayley graph of FA)
P-CA-contr : (x : tot-cover) → Set _
P-CA-contr x = x ≡ CA-z e

-- We first prove it on points coming from reduced words
CA-contr-base-reduced-word : (w : reduced-word)
  → P-CA-contr (CA-z (reduced-to-freegroup w))
CA-contr-base-reduced-word (ε , red) = refl
CA-contr-base-reduced-word ((x ∷ w) , red) =
  ! (CA-e x _)
  ∘ CA-contr-base-reduced-word (w , tail-is-reduced x w red)
CA-contr-base-reduced-word ((x ′∷ w) , red) =
  (CA-e x _ ∘ ap CA-z (right-inverse-· x _))
  ∘ CA-contr-base-reduced-word (w , tail'-is-reduced x w red)

-- Then on every point
CA-contr-base : (u : FA) → P-CA-contr (CA-z u)
CA-contr-base u =
  ap CA-z (! (inv₂ u)) ∘ (CA-contr-base-reduced-word (freegroup-to-reduced u))

-- Now we prove that it’s true on paths, coming from reduced words
abstract
  CA-contr-loop-reduced-word : (t : A) (w : reduced-word) →
    (ap CA-z (reduced-to-freegroup-mul-reduce t w)
    ∘ ! (CA-e t (reduced-to-freegroup w)))
    ∘ (CA-contr-base-reduced-word w)
    ≡ CA-contr-base-reduced-word (mul-reduce t w)
  CA-contr-loop-reduced-word t (ε , red) = refl
  CA-contr-loop-reduced-word t ((x ∷ w) , red) = refl
  CA-contr-loop-reduced-word t ((x ′∷ w) , red) with (eq t x)
  CA-contr-loop-reduced-word x ((.x ′∷ w) , red) | inl refl =
    -- With the notations below, what we have to prove
    -- is [ (ap CA-z (! p) ∘ ! q) ∘ ((q ∘ ap CA-z p) ∘ r) ≡ r ]
    concat-assoc (ap CA-z (! p)) _ _
    ∘ (ap (λ t₁ → t₁ ∘ (! q ∘ ((q ∘ ap CA-z p) ∘ r))) (ap-opposite CA-z p)
    ∘ move!-right-on-left (ap CA-z p) (! q ∘ ((q ∘ ap CA-z p) ∘ r)) r
      (move!-right-on-left q ((q ∘ ap CA-z p) ∘ r) (ap CA-z p ∘ r)
      (concat-assoc q _ _))) where
    fw : FA
    fw = reduced-to-freegroup (w , tail'-is-reduced x w red)

    p : x · (x ⁻¹· fw) ≡ fw
    p = right-inverse-· x fw

    q : CA-z (x ⁻¹· fw) ≡ CA-z (x · (x ⁻¹· fw))
    q = CA-e x (x ⁻¹· fw)

    r : CA-z fw ≡ CA-z e
    r = CA-contr-base-reduced-word (w , tail'-is-reduced x w red)
  CA-contr-loop-reduced-word t ((x ′∷ w) , red) | inr different = refl

-- And finally for every path
CA-contr-loop : (t : A) (u : FA)
  → transport P-CA-contr (CA-e t u) (CA-contr-base u) ≡ (CA-contr-base (t · u))
CA-contr-loop t u =
  -- Idea:
  --
  -- We need to prove
  --   [p u ∘ (ap CA-z (q u) ∘ for-red u)
  --    ≡ ap CA-z (q (t · u)) ∘ for-red (t · u)]
  --
  -- [CA-contr-loop-reduced-word] gives
  -- that [(ap CA-z comp ∘ p (k u)) ∘ for-red u ≡ for-red (t · u)]

  trans-id≡cst (CA-e t u) (CA-contr-base u)
  ∘ (! (concat-assoc (p u) (ap CA-z (q u)) (for-red u))
  ∘ (whisker-right (for-red u) {q = p u ∘ ap CA-z (q u)}
       {r = ap CA-z (q (t · u)) ∘ (ap CA-z comp ∘ p (k u))}
    (! (homotopy-naturality f g p (q u))
    ∘ (whisker-right (p (k u)) {q = ap f (q u)}
         {r = ap CA-z (q (t · u)) ∘ ap CA-z comp}
      (ap-compose CA-z (λ u₁ → t · u₁) (q u)
      ∘ (ap (ap CA-z) (π₁ (freegroup-is-set _ _ _ _))
      ∘ ap-concat CA-z (q (t · u)) comp))
    ∘ concat-assoc (ap CA-z (q (t · u))) (ap CA-z comp) (p (k u))))
  ∘ (concat-assoc (ap CA-z (q (t · u))) (ap CA-z comp ∘ p (k u))
       (for-red u)
       ∘ whisker-left (ap CA-z (q (t · u)))
           auie))) where
  f : FA → tot-cover
  f u = CA-z (t · u)

  g : FA → tot-cover
  g u = CA-z u

  p : (u : FA) → f u ≡ g u
  p u = ! (CA-e t u)

  k : FA → FA
  k u = reduced-to-freegroup (freegroup-to-reduced u)

  q : (u : FA) → u ≡ k u
  q u = ! (inv₂ u)

  for-red : (u : FA) → CA-z (k u) ≡ CA-z e
  for-red u = CA-contr-base-reduced-word (freegroup-to-reduced u)

  comp : k (t · u) ≡ t · (k u)
  comp = reduced-to-freegroup-mul-reduce t (freegroup-to-reduced u)

  auie : (ap CA-z comp ∘ p (k u)) ∘ for-red u ≡ for-red (t · u)
  auie = CA-contr-loop-reduced-word t (freegroup-to-reduced u)

-- Hence, [CA] is contractible
CA-contr : (x : tot-cover) → P-CA-contr x
CA-contr = equivCA.CA-rec P-CA-contr CA-contr-base CA-contr-loop

abstract
  tot-cover-is-contr : is-contr tot-cover
  tot-cover-is-contr = (CA-z e , λ x → CA-contr x)

-- We define now a fiberwise map between the two fibrations [path-fib]
-- and [universal-cover]
fiberwise-map : (x : WA) → (path-fib x → universal-cover x)
fiberwise-map x q = transport universal-cover (! q) e

-- This induces an equivalence on the total spaces, because both total spaces
-- are contractible
total-equiv : is-equiv (total-map fiberwise-map)
total-equiv = contr-to-contr-is-equiv (total-map fiberwise-map)
                                      tot-path-fib-is-contr
                                      tot-cover-is-contr

-- Hence an equivalence fiberwise
fiberwise-map-is-equiv : (x : WA) → is-equiv (fiberwise-map x)
fiberwise-map-is-equiv x = fiberwise-is-equiv fiberwise-map total-equiv x

-- We can then conclude that the based loop space of the wedge of circles on [A]
-- is equivalent to the free group on [A], where [A] is any discrete set (i.e.
-- with decidable equality)
ΩWA≃FA : (baseWA ≡ baseWA) ≃ FA
ΩWA≃FA = (fiberwise-map baseWA , fiberwise-map-is-equiv baseWA)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

module Fragment.Equational.Theory.Bundles where

open import Fragment.Algebra.Signature
open import Fragment.Equational.Theory.Base
open import Fragment.Equational.Theory.Combinators

open import Data.Nat using (ℕ)

module _ where

  data MagmaOp : ℕ → Set where
    • : MagmaOp 2

  Σ-magma : Signature
  Σ-magma = record { ops = MagmaOp }

  import Fragment.Equational.Theory.Laws Σ-magma as L

  data MagmaEq : ℕ → Set where

  magma-eqs : ∀ {n} → MagmaEq n → Eq Σ-magma n
  magma-eqs ()

  data SemigroupEq : ℕ → Set where
    assoc : SemigroupEq 3

  semigroup-eqs : ∀ {n} → SemigroupEq n → Eq Σ-magma n
  semigroup-eqs assoc = L.assoc •

  data CSemigroupEq : ℕ → Set where
    comm  : CSemigroupEq 2
    assoc : CSemigroupEq 3

  csemigroup-eqs : ∀ {n} → CSemigroupEq n → Eq Σ-magma n
  csemigroup-eqs comm  = L.comm •
  csemigroup-eqs assoc = L.assoc •

Θ-magma : Theory
Θ-magma = record { Σ     = Σ-magma
                 ; eqs   = MagmaEq
                 ; _⟦_⟧ₑ = magma-eqs
                 }

Θ-semigroup : Theory
Θ-semigroup = record { Σ     = Σ-magma
                     ; eqs   = SemigroupEq
                     ; _⟦_⟧ₑ = semigroup-eqs
                     }

Θ-csemigroup : Theory
Θ-csemigroup = record { Σ     = Σ-magma
                      ; eqs   = CSemigroupEq
                      ; _⟦_⟧ₑ = csemigroup-eqs
                      }

Θ-monoid : Theory
Θ-monoid = AddId Θ-semigroup •

Θ-cmonoid : Theory
Θ-cmonoid = AddId Θ-csemigroup •

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Unary where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Classes
import Cubical.Foundations.Logic as L

open import Cubical.Data.Sigma
open import Cubical.Data.Empty using (⊥)
open import Cubical.Data.Sum.Base using (_⊎_; rec)
open import Cubical.Foundations.Function

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.Decidable using (IsYes)

private
  variable
    a b c ℓ ℓ₁ ℓ₂ : Level
    A : Type a
    B : Type b
    C : Type c

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

-- Unary relations are known as predicates and `Pred A ℓ` can be viewed
-- as some property that elements of type A might satisfy.

-- Consequently `P : Pred A ℓ` can also be seen as a subset of A
-- containing all the elements of A that satisfy property P. This view
-- informs much of the notation used below.

RawPred : Type a → (ℓ : Level) → Type _
RawPred A ℓ = A → Type ℓ

Pred : Type a → (ℓ : Level) → Type _
Pred A ℓ = A → hProp ℓ

isPropValued : RawPred A ℓ → Type _
isPropValued P = ∀ x → isProp (P x)

instance
  PredCast : Cast (Pred A ℓ) (RawPred A ℓ)
  PredCast = record { [_] = λ P x → P x .fst }

isProp[_] : (P : Pred A ℓ) → isPropValued [ P ]
isProp[ P ] x = P x .snd

fromRaw : (P : RawPred A ℓ) → isPropValued P → Pred A ℓ
fromRaw P isPropP x .fst = P x
fromRaw P isPropP x .snd = isPropP x

------------------------------------------------------------------------
-- Special sets

-- The empty set.

∅ : Pred A _
∅ _ = L.⊥

-- The singleton set.

｛_｝ : A → Pred A _
｛ x ｝ = L._≡ₚ x

-- The universal set.

U : Pred A _
U _ = L.⊤

open import Cubical.Data.Unit public using (tt)

------------------------------------------------------------------------
-- Membership

infix 6 _∈_ _∉_

_∈_ : A → Pred A ℓ → Type _
x ∈ P = ⟨ P x ⟩

_∉_ : A → Pred A ℓ → Type _
x ∉ P = ¬ x ∈ P

------------------------------------------------------------------------
-- Subset relations

infix 6 _⊆_ _⊇_ _⊈_ _⊉_ _⊂_ _⊃_ _⊄_ _⊅_

_⊆_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

_⊇_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⊇ Q = Q ⊆ P

_⊈_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⊈ Q = ¬ (P ⊆ Q)

_⊉_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⊉ Q = ¬ (P ⊇ Q)

_⊂_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⊂ Q = P ⊆ Q × Q ⊈ P

_⊃_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⊃ Q = Q ⊂ P

_⊄_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⊄ Q = ¬ (P ⊂ Q)

_⊅_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⊅ Q = ¬ (P ⊃ Q)

------------------------------------------------------------------------
-- Properties of sets

infix 10 Satisfiable Universal IUniversal

-- Emptiness - no element satisfies P.

Empty : Pred A ℓ → Type _
Empty P = ∀ x → x ∉ P

-- Satisfiable - at least one element satisfies P.

Satisfiable : Pred A ℓ → Type _
Satisfiable {A = A} P = ∃[ x ∈ A ] x ∈ P

syntax Satisfiable P = ∃⟨ P ⟩

-- Universality - all elements satisfy P.

Universal : Pred A ℓ → Type _
Universal P = ∀ x → x ∈ P

syntax Universal P = Π[ P ]

-- Implicit universality - all elements satisfy P.

IUniversal : Pred A ℓ → Type _
IUniversal P = ∀ {x} → x ∈ P

syntax IUniversal P = ∀[ P ]

-- Decidability - it is possible to determine if an arbitrary element
-- satisfies P.

Decidable : Pred A ℓ → Type _
Decidable P = ∀ x → Dec (x ∈ P)

-- Disjointness - Any element satifsying both P and Q is contradictory.

_⊃⊂_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
_⊃⊂_ P Q = ∀ {x} → x ∈ P → x ∈ Q → ⊥

-- Positive version of non-disjointness, dual to inclusion.

_≬_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
_≬_ {A = A} P Q = ∃[ x ∈ A ] x ∈ P × x ∈ Q

------------------------------------------------------------------------
-- Operations on sets

infix 10 ⋃ ⋂
infixr 9 _⊢_ _⊣_
infixr 8 _⇒_
infixr 7 _∩_
infixr 6 _∪_
infix 5 _≬_

-- Complement.

∁ : Pred A ℓ → Pred A ℓ
∁ P = λ x → L.¬ P x

-- Implication.

_⇒_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ⇒ Q = λ x → P x L.⇒ Q x

-- Union.

_∪_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ∪ Q = λ x → P x L.⊔ Q x

-- Intersection.

_∩_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ∩ Q = λ x → P x L.⊓ Q x

-- Infinitary union.

⋃ : ∀ {i} (I : Type i) → (I → Pred A ℓ) → Pred A _
⋃ I P = λ x → L.∃[ i ∶ I ] P i x

syntax ⋃ I (λ i → P) = ⋃[ i ∶ I ] P

-- Infinitary intersection.
⋂ : ∀ {i} (I : Type i) → (I → Pred A ℓ) → Pred A _
⋂ I P = λ x → ((i : I) → x ∈ P i) , isPropΠ λ i → isProp[ P i ] x

syntax ⋂ I (λ i → P) = ⋂[ i ∶ I ] P

-- Preimage.

_⊢_ : (A → B) → Pred B ℓ → Pred A ℓ
f ⊢ P = λ x → P (f x)

-- Image.

_⊣_ : (A → B) → Pred A ℓ → Pred B _
f ⊣ P = λ x → L.∥ Σ[ (y , _) ∈ Σ _ (_∈ P) ] (f y ≡ x) ∥ₚ

------------------------------------------------------------------------
-- Preservation under operations

_Preserves_⟶_ : (A → B) → Pred A ℓ₁ → Pred B ℓ₂ → Type _
f Preserves P ⟶ Q = P ⊆ f ⊢ Q

_Preserves_ : (A → A) → Pred A ℓ → Type _
f Preserves P = f Preserves P ⟶ P

-- A binary variant of _Preserves_⟶_.

_Preserves₂_⟶_⟶_ : (A → B → C) → Pred A ℓ₁ → Pred B ℓ₂ → Pred C ℓ → Type _
_∙_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y} → x ∈ P → y ∈ Q → x ∙ y ∈ R

_Preserves₂_ : (A → A → A) → Pred A ℓ → Type _
_∙_ Preserves₂ P = _∙_ Preserves₂ P ⟶ P ⟶ P

------------------------------------------------------------------------
-- Logical equivalence

infix 8 _⇔_ _⇚⇛_

_⇔_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⇔ Q = P ⊆ Q × P ⊇ Q

-- Direct logical equivalence (more useful for proofs)

_⇚⇛_ : Pred A ℓ₁ → Pred A ℓ₂ → Type _
P ⇚⇛ Q = ∀ x → x ∈ P ≃ x ∈ Q

module _ (P : Pred A ℓ₁) (Q : Pred A ℓ₂) where

  ⇔-⇚⇛ : P ⇔ Q → P ⇚⇛ Q
  ⇔-⇚⇛ (P⊆Q , Q⊆P) x = isPropEquiv→Equiv (P x .snd) (Q x .snd) P⊆Q Q⊆P

  ⇚⇛-⇔ : P ⇚⇛ Q → P ⇔ Q
  ⇚⇛-⇔ P⇚⇛Q = equivFun (P⇚⇛Q _) , invEq (P⇚⇛Q _)

  equiv≃ : P ⇔ Q ≃ P ⇚⇛ Q
  equiv≃ = isPropEquiv→Equiv (isProp× (isPropImplicitΠ λ _ → isPropΠ λ _ → (Q _ .snd)) (isPropImplicitΠ λ _ → isPropΠ λ _ → (P _ .snd)))
                              (isPropΠ λ _ → isPropΣ (isPropΠ λ _ → Q _ .snd) (λ _ → isPropIsEquiv _)) ⇔-⇚⇛ ⇚⇛-⇔

equiv≡ : _⇔_ ≡ _⇚⇛_ {ℓ₁} {A} {ℓ₂} {ℓ}
equiv≡ = funExt (λ P → funExt (λ Q → ua (equiv≃ P Q)))

module _ (P Q : Pred A ℓ) where

  ⇚⇛toPath : P ⇚⇛ Q → P ≡ Q
  ⇚⇛toPath P⇚⇛Q = funExt (λ x → L.hProp≡ (ua (P⇚⇛Q x)))

  ⇔toPath : P ⇔ Q → P ≡ Q
  ⇔toPath P⇔Q = ⇚⇛toPath (⇔-⇚⇛ P Q P⇔Q)

------------------------------------------------------------------------
-- Predicate combinators

-- These differ from the set operations above, as the carrier set of the
-- resulting predicates are not the same as the carrier set of the
-- component predicates.

infixr  2 _⟨×⟩_
infixr  2 _⟨⊙⟩_
infixr  1 _⟨⊎⟩_
infixr  0 _⟨→⟩_
infixl  9 _⟨·⟩_
infix  10 _~
infixr  9 _⟨∘⟩_
infixr  2 _//_ _\\_

-- Product.

_⟨×⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨×⟩ Q) (x , y) = P x L.⊓ Q y

-- Sum over one element.

_⟨⊎⟩_ : Pred A ℓ → Pred B ℓ → Pred (A ⊎ B) _
P ⟨⊎⟩ Q = rec P Q

-- Sum over two elements.

_⟨⊙⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨⊙⟩ Q) (x , y) = P x L.⊔ Q y

-- Implication.

_⟨→⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
(P ⟨→⟩ Q) f = (∀ {x} → x ∈ P → f x ∈ Q) , isPropImplicitΠ λ _ → isPropΠ
                                                          λ _ → isProp[ Q ] _

-- Product.

_⟨·⟩_ : (P : Pred A ℓ₁) (Q : Pred B ℓ₂) →
        (P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ uncurry (flip _$_) ⊢ Q
(P ⟨·⟩ Q) (p , f) = f p

-- Converse.

_~ : Pred (A × B) ℓ → Pred (B × A) ℓ
P ~ = P ∘ λ { (x , y) → y , x }

-- Composition.

_⟨∘⟩_ : Pred (A × B) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × C) _
_⟨∘⟩_ {B = B} P Q (x , z) = L.∃[ y ∶ B ] P (x , y) L.⊓ Q (y , z)

-- Post-division.

_//_ : Pred (A × C) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × B) _
(P // Q) (x , y) = (∀ {z} → (y , z) ∈ Q → (x , z) ∈ P) ,
                      isPropImplicitΠ λ _ → isPropΠ
                                      λ _ → isProp[ P ] _

-- Pre-division.

_\\_ : Pred (A × C) ℓ₁ → Pred (A × B) ℓ₂ → Pred (B × C) _
P \\ Q = (P ~ // Q ~) ~


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

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

module Logic.PropositionalLogicExamples where

emptySubset : {a : _} (A : Set a) → IsSubset False A
emptySubset A = record { ofElt = λ () }

emptyEntailment : {a b : _} {A : Set a} {P : Propositions A} → Entails (emptySubset (Propositions A)) P → Tautology P
emptyEntailment {a} {b} {A} {P} entails v = entails {v} λ {s} → exFalso s

emptyEntailment' : {a b : _} {A : Set a} {P : Propositions A} → Tautology P → Entails (emptySubset (Propositions A)) P
emptyEntailment' isTaut {v} _ = isTaut v

data TwoElements : Set where
  One : TwoElements
  Two : TwoElements

twoElementSubset : {a : _} {A : Set a} → {P Q R : Propositions A} → TwoElements → Propositions A
twoElementSubset {P = P} {Q} {R} One = implies P Q
twoElementSubset {P = P} {Q} {R} Two = implies Q R

twoElementSubsetInj : {a : _} {A : Set a} {P Q R : Propositions A} → (P ≡ Q → False) → Injection (twoElementSubset {P = P} {Q} {R})
twoElementSubsetInj {P = P} {Q} {R} p!=q {One} {One} refl = refl
twoElementSubsetInj {P = P} {Q} {R} p!=q {One} {Two} pr with impliesInjective pr
twoElementSubsetInj {P = P} {Q} {R} p!=q {One} {Two} pr | fst ,, snd = exFalso (p!=q fst)
twoElementSubsetInj {P = P} {Q} {R} p!=q {Two} {One} pr with impliesInjective pr
twoElementSubsetInj {P = P} {Q} {R} p!=q {Two} {One} pr | fst ,, snd = exFalso (p!=q (equalityCommutative fst))
twoElementSubsetInj {P = P} {Q} {R} p!=q {Two} {Two} refl = refl

badBool : BoolFalse ≡ BoolTrue → False
badBool ()

semanticEntailmentTransitive : {a : _} {A : Set a} {P Q R : Propositions A} → (p!=q : P ≡ Q → False) → Entails record { ofElt = twoElementSubset } (implies P R)
semanticEntailmentTransitive {P = P} {Q} {R} p!=q {v} pr with inspect (Valuation.v v P)
semanticEntailmentTransitive {P = P} {Q} {R} p!=q {v} pr | BoolTrue with≡ pT with inspect (Valuation.v v Q)
semanticEntailmentTransitive {P = P} {Q} {R} p!=q {v} pr | BoolTrue with≡ pT | BoolTrue with≡ qT with inspect (Valuation.v v R)
semanticEntailmentTransitive {P = P} {Q} {R} p!=q {v} pr | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolTrue with≡ rT = Valuation.vImplicationT v rT
semanticEntailmentTransitive {P = P} {Q} {R} p!=q {v} pr | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolFalse with≡ rF = exFalso (badBool (transitivity (equalityCommutative (Valuation.vImplicationF v qT rF)) (pr {Two})))
semanticEntailmentTransitive {P = P} {Q} {R} p!=q {v} pr | BoolTrue with≡ pT | BoolFalse with≡ qF = exFalso (badBool (transitivity (equalityCommutative (Valuation.vImplicationF v pT qF)) (pr {One})))
semanticEntailmentTransitive {P = P} {Q} {R} p!=q {v} pr | BoolFalse with≡ pF = Valuation.vImplicationVacuous v pF

-- Subset {p -> q, q -> r}
pQQR : {a : _} {A : Set a} {P Q R : Propositions A} → TwoElements → Propositions A
pQQR {P = P} {Q} {R} One = implies P Q
pQQR {P = P} {Q} {R} Two = implies Q R

pQQRSubsetInj : {a : _} {A : Set a} {P Q R : Propositions A} → (P ≡ Q → False) → Injection (pQQR {P = P} {Q} {R})
pQQRSubsetInj {P = P} {Q} {R} p!=q {One} {One} refl = refl
pQQRSubsetInj {P = P} {Q} {R} p!=q {One} {Two} pr with impliesInjective pr
pQQRSubsetInj {P = P} {Q} {R} p!=q {One} {Two} pr | p=q ,, _ = exFalso (p!=q p=q)
pQQRSubsetInj {P = P} {Q} {R} p!=q {Two} {One} pr with impliesInjective pr
pQQRSubsetInj {P = P} {Q} {R} p!=q {Two} {One} pr | q=p ,, _ = exFalso (p!=q (equalityCommutative q=p))
pQQRSubsetInj {P = P} {Q} {R} p!=q {Two} {Two} refl = refl

syntacticEntailmentExample : {a : _} {A : Set a} {P Q R : Propositions A} → (p!=q : P ≡ Q → False) → Proof propositionalAxioms (record { ofElt = pQQR {P = P} {Q} {R} }) 7
syntacticEntailmentExample {P = P} {Q} {R} p!=q = nextStep 6 (nextStep 5 (nextStep 4 (nextStep 3 (nextStep 2 (nextStep 1 (nextStep 0 empty (axiom (Two , record { one = P ; two = Q ; three = R }))) (given Two)) (axiom (One , ((implies Q R) ,, P)))) (modusPonens (record { element = implies (implies Q R) (implies P (implies Q R)) ; position = 0 ; pos<N = le 2 refl ; elementIsAt = refl }) (record { element = implies Q R ; position = 1 ; elementIsAt = refl ; pos<N = le 1 refl }) (implies P (implies Q R)) refl)) (modusPonens (record { element = implies (implies P (implies Q R)) (implies (implies P Q) (implies P R)) ; position = 3 ; pos<N = le 0 refl ; elementIsAt = refl }) (record { element = implies P (implies Q R) ; position = 0 ; pos<N = succIsPositive _ ; elementIsAt = refl }) (implies (implies P Q) (implies P R)) refl)) (given One)) (modusPonens (record { element = implies (implies P Q) (implies P R) ; position = 1 ; pos<N = succPreservesInequality (succIsPositive _) ; elementIsAt = refl }) (record { element = implies P Q ; position = 0 ; pos<N = succIsPositive _ ; elementIsAt = refl }) (implies P R) refl)

pQQRProof : {a : _} {A : Set a} {P Q R : Propositions A} → (p!=q : P ≡ Q → False) → Proves propositionalAxioms (record { ofElt = pQQR {P = P} {Q} {R} }) (implies P R)
pQQRProof p!=q = record { n = 6 ; proof = syntacticEntailmentExample p!=q ; ofStatement = refl }

-- Subset {p}
pSubset : {a : _} {A : Set a} {P : Propositions A} → True → Propositions A
pSubset {P = P} record {} = implies P P

pSubsetInj : {a : _} {A : Set a} {P : Propositions A} → Injection (pSubset {P = P})
pSubsetInj {P = P} {record {}} {record {}} refl = refl

syntacticEntailmentPP : {a : _} {A : Set a} {P : Propositions A} → Proof propositionalAxioms record { ofElt = pSubset {P = P} } 5
syntacticEntailmentPP {P = P} = nextStep 4 (nextStep 3 (nextStep 2 (nextStep 1 (nextStep 0 empty (axiom (One , (P ,, (implies P P))))) (axiom (Two , record { one = P ; two = implies P P ; three = P }))) (modusPonens (record { element = implies (implies P (implies (implies P P) P)) (implies (implies P (implies P P)) (implies P P)) ; position = 0 ; pos<N = succIsPositive _ ; elementIsAt = refl }) (record { element = implies P (implies (implies P P) P) ; position = 1 ; pos<N = succPreservesInequality (succIsPositive _) ; elementIsAt = refl }) (implies (implies P (implies P P)) (implies P P)) refl)) (axiom (One , (P ,, P)))) (modusPonens (record { element = implies (implies P (implies P P)) (implies P P) ; position = 1 ; pos<N = succPreservesInequality (succIsPositive _) ; elementIsAt = refl }) (record { element = implies P (implies P P) ; position = 0 ; pos<N = succIsPositive _ ; elementIsAt = refl }) (implies P P) refl)

pImpliesP : {a : _} {A : Set a} {P : Propositions A} → Proves propositionalAxioms record { ofElt = pSubset {P = P} } (implies P P)
Proves.n (pImpliesP {P = P}) = 4
Proves.proof (pImpliesP {P = P}) = syntacticEntailmentPP {P = P}
Proves.ofStatement (pImpliesP {P = P}) = refl


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

module IO.Exts where

import IO.Primitive as Prim
open import Class.Monad
open import Class.Functor
open import Data.List
open import Data.Nat using (ℕ)
open import Data.String
open import Data.Sum
open import Data.Unit
open import Function
open import IO using (IO; run; readFiniteFile; lift)
open import IO.Instance
open import Level

private
  variable
    A : Set

{-#
  FOREIGN GHC
  import Data.Text
  import System.CPUTime
  import System.Environment
  import System.Exit
  import System.IO
  import System.IO.Error
  import System.Process
#-}

postulate
  flushStdoutPrim : Prim.IO ⊤
  getCPUTimePrim : Prim.IO ℕ
  putStrErrPrim : String → Prim.IO ⊤
  runShellCmdPrim : String → List String → Prim.IO String
  catchIOErrorPrim : Prim.IO A → (String → Prim.IO A) → Prim.IO A

{-# COMPILE GHC flushStdoutPrim = hFlush stdout #-}
{-# COMPILE GHC getCPUTimePrim = getCPUTime #-}
{-# COMPILE GHC putStrErrPrim = hPutStr stderr . unpack #-}
{-# COMPILE GHC runShellCmdPrim = \ s t -> pack <$> (readProcess (unpack s) (fmap unpack t) "") #-} -- use haskell proc
{-# COMPILE GHC catchIOErrorPrim = \ _ a f -> catchIOError a (f . pack . show) #-}

flushStdout : IO ⊤
flushStdout = lift flushStdoutPrim

getCPUTime : IO ℕ
getCPUTime = lift getCPUTimePrim

putStrErr : String → IO ⊤
putStrErr s = lift (putStrErrPrim s)

runShellCmd : String → List String → IO String
runShellCmd s args = lift (runShellCmdPrim s args)

catchIOError : IO A → (String → IO A) → IO A
catchIOError a f = lift $ catchIOErrorPrim (run a) (run ∘ f)

readFiniteFileError : String → IO (String ⊎ String)
readFiniteFileError name =
  catchIOError (inj₂ <$> readFiniteFile name) (return ∘ inj₁)

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
{-# OPTIONS --no-qualified-instances #-}
open import Data.List
open import Relation.Unary
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax

import JVM.Printer.Printer as Printer
import JVM.Model as Model

module JVM.Syntax.Bytecode.Printer {ℓ T}
  (⟨_⇒_⟩ : T → T → List T → Set ℓ)
  (let open Model T)
  (let open Printer T)
  (print : ∀ {τ₁ τ₂} → ∀[ Down ⟨ τ₁ ⇒ τ₂ ⟩ ⇒ Printer Emp ] ) where

open import JVM.Syntax.Bytecode T ⟨_⇒_⟩
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Data.ReflexiveTransitive
open import Relation.Ternary.Monad

{-# TERMINATING #-}
pretty : ∀ {ψ₁ ψ₂} → ∀[ ⟪ ψ₁ ↝ ψ₂ ⟫ ⇒ Printer Emp ]
pretty nil      = do
  return refl
pretty (instr i   ▹⟨ σ ⟩ is) = do
  is          ← ✴-id⁻ʳ ⟨$⟩ (print i &⟨ ⟪ _ ↝ _ ⟫ # ∙-comm σ ⟩ is)
  pretty is
pretty (labeled l∙i ▹⟨ σ₂ ⟩ is) = do
  let l ∙⟨ σ ⟩ i∙is = ✴-assocᵣ (l∙i ∙⟨ σ₂ ⟩ is)
  i ∙⟨ σ ⟩ is       ← ✴-id⁻ʳ ⟨$⟩ (print-labels l &⟨ _ ✴ ⟪ _ ↝ _ ⟫ # ∙-comm σ ⟩ i∙is)
  is                ← ✴-id⁻ʳ ⟨$⟩ (print i        &⟨                 ∙-comm σ ⟩ is)
  pretty is


text:
-- Discrete category over a type A
-- A must be an h-groupoid for the homs to be sets
{-# OPTIONS --safe #-}

module Cubical.Categories.Instances.Discrete where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Functor.Base
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Transport

private
  variable
    ℓ ℓC ℓC' : Level

open Category

-- Discrete category
DiscreteCategory : hGroupoid ℓ → Category ℓ ℓ
DiscreteCategory A .ob = A .fst
DiscreteCategory A .Hom[_,_] a a' = a ≡ a'
DiscreteCategory A .id = refl
DiscreteCategory A ._⋆_ = _∙_
DiscreteCategory A .⋆IdL f = sym (lUnit f)
DiscreteCategory A .⋆IdR f = sym (rUnit f)
DiscreteCategory A .⋆Assoc f g h = sym (assoc f g h)
DiscreteCategory A .isSetHom {x} {y} = A .snd x y

module _ {A : hGroupoid ℓ}
         {C : Category ℓC ℓC'} where
  open Functor

  -- Functions f: A → ob C give functors F: DiscreteCategory A → C
  DiscFunc : (fst A → ob C) → Functor (DiscreteCategory A) C
  DiscFunc f .F-ob = f
  DiscFunc f .F-hom {x} p = subst (λ z → C [ f x , f z ]) p (id C)
  DiscFunc f .F-id {x} = substRefl {B = λ z → C [ f x , f z ]} (id C)

  -- Preserves composition
  DiscFunc f .F-seq {x} {y} p q =
      let open Category C using () renaming (_⋆_ to _●_) in

      let Hom[fx,f—] = (λ (w : A .fst) → C [ f x , f w ]) in
      let Hom[fy,f—] = (λ (w : A .fst) → C [ f y , f w ]) in
      let id-fx = id C {f x} in
      let id-fy = id C {f y} in
      let Fp = (subst Hom[fx,f—] (p) id-fx) in

      subst Hom[fx,f—] (p ∙ q) id-fx            ≡⟨ substComposite Hom[fx,f—] _ _ _ ⟩
      subst Hom[fx,f—] (q) (Fp)                 ≡⟨ cong (subst _ q) (sym (⋆IdR C _)) ⟩
      subst Hom[fx,f—] (q) (Fp ● id-fy)         ≡⟨ substCommSlice _ _ (λ _ → Fp ●_) q _ ⟩
      Fp ● (subst Hom[fy,f—] (q) id-fy)         ∎

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of Colist
------------------------------------------------------------------------

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

module Codata.Colist.Categorical where

open import Codata.Conat using (infinity)
open import Codata.Colist
open import Category.Functor
open import Category.Applicative

functor : ∀ {ℓ i} → RawFunctor {ℓ} (λ A → Colist A i)
functor = record { _<$>_ = map }

applicative : ∀ {ℓ i} → RawApplicative {ℓ} (λ A → Colist A i)
applicative = record
  { pure = replicate infinity
  ; _⊛_  = ap
  }


text:
-- Fixed on AIM XIV 2011-09-09 AA, UN
-- {-# OPTIONS -v tc.lhs.unify:50 #-}
module Issue292 where

data ⊥ : Set where

infix 3 ¬_

¬_ : Set → Set
¬ P = P → ⊥

infix 4 _≅_

data _≅_ {A : Set} (x : A) : ∀ {B : Set} → B → Set where
  refl : x ≅ x

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

data Bool : Set where true false : Bool

data D : Bool -> Set where
  tt : D true
  ff : D false

P : Set -> Set
P S = Σ S (\s → s ≅ tt)

pbool : P (D true)
pbool = tt , refl

¬pbool2 : ¬ P (D false)
¬pbool2 ( ff , () )
-- Andreas, 2011-09-13 fix of fix: should work again
{- WAS: expected error
ff ≅ tt should be empty, but that's not obvious to me
when checking that the clause ¬pbool2 (ff , ()) has type
¬ P (D false)
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Bicategory.Helpers where

-- quite a bit of the code below is taken from Categories.2-Category
open import Data.Nat using (_+_)
open import Function using (flip)
open import Data.Product using (_,_; curry)

open import Categories.Category
open import Categories.Categories using (Categories)
import Categories.Functor
open import Categories.Terminal using (OneC; One; unit)
open import Categories.Object.Terminal using (module Terminal)
open import Categories.Bifunctor hiding (identityˡ; identityʳ; assoc) renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_)
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation using (NaturalTransformation) renaming (_≡_ to _≡ⁿ_; id to idⁿ)
open import Categories.Product using (Product; assocʳ; πˡ; πʳ)

module BicategoryHelperFunctors {o ℓ t e} (Obj : Set o) (_⇒_ : (A B : Obj) → Category ℓ t e)
    (—⊗— : {A B C : Obj} → Bifunctor (B ⇒ C) (A ⇒ B) (A ⇒ C))
    (id : {A : Obj} → Functor {ℓ} {t} {e} OneC (A ⇒ A)) where

  open Terminal (One {ℓ} {t} {e})

  _∘_ : {A B C : Obj} {L R : Category ℓ t e} → Functor L (B ⇒ C) → Functor R (A ⇒ B) → Bifunctor L R (A ⇒ C)
  _∘_ {A} {B} {C} F G = reduce-× {D₁ = B ⇒ C} {D₂ = A ⇒ B} —⊗— F G

  -- convenience!
  module _⇒_ (A B : Obj) = Category (A ⇒ B)
  open _⇒_ public using () renaming (Obj to _⇒₁_)

  private module imp⇒ {X Y : Obj} = Category (X ⇒ Y)
  open imp⇒ public using () renaming (_⇒_ to _⇒₂_; id to id₂; _∘_ to _•_; _≡_ to _≡₂_)

  id₁ : ∀ {A} → A ⇒₁ A
  id₁ {A} = Functor.F₀ (id {A}) unit

  id₁₂ : ∀ {A} → id₁ {A} ⇒₂ id₁ {A}
  id₁₂ {A} = id₂ {A = id₁ {A}}

  infixr 9 _∘₁_
  _∘₁_ : ∀ {A B C} → B ⇒₁ C → A ⇒₁ B → A ⇒₁ C
  _∘₁_ = curry (Functor.F₀ —⊗—)

  -- horizontal composition
  infixr 9 _∘₂_
  _∘₂_ : ∀ {A B C} {g g′ : B ⇒₁ C} {f f′ : A ⇒₁ B} (β : g ⇒₂ g′) (α : f ⇒₂ f′) → (g ∘₁ f) ⇒₂ (g′ ∘₁ f′)
  _∘₂_ = curry (Functor.F₁ —⊗—)

  -- left whiskering
  infixl 9 _◃_
  _◃_ : ∀ {A B C} {g g′ : B ⇒₁ C} → g ⇒₂ g′ → (f : A ⇒₁ B) → (g ∘₁ f) ⇒₂ (g′ ∘₁ f)
  β ◃ f = β ∘₂ id₂

  -- right whiskering
  infixr 9 _▹_
  _▹_ : ∀ {A B C} (g : B ⇒₁ C) → {f f′ : A ⇒₁ B} → f ⇒₂ f′ → (g ∘₁ f) ⇒₂ (g ∘₁ f′)
  g ▹ α = id₂ ∘₂ α

  module Coherence
      (identityˡ : {A B : Obj} → NaturalIsomorphism  (id ∘ idF {C = A ⇒ B}) (πʳ {C = ⊤} {A ⇒ B}))
      (identityʳ : {A B : Obj} → NaturalIsomorphism (idF {C = A ⇒ B} ∘ id) (πˡ {C = A ⇒ B}))
      (assoc : {A B C D : Obj} → NaturalIsomorphism  (idF ∘ —⊗—) ((—⊗— ∘ idF) ∘F assocʳ (C ⇒ D) (B ⇒ C) (A ⇒ B)) ) where

    open Categories.NaturalTransformation.NaturalTransformation

     -- left/right are inverted between in certain situations!
    -- private so as to not clash with the ones in Bicategory itself
    private
      ρᵤ : {A B : Obj} (f : A ⇒₁ B) → (id₁ ∘₁ f) ⇒₂ f
      ρᵤ f = η (NaturalIsomorphism.F⇒G identityˡ) (unit , f)

      λᵤ : {A B : Obj} (f : A ⇒₁ B) → (f ∘₁ id₁) ⇒₂ f
      λᵤ f = η (NaturalIsomorphism.F⇒G identityʳ) (f , unit)

      α : {A B C D : Obj} (f : A ⇒₁ B) (g : B ⇒₁ C) (h : C ⇒₁ D) →
          (h ∘₁ (g ∘₁ f)) ⇒₂ ((h ∘₁ g) ∘₁ f)
      α f g h = η (NaturalIsomorphism.F⇒G assoc) (h , g , f)

    -- Triangle identity.  Look how closely it matches with the one on
    -- http://ncatlab.org/nlab/show/bicategory
    Triangle : {A B C : Obj} (f : A ⇒₁ B) (g : B ⇒₁ C) → Set e
    Triangle f g = (g ▹ ρᵤ f) ≡₂ ((λᵤ g ◃ f) • (α f id₁ g))

    -- Pentagon identity.  Ditto.
    Pentagon : {A B C D E : Obj} (f : A ⇒₁ B) (g : B ⇒₁ C) (h : C ⇒₁ D) (i : D ⇒₁ E) → Set e
    Pentagon f g h i = ((α g h i ◃ f) • (α f (h ∘₁ g) i)) • (i ▹ α f g h) ≡₂ (α f g (i ∘₁ h) • α (g ∘₁ f) h i)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
-- Andreas, 2015-08-11, issue reported by Martin Stone Davis

-- {-# OPTIONS -v impossible:10 -v interaction.give:20 #-}

open import Data.AVL using (Tree; empty)
open import Data.Vec using (Vec)
open import Data.String using (String)
open import Relation.Binary using (StrictTotalOrder)
open import Data.Nat.Properties using (<-strictTotalOrder)

empty' : Tree (StrictTotalOrder.isStrictTotalOrder <-strictTotalOrder) (Vec String)
empty' = empty {!!}

-- ERROR WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Monad/Trace.hs:56

-- Currently Agsy gives nothing, which is also a weird.
-- It does not report "No solutions found".
-- Somehow, some parts of the solution are not in scope, which might
-- give an internal error that is caught, causing Agsy to discard
-- the solution.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.Network      as Network
import      LibraBFT.Impl.Consensus.RoundManager as RoundManager
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Prelude

-- This module defines the handler for our implementation.  For most message types, it does some
-- initial validation before passing the message on to the proper handlers.

module LibraBFT.Impl.IO.OBM.InputOutputHandlers where

epvv : LBFT (Epoch × ValidatorVerifier)
epvv = _,_ <$> gets (_^∙ rmSafetyRules ∙ srPersistentStorage ∙ pssSafetyData ∙ sdEpoch)
           <*> gets (_^∙ rmEpochState ∙ esVerifier)

module handleProposal (now : Instant) (pm : ProposalMsg) where
  step₀ : LBFT Unit
  step₁ : Epoch → ValidatorVerifier → LBFT Unit

  step₀ = do
    (myEpoch , vv) ← epvv
    step₁ myEpoch vv

  step₁ myEpoch vv = do
    case⊎D Network.processProposal {- {!!} -} pm myEpoch vv of λ where
      (Left (Left e))  → logErr e
      (Left (Right i)) → logInfo i
      (Right _)        → RoundManager.processProposalMsgM now pm

handleProposal : Instant → ProposalMsg → LBFT Unit
handleProposal = handleProposal.step₀

module handleVote (now : Instant) (vm : VoteMsg) where
  step₀ : LBFT Unit
  step₁ : Epoch → ValidatorVerifier → LBFT Unit

  step₀ = do
    (myEpoch , vv) ← epvv
    step₁ myEpoch vv

  step₁ myEpoch vv = do
    case Network.processVote vm myEpoch vv of λ where
      (Left (Left e))  → logErr e
      (Left (Right i)) → logInfo i
      (Right _)        → RoundManager.processVoteMsgM now vm

abstract
  handleVote = handleVote.step₀

  handleVote≡ : handleVote ≡ handleVote.step₀
  handleVote≡ = refl

handle : NodeId → NetworkMsg → Instant → LBFT Unit
handle _self msg now =
  case msg of λ where
    (P pm) → handleProposal now pm
    (V vm) → handleVote     now vm
    (C cm) → pure unit    -- We don't do anything with commit messages, they are just for defining Correctness.


text:
module DivMod where

-- From examples/simple-lib
open import Lib.Vec
open import Lib.Nat
open import Lib.Id
open import Lib.Logic
open import Lib.Fin

-- Certified implementation of division and modulo
module Direct where

  data DivMod : Nat -> Nat -> Set where
    dm : forall {b} q (r : Fin b) -> DivMod (toNat r + q * b) b

  getQ : forall {a b} -> DivMod a b -> Nat
  getQ (dm q _) = q

  getR : forall {a b} -> DivMod a b -> Nat
  getR (dm _ r) = toNat r

  divModˢ : (a b : Nat) -> DivMod a (suc b)
  divModˢ zero    b = dm 0 zero
  divModˢ (suc a) b with divModˢ a b
  divModˢ (suc ._) b | dm q r with maxView r
  divModˢ (suc ._) b | dm q .(fromNat b) | theMax
    with toNat (fromNat b) | lem-toNat-fromNat b
  ...  | .b | refl = dm {suc b} (suc q) zero
  divModˢ (suc ._) b | dm q .(weaken i)  | notMax i
    with toNat (weaken i) | lem-toNat-weaken i
  ...  | .(toNat i) | refl = dm q (suc i)

  divMod : (a b : Nat){nz : NonZero b} -> DivMod a b
  divMod a zero {}
  divMod a (suc b) = divModˢ a b

-- Let's try the inductive version. Less obvious that this one is correct.
module Inductive where

  data DivMod : Nat -> Nat -> Set where
    dmZ : forall {b} (i : Fin b) -> DivMod (toNat i) b
    dmS : forall {a b} -> DivMod a b -> DivMod (b + a) b

  getQ : forall {a b} -> DivMod a b -> Nat
  getQ (dmZ _) = 0
  getQ (dmS d) = suc (getQ d)

  getR : forall {a b} -> DivMod a b -> Nat
  getR (dmZ r) = toNat r
  getR (dmS d) = getR d

  data BoundView (n : Nat) : Nat -> Set where
    below : (i : Fin n) -> BoundView n (toNat i)
    above : forall a    -> BoundView n (n + a)

  boundView : (a b : Nat) -> BoundView a b
  boundView zero b = above b
  boundView (suc a) zero    = below zero
  boundView (suc a) (suc b) with boundView a b
  boundView (suc a) (suc .(toNat i)) | below i = below (suc i)
  boundView (suc a) (suc .(a + k))   | above k = above k

  data _≤_ : Nat -> Nat -> Set where
    leqZ : forall {n}            -> zero  ≤ n
    leqS : forall {n m} -> n ≤ m -> suc n ≤ suc m

  ≤-suc : forall {a b} -> a ≤ b -> a ≤ suc b
  ≤-suc leqZ     = leqZ
  ≤-suc (leqS p) = leqS (≤-suc p)

  plus-≤ : forall a {b c} -> a + b ≤ c -> b ≤ c
  plus-≤ zero    p        = p
  plus-≤ (suc a) (leqS p) = ≤-suc (plus-≤ a p)

  ≤-refl : forall {a} -> a ≤ a
  ≤-refl {zero} = leqZ
  ≤-refl {suc n} = leqS ≤-refl

  -- Recursion over a bound on a (needed for termination).
  divModˢ : forall {size} a b -> a ≤ size -> DivMod a (suc b)
  divModˢ a b prf with boundView (suc b) a
  divModˢ .(toNat r)   b _          | below r = dmZ r
  divModˢ .(suc b + k) b (leqS prf) | above k = dmS (divModˢ k b (plus-≤ b prf))

  divMod : forall a b {nz : NonZero b} -> DivMod a b
  divMod a zero {}
  divMod a (suc b) = divModˢ a b ≤-refl

  -- We ought to prove that the inductive version behaves the same as the
  -- direct version... but that's more work than we're willing to spend.

open Inductive

_div_ : (a b : Nat){nz : NonZero b} -> Nat
_div_ a b {nz} = getQ (divMod a b {nz})

_mod_ : (a b : Nat){nz : NonZero b} -> Nat
_mod_ a b {nz} = getR (divMod a b {nz})

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS -v 2 #-}
module Leftovers.Junk where

open import Data.Bool
open import Relation.Binary.PropositionalEquality

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

the : ∀ X → X → X
the X = id {X}

badEq :
  let f = the (Bool -> Bool -> Bool) (λ x → λ {true → false ; false → true})
  in f true ≡ f false
badEq = {!!} -- refl does not typecheck

goodEq :
  let f = the (Bool -> Bool -> Bool) (λ x → id λ {true → false ; false → true})
  in f true ≡ f false
goodEq = {!!}

max_stars_repo_name: JoeyEremondi/AgdaLeftovers

max_issues_repo_name: JoeyEremondi/AgdaLeftovers

max_forks_repo_name: JoeyEremondi/AgdaLeftovers


text:
module Integer.Difference.Properties where

open import Data.Product as Σ
open import Data.Product.Relation.Pointwise.NonDependent
open import Data.Unit
open import Equality
open import Integer.Difference
open import Natural as ℕ using (ℕ; zero; suc)
open import Quotient as /
open import Relation.Binary
open import Syntax

open Equality.FunctionProperties

+-comm : Commutative {A = ℤ} _+_
+-comm =
  ⟦⟧-≗₂ uip _ _ λ where
    (a – b) (c – d) →
      cong ⟦_⟧ (cong₂ _–_ (⟨ ℕ.+-comm a c ⟩) (⟨ ℕ.+-comm d b ⟩))

+-identityˡ : LeftIdentity {A = ℤ} 0 _+_
+-identityˡ =
  ⟦⟧-≗ uip _ _ λ where
    (a – b) →
      cong (λ z → ⟦ a – z ⟧) ⟨ ℕ.+-identityʳ b ⟩

+-identityʳ : RightIdentity {A = ℤ} 0 _+_
+-identityʳ =
  ⟦⟧-≗ uip _ _ λ where
    (a – b) →
      cong (λ z → ⟦ z – b ⟧) ⟨ ℕ.+-identityʳ a ⟩

+-assoc : Associative {A = ℤ} _+_
+-assoc =
  ⟦⟧-≗₃ uip _ _
    λ where
      (a – b) (c – d) (e – f) →
        cong ⟦_⟧ (cong₂ _–_ (sym (ℕ.+-assoc a _ _)) (ℕ.+-assoc f _ _))


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

open import Base
open import Homotopy.PullbackDef

-- We only consider the universal property internally to a fixed
-- universe [Set i]. If we don’t, we would have to consider an universe
-- polymorphic [P] and I don’t want to quantify over universe polymorphic things
module Homotopy.PullbackUP {i} (d : pullback-diag i)
  (P : Set i → Set i) ⦃ PA : P (pullback-diag.A d) ⦄
  ⦃ PB : P (pullback-diag.B d) ⦄ ⦃ PC : P (pullback-diag.C d) ⦄ where

open pullback-diag d

record cone (top : Set i) : Set i where
  constructor _,_,_
  field
    top→A : top → A
    top→B : top → B
    h : (t : top) → f (top→A t) ≡ g (top→B t)

top→D : (top : Set i) → pullback-diag i
top→D top = diag (top → A), (top → B), (top → C), (λ h → f ◯ h), (λ h → g ◯ h)

pullback-to-cone : (top : Set i) → (pullback (top→D top) → cone top)
pullback-to-cone top (top→A , top→B , h) = (top→A , top→B , happly h)

cone-to-pullback : (top : Set i) → (cone top → pullback (top→D top))
cone-to-pullback top (a , b , h) = (a , b , funext h)

pullback-to-cone-equiv : (top : Set i) → is-equiv (pullback-to-cone top)
pullback-to-cone-equiv top = iso-is-eq _ (cone-to-pullback top)
  (λ y → ap (λ u → _ , _ , u) (happly-funext _))
  (λ x → ap (λ u → _ , _ , u) (funext-happly _))

cone-to-pullback-equiv : (top : Set i) → is-equiv (cone-to-pullback top)
cone-to-pullback-equiv top = iso-is-eq _ (pullback-to-cone top)
  (λ x → ap (λ u → _ , _ , u) (funext-happly _))
  (λ y → ap (λ u → _ , _ , u) (happly-funext _))

compose-cone-map : (D E : Set i) (Dcone : cone D)
  → ((f : E → D) → cone E)
compose-cone-map D E (top→A , top→B , h) f =
  ((top→A ◯ f) , (top→B ◯ f) , λ x → h (f x))

is-pullback : (D : Set i) ⦃ PD : P D ⦄ (Dcone : cone D) → Set _
is-pullback D Dcone = (E : Set i) ⦃ PE : P E ⦄
                        → is-equiv (compose-cone-map D E Dcone)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda