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

module Examples.Queue where

open import Calf.CostMonoid
open import Calf.CostMonoids using (ℕ-CostMonoid)

costMonoid = ℕ-CostMonoid
open CostMonoid costMonoid using (ℂ)

open import Calf costMonoid
open import Calf.Types.Nat
open import Calf.Types.Unit
open import Calf.Types.Sum
open import Calf.Types.Bounded costMonoid

open import Function
open import Data.Nat
open import Data.Nat.Properties
import Data.Integer as Int
import Data.Integer.Properties as IntP
open import Data.List renaming (sum to lsum)
open import Data.Product
open import Relation.Binary.PropositionalEquality as P

record Queue (A : tp pos) : Set where
  field
    Q : tp pos
    emp : val Q
    enq : cmp (Π Q λ _ → Π A λ _ → F Q)
    deq : cmp (Π Q λ _ → F (sum unit (Σ++ Q λ _ → A)))

module CostList (A : tp pos) (n : ℕ) where
  -- Suppose we want to implement the Queue signature above using lists.
  -- One cost model is to count the number of times a cons node is inspected.
  -- This is implemented by the following annotated list type:
  -- destructing a cons node of type list n A consumes n steps.
  postulate
    list : tp pos
    nil : val list
    cons : val A → val list → val list

    list/ind : (l : val list) → (X : val list → tp neg) → cmp (X nil) →
      ((a : val A) → (l : val list) → (r : val (U (X l))) →
        cmp (X (cons a l))) →
      cmp (X l)
    list/ind/nil : ∀ {X} → (e0 : cmp (X nil)) →
        (e1 : (a : val A) → (l : val list) → (r : val (U (X l))) →
        cmp (X (cons a l))) →
      list/ind nil X e0 e1 ≡ e0
    {-# REWRITE list/ind/nil #-}
    list/ind/cons : ∀ {X} → (a : val A) → (l : val list) → (e0 : cmp (X nil)) →
        (e1 : (a : val A) → (l : val list) → (r : val (U (X l))) →
        cmp (X (cons a l))) →
      list/ind (cons a l) X e0 e1 ≡ step (X (cons a l)) n (e1 a l (list/ind l X e0 e1))
    {-# REWRITE list/ind/cons #-}

  list/match : (l : val list) → (X : val list → tp neg) → cmp (X nil) →
    ((a : val A) → (l : val list) → cmp (X (cons a l))) →
    cmp (X l)
  list/match l X e0 e1 = list/ind l X e0 (λ a l _ → e1 a l)

  bound/list/match : ∀ (l : val list) (X : val list → tp pos)
    {e0 : val (U (F (X nil)))} {e1 : (a : val A) → (l : val list) → val (U (F (X (cons a l))))}
    {p0 : val (U cost)} {p1 : (a : val A) → (l : val list) → val (U cost)} →
    IsBounded (X nil) e0 p0 →
    ((a : val A) → (l : val list) → IsBounded (X (cons a l)) (e1 a l) (p1 a l)) →
    IsBounded (X l) (list/match l (F ∘ X) e0 e1) (list/match l (λ _ → cost) p0 (λ a l → n + p1 a l))
  bound/list/match l X {e0} {e1} {p0} {p1} ub0 ub1 =
    list/match l (λ l → meta (IsBounded (X l) (list/match l (F ∘ X) e0 e1) (list/match l (λ _ → cost) p0 (λ a l → n + p1 a l))))
      ub0
      λ a l → bound/circ n (bound/step n (p1 a l) (ub1 a l))

  len : val list → ℕ
  len l = list/ind l (λ _ → meta ℕ) 0 λ a l r → 1 + r

module Ex/CostList where
  open CostList nat 0

  ex : val list
  ex = cons 0 (cons 1 nil)

module Rev (A : tp pos) where
  open CostList A 1

  revAppend : cmp (Π list λ _ → Π list λ _ → F list)
  revAppend l =
    list/ind l (λ _ → Π list λ _ → F list)
      (λ l' → ret l')
      λ x _ r → λ l' → r (cons x l')

  revAppend/lemma/cons : ∀ x xs l' → ◯ (∃ λ y → ∃ λ ys → (len ys ≡ len xs + len l') × revAppend (cons x xs) l' ≡ ret (cons y ys))
  revAppend/lemma/cons x xs =
    list/ind xs (λ xs → meta (∀ x l' → ◯ (∃ λ y → ∃ λ ys → (len ys ≡ len xs + len l') × revAppend (cons x xs) l' ≡ ret (cons y ys))))
      (λ x l' u → (x , l' , refl , step/ext (F list) (ret (cons x l')) 1 u))
      (λ x' xs' ih x l' u →
        let (y , ys , h , ≡) = ih x' (cons x l') u in
        let open ≡-Reasoning in
        y , ys , (
          begin
            len ys
          ≡⟨ h ⟩
            len xs' + len (cons x l')
          ≡⟨⟩
            len xs' + step (meta ℕ) 1 (suc (len l'))
          ≡⟨ cong (len xs' +_) (step/ext (meta ℕ) (suc (len l')) 1 u) ⟩
            len xs' + suc (len l')
          ≡⟨ +-suc (len xs') (len l') ⟩
            suc (len xs' + len l')
          ≡⟨⟩
            suc (len xs') + len l'
          ≡˘⟨ cong (_+ len l') (step/ext (meta ℕ) (suc (len xs')) 1 u) ⟩
            step (meta ℕ) 1 (suc (len xs')) + len l'
          ≡⟨⟩
            len (cons x' xs') + len l'
          ∎
        ) , (
          begin
            revAppend (cons x (cons x' xs')) l'
          ≡⟨⟩
            step (F list) 1 (revAppend (cons x' xs') (cons x l'))
          ≡⟨ step/ext (F list) _ 1 u ⟩
            revAppend (cons x' xs') (cons x l')
          ≡⟨ (≡) ⟩
            ret (cons y ys)
          ∎
        ))
      x

  revAppend/cost : cmp (Π list λ _ → Π list λ _ → cost)
  revAppend/cost l l' = len l

  revAppend≤revAppend/cost : ∀ l l' → IsBounded list (revAppend l l') (revAppend/cost l l')
  revAppend≤revAppend/cost l =
    list/ind l (λ l → meta (∀ l' → IsBounded list (revAppend l l') (revAppend/cost l l')))
      (λ l' → bound/ret)
      (λ a l r → λ l' → bound/circ 1 (bound/step 1 (len l) (r (cons a l'))))

  rev : cmp (Π list λ _ → F list)
  rev l = revAppend l nil

  rev/lemma/cons : ∀ x xs → ◯ (∃ λ y → ∃ λ ys → len ys ≡ len xs × rev (cons x xs) ≡ ret (cons y ys))
  rev/lemma/cons x xs =
    subst (λ n → ◯ (∃ λ y → ∃ λ ys → len ys ≡ n × rev (cons x xs) ≡ ret (cons y ys)))
      (+-identityʳ _)
      (revAppend/lemma/cons x xs nil)

  rev/cost : cmp (Π list λ _ → cost)
  rev/cost l = len l

  rev≤rev/cost : ∀ l → IsBounded list (rev l) (rev/cost l)
  rev≤rev/cost l = revAppend≤revAppend/cost l nil

-- Implement Queue with a pair of lists; (f , b) represents the queue f :: rev b.
module FrontBack (A : tp pos) where
  -- For simplicity, we charge 1 step for each cons node destruction.
  open CostList A 1
  open Rev A

  Q : tp pos
  Q = Σ++ list λ _ → list

  emp : val Q
  emp = (nil , nil)

  enq : cmp (Π Q λ _ → Π A λ _ → F Q)
  enq (f , b) x = ret (f , cons x b)

  enq/cost : cmp (Π Q λ _ → Π A λ _ → cost)
  enq/cost (f , b) x = 0

  enq≤enq/cost : ∀ q x → IsBounded Q (enq q x) (enq/cost q x)
  enq≤enq/cost q x = bound/ret

  deq-tp = sum unit (Σ++ Q λ _ → A)

  deq/emp : cmp (Π list λ _ → F deq-tp)
  deq/emp l =
    list/match l (λ _ → F deq-tp)
      (ret (inj₁ triv))
      λ a l' → ret (inj₂ ((l' , nil) , a))

  deq/emp/cost : cmp (Π list λ _ → cost)
  deq/emp/cost l =
    list/match l (λ _ → cost)
      0
      λ a l' → 1 + 0

  deq/emp≤deq/emp/cost : ∀ l → IsBounded deq-tp (deq/emp l) (deq/emp/cost l)
  deq/emp≤deq/emp/cost l =
    bound/list/match l (λ _ → deq-tp)
      bound/ret
      λ a l' → bound/ret

  deq : cmp (Π Q λ _ → F deq-tp)
  deq (f , b) =
    list/match f (λ _ → F deq-tp)
      (bind (F deq-tp) (rev b) (λ b' → deq/emp b'))
      λ a l → ret (inj₂ ((l , b) , a))

  deq/cost : cmp (Π Q λ _ → cost)
  deq/cost (f , b) =
    list/match f (λ _ → cost)
      (bind cost (rev b) (λ b' → rev/cost b + deq/emp/cost b'))
      λ a l → 1 + 0

  deq/cost/closed : cmp (Π Q λ _ → cost)
  deq/cost/closed (f , b) =
    list/match f (λ _ → cost)
      (list/match b (λ _ → cost) 0 (λ _ b' → 1 + len b))
      λ _ _ → 1

  deq/cost≤deq/cost/closed : ∀ q → ◯ (deq/cost q ≤ deq/cost/closed q)
  deq/cost≤deq/cost/closed (f , b) u =
    list/match f (λ f → meta (deq/cost (f , b) ≤ deq/cost/closed (f , b)))
      (list/match b (λ b → meta (deq/cost (nil , b) ≤ deq/cost/closed (nil , b)))
        ≤-refl
        λ x xs →
          let open ≤-Reasoning in
          let (y , ys , _ , ≡) = rev/lemma/cons x xs u in
          begin
            deq/cost (nil , cons x xs)
          ≡⟨⟩
            bind cost (rev (cons x xs)) (λ b' → rev/cost (cons x xs) + deq/emp/cost b')
          ≡⟨⟩
            bind cost (rev (cons x xs)) (λ b' → rev/cost (cons x xs) + deq/emp/cost b')
          ≡⟨ cong (λ e → bind cost e (λ b' → rev/cost (cons x xs) + deq/emp/cost b')) (≡) ⟩
            rev/cost (cons x xs) + deq/emp/cost (cons y ys)
          ≡⟨⟩
            step cost 1 (suc (len xs)) + step cost 1 1
          ≡⟨ cong₂ _+_ (step/ext cost (suc (len xs)) 1 u) (step/ext cost 1 1 u) ⟩
            suc (len xs) + 1
          ≡⟨ +-comm (suc (len xs)) 1 ⟩
            suc (suc (len xs))
          ≡˘⟨ cong suc (step/ext cost _ 1 u) ⟩
            suc (step cost 1 (suc (len xs)))
          ≡⟨⟩
            suc (len (cons x xs))
          ≡˘⟨ step/ext cost _ 1 u ⟩
            step cost 1 (suc (len (cons x xs)))
          ≡⟨⟩
            list/match (cons x xs) (λ _ → cost) 0 (λ _ b' → 1 + len (cons x xs))
          ≡⟨⟩
            deq/cost/closed (nil , cons x xs)
          ∎
      )
      λ _ _ → ≤-refl

  deq≤deq/cost : ∀ q → IsBounded deq-tp (deq q) (deq/cost q)
  deq≤deq/cost (f , b) =
    bound/list/match f (λ _ → deq-tp)
      (bound/bind (rev/cost b) _ (rev≤rev/cost b) λ b' → deq/emp≤deq/emp/cost b')
      λ a l → bound/ret

  deq≤deq/cost/closed : ∀ q → IsBounded deq-tp (deq q) (deq/cost/closed q)
  deq≤deq/cost/closed q = bound/relax (deq/cost≤deq/cost/closed q) (deq≤deq/cost q)

  -- Amortized analysis for front-back queue.
  -- The goal is to bound the cost of a single-thread sequence of queue operations staring with an initial queue q0,
  -- where an operation is either an enqueue or a dequeue.
  data op : Set where
    op/enq : (x : val A) → op
    op/deq : op

  -- Potential function
  ϕ : val Q → ℕ
  ϕ (f , b) = len f + 2 * len b

  -- o operate q is the computation induced by operation o on queue q.
  -- Needed because deq doesn't always return a queue (e.g., deq emp).
  -- In these cases we just return the empty queue.
  _operate_ : op → val Q → cmp (F Q)
  (op/enq x) operate q = enq q x
  (op/deq) operate q =
    bind (F Q) (deq q) λ s → (sum/case unit (Σ++ Q λ _ → A) (λ _ → F Q) s
    (λ _ → ret (nil , nil))
    (λ (q , x) → ret q))

  -- o operateϕ q is morally ϕ (o operate q), which doesn't type-check since o operate q is a computation.
  -- Easier to work with than bind cost (o operate q) ϕ (but they are equivalent, as shown below).
  _operateϕ_ : op → val Q → ℂ
  (op/enq x) operateϕ (f , b) = len f + 2 * (1 + len b)
  (op/deq) operateϕ (f , b) = list/match f (λ _ → cost) (list/match b (λ _ → cost) 0 (λ _ b' → len b')) (λ _ f' → len f' + 2 * len b)

  operateϕ≡ϕ∘operate : ∀ o q → ◯ (o operateϕ q ≡ bind cost (o operate q) ϕ)
  operateϕ≡ϕ∘operate (op/enq x) (f , b) u =
    begin
      len f + 2 * (1 + len b)
    ≡˘⟨ cong (λ n → len f + 2 * n) (step/ext cost (1 + len b) 1 u) ⟩
      len f + 2 * step cost 1 (1 + len b)
    ≡⟨⟩
      bind cost (enq (f , b) x) ϕ
    ∎
      where open ≡-Reasoning
  operateϕ≡ϕ∘operate op/deq (f , b) u = list/match f
        (λ f →
          meta
          ((op/deq operateϕ (f , b)) ≡
            bind cost (op/deq operate (f , b)) ϕ))
        (list/ind b (λ b → meta ((op/deq operateϕ (nil , b)) ≡ bind cost (op/deq operate (nil , b)) ϕ))
        refl
        λ a l ih → emp/cons a l)
        λ a l → refl

    where
    emp/cons : ∀ a l → op/deq operateϕ (nil , cons a l) ≡ bind cost (op/deq operate (nil , cons a l)) ϕ
    emp/cons a l with rev/lemma/cons a l u
    ... | (x' , l' , eqn1 , eqn2) =
      begin
        op/deq operateϕ (nil , cons a l)
      ≡⟨⟩
        step cost 1 (len l)
      ≡⟨ step/ext cost (len l) 1 u ⟩
        len l
      ≡⟨ P.sym eqn1 ⟩
        len l'
      ≡⟨ P.sym (+-identityʳ (len l')) ⟩
        len l' + 0
      ≡⟨⟩
        len l' + 2 * len nil
      ≡⟨⟩
        ϕ (l' , nil)
      ≡˘⟨ step/ext cost (ϕ (l' , nil)) 1 u ⟩
        step cost 1 (ϕ (l' , nil))
      ≡⟨⟩
        bind cost
          (step (F Q) 1 (ret (l' , nil)))
          ϕ
      ≡⟨⟩
        bind cost
          (bind (F Q) (step (F deq-tp) 1 (ret (inj₂ ((l' , nil) , x')))) λ s → (sum/case unit (Σ++ Q λ _ → A) (λ _ → F Q) s
            (λ _ → ret (nil , nil))
            (λ (q , x) → ret q)))
          ϕ
      ≡⟨⟩
        bind cost
          (bind (F Q) (deq/emp (cons x' l')) λ s → (sum/case unit (Σ++ Q λ _ → A) (λ _ → F Q) s
            (λ _ → ret (nil , nil))
            (λ (q , x) → ret q)))
          ϕ
      ≡˘⟨
        cong
          (λ e →
            bind cost
              (bind (F Q) e λ l' →
                bind (F Q) (deq/emp l') λ s → (sum/case unit (Σ++ Q λ _ → A) (λ _ → F Q) s
                  (λ _ → ret (nil , nil))
                  (λ (q , x) → ret q)))
              ϕ
          )
          eqn2
      ⟩
        bind cost
          (bind (F Q) (rev (cons a l)) λ l' →
            bind (F Q) (deq/emp l') λ s → (sum/case unit (Σ++ Q λ _ → A) (λ _ → F Q) s
              (λ _ → ret (nil , nil))
              (λ (q , x) → ret q)))
          ϕ
      ≡⟨⟩
        bind cost
          (bind (F Q) (deq (nil , cons a l)) λ s → (sum/case unit (Σ++ Q λ _ → A) (λ _ → F Q) s
            (λ _ → ret (nil , nil))
            (λ (q , x) → ret q)))
          ϕ
      ≡⟨⟩
        bind cost (op/deq operate (nil , cons a l)) ϕ
      ∎
      where open ≡-Reasoning

  -- op/cost o q is the cost of o operate q.
  op/cost : op → val Q → ℕ
  op/cost (op/enq x) q = 0
  op/cost (op/deq) (f , b) = list/match f (λ _ → cost) (list/match b (λ _ → cost) 0 (λ _ b' → 2 + len b')) (λ _ _ → 1)

  deq/cost≡cost/deq : ∀ q → ◯ (deq/cost/closed q ≡ op/cost op/deq q)
  deq/cost≡cost/deq (f , b) u =
    P.cong (λ x → list/match f (λ _ → cost) x (λ _ _ → 1)) (
      list/match b
        (λ b →
          meta
            (list/match b (λ _ → cost) 0 (λ _ b' → 1 + len b) ≡
              list/match b (λ _ → cost) 0 (λ _ b' → 2 + len b')))
        refl
        (λ a l →
          let open ≡-Reasoning in
          begin
            list/match (cons a l) (λ _ → cost) 0 (λ _ b' → 1 + len (cons a l))
          ≡⟨⟩
            step cost 1 (1 + len (cons a l))
          ≡⟨ step/ext cost (1 + len (cons a l)) 1 u ⟩
            1 + len (cons a l)
          ≡⟨⟩
            1 + step cost 1 (suc (len l))
          ≡⟨ cong (1 +_) (step/ext cost (suc (len l)) 1 u) ⟩
            2 + len l
          ≡˘⟨ step/ext cost (2 + len l) 1 u ⟩
            step cost 1 (2 + len l)
          ≡⟨⟩
            list/match (cons a l) (λ _ → cost) 0 (λ _ b' → 2 + len b')
          ∎
        )
    )

  -- cost o q upperbounds the cost of o operate q.
  op≤op/cost : ∀ o q → IsBounded Q (o operate q) (op/cost o q)
  op≤op/cost (op/enq x) q = enq≤enq/cost q x
  op≤op/cost op/deq q rewrite P.sym (+-identityʳ (op/cost (op/deq) q)) =
    bound/bind/const {A = deq-tp} {e = deq q} {f = λ s → (sum/case unit (Σ++ Q λ _ → A) (λ _ → F Q) s (λ _ → ret (nil , nil)) (λ (q , x) → ret q))}
      (op/cost op/deq q) 0
      (bound/relax (λ u → ≤-reflexive (deq/cost≡cost/deq q u)) (deq≤deq/cost/closed q))
      λ a →
        bound/sum/case/const/const unit ((Σ++ Q λ _ → A)) (λ _ → Q) a ((λ _ → ret (nil , nil))) (λ (q , x) → ret q) 0
          (λ _ → bound/ret)
          (λ _ → bound/ret)

  -- is/acost o k when for any state q, k suffices for the cost of o on q and the difference in the potential.
  is/acost :  op → ℕ → Set
  is/acost o k = ∀ q → (Int.+ (op/cost o q)) Int.+ ((o operateϕ q) Int.⊖ (ϕ q)) Int.≤ Int.+ k

  acost/weaken : ∀ {m n o} → m ≤ n → is/acost o m → is/acost o n
  acost/weaken h1 h2 = λ q → IntP.≤-trans (h2 q) (Int.+≤+ h1)

  -- A sequence of operations induces a single computation by threading through the initial state q0.
  _op/seq_ : List op → val Q → cmp (F Q)
  [] op/seq q0 = ret q0
  (o ∷ os) op/seq q = bind (F Q) (o operate q) λ q' → os op/seq q'

  op/seq/cost : ∀ (l : List op) → val Q → ℂ
  op/seq/cost [] q0 = 0
  op/seq/cost (o ∷ os) q = bind cost (o operate q) λ q' → op/cost o q + op/seq/cost os q'

  -- Cost of a sequence computation is bounded by the sum of cost of the constituents.
  op/seq≤op/seq/cost : ∀ l q → IsBounded Q (l op/seq q) (op/seq/cost l q)
  op/seq≤op/seq/cost [] q0 = bound/ret
  op/seq≤op/seq/cost (o ∷ os) q = bound/bind {A = Q} {e = o operate q} {f = λ q → os op/seq q}
   (op/cost o q) (op/seq/cost os) (op≤op/cost o q) λ q → op/seq≤op/seq/cost os q

  -- Telescoping the potential.
  op/seq/cost/tele : ∀ (l : List op) → val Q → Int.ℤ
  op/seq/cost/tele [] q0 = Int.0ℤ
  op/seq/cost/tele (o ∷ os) q = bind (meta Int.ℤ) (o operate q) λ q' → (Int.+ (op/cost o q)) Int.+ (o operateϕ q Int.⊖ ϕ q) Int.+ (op/seq/cost/tele os q')

  ϕn : ℕ → List op → val Q → ℕ
  ϕn zero l q0 = ϕ q0
  ϕn (suc n) (o ∷ os) q = bind cost (o operate q) λ q' → ϕn n os q'
  ϕn (suc n) [] q = 0

  -- Potential of the initial state
  ϕ/0 : List op → val Q → ℕ
  ϕ/0 l = ϕn 0 l

  -- Potential of the final state
  ϕ/-1 : List op → val Q → ℕ
  ϕ/-1 l = ϕn (length l) l

  bind/dup : ∀ A 𝕊 𝕋 e f (g : val A → 𝕊 → 𝕋) → bind {A} (meta 𝕋) e (λ a → g a (bind {A} (meta 𝕊) e f)) ≡ bind {A} (meta 𝕋) e (λ a → g a (f a))
  bind/dup A 𝕊 𝕋 e f g =
    begin
    bind (meta 𝕋) e (λ a → g a (bind (meta 𝕊) e f)) ≡⟨ P.cong (λ h → bind (meta 𝕋) e h) (funext (λ a → bind/meta A 𝕊 𝕋 e f (λ s → g a s))) ⟩
    bind (meta 𝕋) e (λ a → bind (meta 𝕋) e (λ a' → g a (f a'))) ≡⟨ bind/idem A 𝕋 e (λ a a' → g a (f a')) ⟩
    bind (meta 𝕋) e (λ a → g a (f a)) ≡⟨ refl ⟩
    bind (meta 𝕋) e (λ a → g a (f a))
    ∎
    where open ≡-Reasoning

  -- Telescoping sum:
  -- Σᵢⁿ op/cost oᵢ + ϕ qᵢ - ϕ qᵢ₋₁ = ϕ q_{n-1} - ϕ q_0 + Σᵢ costᵢ
  cost≡cost/tele : ∀ l q → ◯ (op/seq/cost/tele l q ≡ (ϕ/-1 l q Int.⊖ ϕ/0 l q) Int.+ (Int.+ (op/seq/cost l q)))
  cost≡cost/tele [] q u =
    P.sym
    (
      begin
      (ϕ q Int.⊖ ϕ q) Int.+ (Int.+ 0) ≡⟨ IntP.+-identityʳ (ϕ q Int.⊖ ϕ q) ⟩
      ϕ q Int.⊖ ϕ q ≡⟨ IntP.n⊖n≡0 (ϕ q) ⟩
      Int.+ 0 ≡⟨ refl ⟩
      Int.+ 0
      ∎
    )
    where open ≡-Reasoning
  cost≡cost/tele (o ∷ os) q u rewrite operateϕ≡ϕ∘operate o q u
                                  | bind/meta Q ℕ Int.ℤ
                                    (o operate q)
                                    (λ q' → op/cost o q + op/seq/cost os q')
                                    (λ x → (ϕ/-1 (o ∷ os) q Int.⊖ ϕ/0 (o ∷ os) q) Int.+ (Int.+ x))
                                  | bind/dup Q ℕ Int.ℤ (o operate q) (ϕ/-1 os) (λ q' x → (x Int.⊖ ϕ q) Int.+ (Int.+ (op/cost o q + op/seq/cost os q')))
                                  | bind/dup Q ℕ Int.ℤ (o operate q) ϕ (λ q' x → Int.+ (op/cost o q) Int.+ (x Int.⊖ ϕ q) Int.+ (op/seq/cost/tele os q')) =
    P.cong (λ f → bind (meta Int.ℤ) (o operate q) f)
    (funext (λ q' →
    (
      begin
      (Int.+ (op/cost o q)) Int.+ (ϕ q' Int.⊖ ϕ q) Int.+ (op/seq/cost/tele os q') ≡⟨ P.cong (λ x → (Int.+ (op/cost o q)) Int.+ (ϕ q' Int.⊖ ϕ q) Int.+ x) (cost≡cost/tele os q' u) ⟩
      Int.+ op/cost o q Int.+ (ϕ q' Int.⊖ ϕ q) Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q' Int.+ Int.+ op/seq/cost os q') ≡⟨ P.cong (λ x → x Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q' Int.+ Int.+ op/seq/cost os q')) (IntP.+-comm (Int.+ op/cost o q) (ϕ q' Int.⊖ ϕ q)) ⟩
      ϕ q' Int.⊖ ϕ q Int.+ Int.+ op/cost o q Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q' Int.+ Int.+ op/seq/cost os q') ≡⟨ IntP.+-assoc (ϕ q' Int.⊖ ϕ q) (Int.+ op/cost o q) (ϕ/-1 os q' Int.⊖ ϕ/0 os q' Int.+ Int.+ op/seq/cost os q') ⟩
      ϕ q' Int.⊖ ϕ q Int.+ (Int.+ op/cost o q Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q' Int.+ Int.+ op/seq/cost os q')) ≡⟨ P.cong (λ x → ϕ q' Int.⊖ ϕ q Int.+ x) (P.sym (IntP.+-assoc (Int.+ op/cost o q) (ϕ/-1 os q' Int.⊖ ϕ/0 os q') (Int.+ op/seq/cost os q'))) ⟩
      ϕ q' Int.⊖ ϕ q Int.+ (Int.+ op/cost o q Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q') Int.+ Int.+ op/seq/cost os q') ≡⟨ P.cong (λ x → ϕ q' Int.⊖ ϕ q Int.+ (x Int.+ Int.+ op/seq/cost os q')) (IntP.+-comm (Int.+ op/cost o q) (ϕ/-1 os q' Int.⊖ ϕ/0 os q')) ⟩
      ϕ q' Int.⊖ ϕ q Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q' Int.+ Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q') ≡⟨ P.cong (λ x → ϕ q' Int.⊖ ϕ q Int.+ x) (IntP.+-assoc (ϕ/-1 os q' Int.⊖ ϕ/0 os q') (Int.+ op/cost o q) (Int.+ op/seq/cost os q')) ⟩
      ϕ q' Int.⊖ ϕ q Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q' Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q')) ≡⟨ P.sym (IntP.+-assoc (ϕ q' Int.⊖ ϕ q) (ϕ/-1 os q' Int.⊖ ϕ/0 os q') (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q')) ⟩
      ϕ q' Int.⊖ ϕ q Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q') Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q') ≡⟨ P.cong (λ x → x Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q') Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q')) (P.sym (IntP.m-n≡m⊖n (ϕ q') (ϕ q))) ⟩
      Int.+ ϕ q' Int.- (Int.+ ϕ q) Int.+ (ϕ/-1 os q' Int.⊖ ϕ/0 os q') Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q') ≡⟨ P.cong (λ x → Int.+ ϕ q' Int.- (Int.+ ϕ q) Int.+ x Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q')) (P.sym (IntP.m-n≡m⊖n (ϕ/-1 os q') (ϕ/0 os q'))) ⟩
      Int.+ ϕ q' Int.- Int.+ ϕ q Int.+ (Int.+ ϕ/-1 os q' Int.- (Int.+ ϕ/0 os q')) Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q') ≡⟨ P.cong (λ x → x Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q')) (IntP.+-comm (Int.+ ϕ q' Int.- Int.+ ϕ q) (Int.+ ϕ/-1 os q' Int.- (Int.+ ϕ/0 os q'))) ⟩
      Int.+ ϕ/-1 os q' Int.- Int.+ ϕ/0 os q' Int.+ (Int.+ ϕ q' Int.- Int.+ ϕ q) Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q') ≡⟨ P.cong (λ x → x Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q')) (IntP.+-minus-telescope (Int.+ ϕ/-1 os q') (Int.+ ϕ q') (Int.+ ϕ q)) ⟩
      Int.+ ϕ/-1 os q' Int.- Int.+ ϕ q Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q') ≡⟨ P.cong (λ x → x Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q')) (IntP.m-n≡m⊖n (ϕ/-1 os q') (ϕ q )) ⟩
      ϕ/-1 os q' Int.⊖ ϕ q Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q') ≡⟨ refl ⟩
      ϕ/-1 os q' Int.⊖ ϕ q Int.+ (Int.+ op/cost o q Int.+ Int.+ op/seq/cost os q')
      ∎
    )
    ))
    where open ≡-Reasoning

  data Amortized : List op → List ℕ → Set where
    a/emp : Amortized [] []
    a/cons : ∀ o k l l' → is/acost o k → Amortized l l' → Amortized (o ∷ l) (k ∷ l')

  amortized≥cost/tele : ∀ q0 l l' → Amortized l l' → Int.+ (lsum l') Int.≥ op/seq/cost/tele l q0
  amortized≥cost/tele q .[] .[] a/emp = IntP.≤-refl
  amortized≥cost/tele q .(o ∷ os) .(k ∷ l') (a/cons o k os l' x h) rewrite tbind/meta Q Int.ℤ (o operate q) (λ q' → (Int.+ (op/cost o q)) Int.+ (o operateϕ q Int.⊖ ϕ q) Int.+ (op/seq/cost/tele os q')) (λ z → z Int.≤ Int.+ lsum (k ∷ l')) =
    dbind (λ q' → meta ((Int.+ (op/cost o q)) Int.+ (o operateϕ q Int.⊖ ϕ q) Int.+ (op/seq/cost/tele os q') Int.≤ Int.+ lsum (k ∷ l'))) (o operate q)
    λ q' →
    begin
    Int.+ op/cost o q Int.+ ((o operateϕ q) Int.⊖ ϕ q) Int.+ op/seq/cost/tele os q' ≤⟨ IntP.+-monoˡ-≤ (op/seq/cost/tele os q') (x q) ⟩
    Int.+ k Int.+ op/seq/cost/tele os q' ≤⟨ IntP.+-monoʳ-≤ (Int.+ k) (amortized≥cost/tele q' os l' h) ⟩
    Int.+ k Int.+ Int.+ lsum l' ≤⟨ IntP.≤-refl ⟩
    Int.+ k Int.+ Int.+ lsum l'
    ∎
   where open IntP.≤-Reasoning

  -- Sum of a sequence of amortized costs (plus the initial potential) bounds the sum of the sequence of actual costs
  amortized≥cost : ∀ q l l' → Amortized l l' → ◯ (Int.+ (ϕ q + lsum l') Int.≥ Int.+ (op/seq/cost l q))
  amortized≥cost q l l' h u =
    begin
    Int.+ (op/seq/cost l q) ≤⟨ IntP.n≤m+n (0 + ϕ/-1 l q) ⟩
    Int.0ℤ Int.+ (Int.+ ϕ/-1 l q) Int.+ Int.+ op/seq/cost l q ≡⟨ P.cong (λ x → x Int.+ (Int.+ ϕ/-1 l q) Int.+ Int.+ op/seq/cost l q) (P.sym (IntP.n⊖n≡0 (ϕ q))) ⟩
    ϕ q Int.⊖ ϕ q Int.+ Int.+ ϕ/-1 l q Int.+ Int.+ op/seq/cost l q ≡⟨ P.cong (λ x → x Int.+ (Int.+ ϕ/-1 l q) Int.+ Int.+ op/seq/cost l q) (P.sym (IntP.m-n≡m⊖n (ϕ q) (ϕ q))) ⟩
    Int.+ ϕ q Int.+ Int.- (Int.+ ϕ q) Int.+ Int.+ ϕ/-1 l q Int.+ Int.+ op/seq/cost l q ≡⟨ P.cong (λ x → x Int.+ Int.+ op/seq/cost l q) (IntP.+-assoc (Int.+ ϕ q) (Int.- (Int.+ ϕ q)) (Int.+ ϕ/-1 l q)) ⟩
    Int.+ ϕ q Int.+ (Int.- (Int.+ ϕ q) Int.+ Int.+ ϕ/-1 l q) Int.+ Int.+ op/seq/cost l q ≡⟨ P.cong (λ x → Int.+ ϕ q Int.+ x Int.+ Int.+ op/seq/cost l q) (IntP.+-comm (Int.- (Int.+ ϕ q)) (Int.+ ϕ/-1 l q)) ⟩
    Int.+ ϕ q Int.+ (Int.+ ϕ/-1 l q Int.- (Int.+ ϕ q)) Int.+ Int.+ op/seq/cost l q ≡⟨ IntP.+-assoc (Int.+ ϕ q) (Int.+ ϕ/-1 l q Int.- (Int.+ ϕ q)) (Int.+ op/seq/cost l q) ⟩
    Int.+ ϕ q Int.+ (Int.+ ϕ/-1 l q Int.- Int.+ ϕ q Int.+ Int.+ op/seq/cost l q) ≡⟨ P.cong (λ x → Int.+ ϕ q Int.+ (x Int.+ Int.+ op/seq/cost l q)) (IntP.m-n≡m⊖n (ϕ/-1 l q) (ϕ q)) ⟩
    Int.+ ϕ q Int.+ (ϕ/-1 l q Int.⊖ ϕ q Int.+ Int.+ op/seq/cost l q) ≡⟨ P.cong (λ x → Int.+ ϕ q Int.+ x) (P.sym (cost≡cost/tele l q u)) ⟩
    Int.+ ϕ q Int.+ op/seq/cost/tele l q ≤⟨ IntP.+-monoʳ-≤ (Int.+ ϕ q) (amortized≥cost/tele q l l' h) ⟩
    Int.+ ϕ q Int.+ Int.+ lsum l' ≤⟨ IntP.≤-refl ⟩
    Int.+ ϕ q Int.+ Int.+ lsum l'
    ∎
   where open IntP.≤-Reasoning

  -- Amortized cost for enq and deq on a front-back queue
  enq/acost : ∀ x → ◯ (is/acost (op/enq x) 2)
  enq/acost x u (f , b) =
    begin
      (Int.+ (op/cost (op/enq x) (f , b))) Int.+ (((op/enq x) operateϕ (f , b)) Int.⊖ (ϕ (f , b)))
    ≡⟨⟩
      Int.0ℤ Int.+ ((len f + 2 * (1 + len b)) Int.⊖ (ϕ (f , b)))
    ≡⟨ IntP.+-identityˡ ((len f + 2 * (1 + len b)) Int.⊖ (ϕ (f , b))) ⟩
      len f + 2 * (1 + len b) Int.⊖ ϕ (f , b)
    ≡⟨ P.cong (λ x → (len f + x) Int.⊖ (ϕ (f , b))) (*-distribˡ-+ 2 1 (len b)) ⟩
      len f + (2 * 1 + 2 * len b) Int.⊖ ϕ (f , b)
    ≡⟨ P.cong (λ x → (len f + x) Int.⊖ (ϕ (f , b)) ) (+-comm 2 (2 * len b)) ⟩
      len f + (2 * len b + 2) Int.⊖ ϕ (f , b)
    ≡⟨ P.cong (λ x → x Int.⊖ (ϕ (f , b))) (P.sym (+-assoc (len f) (2 * len b) 2)) ⟩
      len f + 2 * len b + 2 Int.⊖ ϕ (f , b)
    ≡⟨ P.cong (λ x → (len f + 2 * len b + 2) Int.⊖ x) (P.sym (+-identityʳ (ϕ (f , b)))) ⟩
      len f + 2 * len b + 2 Int.⊖ (ϕ (f , b) + 0)
    ≡⟨ IntP.+-cancelˡ-⊖ (len f + 2 * len b) 2 0 ⟩
      Int.+ 2
    ∎
    where open IntP.≤-Reasoning

  n+n≡2*n : ∀ n → n + n ≡ 2 * n
  n+n≡2*n n =
    begin
    n + n ≡⟨ P.cong (λ x → n + x) (P.sym (+-identityʳ n)) ⟩
    2 * n ∎
    where open ≡-Reasoning

  deq/acost : ◯ (is/acost op/deq 0)
  deq/acost u (f , b) =
    list/match f (λ f → meta ((Int.+ (op/cost op/deq (f , b))) Int.+ ((op/deq operateϕ (f , b)) Int.⊖ (ϕ (f , b))) Int.≤ Int.0ℤ))
    (
    list/match b (λ b → meta ((Int.+ (op/cost op/deq (nil , b))) Int.+ ((op/deq operateϕ (nil , b)) Int.⊖ (ϕ (nil , b))) Int.≤ Int.0ℤ))
    IntP.≤-refl
    λ a b' →
      begin
        (Int.+ (op/cost op/deq (nil , cons a b'))) Int.+ ((op/deq operateϕ (nil , cons a b')) Int.⊖ (ϕ (nil , cons a b')))
      ≡⟨⟩
        Int.+ (step cost 1 (2 + len b')) Int.+ (step cost 1 (len b') Int.⊖ (2 * (step cost 1 (1 + len b'))))
      ≡⟨
        cong₂ Int._+_
          (cong Int.+_ (step/ext cost (2 + len b') 1 u))
          (cong₂ Int._⊖_
            (step/ext cost (len b') 1 u)
            (cong (2 *_) (step/ext cost (1 + len b') 1 u))
          )
      ⟩
        Int.+ (2 + len b') Int.+ (len b' Int.⊖ (2 * (1 + len b')))
      ≡⟨ IntP.distribʳ-⊖-+-pos (2 + len b') (len b') (2 * (1 + len b')) ⟩
        2 + len b' + len b' Int.⊖ 2 * (1 + len b')
      ≡⟨ P.cong (λ x → x Int.⊖ 2 * (1 + len b')) (+-assoc 2 (len b') (len b')) ⟩
        2 + (len b' + len b') Int.⊖ 2 * (1 + len b')
      ≡⟨ P.cong (λ x → 2 + (len b'  + len b') Int.⊖ x) (*-distribˡ-+ 2 1 (len b')) ⟩
        2 + (len b' + len b') Int.⊖ (2 * 1 + 2 * len b')
      ≡⟨ P.cong (λ x → 2 + x Int.⊖ (2 + 2 * len b')) (n+n≡2*n (len b')) ⟩
        2 + 2 * len b' Int.⊖ (2 + 2 * len b')
      ≡⟨ IntP.n⊖n≡0 (2 + 2 * len b') ⟩
        Int.0ℤ
      ∎
    )
    λ a f' →
      begin
        (Int.+ (op/cost op/deq (cons a f' , b))) Int.+ ((op/deq operateϕ (cons a f' , b)) Int.⊖ (ϕ (cons a f' , b)))
      ≡⟨⟩
        Int.+ (step cost 1 1) Int.+ (step cost 1 (len f' + 2 * len b) Int.⊖ (step cost 1 (1 + len f') + 2 * len b))
      ≡⟨
        cong₂ Int._+_
          (cong Int.+_ (step/ext cost 1 1 u))
          (cong₂ Int._⊖_
            (step/ext cost (len f' + 2 * len b) 1 u)
            (cong (_+ 2 * len b) (step/ext cost (1 + len f') 1 u))
          )
      ⟩
        Int.+ 1 Int.+ ((len f' + 2 * len b) Int.⊖ (1 + len f' + 2 * len b))
      ≡⟨ IntP.distribʳ-⊖-+-pos 1 (len f' + 2 * len b) (1 + len f' + 2 * len b) ⟩
        1 + (len f' + 2 * len b) Int.⊖ (1 + len f' + 2 * len b)
      ≡⟨ P.cong (λ x → x Int.⊖ (1 + len f' + 2 * len b)) (P.sym (+-assoc 1 (len f') (2 * len b))) ⟩
        1 + len f' + 2 * len b Int.⊖ (1 + len f' + 2 * len b)
      ≡⟨ IntP.n⊖n≡0 (1 + len f' + 2 * len b) ⟩
        Int.0ℤ
      ∎
    where open IntP.≤-Reasoning

  all2s : ℕ → List ℕ
  all2s n = tabulate {n = n} (λ _ → 2)

  sum2s : ∀ n → lsum (all2s n) ≡ 2 * n
  sum2s zero = refl
  sum2s (suc n) =
    begin
    2 + lsum (all2s n) ≡⟨ P.cong (λ x → 2 + x) (sum2s n) ⟩
    2 + 2 * n ≡⟨ P.cong (λ x → x + 2 * n) (*-identityʳ 2) ⟩
    2 * 1 + 2 * n ≡⟨ P.sym (*-distribˡ-+ 2 1 n) ⟩
    2 * (1 + n)
    ∎
   where open ≡-Reasoning

  all2s/is/acost : ∀ l → ◯ (Amortized l (all2s (length l)))
  all2s/is/acost [] u = a/emp
  all2s/is/acost ((op/enq x) ∷ os) u = a/cons (op/enq x) 2 os (all2s (length os)) (enq/acost x u) (all2s/is/acost os u)
  all2s/is/acost (op/deq ∷ os) u = a/cons op/deq 2 os (all2s (length os)) (acost/weaken z≤n (deq/acost u)) (all2s/is/acost os u)

  op/seq/cost≤ϕ₀+2*|l| : ∀ q l → ◯ (Int.+ (op/seq/cost l q) Int.≤  Int.+ (ϕ q + 2 * length l))
  op/seq/cost≤ϕ₀+2*|l| q l u =
    begin
    Int.+ (op/seq/cost l q) ≤⟨ amortized≥cost q l (all2s (length l)) (all2s/is/acost l u) u ⟩
    Int.+ (ϕ q + lsum (all2s (length l))) ≡⟨ P.cong (λ x → Int.+ (ϕ q + x)) (sum2s (length l)) ⟩
    Int.+ (ϕ q + 2 * length l) ≤⟨ IntP.≤-refl ⟩
    Int.+ (ϕ q + 2 * length l)
    ∎
   where open IntP.≤-Reasoning

  -- Starting with an empty queue, a sequence of n operations costs at most 2 * n
  op/seq≤2*|l| : ∀ l → IsBounded Q (l op/seq emp) (2 * length l)
  op/seq≤2*|l| l = bound/relax (λ u → IntP.drop‿+≤+ (op/seq/cost≤ϕ₀+2*|l| emp l u)) (op/seq≤op/seq/cost l emp)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Data.Either where

import      Lvl
open import Data.Boolean using (Bool ; 𝑇 ; 𝐹)
open import Functional using (id ; _∘_)
open import Type

infixr 100 _‖_

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Lvl.Level
private variable A B C A₁ A₂ B₁ B₂ : Type{ℓ}

data _‖_ (A : Type{ℓ₁}) (B : Type{ℓ₂}) : Type{ℓ₁ Lvl.⊔ ℓ₂} where
  Left  : A → (A ‖ B)
  Right : B → (A ‖ B)
{-# FOREIGN GHC type AgdaEither ℓ₁ ℓ₂ = Either #-}
{-# COMPILE GHC _‖_ = data AgdaEither (Left | Right) #-}

elim : ∀{P : (A ‖ B) → Type{ℓ}} → ((a : A) → P(Left a)) → ((b : B) → P(Right b)) → ((e : (A ‖ B)) → P(e))
elim fa _ (Left  a) = fa(a)
elim _ fb (Right b) = fb(b)

map1 : let _ = A ; _ = B ; _ = C in (A → C) → (B → C) → (A ‖ B) → C
map1 = elim

swap : (A ‖ B) → (B ‖ A)
swap (Left t) = Right t
swap (Right t) = Left t

extract : (A ‖ A) → A
extract = map1 id id

map : (A₁ → A₂) → (B₁ → B₂) → (A₁ ‖ B₁) → (A₂ ‖ B₂)
map fa fb = map1 (Left ∘ fa) (Right ∘ fb)

mapLeft : let _ = A₁ ; _ = A₂ ; _ = B in (A₁ → A₂) → (A₁ ‖ B) → (A₂ ‖ B)
mapLeft f = map f id

mapRight : let _ = A ; _ = B₁ ; _ = B₂ in (B₁ → B₂) → (A ‖ B₁) → (A ‖ B₂)
mapRight f = map id f

isLeft : (A ‖ B) → Bool
isLeft(Left  _) = 𝑇
isLeft(Right _) = 𝐹

isRight : (A ‖ B) → Bool
isRight(Left  _) = 𝐹
isRight(Right _) = 𝑇

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-

A possible implementation of the following HIT arr. Note that this type is
mutually defined with App, that is to say, they are defined by
induction-recursion!

Inductive arr (A,B:Set) : Set :=
| base : B -> arr A B
| step : (A -> arr A B) -> arr A B.
| path : (forall x : A, App f x = App g x) -> f = g.

where App is defined by

Fixpoint App (f : arr A B)(a : A) :=
match f with
| base b => b
| step g => App (g a) a
end.

Due to the fact that arr and App are defined by induction-recuriosn, the
recursion principle for arr needs to make extra assumptions, see the parameters
of the arr-Rec module.
Effectively, we see the function space A → B as algebra for the functor (-) × A
and App is an algebra homomorphism from arr A B to A → B.
This is reflected in the extra assumption in the recursion principle.

-}

{-# OPTIONS --without-K #-}
open import lib.Basics
open import lib.PathGroupoid
open import lib.types.Paths
open import lib.Funext

module _ where
  private
    data #arr-aux (A B : Set) : Set where
      #base : B → #arr-aux A B
      #step : (A → #arr-aux A B) → #arr-aux A B

    #App : ∀{A B} → #arr-aux A B → A → B
    #App (#base b) a = b
    #App (#step g) a = #App (g a) a

  _~>_ : Set → Set → Set
  _~>_ = #arr-aux

  base : ∀{A B} → B → A ~> B
  base = #base

  step : ∀{A B} → (A → A ~> B) → A ~> B
  step = #step

  App : ∀{A B} → A ~> B → A → B
  App = #App

  Abstr : ∀{A B} → (A → B) → A ~> B
  Abstr f = step (λ x → base (f x))

  postulate
    path : ∀{A B} (f g : A ~> B) (a : A) → App f a == App g a → f == g

  module arr-Rec {A B X : Set}
    (base* : B → X)
    (step* : (A → X) → X)
    (App* : X → A → B)
    -- Here we need to make the assumption that App* is an algebra homomorphism
    -- from X into the function space.
    (App*-β₂ : (a : A) (f : A → X) → App* (step* f) a == App* (f a) a)
    (path* : (x y : X) (a : A) → App* x a == App* y a → x == y)
    where
    rec : A ~> B → X
    rec = rec-aux phantom where
      rec-aux : Phantom path* → A ~> B → X
      rec-aux ph (#base b) = base* b
      rec-aux ph (#step f) = step* (λ a → rec-aux ph (f a))

    lem : (f g : A ~> B) (a : A) →
      App f a == App g a → App* (rec f) a == App* (rec g) a
    lem (#base b) (#base .b) a idp = idp
    lem (#base b) (#step g) a p =
      let β-red* = App*-β₂ a (rec ∘ g)
          IH = lem (#base b) (g a) a p
      in  IH ∙ ! β-red*
    lem (#step f) (#base b) a p =
      let β-red* = App*-β₂ a (rec ∘ f)
          IH = lem (f a) (#base b) a p
      in  β-red* ∙ IH
    lem (#step f) (#step g) a p =
      let IH = lem (f a) (g a) a p
          β-red-f = App*-β₂ a (rec ∘ f)
          β-red-g = App*-β₂ a (rec ∘ g)
      in β-red-f ∙ IH ∙ ! β-red-g

    postulate
      path-β : (f g : A ~> B) (a : A) (p : App f a == App g a) →
               ap rec (path f g a p)
               == path* (rec f) (rec g) a (lem f g a p)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

open import Algebra

module Algebra.Properties.BooleanAlgebra
         {b₁ b₂} (B : BooleanAlgebra b₁ b₂)
         where

open BooleanAlgebra B
import Algebra.Properties.DistributiveLattice
private
  open module DL = Algebra.Properties.DistributiveLattice
                     distributiveLattice public
    hiding (replace-equality)
open import Algebra.Structures
import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Relation.Binary
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Data.Product

------------------------------------------------------------------------
-- Some simple generalisations

∨-complement : Inverse ⊤ ¬_ _∨_
∨-complement = ∨-complementˡ , ∨-complementʳ
  where
  ∨-complementˡ : LeftInverse ⊤ ¬_ _∨_
  ∨-complementˡ x = begin
    ¬ x ∨ x    ≈⟨ ∨-comm _ _ ⟩
    x   ∨ ¬ x  ≈⟨ ∨-complementʳ _ ⟩
    ⊤          ∎

∧-complement : Inverse ⊥ ¬_ _∧_
∧-complement = ∧-complementˡ , ∧-complementʳ
  where
  ∧-complementˡ : LeftInverse ⊥ ¬_ _∧_
  ∧-complementˡ x = begin
    ¬ x ∧ x    ≈⟨ ∧-comm _ _ ⟩
    x   ∧ ¬ x  ≈⟨ ∧-complementʳ _ ⟩
    ⊥          ∎

------------------------------------------------------------------------
-- The dual construction is also a boolean algebra

∧-∨-isBooleanAlgebra : IsBooleanAlgebra _≈_ _∧_ _∨_ ¬_ ⊥ ⊤
∧-∨-isBooleanAlgebra = record
  { isDistributiveLattice = ∧-∨-isDistributiveLattice
  ; ∨-complementʳ         = proj₂ ∧-complement
  ; ∧-complementʳ         = proj₂ ∨-complement
  ; ¬-cong                = ¬-cong
  }

∧-∨-booleanAlgebra : BooleanAlgebra _ _
∧-∨-booleanAlgebra = record
  { _∧_              = _∨_
  ; _∨_              = _∧_
  ; ⊤                = ⊥
  ; ⊥                = ⊤
  ; isBooleanAlgebra = ∧-∨-isBooleanAlgebra
  }

------------------------------------------------------------------------
-- (∨, ∧, ⊥, ⊤) is a commutative semiring

private

  ∧-identity : Identity ⊤ _∧_
  ∧-identity = (λ _ → ∧-comm _ _ ⟨ trans ⟩ x∧⊤=x _) , x∧⊤=x
    where
    x∧⊤=x : ∀ x → x ∧ ⊤ ≈ x
    x∧⊤=x x = begin
      x ∧ ⊤          ≈⟨ refl ⟨ ∧-cong ⟩ sym (proj₂ ∨-complement _) ⟩
      x ∧ (x ∨ ¬ x)  ≈⟨ proj₂ absorptive _ _ ⟩
      x              ∎

  ∨-identity : Identity ⊥ _∨_
  ∨-identity = (λ _ → ∨-comm _ _ ⟨ trans ⟩ x∨⊥=x _) , x∨⊥=x
    where
    x∨⊥=x : ∀ x → x ∨ ⊥ ≈ x
    x∨⊥=x x = begin
      x ∨ ⊥          ≈⟨ refl ⟨ ∨-cong ⟩ sym (proj₂ ∧-complement _) ⟩
      x ∨ x ∧ ¬ x    ≈⟨ proj₁ absorptive _ _ ⟩
      x              ∎

  ∧-zero : Zero ⊥ _∧_
  ∧-zero = (λ _ → ∧-comm _ _ ⟨ trans ⟩ x∧⊥=⊥ _) , x∧⊥=⊥
    where
    x∧⊥=⊥ : ∀ x → x ∧ ⊥ ≈ ⊥
    x∧⊥=⊥ x = begin
      x ∧ ⊥          ≈⟨ refl ⟨ ∧-cong ⟩ sym (proj₂ ∧-complement _) ⟩
      x ∧  x  ∧ ¬ x  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
      (x ∧ x) ∧ ¬ x  ≈⟨ ∧-idempotent _ ⟨ ∧-cong ⟩ refl ⟩
      x       ∧ ¬ x  ≈⟨ proj₂ ∧-complement _ ⟩
      ⊥              ∎

∨-∧-isCommutativeSemiring : IsCommutativeSemiring _≈_ _∨_ _∧_ ⊥ ⊤
∨-∧-isCommutativeSemiring = record
  { +-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = isEquivalence
      ; assoc         = ∨-assoc
      ; ∙-cong        = ∨-cong
      }
    ; identityˡ = proj₁ ∨-identity
    ; comm      = ∨-comm
    }
  ; *-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = isEquivalence
      ; assoc         = ∧-assoc
      ; ∙-cong        = ∧-cong
      }
    ; identityˡ = proj₁ ∧-identity
    ; comm      = ∧-comm
    }
  ; distribʳ = proj₂ ∧-∨-distrib
  ; zeroˡ    = proj₁ ∧-zero
  }

∨-∧-commutativeSemiring : CommutativeSemiring _ _
∨-∧-commutativeSemiring = record
  { _+_                   = _∨_
  ; _*_                   = _∧_
  ; 0#                    = ⊥
  ; 1#                    = ⊤
  ; isCommutativeSemiring = ∨-∧-isCommutativeSemiring
  }

------------------------------------------------------------------------
-- (∧, ∨, ⊤, ⊥) is a commutative semiring

private

  ∨-zero : Zero ⊤ _∨_
  ∨-zero = (λ _ → ∨-comm _ _ ⟨ trans ⟩ x∨⊤=⊤ _) , x∨⊤=⊤
    where
    x∨⊤=⊤ : ∀ x → x ∨ ⊤ ≈ ⊤
    x∨⊤=⊤ x = begin
      x ∨ ⊤          ≈⟨ refl ⟨ ∨-cong ⟩ sym (proj₂ ∨-complement _) ⟩
      x ∨  x  ∨ ¬ x  ≈⟨ sym $ ∨-assoc _ _ _ ⟩
      (x ∨ x) ∨ ¬ x  ≈⟨ ∨-idempotent _ ⟨ ∨-cong ⟩ refl ⟩
      x       ∨ ¬ x  ≈⟨ proj₂ ∨-complement _ ⟩
      ⊤              ∎

∧-∨-isCommutativeSemiring : IsCommutativeSemiring _≈_ _∧_ _∨_ ⊤ ⊥
∧-∨-isCommutativeSemiring = record
  { +-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = isEquivalence
      ; assoc         = ∧-assoc
      ; ∙-cong        = ∧-cong
      }
    ; identityˡ = proj₁ ∧-identity
    ; comm      = ∧-comm
    }
  ; *-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = isEquivalence
      ; assoc         = ∨-assoc
      ; ∙-cong        = ∨-cong
      }
    ; identityˡ = proj₁ ∨-identity
    ; comm      = ∨-comm
    }
  ; distribʳ = proj₂ ∨-∧-distrib
  ; zeroˡ    = proj₁ ∨-zero
  }

∧-∨-commutativeSemiring : CommutativeSemiring _ _
∧-∨-commutativeSemiring =
  record { isCommutativeSemiring = ∧-∨-isCommutativeSemiring }

------------------------------------------------------------------------
-- Some other properties

-- I took the statement of this lemma (called Uniqueness of
-- Complements) from some course notes, "Boolean Algebra", written
-- by Gert Smolka.

private
  lemma : ∀ x y → x ∧ y ≈ ⊥ → x ∨ y ≈ ⊤ → ¬ x ≈ y
  lemma x y x∧y=⊥ x∨y=⊤ = begin
    ¬ x                ≈⟨ sym $ proj₂ ∧-identity _ ⟩
    ¬ x ∧ ⊤            ≈⟨ refl ⟨ ∧-cong ⟩ sym x∨y=⊤ ⟩
    ¬ x ∧ (x ∨ y)      ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩
    ¬ x ∧ x ∨ ¬ x ∧ y  ≈⟨ proj₁ ∧-complement _ ⟨ ∨-cong ⟩ refl ⟩
    ⊥ ∨ ¬ x ∧ y        ≈⟨ sym x∧y=⊥ ⟨ ∨-cong ⟩ refl ⟩
    x ∧ y ∨ ¬ x ∧ y    ≈⟨ sym $ proj₂ ∧-∨-distrib _ _ _ ⟩
    (x ∨ ¬ x) ∧ y      ≈⟨ proj₂ ∨-complement _ ⟨ ∧-cong ⟩ refl ⟩
    ⊤ ∧ y              ≈⟨ proj₁ ∧-identity _ ⟩
    y                  ∎

¬⊥=⊤ : ¬ ⊥ ≈ ⊤
¬⊥=⊤ = lemma ⊥ ⊤ (proj₂ ∧-identity _) (proj₂ ∨-zero _)

¬⊤=⊥ : ¬ ⊤ ≈ ⊥
¬⊤=⊥ = lemma ⊤ ⊥ (proj₂ ∧-zero _) (proj₂ ∨-identity _)

¬-involutive : Involutive ¬_
¬-involutive x = lemma (¬ x) x (proj₁ ∧-complement _) (proj₁ ∨-complement _)

deMorgan₁ : ∀ x y → ¬ (x ∧ y) ≈ ¬ x ∨ ¬ y
deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂
  where
  lem₁ = begin
    (x ∧ y) ∧ (¬ x ∨ ¬ y)          ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩
    (x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ (∧-comm _ _ ⟨ ∧-cong ⟩ refl) ⟨ ∨-cong ⟩ refl ⟩
    (y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ ∧-assoc _ _ _ ⟨ ∨-cong ⟩ ∧-assoc _ _ _ ⟩
    y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y)  ≈⟨ (refl ⟨ ∧-cong ⟩ proj₂ ∧-complement _) ⟨ ∨-cong ⟩
                                      (refl ⟨ ∧-cong ⟩ proj₂ ∧-complement _) ⟩
    (y ∧ ⊥) ∨ (x ∧ ⊥)              ≈⟨ proj₂ ∧-zero _ ⟨ ∨-cong ⟩ proj₂ ∧-zero _ ⟩
    ⊥ ∨ ⊥                          ≈⟨ proj₂ ∨-identity _ ⟩
    ⊥                              ∎

  lem₃ = begin
    (x ∧ y) ∨ ¬ x          ≈⟨ proj₂ ∨-∧-distrib _ _ _ ⟩
    (x ∨ ¬ x) ∧ (y ∨ ¬ x)  ≈⟨ proj₂ ∨-complement _ ⟨ ∧-cong ⟩ refl ⟩
    ⊤ ∧ (y ∨ ¬ x)          ≈⟨ proj₁ ∧-identity _ ⟩
    y ∨ ¬ x                ≈⟨ ∨-comm _ _ ⟩
    ¬ x ∨ y                ∎

  lem₂ = begin
    (x ∧ y) ∨ (¬ x ∨ ¬ y)  ≈⟨ sym $ ∨-assoc _ _ _ ⟩
    ((x ∧ y) ∨ ¬ x) ∨ ¬ y  ≈⟨ lem₃ ⟨ ∨-cong ⟩ refl ⟩
    (¬ x ∨ y) ∨ ¬ y        ≈⟨ ∨-assoc _ _ _ ⟩
    ¬ x ∨ (y ∨ ¬ y)        ≈⟨ refl ⟨ ∨-cong ⟩ proj₂ ∨-complement _ ⟩
    ¬ x ∨ ⊤                ≈⟨ proj₂ ∨-zero _ ⟩
    ⊤                      ∎

deMorgan₂ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y
deMorgan₂ x y = begin
  ¬ (x ∨ y)          ≈⟨ ¬-cong $ sym (¬-involutive _) ⟨ ∨-cong ⟩
                                 sym (¬-involutive _) ⟩
  ¬ (¬ ¬ x ∨ ¬ ¬ y)  ≈⟨ ¬-cong $ sym $ deMorgan₁ _ _ ⟩
  ¬ ¬ (¬ x ∧ ¬ y)    ≈⟨ ¬-involutive _ ⟩
  ¬ x ∧ ¬ y          ∎

-- One can replace the underlying equality with an equivalent one.

replace-equality :
  {_≈′_ : Rel Carrier b₂} →
  (∀ {x y} → x ≈ y ⇔ x ≈′ y) → BooleanAlgebra _ _
replace-equality {_≈′_} ≈⇔≈′ = record
  { _≈_              = _≈′_
  ; _∨_              = _∨_
  ; _∧_              = _∧_
  ; ¬_               = ¬_
  ; ⊤                = ⊤
  ; ⊥                = ⊥
  ; isBooleanAlgebra =  record
    { isDistributiveLattice = DistributiveLattice.isDistributiveLattice
                                (DL.replace-equality ≈⇔≈′)
    ; ∨-complementʳ         = λ x → to ⟨$⟩ ∨-complementʳ x
    ; ∧-complementʳ         = λ x → to ⟨$⟩ ∧-complementʳ x
    ; ¬-cong                = λ i≈j → to ⟨$⟩ ¬-cong (from ⟨$⟩ i≈j)
    }
  } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})

------------------------------------------------------------------------
-- (⊕, ∧, id, ⊥, ⊤) is a commutative ring

-- This construction is parameterised over the definition of xor.

module XorRing
  (xor : Op₂ Carrier)
  (⊕-def : ∀ x y → xor x y ≈ (x ∨ y) ∧ ¬ (x ∧ y))
  where

  private
    infixl 6 _⊕_

    _⊕_ : Op₂ Carrier
    _⊕_ = xor

  private
    helper : ∀ {x y u v} → x ≈ y → u ≈ v → x ∧ ¬ u ≈ y ∧ ¬ v
    helper x≈y u≈v = x≈y ⟨ ∧-cong ⟩ ¬-cong u≈v

  ⊕-¬-distribˡ : ∀ x y → ¬ (x ⊕ y) ≈ ¬ x ⊕ y
  ⊕-¬-distribˡ x y = begin
    ¬ (x ⊕ y)                              ≈⟨ ¬-cong $ ⊕-def _ _ ⟩
    ¬ ((x ∨ y) ∧ (¬ (x ∧ y)))              ≈⟨ ¬-cong (proj₂ ∧-∨-distrib _ _ _) ⟩
    ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y)))  ≈⟨ ¬-cong $
                                                refl ⟨ ∨-cong ⟩
                                                  (refl ⟨ ∧-cong ⟩
                                                     ¬-cong (∧-comm _ _)) ⟩
    ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x)))  ≈⟨ ¬-cong $ lem _ _ ⟨ ∨-cong ⟩ lem _ _ ⟩
    ¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x))              ≈⟨ deMorgan₂ _ _ ⟩
    ¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x)              ≈⟨ deMorgan₁ _ _ ⟨ ∧-cong ⟩ refl ⟩
    (¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x)          ≈⟨ helper (refl ⟨ ∨-cong ⟩ ¬-involutive _)
                                                     (∧-comm _ _) ⟩
    (¬ x ∨ y) ∧ ¬ (¬ x ∧ y)                ≈⟨ sym $ ⊕-def _ _ ⟩
    ¬ x ⊕ y                                ∎
    where
    lem : ∀ x y → x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y
    lem x y = begin
      x ∧ ¬ (x ∧ y)          ≈⟨ refl ⟨ ∧-cong ⟩ deMorgan₁ _ _ ⟩
      x ∧ (¬ x ∨ ¬ y)        ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩
      (x ∧ ¬ x) ∨ (x ∧ ¬ y)  ≈⟨ proj₂ ∧-complement _ ⟨ ∨-cong ⟩ refl ⟩
      ⊥ ∨ (x ∧ ¬ y)          ≈⟨ proj₁ ∨-identity _ ⟩
      x ∧ ¬ y                ∎

  private
    ⊕-comm : Commutative _⊕_
    ⊕-comm x y = begin
      x ⊕ y                ≈⟨ ⊕-def _ _ ⟩
      (x ∨ y) ∧ ¬ (x ∧ y)  ≈⟨ helper (∨-comm _ _) (∧-comm _ _) ⟩
      (y ∨ x) ∧ ¬ (y ∧ x)  ≈⟨ sym $ ⊕-def _ _ ⟩
      y ⊕ x                ∎

  ⊕-¬-distribʳ : ∀ x y → ¬ (x ⊕ y) ≈ x ⊕ ¬ y
  ⊕-¬-distribʳ x y = begin
    ¬ (x ⊕ y)  ≈⟨ ¬-cong $ ⊕-comm _ _ ⟩
    ¬ (y ⊕ x)  ≈⟨ ⊕-¬-distribˡ _ _ ⟩
    ¬ y ⊕ x    ≈⟨ ⊕-comm _ _ ⟩
    x ⊕ ¬ y    ∎

  ⊕-annihilates-¬ : ∀ x y → x ⊕ y ≈ ¬ x ⊕ ¬ y
  ⊕-annihilates-¬ x y = begin
    x ⊕ y        ≈⟨ sym $ ¬-involutive _ ⟩
    ¬ ¬ (x ⊕ y)  ≈⟨ ¬-cong $ ⊕-¬-distribˡ _ _ ⟩
    ¬ (¬ x ⊕ y)  ≈⟨ ⊕-¬-distribʳ _ _ ⟩
    ¬ x ⊕ ¬ y    ∎

  private
    ⊕-cong : _⊕_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
    ⊕-cong {x} {y} {u} {v} x≈y u≈v = begin
      x ⊕ u                ≈⟨ ⊕-def _ _ ⟩
      (x ∨ u) ∧ ¬ (x ∧ u)  ≈⟨ helper (x≈y ⟨ ∨-cong ⟩ u≈v)
                                     (x≈y ⟨ ∧-cong ⟩ u≈v) ⟩
      (y ∨ v) ∧ ¬ (y ∧ v)  ≈⟨ sym $ ⊕-def _ _ ⟩
      y ⊕ v                ∎

    ⊕-identity : Identity ⊥ _⊕_
    ⊕-identity = ⊥⊕x=x , (λ _ → ⊕-comm _ _ ⟨ trans ⟩ ⊥⊕x=x _)
      where
      ⊥⊕x=x : ∀ x → ⊥ ⊕ x ≈ x
      ⊥⊕x=x x = begin
        ⊥ ⊕ x                ≈⟨ ⊕-def _ _ ⟩
        (⊥ ∨ x) ∧ ¬ (⊥ ∧ x)  ≈⟨ helper (proj₁ ∨-identity _)
                                       (proj₁ ∧-zero _) ⟩
        x ∧ ¬ ⊥              ≈⟨ refl ⟨ ∧-cong ⟩ ¬⊥=⊤ ⟩
        x ∧ ⊤                ≈⟨ proj₂ ∧-identity _ ⟩
        x                    ∎

    ⊕-inverse : Inverse ⊥ id _⊕_
    ⊕-inverse = x⊕x=⊥ , (λ _ → ⊕-comm _ _ ⟨ trans ⟩ x⊕x=⊥ _)
      where
      x⊕x=⊥ : ∀ x → x ⊕ x ≈ ⊥
      x⊕x=⊥ x = begin
        x ⊕ x                ≈⟨ ⊕-def _ _ ⟩
        (x ∨ x) ∧ ¬ (x ∧ x)  ≈⟨ helper (∨-idempotent _)
                                       (∧-idempotent _) ⟩
        x ∧ ¬ x              ≈⟨ proj₂ ∧-complement _ ⟩
        ⊥                    ∎

    distrib-∧-⊕ : _∧_ DistributesOver _⊕_
    distrib-∧-⊕ = distˡ , distʳ
      where
      distˡ : _∧_ DistributesOverˡ _⊕_
      distˡ x y z = begin
        x ∧ (y ⊕ z)                ≈⟨ refl ⟨ ∧-cong ⟩ ⊕-def _ _ ⟩
        x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
        (x ∧ (y ∨ z)) ∧ ¬ (y ∧ z)  ≈⟨ refl ⟨ ∧-cong ⟩ deMorgan₁ _ _ ⟩
        (x ∧ (y ∨ z)) ∧
        (¬ y ∨ ¬ z)                ≈⟨ sym $ proj₁ ∨-identity _ ⟩
        ⊥ ∨
        ((x ∧ (y ∨ z)) ∧
         (¬ y ∨ ¬ z))              ≈⟨ lem₃ ⟨ ∨-cong ⟩ refl ⟩
        ((x ∧ (y ∨ z)) ∧ ¬ x) ∨
        ((x ∧ (y ∨ z)) ∧
         (¬ y ∨ ¬ z))              ≈⟨ sym $ proj₁ ∧-∨-distrib _ _ _ ⟩
        (x ∧ (y ∨ z)) ∧
        (¬ x ∨ (¬ y ∨ ¬ z))        ≈⟨  refl ⟨ ∧-cong ⟩
                                      (refl ⟨ ∨-cong ⟩ sym (deMorgan₁ _ _)) ⟩
        (x ∧ (y ∨ z)) ∧
        (¬ x ∨ ¬ (y ∧ z))          ≈⟨ refl ⟨ ∧-cong ⟩ sym (deMorgan₁ _ _) ⟩
          (x ∧ (y ∨ z)) ∧
        ¬ (x ∧ (y ∧ z))            ≈⟨ helper refl lem₁ ⟩
          (x ∧ (y ∨ z)) ∧
        ¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟨ ∧-cong ⟩
                                      refl ⟩
          ((x ∧ y) ∨ (x ∧ z)) ∧
        ¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ sym $ ⊕-def _ _ ⟩
        (x ∧ y) ⊕ (x ∧ z)          ∎
        where
        lem₂ = begin
          x ∧ (y ∧ z)  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
          (x ∧ y) ∧ z  ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl ⟩
          (y ∧ x) ∧ z  ≈⟨ ∧-assoc _ _ _ ⟩
          y ∧ (x ∧ z)  ∎

        lem₁ = begin
          x ∧ (y ∧ z)        ≈⟨ sym (∧-idempotent _) ⟨ ∧-cong ⟩ refl ⟩
          (x ∧ x) ∧ (y ∧ z)  ≈⟨ ∧-assoc _ _ _ ⟩
          x ∧ (x ∧ (y ∧ z))  ≈⟨ refl ⟨ ∧-cong ⟩ lem₂ ⟩
          x ∧ (y ∧ (x ∧ z))  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
          (x ∧ y) ∧ (x ∧ z)  ∎

        lem₃ = begin
          ⊥                      ≈⟨ sym $ proj₂ ∧-zero _ ⟩
          (y ∨ z) ∧ ⊥            ≈⟨ refl ⟨ ∧-cong ⟩ sym (proj₂ ∧-complement _) ⟩
          (y ∨ z) ∧ (x ∧ ¬ x)    ≈⟨ sym $ ∧-assoc _ _ _ ⟩
          ((y ∨ z) ∧ x) ∧ ¬ x    ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl  ⟩
          (x ∧ (y ∨ z)) ∧ ¬ x    ∎

      distʳ : _∧_ DistributesOverʳ _⊕_
      distʳ x y z = begin
        (y ⊕ z) ∧ x        ≈⟨ ∧-comm _ _ ⟩
        x ∧ (y ⊕ z)        ≈⟨ distˡ _ _ _ ⟩
        (x ∧ y) ⊕ (x ∧ z)  ≈⟨ ∧-comm _ _ ⟨ ⊕-cong ⟩ ∧-comm _ _ ⟩
        (y ∧ x) ⊕ (z ∧ x)  ∎

    lemma₂ : ∀ x y u v →
             (x ∧ y) ∨ (u ∧ v) ≈
             ((x ∨ u) ∧ (y ∨ u)) ∧
             ((x ∨ v) ∧ (y ∨ v))
    lemma₂ x y u v = begin
        (x ∧ y) ∨ (u ∧ v)              ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩
        ((x ∧ y) ∨ u) ∧ ((x ∧ y) ∨ v)  ≈⟨ proj₂ ∨-∧-distrib _ _ _
                                            ⟨ ∧-cong ⟩
                                          proj₂ ∨-∧-distrib _ _ _ ⟩
        ((x ∨ u) ∧ (y ∨ u)) ∧
        ((x ∨ v) ∧ (y ∨ v))            ∎

    ⊕-assoc : Associative _⊕_
    ⊕-assoc x y z = sym $ begin
      x ⊕ (y ⊕ z)                                ≈⟨ refl ⟨ ⊕-cong ⟩ ⊕-def _ _ ⟩
      x ⊕ ((y ∨ z) ∧ ¬ (y ∧ z))                  ≈⟨ ⊕-def _ _ ⟩
        (x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))) ∧
      ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))              ≈⟨ lem₃ ⟨ ∧-cong ⟩ lem₄ ⟩
      (((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
      (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ ∧-assoc _ _ _ ⟩
      ((x ∨ y) ∨ z) ∧
      (((x ∨ ¬ y) ∨ ¬ z) ∧
       (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈⟨ refl ⟨ ∧-cong ⟩ lem₅ ⟩
      ((x ∨ y) ∨ z) ∧
      (((¬ x ∨ ¬ y) ∨ z) ∧
       (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
      (((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
      (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ lem₁ ⟨ ∧-cong ⟩ lem₂ ⟩
        (((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z) ∧
      ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)              ≈⟨ sym $ ⊕-def _ _ ⟩
      ((x ∨ y) ∧ ¬ (x ∧ y)) ⊕ z                  ≈⟨ sym $ ⊕-def _ _ ⟨ ⊕-cong ⟩ refl ⟩
      (x ⊕ y) ⊕ z                                ∎
      where
      lem₁ = begin
        ((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)  ≈⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩
        ((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z        ≈⟨ (refl ⟨ ∧-cong ⟩ sym (deMorgan₁ _ _))
                                                    ⟨ ∨-cong ⟩ refl ⟩
        ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z          ∎

      lem₂' = begin
        (x ∨ ¬ y) ∧ (¬ x ∨ y)              ≈⟨ sym $
                                                proj₁ ∧-identity _
                                                  ⟨ ∧-cong ⟩
                                                proj₂ ∧-identity _ ⟩
        (⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤)  ≈⟨ sym $
                                                (proj₁ ∨-complement _ ⟨ ∧-cong ⟩ ∨-comm _ _)
                                                  ⟨ ∧-cong ⟩
                                                (refl ⟨ ∧-cong ⟩ proj₁ ∨-complement _) ⟩
        ((¬ x ∨ x) ∧ (¬ y ∨ x)) ∧
        ((¬ x ∨ y) ∧ (¬ y ∨ y))            ≈⟨ sym $ lemma₂ _ _ _ _ ⟩
        (¬ x ∧ ¬ y) ∨ (x ∧ y)              ≈⟨ sym $ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
        ¬ (x ∨ y) ∨ ¬ ¬ (x ∧ y)            ≈⟨ sym (deMorgan₁ _ _) ⟩
        ¬ ((x ∨ y) ∧ ¬ (x ∧ y))            ∎

      lem₂ = begin
        ((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)  ≈⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩
        ((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z          ≈⟨ lem₂' ⟨ ∨-cong ⟩ refl ⟩
        ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z          ≈⟨ sym $ deMorgan₁ _ _ ⟩
        ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)          ∎

      lem₃ = begin
        x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))          ≈⟨ refl ⟨ ∨-cong ⟩
                                                (refl ⟨ ∧-cong ⟩ deMorgan₁ _ _) ⟩
        x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z))        ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩
        (x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z))  ≈⟨ sym (∨-assoc _ _ _) ⟨ ∧-cong ⟩
                                              sym (∨-assoc _ _ _) ⟩
        ((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)  ∎

      lem₄' = begin
        ¬ ((y ∨ z) ∧ ¬ (y ∧ z))    ≈⟨ deMorgan₁ _ _ ⟩
        ¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z)    ≈⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
        (¬ y ∧ ¬ z) ∨ (y ∧ z)      ≈⟨ lemma₂ _ _ _ _ ⟩
        ((¬ y ∨ y) ∧ (¬ z ∨ y)) ∧
        ((¬ y ∨ z) ∧ (¬ z ∨ z))    ≈⟨ (proj₁ ∨-complement _ ⟨ ∧-cong ⟩ ∨-comm _ _)
                                        ⟨ ∧-cong ⟩
                                      (refl ⟨ ∧-cong ⟩ proj₁ ∨-complement _) ⟩
        (⊤ ∧ (y ∨ ¬ z)) ∧
        ((¬ y ∨ z) ∧ ⊤)            ≈⟨ proj₁ ∧-identity _ ⟨ ∧-cong ⟩
                                      proj₂ ∧-identity _ ⟩
        (y ∨ ¬ z) ∧ (¬ y ∨ z)      ∎

      lem₄ = begin
        ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))  ≈⟨ deMorgan₁ _ _ ⟩
        ¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ refl ⟨ ∨-cong ⟩ lem₄' ⟩
        ¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z))  ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩
        (¬ x ∨ (y     ∨ ¬ z)) ∧
        (¬ x ∨ (¬ y ∨ z))              ≈⟨ sym (∨-assoc _ _ _) ⟨ ∧-cong ⟩
                                          sym (∨-assoc _ _ _) ⟩
        ((¬ x ∨ y)     ∨ ¬ z) ∧
        ((¬ x ∨ ¬ y) ∨ z)              ≈⟨ ∧-comm _ _ ⟩
        ((¬ x ∨ ¬ y) ∨ z) ∧
        ((¬ x ∨ y)     ∨ ¬ z)          ∎

      lem₅ = begin
        ((x ∨ ¬ y) ∨ ¬ z) ∧
        (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ sym $ ∧-assoc _ _ _ ⟩
        (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
        ((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl ⟩
        (((¬ x ∨ ¬ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
        ((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-assoc _ _ _ ⟩
        ((¬ x ∨ ¬ y) ∨ z) ∧
        (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ∎

  isCommutativeRing : IsCommutativeRing _≈_ _⊕_ _∧_ id ⊥ ⊤
  isCommutativeRing = record
    { isRing = record
      { +-isAbelianGroup = record
        { isGroup = record
          { isMonoid = record
            { isSemigroup = record
              { isEquivalence = isEquivalence
              ; assoc         = ⊕-assoc
              ; ∙-cong        = ⊕-cong
              }
            ; identity = ⊕-identity
            }
          ; inverse   = ⊕-inverse
          ; ⁻¹-cong   = id
          }
        ; comm = ⊕-comm
        }
      ; *-isMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc         = ∧-assoc
          ; ∙-cong        = ∧-cong
          }
        ; identity = ∧-identity
        }
      ; distrib = distrib-∧-⊕
      }
    ; *-comm = ∧-comm
    }

  commutativeRing : CommutativeRing _ _
  commutativeRing = record
    { _+_               = _⊕_
    ; _*_               = _∧_
    ; -_                = id
    ; 0#                = ⊥
    ; 1#                = ⊤
    ; isCommutativeRing = isCommutativeRing
    }

infixl 6 _⊕_

_⊕_ : Op₂ Carrier
x ⊕ y = (x ∨ y) ∧ ¬ (x ∧ y)

module DefaultXorRing = XorRing _⊕_ (λ _ _ → refl)


text:
{-# OPTIONS --universe-polymorphism #-}

-- Should fail with S i != i
module Issue216 where

postulate
  Level : Set
  O : Level
  S : Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO O #-}
{-# BUILTIN LEVELSUC  S #-}

Foo : {i : Level} → Set i
Foo {i} = (R : Set i) → R

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Nullary using (¬_; Dec; yes; no)

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

¬s≤z : ∀ {m : ℕ} → ¬ (suc m ≤ zero)
¬s≤z ()

¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
¬s≤s ¬m≤n (s≤s m≤n) = ¬m≤n m≤n

_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
zero ≤? n = yes z≤n
suc m ≤? zero = no ¬s≤z
suc m ≤? suc n with m ≤? n
... | yes m≤n = yes (s≤s m≤n)
... | no ¬m≤n = no (¬s≤s ¬m≤n)

_ : 2 ≤? 4 ≡ yes (s≤s (s≤s z≤n))
_ = refl

_ : 4 ≤? 2 ≡ no (¬s≤s (¬s≤s ¬s≤z))
_ = refl


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

module Examples where

data _∨_ (A B : Set) : Set where
  inl : A → A ∨ B
  inr : B → A ∨ B

postulate commOr : {A B : Set} → A ∨ B → B ∨ A
{-# ATP prove commOr #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
_ : Set₁
_ = Set

_ : Set₁
_ = Set

module _ where

  _ : Set₁
  _ = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Coinductive "natural" numbers
------------------------------------------------------------------------

module Data.Conat where

open import Coinduction
open import Data.Nat using (ℕ; zero; suc)

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

data Coℕ : Set where
  zero : Coℕ
  suc  : (n : ∞ Coℕ) → Coℕ

------------------------------------------------------------------------
-- Some operations

fromℕ : ℕ → Coℕ
fromℕ zero    = zero
fromℕ (suc n) = suc (♯ fromℕ n)

∞ℕ : Coℕ
∞ℕ = suc (♯ ∞ℕ)

infixl 6 _+_

_+_ : Coℕ → Coℕ → Coℕ
zero  + n = n
suc m + n = suc (♯ (♭ m + n))

max_issues_repo_name: larrytheliquid/Lemmachine


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

module Definition.Typed.Consequences.Equality where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Fundamental.Reducibility
open import Definition.Typed.Consequences.Injectivity

open import Tools.Product
import Tools.PropositionalEquality as PE

{-

-- conversion is cumulative

typeCumul′ : ∀ {A rA lA lA' Γ} → lA ≤∞ lA' →  Γ ⊩⟨ ∞ ⟩ A ^ [ rA , lA ] → Γ ⊩⟨ ∞ ⟩ A ^ [ rA , lA' ]
typeCumul′ (≡is≤∞ PE.refl) [A] = [A]
typeCumul′ (<∞is≤∞ emb<) (Uᵣ (Uᵣ r l′ l<₁ eq d)) = emb ∞< (Uᵣ (Uᵣ r ⁰ emb< PE.refl {!!}))
typeCumul′ (<∞is≤∞ ∞<) (Uᵣ (Uᵣ r l′ l<₁ eq d)) = Uᵣ (Uᵣ r ¹ ∞< PE.refl {!!})
typeCumul′ (<∞is≤∞ emb<) (ℕᵣ [[ ⊢A , ⊢B , D ]]) = emb ∞< (emb emb< {!ℕᵣ ?!})
typeCumul′ (<∞is≤∞ l<) (Emptyᵣ x) = {!!}
typeCumul′ (<∞is≤∞ l<) (ne x) = {!!}
typeCumul′ (<∞is≤∞ l<) (Πᵣ x) = {!!}
typeCumul′ (<∞is≤∞ l<) (∃ᵣ x) = {!!}
typeCumul′ (<∞is≤∞ l<) (emb l<₁ [A]) = {!!}

convCumul′ : ∀ {A B rA lA lA' Γ} → (l< : lA ≤∞ lA') → ([A] : Γ ⊩⟨ ∞ ⟩ A ^ [ rA , lA ])
             → Γ ⊩⟨ ∞ ⟩ A ≡ B ^ [ rA , lA ] / [A] → Γ ⊩⟨ ∞ ⟩ A ≡ B ^ [ rA , lA' ] / typeCumul′ l< [A]
convCumul′ (<∞is≤∞ l<) [A] [A≡B] = {!!}
convCumul′ (≡is≤∞ PE.refl) [A] [A≡B] = [A≡B]

convCumul : ∀ {A B rA lA lA' Γ} → lA ≤∞ lA' → Γ ⊢ A ≡ B ^ [ rA , lA ] → Γ ⊢ A ≡ B ^ [ rA , lA' ]
convCumul {A} {B} {rA} {lA} {lA'} {Γ} (<∞is≤∞ l<) A≡B =
  let X = reducibleEq A≡B
      [A] = proj₁ X
      [B] = proj₁ (proj₂ X)
      [A≡B] = proj₂ (proj₂ X)
      [A]' : Γ ⊩⟨ ∞ ⟩ A ^ [ rA , lA' ]
      [A]' = emb l< {!!} -- [A]
  in {!escapeEq [A]' [A≡B]!}
-- convCumul (<∞is≤∞ ∞<) A≡B =
--   let X = reducibleEq A≡B
--       [A] = proj₁ X
--       [B] = proj₁ (proj₂ X)
--       [A≡B] = proj₂ (proj₂ X)
--   in {!!}
convCumul (≡is≤∞ PE.refl) A≡B = A≡B
-}

U≡A′ : ∀ {A rU Γ l lU nlU } ([U] : Γ ⊩⟨ l ⟩U Univ rU lU ^ nlU)
    → Γ ⊩⟨ l ⟩ Univ rU lU ≡ A ^ [ ! , nlU ] / (U-intr [U])
    → Γ ⊢ A ⇒* Univ rU lU ^ [ ! , nlU ]
U≡A′ (noemb (Uᵣ r l′ l< eq d)) [U≡A] =
 let r≡r , l≡l  = Uinjectivity (subset* (red d))
 in PE.subst (λ r → _ ⊢ _ ⇒* Univ r _ ^ [ ! , _ ]) (PE.sym r≡r)
         (PE.subst (λ l → _ ⊢ _ ⇒* Univ _ l ^ [ ! , _ ]) (PE.sym l≡l) [U≡A])
U≡A′ (emb emb< [U]) [U≡A] = U≡A′ [U] [U≡A]
U≡A′ (emb ∞< [U]) [U≡A] = U≡A′ [U] [U≡A]

-- If A is judgmentally equal to U, then A reduces to U.
U≡A : ∀ {A rU Γ lU nlU }
    → Γ ⊢ Univ rU lU ≡ A ^ [ ! , nlU ]
    → Γ ⊢ A ⇒* Univ rU lU ^ [ ! , nlU ]
U≡A {A} U≡A =
  let X = reducibleEq U≡A
      [U] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [U≡A] = proj₂ (proj₂ X)
  in U≡A′ (U-elim [U]) (irrelevanceEq [U] (U-intr (U-elim [U])) [U≡A])

-- If A is judgmentally equal to U, then A reduces to U.
U≡A-whnf : ∀ {A rU Γ lU nlU }
    → Γ ⊢ Univ rU lU ≡ A ^ [ ! , nlU ]
    → Whnf A
    → A PE.≡ Univ rU lU
U≡A-whnf {A} X whnfA = whnfRed* (U≡A X) whnfA

ℕ≡A′ : ∀ {A Γ l} ([ℕ] : Γ ⊩⟨ l ⟩ℕ ℕ)
    → Γ ⊩⟨ l ⟩ ℕ ≡ A ^ [ ! , ι ⁰ ] / (ℕ-intr [ℕ])
    → Whnf A
    → A PE.≡ ℕ
ℕ≡A′ (noemb x) [ℕ≡A] whnfA = whnfRed* [ℕ≡A] whnfA
ℕ≡A′ (emb emb< [ℕ]) [ℕ≡A] whnfA = ℕ≡A′ [ℕ] [ℕ≡A] whnfA
ℕ≡A′ (emb ∞< [ℕ]) [ℕ≡A] whnfA = ℕ≡A′ [ℕ] [ℕ≡A] whnfA

-- If A in WHNF is judgmentally equal to ℕ, then A is propsitionally equal to ℕ.
ℕ≡A : ∀ {A Γ}
    → Γ ⊢ ℕ ≡ A ^ [ ! , ι ⁰ ]
    → Whnf A
    → A PE.≡ ℕ
ℕ≡A {A} ℕ≡A whnfA =
  let X = reducibleEq ℕ≡A
      [ℕ] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [ℕ≡A] = proj₂ (proj₂ X)
  in ℕ≡A′ (ℕ-elim [ℕ]) (irrelevanceEq [ℕ] (ℕ-intr (ℕ-elim [ℕ])) [ℕ≡A]) whnfA

-- If A in WHNF is judgmentally equal to Empty, then A is propositionally equal to Empty.
Empty≡A′ : ∀ {A Γ l ll} ([Empty] : Γ ⊩⟨ l ⟩Empty Empty ll ^ ll)
    → Γ ⊩⟨ l ⟩ Empty ll ≡ A ^ [ % , ι ll ] / (Empty-intr [Empty])
    → Whnf A
    → A PE.≡ Empty ll
Empty≡A′ (noemb x) [Empty≡A] whnfA = whnfRed* [Empty≡A] whnfA
Empty≡A′ (emb emb< [Empty]) [Empty≡A] whnfA = Empty≡A′ [Empty] [Empty≡A] whnfA
Empty≡A′ (emb ∞< [Empty]) [Empty≡A] whnfA = Empty≡A′ [Empty] [Empty≡A] whnfA

Empty≡A : ∀ {A Γ l}
    → Γ ⊢ Empty l ≡ A ^ [ % , ι l ]
    → Whnf A
    → A PE.≡ Empty l
Empty≡A {A} Empty≡A whnfA =
  let X = reducibleEq Empty≡A
      [Empty] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [Empty≡A] = proj₂ (proj₂ X)
  in Empty≡A′ (Empty-elim [Empty]) (irrelevanceEq [Empty] (Empty-intr (Empty-elim [Empty])) [Empty≡A]) whnfA

ne≡A′ : ∀ {A K r Γ l ll }
     → ([K] : Γ ⊩⟨ l ⟩ne K ^[ r , ll ] )
     → Γ ⊩⟨ l ⟩ K ≡ A ^ [ r , ι ll ] / (ne-intr [K])
     → Whnf A
     → ∃ λ M → Neutral M × A PE.≡ M
ne≡A′ (noemb [K]) (ne₌ M D′ neM K≡M) whnfA =
  M , neM , (whnfRed* (red D′) whnfA)
ne≡A′ (emb emb< [K]) [K≡A] whnfA = ne≡A′ [K] [K≡A] whnfA
ne≡A′ (emb ∞< [K]) [K≡A] whnfA = ne≡A′ [K] [K≡A] whnfA

-- If A in WHNF is judgmentally equal to K, then there exists a M such that
-- A is propsitionally equal to M.
ne≡A : ∀ {A K r l Γ}
    → Neutral K
    → Γ ⊢ K ≡ A ^ [ r , ι l ]
    → Whnf A
    → ∃ λ M → Neutral M × A PE.≡ M
ne≡A {A} neK ne≡A whnfA =
  let X = reducibleEq ne≡A
      [ne] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [ne≡A] = proj₂ (proj₂ X)
  in ne≡A′ (ne-elim neK [ne])
        (irrelevanceEq [ne] (ne-intr (ne-elim neK [ne])) [ne≡A]) whnfA

Π≡A′ : ∀ {A F G rF lF lG rΠ lΠ Γ l} ([Π] : Γ ⊩⟨ l ⟩Π Π F ^ rF ° lF ▹ G ° lG ° lΠ ^[ rΠ , lΠ ] )
    → Γ ⊩⟨ l ⟩ Π F ^ rF ° lF ▹ G ° lG ° lΠ ≡ A ^ [ rΠ ,  ι lΠ ] / (Π-intr [Π])
    → Whnf A
    → ∃₂ λ H E → A PE.≡ Π H ^ rF ° lF ▹ E ° lG ° lΠ
Π≡A′ (noemb (Πᵣ rF′ lF′ lG′ lF≤ lG≤  F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) whnfA =
    let _ , rF≡rF′ , lF≡lF′ , _ , lG≡lG′ , _ = Π-PE-injectivity (whnfRed* (red D) Πₙ)
        X = whnfRed* D′ whnfA
    in F′ , G′ ,
       PE.subst (λ r → _ PE.≡ Π _ ^ r ° _ ▹ _ ° _ ° _) (PE.sym rF≡rF′)
         (PE.subst (λ l → _ PE.≡ Π _ ^ _ ° l ▹ _ ° _ ° _) (PE.sym lF≡lF′)
           (PE.subst (λ l → _ PE.≡ Π _ ^ _ ° _ ▹ _ ° l ° _) (PE.sym lG≡lG′) X))
Π≡A′ (emb emb< [Π]) [Π≡A] whnfA = Π≡A′ [Π] [Π≡A] whnfA
Π≡A′ (emb ∞< [Π]) [Π≡A] whnfA = Π≡A′ [Π] [Π≡A] whnfA

-- If A is judgmentally equal to Π F ▹ G, then there exists H and E such that
-- A is propositionally equal to Π H ▹ E.
Π≡A : ∀ {A F G rF lF lG rΠ lΠ Γ}
    → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ≡ A ^ [ rΠ ,  ι lΠ ]
    → Whnf A
    → ∃₂ λ H E → A PE.≡ Π H ^ rF ° lF ▹ E ° lG ° lΠ
Π≡A {A} Π≡A whnfA  =
  let X = reducibleEq Π≡A
      [Π] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [Π≡A] = proj₂ (proj₂ X)
  in Π≡A′ (Π-elim [Π]) (irrelevanceEq [Π] (Π-intr (Π-elim [Π])) [Π≡A]) whnfA

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

module function.isomorphism.utils where

open import sum
open import equality.core
open import equality.calculus
open import function.core
open import function.overloading
open import function.isomorphism.core
open import function.isomorphism.coherent
open import function.extensionality.proof
open import sets.unit
open import sets.empty
open import sets.fin.core
open import hott.level.core

Σ-split-iso : ∀ {i j}{X : Set i}{Y : X → Set j}
            → {a a' : X}{b : Y a}{b' : Y a'}
            → (Σ (a ≡ a') λ q → subst Y q b ≡ b')
            ≅ ((a , b) ≡ (a' , b'))
Σ-split-iso {Y = Y}{a}{a'}{b}{b'} = iso unapΣ apΣ H K
  where
    H : ∀ {a a'}{b : Y a}{b' : Y a'}
      → (p : Σ (a ≡ a') λ q → subst Y q b ≡ b')
      → apΣ (unapΣ {a = a}{a' = a'}{b = b}{b' = b'} p) ≡ p
    H (refl , refl) = refl

    K : (p : (a , b) ≡ (a' , b')) → unapΣ (apΣ p) ≡ p
    K = J (λ u v p → unapΣ (apΣ p) ≡ p)
          (λ {(a , b) → refl })
          (a , b) (a' , b')

×-split-iso : ∀ {i j}{X : Set i}{Y : Set j}
            → {a a' : X}{b b' : Y}
            → ((a ≡ a') × (b ≡ b'))
            ≅ ((a , b) ≡ (a' , b'))
×-split-iso {X = X}{Y} = record
  { to = λ { (p , q) → ap₂ _,_ p q }
  ; from = λ { p → (ap proj₁ p , ap proj₂ p) }
  ; iso₁ = λ { (p , q) → H p q }
  ; iso₂ = K }
  where
    H : {a a' : X}{b b' : Y}(p : a ≡ a')(q : b ≡ b')
      → (ap proj₁ (ap₂ _,_ p q), ap proj₂ (ap₂ _,_ p q)) ≡ (p , q)
    H refl refl = refl

    K : {a a' : X}{b b' : Y}(p : (a , b) ≡ (a' , b'))
      → ap₂ _,_ (ap proj₁ p) (ap proj₂ p) ≡ p
    K refl = refl

×-ap-iso : ∀ {i i' j j'}{X : Set i}{X' : Set i'}
             {Y : Set j}{Y' : Set j'}
           → (isom : X ≅ X')
           → (isom' : Y ≅ Y')
           → (X × Y) ≅ (X' × Y')
×-ap-iso isom isom' = record
  { to = λ { (x , y) → (apply isom x , apply isom' y) }
  ; from = λ { (x' , y') → (invert isom x' , invert isom' y') }
  ; iso₁ = λ { (x , y) → pair≡ (_≅_.iso₁ isom x) (_≅_.iso₁ isom' y) }
  ; iso₂ = λ { (x' , y') → pair≡ (_≅_.iso₂ isom x') (_≅_.iso₂ isom' y') } }

Σ-ap-iso₂ : ∀ {i j j'}{X : Set i}
          → {Y : X → Set j}{Y' : X → Set j'}
          → ((x : X) → Y x ≅ Y' x)
          → Σ X Y ≅ Σ X Y'
Σ-ap-iso₂ {X = X}{Y}{Y'} isom = record
  { to = λ { (x , y) → (x , apply (isom x) y) }
  ; from = λ { (x , y') → (x , invert (isom x) y') }
  ; iso₁ = λ { (x , y) → unapΣ (refl , _≅_.iso₁ (isom x) y) }
  ; iso₂ = λ { (x , y') → unapΣ (refl , _≅_.iso₂ (isom x) y') } }

Σ-ap-iso₁ : ∀ {i i' j}{X : Set i}{X' : Set i'}{Y : X' → Set j}
          → (isom : X ≅ X')
          → Σ X (Y ∘ apply isom) ≅ Σ X' Y
Σ-ap-iso₁ {X = X}{X'}{Y} isom = record
  { to = λ { (x , y) → (f x , y) }
  ; from = λ { (x , y) → (g x , subst Y (sym (K x)) y) }
  ; iso₁ = λ { (x , y) → unapΣ (H x ,
           subst-naturality Y f (H x) _
         · (subst-hom Y (sym (K (f x))) (ap f (H x)) y
         · ap (λ p → subst Y p y) (lem x) ) ) }
  ; iso₂ = λ { (x , y) → unapΣ (K x ,
           subst-hom Y (sym (K x)) (K x) y
         · ap (λ p → subst Y p y) (right-inverse (K x)) ) } }
  where
    isom-c = ≅⇒≅' isom
    γ = proj₂ isom-c
    open _≅_ (proj₁ isom-c)
      renaming ( to to f ; from to g
               ; iso₁ to H; iso₂ to K )

    lem : (x : X) → sym (K (f x)) · ap f (H x) ≡ refl
    lem x = ap (λ z → sym (K (f x)) · z) (γ x)
          · right-inverse (K (f x))

Σ-ap-iso : ∀ {i i' j j'}{X : Set i}{X' : Set i'}
           {Y : X → Set j}{Y' : X' → Set j'}
         → (isom : X ≅ X')
         → ((x : X) → Y x ≅ Y' (apply isom x))
         → Σ X Y ≅ Σ X' Y'
Σ-ap-iso {X = X}{X'}{Y}{Y'} isom isom' = trans≅
  (Σ-ap-iso₂ isom') (Σ-ap-iso₁ isom)

Σ-ap-iso' : ∀ {i i' j j'}{X : Set i}{X' : Set i'}
            {Y : X → Set j}{Y' : X' → Set j'}
          → (isom : X ≅ X')
          → ((x : X') → Y (invert isom x) ≅ Y' x)
          → Σ X Y ≅ Σ X' Y'
Σ-ap-iso' {X = X}{X'}{Y}{Y'} isom isom'
  = sym≅ (Σ-ap-iso (sym≅ isom) (λ x → sym≅ (isom' x)))

Π-ap-iso : ∀ {i i' j j'}{X : Set i}{X' : Set i'}
             {Y : X → Set j}{Y' : X' → Set j'}
           → (isom : X ≅ X')
           → ((x' : X') → Y (invert isom x') ≅ Y' x')
           → ((x : X) → Y x)
           ≅ ((x' : X') → Y' x')
Π-ap-iso {X = X}{X'}{Y}{Y'} isom isom' =
  trans≅ (Π-iso (≅⇒≅' isom)) (Π-iso' isom')
  where
    Π-iso : (isom : X ≅' X')
          → ((x : X) → Y x)
          ≅ ((x' : X') → Y (invert (proj₁ isom) x'))
    Π-iso (iso f g H K , γ) = record
      { to = λ h x' → h (g x')
      ; from = λ h' x → subst Y (H x) (h' (f x))
      ; iso₁ = λ h → funext λ x → ap' h (H x)
      ; iso₂ = λ h' → funext λ x' →
              ap (λ p → subst Y p _) (sym (γ' x'))
            · sym (subst-naturality Y g (K x') _)
            · ap' h' (K x') }
      where γ' = co-coherence (iso f g H K) γ

    Π-iso' : ∀ {i j j'}{X : Set i}
             {Y : X → Set j}{Y' : X → Set j'}
           → ((x : X) → Y x ≅ Y' x)
           → ((x : X) → Y x)
           ≅ ((x : X) → Y' x)
    Π-iso' isom = record
      { to = λ h x → apply (isom x) (h x)
      ; from = λ h' x → invert (isom x) (h' x)
      ; iso₁ = λ h → funext λ x → _≅_.iso₁ (isom x) _
      ; iso₂ = λ h' → funext λ x → _≅_.iso₂ (isom x) _ }

ΠΣ-swap-iso : ∀ {i j k}{X : Set i}{Y : X → Set j}
            → {Z : (x : X) → Y x → Set k}
            → ((x : X) → Σ (Y x) λ y → Z x y)
            ≅ (Σ ((x : X) → Y x) λ f → ((x : X) → Z x (f x)))
ΠΣ-swap-iso = record
  { to = λ f → (proj₁ ∘' f , proj₂ ∘' f)
  ; from = λ { (f , g) x → (f x , g x) }
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

curry-iso : ∀ {i j k}{X : Set i}{Y : X → Set j}
            (Z : (x : X) → Y x → Set k)
          → ((xy : Σ X Y) → Z (proj₁ xy) (proj₂ xy))
          ≅ ((x : X) → (y : Y x) → Z x y)
curry-iso _ = record
  { to = λ f x y → f (x , y)
  ; from = λ { f (x , y) → f x y }
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

Π-comm-iso : ∀ {i j k}{X : Set i}{Y : Set j}{Z : X → Y → Set k}
           → ((x : X)(y : Y) → Z x y)
           ≅ ((y : Y)(x : X) → Z x y)
Π-comm-iso = record
  { to = λ f y x → f x y
  ; from = λ f x y → f y x
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

Σ-comm-iso : ∀ {i j k}{X : Set i}{Y : Set j}{Z : X → Y → Set k}
           → (Σ X λ x → Σ Y λ y → Z x y)
           ≅ (Σ Y λ y → Σ X λ x → Z x y)
Σ-comm-iso = record
  { to = λ { (x , y , z) → (y , x , z) }
  ; from = λ { (y , x , z) → (x , y , z) }
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

impl-iso : ∀ {i j}{X : Set i}{Y : X → Set j}
         → ((x : X) → Y x) ≅ ({x : X} → Y x)
impl-iso = record
  { to = λ f → f _
  ; from = λ f _ → f
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

Σ-assoc-iso : ∀ {i j k}
              {X : Set i}{Y : X → Set j}
              {Z : (x : X) → Y x → Set k}
            → Σ (Σ X Y) (λ {(x , y) → Z x y})
            ≅ Σ X λ x → Σ (Y x) (Z x)
Σ-assoc-iso = record
  { to = λ {((x , y) , z) → (x , y , z) }
  ; from = λ {(x , y , z) → ((x , y) , z) }
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

⊎-Σ-iso : ∀ {i}(X : Fin 2 → Set i)
        → (X zero ⊎ X (suc zero))
        ≅ Σ (Fin 2) X
⊎-Σ-iso X = record
  { to = λ { (inj₁ x) → zero , x
           ; (inj₂ x) → suc zero , x }
  ; from = λ { (zero , x) → inj₁ x
             ; (suc zero , x) → inj₂ x
             ; (suc (suc ()) , _) }
  ; iso₁ = λ { (inj₁ x) → refl
             ; (inj₂ x) → refl }
  ; iso₂ = λ { (zero , x) → refl
             ; (suc zero , x) → refl
             ; (suc (suc ()) , _) } }

⊎-ap-iso : ∀ {i j i' j'}
         → {X : Set i}{X' : Set i'}
         → {Y : Set j}{Y' : Set j'}
         → X ≅ X'
         → Y ≅ Y'
         → (X ⊎ Y) ≅ (X' ⊎ Y')
⊎-ap-iso (iso f g α β) (iso f' g' α' β') = record
  { to = λ { (inj₁ x) → inj₁ (f x) ; (inj₂ y) → inj₂ (f' y) }
  ; from = λ { (inj₁ x) → inj₁ (g x) ; (inj₂ y) → inj₂ (g' y) }
  ; iso₁ = λ { (inj₁ x) → ap inj₁ (α x) ; (inj₂ y) → ap inj₂ (α' y) }
  ; iso₂ = λ { (inj₁ x) → ap inj₁ (β x) ; (inj₂ y) → ap inj₂ (β' y) } }

⊎-assoc-iso : ∀ {i j k}
            → {X : Set i}{Y : Set j}{Z : Set k}
            → ((X ⊎ Y) ⊎ Z)
            ≅ (X ⊎ (Y ⊎ Z))
⊎-assoc-iso = record
  { to = λ { (inj₁ (inj₁ x)) → inj₁ x
           ; (inj₁ (inj₂ y)) → inj₂ (inj₁ y)
           ; (inj₂ z) → inj₂ (inj₂ z) }
  ; from = λ { (inj₁ x) → inj₁ (inj₁ x)
             ; (inj₂ (inj₁ y)) → inj₁ (inj₂ y)
             ; (inj₂ (inj₂ z)) → inj₂ z }
  ; iso₁ = λ { (inj₁ (inj₁ x)) → refl
             ; (inj₁ (inj₂ y)) → refl
             ; (inj₂ z) → refl }
  ; iso₂ = λ { (inj₁ x) → refl
             ; (inj₂ (inj₁ y)) → refl
             ; (inj₂ (inj₂ z)) → refl } }

⊎×-distr-iso : ∀ {i j k}
             → {X : Set i}{Y : Set j}{Z : Set k}
             → ((X ⊎ Y) × Z)
             ≅ ((X × Z) ⊎ (Y × Z))
⊎×-distr-iso = record
  { to = λ { (inj₁ x , z) → inj₁ (x , z)
           ; (inj₂ y , z) → inj₂ (y , z) }
  ; from = λ { (inj₁ (x , z)) → inj₁ x , z
             ; (inj₂ (y , z)) → inj₂ y , z }
  ; iso₁ = λ { (inj₁ x , z) → refl
             ; (inj₂ y , z) → refl }
  ; iso₂ = λ { (inj₁ (x , z)) → refl
             ; (inj₂ (y , z)) → refl } }

⊎-universal : ∀ {i j k}{X : Set i}{Y : Set j}
            → {Z : X ⊎ Y → Set k}
            → ((u : X ⊎ Y) → Z u)
            ≅ (((x : X) → Z (inj₁ x)) × ((y : Y) → Z (inj₂ y)))
⊎-universal = record
  { to = λ f → (f ∘' inj₁ , f ∘' inj₂)
  ; from = λ { (g₁ , g₂) (inj₁ x) → g₁ x
             ; (g₁ , g₂) (inj₂ y) → g₂ y }
  ; iso₁ = λ f → funext λ
      { (inj₁ x) → refl
      ; (inj₂ x) → refl }
  ; iso₂ = λ { (g₁ , g₂) → refl } }

×-left-unit : ∀ {i}{X : Set i} → (⊤ × X) ≅ X
×-left-unit = record
  { to = λ {(tt , x) → x }
  ; from = λ x → tt , x
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

×-right-unit : ∀ {i}{X : Set i} → (X × ⊤) ≅ X
×-right-unit = record
  { to = λ {(x , tt) → x }
  ; from = λ x → x , tt
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

contr-⊤-iso : ∀ {i}{X : Set i}
            → contr X → X ≅ ⊤
contr-⊤-iso hX = record
  { to = λ x → tt
  ; from = λ { tt → proj₁ hX }
  ; iso₁ = λ x → proj₂ hX x
  ; iso₂ = λ { tt → refl } }

empty-⊥-iso : ∀ {i}{X : Set i}
            → (X → ⊥) → X ≅ ⊥
empty-⊥-iso u = record
  { to = u
  ; from = ⊥-elim
  ; iso₁ = λ x → ⊥-elim (u x)
  ; iso₂ = λ () }

×-comm : ∀ {i j}{X : Set i}{Y : Set j}
       → (X × Y) ≅ (Y × X)
×-comm = record
  { to = λ {(x , y) → (y , x)}
  ; from = λ {(y , x) → (x , y)}
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

Π-left-unit : ∀ {i}{X : Set i}
            → (⊤ → X) ≅ X
Π-left-unit = record
  { to = λ f → f tt
  ; from = λ x _ → x
  ; iso₁ = λ _ → refl
  ; iso₂ = λ f → refl }

-- rewriting lemmas for equations on equalities
sym≡-iso : ∀ {i}{X : Set i}(x y : X)
         → (x ≡ y)
         ≅ (y ≡ x)
sym≡-iso _ _ = iso sym sym double-inverse double-inverse

trans≡-iso : ∀ {i}{X : Set i}{x y z : X}
           → (x ≡ y)
           → (y ≡ z) ≅ (x ≡ z)
trans≡-iso p = record
  { to = λ q → p · q
  ; from = λ q → sym p · q
  ; iso₁ = λ q → sym (associativity (sym p) p q)
                · ap (λ z → z · q) (right-inverse p)
  ; iso₂ = λ q → sym (associativity p (sym p) q)
                · ap (λ z → z · q) (left-inverse p) }

trans≡-iso' : ∀ {i}{X : Set i}{x y z : X}
            → (y ≡ z)
            → (x ≡ y) ≅ (x ≡ z)
trans≡-iso' q = record
  { to = λ p → p · q
  ; from = λ p → p · sym q
  ; iso₁ = λ p → associativity p q (sym q)
               · ap (_·_ p) (left-inverse q)
               · left-unit p
  ; iso₂ = λ p → associativity p (sym q) q
               · (ap (_·_ p) (right-inverse q)
               · left-unit p) }

move-≡-iso : ∀ {i}{X : Set i}{x y z : X}
           → (p : x ≡ y)(q : y ≡ z)(r : x ≡ z)
           → (p · q ≡ r)
           ≅ (sym p · r ≡ q)
move-≡-iso refl = sym≡-iso

J-iso : ∀ {i j}{X : Set i}{x : X}
      → {P : (y : X) → x ≡ y → Set j}
      → P x refl
      ≅ ((y : X)(p : x ≡ y) → P y p)
J-iso {X = X}{x}{P} = record
  { to = J' P
  ; from = λ u → u x refl
  ; iso₁ = λ _ → refl
  ; iso₂ = λ u → funext λ y → funext λ p → β u y p }
  where
    β : (u : (y : X)(p : x ≡ y) → P y p)
      → (y : X)(p : x ≡ y)
      → J' P (u x refl) y p ≡ u y p
    β u .x refl = refl

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Basic Kripke-style semantics with abstract worlds, for soundness only.
-- Ono-style conditions.

module BasicIS4.Semantics.BasicKripkeOno where

open import BasicIS4.Syntax.Common public

-- Intuitionistic modal Kripke models, with frame conditions given by Ono.

record Model : Set₁ where
  infix 3 _⊩ᵅ_
  field
    World : Set

    -- Intuitionistic accessibility; preorder.
    _≤_    : World → World → Set
    refl≤  : ∀ {w} → w ≤ w
    trans≤ : ∀ {w w′ w″} → w ≤ w′ → w′ ≤ w″ → w ≤ w″

    -- Modal accessibility; preorder.
    _R_    : World → World → Set
    reflR  : ∀ {w} → w R w
    transR : ∀ {w w′ w″} → w R w′ → w′ R w″ → w R w″

    -- Forcing for atomic propositions; monotonic.
    _⊩ᵅ_   : World → Atom → Set
    mono⊩ᵅ : ∀ {P w w′} → w ≤ w′ → w ⊩ᵅ P → w′ ⊩ᵅ P

  -- Composition of accessibility.

  _≤⨾R_ : World → World → Set
  _≤⨾R_ = _≤_ ⨾ _R_

  _R⨾≤_ : World → World → Set
  _R⨾≤_ = _R_ ⨾ _≤_

  -- Persistence condition.
  --
  --   w′      v′  →           v′
  --   ◌───R───●   →           ●
  --   │           →         ╱
  --   ≤  ξ,ζ      →       R
  --   │           →     ╱
  --   ●           →   ●
  --   w           →   w

  field
    ≤⨾R→R : ∀ {v′ w} → w ≤⨾R v′ → w R v′

  -- Minor persistence condition.
  --
  --   w′      v′  →           v′
  --   ◌───R───●   →           ●
  --   │           →           │
  --   ≤  ξ,ζ      →           ≤
  --   │           →           │
  --   ●           →   ●───R───◌
  --   w           →   w       v
  --
  --                   w″  →                   w″
  --                   ●   →                   ●
  --                   │   →                   │
  --             ξ′,ζ′ ≤   →                   │
  --                   │   →                   │
  --           ●───R───◌   →                   ≤
  --           │       v′  →                   │
  --      ξ,ζ  ≤           →                   │
  --           │           →                   │
  --   ●───R───◌           →   ●───────R───────◌
  --   w       v           →   w               v″

  ≤⨾R→R⨾≤ : ∀ {v′ w} → w ≤⨾R v′ → w R⨾≤ v′
  ≤⨾R→R⨾≤ {v′} ξ,ζ = v′ , (≤⨾R→R ξ,ζ , refl≤)

  reflR⨾≤ : ∀ {w} → w R⨾≤ w
  reflR⨾≤ {w} = w , (reflR , refl≤)

  transR⨾≤ : ∀ {w′ w w″} → w R⨾≤ w′ → w′ R⨾≤ w″ → w R⨾≤ w″
  transR⨾≤ {w′} (v , (ζ , ξ)) (v′ , (ζ′ , ξ′)) = let v″ , (ζ″ , ξ″) = ≤⨾R→R⨾≤ (w′ , (ξ , ζ′))
                                                 in  v″ , (transR ζ ζ″ , trans≤ ξ″ ξ′)

  ≤→R : ∀ {v′ w} → w ≤ v′ → w R v′
  ≤→R {v′} ξ = ≤⨾R→R (v′ , (ξ , reflR))

open Model {{…}} public

-- Forcing in a particular world of a particular model.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : World → Ty → Set
  w ⊩ α P   = w ⊩ᵅ P
  w ⊩ A ▻ B = ∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B
  w ⊩ □ A   = ∀ {v′} → w R v′ → v′ ⊩ A
  w ⊩ A ∧ B = w ⊩ A × w ⊩ B
  w ⊩ ⊤    = 𝟙

  infix 3 _⊩⋆_
  _⊩⋆_ : World → Cx Ty → Set
  w ⊩⋆ ∅     = 𝟙
  w ⊩⋆ Ξ , A = w ⊩⋆ Ξ × w ⊩ A

-- Monotonicity with respect to intuitionistic accessibility.

module _ {{_ : Model}} where
  mono⊩ : ∀ {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
  mono⊩ {α P}   ξ s = mono⊩ᵅ ξ s
  mono⊩ {A ▻ B} ξ s = λ ξ′ a → s (trans≤ ξ ξ′) a
  mono⊩ {□ A}   ξ s = λ ζ → s (transR (≤→R ξ) ζ)
  mono⊩ {A ∧ B} ξ s = mono⊩ {A} ξ (π₁ s) , mono⊩ {B} ξ (π₂ s)
  mono⊩ {⊤}    ξ s = ∙

  mono⊩⋆ : ∀ {Γ w w′} → w ≤ w′ → w ⊩⋆ Γ → w′ ⊩⋆ Γ
  mono⊩⋆ {∅}     ξ ∙       = ∙
  mono⊩⋆ {Γ , A} ξ (γ , a) = mono⊩⋆ {Γ} ξ γ , mono⊩ {A} ξ a

-- Additional useful equipment.

module _ {{_ : Model}} where
  _⟪$⟫_ : ∀ {A B w} → w ⊩ A ▻ B → w ⊩ A → w ⊩ B
  s ⟪$⟫ a = s refl≤ a

  ⟪K⟫ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A
  ⟪K⟫ {A} a ξ = K (mono⊩ {A} ξ a)

  ⟪S⟫ : ∀ {A B C w} → w ⊩ A ▻ B ▻ C → w ⊩ A ▻ B → w ⊩ A → w ⊩ C
  ⟪S⟫ {A} {B} {C} s₁ s₂ a = _⟪$⟫_ {B} {C} (_⟪$⟫_ {A} {B ▻ C} s₁ a) (_⟪$⟫_ {A} {B} s₂ a)

  ⟪S⟫′ : ∀ {A B C w} → w ⊩ A ▻ B ▻ C → w ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ {A} {B} {C} s₁ ξ s₂ ξ′ a = let s₁′ = mono⊩ {A ▻ B ▻ C} (trans≤ ξ ξ′) s₁
                                      s₂′ = mono⊩ {A ▻ B} ξ′ s₂
                                  in  ⟪S⟫ {A} {B} {C} s₁′ s₂′ a

  _⟪D⟫_ : ∀ {A B w} → w ⊩ □ (A ▻ B) → w ⊩ □ A → w ⊩ □ B
  _⟪D⟫_ {A} {B} s₁ s₂ ζ = let s₁′ = s₁ ζ
                              s₂′ = s₂ ζ
                          in  _⟪$⟫_ {A} {B} s₁′ s₂′

  _⟪D⟫′_ : ∀ {A B w} → w ⊩ □ (A ▻ B) → w ⊩ □ A ▻ □ B
  _⟪D⟫′_ {A} {B} s₁ ξ = _⟪D⟫_ {A} {B} (mono⊩ {□ (A ▻ B)} ξ s₁)

  ⟪↑⟫ : ∀ {A w} → w ⊩ □ A → w ⊩ □ □ A
  ⟪↑⟫ s ζ ζ′ = s (transR ζ ζ′)

  ⟪↓⟫ : ∀ {A w} → w ⊩ □ A → w ⊩ A
  ⟪↓⟫ s = s reflR

  _⟪,⟫′_ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A ∧ B
  _⟪,⟫′_ {A} {B} a ξ = _,_ (mono⊩ {A} ξ a)

-- Forcing in a particular world of a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 _⊩_⇒_
  _⊩_⇒_ : World → Cx Ty → Ty → Set
  w ⊩ Γ ⇒ A = w ⊩⋆ Γ → w ⊩ A

  infix 3 _⊩_⇒⋆_
  _⊩_⇒⋆_ : World → Cx Ty → Cx Ty → Set
  w ⊩ Γ ⇒⋆ Ξ = w ⊩⋆ Γ → w ⊩⋆ Ξ

-- Entailment, or forcing in all worlds of all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx Ty → Ty → Set₁
Γ ⊨ A = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒ A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty → Cx Ty → Set₁
Γ ⊨⋆ Ξ = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒⋆ Ξ

infix 3 _⁏_⊨_
_⁏_⊨_ : Cx Ty → Cx Ty → Ty → Set₁
Γ ⁏ Δ ⊨ A = ∀ {{_ : Model}} {w : World}
             → w ⊩⋆ Γ → (∀ {v′} → w R v′ → v′ ⊩⋆ Δ) → w ⊩ A

-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩ Γ ⇒ A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Dec ( n : ℕ ) where

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

open import Data.PropFormula.Syntax n

open import Data.Bool.Base using  ( Bool; false; true; not; T )
open import Data.Fin       using  ( Fin; suc; zero )
open import Data.Empty     hiding (⊥)

open import Function       using  ( _$_; _∘_ )
open import Relation.Binary.PropositionalEquality using ( _≡_; refl; cong )

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

data ⊥₂ : Set where

⊥₂-elim : ∀ {Whatever : Set} → ⊥₂ → Whatever
⊥₂-elim ()

infix 3 ¬₂_

¬₂_ : Set → Set
¬₂ P = P → ⊥₂

-- Decidable relations.

data Dec (P : Set) : Set where
  yes : ( p :    P) → Dec P
  no  : (¬p : ¬₂ P) → Dec P

⌊_⌋ : {P : Set} → Dec P → Bool
⌊ yes _ ⌋ = true
⌊ no  _ ⌋ = false

REL : Set → Set → Set₁
REL A B = A → B → Set

Decidable : {A : Set} {B : Set} → REL A B → Set
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
postulate
  A : Set

variable
  {xx} : A

record R : Set₁ where
  field
    P : A → Set
    a : P xx
    b : P xx
    c : P xx
    d : P xx
    e : P xx
    f : P xx
    g : P xx
    h : P xx
    i : P xx
    j : P xx
    k : P xx
    l : P xx
    m : P xx
    n : P xx
    o : P xx
    p : P xx
    q : P xx
    r : P xx
    s : P xx
    t : P xx
    u : P xx
    v : P xx
    w : P xx
    x : P xx
    y : P xx
    z : P xx


text:
module BBSTree  {A : Set}(_≤_ : A → A → Set) where

open import Bound.Total A
open import Bound.Total.Order _≤_
open import Data.List
open import List.Order.Simple _≤_

data BBSTree : Bound → Bound → Set where
  bslf : {b t : Bound}
                   → LeB b t
                   → BBSTree b t
  bsnd : {x : A}{b t : Bound}
                   → LeB b (val x)
                   → LeB (val x) t
                   → BBSTree b (val x)
                   → BBSTree (val x) t
                   → BBSTree b t

flatten : {b t : Bound} → BBSTree b t → List A
flatten (bslf _) = []
flatten (bsnd {x = x} b≤x x≤t l r) = flatten l ++ (x ∷ flatten r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
open import Prelude
open import core
open import contexts
open import weakening

module typed-expansion where
  mutual
    typed-expansion-synth : ∀{Φ Γ p e τ} →
                                      Φ , Γ ⊢ p ~~> e ⇒ τ →
                                      Γ ⊢ e => τ
    typed-expansion-synth SPEConst = SConst
    typed-expansion-synth (SPEAsc x) = SAsc (typed-expansion-ana x)
    typed-expansion-synth (SPEVar x₁) = SVar x₁
    typed-expansion-synth (SPELam x₁ D) = SLam x₁ (typed-expansion-synth D)
    typed-expansion-synth (SPEAp D1 x D2 x₂) = SAp x₂ (typed-expansion-synth D1) x (typed-expansion-ana D2)
    typed-expansion-synth SPEHole = SEHole
    typed-expansion-synth (SPNEHole x D) = SNEHole x (typed-expansion-synth D)
    typed-expansion-synth (SPEApLivelit hd fr x x₁ x₂ x₃ x₄ x₅) = SAp (HDAsc hd) (SAsc (weaken-ana-closed fr x₅)) MAArr (typed-expansion-ana x₄)
    typed-expansion-synth (SPEFst h x) = SFst (typed-expansion-synth h) x
    typed-expansion-synth (SPESnd h x) = SSnd (typed-expansion-synth h) x
    typed-expansion-synth (SPEPair h h₁ x) = SPair x (typed-expansion-synth h) (typed-expansion-synth h₁)

    typed-expansion-ana : ∀{Φ Γ p e τ} →
                                  Φ , Γ ⊢ p ~~> e ⇐ τ →
                                  Γ ⊢ e <= τ
    typed-expansion-ana (APELam x₁ x₂ D) = ALam x₁ x₂ (typed-expansion-ana D)
    typed-expansion-ana (APESubsume h ch) = ASubsume (typed-expansion-synth h) ch

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


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

open import Categories.Category using (Category; module Commutation)

-- Defines the induced Monoidal structure of a Cartesian Category

module Categories.Category.Cartesian.Monoidal {o ℓ e} {𝒞 : Category o ℓ e} where

open Category 𝒞
open HomReasoning

open import Categories.Category.BinaryProducts 𝒞 using (BinaryProducts; module BinaryProducts)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Object.Terminal 𝒞 using (Terminal)
open import Categories.Object.Product.Core 𝒞 using (module Product)
open import Categories.Morphism 𝒞 using (_≅_; module ≅)
open import Categories.Morphism.Reasoning 𝒞 using (cancelˡ; pullʳ; pullˡ)
open import Categories.Category.Monoidal using (Monoidal)

open import Categories.Functor using (Functor) renaming (id to idF)
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

private
  variable
    A B C D W X Y Z : Obj
    f f′ g g′ h i : A ⇒ B

-- The cartesian structure induces a monoidal one: 𝒞 is cartesian monoidal.

module CartesianMonoidal (cartesian : Cartesian 𝒞) where
  open Commutation 𝒞
  open Terminal (Cartesian.terminal cartesian)  using (⊤; !; !-unique; !-unique₂)
  open BinaryProducts (Cartesian.products cartesian) using (π₁; π₂; ⟨_,_⟩; _×_; _⁂_;
    _×-; -×_; ⟨⟩∘; ⟨⟩-cong₂; -×-; ×-assoc; assocˡ∘⁂; assocʳ∘⁂; ⁂∘⟨⟩;
    first∘⟨⟩; second∘⟨⟩; ⟨⟩-congˡ; ⟨⟩-congʳ; π₁∘⁂; π₂∘⁂; assocˡ∘⟨⟩;
    assocˡ; assocʳ;
    η; unique; project₁; project₂)

  ⊤×A≅A : ⊤ × A ≅ A
  ⊤×A≅A = record
    { from = π₂
    ; to   = ⟨ ! , id ⟩
    ; iso  = record
      { isoˡ = begin
        ⟨ ! , id ⟩ ∘ π₂ ≈˘⟨ unique !-unique₂ (cancelˡ project₂) ⟩
        ⟨ π₁ , π₂ ⟩     ≈⟨ η ⟩
        id              ∎
      ; isoʳ = project₂
      }
    }

  A×⊤≅A : A × ⊤ ≅ A
  A×⊤≅A = record
    { from = π₁
    ; to   = ⟨ id , ! ⟩
    ; iso  = record
      { isoˡ = begin
        ⟨ id , ! ⟩ ∘ π₁ ≈˘⟨ unique (cancelˡ project₁) !-unique₂ ⟩
        ⟨ π₁ , π₂ ⟩     ≈⟨ η ⟩
        id              ∎
      ; isoʳ = project₁
      }
    }

  ⊤×--id : NaturalIsomorphism (⊤ ×-) idF
  ⊤×--id = record
    { F⇒G = ntHelper record
      { η       = λ _ → π₂
      ; commute = λ _ → project₂
      }
    ; F⇐G = ntHelper record
      { η       = λ _ → ⟨ ! , id ⟩
      ; commute = λ f → begin
        ⟨ ! , id ⟩ ∘ f                                     ≈⟨ ⟨⟩∘ ⟩
        ⟨ ! ∘ f , id  ∘ f ⟩                                ≈⟨ ⟨⟩-cong₂ (⟺ (!-unique _)) identityˡ ⟩
        ⟨ ! , f ⟩                                          ≈˘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩
        ⟨ id ∘ ! , f ∘ id ⟩                                ≈˘⟨ ⟨⟩-cong₂ (pullʳ project₁) (pullʳ project₂) ⟩
        ⟨ (id ∘ π₁) ∘ ⟨ ! , id ⟩ , (f ∘ π₂) ∘ ⟨ ! , id ⟩ ⟩ ≈˘⟨ ⟨⟩∘ ⟩
        ⟨ id ∘ π₁ , f ∘ π₂ ⟩ ∘ ⟨ ! , id ⟩                  ∎
      }
    ; iso = λ _ → _≅_.iso ⊤×A≅A
    }

  -×⊤-id : NaturalIsomorphism (-× ⊤) idF
  -×⊤-id = record
    { F⇒G = ntHelper record
      { η       = λ _ → π₁
      ; commute = λ _ → project₁
      }
    ; F⇐G = ntHelper record
      { η       = λ _ → ⟨ id , ! ⟩
      ; commute = λ f → begin
        ⟨ id , ! ⟩ ∘ f                                     ≈⟨ ⟨⟩∘ ⟩
        ⟨ id ∘ f , ! ∘ f ⟩                                 ≈⟨ ⟨⟩-cong₂ identityˡ (⟺ (!-unique _)) ⟩
        ⟨ f , ! ⟩                                          ≈˘⟨ ⟨⟩-cong₂ identityʳ identityˡ ⟩
        ⟨ f ∘ id , id ∘ ! ⟩                                ≈˘⟨ ⟨⟩-cong₂ (pullʳ project₁) (pullʳ project₂) ⟩
        ⟨ (f ∘ π₁) ∘ ⟨ id , ! ⟩ , (id ∘ π₂) ∘ ⟨ id , ! ⟩ ⟩ ≈˘⟨ ⟨⟩∘ ⟩
        ⟨ f ∘ π₁ , id ∘ π₂ ⟩ ∘ ⟨ id , ! ⟩                  ∎
      }
    ; iso = λ _ → _≅_.iso A×⊤≅A
    }
  private
    infixr 7 _⊗₀_
    infixr 8 _⊗₁_

    _⊗₀_ = _×_
    _⊗₁_ = _⁂_
    α⇒   = assocˡ

  private
   pentagon :  [ ((X ⊗₀ Y) ⊗₀ Z) ⊗₀ W ⇒ X ⊗₀ Y ⊗₀ Z ⊗₀ W ]⟨
                 α⇒ ⊗₁ id         ⇒⟨ (X ⊗₀ Y ⊗₀ Z) ⊗₀ W ⟩
                 α⇒               ⇒⟨ X ⊗₀ (Y ⊗₀ Z) ⊗₀ W ⟩
                 id ⊗₁ α⇒
               ≈ α⇒               ⇒⟨ (X ⊗₀ Y) ⊗₀ Z ⊗₀ W ⟩
                 α⇒
               ⟩
   pentagon             = begin
      (id ⁂ α⇒) ∘ α⇒ ∘ (α⇒ ⁂ id)                                        ≈⟨ pullˡ second∘⟨⟩ ⟩
      ⟨ π₁ ∘ π₁ , α⇒ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (α⇒ ⁂ id)                     ≈⟨ ⟨⟩∘ ⟩
      ⟨ (π₁ ∘ π₁) ∘ (α⇒ ⁂ id) , (α⇒ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (α⇒ ⁂ id) ⟩     ≈⟨ ⟨⟩-cong₂ (pullʳ π₁∘⁂) (pullʳ ⟨⟩∘) ⟩
      ⟨ π₁ ∘ α⇒ ∘ π₁ , α⇒ ∘ ⟨ (π₂ ∘ π₁) ∘ (α⇒ ⁂ id) , π₂ ∘ (α⇒ ⁂ id) ⟩ ⟩  ≈⟨ ⟨⟩-cong₂ (pullˡ project₁) ( refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂) ⟩
      ⟨ (π₁ ∘ π₁) ∘ π₁ , α⇒ ∘ ⟨ π₂ ∘ α⇒ ∘ π₁ , id ∘ π₂ ⟩ ⟩                ≈⟨ ⟨⟩-cong₂ assoc (refl⟩∘⟨ ⟨⟩-cong₂ (pullˡ project₂) identityˡ) ⟩
      ⟨ π₁₁₁ , α⇒ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁ , π₂ ⟩ ⟩                       ≈⟨ ⟨⟩-congˡ (refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘) ⟩
      ⟨ π₁₁₁ , α⇒ ∘ ⟨ ⟨ (π₂ ∘ π₁) ∘ π₁ , π₂ ∘ π₁ ⟩ , π₂ ⟩ ⟩                ≈⟨ ⟨⟩-congˡ assocˡ∘⟨⟩ ⟩
      ⟨ π₁₁₁ , ⟨ (π₂ ∘ π₁) ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ⟩                      ≈˘⟨ ⟨⟩-congˡ (⟨⟩-cong₂ (Equiv.trans (pullʳ project₁) sym-assoc) project₂) ⟩
      ⟨ π₁₁₁ , ⟨ (π₂ ∘ π₁) ∘ α⇒ , π₂ ∘ α⇒ ⟩ ⟩                             ≈˘⟨ ⟨⟩-cong₂ (pullʳ project₁) ⟨⟩∘ ⟩
      ⟨ (π₁ ∘ π₁) ∘ α⇒ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ α⇒ ⟩                          ≈˘⟨ ⟨⟩∘ ⟩
      α⇒ ∘ α⇒                                                           ∎
      where
        π₁₁₁ = π₁ ∘ π₁ ∘ π₁

  monoidal : Monoidal 𝒞
  monoidal = record
    { ⊗                    = -×-
    ; unit                 = ⊤
    ; unitorˡ              = ⊤×A≅A
    ; unitorʳ              = A×⊤≅A
    ; associator           = ≅.sym ×-assoc
    ; unitorˡ-commute-from = project₂
    ; unitorˡ-commute-to   = let open NaturalIsomorphism ⊤×--id in ⇐.commute _
    ; unitorʳ-commute-from = project₁
    ; unitorʳ-commute-to   = let open NaturalIsomorphism -×⊤-id in ⇐.commute _
    ; assoc-commute-from   = assocˡ∘⁂
    ; assoc-commute-to     = assocʳ∘⁂
    ; triangle             = begin
      (id ⁂ π₂) ∘ assocˡ                       ≈⟨ ⁂∘⟨⟩ ⟩
      ⟨ id ∘ π₁ ∘ π₁ , π₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ identityˡ) (project₂ ○ (⟺ identityˡ)) ⟩
      π₁ ⁂ id                                  ∎
    ; pentagon             = pentagon
    }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --no-qualified-instances #-}

module NoQualifiedInstances-InAnonymousModule where

postulate
  A : Set
  f : {{A}} → A

module _ where postulate instance a : A

test : A
test = f

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
open import Relation.Binary.Core

module PLRTree.Everything {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import PLRTree.Complete.Correctness.Base {A}
open import PLRTree.Drop.Complete _≤_ tot≤
open import PLRTree.Drop.Heap _≤_ tot≤ trans≤
open import PLRTree.Drop.Permutation _≤_ tot≤
open import PLRTree.Heap.Correctness _≤_
open import PLRTree.Insert.Complete _≤_ tot≤
open import PLRTree.Insert.Heap _≤_ tot≤ trans≤
open import PLRTree.Insert.Permutation _≤_ tot≤


text:
module Control.Exception.Primitive where

open import IO.Primitive

postulate
  bracket : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → IO A → (A → IO B) → (A → IO C) → IO C

{-# IMPORT Control.Exception #-}
{-# COMPILED bracket (\_ _ _ _ _ _ -> Control.Exception.bracket) #-}

max_stars_repo_name: ilya-fiveisky/agda-exceptions

max_issues_repo_name: ilya-fiveisky/agda-exceptions

max_forks_repo_name: ilya-fiveisky/agda-exceptions