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

syntax Lens | L

type
  S : 0-ary
  A : 0-ary

term
  get : S  ->  A
  put : S  A  ->  S

theory
  (PG) s : S  a : A   |> get (put (s, a))   = a
  (GP) s : S          |> put (s, get(s))    = s
  (PP) s : S  a b : A |> put (put(s, a), b) = put (s, a)
-}

module Lens.Equality where

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

open import Lens.Signature
open import Lens.Syntax

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

private
  variable
    α β γ τ : LT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ L) α Γ → (𝔐 ▷ L) α Γ → Set where
  PG : ⁅ S ⁆ ⁅ A ⁆̣       ▹ ∅ ⊢   get (put 𝔞 𝔟) ≋ₐ 𝔟
  GP : ⁅ S ⁆̣             ▹ ∅ ⊢   put 𝔞 (get 𝔞) ≋ₐ 𝔞
  PP : ⁅ S ⁆ ⁅ A ⁆ ⁅ A ⁆̣ ▹ ∅ ⊢ put (put 𝔞 𝔟) 𝔠 ≋ₐ put 𝔞 𝔟

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

ext: agda

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Homomorphism (Σ : Signature) where

open import Fragment.Algebra.Homomorphism.Base Σ public
open import Fragment.Algebra.Homomorphism.Definitions Σ public
open import Fragment.Algebra.Homomorphism.Properties Σ public
open import Fragment.Algebra.Homomorphism.Setoid Σ public
open import Fragment.Algebra.Homomorphism.Equivalence Σ public

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module sv20.exam1 where

open import Data.Product using (∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function.Base using (_∘_)

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

-- An idiom that makes things slightly more readable (sometimes)
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

-- Exam starts from here:

-- 1.

first : ∀ {Object : Set} {P Q : Object → Set}
      → (∃[ x ] (P x ⊎ Q x)) ⇔ (∃[ x ] (P x) ⊎ ∃[ x ] (Q x))
-- We prove each side separately of the bijection separately. If we are able to
-- prove both ways, we will have proved the bijection
first =
    record { to = to ; from = from }
  where
  -- First, we prove that (∃[ x ] (P x ⊎ Q x)) → (∃[ x ] (P x) ⊎ ∃[ x ] (Q x))
  to : ∀ {Object : Set} {P Q : Object → Set}
     → (∃[ x ] (P x ⊎ Q x)) → (∃[ x ] (P x) ⊎ ∃[ x ] (Q x))
  -- Proof
  --to ⟨ x , inj₁ px ⟩ = inj₁ ⟨ x , px ⟩
  --to ⟨ x , inj₂ qx ⟩ = inj₂ ⟨ x , qx ⟩
  --
  -- Proof explained:
  to ∃x-px⊎qx =
    let
      ⟨ x , px⊎qx ⟩ = ∃x-px⊎qx  -- From ∃[ x ] (P x ⊎ Q x) we find an element x that fullfills (P x ⊎ Q x)
    in case px⊎qx of            -- P x ⊎ Q x  indicates two possible cases, either
      λ { (inj₁ px) → inj₁ ⟨ x , px ⟩  -- P x  is true, and so ∃[ x ] (P x)
        ; (inj₂ qx) → inj₂ ⟨ x , qx ⟩  -- or, Q x is true, and so ∃[ x ] (Q x)
      }

  -- Now, we prove the inverse (∃[ x ] (P x) ⊎ ∃[ x ] (Q x)) → (∃[ x ] (P x ⊎ Q x))
  from : ∀ {Object : Set} {P Q : Object → Set}
       → (∃[ x ] (P x) ⊎ ∃[ x ] (Q x)) → (∃[ x ] (P x ⊎ Q x))
  -- Proof
  --from (inj₁ ⟨ x , px ⟩) = ⟨ x , inj₁ px ⟩
  --from (inj₂ ⟨ x , qx ⟩) = ⟨ x , inj₂ qx ⟩
  --
  -- Proof explained:
  -- There are two possible properties that get fulfilled, either
  from (inj₁ ⟨ x , px ⟩) = ⟨ x , inj₁ px ⟩  -- ∃[ x ] (P x) gets fulfilled
  from (inj₂ ⟨ x , qx ⟩) = ⟨ x , inj₂ qx ⟩  -- or, ∃[ x ] (Q x) gets fulfilled

-- 2.

second : ∀ {Object : Set} {P Q : Object → Set} {_R_ : Object → Object → Set}
       → ∃[ x ] (P x)
       → ∃[ x ] (Q x)
       → (∀ x → P x → ∀ y → Q y → x R y)
       ---------------------------------
       → ∃[ x ] ∃[ y ] (x R y)
--Proof:
--second ⟨ x₁ , px₁ ⟩ ⟨ x₂ , qx₂ ⟩ ∀x→px→∀y→qy→xry = ⟨ x₁ , ⟨ x₂ , ∀x→px→∀y→qy→xry x₁ px₁ x₂ qx₂ ⟩ ⟩
--
--Proof explained:
second ∃x-px ∃x-qx ∀x→px→∀y→qy→xry =
  let
    ⟨ x₁ , px₁ ⟩ = ∃x-px  -- If we have a value from ∃[ x ] (P x), we can get an x₁ that fulfills P
    ⟨ x₂ , qx₂ ⟩ = ∃x-qx  -- and there is a value x₂ that fulfills Q
    px→∀y→qy→xry = ∀x→px→∀y→qy→xry x₁   -- For all x it is true that (P x → ∀ y → Q y → x R y), including x₁
    ∀y→qy→xry    = px→∀y→qy→xry px₁     -- P is fulfilled by x₁
    xry          = ∀y→qy→xry x₂ qx₂     -- In a similar way, x₂ is a value that fulfills Qy, so we can instanciate (∀ y → Q y → x₁ R y) into (x₁ R x₂)
  in ⟨ x₁ , ⟨ x₂ , xry ⟩ ⟩ -- So, we know there is an element x₁ and an element x₂ for which x₁ R x₂ is true


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

-- https://personal.cis.strath.ac.uk/conor.mcbride/pub/DepRep/DepRep.pdf

module Experiment.Outrageous.#02 where

data Zero : Set where
magic : Zero → (X : Set) → X
magic ()
record 𝟏 : Set where
  constructor void
data 𝟐 : Set where
  tt : 𝟐
  ff : 𝟐
If : 𝟐 → Set → Set → Set
If tt T F = T
If ff T F = F
if : (b : 𝟐) → (P : 𝟐 → Set) → P tt → P ff → P b
if tt P t f = t
if ff P t f = f
data ℕ : Set where
  ze : ℕ
  su : ℕ → ℕ
rec : (n : ℕ) → (P : ℕ → Set) → P ze → ((n : ℕ) → P n → P (su n)) → P n
rec ze     P z s = z
rec (su n) P z s = s n (rec n P z s)
record Σ (S : Set) (T : S → Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst


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

-- Monadic Adjunctions
-- https://ncatlab.org/nlab/show/monadic+adjunction
module Categories.Adjoint.Monadic where

open import Level

open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Category
open import Categories.Category.Equivalence
open import Categories.Functor
open import Categories.Monad

open import Categories.Category.Construction.EilenbergMoore
open import Categories.Category.Construction.Properties.EilenbergMoore

private
  variable
    o ℓ e : Level
    𝒞 𝒟 : Category o ℓ e

-- An adjunction is monadic if the adjunction "comes from" the induced monad in some sense.
record IsMonadicAdjunction {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) : Set (levelOfTerm 𝒞 ⊔ levelOfTerm 𝒟) where
  private
    T : Monad 𝒞
    T = adjoint⇒monad adjoint

  field
    Comparison⁻¹ : Functor (EilenbergMoore T) 𝒟
    comparison-equiv : WeakInverse (ComparisonF adjoint) Comparison⁻¹

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg
open import Agda.Builtin.FromString
open import Agda.Builtin.String
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.Int

instance
  NumberNat : Number Nat
  Number.Constraint NumberNat _ = ⊤
  Number.fromNat NumberNat n = n

  StringIsString : IsString String
  IsString.Constraint StringIsString _ = ⊤
  IsString.fromString StringIsString s = s

  ListIsString : IsString (List Char)
  IsString.Constraint ListIsString _ = ⊤
  IsString.fromString ListIsString s = primStringToList s

  NegativeInt : Negative Int
  Negative.Constraint NegativeInt _ = ⊤
  Negative.fromNeg NegativeInt zero = pos 0
  Negative.fromNeg NegativeInt (suc n) = negsuc n

abs : Int → Nat
abs (pos n) = n
abs (negsuc n) = suc n

postulate _+Z_ : Int → Int → Int

append : ∀ {a} {A : Set a} → List A → List A → List A
append [] ys = ys
append (x ∷ xs) ys = x ∷ append xs ys

-- no paren
give1 : Nat
give1 = suc {!4!}

-- paren
give2 : Nat
give2 = suc {!fromNat 4!}

-- no paren
give3 : List Char
give3 = append "foo" {!"bar"!}

-- paren
give4 : List Char
give4 = append "foo" {!fromString "bar"!}

-- no paren
give5 : Nat
give5 = abs {!-4!}

-- paren
give6 : Nat
give6 = abs {!fromNeg 4!}

-- 4 + ?
refine1 : Nat
refine1 = {!_+_ 4!}

-- fromNat 4 + ?
refine2 : Nat
refine2 = {!_+_ (fromNat 4)!}

-- append "foo" ?
refine3 : List Char
refine3 = {!append "foo"!}

-- append (fromString "foo") ?
refine4 : List Char
refine4 = {!append (fromString "foo")!}

-- -4 +Z ?
refine5 : Int
refine5 = {!-4 +Z_!}

-- fromNeg 4 +Z ?
refine6 : Int
refine6 = {!fromNeg 4 +Z_!}

postulate
  P : Nat → Int → List Char → Set

-- No fromXs in the goal
goal : P 4 -5 "6"
goal = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

module _ (A : Set) where

  postulate
    F : Set₁ → Set

  {-# POLARITY F ++ #-}

data D : Set where
  d : F D Set → D


text:
-- {-# OPTIONS -v interaction.give:30 -v 10  #-}
-- {-# OPTIONS -v tc.conv.irr:20 #-}

module GiveInSpiteOfUnsolvedIrr where

postulate
  .irrAxiom : ∀ {a}{A : Set a} → .A → A
{-# BUILTIN IRRAXIOM irrAxiom #-}

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

record MC (M : Set) (op : M → M → M) : Set where
  field
    elem   : M
    fun    : M → M
    .match : fun ≡ op elem

unitM : ∀ {M : Set} {op : M → M → M} → MC M op
unitM {M = M} = record
  { elem = {!!}
  ; fun  = λ x → x
  ; match = {!funExt ?!}  -- try give here
  }

{-
No variable of type
{M : Set} {.op : M → M → M} → (λ x → x) ≡ .op ?0 was found in
scope.
-}

-- This declaration needs to stay to trigger the error!
compM : ∀ {M : Set} {op : M → M → M} → MC M op → MC M op → MC M op
compM = {!!}

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2017-01-12, issue #2386

open import Agda.Primitive

data _≡_ {a b} {A : Set (a ⊔ b)} : (x y : A) → Set where
  refl : (x : A) → x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

-- Should be accepted

-- The type of primTrustMe has to match the flavor of EQUALITY

primitive primTrustMe : ∀ {a b}{A : Set _} {x y : A} → x ≡ y

testTM : ∀{A : Set} {a : A} → primTrustMe {x = a} {y = a} ≡ refl _
testTM = refl _

-- Testing rewrite

subst : ∀{ℓ}{A : Set ℓ} {P : A → Set}{a b : A} → _≡_ {a = ℓ} {b = ℓ} a b → P a → P b
subst eq p rewrite eq = p

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --erased-cubical --safe #-}

module Canon where

open import Data.Fin        using (Fin; #_; toℕ)
open import Data.Integer    using (ℤ; +_; -[1+_]; _-_)
open import Data.List       using (List; _∷_; []; map; concat; _++_; replicate; zip; length; take; drop)
open import Data.Nat        using (_*_; ℕ; suc; _+_)
open import Data.Nat.DivMod using (_mod_)
open import Data.Nat.Show   using (show)
open import Data.Product    using (_,_; uncurry)
open import Data.Sign       renaming (+ to s+ ; - to s-)
open import Data.Vec        using (fromList; toList; Vec; _∷_; []) renaming (replicate to rep; zip to vzip; map to vmap; concat to vconcat; _++_ to _+v_)
open import Function        using (_∘_)

open import Interval
open import Note
open import Pitch
open import MidiEvent
open import Util            using (repeat)
open import Transformation

makeImitations : {k : ℕ} → List Note → Vec Opi k → Vec (List Note) k
makeImitations subject []       = []
makeImitations subject (i ∷ is) = map (transposeNoteInterval i) subject ∷ makeImitations subject is

addDelays : {k : ℕ} → Duration → Vec (List Note) k → Vec (List Note) k
addDelays d lines = ads 0 lines where
  ads : {k : ℕ} → ℕ → Vec (List Note) k → Vec (List Note) k
  ads n []              = []
  ads n (notes ∷ lines) = (rest n ∷ notes) ∷ ads (n + d) lines

makeCanon : {k : ℕ} → List Note → ℕ → Duration → Vec Opi k → Vec (List Note) k
makeCanon subject reps d = addDelays d ∘ vmap (repeat reps) ∘ makeImitations subject

makeCanon2 : {k : ℕ} → List Note → Duration → Vec Opi k → Vec (List Note) k
makeCanon2 subject d is =
  addDelays d (makeImitations (
    repeat 2 subject ++
    inversion subject ++
    retrograde subject ++
    (retrograde ∘ inversion) subject)
    is)

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


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

-- https://ncatlab.org/nlab/show/span
-- The colimit of a functor from this category is a pushout in the target category.
module Categories.Category.Instance.Span where

open import Level
open import Categories.Category
open import Relation.Binary.PropositionalEquality

data SpanObj : Set where
  center : SpanObj
  left   : SpanObj
  right  : SpanObj

data SpanArr : SpanObj → SpanObj → Set where
  span-id   : ∀ {o} → SpanArr o o
  span-arrˡ : SpanArr center left
  span-arrʳ : SpanArr center right

span-compose : ∀ {x y z} → SpanArr y z → SpanArr x y → SpanArr x z
span-compose span-id span-id   = span-id
span-compose span-id span-arrˡ = span-arrˡ
span-compose span-id span-arrʳ = span-arrʳ
span-compose span-arrˡ span-id = span-arrˡ
span-compose span-arrʳ span-id = span-arrʳ

Span : Category 0ℓ 0ℓ 0ℓ
Span = record
  { Obj       = SpanObj
  ; _⇒_       = SpanArr
  ; _≈_       = _≡_
  ; id        = span-id
  ; _∘_       = span-compose
  ; assoc     = assoc
  ; sym-assoc = sym assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = λ {x} → identity² {x}
  ; equiv     = isEquivalence
  ; ∘-resp-≈  = λ { refl refl → refl }
  }
  where assoc : ∀ {x y z w} {f : SpanArr x y} {g : SpanArr y z} {h : SpanArr z w} →
                               span-compose (span-compose h g) f ≡
                               span-compose h (span-compose g f)
        assoc {_} {_} {_} {_} {span-id} {span-id} {span-id}   = refl
        assoc {_} {_} {_} {_} {span-id} {span-id} {span-arrˡ} = refl
        assoc {_} {_} {_} {_} {span-id} {span-id} {span-arrʳ} = refl
        assoc {_} {_} {_} {_} {span-id} {span-arrˡ} {span-id} = refl
        assoc {_} {_} {_} {_} {span-id} {span-arrʳ} {span-id} = refl
        assoc {_} {_} {_} {_} {span-arrˡ} {span-id} {span-id} = refl
        assoc {_} {_} {_} {_} {span-arrʳ} {span-id} {span-id} = refl

        identityˡ : ∀ {x y} {f : SpanArr x y} → span-compose span-id f ≡ f
        identityˡ {_} {_} {span-id}   = refl
        identityˡ {_} {_} {span-arrˡ} = refl
        identityˡ {_} {_} {span-arrʳ} = refl

        identityʳ : ∀ {x y} {f : SpanArr x y} → span-compose f span-id ≡ f
        identityʳ {_} {_} {span-id}   = refl
        identityʳ {_} {_} {span-arrˡ} = refl
        identityʳ {_} {_} {span-arrʳ} = refl

        identity² : {x : SpanObj} → span-compose span-id span-id ≡ span-id
        identity² = refl


text:
module ctxt-types where

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

location : Set
location = string × posinfo -- file path and starting position in the file

-- file path and starting / ending position in file
span-location = string × posinfo × posinfo

-- missing locations
missing-location : location
missing-location = ("missing" , "missing")

missing-span-location : span-location
missing-span-location = ("missing" , "missing" , "missing")

{- we will generally keep classifiers of variables in hnf in the ctxt, although
   we will not necessarily unfold recursive type definitions. -}

defScope : Set
defScope = 𝔹
pattern localScope = tt
pattern globalScope = ff
pattern concrete-datatype = globalScope
pattern abstract-datatype = localScope

defParams : Set
defParams = maybe params

data ctxt-info : Set where
  -- for defining a datatype
--  datatype-def : defParams → (ind reg : kind) → ctrs → ctxt-info

  -- for defining a datatype constructor
  ctr-def : params → type → (ctrs-length ctr-index ctr-unerased-arrows : ℕ) → ctxt-info

  -- for declaring the type that proves a type is a datatype (X/Mu)
--  mu-def : defParams → var → kind → ctxt-info

  -- for declaring a variable to have a given type (with no definition)
  term-decl : type → ctxt-info

  -- for defining a variable to equal a term with a given type
  -- maybe term, because datatype X/Mu and X/mu have params, etc... but no def
  term-def : defParams → opacity → maybe term → type → ctxt-info

  -- for untyped term definitions
  term-udef : defParams → opacity → term → ctxt-info

  -- for declaring a variable to have a given kind (with no definition)
  type-decl : kind → ctxt-info

  -- for defining a variable to equal a type with a given kind
  type-def : defParams → opacity → maybe type → kind → ctxt-info

  -- for defining a variable to equal a kind
  kind-def : params → kind → ctxt-info

  -- to rename a variable at any level to another
  rename-def : var → ctxt-info

  -- representing a declaration of a variable with no other information about it
  var-decl : ctxt-info

sym-info : Set
sym-info = ctxt-info × location

data-info : Set
data-info = params × kind × kind × ctrs × encoding-defs × encoded-defs

is-term-level : ctxt-info → 𝔹
is-term-level (term-decl _) = tt
is-term-level (term-def _ _ _ _) = tt
is-term-level (term-udef _ _ _) = tt
is-term-level (ctr-def _ _ _ _ _ ) = tt
is-term-level _ = ff

record ctxt : Set where
  constructor mk-ctxt
  field
    -- current module fields
    fn : string
    mn : string
    ps : params
    qual : qualif

    -- filename → module name × symbols declared in that module,
    syms : trie (string × 𝕃 string)

    -- module name → filename × params,
    mod-map : trie (string × params)

    -- file ID's for use in to-string.agda
    id-map : trie ℕ
    id-current : ℕ
    id-list : 𝕍 string id-current

    -- symbols → ctxt-info × location
    i : trie sym-info

    -- concrete/global datatypes
    μ : trie data-info
    -- abstract/local datatypes
    μ' : trie (var × args)
    -- Is/D map
    Is/μ : trie var
    -- encoding defs (needed to generate fmaps for some datatypes, like rose tree)
    μ~ : trie (𝕃 (var × tmtp))
    -- highlighting datatypes (μ̲ = \Gm \_--)
    μᵤ : maybe encoding-defs  -- most recent datatype declaration, for use in untyped μ[']
    μ̲ :  stringset

ctxt-binds-var : ctxt → var → 𝔹
ctxt-binds-var Γ x = trie-contains (ctxt.qual Γ) x || trie-contains (ctxt.i Γ) x

ctxt-var-decl' : location → var → ctxt → ctxt
ctxt-var-decl' loc v Γ =
  record Γ {
    qual = trie-insert (ctxt.qual Γ) v (v , []);
    i = trie-insert (ctxt.i Γ) v (var-decl , loc);
    μ = trie-remove (ctxt.μ Γ) v;
    μ' = trie-remove (ctxt.μ' Γ) v;
    Is/μ = trie-remove (ctxt.Is/μ Γ) v;
    μ~ = trie-remove (ctxt.μ~ Γ) v;
    μ̲ = trie-remove (ctxt.μ̲ Γ) v
  }
ctxt-var-decl = ctxt-var-decl' missing-location

ctxt-var-decl-loc : posinfo → var → ctxt → ctxt
ctxt-var-decl-loc pi v Γ = ctxt-var-decl' (ctxt.fn Γ , pi) v Γ

qualif-var : ctxt → var → var
qualif-var Γ v with trie-lookup (ctxt.qual Γ) v
...| just (v' , _) = v'
...| nothing = v

ctxt-get-current-mod : ctxt → string × string × params × qualif
ctxt-get-current-mod (mk-ctxt fn mn ps qual _ _ _ _ _ _ _ _ _ _ _ _) = fn , mn , ps , qual

max_stars_repo_name: mudathirmahgoub/cedille

max_issues_repo_name: mudathirmahgoub/cedille

max_forks_repo_name: mudathirmahgoub/cedille


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

open import Base
open import Homotopy.PushoutDef

module Homotopy.PushoutUP {m} (D : pushout-diag m) (P : Set m → Set m)
  ⦃ PA : P (pushout-diag.A D) ⦄ ⦃ PB : P (pushout-diag.B D) ⦄
  ⦃ PC : P (pushout-diag.C D) ⦄ where

open pushout-diag D

-- Idea : [cocone E = (A → E) ×_(C → E) (B → E)]
record cocone (top : Set m) : Set m where
  constructor _,_,_
  field
    A→top : A → top
    B→top : B → top
    h : (c : C) → (A→top (f c)) ≡ (B→top (g c))
open cocone public

cocone-eq-raw : (top : Set m) {a1 a2 : A → top} {b1 b2 : B → top}
  {h1 : (c : C) → a1 (f c) ≡ b1 (g c)} {h2 : (c : C) → a2 (f c) ≡ b2 (g c)}
  (p1 : a1 ≡ a2) (p2 : b1 ≡ b2) (p3 : transport _ p1 (transport _ p2 h1) ≡ h2)
  → (a1 , b1 , h1) ≡ (a2 , b2 , h2)
cocone-eq-raw top refl refl refl = refl

cocone-eq : (top : Set m) {a1 a2 : A → top} {b1 b2 : B → top}
  {h1 : (c : C) → a1 (f c) ≡ b1 (g c)} {h2 : (c : C) → a2 (f c) ≡ b2 (g c)}
  (p1 : a1 ≡ a2) (p2 : b1 ≡ b2)
  (p3 : (c : C) → happly p1 (f c) ∘ h2 c ≡ h1 c ∘ happly p2 (g c))
  → (a1 , b1 , h1) ≡ (a2 , b2 , h2)
cocone-eq top refl refl p3 =
  cocone-eq-raw top refl refl
    (funext (λ c → ! (refl-right-unit _) ∘ ! (p3 c)))

open import Homotopy.PullbackDef

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

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

pullback-to-cocone : (top : Set m)
  → pullback (D→top top)
  → cocone top
pullback-to-cocone top (a , b , h) = (a , b , happly h)

cocone-equiv-pullback : (top : Set m) → cocone top ≃ pullback (D→top top)
cocone-equiv-pullback top = (cocone-to-pullback top
  , iso-is-eq _
    (pullback-to-cocone top)
    (λ p → ap (λ u → _ , _ , u) (funext-happly _))
    (λ c → ap (λ u → _ , _ , u) (happly-funext _)))

pullback-equiv-cocone : (top : Set m) → pullback (D→top top) ≃ cocone top
pullback-equiv-cocone top = (pullback-to-cocone top
  , iso-is-eq _
    (cocone-to-pullback top)
    (λ c → ap (λ u → _ , _ , u) (happly-funext _))
    (λ p → ap (λ u → _ , _ , u) (funext-happly _)))

compose-cocone-map : (D E : Set m) (Dcocone : cocone D)
  → ((f : D → E) → cocone E)
compose-cocone-map D E (A→top , B→top , h) f =
  ((f ◯ A→top) , (f ◯ B→top) , (λ c → ap f (h c)))

is-pushout : (D : Set m) ⦃ PD : P D ⦄ (Dcocone : cocone D) → Set _
is-pushout D Dcocone = (E : Set m) ⦃ PE : P E ⦄
                     → is-equiv (compose-cocone-map D E Dcocone)

compose-cocone-map-compose : (D E F : Set m) (Dcocone : cocone D) (f : D → E)
  (g : E → F)
  → compose-cocone-map E F (compose-cocone-map D E Dcocone f) g
    ≡ compose-cocone-map D F Dcocone (g ◯ f)
compose-cocone-map-compose D E F Dcocone f g =
  ap (λ u → ((g ◯ (f ◯ cocone.A→top Dcocone))
             , (g ◯ (f ◯ cocone.B→top Dcocone)) , u))
      (funext (λ c → compose-ap g f (cocone.h Dcocone c)))

module _ (D : Set m) ⦃ PD : P D ⦄ (Dcocone : cocone D)
  (Dpushout : is-pushout D Dcocone) (E : Set m) ⦃ PE : P E ⦄
  (Ecocone : cocone E) (Epushout : is-pushout E Ecocone) where

  private
    DE-eq : (D → E) ≃ cocone E
    DE-eq = (compose-cocone-map D E Dcocone , Dpushout E)

    ED-eq : (E → D) ≃ cocone D
    ED-eq = (compose-cocone-map E D Ecocone , Epushout D)

    DD-eq : (D → D) ≃ cocone D
    DD-eq = (compose-cocone-map D D Dcocone , Dpushout D)

    EE-eq : (E → E) ≃ cocone E
    EE-eq = (compose-cocone-map E E Ecocone , Epushout E)

    D→E : D → E
    D→E = (DE-eq ⁻¹) ☆ Ecocone

    E→D : E → D
    E→D = (ED-eq ⁻¹) ☆ Dcocone

    abstract
      D→E→D : (λ x → E→D (D→E x)) ≡ (λ x → x)
      D→E→D = equiv-is-inj (compose-cocone-map D D Dcocone , Dpushout D) _ _
        (! (compose-cocone-map-compose D E D Dcocone D→E E→D)
        ∘ (ap (λ u → compose-cocone-map E D u E→D)
               (inverse-right-inverse DE-eq Ecocone)
        ∘ (inverse-right-inverse ED-eq Dcocone
          ∘ ap (λ u → _ , _ , u) (funext (λ c → ! (ap-id _))))))

      E→D→E : (λ x → D→E (E→D x)) ≡ (λ x → x)
      E→D→E = equiv-is-inj (compose-cocone-map E E Ecocone , Epushout E) _ _
        (! (compose-cocone-map-compose E D E Ecocone E→D D→E)
        ∘ (ap (λ u → compose-cocone-map D E u D→E)
               (inverse-right-inverse ED-eq Dcocone)
        ∘ (inverse-right-inverse DE-eq Ecocone
          ∘ ap (λ u → _ , _ , u) (funext (λ c → ! (ap-id _))))))

  pushout-equiv-pushout : D ≃ E
  pushout-equiv-pushout = (D→E , iso-is-eq _ E→D (happly E→D→E) (happly D→E→D))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Categories
open import Monads

module Monads.CatofAdj.TermAdjObj {a b}{C : Cat {a}{b}}(M : Monad C) where

open import Library
open import Functors
open import Naturals
open import Adjunctions
open import Monads.CatofAdj M
open import Categories.Terminal
open import Monads.EM M
open import Monads.EM.Adjunction M
open import Adjunctions.Adj2Mon

open Cat
open Fun
open Monad M
open NatT
open Adj

lemX : R EMAdj ○ L EMAdj ≅ TFun M
lemX = FunctorEq _ _ refl refl

EMObj : Obj CatofAdj
EMObj = record {
  D       = EM;
  adj     = EMAdj;
  law     = lemX;
  ηlaw    = idl C;
  bindlaw = λ{X Y f} →
    cong bind
         (stripsubst (Hom C X) f (fcong Y (cong OMap (sym lemX))))}

open ObjAdj
open Adj

alaw1lem : ∀{c d}{D : Cat {c}{d}}
  (T : Fun C C)(L : Fun C D)(R : Fun D C)
  (p : R ○ L ≅ T)
  (η : ∀ {X} → Hom C X (OMap T X)) →
  (right : ∀ {X Y} → Hom C X (OMap R Y) → Hom D (OMap L X) Y) →
  (left : ∀ {X Y} → Hom D (OMap L X) Y → Hom C X (OMap R Y)) →
  (ηlaw : ∀ {X} → left (iden D {OMap L X}) ≅ η {X}) →
  ∀ {X}{Z}{f : Hom C Z (OMap R X)} →
  (nat : comp C (HMap R (right f)) (comp C (left (iden D)) (iden C))
         ≅
         left (comp D (right f) (comp D (iden D) (HMap L (iden C))))) →
  (lawb : left (right f) ≅ f) →
  f
  ≅
  comp C (subst (λ Z₁ → Hom C Z₁ (OMap R X))
                (fcong Z (cong OMap p))
                (HMap R (right f)))
         η
alaw1lem {D = D} .(R ○ L) L R refl η right left ηlaw {X}{Z}{f} nat lawb =
  trans (trans (trans (sym lawb)
                      (cong left
                            (trans (sym (idr D))
                                   (cong (comp D (right f))
                                         (trans (sym (fid L))
                                                (sym (idl D)))))))
               (trans (sym nat)
                      (cong (comp C (HMap R (right f)))
                            (idr C))))
        (cong (comp C (HMap R (right f))) ηlaw)

alaw2lem : ∀{c d}{D : Cat {c}{d}}
  (T : Fun C C)(L : Fun C D)(R : Fun D C)
  (p : R ○ L ≅ T) →
  (right : ∀ {X Y} → Hom C X (OMap R Y) → Hom D (OMap L X) Y) →
  (bind : ∀ {X Y} → Hom C X (OMap T Y) → Hom C (OMap T X) (OMap T Y)) →
  (natright : {X₁ X' : Obj C} {Y Y' : Obj D} (f₁ : Hom C X' X₁)
    (g : Hom D Y Y') (h : Hom C X₁ (OMap R Y)) →
    right (comp C (HMap R g) (comp C h f₁))
    ≅
    comp D g (comp D (right h) (HMap L f₁))) →
  ∀ {X}{Z} {W} {k : Hom C Z (OMap T W)}{f : Hom C W (OMap R X)} →
  (bindlaw : HMap R (right (subst (Hom C Z) (fcong W (cong OMap (sym p))) k))
             ≅ bind k) →
  subst (λ Z → Hom C Z (OMap R X))
  (fcong Z (cong OMap p))
  (HMap R
   (right
    (comp C
     (subst (λ Z → Hom C Z (OMap R X))
      (fcong W (cong OMap p)) (HMap R (right f)))
     k)))
  ≅
  comp C
  (subst (λ Z → Hom C Z (OMap R X))
   (fcong W (cong OMap p)) (HMap R (right f)))
  (bind k)
alaw2lem {D = D} .(R ○ L) L R refl right bind natright {X}{Z}{W}{k}{f} bindlaw =
  trans (trans (cong (HMap R)
                     (trans (cong (λ k₁ → right (comp C (HMap R (right f)) k₁))
                                  (sym (idr C)))
                            (trans (natright (iden C) (right f) k)
                                   (trans (cong (λ h → comp D
                                                            (right f)
                                                            (comp D
                                                                  (right k)
                                                                  h))
                                                (fid L))
                                          (trans (sym (ass D))
                                                 (idr D))))))
               (fcomp R))
        (cong (comp C (HMap R (right f))) bindlaw)

ahomlem : ∀{c d}{D : Cat {c}{d}}
          (T : Fun C C)(L : Fun C D)(R : Fun D C)(p : R ○ L ≅ T) →
  (right : ∀ {X Y} → Hom C X (OMap R Y) → Hom D (OMap L X) Y) →
  (natright : {X₁ X' : Obj C} {Y Y' : Obj D} (f₁ : Hom C X' X₁)
    (g : Hom D Y Y') (h : Hom C X₁ (OMap R Y)) →
    right (comp C (HMap R g) (comp C h f₁))
    ≅
    comp D g (comp D (right h) (HMap L f₁))) →
  {X : Obj D}{Y : Obj D}{f : Hom D X Y} →
  {Z : Obj C} {f₁ : Hom C Z (OMap R X)} →
  comp C (HMap R f)
  (subst (λ Z₁ → Hom C Z₁ (OMap R X))
   (fcong Z (cong OMap p))
   (HMap R (right f₁)))
  ≅
  subst (λ Z₁ → Hom C Z₁ (OMap R Y))
  (fcong Z (cong OMap p))
  (HMap R (right (comp C (HMap R f) f₁)))
ahomlem {D = D} .(R ○ L) L R refl right natright {X}{Y}{f}{Z}{g} =
  trans (sym (fcomp R))
    (cong (HMap R)
     (sym
      (trans (cong (λ g₁ → right (comp C (HMap R f) g₁)) (sym (idr C)))
       (trans (natright (iden C) f g)
        (trans (cong (λ h → comp D f (comp D (right g) h)) (fid L))
         (trans (sym (ass D)) (idr D)))))))

Llawlem : ∀{c d}{D : Cat {c}{d}}
  (T : Fun C C)(L : Fun C D)(R : Fun D C)(p : R ○ L ≅ T) →
  (right : ∀ {X Y} → Hom C X (OMap R Y) → Hom D (OMap L X) Y) →
  (bind : ∀ {X Y} → Hom C X (OMap T Y) → Hom C (OMap T X) (OMap T Y)) →
  (bindlaw : {X Y : Obj C} {f : Hom C X (OMap T Y)} →
    HMap R
    (right
     (subst (Hom C X) (fcong Y (cong OMap (sym p))) f))
    ≅ bind f) →
  ∀{X Z} →
  {f  : Hom C Z (OMap R (OMap L X))}
  {f' : Hom C Z (OMap T X)} → (q  : f ≅ f') →
  subst (λ Z₁ → Hom C Z₁ (OMap R (OMap L X)))
  (fcong Z (cong OMap p)) (HMap R (right f))
  ≅ bind f'
Llawlem .(R ○ L) L R refl right bind bindlaw {X}{Z}{f}{.f} refl = bindlaw

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --without-K #-}
module NTypes.Product where

open import NTypes
open import PathOperations
open import PathStructure.Product
open import Types

×-isSet : ∀ {a b} {A : Set a} {B : Set b} →
  isSet A → isSet B → isSet (A × B)
×-isSet A-set B-set x y p q
  = split-eq p ⁻¹
  · ap (λ y → ap₂ _,_ y (ap π₂ p))
    (A-set _ _ (ap π₁ p) (ap π₁ q))
  · ap (λ y → ap₂ _,_ (ap π₁ q) y)
    (B-set _ _ (ap π₂ p) (ap π₂ q))
  · split-eq q
  where
  split-eq : (p : x ≡ y) → ap₂ _,_ (ap π₁ p) (ap π₂ p) ≡ p
  split-eq = π₂ (π₂ (π₂ split-merge-eq))

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


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

module sets.int.utils where

open import sum
open import equality
open import function
open import sets.nat.core
open import sets.int.definition
open import hott.level

module _ {i}{X : Set i}(hX : h 2 X)
  (f : ℕ → ℕ → ℕ → ℕ → X)
  (u : ∀ n n' d m m' e → f n n' m m' ≡ f (d + n) (d + n') (e + m) (e + m')) where

  private
    g : ℕ → ℕ → ℤ → X
    g n n' = elim-ℤ hX (f n n' , u n n' 0)

    lem : (n n' d m m' : ℕ) → g n n' (m [-] m') ≡ g (d + n) (d + n') (m [-] m')
    lem n n' d m m' = u n n' d m m' 0

    v : (n n' d : ℕ) → g n n' ≡ g (d + n) (d + n')
    v n n' d = funext λ m → elim-prop-ℤ
      (λ m → hX (g n n' m) (g (d + n) (d + n') m))
      (lem n n' d) m

    hX' : h 2 (ℤ → X)
    hX' = Π-level λ _ → hX

  elim₂-ℤ : ℤ → ℤ → X
  elim₂-ℤ = elim-ℤ hX' (g , v)

elim₂-prop-ℤ : ∀ {i}{X : ℤ → ℤ → Set i} → (∀ n m → h 1 (X n m))
             → ((n n' m m' : ℕ) → X (n [-] n') (m [-] m'))
             → ∀ n m → X n m
elim₂-prop-ℤ {i}{X} hX f = elim-prop-ℤ hX' g
  where
    g : (n n' : ℕ) → ∀ m → X (n [-] n') m
    g n n' = elim-prop-ℤ (hX (n [-] n')) (f n n')

    hX' : ∀ n → h 1 (∀ m → X n m)
    hX' n = Π-level λ m → hX n m

elim₃-prop-ℤ : ∀ {i}{X : ℤ → ℤ → ℤ → Set i} → (∀ n m p → h 1 (X n m p))
             → ((n n' m m' p p' : ℕ) → X (n [-] n') (m [-] m') (p [-] p'))
             → ∀ n m p → X n m p
elim₃-prop-ℤ {i}{X} hX f = elim-prop-ℤ hX' g
  where
    g : (n n' : ℕ) → ∀ m p → X (n [-] n') m p
    g n n' = elim₂-prop-ℤ (hX (n [-] n')) (f n n')

    hX' : ∀ n → h 1 (∀ m p → X n m p)
    hX' n = Π-level λ m → Π-level λ p → hX n m p

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Generic.Lib.Category where

open import Category.Functor public
open import Category.Applicative public
open import Category.Monad public

open RawFunctor {{...}} public
open RawApplicative {{...}} hiding (_<$>_; _<&>_; _<$_; zip; zipWith) renaming (_⊛_ to _<*>_) public
open RawMonad {{...}} hiding (pure; _<$>_; _<&>_; _<$_; _⊛_; _<⊛_; _⊛>_; _⊗_; rawFunctor; zip; zipWith) public

fmap = _<$>_

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module Issue4835.ModA where

data A : Set where
  a : A -> A


text:
-- Andreas, 2014-12-03 Issue reported by Fabien Renaud

postulate A : Set

f : A → A
g : A → A

f x = g x

ok : A → A
ok x = x

g x = f x

-- Only `f` and `g` should be colored red, not `ok`.


text:
postulate
  X Y Z A : Set

record R : Set where
  field
    x : X
    y : Y
    z : Z

module M where
  postulate
    x : X
    y : Y

r : R
r = record { M; z = zz } where postulate zz : Z

-- Record update. Same as: record r { y = ... }
r2 : R
r2 = record { R r; y = y } where postulate y : Y

module M2 (a : A) where
 postulate
  w : Y
  z : Z

r3 : A → R
r3 a = record { M hiding (y); M2 a renaming (w to y) }


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The reflexive transitive closures of McBride, Norell and Jansson
------------------------------------------------------------------------

-- This module could be placed under Relation.Binary. However, since
-- its primary purpose is to be used for _data_ it has been placed
-- under Data instead.

module Data.Star where

open import Relation.Binary
open import Function
open import Level

infixr 5 _◅_

-- Reflexive transitive closure.

data Star {i t} {I : Set i} (T : Rel I t) : Rel I (i ⊔ t) where
  ε   : Reflexive (Star T)
  _◅_ : ∀ {i j k} (x : T i j) (xs : Star T j k) → Star T i k
        -- The type of _◅_ is Trans T (Star T) (Star T); I expanded
        -- the definition in order to be able to name the arguments (x
        -- and xs).

-- Append/transitivity.

infixr 5 _◅◅_

_◅◅_ : ∀ {i t} {I : Set i} {T : Rel I t} → Transitive (Star T)
ε        ◅◅ ys = ys
(x ◅ xs) ◅◅ ys = x ◅ (xs ◅◅ ys)

-- Sometimes you want to view cons-lists as snoc-lists. Then the
-- following "constructor" is handy. Note that this is _not_ snoc for
-- cons-lists, it is just a synonym for cons (with a different
-- argument order).

infixl 5 _▻_

_▻_ : ∀ {i t} {I : Set i} {T : Rel I t} {i j k} →
      Star T j k → T i j → Star T i k
_▻_ = flip _◅_

-- A corresponding variant of append.

infixr 5 _▻▻_

_▻▻_ : ∀ {i t} {I : Set i} {T : Rel I t} {i j k} →
       Star T j k → Star T i j → Star T i k
_▻▻_ = flip _◅◅_

-- A generalised variant of map which allows the index type to change.

gmap : ∀ {i j t u} {I : Set i} {T : Rel I t} {J : Set j} {U : Rel J u} →
       (f : I → J) → T =[ f ]⇒ U → Star T =[ f ]⇒ Star U
gmap f g ε        = ε
gmap f g (x ◅ xs) = g x ◅ gmap f g xs

map : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} →
      T ⇒ U → Star T ⇒ Star U
map = gmap id

-- A generalised variant of fold.

gfold : ∀ {i j t p} {I : Set i} {J : Set j} {T : Rel I t}
        (f : I → J) (P : Rel J p) →
        Trans     T        (P on f) (P on f) →
        TransFlip (Star T) (P on f) (P on f)
gfold f P _⊕_ ∅ ε        = ∅
gfold f P _⊕_ ∅ (x ◅ xs) = x ⊕ gfold f P _⊕_ ∅ xs

fold : ∀ {i t p} {I : Set i} {T : Rel I t} (P : Rel I p) →
       Trans T P P → Reflexive P → Star T ⇒ P
fold P _⊕_ ∅ = gfold id P _⊕_ ∅

gfoldl : ∀ {i j t p} {I : Set i} {J : Set j} {T : Rel I t}
         (f : I → J) (P : Rel J p) →
         Trans (P on f) T        (P on f) →
         Trans (P on f) (Star T) (P on f)
gfoldl f P _⊕_ ∅ ε        = ∅
gfoldl f P _⊕_ ∅ (x ◅ xs) = gfoldl f P _⊕_ (∅ ⊕ x) xs

foldl : ∀ {i t p} {I : Set i} {T : Rel I t} (P : Rel I p) →
        Trans P T P → Reflexive P → Star T ⇒ P
foldl P _⊕_ ∅ = gfoldl id P _⊕_ ∅

concat : ∀ {i t} {I : Set i} {T : Rel I t} → Star (Star T) ⇒ Star T
concat {T = T} = fold (Star T) _◅◅_ ε

-- If the underlying relation is symmetric, then the reflexive
-- transitive closure is also symmetric.

revApp : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} →
         Sym T U → ∀ {i j k} → Star T j i → Star U j k → Star U i k
revApp rev ε        ys = ys
revApp rev (x ◅ xs) ys = revApp rev xs (rev x ◅ ys)

reverse : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} →
          Sym T U → Sym (Star T) (Star U)
reverse rev xs = revApp rev xs ε

-- Reflexive transitive closures form a (generalised) monad.

-- return could also be called singleton.

return : ∀ {i t} {I : Set i} {T : Rel I t} → T ⇒ Star T
return x = x ◅ ε

-- A generalised variant of the Kleisli star (flip bind, or
-- concatMap).

kleisliStar : ∀ {i j t u}
                {I : Set i} {J : Set j} {T : Rel I t} {U : Rel J u}
              (f : I → J) → T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
kleisliStar f g = concat ∘′ gmap f g

_⋆ : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} →
     T ⇒ Star U → Star T ⇒ Star U
_⋆ = kleisliStar id

infixl 1 _>>=_

_>>=_ : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} {i j} →
        Star T i j → T ⇒ Star U → Star U i j
m >>= f = (f ⋆) m

-- Note that the monad-like structure above is not an indexed monad
-- (as defined in Category.Monad.Indexed). If it were, then _>>=_
-- would have a type similar to
--
--   ∀ {I} {T U : Rel I t} {i j k} →
--   Star T i j → (T i j → Star U j k) → Star U i k.
--                  ^^^^^
-- Note, however, that there is no scope for applying T to any indices
-- in the definition used in Category.Monad.Indexed.


text:
open import Data.Nat using (ℕ)

module Data.BitVector.Properties.LatticeProperties (n : ℕ) where

open import Data.BitVector
open import Algebra.Structures
open import Relation.Binary.PropositionalEquality
open import Data.Vec
open import Data.Product hiding (map)
import Data.Bool.Properties as Bool

private
  module BitProperties = IsBooleanAlgebra Bool.isBooleanAlgebra
  -- All these properties follow trivially from the bit properties. TODO: generalize the pattern to just reuse the bitproperties
  ∨-comm : ∀ {n} (x y : BitVector n) → bitwise-or x y ≡ bitwise-or y x
  ∨-comm [] [] = refl
  ∨-comm (x ∷ xs) (y ∷ ys) rewrite BitProperties.∨-comm x y | ∨-comm xs ys = refl

  ∧-comm : ∀ {n} (x y : BitVector n) → bitwise-and x y ≡ bitwise-and y x
  ∧-comm [] [] = refl
  ∧-comm (x ∷ xs) (y ∷ ys) rewrite BitProperties.∧-comm x y | ∧-comm xs ys = refl

  ∨-assoc : ∀ {n} (x y z : BitVector n) → bitwise-or (bitwise-or x y) z ≡ bitwise-or x (bitwise-or y z)
  ∨-assoc [] [] [] = refl
  ∨-assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) rewrite BitProperties.∨-assoc x y z | ∨-assoc xs ys zs = refl

  ∧-assoc : ∀ {n} (x y z : BitVector n) → bitwise-and (bitwise-and x y) z ≡ bitwise-and x (bitwise-and y z)
  ∧-assoc [] [] [] = refl
  ∧-assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) rewrite BitProperties.∧-assoc x y z | ∧-assoc xs ys zs = refl

  ∨∧-absorb : ∀ {n} (x y : BitVector n) → bitwise-or x (bitwise-and x y) ≡ x
  ∨∧-absorb [] [] = refl
  ∨∧-absorb (x ∷ xs) (y ∷ ys) rewrite proj₁ BitProperties.absorptive x y | ∨∧-absorb xs ys = refl

  ∧∨-absorb : ∀ {n} (x y : BitVector n) → bitwise-and x (bitwise-or x y) ≡ x
  ∧∨-absorb [] [] = refl
  ∧∨-absorb (x ∷ xs) (y ∷ ys) rewrite proj₂ BitProperties.absorptive x y | ∧∨-absorb xs ys = refl

  ∨-cong : ∀ {n} {x y u v : BitVector n} → x ≡ y → u ≡ v → bitwise-or x u ≡ bitwise-or y v
  ∨-cong refl refl = refl

  ∧-cong : ∀ {n} {x y u v : BitVector n} → x ≡ y → u ≡ v → bitwise-and x u ≡ bitwise-and y v
  ∧-cong refl refl = refl

  isLattice : ∀ {n} → IsLattice _≡_ (bitwise-or {n}) bitwise-and
  isLattice = record
    { isEquivalence = isEquivalence
    ; ∨-comm = ∨-comm
    ; ∨-assoc = ∨-assoc
    ; ∨-cong = ∨-cong
    ; ∧-comm = ∧-comm
    ; ∧-assoc = ∧-assoc
    ; ∧-cong = ∧-cong
    ; absorptive = ∨∧-absorb , ∧∨-absorb
    }

  ∨∧-distribʳ : ∀ {n} (x y z : BitVector n) → bitwise-or (bitwise-and y z) x ≡ bitwise-and (bitwise-or y x) (bitwise-or z x)
  ∨∧-distribʳ [] [] [] = refl
  ∨∧-distribʳ (x ∷ xs) (y ∷ ys) (z ∷ zs) rewrite BitProperties.∨-∧-distribʳ x y z | ∨∧-distribʳ xs ys zs = refl

  isDistributiveLattice : ∀ {n} → IsDistributiveLattice _≡_ (bitwise-or {n}) bitwise-and
  isDistributiveLattice = record
    { isLattice = isLattice
    ; ∨-∧-distribʳ = ∨∧-distribʳ
    }

  ∨-complementʳ : ∀ {n} (x : BitVector n) → bitwise-or x (bitwise-negation x) ≡ ones n
  ∨-complementʳ [] = refl
  ∨-complementʳ (x ∷ xs) rewrite BitProperties.∨-complementʳ x | ∨-complementʳ xs = refl

  ∧-complementʳ : ∀ {n} (x : BitVector n) → bitwise-and x (bitwise-negation x) ≡ zero n
  ∧-complementʳ [] = refl
  ∧-complementʳ (x ∷ xs) rewrite BitProperties.∧-complementʳ x | ∧-complementʳ xs = refl

  ¬-cong : ∀ {n} {i j : BitVector n} → i ≡ j → bitwise-negation i ≡ bitwise-negation j
  ¬-cong refl = refl

isBooleanAlgebra : ∀ {n} → IsBooleanAlgebra _≡_ bitwise-or bitwise-and bitwise-negation (ones n) (zero n)
isBooleanAlgebra = record
  { isDistributiveLattice = isDistributiveLattice
  ; ∨-complementʳ = ∨-complementʳ
  ; ∧-complementʳ = ∧-complementʳ
  ; ¬-cong = ¬-cong
  }

max_stars_repo_name: copumpkin/bitvector

max_issues_repo_name: copumpkin/bitvector

max_forks_repo_name: copumpkin/bitvector


text:
------------------------------------------------------------------------------
-- Well-founded induction on the relation TreeT
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Mirror.TreeR.Induction.Acc.WellFoundedInduction
  where

open import FOTC.Base

open import FOT.FOTC.Program.Mirror.Induction.Acc.WellFounded
open import FOT.FOTC.Program.Mirror.TreeR
open import FOTC.Program.Mirror.Type

------------------------------------------------------------------------------
-- The relation TreeR is well-founded.
postulate wf-TreeR : WellFounded TreeR

-- Well-founded induction on the relation TreeT.
wfInd-TreeR :
  (P : D → Set) →
  (∀ {t} → Tree t → (∀ {t'} → Tree t' → TreeR t' t → P t') → P t) →
  ∀ {t} → Tree t → P t
wfInd-TreeR P = WellFoundedInduction wf-TreeR

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.Queue.1List where

open import Cubical.Foundations.Everything

open import Cubical.Structures.Queue

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Maybe
open import Cubical.Data.List
open import Cubical.Data.Sigma

module 1List {ℓ} (A : Type ℓ) (Aset : isSet A) where
 open Queues-on A Aset

 Q = List A

 emp : Q
 emp = []

 enq : A → Q → Q
 enq = _∷_

 deq : Q → Maybe (Q × A)
 deq [] = nothing
 deq (x ∷ []) = just ([] , x)
 deq (x ∷ x' ∷ xs) = deqMap (enq x) (deq (x' ∷ xs))

 Raw : RawQueue
 Raw = (Q , emp , enq , deq)

 WithLaws : Queue
 WithLaws = (Q , S , isSetQ , refl , deq-enq , isInjEnq , isInjDeq)
  where
   S = str Raw

   isSetQ : isSet Q
   isSetQ = isOfHLevelList 0 Aset

   deq-enq : ∀ a q → deq (enq a q) ≡ just (returnOrEnq S a (deq q))
   deq-enq a [] = refl
   deq-enq a (x ∷ []) = refl
   deq-enq a (x ∷ x' ∷ xs) =
     subst
       (λ t →
         deqMap (enq a) (deqMap (enq x) t)
         ≡ just (returnOrEnq S a (deqMap (enq x) t)))
       (deq-enq x' xs ⁻¹)
       refl

   isInjEnq : ∀ a a' q q' → enq a q ≡ enq a' q' → (a ≡ a') × (q ≡ q')
   isInjEnq _ _ _ _ p = fst c , ListPath.decode _ _ (snd c)
     where
     c = ListPath.encode _ _ p

   isInjReturnOrEnq : ∀ a a' qr qr'
     → returnOrEnq S a qr ≡ returnOrEnq S a' qr'
     → (a ≡ a') × (qr ≡ qr')
   isInjReturnOrEnq a a' nothing nothing p = cong snd p , refl
   isInjReturnOrEnq a a' nothing (just (q' , b')) p =
     ⊥.rec (lower (ListPath.encode _ _ (cong fst p)))
   isInjReturnOrEnq a a' (just (q , b)) nothing p =
     ⊥.rec (lower (ListPath.encode _ _ (cong fst p)))
   isInjReturnOrEnq a a' (just (q , b)) (just (q' , b')) p =
     fst c , cong just (ΣPathP (ListPath.decode _ _ (snd c) , cong snd p))
     where
     c = ListPath.encode _ _ (cong fst p)

   isInjDeq-lemma : ∀ q q' → MaybePath.Cover (deq q) (deq q') → q ≡ q'
   isInjDeq-lemma [] [] _ = refl
   isInjDeq-lemma [] (y ∷ q') c =
     ⊥.rec (lower (subst (MaybePath.Cover nothing) (deq-enq y q') c))
   isInjDeq-lemma (x ∷ q) [] c =
     ⊥.rec (lower (subst (λ r → MaybePath.Cover r nothing) (deq-enq x q) c))
   isInjDeq-lemma (x ∷ q) (y ∷ q') c =
     cong₂ _∷_ (fst p) (isInjDeq-lemma q q' (MaybePath.encode _ _ (snd p)))
     where
     p : (x ≡ y) × (deq q ≡ deq q')
     p =
       isInjReturnOrEnq _ _ _ _
         (subst (uncurry MaybePath.Cover) (ΣPathP (deq-enq x q , deq-enq y q')) c)

   isInjDeq : ∀ q q' → deq q ≡ deq q' → q ≡ q'
   isInjDeq _ _ p = isInjDeq-lemma _ _ (MaybePath.encode _ _ p)

 Finite : FiniteQueue
 Finite = (Q , str WithLaws , subst isEquiv (sym (funExt foldrCons)) (idIsEquiv _))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Common.Context where

open import Common public

-- Contexts.

data Cx (U : Set) : Set where
  ∅   : Cx U
  _,_ : Cx U → U → Cx U

-- Vector contexts.

data VCx (U : Set) : ℕ → Set where
  ∅   : VCx U zero
  _,_ : ∀ {n} → VCx U n → U → VCx U (suc n)

-- Inversion principles for contexts.

module _ {U : Set} where
  inv,₁ : ∀ {Γ Γ′ : Cx U} {A A′ : U} → (Γ Cx., A) ≡ (Γ′ , A′) → Γ ≡ Γ′
  inv,₁ refl = refl

  inv,₂ : ∀ {Γ Γ′ : Cx U} {A A′ : U} → (Γ Cx., A) ≡ (Γ′ , A′) → A ≡ A′
  inv,₂ refl = refl

-- Decidable equality for contexts.

module ContextEquality {U : Set} (_≟ᵁ_ : (A A′ : U) → Dec (A ≡ A′)) where
  _≟ᵀ⋆_ : (Γ Γ′ : Cx U) → Dec (Γ ≡ Γ′)
  ∅       ≟ᵀ⋆ ∅         = yes refl
  ∅       ≟ᵀ⋆ (Γ′ , A′) = no λ ()
  (Γ , A) ≟ᵀ⋆ ∅         = no λ ()
  (Γ , A) ≟ᵀ⋆ (Γ′ , A′) with Γ ≟ᵀ⋆ Γ′ | A ≟ᵁ A′
  (Γ , A) ≟ᵀ⋆ (.Γ , .A) | yes refl | yes refl = yes refl
  (Γ , A) ≟ᵀ⋆ (Γ′ , A′) | no  Γ≢Γ′ | _        = no (Γ≢Γ′ ∘ inv,₁)
  (Γ , A) ≟ᵀ⋆ (Γ′ , A′) | _        | no  A≢A′ = no (A≢A′ ∘ inv,₂)

-- Context membership, or nameless typed de Bruijn indices.

module _ {U : Set} where
  infix 3 _∈_
  data _∈_ (A : U) : Cx U → Set where
    instance
      top : ∀ {Γ} → A ∈ Γ , A
      pop : ∀ {B Γ} → A ∈ Γ → A ∈ Γ , B

  pop² : ∀ {A B C Γ} → A ∈ Γ → A ∈ Γ , B , C
  pop² = pop ∘ pop

  i₀ : ∀ {A Γ} → A ∈ Γ , A
  i₀ = top

  i₁ : ∀ {A B Γ} → A ∈ Γ , A , B
  i₁ = pop top

  i₂ : ∀ {A B C Γ} → A ∈ Γ , A , B , C
  i₂ = pop² top

  [_]ⁱ : ∀ {A Γ} → A ∈ Γ → ℕ
  [ top ]ⁱ   = zero
  [ pop i ]ⁱ = suc [ i ]ⁱ

-- Context inclusion, or order-preserving embedding.

module _ {U : Set} where
  infix 3 _⊆_
  data _⊆_ : Cx U → Cx U → Set where
    instance
      done : ∅ ⊆ ∅
      skip : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , A
      keep : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ , A ⊆ Γ′ , A

  skip² : ∀ {A B Γ Γ′} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , B , A
  skip² = skip ∘ skip

  keep² : ∀ {A B Γ Γ′} → Γ ⊆ Γ′ → Γ , B , A ⊆ Γ′ , B , A
  keep² = keep ∘ keep

  instance
    refl⊆ : ∀ {Γ} → Γ ⊆ Γ
    refl⊆ {∅}     = done
    refl⊆ {Γ , A} = keep refl⊆

  trans⊆ : ∀ {Γ Γ′ Γ″} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
  trans⊆ η        done      = η
  trans⊆ η        (skip η′) = skip (trans⊆ η η′)
  trans⊆ (skip η) (keep η′) = skip (trans⊆ η η′)
  trans⊆ (keep η) (keep η′) = keep (trans⊆ η η′)

  unskip⊆ : ∀ {A Γ Γ′} → Γ , A ⊆ Γ′ → Γ ⊆ Γ′
  unskip⊆ (skip η) = skip (unskip⊆ η)
  unskip⊆ (keep η) = skip η

  unkeep⊆ : ∀ {A Γ Γ′} → Γ , A ⊆ Γ′ , A → Γ ⊆ Γ′
  unkeep⊆ (skip η) = unskip⊆ η
  unkeep⊆ (keep η) = η

  weak⊆ : ∀ {A Γ} → Γ ⊆ Γ , A
  weak⊆ = skip refl⊆

  weak²⊆ : ∀ {A B Γ} → Γ ⊆ Γ , A , B
  weak²⊆ = skip² refl⊆

  bot⊆ : ∀ {Γ} → ∅ ⊆ Γ
  bot⊆ {∅}     = done
  bot⊆ {Γ , A} = skip bot⊆

-- Monotonicity of context membership with respect to context inclusion.

module _ {U : Set} where
  mono∈ : ∀ {A : U} {Γ Γ′} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
  mono∈ done     ()
  mono∈ (skip η) i       = pop (mono∈ η i)
  mono∈ (keep η) top     = top
  mono∈ (keep η) (pop i) = pop (mono∈ η i)

  reflmono∈ : ∀ {A Γ} → (i : A ∈ Γ) → i ≡ mono∈ refl⊆ i
  reflmono∈ top     = refl
  reflmono∈ (pop i) = cong pop (reflmono∈ i)

  transmono∈ : ∀ {A Γ Γ′ Γ″} → (η : Γ ⊆ Γ′) (η′ : Γ′ ⊆ Γ″) (i : A ∈ Γ)
               → mono∈ η′ (mono∈ η i) ≡ mono∈ (trans⊆ η η′) i
  transmono∈ done     η′        ()
  transmono∈ η        (skip η′) i       = cong pop (transmono∈ η η′ i)
  transmono∈ (skip η) (keep η′) i       = cong pop (transmono∈ η η′ i)
  transmono∈ (keep η) (keep η′) top     = refl
  transmono∈ (keep η) (keep η′) (pop i) = cong pop (transmono∈ η η′ i)

-- Concatenation of contexts.

module _ {U : Set} where
  _⧺_ : Cx U → Cx U → Cx U
  Γ ⧺ ∅        = Γ
  Γ ⧺ (Γ′ , A) = (Γ ⧺ Γ′) , A

  id⧺₁ : ∀ {Γ} → Γ ⧺ ∅ ≡ Γ
  id⧺₁ = refl

  id⧺₂ : ∀ {Γ} → ∅ ⧺ Γ ≡ Γ
  id⧺₂ {∅}     = refl
  id⧺₂ {Γ , A} = cong² _,_ id⧺₂ refl

  weak⊆⧺₁ : ∀ {Γ} Γ′ → Γ ⊆ Γ ⧺ Γ′
  weak⊆⧺₁ ∅        = refl⊆
  weak⊆⧺₁ (Γ′ , A) = skip (weak⊆⧺₁ Γ′)

  weak⊆⧺₂ : ∀ {Γ Γ′} → Γ′ ⊆ Γ ⧺ Γ′
  weak⊆⧺₂ {Γ} {∅}      = bot⊆
  weak⊆⧺₂ {Γ} {Γ′ , A} = keep weak⊆⧺₂

-- Thinning of contexts.

module _ {U : Set} where
  _∖_ : ∀ {A} → (Γ : Cx U) → A ∈ Γ → Cx U
  ∅       ∖ ()
  (Γ , A) ∖ top   = Γ
  (Γ , B) ∖ pop i = (Γ ∖ i) , B

  thin⊆ : ∀ {A Γ} → (i : A ∈ Γ) → Γ ∖ i ⊆ Γ
  thin⊆ top     = weak⊆
  thin⊆ (pop i) = keep (thin⊆ i)

-- Decidable equality of context membership.

module _ {U : Set} where
  data _=∈_ {A : U} {Γ} (i : A ∈ Γ) : ∀ {B} → B ∈ Γ → Set where
    same : i =∈ i
    diff : ∀ {B} → (j : B ∈ Γ ∖ i) → i =∈ mono∈ (thin⊆ i) j

  _≟∈_ : ∀ {A B : U} {Γ} → (i : A ∈ Γ) (j : B ∈ Γ) → i =∈ j
  top   ≟∈ top    = same
  top   ≟∈ pop j  rewrite reflmono∈ j = diff j
  pop i ≟∈ top    = diff top
  pop i ≟∈ pop j  with i ≟∈ j
  pop i ≟∈ pop .i | same   = same
  pop i ≟∈ pop ._ | diff j = diff (pop j)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

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

module Fields.FieldOfFractions.Ring {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where

open import Fields.FieldOfFractions.Setoid I
open import Fields.FieldOfFractions.Addition I
open import Fields.FieldOfFractions.Group I
open import Fields.FieldOfFractions.Multiplication I

fieldOfFractionsRing : Ring fieldOfFractionsSetoid fieldOfFractionsPlus fieldOfFractionsTimes
Ring.additiveGroup fieldOfFractionsRing = fieldOfFractionsGroup
Ring.*WellDefined fieldOfFractionsRing {a} {b} {c} {d} = fieldOfFractionsTimesWellDefined {a} {b} {c} {d}
Ring.1R fieldOfFractionsRing = record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }
Ring.groupIsAbelian fieldOfFractionsRing {record { num = a ; denom = b }} {record { num = c ; denom = d }} = Equivalence.transitive (Setoid.eq S) (Ring.*Commutative R) (Ring.*WellDefined R (Ring.*Commutative R) (Equivalence.transitive (Setoid.eq S) (Group.+WellDefined (Ring.additiveGroup R) (Ring.*Commutative R) (Ring.*Commutative R)) (Ring.groupIsAbelian R)))
Ring.*Associative fieldOfFractionsRing {record { num = a ; denom = b }} {record { num = c ; denom = d }} {record { num = e ; denom = f }} = Equivalence.transitive (Setoid.eq S) (Ring.*WellDefined R (Ring.*Associative R) (Ring.*Associative' R)) (Ring.*Commutative R)
Ring.*Commutative fieldOfFractionsRing {record { num = a ; denom = b }} {record { num = c ; denom = d }} = Equivalence.transitive (Setoid.eq S) (Ring.*Commutative R) (Ring.*WellDefined R (Ring.*Commutative R) (Ring.*Commutative R))
Ring.*DistributesOver+ fieldOfFractionsRing {record { num = a ; denom = b }} {record { num = c ; denom = d }} {record { num = e ; denom = f }} = need
  where
    open Setoid S
    open Ring R
    open Equivalence eq
    inter : b * (a * ((c * f) + (d * e))) ∼ (((a * c) * (b * f)) + ((b * d) * (a * e)))
    inter = transitive *Associative (transitive *DistributesOver+ (Group.+WellDefined additiveGroup (transitive *Associative (transitive (*WellDefined (transitive (*WellDefined (*Commutative) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative))) reflexive) (symmetric *Associative))) (transitive *Associative (transitive (*WellDefined (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) reflexive) (symmetric *Associative)))))
    need : ((a * ((c * f) + (d * e))) * ((b * d) * (b * f))) ∼ ((b * (d * f)) * (((a * c) * (b * f)) + ((b * d) * (a * e))))
    need = transitive (Ring.*WellDefined R reflexive (Ring.*WellDefined R reflexive (Ring.*Commutative R))) (transitive (Ring.*WellDefined R reflexive (Ring.*Associative R)) (transitive (Ring.*Commutative R) (transitive (Ring.*WellDefined R (Ring.*WellDefined R (symmetric (Ring.*Associative R)) reflexive) reflexive) (transitive (symmetric (Ring.*Associative R)) (Ring.*WellDefined R reflexive inter)))))
Ring.identIsIdent fieldOfFractionsRing {record { num = a ; denom = b }} = need
  where
    open Setoid S
    open Equivalence eq
    need : (((Ring.1R R) * a) * b) ∼ (((Ring.1R R * b)) * a)
    need = transitive (Ring.*WellDefined R (Ring.identIsIdent R) reflexive) (transitive (Ring.*Commutative R) (Ring.*WellDefined R (symmetric (Ring.identIsIdent R)) reflexive))


text:
module Oscar.Category.Semigroup where

open import Oscar.Category.Setoid
open import Oscar.Level

module _ {𝔬 𝔮} (setoid : Setoid 𝔬 𝔮) where
  open Setoid setoid

  record IsSemigroup (_∙_ : ⋆ → ⋆ → ⋆) : Set (𝔬 ⊔ 𝔮) where
    field
      extensionality : ∀ {f₁ f₂} → f₁ ≋ f₂ → ∀ {g₁ g₂} → g₁ ≋ g₂ → g₁ ∙ f₁ ≋ g₂ ∙ f₂
      associativity : ∀ f g h → (h ∙ g) ∙ f ≋ h ∙ (g ∙ f)

open IsSemigroup ⦃ … ⦄ public

record Semigroup 𝔬 𝔮 : Set (lsuc (𝔬 ⊔ 𝔮)) where
  field
    setoid : Setoid 𝔬 𝔮
  open Setoid setoid public

  infixl 7 _∙_
  field
    _∙_ : ⋆ → ⋆ → ⋆
    ⦃ isSemigroup ⦄ : IsSemigroup setoid _∙_


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

open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
open import Properties.Equality using (_≢_)

module Luau.Subtyping where

-- An implementation of semantic subtyping

-- We think of types as languages of trees

data Tree : Set where

  scalar : ∀ {T} → Scalar T → Tree
  function : Tree
  function-ok : Tree → Tree
  function-err : Tree → Tree

data Language : Type → Tree → Set
data ¬Language : Type → Tree → Set

data Language where

  scalar : ∀ {T} → (s : Scalar T) → Language T (scalar s)
  function : ∀ {T U} → Language (T ⇒ U) function
  function-ok : ∀ {T U u} → (Language U u) → Language (T ⇒ U) (function-ok u)
  function-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t)
  scalar-function-err : ∀ {S t} → (Scalar S) → Language S (function-err t)
  left : ∀ {T U t} → Language T t → Language (T ∪ U) t
  right : ∀ {T U u} → Language U u → Language (T ∪ U) u
  _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t
  unknown : ∀ {t} → Language unknown t

data ¬Language where

  scalar-scalar : ∀ {S T} → (s : Scalar S) → (Scalar T) → (S ≢ T) → ¬Language T (scalar s)
  scalar-function : ∀ {S} → (Scalar S) → ¬Language S function
  scalar-function-ok : ∀ {S u} → (Scalar S) → ¬Language S (function-ok u)
  function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s)
  function-ok : ∀ {T U u} → (¬Language U u) → ¬Language (T ⇒ U) (function-ok u)
  function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t)
  _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t
  left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t
  right : ∀ {T U u} → ¬Language U u → ¬Language (T ∩ U) u
  never : ∀ {t} → ¬Language never t

-- Subtyping as language inclusion

_<:_ : Type → Type → Set
(T <: U) = ∀ t → (Language T t) → (Language U t)

-- For warnings, we are interested in failures of subtyping,
-- which is whrn there is a tree in T's language that isn't in U's.

data _≮:_ (T U : Type) : Set where

  witness : ∀ t →

    Language T t →
    ¬Language U t →
    -----------------
    T ≮: U

max_stars_repo_name: EtiTheSpirit/luau

max_issues_repo_name: EtiTheSpirit/luau

max_forks_repo_name: EtiTheSpirit/luau


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

open import Clocked.Primitives
open import Cubical.Foundations.Prelude
open import Cubical.Data.List as List
open import Cubical.Data.List.Properties
open import Cubical.Data.Sum using (_⊎_; inl; inr)

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

-- In this document I want to define a monad, called ListLift, that is the free combination of the Lift monad and the List monad.
-- In order to do so, I will first define the Lift monad and the List monad, and check that they are indeed monads (Step 1 and 2).
-- Then I define the LiftList monad, check that it is a monad (Step 3), and finally check that it is the free monad on the algebra
-- structures of a delay algebra and a monoid (Step 4).

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

--************************--
-- Step 1: The Lift monad --
--************************--

-- Defining the monad myLift.
--(note that the return/unit is just x → nowL x)

data myLift (A : Set) (κ : Cl) : Set where
 nowL : A → (myLift A κ)
 stepL : ▹ κ (myLift A κ) → (myLift A κ)

bindL : {A B : Set} (κ : Cl) → (A → (myLift B κ)) → myLift A κ → myLift B κ
bindL κ f (nowL a) = f a
bindL κ f (stepL x) = stepL \(α) → bindL κ f (x α)

identity : {A : Set} → A → A
identity x = x

MultL : {A : Set} (κ : Cl) → (myLift (myLift A κ) κ) → (myLift A κ)
MultL κ = bindL κ identity

mapL : {A B : Set} (κ : Cl) → (A → B) → (myLift A κ) → (myLift B κ)
mapL κ f (nowL x) = nowL (f x)
mapL κ f (stepL x) = stepL (\ α →  mapL κ f (x α))

--checking that it is indeed a monad
-- needs to satisfy three monad laws:

-- unit is a left-identity for bind: bind (f, return) = f
-- unit is a right-identity for bind: bind (return, x) = x
-- bind is associative: bind (\x > bind (g, f(x)), x) = bind(g,bind(f, x))

-- The first of these is satisfied by definition
-- The other two laws we check here below

-- unit law, two versions to learn and remember to ways of doing guarded recursion in agda:
unitlawL : {A : Set}(κ : Cl) → ∀(x : (myLift A κ)) → (bindL {A} κ nowL x) ≡ x
unitlawL κ (nowL x) = refl
unitlawL κ (stepL x) = cong stepL (later-ext (\ α → unitlawL κ (x α)))

unitlawL' : {A : Set}(κ : Cl) → ∀(x : (myLift A κ)) → (bindL {A} κ nowL x) ≡ x
unitlawL' κ (nowL x) = refl
unitlawL' κ (stepL x) = \ i → stepL (\ α → unitlawL' κ (x α) i )

-- associative law:
associativelawL : {A B C : Set}(κ : Cl) → ∀(f : A → (myLift B κ)) → ∀ (g : B → (myLift C κ)) →
                                                ∀ (y : (myLift A κ)) → (bindL κ (\ x → (bindL κ g (f x))) y) ≡ (bindL κ g (bindL κ f y))
associativelawL κ f g (nowL x) = refl
associativelawL κ f g (stepL x) = cong stepL (((later-ext (\ α → associativelawL κ f g (x α)))))

-- Some properties that will be useful later:

-- interaction of mapL and MultL:
MultMap : {A B : Set} (κ : Cl) → ∀(x : myLift (myLift A κ) κ) → ∀(f : A → B) → mapL κ f (MultL κ x) ≡ MultL κ (mapL κ (mapL κ f) x)
MultMap κ (nowL x) f = refl
MultMap κ (stepL x) f = \ i → stepL (\ α → MultMap κ (x α) f i)

-- mapmap for mapL
mapmapL : {A B C : Set} (κ : Cl) → ∀(f : A → B) → ∀(g : B → C) → ∀(x : myLift A κ) → mapL κ g (mapL κ f x) ≡ mapL κ (\ y → g(f y)) x
mapmapL κ f g (nowL x) = refl
mapmapL κ f g (stepL x) =  (\ i → stepL (\ α → mapmapL κ f g (x α) i ))

--************************--
-- Step 2: The List monad --
--************************--

-- Defining the monad List
--List is already defined, but we define a unit and multiplication for it, so it becomes a monad

List-unit : {A : Set} → A → List A
List-unit x = [ x ]

List-mult : {A : Set} → List (List A) → List A
List-mult {A} = foldr _++_ []

List-bind : {A B : Set} → (A → List B) → List A → List B
List-bind f [] = []
List-bind f (x ∷ xs) = (f x) ++ (List-bind f xs)

-- and some other useful functions for later
safe-head : {A : Set} → A → List A → A
safe-head x []      = x
safe-head _ (x ∷ _) = x

tail : {A : Set} → List A → List A
tail [] = []
tail (x ∷ xs) = xs

-- Proving that this forms a monad
-- satisfying the laws:
-- List-mult (List-unit L) = L
-- List-mult (map List-unit L) = L
-- List-mult (List-Mult L) = List-mult (map List-mult L)
-- and both the unit and the multiplication are natural transformations

-- List-mult (List-unit L) = L
List-unitlaw1 : {A : Set} → ∀(L : List A) → List-mult (List-unit L) ≡ L
List-unitlaw1 [] = refl
List-unitlaw1 (x ∷ L) = cong (_++_ [ x ]) (List-unitlaw1 L)

-- List-mult (map List-unit L) = L
List-unitlaw2 : {A : Set} → ∀(L : List A) → List-mult (map List-unit L) ≡ L
List-unitlaw2 [] = refl
List-unitlaw2 (x ∷ L) = cong (_++_ [ x ]) (List-unitlaw2 L )

-- List-mult (List-Mult L) = List-mult (map List-mult L)
lemma : {A : Set} → ∀(L₁ L₂ : List (List A)) -> List-mult (L₁ ++ L₂) ≡ (List-mult L₁) ++ (List-mult L₂)
lemma [] L₂ = refl
lemma (L₁ ∷ L₃) L₂ = L₁ ++ List-mult (L₃ ++ L₂)
                     ≡⟨ cong (L₁ ++_) (lemma L₃ L₂) ⟩
                     L₁ ++ ((List-mult L₃) ++ (List-mult L₂))
                     ≡⟨ sym (++-assoc L₁ (List-mult L₃) (List-mult L₂)) ⟩
                     (L₁ ++ List-mult L₃) ++ List-mult L₂
                     ≡⟨ refl ⟩
                     (List-mult (L₁ ∷ L₃)) ++ (List-mult L₂) ∎

List-multlaw : {A : Set} -> ∀(L : List (List (List A))) -> List-mult (List-mult L) ≡ List-mult (map List-mult L)
List-multlaw [] = refl
List-multlaw (L ∷ L₁) = List-mult (L ++ List-mult L₁)
                        ≡⟨ lemma L (List-mult L₁) ⟩
                        (List-mult L ++ List-mult (List-mult L₁))
                        ≡⟨ cong (List-mult L ++_) (List-multlaw L₁) ⟩
                        List-mult L ++ List-mult (map List-mult L₁) ∎

-- the unit is a natural transformation:
nattrans-Listunit : {A B : Set} → ∀(f : A → B) → ∀(x : A) → map f (List-unit x) ≡ List-unit (f x)
nattrans-Listunit f x = refl

-- the multiplication is a natural transformation:
lemma-map++ : {A B : Set} → ∀(f : A → B) → ∀(xs ys : List A) → map f (xs ++ ys) ≡ (map f xs) ++ (map f ys)
lemma-map++ f [] ys = refl
lemma-map++ f (x ∷ xs) ys = cong ((f x) ∷_) (lemma-map++ f xs ys)

nattrans-Listmult : {A B : Set} → ∀(f : A → B) → ∀(xss : List (List A)) → map f (List-mult xss) ≡ List-mult (map (map f) xss)
nattrans-Listmult f [] = refl
nattrans-Listmult f (xs ∷ xss) = map f (xs ++ List-mult xss)
                                  ≡⟨ lemma-map++ f xs (List-mult xss) ⟩
                                  map f xs ++ map f (List-mult xss)
                                  ≡⟨ cong (map f xs ++_) (nattrans-Listmult f xss) ⟩
                                  map f xs ++ List-mult (map (map f) xss) ∎

--****************************--
-- Step 3: The ListLift monad --
--****************************--

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

data ListLift (A : Set) (κ : Cl) : Set where
  conLL : List (A ⊎ (▹ κ (ListLift A κ))) -> ListLift A κ

--***algebraic structure for ListLift***--

--nowLL and stepLL turn ListLift into a delay algebra structure:
nowLL : {A : Set} (κ : Cl) → A → (ListLift A κ)
nowLL κ a = conLL [ (inl a) ]

stepLL : {A : Set} (κ : Cl) → ▹ κ (ListLift A κ) → (ListLift A κ)
stepLL κ a = conLL [ (inr a) ]

--union, derived from list concatenation, turns ListLift into a monoid:
_∪_ : {A : Set} {κ : Cl} → (ListLift A κ) → (ListLift A κ) → (ListLift A κ)
_∪_ {A} {κ} (conLL x) (conLL y) = conLL (x ++ y)

--proof that this union does indeed provide a monoid structure:
conLLempty-rightunit : {A : Set} (κ : Cl) → ∀ (xs : (ListLift A κ)) → xs ∪ conLL [] ≡ xs
conLLempty-rightunit κ (conLL x) = conLL (x ++ []) ≡⟨ cong conLL (++-unit-r x) ⟩ conLL x ∎

conLLempty-leftunit : {A : Set} (κ : Cl) → ∀ (xs : (ListLift A κ)) → conLL [] ∪ xs ≡ xs
conLLempty-leftunit κ (conLL x) = refl

assoc∪ : {A : Set} {κ : Cl} → ∀(xs ys zs : (ListLift A κ)) → (xs ∪ ys) ∪ zs ≡ xs ∪ (ys ∪ zs)
assoc∪ {A} {κ} (conLL x) (conLL x₁) (conLL x₂) = cong conLL (++-assoc x x₁ x₂)

--a bind operator to make ListLift into a monad
bindLL : {A B : Set} (κ : Cl) → (A → (ListLift B κ)) → ListLift A κ → ListLift B κ
bindLL κ f (conLL []) = conLL []
bindLL κ f (conLL (inl x ∷ x₁)) = (f x) ∪ bindLL κ f (conLL x₁)
bindLL κ f (conLL (inr x ∷ x₁)) = (stepLL κ (\ α → bindLL κ f (x α))) ∪ bindLL κ f (conLL x₁)

--bind commutes with ∪
bindLL∪ : {A B : Set} (κ : Cl) → ∀(f : A → (ListLift B κ)) → ∀(xs ys : (ListLift A κ)) → bindLL κ f (xs ∪ ys) ≡ (bindLL κ f xs) ∪ (bindLL κ f ys)
bindLL∪ κ f xs (conLL []) =  bindLL κ f (xs ∪ conLL []) ≡⟨ cong (bindLL κ f) (conLLempty-rightunit κ xs)  ⟩
                                     bindLL κ f xs ≡⟨ sym (conLLempty-rightunit κ (bindLL κ f xs)) ⟩
                                     (bindLL κ f xs ∪ conLL [])∎
bindLL∪ κ f (conLL []) (conLL (x ∷ x₁)) = bindLL κ f (conLL (x ∷ x₁))
                                                 ≡⟨ sym (conLLempty-leftunit κ (bindLL κ f (conLL (x ∷ x₁)))) ⟩
                                                 (conLL [] ∪ bindLL κ f (conLL (x ∷ x₁))) ∎
bindLL∪ κ f (conLL (inl x₂ ∷ x₃)) (conLL (x ∷ x₁)) = (f x₂ ∪ bindLL κ f ((conLL x₃) ∪ (conLL (x ∷ x₁)))) ≡⟨ cong (f x₂ ∪_) (bindLL∪ κ f (conLL x₃) (conLL (x ∷ x₁))) ⟩
                                                           (f x₂ ∪ (bindLL κ f (conLL x₃) ∪ bindLL κ f (conLL (x ∷ x₁))))
                                                           ≡⟨ sym (assoc∪ (f x₂) (bindLL κ f (conLL x₃)) (bindLL κ f (conLL (x ∷ x₁))))  ⟩
                                                           ((f x₂ ∪ bindLL κ f (conLL x₃)) ∪ bindLL κ f (conLL (x ∷ x₁))) ∎
bindLL∪ κ f (conLL (inr x₂ ∷ x₃)) (conLL (x ∷ x₁)) = (conLL (inr (λ α → bindLL κ f (x₂ α)) ∷ []) ∪ bindLL κ f ((conLL x₃) ∪ (conLL (x ∷ x₁))))
                                                           ≡⟨ cong (conLL (inr (λ α → bindLL κ f (x₂ α)) ∷ []) ∪_) (bindLL∪ κ f (conLL x₃) (conLL (x ∷ x₁))) ⟩
                                                           (conLL (inr (λ α → bindLL κ f (x₂ α)) ∷ []) ∪ ((bindLL κ f (conLL x₃) ∪ bindLL κ f (conLL (x ∷ x₁)))))
                                                           ≡⟨  sym (assoc∪ (conLL (inr (λ α → bindLL κ f (x₂ α)) ∷ [])) (bindLL κ f (conLL x₃)) (bindLL κ f (conLL (x ∷ x₁))))  ⟩
                                                           ((conLL (inr (λ α → bindLL κ f (x₂ α)) ∷ []) ∪ bindLL κ f (conLL x₃)) ∪ bindLL κ f (conLL (x ∷ x₁))) ∎

--and a map function to prove naturality of bind and now
mapLL : {A B : Set} (κ : Cl) → (f : A → B) → (ListLift A κ) → (ListLift B κ)
mapLL κ f (conLL []) = conLL []
mapLL κ f (conLL (inl x ∷ x₁)) = conLL ([ inl (f x) ]) ∪ mapLL κ f (conLL x₁)
mapLL κ f (conLL (inr x ∷ x₁)) = (stepLL κ (\ α → mapLL κ f (x α))) ∪ mapLL κ f (conLL x₁)

--***proving that ListLift is a monad***--

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

--TODO: bind is a natural transformation

-- bindLL and nowLL also need to satisfy three monad laws:
-- unit is a left-identity for bind: bind (f, nowLL) = f
-- unit is a right-identity for bind: bind (nowLL, x) = x
-- bind is associative: bind (\x > bind (g, f(x)), x) = bind(g,bind(f, x))

-- unit is a left-identity for bind
unitlawLL1 :  {A B : Set} (κ : Cl) → ∀ (f : A → (ListLift B κ)) → ∀ (x : A) → (bindLL {A} κ f (nowLL κ x)) ≡ f x
unitlawLL1 κ f x = (f x ∪ conLL []) ≡⟨ conLLempty-rightunit κ (f x) ⟩ f x ∎

-- unit is a right-identity for bind
unitlawLL2 : {A : Set}(κ : Cl) → ∀(x : (ListLift A κ)) → (bindLL κ (nowLL κ) x) ≡ x
unitlawLL2 κ (conLL []) = refl
unitlawLL2 κ (conLL (inl x ∷ x₁)) = (conLL ([ inl x ]) ∪ bindLL κ (nowLL κ) (conLL x₁)) ≡⟨ cong (conLL ([ inl x ]) ∪_ ) (unitlawLL2 κ (conLL x₁)) ⟩
                                          (conLL ([ inl x ]) ∪ conLL x₁) ≡⟨ refl ⟩
                                          conLL (inl x ∷ x₁) ∎
unitlawLL2 κ (conLL (inr x ∷ x₁)) = (stepLL κ (\ α → bindLL κ (nowLL κ) (x α))) ∪ bindLL κ (nowLL κ) (conLL x₁)
                                          ≡⟨ cong ((stepLL κ (\ α → bindLL κ (nowLL κ) (x α))) ∪_) (unitlawLL2 κ (conLL x₁))  ⟩
                                          (stepLL κ (\ α → bindLL κ (nowLL κ) (x α))) ∪ conLL x₁
                                          ≡⟨  cong (_∪ conLL x₁) (\ i → stepLL κ (\ α → unitlawLL2 κ (x α) i ) )   ⟩
                                          conLL ([ inr x ]) ∪ conLL x₁
                                          ≡⟨ refl ⟩
                                          conLL (inr x ∷ x₁) ∎

-- bind is associative
assoclawLL : {A B C : Set}(κ : Cl) → ∀(f : A → (ListLift B κ)) → ∀ (g : B → (ListLift C κ)) → ∀ (x : (ListLift A κ))
                     → (bindLL κ (\ y → (bindLL κ g (f y))) x) ≡ (bindLL κ g (bindLL κ f x))
assoclawLL {A} {B} {C} κ f g (conLL []) = refl
assoclawLL {A} {B} {C} κ f g (conLL (inl x ∷ x₁)) = (bindLL κ g (f x) ∪ bindLL κ (λ y → bindLL κ g (f y)) (conLL x₁))
                                                          ≡⟨ cong (bindLL κ g (f x) ∪_) (assoclawLL κ f g (conLL x₁)) ⟩
                                                          (bindLL κ g (f x) ∪ bindLL κ g (bindLL κ f (conLL x₁)))
                                                          ≡⟨ sym (bindLL∪ κ g (f x) (bindLL κ f (conLL x₁))) ⟩
                                                          bindLL κ g (f x ∪ bindLL κ f (conLL x₁)) ∎
assoclawLL {A} {B} {C} κ f g (conLL (inr x ∷ x₁)) =  (conLL (inr (λ α → bindLL κ (λ y → bindLL κ g (f y)) (x α)) ∷ []) ∪ bindLL κ (λ y → bindLL κ g (f y)) (conLL x₁))
                                                           ≡⟨ cong (conLL (inr (λ α → bindLL κ (λ y → bindLL κ g (f y)) (x α)) ∷ []) ∪_) (assoclawLL κ f g (conLL x₁)) ⟩
                                                           (conLL (inr (λ α → bindLL κ (λ y → bindLL κ g (f y)) (x α)) ∷ []) ∪ (bindLL κ g (bindLL κ f (conLL x₁))))
                                                           ≡⟨ cong (_∪ (bindLL κ g (bindLL κ f (conLL x₁)))) (\ i → stepLL κ (\ α → assoclawLL κ f g (x α) i ) ) ⟩
                                                           ((bindLL κ g (conLL (inr (λ α → bindLL κ f (x α)) ∷ []))) ∪ (bindLL κ g (bindLL κ f (conLL x₁))) )
                                                           ≡⟨ sym (bindLL∪ κ g (conLL (inr (λ α → bindLL κ f (x α)) ∷ [])) (bindLL κ f (conLL x₁))) ⟩
                                                           bindLL κ g (conLL (inr (λ α → bindLL κ f (x α)) ∷ []) ∪ bindLL κ f (conLL x₁)) ∎

-- If I want to do it via fixpoints instead:

module WithFix where
  LiftList : (A : Set) → (κ : Cl) → Set
  LiftList A κ = fix (\ (X : ▹ κ Set) → List(A ⊎ (▸ κ \ α → (X α))))

  nowLLfix : {A : Set} (κ : Cl) → A → (LiftList A κ)
  nowLLfix κ a = [ (inl a) ]

  stepLLfix : {A : Set} (κ : Cl) → ▹ κ (LiftList A κ) → (LiftList A κ)
  stepLLfix {A} κ a = transport
                     (λ i →
                        fix-eq (λ (X : ▹ κ Type) → List (A ⊎ (▸ κ (λ α → X α)))) (~ i))
                     [ (inr a) ]

--***********************************************************************--
-- Step 4: The ListLift monad as the free delay-algebra and monoid monad --
--***********************************************************************--

-- We already know that (ListLift, stepLL) forms a delay algebra structure
-- and (Listlift, conLL [], _∪_) forms a monoid.
-- What we need to show is that ListLift 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 monoid
-- given a function f : A → B, there is a unique function ListLift A → B extending f that preserves the algebra structures.

record IsDelayalg {A : Set}(κ : Cl)(nextA : ▹ κ A → A) : Set where
  constructor isdelayalg

record IsMonoid {A : Set} (ε : A) (_·_ : A → A → A) : Set where
  constructor ismonoid

  field
    assoc : (x y z : A) → (x · y) · z ≡ x · (y · z)
    leftid : (x : A) → ε · x ≡ x
    rightid : (x : A) → x · ε ≡ x

record DelayMonoidData (A : Set) (κ : Cl) : Set where
  constructor dmdata
  field
    nextA : ▹ κ A → A
    ε : A
    _·_ : A → A → A

record IsDelayMonoid {A : Set}(κ : Cl) (dm : DelayMonoidData A κ) : Set where
  constructor isdelaymonoid

  open DelayMonoidData dm
  field
    isMonoid : IsMonoid (ε) (_·_)
    isDelayalg : IsDelayalg κ (nextA)

  open IsMonoid isMonoid public
  open IsDelayalg isDelayalg public

record IsPreservingDM {A B : Set}(κ : Cl) dmA dmB (g : A → B) : Set where
  constructor ispreservingDM

  open DelayMonoidData dmA renaming (ε to εA)
  open DelayMonoidData dmB renaming (ε to εB; nextA to nextB; _·_ to _*_)
  field
    unit-preserve : g (εA) ≡ εB
    next-preserve : (x : ▹ κ A) → g (nextA x) ≡ nextB (\ α → g (x α))
    union-preserve : (x y : A) → g (x · y) ≡ (g x) * (g y)

record IsExtending {A B : Set}{κ : Cl} (f : A → B) (h : (ListLift A κ) → B) : Set where
  constructor isextending

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

--fold defines the function we are after
fold : {A B : Set}{κ : Cl} → isSet A → isSet B → ∀ dm → IsDelayMonoid {B} κ dm → (A → B) → (ListLift A κ) → B
fold setA setB (dmdata nextB ε _·_) isDMB f (conLL []) = ε
fold setA setB dm@(dmdata nextB ε _·_) isDMB f (conLL (inl x ∷ x₁)) = (f x) · fold setA setB dm isDMB f (conLL x₁)
fold setA setB dm@(dmdata nextB ε _·_) isDMB f (conLL (inr x ∷ x₁)) = (nextB (\ α → fold setA setB dm isDMB f (x α))) · fold setA setB dm isDMB f (conLL x₁)

--fold extends the function f : A → B
--  direct proof:
fold-extends-f : {A B : Set}{κ : Cl} → ∀(setA : isSet A) → ∀(setB : isSet B) → ∀ dm → ∀(isDMB : IsDelayMonoid {B} κ dm) →
                   ∀ (f : A → B) → ∀ (x : A) → fold setA setB dm isDMB f (nowLL κ x) ≡ f x
fold-extends-f setA setB dm isDMB f x = IsDelayMonoid.rightid isDMB (f x)

--  or via the record "IsExtending":
fold-extends : {A B : Set}{κ : Cl} → ∀(setA : isSet A) → ∀(setB : isSet B) → ∀ dm → ∀(isDMB : IsDelayMonoid {B} κ dm) →
                   ∀ (f : A → B) → IsExtending f (fold setA setB dm isDMB f)
IsExtending.extends (fold-extends setA setB dm isDMB f) x = IsDelayMonoid.rightid isDMB (f x)

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

  --fold preseves the DelayMonoid structure
  fold-preserves : IsPreservingDM {ListLift A κ}{B} κ (dmdata (stepLL κ) (conLL []) _∪_) dm (fold setA setB dm isDMB f)
  unit-preserve fold-preserves = refl
  next-preserve fold-preserves x = IsDelayMonoid.rightid isDMB (nextB (λ α → fold setA setB dm isDMB f (x α)))
  union-preserve fold-preserves (conLL xs) (conLL ys) = lemma-union xs ys
    where
      lemma-union : ∀ xs ys → fold setA setB dm isDMB f (conLL xs ∪ conLL ys) ≡
                      (fold setA setB dm isDMB f (conLL xs) ·
                      fold setA setB dm isDMB f (conLL ys))
      lemma-union [] y = sym (IsDelayMonoid.leftid isDMB
                                  (fold setA setB dm isDMB f (conLL y)))
      lemma-union (inl x ∷ x₁) y = (f x · fold setA setB dm isDMB f (conLL (x₁ ++ y)))
                                   ≡⟨ cong (f x ·_) (lemma-union x₁ y) ⟩
                                   ((f x · (fold setA setB dm isDMB f (conLL x₁) ·
                                            fold setA setB dm isDMB f (conLL y))))
                                   ≡⟨ sym (IsDelayMonoid.assoc isDMB (f x)
                                             (fold setA setB dm isDMB f (conLL x₁))
                                             (fold setA setB dm isDMB f (conLL y))) ⟩
                                   ((f x · fold setA setB dm isDMB f (conLL x₁)) ·
                                           fold setA setB dm isDMB f (conLL y)) ∎
      lemma-union (inr x ∷ x₁) y =
                                (nextB (λ α → fold setA setB dm isDMB f (x α)) ·
                                  fold setA setB dm isDMB f (conLL (x₁ ++ y)))
                                ≡⟨ cong (nextB (λ α → fold setA setB dm isDMB f (x α)) ·_)
                                    (lemma-union
                                       x₁ y) ⟩
                                ( (nextB (λ α → fold setA setB dm isDMB f (x α)) ·
                                    (fold setA setB dm isDMB f (conLL x₁) ·
                                     fold setA setB dm isDMB f (conLL y))))
                                ≡⟨ sym (IsDelayMonoid.assoc isDMB
                                    (nextB (λ α → fold setA setB dm isDMB f (x α)))
                                    (fold setA setB dm isDMB f (conLL x₁))
                                    (fold setA setB dm isDMB f (conLL y)))  ⟩
                                ((nextB (λ α → fold setA setB dm isDMB f (x α)) ·
                                  fold setA setB dm isDMB f (conLL x₁)) ·
                                  fold setA setB dm isDMB f (conLL y)) ∎

--and fold 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 : ListLift A κ → B)
                       (setA : isSet A) (setB : isSet B) (dm : _) (isDMB : IsDelayMonoid {B} κ dm)
                       (f : A → B) (isPDM : IsPreservingDM {ListLift A κ}{B} κ (dmdata (stepLL κ) (conLL []) _∪_ ) dm h)
                       (isExt : IsExtending f h) where

  open DelayMonoidData dm renaming (nextA to nextB)

  fold-uniquenessLL : (x : (ListLift A κ)) → h x ≡ (fold setA setB dm isDMB f x)
  fold-uniquenessLL (conLL []) = h (conLL [])
                                 ≡⟨ IsPreservingDM.unit-preserve isPDM ⟩
                                 ε
                                 ≡⟨ refl ⟩
                                 fold setA setB dm isDMB f (conLL []) ∎
  fold-uniquenessLL (conLL (inl x ∷ x₁)) = h (conLL (inl x ∷ x₁))
                                           ≡⟨ refl ⟩
                                           h ((conLL [ inl x ]) ∪ (conLL x₁))
                                           ≡⟨ IsPreservingDM.union-preserve isPDM (conLL [ inl x ]) (conLL x₁) ⟩
                                           ((h (conLL [ inl x ])) ·
                                             (h (conLL x₁)) )
                                           ≡⟨ cong (_· (h (conLL x₁)) ) (IsExtending.extends isExt x)  ⟩
                                           (f x · (h (conLL x₁)))
                                           ≡⟨ cong (f x ·_)(fold-uniquenessLL (conLL x₁)) ⟩
                                           (f x · fold setA setB dm isDMB f (conLL x₁)) ∎
  fold-uniquenessLL (conLL (inr x ∷ x₁)) =  h (conLL (inr x ∷ x₁))
                                            ≡⟨ cong (h ) refl ⟩
                                            h ((conLL [ inr x ]) ∪ (conLL x₁))
                                            ≡⟨ IsPreservingDM.union-preserve isPDM (conLL [ inr x ]) (conLL x₁) ⟩
                                            (h (conLL [ inr x ])) ·
                                              (h (conLL x₁))
                                            ≡⟨ cong (_· h (conLL x₁)) refl ⟩
                                            ((h (stepLL κ x)) ·
                                              (h (conLL x₁)) )
                                            ≡⟨ cong (_· h (conLL x₁)) (IsPreservingDM.next-preserve isPDM x) ⟩
                                            (((nextB (λ α → h (x α))) · (h (conLL x₁))))
                                            ≡⟨ cong (_· h (conLL x₁)) (cong (nextB)
                                               (later-ext (\ α → fold-uniquenessLL (x α)))) ⟩
                                            ((nextB (λ α → fold setA setB dm isDMB f (x α))) · (h (conLL x₁)))
                                            ≡⟨ cong (nextB (λ α → fold setA setB dm isDMB f (x α)) ·_)
                                                 (fold-uniquenessLL (conLL x₁)) ⟩
                                            (nextB (λ α → fold setA setB dm isDMB f (x α)) ·
                                                fold setA setB dm isDMB f (conLL x₁)) ∎

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

--We now define a composite monad of the List and Lift monads, formed via a distributive law.

LcL : (A : Set) → (κ : Cl) → Set
LcL A κ = myLift (List A) κ

-- the unit of this monad is simply the composit of the units for Lift (nowL x) and List ([x])
nowLcL : {A : Set} {κ : Cl} → A → (LcL A κ)
nowLcL x = nowL [ x ]

-- LcL is a monad via a distributive law, distributing List over Lift.
-- Here is the distributive law:
distlawLcL : {A : Set} (κ : Cl) → List (myLift A κ) → (LcL A κ)
distlawLcL κ [] = nowL []
distlawLcL κ (nowL x ∷ xs) = MultL κ (nowL (mapL κ (([ x ]) ++_) (distlawLcL κ xs)))
distlawLcL κ (stepL x ∷ xs) = stepL (\ α → distlawLcL κ ((x α) ∷ xs))

--proof that distlawLcL is indeed a distributive law:
--unit laws:
unitlawLcL1 : {A : Set} (κ : Cl) → ∀(x : myLift A κ) → (distlawLcL κ (List-unit x )) ≡  mapL κ List-unit x
unitlawLcL1 κ (nowL x) = refl
unitlawLcL1 κ (stepL x) = (\ i → stepL (\ α → unitlawLcL1 κ (x α) i ))

unitlawLcL2 : {A : Set} (κ : Cl) → ∀(xs : List A) → (distlawLcL κ (map nowL xs)) ≡  nowL xs
unitlawLcL2 κ [] = refl
unitlawLcL2 κ (x ∷ xs) = mapL κ (λ ys → x ∷ ys) (distlawLcL κ (map nowL xs))
                          ≡⟨ cong (mapL κ (λ ys → x ∷ ys)) (unitlawLcL2 κ xs) ⟩
                          mapL κ (λ ys → x ∷ ys) (nowL xs)
                          ≡⟨ refl ⟩
                          nowL (x ∷ xs) ∎

--multiplication laws:

-- In the proof of the first multiplication law, I need a lemma about list concatenation,
-- namely that putting a singleton list in front of a list of lists, and concatening the result
-- yields the same list as putting the element of the signleton in front of the first list in the list of lists,
-- and then concatenating the result.
-- The lemma is split into two parts, first the general result as described in words here,
-- followed by the specific situation in which I need it in the proofs below.
lemma7a : {A : Set} → ∀(x : A) → ∀(xss : (List (List A))) → List-mult ((x ∷ safe-head [] xss) ∷ tail xss ) ≡ List-mult (([ x ]) ∷ xss)
lemma7a x [] = refl
lemma7a x (xs ∷ xss) = refl

lemma7b : {A : Set} (κ : Cl) → ∀(y : myLift (List (List A)) κ) → ∀(x : A) →
           mapL κ (λ xss → List-mult ((x ∷ safe-head [] xss) ∷ tail xss)) y ≡ mapL κ (λ xss → List-mult (([ x ]) ∷ xss)) y
lemma7b κ (nowL xss) x = cong nowL (lemma7a x xss)
lemma7b κ (stepL xss) x = (\ i → stepL (\ α → lemma7b κ (xss α) x i ))

-- in addition, I need this rather technical lemma that allows me to pull a mapL through the distributive law.
-- without it, I could not finish the proof.
lemma8 :  {A : Set} (κ : Cl) → ∀(x : A) → ∀(xs : myLift (List A) κ) → ∀(xss : List (myLift (List A) κ)) →
                 mapL κ (λ yss → ((x ∷ safe-head [] yss) ∷ tail yss)) (distlawLcL κ (xs ∷ xss)) ≡ distlawLcL κ (mapL κ (λ ys → x ∷ ys) xs ∷ xss)
lemma8 κ x (nowL ys) [] = refl
lemma8 κ x (stepL ys) [] = (\ i → stepL (λ α → lemma8 κ x (ys α) [] i ))
lemma8 κ x (nowL []) (zs ∷ xss) =  mapL κ (λ yss → (x ∷ safe-head [] yss) ∷ tail yss) (mapL κ (λ zss → [] ∷ zss) (distlawLcL κ (zs ∷ xss)))
                                   ≡⟨ mapmapL κ ((λ zss → [] ∷ zss)) ((λ yss → (x ∷ safe-head [] yss) ∷ tail yss)) (distlawLcL κ (zs ∷ xss)) ⟩
                                   mapL κ (λ yss → (x ∷ safe-head [] ([] ∷ yss)) ∷ tail ([] ∷ yss)) (distlawLcL κ (zs ∷ xss))
                                   ≡⟨ refl ⟩
                                   mapL κ (λ yss → (x ∷ []) ∷ yss) (distlawLcL κ (zs ∷ xss)) ∎
lemma8 κ x (nowL (y ∷ ys)) (zs ∷ xss) = mapL κ (λ yss → (x ∷ safe-head [] yss) ∷ tail yss) (mapL κ (λ zss → (y ∷ ys) ∷ zss) (distlawLcL κ (zs ∷ xss)))
                                         ≡⟨ mapmapL κ ((λ zss → (y ∷ ys) ∷ zss)) ((λ yss → (x ∷ safe-head [] yss) ∷ tail yss)) (distlawLcL κ (zs ∷ xss)) ⟩
                                         mapL κ (λ yss → (x ∷ safe-head []((y ∷ ys) ∷ yss)) ∷ tail((y ∷ ys) ∷ yss)) (distlawLcL κ (zs ∷ xss))
                                         ≡⟨ refl ⟩
                                         mapL κ (λ yss → (x ∷ y ∷ ys) ∷ yss) (distlawLcL κ (zs ∷ xss)) ∎
lemma8 κ x (stepL ys) (zs ∷ xss) = (\ i → stepL (λ α → lemma8 κ x (ys α) (zs ∷ xss) i ))

--now we are ready to prove the multiplication laws:
multlawLcL1 : {A : Set} (κ : Cl) → ∀(xss : List (List (myLift A κ))) → distlawLcL κ (List-mult xss) ≡
                                     mapL κ List-mult (distlawLcL κ (map (distlawLcL κ) xss))
multlawLcL1 κ [] = refl
multlawLcL1 κ ([] ∷ xss) = distlawLcL κ (List-mult xss)
                            ≡⟨ multlawLcL1 κ xss ⟩
                            mapL κ List-mult (distlawLcL κ (map (distlawLcL κ) xss))
                            ≡⟨ refl ⟩
                            mapL κ (λ ys → List-mult ([] ∷ ys)) (distlawLcL κ (map (distlawLcL κ) xss))
                            ≡⟨ sym (mapmapL κ (\ ys → [] ∷ ys) List-mult ((distlawLcL κ (map (distlawLcL κ) xss)))) ⟩
                            mapL κ List-mult (mapL κ (λ ys → [] ∷ ys) (distlawLcL κ (map (distlawLcL κ) xss))) ∎
multlawLcL1 κ ((nowL x ∷ []) ∷ xss) =  mapL κ (λ ys → x ∷ ys) (distlawLcL κ (List-mult xss))
                                         ≡⟨ cong (mapL κ (λ ys → x ∷ ys)) (multlawLcL1 κ xss) ⟩
                                         mapL κ (λ ys → x ∷ ys) (mapL κ List-mult (distlawLcL κ (map (distlawLcL κ) xss)))
                                         ≡⟨ mapmapL κ List-mult (λ ys → x ∷ ys) (distlawLcL κ (map (distlawLcL κ) xss)) ⟩
                                         mapL κ (λ ys → x ∷ List-mult ys) (distlawLcL κ (map (distlawLcL κ) xss))
                                         ≡⟨ refl ⟩
                                         mapL κ (λ ys → List-mult (([ x ]) ∷ ys)) (distlawLcL κ (map (distlawLcL κ) xss))
                                         ≡⟨ sym( mapmapL κ (λ ys → ([ x ]) ∷ ys) List-mult (distlawLcL κ (map (distlawLcL κ) xss))) ⟩
                                         mapL κ List-mult (mapL κ (λ ys → ([ x ]) ∷ ys) (distlawLcL κ (map (distlawLcL κ) xss))) ∎
multlawLcL1 κ ((nowL x ∷ y ∷ xs) ∷ xss) = mapL κ (λ ys → x ∷ ys) (distlawLcL κ (List-mult ((y ∷ xs) ∷ xss)))
                                            ≡⟨ cong (mapL κ (λ ys → x ∷ ys)) (multlawLcL1 κ ((y ∷ xs) ∷ xss)) ⟩
                                            mapL κ (λ ys → x ∷ ys) (mapL κ List-mult (distlawLcL κ (map (distlawLcL κ) ((y ∷ xs) ∷ xss))))
                                            ≡⟨ mapmapL κ List-mult (λ ys → x ∷ ys) (distlawLcL κ (map (distlawLcL κ) ((y ∷ xs) ∷ xss))) ⟩
                                            mapL κ (λ yss → x ∷ (List-mult yss)) (distlawLcL κ (map (distlawLcL κ) ((y ∷ xs) ∷ xss)))
                                            ≡⟨ refl ⟩
                                            mapL κ (λ yss → x ∷ List-mult yss) (distlawLcL κ (distlawLcL κ (y ∷ xs) ∷ map (distlawLcL κ) xss))
                                            ≡⟨ refl ⟩
                                            mapL κ (λ yss → List-mult (([ x ]) ∷ yss)) (distlawLcL κ (distlawLcL κ (y ∷ xs) ∷ map (distlawLcL κ) xss))
                                            ≡⟨ sym (lemma7b κ ((distlawLcL κ (distlawLcL κ (y ∷ xs) ∷ map (distlawLcL κ) xss))) x) ⟩
                                            mapL κ (λ yss → List-mult ((x ∷ safe-head [] yss) ∷ tail yss)) (distlawLcL κ (distlawLcL κ (y ∷ xs) ∷ map (distlawLcL κ) xss))
                                            ≡⟨ sym (mapmapL κ ((λ yss → ((x ∷ safe-head [] yss) ∷ tail yss))) List-mult
                                                ((distlawLcL κ (distlawLcL κ (y ∷ xs) ∷ map (distlawLcL κ) xss)))) ⟩
                                            mapL κ List-mult (mapL κ (λ yss → ((x ∷ safe-head [] yss) ∷ tail yss)) (distlawLcL κ (distlawLcL κ (y ∷ xs) ∷ map (distlawLcL κ) xss)))
                                            ≡⟨ cong (mapL κ List-mult) (lemma8 κ x ((distlawLcL κ (y ∷ xs))) ((map (distlawLcL κ) xss))) ⟩
                                            mapL κ List-mult (distlawLcL κ (mapL κ (λ ys → x ∷ ys) (distlawLcL κ (y ∷ xs)) ∷ (map (distlawLcL κ) xss))) ∎
multlawLcL1 κ ((stepL x ∷ xs) ∷ xss) = (\ i → stepL (\ α → multlawLcL1 κ ((x α ∷ xs) ∷ xss) i ))

lemma9a : {A : Set} (κ : Cl) → ∀(x : ▹ κ (myLift A κ)) → ∀(y : ▹ κ (myLift (List (myLift A κ)) κ)) →
                   MultL κ (stepL (λ α → stepL (λ β → mapL κ (λ ys → distlawLcL κ (x α ∷ ys)) (y β)))) ≡
                   MultL κ (stepL (λ β → stepL (λ α → mapL κ (λ ys → distlawLcL κ (x α ∷ ys)) (y β))))
lemma9a κ x y = cong (MultL κ) (cong stepL (later-ext λ α → cong stepL (later-ext λ β →
                     cong₂ (mapL κ) (funExt (λ ys → cong (distlawLcL _) (cong₂ _∷_ (tick-irr x α β) refl)))
                                    (sym (tick-irr y α β)))))

lemma9 : {A : Set} (κ : Cl) → ∀(x : ▹ κ (myLift A κ)) → ∀(y : myLift (List (myLift A κ)) κ) →
            MultL κ (stepL (λ α → (mapL κ (λ ys → distlawLcL κ (x α ∷ ys)) y))) ≡ MultL κ (mapL κ (λ ys → stepL (λ α → distlawLcL κ (x α ∷ ys))) y)
lemma9 κ x (nowL y) = refl
lemma9 κ x (stepL y) = stepL (λ α → stepL (λ β → MultL κ (mapL κ (λ ys → distlawLcL κ (x α ∷ ys)) (y β))))
                        ≡⟨ lemma9a κ x y ⟩
                        stepL (λ β → stepL (λ α → MultL κ (mapL κ (λ ys → distlawLcL κ (x α ∷ ys)) (y β))))
                        ≡⟨ ( (\ i → stepL (\ β → lemma9 κ x (y β) i ))) ⟩
                        stepL (λ β → MultL κ (mapL κ (λ ys → stepL (λ α → distlawLcL κ (x α ∷ ys))) (y β))) ∎

multlawLcL2 : {A : Set} (κ : Cl) → ∀(xs : List (myLift (myLift A κ) κ)) → distlawLcL κ (map (MultL κ) xs) ≡
                                     MultL κ (mapL κ (distlawLcL κ) (distlawLcL κ xs))
multlawLcL2 κ [] = refl
multlawLcL2 κ (nowL (nowL x) ∷ xs) = distlawLcL κ ((nowL x) ∷ map (MultL κ) xs)
                                        ≡⟨ refl ⟩
                                        mapL κ (λ ys → x ∷ ys) (distlawLcL κ (map (MultL κ) xs))
                                        ≡⟨ cong (mapL κ (λ ys → x ∷ ys)) (multlawLcL2 κ xs) ⟩
                                        mapL κ (λ ys → x ∷ ys) (MultL κ (mapL κ (distlawLcL κ) (distlawLcL κ xs)))
                                        ≡⟨ MultMap κ (mapL κ (distlawLcL κ) (distlawLcL κ xs)) (λ ys → x ∷ ys)  ⟩
                                        MultL κ  (mapL κ (mapL κ (λ ys → x ∷ ys)) (mapL κ (distlawLcL κ) (distlawLcL κ xs)) )
                                        ≡⟨ cong (MultL κ) (mapmapL κ ((distlawLcL κ)) (mapL κ (λ ys → x ∷ ys)) ((distlawLcL κ xs))) ⟩
                                        MultL κ (mapL κ (λ ys → mapL κ (λ zs → x ∷ zs) (distlawLcL κ ys)) (distlawLcL κ xs))
                                        ≡⟨ refl ⟩
                                        MultL κ (mapL κ (λ ys → (distlawLcL κ) ((nowL x) ∷ ys)) (distlawLcL κ xs))
                                        ≡⟨ cong (MultL κ) (sym (mapmapL κ ((λ ys → (nowL x) ∷ ys)) ((distlawLcL κ)) ((distlawLcL κ xs)))) ⟩
                                        MultL κ (mapL κ (distlawLcL κ) (mapL κ (λ ys → (nowL x) ∷ ys) (distlawLcL κ xs))) ∎
multlawLcL2 κ (nowL (stepL x) ∷ xs) = distlawLcL κ ((stepL x) ∷ map (MultL κ) xs)
                                        ≡⟨ refl ⟩
                                        stepL (λ α → distlawLcL κ (x α ∷ map (MultL κ) xs))
                                        ≡⟨ refl ⟩
                                        stepL (λ α → distlawLcL κ (map (MultL κ) ((nowL (x α)) ∷ xs)))
                                        ≡⟨ (\ i → stepL (\ α → multlawLcL2 κ (((nowL (x α)) ∷ xs)) i )) ⟩
                                        stepL (λ α → MultL κ (mapL κ (distlawLcL κ) (distlawLcL κ ((nowL (x α) ∷ xs)))) )
                                        ≡⟨ refl ⟩
                                        MultL κ (stepL (λ α → (mapL κ (distlawLcL κ) (distlawLcL κ ((nowL (x α) ∷ xs))))))
                                        ≡⟨ refl ⟩
                                        MultL κ (stepL (λ α → (mapL κ (distlawLcL κ) (mapL κ (λ ys → x α ∷ ys) (distlawLcL κ xs)))))
                                        ≡⟨ cong (MultL κ) ((λ i → stepL (\ α → (mapmapL κ ((λ ys → x α ∷ ys)) ((distlawLcL κ)) ((distlawLcL κ xs))) i ))) ⟩
                                        MultL κ (stepL (λ α → (mapL κ (λ ys → distlawLcL κ (x α ∷ ys)) (distlawLcL κ xs))))
                                        ≡⟨ lemma9 κ x (distlawLcL κ xs) ⟩
                                        MultL κ (mapL κ (λ ys → stepL (λ α → distlawLcL κ (x α ∷ ys))) (distlawLcL κ xs))
                                        ≡⟨ refl ⟩
                                        MultL κ (mapL κ (λ ys → (distlawLcL κ) ((stepL x) ∷ ys)) (distlawLcL κ xs))
                                        ≡⟨ cong (MultL κ) (sym (mapmapL κ ((λ ys → (stepL x) ∷ ys)) ((distlawLcL κ)) ((distlawLcL κ xs)))) ⟩
                                        MultL κ (mapL κ (distlawLcL κ) (mapL κ (λ ys → (stepL x) ∷ ys) (distlawLcL κ xs))) ∎
multlawLcL2 κ (stepL x ∷ xs) = (\ i → stepL (\ α → multlawLcL2 κ ((x α ∷ xs)) i ))

-- Bonusmaterial:

-- we define a union on LcL.
_l∪l_ : {A : Set} {κ : Cl} → (LcL A κ) → (LcL A κ) → (LcL A κ)
nowL x l∪l nowL y = nowL (x ++ y)
nowL x l∪l stepL y = stepL (\ α → (nowL x l∪l (y α)))
stepL x l∪l y = stepL (\ α → ((x α) l∪l y))

--nowL [] is a unit for l∪l
left-unitl∪l : {A : Set} {κ : Cl} → ∀(x : LcL A κ) → (nowL []) l∪l x ≡ x
left-unitl∪l (nowL x) = refl
left-unitl∪l (stepL x) = stepL (λ α → nowL [] l∪l x α)
                    ≡⟨ ((\ i → stepL (\ α → left-unitl∪l (x α) i ))) ⟩
                    stepL (λ α → x α)
                    ≡⟨ refl ⟩
                    stepL x ∎

right-unitl∪l : {A : Set} {κ : Cl} → ∀(x : LcL A κ) → x l∪l (nowL []) ≡ x
right-unitl∪l (nowL x) = cong nowL (++-unit-r x)
right-unitl∪l (stepL x) = stepL (λ α →  x α l∪l nowL [])
                    ≡⟨ ((\ i → stepL (\ α → right-unitl∪l (x α) i ))) ⟩
                    stepL (λ α → x α)
                    ≡⟨ refl ⟩
                    stepL x ∎

--mapL κ f distributes over l∪l if f distributes over ++
dist-mapL-l∪l : {A B : Set} (κ : Cl) → ∀(f : (List A) → (List B)) → ∀(fcom : ∀(xs : List A) → ∀(ys : List A) → f (xs ++ ys) ≡ f xs ++ f ys) →
                                ∀(x : (LcL A κ)) → ∀(y : LcL A κ) →  mapL κ f (x l∪l y) ≡ (mapL κ f x) l∪l (mapL κ f y)
dist-mapL-l∪l κ f fcom (nowL x) (nowL y) = cong nowL (fcom x y)
dist-mapL-l∪l κ f fcom (nowL x) (stepL y) = (\ i → stepL (\ α → dist-mapL-l∪l κ f fcom (nowL x) (y α) i ))
dist-mapL-l∪l κ f fcom (stepL x) y  = \ i → stepL (\ α → dist-mapL-l∪l κ f fcom (x α) y i )

max_stars_repo_name: Saizan/Agda-proofs

max_issues_repo_name: Saizan/Agda-proofs

max_forks_repo_name: Saizan/Agda-proofs


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

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

module Categories.Functor.Definition where

record Functor {a b c d : _} (C : Category {a} {b}) (D : Category {c} {d}) : Set (a ⊔ b ⊔ c ⊔ d) where
  field
    onObj : Category.objects C → Category.objects D
    onArrow : {S T : Category.objects C} → Category.arrows C S T → Category.arrows D (onObj S) (onObj T)
    mapId : {T : Category.objects C} → onArrow (Category.id C T) ≡ Category.id D (onObj T)
    mapCompose : {X Y Z : Category.objects C} → (f : Category.arrows C X Y) (g : Category.arrows C Y Z) → onArrow (Category._∘_ C g f) ≡ Category._∘_ D (onArrow g) (onArrow f)


text:
module Stuck where

postulate
  I   : Set
  i j : I

data D : I → I → Set where
  d : D i i
  e : D j j

f : ∀ {x} → D i x → Set₁
f d = Set


text:
module SetOmega where

postulate
  IsType : ∀ {a} → Set a → Set
  Bad    : IsType (∀ a → Set a)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Builtin.Bool

data Test : Set where
  CTest : Bool -> {Bool} -> Test
{-# COMPILE AGDA2HS Test #-}

getTest : Test → Bool
getTest (CTest b) = b
{-# COMPILE AGDA2HS getTest #-}

putTest : Bool → Test → Test
putTest b (CTest _ {b'}) = CTest b {b'}
{-# COMPILE AGDA2HS putTest #-}


text:
open import Relation.Binary.Core using (Rel)

module GGT.Definitions
  {a b ℓ₁ ℓ₂}
  {G : Set a}      -- The underlying group carrier
  {Ω : Set b}      -- The underlying space
  (_≈_ : Rel G ℓ₁) -- The underlying group equality
  (_≋_ : Rel Ω ℓ₂) -- The underlying space equality
  where

open import Level
open import Algebra.Core
open import Relation.Unary
open import Algebra.Bundles using (Group)
open import Algebra.Definitions _≋_ using (Congruent₁)

ActAssoc : Opᵣ G Ω → Op₂ G → Set _
ActAssoc _·_ _∙_ = ∀ (o : Ω) (g : G) (h : G) → (o · (g ∙ h)) ≋ ((o · g) · h)

ActLeftIdentity : G → Opᵣ G Ω → Set _
ActLeftIdentity ε _·_ = ∀ (o : Ω) → (o · ε) ≋ o

·-≋-Congruence : Opᵣ G Ω → Set _
·-≋-Congruence _·_ = ∀ (g : G) → Congruent₁ (_· g)
-- ∀ (o1 o2 : Ω) (g : G) → o1 ≋ o2 → (o1 · g) ≋ (o2 · g)

≈-Ext : Opᵣ G Ω → Set _
≈-Ext _·_ = ∀ {g h : G} → ∀ {o : Ω} → g ≈ h → (o · g) ≋ (o · h)

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt