text:
module sv20.compiler where

open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
--open import Data.Nat.DivMod using (_/_)
open import Data.List using (List; _++_; []; _∷_; head)
open import Data.Maybe as DM
open DM using (Maybe; just; nothing; maybe; _>>=_; from-just; From-just)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; subst)
open import Data.Product using (∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Function.Base using (_∘_; flip)

pattern [_] z = z ∷ []
pattern [_,_] y z = y ∷ z ∷ []
pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []

data ExOp : Set where
  sum diff prod : ExOp

data Exp : Set where
  const : ℕ → Exp
  exop : ExOp → Exp → Exp → Exp

--exop sum (const 5) (const 2)

prim-ex : ExOp → ℕ → ℕ → ℕ
prim-ex sum  = _+_
prim-ex diff = _∸_
prim-ex prod = _*_

interpreter : Exp → ℕ
interpreter (const ℕ) = ℕ
interpreter (exop op x y) = prim-ex op (interpreter x) (interpreter y)

--interpreter (exop sum (const 5) (const 2))

data BinOp : Set where
  add sub mul : BinOp

data StackCmd : Set where
  push : ℕ → StackCmd
  binop : BinOp → StackCmd

Program = List StackCmd
Stack = List ℕ

prim-op : BinOp → ℕ → ℕ → ℕ
prim-op add = _+_
prim-op sub = _∸_
prim-op mul = _*_

run-vm : Program → Stack → Maybe Stack
run-vm [] st = just st
run-vm (push n ∷ ps) st = run-vm ps (n ∷ st)
run-vm (binop op ∷ ps) (n ∷ m ∷ st) = run-vm ps ((prim-op op n m) ∷ st)
run-vm _ _ = nothing

exop-binop : ExOp → BinOp
exop-binop sum = add
exop-binop diff = sub
exop-binop prod = mul

compile : Exp → Program
compile (const n) = [ push n ]
compile (exop op x y) = compile y ++ compile x ++ [ binop (exop-binop op) ]

-- (3 - 2) + 6  =>  + (- 3 2) 6   =>  "sum (diff 3 2) 6"
_ : compile (exop sum (exop diff (const 3) (const 2)) (const 6))
    ≡ [ push 6 , push 2 , push 3 , binop sub , binop add ]
_ = refl

_ : run-vm (compile (const 3)) [] ≡ just [ interpreter (const 3) ]
_ = refl

--run-vm [ push 2 , push 1 , binop add ] []
--run-vm [ push 1 , binop add ] [ 2 ]
--run-vm [ binop add ] [ 1 , 2 ]
_ :   (run-vm [ push 1 ] [ 2 ] >>= run-vm [ binop add ])
    ≡ run-vm [ push 1 , binop add ] [ 2 ]
_ = refl

lemma₁ : ∀ (a b : Program) (s : Stack) → run-vm (a ++ b) s ≡ (run-vm a s >>= run-vm b)
lemma₁ [] _ _ = refl
lemma₁ (push n ∷ ps) b s rewrite lemma₁ ps b (n ∷ s) = refl
lemma₁ (binop _ ∷ ps) b          []  = refl
lemma₁ (binop _ ∷ _)  _     (_ ∷ []) = refl
lemma₁ (binop op ∷ ps) b (n ∷ m ∷ st) rewrite lemma₁ ps b (prim-op op n m ∷ st) = refl

lemma₂ : ∀ {op : ExOp} → prim-op (exop-binop op) ≡ prim-ex op
lemma₂ {sum} = refl
lemma₂ {diff} = refl
lemma₂ {prod} = refl

compiler-correctness₁ : ∀ {e : Exp} {s : Stack} → run-vm (compile e) s ≡ just (interpreter e ∷ s)
compiler-correctness₁ {const n} = refl
compiler-correctness₁ {exop op x y} {s}
  rewrite
--    run-vm (compile (exop op x y)) s ≡ just (interpreter (exop op x y) ∷ s)
--
--    run-vm (compile y ++ compile x ++ [ binop (exop-binop op) ]) s ≡ just (prim-ex op (interpreter x) (interpreter y) ∷ s)
    lemma₁ (compile y) (compile x ++ [ binop (exop-binop op) ]) s
--    (run-vm (compile y) s >>= run-vm (compile x ++ [ binop (exop-binop op) ])) ≡ just (prim-ex op (interpreter x) (interpreter y) ∷ s)
  | compiler-correctness₁ {y} {s}
--    (just (interpreter y ∷ s) >>= run-vm (compile x ++ [ binop (exop-binop op) ])) ≡ just (prim-ex op (interpreter x) (interpreter y) ∷ s)
--    run-vm (compile x ++ [ binop (exop-binop op) ]) (interpreter y ∷ s) ≡ just (prim-ex op (interpreter x) (interpreter y) ∷ s)
  | lemma₁ (compile x) [ binop (exop-binop op) ] (interpreter y ∷ s)
--    (run-vm (compile x) (interpreter y ∷ s) >>= run-vm [ binop (exop-binop op) ]) ≡ just (prim-ex op (interpreter x) (interpreter y) ∷ s)
  | compiler-correctness₁ {x} {interpreter y ∷ s}
--    (just (interpreter x ∷ interpreter y ∷ s) >>= run-vm [ binop (exop-binop op) ]) ≡ just (prim-ex op (interpreter x) (interpreter y) ∷ s)
--    just (prim-op (exop-binop op) (interpreter x) (interpreter y) ∷ s) ≡ just (prim-ex op (interpreter x) (interpreter y) ∷ s)
  | lemma₂ {op}
  = refl

compiler-correctness : ∀ (e : Exp) → run-vm (compile e) [] ≡ just [ interpreter e ]
compiler-correctness e = compiler-correctness₁ {e} {[]}

-- Which algorithm is it using when executed "interpreter" or "compile then
-- run-vm"?
-- Well, if I understand correctly. "from-just" will return the value
-- contained in "just" and "subst" will pass the values untouched. Which
-- would mean that there is an associated cost in proving stuff but the code
-- that is being used is "compile then run-vm"
run-vm∘compile : Exp → Maybe ℕ
run-vm∘compile e =
  let
    justln = from-just (run-vm (compile e) [])
    list = subst From-just (compiler-correctness e) justln
  in head list

_ : run-vm∘compile (const 5) ≡ just 5
_ = refl

reduce : {A : Set} → Maybe (List A) → Maybe A
reduce (just (x ∷ _)) = just x
reduce _ = nothing

_ : reduce (just [ 5 ]) ≡ just 5
_ = refl

-- Look, it is possible to execute compile and run-vm and get an unwrapped result
-- For an even prettier proof look at the end of the file
run-vm∘compile` : Exp → ℕ
run-vm∘compile` e =
  let
    computing = reduce (run-vm (compile e) [])
    justn = from-just computing
    redruncomp≡jinter = cong reduce (compiler-correctness e) -- reduce (run-vm (compile e) []) ≡ just (interpreter e)
  in subst From-just redruncomp≡jinter justn

_ : run-vm∘compile` (const 5) ≡ 5
_ = refl

---- So. I wanted to generalise the approach used before, but I'm stuck. Agda
---- seems not able to infer some variable.
---- It's because it is never using 'g', I think
---- Ans: NO. IT WAS BECAUSE x WAS IMPLICIT IN eq
--
--unwrap : {A B : Set}
--       → {g : A → B}
--       → (f : A → Maybe (List B))
--       → ({x : A} → f x ≡ just [ g x ])   -- <- This was the problem! It should be explicit!
--       --------------------------------
--       → A → B  -- Computed using f
--unwrap {A} {B} {g} f eq x =
--  let
--    computing = reduce (f x)  -- type: Maybe B
--    justb = from-just computing    -- type: From-just (f x)
--  in subst From-just new-eq justb -- type: B      -- thanks to the magic of From-just
--
--  where
--    new-eq : {x : A} → reduce (f x) ≡ just (g x)
--    new-eq {x} rewrite eq {x} = refl
--
---- Why doesn't this work!? Ans: See above or below
----run-vm∘compile`` : Exp → ℕ
----run-vm∘compile`` = unwrap {Exp} {ℕ}
----                          {interpreter}
----                          (λ e → run-vm (compile e) [])
----                          compiler-correctness

unwrap : {A B : Set} {g : A → B}
       → (f : A → Maybe (List B))
       → ((x : A) → f x ≡ just [ g x ])
       --------------------------------
       → A → B  -- Computed using f not g (g might still be run to prove the property correct)
unwrap f eq x =
  let
    -- Proof: f x ≡ just [ g x ]
    fx≡mlgx = eq x
    -- New proof: reduce (f x) ≡ just (g x)
    redfx≡gx = cong reduce {x = f x} fx≡mlgx
    compute = reduce (f x)          -- type: Maybe B
    justredfx = from-just compute       -- type: From-just (reduce (f x))  -- lifting to the type level, so we can prove stuff
  in subst From-just redfx≡gx justredfx -- type: From-just (just (g x))    which is the same as  `B`      -- thanks to the magic of From-just

--from-just (just 3)   -- evaluates to: 3
--                     -- with type:  From-just (just 3)
--                                 -- which evaluates to: ℕ
-- ie,
-- from-just (just 3) : From-just (just 3)
-- from-just (just 3) : ℕ
--                  3 : ℕ
--                  3 : From-just (just 3)

_ : from-just (just 3) ≡ 3
_ = refl

_ : From-just (just 3) ≡ ℕ
_ = refl

_ : Set
_ = From-just (just 3)

_ : From-just (just 3)  -- same as ℕ
_ = 3
_ = from-just (just 3)
_ = 2 -- This is an ℕ too

run-vm∘compile`` : Exp → ℕ
run-vm∘compile`` = unwrap ((flip run-vm []) ∘ compile) compiler-correctness
--run-vm∘compile`` = unwrap (λ e → run-vm (compile e) []) compiler-correctness

--LESSON LEARNT:
--Don't use implicit paramaters unless it makes for a clearer proof.
--Always use explicit parameters and make them implicit as you use the
--functions in more places (without breaking anything)

_ : run-vm∘compile`` (const 5) ≡ 5
_ = refl

I-am-a-number : ℕ
I-am-a-number = run-vm∘compile`` (exop sum (exop diff (const 3) (const 2)) (const 20))


text:
-- Andreas, 2016-05-06, issue 1967

postulate
  D : {{A : Set}} → Set
  test : (A : Set) → D A

-- Expected error:
-- Set should be a function type, but it isn't
-- when checking that A is a valid argument to a function of type
-- {{A = A₁ : Set}} → Set

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.DirectSum.DirectSumHIT.PseudoNormalForm where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_)
open import Cubical.Data.Sigma
open import Cubical.Data.List
open import Cubical.Data.Vec.DepVec

open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.AbGroup.Instances.DirectSumHIT
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base

private variable
  ℓ : Level

open AbGroupStr
open AbGroupTheory

-----------------------------------------------------------------------------
-- Notation

module DefPNF
  (G : (n : ℕ) → Type ℓ)
  (Gstr : (n : ℕ) → AbGroupStr (G n))
  where

  open AbGroupStr (snd (⊕HIT-AbGr ℕ G Gstr)) using ()
    renaming
    ( 0g       to 0⊕HIT
    ; _+_      to _+⊕HIT_
    ; -_       to -⊕HIT_
    ; +Assoc    to +⊕HIT-Assoc
    ; +IdR     to +⊕HIT-IdR
    ; +IdL     to +⊕HIT-IdL
    ; +InvR    to +⊕HIT-InvR
    ; +InvL    to +⊕HIT-InvL
    ; +Comm     to +⊕HIT-Comm
    ; is-set   to isSet⊕HIT)

-----------------------------------------------------------------------------
-- Lemma

  -- def pseudo normal form
  sumHIT : {n : ℕ} → depVec G n → ⊕HIT ℕ G Gstr
  sumHIT {0} ⋆ = 0⊕HIT
  sumHIT {suc n} (a □ dv) = (base n a) +⊕HIT (sumHIT dv)

  -- 0 and sum
  replicate0g : (n : ℕ) → depVec G n
  replicate0g (zero) = ⋆
  replicate0g (suc n) = (0g (Gstr n)) □ (replicate0g n)

  sumHIT0g : (n : ℕ) → sumHIT (replicate0g n) ≡ 0⊕HIT
  sumHIT0g (zero) = refl
  sumHIT0g (suc n) = cong₂ _+⊕HIT_ (base-neutral n) (sumHIT0g n)
                     ∙ +⊕HIT-IdL _

  -- extension and sum
  extendDVL : (k l : ℕ) → (dv : depVec G l) → depVec G (k +n l)
  extendDVL zero  l dv = dv
  extendDVL (suc k) l dv = (0g (Gstr (k +n l))) □ (extendDVL k l dv)

  extendDVLeq : (k l : ℕ) → (dv : depVec G l) → sumHIT (extendDVL k l dv) ≡ sumHIT dv
  extendDVLeq (zero)  l dv = refl
  extendDVLeq (suc k) l dv = cong (λ X → X +⊕HIT sumHIT (extendDVL k l dv)) (base-neutral (k +n l))
                             ∙ +⊕HIT-IdL _
                             ∙ extendDVLeq k l dv

  extendDVR : (k l : ℕ) → (dv : depVec G k) → depVec G (k +n l)
  extendDVR k l dv = subst (λ X → depVec G X) (+-comm l k) (extendDVL l k dv)

  extendDVReq : (k l : ℕ) → (dv : depVec G k) → sumHIT (extendDVR k l dv) ≡ sumHIT dv
  extendDVReq k l dv = J (λ m p → sumHIT (subst (λ X → depVec G X) p (extendDVL l k dv)) ≡ sumHIT dv)
                       (sumHIT (subst (λ X → depVec G X) refl (extendDVL l k dv))
                               ≡⟨ cong sumHIT (transportRefl (extendDVL l k dv)) ⟩
                       sumHIT (extendDVL l k dv)
                               ≡⟨ extendDVLeq l k dv ⟩
                       sumHIT dv ∎)
                       (+-comm l k)

  -- pointwise add
  _pt+DV_ : {n : ℕ} → (dva dvb : depVec G n) → depVec G n
  _pt+DV_ {0} ⋆ ⋆ = ⋆
  _pt+DV_ {suc n} (a □ dva) (b □ dvb) = Gstr n ._+_ a b □ (dva pt+DV dvb)

  sumHIT+ : {n : ℕ} → (dva dvb : depVec G n) → sumHIT (dva pt+DV dvb) ≡ sumHIT dva +⊕HIT sumHIT dvb
  sumHIT+ {0} ⋆ ⋆ = sym (+⊕HIT-IdR _)
  sumHIT+ {suc n} (a □ dva) (b □ dvb) = cong₂ _+⊕HIT_ (sym (base-add _ _ _)) (sumHIT+ dva dvb)
                                        ∙ comm-4 (⊕HIT-AbGr ℕ G Gstr) _ _ _ _

-----------------------------------------------------------------------------
-- Case Traduction

  {- WARNING :
     The pseudo normal form is not unique.
     It is actually not unique enough so that it is not possible to raise one from ⊕HIT.
     Hence we actually need to make it a prop to be able to eliminate.
  -}

  untruncatedPNF : (x : ⊕HIT ℕ G Gstr) → Type ℓ
  untruncatedPNF x = Σ[ m ∈ ℕ ] Σ[ dv ∈ depVec G m ] x ≡ sumHIT dv

  PNF : (x : ⊕HIT ℕ G Gstr) → Type ℓ
  PNF x = ∥ untruncatedPNF x ∥₁

  untruncatedPNF2 : (x y : ⊕HIT ℕ G Gstr) → Type ℓ
  untruncatedPNF2 x y = Σ[ m ∈ ℕ ] Σ[ a ∈ depVec G m ] Σ[ b ∈ depVec G m ] (x ≡ sumHIT a) × (y ≡ sumHIT b)

  PNF2 :  (x y : ⊕HIT ℕ G Gstr) → Type ℓ
  PNF2 x y = ∥ untruncatedPNF2 x y ∥₁

-----------------------------------------------------------------------------
-- Translation

  ⊕HIT→PNF : (x : ⊕HIT ℕ G Gstr) → ∥ Σ[ m ∈ ℕ ] Σ[ a ∈ depVec G m ] x ≡ sumHIT a ∥₁
  ⊕HIT→PNF = DS-Ind-Prop.f _ _ _ _
        (λ _ → squash₁)
        ∣ (0 , (⋆ , refl)) ∣₁
        base→PNF
        add→PNF
    where
    base→PNF : (n : ℕ) → (a : G n) → PNF (base n a)
    base→PNF n a = ∣ (suc n) , ((a □ replicate0g n) , sym (cong (λ X → base n a +⊕HIT X) (sumHIT0g n)
                    ∙ +⊕HIT-IdR _)) ∣₁

    add→PNF : {U V : ⊕HIT ℕ G Gstr} → (ind-U : PNF U) → (ind-V : PNF V) → PNF (U +⊕HIT V)
    add→PNF {U} {V} = elim2 (λ _ _ → squash₁)
                      (λ { (k , dva , p) →
                      λ { (l , dvb , q) →
                      ∣ ((k +n l)
                        , (((extendDVR k l dva) pt+DV (extendDVL k l dvb))
                        , cong₂ _+⊕HIT_ p q
                          ∙ cong₂ _+⊕HIT_ (sym (extendDVReq k l dva)) (sym (extendDVLeq k l dvb))
                          ∙ sym (sumHIT+ (extendDVR k l dva) (extendDVL k l dvb)) )) ∣₁}})

  ⊕HIT→PNF2 : (x y : ⊕HIT ℕ G Gstr) → ∥ Σ[ m ∈ ℕ ] Σ[ a ∈ depVec G m ] Σ[ b ∈ depVec G m ] (x ≡ sumHIT a) × (y ≡ sumHIT b) ∥₁
  ⊕HIT→PNF2 x y = helper (⊕HIT→PNF x) (⊕HIT→PNF y)
    where
    helper : PNF x → PNF y →
             ∥ Σ[ m ∈ ℕ ] Σ[ a ∈ depVec G m ] Σ[ b ∈ depVec G m ] (x ≡ sumHIT a) × (y ≡ sumHIT b) ∥₁
    helper = elim2 (λ _ _ → squash₁)
                   (λ { (k , dva , p) →
                   λ { (l , dvb , q) →
                       ∣   ((k +n l)
                         , ((extendDVR k l dva)
                         , (extendDVL k l dvb
                         , p ∙ sym (extendDVReq k l dva)
                         , q ∙ sym (extendDVLeq k l dvb)))) ∣₁}})

-----------------------------------------------------------------------------
-- Some idea

{-
   This file should be generalizable to a general decidable index by adding a second vector
-}

{-
   It maybe possible to give a normal for without need the prop truncation.
   The issue with the current one is that we rely on a underline data type depVec
   which forces us to give an explict length. That's what forces the ∥_∥₁.
   Hence by getting rid of it and be rewrittinf the term it might be possible
   to get a normal form without the PT.

   Indeed this basically about pemuting and summing them by G n
   ∑ base (σ i) a (σ i) -> ∑[i ∈ ℕ] ∑[j ∈ I] base i (b i j) -> ∑ base i (c i)
   where a b c are informal "sequences"

   Then prove that if we extract the integer, we get an inceasing list
   with no coefficient being present twice.
-}

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

{- This module defines our notion of connectedness not requiring HITs.
   We define the generic n-connected version of a type, show that it is
   n-connected, and that it behaves like the original type above level n.
   We conclude by shoing this notion coincides with the usual notion.
   of connectedness in the presence of HITs. -}
module Universe.Trunc.Connection where

open import lib.Basics
open import lib.NType2
open import lib.Equivalences2
open import lib.types.Unit
open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Paths
open import lib.types.TLevel

open import Universe.Utility.General
open import Universe.Utility.Pointed
open import Universe.Utility.TruncUniverse

open import Universe.Hierarchy

open import Universe.Trunc.Universal
open import Universe.Trunc.Basics
open import Universe.Trunc.TypeConstructors

open trunc-ty
open trunc-props

-- *** Definition 6.13 ***
{- Our plain MLTT connectedness predicate.
   Because of predicativity issues, it has to live in one universe higher
   than its argument type C. Internally, we really want to quantify over
   truncation operators not only at the level of C, but also at levels below C.
   This would be the same in a theory with cumulative universes, but we are
   working in Agda. Since we are only going to actually use the truncation
   operator at one level lower than C, we restrict ourselves to this specific
   assumption in this particular development for no particular reason other
   than brevity of presentation. The reason for this difference of one level
   will become apparent in the definition of 'connection'. -}
module _ {i} (n : ℕ₋₂) (C : Type (lsucc i)) where
  is-connected⋆ : Type (lsucc (lsucc i))
  is-connected⋆ = (Tr : (X : Type i) → trunc-ty n X (lsucc i))
                  (TrC : trunc-ty n C (lsucc i))
                → is-contr ⟦ type TrC ⟧

{- The (n+1)-connected version, or n-connection of some pointed type A.
   Since we internally quantify over the type of truncations of a path space
   from a before being able to require an element in the truncation,
   predicativity issues force 'connection' to live in a universe one level
   higher than A.

   Take particular care in noting that the parameter n is in fact one-off,
   for example, The type 'connection (-2)' denotes the (-1)-connection. -}
module _ {i} (A : Type• i) where
  module con (n : ℕ₋₂) where
    -- *** Definition 6.11 ***
    connection• : Type• (lsucc i)
    connection• =
      Σ• (A
        , ((λ b → (TrP : trunc-ty n (pt A == b) i) → ⟦ type TrP ⟧)
         , (λ TrP → cons TrP idp)))

    {- The base type of the (n+1)-connection:
      Σ A (λ b → (TrP : trunc-ty n (a == b) i) → ⟦ type TrP ⟧. -}
    connection : Type (lsucc i)
    connection = base connection•

    -- *** Lemma 6.14 ***
    connection-is-connected : is-connected⋆ (S n) connection
    connection-is-connected Tr TrC = equiv-preserves-level (e ⁻¹) h where

      -- The supplied generic truncation operator is used only to truncate A.
      TrA : trunc-ty (S n) (base A) (lsucc i)
      TrA = Tr (base A)

      TrP : (b : base A) → trunc-ty n (pt A == b) i
      TrP = trunc-path.trunc {j = i} TrA (pt A)

      {- This definition typechecks since
              Σ A (λ b → ⟦ type (TrP b) ⟧
           ≡  Σ A (λ a → cons TrA (pt A) == cons TrA b)
         by construction of trunc-path.trunc. -}
      TrD : trunc-ty (S n) (Σ (base A) (λ b → ⟦ type (TrP b) ⟧)) (lsucc i)
      TrD = trunc-Σ.trunc {j = lsucc i} TrA
              (λ b → trunc-self.trunc (Path-≤ (type TrA) (cons TrA (pt A)) b))

      u : connection ≃ Σ (base A) (λ b → ⟦ type (TrP b) ⟧)
      u = equiv-Σ-snd {B = λ _ → Π _ _}  -- No idea why Agda wants this.
                      (λ b → Π₁-contr (trunc-inhab-contr {j = i} (TrP b)))

      e : ⟦ type TrC ⟧ ≃ ⟦ type TrD ⟧
      e = trunc-functor.fmap-equiv {j = lsucc i} TrC TrD u

      {- Note that
           ⟦ type TrD ⟧  ≡  Σ ⟦ type TrA ⟧ (λ tb → cons TrA (pt A) == tb)
         by construction of trunc-Σ.trunc. -}
      h : is-contr ⟦ type TrD ⟧
      h = pathfrom-is-contr (cons TrA (pt A))

  module con2 (n : ℕ) where
    open con (n -2)

    -- *** Lemma 6.12 ***
    -- The (n+1)-connection of A coincides with A on dimension n+2 and above.
    connection-higher-dim : (Ω ^ n) connection• ≃• (Ω ^ n) A
    connection-higher-dim =
      forget-Ω^-Σ•₂ _ n (λ _ → Π-level (λ Tr → snd (type Tr)))

  open con public
  open con2 public

-- For the first time in the dependency chain, we assume HITs.
module with-hits where
  open import lib.types.Truncation
  open import lib.NConnected

  {- With the truncations of the HoTT community's library,
     our truncation types are always inhabited, and hence contractible. -}
  module _ {i j} where
    trunc : (n : ℕ₋₂) (A : Type i) → trunc-ty n A (i ⊔ j)
    trunc n A = record
      { type = (Trunc n A , Trunc-level)
      ; cons = [_]
      ; univ = λ U → is-eq
        (λ f → f ∘ [_]) (Trunc-rec (snd U)) (λ f → idp)
        (λ f → λ= (Trunc-elim (λ _ → =-preserves-level _ (snd U))
                              (λ a → idp)))}

    trunc-contr : {n : ℕ₋₂} {A : Type i} → is-contr (trunc-ty n A (i ⊔ j))
    trunc-contr = trunc-inhab-contr {j = j} (trunc _ _)

  -- *** Lemma 6.15 ***
  -- Our connectedness⋆ is equivalent to HIT connectedness.
  module _ {i} {n : ℕ₋₂} {A : Type (lsucc i)} where
    conn⋆-conn : is-connected⋆ n A ≃ is-connected n A
    conn⋆-conn = Π₁-contr (trunc-contr {j = lsucc i})
              ∘e Π₁-contr (Π-level (λ _ → trunc-contr {j = lsucc i}))

-- *** Theorem 7.1 ***
module _ (n : ℕ) where
  M• : Type• ｢ n + 2 ｣
  M• = connection• (_ , Loop n) (n -1)

  assertion-0 : has-level ⟨ n + 1 ⟩ (base M•)
  assertion-0 = snd (Σ-≤ (⟨ n ⟩ -Type-≤ ｢ n ｣)
                    (λ b → Π-≤ (trunc-ty _ (_ == b) _)
                               (λ tr → raise (raise (type tr)))))

  assertion-1 : ¬ (has-level ⟨ n ⟩ (base M•))
  assertion-1 =
      main' n
    ∘ –> (equiv-is-contr• (connection-higher-dim _ (n + 1)))
    ∘ (λ z → z (pt M•))
    ∘ –> has-level-equiv-contr-loops

  assertion-2 : is-connected⋆ ⟨ n ⟩ (base M•)
  assertion-2 = connection-is-connected _ _

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat

{-# BUILTIN REWRITE _≡_ #-}

not : Bool → Bool
not true = false
not false = true

postulate rew : Nat ≡ Bool
{-# REWRITE rew #-}

0' : Bool
0' = 0

test : not 0' ≡ true
test = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.SimpleMap where

open import Class.Equality
open import Class.Map
open import Data.Bool
open import Data.Maybe
open import Data.List hiding (lookup)
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Negation

SimpleMap : Set -> Set -> Set
SimpleMap A B = List (A × B)

private

  simpleRemove : ∀ {A B} {{_ : EqB A}} -> A -> SimpleMap A B -> SimpleMap A B
  simpleRemove k m = boolFilter (λ {(k' , _) → not (k ≣ k')}) m

  simpleInsert : ∀ {A B} {{_ : EqB A}} -> A -> B -> SimpleMap A B -> SimpleMap A B
  simpleInsert k v m = (k , v) ∷ (simpleRemove k m)

  simpleLookup : ∀ {A B} {{_ : EqB A}} -> A -> SimpleMap A B -> Maybe B
  simpleLookup k [] = nothing
  simpleLookup k ((fst , snd) ∷ m) with k ≣ fst
  simpleLookup k ((fst , snd) ∷ m) | true = just snd
  simpleLookup k ((fst , snd) ∷ m) | false = simpleLookup k m

  simpleMapSnd : ∀ {A B C} -> (B -> C) -> SimpleMap A B -> SimpleMap A C
  simpleMapSnd f [] = []
  simpleMapSnd f ((fst , snd) ∷ m) = (fst , f snd) ∷ (simpleMapSnd f m)

instance
  MapClass-Simple : {K : Set} {{_ : EqB K}} -> MapClass K (SimpleMap K)
  MapClass-Simple = record
    { insert = simpleInsert
    ; remove = simpleRemove
    ; lookup = simpleLookup
    ; mapSnd = simpleMapSnd
    ; emptyMap = [] }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

-- Bundled version of a Cocartesian Category
module Categories.Category.Cocartesian.Bundle where

open import Level

open import Categories.Category.Core using (Category)
open import Categories.Category.Cocartesian using (Cocartesian)

record CocartesianCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U           : Category o ℓ e  -- U for underlying
    cocartesian : Cocartesian U

  open Category U public
  open Cocartesian cocartesian public

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
{-# OPTIONS --allow-unsolved-metas #-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Abstract.Types

-- For each desired property (VotesOnce and LockedRoundRule), we have a
-- module containing a Type that defines a property that an implementation
-- should prove, and a proof that it implies the corresponding rule used by
-- the abstract proofs.  Then, we use those proofs to instantiate thmS5,
-- and the use thmS5 to prove a number of correctness conditions.
--
-- TODO-1: refactor this file to separate the definitions and proofs of
-- VotesOnce and LockedRoundRule from their use in proving the correctness
-- properties.

module LibraBFT.Abstract.Properties
  (𝓔 : EpochConfig)
  (UID    : Set)
  (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁))
  (𝓥      : VoteEvidence 𝓔 UID)
  where

 open import LibraBFT.Abstract.Records 𝓔 UID _≟UID_ 𝓥
 open import LibraBFT.Abstract.Records.Extends 𝓔 UID _≟UID_ 𝓥
 open import LibraBFT.Abstract.RecordChain 𝓔 UID _≟UID_ 𝓥
 import LibraBFT.Abstract.RecordChain.Assumptions 𝓔 UID _≟UID_ 𝓥
   as StaticAssumptions
 open import LibraBFT.Abstract.System 𝓔 UID _≟UID_ 𝓥

 open EpochConfig 𝓔

 open import LibraBFT.Abstract.Obligations.VotesOnce 𝓔 UID _≟UID_ 𝓥 as VO
 open import LibraBFT.Abstract.Obligations.LockedRound 𝓔 UID _≟UID_ 𝓥 as LR

 --------------------------------------------------------------------------------------------
 -- * A /ValidSysState/ is one in which both peer obligations are obeyed by honest peers * --
 --------------------------------------------------------------------------------------------

 record ValidSysState {ℓ}(𝓢 : AbsSystemState ℓ) : Set (ℓ+1 ℓ0 ℓ⊔ ℓ) where
   field
     vss-votes-once   : VO.Type 𝓢
     vss-locked-round : LR.Type 𝓢
 open ValidSysState public

 -- And a valid system state offers the desired /CommitsDoNotConflict/ property
 -- and variants.
 module _ {ℓ}(𝓢 : AbsSystemState ℓ) (st-valid : ValidSysState 𝓢) where
   open AbsSystemState 𝓢
   open All-InSys-props InSys
   import LibraBFT.Abstract.RecordChain.Properties 𝓔 UID _≟UID_ 𝓥 as Props

   CommitsDoNotConflict : ∀{q q'}
        → {rc  : RecordChain (Q q)}  → All-InSys rc
        → {rc' : RecordChain (Q q')} → All-InSys rc'
        → {b b' : Block}
        → CommitRule rc  b
        → CommitRule rc' b'
        → NonInjective-≡ bId ⊎ ((B b) ∈RC rc' ⊎ (B b') ∈RC rc)
   CommitsDoNotConflict = Props.WithInvariants.thmS5 InSys
     (VO.proof 𝓢 (vss-votes-once st-valid))
     (LR.proof 𝓢 (vss-locked-round st-valid))

   -- When we are dealing with a /Complete/ AbsSystem, we can go a few steps
   -- further and prove that commits do not conflict even if we have only partial
   -- knowledge about Records represented in the system.
   module _ (∈QC⇒AllSent : Complete 𝓢) where

    -- For a /complete/ system we can go even further; if we have evidence that
    -- only the tip of the record chains is in the system, we can infer
    -- the rest of it is also in the system (or blockIDs are not injective).
    CommitsDoNotConflict'
      : ∀{q q'}{rc  : RecordChain (Q q)}{rc' : RecordChain (Q q')}{b b' : Block}
      → InSys (Q q) → InSys (Q q')
      → CommitRule rc  b
      → CommitRule rc' b'
      → NonInjective-≡ bId ⊎ ((B b) ∈RC rc' ⊎ (B b') ∈RC rc)
    CommitsDoNotConflict' {q} {q'} {step {r = B bb} rc b←q} {step {r = B bb'} rc' b←q'} {b} {b'} q∈sys q'∈sys cr cr'
       with bft-assumption (qVotes-C2 q) (qVotes-C2 q')
    ...| α , α∈qmem , α∈q'mem , hα
       with Any-sym (Any-map⁻ α∈qmem) | Any-sym (Any-map⁻ α∈q'mem)
    ...| α∈q | α∈q'
       with ∈QC⇒AllSent {q = q} hα α∈q q∈sys | ∈QC⇒AllSent {q = q'} hα α∈q' q'∈sys
    ...| ab , ab←q , arc , ais | ab' , ab←q' , arc' , ais'
       with RecordChain-irrelevant (step arc  ab←q)  (step rc  b←q) |
            RecordChain-irrelevant (step arc' ab←q') (step rc' b←q')
    ...| inj₁ hb     | _       = inj₁ hb
    ...| inj₂ _      | inj₁ hb = inj₁ hb
    ...| inj₂ arc≈rc | inj₂ arc'≈rc'
       with CommitsDoNotConflict
                 (All-InSys-step ais  ab←q  q∈sys )
                 (All-InSys-step ais' ab←q' q'∈sys)
                 (transp-CR (≈RC-sym arc≈rc  ) cr )
                 (transp-CR (≈RC-sym arc'≈rc') cr')
    ...| inj₁ hb = inj₁ hb
    ...| inj₂ (inj₁ b∈arc') = inj₂ (inj₁ (transp-B∈RC arc'≈rc' b∈arc'))
    ...| inj₂ (inj₂ b'∈arc) = inj₂ (inj₂ (transp-B∈RC arc≈rc   b'∈arc))

    -- The final property is even stronger; it states that even if an observer
    -- has access only to suffixes of record chains that match the commit rule,
    -- we can still guarantee that b and b' are non-conflicting blocks.  This
    -- will be important for showing that observers can have confidence in commit
    -- messages without participating in the protocol and without having access to
    -- all previously sent records.
    CommitsDoNotConflict''
      : ∀{o o' q q'}
      → {rcf  : RecordChainFrom o  (Q q)}
      → {rcf' : RecordChainFrom o' (Q q')}
      → {b b' : Block}
      → InSys (Q q)
      → InSys (Q q')
      → CommitRuleFrom rcf  b
      → CommitRuleFrom rcf' b'
      → NonInjective-≡ bId ⊎ Σ (RecordChain (Q q')) ((B b)  ∈RC_)
                           ⊎ Σ (RecordChain (Q q))  ((B b') ∈RC_)
    CommitsDoNotConflict'' {cb} {q = q} {q'} {rcf} {rcf'} q∈sys q'∈sys crf crf'
       with bft-assumption (qVotes-C2 q) (qVotes-C2 q')
    ...| α , α∈qmem , α∈q'mem , hα
       with Any-sym (Any-map⁻ α∈qmem) | Any-sym (Any-map⁻ α∈q'mem)
    ...| α∈q | α∈q'
       with ∈QC⇒AllSent {q = q} hα α∈q q∈sys | ∈QC⇒AllSent {q = q'} hα α∈q' q'∈sys
    ...| ab , ab←q , arc , ais | ab' , ab←q' , arc' , ais'
       with step arc  ab←q | step arc' ab←q'
    ...| rcq | rcq'
       with crf⇒cr rcf  rcq  crf | crf⇒cr rcf' rcq' crf'
    ...| inj₁ hb | _       = inj₁ hb
    ...| inj₂ _  | inj₁ hb = inj₁ hb
    ...| inj₂ cr | inj₂ cr'
       with CommitsDoNotConflict' q∈sys q'∈sys cr cr'
    ...| inj₁ hb = inj₁ hb
    ...| inj₂ (inj₁ b∈arc') = inj₂ (inj₁ (rcq' , b∈arc'))
    ...| inj₂ (inj₂ b'∈arc) = inj₂ (inj₂ (rcq  , b'∈arc))


text:
interleaved mutual

  data Foo : Set → Set
  data Foo_Bar : Set

  constructor
    foobar : Foo Bar

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --rewriting #-}
module MessageClosureProperties where

open import Data.Nat using (ℕ; zero ; suc)
open import Data.Fin using (Fin; zero; suc)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; cong; cong₂; sym; refl)

open import Auxiliary.Extensionality
open import Auxiliary.RewriteLemmas

import Types.COI as COI
import Types.IND1 as IND
import Types.Tail1 as Tail
import DualTail1 as DT
import MessageClosure as MC

open COI using (_≈_; _≈'_; _≈ᵗ_)
open DT using (Stack; ε; ⟪_,_⟫)

private
  variable
    n : ℕ
    σ σ′ : Stack n
    G : IND.GType n

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

var=shift-var : (i : Fin (suc n)) → IND.var i ≡ MC.shift{m = n}{n = 0} IND.var i
var=shift-var zero = refl
var=shift-var (suc i) = refl

apply-id-S : (S : IND.SType n) → MC.applyS{n = 0} IND.var S ≡ S
apply-id-G : (G : IND.GType n) → MC.applyG{n = 0} IND.var G ≡ G
apply-id-T : (T : IND.TType n) → MC.applyT{n = 0} IND.var T ≡ T

apply-id-S (IND.gdd G) = cong IND.gdd (apply-id-G G)
apply-id-S{n} (IND.rec G) rewrite sym (ext (var=shift-var{n})) = cong IND.rec (apply-id-G G)
apply-id-S (IND.var x) = refl

apply-id-G (IND.transmit d T S) = cong₂ (IND.transmit d) (apply-id-T T) (apply-id-S S)
apply-id-G (IND.choice d m alt) = cong (IND.choice d m) (ext (apply-id-S ∘ alt))
apply-id-G IND.end = refl

apply-id-T IND.TUnit = refl
apply-id-T IND.TInt = refl
apply-id-T (IND.TPair T T₁) = cong₂ IND.TPair (apply-id-T T) (apply-id-T T₁)
apply-id-T (IND.TChan S) = cong IND.TChan (apply-id-S S)

mc-equiv-S : (s : IND.SType 0)
  → DT.ind2coiS ε s ≈ DT.tail2coiS ε (MC.mclosureS s)
mc-equiv-G : (g : IND.GType 0)
  → DT.ind2coiG ε g ≈' DT.tail2coiG ε (MC.mclosureG g)
mc-equiv-T : (t : IND.TType 0)
  → DT.ind2coiT ε t ≈ᵗ DT.tail2coiT (MC.injectT (MC.applyT IND.var t))

COI.Equiv.force (mc-equiv-S (IND.gdd g)) = mc-equiv-G g
COI.Equiv.force (mc-equiv-S (IND.rec G)) = {!!}
-- mc-equiv-G (IND.st-substG G zero (IND.rec G))

mc-equiv-G (IND.transmit d t s) =
  COI.eq-transmit d (mc-equiv-T t) (mc-equiv-S s)
mc-equiv-G (IND.choice d m alt) =
  COI.eq-choice d (mc-equiv-S ∘ alt)
mc-equiv-G IND.end =
  COI.eq-end

mc-equiv-T IND.TUnit = COI.eq-unit
mc-equiv-T IND.TInt = COI.eq-int
mc-equiv-T (IND.TPair t t₁) = COI.eq-pair (mc-equiv-T t) (mc-equiv-T t₁)
mc-equiv-T (IND.TChan S) rewrite apply-id-S S = COI.eq-chan COI.≈-refl

-- relation between two stacks (to fill above hole in mc-equiv-S)

data Related : DT.Stack {IND.GType} n → Stack {Tail.GType} n → Set where
  base : Related {0} ε ε
  step : Related {n} σ σ′
       → Related {suc n} ⟪ σ , G ⟫ ⟪ σ′ , MC.mcloG (MC.ext {!!} (IND.rec G)) G ⟫

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


text:
module Logic.Structure.Monoid where

import Logic.Equivalence
import Logic.Operations as Operations

open Logic.Equivalence using (Equivalence; module Equivalence)
open Operations.Param

data Monoid (A : Set)(Eq : Equivalence A) : Set where
  monoid :
    (z   : A)
    (_+_ : A -> A -> A)
    (leftId : LeftIdentity Eq z _+_)
    (rightId : RightIdentity Eq z _+_)
    (assoc : Associative Eq _+_) ->
    Monoid A Eq

-- There should be a simpler way of doing this. Local definitions to data declarations?

module Projections where

  zero : {A : Set}{Eq : Equivalence A} -> Monoid A Eq -> A
  zero (monoid z _ _ _ _) = z

  plus : {A : Set}{Eq : Equivalence A} -> Monoid A Eq -> A -> A -> A
  plus (monoid _ p _ _ _) = p

  leftId : {A : Set}{Eq : Equivalence A}(Mon : Monoid A Eq) -> LeftIdentity Eq (zero Mon) (plus Mon)
  leftId (monoid _ _ li _ _) = li

  rightId : {A : Set}{Eq : Equivalence A}(Mon : Monoid A Eq) -> RightIdentity Eq (zero Mon) (plus Mon)
  rightId (monoid _ _ _ ri _) = ri

  assoc : {A : Set}{Eq : Equivalence A}(Mon : Monoid A Eq) -> Associative Eq (plus Mon)
  assoc (monoid _ _ _ _ a) = a

module Monoid {A : Set}{Eq : Equivalence A}(Mon : Monoid A Eq) where

  zero    = Projections.zero Mon
  _+_     = Projections.plus Mon
  leftId  = Projections.leftId Mon
  rightId = Projections.rightId Mon
  assoc   = Projections.assoc Mon


text:
open import Relation.Binary.Core

module InsertSort.Impl2.Correctness.Permutation.Alternative {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List
open import Data.Sum
open import Function
open import InsertSort.Impl2 _≤_ tot≤
open import List.Permutation.Alternative A renaming (_∼_ to _∼′_)
open import List.Permutation.Alternative.Correctness A
open import List.Permutation.Base A
open import OList _≤_

lemma-insert∼′ : {b : Bound}{x : A}(b≤x : LeB b (val x))(xs : OList b) → (x ∷ forget xs) ∼′ forget (insert b≤x xs)
lemma-insert∼′ b≤x onil = ∼refl
lemma-insert∼′ {x = x} b≤x (:< {x = y} b≤y ys)
    with tot≤ x y
... | inj₁ x≤y = ∼refl
... | inj₂ y≤x = ∼trans (∼swap ∼refl) (∼head y (lemma-insert∼′ (lexy y≤x) ys))

lemma-insertSort∼′ : (xs : List A) → xs ∼′ forget (insertSort xs)
lemma-insertSort∼′ [] = ∼refl
lemma-insertSort∼′ (x ∷ xs) = ∼trans (∼head x (lemma-insertSort∼′ xs)) (lemma-insert∼′ lebx (insertSort xs))

theorem-insertSort∼ : (xs : List A) → xs ∼ forget (insertSort xs)
theorem-insertSort∼ = lemma-∼′-∼ ∘ lemma-insertSort∼′

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Currently open declarations are not allowed in mutual blocks.
-- This might change.
module OpenInMutual where

module A where

mutual
  open A
  T : Set -> Set
  T A = A

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

module TemporalOps.Linear where

open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import CategoryTheory.CartesianStrength
open import CategoryTheory.NatTrans
open import CategoryTheory.Monad
open import CategoryTheory.Linear

open import TemporalOps.Next
open import TemporalOps.Delay
open import TemporalOps.Diamond
open import TemporalOps.OtherOps
open import TemporalOps.Common.Other
open import TemporalOps.Common.Compare
open import TemporalOps.Common.Rewriting

open import Data.Product
open import Data.Product.Properties
open import Data.Sum
open import Data.Nat hiding (_*_)
open import Data.Nat.Properties
            using (+-identityʳ ; +-comm ; +-suc ; +-assoc)

open import Relation.Binary.PropositionalEquality hiding (inspect)

open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

open ≡-Reasoning

open L ℝeactive-BCCC M-◇ public

ℝeactive-linear : Linear ℝeactive-BCCC M-◇
ℝeactive-linear = record
    { linprod = λ A B →
    record { ⟪_,_⟫ = prod-◇
           ; *π₁-comm = λ {C} {l₁} {l₂} {n} {a} →
                        *π₁-comm-◇ {A}{B}{C} {l₁} {l₂} {n} {a}
           ; *π₂-comm = {!   !}
           ; ⊛-unique = {!   !}
           }
    }
    where
    open Functor F-▹
    open Functor F-◇ renaming (fmap to ◇-f)
    private module ▹ᵏ-F k = Functor (F-delay k)
    private module ▹ᵏ-◇ k = _⟹_ (▹ᵏ-to-◇ k)
    private module ▹ᵏ-C k = CartesianFunctor (F-cart-delay k)
    open Monad M-◇
    open CartesianFunctor F-cart-▹ renaming (m to m-▹)

    pair-delay-◇₁ : ∀{A B : τ} -> (k l : ℕ) -> (delay A by suc (k + l) ⊗ delay B by k)
                                   ⇴ delay (◇ A ⊗ B) by k
    pair-delay-◇₁ zero l n (dA , dB) = (suc l , dA) , dB
    pair-delay-◇₁ {A}{B} (suc k) l n p = fmap (pair-delay-◇₁ k l) n
        (m-▹ (delay A by suc (k + l)) (delay B by k) n p)

    pair-delay-◇₂ : ∀{A B : τ} -> (k l : ℕ) -> (delay A by k ⊗ delay B by suc (k + l))
                                   ⇴ delay (A ⊗ ◇ B) by k
    pair-delay-◇₂ zero l n (dA , dB) = dA , (suc l , dB)
    pair-delay-◇₂ {A}{B} (suc k) l n p = fmap (pair-delay-◇₂ k l) n
        (m-▹ (delay A by k) (delay B by suc (k + l)) n p)

    prod-◇-compare : ∀{A B : τ} -> (k₁ k₂ n : ℕ)
                  -> (a₁ : delay A by k₁ at n)(a₂ : delay B by k₂ at n)
                  -> Ordering k₁ k₂ -> ◇ (A ⊛ B) at n
    prod-◇-compare {A} {B} k₁ .(suc (k₁ + l)) n a₁ a₂ (less .k₁ l) =
        k₁ , ▹ᵏ-F.fmap k₁ ι₁ n (▹ᵏ-F.fmap k₁ ι₁ n (pair-delay-◇₂ k₁ l n (a₁ , a₂)))
    prod-◇-compare {A} {B} .(suc (k₂ + l)) k₂ n a₁ a₂ (greater .k₂ l) =
        k₂ , ▹ᵏ-F.fmap k₂ ι₁ n (▹ᵏ-F.fmap k₂ ι₂ n (pair-delay-◇₁ k₂ l n (a₁ , a₂)))
    prod-◇-compare {A} {B} k₁ .k₁ n a₁ a₂ (equal .k₁) =
        k₁ , ▹ᵏ-F.fmap k₁ ι₂ n (▹ᵏ-C.m k₁ A B n (a₁ , a₂))

    ◇-select : ∀{A B : τ} -> (◇ A ⊗ ◇ B) ⇴ ◇ (A ⊛ B)
    ◇-select {A}{B} n ((k₁ , a₁) , (k₂ , a₂)) =
        prod-◇-compare {A}{B} k₁ k₂ n a₁ a₂ (compare k₁ k₂)

    prod-◇ : ∀{A B L : τ} -> (L ⇴ ◇ A) -> (L ⇴ ◇ B) -> (L ⇴ ◇ (A ⊛ B))
    prod-◇ fa fb n lp = ◇-select n (fa n lp , fb n lp)

    *π₁-comm-◇ : ∀{A B L} -> {l₁ : L ⇴ ◇ A} {l₂ : L ⇴ ◇ B}
           -> (μ.at A ∘ ◇-f *π₁) ∘ (prod-◇ l₁ l₂) ≈ l₁
    *π₁-comm-◇ {A}{B}{L}{l₁}{l₂} {n} {a} with inspect (l₁ n a , l₂ n a)
    *π₁-comm-◇ | ((k₁ , a₁) , (k₂ , a₂)) with≡ pf with inspect (compare k₁ k₂)
    *π₁-comm-◇ {A}{B}{L}{l₁}{l₂}{n}{a} | ((k₁ , a₁) , .(suc (k₁ + l)) , a₂) with≡ pf
                                           | less .k₁ l with≡ cpf =
        begin
            (μ.at A n (◇-f *π₁ n (◇-select n ⌞ (l₁ n a , l₂ n a) ⌟)))
        ≡⟨ cong! pf ⟩
            μ.at A n (◇-f *π₁ n
                (prod-◇-compare k₁ (suc (k₁ + l)) n a₁ a₂ (⌞ compare k₁ (suc (k₁ + l)) ⌟)))
        ≡⟨ cong! cpf ⟩
            μ.at A n (◇-f *π₁ n
                (prod-◇-compare k₁ (suc (k₁ + l)) n a₁ a₂ (less k₁ l)))
        ≡⟨⟩
            μ.at A n (k₁ ,
                ▹ᵏ-F.fmap k₁ *π₁ n ⌞ (▹ᵏ-F.fmap k₁ ι₁ n (▹ᵏ-F.fmap k₁ ι₁ n
                    (pair-delay-◇₂ k₁ l n (a₁ , a₂)))) ⌟)
        ≡⟨ cong! (▹ᵏ-F.fmap-∘ k₁ {g = ι₁ {A ⊗ ◇ B ⊕ ◇ A ⊗ B} {A ⊗ B}}
                                    {ι₁ {A ⊗ ◇ B} {◇ A ⊗ B}}{n} {pair-delay-◇₂ k₁ l n (a₁ , a₂)}) ⟩
            μ.at A n (k₁ ,
                ⌞ ▹ᵏ-F.fmap k₁ *π₁ n (▹ᵏ-F.fmap k₁ (ι₁ ∘ ι₁) n
                    (pair-delay-◇₂ k₁ l n (a₁ , a₂))) ⌟)
        ≡⟨ cong! (▹ᵏ-F.fmap-∘ k₁ {g = *π₁} {ι₁ ∘ ι₁} {n} {pair-delay-◇₂ k₁ l n (a₁ , a₂)}) ⟩
            μ.at A n (k₁ ,
                ▹ᵏ-F.fmap k₁ ([ η.at A ∘ π₁ ⁏ π₁ {B = L} ⁏ η.at A ∘ π₁ {B = L} ] ∘ ι₁ ∘ ι₁) n
                    (pair-delay-◇₂ k₁ l n (a₁ , a₂)))
        ≡⟨⟩
            μ.at A n (k₁ ,
                ⌞ ▹ᵏ-F.fmap k₁ (η.at A ∘ π₁) n
                    (pair-delay-◇₂ k₁ l n (a₁ , a₂)) ⌟)
        ≡⟨ cong! (▹ᵏ-F.fmap-∘ k₁) ⟩
            μ.at A n (k₁ , ▹ᵏ-F.fmap k₁ (η.at A) n
                ⌞ ▹ᵏ-F.fmap k₁ π₁ n (pair-delay-◇₂ k₁ l n (a₁ , a₂)) ⌟)
        ≡⟨ cong! (lemma k₁ l {n} {a₁ , a₂}) ⟩
            μ.at A n (k₁ , ▹ᵏ-F.fmap k₁ (η.at A) n a₁)
        ≡⟨ η-unit2 ⟩
            k₁ , a₁
        ≡⟨ sym (,-injectiveˡ pf) ⟩
            l₁ n a
        ∎
        where
        lemma : ∀ (k l : ℕ) -> ▹ᵏ-F.fmap k π₁ ∘ pair-delay-◇₂ k l ≈ π₁
        lemma zero l = refl
        lemma (suc k) l {zero} = refl
        lemma (suc k) l {suc n} = lemma k l {n}

    *π₁-comm-◇ {A}{B}{L}{l₁}{l₂}{n}{a} | ((.(suc (k₂ + l)) , a₁) , k₂ , a₂) with≡ pf
                                      | greater .k₂ l  with≡ cpf  =
        begin
            (μ.at A n (◇-f *π₁ n (◇-select n ⌞ (l₁ n a , l₂ n a) ⌟)))
        ≡⟨ cong! pf ⟩
            μ.at A n (◇-f *π₁ n
                (prod-◇-compare (suc (k₂ + l)) k₂ n a₁ a₂ (⌞ compare (suc (k₂ + l)) k₂ ⌟)))
        ≡⟨ cong! cpf ⟩
            μ.at A n (◇-f *π₁ n
                (prod-◇-compare (suc (k₂ + l)) k₂ n a₁ a₂ (greater k₂ l)))
        ≡⟨⟩
            μ.at A n (k₂ ,
                ▹ᵏ-F.fmap k₂ *π₁ n ⌞ (▹ᵏ-F.fmap k₂ ι₁ n (▹ᵏ-F.fmap k₂ ι₂ n
                    (pair-delay-◇₁ k₂ l n (a₁ , a₂)))) ⌟)
        ≡⟨ cong! (▹ᵏ-F.fmap-∘ k₂ {g = ι₁ {A ⊗ ◇ B ⊕ ◇ A ⊗ B} {A ⊗ B}}
                                    {ι₂ {A ⊗ ◇ B} {◇ A ⊗ B}}{n} {pair-delay-◇₁ k₂ l n (a₁ , a₂)}) ⟩
            μ.at A n (k₂ ,
                ⌞ ▹ᵏ-F.fmap k₂ *π₁ n (▹ᵏ-F.fmap k₂ (ι₁ ∘ ι₂) n
                    (pair-delay-◇₁ k₂ l n (a₁ , a₂))) ⌟)
        ≡⟨ cong! (▹ᵏ-F.fmap-∘ k₂ {g = *π₁} {ι₁ ∘ ι₂} {n} {pair-delay-◇₁ k₂ l n (a₁ , a₂)}) ⟩
            μ.at A n (k₂ ,
                ▹ᵏ-F.fmap k₂ ([ η.at A ∘ π₁ {B = L} ⁏ π₁ {B = B} ⁏ η.at A ∘ π₁ {B = L} ] ∘ ι₁ ∘ ι₂) n
                    (pair-delay-◇₁ k₂ l n (a₁ , a₂)))
        ≡⟨⟩
            μ.at A n (k₂ , ⌞ ▹ᵏ-F.fmap k₂ π₁ n (pair-delay-◇₁ k₂ l n (a₁ , a₂)) ⌟)
        ≡⟨ refl ⟩
            μ.at A n (◇-f π₁ n (k₂ , pair-delay-◇₁ k₂ l n (a₁ , a₂)))
        ≡⟨ {!   !} ⟩
        -- ≡⟨ cong! (lemma k₂ l {n} {a₁ , a₂}) ⟩
        --     μ.at A n (k₂ , ▹ᵏ-F.fmap k₂ (▹ᵏ-◇.at (suc l) A) n (split-▹ᵏ k₂ l n a₁))
            suc (k₂ + l) , a₁
        ≡⟨ sym (,-injectiveˡ pf) ⟩
            l₁ n a
        ∎
        where
        split-▹ᵏ : ∀ {A} k l -> delay A by suc (k + l) ⇴ delay (delay A by suc l) by k
        split-▹ᵏ zero l n a = a
        split-▹ᵏ (suc k) l zero a = top.tt
        split-▹ᵏ (suc k) l (suc n) a = split-▹ᵏ k l n a

        lemma : ∀ {A B} (k l  : ℕ)
             -> ▹ᵏ-F.fmap k (π₁ {B = B}) ∘ pair-delay-◇₁ {A} k l
              ≈ ▹ᵏ-F.fmap k (▹ᵏ-◇.at (suc l) A) ∘ split-▹ᵏ k l ∘ π₁
        lemma zero l {n} = refl
        lemma (suc k) l {zero} = refl
        lemma (suc k) l {suc n} = lemma k l

        lemma2 : ∀ {A B} k l n (a₁ : delay A by suc (k + l) at n)
                               (a₂ : delay B by k at n)
              -> μ.at A n (◇-f π₁ n (k , pair-delay-◇₁ k l n (a₁ , a₂)))
               ≡ (suc (k + l) , a₁)
        lemma2 zero l n a₁ a₂ = refl
        lemma2 (suc k) l zero a₁ a₂ = {!   !}
        lemma2 (suc k) l (suc n) a₁ a₂ = {!   !}

    *π₁-comm-◇ {l₁ = l₁} {l₂} {n} {a} | ((k₁ , a₁) , .k₁ , a₂) with≡ pf
                                      | equal .k₁  with≡ cpf = {!   !}

open Linear ℝeactive-linear public

-- Handle a linear product with three continuations
handle : ∀ {A B C D : τ}
          -> (A ⊗   B ⊗ ◇ C ⇴ ◇ D)
          -> (A ⊗ ◇ B ⊗   C ⇴ ◇ D)
          -> (A ⊗   B ⊗   C ⇴ ◇ D)
          -> A ⊗ (B ⊛ C)    ⇴ ◇ D
handle a b c = [ a ∘ assoc-left ⁏ b ∘ assoc-left ⁏ c ∘ assoc-left ] ∘ dist2

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
------------------------------------------------------------------------
-- Do the parser combinators form a Kleene algebra?
------------------------------------------------------------------------

module TotalParserCombinators.Laws.KleeneAlgebra where

open import Algebra
open import Data.List
open import Data.List.Properties
open import Data.Nat using (ℕ)
open import Data.Product using (_,_; proj₂)
open import Function using (_$_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
import Relation.Binary.PropositionalEquality as P
open import Relation.Nullary

open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
  hiding (_>>=_) renaming (return to return′; _⊛_ to _⊛′_)

------------------------------------------------------------------------
-- A variant of _≲_

infix 4 _≲′_

-- The AdditiveMonoid module shows that _∣_ can be viewed as the join
-- operation of a join-semilattice (if language equivalence is used).
-- This means that the following definition of order is natural.

_≲′_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
p₁ ≲′ p₂ = p₁ ∣ p₂ ≈ p₂

-- This order coincides with _≲_.

≲⇔≲′ : ∀ {Tok R xs₁ xs₂}
       (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) →
       p₁ ≲ p₂ ⇔ p₁ ≲′ p₂
≲⇔≲′ {xs₁ = xs₁} p₁ p₂ = equivalence
  (λ (p₁≲p₂ : p₁ ≲ p₂) {x s} → equivalence (helper p₁≲p₂) (∣-right xs₁))
  (λ (p₁≲′p₂ : p₁ ≲′ p₂) s∈p₁ → Equivalence.to p₁≲′p₂ ⟨$⟩ ∣-left s∈p₁)
  where
  helper : p₁ ≲ p₂ → p₁ ∣ p₂ ≲ p₂
  helper p₁≲p₂ (∣-left       s∈p₁) = p₁≲p₂ s∈p₁
  helper p₁≲p₂ (∣-right .xs₁ s∈p₂) = s∈p₂

------------------------------------------------------------------------
-- A limited notion of *-continuity

-- Least upper bounds.

record _LeastUpperBoundOf_
         {Tok R xs} {f : ℕ → List R}
         (lub : Parser Tok R xs)
         (p : (n : ℕ) → Parser Tok R (f n)) : Set₁ where
  field
    upper-bound : ∀ n → p n ≲ lub
    least       : ∀ {ys} {ub : Parser Tok R ys} →
                  (∀ n → p n ≲ ub) → lub ≲ ub

-- For argument parsers which are not nullable we can prove that the
-- Kleene star operator is *-continuous.

*-continuous :
  ∀ {Tok R₁ R₂ R₃ fs xs}
  (p₁ : Parser Tok (List R₁ → R₂ → R₃) fs)
  (p₂ : Parser Tok R₁ [])
  (p₃ : Parser Tok R₂ xs) →
  (p₁ ⊛ p₂ ⋆ ⊛ p₃) LeastUpperBoundOf (λ n → p₁ ⊛ p₂ ↑ n ⊛ p₃)
*-continuous {Tok} {R₁ = R₁} {R₃ = R₃} {fs} {xs} p₁ p₂ p₃ =
  record { upper-bound = upper-bound; least = least }
  where
  upper-bound : ∀ n → p₁ ⊛ p₂ ↑ n ⊛ p₃ ≲ p₁ ⊛ p₂ ⋆ ⊛ p₃
  upper-bound n (∈p₁ ⊛′ ∈p₂ⁿ ⊛′ ∈p₃) =
    [ ○ - ○ ] [ ○ - ○ ] ∈p₁ ⊛ Exactly.↑≲⋆ n ∈p₂ⁿ ⊛ ∈p₃

  least : ∀ {ys} {p : Parser Tok R₃ ys} →
          (∀ i → p₁ ⊛ p₂ ↑ i ⊛ p₃ ≲ p) → p₁ ⊛ p₂ ⋆ ⊛ p₃ ≲ p
  least ub (∈p₁ ⊛′ ∈p₂⋆ ⊛′ ∈p₃) with Exactly.⋆≲∃↑ ∈p₂⋆
  ... | (n , ∈p₂ⁿ) = ub n ([ ○ - ○ ] [ ○ - ○ ] ∈p₁ ⊛ ∈p₂ⁿ ⊛ ∈p₃)

------------------------------------------------------------------------
-- The parser combinators do not form a Kleene algebra

-- If we allow arbitrary argument parsers, then we cannot prove the
-- following (variant of a) Kleene algebra axiom.

not-Kleene-algebra :
  ∀ {Tok} →
  Tok →
  (f : ∀ {R xs} → Parser Tok R xs → List (List R)) →
  (_⋆′ : ∀ {R xs} (p : Parser Tok R xs) →
         Parser Tok (List R) (f p)) →
  ¬ (∀ {R xs} {p : Parser Tok R xs} →
     return [] ∣ (p >>= λ x → (p ⋆′) >>= λ xs → return (x ∷ xs))
       ≲ (p ⋆′))
not-Kleene-algebra {Tok} t f _⋆′ fold =
  KleeneStar.unrestricted-incomplete t f _⋆′ ⋆′-complete
  where
  ⋆′-complete : ∀ {xs ys s} {p : Parser Tok Tok ys} →
                xs ∈[ p ]⋆· s → xs ∈ p ⋆′ · s
  ⋆′-complete []         = fold (∣-left return′)
  ⋆′-complete (∈p ∷ ∈p⋆) =
    fold (∣-right [ [] ]
            ([ ○ - ○ ] ∈p >>=
                       fix ([ ○ - ○ ] ⋆′-complete ∈p⋆ >>= return′)))
    where
    fix = cast∈ P.refl P.refl $ ++-identityʳ _

-- This shows that the parser combinators do not form a Kleene
-- algebra (interpreted liberally) using _⊛_ for composition, return
-- for unit, etc. However, it should be straightforward to build a
-- recogniser library, based on the parser combinators, which does
-- satisfy the Kleene algebra axioms (see
-- TotalRecognisers.LeftRecursion.KleeneAlgebra).

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Issue282 where

module Works where

  record R : Set where
    constructor c

  foo = R.c

module Doesn't_work where

  private

    record R : Set where
      constructor c

  foo = R.c

-- Bug.agda:17,9-12
-- Not in scope:
--   R.c at Bug.agda:17,9-12
-- when scope checking R.c

module Doesn't_work_either where

  private

    data D : Set where
      c : D

  foo = D.c

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module AllStdLib where

-- Ensure that the entire standard library is compiled.
import README

open import Data.Unit.Polymorphic using (⊤)
open import Data.String
open import IO hiding (_>>_)
import IO.Primitive as Prim

import DivMod
import HelloWorld
import HelloWorldPrim
import ShowNat
import TrustMe
import Vec
import dimensions

infixr 1 _>>_
_>>_ : ∀ {A B : Set} → Prim.IO A → Prim.IO B → Prim.IO B
m >> m₁ = m Prim.>>= λ _ → m₁

main : Prim.IO ⊤
main = run (putStrLn "Hello World!") >>
       DivMod.main >>
       HelloWorld.main >>
       HelloWorldPrim.main >>
       ShowNat.main >>
       TrustMe.main >>
       Vec.main >>
       dimensions.main

max_stars_repo_name: jappeace/agda

max_issues_repo_name: jappeace/agda

max_forks_repo_name: jappeace/agda


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

open import Groups.Definition
open import Groups.Lemmas
open import Groups.Abelian.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Modules.Definition

module Modules.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+R_ _*_} {m n : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} {G : AbelianGroup G'} {_·_ : A → M → M} (mod : Module R G _·_) where

open Group G'
open Ring R
open Setoid T
open Equivalence eq
open Module mod

moduleTimesZero : {x : M} → (0R · x) ∼ 0G
moduleTimesZero {x} = equalsDoubleImpliesZero G' (symmetric x=2x)
  where
    x=2x : (0R · x) ∼ (0R · x) + (0R · x)
    x=2x = transitive (dotWellDefined (Equivalence.symmetric (Setoid.eq S) (Group.identLeft additiveGroup)) reflexive) dotDistributesRight

moduleTimes-1 : {x : M} → ((Group.inverse additiveGroup 1R) · x) ∼ inverse x
moduleTimes-1 {x} = transitive (transferToRight' G' j) (inverseWellDefined G' dotIdentity)
  where
    i : ((1R · x) + ((Group.inverse additiveGroup 1R) · x)) ∼ 0G
    i = transitive (symmetric (transitive (dotWellDefined (Equivalence.symmetric (Setoid.eq S) (Group.invRight additiveGroup {1R})) reflexive) dotDistributesRight)) (moduleTimesZero)
    j : (((Group.inverse additiveGroup 1R) · x) + (1R · x)) ∼ 0G
    j = transitive (AbelianGroup.commutative G) i


text:
module Extensions.Nat where

open import Prelude
open import Data.Nat.Base
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties

m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
m+1+n≡1+m+n zero    n = refl
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)

<-+ : ∀ {m n m' n'} → m ≤ m' → n ≤ n' → m + n ≤ m' + n'
<-+ {zero} {zero} z≤n z≤n = z≤n
<-+ {suc m} (s≤s m<m') x = s≤s (<-+ m<m' x)
<-+ {zero} {suc n} {zero} z≤n (s≤s n<n') = s≤s n<n'
<-+ {zero} {suc n} {suc m'} z≤n (s≤s n<n') = s≤s (<-+ {m' = m'} z≤n (≤-step n<n'))

<-unique : ∀ {i u} (p q : i < u) → p ≡ q
<-unique (s≤s z≤n) (s≤s z≤n) = refl
<-unique (s≤s (s≤s p)) (s≤s (s≤s q)) = sym (cong s≤s (<-unique (s≤s q) (s≤s p)))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between binary relations
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

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

open import Function
open import Relation.Binary
open import Relation.Binary.Morphism

module Relation.Binary.Morphism.RelMonomorphism
  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
  {_∼₁_ : Rel A ℓ₁} {_∼₂_ : Rel B ℓ₂}
  {⟦_⟧ : A → B} (isMonomorphism : IsRelMonomorphism _∼₁_ _∼₂_ ⟦_⟧)
  where

open import Data.Sum.Base as Sum
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable

open IsRelMonomorphism isMonomorphism

------------------------------------------------------------------------
-- Properties

refl : Reflexive _∼₂_ → Reflexive _∼₁_
refl refl = injective refl

sym : Symmetric _∼₂_ → Symmetric _∼₁_
sym sym x∼y = injective (sym (cong x∼y))

trans : Transitive _∼₂_ → Transitive _∼₁_
trans trans x∼y y∼z = injective (trans (cong x∼y) (cong y∼z))

total : Total _∼₂_ → Total _∼₁_
total total x y = Sum.map injective injective (total ⟦ x ⟧ ⟦ y ⟧)

asym : Asymmetric _∼₂_ → Asymmetric _∼₁_
asym asym x∼y y∼x = asym (cong x∼y) (cong y∼x)

dec : Decidable _∼₂_ → Decidable _∼₁_
dec _∼?_ x y = map′ injective cong (⟦ x ⟧ ∼? ⟦ y ⟧)

------------------------------------------------------------------------
-- Structures

isEquivalence : IsEquivalence _∼₂_ → IsEquivalence _∼₁_
isEquivalence isEq = record
  { refl  = refl  E.refl
  ; sym   = sym   E.sym
  ; trans = trans E.trans
  } where module E = IsEquivalence isEq

isDecEquivalence : IsDecEquivalence _∼₂_ → IsDecEquivalence _∼₁_
isDecEquivalence isDecEq = record
  { isEquivalence  = isEquivalence E.isEquivalence
  ; _≟_            = dec E._≟_
  } where module E = IsDecEquivalence isDecEq


text:
open import HoTT

module cohomology.Exactness where

module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (F : fst (X ⊙→ Y)) (G : fst (Y ⊙→ Z)) where

  private
    f = fst F
    g = fst G

  {- in image of F ⇒ in kernel of G -}
  is-exact-itok : Type (lmax k (lmax j i))
  is-exact-itok = (y : fst Y) → Trunc ⟨-1⟩ (Σ (fst X) (λ x → f x == y))
    → g y == snd Z

  {- in kernel of G ⇒ in image of F -}
  is-exact-ktoi : Type (lmax k (lmax j i))
  is-exact-ktoi = (y : fst Y) → g y == snd Z
    → Trunc ⟨-1⟩ (Σ (fst X) (λ x → f x == y))

  record is-exact : Type (lmax k (lmax j i)) where
    field
      itok : is-exact-itok
      ktoi : is-exact-ktoi

  open is-exact public

  {- an equivalent version of is-exact-ktoi if Z is a set -}
  itok-alt-in : has-level ⟨0⟩ (fst Z)
    → ((x : fst X) → g (f x) == snd Z) → is-exact-itok
  itok-alt-in pZ h y = Trunc-rec (pZ _ _)
    (λ {(x , p) → ap g (! p) ∙ h x})

  itok-alt-out : is-exact-itok → ((x : fst X) → g (f x) == snd Z)
  itok-alt-out h x = h (f x) [ x , idp ]

{- Convenient notation for exact sequences. At the moment this is only set
   up for exact sequences of groups. Do we care about the general case?    -}

infix 2 _⊣|
infixr 2 _⟨_⟩→_

data ExactDiag {i} : Group i → Group i → Type (lsucc i) where
  _⊣| : (G : Group i) → ExactDiag G G
  _⟨_⟩→_ : (G : Group i) {H K : Group i} (φ : G →ᴳ H)
             → ExactDiag H K → ExactDiag G K

data ExactSeq {i} : {G H : Group i} → ExactDiag G H → Type (lsucc i) where
  exact-seq-zero : {G : Group i} → ExactSeq (G ⊣|)
  exact-seq-one : {G H : Group i} {φ : G →ᴳ H} → ExactSeq (G ⟨ φ ⟩→ H ⊣|)
  exact-seq-two : {G H K J : Group i} {φ : G →ᴳ H} {ψ : H →ᴳ K}
    {diag : ExactDiag K J} → is-exact (GroupHom.⊙f φ) (GroupHom.⊙f ψ)
    → ExactSeq (H ⟨ ψ ⟩→ diag) → ExactSeq (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ diag)

private
  exact-get-type : ∀ {i} {G H : Group i} → ExactDiag G H → ℕ → Type i
  exact-get-type (G ⊣|) _ = Lift Unit
  exact-get-type (G ⟨ φ ⟩→ H ⊣|) _ = Lift Unit
  exact-get-type (G ⟨ φ ⟩→ (H ⟨ ψ ⟩→ s)) O =
    is-exact (GroupHom.⊙f φ) (GroupHom.⊙f ψ)
  exact-get-type (_ ⟨ _ ⟩→ s) (S n) = exact-get-type s n

exact-get : ∀ {i} {G H : Group i} {diag : ExactDiag G H}
  → ExactSeq diag → (n : ℕ) → exact-get-type diag n
exact-get exact-seq-zero _ = lift unit
exact-get exact-seq-one _ = lift unit
exact-get (exact-seq-two ex s) O = ex
exact-get (exact-seq-two ex s) (S n) = exact-get s n

private
  exact-build-arg-type : ∀ {i} {G H : Group i} → ExactDiag G H → List (Type i)
  exact-build-arg-type (G ⊣|) = nil
  exact-build-arg-type (G ⟨ φ ⟩→ H ⊣|) = nil
  exact-build-arg-type (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ s) =
    is-exact (GroupHom.⊙f φ) (GroupHom.⊙f ψ)
    :: exact-build-arg-type (H ⟨ ψ ⟩→ s)

  exact-build-helper : ∀ {i} {G H : Group i} (diag : ExactDiag G H)
    → HList (exact-build-arg-type diag) → ExactSeq diag
  exact-build-helper (G ⊣|) nil = exact-seq-zero
  exact-build-helper (G ⟨ φ ⟩→ H ⊣|) nil = exact-seq-one
  exact-build-helper (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ s) (ie :: ies) =
    exact-seq-two ie (exact-build-helper (H ⟨ ψ ⟩→ s) ies)

exact-build : ∀ {i} {G H : Group i} (diag : ExactDiag G H)
  → hlist-curry-type (exact-build-arg-type diag) (λ _ → ExactSeq diag)
exact-build diag = hlist-curry (exact-build-helper diag)

private
  exact-snoc-diag : ∀ {i} {G H K : Group i}
    → ExactDiag G H → (H →ᴳ K) → ExactDiag G K
  exact-snoc-diag (G ⊣|) ψ = G ⟨ ψ ⟩→ _ ⊣|
  exact-snoc-diag (G ⟨ φ ⟩→ s) ψ = G ⟨ φ ⟩→ exact-snoc-diag s ψ

  exact-concat-diag : ∀ {i} {G H K : Group i}
    → ExactDiag G H → ExactDiag H K → ExactDiag G K
  exact-concat-diag (G ⊣|) s₂ = s₂
  exact-concat-diag (G ⟨ φ ⟩→ s₁) s₂ = G ⟨ φ ⟩→ (exact-concat-diag s₁ s₂)

abstract
  exact-concat : ∀ {i} {G H K L : Group i}
    {diag₁ : ExactDiag G H} {φ : H →ᴳ K} {diag₂ : ExactDiag K L}
    → ExactSeq (exact-snoc-diag diag₁ φ) → ExactSeq (H ⟨ φ ⟩→ diag₂)
    → ExactSeq (exact-concat-diag diag₁ (H ⟨ φ ⟩→ diag₂))
  exact-concat {diag₁ = G ⊣|} exact-seq-one es₂ = es₂
  exact-concat {diag₁ = G ⟨ ψ ⟩→ H ⊣|} (exact-seq-two ex _) es₂ =
    exact-seq-two ex es₂
  exact-concat {diag₁ = G ⟨ ψ ⟩→ H ⟨ χ ⟩→ s} (exact-seq-two ex es₁) es₂ =
    exact-seq-two ex (exact-concat {diag₁ = H ⟨ χ ⟩→ s} es₁ es₂)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
module Sigma.Renaming.Properties where

open import Data.Nat using (ℕ; _+_; zero; suc)
open import Data.Fin using (Fin; zero; suc)

open import Sigma.Subst.Core
open import Sigma.Renaming.Base

open import Sigma.Subst.Properties using (extensionality)

open import Function using (_∘_)

open import Relation.Binary.PropositionalEquality as Eq
  using (_≡_; refl; cong; cong₂)
open Eq.≡-Reasoning

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

⇑-cong : ∀ { m n } { ρ₁ ρ₂ : Ren m n }
  → ρ₁ ≡ ρ₂
  -- -----------
  → ρ₁ ⇑ ≡ ρ₂ ⇑
⇑-cong ρ₁≡ρ₂ = cong (_⇑) ρ₁≡ρ₂

⇑✶-cong : ∀ { m n } k { ρ₁ ρ₂ : Ren m n }
  → ρ₁ ≡ ρ₂
  -- -----------
  → ρ₁ ⇑✶ k  ≡ ρ₂ ⇑✶ k
⇑✶-cong k ρ₁≡ρ₂ = cong (_⇑✶ k) ρ₁≡ρ₂

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

∘-⇑-distrib : ∀ { m n k } ( ρ₁ : Ren m n ) ( ρ₂ : Ren n k )
  → (ρ₂ ⇑ ∘ ρ₁ ⇑) ≡ (ρ₂ ∘ ρ₁) ⇑
∘-⇑-distrib ρ₁ ρ₂ = extensionality lemma
  where
    lemma : ∀ x → (ρ₂ ⇑ ∘ ρ₁ ⇑) x ≡ ((ρ₂ ∘ ρ₁) ⇑) x
    lemma zero = refl
    lemma (suc x) = refl

-- TODO:
-- generalized for ⇑✶

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

⇑-id : ∀ { n } → (id { n }) ⇑ ≡ id
⇑-id = extensionality lemma
  where
    lemma : ∀ { n } x → (id { n } ⇑) x ≡ x
    lemma zero = refl
    lemma (suc x) = refl

max_stars_repo_name: johnyob/agda-sigma

max_issues_repo_name: johnyob/agda-sigma

max_forks_repo_name: johnyob/agda-sigma


text:
-- Minimal implicational logic, PHOAS approach, initial encoding

module STLC where

-- Types

infixr 0 _=>_

data Ty : Set where
  UNIT :             Ty
  _=>_ : Ty -> Ty -> Ty

-- Context

Cx : Set1
Cx = Ty -> Set

-- Terms

infixl 1 _$_

data Tm (tc : Cx) : Ty -> Set
  where
    var : forall {a}   ->  tc a
                       ----------
                       -> Tm tc a

    lam : forall {a b} ->  (tc a -> Tm tc b)
                       ---------------------
                         -> Tm tc (a => b)

    _$_ : forall {a b} -> Tm tc (a => b) -> Tm tc a
                       ----------------------------
                               -> Tm tc b

T : Ty -> Set1
T a = forall {tc} -> Tm tc a

-- Example theorems

I : forall {a} -> T (a => a)
I = lam \x ->
      var x

K : forall {a b} -> T (a => b => a)
K = lam \x ->
      lam \_ ->
        var x

S : forall {a b c} -> T ((a => b => c) => (a => b) => a => c)
S = lam \f ->
      lam \g ->
        lam \x ->
          (var f $ var x) $ (var g $ var x)

SKK : forall {a} -> T (a => a)
SKK {a = a} = S {b = a => a} $ K $ K


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

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical

data A : Set where
  a  : A
  eq : a ≡ a

bad : ∀ i → eq i ≡ a
bad i j = eq (primIMin i (primINeg j))

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE bad #-}


text:
-- Allow holes in modules to import, by introducing a single general postulate.

module UNDEFINED where

postulate
  UNDEFINED : ∀ {ℓ} → {T : Set ℓ} → T

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
-- Andreas, 2017-01-18, issue #819, reported by stevana
-- Underscores should be preserved when case-splitting

data List (A : Set) : Set where
  _∷_ : (x : A)(xs : List A) → List A

data ⊥ : Set where

-- Case-splitting on x:
test : List ⊥ → ⊥
test (x ∷ _) = {!x!} -- split on x

-- I think the underscore should be kept.

expected : List ⊥ → ⊥
expected (() ∷ _)

-- Likewise here:

test′ : List ⊥ → List ⊥ → List ⊥ → ⊥
test′ (x ∷ _) ys _ = {!ys x!} -- split on ys and x

expected′ : List ⊥ → List ⊥ → List ⊥ → ⊥
expected′ (() ∷ _) (x ∷ ys) _

max_forks_repo_name: Agda-zh/agda


text:
module Class.Map where

open import Class.Equality
open import Data.Maybe using (Maybe; just; nothing)
open import Data.List using (List; []; _∷_; [_])

record MapClass (K : Set) {{_ : EqB K}} (M : Set -> Set) : Set₁ where
  field
    insert : ∀ {V} -> K -> V -> M V -> M V
    remove : ∀ {V} -> K -> M V -> M V
    lookup : ∀ {V} -> K -> M V -> Maybe V
    mapSnd : ∀ {V C} -> (V -> C) -> M V -> M C
    emptyMap : ∀ {V} -> M V

open MapClass {{...}} public

mapFromList : ∀ {K V M} {{_ : EqB K}} {{_ : MapClass K M}} -> (V -> K) -> List V -> M (List V)
mapFromList f [] = emptyMap
mapFromList f (x ∷ l) with mapFromList f l
... | m with lookup (f x) m
... | just x₁ = insert (f x) (x ∷ x₁) m
... | nothing = insert (f x) [ x ] m


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

open import M-types.Base

module M-types.Coalg.M {ℓ : Level} (A : Ty ℓ) (B : A → Ty ℓ) where
    open import M-types.Coalg.Core A B
    open import M-types.Coalg.Bisim A B

    IsFinM : ∏[ M ∈ Coalg ] ∏[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        Ty (ℓ-suc ℓ)
    IsFinM M coiter = ∏[ X ∈ Coalg ] ∏[ f ∈ CoalgMor X M ] f ≡ coiter X

    FinM : Ty (ℓ-suc ℓ)
    FinM = ∑[ M ∈ Coalg ] ∑[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        IsFinM M coiter

    IsCohM : ∏[ M ∈ Coalg ] ∏[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        Ty (ℓ-suc ℓ)
    IsCohM M coiter =
        ∏[ X ∈ Coalg ] ∏[ f₀ ∈ CoalgMor X M ] ∏[ f₁ ∈ CoalgMor X M ]
        ∑[ p ∈ fun f₀ ≡ fun f₁ ] ∏[ x ∈ ty X ]
        ap (λ f → obs M (f x)) p · ≡-apply (com f₁) x ≡
        ≡-apply (com f₀) x · ap (λ f → P-Fun f (obs X x)) p

    CohM : Ty (ℓ-suc ℓ)
    CohM = ∑[ M ∈ Coalg ] ∑[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        IsCohM M coiter

    IsBareM : ∏[ M ∈ Coalg ] ∏[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        Ty (ℓ-suc ℓ)
    IsBareM M coiter =
        ∏[ X ∈ Coalg ] ∏[ f₀ ∈ CoalgMor X M ] ∏[ f₁ ∈ CoalgMor X M ]
        (fun f₀ ≡ fun f₁)

    BareM : Ty (ℓ-suc ℓ)
    BareM = ∑[ M ∈ Coalg ] ∑[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        IsBareM M coiter

    IsTyBisimM : ∏[ M ∈ Coalg ] ∏[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        Ty (ℓ-suc ℓ)
    IsTyBisimM M coiter =
        ∏[ ∼ ∈ TyBisim M ] SpanRelMor (spanRel {M} ∼) ≡-spanRel

    TyBisimM : Ty (ℓ-suc ℓ)
    TyBisimM = ∑[ M ∈ Coalg ] ∑[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        IsTyBisimM M coiter

    IsFunBisimM : ∏[ M ∈ Coalg ] ∏[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        Ty (ℓ-suc ℓ)
    IsFunBisimM M coiter =
        ∏[ ∼ ∈ FunBisim M ] DepRelMor (depRel {M} ∼) ≡-depRel

    FunBisimM : Ty (ℓ-suc ℓ)
    FunBisimM = ∑[ M ∈ Coalg ] ∑[ coiter ∈ (∏[ X ∈ Coalg ] CoalgMor X M) ]
        IsFunBisimM M coiter

    FinM→CohM : {M : Coalg} {coiter : ∏[ X ∈ Coalg ] CoalgMor X M} →
        IsFinM M coiter → IsCohM M coiter
    FinM→CohM {M} {coiter} isFin = λ X → λ f₀ → λ f₁ →
        coh (isFin X f₀ · isFin X f₁ ⁻¹)
        where
            coh : {X : Coalg} {f₀ f₁ : CoalgMor X M} →
                (f₀ ≡ f₁) → (
                    ∑[ p ∈ fun f₀ ≡ fun f₁ ] ∏[ x ∈ ty X ]
                    ap (λ f → obs M (f x)) p · ≡-apply (com f₁) x ≡
                    ≡-apply (com f₀) x · ap (λ f → P-Fun f (obs X x)) p
                )
            coh {X} {f} {f} refl =
                (
                    refl ,
                    λ x →
                        ·-neutr₀ ( ≡-apply (com f) x) ·
                        ·-neutr₁ ( ≡-apply (com f) x) ⁻¹
                )

    CohM→FinM : {M : Coalg} {coiter : ∏[ X ∈ Coalg ] CoalgMor X M} →
        IsCohM M coiter → IsFinM M coiter
    CohM→FinM {M} {coiter} isCoh = λ X → λ f →
        fin (isCoh X f (coiter X))
        where
            fin : {X : Coalg} {f : CoalgMor X M} →
                (
                    ∑[ p ∈ fun f ≡ fun (coiter X) ] ∏[ x ∈ ty X ]
                    ap (λ f → obs M (f x)) p · ≡-apply (com (coiter X)) x ≡
                    ≡-apply (com f) x · ap (λ f → P-Fun f (obs X x)) p
                ) → (f ≡ coiter X)
            fin {X} {f} (refl , coh) =
                ≡-pair (
                    refl ,
                    (hom₀ (≡-apply , funext-axiom) (com f)) ⁻¹ ·
                    ap funext (funext (λ x →
                        (·-neutr₁ (≡-apply (com f) x)) ⁻¹ ·
                        (coh x) ⁻¹ ·
                        (·-neutr₀ (≡-apply (com (coiter X)) x))
                    )) ·
                    (hom₀ (≡-apply , funext-axiom) (com (coiter X)))
                )

    CohM→BareM : {M : Coalg} {coiter : ∏[ X ∈ Coalg ] CoalgMor X M} →
        IsCohM M coiter → IsBareM M coiter
    CohM→BareM {M} {coiter} isCoh = λ X → λ f₀ → λ f₁ → pr₀ (isCoh X f₀ f₁)

    BareM→TyBisimM : {M : Coalg} {coiter : ∏[ X ∈ Coalg ] CoalgMor X M} →
        IsBareM M coiter → IsTyBisimM M coiter
    BareM→TyBisimM {M} {coiter} isBare = λ ∼ →
        (
            fun (ρ₀ ∼) ,
            refl ,
            isBare (ty ∼) (ρ₀ ∼) (ρ₁ ∼)
        )

    TyBisimM→BareM : {M : Coalg} {coiter : ∏[ X ∈ Coalg ] CoalgMor X M} →
        IsTyBisimM M coiter → IsBareM M coiter
    TyBisimM→BareM {M} {coiter} isTyBisim = λ X → λ f₀ → λ f₁ →
        funext (λ x →
            (≡-apply (com₀ (isTyBisim (X , f₀ , f₁))) x) ⁻¹ ·
            (≡-apply (com₁ (isTyBisim (X , f₀ , f₁))) x)
        )

    TyBisimM→FunBisimM : {M : Coalg} {coiter : ∏[ X ∈ Coalg ] CoalgMor X M} →
        IsTyBisimM M coiter → IsFunBisimM M coiter
    TyBisimM→FunBisimM {M} {coiter} isTyBisim = λ ∼ → let
            f : DepRelMor (depRel {M} ∼) (SpanRel→DepRel (DepRel→SpanRel (depRel {M} ∼)))
            f = DepRel→DepRel-mor (depRel {M} ∼)
            g : DepRelMor (SpanRel→DepRel (DepRel→SpanRel (depRel {M} ∼))) (SpanRel→DepRel ≡-spanRel)
            g = SpanRelMor→DepRelMor (isTyBisim (FunBisim→TyBisim {M} ∼))
            h : DepRelMor (SpanRel→DepRel ≡-spanRel) ≡-depRel
            h = ≡-SpanRel→DepRel-mor
        in
            h ∘-depRel (g ∘-depRel f)

    FunBisimM→TyBisimM : {M : Coalg} {coiter : ∏[ X ∈ Coalg ] CoalgMor X M} →
        IsFunBisimM M coiter → IsTyBisimM M coiter
    FunBisimM→TyBisimM {M} {coiter} isFunBisim = λ ∼ → let
            f : SpanRelMor (spanRel {M} ∼) (DepRel→SpanRel (SpanRel→DepRel (spanRel {M} ∼)))
            f = SpanRel→SpanRel-mor (spanRel {M} ∼)
            g : SpanRelMor (DepRel→SpanRel (SpanRel→DepRel (spanRel {M} ∼))) (DepRel→SpanRel ≡-depRel)
            g = DepRelMor→SpanRelMor (isFunBisim (TyBisim→FunBisim {M} ∼))
            h : SpanRelMor (DepRel→SpanRel ≡-depRel) ≡-spanRel
            h = ≡-DepRel→SpanRel-mor
        in
            -- h ∘-spanRel (g ∘-spanRel f)
            _∘-spanRel_ {ℓ} {ty M} {spanRel {M} ∼} {DepRel→SpanRel ≡-depRel} {≡-spanRel}
            h
            (_∘-spanRel_ {ℓ} {ty M} {spanRel {M} ∼} {DepRel→SpanRel (SpanRel→DepRel (spanRel {M} ∼))} {DepRel→SpanRel ≡-depRel} g f)

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


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

module PermutationProperties where

open import Data.Nat using (ℕ; _+_)
open import Data.Fin using (Fin)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; module ≡-Reasoning; proof-irrelevance; setoid)
open import Function.Equality   using    (_⟨$⟩_)
open import Data.Sum using (_⊎_)
open import Data.Product using (_,_; proj₁; proj₂)
--

import FinEquivPlusTimes using (module Plus) -- don't open, just import
import FinEquivTypeEquiv using (module PlusE) -- don't open, just import
open FinEquivPlusTimes.Plus using (⊎≃+; +≃⊎)
open FinEquivTypeEquiv.PlusE using (_+F_)
open import ConcretePermutation
open import Permutation
open import SEquivSCPermEquiv
open import Equiv using (_●_; id≃; sym≃; _⊎≃_)
open import EquivEquiv
  using (id≋; sym≋; ●-assoc; _◎_; lid≋; rid≋; linv≋; rinv≋;
     module ≋-Reasoning)
open import TypeEquivEquiv using (_⊎≋_)
open import FinEquivEquivPlus using ([id+id]≋id; +●≋●+)

open ≋-Reasoning

------------------------------------------------------------------------------
-- Composition

assocp : ∀ {m₁ m₂ m₃ n₁} → {p₁ : CPerm m₁ n₁} → {p₂ : CPerm m₂ m₁} →
  {p₃ : CPerm m₃ m₂} →
  (p₁ ●p p₂) ●p p₃ ≡ p₁ ●p (p₂ ●p p₃)
assocp {p₁ = p₁} {p₂} {p₃} =
  let e₁ = p⇒e p₁ in let e₂ = p⇒e p₂ in let e₃ = p⇒e p₃ in
  ≋⇒≡ (begin (
  p⇒e (e⇒p (e₁ ● e₂)) ● e₃
    ≋⟨ left-α-over-● (e₁ ● e₂) e₃ ⟩
  (e₁ ● e₂) ● e₃
    ≋⟨ ●-assoc {f = e₃} {e₂} {e₁} ⟩
  e₁ ● (e₂ ● e₃)
    ≋⟨ sym≋ (right-α-over-● e₁ (e₂ ● e₃)) ⟩
   e₁ ● (p⇒e (e⇒p (e₂ ● e₃))) ∎))

lidp : ∀ {m₁ m₂} {p : CPerm m₂ m₁} → idp ●p p ≡ p
lidp {p = p} = trans (≋⇒≡ (begin (
  (p⇒e (e⇒p id≃)) ● (p⇒e p)
    ≋⟨ left-α-over-● id≃ (p⇒e p) ⟩
  id≃ ● (p⇒e p)
    ≋⟨ lid≋ ⟩
  (p⇒e p) ∎))) (βu refl)

ridp : ∀ {m₁ m₂} {p : CPerm m₂ m₁} → p ●p idp ≡ p
ridp {p = p} = trans (≋⇒≡ (begin (
  (p⇒e p) ● (p⇒e (e⇒p id≃))
    ≋⟨ right-α-over-● (p⇒e p) id≃ ⟩
  (p⇒e p) ● id≃
    ≋⟨ rid≋ ⟩
  (p⇒e p) ∎))) (βu refl)

-- Inverses

rinv : ∀ {m₁ m₂} (p : CPerm m₂ m₁) → p ●p (symp p) ≡ idp
rinv p = let e = p⇒e p in ≋⇒≡ (begin (
  e ● (p⇒e (e⇒p (sym≃ e)))
    ≋⟨ right-α-over-● e (sym≃ e) ⟩
  e ● (sym≃ e)
    ≋⟨ rinv≋ e ⟩
  id≃ ∎))

linv : ∀ {m₁ m₂} (p : CPerm m₂ m₁) → (symp p) ●p p ≡ idp
linv p = let e = p⇒e p in ≋⇒≡ (begin (
  (p⇒e (e⇒p (sym≃ e))) ● e
    ≋⟨ left-α-over-● (sym≃ e) e ⟩
  (sym≃ e) ● e
    ≋⟨ linv≋ e ⟩
  id≃ ∎))

-- p₁ ⊎p p₂ = e⇒p ((p⇒e p₁) +F (p⇒e p₂))
--   Fm≃Fn +F Fo≃Fp = ⊎≃+ ● Fm≃Fn ⊎≃ Fo≃Fp ● +≃⊎
⊎p●p≡●p⊎p : {m₁ m₂ n₁ n₂ o₁ o₂ : ℕ} →
  {f : CPerm n₁ m₁} {g : CPerm n₂ m₂} {h : CPerm o₁ n₁} {i : CPerm o₂ n₂} →
  ((f ●p h) ⊎p (g ●p i)) ≡ ((f ⊎p g) ●p (h ⊎p i))
⊎p●p≡●p⊎p {f = f} {g} {h} {i} =
  let e₁ = p⇒e f in let e₂ = p⇒e g in let e₃ = p⇒e h in let e₄ = p⇒e i in
  let f≋ = id≋ {x = ⊎≃+} in
  let g≋ = id≋ {x = +≃⊎} in
  ≋⇒≡ (begin -- inline ⊎p
  p⇒e (e⇒p (e₁ ● e₃)) +F p⇒e (e⇒p (e₂ ● e₄))
    ≋⟨ id≋ ⟩ -- inline +F
  ⊎≃+ ● (p⇒e (e⇒p (e₁ ● e₃)) ⊎≃ p⇒e (e⇒p (e₂ ● e₄))) ● +≃⊎
    ≋⟨ f≋ ◎ ((α₁ ⊎≋ α₁) ◎ g≋) ⟩
  ⊎≃+ ● ((e₁ ● e₃) ⊎≃ (e₂ ● e₄)) ● +≃⊎
    ≋⟨ +●≋●+ ⟩
  (e₁ +F e₂) ● (e₃ +F e₄)
    ≋⟨ sym≋ ((α₁ {e = e₁ +F e₂}) ◎ (α₁ {e = e₃ +F e₄})) ⟩
  (p⇒e (e⇒p (e₁ +F e₂)) ● p⇒e (e⇒p (e₃ +F e₄))) ∎)

-- Additives

1p⊎1p≡1p : ∀ {m n} → idp {m} ⊎p idp {n} ≡ idp {m + n}
1p⊎1p≡1p {m} {n} =
  let em = p⇒e (e⇒p (id≃ {A = Fin m})) in
  let en = p⇒e (e⇒p (id≃ {A = Fin n})) in
  let f≋ = id≋ {x = ⊎≃+ {m} {n}} in
  let g≋ = id≋ {x = +≃⊎ {m} {n}} in
  ≋⇒≡ (begin (
  em +F en
    ≋⟨ id≋ ⟩
  ⊎≃+ ● em ⊎≃ en ● +≃⊎
    ≋⟨ f≋ ◎ ((α₁ ⊎≋ α₁) ◎ g≋) ⟩
  ⊎≃+ ● (id≃ {A = Fin m}) ⊎≃ id≃ ● +≃⊎
    ≋⟨ [id+id]≋id ⟩
  id≃ {A = Fin (m + n)} ∎))

-- interaction with composition
{-  The underlying permutations are no longer defined!
unite+p∘[0⊎x]≡x∘unite+p : ∀ {m n} (p : CPerm m n) →
  transp unite+p (0p ⊎p p) ≡ transp p unite+p
unite+p∘[0⊎x]≡x∘unite+p p = p≡ unite+∘[0⊎x]≡x∘unite+

uniti+p∘x≡[0⊎x]∘uniti+p : ∀ {m n} (p : CPerm m n) →
  transp uniti+p p ≡ transp (0p ⊎p p) uniti+p
uniti+p∘x≡[0⊎x]∘uniti+p p = p≡ (uniti+∘x≡[0⊎x]∘uniti+ {x = CPerm.π p})

uniti+rp∘[x⊎0]≡x∘uniti+rp : ∀ {m n} (p : CPerm m n) →
  transp uniti+rp (p ⊎p 0p) ≡ transp p uniti+rp
uniti+rp∘[x⊎0]≡x∘uniti+rp p = p≡ uniti+r∘[x⊎0]≡x∘uniti+r
-}

{-
unite+rp∘[x⊎0]≡x∘unite+rp : ∀ {m n} (p : CPerm m n) →
  transp unite+rp p ≡ transp (p ⊎p 0p) unite+rp
unite+rp∘[x⊎0]≡x∘unite+rp p = p≡ unite+r∘[x⊎0]≡x∘unite+r
-}

-- Multiplicatives
{-
1p×1p≡1p : ∀ {m n} → idp {m} ×p idp {n} ≡ idp
1p×1p≡1p {m} = p≡ (1C×1C≡1C {m})

×p-distrib :  ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → {p₁ : CPerm m₁ n₁} → {p₂ : CPerm m₂ n₂}
    → {p₃ : CPerm m₃ m₁} → {p₄ : CPerm m₄ m₂} →
      (transp p₁ p₃) ×p (transp p₂ p₄) ≡ transp (p₁ ×p p₂) (p₃ ×p p₄)
×p-distrib {p₁ = p₁} = p≡ (sym (×c-distrib {p₁ = CPerm.π p₁}))
-}
------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Logic.IntroInstances where

import      Data.Tuple as Tuple
import      Lvl
open import Logic.Predicate
open import Logic.Propositional
open import Type

private variable ℓ : Lvl.Level
private variable A B Obj : Type{ℓ}
private variable P : Obj → Type{ℓ}
private variable x : Obj

instance
  [∧]-intro-instance : ⦃ _ : A ⦄ → ⦃ _ : B ⦄ → (A ∧ B)
  [∧]-intro-instance ⦃ a ⦄ ⦃ b ⦄ = [∧]-intro a b

instance
  [∨]-introₗ-instance : ⦃ _ : A ⦄ → (A ∨ B)
  [∨]-introₗ-instance ⦃ a ⦄ = [∨]-introₗ a

instance
  [∨]-introᵣ-instance : ⦃ _ : B ⦄ → (A ∨ B)
  [∨]-introᵣ-instance ⦃ b ⦄ = [∨]-introᵣ b

instance
  [∃]-intro-instance : ⦃ _ : P(x) ⦄ → ∃(P)
  [∃]-intro-instance {x = x} ⦃ proof ⦄ = [∃]-intro (x) ⦃ proof ⦄

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- A container for finite binary trees with information in internal
-- nodes
------------------------------------------------------------------------

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

open import Equality

module Container.Tree
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Prelude hiding (id; _∘_; List; []; _∷_)

open import Bijection eq using (_↔_; module _↔_)
open import Container eq hiding (Shape; Position)
open import Container.List eq hiding (fold; fold-lemma)
open import Function-universe eq
import Tree eq as Tree

------------------------------------------------------------------------
-- The type

-- Shapes.

data Shape : Type where
  lf : Shape
  nd : Shape → Shape → Shape

-- Positions.

data Position : Shape → Type where
  root  : ∀ {l r} → Position (nd l r)
  left  : ∀ {l r} → Position l → Position (nd l r)
  right : ∀ {l r} → Position r → Position (nd l r)

-- Trees.

Tree : Container lzero
Tree = Shape ▷ Position

------------------------------------------------------------------------
-- An isomorphism

-- The type of shapes is isomorphic to Tree.Tree ⊤.
--
-- This lemma is included because it was mentioned in the paper "Bag
-- Equivalence via a Proof-Relevant Membership Relation".

Shape↔Tree-⊤ : Shape ↔ Tree.Tree ⊤
Shape↔Tree-⊤ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to : Shape → Tree.Tree ⊤
  to lf       = Tree.leaf
  to (nd l r) = Tree.node (to l) tt (to r)

  from : Tree.Tree ⊤ → Shape
  from Tree.leaf          = lf
  from (Tree.node l tt r) = nd (from l) (from r)

  to∘from : ∀ t → to (from t) ≡ t
  to∘from Tree.leaf          = refl _
  to∘from (Tree.node l tt r) =
    cong₂ (λ l r → Tree.node l tt r) (to∘from l) (to∘from r)

  from∘to : ∀ s → from (to s) ≡ s
  from∘to lf       = refl _
  from∘to (nd l r) = cong₂ nd (from∘to l) (from∘to r)

------------------------------------------------------------------------
-- Constructors

-- Leaves.

leaf : {A : Type} → ⟦ Tree ⟧ A
leaf = (lf , λ ())

-- Internal nodes.

node : {A : Type} → ⟦ Tree ⟧ A → A → ⟦ Tree ⟧ A → ⟦ Tree ⟧ A
node (l , lkup-l) x (r , lkup-r) =
  ( nd l r
  , λ { root      → x
      ; (left  p) → lkup-l p
      ; (right p) → lkup-r p
      }
  )

-- Even if we don't assume extensionality we can prove that
-- intensionally distinct implementations of the constructors are bag
-- equivalent.

leaf≈ : {A : Type} {lkup : _ → A} →
        _≈-bag_ {C₂ = Tree} leaf (lf , lkup)
leaf≈ _ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (() , _) }
      ; from = λ { (() , _) }
      }
    ; right-inverse-of = λ { (() , _) }
    }
  ; left-inverse-of = λ { (() , _) }
  }

node≈ : ∀ {A : Type} {l r} {lkup : _ → A} →
        _≈-bag_ {C₂ = Tree}
                (node (l , lkup ∘ left) (lkup root) (r , lkup ∘ right))
                (nd l r , lkup)
node≈ _ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (root    , eq) → (root    , eq)
                 ; (left p  , eq) → (left p  , eq)
                 ; (right p , eq) → (right p , eq)
                 }
      ; from = λ { (root    , eq) → (root    , eq)
                 ; (left p  , eq) → (left p  , eq)
                 ; (right p , eq) → (right p , eq)
                 }
      }
    ; right-inverse-of = λ { (root    , eq) → refl _
                           ; (left p  , eq) → refl _
                           ; (right p , eq) → refl _
                           }
    }
  ; left-inverse-of = λ { (root    , eq) → refl _
                        ; (left p  , eq) → refl _
                        ; (right p , eq) → refl _
                        }
  }

-- Any lemmas for the constructors.

Any-leaf : ∀ {A : Type} (P : A → Type) →
           Any P leaf ↔ ⊥₀
Any-leaf _ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (() , _) }
      ; from = λ ()
      }
    ; right-inverse-of = λ ()
    }
  ; left-inverse-of = λ { (() , _) }
  }

Any-node : ∀ {A : Type} (P : A → Type) {l x r} →
           Any P (node l x r) ↔ Any P l ⊎ P x ⊎ Any P r
Any-node _ {l = _ , _} {r = _ , _} = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (root    , eq) → inj₂ (inj₁ eq)
                 ; (left p  , eq) → inj₁ (p , eq)
                 ; (right p , eq) → inj₂ (inj₂ (p , eq))
                 }
      ; from = λ { (inj₁ (p , eq))        → (left p  , eq)
                 ; (inj₂ (inj₁ eq))       → (root    , eq)
                 ; (inj₂ (inj₂ (p , eq))) → (right p , eq)
                 }
      }
    ; right-inverse-of = λ { (inj₁ (p , eq))        → refl _
                           ; (inj₂ (inj₁ eq))       → refl _
                           ; (inj₂ (inj₂ (p , eq))) → refl _
                           }
    }
  ; left-inverse-of = λ { (root    , eq) → refl _
                        ; (left p  , eq) → refl _
                        ; (right p , eq) → refl _
                        }
  }

------------------------------------------------------------------------
-- More functions

-- Singleton trees.

singleton : {A : Type} → A → ⟦ Tree ⟧ A
singleton x = node leaf x leaf

-- Any lemma for singleton.

Any-singleton : ∀ {A : Type} (P : A → Type) {x} →
                Any P (singleton x) ↔ P x
Any-singleton P {x} =
  Any P (singleton x)            ↔⟨⟩
  Any P (node leaf x leaf)       ↔⟨ Any-node P ⟩
  Any P leaf ⊎ P x ⊎ Any P leaf  ↔⟨ Any-leaf P ⊎-cong id ⊎-cong Any-leaf P ⟩
  ⊥ ⊎ P x ⊎ ⊥                    ↔⟨ ⊎-left-identity ⟩
  P x ⊎ ⊥                        ↔⟨ ⊎-right-identity ⟩
  P x                            □

-- For the design considerations underlying the inclusion of fold and
-- fold-lemma, see Container.List.fold/fold-lemma.

-- A fold for trees. (Well, this is not a catamorphism, it is a
-- paramorphism.)

fold : {A B : Type} →
       B → (⟦ Tree ⟧ A → A → ⟦ Tree ⟧ A → B → B → B) → ⟦ Tree ⟧ A → B
fold {A} {B} fl fn = uncurry fold′
  where
  fold′ : (s : Shape) → (Position s → A) → B
  fold′ lf       lkup = fl
  fold′ (nd l r) lkup =
    fn (l , lkup ∘ left )
       (lkup root)
       (r , lkup ∘ right)
       (fold′ l (lkup ∘ left ))
       (fold′ r (lkup ∘ right))

-- A lemma which can be used to prove properties about fold.
--
-- The "respects bag equivalence" argument could be omitted if
-- equality of functions were extensional.

fold-lemma : ∀ {A B : Type}
               {fl : B} {fn : ⟦ Tree ⟧ A → A → ⟦ Tree ⟧ A → B → B → B}
             (P : ⟦ Tree ⟧ A → B → Type) →
             (∀ t₁ t₂ → t₁ ≈-bag t₂ → ∀ b → P t₁ b → P t₂ b) →
             P leaf fl →
             (∀ l x r b₁ b₂ →
                P l b₁ → P r b₂ → P (node l x r) (fn l x r b₁ b₂)) →
             ∀ t → P t (fold fl fn t)
fold-lemma {A} {fl = fl} {fn} P resp P-le P-no = uncurry fold-lemma′
  where
  fold-lemma′ : (s : Shape) (lkup : Position s → A) →
                P (s , lkup) (fold fl fn (s , lkup))
  fold-lemma′ lf       lkup = resp _ _ leaf≈ _ P-le
  fold-lemma′ (nd l r) lkup = resp _ _ node≈ _ $
    P-no _ _ _ _ _
       (fold-lemma′ l (lkup ∘ left ))
       (fold-lemma′ r (lkup ∘ right))

-- Inorder flattening of a tree.

flatten : {A : Type} → ⟦ Tree ⟧ A → ⟦ List ⟧ A
flatten = fold [] (λ _ x _ xs ys → xs ++ x ∷ ys)

-- Flatten does not add or remove any elements.

flatten≈ : {A : Type} (t : ⟦ Tree ⟧ A) → flatten t ≈-bag t
flatten≈ = fold-lemma
  (λ t xs → xs ≈-bag t)

  (λ t₁ t₂ t₁≈t₂ xs xs≈t₁ z →
     z ∈ xs  ↔⟨ xs≈t₁ z ⟩
     z ∈ t₁  ↔⟨ t₁≈t₂ z ⟩
     z ∈ t₂  □)

  (λ z →
   z ∈ []    ↔⟨ Any-[] (λ x → z ≡ x) ⟩
   ⊥         ↔⟨ inverse $ Any-leaf (λ x → z ≡ x) ⟩
   z ∈ leaf  □)

  (λ l x r xs ys xs≈l ys≈r z →
     z ∈ xs ++ x ∷ ys         ↔⟨ Any-++ (λ x → z ≡ x) _ _ ⟩
     z ∈ xs ⊎ z ∈ x ∷ ys      ↔⟨ id ⊎-cong Any-∷ (λ x → z ≡ x) ⟩
     z ∈ xs ⊎ z ≡ x ⊎ z ∈ ys  ↔⟨ xs≈l z ⊎-cong id ⊎-cong ys≈r z ⟩
     z ∈ l ⊎ z ≡ x ⊎ z ∈ r    ↔⟨ inverse $ Any-node (λ x → z ≡ x) ⟩
     z ∈ node l x r           □)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality