text:
module Data.Lens.Proofs.LensComposition where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Agda.Primitive
open import Data.Lens.Proofs.LensLaws
open import Data.Lens.Proofs.LensPostulates

-- We proof that if we have 2 valid lenses l1 and l2, that l1 ∘ l2 is also valid
-- We do this law by law

prop-Composition-ViewSet : {a b c : Set}
    -> (l1 : ValidLens a b)
    -> (l2 : ValidLens b c)
    -> ViewSet ((toLens l1) ∘ (toLens l2))
prop-Composition-ViewSet vl1@(CValidLens l1 vs1 sv1 ss1) vl2@(CValidLens l2 vs2 sv2 ss2) v s =
    begin
        view (l1 ∘ l2) (set (l1 ∘ l2) v s)
    =⟨ prop-view-compose vl1 vl2 (set (l1 ∘ l2) v s) ⟩
        view l2 ( view l1 (set (l1 ∘ l2) v s))
    =⟨ cong (view l2 ∘ view l1) (prop-set-compose-dir vl1 vl2 s v) ⟩
        view l2 ( view l1 (set l1 ((set l2 v) (view l1 s)) s))
    =⟨ cong (view l2) (vs1 ((set l2 v) (view l1 s)) s) ⟩
        view l2 (set l2 v (view l1 s))
    =⟨ vs2 v (view l1 s) ⟩
        v
    end

prop-Composition-SetView : {a b c : Set}
    -> (l1 : ValidLens a b)
    -> (l2 : ValidLens b c)
    -> SetView ((toLens l1) ∘ (toLens l2))
prop-Composition-SetView vl1@(CValidLens l1 vs1 sv1 ss1) vl2@(CValidLens l2 vs2 sv2 ss2) s =
    begin
        set (l1 ∘ l2) (view (l1 ∘ l2) s) s
    =⟨ cong (λ x -> set (l1 ∘ l2) x s) (prop-view-compose vl1 vl2 s) ⟩
        set (l1 ∘ l2) (view l2 (view l1 s)) s
    =⟨ prop-set-compose-dir vl1 vl2 s (view l2 (view l1 s)) ⟩
        set l1 (set l2 (view l2 (view l1 s)) (view l1 s)) s
    =⟨ cong (λ x -> set l1 x s) (sv2 (view l1 s)) ⟩
        set l1 (view l1 s) s
    =⟨ sv1 s ⟩
        s
    end

prop-Composition-SetSet : {a b c : Set}
    -> (l1 : ValidLens a b)
    -> (l2 : ValidLens b c)
    -> SetSet ((toLens l1) ∘ (toLens l2))
prop-Composition-SetSet vl1@(CValidLens l1 vs1 sv1 ss1) vl2@(CValidLens l2 vs2 sv2 ss2) v1 v2 s =
    begin
        set (l1 ∘ l2) v2 (set (l1 ∘ l2) v1 s)
    =⟨ cong (set (l1 ∘ l2) v2) (prop-set-compose-dir vl1 vl2 s v1) ⟩
        set (l1 ∘ l2) v2 (set l1 (set l2 v1 (view l1 s)) s)
    =⟨ prop-set-compose-dir vl1 vl2 (set l1 ((set l2 v1) (view l1 s)) s) v2 ⟩
        set l1
            (set l2
                v2
                (view l1
                    (set l1 ((set l2 v1) (view l1 s)) s)
                )
            )
            (set l1 (set l2 v1 (view l1 s)) s)
    =⟨ cong (λ x -> set l1 (set l2 v2 x) (set l1 ((set l2 v1) (view l1 s)) s)) (vs1 ((set l2 v1) (view l1 s)) s) ⟩
        set l1
            (set l2
                v2
                (set l2 v1 (view l1 s))
            )
            (set l1 (set l2 v1 (view l1 s)) s)
    =⟨ cong (λ x -> set l1 x (set l1 (set l2 v1 (view l1 s)) s)) (ss2 v1 v2 (view l1 s)) ⟩
        set l1
            (set l2
                v2
                (view l1 s)
            )
            (set l1 (set l2 v1 (view l1 s)) s)
    =⟨ ss1 ((set l2 v1 (view l1 s))) ((set l2 v2 (view l1 s))) s ⟩
        set l1
            (set l2
                v2
                (view l1 s)
            )
            s
    =⟨ sym (prop-set-compose-dir vl1 vl2 s v2) ⟩
        set (l1 ∘ l2) v2 s
    end

-- Create a function that does the composition
composeLens : {a b c : Set} -> (ValidLens a b) -> (ValidLens b c) -> (ValidLens a c)
composeLens vl1@(CValidLens l1 vs1 sv1 ss1) vl2@(CValidLens l2 vs2 sv2 ss2)
    = CValidLens (l1 ∘ l2) (prop-Composition-ViewSet vl1 vl2) (prop-Composition-SetView vl1 vl2) (prop-Composition-SetSet vl1 vl2)

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
-- Andreas, 2018-09-07 issue #3217 reported by Nisse
--
-- Missing range for cubical error

{-# OPTIONS --cubical #-}

-- {-# OPTIONS -v tc.term.lambda:100 -v tc.term:10 #-}

open import Agda.Builtin.Cubical.Path

data Bool : Set where
  true false : Bool

eq : true ≡ false
eq = λ i → true

-- Expected error
-- Issue3217.agda:15,12-16
-- true != false of type Bool
-- when checking that the expression λ i → true has type true ≡ false

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2015-07-07 continuation of issue 665

-- Jesper, 2015-12-18 some of these don't work anymore with the new unifier,
-- but a few others that weren't accepted are now.

{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.with.strip:10 #-}
-- {-# OPTIONS -v tc.with.strip:60 -v tc.lhs:20 -v tc.lhs.unify:20 #-}

postulate
  C : Set
  anything : C

record I : Set where
  constructor c
  field
    {f} : C

data Wrap : (i : I) → Set where
  wrap : ∀ {i} → Wrap i

-- Test 0: first argument not given

test0 : ∀ {j} → Wrap j → C
test0 wrap with anything
test0 wrap | z = z

test0a : ∀ {j} → Wrap j → C
test0a (wrap {c {x}}) with anything
test0a  wrap | z = z

test0b : ∀ {j} → Wrap j → C
test0b (wrap {c {_}}) with anything
test0b wrap | z = z

test0c : ∀ {j} → Wrap j → C
test0c (wrap {c}) with anything
test0c wrap | z = z

test0d : ∀ {j} → Wrap j → C
test0d (wrap {c {._}}) with anything
test0d  wrap | z = z

test0e : ∀ {j} → Wrap j → C
test0e (wrap .{c}) with anything
test0e  wrap | z = z

test0f : ∀ {j} → Wrap j → C
test0f (wrap .{c {_}}) with anything
test0f  wrap | z = z

--test00 : ∀ {j} → Wrap j → C
--test00 wrap with anything
--test00 {.c} wrap | z = z

test00a : ∀ {j} → Wrap j → C
test00a (wrap {c {x}}) with anything
test00a {.c} wrap | z = z

--test00b : ∀ {j} → Wrap j → C
--test00b (wrap {c {_}}) with anything
--test00b {.c} wrap | z = z

--test00c : ∀ {j} → Wrap j → C
--test00c (wrap {c}) with anything
--test00c {.c} wrap | z = z

--test00d : ∀ {j} → Wrap j → C
--test00d (wrap {c {._}}) with anything
--test00d {.c} wrap | z = z

--test00e : ∀ {j} → Wrap j → C
--test00e (wrap .{c}) with anything
--test00e {.c} wrap | z = z

--test00f : ∀ {j} → Wrap j → C
--test00f (wrap .{c {_}}) with anything
--test00f {.c} wrap | z = z

--test000 : ∀ {j} → Wrap j → C
--test000 wrap with anything
--test000 .{c {_}} wrap | z = z

test000a : ∀ {j} → Wrap j → C
test000a (wrap {c {x}}) with anything
test000a .{c {_}} wrap | z = z

--test000b : ∀ {j} → Wrap j → C
--test000b (wrap {c {_}}) with anything
--test000b .{c {_}} wrap | z = z

--test000c : ∀ {j} → Wrap j → C
--test000c (wrap {c}) with anything
--test000c .{c {_}} wrap | z = z

--test000d : ∀ {j} → Wrap j → C
--test000d (wrap {c {._}}) with anything
--test000d .{c {_}} wrap | z = z

--test000e : ∀ {j} → Wrap j → C
--test000e (wrap .{c}) with anything
--test000e .{c {_}} wrap | z = z

--test000f : ∀ {j} → Wrap j → C
--test000f (wrap .{c {_}}) with anything
--test000f .{c {_}} wrap | z = z

-- Test 1: first argument is dot pattern

test1a : ∀ {j} → Wrap j → C
test1a .{c} (wrap {c {x}}) with anything
test1a .{c} wrap | z = z

test1b : ∀ {j} → Wrap j → C
test1b .{c} (wrap {c {_}}) with anything
test1b .{c} wrap | z = z

test1c : ∀ {j} → Wrap j → C
test1c .{c} (wrap {c}) with anything
test1c .{c} wrap | z = z

test11a : ∀ {j} → Wrap j → C
test11a .{c} (wrap {c {x}}) with anything
test11a wrap | z = z

test11b : ∀ {j} → Wrap j → C
test11b .{c} (wrap {c {_}}) with anything
test11b wrap | z = z

test11c : ∀ {j} → Wrap j → C
test11c .{c} (wrap {c}) with anything
test11c wrap | z = z

test111a : ∀ {j} → Wrap j → C
test111a (wrap {c {x}}) with anything
test111a .{c} wrap | z = z

--test111b : ∀ {j} → Wrap j → C
--test111b (wrap {c {_}}) with anything
--test111b .{c} wrap | z = z

--test111c : ∀ {j} → Wrap j → C
--test111c (wrap {c}) with anything
--test111c .{c} wrap | z = z

-- Test 2: First argument is record pattern

test2a : ∀ {j} → Wrap j → C
test2a {c} wrap with anything
test2a {c} wrap | z = z

test2b : ∀ {j} → Wrap j → C
test2b {c} wrap with anything
test2b wrap | z = z

test2c : ∀ {j} → Wrap j → C
test2c {c} (wrap {c}) with anything
test2c {c} wrap | z = z

test2d : ∀ {j} → Wrap j → C
test2d {c} (wrap {c}) with anything
test2d wrap | z = z

test2e : ∀ {j} → Wrap j → C
test2e {c} (wrap {c {._}}) with anything
test2e {c} wrap | z = z

test2f : ∀ {j} → Wrap j → C
test2f {c} (wrap {c {._}}) with anything
test2f wrap | z = z

test2g : ∀ {j} → Wrap j → C
test2g {c} (wrap {c {x}}) with anything
test2g {c} wrap | z = z

test2h : ∀ {j} → Wrap j → C
test2h {c} (wrap {c {x}}) with anything
test2h wrap | z = z

test2i : ∀ {j} → Wrap j → C
test2i {c} (wrap {c {_}}) with anything
test2i {c} wrap | z = z

test2j : ∀ {j} → Wrap j → C
test2j {c} (wrap {c {_}}) with anything
test2j wrap | z = z

-- Test 3: First argument is record of dot pattern, second is record pattern
-- The commented-out ones fail due to issue 1608

-- test3a : ∀ {j} → Wrap j → C
-- test3a {c {._}} wrap with anything
-- test3a {c {._}} wrap | z = z

test3b : ∀ {j} → Wrap j → C
test3b {c {._}} wrap with anything
test3b wrap | z = z

-- test3c : ∀ {j} → Wrap j → C
-- test3c {c {._}} (wrap {c}) with anything
-- test3c {c {._}} wrap | z = z

test3d : ∀ {j} → Wrap j → C
test3d {c {._}} (wrap {c}) with anything
test3d wrap | z = z

-- test3e : ∀ {j} → Wrap j → C
-- test3e {c {._}} (wrap {c {._}}) with anything
-- test3e {c {._}} wrap | z = z

-- test3f : ∀ {j} → Wrap j → C
-- test3f {c {._}} (wrap {c {._}}) with anything
-- test3f wrap | z = z

test3g : ∀ {j} → Wrap j → C
test3g {c {._}} (wrap {c {x}}) with anything
test3g {c {._}} wrap | z = z

test3h : ∀ {j} → Wrap j → C
test3h {c {._}} (wrap {c {x}}) with anything
test3h wrap | z = z

-- test3i : ∀ {j} → Wrap j → C
-- test3i {c {._}} (wrap {c {_}}) with anything
-- test3i {c {._}} wrap | z = z

test3j : ∀ {j} → Wrap j → C
test3j {c {._}} (wrap {c {_}}) with anything
test3j wrap | z = z


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

open import Categories.Category using (Category; _[_,_]; _[_∘_]; _[_≈_])

-- Bundled versions of Idempotents, as well as maps between idempotents.
module Categories.Morphism.Idempotent.Bundles {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

import Categories.Morphism.Idempotent 𝒞 as Idem
open import Categories.Morphism.Reasoning 𝒞

private
  module 𝒞 = Category 𝒞
  open 𝒞.HomReasoning
  open 𝒞.Equiv

--------------------------------------------------------------------------------
-- Bundled Idempotents, and maps between them

record Idempotent : Set (o ⊔ ℓ ⊔ e) where
  field
    {obj} : 𝒞.Obj
    isIdempotent : Idem.Idempotent obj

  open Idem.Idempotent isIdempotent public

open Idempotent

record Idempotent⇒ (I J : Idempotent) : Set (ℓ ⊔ e) where
  private
    module I = Idempotent I
    module J = Idempotent J
  field
    hom     : 𝒞 [ I.obj , J.obj ]
    absorbˡ : 𝒞 [ 𝒞 [ J.idem ∘ hom ] ≈ hom ]
    absorbʳ : 𝒞 [ 𝒞 [ hom ∘ I.idem ] ≈ hom ]

open Idempotent⇒

--------------------------------------------------------------------------------
-- Identity and Composition of maps between Idempotents

id : ∀ {I} → Idempotent⇒ I I
id {I} = record
  { hom = idem I
  ; absorbˡ = idempotent I
  ; absorbʳ = idempotent I
  }

_∘_ : ∀ {I J K} → (f : Idempotent⇒ J K) → (g : Idempotent⇒ I J) → Idempotent⇒ I K
_∘_ {I} {J} {K} f g = record
  { hom = 𝒞 [ f.hom ∘ g.hom ]
  ; absorbˡ = pullˡ f.absorbˡ
  ; absorbʳ = pullʳ g.absorbʳ
  }
  where
    module f = Idempotent⇒ f
    module g = Idempotent⇒ g

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:
{-# OPTIONS --cubical --safe --no-import-sorts #-}
module Cubical.Algebra.Algebra.Base where

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

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Module    renaming (⟨_⟩ to ⟨_⟩m)
open import Cubical.Algebra.Ring      renaming (⟨_⟩ to ⟨_⟩r)
open import Cubical.Algebra.AbGroup   hiding (⟨_⟩)
open import Cubical.Algebra.Group     hiding (⟨_⟩)
open import Cubical.Algebra.Monoid       hiding (⟨_⟩)

open Iso

private
  variable
    ℓ : Level

record IsAlgebra (R : Ring {ℓ}) {A : Type ℓ}
                 (0a 1a : A) (_+_ _·_ : A → A → A) (-_ : A → A)
                 (_⋆_ : ⟨ R ⟩r → A → A) : Type ℓ where

  constructor isalgebra

  open Ring R using (1r) renaming (_+_ to _+r_; _·_ to _·r_)

  field
    isLeftModule : IsLeftModule R 0a _+_ -_ _⋆_
    ·-isMonoid  : IsMonoid 1a _·_
    dist        : (x y z : A) → (x · (y + z) ≡ (x · y) + (x · z))
                              × ((x + y) · z ≡ (x · z) + (y · z))
    ⋆-lassoc     : (r : ⟨ R ⟩r) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y)
    ⋆-rassoc     : (r : ⟨ R ⟩r) (x y : A) → r ⋆ (x · y) ≡ x · (r ⋆ y)

  open IsLeftModule isLeftModule public

  isRing : IsRing _ _ _ _ _
  isRing = isring (IsLeftModule.+-isAbGroup isLeftModule) ·-isMonoid dist
  open IsRing isRing public hiding (_-_; +-assoc; +-lid; +-linv; +-rid; +-rinv; +-comm)

record Algebra (R : Ring {ℓ}) : Type (ℓ-suc ℓ) where

  constructor algebra

  field
    Carrier        : Type ℓ
    0a             : Carrier
    1a             : Carrier
    _+_            : Carrier → Carrier → Carrier
    _·_            : Carrier → Carrier → Carrier
    -_             : Carrier → Carrier
    _⋆_            : ⟨ R ⟩r → Carrier → Carrier
    isAlgebra      : IsAlgebra R 0a 1a _+_ _·_ -_ _⋆_

  open IsAlgebra isAlgebra public

module commonExtractors {R : Ring {ℓ}} where
  ⟨_⟩ : Algebra R → Type ℓ
  ⟨_⟩ = Algebra.Carrier

  Algebra→Module : (A : Algebra R) → LeftModule R
  Algebra→Module (algebra A _ _ _ _ _ _ (isalgebra isLeftModule _ _ _ _)) =
    leftmodule A _ _ _ _ isLeftModule

  Algebra→Ring : (A : Algebra R) → Ring {ℓ}
  Algebra→Ring A = ring _ _ _ _ _ _ (IsAlgebra.isRing (Algebra.isAlgebra A))

  Algebra→AbGroup : (A : Algebra R) → AbGroup {ℓ}
  Algebra→AbGroup A = LeftModule→AbGroup (Algebra→Module A)

  Algebra→Monoid : (A : Algebra R) → Monoid {ℓ}
  Algebra→Monoid A = Ring→Monoid (Algebra→Ring A)

  isSetAlgebra : (A : Algebra R) → isSet ⟨ A ⟩
  isSetAlgebra A = isSetAbGroup (Algebra→AbGroup A)

  open Ring R using (1r; ·-ldist-+) renaming (_+_ to _+r_; _·_ to _·s_)

  makeIsAlgebra : {A : Type ℓ} {0a 1a : A}
                  {_+_ _·_ : A → A → A} { -_ : A → A} {_⋆_ : ⟨ R ⟩r → A → A}
                  (isSet-A : isSet A)
                  (+-assoc :  (x y z : A) → x + (y + z) ≡ (x + y) + z)
                  (+-rid : (x : A) → x + 0a ≡ x)
                  (+-rinv : (x : A) → x + (- x) ≡ 0a)
                  (+-comm : (x y : A) → x + y ≡ y + x)
                  (·-assoc :  (x y z : A) → x · (y · z) ≡ (x · y) · z)
                  (·-rid : (x : A) → x · 1a ≡ x)
                  (·-lid : (x : A) → 1a · x ≡ x)
                  (·-rdist-+ : (x y z : A) → x · (y + z) ≡ (x · y) + (x · z))
                  (·-ldist-+ : (x y z : A) → (x + y) · z ≡ (x · z) + (y · z))
                  (⋆-assoc : (r s : ⟨ R ⟩r) (x : A) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
                  (⋆-ldist : (r s : ⟨ R ⟩r) (x : A) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
                  (⋆-rdist : (r : ⟨ R ⟩r) (x y : A) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
                  (⋆-lid   : (x : A) → 1r ⋆ x ≡ x)
                  (⋆-lassoc : (r : ⟨ R ⟩r) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y))
                  (⋆-rassoc : (r : ⟨ R ⟩r) (x y : A) → r ⋆ (x · y) ≡ x · (r ⋆ y))
                → IsAlgebra R 0a 1a _+_ _·_ -_ _⋆_
  makeIsAlgebra isSet-A
                +-assoc +-rid +-rinv +-comm
                ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+
                ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid ⋆-lassoc ⋆-rassoc =
                isalgebra
                  (makeIsLeftModule isSet-A
                                    +-assoc +-rid +-rinv +-comm
                                    ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid)
                  (makeIsMonoid isSet-A ·-assoc ·-rid ·-lid)
                  (λ x y z → ·-rdist-+ x y z , ·-ldist-+ x y z)
                  ⋆-lassoc ⋆-rassoc

open commonExtractors public

record AlgebraEquiv {R : Ring {ℓ}} (A B : Algebra R) : Type ℓ where

  constructor algebraiso

  instance
    _ : Algebra R
    _ = A
    _ : Algebra R
    _ = B

  open Algebra {{...}}

  field
    e      : ⟨ A ⟩ ≃ ⟨ B ⟩
    isHom+ : (x y : ⟨ A ⟩) → equivFun e (x + y) ≡ equivFun e x + equivFun e y
    isHom· : (x y : ⟨ A ⟩) → equivFun e (x · y) ≡ equivFun e x · equivFun e y
    pres1  : equivFun e 1a ≡ 1a
    comm⋆  : (r : ⟨ R ⟩r) (x : ⟨ A ⟩) → equivFun e (r ⋆ x) ≡ r ⋆ equivFun e x

record AlgebraHom {R : Ring {ℓ}} (A B : Algebra R) : Type ℓ where

  constructor algebrahom

  private
    instance
      _ : Algebra R
      _ = A
      _ : Algebra R
      _ = B

  open Algebra {{...}}

  field
    f      : ⟨ A ⟩ → ⟨ B ⟩
    isHom+ : (x y : ⟨ A ⟩) → f (x + y) ≡ f x + f y
    isHom· : (x y : ⟨ A ⟩) → f (x · y) ≡ f x · f y
    pres1  : f 1a ≡ 1a
    comm⋆  : (r : ⟨ R ⟩r) (x : ⟨ A ⟩) → f (r ⋆ x) ≡ r ⋆ f x

  pres0 : f 0a ≡ 0a
  pres0 = sym (Theory.+-idempotency→0 (Algebra→Ring B) (f 0a)
          (f 0a        ≡⟨ cong f (sym (+-rid _)) ⟩
           f (0a + 0a) ≡⟨ isHom+ _ _ ⟩
           f 0a + f 0a ∎))

  isHom- : (x : ⟨ A ⟩) → f (- x) ≡ - f x
  isHom- x = Theory.implicitInverse (Algebra→Ring B) (f x) (f (- x))
             (f (x) + f (- x)  ≡⟨ sym (isHom+ _ _) ⟩
             f (x - x)         ≡⟨ cong f (+-rinv _) ⟩
             f 0a              ≡⟨ pres0 ⟩
             0a ∎)

_$a_ : {R : Ring {ℓ}} {A B : Algebra R}
       → AlgebraHom A B
       → ⟨ A ⟩ → ⟨ B ⟩
f $a x = AlgebraHom.f f x

_∘a_ : {R : Ring {ℓ}} {A B C : Algebra R}
       → AlgebraHom B C → AlgebraHom A B → AlgebraHom A C
_∘a_ {ℓ} {R} {A} {B} {C}
  (algebrahom f isHom+f isHom·f pres1f comm⋆f)
  (algebrahom g isHom+g isHom·g pres1g comm⋆g)
  =
  let
    open Algebra ⦃...⦄
    instance
      _ : Algebra R
      _ = A
      _ : Algebra R
      _ = B
      _ : Algebra R
      _ = C
  in algebrahom (f ∘ g)
    (λ x y → f (g (x + y))      ≡⟨ cong f (isHom+g x y) ⟩
             f (g x + g y)      ≡⟨ isHom+f _ _  ⟩
             f (g x) + f (g y)  ∎)
    (λ x y → f (g (x · y))      ≡⟨ cong f (isHom·g x y) ⟩
             f (g x · g y)      ≡⟨ isHom·f _ _  ⟩
             f (g x) · f (g y)  ∎)
    (f (g 1a) ≡⟨ cong f pres1g ⟩ f 1a ≡⟨ pres1f ⟩ 1a ∎)
    λ r x → f (g (r ⋆ x))  ≡⟨ cong f (comm⋆g _ _) ⟩
            f (r ⋆ (g x))  ≡⟨ comm⋆f _ _ ⟩
            r ⋆ (f (g x))  ∎

module AlgebraΣTheory (R : Ring {ℓ}) where

  RawAlgebraStructure = λ (A : Type ℓ) → (A → A → A) × (A → A → A) × A × (⟨ R ⟩r → A → A)

  RawAlgebraEquivStr = AutoEquivStr RawAlgebraStructure

  rawAlgebraUnivalentStr : UnivalentStr _ RawAlgebraEquivStr
  rawAlgebraUnivalentStr = autoUnivalentStr RawAlgebraStructure

  open Ring R using (1r) renaming (_+_ to _+r_; _·_ to _·r_)
  open RingΣTheory
  open LeftModuleΣTheory R
  open MonoidΣTheory

  AlgebraAxioms : (A : Type ℓ) (str : RawAlgebraStructure A) → Type ℓ
  AlgebraAxioms A (_+_ , _·_ , 1a , _⋆_) =
               LeftModuleAxioms A (_+_ , _⋆_)
               × (MonoidAxioms A (1a , _·_))
               × ((x y z : A) → (x · (y + z) ≡ (x · y) + (x · z))
                              × ((x + y) · z ≡ (x · z) + (y · z)))
               × ((r : ⟨ R ⟩r) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y))
               × ((r : ⟨ R ⟩r) (x y : A) → r ⋆ (x · y) ≡ x · (r ⋆ y))

  AlgebraStructure : Type ℓ → Type ℓ
  AlgebraStructure = AxiomsStructure RawAlgebraStructure AlgebraAxioms

  AlgebraΣ : Type (ℓ-suc ℓ)
  AlgebraΣ = TypeWithStr ℓ AlgebraStructure

  AlgebraEquivStr : StrEquiv AlgebraStructure ℓ
  AlgebraEquivStr = AxiomsEquivStr RawAlgebraEquivStr AlgebraAxioms

  isSetAlgebraΣ : (A : AlgebraΣ) → isSet _
  isSetAlgebraΣ (A , _ , (isLeftModule , _ , _) ) = isSetLeftModuleΣ (A , _ , isLeftModule)

  isPropAlgebraAxioms : (A : Type ℓ) (s : RawAlgebraStructure A)
                             → isProp (AlgebraAxioms A s)
  isPropAlgebraAxioms A (_+_ , _·_ , 1a , _⋆_) =
    isPropΣ (isPropLeftModuleAxioms A (_+_ , _⋆_))
    (λ isLeftModule →
     isProp× (isPropMonoidAxioms A (1a , _·_))
    (isProp× (isPropΠ3 (λ _ _ _ → isProp× ((isSetLeftModuleΣ (A , _ , isLeftModule)) _ _)
                                          ((isSetLeftModuleΣ (A , _ , isLeftModule)) _ _)))
    (isProp× (isPropΠ3 (λ _ _ _ → (isSetLeftModuleΣ (A , _ , isLeftModule)) _ _))
             (isPropΠ3 (λ _ _ _ → (isSetLeftModuleΣ (A , _ , isLeftModule)) _ _)))))

  Algebra→AlgebraΣ : Algebra R → AlgebraΣ
  Algebra→AlgebraΣ (algebra A 0a 1a _+_ _·_ -_ _⋆_
                            (isalgebra isLeftModule isMonoid dist ⋆-lassoc ⋆-rassoc)) =
    A , (_+_ , _·_ , 1a , _⋆_) ,
    (LeftModule→LeftModuleΣ (leftmodule A _ _ _ _ isLeftModule) .snd .snd) ,
    Monoid→MonoidΣ (monoid A _ _ isMonoid) .snd .snd ,
    dist ,
    ⋆-lassoc ,
    ⋆-rassoc

  AlgebraΣ→Algebra : AlgebraΣ → Algebra R
  AlgebraΣ→Algebra (A , (_+_ , _·_ , 1a , _⋆_) , isLeftModule , isMonoid , dist , lassoc , rassoc) =
    algebra A _ 1a _+_ _·_ _ _⋆_
    (isalgebra (LeftModule.isLeftModule (LeftModuleΣ→LeftModule (A , (_ , isLeftModule))))
               (Monoid.isMonoid (MonoidΣ→Monoid (A , (_ , isMonoid))))
               dist lassoc rassoc)

  AlgebraIsoAlgebraΣ : Iso (Algebra R) AlgebraΣ
  AlgebraIsoAlgebraΣ = iso Algebra→AlgebraΣ AlgebraΣ→Algebra (λ _ → refl) helper
    where
      -- helper will be refl, if eta-equality is activated for all structure-records
      open MonoidΣTheory
      monoid-helper : retract (Monoid→MonoidΣ {ℓ}) MonoidΣ→Monoid
      monoid-helper = Iso.leftInv MonoidIsoMonoidΣ
      module-helper : retract (LeftModule→LeftModuleΣ) LeftModuleΣ→LeftModule
      module-helper = Iso.leftInv LeftModuleIsoLeftModuleΣ

      open Algebra
      helper : _
      Carrier (helper a i) = Carrier a
      0a (helper a i) = 0a a
      1a (helper a i) = 1a a
      _+_ (helper a i) = _+_ a
      _·_ (helper a i) = _·_ a
      -_ (helper a i) = -_ a
      _⋆_ (helper a i) = _⋆_ a
      IsAlgebra.isLeftModule (isAlgebra (helper a i)) =
        LeftModule.isLeftModule (module-helper
        (leftmodule _ _ _ _ _ (isLeftModule a)) i)
      IsAlgebra.·-isMonoid (isAlgebra (helper a i)) =
        Monoid.isMonoid (monoid-helper (monoid _ _ _ (·-isMonoid a)) i)
      IsAlgebra.dist (isAlgebra (helper a i)) = dist a
      IsAlgebra.⋆-lassoc (isAlgebra (helper a i)) = ⋆-lassoc a
      IsAlgebra.⋆-rassoc (isAlgebra (helper a i)) = ⋆-rassoc a

  algebraUnivalentStr : UnivalentStr AlgebraStructure AlgebraEquivStr
  algebraUnivalentStr = axiomsUnivalentStr _ isPropAlgebraAxioms rawAlgebraUnivalentStr

  AlgebraΣPath : (M N : AlgebraΣ) → (M ≃[ AlgebraEquivStr ] N) ≃ (M ≡ N)
  AlgebraΣPath = SIP algebraUnivalentStr

  AlgebraEquivΣ : (M N : Algebra R) → Type ℓ
  AlgebraEquivΣ M N = Algebra→AlgebraΣ M ≃[ AlgebraEquivStr ] Algebra→AlgebraΣ N

  AlgebraEquivΣPath : {M N : Algebra R} → Iso (AlgebraEquiv M N) (AlgebraEquivΣ M N)
  fun AlgebraEquivΣPath (algebraiso e isHom+ isHom· pres1 comm⋆) =
    e , isHom+ , (isHom· , (pres1 , comm⋆))
  inv AlgebraEquivΣPath (f , isHom+ , isHom· , pres1 , comm⋆) =
    algebraiso f isHom+ isHom· pres1 comm⋆
  rightInv AlgebraEquivΣPath _ = refl
  leftInv AlgebraEquivΣPath _ = refl

  AlgebraPath : (M N : Algebra R) → (AlgebraEquiv M N) ≃ (M ≡ N)
  AlgebraPath M N =
    AlgebraEquiv M N                                    ≃⟨ isoToEquiv AlgebraEquivΣPath ⟩
    AlgebraEquivΣ M N                                   ≃⟨ AlgebraΣPath _ _ ⟩
    Algebra→AlgebraΣ M ≡ Algebra→AlgebraΣ N             ≃⟨ isoToEquiv
                                                             (invIso
                                                             (congIso
                                                             AlgebraIsoAlgebraΣ))
                                                           ⟩
    M ≡ N ■

AlgebraPath : {R : Ring {ℓ}} (M N : Algebra R) → (AlgebraEquiv M N) ≃ (M ≡ N)
AlgebraPath {ℓ} {R} = AlgebraΣTheory.AlgebraPath R

module AlgebraTheory (R : Ring {ℓ}) (A : Algebra R) where
  open Ring R renaming (_+_ to _+r_)
  open Algebra A

  0-actsNullifying : (x : ⟨ A ⟩) → 0r ⋆ x ≡ 0a
  0-actsNullifying x =
    let idempotent-+ = 0r ⋆ x              ≡⟨ cong (λ u → u ⋆ x) (sym (Theory.0-idempotent R)) ⟩
                       (0r +r 0r) ⋆ x      ≡⟨ ⋆-ldist 0r 0r x ⟩
                       (0r ⋆ x) + (0r ⋆ x) ∎
    in sym (Theory.+-idempotency→0 (Algebra→Ring A) (0r ⋆ x) idempotent-+)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
-- Andreas, 2016-10-03, re issue #2231
-- Termination checking a corecursive definition in abstract mode.

{-# OPTIONS --guardedness #-}

infix 1000 ♯_

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

abstract
  data Functor : Set where
    Id : Functor

  _·_ : Functor → Set → Set
  Id · A = A

  data ν (F : Functor) : Set where
    inn : ∞ (F · ν F) → ν F

  -- Evaluation is required to see that Id · ν Id is a coinductive type.

  foo : ∀ F → F · ν F
  foo Id = inn (♯ foo Id)

-- The termination checker needs to treat the generated #-foo function
-- in abstract mode, to have constructor Id in scope.

max_stars_repo_name: caryoscelus/agda

max_issues_repo_name: caryoscelus/agda

max_forks_repo_name: caryoscelus/agda


text:
module _ (A : Set) where

open import Common.Prelude
open import Common.Reflection

macro
  foo : Tactic
  foo _ = returnTC _

bar : ⊤
bar = foo


text:
------------------------------------------------------------------------
-- Some results related to CCS, implemented without using a fixed form
-- of bisimilarity
------------------------------------------------------------------------

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

open import Prelude

module Bisimilarity.CCS.General {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import List equality-with-J
open import Prelude.Size

open import Labelled-transition-system
open import Labelled-transition-system.CCS Name

------------------------------------------------------------------------
-- Exercise 6.1.3 (1) from "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi

6-1-3-1-proc : Proc ∞ → Proc ∞ → ℕ → Proc ∞
6-1-3-1-proc P P′ zero    = ! P ∣ P′
6-1-3-1-proc P P′ (suc n) = 6-1-3-1-proc P P′ n ∣ P

-- Note that the form of the expression is a bit more restrictive
-- than in the exercise formulation: (((! P | P′) | P)…) ∣ P.

6-1-3-1-without-τ :
  ∀ {a P P₀} → let μ = name a in
  ! P [ μ ]⟶ P₀ →
  ∃ λ P′ → ∃ λ n →
    P [ μ ]⟶ P′ × P₀ ≡ 6-1-3-1-proc P P′ n
6-1-3-1-without-τ {a} {P} (replication (par-right {Q′ = P′} tr)) =
    P′ , 0
  , (P   [ name a ]⟶⟨ tr ⟩
     P′)
  , (! P ∣ P′             ≡⟨ refl ⟩∎
     6-1-3-1-proc P P′ 0  ∎)
6-1-3-1-without-τ {a} {P} (replication (par-left {P′ = P′} tr)) =
  let P″ , n , tr′ , eq = 6-1-3-1-without-τ tr in

    P″ , suc n
  , (P   [ name a ]⟶⟨ tr′ ⟩
     P″)
  , (P′                  ∣ P    ≡⟨ cong (_∣ _) eq ⟩
     6-1-3-1-proc P P″ n ∣ P    ≡⟨ refl ⟩∎
     6-1-3-1-proc P P″ (suc n)  ∎)

One-step-away : {A : Type ℓ} → (A → Action) → Proc ∞ → Type ℓ
One-step-away f P = ∃ λ a → ∃ λ P′ → P [ f a ]⟶ P′

cons : {A B : Type ℓ} → A → List A × B → List A × B
cons x (xs , y) = x ∷ xs , y

6-1-3-1-proc′ :
  (P : Proc ∞) →
  List (Maybe (One-step-away name P)) × One-step-away id P →
  Proc ∞
6-1-3-1-proc′ P ([] , (_ , P′ , _))          = ! P ∣ P′
6-1-3-1-proc′ P (just (_ , P′ , _) ∷ Ps , o) = 6-1-3-1-proc′ P (Ps , o) ∣ P′
6-1-3-1-proc′ P (nothing           ∷ Ps , o) = 6-1-3-1-proc′ P (Ps , o) ∣ P

6-1-3-1-with-τ :
  ∀ {μ P P₀} →
  ! P [ μ ]⟶ P₀ →
  ∃ λ Ps → P₀ ≡ 6-1-3-1-proc′ P Ps
6-1-3-1-with-τ {μ} {P} (replication (par-right {Q′ = P′} tr)) =
    Ps
  , (! P ∣ P′            ≡⟨ refl ⟩∎
     6-1-3-1-proc′ P Ps  ∎)
  where
  Ps = [] , (μ , P′ , tr)

6-1-3-1-with-τ {μ} {P} (replication (par-left {P′ = P′} tr)) =
  let Ps , eq = 6-1-3-1-with-τ tr
      Ps′     = cons nothing Ps
  in
    Ps′
  , (P′ ∣ P                  ≡⟨ cong (_∣ _) eq ⟩
     6-1-3-1-proc′ P Ps ∣ P  ≡⟨ refl ⟩∎
     6-1-3-1-proc′ P Ps′     ∎)

6-1-3-1-with-τ .{τ} {P}
               (replication (par-τ {P′ = P′} {Q′ = Q′} {a = a}
                                   tr₁ tr₂)) =
  let Ps , eq = 6-1-3-1-with-τ tr₁
      Ps′     = cons (just (co a , Q′ , tr₂)) Ps
  in
    Ps′
  , (P′ ∣ Q′                  ≡⟨ cong (_∣ _) eq ⟩
     6-1-3-1-proc′ P Ps ∣ Q′  ≡⟨ refl ⟩∎
     6-1-3-1-proc′ P Ps′      ∎)

------------------------------------------------------------------------
-- Exercise 6.1.3 (2) from "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi

-- Assumptions used to state and solve the exercise.

record 6-1-3-2-assumptions ℓ′ : Type (ℓ ⊔ lsuc ℓ′) where
  infix 4 _∼_
  infix  -1 finally-∼
  infixr -2 step-∼
  syntax finally-∼ p q p∼q = p ∼⟨ p∼q ⟩∎ q ∎
  syntax step-∼ p q∼r p∼q  = p ∼⟨ p∼q ⟩ q∼r

  field
    _∼_       : Proc ∞ → Proc ∞ → Type ℓ′
    step-∼    : ∀ P {Q R} → Q ∼ R → P ∼ Q → P ∼ R
    finally-∼ : ∀ P Q → P ∼ Q → P ∼ Q
    reflexive : ∀ {P} → P ∼ P
    symmetric : ∀ {P Q} → P ∼ Q → Q ∼ P
    ∣-comm    : ∀ {P Q} → P ∣ Q ∼ Q ∣ P
    ∣-assoc   : ∀ {P Q R} → P ∣ (Q ∣ R) ∼ (P ∣ Q) ∣ R
    _∣-cong_  : ∀ {P P′ Q Q′} → P ∼ P′ → Q ∼ Q′ → P ∣ Q ∼ P′ ∣ Q′
    6-1-2     : ∀ {P} → ! P ∣ P ∼ ! P

module 6-1-3-2 {ℓ′} (assumptions : 6-1-3-2-assumptions ℓ′) where

  open 6-1-3-2-assumptions assumptions

  swap-rightmost : ∀ {P Q R} → (P ∣ Q) ∣ R ∼ (P ∣ R) ∣ Q
  swap-rightmost {P} {Q} {R} =
    (P ∣ Q) ∣ R  ∼⟨ symmetric ∣-assoc ⟩
    P ∣ (Q ∣ R)  ∼⟨ reflexive ∣-cong ∣-comm ⟩
    P ∣ (R ∣ Q)  ∼⟨ ∣-assoc ⟩∎
    (P ∣ R) ∣ Q  ∎

  6-1-3-2 :
    ∀ {μ P P₀} →
    ! P [ μ ]⟶ P₀ →
    (∃ λ P′ → P [ μ ]⟶ P′ × P₀ ∼ ! P ∣ P′)
      ⊎
    (μ ≡ τ × ∃ λ P′ → ∃ λ P″ → ∃ λ a →
     P [ name a ]⟶ P′ × P [ name (co a) ]⟶ P″ × P₀ ∼ (! P ∣ P′) ∣ P″)
  6-1-3-2 {μ} {P} (replication (par-right {Q′ = P′} P⟶P′)) =
    inj₁ ( _
         , (P   [ μ ]⟶⟨ P⟶P′ ⟩
            P′)
         , (! P ∣ P′  ∼⟨ reflexive ⟩∎
            ! P ∣ P′  ∎))
  6-1-3-2 {μ} {P} (replication (par-left {P′ = P′} tr)) with 6-1-3-2 tr
  ... | inj₁ (P″ , P⟶P″ , P′∼!P∣P″) =
    inj₁ ( _
         , (P   [ μ ]⟶⟨ P⟶P″ ⟩
            P″)
         , (P′  ∣ P         ∼⟨ P′∼!P∣P″ ∣-cong reflexive ⟩
            (! P ∣ P″) ∣ P  ∼⟨ swap-rightmost ⟩
            (! P ∣ P) ∣ P″  ∼⟨ 6-1-2 ∣-cong reflexive ⟩∎
            ! P ∣ P″        ∎))
  ... | inj₂ (μ≡τ , P″ , P‴ , a , P⟶P″ , P⟶P‴ , P′∼!P∣P″∣P‴) =
    inj₂ ( μ≡τ , _ , _ , _
         , (P   [ name a ]⟶⟨ P⟶P″ ⟩
            P″)
         , (P   [ name (co a) ]⟶⟨ P⟶P‴ ⟩
            P‴)
         , (P′ ∣ P                 ∼⟨ P′∼!P∣P″∣P‴ ∣-cong reflexive ⟩
            ((! P ∣ P″) ∣ P‴) ∣ P  ∼⟨ swap-rightmost ⟩
            ((! P ∣ P″) ∣ P) ∣ P‴  ∼⟨ swap-rightmost ∣-cong reflexive ⟩
            ((! P ∣ P) ∣ P″) ∣ P‴  ∼⟨ (6-1-2 ∣-cong reflexive) ∣-cong reflexive ⟩∎
            (! P ∣ P″) ∣ P‴        ∎))
  6-1-3-2 {P = P} (replication (par-τ {P′ = P′} {Q′ = Q′} {a = a}
                                      tr P⟶Q′)) with 6-1-3-2 tr
  ... | inj₁ (P″ , P⟶P″ , P′∼!P∣P″) =
    inj₂ ( refl , _ , _ , _
         , (P   [ name a ]⟶⟨ P⟶P″ ⟩
            P″)
         , (P   [ name (co a) ]⟶⟨ P⟶Q′ ⟩
            Q′)
         , (P′ ∣ Q′          ∼⟨ P′∼!P∣P″ ∣-cong reflexive ⟩∎
            (! P ∣ P″) ∣ Q′  ∎))
  ... | inj₂ (() , _)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
record R : Set₁
 where
  field
    _f_ : Set → Set

postulate A : Set

I₁ : R
I₁ R.f x = A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text: module A.B.M where


text:
module SetClash where

postulate x : Set

y : Set1
y = x

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
------------------------------------------------------------------------------
-- Equivalent approaches for implement the inductive predicate N
------------------------------------------------------------------------------

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

module FOTC.EquivalenceInductivePredicateN where

open import FOTC.Base

------------------------------------------------------------------------------
-- Using succ : D instead of succ₁ : D → D.

module Constant where

  module LFP where

    NatF : (D → Set) → D → Set
    NatF A n = n ≡ zero ∨ (∃[ n' ] n ≡ succ · n' ∧ A n')

    postulate
      N         : D → Set
      N-in-ho   : ∀ {n} → NatF N n → N n
      N-ind'-ho : (A : D → Set) → (∀ {n} → NatF A n → A n) → ∀ {n} → N n → A n

    N-in : ∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ · n' ∧ N n') → N n
    N-in = N-in-ho

    N-ind' : (A : D → Set) →
             (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ · n' ∧ A n') → A n) →
             ∀ {n} → N n → A n
    N-ind' = N-ind'-ho

    --------------------------------------------------------------------------
    -- The data constructors of N using LFP.

    nzero : N zero
    nzero = N-in (inj₁ refl)

    nsucc : ∀ {n} → N n → N (succ · n)
    nsucc Nn = N-in (inj₂ (_ , refl , Nn))

    --------------------------------------------------------------------------
    -- The induction principle of N using LFP.
    N-ind : (A : D → Set) →
            A zero →
            (∀ {n} → A n → A (succ · n)) →
            ∀ {n} → N n → A n
    N-ind A A0 h = N-ind' A h'
      where
      h' : ∀ {m} → m ≡ zero ∨ (∃[ m' ] m ≡ succ · m' ∧ A m') → A m
      h' (inj₁ m≡0)              = subst A (sym m≡0) A0
      h' (inj₂ (m' , prf , Am')) = subst A (sym prf) (h Am')

  ----------------------------------------------------------------------------
  module Data where

    data N : D → Set where
      nzero : N zero
      nsucc : ∀ {n} → N n → N (succ · n)

    N-ind : (A : D → Set) →
            A zero →
            (∀ {n} → A n → A (succ · n)) →
            ∀ {n} → N n → A n
    N-ind A A0 h nzero      = A0
    N-ind A A0 h (nsucc Nn) = h (N-ind A A0 h Nn)

    --------------------------------------------------------------------------
    -- The introduction rule of N using data.
    N-in : ∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ · n' ∧ N n') → N n
    N-in {n} h = case prf₁ prf₂ h
      where
      prf₁ : n ≡ zero → N n
      prf₁ n≡0 = subst N (sym n≡0) nzero

      prf₂ : ∃[ n' ] n ≡ succ · n' ∧ N n' → N n
      prf₂ (n' , prf , Nn') = subst N (sym prf) (nsucc Nn')

    --------------------------------------------------------------------------
    -- The induction principle for N using data.
    N-ind' :
      (A : D → Set) →
      (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ · n' ∧ A n') → A n) →
      ∀ {n} → N n → A n
    N-ind' A h = N-ind A h₁ h₂
      where
      h₁ :  A zero
      h₁ = h (inj₁ refl)

      h₂ : ∀ {m} → A m → A (succ · m)
      h₂ {m} Am = h (inj₂ (m , refl , Am))

------------------------------------------------------------------------------
-- Using succ₁ : D → D instead of succ : D.

module UnaryFunction where

  module LFP where

    NatF : (D → Set) → D → Set
    NatF A n = n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')

    postulate
      N         : D → Set
      N-in-ho   : ∀ {n} → NatF N n → N n
      N-ind'-ho : (A : D → Set) → (∀ {n} → NatF A n → A n) → ∀ {n} → N n → A n

    N-in : ∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n') → N n
    N-in = N-in-ho

    N-ind' : (A : D → Set) →
             (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n') → A n) →
             ∀ {n} → N n → A n
    N-ind' = N-ind'-ho

    --------------------------------------------------------------------------
    -- The data constructors of N using LFP.

    nzero : N zero
    nzero = N-in (inj₁ refl)

    nsucc : ∀ {n} → N n → N (succ₁ n)
    nsucc Nn = N-in (inj₂ (_ , refl , Nn))

    --------------------------------------------------------------------------
    -- The induction principle of N using LFP.
    N-ind : (A : D → Set) →
            A zero →
            (∀ {n} → A n → A (succ₁ n)) →
            ∀ {n} → N n → A n
    N-ind A A0 h = N-ind' A h'
      where
      h' : ∀ {m} → m ≡ zero ∨ (∃[ m' ] m ≡ succ₁ m' ∧ A m') → A m
      h' (inj₁ m≡0)              = subst A (sym m≡0) A0
      h' (inj₂ (m' , prf , Am')) = subst A (sym prf) (h Am')

  ----------------------------------------------------------------------------
  module Data where

    data N : D → Set where
      nzero : N zero
      nsucc : ∀ {n} → N n → N (succ₁ n)

    N-ind : (A : D → Set) →
            A zero →
            (∀ {n} → A n → A (succ₁ n)) →
            ∀ {n} → N n → A n
    N-ind A A0 h nzero      = A0
    N-ind A A0 h (nsucc Nn) = h (N-ind A A0 h Nn)

    --------------------------------------------------------------------------
    -- The introduction rule of N using data.
    N-in : ∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n') → N n
    N-in {n} h = case prf₁ prf₂ h
      where
      prf₁ : n ≡ zero → N n
      prf₁ n≡0 = subst N (sym n≡0) nzero

      prf₂ : ∃[ n' ] n ≡ succ₁ n' ∧ N n' → N n
      prf₂ (n' , prf , Nn') = subst N (sym prf) (nsucc Nn')

    --------------------------------------------------------------------------
    -- The induction principle for N using data.
    N-ind' :
      (A : D → Set) →
      (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n') → A n) →
      ∀ {n} → N n → A n
    N-ind' A h = N-ind A h₁ h₂
      where
      h₁ :  A zero
      h₁ = h (inj₁ refl)

      h₂ : ∀ {m} → A m → A (succ₁ m)
      h₂ {m} Am = h (inj₂ (m , refl , Am))

module EsikProposition2Dot1 where

  postulate
    N : D → Set

    N-ind' : (A : D → Set) →
             (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n') → A n) →
             ∀ {n} → N n → A n

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
postulate
  F : Set → Set

{-# POLARITY F * #-}

data D : Set where
  d : F D → D


text:
module Where where

-- all these examples should not termination check

f : forall {A : Set} -> A
f {A} = g
      where g : A
            g = f

f1 : forall {A : Set} -> A -> A
f1 {A} a = g a
      where g : A -> A
            g a = f1 a

f2 : forall {A : Set} -> A -> A
f2 {A} a = g a
      where g : A -> A
            g = f2

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Cats.Util.Function where

open import Relation.Binary using (Rel ; IsEquivalence ; _Preserves₂_⟶_⟶_)
open import Relation.Binary.PropositionalEquality as ≡

open import Function as Fun public using (id ; _on_)
open import Relation.Binary.Construct.On public
  renaming (isEquivalence to on-isEquivalence)

infixr 9 _∘_

_∘_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (B → C) → (A → B) → A → C
f ∘ g = f Fun.∘ g

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:
{- Name: Bowornmet (Ben) Hudson

-- define the complexity language from the paper

-}

open import Preliminaries
open import Preorder-withmax

module Comp-lang where

  -- define the complexity language from the paper
  -- we want to focus on arrow, cross, and nat types
  -- do I need unit types?
  data CTp : Set where
    unit : CTp
    nat : CTp
    _->c_ : CTp → CTp → CTp
    _×c_ : CTp → CTp → CTp
    C : CTp

  -- represent a context as a list of types
  Ctx = List CTp

  -- de Bruijn indices (for free variables)
  data _∈_ : CTp → Ctx → Set where
    i0 : ∀ {Γ τ}
       → τ ∈ (τ :: Γ)
    iS : ∀ {Γ τ τ1}
       → τ ∈ Γ
       → τ ∈ (τ1 :: Γ)

  data _|-_ : Ctx → CTp → Set where
    unit : ∀ {Γ}
         → Γ |- unit
    0C : ∀ {Γ}
       → Γ |- C
    1C : ∀ {Γ}
       → Γ |- C
    plusC : ∀ {Γ}
         → Γ |- C
         → Γ |- C
         → Γ |- C
    var : ∀ {Γ τ}
        → τ ∈ Γ
        → Γ |- τ
    z : ∀ {Γ}
      → Γ |- nat
    suc : ∀ {Γ}
        → (e : Γ |- nat)
        → Γ |- nat
    rec : ∀ {Γ τ}
        → Γ |- nat
        → Γ |- τ
        → (nat :: (τ :: Γ)) |- τ
        → Γ |- τ
    lam : ∀ {Γ τ ρ}
        → (ρ :: Γ) |- τ
        → Γ |- (ρ ->c τ)
    app : ∀ {Γ τ1 τ2}
        → Γ |- (τ2 ->c τ1)
        → Γ |- τ2
        → Γ |- τ1
    prod : ∀ {Γ τ1 τ2}
         → Γ |- τ1
         → Γ |- τ2
         → Γ |- (τ1 ×c τ2)
    l-proj : ∀ {Γ τ1 τ2}
           → Γ |- (τ1 ×c τ2)
           → Γ |- τ1
    r-proj : ∀ {Γ τ1 τ2}
           → Γ |- (τ1 ×c τ2)
           → Γ |- τ2

  _+C_ : ∀ {Γ τ} → Γ |- C  → Γ |- (C ×c τ)→ Γ |- (C ×c τ)
  c +C e = prod (plusC c (l-proj e)) (r-proj e)

------weakening and substitution lemmas

 -- renaming function
  rctx : Ctx → Ctx → Set
  rctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → τ ∈ Γ

  -- re: transferring variables in contexts
  lem1 : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) (τ :: Γ')
  lem1 d i0 = i0
  lem1 d (iS x) = iS (d x)

  -- renaming lemma
  ren : ∀ {Γ Γ' τ} → Γ' |- τ → rctx Γ Γ' → Γ |- τ
  ren unit d = unit
  ren 0C d = 0C
  ren 1C d = 1C
  ren (plusC e1 e2) d = plusC (ren e1 d) (ren e2 d)
  ren (var x) d = var (d x)
  ren z d = z
  ren (suc e) d = suc (ren e d)
  ren (rec e e0 e1) d = rec (ren e d) (ren e0 d) (ren e1 (lem1 (lem1 d)))
  ren (lam e) d = lam (ren e (lem1 d))
  ren (app e1 e2) d = app (ren e1 d) (ren e2 d)
  ren (prod e1 e2) d = prod (ren e1 d) (ren e2 d)
  ren (l-proj e) d = l-proj (ren e d)
  ren (r-proj e) d = r-proj (ren e d)

  -- substitution
  sctx : Ctx → Ctx → Set
  sctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → Γ |- τ

  -- weakening a context
  wkn : ∀ {Γ τ1 τ2} → Γ |- τ2 → (τ1 :: Γ) |- τ2
  wkn e = ren e iS

  -- weakening also works with substitution
  wkn-s : ∀ {Γ τ1 Γ'} → sctx Γ Γ' → sctx (τ1 :: Γ) Γ'
  wkn-s d = λ f → wkn (d f)

  wkn-r : ∀ {Γ τ1 Γ'} → rctx Γ Γ' → rctx (τ1 :: Γ) Γ'
  wkn-r d = λ x → iS (d x)

  -- lem2 (need a lemma for subst like we did for renaming)
  lem2 : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) (τ :: Γ')
  lem2 d i0 = var i0
  lem2 d (iS i) = wkn (d i)

  -- another substitution lemma
  lem3 : ∀ {Γ τ} → Γ |- τ → sctx Γ (τ :: Γ)
  lem3 e i0 = e
  lem3 e (iS i) = var i

  lem3' : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ |- τ → sctx Γ (τ :: Γ')
  lem3' Θ e i0 = e
  lem3' Θ e (iS i) = Θ i

  -- one final lemma needed for the last stepping rule. Thank you Professor Licata!
  lem4 : ∀ {Γ τ1 τ2} → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ))
  lem4 e1 e2 i0 = e1
  lem4 e1 e2 (iS i0) = e2
  lem4 e1 e2 (iS (iS i)) = var i

  lem4' : ∀ {Γ Γ' τ1 τ2} → sctx Γ Γ' → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ'))
  lem4' Θ a b i0 = a
  lem4' Θ a b (iS i0) = b
  lem4' Θ a b (iS (iS i)) = Θ i

  -- the 'real' substitution lemma (if (x : τ') :: Γ |- (e : τ) and Γ |- (e : τ') , then Γ |- e[x -> e'] : τ)
  subst : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ' |- τ → Γ |- τ
  subst d unit = unit
  subst d 0C = 0C
  subst d 1C = 1C
  subst d (plusC e1 e2) = plusC (subst d e1) (subst d e2)
  subst d (var x) = d x
  subst d z = z
  subst d (suc x) = suc (subst d x)
  subst d (rec e e0 e1) = rec (subst d e) (subst d e0) (subst (lem2 (lem2 d)) e1)
  subst d (lam e) = lam (subst (lem2 d) e)
  subst d (app e1 e2) = app (subst d e1) (subst d e2)
  subst d (prod e1 e2) = prod (subst d e1) (subst d e2)
  subst d (l-proj e) = l-proj (subst d e)
  subst d (r-proj e) = r-proj (subst d e)

  postulate
    subst-compose : ∀ {Γ Γ' τ τ1} (Θ : sctx Γ Γ') (v : Γ |- τ) (e : (τ :: Γ' |- τ1) )
                  → subst (lem3 v) (subst (lem2 Θ) e) == subst (lem3' Θ v) e

  postulate
    subst-compose2 : ∀ {Γ Γ' τ} (Θ : sctx Γ Γ') (n : Γ |- nat) (e1 : Γ' |- τ) (e2 : (nat :: (τ :: Γ')) |- τ)
                  →  subst (lem4 n (rec n (subst Θ e1) (subst (lem2 (lem2 Θ)) e2))) (subst (lem2 (lem2 Θ)) e2) ==
                     subst (lem4' Θ n (rec n (subst Θ e1) (subst (lem2 (lem2 Θ)) e2))) e2

  postulate
    subst-compose3 : ∀ {Γ Γ' τ τ1 τ2} (Θ : sctx Γ Γ') (e1 : (τ1 :: (τ2 :: Γ')) |- τ) (v1 : Γ' |- τ1) (v2 : Γ' |- τ2)
                   → subst Θ (subst (lem4 v1 v2) e1) == subst (lem4' Θ (subst Θ v1) (subst Θ v2)) e1

  postulate
    subst-compose4 : ∀ {Γ Γ' τ} (Θ : sctx Γ Γ') (v' : Γ |- nat) (r : Γ |- τ) (e2 : (nat :: (τ :: Γ')) |- τ)
                   → subst (lem4 v' r) (subst (lem2 (lem2 Θ)) e2) == subst (lem4' Θ v' r) e2

-------

  -- define 'stepping' as a datatype (fig. 1 of proof)
  data _≤s_ : ∀ {Γ T} → Γ |- T → Γ |- T → Set where
    refl-s : ∀ {Γ T}
           → {e : Γ |- T}
           → e ≤s e
    trans-s : ∀ {Γ T}
            → {e e' e'' : Γ |- T}
            → e ≤s e' → e' ≤s e''
            → e ≤s e''
    plus-s : ∀ {Γ}
           → {e1 e2 n1 n2 : Γ |- C}
           → e1 ≤s n1 → e2 ≤s n2
           → (plusC e1 e2) ≤s (plusC n1 n2)
    cong-refl : ∀ {Γ τ} {e e' : Γ |- τ} → e == e' → e ≤s e'
    +-unit-l : ∀ {Γ} {e : Γ |- C} → (plusC 0C e) ≤s e
    +-unit-l' : ∀ {Γ} {e : Γ |- C} → e ≤s (plusC 0C e)
    +-unit-r : ∀ {Γ} {e : Γ |- C} → (plusC e 0C) ≤s e
    +-unit-r' : ∀ {Γ} {e : Γ |- C} → e ≤s (plusC e 0C)
    +-assoc : ∀ {Γ} {e1 e2 e3 : Γ |- C} → (plusC e1 (plusC e2 e3)) ≤s (plusC (plusC e1 e2) e3)
    +-assoc' : ∀ {Γ} {e1 e2 e3 : Γ |- C} → (plusC e1 (plusC e2 e3)) ≤s (plusC (plusC e1 e2) e3)
    refl-+ : ∀ {Γ} {e0 e1 : Γ |- C} → (plusC e0 e1) ≤s (plusC e1 e0)
    cong-+ : ∀ {Γ} {e0 e1 e0' e1' : Γ |- C} → e0 ≤s e0' → e1 ≤s e1' → (plusC e0 e1) ≤s (plusC e0' e1')
    cong-lproj : ∀ {Γ τ τ'} {e e' : Γ |- (τ ×c τ')} → e ≤s e' → (l-proj e) ≤s (l-proj e')
    cong-rproj : ∀ {Γ τ τ'} {e e' : Γ |- (τ ×c τ')} → e ≤s e' → (r-proj e) ≤s (r-proj e')
    cong-app   : ∀ {Γ τ τ'} {e e' : Γ |- (τ ->c τ')} {e1 : Γ |- τ} → e ≤s e' → (app e e1) ≤s (app e' e1)
    cong-rec : ∀ {Γ τ} {e e' : Γ |- nat} {e0 : Γ |- τ} {e1 : (nat :: (τ :: Γ)) |- τ}
             → e ≤s e'
             → rec e e0 e1 ≤s rec e' e0 e1
    lam-s : ∀ {Γ T T'}
          → {e : (T :: Γ) |- T'}
          → {e2 : Γ |- T}
          → subst (lem3 e2) e ≤s app (lam e) e2
    l-proj-s : ∀ {Γ T1 T2}
             → {e1 : Γ |- T1}  {e2 : Γ |- T2}
             → e1 ≤s (l-proj (prod e1 e2))
    r-proj-s : ∀ {Γ T1 T2}
             → {e1 : Γ |- T1} → {e2 : Γ |- T2}
             → e2 ≤s (r-proj (prod e1 e2))
    rec-steps-s : ∀ {Γ T}
                → {e : Γ |- nat}
                → {e0 : Γ |- T}
                → {e1 : (nat :: (T :: Γ)) |- T}
                → subst (lem4 e (rec e e0 e1)) e1 ≤s (rec (suc e) e0 e1)
    rec-steps-z : ∀ {Γ T}
                → {e0 : Γ |- T}
                → {e1 : (nat :: (T :: Γ)) |- T}
                → e0 ≤s (rec z e0 e1)

  _trans_ : ∀ {Γ T}
            → {e e' e'' : Γ |- T}
            → e ≤s e' → e' ≤s e''
            → e ≤s e''
  _trans_ = trans-s
  infixr 10 _trans_

-------

  -- interpret complexity types as preorders
  [_]t : CTp → PREORDER
  [ unit ]t = unit-p
  [ nat ]t = Nat , nat-p
  [ A ->c B ]t = [ A ]t ->p [ B ]t
  [ A ×c B ]t = [ A ]t ×p [ B ]t
  [ C ]t = Nat , nat-p

  -- interpret contexts as preorders
  [_]c : Ctx → PREORDER
  [ [] ]c = unit-p
  [ τ :: Γ ]c = [ τ ]t ×p [ Γ ]c

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


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

open import HoTT
open import cohomology.Theory

open import cw.CW

module cw.cohomology.TipAndAugment {i} (OT : OrdinaryTheory i)
  (⊙skel : ⊙Skeleton {i} 0) where

open OrdinaryTheory OT
open import homotopy.DisjointlyPointedSet
open import cohomology.DisjointlyPointedSet OT

module _ (m : ℤ) where
  CX₀ : Group i
  CX₀ = C m (⊙cw-head ⊙skel)

  CX₀-is-abelian : is-abelian CX₀
  CX₀-is-abelian = C-is-abelian m (⊙cw-head ⊙skel)

  C2×CX₀ : Group i
  C2×CX₀ = C2 m ×ᴳ CX₀

  abstract
    C2×CX₀-is-abelian : is-abelian C2×CX₀
    C2×CX₀-is-abelian = ×ᴳ-is-abelian (C2 m) CX₀ (C2-is-abelian m) CX₀-is-abelian

  C2×CX₀-abgroup : AbGroup i
  C2×CX₀-abgroup = C2×CX₀ , C2×CX₀-is-abelian

  CX₀-β : ⊙has-cells-with-choice 0 ⊙skel i
    → CX₀ ≃ᴳ Πᴳ (MinusPoint (⊙cw-head ⊙skel)) (λ _ → C2 m)
  CX₀-β ac = C-set m (⊙cw-head ⊙skel) (snd (⊙Skeleton.skel ⊙skel)) (⊙Skeleton.pt-dec ⊙skel) ac

abstract
  CX₀-≠-is-trivial : ∀ {m} (m≠0 : m ≠ 0)
    → ⊙has-cells-with-choice 0 ⊙skel i
    → is-trivialᴳ (CX₀ m)
  CX₀-≠-is-trivial {m} m≠0 ac =
    iso-preserves'-trivial (CX₀-β m ac) $
      Πᴳ-is-trivial (MinusPoint (⊙cw-head ⊙skel))
        (λ _ → C2 m) (λ _ → C-dimension m≠0)

cw-coε : C2 0 →ᴳ C2×CX₀ 0
cw-coε = ×ᴳ-inl {G = C2 0} {H = CX₀ 0}

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Class.Monad.State where

open import Class.Monad
open import Data.Product
open import Data.Unit.Polymorphic
open import Function
open import Level

private
  variable
    a : Level
    A : Set a

record MonadState {a} (M : Set a → Set a) {{_ : Monad M}} (S : Set a) : Set (suc a) where
  field
    get : M S
    put : S → M ⊤

  modify : (S → S) → M ⊤
  modify f = do
    s <- get
    put (f s)

  gets : (S → A) → M A
  gets f = do
    s <- get
    return (f s)

  state : (S → A × S) → M A
  state f = do
    s ← get
    let (a , s') = f s
    put s'
    return a

open MonadState {{...}} public

module _ {M : Set a → Set a} {{_ : Monad M}} {S S' : Set a} {{_ : MonadState M (S × S')}} where

  MonadStateProj₁ : MonadState M S
  MonadStateProj₁ = record
    { get = get >>= return ∘ proj₁
    ; put = λ x → modify λ { (s , s') → (x , s') } }

  MonadStateProj₂ : MonadState M S'
  MonadStateProj₂ = record
    { get = get >>= return ∘ proj₂
    ; put = λ x → modify λ { (s , s') → (s , x) } }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
postulate
  M : Set → Set
  _>>=_ : ∀ {A B} → M A → (A → M B) → M B
  _>>_  : ∀ {A B} → M A → M B → M B
  _<|>_ : ∀ {A} → M A → M A → M A

infixr 4 _>>=_ _>>_
infixr -100 _<|>_

expr : ∀ {A} → (A → M A) → (A → M A)
expr f a = do
  x ← {!f a!}
  y ← {!f x <|> f a!}
  {!f x <|> f y!}
  {!f x <|> f y!}


text:
{-# OPTIONS --no-copatterns #-}

-- Andreas, 2015-08-26: copatterns are on by default now.
-- Andreas, James, 2011-11-24
-- trigger error message 'NeedOptionCopatterns'
module NeedOptionCopatterns where

record Bla : Set2 where
  field
    bla : Set1
open Bla

f : Bla
bla f = Set
-- should request option --copatterns


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
------------------------------------------------------------------------

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

module Algebra where

open import Algebra.Core public
open import Algebra.Definitions public
open import Algebra.Structures public
open import Algebra.Bundles public


text:
variable
  ℓ : _
  A : Set ℓ

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Groups.Sn where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.ZCohomology.KcompPrelims
open import Cubical.ZCohomology.Groups.Prelims

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim ; elim2 to pElim2 ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁) hiding (map)

open import Cubical.Data.Bool
open import Cubical.Data.Sigma
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +-comm to +ℤ-comm ; +-assoc to +ℤ-assoc)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec)
open import Cubical.Data.Unit

open import Cubical.Algebra.Group

infixr 31 _□_
_□_ : _
_□_ = compGroupIso

open GroupEquiv
open vSES
open GroupIso
open GroupHom
open BijectionIso

Sn-connected : (n : ℕ) (x : typ (S₊∙ (suc n))) → ∥ pt (S₊∙ (suc n)) ≡ x ∥₁
Sn-connected zero = toPropElim (λ _ → propTruncIsProp) ∣ refl ∣₁
Sn-connected (suc zero) = suspToPropElim base (λ _ → propTruncIsProp) ∣ refl ∣₁
Sn-connected (suc (suc n)) = suspToPropElim north (λ _ → propTruncIsProp) ∣ refl ∣₁

H⁰-Sⁿ≅ℤ : (n : ℕ) → GroupIso (coHomGr 0 (S₊ (suc n))) intGroup
H⁰-Sⁿ≅ℤ zero = H⁰-connected base (Sn-connected 0)
H⁰-Sⁿ≅ℤ (suc n) = H⁰-connected north (Sn-connected (suc n))

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

--- We will need to switch between Sⁿ defined using suspensions and using pushouts
--- in order to apply Mayer Vietoris.

S1Iso : Iso S¹ (Pushout {A = Bool} (λ _ → tt) λ _ → tt)
S1Iso = S¹IsoSuspBool ⋄ invIso PushoutSuspIsoSusp

coHomPushout≅coHomSn : (n m : ℕ) → GroupIso (coHomGr m (S₊ (suc n))) (coHomGr m (Pushout {A = S₊ n} (λ _ → tt) λ _ → tt))
coHomPushout≅coHomSn zero m =
  Iso+Hom→GrIso (setTruncIso (domIso S1Iso))
                (sElim2 (λ _ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ _ → refl))
coHomPushout≅coHomSn (suc n) m =
  Iso+Hom→GrIso (setTruncIso (domIso (invIso PushoutSuspIsoSusp)))
                (sElim2 (λ _ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ _ → refl))

-------------------------- H⁰(S⁰) -----------------------------
S0→Int : (a : Int × Int) → S₊ 0 → Int
S0→Int a true = fst a
S0→Int a false = snd a

H⁰-S⁰≅ℤ×ℤ : GroupIso (coHomGr 0 (S₊ 0)) (dirProd intGroup intGroup)
fun (map H⁰-S⁰≅ℤ×ℤ) = sRec (isSet× isSetInt isSetInt) λ f → (f true) , (f false)
isHom (map H⁰-S⁰≅ℤ×ℤ) = sElim2 (λ _ _ → isSet→isGroupoid (isSet× isSetInt isSetInt) _ _)
                                λ a b i → addLemma (a true) (b true) i , addLemma (a false) (b false) i
inv H⁰-S⁰≅ℤ×ℤ a = ∣ S0→Int a ∣₂
rightInv H⁰-S⁰≅ℤ×ℤ _ = refl
leftInv H⁰-S⁰≅ℤ×ℤ = sElim (λ _ → isSet→isGroupoid setTruncIsSet _ _)
                           λ f → cong ∣_∣₂ (funExt (λ {true → refl ; false → refl}))

-- --------------------------H¹(S¹) -----------------------------------
{-
In order to apply Mayer-Vietoris, we need the following lemma.
Given the following diagram
  a ↦ (a , 0)   ψ         ϕ
 A -->  A × A -------> B --->  C
If ψ is an isomorphism and ϕ is surjective with ker ϕ ≡ {ψ (a , a) ∣ a ∈ A}, then C ≅ B
-}

diagonalIso : ∀ {ℓ ℓ' ℓ''} {A : Group {ℓ}} (B : Group {ℓ'}) {C : Group {ℓ''}}
               (ψ : GroupIso (dirProd A A) B) (ϕ : GroupHom B C)
             → isSurjective _ _ ϕ
             → ((x : ⟨ B ⟩) → isInKer B C ϕ x
                                    → ∃[ y ∈ ⟨ A ⟩ ] x ≡ (fun (map ψ)) (y , y))
             → ((x : ⟨ B ⟩) → (∃[ y ∈ ⟨ A ⟩ ] x ≡ (fun (map ψ)) (y , y))
                                    → isInKer B C ϕ x)
             → GroupIso A C
diagonalIso {A = A} B {C = C} ψ ϕ issurj ker→diag diag→ker = BijectionIsoToGroupIso bijIso
  where
  open GroupStr
  module A = GroupStr (snd A)
  module B = GroupStr (snd B)
  module C = GroupStr (snd C)
  module A×A = GroupStr (snd (dirProd A A))
  module ψ = GroupIso ψ
  module ϕ = GroupHom ϕ
  ψ⁻ = inv ψ

  fstProj : GroupHom A (dirProd A A)
  fun fstProj a = a , GroupStr.0g (snd A)
  isHom fstProj g0 g1 i = (g0 A.+ g1) , GroupStr.lid (snd A) (GroupStr.0g (snd A)) (~ i)

  bijIso : BijectionIso A C
  map' bijIso = compGroupHom fstProj (compGroupHom (map ψ) ϕ)
  inj bijIso a inker = pRec (isSetCarrier A _ _)
                             (λ {(a' , id) → (cong fst (sym (leftInv ψ (a , GroupStr.0g (snd A))) ∙∙ cong ψ⁻ id ∙∙ leftInv ψ (a' , a')))
                                           ∙ cong snd (sym (leftInv ψ (a' , a')) ∙∙ cong ψ⁻ (sym id) ∙∙ leftInv ψ (a , GroupStr.0g (snd A)))})
                             (ker→diag _ inker)
  surj bijIso c =
    pRec propTruncIsProp
         (λ { (b , id) → ∣ (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)))
                          , ((sym (GroupStr.rid (snd C) _)
                           ∙∙ cong ((fun ϕ) ((fun (map ψ)) (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)) , GroupStr.0g (snd A))) C.+_)
                                  (sym (diag→ker (fun (map ψ) ((snd (ψ⁻ b)) , (snd (ψ⁻ b))))
                                                  ∣ (snd (ψ⁻ b)) , refl ∣₁))
                           ∙∙ sym ((isHom ϕ) _ _))
                           ∙∙ cong (fun ϕ) (sym ((isHom (map ψ)) _ _)
                                        ∙∙ cong (fun (map ψ)) (ΣPathP (sym (GroupStr.assoc (snd A) _ _ _)
                                                                           ∙∙ cong (fst (ψ⁻ b) A.+_) (GroupStr.invl (snd A) _)
                                                                           ∙∙ GroupStr.rid (snd A) _
                                                                        , (GroupStr.lid (snd A) _)))
                                        ∙∙ rightInv ψ b)
                           ∙∙ id) ∣₁ })
         (issurj c)

H¹-S¹≅ℤ : GroupIso intGroup (coHomGr 1 (S₊ 1))
H¹-S¹≅ℤ =
    diagonalIso (coHomGr 0 (S₊ 0))
                (invGroupIso H⁰-S⁰≅ℤ×ℤ)
                (K.d 0)
                (λ x → K.Ker-i⊂Im-d 0 x
                                     (ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _
                                            , isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _)))
                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
                        (λ x inker
                            → pRec propTruncIsProp
                                    (λ {((f , g) , id') → helper x f g id' inker})
                                    ((K.Ker-d⊂Im-Δ 0 ∣ x ∣₂ inker)))))
                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                         λ F surj
                           → pRec (setTruncIsSet _ _)
                                   (λ { (x , id) → K.Im-Δ⊂Ker-d 0 ∣ F ∣₂
                                                      ∣ (∣ (λ _ → x) ∣₂ , ∣ (λ _ → 0) ∣₂) ,
                                                       (cong ∣_∣₂ (funExt (surjHelper x))) ∙ sym id ∣₁ })
                                   surj) )
  □ invGroupIso (coHomPushout≅coHomSn 0 1)
  where
  module K = MV Unit Unit (S₊ 0) (λ _ → tt) (λ _ → tt)

  surjHelper :  (x : Int) (x₁ : S₊ 0) → x -[ 0 ]ₖ 0 ≡ S0→Int (x , x) x₁
  surjHelper x true = Iso.leftInv (Iso-Kn-ΩKn+1 0) x
  surjHelper x false = Iso.leftInv (Iso-Kn-ΩKn+1 0) x

  helper : (F : S₊ 0 → Int) (f g : ∥ (Unit → Int) ∥₂)
           (id : GroupHom.fun (K.Δ 0) (f , g) ≡ ∣ F ∣₂)
         → isInKer (coHomGr 0 (S₊ 0))
                    (coHomGr 1 (Pushout (λ _ → tt) (λ _ → tt)))
                    (K.d 0)
                    ∣ F ∣₂
         → ∃[ x ∈ Int ] ∣ F ∣₂ ≡ inv H⁰-S⁰≅ℤ×ℤ (x , x)
  helper F =
    sElim2 (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
           λ f g id inker
             → pRec propTruncIsProp
                     (λ ((a , b) , id2)
                        → sElim2 {C = λ f g → GroupHom.fun (K.Δ 0) (f , g) ≡ ∣ F ∣₂ → _ }
                                  (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
                                  (λ f g id → ∣ (helper2 f g .fst) , (sym id ∙ sym (helper2 f g .snd)) ∣₁)
                                  a b id2)
                     (MV.Ker-d⊂Im-Δ _ _ (S₊ 0) (λ _ → tt) (λ _ → tt) 0 ∣ F ∣₂ inker)
    where
    helper2 : (f g : Unit → Int)
            → Σ[ x ∈ Int ] (inv H⁰-S⁰≅ℤ×ℤ (x , x))
             ≡ GroupHom.fun (K.Δ 0) (∣ f ∣₂ , ∣ g ∣₂)
    helper2 f g = (f _ -[ 0 ]ₖ g _) , cong ∣_∣₂ (funExt λ {true → refl ; false → refl})

------------------------- H¹(S⁰) ≅ 0 -------------------------------

private
  Hⁿ-S0≃Kₙ×Kₙ : (n : ℕ) → Iso (S₊ 0 → coHomK (suc n)) (coHomK (suc n) × coHomK (suc n))
  Iso.fun (Hⁿ-S0≃Kₙ×Kₙ n) f = (f true) , (f false)
  Iso.inv (Hⁿ-S0≃Kₙ×Kₙ n) (a , b) true = a
  Iso.inv (Hⁿ-S0≃Kₙ×Kₙ n) (a , b) false = b
  Iso.rightInv (Hⁿ-S0≃Kₙ×Kₙ n) a = refl
  Iso.leftInv (Hⁿ-S0≃Kₙ×Kₙ n) b = funExt λ {true → refl ; false → refl}

  isContrHⁿ-S0 : (n : ℕ) → isContr (coHom (suc n) (S₊ 0))
  isContrHⁿ-S0 n = isContrRetract (Iso.fun (setTruncIso (Hⁿ-S0≃Kₙ×Kₙ n)))
                                  (Iso.inv (setTruncIso (Hⁿ-S0≃Kₙ×Kₙ n)))
                                  (Iso.leftInv (setTruncIso (Hⁿ-S0≃Kₙ×Kₙ n)))
                                  (isContrHelper n)
    where
    isContrHelper : (n : ℕ) → isContr (∥ (coHomK (suc n) × coHomK (suc n)) ∥₂)
    fst (isContrHelper zero) = ∣ (0₁ , 0₁) ∣₂
    snd (isContrHelper zero) = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                  λ y → elim2 {B = λ x y → ∣ (0₁ , 0₁) ∣₂ ≡ ∣(x , y) ∣₂ }
                                  (λ _ _ → isOfHLevelPlus {n = 2} 2 setTruncIsSet _ _)
                                  (toPropElim2 (λ _ _ → setTruncIsSet _ _) refl) (fst y) (snd y)
    isContrHelper (suc zero) = ∣ (0₂ , 0₂) ∣₂
                          , sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                  λ y → elim2 {B = λ x y → ∣ (0₂ , 0₂) ∣₂ ≡ ∣(x , y) ∣₂ }
                                  (λ _ _ → isOfHLevelPlus {n = 2} 3 setTruncIsSet _ _)
                                  (suspToPropElim2 base (λ _ _ → setTruncIsSet _ _) refl) (fst y) (snd y)
    isContrHelper (suc (suc n)) = ∣ (0ₖ (3 + n) , 0ₖ (3 + n)) ∣₂
                          , sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                  λ y → elim2 {B = λ x y → ∣ (0ₖ (3 + n) , 0ₖ (3 + n)) ∣₂ ≡ ∣(x , y) ∣₂ }
                                  (λ _ _ → isProp→isOfHLevelSuc (4 + n) (setTruncIsSet _ _))
                                  (suspToPropElim2 north (λ _ _ → setTruncIsSet _ _) refl) (fst y) (snd y)

H¹-S⁰≅0 : (n : ℕ) → GroupIso (coHomGr (suc n) (S₊ 0)) trivialGroup
H¹-S⁰≅0 n = IsoContrGroupTrivialGroup (isContrHⁿ-S0 n)

------------------------- H²(S¹) ≅ 0 -------------------------------

H²-S¹≅0 : GroupIso (coHomGr 2 (S₊ 1)) trivialGroup
H²-S¹≅0 =
    coHomPushout≅coHomSn 0 2
  □ invGroupIso (vSES→GroupIso _ _ vSES-helper)
  □ H¹-S⁰≅0 0

  where
  module I = MV Unit Unit (S₊ 0) (λ _ → tt) (λ _ → tt)
  vSES-helper : vSES (coHomGr 1 (S₊ 0)) (coHomGr 2 (Pushout (λ _ → tt) (λ _ → tt)))
                     _ _
  isTrivialLeft vSES-helper = isOfHLevelSuc 0 (isOfHLevelΣ 0 (isContrHⁿ-Unit 0) (λ _ → isContrHⁿ-Unit 0))
  isTrivialRight vSES-helper = isOfHLevelSuc 0 (isOfHLevelΣ 0 (isContrHⁿ-Unit 1) (λ _ → isContrHⁿ-Unit 1))
  left vSES-helper = I.Δ 1
  right vSES-helper = I.i 2
  vSES.ϕ vSES-helper = I.d 1
  Ker-ϕ⊂Im-left vSES-helper = I.Ker-d⊂Im-Δ 1
  Ker-right⊂Im-ϕ vSES-helper = sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp) -- doesn't terminate without elimination
                                          λ a → I.Ker-i⊂Im-d 1 ∣ a ∣₂

-- --------------- H¹(Sⁿ), n ≥ 1 --------------------------------------------

H¹-Sⁿ≅0 : (n : ℕ) → GroupIso (coHomGr 1 (S₊ (2 + n))) trivialGroup
H¹-Sⁿ≅0 zero = coHomPushout≅coHomSn 1 1
             □ BijectionIsoToGroupIso bijIso
             □ dirProdGroupIso (Hⁿ-Unit≅0 0) (Hⁿ-Unit≅0 0)
             □ lUnitGroupIso
  where
  module K = MV Unit Unit (S₊ 1) (λ _ → tt) (λ _ → tt)
  surj-helper : (x : ⟨ coHomGr 0 (S₊ _) ⟩) → isInIm _ _ (K.Δ 0) x
  surj-helper =
    sElim (λ _ → isOfHLevelSuc 1 propTruncIsProp)
           λ f → ∣ (∣ (λ _ → f base) ∣₂ , 0ₕ 0)
                 , (cong ∣_∣₂ (funExt (toPropElim
                                       (λ _ → isSetInt _ _)
                                       (cong (λ x → f base +[ 0 ]ₖ x) (-0ₖ {n = 0})  ∙ rUnitₖ 0 (f base))))) ∣₁
  helper : isInjective _ _ (K.i 1)
  helper =
    sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 (setTruncIsSet _ _))
           λ x inker → pRec (setTruncIsSet _ _)
                            (sigmaElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                        λ a id → sym id ∙ K.Im-Δ⊂Ker-d 0 ∣ a ∣₂ (surj-helper _))
                            (K.Ker-i⊂Im-d 0 ∣ x ∣₂ inker)
  bijIso : BijectionIso (coHomGr 1 (Pushout (λ _ → tt) (λ _ → tt)))
                                   (dirProd (coHomGr 1 Unit) (coHomGr 1 Unit))
  map' bijIso = K.i 1
  inj bijIso = helper
  surj bijIso x = ∣ 0ₕ _ , isOfHLevelSuc 0 (isOfHLevelΣ 0 (isContrHⁿ-Unit zero) (λ _ → isContrHⁿ-Unit 0)) _ x ∣₁
H¹-Sⁿ≅0 (suc n) = coHomPushout≅coHomSn (2 + n) 1
                 □ BijectionIsoToGroupIso bijIso
                 □ dirProdGroupIso (Hⁿ-Unit≅0 0) (Hⁿ-Unit≅0 0)
                 □ lUnitGroupIso
  where
  module K = MV Unit Unit (S₊ (2 + n)) (λ _ → tt) (λ _ → tt)
  surj-helper : (x : ⟨ coHomGr 0 (S₊ _) ⟩) → isInIm _ _ (K.Δ 0) x
  surj-helper =
    sElim (λ _ → isOfHLevelSuc 1 propTruncIsProp)
           λ f → ∣ (∣ (λ _ → f north) ∣₂ , 0ₕ 0)
                 , cong ∣_∣₂ (funExt (suspToPropElim
                                        (ptSn (suc n))
                                        (λ _ → isSetInt _ _)
                                        (cong (λ x → f north +[ 0 ]ₖ x) (-0ₖ {n = 0})  ∙ rUnitₖ 0 (f north)))) ∣₁
  helper : isInjective _ _ (K.i 1)
  helper =
    sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 (setTruncIsSet _ _))
           λ x inker → pRec (setTruncIsSet _ _)
                            (sigmaElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                        λ a id → sym id ∙ K.Im-Δ⊂Ker-d 0 ∣ a ∣₂ (surj-helper _))
                            (K.Ker-i⊂Im-d 0 ∣ x ∣₂ inker)
  bijIso : BijectionIso (coHomGr 1 (Pushout (λ _ → tt) (λ _ → tt)))
                                   (dirProd (coHomGr 1 Unit) (coHomGr 1 Unit))
  map' bijIso = K.i 1
  inj bijIso = helper
  surj bijIso x = ∣ 0ₕ _ , isOfHLevelSuc 0 (isOfHLevelΣ 0 (isContrHⁿ-Unit zero) (λ _ → isContrHⁿ-Unit 0)) _ x ∣₁

--------- Direct proof of H¹(S¹) ≅ ℤ without Mayer-Vietoris -------

-- The strategy is to use the proof that ΩS¹ ≃ ℤ. Since we only have this for S¹ with the base/loop definition
-- we begin with some functions translating between H¹(S₊ 1) and ∥ S¹ → S¹ ∥₀.  The latter type is easy to characterise,
-- by (S¹ → S¹) ≃ S¹ × ℤ (see Cubical.ZCohomology.Groups.Prelims). Truncating this leaves only ℤ, since S¹ is connected.

-- The translation mentioned above uses the basechange function. We use basechange-lemma (Cubical.ZCohomology.Groups.Prelims) to prove the basechange2⁻ preserves
-- path composition (in a more general sense than what is proved in basechange2⁻-morph)

-- We can now give the group equivalence. The first bit is just a big composition of our previously defined translations and is pretty uninteresting.
-- The harder step is proving that the equivalence is a morphism. This relies heavily on the fact that addition the cohomology groups essentially is defined using an
-- application of cong₂, which allows us to use basechange-lemma.

coHom1S1≃ℤ : GroupIso (coHomGr 1 (S₊ 1)) intGroup
coHom1S1≃ℤ = theIso
  where
  F = Iso.fun S¹→S¹≡S¹×Int
  F⁻ = Iso.inv S¹→S¹≡S¹×Int

  theIso : GroupIso (coHomGr 1 (S₊ 1)) intGroup
  fun (map theIso) = sRec isSetInt (λ f → snd (F f))
  isHom (map theIso) = sElim2 (λ _ _ → isOfHLevelPath 2 isSetInt _ _)
                              λ f g → ((λ i → winding (guy (ΩKn+1→Kn 1 (Kn→ΩKn+1 1 (f base) ∙ Kn→ΩKn+1 1 (g base)))
                                              (λ i → S¹map (ΩKn+1→Kn 1 (Kn→ΩKn+1 1 (f (loop i)) ∙ Kn→ΩKn+1 1 (g (loop i))))))))
                                   ∙∙ cong winding (helper (f base) (g base) f g refl refl)
                                   ∙∙ winding-hom (guy (f base) (λ i → S¹map (f (loop i))))
                                                  (guy (g base) (λ i → S¹map (g (loop i))))
    where
    guy = basechange2⁻ ∘ S¹map

    helper : (x y : coHomK 1) (f g : S₊ 1 → coHomK 1)
           → (f base) ≡ x
           → (g base) ≡ y
           → (guy (ΩKn+1→Kn 1 (Kn→ΩKn+1 1 (f base) ∙ Kn→ΩKn+1 1 (g base)))
                   (λ i → S¹map ((ΩKn+1→Kn 1 (Kn→ΩKn+1 1 (f (loop i)) ∙ Kn→ΩKn+1 1 (g (loop i)))))))
             ≡ (guy (f base)
                    (λ i → S¹map (f (loop i))))
             ∙ (guy (g base)
                    (λ i → S¹map ((g (loop i)))))
    helper =
      elim2 (λ _ _ → isGroupoidΠ4 λ _ _ _ _ → isOfHLevelPath 3 (isOfHLevelSuc 3 (isGroupoidS¹) base base) _ _)
            (toPropElim2
              (λ _ _ → isPropΠ4 λ _ _ _ _ → isGroupoidS¹ _ _ _ _)
              λ f g reflf reflg →
              basechange-lemma base base
                (S¹map ∘ (ΩKn+1→Kn 1))
                ((Kn→ΩKn+1 1) ∘ f) ((Kn→ΩKn+1 1) ∘ g)
                (cong (Kn→ΩKn+1 1) reflf ∙ Kn→ΩKn+10ₖ 1) (cong (Kn→ΩKn+1 1) reflg ∙ Kn→ΩKn+10ₖ 1)
              ∙ λ j → guy (Iso.leftInv (Iso-Kn-ΩKn+1 1) (f base) j)
                          (λ i → S¹map (Iso.leftInv (Iso-Kn-ΩKn+1 1) (f (loop i)) j))
                    ∙ guy (Iso.leftInv (Iso-Kn-ΩKn+1 1) (g base) j)
                          (λ i → S¹map (Iso.leftInv (Iso-Kn-ΩKn+1 1) (g (loop i)) j)))
  inv theIso a = ∣ (F⁻ (base , a)) ∣₂
  rightInv theIso a = cong snd (Iso.rightInv S¹→S¹≡S¹×Int (base , a))
  leftInv theIso = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                          λ f → cong ((sRec setTruncIsSet ∣_∣₂)
                                        ∘ sRec setTruncIsSet λ x → ∣ F⁻ (x , (snd (F f))) ∣₂)
                                      (Iso.inv PathIdTrunc₀Iso (isConnectedS¹ (fst (F f))))
                              ∙ cong ∣_∣₂ (Iso.leftInv S¹→S¹≡S¹×Int f)

---------------------------- Hⁿ(Sⁿ) ≅ ℤ , n ≥ 1 -------------------

Hⁿ-Sⁿ≅ℤ : (n : ℕ) → GroupIso intGroup (coHomGr (suc n) (S₊ (suc n)))
Hⁿ-Sⁿ≅ℤ zero = invGroupIso coHom1S1≃ℤ
Hⁿ-Sⁿ≅ℤ (suc n) =
    Hⁿ-Sⁿ≅ℤ n
  □ vSES→GroupIso _ _ theIso
  □ invGroupIso (coHomPushout≅coHomSn (suc n) (suc (suc n)))
  where
  module K = MV Unit Unit (S₊ (suc n)) (λ _ → tt) (λ _ → tt)
  theIso : vSES (coHomGr (suc n) (S₊ (suc n))) (coHomGr (suc (suc n))
                (Pushout {A = S₊ (suc n)} (λ _ → tt) (λ _ → tt)))
                _
                _
  isTrivialLeft theIso p q = ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit n) (fst p) (fst q)
                                        , isOfHLevelSuc 0 (isContrHⁿ-Unit n) (snd p) (snd q))
  isTrivialRight theIso p q = ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit (suc n)) (fst p) (fst q)
                                         , isOfHLevelSuc 0 (isContrHⁿ-Unit (suc n)) (snd p) (snd q))
  left theIso = K.Δ (suc n)
  right theIso = K.i (2 + n)
  vSES.ϕ theIso = K.d (suc n)
  Ker-ϕ⊂Im-left theIso = K.Ker-d⊂Im-Δ  (suc n)
  Ker-right⊂Im-ϕ theIso = K.Ker-i⊂Im-d (suc n)

max_stars_repo_name: mchristianl/cubical

max_issues_repo_name: mchristianl/cubical

max_forks_repo_name: aljungstrom/cubical


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

module Generic.Semantics.Elaboration.LetBinder where

open import Size
open import Data.Product
open import Agda.Builtin.List
open import Function
open import Relation.Unary

open import Data.Environment
open import Generic.Syntax
open import Generic.Syntax.LetBinder
open import Generic.Semantics
open import Generic.Semantics.Syntactic

private
  variable
    I : Set
    d : Desc I
    σ : I
    Γ Δ : List I
    s : Size

-- Elaborating away a single let-binder. The algebra is defined by case analysis
-- over the constructors:

-- * let-binders are inlined thanks to the substitution _[_/0] which takes two
-- arguments t and e and instatiates the first free variable of t with e.

-- * the other constructors are left as is by reusing Substitution's algebra

UnLet : Semantics (d `+ Let) (Tm d ∞) (Tm d ∞)
Semantics.th^𝓥  UnLet = th^Tm
Semantics.var   UnLet = id
Semantics.alg   UnLet = case (Semantics.alg Sub) $ λ where
 (`IN' e t) →  extract t (ε ∙ e)

unLet : (Γ ─Env) (Tm d ∞) Δ → Tm (d `+ Let) s σ Γ → Tm d ∞ σ Δ
unLet ρ t = Semantics.semantics UnLet ρ t

unlet : ∀[ Tm (d `+ Let) ∞ σ ⇒ Tm d ∞ σ ]
unlet = Semantics.semantics UnLet (pack `var)

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module reverse-involution where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open Eq.≡-Reasoning
open import lists using (List; []; _∷_; [_]; _++_; reverse)
open import reverse-++-distrib using (reverse-++-distrib)

-- reverseが対合(involution)である事の証明
reverse-involution : {A : Set} → (xs : List A)
  → reverse (reverse xs) ≡ xs
reverse-involution [] =
  begin
    reverse (reverse [])
  ≡⟨⟩
    reverse []
  ≡⟨⟩
    []
  ∎
reverse-involution (x ∷ xs) =
  begin
    reverse (reverse (x ∷ xs))
  ≡⟨⟩
    reverse ((reverse xs) ++ [ x ])
  ≡⟨ reverse-++-distrib (reverse xs) [ x ] ⟩
    (reverse [ x ]) ++ (reverse (reverse xs))
  ≡⟨⟩
    [ x ] ++ reverse (reverse xs)
  ≡⟨ cong (x ∷_) (reverse-involution xs) ⟩
    x ∷ xs
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
------------------------------------------------------------------------------
-- Definition of the gcd of two natural numbers using the Euclid's algorithm
------------------------------------------------------------------------------

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

module FOTC.Program.GCD.Partial.GCD where

open import FOTC.Base
open import FOTC.Base.Loop
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities

------------------------------------------------------------------------------
-- In GHC ≤ 7.0.4 the gcd is a partial function, i.e. gcd 0 0 = undefined.

postulate
  gcd    : D → D → D
  gcd-eq : ∀ m n → gcd m n ≡
           (if (iszero₁ n)
              then (if (iszero₁ m)
                      then error
                      else m)
              else (if (iszero₁ m)
                      then n
                      else (if (gt m n)
                              then gcd (m ∸ n) n
                              else gcd m (n ∸ m))))
{-# ATP axiom gcd-eq #-}


text:
module Cats.Limit.Product where

open import Data.Bool using (Bool ; true ; false)
open import Data.Product using (_×_ ; _,_ ; ∃-syntax ; proj₁ ; proj₂)

open import Cats.Category
open import Cats.Category.Cones using (Cones ; Cone ; HasObj-Cone)
open import Cats.Category.Discrete as Discrete using (Discrete)
open import Cats.Functor using (Functor)
open import Cats.Limit
open import Cats.Util.Conv

module _ {lo la l≈ li}
  {Cat : Category lo la l≈}
  {I : Set li} {O : I → Category.Obj Cat}
  where

  open Category Cat
  open Product using (isProduct)
  open Cone using (arr)

  F : Functor (Discrete I) Cat
  F = Discrete.functor I O

  private
    module Cones = Category (Cones F)

  productData→cone : ∀ {P} → (∀ i → P ⇒ O i) → Cone F
  productData→cone {P} proj = record
      { Apex = P
      ; arr = proj
      ; commute = λ { Discrete.id → ≈.sym id-l }
      }

  cone→productData : Cone F → ∃[ P ] (∀ i → P ⇒ O i)
  cone→productData c = c ᴼ , arr c

  terminal : ∀ {P} {proj : ∀ i → P ⇒ O i}
    → IsProduct O P proj
    → Cones.IsTerminal (productData→cone proj)
  terminal {P} {proj} isProduct c = record
      { arr = record
          { θ = θ
          ; commute = commute
          }
      ; unique = λ where
          {record { θ = θ′ ; commute = commute′ }} _ →
            ∃!′.unique prod (λ i → ≈.sym (commute′ i))
      }
    where
      prod : ∃![ u ] (∀ i → arr c i ≈ proj i ∘ u)
      prod = isProduct (arr c)

      θ : c ᴼ ⇒ P
      θ = prod ⃗

      commute : ∀ j → arr (productData→cone proj) j ∘ θ ≈ arr c j
      commute j = ≈.sym (∃!′.prop prod j)

  product : ∀ {c}
    → Cones.IsTerminal c
    → let (P , proj) = cone→productData c
      in IsProduct O P proj
  product {c} term {X} x = record
      { arr = f
      ; prop = prop
      ; unique = uniq
      }
    where
      open Cats.Category.Cones._⇒_ using (θ ; commute)

      P = proj₁ (cone→productData c)
      proj = proj₂ (cone→productData c)

      u : Cones.∃! (productData→cone x) c
      u = term (productData→cone x)

      f : X ⇒ P
      f = θ (u ⃗)

      prop : ∀ i → x i ≈ proj i ∘ f
      prop i = ≈.sym (commute (u ⃗) _)

      uniq : IsUniqueSuchThat (λ g → ∀ i → x i ≈ proj i ∘ g) f
      uniq {g} eq = Cones.∃!′.unique u {f′} _
        where
          f′ : productData→cone x Cones.⇒ c
          f′ = record
              { θ = g
              ; commute = λ i → ≈.sym (eq i)
              }

  product→limit : Product O → Limit F
  product→limit P = record
      { cone = productData→cone (Product.proj P)
      ; isLimit = terminal (isProduct P)
      }

  limit→product : Limit F → Product O
  limit→product L
      = let (P , proj) = cone→productData (L ᴼ) in
        record
          { prod = P
          ; proj = proj
          ; isProduct = product (Limit.isLimit L)
          }

  product-unique : (P Q : Product O) → P ᴼ ≅ Q ᴼ
  product-unique P Q = obj-unique (product→limit P) (product→limit Q)


text:
-- Very simple facts about natural numbers
module NatSimple where

import Data.Fin as F

open import Data.Empty
open import Data.Unit
open import Data.Unit.Core
open import Data.Nat renaming (_⊔_ to _⊔ℕ_)
open import Data.Sum renaming (map to _⊎→_)
open import Data.Product renaming (map to _×→_)
open import Function renaming (_∘_ to _○_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import FT

------------------------------------------------------------------------------
-- Equivalences (not used)

data Dec (A : Set) : Set where
  yes : A → Dec A
  no : (A → ⊥) → Dec A

sucEq : {n : ℕ} → (i j : F.Fin n) → (F.suc i) ≡ (F.suc j) → i ≡ j
sucEq i .i refl = refl

_=F=_ : {n : ℕ} → (i j : F.Fin n) → Dec (i ≡ j)
F.zero    =F= F.zero                     = yes refl
(F.suc i) =F= F.zero                     = no (λ ())
F.zero    =F= (F.suc j)                  = no (λ ())
(F.suc i) =F= (F.suc j) with i =F= j
(F.suc i) =F= (F.suc .i) | yes refl      = yes refl
(F.suc i) =F= (F.suc j) | no p           = no (λ q → p (sucEq i j q))

------------------------------------------------------------------
-- Finite Types and the natural numbers are intimately related.

toℕ : FT → ℕ
toℕ ZERO = zero
toℕ ONE = suc zero
toℕ (PLUS b₀ b₁) = (toℕ b₀) + (toℕ b₁)
toℕ (TIMES b₀ b₁) = (toℕ b₀) * (toℕ b₁)

fromℕ : ℕ → FT
fromℕ zero    = ZERO
fromℕ (suc n) = PLUS ONE (fromℕ n)

normalize : FT → FT
normalize = fromℕ ○ toℕ

assocr : {m : ℕ} (n : ℕ) → (PLUS (fromℕ n) (fromℕ m)) ⇛ fromℕ (n + m)
assocr zero = unite₊⇛
assocr (suc n) = assocr₊⇛ ◎ (id⇛ ⊕ (assocr n))

distr : (n₀ : ℕ) {n₁ : ℕ} → TIMES (fromℕ n₀) (fromℕ n₁) ⇛ fromℕ (n₀ * n₁)
distr zero = distz⇛
distr (suc n) {m} = dist⇛ ◎ (unite⋆⇛ ⊕ distr n) ◎ assocr m

normal : (b : FT) → b ⇛ normalize b
normal ZERO = id⇛
normal ONE = uniti₊⇛ ◎ swap₊⇛
normal (PLUS b₀ b₁) = (normal b₀ ⊕ normal b₁) ◎ assocr (toℕ b₀)
normal (TIMES b₀ b₁) = (normal b₀ ⊗ normal b₁) ◎ distr (toℕ b₀)

-- normalize a finite type to (1 + (1 + (1 + ... + (1 + 0) ... )))
-- a bunch of ones ending with zero with left biased + in between

⟦_⟧ℕ : ℕ → Set
⟦ zero ⟧ℕ  = ⊥
⟦ suc n ⟧ℕ = ⊤ ⊎ ⟦ n ⟧ℕ

-- Take a natural number n, and a value of the type represented by that n,
-- and return the canonical finite set of size n.
fromNormalNat : (n : ℕ) → ⟦ n ⟧ℕ → F.Fin n
fromNormalNat zero     ()
fromNormalNat (suc n) (inj₁ tt) = F.zero
fromNormalNat (suc n) (inj₂ x) = F.suc (fromNormalNat n x)

-- Take a natural number n, a finite set of size n, and return a
-- (canonical) value of the type represented by n
toNormalNat : (n : ℕ) → F.Fin n → ⟦ n ⟧ℕ
toNormalNat zero     ()
toNormalNat (suc n) F.zero = inj₁ tt
toNormalNat (suc n) (F.suc f) = inj₂ (toNormalNat n f)

-- BEGIN CODE COPIED (AND SOMEWHAT MODIFIED) FROM Nat.Properties
-- (for some reason +-comm is a private field so I can't get to it without
-- importing superfluous files and going through a bunch of administrative
-- garbage that isn't worth my time)

m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
m+1+n≡1+m+n zero    n = refl
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)

+-identity : {n : ℕ} → n + zero ≡ n
+-identity = n+0≡n _
  where
  n+0≡n : (n : ℕ) → n + zero ≡ n
  n+0≡n zero    = refl
  n+0≡n (suc n) = cong suc (n+0≡n n)

+-comm : (m n : ℕ) → m + n ≡ n + m
+-comm zero    n = sym +-identity
+-comm (suc m) n = begin
    suc m + n
  ≡⟨ refl ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨ sym (m+1+n≡1+m+n n m) ⟩
    n + suc m
  ∎

-- END CODE COPIED FROM Nat.Properties

--
add1modn : ℕ → ℕ → ℕ → ℕ
add1modn zero zero acc = zero
add1modn zero (suc n) acc = (suc n) + acc
add1modn (suc max) zero acc = suc acc
add1modn (suc max) (suc n) acc = add1modn max n (suc acc)

-- Useful for testing
one : ℕ
one = suc (zero)

two : ℕ
two = suc one

three : ℕ
three = suc two

four : ℕ
four = suc three

five : ℕ
five = suc four

six : ℕ
six = suc five

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Cubical.Algebra.Base public
open import Cubical.Algebra.Definitions public

open import Cubical.Algebra.Structures public using (IsGroup; isgroup)
open import Cubical.Algebra.Bundles public using (Group; mkgroup; GroupCarrier)
open import Cubical.Structures.Carrier public

open import Cubical.Algebra.Group.Properties public
open import Cubical.Algebra.Group.Morphism public
open import Cubical.Algebra.Group.MorphismProperties public hiding (isPropIsGroup)


text:
------------------------------------------------------------------------
-- List-related properties
------------------------------------------------------------------------

-- Note that the lemmas below could be generalised to work with other
-- equalities than _≡_.

module Data.List.Properties where

open import Data.List
open import Data.Nat
open import Data.Nat.Properties
open import Data.Bool
open import Data.Function
open import Data.Product as Prod hiding (map)
open import Data.Maybe
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as Eq
open import Algebra

∷-injective : ∀ {A} {x y xs ys} →
              (List A ∶ x ∷ xs) ≡ (y ∷ ys) → (x ≡ y) × (xs ≡ ys)
∷-injective refl = (refl , refl)

right-identity-unique : ∀ {A} (xs : List A) {ys} →
                        xs ≡ xs ++ ys → ys ≡ []
right-identity-unique []       refl = refl
right-identity-unique (x ∷ xs) eq   =
  right-identity-unique xs (proj₂ (∷-injective eq))

-- Map, sum, and append.

map-++-commute : ∀ {a b} (f : a → b) xs ys →
                 map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-commute f []       ys = refl
map-++-commute f (x ∷ xs) ys =
  cong (_∷_ (f x)) (map-++-commute f xs ys)

sum-++-commute : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
sum-++-commute []       ys = refl
sum-++-commute (x ∷ xs) ys = begin
  x + sum (xs ++ ys)
                         ≡⟨ cong (_+_ x) (sum-++-commute xs ys) ⟩
  x + (sum xs + sum ys)
                         ≡⟨ sym $ +-assoc x _ _ ⟩
  (x + sum xs) + sum ys
                         ∎
  where
  open CommutativeSemiring commutativeSemiring hiding (_+_; sym)
  open ≡-Reasoning

-- Various properties about folds.

foldr-universal : ∀ {a b} (h : List a → b) f e →
                  (h [] ≡ e) →
                  (∀ x xs → h (x ∷ xs) ≡ f x (h xs)) →
                  h ≗ foldr f e
foldr-universal h f e base step []       = base
foldr-universal h f e base step (x ∷ xs) = begin
  h (x ∷ xs)
    ≡⟨ step x xs ⟩
  f x (h xs)
    ≡⟨ cong (f x) (foldr-universal h f e base step xs) ⟩
  f x (foldr f e xs)
    ∎
  where open ≡-Reasoning

foldr-fusion : ∀ {a b c} (h : b → c)
                 {f : a → b → b} {g : a → c → c} (e : b) →
               (∀ x y → h (f x y) ≡ g x (h y)) →
               h ∘ foldr f e ≗ foldr g (h e)
foldr-fusion h {f} {g} e fuse =
  foldr-universal (h ∘ foldr f e) g (h e) refl
                  (λ x xs → fuse x (foldr f e xs))

idIsFold : ∀ {a} → id {a = List a} ≗ foldr _∷_ []
idIsFold = foldr-universal id _∷_ [] refl (λ _ _ → refl)

++IsFold : ∀ {a} (xs ys : List a) →
           xs ++ ys ≡ foldr _∷_ ys xs
++IsFold xs ys =
  begin
    xs ++ ys
  ≡⟨ cong (λ xs → xs ++ ys) (idIsFold xs) ⟩
    foldr _∷_ [] xs ++ ys
  ≡⟨ foldr-fusion (λ xs → xs ++ ys) [] (λ _ _ → refl) xs ⟩
    foldr _∷_ ([] ++ ys) xs
  ≡⟨ refl ⟩
    foldr _∷_ ys xs
  ∎
  where open ≡-Reasoning

mapIsFold : ∀ {a b} {f : a → b} →
            map f ≗ foldr (λ x ys → f x ∷ ys) []
mapIsFold {f = f} =
  begin
    map f
  ≈⟨ cong (map f) ∘ idIsFold ⟩
    map f ∘ foldr _∷_ []
  ≈⟨ foldr-fusion (map f) [] (λ _ _ → refl) ⟩
    foldr (λ x ys → f x ∷ ys) []
  ∎
  where open Eq (_ →-setoid _)

concat-map : ∀ {a b} {f : a → b} →
             concat ∘ map (map f) ≗ map f ∘ concat
concat-map {f = f} =
  begin
    concat ∘ map (map f)
  ≈⟨ cong concat ∘ mapIsFold ⟩
    concat ∘ foldr (λ xs ys → map f xs ∷ ys) []
  ≈⟨ foldr-fusion concat [] (λ _ _ → refl) ⟩
    foldr (λ ys zs → map f ys ++ zs) []
  ≈⟨ sym ∘
     foldr-fusion (map f) [] (λ ys zs → map-++-commute f ys zs) ⟩
    map f ∘ concat
  ∎
  where open Eq (_ →-setoid _)

map-id : ∀ {A} → map id ≗ id {List A}
map-id = begin
  map id        ≈⟨ mapIsFold ⟩
  foldr _∷_ []  ≈⟨ sym ∘ idIsFold ⟩
  id            ∎
  where open Eq (_ →-setoid _)

map-compose : ∀ {a b c} {g : b → c} {f : a → b} →
              map (g ∘ f) ≗ map g ∘ map f
map-compose {g = g} {f} =
  begin
    map (g ∘ f)
  ≈⟨ cong (map (g ∘ f)) ∘ idIsFold ⟩
    map (g ∘ f) ∘ foldr _∷_ []
  ≈⟨ foldr-fusion (map (g ∘ f)) [] (λ _ _ → refl) ⟩
    foldr (λ a y → g (f a) ∷ y) []
  ≈⟨ sym ∘ foldr-fusion (map g) [] (λ _ _ → refl) ⟩
    map g ∘ foldr (λ a y → f a ∷ y) []
  ≈⟨ cong (map g) ∘ sym ∘ mapIsFold ⟩
    map g ∘ map f
  ∎
  where open Eq (_ →-setoid _)

foldr-cong : ∀ {a b} {f₁ f₂ : a → b → b} {e₁ e₂ : b} →
             (∀ x y → f₁ x y ≡ f₂ x y) → e₁ ≡ e₂ →
             foldr f₁ e₁ ≗ foldr f₂ e₂
foldr-cong {f₁ = f₁} {f₂} {e} f₁≗₂f₂ refl =
  begin
    foldr f₁ e
  ≈⟨ cong (foldr f₁ e) ∘ idIsFold ⟩
    foldr f₁ e ∘ foldr _∷_ []
  ≈⟨ foldr-fusion (foldr f₁ e) [] (λ x xs → f₁≗₂f₂ x (foldr f₁ e xs)) ⟩
    foldr f₂ e
  ∎
  where open Eq (_ →-setoid _)

map-cong : ∀ {a b} {f g : a → b} → f ≗ g → map f ≗ map g
map-cong {f = f} {g} f≗g =
  begin
    map f
  ≈⟨ mapIsFold ⟩
    foldr (λ x ys → f x ∷ ys) []
  ≈⟨ foldr-cong (λ x ys → cong₂ _∷_ (f≗g x) refl) refl ⟩
    foldr (λ x ys → g x ∷ ys) []
  ≈⟨ sym ∘ mapIsFold ⟩
    map g
  ∎
  where open Eq (_ →-setoid _)

-- Take, drop, and splitAt.

take++drop : ∀ {a} n (xs : List a) → take n xs ++ drop n xs ≡ xs
take++drop zero    xs       = refl
take++drop (suc n) []       = refl
take++drop (suc n) (x ∷ xs) =
  cong (λ xs → x ∷ xs) (take++drop n xs)

splitAt-defn : ∀ {a} n → splitAt {a} n ≗ < take n , drop n >
splitAt-defn zero    xs       = refl
splitAt-defn (suc n) []       = refl
splitAt-defn (suc n) (x ∷ xs) with splitAt n xs | splitAt-defn n xs
... | (ys , zs) | ih = cong (Prod.map (_∷_ x) id) ih

-- TakeWhile, dropWhile, and span.

takeWhile++dropWhile : ∀ {a} (p : a → Bool) (xs : List a) →
                       takeWhile p xs ++ dropWhile p xs ≡ xs
takeWhile++dropWhile p []       = refl
takeWhile++dropWhile p (x ∷ xs) with p x
... | true  = cong (_∷_ x) (takeWhile++dropWhile p xs)
... | false = refl

span-defn : ∀ {a} (p : a → Bool) →
            span p ≗ < takeWhile p , dropWhile p >
span-defn p []       = refl
span-defn p (x ∷ xs) with p x
... | true  = cong (Prod.map (_∷_ x) id) (span-defn p xs)
... | false = refl

-- Partition.

partition-defn : ∀ {a} (p : a → Bool) →
                 partition p ≗ < filter p , filter (not ∘ p) >
partition-defn p []       = refl
partition-defn p (x ∷ xs)
 with p x | partition p xs | partition-defn p xs
...  | true  | (ys , zs) | eq = cong (Prod.map (_∷_ x) id) eq
...  | false | (ys , zs) | eq = cong (Prod.map id (_∷_ x)) eq

-- Inits, tails, and scanr.

scanr-defn : ∀ {a b} (f : a → b → b) (e : b) →
             scanr f e ≗ map (foldr f e) ∘ tails
scanr-defn f e []             = refl
scanr-defn f e (x ∷ [])       = refl
scanr-defn f e (x₁ ∷ x₂ ∷ xs)
  with scanr f e (x₂ ∷ xs) | scanr-defn f e (x₂ ∷ xs)
...  | [] | ()
...  | y ∷ ys | eq with ∷-injective eq
...        | y≡fx₂⦇f⦈xs , _ = cong₂ (λ z zs → f x₁ z ∷ zs) y≡fx₂⦇f⦈xs eq

scanl-defn : ∀ {a b} (f : a → b → a) (e : a) →
             scanl f e ≗ map (foldl f e) ∘ inits
scanl-defn f e []       = refl
scanl-defn f e (x ∷ xs) = cong (_∷_ e) (begin
     scanl f (f e x) xs
  ≡⟨ scanl-defn f (f e x) xs ⟩
     map (foldl f (f e x)) (inits xs)
  ≡⟨ refl ⟩
     map (foldl f e ∘ (_∷_ x)) (inits xs)
  ≡⟨ map-compose (inits xs) ⟩
     map (foldl f e) (map (_∷_ x) (inits xs))
  ∎)
  where open ≡-Reasoning

-- Length.

length-map : ∀ {A B} (f : A → B) xs →
             length (map f xs) ≡ length xs
length-map f []       = refl
length-map f (x ∷ xs) = cong suc (length-map f xs)

length-gfilter : ∀ {A B} (p : A → Maybe B) xs →
                 length (gfilter p xs) ≤ length xs
length-gfilter p []       = z≤n
length-gfilter p (x ∷ xs) with p x
length-gfilter p (x ∷ xs) | just y  = s≤s (length-gfilter p xs)
length-gfilter p (x ∷ xs) | nothing = ≤-step (length-gfilter p xs)

max_issues_repo_name: larrytheliquid/Lemmachine


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.Verifier        as Verifier
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Encode
open import Util.PKCS                           hiding (verify)
open import Util.Prelude
------------------------------------------------------------------------------
import      Data.List.Base                      as List
open import Data.String                         using (String)

module LibraBFT.Impl.Types.EpochChangeProof where

obmLastLIWS : EpochChangeProof → Either ErrLog LedgerInfoWithSignatures
obmLastLIWS self = maybeS (lastMay (self ^∙ ecpLedgerInfoWithSigs))
                          (Left fakeErr {-["EpochChangeProof", "obmLastLIWS", "empty"]-})
                          pure

-- first/lowest epoch of the proof to indicate which epoch this proof is helping with
epoch : EpochChangeProof -> Either ErrLog Epoch
epoch self = maybeS (headMay (self ^∙ ecpLedgerInfoWithSigs))
                    (Left fakeErr {-["EpochChangeProof", "epoch", "empty"]-})
                    (pure ∘ (_^∙ liwsLedgerInfo ∙ liEpoch))

obmLastEpoch : EpochChangeProof → Epoch
obmLastEpoch self = eitherS (obmLastLIWS self) (const ({-Epoch-} 0)) (_^∙ liwsLedgerInfo ∙ liEpoch)

verify
  : {verifier : Set} ⦃ _ : Verifier.Verifier verifier ⦄
  → EpochChangeProof → verifier
  → Either ErrLog LedgerInfoWithSignatures
verify self verifier = do
  lcheck (not (null (self ^∙ ecpLedgerInfoWithSigs)))
         (here' ("empty" ∷ []))
  lastLedgerInfoWithSigs ← last (self ^∙ ecpLedgerInfoWithSigs)
  lcheckInfo (not (Verifier.isLedgerInfoStale verifier (lastLedgerInfoWithSigs ^∙ liwsLedgerInfo)))
             (here' ("stale" ∷ []))
      -- Skip stale ledger infos in the proof prefix.
  let ledgerInfosWithSigs =
        List.boolFilter
          (λ liws → not (Verifier.isLedgerInfoStale verifier (liws ^∙ liwsLedgerInfo)))
          (self ^∙ ecpLedgerInfoWithSigs)

  -- check the non-stale chain
  loop verifier ledgerInfosWithSigs

  pure lastLedgerInfoWithSigs
 where
  loop
    : {verifier : Set} ⦃ _ : Verifier.Verifier verifier ⦄
    → verifier → List LedgerInfoWithSignatures
    → Either ErrLog Unit
  loop verifierRef = λ where
    [] → pure unit
    (liws ∷ liwss) → do
      Verifier.verify verifierRef liws
      verifierRef' ← case liws ^∙ liwsLedgerInfo ∙ liNextEpochState of λ where
        nothing   → Left fakeErr -- ["empty ValidatorSet"]
        (just vs) → pure vs
      loop verifierRef' liwss

  here' : List String → List String
  here' t = "EpochChangeProof" ∷ "verify" ∷ t

  last : ∀ {A : Set} → List A → Either ErrLog A
  last          []  = Left fakeErr
  last     (x ∷ []) = Right x
  last (_ ∷ x ∷ xs) = last xs


text:
------------------------------------------------------------------------------
-- The program to sort a list is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of a program which sorts a list
-- by converting it into an ordered tree and then back to a list
-- (Burstall, 1969, p. 45).

module FOTC.Program.SortList.CorrectnessProofATP where

open import FOTC.Base
open import FOTC.Data.Nat.List.Type
open import FOTC.Program.SortList.PropertiesATP
open import FOTC.Program.SortList.Properties.Totality.TreeATP
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- Main theorem: The sort program generates an ordered list.
postulate sortCorrect : ∀ {is} → ListN is → OrdList (sort is)
{-# ATP prove sortCorrect flatten-OrdList makeTree-Tree makeTree-OrdTree #-}

------------------------------------------------------------------------------
-- References
--
-- Burstall, R. M. (1969). Proving properties of programs by
-- structural induction. The Computer Journal 12.1, pp. 41–48.


text:
module Builtin.Coinduction where

open import Agda.Builtin.Coinduction public

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax TLC | Λ

type
  N   : 0-ary
  _↣_ : 2-ary | r30
  𝟙   : 0-ary
  _⊗_ : 2-ary | l40
  𝟘   : 0-ary
  _⊕_ : 2-ary | l30

term
  app   : α ↣ β  α  ->  β | _$_ l20
  lam   : α.β  ->  α ↣ β | ƛ_ r10
  unit  : 𝟙
  pair  : α  β  ->  α ⊗ β | ⟨_,_⟩
  fst   : α ⊗ β  ->  α
  snd   : α ⊗ β  ->  β
  abort : 𝟘  ->  α
  inl   : α  ->  α ⊕ β
  inr   : β  ->  α ⊕ β
  case  : α ⊕ β  α.γ  β.γ  ->  γ
  ze    : N
  su    : N  ->  N
  nrec  : N  α  (α,N).α  ->  α

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
  (𝟙η) u : 𝟙 |> u = unit
  (fβ) a : α  b : β |> fst (pair(a, b))      = a
  (sβ) a : α  b : β |> snd (pair(a, b))      = b
  (pη) p : α ⊗ β    |> pair (fst(p), snd(p)) = p
  (𝟘η) e : 𝟘  c : α |> abort(e) = c
  (lβ) a : α   f : α.γ  g : β.γ |> case (inl(a), x.f[x], y.g[y])      = f[a]
  (rβ) b : β   f : α.γ  g : β.γ |> case (inr(b), x.f[x], y.g[y])      = g[b]
  (cη) s : α ⊕ β  c : (α ⊕ β).γ |> case (s, x.c[inl(x)], y.c[inr(y)]) = c[s]
  (zeβ) z : α   s : (α,N).α        |> nrec (ze,       z, r m. s[r,m]) = z
  (suβ) z : α   s : (α,N).α  n : N |> nrec (su (n), z, r m. s[r,m]) = s[nrec (n, z, r m. s[r,m]), n]
  (ift) t f : α |> if (true, t, f) = t
  (iff) t f : α |> if (false, t, f) = f
-}

module TLC.Signature where

open import SOAS.Context

-- Type declaration
data ΛT : Set where
  N   : ΛT
  _↣_ : ΛT → ΛT → ΛT
  𝟙   : ΛT
  _⊗_ : ΛT → ΛT → ΛT
  𝟘   : ΛT
  _⊕_ : ΛT → ΛT → ΛT
infixr 30 _↣_
infixl 40 _⊗_
infixl 30 _⊕_

-- Derived types
B : ΛT
B = 𝟙 ⊕ 𝟙

open import SOAS.Syntax.Signature ΛT public
open import SOAS.Syntax.Build ΛT public

-- Operator symbols
data Λₒ : Set where
  appₒ lamₒ pairₒ fstₒ sndₒ inlₒ inrₒ : {α β : ΛT} → Λₒ
  unitₒ zeₒ suₒ : Λₒ
  abortₒ nrecₒ : {α : ΛT} → Λₒ
  caseₒ : {α β γ : ΛT} → Λₒ

-- Term signature
Λ:Sig : Signature Λₒ
Λ:Sig = sig λ
  { (appₒ   {α}{β})    → (⊢₀ α ↣ β) , (⊢₀ α) ⟼₂ β
  ; (lamₒ   {α}{β})    → (α ⊢₁ β) ⟼₁ α ↣ β
  ;  unitₒ             → ⟼₀ 𝟙
  ; (pairₒ  {α}{β})    → (⊢₀ α) , (⊢₀ β) ⟼₂ α ⊗ β
  ; (fstₒ   {α}{β})    → (⊢₀ α ⊗ β) ⟼₁ α
  ; (sndₒ   {α}{β})    → (⊢₀ α ⊗ β) ⟼₁ β
  ; (abortₒ {α})       → (⊢₀ 𝟘) ⟼₁ α
  ; (inlₒ   {α}{β})    → (⊢₀ α) ⟼₁ α ⊕ β
  ; (inrₒ   {α}{β})    → (⊢₀ β) ⟼₁ α ⊕ β
  ; (caseₒ  {α}{β}{γ}) → (⊢₀ α ⊕ β) , (α ⊢₁ γ) , (β ⊢₁ γ) ⟼₃ γ
  ;  zeₒ               → ⟼₀ N
  ;  suₒ               → (⊢₀ N) ⟼₁ N
  ; (nrecₒ  {α})       → (⊢₀ N) , (⊢₀ α) , (α , N ⊢₂ α) ⟼₃ α
  }

open Signature Λ:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- A discussion from -- https://twitter.com/YuumuKonpaku/status/1052959340468953088

module MdJustHighlightAgdaAsHtml where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Primitive public using (lzero)
  renaming (Level to ULevel; lsuc to lsucc; _⊔_ to lmax)

Type : (i : ULevel) -> Set (lsucc i)
Type i = Set i

data ⊥ : Type lzero where
pattern O = zero
pattern S n = (suc n)
variable i : ULevel

¬ : (A : Type i) → Type i
¬ A = A → ⊥
_≠_ : {A : Type i} → (A → A → Type i)
x ≠ y = ¬ (x ≡ y)

infix 10 _∨_
data _∨_ {a b} (A : Type a) (B : Type b) : Set (lmax a b) where
  a-intro : A -> A ∨ B
  b-intro : B -> A ∨ B

test : (x y : Nat) -> (x ≡ y) ∨ (x ≠ y)
test O O = a-intro refl
test O (S y) = b-intro (λ ())
test (S x) O = b-intro (λ ())
test (S x) (S y) with test x y
... | a-intro refl = a-intro refl
... | b-intro k = b-intro (lemma k)
  where
    lemma : {a b : Nat} -> a ≠ b -> S a ≠ S b
    lemma p refl = p refl

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda