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

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Fiberwise
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients.Base
open import Cubical.HITs.PropositionalTruncation.Base

private
  variable
    ℓA ℓ≅A ℓA' ℓ≅A' : Level

Rel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
Rel A B ℓ' = A → B → Type ℓ'

PropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
PropRel A B ℓ' = Σ[ R ∈ Rel A B ℓ' ] ∀ a b → isProp (R a b)

idPropRel : ∀ {ℓ} (A : Type ℓ) → PropRel A A ℓ
idPropRel A .fst a a' = ∥ a ≡ a' ∥
idPropRel A .snd _ _ = squash

invPropRel : ∀ {ℓ ℓ'} {A B : Type ℓ}
  → PropRel A B ℓ' → PropRel B A ℓ'
invPropRel R .fst b a = R .fst a b
invPropRel R .snd b a = R .snd a b

compPropRel : ∀ {ℓ ℓ' ℓ''} {A B C : Type ℓ}
  → PropRel A B ℓ' → PropRel B C ℓ'' → PropRel A C (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
compPropRel R S .fst a c = ∥ Σ[ b ∈ _ ] (R .fst a b × S .fst b c) ∥
compPropRel R S .snd _ _ = squash

graphRel : ∀ {ℓ} {A B : Type ℓ} → (A → B) → Rel A B ℓ
graphRel f a b = f a ≡ b

module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
  isRefl : Type (ℓ-max ℓ ℓ')
  isRefl = (a : A) → R a a

  isSym : Type (ℓ-max ℓ ℓ')
  isSym = (a b : A) → R a b → R b a

  isTrans : Type (ℓ-max ℓ ℓ')
  isTrans = (a b c : A)  → R a b → R b c → R a c

  record isEquivRel : Type (ℓ-max ℓ ℓ') where
    constructor equivRel
    field
      reflexive : isRefl
      symmetric : isSym
      transitive : isTrans

  isPropValued : Type (ℓ-max ℓ ℓ')
  isPropValued = (a b : A) → isProp (R a b)

  isEffective : Type (ℓ-max ℓ ℓ')
  isEffective =
    (a b : A) → isEquiv (eq/ {R = R} a b)

  impliesIdentity : Type _
  impliesIdentity = {a a' : A} → (R a a') → (a ≡ a')

  -- the total space corresponding to the binary relation w.r.t. a
  relSinglAt : (a : A) → Type (ℓ-max ℓ ℓ')
  relSinglAt a = Σ[ a' ∈ A ] (R a a')

  -- the statement that the total space is contractible at any a
  contrRelSingl : Type (ℓ-max ℓ ℓ')
  contrRelSingl = (a : A) → isContr (relSinglAt a)

  isUnivalent : Type (ℓ-max ℓ ℓ')
  isUnivalent = (a a' : A) → (R a a') ≃ (a ≡ a')

  contrRelSingl→isUnivalent : isRefl → contrRelSingl → isUnivalent
  contrRelSingl→isUnivalent ρ c a a' = isoToEquiv i
    where
      h : isProp (relSinglAt a)
      h = isContr→isProp (c a)
      aρa : relSinglAt a
      aρa = a , ρ a
      Q : (y : A) → a ≡ y → _
      Q y _ = R a y
      i : Iso (R a a') (a ≡ a')
      Iso.fun i r = cong fst (h aρa (a' , r))
      Iso.inv i = J Q (ρ a)
      Iso.rightInv i = J (λ y p → cong fst (h aρa (y , J Q (ρ a) p)) ≡ p)
                         (J (λ q _ → cong fst (h aρa (a , q)) ≡ refl)
                           (J (λ α _ → cong fst α ≡ refl) refl
                             (isContr→isProp (isProp→isContrPath h aρa aρa) refl (h aρa aρa)))
                           (sym (JRefl Q (ρ a))))
      Iso.leftInv i r = J (λ w β → J Q (ρ a) (cong fst β) ≡ snd w)
                          (JRefl Q (ρ a)) (h aρa (a' , r))

  isUnivalent→contrRelSingl : isUnivalent → contrRelSingl
  isUnivalent→contrRelSingl u a = q
    where
      abstract
        f : (x : A) → a ≡ x → R a x
        f x p = invEq (u a x) p

        t : singl a → relSinglAt a
        t (x , p) = x , f x p

        q : isContr (relSinglAt a)
        q = isOfHLevelRespectEquiv 0 (t , totalEquiv _ _ f λ x → invEquiv (u a x) .snd)
                                   (isContrSingl a)

EquivRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
EquivRel A ℓ' = Σ[ R ∈ Rel A A ℓ' ] BinaryRelation.isEquivRel R

EquivPropRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
EquivPropRel A ℓ' = Σ[ R ∈ PropRel A A ℓ' ] BinaryRelation.isEquivRel (R .fst)

record RelIso {A : Type ℓA} (_≅_ : Rel A A ℓ≅A)
              {A' : Type ℓA'} (_≅'_ : Rel A' A' ℓ≅A') : Type (ℓ-max (ℓ-max ℓA ℓA') (ℓ-max ℓ≅A ℓ≅A')) where
  constructor reliso
  field
    fun : A → A'
    inv : A' → A
    rightInv : (a' : A') → fun (inv a') ≅' a'
    leftInv : (a : A) → inv (fun a) ≅ a

open BinaryRelation

RelIso→Iso : {A : Type ℓA} {A' : Type ℓA'}
             (_≅_ : Rel A A ℓ≅A) (_≅'_ : Rel A' A' ℓ≅A')
             (uni : impliesIdentity _≅_) (uni' : impliesIdentity _≅'_)
             (f : RelIso _≅_ _≅'_)
             → Iso A A'
Iso.fun (RelIso→Iso _ _ _ _ f) = RelIso.fun f
Iso.inv (RelIso→Iso _ _ _ _ f) = RelIso.inv f
Iso.rightInv (RelIso→Iso _ _ uni uni' f) a'
  = uni' (RelIso.rightInv f a')
Iso.leftInv (RelIso→Iso _ _ uni uni' f) a
  = uni (RelIso.leftInv f a)


text:
module Thesis.SIRelBigStep.Types where

open import Data.Empty
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary hiding (_⇒_)

data Type : Set where
  _⇒_ : (σ τ : Type) → Type
  pair : (σ τ : Type) → Type
  nat : Type
infixr 20 _⇒_

open import Base.Syntax.Context Type public
open import Base.Syntax.Vars Type public

-- Decidable equivalence for types and contexts. Needed later for ⊕ on closures.

⇒-inj : ∀ {τ1 τ2 τ3 τ4 : Type} → _≡_ {A = Type} (τ1 ⇒ τ2) (τ3 ⇒ τ4) → τ1 ≡ τ3 × τ2 ≡ τ4
⇒-inj refl = refl , refl

pair-inj : ∀ {τ1 τ2 τ3 τ4 : Type} → _≡_ {A = Type} (pair τ1 τ2) (pair τ3 τ4) → τ1 ≡ τ3 × τ2 ≡ τ4
pair-inj refl = refl , refl

_≟Type_ : (τ1 τ2 : Type) → Dec (τ1 ≡ τ2)
(τ1 ⇒ τ2) ≟Type (τ3 ⇒ τ4) with τ1 ≟Type τ3 | τ2 ≟Type τ4
(τ1 ⇒ τ2) ≟Type (.τ1 ⇒ .τ2) | yes refl | yes refl = yes refl
(τ1 ⇒ τ2) ≟Type (.τ1 ⇒ τ4) | yes refl | no ¬q = no (λ x → ¬q (proj₂ (⇒-inj x)))
(τ1 ⇒ τ2) ≟Type (τ3 ⇒ τ4) | no ¬p | q = no (λ x → ¬p (proj₁ (⇒-inj x)))
(τ1 ⇒ τ2) ≟Type pair τ3 τ4 = no (λ ())
(τ1 ⇒ τ2) ≟Type nat = no (λ ())
pair τ1 τ2 ≟Type (τ3 ⇒ τ4) = no (λ ())
pair τ1 τ2 ≟Type pair τ3 τ4 with τ1 ≟Type τ3 | τ2 ≟Type τ4
pair τ1 τ2 ≟Type pair .τ1 .τ2 | yes refl | yes refl = yes refl
pair τ1 τ2 ≟Type pair τ3 τ4 | yes p | no ¬q = no (λ x → ¬q (proj₂ (pair-inj x)))
pair τ1 τ2 ≟Type pair τ3 τ4 | no ¬p | q = no (λ x → ¬p (proj₁ (pair-inj x)))
pair τ1 τ2 ≟Type nat = no (λ ())
nat ≟Type pair τ1 τ2 = no (λ ())
nat ≟Type (τ1 ⇒ τ2) = no (λ ())
nat ≟Type nat = yes refl

•-inj : ∀ {τ1 τ2 : Type} {Γ1 Γ2 : Context} → _≡_ {A = Context} (τ1 • Γ1) (τ2 • Γ2) → τ1 ≡ τ2 × Γ1 ≡ Γ2
•-inj refl = refl , refl

_≟Ctx_ : (Γ1 Γ2 : Context) → Dec (Γ1 ≡ Γ2)
∅ ≟Ctx ∅ = yes refl
∅ ≟Ctx (τ2 • Γ2) = no (λ ())
(τ1 • Γ1) ≟Ctx ∅ = no (λ ())
(τ1 • Γ1) ≟Ctx (τ2 • Γ2) with τ1 ≟Type τ2 | Γ1 ≟Ctx Γ2
(τ1 • Γ1) ≟Ctx (.τ1 • .Γ1) | yes refl | yes refl = yes refl
(τ1 • Γ1) ≟Ctx (.τ1 • Γ2) | yes refl | no ¬q = no (λ x → ¬q (proj₂ (•-inj x)))
(τ1 • Γ1) ≟Ctx (τ2 • Γ2) | no ¬p | q = no (λ x → ¬p (proj₁ (•-inj x)))

≟Ctx-refl : ∀ Γ → Γ ≟Ctx Γ ≡ yes refl
≟Ctx-refl Γ with Γ ≟Ctx Γ
≟Ctx-refl Γ | yes refl = refl
≟Ctx-refl Γ | no ¬p = ⊥-elim (¬p refl)

ext: agda

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module MLib.Prelude where

open import MLib.Prelude.FromStdlib public

module Fin where
  open import MLib.Prelude.Fin public
open Fin using (Fin; zero; suc) hiding (module Fin) public


text:
open import Agda.Builtin.Nat

data Vec (A : Set) : Nat → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

infixr 5 _∷_ _++_

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

T : ∀ {A n} → Vec A n → Set
T [] = Nat
T (x ∷ xs) = Vec Nat 0

foo : ∀ {A} m n (xs : Vec A m) (ys : Vec A n) → T (xs ++ ys)
foo m n xs ys with {m + n} | xs ++ ys
... | []     = 0
... | z ∷ zs = []

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module HelloWorld where

open import Common.IO
open import Common.Unit

main : IO Unit
main = putStr "Hello World"


text:
open import Agda.Builtin.Equality

data D (A : Set) : Set where

{-# INJECTIVE D #-}

test : {A₁ A₂ : Set} → D A₁ ≡ D A₂ → A₁ ≡ A₂
test refl = refl

postulate f : Set → Set

{-# INJECTIVE f #-}

test₂ : {A₁ A₂ : Set} → f A₁ ≡ f A₂ → A₁ ≡ A₂
test₂ refl = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Avionics.Bool where

open import Data.Bool using (Bool; true; false; _∧_; T)
open import Data.Unit using (⊤; tt)
open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; inspect; [_])

--open import Avionics.Product using (_×_; ⟨_,_⟩)

--TODO: Replace with T⇔≡ from standard library
≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl = tt

T→≡ : ∀ {b : Bool} → T b → b ≡ true
T→≡ {true} tt = refl

T∧→× : ∀ {x y} → T (x ∧ y) → (T x) × (T y)
T∧→× {true} {true} tt = tt , tt
--TODO: Find a way to extract the function below from `T-∧` (standard library)
--T∧→× {x} {y} = ? -- Equivalence.to (T-∧ {x} {y})

×→T∧ : ∀ {x y} → (T x) × (T y) → T (x ∧ y)
×→T∧ {true} {true} (tt , tt) = tt

lem∧ : {a b : Bool} → a ∧ b ≡ true → a ≡ true × b ≡ true
lem∧ {true} {true} refl = refl , refl

∧≡true→×≡ : ∀ {A B : Set} {f : A → Bool} {g : B → Bool}
            (n : A) (m : B)
          → f n ∧ g m ≡ true
          → f n ≡ true × g m ≡ true
∧≡true→×≡ {f = f} {g = g} n m fn∧gm≡true = lem∧ {f n} {g m} fn∧gm≡true

max_stars_repo_name: RPI-WCL/safety-envelopes-sentinels

max_issues_repo_name: RPI-WCL/safety-envelopes-sentinels

max_forks_repo_name: RPI-WCL/safety-envelopes-sentinels


text:
{-# OPTIONS --universe-polymorphism #-}
open import Level
open import Categories.Category
module Categories.Power.Functorial {o ℓ e : Level} (C : Category o ℓ e) where

open import Relation.Binary.PropositionalEquality using (≡-irrelevance)
open import Data.Unit using (⊤; tt)
open import Function using () renaming (_∘_ to _∙_)
open import Relation.Binary using (module IsEquivalence)

open import Categories.Support.PropositionalEquality
import Categories.Power as Power
open Power C
open import Categories.Functor hiding (identityˡ) renaming (_≡_ to _≡F_; _∘_ to _∘F_; id to idF)
open import Categories.NaturalTransformation using (NaturalTransformation; module NaturalTransformation)
open import Categories.Discrete
open import Categories.Equivalence.Strong hiding (module Equiv)

open Category using (Obj)
open Category C using (_⇒_; _∘_; _≡_; module Equiv)
open import Categories.FunctorCategory
open import Categories.Lift
open import Categories.NaturalIsomorphism as NI using (NaturalIsomorphism; module NaturalIsomorphism)
open Functor using () renaming (F₀ to map₀; F₁ to map₁)
open NaturalTransformation using (η)

z : Level
z = o ⊔ ℓ ⊔ e

open import Categories.Categories using (Categories)
import Categories.Morphisms as M
open M (Categories z z e) using (_≅_)

exp→functor₀ : ∀ {I} → Obj (Exp I) → Functor (Discrete I) C
exp→functor₀ X =
  record
  { F₀ = X
  ; F₁ = my-F₁
  ; identity = Equiv.refl
  ; homomorphism = λ {_ _ _ A≣B B≣C} → my-homomorphism A≣B B≣C
  ; F-resp-≡ = λ {_ _ e1 e2} _ → Equiv.reflexive (≣-cong my-F₁ (≡-irrelevance e1 e2))
  }
  where
  my-F₁ : ∀ {A B} → (A ≣ B) → (X A ⇒ X B)
  my-F₁ ≣-refl = C.id
  .my-homomorphism : ∀ {A B C} (A≣B : A ≣ B) (B≣C : B ≣ C) → my-F₁ (≣-trans A≣B B≣C) ≡ my-F₁ B≣C ∘ my-F₁ A≣B
  my-homomorphism ≣-refl ≣-refl = Equiv.sym C.identityˡ

exp→functor₁ : ∀ {I} {X Y} → Exp I [ X , Y ] → NaturalTransformation (exp→functor₀ X) (exp→functor₀ Y)
exp→functor₁ {X = X} {Y} F = record { η = F; commute = my-commute }
  where
  .my-commute : ∀ {A B} (A≣B : A ≣ B) → F B ∘ map₁ (exp→functor₀ X) A≣B ≡ map₁ (exp→functor₀ Y) A≣B ∘ F A
  my-commute ≣-refl = Equiv.trans C.identityʳ (Equiv.sym C.identityˡ)

exp→functor : ∀ {I} → Functor (Exp I) (Functors (Discrete I) C)
exp→functor =
  record
  { F₀ = exp→functor₀
  ; F₁ = exp→functor₁
  ; identity = Equiv.refl
  ; homomorphism = Equiv.refl
  ; F-resp-≡ = λ eqs {x} → eqs x
  }

functor→exp : ∀ {I} → Functor (Functors (Discrete I) C) (Exp I)
functor→exp =
  record
  { F₀ = Functor.F₀
  ; F₁ = NaturalTransformation.η
  ; identity = λ _ → Equiv.refl
  ; homomorphism = λ _ → Equiv.refl
  ; F-resp-≡ = λ eqs i → eqs {i}
  }

semicanonical : ∀ {I} → (F : Functor (Discrete I) C) → F ≡F (exp→functor₀ (map₀ F))
semicanonical {I} F ≣-refl = ≡⇒∼ F.identity
  where
  module F = Functor F
  open Heterogeneous C

exp≋functor : ∀ {I} → StrongEquivalence (Exp I) (Functors (Discrete I) C)
exp≋functor {I} = record
  { F = exp→functor
  ; G = functor→exp
  ; weak-inverse = record
    { F∘G≅id = record
      { F⇒G = record
        { η = Sc.F⇐G
        ; commute = λ f → Equiv.trans C.identityˡ (Equiv.sym C.identityʳ)
        }
      ; F⇐G = record
        { η = Sc.F⇒G
        ; commute = λ f → Equiv.trans C.identityˡ (Equiv.sym C.identityʳ)
        }
      ; iso = λ X → record { isoˡ = C.identityˡ; isoʳ = C.identityˡ }
      }
    ; G∘F≅id = IsEquivalence.refl NI.equiv
    }
  }
  where
  FDIC = Functors (Discrete I) C
  module Sc (X : Obj FDIC) = NaturalIsomorphism (NI.≡→iso X (exp→functor₀ (map₀ X)) (semicanonical X))

exp≅functor : (ext : ∀ {a b} {A : Set a} {B : A → Set b} (f g : (x : A) → B x) → (∀ x → f x ≣ g x) → f ≣ g) → (id-propositionally-unique : (A : C.Obj) (f : A ⇒ A) → .(f ≡ C.id) → f ≣ C.id) → ∀ {I} → LiftC z z e (Exp I) ≅ Functors (Discrete I) C
exp≅functor ext id-propositionally-unique {I} =
  record
  { f = LiftFˡ exp→functor
  ; g = LiftFʳ functor→exp
  ; iso = record
    { isoˡ = λ f → Heterogeneous.refl _
    ; isoʳ = λ {A B} f → ir A B f
    }
  }
  where
  FDIC = Functors (Discrete I) C
  f∘g = LiftFˡ exp→functor ∘F LiftFʳ functor→exp

  squash : ∀ (A : Obj FDIC) → Obj FDIC
  squash A = exp→functor₀ (map₀ A)

  ≣-cong′ : ∀ {a b} {A : Set a} {B : Set b} {x y : A} (f : (z : A) → (y ≣ z) → B) → (eq : x ≣ y) → f x (≣-sym eq) ≣ f y ≣-refl
  ≣-cong′ f ≣-refl = ≣-refl

  squash-does-nothing : (A : Obj FDIC) → squash A ≣ A
  squash-does-nothing A = ≣-cong′ {B = Obj FDIC} (λ f eq → record {
                             F₀ = map₀ A;
                             F₁ = λ {i j : I} → f i j;
                             identity = λ {i} → ≣-subst (λ f → f i i ≣-refl ≡ C.id) eq (Functor.identity A {i});
                             homomorphism = λ {i j k i≣j j≣k} → ≣-subst (λ f → f i k (≣-trans i≣j j≣k) ≡ f j k j≣k ∘ f i j i≣j) eq (Functor.homomorphism A {f = i≣j} {j≣k});
                             F-resp-≡ = λ {i j ij ji} → ≣-subst (λ f → ⊤ → f i j ij ≡ f i j ji) eq (Functor.F-resp-≡ A {i} {j} {ij} {ji}) })
                    lemma₃
    where
    .lemma₁ : (i : I) (eq : i ≣ i) → map₁ A eq ≡ C.id
    lemma₁ i eq = Equiv.trans (Functor.F-resp-≡ A tt) (Functor.identity A)

    lemma₂ : (i j : I) (eq : i ≣ j) → map₁ (squash A) eq ≣ map₁ A eq
    lemma₂ i .i ≣-refl = ≣-sym (id-propositionally-unique (map₀ A i) (map₁ A ≣-refl) (lemma₁ i ≣-refl))

    lemma₃ : (λ (i j : I) → map₁ (squash A) {i} {j}) ≣ (λ (i j : I) → map₁ A {i} {j})
    lemma₃ = ext (λ (i j : I) → map₁ (squash A)) (λ (i j : I) → map₁ A)
      (λ (i : I) → ext (λ (j : I) → map₁ (squash A)) (λ (j : I) → map₁ A)
        (λ (j : I) → ext (map₁ (squash A)) (map₁ A) (lemma₂ i j)))

  ∼-subst : ∀ {o ℓ e} {C : Category o ℓ e} {A B A′ B′ : Obj C} (f : C [ A , B ]) (g : C [ A′ , B′ ]) (A′≣A : A′ ≣ A) (B′≣B : B′ ≣ B) → .(C [ ≣-subst (λ X → C [ X , B ]) A′≣A (≣-subst (λ Y → C [ A′ , Y ]) B′≣B g) ≡ f ]) → C [ g ∼ f ]
  ∼-subst {C = C} f g ≣-refl ≣-refl eq = ≡⇒∼ eq
    where open Heterogeneous C

  .∼-unsubst : ∀ {o ℓ e} {C : Category o ℓ e} {A B A′ B′ : Obj C} (f : C [ A , B ]) (g : C [ A′ , B′ ]) (A′≣A : A′ ≣ A) (B′≣B : B′ ≣ B) → C [ g ∼ f ] → C [ ≣-subst (λ X → C [ X , B ]) A′≣A (≣-subst (λ Y → C [ A′ , Y ]) B′≣B g) ≡ f ]
  ∼-unsubst f g ≣-refl ≣-refl (Heterogeneous.≡⇒∼ eq) = irr eq
    where open Heterogeneous C

  ≣-subst-irrel : ∀ {a p} {A : Set a} (P : A → Set p) {x y : A} → (eq₁ eq₂ : x ≣ y) → ∀ {it} → ≣-subst P eq₁ it ≣ ≣-subst P eq₂ it
  ≣-subst-irrel _ ≣-refl ≣-refl = ≣-refl

  ≣-subst-cong : ∀ {a a′ p} {A : Set a} {A′ : Set a′} (P′ : A′ → Set p) (f : A → A′) {x y : A} (eq : x ≣ y) → ∀ {it} → ≣-subst (P′ ∙ f) eq it ≣ ≣-subst P′ (≣-cong f eq) it
  ≣-subst-cong P′ f ≣-refl = ≣-refl

  ≣-subst-fatten : ∀ {a a′ p} {A : Set a} {A′ : Set a′} (P′ : A′ → Set p) (f : A → A′) {x y : A} (eq : x ≣ y) (eq′ : f x ≣ f y) → ∀ {it} → ≣-subst (P′ ∙ f) eq it ≣ ≣-subst P′ eq′ it
  ≣-subst-fatten P′ f eq eq′ = ≣-trans (≣-subst-cong P′ f eq) (≣-subst-irrel P′ (≣-cong f eq) eq′)

  η-under-substˡ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F F′ G : Functor C D} (α : NaturalTransformation F′ G) (F′≣F : F′ ≣ F) (c : Obj C) → η (≣-subst (λ H → NaturalTransformation H G) F′≣F α) c ≣ (≣-subst (λ (H : Functor C D) → D [ map₀ H c , map₀ G c ]) F′≣F (η α c))
  η-under-substˡ α ≣-refl c = ≣-refl

  η-under-substʳ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G G′ : Functor C D} (α : NaturalTransformation F G′) (G′≣G : G′ ≣ G) (c : Obj C) → η (≣-subst (λ H → NaturalTransformation F H) G′≣G α) c ≣ (≣-subst (λ (H : Functor C D) → D [ map₀ F c , map₀ H c ]) G′≣G (η α c))
  η-under-substʳ α ≣-refl c = ≣-refl

  .lemma : (A B : Obj FDIC) (f : FDIC [ A , B ]) (i : I) → C [ η (≣-subst (λ X → FDIC [ X , B ]) (squash-does-nothing A) (≣-subst (λ Y → FDIC [ squash A , Y ]) (squash-does-nothing B) (map₁ f∘g f))) i ≡ η f i ]
  lemma A B f i =
    let loc X = map₀ X i in
    let sqdnA = squash-does-nothing A in
    let sqdnB = squash-does-nothing B in
    let MESS = ≣-subst (λ Y → FDIC [ squash A , Y ]) sqdnB (map₁ f∘g f) in

    C.Equiv.reflexive (
      begin
        η (≣-subst (λ X → FDIC [ X , B ]) sqdnA MESS) i
      ≣⟨ η-under-substˡ MESS sqdnA i ⟩
        ≣-subst (λ X → C [ loc X , loc B ]) sqdnA (η MESS i)
      ≣⟨ ≣-subst-fatten (λ c → C [ c , loc B ]) loc sqdnA ≣-refl ⟩
        η (≣-subst (λ Y → FDIC [ squash A , Y ]) sqdnB (map₁ f∘g f)) i
      ≣⟨ η-under-substʳ (map₁ f∘g f) sqdnB i ⟩
        ≣-subst (λ Y → C [ loc A , loc Y ]) sqdnB (η (map₁ f∘g f) i)
      ≣⟨ ≣-subst-fatten (λ c → C [ loc A , c ]) loc sqdnB ≣-refl ⟩
        η f i
      ∎)
    where
    open ≣-reasoning

  ir : (A B : Obj FDIC) (f : FDIC [ A , B ]) → FDIC [ map₁ f∘g f ∼ f ]
  ir A B f = ∼-subst {C = FDIC} f (map₁ f∘g f) (squash-does-nothing A) (squash-does-nothing B) (λ {x} → lemma A B f x)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 16-sets where

import 15-number-theory
open 15-number-theory public

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
module examplesPaperJFP.ConsoleInterface where

open import examplesPaperJFP.NativeIOSafe
open import examplesPaperJFP.BasicIO hiding (main)

module _ where
  data ConsoleCommand : Set where
    getLine   :  ConsoleCommand
    putStrLn  :  String → ConsoleCommand

  ConsoleResponse : ConsoleCommand → Set
  ConsoleResponse  getLine      =  Maybe String
  ConsoleResponse (putStrLn s)  =  Unit

  ConsoleInterface : IOInterface
  Command   ConsoleInterface  =  ConsoleCommand
  Response  ConsoleInterface  =  ConsoleResponse

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
------------------------------------------------------------------------
-- A variant of the set quotients from Quotient
------------------------------------------------------------------------

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

-- Partly following the HoTT book.
--
-- Unlike the HoTT book, but following the cubical library (in which
-- set quotients were implemented by Zesen Qian and Anders Mörtberg),
-- the quotienting relations are not always required to be
-- propositional. Furthermore, unlike the code in the cubical library,
-- the set truncation constructor takes an argument stating that the
-- quotienting relation is propositional.

-- The module is parametrised by a notion of equality. The higher
-- constructors of the HIT defining quotients use path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

module Quotient.Set-truncated-if-propositional
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

private
  open module D = P.Derived-definitions-and-properties eq hiding (elim)

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Equivalence-relation equality-with-J
open import Function-universe equality-with-J as F hiding (_∘_; id)
open import H-level equality-with-J as H
import H-level P.equality-with-J as PH
open import H-level.Closure equality-with-J
import H-level.Truncation.Church equality-with-J as Trunc
open import H-level.Truncation.Propositional eq as TruncP
  using (∥_∥; ∣_∣; Surjective; Axiom-of-countable-choice)
open import Preimage equality-with-J using (_⁻¹_)
import Quotient eq as Quotient
import Quotient.Families-of-equivalence-classes equality-with-J as QF
open import Sum equality-with-J
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

private
  variable
    a a₁ a₂ b p     : Level
    k               : Isomorphism-kind
    A A₁ A₂ B       : Type a
    P               : A → Type p
    e f r r₁ r₂ x y : A
    R R₁ R₂         : A → A → Type r

------------------------------------------------------------------------
-- Quotients

-- The quotient type constructor.

infix 5 _/_

data _/_ (A : Type a) (R : A → A → Type r) : Type (a ⊔ r) where
  [_]                   : A → A / R
  []-respects-relationᴾ : R x y → [ x ] P.≡ [ y ]
  /-is-setᴾ             : (∀ x y → Is-proposition (R x y)) →
                          P.Is-set (A / R)

-- [_] respects the quotient relation.

[]-respects-relation : R x y → _≡_ {A = A / R} [ x ] [ y ]
[]-respects-relation = _↔_.from ≡↔≡ ∘ []-respects-relationᴾ

-- If R is pointwise propositional, then A / R is a set.

/-is-set : (∀ x y → Is-proposition (R x y)) → Is-set (A / R)
/-is-set = _↔_.from (H-level↔H-level 2) ∘ /-is-setᴾ

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

-- An eliminator, expressed using paths.

record Elimᴾ′ {A : Type a} {R : A → A → Type r} (P : A / R → Type p) :
              Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ : ∀ x → P [ x ]

    []-respects-relationʳ :
      (r : R x y) →
      P.[ (λ i → P ([]-respects-relationᴾ r i)) ] []ʳ x ≡ []ʳ y

    is-setʳ :
      (prop : ∀ x y → Is-proposition (R x y))
      {eq₁ eq₂ : x P.≡ y} {p : P x} {q : P y}
      (eq₃ : P.[ (λ i → P (eq₁ i)) ] p ≡ q)
      (eq₄ : P.[ (λ i → P (eq₂ i)) ] p ≡ q) →
      P.[ (λ i → P.[ (λ j → P (/-is-setᴾ prop eq₁ eq₂ i j)) ] p ≡ q) ]
        eq₃ ≡ eq₄

open Elimᴾ′ public

elimᴾ′ : Elimᴾ′ P → (x : A / R) → P x
elimᴾ′ {A = A} {R = R} {P = P} e = helper
  where
  module E = Elimᴾ′ e

  helper : (x : A / R) → P x
  helper [ x ]                       = E.[]ʳ x
  helper ([]-respects-relationᴾ r i) = E.[]-respects-relationʳ r i
  helper (/-is-setᴾ prop p q i j)    =
    E.is-setʳ prop (λ i → helper (p i)) (λ i → helper (q i)) i j

-- A possibly more useful eliminator, expressed using paths.

record Elimᴾ {A : Type a} {R : A → A → Type r} (P : A / R → Type p) :
             Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ : ∀ x → P [ x ]

    []-respects-relationʳ :
      (r : R x y) →
      P.[ (λ i → P ([]-respects-relationᴾ r i)) ] []ʳ x ≡ []ʳ y

    is-setʳ :
      (∀ x y → Is-proposition (R x y)) →
      ∀ x → P.Is-set (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : A / R) → P x
elimᴾ e = elimᴾ′ λ where
    .[]ʳ                   → E.[]ʳ
    .[]-respects-relationʳ → E.[]-respects-relationʳ
    .is-setʳ prop          → P.heterogeneous-UIP (E.is-setʳ prop) _
  where
  module E = Elimᴾ e

private

  -- One can define elimᴾ′ using elimᴾ.

  elimᴾ′₂ : Elimᴾ′ P → (x : A / R) → P x
  elimᴾ′₂ {P = P} e = elimᴾ λ where
      .[]ʳ                        → E.[]ʳ
      .[]-respects-relationʳ      → E.[]-respects-relationʳ
      .is-setʳ prop x {y} {z} p q →                                $⟨ E.is-setʳ prop p q ⟩
        P.[ (λ i →
               P.[ (λ j → P (/-is-setᴾ prop P.refl P.refl i j)) ]
                 y ≡ z) ]
          p ≡ q                                                    ↝⟨ P.subst (λ eq → P.[ (λ i → P.[ (λ j → P (eq i j)) ] y ≡ z) ] p ≡ q)
                                                                              (PH.mono₁ 2 (/-is-setᴾ prop) _ _) ⟩
        P.[ (λ _ → P.[ (λ _ → P x) ] y ≡ z) ] p ≡ q                ↔⟨⟩

        p P.≡ q                                                    □
    where
    module E = Elimᴾ′ e

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

record Recᴾ {A : Type a} (R : A → A → Type r) (B : Type b) :
            Type (a ⊔ r ⊔ b) where
  no-eta-equality
  field
    []ʳ                   : A → B
    []-respects-relationʳ : (r : R x y) → []ʳ x P.≡ []ʳ y
    is-setʳ               : (∀ x y → Is-proposition (R x y)) →
                            P.Is-set B

open Recᴾ public

recᴾ : Recᴾ R B → A / R → B
recᴾ r = elimᴾ λ where
    .[]ʳ                   → R.[]ʳ
    .[]-respects-relationʳ → R.[]-respects-relationʳ
    .is-setʳ prop _        → R.is-setʳ prop
  where
  module R = Recᴾ r

-- An eliminator.

record Elim {A : Type a} {R : A → A → Type r} (P : A / R → Type p) :
            Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ : ∀ x → P [ x ]

    []-respects-relationʳ :
      (r : R x y) →
      subst P ([]-respects-relation r) ([]ʳ x) ≡ []ʳ y

    is-setʳ : (∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x)

open Elim public

elim : Elim P → (x : A / R) → P x
elim e = elimᴾ λ where
    .[]ʳ                   → E.[]ʳ
    .[]-respects-relationʳ → subst≡→[]≡ ∘ E.[]-respects-relationʳ
    .is-setʳ prop          →
      _↔_.to (H-level↔H-level 2) ∘ E.is-setʳ prop
  where
  module E = Elim e

-- A computation rule.

elim-[]-respects-relation :
  dcong (elim e) ([]-respects-relation r) ≡ e .[]-respects-relationʳ r
elim-[]-respects-relation = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec {A : Type a} (R : A → A → Type r) (B : Type b) :
           Type (a ⊔ r ⊔ b) where
  no-eta-equality
  field
    []ʳ                   : A → B
    []-respects-relationʳ : (r : R x y) → []ʳ x ≡ []ʳ y
    is-setʳ               : (∀ x y → Is-proposition (R x y)) → Is-set B

open Rec public

rec : Rec R B → A / R → B
rec r = recᴾ λ where
    .[]ʳ                   → R.[]ʳ
    .[]-respects-relationʳ → _↔_.to ≡↔≡ ∘ R.[]-respects-relationʳ
    .is-setʳ               → _↔_.to (H-level↔H-level 2) ∘ R.is-setʳ
  where
  module R = Rec r

-- A computation rule.

rec-[]-respects-relation :
  cong (rec {R = R} {B = B} r₁)
       ([]-respects-relation {x = x} {y = y} r₂) ≡
  r₁ .[]-respects-relationʳ r₂
rec-[]-respects-relation = cong-≡↔≡ (refl _)

-- A variant of elim that can be used if the motive composed with [_]
-- is a family of propositions.
--
-- I took the idea for this eliminator from Nicolai Kraus.

record Elim-prop
         {A : Type a} {R : A → A → Type r} (P : A / R → Type p) :
         Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ             : ∀ x → P [ x ]
    is-propositionʳ : ∀ x → Is-proposition (P [ x ])

open Elim-prop public

elim-prop : Elim-prop P → (x : A / R) → P x
elim-prop e = elim λ where
    .[]ʳ                     → E.[]ʳ
    .[]-respects-relationʳ _ → E.is-propositionʳ _ _ _
    .is-setʳ _               → elim λ where
      .[]ʳ                     → mono₁ 1 ∘ E.is-propositionʳ
      .[]-respects-relationʳ _ → H-level-propositional ext 2 _ _
      .is-setʳ _ _             → mono₁ 1 (H-level-propositional ext 2)
  where
  module E = Elim-prop e

-- A variant of rec that can be used if the motive is a proposition.

record Rec-prop (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    []ʳ             : A → B
    is-propositionʳ : Is-proposition B

open Rec-prop public

rec-prop : Rec-prop A B → A / R → B
rec-prop r = elim-prop λ where
    .[]ʳ               → R.[]ʳ
    .is-propositionʳ _ → R.is-propositionʳ
  where
  module R = Rec-prop r

------------------------------------------------------------------------
-- Some properties

-- [_] is surjective.

[]-surjective : Surjective ([_] {R = R})
[]-surjective = elim-prop λ where
  .[]ʳ x             → ∣ x , refl _ ∣
  .is-propositionʳ _ → TruncP.truncation-is-proposition

-- If the relation is a propositional equivalence relation, then it is
-- equivalent to equality under [_] (assuming propositional
-- extensionality).
--
-- The basic structure of this proof is that of Proposition 2 in
-- "Quotienting the Delay Monad by Weak Bisimilarity" by Chapman,
-- Uustalu and Veltri.

related≃[equal] :
  {R : A → A → Type r} →
  Propositional-extensionality r →
  Is-equivalence-relation R →
  (∀ {x y} → Is-proposition (R x y)) →
  ∀ {x y} → R x y ≃ _≡_ {A = A / R} [ x ] [ y ]
related≃[equal] {A = A} {r = r} {R = R}
                prop-ext R-equiv R-prop {x = x} {y = y} =
  _↠_.from (Eq.≃↠⇔ R-prop (/-is-set λ _ _ → R-prop))
    (record
       { to   = []-respects-relation
       ; from = λ [x]≡[y] →
                               $⟨ reflexive ⟩
           proj₁ (R′ x [ x ])  ↝⟨ ≡⇒→ (cong (proj₁ ∘ R′ x) [x]≡[y]) ⟩
           proj₁ (R′ x [ y ])  ↝⟨ id ⟩□
           R x y               □
       })
  where
  open Is-equivalence-relation R-equiv

  lemma : ∀ {x y z} → R y z → (R x y , R-prop) ≡ (R x z , R-prop)
  lemma {x} {y} {z} =
    R y z                                ↝⟨ (λ r → record
                                               { to   = flip transitive r
                                               ; from = flip transitive (symmetric r)
                                               }) ⟩
    R x y ⇔ R x z                        ↔⟨ ⇔↔≡″ ext prop-ext ⟩□
    (R x y , R-prop) ≡ (R x z , R-prop)  □

  R′ : A → A / R → Proposition r
  R′ x = rec λ where
    .[]ʳ y                 → R x y , R-prop
    .[]-respects-relationʳ → lemma
    .is-setʳ _             → Is-set-∃-Is-proposition ext prop-ext

-- Quotienting with equality (for a set) amounts to the same thing as
-- not quotienting at all.

/≡↔ : Is-set A → A / _≡_ ↔ A
/≡↔ A-set = record
  { surjection = record
    { logical-equivalence = record
      { from = [_]
      ; to   = rec λ where
          .[]ʳ                   → id
          .[]-respects-relationʳ → id
          .is-setʳ prop          → prop _ _
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = elim λ where
      .[]ʳ _ → refl _

      .is-setʳ prop _ → mono₁ 2 (/-is-set prop)

      .[]-respects-relationʳ _ →
        /-is-set (λ _ _ → A-set) _ _
  }

-- Quotienting with a trivial, pointwise propositional relation
-- amounts to the same thing as using the propositional truncation
-- operator.

/trivial↔∥∥ :
  (∀ x y → R x y) →
  (∀ {x y} → Is-proposition (R x y)) →
  A / R ↔ ∥ A ∥
/trivial↔∥∥ {A = A} {R = R} trivial prop = record
  { surjection = record
    { logical-equivalence = record
      { from = TruncP.rec /-prop [_]
      ; to   = rec-prop λ where
          .[]ʳ             → ∣_∣
          .is-propositionʳ → TruncP.truncation-is-proposition
      }
    ; right-inverse-of = TruncP.elim
        _
        (λ _ → ⇒≡ 1 TruncP.truncation-is-proposition)
        (λ _ → refl _)
    }
  ; left-inverse-of = elim-prop λ where
      .[]ʳ _             → refl _
      .is-propositionʳ _ → /-is-set λ _ _ → prop
  }
  where
  /-prop : Is-proposition (A / R)
  /-prop = elim-prop λ where
    .[]ʳ x → elim-prop λ where
      .[]ʳ y             → []-respects-relation (trivial x y)
      .is-propositionʳ _ → /-is-set λ _ _ → prop
    .is-propositionʳ _ →
      Π-closure ext 1 λ _ →
      /-is-set λ _ _ → prop

-- The previous property gives us an alternative to
-- constant-function≃∥inhabited∥⇒inhabited.

constant-function↔∥inhabited∥⇒inhabited :
  Is-set B →
  (∃ λ (f : A → B) → Constant f) ↔ (∥ A ∥ → B)
constant-function↔∥inhabited∥⇒inhabited {B = B} {A = A} B-set =
  (∃ λ (f : A → B) → Constant f)  ↝⟨ record
                                       { surjection = record
                                         { logical-equivalence = record
                                           { to   = λ { (f , c) → rec λ where
                                                        .[]ʳ                     → f
                                                        .[]-respects-relationʳ _ → c _ _
                                                        .is-setʳ _               → B-set }
                                           ; from = λ f → (f ∘ [_])
                                                        , (λ _ _ → cong f ([]-respects-relation _))
                                           }
                                         ; right-inverse-of = λ f → ⟨ext⟩ $ elim λ where
                                             .[]ʳ _                   → refl _
                                             .[]-respects-relationʳ _ → B-set _ _
                                             .is-setʳ _ _             → mono₁ 2 B-set
                                         }
                                       ; left-inverse-of = λ _ → Σ-≡,≡→≡
                                           (refl _)
                                           ((Π-closure ext 1 λ _ →
                                             Π-closure ext 1 λ _ →
                                             B-set) _ _)
                                       } ⟩
  (A / (λ _ _ → ⊤) → B)           ↝⟨ →-cong₁ ext (/trivial↔∥∥ _ (mono₁ 0 ⊤-contractible)) ⟩□
  (∥ A ∥ → B)                     □

-- The two directions of the proposition above compute in the
-- "right" way. Note that (at the time of writing) an analogue of
-- the second property below fails to hold definitionally for
-- constant-function≃∥inhabited∥⇒inhabited.

_ :
  {B-set : Is-set B} →
  _↔_.to (constant-function↔∥inhabited∥⇒inhabited B-set) f ∣ x ∣ ≡
  proj₁ f x
_ = refl _

_ :
  {B-set : Is-set B} →
  proj₁ (_↔_.from (constant-function↔∥inhabited∥⇒inhabited B-set) f)
        x ≡
  f ∣ x ∣
_ = refl _

------------------------------------------------------------------------
-- Preservation lemmas

-- A preservation lemma for functions.

/-map :
  ((∀ x y → Is-proposition (R₁ x y)) →
   (∀ x y → Is-proposition (R₂ x y))) →
  (A₁→A₂ : A₁ → A₂) →
  (∀ x y → R₁ x y → R₂ (A₁→A₂ x) (A₁→A₂ y)) →
  A₁ / R₁ → A₂ / R₂
/-map {R₁ = R₁} {R₂ = R₂} prop A₁→A₂ R₁→R₂ = rec λ where
  .[]ʳ → [_] ∘ A₁→A₂

  .is-setʳ → /-is-set ∘ prop

  .[]-respects-relationʳ {x = x} {y = y} →
     R₁ x y                     ↝⟨ R₁→R₂ _ _ ⟩
     R₂ (A₁→A₂ x) (A₁→A₂ y)     ↝⟨ []-respects-relation ⟩□
     [ A₁→A₂ x ] ≡ [ A₁→A₂ y ]  □

-- A preservation lemma for logical equivalences.

/-cong-⇔ :
  ((∀ x y → Is-proposition (R₁ x y)) ⇔
   (∀ x y → Is-proposition (R₂ x y))) →
  (A₁⇔A₂ : A₁ ⇔ A₂) →
  (∀ x y → R₁ x y → R₂ (_⇔_.to   A₁⇔A₂ x) (_⇔_.to   A₁⇔A₂ y)) →
  (∀ x y → R₂ x y → R₁ (_⇔_.from A₁⇔A₂ x) (_⇔_.from A₁⇔A₂ y)) →
  A₁ / R₁ ⇔ A₂ / R₂
/-cong-⇔ prop A₁⇔A₂ R₁→R₂ R₂→R₁ = record
  { to   = /-map (_⇔_.to   prop) (_⇔_.to   A₁⇔A₂) R₁→R₂
  ; from = /-map (_⇔_.from prop) (_⇔_.from A₁⇔A₂) R₂→R₁
  }

-- A preservation lemma for split surjections.

/-cong-↠ :
  ((∀ x y → Is-proposition (R₁ x y)) ⇔
   (∀ x y → Is-proposition (R₂ x y))) →
  (A₁↠A₂ : A₁ ↠ A₂) →
  (∀ x y → R₁ x y ↠ R₂ (_↠_.to A₁↠A₂ x) (_↠_.to A₁↠A₂ y)) →
  A₁ / R₁ ↠ A₂ / R₂
/-cong-↠ {R₁ = R₁} {R₂ = R₂} prop A₁↠A₂ R₁↠R₂ = record
  { logical-equivalence = /-cong-⇔
      prop
      (_↠_.logical-equivalence A₁↠A₂)
      (λ x y → _↠_.to (R₁↠R₂ x y))
      (λ x y → R₂ x y                          ↝⟨ ≡⇒↝ _ (sym $ cong₂ R₂ (right-inverse-of x) (right-inverse-of y)) ⟩
               R₂ (to (from x)) (to (from y))  ↝⟨ _↠_.from (R₁↠R₂ _ _) ⟩□
               R₁ (from x) (from y)            □)
  ; right-inverse-of = elim λ where
      .[]ʳ x →
        [ to (from x) ]  ≡⟨ cong [_] $ right-inverse-of x ⟩∎
        [ x ]            ∎

      .is-setʳ prop _ → mono₁ 1 (/-is-set prop)

      .[]-respects-relationʳ {x = x} {y = y} r →
        let tr = λ x y → _↠_.to (R₁↠R₂ x y)

            fr = λ x y →
                   _↠_.from (R₁↠R₂ (from x) (from y)) ∘
                   ≡⇒↝ _
                     (sym (cong₂ R₂ (right-inverse-of x)
                                    (right-inverse-of y)))

            t = /-map (_⇔_.to prop) to tr

            f = /-map (_⇔_.from prop) from fr
        in
        subst (λ x → t (f x) ≡ x)
          ([]-respects-relation r)
          (cong [_] (right-inverse-of x))                       ≡⟨ subst-in-terms-of-trans-and-cong ⟩

        trans
          (sym (cong (t ∘ f) ([]-respects-relation r)))
          (trans (cong [_] (right-inverse-of x))
             (cong id ([]-respects-relation r)))                ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym eq₁)
                                                                                (trans (cong [_] (right-inverse-of x)) eq₂))
                                                                     (sym $ cong-∘ _ _ _)
                                                                     (sym $ cong-id _) ⟩
        trans
          (sym (cong t (cong f ([]-respects-relation r))))
          (trans (cong [_] (right-inverse-of x))
             ([]-respects-relation r))                          ≡⟨ cong (λ eq → trans (sym (cong t eq))
                                                                                (trans (cong [_] (right-inverse-of x))
                                                                                ([]-respects-relation r))) $
                                                                   rec-[]-respects-relation ⟩
        trans
          (sym (cong t ([]-respects-relation (fr _ _ r))))
          (trans (cong [_] (right-inverse-of x))
             ([]-respects-relation r))                          ≡⟨ cong (λ eq → trans (sym eq)
                                                                                (trans (cong [_] (right-inverse-of x))
                                                                                ([]-respects-relation r))) $
                                                                   rec-[]-respects-relation ⟩
        trans
          (sym ([]-respects-relation (tr _ _ (fr _ _ r))))
          (trans (cong [_] (right-inverse-of x))
             ([]-respects-relation r))                          ≡⟨ cong (λ r′ → trans (sym ([]-respects-relation r′))
                                                                                (trans (cong [_] (right-inverse-of x))
                                                                                ([]-respects-relation r))) $
                                                                   _↠_.right-inverse-of (R₁↠R₂ _ _) _ ⟩
        trans
          (sym ([]-respects-relation
                  (≡⇒↝ _ (sym (cong₂ R₂ (right-inverse-of x)
                                        (right-inverse-of y)))
                     r)))
          (trans (cong [_] (right-inverse-of x))
             ([]-respects-relation r))                          ≡⟨ lemma _ _ _ ⟩∎

        cong [_] (right-inverse-of y)                           ∎
  }
  where
  open _↠_ A₁↠A₂

  lemma : ∀ _ _ _ → _
  lemma x y r =
    elim₁
      (λ eq →
         trans
           (sym ([]-respects-relation
                   (≡⇒↝ _ (sym (cong₂ R₂ (right-inverse-of x) eq)) r)))
           (trans (cong [_] (right-inverse-of x))
              ([]-respects-relation r)) ≡
         cong [_] eq)
      (elim₁
         (λ eq →
            trans
              (sym ([]-respects-relation
                      (≡⇒↝ _ (sym (cong₂ R₂ eq (refl _))) r)))
              (trans (cong [_] eq) ([]-respects-relation r)) ≡
            cong [_] (refl _))
         (trans
            (sym ([]-respects-relation
                    (≡⇒↝ _ (sym (cong₂ R₂ (refl _) (refl _))) r)))
            (trans (cong [_] (refl _)) ([]-respects-relation r))    ≡⟨ cong₂ (λ eq₁ eq₂ →
                                                                                trans (sym ([]-respects-relation (≡⇒↝ _ eq₁ r)))
                                                                                (trans eq₂ ([]-respects-relation r)))
                                                                         (trans (cong sym $ cong₂-refl R₂) sym-refl)
                                                                         (cong-refl _) ⟩
          trans
            (sym ([]-respects-relation (≡⇒↝ _ (refl _) r)))
            (trans (refl _) ([]-respects-relation r))               ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym ([]-respects-relation eq₁)) eq₂)
                                                                         (cong (_$ r) ≡⇒↝-refl)
                                                                         (trans-reflˡ _) ⟩
          trans
            (sym ([]-respects-relation r))
            ([]-respects-relation r)                                ≡⟨ trans-symˡ _ ⟩

          refl _                                                    ≡⟨ sym $ cong-refl _ ⟩∎

          cong [_] (refl _)                                         ∎)
         (right-inverse-of x))
      (right-inverse-of y)

private

  -- A preservation lemma for equivalences.

  /-cong-≃ :
    ((∀ x y → Is-proposition (R₁ x y)) ⇔
     (∀ x y → Is-proposition (R₂ x y))) →
    (A₁≃A₂ : A₁ ≃ A₂) →
    (∀ x y →
       R₁ x y ≃ R₂ (to-implication A₁≃A₂ x) (to-implication A₁≃A₂ y)) →
    A₁ / R₁ ≃ A₂ / R₂
  /-cong-≃ {R₁ = R₁} {R₂ = R₂} prop A₁≃A₂ R₁≃R₂ = Eq.↔⇒≃ (record
    { surjection = /-cong-↠ prop (_≃_.surjection A₁≃A₂) λ x y →
        R₁ x y            ↔⟨ R₁≃R₂ x y ⟩□
        R₂ (to x) (to y)  □
    ; left-inverse-of = elim λ where
        .[]ʳ x →
          [ from (to x) ]  ≡⟨ cong [_] $ left-inverse-of x ⟩∎
          [ x ]            ∎

        .is-setʳ prop _ → mono₁ 1 (/-is-set prop)

        .[]-respects-relationʳ {x = x} {y = y} r →
          let tr = λ x y → _≃_.to (R₁≃R₂ x y)

              fr = λ x y →
                     _≃_.from (R₁≃R₂ (from x) (from y)) ∘
                     ≡⇒↝ _
                       (sym (cong₂ R₂ (right-inverse-of x)
                                      (right-inverse-of y)))

              t = /-map (_⇔_.to prop) to tr

              f = /-map (_⇔_.from prop) from fr
          in
          subst (λ x → f (t x) ≡ x)
            ([]-respects-relation r)
            (cong [_] (left-inverse-of x))                       ≡⟨ subst-in-terms-of-trans-and-cong ⟩

          trans
            (sym (cong (f ∘ t) ([]-respects-relation r)))
            (trans (cong [_] (left-inverse-of x))
               (cong id ([]-respects-relation r)))               ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym eq₁)
                                                                                (trans (cong [_] (left-inverse-of x)) eq₂))
                                                                      (sym $ cong-∘ _ _ _)
                                                                      (sym $ cong-id _) ⟩
          trans
            (sym (cong f (cong t ([]-respects-relation r))))
            (trans (cong [_] (left-inverse-of x))
               ([]-respects-relation r))                         ≡⟨ cong (λ eq → trans (sym (cong f eq))
                                                                                (trans (cong [_] (left-inverse-of x))
                                                                                ([]-respects-relation r))) $
                                                                    rec-[]-respects-relation ⟩
          trans
            (sym (cong f ([]-respects-relation (tr _ _ r))))
            (trans (cong [_] (left-inverse-of x))
               ([]-respects-relation r))                         ≡⟨ cong (λ eq → trans (sym eq)
                                                                                (trans (cong [_] (left-inverse-of x))
                                                                                ([]-respects-relation r))) $
                                                                    rec-[]-respects-relation ⟩
          trans
            (sym ([]-respects-relation (fr _ _ (tr _ _ r))))
            (trans (cong [_] (left-inverse-of x))
               ([]-respects-relation r))                         ≡⟨ cong (λ r′ → trans (sym ([]-respects-relation r′))
                                                                                (trans (cong [_] (left-inverse-of x))
                                                                                ([]-respects-relation r))) $
                                                                    lemma₁ _ _ _ ⟩
          trans
            (sym ([]-respects-relation
                    (≡⇒↝ _ (sym (cong₂ R₁ (left-inverse-of x)
                                          (left-inverse-of y)))
                       r)))
            (trans (cong [_] (left-inverse-of x))
               ([]-respects-relation r))                         ≡⟨ lemma₂ _ _ _ ⟩∎

          cong [_] (left-inverse-of y)                           ∎
    })
    where
    open _≃_ A₁≃A₂

    lemma₀ : ∀ _ _ _ → _
    lemma₀ x y r =
      elim₁
        (λ eq →
           _≃_.from (R₁≃R₂ (from (to x)) _)
             (≡⇒↝ _ (sym (cong₂ (λ x y → R₂ (to x) (to y))
                            (left-inverse-of x) eq))
                (_≃_.to (R₁≃R₂ x y) r)) ≡
           ≡⇒↝ _ (sym (cong₂ R₁ (left-inverse-of x) eq)) r)
        (elim₁
           (λ eq →
              _≃_.from (R₁≃R₂ _ _)
                (≡⇒↝ _ (sym (cong₂ (λ x y → R₂ (to x) (to y))
                               eq (refl _)))
                   (_≃_.to (R₁≃R₂ x y) r)) ≡
              ≡⇒↝ _ (sym (cong₂ R₁ eq (refl _))) r)
           (_≃_.from (R₁≃R₂ _ _)
              (≡⇒↝ _ (sym (cong₂ (λ x y → R₂ (to x) (to y))
                             (refl _) (refl _)))
                 (_≃_.to (R₁≃R₂ x y) r))                                  ≡⟨ cong (λ eq → _≃_.from (R₁≃R₂ _ _) (≡⇒↝ _ eq (_≃_.to (R₁≃R₂ x y) r))) $
                                                                             trans (cong sym $ cong₂-refl _) sym-refl ⟩

            _≃_.from (R₁≃R₂ _ _) (≡⇒↝ _ (refl _) (_≃_.to (R₁≃R₂ x y) r))  ≡⟨ cong (_≃_.from (R₁≃R₂ _ _)) $ cong (_$ _≃_.to (R₁≃R₂ x y) r)
                                                                             ≡⇒↝-refl ⟩

            _≃_.from (R₁≃R₂ _ _) (_≃_.to (R₁≃R₂ x y) r)                   ≡⟨ _≃_.left-inverse-of (R₁≃R₂ _ _) _ ⟩

            r                                                             ≡⟨ sym $ cong (_$ r) ≡⇒↝-refl ⟩

            ≡⇒↝ _ (refl _) r                                              ≡⟨ cong (λ eq → ≡⇒↝ _ eq r) $ sym $
                                                                             trans (cong sym $ cong₂-refl _) sym-refl ⟩∎
            ≡⇒↝ _ (sym (cong₂ R₁ (refl _) (refl _))) r                    ∎)
           (left-inverse-of x))
        (left-inverse-of y)

    lemma₁ : ∀ _ _ _ → _
    lemma₁ x y r =
      _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
        (≡⇒↝ _ (sym (cong₂ R₂ (right-inverse-of (to x))
                              (right-inverse-of (to y))))
           (_≃_.to (R₁≃R₂ x y) r))                                       ≡⟨⟩

      _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
        (≡⇒↝ _ (sym (trans (cong (flip R₂ _) (right-inverse-of (to x)))
                       (cong (R₂ _) (right-inverse-of (to y)))))
           (_≃_.to (R₁≃R₂ x y) r))                                       ≡⟨ cong₂ (λ eq₁ eq₂ →
                                                                                _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
                                                                                (≡⇒↝ _ (sym (trans eq₁ eq₂)) (_≃_.to (R₁≃R₂ x y) r)))
                                                                              (trans (cong (cong _) $ sym $ left-right-lemma _) (cong-∘ _ _ _))
                                                                              (trans (cong (cong _) $ sym $ left-right-lemma _) (cong-∘ _ _ _)) ⟩
      _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
        (≡⇒↝ _ (sym (trans (cong (flip R₂ _ ∘ to) (left-inverse-of x))
                       (cong (R₂ _ ∘ to) (left-inverse-of y))))
           (_≃_.to (R₁≃R₂ x y) r))                                       ≡⟨⟩

      _≃_.from (R₁≃R₂ (from (to x)) (from (to y)))
        (≡⇒↝ _ (sym (cong₂ (λ x y → R₂ (to x) (to y))
                       (left-inverse-of x)
                       (left-inverse-of y)))
           (_≃_.to (R₁≃R₂ x y) r))                                       ≡⟨ lemma₀ _ _ _ ⟩∎

      ≡⇒↝ _ (sym (cong₂ R₁ (left-inverse-of x) (left-inverse-of y))) r   ∎

    lemma₂ : ∀ _ _ _ → _
    lemma₂ x y r =
      elim₁
        (λ eq →
           trans
             (sym ([]-respects-relation
                     (≡⇒↝ _ (sym (cong₂ R₁ (left-inverse-of x) eq)) r)))
             (trans (cong [_] (left-inverse-of x))
                ([]-respects-relation r)) ≡
           cong [_] eq)
        (elim₁
           (λ eq →
              trans
                (sym ([]-respects-relation
                        (≡⇒↝ _ (sym (cong₂ R₁ eq (refl _))) r)))
                (trans (cong [_] eq) ([]-respects-relation r)) ≡
              cong [_] (refl _))
           (trans
              (sym ([]-respects-relation
                      (≡⇒↝ _ (sym (cong₂ R₁ (refl _) (refl _))) r)))
              (trans (cong [_] (refl _)) ([]-respects-relation r))    ≡⟨ cong₂ (λ eq₁ eq₂ →
                                                                                trans (sym ([]-respects-relation (≡⇒↝ _ eq₁ r)))
                                                                                (trans eq₂ ([]-respects-relation r)))
                                                                           (trans (cong sym $ cong₂-refl R₁) sym-refl)
                                                                           (cong-refl _) ⟩
            trans
              (sym ([]-respects-relation (≡⇒↝ _ (refl _) r)))
              (trans (refl _) ([]-respects-relation r))               ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym ([]-respects-relation eq₁)) eq₂)
                                                                           (cong (_$ r) ≡⇒↝-refl)
                                                                           (trans-reflˡ _) ⟩
            trans
              (sym ([]-respects-relation r))
              ([]-respects-relation r)                                ≡⟨ trans-symˡ _ ⟩

            refl _                                                    ≡⟨ sym $ cong-refl _ ⟩∎

            cong [_] (refl _)                                         ∎)
           (left-inverse-of x))
        (left-inverse-of y)

-- A preservation lemma for isomorphisms.

/-cong-↔ :
  {A₁ : Type a₁} {R₁ : A₁ → A₁ → Type r₁}
  {A₂ : Type a₂} {R₂ : A₂ → A₂ → Type r₂} →
  ((∀ x y → Is-proposition (R₁ x y)) ⇔
   (∀ x y → Is-proposition (R₂ x y))) →
  (A₁↔A₂ : A₁ ↔[ k ] A₂) →
  (∀ x y →
     R₁ x y ↔[ k ]
     R₂ (to-implication A₁↔A₂ x) (to-implication A₁↔A₂ y)) →
  A₁ / R₁ ↔[ k ] A₂ / R₂
/-cong-↔ {k = k} {R₁ = R₁} {R₂ = R₂} prop A₁↔A₂ R₁↔R₂ =
  from-isomorphism $
  /-cong-≃ prop A₁≃A₂ λ x y →
    R₁ x y                                                ↔⟨ R₁↔R₂ x y ⟩
    R₂ (to-implication A₁↔A₂ x) (to-implication A₁↔A₂ y)  ↝⟨ ≡⇒↝ _ $ cong₂ (λ f g → R₂ (f x) (g y))
                                                                       (to-implication∘from-isomorphism k equivalence)
                                                                       (to-implication∘from-isomorphism k equivalence) ⟩□
    R₂ (_≃_.to A₁≃A₂ x) (_≃_.to A₁≃A₂ y)                  □
  where
  A₁≃A₂ = from-isomorphism A₁↔A₂

------------------------------------------------------------------------
-- The quotients defined here can be related to the ones defined in
-- Quotient

-- If the quotient relation is propositional, then the definition of
-- quotients given in Quotient is equivalent to the one given here.

/≃/ :
  (∀ {x y} → Is-proposition (R x y)) →
  A / R ≃ A Quotient./ R
/≃/ R-prop = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to = rec (λ where
          .[]ʳ → Quotient.[_]

          .[]-respects-relationʳ → Quotient.[]-respects-relation

          .is-setʳ _ → Quotient./-is-set)
      ; from = Quotient.rec λ where
          .Quotient.Rec.[]ʳ → [_]

          .Quotient.Rec.[]-respects-relationʳ → []-respects-relation

          .Quotient.Rec.is-setʳ → /-is-set λ _ _ → R-prop
      }
    ; right-inverse-of = Quotient.elim-prop λ where
        .Quotient.Elim-prop.[]ʳ _ → refl _

        .Quotient.Elim-prop.is-propositionʳ _ → Quotient./-is-set
    }
  ; left-inverse-of = elim-prop λ where
        .Elim-prop.[]ʳ _ → refl _

        .Elim-prop.is-propositionʳ _ → /-is-set λ _ _ → R-prop
  })

------------------------------------------------------------------------
-- The quotients defined here can be related to the ones defined in
-- QF.Families-of-equivalence-classes

private

  -- An alternative definition of the quotients from
  -- QF.Families-of-equivalence-classes.

  infix 5 _/′_

  _/′_ : (A : Type a) → (A → A → Type a) → Type (lsuc a)
  _/′_ {a = a} A R = ∃ λ (P : A → Type a) → ∥ (∃ λ x → R x ≡ P) ∥

  /↔/′ : A QF./ R ↔ A /′ R
  /↔/′ {A = A} {R = R} =
    A QF./ R                                                  ↔⟨⟩
    (∃ λ (P : A → Type _) → Trunc.∥ (∃ λ x → R x ≡ P) ∥ 1 _)  ↝⟨ (∃-cong λ _ → inverse $ TruncP.∥∥↔∥∥ lzero) ⟩
    (∃ λ (P : A → Type _) → ∥ (∃ λ x → R x ≡ P) ∥)            ↔⟨⟩
    A /′ R                                                    □

  [_]′ : A → A /′ R
  [_]′ = _↔_.to /↔/′ ∘ QF.[_]

  rec′ :
    {A : Type a} {R : A → A → Type a} →
    (∀ {x} → R x x) →
    (B : Type a) →
    Is-set B →
    (f : A → B) →
    (∀ {x y} → R x y → f x ≡ f y) →
    A /′ R → B
  rec′ refl B B-set f R⇒≡ =
    QF.rec ext refl B B-set f R⇒≡ ∘
    _↔_.from /↔/′

  elim-Prop′ :
    {A : Type a} {R : A → A → Type a} →
    QF.Strong-equivalence-with surjection R →
    (B : A /′ R → Type (lsuc a)) →
    (∀ x → Is-proposition (B [ x ]′)) →
    (f : ∀ x → B [ x ]′) →
    ∀ x → B x
  elim-Prop′ strong-equivalence B B-prop f x =
    subst B (_↔_.right-inverse-of /↔/′ _) $
      QF.elim-Prop
        ext
        strong-equivalence
        (B ∘ _↔_.to /↔/′)
        B-prop
        f
        (_↔_.from /↔/′ x)

-- If the relation is a propositional equivalence relation of a
-- certain size, then the quotients defined above are isomorphic to
-- families of equivalence relations, defined in a certain way
-- (assuming univalence).

/↔ :
  {A : Type a} {R : A → A → Type a} →
  Univalence a →
  Univalence lzero →
  Is-equivalence-relation R →
  (∀ {x y} → Is-proposition (R x y)) →
  A / R ↔ ∃ λ (P : A → Type a) → ∥ (∃ λ x → R x ≡ P) ∥
/↔ {a = a} {A = A} {R = R} univ univ₀ R-equiv R-prop = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  R-is-strong-equivalence : QF.Strong-equivalence R
  R-is-strong-equivalence =
    QF.propositional-equivalence⇒strong-equivalence
      ext univ R-equiv (λ _ _ → R-prop)

  to : A / R → A /′ R
  to = rec λ where
    .[]ʳ → [_]′

    .[]-respects-relationʳ {x = x} {y = y} →
      R x y                ↝⟨ _≃_.to (QF.related↝[equal] ext R-is-strong-equivalence) ⟩
      QF.[ x ] ≡ QF.[ y ]  ↝⟨ cong (_↔_.to /↔/′) ⟩□
      [ x ]′ ≡ [ y ]′      □

    .is-setʳ prop →      $⟨ (λ {_ _} → QF.quotient's-h-level-is-1-+-relation's-h-level
                                         ext univ univ₀ 1 (λ _ _ → R-prop)) ⟩
      Is-set (A QF./ R)  ↝⟨ H.respects-surjection (_↔_.surjection /↔/′) 2 ⟩□
      Is-set (A /′ R)    □

  from : A /′ R → A / R
  from = rec′
    (Is-equivalence-relation.reflexive R-equiv)
    _
    (/-is-set λ _ _ → R-prop)
    [_]
    []-respects-relation

  to∘from : ∀ x → to (from x) ≡ x
  to∘from = elim-Prop′
    (QF.strong-equivalence⇒strong-equivalence-with
       R-is-strong-equivalence)
    _
    (λ x →                                         $⟨ (λ {_ _} → QF.quotient's-h-level-is-1-+-relation's-h-level
                                                                   ext univ univ₀ 1 λ _ _ → R-prop) ⟩
       Is-set (A QF./ R)                           ↝⟨ H.respects-surjection (_↔_.surjection /↔/′) 2 ⟩
       Is-set (A /′ R)                             ↝⟨ +⇒≡ {n = 1} ⟩□
       Is-proposition (to (from [ x ]′) ≡ [ x ]′)  □)
    (λ _ → refl _)

  from∘to : ∀ x → from (to x) ≡ x
  from∘to = elim-prop λ where
    .[]ʳ _             → refl _
    .is-propositionʳ _ → /-is-set λ _ _ → R-prop

-- If the relation is a propositional equivalence relation of a
-- certain size, then the definition of quotients given in
-- QF.Families-of-equivalence-classes is isomorphic to the one given
-- here (assuming univalence).

/↔/ :
  {A : Type a} {R : A → A → Type a} →
  Univalence a →
  Univalence lzero →
  Is-equivalence-relation R →
  (R-prop : ∀ {x y} → Is-proposition (R x y)) →
  A QF./ R ↔ A / R
/↔/ {a = a} {A = A} {R = R} univ univ₀ R-equiv R-prop =
  A QF./ R                                                         ↔⟨⟩
  (∃ λ (P : A → Type a) → Trunc.∥ (∃ λ x → R x ≡ P) ∥ 1 (lsuc a))  ↝⟨ (∃-cong λ _ → inverse $ TruncP.∥∥↔∥∥ lzero) ⟩
  (∃ λ (P : A → Type a) →       ∥ (∃ λ x → R x ≡ P) ∥)             ↝⟨ inverse $ /↔ univ univ₀ R-equiv R-prop ⟩□
  A / R                                                            □

------------------------------------------------------------------------
-- Various type formers commute with quotients

-- _⊎_ commutes with quotients if the relations are pointwise
-- propositional.

⊎/-comm :
  (∀ {x y} → Is-proposition (R₁ x y)) →
  (∀ {x y} → Is-proposition (R₂ x y)) →
  (A₁ ⊎ A₂) / (R₁ ⊎ᴾ R₂) ↔ A₁ / R₁ ⊎ A₂ / R₂
⊎/-comm R₁-prop R₂-prop = record
  { surjection = record
    { logical-equivalence = record
      { to = rec λ where
          .[]ʳ          → ⊎-map [_] [_]
          .is-setʳ prop → ⊎-closure 0 is-set₁ is-set₂

          .[]-respects-relationʳ {x = inj₁ _} {y = inj₁ _} →
            cong inj₁ ∘ []-respects-relation
          .[]-respects-relationʳ {x = inj₂ _} {y = inj₂ _} →
            cong inj₂ ∘ []-respects-relation

      ; from = Prelude.[ rec (λ where
                           .[]ʳ                   → [_] ∘ inj₁
                           .[]-respects-relationʳ → []-respects-relation
                           .is-setʳ prop          → is-set₁₂)
                       , rec (λ where
                           .[]ʳ                   → [_] ∘ inj₂
                           .[]-respects-relationʳ → []-respects-relation
                           .is-setʳ prop          → is-set₁₂)
                       ]
      }
    ; right-inverse-of =
        Prelude.[ elim-prop (λ where
                    .[]ʳ _             → refl _
                    .is-propositionʳ _ → ⊎-closure 0 is-set₁ is-set₂)
                , elim-prop (λ where
                    .[]ʳ _             → refl _
                    .is-propositionʳ _ → ⊎-closure 0 is-set₁ is-set₂)
                ]
    }
  ; left-inverse-of = elim-prop λ where
      .[]ʳ               → Prelude.[ (λ _ → refl _) , (λ _ → refl _) ]
      .is-propositionʳ _ → is-set₁₂
  }
  where
  is-set₁  = /-is-set λ _ _ → R₁-prop
  is-set₂  = /-is-set λ _ _ → R₂-prop
  is-set₁₂ = /-is-set λ x y → ⊎ᴾ-preserves-Is-proposition
                                R₁-prop R₂-prop {x = x} {y = y}

-- Maybe commutes with quotients if the relation is pointwise
-- propositional.
--
-- Chapman, Uustalu and Veltri mention a similar result in
-- "Quotienting the Delay Monad by Weak Bisimilarity".

Maybe/-comm :
  (∀ {x y} → Is-proposition (R x y)) →
  Maybe A / Maybeᴾ R ↔ Maybe (A / R)
Maybe/-comm {A = A} {R = R} R-prop =
  Maybe A / Maybeᴾ R   ↝⟨ ⊎/-comm (↑-closure 1 (mono₁ 0 ⊤-contractible)) R-prop ⟩
  ⊤ / Trivial ⊎ A / R  ↝⟨ /trivial↔∥∥ _ (↑-closure 1 (mono₁ 0 ⊤-contractible)) ⊎-cong F.id ⟩
  ∥ ⊤ ∥ ⊎ A / R        ↝⟨ TruncP.∥∥↔ (mono₁ 0 ⊤-contractible) ⊎-cong F.id ⟩□
  Maybe (A / R)        □

-- A simplification lemma for Maybe/-comm.

Maybe/-comm-[] :
  {R : A → A → Type r}
  {R-prop : ∀ {x y} → Is-proposition (R x y)} →
  _↔_.to (Maybe/-comm {R = R} R-prop) ∘ [_] ≡ ⊎-map id [_]
Maybe/-comm-[] {R-prop = R-prop} =
  _↔_.to (Maybe/-comm R-prop) ∘ [_]        ≡⟨⟩
  ⊎-map _ id ∘ ⊎-map _ id ∘ ⊎-map [_] [_]  ≡⟨ cong (_∘ ⊎-map [_] [_]) $ sym $ ⟨ext⟩ ⊎-map-∘ ⟩
  ⊎-map _ id ∘ ⊎-map [_] [_]               ≡⟨ sym $ ⟨ext⟩ ⊎-map-∘ ⟩∎
  ⊎-map id [_]                             ∎

-- The sigma type former commutes (kind of) with quotients, assuming
-- that certain families are propositional.

Σ/-comm :
  {P : A / R → Type p} →
  (∀ {x} → Is-proposition (P x)) →
  (∀ {x y} → Is-proposition (R x y)) →
  Σ (A / R) P ↔ Σ A (P ∘ [_]) / (R on proj₁)
Σ/-comm {A = A} {R = R} {P = P} P-prop R-prop = record
  { surjection = record
    { logical-equivalence = record
      { to =
          uncurry $
          elim λ where
            .[]ʳ → curry [_]
            .[]-respects-relationʳ {x = x} {y = y} r → ⟨ext⟩ λ P[y] →
              subst (λ x → P x → Σ A (P ∘ [_]) / (R on proj₁))
                    ([]-respects-relation r)
                    (curry [_] x) P[y]                               ≡⟨ subst-→-domain P {f = curry [_] _} ([]-respects-relation r) ⟩

              [ (x , subst P (sym $ []-respects-relation r) P[y]) ]  ≡⟨ []-respects-relation r ⟩∎

              [ (y , P[y]) ]                                         ∎
            .is-setʳ prop _ →
              Π-closure ext 2 λ _ →
              /-is-set λ _ _ → prop _ _
      ; from = rec λ where
          .[]ʳ       → Σ-map [_] id
          .is-setʳ _ →
            Σ-closure 2 (/-is-set λ _ _ → R-prop) (λ _ → mono₁ 1 P-prop)

          .[]-respects-relationʳ {x = (x₁ , x₂)} {y = (y₁ , y₂)} →
            R x₁ y₁                        ↝⟨ []-respects-relation ⟩
            [ x₁ ] ≡ [ y₁ ]                ↔⟨ ignore-propositional-component P-prop ⟩
            ([ x₁ ] , x₂) ≡ ([ y₁ ] , y₂)  □
      }
    ; right-inverse-of = elim-prop λ where
        .[]ʳ _             → refl _
        .is-propositionʳ _ → /-is-set λ _ _ → R-prop
    }
  ; left-inverse-of = uncurry $ elim-prop λ where
      .[]ʳ _ _           → refl _
      .is-propositionʳ _ →
        Π-closure ext 1 λ _ →
        Σ-closure 2 (/-is-set λ _ _ → R-prop) (λ _ → mono₁ 1 P-prop)
  }

-- The type former λ X → ℕ → X commutes with quotients, assuming that
-- the quotient relation is a propositional equivalence relation, and
-- also assuming countable choice and propositional extensionality.
--
-- This result is very similar to Proposition 5 in "Quotienting the
-- Delay Monad by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

-- The forward component of the isomorphism. This component can be
-- defined without any extra assumptions.

ℕ→/-comm-to : (ℕ → A) / (ℕ →ᴾ R) → (ℕ → A / R)
ℕ→/-comm-to {A = A} = rec λ where
    .[]ʳ f n → [ f n ]

    .[]-respects-relationʳ r →
      ⟨ext⟩ ([]-respects-relation ∘ r)

    .is-setʳ prop →
      Π-closure ext 2 λ _ →
      /-is-set (prop⇒prop prop)
  where
  prop⇒prop :
    ((f g : ℕ → A) → Is-proposition ((ℕ →ᴾ R) f g)) →
    ((x y : A) → Is-proposition (R x y))
  prop⇒prop prop x y p q =
    cong (_$ 0) $ prop (λ _ → x) (λ _ → y) (λ _ → p) (λ _ → q)

-- The isomorphism.

ℕ→/-comm :
  {A : Type a} {R : A → A → Type r} →
  Axiom-of-countable-choice (a ⊔ r) →
  Propositional-extensionality r →
  Is-equivalence-relation R →
  (∀ {x y} → Is-proposition (R x y)) →
  (ℕ → A) / (ℕ →ᴾ R) ↔ (ℕ → A / R)
ℕ→/-comm {A = A} {R = R} cc prop-ext R-equiv R-prop = record
  { surjection = record
    { logical-equivalence = record
      { to   = ℕ→/-comm-to
      ; from = from unit
      }
    ; right-inverse-of = to∘from unit
    }
  ; left-inverse-of = from∘to unit
  }
  where
  [_]→ : (ℕ → A) → (ℕ → A / R)
  [ f ]→ n = [ f n ]

  -- A module that is introduced to ensure that []→-surjective is not
  -- in the same abstract block as the abstract definitions below.

  module Dummy where

    abstract

      []→-surjective : Surjective [_]→
      []→-surjective f =                    $⟨ []-surjective ⟩
        Surjective [_]                      ↝⟨ (λ surj → surj ∘ f) ⦂ (_ → _) ⟩
        (∀ n → ∥ (∃ λ x → [ x ] ≡ f n) ∥)   ↔⟨ TruncP.countable-choice-bijection cc ⟩
        ∥ (∀ n → ∃ λ x → [ x ] ≡ f n) ∥     ↔⟨ TruncP.∥∥-cong ΠΣ-comm ⟩
        ∥ (∃ λ g → ∀ n → [ g n ] ≡ f n) ∥   ↔⟨⟩
        ∥ (∃ λ g → ∀ n → [ g ]→ n ≡ f n) ∥  ↔⟨ TruncP.∥∥-cong (∃-cong λ _ → Eq.extensionality-isomorphism ext) ⟩□
        ∥ (∃ λ g → [ g ]→ ≡ f) ∥            □

  open Dummy

  from₁ : ∀ f → [_]→ ⁻¹ f → ℕ→/-comm-to ⁻¹ f
  from₁ f (g , [g]→≡f) =
      [ g ]
    , (ℕ→/-comm-to [ g ]  ≡⟨⟩
       [ g ]→             ≡⟨ [g]→≡f ⟩∎
       f                  ∎)

  from₁-constant : ∀ f → Constant (from₁ f)
  from₁-constant f (g₁ , [g₁]→≡f) (g₂ , [g₂]→≡f) =
                                             $⟨ (λ n → cong (_$ n) (
        [ g₁ ]→                                    ≡⟨ [g₁]→≡f ⟩
        f                                          ≡⟨ sym [g₂]→≡f ⟩∎
        [ g₂ ]→                                    ∎)) ⟩

    (∀ n → [ g₁ ]→ n ≡ [ g₂ ]→ n)            ↔⟨⟩

    (∀ n → [ g₁ n ] ≡ [ g₂ n ])              ↔⟨ ∀-cong ext (λ _ → inverse $ related≃[equal] prop-ext R-equiv R-prop) ⟩

    (∀ n → R (g₁ n) (g₂ n))                  ↔⟨⟩

    (ℕ →ᴾ R) g₁ g₂                           ↝⟨ []-respects-relation ⟩

    [ g₁ ] ≡ [ g₂ ]                          ↔⟨ ignore-propositional-component
                                                  (Π-closure ext 2 λ _ →
                                                   /-is-set λ _ _ → R-prop) ⟩□
    ([ g₁ ] , [g₁]→≡f) ≡ ([ g₂ ] , [g₂]→≡f)  □

  from₂ : Unit → ∀ f → ∥ [_]→ ⁻¹ f ∥ → ℕ→/-comm-to ⁻¹ f
  from₂ unit f =
    _≃_.to
      (TruncP.constant-function≃∥inhabited∥⇒inhabited
         (Σ-closure 2
            (/-is-set λ _ _ →
               →ᴾ-preserves-Is-proposition R ext R-prop) λ _ →
            mono₁ 1 (Π-closure ext 2 (λ _ → /-is-set λ _ _ → R-prop))))
      (from₁ f , from₁-constant f)

  unblock-from₂ : ∀ x f p → from₂ x f ∣ p ∣ ≡ from₁ f p
  unblock-from₂ unit _ _ = refl _

  abstract

    from₃ : Unit → (f : ℕ → A / R) → ℕ→/-comm-to ⁻¹ f
    from₃ x f = from₂ x f ([]→-surjective f)

    from : Unit → (ℕ → A / R) → (ℕ → A) / (ℕ →ᴾ R)
    from x f = proj₁ (from₃ x f)

    to∘from : ∀ x f → ℕ→/-comm-to (from x f) ≡ f
    to∘from x f = proj₂ (from₃ x f)

    from∘to : ∀ x f → from x (ℕ→/-comm-to f) ≡ f
    from∘to x = elim-prop λ where
      .[]ʳ f →
        from x (ℕ→/-comm-to [ f ])                      ≡⟨⟩
        proj₁ (from₂ x [ f ]→ ([]→-surjective [ f ]→))  ≡⟨ cong (proj₁ ∘ from₂ x [ f ]→) $ TruncP.truncation-is-proposition _ _ ⟩
        proj₁ (from₂ x [ f ]→ ∣ f , refl _ ∣)           ≡⟨ cong proj₁ $ unblock-from₂ x _ (f , refl _) ⟩
        proj₁ (from₁ [ f ]→ (f , refl _))               ≡⟨⟩
        [ f ]                                           ∎
      .is-propositionʳ _ →
        /-is-set λ _ _ →
          →ᴾ-preserves-Is-proposition R ext R-prop

------------------------------------------------------------------------
-- Quotient-like eliminators

-- If there is a split surjection from a quotient type to some other
-- type, then one can construct a quotient-like eliminator for the
-- other type.
--
-- This kind of construction is used in "Quotienting the Delay Monad
-- by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

↠-eliminator :
  (surj : A / R ↠ B)
  (P : B → Type p)
  (p-[] : ∀ x → P (_↠_.to surj [ x ])) →
  (∀ {x y} (r : R x y) →
   subst P (cong (_↠_.to surj) ([]-respects-relation r)) (p-[] x) ≡
   p-[] y) →
  ((∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x)) →
  ∀ x → P x
↠-eliminator surj P p-[] ok P-set x =
  subst P (_↠_.right-inverse-of surj x) p′
  where
  p′ : P (_↠_.to surj (_↠_.from surj x))
  p′ = elim
    (λ where
       .[]ʳ                                     → p-[]
       .[]-respects-relationʳ {x = x} {y = y} r →
         subst (P ∘ _↠_.to surj) ([]-respects-relation r) (p-[] x)       ≡⟨ subst-∘ P (_↠_.to surj) ([]-respects-relation r) ⟩
         subst P (cong (_↠_.to surj) ([]-respects-relation r)) (p-[] x)  ≡⟨ ok r ⟩∎
         p-[] y                                                          ∎
       .is-setʳ prop _ → P-set prop _)
    (_↠_.from surj x)

-- The eliminator "computes" in the "right" way for elements that
-- satisfy a certain property, assuming that the quotient relation is
-- pointwise propositional.

↠-eliminator-[] :
  ∀ (surj : A / R ↠ B)
  (P : B → Type p)
  (p-[] : ∀ x → P (_↠_.to surj [ x ]))
  (ok : ∀ {x y} (r : R x y) →
        subst P (cong (_↠_.to surj) ([]-respects-relation r)) (p-[] x) ≡
        p-[] y)
  (P-set : (∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x))
  x →
  (∀ {x y} → Is-proposition (R x y)) →
  _↠_.from surj (_↠_.to surj [ x ]) ≡ [ x ] →
  ↠-eliminator surj P p-[] ok P-set (_↠_.to surj [ x ]) ≡ p-[] x
↠-eliminator-[] {R = R} surj P p-[] ok P-set x R-prop hyp =
  subst P (_↠_.right-inverse-of surj (_↠_.to surj [ x ]))
    (elim e′ (_↠_.from surj (_↠_.to surj [ x ])))          ≡⟨ cong (λ p → subst P p (elim e′ _)) $
                                                              H.respects-surjection surj 2 (/-is-set λ _ _ → R-prop)
                                                                (_↠_.right-inverse-of surj (_↠_.to surj [ x ]))
                                                                (cong (_↠_.to surj) hyp) ⟩
  subst P (cong (_↠_.to surj) hyp)
    (elim e′ (_↠_.from surj (_↠_.to surj [ x ])))          ≡⟨ D.elim
                                                                (λ {x y} p → subst P (cong (_↠_.to surj) p) (elim e′ x) ≡ elim e′ y)
                                                                (λ y →
      subst P (cong (_↠_.to surj) (refl _)) (elim e′ y)            ≡⟨ cong (λ p → subst P p (elim e′ _)) $ cong-refl (_↠_.to surj) ⟩
      subst P (refl _) (elim e′ y)                                 ≡⟨ subst-refl P _ ⟩∎
      elim e′ y                                                    ∎)
                                                                hyp ⟩
  elim e′ [ x ]                                            ≡⟨⟩

  p-[] x                                                   ∎
  where
  e′ = _

-- If there is a bijection from a quotient type to some other type,
-- then one can also construct a quotient-like eliminator for the
-- other type.

↔-eliminator :
  (bij : A / R ↔ B)
  (P : B → Type p)
  (p-[] : ∀ x → P (_↔_.to bij [ x ])) →
  (∀ {x y} (r : R x y) →
   subst P (cong (_↔_.to bij) ([]-respects-relation r)) (p-[] x) ≡
   p-[] y) →
  ((∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x)) →
  ∀ x → P x
↔-eliminator bij = ↠-eliminator (_↔_.surjection bij)

-- This latter eliminator always "computes" in the "right" way,
-- assuming that the quotient relation is pointwise propositional.

↔-eliminator-[] :
  ∀ (bij : A / R ↔ B)
  (P : B → Type p)
  (p-[] : ∀ x → P (_↔_.to bij [ x ]))
  (ok : ∀ {x y} (r : R x y) →
        subst P (cong (_↔_.to bij) ([]-respects-relation r)) (p-[] x) ≡
        p-[] y)
  (P-set : (∀ x y → Is-proposition (R x y)) → ∀ x → Is-set (P x)) x →
  (∀ {x y} → Is-proposition (R x y)) →
  ↔-eliminator bij P p-[] ok P-set (_↔_.to bij [ x ]) ≡ p-[] x
↔-eliminator-[] bij P p-[] ok P-set x R-prop =
  ↠-eliminator-[] (_↔_.surjection bij) P p-[] ok P-set x
    R-prop
    (_↔_.left-inverse-of bij [ x ])

-- A quotient-like eliminator for functions of type ℕ → A / R, where R
-- is a propositional equivalence relation. Defined using countable
-- choice and propositional extensionality.
--
-- This eliminator is taken from Corollary 1 in "Quotienting the Delay
-- Monad by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

ℕ→/-elim :
  {A : Type a} {R : A → A → Type r} →
  Axiom-of-countable-choice (a ⊔ r) →
  Propositional-extensionality r →
  Is-equivalence-relation R →
  (∀ {x y} → Is-proposition (R x y)) →
  (P : (ℕ → A / R) → Type p)
  (p-[] : ∀ f → P (λ n → [ f n ])) →
  (∀ {f g} (r : (ℕ →ᴾ R) f g) →
   subst P (cong ℕ→/-comm-to ([]-respects-relation r)) (p-[] f) ≡
   p-[] g) →
  (∀ f → Is-set (P f)) →
  ∀ f → P f
ℕ→/-elim cc prop-ext R-equiv R-prop P p-[] ok P-set =
  ↔-eliminator
    (ℕ→/-comm cc prop-ext R-equiv R-prop)
    P p-[] ok (λ _ → P-set)

-- The eliminator "computes" in the "right" way.

ℕ→/-elim-[] :
  ∀ {A : Type a} {R : A → A → Type r}
  (cc : Axiom-of-countable-choice (a ⊔ r))
  (prop-ext : Propositional-extensionality r)
  (R-equiv : Is-equivalence-relation R)
  (R-prop : ∀ {x y} → Is-proposition (R x y))
  (P : (ℕ → A / R) → Type p)
  (p-[] : ∀ f → P (λ n → [ f n ]))
  (ok : ∀ {f g} (r : (ℕ →ᴾ R) f g) →
        subst P (cong ℕ→/-comm-to ([]-respects-relation r)) (p-[] f) ≡
        p-[] g)
  (P-set : ∀ f → Is-set (P f)) f →
  ℕ→/-elim cc prop-ext R-equiv R-prop P p-[] ok P-set (λ n → [ f n ]) ≡
  p-[] f
ℕ→/-elim-[] {R = R} cc prop-ext R-equiv R-prop P p-[] ok P-set f =
  ↔-eliminator-[]
    (ℕ→/-comm cc prop-ext R-equiv R-prop)
    P p-[] ok (λ _ → P-set) f
    (→ᴾ-preserves-Is-proposition R ext R-prop)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module List.Sorted  {A : Set}(_≤_ : A → A → Set) where

open import Data.List

data Sorted :  List A → Set where
  nils : Sorted []
  singls : (x : A)
                   → Sorted [ x ]
  conss : {x y : A}{xs : List A}
                   → x ≤ y
                   → Sorted (y ∷ xs)
                   → Sorted (x ∷ y ∷ xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import Cubical.HITs.TypeQuotients.Base public
open import Cubical.HITs.TypeQuotients.Properties public

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{-

Descriptor language for easily defining structures

-}
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.Macro where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.SIP
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Sigma
open import Cubical.Data.Maybe

open import Cubical.Structures.Constant
open import Cubical.Structures.Function
open import Cubical.Structures.Maybe
open import Cubical.Structures.Parameterized
open import Cubical.Structures.Pointed
open import Cubical.Structures.Product

data TranspDesc (ℓ : Level) : Typeω where
  -- constant structure: X ↦ A
  constant : ∀ {ℓ'} (A : Type ℓ') → TranspDesc ℓ
  -- pointed structure: X ↦ X
  var : TranspDesc ℓ
  -- product of structures S,T : X ↦ (S X × T X)
  _,_ : (d₀ : TranspDesc ℓ) (d₁ : TranspDesc ℓ) → TranspDesc ℓ
  -- functions between structures S,T: X ↦ (S X → T X)
  function : (d₀ : TranspDesc ℓ) (d₁ : TranspDesc ℓ) → TranspDesc ℓ
  -- Maybe on a structure S: X ↦ Maybe (S X)
  maybe : TranspDesc ℓ → TranspDesc ℓ
  -- arbitrary transport structure
  foreign : ∀ {ℓ'} {S : Type ℓ → Type ℓ'} (α : EquivAction S) → TransportStr α → TranspDesc ℓ

data Desc (ℓ : Level) : Typeω where
  -- constant structure: X ↦ A
  constant : ∀ {ℓ'} (A : Type ℓ') → Desc ℓ
  -- pointed structure: X ↦ X
  var : Desc ℓ
  -- product of structures S,T : X ↦ (S X × T X)
  _,_ : (d₀ : Desc ℓ) (d₁ : Desc ℓ) → Desc ℓ
  -- functions between structures S,T : X ↦ (S X → T X)
  function : (d₀ : Desc ℓ) (d₁ : Desc ℓ) → Desc ℓ
  -- functions between structures S,T where S is functorial : X ↦ (S X → T X)
  function+ : (d₀ : TranspDesc ℓ) (d₁ : Desc ℓ) → Desc ℓ
  -- Maybe on a structure S: X ↦ Maybe (S X)
  maybe : Desc ℓ → Desc ℓ
  -- univalent structure from transport structure
  transpDesc : TranspDesc ℓ → Desc ℓ
  -- arbitrary univalent notion of structure
  foreign : ∀ {ℓ' ℓ''} {S : Type ℓ → Type ℓ'} (ι : StrEquiv S ℓ'') → UnivalentStr S ι → Desc ℓ

infixr 4 _,_

{- Transport structures -}

transpMacroLevel : ∀ {ℓ} → TranspDesc ℓ → Level
transpMacroLevel (constant {ℓ'} x) = ℓ'
transpMacroLevel {ℓ} var = ℓ
transpMacroLevel {ℓ} (d₀ , d₁) = ℓ-max (transpMacroLevel d₀) (transpMacroLevel d₁)
transpMacroLevel (function d₀ d₁) = ℓ-max (transpMacroLevel d₀) (transpMacroLevel d₁)
transpMacroLevel (maybe d) = transpMacroLevel d
transpMacroLevel (foreign {ℓ'} α τ) = ℓ'

-- Structure defined by a transport descriptor
TranspMacroStructure : ∀ {ℓ} (d : TranspDesc ℓ) → Type ℓ → Type (transpMacroLevel d)
TranspMacroStructure (constant A) X = A
TranspMacroStructure var X = X
TranspMacroStructure (d₀ , d₁) X = TranspMacroStructure d₀ X × TranspMacroStructure d₁ X
TranspMacroStructure (function d₀ d₁) X = TranspMacroStructure d₀ X → TranspMacroStructure d₁ X
TranspMacroStructure (maybe d) = MaybeStructure (TranspMacroStructure d)
TranspMacroStructure (foreign {S = S} α τ) = S

-- Action defined by a transport descriptor
transpMacroAction : ∀ {ℓ} (d : TranspDesc ℓ) → EquivAction (TranspMacroStructure d)
transpMacroAction (constant A) = constantEquivAction A
transpMacroAction var = pointedEquivAction
transpMacroAction (d₀ , d₁) = productEquivAction (transpMacroAction d₀) (transpMacroAction d₁)
transpMacroAction (function d₀ d₁) =
  functionEquivAction (transpMacroAction d₀) (transpMacroAction d₁)
transpMacroAction (maybe d) = maybeEquivAction (transpMacroAction d)
transpMacroAction (foreign α _) = α

-- Action defines a transport structure
transpMacroTransportStr : ∀ {ℓ} (d : TranspDesc ℓ) → TransportStr (transpMacroAction d)
transpMacroTransportStr (constant A) = constantTransportStr A
transpMacroTransportStr var = pointedTransportStr
transpMacroTransportStr (d₀ , d₁) =
  productTransportStr
    (transpMacroAction d₀) (transpMacroTransportStr d₀)
    (transpMacroAction d₁) (transpMacroTransportStr d₁)
transpMacroTransportStr (function d₀ d₁) =
  functionTransportStr
    (transpMacroAction d₀) (transpMacroTransportStr d₀)
    (transpMacroAction d₁) (transpMacroTransportStr d₁)
transpMacroTransportStr (maybe d) =
  maybeTransportStr (transpMacroAction d) (transpMacroTransportStr d)
transpMacroTransportStr (foreign α τ) = τ

{- General structures -}

macroStrLevel : ∀ {ℓ} → Desc ℓ → Level
macroStrLevel (constant {ℓ'} x) = ℓ'
macroStrLevel {ℓ} var = ℓ
macroStrLevel {ℓ} (d₀ , d₁) = ℓ-max (macroStrLevel d₀) (macroStrLevel d₁)
macroStrLevel {ℓ} (function+ d₀ d₁) = ℓ-max (transpMacroLevel d₀) (macroStrLevel d₁)
macroStrLevel (function d₀ d₁) = ℓ-max (macroStrLevel d₀) (macroStrLevel d₁)
macroStrLevel (maybe d) = macroStrLevel d
macroStrLevel (transpDesc d) = transpMacroLevel d
macroStrLevel (foreign {ℓ'} _ _) = ℓ'

macroEquivLevel : ∀ {ℓ} → Desc ℓ → Level
macroEquivLevel (constant {ℓ'} x) = ℓ'
macroEquivLevel {ℓ} var = ℓ
macroEquivLevel (d₀ , d₁) = ℓ-max (macroEquivLevel d₀) (macroEquivLevel d₁)
macroEquivLevel {ℓ} (function+ d₀ d₁) = ℓ-max (transpMacroLevel d₀) (macroEquivLevel d₁)
macroEquivLevel (function d₀ d₁) = ℓ-max (macroStrLevel d₀) (ℓ-max (macroEquivLevel d₀) (macroEquivLevel d₁))
macroEquivLevel (maybe d) = macroEquivLevel d
macroEquivLevel (transpDesc d) = transpMacroLevel d
macroEquivLevel (foreign {ℓ'' = ℓ''} _ _) = ℓ''

-- Structure defined by a descriptor
MacroStructure : ∀ {ℓ} (d : Desc ℓ) → Type ℓ → Type (macroStrLevel d)
MacroStructure (constant A) X = A
MacroStructure var X = X
MacroStructure (d₀ , d₁) X = MacroStructure d₀ X × MacroStructure d₁ X
MacroStructure (function+ d₀ d₁) X = TranspMacroStructure d₀ X → MacroStructure d₁ X
MacroStructure (function d₀ d₁) X = MacroStructure d₀ X → MacroStructure d₁ X
MacroStructure (maybe d) = MaybeStructure (MacroStructure d)
MacroStructure (transpDesc d) = TranspMacroStructure d
MacroStructure (foreign {S = S} _ _) = S

-- Notion of structured equivalence defined by a descriptor
MacroEquivStr : ∀ {ℓ} → (d : Desc ℓ) → StrEquiv {ℓ} (MacroStructure d) (macroEquivLevel d)
MacroEquivStr (constant A) = ConstantEquivStr A
MacroEquivStr var = PointedEquivStr
MacroEquivStr (d₀ , d₁) = ProductEquivStr (MacroEquivStr d₀) (MacroEquivStr d₁)
MacroEquivStr (function+ d₀ d₁) = FunctionEquivStr+ (transpMacroAction d₀) (MacroEquivStr d₁)
MacroEquivStr (function d₀ d₁) = FunctionEquivStr (MacroEquivStr d₀) (MacroEquivStr d₁)
MacroEquivStr (maybe d) = MaybeEquivStr (MacroEquivStr d)
MacroEquivStr (transpDesc d) = EquivAction→StrEquiv (transpMacroAction d)
MacroEquivStr (foreign ι _) = ι

-- Proof that structure induced by descriptor is univalent
MacroUnivalentStr : ∀ {ℓ} → (d : Desc ℓ) → UnivalentStr (MacroStructure d) (MacroEquivStr d)
MacroUnivalentStr (constant A) = constantUnivalentStr A
MacroUnivalentStr var = pointedUnivalentStr
MacroUnivalentStr (d₀ , d₁) =
  productUnivalentStr
    (MacroEquivStr d₀) (MacroUnivalentStr d₀)
    (MacroEquivStr d₁) (MacroUnivalentStr d₁)
MacroUnivalentStr (function+ d₀ d₁) =
  functionUnivalentStr+
    (transpMacroAction d₀) (transpMacroTransportStr d₀)
    (MacroEquivStr d₁) (MacroUnivalentStr d₁)
MacroUnivalentStr (function d₀ d₁) =
  functionUnivalentStr
    (MacroEquivStr d₀) (MacroUnivalentStr d₀)
    (MacroEquivStr d₁) (MacroUnivalentStr d₁)
MacroUnivalentStr (maybe d) = maybeUnivalentStr (MacroEquivStr d) (MacroUnivalentStr d)
MacroUnivalentStr (transpDesc d) =
  TransportStr→UnivalentStr (transpMacroAction d) (transpMacroTransportStr d)
MacroUnivalentStr (foreign _ θ) = θ

-- Module for easy importing
module Macro ℓ (d : Desc ℓ) where

  structure = MacroStructure d
  equiv = MacroEquivStr d
  univalent = MacroUnivalentStr d

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- Lists where all elements satisfy a given property
------------------------------------------------------------------------

module Data.List.All where

open import Data.Function
open import Data.List as List hiding (map; all)
open import Data.List.Any as Any using (here; there)
open Any.Membership-≡ using (_∈_; _⊆_)
open import Data.Product as Prod using (_,_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)
open import Relation.Binary.PropositionalEquality

-- All P xs means that all elements in xs satisfy P.

infixr 5 _∷_

data All {A} (P : A → Set) : List A → Set where
  []  : All P []
  _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs)

head : ∀ {A} {P : A → Set} {x xs} → All P (x ∷ xs) → P x
head (px ∷ pxs) = px

tail : ∀ {A} {P : A → Set} {x xs} → All P (x ∷ xs) → All P xs
tail (px ∷ pxs) = pxs

lookup : ∀ {A} {P : A → Set} {xs} → All P xs → (∀ {x} → x ∈ xs → P x)
lookup []         ()
lookup (px ∷ pxs) (here refl)  = px
lookup (px ∷ pxs) (there x∈xs) = lookup pxs x∈xs

tabulate : ∀ {A} {P : A → Set} {xs} → (∀ {x} → x ∈ xs → P x) → All P xs
tabulate {xs = []}     hyp = []
tabulate {xs = x ∷ xs} hyp = hyp (here refl) ∷ tabulate (hyp ∘ there)

map : ∀ {A} {P Q : Pred A} → P ⋐ Q → All P ⋐ All Q
map g []         = []
map g (px ∷ pxs) = g px ∷ map g pxs

all : ∀ {A} {P : A → Set} →
      (∀ x → Dec (P x)) → (xs : List A) → Dec (All P xs)
all p []       = yes []
all p (x ∷ xs) with p x
all p (x ∷ xs) | yes px = Dec.map (_∷_ px , tail) (all p xs)
all p (x ∷ xs) | no ¬px = no (¬px ∘ head)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma

data Unit : Set where
  unit : Unit

data Empty : Set where

qq : ∀ {a} {A : Set a} → A → Term → TC _
qq t hole = withNormalisation true do
  `t ← quoteTC t
  ``t ← quoteTC `t
  unify hole ``t

macro

  qU  = qq {A = Unit → Set → Set}
  qE  = qq {A = Empty → Set → Set}
  qA  = qq {A = Set → Set}

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

pattern vArg x = arg (arg-info visible relevant) x
pattern [_] x = x ∷ []

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

mkArgs : List Nat → List (Arg Term)
mkArgs = map λ i → vArg (var i [])

unit,X=>_∙_ : Nat → List Nat → Term
unit,X=> n ∙ args =
  pat-lam [ clause [ "X" , vArg (agda-sort (lit 0)) ]
                   (vArg (con (quote unit) []) ∷ vArg (var 0) ∷ [])
                   (var n []) ]
          (mkArgs args)

abs,X=>∙_ : List Nat → Term
abs,X=>∙ is = pat-lam [ absurd-clause ( ("()" , vArg (def (quote Empty) [])) ∷  ("X" , vArg (agda-sort (lit 0))) ∷ [])
                                      (vArg absurd ∷ vArg (var 0) ∷ []) ]
                      (mkArgs is)

abs=>∙_ : List Nat → Term
abs=>∙ is = pat-lam [ absurd-clause [ "()" , vArg (def (quote Empty) []) ] (vArg absurd ∷ []) ]
                    (mkArgs is)

_ : qU (λ { unit X → X }) ≡ unit,X=> 0 ∙ []
_ = refl

_ : (B : Set) → qU (λ { unit X → B }) ≡ unit,X=> 1 ∙ []
_ = λ _ → refl

_ : qE (λ { () X }) ≡ abs,X=>∙ []
_ = refl

_ : (B : Set) → qE (λ { () X }) ≡ abs,X=>∙ []
_ = λ _ → refl

_ : (u : Unit) → qA (case u of λ { unit X → X }) ≡ (unit,X=> 0 ∙ [ 0 ])
_ = λ _ → refl

_ : (B : Set) (u : Unit) → qA (case u of λ { unit X → B }) ≡ unit,X=> 2 ∙ [ 0 ]
_ = λ _ _ → refl

_ : (B : Set) (e : Empty) → qA (case e of λ { () X }) ≡ abs,X=>∙ [ 0 ]
_ = λ _ _ → refl

_ : qE (λ ()) ≡ abs=>∙ []
_ = refl

_ : (B : Set) → qE (λ ()) ≡ abs=>∙ []
_ = λ _ → refl

_ : (B : Set) (e : Empty) → qA (case e of λ ()) ≡ abs=>∙ [ 0 ]
_ = λ _ _ → refl

module _ (A : Set) where

  _ : qU (λ { unit X → X }) ≡ unit,X=> 0 ∙ []
  _ = refl

  _ : (B : Set) → qU (λ { unit X → B }) ≡ unit,X=> 1 ∙ []
  _ = λ _ → refl

  _ : qE (λ { () X }) ≡ abs,X=>∙ []
  _ = refl

  _ : (u : Unit) → qA (case u of λ { unit X → X }) ≡ (unit,X=> 0 ∙ [ 0 ])
  _ = λ _ → refl

  _ : (B : Set) (u : Unit) → qA (case u of λ { unit X → B }) ≡ unit,X=> 2 ∙ [ 0 ]
  _ = λ _ _ → refl

  _ : (B : Set) (e : Empty) → qA (case e of λ { () X }) ≡ abs,X=>∙ [ 0 ]
  _ = λ _ _ → refl

  _ : qE (λ ()) ≡ abs=>∙ []
  _ = refl

  _ : (B : Set) → qE (λ ()) ≡ abs=>∙ []
  _ = λ _ → refl

  _ : (B : Set) (e : Empty) → qA (case e of λ ()) ≡ abs=>∙ [ 0 ]
  _ = λ _ _ → refl

max_forks_repo_name: shlevy/agda


text:
module API.Theorems where

open import Algebra
open import Algebra.Theorems
open import API
open import Prelude
open import Reasoning

-- vertices [x] == vertex x
vertices-vertex : ∀ {A} {x : A} -> vertices [ x ] ≡ vertex x
vertices-vertex = +identity >> reflexivity

-- edge x y == clique [x, y]
edge-clique : ∀ {A} {x y : A} -> edge x y ≡ clique (x :: [ y ])
edge-clique = symmetry (R *right-identity)

-- vertices xs ⊆ clique xs
vertices-clique : ∀ {A} {xs : List A} -> vertices xs ⊆ clique xs
vertices-clique {_} {[]}     = ⊆reflexivity
vertices-clique {a} {_ :: t} = ⊆transitivity (⊆right-monotony (vertices-clique {a} {t})) ⊆connect

-- clique (xs ++ ys) == connect (clique xs) (clique ys)
connect-clique : ∀ {A} {xs ys : List A} -> clique (xs ++ ys) ≡ connect (clique xs) (clique ys)
connect-clique {_} {[]}     = symmetry *left-identity
connect-clique {a} {_ :: t} = R (connect-clique {a} {t}) >> *associativity

max_stars_repo_name: asr/alga

max_issues_repo_name: asr/alga

max_forks_repo_name: asr/alga


text:
module LC.Reduction where

open import LC.Base
open import LC.Subst

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Nullary

-- β-reduction
infix 3 _β→_
data _β→_ : Term → Term → Set where

  β-ƛ-∙ : ∀ {M N} → ((ƛ M) ∙ N) β→ (M [ N ])

  β-ƛ : ∀ {M N} → M β→ N → ƛ M β→ ƛ N

  β-∙-l : ∀ {L M N} → M β→ N → M ∙ L β→ N ∙ L

  β-∙-r : ∀ {L M N} → M β→ N → L ∙ M β→ L ∙ N

open import Relation.Binary.Construct.Closure.ReflexiveTransitive

infix  2 _β→*_
_β→*_ : Term → Term → Set
_β→*_ = Star _β→_
{-# DISPLAY Star _β→_ = _β→*_ #-}

open import Relation.Binary.PropositionalEquality hiding ([_]; preorder)

≡⇒β→* : ∀ {M N} → M ≡ N → M β→* N
≡⇒β→* refl = ε

cong-var : ∀ {x y} → x ≡ y → var x β→* var y
cong-var {x} {y} refl = ε

cong-ƛ : {M N : Term} → M β→* N → ƛ M β→* ƛ N
cong-ƛ = gmap _ β-ƛ

cong-∙-l : {L M N : Term} → M β→* N → M ∙ L β→* N ∙ L
cong-∙-l = gmap _ β-∙-l

cong-∙-r : {L M N : Term} → M β→* N → L ∙ M β→* L ∙ N
cong-∙-r = gmap _ β-∙-r

cong-∙ : {M M' N N' : Term} → M β→* M' → N β→* N' → M ∙ N β→* M' ∙ N'
cong-∙ M→M' N→N' = (cong-∙-l M→M') ◅◅ (cong-∙-r N→N')

open import LC.Subst.Term

cong-lift : {n i : ℕ} {M N : Term} → M β→ N → lift n i M β→* lift n i N
cong-lift (β-ƛ M→N)        = cong-ƛ (cong-lift M→N)
cong-lift (β-ƛ-∙ {M} {N})  = β-ƛ-∙ ◅ ≡⇒β→* (lemma M N)
cong-lift (β-∙-l M→N)      = cong-∙-l (cong-lift M→N)
cong-lift (β-∙-r M→N)      = cong-∙-r (cong-lift M→N)

cong-[]-r : ∀ L {M N i} → M β→ N → L [ M / i ] β→* L [ N / i ]
cong-[]-r (var x) {M} {N} {i} M→N with match x i
... | Under _ = ε
... | Exact _ = cong-lift M→N
... | Above _ _ = ε
cong-[]-r (ƛ L)   M→N = cong-ƛ (cong-[]-r L M→N)
cong-[]-r (K ∙ L) M→N = cong-∙ (cong-[]-r K M→N) (cong-[]-r L M→N)

cong-[]-l : ∀ {M N L i} → M β→ N → M [ L / i ] β→* N [ L / i ]
cong-[]-l {ƛ M}                 (β-ƛ M→N)   = cong-ƛ   (cong-[]-l M→N)
cong-[]-l {.(ƛ K) ∙ M} {L = L}  (β-ƛ-∙ {K}) = β-ƛ-∙ ◅ ≡⇒β→* (subst-lemma K M L)
cong-[]-l {K ∙ M}               (β-∙-l M→N) = cong-∙-l (cong-[]-l M→N)
cong-[]-l {K ∙ M}               (β-∙-r M→N) = cong-∙-r (cong-[]-l M→N)

cong-[] : {M M' N N' : Term} → M β→* M' → N β→* N' → M [ N ] β→* M' [ N' ]
cong-[] {M} ε            ε            = ε
cong-[] {M} {N = L} {N'} ε (_◅_ {j = N} L→N N→N') = M[L]→M[N] ◅◅ M[N]→M[N']
    where
        M[L]→M[N] : M [ L ] β→* M [ N ]
        M[L]→M[N] = cong-[]-r M L→N

        M[N]→M[N'] : M [ N ] β→* M [ N' ]
        M[N]→M[N'] = cong-[] {M} ε N→N'
cong-[] {M} (K→M ◅ M→M') N→N' = cong-[]-l K→M ◅◅ cong-[] M→M' N→N'

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>
--
-- This module contains definitions that are fundamental and/or used
-- everywhere.

module Core where

open import Agda.Builtin.Equality public
  renaming (refl to ≡-refl)
  using (_≡_)
open import Agda.Builtin.FromNat public
open import Agda.Builtin.FromNeg public
open import Agda.Builtin.FromString public
open import Agda.Builtin.Unit using (⊤; tt) public
open import Agda.Primitive using (Level; lsuc; lzero; _⊔_) public

-- An empty type (or a false hypothesis).

data ⊥ : Set where

-- Dependent sums (or existential quantification).

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

infixr 4 _,_
infixr 0 _because_ _because:_

∃ : ∀ {a b} {A : Set a} (B : A → Set b) → Set (a ⊔ b)
∃ = Σ _

_because_ : ∀ {a b} {A : Set a} {B : A → Set b} → (x : A) → B x → Σ A B
_because_ = _,_

_because:_ : ∀ {a b} {A : Set a} {B : A → Set b} → (x : A) → B x → Σ A B
_because:_ = _,_

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

infixr 7 _×_

-- Tagged unions.

data Either {a} {b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  Left  : A → Either A B
  Right : B → Either A B

-- Equivalence relations.

record Equiv {a r} (A : Set a) : Set (a ⊔ lsuc r) where
  field
    _≈_   : A → A → Set r
    refl  : ∀ {x} → x ≈ x
    sym   : ∀ {x y} → x ≈ y → y ≈ x
    trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z

  infix 4 _≈_

  -- Helper functions for equational reasoning.
  begin_ : ∀ {x y} → x ≈ y → x ≈ y
  begin_ p = p

  _≈[_]_ : ∀ x {y z} → x ≈ y → y ≈ z → x ≈ z
  _ ≈[ x≈y ] y≈z = trans x≈y y≈z

  _≈[]_ : ∀ x {y} → x ≈ y → x ≈ y
  _ ≈[] p = p

  _qed : ∀ (x : A) → x ≈ x
  _qed _ = refl

  infix  1 begin_
  infixr 2 _≈[_]_ _≈[]_
  infix  3 _qed

PropEq : ∀ {a} → (A : Set a) → Equiv A
PropEq A =
  record {
    _≈_ = _≡_;
    refl = ≡-refl;
    sym = sym';
    trans = trans'
  }

  where
  sym' : ∀ {x y} → x ≡ y → y ≡ x
  sym' ≡-refl = ≡-refl

  trans' : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z
  trans' ≡-refl q = q

module PropEq {a} {A : Set a} = Equiv (PropEq A)

FuncEq : ∀ {a b} (A : Set a) (B : Set b) → Equiv (A → B)
FuncEq A B =
  record {
    _≈_ = λ f g → ∀ x → f x ≡ g x;
    refl = λ _ → ≡-refl;
    sym = λ p x → PropEq.sym (p x);
    trans = λ p q x → PropEq.trans (p x) (q x)
  }

module FuncEq {a b} {A : Set a} {B : Set b} = Equiv (FuncEq A B)

cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong _ ≡-refl = ≡-refl

cong2 :
  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
    (f : A → B → C)
  → ∀ {x1 x2 : A} {y1 y2 : B}
    → x1 ≡ x2
    → y1 ≡ y2
    → f x1 y1 ≡ f x2 y2
cong2 _ ≡-refl ≡-refl = ≡-refl

-- Partial orders.

record PartialOrder {a re rl} (A : Set a) : Set (a ⊔ lsuc (re ⊔ rl)) where
  field Eq : Equiv {r = re} A
  module ≈ = Equiv Eq
  open ≈ public using (_≈_)

  field
    _≤_     : (x : A) → (y : A) → Set rl
    antisym : ∀ {x y} → x ≤ y → y ≤ x → x ≈ y
    refl'   : ∀ {x y} → x ≈ y → x ≤ y
    trans   : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z

  infix 4 _≤_

  refl : ∀ {x} → x ≤ x
  refl = refl' ≈.refl

  -- Helper functions for transitivity reasoning.
  begin_ : ∀ {x y} → x ≤ y → x ≤ y
  begin_ p = p

  _≤[_]_ : ∀ x {y z} → x ≤ y → y ≤ z → x ≤ z
  _ ≤[ x≤y ] y≤z = trans x≤y y≤z

  _≤[]_ : ∀ x {y} → x ≤ y → x ≤ y
  _ ≤[] p = p

  _qed : ∀ (x : A) → x ≤ x
  _qed _ = refl

  infix  1 begin_
  infixr 2 _≤[_]_ _≤[]_
  infix  3 _qed

-- Total orders.

record TotalOrder {a re rl} (A : Set a) : Set (a ⊔ lsuc (re ⊔ rl)) where
  field partialOrder : PartialOrder {a} {re} {rl} A
  open PartialOrder partialOrder public

  field
    total : ∀ x y → Either (x ≤ y) (y ≤ x)

-- Low-priority function application.

_$_ : ∀ {a} {A : Set a} → A → A
_$_ f = f

infixr 0 _$_

-- Given two predicates, this is the predicate that requires both.

_and_ : ∀ {a r1 r2} {A : Set a} → (A → Set r1) → (A → Set r2) → A → Set (r1 ⊔ r2)
(P and Q) x = P x × Q x

infixr 6 _and_

-- Use instance resolution to find a value of the target type.

it : ∀ {a} {A : Set a} {{_ : A}} → A
it {{x}} = x

-- Not.

not : ∀ {a} → Set a → Set a
not A = A → ⊥

-- Given two predicates, this is the predicate that requires at least
-- one of them.

_or_ : ∀ {a r1 r2} {A : Set a} → (A → Set r1) → (A → Set r2) → A → Set (r1 ⊔ r2)
(P or Q) x = Either (P x) (Q x)

-- Values with inline type signatures.

the : ∀ {a} (A : Set a) → A → A
the _ x = x

-- Decidable properties.

data Decision {a} (P : Set a) : Set a where
  yes : (p : P) → Decision P
  no  : (np : not P) → Decision P

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
module Oscar.Data.Term.AlphaConversion.internal {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Data.Term FunctionName

open import Oscar.Data.Equality
open import Oscar.Data.Fin
open import Oscar.Data.Vec
open import Oscar.Function
open import Oscar.Relation

infixr 19 _◂_ _◂s_

mutual

  _◂_ : ∀ {m n} → m ⟨ Fin ⟩→ n → m ⟨ Term ⟩→ n
  _◂_ f (i 𝑥) = i (f 𝑥)
  _◂_ f leaf = leaf
  _◂_ f (τ₁ fork τ₂) = (f ◂ τ₁) fork (f ◂ τ₂)
  _◂_ f (function 𝑓 τs) = function 𝑓 (f ◂s τs)

  _◂s_ : ∀ {m n} → m ⟨ Fin ⟩→ n → ∀ {N} → m ⟨ Terms N ⟩→ n
  _◂s_ f [] = []
  _◂s_ f (τ ∷ τs) = f ◂ τ ∷ f ◂s τs

mutual

  ◂-identity : ∀ {m} (τ : Term m) → id ◂ τ ≡ τ
  ◂-identity (i _) = refl
  ◂-identity leaf = refl
  ◂-identity (τ₁ fork τ₂) rewrite ◂-identity τ₁ | ◂-identity τ₂ = refl
  ◂-identity (function 𝑓 τs) rewrite ◂s-identity τs = refl

  ◂s-identity : ∀ {N m} (τs : Terms N m) → id ◂s τs ≡ τs
  ◂s-identity [] = refl
  ◂s-identity (τ ∷ τs) rewrite ◂-identity τ | ◂s-identity τs = refl

mutual

  ◂-associativity : ∀ {l m n} (f : l ⟨ Fin ⟩→ m) (g : m ⟨ Fin ⟩→ n) → (τ : Term l) → (g ∘ f) ◂ τ ≡ g ◂ f ◂ τ
  ◂-associativity _ _ (i _) = refl
  ◂-associativity _ _ leaf = refl
  ◂-associativity f g (τ₁ fork τ₂) rewrite ◂-associativity f g τ₁ | ◂-associativity f g τ₂ = refl
  ◂-associativity f g (function 𝑓 τs) rewrite ◂s-associativity f g τs = refl

  ◂s-associativity : ∀ {l m n} (f : l ⟨ Fin ⟩→ m) (g : m ⟨ Fin ⟩→ n) → ∀ {N} (x : Terms N l) → (g ∘ f) ◂s x ≡ g ◂s f ◂s x
  ◂s-associativity _ _ [] = refl
  ◂s-associativity f g (τ ∷ τs) rewrite ◂-associativity f g τ | ◂s-associativity f g τs = refl

mutual

  ◂-extensionality : ∀ {m n} {f g : m ⟨ Fin ⟩→ n} → f ≡̇ g → f ◂_ ≡̇ g ◂_
  ◂-extensionality f≡̇g (i 𝑥) rewrite f≡̇g 𝑥 = refl
  ◂-extensionality f≡̇g leaf = refl
  ◂-extensionality f≡̇g (τ₁ fork τ₂) rewrite ◂-extensionality f≡̇g τ₁ | ◂-extensionality f≡̇g τ₂ = refl
  ◂-extensionality f≡̇g (function 𝑓 τs) rewrite ◂s-extensionality f≡̇g τs = refl

  ◂s-extensionality : ∀ {m n} {f g : m ⟨ Fin ⟩→ n} → f ≡̇ g → ∀ {N} → _◂s_ f {N} ≡̇ _◂s_ g {N}
  ◂s-extensionality _ [] = refl
  ◂s-extensionality f≡̇g (τ ∷ τs) rewrite ◂-extensionality f≡̇g τ | ◂s-extensionality f≡̇g τs = refl


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

open import LogicalFormulae
open import Numbers.Naturals.Definition

module Numbers.Naturals.Addition where

infix 15 _+N_
_+N_ : ℕ → ℕ → ℕ
zero +N y = y
succ x +N y = succ (x +N y)
{-# BUILTIN NATPLUS _+N_ #-}

addZeroRight : (x : ℕ) → (x +N zero) ≡ x
addZeroRight zero = refl
addZeroRight (succ x) rewrite addZeroRight x = refl

private
  succExtracts : (x y : ℕ) → (x +N succ y) ≡ (succ (x +N y))
  succExtracts zero y = refl
  succExtracts (succ x) y = applyEquality succ (succExtracts x y)

succCanMove : (x y : ℕ) → (x +N succ y) ≡ (succ x +N y)
succCanMove x y = transitivity (succExtracts x y) refl

additionNIsCommutative : (x y : ℕ) → (x +N y) ≡ (y +N x)
additionNIsCommutative zero y = equalityCommutative (addZeroRight y)
additionNIsCommutative (succ x) zero = transitivity (addZeroRight (succ x)) refl
additionNIsCommutative (succ x) (succ y) = transitivity refl (applyEquality succ (transitivity (succCanMove x y) (additionNIsCommutative (succ x) y)))

addingPreservesEqualityRight : {a b : ℕ} (c : ℕ) → (a ≡ b) → (a +N c ≡ b +N c)
addingPreservesEqualityRight {a} {b} c pr = applyEquality (λ n -> n +N c) pr
addingPreservesEqualityLeft : {a b : ℕ} (c : ℕ) → (a ≡ b) → (c +N a ≡ c +N b)
addingPreservesEqualityLeft {a} {b} c pr = applyEquality (λ n -> c +N n) pr

additionNIsAssociative : (a b c : ℕ) → ((a +N b) +N c) ≡ (a +N (b +N c))
additionNIsAssociative zero b c = refl
additionNIsAssociative (succ a) zero c = transitivity (transitivity (applyEquality (λ n → n +N c) (applyEquality succ (addZeroRight a))) refl) (transitivity refl refl)
additionNIsAssociative (succ a) (succ b) c = transitivity refl (transitivity refl (transitivity (applyEquality succ (additionNIsAssociative a (succ b) c)) refl))

succIsAddOne : (a : ℕ) → succ a ≡ a +N succ zero
succIsAddOne a = equalityCommutative (transitivity (additionNIsCommutative a (succ zero)) refl)

canSubtractFromEqualityRight : {a b c : ℕ} → (a +N b ≡ c +N b) → a ≡ c
canSubtractFromEqualityRight {a} {zero} {c} pr = transitivity (equalityCommutative (addZeroRight a)) (transitivity pr (addZeroRight c))
canSubtractFromEqualityRight {a} {succ b} {c} pr rewrite additionNIsCommutative a (succ b) | additionNIsCommutative c (succ b) | additionNIsCommutative b a | additionNIsCommutative b c = canSubtractFromEqualityRight {a} {b} {c} (succInjective pr)

canSubtractFromEqualityLeft : {a b c : ℕ} → (a +N b ≡ a +N c) → b ≡ c
canSubtractFromEqualityLeft {a} {b} {c} pr rewrite additionNIsCommutative a b | additionNIsCommutative a c = canSubtractFromEqualityRight {b} {a} {c} pr