text:
------------------------------------------------------------------------
-- An ad-hoc but straightforward solution to the problem of showing
-- that elegant definitions of the Hamming numbers (see EWD 792) and
-- the Fibonacci sequence are productive
------------------------------------------------------------------------

module StreamProg where

open import Codata.Musical.Notation
open import Codata.Musical.Stream as S using (Stream; _∷_; _≈_)
open import Data.Nat
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

private
  module SS {A : Set} = Setoid (S.setoid A)

------------------------------------------------------------------------
-- Merging of streams

data Ord : Set where
  lt : Ord
  eq : Ord
  gt : Ord

merge : {A : Set} → (A → A → Ord) → Stream A → Stream A → Stream A
merge cmp (x ∷ xs) (y ∷ ys) with cmp x y
... | lt = x ∷ ♯ merge cmp (♭ xs)   (y ∷ ys)
... | eq = x ∷ ♯ merge cmp (♭ xs)   (♭ ys)
... | gt = y ∷ ♯ merge cmp (x ∷ xs) (♭ ys)

------------------------------------------------------------------------
-- Stream programs

infixr 5 _∷_

data StreamP (A : Set) : Set1 where
  _∷_     : (x : A) (xs : ∞ (StreamP A)) → StreamP A
  zipWith : ∀ {B C} (f : B → C → A)
            (xs : StreamP B) (ys : StreamP C) → StreamP A
  map     : ∀ {B} (f : B → A) (xs : StreamP B) → StreamP A
  mergeP  : (cmp : A → A → Ord)
            (xs : StreamP A) (ys : StreamP A) → StreamP A

data StreamW A : Set1 where
  _∷_ : (x : A) (xs : StreamP A) → StreamW A

zipWithW : {A B C : Set} →
           (A → B → C) → StreamW A → StreamW B → StreamW C
zipWithW f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys

mapW : {A B : Set} → (A → B) → StreamW A → StreamW B
mapW f (x ∷ xs) = f x ∷ map f xs

mergeW : {A : Set} →
         (A → A → Ord) → StreamW A → StreamW A → StreamW A
mergeW cmp (x ∷ xs) (y ∷ ys) with cmp x y
... | lt = x ∷ mergeP cmp xs (y ∷ ♯ ys)
... | eq = x ∷ mergeP cmp xs ys
... | gt = y ∷ mergeP cmp (x ∷ ♯ xs) ys

whnf : ∀ {A} → StreamP A → StreamW A
whnf (x ∷ xs)           = x ∷ ♭ xs
whnf (zipWith f xs ys)  = zipWithW f (whnf xs) (whnf ys)
whnf (map f xs)         = mapW f (whnf xs)
whnf (mergeP cmp xs ys) = mergeW cmp (whnf xs) (whnf ys)

mutual

  ⟦_⟧W : ∀ {A} → StreamW A → Stream A
  ⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧P

  ⟦_⟧P : ∀ {A} → StreamP A → Stream A
  ⟦ xs ⟧P = ⟦ whnf xs ⟧W

------------------------------------------------------------------------
-- Examples

fib : StreamP ℕ
fib = 0 ∷ ♯ zipWith _+_ fib (1 ∷ ♯ fib)

-- Alternative definition showing that definitions do not need to
-- start with a cons constructor.

fib′ : StreamP ℕ
fib′ = zipWith _+_ (0 ∷ ♯ fib′) (0 ∷ ♯ (1 ∷ ♯ fib′))

cmp : ℕ → ℕ → Ord
cmp m n = toOrd (compare m n)
  where
  toOrd : ∀ {m n} → Ordering m n → Ord
  toOrd (less _ _)    = lt
  toOrd (equal _)     = eq
  toOrd (greater _ _) = gt

hamming : StreamP ℕ
hamming = 1 ∷ ♯ mergeP cmp (map (_*_ 2) hamming) (map (_*_ 3) hamming)

------------------------------------------------------------------------
-- The definition of fib is correct

-- ⟦_⟧P is homomorphic with respect to zipWith/S.zipWith.

zipWith-hom : ∀ {A B C} (_∙_ : A → B → C) xs ys →
              ⟦ zipWith _∙_ xs ys ⟧P ≈ S.zipWith _∙_ ⟦ xs ⟧P ⟦ ys ⟧P
zipWith-hom _∙_ xs ys with whnf xs | whnf ys
zipWith-hom _∙_ xs ys | x ∷ xs′ | y ∷ ys′ =
  P.refl ∷ ♯ zipWith-hom _∙_ xs′ ys′

-- Unfortunately Agda's definitional equality for coinductive
-- constructors is currently a little strange, so the result type
-- cannot be written out completely here:

fib-correct′ :
  ⟦ fib ⟧P ≈ 0 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (1 ∷ _ {- ♯ ⟦ fib ⟧P -})
fib-correct′ = P.refl ∷ ♯ zipWith-hom _+_ fib (1 ∷ ♯ fib)

-- Fortunately there is a workaround.

fib-correct : ⟦ fib ⟧P ≈ 0 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (1 ∷ ♯ ⟦ fib ⟧P)
fib-correct =
  P.refl ∷ ♯ SS.trans (zipWith-hom _+_ fib (1 ∷ ♯ fib))
                      (S.zipWith-cong _+_ (SS.refl {x = 0 ∷ _})
                                          (P.refl ∷ ♯ SS.refl))

-- For a proof showing that the given equation for fib has a unique
-- solution, see MapIterate.

------------------------------------------------------------------------
-- The definition of hamming is correct

-- ⟦_⟧P is homomorphic with respect to map/S.map.

map-hom : ∀ {A B} (f : A → B) xs →
          ⟦ map f xs ⟧P ≈ S.map f ⟦ xs ⟧P
map-hom f xs with whnf xs
... | x ∷ xs′ = P.refl ∷ ♯ map-hom f xs′

-- ⟦_⟧P is homomorphic with respect to mergeP/merge.

merge-hom : ∀ {A} (cmp : A → A → Ord) xs ys →
            ⟦ mergeP cmp xs ys ⟧P ≈ merge cmp ⟦ xs ⟧P ⟦ ys ⟧P
merge-hom cmp xs ys with whnf xs | whnf ys
... | x ∷ xs′ | y ∷ ys′ with cmp x y
...   | lt = P.refl ∷ ♯ merge-hom cmp xs′ (y ∷ ♯ ys′)
...   | eq = P.refl ∷ ♯ merge-hom cmp xs′ ys′
...   | gt = P.refl ∷ ♯ merge-hom cmp (x ∷ ♯ xs′) ys′

-- merge is a congruence.

merge-cong : ∀ {A} (cmp : A → A → Ord) {xs xs′ ys ys′} →
             xs ≈ xs′ → ys ≈ ys′ →
             merge cmp xs ys ≈ merge cmp xs′ ys′
merge-cong cmp (_∷_ {x = x} P.refl xs≈)
               (_∷_ {x = y} P.refl ys≈) with cmp x y
... | lt = P.refl ∷ ♯ merge-cong cmp (♭ xs≈) (P.refl ∷ ys≈)
... | eq = P.refl ∷ ♯ merge-cong cmp (♭ xs≈) (♭ ys≈)
... | gt = P.refl ∷ ♯ merge-cong cmp (P.refl ∷ xs≈) (♭ ys≈)

-- hamming is correct.

hamming-correct : ⟦ hamming ⟧P ≈
                  1 ∷ ♯ merge cmp (S.map (_*_ 2) ⟦ hamming ⟧P)
                                  (S.map (_*_ 3) ⟦ hamming ⟧P)
hamming-correct =
  P.refl ∷ ♯ SS.trans (merge-hom cmp (map (_*_ 2) hamming)
                                     (map (_*_ 3) hamming))
                      (merge-cong cmp (map-hom (_*_ 2) hamming)
                                      (map-hom (_*_ 3) hamming))

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module AKS.Modular.Quotient where

open import AKS.Modular.Quotient.Base public
open import AKS.Modular.Quotient.Properties public

ext: agda

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
module Formalization.ClassicalPropositionalLogic.Semantics.Proofs where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Either as Either using (_‖_ ; Left ; Right)
open import Formalization.ClassicalPropositionalLogic.Syntax
open import Formalization.ClassicalPropositionalLogic.Semantics
open import Functional
open import Logic.Classical     as Logic using (Classical)
import      Logic.Propositional as Logic
import      Logic.Predicate     as Logic
open import Relator.Equals
open import Relator.Equals.Proofs
open import Sets.PredicateSet using (PredSet ; _∈_ ; _∉_ ; _∪_ ; _∪•_ ; _∖_ ; _⊆_ ; _⊇_ ; ∅ ; [≡]-to-[⊆] ; [≡]-to-[⊇]) renaming (•_ to singleton ; _≡_ to _≡ₛ_)
open import Type

private variable ℓₚ ℓ : Lvl.Level
private variable P : Type{ℓₚ}
private variable 𝔐 : Model(P)
private variable Γ Γ₁ Γ₂ : Formulas(P){ℓ}
private variable φ ψ : Formula(P)

[⊧₊]-antimonotone : (Γ₁ ⊆ Γ₂) → ((_⊧₊ Γ₁) ⊇ (_⊧₊ Γ₂))
[⊧₊]-antimonotone Γ₁Γ₂ 𝔐Γ₂ Γ₁γ = 𝔐Γ₂ (Γ₁Γ₂ Γ₁γ)

[⊧₊]-strengthen : (𝔐 ⊧₊ Γ₁) → (𝔐 ⊧₊ Γ₂) → (𝔐 ⊧₊ (Γ₁ ∪ Γ₂))
[⊧₊]-strengthen 𝔐Γ₁ 𝔐Γ₂ Γ₁Γ₂γ = Logic.[∨]-elim 𝔐Γ₁ 𝔐Γ₂ Γ₁Γ₂γ

[⊧₊]-of-[∪]ₗ : (𝔐 ⊧₊ (Γ₁ ∪ Γ₂)) → (𝔐 ⊧₊ Γ₁)
[⊧₊]-of-[∪]ₗ 𝔐Γ₁Γ₂ 𝔐Γ₁ = 𝔐Γ₁Γ₂ (Left 𝔐Γ₁)

[⊧₊]-of-[∪]ᵣ : (𝔐 ⊧₊ (Γ₁ ∪ Γ₂)) → (𝔐 ⊧₊ Γ₂)
[⊧₊]-of-[∪]ᵣ 𝔐Γ₁Γ₂ 𝔐Γ₂ = 𝔐Γ₁Γ₂ (Right 𝔐Γ₂)

[⊧]-to-[⊧₊] : (𝔐 ⊧ φ) Logic.↔ (𝔐 ⊧₊ singleton(φ))
[⊧]-to-[⊧₊] = Logic.[↔]-intro (_$ [≡]-intro) (\𝔐φ φγ → [≡]-substitutionᵣ φγ 𝔐φ)

[⊧]-contradiction : (𝔐 ⊧ φ) → (𝔐 ⊧ (¬ φ)) → (𝔐 ⊧ ⊥)
[⊧]-contradiction = apply

[⊨]-monotone : (Γ₁ ⊆ Γ₂) → ((Γ₁ ⊨_) ⊆ (Γ₂ ⊨_))
[⊨]-monotone Γ₁Γ₂ Γ₁φ 𝔐Γ₂ = Γ₁φ (Γ₁γ ↦ 𝔐Γ₂ (Γ₁Γ₂ Γ₁γ))

[⊨]-functionₗ : (Γ₁ ≡ₛ Γ₂) → ((Γ₁ ⊨_) ≡ₛ (Γ₂ ⊨_))
[⊨]-functionₗ {Γ₁ = Γ₁}{Γ₂ = Γ₂} Γ₁Γ₂ {φ} = Logic.[↔]-intro ([⊨]-monotone{Γ₁ = Γ₂}{Γ₂ = Γ₁}(\{x} → [≡]-to-[⊇] (Γ₁Γ₂{x}) {x}){φ}) ([⊨]-monotone{Γ₁ = Γ₁}{Γ₂ = Γ₂}(\{x} → [≡]-to-[⊆] (Γ₁Γ₂{x}) {x}){φ})

[⊨]-weaken : (Γ₁ ⊨ φ) → ((Γ₁ ∪ Γ₂) ⊨ φ)
[⊨]-weaken Γ₁φ 𝔐Γ₁Γ₂ = Γ₁φ (Γ₁γ ↦ 𝔐Γ₁Γ₂ (Left Γ₁γ))

[⊨]-validity : (∀{Γ : Formulas(P){ℓ}} → (Γ ⊨ φ)) Logic.↔ Valid(φ)
[⊨]-validity = Logic.[↔]-intro (λ r → const r) (λ l → l{∅} empty)

[⊨]-contradiction : (Γ ⊨ φ) → (Γ ⊨ (¬ φ)) → (Γ ⊨ ⊥)
[⊨]-contradiction Γφ Γ¬φ 𝔐Γ = Γ¬φ 𝔐Γ (Γφ 𝔐Γ)

[⊨]-unsatisfiability : (Γ ⊨ ⊥) Logic.↔ Unsatisfiable(Γ)
[⊨]-unsatisfiability {Γ = Γ} = Logic.[↔]-intro l r where
  l : (Γ ⊨ ⊥) ← Unsatisfiable(Γ)
  l unsatΓ {𝔐} 𝔐Γ = unsatΓ (Logic.[∃]-intro 𝔐 ⦃ 𝔐Γ ⦄)

  r : (Γ ⊨ ⊥) → Unsatisfiable(Γ)
  r Γ⊥ (Logic.[∃]-intro 𝔐 ⦃ 𝔐Γ ⦄) = Γ⊥ 𝔐Γ

[⊨][¬]-intro : ((Γ ∪ singleton(φ)) ⊨ ⊥) Logic.↔ (Γ ⊨ (¬ φ))
[⊨][¬]-intro {Γ = Γ}{φ = φ} = Logic.[↔]-intro l r where
  l : ((Γ ∪ singleton(φ)) ⊨ ⊥) ← (Γ ⊨ (¬ φ))
  l Γ¬φ 𝔐Γφ = Γ¬φ (𝔐Γφ ∘ Left) (𝔐Γφ (Right [≡]-intro))

  r : ((Γ ∪ singleton(φ)) ⊨ ⊥) → (Γ ⊨ (¬ φ))
  r Γφ⊥ 𝔐Γ 𝔐φ = Γφ⊥ ([⊧₊]-strengthen {Γ₁ = Γ}{Γ₂ = singleton(φ)} 𝔐Γ (Logic.[↔]-to-[→] [⊧]-to-[⊧₊] 𝔐φ))

[∅]-satisfiable : Satisfiable{P = P}{ℓ = ℓ}(∅)
[∅]-satisfiable = Logic.[∃]-intro (const(𝑇)) ⦃ \{_}() ⦄

module _ ⦃ classical : ∀{ℓ} → Logic.∀ₗ(Classical{ℓ}) ⦄ where
  [⊧]-of-[¬¬] : (𝔐 ⊧ ¬(¬ φ)) → (𝔐 ⊧ φ)
  [⊧]-of-[¬¬] {𝔐 = 𝔐}{φ = φ} = Logic.[¬¬]-elim

  [⊨]-entailment-unsatisfiability : (Γ ⊨ φ) Logic.↔ Unsatisfiable(Γ ∪ singleton(¬ φ))
  [⊨]-entailment-unsatisfiability {Γ = Γ}{φ = φ} = Logic.[↔]-intro l r where
    l : (Γ ⊨ φ) ← Unsatisfiable(Γ ∪ singleton(¬ φ))
    l r {𝔐} 𝔐Γ = [⊧]-of-[¬¬] {𝔐 = 𝔐}{φ = φ} (𝔐¬φ ↦ r (Logic.[∃]-intro 𝔐 ⦃ Logic.[∨]-elim 𝔐Γ (\{[≡]-intro → 𝔐¬φ}) ⦄))

    r : (Γ ⊨ φ) → Unsatisfiable(Γ ∪ singleton(¬ φ))
    r l (Logic.[∃]-intro 𝔐 ⦃ sat ⦄) = [⊧]-contradiction {φ = φ} 𝔐φ 𝔐¬φ where
      𝔐φ  = l([⊧₊]-of-[∪]ₗ {Γ₁ = Γ} sat)
      𝔐¬φ = Logic.[↔]-to-[←] [⊧]-to-[⊧₊] ([⊧₊]-of-[∪]ᵣ {Γ₁ = Γ} sat)

  [⊨][⟶]-intro : ((Γ ∪ singleton(φ)) ⊨ ψ) Logic.↔ (Γ ⊨ (φ ⟶ ψ))
  [⊨][⟶]-intro {Γ = Γ}{φ = φ}{ψ = ψ} = Logic.[↔]-intro l r where
    l : (Γ ⊨ (φ ⟶ ψ)) → ((Γ ∪ singleton(φ)) ⊨ ψ)
    l φψ {𝔐 = 𝔐} 𝔐Γφ = Logic.[∨]-elim (¬φ ↦ Logic.[⊥]-elim(¬φ 𝔐φ)) id (φψ 𝔐Γ) where
      𝔐Γ : 𝔐 ⊧₊ Γ
      𝔐Γ {γ} Γγ = 𝔐Γφ {γ} (Logic.[∨]-introₗ Γγ)

      𝔐φ : 𝔐 ⊧ φ
      𝔐φ = 𝔐Γφ {φ} (Logic.[∨]-introᵣ [≡]-intro)

    r : ((Γ ∪ singleton(φ)) ⊨ ψ) → (Γ ⊨ (φ ⟶ ψ))
    r Γφψ {𝔐 = 𝔐} 𝔐Γ with Logic.excluded-middle(𝔐 ⊧ φ)
    ... | Logic.[∨]-introₗ 𝔐φ  = Logic.[∨]-introᵣ (Γφψ(Logic.[∨]-elim 𝔐Γ \{[≡]-intro → 𝔐φ}))
    ... | Logic.[∨]-introᵣ ¬𝔐φ = Logic.[∨]-introₗ ¬𝔐φ

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module InstanceArgumentsHidden where

record ⊤ : Set where

-- check that the instance argument resolution takes into account
-- instances which take hidden arguments to be of the correct type.
postulate A1 A2 B : Set
          f1 : {{a : A1}} → B
          f2 : {{a : A2}} → B
          inst1 : {_ : ⊤} → A1

checkProperty : ⊤ → Set
checkProperty _ = ⊤

postulate inst2 : {a : ⊤} → {_ : checkProperty a} → A2

test1 = f1
test2 = f2

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module MagicWith where

data _×_ (A : Set)(B : A -> Set) : Set where
  _,_ : (x : A) -> B x -> A × B

fst : {A : Set}{B : A -> Set} -> A × B -> A
fst (x , y) = x

snd : {A : Set}{B : A -> Set}(p : A × B) -> B (fst p)
snd (x , y) = y

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

record True  : Set where
data   False : Set where

IsZero : Nat -> Set
IsZero zero    = True
IsZero (suc _) = False

Uncurry : {A : Set}{B : A -> Set} -> ((x : A) -> B x -> Set) -> A × B -> Set
Uncurry F p = F (fst p) (snd p)

F : (n : Nat) -> IsZero n -> Set
F zero _ = True
F (suc _) ()

-- Trying to match only on fst p will give a (bad) error,
-- just as it should.
f : (p : Nat × IsZero) -> Uncurry F p
f p with fst p | snd p
f p | zero  | q = _
f p | suc _ | ()


text:
------------------------------------------------------------------------
-- An alternative definition of listed finite subsets
------------------------------------------------------------------------

-- The code in this module is based on Frumin, Geuvers, Gondelman and
-- van der Weide's "Finite Sets in Homotopy Type Theory". However, the
-- type of subsets is defined mutually with a membership predicate,
-- and two higher constructors have been replaced by a constructor
-- that states that extensionally equal subsets are equal.
--
-- The type in this module is perhaps harder to work with than the one
-- in Finite-subset.Listed: the "natural" eliminator only works for
-- motives that are propositional. However, the two types are shown to
-- be equivalent.

{-# OPTIONS --cubical --safe #-}

import Equality.Path as P

module Finite-subset.Listed.Alternative
  {c⁺} (eq : ∀ {a p} → P.Equality-with-paths a p c⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

import Equality.Path.Univalence as EPU
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (_∷_; swap)

open import Bijection equality-with-J using (_↔_)
import Bijection P.equality-with-J as PB
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence P.equality-with-J as PEq
import Finite-subset.Listed eq as Listed
open import Function-universe equality-with-J as F hiding (id; _∘_)
import H-level P.equality-with-J as PH
open import H-level.Closure equality-with-J
import H-level.Closure P.equality-with-J as PHC
open import H-level.Truncation.Propositional eq as Trunc
  using (∥_∥; _∥⊎∥_)
open import Injection equality-with-J using (Injective)
import Univalence-axiom P.equality-with-J as PU

private
  variable
    a b p                 : Level
    A B                   : Type a
    P                     : A → Type p
    x x∼y y y₁ y₂ z z₁ z₂ : A

------------------------------------------------------------------------
-- Listed finite subsets

mutual

  -- Listed finite subsets of a given type, defined mutually with a
  -- membership predicate.

  infixr 5 _∷_

  data Finite-subset-of (A : Type a) : Type a where
    []              : Finite-subset-of A
    _∷_             : A → Finite-subset-of A → Finite-subset-of A
    extensionalityᴾ : x ∼ y → x P.≡ y
    is-setᴾ         : P.Is-set (Finite-subset-of A)

  private

    Membership :
      {A : Type a} → A → Finite-subset-of A → PH.Proposition a

  -- Membership.

  infix 4 _∈_

  _∈_ : {A : Type a} → A → Finite-subset-of A → Type a
  x ∈ y = proj₁ (Membership x y)

  -- Membership is propositional.

  ∈-propositionalᴾ : ∀ y → P.Is-proposition (x ∈ y)
  ∈-propositionalᴾ y = proj₂ (Membership _ y)

  -- Extensional equality.

  infix 4 _∼_

  _∼_ :
    {A : Type a} → Finite-subset-of A → Finite-subset-of A → Type a
  x ∼ y = ∀ z → z ∈ x ⇔ z ∈ y

  Membership x [] =
    ⊥ , PHC.⊥-propositional

  Membership x (y ∷ z) =
    (x ≡ y ∥⊎∥ x ∈ z) , Trunc.truncation-is-propositionᴾ

  Membership x (extensionalityᴾ {x = y} {y = z} y∼z i) =
    lemma i
    where
    lemma : Membership x y P.≡ Membership x z
    lemma = P.Σ-≡,≡→≡
      (x ∈ y  P.≡⟨ PEq._≃_.from
                     (PU.Propositional-extensionality-is-univalence-for-propositions P.ext)
                     (λ _ _ → EPU.univ)
                     (∈-propositionalᴾ y)
                     (∈-propositionalᴾ z)
                     (y∼z x) ⟩∎
       x ∈ z  ∎)
      (PHC.H-level-propositional P.ext 1 _ _)

  Membership x (is-setᴾ {x = y} {y = z} p q i j) =
    P.heterogeneous-UIP₀₀
      {x = λ _ → Membership x y}
      {y = λ _ → Membership x z}
      {p = λ i → Membership x (p i)}
      {q = λ i → Membership x (q i)}
      (PU.∃-H-level-H-level-1+ P.ext EPU.univ 1)
      i j

-- Variants of some of the constructors.

extensionality : x ∼ y → x ≡ y
extensionality = _↔_.from ≡↔≡ ∘ extensionalityᴾ

is-set : Is-set (Finite-subset-of A)
is-set =
  _↔_.from (H-level↔H-level 2) Finite-subset-of.is-setᴾ

-- Membership is propositional.

∈-propositional : ∀ y → Is-proposition (x ∈ y)
∈-propositional = _↔_.from (H-level↔H-level 1) ∘ ∈-propositionalᴾ

-- Unit tests documenting some of the computational behaviour of _∈_.

_ : (x ∈ []) ≡ ⊥
_ = refl _

_ : (x ∈ y ∷ z) ≡ (x ≡ y ∥⊎∥ x ∈ z)
_ = refl _

------------------------------------------------------------------------
-- Eliminators

private

  -- The following dependent eliminator is not exported, because the
  -- motive is necessarily pointwise propositional (see
  -- motive-propositional below).

  record Elimᴾ′ {A : Type a} (P : Finite-subset-of A → Type p) :
                Type (a ⊔ p) where
    no-eta-equality
    field
      []ʳ             : P []
      ∷ʳ              : ∀ x → P y → P (x ∷ y)
      is-setʳ         : ∀ x → P.Is-set (P x)
      extensionalityʳ :
        (p : P x) (q : P y) →
        P.[ (λ i → P (extensionalityᴾ {x = x} {y = y} x∼y i)) ] p ≡ q

  open Elimᴾ′

  elimᴾ′ : Elimᴾ′ P → (x : Finite-subset-of A) → P x
  elimᴾ′ {A = A} {P = P} e = helper
    where
    module E = Elimᴾ′ e

    helper : (x : Finite-subset-of A) → P x
    helper []      = E.[]ʳ
    helper (x ∷ y) = E.∷ʳ x (helper y)

    helper (extensionalityᴾ {x = x} {y = y} _ i) =
      E.extensionalityʳ (helper x) (helper y) i

    helper (is-setᴾ x y i j) =
      P.heterogeneous-UIP
        E.is-setʳ (is-setᴾ x y)
        (λ i → helper (x i)) (λ i → helper (y i)) i j

  -- The motive is necessarily pointwise propositional.

  motive-propositional :
    Elimᴾ′ P → ∀ x → P.Is-proposition (P x)
  motive-propositional {P = P} e x p q =
    p                                         P.≡⟨ P.sym $ P.subst-refl P _ ⟩
    P.subst P P.refl p                        P.≡⟨ P.cong (λ eq → P.subst P eq p) $ is-setᴾ _ _ ⟩
    P.subst P (extensionalityᴾ λ _ → F.id) p  P.≡⟨ PB._↔_.to (P.heterogeneous↔homogeneous _)
                                                     (e .extensionalityʳ {x∼y = λ _ → F.id} p q) ⟩∎
    q                                         ∎

-- A dependent eliminator, expressed using paths.

record Elimᴾ {A : Type a} (P : Finite-subset-of A → Type p) :
             Type (a ⊔ p) where
  no-eta-equality
  field
    []ʳ             : P []
    ∷ʳ              : ∀ x → P y → P (x ∷ y)
    is-propositionʳ : ∀ x → P.Is-proposition (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : Finite-subset-of A) → P x
elimᴾ {A = A} {P = P} e = elimᴾ′ e′
  where
  module E = Elimᴾ e

  e′ : Elimᴾ′ _
  e′ .[]ʳ                 = e .[]ʳ
  e′ .∷ʳ                  = e .∷ʳ
  e′ .is-setʳ             = PH.mono₁ 1 ∘ e .is-propositionʳ
  e′ .extensionalityʳ _ _ =
    PB._↔_.from (P.heterogeneous↔homogeneous _)
      (e .is-propositionʳ _ _ _)

-- A non-dependent eliminator, expressed using paths.

record Recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    []ʳ             : B
    ∷ʳ              : A → Finite-subset-of A → B → B
    is-propositionʳ : P.Is-proposition B

open Recᴾ public

recᴾ : Recᴾ A B → Finite-subset-of A → B
recᴾ {A = A} {B = B} r = elimᴾ e
  where
  module R = Recᴾ r

  e : Elimᴾ _
  e .[]ʳ               = R.[]ʳ
  e .∷ʳ {y = y} x      = R.∷ʳ x y
  e .is-propositionʳ _ = R.is-propositionʳ

-- A dependent eliminator, expressed using equality.

record Elim
         {A : Type a} (P : Finite-subset-of A → Type p) :
         Type (a ⊔ p) where
  field
    []ʳ             : P []
    ∷ʳ              : ∀ x → P y → P (x ∷ y)
    is-propositionʳ : ∀ x → Is-proposition (P x)

open Elim public

elim : Elim P → (x : Finite-subset-of A) → P x
elim e = elimᴾ e′
  where
  module E = Elim e

  e′ : Elimᴾ _
  e′ .[]ʳ             = E.[]ʳ
  e′ .∷ʳ              = E.∷ʳ
  e′ .is-propositionʳ = _↔_.to (H-level↔H-level 1) ∘ E.is-propositionʳ

-- A non-dependent eliminator, expressed using equality.

record Rec (A : Type a) (B : Type b) : Type (a ⊔ b) where
  field
    []ʳ             : B
    ∷ʳ              : A → Finite-subset-of A → B → B
    is-propositionʳ : Is-proposition B

open Rec public

rec : Rec A B → Finite-subset-of A → B
rec r = elim e
  where
  module R = Rec r

  e : Elim _
  e .[]ʳ               = R.[]ʳ
  e .∷ʳ {y = y} x      = R.∷ʳ x y
  e .is-propositionʳ _ = R.is-propositionʳ

------------------------------------------------------------------------
-- Some lemmas

-- If A is inhabited, then Finite-subset-of A is not a proposition.

¬-proposition : A → ¬ Is-proposition (Finite-subset-of A)
¬-proposition {A = A} x =
  Is-proposition (Finite-subset-of A)  ↝⟨ (λ hyp → hyp _ _) ⟩
  x ∷ [] ≡ []                          ↝⟨ (λ hyp → subst (x ∈_) hyp (Trunc.∣inj₁∣ (refl _))) ⟩
  x ∈ []                               ↔⟨ ⊥↔⊥ ⟩□
  ⊥                                    □

abstract

  -- Duplicated elements can be dropped.

  drop : x ∷ x ∷ y ≡ x ∷ y
  drop {x = x} {y = y} = extensionality λ z →
    z ≡ x ∥⊎∥ (z ≡ x ∥⊎∥ z ∈ y)  ↔⟨ Trunc.drop-left-∥⊎∥ Trunc.∥⊎∥-propositional Trunc.∣inj₁∣ ⟩□
    z ≡ x ∥⊎∥ z ∈ y              □

  -- The "first" two elements can be swapped.

  swap : x ∷ y ∷ z ≡ y ∷ x ∷ z
  swap {x = x} {y = y} {z = z} = extensionality λ u →
    u ≡ x ∥⊎∥ (u ≡ y ∥⊎∥ u ∈ z)  ↔⟨ Trunc.∥⊎∥-assoc ⟩
    (u ≡ x ∥⊎∥ u ≡ y) ∥⊎∥ u ∈ z  ↔⟨ Trunc.∥⊎∥-comm Trunc.∥⊎∥-cong F.id ⟩
    (u ≡ y ∥⊎∥ u ≡ x) ∥⊎∥ u ∈ z  ↔⟨ inverse Trunc.∥⊎∥-assoc ⟩□
    u ≡ y ∥⊎∥ (u ≡ x ∥⊎∥ u ∈ z)  □

-- If x is a member of y, then x ∷ y is equal to y.

∈→∷≡ : x ∈ y → x ∷ y ≡ y
∈→∷≡ {x = x} = elim e _
  where
  e : Elim (λ y → x ∈ y → x ∷ y ≡ y)
  e .∷ʳ {y = y} z hyp =
    Trunc.rec is-set
      [ (λ x≡z →
           x ∷ z ∷ y  ≡⟨ cong (λ x → x ∷ _) x≡z ⟩
           z ∷ z ∷ y  ≡⟨ drop ⟩∎
           z ∷ y      ∎)
      , (λ x∈y →
           x ∷ z ∷ y  ≡⟨ swap ⟩
           z ∷ x ∷ y  ≡⟨ cong (_ ∷_) (hyp x∈y) ⟩∎
           z ∷ y      ∎)
      ]

  e .is-propositionʳ _ =
    Π-closure ext 1 λ _ →
    is-set

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

-- Singleton subsets.

singleton : A → Finite-subset-of A
singleton x = x ∷ []

-- A lemma characterising singleton.

∈singleton≃ :
  (x ∈ singleton y) ≃ ∥ x ≡ y ∥
∈singleton≃ {x = x} {y = y} =
  x ∈ singleton y  ↔⟨⟩
  x ≡ y ∥⊎∥ ⊥      ↔⟨ Trunc.∥∥-cong $ drop-⊥-right ⊥↔⊥ ⟩□
  ∥ x ≡ y ∥        □

-- If truncated equality is decidable, then membership is also
-- decidable.

member? :
  ((x y : A) → Dec ∥ x ≡ y ∥) →
  (x : A) (y : Finite-subset-of A) → Dec (x ∈ y)
member? equal? x = elim e
  where
  e : Elim _
  e .[]ʳ          = no λ ()
  e .∷ʳ {y = z} y = case equal? x y of
    [ (λ  ∥x≡y∥ _ → yes (Trunc.∥∥-map inj₁ ∥x≡y∥))
    , (λ ¬∥x≡y∥ →
         [ (λ x∈z → yes (Trunc.∣inj₂∣ x∈z))
         , (λ x∉z → no (
              x ∈ y ∷ z        ↔⟨⟩
              x ≡ y ∥⊎∥ x ∈ z  ↝⟨ Trunc.∥∥-map [ ¬∥x≡y∥ ∘ Trunc.∣_∣ , x∉z ] ⟩
              ∥ ⊥ ∥            ↔⟨ Trunc.not-inhabited⇒∥∥↔⊥ id ⟩□
              ⊥                □))
         ])
    ]
  e .is-propositionʳ y =
    Dec-closure-propositional ext (∈-propositional y)

------------------------------------------------------------------------
-- The union operation

private

  -- A specification of what it means for a subset to be the union of
  -- two subsets.

  Is-union-of :
    {A : Type a} (_ _ _ : Finite-subset-of A) → Type a
  Is-union-of x y z = ∀ u → (u ∈ z) ≃ (u ∈ x ∥⊎∥ u ∈ y)

  -- Is-union-of x y is functional.

  Is-union-of-functional :
    (x y : Finite-subset-of A) →
    Is-union-of x y z₁ → Is-union-of x y z₂ →
    z₁ ≡ z₂
  Is-union-of-functional {z₁ = z₁} {z₂ = z₂} x y p₁ p₂ =
    extensionality λ u →
      u ∈ z₁           ↔⟨ p₁ u ⟩
      u ∈ x ∥⊎∥ u ∈ y  ↔⟨ inverse $ p₂ u ⟩□
      u ∈ z₂           □

  -- Is-union-of is propositional.

  Is-union-of-propositional :
    (x y z : Finite-subset-of A) →
    Is-proposition (Is-union-of x y z)
  Is-union-of-propositional x y z =
    Π-closure ext 1 λ _ →
    Eq.left-closure ext 0 (∈-propositional z)

  -- The union operation, along with a correctness proof.

  union : (x y : Finite-subset-of A) → ∃ (Is-union-of x y)
  union = elim e
    where
    e : Elim _
    e .[]ʳ y =
        y
      , λ u →
          u ∈ y        ↔⟨ inverse $ Trunc.∥⊎∥-left-identity (∈-propositional y) ⟩□
          ⊥ ∥⊎∥ u ∈ y  □

    e .∷ʳ {y = y} x hyp z =
        x ∷ proj₁ (hyp z)
      , λ u →
          u ∈ x ∷ proj₁ (hyp z)        ↔⟨⟩
          u ≡ x ∥⊎∥ u ∈ proj₁ (hyp z)  ↝⟨ F.id Trunc.∥⊎∥-cong proj₂ (hyp z) u ⟩
          u ≡ x ∥⊎∥ (u ∈ y ∥⊎∥ u ∈ z)  ↔⟨ Trunc.∥⊎∥-assoc ⟩
          (u ≡ x ∥⊎∥ u ∈ y) ∥⊎∥ u ∈ z  ↔⟨⟩
          u ∈ x ∷ y ∥⊎∥ u ∈ z          □

    e .is-propositionʳ x f g = ⟨ext⟩ λ y →
      Σ-≡,≡→≡
        (Is-union-of-functional x y (proj₂ (f y)) (proj₂ (g y)))
        (Is-union-of-propositional x y (proj₁ (g y)) _ _)

-- The union of two finite subsets.

infixr 5 _∪_

_∪_ :
  Finite-subset-of A → Finite-subset-of A →
  Finite-subset-of A
x ∪ y = proj₁ (union x y)

-- Unit tests documenting some of the computational behaviour of _∪_.

_ : [] ∪ x ≡ x
_ = refl _

_ : (x ∷ y) ∪ z ≡ x ∷ (y ∪ z)
_ = refl _

-- Membership of a union of two subsets can be expressed in terms of
-- membership of the subsets.

∈∪≃∈∥⊎∥∈ : ∀ y → (x ∈ y ∪ z) ≃ (x ∈ y ∥⊎∥ x ∈ z)
∈∪≃∈∥⊎∥∈ {z = z} y = proj₂ (union y z) _

-- If x is a member of y, then x is a member of y ∪ z.

∈→∈∪ˡ : ∀ y → x ∈ y → x ∈ y ∪ z
∈→∈∪ˡ y = _≃_.from (∈∪≃∈∥⊎∥∈ y) ∘ Trunc.∣inj₁∣

-- If x is a member of z, then x is a member of y ∪ z.

∈→∈∪ʳ : ∀ y → x ∈ z → x ∈ y ∪ z
∈→∈∪ʳ y = _≃_.from (∈∪≃∈∥⊎∥∈ y) ∘ Trunc.∣inj₂∣

-- [] is a right identity of _∪_.

∪[] :
  (x : Finite-subset-of A) →
  x ∪ [] ≡ x
∪[] = elim e
  where
  e : Elim _
  e .is-propositionʳ _ = is-set
  e .[]ʳ               = refl _
  e .∷ʳ {y = y} x hyp  =
    x ∷ y ∪ []  ≡⟨ cong (x ∷_) hyp ⟩∎
    x ∷ y        ∎

-- A lemma relating _∪_ and _∷_.

∪∷ :
  (x : Finite-subset-of A) →
  x ∪ (y ∷ z) ≡ y ∷ x ∪ z
∪∷ {y = y} {z = z} = elim e
  where
  e : Elim _
  e .is-propositionʳ _ = is-set

  e .[]ʳ = refl _

  e .∷ʳ {y = u} x hyp =
    (x ∷ u) ∪ (y ∷ z)  ≡⟨⟩
    x ∷ u ∪ (y ∷ z)    ≡⟨ cong (x ∷_) hyp ⟩
    x ∷ y ∷ u ∪ z      ≡⟨ swap ⟩
    y ∷ x ∷ u ∪ z      ≡⟨⟩
    y ∷ (x ∷ u) ∪ z    ∎

-- The union operator is associative.

∪-assoc :
  (x : Finite-subset-of A) →
  x ∪ (y ∪ z) ≡ (x ∪ y) ∪ z
∪-assoc {y = y} {z = z} = elim e
  where
  e : Elim _
  e .is-propositionʳ _ = is-set

  e .[]ʳ = refl _

  e .∷ʳ {y = u} x hyp =
    x ∷ u ∪ (y ∪ z)  ≡⟨ cong (x ∷_) hyp ⟩∎
    x ∷ (u ∪ y) ∪ z  ∎

-- The union operator is commutative.

∪-comm :
  (x : Finite-subset-of A) →
  x ∪ y ≡ y ∪ x
∪-comm {y = y} = elim e
  where
  e : Elim _
  e .is-propositionʳ _ = is-set

  e .[]ʳ =
    [] ∪ y  ≡⟨⟩
    y       ≡⟨ sym (∪[] y) ⟩∎
    y ∪ []  ∎

  e .∷ʳ {y = z} x hyp =
    x ∷ z ∪ y    ≡⟨ cong (x ∷_) hyp ⟩
    x ∷ y ∪ z    ≡⟨ sym (∪∷ y) ⟩∎
    y ∪ (x ∷ z)  ∎

-- The union operator is idempotent.

∪-idem : (x : Finite-subset-of A) → x ∪ x ≡ x
∪-idem = elim e
  where
  e : Elim _
  e .[]ʳ =
    [] ∪ []  ≡⟨⟩
    []       ∎

  e .∷ʳ {y = y} x hyp =
    (x ∷ y) ∪ (x ∷ y)  ≡⟨⟩
    x ∷ y ∪ x ∷ y      ≡⟨ cong (_ ∷_) (∪∷ y) ⟩
    x ∷ x ∷ y ∪ y      ≡⟨ drop ⟩
    x ∷ y ∪ y          ≡⟨ cong (_ ∷_) hyp ⟩∎
    x ∷ y              ∎

  e .is-propositionʳ = λ _ → is-set

-- The union operator distributes from the left and right over itself.

∪-distrib-left : ∀ x → x ∪ (y ∪ z) ≡ (x ∪ y) ∪ (x ∪ z)
∪-distrib-left {y = y} {z = z} x =
  x ∪ (y ∪ z)        ≡⟨ cong (_∪ _) $ sym (∪-idem x) ⟩
  (x ∪ x) ∪ (y ∪ z)  ≡⟨ sym $ ∪-assoc x ⟩
  x ∪ (x ∪ (y ∪ z))  ≡⟨ cong (x ∪_) $ ∪-assoc x ⟩
  x ∪ ((x ∪ y) ∪ z)  ≡⟨ cong ((x ∪_) ∘ (_∪ _)) $ ∪-comm x ⟩
  x ∪ ((y ∪ x) ∪ z)  ≡⟨ cong (x ∪_) $ sym $ ∪-assoc y ⟩
  x ∪ (y ∪ (x ∪ z))  ≡⟨ ∪-assoc x ⟩∎
  (x ∪ y) ∪ (x ∪ z)  ∎

∪-distrib-right : ∀ x → (x ∪ y) ∪ z ≡ (x ∪ z) ∪ (y ∪ z)
∪-distrib-right {y = y} {z = z} x =
  (x ∪ y) ∪ z        ≡⟨ ∪-comm (x ∪ _) ⟩
  z ∪ (x ∪ y)        ≡⟨ ∪-distrib-left z ⟩
  (z ∪ x) ∪ (z ∪ y)  ≡⟨ cong₂ _∪_ (∪-comm z) (∪-comm z) ⟩∎
  (x ∪ z) ∪ (y ∪ z)  ∎

------------------------------------------------------------------------
-- Subsets of subsets

-- Subsets.

infix 4 _⊆_

_⊆_ : {A : Type a} → Finite-subset-of A → Finite-subset-of A → Type a
x ⊆ y = ∀ z → z ∈ x → z ∈ y

-- _⊆_ is pointwise propositional.

⊆-propositional :
  (x y : Finite-subset-of A) → Is-proposition (x ⊆ y)
⊆-propositional x y =
  Π-closure ext 1 λ _ →
  Π-closure ext 1 λ _ →
  ∈-propositional y

-- The function x ∷_ is monotone with respect to _⊆_.

∷-cong-⊆ : ∀ y z → y ⊆ z → x ∷ y ⊆ x ∷ z
∷-cong-⊆ {x = x} y z y⊆z = λ u →
  u ∈ x ∷ y        ↔⟨⟩
  u ≡ x ∥⊎∥ u ∈ y  ↝⟨ id Trunc.∥⊎∥-cong y⊆z _ ⟩
  u ≡ x ∥⊎∥ u ∈ z  ↔⟨⟩
  u ∈ x ∷ z        □

-- The union operator is monotone with respect to _⊆_.

∪-mono-⊆ : ∀ x₁ x₂ → x₁ ⊆ x₂ → y₁ ⊆ y₂ → x₁ ∪ y₁ ⊆ x₂ ∪ y₂
∪-mono-⊆ {y₁ = y₁} {y₂ = y₂} x₁ x₂ x₁⊆x₂ y₁⊆y₂ = λ u →
  u ∈ x₁ ∪ y₁        ↔⟨ ∈∪≃∈∥⊎∥∈ x₁ ⟩
  u ∈ x₁ ∥⊎∥ u ∈ y₁  ↝⟨ x₁⊆x₂ u Trunc.∥⊎∥-cong y₁⊆y₂ u ⟩
  u ∈ x₂ ∥⊎∥ u ∈ y₂  ↔⟨ inverse $ ∈∪≃∈∥⊎∥∈ x₂ ⟩□
  u ∈ x₂ ∪ y₂        □

-- The subset property can be expressed using _∪_ and _≡_.

⊆≃∪≡ : ∀ x → (x ⊆ y) ≃ (x ∪ y ≡ y)
⊆≃∪≡ {y = y} x = Eq.⇔→≃
  (⊆-propositional x y)
  is-set
  (elim e x)
  (λ p z →
     z ∈ x      ↝⟨ ∈→∈∪ˡ x ⟩
     z ∈ x ∪ y  ↝⟨ ≡⇒↝ _ (cong (z ∈_) p) ⟩□
     z ∈ y      □)
  where
  e : Elim (λ x → x ⊆ y → x ∪ y ≡ y)
  e .[]ʳ _ =
    [] ∪ y  ≡⟨⟩
    y       ∎

  e .∷ʳ {y = z} x hyp x∷z⊆y =
    x ∷ z ∪ y  ≡⟨ cong (x ∷_) (hyp (λ _ → x∷z⊆y _ ∘ Trunc.∣inj₂∣)) ⟩
    x ∷ y      ≡⟨ ∈→∷≡ (x∷z⊆y x (Trunc.∣inj₁∣ (refl _))) ⟩∎
    y          ∎

  e .is-propositionʳ _ =
    Π-closure ext 1 λ _ →
    is-set

-- _⊆_ is a partial order.

⊆-refl : x ⊆ x
⊆-refl _ = id

⊆-trans : x ⊆ y → y ⊆ z → x ⊆ z
⊆-trans x⊆y y⊆z _ = y⊆z _ ∘ x⊆y _

⊆-antisymmetric : x ⊆ y → y ⊆ x → x ≡ y
⊆-antisymmetric x⊆y y⊆x =
  extensionality λ z →
    record { to = x⊆y z; from = y⊆x z }

------------------------------------------------------------------------
-- Another lemma

-- Equality can be expressed using _⊆_.

≡≃⊆×⊇ : (x ≡ y) ≃ (x ⊆ y × y ⊆ x)
≡≃⊆×⊇ {x = x} {y = y} =
  x ≡ y                  ↝⟨ Eq.⇔→≃
                              is-set
                              (×-closure 1 is-set is-set)
                              (λ x≡y →
                                   (x ∪ y  ≡⟨ cong (_∪ _) x≡y ⟩
                                    y ∪ y  ≡⟨ ∪-idem y ⟩∎
                                    y      ∎)
                                 , (y ∪ x  ≡⟨ cong (_∪ _) $ sym x≡y ⟩
                                    x ∪ x  ≡⟨ ∪-idem x ⟩∎
                                    x      ∎))
                              (λ (p , q) →
                                 x      ≡⟨ sym q ⟩
                                 y ∪ x  ≡⟨ ∪-comm y ⟩
                                 x ∪ y  ≡⟨ p ⟩∎
                                 y      ∎) ⟩
  x ∪ y ≡ y × y ∪ x ≡ x  ↝⟨ inverse $ ⊆≃∪≡ x ×-cong ⊆≃∪≡ y ⟩□
  x ⊆ y × y ⊆ x          □

-- Extensional equality is equivalent to equality.

∼≃≡ : (x ∼ y) ≃ (x ≡ y)
∼≃≡ {x = x} {y = y} =
  x ∼ y                                      ↔⟨⟩
  (∀ z → z ∈ x ⇔ z ∈ y)                      ↔⟨ (∀-cong ext λ _ → ⇔↔→×→) ⟩
  (∀ z → (z ∈ x → z ∈ y) × (z ∈ y → z ∈ x))  ↔⟨ ΠΣ-comm ⟩
  x ⊆ y × y ⊆ x                              ↝⟨ inverse ≡≃⊆×⊇ ⟩□
  x ≡ y                                      □

------------------------------------------------------------------------
-- Definitions related to the listed finite subsets defined in Listed

-- Some lemmas used below.

private

  module Listed≃Listed where

    -- Converts one kind of finite subset to another.

    from : Listed.Finite-subset-of A → Finite-subset-of A
    from = Listed.rec r
      where
      r : Listed.Rec _ _
      r .Listed.Rec.[]ʳ           = []
      r .Listed.Rec.∷ʳ x _ y      = x ∷ y
      r .Listed.Rec.dropʳ _ _ _   = drop
      r .Listed.Rec.swapʳ _ _ _ _ = swap
      r .Listed.Rec.is-setʳ       = is-set

    -- A lemma relating from, _∈_ and Listed._∈_.

    ∈from≃ : ∀ x → (z ∈ from x) ≃ (z Listed.∈ x)
    ∈from≃ {z = z} = Listed.elim-prop e
      where
      e : Listed.Elim-prop _
      e .Listed.Elim-prop.[]ʳ =
        z ∈ from Listed.[]    ↔⟨⟩
        ⊥                     ↔⟨ ⊥↔⊥ ⟩
        ⊥₀                    ↝⟨ inverse $ Listed.∈[]≃ ⟩
        z Listed.∈ Listed.[]  □

      e .Listed.Elim-prop.∷ʳ {y = y} x hyp =
        z ∈ from (x Listed.∷ y)  ↔⟨⟩
        z ≡ x ∥⊎∥ z ∈ from y     ↝⟨ F.id Trunc.∥⊎∥-cong hyp ⟩
        z ≡ x ∥⊎∥ z Listed.∈ y   ↝⟨ inverse Listed.∈∷≃ ⟩□
        z Listed.∈ x Listed.∷ y  □

      e .Listed.Elim-prop.is-propositionʳ _ =
        Eq.right-closure ext 0 Listed.∈-propositional

    -- A lemma relating from, _⊆_ and Listed._⊆_.

    from⊆from→ :
      (x y : Listed.Finite-subset-of A) →
      from x ⊆ from y → x Listed.⊆ y
    from⊆from→ = Listed.elim-prop e
      where
      e : Listed.Elim-prop _
      e .Listed.Elim-prop.[]ʳ = Listed.elim-prop e′
        where
        e′ : Listed.Elim-prop _
        e′ .Listed.Elim-prop.[]ʳ _ = Listed.⊆-refl

        e′ .Listed.Elim-prop.∷ʳ {y = y} x _ _ z =
          z Listed.∈ Listed.[]     ↔⟨ Listed.∈[]≃ ⟩
          ⊥₀                       ↝⟨ ⊥-elim ⟩□
          z Listed.∈ x Listed.∷ y  □

        e′ .Listed.Elim-prop.is-propositionʳ _ =
          Π-closure ext 1 λ _ →
          Listed.⊆-propositional

      e .Listed.Elim-prop.∷ʳ {y = y₁} x hyp₁ y₂ =
        from (x Listed.∷ y₁) ⊆ from y₂                   ↔⟨⟩
        (∀ z → z ≡ x ∥⊎∥ z ∈ from y₁ → z ∈ from y₂)      ↝⟨ (λ hyp₂ z → Trunc.rec Listed.∈-propositional
                                                                          [ (
            z ≡ x                                                            ↝⟨ Trunc.∣inj₁∣ ⟩
            z ≡ x ∥⊎∥ z ∈ from y₁                                            ↝⟨ hyp₂ z ⟩
            z ∈ from y₂                                                      ↔⟨ ∈from≃ _ ⟩□
            z Listed.∈ y₂                                                    □)
                                                                          , ($⟨ (λ z → hyp₂ z ∘ Trunc.∣inj₂∣) ⟩
            from y₁ ⊆ from y₂                                                ↝⟨ hyp₁ y₂ ⟩
            y₁ Listed.⊆ y₂                                                   ↝⟨ _$ z ⟩□
            (z Listed.∈ y₁ → z Listed.∈ y₂)                                  □)
                                                                          ]) ⟩
        (∀ z → z ≡ x ∥⊎∥ z Listed.∈ y₁ → z Listed.∈ y₂)  ↔⟨ (∀-cong ext λ _ → →-cong ext (inverse Listed.∈∷≃) F.id) ⟩□
        x Listed.∷ y₁ Listed.⊆ y₂                        □

      e .Listed.Elim-prop.is-propositionʳ _ =
        Π-closure ext 1 λ _ →
        Π-closure ext 1 λ _ →
        Listed.⊆-propositional

    -- The function from is injective.

    from-injective : Injective (from {A = A})
    from-injective {x = x} {y = y} =
      from x ≡ from y                    ↔⟨ ≡≃⊆×⊇ ⟩
      from x ⊆ from y × from y ⊆ from x  ↝⟨ Σ-map (from⊆from→ _ _) (from⊆from→ _ _) ⟩
      x Listed.⊆ y × y Listed.⊆ x        ↝⟨ uncurry Listed.⊆-antisymmetric ⟩□
      x ≡ y                              □

    -- Converts one kind of finite subset to another, and returns a
    -- partial correctness result.

    to :
      (x : Finite-subset-of A) →
      ∃ λ (y : Listed.Finite-subset-of A) → from y ≡ x
    to = elim e
      where
      e : Elim _
      e .Elim.[]ʳ = Listed.[] , refl _

      e .Elim.∷ʳ x (y , eq) = x Listed.∷ y , cong (x ∷_) eq

      e .Elim.is-propositionʳ x (y₁ , eq₁) (y₂ , eq₂) =
        Σ-≡,≡→≡
          (from-injective
             (from y₁  ≡⟨ eq₁ ⟩
              x        ≡⟨ sym eq₂ ⟩∎
              from y₂  ∎))
          (is-set _ _)

    -- Another correctness result.

    to-from :
      (x : Listed.Finite-subset-of A) →
      proj₁ (to (from x)) ≡ x
    to-from = Listed.elim-prop e
      where
      e : Listed.Elim-prop _
      e .Listed.Elim-prop.[]ʳ               = refl _
      e .Listed.Elim-prop.∷ʳ x              = cong (x Listed.∷_)
      e .Listed.Elim-prop.is-propositionʳ _ = Listed.is-set

-- The type of listed finite subsets defined above is pointwise
-- equivalent to the type of listed finite subsets defined in Listed.

Listed≃Listed : Finite-subset-of A ≃ Listed.Finite-subset-of A
Listed≃Listed = Eq.↔→≃ (proj₁ ∘ to) from to-from (proj₂ ∘ to)
  where
  open Listed≃Listed

-- The equivalence preserves membership.

∈≃∈ : ∀ y → (x ∈ y) ≃ (x Listed.∈ _≃_.to Listed≃Listed y)
∈≃∈ {x = x} y =
  x ∈ y                                                ↝⟨ ≡⇒↝ _ $ cong (_ ∈_) $ sym $ _≃_.left-inverse-of Listed≃Listed y ⟩
  x ∈ _≃_.from Listed≃Listed (_≃_.to Listed≃Listed y)  ↝⟨ ∈from≃ _ ⟩□
  x Listed.∈ _≃_.to Listed≃Listed y                    □
  where
  open Listed≃Listed

-- Another dependent eliminator (expressed using equality).
--
-- Note that the motive is not required to be propositional.

record Elim′ {A : Type a} (P : Finite-subset-of A → Type p) :
             Type (a ⊔ p) where
  no-eta-equality
  field
    []ʳ     : P []
    ∷ʳ      : ∀ x → P y → P (x ∷ y)
    dropʳ   : ∀ x (p : P y) →
              subst P (drop {x = x} {y = y}) (∷ʳ x (∷ʳ x p)) ≡ ∷ʳ x p
    swapʳ   : ∀ x y (p : P z) →
              subst P (swap {x = x} {y = y} {z = z}) (∷ʳ x (∷ʳ y p)) ≡
              ∷ʳ y (∷ʳ x p)
    is-setʳ : ∀ x → Is-set (P x)

open Elim′ public

elim′ : Elim′ P → (x : Finite-subset-of A) → P x
elim′ {P = P} e x =
  subst P (_≃_.left-inverse-of Listed≃Listed x)
    (Listed.elim e′ (_≃_.to Listed≃Listed x))
  where
  module E = Elim′ e

  e′ : Listed.Elim (P ∘ _≃_.from Listed≃Listed)
  e′ .Listed.[]ʳ = E.[]ʳ

  e′ .Listed.∷ʳ = E.∷ʳ

  e′ .Listed.dropʳ x p =
    subst (P ∘ _≃_.from Listed≃Listed)
      Listed.drop
      (e .∷ʳ x (e .∷ʳ x p))                        ≡⟨ subst-∘ _ _ _ ⟩

    subst P
      (cong (_≃_.from Listed≃Listed) Listed.drop)
      (e .∷ʳ x (e .∷ʳ x p))                        ≡⟨ cong (flip (subst P) _) $ is-set _ _ ⟩

    subst P drop (e .∷ʳ x (e .∷ʳ x p))             ≡⟨ e .dropʳ x p ⟩∎

    e .∷ʳ x p                                      ∎

  e′ .Listed.swapʳ x y p =
    subst (P ∘ _≃_.from Listed≃Listed)
      Listed.swap
      (e .∷ʳ x (e .∷ʳ y p))                        ≡⟨ subst-∘ _ _ _ ⟩

    subst P
      (cong (_≃_.from Listed≃Listed) Listed.swap)
      (e .∷ʳ x (e .∷ʳ y p))                        ≡⟨ cong (flip (subst P) _) $ is-set _ _ ⟩

    subst P swap (e .∷ʳ x (e .∷ʳ y p))             ≡⟨ e .swapʳ x y p ⟩∎

    e .∷ʳ y (e .∷ʳ x p)                            ∎

  e′ .Listed.is-setʳ _ = E.is-setʳ _

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------------
-- Properties for the nest function
------------------------------------------------------------------------------

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

module FOTC.Program.Nest.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat.Type
open import FOTC.Program.Nest.Nest

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

nest-x≡0 : ∀ {n} → N n → nest n ≡ zero
nest-x≡0 nzero = prf
  where postulate prf : nest zero ≡ zero
        {-# ATP prove prf #-}
nest-x≡0 (nsucc {n} Nn) = prf (nest-x≡0 Nn)
  where postulate prf : nest n ≡ zero → nest (succ₁ n) ≡ zero
        {-# ATP prove prf #-}

postulate nest-N : ∀ {n} → N n → N (nest n)
{-# ATP prove nest-N nest-x≡0 #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module README where

import Semantics
import Theory
import Soundness

import Categories.Category.Construction.Models
import Categories.Category.Construction.Classifying
import Categories.Functor.Construction.Inclusion

import Internal

import Examples

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Concrete.Records
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Consensus.Network            as Network
open import LibraBFT.Impl.Consensus.Network.Properties as NetworkProps
open import LibraBFT.Impl.Consensus.RoundManager       as RoundManager
open import LibraBFT.Impl.Consensus.RoundManager.Properties
open import LibraBFT.Impl.IO.OBM.InputOutputHandlers
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.NetworkMsg
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Prelude
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

open Invariants
open RoundManagerTransProps

module LibraBFT.Impl.IO.OBM.Properties.InputOutputHandlers where

module epvvSpec where

  contract
    : ∀ pre Post
      → let ep = pre ^∙ pssSafetyData-rm ∙ sdEpoch
            vv = pre ^∙ rmEpochState ∙ esVerifier in
        (Post (ep , vv) pre [])
      → LBFT-weakestPre epvv Post pre
  contract pre Post pf ._ refl ._ refl ._ refl ._ refl = pf

module handleProposalSpec (now : Instant) (pm : ProposalMsg) where

  open handleProposal now pm

  module _ (pool : SentMessages) (pre : RoundManager) where

    open Invariants.Reqs (pm ^∙ pmProposal) (pre ^∙ lBlockTree)

    record Contract (_ : Unit) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        -- General properties / invariants
        rmInv              : Preserves RoundManagerInv pre post
        invalidProposal    : ¬ (BlockId-correct (pm ^∙ pmProposal)) → pre ≡ post × OutputProps.NoVotes outs
        noEpochChange      : NoEpochChange pre post
        -- Voting
        voteAttemptCorrect : BlockId-correct (pm ^∙ pmProposal)
                           → NoHC1 → Voting.VoteAttemptCorrectWithEpochReq pre post outs (pm ^∙ pmProposal)
        -- voteBuildsOnRC : TODO-2: We will need to know that, if we're sending a Vote, then there
        --                          is a Block b such that the Vote's proposed id is bId B and there
        --                          is a RecordChain (B b) and all the Records in that RecordChain
        --                          are InSys.  This is needed to prove ImplObligation-RC.  However,
        --                          before doing so, it may be worth considering strengthening the
        --                          Concrete PreferredRound proof, so that only IsValidVote is
        --                          required of the implementation, and that is used to construct
        --                          the required RecordChain, independently of the implementation.
        -- QCs
        outQcs∈RM : QCProps.OutputQc∈RoundManager outs post
        qcPost    : QCProps.∈Post⇒∈PreOr (_QC∈NM (P pm)) pre post

    contract : LBFT-weakestPre (handleProposal now pm) Contract pre
    contract =
      epvvSpec.contract pre Post-epvv contract-step₁
      where
      Post-epvv : LBFT-Post (Epoch × ValidatorVerifier)
      Post-epvv = RWS-weakestPre-bindPost unit (λ where (myEpoch , vv) → step₁ myEpoch vv) Contract

      myEpoch = pre ^∙ pssSafetyData-rm ∙ sdEpoch
      vv      = pre ^∙ rmEpochState ∙ esVerifier

      contractBail : ∀ outs → OutputProps.NoMsgs outs → Contract unit pre outs
      contractBail outs noMsgs =
        mkContract reflPreservesRoundManagerInv (const $ refl , OutputProps.NoMsgs⇒NoVotes outs noMsgs) (reflNoEpochChange{pre})
          vac outQcs∈RM qcPost
        where
        vac : BlockId-correct (pm ^∙ pmProposal) → NoHC1 → Voting.VoteAttemptCorrectWithEpochReq pre pre outs (pm ^∙ pmProposal)
        vac _ _ = Voting.mkVoteAttemptCorrectWithEpochReq
                    (Voting.voteAttemptBailed outs (OutputProps.NoMsgs⇒NoVotes outs noMsgs)) tt

        outQcs∈RM : QCProps.OutputQc∈RoundManager outs pre
        outQcs∈RM = QCProps.NoMsgs⇒OutputQc∈RoundManager outs pre noMsgs

        qcPost : QCProps.∈Post⇒∈PreOr _  pre pre
        qcPost qc = Left

      contract-step₁ : Post-epvv (myEpoch , vv) pre []
      proj₁ (contract-step₁ (myEpoch@._ , vv@._) refl) (inj₁ e) pp≡Left =
        contractBail _ refl
      proj₁ (contract-step₁ (myEpoch@._ , vv@._) refl) (inj₂ i) pp≡Left =
        contractBail _ refl
      proj₂ (contract-step₁ (myEpoch@._ , vv@._) refl) unit pp≡Right =
        processProposalMsgMSpec.contract now pm proposalId≡ pre Contract pf
        where

        sdEpoch≡ : pre ^∙ pssSafetyData-rm ∙ sdEpoch ≡ pm ^∙ pmProposal ∙ bEpoch
        sdEpoch≡
          with processProposalSpec.contract pm myEpoch vv
        ...| con rewrite pp≡Right = sym (proj₁ con)

        proposalId≡ : BlockId-correct (pm ^∙ pmProposal)
        proposalId≡
           with processProposalSpec.contract pm myEpoch vv
        ...| con rewrite pp≡Right = proj₂ con

        module PPM = processProposalMsgMSpec now pm proposalId≡

        pf : RWS-Post-⇒ (PPM.Contract pre) Contract
        pf unit st outs con =
          mkContract PPMSpec.rmInv (λ x → ⊥-elim (x proposalId≡)) PPMSpec.noEpochChange
            vac PPMSpec.outQcs∈RM PPMSpec.qcPost
          where
          module PPMSpec = processProposalMsgMSpec.Contract con

          vac : BlockId-correct (pm ^∙ pmProposal) → NoHC1
              → Voting.VoteAttemptCorrectWithEpochReq pre st outs (pm ^∙ pmProposal)
          vac _ nohc = Voting.mkVoteAttemptCorrectWithEpochReq (PPMSpec.voteAttemptCorrect nohc)
                         (Voting.voteAttemptEpochReq! (PPMSpec.voteAttemptCorrect nohc) sdEpoch≡)

    contract! : LBFT-Post-True Contract (handleProposal now pm) pre
    contract! = LBFT-contract (handleProposal now pm) Contract pre contract

module handleVoteSpec (now : Instant) (vm : VoteMsg) where
  open handleVote now vm

  module _ (pool : SentMessages) (pre : RoundManager) where

    record Contract (_ : Unit) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        -- General properties / invariants
        rmInv         : Preserves RoundManagerInv pre post
        noEpochChange : NoEpochChange pre post
        noSDChange    : NoSafetyDataChange pre post
        -- Output
        noVotes       : OutputProps.NoVotes outs
        -- Signatures
        outQcs∈RM : QCProps.OutputQc∈RoundManager outs post
        qcPost    : QCProps.∈Post⇒∈PreOr (_QC∈NM (V vm)) pre post
        -- TODO-2: `handleVote` can create a new QC once it receives enough
        -- votes. We need to be tracking /votes/ here, not QCs

    postulate -- TODO-2: prove (waiting on: refinement of `Contract`)
      contract : LBFT-weakestPre (handleVote now vm) Contract pre

    contract! : LBFT-Post-True Contract (handleVote now vm) pre
    contract! = LBFT-contract (handleVote now vm) Contract pre contract


text:
{-
  Copyright 2019 Lisandra Silva

  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  You may obtain a copy of the License at

      http://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing, software
  distributed under the License is distributed on an "AS IS" BASIS,
  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  See the License for the specific language governing permissions and
  limitations under the License.
-}

open import Prelude
open import Data.Nat.Divisibility

open import StateMachineModel

{-
  This State Machine begins in a state equal to 0 or 1 and if :
    - The current state s is Even then jump to state (s + 2)
    - The current state is Odd jump to state (s + 1)

  We want to prove that a state s always leads-to a state Even
-}

module Examples.SMCounterEven where

  -- DEFINITIONS and proofs about Even and Odd
  Even : ℕ → Set
  Even n = 2 ∣ n

  Odd : ℕ → Set
  Odd = ¬_ ∘ Even

  even? : (n : ℕ) → Dec (Even n)
  even? n = 2 ∣? n

  evenK⇒even2+K : ∀ {k} → Even k → Even (2 + k)
  evenK⇒even2+K (divides q₁ refl) = divides (1 + q₁) refl

  -- The following are mutually recursive properties.
  oddK⇒even1+K : ∀ {k} → Odd k → Even (suc k)
  oddK⇒evenK-1 : ∀ {k} → Odd k → Even (pred k)

  oddK⇒even1+K {zero} x = ⊥-elim (x (divides 0 refl))
  oddK⇒even1+K {suc k} x = evenK⇒even2+K (oddK⇒evenK-1 x)

  oddK⇒evenK-1 {zero} x = ⊥-elim (x (divides 0 refl))
  oddK⇒evenK-1 {suc k} x with even? k
  ...| no imp = ⊥-elim (x (oddK⇒even1+K imp))
  ...| yes prf = prf

  odd1 : Odd 1
  odd1 (divides zero ())
  odd1 (divides (suc q₁) ())

   -----------------------------------------------------------------------------
   -- SPECIFICATION
   -----------------------------------------------------------------------------

  data MyEvent : Set where
    inc  : MyEvent
    inc2 : MyEvent
    -- TODO : Try with an event iddle that doesn't do anything and is in another
    -- EventSet in the weakFairness relation (just to try)

  -- If we are in a state that is odd then the enabled event is inc
  -- otherwise the enabled event is inc2
  data MyEnabled : MyEvent → ℕ → Set where
    odd  : ∀ {n} → Odd n  → MyEnabled inc  n
    even : ∀ {n} → Even n → MyEnabled inc2 n

  MyStateMachine : StateMachine ℕ MyEvent
  MyStateMachine = record
                   { initial =  (0 ≡_) ∪ (1 ≡_)
                   ; enabled = MyEnabled
                   ; action  = λ { {pre} {inc}  cond → 1 + pre
                                 ; {pre} {inc2} cond → 2 + pre }
                   }

  MyEventSet : EventSet {Event = MyEvent}
  MyEventSet inc  = ⊤
  MyEventSet inc2 = ⊤

  data MyWeakFairness : EventSet → Set where
    wf : MyWeakFairness MyEventSet

  MySystem : System ℕ MyEvent
  MySystem = record
             { stateMachine = MyStateMachine
             ; weakFairness = MyWeakFairness
             }

   -----------------------------------------------------------------------------
   -- PROOFS
   -----------------------------------------------------------------------------

  open LeadsTo ℕ MyEvent MySystem

  -- In every state there is always an enabled transition
  alwaysEnabled : ∀ (s : ℕ) → enabledSet MyStateMachine MyEventSet s
  alwaysEnabled s with even? s
  ... | yes p = inc2 , tt , even p
  ... | no ¬p = inc  , tt , odd ¬p

  -- Any state n leads to an Even state
  progressEven : ∀ {n : ℕ} → (n ≡_) l-t Even
  progressEven = viaEvSet
                   MyEventSet wf
                   (λ { inc  ⊤ → hoare λ { refl (odd x)  → oddK⇒even1+K  x }
                      ; inc2 ⊤ → hoare λ { refl (even x) → evenK⇒even2+K x } })
                   (λ { inc  ⊥ → ⊥-elim (⊥ tt)
                      ; inc2 ⊥ → ⊥-elim (⊥ tt) })
                   λ {s} rs n≡s → alwaysEnabled s

  -- QUESTION : Although we don't have weakfairness (WF) on event inc it was
  -- possible to prove this.
  -- ANSWER : This is because of the 2nd constraint in the viaEvSet constructor:
  --      - ∀ event e ∉ WF (in this case only inc) → [P] e [P ∪ Q], in this case
  --   we achieve Q (Even), because the event inc is enabled only in Odd states.

  -- REFACTOR: Maybe m is the one that should be explicit
  myWFR : ∀ {m} → ℕ → Z → Set
  myWFR {m} d s = m ≡ d + s

  -- For every m and even state s, or s is greater than m or there is a distance
  -- x between s and m
  [Q∪Fx] :  ∀ {m} → (s : Z) → Even s
                       → (m ≤ s × Even s) ⊎ ∃[ x ] myWFR {m} x s
  [Q∪Fx] {m} s sEven with m ≤? s
  ... | yes m≤s = inj₁ (m≤s , sEven)
  ... | no  s<m = inj₂ ( m ∸ s , sym (m∸n+n≡m (<⇒≤ (≰⇒> s<m))) )

  -- First constraint for WFR rule
  [P]l-t[Q∪Fx] : ∀ {n m}
                 → (n ≡_) l-t ( ((m ≤_) ∩ Even) ∪ [∃ x ∶ myWFR {m} x ] )
  [P]l-t[Q∪Fx] {n} {m} = viaEvSet
                           MyEventSet wf
                           (λ { inc ⊤
                                    → hoare λ { refl (odd x)
                                      → [Q∪Fx] (1 + n) (oddK⇒even1+K x) }
                              ; inc2 ⊤
                                    → hoare λ { refl (even x)
                                      → [Q∪Fx] (2 + n) (evenK⇒even2+K x) }})
                           (λ { inc  ⊥ → ⊥-elim (⊥ tt)
                              ; inc2 ⊥ → ⊥-elim (⊥ tt) })
                           λ {s} rs n≡s → alwaysEnabled s

  -- If we are at distance 0 from m, which means state s ≡ m, then it leads-to a
  -- state s₁ > m ∩ Even s₁, because or we increment 1 if s is odd or we
  -- increment 2 if s is even.
  d≡0⇒Q : ∀ {m}
          → myWFR {m} 0
            l-t
            ( (m ≤_) ∩ Even )
  d≡0⇒Q {m} = viaEvSet
                MyEventSet wf
                (λ { inc  ⊤
                          → hoare λ { refl (odd x)
                           → m≤n+m m 1 , oddK⇒even1+K x }
                   ; inc2 ⊤
                          → hoare λ { refl (even x)
                            → m≤n+m m 2 , evenK⇒even2+K x }})
                (λ { inc  ⊥ → ⊥-elim (⊥ tt)
                   ; inc2 ⊥ → ⊥-elim (⊥ tt) })
                λ {s} rs F0 → alwaysEnabled s

  -- If we are at distance 1 from m, which means m ≡ s + 1.
  -- If s is odd then s is incremented by 1 (because of the enabling
  -- condition) then we go to an even state s₁ ≡ s + 1 ≡ m.
  -- If if s is even then s is incremented by 2, which leads to a state
  -- s₁ ≡ s + 2 > s + 1 ≡ m. As so, m ≤ s₁ ∩ Even s₁ will always  hold.
  d≡1⇒Q∪d≡0 : ∀ {m}
              → myWFR {m} 1
                l-t
                ( ((m ≤_) ∩ Even) ∪ [∃ x ⇒ _< 1 ∶ myWFR {m} x ] )
  d≡1⇒Q∪d≡0 {m} = viaEvSet
                    MyEventSet wf
                    (λ { inc  ⊤
                          → hoare λ { {ps} refl (odd x)
                           → inj₁ (≤-refl , oddK⇒even1+K x) }
                       ; inc2 ⊤
                         → hoare λ { {ps} refl (even x)
                           → inj₁ (m≤n+m (suc ps) 1 , evenK⇒even2+K x) }})
                    (λ { inc  ⊥ → ⊥-elim (⊥ tt)
                       ; inc2 ⊥ → ⊥-elim (⊥ tt) })
                    λ {s} rs F1 → alwaysEnabled s

  -- Auxiliary properties
  assoc∘comm : ∀ {w s : ℕ} n → n + w + s ≡ w + (n + s)
  assoc∘comm {w} {s} n = trans (cong (_+ s) (+-comm n w)) (+-assoc w n s)

  assoc∘assoc : ∀ {w s : ℕ} n p → (n + p) + w + s ≡ n + w + (p + s)
  assoc∘assoc {w} {s} n p
    rewrite +-assoc n p w
          | +-comm p w
          | +-assoc n (w + p) s
          | +-assoc w p s
          | +-assoc n w (p + s) = refl

  -- If we are at a distance greater o equal to 2 then with we decrease the
  -- distance in 1 or 2, because we can jump 1 or 2 states (inc or onc2)
  -- This property together with d≡0⇒Q and d≡1⇒Q∪d≡0 allows to prove the
  -- second constraint for the WFR rule (see below)
  [d≡2+w]⇒[d≡1+w]∪[d≡w] : ∀ {m w}
                → myWFR {m} (2 + w)
                  l-t
                  ( myWFR {m} (1 + w) ∪ myWFR {m} w )
  [d≡2+w]⇒[d≡1+w]∪[d≡w] {m} {w} =
    viaEvSet
      MyEventSet wf
      (λ { inc  ⊤
                → hoare λ { {ps} refl (odd x) → inj₁ (assoc∘assoc 1 1) }
         ; inc2 ⊤
                → hoare λ { {ps} refl enEv → inj₂ (assoc∘comm 2) }})
      (λ { inc  ⊥ → ⊥-elim (⊥ tt)
         ; inc2 ⊥ → ⊥-elim (⊥ tt) })
      λ {s} rs F2+d → alwaysEnabled s

  -- Second constraint for WFR rule
  [Fw]l-t[Q∪Fx] : ∀ {m w}
                  → myWFR {m} w
                    l-t
                    ( ((m ≤_) ∩ Even) ∪ [∃ x ⇒ _< w ∶ myWFR {m} x ] )
  [Fw]l-t[Q∪Fx] {m} {zero}        = viaTrans d≡0⇒Q (viaInv (λ rs x → inj₁ x))
  [Fw]l-t[Q∪Fx] {m} {suc zero}    = d≡1⇒Q∪d≡0
  [Fw]l-t[Q∪Fx] {m} {suc (suc w)} =
    viaTrans
      [d≡2+w]⇒[d≡1+w]∪[d≡w]
      (viaInv (λ { rs (inj₁ mfr[1+w]) → inj₂ ( 1 + w , s≤s ≤-refl , mfr[1+w] )
                 ; rs (inj₂ mfr[w])   → inj₂ ( w , s≤s (m≤n+m w 1) , mfr[w]) }))

  ------------------------------------------------------------------------------
  -- MAIN PROPERTY
  ------------------------------------------------------------------------------
  -- From any n, we can reach any state m such that m is Even
  progressAlwaysEven : ∀ {n m : ℕ} → (n ≡_) l-t ((m ≤_) ∩ Even)
  progressAlwaysEven {n} {m} = viaWFR
                                 (myWFR {m})
                                 [P]l-t[Q∪Fx]
                                 λ w → [Fw]l-t[Q∪Fx]

max_stars_repo_name: lisandrasilva/agda-liveness

max_issues_repo_name: lisandrasilva/agda-liveness

max_forks_repo_name: lisandrasilva/agda-liveness


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

module Categories.Functor.Instance.0-Truncation where

-- 0-trucation of groupoids as a functor from Groupoids to Setoids.
--
-- This is the right-adjoint of the inclusion functor from Setoids to
-- Groupoids (see Categories.Functor.Adjoint.Instance.ZeroTruncation)

import Function
open import Function.Equality using (_⟶_)
open import Relation.Binary using (Setoid)

open import Categories.Category using (Category; _[_≈_])
open import Categories.Functor hiding (id)
open import Categories.Category.Groupoid using (Groupoid)
open import Categories.Category.Instance.Groupoids using (Groupoids)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; _≃_)

Trunc : ∀ {o ℓ e} → Functor (Groupoids o ℓ e) (Setoids o ℓ)
Trunc {o} {ℓ} {e} = record
   { F₀           = TruncSetoid
   ; F₁           = λ {G H} F → TruncMap {G} {H} F
   ; identity     = Function.id
   ; homomorphism = λ {_ _ _ F G} f → F₁ G (F₁ F f)
   ; F-resp-≈     = λ {G H} → TruncRespNI {G} {H}
   }
   where
     open Groupoid using (category)
     open Functor

     TruncSetoid : Groupoid o ℓ e → Setoid o ℓ
     TruncSetoid G = record
       { Carrier       = Obj
       ; _≈_           = _⇒_
       ; isEquivalence = record
         { refl  = id
         ; sym   = _⁻¹
         ; trans = λ f g → g ∘ f
         }
       }
       where open Groupoid G

     TruncMap : ∀ {G H} → Functor (category G) (category H) →
                TruncSetoid G ⟶ TruncSetoid H
     TruncMap F = record { _⟨$⟩_ = F₀ F ; cong  = F₁ F }

     TruncRespNI : ∀ {G H : Groupoid o ℓ e}
                   {E F : Functor (category G) (category H)} →
                   E ≃ F → Setoids o ℓ [ TruncMap {G} {H} E ≈ TruncMap {G} {H} F ]
     TruncRespNI {_} {H} {_} {F} μ {a} f = F₁ F f ∘ ⇒.η a
       where
         open Groupoid H
         open NaturalIsomorphism μ

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Relation.Nullary.Decidable using (False; toWitnessFalse)
open import Data.Fin using (Fin; _≟_)
open import Data.Nat using (ℕ; suc)
open import Data.Product using (_×_; _,_)

open import Common

data Global (n : ℕ) : Set where
  endG : Global n
  msgSingle : (p q : Fin n) -> p ≢ q -> Label -> Global n -> Global n

private
  variable
    n : ℕ
    p p′ q q′ r s : Fin n
    l l′ : Label
    g gSub gSub′ : Global n

msgSingle′ : (p q : Fin n) -> {False (p ≟ q)} -> Label -> Global n -> Global n
msgSingle′ p q {p≢q} l gSub = msgSingle p q (toWitnessFalse p≢q) l gSub

size-g : ∀ { n : ℕ } -> (g : Global n) -> ℕ
size-g endG = 0
size-g (msgSingle _ _ _ _ gSub) = suc (size-g gSub)

size-g-reduces :
  ∀ { p≢q }
  -> g ≡ msgSingle {n} p q p≢q l gSub
  -> size-g g ≡ suc (size-g gSub)
size-g-reduces {g = endG} ()
size-g-reduces {g = msgSingle _ _ _ _ gSub} refl = refl

msgSingle-subst-left :
  ∀ { p≢q }
  -> g ≡ msgSingle {n} p q p≢q l gSub
  -> (p≡p′ : p ≡ p′)
  -> g ≡ msgSingle {n} p′ q (≢-subst-left p≢q p≡p′) l gSub
msgSingle-subst-left refl refl = refl

msgSingle-subst-right :
  ∀ { p≢q }
  -> g ≡ msgSingle {n} p q p≢q l gSub
  -> (q≡q′ : q ≡ q′)
  -> g ≡ msgSingle {n} p q′ (≢-subst-right p≢q q≡q′) l gSub
msgSingle-subst-right refl refl = refl

msgSingle-injective :
  ∀ { p≢q p′≢q′ }
  -> msgSingle {n} p q p≢q l gSub ≡ msgSingle p′ q′ p′≢q′ l′ gSub′
  -> p ≡ p′ × q ≡ q′ × l ≡ l′ × gSub ≡ gSub′
msgSingle-injective refl = refl , refl , refl , refl

data _-_→g_ {n : ℕ} : Global n -> Action n -> Global n -> Set where
  →g-prefix :
    ∀ { p≢q p≢q′ }
    -> (msgSingle p q p≢q l gSub) - (action p q p≢q′ l) →g gSub
  →g-cont :
    ∀ { p≢q r≢s }
    -> gSub - (action p q p≢q l) →g gSub′
    -> p ≢ r
    -> q ≢ r
    -> p ≢ s
    -> q ≢ s
    -> (msgSingle r s r≢s l′ gSub) - (action p q p≢q l) →g (msgSingle r s r≢s l′ gSub′)

max_stars_repo_name: fangyi-zhou/mpst-in-agda

max_issues_repo_name: fangyi-zhou/mpst-in-agda

max_forks_repo_name: fangyi-zhou/mpst-in-agda


text:
-- Andreas, 2012-04-21
-- {-# OPTIONS -v tc.proj.like:100 -v tc.with:100 #-}
module ReifyProjectionLike where

data Maybe (A : Set) : Set where
  just    : A → Maybe A

fromJust : (A : Set) → Maybe A → A
fromJust A (just a) = a

data Sing (A : Set) : A -> Set where
  sing : (a : A) -> Sing A a

succeed : (A : Set) -> Maybe A -> Set
succeed A m with sing (fromJust A m)
... | _ = A

fail : (A : Set) -> Maybe A -> Set
fail A m with sing (fromJust A m)
... | (just x) = x

-- error message is wrong:
--
--   just is not a constructor of the datatype Sing
--   when checking that the pattern just x has type Sing A (fromJust m)
--
-- the "A" got dropped from "fromJust"
--
-- correct message is
--
--   just is not a constructor of the datatype Sing
--   when checking that the pattern just x has type Sing A (fromJust A m)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

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

module Categories.Category.Monoidal.Braided.Properties
  {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (BM : Braided M) where

open import Data.Product using (_,_)

open import Categories.Category.Monoidal.Properties M
open import Categories.Category.Monoidal.Reasoning M
open import Categories.Category.Monoidal.Utilities M
open import Categories.Functor using (Functor)
open import Categories.Morphism C using (module ≅)
open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟)
open import Categories.Morphism.Reasoning C hiding (push-eq)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
  using (push-eq)

open Category C
open Braided BM
open Commutation C

private
  variable
    X Y Z : Obj

  -- A shorthand for the braiding
  B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X
  B {X} {Y} = braiding.⇒.η (X , Y)

  -- It's easier to prove the following lemma, which is the desired
  -- coherence theorem moduolo application of the |-⊗ unit| functor.
  -- Because |-⊗ unit| is equivalent to the identity functor, the
  -- lemma and the theorem are equivalent.

  -- The following diagram illustrates the hexagon that we are
  -- operating on. The main outer hexagon is hexagon₁, the braiding
  -- coherence, instantiated with X, 1 and 1 (Here we denote the unit
  -- by 1 for brevity).
  -- In the middle are X1 and 1X along with morphisms towards them.
  -- The lower hexagon (given by the double lines) commutes and is
  -- an intermediary in the final proof. It is there to effectively
  -- get rid of the top half of the main hexagon.
  -- The rest of the proof is isolating the bottom left triangle
  -- which represents our desired identity. It is doing that by
  -- proving that the pentagon to the right of it commutes.
  -- The pentagon commuting is, in turn, proved by gluing the
  -- rightmost "square" onto the middle triangle.
  --
  --
  --       ┌─────>  X(11)  ─────────>  (11)X ──────┐
  --      ┌┘ α        │        B         │       α └┐
  --     ┌┘           │id⊗λ              │λ⊗id     └┐
  --    ┌┘            V                  V           V
  --  (X1)1 ═══════> X1  ════════════>  1X <══════ 1(1X)
  --    ╚╗   ρ⊗id     Λ <───┐  B              λ      Λ
  --     ╚╗           │λ⊗id └────────┐              ╔╝
  --      ╚╗          │           λ   └┐           ╔╝
  --       ╚═════>  (1X)1  ═════════>  1(X1)  ═════╝
  --       B⊗id                α                id⊗B

  braiding-coherence⊗unit : [ (X ⊗₀ unit) ⊗₀ unit ⇒ X ⊗₀ unit ]⟨
               B ⊗₁ id                       ⇒⟨ (unit ⊗₀ X) ⊗₀ unit ⟩
               unitorˡ.from ⊗₁ id
             ≈ unitorʳ.from ⊗₁ id
             ⟩
  braiding-coherence⊗unit = cancel-fromˡ braiding.FX≅GX (
    begin
      B ∘ unitorˡ.from ⊗₁ id ∘ B ⊗₁ id                               ≈⟨ pullˡ (⟺ (glue◽◃ unitorˡ-commute-from coherence₁)) ⟩
      (unitorˡ.from ∘ id ⊗₁ B ∘ associator.from) ∘ B ⊗₁ id           ≈⟨ assoc²' ⟩
      unitorˡ.from ∘ id ⊗₁ B ∘ associator.from ∘ B ⊗₁ id             ≈⟨ refl⟩∘⟨ hexagon₁ ⟩
      unitorˡ.from ∘ associator.from ∘ B ∘ associator.from            ≈⟨ pullˡ coherence₁ ⟩
      unitorˡ.from ⊗₁ id ∘ B ∘ associator.from                       ≈˘⟨ pushˡ (braiding.⇒.commute _) ⟩
      (B ∘ id ⊗₁ unitorˡ.from) ∘ associator.from                     ≈⟨ pullʳ triangle ⟩
      B ∘ unitorʳ.from ⊗₁ id
    ∎)

-- The desired theorem follows from |braiding-coherence⊗unit| by
-- translating it along the right unitor (which is a natural iso).

braiding-coherence : [ X ⊗₀ unit ⇒ X ]⟨
                       B              ⇒⟨ unit ⊗₀ X ⟩
                       unitorˡ.from
                     ≈ unitorʳ.from
                     ⟩
braiding-coherence = push-eq unitorʳ-naturalIsomorphism (begin
  (unitorˡ.from ∘ B) ⊗₁ id           ≈⟨ homomorphism ⟩
  (unitorˡ.from ⊗₁ id) ∘ (B ⊗₁ id)   ≈⟨ braiding-coherence⊗unit ⟩
  unitorʳ.from  ⊗₁ id                ∎)
  where open Functor (-⊗ unit)

-- Shorthands for working with isomorphisms.

open ≅ using () renaming (refl to idᵢ; sym to _⁻¹)
infixr 9 _∘ᵢ_
private
  _∘ᵢ_ = λ {A B C} f g → ≅.trans {A} {B} {C} g f
  Bᵢ   = braiding.FX≅GX
  B⁻¹  = λ {X} {Y} → braiding.⇐.η (X , Y)

-- Variants of the hexagon identities defined on isos.

hexagon₁-iso : idᵢ ⊗ᵢ Bᵢ ∘ᵢ associator ∘ᵢ Bᵢ {X , Y} ⊗ᵢ idᵢ {Z}  ≃
               associator ∘ᵢ Bᵢ {X , Y ⊗₀ Z} ∘ᵢ associator
hexagon₁-iso = ⌞ hexagon₁ ⌟

hexagon₂-iso : (Bᵢ ⊗ᵢ idᵢ ∘ᵢ associator ⁻¹) ∘ᵢ idᵢ {X} ⊗ᵢ Bᵢ {Y , Z} ≃
               (associator ⁻¹ ∘ᵢ Bᵢ {X ⊗₀ Y , Z}) ∘ᵢ associator ⁻¹
hexagon₂-iso = ⌞ hexagon₂ ⌟

-- A variants of the above coherence law defined on isos.

braiding-coherence-iso : unitorˡ ∘ᵢ Bᵢ ≃ unitorʳ {X}
braiding-coherence-iso = ⌞ braiding-coherence ⌟

-- The inverse of the braiding is also a braiding on M.

inv-Braided : Braided M
inv-Braided = record
  { braiding = niHelper (record
    { η       = λ _ → B⁻¹
    ; η⁻¹     = λ _ → B
    ; commute = λ{ (f , g) → braiding.⇐.commute (g , f) }
    ; iso     = λ{ (X , Y) → record
      { isoˡ = braiding.iso.isoʳ (Y , X)
      ; isoʳ = braiding.iso.isoˡ (Y , X) } }
    })
  ; hexagon₁ = _≃_.to-≈ hexagon₂-iso
  ; hexagon₂ = _≃_.to-≈ hexagon₁-iso
  }

-- A variant of the above coherence law for the inverse of the braiding.

inv-braiding-coherence : [ unit ⊗₀ X ⇒ X ]⟨
                           B⁻¹            ⇒⟨ X ⊗₀ unit ⟩
                           unitorʳ.from
                         ≈ unitorˡ.from
                         ⟩
inv-braiding-coherence = ⟺ (switch-fromtoʳ Bᵢ braiding-coherence)

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: TOTBWF/agda-categories

max_forks_repo_name: TOTBWF/agda-categories


text:
module Implicits.Resolution.Ambiguous.Undecidable where

open import Prelude hiding (Dec)

open import Relation.Nullary
open import Relation.Nullary.Decidable as DecM
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Binary.HeterogeneousEquality as H using ()

open import Implicits.Syntax
open import Implicits.Resolution.Ambiguous.Resolution
open import Implicits.Resolution.Ambiguous.Semantics
open import Implicits.Resolution.Ambiguous.SystemFEquiv
open import Implicits.Resolution.Embedding
open import Implicits.Resolution.Embedding.Lemmas

open import SystemF.Everything as F using ()

{-
  Assuming undecidability of the type inhabitation problem for System F
  (as proven by e.g. Barendregt) we can prove the undecidability of Ambiguous resolution
-}

private
  -- type of inhabitation problem decider
  ?:-Dec : Set
  ?:-Dec = ∀ {n ν} (Γ : F.Ctx ν n) (a : F.Type ν) → Dec (∃ λ t → Γ F.⊢ t ∈ a)

module Undecidable (?:-undec : ¬ ?:-Dec) where

  -- type of decider for ambiguous resolution
  ⊢ᵣ-Dec : Set
  ⊢ᵣ-Dec = ∀ {ν} (Δ : ICtx ν) (a : Type ν) → Dec (Δ ⊢ᵣ a)

  -- proof that such a decider would imply a decider for type inhabitation problem
  reduction : ⊢ᵣ-Dec → ?:-Dec
  reduction f Γ x = DecM.map (equivalent' Γ x) (f ⟦ Γ ⟧ctx← ⟦ x ⟧tp←)

  -- completing the proof
  undecidable : ¬ ⊢ᵣ-Dec
  undecidable f = ?:-undec (reduction f)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the sublist relation for types which have
-- a decidable equality. This is commonly known as Order Preserving
-- Embeddings (OPE).
------------------------------------------------------------------------

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

open import Relation.Binary
open import Agda.Builtin.Equality using (_≡_)

module Data.List.Relation.Binary.Sublist.DecPropositional
  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
  where

open import Data.List.Relation.Binary.Equality.DecPropositional _≟_
  using (_≡?_)
import Data.List.Relation.Binary.Sublist.DecSetoid as DecSetoidSublist
import Data.List.Relation.Binary.Sublist.Propositional as PropositionalSublist
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Re-export core definitions and operations

open PropositionalSublist {A = A} public
open DecSetoidSublist (decSetoid _≟_) using (_⊆?_) public

------------------------------------------------------------------------
-- Additional relational properties

⊆-isDecPartialOrder : IsDecPartialOrder _≡_ _⊆_
⊆-isDecPartialOrder = record
  { isPartialOrder = ⊆-isPartialOrder
  ; _≟_            = _≡?_
  ; _≤?_           = _⊆?_
  }

⊆-decPoset : DecPoset a a a
⊆-decPoset = record
  { isDecPartialOrder = ⊆-isDecPartialOrder
  }


text:
module _ where

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

postulate
  PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

{-# BUILTIN PATHP        PathP     #-}

postulate
  A : Set
  a : A
  b : A
  p : PathP (\ _ → A) a b

test1 : ∀ {p : PathP (\ _ → A) a a} {P : A → Set} → P (p i0) → P a
test1 x = x

test2 : ∀ {P : A → Set} → P (p i0) → P a
test2 x = x

q : (x : Nat) → PathP (\ _ → Nat) x x
q zero i = zero
q (suc n) i = suc (q n i)

test3 : ∀ {P : Nat → Set}{n : Nat} → P (q n i0) → P n
test3 x = x

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module NothingAppliedToHiddenArg where

bad = {x}


text:
module Utils.Decidable where

open import Data.Nat
open import Data.Char
open import Data.String
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable hiding (True; False)
open import Relation.Nullary
open import Data.Product
open import Data.Sum
open import Function
import Level as L

{-
A type class for decidable types.

The part we actually end up using in the formal semantics proofs is
mostly decidable equality (_≡⁇_).
-}

_=>_ : ∀ {α β} → Set α → Set β → Set (α L.⊔ β)
Dict => A = ⦃ _ : Dict ⦄ → A
infixr 5 _=>_

record Decidable {a}(A : Set a) : Set a where
  constructor rec
  field
    decide : Dec A

DecRel : ∀ {a b}{A : Set a}{B : Set b} → (A → B → Set (a L.⊔ b)) → Set (a L.⊔ b)
DecRel Rel = ∀ {x y} → Decidable (Rel x y)

DecEq : ∀ {a} → Set a → Set a
DecEq A = DecRel (_≡_ {_} {A})

_⁇ : ∀ {a} A → Decidable {a} A => Dec A
_⁇ A ⦃ dict ⦄ = Decidable.decide dict

_≡⁇_ : ∀ {a A} → DecEq {a} A => ((x y : A) → Dec (x ≡ y))
x ≡⁇ y = (x ≡ y) ⁇

True : ∀ {a} A → Decidable {a} A => Set
True A = T ⌊ A ⁇ ⌋

F : Bool → Set
F = T ∘ not

False : ∀ {a} A → Decidable {a} A => Set
False A = F ⌊ A ⁇ ⌋

_≤⁇_ : ∀ a b → Dec (a ≤ b)
_≤⁇_ = _≤?_

_<⁇_ : ∀ a b → Dec (a < b)
a <⁇ b = suc a ≤⁇ b

module _ where
  open import Data.Nat.Properties
  _≤′⁇_ : ∀ a b → Dec (a ≤′ b)
  _≤′⁇_ a b with a ≤⁇ b
  ... | yes p = yes (≤⇒≤′ p)
  ... | no  p = no (p ∘ ≤′⇒≤)

_<′⁇_ : ∀ a b → Dec (a <′ b)
a <′⁇ b = suc a ≤′⁇ b

instance
  DecEqBool : DecEq Bool
  DecEqBool = rec (_ Data.Bool.≟ _)

instance
  DecEqChar : DecEq Char
  DecEqChar = rec (_ Data.Char.≟ _)

module _ where
  open import Data.Fin
  open import Data.Fin.Properties

  instance
    DecEqFin : ∀ {n} → DecEq (Fin n)
    DecEqFin = rec (_ Data.Fin.Properties.≟ _)

instance
  DecEqℕ : DecEq ℕ
  DecEqℕ = rec (_ Data.Nat.≟ _)

instance
  DecEqString : DecEq String
  DecEqString = rec (_ Data.String.≟ _)

instance
  Decℕ≤ : DecRel _≤_
  Decℕ≤ = rec (_ ≤⁇ _)

instance
  Decℕ≤′ : DecRel _≤′_
  Decℕ≤′ = rec (_ ≤′⁇ _)

-- Conversions between decidable / boolean
--------------------------------------------------

T→∧ : ∀ {a b} → T (a ∧ b) → T a × T b
T→∧ {true} {true} x = _
T→∧ {true} {false} ()
T→∧ {false} ()

∧→T : ∀ {a b} → T a → T b → T (a ∧ b)
∧→T {true} {true} p1 p2 = _
∧→T {true} {false} p1 ()
∧→T {false} () p2

F-not-elim : ∀ {b} → F (not b) → T b
F-not-elim {true} p = p
F-not-elim {false} p = p

F-not-add : ∀ {b} → T b → F (not b)
F-not-add {true}  p = p
F-not-add {false} p = p

F-not-≡ : ∀ b → T b ≡ F (not b)
F-not-≡ true  = refl
F-not-≡ false = refl

TrueA→A : ∀ {a A}⦃ _ : Decidable {a} A ⦄ → True A → A
TrueA→A = toWitness

FalseA→¬A : ∀ {a A}⦃ _ : Decidable {a} A ⦄ → False A → ¬ A
FalseA→¬A = toWitnessFalse

A→TrueA : ∀ {a A}⦃ _ : Decidable {a} A ⦄ → A → True A
A→TrueA = fromWitness

¬A→FalseA : ∀ {a A}⦃ _ : Decidable {a} A ⦄ → ¬ A → False A
¬A→FalseA = fromWitnessFalse

T→≡true : ∀ {b} → T b → b ≡ true
T→≡true {true} p = refl
T→≡true {false} ()

≡true→T : ∀ {b} → b ≡ true → T b
≡true→T {true} p = _
≡true→T {false} ()

≡false→F : ∀ {b} → b ≡ false → F b
≡false→F {true} ()
≡false→F {false} p = _

F→≡false : ∀ {b} → F b → b ≡ false
F→≡false {true} ()
F→≡false {false} p = refl

A→≡true : ∀ {a A}{Q : Dec {a} A} → A → ⌊ Q ⌋ ≡ true
A→≡true = T→≡true ∘ fromWitness

¬A→≡false : ∀ {a A}{Q : Dec {a} A} → ¬ A → ⌊ Q ⌋ ≡ false
¬A→≡false = F→≡false ∘ fromWitnessFalse

≡true→A : ∀ {a A}{Q : Dec {a} A} → ⌊ Q ⌋ ≡ true → A
≡true→A = toWitness ∘ ≡true→T

≡false→¬A : ∀ {a A}{Q : Dec {a} A} → ⌊ Q ⌋ ≡ false → ¬ A
≡false→¬A = toWitnessFalse ∘ ≡false→F

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

instance
  Dec¬ :
    ∀ {α A}
    →  Decidable {α} A
    => Decidable (¬ A)

  Dec¬ {_}{A} = rec dec¬ where

    dec¬ : Dec (¬ A)
    dec¬ with A ⁇
    ... | yes p = no (λ z → z p)
    ... | no ¬p = yes ¬p

instance
  Dec⊎ :
    ∀ {α β A B}
    →  Decidable {α} A
    => Decidable {β} B
    => Decidable (A ⊎ B)

  Dec⊎ {_}{_}{A}{B} = rec dec⊎ where

    dec⊎ : Dec (A ⊎ B)
    dec⊎ with A ⁇ | B ⁇
    ... | yes p   | _      = yes (inj₁ p)
    ... | _       | yes p  = yes (inj₂ p)
    ... | no ¬p₁  | no ¬p₂ = no [ ¬p₁ , ¬p₂ ]′

instance
  Dec× :
    ∀ {α β A B}
    →  Decidable {α} A
    => Decidable {β} B
    => Decidable (A × B)

  Dec× {_}{_}{A}{B} = rec dec× where

    dec× : Dec (A × B)
    dec× with A ⁇ | B ⁇
    ... | yes p | yes p₁ = yes (p , p₁)
    ... | yes p | no ¬p  = no (¬p ∘ proj₂)
    ... | no ¬p | _      = no (¬p ∘ proj₁)

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
-- pull in Haskell Ints
module int where

open import bool
open import string

postulate
  int : Set
  int0 : int
  int1 : int
  _+int_ : int → int → int
  _*int_ : int → int → int
  _-int_ : int → int → int
  string-to-int : string → int
  is-zero-int : int → 𝔹

{-# COMPILED_TYPE int Int #-}
{-# COMPILED int0 0 #-}
{-# COMPILED int1 1 #-}
{-# COMPILED _+int_ (+) #-}
{-# COMPILED _*int_ (*) #-}
{-# COMPILED _-int_ (-) #-}
{-# COMPILED string-to-int (\ x -> read x :: Int) #-}
{-# COMPILED is-zero-int ((==) 0) #-}

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- {-# OPTIONS -v tc.rec:100 -v tc.signature:20 #-}

module Issue414 where

record P : Set₁ where
  field
    q : Set

  x : P
  x = record { q = q }
-- Andreas 2011-05-19
-- record constructor should have been added to the signature
-- before record module is constructed!


text:
------------------------------------------------------------------------
-- Contexts, variables, context morphisms, context extensions, etc.
------------------------------------------------------------------------

-- The contexts, variables, etc. are parametrised by a universe.

open import Data.Universe.Indexed

module deBruijn.Context
  {i u e} (Uni : IndexedUniverse i u e) where

-- Contexts, variables, context morphisms, etc.

import deBruijn.Context.Basics as Basics
open Basics Uni public

-- Context extensions with the rightmost element in the outermost
-- position.

import deBruijn.Context.Extension.Right as Right
open Right Uni public

-- Context extensions with the leftmost element in the outermost
-- position.

import deBruijn.Context.Extension.Left as Left
open Left Uni public

-- The two definitions of context extensions are isomorphic.

import deBruijn.Context.Extension.Isomorphic as Isomorphic
open Isomorphic Uni public

-- An abstraction: term-like things.

import deBruijn.Context.Term-like as Term-like
open Term-like Uni public

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
data D : Set where
  c : D
  s : D → D

predD : D → D
predD c = c
predD (s x) = x

f : D → D
f c = c
f (s n) with c
f x@(s _) | c = x
f (s _)   | s _ = c

data E : D → Set where
  e : E c
  s : ∀ {x} → E x → E (s x)

predE : ∀ {d} → E d → E (predD d)
predE e     = e
predE (s x) = x

g : ∀ {d} → E d → E (predD d)
g e = e
g (s x) with x
g y@(s _) | s z = predE y
g (s z@e) | e   = predE z


text:
module Everything where

import Prelude
import Stack

import Syntax

import ProposedSemantics
import Semantics.Ono
import Semantics.BozicDosen
import Semantics.AlechinaEtAl
import Semantics.Iemhoff

import CompleteProposedSemantics
import CompleteSemantics.Ono
import CompleteSemantics.BozicDosen
import CompleteSemantics.AlechinaEtAl
import CompleteSemantics.Iemhoff


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

open import Prelude hiding (sym; refl)
open import Relation.Binary

module Relation.Binary.Lattice {ℓ₁ ℓ₂ ℓ₃} {𝑆 : Type ℓ₁} (totalOrder : TotalOrder 𝑆 ℓ₂ ℓ₃) where

open TotalOrder totalOrder

import Path as ≡

min-max : 𝑆 → 𝑆 → 𝑆 × 𝑆
min-max x y = bool′ (y , x) (x , y) (x <ᵇ y)

_⊔_ : 𝑆 → 𝑆 → 𝑆
x ⊔ y = snd (min-max x y)

_⊓_ : 𝑆 → 𝑆 → 𝑆
x ⊓ y = fst (min-max x y)

min-max-assoc : ∀ x y z → map-Σ (_⊓ z) (_⊔ z) (min-max x y) ≡ map-Σ (x ⊓_) (x ⊔_) (min-max y z)
min-max-assoc x y z with x <? y | inspect (x <ᵇ_) y | y <? z | inspect (y <ᵇ_) z
min-max-assoc x y z | yes x≤y | 〖 xyp 〗 | yes y≤z | 〖 yzp 〗 with x <? z
min-max-assoc x y z | yes x≤y | 〖 xyp 〗 | yes y≤z | 〖 yzp 〗 | yes x≤z = cong₂ _,_ (cong (fst ∘ bool _ _) (≡.sym xyp)) (cong (snd ∘ bool _ _) yzp)
min-max-assoc x y z | yes x≤y | 〖 xyp 〗 | yes y≤z | 〖 yzp 〗 | no  x≥z = ⊥-elim (x≥z (<-trans x≤y y≤z))
min-max-assoc x y z | no  x≥y | 〖 xyp 〗 | yes y≤z | 〖 yzp 〗 = cong (_, (x ⊔ z)) (cong (fst ∘ bool _ _) yzp ; cong (fst ∘ bool _ _) (≡.sym xyp))
min-max-assoc x y z | yes x≤y | 〖 xyp 〗 | no  y≥z | 〖 yzp 〗 = cong ((x ⊓ z) ,_) (cong (snd ∘ bool _ _) yzp ; cong (snd ∘ bool _ _) (≡.sym xyp))
min-max-assoc x y z | no  x≥y | 〖 xyp 〗 | no  y≥z | 〖 yzp 〗 with x <? z
min-max-assoc x y z | no  x≥y | 〖 xyp 〗 | no  y≥z | 〖 yzp 〗 | no  x≥z = cong₂ _,_ (cong (fst ∘ bool _ _) yzp) (cong (snd ∘ bool _ _) (≡.sym xyp))
min-max-assoc x y z | no  x≥y | 〖 xyp 〗 | no  y≥z | 〖 yzp 〗 | yes x≤z = cong₂ _,_ (cong (fst ∘ bool _ _) yzp ; lemma) (lemma ; cong (snd ∘ bool _ _) (≡.sym xyp))
  where
  lemma : z ≡ x
  lemma = antisym (≤-trans (≮⇒≥ y≥z) (≮⇒≥ x≥y)) (<⇒≤ x≤z)

⊓-assoc : ∀ x y z → (x ⊓ y) ⊓ z ≡ x ⊓ (y ⊓ z)
⊓-assoc x y z = cong fst (min-max-assoc x y z)

⊔-assoc : ∀ x y z → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z)
⊔-assoc x y z = cong snd (min-max-assoc x y z)

min-max-comm : ∀ x y → min-max x y ≡ min-max y x
min-max-comm x y with x <? y | y <? x
min-max-comm x y | yes x<y | yes y<x = ⊥-elim (asym x<y y<x)
min-max-comm x y | no  x≮y | yes y<x = ≡.refl
min-max-comm x y | yes x<y | no  y≮x = ≡.refl
min-max-comm x y | no  x≮y | no  y≮x = cong₂ _,_ (conn y≮x x≮y) (conn x≮y y≮x)

⊓-comm : ∀ x y → x ⊓ y ≡ y ⊓ x
⊓-comm x y = cong fst (min-max-comm x y)

⊔-comm : ∀ x y → x ⊔ y ≡ y ⊔ x
⊔-comm x y = cong snd (min-max-comm x y)

min-max-idem : ∀ x → min-max x x ≡ (x , x)
min-max-idem x = bool {P = λ r → bool′ (x , x) (x , x) r ≡ (x , x)} ≡.refl ≡.refl (x <ᵇ x)

⊓-idem : ∀ x → x ⊓ x ≡ x
⊓-idem x = cong fst (min-max-idem x)

⊔-idem : ∀ x → x ⊔ x ≡ x
⊔-idem x = cong snd (min-max-idem x)

≤⊔ : ∀ x y → x ≤ x ⊔ y
≤⊔ x y with x <? y
≤⊔ x y | yes x<y = <⇒≤ x<y
≤⊔ x y | no  x≮y = refl

⊓≤ : ∀ x y → x ⊓ y ≤ x
⊓≤ x y with x <? y
⊓≤ x y | yes x<y = refl
⊓≤ x y | no  x≮y = ≮⇒≥ x≮y

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import HoTT
open import cohomology.CupProduct.OnEM.InAllDegrees
open import cohomology.CupProduct.OnEM.CommutativityInAllDegrees
open import cohomology.EMModel
open import cohomology.Theory
open import groups.ToOmega
open import homotopy.EilenbergMacLane
open import homotopy.EilenbergMacLaneFunctor
open import homotopy.Freudenthal
open import homotopy.SuspensionLoopSpaceInverse

module cohomology.CupProduct.Definition {i} (X : Ptd i) where

private
  module M {k} (A : AbGroup k) = CohomologyTheory (EM-Cohomology A)
  open M

⊙×-diag : X ⊙→ X ⊙× X
⊙×-diag = (λ x → x , x) , idp

smin-map : ∀ {j k} {Y : Ptd j} {Z : Ptd k}
  → X ⊙→ Y
  → X ⊙→ Z
  → X ⊙→ Y ⊙× Z
smin-map f g = ⊙×-fmap f g ⊙∘ ⊙×-diag

smin-map-⊙×-swap : ∀ {j k} (Y : Ptd j) (Z : Ptd k)
  (f : X ⊙→ Y)
  (g : X ⊙→ Z)
  → ⊙×-swap ⊙∘ smin-map g f == smin-map f g
smin-map-⊙×-swap Y Z (_ , idp) (_ , idp) = idp

module _ (G : AbGroup i) (H : AbGroup i) where

  private
    module G⊗H = TensorProduct G H
    module H⊗G = TensorProduct H G
  open EMExplicit

  ⊙Ω×-cp-seq : ∀ (m n : ℕ) → (⊙Ω (⊙EM G (S m)) ⊙× ⊙Ω (⊙EM H (S n))) ⊙–→ ⊙Ω (⊙EM G⊗H.abgroup (S (m + n)))
  ⊙Ω×-cp-seq m n =
    ⊙<– (spectrum G⊗H.abgroup (m + n)) ◃⊙∘
    ⊙×-cp G H m n ◃⊙∘
    ⊙×-fmap (⊙–> (spectrum G m)) (⊙–> (spectrum H n)) ◃⊙idf

  ⊙Ω×-cp : ∀ (m n : ℕ) → ⊙Ω (⊙EM G (S m)) ⊙× ⊙Ω (⊙EM H (S n)) ⊙→ ⊙Ω (⊙EM G⊗H.abgroup (S (m + n)))
  ⊙Ω×-cp m n = ⊙compose (⊙Ω×-cp-seq m n)

  _∪_  : ∀ {m n : ℕ} → CEl G (pos m) X → CEl H (pos n) X → CEl G⊗H.abgroup (pos (m + n)) X
  _∪_ {m} {n} = Trunc-fmap2 {n = 0} (λ s' t' → ⊙Ω×-cp m n ⊙∘ smin-map s' t')

module _ (G : AbGroup i) (H : AbGroup i) where

  private
    module G⊗H = TensorProduct G H
    module H⊗G = TensorProduct H G
  open EMExplicit

  abstract
    ⊙Ω×-cp-comm : ∀ (m n : ℕ)
      → ⊙transport (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ◃⊙∘
        ⊙Ω-fmap (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + n))) ◃⊙∘
        ⊙Ω×-cp G H m n ◃⊙idf
        =⊙∘
        ⊙Ω-fmap (⊙cond-neg H⊗G.abgroup (S (n + m)) (and (odd m) (odd n))) ◃⊙∘
        ⊙Ω×-cp H G n m ◃⊙∘
        ⊙×-swap ◃⊙idf
    ⊙Ω×-cp-comm m n =
      ⊙transport (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ◃⊙∘
      ⊙Ω-fmap (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + n))) ◃⊙∘
      ⊙Ω×-cp G H m n ◃⊙idf
        =⊙∘⟨ 2 & 1 & ⊙expand (⊙Ω×-cp-seq G H m n) ⟩
      ⊙transport (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ◃⊙∘
      ⊙Ω-fmap (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + n))) ◃⊙∘
      ⊙<– (spectrum G⊗H.abgroup (m + n)) ◃⊙∘
      ⊙×-cp G H m n ◃⊙∘
      ⊙×-fmap (⊙–> (spectrum G m)) (⊙–> (spectrum H n)) ◃⊙idf
        =⊙∘⟨ 1 & 2 & !⊙∘ $ ⊙<–-spectrum-natural G⊗H.abgroup H⊗G.abgroup G⊗H.swap (m + n) ⟩
      ⊙transport (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ◃⊙∘
      ⊙<– (spectrum H⊗G.abgroup (m + n)) ◃⊙∘
      ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (m + n) ◃⊙∘
      ⊙×-cp G H m n ◃⊙∘
      ⊙×-fmap (⊙–> (spectrum G m)) (⊙–> (spectrum H n)) ◃⊙idf
        =⊙∘⟨ 0 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘
               (+-comm m n)
               (λ k → ⊙<– (spectrum H⊗G.abgroup k)) ⟩
      ⊙<– (spectrum H⊗G.abgroup (n + m)) ◃⊙∘
      ⊙transport (λ k → ⊙EM H⊗G.abgroup k) (+-comm m n) ◃⊙∘
      ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (m + n) ◃⊙∘
      ⊙×-cp G H m n ◃⊙∘
      ⊙×-fmap (⊙–> (spectrum G m)) (⊙–> (spectrum H n)) ◃⊙idf
        =⊙∘⟨ 1 & 3 & ⊙×-cp-comm G H m n ⟩
      ⊙<– (spectrum H⊗G.abgroup (n + m)) ◃⊙∘
      ⊙cond-neg H⊗G.abgroup (n + m) (and (odd m) (odd n)) ◃⊙∘
      ⊙×-cp H G n m ◃⊙∘
      ⊙×-swap ◃⊙∘
      ⊙×-fmap (⊙–> (spectrum G m)) (⊙–> (spectrum H n)) ◃⊙idf
        =⊙∘⟨ 0 & 2 & ⊙transport-natural-=⊙∘
               (Bool-elim (inv-path H⊗G.abgroup) idp (and (odd m) (odd n)))
               (λ A → ⊙<– (spectrum A (n + m))) ⟩
      ⊙transport (λ A → ⊙Ω (⊙EM A (S (n + m)))) neg ◃⊙∘
      ⊙<– (spectrum H⊗G.abgroup (n + m)) ◃⊙∘
      ⊙×-cp H G n m ◃⊙∘
      ⊙×-swap ◃⊙∘
      ⊙×-fmap (⊙–> (spectrum G m)) (⊙–> (spectrum H n)) ◃⊙idf
        =⊙∘₁⟨ 0 & 1 &
              ⊙transport-⊙coe (λ A → ⊙Ω (⊙EM A (S (n + m)))) neg ∙
              ap ⊙coe (ap-∘ ⊙Ω (λ A → ⊙EM A (S (n + m))) neg) ∙
              ! (⊙transport-⊙coe ⊙Ω (ap (λ A → ⊙EM A (S (n + m))) neg)) ∙
              ⊙transport-⊙Ω (ap (λ A → ⊙EM A (S (n + m))) neg) ∙
              ap ⊙Ω-fmap (! (⊙transport-⊙coe (λ A → ⊙EM A (S (n + m))) neg)) ⟩
      ⊙Ω-fmap (⊙cond-neg H⊗G.abgroup (S (n + m)) (and (odd m) (odd n))) ◃⊙∘
      ⊙<– (spectrum H⊗G.abgroup (n + m)) ◃⊙∘
      ⊙×-cp H G n m ◃⊙∘
      ⊙×-swap ◃⊙∘
      ⊙×-fmap (⊙–> (spectrum G m)) (⊙–> (spectrum H n)) ◃⊙idf
        =⊙∘⟨ 3 & 2 & =⊙∘-in {gs = ⊙×-fmap (⊙–> (spectrum H n)) (⊙–> (spectrum G m)) ◃⊙∘
                                  ⊙×-swap ◃⊙idf} $
                     ! $ ⊙λ= $ ⊙×-swap-natural (⊙–> (spectrum G m)) (⊙–> (spectrum H n)) ⟩
      ⊙Ω-fmap (⊙cond-neg H⊗G.abgroup (S (n + m)) (and (odd m) (odd n))) ◃⊙∘
      ⊙<– (spectrum H⊗G.abgroup (n + m)) ◃⊙∘
      ⊙×-cp H G n m ◃⊙∘
      ⊙×-fmap (⊙–> (spectrum H n)) (⊙–> (spectrum G m)) ◃⊙∘
      ⊙×-swap ◃⊙idf
        =⊙∘⟨ 1 & 3 & ⊙contract ⟩
      ⊙Ω-fmap (⊙cond-neg H⊗G.abgroup (S (n + m)) (and (odd m) (odd n))) ◃⊙∘
      ⊙Ω×-cp H G n m ◃⊙∘
      ⊙×-swap ◃⊙idf ∎⊙∘
      where
      neg : H⊗G.abgroup == H⊗G.abgroup
      neg = Bool-elim (inv-path H⊗G.abgroup) idp (and (odd m) (odd n))

  ∪-swap : ∀ (m n : ℕ)
    → CEl G⊗H.abgroup (pos (m + n)) X → CEl H⊗G.abgroup (pos (n + m)) X
  ∪-swap m n =
    transport (λ k → CEl H⊗G.abgroup (pos k) X) (+-comm m n) ∘
    EM-CEl-coeff-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (pos (m + n)) X

  maybe-inv : ∀ (n : ℤ) → Bool → CEl H⊗G.abgroup n X → CEl H⊗G.abgroup n X
  maybe-inv n = Bool-rec (Group.inv (C H⊗G.abgroup n X)) (idf _)

  private
    _G∪H_ = _∪_ G H
    _H∪G_ = _∪_ H G

  ∪-comm : ∀ {m n : ℕ}
    (s : CEl G (pos m) X)
    (t : CEl H (pos n) X)
    → ∪-swap m n (s G∪H t) ==
      maybe-inv (pos (n + m)) (and (odd m) (odd n)) (t H∪G s)
  ∪-comm {m} {n} =
    Trunc-elim {{λ s → Π-level (λ t → =-preserves-level Trunc-level)}} $ λ s' →
    Trunc-elim {{λ t → =-preserves-level Trunc-level}} $ λ t' →
    transport (λ k → CEl H⊗G.abgroup (pos k) X) (+-comm m n)
    [ ⊙Ω-fmap (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + n))) ⊙∘
      ⊙Ω×-cp G H m n ⊙∘
      smin-map s' t' ]
      =⟨ app= step₁
         [ ⊙Ω-fmap (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + n))) ⊙∘
           ⊙Ω×-cp G H m n ⊙∘
           smin-map s' t' ] ⟩
    [ ⊙transport (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ⊙∘
      ⊙Ω-fmap (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + n))) ⊙∘
      ⊙Ω×-cp G H m n ⊙∘
      smin-map s' t' ]
      =⟨ ap [_] (=⊙∘-out (step₂ s' t')) ⟩
    Trunc-fmap (⊙Ω-fmap (⊙cond-neg H⊗G.abgroup (S (n + m)) (and (odd m) (odd n))) ⊙∘_)
    [ ⊙Ω×-cp H G n m ⊙∘ smin-map t' s' ]
      =⟨ app= (step₃ (n + m) (and (odd m) (odd n))) [ ⊙Ω×-cp H G n m ⊙∘ smin-map t' s' ] ⟩
    maybe-inv (pos (n + m)) (and (odd m) (odd n))
    [ ⊙Ω×-cp H G n m ⊙∘ smin-map t' s' ] =∎
    where
    step₁ : transport (λ k → CEl H⊗G.abgroup (pos k) X) (+-comm m n) ==
            Trunc-fmap (⊙transport (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ⊙∘_)
    step₁ =
      transport (λ k → CEl H⊗G.abgroup (pos k) X) (+-comm m n)
        =⟨ ap coe (ap-∘ (Trunc 0) (λ k → X ⊙→ ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n)) ⟩
      transport (Trunc 0) (ap (λ k → X ⊙→ ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n))
        =⟨ transport-Trunc (ap (λ k → X ⊙→ ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n)) ⟩
      Trunc-fmap (transport (λ k → X ⊙→ ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n))
        =⟨ ap (Trunc-fmap ∘ coe) (ap-∘ (X ⊙→_) (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n)) ⟩
      Trunc-fmap (transport (X ⊙→_) (ap (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n)))
        =⟨ ap Trunc-fmap $ λ= $ transport-post⊙∘ X (ap (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n)) ⟩
      Trunc-fmap (⊙coe (ap (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n)) ⊙∘_)
        =⟨ ap (λ g → Trunc-fmap (g ⊙∘_)) $
           ! $ ⊙transport-⊙coe (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ⟩
      Trunc-fmap (⊙transport (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ⊙∘_) =∎
    step₂ : ∀ (s' : X ⊙→ ⊙Ω (⊙EM G (S m))) (t' : X ⊙→ ⊙Ω (⊙EM H (S n)))
      → ⊙transport (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ◃⊙∘
        ⊙Ω-fmap (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + n))) ◃⊙∘
        ⊙Ω×-cp G H m n ◃⊙∘
        smin-map s' t' ◃⊙idf
        =⊙∘
        ⊙Ω-fmap (⊙cond-neg H⊗G.abgroup (S (n + m)) (and (odd m) (odd n))) ◃⊙∘
        ⊙Ω×-cp H G n m ◃⊙∘
        smin-map t' s' ◃⊙idf
    step₂ s' t' =
      ⊙transport (λ k → ⊙Ω (⊙EM H⊗G.abgroup (S k))) (+-comm m n) ◃⊙∘
      ⊙Ω-fmap (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + n))) ◃⊙∘
      ⊙Ω×-cp G H m n ◃⊙∘
      smin-map s' t' ◃⊙idf
        =⊙∘⟨ 0 & 3 & ⊙Ω×-cp-comm m n ⟩
      ⊙Ω-fmap (⊙cond-neg H⊗G.abgroup (S (n + m)) (and (odd m) (odd n))) ◃⊙∘
      ⊙Ω×-cp H G n m ◃⊙∘
      ⊙×-swap ◃⊙∘
      smin-map s' t' ◃⊙idf
        =⊙∘⟨ 2 & 2 & =⊙∘-in {gs = smin-map t' s' ◃⊙idf} $
             smin-map-⊙×-swap (⊙Ω (⊙EM H (S n))) (⊙Ω (⊙EM G (S m))) t' s' ⟩
      ⊙Ω-fmap (⊙cond-neg H⊗G.abgroup (S (n + m)) (and (odd m) (odd n))) ◃⊙∘
      ⊙Ω×-cp H G n m ◃⊙∘
      smin-map t' s' ◃⊙idf ∎⊙∘
    step₃ : ∀ (k : ℕ) (b : Bool) →
      Trunc-fmap (⊙Ω-fmap (⊙cond-neg H⊗G.abgroup (S k) b) ⊙∘_) ==
      maybe-inv (pos k) b
    step₃ k false =
      Trunc-fmap (⊙Ω-fmap (⊙idf (⊙EM H⊗G.abgroup (S k))) ⊙∘_)
        =⟨ ap (λ g → Trunc-fmap (g ⊙∘_)) ⊙Ω-fmap-idf ⟩
      Trunc-fmap (⊙idf (⊙Ω (⊙EM H⊗G.abgroup (S k))) ⊙∘_)
        =⟨ ap Trunc-fmap (λ= (⊙λ= ∘ ⊙∘-unit-l)) ⟩
      Trunc-fmap (idf (X ⊙→ ⊙Ω (⊙EM H⊗G.abgroup (S k))))
        =⟨ λ= Trunc-fmap-idf ⟩
      idf (Trunc 0 (X ⊙→ ⊙Ω (⊙EM H⊗G.abgroup (S k)))) =∎
    step₃ k true =
      Trunc-fmap (⊙Ω-fmap (⊙transport (λ A → ⊙EM A (S k)) (inv-path H⊗G.abgroup)) ⊙∘_)
        =⟨ ap (λ f → Trunc-fmap (⊙Ω-fmap f ⊙∘_)) $
           ⊙transport-⊙EM-uaᴬᴳ H⊗G.abgroup H⊗G.abgroup (inv-iso H⊗G.abgroup) (S k) ⟩
      Trunc-fmap (⊙Ω-fmap (⊙EM-fmap H⊗G.abgroup H⊗G.abgroup (inv-hom H⊗G.abgroup) (S k)) ⊙∘_)
        =⟨ ap GroupHom.f (EM-C-coeff-fmap-inv-hom H⊗G.abgroup (pos k) X) ⟩
      Group.inv (C H⊗G.abgroup (pos k) X) =∎

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import Agda.Builtin.Unit

data D : Set where
  c₁ c₂ : D
  @0 c₃ : D

f : @0 D → ⊤
f c₁ = tt
f c₂ = tt
f c₃ = tt


text:
------------------------------------------------------------------------
-- This file contains the definition of a preorder as a category with --
-- additional properties.                                             --
------------------------------------------------------------------------
module Category.Poset where

open import Level renaming (suc to lsuc)
open import Data.List
open import Data.Product hiding (map)
open import Data.Sum hiding (map)
open import Data.Empty
open import Data.Unit

open import Setoid.Total
open import Category.Category
open import Category.Preorder
open import Equality.Eq

record Poset {l : Level} : Set (lsuc l) where
  field
    -- The underlying category.
    𝕊 : PO {l}

    -- The poset axiom.
    PSax : ∀{A B}{f : el (Hom (po-cat 𝕊) A B)}{g : el (Hom (po-cat 𝕊) B A)} → A ≅ B

open Poset public renaming (𝕊 to poset-cat)

_≇_ : {l : Level}{A B : Set l} → (a : A) → (b : B) → Set l
a ≇ b = (a ≅ b → ⊥)

postulate eq-dec : ∀{l}{A B : Set l} → (a : A) → (b : B) → a ≅ b ⊎ a ≇ b

PosetCat : {l : Level} → (J : Poset {l}) → Cat {l}
PosetCat J = (po-cat (poset-cat J))

PosetObj : {l : Level} → (J : Poset {l}) → Set l
PosetObj J = Obj (PosetCat J)


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids

module Setoids.Functions.Definition {a b c d : _} {A : Set a} {B : Set b} where

WellDefined : (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) → Set (a ⊔ c ⊔ d)
WellDefined S T f = {x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y)