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

module MoreLogic.Properties where -- hProp logic

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Data.Sigma renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Function.Base using (_∋_)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) renaming (⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.HITs.PropositionalTruncation.Base -- ∣_∣

import Cubical.Data.Empty as Empty
open import Cubical.Data.Unit.Base

open import Utils

-- lifted versions of ⊥ and ⊤

open import MoreLogic.Reasoning
open import MoreLogic.Definitions

isProp⊤ : isProp [ ⊤ ]
isProp⊤ tt tt = refl

symₚ : ∀{ℓ} → {A : Type ℓ} {x y : A} → [ x ≡ₚ y ] → [ y ≡ₚ x ]
symₚ {x = x} x≡y = substₚ (λ p → p ≡ₚ x) x≡y ∣ refl ∣

⊔-identityˡ-↑ : (P : hProp ℓ) → ⊥↑ {ℓ} ⊔ P ≡ P
⊔-identityˡ-↑ P =
  ⇒∶ (⊔-elim ⊥↑ P (λ _ → P) (λ ()) (λ x → x))
  ⇐∶ inrᵖ

⊔-identityʳ-↑ : (P : hProp ℓ) → P ⊔ ⊥↑ {ℓ} ≡ P
⊔-identityʳ-↑ P = ⇔toPath (⊔-elim P ⊥↑ (λ _ → P) (λ x → x) λ ()) inlᵖ

⊓-identityˡ-↑ : (P : hProp ℓ) → ⊤↑ {ℓ} ⊓ P ≡ P
⊓-identityˡ-↑ _ = ⇔toPath snd  λ x → lift tt , x

⊓-identityʳ-↑ : (P : hProp ℓ) → P ⊓ ⊤↑ {ℓ} ≡ P
⊓-identityʳ-↑ _ = ⇔toPath fst λ x → x , lift tt

¬↑≡¬ : ∀{ℓ} → {P : hProp ℓ} → (¬↑ P) ≡ (¬ P)
¬↑≡¬ =
 ⇒∶ (λ ¬↑P P → lower (¬↑P P))
 ⇐∶ (λ  ¬P P → lift  ( ¬P P))

¬¬-introᵗ : (P : Type ℓ) → P → ¬ᵗ ¬ᵗ P
¬¬-introᵗ _ p ¬p = ¬p p

¬¬-elimᵗ : (P : Type ℓ) → ¬ᵗ ¬ᵗ ¬ᵗ P → ¬ᵗ P
¬¬-elimᵗ _ ¬¬¬p p = ¬¬¬p (λ ¬p → ¬p p)

¬¬-intro : (P : hProp ℓ) → [ P ] → [ ¬ ¬ P ]
¬¬-intro _ p ¬p = ¬p p

¬¬-elim : (P : hProp ℓ) → [ ¬ ¬ ¬ P ] → [ ¬ P ]
¬¬-elim _ ¬¬¬p p = ¬¬¬p (λ ¬p → ¬p p)

¬¬-involutive : (P : hProp ℓ) → [ ¬ ¬ ¬ P ⇔ ¬ P ]
¬¬-involutive P .fst = ¬¬-elim     P
¬¬-involutive P .snd = ¬¬-intro (¬ P)

⇔toPath' : ∀{ℓ} {P Q : hProp ℓ} → [ P ⇔ Q ] → P ≡ Q
⇔toPath' = uncurry ⇔toPath

pathTo⇔ : ∀{ℓ} {P Q : hProp ℓ} → P ≡ Q → [ P ⇔ Q ]
pathTo⇔ p≡q = (pathTo⇒ p≡q , pathTo⇐ p≡q)

⊓⇔⊓ : ∀{ℓ ℓ' ℓ'' ℓ'''} {P : hProp ℓ} {Q : hProp ℓ'} {R : hProp ℓ''} {S : hProp ℓ'''}
   → [ (P ⇔ R) ⊓ (Q ⇔ S) ] → [ (P ⊓ Q) ⇔ (R ⊓ S) ]
⊓⇔⊓ (p⇔r , q⇔s) .fst (p , q) = p⇔r .fst p , q⇔s .fst q
⊓⇔⊓ (p⇔r , q⇔s) .snd (r , s) = p⇔r .snd r , q⇔s .snd s

⊓≡⊓ : ∀{ℓ} {P Q R S : hProp ℓ} → P ≡ R → Q ≡ S → (P ⊓ Q) ≡ (R ⊓ S)
⊓≡⊓ p≡r q≡s i = p≡r i ⊓ q≡s i

[path]To⇒ : (P Q : hProp ℓ) → [ P ] ≡ [ Q ] → [ P ⇒ Q ]
[path]To⇒ P Q [P]≡[Q] p = transport [P]≡[Q] p

[path]To⇐ : (P Q : hProp ℓ) → [ P ] ≡ [ Q ] → [ Q ⇒ P ]
[path]To⇐ P Q [P]≡[Q] q = transport (sym [P]≡[Q]) q

¬¬-involutiveᵗ : (A : Type ℓ) → (¬ᵗ ¬ᵗ ¬ᵗ A) ≡ (¬ᵗ A)
abstract
  ¬¬-involutiveᵗ A = isoToPath λ where
    .Iso.fun      ¬¬¬a a → ¬¬¬a (λ ¬a → ¬a a)
    .Iso.inv      ¬a ¬¬a → ¬¬a ¬a
    .Iso.rightInv ¬a     → refl
    -- the following proof is `... ≡ ¬¬¬a` and uses funext to reduce this to a proof `∀ x → ... x ≡ ¬¬¬a x`
    -- but this does not matter, since we have `¬¬¬a x` which is `⊥` and then we can use ⊥-elim to obtain whatever is necessary
    -- `⊥-elim` needed a detailed hint what to produce and this might not be the most elegant way to proof this
    .Iso.leftInv  ¬¬¬a   →
      funExt {A = (¬ᵗ ¬ᵗ A)} {B = λ _ i → ⊥⊥} {f = (λ ¬¬a → ¬¬a (λ a → ¬¬¬a (λ ¬a → ¬a a)))} {g = ¬¬¬a}
             (λ x → ⊥-elim {A = λ _ → (x (λ a → ¬¬¬a (λ ¬a → ¬a a)) ≡ ¬¬¬a x)} (¬¬¬a x))

-- taken from https://ncatlab.org/nlab/show/excluded+middle#DoubleNegatedPEM
-- Double-negated PEM
weak-LEM : ∀(P : hProp ℓ) → [ ¬ ¬ (P ⊔ ¬ P) ]
weak-LEM _ ¬[p⊔¬p] = ¬[p⊔¬p] (inrᵖ (λ p → ¬[p⊔¬p] (inlᵖ p)))

weak-LEMᵗ : ∀(P : Type ℓ) → ¬ᵗ ¬ᵗ (P ⊎ (¬ᵗ P))
weak-LEMᵗ _ ¬[p⊔¬p] = ¬[p⊔¬p] (inr (λ p → ¬[p⊔¬p] (inl p)))

⊤-introᵖ : {P : hProp ℓ} → [ P ] → P ≡ ⊤↑
⊤-introᵖ {ℓ = ℓ} {P = P} p = let
  P⇔⊤↑ : [ P ⇔ ⊤↑ {ℓ} ]
  P⇔⊤↑ = (λ _ → lift tt) , (λ _ → p)
  in ⇔toPath (fst P⇔⊤↑) (snd P⇔⊤↑)

⊤-elimᵖ : {P : hProp ℓ} → P ≡ ⊤↑ → [ P ]
⊤-elimᵖ {ℓ = ℓ} {P = P} p≡⊤ = (
  [ ⊤↑ {ℓ} ] ⇒⟨ transport ( λ i → [ p≡⊤ (~ i) ]) ⟩
  [ P      ] ◼) (lift tt)

contraposition : (P : hProp ℓ) (Q : hProp ℓ') → [ P ⇒ Q ] → [ ¬ Q ⇒ ¬ P ]
contraposition P Q f ¬q p = ⊥-elim (¬q (f p))

instance≡ : ∀{ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → ({{x : A}} → B x) ≡ ((x : A) → B x)
instance≡ = isoToPath (iso (λ f a → f {{a}}) (λ f {{a}} → f a) (λ f i → f) (λ f i → f))

implicit≡ : ∀{ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → ({x : A} → B x) ≡ ((x : A) → B x)
implicit≡ = isoToPath (iso (λ f a → f {a}) (λ f {a} → f a) (λ f i → f) (λ f i → f))

instanceFunExt : {A : Type ℓ} {B : A → I → Type ℓ'}
                 {f : {{x : A}} → B x i0} {g : {{x : A}} → B x i1}
               → ({{x : A}} → PathP (B x) (f {{x}}) (g {{x}}))
               → PathP (λ i → {{x : A}} → B x i) f g
instanceFunExt p i {{x}} = p {{x}} i

funExt-⊥ : {A : Type ℓ} (f g : A → Empty.⊥) → f ≡ g
funExt-⊥ f g = funExt (λ x → ⊥-elim {A = λ _ →  f x ≡ g x} (f x)) -- ⊥-elim needed a hint here

-- uncurry-preserves-≡
--   : {A : Type ℓ} {B : A → Type ℓ'} {C : (a : A) → B a → Type ℓ''}
--   → (f : (a : A) → (b : B a) → C a b)
--   -------------------------------------------------------------
--   → ∀ a b → f a b ≡ (uncurry f) (a , b)
-- uncurry-preserves-≡ f a b = refl

Σ-preserves-≡ :
      {A : Type ℓ}
      {B : A → Type ℓ'}
      {C : (a : A) → (b : B a) → Type ℓ''}
      {f g : ((a , b) : Σ A B) → C a b}
    → ((a : A) (b : B a) → (f (a , b)) ≡ (g (a , b)))
    → ((ab : Σ A B)      → (f   ab   ) ≡ (g   (ab) ))
Σ-preserves-≡ p (a , b) = p a b

Σ-reflects-≡ :
      {A : Type ℓ}
      {B : A → Type ℓ'}
      {a b : Σ A B}
    → a ≡ b
    → Σ[ p ∈ (fst a ≡ fst b) ] transport (λ i → B (p i)) (snd a) ≡ snd b
    --  Σ[ q ∈ (fst a ≡ fst b) ] (PathP (λ i → B (q i)) (snd a) (snd b))
Σ-reflects-≡ a≡b with PathΣ→ΣPathTransport _ _ a≡b
... | fst≡fst , snd≡snd = fst≡fst , snd≡snd

uncurry-reflects-≡
  : {A : Type ℓ} {B : A → Type ℓ'} {C : (a : A) → B a → Type ℓ''}
  → (f g : (a : A) → (b : B a) → C a b)
  -------------------------------------------------------------
  → (uncurry f ≡ uncurry g) → f ≡ g
uncurry-reflects-≡ f g p = funExt (λ x →
  f x                         ≡⟨ refl ⟩
  (λ y → (uncurry f) (x , y)) ≡⟨ ( λ i → λ y → (p i) (x , y)) ⟩
  (λ y → (uncurry g) (x , y)) ≡⟨ refl ⟩
  g x                         ∎)

-- "constant" version of funExt
funExt₂ᶜ :
      {A : Type ℓ}
      {B : A → Type ℓ'}
      {C : (a : A) → (b : B a) → Type ℓ''}
      {f g : (a : A) → (b : B a) → C a b}
      → ((a : A) → (b : B a) → (f a b) ≡ (g a b)) → f ≡ g
funExt₂ᶜ {A = A} {B = B} {C = C} {f = f} {g = g} = (
 ((a : A) (b : B a) → (         f   a   b)  ≡ (         g   a   b) ) ⇒⟨ (λ z → z) ⟩ -- holds definitionally
 ((a : A) (b : B a) → ((uncurry f) (a , b)) ≡ ((uncurry g) (a , b))) ⇒⟨ Σ-preserves-≡ ⟩
 ((ab : Σ A B)      → ((uncurry f)   ab   ) ≡ ((uncurry g) ( ab  ))) ⇒⟨ funExt ⟩
                       (uncurry f)          ≡  (uncurry g)           ⇒⟨ uncurry-reflects-≡ f g ⟩
                                f           ≡           g            ◼)

funExt-⊥₂ : {A B : Type ℓ} (f g : A → B → Empty.⊥) → f ≡ g
funExt-⊥₂ f g =  funExt₂ᶜ λ a b → ⊥-elim {A = λ _ → f a b ≡ g a b} (g a b)

-- weak deMorgan laws: only these three hold without further assumptions

deMorgan₂ : (P : hProp ℓ) (Q : hProp ℓ') → [ ¬ (P ⊔ Q) ] → [ ¬ P ⊓ ¬ Q ]
abstract deMorgan₂ P Q ¬[p⊔q] = (λ p →  ⊥-elim (¬[p⊔q] (inlᵖ p))) , λ q → ⊥-elim (¬[p⊔q] (inrᵖ q))

deMorgan₂-back : (P : hProp ℓ) (Q : hProp ℓ') → [ ¬ P ⊓ ¬ Q ] → [ ¬ (P ⊔ Q) ]
abstract deMorgan₂-back P Q (¬p , ¬q) p⊔q = ⊔-elim P Q (λ p⊔q → ⊥) ¬p ¬q p⊔q

deMorgan₁-back : (P : hProp ℓ) (Q : hProp ℓ') → [ ¬ P ⊔ ¬ Q ] → [ ¬ (P ⊓ Q) ]
abstract deMorgan₁-back {ℓ = ℓ} P Q [¬p⊔¬q] (p , q) = ⊔-elim (¬ P) (¬ Q) (λ [¬p⊔¬q] → ⊥) (λ ¬p → ¬p p) (λ ¬q → ¬q q) [¬p⊔¬q]

¬-⊓-distrib  : (P : hProp ℓ) (Q : hProp ℓ') → [ ¬ (P ⊓ Q) ] → [ (P ⇒ ¬ Q) ⊓ (Q ⇒ ¬ P) ]
¬-⊓-distrib P Q ¬p⊓q = (λ p q → ¬p⊓q (p , q)) , (λ q p → ¬p⊓q (p , q))

implication : (P : hProp ℓ) (Q : hProp ℓ') → [ ¬ (P ⊓ Q) ] → [ P ⇒ ¬ Q ]
implication {ℓ = ℓ} P Q ¬[p⊓q] p q = ⊥-elim (¬[p⊓q] (p , q))

uncurryₚ : ∀{ℓ ℓ' ℓ''} (P : hProp ℓ) (Q : hProp ℓ')(R : hProp ℓ'') → (f : [ P ] → [ Q ] → [ R ]) → [ P ⊓ Q ] → [ R ]
uncurryₚ P Q R f = uncurry f

⊓¬¬⇒¬¬⊓ : ∀{ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ') → [ ¬ ¬ P ] → [ ¬ ¬ Q ] → [ ¬ ¬ (P ⊓ Q) ]
⊓¬¬⇒¬¬⊓ P Q ¬¬p ¬¬q = contraposition (¬ (P ⊓ Q)) (P ⇒ ¬ Q) (implication P Q) λ p⇒¬q → ¬¬p (contraposition P (¬ Q) p⇒¬q ¬¬q)

-- Q and P are disjoint if P ⇒ ¬ Q or equivalently Q ⇒ ¬ P

abstract
  -- we have that  (P ⇒ ¬ Q)   ≡ (Q ⇒ ¬ P)
  -- normalizes to (P ⇒ Q ⇒ ⊥) ≡ (Q ⇒ P ⇒ ⊥)
  -- which is just flipping of the arguments
  [P⇒¬Q]≡[Q⇒¬P] : ∀{ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ') → (P ⇒ ¬ Q) ≡ (Q ⇒ ¬ P)
  [P⇒¬Q]≡[Q⇒¬P] P Q = ⇒∶ flip ⇐∶ flip
    -- ⇒∶ (λ p⇒¬q q p → p⇒¬q p q)
    -- ⇐∶ (λ q⇒¬p p q → q⇒¬p q p)

  [P⇒¬Q]⇒[Q⇒¬P] : ∀{ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ') → [ (P ⇒ ¬ Q) ] → [ (Q ⇒ ¬ P) ]
  [P⇒¬Q]⇒[Q⇒¬P] P Q = flip -- pathTo⇒ ([P⇒¬Q]≡[Q⇒¬P] P Q)

  [P⇒¬Q]≡¬[P⊓Q] : ∀{ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ') → (P ⇒ ¬ Q) ≡ ¬ (P ⊓ Q)
  [P⇒¬Q]≡¬[P⊓Q] P Q = ⇒∶ uncurry ⇐∶ curry
    -- ⇒∶ (λ{ p⇒¬q (p , q) →  p⇒¬q   p   q })
    -- ⇐∶ (λ ¬[p⊓q] p   q  → ¬[p⊓q] (p , q) )

-- [¬P⇒Q]⇒[¬Q⇒¬¬P]
-- [¬P⇒¬¬Q]≡[¬Q⇒¬¬P]
--         ≡¬[¬P⊓¬Q]
--         ≡¬¬[P⊔Q]
-- [¬P≡Q]⇒¬[P⊓Q]≡¬[P⊓¬P]

¬[P⊓¬P] : ∀{ℓ} (P : hProp ℓ) → [ ¬ (P ⊓ ¬ P) ]
¬[P⊓¬P] P (p , ¬p) = ¬p p

-- NOTE: I think that we do not have ¬ P ≡ ¬ Q → P ≡ Q
--       since this might be equivalent to some LEM ?

-- ¬-reflects-≡ : ∀{ℓ} (P Q : hProp ℓ) → ¬ P ≡ ¬ Q → P ≡ Q
-- ¬-reflects-≡ P Q ¬p≡¬q with Σ-reflects-≡ ¬p≡¬q
-- ... | fst≡fst , snd≡snd = ΣPathP ({!   !} , {!   !})
--
-- -- (∀ x → P x ≡ P y) → x ≡ y
--
-- postulate dne : ∀{ℓ} (P : hProp ℓ) → ¬ ¬ P ≡ P
--
-- ¬-isEquiv : ∀ ℓ → isEquiv (¬_ {ℓ = ℓ})
-- ¬-isEquiv ℓ = λ where
--   .equiv-proof P → ((¬ P) , dne P) , λ{ (Q , ¬Q≡P) →
--     let γ = {! isPropIsProp (isProp[] Q) (isProp[] Q)  !}
--     in {!   !} }

-- fst (fst (equiv-proof (¬-isEquiv ℓ) P)) = ¬ P
-- snd (fst (equiv-proof (¬-isEquiv ℓ) P)) = dne P
-- snd (equiv-proof (¬-isEquiv ℓ) P) (Q , ¬Q≡P) = {!   !}

-- ¬[P⊓¬P]≡¬[P⊓Q]⇒[¬P≡Q] : ∀{ℓ } (P Q : hProp ℓ) → [ ¬ (P ⊓ ¬ P) ] ≡ [ ¬ (P ⊓ Q) ] → [ P ] ≡ [ ¬ Q ]
-- ¬[P⊓¬P]≡¬[P⊓Q]⇒[¬P≡Q] P Q p = {! [P⇒¬Q]≡¬[P⊓Q] P Q  !}
--
-- ¬[P⊓¬P]≡¬[P⊓Q]≡[P⇒¬Q]≡[P⇒¬¬P]

-- foo : ∀{ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ') → [ (P ⇒ ¬ Q) ] → [ (¬ Q ⇒ P) ] → P ≡ ¬ Q

-- bar : ∀{ℓ} (P Q : hProp ℓ) → [ ¬ (P ⊓ Q) ] → P ≡ ¬ Q
-- -- ¬-⊓-distrib P Q ¬p⊓q
-- bar P Q ¬p⊓q = let r1 : [ (P ⇒ ¬ Q) ⊓ (Q ⇒ ¬ P) ]
--                    r1 =
--                    r2 : [ (Q ⇒ ¬ P) ⊓ (P ⇒ ¬ Q) ]
--                    r2 =
--                in {! ¬-⊓-distrib Q P (transport (λ i → [ ¬ ⊓-comm P Q i ]) ¬p⊓q)  !}

-- more logic

⊓-⊔-distribʳ : (P : hProp ℓ) (Q : hProp ℓ')(R : hProp ℓ'')
  → (Q ⊔ R) ⊓ P ≡ (Q ⊓ P) ⊔ (R ⊓ P)
⊓-⊔-distribʳ P Q R = (
  (Q ⊔ R) ⊓ P       ≡⟨ ⊓-comm _ _ ⟩
   P ⊓ (Q ⊔ R)      ≡⟨ ⊓-⊔-distribˡ P Q R ⟩
  (P ⊓ Q) ⊔ (P ⊓ R) ≡⟨ ( λ i → ⊓-comm P Q i ⊔ ⊓-comm P R i) ⟩
  (Q ⊓ P) ⊔ (R ⊓ P) ∎)

-- NOTE: this is in the standard library
-- ⊓-∀-distrib :  (P : A → hProp ℓ) (Q : A → hProp ℓ')
--   → (∀[ a ∶ A ] P a) ⊓ (∀[ a ∶ A ] Q a) ≡ (∀[ a ∶ A ] (P a ⊓ Q a))
-- ⊓-∀-distrib P Q =
--   ⇒∶ (λ {(p , q) a → p a , q a})
--   ⇐∶ λ pq → (fst ∘ pq ) , (snd ∘ pq)

-- well, we do not have `∀-⊔-distrib`
-- ∀-⊔-distrib : ∀{ℓ ℓ' ℓ''} {A : Type ℓ} → (P : A → hProp ℓ') → (Q : A → hProp ℓ'')
--             → ((∀[ x ∶ A ] P x) ⊔ (∀[ x ∶ A ] Q x)) ≡ (∀[ x ∶ A ] (P x ⊔ Q x))
-- ∀-⊔-distrib {A = A} P Q =
--   ⇒∶ (λ [∀xPx]⊔[∀xQx] x → ⊔-elim (∀[ x ] P x) (∀[ x ] Q x) (λ _ → P x ⊔ Q x) (λ ∀xPx → inlᵖ (∀xPx x)) (λ ∀xQx → inrᵖ (∀xQx x)) [∀xPx]⊔[∀xQx])
--   ⇐∶ λ ∀x[Px⊔Qx] → {!   !}

-- ∀-⊔-distribʳ : ∀{ℓ ℓ' ℓ''} {A : Type ℓ} → (P : hProp ℓ') → (Q : A → hProp ℓ'')
--             → (P ⊔ (∀[ x ∶ A ] Q x)) ≡ (∀[ x ∶ A ] (P ⊔ Q x))
-- ∀-⊔-distribʳ {A = A} P Q =
--   ⇒∶ (λ [P]⊔[∀xQx] x → ⊔-elim P (∀[ x ] Q x) (λ _ → P ⊔ Q x) (λ p → inlᵖ p) (λ ∀xQx → inrᵖ (∀xQx x)) [P]⊔[∀xQx])
--   ⇐∶ λ ∀x[P⊔Qx] → {!   !}

-- ∀-⊎-distribʳ : ∀{ℓ ℓ' ℓ''} (a : Type ℓ) {B : Type ℓ'} (f : B → Type ℓ'')
--              → (a → ∀ b → ¬ᵗ f b) -- a implies that fb is wrong
--              → (∀ b → f b → ¬ᵗ a) -- b implies that a is wrong
--              → (∀ b → a ⊎ f b)    -- for all b, either a holds or fb holds
--              → a ⊎ (∀ b → f b)    -- either a holds or fb holds forall b
-- ∀-⊎-distribʳ a f a→¬fb fb→¬a g = {!   !}

-- hProp-union and Σ-Type-union are equivalent when the two disjuncts are disjoint such that one disproves the other and vice versa

⊎-Level : ∀{A : Type ℓ}{B : Type ℓ'} → A ⊎ B → Level
⊎-Level {ℓ  = ℓ } (inl x) = ℓ
⊎-Level {ℓ' = ℓ'} (inr x) = ℓ'

⊎-Type : ∀{A : Type ℓ}{B : Type ℓ'}(x : A ⊎ B) → Type (⊎-Level x)
⊎-Type {A = A} (inl x) = A
⊎-Type {B = B} (inr x) = B

⊎-pred : ∀{A : Type ℓ}{B : Type ℓ'}(x : A ⊎ B) → ⊎-Type x
⊎-pred (inl x) = x
⊎-pred (inr x) = x

⊎-predˡ : ∀{A : Type ℓ}{B : Type ℓ'}(z : A ⊎ B) → {y : A} → z ≡ inl y → A
⊎-predˡ (inl x) {y} p = x
⊎-predˡ (inr x) {y} p = y

inl-reflects-≡ : ∀{A : Type ℓ}{B : Type ℓ'} {x y : A} → ((A ⊎ B) ∋ inl x) ≡ inl y → x ≡ y
inl-reflects-≡ {A = A} {B = B} {x = x} {y = y} p =  cong γ p where
  γ : (z : A ⊎ B) → A
  γ (inl y) = y
  γ (inr y) = x

inr-reflects-≡ : ∀{A : Type ℓ}{B : Type ℓ'} {x y : B} → ((A ⊎ B) ∋ inr x) ≡ inr y → x ≡ y
inr-reflects-≡ {A = A} {B = B} {x = x} {y = y} p = cong γ p where
  γ : (z : A ⊎ B) → B
  γ (inl y) = x
  γ (inr y) = y

isProp⊎ : ∀{ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → isProp A → isProp B → (A → ¬ᵗ B) ⊎ (B → ¬ᵗ A) → isProp (A ⊎ B)
isProp⊎ pA pB      X⇒¬Y  (inl x) (inl y) = cong inl (pA x y)
isProp⊎ pA pB      X⇒¬Y  (inr x) (inr y) = cong inr (pB x y)
isProp⊎ pA pB (inl A⇒¬B) (inl x) (inr y) = ⊥-elim (A⇒¬B x y)
isProp⊎ pA pB (inr B⇒¬A) (inl x) (inr y) = ⊥-elim (B⇒¬A y x)
isProp⊎ pA pB (inl A⇒¬B) (inr x) (inl y) = ⊥-elim (A⇒¬B y x)
isProp⊎ pA pB (inr B⇒¬A) (inr x) (inl y) = ⊥-elim (B⇒¬A x y)

module _ {ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ')
         (X⇒¬Y : [ P ⇒ ¬ Q ] ⊎ [ Q ⇒ ¬ P ]) where

  ⊎-isProp : isProp ([ P ] ⊎ [ Q ])
  ⊎-isProp = isProp⊎ (isProp[] P) (isProp[] Q) X⇒¬Y

  P⊎Qᵖ : hProp (ℓ-max ℓ ℓ')
  P⊎Qᵖ = ([ P ] ⊎ [ Q ]) , ⊎-isProp

  -- ⊎⇒⊔' : [ P⊎Qᵖ ] → [ P ⊔ Q ]
  -- ⊎⇒⊔' x = ∣ x ∣

  ⊔⇒⊎ : [ P ⊔ Q ] → [ P⊎Qᵖ ]
  abstract ⊔⇒⊎ x = ⊔-elim P Q (λ x → ([ P ] ⊎ [ Q ]) , ⊎-isProp) (λ p → inl p) (λ q → inr q) x

  ⊔⊎-equiv : [ P⊎Qᵖ ⇔ P ⊔ Q ]
  ⊔⊎-equiv = ⊎⇒⊔ P Q , ⊔⇒⊎

  ⊔⊎-≡ : P⊎Qᵖ ≡ P ⊔ Q
  abstract
    ⊔⊎-≡ with ⊔⊎-equiv
    ... | p , q = ⇔toPath p q

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
-----------------------------------------------------------------------------------
-- This file contains facts about equational reasoning pertaining to categories. --
-----------------------------------------------------------------------------------
module Category.CatEq where

open import Level

open import Category.Category
open import Setoid.Total

-- The following models the communative square:
--
--  A ---f₁---> C
--  |           |
--  f₃          f₂
--  |           |
--  V           V
--  D ---f₄---> D
--
-- However, as an equation.
comm-square : {l : Level}{ℂ : Cat {l}}{A B D C : Obj ℂ}
            → el (Hom ℂ A B)
            → el (Hom ℂ B C)
            → el (Hom ℂ A D)
            → el (Hom ℂ D C)
            → Set l
comm-square {ℂ = ℂ}{A}{C = C} f₁ f₂ f₃ f₄ = ⟨ Hom ℂ A C ⟩[ f₁ ○[ comp ℂ ] f₂ ≡ f₃ ○[ comp ℂ ] f₄ ]

ext: agda

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

open import LogicalFormulae
open import Groups.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition

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

module Rings.Subrings.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ _*A_ : A → A → A} (R : Ring S _+A_ _*A_) where

open import Setoids.Subset S
open Ring R
open Group additiveGroup
open import Groups.Subgroups.Definition additiveGroup
open Setoid S
open Equivalence eq

record Subring {c : _} (pred : A → Set c) : Set (a ⊔ b ⊔ c) where
  field
    isSubgroup : Subgroup pred
    containsOne : pred 1R
    closedUnderProduct : {x y : A} → pred x → pred y → pred (x *A y)
  isSubset = Subgroup.isSubset isSubgroup

subringMult : {c : _} {pred : A → Set c} → (s : Subring pred) → Sg A pred → Sg A pred → Sg A pred
subringMult s (a , prA) (b , prB) = (a *A b) , Subring.closedUnderProduct s prA prB

subringIsRing : {c : _} {pred : A → Set c} → (subring : Subring pred) → Ring (subsetSetoid (Subring.isSubset subring)) (subgroupOp (Subring.isSubgroup subring)) (subringMult subring)
Ring.additiveGroup (subringIsRing sub) = subgroupIsGroup (Subring.isSubgroup sub)
Ring.*WellDefined (subringIsRing sub) {r , prR} {s , prS} {t , prT} {u , prU} r=t s=u = *WellDefined r=t s=u
Ring.1R (subringIsRing sub) = (1R , Subring.containsOne sub)
Ring.groupIsAbelian (subringIsRing sub) {a , prA} {b , prB} = groupIsAbelian
Ring.*Associative (subringIsRing sub) {a , prA} {b , prB} {c , prC} = *Associative
Ring.*Commutative (subringIsRing sub) {a , prA} {b , prB} = *Commutative
Ring.*DistributesOver+ (subringIsRing sub) {a , prA} {b , prB} {c , prC} = *DistributesOver+
Ring.identIsIdent (subringIsRing sub) {a , prA} = identIsIdent


text:
module JuiceMaker where

open import Human.Nat hiding (_==_)
open import Human.List hiding (remove-last)
open import Human.Equality
open import Human.Maybe
open import Human.Empty

Not : (P : Set) -> Set
Not P = P -> Empty

-- Different from Bool, shows an evidence of why the value is "yes" or "nop"
data Dec (P : Set) : Set where
  yes : P     -> Dec P
  nop : Not P -> Dec P

-- Define constructors of what are the types of ingredients available
data Ingredient : Set where
  orange    : Ingredient
  pineapple : Ingredient
  carrot    : Ingredient
  apple     : Ingredient
  beet      : Ingredient
  cabbage   : Ingredient

{- Pair is a polimorfic type (as is List). Depends on two types to create a type (Pair of something).
   Ex: Pair Nat Nat, Pair Nat Ingredient, Pair Bool Bool -}
data Pair (A B : Set) : Set where
  pair : A -> B -> Pair A B

--Create a subset (or sigma).Receives a Set and a proof/filter to restricts what items can be part of a subset
data Subset (A : Set) (IsOk : A → Set) : Set where
  subset : (a : A) (b : IsOk a) → Subset A IsOk

----------------------------------------------------------------
------ Items -------
{- Restricts of which can be the pair of ingredients.
   Acts like a filter to create a subset of valid Pair Nat Ingredient -}
data IsItem : Pair Nat Ingredient → Set where
  100-orange    : IsItem (pair 100 orange)
  50-beet       : IsItem (pair 50 beet)

-- An Item is a subset of Pair Nat Ingredient that restricts its elements using IsItem filter
Item : Set
Item = Subset (Pair Nat Ingredient) IsItem

{- n: quantity of ml in an item
   i: a type of ingredient
   p: a proof that a Pair formed by n and i passed the "filter" of IsItem
   item-has-ml: returns a proof that an item has n ml -}
data ItemHasMl : (n : Nat) → (i : Item) → Set where
  item-has-ml : (n : Nat) (i : Ingredient) (p : IsItem (pair n i)) → ItemHasMl n (subset (pair n i) p)

--- Items ---
100ml-orange : Item
100ml-orange = subset (pair 100 orange) 100-orange

50ml-beet : Item
50ml-beet = subset (pair 50 beet) 50-beet

default-items : List Item
default-items = 100ml-orange , 100ml-orange , 100ml-orange , end

--- Auxiliar ---
-- Quantity of ml in an item and a proof that an item has n ml
get-ml-item : (i : Item) -> Subset Nat (λ n -> ItemHasMl n i)
get-ml-item (subset .(pair 100 orange) 100-orange) = subset 100 (item-has-ml 100 orange 100-orange)
get-ml-item (subset .(pair 50 beet) 50-beet)       = subset 50 (item-has-ml 50 beet 50-beet)

get-ml-item-aux : (i : Item) -> Subset Nat (λ n -> ItemHasMl n i) → Nat
get-ml-item-aux i (subset a b) = a

-- Get the ingredient in an Item
get-ingredient-item : (i : Item) → Ingredient
get-ingredient-item (subset (pair ml ing) _) = ing

----------------------------------------------------------------
------ Juice -------
{- This function helps to proof something about the ml in a list.
   n: quantity of ml in a list
   list: list of items
   empty-list-has-0ml: a proof that 0ml represents an empty list
   append-item-adds-ml: a proof that adding an item to a list, adds its ml to the result of list's ml
-}
data ListHasMl : (n : Nat) (list : List Item) → Set where
  empty-list-has-0ml  : ListHasMl 0 end
  -- receives ml in item, an item, ml is a list, a list. Also, a proof of ItemHasMl and ListHasMl
  append-item-adds-ml : ∀ it-ml it li-ml li → ItemHasMl it-ml it → ListHasMl li-ml li → ListHasMl (it-ml + li-ml) (it , li)

{- Get the quantity of ml in a list by returning the proof that n is the quantity of ml in a list.
   Obs: the second argument in Subset is something applied to n.
   λ is used to represents that something (ListhasMl) is applied to n. -}
get-ml-list : (list : List Item) -> Subset Nat (λ n → ListHasMl n list)
get-ml-list end = subset zero empty-list-has-0ml
get-ml-list (it , rest) with get-ml-item it | get-ml-list rest -- "with" acts similar to case, but opening values inside this case
get-ml-list (it , rest)
  | subset it-ml it-ml-pf
  | subset rest-ml rest-ml-pf
  = let sum-ml                 = it-ml + rest-ml
        append-list-has-sum-ml = append-item-adds-ml it-ml it rest-ml rest it-ml-pf rest-ml-pf
    in subset sum-ml append-list-has-sum-ml

  {- IsJuice is a filter indexed in List Item (receives a list of Item),
  restricts what can become a juice (a proof that it have 300ml),
  and returns an element of IsJuice, that is, a proof that it was approved to become a juice -}
data IsJuice : List Item → Set where
  juice : ∀ (l : List Item) → (ListHasMl 300 l) -> IsJuice l

-- A Juice is a subset of List Item that restricts its elements using IsJuice filter
Juice : Set
Juice = Subset (List Item) IsJuice

-- default-juice : Juice
-- default-juice = subset default-items (juice default-items refl)

----------------------------------------------------------------
----- Events -----
data Event : Set where
  pick : Item -> Event
  undo : Event
  copy : Event -- add again the last element
  done : Event

remove-last : List Item → List Item
remove-last end     = end
remove-last (x , l) = l

copy-last : List Item → List Item
copy-last end     = end
copy-last (x , l) = x , x , l

-- Look into a list of events and return a list of items
event-to-item : List Event -> List Item
event-to-item end          = end
event-to-item (pick x , e) = x , (event-to-item e) -- add element in the list and continues to look into List of Event
event-to-item (undo , e)   = remove-last (event-to-item e)
event-to-item (copy , e)   = copy-last (event-to-item e)
event-to-item (done , e)   = event-to-item e

-- Given a list and a proof that the list has a quantity of ml, returns the ml
get-ml-list-aux : (l : List Item) → Subset Nat (λ n → ListHasMl n l) → Nat
get-ml-list-aux l (subset a b) = a

-- goal: Maybe (Subset (List (Subset (Pair Nat Ingredient) IsItem)) IsJuice)
make : List Item -> Maybe Juice
make end     = nothing
make (x , l) with make l
... | just m  =
      let it-ml = (get-ml-item-aux x (get-ml-item x)) -- quantity of ml in x
          li-ml = (get-ml-list-aux l (get-ml-list l)) --
          -- is-juice = subset l (juice l (append-item-aadds-ml it-ml x li-ml l (item-has-ml it-ml x) ? ))
          -- usar o get-ml-list pra provar que o suco tem 300 ml
          -- is-juice = subset l (juice l (get-ml-list l))
      in {!   !} -- just (subset l) (juice l is-juice))
... | nothing = nothing

-- pra satisfazer o chefe
-- make-always : List Item -> Juice
-- make-always items with make items
-- ... | yes items-is-juice = subset items (juice items-is-juice)
-- ... | no items           = default-juice

---------------
---- Test -----

test-list : Nat
test-list = (sum (1 , 2 , 3 , 4 , 5 , end))

event-list : List Event
event-list = pick 100ml-orange , pick 50ml-beet , pick 50ml-beet , pick 100ml-orange , end

-- qtd-juice : Nat
-- qtd-juice = sum (map get-ml-item (make event-list))

-- made-juice-has-300-ml-ex : (sum (map get-ml-item (make event-list))) == 300
-- made-juice-has-300-ml-ex = refl

-- For all sum of ml in the items, the result must be 300
-- a Nat (value) is different than a proof that this number will always be something
-- made-juice-has-300-ml : ∀ (events : List Event) → (sum (map get-ml-item (make events))) == 300
-- made-juice-has-300-ml events = {!   !}
--
--
-- made-juice-has-5-items : ∀ (events : List Event) → length (map get-ingredient-item (make events)) == 5
-- made-juice-has-5-items = {!   !}

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


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

open import HoTT

module homotopy.SuspensionJoin {i} (A : Type i) where

{- To -}

false, : A → Bool × A
false, a = false , a

true, : A → Bool × A
true, a = true , a

module To = SuspensionRec {i} (left false :> Bool * A) (left true) (λ a → glue (false, a) ∙ ! (glue (true, a)))

to : Suspension A → (Bool * A)
to = To.f

{- From -}

from : Bool * A → Suspension A
from = From.f  module _ where

  from-bool : Bool → Suspension A
  from-bool false = north
  from-bool true = south

  from-glue : (c : Bool × A) → from-bool (fst c) == south
  from-glue (false , a) = merid a
  from-glue (true , a) = idp

  module From = PushoutRec {d = *-span Bool A} from-bool (λ _ → south) from-glue

{- ToFrom -}

to-from : (c : Bool * A) → to (from c) == c
to-from = Pushout-elim to-from-left (λ a → glue (true , a)) to-from-glue  where

  to-from-left : (b : Bool) → to (from (left b)) == left b
  to-from-left false = idp
  to-from-left true = idp

  to-from-glue' : (b : Bool) (a : A)
    → ap to (ap from (glue (b , a))) ∙' glue (true , a) == to-from-left b ∙ glue (b , a)
  to-from-glue' true a =
    ap to (ap from (glue (true , a))) ∙' glue (true , a)   =⟨ From.glue-β (true , a) |in-ctx (λ u → ap to u ∙' glue (true , a)) ⟩
    idp ∙' glue (true , a)                                 =⟨ ∙'-unit-l _ ⟩
    glue (true , a) ∎
  to-from-glue' false a =
    ap to (ap from (glue (false , a))) ∙' glue (true , a)   =⟨ From.glue-β (false , a) |in-ctx (λ u → ap to u ∙' glue (true , a)) ⟩
    ap to (merid a) ∙' glue (true , a)   =⟨ To.merid-β a |in-ctx (λ u → u ∙' glue (true , a)) ⟩
    (glue (false , a) ∙ ! (glue (true , a))) ∙' glue (true , a)   =⟨ coh (glue (false , a)) (glue (true , a)) ⟩
    glue (false , a) ∎  where

    coh : ∀ {i} {A : Type i} {a b c : A} (p : a == b) (q : c == b) → (p ∙ ! q) ∙' q == p
    coh idp idp = idp

  to-from-glue : (c : Bool × A)
    → to-from-left (fst c) == glue (true , snd c) [ (λ z → to (from z) == z) ↓ glue c ]
  to-from-glue c = ↓-∘=idf-in to from (uncurry to-from-glue' c)

{- FromTo -}

from-to : (c : Suspension A) → from (to c) == c
from-to = Suspension-elim idp idp from-to-merid  where

  from-to-merid' : (a : A) → ap from (ap to (merid a)) == merid a
  from-to-merid' a =
    ap from (ap to (merid a))   =⟨ To.merid-β a |in-ctx ap from ⟩
    ap from (glue (false , a) ∙ ! (glue (true , a)))   =⟨ ap-∙ from (glue (false , a)) (! (glue (true , a))) ⟩
    ap from (glue (false , a)) ∙ ap from (! (glue (true , a)))   =⟨ ap-! from (glue (true , a)) |in-ctx (λ u → ap from (glue (false , a)) ∙ u) ⟩
    ap from (glue (false , a)) ∙ ! (ap from (glue (true , a)))   =⟨ From.glue-β (false , a) |in-ctx (λ u → u ∙ ! (ap from (glue (true , a)))) ⟩
    merid a ∙ ! (ap from (glue (true , a)))   =⟨ From.glue-β (true , a) |in-ctx (λ u → merid a ∙ ! u) ⟩
    merid a ∙ idp   =⟨ ∙-unit-r _ ⟩
    merid a ∎

  from-to-merid : (a : A) → idp == idp [ (λ z → from (to z) == z) ↓ merid a ]
  from-to-merid a = ↓-∘=idf-in from to (from-to-merid' a)

{- Conclusion -}

e : Suspension A ≃ (Bool * A)
e = equiv to from to-from from-to

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
postulate
  A : Set₁

barb : Set₁
barb = {!(x y : A) → ?!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Functors
open import Categories
open import RMonads

module RMonads.REM.Functors {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
                            (J : Fun C D)(M : RMonad J) where

open import Library
open import RMonads.REM M

open Cat
open Fun
open RAlg
open RAlgMorph
open RMonad M

REML : Fun C EM
REML = record {
  OMap  = λ X → record {
    acar  = T X;
    astr  = bind;
    alaw1 = sym law2;
    alaw2 = law3};
  HMap  = λ f → record {
    amor = bind (comp D η (HMap J f));
    ahom = sym law3};
  fid   = RAlgMorphEq (
    proof
    bind (comp D η (HMap J (iden C)))
    ≅⟨ cong (bind ∘ comp D η) (fid J) ⟩
    bind (comp D η (iden D))
    ≅⟨ cong bind (idr D) ⟩
    bind η
    ≅⟨ law1 ⟩
    iden D ∎);
  fcomp = λ{_ _ _ f g} → RAlgMorphEq (
    proof
    bind (comp D η (HMap J (comp C f g)))
    ≅⟨ cong (bind ∘ comp D η) (fcomp J) ⟩
    bind (comp D η (comp D (HMap J f) (HMap J g)))
    ≅⟨ cong bind (sym (ass D)) ⟩
    bind (comp D (comp D η (HMap J f)) (HMap J g))
    ≅⟨ cong (λ f₁ → bind (comp D f₁ (HMap J g))) (sym law2) ⟩
    bind (comp D (comp D (bind (comp D η (HMap J f))) η) (HMap J g))
    ≅⟨ cong bind (ass D) ⟩
    bind (comp D (bind (comp D η (HMap J f))) (comp D η (HMap J g)))
    ≅⟨ law3 ⟩
    comp D (bind (comp D η (HMap J f))) (bind (comp D η (HMap J g)))
    ∎)}

REMR : Fun EM D
REMR = record {
  OMap  = acar;
  HMap  = amor;
  fid   = refl;
  fcomp = refl}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module Sessions.Syntax.Types where

open import Level
open import Function

open import Data.Bool
open import Data.List
open import Data.List.All
open import Data.List.Membership.Propositional
open import Data.List.Relation.Binary.Permutation.Inductive
open import Data.List.Relation.Ternary.Interleaving.Propositional as I
open import Data.List.Relation.Ternary.Interleaving.Properties
open import Data.List.Relation.Binary.Equality.Propositional
open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Codata.Thunk as Thunk

open import Algebra
open import Algebra.FunctionProperties

open import Relation.Unary hiding (_∈_; _⊢_)
open import Relation.Nullary
open import Relation.Nullary.Decidable as DecM
open import Relation.Nullary.Product
open import Relation.Binary.PropositionalEquality as P hiding ([_])

open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Construct.Product
open import Relation.Ternary.Separation.Construct.List

{- Unrestricted-, Session- and Expression types-}
module _ where
  mutual
    -- crefnel types
    infixr 10 _¿_
    data SType : Set where
      _!_ _¿_ : Type → SType → SType
      end     : SType

    data Type : Set where
      unit  : Type
      cref  : SType → Type
      prod  : Type → Type → Type
      _⊸_   : Type → Type → Type

  LCtx = List Type   -- linear contexts
  variable
    Γ Γ' Γ₁ Γ₂ Γ₃ Γ₄ : LCtx

{- Some conventions -}
variable
  a b c   : Type
  α β γ   : SType

{- Duality -}
module _ where

  infixl 1000 _⁻¹
  _⁻¹  : SType → SType
  (a ! β) ⁻¹ = a ¿ β ⁻¹
  (a ¿ β) ⁻¹ = a ! β ⁻¹
  end ⁻¹     = end

  dual-end : ∀ {α} → α ⁻¹ ≡ end → α ≡ end
  dual-end {x ! α} ()
  dual-end {x ¿ α} ()
  dual-end {end} refl = refl

  dual-involutive : ∀ {α} → α ⁻¹ ⁻¹ ≡ α
  dual-involutive {x ! α} = cong (_!_ _) dual-involutive
  dual-involutive {x ¿ α} = cong (_¿_ _) dual-involutive
  dual-involutive {end} = refl


text:
----------------------------------------------------------------------------------
-- Types for parse trees
----------------------------------------------------------------------------------

module cedille-types where

open import lib
-- open import parse-tree

posinfo = string
alpha = string
alpha-bar-3 = string
alpha-range-1 = string
alpha-range-2 = string
bvar = string
bvar-bar-13 = string
fpth = string
fpth-bar-15 = string
fpth-bar-16 = string
fpth-bar-17 = string
fpth-plus-14 = string
fpth-star-18 = string
kvar = string
kvar-bar-19 = string
kvar-star-20 = string
num = string
num-plus-5 = string
numone = string
numone-range-4 = string
numpunct = string
numpunct-bar-10 = string
numpunct-bar-6 = string
numpunct-bar-7 = string
numpunct-bar-8 = string
numpunct-bar-9 = string
qkvar = string
qvar = string
var = string
var-bar-11 = string
var-star-12 = string

{-# FOREIGN GHC import qualified CedilleTypes #-}

data arg : Set
args : Set
opacity : Set
data cmd : Set
cmds : Set
data decl : Set
data defDatatype : Set
data ctr : Set
ctrs : Set
data defTermOrType : Set
imports : Set
data imprt : Set
data kind : Set
data leftRight : Set
data liftingType : Set
data lterm : Set
lterms : Set
data optType : Set
maybeErased : Set
forceErased : Set
maybeMinus : Set
data nums : Set
data optAs : Set
data optClass : Set
data optGuide : Set
rhoHnf : Set
data optNums : Set
optPublic : Set
data optTerm : Set
params : Set
data start : Set
data term : Set
data theta : Set
data tk : Set
data type : Set
data vars : Set
cases : Set
data case : Set
caseArgs : Set
data caseArg : Set

{-# COMPILE GHC arg = type CedilleTypes.Arg #-}
{-# COMPILE GHC args = type CedilleTypes.Args #-}
{-# COMPILE GHC opacity = type CedilleTypes.Opacity #-}
{-# COMPILE GHC cmd = type CedilleTypes.Cmd #-}
{-# COMPILE GHC cmds = type CedilleTypes.Cmds #-}
{-# COMPILE GHC decl = type CedilleTypes.Decl #-}
{-# COMPILE GHC defDatatype = type CedilleTypes.DefDatatype #-}
{-# COMPILE GHC ctr = type CedilleTypes.DataCtr #-}
{-# COMPILE GHC ctrs = type CedilleTypes.Ctrs #-}
{-# COMPILE GHC defTermOrType = type CedilleTypes.DefTermOrType #-}
{-# COMPILE GHC imports = type CedilleTypes.Imports #-}
{-# COMPILE GHC imprt = type CedilleTypes.Imprt #-}
{-# COMPILE GHC kind = type CedilleTypes.Kind #-}
{-# COMPILE GHC leftRight = type CedilleTypes.LeftRight #-}
{-# COMPILE GHC liftingType = type CedilleTypes.LiftingType #-}
{-# COMPILE GHC lterm = type CedilleTypes.Lterm #-}
{-# COMPILE GHC lterms = type CedilleTypes.Lterms #-}
{-# COMPILE GHC optType = type CedilleTypes.OptType #-}
{-# COMPILE GHC maybeErased = type CedilleTypes.MaybeErased #-}
{-# COMPILE GHC forceErased = type CedilleTypes.MaybeErased #-}
{-# COMPILE GHC maybeMinus = type CedilleTypes.MaybeMinus #-}
{-# COMPILE GHC nums = type CedilleTypes.Nums #-}
{-# COMPILE GHC optAs = type CedilleTypes.OptAs #-}
{-# COMPILE GHC optClass = type CedilleTypes.OptClass #-}
{-# COMPILE GHC optGuide = type CedilleTypes.OptGuide #-}
{-# COMPILE GHC rhoHnf = type CedilleTypes.RhoHnf #-}
{-# COMPILE GHC optNums = type CedilleTypes.OptNums #-}
{-# COMPILE GHC optPublic = type CedilleTypes.OptPublic #-}
{-# COMPILE GHC optTerm = type CedilleTypes.OptTerm #-}
{-# COMPILE GHC params = type CedilleTypes.Params #-}
{-# COMPILE GHC start = type CedilleTypes.Start #-}
{-# COMPILE GHC term = type CedilleTypes.Term  #-}
{-# COMPILE GHC theta = type CedilleTypes.Theta  #-}
{-# COMPILE GHC tk = type CedilleTypes.Tk  #-}
{-# COMPILE GHC type = type CedilleTypes.Type  #-}
{-# COMPILE GHC vars = type CedilleTypes.Vars  #-}
{-# COMPILE GHC cases = type CedilleTypes.Cases  #-}
{-# COMPILE GHC case = type CedilleTypes.Case #-}
{-# COMPILE GHC caseArgs = type CedilleTypes.CaseArgs  #-}
{-# COMPILE GHC caseArg = type CedilleTypes.CaseArg #-}

data arg where
  TermArg : maybeErased → term → arg
  TypeArg : type → arg
{-# COMPILE GHC arg = data CedilleTypes.Arg (CedilleTypes.TermArg | CedilleTypes.TypeArg) #-}

args = 𝕃 arg

opacity = 𝔹

data cmd where
  DefKind : posinfo → kvar → params → kind → posinfo → cmd
  DefTermOrType : opacity → defTermOrType → posinfo → cmd
  DefDatatype   : defDatatype   → posinfo → cmd
  ImportCmd : imprt → cmd
{-# COMPILE GHC cmd = data CedilleTypes.Cmd (CedilleTypes.DefKind | CedilleTypes.DefTermOrType | CedilleTypes.DefDatatype |CedilleTypes.ImportCmd) #-}

cmds = 𝕃 cmd

data decl where
  Decl : posinfo → posinfo → maybeErased → bvar → tk → posinfo → decl
{-# COMPILE GHC decl = data CedilleTypes.Decl (CedilleTypes.Decl) #-}

data defDatatype where
  Datatype : posinfo → posinfo → var → params → kind → ctrs → defDatatype
{-# COMPILE GHC defDatatype = data CedilleTypes.DefDatatype (CedilleTypes.Datatype) #-}

data ctr where
  Ctr : posinfo → var → type → ctr
{-# COMPILE GHC ctr = data CedilleTypes.DataCtr (CedilleTypes.Ctr) #-}

ctrs = 𝕃 ctr

data defTermOrType where
  DefTerm : posinfo → var → optType → term → defTermOrType
  DefType : posinfo → var → kind → type → defTermOrType
{-# COMPILE GHC defTermOrType = data CedilleTypes.DefTermOrType (CedilleTypes.DefTerm | CedilleTypes.DefType) #-}

imports = 𝕃 imprt

data imprt where
  Import : posinfo → optPublic → posinfo → fpth → optAs → args → posinfo → imprt
{-# COMPILE GHC imprt = data CedilleTypes.Imprt (CedilleTypes.Import) #-}

data kind where
  KndArrow : kind → kind → kind
  KndParens : posinfo → kind → posinfo → kind
  KndPi : posinfo → posinfo → bvar → tk → kind → kind
  KndTpArrow : type → kind → kind
  KndVar : posinfo → qkvar → args → kind
  Star : posinfo → kind
{-# COMPILE GHC kind = data CedilleTypes.Kind (CedilleTypes.KndArrow | CedilleTypes.KndParens | CedilleTypes.KndPi | CedilleTypes.KndTpArrow | CedilleTypes.KndVar | CedilleTypes.Star) #-}

data leftRight where
  Both : leftRight
  Left : leftRight
  Right : leftRight
{-# COMPILE GHC leftRight = data CedilleTypes.LeftRight (CedilleTypes.Both | CedilleTypes.Left | CedilleTypes.Right) #-}

data liftingType where
  LiftArrow : liftingType → liftingType → liftingType
  LiftParens : posinfo → liftingType → posinfo → liftingType
  LiftPi : posinfo → bvar → type → liftingType → liftingType
  LiftStar : posinfo → liftingType
  LiftTpArrow : type → liftingType → liftingType
{-# COMPILE GHC liftingType = data CedilleTypes.LiftingType (CedilleTypes.LiftArrow | CedilleTypes.LiftParens | CedilleTypes.LiftPi | CedilleTypes.LiftStar | CedilleTypes.LiftTpArrow) #-}

data lterm where
  Lterm : maybeErased → term → lterm
{-# COMPILE GHC lterm = data CedilleTypes.Lterm (CedilleTypes.MkLterm) #-}

lterms = 𝕃 lterm

data optType where
  SomeType : type → optType
  NoType : optType
{-# COMPILE GHC optType = data CedilleTypes.OptType (CedilleTypes.SomeType | CedilleTypes.NoType) #-}

maybeErased = 𝔹

forceErased = 𝔹

maybeMinus = 𝔹

data nums where
  NumsStart : num → nums
  NumsNext : num → nums → nums
{-# COMPILE GHC nums = data CedilleTypes.Nums (CedilleTypes.NumsStart | CedilleTypes.NumsNext) #-}

data optAs where
  NoOptAs : optAs
  SomeOptAs : posinfo → var → optAs
{-# COMPILE GHC optAs = data CedilleTypes.OptAs (CedilleTypes.NoOptAs | CedilleTypes.SomeOptAs) #-}

optPublic = 𝔹

data optClass where
  NoClass : optClass
  SomeClass : tk → optClass
{-# COMPILE GHC optClass = data CedilleTypes.OptClass (CedilleTypes.NoClass | CedilleTypes.SomeClass) #-}

data optGuide where
  NoGuide : optGuide
  Guide : posinfo → var → type → optGuide
{-# COMPILE GHC optGuide = data CedilleTypes.OptGuide (CedilleTypes.NoGuide | CedilleTypes.Guide) #-}

rhoHnf = 𝔹

data optNums where
  NoNums : optNums
  SomeNums : nums → optNums
{-# COMPILE GHC optNums = data CedilleTypes.OptNums (CedilleTypes.NoNums | CedilleTypes.SomeNums) #-}

data optTerm where
  NoTerm : optTerm
  SomeTerm : term → posinfo → optTerm
{-# COMPILE GHC optTerm = data CedilleTypes.OptTerm (CedilleTypes.NoTerm | CedilleTypes.SomeTerm) #-}

params = 𝕃 decl

data start where
  File : imports → posinfo → posinfo → qvar → params → cmds → posinfo → start
{-# COMPILE GHC start = data CedilleTypes.Start (CedilleTypes.File) #-}

data term where
  App : term → maybeErased → term → term
  AppTp : term → type → term
  Beta : posinfo → optTerm → optTerm → term
  Chi : posinfo → optType → term → term
  Delta : posinfo → optType → term → term
  Epsilon : posinfo → leftRight → maybeMinus → term → term
  Hole : posinfo → term
  IotaPair : posinfo → term → term → optGuide → posinfo → term
  IotaProj : term → num → posinfo → term
  Lam : posinfo → maybeErased → posinfo → bvar → optClass → term → term
  Let : posinfo → forceErased → defTermOrType → term → term
  Open : posinfo → opacity → posinfo → var → term → term
  Parens : posinfo → term → posinfo → term
  Phi : posinfo → term → term → term → posinfo → term
  Rho : posinfo → rhoHnf → optNums → term → optGuide → term → term
  Sigma : posinfo → term → term
  Theta : posinfo → theta → term → lterms → term
  Mu  : posinfo → posinfo → bvar → term → optType → posinfo → cases → posinfo → term
  Mu' : posinfo → optTerm → term → optType → posinfo → cases → posinfo → term
  Var : posinfo → qvar → term
{-# COMPILE GHC term = data CedilleTypes.Term (CedilleTypes.App | CedilleTypes.AppTp | CedilleTypes.Beta | CedilleTypes.Chi | CedilleTypes.Delta | CedilleTypes.Epsilon | CedilleTypes.Hole | CedilleTypes.IotaPair | CedilleTypes.IotaProj | CedilleTypes.Lam | CedilleTypes.Let | CedilleTypes.Open | CedilleTypes.Parens | CedilleTypes.Phi | CedilleTypes.Rho | CedilleTypes.Sigma | CedilleTypes.Theta | CedilleTypes.Mu | CedilleTypes.Mu' | CedilleTypes.Var) #-}

data case where
  Case : posinfo → var → caseArgs → term → case
{-# COMPILE GHC case = data CedilleTypes.Case (CedilleTypes.MkCase) #-}

cases = 𝕃 case

data caseArg where
  CaseTermArg : posinfo → maybeErased → var → caseArg
  CaseTypeArg : posinfo → var → caseArg
{-# COMPILE GHC caseArg = data CedilleTypes.CaseArg (CedilleTypes.CaseTermArg | CedilleTypes.CaseTypeArg) #-}

caseArgs = 𝕃 caseArg

data theta where
  Abstract : theta
  AbstractEq : theta
  AbstractVars : vars → theta
{-# COMPILE GHC theta = data CedilleTypes.Theta (CedilleTypes.Abstract | CedilleTypes.AbstractEq | CedilleTypes.AbstractVars) #-}

data tk where
  Tkk : kind → tk
  Tkt : type → tk
{-# COMPILE GHC tk = data CedilleTypes.Tk (CedilleTypes.Tkk | CedilleTypes.Tkt) #-}

data type where
  Abs : posinfo → maybeErased → posinfo → bvar → tk → type → type
  Iota : posinfo → posinfo → bvar → type → type → type
  Lft : posinfo → posinfo → var → term → liftingType → type
  NoSpans : type → posinfo → type
  TpLet : posinfo → defTermOrType → type → type
  TpApp : type → type → type
  TpAppt : type → term → type
  TpArrow : type → maybeErased → type → type
  TpEq : posinfo → term → term → posinfo → type
  TpHole : posinfo → type
  TpLambda : posinfo → posinfo → bvar → tk → type → type
  TpParens : posinfo → type → posinfo → type
  TpVar : posinfo → qvar → type
{-# COMPILE GHC type = data CedilleTypes.Type (CedilleTypes.Abs | CedilleTypes.Iota | CedilleTypes.Lft | CedilleTypes.NoSpans | CedilleTypes.TpLet | CedilleTypes.TpApp | CedilleTypes.TpAppt | CedilleTypes.TpArrow | CedilleTypes.TpEq | CedilleTypes.TpHole | CedilleTypes.TpLambda | CedilleTypes.TpParens | CedilleTypes.TpVar) #-}

data vars where
  VarsNext : var → vars → vars
  VarsStart : var → vars
{-# COMPILE GHC vars = data CedilleTypes.Vars (CedilleTypes.VarsNext | CedilleTypes.VarsStart) #-}

pattern Erased = tt
pattern NotErased = ff
pattern Pi = NotErased
pattern All = Erased
pattern OpacTrans = tt
pattern OpacOpaque = ff
pattern IsPublic = tt
pattern NotPublic = ff
pattern EpsHnf = ff
pattern EpsHanf = tt
pattern RhoPlain = ff
pattern RhoPlus = tt

-- embedded types:
-- aterm = term
-- atype = type
-- lliftingType = liftingType
-- lterm = term
-- ltype = type
-- pterm = term

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
------------------------------------------------------------------------
-- A solver for certain natural number equalities
------------------------------------------------------------------------

-- The standard library's solver is used.

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

open import Equality

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

open Derived-definitions-and-properties eq

import Equality.Propositional as EP
open import Equality.Instances-related
open import Prelude

open import Bijection eq using (_↔_)
open import Function-universe eq

open import Data.Nat.Solver
open import Data.Vec as Vec
open import Data.Vec.N-ary
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (Equivalence)
import Relation.Binary.Reflection
import Relation.Binary.PropositionalEquality as P

open +-*-Solver public using (_:=_; _:+_; _:*_; _:^_)
open +-*-Solver.Polynomial public using (con)

open +-*-Solver hiding (solve)
open Relation.Binary.Reflection (P.setoid _) var ⟦_⟧ ⟦_⟧↓ correct
  using (close)

private

  -- Some simple lemmas.

  ≡↔≡ : ∀ {a} {A : Type a} {x y : A} → x ≡ y ↔ x P.≡ y
  ≡↔≡ = proj₁ (all-equality-types-isomorphic eq EP.equality-with-J)

  ≡→≡ : ∀ {a} {A : Type a} {x y : A} → x ≡ y → x P.≡ y
  ≡→≡ = _↔_.to ≡↔≡

  ≡←≡ : ∀ {a} {A : Type a} {x y : A} → x P.≡ y → x ≡ y
  ≡←≡ = _↔_.from ≡↔≡

-- A variant of +-*-Solver.solve.

solve :
  ∀ n (f : N-ary n (Polynomial n)
                   (Polynomial n × Polynomial n)) →
  Eqʰ n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
            (curryⁿ ⟦ proj₂ (close n f) ⟧↓) →
  Eq  n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧)
            (curryⁿ ⟦ proj₂ (close n f) ⟧)
solve n f =
  Eqʰ n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
            (curryⁿ ⟦ proj₂ (close n f) ⟧↓)                        ↝⟨ Eqʰ-to-Eq n _≡_ ⟩

  Eq n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
           (curryⁿ ⟦ proj₂ (close n f) ⟧↓)                         ↔⟨⟩

  ∀ⁿ n (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) ≡
                      (curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs))       ↝⟨ Equivalence.to (uncurry-∀ⁿ n) ⟨$⟩_ ⟩

  (∀ (xs : Vec _ n) →
     (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) ≡
                    (curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs)) $ⁿ xs)  ↝⟨ (∀-cong _ λ xs → ≡⇒↝ _ $ ≡←≡ $ left-inverse _ xs) ⟩

  (∀ (xs : Vec _ n) →
     (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) ≡
     (curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs))                        ↝⟨ (∀-cong _ λ _ → ≡→≡) ⟩

  (∀ (xs : Vec _ n) →
     (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) P.≡
     (curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs))                        ↝⟨ (∀-cong _ λ xs → ≡⇒↝ _ $ sym $ ≡←≡ $ left-inverse _ xs) ⟩

  (∀ (xs : Vec _ n) →
     (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) P.≡
                    (curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs)) $ⁿ xs)  ↝⟨ Equivalence.from (uncurry-∀ⁿ n) ⟨$⟩_ ⟩

  ∀ⁿ n (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) P.≡
                      (curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs))       ↔⟨⟩

  Eq n P._≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
             (curryⁿ ⟦ proj₂ (close n f) ⟧↓)                       ↝⟨ Eq-to-Eqʰ n P._≡_ ⟩

  Eqʰ n P._≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
              (curryⁿ ⟦ proj₂ (close n f) ⟧↓)                      ↝⟨ +-*-Solver.solve n f ⟩

  Eq n P._≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧)
             (curryⁿ ⟦ proj₂ (close n f) ⟧)                        ↔⟨⟩

  ∀ⁿ n (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) P.≡
                      (curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs))        ↝⟨ Equivalence.to (uncurry-∀ⁿ n) ⟨$⟩_ ⟩

  (∀ (xs : Vec _ n) →
     (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) P.≡
                    (curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs)) $ⁿ xs)   ↝⟨ (∀-cong _ λ xs → ≡⇒↝ _ $ ≡←≡ $ left-inverse _ xs) ⟩

  (∀ (xs : Vec _ n) →
     (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) P.≡
     (curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs))                         ↝⟨ (∀-cong _ λ _ → ≡←≡) ⟩

  (∀ (xs : Vec _ n) →
     (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) ≡
     (curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs))                         ↝⟨ (∀-cong _ λ xs → ≡⇒↝ _ $ sym $ ≡←≡ $ left-inverse _ xs) ⟩

  (∀ (xs : Vec _ n) →
     (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) ≡
                    (curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs)) $ⁿ xs)   ↝⟨ Equivalence.from (uncurry-∀ⁿ n) ⟨$⟩_ ⟩

  ∀ⁿ n (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) ≡
                      (curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs))        ↔⟨⟩

  Eq n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧)
           (curryⁿ ⟦ proj₂ (close n f) ⟧)                          □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax CommMonoid | CM

type
  * : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
-}

module CommMonoid.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import CommMonoid.Signature
open import CommMonoid.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution CM:Syn
open import SOAS.Metatheory.SecondOrder.Equality CM:Syn

private
  variable
    α β γ τ : *T
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ CM) α Γ → (𝔐 ▷ CM) α Γ → Set where
  εU⊕ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢       ε ⊕ 𝔞 ≋ₐ 𝔞
  ⊕A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ⊕ 𝔟) ⊕ 𝔠 ≋ₐ 𝔞 ⊕ (𝔟 ⊕ 𝔠)
  ⊕C   : ⁅ * ⁆ ⁅ * ⁆̣       ▹ ∅ ⊢       𝔞 ⊕ 𝔟 ≋ₐ 𝔟 ⊕ 𝔞

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

-- Derived equations
εU⊕ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ⊕ ε ≋ 𝔞
εU⊕ᴿ = tr (ax ⊕C with《 𝔞 ◃ ε 》) (ax εU⊕ᴸ with《 𝔞 》)

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module fizzbuzz where

import Data.Nat        as N
import Data.Nat.DivMod as N
import Data.Nat.Show   as N
import Data.Bool       as B
import Data.Fin        as F
import Data.Unit       as U
import Data.String     as S
open import Data.Product using (_,_ ; _×_)
open import IO
open import Agda.Builtin.Coinduction
open import Relation.Nullary
open import Function

congruent : N.ℕ → N.ℕ → B.Bool
congruent n N.zero    = B.false
congruent n (N.suc m) with N._≟_ 0 $ F.toℕ (N._mod_ n (N.suc m) {U.tt})
... | yes _ = B.true
... | no  _ = B.false

_and_ : {A B : Set} → A → B → A × B
_and_ = _,_

fizzbuzz : N.ℕ → S.String
fizzbuzz N.zero    = "fizzbuzz"
fizzbuzz n with congruent n 3 and congruent n 5
... | B.true  , B.true   = "fizzbuzz"
... | B.true  , B.false  = "fizz"
... | B.false , B.true   = "buzz"
... | B.false , B.false  = N.show n

worker : N.ℕ → IO U.⊤
worker N.zero    = putStrLn $ fizzbuzz N.zero
worker (N.suc n) = ♯ worker n >> ♯ putStrLn (fizzbuzz $ N.suc n)

main = run $ worker 100

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

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

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


text:
module Ag12 where

import Relation.Binary.PropositionalEquality as Eq
open Eq
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function
open import Ag09 hiding (_∘_)
-- open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)
open ≡-Reasoning
open ≃-Reasoning

postulate
  funExt : ∀ {m n : Level} {A : Set m} {B : Set n} {f g : A → B}
           → (∀ (x : A) → f x ≡ g x)
           → f ≡ g

lemma₀ : ∀ {A B : Set} → (a : A × B) → ⟨ proj₁ a , proj₂ a ⟩ ≡ a
lemma₀ ⟨ fst , snd ⟩ = refl

lemma₁ : ∀ {A : Set} {B C : A → Set}
         → (f : (x : A) → B x × C x)
         → (λ a → ⟨ proj₁ (f a) , proj₂ (f a) ⟩) ≡ f
lemma₁ f = refl

∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
  (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
∀-distrib-× {A} {B} {C} =
  record
  { to      = λ bc → ⟨ proj₁ ∘ bc , proj₂ ∘ bc ⟩
  ; from    = λ bc a → ⟨ proj₁ bc a , proj₂ bc a ⟩
  ; from∘to = λ f → refl
  ; to∘from = λ f → refl
  }
⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
  (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x)  →  ∀ (x : A) → B x ⊎ C x
⊎∀-implies-∀⊎ (_⊎_.inj₁ x₁) x = _⊎_.inj₁ (x₁ x)
⊎∀-implies-∀⊎ (_⊎_.inj₂ y) x = _⊎_.inj₂ (y x)

data Σ (A : Set) (B : A → Set) : Set where
  ⟨_,_⟩ : (x : A) → B x → Σ A B

Σ-syntax = Σ
infix 2 Σ-syntax
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

∃ : ∀ {A : Set} (B : A → Set) → Set
∃ {A} B = Σ A B

∃-syntax = ∃
syntax ∃-syntax (λ x → B) = ∃[ x ] B

∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
  ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
∃-distrib-⊎ =
  record
  { to = λ x → {!!}
  ; from = λ{ (inj₁ x) → ⟨ {!!} , {!!} ⟩ ; (inj₂ x) → {!!} }
  ; from∘to = {!!}
  ; to∘from = {!!}
  }

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
open import IO

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

seven = suc (suc (suc (suc (suc (suc (suc zero))))))

main = run (putStrLn "Hello, world!")


text:
-- Andreas, 2016-09-19, issue #2168, reported by Nisse

-- {-# OPTIONS -v tc.cover:10 #-}
-- {-# OPTIONS -v tc.cover.splittree:30 -v tc.cc:40 -v tc.cover.split.con:30 #-}

open import Common.Equality

data Three : Set where
  one two three : Three

data Bool : Set where
  true false : Bool

P : Bool → Bool → Three
P z false = one
P false = λ _ → two  -- This caused internal error during clause compilation.
P z true = three

test-one : ∀ x → P x false ≡ one
test-one true  = refl
test-one false = refl

test-two : P false true ≡ two
test-two = refl

test-three : P true true ≡ three
test-three = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Quasigroup.Bundles where

open import Algebra.Core
open import Quasigroup.Structures
open import Relation.Binary
open import Level
open import Algebra.Bundles
open import Algebra.Structures

record Pique c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infixl 7 _\\_
  infixl 7 _//_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    _\\_    : Op₂ Carrier
    _//_    : Op₂ Carrier
    ε       : Carrier
    isPique : IsPique _≈_ _∙_ _\\_ _//_ ε

  open IsPique isPique public


text:
module Issue413 where

data Bool : Set where

data ℕ : Set where
  zero : ℕ

data Type : (A : Set) → Set where
   isBool : Type Bool
   isℕ    : Type ℕ

g : (A : Set) → Type A → Type A → ℕ
g .Bool isBool isBool = zero