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

open import LogicalFormulae
open import Setoids.Setoids
open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Naturals
open import Numbers.Integers.Integers
open import Groups.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Groups.Isomorphisms.Definition
open import Groups.Abelian.Definition
open import Groups.Subgroups.Definition
open import Groups.Lemmas
open import Groups.Groups
open import Rings.Definition
open import Rings.Lemmas
open import Fields.Fields
open import Sets.EquivalenceRelations

module Groups.Examples.ExampleSheet1 where

  {-
    Question 1: e is the unique solution of x^2 = x
  -}
  question1 : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} → (G : Group S _+_) → (x : A) → Setoid._∼_ S (x + x) x → Setoid._∼_ S x (Group.0G G)
  question1 {S = S} {_+_ = _+_} G x x+x=x = transitive (symmetric identRight) (transitive (+WellDefined reflexive (symmetric invRight)) (transitive +Associative (transitive (+WellDefined x+x=x reflexive) invRight)))
    where
      open Group G
      open Setoid S
      open Equivalence eq

  question1' : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} → (G : Group S _+_) → Setoid._∼_ S ((Group.0G G) + (Group.0G G)) (Group.0G G)
  question1' G = Group.identRight G

  {-
    Question 3. We can't talk about ℝ yet, so we'll just work in an arbitrary integral domain.
    Show that the collection of linear functions over a ring forms a group; is it abelian?
  -}

  record LinearFunction {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (F : Field R) : Set (a ⊔ b) where
    field
      xCoeff : A
      xCoeffNonzero : (Setoid._∼_ S xCoeff (Ring.0R R) → False)
      constant : A

  interpretLinearFunction : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {F : Field R} (f : LinearFunction F) → A → A
  interpretLinearFunction {_+_ = _+_} {_*_ = _*_} record { xCoeff = xCoeff ; xCoeffNonzero = xCoeffNonzero ; constant = constant } a = (xCoeff * a) + constant

  composeLinearFunctions : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {F : Field R} (f1 : LinearFunction F) (f2 : LinearFunction F) → LinearFunction F
  LinearFunction.xCoeff (composeLinearFunctions {_+_ = _+_} {_*_ = _*_} record { xCoeff = xCoeff1 ; xCoeffNonzero = xCoeffNonzero1 ; constant = constant1 } record { xCoeff = xCoeff2 ; xCoeffNonzero = xCoeffNonzero2 ; constant = constant2 }) = xCoeff1 * xCoeff2
  LinearFunction.xCoeffNonzero (composeLinearFunctions {S = S} {R = R} {F = F} record { xCoeff = xCoeff1 ; xCoeffNonzero = xCoeffNonzero1 ; constant = constant1 } record { xCoeff = xCoeff2 ; xCoeffNonzero = xCoeffNonzero2 ; constant = constant2 }) pr = xCoeffNonzero2 bad
    where
      open Setoid S
      open Ring R
      open Equivalence eq
      bad : Setoid._∼_ S xCoeff2 0R
      bad with Field.allInvertible F xCoeff1 xCoeffNonzero1
      ... | xinv , pr' = transitive (symmetric identIsIdent) (transitive (*WellDefined (symmetric pr') reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive pr) (Ring.timesZero R))))
  LinearFunction.constant (composeLinearFunctions {_+_ = _+_} {_*_ = _*_} record { xCoeff = xCoeff1 ; xCoeffNonzero = xCoeffNonzero1 ; constant = constant1 } record { xCoeff = xCoeff2 ; xCoeffNonzero = xCoeffNonzero2 ; constant = constant2 }) = (xCoeff1 * constant2) + constant1

  compositionIsCorrect : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {F : Field R} (f1 : LinearFunction F) (f2 : LinearFunction F) → {r : A} → Setoid._∼_ S (interpretLinearFunction (composeLinearFunctions f1 f2) r) (((interpretLinearFunction f1) ∘ (interpretLinearFunction f2)) r)
  compositionIsCorrect {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} record { xCoeff = xCoeff ; xCoeffNonzero = xCoeffNonzero ; constant = constant } record { xCoeff = xCoeff' ; xCoeffNonzero = xCoeffNonzero' ; constant = constant' } {r} = ans
    where
      open Setoid S
      open Ring R
      open Equivalence eq
      ans : (((xCoeff * xCoeff') * r) + ((xCoeff * constant') + constant)) ∼ (xCoeff * ((xCoeff' * r) + constant')) + constant
      ans = transitive (Group.+Associative additiveGroup) (Group.+WellDefined additiveGroup (transitive (Group.+WellDefined additiveGroup (symmetric (Ring.*Associative R)) reflexive) (symmetric (Ring.*DistributesOver+ R))) (reflexive {constant}))

  linearFunctionsSetoid : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : Field R) → Setoid (LinearFunction I)
  Setoid._∼_ (linearFunctionsSetoid {S = S} I) f1 f2 = ((LinearFunction.xCoeff f1) ∼ (LinearFunction.xCoeff f2)) && ((LinearFunction.constant f1) ∼ (LinearFunction.constant f2))
    where
      open Setoid S
  Equivalence.reflexive (Setoid.eq (linearFunctionsSetoid {S = S} I)) = Equivalence.reflexive (Setoid.eq S) ,, Equivalence.reflexive (Setoid.eq S)
  Equivalence.symmetric (Setoid.eq (linearFunctionsSetoid {S = S} I)) (fst ,, snd) = Equivalence.symmetric (Setoid.eq S) fst ,, Equivalence.symmetric (Setoid.eq S) snd
  Equivalence.transitive (Setoid.eq (linearFunctionsSetoid {S = S} I)) (fst1 ,, snd1) (fst2 ,, snd2) = Equivalence.transitive (Setoid.eq S) fst1 fst2 ,, Equivalence.transitive (Setoid.eq S) snd1 snd2

  linearFunctionsGroup : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (F : Field R) → Group (linearFunctionsSetoid F) (composeLinearFunctions)
  Group.+WellDefined (linearFunctionsGroup {R = R} F) {record { xCoeff = xCoeffM ; xCoeffNonzero = xCoeffNonzeroM ; constant = constantM }} {record { xCoeff = xCoeffN ; xCoeffNonzero = xCoeffNonzeroN ; constant = constantN }} {record { xCoeff = xCoeffX ; xCoeffNonzero = xCoeffNonzeroX ; constant = constantX }} {record { xCoeff = xCoeff ; xCoeffNonzero = xCoeffNonzero ; constant = constant }} (fst1 ,, snd1) (fst2 ,, snd2) = *WellDefined fst1 fst2 ,, Group.+WellDefined additiveGroup (*WellDefined fst1 snd2) snd1
    where
      open Ring R
  Group.0G (linearFunctionsGroup {S = S} {R = R} F) = record { xCoeff = Ring.1R R ; constant = Ring.0R R ; xCoeffNonzero = λ p → Field.nontrivial F (Equivalence.symmetric (Setoid.eq S) p) }
  Group.inverse (linearFunctionsGroup {S = S} {_*_ = _*_} {R = R} F) record { xCoeff = xCoeff ; constant = c ; xCoeffNonzero = pr } with Field.allInvertible F xCoeff pr
  ... | (inv , pr') = record { xCoeff = inv ; constant = inv * (Group.inverse (Ring.additiveGroup R) c) ; xCoeffNonzero = λ p → Field.nontrivial F (transitive (symmetric (transitive (Ring.*WellDefined R p reflexive) (transitive (Ring.*Commutative R) (Ring.timesZero R)))) pr') }
    where
      open Setoid S
      open Equivalence eq
  Group.+Associative (linearFunctionsGroup {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} F) {record { xCoeff = xA ; xCoeffNonzero = xANonzero ; constant = cA }} {record { xCoeff = xB ; xCoeffNonzero = xBNonzero ; constant = cB }} {record { xCoeff = xC ; xCoeffNonzero = xCNonzero ; constant = cC }} = Ring.*Associative R ,, transitive (Group.+WellDefined additiveGroup (transitive *DistributesOver+ (Group.+WellDefined additiveGroup *Associative reflexive)) reflexive) (symmetric (Group.+Associative additiveGroup))
    where
      open Setoid S
      open Equivalence eq
      open Ring R
  Group.identRight (linearFunctionsGroup {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} F) {record { xCoeff = xCoeff ; xCoeffNonzero = xCoeffNonzero ; constant = constant }} = transitive (Ring.*Commutative R) (Ring.identIsIdent R) ,, transitive (Group.+WellDefined additiveGroup (Ring.timesZero R) reflexive) (Group.identLeft additiveGroup)
    where
      open Ring R
      open Setoid S
      open Equivalence eq
  Group.identLeft (linearFunctionsGroup {S = S} {R = R} F) {record { xCoeff = xCoeff ; xCoeffNonzero = xCoeffNonzero ; constant = constant }} = identIsIdent ,, transitive (Group.identRight additiveGroup) identIsIdent
    where
      open Setoid S
      open Ring R
      open Equivalence eq
  Group.invLeft (linearFunctionsGroup F) {record { xCoeff = xCoeff ; xCoeffNonzero = xCoeffNonzero ; constant = constant }} with Field.allInvertible F xCoeff xCoeffNonzero
  Group.invLeft (linearFunctionsGroup {S = S} {R = R} F) {record { xCoeff = xCoeff ; xCoeffNonzero = xCoeffNonzero ; constant = constant }} | inv , prInv = prInv ,, transitive (symmetric *DistributesOver+) (transitive (*WellDefined reflexive (Group.invRight additiveGroup)) (Ring.timesZero R))
    where
      open Setoid S
      open Ring R
      open Equivalence eq
  Group.invRight (linearFunctionsGroup {S = S} {R = R} F) {record { xCoeff = xCoeff ; xCoeffNonzero = xCoeffNonzero ; constant = constant }} with Field.allInvertible F xCoeff xCoeffNonzero
  ... | inv , pr = transitive *Commutative pr  ,, transitive (Group.+WellDefined additiveGroup *Associative reflexive) (transitive (Group.+WellDefined additiveGroup (*WellDefined (transitive *Commutative pr) reflexive) reflexive) (transitive (Group.+WellDefined additiveGroup identIsIdent reflexive) (Group.invLeft additiveGroup)))
    where
      open Setoid S
      open Ring R
      open Equivalence eq

  {-
    Question 3, part 2: prove that linearFunctionsGroup is not abelian
  -}

  -- We'll assume the field doesn't have characteristic 2.
  linearFunctionsGroupNotAbelian : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {F : Field R} → (nonChar2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) → AbelianGroup (linearFunctionsGroup F) → False
  linearFunctionsGroupNotAbelian {S = S} {_+_ = _+_} {_*_ = _*_} {R = R} {F = F} pr record { commutative = commutative } = ans
    where
      open Ring R
      open Group additiveGroup
      open Equivalence (Setoid.eq S) renaming (symmetric to symmetricS ; transitive to transitiveS ; reflexive to reflexiveS)

      f : LinearFunction F
      f = record { xCoeff = 1R ; xCoeffNonzero = λ p → Field.nontrivial F (symmetricS p) ; constant = 1R }
      g : LinearFunction F
      g = record { xCoeff = 1R + 1R ; xCoeffNonzero = pr ; constant = 0R }

      gf : LinearFunction F
      gf = record { xCoeff = 1R + 1R ; xCoeffNonzero = pr ; constant = 1R + 1R }

      fg : LinearFunction F
      fg = record { xCoeff = 1R + 1R ; xCoeffNonzero = pr ; constant = 1R }

      oneWay : Setoid._∼_ (linearFunctionsSetoid F) gf (composeLinearFunctions g f)
      oneWay = symmetricS (transitiveS *Commutative identIsIdent) ,, transitiveS (symmetricS (transitiveS *Commutative identIsIdent)) (symmetricS (Group.identRight additiveGroup))

      otherWay : Setoid._∼_ (linearFunctionsSetoid F) fg (composeLinearFunctions f g)
      otherWay = symmetricS identIsIdent ,, transitiveS (symmetricS (Group.identLeft additiveGroup)) (Group.+WellDefined additiveGroup (symmetricS identIsIdent) (reflexiveS {1R}))

      open Equivalence (Setoid.eq (linearFunctionsSetoid F))
      bad : Setoid._∼_ (linearFunctionsSetoid F) gf fg
      bad = transitive {gf} {composeLinearFunctions g f} {fg} oneWay (transitive {composeLinearFunctions g f} {composeLinearFunctions f g} {fg} (commutative {g} {f}) (symmetric {fg} {composeLinearFunctions f g} otherWay))

      ans : False
      ans with bad
      ans | _ ,, contr = Field.nontrivial F (symmetricS (transitiveS {1R} {1R + (1R + Group.inverse additiveGroup 1R)} (transitiveS (symmetricS (Group.identRight additiveGroup)) (Group.+WellDefined additiveGroup reflexiveS (symmetricS (Group.invRight additiveGroup)))) (transitiveS (Group.+Associative additiveGroup) (transitiveS (Group.+WellDefined additiveGroup contr reflexiveS) (Group.invRight additiveGroup)))))


text:
------------------------------------------------------------------------
-- The partiality monad's monad instance, defined via an adjunction
------------------------------------------------------------------------

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

module Partiality-monad.Inductive.Monad.Adjunction where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (T; ⊥)

open import Adjunction equality-with-J
open import Bijection equality-with-J using (_↔_)
open import Category equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import Functor equality-with-J
open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Partiality-algebra as PA hiding (id; _∘_)
open import Partiality-algebra.Category as PAC
import Partiality-algebra.Properties as PAP
open import Partiality-monad.Inductive as PI
  using (_⊥; partiality-algebra; initial)
open import Partiality-monad.Inductive.Eliminators
import Partiality-monad.Inductive.Monad as PM
import Partiality-monad.Inductive.Omega-continuous as PO

-- A forgetful functor from partiality algebras to sets.

Forget : ∀ {a p q} {A : Type a} →
         PAC.precategory p q A ⇨ precategory-Set p ext
functor Forget =
    (λ P → T P , T-is-set P)
  , Morphism.function
  , refl
  , refl
  where
  open Partiality-algebra

-- The precategory of pointed ω-cpos.

ω-CPPO : ∀ p q → Precategory (lsuc (p ⊔ q)) (p ⊔ q)
ω-CPPO p q = PAC.precategory p q ⊥₀

-- Pointed ω-cpos.

ω-cppo : ∀ p q → Type (lsuc (p ⊔ q))
ω-cppo p q = Partiality-algebra p q ⊥₀

-- If there is a function from B to the carrier of P, then P
-- can be converted to a partiality algebra over B.

convert : ∀ {a b p q} {A : Type a} {B : Type b} →
          (P : Partiality-algebra p q A) →
          (B → Partiality-algebra.T P) →
          Partiality-algebra p q B
convert P f = record
  { T                       = T
  ; partiality-algebra-with = record
    { _⊑_               = _⊑_
    ; never             = never
    ; now               = f
    ; ⨆                 = ⨆
    ; antisymmetry      = antisymmetry
    ; T-is-set-unused   = T-is-set-unused
    ; ⊑-refl            = ⊑-refl
    ; ⊑-trans           = ⊑-trans
    ; never⊑            = never⊑
    ; upper-bound       = upper-bound
    ; least-upper-bound = least-upper-bound
    ; ⊑-propositional   = ⊑-propositional
    }
  }
  where
  open Partiality-algebra P

-- A lemma that removes convert from certain types.

drop-convert :
  ∀ {a p q p′ q′} {A : Type a} {X : ω-cppo p q} {Y : ω-cppo p′ q′}
    {f : A → _} {g : A → _} →
  Morphism (convert X f) (convert Y g) → Morphism X Y
drop-convert m = record
  { function     = function
  ; monotone     = monotone
  ; strict       = strict
  ; now-to-now   = λ x → ⊥-elim x
  ; ω-continuous = ω-continuous
  }
  where
  open Morphism m

-- Converts partiality algebras to ω-cppos.

drop-now : ∀ {a p q} {A : Type a} →
           Partiality-algebra p q A → ω-cppo p q
drop-now P = convert P ⊥-elim

-- The function drop-now does not modify ω-cppos.

drop-now-constant :
  ∀ {p q} {P : ω-cppo p q} →
  drop-now P ≡ P
drop-now-constant =
  cong (λ now → record { partiality-algebra-with =
                           record { now = now } })
       (⟨ext⟩ λ x → ⊥-elim x)

-- Converts types to ω-cppos.

Partial⊚ : ∀ {ℓ} → Type ℓ → ω-cppo ℓ ℓ
Partial⊚ = drop-now ∘ partiality-algebra

private

  -- A lemma.

  Partial⊙′ :
    let open Partiality-algebra; open Morphism in

    ∀ {a b p q} {A : Type a} {B : Type b}
    (P : Partiality-algebra p q B) →
    (f : A → T P) →
    ∃ λ (m : Morphism (Partial⊚ A) (drop-now P)) →
      (∀ x → function m (PI.now x) ≡ now (convert P f) x)
        ×
      (∀ m′ → (∀ x → function m′ (PI.now x) ≡ now (convert P f) x) →
              m ≡ m′)
  Partial⊙′ {A = A} P f = m′ , PI.⊥-rec-now _ , lemma
    where
    P′ : Partiality-algebra _ _ A
    P′ = convert P f

    m : Morphism (partiality-algebra A) P′
    m = proj₁ (initial P′)

    m′ : Morphism (Partial⊚ A) (drop-now P)
    m′ = drop-convert m

    abstract

      lemma :
        ∀ m″ →
        (∀ x → Morphism.function m″ (PI.now x) ≡
               Partiality-algebra.now P′ x) →
        m′ ≡ m″
      lemma m″ hyp = _↔_.to equality-characterisation-Morphism (
        function m′  ≡⟨⟩
        function m   ≡⟨ cong function (proj₂ (initial P′) record
                                         { function     = function m″
                                         ; monotone     = monotone m″
                                         ; strict       = strict m″
                                         ; now-to-now   = hyp
                                         ; ω-continuous =
                                             ω-continuous m″
                                         }) ⟩∎
        function m″  ∎)
        where
        open Morphism

-- Lifts functions between types to morphisms between the
-- corresponding ω-cppos.

Partial⊙ :
  ∀ {a b} {A : Type a} {B : Type b} →
  (A → B) → Morphism (Partial⊚ A) (Partial⊚ B)
Partial⊙ f = proj₁ (Partial⊙′ (partiality-algebra _) (PI.now ∘ f))

-- Partial⊙ f is the unique morphism (of the given type) mapping
-- PI.now x to PI.now (f x) (for all x).

Partial⊙-now :
  ∀ {a b} {A : Type a} {B : Type b} {f : A → B} {x} →
  Morphism.function (Partial⊙ f) (PI.now x) ≡ PI.now (f x)
Partial⊙-now = proj₁ (proj₂ (Partial⊙′ (partiality-algebra _) _)) _

Partial⊙-unique :
  ∀ {a b} {A : Type a} {B : Type b} {f : A → B} {m} →
    (∀ x → Morphism.function m (PI.now x) ≡ PI.now (f x)) →
  Partial⊙ f ≡ m
Partial⊙-unique = proj₂ (proj₂ (Partial⊙′ (partiality-algebra _) _)) _

-- A functor that maps a set A to A ⊥.

Partial : ∀ {ℓ} → precategory-Set ℓ ext ⇨ ω-CPPO ℓ ℓ
_⇨_.functor (Partial {ℓ}) =
    Partial⊚ ∘ proj₁
  , Partial⊙
  , L.lemma₁
  , L.lemma₂
  where
  open Morphism

  module L where
   abstract

    lemma₁ : {A : Type ℓ} → Partial⊙ (id {A = A}) ≡ PA.id
    lemma₁ = Partial⊙-unique λ _ → refl

    lemma₂ : {A B C : Type ℓ} {f : A → B} {g : B → C} →
             Partial⊙ (g ∘ f) ≡ Partial⊙ g PA.∘ Partial⊙ f
    lemma₂ {f = f} {g} = Partial⊙-unique λ x →
      function (Partial⊙ g PA.∘ Partial⊙ f) (PI.now x)  ≡⟨ cong (function (Partial⊙ g)) Partial⊙-now ⟩
      function (Partial⊙ g) (PI.now (f x))              ≡⟨ Partial⊙-now ⟩∎
      PI.now (g (f x))                                  ∎

-- Partial is a left adjoint of Forget.

Partial⊣Forget : ∀ {ℓ} → Partial {ℓ = ℓ} ⊣ Forget
Partial⊣Forget {ℓ} =
    η
  , ε
  , (λ {X} →
       let P = Partial⊚ (proj₁ X) in
       _↔_.to equality-characterisation-Morphism $ ⟨ext⟩ $
       ⊥-rec-⊥ record
         { pe = fun P (function (Partial⊙ PI.now) PI.never)  ≡⟨ cong (fun P) $ strict (Partial⊙ PI.now) ⟩
                fun P PI.never                               ≡⟨ strict (m P) ⟩∎
                PI.never                                     ∎
         ; po = λ x →
                  fun P (function (Partial⊙ PI.now) (PI.now x))  ≡⟨ cong (fun P) Partial⊙-now ⟩
                  fun P (PI.now (PI.now x))                      ≡⟨ fun-now P ⟩∎
                  PI.now x                                       ∎
         ; pl = λ s hyp →
                  fun P (function (Partial⊙ PI.now) (PI.⨆ s))  ≡⟨ cong (fun P) $ ω-continuous (Partial⊙ PI.now) _ ⟩
                  fun P (PI.⨆ _)                               ≡⟨ ω-continuous (m P) _ ⟩
                  PI.⨆ _                                       ≡⟨ cong PI.⨆ $ _↔_.to PI.equality-characterisation-increasing hyp ⟩∎
                  PI.⨆ s                                       ∎
         ; pp = λ _ → PI.⊥-is-set
         })
  , (λ {X} → ⟨ext⟩ λ x →
       fun X (PI.now x)  ≡⟨ fun-now X ⟩∎
       x                 ∎)
  where
  open Morphism {q₂ = ℓ}
  open PAP
  open Partiality-algebra

  η : id⇨ ⇾ Forget ∙⇨ Partial
  _⇾_.natural-transformation η =
      PI.now
    , (λ {X Y f} → ⟨ext⟩ λ x →
         function (Partial⊙ f) (PI.now x)  ≡⟨ Partial⊙-now ⟩∎
         PI.now (f x)                      ∎)

  m : (X : ω-cppo ℓ ℓ) → Morphism (Partial⊚ (T X)) X
  m X =                                     $⟨ id ⟩
    (T X → T X)                             ↝⟨ proj₁ ∘ Partial⊙′ X ⟩
    Morphism (Partial⊚ (T X)) (drop-now X)  ↝⟨ drop-convert ⟩□
    Morphism (Partial⊚ (T X)) X             □

  fun : (X : ω-cppo ℓ ℓ) → T X ⊥ → T X
  fun X = function (m X)

  fun-now : ∀ (X : ω-cppo ℓ ℓ) {x} → fun X (PI.now x) ≡ x
  fun-now X = proj₁ (proj₂ (Partial⊙′ X _)) _

  fun-unique :
    (X : ω-cppo ℓ ℓ) (m′ : Morphism (Partial⊚ (T X)) X) →
    (∀ x → function m′ (PI.now x) ≡ x) →
    fun X ≡ function m′
  fun-unique X m′ hyp =
    cong function $ proj₂ (proj₂ (Partial⊙′ X _)) (drop-convert m′) hyp

  ε : Partial ∙⇨ Forget ⇾ id⇨
  _⇾_.natural-transformation ε =
      (λ {X} → m X)
    , (λ {X Y f} →
         let m′ = (Partial ∙⇨ Forget) ⊙ f in
         _↔_.to equality-characterisation-Morphism $ ⟨ext⟩ $
         ⊥-rec-⊥ record
           { pe = function f (fun X PI.never)   ≡⟨ cong (function f) (strict (m X)) ⟩
                  function f (never X)          ≡⟨ strict f ⟩
                  never Y                       ≡⟨ sym $ strict (m Y) ⟩
                  fun Y PI.never                ≡⟨ cong (fun Y) $ sym $ strict m′ ⟩∎
                  fun Y (function m′ PI.never)  ∎
           ; po = λ x →
                    function f (fun X (PI.now x))   ≡⟨ cong (function f) (fun-now X) ⟩
                    function f x                    ≡⟨ sym $ fun-now Y ⟩
                    fun Y (PI.now (function f x))   ≡⟨ cong (fun Y) $ sym Partial⊙-now ⟩∎
                    fun Y (function m′ (PI.now x))  ∎
           ; pl = λ s hyp →
                    function f (fun X (PI.⨆ s))   ≡⟨ cong (function f) (ω-continuous (m X) _) ⟩
                    function f (⨆ X _)            ≡⟨ ω-continuous f _ ⟩
                    ⨆ Y _                         ≡⟨ cong (⨆ Y) $ _↔_.to (equality-characterisation-increasing Y) hyp ⟩
                    ⨆ Y _                         ≡⟨ sym $ ω-continuous (m Y) _ ⟩
                    fun Y (PI.⨆ _)                ≡⟨ cong (fun Y) $ sym $ ω-continuous m′ _ ⟩∎
                    fun Y (function m′ (PI.⨆ s))  ∎
           ; pp = λ _ → T-is-set Y
           })

-- Thus we get that the partiality monad is a monad.

Partiality-monad : ∀ {ℓ} → Monad (precategory-Set ℓ ext)
Partiality-monad = adjunction→monad (Partial , Forget , Partial⊣Forget)

private

  -- The object part of the monad's functor really does correspond to
  -- the partiality monad.

  object-part-of-functor-correct :
    ∀ {a} {A : Set a} →
    proj₁ (proj₁ Partiality-monad ⊚ A) ≡ proj₁ A ⊥
  object-part-of-functor-correct = refl

  -- The definition of "map" obtained here matches the explicit
  -- definition in Partiality-monad.Inductive.Monad.

  map-correct :
    ∀ {ℓ} {A B : Set ℓ} {f : proj₁ A → proj₁ B} →
    _⊙_ (proj₁ Partiality-monad) {X = A} {Y = B} f ≡
    PO.[_⊥→_⊥].function (PM.map f)
  map-correct = refl

  -- The definition of "return" is the expected one.

  return-correct :
    ∀ {a} {A : Set a} →
    _⇾_.transformation (proj₁ (proj₂ Partiality-monad)) {X = A} ≡ PI.now
  return-correct = refl

  -- The definition of "join" obtained here matches the explicit
  -- definition in Partiality-monad.Inductive.Monad.

  join-correct :
    ∀ {a} {A : Set a} →
    _⇾_.transformation
      (proj₁ (proj₂ (proj₂ Partiality-monad))) {X = A} ≡
    PM.join
  join-correct = refl

ext: agda

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
------------------------------------------------------------------------------
-- The group commutator
------------------------------------------------------------------------------

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

module GroupTheory.Commutator where

open import GroupTheory.Base

------------------------------------------------------------------------------
-- The group commutator
--
-- There are two definitions for the group commutator:
--
-- [a,b] = aba⁻¹b⁻¹ (Mac Lane and Garret 1999, p. 418), or
--
-- [a,b] = a⁻¹b⁻¹ab (Kurosh 1960, p. 99).
--
-- We use Kurosh's definition, because this is the definition used by
-- the TPTP 6.4.0 problem GRP/GRP024-5.p. Actually the problem uses
-- the definition
--
-- [a,b] = a⁻¹(b⁻¹(ab)).

[_,_] : G → G → G
[ a , b ] = a ⁻¹ · b ⁻¹ · a · b
{-# ATP definition [_,_] #-}

commutatorAssoc : G → G → G → Set
commutatorAssoc a b c = [ [ a , b ] , c ] ≡ [ a , [ b , c ] ]
{-# ATP definition commutatorAssoc #-}

------------------------------------------------------------------------------
-- References
--
-- Mac Lane, S. and Birkhof, G. (1999). Algebra. 3rd ed. AMS Chelsea
-- Publishing.
--
-- Kurosh, A. G. (1960). The Theory of Groups. 2nd
-- ed. Vol. 1. Translated and edited by K. A. Hirsch. Chelsea
-- Publising Company.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Categories.Congruence where

open import Level
open import Relation.Binary hiding (_⇒_; Setoid)

open import Categories.Support.PropositionalEquality
open import Categories.Support.Equivalence
open import Categories.Support.EqReasoning

open import Categories.Category hiding (module Heterogeneous; _[_∼_])

record Congruence {o ℓ e} (C : Category o ℓ e) q : Set (o ⊔ ℓ ⊔ e ⊔ suc q) where
  open Category C
  field
    _≡₀_ : Rel Obj q
    equiv₀ : IsEquivalence _≡₀_

  module Equiv₀ = IsEquivalence equiv₀

  field
    coerce : ∀ {X₁ X₂ Y₁ Y₂} → X₁ ≡₀ X₂ → Y₁ ≡₀ Y₂ → X₁ ⇒ Y₁ → X₂ ⇒ Y₂

    .coerce-resp-≡ : ∀ {X₁ X₂ Y₁ Y₂} (xpf : X₁ ≡₀ X₂) (ypf : Y₁ ≡₀ Y₂)
                   → {f₁ f₂ : X₁ ⇒ Y₁} → f₁ ≡ f₂
                   → coerce xpf ypf f₁ ≡ coerce xpf ypf f₂
    .coerce-refl : ∀ {X Y} (f : X ⇒ Y) → coerce Equiv₀.refl Equiv₀.refl f ≡ f
    .coerce-invariant : ∀ {X₁ X₂ Y₁ Y₂} (xpf₁ xpf₂ : X₁ ≡₀ X₂)
                                        (ypf₁ ypf₂ : Y₁ ≡₀ Y₂)
                      → (f : X₁ ⇒ Y₁)
                      → coerce xpf₁ ypf₁ f ≡ coerce xpf₂ ypf₂ f
    .coerce-trans : ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃} (xpf₁ : X₁ ≡₀ X₂) (xpf₂ : X₂ ≡₀ X₃)
                                          (ypf₁ : Y₁ ≡₀ Y₂) (ypf₂ : Y₂ ≡₀ Y₃)
                  → (f : X₁ ⇒ Y₁)
                  →   coerce (Equiv₀.trans xpf₁ xpf₂) (Equiv₀.trans ypf₁ ypf₂) f
                    ≡ coerce xpf₂ ypf₂ (coerce xpf₁ ypf₁ f)
    .coerce-∘ : ∀ {X₁ X₂ Y₁ Y₂ Z₁ Z₂}
              →   (pfX : X₁ ≡₀ X₂) (pfY : Y₁ ≡₀ Y₂) (pfZ : Z₁ ≡₀ Z₂)
              →   (g : Y₁ ⇒ Z₁) (f : X₁ ⇒ Y₁)
              → coerce pfX pfZ (g ∘ f) ≡ coerce pfY pfZ g ∘ coerce pfX pfY f

  .coerce-local : ∀ {X Y} (xpf : X ≡₀ X) (ypf : Y ≡₀ Y) {f : X ⇒ Y} → coerce xpf ypf f ≡ f
  coerce-local xpf ypf {f} =
    begin
      coerce xpf ypf f
    ↓⟨ coerce-invariant xpf Equiv₀.refl ypf Equiv₀.refl f ⟩
      coerce Equiv₀.refl Equiv₀.refl f
    ↓⟨ coerce-refl f ⟩
      f
    ∎
    where open HomReasoning

  .coerce-zigzag : ∀ {X₁ X₂ Y₁ Y₂} (pfX : X₁ ≡₀ X₂) (rfX : X₂ ≡₀ X₁)
                                   (pfY : Y₁ ≡₀ Y₂) (rfY : Y₂ ≡₀ Y₁)
                   → {f : X₁ ⇒ Y₁}
                   → coerce rfX rfY (coerce pfX pfY f) ≡ f
  coerce-zigzag pfX rfX pfY rfY {f} =
    begin
      coerce rfX rfY (coerce pfX pfY f)
    ↑⟨ coerce-trans _ _ _ _ _ ⟩
      coerce (trans pfX rfX) (trans pfY rfY) f
    ↓⟨ coerce-local _ _ ⟩
      f
    ∎
    where
    open HomReasoning
    open Equiv₀

  .coerce-uncong : ∀ {X₁ X₂ Y₁ Y₂} (pfX : X₁ ≡₀ X₂) (pfY : Y₁ ≡₀ Y₂) (f g : X₁ ⇒ Y₁) → coerce pfX pfY f ≡ coerce pfX pfY g → f ≡ g
  coerce-uncong xpf ypf f g fg-pf =
    begin
      f
    ↑⟨ coerce-zigzag _ _ _ _ ⟩
      coerce (sym xpf) (sym ypf) (coerce xpf ypf f)
    ↓⟨ coerce-resp-≡ _ _ fg-pf ⟩
      coerce (sym xpf) (sym ypf) (coerce xpf ypf g)
    ↓⟨ coerce-zigzag _ _ _ _ ⟩
      g
    ∎
    where
    open HomReasoning
    open Equiv₀

  .coerce-slide⇒ : ∀ {X₁ X₂ Y₁ Y₂} (pfX : X₁ ≡₀ X₂) (rfX : X₂ ≡₀ X₁)
                                   (pfY : Y₁ ≡₀ Y₂) (rfY : Y₂ ≡₀ Y₁)
                   → (f : X₁ ⇒ Y₁) (g : X₂ ⇒ Y₂)
                   → coerce pfX pfY f ≡ g → f ≡ coerce rfX rfY g
  coerce-slide⇒ pfX rfX pfY rfY f g eq =
    begin
      f
    ↑⟨ coerce-zigzag _ _ _ _ ⟩
      coerce rfX rfY (coerce pfX pfY f)
    ↓⟨ coerce-resp-≡ _ _ eq ⟩
      coerce rfX rfY g
    ∎
    where open HomReasoning

  .coerce-slide⇐ : ∀ {X₁ X₂ Y₁ Y₂} (pfX : X₁ ≡₀ X₂) (rfX : X₂ ≡₀ X₁)
                                   (pfY : Y₁ ≡₀ Y₂) (rfY : Y₂ ≡₀ Y₁)
                   → (f : X₁ ⇒ Y₁) (g : X₂ ⇒ Y₂)
                   → f ≡ coerce rfX rfY g → coerce pfX pfY f ≡ g
  coerce-slide⇐ pfX rfX pfY rfY f g eq =
    begin
      coerce pfX pfY f
    ↓⟨ coerce-resp-≡ _ _ eq ⟩
      coerce pfX pfY (coerce rfX rfY g)
    ↓⟨ coerce-zigzag _ _ _ _ ⟩
      g
    ∎
    where open HomReasoning

  .coerce-id : ∀ {X Y} (pf₁ pf₂ : X ≡₀ Y) → coerce pf₁ pf₂ id ≡ id
  coerce-id pf₁ pf₂ =
    begin
      coerce pf₁ pf₂ id
    ↑⟨ identityˡ ⟩
      id ∘ coerce pf₁ pf₂ id
    ↑⟨ ∘-resp-≡ˡ (coerce-local _ _) ⟩
      coerce (trans (sym pf₂) pf₂) (trans (sym pf₂) pf₂) id ∘ coerce pf₁ pf₂ id
    ↓⟨ ∘-resp-≡ˡ (coerce-trans _ _ _ _ _) ⟩
      coerce pf₂ pf₂ (coerce (sym pf₂) (sym pf₂) id) ∘ coerce pf₁ pf₂ id
    ↑⟨ coerce-∘ _ _ _ _ _ ⟩
      coerce pf₁ pf₂ (coerce (sym pf₂) (sym pf₂) id ∘ id)
    ↓⟨ coerce-resp-≡ _ _ identityʳ ⟩
      coerce pf₁ pf₂ (coerce (sym pf₂) (sym pf₂) id)
    ↑⟨ coerce-trans _ _ _ _ _ ⟩
      coerce (trans (sym pf₂) pf₁) (trans (sym pf₂) pf₂) id
    ↓⟨ coerce-local _ _ ⟩
      id
    ∎
    where
    open HomReasoning
    open Equiv₀

module Heterogeneous {o ℓ e} {C : Category o ℓ e} {q} (Q : Congruence C q) where
  open Category C
  open Congruence Q
  open Equiv renaming (refl to refl′; sym to sym′; trans to trans′; reflexive to reflexive′)
  open Equiv₀ renaming (refl to refl₀; sym to sym₀; trans to trans₀; reflexive to reflexive₀)

  infix 4 _∼_

  data _∼_ {A B} (f : A ⇒ B) {X Y} (g : X ⇒ Y) : Set (o ⊔ ℓ ⊔ e ⊔ q) where
    ≡⇒∼ : (ax : A ≡₀ X) (by : B ≡₀ Y) → .(coerce ax by f ≡ g) → f ∼ g

  refl : ∀ {A B} {f : A ⇒ B} → f ∼ f
  refl = ≡⇒∼ refl₀ refl₀ (coerce-refl _)

  sym : ∀ {A B} {f : A ⇒ B} {D E} {g : D ⇒ E} → f ∼ g → g ∼ f
  sym (≡⇒∼ A≡D B≡E f≡g) = ≡⇒∼ (sym₀ A≡D) (sym₀ B≡E) (coerce-slide⇐ _ _ _ _ _ _ (sym′ f≡g))

  trans : ∀ {A B} {f : A ⇒ B}
             {D E} {g : D ⇒ E}
             {F G} {h : F ⇒ G}
          → f ∼ g → g ∼ h → f ∼ h
  trans (≡⇒∼ A≡D B≡E f≡g) (≡⇒∼ D≡F E≡G g≡h) = ≡⇒∼
    (trans₀ A≡D D≡F)
    (trans₀ B≡E E≡G)
    (trans′ (trans′ (coerce-trans _ _ _ _ _) (coerce-resp-≡ _ _ f≡g)) g≡h)

  reflexive : ∀ {A B} {f g : A ⇒ B} → f ≣ g → f ∼ g
  reflexive f≣g = ≡⇒∼ refl₀ refl₀ (trans′ (coerce-refl _) (reflexive′ f≣g))

  ∘-resp-∼ : ∀ {A B C A′ B′ C′} {f : B ⇒ C} {h : B′ ⇒ C′} {g : A ⇒ B} {i : A′ ⇒ B′} → f ∼ h → g ∼ i → (f ∘ g) ∼ (h ∘ i)
  ∘-resp-∼ {f = f} {h} {g} {i} (≡⇒∼ B≡B′₁ C≡C′ f≡h) (≡⇒∼ A≡A′ B≡B′₂ g≡i) = ≡⇒∼
    A≡A′
    C≡C′
    (begin
      coerce A≡A′ C≡C′ (f ∘ g)
    ↓⟨ coerce-∘ _ _ _ _ _ ⟩
      coerce B≡B′₁ C≡C′ f ∘ coerce A≡A′ B≡B′₁ g
    ↓⟨ ∘-resp-≡ʳ (coerce-invariant _ _ _ _ _) ⟩
      coerce B≡B′₁ C≡C′ f ∘ coerce A≡A′ B≡B′₂ g
    ↓⟨ ∘-resp-≡ f≡h g≡i ⟩
      h ∘ i
    ∎)
    where open HomReasoning

  ∘-resp-∼ˡ : ∀ {A B C C′} {f : B ⇒ C} {h : B ⇒ C′} {g : A ⇒ B} → f ∼ h → (f ∘ g) ∼ (h ∘ g)
  ∘-resp-∼ˡ {f = f} {h} {g} (≡⇒∼ B≡B C≡C′ f≡h) = ≡⇒∼ refl₀ C≡C′
    (begin
      coerce refl₀ C≡C′ (f ∘ g)
    ↓⟨ coerce-∘ _ _ _ _ _ ⟩
      coerce B≡B C≡C′ f ∘ coerce refl₀ B≡B g
    ↓⟨ ∘-resp-≡ʳ (coerce-local _ _) ⟩
      coerce B≡B C≡C′ f ∘ g
    ↓⟨ ∘-resp-≡ˡ f≡h ⟩
      h ∘ g
    ∎)
    where open HomReasoning

  ∘-resp-∼ʳ : ∀ {A A′ B C} {f : A ⇒ B} {h : A′ ⇒ B} {g : B ⇒ C} → f ∼ h → (g ∘ f) ∼ (g ∘ h)
  ∘-resp-∼ʳ {f = f} {h} {g} (≡⇒∼ A≡A′ B≡B f≡h) = ≡⇒∼ A≡A′ refl₀
    (begin
      coerce A≡A′ refl₀ (g ∘ f)
    ↓⟨ coerce-∘ _ _ _ _ _ ⟩
      coerce B≡B refl₀ g ∘ coerce A≡A′ B≡B f
    ↓⟨ ∘-resp-≡ˡ (coerce-local _ _) ⟩
      g ∘ coerce A≡A′ B≡B f
    ↓⟨ ∘-resp-≡ʳ f≡h ⟩
      g ∘ h
    ∎)
    where open HomReasoning

  .∼⇒≡ : ∀ {A B} {f g : A ⇒ B} → f ∼ g → f ≡ g
  ∼⇒≡ (≡⇒∼ A≡A B≡B f≡g) = trans′ (sym′ (coerce-local A≡A B≡B)) (irr f≡g)

  domain-≣ : ∀ {A A′ B B′} {f : A ⇒ B} {f′ : A′ ⇒ B′} → f ∼ f′ → A ≡₀ A′
  domain-≣ (≡⇒∼ eq _ _) = eq

  codomain-≣ : ∀ {A A′ B B′} {f : A ⇒ B} {f′ : A′ ⇒ B′} → f ∼ f′ → B ≡₀ B′
  codomain-≣ (≡⇒∼ _ eq _) = eq

  ∼-cong : ∀ {t : Level} {T : Set t} {dom cod : T → Obj} (f : (x : T) → dom x ⇒ cod x) → ∀ {i j} (eq : i ≣ j) → f i ∼ f j
  ∼-cong f ≣-refl = refl

  -- henry ford versions
  .∼⇒≡₂ : ∀ {A A′ B B′} {f : A ⇒ B} {f′ : A′ ⇒ B′} → f ∼ f′ → (A≡A′ : A ≡₀ A′) (B≡B′ : B ≡₀ B′) → coerce A≡A′ B≡B′ f ≡ f′
  ∼⇒≡₂ (≡⇒∼ pfA pfB pff) A≡A′ B≡B′ = trans′ (coerce-invariant _ _ _ _ _) (irr pff)

  -- .∼⇒≡ˡ : ∀ {A B B′} {f : A ⇒ B} {f′ : A ⇒ B′} → f ∼ f′ → (B≣B′ : B ≣ B′) → floatˡ B≣B′ f ≡ f′
  -- ∼⇒≡ˡ pf ≣-refl = ∼⇒≡ pf

  -- .∼⇒≡ʳ : ∀ {A A′ B} {f : A ⇒ B} {f′ : A′ ⇒ B} → f ∼ f′ → (A≣A′ : A ≣ A′) → floatʳ A≣A′ f ≡ f′
  -- ∼⇒≡ʳ pf ≣-refl = ∼⇒≡ pf

  -- ≡⇒∼ʳ : ∀ {A A′ B} {f : A ⇒ B} {f′ : A′ ⇒ B} → (A≣A′ : A ≣ A′) → .(floatʳ A≣A′ f ≡ f′) → f ∼ f′
  -- ≡⇒∼ʳ ≣-refl pf = ≡⇒∼ pf

  coerce-resp-∼ : ∀ {A A′ B B′} (A≡A′ : A ≡₀ A′) (B≡B′ : B ≡₀ B′) {f : C [ A , B ]} → f ∼ coerce A≡A′ B≡B′ f
  coerce-resp-∼ A≡A′ B≡B′ = ≡⇒∼ A≡A′ B≡B′ refl′

  -- floatˡ-resp-∼ : ∀ {A B B′} (B≣B′ : B ≣ B′) {f : C [ A , B ]} → f ∼ floatˡ B≣B′ f
  -- floatˡ-resp-∼ ≣-refl = refl

  -- floatʳ-resp-∼ : ∀ {A A′ B} (A≣A′ : A ≣ A′) {f : C [ A , B ]} → f ∼ floatʳ A≣A′ f
  -- floatʳ-resp-∼ ≣-refl = refl

  infixr 4 ▹_

  record -⇒- : Set (o ⊔ ℓ) where
    constructor ▹_
    field
      {Dom} : Obj
      {Cod} : Obj
      morphism : Dom ⇒ Cod

  ∼-setoid : Setoid _ _
  ∼-setoid = record {
               Carrier = -⇒-;
               _≈_ = λ x y → -⇒-.morphism x ∼ -⇒-.morphism y;
               isEquivalence = record { refl = refl; sym = sym; trans = trans } }

  module HetReasoning where
    open SetoidReasoning ∼-setoid public

_[_∼_] : ∀ {o ℓ e} {C : Category o ℓ e} {q} (Q : Congruence C q) {A B} (f : C [ A , B ]) {X Y} (g : C [ X , Y ]) → Set (q ⊔ o ⊔ ℓ ⊔ e)
Q [ f ∼ g ] = Heterogeneous._∼_ Q f g

TrivialCongruence : ∀ {o ℓ e} (C : Category o ℓ e) → Congruence C _
TrivialCongruence C = record
  { _≡₀_ = _≣_
  ; equiv₀ = ≣-isEquivalence
  ; coerce = ≣-subst₂ (_⇒_)
  ; coerce-resp-≡ = resp-≡
  ; coerce-refl = λ f → refl
  ; coerce-invariant = invariant
  ; coerce-trans = tranz
  ; coerce-∘ = compose
  }
  where
  open Category C
  open Equiv
  -- XXX must this depend on proof irrelevance?

  .resp-≡ : ∀ {X₁ X₂ Y₁ Y₂} (xpf : X₁ ≣ X₂) (ypf : Y₁ ≣ Y₂) {f₁ f₂ : X₁ ⇒ Y₁}
            → f₁ ≡ f₂ → ≣-subst₂ _⇒_ xpf ypf f₁ ≡ ≣-subst₂ _⇒_ xpf ypf f₂
  resp-≡ ≣-refl ≣-refl eq = eq

  .invariant : ∀ {X₁ X₂ Y₁ Y₂} (xpf₁ xpf₂ : X₁ ≣ X₂) (ypf₁ ypf₂ : Y₁ ≣ Y₂)
               → (f : X₁ ⇒ Y₁)
               → ≣-subst₂ _⇒_ xpf₁ ypf₁ f ≡ ≣-subst₂ _⇒_ xpf₂ ypf₂ f
  invariant ≣-refl ≣-refl ≣-refl ≣-refl f = refl

  .tranz : ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃} (xpf₁ : X₁ ≣ X₂) (xpf₂ : X₂ ≣ X₃)
                                 (ypf₁ : Y₁ ≣ Y₂) (ypf₂ : Y₂ ≣ Y₃)
           → (f : X₁ ⇒ Y₁)
           →   ≣-subst₂ _⇒_ (≣-trans xpf₁ xpf₂) (≣-trans ypf₁ ypf₂) f
             ≡ ≣-subst₂ _⇒_ xpf₂ ypf₂ (≣-subst₂ _⇒_ xpf₁ ypf₁ f)
  tranz ≣-refl xpf₂ ≣-refl ypf₂ f = refl

  .compose : ∀ {X₁ X₂ Y₁ Y₂ Z₁ Z₂} (pfX : X₁ ≣ X₂)(pfY : Y₁ ≣ Y₂)(pfZ : Z₁ ≣ Z₂)
             → (g : Y₁ ⇒ Z₁) (f : X₁ ⇒ Y₁)
             →   ≣-subst₂ _⇒_ pfX pfZ (g ∘ f)
               ≡ ≣-subst₂ _⇒_ pfY pfZ g ∘ ≣-subst₂ _⇒_ pfX pfY f
  compose ≣-refl ≣-refl ≣-refl g f = refl

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --sized-types --guardedness #-}

open import Agda.Builtin.Equality
open import Data.Product
open import Data.Sum
open import Codata.Thunk
open import Size
open import Level
open import Relation.Unary using (_⊆_)

module is-lib.InfSys.Equivalence {𝓁} where

  private
    variable
      U : Set 𝓁

  open import is-lib.InfSys.Base {𝓁}
  open import is-lib.InfSys.Coinduction {𝓁}
  open import is-lib.InfSys.SCoinduction {𝓁}
  open IS

  {- Equivalence CoInd and SCoInd -}

  coind-size : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → CoInd⟦ is ⟧ ⊆ λ u → ∀ {i} → SCoInd⟦ is ⟧ u i
  coind-size p-coind with CoInd⟦_⟧.unfold p-coind
  ... | rn , c , refl , pr = sfold (rn , c , refl , λ i → λ where .force → coind-size (pr i))

  size-coind : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → (λ u → ∀ {i} → SCoInd⟦ is ⟧ u i) ⊆ CoInd⟦ is ⟧
  size-coind {is = is} p-scoind = coind[ is ] (λ u → ∀ {j} → SCoInd⟦ is ⟧ u j) scoind-postfix p-scoind

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module Data.Bin.Minus where

  open import Data.Bin hiding (suc; fromℕ)
  open Data.Bin using (2+_)
  open import Data.Bin.Bijection using (fromℕ)
  open import Data.Fin hiding (_-_; _+_; toℕ; _<_; fromℕ)
  open import Data.List
  open import Data.Digit
  open import Relation.Binary.PropositionalEquality
  open import Data.Nat using (ℕ; _∸_; suc; zero) renaming (_+_ to _ℕ+_)

  infixl 6 _-?_
  infixl 6 _-_

  open import Function

  pred' : Bin → Bin
  pred' 0# = 0#
  pred' ([] 1#) = 0#
  pred' ((zero ∷ t) 1#) = case Data.Bin.pred t of
    λ {
      0# → [] 1# ;
      (t' 1#) → (suc zero ∷ t') 1#
    }
  pred' ((suc zero ∷ t) 1#) = (zero ∷ t) 1#
  pred' ((suc (suc ()) ∷ _) 1#)

  open import Data.Sum
  open import Data.Unit
  import Data.Nat.Properties

  data Greater (a b : Bin) : Set where
   greater : ∀ (diff : Bin⁺) → b + diff 1# ≡ a → Greater a b

  open import Data.Empty using (⊥; ⊥-elim)

  import Data.Bin.Addition
  open import Data.Bin.Props

  greater-to-< : ∀ a b → Greater a b → b < a
  greater-to-< ._ b (greater diff refl) =
    let
      zz = Data.Nat.Properties.+-mono-≤
        {1} {toℕ (diff 1#)} {toℕ b} {toℕ b}
        (case z<nz diff of λ { (Data.Bin.less p) → p })
        Data.Nat.Properties.≤-refl
    in
     Data.Bin.less (Data.Nat.Properties.≤-trans zz (
       Data.Nat.Properties.≤-reflexive (
         trans
           (sym (Data.Nat.Properties.+-comm (toℕ b) _))
           (sym (Data.Bin.Addition.+-is-addition b (diff 1#)))
           )))

  open import Data.Product

  data Difference (a b : Bin) : Set where
    positive : Greater a b → Difference a b
    negative : Greater b a → Difference a b
    equal : a ≡ b → Difference a b

  open import Relation.Nullary

  open import Algebra.Structures

  import Data.Bin.Addition
  open IsCommutativeMonoid Data.Bin.Addition.is-commutativeMonoid
    using (identity; identityˡ)
    renaming (comm to +-comm; assoc to +-assoc)

  open import Data.Product
  identityʳ = proj₂ identity

  ∷-pred : Bit → Bin⁺ → Bin⁺
  ∷-pred zero [] = []
  ∷-pred zero (h ∷ t) = suc zero ∷ ∷-pred h t
  ∷-pred (suc zero) l = zero ∷ l
  ∷-pred (suc (suc ())) l

  open Relation.Binary.PropositionalEquality.≡-Reasoning

  open import Data.Bin.Multiplication using (∷1#-interpretation)

  open import Function using (_⟨_⟩_)

  seems-trivial : ∀ xs → (zero ∷ xs) 1# + [] 1# ≡ (suc zero ∷ xs) 1#
  seems-trivial xs = cong (λ q → q + [] 1#) (∷1#-interpretation zero xs ⟨ trans ⟩ (identityˡ (xs 1# *2))) ⟨ trans ⟩ +-comm (xs 1# *2) ([] 1#) ⟨ trans ⟩ sym (∷1#-interpretation (suc zero) xs)

  open import Data.Bin.Props

  carry : ∀ t → [] 1# + (suc zero ∷ t) 1# ≡ ([] 1# + t 1#) *2
  carry t =
   begin
    [] 1# + (suc zero ∷ t) 1#
     ≡⟨ cong (_+_ ([] 1#)) (∷1#-interpretation (suc zero) t) ⟩
    [] 1# + ([] 1# + t 1# *2)
     ≡⟨ sym (+-assoc ([] 1#) ([] 1#) (t 1# *2)) ⟩
    [] 1# *2 + (t 1# *2)
     ≡⟨ sym (*2-distrib ([] 1#) (t 1#)) ⟩
    ([] 1# + t 1#) *2
   ∎

  1+∷-pred : ∀ h t → [] 1# + (∷-pred h t) 1# ≡ (h ∷ t) 1#
  1+∷-pred zero [] = refl
  1+∷-pred zero (x ∷ xs) =
   begin
    [] 1# + (suc zero ∷ ∷-pred x xs) 1#
     ≡⟨ carry (∷-pred x xs) ⟩
    ([] 1# + (∷-pred x xs) 1#) *2
     ≡⟨ cong _*2 (1+∷-pred x xs) ⟩
    (x ∷ xs) 1# *2
     ≡⟨ refl ⟩
    (zero ∷ x ∷ xs) 1#
   ∎
  1+∷-pred (suc zero) t = +-comm ([] 1#) ((zero ∷ t) 1#) ⟨ trans ⟩ seems-trivial t
  1+∷-pred (suc (suc ())) t

  data Comparison (A : Set) : Set where
    greater : A → Comparison A
    equal : Comparison A
    less : A → Comparison A

  map-cmp : {A B : Set} → (A → B) → Comparison A → Comparison B
  map-cmp f (greater a) = greater (f a)
  map-cmp f (less a) = less (f a)
  map-cmp f equal = equal

  _%f_ : ∀ {b} → Fin (suc b) → Fin (suc b) → Comparison (Fin b)
  zero %f zero = equal
  zero %f suc b = less b
  suc a %f zero = greater a
  _%f_ {suc base} (suc a) (suc b) = map-cmp inject₁ (a %f b)
  _%f_ {zero} (suc ()) (suc ())

  _*2-1 : Bin⁺ → Bin⁺
  [] *2-1 = []
  (suc zero ∷ t) *2-1 = suc zero ∷ zero ∷ t
  (zero ∷ t) *2-1 = suc zero ∷ (t *2-1)
  (suc (suc ()) ∷ t) *2-1

  _*2+1' : Bin⁺ → Bin⁺
  l *2+1' = suc zero ∷ l

  addBit : Bin⁺ → Comparison (Fin 1) → Bin⁺
  addBit gt (greater zero) = gt *2+1'
  addBit gt equal = zero ∷ gt
  addBit gt (less zero) = gt *2-1
  addBit gt (less (suc ()))
  addBit gt (greater (suc ()))

  open import Data.Bin.Utils

  *2-1-lem : ∀ d → (d *2-1) 1# + [] 1# ≡ d 1# *2
  *2-1-lem [] = refl
  *2-1-lem (zero ∷ xs) =
   begin
    (zero ∷ xs) *2-1 1# + [] 1#
     ≡⟨ refl ⟩
    (suc zero ∷ (xs *2-1)) 1# + [] 1#
     ≡⟨ +-comm ((suc zero ∷ xs *2-1) 1#) ([] 1#)  ⟩
    [] 1# + (suc zero ∷ (xs *2-1)) 1#
     ≡⟨ carry (xs *2-1) ⟩
    ([] 1# + (xs *2-1) 1#) *2
     ≡⟨ cong _*2 (+-comm ([] 1#) ((xs *2-1) 1#)) ⟩
    ((xs *2-1) 1# + [] 1#) *2
     ≡⟨ cong _*2 (*2-1-lem xs) ⟩
    (xs 1# *2) *2
     ≡⟨ refl ⟩
    (zero ∷ xs) 1# *2
   ∎
  *2-1-lem (suc zero ∷ xs) =
   begin
    (suc zero ∷ zero ∷ xs) 1# + [] 1#
     ≡⟨ cong (λ q → q + [] 1#) (∷1#-interpretation (suc zero) (zero ∷ xs)) ⟩
    [] 1# + (zero ∷ xs) 1# *2 + [] 1#
     ≡⟨ refl ⟩
    [] 1# + xs 1# *2 *2 + [] 1#
     ≡⟨ +-comm ([] 1# + xs 1# *2 *2) ([] 1#) ⟩
    [] 1# + ([] 1# + xs 1# *2 *2)
     ≡⟨ sym (+-assoc ([] 1#) ([] 1#) (xs 1# *2 *2)) ⟩
    [] 1# *2 + xs 1# *2 *2
     ≡⟨ sym (*2-distrib ([] 1#) (xs 1# *2)) ⟩
    ([] 1# + xs 1# *2) *2
     ≡⟨ cong _*2 (sym (∷1#-interpretation (suc zero) xs)) ⟩
    (suc zero ∷ xs) 1# *2
     ≡⟨ refl ⟩
    (zero ∷ suc zero ∷ xs) 1#
   ∎
  *2-1-lem (suc (suc ()) ∷ xs)

  addBit-lem : ∀ x y d → addBit d (x %f y) 1# + bitToBin y ≡ d 1# *2 + bitToBin x
  addBit-lem zero zero d = refl
  addBit-lem (suc zero) zero d = refl
  addBit-lem zero (suc zero) d = *2-1-lem d ⟨ trans ⟩ sym (identityʳ (d 1# *2))
  addBit-lem (suc zero) (suc zero) d = refl
  addBit-lem (suc (suc ())) _ d
  addBit-lem _ (suc (suc ())) d

  +-cong₁ : ∀ {z} {x y} → x ≡ y → x + z ≡ y + z
  +-cong₁ {z} = cong (λ q → q + z)

  +-cong₂ : ∀ {z} {x y} → x ≡ y → z + x ≡ z + y
  +-cong₂ {z} = cong (λ q → z + q)

  refineGt : ∀ xs ys (x y : Bit) → Greater (xs 1#) (ys 1#) → Greater ((x ∷ xs) 1#) ((y ∷ ys) 1#)
  refineGt xs ys x y (greater d ys+d=xs) = greater (addBit d (x %f y)) good where
    good : (y ∷ ys) 1# + addBit d (x %f y) 1# ≡ (x ∷ xs) 1#
    good =
     begin
      (y ∷ ys) 1# + addBit d (x %f y) 1#
       ≡⟨ +-cong₁ {addBit d (x %f y) 1#} (∷1#-interpretation y ys) ⟩
      bitToBin y + (ys 1#) *2 + addBit d (x %f y) 1#
       ≡⟨ +-comm (bitToBin y + (ys 1#) *2) (addBit d (x %f y) 1#) ⟩
      addBit d (x %f y) 1# + (bitToBin y + (ys 1#) *2)
       ≡⟨ sym (+-assoc (addBit d (x %f y) 1#) (bitToBin y) ((ys 1#) *2)) ⟩
      (addBit d (x %f y) 1# + bitToBin y) + (ys 1#) *2
       ≡⟨ +-cong₁ {(ys 1#) *2} (addBit-lem x y d) ⟩
      (d 1# *2 + bitToBin x) + (ys 1#) *2
       ≡⟨ +-cong₁ {(ys 1#) *2} (+-comm (d 1# *2) (bitToBin x)) ⟩
      (bitToBin x + d 1# *2 ) + (ys 1#) *2
       ≡⟨  +-assoc (bitToBin x) (d 1# *2) ((ys 1#) *2) ⟩
      bitToBin x + (d 1# *2 + (ys 1#) *2)
       ≡⟨ +-cong₂ {bitToBin x} (+-comm (d 1# *2) ((ys 1#) *2)) ⟩
      bitToBin x + ((ys 1#) *2 + d 1# *2)
       ≡⟨ +-cong₂ {bitToBin x} (sym (*2-distrib (ys 1#) (d 1#))) ⟩
      bitToBin x + (ys 1# + d 1#) *2
       ≡⟨ +-cong₂ {bitToBin x} (cong _*2 ys+d=xs) ⟩
      bitToBin x + xs 1# *2
       ≡⟨ sym (∷1#-interpretation x xs) ⟩
      (x ∷ xs) 1#
     ∎

  compare-bit : ∀ a b xs → Difference ((a ∷ xs) 1#) ((b ∷ xs) 1#)
  compare-bit 0b 0b xs = equal refl
  compare-bit 1b 0b xs = positive (greater [] (seems-trivial xs))
  compare-bit 0b 1b xs = negative (greater [] (seems-trivial xs))
  compare-bit 1b 1b xs = equal refl
  compare-bit (2+ ()) _ xs
  compare-bit _ (2+ ()) xs

  _-⁺_ : ∀ a b → Difference (a 1#) (b 1#)
  [] -⁺ [] = equal refl
  [] -⁺ (x ∷ xs) = negative (greater (∷-pred x xs) (1+∷-pred x xs))
  (x ∷ xs) -⁺ [] = positive (greater (∷-pred x xs) (1+∷-pred x xs))
  (x ∷ xs) -⁺ (y ∷ ys) =
    case xs -⁺ ys of
      λ {
        (positive gt) → positive (refineGt xs ys x y gt) ;
        (negative lt) → negative (refineGt ys xs y x lt) ;
        (equal refl) → compare-bit _ _ xs
     }

  _-?_ : ∀ a b → Difference a b
  0# -? 0# = equal refl
  a 1# -? 0# = positive (greater a (identityˡ (a 1#)))
  0# -? a 1# = negative (greater a (identityˡ (a 1#)))
  a 1# -? b 1# = a -⁺ b

  _%⁺_ : Bin⁺ → Bin⁺ → Comparison Bin⁺
  [] %⁺ [] = equal
  (h ∷ t) %⁺ [] = greater (∷-pred h t)
  [] %⁺ (h ∷ t) = less (∷-pred h t)
  (x ∷ xs) %⁺ (y ∷ ys) with xs %⁺ ys
  ... | greater gt = greater (addBit gt (x %f y))
  ... | less lt = less (addBit lt (y %f x))
  ... | equal = map-cmp (λ _ → []) (x %f y)

  succ : Bin⁺ → Bin⁺
  succ [] = zero ∷ []
  succ (zero ∷ t) = suc zero ∷ t
  succ (suc zero ∷ t) = zero ∷ succ t
  succ (suc (suc ()) ∷ t)

  succpred-id : ∀ x xs → succ (∷-pred x xs) ≡ x ∷ xs
  succpred-id zero [] = refl
  succpred-id zero (x ∷ xs) = cong (λ z → zero ∷ z) (succpred-id x xs)
  succpred-id (suc zero) xs = refl
  succpred-id (suc (suc ())) xs

  -- CR: difference-to-∸ : ∀ {a b} → Difference a b → Bin
  -- difference-to-bin

  _-_ : Bin → Bin → Bin
  x - y with x -? y
  ... | positive (greater d _) = d 1#
  ... | equal _ = 0#
  ... | negative _ = 0#

  open import Data.Bin.Bijection using (fromℕ-bijection; toℕ-inj; fromToℕ-inverse; fromℕ-inj)

  open import Data.Bin.Addition using (+-is-addition)

  suc-inj : ∀ {x y : ℕ} → Data.Nat.suc x ≡ suc y → x ≡ y
  suc-inj {x} .{x} refl = refl

  ℕ-+-inj₂ : ∀ z {a b} → Data.Nat._+_ z a ≡ Data.Nat._+_ z b → a ≡ b
  ℕ-+-inj₂ zero refl = refl
  ℕ-+-inj₂ (suc n) eq = ℕ-+-inj₂ n (suc-inj eq)

  +-inj₂ : ∀ z {a b} → z + a ≡ z + b → a ≡ b
  +-inj₂ z {a} {b} z+a≡z+b = toℕ-inj ( ℕ-+-inj₂ (toℕ z) (sym (+-is-addition z a) ⟨ trans ⟩ cong toℕ z+a≡z+b ⟨ trans ⟩ +-is-addition z b) )

  nat-+zz : ∀ a b → Data.Nat._+_ a b ≡ 0 → a ≡ 0
  nat-+zz zero b _ = refl
  nat-+zz (suc _) b ()

  +zz : ∀ a b → a + b ≡ 0# → a ≡ 0#
  +zz a b eq = toℕ-inj (nat-+zz (toℕ a) (toℕ b) (sym (+-is-addition a b) ⟨ trans ⟩ cong toℕ eq))

  minus-elim : ∀ x z → z + x - z ≡ x
  minus-elim x z with (z + x -? z)
  ... | positive (greater d z+d=z+x) = +-inj₂ z z+d=z+x
  ... | equal z+x≡z = +-inj₂ z (identityʳ z ⟨ trans ⟩ sym z+x≡z)
  ... | negative (greater d z+x+d≡z) = sym (+zz x (d 1#) (+-inj₂ z
         ( sym (+-assoc z x (d 1#)) ⟨ trans ⟩ z+x+d≡z ⟨ trans ⟩ sym (identityʳ z))))

  import Data.Bin.NatHelpers

  x≮z→x≡z+y : ∀ {x z} → ¬ x < z → ∃ λ y → x ≡ z + y
  x≮z→x≡z+y {x} {z} x≮z = case
    Data.Bin.NatHelpers.x≮z→x≡z+y (λ toℕ-leq → x≮z (less toℕ-leq))
    of λ { (y , eq) →  fromℕ y , toℕ-inj (
    begin
     toℕ x
      ≡⟨ eq ⟩
     toℕ z ℕ+ y
      ≡⟨ cong (λ q → toℕ z ℕ+ q) (fromℕ-inj (sym (fromToℕ-inverse (fromℕ y)))) ⟩
     toℕ z ℕ+ toℕ (fromℕ y)
      ≡⟨ sym (+-is-addition z (fromℕ y)) ⟩
     toℕ (z + fromℕ y)
    ∎) }

  -+-elim' : ∀ {x z} → ¬ x < z → x - z + z ≡ x
  -+-elim' {x} {z} x≮z = case x≮z→x≡z+y x≮z of
    λ { (y , refl) →
   begin
    z + y - z + z
     ≡⟨ cong (λ q → q + z) (minus-elim y z)⟩
    y + z
     ≡⟨ +-comm y z ⟩
    z + y
   ∎ }

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homogeneously-indexed binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Homogeneous`.

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

module Relation.Binary.Indexed.Homogeneous.Bundles where

open import Data.Product using (_,_)
open import Function using (_⟨_⟩_)
open import Level using (Level; _⊔_; suc)
open import Relation.Binary as B using (_⇒_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary using (¬_)
open import Relation.Binary.Indexed.Homogeneous.Core
open import Relation.Binary.Indexed.Homogeneous.Structures

-- Indexed structures are laid out in a similar manner as to those
-- in Relation.Binary. The main difference is each structure also
-- contains proofs for the lifted version of the relation.

------------------------------------------------------------------------
-- Equivalences

record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
  infix 4 _≈ᵢ_ _≈_
  field
    Carrierᵢ       : I → Set c
    _≈ᵢ_           : IRel Carrierᵢ ℓ
    isEquivalenceᵢ : IsIndexedEquivalence Carrierᵢ _≈ᵢ_

  open IsIndexedEquivalence isEquivalenceᵢ public

  Carrier : Set _
  Carrier = ∀ i → Carrierᵢ i

  _≈_ : B.Rel Carrier _
  _≈_ = Lift Carrierᵢ _≈ᵢ_

  _≉_ : B.Rel Carrier _
  x ≉ y = ¬ (x ≈ y)

  setoid : B.Setoid _ _
  setoid = record
    { isEquivalence = isEquivalence
    }

record IndexedDecSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
  infix 4 _≈ᵢ_
  field
    Carrierᵢ          : I → Set c
    _≈ᵢ_              : IRel Carrierᵢ ℓ
    isDecEquivalenceᵢ : IsIndexedDecEquivalence Carrierᵢ _≈ᵢ_

  open IsIndexedDecEquivalence isDecEquivalenceᵢ public

  indexedSetoid : IndexedSetoid I c ℓ
  indexedSetoid = record
    { isEquivalenceᵢ = isEquivalenceᵢ
    }

  open IndexedSetoid indexedSetoid public
    using (Carrier; _≈_; _≉_; setoid)

------------------------------------------------------------------------
-- Preorders

record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
                       Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where

  infix 4 _≈ᵢ_ _∼ᵢ_ _≈_ _∼_

  field
    Carrierᵢ    : I → Set c
    _≈ᵢ_        : IRel Carrierᵢ ℓ₁
    _∼ᵢ_        : IRel Carrierᵢ ℓ₂
    isPreorderᵢ : IsIndexedPreorder Carrierᵢ _≈ᵢ_ _∼ᵢ_

  open IsIndexedPreorder isPreorderᵢ public

  Carrier : Set _
  Carrier = ∀ i → Carrierᵢ i

  _≈_ : B.Rel Carrier _
  x ≈ y = ∀ i → x i ≈ᵢ y i

  _∼_ : B.Rel Carrier _
  x ∼ y = ∀ i → x i ∼ᵢ y i

  preorder : B.Preorder _ _ _
  preorder = record
    { isPreorder = isPreorder
    }

------------------------------------------------------------------------
-- Partial orders

record IndexedPoset {i} (I : Set i) c ℓ₁ ℓ₂ :
                    Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
  field
    Carrierᵢ        : I → Set c
    _≈ᵢ_            : IRel Carrierᵢ ℓ₁
    _≤ᵢ_            : IRel Carrierᵢ ℓ₂
    isPartialOrderᵢ : IsIndexedPartialOrder Carrierᵢ _≈ᵢ_ _≤ᵢ_

  open IsIndexedPartialOrder isPartialOrderᵢ public

  preorderᵢ : IndexedPreorder I c ℓ₁ ℓ₂
  preorderᵢ = record
    { isPreorderᵢ = isPreorderᵢ
    }

  open IndexedPreorder preorderᵢ public
    using (Carrier; _≈_; preorder) renaming (_∼_ to _≤_)

  poset : B.Poset _ _ _
  poset = record
    { isPartialOrder = isPartialOrder
    }


text:
------------------------------------------------------------------------------
-- FOTC combinators for lists, colists, streams, etc.
------------------------------------------------------------------------------

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

module FOTC.Base.List where

open import FOTC.Base

infixr 5 _∷_

------------------------------------------------------------------------------
-- List constants.
postulate [] cons head tail null : D  -- FOTC partial lists.

-- Definitions
abstract
  _∷_  : D → D → D
  x ∷ xs = cons · x · xs
  -- {-# ATP definition _∷_ #-}

  head₁ : D → D
  head₁ xs = head · xs
  -- {-# ATP definition head₁ #-}

  tail₁ : D → D
  tail₁ xs = tail · xs
  -- {-# ATP definition tail₁ #-}

  null₁ : D → D
  null₁ xs = null · xs
  -- {-# ATP definition null₁ #-}

------------------------------------------------------------------------------
-- Conversion rules

-- Conversion rules for null.
-- null-[] :          null · []              ≡ true
-- null-∷  : ∀ x xs → null · (cons · x · xs) ≡ false
postulate
  null-[] : null₁ []                ≡ true
  null-∷  : ∀ x xs → null₁ (x ∷ xs) ≡ false

-- Conversion rule for head.
-- head-∷ : ∀ x xs → head · (cons · x · xs) ≡ x
postulate head-∷ : ∀ x xs → head₁ (x ∷ xs) ≡ x
{-# ATP axiom head-∷ #-}

-- Conversion rule for tail.
-- tail-∷ : ∀ x xs → tail · (cons · x · xs) ≡ xs
postulate tail-∷ : ∀ x xs → tail₁ (x ∷ xs) ≡ xs
{-# ATP axiom tail-∷ #-}

------------------------------------------------------------------------------
-- Discrimination rules

-- postulate []≢cons : ∀ {x xs} → [] ≢ cons · x · xs
postulate []≢cons : ∀ {x xs} → [] ≢ x ∷ xs


text:
{-# OPTIONS --no-syntactic-equality #-}

open import Agda.Primitive

variable
  a : Level

postulate
  A : Set a

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module MultipleIdentifiersOneSignature where

data Bool : Set where
  false true : Bool

data Suit : Set where
  ♥ ♢ ♠ ♣ : Suit

record R : Set₁ where
  field
    A B C : Set

postulate
  A Char : Set
  B C    : Set

{-# BUILTIN CHAR  Char  #-}
{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

primitive
  primIsDigit primIsSpace : Char → Bool

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
{-# OPTIONS --type-in-type #-}
module Spire.DarkwingDuck.Primitive where

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

infixr 4 _,_
infixr 5 _∷_

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

postulate String : Set
{-# BUILTIN STRING String #-}

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

data ⊥ : Set where

elimBot : (P : ⊥ → Set)
  (v : ⊥) → P v
elimBot P ()

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

data ⊤ : Set where
  tt : ⊤

elimUnit : (P : ⊤ → Set)
  (ptt : P tt)
  (u : ⊤) → P u
elimUnit P ptt tt = ptt

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

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) (b : B a) → Σ A B

elimPair : (A : Set) (B : A → Set)
  (P : Σ A B → Set)
  (ppair : (a : A) (b : B a) → P (a , b))
  (ab : Σ A B) → P ab
elimPair A B P ppair (a , b) = ppair a b

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

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

elimEq : (A : Set) (x : A) (P : (y : A) → x ≡ y → Set)
  (prefl : P x refl)
  (y : A) (q : x ≡ y) → P y q
elimEq A .x P prefl x refl = prefl

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

data Enum : Set where
  []  : Enum
  _∷_ : (x : String) (xs : Enum) → Enum

elimEnum : (P : Enum → Set)
  (pnil : P [])
  (pcons : (x : String) (xs : Enum) → P xs → P (x ∷ xs))
  (xs : Enum) → P xs
elimEnum P pnil pcons [] = pnil
elimEnum P pnil pcons (x ∷ xs) = pcons x xs (elimEnum P pnil pcons xs)

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

data Tag : Enum → Set where
  here : ∀{x xs} → Tag (x ∷ xs)
  there : ∀{x xs} → Tag xs → Tag (x ∷ xs)

Branches : (E : Enum) (P : Tag E → Set) → Set
Branches [] P = ⊤
Branches (l ∷ E) P = Σ (P here) (λ _ → Branches E (λ t → P (there t)))

case : (E : Enum) (P : Tag E → Set) (cs : Branches E P) (t : Tag E) → P t
case (ℓ ∷ E) P ccs here = elimPair (P here) (λ _ → Branches E (λ t → P (there t))) (λ _ → P here)
  (λ c cs → c) ccs
case (ℓ ∷ E) P ccs (there t) = elimPair (P here) (λ _ → Branches E (λ t → P (there t))) (λ _ → P (there t))
  (λ c cs → case E (λ t → P (there t)) cs t) ccs

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

data Tel : Set₁ where
  Emp : Tel
  Ext : (A : Set) (B : A → Tel) → Tel

elimTel : (P : Tel → Set)
  (pemp : P Emp)
  (pext  : (A : Set) (B : A → Tel) (pb : (a : A) → P (B a)) → P (Ext A B))
  (T : Tel) → P T
elimTel P pemp pext Emp = pemp
elimTel P pemp pext (Ext A B) = pext A B (λ a → elimTel P pemp pext (B a))

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

data Desc (I : Set) : Set₁ where
  End : (i : I) → Desc I
  Rec : (i : I) (D : Desc I) → Desc I
  Arg : (A : Set) (B : A → Desc I) → Desc I

elimDesc : (I : Set) (P : Desc I → Set)
  (pend : (i : I) → P (End i))
  (prec  : (i : I) (D : Desc I) (pd : P D) → P (Rec i D))
  (parg : (A : Set) (B : A → Desc I) (pb : (a : A) → P (B a)) → P (Arg A B))
  (D : Desc I) → P D
elimDesc I P pend prec parg (End i) = pend i
elimDesc I P pend prec parg (Rec i D) = prec i D (elimDesc I P pend prec parg D)
elimDesc I P pend prec parg (Arg A B) = parg A B (λ a → elimDesc I P pend prec parg (B a))

Func : (I : Set) (D : Desc I) → (I → Set) → I → Set
Func I (End j) X i = j ≡ i
Func I (Rec j D) X i = Σ (X j) (λ _ → Func I D X i)
Func I (Arg A B) X i = Σ A (λ a → Func I (B a) X i)

Hyps : (I : Set) (D : Desc I) (X : I → Set) (M : (i : I) → X i → Set) (i : I) (xs : Func I D X i) → Set
Hyps I (End j) X M i q = ⊤
Hyps I (Rec j D) X M i = elimPair (X j) (λ _ → Func I D X i) (λ _ → Set)
  (λ x xs → Σ (M j x) (λ _ → Hyps I D X M i xs))
Hyps I (Arg A B) X M i = elimPair A (λ a → Func I (B a) X i) (λ _ → Set)
  (λ a xs → Hyps I (B a) X M i xs)

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

data μ (ℓ : String) (P I : Set) (D : Desc I) (p : P) (i : I) : Set where
  init : Func I D (μ ℓ P I D p) i → μ ℓ P I D p i

prove : (I : Set) (D : Desc I) (X : I → Set) (M : (i : I) → X i → Set)
  (m : (i : I) (x : X i) → M i x)
  (i : I) (xs : Func I D X i)
  → Hyps I D X M i xs
prove I (End j) X M m i q = tt
prove I (Rec j D) X M m i = elimPair (X j) (λ _ → Func I D X i)
  (λ xxs → Hyps I (Rec j D) X M i xxs)
  (λ x xs → m j x , prove I D X M m i xs)
prove I (Arg A B) X M m i = elimPair A (λ a → Func I (B a) X i)
  (λ axs → Hyps I (Arg A B) X M i axs)
  (λ a xs → prove I (B a) X M m i xs)

{-# NO_TERMINATION_CHECK #-}
ind : (ℓ : String) (P I : Set) (D : Desc I) (p : P)
  (M : (i : I) → μ ℓ P I D p i → Set)
  (α : ∀ i (xs : Func I D (μ ℓ P I D p) i) (ihs : Hyps I D (μ ℓ P I D p) M i xs) → M i (init xs))
  (i : I)
  (x : μ ℓ P I D p i)
  → M i x
ind ℓ P I D p M α i (init xs) = α i xs (prove I D (μ ℓ P I D p) M (ind ℓ P I D p M α) i xs)

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Instances.Int where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing
open import Cubical.Data.Int as Int
  renaming ( ℤ to ℤType ; _+_ to _+ℤ_; _·_ to _·ℤ_; -_ to -ℤ_)

open CommRingStr

ℤ : CommRing ℓ-zero
fst ℤ = ℤType
0r (snd ℤ) = 0
1r (snd ℤ) = 1
_+_ (snd ℤ) = _+ℤ_
_·_ (snd ℤ) = _·ℤ_
- snd ℤ = -ℤ_
isCommRing (snd ℤ) = isCommRingℤ
  where
  abstract
    isCommRingℤ : IsCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_
    isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc (λ _ → refl)
                                 -Cancel Int.+Comm Int.·Assoc
                                 Int.·Rid ·DistR+ Int.·Comm

max_stars_repo_name: FernandoLarrain/cubical


text:
open import eq
open import bool
open import bool-relations using (transitive; total)
open import maybe
open import nat
open import nat-thms       using (≤-trans; ≤-total)
open import product

module z05-01-hc-sorted-list-test where

open import bool-relations _≤_ hiding (transitive; total)

import z05-01-hc-sorted-list as SL
open SL nat _≤_ (λ {x} {y} {z} → ≤-trans {x} {y} {z})
                (λ {x} {y}     → ≤-total {x} {y})

empty : slist 10 10
empty = snil refl

_ : slist 9 10
_ = slist-insert 9 empty refl

--_ : slist-insert 9 empty refl ≡ scons 9  (snil {!!}) {!!}
--_ = refl

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
-- A variant of code reported by Andreas Abel.

{-# OPTIONS --guardedness --sized-types #-}

open import Agda.Builtin.Size

data ⊥ : Set where

mutual
  data D (i : Size) : Set where
    inn : D' i → D i

  record D' (i : Size) : Set where
    coinductive
    field ♭   : {j : Size< i} → D j
open D'

bla : ∀{i} → D' i
♭ bla = inn bla

-- Should be rejected by termination checker
iter : D ∞ → ⊥
iter (inn t) = iter (♭ t)

false : ⊥
false = iter (♭ bla)


text:
postulate
  H I : Set → Set → Set
  !_  : Set → Set
  X   : Set

infix 1 !_
infix 0 H

syntax H X Y = X , Y
syntax I X Y = Y , X

-- This parsed when default fixity was 'unrelated', but with
-- an actual default fixity (of any strength) in place it really
-- should not.
Foo : Set
Foo = ! X , X


text:
open import Nat
open import Prelude
open import core
open import contexts
open import lemmas-consistency
open import type-assignment-unicity
open import lemmas-progress-checks

-- taken together, the theorems in this file argue that for any expression
-- d, at most one summand of the labeled sum that results from progress may
-- be true at any time: that boxed values, indeterminates, and expressions
-- that step are pairwise disjoint.
--
-- note that as a consequence of currying and comutativity of products,
-- this means that there are three theorems to prove. in addition to those,
-- we also prove several convenince forms that combine theorems about
-- indeterminate and boxed value forms into the same statement about final
-- forms, which mirrors the mutual definition of indeterminate and final
-- and saves some redundant argumentation.
module progress-checks where
  -- boxed values are not indeterminates
  boxedval-not-indet : ∀{d} → d boxedval → d indet → ⊥
  boxedval-not-indet (BVVal VConst) ()
  boxedval-not-indet (BVVal VLam) ()
  boxedval-not-indet (BVArrCast x bv) (ICastArr x₁ ind) = boxedval-not-indet bv ind
  boxedval-not-indet (BVHoleCast x bv) (ICastGroundHole x₁ ind) = boxedval-not-indet bv ind
  boxedval-not-indet (BVHoleCast x bv) (ICastHoleGround x₁ ind x₂) = boxedval-not-indet bv ind

  -- boxed values don't step
  boxedval-not-step : ∀{d} → d boxedval → (Σ[ d' ∈ ihexp ] (d ↦ d')) → ⊥
  boxedval-not-step (BVVal VConst) (d' , Step FHOuter () x₃)
  boxedval-not-step (BVVal VLam) (d' , Step FHOuter () x₃)
  boxedval-not-step (BVArrCast x bv) (d0' , Step FHOuter (ITCastID) FHOuter) = x refl
  boxedval-not-step (BVArrCast x bv) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = boxedval-not-step bv (_ , Step x₁ x₂ x₃)
  boxedval-not-step (BVHoleCast () bv) (d' , Step FHOuter (ITCastID) FHOuter)
  boxedval-not-step (BVHoleCast x bv) (d' , Step FHOuter (ITCastSucceed ()) FHOuter)
  boxedval-not-step (BVHoleCast GHole bv) (_ , Step FHOuter (ITGround (MGArr x)) FHOuter) = x refl
  boxedval-not-step (BVHoleCast x bv) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = boxedval-not-step bv (_ , Step x₁ x₂ x₃)
  boxedval-not-step (BVHoleCast x x₁) (_ , Step FHOuter (ITExpand ()) FHOuter)
  boxedval-not-step (BVHoleCast x x₁) (_ , Step FHOuter (ITCastFail x₂ () x₄) FHOuter)

  mutual
    -- indeterminates don't step
    indet-not-step : ∀{d} → d indet → (Σ[ d' ∈ ihexp ] (d ↦ d')) → ⊥
    indet-not-step IEHole (d' , Step FHOuter () FHOuter)
    indet-not-step (INEHole x) (d' , Step FHOuter () FHOuter)
    indet-not-step (INEHole x) (_ , Step (FHNEHole x₁) x₂ (FHNEHole x₃)) = final-sub-not-trans x x₁ x₂
    indet-not-step (IAp x₁ () x₂) (_ , Step FHOuter (ITLam) FHOuter)
    indet-not-step (IAp x (ICastArr x₁ ind) x₂) (_ , Step FHOuter (ITApCast) FHOuter) = x _ _ _ _ _  refl
    indet-not-step (IAp x ind _) (_ , Step (FHAp1 x₂) x₃ (FHAp1 x₄)) = indet-not-step ind (_ , Step x₂ x₃ x₄)
    indet-not-step (IAp x ind f) (_ , Step (FHAp2 x₃) x₄ (FHAp2 x₆)) = final-not-step f (_ , Step x₃ x₄ x₆)
    indet-not-step (ICastArr x ind) (d0' , Step FHOuter (ITCastID) FHOuter) = x refl
    indet-not-step (ICastArr x ind) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)
    indet-not-step (ICastGroundHole () ind) (d' , Step FHOuter (ITCastID) FHOuter)
    indet-not-step (ICastGroundHole x ind) (d' , Step FHOuter (ITCastSucceed ()) FHOuter)
    indet-not-step (ICastGroundHole GHole ind) (_ , Step FHOuter (ITGround (MGArr x₁)) FHOuter) = x₁ refl
    indet-not-step (ICastGroundHole x ind) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)
    indet-not-step (ICastHoleGround x ind ()) (d' , Step FHOuter (ITCastID ) FHOuter)
    indet-not-step (ICastHoleGround x ind g) (d' , Step FHOuter (ITCastSucceed  x₂) FHOuter) = x _ _ refl
    indet-not-step (ICastHoleGround x ind GHole) (_ , Step FHOuter (ITExpand (MGArr x₂)) FHOuter) = x₂ refl
    indet-not-step (ICastHoleGround x ind g) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)
    indet-not-step (ICastGroundHole x x₁) (_ , Step FHOuter (ITExpand ()) FHOuter)
    indet-not-step (ICastHoleGround x x₁ x₂) (_ , Step FHOuter (ITGround ()) FHOuter)
    indet-not-step (ICastGroundHole x x₁) (_ , Step FHOuter (ITCastFail x₂ () x₄) FHOuter)
    indet-not-step (ICastHoleGround x x₁ x₂) (_ , Step FHOuter (ITCastFail x₃ x₄ x₅) FHOuter) = x _ _ refl
    indet-not-step (IFailedCast x x₁ x₂ x₃) (d' , Step FHOuter () FHOuter)
    indet-not-step (IFailedCast x x₁ x₂ x₃) (_ , Step (FHFailedCast x₄) x₅ (FHFailedCast x₆)) = final-not-step x (_ , Step x₄ x₅ x₆)

    -- final expressions don't step
    final-not-step : ∀{d} → d final → Σ[ d' ∈ ihexp ] (d ↦ d') → ⊥
    final-not-step (FBoxedVal x) stp = boxedval-not-step x stp
    final-not-step (FIndet x) stp = indet-not-step x stp

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
-- Haskell-like do-notation.
module Syntax.Do where

open import Functional
import      Lvl
open import Syntax.Idiom
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable A B : Type{ℓ}
private variable F : Type{ℓ₁} → Type{ℓ₂}

record DoNotation (F : Type{ℓ₁} → Type{ℓ₂}) : Type{Lvl.𝐒(ℓ₁) Lvl.⊔ ℓ₂} where
  constructor intro
  field
    return : A → F(A)
    _>>=_  : F(A) → (A → F(B)) → F(B)

  module HaskellNames where
    _=<<_ : ∀{A B} → (A → F(B)) → F(A) → F(B)
    _=<<_ = swap(_>>=_)

    _>>_ : ∀{A B} → F(A) → F(B) → F(B)
    f >> g = f >>= const g

    _>=>_ : ∀{A B C : Type} → (A → F(B)) → (B → F(C)) → (A → F(C))
    (f >=> g)(A) = f(A) >>= g

    _<=<_ : ∀{A B C : Type} → (B → F(C)) → (A → F(B)) → (A → F(C))
    _<=<_ = swap(_>=>_)

  idiomBrackets : IdiomBrackets(F)
  IdiomBrackets.pure  idiomBrackets = return
  IdiomBrackets._<*>_ idiomBrackets Ff Fa = do
    f <- Ff
    a <- Fa
    return(f(a))

open DoNotation ⦃ … ⦄ using (return ; _>>=_) public

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K #-}
module Model.Terminal where

open import Cats.Category

open import Model.Type.Core
open import Util.HoTT.HLevel
open import Util.Prelude hiding (⊤)

⊤ : ∀ {Δ} → ⟦Type⟧ Δ
⊤ = record
  { ObjHSet = λ _ → HLevel-suc ⊤-HProp
  ; eqHProp = λ _ _ _ → ⊤-HProp
  }

instance
  hasTerminal : ∀ {Δ} → HasTerminal (⟦Types⟧ Δ)
  hasTerminal = record
    { ⊤ = ⊤
    ; isTerminal = λ T → record
      { arr = record {}
      ; unique = λ _ → ≈⁺ λ γ x → refl
      }
    }

private
  open module HT {Δ} = HasTerminal (hasTerminal {Δ}) public using (! ; !-unique)

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module tree-io-example where

open import io
open import list
open import maybe
open import string
open import tree
open import unit
open import nat-to-string

errmsg = "Run with a single (small) number as the command-line argument.\n"

processArgs : 𝕃 string → IO ⊤
processArgs (s :: []) with string-to-ℕ s
... | nothing = putStr errmsg
... | just n = putStr (𝕋-to-string ℕ-to-string (perfect-binary-tree n n)) >> putStr "\n"
processArgs _ = putStr errmsg

main : IO ⊤
main = getArgs >>= processArgs

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module STLC.Syntax where

open import Prelude public

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

-- Types
infixr 7 _⇒_
data 𝒯 : Set
  where
    ⎵    : 𝒯

    _⇒_ : (A B : 𝒯) → 𝒯

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

-- Contexts
data 𝒞 : Set
  where
    ∅   : 𝒞

    _,_ : (Γ : 𝒞) (A : 𝒯) → 𝒞

length : 𝒞 → Nat
length ∅       = zero
length (Γ , x) = suc (length Γ)

lookup : (Γ : 𝒞) (i : Nat) {{_ : True (length Γ >? i)}} → 𝒯
lookup ∅       i       {{()}}
lookup (Γ , A) zero    {{yes}} = A
lookup (Γ , B) (suc i) {{p}}   = lookup Γ i

-- Variables
infix 4 _∋_
data _∋_ : 𝒞 → 𝒯 → Set
  where
    zero : ∀ {Γ A} → Γ , A ∋ A

    suc  : ∀ {Γ A B} → (i : Γ ∋ A)
                     → Γ , B ∋ A

Nat→∋ : ∀ {Γ} → (i : Nat) {{_ : True (length Γ >? i)}}
               → Γ ∋ lookup Γ i
Nat→∋ {Γ = ∅}     i       {{()}}
Nat→∋ {Γ = Γ , A} zero    {{yes}} = zero
Nat→∋ {Γ = Γ , B} (suc i) {{p}}   = suc (Nat→∋ i)

instance
  num∋ : ∀ {Γ A} → Number (Γ ∋ A)
  num∋ {Γ} {A} =
    record
      { Constraint = λ i → Σ (True (length Γ >? i))
                              (λ p → lookup Γ i {{p}} ≡ A)
      ; fromNat    = λ { i {{p , refl}} → Nat→∋ i }
      }

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

-- Terms
infix 3 _⊢_
data _⊢_ : 𝒞 → 𝒯 → Set
  where
    𝓋   : ∀ {Γ A} → (i : Γ ∋ A)
                  → Γ ⊢ A

    ƛ   : ∀ {Γ A B} → (M : Γ , A ⊢ B)
                    → Γ ⊢ A ⇒ B

    _∙_ : ∀ {Γ A B} → (M : Γ ⊢ A ⇒ B) (N : Γ ⊢ A)
                    → Γ ⊢ B

instance
  num⊢ : ∀ {Γ A} → Number (Γ ⊢ A)
  num⊢ {Γ} {A} =
    record
      { Constraint = λ i → Σ (True (length Γ >? i))
                              (λ p → lookup Γ i {{p}} ≡ A)
      ; fromNat    = λ { i {{p , refl}} → 𝓋 (Nat→∋ i) }
      }

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

-- Normal forms
mutual
  infix 3 _⊢ⁿᶠ_
  data _⊢ⁿᶠ_ : 𝒞 → 𝒯 → Set where
    ƛ   : ∀ {Γ A B} → (M : Γ , A ⊢ⁿᶠ B)
                    → Γ ⊢ⁿᶠ A ⇒ B

    ne  : ∀ {Γ} → (M : Γ ⊢ⁿᵉ ⎵)
                → Γ ⊢ⁿᶠ ⎵

  infix 3 _⊢ⁿᵉ_
  data _⊢ⁿᵉ_ : 𝒞 → 𝒯 → Set where
    𝓋   : ∀ {Γ A} → (i : Γ ∋ A)
                  → Γ ⊢ⁿᵉ A

    _∙_ : ∀ {Γ A B} → (M : Γ ⊢ⁿᵉ A ⇒ B) (N : Γ ⊢ⁿᶠ A)
                    → Γ ⊢ⁿᵉ B

instance
  num⊢ⁿᵉ : ∀ {Γ A} → Number (Γ ⊢ⁿᵉ A)
  num⊢ⁿᵉ {Γ} {A} =
    record
      { Constraint = λ i → Σ (True (length Γ >? i))
                              (λ p → lookup Γ i {{p}} ≡ A)
      ; fromNat    = λ { i {{p , refl}} → 𝓋 (Nat→∋ i) }
      }

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Level

module IndexedMap
         {Index : Set} {Key : Index → Set} {_≈_ _<_ : Rel (∃ Key) zero}
         (isOrderedKeySet : IsStrictTotalOrder _≈_ _<_)
         -- Equal keys must have equal indices.
         (indicesEqual : _≈_ =[ proj₁ ]⇒ _≡_)
         (Value : Index → Set)
         where


text:
-- 2012-03-08 Andreas
module NoTerminationCheck1 where

{-# NO_TERMINATION_CHECK #-}

-- error: misplaced pragma

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" using a partial order
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.PartialOrderReasoning
         {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where

open Poset P
import Relation.Binary.PreorderReasoning as PreR
open PreR preorder public renaming (_∼⟨_⟩_ to _≤⟨_⟩_)


text:
open import Level
module Ordinals where

open import zf

open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import Data.Empty
open import  Relation.Binary.PropositionalEquality
open import  logic
open import  nat
open import Data.Unit using ( ⊤ )
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Core

record Oprev {n : Level} (ord : Set n) (osuc :  ord → ord ) (x : ord ) : Set (suc n) where
   field
     oprev : ord
     oprev=x : osuc oprev ≡ x

record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
   field
     ordtrans : {x y z : ord }  → x o< y → y o< z → x o< z
     trio<    : Trichotomous {n} _≡_  _o<_
     ¬x<0     : { x : ord  } → ¬ ( x o< o∅  )
     <-osuc   : { x : ord  } → x o< osuc x
     osuc-≡<  : { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)
     Oprev-p  : ( x : ord  ) → Dec ( Oprev ord osuc x )
     TransFinite : { ψ : ord  → Set (suc n) }
          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
          →  ∀ (x : ord)  → ψ x

record IsNext {n : Level } (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
   field
     x<nx :    { y : ord } → (y o< next y )
     osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
     ¬nx<nx :  {x y : ord} → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z))

record Ordinals {n : Level} : Set (suc (suc n)) where
   field
     Ordinal : Set n
     o∅ : Ordinal
     osuc : Ordinal → Ordinal
     _o<_ : Ordinal → Ordinal → Set n
     next :  Ordinal → Ordinal
     isOrdinal : IsOrdinals Ordinal o∅ osuc _o<_ next
     isNext : IsNext Ordinal o∅ osuc _o<_ next

module inOrdinal  {n : Level} (O : Ordinals {n} ) where

  open Ordinals  O
  open IsOrdinals isOrdinal
  open IsNext isNext

  TransFinite0 : { ψ : Ordinal  → Set n }
          → ( (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
          →  ∀ (x : Ordinal)  → ψ x
  TransFinite0 {ψ} ind x = lower (TransFinite {λ y → Lift (suc n) ( ψ y)} ind1 x) where
       ind1 : (z : Ordinal) → ((y : Ordinal) → y o< z → Lift (suc n) (ψ y)) → Lift (suc n) (ψ z)
       ind1 z prev = lift (ind z (λ y y<z → lower (prev y y<z ) ))

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
module Fin where

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

data Fin : Nat -> Set where
    fzero : {n : Nat} -> Fin (succ n)
    fsucc : {n : Nat} -> Fin n -> Fin (succ n)

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
module sets.nat.ordering.leq.alternative where

open import equality.core
open import equality.calculus
open import function.isomorphism
open import hott.equivalence.logical
open import hott.level.core
open import hott.level.sets
open import sets.nat.core
open import sets.nat.properties
open import sets.nat.ordering.leq.core
open import sets.nat.ordering.leq.level
open import sum

Less : ℕ → ℕ → Set _
Less n m = Σ ℕ λ d → n + d ≡ m

Less-level : ∀ {n m} → h 1 (Less n m)
Less-level {n}{m} = prop⇒h1 λ { (d₁ , p₁) (d₂ , p₂)
  → unapΣ ( +-left-cancel n (p₁ · sym p₂)
          , h1⇒prop (nat-set _ _) _ _) }

leq-sum : ∀ {n m}(p : n ≤ m) → Less n m
leq-sum {m = m} z≤n = m , refl
leq-sum (s≤s p) with leq-sum p
leq-sum (s≤s p) | d , q = d , ap suc q

diff : ∀ {n m} → n ≤ m → ℕ
diff p = proj₁ (leq-sum p)

sum-leq : ∀ n d → n ≤ (n + d)
sum-leq n 0 = ≡⇒≤ (sym (+-right-unit _))
sum-leq n (suc d) = trans≤ (sum-leq n d)
                    (trans≤ suc≤ (≡⇒≤ ( ap suc (+-commutativity n d)
                                      · +-commutativity (suc d) n)))

leq-sum-iso : ∀ {n m} → (n ≤ m) ≅ Less n m
leq-sum-iso = ↔⇒≅ ≤-level Less-level
  ( leq-sum
  , (λ { (d , refl) → sum-leq _ d }))

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Type.Properties.Empty.Proofs where

import      Data.Tuple
open import Data
open import Functional
open import Logic.Propositional
import      Lvl
open import Type.Properties.Inhabited
open import Type.Properties.Empty
open import Type

private variable ℓ : Lvl.Level
private variable A B T : Type{ℓ}

-- A type is never inhabited and empty at the same time.
notInhabitedAndEmpty : (◊ T) → IsEmpty(T) → ⊥
notInhabitedAndEmpty (intro ⦃ obj ⦄) (intro empty) with () ← empty{Empty} (obj)

-- A type being empty is equivalent to the existence of a function from the type to the empty type of any universe level.
empty-negation-eq : IsEmpty(T) ↔ (T → Empty{ℓ})
IsEmpty.empty (Data.Tuple.left empty-negation-eq nt) = empty ∘ nt
Data.Tuple.right empty-negation-eq (intro e) t with () ← e {Empty} t

empty-by-function : (f : A → B) → (IsEmpty{ℓ}(B) → IsEmpty{ℓ}(A))
empty-by-function f (intro empty-B) = intro(empty-B ∘ f)


text:
-- Andreas, 2011-05-30
-- {-# OPTIONS -v tc.lhs.unify:50 #-}
module Issue292 where

data Bool  : Set where true  false  : Bool
data Bool2 : Set where true2 false2 : Bool2

data ⊥ : Set where

infix 3 ¬_

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

infix 4 _≅_

data _≅_ {A : Set} (x : A) : ∀ {B : Set} → B → Set where
  refl : x ≅ x

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

P : Set -> Set
P S = Σ S (\s → s ≅ true)

pbool : P Bool
pbool = true , refl

-- the following should fail:
¬pbool2 : ¬ P Bool2
¬pbool2 ( true2 , () )
¬pbool2 ( false2 , () )

{- using subst, one could now prove distinctness of types, which we don't want
tada : ¬ (Bool ≡ Bool2)
tada eq = ¬pbool2 (subst (\ S → P S) eq pbool )
-}


text:
module Structure.Relator.Equivalence.Proofs where

import      Lvl
open import Functional
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties.Proofs
open import Type

private variable ℓ : Lvl.Level
private variable T A B : Type{ℓ}
private variable _▫_ : T → T → Type{ℓ}
private variable f : A → B

on₂-equivalence : ⦃ eq : Equivalence(_▫_) ⦄ → Equivalence((_▫_) on₂ f)
Equivalence.reflexivity  (on₂-equivalence {_▫_ = _▫_}) = on₂-reflexivity
Equivalence.symmetry     (on₂-equivalence {_▫_ = _▫_}) = on₂-symmetry
Equivalence.transitivity (on₂-equivalence {_▫_ = _▫_}) = on₂-transitivity


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Category.Construction.F-Algebras where

open import Level
open import Data.Product using (proj₁; proj₂)

open import Categories.Category
open import Categories.Functor hiding (id)
open import Categories.Functor.Algebra
open import Categories.Object.Initial
import Categories.Morphism.Reasoning as MR
import Categories.Morphism as Mor using (_≅_)

private
  variable
    o ℓ e : Level
    𝒞 : Category o ℓ e

F-Algebras : {𝒞 : Category o ℓ e} → Endofunctor 𝒞 → Category (ℓ ⊔ o) (e ⊔ ℓ) e
F-Algebras {𝒞 = 𝒞} F = record
  { Obj       = F-Algebra F
  ; _⇒_       = F-Algebra-Morphism
  ; _≈_       = λ α₁ α₂ → f α₁ ≈ f α₂
  ; _∘_       = λ α₁ α₂ → record { f = f α₁ ∘ f α₂ ; commutes = commut α₁ α₂ }
  ; id        = record { f = id ; commutes = identityˡ ○ ⟺ identityʳ ○ ⟺ (∘-resp-≈ʳ identity) }
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  ; ∘-resp-≈  = ∘-resp-≈
  }
  where
    open Category 𝒞
    open Equiv
    open HomReasoning using (⟺; _○_; begin_; _≈⟨_⟩_; _∎)
    open Functor F
    open F-Algebra-Morphism
    open F-Algebra
    commut : {A B C : F-Algebra F} (α₁ : F-Algebra-Morphism B C) (α₂ : F-Algebra-Morphism A B) →
      (f α₁ ∘ f α₂) ∘ α A ≈ α C ∘ F₁ (f α₁ ∘ f α₂)
    commut {A} {B} {C} α₁ α₂ = begin
      (f α₁ ∘ f α₂) ∘ α A            ≈⟨ assoc ○ ∘-resp-≈ʳ (commutes α₂) ⟩
      f α₁ ∘ (α B ∘ F₁ (f α₂))       ≈⟨ ⟺ assoc ○ ∘-resp-≈ˡ (commutes α₁) ⟩
      (α C ∘ F₁ (f α₁)) ∘ F₁ (f α₂)  ≈⟨ assoc ○ ∘-resp-≈ʳ (⟺ homomorphism) ⟩
      α C ∘ F₁ (f α₁ ∘ f α₂)   ∎

module Lambek {𝒞 : Category o ℓ e} {F : Endofunctor 𝒞} (I : Initial (F-Algebras F)) where
  open Category 𝒞
  open Functor F
  open F-Algebra using (α)

  open MR 𝒞 using (glue)
  open Mor 𝒞
  open Initial I -- so ⊥ is an F-Algebra, which is initial

  -- While an expert might be able to decipher the proof at the nLab
  --   (https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor)
  -- I (JC) have found that the notes at
  --   http://www.cs.ru.nl/~jrot/coalgebra/ak-algebras.pdf
  -- are easier to follow, and lead to the full proof below.
  private
    module ⊥ = F-Algebra ⊥
    A = ⊥.A
    a : F₀ A ⇒ A
    a = ⊥.α

    -- The F-Algebra structure that will make things work
    F⊥ : F-Algebra F
    F⊥ = iterate ⊥

    -- By initiality, we get the following morphism
    f : F-Algebra-Morphism ⊥ F⊥
    f = !

    module FAM = F-Algebra-Morphism f

    i : A ⇒ F₀ A
    i = FAM.f

    a∘f : F-Algebra-Morphism ⊥ ⊥
    a∘f = record
      { f = a ∘ i
      ; commutes = glue triv FAM.commutes ○ ∘-resp-≈ʳ (⟺ homomorphism)
      }
      where
        open HomReasoning using (_○_; ⟺)
        triv : CommutativeSquare (α F⊥) (α F⊥) a a
        triv = Equiv.refl

  lambek : A ≅ F₀ A
  lambek = record
    { from = i
    ; to = a
    ; iso = record
      { isoˡ = ⊥-id a∘f
      ; isoʳ = begin
        i ∘ a       ≈⟨ F-Algebra-Morphism.commutes f ⟩
        F₁ a ∘ F₁ i ≈˘⟨ homomorphism ⟩
        F₁ (a ∘ i)  ≈⟨ F-resp-≈ (⊥-id a∘f) ⟩
        F₁ id       ≈⟨ identity ⟩
        id ∎
      }
    }
    where
      open HomReasoning

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
-- ----------------------------------------------------------------------
-- The Agda Descriptor Library
--
-- (Open) Descriptors
-- ----------------------------------------------------------------------

module Data.Desc where

open import Data.List using (List; []; _∷_)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.Product using (Σ; _,_)
open import Data.Var using (_-Scoped[_]; Var; get; zero; suc; tabulate)
open import Data.Unit.Polymorphic using (⊤; tt)

open import Level using (Level; 0ℓ; _⊔_)

open import Relation.Unary using (IUniversal; _⇒_)

private
  variable
    A : Set

1ℓ : Level
1ℓ = Level.suc 0ℓ

-- ----------------------------------------------------------------------
-- Definition
--
-- An open description is a open dependent type theory.
-- Our theoretic model is described by:
--
-- Metatheoretic terms:
--
-- Agda sets          A, B ∷= ...
-- Agda values        x, y ∷= ...
--
-- Open object terms:
--
-- kinds              κ ∷= Set | Π A κ
-- types              T ∷= a | T x | Π A T | T ⟶ T
--
-- A descriptor is a set of well-kinded constructor types.

data Kind : Set₁ where
  `Set₀ : Kind
  `Π : (A : Set) → (A → Kind) → Kind

private
  variable
    κ κ′ : Kind
    Γ : List Kind
    B : A → Kind

infixr 6 _⟶_

data Type : Kind -Scoped[ 1ℓ ] where
  `_ : ∀[ Var κ ⇒ Type κ ]
  _·_ : Type (`Π A B) Γ → (a : A) → Type (B a) Γ
  `Π : (A : Set) → (A → Type `Set₀ Γ) → Type `Set₀ Γ
  _⟶_ : Type `Set₀ Γ → Type `Set₀ Γ → Type `Set₀ Γ

mutual

  data Pos : Type κ Γ → Set where

    `_ : ∀ (x : Var κ Γ)
      -- ----------------
      → Pos (` x)

    _·_ : ∀ {T : Type (`Π A B) Γ}
      → Pos T
      → (a : A)
      -- ------------------------
      → Pos (T · a)

    `Π : (A : Set) {T : A → Type `Set₀ Γ}
      → ((a : A) → Pos (T a))
      -- --------------------------------
      → Pos (`Π A T)

    _⟶_ : ∀ {T T′ : Type `Set₀ Γ}
      → Neg T
      → Pos T′
      -- --------------------------
      → Pos (T ⟶ T′)

  data Neg : Type κ Γ → Set where

    _·_ : ∀ {T : Type (`Π A B) Γ}
      → Neg T
      → (a : A)
      -- ------------------------
      → Neg (T · a)

    `Π : (A : Set) {T : A → Type `Set₀ Γ}
      → ((a : A) → Neg (T a))
      -- --------------------------------
      → Neg (`Π A T)

    _⟶_ : ∀ {T T′ : Type `Set₀ Γ}
      → Pos T
      → Neg T′
      -- --------------------------
      → Neg (T ⟶ T′)

data StrictPos : Type κ Γ → Set where

  `_ : ∀ (x : Var κ Γ)
    -- ----------------
    → StrictPos (` x)

  _·_ : ∀ {T : Type (`Π A B) Γ}
    → StrictPos T
    → (a : A)
    -- ------------------------
    → StrictPos (T · a)

  `Π : (A : Set) {T : A → Type `Set₀ Γ}
    → ((a : A) → StrictPos (T a))
    -- --------------------------------
    → StrictPos (`Π A T)

data Con : Type κ Γ → Set where

  `_ : ∀ (x : Var κ Γ)
  -- ----------------
    → Con (` x)

  _·_ : ∀ {T : Type (`Π A B) Γ}
    → Con T
    → (a : A)
    -- ------------------------
    → Con (T · a)

  `Π : (A : Set) {T : A → Type `Set₀ Γ}
    → ((a : A) → Con (T a))
    -- --------------------------------
    → Con (`Π A T)

  _⟶_ : ∀ {T T′ : Type `Set₀ Γ}
    → StrictPos T
    → Con T′
    -- --------------------------
    → Con (T ⟶ T′)

data Constr : Kind -Scoped[ 1ℓ ] where
  ! : {T : Type κ Γ} → Con T → Constr κ Γ

++⇒C : ∀{T : Type κ Γ} → StrictPos T → Con T
++⇒C (` x) = ` x
++⇒C (P · a) = ++⇒C P · a
++⇒C (`Π A P) = `Π A (λ a → ++⇒C (P a))

Desc : List Kind → Set₁
Desc Γ = List (Constr `Set₀ Γ)

-- ----------------------------------------------------------------------
-- Interpretation

lift⟦_⟧ᴷ : Kind → (ℓ : Level) → Set (Level.suc ℓ)
lift⟦ `Set₀ ⟧ᴷ ℓ = Set ℓ
lift⟦ `Π A κ ⟧ᴷ ℓ = (a : A) → lift⟦ κ a ⟧ᴷ ℓ

-- Lifting of lift⟦_⟧ᴷ to a context
lift⟪_⟫ᴷ : List Kind → (ℓ : Level) → Set (Level.suc ℓ)
lift⟪ Γ ⟫ᴷ ℓ = All (λ κ → lift⟦ κ ⟧ᴷ ℓ) Γ

⟦_⟧ᴷ : Kind → Set₁
⟦ `Set₀ ⟧ᴷ = Set
⟦ `Π A κ ⟧ᴷ = (a : A) → ⟦ κ a ⟧ᴷ

⟪_⟫ᴷ : List Kind → Set₁
⟪ Γ ⟫ᴷ = All ⟦_⟧ᴷ Γ

-- ----------------------------------------------------------------------
-- Fixpoint
--

-- To define the fixed point, we're looking for a fixpoint of the form:
--  μ : Desc Γ → ⟪ Γ ⟫ᴷ
--
-- To consider the interpretation of constructors and type formers,
-- we first describe the terms formed by constructors and
-- positive types:
--
-- constructor terms    c ∷= Constrᵢ | c · a | c · p

private
  variable
    C : Constr `Set₀ Γ
    D : Desc Γ

data Term : Constr `Set₀ Γ -Scoped[ 1ℓ ] where
  `Constr : ∀[ Var C ⇒ Term C ]
  _·_ : ∀ {A} {T : A → Type `Set₀ Γ} {C : (a : A) → Con (T a)}
    → Term (! (`Π A C)) D → (a : A) → Term (! (C a)) D
  _•_ :  ∀ {T T′ : Type `Set₀ Γ} {P : StrictPos T} {C : Con T′}
    → Term (! (P ⟶ C)) D → Term (! (++⇒C P)) D → Term (! C) D

μᵏ : Constr κ Γ → Desc Γ → lift⟦ κ ⟧ᴷ 1ℓ
μᵏ {κ = `Set₀} C D = Term C D
μᵏ {κ = `Π _ _} (! C) D = λ a → μᵏ (! (C · a)) D

μᴰ : Desc Γ → lift⟪ Γ ⟫ᴷ 1ℓ
μᴰ D = tabulate λ x → μᵏ (! (` x)) D

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

ℕᴰ : Desc (`Set₀ ∷ [])
ℕᴰ = ! (` zero) ∷ ! ((` zero) ⟶ (` zero)) ∷ []

`ℕ : Set₁
`ℕ = get zero (μᴰ ℕᴰ)

pattern `zero = `Constr zero
pattern `suc n = `Constr (suc zero) • n

_ : `ℕ
_ = `suc (`suc `zero)

max_stars_repo_name: johnyob/agda-desc

max_issues_repo_name: johnyob/agda-desc

max_forks_repo_name: johnyob/agda-desc


text:
module _ where

module M where

  F : Set → Set
  F A = A

open M

infix 0 F
syntax F A = [ A ]

G : Set → Set
G A = [ A ]


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

-- Composition of pseudofunctors

module Categories.Pseudofunctor.Composition where

open import Data.Product using (_,_)

open import Categories.Bicategory using (Bicategory)
import Categories.Bicategory.Extras as BicategoryExt
open import Categories.Category using (Category)
open import Categories.Category.Instance.One using (shift)
open import Categories.Category.Product using (_⁂_)
open import Categories.Functor using (Functor; _∘F_)
import Categories.Morphism.Reasoning as MorphismReasoning
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; _≃_; niHelper; _ⓘˡ_; _ⓘʳ_)
open import Categories.Pseudofunctor using (Pseudofunctor)

open Category using (module HomReasoning)
open NaturalIsomorphism using (F⇒G; F⇐G)

infixr 9 _∘P_

-- Composition of pseudofunctors

_∘P_ : ∀ {o ℓ e t o′ ℓ′ e′ t′ o″ ℓ″ e″ t″}
         {C : Bicategory o ℓ e t} {D : Bicategory o′ ℓ′ e′ t′}
         {E : Bicategory o″ ℓ″ e″ t″} →
       Pseudofunctor D E → Pseudofunctor C D → Pseudofunctor C E
_∘P_ {o″ = o″} {ℓ″ = ℓ″} {e″ = e″} {C = C} {D = D} {E = E} F G = record
  { P₀             = λ x → F₀ (G₀ x)
  ; P₁             = F₁ ∘F G₁
  ; P-identity     = P-identity
  ; P-homomorphism = P-homomorphism
  ; unitaryˡ       = unitaryˡ
  ; unitaryʳ       = unitaryʳ
  ; assoc          = assoc
  }
  where
    module C  = BicategoryExt C
    module D  = BicategoryExt D
    module E  = BicategoryExt E
    module F  = Pseudofunctor F
    module G  = Pseudofunctor G
    open E
    open F using () renaming (P₀ to F₀; P₁ to F₁)
    open G using () renaming (P₀ to G₀; P₁ to G₁)
    module F₁G₁ {x} {y} = Functor (F₁ {G₀ x} {G₀ y} ∘F G₁ {x} {y})
    open NaturalIsomorphism

    F∘G-id = λ {x} → F₁ ⓘˡ G.P-identity {x}
    F-id   = λ {x} → F.P-identity {G₀ x}

    P-identity : ∀ {x} → E.id ∘F shift o″ ℓ″ e″ ≃ (F₁ ∘F G₁) ∘F (C.id {x})
    P-identity {x} = niHelper (record
      { η       = λ _ → ⇒.η F∘G-id _ ∘ᵥ ⇒.η F-id _
      ; η⁻¹     = λ _ → ⇐.η F-id _ ∘ᵥ ⇐.η F∘G-id _
      ; commute = λ _ → glue (⇒.commute F∘G-id _) (⇒.commute F-id _)
      ; iso     = λ _ → record
        { isoˡ = begin
            (⇐.η F-id _ ∘ᵥ ⇐.η F∘G-id _) ∘ᵥ ⇒.η F∘G-id _ ∘ᵥ ⇒.η F-id _
          ≈⟨ cancelInner (iso.isoˡ F∘G-id _) ⟩
            ⇐.η F-id _ ∘ᵥ ⇒.η F-id _
          ≈⟨ iso.isoˡ F-id _ ⟩
            id₂
          ∎
        ; isoʳ = begin
            (⇒.η F∘G-id _ ∘ᵥ ⇒.η F-id _) ∘ᵥ ⇐.η F-id _ ∘ᵥ ⇐.η F∘G-id _
          ≈⟨ cancelInner (iso.isoʳ F-id _) ⟩
            ⇒.η F∘G-id _ ∘ᵥ ⇐.η F∘G-id _
          ≈⟨ iso.isoʳ F∘G-id _ ⟩
            id₂
          ∎
        }
      })
      where
        FGx = F₀ (G₀ x)
        open HomReasoning (hom FGx FGx)
        open MorphismReasoning (hom FGx FGx)

    F∘G-h = λ {x y z} → F₁ ⓘˡ G.P-homomorphism {x} {y} {z}
    F-h∘G = λ {x y z} → F.P-homomorphism {G₀ x} {G₀ y} {G₀ z} ⓘʳ (G₁ ⁂ G₁)

    P-homomorphism : ∀ {x y z} →
                     E.⊚ ∘F (F₁ ∘F G₁ ⁂ F₁ ∘F G₁) ≃
                       (F₁ ∘F G₁) ∘F C.⊚ {x} {y} {z}
    P-homomorphism {x} {y} {z} = niHelper (record
      { η       = λ f,g → ⇒.η F∘G-h f,g ∘ᵥ ⇒.η F-h∘G f,g
      ; η⁻¹     = λ f,g → ⇐.η F-h∘G f,g ∘ᵥ ⇐.η F∘G-h f,g
      ; commute = λ α,β → glue (⇒.commute F∘G-h α,β) (⇒.commute F-h∘G α,β)
      ; iso     = λ f,g → record
        { isoˡ = cancelInner (iso.isoˡ F∘G-h f,g) ○ iso.isoˡ F-h∘G f,g
        ; isoʳ = cancelInner (iso.isoʳ F-h∘G f,g) ○ iso.isoʳ F∘G-h f,g
        }
      })
      where
        FGx = F₀ (G₀ x)
        FGz = F₀ (G₀ z)
        open HomReasoning (hom FGx FGz)
        open MorphismReasoning (hom FGx FGz)

    Pid  = λ {A} → NaturalTransformation.η (F⇒G (P-identity {A})) _
    Phom = λ {x} {y} {z} f,g →
           NaturalTransformation.η (F⇒G (P-homomorphism {x} {y} {z})) f,g
    λ⇒   = unitorˡ.from
    ρ⇒   = unitorʳ.from
    α⇒   = associator.from

    unitaryˡ : ∀ {x y} {f : x C.⇒₁ y} →
               let open ComHom in
               [ id₁ ⊚₀ F₁G₁.₀ f ⇒ F₁G₁.₀ f ]⟨
                 Pid ⊚₁ id₂             ⇒⟨ F₁G₁.₀ C.id₁ ⊚₀ F₁G₁.₀ f ⟩
                 Phom (C.id₁ , f)       ⇒⟨ F₁G₁.₀ (C.id₁ C.⊚₀ f) ⟩
                 F₁G₁.₁ C.unitorˡ.from
               ≈ E.unitorˡ.from
               ⟩
    unitaryˡ {x} {y} {f} = begin
        F₁G₁.₁ C.unitorˡ.from ∘ᵥ Phom (C.id₁ , f) ∘ᵥ Pid ⊚₁ id₂
      ≡⟨⟩
        F₁.₁ (G₁.₁ C.unitorˡ.from) ∘ᵥ
        (⇒.η F∘G-h (C.id₁ , f) ∘ᵥ ⇒.η F-h∘G (C.id₁ , f)) ∘ᵥ
        (⇒.η F∘G-id _ ∘ᵥ ⇒.η F-id _) ⊚₁ id₂
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ E.∘ᵥ-distr-◁ ⟩
        F₁.₁ (G₁.₁ C.unitorˡ.from) ∘ᵥ
        (⇒.η F∘G-h (C.id₁ , f) ∘ᵥ ⇒.η F-h∘G (C.id₁ , f)) ∘ᵥ
        ⇒.η F∘G-id _ ⊚₁ id₂ ∘ᵥ ⇒.η F-id _ ⊚₁ id₂
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ E.⊚.F-resp-≈ (hom.Equiv.refl , F₁.identity) ⟩∘⟨refl ⟩
        F₁.₁ (G₁.₁ C.unitorˡ.from) ∘ᵥ
        (⇒.η F∘G-h (C.id₁ , f) ∘ᵥ ⇒.η F-h∘G (C.id₁ , f)) ∘ᵥ
        ⇒.η F∘G-id _ ⊚₁ F₁.₁ D.id₂ ∘ᵥ ⇒.η F-id _ ⊚₁ id₂
      ≈⟨ refl⟩∘⟨ extend² (F.Hom.commute (G.unitˡ.η _ , D.id₂)) ⟩
        F₁.₁ (G₁.₁ C.unitorˡ.from) ∘ᵥ
        (⇒.η F∘G-h (C.id₁ , f) ∘ᵥ F₁.₁ (G.unitˡ.η _ D.⊚₁ D.id₂)) ∘ᵥ
        F.Hom.η (D.id₁ , G₁.₀ f) ∘ᵥ ⇒.η F-id _ ⊚₁ id₂
      ≈˘⟨ pushˡ (F₁.homomorphism ○ hom.∘-resp-≈ʳ F₁.homomorphism) ⟩
        F₁.₁ (G₁.₁ C.unitorˡ.from D.∘ᵥ
              G.Hom.η (C.id₁ , f) D.∘ᵥ G.unitˡ.η _ D.⊚₁ D.id₂) ∘ᵥ
        F.Hom.η (D.id₁ , G₁.₀ f) ∘ᵥ ⇒.η F-id _ ⊚₁ id₂
      ≈⟨ F₁.F-resp-≈ G.unitaryˡ ⟩∘⟨refl ⟩
        F₁.₁ (D.unitorˡ.from) ∘ᵥ
        F.Hom.η (D.id₁ , G₁.₀ f) ∘ᵥ ⇒.η F-id _ ⊚₁ id₂
      ≈⟨ F.unitaryˡ ⟩
        E.unitorˡ.from
      ∎
      where
        FGx = F₀ (G₀ x)
        FGy = F₀ (G₀ y)
        open HomReasoning (hom FGx FGy)
        open MorphismReasoning (hom FGx FGy)

    unitaryʳ : ∀ {x y} {f : x C.⇒₁ y} →
               let open ComHom in
               [ F₁G₁.₀ f ⊚₀ id₁ ⇒ F₁G₁.₀ f ]⟨
                 id₂ ⊚₁ Pid             ⇒⟨ F₁G₁.₀ f ⊚₀ F₁G₁.₀ C.id₁ ⟩
                 Phom (f , C.id₁)       ⇒⟨ F₁G₁.₀ (f C.⊚₀ C.id₁) ⟩
                 F₁G₁.₁ C.unitorʳ.from
               ≈ E.unitorʳ.from
               ⟩
    unitaryʳ {x} {y} {f} = begin
        F₁G₁.₁ C.unitorʳ.from ∘ᵥ Phom (f , C.id₁) ∘ᵥ id₂ ⊚₁ Pid
      ≡⟨⟩
        F₁.₁ (G₁.₁ C.unitorʳ.from) ∘ᵥ
        (⇒.η F∘G-h (f , C.id₁) ∘ᵥ ⇒.η F-h∘G (f , C.id₁)) ∘ᵥ
        id₂ ⊚₁ (⇒.η F∘G-id _ ∘ᵥ ⇒.η F-id _)
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ E.∘ᵥ-distr-▷ ⟩
        F₁.₁ (G₁.₁ C.unitorʳ.from) ∘ᵥ
        (⇒.η F∘G-h (f , C.id₁) ∘ᵥ ⇒.η F-h∘G (f , C.id₁)) ∘ᵥ
        id₂ ⊚₁ ⇒.η F∘G-id _ ∘ᵥ id₂ ⊚₁ ⇒.η F-id _
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ E.⊚.F-resp-≈ (F₁.identity , hom.Equiv.refl) ⟩∘⟨refl ⟩
        F₁.₁ (G₁.₁ C.unitorʳ.from) ∘ᵥ
        (⇒.η F∘G-h (f , C.id₁) ∘ᵥ ⇒.η F-h∘G (f , C.id₁)) ∘ᵥ
        F₁.₁ D.id₂ ⊚₁ ⇒.η F∘G-id _ ∘ᵥ id₂ ⊚₁ ⇒.η F-id _
      ≈⟨ refl⟩∘⟨ extend² (F.Hom.commute (D.id₂ , G.unitˡ.η _)) ⟩
        F₁.₁ (G₁.₁ C.unitorʳ.from) ∘ᵥ
        (⇒.η F∘G-h (f , C.id₁) ∘ᵥ F₁.₁ (D.id₂ D.⊚₁ G.unitˡ.η _)) ∘ᵥ
        F.Hom.η (G₁.₀ f , D.id₁) ∘ᵥ id₂ ⊚₁ ⇒.η F-id _
      ≈˘⟨ pushˡ (F₁.homomorphism ○ hom.∘-resp-≈ʳ F₁.homomorphism) ⟩
        F₁.₁ (G₁.₁ C.unitorʳ.from D.∘ᵥ
              G.Hom.η (f , C.id₁) D.∘ᵥ D.id₂ D.⊚₁ G.unitˡ.η _) ∘ᵥ
        F.Hom.η (G₁.₀ f , D.id₁) ∘ᵥ id₂ ⊚₁ ⇒.η F-id _
      ≈⟨ F₁.F-resp-≈ G.unitaryʳ ⟩∘⟨refl ⟩
        F₁.₁ (D.unitorʳ.from) ∘ᵥ
        F.Hom.η (G₁.₀ f , D.id₁) ∘ᵥ id₂ ⊚₁ ⇒.η F-id _
      ≈⟨ F.unitaryʳ ⟩
        E.unitorʳ.from
      ∎
      where
        FGx = F₀ (G₀ x)
        FGy = F₀ (G₀ y)
        open HomReasoning (hom FGx FGy)
        open MorphismReasoning (hom FGx FGy)

    assoc : ∀ {x y z w} {f : x C.⇒₁ y} {g : y C.⇒₁ z} {h : z C.⇒₁ w} →
            let open ComHom in
            [ (F₁G₁.₀ h ⊚₀ F₁G₁.₀ g) ⊚₀ F₁G₁.₀ f ⇒ F₁G₁.₀ (h C.⊚₀ (g C.⊚₀ f)) ]⟨
              Phom (h , g) ⊚₁ id₂     ⇒⟨ F₁G₁.₀ (h C.⊚₀ g) ⊚₀ F₁G₁.₀ f ⟩
              Phom (_ , f)            ⇒⟨ F₁G₁.₀ ((h C.⊚₀ g) C.⊚₀ f) ⟩
              F₁G₁.₁ C.associator.from
            ≈ E.associator.from       ⇒⟨ F₁G₁.₀ h ⊚₀ (F₁G₁.₀ g ⊚₀ F₁G₁.₀ f) ⟩
              id₂ ⊚₁ Phom (g , f)     ⇒⟨ F₁G₁.₀ h ⊚₀ F₁G₁.₀ (g C.⊚₀ f) ⟩
              Phom (h , _)
            ⟩
    assoc {x} {_} {_} {w} {f} {g} {h} = begin
        F₁G₁.₁ C.associator.from ∘ᵥ Phom (_ , f) ∘ᵥ Phom (h , g) ⊚₁ id₂
      ≡⟨⟩
        F₁.₁ (G₁.₁ C.associator.from) ∘ᵥ
        (⇒.η F∘G-h (_ , f) ∘ᵥ ⇒.η F-h∘G (_ , f)) ∘ᵥ
        (⇒.η F∘G-h (h , g) ∘ᵥ ⇒.η F-h∘G (h , g)) ⊚₁ id₂
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ E.∘ᵥ-distr-◁ ⟩
        F₁.₁ (G₁.₁ C.associator.from) ∘ᵥ
        (⇒.η F∘G-h (_ , f) ∘ᵥ ⇒.η F-h∘G (_ , f)) ∘ᵥ
        ⇒.η F∘G-h (h , g) ⊚₁ id₂ ∘ᵥ ⇒.η F-h∘G (h , g) ⊚₁ id₂
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ E.⊚.F-resp-≈ (hom.Equiv.refl , F₁.identity) ⟩∘⟨refl ⟩
        F₁.₁ (G₁.₁ C.associator.from) ∘ᵥ
        (⇒.η F∘G-h (_ , f) ∘ᵥ ⇒.η F-h∘G (_ , f)) ∘ᵥ
        ⇒.η F∘G-h (h , g) ⊚₁ F₁.₁ D.id₂ ∘ᵥ ⇒.η F-h∘G (h , g) ⊚₁ id₂
      ≈⟨ refl⟩∘⟨ extend² (F.Hom.commute (G.Hom.η (h , g) , D.id₂)) ⟩
        F₁.₁ (G₁.₁ C.associator.from) ∘ᵥ
        (⇒.η F∘G-h (_ , f) ∘ᵥ F₁.₁ (G.Hom.η (h , g) D.⊚₁ D.id₂)) ∘ᵥ
        F.Hom.η (_ , G₁.₀ f) ∘ᵥ ⇒.η F-h∘G (h , g) ⊚₁ id₂
      ≈˘⟨ pushˡ (F₁.homomorphism ○ hom.∘-resp-≈ʳ F₁.homomorphism) ⟩
        F₁.₁ (G₁.₁ C.associator.from D.∘ᵥ
              G.Hom.η (_ , f) D.∘ᵥ G.Hom.η (h , g) D.⊚₁ D.id₂) ∘ᵥ
        F.Hom.η (_ , G₁.₀ f) ∘ᵥ ⇒.η F-h∘G (h , g) ⊚₁ id₂
      ≈⟨ F₁.F-resp-≈ G.assoc ⟩∘⟨refl ⟩
        F₁.₁ (G.Hom.η (h , _) D.∘ᵥ D.id₂ D.⊚₁ G.Hom.η (g , f) D.∘ᵥ
              D.associator.from) ∘ᵥ
        F.Hom.η (_ , G₁.₀ f) ∘ᵥ ⇒.η F-h∘G (h , g) ⊚₁ id₂
      ≈⟨ (F₁.homomorphism ○ pushʳ F₁.homomorphism) ⟩∘⟨refl ⟩
        ((⇒.η F∘G-h (h , _) ∘ᵥ F₁.₁ (D.id₂ D.⊚₁ G.Hom.η (g , f))) ∘ᵥ
         F₁.₁ D.associator.from) ∘ᵥ
        F.Hom.η (_ , G₁.₀ f) ∘ᵥ ⇒.η F-h∘G (h , g) ⊚₁ id₂
      ≈⟨ pullʳ F.assoc ⟩
        (⇒.η F∘G-h (h , _) ∘ᵥ F₁.₁ (D.id₂ D.⊚₁ G.Hom.η (g , f))) ∘ᵥ
        F.Hom.η (G₁.₀ h , _) ∘ᵥ id₂ ⊚₁ ⇒.η F-h∘G (g , f) ∘ᵥ
        E.associator.from
      ≈˘⟨ extend² (F.Hom.commute (D.id₂ , G.Hom.η (g , f))) ⟩
        (⇒.η F∘G-h (h , _) ∘ᵥ ⇒.η F-h∘G (h , _)) ∘ᵥ
        F₁.₁ D.id₂ ⊚₁ ⇒.η F∘G-h (g , f) ∘ᵥ id₂ ⊚₁ ⇒.η F-h∘G (g , f) ∘ᵥ
        E.associator.from
      ≈⟨ refl⟩∘⟨ pullˡ (E.⊚.F-resp-≈ (F₁.identity , hom.Equiv.refl) ⟩∘⟨refl) ⟩
        (⇒.η F∘G-h (h , _) ∘ᵥ ⇒.η F-h∘G (h , _)) ∘ᵥ
        (id₂ ⊚₁ ⇒.η F∘G-h (g , f) ∘ᵥ id₂ ⊚₁ ⇒.η F-h∘G (g , f)) ∘ᵥ
        E.associator.from
      ≈⟨ refl⟩∘⟨ E.∘ᵥ-distr-▷ ⟩∘⟨refl ⟩
        (⇒.η F∘G-h (h , _) ∘ᵥ ⇒.η F-h∘G (h , _)) ∘ᵥ
        id₂ ⊚₁ (⇒.η F∘G-h (g , f) ∘ᵥ ⇒.η F-h∘G (g , f)) ∘ᵥ
        E.associator.from
      ≡⟨⟩
        Phom (h , _) ∘ᵥ id₂ ⊚₁ Phom (g , f) ∘ᵥ E.associator.from
      ∎
      where
        FGx = F₀ (G₀ x)
        FGw = F₀ (G₀ w)
        open HomReasoning (hom FGx FGw)
        open MorphismReasoning (hom FGx FGw)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories