text:
module Data.Proofs where

import      Lvl
open import Data
open import Logic
open import Logic.Propositional
open import Structure.Setoid renaming (_≡_ to _≡ₛ_)
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Type
open import Type.Properties.Empty
open import Type.Properties.Singleton

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ ℓ₁ ℓ₂ : Lvl.Level
private variable T : Type{ℓ}

module General where
  module _ {_▫_ : Empty{ℓ} → Empty{ℓ} → Stmt{ℓₑ}} where
    Empty-equiv : Equiv(Empty)
    Equiv._≡_ Empty-equiv = _▫_
    Reflexivity.proof  (Equivalence.reflexivity  (Equiv.equivalence Empty-equiv)) {}
    Symmetry.proof     (Equivalence.symmetry     (Equiv.equivalence Empty-equiv)) {}
    Transitivity.proof (Equivalence.transitivity (Equiv.equivalence Empty-equiv)) {}

  -- Any binary relation on Unit is an equivalence given that it is reflexive.
  module _ {_▫_ : Unit{ℓ} → Unit{ℓ} → Stmt{ℓ}} ⦃ proof : (<> ▫ <>) ⦄ where
    Unit-equiv : Equiv(Unit)
    Equiv._≡_ Unit-equiv = (_▫_)
    Reflexivity.proof  (Equivalence.reflexivity  (Equiv.equivalence Unit-equiv))       = proof
    Symmetry.proof     (Equivalence.symmetry     (Equiv.equivalence Unit-equiv)) _     = proof
    Transitivity.proof (Equivalence.transitivity (Equiv.equivalence Unit-equiv)) _ _   = proof

module _ where
  open import Relator.Equals

  instance
    Empty-equiv : Equiv(Empty{ℓ})
    Empty-equiv = General.Empty-equiv {_▫_ = _≡_}

  instance
    Unit-equiv : Equiv(Unit{ℓ})
    Unit-equiv = General.Unit-equiv ⦃ [≡]-intro {x = <>} ⦄

  {- TODO: So, why is this unprovable but Unit-IsUnit is? UIP? What is the difference?
  module _ where
    open import Relator.Equals.Proofs.Equiv
    testee : ∀{T : Type{ℓ}}{a : T} → IsUnit{ℓ}(a ≡ a)
    IsUnit.unit       testee     = [≡]-intro
    IsUnit.uniqueness testee {x} = {!!}
  -}

instance
  -- `Unit` is an unit type.
  Unit-IsUnit : ⦃ equiv : Equiv{ℓₑ}(Unit) ⦄ → IsUnit{ℓ}(Unit)
  IsUnit.unit       Unit-IsUnit = <>
  IsUnit.uniqueness Unit-IsUnit = reflexivity(_≡ₛ_)

instance
  -- `Empty` is an empty type.
  Empty-IsEmpty : IsEmpty{ℓ}(Empty)
  Empty-IsEmpty = intro(empty)

module _ ⦃ _ : Equiv{ℓₑ₁}(T) ⦄ ⦃ empty-equiv : Equiv{ℓₑ₂}(Empty{ℓ₂}) ⦄ where
  instance
    empty-injective : Injective ⦃ empty-equiv ⦄(empty{T = T})
    Injective.proof(empty-injective) {}

  instance
    empty-function : Function ⦃ empty-equiv ⦄(empty{T = T})
    Function.congruence empty-function {()}

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where -- TODO: Duplicated in Type.Properties.Singleton.Proofs
  Unit-fn-unique-value : ∀{f : Unit{ℓ} → T} → (∀{x y} → (f(x) ≡ₛ f(y)))
  Unit-fn-unique-value {x = <>} {y = <>} = reflexivity(_≡ₛ_)

module _ ⦃ equiv : Equiv{ℓₑ}(Unit{ℓ₁}) ⦄ where
  Unit-fn-unique-fn : ∀{f g : T → Unit{ℓ₁}} → (∀{x y} → (_≡ₛ_ ⦃ equiv ⦄ (f(x)) (g(y))))
  Unit-fn-unique-fn {f = f}{g = g}{x = x}{y = y} with f(x) | g(y)
  ... | <> | <> = reflexivity(_≡ₛ_ ⦃ equiv ⦄)


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output

-- This module defines the LBFT monad used by our (fake/simple,
-- for now) "implementation", along with some utility functions
-- to facilitate reasoning about it.

module LibraBFT.ImplShared.Util.Util where
  open import Optics.All
  open import LibraBFT.ImplShared.Util.Dijkstra.Syntax public
  open import LibraBFT.ImplShared.Util.Dijkstra.RWS public
  open import LibraBFT.ImplShared.Util.Dijkstra.RWS.Syntax public
  open import LibraBFT.ImplShared.Util.Dijkstra.EitherD public
  open import LibraBFT.ImplShared.Util.Dijkstra.EitherD.Syntax public
  ----------------
  -- LBFT Monad --
  ----------------

  -- Global 'LBFT'; works over the whole state.
  LBFT : Set → Set₁
  LBFT = RWS Unit Output RoundManager

  LBFT-run : ∀ {A} → LBFT A → RoundManager → (A × RoundManager × List Output)
  LBFT-run m = RWS-run m unit

  LBFT-result : ∀ {A} → LBFT A → RoundManager → A
  LBFT-result m rm = proj₁ (LBFT-run m rm)

  LBFT-post : ∀ {A} → LBFT A → RoundManager → RoundManager
  LBFT-post m rm = proj₁ (proj₂ (LBFT-run m rm))

  LBFT-outs : ∀ {A} → LBFT A → RoundManager → List Output
  LBFT-outs m rm = proj₂ (proj₂ (LBFT-run m rm))

  LBFT-Pre  = RoundManager → Set
  LBFT-Post = RWS-Post Output RoundManager

  LBFT-Post-True : ∀ {A} → LBFT-Post A → LBFT A → RoundManager → Set
  LBFT-Post-True Post m pre =
    let (x , post , outs) = LBFT-run m pre in
    Post x post outs

  LBFT-weakestPre : ∀ {A} (m : LBFT A)
                    → LBFT-Post A → LBFT-Pre
  LBFT-weakestPre m Post pre = RWS-weakestPre m Post unit pre

  LBFT-Contract : ∀ {A} (m : LBFT A) → Set₁
  LBFT-Contract{A} m =
    (Post : RWS-Post Output RoundManager A)
    → (pre : RoundManager) → LBFT-weakestPre m Post pre
    → LBFT-Post-True Post m pre

  LBFT-contract : ∀ {A} (m : LBFT A) → LBFT-Contract m
  LBFT-contract m Post pre pf = RWS-contract m Post unit pre pf

  LBFT-⇒
    : ∀ {A} (P Q : LBFT-Post A) → (RWS-Post-⇒ P Q)
    → ∀ m pre → LBFT-weakestPre m P pre → LBFT-weakestPre m Q pre
  LBFT-⇒ Post₁ Post₂ f m pre pf = RWS-⇒ Post₁ Post₂ f m unit pre pf

  LBFT-⇒-bind
    : ∀ {A B} (P : LBFT-Post A) (Q : LBFT-Post B) (f : A → LBFT B)
      → (RWS-Post-⇒ P (RWS-weakestPre-bindPost unit f Q))
      → ∀ m st → LBFT-weakestPre m P st → LBFT-weakestPre (m >>= f) Q st
  LBFT-⇒-bind Post Q f pf m st con = RWS-⇒-bind Post Q f unit pf m st con

  LBFT-⇒-ebind
    : ∀ {A B C} (P : LBFT-Post (Either C A)) (Q : LBFT-Post (Either C B))
      → (f : A → LBFT (Either C B))
      → RWS-Post-⇒ P (RWS-weakestPre-ebindPost unit f Q)
      → ∀ m st → LBFT-weakestPre m P st
      → LBFT-weakestPre (m ∙?∙ f) Q st
  LBFT-⇒-ebind Post Q f pf m st con =
    RWS-⇒-ebind Post Q f unit pf m st con

ext: agda

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
{-# OPTIONS --without-K #-}
module README where

-- This is a self-contained repository of basic results and utilities for
-- Homotopy Type Theory.
--
-- Modules are structured in a hierarchy, where all top-level modules are
-- imported in this file, and each module only imports and re-exports all
-- sub-modules. The most basic definitions for a submodule collection are
-- defined in the `core` submodule.
--
-- For example, in the case of equality, the module called `equality` is
-- composed of a number of submodules: `core` (containing the basic
-- definitions), `groupoid` (groupoid laws), `calculus` (for calculations
-- involving equality proofs) and `reasoning` (for equational reasoning).

-- Σ types and related utilities
import sum

-- Propositional equality
import equality

-- Basic types
import sets

-- Algebra
import algebra

-- Decidable predicates
import decidable

-- Pointed types and maps
import pointed

-- Functions, isomorphisms and properties thereof
import function

-- Overloading system
import overloading

-- Universe levels
import level

-- Container functors, W and M types
import container

-- Homotopy type theory infrastructure and results
import hott

-- Higher Inductive Types
import higher

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --cubical --guarded -W ignore #-}
module combinations-of-lift-and-multiset where

open import Clocked.Primitives
open import Cubical.Foundations.Everything
open import Cubical.Data.List as List
open import Cubical.Data.List.Properties
open import Cubical.Data.Sum using (_⊎_; inl; inr)
open import combinations-of-lift-and-list

--**************************************************************************--
--**************************************************************************--
-- Combining the monads Lift and Multiset freely and via a distributive law --
--**************************************************************************--
--**************************************************************************--

-- In this document I want to define a monad, called MultiLift, that is the free combination of the Lift monad and the Multiset monad.
-- In order to do so, I will first define the the Multiset monad, and check that it is indeed a monad (Step 1).
-- Then I define the LiftMulti monad, check that it is a monad (Step 2), and finally check that it is the free monad on the algebra
-- structures of a delay algebra and a monoid (Step 3).
-- The Lift monad has aleady been defined in my earlier work, combinations-of-lift-and-list.
-- In the same file I check that lift is indeed a monad, and define various usefull functions, such as a map function for Lift.

-- In addition to the free combination of the Multiset and the Lift monads, I also compose the two monads to form the monad
-- LcM : A → Lift(Multiset A). This composition uses a distributive law, which I prove does indeed satisfy all the axioms for a
-- distributive law.

--****************************--
-- Step 1: The Multiset monad --
--****************************--

--This code is based on the finite powerset example from:
--https://github.com/niccoloveltri/final-pfin/blob/main/Pfin/AsFreeJoinSemilattice.agda

--We define the multiset monad as the free commutative monoid monad on A.
--This is a HIT.

data Multiset {ℓ} (A : Type ℓ) : Type ℓ where
  m∅        : Multiset A
  unitM     : A → Multiset A
  _∪ₘ_      : Multiset A → Multiset A → Multiset A
  ass       : ∀ x y z → x ∪ₘ (y ∪ₘ z) ≡ (x ∪ₘ y) ∪ₘ z
  com       : ∀ x y → x ∪ₘ y ≡ y ∪ₘ x
  unitr     : ∀ x → x ∪ₘ m∅ ≡ x
  trunc     : isSet (Multiset A)

-- map function for Multiset
mapM : {A B : Set} → (A → B) → Multiset A → Multiset B
mapM f m∅ = m∅
mapM f (unitM x) = unitM (f x)
mapM f (M ∪ₘ N) = (mapM f M) ∪ₘ (mapM f N)
mapM f (ass M M₁ M₂ i) = ass (mapM f M) (mapM f M₁) (mapM f M₂) i
mapM f (com M N i) = com (mapM f M) (mapM f N) i
mapM f (unitr M i) = unitr (mapM f M) i
mapM f (trunc M N x y i i₁) = trunc (mapM f M) (mapM f N) (λ j → mapM f (x j)) (λ j → mapM f (y j)) i i₁

-- Bind and multiplication functions for Multiset
Multiset-bind : {A B : Set} → (A → Multiset B) → Multiset A → Multiset B
Multiset-bind f m∅ = m∅
Multiset-bind f (unitM a) = f a
Multiset-bind f (x ∪ₘ y) = (Multiset-bind f x) ∪ₘ (Multiset-bind f y)
Multiset-bind f (ass x y z i) = ass (Multiset-bind f x) (Multiset-bind f y) (Multiset-bind f z) i
Multiset-bind f (com x y i) = com (Multiset-bind f x) (Multiset-bind f y) i
Multiset-bind f (unitr x i) = unitr (Multiset-bind f x) i
Multiset-bind f (trunc s₁ s₂ x y i i₁) = trunc (Multiset-bind f s₁) (Multiset-bind f s₂) (\ j → Multiset-bind f (x j)) (\ j → Multiset-bind f (y j)) i i₁

Multiset-mult : {A : Set} → Multiset (Multiset A) → Multiset A
Multiset-mult m∅ = m∅
Multiset-mult (unitM x) = x
Multiset-mult (x ∪ₘ y) = (Multiset-mult x) ∪ₘ (Multiset-mult y)
Multiset-mult (ass x y z i) = ass (Multiset-mult x) (Multiset-mult y) (Multiset-mult z) i
Multiset-mult (com x y i) = com (Multiset-mult x) (Multiset-mult y) i
Multiset-mult (unitr x i) = unitr (Multiset-mult x) i
Multiset-mult (trunc s₁ s₂ x y i i₁) = trunc (Multiset-mult s₁) (Multiset-mult s₂) (\ j → Multiset-mult (x j)) (\ j → Multiset-mult (y j)) i i₁

-- Elimination principle for Multiset

-- module to make the inputs more readable
-- no name for the module to make the use of it more readable
module _ {ℓ}{A : Type ℓ}
         (P : Multiset A → hProp ℓ)
         (P∅ : fst (P m∅))
         (Pη : ∀ m → fst (P (unitM m)))
         (P∪ : ∀ {m n} → fst(P m) → fst(P n) → fst(P (m ∪ₘ n)))
         where

  elimM : ∀ M → fst(P M)
  elimM m∅ = P∅
  elimM (unitM x) = Pη x
  elimM (M ∪ₘ N) = P∪ (elimM M) (elimM N)
  elimM (ass M N O i) = isProp→PathP (λ j → snd (P (ass M N O j)))
                               ((P∪ (elimM M) (P∪ (elimM N) (elimM O))))
                               ((P∪ (P∪ (elimM M) (elimM N)) (elimM O) ))
                               i
  elimM (com M N i) = isProp→PathP (λ j → snd (P (com M N j))) (P∪ (elimM M) (elimM N)) (P∪ (elimM N) (elimM M)) i
  elimM (unitr M i) = isProp→PathP (λ j → snd (P (unitr M j))) (P∪ (elimM M) (P∅)) (elimM M) i
  elimM (trunc M N x y i j) = isOfHLevel→isOfHLevelDep 2 (λ k → isProp→isSet (snd (P k))) (elimM M) (elimM N) (cong elimM x) (cong elimM y)
                                      (trunc M N x y) i j

-- Proving that the Multiset forms a monad

-- Multiset-mult (unitM M) = M
Multiset-unitlaw1 : {A : Set} → ∀(M : Multiset A) → Multiset-mult (unitM M) ≡ M
Multiset-unitlaw1 M = refl

-- Multiset-mult (map unitM M) = M
Multiset-unitlaw2 : {A : Set} → ∀(M : Multiset A) → Multiset-mult (mapM unitM M) ≡ M
Multiset-unitlaw2 m∅ = refl
Multiset-unitlaw2 (unitM x) = refl
Multiset-unitlaw2 (M ∪ₘ N) = cong₂ (_∪ₘ_) (Multiset-unitlaw2 M) (Multiset-unitlaw2 N)
Multiset-unitlaw2 (ass M N P i) = λ j → ass (Multiset-unitlaw2 M j) (Multiset-unitlaw2 N j) (Multiset-unitlaw2 P j) i
Multiset-unitlaw2 (com M N i) = λ j → com (Multiset-unitlaw2 M j) (Multiset-unitlaw2 N j) i
Multiset-unitlaw2 (unitr M i) = λ j → unitr (Multiset-unitlaw2 M j) i
Multiset-unitlaw2 (trunc M N x y i i₁) = λ k → trunc (Multiset-unitlaw2 M k) (Multiset-unitlaw2 N k) (λ j → (Multiset-unitlaw2 (x j)) k) ((λ j → (Multiset-unitlaw2 (y j)) k)) i i₁

--proving the same with elimM:
Multiset-unitlaw2' : {A : Set} → ∀(M : Multiset A) → Multiset-mult (mapM unitM M) ≡ M
Multiset-unitlaw2' M = elimM
                        (λ N → (Multiset-mult (mapM unitM N) ≡ N) , trunc (Multiset-mult (mapM unitM N)) N)
                        refl
                        (λ N → refl)
                        (λ eq1 → λ eq2 → cong₂ _∪ₘ_ eq1 eq2 )
                        M

-- Multiset-mult (Multiset-mult M) = Multiset-mult (map Multiset-mult M)
Multiset-multlaw : {A : Set} → ∀(M : Multiset (Multiset (Multiset A))) →  Multiset-mult (Multiset-mult M) ≡ Multiset-mult (mapM Multiset-mult M)
Multiset-multlaw m∅ = refl
Multiset-multlaw (unitM M) = refl
Multiset-multlaw (M ∪ₘ N) = cong₂ (_∪ₘ_) (Multiset-multlaw M) (Multiset-multlaw N)
Multiset-multlaw (ass M N P i) = λ j → ass (Multiset-multlaw M j) (Multiset-multlaw N j) (Multiset-multlaw P j) i
Multiset-multlaw (com M N i) = λ j → com (Multiset-multlaw M j) (Multiset-multlaw N j) i
Multiset-multlaw (unitr M i) = λ j → unitr (Multiset-multlaw M j) i
Multiset-multlaw (trunc M N x y i i₁) = λ k → trunc (Multiset-multlaw M k) (Multiset-multlaw N k) (λ j → (Multiset-multlaw (x j)) k) ((λ j → (Multiset-multlaw (y j)) k)) i i₁

--proving the same with Elim:
Multiset-multlaw' :  {A : Set} → ∀(M : Multiset (Multiset (Multiset A))) →  Multiset-mult (Multiset-mult M) ≡ Multiset-mult (mapM Multiset-mult M)
Multiset-multlaw' M = elimM
                        (λ N → (Multiset-mult (Multiset-mult N) ≡ Multiset-mult (mapM Multiset-mult N))
                              , trunc (Multiset-mult (Multiset-mult N)) (Multiset-mult (mapM Multiset-mult N)))
                        refl
                        (λ N → refl)
                        (λ eq1 → λ eq2 → cong₂ (_∪ₘ_) eq1 eq2)
                        M

-- the unit is a natural transformation:
nattrans-Multunit : {A B : Set} → ∀(f : A → B) → ∀(x : A) → mapM f (unitM x) ≡ unitM (f x)
nattrans-Multunit f x = refl

-- the multiplication is a natural transformation:
nattrans-MultisetMult : {A B : Set} → ∀(f : A → B) → ∀(MM : Multiset (Multiset A)) → mapM f (Multiset-mult MM) ≡ Multiset-mult (mapM (mapM f) MM)
nattrans-MultisetMult f MM = elimM
                               ((λ NN →  (mapM f (Multiset-mult NN) ≡ Multiset-mult (mapM (mapM f) NN))
                                      , trunc (mapM f (Multiset-mult NN)) (Multiset-mult (mapM (mapM f) NN))))
                               refl
                               (λ M → refl)
                               (λ eq1 → λ eq2 → cong₂ (_∪ₘ_) eq1 eq2)
                               MM

--*****************************--
-- Step 2: The MultiLift monad --
--*****************************--

--Now that we have a multiset monad and a lift monad, I want to show that the following combination of the two is again a monad:
--MultiLift : (A : Set) → (κ : Cl) → Set
--MultiLift A κ = Multiset (A ⊎ (▹ κ (MultiLift A κ)))

data MultiLift (A : Set) (κ : Cl) : Set where
  conML : Multiset (A ⊎ (▹ κ (MultiLift A κ))) -> MultiLift A κ

-- Elimination principle for MultiLift

-- module to make the inputs more readable
-- no name for the module to make the use of it more readable
module _ {ℓ}{A : Set}{κ : Cl}
         (P : MultiLift A κ → hProp ℓ)
         (P∅ : fst (P (conML m∅)))
         (Pη1 : ∀ x → fst (P (conML (unitM (inl x)))))
         (Pη2 : ∀ {x} → (∀ α → fst (P (x α))) → fst (P (conML (unitM (inr x)))))
         (P∪ : ∀ {m n} → fst(P (conML m)) → fst(P (conML n)) → fst(P (conML (m ∪ₘ n))))
         where

  elimML : ∀ M → fst(P M)
  elimML (conML m∅) = P∅
  elimML (conML (unitM (inl x))) = Pη1 x
  elimML (conML (unitM (inr x))) = Pη2 λ α → elimML (x α)
  elimML (conML (x ∪ₘ y)) = P∪ (elimML (conML x)) (elimML (conML y))
  elimML (conML (ass M N O i)) = isProp→PathP (λ j → snd (P (conML (ass M N O j))))
                               ((P∪ (elimML (conML M)) (P∪ (elimML (conML N)) (elimML (conML O)))))
                               ((P∪ (P∪ (elimML (conML M)) (elimML (conML N))) (elimML (conML O)) ))
                               i
  elimML (conML (com M N i)) = isProp→PathP (λ j → snd (P (conML (com M N j)))) (P∪ (elimML (conML M)) (elimML (conML N))) (P∪ (elimML (conML N)) (elimML (conML M))) i
  elimML (conML (unitr M i)) = isProp→PathP (λ j → snd (P (conML (unitr M j)))) (P∪ (elimML (conML M)) (P∅)) (elimML (conML M)) i
  elimML (conML (trunc M N x y i j)) = isOfHLevel→isOfHLevelDep 2 (λ z → isProp→isSet (snd (P (conML z)))) (elimML (conML M)) (elimML (conML N))
                                        (cong elimML (cong conML x)) (cong elimML (cong conML y)) (trunc M N x y ) i j

--***proof that MultiLift is a set***--
-- strategy: build isomorphism, then make equivalence, then use univalence to turn equivalence into equality, then transport.

isoML :  {A : Set}{κ : Cl} → Iso (Multiset (A ⊎ (▹ κ (MultiLift A κ)))) (MultiLift A κ)
Iso.fun isoML = conML
Iso.inv isoML (conML x) = x
Iso.rightInv isoML (conML x) = refl
Iso.leftInv isoML a = refl

equivML :  {A : Set}{κ : Cl} → (Multiset (A ⊎ (▹ κ (MultiLift A κ)))) ≃ (MultiLift A κ)
equivML = isoToEquiv isoML

equalML : {A : Set}{κ : Cl} → (Multiset (A ⊎ (▹ κ (MultiLift A κ)))) ≡ (MultiLift A κ)
equalML = ua equivML

truncML : {A : Set} {κ : Cl} → isSet (MultiLift A κ)
truncML = subst⁻ isSet (sym equalML) trunc

--IsotoPath as shortcut for this bit of code

--***algebraic structure for MultiLift***--

--nowML and stepML turn MultiLift into a delay algebra structure:
nowML : {A : Set} (κ : Cl) → A → (MultiLift A κ)
nowML κ a = conML (unitM (inl a))

stepML : {A : Set} (κ : Cl) → ▹ κ (MultiLift A κ) → (MultiLift A κ)
stepML κ a = conML (unitM (inr a))

--the union is derived from the multiset union, and turns MultiLift into a monoid:
_∪ₘₗ_ : {A : Set} {κ : Cl} → (MultiLift A κ) → (MultiLift A κ) → (MultiLift A κ)
_∪ₘₗ_ {A} {κ} (conML m) (conML n) = conML (m ∪ₘ n)

--proof that this union does indeed provide a commutative monoid structure:
assoc∪ₘₗ : {A : Set} {κ : Cl} → ∀(ml nl ol : (MultiLift A κ)) → (ml ∪ₘₗ nl) ∪ₘₗ ol ≡ ml ∪ₘₗ (nl ∪ₘₗ ol)
assoc∪ₘₗ {A} {κ} (conML m) (conML n) (conML o) = cong conML (sym (ass m n o))

comm∪ₘₗ : {A : Set} {κ : Cl} → ∀(ml nl : (MultiLift A κ)) → ml ∪ₘₗ nl ≡ nl ∪ₘₗ ml
comm∪ₘₗ {A} {κ} (conML m) (conML n) = cong conML (com m n)

unitr∪ₘₗ : {A : Set} {κ : Cl} → ∀ (ml : (MultiLift A κ)) → ml ∪ₘₗ conML m∅ ≡ ml
unitr∪ₘₗ {A} {κ} (conML m) = cong conML (unitr m )

--***monadic structure for MultiLift***--

--a map function to turn MultiLift into a functor
mapML : {A B : Set} (κ : Cl) → (f : A → B) → (MultiLift A κ) → (MultiLift B κ)
mapML κ f (conML m∅) = conML m∅
mapML κ f (conML (unitM (inl x))) = conML (unitM (inl (f x)))
mapML κ f (conML (unitM (inr x))) = stepML κ (λ α → mapML κ f (x α))
mapML κ f (conML (x ∪ₘ y)) = (mapML κ f (conML x)) ∪ₘₗ (mapML κ f (conML y))
mapML κ f (conML (ass x y z i)) = sym (assoc∪ₘₗ (mapML κ f (conML x)) (mapML κ f (conML y)) (mapML κ f (conML z))) i
mapML κ f (conML (com x y i)) = comm∪ₘₗ (mapML κ f (conML x)) (mapML κ f (conML y)) i
mapML κ f (conML (unitr x i)) = unitr∪ₘₗ (mapML κ f (conML x)) i
mapML κ f (conML (trunc x y z w i i₁)) = truncML (mapML κ f (conML x)) (mapML κ f (conML y)) (\ j → mapML κ f (conML (z j))) (\ j → mapML κ f (conML (w j))) i i₁

--a bind operator to make MultiLift into a monad
bindML : {A B : Set} (κ : Cl) → (A → (MultiLift B κ)) → MultiLift A κ → MultiLift B κ
bindML κ f (conML m∅) = conML m∅
bindML κ f (conML (unitM (inl x))) = f x
bindML κ f (conML (unitM (inr x))) = stepML κ (\ α → bindML κ f (x α))
bindML κ f (conML (x ∪ₘ y)) = (bindML κ f (conML x)) ∪ₘₗ (bindML κ f (conML y))
bindML κ f (conML (ass x y z i)) = sym (assoc∪ₘₗ (bindML κ f (conML x)) (bindML κ f (conML y)) (bindML κ f (conML z))) i
bindML κ f (conML (com x y i)) = comm∪ₘₗ (bindML κ f (conML x)) (bindML κ f (conML y)) i
bindML κ f (conML (unitr x i)) = unitr∪ₘₗ (bindML κ f (conML x)) i
bindML κ f (conML (trunc x y z w i i₁)) = truncML (bindML κ f (conML x)) (bindML κ f (conML y)) (\ j → bindML κ f (conML (z j))) (\ j → bindML κ f (conML (w j))) i i₁

--bindML commutes with ∪ₘₗ
bindML-∪ₘₗ : {A B : Set} (κ : Cl) → ∀(f : A → (MultiLift B κ)) → ∀(ml nl : (MultiLift A κ)) → bindML κ f (ml ∪ₘₗ nl) ≡ (bindML κ f ml) ∪ₘₗ (bindML κ f nl)
bindML-∪ₘₗ κ f (conML x) (conML y) = refl

--***proof that MultiLift is a monad***--

--bindML and nowML need to be natural transformations
nattrans-nowML : {A B : Set} (κ : Cl) → ∀(f : A → B) → ∀(x : A) → mapML κ f (nowML κ x) ≡ nowML κ (f x)
nattrans-nowML {A}{B} κ f x = refl

-- TODO: bindML

-- bindML and nowML also need to satisfy three monad laws:
-- unit is a left-identity for bind
unitlawML1 : {A B : Set} (κ : Cl) → ∀ (f : A → (MultiLift B κ)) → ∀ (x : A) → (bindML {A} κ f (nowML κ x)) ≡ f x
unitlawML1 κ f x = refl

-- unit is a right-identity for bind
unitlawML2 : {A : Set}(κ : Cl) → ∀(x : (MultiLift A κ)) → (bindML κ (nowML κ) x) ≡ x
unitlawML2 κ x = elimML ((λ y → ((bindML κ (nowML κ) y) ≡ y)
                           , truncML (bindML κ (nowML κ) y) y))
                         refl
                         (λ y → refl)
                         (λ p → cong conML (cong unitM (cong inr (later-ext (λ β → p β)))))
                         (λ eq1 → λ eq2 → cong₂ _∪ₘₗ_ eq1 eq2)
                         x
-- bind is associative
assoclawML : {A B C : Set}(κ : Cl) → ∀(f : A → (MultiLift B κ)) → ∀ (g : B → (MultiLift C κ)) → ∀ (x : (MultiLift A κ))
                     → (bindML κ (\ y → (bindML κ g (f y))) x) ≡ (bindML κ g (bindML κ f x))
assoclawML {A} {B} {C} κ f g x = elimML ((λ z → ((bindML κ (\ y → (bindML κ g (f y))) z) ≡ (bindML κ g (bindML κ f z)))
                                           , truncML ((bindML κ (\ y → (bindML κ g (f y))) z)) (bindML κ g (bindML κ f z))))
                                        refl
                                        (λ y → refl)
                                        (λ p → cong conML (cong unitM (cong inr (later-ext (λ α → p α)))))
                                        (λ {m n} → λ eq1 → λ eq2 → (bindML κ (λ y → bindML κ g (f y)) (conML m) ∪ₘₗ
                                                           bindML κ (λ y → bindML κ g (f y)) (conML n))
                                                           ≡⟨ cong₂ (_∪ₘₗ_) eq1 eq2 ⟩
                                                           (bindML κ g (bindML κ f (conML m)) ∪ₘₗ bindML κ g (bindML κ f (conML n)))
                                                           ≡⟨ sym (bindML-∪ₘₗ κ g (bindML κ f (conML m)) (bindML κ f (conML n))) ⟩
                                                            bindML κ g (bindML κ f (conML m) ∪ₘₗ bindML κ f (conML n)) ∎)
                                        x

--*************************************************************************************--
-- Step 3: The MultiLift monad as the free delay-algebra and commutiative monoid monad --
--*************************************************************************************--

-- We already know that (MultiLift, stepML) forms a delay algebra structure,
-- and (Multilift, conML m∅ ,  ∪ₘₗ) forms a commutative monoid.
-- What we need to show is that MultiLift is the free monad with these properties.
-- That is, for a set A, and any other structure (B, δ, ε, _·_) where (B, δ) is a delay algebra and (B, ε, _·_) a commutative monoid
-- given a function f : A → B, there is a unique function MultiLift A → B extending f that preserves the algebra structures.

record IsComMonoid {A : Set} (ε : A) (_·_ : A → A → A) : Set where
  constructor iscommonoid

  field
    asso : (x y z : A) → (x · y) · z ≡ x · (y · z)
    comm : (x y : A) → (x · y) ≡ (y · x)
    uniteq : (x : A) → x · ε ≡ x

record IsDelayComMonoid {A : Set}(κ : Cl) (dm : DelayMonoidData A κ) : Set where
  constructor isdelaycommonoid

  open DelayMonoidData dm
  field
    isComMonoid : IsComMonoid (ε) (_·_)
    isDelayalg : IsDelayalg κ (nextA)

  open IsComMonoid isComMonoid public
  open IsDelayalg isDelayalg public

record IsExtendingML {A B : Set}{κ : Cl} (f : A → B) (h : (MultiLift A κ) → B) : Set where
  constructor isextendingML

  field
    extends : (x : A) → h (nowML κ x) ≡ (f x)

--foldML defines the function we are after
foldML : {A B : Set}{κ : Cl} → isSet A → isSet B → ∀ dm → IsDelayComMonoid {B} κ dm → (A → B) → (MultiLift A κ) → B
foldML setA setB (dmdata nextB ε _·_) isDMB f (conML m∅) = ε
foldML setA setB (dmdata nextB ε _·_) isDMB f (conML (unitM (inl x))) = f x
foldML setA setB dm@(dmdata nextB ε _·_) isDMB f (conML (unitM (inr x))) = nextB (λ α → foldML setA setB dm isDMB f (x α))
foldML setA setB dm@(dmdata nextB ε _·_) isDMB f (conML (x ∪ₘ y)) = (foldML setA setB dm isDMB f (conML x)) · (foldML setA setB dm isDMB f (conML y))
foldML setA setB dm@(dmdata nextB ε _·_) isDMB f (conML (ass x y z i)) = sym (IsDelayComMonoid.asso isDMB (foldML setA setB dm isDMB f (conML x))
                                                                                (foldML setA setB dm isDMB f (conML y))
                                                                                (foldML setA setB dm isDMB f (conML z))) i
foldML setA setB dm@(dmdata nextB ε _·_) isDMB f (conML (com x y i)) = IsDelayComMonoid.comm isDMB (foldML setA setB dm isDMB f (conML x)) (foldML setA setB dm isDMB f (conML y)) i
foldML setA setB dm@(dmdata nextB ε _·_) isDMB f (conML (unitr x i)) = IsDelayComMonoid.uniteq isDMB (foldML setA setB dm isDMB f (conML x)) i
foldML setA setB dm@(dmdata nextB ε _·_) isDMB f (conML (trunc x y x₁ y₁ i i₁)) = setB (foldML setA setB dm isDMB f (conML x))
                                                                                (foldML setA setB dm isDMB f (conML y))
                                                                                (λ j → (foldML setA setB dm isDMB f (conML (x₁ j))))
                                                                                (λ j → (foldML setA setB dm isDMB f (conML (y₁ j))))
                                                                                i i₁

--foldML extends the function f : A → B
foldML-extends : {A B : Set}{κ : Cl} → ∀(setA : isSet A) → ∀(setB : isSet B) → ∀ dm → ∀(isDMB : IsDelayComMonoid {B} κ dm) →
                   ∀ (f : A → B) → IsExtendingML f (foldML setA setB dm isDMB f)
IsExtendingML.extends (foldML-extends setA setB dm isDMB f) x = refl

-- or a more direct proof of the same fact:
foldML-extends-f : {A B : Set}{κ : Cl} → ∀(setA : isSet A) → ∀(setB : isSet B) → ∀ dm → ∀(isDMB : IsDelayComMonoid {B} κ dm) →
                   ∀ (f : A → B) → ∀ (x : A) → foldML setA setB dm isDMB f (nowML κ x) ≡ f x
foldML-extends-f setA setB dm isDMB f x = refl

--foldML preseves the DelayMonoid structure

module _ {A B : Set}{κ : Cl} (setA : isSet A) (setB : isSet B) (dm : _) (isDMB : IsDelayComMonoid {B} κ dm)
         (f : A → B)
 where
  open IsPreservingDM
  open DelayMonoidData dm renaming (nextA to nextB)

  foldML-preserves : IsPreservingDM {MultiLift A κ}{B} κ (dmdata (stepML κ) (conML m∅) _∪ₘₗ_) dm (foldML setA setB dm isDMB f)
  unit-preserve foldML-preserves = refl
  next-preserve foldML-preserves x = cong nextB (later-ext (λ α → refl))
  union-preserve foldML-preserves (conML x) (conML y) = refl

--and foldML is unique in doing so.
--That is, for any function h that both preserves the algebra structure
--and extends the function f : A → B,
-- h is equivalent to fold.

module _ {A B : Set} {κ : Cl} (h : MultiLift A κ → B)
                       (setA : isSet A) (setB : isSet B) (dm : _) (isDMB : IsDelayComMonoid {B} κ dm)
                       (f : A → B) (isPDM : IsPreservingDM {MultiLift A κ}{B} κ (dmdata (stepML κ) (conML m∅) _∪ₘₗ_ ) dm h)
                       (isExt : IsExtendingML f h) where

  open DelayMonoidData dm renaming (nextA to nextB)

  fold-uniquenessML : (x : (MultiLift A κ)) → h x ≡ (foldML setA setB dm isDMB f x)
  fold-uniquenessML x = elimML
                           ((λ x → (h x ≡ (foldML setA setB dm isDMB f x)) , setB (h x) ((foldML setA setB dm isDMB f x))))
                           (IsPreservingDM.unit-preserve isPDM)
                           (λ a →  h (conML (unitM (inl a)))
                                    ≡⟨ refl ⟩
                                    h (nowML κ a)
                                    ≡⟨ IsExtendingML.extends isExt a ⟩
                                    f a ∎)
                           (λ {x} → λ eq → h (conML (unitM (inr x)))
                                            ≡⟨ refl ⟩
                                            h (stepML κ x)
                                            ≡⟨ IsPreservingDM.next-preserve isPDM x ⟩
                                            nextB (λ α → h (x α))
                                            ≡⟨ cong nextB (later-ext (λ α → (eq α)))  ⟩
                                            nextB (λ α → foldML setA setB (dmdata nextB ε _·_) isDMB f (x α)) ∎)
                           (λ {x y} → λ eqx eqy → h (conML (x ∪ₘ y))
                                                   ≡⟨ refl ⟩
                                                   h ((conML x) ∪ₘₗ (conML y))
                                                   ≡⟨ IsPreservingDM.union-preserve isPDM (conML x) (conML y) ⟩
                                                   (h (conML x) · h (conML y))
                                                   ≡⟨ cong₂ _·_ eqx eqy ⟩
                                                   (foldML setA setB (dmdata nextB ε _·_) isDMB f (conML x) ·
                                                   foldML setA setB (dmdata nextB ε _·_) isDMB f (conML y)) ∎)
                           x

--****************************************************--
-- Composing Lift and Multiset via a distributive law --
--****************************************************--

--We now define a composite monad of the Multiset and Lift monads, formed via a distributive law.
LcM : (A : Set) → (κ : Cl) → Set
LcM A κ = myLift (Multiset A) κ

-- the unit of this monad is simply the composit of the units for Lift (nowL x) and Multiset (unitM)
nowLcM : {A : Set} {κ : Cl} → A → (LcM A κ)
nowLcM x = nowL (unitM x)

--LcM is a set.
truncLcM : {A : Set} {κ : Cl} → isSet (LcM A κ)
truncLcM = MyLiftSet.isSetmyLift trunc

--LLCM is a set
truncLLcM : {A : Set} {κ : Cl} → isSet (myLift (LcM A κ) κ)
truncLLcM = MyLiftSet.isSetmyLift truncLcM

-- we define a union on LcM, which will help in defining the distributive law.
_l∪m_ : {A : Set} {κ : Cl} → (LcM A κ) → (LcM A κ) → (LcM A κ)
nowL x l∪m nowL y = nowL (x ∪ₘ y)
nowL x l∪m stepL y = stepL (λ α → (nowL x l∪m (y α)))
stepL x l∪m y = stepL (λ α → ((x α) l∪m y))

--l∪m is associative, commutative, and nowL m∅ is a unit for l∪m
assoc-l∪m : {A : Set} {κ : Cl} → ∀(x y z : LcM A κ) → (x l∪m y) l∪m z ≡ x l∪m (y l∪m z)
assoc-l∪m (nowL x) (nowL y) (nowL z) = cong nowL (sym (ass x y z))
assoc-l∪m (nowL x) (nowL y) (stepL z) = cong stepL (later-ext λ α → assoc-l∪m (nowL x) (nowL y) (z α))
assoc-l∪m (nowL x) (stepL y) z = cong stepL (later-ext λ α → assoc-l∪m (nowL x) (y α) z)
assoc-l∪m (stepL x) y z = cong stepL (later-ext λ α → assoc-l∪m (x α) y z)

comm-l∪m : {A : Set} {κ : Cl} → ∀(x y : LcM A κ) → (x l∪m y) ≡ y l∪m x
comm-l∪m (nowL x) (nowL y) = cong nowL (com x y)
comm-l∪m (nowL x) (stepL y) = cong stepL (later-ext λ α → comm-l∪m (nowL x) (y α))
comm-l∪m (stepL x) (nowL y) = cong stepL (later-ext λ α → comm-l∪m (x α) (nowL y))
comm-l∪m (stepL x) (stepL y) = stepL (λ α → x α l∪m stepL y)
                                 ≡⟨ cong stepL (later-ext λ α → comm-l∪m (x α) (stepL y))  ⟩
                                 stepL (λ α → stepL y l∪m x α)
                                 ≡⟨ refl ⟩
                                 stepL (λ α → stepL (λ β → (y β) l∪m (x α)))
                                 ≡⟨ cong stepL (later-ext λ α → cong stepL (later-ext λ β → cong₂ _l∪m_ (sym (tick-irr y α β)) (tick-irr x α β) )) ⟩
                                 stepL (λ α → stepL (λ β → (y α) l∪m (x β)))
                                 ≡⟨ cong stepL (later-ext λ α → cong stepL (later-ext λ β → comm-l∪m (y α) (x β))) ⟩
                                 stepL (λ α → stepL (λ β → (x β) l∪m (y α)))
                                 ≡⟨ refl ⟩
                                 stepL (λ α → (stepL x) l∪m (y α))
                                 ≡⟨ cong stepL (later-ext λ α → comm-l∪m (stepL x) (y α)) ⟩
                                 stepL (λ α → y α l∪m stepL x) ∎

unit-l∪m : {A : Set} {κ : Cl} → ∀(x : LcM A κ) → x l∪m (nowL m∅) ≡ x
unit-l∪m (nowL x) = cong nowL (unitr x)
unit-l∪m (stepL x) = cong stepL (later-ext λ α → unit-l∪m (x α))

lemma-nowL-l∪m-mapL : {A : Set} {κ : Cl} → ∀(x : LcM A κ) → ∀(M : Multiset A) → nowL M l∪m x ≡ mapL κ (M ∪ₘ_) x
lemma-nowL-l∪m-mapL (nowL x) M = refl
lemma-nowL-l∪m-mapL (stepL x) M = cong stepL (later-ext (λ α → lemma-nowL-l∪m-mapL (x α) M))

--mapL κ f distributes over l∪m if f distributes over ∪ₘ
dist-mapL-l∪m : {A B : Set} {κ : Cl} → ∀(f : (Multiset A) → (Multiset B)) → ∀(fdist : ∀(m n : Multiset A) → f (m ∪ₘ n) ≡ f m ∪ₘ f n)
                                     → ∀(x y : (LcM A κ)) → mapL κ f (x l∪m y) ≡ (mapL κ f x) l∪m (mapL κ f y)
dist-mapL-l∪m f fdist (nowL x) (nowL y) = cong nowL (fdist x y)
dist-mapL-l∪m f fdist (nowL x) (stepL y) = cong stepL (later-ext λ α → dist-mapL-l∪m f fdist (nowL x) (y α))
dist-mapL-l∪m f fdist (stepL x) y = cong stepL (later-ext λ α → dist-mapL-l∪m f fdist (x α) y)

-- and why not, I also need a ll∪m:
_ll∪m_ : {A : Set} {κ : Cl} → (myLift (LcM A κ) κ) → (myLift (LcM A κ) κ) → (myLift (LcM A κ) κ)
nowL x ll∪m nowL y = nowL (x l∪m y)
nowL x ll∪m stepL y = stepL (λ α → (nowL x ll∪m (y α)))
stepL x ll∪m y = stepL (λ α → ((x α) ll∪m y))

assoc-ll∪m : {A : Set} {κ : Cl} → ∀(x y z : (myLift (LcM A κ) κ)) → (x ll∪m y) ll∪m z ≡ x ll∪m (y ll∪m z)
assoc-ll∪m (nowL x) (nowL y) (nowL z) = cong nowL (assoc-l∪m x y z)
assoc-ll∪m (nowL x) (nowL y) (stepL z) = cong stepL (later-ext λ α → assoc-ll∪m (nowL x) (nowL y) (z α))
assoc-ll∪m (nowL x) (stepL y) z = cong stepL (later-ext λ α → assoc-ll∪m (nowL x) (y α) z)
assoc-ll∪m (stepL x) y z = cong stepL (later-ext λ α → assoc-ll∪m (x α) y z)

unit-ll∪m : {A : Set} {κ : Cl} → ∀(x : myLift (LcM A κ) κ) → nowL (nowL m∅) ll∪m x ≡ x
unit-ll∪m (nowL x) = nowL (nowL m∅ l∪m x)
                      ≡⟨ cong nowL (comm-l∪m (nowL m∅) x) ⟩
                      nowL (x l∪m nowL m∅)
                      ≡⟨ cong nowL (unit-l∪m x) ⟩
                      nowL x ∎
unit-ll∪m (stepL x) = cong stepL (later-ext λ α → unit-ll∪m (x α))

lemma-nowL-ll∪m-mapL : {A : Set} {κ : Cl} → ∀(x : myLift (LcM A κ) κ) → ∀(M : LcM A κ) → nowL M ll∪m x ≡ mapL κ (M l∪m_) x
lemma-nowL-ll∪m-mapL (nowL x) M = refl
lemma-nowL-ll∪m-mapL (stepL x) M = cong stepL (later-ext (λ α → lemma-nowL-ll∪m-mapL (x α) M))

multL-ll∪m-l∪m : {A : Set} (κ : Cl) → ∀(x y : myLift (LcM A κ) κ) → MultL κ (x ll∪m y) ≡ MultL κ x l∪m MultL κ y
multL-ll∪m-l∪m κ (nowL x) (nowL y) = refl
multL-ll∪m-l∪m κ (nowL x) (stepL y) = stepL (λ α → MultL κ (nowL x ll∪m y α))
                                          ≡⟨ cong stepL (later-ext(λ α → multL-ll∪m-l∪m κ (nowL x) (y α) )) ⟩
                                          stepL (λ α → MultL κ (nowL x) l∪m MultL κ (y α))
                                          ≡⟨ refl ⟩
                                          stepL (λ α → x l∪m MultL κ (y α))
                                          ≡⟨ cong stepL (later-ext (λ α → comm-l∪m x (MultL κ (y α)))) ⟩
                                          (stepL (λ α → MultL κ (y α)) l∪m x)
                                          ≡⟨ refl ⟩
                                          (stepL (λ α → MultL κ (y α)) l∪m x)
                                          ≡⟨ comm-l∪m (stepL (λ α → MultL κ (y α))) x ⟩
                                          (x l∪m stepL (λ α → MultL κ (y α))) ∎
multL-ll∪m-l∪m κ (stepL x) y = cong stepL (later-ext (λ α → multL-ll∪m-l∪m κ (x α) y))

-- LcM is a monad via a distributive law, distributing Multiset over Lift.
-- Here is the distributive law:
distlawLcM : {A : Set} {κ : Cl} → Multiset (myLift A κ) → (LcM A κ)
distlawLcM m∅ = nowL m∅
distlawLcM (unitM (nowL x)) = nowL (unitM x)
distlawLcM (unitM (stepL x)) = stepL (λ α → distlawLcM (unitM (x α)))
distlawLcM (x ∪ₘ y) = (distlawLcM x) l∪m (distlawLcM y)
distlawLcM (ass x y z i) = assoc-l∪m (distlawLcM x) (distlawLcM y) (distlawLcM z) (~ i)
distlawLcM (com x y i) = comm-l∪m (distlawLcM x) (distlawLcM y) i
distlawLcM (unitr x i) = unit-l∪m (distlawLcM x) i
distlawLcM (trunc x y x₁ y₁ i i₁) = truncLcM (distlawLcM x) (distlawLcM y) (λ j → distlawLcM (x₁ j)) (λ j → distlawLcM (y₁ j)) i i₁

--proof that distlawLcM is indeed a distributive law:
--unit laws:
unitlawLcM1 : {A : Set} {κ : Cl} → ∀(x : myLift A κ) → (distlawLcM (unitM x)) ≡  mapL κ unitM x
unitlawLcM1 (nowL x) = refl
unitlawLcM1 (stepL x) = cong stepL (later-ext λ α → unitlawLcM1 (x α))

unitlawLcM2 : {A : Set} {κ : Cl} → ∀(M : Multiset A) → (distlawLcM {A}{κ} (mapM nowL M)) ≡ nowL M
unitlawLcM2 M = elimM
                 (λ N → ((distlawLcM (mapM nowL N) ≡ nowL N) , truncLcM (distlawLcM (mapM nowL N)) (nowL N)))
                 refl
                 (λ N → refl)
                 (λ {M N} → λ eqM eqN → distlawLcM (mapM nowL M) l∪m distlawLcM (mapM nowL N)
                                         ≡⟨ cong₂ (_l∪m_) eqM eqN ⟩
                                         ((nowL M) l∪m (nowL N))
                                         ≡⟨ refl ⟩
                                         nowL (M ∪ₘ N) ∎ )
                 M

--multiplication laws:
multlawLcM1 : {A : Set} (κ : Cl) → ∀(M : Multiset (Multiset (myLift A κ))) → distlawLcM (Multiset-mult M) ≡
                                                                             mapL κ Multiset-mult (distlawLcM (mapM distlawLcM M))
multlawLcM1 κ M = elimM
                    (λ N → ((distlawLcM (Multiset-mult N) ≡ mapL κ Multiset-mult (distlawLcM (mapM distlawLcM N))) ,
                     truncLcM (distlawLcM (Multiset-mult N)) (mapL κ Multiset-mult (distlawLcM (mapM distlawLcM N))) ))
                    refl
                    (λ N → distlawLcM N
                            ≡⟨ sym (mapL-identity (distlawLcM N)) ⟩
                            mapL κ (λ y → y) (distlawLcM N)
                            ≡⟨ cong₂ (mapL κ) (funExt (λ y → sym (Multiset-unitlaw1 y))) refl ⟩
                            mapL κ (λ y → Multiset-mult (unitM y)) (distlawLcM N)
                            ≡⟨ sym (mapmapL κ unitM Multiset-mult (distlawLcM N)) ⟩
                            mapL κ Multiset-mult (mapL κ unitM (distlawLcM N))
                            ≡⟨ cong (mapL κ Multiset-mult) (sym (unitlawLcM1 (distlawLcM N)))  ⟩
                            mapL κ Multiset-mult (distlawLcM (unitM (distlawLcM N))) ∎)
                    (λ {M N} → λ eqM eqN → (distlawLcM (Multiset-mult M) l∪m distlawLcM (Multiset-mult N))
                              ≡⟨ cong₂ _l∪m_ eqM eqN ⟩
                              (mapL κ Multiset-mult (distlawLcM (mapM distlawLcM M)) l∪m mapL κ Multiset-mult (distlawLcM (mapM distlawLcM N)))
                              ≡⟨ sym (dist-mapL-l∪m Multiset-mult (λ x y → refl) (distlawLcM (mapM distlawLcM M)) (distlawLcM (mapM distlawLcM N))) ⟩
                              mapL κ Multiset-mult (distlawLcM (mapM distlawLcM M) l∪m distlawLcM (mapM distlawLcM N)) ∎)
                    M

-- lemma before we can do the second multiplication law:

-- I don't know hot to split cases within elimM, so here is a lemma for the unitM case of the unitM case for the lemma-llum, split into nowL and stepL:
lemma-llum-unit-unitcase : {A : Set} (κ : Cl) → ∀(x : myLift A κ) → ∀(y : (myLift (myLift A κ) κ)) →
                                            (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) ll∪m (mapL κ distlawLcM (distlawLcM (unitM y)))
                                             ≡ mapL κ distlawLcM (distlawLcM (unitM (nowL x)) l∪m distlawLcM (unitM y))
lemma-llum-unit-unitcase κ x (nowL y) = refl
lemma-llum-unit-unitcase κ x (stepL y) = cong stepL (later-ext λ α → lemma-llum-unit-unitcase κ x (y α))

-- I don't know how to split cases within elimM, so here a lemma for the unitM case of elimM for lemma-llum, split into nowL and stepL:
lemma-llum-unitcase : {A : Set} (κ : Cl) →  ∀(x : (myLift (myLift A κ) κ))→ ∀(N : Multiset (myLift (myLift A κ) κ)) →
                                            (mapL κ distlawLcM (distlawLcM (unitM x))) ll∪m (mapL κ distlawLcM (distlawLcM N))
                                             ≡ mapL κ distlawLcM (distlawLcM (unitM x) l∪m distlawLcM N)
lemma-llum-unitcase κ (nowL x) N = elimM
                                      (λ N → ((mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) ll∪m (mapL κ distlawLcM (distlawLcM N))
                                             ≡ mapL κ distlawLcM (distlawLcM (unitM (nowL x)) l∪m distlawLcM N)) ,
                                             truncLLcM ((mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) ll∪m (mapL κ distlawLcM (distlawLcM N)))
                                                       ( mapL κ distlawLcM (distlawLcM (unitM (nowL x)) l∪m distlawLcM N)))
                                      refl
                                      (λ y → lemma-llum-unit-unitcase κ x y)
                                      (λ {M N} → λ eqM eqN → (nowL (distlawLcM (unitM x)) ll∪m mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N))
                                                              ≡⟨ lemma-nowL-ll∪m-mapL (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N)) (distlawLcM (unitM x)) ⟩
                                                              mapL κ (distlawLcM (unitM x) l∪m_) (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N))
                                                              ≡⟨ mapmapL κ distlawLcM (distlawLcM (unitM x) l∪m_) (distlawLcM M l∪m distlawLcM N) ⟩
                                                              mapL κ (λ y → distlawLcM (unitM x) l∪m distlawLcM y) (distlawLcM M l∪m distlawLcM N)
                                                              ≡⟨ refl ⟩
                                                              mapL κ (λ y → distlawLcM ((unitM x) ∪ₘ y)) (distlawLcM M l∪m distlawLcM N)
                                                              ≡⟨ sym (mapmapL κ (unitM x ∪ₘ_) distlawLcM (distlawLcM M l∪m distlawLcM N)) ⟩
                                                              mapL κ distlawLcM (mapL κ ((unitM x) ∪ₘ_) (distlawLcM M l∪m distlawLcM N))
                                                              ≡⟨ cong (mapL κ distlawLcM) (sym (lemma-nowL-l∪m-mapL (distlawLcM M l∪m distlawLcM N) (unitM x))) ⟩
                                                              mapL κ distlawLcM (nowL (unitM x) l∪m (distlawLcM M l∪m distlawLcM N)) ∎)
                                      N
lemma-llum-unitcase κ (stepL x) N = cong stepL (later-ext (λ α → lemma-llum-unitcase κ (x α) N))

lemma-llum' : {A : Set} (κ : Cl) → ∀(M N : Multiset (myLift (myLift A κ) κ)) → (mapL κ distlawLcM (distlawLcM M)) ll∪m (mapL κ distlawLcM (distlawLcM N))
                                                                               ≡ mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N)

lemma-llum' κ M = elimM
                    (λ M₁ → (( ∀ N → (mapL κ distlawLcM (distlawLcM M₁)) ll∪m (mapL κ distlawLcM (distlawLcM N)) ≡ mapL κ distlawLcM (distlawLcM M₁ l∪m distlawLcM N)) ,
                     λ x y i N → truncLLcM ((mapL κ distlawLcM (distlawLcM M₁)) ll∪m (mapL κ distlawLcM (distlawLcM N)))
                                            (mapL κ distlawLcM (distlawLcM M₁ l∪m distlawLcM N))
                                            (x N)
                                            (y N)
                                            i))
                    (λ N → ((nowL (nowL m∅) ll∪m mapL κ distlawLcM (distlawLcM N))
                      ≡⟨ unit-ll∪m (mapL κ distlawLcM (distlawLcM N)) ⟩
                      (mapL κ distlawLcM (distlawLcM N))
                      ≡⟨ cong (mapL κ distlawLcM) (sym (unit-l∪m (distlawLcM N))) ⟩
                      mapL κ distlawLcM (distlawLcM N l∪m nowL m∅)
                      ≡⟨ cong (mapL κ distlawLcM) (comm-l∪m (distlawLcM N) (nowL m∅)) ⟩
                      mapL κ distlawLcM (nowL m∅ l∪m distlawLcM N) ∎))
                    (λ x → λ N → lemma-llum-unitcase κ x N)
                    (λ {M M₁} → λ eqM eqM₁ → λ N → (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM M₁) ll∪m mapL κ distlawLcM (distlawLcM N))
                                             ≡⟨ cong (_ll∪m mapL κ distlawLcM (distlawLcM N)) (sym (eqM M₁)) ⟩
                                             (((mapL κ distlawLcM (distlawLcM M)) ll∪m (mapL κ distlawLcM (distlawLcM M₁))) ll∪m mapL κ distlawLcM (distlawLcM N))
                                             ≡⟨ assoc-ll∪m ((mapL κ distlawLcM (distlawLcM M))) ((mapL κ distlawLcM (distlawLcM M₁))) ((mapL κ distlawLcM (distlawLcM N))) ⟩
                                             ((mapL κ distlawLcM (distlawLcM M)) ll∪m ((mapL κ distlawLcM (distlawLcM M₁)) ll∪m mapL κ distlawLcM (distlawLcM N)))
                                             ≡⟨ cong (mapL κ distlawLcM (distlawLcM M) ll∪m_) (eqM₁ N) ⟩
                                             ((mapL κ distlawLcM (distlawLcM M) ll∪m mapL κ distlawLcM (distlawLcM M₁ l∪m distlawLcM N)))
                                             ≡⟨ refl ⟩
                                             (mapL κ distlawLcM (distlawLcM M) ll∪m mapL κ distlawLcM (distlawLcM (M₁ ∪ₘ N)))
                                             ≡⟨ eqM (M₁ ∪ₘ N) ⟩
                                             mapL κ distlawLcM (distlawLcM M l∪m (distlawLcM M₁ l∪m distlawLcM N))
                                             ≡⟨ cong (mapL κ distlawLcM) (sym (assoc-l∪m (distlawLcM M) (distlawLcM M₁) (distlawLcM N))) ⟩
                                             mapL κ distlawLcM ((distlawLcM M l∪m distlawLcM M₁) l∪m distlawLcM N) ∎)
                    M

-- then now the second multiplication law:

-- I don't know how to split cases within elimM, so here a lemma for the unitM case of elimM for multlawLcM2, split into nowL and stepL:
multlawLcM2-unitMcase : {A : Set} {κ : Cl} → ∀(x : (myLift (myLift A κ) κ)) →
                                      distlawLcM (mapM (MultL κ) (unitM x)) ≡ MultL κ (mapL κ distlawLcM (distlawLcM (unitM x)))
multlawLcM2-unitMcase (nowL x) = refl
multlawLcM2-unitMcase (stepL x) = cong stepL (later-ext λ α → multlawLcM2-unitMcase (x α))

-- and here the full proof of the second multiplication law:
multlawLcM2 : {A : Set} (κ : Cl) → ∀(M : Multiset (myLift (myLift A κ) κ)) →
                                     distlawLcM (mapM (MultL κ) M) ≡ MultL κ (mapL κ distlawLcM (distlawLcM M))
multlawLcM2 κ M = elimM
                   (λ N → ((distlawLcM (mapM (MultL κ) N) ≡ MultL κ (mapL κ distlawLcM (distlawLcM N))) ,
                          truncLcM (distlawLcM (mapM (MultL κ) N)) (MultL κ (mapL κ distlawLcM (distlawLcM N)))))
                   refl
                   (λ x → multlawLcM2-unitMcase x )
                   (λ {M N} → λ eqM eqN → distlawLcM (mapM (MultL κ) M) l∪m distlawLcM (mapM (MultL κ) N)
                                           ≡⟨ cong₂ (_l∪m_) eqM eqN ⟩
                                           (MultL κ (mapL κ distlawLcM (distlawLcM M)) l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
                                           ≡⟨ sym (multL-ll∪m-l∪m κ (mapL κ distlawLcM (distlawLcM M)) (mapL κ distlawLcM (distlawLcM N))) ⟩
                                           MultL κ ((mapL κ distlawLcM (distlawLcM M)) ll∪m (mapL κ distlawLcM (distlawLcM N)))
                                           ≡⟨ cong (MultL κ) (lemma-llum' κ M N) ⟩
                                           MultL κ (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N)) ∎)
                   M

--some random proofs that did not work, or work partially, that I'm not ready to through away yet:

-- lemma-llum : {A : Set} (κ : Cl) → ∀(M N : Multiset (myLift (myLift A κ) κ)) → (mapL κ distlawLcM (distlawLcM M)) ll∪m (mapL κ distlawLcM (distlawLcM N))
--                                                                                ≡ mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N)
-- lemma-llum κ m∅ N = (nowL (nowL m∅) ll∪m mapL κ distlawLcM (distlawLcM N))
--                        ≡⟨ unit-ll∪m (mapL κ distlawLcM (distlawLcM N)) ⟩
--                        (mapL κ distlawLcM (distlawLcM N))
--                        ≡⟨ cong (mapL κ distlawLcM) (sym (unit-l∪m (distlawLcM N))) ⟩
--                        mapL κ distlawLcM (distlawLcM N l∪m nowL m∅)
--                        ≡⟨ cong (mapL κ distlawLcM) (comm-l∪m (distlawLcM N) (nowL m∅)) ⟩
--                        mapL κ distlawLcM (nowL m∅ l∪m distlawLcM N) ∎
-- lemma-llum κ (unitM (nowL x)) m∅ = refl
-- lemma-llum κ (unitM (nowL x)) (unitM (nowL y)) = refl
-- lemma-llum κ (unitM (nowL x)) (unitM (stepL y)) = cong stepL (later-ext (λ α → lemma-llum κ (unitM (nowL x)) (unitM (y α))))
-- lemma-llum κ (unitM (nowL x)) (M ∪ₘ N) = (nowL (distlawLcM (unitM x)) ll∪m
--                                            mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N))
--                                            ≡⟨ lemma-nowL-ll∪m-mapL (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N)) (distlawLcM (unitM x)) ⟩
--                                            mapL κ (distlawLcM (unitM x) l∪m_) (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N))
--                                            ≡⟨ mapmapL κ distlawLcM (distlawLcM (unitM x) l∪m_) ((distlawLcM M l∪m distlawLcM N)) ⟩
--                                            mapL κ (λ y → distlawLcM (unitM x) l∪m (distlawLcM y)) (distlawLcM M l∪m distlawLcM N)
--                                            ≡⟨ cong₂ (mapL κ) (funExt (λ y → refl)) refl ⟩
--                                            mapL κ (λ y → distlawLcM ((unitM x) ∪ₘ y)) (distlawLcM M l∪m distlawLcM N)
--                                            ≡⟨ sym (mapmapL κ ((unitM x) ∪ₘ_) distlawLcM (distlawLcM M l∪m distlawLcM N)) ⟩
--                                            mapL κ distlawLcM (mapL κ ((unitM x) ∪ₘ_) (distlawLcM M l∪m distlawLcM N))
--                                            ≡⟨ cong (mapL κ distlawLcM) (sym (lemma-nowL-l∪m-mapL (distlawLcM M l∪m distlawLcM N) (unitM x))) ⟩
--                                            mapL κ distlawLcM (nowL (unitM x) l∪m (distlawLcM M l∪m distlawLcM N)) ∎
-- lemma-llum κ (unitM (nowL x)) (ass N N₁ N₂ i) = {!!}
-- lemma-llum κ (unitM (nowL x)) (com N N₁ i) = {!!}
-- lemma-llum κ (unitM (nowL x)) (unitr N i) = {!!}
-- lemma-llum κ (unitM (nowL x)) (trunc N N₁ x₁ y i i₁) = {!!}
-- lemma-llum κ (unitM (stepL x)) N = cong stepL (later-ext (λ α → lemma-llum κ (unitM (x α)) N))
-- lemma-llum κ  (M ∪ₘ M₁) N = (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM M₁) ll∪m mapL κ distlawLcM (distlawLcM N))
--                              ≡⟨ cong (_ll∪m mapL κ distlawLcM (distlawLcM N)) (sym (lemma-llum κ M M₁)) ⟩
--                              (((mapL κ distlawLcM (distlawLcM M)) ll∪m (mapL κ distlawLcM (distlawLcM M₁))) ll∪m mapL κ distlawLcM (distlawLcM N))
--                              ≡⟨ assoc-ll∪m ((mapL κ distlawLcM (distlawLcM M))) ((mapL κ distlawLcM (distlawLcM M₁))) ((mapL κ distlawLcM (distlawLcM N))) ⟩
--                              ((mapL κ distlawLcM (distlawLcM M)) ll∪m ((mapL κ distlawLcM (distlawLcM M₁)) ll∪m mapL κ distlawLcM (distlawLcM N)))
--                              ≡⟨ cong (mapL κ distlawLcM (distlawLcM M) ll∪m_) (lemma-llum κ M₁ N) ⟩
--                              ((mapL κ distlawLcM (distlawLcM M) ll∪m mapL κ distlawLcM (distlawLcM M₁ l∪m distlawLcM N)))
--                              ≡⟨ refl ⟩
--                              (mapL κ distlawLcM (distlawLcM M) ll∪m mapL κ distlawLcM (distlawLcM (M₁ ∪ₘ N)))
--                              ≡⟨ lemma-llum κ M (M₁ ∪ₘ N) ⟩
--                              mapL κ distlawLcM (distlawLcM M l∪m (distlawLcM M₁ l∪m distlawLcM N))
--                              ≡⟨ cong (mapL κ distlawLcM) (sym (assoc-l∪m (distlawLcM M) (distlawLcM M₁) (distlawLcM N))) ⟩
--                              mapL κ distlawLcM ((distlawLcM M l∪m distlawLcM M₁) l∪m distlawLcM N) ∎
-- lemma-llum κ  (ass M M₁ M₂ i) N = {!!}
-- lemma-llum κ  (com M M₁ i) N = {!!}
-- lemma-llum κ  (unitr M i) N = {!!}
-- lemma-llum κ  (trunc M M₁ x y i i₁) N = {!!}

-- -- lemma-multlawLcM2-unitMcase-unitMcase : {A : Set} (κ : Cl) → ∀(x : (myLift A κ)) → ∀(y : (myLift (myLift A κ) κ)) →
-- --                                           (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m MultL κ (mapL κ distlawLcM (distlawLcM (unitM y))))
-- --                                            ≡ MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)) l∪m distlawLcM (unitM y)))
-- -- lemma-multlawLcM2-unitMcase-unitMcase κ x (nowL y) = refl
-- -- lemma-multlawLcM2-unitMcase-unitMcase κ x (stepL y) = (distlawLcM (unitM x) l∪m
-- --                                                         stepL (λ α → MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α))))))
-- --                                                         ≡⟨ comm-l∪m (distlawLcM (unitM x))
-- --                                                                     (stepL (λ α → MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α)))))) ⟩
-- --                                                         (stepL (λ α → MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α))))) l∪m
-- --                                                          distlawLcM (unitM x))
-- --                                                         ≡⟨ refl ⟩
-- --                                                         stepL (λ α → (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α)))) l∪m
-- --                                                         distlawLcM (unitM x)))
-- --                                                         ≡⟨ cong stepL (later-ext λ α → comm-l∪m (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α)))))
-- --                                                                                (distlawLcM (unitM x)) ) ⟩
-- --                                                         stepL (λ α → (distlawLcM (unitM x) l∪m
-- --                                                         (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α)))))))
-- --                                                         ≡⟨ refl ⟩
-- --                                                         stepL (λ α → (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x))))) l∪m
-- --                                                         (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α))))))
-- --                                                         ≡⟨ cong stepL (later-ext λ α → lemma-multlawLcM2-unitMcase-unitMcase κ x (y α)) ⟩
-- --                                                         stepL (λ α → MultL κ (mapL κ distlawLcM (nowL (unitM x) l∪m distlawLcM (unitM (y α))))) ∎

-- -- lemma-multlawLcM2-unitMcase : {A : Set} (κ : Cl) → ∀(x : (myLift (myLift A κ) κ)) → ∀ (N : Multiset (myLift (myLift A κ) κ)) →
-- --                                  (MultL κ (mapL κ distlawLcM (distlawLcM (unitM x))) l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                   ≡ MultL κ (mapL κ distlawLcM (distlawLcM (unitM x) l∪m distlawLcM N))

-- -- lemma-multlawLcM2 : {A : Set} (κ : Cl) → ∀(M N : Multiset (myLift (myLift A κ) κ)) →
-- --                                  (MultL κ (mapL κ distlawLcM (distlawLcM M)) l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                   ≡ MultL κ (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N))

-- -- lemma-multlawLcM2-unitMcase κ (nowL x) N = elimM
-- --                                             (λ N → (((MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                                    ≡ (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)) l∪m distlawLcM N)))) ,
-- --                                                    truncLcM (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                                             (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)) l∪m distlawLcM N)))
-- --                                                     ))
-- --                                             refl
-- --                                             (λ y → lemma-multlawLcM2-unitMcase-unitMcase κ x y)
-- --                                             (λ {M N} → λ eqM eqN →
-- --                                                        MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m
-- --                                                        MultL κ (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N))
-- --                                                        ≡⟨ cong (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m_)
-- --                                                                         (sym (lemma-multlawLcM2 κ M N)) ⟩
-- --                                                        (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m
-- --                                                        (MultL κ (mapL κ distlawLcM (distlawLcM M)) l∪m
-- --                                                         MultL κ (mapL κ distlawLcM (distlawLcM N))))
-- --                                                        ≡⟨ sym (assoc-l∪m (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))))
-- --                                                                          (MultL κ (mapL κ distlawLcM (distlawLcM M)))
-- --                                                                          (MultL κ (mapL κ distlawLcM (distlawLcM N)))) ⟩
-- --                                                        ((MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m
-- --                                                          MultL κ (mapL κ distlawLcM (distlawLcM M))) l∪m
-- --                                                          MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                                        ≡⟨ cong (_l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                                         (lemma-multlawLcM2-unitMcase κ (nowL x) M) ⟩
-- --                                                        (MultL κ (mapL κ distlawLcM (nowL (unitM x) l∪m (distlawLcM M))) l∪m
-- --                                                         MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                                        ≡⟨ refl ⟩
-- --                                                        (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)) l∪m (distlawLcM M))) l∪m
-- --                                                         MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                                        ≡⟨ refl ⟩
-- --                                                        (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x) ∪ₘ M))) l∪m
-- --                                                         MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                                        ≡⟨ lemma-multlawLcM2 κ (unitM (nowL x) ∪ₘ M) N ⟩
-- --                                                        MultL κ (mapL κ distlawLcM ((distlawLcM (unitM (nowL x) ∪ₘ M)) l∪m distlawLcM N))
-- --                                                        ≡⟨ refl ⟩
-- --                                                        MultL κ (mapL κ distlawLcM ((nowL (unitM x) l∪m distlawLcM M) l∪m distlawLcM N))
-- --                                                        ≡⟨ cong (MultL κ) (cong (mapL κ distlawLcM)
-- --                                                                                (assoc-l∪m (nowL (unitM x)) (distlawLcM M) (distlawLcM N))) ⟩
-- --                                                        MultL κ (mapL κ distlawLcM (nowL (unitM x) l∪m (distlawLcM M l∪m distlawLcM N))) ∎)
-- --                                             N

-- -- lemma-multlawLcM2-unitMcase κ (stepL x) N = cong stepL (later-ext λ α → lemma-multlawLcM2-unitMcase κ (x α) N)

-- -- lemma-multlawLcM2 κ M N = elimM
-- --                           (λ M → ((MultL κ (mapL κ distlawLcM (distlawLcM M)) l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                   ≡ MultL κ (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N))) ,
-- --                                   truncLcM (MultL κ (mapL κ distlawLcM (distlawLcM M)) l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                             (MultL κ (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N)))  )
-- --                           (nowL m∅ l∪m MultL κ (mapL κ distlawLcM (distlawLcM N))
-- --                              ≡⟨ comm-l∪m (nowL m∅) (MultL κ (mapL κ distlawLcM (distlawLcM N))) ⟩
-- --                              (MultL κ (mapL κ distlawLcM (distlawLcM N)) l∪m nowL m∅)
-- --                              ≡⟨ unit-l∪m (MultL κ (mapL κ distlawLcM (distlawLcM N))) ⟩
-- --                              MultL κ (mapL κ distlawLcM (distlawLcM N))
-- --                              ≡⟨ cong (MultL κ) (cong (mapL κ distlawLcM) (sym (unit-l∪m (distlawLcM N)))) ⟩
-- --                              MultL κ (mapL κ distlawLcM (distlawLcM N l∪m nowL m∅ ))
-- --                              ≡⟨ cong (MultL κ) (cong (mapL κ distlawLcM) (comm-l∪m (distlawLcM N) (nowL m∅))) ⟩
-- --                              MultL κ (mapL κ distlawLcM (nowL m∅ l∪m distlawLcM N)) ∎ )
-- --                           (λ x → lemma-multlawLcM2-unitMcase κ x N )
-- --                           (λ {M₁ M₂} → λ eq1 eq2 → MultL κ (mapL κ distlawLcM (distlawLcM M₁ l∪m distlawLcM M₂)) l∪m
-- --                                                     MultL κ (mapL κ distlawLcM (distlawLcM N))
-- --                                                     ≡⟨ cong (_l∪m MultL κ (mapL κ distlawLcM (distlawLcM N))) (sym (lemma-multlawLcM2 κ M₁ M₂)) ⟩
-- --                                                     ((MultL κ (mapL κ distlawLcM (distlawLcM M₁))l∪m MultL κ (mapL κ distlawLcM (distlawLcM M₂))) l∪m
-- --                                                     MultL κ (mapL κ distlawLcM (distlawLcM N)))
-- --                                                     ≡⟨ assoc-l∪m (MultL κ (mapL κ distlawLcM (distlawLcM M₁)))
-- --                                                                  (MultL κ (mapL κ distlawLcM (distlawLcM M₂)))
-- --                                                                  (MultL κ (mapL κ distlawLcM (distlawLcM N))) ⟩
-- --                                                     (MultL κ (mapL κ distlawLcM (distlawLcM M₁))l∪m (MultL κ (mapL κ distlawLcM (distlawLcM M₂)) l∪m
-- --                                                     MultL κ (mapL κ distlawLcM (distlawLcM N))))
-- --                                                     ≡⟨ cong (MultL κ (mapL κ distlawLcM (distlawLcM M₁)) l∪m_) (lemma-multlawLcM2 κ M₂ N) ⟩
-- --                                                     (MultL κ (mapL κ distlawLcM (distlawLcM M₁)) l∪m  MultL κ (mapL κ distlawLcM (distlawLcM M₂ l∪m distlawLcM N)) )
-- --                                                     ≡⟨ cong (MultL κ (mapL κ distlawLcM (distlawLcM M₁)) l∪m_) refl ⟩
-- --                                                     (MultL κ (mapL κ distlawLcM (distlawLcM M₁)) l∪m  MultL κ (mapL κ distlawLcM (distlawLcM (M₂ ∪ₘ N))) )
-- --                                                     ≡⟨ lemma-multlawLcM2 κ M₁ ((M₂ ∪ₘ N)) ⟩
-- --                                                     MultL κ (mapL κ distlawLcM (distlawLcM M₁ l∪m (distlawLcM M₂ l∪m distlawLcM N)))
-- --                                                     ≡⟨ cong (MultL κ) (cong (mapL κ distlawLcM) (sym (assoc-l∪m (distlawLcM M₁) (distlawLcM M₂) (distlawLcM N)))) ⟩
-- --                                                     MultL κ (mapL κ distlawLcM ((distlawLcM M₁ l∪m distlawLcM M₂) l∪m distlawLcM N)) ∎)
-- --                           M
-- --

-- lemma-lum : {A : Set} (κ : Cl) → ∀(M N : Multiset (myLift (myLift A κ) κ)) →
--                                  (MultL κ (mapL κ distlawLcM (distlawLcM M)) l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
--                                   ≡ MultL κ (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N))
-- lemma-lum κ m∅ N = nowL m∅ l∪m MultL κ (mapL κ distlawLcM (distlawLcM N))
--                     ≡⟨ comm-l∪m (nowL m∅) (MultL κ (mapL κ distlawLcM (distlawLcM N))) ⟩
--                     (MultL κ (mapL κ distlawLcM (distlawLcM N)) l∪m nowL m∅)
--                     ≡⟨ unit-l∪m (MultL κ (mapL κ distlawLcM (distlawLcM N))) ⟩
--                     MultL κ (mapL κ distlawLcM (distlawLcM N))
--                     ≡⟨ cong (MultL κ) (cong (mapL κ distlawLcM) (sym (unit-l∪m (distlawLcM N)))) ⟩
--                     MultL κ (mapL κ distlawLcM (distlawLcM N l∪m nowL m∅ ))
--                     ≡⟨ cong (MultL κ) (cong (mapL κ distlawLcM) (comm-l∪m (distlawLcM N) (nowL m∅))) ⟩
--                     MultL κ (mapL κ distlawLcM (nowL m∅ l∪m distlawLcM N)) ∎
-- lemma-lum κ (unitM (nowL x)) m∅ = refl
-- lemma-lum κ (unitM (nowL x)) (unitM (nowL y)) = refl
-- lemma-lum κ (unitM (nowL x)) (unitM (stepL y)) = (distlawLcM (unitM x) l∪m
--                                                   stepL (λ α → MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α))))))
--                                                   ≡⟨ comm-l∪m (distlawLcM (unitM x))
--                                                               (stepL (λ α → MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α)))))) ⟩
--                                                   (stepL (λ α → MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α))))) l∪m
--                                                    distlawLcM (unitM x))
--                                                   ≡⟨ refl ⟩
--                                                   stepL (λ α → (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α)))) l∪m
--                                                    distlawLcM (unitM x)))
--                                                   ≡⟨ cong stepL (later-ext λ α → comm-l∪m (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α)))))
--                                                                                (distlawLcM (unitM x)) ) ⟩
--                                                   stepL (λ α → (distlawLcM (unitM x) l∪m
--                                                   (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α)))))))
--                                                   ≡⟨ refl ⟩
--                                                   stepL (λ α → (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x))))) l∪m
--                                                   (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (y α))))))
--                                                   ≡⟨ cong stepL (later-ext λ α → lemma-lum κ (unitM (nowL x)) (unitM (y α))) ⟩
--                                                   stepL (λ α → MultL κ (mapL κ distlawLcM (nowL (unitM x) l∪m distlawLcM (unitM (y α))))) ∎
-- lemma-lum κ (unitM (nowL x)) (M ∪ₘ N) = MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m
--                                                 MultL κ (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N))
--                                                 ≡⟨ cong (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m_)
--                                                         (sym (lemma-lum κ M N)) ⟩
--                                                 (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m
--                                                 (MultL κ (mapL κ distlawLcM (distlawLcM M)) l∪m
--                                                  MultL κ (mapL κ distlawLcM (distlawLcM N))))
--                                                 ≡⟨ sym (assoc-l∪m (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))))
--                                                                   (MultL κ (mapL κ distlawLcM (distlawLcM M)))
--                                                                   (MultL κ (mapL κ distlawLcM (distlawLcM N)))) ⟩
--                                                 ((MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)))) l∪m
--                                                   MultL κ (mapL κ distlawLcM (distlawLcM M))) l∪m
--                                                   MultL κ (mapL κ distlawLcM (distlawLcM N)))
--                                                 ≡⟨ cong (_l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
--                                                         (lemma-lum κ (unitM (nowL x)) M) ⟩
--                                                 (MultL κ (mapL κ distlawLcM (nowL (unitM x) l∪m (distlawLcM M))) l∪m
--                                                  MultL κ (mapL κ distlawLcM (distlawLcM N)))
--                                                 ≡⟨ refl ⟩
--                                                 (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x)) l∪m (distlawLcM M))) l∪m
--                                                  MultL κ (mapL κ distlawLcM (distlawLcM N)))
--                                                 ≡⟨ refl ⟩
--                                                 (MultL κ (mapL κ distlawLcM (distlawLcM (unitM (nowL x) ∪ₘ M))) l∪m
--                                                  MultL κ (mapL κ distlawLcM (distlawLcM N)))
--                                                 ≡⟨ {!lemma-lum κ (unitM (nowL x) ∪ₘ M) N!} ⟩
--                                                 MultL κ (mapL κ distlawLcM ((distlawLcM (unitM (nowL x) ∪ₘ M)) l∪m distlawLcM N))
--                                                 ≡⟨ refl ⟩
--                                                 MultL κ (mapL κ distlawLcM ((nowL (unitM x) l∪m distlawLcM M) l∪m distlawLcM N))
--                                                 ≡⟨ cong (MultL κ) (cong (mapL κ distlawLcM)
--                                                                         (assoc-l∪m (nowL (unitM x)) (distlawLcM M) (distlawLcM N))) ⟩
--                                                 MultL κ (mapL κ distlawLcM (nowL (unitM x) l∪m (distlawLcM M l∪m distlawLcM N))) ∎
-- lemma-lum κ (unitM (nowL x)) (ass M N O i) = isProp→PathP {!!} {!!} {!!} {!!}
-- lemma-lum κ (unitM (nowL x)) (com M N i) = {!!}
-- lemma-lum κ (unitM (nowL x)) (unitr N i) = {!!}
-- lemma-lum κ (unitM (nowL x)) (trunc M N y z i i₁) = {!!}
-- lemma-lum κ (unitM (stepL x)) N = cong stepL (later-ext λ α → lemma-lum κ (unitM (x α)) N  )
-- lemma-lum κ (M₁ ∪ₘ M₂) N =  MultL κ (mapL κ distlawLcM (distlawLcM M₁ l∪m distlawLcM M₂)) l∪m
--                             MultL κ (mapL κ distlawLcM (distlawLcM N))
--                            ≡⟨ cong (_l∪m MultL κ (mapL κ distlawLcM (distlawLcM N))) (sym (lemma-lum κ M₁ M₂)) ⟩
--                            ((MultL κ (mapL κ distlawLcM (distlawLcM M₁))l∪m MultL κ (mapL κ distlawLcM (distlawLcM M₂))) l∪m
--                              MultL κ (mapL κ distlawLcM (distlawLcM N)))
--                            ≡⟨ assoc-l∪m (MultL κ (mapL κ distlawLcM (distlawLcM M₁)))
--                                         (MultL κ (mapL κ distlawLcM (distlawLcM M₂)))
--                                         (MultL κ (mapL κ distlawLcM (distlawLcM N))) ⟩
--                            (MultL κ (mapL κ distlawLcM (distlawLcM M₁))l∪m (MultL κ (mapL κ distlawLcM (distlawLcM M₂)) l∪m
--                             MultL κ (mapL κ distlawLcM (distlawLcM N))))
--                            ≡⟨ cong (MultL κ (mapL κ distlawLcM (distlawLcM M₁)) l∪m_) (lemma-lum κ M₂ N) ⟩
--                            (MultL κ (mapL κ distlawLcM (distlawLcM M₁)) l∪m  MultL κ (mapL κ distlawLcM (distlawLcM M₂ l∪m distlawLcM N)) )
--                            ≡⟨ cong (MultL κ (mapL κ distlawLcM (distlawLcM M₁)) l∪m_) refl ⟩
--                            (MultL κ (mapL κ distlawLcM (distlawLcM M₁)) l∪m  MultL κ (mapL κ distlawLcM (distlawLcM (M₂ ∪ₘ N))) )
--                            ≡⟨ lemma-lum κ M₁ ((M₂ ∪ₘ N)) ⟩
--                            MultL κ (mapL κ distlawLcM (distlawLcM M₁ l∪m (distlawLcM M₂ l∪m distlawLcM N)))
--                            ≡⟨ cong (MultL κ) (cong (mapL κ distlawLcM) (sym (assoc-l∪m (distlawLcM M₁) (distlawLcM M₂) (distlawLcM N)))) ⟩
--                            MultL κ (mapL κ distlawLcM ((distlawLcM M₁ l∪m distlawLcM M₂) l∪m distlawLcM N)) ∎
-- lemma-lum κ (ass M M₁ M₂ i) N = isProp→PathP (λ j → {!!}) (lemma-lum κ ((M ∪ₘ M₁) ∪ₘ M₂) N) (lemma-lum κ (M ∪ₘ (M₁ ∪ₘ M₂)) N) i
-- lemma-lum κ (com M M₁ i) N = λ j → comm-l∪m {!!} {!!} i
-- lemma-lum κ (unitr M i) N = λ j → {!!}
-- lemma-lum κ (trunc M M₁ x y i i₁) N = {!!}

-- --λ j → unitr (Multiset-unitlaw2 M j) i

-- -- I don't know how to split cases within elimM, so here a lemma for the unitM case of elimM for multlawLcM2, split into nowL and stepL:
-- multlawLcM2-unitMcase : {A : Set} {κ : Cl} → ∀(x : (myLift (myLift A κ) κ)) →
--                                      distlawLcM (mapM (MultL κ) (unitM x)) ≡ MultL κ (mapL κ distlawLcM (distlawLcM (unitM x)))
-- multlawLcM2-unitMcase (nowL x) = refl
-- multlawLcM2-unitMcase (stepL x) = cong stepL (later-ext λ α → multlawLcM2-unitMcase (x α))

-- -- and here the full proof of the second multiplication law:
-- multlawLcM2 : {A : Set} (κ : Cl) → ∀(M : Multiset (myLift (myLift A κ) κ)) →
--                                      distlawLcM (mapM (MultL κ) M) ≡ MultL κ (mapL κ distlawLcM (distlawLcM M))
-- multlawLcM2 κ M = elimM
--                    (λ N → ((distlawLcM (mapM (MultL κ) N) ≡ MultL κ (mapL κ distlawLcM (distlawLcM N))) ,
--                           truncLcM (distlawLcM (mapM (MultL κ) N)) (MultL κ (mapL κ distlawLcM (distlawLcM N)))))
--                    refl
--                    (λ x → multlawLcM2-unitMcase x )
--                    (λ {M N} → λ eqM eqN → distlawLcM (mapM (MultL κ) M) l∪m distlawLcM (mapM (MultL κ) N)
--                                            ≡⟨ cong₂ (_l∪m_) eqM eqN ⟩
--                                            (MultL κ (mapL κ distlawLcM (distlawLcM M)) l∪m MultL κ (mapL κ distlawLcM (distlawLcM N)))
--                                            ≡⟨ lemma-lum κ M N ⟩
--                                            MultL κ (mapL κ distlawLcM (distlawLcM M l∪m distlawLcM N)) ∎)
--                    M

max_stars_repo_name: maaikezwart/Agda-proofs

max_issues_repo_name: maaikezwart/Agda-proofs

max_forks_repo_name: maaikezwart/Agda-proofs


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

open import Relation.Binary.Core

module Magma.Definitions
  {a ℓ} {A : Set a}   -- The underlying set
  (_≈_ : Rel A ℓ)     -- The underlying equality
  where

open import Algebra.Core
open import Data.Product

Alternativeˡ : Op₂ A → Set _
Alternativeˡ _∙_ = ∀ x y  →  ((x ∙ x) ∙ y) ≈ (x ∙ (y ∙ y))

Alternativeʳ : Op₂ A → Set _
Alternativeʳ _∙_ = ∀ x y → (x ∙ (y ∙ y)) ≈ ((x ∙ y) ∙ y)

Alternative : Op₂ A → Set _
Alternative _∙_ = (Alternativeˡ _∙_ ) × ( Alternativeʳ _∙_)

Flexible : Op₂ A → Set _
Flexible _∙_ = ∀ x y → ((x ∙ y) ∙ x) ≈ (x ∙ (y ∙ x))

Medial : Op₂ A → Set _
Medial _∙_ = ∀ x y u z → ((x ∙ y) ∙ (u ∙ z)) ≈ ((x ∙ u) ∙ (y ∙ z))

LeftSemimedial : Op₂ A → Set _
LeftSemimedial _∙_ = ∀ x y z → ((x ∙ x) ∙ (y ∙ z)) ≈ ((x ∙ y) ∙ (x ∙ z))

RightSemimedial : Op₂ A → Set _
RightSemimedial _∙_ = ∀ x y z → ((y ∙ z) ∙ (x ∙ x)) ≈ ((y ∙ x) ∙ (z ∙ x))

Semimedial : Op₂ A → Set _
Semimedial _∙_ = (LeftSemimedial _∙_) × (RightSemimedial _∙_)


text:
module Luau.Type.FromJSON where

open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)

open import Agda.Builtin.List using (List; _∷_; [])

open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
open import FFI.Data.Bool using (true; false)
open import FFI.Data.Either using (Either; Left; Right)
open import FFI.Data.Maybe using (Maybe; nothing; just)
open import FFI.Data.String using (String; _++_)
open import FFI.Data.Vector using (head; tail; null; empty)

name = fromString "name"
type = fromString "type"
argTypes = fromString "argTypes"
returnTypes = fromString "returnTypes"
types = fromString "types"

{-# TERMINATING #-}
typeFromJSON : Value → Either String Type
compoundFromArray : (Type → Type → Type) → Array → Either String Type

typeFromJSON (object o) with lookup type o
typeFromJSON (object o) | just (string "AstTypeFunction") with lookup argTypes o | lookup returnTypes o
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) with lookup types argsSet | lookup types retsSet
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) with head args | head rets
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue with typeFromJSON argValue | typeFromJSON retValue
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue | Right arg | Right ret = Right (arg ⇒ ret)
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue | Left err | _ = Left err
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | just argValue | just retValue | _ | Left err = Left err
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | _ | nothing = Left "No return type"
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just (array args) | just (array rets) | nothing | _ = Left "No argument type"
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | just _ | _ = Left "argTypes.types is not an array"
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | _ | just _ = Left "retTypes.types is not an array"
typeFromJSON (object o) | just (string "AstTypeFunction") | just (object argsSet) | just (object retsSet) | nothing | _ = Left "argTypes.types does not exist"
typeFromJSON (object o) | just (string "AstTypeFunction") | _ | just _ = Left "argTypes is not an object"
typeFromJSON (object o) | just (string "AstTypeFunction") | just _ | _ = Left "returnTypes is not an object"
typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing = Left "Missing argTypes and returnTypes"

typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right any
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "number") = Right number
typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"

typeFromJSON (object o) | just (string "AstTypeUnion") with lookup types o
typeFromJSON (object o) | just (string "AstTypeUnion") | just (array types) = compoundFromArray _∪_ types
typeFromJSON (object o) | just (string "AstTypeUnion") | _ = Left "`types` field must be an array"

typeFromJSON (object o) | just (string "AstTypeIntersection") with lookup types o
typeFromJSON (object o) | just (string "AstTypeIntersection") | just (array types) = compoundFromArray _∩_ types
typeFromJSON (object o) | just (string "AstTypeIntersection") | _ = Left "`types` field must be an array"

typeFromJSON (object o) | just (string ty) = Left ("Unsupported type " ++ ty)
typeFromJSON (object o) | just _ = Left "`type` field must be a string"
typeFromJSON (object o) | nothing = Left "No `type` field"
typeFromJSON _ = Left "Unsupported JSON type"

compoundFromArray ctor ts with head ts | tail ts
compoundFromArray ctor ts | just hd | tl with null tl
compoundFromArray ctor ts | just hd | tl | true = typeFromJSON hd
compoundFromArray ctor ts | just hd | tl | false with typeFromJSON hd | compoundFromArray ctor tl
compoundFromArray ctor ts | just hd | tl | false | Right hdTy | Right tlTy = Right (ctor hdTy tlTy)
compoundFromArray ctor ts | just hd | tl | false | Left err | _ = Left err
compoundFromArray ctor ts | just hd | tl | false | _ | Left Err = Left Err
compoundFromArray ctor ts | nothing | empty = Left "Empty types array?"


text:
-- Andreas, 2015-05-06 issue reported by Jesper Cockx

{-# OPTIONS --copatterns #-}

record Foo (A : Set) : Set where
  field
    foo : A

open Foo {{...}} public

record ⊤ : Set where

instance
  Foo⊤ : Foo ⊤
  foo Foo⊤ = {!!}
  -- foo {{Foo⊤}} = {!!}

-- Error WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Rules/LHS/Split.hs:103

-- Better error:
-- Not a valid projection for a copattern: foo
-- when checking that the clause foo Foo⊤ = ? has type Foo ⊤


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Vec.DepVec where

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

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Vec

open import Cubical.Relation.Nullary

open Iso

private
  variable
    ℓ : Level

data depVec (G : (n : ℕ) → Type ℓ) : ℕ → Type ℓ where
  ⋆   : depVec G 0
  _□_ : {n : ℕ} → (a : G n) → (v : depVec G n) → depVec G (suc n)

module depVecPath (G : (n : ℕ) → Type ℓ)
  where

  code : {n : ℕ} → (v v' : depVec G n) → Type ℓ
  code ⋆ ⋆ = Unit*
  code (a □ v) (a' □ v') = (a ≡ a') × (v ≡ v')

  -- encode
  reflEncode : {n : ℕ} → (v : depVec G n) → code v v
  reflEncode ⋆ = tt*
  reflEncode (a □ v) = refl , refl

  encode : {n : ℕ} → (v v' : depVec G n) → (v ≡ v') → code v v'
  encode v v' p = J (λ v' _ → code v v') (reflEncode v) p

  encodeRefl : {n : ℕ} → (v : depVec G n) → encode v v refl ≡ reflEncode v
  encodeRefl v = JRefl (λ v' _ → code v v') (reflEncode v)

  -- decode
  decode : {n : ℕ} → (v v' : depVec G n) → (r : code v v') → (v ≡ v')
  decode ⋆ ⋆ _ = refl
  decode (a □ v) (a' □ v') (p , q) = cong₂ _□_ p q

  decodeRefl : {n : ℕ} → (v : depVec G n) → decode v v (reflEncode v) ≡ refl
  decodeRefl ⋆ = refl
  decodeRefl (a □ v) = refl

  -- equiv
  ≡Vec≃codeVec : {n : ℕ} → (v v' : depVec G n) → (v ≡ v') ≃ (code v v')
  ≡Vec≃codeVec v v' = isoToEquiv is
    where
    is : Iso (v ≡ v') (code v v')
    fun is = encode v v'
    inv is = decode v v'
    rightInv is = sect v v'
      where
      sect : {n : ℕ} → (v v' : depVec G n) → (r : code v v')
             → encode v v' (decode v v' r) ≡ r
      sect ⋆ ⋆ tt* = encodeRefl ⋆
      sect (a □ v) (a' □ v') (p , q) = J (λ a' p → encode (a □ v) (a' □ v') (decode (a □ v) (a' □ v') (p , q)) ≡ (p , q))
                                       (J (λ v' q → encode (a □ v) (a □ v') (decode (a □ v) (a □ v') (refl , q)) ≡ (refl , q))
                                       (encodeRefl (a □ v)) q) p
    leftInv is = retr v v'
      where
      retr : {n : ℕ} → (v v' : depVec G n) → (p : v ≡ v')
             → decode v v' (encode v v' p) ≡ p
      retr v v' p = J (λ v' p → decode v v' (encode v v' p) ≡ p)
                    (cong (decode v v) (encodeRefl v) ∙ decodeRefl v) p

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS -v tc.record.eta:20 -v tc.eta:100  -v tc.constr:50 #-}

-- Andreas, 2013-05-15 reported by nomeata

module Issue846 where

open import Issue846.Imports

opt-is-opt2 : ∀ n s → n mod 7 ≡ 1' → winner n s opt ≡ false
opt-is-opt2 0 s ()
opt-is-opt2 (suc n) s eq =
  let (pick k 1≤k k≤6) = s (suc n)
  in
    cong not (opt-is-opt (suc n ∸ k) s (lem-sub-p n k eq {!1≤k!} {!!} ))

-- The problem here was that the first hole was solved by
-- 'nonEmpty' by the instance finder,
-- which is called since the first hole is an unused argument.
-- 'nonEmpty' of course does not fit, but the instance finder
-- did not see it and produced constraints.
-- The eta-contractor broke on something ill-typed.

-- Now, the instance finder is a bit smarter due to
-- improved equality checking for dependent function types.
-- Unequal domains now do not block comparison of
-- codomains, only block the domain type.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module DecidableOrder where

open import Logic.Relations
open import Logic.Identity using (_≡_)

open module Antisym = PolyEq _≡_ using (Antisymmetric)

record DecidableOrder (A : Set) : Set1 where
  field
    _≤_     : Rel A
    refl    : Reflexive _≤_
    antisym : Antisymmetric _≤_
    trans   : Transitive _≤_
    total   : Total _≤_
    decide  : forall x y -> Decidable (x ≤ y)

  infix 80 _≤_ _≥_

  _≥_ = \(x y : A) -> y ≤ x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties, related to products, that rely on the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Product.Properties.WithK where

open import Data.Bool.Base
open import Data.Product
open import Data.Product.Properties using (,-injectiveˡ)
open import Function
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Reflects
open import Relation.Nullary using (Dec; _because_; yes; no)
open import Relation.Nullary.Decidable using (map′)

------------------------------------------------------------------------
-- Equality

module _ {a b} {A : Set a} {B : Set b} where

  ,-injective : ∀ {a c : A} {b d : B} → (a , b) ≡ (c , d) → a ≡ c × b ≡ d
  ,-injective refl = refl , refl

module _ {a b} {A : Set a} {B : A → Set b} where

  ,-injectiveʳ : ∀ {a} {b c : B a} → (Σ A B ∋ (a , b)) ≡ (a , c) → b ≡ c
  ,-injectiveʳ refl = refl

  -- Note: this is not an instance of `_×-dec_`, because we need `x` and `y`
  -- to have the same type before we can test them for equality.
  ≡-dec : Decidable _≡_ → (∀ {a} → Decidable {A = B a} _≡_) →
          Decidable {A = Σ A B} _≡_
  ≡-dec dec₁ dec₂ (a , x) (b , y) with dec₁ a b
  ... | false because [a≢b] = no (invert [a≢b] ∘ ,-injectiveˡ)
  ... | yes refl = map′ (cong (a ,_)) ,-injectiveʳ (dec₂ x y)


text:
-- Andreas, 2022-06-14, issue #5953 reported by Szumi Xi
-- Cubical Agda switches dot-pattern termination off (#4606).
-- However, this breaks also some benign cases.
--
-- In this example with inductive-inductive types,
-- dotted variables should still be recognized
-- as variable patterns for termination certification.

{-# OPTIONS --cubical #-}  -- worked with --without-K but not --cubical

-- Debugging:
-- {-# OPTIONS -v term.check.clause:25 #-}
-- {-# OPTIONS -v term:20 #-}

data Con : Set
data Ty : Con → Set

data Con where
  nil : Con
  ext : (Γ : Con) → Ty Γ → Con

data Ty where
  univ : (Γ : Con) → Ty Γ
  pi : (Γ : Con) (A : Ty Γ) → Ty (ext Γ A) → Ty Γ

module _
  (A : Set)
  (B : A → Set)
  (n : A)
  (e : (a : A) → B a → A)
  (u : (a : A) → B a)
  (p : (a : A) (b : B a) → B (e a b) → B a)
  where
  recCon : Con → A
  recTy : (Γ : Con) → Ty Γ → B (recCon Γ)

  recCon nil = n
  recCon (ext Γ A) = e (recCon Γ) (recTy Γ A)

  recTy Γ (univ Γ) = u (recCon Γ)
  recTy Γ (pi Γ A B) = p (recCon Γ) (recTy Γ A) (recTy (ext Γ A) B)

-- Should pass the termination checker.


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts

module htype-decidable where
  arr-lemma : ∀{t1 t2 t3 t4} → t1 ==> t2 == t3 ==> t4 → t1 == t3 × t2 == t4
  arr-lemma refl = refl , refl

  sum-lemma : ∀{t1 t2 t3 t4} → t1 ⊕ t2 == t3 ⊕ t4 → t1 == t3 × t2 == t4
  sum-lemma refl = refl , refl

  prod-lemma : ∀{t1 t2 t3 t4} → t1 ⊠ t2 == t3 ⊠ t4 → t1 == t3 × t2 == t4
  prod-lemma refl = refl , refl

  htype-dec : (t1 t2 : htyp) → t1 == t2 + (t1 == t2 → ⊥)
  htype-dec num num = Inl refl
  htype-dec num ⦇-⦈ = Inr (λ ())
  htype-dec num (t1 ==> t2) = Inr (λ ())
  htype-dec num (t1 ⊕ t2) = Inr (λ ())
  htype-dec ⦇-⦈ num = Inr (λ ())
  htype-dec ⦇-⦈ ⦇-⦈ = Inl refl
  htype-dec ⦇-⦈ (t1 ==> t2) = Inr (λ ())
  htype-dec ⦇-⦈ (t1 ⊕ t2) = Inr (λ ())
  htype-dec (t1 ==> t2) num = Inr (λ ())
  htype-dec (t1 ==> t2) ⦇-⦈ = Inr (λ ())
  htype-dec (t1 ==> t2) (t3 ==> t4)
    with htype-dec t1 t3 | htype-dec t2 t4
  ... | Inl refl | Inl refl = Inl refl
  ... | Inl refl | Inr x₁   = Inr (λ x → x₁ (π2 (arr-lemma x)))
  ... | Inr x    | Inl refl = Inr (λ x₁ → x (π1 (arr-lemma x₁)))
  ... | Inr x    | Inr x₁   = Inr (λ x₂ → x (π1 (arr-lemma x₂)))
  htype-dec (t1 ==> t2) (t3 ⊕ t4) = Inr (λ ())
  htype-dec (t1 ⊕ t2) num = Inr (λ ())
  htype-dec (t1 ⊕ t2) ⦇-⦈ = Inr (λ ())
  htype-dec (t1 ⊕ t2) (t3 ==> t4) = Inr (λ ())
  htype-dec (t1 ⊕ t2) (t3 ⊕ t4)
    with htype-dec t1 t3 | htype-dec t2 t4
  ... | Inl refl | Inl refl = Inl refl
  ... | Inl refl | Inr x₁   = Inr (λ x → x₁ (π2 (sum-lemma x)))
  ... | Inr x    | Inl refl = Inr (λ x₁ → x (π1 (sum-lemma x₁)))
  ... | Inr x    | Inr x₁   = Inr (λ x₂ → x (π1 (sum-lemma x₂)))
  htype-dec num (t3 ⊠ t4) = Inr (λ ())
  htype-dec ⦇-⦈ (t3 ⊠ t4) = Inr (λ ())
  htype-dec (t1 ==> t2) (t3 ⊠ t4) = Inr (λ ())
  htype-dec (t1 ⊕ t2) (t3 ⊠ t4) = Inr (λ ())
  htype-dec (t1 ⊠ t2) num = Inr (λ ())
  htype-dec (t1 ⊠ t2) ⦇-⦈ = Inr (λ ())
  htype-dec (t1 ⊠ t2) (t3 ==> t4) = Inr (λ ())
  htype-dec (t1 ⊠ t2) (t3 ⊕ t4) = Inr (λ ())
  htype-dec (t1 ⊠ t2) (t3 ⊠ t4)
    with htype-dec t1 t3 | htype-dec t2 t4
  ... | Inl refl | Inl refl = Inl refl
  ... | Inl refl | Inr x₁   = Inr (λ x → x₁ (π2 (prod-lemma x)))
  ... | Inr x    | Inl refl = Inr (λ x₁ → x (π1 (prod-lemma x₁)))
  ... | Inr x    | Inr x₁   = Inr (λ x₂ → x (π1 (prod-lemma x₂)))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Sets.PredicateSet.Filter {ℓₒ} {ℓₒₗ} where

import      Lvl
open import Functional
open import Logic.Propositional
-- open import Sets.PredicateSet
open import Type{ℓₒ Lvl.⊔ ℓₒₗ}

-- An element in Filter(T) is in the subset of T.
-- Something of type Filter(T) is of a restricted part of T.
-- Note: The level of Stmt inside P is lower than Type.
-- TODO: Is this the same as (⊤ ∩ P) in "Sets.PredicateSet"?
record Filter {T : Type} (P : T → Stmt{ℓₒₗ}) : Type where
  constructor subelem
  field
    elem             : T
    ⦃ satisfaction ⦄ : P(elem)

-- postulate nested-subset : ∀{T}{φ₁}{φ₂} → (Tₛ₁ : Filter{T}(φ₁)) → (Tₛ₂ : Filter{Filter{T}(φ₁)}(φ₂)) → Filter{T}(x ↦ φ₁(x) ∧ φ₂(subelem (x) ⦃ ⦄))
-- postulate nested-subset : ∀{T}{φ₁}{φ₂} → (Tₛ₁ : Filter{T}(φ₁)) → (Tₛ₂ : Filter{Filter{T}(φ₁)}(φ₂ ∘ Filter.elem)) → Filter{T}(x ↦ φ₁(x) ∧ φ₂(x))
-- postulate nested-subset : ∀{T}{φ₁}{φ₂} → (Filter{Filter{T}(φ₁)}(φ₂ ∘ Filter.elem) ≡ Filter{T}(x ↦ φ₁(x) ∧ φ₂(x)))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- "Equational" reasoning combinator setup
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Labelled-transition-system

module Bisimilarity.Weak.Alternative.Equational-reasoning-instances
         {ℓ} {lts : LTS ℓ} where

open import Prelude

open import Bisimilarity lts
import Bisimilarity.Equational-reasoning-instances
open import Bisimilarity.Weak.Alternative lts
open import Equational-reasoning

instance

  trans∼≈ : ∀ {i} → Transitive _∼_ [ i ]_≈_
  trans∼≈ = is-transitive (transitive {a = ℓ} ∘ ∼⇒≈)

  trans∼′≈ : ∀ {i} → Transitive _∼′_ [ i ]_≈_
  trans∼′≈ = is-transitive (transitive {a = ℓ} ∘ ∼⇒≈″)

  trans∼′≈′ : ∀ {i} → Transitive _∼′_ [ i ]_≈′_
  trans∼′≈′ = is-transitive (transitive {a = ℓ} ∘ ∼⇒≈″)

  trans∼≈′ : ∀ {i} → Transitive _∼_ [ i ]_≈′_
  trans∼≈′ {i} = is-transitive (transitive {a = ℓ} ∘ ∼⇒≈ {i})

  convert∼≈ : Convertible _∼_ _≈_
  convert∼≈ = is-convertible ∼⇒≈

  convert∼′≈ : Convertible _∼′_ _≈_
  convert∼′≈ = is-convertible (convert {a = ℓ} ∘ ∼⇒≈″)

  convert∼≈′ : Convertible _∼_ _≈′_
  convert∼≈′ = is-convertible ∼⇒≈′

  convert∼′≈′ : Convertible _∼′_ _≈′_
  convert∼′≈′ = is-convertible ∼⇒≈″

open Bisimilarity.Equational-reasoning-instances
       {lts = weak lts} public

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module monad where

open import eq

open import functor
open import functions

record Triple (T : Set → Set) : Set₁ where
  constructor MkTriple
  field
    η : ∀{A : Set} → A → T A
    μ : ∀{A : Set} → T (T A) → T A
    η-inv : ∀{A : Set} → T A → A

    -- triple-func : Functor T
    -- triple-assoc : ∀{A : Set} → μ {A} ∘ (fmap triple-func μ) ≡ (μ ∘ μ)
    -- triple-id₁ : ∀{A : Set} → μ ∘ η {T A} ≡ id
    -- triple-id₂ : ∀{A : Set} → (μ {A} ∘ fmap triple-func (η {A})) ≡ id

record Monad (M : Set → Set) : Set₁ where
  constructor MkMonad
  field
    return : ∀{A : Set} → A → M A
    bind : ∀{A B : Set} → M A → (A → M B) → M B

    -- monad-funct : Functor M

    -- monad-left-id : ∀{A B : Set}{a : A}{f : A → M B}
    --   → bind (return a) f ≡ f a

    -- monad-right-id : ∀{A : Set}{c : M A}
    --   → bind c return ≡ c

    -- monad-assoc : ∀{A B C : Set}{c : M A}{f : A → M B}{g : B → M C}
    --   → bind (bind c f) g ≡ bind c (λ a → bind (f a) g)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; trans ; cong )

open import AssocFree.DList using ( List )
open import AssocFree.DNat using ( ℕ )

module AssocFree.STLambdaC.Typ (TConst : Set) where

infixr 2 _⇝_

data Typ : Set where
  const : TConst → Typ
  _⇝_ : Typ → Typ → Typ

Var : Set
Var = ℕ

Ctxt : Set
Ctxt = List Typ

open AssocFree.DList public using
  ( [] ; [_] ; _++_ ; _∷_ ; _∈_ ; _≪_ ; _≫_ ; _⋙_ ; uniq ; singleton
  ; Case ; case ; inj₁ ; inj₂ ; inj₃ ; case-≪ ; case-≫ ; case-⋙
  ; Case₃ ; case₃ ; caseˡ ; caseʳ ; caseˡ₃ ; caseʳ₃ ; case⁻¹ ; case-iso )

max_stars_repo_name: agda/agda-assoc-free

max_issues_repo_name: agda/agda-assoc-free

max_forks_repo_name: agda/agda-assoc-free


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.Semilattice {l₁ l₂} (L : Semilattice l₁ l₂) where

open Semilattice L
open import Algebra.Structures
open import Relation.Binary
import Relation.Binary.Construct.NaturalOrder.Left as LeftNaturalOrder
import Relation.Binary.Lattice as R
import Relation.Binary.Properties.Poset as R
open import Relation.Binary.EqReasoning setoid
open import Function
open import Data.Product

------------------------------------------------------------------------
-- Every semilattice can be turned into a poset via the left natural
-- order.

poset : Poset _ _ _
poset = LeftNaturalOrder.poset _≈_ _∧_ isSemilattice

open Poset poset using (_≤_; isPartialOrder)

------------------------------------------------------------------------
-- Every algebraic semilattice can be turned into an order-theoretic one.

isOrderTheoreticMeetSemilattice : R.IsMeetSemilattice _≈_ _≤_ _∧_
isOrderTheoreticMeetSemilattice = record
  { isPartialOrder = isPartialOrder
  ; infimum        = LeftNaturalOrder.infimum _≈_ _∧_ isSemilattice
  }

orderTheoreticMeetSemilattice : R.MeetSemilattice _ _ _
orderTheoreticMeetSemilattice = record
  { isMeetSemilattice = isOrderTheoreticMeetSemilattice }

isOrderTheoreticJoinSemilattice : R.IsJoinSemilattice _≈_ (flip _≤_) _∧_
isOrderTheoreticJoinSemilattice = record
  { isPartialOrder = R.invIsPartialOrder poset
  ; supremum       = R.IsMeetSemilattice.infimum
                       isOrderTheoreticMeetSemilattice
  }

orderTheoreticJoinSemilattice : R.JoinSemilattice _ _ _
orderTheoreticJoinSemilattice = record
  { isJoinSemilattice = isOrderTheoreticJoinSemilattice }