text:
module Issue277 where

data D : Set where
  d : D

abstract

  x : D
  x = d

-- Normalise x using the Emacs mode, at the top-level. Result: d. The
-- result should be x. Agda.Interaction.GhciTop.cmd_compute_toplevel
-- receives the right arguments, so the problem does not lie in the
-- Emacs Lisp code.

y : D
y = {!x!}  -- Normalisation works correctly in the goal.

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

-- Mentioned in passing here:
-- https://ncatlab.org/nlab/show/slice+2-category

open import Categories.Bicategory using (Bicategory)

module Categories.Bicategory.Construction.LaxSlice
       {o ℓ e t}
       (𝒞 : Bicategory o ℓ e t)
       where

open import Data.Product using (_,_)
open import Function using (_$_)
open import Level using (_⊔_)

open import Categories.Bicategory.Extras 𝒞
open Shorthands
open import Categories.Category using () renaming (Category to 1Category)
open import Categories.Functor using (Functor)
open Functor using (F₀)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Construction.Constant using (const)
import Categories.Morphism.Reasoning as MR
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper)

record SliceObj (X : Obj) : Set (t ⊔ o) where
  constructor sliceobj
  field
    {Y} : Obj
    arr : Y ⇒₁ X

module SliceHom (A : Obj) where

  record Slice⇒₁ (X Y : SliceObj A) : Set (o ⊔ ℓ) where
    constructor slicearr₁
    private
      module X = SliceObj X
      module Y = SliceObj Y

    field
      {h} : X.Y ⇒₁ Y.Y
      Δ   : X.arr ⇒₂ (Y.arr ∘₁ h)

  record Slice⇒₂ {X Y : SliceObj A} (J K : Slice⇒₁ X Y) : Set (ℓ ⊔ e) where
    constructor slicearr₂
    private
      module Y = SliceObj Y
      module J = Slice⇒₁ J
      module K = Slice⇒₁ K

    field
      {ϕ} : J.h ⇒₂ K.h
      E   : K.Δ ≈ (Y.arr ▷ ϕ ∘ᵥ J.Δ)

  _∘ᵥ/_ : ∀ {X Y : SliceObj A}{J K L : Slice⇒₁ X Y} → Slice⇒₂ K L → Slice⇒₂ J K → Slice⇒₂ J L
  _∘ᵥ/_ {X}{Y}{J}{K}{L} (slicearr₂ {ϕ = ϕ} E) (slicearr₂ {ϕ = ψ} F) = slicearr₂ {ϕ = ϕ ∘ᵥ ψ} $ begin
      L.Δ                             ≈⟨ E ⟩
      (Y.arr ▷ ϕ ∘ᵥ K.Δ)              ≈⟨ refl⟩∘⟨ F ⟩
      Y.arr ▷ ϕ ∘ᵥ (Y.arr ▷ ψ ∘ᵥ J.Δ) ≈⟨ pullˡ ∘ᵥ-distr-▷ ⟩
      Y.arr ▷ (ϕ ∘ᵥ ψ) ∘ᵥ J.Δ         ∎
    where module X = SliceObj X
          module Y = SliceObj Y
          module J = Slice⇒₁ J
          module K = Slice⇒₁ K
          module L = Slice⇒₁ L
          open 1Category (hom X.Y A)
          open HomReasoning
          open Equiv
          open MR (hom X.Y A)

  SliceHomCat : SliceObj A → SliceObj A → 1Category (o ⊔ ℓ) (ℓ ⊔ e) e
  SliceHomCat X Y = record
    { Obj = Slice⇒₁ X Y
    ; _⇒_ = Slice⇒₂
    ; _≈_ = λ (slicearr₂ {ϕ} _) (slicearr₂ {ψ} _) → ϕ ≈ ψ
    ; id = slice-id _
    ; _∘_ = _∘ᵥ/_
    ; assoc = hom.assoc
    ; sym-assoc = hom.sym-assoc
    ; identityˡ = hom.identityˡ
    ; identityʳ = hom.identityʳ
    ; identity² = hom.identity²
    ; equiv = record { refl = refl ; sym = sym ; trans = trans }
    ; ∘-resp-≈ = hom.∘-resp-≈
    }
    where
      open hom.Equiv
      module X = SliceObj X
      module Y = SliceObj Y

      slice-id : ∀ (J : Slice⇒₁ X Y) → Slice⇒₂ J J
      slice-id J = slicearr₂ $ begin
        J.Δ                 ≈˘⟨ identity₂ˡ ⟩
        id₂ ∘ᵥ J.Δ          ≈˘⟨ ▷id₂ ⟩∘⟨refl ⟩
        (Y.arr ▷ id₂) ∘ J.Δ ∎
        where module J = Slice⇒₁ J
              open 1Category (hom X.Y A)
              open HomReasoning

  _⊚₀/_ : ∀ {X Y Z : SliceObj A} → Slice⇒₁ Y Z → Slice⇒₁ X Y → Slice⇒₁ X Z
  _⊚₀/_ {X}{Y}{Z} J K = slicearr₁ ((α⇒ ∘ᵥ J.Δ ◁ K.h) ∘ᵥ K.Δ)
    where module K = Slice⇒₁ K
          module J = Slice⇒₁ J

  _⊚₁/_ : ∀ {X Y Z : SliceObj A} → {J J' : Slice⇒₁ Y Z} → {K K' : Slice⇒₁ X Y} → Slice⇒₂ J J' → Slice⇒₂ K K' → Slice⇒₂ (J ⊚₀/ K) (J' ⊚₀/ K')
  _⊚₁/_ {X}{Y}{Z}{J'}{J}{K'}{K} δ γ = slicearr₂ $ begin
    (α⇒ ∘ᵥ J.Δ ◁ K.h) ∘ᵥ K.Δ                                                  ≈⟨ (refl⟩∘⟨ γ.E) ⟩
    (α⇒ ∘ᵥ J.Δ ◁ K.h) ∘ᵥ (Y.arr ▷ γ.ϕ ∘ᵥ K'.Δ)                                ≈⟨ ((refl⟩∘⟨ δ.E ⟩⊚⟨refl) ⟩∘⟨refl) ⟩
    (α⇒ ∘ᵥ (Z.arr ▷ δ.ϕ ∘ᵥ J'.Δ) ◁ K.h) ∘ᵥ (Y.arr ▷ γ.ϕ ∘ᵥ K'.Δ)              ≈˘⟨ (((refl⟩∘⟨ ∘ᵥ-distr-◁ ) ⟩∘⟨refl)) ⟩
    (α⇒ ∘ᵥ ((Z.arr ▷ δ.ϕ) ◁ K.h ∘ᵥ J'.Δ ◁ K.h)) ∘ᵥ (Y.arr ▷ γ.ϕ ∘ᵥ K'.Δ)      ≈⟨ pullʳ (center (sym ◁-▷-exchg)) ⟩
    α⇒ ∘ᵥ (Z.arr ▷ δ.ϕ) ◁ K.h ∘ᵥ (Z.arr ⊚₀ J'.h ▷ γ.ϕ ∘ᵥ J'.Δ ◁ K'.h) ∘ᵥ K'.Δ ≈⟨ pushʳ ( pullˡ (pullˡ (sym ⊚.homomorphism)) ) ⟩
    (α⇒ ∘ᵥ (Z.arr ▷ δ.ϕ ∘ᵥ id₂) ⊚₁ (id₂ ∘ᵥ γ.ϕ) ∘ᵥ J'.Δ ◁ K'.h) ∘ᵥ K'.Δ       ≈⟨ ((refl⟩∘⟨ (identity₂ʳ ⟩⊚⟨ identity₂ˡ ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
    (α⇒ ∘ᵥ ((Z.arr ▷ δ.ϕ) ⊚₁ γ.ϕ) ∘ᵥ J'.Δ ◁ K'.h) ∘ᵥ K'.Δ                     ≈⟨ pushˡ (pullˡ (⊚-assoc.⇒.commute ((id₂ , δ.ϕ) , γ.ϕ))) ⟩
    (Z.arr ▷ δ.ϕ ⊚₁ γ.ϕ ∘ᵥ α⇒) ∘ᵥ J'.Δ ◁ K'.h ∘ᵥ K'.Δ                         ≈⟨ pullʳ (sym assoc) ⟩
    (Z.arr ▷ δ.ϕ ⊚₁ γ.ϕ) ∘ᵥ ((α⇒ ∘ᵥ J'.Δ ◁ K'.h) ∘ᵥ K'.Δ)                     ∎
    where module X = SliceObj X
          module Y = SliceObj Y
          module Z = SliceObj Z
          module J = Slice⇒₁ J
          module J' = Slice⇒₁ J'
          module K = Slice⇒₁ K
          module K' = Slice⇒₁ K'
          module γ = Slice⇒₂ γ
          module δ = Slice⇒₂ δ
          open 1Category (hom X.Y A)
          open HomReasoning
          open MR (hom X.Y A)
          open Equiv

  id/ : ∀ {X : SliceObj A} → Slice⇒₁ X X
  id/ = slicearr₁ ρ⇐

  _⊚/_ : ∀ {X Y Z : SliceObj A} → Bifunctor (SliceHomCat Y Z) (SliceHomCat X Y) (SliceHomCat X Z)
  _⊚/_ {X}{Y}{Z} = record
    { F₀ = λ (J , K) → J ⊚₀/ K
    ; F₁ = λ (δ , γ) → δ ⊚₁/ γ
      ; identity = ⊚.identity
      ; homomorphism = ⊚.homomorphism
      ; F-resp-≈ = ⊚.F-resp-≈
      }
      where module X = SliceObj X
            module Y = SliceObj Y
            module Z = SliceObj Z

  α⇒/ : ∀ {W X Y Z}(J : Slice⇒₁ Y Z) (K : Slice⇒₁ X Y) (L : Slice⇒₁ W X) → Slice⇒₂ ((J ⊚₀/ K) ⊚₀/ L) (J ⊚₀/ (K ⊚₀/ L))
  α⇒/ {W}{X}{Y}{Z} J K L = slicearr₂ $ begin
    (α⇒ ∘ᵥ J.Δ ◁ K.h ⊚₀ L.h) ∘ᵥ ((α⇒ ∘ᵥ K.Δ ◁ L.h) ∘ᵥ L.Δ  )                  ≈⟨ pullʳ (center⁻¹ (sym α⇒-◁-∘₁) refl) ⟩
    α⇒ ∘ᵥ (α⇒ ∘ᵥ J.Δ ◁ K.h ◁ L.h) ∘ᵥ K.Δ ◁ L.h ∘ᵥ L.Δ                         ≈⟨ pullˡ (pullˡ (sym pentagon)) ⟩
    ((Z.arr ▷ α⇒ ∘ᵥ α⇒ ∘ᵥ α⇒ ◁ L.h) ∘ᵥ J.Δ ◁ K.h ◁ L.h) ∘ᵥ (K.Δ ◁ L.h ∘ᵥ L.Δ) ≈⟨ pullˡ (pushˡ (pull-last ∘ᵥ-distr-◁ )) ⟩
    (Z.arr ▷ α⇒ ∘ᵥ (α⇒ ∘ᵥ ((α⇒ ∘ᵥ J.Δ ◁ K.h) ◁ L.h)) ∘ᵥ K.Δ ◁ L.h) ∘ᵥ L.Δ     ≈⟨ pushˡ (pushʳ (pullʳ ∘ᵥ-distr-◁)) ⟩
    ((Z.arr ▷ α⇒ ∘ᵥ α⇒)) ∘ᵥ (((α⇒ ∘ᵥ J.Δ ◁ K.h) ∘ᵥ K.Δ) ◁ L.h) ∘ᵥ L.Δ         ≈⟨ pullʳ (pushʳ refl) ⟩
    Z.arr ▷ α⇒ ∘ᵥ ((α⇒ ∘ᵥ (((α⇒ ∘ᵥ J.Δ ◁ K.h)) ∘ᵥ K.Δ) ◁ L.h) ∘ᵥ L.Δ)         ∎
    where module W = SliceObj W
          module X = SliceObj X
          module Y = SliceObj Y
          module Z = SliceObj Z
          module J = Slice⇒₁ J
          module K = Slice⇒₁ K
          module L = Slice⇒₁ L
          open 1Category (hom W.Y A)
          open HomReasoning
          open MR (hom W.Y A)
          open hom.Equiv

  λ⇒/ : ∀ {X Y} (J : Slice⇒₁ X Y) → Slice⇒₂ (id/ ⊚₀/ J) J
  λ⇒/ {X}{Y} J = slicearr₂ $ begin
    J.Δ                                   ≈⟨ introˡ id₂◁ ⟩
    (id₂ ◁ J.h) ∘ᵥ J.Δ                    ≈˘⟨ (unitʳ.iso.isoʳ (Y.arr , _) ⟩⊚⟨refl ⟩∘⟨refl) ⟩
    ((ρ⇒ ∘ᵥ ρ⇐) ◁ J.h) ∘ᵥ J.Δ             ≈˘⟨ (∘ᵥ-distr-◁ ⟩∘⟨refl) ⟩
    (ρ⇒ ◁ J.h ∘ᵥ ρ⇐ ◁ J.h) ∘ᵥ J.Δ         ≈⟨ pushˡ (sym triangle ⟩∘⟨ refl) ⟩
    (Y.arr ▷ λ⇒ ∘ᵥ α⇒) ∘ᵥ ρ⇐ ◁ J.h ∘ᵥ J.Δ ≈⟨ pullʳ (sym assoc) ⟩
    Y.arr ▷ λ⇒ ∘ᵥ (α⇒ ∘ᵥ ρ⇐ ◁ J.h) ∘ᵥ J.Δ ∎
    where module X = SliceObj X
          module Y = SliceObj Y
          module J = Slice⇒₁ J
          open 1Category (hom X.Y A)
          open HomReasoning
          open MR (hom X.Y A)
          open hom.Equiv

  ρ⇒/ : ∀{X}{Y} (J : Slice⇒₁ X Y) → Slice⇒₂ (J ⊚₀/ id/) J
  ρ⇒/ {X}{Y} J = slicearr₂ $ begin
    J.Δ                                     ≈⟨ introʳ (unitʳ.iso.isoʳ _) ⟩
    J.Δ ∘ᵥ ρ⇒ ∘ᵥ ρ⇐                         ≈⟨ pullˡ (sym ρ⇒-∘ᵥ-◁) ⟩
    (ρ⇒ ∘ᵥ J.Δ ◁ id₁) ∘ᵥ ρ⇐                 ≈⟨ unitorʳ-coherence  ⟩∘⟨refl ⟩∘⟨refl ⟩
    ((Y.arr ▷ ρ⇒ ∘ᵥ α⇒) ∘ᵥ J.Δ ◁ id₁) ∘ᵥ ρ⇐ ≈⟨ pushˡ assoc ⟩
    Y.arr ▷ ρ⇒ ∘ᵥ (α⇒ ∘ᵥ J.Δ ◁ id₁) ∘ᵥ ρ⇐   ∎
    where module X = SliceObj X
          module Y = SliceObj Y
          module J = Slice⇒₁ J
          open 1Category (hom X.Y A)
          open HomReasoning
          open MR (hom X.Y A)
          open hom.Equiv

  slice-inv : ∀ {X}{Y}{J : Slice⇒₁ X Y}{K} (α : Slice⇒₂ J K) → (f : Slice⇒₁.h K ⇒₂ Slice⇒₁.h J) → (f ∘ᵥ (Slice⇒₂.ϕ α) ≈ id₂) → Slice⇒₂ K J
  slice-inv {X}{Y}{J}{K} α f p = slicearr₂ $ begin
    J.Δ                               ≈⟨ introˡ ▷id₂ ⟩
    (Y.arr ▷ id₂) ∘ᵥ J.Δ              ≈˘⟨ (refl⟩⊚⟨ p ⟩∘⟨refl) ⟩
    (Y.arr ▷ (f ∘ᵥ α.ϕ)) ∘ᵥ J.Δ       ≈˘⟨ (∘ᵥ-distr-▷ ⟩∘⟨refl) ⟩
    (Y.arr ▷ f ∘ᵥ Y.arr ▷ α.ϕ) ∘ᵥ J.Δ ≈⟨ pullʳ (sym α.E) ⟩
    Y.arr ▷ f ∘ᵥ K.Δ                  ∎
    where module X = SliceObj X
          module Y = SliceObj Y
          module J = Slice⇒₁ J
          module K = Slice⇒₁ K
          module α = Slice⇒₂ α
          open 1Category (hom X.Y A)
          open HomReasoning
          open MR (hom X.Y A)
          open hom.Equiv

LaxSlice : Obj → Bicategory (o ⊔ ℓ) (ℓ ⊔ e) e (o ⊔ t)
LaxSlice A   = record
  { enriched = record
    { Obj = SliceObj A
    ; hom = SliceHomCat
    ; id = const id/
    ; ⊚ = _⊚/_
    ; ⊚-assoc = niHelper (record
      { η       = λ ((J , K) , L) → α⇒/ J K L
      ; η⁻¹     = λ ((J , K) , L) → slice-inv (α⇒/ J K L) α⇐ (⊚-assoc.iso.isoˡ _)
      ; commute = λ f → ⊚-assoc.⇒.commute _
      ; iso = λ _ → record { isoˡ = ⊚-assoc.iso.isoˡ _ ; isoʳ = ⊚-assoc.iso.isoʳ _ }
      })
    ; unitˡ = niHelper (record
      { η       = λ (_ , J) → λ⇒/ J
      ; η⁻¹     = λ (_ , J) → slice-inv (λ⇒/ J) λ⇐ (unitˡ.iso.isoˡ _)
      ; commute = λ _ → λ⇒-∘ᵥ-▷
      ; iso     = λ _ → record { isoˡ = unitˡ.iso.isoˡ _ ; isoʳ = unitˡ.iso.isoʳ _ }
      })
    ; unitʳ = niHelper (record
         { η       = λ (J , _) → ρ⇒/ J
         ; η⁻¹     = λ (J , _) → slice-inv (ρ⇒/ J) ρ⇐ (unitʳ.iso.isoˡ _)
         ; commute = λ _ → ρ⇒-∘ᵥ-◁
         ; iso     = λ _ → record { isoˡ = unitʳ.iso.isoˡ _ ; isoʳ = unitʳ.iso.isoʳ _ } })
    }
  ; triangle = triangle
  ; pentagon = pentagon
  }
  where open SliceHom A

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text:
module L.Base.Id.Core where

-- Use the builtin _≡_ and refl
open import Agda.Builtin.Equality public

J : ∀{a c} {A : Set a} → (C : (x y : A) → x ≡ y → Set c)
              → ((x : A) → C x x refl)
              → (M N : A) → (P : M ≡ N ) → C M N P
J C c M .M refl = c M

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
open import Prelude
open import Nat

module List where
  -- lets us omit a bunch of parens
  infixr 99 _::_
  infixr 9 _++_

  -- standard definition of polymorphic lists
  data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A

  {-# BUILTIN LIST List #-}

  -- shorthand notation for small lists
  [_] : {A : Set} → A → List A
  [ x ] = x :: []

  -- list append
  _++_ : {A : Set} → List A → List A → List A
  [] ++ l2 = l2
  x :: l1 ++ l2 = x :: (l1 ++ l2)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module plfa.Relations where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open import Data.Nat using (ℕ ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ { n : ℕ }
      ---------
      → zero ≤ n

  s≤s : ∀ { m n : ℕ }
    → m ≤ n
      ---------------
    → suc m ≤ suc n

infix 4 _≤_

_ : 2 ≤ 4
_ = s≤s (s≤s z≤n)

_ : 2 ≤ 4
_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))

_ : 2 ≤ 4
_ = s≤s {m = 1} {n = 3} (s≤s {m = 0} {n = 2} (z≤n {n = 2}))

_ : 2 ≤ 4
_ = s≤s {n = 3} (s≤s {n = 2} z≤n)

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

inv-z≤n : ∀ { m : ℕ }
  → m ≤ zero
    --------
  → m ≡ zero
inv-z≤n z≤n = refl

-- @practice: exercise `orderings` start

-- _⊆_ relations has partial order property but not total order
-- adjacency relation has preorder property but not partial order

-- @practice: exercise `orderings` end

-- 自反: reflexive - refl
-- 传递: transitive - trans
-- 反对称: anti-symmetric - antisym
-- 完全: total - total

≤-refl : ∀ { n : ℕ }
    -----
    → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

≤-trans : ∀ { m n p : ℕ }
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans z≤n    _ = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

max_stars_repo_name: lonelyhentai/workspace

max_issues_repo_name: lonelyhentai/workspace

max_forks_repo_name: lonelyhentai/workspace


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
{-# OPTIONS --allow-unsolved-metas #-}
open import LibraBFT.Prelude
open import LibraBFT.Base.PKCS
open import LibraBFT.Concrete.Obligations
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Util.Crypto
open        EpochConfig
open import LibraBFT.Yasm.Yasm (ℓ+1 0ℓ) EpochConfig epochId authorsN ConcSysParms NodeId-PK-OK

-- In this module, we will prove a structural property that any new signed message produced by an
-- honest handler from a reachable state correctly identifies the sender, and is for a valid epoch
-- of which that sender is a member.  It is postulated for now, because the property does not yet
-- hold for our fake implementation that does not actually comply.  A proof outline and notes are
-- included below, which we can finish once we do have a compliant implementation.

module LibraBFT.Impl.Properties.Aux where
  -- This proof is complete except for pieces that are directly about the handlers.  Our
  -- fake/simple handler does not yet obey the needed properties, so we can't finish this yet.
  impl-sps-avp : StepPeerState-AllValidParts
  -- In our fake/simple implementation, init and handling V and C msgs do not send any messages
  impl-sps-avp _ hpk (step-init ix) m∈outs part⊂m ver      = ⊥-elim (¬Any[] m∈outs)
  impl-sps-avp _ hpk (step-msg {sndr , V vm} _ _) m∈outs _ _ = ⊥-elim (¬Any[] m∈outs)
  impl-sps-avp _ hpk (step-msg {sndr , C cm} _ _) m∈outs _ _ = ⊥-elim (¬Any[] m∈outs)
  -- These aren't true yet, because processProposalMsgM sends fake votes that don't follow the rules for ValidPartForPK
  impl-sps-avp preach hpk (step-msg {sndr , P pm} m∈pool ps≡) m∈outs v⊂m ver
     with m∈outs
     -- Handler sends at most one vote, so it can't be "there"
  ...| there {xs = xs} imp = ⊥-elim (¬Any[] imp)
  ...| here refl
     with v⊂m
  ...| vote∈qc vs∈qc rbld≈ qc∈m
     with qc∈m
  ...| xxx = {!x!}                -- We will prove that votes represented in the SyncInfo of a
                                  -- proposal message were sent before, so these will be inj₂.
                                  -- This will be based on an invariant of the implementation, for
                                  -- example that the QCs included in the SyncInfo of a VoteMsg have
                                  -- been sent before.  We will need to use hash injectivity and
                                  -- signature injectivity to ensure a different vote was not sent
                                  -- previously with the same signature.

  impl-sps-avp {pk = pk} {α = α} {st = st} preach hpk (step-msg {sndr , P pm} m∈pool ps≡) m∈outs v⊂m ver
     | here refl
     | vote∈vm {si}
     with MsgWithSig∈? {pk} {ver-signature ver} {msgPool st}
  ...| yes msg∈ = inj₂ msg∈
  ...| no  msg∉ = inj₁ ((mkValidSenderForPK      {! epoch !} -- We will need an invariant that says the epoch
                                                             -- used by a voter is "in range".
                                                 (EC-lookup' (availEpochs st) {!!})
                                                 refl
                                                 {! !}       -- The implementation will need to check that the voter is a member of
                                                             -- the epoch of the message it's sending.
                                                 )
                        , msg∉)

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


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

module Relation.Binary.Equivalence.PropTruncated where

open import Prelude
open import Relation.Nullary.Stable

infix 4 _≐_
data _≐_ {a} {A : Type a} (x y : A) : Prop a where
  ∣_∣ : x ≡ y → x ≐ y

data ∙⊥ : Prop where

private
  variable
    x y z : A

rerel : ∙⊥ → ⊥
rerel ()

∙refute : x ≐ y → (x ≡ y → ⊥) → ∙⊥
∙refute ∣ x≡y ∣ x≢y with x≢y x≡y
∙refute ∣ x≡y ∣ x≢y | ()

refute : x ≐ y → ¬ (¬ (x ≡ y))
refute x≐y x≢y = rerel (∙refute x≐y x≢y)

unsquash : Stable (x ≡ y) → x ≐ y → x ≡ y
unsquash st x≐y = st (refute x≐y)

∙refl : x ≐ x
∙refl = ∣ refl ∣

∙trans : x ≐ y → y ≐ z → x ≐ z
∙trans ∣ xy ∣ (∣_∣ yz) = ∣_∣ (xy ; yz)

∙sym : x ≐ y → y ≐ x
∙sym (∣_∣ p) = ∣_∣ (sym p)

∙cong : (f : A → B) → x ≐ y → f x ≐ f y
∙cong f ∣ x≡y ∣ = ∣ cong f x≡y ∣

module Reasoning where
  infixr 2 ≐˘⟨⟩-syntax ≐⟨∙⟩-syntax

  ≐˘⟨⟩-syntax : ∀ (x : A) {y z} → y ≐ z → y ≐ x → x ≐ z
  ≐˘⟨⟩-syntax _ y≡z y≡x = ∙trans (∙sym y≡x) y≡z

  syntax ≐˘⟨⟩-syntax x y≡z y≡x = x ≐˘⟨ y≡x ⟩ y≡z

  ≐⟨∙⟩-syntax : ∀ (x : A) {y z} → y ≐ z → x ≐ y → x ≐ z
  ≐⟨∙⟩-syntax _ y≡z x≡y = ∙trans x≡y y≡z

  syntax ≐⟨∙⟩-syntax x y≡z x≡y = x ≐⟨ x≡y ⟩ y≡z

  _≐⟨⟩_ : ∀ (x : A) {y} → x ≐ y → x ≐ y
  _ ≐⟨⟩ x≡y = x≡y

  infix 2.5 _∎
  _∎ : ∀ {A : Type a} (x : A) → x ≐ x
  _∎ x = ∙refl

  infixr 2 ≡˘⟨⟩-syntax ≡⟨∙⟩-syntax

  ≡˘⟨⟩-syntax : ∀ (x : A) {y z} → y ≐ z → y ≡ x → x ≐ z
  ≡˘⟨⟩-syntax _ y≡z y≡x = ∙trans (∣_∣ (sym y≡x)) y≡z

  syntax ≡˘⟨⟩-syntax x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

  ≡⟨∙⟩-syntax : ∀ (x : A) {y z} → y ≐ z → x ≡ y → x ≐ z
  ≡⟨∙⟩-syntax _ y≡z x≡y = ∙trans ∣ x≡y ∣ y≡z

  syntax ≡⟨∙⟩-syntax x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Mockingbird.Forest using (Forest)

-- Mockingbirds, Warblers, and Starlings
module Mockingbird.Problems.Chapter12 {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Product using (_×_; _,_; proj₁; ∃-syntax)
open import Function using (_$_)

open import Mockingbird.Forest.Birds forest
import Mockingbird.Problems.Chapter11 forest as Chapter₁₁

open Forest forest

problem₁ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ → HasDoubleMockingbird
problem₁ = record
  { M₂ = B ∙ M
  ; isDoubleMockingbird = λ x y → begin
     B ∙ M ∙ x ∙ y    ≈⟨ isBluebird M x y ⟩
     M ∙ (x ∙ y)      ≈⟨ isMockingbird (x ∙ y) ⟩
     x ∙ y ∙ (x ∙ y)  ∎
  }

problem₂-BCM : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ ⦃ _ : HasMockingbird ⦄ → HasLark
problem₂-BCM = record
  { L = C ∙ B ∙ M
  ; isLark = λ x y → begin
      C ∙ B ∙ M ∙ x ∙ y  ≈⟨ congʳ $ isCardinal B M x ⟩
      B ∙ x ∙ M ∙ y      ≈⟨ isBluebird x M y ⟩
      x ∙ (M ∙ y)        ≈⟨ congˡ $ isMockingbird y ⟩
      x ∙ (y ∙ y)        ∎
  } where instance hasCardinal = Chapter₁₁.problem₂₁′

problem₂-BRM : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ ⦃ _ : HasMockingbird ⦄ → HasLark
problem₂-BRM = record
  { L = R ∙ M ∙ B
  ; isLark = λ x y → begin
      R ∙ M ∙ B ∙ x ∙ y  ≈⟨ congʳ $ isRobin M B x ⟩
      B ∙ x ∙ M ∙ y      ≈⟨ isBluebird x M y ⟩
      x ∙ (M ∙ y)        ≈⟨ congˡ $ isMockingbird y ⟩
      x ∙ (y ∙ y)        ∎
  } where instance hasRobin = Chapter₁₁.problem₂₀

problem₃ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasWarbler ⦄ → HasLark
problem₃ = record
  { L = B ∙ W ∙ B
  ; isLark = λ x y → begin
      B ∙ W ∙ B ∙ x ∙ y  ≈⟨ congʳ $ isBluebird W B x ⟩
      W ∙ (B ∙ x) ∙ y    ≈⟨ isWarbler (B ∙ x) y ⟩
      B ∙ x ∙ y ∙ y      ≈⟨ isBluebird x y y ⟩
      x ∙ (y ∙ y)        ∎
  }

problem₄ : ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasQueerBird ⦄ → HasLark
problem₄ = record
  { L = Q ∙ M
  ; isLark = λ x y → begin
      Q ∙ M ∙ x ∙ y  ≈⟨ isQueerBird M x y ⟩
      x ∙ (M ∙ y)    ≈⟨ congˡ $ isMockingbird y ⟩
      x ∙ (y ∙ y)    ∎
  }

problem₅ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasRobin ⦄ ⦃ _ : HasMockingbird ⦄ → HasConverseWarbler
problem₅ = record
  { W′ = M₂ ∙ R
  ; isConverseWarbler = λ x y → begin
      M₂ ∙ R ∙ x ∙ y       ≈⟨ congʳ $ isDoubleMockingbird R x ⟩
      R ∙ x ∙ (R ∙ x) ∙ y  ≈⟨ isRobin x (R ∙ x) y ⟩
      R ∙ x ∙ y ∙ x        ≈⟨ isRobin x y x ⟩
      y ∙ x ∙ x            ∎
  } where instance hasDoubleMockingbird = problem₁

problem₆′ : ⦃ _ : HasCardinal ⦄ ⦃ _ : HasConverseWarbler ⦄ → HasWarbler
problem₆′ = record
  { W = C ∙ W′
  ; isWarbler = λ x y → begin
      C ∙ W′ ∙ x ∙ y ≈⟨ isCardinal W′ x y ⟩
      W′ ∙ y ∙ x     ≈⟨ isConverseWarbler y x ⟩
      x ∙ y ∙ y      ∎
  }

problem₆ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasRobin ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasMockingbird ⦄ → HasWarbler
problem₆ = record
  { W = C ∙ (B ∙ M ∙ R)
  ; isWarbler = λ x y → begin
      C ∙ (B ∙ M ∙ R) ∙ x ∙ y  ≈⟨⟩
      C ∙ (M₂ ∙ R) ∙ x ∙ y     ≈⟨⟩
      C ∙ W′ ∙ x ∙ y           ≈⟨⟩
      W ∙ x ∙ y                ≈⟨ isWarbler x y ⟩
      x ∙ y ∙ y                ∎
  } where
  instance
    hasDoubleMockingbird = problem₁
    hasConverseWarbler = problem₅
    hasWarbler = problem₆′

problem₇ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ ⦃ _ : HasMockingbird ⦄ → HasWarbler
problem₇ = record
  { W = B ∙ (T ∙ (B ∙ M ∙ (B ∙ B ∙ T))) ∙ (B ∙ B ∙ T)
  ; isWarbler = λ x y → begin
      B ∙ (T ∙ (B ∙ M ∙ (B ∙ B ∙ T))) ∙ (B ∙ B ∙ T) ∙ x ∙ y  ≈˘⟨ congʳ $ congʳ $ isWarbler′ ⟩
      W ∙ x ∙ y                                              ≈⟨ isWarbler x y ⟩
      x ∙ y ∙ y                                              ∎
  } where
  instance
    hasRobin = Chapter₁₁.problem₂₀
    hasCardinal = Chapter₁₁.problem₂₁-bonus
    hasWarbler = problem₆

  isWarbler′ : W ≈ B ∙ (T ∙ (B ∙ M ∙ (B ∙ B ∙ T))) ∙ (B ∙ B ∙ T)
  isWarbler′ = begin
    W                                                            ≈⟨⟩
    C ∙ (B ∙ M ∙ R)                                              ≈⟨⟩
    C ∙ (B ∙ M ∙ (B ∙ B ∙ T))                                    ≈⟨⟩
    B ∙ (T ∙ (B ∙ B ∙ T)) ∙ (B ∙ B ∙ T) ∙ (B ∙ M ∙ (B ∙ B ∙ T))  ≈⟨ isBluebird (T ∙ (B ∙ B ∙ T)) (B ∙ B ∙ T) (B ∙ M ∙ (B ∙ B ∙ T)) ⟩
    T ∙ (B ∙ B ∙ T) ∙ (B ∙ B ∙ T ∙ (B ∙ M ∙ (B ∙ B ∙ T)))        ≈⟨ isThrush (B ∙ B ∙ T) (B ∙ B ∙ T ∙ (B ∙ M ∙ (B ∙ B ∙ T))) ⟩
    B ∙ B ∙ T ∙ (B ∙ M ∙ (B ∙ B ∙ T)) ∙ (B ∙ B ∙ T)              ≈⟨ congʳ $ isBluebird B T (B ∙ M ∙ (B ∙ B ∙ T)) ⟩
    B ∙ (T ∙ (B ∙ M ∙ (B ∙ B ∙ T))) ∙ (B ∙ B ∙ T)                ∎

-- TODO: other expression in problem 7.

-- NOTE: the bluebird B is not necessary.
problem₈ : ⦃ _ : HasThrush ⦄ ⦃ _ : HasWarbler ⦄ → HasMockingbird
problem₈ = record
  { M = W ∙ T
  ; isMockingbird = λ x → begin
      W ∙ T ∙ x  ≈⟨ isWarbler T x ⟩
      T ∙ x ∙ x  ≈⟨ isThrush x x ⟩
      x ∙ x      ∎
  }

problem₉-W* : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ ⦃ _ : HasMockingbird ⦄ → HasWarblerOnceRemoved
problem₉-W* = record
  { W* = B ∙ W
  ; isWarblerOnceRemoved = λ x y z → begin
      B ∙ W ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isBluebird W x y ⟩
      W ∙ (x ∙ y) ∙ z    ≈⟨ isWarbler (x ∙ y) z ⟩
      x ∙ y ∙ z ∙ z      ∎
  } where instance hasWarbler = problem₇

problem₉-W** : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ ⦃ _ : HasMockingbird ⦄ → HasWarblerTwiceRemoved
problem₉-W** = record
  { W** = B ∙ W*
  ; isWarblerTwiceRemoved = λ x y z w → begin
      B ∙ W* ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ congʳ $ isBluebird W* x y ⟩
      W* ∙ (x ∙ y) ∙ z ∙ w    ≈⟨ isWarblerOnceRemoved (x ∙ y) z w ⟩
      x ∙ y ∙ z ∙ w ∙ w       ∎
  } where
  instance
    hasWarbler = problem₇
    hasWarblerOnceRemoved = problem₉-W*

problem₁₀ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasWarbler ⦄ → HasHummingbird
problem₁₀ = record
  { H = B ∙ W ∙ (B ∙ C)
  ; isHummingbird = λ x y z → begin
      B ∙ W ∙ (B ∙ C) ∙ x ∙ y ∙ z   ≈⟨ congʳ $ congʳ $ isBluebird W (B ∙ C) x ⟩
      W ∙ (B ∙ C ∙ x) ∙ y ∙ z       ≈⟨ congʳ $ isWarbler (B ∙ C ∙ x) y ⟩
      B ∙ C ∙ x ∙ y ∙ y ∙ z         ≈⟨ congʳ $ congʳ $ isBluebird C x y ⟩
      C ∙ (x ∙ y) ∙ y ∙ z           ≈⟨ isCardinal (x ∙ y) y z ⟩
      x ∙ y ∙ z ∙ y                 ∎
  }

problem₁₁ : ⦃ _ : HasRobin ⦄ ⦃ _ : HasHummingbird ⦄ → HasWarbler
problem₁₁ = problem₆′
  where
    instance
      hasCardinal = Chapter₁₁.problem₂₁

      hasConverseWarbler : HasConverseWarbler
      hasConverseWarbler = record
        { W′ = H ∙ R
        ; isConverseWarbler = λ x y → begin
            H ∙ R ∙ x ∙ y  ≈⟨ isHummingbird R x y ⟩
            R ∙ x ∙ y ∙ x  ≈⟨ isRobin x y x ⟩
            y ∙ x ∙ x      ∎
        }

problem₁₂ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ ⦃ _ : HasMockingbird ⦄ → HasStarling
problem₁₂ = record
  { S = W** ∙ G
  ; isStarling = λ x y z → begin
      W** ∙ G ∙ x ∙ y ∙ z  ≈⟨ isWarblerTwiceRemoved G x y z ⟩
      G ∙ x ∙ y ∙ z ∙ z    ≈⟨ isGoldfinch x y z z ⟩
      x ∙ z ∙ (y ∙ z)      ∎
  } where
  instance
    hasWarblerTwiceRemoved = problem₉-W**
    hasGoldfinch = Chapter₁₁.problem₄₇

problem₁₃ : ⦃ _ : HasStarling ⦄ ⦃ _ : HasRobin ⦄ → HasHummingbird
problem₁₃ = record
  { H = S ∙ R
  ; isHummingbird = λ x y z → begin
      S ∙ R ∙ x ∙ y ∙ z    ≈⟨ congʳ $ isStarling R x y ⟩
      R ∙ y ∙ (x ∙ y) ∙ z  ≈⟨ isRobin y (x ∙ y) z ⟩
      x ∙ y ∙ z ∙ y        ∎
  }

problem₁₄-SR : ⦃ _ : HasStarling ⦄ ⦃ _ : HasRobin ⦄ → HasWarbler
problem₁₄-SR = record
  { W = R ∙ (S ∙ R ∙ R) ∙ R
  ; isWarbler = λ x y → begin
      R ∙ (S ∙ R ∙ R) ∙ R ∙ x ∙ y      ≈˘⟨ congʳ $ congʳ $ isRobin R R (S ∙ R ∙ R) ⟩
      R ∙ R ∙ R ∙ (S ∙ R ∙ R) ∙ x ∙ y  ≈⟨⟩
      C ∙ (S ∙ R ∙ R) ∙ x ∙ y          ≈⟨⟩
      C ∙ (H ∙ R) ∙ x ∙ y              ≈⟨⟩
      W ∙ x ∙ y                        ≈⟨ isWarbler x y ⟩
      x ∙ y ∙ y                        ∎
  } where
  instance
    hasCardinal = Chapter₁₁.problem₂₁
    hasHummingbird = problem₁₃
    hasWarbler = problem₁₁

problem₁₄-SC : ⦃ _ : HasStarling ⦄ ⦃ _ : HasCardinal ⦄ → HasWarbler
problem₁₄-SC = record
  { W = C ∙ (S ∙ (C ∙ C) ∙ (C ∙ C))
  ; isWarbler = λ x y → begin
      C ∙ (S ∙ (C ∙ C) ∙ (C ∙ C)) ∙ x ∙ y  ≈⟨⟩
      C ∙ (S ∙ R ∙ R) ∙ x ∙ y              ≈⟨ isCardinal (S ∙ R ∙ R) x y ⟩
      S ∙ R ∙ R ∙ y ∙ x                    ≈⟨ congʳ $ isStarling R R y ⟩
      R ∙ y ∙ (R ∙ y) ∙ x                  ≈⟨ isRobin y (R ∙ y) x ⟩
      R ∙ y ∙ x ∙ y                        ≈⟨ isRobin y x y ⟩
      x ∙ y ∙ y                            ∎
  } where instance hasRobin = Chapter₁₁.problem₂₃

problem₁₅ : ⦃ _ : HasThrush ⦄ ⦃ _ : HasStarling ⦄ → HasWarbler
problem₁₅ = record
  { W = S ∙ T
  ; isWarbler = λ x y → begin
      S ∙ T ∙ x ∙ y    ≈⟨ isStarling T x y ⟩
      T ∙ y ∙ (x ∙ y)  ≈⟨ isThrush y (x ∙ y) ⟩
      x ∙ y ∙ y        ∎
  }

problem₁₆ : ⦃ _ : HasThrush ⦄ ⦃ _ : HasStarling ⦄ → HasMockingbird
problem₁₆ = record
  { M = S ∙ T ∙ T
  ; isMockingbird = λ x → begin
      S ∙ T ∙ T ∙ x    ≈⟨ isStarling T T x ⟩
      T ∙ x ∙ (T ∙ x)  ≈⟨ isThrush x (T ∙ x) ⟩
      T ∙ x ∙ x        ≈⟨ isThrush x x ⟩
      x ∙ x            ∎
  }

module Exercises where
  exercise₁-a : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄
    → ∃[ G₁ ] (∀ x y z w v → G₁ ∙ x ∙ y ∙ z ∙ w ∙ v ≈ x ∙ y ∙ v ∙ (z ∙ w))
  exercise₁-a =
    ( D₁ ∙ C*
    , λ x y z w v → begin
        D₁ ∙ C* ∙ x ∙ y ∙ z ∙ w ∙ v  ≈⟨ congʳ $ isDickcissel C* x y z w ⟩
        C* ∙ x ∙ y ∙ (z ∙ w) ∙ v     ≈⟨ isCardinalOnceRemoved x y (z ∙ w) v ⟩
        x ∙ y ∙ v ∙ (z ∙ w)          ∎
    )
    where
      instance
        hasCardinal = Chapter₁₁.problem₂₁′
        hasCardinalOnceRemoved = Chapter₁₁.problem₃₁
        hasDickcissel = Chapter₁₁.problem₉

  -- Note: in the solutions, the bluebird is used, but the exercise does not
  -- state that the bluebird may be used.
  exercise₁-b : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄
    → ∃[ G₁ ] (∀ x y z w v → G₁ ∙ x ∙ y ∙ z ∙ w ∙ v ≈ x ∙ y ∙ v ∙ (z ∙ w))
    → ∃[ G₂ ] (∀ x y z w → G₂ ∙ x ∙ y ∙ z ∙ w ≈ x ∙ w ∙ (x ∙ w) ∙ (y ∙ z))
  exercise₁-b (G₁ , isG₁) =
    ( G₁ ∙ (B ∙ M)
    , λ x y z w → begin
        G₁ ∙ (B ∙ M) ∙ x ∙ y ∙ z ∙ w  ≈⟨ isG₁ (B ∙ M) x y z w ⟩
        B ∙ M ∙ x ∙ w ∙ (y ∙ z)       ≈⟨ congʳ $ isBluebird M x w ⟩
        M ∙ (x ∙ w) ∙ (y ∙ z)         ≈⟨ congʳ $ isMockingbird (x ∙ w) ⟩
        x ∙ w ∙ (x ∙ w) ∙ (y ∙ z)     ∎
    )

  exercise₁-c : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄ ⦃ _ : HasIdentity ⦄
    → ∃[ I₂ ] (∀ x → I₂ ∙ x ≈ x ∙ I ∙ I)
  exercise₁-c =
    ( B ∙ (T ∙ I) ∙ (T ∙ I)
    , λ x → begin
        B ∙ (T ∙ I) ∙ (T ∙ I) ∙ x  ≈⟨ isBluebird (T ∙ I) (T ∙ I) x ⟩
        T ∙ I ∙ (T ∙ I ∙ x)        ≈⟨ isThrush I (T ∙ I ∙ x) ⟩
        T ∙ I ∙ x ∙ I              ≈⟨ congʳ $ isThrush I x ⟩
        x ∙ I ∙ I                  ∎
    )

  exercise₁-d : ⦃ _ : HasIdentity ⦄ ⦃ _ : HasFinch ⦄
    → (hasI₂ : ∃[ I₂ ] (∀ x → I₂ ∙ x ≈ x ∙ I ∙ I))
    → ∀ x → proj₁ hasI₂ ∙ (F ∙ x) ≈ x
  exercise₁-d (I₂ , isI₂) x = begin
    I₂ ∙ (F ∙ x)   ≈⟨ isI₂ (F ∙ x) ⟩
    F ∙ x ∙ I ∙ I  ≈⟨ isFinch x I I ⟩
    I ∙ I ∙ x      ≈⟨ congʳ $ isIdentity I ⟩
    I ∙ x          ≈⟨ isIdentity x ⟩
    x              ∎

  exercise₁-e : ⦃ _ : HasFinch ⦄ ⦃ _ : HasQueerBird ⦄ ⦃ _ : HasIdentity ⦄
    → (hasG₂ : ∃[ G₂ ] (∀ x y z w → G₂ ∙ x ∙ y ∙ z ∙ w ≈ x ∙ w ∙ (x ∙ w) ∙ (y ∙ z)))
    → (hasI₂ : ∃[ I₂ ] (∀ x → I₂ ∙ x ≈ x ∙ I ∙ I))
    → IsWarbler (proj₁ hasG₂ ∙ F ∙ (Q ∙ proj₁ hasI₂))
  exercise₁-e (G₂ , isG₂) (I₂ , isI₂) x y = begin
    G₂ ∙ F ∙ (Q ∙ I₂) ∙ x ∙ y       ≈⟨ isG₂ F (Q ∙ I₂) x y ⟩
    F ∙ y ∙ (F ∙ y) ∙ (Q ∙ I₂ ∙ x)  ≈⟨ isFinch y (F ∙ y) (Q ∙ I₂ ∙ x) ⟩
    Q ∙ I₂ ∙ x ∙ (F ∙ y) ∙ y        ≈⟨ congʳ $ isQueerBird I₂ x (F ∙ y) ⟩
    x ∙ (I₂ ∙ (F ∙ y)) ∙ y          ≈⟨ congʳ $ congˡ $ exercise₁-d (I₂ , isI₂) y ⟩
    x ∙ y ∙ y                       ∎

  exercise₂ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasWarbler ⦄
    → IsStarling (B ∙ (B ∙ (B ∙ W) ∙ C) ∙ (B ∙ B))
  exercise₂ x y z = begin
    B ∙ (B ∙ (B ∙ W) ∙ C) ∙ (B ∙ B) ∙ x ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ isBluebird (B ∙ (B ∙ W) ∙ C) (B ∙ B) x ⟩
    B ∙ (B ∙ W) ∙ C ∙ (B ∙ B ∙ x) ∙ y ∙ z        ≈⟨ congʳ $ congʳ $ isBluebird (B ∙ W) C (B ∙ B ∙ x) ⟩
    B ∙ W ∙ (C ∙ (B ∙ B ∙ x)) ∙ y ∙ z            ≈⟨ congʳ $ isBluebird W (C ∙ (B ∙ B ∙ x)) y ⟩
    W ∙ (C ∙ (B ∙ B ∙ x) ∙ y) ∙ z                ≈⟨ isWarbler (C ∙ (B ∙ B ∙ x) ∙ y) z ⟩
    C ∙ (B ∙ B ∙ x) ∙ y ∙ z ∙ z                  ≈⟨ congʳ $ isCardinal (B ∙ B ∙ x) y z ⟩
    B ∙ B ∙ x ∙ z ∙ y ∙ z                        ≈⟨ congʳ $ congʳ $ isBluebird B x z ⟩
    B ∙ (x ∙ z) ∙ y ∙ z                          ≈⟨ isBluebird (x ∙ z) y z ⟩
    x ∙ z ∙ (y ∙ z)                              ∎

  exercise₃ : ⦃ _ : HasStarling ⦄ ⦃ _ : HasBluebird ⦄ → HasPhoenix
  exercise₃ = record
    { Φ = B ∙ (B ∙ S) ∙ B
    ; isPhoenix = λ x y z w → begin
        B ∙ (B ∙ S) ∙ B ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird (B ∙ S) B x ⟩
        B ∙ S ∙ (B ∙ x) ∙ y ∙ z ∙ w      ≈⟨ congʳ $ congʳ $ isBluebird S (B ∙ x) y ⟩
        S ∙ (B ∙ x ∙ y) ∙ z ∙ w          ≈⟨ isStarling (B ∙ x ∙ y) z w ⟩
        B ∙ x ∙ y ∙ w ∙ (z ∙ w)          ≈⟨ congʳ $ isBluebird x y w ⟩
        x ∙ (y ∙ w) ∙ (z ∙ w)            ∎
    }

  exercise₄ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasWarbler ⦄ → HasPsiBird
  exercise₄ = record
    { Ψ = H* ∙ D₂
    ; isPsiBird = λ x y z w → begin
        H* ∙ D₂ ∙ x ∙ y ∙ z ∙ w     ≈⟨⟩
        B ∙ H ∙ D₂ ∙ x ∙ y ∙ z ∙ w  ≈⟨ congʳ $ congʳ $ congʳ $ isBluebird H D₂ x ⟩
        H ∙ (D₂ ∙ x) ∙ y ∙ z ∙ w    ≈⟨ congʳ $ isHummingbird (D₂ ∙ x) y z ⟩
        D₂ ∙ x ∙ y ∙ z ∙ y ∙ w      ≈⟨ isDovekie x y z y w ⟩
        x ∙ (y ∙ z) ∙ (y ∙ w)       ∎
    } where
    instance
      hasHummingbird = problem₁₀
      hasDovekie = Chapter₁₁.problem₁₁
    H* = B ∙ H

  -- NOTE: my copy of the book contains a mistake (looking at the given
  -- solutions): it says Γxyzwv = y(zw)(xywv) instead of Γxyzwv = y(zw)(xyzwv).
  exercise₅-a : ⦃ _ : HasPhoenix ⦄ ⦃ _ : HasBluebird ⦄
    → ∃[ Γ ] (∀ x y z w v → Γ ∙ x ∙ y ∙ z ∙ w ∙ v ≈ y ∙ (z ∙ w) ∙ (x ∙ y ∙ z ∙ w ∙ v))
  exercise₅-a =
    ( Φ ∙ (Φ ∙ (Φ ∙ B)) ∙ B
    , λ x y z w v → begin
        Φ ∙ (Φ ∙ (Φ ∙ B)) ∙ B ∙ x ∙ y ∙ z ∙ w ∙ v    ≈⟨ congʳ $ congʳ $ congʳ $ isPhoenix (Φ ∙ (Φ ∙ B)) B x y ⟩
        Φ ∙ (Φ ∙ B) ∙ (B ∙ y) ∙ (x ∙ y) ∙ z ∙ w ∙ v  ≈⟨ congʳ $ congʳ $ isPhoenix (Φ ∙ B) (B ∙ y) (x ∙ y) z ⟩
        Φ ∙ B ∙ (B ∙ y ∙ z) ∙ (x ∙ y ∙ z) ∙ w ∙ v    ≈⟨ congʳ $ isPhoenix B (B ∙ y ∙ z) (x ∙ y ∙ z) w ⟩
        B ∙ (B ∙ y ∙ z ∙ w) ∙ (x ∙ y ∙ z ∙ w) ∙ v    ≈⟨ isBluebird (B ∙ y ∙ z ∙ w) (x ∙ y ∙ z ∙ w) v ⟩
        B ∙ y ∙ z ∙ w ∙ (x ∙ y ∙ z ∙ w ∙ v)          ≈⟨ congʳ $ isBluebird y z w ⟩
        y ∙ (z ∙ w) ∙ (x ∙ y ∙ z ∙ w ∙ v)            ∎
    )

  exercise₅-b : ⦃ _ : HasKestrel ⦄
    → ∃[ Γ ] (∀ x y z w v → Γ ∙ x ∙ y ∙ z ∙ w ∙ v ≈ y ∙ (z ∙ w) ∙ (x ∙ y ∙ z ∙ w ∙ v))
    → HasPsiBird
  exercise₅-b (Γ , isΓ) = record
    { Ψ = Γ ∙ (K ∙ K)
    ; isPsiBird = λ x y z w → begin
        Γ ∙ (K ∙ K) ∙ x ∙ y ∙ z ∙ w            ≈⟨ isΓ (K ∙ K) x y z w ⟩
        x ∙ (y ∙ z) ∙ (K ∙ K ∙ x ∙ y ∙ z ∙ w)  ≈⟨ congˡ $ congʳ $ congʳ $ congʳ $ isKestrel K x ⟩
        x ∙ (y ∙ z) ∙ (K ∙ y ∙ z ∙ w)          ≈⟨ congˡ $ congʳ $ isKestrel y z ⟩
        x ∙ (y ∙ z) ∙ (y ∙ w)                  ∎
    }

  exercise₅ : ⦃ _ : HasPhoenix ⦄ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasKestrel ⦄ → HasPsiBird
  exercise₅ = exercise₅-b exercise₅-a

  exercise₆-a : ⦃ _ : HasStarling ⦄ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasThrush ⦄
    → ∃[ S′ ] (∀ x y z → S′ ∙ x ∙ y ∙ z ≈ y ∙ z ∙ (x ∙ z))
  exercise₆-a =
    ( C ∙ S
    , λ x y z → begin
        C ∙ S ∙ x ∙ y ∙ z  ≈⟨ congʳ $ isCardinal S x y ⟩
        S ∙ y ∙ x ∙ z      ≈⟨ isStarling y x z ⟩
        y ∙ z ∙ (x ∙ z)    ∎
    )
    where instance hasCardinal = Chapter₁₁.problem₂₁′

  exercise₆-b : ⦃ _ : HasIdentity ⦄
    → ∃[ S′ ] (∀ x y z → S′ ∙ x ∙ y ∙ z ≈ y ∙ z ∙ (x ∙ z))
    → HasWarbler
  exercise₆-b (S′ , isS′) = record
    { W = S′ ∙ I
    ; isWarbler = λ x y → begin
        S′ ∙ I ∙ x ∙ y   ≈⟨ isS′ I x y ⟩
        x ∙ y ∙ (I ∙ y)  ≈⟨ congˡ $ isIdentity y ⟩
        x ∙ y ∙ y        ∎
    }

  exercise₇ : ⦃ _ : HasQueerBird ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasWarbler ⦄
    → ∃[ Q̂ ] IsStarling (C ∙ Q̂ ∙ W)
  exercise₇ = let Q̂ = Q ∙ (Q ∙ Q ∙ (Q ∙ Q)) ∙ Q in
    ( Q̂
    , λ x y z → begin
        C ∙ Q̂ ∙ W ∙ x ∙ y ∙ z ≈⟨ congʳ $ congʳ $ isCardinal Q̂ W x ⟩
        Q̂ ∙ x ∙ W ∙ y ∙ z                          ≈⟨⟩
        Q ∙ (Q ∙ Q ∙ (Q ∙ Q)) ∙ Q ∙ x ∙ W ∙ y ∙ z  ≈⟨ congʳ $ congʳ $ congʳ $ isQueerBird (Q ∙ Q ∙ (Q ∙ Q)) Q  x ⟩
        Q ∙ (Q ∙ Q ∙ (Q ∙ Q) ∙ x) ∙ W ∙ y ∙ z      ≈⟨ congʳ $ isQueerBird (Q ∙ Q ∙ (Q ∙ Q) ∙ x) W y ⟩
        W ∙ (Q ∙ Q ∙ (Q ∙ Q) ∙ x ∙ y) ∙ z          ≈⟨ isWarbler (Q ∙ Q ∙ (Q ∙ Q) ∙ x ∙ y) z ⟩
        Q ∙ Q ∙ (Q ∙ Q) ∙ x ∙ y ∙ z ∙ z            ≈⟨ congʳ $ congʳ $ congʳ $ isQueerBird Q (Q ∙ Q) x ⟩
        Q ∙ Q ∙ (Q ∙ x) ∙ y ∙ z ∙ z                ≈⟨ congʳ $ congʳ $ isQueerBird Q (Q ∙ x) y ⟩
        Q ∙ x ∙ (Q ∙ y) ∙ z ∙ z                    ≈⟨ congʳ $ isQueerBird x (Q ∙ y) z ⟩
        Q ∙ y ∙ (x ∙ z) ∙ z                        ≈⟨ isQueerBird y (x ∙ z) z ⟩
        x ∙ z ∙ (y ∙ z)                            ∎
    )

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
module Syntax where

open import Data.List using (List; []; _∷_; _++_; lookup; length)
open import Data.Product using (Σ; Σ-syntax; proj₁; proj₂)
open import Data.Unit renaming (⊤ to top)
open import Data.Empty renaming (⊥ to bot)

open import Level using (suc; _⊔_)

module PType {ℓ} (Gr : Set ℓ) where
  infixr 10 _*_
  infixr 9 _=>_

  data Type : Set ℓ where
    ⌊_⌋ : Gr -> Type
    Unit : Type
    _*_ : Type -> Type -> Type
    _=>_ : Type -> Type -> Type

  record Sorting : Set ℓ where
    field
      dom : Type
      cod : Type

  Context : Set ℓ
  Context = List Type

record Signature ℓ₁ ℓ₂ : Set (suc (ℓ₁ ⊔ ℓ₂)) where
  field
    Gr : Set ℓ₁
    Func : Set ℓ₂

  open PType Gr public

  field
    sorting : Func -> Sorting

  dom : Func -> Type
  dom f = Sorting.dom (sorting f)

  cod : Func -> Type
  cod f = Sorting.cod (sorting f)

module Term {ℓ₁ ℓ₂} (Sg : Signature ℓ₁ ℓ₂) where
  open Signature Sg

  infix 3 _⊨_
  infix 8 _∙_

  infix 3 _⊢_
  infixl 4 _[_]

  data _⊨_ : Context -> Context -> Set (ℓ₁ ⊔ ℓ₂)
  data _⊢_ : Context -> Type -> Set (ℓ₁ ⊔ ℓ₂)

  data _⊨_ where
    id : forall {Γ} -> Γ ⊨ Γ  -- identity morphism
    _∙_ : forall {Γ Γ′ Γ′′} -> Γ′ ⊨ Γ′′ -> Γ ⊨ Γ′ -> Γ ⊨ Γ′′ -- composition of morphisms
    weaken : forall {Γ A} -> A ∷ Γ ⊨ Γ -- the first projection
    ext : forall {Γ Γ′ A} -> Γ ⊨ Γ′ -> Γ ⊢ A -> Γ ⊨ A ∷ Γ′ -- the unique morphism into the product
    ! : forall {Γ} -> Γ ⊨ [] -- the unique morphism into the terminal object

  data _⊢_ where
    func : forall {Γ} (f : Func) -> Γ ⊢ dom f -> Γ ⊢ cod f

    var : forall {Γ A} -> A ∷ Γ ⊢ A

    unit : forall {Γ} -> Γ ⊢ Unit

    pair : forall {Γ A B} -> Γ ⊢ A -> Γ ⊢ B -> Γ ⊢ A * B
    fst : forall {Γ A B} -> Γ ⊢ A * B -> Γ ⊢ A
    snd : forall {Γ A B} -> Γ ⊢ A * B -> Γ ⊢ B

    abs : forall {Γ A B} -> A ∷ Γ ⊢ B -> Γ ⊢ A => B
    app : forall {Γ A B} -> Γ ⊢ A => B -> Γ ⊢ A -> Γ ⊢ B

    _[_] : forall {Γ Γ′ A} -> Γ′ ⊢ A -> Γ ⊨ Γ′ -> Γ ⊢ A

  infix 10 _×id′

  _×id′ : forall {Γ Γ′} {A} -> Γ ⊨ Γ′ -> A ∷ Γ ⊨ A ∷ Γ′
  γ ×id′ = ext (γ ∙ weaken) var

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
-- Andreas, 2019-02-25, issue #3588
-- C-c C-r (refine) produces unqualified constructor, but only
-- a qualified constructor is accepted in this place.

-- {-# OPTIONS -v interaction.intro:100 #-}
-- {-# OPTIONS -v scope.inverse:100 #-}
-- {-# OPTIONS -v toConcrete:50 #-}

module Issue3588 where

module M (_ : Set₁) where

  data D : Set where
    c : D

  data P : D → Set where
    c : P c

open M Set using (D; P)
open M.D

test : P c
test = {!!}  -- C-c C-r

  -- "c" suggested by refine, but rejected by reload or give
  -- correct: P.c

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module LogicalFramework.NonIntuitionistic where

infix  6 ¬_
infixr 5 _∧_
infixr 4 _∨_

postulate
  ⊥      : Set
  ⊥-elim : {A : Set} → ⊥ → A

-- Disjunction.
postulate
  _∨_   : Set → Set → Set
  inj₁  : {A B : Set} → A → A ∨ B
  inj₂  : {A B : Set} → B → A ∨ B
  case  : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C

-- Conjunction.
postulate
  _∧_     : Set → Set → Set
  _,_     : {A B : Set} → A → B → A ∧ B
  ∧-proj₁ : {A B : Set} → A ∧ B → A
  ∧-proj₂ : {A B : Set} → A ∧ B → B

-- Negation.
-- The underscore allows to write for example '¬ ¬ A' instead of '¬ (¬ A)'.
¬_ : Set → Set
¬ A = A → ⊥

module pem→¬-elim where

  -- The principle of the excluded middle.
  postulate pem : ∀ {A} → A ∨ ¬ A

  -- The principle of indirect proof (proof by contradiction).
  ¬-elim : ∀ {A} → (¬ A → ⊥) → A
  ¬-elim h = case (λ a → a) (λ ¬a → ⊥-elim (h ¬a)) pem

module ¬-elim→pem where

  -- The principle of indirect proof (proof by contradiction).
  postulate ¬-elim : ∀ {A} → (¬ A → ⊥) → A

  helper₁ : {A : Set} → ¬ (A ∨ ¬ A) → ¬ A ∧ ¬ ¬ A
  helper₁ h = (λ a → h (inj₁ a)) , (λ ¬a → h (inj₂ ¬a))

  helper₂ : {A : Set} → ¬ A ∧ ¬ ¬ A → ⊥
  helper₂ h = ∧-proj₂ h (∧-proj₁ h)

  helper₃ : {A : Set} → ¬ (A ∨ ¬ A) → ⊥
  helper₃ h = helper₂ (helper₁ h)

  -- The principle of the excluded middle.
  pem : ∀ {A} → A ∨ ¬ A
  pem = ¬-elim helper₃

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Generalized variables in datatype (and record) parameters

module _ where

open import Agda.Primitive
open import Agda.Builtin.Nat

module NotParameterised where

  variable
    ℓ : Level
    A : Set ℓ
    x y : A
    m n : Nat

  data Vec (A : Set ℓ) : Nat → Set ℓ where
    []  : Vec A zero
    _∷_ : A → Vec A n → Vec A (suc n)

  variable
    xs : Vec A n

  -- n should be generalized as an index here
  data All (P : A → Set ℓ) : Vec A n → Set ℓ where
    []  : All P []
    _∷_ : P x → All P xs → All P (x ∷ xs)

  infix 2 _∈_
  -- need an occurrence of ℓ in the params to not generalize it as an index,
  -- so we bind A explicitly
  data _∈_ {A : Set ℓ} (x : A) : Vec A n → Set ℓ where
    zero : x ∈ x ∷ xs
    suc  : x ∈ xs → x ∈ y ∷ xs

  lookup : {P : A → Set ℓ} → All P xs → x ∈ xs → P x
  lookup (x ∷  _)  zero   = x
  lookup (_ ∷ xs) (suc i) = lookup xs i

-- Check that we can do the same in a parameterised module
module Parameterised (Dummy : Set) where

  variable
    ℓ : Level
    A : Set ℓ
    x y : A
    m n : Nat

  data Vec (A : Set ℓ) : Nat → Set ℓ where
    []  : Vec A zero
    _∷_ : A → Vec A n → Vec A (suc n)

  variable
    xs : Vec A n

  -- n should be generalized as an index here
  data All (P : A → Set ℓ) : Vec A n → Set ℓ where
    []  : All P []
    _∷_ : P x → All P xs → All P (x ∷ xs)

  infix 2 _∈_
  -- need an occurrence of ℓ in the params to not generalize it as an index,
  -- so we bind A explicitly
  data _∈_ {A : Set ℓ} (x : A) : Vec A n → Set ℓ where
    zero : x ∈ x ∷ xs
    suc  : x ∈ xs → x ∈ y ∷ xs

  lookup : {P : A → Set ℓ} → All P xs → x ∈ xs → P x
  lookup (x ∷  _)  zero   = x
  lookup (_ ∷ xs) (suc i) = lookup xs i


text:
-- {-# OPTIONS -v interaction.give:20 #-}

-- Reported by stevan.andjelkovic, Yesterday (17 hours ago)

-- Trying to give the expression in the goal gives the following error:

--   tt != tt p a of type Prop
--   when checking that the expression (λ x y → ?) has type
--   ({o : ⊤} (p : ⊤) → ⊥ → ⊤)

record _▷_ (I O : Set) : Set₁ where
  constructor _◃_/_
  field
    Parameter  : (o : O) → Set
    Arity      : ∀ {o} (p : Parameter o) → Set
    input      : ∀ {o} (p : Parameter o) (a : Arity p) → I

open _▷_ public

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

--data ⊤ : Set where
--  tt : ⊤

Abort : ⊤ ▷ ⊤
Abort = (λ _ → ⊤) ◃ (λ _ → ⊥) / {!!λ x y → {!!}!}


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

open import Level
open import Categories.Category
open import Categories.Product

module Categories.Product.Projections
    {o ℓ e o′ ℓ′ e′}
    (C : Category o ℓ e)
    (D : Category o′ ℓ′ e′)
    where

open import Categories.Functor
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)

∏₁ : Functor (Product C D) C
∏₁ = record
    { F₀            = proj₁
    ; F₁            = proj₁
    ; identity      = refl
    ; homomorphism  = refl
    ; F-resp-≡      = proj₁
    } where
        open Category.Equiv C

∏₂ : Functor (Product C D) D
∏₂ = record
    { F₀            = proj₂
    ; F₁            = proj₂
    ; identity      = refl
    ; homomorphism  = refl
    ; F-resp-≡      = proj₂
    } where
        open Category.Equiv D

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Cubical.Categories.Instances.Sets where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Unit
open import Cubical.Data.Sigma using (ΣPathP)
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation

open import Cubical.Categories.Limits

open Category

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

private
  variable
    ℓ ℓ' : Level

open Functor

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

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

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

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

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

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

-- SET is complete

-- notes:
-- didn't need to restrict to *finite* diagrams , why is that required in Set theoretic?
-- didn't use coinduction here because Agda didn't like me referencing 'cone' frome 'up' (termination check)

open NatTrans

isCompleteSET : ∀ {ℓJ ℓJ'} → complete' {ℓJ = ℓJ} {ℓJ'} (SET (ℓ-max ℓJ ℓJ'))
isCompleteSET J K = record
                  { head = head'
                  ; islim = record { cone = cone' ; up = up' } }
  where
    -- the limit is defined as the Set of all cones with head Unit
    head' = Cone K (Unit* , isOfHLevelLift 2 isSetUnit) , isSetNatTrans

    -- the legs are defined by taking a cone to its component at j
    cone' : Cone K head'
    cone' .N-ob j μ = (μ ⟦ j ⟧) tt*
    -- Naturality follows from naturality of the Unit cone
    cone' .N-hom {x = i} {j} f
      = funExt λ μ → (μ ⟦ j ⟧) tt*
        ≡[ i ]⟨ (μ .N-hom f i) tt* ⟩
          (K ⟪ f ⟫) ((μ ⟦ i ⟧) tt*)
        ∎

    -- Given another cone α, we want a unique function f from α → cone' which factors it
    -- factorization property enforces that (cone' ⟦ j ⟧ ● f) ≡ α ⟦ j ⟧
    -- but cone' ⟦ j ⟧ simply takes the jth component the output Cone K Unit from f
    -- so this enforces that for all x ∈ A, (f x) ⟦ j ⟧ ≡ α ⟦ j ⟧ x
    -- this determines the *only* possible factoring morphism
    up' : ∀ {A} (α : Cone K A) → cone' uniquelyFactors α
    up' {A} α = (f , fact) , unique
      where
        f : fst A → Cone K (Unit* , isOfHLevelLift 2 isSetUnit)
        f x = natTrans (λ j _ → α .N-ob j x)
                       (λ {m} {n} f → funExt λ μ i → α .N-hom f i x)

        fact : α ≡ (f ◼ cone')
        fact = makeNatTransPath refl -- I LOVE DEFINITIONAL EQUALITY

        unique : (τ : cone' factors α) → (f , fact) ≡ τ
        unique (f' , fact') = ΣPathP (f≡f' , fact≡fact')
          where
            f≡f' : f ≡ f'
            f≡f' = funExt λ x → makeNatTransPath (funExt λ _ → sym eq2)
              where
                -- the factorization property enforces that f' must have the same behavior as f
                eq1 : ∀ {x j} → ((cone' ⟦ j ⟧) (f' x)) ≡ (α ⟦ j ⟧) x
                eq1 {x} {j} i = ((fact' (~ i)) ⟦ j ⟧) x

                eq2 : ∀ {x j} → (f' x) ⟦ j ⟧ ≡ λ _ → (α ⟦ j ⟧) x -- = (f x) ⟦ j ⟧
                eq2 {x} {j} = funExt λ _ → eq1

            -- follows from Set having homsets
            fact≡fact' : PathP (λ i → α ≡ ((f≡f' i) ◼ cone')) fact fact'
            fact≡fact' = isOfHLevel→isOfHLevelDep 1 (λ β → isSetNatTrans α β) fact fact' λ i → (f≡f' i) ◼ cone'


text:
-- Andreas, 2014-01-09, extend parser of typed bindings to allow hiding

postulate
  _≡_   : ∀{A : Set} (a b : A) → Set
  List  : Set → Set
  _++_  : ∀{A : Set} (xs ys : List A) → List A
  assoc : ∀{A : Set} (xs {ys} {zs} : List A) → ((xs ++ ys) ++ zs) ≡ (xs ++ (ys ++ zs))
  assoc1 : ∀{A : Set} (xs {ys zs} : List A) → ((xs ++ ys) ++ zs) ≡ (xs ++ (ys ++ zs))
  test  : (xs {ys zs} _ us : Set) → Set
  test1 : .(xs {ys zs} _ us : Set) → Set
  test2 : ..(xs {ys zs} _ us : Set) → Set


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

module Data.Nat.Base where

open import Agda.Builtin.Nat public
  using (_+_; _*_; zero; suc)
  renaming (Nat to ℕ; _-_ to _∸_)

open import Level

data Ordering : ℕ → ℕ → Type where
  less    : ∀ m k → Ordering m (suc (m + k))
  equal   : ∀ m   → Ordering m m
  greater : ∀ m k → Ordering (suc (m + k)) m

compare : ∀ m n → Ordering m n
compare zero    zero    = equal   zero
compare (suc m) zero    = greater zero m
compare zero    (suc n) = less    zero n
compare (suc m) (suc n) with compare m n
... | less    m k = less (suc m) k
... | equal   m   = equal (suc m)
... | greater n k = greater (suc n) k


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Inference.Solver(x : X) where
  import OutsideIn.Inference.Separator as S
  import OutsideIn.Expressions as E
  import OutsideIn.Constraints as C
  open import Data.Bool renaming (_∧_ to _and_)
  open E(x)
  open S(x)
  open X(x)
  open C(x)

  private module PlusN-m {n} = Monad (PlusN-is-monad {n})
          module QC-f = Functor (qconstraint-is-functor)
          module Ax-f = Functor (axiomscheme-is-functor)
          module Type-f = Functor (type-is-functor)
          module Type-m = Monad (type-is-monad)

  mutual
    data _,_solvI►_ {x : Set}⦃ eq : Eq x ⦄(Q : AxiomScheme x)(Qg : QConstraint x) : {s : Shape} → Implications x s → Set where
      I-ε : Q , Qg solvI► imp-ε
      I-∧ : ∀ {r₁ r₂}{a : Implications x r₁}{b : Implications x r₂}
          → Q , Qg solvI► a → Q , Qg solvI► b → Q , Qg solvI► (a imp-∧ b)
      I-i : ∀ {r}{n}{Qv}{C : SeparatedConstraint _ r}{n′}{θ}
          → ( let peq = (PlusN-eq {n} eq) in  Q , Qg ∧ Qv , n solv► C ↝ n′ , ε , θ)
          → Q , Qg solvI► imp (∃ n · Qv ⊃ C)

    data _,_,_solv►_↝_,_,_ {x : Set}⦃ eq : Eq x ⦄(Q : AxiomScheme x)(Qg : QConstraint x)(n : ℕ) : {s : Shape} →
                        (SeparatedConstraint (x ⨁ n) s) → (m : ℕ) → (Qr : QConstraint (x ⨁ m)) → (θ : x ⨁ n → Type (x ⨁ m)) → Set where
      SOLVE : ∀ {s}{simpl}{imps : Implications _ s}{m}{Qr}{θ}
            → simplifier eq n Q Qg simpl ≡ m , Qr , solved Qr θ
            → let peq = (PlusN-eq {m} eq) in (Ax-f.map (PlusN-m.unit {m}) Q) , (Qr ∧ QC-f.map (PlusN-m.unit {m}) Qg) solvI► substituteImp θ imps
            → Q , Qg , n solv► SC simpl imps ↝ m , Qr , θ

  solveImps : {x : Set}{s : Shape} → (eq : Eq x) → (Q : AxiomScheme x) → (Qg : QConstraint x) → (C : Implications x s)
            → Ⓢ (Q , Qg solvI► C)
  solver′ : {x : Set}{s : Shape} → (eq : Eq x)
          → (n : ℕ) → (Q : AxiomScheme x) → (Qg : QConstraint x) →  (C : SeparatedConstraint (x ⨁ n) s)
          → Ⓢ (∃ (λ m → ∃ (λ θ →  Q , Qg , n solv► C ↝ m , ε , θ)))
  solver′  eq n axioms given (SC simpl imps) with simplifier eq n axioms given simpl | inspect (simplifier eq n axioms given) simpl
  ... | m , ε? , solved .ε? θ | iC prf with is-ε ε?
  solver′  eq n axioms given (SC simpl imps)
      | m , .ε , solved .ε θ | iC prf | yes refl = solveImps (PlusN-eq {m} eq)
                                                             (Ax-f.map (PlusN-m.unit {m}) axioms)
                                                             ( ε ∧ QC-f.map (PlusN-m.unit {m}) given)
                                                             (substituteImp θ imps)
                                               >>= λ impP →  suc (m , θ , SOLVE prf impP)
       where open Monad(Ⓢ-is-monad)
  ...                        | no isntε = zero
  solveImps eq Q Qg imp-ε = suc I-ε
  solveImps eq Q Qg (a imp-∧ b) = solveImps eq Q Qg a
                       >>= λ a′ → solveImps eq Q Qg b
                       >>= λ b′ → suc (I-∧ a′ b′)
       where open Monad(Ⓢ-is-monad)
  solveImps eq Q Qg (imp (∃ n · Qv ⊃ C)) = solver′ eq n Q (Qg ∧ Qv) C >>= λ { (m , θ , prf) → suc (I-i prf) }
       where open Monad(Ⓢ-is-monad)

  solver : {x : Set}{s : Shape} → (eq : Eq x)
         → (n : ℕ) → (Q : AxiomScheme x) → (Qg : QConstraint x) →  (C : SeparatedConstraint (x ⨁ n) s)
         → Ⓢ (∃ (λ m → ∃ (λ Qr → ∃ (λ θ →  Q , Qg , n solv► C ↝ m , Qr , θ))))
  solver eq n Q Qg (SC simpl imps) with simplifier eq n Q Qg simpl | inspect (simplifier eq n Q Qg) simpl
  ... | m , Qr , solved .Qr θ | iC prf = solveImps (PlusN-eq {m} eq)
                                                   (Ax-f.map (PlusN-m.unit {m}) Q)
                                                   (Qr ∧ QC-f.map (PlusN-m.unit {m}) Qg)
                                                   (substituteImp θ imps)
                                     >>= λ prf′ → suc (m , Qr , θ , SOLVE prf prf′)
       where open Monad(Ⓢ-is-monad)

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
module Data.Boolean.Proofs where

import      Lvl
open import Data
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Logic using (_⊼_ ; _⊽_ ; _⊕_)
open        Data.Boolean.Operators.Programming
open import Data.Either as Either using (_‖_ ; Left ; Right)
open import Functional
open import Logic.IntroInstances
open import Logic.Propositional as Logic using (_∨_ ; _∧_ ; ¬_ ; _↔_ ; [⊤]-intro ; [↔]-intro ; [⊥]-elim ; [↔]-to-[←] ; [↔]-to-[→])
open import Logic.Predicate
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Operator.Monoid
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Type

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}
private variable P : Bool → Type{ℓ}
private variable a b c t f : Bool
private variable x y : Bool
private variable pt pf : ∀{b} → P(b)

---------------------------------------------
-- Eliminator

module _ {pt pf : T} where
  elim-nested : (elim pt pf (elim t f b) ≡ elim{T = const T} (elim pt pf t) (elim pt pf f) b)
  elim-nested{t = t}{f = f}{b = b} = elim{T = b ↦ (elim pt pf (elim t f b) ≡ elim(elim pt pf t) (elim pt pf f) b)} [≡]-intro [≡]-intro b

module _ {x : T} where
  elim-redundant : (elim{T = const T} x x b ≡ x)
  elim-redundant{b = b} = elim{T = b ↦ elim x x b ≡ x} [≡]-intro [≡]-intro b

elim-inverse : (elim 𝑇 𝐹 b ≡ b)
elim-inverse{b = b} = elim{T = b ↦ elim 𝑇 𝐹 b ≡ b} [≡]-intro [≡]-intro b

elim-anti-inverse : (elim 𝐹 𝑇 b ≡ ! b)
elim-anti-inverse {𝑇} = [≡]-intro
elim-anti-inverse {𝐹} = [≡]-intro

---------------------------------------------
-- Negation

[!]-no-fixpoints : ∀{b} → (! b ≢ b)
[!]-no-fixpoints {𝑇} ()
[!]-no-fixpoints {𝐹} ()

[!!]-elim : ∀{a} → (!(! a) ≡ a)
[!!]-elim {𝑇} = [≡]-intro
[!!]-elim {𝐹} = [≡]-intro
{-# REWRITE [!!]-elim #-}

---------------------------------------------
-- Idempotence

[&&]-idempotence-raw : ∀{a} → (a && a ≡ a)
[&&]-idempotence-raw {𝑇} = [≡]-intro
[&&]-idempotence-raw {𝐹} = [≡]-intro
{-# REWRITE [&&]-idempotence-raw #-}
instance
  [&&]-idempotence : Idempotence(_&&_)
  Idempotence.proof([&&]-idempotence) = [&&]-idempotence-raw

[||]-idempotence-raw : ∀{a} → (a || a ≡ a)
[||]-idempotence-raw {𝑇} = [≡]-intro
[||]-idempotence-raw {𝐹} = [≡]-intro
{-# REWRITE [||]-idempotence-raw #-}
instance
  [||]-idempotence : Idempotence(_||_)
  Idempotence.proof([||]-idempotence) = [||]-idempotence-raw
---------------------------------------------
-- Left anti-identities

[==]-anti-identityₗ : ∀{a} → (𝐹 == a ≡ ! a)
[==]-anti-identityₗ {𝑇} = [≡]-intro
[==]-anti-identityₗ {𝐹} = [≡]-intro
{-# REWRITE [==]-anti-identityₗ #-}

[!=]-anti-identityₗ : ∀{a} → (𝑇 != a ≡ ! a)
[!=]-anti-identityₗ {𝑇} = [≡]-intro
[!=]-anti-identityₗ {𝐹} = [≡]-intro
{-# REWRITE [!=]-anti-identityₗ #-}

---------------------------------------------
-- Right anti-identities

[==]-anti-identityᵣ : ∀{a} → (a == 𝐹 ≡ ! a)
[==]-anti-identityᵣ {𝑇} = [≡]-intro
[==]-anti-identityᵣ {𝐹} = [≡]-intro
{-# REWRITE [==]-anti-identityᵣ #-}

[!=]-anti-identityᵣ : ∀{a} → (a != 𝑇 ≡ ! a)
[!=]-anti-identityᵣ {𝑇} = [≡]-intro
[!=]-anti-identityᵣ {𝐹} = [≡]-intro
{-# REWRITE [!=]-anti-identityᵣ #-}

---------------------------------------------
-- Left identities

[||]-identityₗ-raw : ∀{a} → (𝐹 || a ≡ a)
[||]-identityₗ-raw {𝑇} = [≡]-intro
[||]-identityₗ-raw {𝐹} = [≡]-intro
{-# REWRITE [||]-identityₗ-raw #-}
instance
  [||]-identityₗ : Identityₗ(_||_)(𝐹)
  Identityₗ.proof([||]-identityₗ) = [||]-identityₗ-raw

[&&]-identityₗ-raw : ∀{a} → (𝑇 && a ≡ a)
[&&]-identityₗ-raw {𝑇} = [≡]-intro
[&&]-identityₗ-raw {𝐹} = [≡]-intro
{-# REWRITE [&&]-identityₗ-raw #-}
instance
  [&&]-identityₗ : Identityₗ(_&&_)(𝑇)
  Identityₗ.proof([&&]-identityₗ) = [&&]-identityₗ-raw

[==]-identityₗ-raw : ∀{a} → (𝑇 == a ≡ a)
[==]-identityₗ-raw {𝑇} = [≡]-intro
[==]-identityₗ-raw {𝐹} = [≡]-intro
{-# REWRITE [==]-identityₗ-raw #-}
instance
  [==]-identityₗ : Identityₗ(_==_)(𝑇)
  Identityₗ.proof([==]-identityₗ) = [==]-identityₗ-raw

[!=]-identityₗ-raw : ∀{a} → (𝐹 != a ≡ a)
[!=]-identityₗ-raw {𝑇} = [≡]-intro
[!=]-identityₗ-raw {𝐹} = [≡]-intro
{-# REWRITE [!=]-identityₗ-raw #-}
instance
  [!=]-identityₗ : Identityₗ(_!=_)(𝐹)
  Identityₗ.proof([!=]-identityₗ) = [!=]-identityₗ-raw

---------------------------------------------
-- Left absorbers

[||]-absorberₗ-raw : ∀{a} → (𝑇 || a ≡ 𝑇)
[||]-absorberₗ-raw {𝑇} = [≡]-intro
[||]-absorberₗ-raw {𝐹} = [≡]-intro
{-# REWRITE [||]-absorberₗ-raw #-}
instance
  [||]-absorberₗ : Absorberₗ(_||_)(𝑇)
  Absorberₗ.proof([||]-absorberₗ) {a} = [||]-absorberₗ-raw {a}

[&&]-absorberₗ-raw : ∀{a} → (𝐹 && a ≡ 𝐹)
[&&]-absorberₗ-raw {𝑇} = [≡]-intro
[&&]-absorberₗ-raw {𝐹} = [≡]-intro
{-# REWRITE [&&]-absorberₗ-raw #-}
instance
  [&&]-absorberₗ : Absorberₗ(_&&_)(𝐹)
  Absorberₗ.proof([&&]-absorberₗ) {a} = [&&]-absorberₗ-raw {a}

---------------------------------------------
-- Right identities

[||]-identityᵣ-raw : ∀{a} → (a || 𝐹 ≡ a)
[||]-identityᵣ-raw {𝑇} = [≡]-intro
[||]-identityᵣ-raw {𝐹} = [≡]-intro
{-# REWRITE [||]-identityᵣ-raw #-}
instance
  [||]-identityᵣ : Identityᵣ(_||_)(𝐹)
  Identityᵣ.proof([||]-identityᵣ) = [||]-identityᵣ-raw

[&&]-identityᵣ-raw : ∀{a} → (a && 𝑇 ≡ a)
[&&]-identityᵣ-raw {𝑇} = [≡]-intro
[&&]-identityᵣ-raw {𝐹} = [≡]-intro
{-# REWRITE [&&]-identityᵣ-raw #-}
instance
  [&&]-identityᵣ : Identityᵣ(_&&_)(𝑇)
  Identityᵣ.proof([&&]-identityᵣ) = [&&]-identityᵣ-raw

[==]-identityᵣ-raw : ∀{a} → (a == 𝑇 ≡ a)
[==]-identityᵣ-raw {𝑇} = [≡]-intro
[==]-identityᵣ-raw {𝐹} = [≡]-intro
{-# REWRITE [==]-identityᵣ-raw #-}
instance
  [==]-identityᵣ : Identityᵣ(_==_)(𝑇)
  Identityᵣ.proof([==]-identityᵣ) = [==]-identityᵣ-raw

[!=]-identityᵣ-raw : ∀{a} → (a != 𝐹 ≡ a)
[!=]-identityᵣ-raw {𝑇} = [≡]-intro
[!=]-identityᵣ-raw {𝐹} = [≡]-intro
{-# REWRITE [!=]-identityᵣ-raw #-}
instance
  [!=]-identityᵣ : Identityᵣ(_!=_)(𝐹)
  Identityᵣ.proof([!=]-identityᵣ) = [!=]-identityᵣ-raw

---------------------------------------------
-- Identities

instance
  [||]-identity : Identity(_||_)(𝐹)
  [||]-identity = record{}

instance
  [&&]-identity : Identity(_&&_)(𝑇)
  [&&]-identity = record{}

instance
  [==]-identity : Identity(_==_)(𝑇)
  [==]-identity = record{}

instance
  [!=]-identity : Identity(_!=_)(𝐹)
  [!=]-identity = record{}

---------------------------------------------
-- Right absorbers

[||]-absorberᵣ-raw : ∀{a} → (a || 𝑇 ≡ 𝑇)
[||]-absorberᵣ-raw {𝑇} = [≡]-intro
[||]-absorberᵣ-raw {𝐹} = [≡]-intro
{-# REWRITE [||]-absorberᵣ-raw #-}
instance
  [||]-absorberᵣ : Absorberᵣ(_||_)(𝑇)
  Absorberᵣ.proof([||]-absorberᵣ) {a} = [||]-absorberᵣ-raw {a}

[&&]-absorberᵣ-raw : ∀{a} → (a && 𝐹 ≡ 𝐹)
[&&]-absorberᵣ-raw {𝑇} = [≡]-intro
[&&]-absorberᵣ-raw {𝐹} = [≡]-intro
{-# REWRITE [&&]-absorberᵣ-raw #-}
instance
  [&&]-absorberᵣ : Absorberᵣ(_&&_)(𝐹)
  Absorberᵣ.proof([&&]-absorberᵣ) {a} = [&&]-absorberᵣ-raw {a}

---------------------------------------------
-- Associativity

instance
  [||]-associativity : Associativity(_||_)
  Associativity.proof([||]-associativity) = proof where
    proof : Names.Associativity(_||_)
    proof {𝑇}{𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝑇}{𝐹} = [≡]-intro
    proof {𝑇}{𝐹}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇}{𝑇} = [≡]-intro
    proof {𝐹}{𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹}{𝐹} = [≡]-intro

instance
  [&&]-associativity : Associativity(_&&_)
  Associativity.proof([&&]-associativity) = proof where
    proof : Names.Associativity(_&&_)
    proof {𝑇}{𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝑇}{𝐹} = [≡]-intro
    proof {𝑇}{𝐹}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇}{𝑇} = [≡]-intro
    proof {𝐹}{𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹}{𝐹} = [≡]-intro

instance
  [==]-associativity : Associativity(_==_)
  Associativity.proof([==]-associativity) = proof where
    proof : Names.Associativity(_==_)
    proof {𝑇}{𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝑇}{𝐹} = [≡]-intro
    proof {𝑇}{𝐹}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇}{𝑇} = [≡]-intro
    proof {𝐹}{𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹}{𝐹} = [≡]-intro

instance
  [!=]-associativity : Associativity(_!=_)
  Associativity.proof([!=]-associativity) = proof where
    proof : Names.Associativity(_!=_)
    proof {𝑇}{𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝑇}{𝐹} = [≡]-intro
    proof {𝑇}{𝐹}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇}{𝑇} = [≡]-intro
    proof {𝐹}{𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹}{𝐹} = [≡]-intro

---------------------------------------------
-- Other

[⊼]-pseudo-associativity : (!(a ⊼ b) ⊼ c ≡ a ⊼ !(b ⊼ c))
[⊼]-pseudo-associativity {𝑇} {𝑇} {𝑇} = [≡]-intro
[⊼]-pseudo-associativity {𝑇} {𝑇} {𝐹} = [≡]-intro
[⊼]-pseudo-associativity {𝑇} {𝐹} {𝑇} = [≡]-intro
[⊼]-pseudo-associativity {𝑇} {𝐹} {𝐹} = [≡]-intro
[⊼]-pseudo-associativity {𝐹} {𝑇} {𝑇} = [≡]-intro
[⊼]-pseudo-associativity {𝐹} {𝑇} {𝐹} = [≡]-intro
[⊼]-pseudo-associativity {𝐹} {𝐹} {𝑇} = [≡]-intro
[⊼]-pseudo-associativity {𝐹} {𝐹} {𝐹} = [≡]-intro

[⊼]-to-conjunction : (!(a ⊼ b) ≡ a && b)
[⊼]-to-conjunction {𝑇} {𝑇} = [≡]-intro
[⊼]-to-conjunction {𝑇} {𝐹} = [≡]-intro
[⊼]-to-conjunction {𝐹} {𝑇} = [≡]-intro
[⊼]-to-conjunction {𝐹} {𝐹} = [≡]-intro

[⊼]-to-negation : (b ⊼ b ≡ ! b)
[⊼]-to-negation {𝑇} = [≡]-intro
[⊼]-to-negation {𝐹} = [≡]-intro

[⊼]-pseudo-absorptionₗ : (a ⊼ (a ⊼ b) ≡ a ⊼ (! b))
[⊼]-pseudo-absorptionₗ {𝑇} {𝑇} = [≡]-intro
[⊼]-pseudo-absorptionₗ {𝑇} {𝐹} = [≡]-intro
[⊼]-pseudo-absorptionₗ {𝐹} {𝑇} = [≡]-intro
[⊼]-pseudo-absorptionₗ {𝐹} {𝐹} = [≡]-intro

[⊼]-pseudo-absorptionᵣ : ((a ⊼ b) ⊼ b ≡ (! a) ⊼ b)
[⊼]-pseudo-absorptionᵣ {𝑇} {𝑇} = [≡]-intro
[⊼]-pseudo-absorptionᵣ {𝑇} {𝐹} = [≡]-intro
[⊼]-pseudo-absorptionᵣ {𝐹} {𝑇} = [≡]-intro
[⊼]-pseudo-absorptionᵣ {𝐹} {𝐹} = [≡]-intro

[⊼]-pseudo-pseudo-absorptionₗ : (((! a) ⊼ b) ⊼ (a ⊼ b) ≡ b)
[⊼]-pseudo-pseudo-absorptionₗ {𝑇} {𝑇} = [≡]-intro
[⊼]-pseudo-pseudo-absorptionₗ {𝑇} {𝐹} = [≡]-intro
[⊼]-pseudo-pseudo-absorptionₗ {𝐹} {𝑇} = [≡]-intro
[⊼]-pseudo-pseudo-absorptionₗ {𝐹} {𝐹} = [≡]-intro

[⊼]-pseudo-pseudo-absorptionᵣ : ((a ⊼ (! b)) ⊼ (a ⊼ b) ≡ a)
[⊼]-pseudo-pseudo-absorptionᵣ {𝑇} {𝑇} = [≡]-intro
[⊼]-pseudo-pseudo-absorptionᵣ {𝑇} {𝐹} = [≡]-intro
[⊼]-pseudo-pseudo-absorptionᵣ {𝐹} {𝑇} = [≡]-intro
[⊼]-pseudo-pseudo-absorptionᵣ {𝐹} {𝐹} = [≡]-intro

[⊽]-pseudo-associativity : (!(a ⊽ b) ⊽ c ≡ a ⊽ !(b ⊽ c))
[⊽]-pseudo-associativity {𝑇} {𝑇} {𝑇} = [≡]-intro
[⊽]-pseudo-associativity {𝑇} {𝑇} {𝐹} = [≡]-intro
[⊽]-pseudo-associativity {𝑇} {𝐹} {𝑇} = [≡]-intro
[⊽]-pseudo-associativity {𝑇} {𝐹} {𝐹} = [≡]-intro
[⊽]-pseudo-associativity {𝐹} {𝑇} {𝑇} = [≡]-intro
[⊽]-pseudo-associativity {𝐹} {𝑇} {𝐹} = [≡]-intro
[⊽]-pseudo-associativity {𝐹} {𝐹} {𝑇} = [≡]-intro
[⊽]-pseudo-associativity {𝐹} {𝐹} {𝐹} = [≡]-intro

[⊽]-to-disjunction : (!(a ⊽ b) ≡ a || b)
[⊽]-to-disjunction {𝑇} {𝑇} = [≡]-intro
[⊽]-to-disjunction {𝑇} {𝐹} = [≡]-intro
[⊽]-to-disjunction {𝐹} {𝑇} = [≡]-intro
[⊽]-to-disjunction {𝐹} {𝐹} = [≡]-intro

[⊽]-to-negation : (b ⊽ b ≡ ! b)
[⊽]-to-negation {𝑇} = [≡]-intro
[⊽]-to-negation {𝐹} = [≡]-intro

[⊽]-pseudo-absorptionₗ : (a ⊽ (a ⊽ b) ≡ a ⊽ (! b))
[⊽]-pseudo-absorptionₗ {𝑇} {𝑇} = [≡]-intro
[⊽]-pseudo-absorptionₗ {𝑇} {𝐹} = [≡]-intro
[⊽]-pseudo-absorptionₗ {𝐹} {𝑇} = [≡]-intro
[⊽]-pseudo-absorptionₗ {𝐹} {𝐹} = [≡]-intro

[⊽]-pseudo-absorptionᵣ : ((a ⊽ b) ⊽ b ≡ (! a) ⊽ b)
[⊽]-pseudo-absorptionᵣ {𝑇} {𝑇} = [≡]-intro
[⊽]-pseudo-absorptionᵣ {𝑇} {𝐹} = [≡]-intro
[⊽]-pseudo-absorptionᵣ {𝐹} {𝑇} = [≡]-intro
[⊽]-pseudo-absorptionᵣ {𝐹} {𝐹} = [≡]-intro

[⊽]-pseudo-pseudo-absorptionₗ : (((! a) ⊽ b) ⊽ (a ⊽ b) ≡ b)
[⊽]-pseudo-pseudo-absorptionₗ {𝑇} {𝑇} = [≡]-intro
[⊽]-pseudo-pseudo-absorptionₗ {𝑇} {𝐹} = [≡]-intro
[⊽]-pseudo-pseudo-absorptionₗ {𝐹} {𝑇} = [≡]-intro
[⊽]-pseudo-pseudo-absorptionₗ {𝐹} {𝐹} = [≡]-intro

[⊽]-pseudo-pseudo-absorptionᵣ : ((a ⊽ (! b)) ⊽ (a ⊽ b) ≡ a)
[⊽]-pseudo-pseudo-absorptionᵣ {𝑇} {𝑇} = [≡]-intro
[⊽]-pseudo-pseudo-absorptionᵣ {𝑇} {𝐹} = [≡]-intro
[⊽]-pseudo-pseudo-absorptionᵣ {𝐹} {𝑇} = [≡]-intro
[⊽]-pseudo-pseudo-absorptionᵣ {𝐹} {𝐹} = [≡]-intro

---------------------------------------------
-- Commutativity

instance
  [||]-commutativity : Commutativity(_||_)
  Commutativity.proof([||]-commutativity) = proof where
    proof : Names.Commutativity(_||_)
    proof {𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹} = [≡]-intro

instance
  [&&]-commutativity : Commutativity(_&&_)
  Commutativity.proof([&&]-commutativity) = proof where
    proof : Names.Commutativity(_&&_)
    proof {𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹} = [≡]-intro

instance
  [==]-commutativity : Commutativity(_==_)
  Commutativity.proof([==]-commutativity) = proof where
    proof : Names.Commutativity(_==_)
    proof {𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹} = [≡]-intro

instance
  [!=]-commutativity : Commutativity(_!=_)
  Commutativity.proof([!=]-commutativity) = proof where
    proof : Names.Commutativity(_!=_)
    proof {𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹} = [≡]-intro

instance
  [⊼]-commutativity : Commutativity(_⊼_)
  Commutativity.proof([⊼]-commutativity) = proof where
    proof : Names.Commutativity(_⊼_)
    proof {𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹} = [≡]-intro

instance
  [⊽]-commutativity : Commutativity(_⊽_)
  Commutativity.proof([⊽]-commutativity) = proof where
    proof : Names.Commutativity(_⊽_)
    proof {𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹} = [≡]-intro

instance
  [⊕]-commutativity : Commutativity(_⊕_)
  Commutativity.proof([⊕]-commutativity) = proof where
    proof : Names.Commutativity(_⊕_)
    proof {𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹} = [≡]-intro

instance
  [&&][||]-distributivityₗ : Distributivityₗ(_&&_)(_||_)
  Distributivityₗ.proof([&&][||]-distributivityₗ) = proof where
    proof : Names.Distributivityₗ(_&&_)(_||_)
    proof {𝑇}{𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝑇}{𝐹} = [≡]-intro
    proof {𝑇}{𝐹}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇}{𝑇} = [≡]-intro
    proof {𝐹}{𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹}{𝐹} = [≡]-intro

instance
  [||][&&]-distributivityₗ : Distributivityₗ(_||_)(_&&_)
  Distributivityₗ.proof([||][&&]-distributivityₗ) = proof where
    proof : Names.Distributivityₗ(_||_)(_&&_)
    proof {𝑇}{𝑇}{𝑇} = [≡]-intro
    proof {𝑇}{𝑇}{𝐹} = [≡]-intro
    proof {𝑇}{𝐹}{𝑇} = [≡]-intro
    proof {𝑇}{𝐹}{𝐹} = [≡]-intro
    proof {𝐹}{𝑇}{𝑇} = [≡]-intro
    proof {𝐹}{𝑇}{𝐹} = [≡]-intro
    proof {𝐹}{𝐹}{𝑇} = [≡]-intro
    proof {𝐹}{𝐹}{𝐹} = [≡]-intro

instance
  [||]-oppositeFunctionₗ : ComplementFunctionₗ(_||_)(!)
  ComplementFunctionₗ.proof([||]-oppositeFunctionₗ) = proof where
    proof : Names.InverseFunctionₗ(_||_)(𝑇)(!)
    proof {𝑇} = [≡]-intro
    proof {𝐹} = [≡]-intro

instance
  [||]-oppositeFunctionᵣ : ComplementFunctionᵣ(_||_)(!)
  ComplementFunctionᵣ.proof([||]-oppositeFunctionᵣ) = proof where
    proof : Names.InverseFunctionᵣ(_||_)(𝑇)(!)
    proof {𝑇} = [≡]-intro
    proof {𝐹} = [≡]-intro

instance
  [&&]-oppositeFunctionₗ : ComplementFunctionₗ(_&&_)(!)
  ComplementFunctionₗ.proof([&&]-oppositeFunctionₗ) = proof where
    proof : Names.InverseFunctionₗ(_&&_)(𝐹)(!)
    proof {𝑇} = [≡]-intro
    proof {𝐹} = [≡]-intro

instance
  [&&]-oppositeFunctionᵣ : ComplementFunctionᵣ(_&&_)(!)
  ComplementFunctionᵣ.proof([&&]-oppositeFunctionᵣ) = proof where
    proof : Names.InverseFunctionᵣ(_&&_)(𝐹)(!)
    proof {𝑇} = [≡]-intro
    proof {𝐹} = [≡]-intro

---------------------------------------------
-- Algebraic structures

instance
  [&&]-monoid : Monoid(_&&_)
  [&&]-monoid = record{}

instance
  [||]-monoid : Monoid(_||_)
  [||]-monoid = record{}

instance
  [==]-monoid : Monoid(_==_)
  [==]-monoid = record{}

instance
  [!=]-monoid : Monoid(_!=_)
  [!=]-monoid = record{}

-- TODO: Set algebra

---------------------------------------------
-- Inverting

inverted-[==][!=] : ∀{a b} → (!(a == b) ≡ (a != b))
inverted-[==][!=] {𝑇}{𝑇} = [≡]-intro
inverted-[==][!=] {𝑇}{𝐹} = [≡]-intro
inverted-[==][!=] {𝐹}{𝑇} = [≡]-intro
inverted-[==][!=] {𝐹}{𝐹} = [≡]-intro

inverted-[!=][==] : ∀{a b} → (!(a != b) ≡ (a == b))
inverted-[!=][==] {𝑇}{𝑇} = [≡]-intro
inverted-[!=][==] {𝑇}{𝐹} = [≡]-intro
inverted-[!=][==] {𝐹}{𝑇} = [≡]-intro
inverted-[!=][==] {𝐹}{𝐹} = [≡]-intro

---------------------------------------------
-- Rules of classical logic

-- A boolean operation is either true or false
bivalence : ∀{a} → ((a ≡ 𝑇) ∨ (a ≡ 𝐹))
bivalence {𝑇} = Logic.[∨]-introₗ [≡]-intro
bivalence {𝐹} = Logic.[∨]-introᵣ [≡]-intro

-- A boolean operation is not both true and false at the same time
disjointness : ∀{a} → ¬((a ≡ 𝑇) ∧ (a ≡ 𝐹))
disjointness {𝑇} (Logic.[∧]-intro [≡]-intro ())
disjointness {𝐹} (Logic.[∧]-intro () [≡]-intro)

[→?]-disjunctive-form : ∀{a b} → ((a →? b) ≡ ((! a) || b))
[→?]-disjunctive-form {𝑇} {𝑇} = [≡]-intro
[→?]-disjunctive-form {𝑇} {𝐹} = [≡]-intro
[→?]-disjunctive-form {𝐹} {𝑇} = [≡]-intro
[→?]-disjunctive-form {𝐹} {𝐹} = [≡]-intro

[==]-disjunctive-form : ∀{a b} → ((a == b) ≡ ((a && b) || ((! a) && (! b))))
[==]-disjunctive-form {𝑇} {𝑇} = [≡]-intro
[==]-disjunctive-form {𝑇} {𝐹} = [≡]-intro
[==]-disjunctive-form {𝐹} {𝑇} = [≡]-intro
[==]-disjunctive-form {𝐹} {𝐹} = [≡]-intro

module 𝑇 where
  [∧]-intro : ∀{a b} → (a ≡ 𝑇) → (b ≡ 𝑇) → ((a && b) ≡ 𝑇)
  [∧]-intro [≡]-intro [≡]-intro = [≡]-intro

  [∨]-introₗ : ∀{a b} → (a ≡ 𝑇) → ((a || b) ≡ 𝑇)
  [∨]-introₗ {_}{𝑇} [≡]-intro = [≡]-intro
  [∨]-introₗ {_}{𝐹} [≡]-intro = [≡]-intro

  [∨]-introᵣ : ∀{a b} → (b ≡ 𝑇) → ((a || b) ≡ 𝑇)
  [∨]-introᵣ {𝑇}{_} [≡]-intro = [≡]-intro
  [∨]-introᵣ {𝐹}{_} [≡]-intro = [≡]-intro

  [∧]-elimₗ : ∀{a b} → ((a && b) ≡ 𝑇) → (a ≡ 𝑇)
  [∧]-elimₗ {𝑇}{𝑇} [≡]-intro = [≡]-intro
  [∧]-elimₗ {𝑇}{𝐹} ()
  [∧]-elimₗ {𝐹}{𝑇} ()
  [∧]-elimₗ {𝐹}{𝐹} ()

  [∧]-elimᵣ : ∀{a b} → ((a && b) ≡ 𝑇) → (b ≡ 𝑇)
  [∧]-elimᵣ {𝑇}{𝑇} [≡]-intro = [≡]-intro
  [∧]-elimᵣ {𝑇}{𝐹} ()
  [∧]-elimᵣ {𝐹}{𝑇} ()
  [∧]-elimᵣ {𝐹}{𝐹} ()

  [∨]-elim : ∀{a b}{ℓ₂}{φ : Type{ℓ₂}} → ((a ≡ 𝑇) → φ) → ((b ≡ 𝑇) → φ) → ((a || b) ≡ 𝑇) → φ
  [∨]-elim {𝑇}{𝑇}{_} f _ [≡]-intro = f [≡]-intro
  [∨]-elim {𝑇}{𝐹}{_} f _ [≡]-intro = f [≡]-intro
  [∨]-elim {𝐹}{𝑇}{_} _ f [≡]-intro = f [≡]-intro
  [∨]-elim {𝐹}{𝐹}{_} _ f ()

  [¬]-intro : ∀{a} → (a ≡ 𝐹) → (! a ≡ 𝑇)
  [¬]-intro [≡]-intro = [≡]-intro

  [¬]-elim : ∀{a} → (! a ≡ 𝑇) → (a ≡ 𝐹)
  [¬]-elim {𝑇} ()
  [¬]-elim {𝐹} [≡]-intro = [≡]-intro

  [¬¬]-elim : ∀{a} → (!(! a) ≡ 𝑇) → (a ≡ 𝑇)
  [¬¬]-elim {𝑇} [≡]-intro = [≡]-intro
  [¬¬]-elim {𝐹} ()

  preserves-[&&][∧] : ∀{a b} → ((a && b) ≡ 𝑇) ↔ (a ≡ 𝑇)∧(b ≡ 𝑇)
  preserves-[&&][∧] = [↔]-intro
    (\{(Logic.[∧]-intro l r) → [∧]-intro l r})
    (proof ↦ Logic.[∧]-intro ([∧]-elimₗ proof) ([∧]-elimᵣ proof))

  preserves-[||][∨] : ∀{a b} → ((a || b) ≡ 𝑇) ↔ (a ≡ 𝑇)∨(b ≡ 𝑇)
  preserves-[||][∨] = [↔]-intro
    (Logic.[∨]-elim [∨]-introₗ [∨]-introᵣ)
    ([∨]-elim Logic.[∨]-introₗ Logic.[∨]-introᵣ)

  preserves-[!][¬] : ∀{a} → (! a ≡ 𝑇) ↔ ¬(a ≡ 𝑇)
  preserves-[!][¬] {a} = [↔]-intro (l{a}) (r{a}) where
    l : ∀{a} → (! a ≡ 𝑇) ← ¬(a ≡ 𝑇)
    l {𝐹} _ = [≡]-intro
    l {𝑇} f = [⊥]-elim (f [≡]-intro)

    r : ∀{a} → (! a ≡ 𝑇) → ¬(a ≡ 𝑇)
    r {𝑇} () _
    r {𝐹} _ ()

  [≡]-transfer : ∀{a b} → ((a == b) ≡ 𝑇) ↔ (a ≡ b)
  [≡]-transfer {𝑇}{𝑇} = [↔]-intro (_ ↦ [≡]-intro) (_ ↦ [≡]-intro)
  [≡]-transfer {𝐹}{𝑇} = [↔]-intro (\()) (\())
  [≡]-transfer {𝑇}{𝐹} = [↔]-intro (\()) (\())
  [≡]-transfer {𝐹}{𝐹} = [↔]-intro (_ ↦ [≡]-intro) (_ ↦ [≡]-intro)

  [≢]-transfer : ∀{a b} → ((a != b) ≡ 𝑇) ↔ (a ≢ b)
  [≢]-transfer {𝑇}{𝑇} = [↔]-intro (ab ↦ [⊥]-elim(ab [≡]-intro)) (\())
  [≢]-transfer {𝐹}{𝑇} = [↔]-intro (_ ↦ [≡]-intro) (_ ↦ \())
  [≢]-transfer {𝑇}{𝐹} = [↔]-intro (_ ↦ [≡]-intro) (_ ↦ \())
  [≢]-transfer {𝐹}{𝐹} = [↔]-intro (ab ↦ [⊥]-elim(ab [≡]-intro)) (\())

module 𝐹 where
  [∧]-introₗ : ∀{a b} → (a ≡ 𝐹) → ((a && b) ≡ 𝐹)
  [∧]-introₗ {_}{𝑇} [≡]-intro = [≡]-intro
  [∧]-introₗ {_}{𝐹} [≡]-intro = [≡]-intro

  [∧]-introᵣ : ∀{a b} → (b ≡ 𝐹) → ((a && b) ≡ 𝐹)
  [∧]-introᵣ {𝑇}{_} [≡]-intro = [≡]-intro
  [∧]-introᵣ {𝐹}{_} [≡]-intro = [≡]-intro

  [∨]-intro : ∀{a b} → (a ≡ 𝐹) → (b ≡ 𝐹) → ((a || b) ≡ 𝐹)
  [∨]-intro [≡]-intro [≡]-intro = [≡]-intro

  [¬]-intro : ∀{a} → (! a ≡ 𝑇) → (a ≡ 𝐹)
  [¬]-intro = 𝑇.[¬]-elim

  [¬]-elim : ∀{a} → (a ≡ 𝐹) → (! a ≡ 𝑇)
  [¬]-elim = 𝑇.[¬]-intro

[≢][𝑇]-is-[𝐹] : ∀{a} → (a ≢ 𝑇) ↔ (a ≡ 𝐹)
[≢][𝑇]-is-[𝐹] {a} = [↔]-intro (l{a}) (r{a}) where
  r : ∀{a} → (a ≢ 𝑇) → (a ≡ 𝐹)
  r {𝑇} (a≢𝑇) = [⊥]-elim ((a≢𝑇) ([≡]-intro))
  r {𝐹} (a≢𝑇) = [≡]-intro

  l : ∀{a} → (a ≢ 𝑇) ← (a ≡ 𝐹)
  l {𝑇} ()
  l {𝐹} (a≡𝐹) ()

[≢][𝐹]-is-[𝑇] : ∀{a} → (a ≢ 𝐹) ↔ (a ≡ 𝑇)
[≢][𝐹]-is-[𝑇] {a} = [↔]-intro (l{a}) (r{a}) where
  r : ∀{a} → (a ≢ 𝐹) → (a ≡ 𝑇)
  r {𝑇} (a≢𝐹) = [≡]-intro
  r {𝐹} (a≢𝐹) = [⊥]-elim ((a≢𝐹) ([≡]-intro))

  l : ∀{a} → (a ≢ 𝐹) ← (a ≡ 𝑇)
  l {𝑇} (a≡𝑇) ()
  l {𝐹} ()

---------------------------------------------
-- If-statements

module _ {ℓ₁ ℓ₂} {T : Type{ℓ₁}} {x y : T} {P : T → Type{ℓ₂}} where
  if-intro : ∀{B} → ((B ≡ 𝑇) → P(x)) → ((B ≡ 𝐹) → P(y)) → P(if B then x else y)
  if-intro {𝑇} px py = px [≡]-intro
  if-intro {𝐹} px py = py [≡]-intro

module _ {ℓ₁ ℓ₂ ℓ₃} {T : Type{ℓ₁}} {x y : T} {P : T → Type{ℓ₂}} {Q : Bool → Type{ℓ₃}} where
  if-elim : ∀{B} → P(if B then x else y) → (P(x) → Q(𝑇)) → (P(y) → Q(𝐹)) → Q(B)
  if-elim{𝑇} p pxq pyq = pxq p
  if-elim{𝐹} p pxq pyq = pyq p

module _ {ℓ₁ ℓ₂ ℓ₃} {T : Type{ℓ₁}} {x y : T} {P : T → Type{ℓ₂}} {Q : Type{ℓ₃}} where
  if-bool-elim : ∀{B} → P(if B then x else y) → (P(x) → (B ≡ 𝑇) → Q) → (P(y) → (B ≡ 𝐹) → Q) → Q
  if-bool-elim{𝑇} p pxq pyq = pxq p [≡]-intro
  if-bool-elim{𝐹} p pxq pyq = pyq p [≡]-intro

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {T : Type{ℓ₁}} {P : T → Type{ℓ₂}} {X : Type{ℓ₃}} {Y : Type{ℓ₄}} (nxy : X → Y → Logic.⊥) where
  either-bool-left : (xy : (X ∨ Y)) → (X ↔ (Either.isRight(xy) ≡ 𝐹))
  either-bool-left xy with bivalence{Either.isRight(xy)}
  either-bool-left (Left  x) | Right f = [↔]-intro (const x) (const f)
  either-bool-left (Right y) | Left  t = [↔]-intro (\()) (x ↦ empty(nxy x y))

  either-bool-right : (xy : (X ∨ Y)) → (Y ↔ (Either.isRight(xy) ≡ 𝑇))
  either-bool-right xy with bivalence{Either.isRight(xy)}
  either-bool-right (Left  x) | Right f = [↔]-intro (\()) (y ↦ empty(nxy x y))
  either-bool-right (Right y) | Left  t = [↔]-intro (const y) (const t)

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {T : Type{ℓ₁}} {P : T → Type{ℓ₂}} {X : Type{ℓ₃}} {Y : Type{ℓ₄}} where
  either-bool-leftₗ : (xy : (X ∨ Y)) → (X ← (Either.isRight(xy) ≡ 𝐹))
  either-bool-leftₗ xy with bivalence{Either.isRight(xy)}
  either-bool-leftₗ (Left  x) | Right f = const x
  either-bool-leftₗ (Right y) | Left  t = \()

  either-bool-rightₗ : (xy : (X ∨ Y)) → (Y ← (Either.isRight(xy) ≡ 𝑇))
  either-bool-rightₗ xy with bivalence{Either.isRight(xy)}
  either-bool-rightₗ (Left  x) | Right f = \()
  either-bool-rightₗ (Right y) | Left  t = const y

  if-not-either-bool-intro : ∀{x y : T} → (X → P(x)) → (Y → P(y)) → (xy : (X ∨ Y)) → P(if not(Either.isRight(xy)) then x else y)
  if-not-either-bool-intro {x}{y} xp yp xy = if-intro {x = x}{y = y} (xp ∘ either-bool-leftₗ xy ∘ 𝑇.[¬]-elim) (yp ∘ either-bool-rightₗ xy ∘ 𝑇.[¬¬]-elim ∘ 𝐹.[¬]-elim)

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {T : Type{ℓ₁}} {P : T → Type{ℓ₂}} {X : Type{ℓ₃}} {Y : Type{ℓ₄}} where
  if-either-bool-intro : ∀{x y : T} → (X → P(x)) → (Y → P(y)) → (xy : (X ∨ Y)) → P(if Either.isRight(xy) then y else x)
  if-either-bool-intro {x}{y} xp yp xy = if-intro {x = y}{y = x} (yp ∘ either-bool-rightₗ {P = P} xy) (xp ∘ either-bool-leftₗ {P = P} xy)

---------------------------------------------
-- The predicate of if-statements

module _ {ℓ} {T : Type{ℓ}} {x y : T} where
  if-and : ∀{B₁ B₂} → (if (B₁ && B₂) then x else y ≡ if B₁ then (if B₂ then x else y) else y)
  if-and {𝐹}{𝐹} = [≡]-intro
  if-and {𝐹}{𝑇} = [≡]-intro
  if-and {𝑇}{𝐹} = [≡]-intro
  if-and {𝑇}{𝑇} = [≡]-intro

  if-or : ∀{B₁ B₂} → (if (B₁ || B₂) then x else y ≡ if B₁ then x else if B₂ then x else y)
  if-or {𝐹}{𝐹} = [≡]-intro
  if-or {𝐹}{𝑇} = [≡]-intro
  if-or {𝑇}{𝐹} = [≡]-intro
  if-or {𝑇}{𝑇} = [≡]-intro

  if-not : ∀{B} → (if (! B) then x else y ≡ if B then y else x)
  if-not {𝐹} = [≡]-intro
  if-not {𝑇} = [≡]-intro

---------------------------------------------
-- The results of if-statements

module _ {ℓ} {T : Type{ℓ}} {x : T} {B} where
  if-then-redundant : (if B then x else x ≡ x)
  if-then-redundant = elim-redundant{b = B}

module _ {ℓ} {T : Type{ℓ}} {B} where
  if-then-bool-inverse : (if B then 𝑇 else 𝐹 ≡ B)
  if-then-bool-inverse = elim-inverse{b = B}

  if-then-bool-anti-inverse : (if B then 𝐹 else 𝑇 ≡ ! B)
  if-then-bool-anti-inverse = elim-anti-inverse{b = B}

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:
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

data ⊤ : Set where
  tt : ⊤

foo : Nat → ⊤ → ⊤
foo 0 tt = tt
foo (suc n) tt = foo n tt -- NB tail-recursive

test : foo 100000 tt ≡ tt
test = refl -- memory blows up here


text:
module Issue2486.Import where

open import Issue2486.Haskell

{-# FOREIGN GHC import qualified MAlonzo.Code.Issue2486.Haskell #-}

data MyList (A : Set) : Set where
  [] : MyList A
  _::_ : A → MyList A → MyList A

{-# COMPILE GHC MyList = data MAlonzo.Code.Issue2486.Haskell.MyList ( MAlonzo.Code.Issue2486.Haskell.Nil | MAlonzo.Code.Issue2486.Haskell.Cons ) #-}


text:
{-# OPTIONS --allow-unsolved-metas #-}
module FLutil where

open import Level hiding ( suc ; zero )
open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
open import Data.Fin.Permutation  -- hiding ([_,_])
open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
open import Data.Nat.Properties as DNP
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
open import Data.Product
open import Relation.Nullary
open import Data.Empty
open import  Relation.Binary.Core
open import  Relation.Binary.Definitions
open import logic
open import nat

infixr  100 _::_

data  FL : (n : ℕ )→ Set where
   f0 :  FL 0
   _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)

data _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  where
   f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn →   (xn :: xt) f< ( yn :: yt )
   f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt →   (xn :: xt) f< ( xn :: yt )

FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n}  → xn :: x ≡ yn :: y → ( xn ≡ yn )  × (x ≡ y )
FLeq refl = refl , refl

FLpos : {n : ℕ} → FL (suc n) → Fin (suc n)
FLpos (x :: _) = x

f-<> :  {n : ℕ } {x : FL n } {y : FL n}  → x f< y → y f< x → ⊥
f-<> (f<n x) (f<n x₁) = nat-<> x x₁
f-<> (f<n x) (f<t lt2) = nat-≡< refl x
f-<> (f<t lt) (f<n x) = nat-≡< refl x
f-<> (f<t lt) (f<t lt2) = f-<> lt lt2

f-≡< :  {n : ℕ } {x : FL n } {y : FL n}  → x ≡ y → y f< x → ⊥
f-≡< refl (f<n x) = nat-≡< refl x
f-≡< refl (f<t lt) = f-≡< refl lt

FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n}  _≡_  _f<_
FLcmp f0 f0 = tri≈ (λ ()) refl (λ ())
FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn
... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj₁ (FLeq eq)) ) a) (λ lt  → f-<> lt (f<n a) )
... | tri> ¬a ¬b c = tri> (λ lt  → f-<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj₁ (FLeq eq)) )) c) (f<n c)
... | tri≈ ¬a refl ¬c with FLcmp xt yt
... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj₂ (FLeq eq) )) (λ lt  → f-<> lt (f<t a) )
... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt )  refl (λ lt → f-≡< refl lt )
... | tri> ¬a₁ ¬b c = tri> (λ lt  → f-<> lt (f<t c) ) (λ eq → ¬b (proj₂ (FLeq eq) )) (f<t c)

f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z
f<-trans {suc n} (f<n x) (f<n x₁) = f<n ( Data.Fin.Properties.<-trans x x₁ )
f<-trans {suc n} (f<n x) (f<t y<z) = f<n x
f<-trans {suc n} (f<t x<y) (f<n x) = f<n x
f<-trans {suc n} (f<t x<y) (f<t y<z) = f<t (f<-trans x<y y<z)

infixr 250 _f<?_

_f<?_ : {n  : ℕ} → (x y : FL n ) → Dec (x f< y )
x f<? y with FLcmp x y
... | tri< a ¬b ¬c = yes a
... | tri≈ ¬a refl ¬c = no ( ¬a )
... | tri> ¬a ¬b c = no ( ¬a )

_f≤_ : {n : ℕ } (x : FL n ) (y : FL n)  → Set
_f≤_ x y = (x ≡ y ) ∨  (x f< y )

FL0 : {n : ℕ } → FL n
FL0 {zero} = f0
FL0 {suc n} = zero :: FL0

fmax : { n : ℕ } →  FL n
fmax {zero} = f0
fmax {suc n} = fromℕ< a<sa :: fmax {n}

fmax< : { n : ℕ } → {x : FL n } → ¬ (fmax f< x )
fmax< {suc n} {x :: y} (f<n lt) = nat-≤> (fmax1 x) lt where
    fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a<sa)
    fmax1 {zero} zero = z≤n
    fmax1 {suc n} zero = z≤n
    fmax1 {suc n} (suc x) = s≤s (fmax1 x)
fmax< {suc n} {x :: y} (f<t lt) = fmax< {n} {y} lt

fmax¬ : { n : ℕ } → {x : FL n } → ¬ ( x ≡ fmax ) → x f< fmax
fmax¬ {zero} {f0} ne = ⊥-elim ( ne refl )
fmax¬ {suc n} {x} ne with FLcmp x fmax
... | tri< a ¬b ¬c = a
... | tri≈ ¬a b ¬c = ⊥-elim ( ne b)
... | tri> ¬a ¬b c = ⊥-elim (fmax< c)

x≤fmax : {n : ℕ } → {x : FL n} → x f≤ fmax
x≤fmax {n} {x} with FLcmp x fmax
... | tri< a ¬b ¬c = case2 a
... | tri≈ ¬a b ¬c = case1 b
... | tri> ¬a ¬b c = ⊥-elim ( fmax< c )

open import Data.Nat.Properties using ( ≤-trans ; <-trans )
fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n
fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
    fsuc1 : suc (toℕ x) < n
    fsuc1 =  Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
fsuc (x :: y) (f<t lt) = x :: fsuc y lt

open import fin

flist1 :  {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n))
flist1 zero i<n [] _ = []
flist1 zero i<n (a ∷ x ) z  = ( zero :: a ) ∷ flist1 zero i<n x z
flist1 (suc i) (s≤s i<n) [] z  = flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z
flist1 (suc i) i<n (a ∷ x ) z  = ((fromℕ< i<n ) :: a ) ∷ flist1 (suc i) i<n x z

flist : {n : ℕ } → FL n → List (FL n)
flist {zero} f0 = f0 ∷ []
flist {suc n} (x :: y)  = flist1 n a<sa (flist y) (flist y)

FL1 : List ℕ → List ℕ
FL1 [] = []
FL1 (x ∷ y) = suc x ∷ FL1 y

FL→plist : {n : ℕ} → FL n → List ℕ
FL→plist {0} f0 = []
FL→plist {suc n} (zero :: y) = zero ∷ FL1 (FL→plist y)
FL→plist {suc n} (suc x :: y) with FL→plist y
... | [] = zero ∷ []
... | x1 ∷ t = suc x1 ∷ FL2 x t where
  FL2 : {n : ℕ} → Fin n → List ℕ → List ℕ
  FL2 zero y = zero ∷ FL1 y
  FL2 (suc i) [] = zero ∷ []
  FL2 (suc i) (x ∷ y) = suc x ∷ FL2 i y

tt0 = (# 2) :: (# 1) :: (# 0) :: zero :: f0
tt1 = FL→plist tt0

open _∧_

find-zero : {n i : ℕ} → List ℕ → i < n  → Fin n ∧ List ℕ
find-zero  [] i<n = record { proj1 = fromℕ< i<n  ; proj2 = [] }
find-zero x (s≤s z≤n) = record { proj1 = fromℕ< (s≤s z≤n)  ; proj2 = x }
find-zero (zero ∷ y) (s≤s (s≤s i<n)) = record { proj1 = fromℕ< (s≤s (s≤s i<n)) ; proj2 = y }
find-zero (suc x ∷ y) (s≤s (s≤s i<n)) with find-zero y (s≤s i<n)
... | record { proj1 = i ; proj2 = y1 } = record { proj1 = suc i ; proj2 = suc x ∷ y1 }

plist→FL : {n : ℕ} → List ℕ → FL n -- wrong implementation
plist→FL {zero} [] = f0
plist→FL {suc n} [] = zero :: plist→FL {n} []
plist→FL {zero} x = f0
plist→FL {suc n} x with find-zero x a<sa
... | record { proj1 = i ; proj2 = y } = i :: plist→FL y

tt2 = 2 ∷ 1 ∷ 0 ∷ 3 ∷ []
tt3 : FL 4
tt3 = plist→FL tt2
tt4 = FL→plist tt3
tt5 = plist→FL {4} (FL→plist tt0)

-- maybe FL→iso can be easier using this ...
-- FL→plist-iso : {n : ℕ} → (f : FL n ) → plist→FL (FL→plist f ) ≡ f
-- FL→plist-iso = {!!}
-- FL→plist-inject : {n : ℕ} → (f g : FL n ) → FL→plist f ≡ FL→plist g → f ≡ g
-- FL→plist-inject = {!!}

open import Relation.Binary as B hiding (Decidable; _⇔_)
open import Data.Sum.Base as Sum --  inj₁
open import Relation.Nary using (⌊_⌋)
open import Data.List.Fresh hiding ([_])

FList : (n : ℕ ) → Set
FList n = List# (FL n) ⌊ _f<?_ ⌋

fr1 : FList 3
fr1 =
   ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
   ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
   ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
   ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷#
   ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷#
   []

open import Data.Product
open import Relation.Nullary.Decidable hiding (⌊_⌋)
-- open import Data.Bool hiding (_<_ ; _≤_ )
open import Data.Unit.Base using (⊤ ; tt)

--  fresh a []        = ⊤
--  fresh a (x ∷# xs) = R a x × fresh a xs

-- toWitness
-- ttf< :  {n : ℕ } → {x a : FL n } → x f< a  → T (isYes (x f<? a))
-- ttf< {n} {x} {a} x<a with x f<? a
-- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
-- ... | no nn = ⊥-elim ( nn x<a )

ttf : {n : ℕ } {x a : FL (n)} → x f< a → (y : FList (n)) →  fresh (FL (n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (n)) ⌊ _f<?_ ⌋  x y
ttf _ [] fr = Level.lift tt
ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where
       ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
       ttf1 t x<a = f<-trans x<a (toWitness t)

-- by https://gist.github.com/aristidb/1684202

FLinsert : {n : ℕ } → FL n → FList n  → FList n
FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x
     → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
FLinsert {zero} f0 y = f0 ∷# []
FLinsert {suc n} x [] = x ∷# []
FLinsert {suc n} x (cons a y x₁) with FLcmp x a
... | tri≈ ¬a b ¬c  = cons a y x₁
... | tri< lt ¬b ¬c  = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁)
FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt  = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
FLinsert {suc n} x (cons a y yr)  | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr )

FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
... | tri< x<b ¬b ¬c  = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt
... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt
... | tri> ¬a ¬b b<x =  Level.lift a<b  ,  Level.lift (fromWitness  (f<-trans (toWitness a<b) b<x))  , Level.lift tt
FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b
... | tri< x<b ¬b ¬c =  Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br
... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br
FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
    Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt
FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x =
    Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y

fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1

open import Data.List.Fresh.Relation.Unary.Any
open import Data.List.Fresh.Relation.Unary.All

x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_) (FLinsert x xs)
x∈FLins {zero} f0 [] = here refl
x∈FLins {zero} f0 (cons f0 xs x) = here refl
x∈FLins {suc n} x [] = here refl
x∈FLins {suc n} x (cons a xs x₁) with FLcmp x a
... | tri< x<a ¬b ¬c = here refl
... | tri≈ ¬a b ¬c   = here b
x∈FLins {suc n} x (cons a [] x₁)              | tri> ¬a ¬b a<x = there ( here refl )
x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) )

nextAny : {n : ℕ} → {x h : FL n } → {L : FList n}  → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_) L → Any (x ≡_) (cons h L hr )
nextAny (here x₁) = there (here x₁)
nextAny (there any) = there (there any)

insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs)
insAny {zero} {f0} {f0} (cons a L xr) (here refl) = here refl
insAny {zero} {f0} {f0} (cons a L xr) (there any) = insAny {zero} {f0} {f0} L any
insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h a
... | tri< x<a ¬b ¬c = there any
... | tri≈ ¬a b ¬c = any
insAny {suc n} {a} {h} (cons a [] (Level.lift tt)) (here refl) | tri> ¬a ¬b c = here refl
insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here refl) | tri> ¬a ¬b c = here refl
insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any)

-- FLinsert membership

module FLMB { n : ℕ } where

  FL-Setoid : Setoid Level.zero Level.zero
  FL-Setoid  = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }}

  open import Data.List.Fresh.Membership.Setoid FL-Setoid

  FLinsert-mb :  (x : FL n ) → (xs : FList n)  → x ∈ FLinsert x xs
  FLinsert-mb x xs = x∈FLins {n} x xs

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois