text:
{-

Definition of finite sets

A set is finite if it is merely equivalent to `Fin n` for some `n`. We
can translate this to code in two ways: a truncated sigma of a nat and
an equivalence, or a sigma of a nat and a truncated equivalence. We
prove that both formulations are equivalent.

-}

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

module Cubical.Data.FinSet where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Data.Unit
open import Cubical.Data.Nat
open import Cubical.Data.Fin
open import Cubical.Data.Sigma

private
  variable
    ℓ : Level
    A : Type ℓ

isFinSet : Type ℓ → Type ℓ
isFinSet A = ∃[ n ∈ ℕ ] A ≃ Fin n

isProp-isFinSet : isProp (isFinSet A)
isProp-isFinSet = propTruncIsProp

FinSet : Type (ℓ-suc ℓ)
FinSet = TypeWithStr _ isFinSet

isFinSetFin : ∀ {n} → isFinSet (Fin n)
isFinSetFin = ∣ _ , pathToEquiv refl ∣

isFinSetUnit : isFinSet Unit
isFinSetUnit = ∣ 1 , Unit≃Fin1 ∣

isFinSetΣ : Type ℓ → Type ℓ
isFinSetΣ A = Σ[ n ∈ ℕ ] ∥ A ≃ Fin n ∥

FinSetΣ : Type (ℓ-suc ℓ)
FinSetΣ = TypeWithStr _ isFinSetΣ

isProp-isFinSetΣ : isProp (isFinSetΣ A)
isProp-isFinSetΣ {A = A} (n , equivn) (m , equivm) =
  Σ≡Prop (λ _ → propTruncIsProp) n≡m
  where
    Fin-n≃Fin-m : ∥ Fin n ≃ Fin m ∥
    Fin-n≃Fin-m = rec
      propTruncIsProp
      (rec
        (isPropΠ λ _ → propTruncIsProp)
        (λ hm hn → ∣ Fin n ≃⟨ invEquiv hn ⟩ A ≃⟨ hm ⟩ Fin m ■ ∣)
        equivm
      )
      equivn

    Fin-n≡Fin-m : ∥ Fin n ≡ Fin m ∥
    Fin-n≡Fin-m = rec propTruncIsProp (∣_∣ ∘ ua) Fin-n≃Fin-m

    ∥n≡m∥ : ∥ n ≡ m ∥
    ∥n≡m∥ = rec propTruncIsProp (∣_∣ ∘ Fin-inj n m) Fin-n≡Fin-m

    n≡m : n ≡ m
    n≡m = rec (isSetℕ n m) (λ p → p) ∥n≡m∥

isFinSet≡isFinSetΣ : isFinSet A ≡ isFinSetΣ A
isFinSet≡isFinSetΣ {A = A} = hPropExt isProp-isFinSet isProp-isFinSetΣ to from
  where
    to : isFinSet A → isFinSetΣ A
    to ∣ n , equiv ∣ = n , ∣ equiv ∣
    to (squash p q i) = isProp-isFinSetΣ (to p) (to q) i

    from : isFinSetΣ A → isFinSet A
    from (n , ∣ isFinSet-A ∣) = ∣ n , isFinSet-A ∣
    from (n , squash p q i) = isProp-isFinSet (from (n , p)) (from (n , q)) i

FinSet≡FinSetΣ : FinSet {ℓ} ≡ FinSetΣ
FinSet≡FinSetΣ = ua (isoToEquiv (iso to from to-from from-to))
  where
    to : FinSet → FinSetΣ
    to (A , isFinSetA) = A , transport isFinSet≡isFinSetΣ isFinSetA

    from : FinSetΣ → FinSet
    from (A , isFinSetΣA) = A , transport (sym isFinSet≡isFinSetΣ) isFinSetΣA

    to-from : ∀ A → to (from A) ≡ A
    to-from A = Σ≡Prop (λ _ → isProp-isFinSetΣ) refl

    from-to : ∀ A → from (to A) ≡ A
    from-to A = Σ≡Prop (λ _ → isProp-isFinSet) refl

card : FinSet {ℓ} → ℕ
card = fst ∘ snd ∘ transport FinSet≡FinSetΣ

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Data.Collection.Core where

open import Data.List public using (List; []; _∷_)
open import Data.String public using (String; _≟_)
open import Level using (zero)

open import Function using (flip)
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Nullary.Decidable renaming (map to mapDec; map′ to mapDec′)
open import Relation.Unary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

--------------------------------------------------------------------------------
--  Types
--------------------------------------------------------------------------------

Element : Set
Element = String

Collection : Set
Collection = List Element

Membership : Set _
Membership = Pred Element zero

--------------------------------------------------------------------------------
--  Membership
--------------------------------------------------------------------------------

infix 4 _∈c_ _∉c_

data _∈c_ : REL Element Collection zero where
    here  : ∀ {   x A}         → x ∈c x ∷ A
    there : ∀ {a x A} → x ∈c A → x ∈c a ∷ A

_∉c_ : REL Element Collection _
x ∉c A = ¬ x ∈c A

infixr 6 _⊈_

-- I know this notation is a bit confusing
_⊈_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ⊈ Q = ∀ {x} → x ∉ P → x ∉ Q

c[_] : REL Collection Element zero
c[_] = flip _∈c_

infix 4 _∈?_

_∈?_ : (x : Element) → (A : Collection) → Dec (x ∈ c[ A ])
x ∈? []       = no (λ ())
x ∈? ( a ∷ A) with x ≟ a
x ∈? (.x ∷ A) | yes refl = yes here
x ∈? ( a ∷ A) | no ¬p    = mapDec′ there (there-if-not-here ¬p) (x ∈? A)
    where
            there-if-not-here : ∀ {x a A} → x ≢ a → x ∈ c[ a ∷ A ] → x ∈ c[ A ]
            there-if-not-here x≢a here          = contradiction refl x≢a
            there-if-not-here x≢a (there x∈a∷A) = x∈a∷A

--------------------------------------------------------------------------------
--  Miscs
--------------------------------------------------------------------------------
--
-- ∷-⊆-monotone : ∀ {a A B} → c[ A ] ⊆ c[ B ] → c[ a ∷ A ] ⊆ c[ a ∷ B ]
-- ∷-⊆-monotone f here       = here
-- ∷-⊆-monotone f (there ∈A) = there (f ∈A)

ext: agda

max_stars_repo_name: banacorn/lambda-calculus

max_issues_repo_name: banacorn/lambda-calculus

max_forks_repo_name: banacorn/lambda-calculus


text:
------------------------------------------------------------------------
-- Parser monad
------------------------------------------------------------------------

open import Relation.Binary
open import Relation.Binary.OrderMorphism
open import Relation.Binary.PropositionalEquality hiding (poset)
import Relation.Binary.Properties.StrictTotalOrder as STOProps
open import Data.Product
open import Level

module MonadPostulates where

postulate
  -- Input string positions.

  Position : Set
  _<P_ : Rel Position zero
  posOrdered : IsStrictTotalOrder _≡_ _<P_

  -- Input strings.

  Input : Position -> Set

  -- In order to be able to store results in a memo table (and avoid
  -- having to lift the table code to Set1) the result types have to
  -- come from the following universe:

  Result : Set
  ⟦_⟧ : Result -> Set

  -- Memoisation keys. These keys must uniquely identify the
  -- computation that they are associated with, when paired up with
  -- the current input string position.

  Key : let PosPoset = STOProps.poset
                          (record { Carrier = _ ; _≈_ = _; _<_ = _
                                  ; isStrictTotalOrder = posOrdered })
            MonoFun = PosPoset ⇒-Poset PosPoset in
         MonoFun -> Result -> Set
  _≈'_ _<_ : Rel (∃₂ Key) zero
  keyOrdered : IsStrictTotalOrder _≈'_ _<_

  -- Furthermore the underlying equality needs to be strong enough.

  funsEqual    : _≈'_ =[ proj₁ ]⇒ _≡_
  resultsEqual : _≈'_ =[ (\rfk -> proj₁ (proj₂ rfk)) ]⇒ _≡_

--  where

open _⇒-Poset_
open STOProps (record { Carrier = _ ; _≈_ = _; _<_ = _
                      ; isStrictTotalOrder = posOrdered })

import IndexedMap as Map -- renaming (Map to MemoTable)
open import Effect.Monad
open import Effect.Monad.State
import Data.List as List; open List using (List)
open import Data.Unit
open import Function
open import Data.Maybe
open import Data.Product.Relation.Binary.Lex.Strict
open import Data.Product.Relation.Binary.Pointwise.NonDependent
import Relation.Binary.Construct.On as On

------------------------------------------------------------------------
-- Monotone functions

MonoFun : Set
MonoFun = poset ⇒-Poset poset

------------------------------------------------------------------------
-- Memo tables

-- Indices and keys used by the memo table.

Index : Set
Index = Position × MonoFun × Result

data MemoTableKey : Index -> Set where
  key : forall {f r} (key : Key f r) pos -> MemoTableKey (pos , f , r)

-- Input strings of a certain maximum length.

Input≤ : Position -> Set
Input≤ pos = ∃ \pos′ -> pos′ ≤ pos × Input pos′

-- Memo table values.

Value : Index -> Set
Value (pos , f , r) = List (⟦ r ⟧ × Input≤ (fun f pos))

-- Shuffles the elements to simplify defining equality and order
-- relations for the keys.

shuffle : ∃ MemoTableKey -> Position × ∃₂ Key
shuffle ((pos , f , r) , key k .pos) = (pos , f , r , k)

-- Equality and order.

Eq : Rel (∃ MemoTableKey) _
Eq = Pointwise _≡_ _≈'_  on  shuffle

Lt : Rel (∃ MemoTableKey) _
Lt = ×-Lex _≡_ _<P_ _<_  on  shuffle

isOrdered : IsStrictTotalOrder Eq Lt
isOrdered = On.isStrictTotalOrder shuffle
              (×-isStrictTotalOrder posOrdered keyOrdered)

indicesEqual′ : Eq =[ proj₁ ]⇒ _≡_
indicesEqual′ {((_ , _ , _) , key _ ._)}
              {((_ , _ , _) , key _ ._)} (eq₁ , eq₂) =
  cong₂ _,_ eq₁ (cong₂ _,_ (funsEqual eq₂) (resultsEqual eq₂))

open Map isOrdered (\{k₁} {k₂} -> indicesEqual′ {k₁} {k₂}) Value

{-
------------------------------------------------------------------------
-- Parser monad

-- The parser monad is built upon a list monad, for backtracking, and
-- two state monads. One of the state monads stores a memo table, and
-- is unaffected by backtracking. The other state monad, which /is/
-- affected by backtracking, stores the remaining input string.

-- The memo table state monad.

module MemoState = RawMonadState (StateMonadState MemoTable)

-- The list monad.

module List = RawMonadPlus List.ListMonadPlus

-- The inner monad (memo table plus list).

module IM where

  Inner : Set -> Set
  Inner R = State MemoTable (List R)

  InnerMonadPlus : RawMonadPlus Inner
  InnerMonadPlus = record
    { monadZero = record
      { monad = record
        { return = \x -> return (List.return x)
        ; _>>=_  = \m f -> List.concat <$> (List.mapM monad f =<< m)
        }
      ; ∅ = return List.∅
      }
    ; _∣_ = \m₁ m₂ -> List._∣_ <$> m₁ ⊛ m₂
    }
    where
    open MemoState

  InnerMonadState : RawMonadState MemoTable Inner
  InnerMonadState = record
    { monad = RawMonadPlus.monad InnerMonadPlus
    ; get   = List.return <$> get
    ; put   = \s -> List.return <$> put s
    }
    where open MemoState

  open RawMonadPlus  InnerMonadPlus  public
  open RawMonadState InnerMonadState public
    using (get; put; modify)

-- The complete parser monad.

module PM where

  P : MonoFun -> Set -> Set
  P f A = forall {n} -> Input n -> IM.Inner (A × Input≤ (fun f n))

  -- Memoises the computation, assuming that the key is sufficiently
  -- unique.

  memoise : forall {f r} -> Key f r -> P f ⟦ r ⟧ -> P f ⟦ r ⟧
  memoise k p {pos} xs =
    let open IM in helper =<< lookup k′ <$> get
    where
    i = (pos , _)

    k′ : MemoTableKey i
    k′ = key k pos

    helper : Maybe (Value i) -> State MemoTable (Value i)
    helper (just ris) = return ris  where open MemoState
    helper nothing    = p xs                   >>= \ris ->
                        modify (insert k′ ris) >>
                        return ris
      where open MemoState

  -- Other monadic operations.

  return : forall {A} -> A -> P idM A
  return a = \xs -> IM.return (a , _ , refl , xs)

  _>>=_ : forall {A B f g} -> P f A -> (A -> P g B) -> P (g ∘M f) B
  _>>=_ {g = g} m₁ m₂ xs =
    m₁ xs ⟨ IM._>>=_ ⟩ \ays ->
    let a  = proj₁ ays
        le = proj₁ $ proj₂ $ proj₂ ays
        ys = proj₂ $ proj₂ $ proj₂ ays in
    fix le ⟨ IM._<$>_ ⟩ m₂ a ys
    where
    lemma : forall {i j k} -> j ≤ k -> i ≤ fun g j -> i ≤ fun g k
    lemma j≤k i≤gj = trans i≤gj (monotone g j≤k)

    fix : forall {A i j} -> i ≤ j ->
          A × Input≤ (fun g i) ->
          A × Input≤ (fun g j)
    fix le = map-× id (map-Σ id (map-× (lemma le) id))

  ∅ : forall {A} -> P idM A
  ∅ = const IM.∅

  _∣_ : forall {A f} -> P f A -> P f A -> P f A
  m₁ ∣ m₂ = \xs -> IM._∣_ (m₁ xs) (m₂ xs)

  put : forall {n} -> Input n -> P (constM n) ⊤
  put xs = \_ -> IM.return (_ , _ , refl , xs)

  modify : forall {A f} ->
           (forall {n} -> Input n -> A × Input (fun f n)) ->
           P f A
  modify g xs = IM.return (proj₁ gxs , _ , refl , proj₂ gxs)
    where gxs = g xs
-}


text:
module Prelude where

infixr 50 _,_
infixl 40 _◄_
infix  30 _∈_

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

data List (A : Set) : Set where
  ε   : List A
  _◄_ : List A -> A -> List A

data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs}   ->           x ∈ xs ◄ x
  tl : forall {y xs} -> x ∈ xs -> x ∈ xs ◄ y

data Box {A : Set}(P : A -> Set) : List A -> Set where
  ⟨⟩  : Box P ε
  _◃_ : forall {xs x} -> Box P xs -> P x -> Box P (xs ◄ x)

_!_ : {A : Set}{P : A -> Set}{xs : List A}{x : A} ->
      Box P xs -> x ∈ xs -> P x
⟨⟩      ! ()
(_ ◃ v) ! hd   = v
(ρ ◃ _) ! tl x = ρ ! x

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- This module introduces the basic structure of an Agda program.

{- Every Agda file contains a single top-level module. To make it possible to
   find the file corresponding to a particular module, the name of the file
   should correspond to the name of the module. In this case the module
   'Introduction.Basics' is defined in the file 'Introduction/Basics.agda'.
-}
module Basics where

{- The top-level module contains a sequence of declarations, such as datatype
   declarations and function definitions. The most common forms of declarations
   are introduced below.

   A module can also contain sub-modules, see 'Introduction.Modules.SubModules'
   for more information.
-}

-- Agda can be used as a pure logical framework. The 'postulate' declaration
-- introduces new constants :
postulate
  N : Set     -- Set is the first universe
  z : N
  s : N -> N  -- The independent function space is written A -> B

-- Using 'postulate' it is not possible to introduce new computation rules. A
-- better way is to introduce a datatype and define functions by pattern
-- matching on elements of the datatype.

-- A datatype is introduced with the 'data' keyword. All constructors of the
-- datatype are given with their types after the 'where'. Datatypes can be
-- parameterised (see 'Introduction.Data.Parameterised').

data Bool : Set where
  false : Bool
  true  : Bool

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

-- Functions over datatypes can be defined by pattern matching.

plus : Nat -> Nat -> Nat
plus  zero   m = m
plus (suc n) m = suc (plus n m)

-- With this definition plus (suc zero) (suc zero) will reduce to suc (suc
-- zero).

-- When defining mutually recursive functions you have to declare functions
-- before they can be called.

odd : Nat -> Bool

even : Nat -> Bool
even (suc n) = odd n
even zero    = true

odd zero    = false
odd (suc n) = even n

-- Agda is a monomorphic, but dependently typed, language. This means that
-- polymorphism is simulated by having functions take type arguments. For
-- instance, the polymorphic identity function can be represented as follows :

id : (A : Set) -> A -> A        -- the dependent function space is written (x : A) -> B
id A x = x

one : Nat
one = id Nat (suc zero) -- a silly use of the identity function

-- To faithfully simulate a polymorphic function we would like to omit the type
-- argument when using the function. See 'Introduction.Implicit' for
-- information on how to do this.

-- Agda is both a programming language and a formal proof language, so we
-- expect to be able to prove theorems about our programs. As an example we
-- prove the very simple theorem n + 0 == n.

-- First we introduce datatypes for truth (a singleton type) and falsity (an
-- empty type).

data True : Set where   -- Here it would make sense to declare True to be a
  tt : True             -- Prop (the universe of propositions) rather than a
                        -- Set. See 'Introduction.Universes' for more
                        -- information.

data False : Set where  -- see 'Introduction.Data.Empty' for more information
                        -- on empty types.

-- Second, we define what it means for two natural numbers to be equal. Infix
-- operators are declared by enclosing the operator in _. See
-- 'Introduction.Operators' for more information.

_==_ : Nat -> Nat -> Set
zero  == zero  = True
zero  == suc m = False
suc n == zero  = False
suc n == suc m = n == m

-- Now we are ready to state and prove our theorem. The proof is by induction
-- (i.e. recursion) on 'n'.

thmPlusZero : (n : Nat) -> plus n zero == n   -- A function from a number n to
                                            -- P n can be seen as the
                                            -- proposition ∀ n. P n.
thmPlusZero  zero   = tt
thmPlusZero (suc n) = thmPlusZero n

thmPlusZero' : (n : Nat) -> plus zero n == n
thmPlusZero'  zero   = tt
thmPlusZero' (suc n) = thmPlusZero' n

{- In both branches the reduction makes the proof very simple. In the first
   case the goal is

    plus zero zero == zero    which reduces to
    zero == zero              and
    True

  In the second case we have

    plus (suc n) zero == suc n
    suc (plus n zero) == suc n
    plus n zero == n

  so the induction hypothesis (the recursive call) is directly applicable.
-}

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
module nat-division where

open import bool
open import bool-thms
open import eq
open import neq
open import nat
open import nat-thms
open import product
open import product-thms
open import sum

{- a div-result for dividend x and divisor d consists of the quotient q, remainder r, and a proof that q * d + r = x -}
div-result : ℕ → ℕ → Set
div-result x d = Σ ℕ (λ q → Σ ℕ (λ r → q * d + r ≡ x ∧ r < d ≡ tt))

-- we use an upper bound n on the dividend x.  For an alternative approach, see nat-division-wf.agda.
divh : (n : ℕ) → (x : ℕ) → (y : ℕ) → x ≤ n ≡ tt → y =ℕ 0 ≡ ff → div-result x y
divh 0 0 0 p1 ()
divh 0 0 (suc y) p1 p2 = 0 , 0 , refl , refl
divh 0 (suc x) y () p2
divh (suc n) x y p1 p2 with keep (x < y)
divh (suc n) x y p1 p2 | tt , pl = 0 , x , refl , pl
divh (suc n) x y p1 p2 | ff , pl with divh n (x ∸ y) y (∸≤2 n x y p1 p2) p2
divh (suc n) x y p1 p2 | ff , pl | q , r , pa , pb = suc q , r , lem{q}{r} pa , pb
  where lem : ∀{q r} → q * y + r ≡ x ∸ y → y + q * y + r ≡ x
        lem{q}{r} p rewrite sym (+assoc y (q * y) r) | p | +comm y (x ∸ y) = ∸+2{x}{y} (<ff{x}{y} pl)

-- the div-result contains the quotient, remainder, and proof relating them to the inputs
_÷_!_ : (x : ℕ) → (y : ℕ) → y =ℕ 0 ≡ ff → div-result x y
x ÷ y ! p = divh x x y (≤-refl x) p

-- return a pair of the quotient and remainder
_÷_!!_ : ℕ → (y : ℕ) → y =ℕ 0 ≡ ff → ℕ × ℕ
x ÷ y !! p with x ÷ y ! p
... | q , r , p' = q , r

-- return the quotient only
_÷_div_ : ℕ → (y : ℕ) → y =ℕ 0 ≡ ff → ℕ
x ÷ y div p with x ÷ y ! p
... | q , r , p' = q

-- return the remainder only
_÷_mod_ : ℕ → (y : ℕ) → y =ℕ 0 ≡ ff → ℕ
x ÷ y mod p with x ÷ y ! p
... | q , r , p' = r

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- You can't use the same name more than once in the same scope.
module ClashingDefinition where

postulate
  X : Set
  X : Set

Y = X

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- An LTS from Section 6.2.5 of "Enhancements of the bisimulation
-- proof method" by Pous and Sangiorgi
------------------------------------------------------------------------

{-# OPTIONS --safe #-}

open import Prelude

module Labelled-transition-system.6-2-5 (Name : Type) where

open import Labelled-transition-system

infixr 12 _·_
infix   5 _[_]
infix   4 _[_]⟶_

-- Processes.

data Proc : Type where
  op  : Proc → Proc
  _·_ : Name → Proc → Proc
  ∅   : Proc

-- Transitions.

data _[_]⟶_ : Proc → Name → Proc → Type where
  action : ∀ {a P} → a · P [ a ]⟶ P
  op     : ∀ {a P P′ P″} → P [ a ]⟶ P′ → P′ [ a ]⟶ P″ → op P [ a ]⟶ P″

-- The LTS.

6-2-5 : LTS lzero
6-2-5 = record
  { Proc      = Proc
  ; Label     = Name
  ; _[_]⟶_    = _[_]⟶_
  ; is-silent = λ _ → false
  }

open LTS 6-2-5 public hiding (Proc; _[_]⟶_)

-- Polyadic contexts.

data Context (n : ℕ) : Type where
  hole : (x : Fin n) → Context n
  op   : Context n → Context n
  _·_  : (a : Name) → Context n → Context n
  ∅    : Context n

-- Hole filling.

_[_] : ∀ {n} → Context n → (Fin n → Proc) → Proc
hole x [ ps ] = ps x
op C   [ ps ] = op (C [ ps ])
a · C  [ ps ] = a · (C [ ps ])
∅      [ ps ] = ∅

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
-- Tests unreachable clause detection
module Unreachable where

data C : Set where
  c₁ : C
  c₂ : C -> C

data Bool : Set where
  t : Bool
  f : Bool

maj : Bool -> Bool -> Bool -> Bool
maj f f f = f
maj t f x = x
maj f x t = x
maj x t f = x
maj t t t = t

unreachable : C -> C
unreachable (c₂ x)      = c₁
unreachable (c₂ (c₂ y)) = c₂ c₁
unreachable c₁          = c₁
unreachable _ = c₁


text:
{-# OPTIONS --guardedness #-}

record _≈_ {A : Set} (xs : Stream A) (ys : Stream A) : Set where
  coinductive
  field
    hd-≈ : hd xs ≡ hd ys
    tl-≈ : tl xs ≈ tl ys

even : ∀ {A} → Stream A → Stream A
hd (even x) = hd x
tl (even x) = even (tl (tl x))

odd : ∀ {A} → Stream A → Stream A
odd x = even (tl x)

split : ∀ {A} → Stream A → Stream A × Stream A
split xs = even xs , odd xs

merge : ∀ {A} → Stream A × Stream A → Stream A
hd (merge (fst , snd)) = hd fst
tl (merge (fst , snd)) = merge (snd , tl fst)

merge-split-id : ∀ {A} (xs : Stream A) → merge (split xs) ≈ xs
hd-≈ (merge-split-id _)  = refl
tl-≈ (merge-split-id xs) = merge-split-id (tl xs)


text:
module exampleTypeAbbreviations where

postulate A : Set
A2 : Set
A2 = A -> A

A3 : Set
A3 = A2 -> A2

a2 : A2
a2 = \x -> x

a3 : A3
a3 = \x -> x


text:
------------------------------------------------------------------------
-- Theorems relating the coinductive definition of the delay
-- monad to the alternative one and to another type
------------------------------------------------------------------------

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

open import Prelude hiding (↑)

module Delay-monad.Alternative.Equivalence {a} {A : Type a} where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J
open import Surjection equality-with-J using (_↠_)

open import Delay-monad as D hiding (Delay)
open import Delay-monad.Alternative
open import Delay-monad.Alternative.Properties
open import Delay-monad.Bisimilarity as Bisimilarity
  using ([_]_∼_; now; later; force)

private
  variable
    i : Size

-- Building blocks used in the theorems below.

module Delay⇔Delay where

  -- The function to₁ is basically π from Section 7.1 of
  -- "Quotienting the Delay Monad by Weak Bisimilarity" by Chapman,
  -- Uustalu and Veltri, but the function proj₁ ∘ from is different
  -- from their function ε, which is defined so that (with the
  -- terminology used here) ε (now x) (suc n) = nothing.

  to₁ : (ℕ → Maybe A) → D.Delay A i
  to₁ f = to′ (f 0)
    module To where
    to′ : Maybe A → D.Delay A i
    to′ (just x) = now x
    to′ nothing  =
      later λ { .force → to₁ (f ∘ suc) }

  to : Delay A → D.Delay A i
  to = to₁ ∘ proj₁

  from : D.Delay A ∞ → Delay A
  from = λ x → from₁ x , from₂ x
    where
    from₁ : D.Delay A ∞ → ℕ → Maybe A
    from₁ (now x)   _       = just x
    from₁ (later x) zero    = nothing
    from₁ (later x) (suc n) = from₁ (force x) n

    from₂ : ∀ x → Increasing (from₁ x)
    from₂ (now x)   _       = inj₁ refl
    from₂ (later x) zero    = proj₁ LE-nothing-contractible
    from₂ (later x) (suc n) = from₂ (force x) n

-- The two definitions of the delay monad are logically equivalent.

Delay⇔Delay : Delay A ⇔ D.Delay A ∞
Delay⇔Delay = record { to = Delay⇔Delay.to; from = Delay⇔Delay.from }

-- There is a split surjection from D.Delay A ∞ to Delay A.

Delay↠Delay : D.Delay A ∞ ↠ Delay A
Delay↠Delay = record
  { logical-equivalence = inverse Delay⇔Delay
  ; right-inverse-of    = from∘to
  }
  where
  open Delay⇔Delay

  from∘to : ∀ x → from (to x) ≡ x
  from∘to x = Σ-≡,≡→≡
    (⟨ext⟩ (proj₁∘from∘to x))
    (⟨ext⟩ λ n →

       subst Increasing
             (⟨ext⟩ (proj₁∘from∘to x))
             (proj₂ (from (to x)))
             n                          ≡⟨ sym $ push-subst-application (⟨ext⟩ (proj₁∘from∘to x)) (flip Increasing-at) ⟩

       subst (Increasing-at n)
             (⟨ext⟩ (proj₁∘from∘to x))
             (proj₂ (from (to x)) n)    ≡⟨ uncurry proj₂∘from∘to x n _ refl ⟩∎

       proj₂ x n                        ∎)

    where

    proj₁∘from∘to′ :
      (g : ℕ → Maybe A) →
      Increasing g →
      ∀ x → g 0 ≡ x → ∀ n →
      proj₁ (from (To.to′ g x)) n ≡ g n
    proj₁∘from∘to′ g g-inc (just x) g0↓x n       = sym $ ↓-upwards-closed₀ g-inc g0↓x n
    proj₁∘from∘to′ g g-inc nothing  g0↑  zero    = sym g0↑
    proj₁∘from∘to′ g g-inc nothing  g0↑  (suc n) =
        proj₁∘from∘to′ (g ∘ suc) (g-inc ∘ suc) _ refl n

    proj₁∘from∘to :
      (x : Delay A) →
      ∀ n → proj₁ (from (to x)) n ≡ proj₁ x n
    proj₁∘from∘to (g , g-inc) = proj₁∘from∘to′ g g-inc (g 0) refl

    ↓-lemma :
      (g : ℕ → Maybe A) →
      (g-increasing : Increasing g) →
      ∀ n x (g0↓x : g 0 ↓ x) p → p ≡ g-increasing 0 →

      subst (Increasing-at n)
            (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ g-increasing g0↓x))
            (inj₁ refl)
        ≡
      g-increasing n

    ↓-lemma g _ _ x g0↓x (inj₂ (g0↑ , _)) _ =
      ⊥-elim $ ⊎.inj₁≢inj₂ (
        nothing  ≡⟨ sym g0↑ ⟩
        g 0      ≡⟨ g0↓x ⟩∎
        just x   ∎)

    ↓-lemma g g-inc zero x g0↓x (inj₁ g0≡g1) ≡g-inc0 =

      subst (Increasing-at zero)
            (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ g-inc g0↓x))
            (inj₁ refl)                                         ≡⟨ push-subst-inj₁
                                                                     {y≡z = ⟨ext⟩ (sym ∘ ↓-upwards-closed₀ g-inc g0↓x)}
                                                                     (λ f → f 0 ≡ f 1) (λ f → f 0 ↑ × ¬ f 1 ↑) ⟩
      inj₁ (subst (λ f → f 0 ≡ f 1)
                  (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ g-inc g0↓x))
                  refl)                                         ≡⟨ cong inj₁ lemma ⟩

      inj₁ g0≡g1                                                ≡⟨ ≡g-inc0 ⟩∎

      g-inc zero                                                ∎

      where
      eq    = ↓-upwards-closed₀ g-inc g0↓x
      lemma =

        subst (λ f → f 0 ≡ f 1) (⟨ext⟩ (sym ∘ eq)) refl      ≡⟨ subst-in-terms-of-trans-and-cong {x≡y = ⟨ext⟩ (sym ∘ eq)} ⟩

        trans (sym (cong (_$ 0) (⟨ext⟩ (sym ∘ eq))))
              (trans refl (cong (_$ 1) (⟨ext⟩ (sym ∘ eq))))  ≡⟨ cong (trans (sym (cong (_$ 0) (⟨ext⟩ (sym ∘ eq))))) $
                                                                  trans-reflˡ (cong (_$ 1) (⟨ext⟩ (sym ∘ eq))) ⟩
        trans (sym (cong (_$ 0) (⟨ext⟩ (sym ∘ eq))))
              (cong (_$ 1) (⟨ext⟩ (sym ∘ eq)))               ≡⟨ cong₂ (λ p q → trans (sym p) q) (cong-ext (sym ∘ eq)) (cong-ext (sym ∘ eq)) ⟩

        trans (sym $ sym $ eq 0) (sym $ eq 1)                ≡⟨ cong (λ eq′ → trans eq′ (sym $ eq 1)) $ sym-sym _ ⟩

        trans (eq 0) (sym $ eq 1)                            ≡⟨⟩

        trans g0↓x (sym $ ↓.step g-inc g0↓x (g-inc 0))       ≡⟨ cong (λ eq′ → trans g0↓x (sym $ ↓.step g-inc g0↓x eq′)) $ sym $ ≡g-inc0 ⟩

        trans g0↓x (sym $ ↓.step g-inc g0↓x (inj₁ g0≡g1))    ≡⟨⟩

        trans g0↓x (sym $ trans (sym g0≡g1) g0↓x)            ≡⟨ cong (trans g0↓x) $ sym-trans (sym g0≡g1) g0↓x ⟩

        trans g0↓x (trans (sym g0↓x) (sym (sym g0≡g1)))      ≡⟨ trans--[trans-sym] _ _ ⟩

        sym (sym g0≡g1)                                      ≡⟨ sym-sym _ ⟩∎

        g0≡g1                                                ∎

    ↓-lemma g g-inc (suc n) x g0↓x (inj₁ g0≡g1) ≡g-inc0 =

      subst (Increasing-at (suc n))
            (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ g-inc g0↓x))
            (inj₁ refl)                                                   ≡⟨⟩

      subst (Increasing-at n ∘ (_∘ suc))
            (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ g-inc g0↓x))
            (inj₁ refl)                                                   ≡⟨ subst-∘ (Increasing-at n) (_∘ suc)
                                                                                (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ g-inc g0↓x)) ⟩
      subst (Increasing-at n)
            (cong (_∘ suc) (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ g-inc g0↓x)))
            (inj₁ refl)                                                   ≡⟨ cong (λ eq → subst (Increasing-at n) eq _) $
                                                                               cong-pre-∘-ext (sym ∘ ↓-upwards-closed₀ g-inc g0↓x) ⟩
      subst (Increasing-at n)
            (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ g-inc g0↓x ∘ suc))
            (inj₁ refl)                                                   ≡⟨⟩

      subst (Increasing-at n)
            (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ (g-inc ∘ suc)
                            (↓.step g-inc g0↓x (g-inc 0))))
            (inj₁ refl)                                                   ≡⟨ cong (λ p → subst (Increasing-at n)
                                                                                (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ (g-inc ∘ suc)
                                                                                (↓.step g-inc g0↓x p)))
                                                                                (inj₁ refl))
                                                                                (sym ≡g-inc0) ⟩
      subst (Increasing-at n)
            (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ (g-inc ∘ suc)
                            (↓.step g-inc g0↓x (inj₁ g0≡g1))))
            (inj₁ refl)                                                   ≡⟨⟩

      subst (Increasing-at n)
            (⟨ext⟩ (sym ∘ ↓-upwards-closed₀ (g-inc ∘ suc)
                            (trans (sym g0≡g1) g0↓x)))
            (inj₁ refl)                                                   ≡⟨ ↓-lemma (g ∘ suc) (g-inc ∘ suc) n _ _ _ refl ⟩∎

      g-inc (suc n)                                                       ∎

    proj₂∘from∘to :
      (g : ℕ → Maybe A) →
      (g-increasing : Increasing g) →
      ∀ n y (g0≡y : g 0 ≡ y) →

      subst (Increasing-at n)
            (⟨ext⟩ (proj₁∘from∘to′ g g-increasing y g0≡y))
            (proj₂ (from (To.to′ g y)) n)
        ≡
      g-increasing n

    proj₂∘from∘to g g-inc n (just y) g0↓y =
      ↓-lemma g g-inc n y g0↓y _ refl

    proj₂∘from∘to g g-inc zero nothing g0↑ =
      (                                   $⟨ mono₁ 0 LE-nothing-contractible ⟩
       Is-proposition (LE nothing (g 1))  ↝⟨ subst (λ x → Is-proposition (LE x (g 1))) (sym g0↑) ⟩□
       Is-proposition (LE (g 0) (g 1))    □) _ _

    proj₂∘from∘to g g-inc (suc n) nothing g0↑ =

      subst (Increasing-at (suc n))
            (⟨ext⟩ (proj₁∘from∘to′ g g-inc nothing g0↑))
            (proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n)                 ≡⟨⟩

      subst (Increasing-at n ∘ (_∘ suc))
            (⟨ext⟩ (proj₁∘from∘to′ g g-inc nothing g0↑))
            (proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n)                 ≡⟨ subst-∘ (Increasing-at n) (_∘ suc)
                                                                                (⟨ext⟩ (proj₁∘from∘to′ g g-inc nothing g0↑)) ⟩
      subst (Increasing-at n)
            (cong (_∘ suc) (⟨ext⟩ (proj₁∘from∘to′ g g-inc nothing g0↑)))
            (proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n)                 ≡⟨ cong (λ eq → subst (Increasing-at n) eq
                                                                                (proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n)) $
                                                                               cong-pre-∘-ext (proj₁∘from∘to′ g g-inc nothing g0↑) ⟩
      subst (Increasing-at n)
            (⟨ext⟩ (proj₁∘from∘to′ g g-inc nothing g0↑ ∘ suc))
            (proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n)                 ≡⟨⟩

      subst (Increasing-at n)
            (⟨ext⟩ (proj₁∘from∘to′ (g ∘ suc) (g-inc ∘ suc) _ refl))
            (proj₂ (from (to (g ∘ suc , g-inc ∘ suc))) n)                 ≡⟨ proj₂∘from∘to (g ∘ suc) (g-inc ∘ suc) n _ refl ⟩∎

      g-inc (suc n)                                                       ∎

-- The two definitions of the delay monad are isomorphic (assuming
-- extensionality).

Delay↔Delay : Bisimilarity.Extensionality a →
              Delay A ↔ D.Delay A ∞
Delay↔Delay delay-ext = record
  { surjection = record
    { logical-equivalence = Delay⇔Delay
    ; right-inverse-of    = delay-ext ∘ to∘from
    }
  ; left-inverse-of = _↠_.right-inverse-of Delay↠Delay
  }
  where
  open Delay⇔Delay

  to∘from : ∀ x → [ i ] to (from x) ∼ x
  to∘from (now x)   = now
  to∘from (later x) = later λ { .force → to∘from (force x) }

-- There is a split surjection from ℕ → Maybe A (without any
-- requirement that the sequences are increasing) to D.Delay A ∞
-- (assuming extensionality).
--
-- Chapman, Uustalu and Veltri prove this result in "Quotienting the
-- Delay Monad by Weak Bisimilarity".

→↠Delay-coinductive : Bisimilarity.Extensionality a →
                      (ℕ → Maybe A) ↠ D.Delay A ∞
→↠Delay-coinductive delay-ext = record
  { logical-equivalence = record
    { to   = Delay⇔Delay.to₁
    ; from = proj₁ ∘ Delay⇔Delay.from
    }
  ; right-inverse-of = _↔_.right-inverse-of (Delay↔Delay delay-ext)
  }

-- There is also a split surjection from ℕ → Maybe A to Delay A.

→↠Delay-function : (ℕ → Maybe A) ↠ Delay A
→↠Delay-function = record
  { logical-equivalence = record
    { to   = Delay⇔Delay.from ∘ Delay⇔Delay.to₁
    ; from = proj₁
    }
  ; right-inverse-of = _↠_.right-inverse-of Delay↠Delay
  }

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Object.NaturalNumber.Properties.F-Algebras where

open import Level
open import Function using (_$_)

open import Categories.Category
open import Categories.Category.Construction.F-Algebras
open import Categories.Category.Cocartesian
open import Categories.Functor
open import Categories.Functor.Algebra
open import Categories.Object.Terminal renaming (up-to-iso to ⊤-up-to-iso)
open import Categories.Object.Initial

import Categories.Morphism.Reasoning as MR
import Categories.Object.NaturalNumber as NNO

-- A NNO is an inital algebra for the 'X ↦ ⊤ + X' endofunctor.
module _ {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-Terminal : Terminal 𝒞) (𝒞-Coproducts : BinaryCoproducts 𝒞) where

  open Terminal 𝒞-Terminal
  open BinaryCoproducts 𝒞-Coproducts
  open Category 𝒞
  open HomReasoning
  open Equiv
  open MR 𝒞
  open NNO 𝒞 𝒞-Terminal

  Maybe : Functor 𝒞 𝒞
  Maybe = record
    { F₀ = λ X → ⊤ + X
    ; F₁ = λ f → [ i₁ , i₂ ∘ f ]
    ; identity = []-cong₂ refl identityʳ ○ +-η
    ; homomorphism = +-unique (pullʳ inject₁ ○ inject₁) (pullʳ inject₂ ○ pullˡ inject₂ ○ assoc)
    ; F-resp-≈ = λ eq → []-cong₂ refl (∘-resp-≈ʳ eq)
    }

  private
    module Maybe = Functor Maybe

  Initial⇒NNO : Initial (F-Algebras Maybe) → NaturalNumber
  Initial⇒NNO initial = record
    { N = ⊥.A
    ; isNaturalNumber = record
      { z = ⊥.α ∘ i₁
      ; s = ⊥.α ∘ i₂
      ; universal = λ {A} q f →
        F-Algebra-Morphism.f (initial.! {A = alg q f})
      ; z-commute = λ {A} {q} {f} → begin
        q                                                                 ≈⟨ ⟺ inject₁ ⟩
        [ q , f ] ∘ i₁                                                    ≈⟨ pushʳ (⟺ inject₁) ⟩
        (([ q , f ] ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f initial.! ]) ∘ i₁) ≈⟨ pushˡ (⟺ (F-Algebra-Morphism.commutes (initial.! {A = alg q f}))) ⟩
        F-Algebra-Morphism.f initial.! ∘ ⊥.α ∘ i₁                         ∎
      ; s-commute = λ {A} {q} {f} → begin
        (f ∘ F-Algebra-Morphism.f initial.!) ≈⟨ pushˡ (⟺ inject₂) ⟩
        [ q , f ] ∘ i₂ ∘ F-Algebra-Morphism.f initial.!                 ≈⟨ pushʳ (⟺ inject₂) ⟩
        ([ q , f ] ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f initial.! ]) ∘ i₂ ≈⟨ pushˡ (⟺ (F-Algebra-Morphism.commutes (initial.! {A = alg q f}))) ⟩
        F-Algebra-Morphism.f initial.! ∘ ⊥.α ∘ i₂                       ∎
      ; unique = λ {A} {f} {q} {u} eqᶻ eqˢ → ⟺ $ initial.!-unique record
          { f = u
          ; commutes = begin
            u ∘ ⊥.α ≈⟨ ⟺ +-g-η ⟩
            [ (u ∘ ⊥.α) ∘ i₁ , (u ∘ ⊥.α) ∘ i₂ ] ≈⟨ []-cong₂ (assoc ○ ⟺ eqᶻ) (assoc ○ ⟺ eqˢ) ⟩
            [ f , q ∘ u ]                       ≈⟨ +-unique (pullʳ inject₁ ○ inject₁) (pullʳ inject₂ ○ pullˡ inject₂) ⟩
            [ f , q ] ∘ [ i₁ , i₂ ∘ u ]         ∎
          }
      }
    }
    where
      module initial = Initial initial
      module ⊥ = F-Algebra initial.⊥

      alg : ∀ {A} → (q : ⊤ ⇒ A) → (f : A ⇒ A) → F-Algebra Maybe
      alg {A} q f = record
        { A = A
        ; α = [ q , f ]
        }

  NNO⇒Initial : NaturalNumber → Initial (F-Algebras Maybe)
  NNO⇒Initial NNO = record
    { ⊥ = record
      { A = N
      ; α = [ z , s ]
      }
    ; ⊥-is-initial = record
      { ! = λ {alg} → record
        { f = universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂)
        ; commutes = begin
          universal _ _ ∘ [ z , s ]                                         ≈⟨ ∘-distribˡ-[] ⟩
          [ universal _ _ ∘ z , universal _ _ ∘ s ]                         ≈⟨ []-cong₂ (⟺ z-commute) (⟺ s-commute ○ assoc) ⟩
          [ F-Algebra.α alg ∘ i₁ , F-Algebra.α alg ∘ (i₂ ∘ universal _ _) ] ≈˘⟨ ∘-distribˡ-[] ⟩
          F-Algebra.α alg ∘ [ i₁ , i₂ ∘ universal _ _ ]                     ∎
        }
      ; !-unique = λ {A} f →
        let z-commutes = begin
              F-Algebra.α A ∘ i₁                                          ≈⟨ pushʳ (⟺ inject₁) ⟩
              (F-Algebra.α A ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f f ]) ∘ i₁ ≈˘⟨ F-Algebra-Morphism.commutes f ⟩∘⟨refl ⟩
              (F-Algebra-Morphism.f f ∘ [ z , s ]) ∘ i₁                   ≈⟨ pullʳ inject₁ ⟩
              F-Algebra-Morphism.f f ∘ z                                  ∎
            s-commutes = begin
              (F-Algebra.α A ∘ i₂) ∘ F-Algebra-Morphism.f f               ≈⟨ pullʳ (⟺ inject₂) ○ ⟺ assoc ⟩
              (F-Algebra.α A ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f f ]) ∘ i₂ ≈˘⟨ F-Algebra-Morphism.commutes f ⟩∘⟨refl ⟩
              (F-Algebra-Morphism.f f ∘ [ z , s ]) ∘ i₂                   ≈⟨ pullʳ inject₂ ⟩
              F-Algebra-Morphism.f f ∘ s                                  ∎
        in ⟺ $ unique z-commutes s-commutes
      }
    }
    where
      open NaturalNumber NNO

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:
{-

This file contains:

- Properties of set truncations

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SetTruncation.Properties where

open import Cubical.HITs.SetTruncation.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma

private
  variable
    ℓ : Level
    A : Type ℓ

rec : {B : Type ℓ} → isSet B → (A → B) → ∥ A ∥₂ → B
rec Bset f ∣ x ∣₂ = f x
rec Bset f (squash₂ x y p q i j) =
  Bset _ _ (cong (rec Bset f) p) (cong (rec Bset f) q) i j

-- lemma 6.9.1 in HoTT book
elim : {B : ∥ A ∥₂ → Type ℓ}
       (Bset : (x : ∥ A ∥₂) → isSet (B x))
       (g : (a : A) → B (∣ a ∣₂))
       (x : ∥ A ∥₂) → B x
elim Bset g ∣ a ∣₂ = g a
elim Bset g (squash₂ x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 Bset _ _
    (cong (elim Bset g) p) (cong (elim Bset g) q) (squash₂ x y p q) i j

setTruncUniversal : {B : Type ℓ} → isSet B → (∥ A ∥₂ → B) ≃ (A → B)
setTruncUniversal {B = B} Bset =
  isoToEquiv (iso (λ h x → h ∣ x ∣₂) (rec Bset) (λ _ → refl) rinv)
  where
  rinv : (f : ∥ A ∥₂ → B) → rec Bset (λ x → f ∣ x ∣₂) ≡ f
  rinv f i x =
    elim (λ x → isProp→isSet (Bset (rec Bset (λ x → f ∣ x ∣₂) x) (f x)))
         (λ _ → refl) x i

elim2 : {B : ∥ A ∥₂ → ∥ A ∥₂ → Type ℓ}
        (Bset : ((x y : ∥ A ∥₂) → isSet (B x y)))
        (g : (a b : A) → B ∣ a ∣₂ ∣ b ∣₂)
        (x y : ∥ A ∥₂) → B x y
elim2 Bset g = elim (λ _ → isSetΠ (λ _ → Bset _ _))
                    (λ a → elim (λ _ → Bset _ _) (g a))

elim3 : {B : (x y z : ∥ A ∥₂) → Type ℓ}
        (Bset : ((x y z : ∥ A ∥₂) → isSet (B x y z)))
        (g : (a b c : A) → B ∣ a ∣₂ ∣ b ∣₂ ∣ c ∣₂)
        (x y z : ∥ A ∥₂) → B x y z
elim3 Bset g = elim2 (λ _ _ → isSetΠ (λ _ → Bset _ _ _))
                     (λ a b → elim (λ _ → Bset _ _ _) (g a b))

setTruncIsSet : isSet ∥ A ∥₂
setTruncIsSet a b p q = squash₂ a b p q

setTruncIdempotent≃ : isSet A → ∥ A ∥₂ ≃ A
setTruncIdempotent≃ {A = A} hA = isoToEquiv f
  where
  f : Iso ∥ A ∥₂ A
  Iso.fun f = rec hA (idfun A)
  Iso.inv f x = ∣ x ∣₂
  Iso.rightInv f _ = refl
  Iso.leftInv f = elim (λ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ → refl)

setTruncIdempotent : isSet A → ∥ A ∥₂ ≡ A
setTruncIdempotent hA = ua (setTruncIdempotent≃ hA)

setSigmaIso : ∀ {ℓ} {B : A → Type ℓ} → Iso ∥ Σ A B ∥₂ ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
setSigmaIso {A = A} {B = B} = iso fun funinv sect retr
  where
  {- writing it out explicitly to avoid yellow highlighting -}
  fun : ∥ Σ A B ∥₂ → ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
  fun = rec setTruncIsSet λ {(a , p) → ∣ a , ∣ p ∣₂ ∣₂}
  funinv : ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂ → ∥ Σ A B ∥₂
  funinv = rec setTruncIsSet (λ {(a , p) → rec setTruncIsSet (λ p → ∣ a , p ∣₂) p})
  sect : section fun funinv
  sect = elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
              λ { (a , p) → elim {B = λ p → fun (funinv ∣ a , p ∣₂) ≡ ∣ a , p ∣₂}
              (λ p → isOfHLevelPath 2 setTruncIsSet _ _) (λ _ → refl) p }
  retr : retract fun funinv
  retr = elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
              λ { _ → refl }


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

module WithoutK7 where

data I : Set where
  i : I

data D (x : I) : Set where
  d : D x

data P (x : I) : D x → Set where

Foo : ∀ x → P x (d {x = x}) → Set
Foo x ()

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Issue249-2 where

postulate
  A B : Set

module A where
  X = A
  Y = B

-- open A renaming (X to C; Y to C)

open A using (X) renaming (Y to X)


text:
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Data.Fin using (Fin)
open import Data.Nat using (ℕ)
open import Data.Product using (_×_; _,_)
open import Data.Vec using (Vec; lookup; _[_]≔_)

open import Common

data Local (n : ℕ) : Set where
  endL : Local n
  sendSingle recvSingle : Fin n -> Label -> Local n -> Local n

private
  variable
    n : ℕ
    p p′ q : Fin n
    l l′ : Label
    lSub lSub′ : Local n

endL≢sendSingle : ∀ { lSub } -> endL {n} ≢ sendSingle q l lSub
endL≢sendSingle ()

endL≢recvSingle : ∀ { lSub } -> endL {n} ≢ recvSingle q l lSub
endL≢recvSingle ()

sendSingle-injective :
  sendSingle {n} p l lSub ≡ sendSingle p′ l′ lSub′
  -> p ≡ p′ × l ≡ l′ × lSub ≡ lSub′
sendSingle-injective refl = refl , refl , refl

recvSingle-injective :
  recvSingle {n} p l lSub ≡ recvSingle p′ l′ lSub′
  -> p ≡ p′ × l ≡ l′ × lSub ≡ lSub′
recvSingle-injective refl = refl , refl , refl

Configuration : ℕ -> Set
Configuration n = Vec (Local n) n

data _-_→l_ {n : ℕ} : (Fin n × Local n) -> Action n -> (Fin n × Local n) -> Set where
  →l-send :
    ∀ { lp lpSub }
    -> (p : Fin n)
    -> lp ≡ sendSingle q l lpSub
    -> (p≢q : p ≢ q)
    -> (p , lp) - (action p q p≢q l) →l (p , lpSub)
  →l-recv :
    ∀ { lp lpSub }
    -> (p : Fin n)
    -> lp ≡ recvSingle q l lpSub
    -> (q≢p : q ≢ p)
    -> (p , lp) - (action q p q≢p l) →l (p , lpSub)

data _-_→c_ {n : ℕ} : Configuration n -> Action n -> Configuration n -> Set where
  →c-comm :
    ∀ { lp lp′ lq lq′ c′ p≢q-p p≢q-q }
    -> (c : Configuration n)
    -> (p≢q : p ≢ q)
    -> lp ≡ lookup c p
    -> lq ≡ lookup c q
    -> c′ ≡ c [ p ]≔ lp′ [ q ]≔ lq′
    -> (p , lp) - (action p q p≢q-p l) →l (p , lp′)
    -> (q , lq) - (action p q p≢q-q l) →l (q , lq′)
    -> c - (action p q p≢q l) →c  c′

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:
module Test where

open import Algebra using (CommutativeRing; IsCommutativeRing)

open import Assume using (assume)
import Data.Nat as ℕ
open ℕ using (ℕ; zero; suc)

import Data.Fin as F
open F using (Fin)

open import Relation.Binary using (Rel; Setoid; _Preserves_⟶_)
open import Function using (Inverse; _on_; _∘_; _|>_; id; flip)

open import Algebra.Module using (Module)
module Mod = Module

open import Data.Product using (_,_; proj₂; _×_)

open import Algebra.Module.Construct.DirectProduct using () renaming (⟨module⟩ to ×-module)
open import Level using (_⊔_; Level; 0ℓ; Lift)
open import Data.Vec.Recursive
open import Algebra.Module.Vec.Recursive

module _
  {r ℓ} {CR : CommutativeRing r ℓ}
  where

  -- D B k is the solution to
  -- (A → X) → A ^ suc k → B
  -- i.e. D B k ~ A ^ k → B

  open Module

  D : ∀ {m ℓm} (M : Module CR m ℓm) → ℕ → Set _
  D {m = m} M k = ∀ {X : Set m} → X ^ suc k → Carrierᴹ M

  const
    : ∀ {m ℓm} {{M : Module CR m ℓm}}
    → ∀ {k} → Carrierᴹ M → D M k
  const {k = zero} c x = c
  const {{M}} {k = suc k} c v = 0ᴹ M

  double
    : ∀ {m ℓm} {{M : Module CR m ℓm}}
    → ∀ {k} → D M k → D M k
  double {{M}} x y = let x' = x y in _+ᴹ_ M x' x'

  -- D : Level → ∀ {n ℓn} (N : Module CR n ℓn) → ℕ → Set _
  -- D m N k = {M : Set m} → M → M ^ k → Carrierᴹ N

  -- compose
  --   : ∀ {x} {X : Set x}
  --   → ∀ {n ℓn} {N : Module CR n ℓn}
  --   → ∀ {o ℓo} {O : Module CR o ℓo}
  --   → ∀ {k} → (f : X → D N k) → (g : Carrierᴹ N → D O k)
  --   → X → D O k
  -- compose = ?

  -- _th-derivative_ : ∀ k → (D k → D k) → M.Carrierᴹ → N.Carrierᴹ

  -- k th-derivative f = {!   !}

  -- TODO
  -- can we use M → D N k everywhere?!
  -- data D : ℕ → Set (m ⊔ n) where
  --   z : N.Carrierᴹ → D zero
  --   d : ∀ {k} → (fx : N.Carrierᴹ) → (dfx : M.Carrierᴹ → D k) → D (suc k)

-- module _
--   {r ℓ} {CR : CommutativeRing r ℓ}
--   {m ℓm} {M : Module CR m ℓm}
--   {n ℓn} {N : Module CR n ℓn}
--   where

--   private
--     module CR = CommutativeRing CR
--     module M = Module M
--     module N = Module N

--   private
--     module dmod where

--       Carrierᴹ : ∀ {k : ℕ} → Set (m ⊔ n)
--       Carrierᴹ {k} = D M N k

--       _≈ᴹ_ : ∀ {k} → Rel (D M N k) (m ⊔ ℓn)
--       _≈ᴹ_ (z x) (z y) = Lift (m ⊔ ℓn) (x N.≈ᴹ y)
--       _≈ᴹ_ (d fx dfx) (d fy dfy) = (fx N.≈ᴹ fy) × (∀ v → dfx v ≈ᴹ dfy v)

--       _+ᴹ_ : ∀ {k} → (x y : D M N k) → D M N k
--       _+ᴹ_ (z x) (z y) = z (x N.+ᴹ y)
--       _+ᴹ_ (d fx dfx) (d fy dfy) = d (fx N.+ᴹ fy) λ v → dfx v +ᴹ dfy v

--       _*ₗ_ : ∀ {k} → (s : CR.Carrier) (x : D M N k) → D M N k
--       _*ₗ_ s (z x) = z (s N.*ₗ x)
--       _*ₗ_ s (d fx dfx) = d (s N.*ₗ fx) λ v → s *ₗ dfx v

--       _*ᵣ_ : ∀ {k} → (x : D M N k) (s : CR.Carrier) → D M N k
--       _*ᵣ_ = flip _*ₗ_

--       0ᴹ : ∀ {k} → D M N k
--       0ᴹ {zero} = z N.0ᴹ
--       0ᴹ {suc k} = d N.0ᴹ λ v → 0ᴹ

--       -ᴹ_ : ∀ {k} → D M N k → D M N k
--       -ᴹ_ (z x) = z (N.-ᴹ x)
--       -ᴹ_ (d fx dfx) = d (N.-ᴹ fx) λ v → -ᴹ dfx v

--   instance
--     D-module : ∀ {k : ℕ} → Module CR _ _
--     D-module {k} =
--       record
--       { Carrierᴹ = dmod.Carrierᴹ {k}
--       ; isModule = assume
--       ; dmod
--       }

--   private variable k : ℕ

--   run : D M N k → N.Carrierᴹ
--   run (z x) = x
--   run (d x _) = x

--   extract : D M N zero → N.Carrierᴹ
--   extract = run

--   diff : M.Carrierᴹ → D M N (suc k) → D M N k
--   diff v (d _ x) = x v

--   konst _# : ∀ (c : N.Carrierᴹ) → D M N k
--   konst {k = zero} c = z c
--   konst {k = suc k} c = d c (λ v → konst N.0ᴹ)
--   x # = konst x

--   jacobian : (df : D M N 1) (v : M.Carrierᴹ) → N.Carrierᴹ
--   jacobian df v = df |> diff v |> extract

--   hessian : (df : D M N 2) (v v' : M.Carrierᴹ) → N.Carrierᴹ
--   hessian df v v' = df |> diff v |> diff v' |> extract

--   hack : ∀ {l} → D M N (suc l) → D M N l
--   hack {zero} (d fx dfx) = z fx
--   hack {suc l} (d fx dfx) = d fx λ v → hack {l} (dfx v)

module _ where
  import Real as ℝ
  open ℝ using (ℝ)

  open import Data.Vec.Recursive

  ℝ-isCommutativeRing : IsCommutativeRing ℝ._≈_ ℝ._+_ ℝ._*_ ℝ.-_ 0.0 1.0
  ℝ-isCommutativeRing = assume

  instance
    ℝ-commutativeRing : CommutativeRing 0ℓ 0ℓ
    ℝ-commutativeRing = record { isCommutativeRing = ℝ-isCommutativeRing }

  ℝ-cr : CommutativeRing 0ℓ 0ℓ
  ℝ-cr = ℝ-commutativeRing

  private
    ℝ-mod' : Module ℝ-commutativeRing 0ℓ 0ℓ
    ℝ-mod' = U.⟨module⟩
      where import Algebra.Module.Construct.TensorUnit as U

  ℝ^ : ∀ n → Module ℝ-commutativeRing 0ℓ 0ℓ
  ℝ^ n = ℝ-mod' ^ᴹ n

  ℝ-mod : Module ℝ-commutativeRing 0ℓ 0ℓ
  ℝ-mod = ℝ^ 1

  exp : ∀ {k} → D ℝ-mod k → D ℝ-mod k
  exp {0} f x = ℝ.e^ f x
  exp {1} f' xdx = let (fx , f'x) = f xdx in {! (ℝ.e^ fx) ℝ.* f'x   !}
  exp {k} f y = {!   !}

--   -- TODO
--   -- is this really the identity?
--   var : ∀ {rank k} (c : Mod.Carrierᴹ (ℝ^ rank)) → D (ℝ^ rank) (ℝ^ rank) k
--   var {rank} {zero} c = z c
--   var {rank} {suc n} c = d c (λ v → konst (replicate rank 1.0))

--   instance
--     ℝ^n : ∀ {n} → Module ℝ-cr 0ℓ 0ℓ
--     ℝ^n {n} = ℝ^ n

--   infixl 6 _+_ _-_
--   infixl 7 _*_
--   -- linear and bilinear forms
--   _*_
--     : ∀ {m ℓm} {M : Module ℝ-cr m ℓm} {k rank}
--     → (x y : D M (ℝ^ rank) k)
--     → D M (ℝ^ rank) k

--   open Module {{...}}
--   _+_ _-_
--     : ∀ {r ℓ} {CR : CommutativeRing r ℓ} {m ℓm} {{M : Module CR m ℓm}} (x y : Mod.Carrierᴹ M)
--     → Mod.Carrierᴹ M
--   x + y = x +ᴹ y
--   x - y = x +ᴹ (-ᴹ y)

--   _*_ {rank = rank} (z x) (z y) = z (zipWith ℝ._*_ rank x y)
--   _*_ {rank = rank} dfx@(d fx f'x) dgx@(d gx g'x) =
--     d (zipWith ℝ._*_ rank fx gx) (λ v → hack dfx * g'x v + hack dgx * f'x v)

--   -- convenience function
--   _>-<_
--     : ∀ {k}
--     → (f : ℝ → ℝ) (f' : ∀ {l} → D ℝ-mod ℝ-mod l → D ℝ-mod ℝ-mod l)
--     → D ℝ-mod ℝ-mod k → D ℝ-mod ℝ-mod k
--   (f >-< _) (z x) = z (f x)
--   (f >-< f') dfx@(d x dx) = d (f x) λ v → dx v * f' (hack dfx)

--   ε : ∀ {rank} → Fin rank → ℝ ^ rank
--   ε {zero} n = _
--   ε {suc zero} _ = 1.0
--   ε {2+ rank} F.zero = 1.0 , Mod.0ᴹ (ℝ^ (suc rank))
--   ε {2+ rank} (F.suc n) = Mod.0ᴹ ℝ-mod , ε n

--   ∇_ grad : ∀ {rank} → D (ℝ^ rank) (ℝ^ 1) 1 → ℝ ^ rank
--   ∇_ {rank = rank} f = map (jacobian f) rank unitvecs
--     where
--       unitvecs : (ℝ ^ rank) ^ rank
--       unitvecs = map ε rank (tabulate rank id)

--   grad = ∇_

--   infixl 8 _**_
--   infixr 9 -_
--   infixr 9 e^_

--   -_
--     : ∀ {r ℓ} {CR : CommutativeRing r ℓ} {m ℓm} {{M : Module CR m ℓm}} (x : Mod.Carrierᴹ M)
--     → Mod.Carrierᴹ M
--   -_ x = -ᴹ x

--   ℝ-sgn : ℝ → ℝ
--   ℝ-sgn x = if does (0.0 ℝ.≤? x) then 1.0 else ℝ.- 1.0
--     where
--       open import Data.Bool using (if_then_else_)
--       open import Relation.Nullary using (does)

--   ℝ-abs : ℝ → ℝ
--   ℝ-abs x = x ℝ.* ℝ-sgn x

--   -- the first is the zero-order
--   poly : ∀ {rank k} → ℝ ^ suc rank → D ℝ-mod ℝ-mod k → D ℝ-mod ℝ-mod k
--   poly {rank = zero} cs x = konst cs
--   poly {rank = suc rank} (c , cs) x = konst c + x * poly cs x

--   pow : ℕ → ∀ {k} → D ℝ-mod ℝ-mod k → D ℝ-mod ℝ-mod k
--   pow 0 x = konst 1.0
--   pow 1 x = x
--   pow (suc n) dx = dx * pow n dx

--   log e^_ recip abs sgn : ∀ {k} → D ℝ-mod ℝ-mod k → D ℝ-mod ℝ-mod k
--   log = ℝ.log >-< recip ∘ abs

--   recip (z x) = z (1.0 ℝ.÷ x)
--   recip dfx@(d fx f'x) = d (1.0 ℝ.÷ fx) λ x → - (f'x x * tmp * tmp)
--     where
--       tmp = recip (hack dfx)

--   abs = ℝ-abs >-< sgn

--   sgn = ℝ-sgn >-< λ _ → 0ᴹ

--   e^ z x = z (ℝ.e^ x)
--   e^ dfx@(d fx f'x) = d (run tmp) λ v → f'x v * tmp
--     where
--       tmp = e^ hack dfx

--   infixl 7 _÷_
--   _÷_ _**_ : ∀ {k} (x y : D ℝ-mod ℝ-mod k) → D ℝ-mod ℝ-mod k
--   x ÷ y = x * recip x
--   x ** y = e^ y * log x

--   _! : ℕ → ℕ
--   0 ! = 1
--   1 ! = 1
--   sucn@(suc n) ! = sucn ℕ.* (n !)

--   sterling : ∀ {k} → ℕ → D ℝ-mod ℝ-mod k
--   sterling {k} m = m' * log m' - m'
--     where
--       m' : D ℝ-mod ℝ-mod k
--       m' = ℝ.fromℕ m #

--   -- without the constant denominator term
--   logPoisson' : ∀ {n} → ℕ → D ℝ-mod ℝ-mod n → D ℝ-mod ℝ-mod n
--   logPoisson' k λ' = k' * log λ' - λ'
--     where k' = ℝ.fromℕ k #

--   logPoisson : ∀ {n} → ℕ → D ℝ-mod ℝ-mod n → D ℝ-mod ℝ-mod n
--   logPoisson k λ' = logPoisson' k λ' - sterling k

--   -- descend : ∀ {rank} (f : D (ℝ^ rank) 1 → D ℝ-mod 1) (steps : ℕ) (start : ℝ ^ rank) → ℝ ^ rank
--   -- descend f zero start = start
--   -- descend f (suc steps) start = {!   !}

--   module _ where
--     open import Relation.Binary.PropositionalEquality using (refl)

--     _ : (∇ (var 1.0 * var 1.0)) ℝ.≈ 2.0
--     _ = refl

-- -- -- --   _ : run e^_ 2.0 ℝ.≈ (ℝ.e^ 2.0)
-- -- -- --   _ = refl

-- -- -- --   testpoly : ∀ {n} → D ℝ-mod n → D ℝ-mod n
-- -- -- --   testpoly = poly (1.0 , 2.0 , 3.0)

-- -- -- --   _ : run testpoly 2.0 ℝ.≈ (1.0 + 4.0 + 12.0)
-- -- -- --   _ = refl

-- -- -- --   _ : ∇ testpoly [ 2.0 ] ℝ.≈ (0.0 + 2.0 + 3.0 ℝ.* 2.0 ℝ.* 2.0)
-- -- -- --   _ = refl

-- -- -- --   _ : ∇ testpoly [ 7.0 ] ℝ.≈ (0.0 + 2.0 + 2.0 ℝ.* 3.0 ℝ.* 7.0)
-- -- -- --   _ = refl

-- -- -- --   _ : hessian e^_ 1.0 1.0 0.0 ℝ.≈ (ℝ.e^ 1.0)
-- -- -- --   _ = refl

-- -- -- --   asdf : D ℝ-mod 2
-- -- -- --   asdf = e^ var (2.0 , 1.0 , 0.0)

-- -- -- --   _ : hessian (poly (1.0 , 2.0 , 3.0)) 1.0 1.0 0.0 ℝ.≈ (2.0 ℝ.* 3.0)
-- -- -- --   _ = refl

-- -- -- --   _ : ∇ log [ 1.0 ] ℝ.≈ 1.0
-- -- -- --   _ = refl

-- -- -- --   _ : ∇ log [ -ᴹ 1.0 ] ℝ.≈ 1.0
-- -- -- --   _ = refl

-- -- -- --   _ : ∇ sgn [ 2.0 ] ℝ.≈ 0.0
-- -- -- --   _ = refl

-- -- -- --   _ : ∇ abs [ 2.0 ] ℝ.≈ 1.0
-- -- -- --   _ = refl

-- -- -- --   _ : run abs (- 2.0) ℝ.≈ 2.0
-- -- -- --   _ = refl

-- -- -- --   _ : ∇ abs [ - 1.0 ] ℝ.≈ (- 1.0)
-- -- -- --   _ = refl

-- -- -- --   _ : ∇ recip [ - 2.0 ] ℝ.≈ (- 0.25)
-- -- -- --   _ = refl

-- -- -- --   _ : ∇ log [ 2.0 ] ℝ.≈ 0.5
-- -- -- --   _ = refl

max_stars_repo_name: cspollard/diff

max_issues_repo_name: cspollard/diff

max_forks_repo_name: cspollard/diff


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

open import HoTT
open import cohomology.CofiberSequence
open import cohomology.FunctionOver

module cohomology.MayerVietoris {i} where

{- Mayer-Vietoris Sequence: Given a span X ←f– Z –g→ Y, the cofiber space
   of the natural map [reglue : X ∨ Y → X ⊔_Z Y] (defined below) is equivalent
   to the suspension of Z. -}

{- Relevant functions -}
module MayerVietorisFunctions (ps : ⊙Span {i} {i} {i}) where

  open ⊙Span ps

  module Reglue = WedgeRec
    {X = ⊙Span.X ps} {Y = ⊙Span.Y ps} {C = fst (⊙Pushout ps)}
    left right (! (ap left (snd f)) ∙ glue (snd Z) ∙' ap right (snd g))

  reglue : X ∨ Y → fst (⊙Pushout ps)
  reglue = Reglue.f

  ⊙reglue : fst (X ⊙∨ Y ⊙→ ⊙Pushout ps)
  ⊙reglue = (reglue , idp)

  module MVDiff = SuspensionRec (fst Z) {C = Suspension (X ∨ Y)}
    (north _)
    (north _)
    (λ z → merid _ (winl (fst f z)) ∙ ! (merid _ (winr (fst g z))))

  mv-diff : Suspension (fst Z) → Suspension (X ∨ Y)
  mv-diff = MVDiff.f

  ⊙mv-diff : fst (⊙Susp Z ⊙→ ⊙Susp (X ⊙∨ Y))
  ⊙mv-diff = (mv-diff , idp)

{- We use path induction (via [⊙pushout-J]) to assume that the
   basepoint preservation paths of the span maps are [idp]. The module
   [Base] contains the proof of the theorem for this case. -}
module MayerVietorisBase
  {A B : Type i} (Z : Ptd i) (f : fst Z → A) (g : fst Z → B) where

  X = ⊙[ A , f (snd Z) ]
  Y = ⊙[ B , g (snd Z) ]
  ps = ⊙span X Y Z (f , idp) (g , idp)
  F : fst (Z ⊙→ X)
  F = (f , idp)
  G : fst (Z ⊙→ Y)
  G = (g , idp)

  open MayerVietorisFunctions ps

  {- Definition of the maps
       into : Cofiber reglue → ΣZ
       out  : ΣZ → Cofiber reglue
   -}

  private
    into-glue-square :
      Square idp idp (ap (ext-glue ∘ reglue) wglue) (merid _ (snd Z))
    into-glue-square =
      connection ⊡v∙
      ! (ap-∘ ext-glue reglue wglue ∙ ap (ap ext-glue) Reglue.glue-β
         ∙ ExtGlue.glue-β (snd Z))

    module IntoGlue = WedgeElim {P = λ xy → north _ == ext-glue (reglue xy)}
      (λ _ → idp)
      (λ _ → merid _ (snd Z))
      (↓-cst=app-from-square into-glue-square)

    into-glue = IntoGlue.f

  module Into = CofiberRec reglue (north _) ext-glue into-glue

  private
    out-glue-and-square : (z : fst Z)
      → Σ (cfbase reglue == cfbase reglue)
          (λ p → Square (cfglue _ (winl (f z))) p
                   (ap (cfcod _) (glue z)) (cfglue _ (winr (g z))))
    out-glue-and-square z = fill-square-top _ _ _

    out-glue = fst ∘ out-glue-and-square
    out-square = snd ∘ out-glue-and-square

  module Out = SuspensionRec (fst Z) {C = Cofiber reglue}
    (cfbase _)
    (cfbase _)
    out-glue

  into = Into.f
  out = Out.f

  {- [out] is a right inverse for [into] -}

  private
    into-out-sq : (z : fst Z) →
      Square idp (ap into (ap out (merid _ z))) (merid _ z) (merid _ (snd Z))
    into-out-sq z =
      (ap (ap into) (Out.glue-β z) ∙v⊡
        (! (Into.glue-β (winl (f z)))) ∙h⊡
          ap-square into (out-square z)
        ⊡h∙ (Into.glue-β (winr (g z))))
      ⊡v∙ (∘-ap into (cfcod _) (glue z) ∙ ExtGlue.glue-β z)

  into-out : ∀ σ → into (out σ) == σ
  into-out = Suspension-elim (fst Z)
    idp
    (merid _ (snd Z))
    (λ z → ↓-∘=idf-from-square into out (into-out-sq z))

  {- [out] is a left inverse for [into] -}

  {- [out] is left inverse on codomain part of cofiber space,
   - i.e. [out (into (cfcod _ γ)) == cfcod _ γ] -}

  private
    out-into-cod-square : (z : fst Z) →
      Square (cfglue reglue (winl (f z)))
             (ap (out ∘ ext-glue {s = ⊙span-out ps}) (glue z))
             (ap (cfcod _) (glue z)) (cfglue _ (winr (g z)))
    out-into-cod-square z =
      (ap-∘ out ext-glue (glue z)
        ∙ ap (ap out) (ExtGlue.glue-β z) ∙ Out.glue-β z)
      ∙v⊡ out-square z

    module OutIntoCod = PushoutElim
      {d = ⊙span-out ps} {P = λ γ → out (into (cfcod _ γ)) == cfcod _ γ}
      (λ x → cfglue _ (winl x))
      (λ y → cfglue _ (winr y))
      (λ z → ↓-='-from-square (out-into-cod-square z))

    out-into-cod = OutIntoCod.f

  {- Cube move lemma for the left inverse coherence. This is used to
     build up a right square (in this case starting from a cube filler)  -}
  private
    square-push-rb : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A} {b : A}
      {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == b}
      (q : b == a₁₁) (sq : Square p₀₋ p₋₀ p₋₁ (p₁₋ ∙ q))
      → Square p₀₋ p₋₀ (p₋₁ ∙' ! q) p₁₋
    square-push-rb {p₁₋ = idp} idp sq = sq

    right-from-bot-lemma : ∀ {i} {A : Type i}
      {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ b₀ b₁ : A}
      {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
      {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
      {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

      {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
      {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
      (sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) -- right

      {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == b₀}
      {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == b₁}
      {q₀₋ : a₀₁₁ == b₀} {q₋₁ : b₀ == b₁} {q₁₋ : a₁₁₁ == b₁}
      {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ (p₀₋₁ ∙ q₀₋)} -- back
      {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
      {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ q₋₁} -- bottom
      {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ (p₁₋₁ ∙ q₁₋)} -- front
      (sq' : Square q₀₋ p₋₁₁ q₋₁ q₁₋)
      (cu : Cube sq₋₋₀ sq₋₋₁ (square-push-rb q₀₋ sq₀₋₋)
                 sq₋₀₋ (sq₋₁₋ ⊡h' !□h (square-symmetry sq'))
                 (square-push-rb q₁₋ sq₁₋₋))
      → Cube sq₋₋₀ (sq₋₋₁ ⊡v sq') sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    right-from-bot-lemma sq₋₋₁ ids cu = right-from-bot-lemma' sq₋₋₁ cu
      where
      right-from-bot-lemma' : ∀ {i} {A : Type i}
        {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
        {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
        {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
        {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

        {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
        {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
        (sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) -- right

        {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
        {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
        {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ (p₀₋₁ ∙ idp)} -- back
        {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
        {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
        {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ (p₁₋₁ ∙ idp)} -- front
        (cu : Cube sq₋₋₀ sq₋₋₁ (square-push-rb idp sq₀₋₋) sq₋₀₋
                   (sq₋₁₋ ⊡h' !□h (square-symmetry vid-square))
                   (square-push-rb idp sq₁₋₋))
        → Cube sq₋₋₀ (sq₋₋₁ ⊡v vid-square) sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
      right-from-bot-lemma' ids cu = cu

  {- Proving the coherence term for the left inverse. This means proving
     [(w : X ∨ Y) → Square idp (ap out (ap into (glue w)))
                               (cfglue _ w) (out-into-cod (reglue w))]
  -}

  private
    out-into-sql : (x : fst X) → Square idp (ap out (into-glue (winl x)))
                                        (cfglue _ (winl x)) (cfglue _ (winl x))
    out-into-sql x = connection

    out-into-fill : Σ (Square idp (ap out (glue (snd Z))) idp idp) (λ sq →
      Cube (out-into-sql (snd X)) sq
           (natural-square (λ _ → idp) wglue)
           (natural-square (ap out ∘ into-glue) wglue)
           (natural-square (cfglue _) wglue
             ⊡h' !□h (square-symmetry connection))
           (square-push-rb (cfglue _ (winr (snd Y)))
             (natural-square (out-into-cod ∘ reglue) wglue)))
    out-into-fill = fill-cube-right _ _ _ _ _

    {- [fst out-into-fill] is chosen so that we can prove
       [out-into-sql == out-into-sqr [ ⋯ ↓ ⋯ ]];
       this is proven by massaging [out-into-fill-cube] into the right shape.
       The trick is that the type of [out-into-fill-square] is independent of
       [y], so we can pick it to give the right result at the basepoint.
    -}
    out-into-sqr : (y : fst Y)
      → Square idp (ap out (into-glue (winr y)))
               (cfglue _ (winr y)) (cfglue _ (winr y))
    out-into-sqr y = fst out-into-fill ⊡v connection

  out-into : ∀ κ → out (into κ) == κ
  out-into = Cofiber-elim reglue
    idp out-into-cod
    (λ w → ↓-∘=idf-from-square out into $
       ap (ap out) (Into.glue-β w) ∙v⊡
         Wedge-elim
           {P = λ w → Square idp (ap out (into-glue w))
                             (cfglue _ w) (out-into-cod (reglue w))}
           out-into-sql
           out-into-sqr
           (cube-to-↓-square $
             right-from-bot-lemma (fst out-into-fill) connection $
               (snd out-into-fill))
           w)

  {- equivalence and paths -}

  eq : Cofiber reglue ≃ Suspension (fst Z)
  eq = equiv into out into-out out-into

  path : Cofiber reglue == Suspension (fst Z)
  path = ua eq

  ⊙path : ⊙Cof ⊙reglue == ⊙Susp Z
  ⊙path = ⊙ua eq idp

  {- Transporting [cfcod reglue] over the equivalence -}

  cfcod-over : ⊙cfcod ⊙reglue == ⊙ext-glue
              [ (λ W → fst (⊙Pushout ps ⊙→ W)) ↓ ⊙path ]
  cfcod-over =
    codomain-over-⊙equiv (⊙cfcod ⊙reglue) eq idp ▹ lemma
    where
    lemma : (into , idp) ⊙∘ ⊙cfcod ⊙reglue == ⊙ext-glue
    lemma = pair= idp $
      ap into (! (cfglue reglue (winl (snd X)))) ∙ idp
        =⟨ ap-! into (cfglue reglue (winl (snd X))) |in-ctx (λ w → w ∙ idp) ⟩
      ! (ap into (cfglue reglue (winl (snd X)))) ∙ idp
        =⟨ Into.glue-β (winl (snd X)) |in-ctx (λ w → ! w ∙ idp) ⟩
      idp ∎

  {- Transporting [ext-glue] over the equivalence. Uses the same sort of
   - cube technique as in the proof of [⊙path]. -}

  private
    square-push-rt : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A} {b : A}
      {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : b == a₁₁}
      (q : a₁₀ == b) (sq : Square p₀₋ p₋₀ p₋₁ (q ∙' p₁₋))
      → Square p₀₋ (p₋₀ ∙' q) p₋₁ p₁₋
    square-push-rt {p₁₋ = idp} idp sq = sq

    right-from-top-lemma : ∀ {i} {A : Type i}
      {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ b₀ b₁ : A}
      {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
      {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
      {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

      {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
      {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
      (sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) -- right

      {p₀₀₋ : a₀₀₀ == b₀ {-a₀₀₁-}} {p₀₁₋ : a₀₁₀ == a₀₁₁}
      {p₁₀₋ : a₁₀₀ == b₁ {-a₁₀₁-}} {p₁₁₋ : a₁₁₀ == a₁₁₁}
      {q₀₋ : b₀ == a₀₀₁} {q₋₀ : b₀ == b₁} {q₁₋ : b₁ == a₁₀₁}
      {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ (q₀₋ ∙' p₀₋₁)} -- back
      {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ q₋₀} -- top
      {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
      {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ (q₁₋ ∙' p₁₋₁)} -- front
      (sq' : Square q₀₋ q₋₀ p₋₀₁ q₁₋)
      (cu : Cube sq₋₋₀ sq₋₋₁ (square-push-rt q₀₋ sq₀₋₋)
                 (sq₋₀₋ ⊡h' square-symmetry sq') sq₋₁₋
                 (square-push-rt q₁₋ sq₁₋₋))
      → Cube sq₋₋₀ (sq' ⊡v' sq₋₋₁) sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    right-from-top-lemma sq₋₋₁ ids cu = right-from-top-lemma' sq₋₋₁ cu
      where
      right-from-top-lemma' : ∀ {i} {A : Type i}
        {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
        {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
        {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
        {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

        {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
        {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
        (sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) -- right

        {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
        {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
        {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ (idp ∙' p₀₋₁)} -- back
        {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
        {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
        {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ (idp ∙' p₁₋₁)} -- front
        (cu : Cube sq₋₋₀ sq₋₋₁ (square-push-rt idp sq₀₋₋)
                   (sq₋₀₋ ⊡h' square-symmetry vid-square) sq₋₁₋
                   (square-push-rt idp sq₁₋₋))
        → Cube sq₋₋₀ (vid-square ⊡v' sq₋₋₁) sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
      right-from-top-lemma' ids cu = cu

  ext-over : ⊙ext-glue == ⊙mv-diff
             [ (λ W → fst (W ⊙→ ⊙Susp (X ⊙∨ Y))) ↓ ⊙path ]
  ext-over = ⊙λ= fn-lemma idp ◃ domain-over-⊙equiv ⊙mv-diff _ _
    where
    fn-lemma : ∀ κ → ext-glue κ == mv-diff (into κ)
    fn-lemma = Cofiber-elim reglue
      idp fn-cod
      (λ w → ↓-='-from-square $
        ExtGlue.glue-β w ∙v⊡
          fn-coh w
        ⊡v∙ ! (ap-∘ mv-diff into (glue w) ∙ ap (ap mv-diff) (Into.glue-β w)))
      where
      fn-cod : (γ : fst (⊙Pushout ps))
        → ext-glue (cfcod reglue γ) == mv-diff (ext-glue γ)
      fn-cod = Pushout-elim
        (λ x → ! (merid _ (winl x)))
        (λ y → ! (merid _ (winr y)))
        (λ z → ↓-='-from-square $
          ap-cst (south _) (glue z) ∙v⊡
            (bl-square (merid _ (winl (f z))) ⊡h connection)
          ⊡v∙ ! (ap-∘ mv-diff ext-glue (glue z)
                 ∙ ap (ap mv-diff) (ExtGlue.glue-β z)
                 ∙ MVDiff.glue-β z))

      fn-fill : Σ (Square idp idp (ap mv-diff (merid _ (snd Z))) idp)
        (λ sq → Cube (tr-square (merid _ (winl (snd X)))) sq
                     (natural-square (λ _ → idp) wglue)
                     (natural-square (merid _) wglue
                       ⊡h' square-symmetry (tr-square (merid _ (winr (snd Y)))))
                     (natural-square (ap mv-diff ∘ into-glue) wglue)
                     (square-push-rt (! (merid _ (winr (snd Y))))
                       (natural-square (fn-cod ∘ reglue) wglue)))
      fn-fill = fill-cube-right _ _ _ _ _

      fn-coh : (w : X ∨ Y)
        → Square idp (merid _ w) (ap mv-diff (into-glue w)) (fn-cod (reglue w))
      fn-coh = Wedge-elim
        (λ x → tr-square (merid _ (winl x)))
          (λ y → tr-square (merid _ (winr y)) ⊡v' (fst fn-fill))
        (cube-to-↓-square $ right-from-top-lemma
          (fst fn-fill)
          (tr-square (merid _ (winr (snd Y))))
          (snd fn-fill))

{- Main results -}
module MayerVietoris (ps : ⊙Span {i} {i} {i}) where

  private
    record Results (ps : ⊙Span {i} {i} {i}) : Type (lsucc i) where
      open ⊙Span ps
      open MayerVietorisFunctions ps public
      field
        eq : Cofiber reglue ≃ Suspension (fst Z)
        path : Cofiber reglue == Suspension (fst Z)
        ⊙path : ⊙Cof ⊙reglue == ⊙Susp Z
        cfcod-over : ⊙cfcod ⊙reglue == ⊙ext-glue
                     [ (λ W → fst (⊙Pushout ps ⊙→ W)) ↓ ⊙path ]
        ext-over : ⊙ext-glue == ⊙mv-diff
                   [ (λ W → fst (W ⊙→ ⊙Susp (X ⊙∨ Y))) ↓ ⊙path ]

    results : Results ps
    results = ⊙pushout-J Results base-results ps
      where
      base-results : ∀ {A} {B} Z (f : fst Z → A) (g : fst Z → B) →
        Results (⊙span _ _ Z (f , idp) (g , idp))
      base-results Z f g = record {
        eq = eq;
        path = path;
        ⊙path = ⊙path;
        cfcod-over = cfcod-over;
        ext-over = ext-over}
        where open MayerVietorisBase Z f g

    open Results results public

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
module Id1 where

import Level
open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Data.Bool using (Bool)
open import Data.Sum using (_⊎_)
open import Data.Nat
open import Data.Product
open import Data.Vec
open import Function using (id)

-- Study identity types from first principles

-- As we have seen for the previous types, we need to define the type,
-- its constructors, and then focus on the recursion and induction
-- principles. All computations and all properties of the identity
-- type should be derivable from these (recursion and induction)
-- principles.

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

data _≡_ {A : Set} : (x y : A) → Set where
  refl : (x : A) → x ≡ x

-- We have to write (refl x) for some x. This is different from the
-- Agda library which leaves the 'x' implicit

infix 4 _≡_

{--
Convention:
multiplicative          precedence 7
additive                precedence 6
equality and comparison precedence 4
--}

-- Simple examples

private
  p₁ : 3 ≡ 3
  p₁ = refl 3

  p₂ : 3 * 1 ≡ 1 + 2
  p₂ = refl (4 ∸ 1)

-- Let's try to derive the recursion principle for identity
-- types... This type has one constructor just like ⊤ in some sense.
-- Recall the recursion principle for ⊤:
-- rec⊤ : (C : Set) → C → (v : ⊤) → C

-- So at first approximation, the recursion principle for ≡ looks like:

--
-- rec≡ : (C : Set) → C → ({A : Set} {x y : A} (p : x ≡ y) → C)
--

-- In the case of ⊤, we wanted to map the element of ⊤ to an element
-- of C. For ≡, we also want to map the element of (x ≡ y) to an
-- element of C. Note that the element of (x ≡ y) is some kind of
-- relation between x and y so it makes sense to insist that the
-- target C is also a relation between x and y, i.e., we map relations
-- to relations.

-- So as a second approximation, the recursion principle for ≡ looks like:

--
-- rec≡ : {A : Set} {x y : A} →
--        (R : A → A → Set) → R x y → (p : x ≡ y) → R x y
--

-- In the case of ⊤, the second argument to the recursion operation
-- specified an element of C which would serve as the target for
-- tt. Now in the case of ≡, we want to specify an element of R x y
-- which would be the target of refl. This requires two adjustments:
-- first the second argument of type (R x y) makes no sense in general
-- as we don't want to insist that the relation R is universal (i.e.,
-- holds between arbitrary x and y). Second we must insist that the
-- relation R is reflexive.

rec≡ : {A : Set} →
       (R : A → A → Set) {reflexiveR : {a : A} → R a a} →
       ({x y : A} (p : x ≡ y) → R x y)
rec≡ R {reflR} (refl y) = reflR {y}

-- A special case of reflexive relations on A is the class of
-- functions from C a -> C a for some predicate C. Let's specialize
-- the above recursion principle to this special case.

rec≡S : {A : Set} {C : A → Set} →
        ({x y : A} (p : x ≡ y) → C x → C y)
rec≡S {C = C} p = rec≡ (λ a b → C a → C b) {id} p

-- Or we can prove the specialized version directly (rename to subst)

subst : {A : Set} {C : A → Set} →
        ({x y : A} (p : x ≡ y) → C x → C y)
subst {x = x} {y = .x} (refl .x) = id

-- So the recursion principle for the identity type says
-- equals may be substituted for equals OR
-- indiscernability of identicals OR
-- every type family respects equality

-- Examples:

private

  ex₁ : ∀ {n} → (p : n + 0 ≡ n) → (n + 0 > 0) → (n > 0)
  ex₁ {n} p = subst {C = λ m → m > 0} {n + 0} {n} p

  ex₂ : ∀ {A n} → (p : n + 0 ≡ n) → (Vec A (n + 0)) → (Vec A n)
  ex₂ {A} {n} p = subst {C = λ m → Vec A m} {n + 0} {n} p

  {--

  From Data.Nat library:

  data _≤_ : Rel ℕ Level.zero where
    z≤n : ∀ {n}                 → zero  ≤ n
    s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

  --}

  ≤-reflexive : {a : ℕ} → a ≤ a
  ≤-reflexive {zero} = z≤n
  ≤-reflexive {suc a} = s≤s (≤-reflexive {a})

  ex₃ : ∀ {n} → (p : n + 0 ≡ n) → (n + 0 ≤ n)
  ex₃ {n} = rec≡ {ℕ} (_≤_) {≤-reflexive} {n + 0} {n}

------------------------------------------------------------------------------
-- Now let's look at the induction principle for identity types

-- Our usual idiom is to use the same code for the recursion principle
-- and just make the eliminator a dependent function

-- Let's look at rec≡ again

-- rec≡ : {A : Set} →
--        (R : A → A → Set) {reflexiveR : {a : A} → R a a} →
--        ({x y : A} (p : x ≡ y) → R x y)
-- rec≡ R {reflR} (refl y) = reflR {y}

-- The relation R is already dependent on x and y; we just need to
-- make it dependent on p too

ind≡ : {A : Set} →
       (R : (x : A) → (y : A) → (p : x ≡ y) → Set)
       {reflexiveR : {a : A} → R a a (refl a)} →
       ({x y : A} (p : x ≡ y) → R x y p)
ind≡ R {reflR} (refl y) = reflR {y}

-- Changing some implicit argument to being explicit and vice-versa,
-- and changing names of bound variables we get:

J : {A : Set} →
    (R : {x y : A} → (p : x ≡ y) → Set)
    (r : (a : A) → R (refl a)) →
    ({a b : A} (p : a ≡ b) → R p)
J R r (refl y) = r y

-- Examples

sym : {A : Set} {x y : A} → (x ≡ y) → (y ≡ x)
sym = J (λ {x} {y} p → y ≡ x) (λ a → refl a)

-- Next we want to prove:
-- trans : {A : Set} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
-- if we try to directly use J we discover that the definition of R
-- (λ {x} {y} p → y ≡ z → x ≡ z)
-- refers to an unbound z

trans' : {A : Set} {x y : A} → (x ≡ y) → ((z : A) → (q : y ≡ z) → (x ≡ z))
trans' {A} =
  J (λ {x} {y} p → ((z : A) → (q : y ≡ z) → (x ≡ z)))
    (λ a z → id)

-- then

trans : {A : Set} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
trans {A} {x} {y} {z} p q = trans' {A} {x} {y} p z q

-- trans' refl q will simplify to q because we did induction on the first argument

idR : {A : Set} {x y : A} (q : x ≡ y) → trans (refl x) q ≡ q
idR q = refl q

-- but trans' p refl will NOT simplify

-- idL : {A : Set} {x y : A} (p : x ≡ y) → trans p (refl y) ≡ p
-- idL p = refl p -- does not work

-- We can do induction on the right and get the reverse situation
-- OR we can do induction twice and lose BOTH and ONLY get
-- trans refl refl = refl
-- Even though this seems "worse", it is symmetric at least and easy to work is.

trans2' : {A : Set} {x y : A} → (x ≡ y) → ((z : A) → (q : y ≡ z) → (x ≡ z))
trans2' {A} =
  J (λ {x} {y} p → ((z : A) → (q : y ≡ z) → (x ≡ z)))
    (λ a z → J (λ {x'} {y'} q → x' ≡ y') (λ b → refl b))

trans2 : {A : Set} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
trans2 {A} {x} {y} {z} p q = trans2' {A} {x} {y} p z q

idLR : {A : Set} {a : A} → trans2 (refl a) (refl a) ≡ refl a
idLR {A} {a} = refl (refl a)

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

-- If we restrict ourselves to proofs about "points" like numbers,
-- booleans, etc. all we are saying is that if we normalize the
-- calculation for each point they each reduce to same identical
-- result. Things get much more interesting if we start thinking about
-- identity in higher universes... So for example, say we want to
-- prove that groups are the same, in that case we might have to prove
-- that two types are the same etc. Unfortunately J by itself is
-- helpless here... This motivates the univalence axiom to be discussed next...

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

max_stars_repo_name: andmkent/misc-HoTT

max_issues_repo_name: andmkent/misc-HoTT

max_forks_repo_name: andmkent/misc-HoTT


text:
module automaton where

open import Data.Nat
open import Data.List
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import logic

record Automaton ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
        δ : Q → Σ → Q
        aend : Q → Bool

open Automaton

accept : { Q : Set } { Σ : Set  }
    → Automaton Q  Σ
    → Q
    → List  Σ → Bool
accept M q [] = aend M q
accept M q ( H  ∷ T ) = accept M ( δ M q H ) T

moves : { Q : Set } { Σ : Set  }
    → Automaton Q  Σ
    → Q → List  Σ → Q
moves M q [] = q
moves M q ( H  ∷ T ) = moves M ( δ M q H)  T

trace : { Q : Set } { Σ : Set  }
    → Automaton Q  Σ
    → Q → List  Σ → List Q
trace {Q} { Σ} M q [] = q ∷ []
trace {Q} { Σ} M q ( H  ∷ T ) = q ∷ trace M ( (δ M) q H ) T

reachable : { Q : Set } { Σ : Set  }
    → (M : Automaton Q  Σ  )
    → (astart q : Q )
    → (L : List  Σ ) → Set
reachable M astart q L = moves M astart  L ≡ q

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- All library modules, along with short descriptions
------------------------------------------------------------------------

-- Note that core modules are not included.

module Everything where

-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
open import Algebra

-- Solver for equations in commutative monoids
open import Algebra.CommutativeMonoidSolver

-- An example of how Algebra.CommutativeMonoidSolver can be used
open import Algebra.CommutativeMonoidSolver.Example

-- Properties of functions, such as associativity and commutativity
open import Algebra.FunctionProperties

-- Relations between properties of functions, such as associativity and
-- commutativity
open import Algebra.FunctionProperties.Consequences

-- Solver for equations in commutative monoids
open import Algebra.IdempotentCommutativeMonoidSolver

-- An example of how Algebra.IdempotentCommutativeMonoidSolver can be
-- used
open import Algebra.IdempotentCommutativeMonoidSolver.Example

-- Solver for monoid equalities
open import Algebra.Monoid-solver

-- Morphisms between algebraic structures
open import Algebra.Morphism

-- Some defined operations (multiplication by natural number and
-- exponentiation)
open import Algebra.Operations

-- Some derivable properties
open import Algebra.Properties.AbelianGroup

-- Some derivable properties
open import Algebra.Properties.BooleanAlgebra

-- Boolean algebra expressions
open import Algebra.Properties.BooleanAlgebra.Expression

-- Some derivable properties
open import Algebra.Properties.DistributiveLattice

-- Some derivable properties
open import Algebra.Properties.Group

-- Some derivable properties
open import Algebra.Properties.Lattice

-- Some derivable properties
open import Algebra.Properties.Ring

-- Solver for commutative ring or semiring equalities
open import Algebra.RingSolver

-- Commutative semirings with some additional structure ("almost"
-- commutative rings), used by the ring solver
open import Algebra.RingSolver.AlmostCommutativeRing

-- Some boring lemmas used by the ring solver
open import Algebra.RingSolver.Lemmas

-- Instantiates the ring solver, using the natural numbers as the
-- coefficient "ring"
open import Algebra.RingSolver.Natural-coefficients

-- Instantiates the ring solver with two copies of the same ring with
-- decidable equality
open import Algebra.RingSolver.Simple

-- Some algebraic structures (not packed up with sets, operations,
-- etc.)
open import Algebra.Structures

-- Applicative functors
open import Category.Applicative

-- Indexed applicative functors
open import Category.Applicative.Indexed

-- Applicative functors on indexed sets (predicates)
open import Category.Applicative.Predicate

-- Functors
open import Category.Functor

-- The identity functor
open import Category.Functor.Identity

-- Functors on indexed sets (predicates)
open import Category.Functor.Predicate

-- Monads
open import Category.Monad

-- A delimited continuation monad
open import Category.Monad.Continuation

-- The identity monad
open import Category.Monad.Identity

-- Indexed monads
open import Category.Monad.Indexed

-- The partiality monad
open import Category.Monad.Partiality

-- An All predicate for the partiality monad
open import Category.Monad.Partiality.All

-- Monads on indexed sets (predicates)
open import Category.Monad.Predicate

-- The state monad
open import Category.Monad.State

-- Basic types related to coinduction
open import Coinduction

-- AVL trees
open import Data.AVL

-- Types and functions which are used to keep track of height
-- invariants in AVL Trees
open import Data.AVL.Height

-- Indexed AVL trees
open import Data.AVL.Indexed

-- Finite maps with indexed keys and values, based on AVL trees
open import Data.AVL.IndexedMap

-- Keys for AVL trees
-- The key type extended with a new minimum and maximum.
open import Data.AVL.Key

-- Finite sets, based on AVL trees
open import Data.AVL.Sets

-- A binary representation of natural numbers
open import Data.Bin

-- Properties of the binary representation of natural numbers
open import Data.Bin.Properties

-- Booleans
open import Data.Bool

-- The type for booleans and some operations
open import Data.Bool.Base

-- A bunch of properties
open import Data.Bool.Properties

-- Showing booleans
open import Data.Bool.Show

-- Bounded vectors
open import Data.BoundedVec

-- Bounded vectors (inefficient, concrete implementation)
open import Data.BoundedVec.Inefficient

-- Characters
open import Data.Char

-- Basic definitions for Characters
open import Data.Char.Base

-- "Finite" sets indexed on coinductive "natural" numbers
open import Data.Cofin

-- Coinductive lists
open import Data.Colist

-- Infinite merge operation for coinductive lists
open import Data.Colist.Infinite-merge

-- Coinductive "natural" numbers
open import Data.Conat

-- Containers, based on the work of Abbott and others
open import Data.Container

-- Properties related to ◇
open import Data.Container.Any

-- Container combinators
open import Data.Container.Combinator

-- The free monad construction on containers
open import Data.Container.FreeMonad

-- Indexed containers aka interaction structures aka polynomial
-- functors. The notation and presentation here is closest to that of
-- Hancock and Hyvernat in "Programming interfaces and basic topology"
-- (2006/9).
open import Data.Container.Indexed

-- Indexed container combinators
open import Data.Container.Indexed.Combinator

-- The free monad construction on indexed containers
open import Data.Container.Indexed.FreeMonad

-- Coinductive vectors
open import Data.Covec

-- Lists with fast append
open import Data.DifferenceList

-- Natural numbers with fast addition (for use together with
-- DifferenceVec)
open import Data.DifferenceNat

-- Vectors with fast append
open import Data.DifferenceVec

-- Digits and digit expansions
open import Data.Digit

-- Empty type
open import Data.Empty

-- An irrelevant version of ⊥-elim
open import Data.Empty.Irrelevant

-- Finite sets
open import Data.Fin

-- Decision procedures for finite sets and subsets of finite sets
open import Data.Fin.Dec

-- Properties related to Fin, and operations making use of these
-- properties (or other properties not available in Data.Fin)
open import Data.Fin.Properties

-- Subsets of finite sets
open import Data.Fin.Subset

-- Some properties about subsets
open import Data.Fin.Subset.Properties

-- Substitutions
open import Data.Fin.Substitution

-- An example of how Data.Fin.Substitution can be used: a definition
-- of substitution for the untyped λ-calculus, along with some lemmas
open import Data.Fin.Substitution.Example

-- Substitution lemmas
open import Data.Fin.Substitution.Lemmas

-- Application of substitutions to lists, along with various lemmas
open import Data.Fin.Substitution.List

-- Floats
open import Data.Float

-- Directed acyclic multigraphs
open import Data.Graph.Acyclic

-- Integers
open import Data.Integer

-- Properties related to addition of integers
open import Data.Integer.Addition.Properties

-- Integers, basic types and operations
open import Data.Integer.Base

-- Divisibility and coprimality
open import Data.Integer.Divisibility

-- Properties related to multiplication of integers
open import Data.Integer.Multiplication.Properties

-- Some properties about integers
open import Data.Integer.Properties

-- Lists
open import Data.List

-- Lists where all elements satisfy a given property
open import Data.List.All

-- Properties related to All
open import Data.List.All.Properties

-- Lists where at least one element satisfies a given property
open import Data.List.Any

-- Properties related to bag and set equality
open import Data.List.Any.BagAndSetEquality

-- List membership and some related definitions
open import Data.List.Any.Membership

-- Properties related to propositional list membership
open import Data.List.Any.Membership.Properties

-- Data.List.Any.Membership instantiated with propositional equality,
-- along with some additional definitions.
open import Data.List.Any.Membership.Propositional

-- Properties related to propositional list membership
open import Data.List.Any.Membership.Propositional.Properties

-- Properties related to Any
open import Data.List.Any.Properties

-- Lists, basic types and operations
open import Data.List.Base

-- A categorical view of List
open import Data.List.Categorical

-- A data structure which keeps track of an upper bound on the number
-- of elements /not/ in a given list
open import Data.List.Countdown

-- Non-empty lists
open import Data.List.NonEmpty

-- Properties of non-empty lists
open import Data.List.NonEmpty.Properties

-- List-related properties
open import Data.List.Properties

-- Lexicographic ordering of lists
open import Data.List.Relation.NonStrictLex

-- Pointwise lifting of relations to lists
open import Data.List.Relation.Pointwise

-- Lexicographic ordering of lists
open import Data.List.Relation.StrictLex

-- Reverse view
open import Data.List.Reverse

-- M-types (the dual of W-types)
open import Data.M

-- Indexed M-types (the dual of indexed W-types aka Petersson-Synek
-- trees).
open import Data.M.Indexed

-- The Maybe type
open import Data.Maybe

-- The Maybe type and some operations
open import Data.Maybe.Base

-- Natural numbers
open import Data.Nat

-- Natural numbers, basic types and operations
open import Data.Nat.Base

-- Coprimality
open import Data.Nat.Coprimality

-- Integer division
open import Data.Nat.DivMod

-- Divisibility
open import Data.Nat.Divisibility

-- Greatest common divisor
open import Data.Nat.GCD

-- Boring lemmas used in Data.Nat.GCD and Data.Nat.Coprimality
open import Data.Nat.GCD.Lemmas

-- A generalisation of the arithmetic operations
open import Data.Nat.GeneralisedArithmetic

-- Definition of and lemmas related to "true infinitely often"
open import Data.Nat.InfinitelyOften

-- Least common multiple
open import Data.Nat.LCM

-- Primality
open import Data.Nat.Primality

-- A bunch of properties about natural number operations
open import Data.Nat.Properties

-- A bunch of properties about natural number operations
open import Data.Nat.Properties.Simple

-- Showing natural numbers
open import Data.Nat.Show

-- Transitive closures
open import Data.Plus

-- Products
open import Data.Product

-- N-ary products
open import Data.Product.N-ary

-- Properties of products
open import Data.Product.Properties

-- Lexicographic products of binary relations
open import Data.Product.Relation.NonStrictLex

-- Pointwise products of binary relations
open import Data.Product.Relation.Pointwise

-- Pointwise lifting of binary relations to sigma types
open import Data.Product.Relation.SigmaPointwise

-- Lexicographic products of binary relations
open import Data.Product.Relation.StrictLex

-- Rational numbers
open import Data.Rational

-- Properties of Rational numbers
open import Data.Rational.Properties

-- Reflexive closures
open import Data.ReflexiveClosure

-- Signs
open import Data.Sign

-- Some properties about signs
open import Data.Sign.Properties

-- The reflexive transitive closures of McBride, Norell and Jansson
open import Data.Star

-- Bounded vectors (inefficient implementation)
open import Data.Star.BoundedVec

-- Decorated star-lists
open import Data.Star.Decoration

-- Environments (heterogeneous collections)
open import Data.Star.Environment

-- Finite sets defined in terms of Data.Star
open import Data.Star.Fin

-- Lists defined in terms of Data.Star
open import Data.Star.List

-- Natural numbers defined in terms of Data.Star
open import Data.Star.Nat

-- Pointers into star-lists
open import Data.Star.Pointer

-- Some properties related to Data.Star
open import Data.Star.Properties

-- Vectors defined in terms of Data.Star
open import Data.Star.Vec

-- Streams
open import Data.Stream

-- Strings
open import Data.String

-- Strings
open import Data.String.Base

-- Sums (disjoint unions)
open import Data.Sum

-- Properties of sums (disjoint unions)
open import Data.Sum.Properties

-- Sums of binary relations
open import Data.Sum.Relation.General

-- Fixed-size tables of values, implemented as functions from 'Fin n'.
-- Similar to 'Data.Vec', but focusing on ease of retrieval instead of
-- ease of adding and removing elements.
open import Data.Table

-- Tables, basic types and operations
open import Data.Table.Base

-- Table-related properties
open import Data.Table.Properties

-- Pointwise table equality
open import Data.Table.Relation.Equality

-- Some unit types
open import Data.Unit

-- The unit type and the total relation on unit
open import Data.Unit.Base

-- Some unit types
open import Data.Unit.NonEta

-- Vectors
open import Data.Vec

-- Vectors where all elements satisfy a given property
open import Data.Vec.All

-- Properties related to All
open import Data.Vec.All.Properties

-- A categorical view of Vec
open import Data.Vec.Categorical

-- Code for converting Vec A n → B to and from n-ary functions
open import Data.Vec.N-ary

-- Some Vec-related properties
open import Data.Vec.Properties

-- Semi-heterogeneous vector equality
open import Data.Vec.Relation.Equality

-- Extensional pointwise lifting of relations to vectors
open import Data.Vec.Relation.ExtensionalPointwise

-- Inductive pointwise lifting of relations to vectors
open import Data.Vec.Relation.InductivePointwise

-- W-types
open import Data.W

-- Indexed W-types aka Petersson-Synek trees
open import Data.W.Indexed

-- Machine words
open import Data.Word

-- Type(s) used (only) when calling out to Haskell via the FFI
open import Foreign.Haskell

-- Simple combinators working solely on and with functions
open import Function

-- Bijections
open import Function.Bijection

-- Function setoids and related constructions
open import Function.Equality

-- Equivalence (coinhabitance)
open import Function.Equivalence

-- Injections
open import Function.Injection

-- Inverses
open import Function.Inverse

-- Left inverses
open import Function.LeftInverse

-- A universe which includes several kinds of "relatedness" for sets,
-- such as equivalences, surjections and bijections
open import Function.Related

-- Basic lemmas showing that various types are related (isomorphic or
-- equivalent or…)
open import Function.Related.TypeIsomorphisms

-- Surjections
open import Function.Surjection

-- IO
open import IO

-- Primitive IO: simple bindings to Haskell types and functions
open import IO.Primitive

-- An abstraction of various forms of recursion/induction
open import Induction

-- Lexicographic induction
open import Induction.Lexicographic

-- Various forms of induction for natural numbers
open import Induction.Nat

-- Well-founded induction
open import Induction.WellFounded

-- Universe levels
open import Level

-- Record types with manifest fields and "with", based on Randy
-- Pollack's "Dependently Typed Records in Type Theory"
open import Record

-- Support for reflection
open import Reflection

-- Properties of homogeneous binary relations
open import Relation.Binary

-- Some properties imply others
open import Relation.Binary.Consequences

-- Convenient syntax for equational reasoning
open import Relation.Binary.EqReasoning

-- Equivalence closures of binary relations
open import Relation.Binary.EquivalenceClosure

-- Many properties which hold for _∼_ also hold for flip _∼_
open import Relation.Binary.Flip

-- Heterogeneous equality
open import Relation.Binary.HeterogeneousEquality

-- Quotients for Heterogeneous equality
open import Relation.Binary.HeterogeneousEquality.Quotients

-- Example of a Quotient: ℤ as (ℕ × ℕ / ~)
open import Relation.Binary.HeterogeneousEquality.Quotients.Examples

-- Indexed binary relations
open import Relation.Binary.Indexed

-- Induced preorders
open import Relation.Binary.InducedPreorders

-- Order-theoretic lattices
open import Relation.Binary.Lattice

-- Lexicographic ordering of lists
open import Relation.Binary.List.NonStrictLex

-- Pointwise lifting of relations to lists
open import Relation.Binary.List.Pointwise

-- Lexicographic ordering of lists
open import Relation.Binary.List.StrictLex

-- Conversion of ≤ to <, along with a number of properties
open import Relation.Binary.NonStrictToStrict

-- Many properties which hold for _∼_ also hold for _∼_ on f
open import Relation.Binary.On

-- Order morphisms
open import Relation.Binary.OrderMorphism

-- Convenient syntax for "equational reasoning" using a partial order
open import Relation.Binary.PartialOrderReasoning

-- Convenient syntax for "equational reasoning" using a preorder
open import Relation.Binary.PreorderReasoning

-- Lexicographic products of binary relations
open import Relation.Binary.Product.NonStrictLex

-- Pointwise products of binary relations
open import Relation.Binary.Product.Pointwise

-- Lexicographic products of binary relations
open import Relation.Binary.Product.StrictLex

-- Properties satisfied by bounded join semilattices
open import Relation.Binary.Properties.BoundedJoinSemilattice

-- Properties satisfied by bounded meet semilattices
open import Relation.Binary.Properties.BoundedMeetSemilattice

-- Properties satisfied by decidable total orders
open import Relation.Binary.Properties.DecTotalOrder

-- Properties satisfied by join semilattices
open import Relation.Binary.Properties.JoinSemilattice

-- Properties satisfied by lattices
open import Relation.Binary.Properties.Lattice

-- Properties satisfied by meet semilattices
open import Relation.Binary.Properties.MeetSemilattice

-- Properties satisfied by posets
open import Relation.Binary.Properties.Poset

-- Properties satisfied by preorders
open import Relation.Binary.Properties.Preorder

-- Properties satisfied by strict partial orders
open import Relation.Binary.Properties.StrictPartialOrder

-- Properties satisfied by strict partial orders
open import Relation.Binary.Properties.StrictTotalOrder

-- Properties satisfied by total orders
open import Relation.Binary.Properties.TotalOrder

-- Propositional (intensional) equality
open import Relation.Binary.PropositionalEquality

-- An equality postulate which evaluates
open import Relation.Binary.PropositionalEquality.TrustMe

-- Helpers intended to ease the development of "tactics" which use
-- proof by reflection
open import Relation.Binary.Reflection

-- Convenient syntax for "equational reasoning" in multiple Setoids
open import Relation.Binary.SetoidReasoning

-- Pointwise lifting of binary relations to sigma types
open import Relation.Binary.Sigma.Pointwise

-- Some simple binary relations
open import Relation.Binary.Simple

-- Convenient syntax for "equational reasoning" using a strict partial
-- order
open import Relation.Binary.StrictPartialOrderReasoning

-- Conversion of < to ≤, along with a number of properties
open import Relation.Binary.StrictToNonStrict

-- Sums of binary relations
open import Relation.Binary.Sum

-- Symmetric closures of binary relations
open import Relation.Binary.SymmetricClosure

-- Pointwise lifting of relations to vectors
open import Relation.Binary.Vec.Pointwise

-- Operations on nullary relations (like negation and decidability)
open import Relation.Nullary

-- Operations on and properties of decidable relations
open import Relation.Nullary.Decidable

-- Implications of nullary relations
open import Relation.Nullary.Implication

-- Properties related to negation
open import Relation.Nullary.Negation

-- Products of nullary relations
open import Relation.Nullary.Product

-- Sums of nullary relations
open import Relation.Nullary.Sum

-- A universe of proposition functors, along with some properties
open import Relation.Nullary.Universe

-- Unary relations
open import Relation.Unary

-- Predicate transformers
open import Relation.Unary.PredicateTransformer

-- Sizes for Agda's sized types
open import Size

-- Strictness combinators
open import Strict

-- Universes
open import Universe