text:
-- Left ℤ-multiplication on groups and some of its properties
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Group.ZAction where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

open import Cubical.Data.Sigma
open import Cubical.Data.Int
  renaming (_·_ to _*_ ; _+_ to _+ℤ_ ; _-_ to _-ℤ_)
open import Cubical.Data.Nat
  hiding (_·_) renaming (_+_ to _+ℕ_)
open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.Sum

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int renaming (ℤ to ℤGroup)
open import Cubical.Algebra.Group.DirProd

open import Cubical.Relation.Nullary

private
  variable
    ℓ ℓ' : Level

open Iso
open GroupStr
open IsGroupHom

_ℤ[_]·_ : ℤ → (G : Group ℓ) → fst G → fst G
pos zero ℤ[ G' ]· g = 1g (snd G')
pos (suc n) ℤ[ G' ]· g = _·_ (snd G') g (pos n ℤ[ G' ]· g)
negsuc zero ℤ[ G' ]· g = inv (snd G') g
negsuc (suc n) ℤ[ G' ]· g =
  _·_ (snd G') (inv (snd G') g) (negsuc n ℤ[ G' ]· g)

homPresℤ· : {G : Group ℓ} {H : Group ℓ'}
         → (ϕ : GroupHom G H)
         → (x : fst G) (z : ℤ)
         → fst ϕ (z ℤ[ G ]· x) ≡ (z ℤ[ H ]· fst ϕ x)
homPresℤ· (ϕ , ϕhom) x (pos zero) = pres1 ϕhom
homPresℤ· {H = H} (ϕ , ϕhom) x (pos (suc n)) =
    pres· ϕhom _ _
  ∙ cong (_·_ (snd H) (ϕ x)) (homPresℤ· (ϕ , ϕhom) x (pos n))
homPresℤ· (ϕ , ϕhom) x (negsuc zero) = presinv ϕhom _
homPresℤ· {H = H} (ϕ , ϕhom) x (negsuc (suc n)) =
    pres· ϕhom _ _
  ∙ cong₂ (_·_ (snd H)) (presinv ϕhom x)
                        (homPresℤ· (ϕ , ϕhom) x (negsuc n))

rUnitℤ· : (G : Group ℓ) (x : ℤ) → (x ℤ[ G ]· 1g (snd G)) ≡ 1g (snd G)
rUnitℤ· G (pos zero) = refl
rUnitℤ· G (pos (suc n)) =
    cong (_·_ (snd G) (1g (snd G)))
      (rUnitℤ· G (pos n))
  ∙ lid (snd G) (1g (snd G))
rUnitℤ· G (negsuc zero) = GroupTheory.inv1g G
rUnitℤ· G (negsuc (suc n)) =
    cong₂ (_·_ (snd G)) (GroupTheory.inv1g G) (rUnitℤ· G (negsuc n))
  ∙ lid (snd G) (1g (snd G))

rUnitℤ·ℤ : (x : ℤ) → (x ℤ[ ℤGroup ]· 1) ≡ x
rUnitℤ·ℤ (pos zero) = refl
rUnitℤ·ℤ (pos (suc n)) = cong (pos 1 +ℤ_) (rUnitℤ·ℤ (pos n)) ∙ sym (pos+ 1 n)
rUnitℤ·ℤ (negsuc zero) = refl
rUnitℤ·ℤ (negsuc (suc n)) = cong (-1 +ℤ_) (rUnitℤ·ℤ (negsuc n))
                          ∙ +Comm (negsuc 0) (negsuc n)

private
  precommℤ : (G : Group ℓ) (g : fst G) (y : ℤ)
           → (snd G · (y ℤ[ G ]· g)) g ≡ (sucℤ y ℤ[ G ]· g)
  precommℤ G g (pos zero) = lid (snd G) g ∙ sym (rid (snd G) g)
  precommℤ G g (pos (suc n)) =
       sym (assoc (snd G) _ _ _)
     ∙ cong ((snd G · g)) (precommℤ G g (pos n))
  precommℤ G g (negsuc zero) = invl (snd G) g
  precommℤ G g (negsuc (suc n)) =
    sym (assoc (snd G) _ _ _)
    ∙ cong ((snd G · inv (snd G) g)) (precommℤ G g (negsuc n))
    ∙ negsucLem n
    where
    negsucLem : (n : ℕ) → (snd G · inv (snd G) g)
      (sucℤ (negsuc n) ℤ[ G ]· g)
      ≡ (sucℤ (negsuc (suc n)) ℤ[ G ]· g)
    negsucLem zero = (rid (snd G) _)
    negsucLem (suc n) = refl

module _ (G : Group ℓ) (g : fst G) where
  private
    lem : (y : ℤ) → (predℤ y ℤ[ G ]· g)
                   ≡ (snd G · inv (snd G) g) (y ℤ[ G ]· g)
    lem (pos zero) = sym (rid (snd G) _)
    lem (pos (suc n)) =
         sym (lid (snd G) ((pos n ℤ[ G ]· g)))
      ∙∙ cong (λ x → _·_ (snd G) x (pos n ℤ[ G ]· g))
              (sym (invl (snd G) g))
      ∙∙ sym (assoc (snd G) _ _ _)
    lem (negsuc n) = refl

  distrℤ· : (x y : ℤ) → ((x +ℤ y) ℤ[ G ]· g)
           ≡ _·_ (snd G) (x ℤ[ G ]· g) (y ℤ[ G ]· g)
  distrℤ· (pos zero) y = cong (_ℤ[ G ]· g) (+Comm 0 y)
                            ∙ sym (lid (snd G) _)
  distrℤ· (pos (suc n)) (pos n₁) =
      cong (_ℤ[ G ]· g) (sym (pos+ (suc n) n₁))
    ∙ cong (_·_ (snd G) g)
           (cong (_ℤ[ G ]· g) (pos+ n n₁) ∙ distrℤ· (pos n) (pos n₁))
    ∙ assoc (snd G) _ _ _
  distrℤ· (pos (suc n)) (negsuc zero) =
      distrℤ· (pos n) 0
    ∙ ((rid (snd G) (pos n ℤ[ G ]· g) ∙ sym (lid (snd G) (pos n ℤ[ G ]· g)))
    ∙ cong (λ x → _·_ (snd G) x (pos n ℤ[ G ]· g))
           (sym (invl (snd G) g)) ∙ sym (assoc (snd G) _ _ _))
    ∙ (assoc (snd G) _ _ _)
    ∙ cong (λ x → _·_ (snd G)  x (pos n ℤ[ G ]· g)) (invl (snd G) g)
    ∙ lid (snd G) _
    ∙ sym (rid (snd G) _)
    ∙ (cong (_·_ (snd G) (pos n ℤ[ G ]· g)) (sym (invr (snd G) g))
    ∙ assoc (snd G) _ _ _)
    ∙ cong (λ x → _·_ (snd G)  x (inv (snd G) g))
           (precommℤ G g (pos n))
  distrℤ· (pos (suc n)) (negsuc (suc n₁)) =
       cong (_ℤ[ G ]· g) (predℤ+negsuc n₁ (pos (suc n)))
    ∙∙ distrℤ· (pos n) (negsuc n₁)
    ∙∙ (cong (λ x → _·_ (snd G) x (negsuc n₁ ℤ[ G ]· g))
             ((sym (rid (snd G) (pos n ℤ[ G ]· g))
             ∙ cong (_·_ (snd G) (pos n ℤ[ G ]· g)) (sym (invr (snd G) g)))
           ∙∙ assoc (snd G) _ _ _
           ∙∙ cong (λ x → _·_ (snd G) x (inv (snd G) g)) (precommℤ G g (pos n)))
      ∙ sym (assoc (snd G) _ _ _))
  distrℤ· (negsuc zero) y =
      cong (_ℤ[ G ]· g) (+Comm -1 y) ∙ lem y
  distrℤ· (negsuc (suc n)) y =
       cong (_ℤ[ G ]· g) (+Comm (negsuc (suc n)) y)
    ∙∙ lem (y +negsuc n)
    ∙∙ cong (snd G · inv (snd G) g)
            (cong (_ℤ[ G ]· g) (+Comm y (negsuc n)) ∙ distrℤ· (negsuc n) y)
     ∙ (assoc (snd G) _ _ _)

GroupHomℤ→ℤpres- : (e : GroupHom ℤGroup ℤGroup) (a : ℤ)
                  → fst e (- a) ≡ - fst e a
GroupHomℤ→ℤpres- e a =
  cong (fst e) (minus≡0- a) ∙∙ presinv (snd e) a ∙∙ sym (minus≡0- _)

ℤ·≡· : (a b : ℤ) → a * b ≡ (a ℤ[ ℤGroup ]· b)
ℤ·≡· (pos zero) b = refl
ℤ·≡· (pos (suc n)) b = cong (b +ℤ_) (ℤ·≡· (pos n) b)
ℤ·≡· (negsuc zero) b = minus≡0- b
ℤ·≡· (negsuc (suc n)) b = cong₂ _+ℤ_ (minus≡0- b) (ℤ·≡· (negsuc n) b)

GroupHomℤ→ℤPres· : (e : GroupHom ℤGroup ℤGroup) (a b : ℤ)
                  → fst e (a * b) ≡ a * fst e b
GroupHomℤ→ℤPres· e a b =
  cong (fst e) (ℤ·≡· a b) ∙∙ homPresℤ· e b a ∙∙ sym (ℤ·≡· a (fst e b))

-- Generators in terms of ℤ-multiplication
-- Todo : generalise
gen₁-by : (G : Group ℓ) → (g : fst G) → Type _
gen₁-by G g = (h : fst G)
          → Σ[ a ∈ ℤ ] h ≡ (a ℤ[ G ]· g)

gen₂-by : ∀ {ℓ} (G : Group ℓ) → (g₁ g₂ : fst G) → Type _
gen₂-by G g₁ g₂ =
  (h : fst G) → Σ[ a ∈ ℤ × ℤ ] h ≡ _·_ (snd G) ((fst a) ℤ[ G ]· g₁) ((snd a) ℤ[ G ]· g₂)

Iso-pres-gen₁ : ∀ {ℓ ℓ'} (G : Group ℓ) (H : Group ℓ') (g : fst G)
  → gen₁-by G g → (e : GroupIso G H)
  → gen₁-by H (Iso.fun (fst e) g)
Iso-pres-gen₁ G H g genG is h =
    (fst (genG (Iso.inv (fst is) h)))
  , (sym (Iso.rightInv (fst is) h)
    ∙∙ cong (Iso.fun (fst is)) (snd (genG (Iso.inv (fst is) h)))
    ∙∙ (homPresℤ· (_ , snd is) g (fst (genG (Iso.inv (fst is) h)))))

Iso-pres-gen₂ : (G : Group ℓ) (H : Group ℓ') (g₁ g₂ : fst G)
  → gen₂-by G g₁ g₂ → (e : GroupIso G H)
  → gen₂-by H (Iso.fun (fst e) g₁) (Iso.fun (fst e) g₂)
fst (Iso-pres-gen₂ G H g₁ g₂ genG is h) = genG (Iso.inv (fst is) h) .fst
snd (Iso-pres-gen₂ G H g₁ g₂ genG is h) =
     sym (Iso.rightInv (fst is) h)
  ∙∙ cong (fun (fst is)) (snd (genG (Iso.inv (fst is) h)))
  ∙∙ (pres· (snd is) _ _
  ∙ cong₂ (_·_ (snd H))
          (homPresℤ· (_ , snd is) g₁ (fst (fst (genG (inv (fst is) h)))))
          (homPresℤ· (_ , snd is) g₂ (snd (fst (genG (inv (fst is) h))))))

private
  intLem₁ : (n m : ℕ) → Σ[ a ∈ ℕ ] (negsuc n * pos (suc m)) ≡ negsuc a
  intLem₁ n zero = n , ·Comm  (negsuc n) (pos 1)
  intLem₁ n (suc m) = lem _ _ .fst ,
       (·Comm (negsuc n) (pos (suc (suc m)))
    ∙∙ cong (negsuc n +ℤ_) (·Comm (pos (suc m)) (negsuc n) ∙ (intLem₁ n m .snd))
    ∙∙ lem _ _ .snd)
    where
    lem : (x y : ℕ) → Σ[ a ∈ ℕ ] negsuc x +ℤ negsuc y ≡ negsuc a
    lem zero zero = 1 , refl
    lem zero (suc y) = (suc (suc y)) , +Comm (negsuc zero) (negsuc (suc y))
    lem (suc x) zero = (suc (suc x)) , refl
    lem (suc x) (suc y) =
       (lem (suc (suc x)) y .fst)
     , (predℤ+negsuc y (negsuc (suc x)) ∙ snd ((lem (suc (suc x))) y))

  intLem₂ : (n x : ℕ)
    → Σ[ a ∈ ℕ ] ((pos (suc x)) * pos (suc (suc n)) ≡ pos (suc (suc a)))
  intLem₂ n zero = n , refl
  intLem₂ n (suc x) = lem _ _ (intLem₂ n x)
    where
    lem : (x : ℤ) (n : ℕ) → Σ[ a ∈ ℕ ] (x ≡ pos (suc (suc a)))
                  → Σ[ a ∈ ℕ ] pos n +ℤ x ≡ pos (suc (suc a))
    lem x n (a , p) = n +ℕ a
      , cong (pos n +ℤ_) p ∙ cong sucℤ (sucℤ+pos a (pos n))
         ∙ sucℤ+pos a (pos (suc n)) ∙ (sym (pos+ (suc (suc n)) a))

  ¬1=x·suc-suc : (n : ℕ) (x : ℤ) → ¬ pos 1 ≡ x * pos (suc (suc n))
  ¬1=x·suc-suc n (pos zero) p = snotz (injPos p)
  ¬1=x·suc-suc n (pos (suc n₁)) p =
    snotz (injPos (sym (cong predℤ (snd (intLem₂ n n₁))) ∙ sym (cong predℤ p)))
  ¬1=x·suc-suc n (negsuc n₁) p = posNotnegsuc _ _ (p ∙ intLem₁ _ _ .snd)

GroupEquivℤ-pres1 : (e : GroupEquiv ℤGroup ℤGroup) (x : ℤ)
  → (fst (fst e) 1) ≡ x → abs (fst (fst e) 1) ≡ 1
GroupEquivℤ-pres1 e (pos zero) p =
  ⊥-rec (snotz (injPos (sym (retEq (fst e) 1)
            ∙∙ (cong (fst (fst (invGroupEquiv e))) p)
            ∙∙ IsGroupHom.pres1 (snd (invGroupEquiv e)))))
GroupEquivℤ-pres1 e (pos (suc zero)) p = cong abs p
GroupEquivℤ-pres1 e (pos (suc (suc n))) p =
  ⊥-rec (¬1=x·suc-suc _ _ (h3 ∙ ·Comm (pos (suc (suc n))) (invEq (fst e) 1)))
  where
  h3 : pos 1 ≡ _
  h3 = sym (retEq (fst e) 1)
    ∙∙ cong (fst (fst (invGroupEquiv e)))
            (p ∙ ·Comm 1 (pos (suc (suc n))))
    ∙∙ GroupHomℤ→ℤPres· (_ , snd (invGroupEquiv e)) (pos (suc (suc n))) 1
GroupEquivℤ-pres1 e (negsuc zero) p = cong abs p
GroupEquivℤ-pres1 e (negsuc (suc n)) p = ⊥-rec (¬1=x·suc-suc _ _ lem₂)
  where
  lem₁ : fst (fst e) (negsuc zero) ≡ pos (suc (suc n))
  lem₁ = GroupHomℤ→ℤpres- (_ , snd e) (pos 1) ∙ cong -_ p

  compGroup : GroupEquiv ℤGroup ℤGroup
  fst compGroup = isoToEquiv (iso -_ -_ -Involutive -Involutive)
  snd compGroup = makeIsGroupHom -Dist+

  compHom : GroupEquiv ℤGroup ℤGroup
  compHom = compGroupEquiv compGroup e

  lem₂ : pos 1 ≡ invEq (fst compHom) (pos 1) * pos (suc (suc n))
  lem₂ = sym (retEq (fst compHom) (pos 1))
     ∙∙ cong (invEq (fst compHom)) lem₁
     ∙∙ (cong (invEq (fst compHom)) (·Comm (pos 1) (pos (suc (suc n))))
       ∙ GroupHomℤ→ℤPres· (_ , (snd (invGroupEquiv compHom)))
                           (pos (suc (suc n))) (pos 1)
       ∙ ·Comm (pos (suc (suc n))) (invEq (fst compHom) (pos 1)))

groupEquivPresGen : ∀ {ℓ} (G : Group ℓ) (ϕ : GroupEquiv G ℤGroup) (x : fst G)
              → (fst (fst ϕ) x ≡ 1) ⊎ (fst (fst ϕ) x ≡ - 1)
              → (ψ : GroupEquiv G ℤGroup)
              → (fst (fst ψ) x ≡ 1) ⊎ (fst (fst ψ) x ≡ - 1)
groupEquivPresGen G (ϕeq , ϕhom) x (inl r) (ψeq , ψhom) =
     abs→⊎ _ _ (cong abs (cong (fst ψeq) (sym (retEq ϕeq x)
               ∙ cong (invEq ϕeq) r))
   ∙ GroupEquivℤ-pres1 (compGroupEquiv
                         (invGroupEquiv (ϕeq , ϕhom)) (ψeq , ψhom)) _ refl)
groupEquivPresGen G (ϕeq , ϕhom) x (inr r) (ψeq , ψhom) =
  abs→⊎ _ _
    (cong abs (cong (fst ψeq) (sym (retEq ϕeq x) ∙ cong (invEq ϕeq) r))
    ∙ cong abs (IsGroupHom.presinv
                (snd (compGroupEquiv (invGroupEquiv (ϕeq , ϕhom))
                       (ψeq , ψhom))) 1)
    ∙ absLem _ (GroupEquivℤ-pres1
                (compGroupEquiv (invGroupEquiv (ϕeq , ϕhom)) (ψeq , ψhom))
                 _ refl))
  where
  absLem : ∀ x → abs x ≡ 1 → abs (pos 0 -ℤ x) ≡ 1
  absLem (pos zero) p = ⊥-rec (snotz (sym p))
  absLem (pos (suc zero)) p = refl
  absLem (pos (suc (suc n))) p = ⊥-rec (snotz (cong predℕ p))
  absLem (negsuc zero) p = refl
  absLem (negsuc (suc n)) p = ⊥-rec (snotz (cong predℕ p))

gen₂ℤ×ℤ : gen₂-by (DirProd ℤGroup ℤGroup) (1 , 0) (0 , 1)
fst (gen₂ℤ×ℤ (x , y)) = x , y
snd (gen₂ℤ×ℤ (x , y)) =
  ΣPathP ((cong₂ _+ℤ_ ((·Comm 1 x) ∙ cong fst (sym (distrLem 1 0 x)))
                     ((·Comm 0 y) ∙ cong fst (sym (distrLem 0 1 y))))
        , +Comm y 0
         ∙ cong₂ _+ℤ_ (·Comm 0 x ∙ cong snd (sym (distrLem 1 0 x)))
                     (·Comm 1 y ∙ cong snd (sym (distrLem 0 1 y))))
  where
  ℤ×ℤ = DirProd ℤGroup ℤGroup
  _+''_ = GroupStr._·_ (snd ℤ×ℤ)

  -lem : (x : ℤ) → - x ≡ 0 -ℤ x
  -lem (pos zero) = refl
  -lem (pos (suc zero)) = refl
  -lem (pos (suc (suc n))) =
    cong predℤ (-lem (pos (suc n)))
  -lem (negsuc zero) = refl
  -lem (negsuc (suc n)) = cong sucℤ (-lem (negsuc n))

  distrLem : (x y : ℤ) (z : ℤ)
         → Path (ℤ × ℤ) (z ℤ[ ℤ×ℤ ]· (x , y)) (z * x , z * y)
  distrLem x y (pos zero) = refl
  distrLem x y (pos (suc n)) =
    (cong ((x , y) +''_) (distrLem x y (pos n)))
  distrLem x y (negsuc zero) = ΣPathP (sym (-lem x) , sym (-lem y))
  distrLem x y (negsuc (suc n)) =
    cong₂ _+''_ (ΣPathP (sym (-lem x) , sym (-lem y)))
                (distrLem x y (negsuc n))

max_stars_repo_name: ecavallo/cubical

max_issues_repo_name: ecavallo/cubical

max_forks_repo_name: ecavallo/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Monad syntax for the TC monad
------------------------------------------------------------------------

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

module Reflection.TypeChecking.MonadSyntax where

open import Agda.Builtin.Reflection
open import Level using (Level)

private
  variable
    a b : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Monad syntax

pure : A → TC A
pure = returnTC
{-# INLINE pure #-}

infixl 3 _<|>_
_<|>_ : TC A → TC A → TC A
_<|>_ = catchTC
{-# INLINE _<|>_ #-}

infixl 1 _>>=_ _>>_ _<&>_
_>>=_ : TC A → (A → TC B) → TC B
_>>=_ = bindTC
{-# INLINE _>>=_ #-}

_>>_ : TC A → TC B → TC B
xs >> ys = bindTC xs (λ _ → ys)
{-# INLINE _>>_ #-}

infixl 4 _<$>_ _<*>_ _<$_
_<*>_ : TC (A → B) → TC A → TC B
fs <*> xs = bindTC fs (λ f → bindTC xs (λ x → returnTC (f x)))
{-# INLINE _<*>_ #-}

_<$>_ : (A → B) → TC A → TC B
f <$> xs = bindTC xs (λ x → returnTC (f x))
{-# INLINE _<$>_ #-}

_<$_ : A → TC B → TC A
x <$ xs = bindTC xs (λ _ → returnTC x)
{-# INLINE _<$_ #-}

_<&>_ : TC A → (A → B) → TC B
xs <&> f = bindTC xs (λ x → returnTC (f x))
{-# INLINE _<&>_ #-}

ext: agda


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

open import HoTT
open import homotopy.HSpace
open import homotopy.EM1HSpace
open import homotopy.EilenbergMacLane1 using (EM₁-level₁)
open import lib.types.TwoSemiCategory
open import lib.two-semi-categories.FundamentalCategory

module homotopy.EM1HSpaceAssoc where

module EM₁HSpaceAssoc {i} (G : AbGroup i) where

  private
    module G = AbGroup G
  open EM₁HSpace G public
  private
    module H-⊙EM₁ = HSpaceStructure H-⊙EM₁

  mult-loop-assoc : (g : G.El) (y z : EM₁ G.grp)
    → mult-loop g (mult y z) == ap (λ x' → mult x' z) (mult-loop g y)
  mult-loop-assoc g y z =
    EM₁-prop-elim {P = λ y → mult-loop g (mult y z) == ap (λ x' → mult x' z) (mult-loop g y)}
                  {{λ y → has-level-apply (has-level-apply (EM₁-level₁ G.grp) _ _) _ _}}
                  base' y
    where
    base' : mult-loop g (mult embase z) == ap (λ x' → mult x' z) (mult-loop g embase)
    base' = ! (mult-emloop-β g z)

  H-⊙EM₁-assoc : (x y z : EM₁ G.grp) → mult (mult x y) z == mult x (mult y z)
  H-⊙EM₁-assoc x y z =
    EM₁-set-elim {P = λ x → mult (mult x y) z == mult x (mult y z)}
                 {{λ x → has-level-apply (EM₁-level₁ G.grp) _ _}}
                 idp
                 comp'
                 x
    where
      abstract
        comp' : (g : G.El) → idp == idp [ (λ x → mult (mult x y) z == mult x (mult y z)) ↓ emloop g ]
        comp' g =
          ↓-='-in $
          idp ∙' ap (λ x → mult x (mult y z)) (emloop g)
            =⟨ ∙'-unit-l _ ⟩
          ap (λ x → mult x (mult y z)) (emloop g)
            =⟨ mult-emloop-β g (mult y z) ⟩
          mult-loop g (mult y z)
            =⟨ mult-loop-assoc g y z ⟩
          ap (λ v → mult v z) (mult-loop g y)
            =⟨ ap (ap (λ v → mult v z)) (! (mult-emloop-β g y)) ⟩
          ap (λ v → mult v z) (ap (λ x → mult x y) (emloop g))
            =⟨ ∘-ap (λ v → mult v z) (λ x → mult x y) (emloop g) ⟩
          ap (λ x → mult (mult x y) z) (emloop g)
            =⟨ ! (∙-unit-r _) ⟩
          ap (λ x → mult (mult x y) z) (emloop g) ∙ idp =∎

  H-EM₁-assoc-coh-unit-l : coh-unit-l H-⊙EM₁ H-⊙EM₁-assoc
  H-EM₁-assoc-coh-unit-l x y = =ₛ-in idp

  H-EM₁-assoc-coh-unit-r : coh-unit-r H-⊙EM₁ H-⊙EM₁-assoc
  H-EM₁-assoc-coh-unit-r =
    EM₁-prop-elim {P = λ x → ∀ y → P x y} {{λ x → Π-level (P-level x)}}
      (EM₁-prop-elim {P = P embase} {{P-level embase}} (=ₛ-in idp))
    where
    P : EM₁ G.grp → EM₁ G.grp → Type i
    P = coh-unit-r-eq H-⊙EM₁ H-⊙EM₁-assoc
    P-level : ∀ x y → is-prop (P x y)
    P-level x y = =ₛ-level (EM₁-level₁ G.grp)

  H-EM₁-assoc-coh-unit-l-r-pentagon : coh-unit-l-r-pentagon H-⊙EM₁ H-⊙EM₁-assoc
  H-EM₁-assoc-coh-unit-l-r-pentagon =
    coh-unit-l-to-unit-l-r-pentagon H-⊙EM₁ H-⊙EM₁-assoc H-EM₁-assoc-coh-unit-l

  import homotopy.Pi2HSuspCompose H-⊙EM₁ H-⊙EM₁-assoc H-EM₁-assoc-coh-unit-l-r-pentagon as Pi2EMSuspCompose
  open Pi2EMSuspCompose hiding (comp-functor) public

  abstract
    H-EM₁-assoc-pentagon : coh-assoc-pentagon H-⊙EM₁ H-⊙EM₁-assoc
    H-EM₁-assoc-pentagon w x y z =
      EM₁-prop-elim {P = λ w' → P w' x y z} {{λ w' → P-level w' x y z}}
        (EM₁-prop-elim {P = λ x' → P embase x' y z} {{λ x' → P-level embase x' y z}} (=ₛ-in idp) x)
        w
      where
      P : (w x y z : EM₁ G.grp) → Type i
      P = coh-assoc-pentagon-eq H-⊙EM₁ H-⊙EM₁-assoc
      P-level : ∀ w x y z → is-prop (P w x y z)
      P-level w x y z = =ₛ-level (EM₁-level₁ G.grp)

  EM₁-2-semi-category : TwoSemiCategory lzero i
  EM₁-2-semi-category = HSpace-2-semi-category H-⊙EM₁ H-⊙EM₁-assoc H-EM₁-assoc-pentagon

  comp-functor :
    TwoSemiFunctor
      EM₁-2-semi-category
      (=ₜ-fundamental-cat (Susp (EM₁ G.grp)))
  comp-functor =
    record
    { F₀ = λ _ → [ north ]
    ; F₁ = λ x → [ η x ]
    ; pres-comp = comp
    ; pres-comp-coh = comp-coh
    }
    -- this is *exactly* the same as
    --   `Pi2EMSuspCompose.comp-functor H-EM₁-assoc-pentagon`
    -- inlined but Agda chokes on this shorter definition

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module Vec where

open import Basics
open import Ix
open import All
open import Cutting
open import Tensor

data Vec (X : Set) : Nat -> Set where
  [] : Vec X zero
  _,-_ : forall {n} -> X -> Vec X n -> Vec X (suc n)

_+V_ : forall {X n m} -> Vec X n -> Vec X m -> Vec X (n +N m)
[]        +V ys = ys
(x ,- xs) +V ys = x ,- (xs +V ys)

record Applicative (F : Set -> Set) : Set1 where
  field
    pure : {X : Set} -> X -> F X
    _<*>_ : {S T : Set} -> F (S -> T) -> F S -> F T
  infixl 2 _<*>_

VecAppl : (n : Nat) -> Applicative \ X -> Vec X n
Applicative.pure (VecAppl zero)    x = []
Applicative.pure (VecAppl (suc n)) x = x ,- Applicative.pure (VecAppl n) x
Applicative._<*>_ (VecAppl .zero)    []        []        = []
Applicative._<*>_ (VecAppl .(suc _)) (f ,- fs) (s ,- ss) =
  f s ,- Applicative._<*>_ (VecAppl _) fs ss

module VTRAVERSE {F}(A : Applicative F) where

  open Applicative A

  vtraverse : forall {n S T} -> (S -> F T) -> Vec S n -> F (Vec T n)
  vtraverse f []        = pure []
  vtraverse f (s ,- ss) = pure _,-_ <*> f s <*> vtraverse f ss

Matrix : Set -> Nat * Nat -> Set
Matrix X (i , j) = Vec (Vec X i) j

xpose : forall {X ij} -> Matrix X ij -> Matrix X (swap ij)
xpose = vtraverse id where
  open VTRAVERSE (VecAppl _)

module VECALL {I : Set}{P : I -> Set}{n : Nat}where

  open Applicative (VecAppl n)

  vecAll : {is : List I} ->
         All (\ i -> Vec (P i) n) is -> Vec (All P is) n
  vecAll {[]} pss = pure <>
  vecAll {i ,- is} (ps , pss) = pure _,_ <*> ps <*> vecAll pss

  VecLiftAlg : (C : I |> I) ->
             Algebra (Cutting C) P ->
             Algebra (Cutting C) (\ i -> Vec (P i) n)
  VecLiftAlg C alg i (c 8>< pss) = pure (alg i << (c 8><_)) <*> vecAll pss

open VECALL

NatCutVecAlg : {X : Set} -> Algebra (Cutting NatCut) (Vec X)
NatCutVecAlg {X} .(m +N n) (m , n , refl .(m +N n) 8>< xm , xn , <>) = xm +V xn

open RECTANGLE

NatCut2DMatAlg : {X : Set} -> Algebra (Cutting RectCut) (Matrix X)
NatCut2DMatAlg _ (inl c 8>< ms) = VecLiftAlg NatCut NatCutVecAlg _ (c 8>< ms)
NatCut2DMatAlg _ (inr c 8>< ms) = NatCutVecAlg _ (c 8>< ms)

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


text:
------------------------------------------------------------------------------
-- Test the consistency of FOTC.Relation.Binary.Bisimilarity.Type
------------------------------------------------------------------------------

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

-- In the module FOTC.Relation.Binary.Bisimilarity.Type we declare
-- Agda postulates as first-order logic axioms. We test if it is
-- possible to prove unprovable theorems from these axioms.

module FOTC.Relation.Binary.Bisimilarity.Consistency.Axioms where

open import FOTC.Base
open import FOTC.Relation.Binary.Bisimilarity.Type

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

postulate impossible : ∀ d e → d ≡ e
{-# ATP prove impossible #-}

postulate ≡→≈ : ∀ {xs ys} → xs ≡ ys → xs ≈ ys
{-# ATP prove ≡→≈ #-}

postulate ≈→≡ : ∀ {xs ys} → xs ≈ ys → xs ≡ ys
{-# ATP prove ≈→≡ #-}

postulate ≉→≢ : ∀ {xs ys} → xs ≉ ys → xs ≢ ys
{-# ATP prove ≉→≢ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Math.NumberTheory.Product.Nat where

-- agda-stdlib
open import Data.Nat.Properties

-- agda-misc
open import Math.NumberTheory.Product.Generic

open MonoidProduct *-1-monoid public


text:
open import Prelude

module Implicits.Syntax.Context where

open import Implicits.Syntax.Type
open import Data.List.All
open import Data.Vec
open import Data.List

Ctx : ℕ → ℕ → Set
Ctx ν n = Vec (Type ν) n

ICtx : ℕ → Set
ICtx ν = List (Type ν)

-- wellformed implicit contexts
_⊢OK : ∀ {ν} → ICtx ν → Set
Δ ⊢OK = All (λ a → List.[] ⊢unamb a) Δ

Ktx : ℕ → ℕ → Set
Ktx ν n = Ctx ν n × ICtx ν

_∷Γ_ : ∀ {ν n} → Type ν → Ktx ν n → Ktx ν (suc n)
a ∷Γ (Γ , Δ) = (a ∷ Γ) , Δ

_∷Δ_ : ∀ {ν n} → Type ν → Ktx ν n → Ktx ν n
a ∷Δ (Γ , Δ) = Γ , a List.∷ Δ

_∷K_ : ∀ {ν n} → Type ν → Ktx ν n → Ktx ν (suc n)
a ∷K (Γ , Δ) = a ∷ Γ , a List.∷ Δ

nil : ∀ {ν} → Ktx ν 0
nil = [] , List.[]


text:
------------------------------------------------------------------------------
-- Distributive laws on a binary operation (Stanovský example)
------------------------------------------------------------------------------

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

module DistributiveLaws.README where

------------------------------------------------------------------------------
-- Description

-- Let _·_ be a left-associative binary operation which satifies the
-- left and right distributive axioms:
--
-- ∀ x y z → x ∙ (y ∙ z) ≡ (x ∙ y) ∙ (x ∙ z)
-- ∀ x y z → (x ∙ y) ∙ z ≡ (x ∙ z) ∙ (y ∙ z).

-- We prove some properties of Stanovský (2008): Task B, Lemma 3,
-- Lemma 4, Lemma 5 (Task A) and Lemma 6.

------------------------------------------------------------------------------
-- The axioms
open import DistributiveLaws.Base

-- The interactive and combined proofs
open import DistributiveLaws.Lemma3-ATP
open import DistributiveLaws.Lemma4-ATP
open import DistributiveLaws.Lemma5-ATP
open import DistributiveLaws.Lemma6-ATP
open import DistributiveLaws.TaskB-AllStepsATP
open import DistributiveLaws.TaskB-HalvedStepsATP
open import DistributiveLaws.TaskB-I
open import DistributiveLaws.TaskB-TopDownATP

-- Unproven theorem by the ATPs
open import DistributiveLaws.TaskB.UnprovedATP

------------------------------------------------------------------------------
-- References:
--
-- Stanovský, David (2008). Distributive Groupoids are
-- Symmetrical-by-Medial: An Elementary Proof. Commentations
-- Mathematicae Universitatis Carolinae 49.4, pp. 541–546.


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

open import Sets.EquivalenceRelations
open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Modules.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Lists.Lists
open import Vectors
open import Groups.Definition
open import Orders.Total.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Rings.Homomorphisms.Definition

module Modules.PolynomialModule {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open Ring R
open import Groups.Polynomials.Definition additiveGroup
open import Groups.Polynomials.Group additiveGroup
open import Rings.Polynomial.Multiplication R
open import Rings.Polynomial.Evaluation R
open import Rings.Polynomial.Ring R
open import Rings.Lemmas polyRing

polynomialRingModule : Module R abelianUnderlyingGroup (λ a b → _*P_ (polyInjection a) b)
Module.dotWellDefined (polynomialRingModule) r=s t=u = Ring.*WellDefined polyRing (r=s ,, record {}) t=u
Module.dotDistributesLeft (polynomialRingModule) {r} {s} {t} = Ring.*DistributesOver+ polyRing {polyInjection r} {s} {t}
Module.dotDistributesRight (polynomialRingModule) {r} {s} {t} = Ring.*DistributesOver+' polyRing {polyInjection r} {polyInjection s} {t}
Module.dotAssociative (polynomialRingModule) {r} {s} {t} = Equivalence.transitive (Setoid.eq naivePolySetoid) (Ring.*WellDefined polyRing m (Equivalence.reflexive (Setoid.eq naivePolySetoid) {t})) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Ring.*Associative polyRing {polyInjection r} {polyInjection s} {t}))
  where
    m : Setoid._∼_ naivePolySetoid ((r * s) :: []) ((r * s) :: (([] +P []) +P (0R :: [])))
    m = Equivalence.reflexive (Setoid.eq S) ,, (Equivalence.reflexive (Setoid.eq S) ,, record {})
Module.dotIdentity (polynomialRingModule) = Ring.identIsIdent polyRing

open import Modules.Span polynomialRingModule

polynomialBasis : ℕ → NaivePoly
polynomialBasis zero = polyInjection 1R
polynomialBasis (succ a) = 0R :: polynomialBasis a

count : (n : ℕ) → Vec ℕ n
count zero = []
count (succ n) = 0 ,- vecMap succ (count n)

lemma : {d : _} {D : Set d} → (f : D → List A) → {n : ℕ} → (m : Vec D n) (r : Vec A n)  → Setoid._∼_ naivePolySetoid (dot (vecMap (λ i → 0R :: f i) m) r) (0R :: dot (vecMap f m) r)
lemma f [] [] = reflexive ,, record {}
  where
    open Setoid S
    open Equivalence eq
lemma f (m ,- ms) (r ,- rs) rewrite refl {x = 0} = transitive (+WellDefined {(r * 0R) :: (((map (_*_ r) (f m)) +P []) +P (0R :: []))} {_} {(r * 0R) :: (((map (_*_ r) (f m)) +P []) +P (0R :: []))} (reflexive {(r * 0R) :: (((map (_*_ r) (f m)) +P []) +P (0R :: []))}) (lemma f ms rs)) (Equivalence.transitive (Setoid.eq S) (Group.identRight additiveGroup) (Ring.timesZero R) ,, +WellDefined {((map (_*_ r) (f m)) +P []) +P (0R :: [])} {dot (vecMap f ms) rs} {(r :: []) *P f m} {dot (vecMap f ms) rs} t (reflexive {dot (vecMap f ms) rs}))
  where
    open Setoid naivePolySetoid
    open Equivalence eq
    open Group polyGroup
    lemm : (v : List A) → polysEqual (map (_*_ r) v) ((r :: []) *P v)
    lemm [] = record {}
    lemm (x :: v) = Equivalence.reflexive (Setoid.eq S) ,, symmetric (transitive (+WellDefined {map (_*_ r) v +P []} {0R :: []} {_} {[]} reflexive (Equivalence.reflexive (Setoid.eq S) ,, record {})) (transitive (identRight {(map (_*_ r) v) +P []}) (identRight {map (_*_ r) v})))
    t : ((map (_*_ r) (f m) +P []) +P (0R :: [])) ∼ ((r :: []) *P f m)
    t = transitive (+WellDefined {map (_*_ r) (f m) +P []} {0R :: []} {_} {[]} reflexive (Equivalence.reflexive (Setoid.eq S) ,, record {})) (transitive (identRight {map (_*_ r) (f m) +P []}) (transitive (identRight {map (_*_ r) (f m)}) (lemm (f m))))

identityMap : (v : List A) → Setoid._∼_ naivePolySetoid (dot (vecMap polynomialBasis (count (length v))) (listToVec v)) v
identityMap [] = record {}
identityMap (x :: v) rewrite vecMapCompose succ polynomialBasis (count (length v)) = transitive (+WellDefined {(x * 1R) :: Group.0G additiveGroup :: []} {dot (vecMap (λ i → Group.0G additiveGroup :: polynomialBasis i) (count (length v))) (listToVec v)} {(x * 1R) :: 0R :: []} {0R :: dot (vecMap polynomialBasis (count (length v))) (listToVec v)} (reflexive {(x * 1R) :: 0R :: []}) (lemma polynomialBasis (count (length v)) (listToVec v))) (Equivalence.transitive (Setoid.eq S) (Group.identRight additiveGroup) (Equivalence.transitive (Setoid.eq S) *Commutative identIsIdent) ,, transitive (+WellDefined {0R :: []} {dot (vecMap polynomialBasis (count (length v))) (listToVec v)} {[]} (Equivalence.reflexive (Setoid.eq S) ,, record {}) reflexive) (transitive identLeft (identityMap v)))
  where
    open Group polyGroup
    open Setoid naivePolySetoid
    open Equivalence eq

polynomialBasisSpans : Spans polynomialBasis
polynomialBasisSpans m = length m , ((count (length m) ,, listToVec m) , identityMap m)

{-
private
  indepWithZero : {n : ℕ} (rs : Vec ℕ n) (indicesDistinct : {a b : ℕ} → (a<n : a <N succ n) (b<n : b <N succ n) → vecIndex (0 ,- rs) a a<n ≡ vecIndex (0 ,- rs) b b<n → a ≡ b) (b : A) (bs : Vec A n) (dotZero : Setoid._∼_ naivePolySetoid (((b * 1R) :: 0R :: []) +P (dot (vecMap polynomialBasis rs) bs)) []) → (nonzero : {a : ℕ} → (a<n : a <N n) → 0 <N vecIndex rs a a<n) → Setoid._∼_ S 0R b && _=V_ additiveGroup (vecPure 0R) bs
  indepWithZero rs indicesDistinct b bs dotZero indicesNonzero = symmetric b=0 ,, {!!}
    where
      open Setoid S
      open Equivalence eq
      open Group additiveGroup
      t : (inducedFunction (((b * 1R) :: 0R :: []) +P (dot (vecMap polynomialBasis rs) bs)) 0R) ∼ 0R
      t = inducedFunctionWellDefined dotZero 0R
      u : ((inducedFunction ((b * 1R) :: 0R :: []) 0R) + inducedFunction (dot (vecMap polynomialBasis rs) bs) 0R) ∼ 0R
      u = transitive (symmetric (GroupHom.groupHom (RingHom.groupHom (inducedFunctionIsHom 0R)) {((b * 1R) :: 0R :: [])} {dot (vecMap polynomialBasis rs) bs})) t
      b=0 : b ∼ 0R
      b=0 = transitive (symmetric (transitive (+WellDefined (transitive (transitive (transitive (+WellDefined reflexive (transitive *Commutative timesZero)) identRight) *Commutative) identIsIdent) {!imageOfIdentityIsIdentity (RingHom.groupHom (inducedFunctionIsHom 0R))!}) (identRight {b}))) u

polynomialBasisIndependent : Independent polynomialBasis
polynomialBasisIndependent [] indicesDistinct [] dotZero = record {}
polynomialBasisIndependent {succ n} (zero ,- rs) indicesDistinct (b ,- bs) dotZero = indepWithZero rs indicesDistinct b bs dotZero t
  where
    t : {a : ℕ} (a<n : a <N n) → 0 <N vecIndex rs a a<n
    t {a} a<n with TotalOrder.totality ℕTotalOrder 0 (vecIndex rs a a<n)
    t {a} a<n | inl (inl x) = x
    t {a} a<n | inr x with indicesDistinct {succ a} {0} (succPreservesInequality a<n) (succIsPositive n) (equalityCommutative x)
    ... | ()
polynomialBasisIndependent (succ r ,- rs) indicesDistinct (b ,- bs) dotZero = {!!}
  where
    rearr : {!!}
    rearr = {!!}

-}


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

-- 2014-05-27 Jesper and Andreas

postulate
  A B : Set
  R   : A → B → Set

{-# BUILTIN REWRITE R #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

open import lib.Basics
open import lib.NConnected
open import lib.NType2
open import lib.types.Truncation

open import Coequalizers.Definition
open import Coequalizers.Misc

open import Graphs.Definition

open import Util.Misc

module Groups.Definition where

{- BG has the structure of a type theoretic group if it is pointed, connected and
   1-truncated.
-}
record TTGroup {i : ULevel} (BG : Type i) : Type i where
  field
    base : BG
    ⦃ gp-conn ⦄ : is-connected 0 BG
    ⦃ gp-trunc ⦄ : is-gpd BG

open TTGroup ⦃...⦄ public

{- Some functions related to free higher groups (which we never define explicitly). -}
module _ {i : ULevel} {A : Type i} where
  instance -- Whenever we need a pair of maps A ⇉ 1 they are defined as follows
    gph-fhg : Graph A Unit
    gph-fhg = record { π₀ = λ _ → unit ; π₁ = λ _ → unit }

    conn-fhg : is-connected 0 (⊤ / A)
    conn-fhg = has-level-in ([ c[ unit ] ] , Trunc-elim (λ x → Trunc-rec (λ { (t , p) → ap [_] p}) (quotient-map-is-surj x)))

  fhg-base : ⊤ / A
  fhg-base = c[ unit ]

{- The definition of a free group. -}
FreeGroup : {i : ULevel} (A : Type i) → Type i
FreeGroup A = ∥ ⊤ / A ∥₁

instance -- free groups are groups
  free-gp-str : {i : ULevel} {A : Type i} → TTGroup (FreeGroup A)
  free-gp-str = record { base = [ fhg-base ] }

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
module CTL.Proof where

open import CTL.Proof.AG public
open import CTL.Proof.EG public

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
module ReflectionExposeConstraints where

open import Agda.Builtin.Reflection
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Equality

_>>=_ : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
_>>=_ = bindTC

_ifMeta_ : {A : Set} → Term → (Meta → TC A) → TC A
meta x x₁ ifMeta f = f x
_ ifMeta _ = typeError (strErr "Error1" ∷ [])

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

foo : Constraint → TC Term
foo (valueCmp cmpEq y t1 (def f args)) = returnTC (def f [])
foo _ = typeError (strErr "Error2" ∷ [])

q : Nat → Nat
q zero = 4
q (suc x) = 4

macro
  mfun : Term → TC ⊤
  mfun hole
     = delayMacro >>= (λ _ →
         hole ifMeta (λ x → do
                              c ← getConstraintsMentioning (x ∷ [])
                              case c of
                                λ {[] → typeError (strErr "Error3" ∷ [])
                                  ; (c ∷ cs) → do
                                                 g ← foo c
                                                 unify hole g }
                              ))
postulate
  g : (Q : Nat → Nat) → ∀ k → Q k ≡ 4

f : ∀ k → q k ≡ 4
f k = g mfun k

max_stars_repo_name: xekoukou/agda

max_issues_repo_name: xekoukou/agda

max_forks_repo_name: xekoukou/agda


text:
open import Relation.Unary
open import Relation.Ternary.Separation

module Relation.Ternary.Separation.Monad.Free {ℓ} {A : Set ℓ}
  {{r : RawSep A}}
  (Cmd : Pred A ℓ)
  (δ   : ∀ {Φ} → Cmd Φ → Pred A ℓ)
  where

open import Level
open import Function
open import Data.Unit
open import Data.Product
open import Relation.Unary.PredicateTransformer using (PT)
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad
open import Relation.Binary.PropositionalEquality

mutual
  Cont : ∀ {Δ} → Cmd Δ → Pred A ℓ → Pred A ℓ
  Cont c P = δ c ─✴ Free P

  data Free : PT A A ℓ ℓ where
    pure   : ∀ {P}   → ∀[ P ⇒ Free P ]
    impure : ∀ {P}   → ∀[ ∃[ Cmd ]✴ (λ c → Cont c P) ⇒ Free P ]

module _ {u} {{_ : IsUnitalSep r u}} where
  open Monads
  instance
    free-monad : Monad ⊤ ℓ (λ _ _ → Free)
    Monad.return free-monad = pure
    app (Monad.bind free-monad f) (pure x) σ = app f x σ
    app (Monad.bind free-monad f) (impure (cmd ×⟨ σ₁ ⟩ κ)) σ =
      let _ , σ₂ , σ₃ = ⊎-assoc σ₁ (⊎-comm σ) in
      impure (cmd ×⟨ σ₂ ⟩ wand λ resp σ₄ →
        let _ , τ₁ , τ₂ = ⊎-assoc (⊎-comm σ₃) σ₄ in
        app (bind f) (app κ resp τ₂) τ₁)

  ⟪_⟫ : ∀ {Φ} → (c : Cmd Φ) → Free (δ c) Φ
  ⟪_⟫ c =
    impure (c ×⟨ ⊎-idʳ ⟩
      wand λ r σ → case ⊎-id⁻ˡ σ of λ where refl → return r  )

module _ {B : Set ℓ} {M : PT A B ℓ ℓ} {P : Pred A ℓ}
  {{rb : RawSep B}} {u} {{_ : IsUnitalSep r u}}
  {{jm : Morphism A B}}
  {{_ : IsUnitalSep rb (Morphism.j jm u)}}
  {{ monad : Monads.Monad {{jm = jm}} ⊤ ℓ (λ _ _ → M) }}
  where

  open Morphism jm
  open Monads.Monad {{jm = jm}} monad
  open Monads {{jm = jm}} using (str; typed-str)

  open import Data.Nat

  -- Unfolding a command tree one step
  step : (cmd : ∀ {Φ} → (c : Cmd Φ) → M (δ c) (j Φ)) → ∀[ Free P ⇒ⱼ M (Free P) ]
  step cmd (pure px) = return (pure px)
  step cmd (impure (c ×⟨ σ ⟩ κ)) = do
    r ×⟨ σ ⟩ κ ← cmd c &⟨ Cont c P ∥ j-⊎ σ ⟩ κ
    return (app κ r (⊎-comm σ))

  -- A fueled generic interpreter for command trees in Free
  interpret : ℕ → ∀[ M P ] → (cmd : ∀ {Φ} → (c : Cmd Φ) → M (δ c) (j Φ)) → ∀[ Free P ⇒ⱼ M P ]
  interpret zero    def cmd f = def
  interpret (suc n) def cmd f = do
    impure f ← step cmd f
      where
        (pure v) → return v
    interpret n def cmd (impure f)


text:
module PLRTree.Complete.Correctness.Alternative {A : Set} where

open import BTree.Complete.Alternative {A}
open import BTree.Complete.Alternative.Properties {A}
open import BTree.Equality {A}
open import PLRTree {A}
open import PLRTree.Complete {A} renaming (Complete to Complete' ; _⋗_ to _⋗'_ ; _⋘_ to _⋘'_ ; _⋙_ to _⋙'_)
open import PLRTree.Equality.Correctness {A}

lemma-⋗'-⋗ : {l r : PLRTree} → l ⋗' r → forget l ⋗ forget r
lemma-⋗'-⋗ (⋗lf x) = ⋗lf x
lemma-⋗'-⋗ (⋗nd x x' l≃'r l'≃'r' l⋗'l') = ⋗nd x x'  (lemma-≃'-≃ l≃'r) (lemma-≃'-≃ l'≃'r') (lemma-⋗'-⋗ l⋗'l')

mutual
  lemma-⋘'-⋘ : {l r : PLRTree} → l ⋘' r → forget l ⋘ forget r
  lemma-⋘'-⋘ (x⋘ x y z) = lr⋘ x z (⋙lf y) ≃lf (⋗lf y)
  lemma-⋘'-⋘ (l⋘ x x' l'⋘'r' l'≃'r' r≃'l') = ll⋘ x x' (lemma-⋘'-⋘ l'⋘'r') (lemma-≃'-≃ l'≃'r') (lemma-≃'-≃ r≃'l')
  lemma-⋘'-⋘ (r⋘ x x' l'⋙'r' l'≃'r' l⋗'l') = lr⋘ x x' (lemma-⋙'-⋙ l'⋙'r') (lemma-≃'-≃ l'≃'r') (lemma-⋗'-⋗ l⋗'l')

  lemma-⋙'-⋙ : {l r : PLRTree} → l ⋙' r → forget l ⋙ forget r
  lemma-⋙'-⋙ (⋙p l⋗'r) = lemma-⋗-⋙ (lemma-⋗'-⋗ l⋗'r)
  lemma-⋙'-⋙ (⋙l x x' l≃'r l'⋘'r' l⋗'r') = ⋙rl x x' (lemma-≃'-≃ l≃'r) (lemma-⋘'-⋘ l'⋘'r') (lemma-⋗'-⋗ l⋗'r')
  lemma-⋙'-⋙ (⋙r x x' l≃'r l'⋙'r' l≃'l') = ⋙rr x x' (lemma-≃'-≃ l≃'r) (lemma-⋙'-⋙ l'⋙'r') (lemma-≃'-≃ l≃'l')

lemma-complete'-complete : {t : PLRTree} → Complete' t → Complete (forget t)
lemma-complete'-complete leaf = leaf
lemma-complete'-complete (perfect x c'l c'r l≃'r) =  left x cl cr l⋘r
                   where cl = lemma-complete'-complete c'l ;
                              cr = lemma-complete'-complete c'r ;
                              l⋘r = lemma-≃-⋘ (lemma-≃'-≃ l≃'r)
lemma-complete'-complete (left x c'l c'r l⋘'r) = left x cl cr l⋘r
                   where cl = lemma-complete'-complete c'l ;
                              cr = lemma-complete'-complete c'r ;
                              l⋘r = lemma-⋘'-⋘ l⋘'r
lemma-complete'-complete (right x c'l c'r l⋙'r) = right x cl cr l⋙r
                   where cl = lemma-complete'-complete c'l ;
                              cr = lemma-complete'-complete c'r ;
                              l⋙r = lemma-⋙'-⋙ l⋙'r

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Andreas, 2012-02-13: polarity info must be correct

{-# OPTIONS --sized-types --show-implicit #-}
-- {-# OPTIONS -v tc.size.solve:20 -v tc.conv.size:20 #-}
-- {-# OPTIONS -v tc.polarity.set:10 -v tc.conv.term.shortcut:20 #-}
module WrongPolarity where

open import Common.Size

data ⊥ : Set where

data Sink (A : Set) : Set where
  sink : (A → ⊥) → Sink A

postulate
  dump : {A : Set} → A → Sink A

-- A sized type
data Nat : {size : Size} → Set where
  zero : {size : Size} → Nat {↑ size}
  suc  : {size : Size} → Nat {size} → Nat {↑ size}

dumpNat : {i : Size} → Nat {i} → Sink (Nat {i})
dumpNat zero        = dump zero
dumpNat (suc {i} n) = dumpNat {i} n
-- should fail!
-- i != ↑ i of type Size
-- when checking that the expression dumpNat n has type Sink Nat

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso