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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Application {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Weakening
import Definition.LogicalRelation.Substitution.Irrelevance as S

open import Tools.Product
import Tools.PropositionalEquality as PE

import Data.Nat as Nat

-- Application of valid terms.
appᵛ : ∀ {F G rF lF lG rΠ lΠ t u Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([F] : Γ ⊩ᵛ⟨ l ⟩ F ^ [ rF , ι lF ] / [Γ])
       ([ΠFG] : Γ ⊩ᵛ⟨ l ⟩ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ rΠ , ι lΠ ] / [Γ])
       ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ rΠ , ι lΠ ] / [Γ] / [ΠFG])
       ([u] : Γ ⊩ᵛ⟨ l ⟩ u ∷ F ^ [ rF , ι lF ] / [Γ] / [F])
     → Γ ⊩ᵛ⟨ l ⟩ t ∘ u ^ lΠ ∷ G [ u ] ^ [ rΠ , ι lG ] / [Γ] / substSΠ {F} {G} {u} [Γ] [F] [ΠFG] [u]
appᵛ {F} {G} {rF} {lF} {lG} {rΠ} {lΠ} {t} {u} [Γ] [F] [ΠFG] [t] [u] {σ = σ} ⊢Δ [σ] =
  let [G[u]] = substSΠ {F} {G} {u} [Γ] [F] [ΠFG] [u]
      [σF] = proj₁ ([F] ⊢Δ [σ])
      [σΠFG] = proj₁ ([ΠFG] ⊢Δ [σ])
      [σt] = proj₁ ([t] ⊢Δ [σ])
      [σu] = proj₁ ([u] ⊢Δ [σ])
      [σG[u]]  = proj₁ ([G[u]] ⊢Δ [σ])
      [σG[u]]′ = irrelevance′ (singleSubstLift G u) [σG[u]]
  in  irrelevanceTerm′ (PE.sym (singleSubstLift G u)) PE.refl PE.refl
                       [σG[u]]′ [σG[u]]
                       (appTerm PE.refl [σF] [σG[u]]′ [σΠFG] [σt] [σu])
  ,   (λ [σ′] [σ≡σ′] →
         let [σu′] = convTerm₂ [σF] (proj₁ ([F] ⊢Δ [σ′]))
                               (proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′])
                               (proj₁ ([u] ⊢Δ [σ′]))
         in  irrelevanceEqTerm′ (PE.sym (singleSubstLift G u)) PE.refl PE.refl
                                [σG[u]]′ [σG[u]]
                                (app-congTerm [σF] [σG[u]]′ [σΠFG]
                                              (proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′])
                                              [σu] [σu′]
                                              (proj₂ ([u] ⊢Δ [σ]) [σ′] [σ≡σ′])))

-- Application congurence of valid terms.
app-congᵛ : ∀ {F G rF lF lG rΠ lΠ t u a b Γ l}
            ([Γ] : ⊩ᵛ Γ)
            ([F] : Γ ⊩ᵛ⟨ l ⟩ F ^ [ rF , ι lF ] / [Γ])
            ([ΠFG] : Γ ⊩ᵛ⟨ l ⟩ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ rΠ , ι lΠ ] / [Γ])
            ([t≡u] : Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ rΠ , ι lΠ ] / [Γ] / [ΠFG])
            ([a] : Γ ⊩ᵛ⟨ l ⟩ a ∷ F ^ [ rF , ι lF ] / [Γ] / [F])
            ([b] : Γ ⊩ᵛ⟨ l ⟩ b ∷ F ^ [ rF , ι lF ] / [Γ] / [F])
            ([a≡b] : Γ ⊩ᵛ⟨ l ⟩ a ≡ b ∷ F ^ [ rF , ι lF ] / [Γ] / [F])
          → Γ ⊩ᵛ⟨ l ⟩ t ∘ a ^ lΠ ≡ u ∘ b ^ lΠ ∷ G [ a ] ^ [ rΠ , ι lG ] / [Γ]
              / substSΠ {F} {G} {a} [Γ] [F] [ΠFG] [a]
app-congᵛ {F} {G} {rF} {lF} {lG} {rΠ} {a = a} [Γ] [F] [ΠFG] [t≡u] [a] [b] [a≡b] ⊢Δ [σ] =
  let [σF] = proj₁ ([F] ⊢Δ [σ])
      [G[a]]  = proj₁ (substSΠ {F} {G} {a} [Γ] [F] [ΠFG] [a] ⊢Δ [σ])
      [G[a]]′ = irrelevance′ (singleSubstLift G a) [G[a]]
      [σΠFG] = proj₁ ([ΠFG] ⊢Δ [σ])
      [σa] = proj₁ ([a] ⊢Δ [σ])
      [σb] = proj₁ ([b] ⊢Δ [σ])
  in  irrelevanceEqTerm′ (PE.sym (singleSubstLift G a)) PE.refl PE.refl [G[a]]′ [G[a]]
                         (app-congTerm [σF] [G[a]]′ [σΠFG] ([t≡u] ⊢Δ [σ])
                                       [σa] [σb] ([a≡b] ⊢Δ [σ]))

appᵛ↑ : ∀ {F F' G rF rF' lF lF' lG rΠ lΠ t u Γ l}
       (lF≤ : lF ≤ lΠ)
       (lG≤ : lG ≤ lΠ)
       ([Γ] : ⊩ᵛ Γ)
       ([F] : Γ ⊩ᵛ⟨ l ⟩ F ^ [ rF , ι lF ] / [Γ])
       ([F'] : Γ ⊩ᵛ⟨ l ⟩ F' ^ [ rF' , ι lF' ] / [Γ])
       ([G] : Γ ∙ F ^ [ rF , ι lF ] ⊩ᵛ⟨ l ⟩ G ^ [ rΠ , ι lG ] / [Γ] ∙ [F])
       ([ΠFG] : Γ ⊩ᵛ⟨ l ⟩ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ rΠ , ι lΠ ] / [Γ])
       ([t] : Γ ∙ F' ^ [ rF' , ι lF' ] ⊩ᵛ⟨ l ⟩ t ∷ wk1 (Π F ^ rF ° lF ▹ G ° lG ° lΠ) ^ [ rΠ , ι lΠ ] / [Γ] ∙ [F'] / wk1ᵛ {A = Π F ^ rF ° lF ▹ G ° lG ° lΠ} {F = F'} [Γ] [F'] [ΠFG])
       ([u] : Γ ∙ F' ^ [ rF' , ι lF' ] ⊩ᵛ⟨ l ⟩ u ∷ wk1 F ^ [ rF , ι lF ] / [Γ] ∙ [F'] / wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F])
         → Γ ∙ F' ^ [ rF' , ι lF' ] ⊩ᵛ⟨ l ⟩ t ∘ u ^ lΠ ∷ G [ u ]↑ ^ [ rΠ , ι lG ] / [Γ] ∙ [F'] / subst↑S {F'} {G} {u} {F' = F} [Γ] [F'] [F] [G] [u]
appᵛ↑ {F} {F'} {G} {rF} {rF'} {lF} {lF'} {lG} {rΠ} {lΠ} {t} {u} lF≤ lG≤ [Γ] [F] [F'] [G] [ΠFG] [t] [u] =
  let [G[u]] = subst↑S {F'} {G} {u} {F' = F} [Γ] [F'] [F] [G] [u]
      [wF] = wk1ᵛ {A = F} {F = F'} [Γ] [F'] [F]
      [wΠFG] = wk1ᵛ {A = Π F ^ rF ° lF ▹ G ° lG ° lΠ} {F = F'} [Γ] [F'] [ΠFG]
      [app] = appᵛ {F = wk1 F} {G = wk1d G} {t = t} {u = u} (_∙_ {A = F'} [Γ] [F']) [wF] [wΠFG] [t] [u]
  in S.irrelevanceTerm′ {A = wk1d G [ u ]} {A′ =  G [ u ]↑} {t = t ∘ u ^ lΠ} (PE.sym (wk1d[]-[]↑ G u)) PE.refl (_∙_ {A = F'} [Γ] [F']) (_∙_ {A = F'} [Γ] [F'])
                        (substSΠ {wk1 F} {wk1d G} {u} (_∙_ {A = F'} [Γ] [F']) [wF] [wΠFG] [u]) [G[u]] [app]

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Literals.Definition.Negative where

open import Light.Library.Data.Natural as ℕ using (ℕ ; zero ; successor) renaming (ℓ to nℓ)
open import Light.Level using (++_ ; _⊔_)
open import Light.Variable.Sets
open import Light.Variable.Levels
open import Light.Package using (Package)

record FromNegative ⦃ package : Package record { ℕ } ⦄ (𝕒 : Set ℓ) : Set (++ (nℓ ⊔ ℓ)) where
      field convert : ℕ → 𝕒

open FromNegative ⦃ ... ⦄ using (convert)
open import Agda.Builtin.Nat as Nat using (Nat)

private
      change : ∀ ⦃ package : Package record { ℕ } ⦄ → Nat → ℕ
      change Nat.zero = zero
      change (Nat.suc n) = successor (change n)

from‐literal : ∀ ⦃ package : Package record { ℕ } ⦄ ⦃ natural : FromNegative 𝕒 ⦄ (n : Nat) → 𝕒
from‐literal n = convert (change n)
{-# BUILTIN FROMNEG from‐literal #-}

ext: agda

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module Cats.Category.Setoids.Facts.Exponentials where

open import Data.Product using (_,_)
open import Relation.Binary using (Setoid)

open import Cats.Category
open import Cats.Category.Setoids as Setoids using (Setoids ; ≈-intro ; ≈-elim)
open import Cats.Category.Setoids.Facts.Products as Products using
  (hasBinaryProducts)
open import Cats.Util.Conv

import Relation.Binary.PropositionalEquality as ≡

import Cats.Category.Base as Base
import Cats.Util.SetoidReasoning as SetoidReasoning

module Build l where

  infixr 1 _↝_

  open Base.Category (Setoids l l)
  open Category (Setoids l l) using (∃!-intro ; Exp ; IsUniqueSuchThat)
  open HasBinaryProducts (hasBinaryProducts l l)
  open Setoids._⇒_ using (resp)

  _↝_ : Obj → Obj → Obj
  A ↝ B = record
      { Carrier = A ⇒ B
      ; _≈_ = _≈_ {A} {B}
      ; isEquivalence = equiv
      }

  eval : ∀ {B C} → (B ↝ C) × B ⇒ C
  eval = record
      { arr = λ { (f , x) → (f ⃗) x }
      ; resp = λ { (eq₁ , eq₂) → ≈-elim eq₁ eq₂ }
      }

  curry : ∀ {A B C} → A × B ⇒ C → A ⇒ B ↝ C
  curry {A} f = record
      { arr = λ a → record
           { arr = λ b → (f ⃗) (a , b)
           ; resp = λ eqb → resp f (refl , eqb)
           }
      ; resp = λ eqa → ≈-intro λ eqb → resp f (eqa , eqb)
      }
    where
      open Setoid A using (refl)

  curry-correct : ∀ {A B C} (f : A × B ⇒ C)
    → eval ∘ ⟨ curry f × id ⟩ ≈ f
  curry-correct f = ≈-intro (resp f)

  curry-unique : ∀ {A B C} (f : A × B ⇒ C)
    → IsUniqueSuchThat (λ f̃ → eval ∘ ⟨ f̃ × id ⟩ ≈ f) (curry f)
  curry-unique {A} {B} {C} f {g} eval∘g≈f
      = ≈-intro λ {a} {a′} a≈a′ → ≈-intro λ {b} {b′} b≈b′ →
        begin⟨ C ⟩
          ((((curry f) ⃗) a) ⃗) b
        ≡⟨⟩
          (f ⃗) (a , b)
        ≈⟨ sym C (≈-elim eval∘g≈f (sym A a≈a′ , sym B b≈b′)) ⟩
          (((g ⃗) a′) ⃗) b′
        ∎
    where
      open SetoidReasoning
      open Setoid using (sym)

  _↝′_ : ∀ B C → Exp B C
  B ↝′ C = record
      { Cᴮ = B ↝ C
      ; eval = eval
      ; curry′ = λ f → ∃!-intro
          (curry f)
          (curry-correct f)
          (λ {g} eval∘g≈f → curry-unique f {g} eval∘g≈f)
      }

instance
  hasExponentials : ∀ l → HasExponentials (Setoids l l)
  hasExponentials l = record { _↝′_ = Build._↝′_ l }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
------------------------------------------------------------------------------
-- Testing the function FOL.Translation.Terms.termToFOLTerm: Con term
------------------------------------------------------------------------------

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

module TermToFOLTerm.ConTerm where

-- We add 3 to the fixities of the standard library.
infixl 9 _+_
infix  7 _≡_

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

data ℕ : Set where
  zero :     ℕ
  succ : ℕ → ℕ

data _≡_ (m : ℕ) : ℕ → Set where
  refl : m ≡ m

sym : ∀ {x y} → x ≡ y → y ≡ x
sym refl = refl

_+_ : ℕ → ℕ → ℕ
zero   + n = n
succ m + n = succ (m + n)

+-Sx : ∀ m n → succ m + n ≡ succ (m + n)
+-Sx m n = refl
{-# ATP hint +-Sx #-}

postulate
  +-rightIdentity : ∀ n → n + zero ≡ n
  x+Sy≡S[x+y] : ∀ m n → m + succ n ≡ succ (m + n)

+-comm : ∀ m n → m + n ≡ n + m
+-comm zero     n = sym (+-rightIdentity n)
+-comm (succ m) n = prf (+-comm m n)
  where
  postulate prf : m + n ≡ n + m →
                  succ m + n ≡ n + succ m
  {-# ATP prove prf x+Sy≡S[x+y] #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Numeral.Matrix.Relations where

open import Data.Tuple as Tuple using (_,_)
open import Logic.Predicate
open import Logic
open import Numeral.Matrix hiding (module SquareMatrix)
open import Numeral.Matrix.OverField
import      Relator.Equals as Eq
open import Structure.Operator.Field
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Setoid
open import Syntax.Function
open import Type

module SquareMatrix {ℓ ℓₑ} {d} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  record Symmetric(M : SquareMatrix(d)(T)) : Stmt{ℓₑ} where
    constructor intro
    field proof : ∀{x y} → Matrix.proj M(x , y) ≡ Matrix.proj M(y , x)

  module _ {_▫_ : T → T → T} ⦃ monoid : Monoid(_▫_) ⦄ where
    record Diagonal(M : SquareMatrix(d)(T)) : Stmt{ℓₑ} where
      constructor intro
      field proof : ∀{x y} → (x Eq.≢ y) → (Matrix.proj M(x , y) ≡ Monoid.id monoid)

    record Scalar (s : T) (M : SquareMatrix(d)(T)) : Stmt{ℓₑ} where
      constructor intro
      field
        ⦃ diagonal ⦄ : Diagonal(M)
        proof : ∀{x} → (Matrix.proj M(x , x) ≡ s)

  module _ {_+ₛ_ _⋅ₛ_ : T → T → T} ⦃ field-structure : Field(_+ₛ_)(_⋅ₛ_) ⦄ where
    record Similar(A B : SquareMatrix(d)(T)) : Stmt{ℓₑ} where
      constructor intro
      field proof : ∃(P ↦ ∃{Obj = Invertible(P)}(inver ↦ B ≡ inv(P) ⨯ A ⨯ P))

    record Diagonalizable(M : SquareMatrix(d)(T)) : Stmt{ℓₑ} where
      constructor intro
      field proof : ∃(P ↦ ∃{Obj = Invertible(P)}(inver ↦ Diagonal(inv(P) ⨯ M ⨯ P)))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Text.Parse (Tok : Set) where

open import Prelude

private
  data P′ (A : Set) : Set where
    symbolBind : (Tok → P′ A) → P′ A
    fail′ : P′ A
    returnPlus : A → P′ A → P′ A

  _+++′_ : ∀ {A} → P′ A → P′ A → P′ A
  symbolBind f +++′ symbolBind g = symbolBind λ x → f x +++′ g x
  fail′ +++′ q = q
  p +++′ fail′ = p
  returnPlus x p +++′ q = returnPlus x (p +++′ q)
  p +++′ returnPlus x q = returnPlus x (p +++′ q)

  parse′ : ∀ {A} → P′ A → List Tok → List (A × List Tok)
  parse′ (symbolBind _) [] = []
  parse′ (symbolBind f) (c ∷ s) = parse′ (f c) s
  parse′ (returnPlus x p) s = (x , s) ∷ parse′ p s
  parse′ fail′ xs = []

record P (A : Set) : Set₁ where
  constructor mkP
  field
    unP : ∀ {B} → (A → P′ B) → P′ B

open P

symbol : P Tok
symbol = mkP symbolBind

fail : ∀ {A} → P A
fail = mkP λ _ → fail′

infixr 2 _+++_
_+++_ : ∀ {A} → P A → P A → P A
p +++ q = mkP λ k → unP p k +++′ unP q k

private
  ret : ∀ {A} → A → P A
  ret x = mkP λ k → k x

  bind : ∀ {A B} → P A → (A → P B) → P B
  bind p f = mkP λ k → unP p (λ x → unP (f x) k)

parse : ∀ {A} → P A → List Tok → List (A × List Tok)
parse p = parse′ (unP p (λ x → returnPlus x fail′))

parse! : ∀ {A} → P A → List Tok → Maybe A
parse! p s with filter (null ∘ snd) (parse p s)
... | []          = nothing
... | (x , _) ∷ _ = just x

--- Instances ---

instance
  FunctorP : Functor P
  fmap {{FunctorP}} f m = bind m λ x → ret (f x)

  ApplicativeP : Applicative P
  pure {{ApplicativeP}} = ret
  _<*>_ {{ApplicativeP}} = monadAp bind

  MonadP : Monad P
  _>>=_  {{MonadP}} = bind

  MonoidP : ∀ {A} → Monoid (P A)
  mempty {{MonoidP}} = fail
  _<>_   {{MonoidP}} = _+++_

--- Derived combinators ---

sat : (p : Tok → Bool) → P (Σ Tok (IsTrue ∘ p))
sat p = symbol >>= match
  where
    -- Inlining 'match' gives internal error!
    match : Tok → P (Σ Tok (IsTrue ∘ p))
    match t = if′ p t then return (t , it) else fail

sat! : (Tok → Bool) → P Tok
sat! p = fst <$> sat p

token : {{EqTok : Eq Tok}} → Tok → P ⊤
token t = _ <$ sat (isYes ∘ _==_ t)

{-# NON_TERMINATING #-}
many many₁ : ∀ {A} → P A → P (List A)
many p = return [] +++ many₁ p
many₁ p = _∷_ <$> p <*> many p

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module json where

open import general-util

data json : Set where
  json-null : json
  json-raw : rope → json
  json-string : string → json
  json-nat : nat → json
  json-array : 𝕃 json → json
  json-object : 𝕃 (string × json) → json

json-escape-string : string → string
json-escape-string str = 𝕃char-to-string $ rec $ string-to-𝕃char str where
  rec : 𝕃 char → 𝕃 char
  rec [] = []
  rec ('\b' :: chars) = '\\' :: 'b' :: rec chars
  rec ('\f' :: chars) = '\\' :: 'f' :: rec chars
  rec ('\n' :: chars) = '\\' :: 'n' :: rec chars
  rec ('\r' :: chars) = '\\' :: 'r' :: rec chars
  rec ('\t' :: chars) = '\\' :: 't' :: rec chars
  rec ('"'  :: chars) = '\\' :: '"' :: rec chars
  rec ('\\' :: chars) = '\\' :: '\\' :: rec chars
  rec (char :: chars) = char :: rec chars

{-# TERMINATING #-}
json-to-rope : json → rope
json-to-rope json-null = [[ "null" ]]
json-to-rope (json-raw rope) = rope
json-to-rope (json-string string) = [[ "\"" ]] ⊹⊹ [[ json-escape-string string ]] ⊹⊹ [[ "\"" ]]
json-to-rope (json-nat nat) = [[ ℕ-to-string nat ]]
json-to-rope (json-array array) = [[ "[" ]] ⊹⊹ 𝕃-to-rope json-to-rope "," array ⊹⊹ [[ "]" ]]
json-to-rope (json-object t) = [[ "{" ]] ⊹⊹ 𝕃-to-rope (uncurry λ k v → [[ "\"" ]] ⊹⊹ [[ json-escape-string k ]] ⊹⊹ [[ "\":" ]] ⊹⊹ json-to-rope v)  "," t ⊹⊹ [[ "}" ]]

json-rope : rope → json
json-rope rope = json-raw ([[ "\"" ]] ⊹⊹ rope ⊹⊹ [[ "\"" ]])

json-raw-string : string → json
json-raw-string str = json-raw [[ str ]]

putJson : json → IO ⊤
putJson = putRopeLn ∘ json-to-rope

max_stars_repo_name: mudathirmahgoub/cedille

max_issues_repo_name: mudathirmahgoub/cedille

max_forks_repo_name: mudathirmahgoub/cedille


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

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

module Dijkstra.EitherD.Syntax where

open import Dijkstra.EitherD
open import Dijkstra.EitherLike
open import Dijkstra.Syntax
open import Haskell.Prelude

private
  variable
    E     : Set
    A B C : Set

-- From this instance declaration, we get _<$>_, pure, and _<*>_ also.
instance
  Monad-EitherD : ∀ {E : Set} → Monad (EitherD E)
  Monad.return Monad-EitherD = EitherD-return
  Monad._>>=_  Monad-EitherD = EitherD-bind

-- These instance declarations give us variant conditional operations that we
-- can define to play nice with `EitherD-weakestPre`

instance
  EitherD-MonadIfD : MonadIfD{ℓ₃ = ℓ0} (EitherD E)
  MonadIfD.monad EitherD-MonadIfD = Monad-EitherD
  MonadIfD.ifD‖  EitherD-MonadIfD = EitherD-if

  EitherD-MonadMaybeD : MonadMaybeD (EitherD E)
  MonadMaybeD.monad  EitherD-MonadMaybeD = Monad-EitherD
  MonadMaybeD.maybeD EitherD-MonadMaybeD = EitherD-maybe

  EitherD-MonadEitherD : MonadEitherD (EitherD E)
  MonadEitherD.monad    EitherD-MonadEitherD = Monad-EitherD
  MonadEitherD.eitherD  EitherD-MonadEitherD = EitherD-either

-- `EitherD` is Either-like
instance
  EitherD-EitherLike : EitherLike EitherD
  EitherLike.fromEither EitherD-EitherLike (Left  a) = EitherD-bail a
  EitherLike.fromEither EitherD-EitherLike (Right b) = EitherD-return b

  EitherLike.toEither   EitherD-EitherLike = EitherD-run


text:
_ : @ω Set → Set₁
_ = λ (@0 _) → Set

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
------------------------------------------------------------------------
-- The Eilenberg-MacLane space K(G, 1)
------------------------------------------------------------------------

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

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

import Equality.Path as P

module Eilenberg-MacLane-space
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

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

open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)

open import Bijection equality-with-J as B using (_↔_)
open import Embedding equality-with-J using (Embedding; Is-embedding)
import Equality.Groupoid equality-with-J as EG
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
import Equivalence P.equality-with-J as PEq
open import Function-universe equality-with-J hiding (id; _∘_)
open import Group equality-with-J
open import H-level equality-with-J as H-level
import H-level P.equality-with-J as PH
open import H-level.Closure equality-with-J
open import H-level.Truncation eq as T using (∥_∥[1+_]; ∣_∣)
open import H-level.Truncation.Propositional eq as TP using (Surjective)
open import Pointed-type equality-with-J
open import Pointed-type.Connected eq
open import Pointed-type.Homotopy-group eq
open import Univalence-axiom equality-with-J

private
  variable
    a p     : Level
    A       : Type a
    P       : A → Type p
    e g x y : A
    G G₁ G₂ : Group g

------------------------------------------------------------------------
-- The type

-- The Eilenberg-MacLane space K(G, 1).
--
-- This definition is taken from "Eilenberg-MacLane Spaces in Homotopy
-- Type Theory" by Licata and Finster.

data K[_]1 (G : Group g) : Type g where
  base        : K[ G ]1
  loopᴾ        : Group.Carrier G → base P.≡ base
  loop-idᴾ     : loopᴾ (Group.id G) P.≡ P.refl
  loop-∘ᴾ      : loopᴾ (Group._∘_ G x y) P.≡ P.trans (loopᴾ x) (loopᴾ y)
  is-groupoidᴾ : PH.H-level 3 K[ G ]1

-- Variants of the higher constructors.

loop : Group.Carrier G → base ≡ base
loop {G = G} = _↔_.from ≡↔≡ ⊚ loopᴾ {G = G}

loop-id : loop {G = G} (Group.id G) ≡ refl base
loop-id {G = G} =
  loop id              ≡⟨ _≃_.from (Eq.≃-≡ (Eq.↔⇒≃ (inverse ≡↔≡))) (_↔_.from ≡↔≡ loop-idᴾ) ⟩
  _↔_.from ≡↔≡ P.refl  ≡⟨ from-≡↔≡-refl ⟩∎
  refl base            ∎
  where
  open Group G

loop-∘ : loop {G = G} (Group._∘_ G x y) ≡ trans (loop x) (loop y)
loop-∘ {G = G} {x = x} {y = y} =
  loop (Group._∘_ G x y)                      ≡⟨ _≃_.from (Eq.≃-≡ (Eq.↔⇒≃ (inverse ≡↔≡))) (_↔_.from ≡↔≡ loop-∘ᴾ) ⟩
  _↔_.from ≡↔≡ (P.trans (loopᴾ x) (loopᴾ y))  ≡⟨ sym trans≡trans ⟩∎
  trans (loop x) (loop y)                     ∎

is-groupoid : H-level 3 K[ G ]1
is-groupoid = _↔_.from (H-level↔H-level 3) is-groupoidᴾ

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

-- A dependent eliminator, expressed using paths.
--
-- This eliminator is based on one from "Eilenberg-MacLane Spaces in
-- Homotopy Type Theory" by Licata and Finster.

record Elimᴾ {G : Group g} (P : K[ G ]1 → Type p) : Type (g ⊔ p) where
  no-eta-equality
  open Group G
  field
    baseʳ        : P base
    loopʳ        : ∀ g → P.[ (λ i → P (loopᴾ g i)) ] baseʳ ≡ baseʳ
    loop-idʳ     : P.[ (λ i → P.[ (λ j → P (loop-idᴾ i j)) ]
                                baseʳ ≡ baseʳ) ]
                     loopʳ id ≡ P.refl {x = baseʳ}
    loop-∘ʳ      : P.[ (λ i →
                          P.[ (λ j → P (loop-∘ᴾ {x = x} {y = y} i j)) ]
                            baseʳ ≡ baseʳ) ]
                     loopʳ (x ∘ y) ≡ P.htrans P (loopʳ x) (loopʳ y)
    is-groupoidʳ : ∀ x → PH.H-level 3 (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : K[ G ]1) → P x
elimᴾ {G = G} {P = P} e = helper
  where
  module E = Elimᴾ e

  helper : (x : K[ G ]1) → P x
  helper base                     = E.baseʳ
  helper (loopᴾ x i)              = E.loopʳ x i
  helper (loop-idᴾ i j)           = E.loop-idʳ i j
  helper (loop-∘ᴾ i j)            = E.loop-∘ʳ i j
  helper (is-groupoidᴾ p q i j k) =
    P.heterogeneous-UIP₃ E.is-groupoidʳ (is-groupoidᴾ p q)
      (λ j k → helper (p j k)) (λ j k → helper (q j k)) i j k

-- A non-dependent eliminator, expressed using paths.
--
-- This eliminator is based on one from "Eilenberg-MacLane Spaces in
-- Homotopy Type Theory" by Licata and Finster.

record Recᴾ (G : Group g) (A : Type a) : Type (g ⊔ a) where
  no-eta-equality
  open Group G
  field
    baseʳ        : A
    loopʳ        : Carrier → baseʳ P.≡ baseʳ
    loop-idʳ     : loopʳ id P.≡ P.refl
    loop-∘ʳ      : loopʳ (x ∘ y) P.≡ P.trans (loopʳ x) (loopʳ y)
    is-groupoidʳ : PH.H-level 3 A

open Recᴾ public

recᴾ : Recᴾ G A → K[ G ]1 → A
recᴾ {G = G} {A = A} r = elimᴾ λ where
    .is-groupoidʳ _          → R.is-groupoidʳ
    .baseʳ                   → R.baseʳ
    .loopʳ                   → R.loopʳ
    .loop-idʳ                → R.loop-idʳ
    .loop-∘ʳ {x = x} {y = y} →
      R.loopʳ (x ∘ y)                                             P.≡⟨ R.loop-∘ʳ ⟩

      P.trans (R.loopʳ x) (R.loopʳ y)                             P.≡⟨ P.sym $ P.htrans-const (loopᴾ {G = G} x) (loopᴾ y) (R.loopʳ x) ⟩∎

      P.htrans {x≡y = loopᴾ {G = G} x} {y≡z = loopᴾ y} (const A)
        (R.loopʳ x) (R.loopʳ y)                                   ∎
  where
  open Group G
  module R = Recᴾ r

-- A non-dependent eliminator.
--
-- This eliminator is based on one from "Eilenberg-MacLane Spaces in
-- Homotopy Type Theory" by Licata and Finster.

record Rec (G : Group g) (A : Type a) : Type (g ⊔ a) where
  no-eta-equality
  open Group G
  field
    baseʳ        : A
    loopʳ        : Carrier → baseʳ ≡ baseʳ
    loop-idʳ     : loopʳ id ≡ refl baseʳ
    loop-∘ʳ      : loopʳ (x ∘ y) ≡ trans (loopʳ x) (loopʳ y)
    is-groupoidʳ : H-level 3 A

open Rec public

rec : Rec G A → K[ G ]1 → A
rec {G = G} {A = A} r = recᴾ λ where
    .is-groupoidʳ            → _↔_.to (H-level↔H-level 3) R.is-groupoidʳ
    .baseʳ                   → R.baseʳ
    .loopʳ                   → _↔_.to ≡↔≡ ⊚ R.loopʳ
    .loop-idʳ                →
      _↔_.to ≡↔≡ (R.loopʳ id)    P.≡⟨ P.cong (_↔_.to ≡↔≡) $ _↔_.to ≡↔≡ R.loop-idʳ ⟩
      _↔_.to ≡↔≡ (refl R.baseʳ)  P.≡⟨ _↔_.to ≡↔≡ to-≡↔≡-refl ⟩∎
      P.refl                     ∎
    .loop-∘ʳ {x = x} {y = y} →
      _↔_.to ≡↔≡ (R.loopʳ (x ∘ y))                                 P.≡⟨ P.cong (_↔_.to ≡↔≡) $ _↔_.to ≡↔≡ R.loop-∘ʳ ⟩

      _↔_.to ≡↔≡ (trans (R.loopʳ x) (R.loopʳ y))                   P.≡⟨ _↔_.to ≡↔≡ $ sym $ cong₂ (λ p q → _↔_.to ≡↔≡ (trans p q))
                                                                          (_↔_.left-inverse-of ≡↔≡ _)
                                                                          (_↔_.left-inverse-of ≡↔≡ _) ⟩
      _↔_.to ≡↔≡ (trans (_↔_.from ≡↔≡ (_↔_.to ≡↔≡ (R.loopʳ x)))
                        (_↔_.from ≡↔≡ (_↔_.to ≡↔≡ (R.loopʳ y))))   P.≡⟨ P.cong (_↔_.to ≡↔≡) $ _↔_.to ≡↔≡ trans≡trans ⟩

      (_↔_.to ≡↔≡ $ _↔_.from ≡↔≡ $
       P.trans (_↔_.to ≡↔≡ (R.loopʳ x)) (_↔_.to ≡↔≡ (R.loopʳ y)))  P.≡⟨ _↔_.to ≡↔≡ $ _↔_.right-inverse-of ≡↔≡ _ ⟩∎

      P.trans (_↔_.to ≡↔≡ (R.loopʳ x)) (_↔_.to ≡↔≡ (R.loopʳ y))    ∎
  where
  open Group G
  module R = Rec r

-- A "computation" rule.

rec-loop : cong (rec e) (loop g) ≡ e .loopʳ g
rec-loop = cong-≡↔≡ (refl _)

-- A dependent eliminator that can be used when eliminating into sets,
-- expressed using paths.

record Elim-setᴾ {G : Group g}
                 (P : K[ G ]1 → Type p) : Type (g ⊔ p) where
  no-eta-equality
  open Group G
  field
    baseʳ   : P base
    loopʳ   : ∀ g → P.[ (λ i → P (loopᴾ g i)) ] baseʳ ≡ baseʳ
    is-setʳ : ∀ x → P.Is-set (P x)

open Elim-setᴾ public

elim-setᴾ : Elim-setᴾ P → (x : K[ G ]1) → P x
elim-setᴾ e = elimᴾ λ where
    .baseʳ        → E.baseʳ
    .loopʳ        → E.loopʳ
    .loop-idʳ     → P.heterogeneous-UIP E.is-setʳ _ _ _
    .loop-∘ʳ      → P.heterogeneous-UIP E.is-setʳ _ _ _
    .is-groupoidʳ → PH.mono₁ 2 ⊚ E.is-setʳ
  where
  module E = Elim-setᴾ e

-- A dependent eliminator that can be used when eliminating into sets.

record Elim-set {G : Group g}
                (P : K[ G ]1 → Type p) : Type (g ⊔ p) where
  no-eta-equality
  open Group G
  field
    baseʳ   : P base
    loopʳ   : ∀ g → subst P (loop g) baseʳ ≡ baseʳ
    is-setʳ : ∀ x → Is-set (P x)

open Elim-set public

elim-set : Elim-set P → (x : K[ G ]1) → P x
elim-set e = elim-setᴾ λ where
    .baseʳ   → E.baseʳ
    .loopʳ   → subst≡→[]≡ ⊚ E.loopʳ
    .is-setʳ → _↔_.to (H-level↔H-level 2) ⊚ E.is-setʳ
  where
  module E = Elim-set e

-- A "computation" rule.

elim-set-loop : dcong (elim-set e) (loop g) ≡ e .loopʳ g
elim-set-loop = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator that can be used when eliminating into
-- sets, expressed using paths.

record Rec-setᴾ (G : Group g) (A : Type a) : Type (g ⊔ a) where
  no-eta-equality
  open Group G
  field
    baseʳ   : A
    loopʳ   : Carrier → baseʳ P.≡ baseʳ
    is-setʳ : P.Is-set A

open Rec-setᴾ public

rec-setᴾ : Rec-setᴾ G A → K[ G ]1 → A
rec-setᴾ r = elim-setᴾ λ where
    .baseʳ     → R.baseʳ
    .loopʳ     → R.loopʳ
    .is-setʳ _ → R.is-setʳ
  where
  module R = Rec-setᴾ r

-- A non-dependent eliminator that can be used when eliminating into
-- sets.

record Rec-set (G : Group g) (A : Type a) : Type (g ⊔ a) where
  no-eta-equality
  open Group G
  field
    baseʳ   : A
    loopʳ   : Carrier → baseʳ ≡ baseʳ
    is-setʳ : Is-set A

open Rec-set public

rec-set : Rec-set G A → K[ G ]1 → A
rec-set r = rec-setᴾ λ where
    .baseʳ   → R.baseʳ
    .loopʳ   → _↔_.to ≡↔≡ ⊚ R.loopʳ
    .is-setʳ → _↔_.to (H-level↔H-level 2) R.is-setʳ
  where
  module R = Rec-set r

-- A "computation" rule.

rec-set-loop : cong (rec-set e) (loop g) ≡ e .loopʳ g
rec-set-loop = cong-≡↔≡ (refl _)

-- A dependent eliminator that can be used when eliminating into
-- propositions.

record Elim-prop {G : Group g} (P : K[ G ]1 → Type p) :
                 Type (g ⊔ p) where
  no-eta-equality
  field
    baseʳ           : P base
    is-propositionʳ : ∀ x → Is-proposition (P x)

open Elim-prop public

elim-prop : Elim-prop P → (x : K[ G ]1) → P x
elim-prop e = elim-set λ where
    .baseʳ   → E.baseʳ
    .loopʳ _ → E.is-propositionʳ _ _ _
    .is-setʳ → mono₁ 1 ⊚ E.is-propositionʳ
  where
  module E = Elim-prop e

------------------------------------------------------------------------
-- Universal properties

-- A dependent universal property, restricted to families of sets.
--
-- This property is expressed using P.[_]_≡_.

universal-property-Π-setᴾ :
  (∀ x → P.Is-set (P x)) →
  ((x : K[ G ]1) → P x) ≃
  (∃ λ (x : P base) → ∀ g → P.[ (λ i → P (loopᴾ g i)) ] x ≡ x)
universal-property-Π-setᴾ {G = G} {P = P} P-set =
  _↔_.from ≃↔≃ $
  PEq.↔→≃
    (λ f → f base , P.hcong f ⊚ loopᴾ)
    (λ (x , f) → elim-setᴾ λ where
       .baseʳ   → x
       .loopʳ   → f
       .is-setʳ → P-set)
    (λ _ → P.refl)
    (λ f → P.⟨ext⟩ $ elim-setᴾ λ where
       .baseʳ     → P.refl
       .loopʳ _ _ → P.refl
       .is-setʳ _ → PH.mono₁ 2 (P-set _))

-- A variant of the dependent universal property, restricted to
-- families of sets.
--
-- This property is expressed using subst.

universal-property-Π-set :
  (∀ x → Is-set (P x)) →
  ((x : K[ G ]1) → P x) ≃
  (∃ λ (x : P base) → ∀ g → subst P (loop g) x ≡ x)
universal-property-Π-set {G = G} {P = P} P-set =
  ((x : K[ G ]1) → P x)                                         ↝⟨ universal-property-Π-setᴾ (_↔_.to (H-level↔H-level 2) ⊚ P-set) ⟩
  (∃ λ (x : P base) → ∀ g → P.[ (λ i → P (loopᴾ g i)) ] x ≡ x)  ↔⟨ (∃-cong λ _ → ∀-cong ext λ _ → inverse subst≡↔[]≡) ⟩□
  (∃ λ (x : P base) → ∀ g → subst P (loop g) x ≡ x)             □

-- A non-dependent universal property, restricted to sets.

universal-property-set :
  Is-set A →
  (K[ G ]1 → A) ≃ (∃ λ (x : A) → Group.Carrier G → x ≡ x)
universal-property-set {A = A} {G = G} A-set =
  (K[ G ]1 → A)                      ↝⟨ universal-property-Π-setᴾ (λ _ → _↔_.to (H-level↔H-level 2) A-set) ⟩
  (∃ λ (x : A) → Carrier → x P.≡ x)  ↔⟨ (∃-cong λ _ → ∀-cong ext λ _ → inverse ≡↔≡) ⟩□
  (∃ λ (x : A) → Carrier → x ≡ x)    □
  where
  open Group G

------------------------------------------------------------------------
-- Some conversion functions

-- A map function.
--
-- The existence of such a function was suggested to me by Christian
-- Sattler.

map : G₁ →ᴳ G₂ → K[ G₁ ]1 → K[ G₂ ]1
map {G₁ = G₁} {G₂ = G₂} h = rec λ where
    .is-groupoidʳ → is-groupoid
    .baseʳ        → base
    .loopʳ x      → loop (to x)
    .loop-idʳ     →
      loop (to G₁.id)  ≡⟨ cong loop (→ᴳ-id h) ⟩
      loop G₂.id       ≡⟨ loop-id ⟩∎
      refl _           ∎
    .loop-∘ʳ {x = x} {y = y} →
      loop (to (x G₁.∘ y))               ≡⟨ cong loop (h .homomorphic x y) ⟩
      loop (to x G₂.∘ to y)              ≡⟨ loop-∘ ⟩∎
      trans (loop (to x)) (loop (to y))  ∎
  where
  module G₁ = Group G₁
  module G₂ = Group G₂
  open Homomorphic h using (to)

-- If G₁ and G₂ are isomorphic groups, then K[ G₁ ]1 and K[ G₂ ]1 are
-- equivalent.

cong-≃ : G₁ ≃ᴳ G₂ → K[ G₁ ]1 ≃ K[ G₂ ]1
cong-≃ G₁≃G₂ = Eq.↔→≃
  (map (↝ᴳ→→ᴳ G₁≃G₂))
  (map (↝ᴳ→→ᴳ (≃ᴳ-sym G₁≃G₂)))
  (lemma (↝ᴳ→→ᴳ G₁≃G₂) (↝ᴳ→→ᴳ (≃ᴳ-sym G₁≃G₂))
     (_≃_.right-inverse-of (related G₁≃G₂)))
  (lemma (↝ᴳ→→ᴳ (≃ᴳ-sym G₁≃G₂)) (↝ᴳ→→ᴳ G₁≃G₂)
     (_≃_.left-inverse-of (related G₁≃G₂)))
  where
  open Homomorphic using (to)

  lemma :
    (f₁ : G₁ →ᴳ G₂) (f₂ : G₂ →ᴳ G₁) →
    (∀ x → to f₁ (to f₂ x) ≡ x) →
    ∀ x → map f₁ (map f₂ x) ≡ x
  lemma f₁ f₂ hyp = elim-set λ where
    .is-setʳ _ → is-groupoid
    .baseʳ     → refl _
    .loopʳ g   →
      subst (λ x → map f₁ (map f₂ x) ≡ x) (loop g) (refl _)          ≡⟨ subst-in-terms-of-trans-and-cong ⟩

      trans (sym $ cong (map f₁ ⊚ map f₂) (loop g))
        (trans (refl _) (cong P.id (loop g)))                        ≡⟨ cong₂ (trans ⊚ sym)
                                                                          (sym $ cong-∘ _ _ _)
                                                                          (trans (trans-reflˡ _) $
                                                                           sym $ cong-id _) ⟩

      trans (sym $ cong (map f₁) $ cong (map f₂) (loop g)) (loop g)  ≡⟨ cong (flip trans (loop g) ⊚ sym) $
                                                                        trans (cong (cong _) rec-loop)
                                                                        rec-loop ⟩

      trans (sym $ loop (to f₁ (to f₂ g))) (loop g)                  ≡⟨ cong (flip trans _ ⊚ sym ⊚ loop) $ hyp _ ⟩

      trans (sym $ loop g) (loop g)                                  ≡⟨ trans-symˡ _ ⟩∎

      refl _                                                         ∎

------------------------------------------------------------------------
-- A lemma

-- The pointed type (K[ G ]1 , base) is connected.
--
-- This result was pointed out to me by Christian Sattler.

connected : Connected (K[ G ]1 , base)
connected = elim-prop λ where
  .is-propositionʳ _ → TP.truncation-is-proposition
  .baseʳ             → TP.∣ refl _ ∣

------------------------------------------------------------------------
-- Some lemmas related to the fundamental group of (K[ G ]1 , base)

-- A variant of the fundamental group of (K[ G ]1 , base) is
-- isomorphic to G (assuming univalence).
--
-- The proof is based on the one given in "Eilenberg-MacLane Spaces in
-- Homotopy Type Theory" by Licata and Finster.

Fundamental-group′[K1]≃ᴳ :
  {G : Group g} →
  Univalence g →
  (s : Is-set (proj₁ (Ω (K[ G ]1 , base)))) →
  Fundamental-group′ (K[ G ]1 , base) s ≃ᴳ G
Fundamental-group′[K1]≃ᴳ {g = g} {G = G} univ _ = λ where
    .related     → equiv
    .homomorphic → hom
  where
  module FG = Group (Fundamental-group′ (K[ G ]1 , base) is-groupoid)
  open Group G

  -- Postcomposition is an equivalence.

  to-≃ : Carrier → Carrier ≃ Carrier
  to-≃ x = Eq.↔→≃
    (_∘ x)
    (_∘ x ⁻¹)
    (λ y →
       (y ∘ x ⁻¹) ∘ x  ≡⟨ sym $ assoc _ _ _ ⟩
       y ∘ (x ⁻¹ ∘ x)  ≡⟨ cong (y ∘_) $ left-inverse _ ⟩
       y ∘ id          ≡⟨ right-identity _ ⟩∎
       y               ∎)
    (λ y →
       (y ∘ x) ∘ x ⁻¹  ≡⟨ sym $ assoc _ _ _ ⟩
       y ∘ (x ∘ x ⁻¹)  ≡⟨ cong (y ∘_) $ right-inverse _ ⟩
       y ∘ id          ≡⟨ right-identity _ ⟩∎
       y               ∎)

  -- A family of codes.

  Code : K[ G ]1 → Set g
  Code = rec λ where
    .is-groupoidʳ → ∃-H-level-H-level-1+ ext univ 2
    .baseʳ        → Carrier , Carrier-is-set
    .loopʳ x      → Σ-≡,≡→≡ (≃⇒≡ univ (to-≃ x))
                      (H-level-propositional ext 2 _ _)
    .loop-idʳ     →
      Σ-≡,≡→≡ (≃⇒≡ univ (to-≃ id)) _     ≡⟨ _≃_.from (Eq.≃-≡ $ Eq.↔⇒≃ B.Σ-≡,≡↔≡) $
                                            Σ-≡,≡→≡
                                              (
          ≃⇒≡ univ (to-≃ id)                   ≡⟨ cong (≃⇒≡ univ) $ Eq.lift-equality ext $ ⟨ext⟩
                                                  right-identity ⟩
          ≃⇒≡ univ Eq.id                       ≡⟨ ≃⇒≡-id univ ⟩∎
          refl _                               ∎)
                                              (H-level.⇒≡ 1 (H-level-propositional ext 2) _ _) ⟩

      Σ-≡,≡→≡ (refl _) (subst-refl _ _)  ≡⟨ Σ-≡,≡→≡-refl-subst-refl ⟩∎

      refl _                             ∎
    .loop-∘ʳ {x = x} {y = y} →
      Σ-≡,≡→≡ (≃⇒≡ univ (to-≃ (x ∘ y))) _                        ≡⟨ _≃_.from (Eq.≃-≡ $ Eq.↔⇒≃ B.Σ-≡,≡↔≡) $
                                                                    Σ-≡,≡→≡
                                                                      (
          ≃⇒≡ univ (to-≃ (x ∘ y))                                      ≡⟨ (cong (≃⇒≡ univ) $ Eq.lift-equality ext $ ⟨ext⟩ λ _ →
                                                                           assoc _ _ _) ⟩
          ≃⇒≡ univ (to-≃ y Eq.∘ to-≃ x)                                ≡⟨ ≃⇒≡-∘ univ ext _ _ ⟩∎
          trans (≃⇒≡ univ (to-≃ x)) (≃⇒≡ univ (to-≃ y))                ∎)
                                                                      (H-level.⇒≡ 1 (H-level-propositional ext 2) _ _) ⟩

      Σ-≡,≡→≡ (trans (≃⇒≡ univ (to-≃ x)) (≃⇒≡ univ (to-≃ y))) _  ≡⟨ sym $ trans-Σ-≡,≡→≡ _ _ _ _ ⟩∎

      trans (Σ-≡,≡→≡ (≃⇒≡ univ (to-≃ x)) _)
        (Σ-≡,≡→≡ (≃⇒≡ univ (to-≃ y)) _)                          ∎

  -- Some "computation" rules.

  ≡⇒≃-cong-Code-loop :
    ≡⇒≃ (cong (proj₁ ⊚ Code) (loop x)) ≡ to-≃ x
  ≡⇒≃-cong-Code-loop {x = x} =
    ≡⇒≃ (cong (proj₁ ⊚ Code) (loop x))         ≡⟨ cong ≡⇒≃ $ sym $ cong-∘ proj₁ Code (loop x) ⟩

    ≡⇒≃ (cong proj₁ (cong Code (loop x)))      ≡⟨ cong (≡⇒≃ ⊚ cong proj₁) rec-loop ⟩

    ≡⇒≃ (cong proj₁ $
         Σ-≡,≡→≡ (≃⇒≡ univ (to-≃ x))
           (H-level-propositional ext 2 _ _))  ≡⟨ cong ≡⇒≃ $ proj₁-Σ-≡,≡→≡ _ _ ⟩

    ≡⇒≃ (≃⇒≡ univ (to-≃ x))                    ≡⟨ _≃_.right-inverse-of (≡≃≃ univ) _ ⟩∎

    to-≃ x                                     ∎

  subst-Code-loop :
    subst (proj₁ ⊚ Code) (loop x) ≡ _∘ x
  subst-Code-loop {x = x} = ⟨ext⟩ λ y →
    subst (proj₁ ⊚ Code) (loop x) y                ≡⟨ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
    _≃_.to (≡⇒≃ (cong (proj₁ ⊚ Code) (loop x))) y  ≡⟨ cong (λ eq → _≃_.to eq y) ≡⇒≃-cong-Code-loop ⟩∎
    _≃_.to (to-≃ x) y                              ∎

  subst-Code-sym-loop :
    subst (proj₁ ⊚ Code) (sym (loop x)) ≡ _∘ x ⁻¹
  subst-Code-sym-loop {x = x} = ⟨ext⟩ λ y →
    subst (proj₁ ⊚ Code) (sym (loop x)) y            ≡⟨ subst-in-terms-of-inverse∘≡⇒↝ equivalence _ _ _ ⟩
    _≃_.from (≡⇒≃ (cong (proj₁ ⊚ Code) (loop x))) y  ≡⟨ cong (λ eq → _≃_.from eq y) ≡⇒≃-cong-Code-loop ⟩∎
    _≃_.from (to-≃ x) y                              ∎

  -- An equivalence.

  to : base ≡ x → proj₁ (Code x)
  to eq = subst (proj₁ ⊚ Code) eq id

  from : ∀ x → proj₁ (Code x) → base ≡ x
  from = elim-set λ where
    .is-setʳ _ → Π-closure ext 2 λ _ →
                 is-groupoid
    .baseʳ     → loop
    .loopʳ x   → ⟨ext⟩ λ y →
      subst (λ x → proj₁ (Code x) → base ≡ x) (loop x) loop y        ≡⟨ subst-→ ⟩

      subst (base ≡_) (loop x)
        (loop (subst (proj₁ ⊚ Code) (sym (loop x)) y))               ≡⟨ sym trans-subst ⟩

      trans (loop (subst (proj₁ ⊚ Code) (sym (loop x)) y)) (loop x)  ≡⟨ cong (flip trans (loop x) ⊚ loop ⊚ (_$ y))
                                                                        subst-Code-sym-loop ⟩

      trans (loop (y ∘ x ⁻¹)) (loop x)                               ≡⟨ cong (flip trans _) loop-∘ ⟩

      trans (trans (loop y) (loop (x ⁻¹))) (loop x)                  ≡⟨ trans-assoc _ _ _ ⟩

      trans (loop y) (trans (loop (x ⁻¹)) (loop x))                  ≡⟨ cong (trans _) $ sym loop-∘ ⟩

      trans (loop y) (loop (x ⁻¹ ∘ x))                               ≡⟨ cong (trans (loop y) ⊚ loop) $ left-inverse _ ⟩

      trans (loop y) (loop id)                                       ≡⟨ cong (trans _) loop-id ⟩

      trans (loop y) (refl base)                                     ≡⟨ trans-reflʳ _ ⟩∎

      loop y                                                         ∎

  to-loop : ∀ x → to (loop x) ≡ x
  to-loop x =
    subst (proj₁ ⊚ Code) (loop x) id  ≡⟨ cong (_$ id) subst-Code-loop ⟩
    id ∘ x                            ≡⟨ left-identity _ ⟩∎
    x                                 ∎

  from-to : ∀ eq → from x (to eq) ≡ eq
  from-to = elim¹ (λ {x} eq → from x (to eq) ≡ eq)
    (loop (subst (proj₁ ⊚ Code) (refl base) id)  ≡⟨ cong loop $ subst-refl _ _ ⟩
     loop id                                     ≡⟨ loop-id ⟩∎
     refl base                                   ∎)

  equiv : proj₁ (Ω (K[ G ]1 , base)) ≃ Carrier
  equiv =
    base ≡ base  ↝⟨ Eq.↔→≃ to loop to-loop from-to ⟩□
    Carrier      □

  -- The equivalence is homomorphic.

  hom′ :
    ∀ x y →
    _≃_.from equiv (x ∘ y) ≡
    _≃_.from equiv x FG.∘ _≃_.from equiv y
  hom′ x y =
    loop (x ∘ y)             ≡⟨ loop-∘ ⟩∎
    trans (loop x) (loop y)  ∎

  hom :
    ∀ p q →
    _≃_.to equiv (p FG.∘ q) ≡
    _≃_.to equiv p ∘ _≃_.to equiv q
  hom p q = _≃_.from-to equiv
    (_≃_.from equiv (_≃_.to equiv p ∘ _≃_.to equiv q)  ≡⟨ hom′ _ _ ⟩

     _≃_.from equiv (_≃_.to equiv p) FG.∘
     _≃_.from equiv (_≃_.to equiv q)                   ≡⟨ cong₂ FG._∘_
                                                            (_≃_.left-inverse-of equiv p)
                                                            (_≃_.left-inverse-of equiv q) ⟩∎
     p FG.∘ q                                          ∎)

-- The right-to-left direction of Fundamental-group′[K1]≃ᴳ is loop.

_ :
  {G : Group g} {univ : Univalence g} {s : Is-set _} →
  _≃_.from (Fundamental-group′[K1]≃ᴳ {G = G} univ s .related) ≡
  loop
_ = refl _

-- The fundamental group of (K[ G ]1 , base) is isomorphic to G
-- (assuming univalence).
--
-- The proof is based on the one given in "Eilenberg-MacLane Spaces in
-- Homotopy Type Theory" by Licata and Finster.

Fundamental-group[K1]≃ᴳ :
  {G : Group g} →
  Univalence g →
  Fundamental-group (K[ G ]1 , base) ≃ᴳ G
Fundamental-group[K1]≃ᴳ univ =
  ↝ᴳ-trans (≃ᴳ-sym Homotopy-group-[1+]′≃ᴳHomotopy-group-[1+])
    (Fundamental-group′[K1]≃ᴳ univ is-groupoid)

-- If G is abelian, then the fundamental group of (K[ G ]1 , base) is
-- abelian.

Abelian→Abelian-Fundamental-group′ :
  Abelian G → Abelian (Fundamental-group′ (K[ G ]1 , base) is-groupoid)
Abelian→Abelian-Fundamental-group′ {G = G} abelian =
  flip $ EG.Transitivity-commutative.commutative base _∙_ ∙-base base-∙
  where
  open Group G

  lemma : Carrier → (x : K[ G ]1) → x ≡ x
  lemma g₁ = elim-set λ where
    .is-setʳ  → λ _ → is-groupoid
    .baseʳ    → loop g₁
    .loopʳ g₂ → ≡⇒↝ _ (sym [subst≡]≡[trans≡trans])
      (trans (loop g₁) (loop g₂)  ≡⟨ sym loop-∘ ⟩
       loop (g₁ ∘ g₂)             ≡⟨ cong loop (abelian g₁ g₂) ⟩
       loop (g₂ ∘ g₁)             ≡⟨ loop-∘ ⟩∎
       trans (loop g₂) (loop g₁)  ∎)

  lemma-id : ∀ x → lemma id x ≡ refl x
  lemma-id = elim-prop λ where
    .is-propositionʳ _ → is-groupoid
    .baseʳ →
      loop id    ≡⟨ loop-id ⟩∎
      refl base  ∎

  lemma-∘ :
    ∀ g₁ g₂ x → lemma (g₁ ∘ g₂) x ≡ trans (lemma g₁ x) (lemma g₂ x)
  lemma-∘ g₁ g₂ = elim-prop λ where
    .is-propositionʳ _ → is-groupoid
    .baseʳ →
      loop (g₁ ∘ g₂)             ≡⟨ loop-∘ ⟩∎
      trans (loop g₁) (loop g₂)  ∎

  _∙_ : K[ G ]1 → K[ G ]1 → K[ G ]1
  _∙_ x = rec λ where
    .is-groupoidʳ → is-groupoid
    .baseʳ    → x
    .loopʳ g  → lemma g x
    .loop-idʳ → lemma-id x
    .loop-∘ʳ  → lemma-∘ _ _ x

  base-∙ : ∀ x → x ∙ base ≡ x
  base-∙ _ = refl _

  ∙-base : ∀ y → base ∙ y ≡ y
  ∙-base = elim-set λ where
    .is-setʳ _ → is-groupoid
    .baseʳ     → refl _
    .loopʳ y   →
      subst (λ y → base ∙ y ≡ y) (loop y) (refl _)    ≡⟨ subst-in-terms-of-trans-and-cong ⟩

      trans (sym (cong (base ∙_) (loop y)))
        (trans (refl _) (cong P.id (loop y)))         ≡⟨ cong (trans _) $
                                                         trans (trans-reflˡ _) $
                                                         sym $ cong-id _ ⟩

      trans (sym (cong (base ∙_) (loop y))) (loop y)  ≡⟨ cong (flip trans (loop y) ⊚ sym) $
                                                         rec-loop ⟩

      trans (sym (loop y)) (loop y)                   ≡⟨ trans-symˡ _ ⟩∎

      refl _                                          ∎

-- If P is a groupoid, then there is a based embedding from
-- (K[ Fundamental-group′ P s ]1 , base) to P (assuming univalence).
--
-- Christian Sattler showed me a similar proof of this result.

K[Fundamental-group′]1↣ᴮ :
  {P : Pointed-type p} {s : Is-set (proj₁ (Ω P))} →
  Univalence p →
  H-level 3 (proj₁ P) →
  (K[ Fundamental-group′ P s ]1 , base) ↝[ embedding ]ᴮ P
K[Fundamental-group′]1↣ᴮ {P = P@(A , a)} {s = s} univ g =
  record { to = to; is-embedding = emb } , refl _
  where
  to : K[ Fundamental-group′ P s ]1 → A
  to = rec λ where
    .baseʳ        → a
    .loopʳ        → P.id
    .loop-idʳ     → refl _
    .loop-∘ʳ      → refl _
    .is-groupoidʳ → g

  iso :
    Fundamental-group′ P s ≃ᴳ
    Fundamental-group′ (K[ Fundamental-group′ P s ]1 , base) is-groupoid
  iso = ≃ᴳ-sym $ Fundamental-group′[K1]≃ᴳ univ is-groupoid

  cong-to-iso : cong to ⊚ Homomorphic.to iso ≡ P.id
  cong-to-iso = ⟨ext⟩ λ eq →
    cong to (loop eq)  ≡⟨ rec-loop ⟩∎
    eq                 ∎

  cong-to-equivalence :
    Eq.Is-equivalence (cong {x = base} {y = base} to)
  cong-to-equivalence = Eq.Two-out-of-three.g∘f-f
    (Eq.two-out-of-three _ _)
    (Is-equivalence-cong _ (ext⁻¹ (sym cong-to-iso))
       (_≃_.is-equivalence Eq.id))
    (_≃_.is-equivalence (iso .related))

  emb : Is-embedding to
  emb = elim-prop λ where
    .is-propositionʳ _ →
      Π-closure ext 1 λ _ →
      Eq.propositional ext _
    .baseʳ → elim-prop λ where
      .is-propositionʳ _ → Eq.propositional ext _
      .baseʳ             → cong-to-equivalence

-- If P is a connected groupoid, then there is a based equivalence
-- from (K[ Fundamental-group′ P s ]1 , base) to P (assuming
-- univalence).
--
-- Christian Sattler showed me a similar proof of this result.

K[Fundamental-group′]1≃ᴮ :
  {P : Pointed-type p} {s : Is-set (proj₁ (Ω P))} →
  Univalence p →
  H-level 3 (proj₁ P) →
  Connected P →
  (K[ Fundamental-group′ P s ]1 , base) ≃ᴮ P
K[Fundamental-group′]1≃ᴮ {P = P@(A , a)} {s = s} univ g conn =
    Eq.⟨ Embedding.to (proj₁ f)
       , _≃_.to TP.surjective×embedding≃equivalence
           (surj , Embedding.is-embedding (proj₁ f)) ⟩
  , proj₂ f
  where
  f = K[Fundamental-group′]1↣ᴮ univ g

  surj : Surjective (Embedding.to (proj₁ f))
  surj x = flip TP.∥∥-map (conn x) λ a≡x →
      base
    , (Embedding.to (proj₁ f) base  ≡⟨⟩
       a                            ≡⟨ a≡x ⟩∎
       x                            ∎)

------------------------------------------------------------------------
-- Another result related to a fundamental group

-- If G is abelian, then the fundamental group of
-- (K[ G ]1 ≃ K[ G ]1 , Eq.id) is isomorphic to G (assuming
-- univalence).
--
-- I was informed of a related result by Christian Sattler.

Fundamental-group′[K1≃K1]≃ᴳ :
  {G : Group g} {s : Is-set _} →
  Univalence g →
  Abelian G →
  Fundamental-group′ ((K[ G ]1 ≃ K[ G ]1) , Eq.id) s ≃ᴳ G
Fundamental-group′[K1≃K1]≃ᴳ {G = G} univ abelian = λ where
    .related →
      _≡_ {A = K[ G ]1 ≃ K[ G ]1} Eq.id Eq.id  ↝⟨ inverse $ ≃-to-≡≃≡ ext ext ⟩
      ((x : K[ G ]1) → x ≡ x)                  ↝⟨ Eq.↔→≃ to from to-from from-to ⟩□
      Carrier                                  □
    .homomorphic p q →
      Homomorphic.to iso (cong (λ eq → _≃_.to eq base) (trans p q))  ≡⟨ cong (Homomorphic.to iso) $
                                                                        cong-trans _ _ _ ⟩
      Homomorphic.to iso
        (trans (cong (λ eq → _≃_.to eq base) p)
               (cong (λ eq → _≃_.to eq base) q))                     ≡⟨ Homomorphic.homomorphic iso _ _ ⟩∎

      Homomorphic.to iso (cong (λ eq → _≃_.to eq base) p) ∘
      Homomorphic.to iso (cong (λ eq → _≃_.to eq base) q)            ∎
  where
  open Group G

  iso = Fundamental-group′[K1]≃ᴳ {G = G} univ is-groupoid

  to : ((x : K[ G ]1) → x ≡ x) → Carrier
  to f = Homomorphic.to iso (f base)

  from : Carrier → (x : K[ G ]1) → x ≡ x
  from x = elim-set λ where
    .is-setʳ _ → is-groupoid
    .baseʳ     → loop x
    .loopʳ y   → ≡⇒↝ _ (sym [subst≡]≡[trans≡trans])
      (trans (loop x) (loop y)  ≡⟨ sym loop-∘ ⟩
       loop (x ∘ y)             ≡⟨ cong loop $ abelian x y ⟩
       loop (y ∘ x)             ≡⟨ loop-∘ ⟩∎
       trans (loop y) (loop x)  ∎)

  to-from : ∀ p → to (from p) ≡ p
  to-from x =
    Homomorphic.to iso (loop x)  ≡⟨ _≃_.right-inverse-of (Homomorphic.related iso) _ ⟩∎
    x                            ∎

  from-to : ∀ f → from (to f) ≡ f
  from-to f = ⟨ext⟩ $ elim-prop λ where
    .is-propositionʳ _ → is-groupoid
    .baseʳ             →
      loop (Homomorphic.to iso (f base))  ≡⟨ _≃_.left-inverse-of (Homomorphic.related iso) _ ⟩∎
      f base                              ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The equality can be turned into a groupoid which is sometimes
-- commutative
------------------------------------------------------------------------

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

open import Equality

module Equality.Groupoid
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Equality.Tactic eq
open import Groupoid eq
open import Pointed-type eq
open import Prelude hiding (id; _∘_)

------------------------------------------------------------------------
-- _≡_ comes with a groupoid structure

groupoid : ∀ {a} (A : Type a) → Groupoid a a
groupoid A = record
  { Object = A
  ; _∼_    = _≡_

  ; id  = refl _
  ; _∘_ = flip trans
  ; _⁻¹ = sym

  ; left-identity  = trans-reflʳ
  ; right-identity = trans-reflˡ
  ; assoc          = λ z≡u y≡z x≡y → trans-assoc x≡y y≡z z≡u
  ; left-inverse   = trans-symʳ
  ; right-inverse  = trans-symˡ
  }

------------------------------------------------------------------------
-- In some cases transitivity is commutative

-- This proof is based on an informal proof due to Thierry Coquand,
-- based on a result from homotopy theory.

module Transitivity-commutative
  {a} {A : Type a} (e : A) (_∙_ : A → A → A)
  (left-identity  : ∀ x → (e ∙ x) ≡ x)
  (right-identity : ∀ x → (x ∙ e) ≡ x)
  where

  open Groupoid (groupoid A) hiding (left-identity; right-identity)

  abstract

    commutative : (p q : e ≡ e) → p ∘ q ≡ q ∘ p
    commutative p q =
      p ∘ q                                 ≡⟨ cong (_∘_ p) (lem₁ _) ⟩
      p ∘ (ri ∘ li ⁻¹ ∘ q′ ∘ li ∘ ri ⁻¹)    ≡⟨ prove (Trans (Trans (Trans (Trans (Trans (Sym (Lift ri)) (Lift li)) (Lift q′))
                                                                          (Sym (Lift li))) (Lift ri)) (Lift p))
                                                     (Trans (Trans (Sym (Lift ri))
                                                                              (Trans (Trans (Lift li) (Lift q′)) (Sym (Lift li))))
                                                            (Trans (Lift ri) (Lift p)))
                                                     (refl _) ⟩
      (p ∘ ri) ∘ (li ⁻¹ ∘ q′ ∘ li) ∘ ri ⁻¹  ≡⟨ cong₂ (λ p q → p ∘ q ∘ ri ⁻¹) (lem₂ _) (lem₃ _) ⟩
      (ri ∘ lc p) ∘ rc q′ ∘ ri ⁻¹           ≡⟨ prove (Trans (Trans (Sym (Lift ri)) (Lift (rc q′))) (Trans (Lift (lc p)) (Lift ri)))
                                                     (Trans (Trans (Sym (Lift ri)) (Trans (Lift (rc q′)) (Lift (lc p)))) (Lift ri))
                                                     (refl _) ⟩
      ri ∘ (lc p ∘ rc q′) ∘ ri ⁻¹           ≡⟨ cong (λ p → ri ∘ p ∘ ri ⁻¹) (lem₄ _ _) ⟩
      ri ∘ (rc q′ ∘ lc p) ∘ ri ⁻¹           ≡⟨ prove (Trans (Trans (Sym (Lift ri)) (Trans (Lift (lc p)) (Lift (rc q′)))) (Lift ri))
                                                     (Trans (Trans (Trans (Sym (Lift ri)) (Lift (lc p))) (Lift (rc q′))) (Lift ri))
                                                     (refl _) ⟩
      ri ∘ rc q′ ∘ (lc p ∘ ri ⁻¹)           ≡⟨ cong₂ (λ p q → ri ∘ p ∘ q) (sym (lem₃ _)) (lem₅ _) ⟩
      ri ∘ (li ⁻¹ ∘ q′ ∘ li) ∘ (ri ⁻¹ ∘ p)  ≡⟨ prove (Trans (Trans (Trans (Lift p) (Sym (Lift ri)))
                                                                   (Trans (Trans (Lift li) (Lift q′)) (Sym (Lift li))))
                                                            (Lift ri))
                                                     (Trans (Lift p) (Trans (Trans (Trans (Trans (Sym (Lift ri)) (Lift li)) (Lift q′))
                                                                                (Sym (Lift li)))
                                                                            (Lift ri)))
                                                     (refl _) ⟩
      (ri ∘ li ⁻¹ ∘ q′ ∘ li ∘ ri ⁻¹) ∘ p    ≡⟨ cong (λ q → q ∘ p) (sym (lem₁ _)) ⟩∎
      q ∘ p                                 ∎
      where

      -- Abbreviations.

      li : ∀ {x} → (e ∙ x) ≡ x
      li = left-identity _

      ri : ∀ {x} → (x ∙ e) ≡ x
      ri = right-identity _

      q′ : e ≡ e
      q′ = li ∘ ri ⁻¹ ∘ q ∘ ri ∘ li ⁻¹

      lc : ∀ {x y} → x ≡ y → (x ∙ e) ≡ (y ∙ e)
      lc = cong (λ x → (x ∙ e))

      rc : ∀ {x y} → x ≡ y → (e ∙ x) ≡ (e ∙ y)
      rc = cong (λ y → (e ∙ y))

      -- Lemmas.

      lem₁ : (p : e ≡ e) →
             p ≡ ri ∘ li ⁻¹ ∘ (li ∘ ri ⁻¹ ∘ p ∘ ri ∘ li ⁻¹) ∘ li ∘ ri ⁻¹
      lem₁ p =
        p                                                          ≡⟨ prove (Lift p) (Trans (Trans Refl (Lift p)) Refl) (refl _) ⟩
        refl _ ∘ p ∘ refl _                                        ≡⟨ sym (cong₂ (λ q r → q ∘ p ∘ r)
                                                                                (right-inverse _) (right-inverse _)) ⟩
        (ri ∘ ri ⁻¹) ∘ p ∘ (ri ∘ ri ⁻¹)                            ≡⟨ prove (Trans (Trans (Trans (Sym (Lift ri)) (Lift ri)) (Lift p))
                                                                                (Trans (Sym (Lift ri)) (Lift ri)))
                                                                            (Trans (Trans (Trans (Trans (Trans (Trans
                                                                               (Sym (Lift ri)) Refl) (Lift ri)) (Lift p))
                                                                               (Sym (Lift ri))) Refl) (Lift ri))
                                                                            (refl _) ⟩
        ri ∘ refl _ ∘ ri ⁻¹ ∘ p ∘ ri ∘ refl _ ∘ ri ⁻¹              ≡⟨ sym (cong₂ (λ q r → ri ∘ q ∘ ri ⁻¹ ∘ p ∘ ri ∘ r ∘ ri ⁻¹)
                                                                                (left-inverse _) (left-inverse _)) ⟩
        ri ∘ (li ⁻¹ ∘ li) ∘ ri ⁻¹ ∘ p ∘ ri ∘ (li ⁻¹ ∘ li) ∘ ri ⁻¹  ≡⟨ prove (Trans (Trans (Trans (Trans (Trans (Trans
                                                                               (Sym (Lift ri)) (Trans (Lift li) (Sym (Lift li))))
                                                                               (Lift ri)) (Lift p)) (Sym (Lift ri)))
                                                                               (Trans (Lift li) (Sym (Lift li)))) (Lift ri))
                                                                            (Trans (Trans (Trans (Trans
                                                                               (Sym (Lift ri)) (Lift li))
                                                                               (Trans (Trans (Trans (Trans
                                                                                (Sym (Lift li)) (Lift ri)) (Lift p)) (Sym (Lift ri)))
                                                                                (Lift li))) (Sym (Lift li))) (Lift ri))
                                                                            (refl _) ⟩∎
        ri ∘ li ⁻¹ ∘ (li ∘ ri ⁻¹ ∘ p ∘ ri ∘ li ⁻¹) ∘ li ∘ ri ⁻¹    ∎

      lem₂ : ∀ {x y} (p : x ≡ y) → p ∘ ri ≡ ri ∘ lc p
      lem₂ = elim (λ p → p ∘ ri ≡ ri ∘ lc p) λ _ →
        prove (Trans (Lift ri) Refl)
              (Trans (Cong (λ x → (x ∙ e)) Refl) (Lift ri))
              (refl _)

      lem₃ : ∀ {x y} (p : x ≡ y) → li ⁻¹ ∘ p ∘ li ≡ rc p
      lem₃ = elim (λ p → li ⁻¹ ∘ p ∘ li ≡ rc p) λ x →
        li ⁻¹ ∘ refl x ∘ li  ≡⟨ prove (Trans (Trans (Lift li) Refl) (Sym (Lift li)))
                                      (Trans (Lift li) (Sym (Lift li)))
                                      (refl _) ⟩
        li ⁻¹ ∘ li           ≡⟨ left-inverse _ ⟩
        refl (e ∙ x)         ≡⟨ prove Refl (Cong (λ y → (e ∙ y)) Refl) (refl _) ⟩∎
        rc (refl x)          ∎

      lem₄ : (p q : e ≡ e) → lc p ∘ rc q ≡ rc q ∘ lc p
      lem₄ p q = elim
        (λ {x y} x≡y → lc x≡y ∘ cong (λ z → (x ∙ z)) q ≡
                       cong (λ z → (y ∙ z)) q ∘ lc x≡y)
        (λ x → prove (Trans (Cong (λ z → x ∙ z) (Lift q))
                            (Cong (λ x → x ∙ e) Refl))
                     (Trans (Cong (λ x → x ∙ e) Refl)
                            (Cong (λ z → x ∙ z) (Lift q)))
                     (refl _))
        p

      lem₅ : ∀ {x y} (p : x ≡ y) → lc p ∘ ri ⁻¹ ≡ ri ⁻¹ ∘ p
      lem₅ = elim (λ p → lc p ∘ ri ⁻¹ ≡ ri ⁻¹ ∘ p) λ _ →
        prove (Trans (Sym (Lift ri)) (Cong (λ x → (x ∙ e)) Refl))
              (Trans Refl (Sym (Lift ri)))
              (refl _)

-- In particular, transitivity is commutative for proofs in
-- proj₁ (Ω[ 2 + n ] X).

Ω[2+n]-commutative :
  ∀ {x} {X : Pointed-type x} n →
  (p q : proj₁ (Ω[ 2 + n ] X)) → trans p q ≡ trans q p
Ω[2+n]-commutative {X = X} n p q =
  Transitivity-commutative.commutative
    id _∘_ left-identity right-identity q p
  where
  open Groupoid (groupoid (proj₁ (Ω[ n ] X)))


text:
module Implicits.Syntax.Type.Unification.Lemmas where

open import Prelude
open import Data.Nat.Properties.Simple
open import Data.Maybe as Maybe
open import Data.Vec
open import Extensions.Vec

open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification hiding (open-meta)
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas.MetaType

open MetaTypeMetaSubst
open MetaTypeMetaLemmas

open import Relation.Binary.HeterogeneousEquality as H using ()

-- the following properties of mgu are assumed to hold here but have been proven by
-- Conor McBride (and verified using the LEGO dependently typed language)

postulate sound : ∀ {m ν} (a : MetaType m ν) (b : SimpleType ν) →
                  Maybe.All (Unifier a b) (mgu a b)

postulate complete : ∀ {m ν} (a : MetaType m ν) (b : SimpleType ν) u →
                     Unifier a b u →
                     Is-just (mgu a b)

to-meta-zero-vanishes : ∀ {ν} {a : Type ν} → from-meta (to-meta a) ≡ a
to-meta-zero-vanishes {a = simpl (tc x)} = refl
to-meta-zero-vanishes {a = simpl (tvar n)} = refl
to-meta-zero-vanishes {a = simpl (a →' b)} =
  cong₂ (λ u v → simpl (u →' v)) to-meta-zero-vanishes to-meta-zero-vanishes
to-meta-zero-vanishes {a = a ⇒ b} = cong₂ _⇒_ to-meta-zero-vanishes to-meta-zero-vanishes
to-meta-zero-vanishes {a = ∀' a} = cong ∀' to-meta-zero-vanishes

mutual
  from-to-smeta : ∀ {ν} (a : SimpleType ν) → from-smeta (to-smeta a) ≡ a
  from-to-smeta (tc x) = refl
  from-to-smeta (tvar n) = refl
  from-to-smeta (a →' b) = cong₂ _→'_ (from-to-meta a) (from-to-meta b)

  from-to-meta : ∀ {ν} (a : Type ν) → from-meta (to-meta a) ≡ a
  from-to-meta (simpl x) = cong simpl (from-to-smeta x)
  from-to-meta (a ⇒ b) = cong₂ _⇒_ (from-to-meta a) (from-to-meta b)
  from-to-meta (∀' a) = cong ∀' (from-to-meta a)

from-to-meta-/-vanishes : ∀ {ν} {a : Type ν} {s} →
                          from-meta (to-meta {zero} a MetaTypeMetaSubst./ s) ≡ a
from-to-meta-/-vanishes {a = a} {s = []} = begin
  from-meta (MetaTypeMetaSubst._/_ (to-meta {zero} a) [])
    ≡⟨ cong (λ q → from-meta q) (MetaTypeMetaLemmas.id-vanishes (to-meta {zero} a)) ⟩
  from-meta (to-meta {zero} a)
    ≡⟨ to-meta-zero-vanishes ⟩
  a ∎

mgu-id : ∀ {ν} → (a : SimpleType ν) → Unifiable {m = zero} (simpl (to-smeta a)) a
mgu-id a = [] , (begin
  from-meta (MetaTypeMetaSubst._/_ (simpl (to-smeta a)) [])
    ≡⟨ from-to-meta-/-vanishes ⟩
  simpl a ∎)

mvar-unifiable : ∀ {ν m} (n : Fin m) (τ : SimpleType ν) → Unifiable (simpl (mvar n)) τ
mvar-unifiable n τ = u , p
  where
    u = replicate (simpl (tc zero)) [ n ]≔ simpl (to-smeta τ)

    p : from-meta (lookup n u) ≡ simpl τ
    p = begin
      from-meta (lookup n u)
        ≡⟨ cong from-meta (lookup-≔ (replicate (simpl (tc zero))) n _) ⟩
      simpl (from-smeta (to-smeta τ))
        ≡⟨ cong simpl (from-to-smeta τ) ⟩
      simpl τ ∎


text:
-- Andreas, 2017-01-13, issue #2402
-- Error message: incomplete pattern matching

open import Common.Bool

module _ (A B C D E F G H I J K L M O P Q R S T U V W X Y Z : Set) where

test2 : Bool → Bool
test2 x with true
test2 true | x = ?

-- WAS: Reports:
-- Incomplete pattern matching for .IncompletePattern.with-56.
-- Missing cases:
--   .IncompletePattern.with-56 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ false
-- when checking the definition of with-56
-- That's total bogus!

-- Expected:

-- Incomplete pattern matching for .Issue2402-2.with-56.
-- Missing cases:
--   test2 false | w
-- when checking the definition of with-56

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Ring.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

record IsRing {R : Type ℓ}
              (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where

  constructor isring

  field
    +IsAbGroup : IsAbGroup 0r _+_ -_
    ·IsMonoid  : IsMonoid 1r _·_
    dist        : (x y z : R) → (x · (y + z) ≡ (x · y) + (x · z))
                              × ((x + y) · z ≡ (x · z) + (y · z))
    -- This is in the Agda stdlib, but it's redundant
    -- zero             : (x : R) → (x · 0r ≡ 0r) × (0r · x ≡ 0r)

  open IsAbGroup +IsAbGroup public
    renaming
      ( assoc       to +Assoc
      ; identity    to +Identity
      ; lid         to +Lid
      ; rid         to +Rid
      ; inverse     to +Inv
      ; invl        to +Linv
      ; invr        to +Rinv
      ; comm        to +Comm
      ; isSemigroup to +IsSemigroup
      ; isMonoid    to +IsMonoid
      ; isGroup     to +IsGroup )

  open IsMonoid ·IsMonoid public
    renaming
      ( assoc       to ·Assoc
      ; identity    to ·Identity
      ; lid         to ·Lid
      ; rid         to ·Rid
      ; isSemigroup to ·IsSemigroup )
    hiding
      ( is-set ) -- We only want to export one proof of this

  ·Rdist+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
  ·Rdist+ x y z = dist x y z .fst

  ·Ldist+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z)
  ·Ldist+ x y z = dist x y z .snd

record RingStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor ringstr

  field
    0r      : A
    1r      : A
    _+_     : A → A → A
    _·_     : A → A → A
    -_      : A → A
    isRing  : IsRing 0r 1r _+_ _·_ -_

  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_

  open IsRing isRing public

Ring : ∀ ℓ → Type (ℓ-suc ℓ)
Ring ℓ = TypeWithStr ℓ RingStr

isSetRing : (R : Ring ℓ) → isSet ⟨ R ⟩
isSetRing R = R .snd .RingStr.isRing .IsRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

makeIsRing : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R}
             (is-setR : isSet R)
             (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
             (+-rid : (x : R) → x + 0r ≡ x)
             (+-rinv : (x : R) → x + (- x) ≡ 0r)
             (+-comm : (x y : R) → x + y ≡ y + x)
             (r+-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
             (·-rid : (x : R) → x · 1r ≡ x)
             (·-lid : (x : R) → 1r · x ≡ x)
             (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
             (·-ldist-+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z))
           → IsRing 0r 1r _+_ _·_ -_
makeIsRing is-setR assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+ =
  isring (makeIsAbGroup is-setR assoc +-rid +-rinv +-comm)
         (makeIsMonoid is-setR ·-assoc ·-rid ·-lid)
         λ x y z → ·-rdist-+ x y z , ·-ldist-+ x y z

makeRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
           (is-setR : isSet R)
           (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
           (+-rid : (x : R) → x + 0r ≡ x)
           (+-rinv : (x : R) → x + (- x) ≡ 0r)
           (+-comm : (x y : R) → x + y ≡ y + x)
           (+-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
           (·-rid : (x : R) → x · 1r ≡ x)
           (·-lid : (x : R) → 1r · x ≡ x)
           (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
           (·-ldist-+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z))
         → Ring ℓ
makeRing 0r 1r _+_ _·_ -_ is-setR assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+ =
  _ , ringstr 0r 1r _+_ _·_ -_
       (makeIsRing is-setR assoc +-rid +-rinv +-comm
                   ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+ )

record IsRingHom {A : Type ℓ} {B : Type ℓ'} (R : RingStr A) (f : A → B) (S : RingStr B)
  : Type (ℓ-max ℓ ℓ')
  where

  -- Shorter qualified names
  private
    module R = RingStr R
    module S = RingStr S

  field
    pres0 : f R.0r ≡ S.0r
    pres1 : f R.1r ≡ S.1r
    pres+ : (x y : A) → f (x R.+ y) ≡ f x S.+ f y
    pres· : (x y : A) → f (x R.· y) ≡ f x S.· f y
    pres- : (x : A) → f (R.- x) ≡ S.- (f x)

unquoteDecl IsRingHomIsoΣ = declareRecordIsoΣ IsRingHomIsoΣ (quote IsRingHom)

RingHom : (R : Ring ℓ) (S : Ring ℓ') → Type (ℓ-max ℓ ℓ')
RingHom R S = Σ[ f ∈ (⟨ R ⟩ → ⟨ S ⟩) ] IsRingHom (R .snd) f (S .snd)

IsRingEquiv : {A : Type ℓ} {B : Type ℓ'} (M : RingStr A) (e : A ≃ B) (N : RingStr B)
  → Type (ℓ-max ℓ ℓ')
IsRingEquiv M e N = IsRingHom M (e .fst) N

RingEquiv : (R : Ring ℓ) (S : Ring ℓ') → Type (ℓ-max ℓ ℓ')
RingEquiv R S = Σ[ e ∈ (⟨ R ⟩ ≃ ⟨ S ⟩) ] IsRingEquiv (R .snd) e (S .snd)

_$_ : {R S : Ring ℓ} → (φ : RingHom R S) → (x : ⟨ R ⟩) → ⟨ S ⟩
φ $ x = φ .fst x

RingEquiv→RingHom : {A B : Ring ℓ} → RingEquiv A B → RingHom A B
RingEquiv→RingHom (e , eIsHom) = e .fst , eIsHom

isPropIsRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
             → isProp (IsRing 0r 1r _+_ _·_ -_)
isPropIsRing 0r 1r _+_ _·_ -_ (isring RG RM RD) (isring SG SM SD) =
  λ i → isring (isPropIsAbGroup _ _ _ RG SG i)
               (isPropIsMonoid _ _ RM SM i)
               (isPropDistr RD SD i)
  where
  isSetR : isSet _
  isSetR = RM .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropDistr : isProp ((x y z : _) → ((x · (y + z)) ≡ ((x · y) + (x · z)))
                                    × (((x + y) · z) ≡ ((x · z) + (y · z))))
  isPropDistr = isPropΠ3 λ _ _ _ → isProp× (isSetR _ _) (isSetR _ _)

isPropIsRingHom : {A : Type ℓ} {B : Type ℓ'} (R : RingStr A) (f : A → B) (S : RingStr B)
  → isProp (IsRingHom R f S)
isPropIsRingHom R f S = isOfHLevelRetractFromIso 1 IsRingHomIsoΣ
                        (isProp×4 (isSetRing (_ , S) _ _)
                                  (isSetRing (_ , S) _ _)
                                  (isPropΠ2 λ _ _ → isSetRing (_ , S) _ _)
                                  (isPropΠ2 λ _ _ → isSetRing (_ , S) _ _)
                                  (isPropΠ λ _ → isSetRing (_ , S) _ _))

isSetRingHom : (R : Ring ℓ) (S : Ring ℓ') → isSet (RingHom R S)
isSetRingHom R S = isSetΣSndProp (isSetΠ (λ _ → isSetRing S)) (λ f → isPropIsRingHom (snd R) f (snd S))

RingHomPathP : (R S T : Ring ℓ) (p : S ≡ T) (φ : RingHom R S) (ψ : RingHom R T)
             → PathP (λ i → R .fst → p i .fst) (φ .fst) (ψ .fst)
             → PathP (λ i → RingHom R (p i)) φ ψ
RingHomPathP R S T p φ ψ q = ΣPathP (q , isProp→PathP (λ _ → isPropIsRingHom _ _ _) _ _)

RingHom≡ : {R S : Ring ℓ} {φ ψ : RingHom R S} → fst φ ≡ fst ψ → φ ≡ ψ
RingHom≡ = Σ≡Prop λ f → isPropIsRingHom _ f _

𝒮ᴰ-Ring : DUARel (𝒮-Univ ℓ) RingStr ℓ
𝒮ᴰ-Ring =
  𝒮ᴰ-Record (𝒮-Univ _) IsRingEquiv
    (fields:
      data[ 0r ∣ null ∣ pres0 ]
      data[ 1r ∣ null ∣ pres1 ]
      data[ _+_ ∣ bin ∣ pres+ ]
      data[ _·_ ∣ bin ∣ pres· ]
      data[ -_ ∣ un ∣ pres- ]
      prop[ isRing ∣ (λ _ _ → isPropIsRing _ _ _ _ _) ])
 where
  open RingStr
  open IsRingHom

  -- faster with some sharing
  null = autoDUARel (𝒮-Univ _) (λ A → A)
  un = autoDUARel (𝒮-Univ _) (λ A → A → A)
  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)

RingPath : (R S : Ring ℓ) → RingEquiv R S ≃ (R ≡ S)
RingPath = ∫ 𝒮ᴰ-Ring .UARel.ua

-- Rings have an abelian group and a monoid

Ring→AbGroup : Ring ℓ → AbGroup ℓ
Ring→AbGroup (A , ringstr _ _ _ _ _ R) = A , abgroupstr _ _ _ (IsRing.+IsAbGroup R)

Ring→Group : Ring ℓ → Group ℓ
Ring→Group = AbGroup→Group ∘ Ring→AbGroup

Ring→AddMonoid : Ring ℓ → Monoid ℓ
Ring→AddMonoid = Group→Monoid ∘ Ring→Group

Ring→MultMonoid : Ring ℓ → Monoid ℓ
Ring→MultMonoid (A , ringstr _ _ _ _ _ R) = monoid _ _ _ (IsRing.·IsMonoid R)

-- Smart constructor for ring homomorphisms
-- that infers the other equations from pres1, pres+, and pres·

module _ {R : Ring ℓ} {S : Ring ℓ'} {f : ⟨ R ⟩ → ⟨ S ⟩} where

  private
    module R = RingStr (R .snd)
    module S = RingStr (S .snd)

  module _
    (p1 : f R.1r ≡ S.1r)
    (p+ : (x y : ⟨ R ⟩) → f (x R.+ y) ≡ f x S.+ f y)
    (p· : (x y : ⟨ R ⟩) → f (x R.· y) ≡ f x S.· f y)
    where

    open IsRingHom
    private
      isGHom : IsGroupHom (Ring→Group R .snd) f (Ring→Group S .snd)
      isGHom = makeIsGroupHom p+

    makeIsRingHom : IsRingHom (R .snd) f (S .snd)
    makeIsRingHom .pres0 = isGHom .IsGroupHom.pres1
    makeIsRingHom .pres1 = p1
    makeIsRingHom .pres+ = p+
    makeIsRingHom .pres· = p·
    makeIsRingHom .pres- = isGHom .IsGroupHom.presinv


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Operations on and properties of decidable relations
--
-- This file contains some core definitions which are re-exported by
-- Relation.Nullary.Decidable
------------------------------------------------------------------------

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

module Relation.Nullary.Decidable.Core where

open import Level using (Level; Lift)
open import Data.Bool.Base using (Bool; false; true; not; T)
open import Data.Unit.Base using (⊤)
open import Data.Empty
open import Data.Product
open import Function.Base

open import Agda.Builtin.Equality
open import Relation.Nullary.Reflects
open import Relation.Nullary

private
  variable
    p q : Level
    P : Set p
    Q : Set q

-- `isYes` is a stricter version of `does`. The lack of computation means that
-- we can recover the proposition `P` from `isYes P?` by unification. This is
-- useful when we are using the decision procedure for proof automation.

isYes : Dec P → Bool
isYes ( true because _) = true
isYes (false because _) = false

isYes≗does : (P? : Dec P) → isYes P? ≡ does P?
isYes≗does ( true because _) = refl
isYes≗does (false because _) = refl

-- The traditional name for isYes is ⌊_⌋, indicating the stripping of evidence.
⌊_⌋ = isYes

isNo : Dec P → Bool
isNo = not ∘ isYes

True : Dec P → Set
True Q = T (isYes Q)

False : Dec P → Set
False Q = T (isNo Q)

-- Gives a witness to the "truth".

toWitness : {Q : Dec P} → True Q → P
toWitness {Q = true  because [p]} _  = invert [p]
toWitness {Q = false because  _ } ()

-- Establishes a "truth", given a witness.

fromWitness : {Q : Dec P} → P → True Q
fromWitness {Q = true  because   _ } = const _
fromWitness {Q = false because [¬p]} = invert [¬p]

-- Variants for False.

toWitnessFalse : {Q : Dec P} → False Q → ¬ P
toWitnessFalse {Q = true  because   _ } ()
toWitnessFalse {Q = false because [¬p]} _  = invert [¬p]

fromWitnessFalse : {Q : Dec P} → ¬ P → False Q
fromWitnessFalse {Q = true  because [p]} = flip _$_ (invert [p])
fromWitnessFalse {Q = false because  _ } = const _

-- If a decision procedure returns "yes", then we can extract the
-- proof using from-yes.

module _ {p} {P : Set p} where

  From-yes : Dec P → Set p
  From-yes (true  because _) = P
  From-yes (false because _) = Lift p ⊤

  from-yes : (p : Dec P) → From-yes p
  from-yes (true  because [p]) = invert [p]
  from-yes (false because _ ) = _

-- If a decision procedure returns "no", then we can extract the proof
-- using from-no.

  From-no : Dec P → Set p
  From-no (false because _) = ¬ P
  From-no (true  because _) = Lift p ⊤

  from-no : (p : Dec P) → From-no p
  from-no (false because [¬p]) = invert [¬p]
  from-no (true  because   _ ) = _

------------------------------------------------------------------------
-- Result of decidability

dec-true : (p? : Dec P) → P → does p? ≡ true
dec-true (true  because   _ ) p = refl
dec-true (false because [¬p]) p = ⊥-elim (invert [¬p] p)

dec-false : (p? : Dec P) → ¬ P → does p? ≡ false
dec-false (false because  _ ) ¬p = refl
dec-false (true  because [p]) ¬p = ⊥-elim (¬p (invert [p]))

dec-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
dec-yes p? p with dec-true p? p
dec-yes (yes p′) p | refl = p′ , refl

dec-no : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
dec-no p? ¬p with dec-false p? ¬p
dec-no (no ¬p′) ¬p | refl = ¬p′ , refl

dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
dec-yes-irr p? irr p with dec-yes p? p
... | p′ , eq rewrite irr p p′ = eq

------------------------------------------------------------------------
-- Maps

map′ : (P → Q) → (Q → P) → Dec P → Dec Q
does  (map′ P→Q Q→P p?)                   = does p?
proof (map′ P→Q Q→P (true  because  [p])) = ofʸ (P→Q (invert [p]))
proof (map′ P→Q Q→P (false because [¬p])) = ofⁿ (invert [¬p] ∘ Q→P)


text:
------------------------------------------------------------------------
-- Digits and digit expansions
------------------------------------------------------------------------

module Data.Digit where

open import Data.Nat
open import Data.Nat.Properties
open SemiringSolver
open import Data.Fin as Fin using (Fin; zero; suc; toℕ)
open import Relation.Nullary.Decidable
open import Data.Char using (Char)
open import Data.List
open import Data.Vec as Vec using (Vec; _∷_; [])
open import Induction.Nat
open import Data.Nat.DivMod
open ≤-Reasoning
open import Relation.Binary.PropositionalEquality
open import Data.Function

------------------------------------------------------------------------
-- A boring lemma

private

  lem : ∀ x k r → 2 + x ≤′ r + (1 + x) * (2 + k)
  lem x k r = ≤⇒≤′ $ begin
    2 + x
      ≤⟨ m≤m+n _ _ ⟩
    2 + x + (x + (1 + x) * k + r)
      ≡⟨ solve 3 (λ x r k → con 2 :+ x :+ (x :+ (con 1 :+ x) :* k :+ r)
                              :=
                            r :+ (con 1 :+ x) :* (con 2 :+ k))
                 refl x r k ⟩
    r + (1 + x) * (2 + k)
      ∎

------------------------------------------------------------------------
-- Digits

-- Digit b is the type of digits in base b.

Digit : ℕ → Set
Digit b = Fin b

-- Some specific digit kinds.

Decimal = Digit 10
Bit     = Digit 2

-- Some named digits.

0b : Bit
0b = zero

1b : Bit
1b = suc zero

------------------------------------------------------------------------
-- Showing digits

-- The characters used to show the first 16 digits.

digitChars : Vec Char 16
digitChars =
  '0' ∷ '1' ∷ '2' ∷ '3' ∷ '4' ∷ '5' ∷ '6' ∷ '7' ∷ '8' ∷ '9' ∷
  'a' ∷ 'b' ∷ 'c' ∷ 'd' ∷ 'e' ∷ 'f' ∷ []

-- showDigit shows digits in base ≤ 16.

showDigit : ∀ {base} {base≤16 : True (base ≤? 16)} →
            Digit base → Char
showDigit {base≤16 = base≤16} d =
  Vec.lookup (Fin.inject≤ d (witnessToTruth base≤16)) digitChars

------------------------------------------------------------------------
-- Digit expansions

-- fromDigits takes a digit expansion of a natural number, starting
-- with the _least_ significant digit, and returns the corresponding
-- natural number.

fromDigits : ∀ {base} → List (Fin base) → ℕ
fromDigits        []       = 0
fromDigits {base} (d ∷ ds) = toℕ d + fromDigits ds * base

-- toDigits b n yields the digits of n, in base b, starting with the
-- _least_ significant digit.
--
-- Note that the list of digits is always non-empty.
--
-- This function should be linear in n, if optimised properly (see
-- Data.Nat.DivMod).

data Digits (base : ℕ) : ℕ → Set where
  digits : (ds : List (Fin base)) → Digits base (fromDigits ds)

toDigits : (base : ℕ) {base≥2 : True (2 ≤? base)} (n : ℕ) →
           Digits base n
toDigits zero       {base≥2 = ()} _
toDigits (suc zero) {base≥2 = ()} _
toDigits (suc (suc k)) n = <-rec Pred helper n
  where
  base = suc (suc k)
  Pred = Digits base

  cons : ∀ {n} (r : Fin base) → Pred n → Pred (toℕ r + n * base)
  cons r (digits ds) = digits (r ∷ ds)

  helper : ∀ n → <-Rec Pred n → Pred n
  helper n rec with n divMod base
  helper .(toℕ r + 0     * base) rec | result zero    r = digits (r ∷ [])
  helper .(toℕ r + suc x * base) rec | result (suc x) r =
    cons r (rec (suc x) (lem (pred (suc x)) k (toℕ r)))

theDigits : (base : ℕ) {base≥2 : True (2 ≤? base)} (n : ℕ) →
            List (Fin base)
theDigits base {base≥2} n       with toDigits base {base≥2} n
theDigits base .(fromDigits ds) | digits ds = ds

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Adding forcing to functions (f in this case) leaves
-- an unsolved meta of type I (for the argument to f).
module Issue330 where

postulate
 I : Set
 i : I

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

f : ∀ n → D n → D n
f n d = d

data P : D i → Set where
 c : ∀ v → P (f i v)

p : P d
p = c _


text:
module Language.Greek where

data Maybe A : Set where
  none : Maybe A
  just : A → Maybe A

data Unicode : Set where
  Α Β Γ Δ Ε Ζ Η Θ Ι Κ Λ Μ Ν Ξ Ο Π Ρ Σ Τ Υ Φ Χ Ψ Ω α β γ δ ε ζ η θ ι κ λ′ μ ν ξ ο π ρ σ ς τ υ φ χ ψ ω : Unicode
  grave acute diaeresis smooth rough circumflex iotaSubscript : Unicode

postulate
  Char : Set

{-# BUILTIN CHAR Char #-}
{-# COMPILED_TYPE Char Char #-}

charToUnicode : Char -> Maybe Unicode
charToUnicode 'Α' = just Α
charToUnicode 'Β' = just Β
charToUnicode 'Γ' = just Γ
charToUnicode 'Δ' = just Δ
charToUnicode 'Ε' = just Ε
charToUnicode 'Ζ' = just Ζ
charToUnicode 'Η' = just Η
charToUnicode 'Θ' = just Θ
charToUnicode 'Ι' = just Ι
charToUnicode 'Κ' = just Κ
charToUnicode 'Λ' = just Λ
charToUnicode 'Μ' = just Μ
charToUnicode 'Ν' = just Ν
charToUnicode 'Ξ' = just Ξ
charToUnicode 'Ο' = just Ο
charToUnicode 'Π' = just Π
charToUnicode 'Ρ' = just Ρ
charToUnicode 'Σ' = just Σ
charToUnicode 'Τ' = just Τ
charToUnicode 'Υ' = just Υ
charToUnicode 'Φ' = just Φ
charToUnicode 'Χ' = just Χ
charToUnicode 'Ψ' = just Ψ
charToUnicode 'Ω' = just Ω
charToUnicode 'α' = just α
charToUnicode 'β' = just β
charToUnicode 'γ' = just γ
charToUnicode 'δ' = just δ
charToUnicode 'ε' = just ε
charToUnicode 'ζ' = just ζ
charToUnicode 'η' = just η
charToUnicode 'θ' = just θ
charToUnicode 'ι' = just ι
charToUnicode 'κ' = just κ
charToUnicode 'λ' = just λ′
charToUnicode 'μ' = just μ
charToUnicode 'ν' = just ν
charToUnicode 'ξ' = just ξ
charToUnicode 'ο' = just ο
charToUnicode 'π' = just π
charToUnicode 'ρ' = just ρ
charToUnicode 'ς' = just ς
charToUnicode 'σ' = just σ
charToUnicode 'τ' = just τ
charToUnicode 'υ' = just υ
charToUnicode 'φ' = just φ
charToUnicode 'χ' = just χ
charToUnicode 'ψ' = just ψ
charToUnicode 'ω' = just ω
charToUnicode '\x0300' = just grave          -- COMBINING GRAVE ACCENT
charToUnicode '\x0301' = just acute          -- COMBINING ACUTE ACCENT
charToUnicode '\x0308' = just diaeresis      -- COMBINING DIAERESIS
charToUnicode '\x0313' = just smooth         -- COMBINING COMMA ABOVE
charToUnicode '\x0314' = just rough          -- COMBINING REVERSED COMMA ABOVE
charToUnicode '\x0342' = just circumflex     -- COMBINING GREEK PERISPOMENI
charToUnicode '\x0345' = just iotaSubscript  -- COMBINING GREEK YPOGEGRAMMENI
charToUnicode _ = none

data UnicodeCategory : Set where
  letter mark : UnicodeCategory

unicodeToCategory : Unicode → UnicodeCategory
unicodeToCategory Α = letter
unicodeToCategory Β = letter
unicodeToCategory Γ = letter
unicodeToCategory Δ = letter
unicodeToCategory Ε = letter
unicodeToCategory Ζ = letter
unicodeToCategory Η = letter
unicodeToCategory Θ = letter
unicodeToCategory Ι = letter
unicodeToCategory Κ = letter
unicodeToCategory Λ = letter
unicodeToCategory Μ = letter
unicodeToCategory Ν = letter
unicodeToCategory Ξ = letter
unicodeToCategory Ο = letter
unicodeToCategory Π = letter
unicodeToCategory Ρ = letter
unicodeToCategory Σ = letter
unicodeToCategory Τ = letter
unicodeToCategory Υ = letter
unicodeToCategory Φ = letter
unicodeToCategory Χ = letter
unicodeToCategory Ψ = letter
unicodeToCategory Ω = letter
unicodeToCategory α = letter
unicodeToCategory β = letter
unicodeToCategory γ = letter
unicodeToCategory δ = letter
unicodeToCategory ε = letter
unicodeToCategory ζ = letter
unicodeToCategory η = letter
unicodeToCategory θ = letter
unicodeToCategory ι = letter
unicodeToCategory κ = letter
unicodeToCategory λ′ = letter
unicodeToCategory μ = letter
unicodeToCategory ν = letter
unicodeToCategory ξ = letter
unicodeToCategory ο = letter
unicodeToCategory π = letter
unicodeToCategory ρ = letter
unicodeToCategory σ = letter
unicodeToCategory ς = letter
unicodeToCategory τ = letter
unicodeToCategory υ = letter
unicodeToCategory φ = letter
unicodeToCategory χ = letter
unicodeToCategory ψ = letter
unicodeToCategory ω = letter
unicodeToCategory grave = mark
unicodeToCategory acute = mark
unicodeToCategory diaeresis = mark
unicodeToCategory smooth = mark
unicodeToCategory rough = mark
unicodeToCategory circumflex = mark
unicodeToCategory iotaSubscript = mark

data List A : Set where
  [] : List A
  _∷_ : A → List A -> List A

infixr 6 _∷_

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

data _And_ : (A : Set) → (B : Set) → Set₁ where
  _and_ : {A B : Set} → A → B → A And B

data ConcreteLetter : Set where
  Α Β Γ Δ Ε Ζ Η Θ Ι Κ Λ Μ Ν Ξ Ο Π Ρ Σ Τ Υ Φ Χ Ψ Ω α β γ δ ε ζ η θ ι κ λ′ μ ν ξ ο π ρ σ ς τ υ φ χ ψ ω : ConcreteLetter

data ConcreteMark : Set where
  grave acute diaeresis smooth rough circumflex iotaSubscript : ConcreteMark

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
module Issue481Record where

record Issue481Record : Set where


text:
{-# OPTIONS --without-K --safe #-}
open import Level
open import Categories.Category using (Category)

module Categories.NaturalTransformation.Hom {o ℓ e : Level} (C : Category o ℓ e) where

open import Categories.Category.Instance.Setoids
open import Categories.Functor.Hom using (module Hom; Hom[_][-,_]; Hom[_][_,-]; Hom[_][-,-])
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN)

import Categories.Morphism.Reasoning as MR

open Category C
open HomReasoning
open MR C
open NaturalTransformation
private
  module CE = Category.Equiv C
  module C = Category C

Hom[A,C]⇒Hom[B,C] : {A B : Obj} → (A ⇒ B) → NaturalTransformation Hom[ C ][-, A ] Hom[ C ][-, B ]
Hom[A,C]⇒Hom[B,C] {A} A⇒B = ntHelper record
  { η       = λ X → record { _⟨$⟩_ = λ X⇒A → A⇒B ∘ X⇒A ; cong = ∘-resp-≈ʳ }
  ; commute = λ f {g} {h} g≈h → begin
      A⇒B ∘ id ∘ g ∘ f   ≈⟨ sym-assoc ⟩
      (A⇒B ∘ id) ∘ g ∘ f ≈⟨ id-comm ⟩∘⟨ g≈h ⟩∘⟨refl ⟩
      (id ∘ A⇒B) ∘ h ∘ f ≈⟨ pullʳ sym-assoc ⟩
      id ∘ (A⇒B ∘ h) ∘ f ∎
  }

Hom[C,A]⇒Hom[C,B] : {A B : Obj} → (B ⇒ A) → NaturalTransformation Hom[ C ][ A ,-] Hom[ C ][ B ,-]
Hom[C,A]⇒Hom[C,B] {A} B⇒A = ntHelper record
  { η = λ X → record { _⟨$⟩_ = λ A⇒X → A⇒X ∘ B⇒A ; cong = ∘-resp-≈ˡ }
  ; commute = λ f {g} {h} g≈h → begin
      (f ∘ g ∘ id) ∘ B⇒A ≈⟨ pullʳ assoc ⟩
      f ∘ g ∘ id ∘ B⇒A   ≈⟨ (refl⟩∘⟨ g≈h ⟩∘⟨ id-comm-sym) ⟩
      f ∘ h ∘ B⇒A ∘ id   ≈⟨ (refl⟩∘⟨ sym-assoc) ⟩
      f ∘ (h ∘ B⇒A) ∘ id ∎
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Comments where

{- Single-line comments cannot be started inside multi-line ones:

-- -} postulate
        foo-- : Set -- Note that -- does not start a comment when
                    -- located inside or at the end of an identifier.

-- The following comment marker is followed by an alphabetic
-- character:

--This is a {- non-nested comment.
{-This is a comment.-}

{-
-- The final comment marker {- is followed by -} the end of the file
-- without any intervening newline.
-}

--

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pairs of lists that share no common elements (propositional equality)
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Relation.Binary.Disjoint.Propositional
  {a} {A : Set a} where

open import Relation.Binary.PropositionalEquality using (setoid)
open import Data.List.Relation.Binary.Disjoint.Setoid as DisjointUnique

------------------------------------------------------------------------
-- Re-export the contents of setoid uniqueness

open DisjointUnique (setoid A) public


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

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

import      LibraBFT.Impl.OBM.Crypto              as Crypto
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.Types.ValidatorVerifier as ValidatorVerifier
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
import      Util.KVMap                   as Map
open import Util.PKCS
open import Util.Prelude

module LibraBFT.Impl.Types.LedgerInfoWithSignatures where

obmNewNoSigs : LedgerInfo → LedgerInfoWithSignatures
obmNewNoSigs li = LedgerInfoWithSignatures∙new li Map.empty

-- HC-TODO : refactor this and TimeoutCertificate
addSignature : AccountAddress → Signature → LedgerInfoWithSignatures → LedgerInfoWithSignatures
addSignature validator sig liws =
  case Map.lookup validator (liws ^∙ liwsSignatures) of λ where
    (just _) → liws
    nothing  →
      liws & liwsSignatures ∙~ Map.kvm-insert-Haskell validator sig (liws ^∙ liwsSignatures)

verifySignatures : LedgerInfoWithSignatures → ValidatorVerifier → Either ErrLog Unit
verifySignatures self validator = withErrCtx'
  ("LedgerInfoWithSignatures" ∷ "verify" ∷ [])
  (ValidatorVerifier.batchVerifyAggregatedSignatures
     validator (self ^∙ liwsLedgerInfo) (self ^∙ liwsSignatures))