text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Cones where

open import Relation.Binary using (Rel ; IsEquivalence ; _Preserves₂_⟶_⟶_)
open import Level using (_⊔_)

open import Cats.Category.Base
open import Cats.Category.Cat using (Cat)
open import Cats.Category.Fun as Fun using (Fun ; Trans)
open import Cats.Functor using (Functor) renaming (_∘_ to _∘F_)
open import Cats.Util.Conv

import Relation.Binary.PropositionalEquality as ≡

import Cats.Category.Constructions.Iso as Iso
import Cats.Util.Function as Fun

open Functor
open Trans
open Fun._≈_

module Build {lo la l≈ lo′ la′ l≈′}
  {J : Category lo la l≈}
  {Z : Category lo′ la′ l≈′}
  (D : Functor J Z)
  where

  infixr 9 _∘_
  infixr 4 _≈_

  private
    module Z = Category Z
    module J = Category J
    module D = Functor D

  -- We could define cones in terms of wedges (and limits in terms of ends).
  record Cone : Set (lo ⊔ la ⊔ la′ ⊔ lo′ ⊔ l≈′) where
    field
      Apex : Z.Obj
      arr : ∀ j → Apex Z.⇒ D.fobj j
      commute : ∀ {i j} (α : i J.⇒ j) → arr j Z.≈ D.fmap α Z.∘ arr i

  open Cone public

  instance
    HasObj-Cone : HasObj Cone lo′ la′ l≈′
    HasObj-Cone = record { Cat = Z ; _ᴼ = Cone.Apex }

  Obj = Cone

  record _⇒_ (A B : Obj) : Set (lo ⊔ la′ ⊔ l≈′) where
    private
      module A = Cone A ; module B = Cone B

    field
      arr : A.Apex Z.⇒ B.Apex
      commute : ∀ j → B.arr j Z.∘ arr Z.≈ A.arr j

  open _⇒_ public

  instance
    HasArrow-⇒ : ∀ {A B} → HasArrow (A ⇒ B) lo′ la′ l≈′
    HasArrow-⇒ = record { Cat = Z ; _⃗ = _⇒_.arr }

  _≈_ : ∀ {A B} → Rel (A ⇒ B) l≈′
  _≈_ = Z._≈_ Fun.on arr

  equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
  equiv = Fun.on-isEquivalence _⇒_.arr Z.equiv

  id : ∀ {A} → A ⇒ A
  id = record
      { arr = Z.id
      ; commute = λ j → Z.id-r
      }

  _∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C
  _∘_ {A} {B} {C} f g = record
      { arr = f ⃗ Z.∘ g ⃗
      ; commute = λ j →
          begin
            arr C j Z.∘ f ⃗ Z.∘ g ⃗
          ≈⟨ Z.unassoc ⟩
            (arr C j Z.∘ f ⃗) Z.∘ g ⃗
          ≈⟨ Z.∘-resp-l (commute f j) ⟩
            arr B j Z.∘ g ⃗
          ≈⟨ commute g j ⟩
            arr A j
          ∎
      }
    where
      open Z.≈-Reasoning

  Cones : Category (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′) (lo ⊔ la′ ⊔ l≈′) l≈′
  Cones = record
      { Obj = Obj
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = _∘_
      ; equiv = equiv
      ; ∘-resp = Z.∘-resp
      ; id-r = Z.id-r
      ; id-l = Z.id-l
      ; assoc = Z.assoc
      }

  open Iso.Build Cones using (_≅_)
  open Iso.Build Z using () renaming (_≅_ to _≅Z_)

  cone-iso→obj-iso : ∀ {c d : Cone}
    → c ≅ d
    → c ᴼ ≅Z d ᴼ
  cone-iso→obj-iso i = record
      { forth = forth i ⃗
      ; back = back i ⃗
      ; back-forth = back-forth i
      ; forth-back = forth-back i
      }
    where
      open _≅_

open Build public hiding (HasObj-Cone ; HasArrow-⇒)

private
  open module Build′ {lo la l≈ lo′ la′ l≈′}
    {J : Category lo la l≈}
    {Z : Category lo′ la′ l≈′}
    {D : Functor J Z}
    = Build D
    public using (HasObj-Cone ; HasArrow-⇒)

-- TODO better name
apFunctor : ∀ {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″}
  → {Y : Category lo la l≈}
  → {Z : Category lo′ la′ l≈′}
  → (F : Functor Y Z)
  → {J : Category lo″ la″ l≈″}
  → {D : Functor J Y}
  → Cone D
  → Cone (F ∘F D)
apFunctor {Y = Y} {Z} F {J} {D} c = record
    { Apex = fobj F (c .Apex)
    ; arr = λ j → fmap F (c .arr j)
    ; commute = λ {i} {j} α → Z.≈.sym (
        begin
          fmap F (fmap D α) Z.∘ fmap F (c .arr i)
        ≈⟨ fmap-∘ F ⟩
          fmap F (fmap D α Y.∘ c .arr i)
        ≈⟨ fmap-resp F (Y.≈.sym (c .commute α)) ⟩
          fmap F (c .arr j)
        ∎
      )
    }
  where
    module Y = Category Y
    module Z = Category Z
    open Z.≈-Reasoning

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  where

  module D = Category D

  trans : {F G : Functor C D} → Trans F G → Cone F → Cone G
  trans {F} {G} θ c = record
    { Apex = c .Apex
    ; arr = λ j → component θ j D.∘ c .arr j
    ; commute = λ {i} {j} α →
      let open D.≈-Reasoning in
      begin
      component θ j D.∘ c .arr j
      ≈⟨ D.∘-resp-r (c .commute α) ⟩
      component θ j D.∘ fmap F α D.∘ c .arr i
      ≈⟨ D.unassoc ⟩
      (component θ j D.∘ fmap F α) D.∘ c .arr i
      ≈⟨ D.∘-resp-l (natural θ) ⟩
      (fmap G α D.∘ component θ i) D.∘ c .arr i
      ≈⟨ D.assoc ⟩
      fmap G α D.∘ component θ i D.∘ c .arr i
      ∎
    }

  ConesF : Functor (Fun C D) (Cat (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′) (lo ⊔ la′ ⊔ l≈′) l≈′)
  ConesF = record
    { fobj = Cones
    ; fmap = λ {F} {G} ϑ → record
      { fobj = λ c → trans ϑ c
      ; fmap = λ f → record
        { arr = f .arr
        ; commute = λ j → D.≈.trans D.assoc (D.∘-resp-r (commute f j))
        }
      ; fmap-resp = λ x → x
      ; fmap-id = D.≈.refl
      ; fmap-∘ = D.≈.refl
      }
    ; fmap-resp = λ ϑ≈ι → record
      { iso = record
        { forth = record
          { arr = D.id
          ; commute = λ j → D.≈.trans D.id-r (D.∘-resp-l (D.≈.sym (≈-elim ϑ≈ι)))
          }
        ; back = record
          { arr = D.id
          ; commute = λ j → D.≈.trans D.id-r (D.∘-resp-l (≈-elim ϑ≈ι))
          }
        ; back-forth = D.id-l
        ; forth-back = D.id-l
        }
      ; forth-natural = D.≈.trans D.id-l (D.≈.sym D.id-r)
      }
    ; fmap-id = record
      { iso = record
        { forth = record
          { arr = D.id
          ; commute = λ j → D.≈.trans D.id-r (D.≈.sym D.id-l)
          }
        ; back = record
          { arr = D.id
          ; commute = λ j → D.≈.trans D.id-r D.id-l
          }
        ; back-forth = D.id-l
        ; forth-back = D.id-l
        }
      ; forth-natural = D.≈.trans D.id-l (D.≈.sym D.id-r)
      }
    ; fmap-∘ = record
      { iso = record
        { forth = record
          { arr = D.id
          ; commute = λ j → D.≈.trans D.id-r D.assoc
          }
        ; back = record
          { arr = D.id
          ; commute = λ j → D.≈.trans D.id-r D.unassoc
          }
        ; back-forth = D.id-l
        ; forth-back = D.id-l
        }
      ; forth-natural = D.≈.trans D.id-l (D.≈.sym D.id-r)
      }
    }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.QuoInt where

open import Cubical.HITs.Ints.QuoInt.Base public

open import Cubical.HITs.Ints.QuoInt.Properties public

ext: agda

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:
-- Andreas, 2019-09-13, AIM XXX, test for #4050 by gallais

record Wrap : Set₂ where
  field wrapped : Set₁

f : Wrap
f = record { M }
  module M where
    wrapped : Set₁
    wrapped = Set

-- Should be accepted.

max_stars_repo_name: strake/agda

max_issues_repo_name: strake/agda

max_forks_repo_name: strake/agda


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

module Cubical.Categories.Instances.Sets where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation

open import Cubical.Categories.Limits

open Category

module _ ℓ where
  SET : Category (ℓ-suc ℓ) ℓ
  ob SET = hSet ℓ
  Hom[_,_] SET (A , _) (B , _) = A → B
  id SET x = x
  _⋆_ SET f g x = g (f x)
  ⋆IdL SET f = refl
  ⋆IdR SET f = refl
  ⋆Assoc SET f g h = refl
  isSetHom SET {A} {B} = isSetΠ (λ _ → snd B)

private
  variable
    ℓ ℓ' : Level

open Functor

-- Hom functors
_[-,_] : (C : Category ℓ ℓ') → (c : C .ob) → Functor (C ^op) (SET ℓ')
(C [-, c ]) .F-ob x    = (C [ x , c ]) , C .isSetHom
(C [-, c ]) .F-hom f k = f ⋆⟨ C ⟩ k
(C [-, c ]) .F-id      = funExt λ _ → C .⋆IdL _
(C [-, c ]) .F-seq _ _ = funExt λ _ → C .⋆Assoc _ _ _

_[_,-] : (C : Category ℓ ℓ') → (c : C .ob)→ Functor C (SET ℓ')
(C [ c ,-]) .F-ob x    = (C [ c , x ]) , C .isSetHom
(C [ c ,-]) .F-hom f k = k ⋆⟨ C ⟩ f
(C [ c ,-]) .F-id      = funExt λ _ → C .⋆IdR _
(C [ c ,-]) .F-seq _ _ = funExt λ _ → sym (C .⋆Assoc _ _ _)

module _ {C : Category ℓ ℓ'} {F : Functor C (SET ℓ')} where
  open NatTrans

  -- natural transformations by pre/post composition
  preComp : {x y : C .ob}
          → (f : C [ x , y ])
          → C [ x ,-] ⇒ F
          → C [ y ,-] ⇒ F
  preComp f α .N-ob c k = (α ⟦ c ⟧) (f ⋆⟨ C ⟩ k)
  preComp f α .N-hom {x = c} {d} k
    = (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ (l ⋆⟨ C ⟩ k)))
    ≡[ i ]⟨ (λ l → (α ⟦ d ⟧) (⋆Assoc C f l k (~ i))) ⟩
      (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ l ⋆⟨ C ⟩ k))
    ≡[ i ]⟨ (λ l → (α .N-hom k) i (f ⋆⟨ C ⟩ l)) ⟩
      (λ l → (F ⟪ k ⟫) ((α ⟦ c ⟧) (f ⋆⟨ C ⟩ l)))
    ∎

-- properties
-- TODO: move to own file
open CatIso renaming (inv to cInv)
open Iso

module _ {A B : (SET ℓ) .ob } where

  Iso→CatIso : Iso (fst A) (fst B)
             → CatIso (SET ℓ) A B
  Iso→CatIso is .mor = is .fun
  Iso→CatIso is .cInv = is .inv
  Iso→CatIso is .sec = funExt λ b → is .rightInv b -- is .rightInv
  Iso→CatIso is .ret = funExt λ b → is .leftInv b -- is .rightInv

  CatIso→Iso : CatIso (SET ℓ) A B
             → Iso (fst A) (fst B)
  CatIso→Iso cis .fun = cis .mor
  CatIso→Iso cis .inv = cis .cInv
  CatIso→Iso cis .rightInv = funExt⁻ λ b → cis .sec b
  CatIso→Iso cis .leftInv = funExt⁻ λ b → cis .ret b

  Iso-Iso-CatIso : Iso (Iso (fst A) (fst B)) (CatIso (SET ℓ) A B)
  fun Iso-Iso-CatIso = Iso→CatIso
  inv Iso-Iso-CatIso = CatIso→Iso
  rightInv Iso-Iso-CatIso b = refl
  fun (leftInv Iso-Iso-CatIso a i) = fun a
  inv (leftInv Iso-Iso-CatIso a i) = inv a
  rightInv (leftInv Iso-Iso-CatIso a i) = rightInv a
  leftInv (leftInv Iso-Iso-CatIso a i) = leftInv a

  Iso-CatIso-≡ : Iso (CatIso (SET ℓ) A B) (A ≡ B)
  Iso-CatIso-≡ = compIso (invIso Iso-Iso-CatIso) (hSet-Iso-Iso-≡ _ _)

-- SET is univalent

isUnivalentSET : isUnivalent {ℓ' = ℓ} (SET _)
isUnivalent.univ isUnivalentSET (A , isSet-A) (B , isSet-B)  =
   precomposesToId→Equiv
      pathToIso _ (funExt w) (isoToIsEquiv Iso-CatIso-≡)
   where
     w : _
     w ci =
       invEq
         (congEquiv (isoToEquiv (invIso Iso-Iso-CatIso)))
         (SetsIso≡-ext isSet-A isSet-B
            (λ x i → transp (λ _ → B) i (ci .mor  (transp (λ _ → A) i x)))
            (λ x i → transp (λ _ → A) i (ci .cInv (transp (λ _ → B) i x))))

-- SET is complete

open LimCone
open Cone

completeSET : ∀ {ℓJ ℓJ'} → Limits {ℓJ} {ℓJ'} (SET (ℓ-max ℓJ ℓJ'))
lim (completeSET J D) = Cone D (Unit* , isOfHLevelLift 2 isSetUnit) , isSetCone D _
coneOut (limCone (completeSET J D)) j e = coneOut e j tt*
coneOutCommutes (limCone (completeSET J D)) j i e = coneOutCommutes e j i tt*
univProp (completeSET J D) c cc =
  uniqueExists
    (λ x → cone (λ v _ → coneOut cc v x) (λ e i _ → coneOutCommutes cc e i x))
    (λ _ → funExt (λ _ → refl))
    (λ x → isPropIsConeMor cc (limCone (completeSET J D)) x)
    (λ x hx → funExt (λ d → cone≡ λ u → funExt (λ _ → sym (funExt⁻ (hx u) d))))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Inductive.Examples.Empty where

open import Inductive
open import Tuple

open import Data.Fin
open import Data.Product
open import Data.List
open import Data.Vec

⊥ : Set
⊥ = Inductive []

contradiction : {A : Set} → ⊥ → A
contradiction = rec []

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


text:
module CS410-Prelude where

open import Agda.Primitive

----------------------------------------------------------------------------
-- Zero -- the empty type (logically, a false proposition)
----------------------------------------------------------------------------

data Zero : Set where

magic : forall {l}{A : Set l} -> Zero -> A
magic ()

----------------------------------------------------------------------------
-- One -- the type with one value (logically, a true proposition)
----------------------------------------------------------------------------

record One : Set where
  constructor <>
open One public
{-# COMPILED_DATA One () () #-}

----------------------------------------------------------------------------
-- Two -- the type of Boolean values
----------------------------------------------------------------------------

data Two : Set where tt ff : Two
{-# BUILTIN BOOL Two #-}
{-# BUILTIN TRUE tt #-}
{-# BUILTIN FALSE ff #-}
{-# COMPILED_DATA Two Bool True False #-}

-- nondependent conditional with traditional syntax
if_then_else_ : {l : Level}{X : Set l} -> Two -> X -> X -> X
if tt then t else e = t
if ff then t else e = e

-- dependent conditional cooked for partial application
caseTwo : forall {l}{P : Two -> Set l} -> P tt -> P ff -> (b : Two) -> P b
caseTwo t f tt = t
caseTwo t f ff = f

----------------------------------------------------------------------------
-- "Sigma" -- the type of dependent pairs, giving binary products and sums
----------------------------------------------------------------------------

record Sg {l : Level}(S : Set l)(T : S -> Set l) : Set l where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg public
_*_ : {l : Level} -> Set l -> Set l -> Set l
S * T = Sg S \ _ -> T
infixr 4 _,_ _*_

_+_ : Set -> Set -> Set
S + T = Sg Two (caseTwo S T)

pattern inl s = tt , s
pattern inr t = ff , t

----------------------------------------------------------------------------
-- "Equality" -- the type of evidence that things are the same
----------------------------------------------------------------------------

data _==_ {l}{X : Set l}(x : X) : X -> Set l where
  refl : x == x
infix 1 _==_
{-# BUILTIN EQUALITY _==_ #-}
{-# BUILTIN REFL refl #-}

sym : forall {l}{X : Set l}{x y : X} -> x == y -> y == x
sym refl = refl

-- this proof principle is useful for proving laws, don't use it for
-- fixing type problems in your programs

postulate ext : forall {l m}{A : Set l}{B : Set m}{f g : A -> B} ->
            (forall a -> f a == g a) -> f == g

----------------------------------------------------------------------------
-- functional plumbing
----------------------------------------------------------------------------

id : forall {l}{X : Set l} -> X -> X
id x = x

-- the type of composition can be generalized further
_o_ : forall {l}{X Y Z : Set l} -> (Y -> Z) -> (X -> Y) -> X -> Z
(f o g) x = f (g x)

_$_ : forall{l}{X Y : Set l} -> (X -> Y) -> X -> Y
f $ x = f x

----------------------------------------------------------------------------
-- lists
----------------------------------------------------------------------------

data List (X : Set) : Set where  -- X scopes over the whole declaration...
  []    : List X                 -- ...so you can use it here...
  _::_  : X -> List X -> List X  -- ...and here.
infixr 3 _::_
{-# COMPILED_DATA List [] [] (:) #-}
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _::_ #-}

----------------------------------------------------------------------------
-- chars and strings
----------------------------------------------------------------------------

postulate       -- this means that we just suppose the following things exist...
  Char : Set
  String : Set
{-# BUILTIN CHAR Char #-}
{-# COMPILED_TYPE Char Char #-}      -- ...and by the time we reach Haskell...
{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}  -- ...they *do* exist!

primitive       -- these are baked in; they even work!
  primCharEquality    : Char -> Char -> Two
  primStringAppend    : String -> String -> String
  primStringToList    : String -> List Char
  primStringFromList  : List Char -> String

---------------------------------------------------------------------------
-- COLOURS
---------------------------------------------------------------------------

-- We're going to be making displays from coloured text.

data Colour : Set where
  black red green yellow blue magenta cyan white : Colour
{-# COMPILED_DATA Colour HaskellSetup.Colour
      HaskellSetup.Black HaskellSetup.Red HaskellSetup.Green
      HaskellSetup.Yellow HaskellSetup.Blue HaskellSetup.Magenta
      HaskellSetup.Cyan HaskellSetup.White #-}


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Graph.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

private variable ℓv ℓv' ℓv'' ℓe ℓe' ℓe'' ℓd ℓd' : Level

-- The type of directed multigraphs (with loops)

record Graph ℓv ℓe : Type (ℓ-suc (ℓ-max ℓv ℓe)) where
  field
    Obj : Type ℓv
    Hom : Obj → Obj → Type ℓe

open Graph public

_ᵒᵖ : Graph ℓv ℓe → Graph ℓv ℓe
Obj (G ᵒᵖ) = Obj G
Hom (G ᵒᵖ) x y = Hom G y x

TypeGr : ∀ ℓ → Graph (ℓ-suc ℓ) ℓ
Obj (TypeGr ℓ) = Type ℓ
Hom (TypeGr ℓ) A B = A → B

-- Graph functors/homomorphisms

record GraphHom (G  : Graph ℓv  ℓe ) (G' : Graph ℓv' ℓe')
                : Type (ℓ-suc (ℓ-max (ℓ-max ℓv ℓe) (ℓ-max ℓv' ℓe'))) where
  field
    _$_ : Obj G → Obj G'
    _<$>_ : ∀ {x y : Obj G} → Hom G x y → Hom G' (_$_ x) (_$_ y)

open GraphHom public

GraphGr : ∀ ℓv ℓe → Graph _ _
Obj (GraphGr ℓv ℓe) = Graph ℓv ℓe
Hom (GraphGr ℓv ℓe) G G' = GraphHom G G'

-- Diagrams are (graph) functors with codomain Type

Diag : ∀ ℓd (G : Graph ℓv ℓe) → Type (ℓ-suc (ℓ-max (ℓ-max ℓv ℓe) (ℓ-suc ℓd)))
Diag ℓd G = GraphHom G (TypeGr ℓd)

record DiagMor {G : Graph ℓv ℓe} (F : Diag ℓd G) (F' : Diag ℓd' G)
               : Type (ℓ-suc (ℓ-max (ℓ-max ℓv ℓe) (ℓ-suc (ℓ-max ℓd ℓd')))) where
  field
    nat : ∀ (x : Obj G) → F $ x → F' $ x
    comSq : ∀ {x y : Obj G} (f : Hom G x y) → nat y ∘ F <$> f ≡ F' <$> f ∘ nat x

open DiagMor public

DiagGr : ∀ ℓd (G : Graph ℓv ℓe) → Graph _ _
Obj (DiagGr ℓd G) = Diag ℓd G
Hom (DiagGr ℓd G) = DiagMor


text:
-- Andreas, 2017-12-16, issue #2871

-- If there is nothing to result-split, introduce trailing hidden args.

-- {-# OPTIONS -v interaction.case:40 #-}

data Fun (A : Set) : Set where
  mkFun : (A → A) → Fun A

test : ∀ {A : Set} → Fun A
test = {!!}  -- C-c C-x C-h C-c C-c RET

-- Works also with C-c C-c RET
--
-- Expected:
-- test {A} = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Delta-observational equivalence - base definitions
------------------------------------------------------------------------
module Base.Change.Equivalence.Base where

open import Relation.Binary.PropositionalEquality
open import Base.Change.Algebra
open import Function

module _ {a} {A : Set a} {{ca : ChangeAlgebra A}} {x : A} where
  -- Delta-observational equivalence: these asserts that two changes
  -- give the same result when applied to a base value.

  -- To avoid unification problems, use a one-field record (a Haskell "newtype")
  -- instead of a "type synonym".
  record _≙_ (dx dy : Δ x) : Set a where
    -- doe = Delta-Observational Equivalence.
    constructor doe
    field
      proof : x ⊞ dx ≡ x ⊞ dy

  open _≙_ public

  -- Same priority as ≡
  infix 4 _≙_

  open import Relation.Binary

  -- _≙_ is indeed an equivalence relation:
  ≙-refl : ∀ {dx} → dx ≙ dx
  ≙-refl = doe refl

  ≙-sym : ∀ {dx dy} → dx ≙ dy → dy ≙ dx
  ≙-sym ≙ = doe $ sym $ proof ≙

  ≙-trans : ∀ {dx dy dz} → dx ≙ dy → dy ≙ dz → dx ≙ dz
  ≙-trans ≙₁ ≙₂ = doe $ trans (proof ≙₁) (proof ≙₂)

  -- That's standard congruence applied to ≙
  ≙-cong  : ∀ {b} {B : Set b}
       (f : A → B) {dx dy} → dx ≙ dy → f (x ⊞ dx) ≡ f (x ⊞ dy)
  ≙-cong f da≙db = cong f $ proof da≙db

  ≙-isEquivalence : IsEquivalence (_≙_)
  ≙-isEquivalence = record
    { refl  = ≙-refl
    ; sym   = ≙-sym
    ; trans = ≙-trans
    }

  ≙-setoid : Setoid a a
  ≙-setoid = record
    { Carrier       = Δ x
    ; _≈_           = _≙_
    ; isEquivalence = ≙-isEquivalence
    }

≙-syntax : ∀ {a} {A : Set a} {{ca : ChangeAlgebra A}} (x : A) (dx₁ dx₂ : Δ x) → Set a
≙-syntax x dx₁ dx₂ = _≙_ {x = x} dx₁ dx₂
syntax ≙-syntax x dx₁ dx₂ = dx₁ ≙₍ x ₎ dx₂

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

module Data.List.Kleene.Membership where

open import Prelude
open import Data.List.Kleene
open import Data.List.Kleene.Relation.Unary

infixr 5 _∈⋆_ _∈⁺_ _∉⋆_ _∉⁺_

_∈⋆_ _∉⋆_ : A → A ⋆ → Type _
x ∈⋆ xs = ◇⋆ (_≡ x) xs
x ∉⋆ xs = ¬ (x ∈⋆ xs)

_∈⁺_ _∉⁺_ : A → A ⁺ → Type _
x ∈⁺ xs = ◇⁺ (_≡ x) xs
x ∉⁺ xs = ¬ (x ∈⁺ xs)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Data.Product using ( _,_ )
open import FRP.LTL.ISet.Core using ( ISet ; _⇛_ ; mset ; M⟦_⟧ ; ⟦_⟧ ; [_] ; subsumM⟦_⟧ )
open import FRP.LTL.Time.Interval using ( ⊑-refl )

module FRP.LTL.ISet.Stateless where

infixr 2 _⇒_

_⇒_ : ISet → ISet → ISet
A ⇒ B = mset A ⇛ B

-- We could define $ as
-- f $ σ = i→m (λ j j⊑i → f j j⊑i [ subsumM⟦ A ⟧ j i j⊑i σ ])
-- but we inline i→m for efficiency

_$_ : ∀ {A B i} → M⟦ A ⇒ B ⟧ i → M⟦ A ⟧ i → M⟦ B ⟧ i
_$_ {A} {[ B ]} {i} f σ = f i ⊑-refl [ σ ]
_$_ {A} {B ⇛ C} {i} f σ = λ j j⊑i → f j j⊑i [ subsumM⟦ A ⟧ j i j⊑i σ ]

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


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

open import lib.Base
open import lib.PathGroupoid
open import lib.Relation
open import lib.NType
open import lib.types.Empty

module lib.types.Nat where

infixl 80 _+_
_+_ : ℕ → ℕ → ℕ
0 + n = n
(S m) + n = S (m + n)

{-# BUILTIN NATPLUS _+_ #-}

+-unit-r : (m : ℕ) → m + 0 == m
+-unit-r 0     = idp
+-unit-r (S m) = ap S (+-unit-r m)

+-βr : (m n : ℕ) → m + (S n) == S (m + n)
+-βr 0     n = idp
+-βr (S m) n = ap S (+-βr m n)

+-comm : (m n : ℕ) → m + n == n + m
+-comm m 0     = +-unit-r m
+-comm m (S n) = +-βr m n ∙ ap S (+-comm m n)

+-assoc : (k m n : ℕ) → (k + m) + n == k + (m + n)
+-assoc 0     m n = idp
+-assoc (S k) m n = ap S (+-assoc k m n)

infix 120 _*2
_*2 : ℕ → ℕ
O *2 = O
(S n) *2 = S (S (n *2))

ℕ-pred : ℕ → ℕ
ℕ-pred 0 = 0
ℕ-pred (S n) = n

ℕ-S-inj : (n m : ℕ) (p : S n == S m) → n == m
ℕ-S-inj n m p = ap ℕ-pred p

ℕ-S-≠ : ∀ {n m : ℕ} (p : n ≠ m) → S n ≠ S m
ℕ-S-≠ p = p ∘ ℕ-S-inj _ _

private
  ℕ-S≠O-type : ℕ → Type₀
  ℕ-S≠O-type O = Empty
  ℕ-S≠O-type (S n) = Unit

abstract
  ℕ-S≠O : (n : ℕ) → S n ≠ O
  ℕ-S≠O n p = transport ℕ-S≠O-type p unit

  ℕ-O≠S : (n : ℕ) → (O ≠ S n)
  ℕ-O≠S n p = ℕ-S≠O n (! p)

  ℕ-has-dec-eq : has-dec-eq ℕ
  ℕ-has-dec-eq O O = inl idp
  ℕ-has-dec-eq O (S n) = inr (ℕ-O≠S n)
  ℕ-has-dec-eq (S n) O = inr (ℕ-S≠O n)
  ℕ-has-dec-eq (S n) (S m) with ℕ-has-dec-eq n m
  ℕ-has-dec-eq (S n) (S m) | inl p = inl (ap S p)
  ℕ-has-dec-eq (S n) (S m) | inr p⊥ = inr (λ p → p⊥ (ℕ-S-inj n m p))

  ℕ-is-set : is-set ℕ
  ℕ-is-set = dec-eq-is-set ℕ-has-dec-eq

ℕ-level = ℕ-is-set

{- Inequalities -}
infix 40 _<_ _≤_

data _<_ : ℕ → ℕ → Type₀ where
  ltS : {m : ℕ} → m < (S m)
  ltSR : {m n : ℕ} → m < n → m < (S n)

_≤_ : ℕ → ℕ → Type₀
m ≤ n = Coprod (m == n) (m < n)

-- properties of [<]

instance
  O<S : (m : ℕ) → O < S m
  O<S O = ltS
  O<S (S m) = ltSR (O<S m)

O≤ : (m : ℕ) → O ≤ m
O≤ O = inl idp
O≤ (S m) = inr (O<S m)

≮O : ∀ n → ¬ (n < O)
≮O _ ()

<-trans : {m n k : ℕ} → m < n → n < k → m < k
<-trans lt₁ ltS = ltSR lt₁
<-trans lt₁ (ltSR lt₂) = ltSR (<-trans lt₁ lt₂)

≤-refl : {m : ℕ} → m ≤ m
≤-refl = inl idp

≤-trans : {m n k : ℕ} → m ≤ n → n ≤ k → m ≤ k
≤-trans {k = k} (inl p₁) lte₂ = transport (λ t → t ≤ k) (! p₁) lte₂
≤-trans {m = m} lte₁ (inl p₂) = transport (λ t → m ≤ t) p₂ lte₁
≤-trans (inr lt₁) (inr lt₂) = inr (<-trans lt₁ lt₂)

<-ap-S : {m n : ℕ} → m < n → S m < S n
<-ap-S ltS = ltS
<-ap-S (ltSR lt) = ltSR (<-ap-S lt)

≤-ap-S : {m n : ℕ} → m ≤ n → S m ≤ S n
≤-ap-S (inl p) = inl (ap S p)
≤-ap-S (inr lt) = inr (<-ap-S lt)

<-cancel-S : {m n : ℕ} → S m < S n → m < n
<-cancel-S ltS = ltS
<-cancel-S (ltSR lt) = <-trans ltS lt

≤-cancel-S : {m n : ℕ} → S m ≤ S n → m ≤ n
≤-cancel-S (inl p) = inl (ap ℕ-pred p)
≤-cancel-S (inr lt) = inr (<-cancel-S lt)

<-dec : Decidable _<_
<-dec _     O     = inr (≮O _)
<-dec O     (S m) = inl (O<S m)
<-dec (S n) (S m) with <-dec n m
<-dec (S n) (S m) | inl p  = inl (<-ap-S p)
<-dec (S n) (S m) | inr p⊥ = inr (p⊥ ∘ <-cancel-S)

≯-to-≤ : {m n : ℕ} → ¬ (n < m) → m ≤ n
≯-to-≤ {O} {O} _ = inl idp
≯-to-≤ {O} {S n} _ = inr (O<S n)
≯-to-≤ {S m} {O} neggt = ⊥-elim $ neggt (O<S m)
≯-to-≤ {S m} {S n} neggt = ≤-ap-S (≯-to-≤ (neggt ∘ <-ap-S))

<-+-l : {m n : ℕ} (k : ℕ) → m < n → (k + m) < (k + n)
<-+-l O lt = lt
<-+-l (S k) lt = <-ap-S (<-+-l k lt)

≤-+-l : {m n : ℕ} (k : ℕ) → m ≤ n → (k + m) ≤ (k + n)
≤-+-l k (inl p) = inl (ap (λ t → k + t) p)
≤-+-l k (inr lt) = inr (<-+-l k lt)

<-+-r : {m n : ℕ} (k : ℕ) → m < n → (m + k) < (n + k)
<-+-r k ltS = ltS
<-+-r k (ltSR lt) = ltSR (<-+-r k lt)

≤-+-r : {m n : ℕ} (k : ℕ) → m ≤ n → (m + k) ≤ (n + k)
≤-+-r k (inl p) = inl (ap (λ t → t + k) p)
≤-+-r k (inr lt) = inr (<-+-r k lt)

<-witness : {m n : ℕ} → (m < n) → Σ ℕ (λ k → S k + m == n)
<-witness ltS = (O , idp)
<-witness (ltSR lt) = let w' = <-witness lt in (S (fst w') , ap S (snd w'))

≤-witness : {m n : ℕ} → (m ≤ n) → Σ ℕ (λ k → k + m == n)
≤-witness (inl p) = (O , p)
≤-witness (inr lt) = let w' = <-witness lt in (S (fst w') , snd w')

*2-increasing : (m : ℕ) → (m ≤ m *2)
*2-increasing O = inl idp
*2-increasing (S m) = ≤-trans (≤-ap-S (*2-increasing m)) (inr ltS)

*2-monotone-< : {m n : ℕ} → m < n → m *2 < n *2
*2-monotone-< ltS = ltSR ltS
*2-monotone-< (ltSR lt) = ltSR (ltSR (*2-monotone-< lt))

*2-monotone-≤ : {m n : ℕ} → m ≤ n → m *2 ≤ n *2
*2-monotone-≤ (inl p) = inl (ap _*2 p)
*2-monotone-≤ (inr lt) = inr (*2-monotone-< lt)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; trans)
open Relation.Binary.PropositionalEquality.≡-Reasoning
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (fromWitness)

import Data.Product as Product
import Data.Product.Properties as Productₚ
import Data.Unit as Unit
import Data.Nat as ℕ
import Data.Vec as Vec
import Data.Fin as Fin
import Data.Vec.Relation.Unary.All as All

open Unit using (⊤; tt)
open ℕ using (ℕ; zero; suc)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)
open Fin using (Fin ; zero ; suc)
open Product using (Σ-syntax; _×_; _,_; proj₁; proj₂)

open import PiCalculus.Syntax
open Scoped
open import PiCalculus.Semantics
open import PiCalculus.Semantics.Properties
open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem.SubjectCongruence (Ω : Algebras) where
open Algebras Ω
open import PiCalculus.LinearTypeSystem Ω
open import PiCalculus.LinearTypeSystem.ContextLemmas Ω
open import PiCalculus.LinearTypeSystem.Framing Ω
open import PiCalculus.LinearTypeSystem.Weakening Ω
open import PiCalculus.LinearTypeSystem.Strengthening Ω
open import PiCalculus.LinearTypeSystem.Exchange Ω

SubjectCongruence : Set
SubjectCongruence = {n : ℕ} {γ : PreCtx n} {idxs : Idxs n} {Γ Δ : Ctx idxs}
                  → {r : RecTree} {P Q : Scoped n}
                  → P ≅⟨ r ⟩ Q
                  → γ ； Γ ⊢ P ▹ Δ
                  → γ ； Γ ⊢ Q ▹ Δ

private
  variable
    n : ℕ
    P Q : Scoped n

comp-comm : {γ : PreCtx n} {idxs : Idxs n} {Γ Ξ : Ctx idxs}
          → γ ； Γ ⊢ P ∥ Q ▹ Ξ
          → γ ； Γ ⊢ Q ∥ P ▹ Ξ
comp-comm (⊢P ∥ ⊢Q) with ⊢-⊗ ⊢P | ⊢-⊗ ⊢Q
comp-comm (⊢P ∥ ⊢Q) | _ , P≔ | _ , Q≔ =
  let _ , (Q'≔ , P'≔) = ⊗-assoc (⊗-comm P≔) Q≔ in
  ⊢-frame Q≔ Q'≔ ⊢Q ∥ ⊢-frame P≔ (⊗-comm P'≔) ⊢P

subject-cong : SubjectCongruence
subject-cong (stop comp-assoc) (⊢P ∥ (⊢Q ∥ ⊢R)) = (⊢P ∥ ⊢Q) ∥ ⊢R
subject-cong (stop comp-symm) (⊢P ∥ ⊢Q) = comp-comm (⊢P ∥ ⊢Q)
subject-cong (stop comp-end) (⊢P ∥ 𝟘) = ⊢P
subject-cong (stop scope-end) (ν t c ._ 𝟘) = 𝟘
subject-cong (stop (scope-ext u)) (ν t c μ (_∥_ {Δ = _ -, _} ⊢P ⊢Q)) rewrite sym (⊢-unused _ u ⊢P) = ⊢-strengthen zero u ⊢P ∥ ν t c μ ⊢Q
subject-cong (stop scope-scope-comm) (ν t c μ (ν t₁ c₁ μ₁ ⊢P)) = ν t₁ c₁ μ₁ (ν t c μ (⊢-exchange zero ⊢P))
subject-cong (cong-symm (stop comp-assoc)) ((⊢P ∥ ⊢Q) ∥ ⊢R) = ⊢P ∥ (⊢Q ∥ ⊢R)
subject-cong (cong-symm (stop comp-symm)) (⊢P ∥ ⊢Q) = comp-comm (⊢P ∥ ⊢Q)
subject-cong (cong-symm (stop comp-end)) ⊢P = ⊢P ∥ 𝟘
subject-cong (cong-symm (stop scope-end)) 𝟘 = ν 𝟙 {∃Idx} (0∙ , 0∙) {∃Idx} 0∙ 𝟘
subject-cong (cong-symm (stop (scope-ext u))) (⊢P ∥ (ν t c μ ⊢Q)) = ν t c μ ((subst (λ ● → _ ； _ ⊢ ● ▹ _) (lift-lower zero _ u) (⊢-weaken zero ⊢P)) ∥ ⊢Q)
subject-cong (cong-symm (stop scope-scope-comm)) (ν t c μ (ν t₁ c₁ μ₁ ⊢P)) = ν _ _ _ (ν _ _ _ (subst (λ ● → _ ； _ ⊢ ● ▹ _) (exchange-exchange zero _) (⊢-exchange zero ⊢P)))

-- Equivalence and congruence
subject-cong cong-refl ⊢P = ⊢P
subject-cong (cong-trans P≅Q Q≅R) ⊢P = subject-cong Q≅R (subject-cong P≅Q ⊢P)
subject-cong (ν-cong P≅Q) (ν t m μ ⊢P) = ν t m μ (subject-cong P≅Q ⊢P)
subject-cong (comp-cong P≅Q) (⊢P ∥ ⊢R) = subject-cong P≅Q ⊢P ∥ ⊢R
subject-cong (input-cong P≅Q) (x ⦅⦆ ⊢P) = x ⦅⦆ subject-cong P≅Q ⊢P
subject-cong (output-cong P≅Q) (x ⟨ y ⟩ ⊢P) = x ⟨ y ⟩ subject-cong P≅Q ⊢P
subject-cong (cong-symm cong-refl) ⊢P = ⊢P
subject-cong (cong-symm (cong-symm P≅Q)) ⊢P = subject-cong P≅Q ⊢P
subject-cong (cong-symm cong-trans P≅Q P≅R) ⊢P = subject-cong (cong-symm P≅Q) (subject-cong (cong-symm P≅R) ⊢P)
subject-cong (cong-symm (ν-cong P≅Q)) (ν t m μ ⊢P) = ν t m μ (subject-cong (cong-symm P≅Q) ⊢P)
subject-cong (cong-symm (comp-cong P≅Q)) (⊢P ∥ ⊢R) = subject-cong (cong-symm P≅Q) ⊢P ∥ ⊢R
subject-cong (cong-symm (input-cong P≅Q)) (x ⦅⦆ ⊢P) = x ⦅⦆ subject-cong (cong-symm P≅Q) ⊢P
subject-cong (cong-symm (output-cong P≅Q)) (x ⟨ y ⟩ ⊢P) = x ⟨ y ⟩ subject-cong (cong-symm P≅Q) ⊢P

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
-- We can let Agda infer the parameters of the constructor target

data List (A : Set) : Set where
  nil  : List _
  cons : A → List A → List _

-- 2017-01-12, Andreas: we can even omit the whole target
-- (for parameterized data types, but not inductive families)

data Bool : Set where
  true false : _

data Maybe (A : Set) : Set where
  nothing : _
  just : (x : A) → _

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

This module converts between the path equality
and the inductively define equality types.

- _≡c_ stands for "c"ubical equality.
- _≡p_ stands for "p"ropositional equality.

TODO: reconsider naming scheme.
-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Data.Equality where

open import Cubical.Foundations.Prelude
  renaming ( _≡_ to _≡c_ ; refl to reflc )
  public
open import Agda.Builtin.Equality
  renaming ( _≡_ to _≡p_ ; refl to reflp )
  public

open import Cubical.Foundations.Isomorphism

private
 variable
  ℓ : Level
  A : Type ℓ
  x y z : A

ptoc : x ≡p y → x ≡c y
ptoc reflp = reflc

ctop : x ≡c y → x ≡p y
ctop p = transport (cong (λ u → _ ≡p u) p) reflp

ptoc-ctop : (p : x ≡c y) → ptoc (ctop p) ≡c p
ptoc-ctop p =
  J (λ _ h → ptoc (ctop h) ≡c h) (cong ptoc (transportRefl reflp)) p

ctop-ptoc : (p : x ≡p y) → ctop (ptoc p) ≡c p
ctop-ptoc {x = x} reflp = transportRefl reflp

p≅c : {x y : A} → Iso (x ≡c y) (x ≡p y)
p≅c = iso ctop ptoc ctop-ptoc ptoc-ctop

p-c : {x y : A} → (x ≡c y) ≡c (x ≡p y)
p-c = isoToPath p≅c

p=c : {x y : A} → (x ≡c y) ≡p (x ≡p y)
p=c = ctop p-c


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.Preorder module directly.
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.PreorderReasoning
         {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where

open import Relation.Binary.Reasoning.Preorder P public


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

open import Polynomial.Parameters

-- Here, we provide proofs of homomorphism between the operations
-- defined on polynomials and those on the underlying ring.

module Polynomial.Homomorphism
  {c r₁ r₂ r₃}
  (homo : Homomorphism c r₁ r₂ r₃)
  where

-- The lemmas are the general-purpose proofs we reuse in each other section
open import Polynomial.Homomorphism.Lemmas         homo using (pow-cong) public

-- Proofs which deal with variables and constants
open import Polynomial.Homomorphism.Semantics      homo using (κ-hom; ι-hom) public

-- Proofs for each operation
open import Polynomial.Homomorphism.Addition       homo using (⊞-hom) public
open import Polynomial.Homomorphism.Multiplication homo using (⊠-hom) public
open import Polynomial.Homomorphism.Negation       homo using (⊟-hom) public
open import Polynomial.Homomorphism.Exponentiation homo using (⊡-hom) public

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


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

open import Cubical.Foundations.Everything

open import Cubical.Foundations.SIP
open import Cubical.Structures.Queue

open import Cubical.Data.Maybe
open import Cubical.Data.List
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Data.Queue.1List

-- All finite queues are equal to 1List.Finite

private
  variable
    ℓ : Level

module _ (A : Type ℓ) (Aset : isSet A) where
 open Queues-on A Aset
 private
   module One = 1List A Aset
   open One renaming (Q to Q₁; emp to emp₁; enq to enq₁; deq to deq₁)

 isContrFiniteQueue : isContr FiniteQueue
 isContrFiniteQueue .fst = One.Finite
 isContrFiniteQueue .snd (Q , (S@(emp , enq , deq) , _ , deq-emp , deq-enq , _) , fin) =
   sip finiteQueueUnivalentStr _ _ ((f , fin) , f∘emp , f∘enq , sym ∘ f∘deq)
   where
   deq₁-enq₁ = str One.WithLaws .snd .snd .snd .fst

   f : Q₁ → Q
   f = foldr enq emp

   f∘emp : f emp₁ ≡ emp
   f∘emp = refl

   f∘enq : ∀ a xs → f (enq₁ a xs) ≡ enq a (f xs)
   f∘enq _ _ = refl

   fA : Q₁ × A → Q × A
   fA (q , a) = (f q , a)

   f∘returnOrEnq : (x : A) (xsr : Maybe (List A × A)) →
     returnOrEnq S x (deqMap f xsr) ≡ fA (returnOrEnq (str One.Raw) x xsr)
   f∘returnOrEnq _ nothing = refl
   f∘returnOrEnq _ (just _) = refl

   f∘deq : ∀ xs → deq (f xs) ≡ deqMap f (deq₁ xs)
   f∘deq [] = deq-emp
   f∘deq (x ∷ xs) =
     deq-enq x (f xs)
     ∙ cong (just ∘ returnOrEnq S x) (f∘deq xs)
     ∙ cong just (f∘returnOrEnq x (deq₁ xs))
     ∙ cong (deqMap f) (sym (deq₁-enq₁ x xs))


text:
-- Andreas, 2015-05-28 example by Andrea Vezzosi

open import Common.Size

data Nat (i : Size) : Set where
  zero : ∀ {j : Size< i} → Nat i
  suc  : ∀ {j : Size< i} → Nat j → Nat i

{-# TERMINATING #-}
-- This definition is fine, the termination checker is too strict at the moment.
fix : ∀ {C : Size → Set}
  → (∀{i} → (∀ {j : Size< i} → Nat j -> C j) → Nat i → C i)
  → ∀{i} → Nat i → C i
fix t zero    = t (fix t) zero
fix t (suc n) = t (fix t) (suc n)

case : ∀ {i} {C : Set} (n : Nat i) (z : C) (s : ∀ {j : Size< i} → Nat j → C) → C
case zero    z s = z
case (suc n) z s = s n

applyfix : ∀ {C : Size → Set} {i} (n : Nat i)
  → (∀{i} → (∀ {j : Size< i} → Nat j -> C j) → Nat i → C i)
  → C i
applyfix n f = fix f n

module M (i0 : Size) (bot : ∀{i} → Nat i) (A : Set) (default : A) where

  loops : A
  loops = applyfix (zero {i = ↑ i0}) λ {i} r _ →
      case {i} bot default λ n →   -- Size< i is possibly empty, should be rejected
      case     n   default λ _ →
      r zero

  -- loops
  -- --> fix t zero
  -- --> t (fix t) zero
  -- --> case bot default λ n → case n default λ _ → fix t zero
  -- and we have reproduced (modulo sizes) what we started with


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Weight biased leftist heap that proves to maintain priority      --
-- invariant: priority at the node is not lower than priorities of  --
-- its two children. Uses a two-pass merging algorithm.             --
----------------------------------------------------------------------

{-# OPTIONS --sized-types #-}
module TwoPassMerge.PriorityProof where

open import Basics.Nat renaming (_≥_ to _≥ℕ_)
open import Basics
open import Sized

-- Priority invariant says that: for any node in the tree priority in
-- that node is higher than priority stored by its children. This
-- means that any path from root to leaf is ordered (highest priority
-- at the root, lowest at the leaf). This property allows us to
-- construct an efficient merging operation (see paper for more
-- details).
--
-- To prove this invariant we will index nodes using Priority. Index
-- of value n says that "this heap can store elements with priorities
-- n or lower" (remember that lower priority means larger Nat). In
-- other words Heap indexed with 0 can store any Priority, while Heap
-- indexed with 3 can store priorities 3, 4 and lower, but can't store
-- 0, 1 and 2.
--
-- As previously, Heap has two constructors:
--
--  1) empty returns Heap n, where index n is not constrained in any
--     way. This means that empty heap can be given any restriction on
--     priorities of stored elements.
--
--  2) node also creates Heap n, but this time n is constrained. If we
--     store priority p in a node then:

--       a) the resulting heap can only be restricted to store
--          priorities at least as high as p. For example, if we
--          create a node that stores priority 3 we cannot restrict
--          the resulting heap to store priorities 4 and lower,
--          because the fact that we store 3 in that node violates the
--          restriction. This restriction is expressed by the "p ≥ n"
--          parameter: if we can construct a value of type (p ≥ n)
--          then existance of such a value becomes a proof that p is
--          greater-equal to n. We must supply such proof to every
--          node.

--       b) children of a node can only be restricted to store
--          priorities that are not higher than p. Example: if we
--          restrict a node to store priorities 4 and lower we cannot
--          restrict its children to store priorities 3 and
--          higher. This restriction is expressed by index "p" in the
--          subheaps passed to node constructor.

data Heap : {i : Size} → Priority → Set where
  empty : {i : Size} {n : Priority} → Heap {↑ i} n
  node  : {i : Size} {n : Priority} → (p : Priority) → Rank → p ≥ n →
          Heap {i} p → Heap {i} p → Heap {↑ i} n

-- Let's demonstrate that priority invariant cannot be broken. Below
-- we construct a heap like this:
--
--      ?
--     / \
--    /   \
--   E     0
--
-- where E means empty node and 0 means node storing Priority 0 (yes,
-- this heap violates the rank invariant!). We left out the root
-- element. The only value that can be supplied there is zero (try
-- giving one and see that typechecker will not accept it). This is
-- beacuse the value n with which 0 node can be index must obey the
-- restriction 0 ≥ n. This means that 0 node can only be indexed with
-- 0. When we try to construct ? node we are thus only allowed to
-- insert priority 0.
heap-broken : Heap zero
heap-broken = node {!!} (suc one) ge0 empty (node zero one ge0 empty empty)

-- Here is a correct heap. It stores one at the leaf and 0 at the
-- root. It still violates the rank invariant - we deal with that in
-- TwoPassMerge.RankProof.
heap-correct : Heap zero
heap-correct = node zero (suc one) ge0 empty (node one one ge0 empty empty)

-- Again, we need a function to extract rank from a node
rank : {b : Priority} → Heap b → Rank
rank empty            = zero
rank (node _ r _ _ _) = r

-- The first question is how to create a singleton heap, ie. a Heap
-- storing one element. The question we need to answer is "what
-- Priorities can we later store in a singleton Heap?". "Any" seems to
-- be a reasonable answer. This means the resulting Heap will be
-- indexed with zero, meaning "Priorities lower or equal to zero can
-- be stored in this Heap" (remember that any priority is lower or
-- equal to zero). This leads us to following definition:
singleton : (p : Priority) → Heap zero
singleton p = node p one ge0 empty empty

-- We can imagine we would like to limit the range of priorities we
-- can insert into a singleton Heap. This means the resulting Heap
-- would be index with some b (the bound on allowed Priority
-- values). In such case however we are required to supply a proof
-- that p ≥ b. This would lead us to a definition like this:
--
-- singletonB : {b : Priority} → (p : Priority) → p ≥ b → Heap b
-- singletonB p p≥b = node p one p≥b empty empty
--
-- We'll return to that idea soon.

-- makeT now returns indexed heaps, so it requires one more parameter:
-- a proof that priorities stored in resulting heap are not lower than
-- in the subheaps.
makeT : {b : Nat} → (p : Priority) → p ≥ b → Heap p → Heap p → Heap b
makeT p p≥b l r with rank l ≥ℕ rank r
makeT p p≥b l r | true  = node p (suc (rank l + rank r)) p≥b l r
makeT p p≥b l r | false = node p (suc (rank l + rank r)) p≥b r l

-- The important change in merge is that now we don't compare node
-- priorities using an operator that returns Bool. We compare them
-- using "order" function that not only returns result of comparison,
-- but also supplies a proof of the result. This proof tells us
-- something important about the relationship between p1, p2 and
-- priority bound of the merged Heap. Note that we use the new proof
-- to reconstruct one of the heaps that is passed in recursive call to
-- merge. We must do this because by comparing priorities p1 and p2 we
-- learned something new about restriction placed on priorities in one
-- of the heaps and we can now be more precise in expressing these
-- restrictions.
--
-- Note also that despite indexing our data types with Size the
-- termination checker complains that merge function does not
-- terminate. This is not a problem in our definitions but a bug in
-- Agda's implementation. I leave the code in this form in hope that
-- this bug will be fixed in a future release of Agda. For mor details
-- see http://code.google.com/p/agda/issues/detail?id=59#c23
merge : {i j : Size} {p : Nat} → Heap {i} p → Heap {j} p → Heap p
merge empty h2 = h2
merge h1 empty = h1
merge .{↑ i} .{↑ j}
  (node {i} p1 l-rank p1≥p l1 r1)
  (node {j} p2 r-rank p2≥p l2 r2)
  with order p1 p2
merge .{↑ i} .{↑ j}
  (node {i} p1 l-rank p1≥p l1 r1)
  (node {j} p2 r-rank p2≥p l2 r2)
  | le p1≤p2
  = makeT p1 p1≥p l1 (merge {i} {↑ j} r1 (node p2 r-rank p1≤p2 l2 r2))
merge .{↑ i} .{↑ j}
  (node {i} p1 l-rank p1≥p l1 r1)
  (node {j} p2 r-rank p2≥p l2 r2)
  | ge p1≥p2
  = makeT p2 p2≥p l2 (merge {↑ i} {j} (node p1 l-rank p1≥p2 l1 r1) r2)

-- When writing indexed insert function we once again have to answer a
-- question of how to index input and output Heap. The easiest
-- solution is to be liberal: let us require that the input and output
-- Heap have no limitations on Priorities they can store. In other
-- words, let they be indexed by zero:
insert : Priority → Heap zero → Heap zero
insert p h = merge (singleton p) h

-- Now we can create an example heap. The only difference between this
-- heap and the heap without any proofs is that we need to explicitly
-- instantiate implicit Priority parameter of empty constructor.
heap : Heap zero
heap = insert (suc (suc zero))
      (insert (suc zero)
      (insert zero
      (insert (suc (suc (suc zero))) (empty {n = zero}))))

-- But what if we want to insert into a heap that is not indexed with
-- 0? One solution is to be liberal and ``promote'' that heap so that
-- after insertion it can store elements with any priorities:
toZero : {b : Priority} → Heap b → Heap zero
toZero empty               = empty
toZero (node p rank _ l r) = node p rank ge0 l r

insert0 : {b : Priority} → Priority → Heap b → Heap zero
insert0 p h = merge (singleton p) (toZero h)

-- But what if we actaully want to maintain bounds imposed on the heap
-- by its index? To achieve that we need a new singleton function that
-- constructs a singleton Heap with a bound equal to priority of a
-- single element stored by the heap. To construct a proof required by
-- node we use ≥sym, which proves that if p ≡ p then p ≥ p.
singletonB : (p : Priority) → Heap p
singletonB p = node p one (≥sym refl) empty empty

-- We can now write new insert function that uses singletonB function:
insertB : (p : Priority) → Heap p → Heap p
insertB p h = merge (singletonB p) h
-- However, that function is pretty much useless - it can insert
-- element with priority p only to a heap that has p as its bound. In
-- other words if we have Heap zero - ie. a heap that can store any
-- possible priority -- the only thing that we can insert into it
-- using insertB function is zero. That's clearly not what we want. We
-- need a way to manipulate resulting priority bound.

-- Let's try again. This time we will write functions with signatures:
--
--  singletonB' : {b : Priority} → (p : Priority) → p ≥ b → Heap b
--  insertB' : {b : Priority} → (p : Priority) → p ≥ b → Heap p → Heap b
--
-- Singleton allows to construct Heap containing priority p but
-- bounded by b. This of course requires proof that p ≥ b, ie. that
-- priority p can actually be stored in Heap b. insertB' is similar -
-- it can insert element of priority p into Heap bounded by p but the
-- resulting Heap can be bounded by b (provided that p ≥ b, for which
-- we must supply evidence). Let's implement that.

-- Implementing singletonB' is straightforward:
singletonB' : {b : Priority} → (p : Priority) → p ≥ b → Heap b
singletonB' p p≥b = node p one p≥b empty empty

-- To implement insertB' we need two additional functions. Firstly, we
-- need a proof of transitivity of ≥. We proceed by induction on
-- c. Our base case is:
--
--   a ≥ b ∧ b ≥ 0 ⇒ a ≥ 0
--
-- In other words if c is 0 then ge0 proves the property. If c is not
-- zero, then b is also not zero (by definitions of data constructors
-- of ≥) and hence a is also not zero. This gives us second equation
-- that is a recursive proof on ≥trans.
≥trans : {a b c : Nat} → a ≥ b → b ≥ c → a ≥ c
≥trans a≥b        ge0      = ge0
≥trans (geS a≥b) (geS b≥c) = geS (≥trans a≥b b≥c)

-- Having proved the transitivity of ≥ we can construct a function
-- that loosens the bound we put on a heap. If we have a heap with a
-- bound p - meaning that all priorities in a heap are guaranteed to
-- be lower than or equal to p - and we also have evidence than n is a
-- priority higher than p then we can change the restriction on the
-- heap so that it accepts higher priorites. For example if we have
-- Heap 5, ie. all elements in the heap are 5 or greater, and we have
-- evidence that 5 ≥ 3, then we can convert Heap 5 to Heap 3. Note how
-- we are prevented from writing wrong code: if we have Heap 3 we
-- cannot convert it to Heap 5. This is not possible from theoretical
-- point of view: Heap 3 may contain 4, but Heap 5 is expected to
-- contain elements not smaller than 5. It is also not possible
-- practically: thanks to our definition of ≥ we can't orivide
-- evidence that 3 ≥ 5 because we cannot construct value of that type.
liftBound : {p b : Priority} → b ≥ p → Heap b → Heap p
liftBound b≥n empty = empty
liftBound b≥n (node p rank p≥b l r)
  = node p rank (≥trans p≥b b≥n) l r

-- With singletonB and liftBound we can construct insert function that
-- allows to insert element with priority p into a Heap bound by b,
-- but only if we can supply evidence that p ≥ b, ie. that p can
-- actually be stored in the heap.
insertB' : {b : Priority} → (p : Priority) → p ≥ b → Heap p → Heap b
insertB' p p≥b h = merge (singletonB' p p≥b) (liftBound p≥b h)

-- But if we try to create an example Heap as we did previously we
-- quickly discover that this function isn't of much use either:
heap' : Heap zero
heap' = insertB' (suc (suc zero)) {!!}
       (insertB' (suc zero) {!!}
       (insertB' zero {!!}
       (insertB' (suc (suc (suc zero))) {!!} (empty))))

-- In third hole we are required to supply evidence that 0 ≥ 1 and
-- that is not possible. The reason is that our insertB' function
-- allows us only to insert elements into a heap in decreasing order:
heap'' : Heap zero
heap'' = insertB' zero ge0
        (insertB' (suc zero) ge0
        (insertB' (suc (suc zero)) (geS ge0)
        (insertB' (suc (suc (suc zero))) (geS (geS ge0)) (empty))))
-- This is a direct consequence of our requirement that priority of
-- element being inserted and bound on the Heap we insert into match.

-- Again, findMin and deletMin are incomplete
findMin : {b : Priority} → Heap b → Priority
findMin empty            = {!!}
findMin (node p _ _ _ _) = p

-- deleteMin requires a bit more work than previously. First, notice
-- that the bound placed on the input and output heaps is the
-- same. This happens because relation between priorities in a node
-- and it's children is ≥, not > (ie. equality is allowed). We cannot
-- therefore guearantee that bound on priority will increase after
-- removing highest-priority element from the Heap. When we merge
-- left and right subtrees we need to lift their bounds so they are
-- now both b (not p).
deleteMin : {b : Priority} → Heap b → Heap b
deleteMin empty                 = {!!}
deleteMin (node p rank p≥b l r) = merge (liftBound p≥b l) (liftBound p≥b r)

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
import cedille-options
open import general-util
module meta-vars (options : cedille-options.options) {mF : Set → Set} ⦃ _ : monad mF ⦄ where

open import cedille-types
open import constants
open import conversion
open import ctxt
open import free-vars
open import rename
open import spans options {mF}
open import subst
open import syntax-util
open import to-string options

-- misc
----------------------------------------------------------------------

-- Meta-variables, prototypes, decorated types
-- ==================================================

record meta-var-sol (A : Set) : Set where
  constructor mk-meta-var-sol
  field
    sol : A
    src : checking-mode

data meta-var-sort : Set where
  meta-var-tp : (k  : kind) → (mtp : maybe $ meta-var-sol type) → meta-var-sort
  meta-var-tm : (tp : type) → (mtm : maybe $ meta-var-sol term) → meta-var-sort

record meta-var : Set where
  constructor meta-var-mk
  field
    name : string
    sort  : meta-var-sort
    loc  : span-location
open meta-var

pattern meta-var-mk-tp x k mtp l = meta-var-mk x (meta-var-tp k mtp) l

record meta-vars : Set where
  constructor meta-vars-mk
  field
    order   : 𝕃 var
    varset  : trie meta-var
open meta-vars

data prototype : Set where
  proto-maybe : maybe type → prototype
  proto-arrow : erased? → prototype → prototype

data decortype : Set where
  decor-type  : type → decortype
  decor-arrow : erased? → type → decortype → decortype
  decor-decor : erased? → var → tpkd → meta-var-sort → decortype → decortype
  decor-stuck : type → prototype → decortype
  decor-error : type → prototype → decortype

-- Simple definitions and accessors
-- --------------------------------------------------

meta-var-name : meta-var → var
meta-var-name X = meta-var.name X

meta-vars-get-varlist : meta-vars → 𝕃 var
meta-vars-get-varlist Xs = map (name ∘ snd) (trie-mappings (varset Xs))

meta-var-solved? : meta-var → 𝔹
meta-var-solved? (meta-var-mk n (meta-var-tp k nothing) _) = ff
meta-var-solved? (meta-var-mk n (meta-var-tp k (just _)) _) = tt
meta-var-solved? (meta-var-mk n (meta-var-tm tp nothing) _) = ff
meta-var-solved? (meta-var-mk n (meta-var-tm tp (just _)) _) = tt

meta-vars-empty : meta-vars
meta-vars-empty = meta-vars-mk [] empty-trie

meta-vars-empty? : meta-vars → 𝔹
meta-vars-empty? Xs = ~ (trie-nonempty (varset Xs ))

meta-vars-solved? : meta-vars → 𝔹
meta-vars-solved? Xs = trie-all meta-var-solved? (varset Xs)

meta-vars-filter : (meta-var → 𝔹) → meta-vars → meta-vars
meta-vars-filter f Xs =
  meta-vars-mk or vs
  where
  vs = trie-filter f (varset Xs)
  or = filter (trie-contains vs) (order Xs)

meta-var-sort-eq? : ctxt → (=S =T : meta-var-sort) → 𝔹
meta-var-sort-eq? Γ (meta-var-tp k₁ mtp₁) (meta-var-tp k₂ mtp₂)
  with conv-kind Γ k₁ k₂
... | ff = ff
... | tt =
  maybe-equal? sol-eq mtp₁ mtp₂
  where
    sol-eq : (sol₁ sol₂ : meta-var-sol type) → 𝔹
    sol-eq (mk-meta-var-sol sol₁ src) (mk-meta-var-sol sol₂ src₁) =
      conv-type Γ sol₁ sol₂

meta-var-sort-eq? _ _ _ = ff
-- TODO terms not supported
-- meta-var-sol-eq? (meta-var-tm tp mtm) (meta-var-tm tp₁ mtm₁) = {!!}

meta-var-equal? : ctxt → (X Y : meta-var) → 𝔹
meta-var-equal? Γ (meta-var-mk name₁ sol₁ _) (meta-var-mk name₂ sol₂ _) =
  name₁ =string name₂ && meta-var-sort-eq? Γ sol₁ sol₂

meta-vars-equal? : ctxt → (Xs Ys : meta-vars) → 𝔹
meta-vars-equal? Γ Xs Ys =
  trie-equal? (meta-var-equal? Γ) (meta-vars.varset Xs) (meta-vars.varset Ys)

meta-vars-lookup : meta-vars → var → maybe meta-var
meta-vars-lookup Xs x = trie-lookup (varset Xs) x

meta-vars-lookup-with-kind : meta-vars → var → maybe (meta-var × kind)
meta-vars-lookup-with-kind Xs x
  with meta-vars-lookup Xs x
... | nothing = nothing
... | (just X@(meta-var-mk-tp _ k _ _)) = just $ X , k
... | (just X) = nothing

meta-var-set-src : meta-var → checking-mode → meta-var
meta-var-set-src (meta-var-mk-tp name₁ k (just sol) loc₁) m =
  meta-var-mk-tp name₁ k (just (record sol { src = m })) loc₁
meta-var-set-src (meta-var-mk-tp name₁ k nothing loc₁) m =
  meta-var-mk-tp name₁ k nothing loc₁
meta-var-set-src (meta-var-mk name₁ (meta-var-tm tp (just sol)) loc₁) m =
  meta-var-mk name₁ (meta-var-tm tp (just (record sol { src = m }))) loc₁
meta-var-set-src (meta-var-mk name₁ (meta-var-tm tp nothing) loc₁) m
  = meta-var-mk name₁ (meta-var-tm tp nothing) loc₁

meta-vars-lookup-kind : meta-vars → var → maybe kind
meta-vars-lookup-kind Xs x with meta-vars-lookup Xs x
... | nothing = nothing
... | (just (meta-var-mk-tp _ k _ _)) = just k
... | (just X) = nothing

-- conversion to types, terms, tks
-- --------------------------------------------------

meta-var-sort-to-tk : meta-var-sort → tpkd
meta-var-sort-to-tk (meta-var-tp k mtp) = Tkk k
meta-var-sort-to-tk (meta-var-tm tp mtm) = Tkt tp

meta-var-to-type : meta-var → maybe type
meta-var-to-type (meta-var-mk-tp x k (just tp) _) = just (meta-var-sol.sol tp)
meta-var-to-type (meta-var-mk-tp x k nothing _) = just (TpVar x)
meta-var-to-type (meta-var-mk x (meta-var-tm tp mtm) _) = nothing

meta-var-to-term : meta-var → maybe term
meta-var-to-term (meta-var-mk-tp x k mtp _) = nothing
meta-var-to-term (meta-var-mk x (meta-var-tm tp (just tm)) _) = just (meta-var-sol.sol tm)
meta-var-to-term (meta-var-mk x (meta-var-tm tp nothing) _) = just (Var x)

meta-var-to-type-unsafe : meta-var → type
meta-var-to-type-unsafe X
  with meta-var-to-type X
... | just tp = tp
... | nothing = TpVar (meta-var-name X)

meta-var-to-term-unsafe : meta-var → term
meta-var-to-term-unsafe X
  with meta-var-to-term X
... | just tm = tm
... | nothing = Var (meta-var-name X)

-- if all meta-vars are solved, return their solutions as args
meta-vars-to-args : meta-vars → maybe args
meta-vars-to-args (meta-vars-mk or vs) =
  flip 𝕃maybe-map or λ x → trie-lookup vs x ≫=maybe λ where
    (meta-var-mk name (meta-var-tm tp tm?) loc) →
      tm? >>= just ∘' ArgEr ∘' meta-var-sol.sol
    (meta-var-mk name (meta-var-tp kd tp?) loc) →
      tp? >>= just ∘' ArgTp ∘' meta-var-sol.sol

prototype-to-maybe : prototype → maybe type
prototype-to-maybe (proto-maybe mtp) = mtp
prototype-to-maybe (proto-arrow _ _) = nothing

prototype-to-checking : prototype → checking-mode
prototype-to-checking = maybe-to-checking ∘ prototype-to-maybe

decortype-to-type : decortype → type
decortype-to-type (decor-type tp) = tp
decortype-to-type (decor-arrow at tp dt) =
  TpArrow tp at (decortype-to-type dt)
decortype-to-type (decor-decor b x tk sol dt) =
  TpAbs b x tk (decortype-to-type dt)
decortype-to-type (decor-stuck tp pt) = tp
decortype-to-type (decor-error tp pt) = tp

-- hnf for decortype
-- --------------------------------------------------

hnf-decortype : ctxt → unfolding → decortype → (is-head : 𝔹) → decortype
hnf-decortype Γ uf (decor-type tp) ish =
  decor-type (hnf Γ (record uf {unfold-defs = ish}) tp)
hnf-decortype Γ uf (decor-arrow e? tp dt) ish =
  decor-arrow e? (hnf Γ (record uf {unfold-defs = ff}) tp) (hnf-decortype Γ uf dt ff)
hnf-decortype Γ uf (decor-decor e? x tk sol dt) ish =
  decor-decor e? x tk sol (hnf-decortype Γ uf dt ff)
hnf-decortype Γ uf dt@(decor-stuck _ _) ish = dt
hnf-decortype Γ uf (decor-error tp pt) ish =
  decor-error (hnf Γ (record uf {unfold-defs = ff}) tp) pt

-- substitutions
-- --------------------------------------------------

substh-meta-var-sort : substh-ret-t meta-var-sort
substh-meta-var-sort Γ ρ σ (meta-var-tp k mtp) =
  meta-var-tp (substh Γ ρ σ k) ((flip maybe-map) mtp λ sol →
    record sol { sol = substh Γ ρ σ (meta-var-sol.sol sol) })
substh-meta-var-sort Γ ρ σ (meta-var-tm tp mtm) =
  meta-var-tm (substh Γ ρ σ tp) (flip maybe-map mtm λ sol →
    record sol { sol = substh Γ ρ σ (meta-var-sol.sol sol) })

subst-meta-var-sort : subst-ret-t meta-var-sort
subst-meta-var-sort Γ t x (meta-var-tp k mtp) =
  meta-var-tp (subst Γ t x k) $ (flip maybe-map) mtp λ sol →
    record sol { sol = subst Γ t x $ meta-var-sol.sol sol }

subst-meta-var-sort Γ t x (meta-var-tm tp mtm) =
  meta-var-tm (subst Γ t x tp) $ (flip maybe-map) mtm λ where
    (mk-meta-var-sol sol src) → mk-meta-var-sol (subst Γ t x sol) src

meta-vars-get-sub : meta-vars → trie (Σi exprd ⟦_⟧)
meta-vars-get-sub Xs =
  trie-catMaybe (trie-map (maybe-map ,_ ∘ meta-var-to-type) (varset Xs))

meta-vars-subst-type' : (unfold : 𝔹) → ctxt → meta-vars → type → type
meta-vars-subst-type' u Γ Xs tp =
  let tp' = substs Γ (meta-vars-get-sub Xs) tp in
  if u then hnf Γ unfold-head-elab tp' else tp'

meta-vars-subst-type : ctxt → meta-vars → type → type
meta-vars-subst-type = meta-vars-subst-type' tt

meta-vars-subst-kind : ctxt → meta-vars → kind → kind
meta-vars-subst-kind Γ Xs k
  = hnf Γ unfold-head-elab (substh Γ empty-renamectxt (meta-vars-get-sub Xs) k)

-- string and span helpers
-- --------------------------------------------------

meta-var-to-string : meta-var → strM
meta-var-to-string (meta-var-mk-tp name k nothing sl)
  = strMetaVar name sl
    >>str strAdd " : " >>str to-stringe k
meta-var-to-string (meta-var-mk-tp name k (just tp) sl)
  = strMetaVar name sl
    >>str strAdd " : " >>str to-stringe k
    >>str strAdd " = " >>str to-stringe (meta-var-sol.sol tp) -- tp
meta-var-to-string (meta-var-mk name (meta-var-tm tp nothing) sl)
  = strMetaVar name sl
    >>str strAdd " : " >>str to-stringe tp
meta-var-to-string (meta-var-mk name (meta-var-tm tp (just tm)) sl)
  = strMetaVar name sl
    >>str strAdd " : " >>str to-stringe tp
    >>str strAdd " = " >>str to-stringe (meta-var-sol.sol tm) -- tm

meta-vars-to-stringe : 𝕃 meta-var → strM
meta-vars-to-stringe []
  = strEmpty
meta-vars-to-stringe (v :: [])
  = meta-var-to-string v
meta-vars-to-stringe (v :: vs)
  = meta-var-to-string v >>str strAdd ", " >>str meta-vars-to-stringe vs

meta-vars-to-string : meta-vars → strM
meta-vars-to-string Xs =
  meta-vars-to-stringe
    ((flip map) (order Xs) λ x →
      case trie-lookup (varset Xs) x of λ where
        nothing  →
          meta-var-mk
            (x ^ "-missing!") (meta-var-tp KdStar nothing)
            missing-span-location
        (just X) → X)

prototype-to-string : prototype → strM
prototype-to-string (proto-maybe nothing) = strAdd "⁇"
prototype-to-string (proto-maybe (just tp)) = to-stringe tp
prototype-to-string (proto-arrow e? pt) =
  strAdd "⁇" >>str strAdd (arrowtype-to-string e?)
  >>str prototype-to-string pt

decortype-to-string : decortype → strM
decortype-to-string (decor-type tp) =
  strAdd "[" >>str to-stringe tp >>str strAdd "]"
decortype-to-string (decor-arrow e? tp dt) =
  to-stringe tp
  >>str strAdd (arrowtype-to-string e?)
  >>str decortype-to-string dt
decortype-to-string (decor-decor e? x tk sol dt) =
  strAdd (binder e? sol) >>str meta-var-to-string (meta-var-mk x sol missing-span-location)
  >>str strAdd "<" >>str tpkd-to-stringe tk >>str strAdd ">" >>str strAdd " . " >>str decortype-to-string dt
  where
  binder : erased? → meta-var-sort → string
  binder Erased sol = "∀ "
  binder Pi (meta-var-tm tp mtm) = "Π "
  -- vv clause below "shouldn't" happen
  binder Pi (meta-var-tp k mtp) = "∀ "

decortype-to-string (decor-stuck tp pt) =
  strAdd "(" >>str to-stringe tp >>str strAdd " , " >>str prototype-to-string pt >>str strAdd ")"
decortype-to-string (decor-error tp pt) =
  strAdd "([" >>str (to-stringe tp) >>str strAdd "] ‼ " >>str prototype-to-string pt >>str strAdd ")"

meta-vars-data-h : ctxt → string → kind ∨ (meta-var-sol type) → tagged-val
meta-vars-data-h Γ X (inj₁ k) =
  strRunTag "meta-vars-intro" Γ
    (strAdd (unqual-local X ^ "  ") >>str to-stringe k)
meta-vars-data-h Γ X (inj₂ sol) =
  strRunTag "meta-vars-sol" Γ $
  strAdd (unqual-local X ^ " ") >>str
  strAdd (checking-to-string (meta-var-sol.src sol) ^ " ") >>str
  (to-stringe ∘ meta-var-sol.sol $ sol)

meta-vars-data-all : ctxt → meta-vars → 𝕃 tagged-val
meta-vars-data-all Γ = foldr
  (uncurry λ where
    _ (meta-var-mk X (meta-var-tp kd nothing) loc) xs →
      meta-vars-data-h Γ X (inj₁ kd) :: xs
    _ (meta-var-mk X (meta-var-tp kd (just tp)) loc) xs →
      meta-vars-data-h Γ X (inj₁ kd)
      :: meta-vars-data-h Γ X (inj₂ tp) :: xs
    _ _ xs → xs)
  [] ∘ (trie-mappings ∘ meta-vars.varset)

meta-vars-intro-data : ctxt → meta-vars → 𝕃 tagged-val
meta-vars-intro-data Γ = map (h ∘ snd) ∘ (trie-mappings ∘ meta-vars.varset)
  where
  h : meta-var → tagged-val
  h (meta-var-mk X (meta-var-tp kd mtp) loc) = meta-vars-data-h Γ X (inj₁ kd)
  h (meta-var-mk X (meta-var-tm tp mtm) loc) =
    meta-vars-data-h Γ X
      (inj₂ (mk-meta-var-sol (TpVar "unimplemented") untyped))

meta-vars-sol-data : ctxt → meta-vars → meta-vars → 𝕃 tagged-val
meta-vars-sol-data Γ Xsₒ Xsₙ = foldr (λ X xs → maybe-else xs (_:: xs) (h (snd X)))
  [] (trie-mappings (meta-vars.varset Xsₙ))
  where
  h : meta-var → maybe tagged-val
  h (meta-var-mk X (meta-var-tp kd (just tp)) loc) with trie-lookup (meta-vars.varset Xsₒ) X
  ...| just (meta-var-mk _ (meta-var-tp _ (just _)) _) = nothing
  ...| _ = just (meta-vars-data-h Γ X (inj₂ tp)
    )
  h (meta-var-mk X (meta-var-tp kd nothing) loc) = nothing
  h (meta-var-mk X (meta-var-tm tp mtm) loc) =
    just (meta-vars-data-h Γ X
      (inj₂ (mk-meta-var-sol (TpVar "unimplemented") untyped)))

meta-vars-check-type-mismatch : ctxt → string → type → meta-vars → type
                                 → 𝕃 tagged-val × err-m
meta-vars-check-type-mismatch Γ s tp Xs tp'
  = (expected-type Γ tp :: [ type-data Γ tp'' ]) ,
    (if conv-type Γ tp tp''
        then nothing
        else just ("The expected type does not match the "
               ^ s ^ " type."))
    where tp'' = meta-vars-subst-type' ff Γ Xs tp'

meta-vars-check-type-mismatch-if : maybe type → ctxt → string → meta-vars
                                    → type → 𝕃 tagged-val × err-m
meta-vars-check-type-mismatch-if (just tp) Γ s Xs tp'
  = meta-vars-check-type-mismatch Γ s tp Xs tp'
meta-vars-check-type-mismatch-if nothing Γ s Xs tp'
  = [ type-data Γ tp″ ] , nothing
  where
  tp″ = meta-vars-subst-type' ff Γ Xs tp'

decortype-data : ctxt → decortype → tagged-val
decortype-data Γ dt = strRunTag "head decoration" Γ (decortype-to-string dt)

prototype-data : ctxt → prototype → tagged-val
prototype-data Γ pt = strRunTag "head prototype" Γ (prototype-to-string pt)

-- collecting, merging, matching
-- --------------------------------------------------

meta-var-fresh-t : (S : Set) → Set
meta-var-fresh-t S = meta-vars → var → span-location → S → meta-var

meta-var-fresh : meta-var-fresh-t meta-var-sort
meta-var-fresh Xs x sl sol
  with fresh-h (trie-contains (varset Xs)) (meta-var-pfx-str ^ x)
... | x' = meta-var-mk x' sol sl

meta-var-fresh-tp : meta-var-fresh-t (kind × maybe (meta-var-sol type))
meta-var-fresh-tp Xs x sl (k , msol) =
  meta-var-fresh Xs x sl (meta-var-tp k msol)

meta-var-fresh-tm : meta-var-fresh-t (type × maybe (meta-var-sol term))
meta-var-fresh-tm Xs x sl (tp , mtm) = meta-var-fresh Xs x sl (meta-var-tm tp mtm)

private
  meta-vars-set : meta-vars → meta-var → meta-vars
  meta-vars-set Xs X = record Xs { varset = trie-insert (varset Xs) (name X) X }

-- add a meta-var
meta-vars-add : meta-vars → meta-var → meta-vars
meta-vars-add Xs X
 = record (meta-vars-set Xs X) { order = (order Xs) ++ [ name X ] }

meta-vars-add* : meta-vars → 𝕃 meta-var → meta-vars
meta-vars-add* Xs [] = Xs
meta-vars-add* Xs (Y :: Ys) = meta-vars-add* (meta-vars-add Xs Y) Ys

meta-vars-from-list : 𝕃 meta-var → meta-vars
meta-vars-from-list Xs = meta-vars-add* meta-vars-empty Xs

meta-vars-remove : meta-vars → meta-var → meta-vars
meta-vars-remove (meta-vars-mk or vs) X =
  let x = meta-var-name X
  in meta-vars-mk (remove _=string_ x or) (trie-remove vs x)

meta-vars-in-type : meta-vars → type → meta-vars
meta-vars-in-type Xs tp =
  let xs = free-vars tp in
  meta-vars-filter (stringset-contains xs ∘ name) Xs

meta-vars-unsolved : meta-vars → meta-vars
meta-vars-unsolved = meta-vars-filter λ where
  (meta-var-mk x (meta-var-tp k mtp) _)  → ~ isJust mtp
  (meta-var-mk x (meta-var-tm tp mtm) _) → ~ isJust mtm

meta-vars-are-free-in-type : meta-vars → type → 𝔹
meta-vars-are-free-in-type Xs tp =
  let xs = free-vars tp in
  list-any (stringset-contains xs) (order Xs)

-- Unfolding a type with meta-vars
-- ==================================================

-- ... in order to reveal a term or type application

-- "View" data structures
-- --------------------------------------------------

-- The decorated type is really an arrow
record is-tmabsd : Set where
  constructor mk-tmabsd
  field
    is-tmabsd-dt  : decortype
    is-tmabsd-e?  : erased?
    is-tmabsd-var : var
    is-tmabsd-dom : type
    is-tmabsd-var-in-body : 𝔹
    is-tmabsd-cod : decortype
open is-tmabsd public

is-tmabsd? = decortype ∨ is-tmabsd

pattern yes-tmabsd dt e? x dom occ cod = inj₂ (mk-tmabsd dt e? x dom occ cod)
pattern not-tmabsd tp = inj₁ tp

record is-tpabsd : Set where
  constructor mk-tpabsd
  field
    is-tpabsd-dt   : decortype
    is-tpabsd-e?   : erased?
    is-tpabsd-var  : var
    is-tpabsd-kind : kind
    is-tpabsd-sol  : maybe type
    is-tpabsd-body : decortype
open is-tpabsd public

is-tpabsd? = decortype ∨ is-tpabsd

pattern yes-tpabsd dt e? x k mtp dt' = inj₂ (mk-tpabsd dt e? x k mtp dt')
pattern not-tpabsd dt = inj₁ dt

{-# TERMINATING #-}
num-arrows-in-type : ctxt → type → ℕ
num-arrows-in-type Γ tp = nait Γ (hnf' Γ tp) 0 tt
  where
  hnf' : ctxt → type → type
  hnf' Γ tp = hnf Γ unfold-head-elab tp

  nait : ctxt → type → (acc : ℕ) → 𝔹 → ℕ
  -- definitely another arrow
  nait Γ (TpAbs _ _ (Tkk _) tp) acc uf = nait Γ tp acc ff
  nait Γ (TpAbs _ _ (Tkt _) tp) acc uf = nait Γ tp (1 + acc) ff
  -- definitely not another arrow
  nait Γ (TpIota _ _ _) acc uf = acc
  nait Γ (TpEq _ _) acc uf = acc
  nait Γ (TpHole _) acc uf = acc
  nait Γ (TpLam _ _ _) acc uf = acc
  nait Γ (TpVar x) acc tt = acc
  nait Γ (TpApp tp₁ tp₂) acc tt = acc
  nait Γ tp acc ff = nait Γ (hnf' Γ tp) acc tt

-- Utilities for match-types in classify.agda
-- ==================================================
--
-- Match a type with meta-variables in it to one without

-- errors
-- --------------------------------------------------

match-error-data = string × 𝕃 tagged-val

match-error-t : ∀ {a} → Set a → Set a
match-error-t A = match-error-data ∨ A

pattern match-error e = inj₁ e
pattern match-ok a = inj₂ a

module meta-vars-match-errors where
  -- boilerplate
  match-error-msg = "Matching failed"

  -- tagged values for error messages
  match-lhs : {ed : exprd} → ctxt → ⟦ ed ⟧ → tagged-val
  match-lhs = to-string-tag "expected lhs"

  match-rhs : {ed : exprd} → ctxt → ⟦ ed ⟧ → tagged-val
  match-rhs = to-string-tag "computed rhs"

  the-meta-var : var → tagged-val
  the-meta-var = strRunTag "the meta-var" empty-ctxt ∘ strAdd

  the-solution : ctxt → type → tagged-val
  the-solution = to-string-tag "the solution"

  fst-snd-sol : {ed : exprd} → ctxt → (t₁ t₂ : ⟦ ed ⟧) → 𝕃 tagged-val
  fst-snd-sol Γ t₁ t₂ =
    to-string-tag "first solution" Γ t₁ :: [ to-string-tag "second solution" Γ t₂ ]

  lhs-rhs : {ed : exprd} → ctxt → (t₁ t₂ : ⟦ ed ⟧) → 𝕃 tagged-val
  lhs-rhs Γ t₁ t₂ = match-lhs Γ t₁ :: [ match-rhs Γ t₂ ]

  -- error-data
  e-solution-ineq : ctxt → (tp₁ tp₂ : type) → var → match-error-data
  e-solution-ineq Γ tp₁ tp₂ X =
    match-error-msg ^ " because it produced two incovertible solutions for a meta-variable"
    , the-meta-var X :: fst-snd-sol Γ tp₁ tp₂

  e-match-failure : match-error-data
  e-match-failure =
    "The expected argument type is not a (first-order) match of the computed type"
    , []

  e-matchk-failure : match-error-data
  e-matchk-failure =
    "The expected argument kind is not a (first-order) match of the computed kind"
    , []

  e-meta-scope : ctxt → (X tp : type) → match-error-data
--  e-meta-scope : ctxt → (x : var) → (tp₁ tp₂ : type) → match-error-data
  e-meta-scope Γ X tp =
    match-error-msg ^ " because the solution contains a bound variable of the computed argument type"
    , to-string-tag "the meta var" Γ X :: [ to-string-tag "the solution" Γ tp ]

  e-bad-sol-kind : ctxt → (X : var) → (sol : type) → match-error-data
  e-bad-sol-kind Γ X sol =
    "The meta-variable was matched to a type whose kind does not match its own"
    , the-meta-var X :: [ the-solution Γ sol ]

open meta-vars-match-errors

-- meta-vars-match auxiliaries
-- --------------------------------------------------

local-vars = stringset

meta-vars-solve-tp : ctxt → meta-vars → var → type → checking-mode → match-error-t meta-vars
meta-vars-solve-tp Γ Xs x tp m with trie-lookup (varset Xs) x
... | nothing
  = match-error $ x ^ " is not a meta-var!" , []
... | just (meta-var-mk _ (meta-var-tm tp' mtm) _)
  = match-error $ x ^ " is a term meta-var!" , []
... | just (meta-var-mk-tp _ k nothing sl)
  = match-ok (meta-vars-set Xs (meta-var-mk-tp x k (just (mk-meta-var-sol tp m)) sl))
... | just (meta-var-mk-tp _ k (just sol) _) =
  let mk-meta-var-sol tp' src = sol in
  err⊎-guard (~ conv-type Γ tp tp') (e-solution-ineq Γ tp tp x)
  >> match-ok Xs

-- update the kinds of HO meta-vars with
-- solutions
meta-vars-update-kinds : ctxt → (Xs Xsₖ : meta-vars) → meta-vars
meta-vars-update-kinds Γ Xs Xsₖ =
  record Xs { varset = (flip trie-map) (varset Xs) λ where
    (meta-var-mk-tp x k mtp sl) → meta-var-mk-tp x (meta-vars-subst-kind Γ Xsₖ k) mtp sl
    sol → sol
  }

hnf-elab-if : {ed : exprd} → 𝔹 → ctxt → ⟦ ed ⟧ → 𝔹 → ⟦ ed ⟧
hnf-elab-if b Γ t b' = if b then hnf Γ (record unfold-head-elab {unfold-defs = b'}) t else t

meta-vars-add-from-tpabs : ctxt → span-location → meta-vars → erased? → var → kind → type → meta-var × meta-vars
meta-vars-add-from-tpabs Γ sl Xs e? x k tp =
  let Y   = meta-var-fresh-tp Xs x sl (k , nothing)
      Xs' = meta-vars-add Xs Y
--      tp' = subst Γ (meta-var-to-type-unsafe Y) x tp
  in Y , Xs'

{-
-- Legacy for elaboration.agda
-- ==================================================

-- TODO: remove dependency and delete code

{-# TERMINATING #-} -- subst of a meta-var does not increase distance to arrow
meta-vars-peel : ctxt → span-location → meta-vars → type → (𝕃 meta-var) × type
meta-vars-peel Γ sl Xs (Abs pi e? pi' x tk@(Tkk k) tp)
  with meta-vars-add-from-tpabs Γ sl Xs (mk-tpabs e? x k tp)
... | (Y , Xs')
  with subst Γ (meta-var-to-type-unsafe Y) x tp
... | tp' =
  let ret =  meta-vars-peel Γ sl Xs' tp' ; Ys  = fst ret ; rtp = snd ret
  in (Y :: Ys , rtp)
meta-vars-peel Γ sl Xs (NoSpans tp _) =
  meta-vars-peel Γ sl Xs tp
meta-vars-peel Γ sl Xs (TpParens _ tp _) =
  meta-vars-peel Γ sl Xs tp
meta-vars-peel Γ sl Xs tp = [] , tp

meta-vars-unfold-tpapp : ctxt → meta-vars → type → is-tpabs?
meta-vars-unfold-tpapp Γ Xs tp
  with meta-vars-subst-type Γ Xs tp
... | Abs _ b _ x (Tkk k) tp' = yes-tpabs b x k tp'
... | tp'                        = not-tpabs tp'

meta-vars-unfold-tmapp : ctxt → span-location → meta-vars → type → 𝕃 meta-var × is-tmabs?
meta-vars-unfold-tmapp Γ sl Xs tp
  with meta-vars-peel Γ sl Xs (meta-vars-subst-type Γ Xs tp)
... | Ys , Abs _ b _ x (Tkt dom) cod =
  Ys , yes-tmabs b x dom (is-free-in check-erased x cod) cod
... | Ys , TpArrow dom e? cod =
  Ys , yes-tmabs e? "_" dom ff cod
... | Ys , tp' = Ys , not-tmabs tp'

-}


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Types.EpochState      as EpochState
import      LibraBFT.Impl.Types.Waypoint        as Waypoint
open import LibraBFT.ImplShared.Consensus.Types
open import Util.Encode
open import Util.PKCS                           hiding (verify)
open import Util.Prelude

module LibraBFT.Impl.Types.Verifier where

record Verifier (A : Set) : Set where
  field
    verify                          : A → LedgerInfoWithSignatures → Either ErrLog Unit
    epochChangeVerificationRequired : A → Epoch                    → Bool
    isLedgerInfoStale               : A → LedgerInfo               → Bool
    ⦃ encodeA ⦄                     : Encoder A

open Verifier ⦃ ... ⦄ public

instance
  VerifierEpochState : Verifier EpochState
  VerifierEpochState = record
    { verify                          = EpochState.verify
    ; epochChangeVerificationRequired = EpochState.epochChangeVerificationRequired
    ; isLedgerInfoStale               = EpochState.isLedgerInfoStale
    }

instance
  VerifierWaypoint   : Verifier Waypoint
  VerifierWaypoint   = record
    { verify                          = Waypoint.verifierVerify
    ; epochChangeVerificationRequired = Waypoint.epochChangeVerificationRequired
    ; isLedgerInfoStale               = Waypoint.isLedgerInfoStale
    }


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

open import Cubical.Core.Everything
open import Cubical.Foundations.HLevels

module Cubical.Algebra.Magma.Construct.Left {ℓ} (Aˢ : hSet ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Magma

private
  A = ⟨ Aˢ ⟩
  isSetA = Aˢ .snd

_◂_ : Op₂ A
x ◂ y = x

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

◂-zeroˡ : ∀ x → LeftZero x _◂_
◂-zeroˡ _ _ = refl

◂-identityʳ : ∀ x → RightIdentity x _◂_
◂-identityʳ _ _ = refl

------------------------------------------------------------------------
-- Magma definition

Left-isMagma : IsMagma A _◂_
Left-isMagma = record { is-set = isSetA }

LeftMagma : Magma ℓ
LeftMagma = record { isMagma = Left-isMagma }


text:
------------------------------------------------------------------------
-- A type soundness result
------------------------------------------------------------------------

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

module Lambda.Partiality-monad.Inductive.Type-soundness where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Equivalence equality-with-J using (_≃_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc
open import Maybe equality-with-J
open import Monad equality-with-J
open import Univalence-axiom equality-with-J
open import Vec.Function equality-with-J

open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Alternative-order
open import Partiality-monad.Inductive.Monad

open import Lambda.Partiality-monad.Inductive.Interpreter
open import Lambda.Syntax

open Closure Tm

-- A propositionally truncated variant of WF-MV.

∥WF-MV∥ : Ty ∞ → Maybe Value → Type
∥WF-MV∥ σ x = ∥ WF-MV σ x ∥

-- If we can prove □ (∥WF-MV∥ σ) (run x), then x does not "go wrong".

does-not-go-wrong : ∀ {σ} {x : M Value} →
                    □ (∥WF-MV∥ σ) (run x) → ¬ x ≡ fail
does-not-go-wrong {σ} {x} always =
  x ≡ fail             ↝⟨ cong MaybeT.run ⟩
  run x ≡ now nothing  ↝⟨ always _ ⟩
  ∥WF-MV∥ σ nothing    ↝⟨ id ⟩
  ∥ ⊥₀ ∥               ↝⟨ _↔_.to (not-inhabited⇒∥∥↔⊥ id) ⟩□
  ⊥₀                   □

-- Some "constructors" for □ ∘ ∥WF-MV∥.

return-wf :
  ∀ {σ v} →
  WF-Value σ v →
  □ (∥WF-MV∥ σ) (MaybeT.run (return v))
return-wf v-wf = □-now truncation-is-proposition ∣ v-wf ∣

_>>=-wf_ :
  ∀ {σ τ} {x : M Value} {f : Value → M Value} →
  □ (∥WF-MV∥ σ) (run x) →
  (∀ {v} → WF-Value σ v → □ (∥WF-MV∥ τ) (run (f v))) →
  □ (∥WF-MV∥ τ) (MaybeT.run (x >>= f))
_>>=-wf_ {σ} {τ} {f = f} x-wf f-wf =
  □->>= (λ _ → truncation-is-proposition) x-wf
    λ { {nothing} → Trunc.rec prop ⊥-elim
      ; {just v}  → Trunc.rec prop f-wf
      }
  where
  prop : ∀ {x} → Is-proposition (□ (∥WF-MV∥ τ) x)
  prop = □-closure 1 (λ _ → truncation-is-proposition)

-- Type soundness.

mutual

  ⟦⟧′-wf : ∀ {n Γ} (t : Tm n) {σ} → Γ ⊢ t ∈ σ →
           ∀ {ρ} → WF-Env Γ ρ →
           ∀ n → □ (∥WF-MV∥ σ) (run (⟦ t ⟧′ ρ n))
  ⟦⟧′-wf (con i)   con             ρ-wf n = return-wf con
  ⟦⟧′-wf (var x)   var             ρ-wf n = return-wf (ρ-wf x)
  ⟦⟧′-wf (ƛ t)     (ƛ t∈)          ρ-wf n = return-wf (ƛ t∈ ρ-wf)
  ⟦⟧′-wf (t₁ · t₂) (t₁∈ · t₂∈) {ρ} ρ-wf n =
     ⟦⟧′-wf t₁ t₁∈ ρ-wf n >>=-wf λ f-wf →
     ⟦⟧′-wf t₂ t₂∈ ρ-wf n >>=-wf λ v-wf →
     ∙-wf f-wf v-wf n

  ∙-wf : ∀ {σ τ f v} →
         WF-Value (σ ⇾ τ) f → WF-Value (force σ) v →
         ∀ n → □ (∥WF-MV∥ (force τ)) (run ((f ∙ v) n))
  ∙-wf (ƛ t₁∈ ρ₁-wf) v₂-wf (suc n) = ⟦⟧′-wf _ t₁∈ (cons-wf v₂-wf ρ₁-wf) n
  ∙-wf (ƛ t₁∈ ρ₁-wf) v₂-wf zero    =         $⟨ □-never ⟩
    □ (∥WF-MV∥ _) never                      ↝⟨ ≡⇒↝ bijection $ cong (□ (∥WF-MV∥ _)) (sym never->>=) ⟩□
    □ (∥WF-MV∥ _) (never >>= return ∘ just)  □

type-soundness : ∀ {t : Tm 0} {σ} →
                 nil ⊢ t ∈ σ → ¬ ⟦ t ⟧ nil ≡ fail
type-soundness {t} {σ} =
  nil ⊢ t ∈ σ                                 ↝⟨ (λ t∈ → ⟦⟧′-wf _ t∈ nil-wf) ⟩
  (∀ n → □ (∥WF-MV∥ σ) (run (⟦ t ⟧′ nil n)))  ↝⟨ □-⨆ (λ _ → truncation-is-proposition) ⟩
  □ (∥WF-MV∥ σ) (run (⟦ t ⟧ nil))             ↝⟨ does-not-go-wrong ⟩□
  ¬ ⟦ t ⟧ nil ≡ fail                          □

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module Issue1760a where

-- Skipping a single record definition.
{-# NO_POSITIVITY_CHECK #-}
record U : Set where
  field ap : U → U


text:
module StrongRMonads where

open import Library
open import Categories
open import Functors
open import MonoidalCat
open import RMonads

record SRMonad {a b c d}{M : Monoidal {a}{b}}{M' : Monoidal {c}{d}}
       (J : MonoidalFun M M') : Set (a ⊔ b ⊔ c ⊔ d) where
  constructor srmonad
  open MonoidalFun J
  field RM : RMonad F
  open RMonad RM
  open Cat
  open Monoidal
  open Fun
  field st : ∀{X Y} -> Hom (C M') (OMap (⊗ M') (T X , OMap F Y))
                                  (T (OMap (⊗ M) (X , Y)))
  -- laws later

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Sum.Relation.Binary.LeftOrder directly.
------------------------------------------------------------------------

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

module Data.Sum.Relation.LeftOrder where

open import Data.Sum.Relation.Binary.LeftOrder public


text:
-- Andreas, 2017-02-27, issue #2477

{-# OPTIONS --show-irrelevant #-}

open import Agda.Builtin.Size
open import Agda.Builtin.Nat using (suc) renaming (Nat to ℕ)

_+_ : Size → ℕ → Size
s + 0 = s
s + suc n = ↑ (s + n)

data Nat : Size → Set where
  zero  :  ∀ i → Nat (i + 1)
  suc   :  ∀ i → Nat i → Nat (i + 1)
  -- i + 1 should be reduced to ↑ i
  -- to make Nat monotone in its size argument

pred : ∀ i → Nat i → Nat i
pred .(i + 1) (zero i)   =  zero i
pred .(i + 1) (suc i x)  =  x

-- Should succeed


text:
module RMonads.SpecialCase where

open import Categories
open import Functors
open import Naturals hiding (Iso)
open import Monads
open import RMonads

leftM : ∀{a}{b}{C : Cat {a}{b}} → Monad C → RMonad (IdF C)
leftM M = record {
  T    = T;
  η    = η;
  bind = bind;
  law1 = law1;
  law2 = law2;
  law3 = law3}
  where open Monad M

rightM : ∀{a b}{C : Cat {a}{b}} → RMonad (IdF C) → Monad C
rightM {C = C} M = record {
  T    = T;
  η    = η;
  bind = bind;
  law1 = law1;
  law2 = law2;
  law3 = law3} where open RMonad M

open import Relation.Binary.HeterogeneousEquality
open import Isomorphism

isoM : ∀{a b}{C : Cat {a}{b}} → Iso (RMonad (IdF C)) (Monad C)
isoM = record {fun = rightM; inv = leftM; law1 = λ {(monad _ _ _ _ _ _) → refl}; law2 = λ {(rmonad _ _ _ _ _ _) → refl}}

open import Monads.MonadMorphs
open import RMonads.RMonadMorphs

leftMM : ∀{a b}{C : Cat {a}{b}}{M M' : Monad C} → MonadMorph M M' →
         RMonadMorph (leftM M) (leftM M')
leftMM MM = record {
  morph   = morph;
  lawη    = lawη;
  lawbind = lawbind} where open MonadMorph MM

rightMM : ∀{a b}{C : Cat {a}{b}}{M M' : RMonad (IdF C)} → RMonadMorph M M' →
          MonadMorph (rightM M) (rightM M')
rightMM MM = record {
  morph   = morph;
  lawη    = lawη;
  lawbind = lawbind} where open RMonadMorph MM

isoMM : ∀{a b}{C : Cat {a}{b}}{M M' : Monad C} →
        Iso (RMonadMorph (leftM M) (leftM M')) (MonadMorph M M')
isoMM {M = monad _ _ _ _ _ _}{M' = monad _ _ _ _ _ _} = record {
 fun  = rightMM;
 inv  = leftMM;
 law1 = λ {(monadmorph _ _ _) → refl};
 law2 = λ {(rmonadmorph _ _ _) → refl}}

open import Adjunctions
open import RAdjunctions

leftA : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}} → Adj C D → RAdj (IdF C) D
leftA {C}{D} A = record{
  L        = L;
  R        = R;
  left     = left;
  right    = right;
  lawa     = lawa;
  lawb     = lawb;
  natleft  = natleft;
  natright = natright} where open Adj A

rightA : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}} → RAdj (IdF C) D → Adj C D
rightA {C = C}{D = D} A = record{
  L        = L;
  R        = R;
  left     = left;
  right    = right;
  lawa     = lawa;
  lawb     = lawb;
  natleft  = natleft;
  natright = natright} where open RAdj A

isoA : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}} →
       Iso (RAdj (IdF C) D) (Adj C D)
isoA = record {
  fun = rightA;
  inv = leftA;
  law1 = λ {(adjunction _ _ _ _ _ _ _ _) → refl};
  law2 = λ {(radjunction _ _ _ _ _ _ _ _) → refl}}


text:
------------------------------------------------------------------------
-- Compiler correctness
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --sized-types #-}

module Lambda.Delay-monad.Compiler-correctness where

import Equality.Propositional as E
open import Prelude
open import Prelude.Size

open import Maybe E.equality-with-J hiding (_>>=′_)
open import Monad E.equality-with-J
open import Vec.Function E.equality-with-J

open import Delay-monad.Bisimilarity
open import Delay-monad.Monad

open import Lambda.Compiler
open import Lambda.Delay-monad.Interpreter
open import Lambda.Delay-monad.Virtual-machine
open import Lambda.Syntax hiding ([_])
open import Lambda.Virtual-machine

private
  module C = Closure Code
  module T = Closure Tm

-- Bind preserves strong bisimilarity.

infixl 5 _>>=-congM_

_>>=-congM_ :
  ∀ {i ℓ} {A B : Type ℓ} {x y : M ∞ A} {f g : A → M ∞ B} →
  [ i ] run x ∼ run y →
  (∀ z → [ i ] run (f z) ∼ run (g z)) →
  [ i ] run (x >>= f) ∼ run (y >>= g)
p >>=-congM q = p >>=-cong [ (λ _ → run fail ∎) , q ]

-- Bind is associative.

associativityM :
  ∀ {ℓ} {A B C : Type ℓ} (x : M ∞ A) (f : A → M ∞ B) (g : B → M ∞ C) →
  run (x >>= (λ x → f x >>= g)) ∼ run (x >>= f >>= g)
associativityM x f g =
  run (x >>= λ x → f x >>= g)                                       ∼⟨⟩

  run x >>=′ maybe (λ x → run (f x >>= g)) (return nothing)         ∼⟨ (run x ∎) >>=-cong [ (λ _ → run fail ∎) , (λ x → run (f x >>= g) ∎) ] ⟩

  run x >>=′ (λ x → maybe (MaybeT.run ∘ f) (return nothing) x >>=′
                    maybe (MaybeT.run ∘ g) (return nothing))        ∼⟨ associativity′ (run x) _ _ ⟩

  run x >>=′ maybe (MaybeT.run ∘ f) (return nothing)
        >>=′ maybe (MaybeT.run ∘ g) (return nothing)                ∼⟨⟩

  run (x >>= f >>= g)                                               ∎

-- Compiler correctness.

mutual

  ⟦⟧-correct :
    ∀ {i n} t {ρ : T.Env n} {c s} {k : T.Value → M ∞ C.Value} →
    (∀ v → [ i ] run (exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩) ≈
                 run (k v)) →
    [ i ] run (exec ⟨ comp t c , s , comp-env ρ ⟩) ≈ run (⟦ t ⟧ ρ >>= k)

  ⟦⟧-correct (con i) {ρ} {c} {s} {k} hyp =
    run (exec ⟨ con i ∷ c , s , comp-env ρ ⟩)                     ≳⟨⟩
    run (exec ⟨ c , val (comp-val (T.con i)) ∷ s , comp-env ρ ⟩)  ≈⟨ hyp (T.con i) ⟩∼
    run (k (T.con i))                                             ∼⟨⟩
    run (⟦ con i ⟧ ρ >>= k)                                       ∎

  ⟦⟧-correct (var x) {ρ} {c} {s} {k} hyp =
    run (exec ⟨ var x ∷ c , s , comp-env ρ ⟩)                 ≳⟨⟩
    run (exec ⟨ c , val (comp-val (ρ x)) ∷ s , comp-env ρ ⟩)  ≈⟨ hyp (ρ x) ⟩∼
    run (k (ρ x))                                             ∼⟨⟩
    run (⟦ var x ⟧ ρ >>= k)                                   ∎

  ⟦⟧-correct (ƛ t) {ρ} {c} {s} {k} hyp =
    run (exec ⟨ clo (comp t (ret ∷ [])) ∷ c , s , comp-env ρ ⟩)   ≳⟨⟩
    run (exec ⟨ c , val (comp-val (T.ƛ t ρ)) ∷ s , comp-env ρ ⟩)  ≈⟨ hyp (T.ƛ t ρ) ⟩∼
    run (k (T.ƛ t ρ))                                             ∼⟨⟩
    run (⟦ ƛ t ⟧ ρ >>= k)                                         ∎

  ⟦⟧-correct (t₁ · t₂) {ρ} {c} {s} {k} hyp =
    run (exec ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩)    ≈⟨ (⟦⟧-correct t₁ λ v₁ → ⟦⟧-correct t₂ λ v₂ → ∙-correct v₁ v₂ hyp) ⟩∼

    run (⟦ t₁ ⟧ ρ >>= λ v₁ → ⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂ >>= k)    ∼⟨ (run (⟦ t₁ ⟧ ρ) ∎) >>=-congM (λ _ → associativityM (⟦ t₂ ⟧ ρ) _ _) ⟩

    run (⟦ t₁ ⟧ ρ >>= λ v₁ → (⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂) >>= k)  ∼⟨ associativityM (⟦ t₁ ⟧ ρ) _ _ ⟩

    run (⟦ t₁ · t₂ ⟧ ρ >>= k)                                      ∎

  ∙-correct :
    ∀ {i n} v₁ v₂ {ρ : T.Env n} {c s} {k : T.Value → M ∞ C.Value} →
    (∀ v → [ i ] run (exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩) ≈
                 run (k v)) →
    [ i ] run (exec ⟨ app ∷ c
                    , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
                    , comp-env ρ
                    ⟩) ≈
          run (v₁ ∙ v₂ >>= k)
  ∙-correct (T.con i) v₂ {ρ} {c} {s} {k} hyp =
    run (exec ⟨ app ∷ c
              , val (comp-val v₂) ∷ val (C.con i) ∷ s
              , comp-env ρ
              ⟩)                                       ∼⟨⟩

    run fail                                           ∼⟨⟩

    run (T.con i ∙ v₂ >>= k)                           ∎

  ∙-correct (T.ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} hyp =
    run (exec ⟨ app ∷ c
              , val (comp-val v₂) ∷ val (comp-val (T.ƛ t₁ ρ₁)) ∷ s
              , comp-env ρ
              ⟩)                                                    ≈⟨ later (λ { .force →

      run (exec ⟨ comp t₁ (ret ∷ [])
                , ret c (comp-env ρ) ∷ s
                , cons (comp-val v₂) (comp-env ρ₁)
             ⟩)                                                          ≡⟨ E.cong (λ ρ′ → run (exec ⟨ comp t₁ (ret ∷ []) ,
                                                                                ret c (comp-env ρ) ∷ s , ρ′ ⟩))
                                                                                (E.sym comp-cons) ⟩
      run (exec ⟨ comp t₁ (ret ∷ [])
                , ret c (comp-env ρ) ∷ s
                , comp-env (cons v₂ ρ₁)
                ⟩)                                                       ≈⟨ ⟦⟧-correct t₁ (λ v →

        run (exec ⟨ ret ∷ []
                  , val (comp-val v) ∷ ret c (comp-env ρ) ∷ s
                  , comp-env (cons v₂ ρ₁)
                  ⟩)                                                          ≳⟨⟩

        run (exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩)                  ≈⟨ hyp v ⟩∎

        run (k v)                                                             ∎) ⟩∼

      run (⟦ t₁ ⟧ (cons v₂ ρ₁) >>= k)                                    ∎ }) ⟩∎

    run (T.ƛ t₁ ρ₁ ∙ v₂ >>= k)                                      ∎

-- Note that the equality that is used here is syntactic.

correct :
  ∀ t →
  exec ⟨ comp t [] , [] , nil ⟩ ≈M
  ⟦ t ⟧ nil >>= λ v → return (comp-val v)
correct t =
  run (exec ⟨ comp t [] , [] , nil ⟩)            ≡⟨ E.cong (λ ρ → run (exec ⟨ comp t [] , [] , ρ ⟩)) $ E.sym comp-nil ⟩
  run (exec ⟨ comp t [] , [] , comp-env nil ⟩)   ≈⟨ ⟦⟧-correct t (λ v → return (just (comp-val v)) ∎) ⟩
  run (⟦ t ⟧ nil >>= λ v → return (comp-val v))  ∎


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

open import HoTT

-- Associativity of the join (work in progress)

module experimental.JoinAssoc2 where

import experimental.JoinAssoc as Assoc

module Assoc2 {i j k} (A : Type i) (B : Type j) (C : Type k) where

  open Assoc A B C

  {- Here are the steps, without the junk around:

       apd (λ x → ap to (ap from (glue (a , x)))) (glue (b , c))
1 (From.glue-β)
       apd (λ x → ap to (from-glue (a , x))) (glue (b , c))
2 (unfuse)
       ap↓ (λ x → ap to {x = from-left a} {y = from-right x}) (apd (λ x → from-glue (a , x)) (glue (b , c)))
3 (FromGlue.glue-β)
       ap↓ (λ x → ap to {x = from-left a} {y = from-right x}) (apd (λ x → glue (x , c)) (glue (a , b)))
4 (fuse)
       apd (λ x → ap to (glue (x , c))) (glue (a , b))
5 (To.glue-β)
       apd (λ x → to-glue (x , c)) (glue (a , b))
6 (ToGlue.glue-β)
       apd (λ x → glue (a , x)) (glue (b , c))

  -}

  to-from-glue-glue' : (a : A) (b : B) (c : C)
   → (↯ to-from-glue-left' a b) == (↯ to-from-glue-right' a c) [ (λ x → ap to (ap from (glue (a , x))) ∙' to-from-right x == glue (a , x)) ↓ glue (b , c) ]
  to-from-glue-glue' a b c =
    ↓-=-in (!(
    apd (λ x → ap to (ap from (glue (a , x))) ∙' to-from-right x) (glue (b , c)) ▹ (↯ to-from-glue-right' a c)
               =⟨ apd∙' (λ x → ap to (ap from (glue (a , x)))) to-from-right (glue (b , c)) |in-ctx (λ u → u ▹ (↯ to-from-glue-right' a c)) ⟩
    ((apd (λ x → ap to (ap from (glue (a , x)))) (glue (b , c))) ∙'2ᵈ (apd to-from-right (glue (b , c)))) ▹ (↯ to-from-glue-right' a c)
               =⟨ ToFromRight.glue-β (b , c) |in-ctx
                         (λ u → ((apd (λ x → ap to (ap from (glue (a , x)))) (glue (b , c))) ∙'2ᵈ u) ▹ (↯ to-from-glue-right' a c)) ⟩
    ((apd (λ x → ap to (ap from (glue (a , x)))) (glue (b , c))) ∙'2ᵈ (to-from-right-glue (b , c))) ▹ (↯ to-from-glue-right' a c)
               =⟨ ▹-∙'2ᵈ (apd (λ x → ap to (ap from (glue (a , x)))) (glue (b , c))) (to-from-right-glue (b , c)) (↯ to-from-glue-right' a c) idp ⟩
    (apd (λ x → ap to (ap from (glue (a , x)))) (glue (b , c)) ▹ (↯ to-from-glue-right' a c)) ∙'2ᵈ (to-from-right-glue (b , c) ▹ idp)
               =⟨ (▹idp (to-from-right-glue (b , c))) |in-ctx (λ u → (apd (λ x → ap to (ap from (glue (a , x)))) (glue (b , c)) ▹ (↯ to-from-glue-right' a c)) ∙'2ᵈ u) ⟩
    (apd (λ x → ap to (ap from (glue (a , x)))) (glue (b , c)) ▹ (↯ to-from-glue-right' a c)) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ apd=-red (λ x → ap (ap to) (From.glue-β (a , x))) (glue (b , c)) (1! (to-from-glue-right' a c)) |in-ctx (λ u → u ∙'2ᵈ (to-from-right-glue (b , c))) ⟩
{- 1 -}
    ((↯ 1# (to-from-glue-left' a b)) ◃ (apd (λ x → ap to (from-glue (a , x))) (glue (b , c)) ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ apd-∘' (ap to) (λ x → from-glue (a , x)) (glue (b , c)) |in-ctx (λ u → ((↯ 1# (to-from-glue-left' a b)) ◃ (u ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))) ⟩
{- 2 -}
    ((↯ 1# (to-from-glue-left' a b)) ◃ (ap↓ (ap to) (apd (λ x → from-glue (a , x)) (glue (b , c))) ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ FromGlue.glue-β a (b , c) |in-ctx (λ u → ((↯ 1# (to-from-glue-left' a b)) ◃ (ap↓ (ap to) u ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))) ⟩
{- 3 -}
    ((↯ 1# (to-from-glue-left' a b)) ◃ (ap↓ (ap to) (from-glue-glue a (b , c)) ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ idp ⟩

    ((↯ 1# (to-from-glue-left' a b)) ◃ (ap↓ (ap to) (↓-swap! left from-right _ idp
      (apd (λ x → glue (x , c)) (glue (a , b)) ▹! (FromRight.glue-β (b , c))))
    ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ Ap↓-swap!.β to left from-right _ idp (apd (λ x → glue (x , c)) (glue (a , b)) ▹! (FromRight.glue-β (b , c)))
                  |in-ctx (λ u → ((↯ 1# (to-from-glue-left' a b)) ◃ (u ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))) ⟩

    ((↯ 1# (to-from-glue-left' a b)) ◃ (((ap (λ u → u) (∘-ap to left (glue (a , b)))) ◃ ↓-swap! (to ∘ left) (to ∘ from-right) _ idp (ap↓ (ap to) (apd (λ x → glue (x , c)) (glue (a , b)) ▹! (FromRight.glue-β (b , c))) ▹ (ap (λ u → u) (∘-ap to from-right (glue (b , c))))))
    ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ ap-idf (∘-ap to left (glue (a , b))) |in-ctx (λ v → ((↯ 1# (to-from-glue-left' a b)) ◃ ((v ◃ ↓-swap! (to ∘ left) (to ∘ from-right) _ idp (ap↓ (ap to) (apd (λ x → glue (x , c)) (glue (a , b)) ▹! (FromRight.glue-β (b , c))) ▹ (ap (λ u → u) (∘-ap to from-right (glue (b , c))))))
    ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))) ⟩

    ((↯ 1# (to-from-glue-left' a b)) ◃ (((∘-ap to left (glue (a , b))) ◃ ↓-swap! (to ∘ left) (to ∘ from-right) _ idp (ap↓ (ap to) (apd (λ x → glue (x , c)) (glue (a , b)) ▹! (FromRight.glue-β (b , c))) ▹ (ap (λ u → u) (∘-ap to from-right (glue (b , c))))))
    ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ {!!} ⟩

    ((↯ 2# (to-from-glue-left' a b)) ◃ ((↓-swap! to-left (to ∘ from-right) _ idp (ap↓ (ap to) (apd (λ x → glue (x , c)) (glue (a , b)) ▹! (FromRight.glue-β (b , c))) ▹ (ap (λ u → u) (∘-ap to from-right (glue (b , c))))))
    ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ ap↓-▹! (ap to) (apd (λ x → glue (x , c)) (glue (a , b))) (FromRight.glue-β (b , c)) |in-ctx (λ v → ((↯ 2# (to-from-glue-left' a b)) ◃ ((↓-swap! to-left (to ∘ from-right) _ idp (v ▹ (ap (λ u → u) (∘-ap to from-right (glue (b , c))))))
    ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))) ⟩

    ((↯ 2# (to-from-glue-left' a b)) ◃ ((↓-swap! to-left (to ∘ from-right) _ idp ((ap↓ (ap to) (apd (λ x → glue (x , c)) (glue (a , b))) ▹! ap (ap to) (FromRight.glue-β (b , c))) ▹ (ap (λ u → u) (∘-ap to from-right (glue (b , c))))))
    ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ ∘'-apd (ap to) (λ x → glue (x , c)) (glue (a , b)) |in-ctx (λ v → ((↯ 2# (to-from-glue-left' a b)) ◃ ((↓-swap! to-left (to ∘ from-right) _ idp ((v ▹! ap (ap to) (FromRight.glue-β (b , c))) ▹ (ap (λ u → u) (∘-ap to from-right (glue (b , c))))))
    ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))) ⟩
{- 4 -}

    ((↯ 2# (to-from-glue-left' a b)) ◃ ((↓-swap! to-left (to ∘ from-right) _ idp ((apd (λ x → ap to (glue (x , c))) (glue (a , b)) ▹! ap (ap to) (FromRight.glue-β (b , c))) ▹ (ap (λ u → u) (∘-ap to from-right (glue (b , c))))))
    ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
               =⟨ {!!} ⟩
{- 5 -}

    -- ((↯ 2# (to-from-glue-left' a b)) ◃ ((↓-swap! to-left (to ∘ from-right) _ idp ((apd (λ x → to-glue (x , c)) (glue (a , b)) ▹! ap (ap to) (FromRight.glue-β (b , c))) ▹ (ap (λ u → u) (∘-ap to from-right (glue (b , c))))))
    -- ▹ (↯ 1! (to-from-glue-right' a c)))) ∙'2ᵈ (to-from-right-glue (b , c))
    --            =⟨ {!!} ⟩

-- {- 5 -}
--      (↯ 2# (to-from-glue-left' a b)) ◃ (↓-swap! to-left right _ idp (To.glue-β (left a , c) !◃ (apd (λ x → ap to (glue (x , c))) (glue (a , b)) ▹ To.glue-β (right b , c))))
--                =⟨ {!!} ⟩
     (↯ 2# (to-from-glue-left' a b)) ◃ (↓-swap! to-left right _ idp (apd (λ x → to-glue (x , c)) (glue (a , b))))
               =⟨ ToGlue.glue-β c (a , b) |in-ctx (λ v → (↯ 2# (to-from-glue-left' a b)) ◃ (↓-swap! to-left right _ idp v)) ⟩
{- 6 -}

     (↯ 2# (to-from-glue-left' a b)) ◃ (↓-swap! to-left right _ idp (to-glue-glue c (a , b)))
               =⟨ ↓-swap-β to-left right {p = glue (a , b)} (to-glue-left c a) idp (ToLeft.glue-β (a , b) ◃ apd (λ x → glue (a , x)) (glue (b , c))) |in-ctx (λ v → (↯ 2# (to-from-glue-left' a b)) ◃ v) ⟩
     (↯ 2# (to-from-glue-left' a b)) ◃ (ToLeft.glue-β (a , b) ◃ apd (λ x → glue (a , x)) (glue (b , c)))
               =⟨ {!!} ⟩ -- associativity
     (↯ to-from-glue-left' a b) ◃ apd (λ x → glue (a , x)) (glue (b , c)) ∎))

       -- ((↓-apd-out (λ a' _ → to (from (left a)) == to (from (right a'))) (λ x → glue (a , x)) (glue (b , c)) (apdd (ap to ∘ ap from) (glue (b , c)) (apd (λ x → (glue (a , x))) (glue (b , c))))) ∙'2ᵈ (to-from-right-glue (b , c))) ▹ to-from-glue-right' a c =⟨ {!!} ⟩

    -- to-from-glue-glue : (a : A) (bc : B × C)
    --  → to-from-glue-left a (fst bc) == to-from-glue-right a (snd bc) [ (λ x → to-from-left a == to-from-right x [ (λ y → to (from y) == y) ↓ glue (a , x) ]) ↓ glue bc ]
    -- to-from-glue-glue a (b , c) = {!!}  -- Should not be too hard

    -- to-from-glue : (x : A × (B * C)) → to-from-left (fst x) == to-from-right (snd x) [ (λ x → to (from x) == x) ↓ glue x ]
    -- to-from-glue (a , bc) = pushout-rec (to-from-glue-left a) (to-from-glue-right a) (to-from-glue-glue a) bc

    -- to-from : (x : A * (B * C)) → to (from x) == x
    -- to-from = pushout-rec to-from-left to-from-right to-from-glue

  -- *-assoc : (A * B) * C ≃ A * (B * C)
  -- *-assoc = equiv to from to-from from-to