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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.SIP
open import Cubical.Data.Sigma
open import Cubical.Data.Int renaming (_+_ to _+Int_ ; _-_ to _-Int_)
open import Cubical.Data.Unit

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Semigroup
open import Cubical.Foundations.HLevels

private
  variable
    ℓ : Level

record IsGroup {G : Type ℓ}
               (0g : G) (_+_ : G → G → G) (-_ : G → G) : Type ℓ where

  constructor isgroup

  field
    isMonoid  : IsMonoid 0g _+_
    inverse   : (x : G) → (x + (- x) ≡ 0g) × ((- x) + x ≡ 0g)

  open IsMonoid isMonoid public

  infixl 6 _-_

  _-_ : G → G → G
  x - y = x + (- y)

  invl : (x : G) → (- x) + x ≡ 0g
  invl x = inverse x .snd

  invr : (x : G) → x + (- x) ≡ 0g
  invr x = inverse x .fst

record GroupStr (G : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor groupstr

  field
    0g      : G
    _+_     : G → G → G
    -_      : G → G
    isGroup : IsGroup 0g _+_ -_

  infix  8 -_
  infixr 7 _+_

  open IsGroup isGroup public

Group : Type (ℓ-suc ℓ)
Group = TypeWithStr _ GroupStr

Group₀ : Type₁
Group₀ = Group {ℓ-zero}

group : (G : Type ℓ) (0g : G) (_+_ : G → G → G) (-_ : G → G) (h : IsGroup 0g _+_ -_) → Group
group G 0g _+_ -_ h = G , groupstr 0g _+_ -_ h

isSetGroup : (G : Group {ℓ}) → isSet ⟨ G ⟩
isSetGroup G = GroupStr.isGroup (snd G) .IsGroup.isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

makeIsGroup : {G : Type ℓ} {0g : G} {_+_ : G → G → G} { -_ : G → G}
              (is-setG : isSet G)
              (assoc : (x y z : G) → x + (y + z) ≡ (x + y) + z)
              (rid : (x : G) → x + 0g ≡ x)
              (lid : (x : G) → 0g + x ≡ x)
              (rinv : (x : G) → x + (- x) ≡ 0g)
              (linv : (x : G) → (- x) + x ≡ 0g)
            → IsGroup 0g _+_ -_
IsGroup.isMonoid (makeIsGroup is-setG assoc rid lid rinv linv) = makeIsMonoid is-setG assoc rid lid
IsGroup.inverse (makeIsGroup is-setG assoc rid lid rinv linv) = λ x → rinv x , linv x

makeGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
            (is-setG : isSet G)
            (assoc : (x y z : G) → x + (y + z) ≡ (x + y) + z)
            (rid : (x : G) → x + 0g ≡ x)
            (lid : (x : G) → 0g + x ≡ x)
            (rinv : (x : G) → x + (- x) ≡ 0g)
            (linv : (x : G) → (- x) + x ≡ 0g)
          → Group
makeGroup 0g _+_ -_ is-setG assoc rid lid rinv linv = _ , helper
  where
  helper : GroupStr _
  GroupStr.0g helper = 0g
  GroupStr._+_ helper = _+_
  GroupStr.- helper = -_
  GroupStr.isGroup helper = makeIsGroup is-setG assoc rid lid rinv linv

makeGroup-right : ∀ {ℓ} {A : Type ℓ}
  → (id : A)
  → (comp : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (assoc : ∀ a b c → comp a (comp b c) ≡ comp (comp a b) c)
  → (rUnit : ∀ a → comp a id ≡ a)
  → (rCancel : ∀ a → comp a (inv a) ≡ id)
  → Group
makeGroup-right id comp inv set assoc rUnit rCancel =
  makeGroup id comp inv set assoc rUnit lUnit rCancel lCancel
  where
    _⨀_ = comp
    abstract
      lCancel : ∀ a → comp (inv a) a ≡ id
      lCancel a =
        inv a ⨀ a
          ≡⟨ sym (rUnit (comp (inv a) a))  ⟩
        (inv a ⨀ a) ⨀ id
          ≡⟨ cong (comp (comp (inv a) a)) (sym (rCancel (inv a))) ⟩
        (inv a ⨀ a) ⨀ (inv a ⨀ (inv (inv a)))
          ≡⟨ assoc _ _ _ ⟩
        ((inv a ⨀ a) ⨀ (inv a)) ⨀ (inv (inv a))
          ≡⟨ cong (λ □ → □ ⨀ _) (sym (assoc _ _ _)) ⟩
        (inv a ⨀ (a ⨀ inv a)) ⨀ (inv (inv a))
          ≡⟨ cong (λ □ → (inv a ⨀ □) ⨀ (inv (inv a))) (rCancel a) ⟩
        (inv a ⨀ id) ⨀ (inv (inv a))
          ≡⟨ cong (λ □ → □ ⨀ (inv (inv a))) (rUnit (inv a)) ⟩
        inv a ⨀ (inv (inv a))
          ≡⟨ rCancel (inv a) ⟩
        id
          ∎

      lUnit : ∀ a → comp id a ≡ a
      lUnit a =
        id ⨀ a
          ≡⟨ cong (λ b → comp b a) (sym (rCancel a)) ⟩
        (a ⨀ inv a) ⨀ a
          ≡⟨ sym (assoc _ _ _) ⟩
        a ⨀ (inv a ⨀ a)
          ≡⟨ cong (comp a) (lCancel a) ⟩
        a ⨀ id
          ≡⟨ rUnit a ⟩
        a
          ∎

makeGroup-left : ∀ {ℓ} {A : Type ℓ}
  → (id : A)
  → (comp : A → A → A)
  → (inv : A → A)
  → (set : isSet A)
  → (assoc : ∀ a b c → comp a (comp b c) ≡ comp (comp a b) c)
  → (lUnit : ∀ a → comp id a ≡ a)
  → (lCancel : ∀ a → comp (inv a) a ≡ id)
  → Group
makeGroup-left id comp inv set assoc lUnit lCancel =
  makeGroup id comp inv set assoc rUnit lUnit rCancel lCancel
  where
    abstract
      rCancel : ∀ a → comp a (inv a) ≡ id
      rCancel a =
        comp a (inv a)
          ≡⟨ sym (lUnit (comp a (inv a)))  ⟩
        comp id (comp a (inv a))
          ≡⟨ cong (λ b → comp b (comp a (inv a))) (sym (lCancel (inv a))) ⟩
        comp (comp (inv (inv a)) (inv a)) (comp a (inv a))
          ≡⟨ sym (assoc (inv (inv a)) (inv a) (comp a (inv a))) ⟩
        comp (inv (inv a)) (comp (inv a) (comp a (inv a)))
          ≡⟨ cong (comp (inv (inv a))) (assoc (inv a) a (inv a)) ⟩
        comp (inv (inv a)) (comp (comp (inv a) a) (inv a))
          ≡⟨ cong (λ b → comp (inv (inv a)) (comp b (inv a))) (lCancel a) ⟩
        comp (inv (inv a)) (comp id (inv a))
          ≡⟨ cong (comp (inv (inv a))) (lUnit (inv a)) ⟩
        comp (inv (inv a)) (inv a)
          ≡⟨ lCancel (inv a) ⟩
        id
          ∎

      rUnit : ∀ a → comp a id ≡ a
      rUnit a =
        comp a id
          ≡⟨ cong (comp a) (sym (lCancel a)) ⟩
        comp a (comp (inv a) a)
          ≡⟨ assoc a (inv a) a ⟩
        comp (comp a (inv a)) a
          ≡⟨ cong (λ b → comp b a) (rCancel a) ⟩
        comp id a
          ≡⟨ lUnit a ⟩
        a
          ∎

open GroupStr hiding (0g ; _+_ ; -_)

isSetCarrier : ∀ {ℓ} → (G : Group {ℓ}) → isSet ⟨ G ⟩
isSetCarrier G = IsSemigroup.is-set (IsMonoid.isSemigroup (GroupStr.isMonoid (snd G)))

open GroupStr

dirProd : ∀ {ℓ ℓ'} → Group {ℓ} → Group {ℓ'} → Group
dirProd (GC , G) (HC , H) =
  makeGroup (0g G , 0g H)
            (λ { (x1 , x2) (y1 , y2) → _+_ G x1 y1 , _+_ H x2 y2 })
            (λ { (x1 , x2) → -_ G x1 , -_ H x2 })
            (isSet× (isSetCarrier (GC , G)) (isSetCarrier (HC , H)))
            (λ { (x1 , x2) (y1 , y2) (z1 , z2) i →
               assoc G x1 y1 z1 i , assoc H x2 y2 z2 i })
            (λ { (x1 , x2) i → GroupStr.rid G x1 i , GroupStr.rid H x2 i })
            (λ { (x1 , x2) i → GroupStr.lid G x1 i , GroupStr.lid H x2 i })
            (λ { (x1 , x2) i → GroupStr.invr G x1 i , GroupStr.invr H x2 i })
            (λ { (x1 , x2) i → GroupStr.invl G x1 i , GroupStr.invl H x2 i })

trivialGroup : Group₀
trivialGroup = Unit , groupstr tt (λ _ _ → tt) (λ _ → tt)
                      (makeIsGroup isSetUnit (λ _ _ _ → refl) (λ _ → refl) (λ _ → refl)
                                   (λ _ → refl) (λ _ → refl))

intGroup : Group₀
intGroup = Int , groupstr 0 _+Int_ (0 -Int_)
                 (makeIsGroup isSetInt +-assoc (λ x → refl) (λ x → +-comm 0 x)
                              (λ x → +-comm x (pos 0 -Int x) ∙ minusPlus x 0) (λ x → minusPlus x 0))

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


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

module n2o.Network.WebSocket where

open import proto.Base
open import proto.IO

open import n2o.Network.Internal

{-# FOREIGN GHC import Network.N2O.Web.WebSockets #-}

data N2OProto (A : Set) : Set where
    Io  : ByteString Strict → ByteString Strict → N2OProto A
    Nop :                                         N2OProto A

Cx : Set → Set
Cx = Context N2OProto

CxHandler : Set → Set
CxHandler a = Cx a → Cx a

-- mkHandler : ∀ {A : Set} (h : Set → IO A) → Set → IO A
-- mkHandler h m = h m >> return Empty -- TODO : monad instance for Result

postulate
    runServer : ∀ {A : Set} → String → ℤ → Context N2OProto A → IO ⊤

{-# COMPILE GHC        Cx =      Network.N2O.Web.WebSockets.Cx                    #-}
{-# COMPILE GHC CxHandler =      Network.N2O.Web.WebSockets.CxHandler             #-}
{-# COMPILE GHC runServer =      Network.N2O.Web.WebSockets.runServer             #-}
{-# COMPILE GHC  N2OProto = data Network.N2O.Web.Websockets.N2OProto ( Io | Nop ) #-}

ext: agda


text:
-- Andreas, 2012-11-22 abstract aliases
module Issue729 where

abstract
  B = Set
  B₁ = B
  B₂ = Set

abstract
  foo : Set₁
  foo = x
    where x = B

{- does not work yet
mutual
 abstract
  D = C
  C = B
-}

-- other stuff

private
  A = Set

Y = let X = Set in Set

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module root2 where

-- imports. We use the latest agda stdlib.
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum renaming (inj₁ to even ; inj₂ to odd)
open import Relation.Nullary
open import Data.Empty

-- Even predicate.
Even : ℕ -> Set
Even n = ∃ λ k → n ≡ 2 * k

-- Odd predicate.
Odd : ℕ -> Set
Odd n = ∃ λ k → n ≡ 1 + 2 * k

open +-*-Solver

-- Lemma: an even number cannot equal to an odd number.
lemma-even-odd-exclusive : ∀ k l ->  ¬ 2 * k ≡ 1 + 2 * l
lemma-even-odd-exclusive k l hyp = z hyp'
  where
    z : ¬ 0 ≡ 1
    z ()

    n*m%n≡0 : ∀ m n .{{_ : NonZero n}} → (n * m) % n ≡ 0
    n*m%n≡0 m n = begin
        (n * m) % n ≡⟨ cong (_% n) (solve 2 (λ n m → n :* m := m :* n) refl n m) ⟩
        (m * n) % n ≡⟨ m*n%n≡0 m n ⟩
        0 ∎
        where
          open ≡-Reasoning

    lem1%2 : 1 % 2 ≡ 1
    lem1%2 = refl

    hyp' : 0 ≡ 1
    hyp' =  begin
        0 ≡⟨ sym (n*m%n≡0 k 2)  ⟩
        (2 * k) % 2 ≡⟨ cong (_% 2) hyp ⟩
        (1 + 2 * l) % 2 ≡⟨ %-distribˡ-+ 1 (2 * l) 2 ⟩
        ((1 % 2) + ((2 * l) % 2)) % 2 ≡⟨ cong (_% 2) (cong₂ (_+_) lem1%2 (n*m%n≡0 l 2)) ⟩
        (1 + 0) % 2 ≡⟨ refl ⟩
        1 % 2 ≡⟨ refl ⟩
        1 ∎
        where
          open ≡-Reasoning

-- Lemma: a natural number cannot be both even and odd.
lemma-even-odd-exclusive' : ∀ n -> ¬ (Even n × Odd n)
lemma-even-odd-exclusive' n ((k , eqn) , (l , eqn')) = lemma-even-odd-exclusive k l claim
  where
    claim : 2 * k ≡ 1 + 2 * l
    claim = begin
        2 * k ≡⟨ sym eqn ⟩
        n ≡⟨ eqn' ⟩
        1 + 2 * l ∎
        where
          open ≡-Reasoning

-- Lemma: a natrual number is either even or odd (but not both as shown by lemma-even-odd-exclusive').
Parity : (n : ℕ) -> Even n ⊎ Odd n
Parity zero = even (zero , refl)
Parity (suc n) with Parity n
... | even (k , eq) = odd (k , cong suc eq)
... | odd (k , eq) = even (suc k , claim)
  where
    claim : suc n ≡ suc (k + suc (k + 0))
    claim = begin
      suc n ≡⟨ refl ⟩
      1 + n ≡⟨ cong (1 +_) eq ⟩
      1 +  suc (k + (k + 0)) ≡⟨ solve 1 (λ k → con 1 :+ (con 1 :+ (k :+ (k :+ con 0))) := con 1 :+ (k :+ (con 1 :+ (k :+ con 0)))) refl k ⟩
      1 + (k + (1 + (k + 0))) ≡⟨ refl ⟩
      suc (k + suc (k + 0)) ∎
      where
        open ≡-Reasoning

-- Auxillary lemmas:
lemma-div2 : ∀ n .{{_ : NonZero n}} -> n / 2 < n
lemma-div2 n = m/n<m n 2 (s≤s (s≤s z≤n))

lemma-<-< : ∀ {a b c} -> a < b -> b < suc c -> a < c
lemma-<-<  (s≤s ab) (s≤s bc) = <-transˡ (s≤s ab) bc

lemma-div2' : ∀ n b .{{_ : NonZero n}} -> n < 1 + b -> n / 2 < b
lemma-div2' n b n1b = lemma-<-< (lemma-div2 n) n1b

-- We do a case split in the parity of m and n. For each of the four
-- cases, we can derive a contradiction using induction on the bound
-- of m and n.
lemma-root2-irra : ∀ b m n -> ¬ m ≡ 0 -> ¬ n ≡ 0 → m < b → n < b → ¬ m * m ≡ 2 * (n * n)
lemma-root2-irra (suc b) 0 0 mnz nnz mlb nlb hyp = mnz refl
lemma-root2-irra (suc b) 0 (suc n) mnz nnz mlb nlb hyp = mnz refl
lemma-root2-irra (suc b) (suc m) 0 mnz nnz mlb nlb hyp = nnz refl
lemma-root2-irra (suc b) m@(suc m') n@(suc n') mnz nnz mlb nlb hyp with Parity m | Parity n
... | even (k , eqm) | even (l , eqn) = ih
  where
    factor-four : 4 * (k * k) ≡ 4 * (2 * (l * l))
    factor-four = begin
      4 * (k * k) ≡⟨ solve 1 (λ k → con 4 :* (k :* k) := (con 2 :* k) :* (con 2 :* k)) refl k ⟩
      (2 * k) * (2 * k) ≡⟨ cong₂ _*_ (sym eqm) (sym eqm) ⟩
      m * m ≡⟨ hyp ⟩
      2 * (n * n) ≡⟨ cong (2 *_) (cong₂ _*_ eqn eqn) ⟩
      2 * ((2 * l) * (2 * l)) ≡⟨ solve 1 (λ l → con 2 :* ((con 2 :* l) :* (con 2 :* l)) := con 4 :* (con 2 :* (l :* l))) refl l ⟩
      4 * (2 * (l * l)) ∎
      where
        open ≡-Reasoning

    hyp' : k * k ≡ 2 * (l * l)
    hyp' = *-cancelˡ-≡ 4 factor-four

    klb : k < b
    klb = begin-strict
      k ≡⟨ sym (m*n/n≡m k 2) ⟩
      (k * 2) / 2 ≡⟨ cong (_/ 2) (solve 1 (λ k → k :* con 2 := con 2 :* k) refl k) ⟩
      (2 * k) / 2 ≡⟨ cong (_/ 2) (sym eqm) ⟩
      m / 2 <⟨ lemma-div2' m b mlb ⟩
      b ∎
      where
        open ≤-Reasoning

    llb : l < b
    llb = begin-strict
      l ≡⟨ sym (m*n/n≡m l 2) ⟩
      (l * 2) / 2 ≡⟨ cong (_/ 2) (solve 1 (λ l → l :* con 2 := con 2 :* l) refl l) ⟩
      (2 * l) / 2 ≡⟨ cong (_/ 2) (sym eqn) ⟩
      n / 2 <⟨ lemma-div2' n b nlb ⟩
      b ∎
      where
        open ≤-Reasoning

    knz : ¬ k ≡ 0
    knz k0 = mnz m0
      where
      m0 : m ≡ 0
      m0 = begin
        m ≡⟨ eqm ⟩
        2 * k ≡⟨ cong (2 *_) k0 ⟩
        2 * 0 ≡⟨ refl ⟩
        0 ∎
        where
          open ≡-Reasoning

    lnz : ¬ l ≡ 0
    lnz l0 = nnz n0
      where
      n0 : n ≡ 0
      n0 = begin
        n ≡⟨ eqn ⟩
        2 * l ≡⟨ cong (2 *_) l0 ⟩
        2 * 0 ≡⟨ refl ⟩
        0 ∎
        where
          open ≡-Reasoning

    ih : ⊥
    ih = lemma-root2-irra b k l knz lnz klb llb hyp'

... | even (k , eqm) | odd (l , eqn) = lemma-even-odd-exclusive' (n * n) (even-right , odd-right)
  where
    even-left : Even (m * m)
    even-left = 2 * (k * k) , claim
      where
        claim : m * m ≡ 2 * (2 * (k * k))
        claim = begin
          m * m ≡⟨ cong₂ _*_ eqm eqm ⟩
          (2 * k) * (2 * k) ≡⟨ solve 1 (λ k → (con 2 :* k) :* (con 2 :* k) := con 2 :* (con 2 :* (k :* k))) refl k ⟩
          2 * (2 * (k * k)) ∎
            where
              open ≡-Reasoning

    odd-right : Odd (n * n)
    odd-right = (2 * (l * l) + 2 * l) , claim
      where
        claim : n * n ≡ 1 + 2 * (2 * (l * l) + 2 * l)
        claim = begin
          n * n ≡⟨ cong₂ _*_ eqn eqn ⟩
          (1 + 2 * l) * (1 + 2 * l) ≡⟨ solve 1 (λ l → (con 1 :+ con 2 :* l) :* (con 1 :+ con 2 :* l) := con 1 :+ (con 2 :* ((con 2 :* (l :* l)) :+ con 2 :* l))) refl l ⟩
          1 + 2 * (2 * (l * l) + 2 * l)  ∎
            where
              open ≡-Reasoning

    2*n*n≡2*2*k*k : 2 * (n * n) ≡ 2 * (2 * (k * k))
    2*n*n≡2*2*k*k = begin
          2 * (n * n) ≡⟨ sym hyp ⟩
          m * m ≡⟨ (let (_ , p) = even-left in p) ⟩
          2 * (2 * (k * k)) ∎
            where
              open ≡-Reasoning

    n*n≡2*k*k : (n * n) ≡ (2 * (k * k))
    n*n≡2*k*k = *-cancelˡ-≡ 2 2*n*n≡2*2*k*k

    even-right : Even (n * n)
    even-right = k * k , (n*n≡2*k*k)

... | odd (k , eqn) | _  = lemma-even-odd-exclusive' (m * m) (even-left , odd-left)
  where
    odd-left : Odd (m * m)
    odd-left = (2 * (k * k) + 2 * k) , claim
      where
        claim : m * m ≡ 1 + 2 * (2 * (k * k) + 2 * k)
        claim = begin
          m * m ≡⟨ cong₂ _*_ eqn eqn ⟩
          (1 + 2 * k) * (1 + 2 * k) ≡⟨ solve 1 (λ k → (con 1 :+ con 2 :* k) :* (con 1 :+ con 2 :* k) := con 1 :+ (con 2 :* ((con 2 :* (k :* k)) :+ con 2 :* k))) refl k ⟩
          1 + 2 * (2 * (k * k) + 2 * k)  ∎
            where
              open ≡-Reasoning

    even-left : Even (m * m)
    even-left = (n * n) , hyp

-- Main theorem: for any natural number m and n, it impossible that m
-- * m ≡ 2 * (n * n) except when m ≡ 0 and n ≡ 0 (in this situation,
-- m/n is not defined), in other words, no rational number equals √2.
theorem-root2-irra : ∀ m n ->  m * m ≡ 2 * (n * n) -> m ≡ 0 × n ≡ 0
theorem-root2-irra zero zero hyp = (refl , refl )
theorem-root2-irra zero n@(suc n') hyp = (refl , sym 0≡n )
  where
    2*0≡2*n*n : 2 * 0 ≡ 2 * (n * n)
    2*0≡2*n*n = hyp
    0≡n*n : 0 ≡ n * n
    0≡n*n = *-cancelˡ-≡ 2 hyp
    n*0≡n*n : n * 0 ≡ n * n
    n*0≡n*n = begin
          n * 0 ≡⟨ *-comm n 0 ⟩
          0 * n ≡⟨ refl ⟩
          0  ≡⟨ 0≡n*n ⟩
          n * n  ∎
            where
              open ≡-Reasoning

    0≡n : 0 ≡ n
    0≡n = *-cancelˡ-≡ n n*0≡n*n

theorem-root2-irra m@(suc m') n@(suc n') hyp = ⊥-elim claim
  where
    -- m ⊔ n = max m n
    b = 1 + (m ⊔ n)
    mlb : m < b
    mlb = s≤s (m≤m⊔n m n)
    nlb : n < b
    nlb = s≤s (m≤n⊔m m n)
    claim = lemma-root2-irra b m n (λ ()) (λ ()) mlb nlb hyp


text:
module pretty where
open import general-util

-- Adapted from A Prettier Printer (Philip Wadler)
-- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf

-- The pretty printer
infixr 5 _:<|>_
infixr 6 _:<>_
infixr 6 _<>_

data DOC : Set where
  NIL : DOC
  _:<>_ : DOC → DOC → DOC
  NEST : ℕ → DOC → DOC
  TEXT : rope → DOC
  LINE : DOC
  _:<|>_ : DOC → DOC → DOC

data Doc : Set where
  Nil : Doc
  _Text_ : rope → Doc → Doc
  _Line_ : ℕ → Doc → Doc

nil = NIL
_<>_ = _:<>_
nest = NEST
text = TEXT
line = LINE

flatten : DOC → DOC
flatten NIL = NIL
flatten (x :<> y) = flatten x :<> flatten y
flatten (NEST i x) = NEST i (flatten x)
flatten (TEXT s) = TEXT s
flatten LINE = TEXT [[ " " ]]
flatten (x :<|> y) = flatten x

flatten-out : DOC → rope
flatten-out NIL = [[]]
flatten-out (x :<> y) = flatten-out x ⊹⊹ flatten-out y
flatten-out (NEST i x) = flatten-out x
flatten-out (TEXT s) = s
flatten-out LINE = [[ " " ]]
flatten-out (x :<|> y) = flatten-out x

group = λ x → flatten x :<|> x

fold : ∀ {ℓ} {X : Set ℓ} → ℕ → X → (X → X) → X
fold 0 z s = z
fold (suc n) z s = s (fold n z s)

copy : ∀ {ℓ} {X : Set ℓ} → ℕ → X → 𝕃 X
copy i x = fold i [] (x ::_)

layout : Doc → rope
layout Nil = [[]]
layout (s Text x) = s ⊹⊹ layout x
layout (i Line x) = [[ 𝕃char-to-string ('\n' :: copy i ' ') ]] ⊹⊹ layout x

_∸'_ : ℕ → ℕ → maybe ℕ
m ∸' n with suc m ∸ n
...| zero = nothing
...| suc o = just o

fits : maybe ℕ → Doc → 𝔹
fits nothing x  = ff
fits (just w) Nil = tt
fits (just w) (s Text x) = fits (w ∸' rope-length s) x
fits (just w) (i Line x) = tt

{-# TERMINATING #-}
be : ℕ → ℕ → 𝕃 (ℕ × DOC) → Doc
better : ℕ → ℕ → Doc → Doc → Doc
best : ℕ → ℕ → DOC → Doc

better w k x y = if fits (w ∸' k) x then x else y
best w k x = be w k [ 0 , x ]

be w k [] = Nil
be w k ((i , NIL) :: z) = be w k z
be w k ((i , x :<> y) :: z) = be w k ((i , x) :: (i , y) :: z)
be w k ((i , NEST j x) :: z) = be w k ((i + j , x) :: z)
be w k ((i , TEXT s) :: z) = s Text be w (k + rope-length s) z
be w k ((i , LINE) :: z) = i Line be w i z
be w k ((i , x :<|> y) :: z) = better w k (be w k ((i , x) :: z)) (be w k ((i , y) :: z))

pretty : ℕ → DOC → rope
pretty w x = layout (best w 0 x)

-- Utility functions

infixr 6 _<+>_ _</>_ _<+/>_
_<+>_ : DOC → DOC → DOC
x <+> y = x <> text [[ " " ]] <> y
_</>_ : DOC → DOC → DOC
x </> y = x <> line <> y

folddoc : (DOC → DOC → DOC) → 𝕃 DOC → DOC
folddoc f [] = nil
folddoc f (x :: []) = x
folddoc f (x :: xs) = f x (folddoc f xs)

spread = folddoc _<+>_

stack = folddoc _</>_

bracket : string → DOC → string → DOC
bracket l x r = group (text [[ l ]] <> nest 2 (line <> x) <> line <> text [[ r ]])

_<+/>_ : DOC → DOC → DOC
x <+/> y = x <> (text [[ " " ]] :<|> line) <> y

{-# TERMINATING #-}
fill : 𝕃 DOC → DOC
fill [] = nil
fill (x :: []) = x
fill (x :: y :: zs) = (flatten x <+> fill (flatten y :: zs)) :<|> (x </> fill (y :: zs))

{-# TERMINATING #-}
filln : 𝕃 (ℕ × DOC) → DOC
filln [] = nil
filln ((i , x) :: []) = nest i x
filln ((i , x) :: (j , y) :: zs) =
  (flatten x <+> filln ((j , flatten y) :: zs))
    :<|> (nest i x <> nest j line <> filln ((j , y) :: zs))

{-# TERMINATING #-}
fill-last : ℕ → 𝕃 DOC → DOC
fill-last i [] = nil
fill-last i (x :: []) = nest i x
fill-last i (x :: y :: []) = (flatten x <+> flatten y) :<|> (nest i (x </> y))
fill-last i (x :: y :: zs) = (flatten x <+> fill-last i (flatten y :: zs)) :<|> (x </> fill-last i (y :: zs))

max_stars_repo_name: mudathirmahgoub/cedille

max_issues_repo_name: mudathirmahgoub/cedille

max_forks_repo_name: mudathirmahgoub/cedille


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

open import Categories.Category.Core using (Category)

module Categories.Diagram.Pushout {o ℓ e} (C : Category o ℓ e) where

open Category C
open HomReasoning

open import Level

private
  variable
    A B E X Y Z : Obj

record Pushout (f : X ⇒ Y) (g : X ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
  field
    {Q} : Obj
    i₁  : Y ⇒ Q
    i₂  : Z ⇒ Q

  field
    commute   : i₁ ∘ f ≈ i₂ ∘ g
    universal : {h₁ : Y ⇒ B} {h₂ : Z ⇒ B} → h₁ ∘ f ≈ h₂ ∘ g → Q ⇒ B
    unique    : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {j : Q ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} →
                  j ∘ i₁ ≈ h₁ → j ∘ i₂ ≈ h₂ →
                  j ≈ universal eq

    universal∘i₁≈h₁  : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} →
                         universal eq ∘ i₁ ≈ h₁
    universal∘i₂≈h₂  : {h₁ : Y ⇒ E} {h₂ : Z ⇒ E} {eq : h₁ ∘ f ≈ h₂ ∘ g} →
                         universal eq ∘ i₂ ≈ h₂

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module Prelude.Product where

open import Agda.Primitive
open import Agda.Builtin.Sigma public
open import Prelude.Function
open import Prelude.Equality
open import Prelude.Decidable
open import Prelude.Ord

instance
  ipair : ∀ {a b} {A : Set a} {B : A → Set b} {{x : A}} {{y : B x}} → Σ A B
  ipair {{x}} {{y}} = x , y

infixr 3 _×_
_×_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
A × B = Σ A (λ _ → B)

_,′_ : ∀ {a b} {A : Set a} {B : Set b} → A → B → A × B
_,′_ = _,_

uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c} →
            (∀ x (y : B x) → C x y) → (p : Σ A B) → C (fst p) (snd p)
uncurry f (x , y) = f x y

uncurry′ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Set c} →
            (∀ x → B x → C) → Σ A B → C
uncurry′ f (x , y) = f x y

curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
          (∀ p → C p) → ∀ x (y : B x) → C (x , y)
curry f x y = f (x , y)

infixr 3 _***_ _***′_ _&&&_
_***_ : ∀ {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
          (f : A₁ → A₂) → (∀ {x} → B₁ x → B₂ (f x)) → Σ A₁ B₁ → Σ A₂ B₂
(f *** g) (x , y) = f x , g y

_***′_ : ∀ {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : Set b₁} {B₂ : Set b₂} →
          (A₁ → A₂) → (B₁ → B₂) → A₁ × B₁ → A₂ × B₂
(f ***′ g) (x , y) = f x , g y

_&&&_ : ∀ {c a b} {C : Set c} {A : Set a} {B : A → Set b}
          (f : C → A) → (∀ x → B (f x)) → C → Σ A B
(f &&& g) x = f x , g x

first : ∀ {a₁ a₂ b} {A₁ : Set a₁} {A₂ : Set a₂} {B : Set b} →
          (A₁ → A₂) → A₁ × B → A₂ × B
first f = f *** id

second : ∀ {a b₁ b₂} {A : Set a} {B₁ : A → Set b₁} {B₂ : A → Set b₂} →
           (∀ {x} → B₁ x → B₂ x) → Σ A B₁ → Σ A B₂
second f = id *** f

-- Eq instance --

sigma-inj-fst : ∀ {a b} {A : Set a} {B : A → Set b} {x : A} {y : B x}
                 {x₁ : A} {y₁ : B x₁} →
               (x , y) ≡ (x₁ , y₁) → x ≡ x₁
sigma-inj-fst refl = refl

sigma-inj-snd : ∀ {a b} {A : Set a} {B : A → Set b} {x : A} {y y₁ : B x} →
               _≡_ {A = Σ A B} (x , y) (x , y₁) → y ≡ y₁
sigma-inj-snd refl = refl

instance
  EqSigma : ∀ {a b} {A : Set a} {B : A → Set b} {{EqA : Eq A}} {{EqB : ∀ {x} → Eq (B x)}} → Eq (Σ A B)
  _==_ {{EqSigma}} (x , y) (x₁ , y₁) with x == x₁
  _==_ {{EqSigma}} (x , y) (x₁ , y₁) | no  neq  = no λ eq → neq (sigma-inj-fst eq)
  _==_ {{EqSigma}} (x , y) (.x , y₁) | yes refl with y == y₁
  _==_ {{EqSigma}} (x , y) (.x , y₁) | yes refl | no neq = no λ eq → neq (sigma-inj-snd eq)
  _==_ {{EqSigma}} (x , y) (.x , .y) | yes refl | yes refl = yes refl

-- Ord instance --

data LexiographicOrder {a b} {A : Set a} {B : A → Set b}
                       (_<A_ : A → A → Set a) (_<B_ : ∀ {x} → B x → B x → Set b) :
                       Σ A B → Σ A B → Set (a ⊔ b) where
  fst< : ∀ {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂} → x₁ <A x₂ → LexiographicOrder _<A_ _<B_ (x₁ , y₁) (x₂ , y₂)
  snd< : ∀ {x} {y₁ y₂ : B x} → y₁ <B y₂ → LexiographicOrder _<A_ _<B_ (x , y₁) (x , y₂)

module _ {a b} {A : Set a} {B : A → Set b} {{OrdA : Ord A}} {{OrdB : ∀ {x} → Ord (B x)}} where
  private
    cmpSigma : (x y : Σ A B) → Comparison (LexiographicOrder _<_ _<_) x y
    cmpSigma (x , y)  (x₁ , y₁)  with compare x x₁
    cmpSigma (x , y)  (x₁ , y₁)  | less x<x₁    = less    (fst< x<x₁)
    cmpSigma (x , y)  (x₁ , y₁)  | greater x₁<x = greater (fst< x₁<x)
    cmpSigma (x , y)  (.x , y₁)  | equal refl with compare y y₁
    cmpSigma (x₁ , y) (.x₁ , y₁) | equal refl | less y<y₁    = less    (snd< y<y₁)
    cmpSigma (x₁ , y) (.x₁ , y₁) | equal refl | greater y₁<y = greater (snd< y₁<y)
    cmpSigma (x₁ , y) (.x₁ , .y) | equal refl | equal refl   = equal refl

    from-eq : (x y : Σ A B) → x ≡ y → LexiographicOrder _<_ _≤_ x y
    from-eq (x , y) (.x , .y) refl = snd< (eq-to-leq (refl {x = y}))

    from-lt : (x y : Σ A B) → LexiographicOrder _<_ _<_ x y → LexiographicOrder _<_ _≤_ x y
    from-lt (x₁ , y₁) (x₂ , y₂) (fst< lt) = fst< lt
    from-lt (x  , y₁) (.x , y₂) (snd< lt) = snd< (lt-to-leq {x = y₁} lt)

    from-leq : (x y : Σ A B) → LexiographicOrder _<_ _≤_ x y → LessEq (LexiographicOrder _<_ _<_) x y
    from-leq (a , b) (a₁ , b₁) (fst< a<a₁) = less (fst< a<a₁)
    from-leq (a , b) (.a , b₁) (snd< b≤b₁) with leq-to-lteq {{OrdB}} b≤b₁
    ... | less b<b₁  = less (snd< b<b₁)
    ... | equal b=b₁ = equal ((a ,_) $≡ b=b₁)

  instance
    OrdSigma : Ord (Σ A B)
    Ord._<_         OrdSigma = _
    Ord._≤_         OrdSigma = LexiographicOrder _<_ _≤_
    Ord.compare     OrdSigma = cmpSigma
    Ord.eq-to-leq   OrdSigma = from-eq _ _
    Ord.lt-to-leq   OrdSigma = from-lt _ _
    Ord.leq-to-lteq OrdSigma = from-leq _ _

module _ {a b} {A : Set a} {B : A → Set b} {{OrdA : Ord/Laws A}} {{OrdB : ∀ {x} → Ord/Laws (B x)}} where

    OrdLawsSigma : Ord/Laws (Σ A B)
    Ord/Laws.super OrdLawsSigma = OrdSigma {{OrdB = OrdB .Ord/Laws.super}}
    less-antirefl {{OrdLawsSigma}} (fst< lt)                    = less-antirefl {A = A} lt
    less-antirefl {{OrdLawsSigma}} (snd< {x = x} lt)            = less-antirefl {A = B x} lt
    less-trans    {{OrdLawsSigma}} (fst<         lt) (fst< lt₁) = fst< (less-trans {A = A} lt lt₁)
    less-trans    {{OrdLawsSigma}} (fst<         lt) (snd< lt₁) = fst< lt
    less-trans    {{OrdLawsSigma}} (snd<         lt) (fst< lt₁) = fst< lt₁
    less-trans    {{OrdLawsSigma}} (snd< {x = x} lt) (snd< lt₁) = snd< (less-trans {A = B x} lt lt₁)

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


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

open import Cubical.Data.DescendingList.Base public
open import Cubical.Data.DescendingList.Properties public
open import Cubical.Data.DescendingList.Examples public
open import Cubical.Data.DescendingList.Strict public

open import Cubical.Data.DescendingList.Strict.Properties public

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:
import      Lvl

-- TODO: Is it possible formalize this like this? Is it even correct?

-- Based on http://www.maths.ed.ac.uk/~tl/edinburgh_yrm/ (2017-11-22)
module Sets.ETCS where

  open import Logic.Propositional

  module Theory (S : Set(Lvl.𝟎)) (F : S → S → Set(Lvl.𝟎)) (_∘_ : ∀{a b c} → F(b)(c) → F(a)(b) → F(a)(c)) (_≡_ : ∀{a b} → F(a)(b) → F(a)(b) → Stmt{Lvl.𝟎}) where
    open import Functional hiding (_∘_)
    open import Logic.Predicate{Lvl.𝟎}{Lvl.𝟎}
    open import Logic.Propositional.Theorems{Lvl.𝟎}
    open import Relator.Equals{Lvl.𝟎} using () renaming (_≡_ to _≡ᵣ_)
    open import Type{Lvl.𝟎}

    Terminal : S → Stmt
    Terminal(x) = (∀{a : S} → (f g : F(a)(x)) → (f ≡ g))

    record Axioms : Set(Lvl.𝐒(Lvl.𝟎)) where
      field
        associativity : ∀{a b c d : S}{f : F(a)(b)}{g : F(b)(c)}{h : F(c)(d)} → ((h ∘ (g ∘ f)) ≡ ((h ∘ g) ∘ f))
        identity : ∀{a : S} → ∃{F(a)(a)}(id ↦ (∀{b : S}{f : F(a)(b)} → ((f ∘ id) ≡ f)) ∧ (∀{b : S}{f : F(b)(a)} → ((id ∘ f) ≡ f)))
        terminal : ∃(term ↦ Terminal(term))

      𝟏 : S
      𝟏 = [∃]-witness(terminal)

      _∈_ : ∀{a b : S} → F(a)(b) → S → Stmt
      _∈_ {a}{b} x X = (a ≡ᵣ 𝟏)∧(b ≡ᵣ X)

      _∉_ : ∀{a b : S} → F(a)(b) → S → Stmt
      _∉_ x X = ¬(x ∈ X)

      field
        empty : ∃{S}(∅ ↦ ∀{a b : S}{f : F(a)(b)} → (f ∉ ∅))

      -- TODO

  module Construction where
    open import Data
    open import Functional using (_∘_ ; id)
    open import Logic.Predicate{Lvl.𝐒(Lvl.𝟎)}{Lvl.𝟎}
    open import Logic.Propositional.Theorems{Lvl.𝐒(Lvl.𝟎)}
    open import Relator.Equals{Lvl.𝟎}

    Terminal : Set → Stmt
    Terminal(x) = (∀{a : Set}{f g : a → x} → (f ≡ g))

    _∈_ : ∀{a b : Set} → (a → b) → Set → Stmt
    _∈_ {a}{b} _ X = (a ≡ Unit)∧(b ≡ X)

    ∅ : Set
    ∅ = Empty

    -- TODO: Maybe use FunctionEquals instead?
    -- TODO: Is this construction working? Try to prove some of the theorems of standard set theory

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Lectures.Two where

-- Introduce imports
open import Lectures.One

-- Introduce type parameters

module List-types where

  data List (A : Set₁) : Set₁ where
    []  : List A
    _∷_ : A → List A → List A

  _ : List Set
  _ = ⊥ ∷ (ℕ ∷ (⊤ ∷ []))

module List {ℓ} where

  data List (A : Set ℓ) : Set ℓ where
    [] : List A
    _∷_ : A → List A → List A

  _++_ : {A : Set ℓ} → List A → List A → List A
  [] ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

  map : {A B : Set ℓ} → (A → B) → List A → List B
  map f [] = []
  map f (x ∷ xs) = f x ∷ map f xs

open List using (List; []; _∷_)

_ : List ℕ
_ = 0 ∷ (1 ∷ (2 ∷ []))

-- Introduce type families

module Vec where
  data Vec (A : Set) : ℕ → Set where
    []  : Vec A zero
    _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

  head : ∀ {A n} → Vec A (suc n) → A
  head (x ∷ xs) = x

  _++_ : ∀ {A n m} → Vec A n → Vec A m → Vec A (n + m)
  [] ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

  map : ∀ {A B n} → (A → B) → Vec A n → Vec B n
  map f [] = []
  map f (x ∷ xs) = f x ∷ map f xs

  zipWith : ∀ {A B C : Set} {n} (f : A → B → C)
          → Vec A n → Vec B n → Vec C n
  zipWith f [] [] = []
  zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys

--  \u+
data _⊎_ (A : Set) (B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

Dec : Set → Set
Dec B = B ⊎ (¬ B)

private
  data _×'_ (A : Set) (B : Set) : Set where
    _,'_ : A → B → A ×' B

  record _×''_ (A : Set) (B : Set) : Set where
    constructor _,''_
    field
      proj₁ : A
      proj₂ : B

-- \Sigma
record Σ {ℓ} (A : Set ℓ) (B : A → Set ℓ) : Set ℓ where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

_ : Σ ℕ _isEven
_ = 0 , tt

_×_ : Set → Set → Set
A × B = Σ A λ _ → B


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

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Level
open import Function
open import Category.Functor
open import Relation.Binary.PropositionalEquality

module Optics.Functorial where

  Lens' : (F : Set → Set) → RawFunctor F → Set → Set → Set
  Lens' F _ S A = (A → F A) → S → F S

  data Lens (S A : Set) : Set₁ where
    lens : ((F : Set → Set)(rf : RawFunctor F) → Lens' F rf S A)
         → Lens S A

  private
    cf : {A : Set} → RawFunctor {Level.zero} (const A)
    cf = record { _<$>_ = λ x x₁ → x₁ }

    if : RawFunctor {Level.zero} id
    if = record { _<$>_ = λ x x₁ → x x₁ }

  -- We can make lenses relatively painlessly without requiring reflection
  -- by providing getter and setter functions
  mkLens' : ∀ {A B : Set}
          → (B → A)
          → (B → A → B)
          → Lens B A
  mkLens' {A} {B} get set =
    lens (λ F rf f b → Category.Functor.RawFunctor._<$>_
                         {F = F} rf
                         {A = A}
                         {B = B}
                         (set b)
                         (f (get b)))

  -- Getter:

  -- this is typed as ^\.
  _^∙_ : ∀{S A} → S → Lens S A → A
  _^∙_ {_} {A} s (lens p) = p (const A) cf id s

   -- Setter:

  set : ∀{S A} → Lens S A → A → S → S
  set (lens p) a s = p id if (const a) s
  syntax set p a s = s [ p := a ]

  -- Modifier:

  over : ∀{S A} → Lens S A → (A → A) → S → S
  over (lens p) f s = p id if f s
  syntax over p f s = s [ p %~ f ]

  -- Composition

  infixr 30 _∙_
  _∙_ : ∀{S A B} → Lens S A → Lens A B → Lens S B
  (lens p) ∙ (lens q) = lens (λ F rf x x₁ → p F rf (q F rf x) x₁)

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
open import Agda.Primitive
open import Agda.Builtin.Nat

-- Named implicit function types

postulate
  T : Set → Set → Set
  foo : {A = X : Set} {B : Set} → T X B
  bar : ∀ {A = X} {B} → T X B

foo₁ : (X : Set) → T X X
foo₁ X = foo {A = X} {B = X}

bar₁ : ∀ X → T X X
bar₁ X = bar {A = X} {B = X}

Id : {A = _ : Set} → Set
Id {A = X} = X

Id₁ : Set → Set
Id₁ X = Id {A = X}

-- With blanks

postulate
  namedUnused   : {A = _ : Set} → Set
  unnamedUsed   : {_ = X : Set} → X → X
  unnamedUnused : {_ = _ : Set} → Set

_ : Set
_ = namedUnused {A = Nat}

_ : Nat → Nat
_ = unnamedUsed {Nat} -- can't give by name

_ : Set
_ = unnamedUnused {Nat}

-- In left-hand sides

id : {A = X : Set} → X → X
id {A = Y} x = x

-- In with-functions

with-fun : ∀ {A} {B = X} → T A X → T A X
with-fun {A = A} {B = Z} x with T A Z
with-fun {B = Z} x | Goal = x

-- In datatypes

data List {ℓ = a} (A : Set a) : Set a where
  [] : List A
  _∷_ : A → List A → List A

List₁ = List {ℓ = lsuc lzero}

-- In module telescopes

module Named {A : Set} {B = X : Set} where
   postulate H : X → A

h : (A : Set) → A → A
h A = Named.H {A = A} {B = A}

postulate
  X : Set

open Named {A = X} {B = X}

hh : X → X
hh = H

-- Constructors

data Q (n : Nat) : Set where
  mkQ : Q n

data E {n = x} (q : Q x) : Set where
  mkE : E q

e₁ : (q : Q 1) → E q
e₁ q = mkE {n = 1} {q = q}

-- Generalized variables

variable
  m n : Nat

q₁ = mkQ {n = 1}

data D (x : Q n) : Q m → Set where
  refl : {y = z : Q m} → D x z

D₁  = D {n = 1}
D₁₂ = λ x → D {n = 1} x {m = 2}

refl′ = λ x → refl {n = 1} {x = x} {m = 2} {y = mkQ}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Prelude.Bot where

data Bot : Set where

magic : ∀{A : Set} -> Bot -> A
magic ()


text:
open import Data.List

{- --- 6. Vectors --- -}

{- 6.1 Warmup -}

{- Problem: what do we return for the empty list ? -}
head2 : {A : Set} → List A → A
head2 [] = {!!}
head2 (x ∷ l) = x

{- 6.2 Definition -}
open import Data.Nat

data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _::_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

{- 6.3 Head and tail -}
head-vec : {A : Set} → {n : ℕ} → Vec A (suc n) → A
head-vec (x :: v) = x

tail-vec : {A : Set} → {n : ℕ} → Vec A (suc n) → Vec A n
tail-vec (x :: v) = v

{- 6.4 Concatenation -}
concat-vec : {A : Set} → {m n : ℕ} → Vec A m → Vec A n → Vec A (m + n)
concat-vec [] v2 = v2
concat-vec (x :: v1) v2 = x :: (concat-vec v1 v2)

{- 6.5 Reversal -}
snoc-vec : {A : Set} → {n : ℕ} → A → Vec A n → Vec A (suc n)
snoc-vec a [] = a :: []
snoc-vec a (x :: v) = x :: (snoc-vec a v)

rev-vec : {A : Set} → {n : ℕ} → Vec A n → Vec A n
rev-vec [] = []
rev-vec (x :: v) = snoc-vec x (rev-vec v)

{- 6.6 Accessing an element -}
data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc : {n : ℕ} (i : Fin n) → Fin (suc n)

{- 6.7 Zipping -}
open import Data.Product hiding (zip)

zip-vec : {A : Set} → {n : ℕ} → Vec A n → Vec A n → Vec (A × A) n
zip-vec [] [] = []
zip-vec (x₁ :: y₁) (x₂ :: y₂) = (x₁ , x₂) :: (zip-vec y₁ y₂)

max_stars_repo_name: erwinkn/program-eq-proof

max_issues_repo_name: erwinkn/program-eq-proof

max_forks_repo_name: erwinkn/program-eq-proof


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

open import Level

module Categories.Category.Instance.One where

open import Data.Unit using (⊤; tt)

open import Categories.Category
open import Categories.Functor
open import Categories.Category.Instance.Cats
import Categories.Object.Terminal as Term

module _ {o ℓ e : Level} where
  open Term (Cats o ℓ e)

  One : Category o ℓ e
  One = record
    { Obj       = Lift o ⊤
    ; _⇒_       = λ _ _ → Lift ℓ ⊤
    ; _≈_       = λ _ _ → Lift e ⊤
    }

  One-⊤ : Terminal
  One-⊤ = record { ⊤ = One ; ! = record { F₀ = λ _ → lift tt } }

-- not only is One terminal, it can be shifted anywhere else. Stronger veersion of !
shift : {o ℓ e : Level} (o′ ℓ′ e′ : Level) → Functor (One {o} {ℓ} {e}) (One {o′} {ℓ′} {e′})
shift o′ ℓ′ e′ = _ -- so obvious, Agda can fill it all in automatically!

One0 : Category 0ℓ 0ℓ 0ℓ
One0 = One {0ℓ} {0ℓ} {0ℓ}

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Presheaves where

open import Level

open import Categories.Category
open import Categories.Agda
open import Categories.FunctorCategory

Presheaves : ∀ {o ℓ e : Level} → Category o ℓ e → Category _ _ _
Presheaves {o} {ℓ} {e} C = Functors (Category.op C) (ISetoids ℓ e)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of homogeneous binary relations
------------------------------------------------------------------------

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

module Relation.Binary where

open import Agda.Builtin.Equality using (_≡_)
open import Data.Product
open import Data.Sum
open import Function
open import Level
import Relation.Binary.PropositionalEquality.Core as PropEq
open import Relation.Binary.Consequences

------------------------------------------------------------------------
-- Simple properties and equivalence relations

open import Relation.Binary.Core public

------------------------------------------------------------------------
-- Preorders

record IsPreorder {a ℓ₁ ℓ₂} {A : Set a}
                  (_≈_ : Rel A ℓ₁) -- The underlying equality.
                  (_∼_ : Rel A ℓ₂) -- The relation.
                  : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence _≈_
    -- Reflexivity is expressed in terms of an underlying equality:
    reflexive     : _≈_ ⇒ _∼_
    trans         : Transitive _∼_

  module Eq = IsEquivalence isEquivalence

  refl : Reflexive _∼_
  refl = reflexive Eq.refl

  ∼-respˡ-≈ : _∼_ Respectsˡ _≈_
  ∼-respˡ-≈ x≈y x∼z = trans (reflexive (Eq.sym x≈y)) x∼z

  ∼-respʳ-≈ : _∼_ Respectsʳ _≈_
  ∼-respʳ-≈ x≈y z∼x = trans z∼x (reflexive x≈y)

  ∼-resp-≈ : _∼_ Respects₂ _≈_
  ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈

record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _∼_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
    _∼_        : Rel Carrier ℓ₂  -- The relation.
    isPreorder : IsPreorder _≈_ _∼_

  open IsPreorder isPreorder public

------------------------------------------------------------------------
-- Setoids

-- Equivalence relations are defined in Relation.Binary.Core.

record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ
    isEquivalence : IsEquivalence _≈_

  open IsEquivalence isEquivalence public

  isPreorder : IsPreorder _≡_ _≈_
  isPreorder = record
    { isEquivalence = PropEq.isEquivalence
    ; reflexive     = reflexive
    ; trans         = trans
    }

  preorder : Preorder c c ℓ
  preorder = record { isPreorder = isPreorder }

------------------------------------------------------------------------
-- Decidable equivalence relations

record IsDecEquivalence {a ℓ} {A : Set a}
                        (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
  infix 4 _≟_
  field
    isEquivalence : IsEquivalence _≈_
    _≟_           : Decidable _≈_

  open IsEquivalence isEquivalence public

record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ
    isDecEquivalence : IsDecEquivalence _≈_

  open IsDecEquivalence isDecEquivalence public

  setoid : Setoid c ℓ
  setoid = record { isEquivalence = isEquivalence }

  open Setoid setoid public using (preorder)

------------------------------------------------------------------------
-- Partial orders

record IsPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
                      (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
                      Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isPreorder : IsPreorder _≈_ _≤_
    antisym    : Antisymmetric _≈_ _≤_

  open IsPreorder isPreorder public
    renaming
    ( ∼-respˡ-≈ to ≤-respˡ-≈
    ; ∼-respʳ-≈ to ≤-respʳ-≈
    ; ∼-resp-≈  to ≤-resp-≈
    )

record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≤_
  field
    Carrier        : Set c
    _≈_            : Rel Carrier ℓ₁
    _≤_            : Rel Carrier ℓ₂
    isPartialOrder : IsPartialOrder _≈_ _≤_

  open IsPartialOrder isPartialOrder public

  preorder : Preorder c ℓ₁ ℓ₂
  preorder = record { isPreorder = isPreorder }

------------------------------------------------------------------------
-- Decidable partial orders

record IsDecPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
                         (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
                         Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  infix 4 _≟_ _≤?_
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    _≟_            : Decidable _≈_
    _≤?_           : Decidable _≤_

  private
    module PO = IsPartialOrder isPartialOrder
  open PO public hiding (module Eq)

  module Eq where

    isDecEquivalence : IsDecEquivalence _≈_
    isDecEquivalence = record
      { isEquivalence = PO.isEquivalence
      ; _≟_           = _≟_
      }

    open IsDecEquivalence isDecEquivalence public

record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≤_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ₁
    _≤_               : Rel Carrier ℓ₂
    isDecPartialOrder : IsDecPartialOrder _≈_ _≤_

  private
    module DPO = IsDecPartialOrder isDecPartialOrder
  open DPO public hiding (module Eq)

  poset : Poset c ℓ₁ ℓ₂
  poset = record { isPartialOrder = isPartialOrder }

  open Poset poset public using (preorder)

  module Eq where

    decSetoid : DecSetoid c ℓ₁
    decSetoid = record { isDecEquivalence = DPO.Eq.isDecEquivalence }

    open DecSetoid decSetoid public

------------------------------------------------------------------------
-- Strict partial orders

record IsStrictPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
                            (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
                            Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence _≈_
    irrefl        : Irreflexive _≈_ _<_
    trans         : Transitive _<_
    <-resp-≈      : _<_ Respects₂ _≈_

  module Eq = IsEquivalence isEquivalence

  asym : Asymmetric _<_
  asym {x} {y} = trans∧irr⟶asym Eq.refl trans irrefl {x = x} {y}

  <-respʳ-≈ : _<_ Respectsʳ _≈_
  <-respʳ-≈ = proj₁ <-resp-≈

  <-respˡ-≈ : _<_ Respectsˡ _≈_
  <-respˡ-≈ = proj₂ <-resp-≈

  asymmetric = asym
  {-# WARNING_ON_USAGE asymmetric
  "Warning: asymmetric was deprecated in v0.16.
  Please use asym instead."
  #-}

record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _<_
  field
    Carrier              : Set c
    _≈_                  : Rel Carrier ℓ₁
    _<_                  : Rel Carrier ℓ₂
    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_

  open IsStrictPartialOrder isStrictPartialOrder public

------------------------------------------------------------------------
-- Decidable strict partial orders

record IsDecStrictPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
                               (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
                               Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  infix 4 _≟_ _<?_
  field
    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
    _≟_                  : Decidable _≈_
    _<?_                 : Decidable _<_

  private
    module SPO = IsStrictPartialOrder isStrictPartialOrder
    open SPO public hiding (module Eq)

  module Eq where

    isDecEquivalence : IsDecEquivalence _≈_
    isDecEquivalence = record
      { isEquivalence = SPO.isEquivalence
      ; _≟_           = _≟_
      }

    open IsDecEquivalence isDecEquivalence public

record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _<_
  field
    Carrier                 : Set c
    _≈_                     : Rel Carrier ℓ₁
    _<_                     : Rel Carrier ℓ₂
    isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_

  private
    module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder
    open DSPO public hiding (module Eq)

  strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
  strictPartialOrder = record { isStrictPartialOrder = isStrictPartialOrder }

  module Eq where

    decSetoid : DecSetoid c ℓ₁
    decSetoid = record { isDecEquivalence = DSPO.Eq.isDecEquivalence }

    open DecSetoid decSetoid public

------------------------------------------------------------------------
-- Total orders

record IsTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
                    (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
                    Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    total          : Total _≤_

  open IsPartialOrder isPartialOrder public

record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≤_
  field
    Carrier      : Set c
    _≈_          : Rel Carrier ℓ₁
    _≤_          : Rel Carrier ℓ₂
    isTotalOrder : IsTotalOrder _≈_ _≤_

  open IsTotalOrder isTotalOrder public

  poset : Poset c ℓ₁ ℓ₂
  poset = record { isPartialOrder = isPartialOrder }

  open Poset poset public using (preorder)

------------------------------------------------------------------------
-- Decidable total orders

record IsDecTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
                       (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
                       Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  infix 4 _≟_ _≤?_
  field
    isTotalOrder : IsTotalOrder _≈_ _≤_
    _≟_          : Decidable _≈_
    _≤?_         : Decidable _≤_

  open IsTotalOrder isTotalOrder public hiding (module Eq)

  module Eq where

    isDecEquivalence : IsDecEquivalence _≈_
    isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = _≟_
      }

    open IsDecEquivalence isDecEquivalence public

record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≤_
  field
    Carrier         : Set c
    _≈_             : Rel Carrier ℓ₁
    _≤_             : Rel Carrier ℓ₂
    isDecTotalOrder : IsDecTotalOrder _≈_ _≤_

  private
    module DTO = IsDecTotalOrder isDecTotalOrder
  open DTO public hiding (module Eq)

  totalOrder : TotalOrder c ℓ₁ ℓ₂
  totalOrder = record { isTotalOrder = isTotalOrder }

  open TotalOrder totalOrder public using (poset; preorder)

  module Eq where

    decSetoid : DecSetoid c ℓ₁
    decSetoid = record { isDecEquivalence = DTO.Eq.isDecEquivalence }

    open DecSetoid decSetoid public

------------------------------------------------------------------------
-- Strict total orders

-- Note that these orders are decidable. The current implementation
-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
-- definition capturing these three properties implies decidability
-- as `Trichotomous` necessarily separates out the equality case.

record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
                          (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
                          Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence _≈_
    trans         : Transitive _<_
    compare       : Trichotomous _≈_ _<_

  infix 4 _≟_ _<?_

  _≟_ : Decidable _≈_
  _≟_ = tri⟶dec≈ compare

  _<?_ : Decidable _<_
  _<?_ = tri⟶dec< compare

  isDecEquivalence : IsDecEquivalence _≈_
  isDecEquivalence = record
    { isEquivalence = isEquivalence
    ; _≟_           = _≟_
    }

  module Eq = IsDecEquivalence isDecEquivalence

  <-respˡ-≈ : _<_ Respectsˡ _≈_
  <-respˡ-≈ = trans∧tri⟶respˡ≈ Eq.trans trans compare

  <-respʳ-≈ : _<_ Respectsʳ _≈_
  <-respʳ-≈ = trans∧tri⟶respʳ≈ Eq.sym Eq.trans trans compare

  <-resp-≈ : _<_ Respects₂ _≈_
  <-resp-≈ = <-respʳ-≈ , <-respˡ-≈

  isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
  isStrictPartialOrder = record
    { isEquivalence = isEquivalence
    ; irrefl        = tri⟶irr compare
    ; trans         = trans
    ; <-resp-≈      = <-resp-≈
    }

  open IsStrictPartialOrder isStrictPartialOrder public
    using (irrefl; asym)

record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _<_
  field
    Carrier            : Set c
    _≈_                : Rel Carrier ℓ₁
    _<_                : Rel Carrier ℓ₂
    isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_

  open IsStrictTotalOrder isStrictTotalOrder public
    hiding (module Eq)

  strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
  strictPartialOrder =
    record { isStrictPartialOrder = isStrictPartialOrder }

  decSetoid : DecSetoid c ℓ₁
  decSetoid = record { isDecEquivalence = isDecEquivalence }

  module Eq = DecSetoid decSetoid


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.SimilaritySingleton
open import Oscar.Class.SimilarityM

module Oscar.Class.Similarity where

module Similarity
  {𝔞} {𝔄 : Ø 𝔞}
  {𝔟} {𝔅 : Ø 𝔟}
  {𝔣} {𝔉 : Ø 𝔣}
  {𝔞̇ 𝔟̇}
  (_∼₁_ : 𝔄 → 𝔄 → Ø 𝔞̇)
  (_∼₂_ : 𝔅 → 𝔅 → Ø 𝔟̇) (let _∼₂_ = _∼₂_; infix 4 _∼₂_)
  (_◃_ : 𝔉 → 𝔄 → 𝔅) (let _◃_ = _◃_; infix 16 _◃_)
  = ℭLASS (_◃_ , _∼₂_) (∀ {x y} f → x ∼₁ y → f ◃ x ∼₂ f ◃ y)

module _
  {𝔞} {𝔄 : Ø 𝔞}
  {𝔟} {𝔅 : Ø 𝔟}
  {𝔣} {𝔉 : Ø 𝔣}
  {𝔞̇ 𝔟̇}
  {_∼₁_ : 𝔄 → 𝔄 → Ø 𝔞̇}
  {_∼₂_ : 𝔅 → 𝔅 → Ø 𝔟̇}
  {_◃_ : 𝔉 → 𝔄 → 𝔅}
  where
  similarity = Similarity.method _∼₁_ _∼₂_ _◃_
  module _ ⦃ _ : Similarity.class _∼₁_ _∼₂_ _◃_ ⦄ where
    instance
      toSimilaritySingleton : ∀ {x y f} → SimilaritySingleton.class (x ∼₁ y) _∼₂_ _◃_ x y f
      toSimilaritySingleton .⋆ = similarity _
      toSimilarityM : ∀ {x y} → SimilarityM.class _∼₁_ _∼₂_ _◃_ x y
      toSimilarityM .⋆ = similarity

open import Oscar.Class.Smap
open import Oscar.Class.Surjection

module Similarity,cosmaparrow
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭₁} (𝔓₁ : 𝔛₂ → Ø 𝔭₁)
  {𝔭₂} (𝔓₂ : 𝔛₂ → Ø 𝔭₂)
  (smaparrow : Smaparrow.type ℜ 𝔓₁ 𝔓₂ surjection surjection)
  {𝔯̇} (ℜ̇ : ∀ {x y} → ℜ x y → ℜ x y → Ø 𝔯̇)
  {𝔭̇₂} (𝔓̇₂ : ∀ {x} → 𝔓₂ x → 𝔓₂ x → Ø 𝔭̇₂)
  where
  class = ∀ {m n} → Similarity.class (ℜ̇ {m} {n}) (𝔓̇₂ {surjection n}) (flip smaparrow)
  type = ∀ {m n} → Similarity.type (ℜ̇ {m} {n}) (𝔓̇₂ {surjection n}) (flip smaparrow)

module Similarity,cosmaparrow!
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭₁} (𝔓₁ : 𝔛₂ → Ø 𝔭₁)
  {𝔭₂} (𝔓₂ : 𝔛₂ → Ø 𝔭₂)
  ⦃ _ : Smaparrow!.class ℜ 𝔓₁ 𝔓₂ ⦄
  {𝔯̇} (ℜ̇ : ∀ {x y} → ℜ x y → ℜ x y → Ø 𝔯̇)
  {𝔭̇₂} (𝔓̇₂ : ∀ {x} → 𝔓₂ x → 𝔓₂ x → Ø 𝔭̇₂)
  = Similarity,cosmaparrow surjection ℜ 𝔓₁ 𝔓₂ smaparrow ℜ̇ 𝔓̇₂

module Similarity,cosmaphomarrow
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭} (𝔓 : 𝔛₂ → Ø 𝔭)
  (smaparrow : Smaphomarrow.type ℜ 𝔓 surjection)
  {𝔯̇} (ℜ̇ : ∀ {x y} → ℜ x y → ℜ x y → Ø 𝔯̇)
  {𝔭̇} (𝔓̇ : ∀ {x} → 𝔓 x → 𝔓 x → Ø 𝔭̇)
  = Similarity,cosmaparrow surjection ℜ 𝔓 𝔓 smaparrow ℜ̇ 𝔓̇

module Similarity,cosmaphomarrow!
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭} (𝔓 : 𝔛₂ → Ø 𝔭)
  ⦃ _ : Smaphomarrow!.class ℜ 𝔓 ⦄
  {𝔯̇} (ℜ̇ : ∀ {x y} → ℜ x y → ℜ x y → Ø 𝔯̇)
  {𝔭̇} (𝔓̇ : ∀ {x} → 𝔓 x → 𝔓 x → Ø 𝔭̇)
  = Similarity,cosmaphomarrow surjection ℜ 𝔓 smaparrow ℜ̇ 𝔓̇

module Similarity,smaparrow
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  {𝔯} (ℜ : π̂² 𝔯 𝔛₁)
  {𝔭₁} (𝔓₁ : π̂ 𝔭₁ 𝔛₂)
  {𝔭₂} (𝔓₂ : π̂ 𝔭₂ 𝔛₂)
  (smaparrow : Smaparrow.type ℜ 𝔓₁ 𝔓₂ surjection surjection)
  {𝔭̇₁} (𝔓̇₁ : ∀̇ π̂² 𝔭̇₁ (𝔓₁ ∘ surjection))
  {𝔭̇₂} (𝔓̇₂ : ∀̇ π̂² 𝔭̇₂ (𝔓₂ ∘ surjection))
  where
  class = ∀ {m n} → Similarity.class (𝔓̇₁ {m}) (𝔓̇₂ {n}) smaparrow
  type = ∀ {m n} → Similarity.type (𝔓̇₁ {m}) (𝔓̇₂ {n}) smaparrow

module Similarity,smaparrow!
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  {𝔯} (ℜ : π̂² 𝔯 𝔛₁)
  {𝔭₁} (𝔓₁ : π̂ 𝔭₁ 𝔛₂)
  {𝔭₂} (𝔓₂ : π̂ 𝔭₂ 𝔛₂)
  ⦃ _ : Smaparrow!.class ℜ 𝔓₁ 𝔓₂ ⦄
  {𝔭̇₁} (𝔓̇₁ : ∀̇ π̂² 𝔭̇₁ (𝔓₁ ∘ surjection))
  {𝔭̇₂} (𝔓̇₂ : ∀̇ π̂² 𝔭̇₂ (𝔓₂ ∘ surjection))
  = Similarity,smaparrow surjection ℜ 𝔓₁ 𝔓₂ smaparrow 𝔓̇₁ 𝔓̇₂

module Similarity,smaphomarrow
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  {𝔯} (ℜ : π̂² 𝔯 𝔛₁)
  {𝔭} (𝔓 : π̂ 𝔭 𝔛₂)
  (smaparrow : Smaphomarrow.type ℜ 𝔓 surjection)
  {𝔭̇} (𝔓̇ : ∀̇ π̂² 𝔭̇ (𝔓 ∘ surjection))
  = Similarity,smaparrow surjection ℜ 𝔓 𝔓 smaparrow 𝔓̇ 𝔓̇

module Similarity,smaphomarrow!
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  {𝔯} (ℜ : π̂² 𝔯 𝔛₁)
  {𝔭} (𝔓 : π̂ 𝔭 𝔛₂)
  ⦃ _ : Smaphomarrow!.class ℜ 𝔓 ⦄
  {𝔭̇} (𝔓̇ : ∀̇ π̂² 𝔭̇ (𝔓 ∘ surjection))
  = Similarity,smaphomarrow surjection ℜ 𝔓 smaparrow 𝔓̇


text:
module Silica where
  open import Agda.Builtin.Bool public
  open import Data.Bool using (true; false) public
  open import Prelude public
  open import Data.Nat public
  open import Data.List public
  open import Data.Nat.Properties public
  open import Relation.Nullary using (¬_; Dec; yes; no) public
  open import Relation.Binary using (module StrictTotalOrder; DecSetoid; IsDecEquivalence) public
  open import Data.Maybe using (just) public
  import Relation.Binary.PropositionalEquality as Eq
  import Relation.Binary.Core
  import Relation.Binary.HeterogeneousEquality
  open Eq using (_≡_; _≢_; refl; cong; sym) public
  open Eq.≡-Reasoning public
  open import Data.Product using (_×_; proj₁; proj₂; ∃-syntax; ∃) renaming (_,_ to ⟨_,_⟩) public
  import Context
  open import Data.List.Membership.DecSetoid ≡-decSetoid
  import Data.List.Membership.DecSetoid
  import Data.List.Relation.Binary.Subset.Setoid using (_⊆_)
  import Data.List.Relation.Binary.Equality.DecPropositional using (_≡?_)
  open import Data.List.Relation.Unary.Any
  open import Data.List.All
  open import Data.Empty
  open import Data.Sum
  open import Level

  import Data.Fin

  -------------- Syntax ------------
  Id : Set
  Id = ℕ

  -- State sets
  σ : Set
  σ = List ℕ

  -- List of ℕ subset
  _⊆_ : σ → σ → Set
  _⊆_ = Data.List.Relation.Binary.Subset.Setoid._⊆_ (DecSetoid.setoid ≡-decSetoid)

  -- List of ℕ decidable equality
  _≟l_ : Relation.Binary.Core.Decidable {A = σ} _≡_
  _≟l_ = Data.List.Relation.Binary.Equality.DecPropositional._≡?_ _≟_

  data Perm : Set where
    Owned : Perm
    Unowned : Perm
    Shared : Perm
    S : σ → Perm

  record Tc : Set where
    constructor tc
    field
      contractName : Id
      perm : Perm

  data Tbase : Set where
    Void : Tbase
    Boolean : Tbase

  data Type : Set where
    base : Tbase -> Type
    contractType : Tc -> Type

  SInjective : (l₁ l₂ : σ)
               → l₁ ≢ l₂
               → S l₁ ≢ S l₂
  SInjective l₁ .l₁ lsEq refl = lsEq refl

  TCInjectiveContractName : ∀ {p₁ p₂}
                            → (cn₁ cn₂ : Id)
                            → cn₁ ≢ cn₂
                            → tc cn₁ p₁ ≢ tc cn₂ p₂
  TCInjectiveContractName cn₁ cn₂ nEq refl = nEq refl

  TCInjectivePermission : ∀ {cn₁ cn₂}
                            → (p₁ p₂ : Perm)
                            → p₁ ≢ p₂
                            → tc cn₁ p₁ ≢ tc cn₂ p₂
  TCInjectivePermission cn₁ cn₂ nEq refl = nEq refl

  contractTypeInjective : ∀ {tc₁ tc₂}
    → tc₁ ≢ tc₂
    → contractType tc₁ ≢ contractType tc₂

  contractTypeInjective nEq refl = nEq refl

  -- Decidable equality for permissions
  infix 4 _≟p_
  _≟p_ : Relation.Binary.Core.Decidable {A = Perm} _≡_
  Owned ≟p Owned = yes refl
  Owned ≟p Unowned =  no (λ ())
  Owned ≟p Shared =  no (λ ())
  Owned ≟p S x =  no (λ ())
  Unowned ≟p Owned =  no (λ ())
  Unowned ≟p Unowned = yes refl
  Unowned ≟p Shared =  no (λ ())
  Unowned ≟p S x =  no (λ ())
  Shared ≟p Owned =  no (λ ())
  Shared ≟p Unowned =  no (λ ())
  Shared ≟p Shared = yes refl
  Shared ≟p S x =  no (λ ())
  S x ≟p Owned =  no (λ ())
  S x ≟p Unowned =  no (λ ())
  S x ≟p Shared =  no (λ ())
  S s1 ≟p S s2 with s1 ≟l s2
  ... | yes eq = yes (Eq.cong S eq)
  ... | no nEq = no λ sEq → SInjective s1 s2 nEq sEq

  -- Decidable equality for types
  infix 4 _≟t_
  _≟t_ : Relation.Binary.Core.Decidable {A = Type} _≡_
  base Void ≟t base Void = yes refl
  base Void ≟t base Boolean = no (λ ())
  base Boolean ≟t base Void = no (λ ())
  base Boolean ≟t base Boolean = yes refl
  base x ≟t contractType x₁ = no (λ ())
  contractType x ≟t base x₁ = no (λ ())
  contractType (tc contractName p₁) ≟t contractType (tc contractName₁ p₂) with contractName ≟ contractName₁ | p₁ ≟p p₂
  ... | yes eqNames | yes eqPerms = yes (Eq.cong₂ (λ a → λ b → contractType (tc a b)) eqNames eqPerms)
  ... | no nEqNames | _ = no (contractTypeInjective (TCInjectiveContractName contractName contractName₁ nEqNames))
  ... | _ | no nEqPerms =  no (contractTypeInjective (TCInjectivePermission p₁ p₂ nEqPerms))

  ≟tIsEquivalence : Relation.Binary.IsEquivalence {A = Type} _≡_ -- _≟t_
  ≟tIsEquivalence = Eq.isEquivalence

  ≡t-isDecEquivalence : IsDecEquivalence (_≡_ {A = Type})
  ≡t-isDecEquivalence = record
    { isEquivalence = ≟tIsEquivalence
    ; _≟_           = _≟t_
    }

  ≡t-decSetoid : DecSetoid 0ℓ 0ℓ
  ≡t-decSetoid = record
    { Carrier          = Type
    ; _≈_              = _≡_
    ; isDecEquivalence = ≡t-isDecEquivalence
    }

  module tDecSetoid = Data.List.Membership.DecSetoid ≡t-decSetoid
  _∈ₜ_ : Type → List Type → Set
  _∈ₜ_ = tDecSetoid._∈_

  isShared : Type → Bool
  isShared (contractType (record {contractName = _ ; perm = Shared})) = true
  isShared _ = false

  eqContractTypes : ∀ {t₁ : Tc}
                    → ∀ {t₂ : Tc}
                    → Tc.perm t₁ ≡ Tc.perm t₂
                    → Tc.contractName t₁ ≡ Tc.contractName t₂
                    → t₁ ≡ t₂
  eqContractTypes {t₁} {t₂} refl refl = refl

  record State : Set where
    field
      field₁ : Tc
      field₂ : Tc
      isAsset : Bool

  data Targ : Set where
    arg-trans : Tc -> Perm -> Targ
    base : Tbase -> Targ

  IndirectRef : Set
  IndirectRef = Id

  ObjectRef : Set
  ObjectRef = Id

  data SimpleExpr : Set where
    var : Id -> SimpleExpr
    loc : IndirectRef -> SimpleExpr

  record Object : Set where
    field
      contractName : Id
      stateName : Id
      x₁ : SimpleExpr
      x₂ : SimpleExpr

  data Value : Set where
    boolVal : (b : Bool)
              ------------
              → Value

    voidVal : Value

    objVal : ∀ (o : ObjectRef)
             --------------
             → Value

  data Expr : Set where
    valExpr : Value → Expr
    simpleExpr : SimpleExpr → Expr
    fieldAccess : Id → Expr  -- All field accesses are to 'this', so the field name suffices.
    assertₓ : Id → σ → Expr
    assertₗ : IndirectRef → σ → Expr
    new : Id → Id → SimpleExpr → SimpleExpr → Expr  -- Contract, state, field values (always two of them).
    -- TODO: add the rest of the expressions

  objValInjective : ∀ {o o'}
                      → o ≢ o'
                      → objVal o ≢ objVal o'
  objValInjective {o} {.o} oNeqo' refl = oNeqo' refl

  objValInjectiveContrapositive : ∀ {o o'}
                                  → objVal o ≡ objVal o'
                                  → o ≡ o'
  objValInjectiveContrapositive {o} {o'} refl = refl

  record PublicTransaction : Set where
    constructor publicTransaction
    field
      retType : Type
      name : Id
      argType : Targ
      argName : Id
      initialState : Perm
      finalState : Perm
      expr : Expr

  -- TODO: add private transactions

  record Contract : Set where
    constructor contract
    field
      isAsset : Bool
      name : Id
      states : List State
      transactions : List PublicTransaction

  data Program : Set where
    program : List Contract -> Expr -> Program

  --============= Utilities ================
  data FreeLocations : Expr → List IndirectRef → Set where
    boolFL : ∀ {b : Bool} → FreeLocations (valExpr (boolVal b)) []
    varFL : ∀ {x : Id} → FreeLocations (simpleExpr (var x)) []
    voidFL : FreeLocations (valExpr voidVal) []
    objValFL : ∀ {o : ObjectRef} → FreeLocations (valExpr (objVal o)) []
    locFL : ∀ (l : IndirectRef) → FreeLocations (simpleExpr (loc l)) [ l ]

  freeLocationsOfSimpleExpr : SimpleExpr → List IndirectRef
  freeLocationsOfSimpleExpr (var x) = []
  freeLocationsOfSimpleExpr (loc l) = [ l ]

  freeLocations : Expr → List IndirectRef
  freeLocations (valExpr (boolVal b)) = []
  freeLocations (simpleExpr (se)) = freeLocationsOfSimpleExpr se
  freeLocations (valExpr voidVal) = []
  freeLocations (valExpr (objVal o)) = []
  freeLocations (fieldAccess x) = []
  freeLocations (assertₓ x x₁) = []
  freeLocations (assertₗ l x₁) = [ l ]
  freeLocations (new _ _ f₁ f₂) = (freeLocationsOfSimpleExpr f₁) ++ (freeLocationsOfSimpleExpr f₂)

  data FreeVariables : Expr → List Id → Set where
    boolFL : ∀ {b : Bool} → FreeVariables (valExpr (boolVal b)) []
    varFL : ∀ {x : Id} → FreeVariables (simpleExpr (var x)) [ x ]
    voidFL : FreeVariables (valExpr voidVal) []
    objValFL : ∀ {o : ObjectRef} → FreeVariables (valExpr (objVal o)) []
    locFL : ∀ (l : IndirectRef) → FreeVariables (simpleExpr (loc l)) []

  data Closed : Expr → Set where
    closed : ∀ (e : Expr)
             → FreeVariables e []
             --------------------
             → Closed e

  freeVariablesOfSimpleExpr : SimpleExpr → List IndirectRef
  freeVariablesOfSimpleExpr (var x) = [ x ]
  freeVariablesOfSimpleExpr (loc l) = []

  freeVariables : Expr → List IndirectRef
  freeVariables (valExpr (boolVal b)) = []
  freeVariables (simpleExpr se) = freeVariablesOfSimpleExpr se
  freeVariables (valExpr voidVal) = []
  freeVariables (valExpr (objVal o)) = []
  freeVariables (fieldAccess x) = []
  freeVariables (assertₓ x x₁) = [ x ]
  freeVariables (assertₗ l x₁) =  []
  freeVariables (new _ _ f₁ f₂) = (freeVariablesOfSimpleExpr f₁) ++ (freeVariablesOfSimpleExpr f₂)

  --=============== Static Semantics ================
  -- A ContractEnv (written Γ) maps from Ids to contract definitions.
  module ContractEnv = Context Contract

  module TypeEnvContext = Context Type
  TypeEnv = TypeEnvContext.ctx
  open TypeEnvContext

  record StaticEnv : Set where
    constructor se
    field
      varEnv : TypeEnv
      locEnv : TypeEnv
      objEnv : TypeEnv

  _,ₓ_⦂_ : StaticEnv → Id → Type → StaticEnv
  Δ ,ₓ x ⦂ T = record Δ {varEnv = (StaticEnv.varEnv Δ) , x ⦂ T}

  _,ₗ_⦂_ : StaticEnv → Id → Type → StaticEnv
  Δ ,ₗ l ⦂ T = record Δ {locEnv = (StaticEnv.locEnv Δ) , l ⦂ T}

  _,ₒ_⦂_ : StaticEnv → Id → Type → StaticEnv
  Δ ,ₒ o ⦂ T = record Δ {objEnv = (StaticEnv.objEnv Δ) , o ⦂ T}

  -- Subtyping --
  data _<:_ : Type → Type → Set where
    <:-refl : ∀ {T : Type}
           ----------------
           → T <: T
    -- TODO: add more subtyping judgments

  -- Helper judgments --

  --data _⊢_NotAsset : ContractEnv.ctx → Id → Set where
  data NotAsset : ContractEnv.ctx → Id → Set where
    inContext :
      {Γ : ContractEnv.ctx}
      → {id : Id}
      → (contr : Contract)
      → (p : Contract.isAsset contr ≡ false)
      → (q : (Γ ContractEnv.∋ id ⦂ contr))
      -------------
      → NotAsset Γ id

  -- Context strength --
  data _<ₗ_ : TypeEnv → TypeEnv → Set where
    empty< : ∀ { Δ Δ' : TypeEnv}
          → (Δ' ≡ ∅)
          --------------
           → Δ <ₗ Δ'

    nonempty< : ∀ {Δ Δ' Δ'' Δ''' : TypeEnv}
      → ∀ {l : ℕ}
      → ∀ {T T' : Type}
      → Δ' ≡ (Δ'' , l ⦂ T')
      → Δ ≡ (Δ''' , l ⦂ T)
      → T <: T'
      → Δ''' <ₗ Δ''
      -------------
      → Δ <ₗ Δ'

  data _<*_ : StaticEnv → StaticEnv → Set where
    * : ∀ {Δ Δ'}
          → (StaticEnv.locEnv Δ) <ₗ (StaticEnv.locEnv Δ')
          -----------------------------------------------
          → Δ <* Δ'

  <ₗ-refl : ∀ {Δ : TypeEnv}
            → Δ <ₗ Δ
  <ₗ-refl {Context.∅} = empty< refl
  <ₗ-refl {Δ , x ⦂ x₁} = nonempty< refl refl (<:-refl) (<ₗ-refl {Δ})

  <*-refl : ∀ {Δ : StaticEnv}
            → Δ <* Δ

  <*-refl = * <ₗ-refl

  <*-o-extension : ∀ {Δ o T}
                   → (Δ ,ₒ o ⦂ T) <* Δ
  <*-o-extension {Δ} {o} {T} = * <ₗ-refl

  -- Splitting --
  record SplitType : Set where
    constructor _⇛_/_
    field
      t₁ : Type
      t₂ : Type
      t₃ : Type

  infix 4 _⊢_
  data _⊢_ : ContractEnv.ctx -> SplitType -> Set where
    voidSplit : ∀ {Γ : ContractEnv.ctx}
                ---------------
                → Γ ⊢ (base Void) ⇛ (base Void) / (base Void)

    booleanSplit : ∀ {Γ : ContractEnv.ctx}
                   --------------
                   → Γ ⊢ base Boolean ⇛ base Boolean / base Boolean

    -- split Unowned off of anything.
    unownedSplit : ∀ {Γ : ContractEnv.ctx}
                   → ∀ {t1 t2 t3 : Tc}
                   → (Tc.contractName t1) ≡ (Tc.contractName t2)
                   → Tc.contractName t1 ≡ Tc.contractName t3
                   → (Tc.perm t1) ≡ (Tc.perm t2)
                   → Tc.perm t3 ≡ Unowned
                   --------------
                   → Γ ⊢ contractType t1 ⇛ contractType t2 / contractType t3

    shared-shared-shared : ∀ {Γ : ContractEnv.ctx}
                           → ∀ {t : Tc}
                           → Tc.perm t ≡ Shared
                           --------------------------------------------------------
                           → Γ ⊢ contractType t  ⇛ contractType t / contractType t

    owned-shared :
     ∀ {c : Id}
     → ∀ {Γ : ContractEnv.ctx}
     → NotAsset Γ c
     --------------
      → Γ ⊢ contractType (tc c Owned)  ⇛ contractType (tc c Shared) / contractType (tc c Shared)

    states-shared :
      ∀ {s : σ}
      → ∀ {c : Id}
      → ∀ {Γ : ContractEnv.ctx}
      → NotAsset Γ c
      --------------
      → Γ ⊢ contractType ( record {perm = S s ; contractName = c} )  ⇛ contractType ( record {perm = Shared ; contractName = c} ) / contractType ( record {perm = Shared ; contractName = c} )

  splitType : ∀ {Γ : ContractEnv.ctx}
            → ∀ {t1 t2 t3 : Type}
            → Γ ⊢ t1 ⇛ t2 / t3
            → SplitType

  splitType voidSplit = (base Void) ⇛ (base Void) / (base Void)
  splitType booleanSplit =  base Boolean ⇛ base Boolean / base Boolean
  splitType (unownedSplit {Γ} {t1} {t2} {t3} eqNames1 eqNames2 eqPerms eqUnownedPerm) = contractType t1 ⇛ contractType t2 / contractType t3
  splitType (shared-shared-shared {Γ} {t} _) =  contractType t  ⇛ contractType t / contractType t
  splitType (owned-shared {c} x) = contractType ( record {perm = Owned ; contractName = c} )  ⇛ contractType ( record {perm = Shared ; contractName = c} ) / contractType ( record {perm = Shared ; contractName = c} )
  splitType (states-shared {s} {c} x) = contractType ( record {perm = S s ; contractName = c} )  ⇛ contractType ( record {perm = Shared ; contractName = c} ) / contractType ( record {perm = Shared ; contractName = c} )

  splitTypeCorrect :  ∀ {Γ}
                      → ∀ {t1 t2 t3 : Type}
                      → ∀ (p : Γ ⊢ t1 ⇛ t2 / t3)
                      → splitType p ≡ t1 ⇛ t2 / t3
  splitTypeCorrect voidSplit = refl
  splitTypeCorrect booleanSplit = refl
  splitTypeCorrect (unownedSplit x _ _ _) = refl
  splitTypeCorrect (shared-shared-shared _) = refl
  splitTypeCorrect (owned-shared x) = refl
  splitTypeCorrect (states-shared x) = refl

  ------------ Type judgments ----------------
  data _⊢_⦂_⊣_ : StaticEnv → Expr → Type → StaticEnv → Set where
    varTy : ∀ {Γ : ContractEnv.ctx}
        → ∀ {Δ : StaticEnv}
        → ∀ {T₁ T₂ T₃ : Type}
        → ∀ (x : Id)
        → Γ ⊢ T₁ ⇛ T₂ / T₃
        -----------------------------------
        → (Δ ,ₓ x ⦂ T₁) ⊢ (simpleExpr (var x)) ⦂ T₂ ⊣ (Δ ,ₓ x ⦂ T₃)

    locTy :  ∀ {Γ : ContractEnv.ctx}
        → ∀ {Δ : StaticEnv}
        → ∀ {T₁ T₂ T₃ : Type}
        → ∀ (l : IndirectRef)
        → Γ ⊢ T₁ ⇛ T₂ / T₃
        ------------------------------------
        → (Δ ,ₗ l ⦂ T₁) ⊢ (simpleExpr (loc l)) ⦂ T₂ ⊣ (Δ ,ₗ l ⦂ T₃)

    objTy :  ∀ {Γ : ContractEnv.ctx}
        → ∀ {Δ : StaticEnv}
        → ∀ {T₁ T₂ T₃ : Type}
        → ∀ (o : ObjectRef)
        → Γ ⊢ T₁ ⇛ T₂ / T₃
        ------------------------------------
        → (Δ ,ₒ o ⦂ T₁) ⊢ (valExpr (objVal o)) ⦂ T₂ ⊣ (Δ ,ₒ o ⦂ T₃)

    boolTy : ∀ {Γ : ContractEnv.ctx}
           → ∀ {Δ : StaticEnv}
           → ∀ (b : Bool)
           ------------------------------------
           → Δ ⊢ (valExpr (boolVal b)) ⦂ (base Boolean) ⊣ Δ

    voidTy : ∀ {Γ : ContractEnv.ctx}
           → ∀ {Δ : StaticEnv}
           --------------------
            → Δ ⊢ (valExpr voidVal) ⦂ base Void ⊣ Δ

    assertTyₓ : ∀ {Γ : ContractEnv.ctx}
             → ∀ {Δ : StaticEnv}
             → ∀ {s₁ s₂ : σ}
             → ∀ {tc : Tc}
             → ∀ {x : Id}
             → Tc.perm tc ≡ S s₁
             → s₁ ⊆ s₂
             --------------------------
             → (Δ ,ₓ x ⦂ (contractType tc)) ⊢ assertₓ x s₁ ⦂ base Void ⊣ (Δ ,ₓ x ⦂ (contractType tc))

    assertTyₗ : ∀ {Γ : ContractEnv.ctx}
             → ∀ {Δ : StaticEnv}
             → ∀ {s₁ s₂ : σ}
             → ∀ {tc : Tc}
             → ∀ {l : IndirectRef}
             → Tc.perm tc ≡ S s₁
             → s₁ ⊆ s₂
             --------------------------
             → (Δ ,ₗ l ⦂ (contractType tc)) ⊢ assertₗ l s₁ ⦂ base Void ⊣ (Δ ,ₗ l ⦂ (contractType tc))

    newTy : ∀ {Γ Δ Δ' Δ''}
            → {states : List State}
            → {C st : Id}
            → {x₁ x₂ : SimpleExpr}
            → {T₁ T₂ Tf₁ Tf₂ : Tc}
            → ∀ {isCAsset isSAsset transactions}
            → (stOK : st < (length states))
            → Δ ⊢ simpleExpr x₁ ⦂ (contractType T₁) ⊣ Δ'
            → Δ' ⊢ simpleExpr x₂ ⦂ (contractType T₂) ⊣ Δ''
            → Γ ContractEnv.∋ C ⦂ (contract isCAsset C states transactions)
            → (Data.List.lookup states (Data.Fin.fromℕ≤ stOK)) ≡ record {field₁ = Tf₁ ; field₂ = Tf₂ ; isAsset = isSAsset}
            --------------------------
            → Δ ⊢ new C st x₁ x₂ ⦂ (contractType (tc C (S [ st ]))) ⊣ Δ''

  ------------ DYNAMIC SEMANTICS --------------

  -- μ
  module ObjectRefContext = Context Object
  ObjectRefEnv = ObjectRefContext.ctx

  -- ρ
  module IndirectRefContext = Context Value -- TODO: require that these are all values
  IndirectRefEnv = IndirectRefContext.ctx

  -- φ
  module StateLockingContext = Context Bool
  StateLockingEnv = StateLockingContext.ctx

  -- ψ
  module ReentrancyContext = Context Bool
  ReentrancyEnv = ReentrancyContext.ctx

  record RuntimeEnv : Set where
    constructor re
    field
      μ : ObjectRefEnv
      ρ : IndirectRefEnv
      φ : StateLockingEnv
      ψ : ReentrancyEnv

  ----------- Reduction Rules ------------
  data _,_⟶_,_ : RuntimeEnv → Expr → RuntimeEnv → Expr → Set where
    SElookup : -- of locations (i.e. let-bound variables)
      ∀ {Σ : RuntimeEnv}
      → ∀ {Δ Δ' : StaticEnv}
      → ∀ {T : Type}
      → ∀ {l : IndirectRef}
      → ∀ {v : Value}
      → Δ ⊢ (simpleExpr (loc l)) ⦂ T ⊣ Δ'
      → RuntimeEnv.ρ Σ IndirectRefContext.∋ l ⦂ v
      -----------------------------------------------------------
      → (Σ , (simpleExpr (loc l)) ⟶ Σ , valExpr v)

    SEassertₓ :
      ∀ {Σ : RuntimeEnv}
      → ∀ (x : Id)
      → ∀ (s : σ)
      --------------
      → (Σ , assertₓ x s ⟶ Σ , valExpr voidVal)

    SEassertₗ :
      ∀ {Σ : RuntimeEnv}
      → ∀ (l : IndirectRef)
      → ∀ (s : σ)
      --------------
      → (Σ , assertₗ l s ⟶ Σ , valExpr voidVal)

    SEnew :
      ∀ {Σ μ' Σ' C st x₁ x₂ o}
      → o ObjectRefContext.∉dom (RuntimeEnv.μ Σ)
      → μ' ≡ (RuntimeEnv.μ Σ) ObjectRefContext., o ⦂ record { contractName = C ; stateName = st ; x₁ = x₁ ; x₂ = x₂ }
      → Σ' ≡ record Σ {μ = μ'}
      -------------
      → (Σ , new C st x₁ x₂ ⟶ Σ' , valExpr (objVal o))

max_stars_repo_name: ivoysey/Obsidian

max_issues_repo_name: ivoysey/Obsidian

max_forks_repo_name: ivoysey/Obsidian


text:
-- labeled λ-calculus

module IntrinsicallyTypedLLC where

open import Data.List
open import Data.List.Relation.Unary.All
open import Data.List.Base
open import Data.Vec hiding (_++_)
open import Data.Unit hiding (_≤_)
open import Data.Nat hiding (_≤_)
open import Data.Fin.Subset
open import Data.Fin.Subset.Properties
open import Data.Fin hiding (_≤_)
open import Data.Product
open import Data.Empty
open import Relation.Binary

-- definitions

data Ty (nl : ℕ) : Set where   -- nl ~ (max.) number of labels
  Tunit : Ty nl
  Tlabel : Subset nl → Ty nl
  Tfun : Ty nl → Ty nl → Ty nl

TEnv : ℕ → Set
TEnv nl = List (Ty nl)

data _≤_ {nl} : Ty nl → Ty nl → Set where
  Sunit  : Tunit ≤ Tunit
  Slabel : ∀ {snl snl'} → snl ⊆ snl' → (Tlabel snl) ≤ (Tlabel snl')
  Sfun   : ∀ {A A' B B'} → A' ≤ A → B ≤ B' → (Tfun A B) ≤ (Tfun A' B')

data _∈`_ {nl : ℕ} : Ty nl → TEnv nl → Set where
  here  : ∀ {lt φ} → lt ∈` (lt ∷ φ)
  there : ∀ {lt lt' φ} → lt ∈` φ → lt ∈` (lt' ∷ φ)

data Exp {nl : ℕ} : TEnv nl → Ty nl → Set where
  Unit     : ∀ {φ} → Exp φ Tunit
  Var      : ∀ {φ t} → (x : t ∈` φ) → Exp φ t   -- t ∈` φ gives us the position of "x" in env
  SubType  : ∀ {A A' φ} →  Exp φ A → A ≤ A'
                        →  Exp φ A'
  Lab-I    : ∀ {l snl φ} → l ∈ snl → Exp φ (Tlabel snl)
  Lab-E    : ∀ {snl φ B} → Exp φ (Tlabel snl)
                         → (∀ l → l ∈ snl → Exp φ B)
                         → Exp φ B
  Abs     : ∀ {B A φ} → Exp (A ∷ φ) B
                      → Exp φ (Tfun A B)
  App     : ∀ {A B φ} → Exp φ (Tfun A B)
                      → (ex : Exp φ A)
                      → Exp φ B

-- subtyping properties

≤-trans : ∀ {nl} {t t' t'' : Ty nl} → t ≤ t' → t' ≤ t'' → t ≤ t''
≤-trans Sunit Sunit = Sunit
≤-trans (Slabel snl⊆snl') (Slabel snl'⊆snl'') = Slabel (⊆-trans snl⊆snl' snl'⊆snl'')
≤-trans (Sfun a'≤a b≤b') (Sfun a''≤a' b'≤b'') = Sfun (≤-trans a''≤a' a'≤a) (≤-trans b≤b' b'≤b'')

≤-refl : ∀ {nl} → (t : Ty nl) → t ≤ t
≤-refl Tunit = Sunit
≤-refl (Tlabel x) = Slabel (⊆-refl)
≤-refl (Tfun t t') = Sfun (≤-refl t) (≤-refl t')

-- big-step semantics

Val : ∀ {nl} → Ty nl → Set
Val Tunit = Data.Unit.⊤
Val {nl} (Tlabel snl) = Σ (Fin nl) (λ l → l ∈ snl)
Val (Tfun ty ty₁) = (Val ty) → (Val ty₁)

coerce : ∀ {nl} {t t' : Ty nl} → t ≤ t' → Val t → Val t' -- supertype of a Value is also a Value
coerce Sunit t = tt
coerce (Slabel snl⊆snl') (Finnl , Finnl∈snl) = (Finnl , (snl⊆snl' Finnl∈snl))
coerce (Sfun A'≤A B≤B') f = λ x → coerce B≤B' (f (coerce A'≤A x))

access : ∀ {nl} {t : Ty nl} {φ} → t ∈` φ → All Val φ → Val t
access here (px ∷ ρ) = px
access (there x) (px ∷ ρ) = access x ρ

eval : ∀ {nl φ t} → Exp {nl} φ t → All Val φ → Val t
eval Unit ϱ = tt
eval (Var x) ϱ = access x ϱ
eval (SubType e a≤a') ϱ = coerce a≤a' (eval e ϱ)
eval (Lab-I {l} l∈snl) ϱ = l , (l∈snl)
eval (Lab-E e case) ϱ with eval e ϱ
... | lab , lab∈nl = eval (case lab lab∈nl) ϱ
eval (Abs e) ϱ = λ x → eval e (x ∷ ϱ)
eval (App e e₁) ϱ = (eval e ϱ) (eval e₁ ϱ)

-- small-step semantics
-- substitution taken from PLFA

ext : ∀ {nl φ ψ} → (∀ {A : Ty nl} → A ∈` φ → A ∈` ψ)
                 → (∀ {A B} → A ∈` (B ∷ φ) → A ∈` (B ∷ ψ))
ext ϱ here      = here
ext ϱ (there x) = there (ϱ x)

rename : ∀ {nl φ ψ} → (∀ {A : Ty nl} → A ∈` φ → A ∈` ψ)
                    → (∀ {A} → Exp φ A → Exp ψ A)
rename ϱ Unit                    = Unit
rename ϱ (Var x)                 = Var (ϱ x)
rename ϱ (SubType expr:A' A'≤A)  = SubType (rename ϱ expr:A') A'≤A
rename {ψ} ϱ (Lab-I l∈snl)       = Lab-I {ψ} l∈snl
rename ϱ (Lab-E expr:snl case)   = Lab-E (rename ϱ expr:snl)
                                   λ l l∈snl → (rename ϱ (case l l∈snl))
rename ϱ (Abs expr:B)            = Abs (rename (ext ϱ) expr:B)
rename ϱ (App expr:A->B expr:A)  = App (rename ϱ expr:A->B) (rename ϱ expr:A)

exts : ∀ {nl φ ψ} → (∀ {A : Ty nl} → A ∈` φ → Exp ψ A)
                  → (∀ {A B} → A ∈` (B ∷ φ) → Exp (B ∷ ψ) A)
exts ϱ here      = Var (here)
exts ϱ (there x) = rename there (ϱ x)

subst : ∀ {nl φ ψ} → (∀ {A : Ty nl} → A ∈` φ → Exp ψ A) -- simult. substitution
                   → (∀ {A : Ty nl} → Exp φ A → Exp ψ A)
subst ϱ Unit                       = Unit
subst ϱ (Var x)                    = ϱ x
subst ϱ (SubType expr:A' A'≤A)     = SubType (subst ϱ expr:A') A'≤A
subst {ψ} ϱ (Lab-I l∈snl)          = Lab-I {ψ} l∈snl
subst ϱ (Lab-E expr:snl case)      = Lab-E (subst ϱ expr:snl)
                                     λ l l∈snl → (subst ϱ (case l l∈snl))
subst ϱ (Abs expr:B)               = Abs (subst (exts ϱ) expr:B)
subst ϱ (App expr:A→B expr:A)     = App (subst ϱ expr:A→B) (subst ϱ expr:A)

_[[_]] : ∀ {nl φ} {A B : Ty nl} → Exp (B ∷ φ) A → Exp φ B → Exp φ A -- single substitution
_[[_]] {nl} {φ} {A} {B} N M = subst {nl} {B ∷ φ} {φ} ϱ {A} N
  where
  ϱ : ∀ {A} → A ∈` (B ∷ φ) → Exp φ A
  ϱ here      = M
  ϱ (there x) = Var x

expansionlemma : ∀ {nl} {lt : Ty nl} {φ φ'} → lt ∈` φ' → lt ∈` (φ' ++ φ)
expansionlemma here      = here
expansionlemma (there x) = there (expansionlemma x)

extensionlemma : ∀ {nl} {lt : Ty nl} {φ φ'} → lt ∈` φ → lt ∈` (φ' ++ φ)
extensionlemma {φ' = []}        here     = here
extensionlemma {φ' = x ∷ xs}   here     = there (extensionlemma{φ' = xs} here)
extensionlemma {φ' = []}       (there y) = there y
extensionlemma {φ' = x ∷ xs}  (there y) = there (extensionlemma {φ' = xs} (there y))

inextdebr : ∀ {nl} {B A : Ty nl} {φ' φ} → B ∈` (φ' ++ φ) → B ∈` (φ' ++ (A ∷ φ))
inextdebr {φ' = []} here           = there here
inextdebr {φ' = []} (there x)      = there (there x)
inextdebr {φ' = x ∷ xs} here      = here
inextdebr {φ' = x ∷ xs} (there y) = there (inextdebr{φ' = xs} y)

inext : ∀ {nl} {φ φ'} {A B : Ty nl} → Exp (φ' ++ φ) B → Exp (φ' ++ (A ∷ φ)) B
inext Unit                                 = Unit
inext {φ' = φ'} (Var x)                    = Var (inextdebr{φ' = φ'} x)
inext {φ = φ}{φ' = φ'} (SubType expr b≤b') = SubType (inext{φ = φ}{φ' = φ'} expr) b≤b'
inext (Lab-I x)                            = Lab-I x
inext {φ = φ} {φ' = φ'} (Lab-E x x₁)       = Lab-E (inext{φ = φ}{φ' = φ'} x) λ l x₂ → inext{φ = φ}{φ' = φ'} (x₁ l x₂)
inext {nl} {φ} {φ'} (Abs{A = A°} x)        = Abs (inext{φ = φ}{φ' = A° ∷ φ'} x)
inext {φ = φ} {φ' = φ'} (App x x₁)         = App (inext{φ = φ}{φ' = φ'} x) (inext{φ = φ}{φ' = φ'} x₁)

debrsub : ∀ {nl} {B B' A A' : Ty nl} {φ' φ} → B ∈` (φ' ++ (A ∷ φ)) → A' ≤ A → B ≤ B' → Exp (φ' ++ (A' ∷ φ)) B'
debrsub {φ' = []}  here a'≤a b≤b'          = SubType (Var here) (≤-trans a'≤a b≤b')
debrsub {φ' = []} (there x) a'≤a b≤b'      = SubType (Var (there x)) b≤b'
debrsub {φ' = x ∷ xs} here a'≤a b≤b'      = SubType (Var (here)) b≤b'
debrsub {φ' = x ∷ xs} (there z) a'≤a b≤b' = inext{φ' = []}{A = x} (debrsub{φ' = xs} z a'≤a b≤b')

typesub : ∀ {nl φ φ' A B A' B'} → Exp{nl} (φ' ++ (A ∷ φ)) B → A' ≤ A → B ≤ B' → Exp (φ' ++ (A' ∷ φ)) B'  -- subtyping "substitution"
typesub Unit a'≤a Sunit = Unit
typesub {φ = φ} {φ'} {A} {B} {A'} {B'} (Var x) a'≤a b≤b'                        = debrsub{φ' = φ'}{φ = φ} x a'≤a b≤b'
typesub {nl} {φ} {φ'} (SubType expr x) a'≤a b≤b'                                = typesub{nl}{φ}{φ'} expr a'≤a (≤-trans x b≤b')
typesub (Lab-I l∈snl) a'≤a b≤b'                                                 = SubType (Lab-I l∈snl) b≤b'
typesub {nl} {φ} {φ'} (Lab-E{snl = snl} expr cases) a'≤a b≤b'                   = Lab-E (typesub{nl}{φ}{φ'} expr a'≤a (≤-refl (Tlabel snl))) λ l x → typesub{nl}{φ}{φ'} (cases l x) a'≤a b≤b'
typesub {φ' = φ'}{A = A}{B = A°→B°}{A' = A'}{B' = A°°→B°°} (Abs{A = A°} expr) a'≤a (Sfun{A = .A°}{A' = A°°}{B = B°}{B' = B°°} A°°≤A° B°≤B°°)
                                                                                = SubType (Abs (typesub{φ' = A° ∷ φ'} expr a'≤a B°≤B°°)) (Sfun A°°≤A° (≤-refl B°°))
typesub {nl}{φ}{φ'}{A}{B}{A'}{B'} (App{A = A°}{B = .B} expr expr') a'≤a b≤b'    = SubType (App (typesub{nl}{φ}{φ'} expr a'≤a (≤-refl (Tfun A° B))) (typesub{nl}{φ}{φ'} expr' a'≤a (≤-refl A°))) b≤b'

-- we force values to have type SubType, since Lab-I results in expressions with type {l}
-- and we want to keep the information about which subset l is in
data Val' {n φ} : (t : Ty n) → Exp {n} φ t → Set where
  Vunit :  Val' (Tunit) Unit
  Vlab : ∀ {l snl l∈snl} → Val' (Tlabel snl) (Lab-I{l = l}{snl} l∈snl)
  Vfun : ∀ {A B exp} → Val' (Tfun A B) (Abs exp)

data _~>_ {n φ} : {A : Ty n} → Exp {n} φ A → Exp {n} φ A → Set where  -- small-steps semantics relation (call-by-value)

  ξ-App1 : ∀ {A B} {L L' : (Exp φ (Tfun B A))} {M}
           → L ~> L'
           → App L M ~> App L' M

  ξ-App2 : ∀ {A B} {M M' : Exp φ A} {L : Exp φ (Tfun A B)}
           → Val' (Tfun A B) L
           → M ~> M'
           → App L M ~> App L M'

  β-App : ∀ {A B M exp}
          → Val' B M
          → App{B = A} (Abs exp) M
             ~>
             (exp [[ M ]])

  ξ-SubType : ∀ {A A' A≤A' } {L L' : Exp φ A}
              → L ~> L'
              → SubType{A = A}{A'} L A≤A' ~> SubType{A = A} L' A≤A'

  ξ-Lab-E : ∀ {A snl} {L L' : Exp φ (Tlabel snl)} {cases}
            → L ~> L'
            → Lab-E{B = A} L cases ~> Lab-E L' cases

  β-Lab-E : ∀ {A l snl l∈snl cases}
            → Lab-E{B = A} (Lab-I{l = l}{snl} l∈snl) cases
               ~>
               cases l (l∈snl)

  γ-Lab-I : ∀ {l snl snl'} {l∈snl : l ∈ snl} {snl⊆snl' : snl ⊆ snl'}
            → SubType (Lab-I{l = l}{snl = snl} l∈snl) (Slabel snl⊆snl')
               ~>
               Lab-I (snl⊆snl' l∈snl)

  γ-Abs : ∀ {A B A' B' e} {A'≤A : A' ≤ A} {B≤B' : B ≤ B'}
          → SubType (Abs{B = B}{A = A} e) (Sfun A'≤A B≤B')
             ~>
             Abs{B = B'}{A = A'} (typesub{φ' = []} e A'≤A B≤B')

  γ-SubType : ∀ {A A' A'' A≤A' A'≤A'' expr}
              → SubType{A = A'}{A' = A''} (SubType{A = A} expr A≤A') A'≤A''
                 ~>
                 SubType expr (≤-trans A≤A' A'≤A'')

  -- either we define Unit values to be SubTypes of Unit≤Unit; or we introducte the following rule
  β-SubType-Unit : SubType Unit Sunit
                   ~>
                   Unit

-- properties of small-step evaluation
infix 2 _~>>_ -- refl. transitive closure
infix 1 begin_
infixr 2 _~>⟨_⟩_
infix 3 _∎

data _~>>_ : ∀ {n} {φ} {A : Ty n} → Exp φ A → Exp φ A → Set where
  _∎ : ∀ {n φ} {A : Ty n} (L : Exp φ A)
       → L ~>> L

  _~>⟨_⟩_ : ∀ {n φ} {A : Ty n} (L : Exp φ A) {M N : Exp φ A}
           → L ~> M
           → M ~>> N
           → L ~>> N

begin_ : ∀ {n φ} {A : Ty n} {M N : Exp φ A} → M ~>> N → M ~>> N
begin M~>>N = M~>>N

-- progress theorem
data Progress {n A} (M : Exp{n} [] A) : Set where
  step : ∀ {N : Exp [] A} → M ~> N → Progress M
  done : Val' A M → Progress M

-- proof
progress : ∀ {n A} → (M : Exp{n} [] A) → Progress M
progress Unit                                                                             = done Vunit
progress (Var ())                                                         -- Var requires a proof for A ∈ [] which cannot exist
progress (SubType Unit Sunit)                                                             = step β-SubType-Unit
progress (SubType (Var ()) A'≤A)
progress (SubType (SubType expr:A' x) A'≤A)                                               = step γ-SubType
progress (SubType (Lab-I{l}{snl} l∈snl) (Slabel{snl' = snl'} snl⊆snl'))                  = step γ-Lab-I
progress (SubType (Lab-E expr:A' x) A'≤A) with progress (Lab-E expr:A' x)
...                                           | step a                                    = step (ξ-SubType a)
...                                           | done ()                   -- Lab-E without SubType can't be a value
progress (SubType (Abs expr:A') (Sfun A'≤A B≤B')) with progress (Abs expr:A')
...                                           | step a                                    = step (ξ-SubType a)
...                                           | done Vfun                                 = step γ-Abs
progress (SubType (App expr:A' expr:A'') A'≤A) with progress (expr:A')
...                                           | step a                                    = step (ξ-SubType (ξ-App1 a))
...                                           | done Vfun with progress (expr:A'')
...                                              | step b                                 = step (ξ-SubType (ξ-App2 Vfun b))
...                                              | done val                               = step (ξ-SubType (β-App val))
progress (Lab-I l∈snl)                                                                    = done Vlab
progress (Lab-E expr cases) with progress expr
...                                           | step expr~>expr'                          = step (ξ-Lab-E expr~>expr')
...                                           | done Vlab                                 = step (β-Lab-E)
progress (Abs expr)                                                                       = done Vfun
progress (App L M) with progress L
...                                           | step L~>L'                                = step (ξ-App1 L~>L')
...                                           | done Vfun with progress M
...                                              | step M~>M'                             = step (ξ-App2 Vfun M~>M')
...                                              | done x                                 = step (β-App x)

-- generation of evaluation sequences
-- taken from plfa

data Gas : Set where
  gas : ℕ → Gas

data Finished {n φ A} (N : Exp{n} φ A) : Set where
  done : Val' A N → Finished N
  out-of-gas : Finished N

data Steps : ∀ {n A} → Exp{n} [] A → Set where
  steps : ∀ {n A} {L N : Exp{n} [] A}
          → L ~>> N
          → Finished N
          → Steps L

eval' : ∀ {n A} → Gas → (L : Exp{n} [] A) → Steps L
eval' (gas zero) L              = steps (L ∎) out-of-gas
eval' (gas (suc m)) L with progress L
...      | done VL              = steps (L ∎) (done VL)
...      | step {M} L~>M with eval' (gas m) M
...         | steps M~>>N fin   = steps (L ~>⟨ L~>M ⟩ M~>>N) fin

-- examples
-- (λ (x : Unit) → x) (Unit)
ex0 : Exp{suc zero} [] Tunit
ex0 = App (Abs (Unit{φ = (Tunit ∷ [])})) (Unit)

_ : ex0 ~>> Unit
_ =
  begin
    App (Abs (Unit)) (Unit)
  ~>⟨ β-App (Vunit) ⟩
    Unit
  ∎

ex1 : Exp{suc zero} [] Tunit
ex1 = Lab-E (Lab-I (x∈⁅x⁆ zero)) λ l x → Unit

_ : ex1 ~>> Unit
_ =
  begin
    Lab-E (Lab-I (x∈⁅x⁆ zero)) (λ l x → Unit)
  ~>⟨ β-Lab-E ⟩
    Unit
  ∎

ex2 : Exp{suc zero} [] Tunit
ex2 = App (SubType (Abs Unit) (Sfun Sunit Sunit)) Unit

-- proof that {inside, outside} ⊆ {inside, inside}
-- i.e.                     {0} ⊆ {0, 1}
x⊆y : (inside ∷ outside ∷ []) ⊆ (inside ∷ inside ∷ [])
x⊆y {.zero}    here      = here
x⊆y {.(suc (suc _))} (there (there ()))

-- proof that zero is in (inside ∷ outside ∷ [])
-- i.e.                    0 ∈ {0}
l∈snl : (zero) ∈ (inside ∷ outside ∷ [])
l∈snl = here

-- [({0, 1}→{0, 1} <: {0}→{0, 1}) (λ x : {0, 1} . x)] 0
ex3 : Exp{suc (suc zero)} [] (Tlabel (inside ∷ inside ∷ []))
ex3 = App (SubType (Abs{A = Tlabel (inside ∷ inside ∷ [])}  (Var here)) (Sfun (Slabel{snl = (inside ∷ outside ∷ [])} x⊆y) (≤-refl (Tlabel (inside ∷ inside ∷ [])))))
          (Lab-I l∈snl)

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Wrapper for the erased modality
--
-- This allows us to store erased proofs in a record and use projections
-- to manipulate them without having to turn on the unsafe option
-- --irrelevant-projections.
------------------------------------------------------------------------

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

module Data.Erased where

open import Level using (Level)

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

------------------------------------------------------------------------
-- Type

record Erased (A : Set a) : Set a where
  constructor [_]
  field .erased : A
open Erased public

------------------------------------------------------------------------
-- Algebraic structure: Functor, Appplicative and Monad-like

map : (A → B) → Erased A → Erased B
map f [ a ] = [ f a ]

pure : A → Erased A
pure x = [ x ]

infixl 4 _<*>_
_<*>_ : Erased (A → B) → Erased A → Erased B
[ f ] <*> [ a ] = [ f a ]

infixl 1 _>>=_
_>>=_ : Erased A → (.A → Erased B) → Erased B
[ a ] >>= f = f a

------------------------------------------------------------------------
-- Other functions

zipWith : (A → B → C) → Erased A → Erased B → Erased C
zipWith f a b = ⦇ f a b ⦈