text:
module Integer8 where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Relation.Binary.PropositionalEquality as PropEq

-- ---------- record ----------
record IsSemiGroup (A : Set) (_∙_ : A → A → A) : Set where
  field
    assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
record IsMonoid (A : Set) (_∙_ : A → A → A) (e : A) : Set where
  field
    isSemiGroup : IsSemiGroup A _∙_
    identity : (∀ x → e ∙ x ≡ x) × (∀ x → x ∙ e ≡ x)
record IsGroup (A : Set) (_∙_ : A → A → A) (e : A) (iF : A → A) : Set where
  field
    isMonoid : IsMonoid A _∙_ e
    inv : (∀ x → (iF x) ∙ x ≡ e) × (∀ x → x ∙ (iF x) ≡ e)
record IsAbelianGroup (A : Set) (_∙_ : A → A → A) (e : A) (iF : A → A) : Set where
  field
    isGroup : IsGroup A _∙_ e iF
    comm : ∀ x y → x ∙ y ≡ y ∙ x
record IsRing (A : Set) (_⊕_ _⊗_ : A → A → A) (eP eT : A) (iF : A → A) : Set where
  field
    ⊕isAbelianGroup : IsAbelianGroup A _⊕_ eP iF
    ⊗isMonoid : IsMonoid A _⊗_ eT
    isDistR : (x y z : A) → (x ⊕ y) ⊗ z ≡ (x ⊗ z) ⊕ (y ⊗ z)
    isDistL : (x y z : A) → x ⊗ (y ⊕ z) ≡ (x ⊗ y) ⊕ (x ⊗ z)
-- ----------------------------

-- ---------- practice nat ----------
ℕ+-isSemiGroup : IsSemiGroup ℕ _+_
ℕ+-isSemiGroup = record { assoc = ℕ+-assoc }
  where
    ℕ+-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
    ℕ+-assoc zero y z = refl
    ℕ+-assoc (suc x) y z = cong suc (ℕ+-assoc x y z)

ℕ+0-isMonoid : IsMonoid ℕ _+_ 0
ℕ+0-isMonoid = record { isSemiGroup = ℕ+-isSemiGroup ; identity = (0+x≡x , x+0≡x) }
  where
    0+x≡x : ∀ x → 0 + x ≡ x
    0+x≡x x = refl
    x+0≡x : ∀ x → x + 0 ≡ x
    x+0≡x zero = refl
    x+0≡x (suc x) = cong suc (x+0≡x x)
-- -------------------------

-- ---------- Int ----------
data ℤ : Set where
  O : ℤ
  I : ℕ → ℕ → ℤ
postulate
  zeroZ : (x : ℕ) → I x x ≡ O
  zeroZ₂ : (x y : ℕ) → I (x + y) (y + x) ≡ O
-- plusInt
_++_ : ℤ → ℤ → ℤ
O ++ O = O
O ++ X = X
X ++ O = X
I x y ++ I z w = I (x + z) (y + w)
-- productInt
_**_ : ℤ → ℤ → ℤ
O ** O = O
O ** _ = O
_ ** O = O
I x y ** I z w = I (x * z + y * w) (x * w + y * z)
-- -------------------------

-- ---------- Int + ----------
ℤ++-isSemiGroup : IsSemiGroup ℤ _++_
ℤ++-isSemiGroup = record { assoc = ℤ++-assoc }
  where
    open IsSemiGroup
    ℤ++-assoc : ∀ x y z → (x ++ y) ++ z ≡ x ++ (y ++ z)
    ℤ++-assoc O O O = refl
    ℤ++-assoc O O (I x x₁) = refl
    ℤ++-assoc O (I x x₁) O = refl
    ℤ++-assoc O (I x x₁) (I x₂ x₃) = refl
    ℤ++-assoc (I x x₁) O O = refl
    ℤ++-assoc (I x x₁) O (I x₂ x₃) = refl
    ℤ++-assoc (I x x₁) (I x₂ x₃) O = refl
    ℤ++-assoc (I x x₁) (I x₂ x₃) (I x₄ x₅)
      = cong₂ I ((assoc ℕ+-isSemiGroup) x x₂ x₄) ((assoc ℕ+-isSemiGroup) x₁ x₃ x₅)

ℤ++O-isMonoid : IsMonoid ℤ _++_ O
ℤ++O-isMonoid = record { isSemiGroup = ℤ++-isSemiGroup ; identity = (O++x≡x , x++O≡x) }
  where
    O++x≡x : (x : ℤ) → (O ++ x) ≡ x
    O++x≡x O = refl
    O++x≡x (I x x₁) = refl
    x++O≡x : (x : ℤ) → (x ++ O) ≡ x
    x++O≡x O = refl
    x++O≡x (I x x₁) = refl

invℤ : ℤ → ℤ
invℤ O = O
invℤ (I x x₁) = I x₁ x
ℤ++Oinvℤ-isGroup : IsGroup ℤ _++_ O invℤ
ℤ++Oinvℤ-isGroup = record { isMonoid = ℤ++O-isMonoid ; inv = (leftInv , rightInv) }
  where
    leftInv : (x : ℤ) → (invℤ x ++ x) ≡ O
    leftInv O = refl
    leftInv (I x x₁) = zeroZ₂ x₁ x
    rightInv : (x : ℤ) → (x ++ invℤ x) ≡ O
    rightInv O = refl
    rightInv (I x x₁) = zeroZ₂ x x₁

ℤ++Oinvℤ-isAbelianGroup : IsAbelianGroup ℤ _++_ O invℤ
ℤ++Oinvℤ-isAbelianGroup = record { isGroup = ℤ++Oinvℤ-isGroup ; comm = ℤ++Oinvℤ-Comm }
  where
    ℤ++Oinvℤ-Comm : (x y : ℤ) → (x ++ y) ≡ (y ++ x)
    ℤ++Oinvℤ-Comm O O = refl
    ℤ++Oinvℤ-Comm O (I x x₁) = refl
    ℤ++Oinvℤ-Comm (I x x₁) O = refl
    ℤ++Oinvℤ-Comm (I x x₁) (I x₂ x₃) = cong₂ I (+-comm x x₂) (+-comm x₁ x₃)
-- ---------------------------

-- ---------- Int * ----------
ℤ**-isSemiGroup : IsSemiGroup ℤ _**_
ℤ**-isSemiGroup = record { assoc = ℤ**-assoc }
  where
    ℤ**-assoc : ∀ x y z → (x ** y) ** z ≡ x ** (y ** z)
    ℤ**-assoc O O O = refl
    ℤ**-assoc O O (I x x₁) = refl
    ℤ**-assoc O (I x x₁) O = refl
    ℤ**-assoc O (I x x₁) (I x₂ x₃) = refl
    ℤ**-assoc (I x x₁) O O = refl
    ℤ**-assoc (I x x₁) O (I x₂ x₃) = refl
    ℤ**-assoc (I x x₁) (I x₂ x₃) O = refl
    ℤ**-assoc (I x x₁) (I x₂ x₃) (I x₄ x₅)
      = cong₂ I (ℤ**-assoc₁ x x₁ x₂ x₃ x₄ x₅) (ℤ**-assoc₁ x x₁ x₂ x₃ x₅ x₄)
      where
        open PropEq.≡-Reasoning
        open IsSemiGroup
        ℤ**-assoc₁ : ∀ x y z u v w →
          (x * z + y * u) * v + (x * u + y * z) * w ≡ x * (z * v + u * w) + y * (z * w + u * v)
        ℤ**-assoc₁ x y z u v w = begin
            (x * z + y * u) * v + (x * u + y * z) * w
          ≡⟨ cong (\ t → (t + (x * u + y * z) * w)) (*-distribʳ-+ v (x * z) (y * u)) ⟩
            x * z * v + y * u * v + (x * u + y * z) * w
          ≡⟨ cong (\ t → (x * z * v + y * u * v + t)) (*-distribʳ-+ w (x * u) (y * z)) ⟩
            x * z * v + y * u * v + (x * u * w + y * z * w)
          ≡⟨ +-assoc (x * z * v) (y * u * v) (x * u * w + y * z * w) ⟩
            x * z * v + (y * u * v + (x * u * w + y * z * w))
          ≡⟨ cong (\ t → ((x * z * v) + t)) (+-comm (y * u * v) (x * u * w + y * z * w)) ⟩
            x * z * v + ((x * u * w + y * z * w) + y * u * v)
          ≡⟨ sym (+-assoc (x * z * v) (x * u * w + y * z * w) (y * u * v)) ⟩
            x * z * v + (x * u * w + y * z * w) + y * u * v
          ≡⟨ sym (cong (\ t → (t + y * u * v)) ((assoc ℕ+-isSemiGroup) (x * z * v) (x * u * w) (y * z * w))) ⟩
            x * z * v + x * u * w + y * z * w + y * u * v
          ≡⟨ cong (\ t → t + x * u * w + y * z * w + y * u * v) (*-assoc x z v) ⟩
            x * (z * v) + x * u * w + y * z * w + y * u * v
          ≡⟨ cong (\ t → x * (z * v) + t + y * z * w + y * u * v) (*-assoc x u w) ⟩
            x * (z * v) + x * (u * w) + y * z * w + y * u * v
          ≡⟨ cong (\ t → x * (z * v) + x * (u * w) + t + y * u * v) (*-assoc y z w) ⟩
            x * (z * v) + x * (u * w) + y * (z * w) + y * u * v
          ≡⟨ cong (\ t → x * (z * v) + x * (u * w) + y * (z * w) + t) (*-assoc y u v) ⟩
            x * (z * v) + x * (u * w) + y * (z * w) + y * (u * v)
          ≡⟨ sym (cong (\ t → (t + y * (z * w) + y * (u * v))) (*-distribˡ-+ x (z * v) (u * w))) ⟩
            x * (z * v + u * w) + y * (z * w) + y * (u * v)
          ≡⟨ +-assoc (x * (z * v + u * w)) (y * (z * w))  (y * (u * v)) ⟩
            x * (z * v + u * w) + (y * (z * w) + y * (u * v))
          ≡⟨ sym (cong (\ t → (x * (z * v + u * w) + t)) (*-distribˡ-+ y (z * w) (u * v))) ⟩
            x * (z * v + u * w) + y * (z * w + u * v)
          ∎

ℤ**1-isMonoid : IsMonoid ℤ _**_ (I 1 0)
ℤ**1-isMonoid = record { isSemiGroup = ℤ**-isSemiGroup ; identity = (1**x≡x , x**1≡x) }
  where
    1**x≡x : (x : ℤ) → (I 1 0 ** x) ≡ x
    1**x≡x O = refl
    1**x≡x (I x x₁) = cong₂ I (x+z+z≡x x) (x+z+z≡x x₁)
      where
        x+z+z≡x : (x : ℕ) → x + 0 + 0 ≡ x
        x+z+z≡x zero = refl
        x+z+z≡x (suc x) = cong suc (x+z+z≡x x)
    x**1≡x : (x : ℤ) → (x ** I 1 0) ≡ x
    x**1≡x O = refl
    x**1≡x (I x x₁) = cong₂ I (x*1+x*0≡x x x₁) (x*0+x*1=x x x₁)
      where
        x*1+x*0≡x : (x x₁ : ℕ) → x * 1 + x₁ * 0 ≡ x
        x*1+x*0≡x zero zero = refl
        x*1+x*0≡x zero (suc x₁) = x*1+x*0≡x zero x₁
        x*1+x*0≡x (suc x) zero = cong suc (x*1+x*0≡x x zero)
        x*1+x*0≡x (suc x) (suc x₁) = x*1+x*0≡x (suc x) x₁
        x*0+x*1=x : (x x₁ : ℕ) → x * 0 + x₁ * 1 ≡ x₁
        x*0+x*1=x zero zero = refl
        x*0+x*1=x zero (suc x₁) = cong suc (x*0+x*1=x zero x₁)
        x*0+x*1=x (suc x) zero = x*0+x*1=x x zero
        x*0+x*1=x (suc x) (suc x₁) = x*0+x*1=x x (suc x₁)
-- ---------------------------

-- ---------- Int + * ----------
ℤ++0invℤ-**1-isRing : IsRing ℤ _++_ _**_ O (I 1 0) invℤ
ℤ++0invℤ-**1-isRing =
  record
    { ⊕isAbelianGroup = ℤ++Oinvℤ-isAbelianGroup
    ; ⊗isMonoid = ℤ**1-isMonoid
    ; isDistR = ℤdistR
    ; isDistL = ℤdistL }
    where
      ℤdistR : (x y z : ℤ) → (x ++ y) ** z ≡ (x ** z) ++ (y ** z)
      ℤdistR O O O = refl
      ℤdistR O O (I x x₁) = refl
      ℤdistR O (I x x₁) O = refl
      ℤdistR O (I x x₁) (I x₂ x₃) = refl
      ℤdistR (I x x₁) O O = refl
      ℤdistR (I x x₁) O (I x₂ x₃) = refl
      ℤdistR (I x x₁) (I x₂ x₃) O = refl
      ℤdistR (I x x₁) (I x₂ x₃) (I x₄ x₅) = cong₂ I (ℤdistR₁ x x₂ x₄ x₁ x₃ x₅) (ℤdistR₁ x x₂ x₅ x₁ x₃ x₄)
        where
          open PropEq.≡-Reasoning
          open IsSemiGroup
          ℤdistR₁ : (x y z u v w : ℕ) →
            (x + y) * z + (u + v) * w ≡ x * z + u * w + (y * z + v * w)
          ℤdistR₁ x y z u v w = begin
              (x + y) * z + (u + v) * w
            ≡⟨ cong (\ t → t + (u + v) * w) (*-distribʳ-+ z x y) ⟩
               x * z + y * z + (u + v) * w
            ≡⟨ cong (\ t → (x * z + y * z + t)) (*-distribʳ-+ w u v) ⟩
               x * z + y * z + (u * w + v * w)
            ≡⟨ +-assoc (x * z) (y * z) (u * w + v * w) ⟩
               x * z + (y * z + (u * w + v * w))
            ≡⟨ cong (\ t → x * z + t) (+-comm (y * z) (u * w + v * w)) ⟩
               x * z + ((u * w + v * w) + y * z)
            ≡⟨ cong (\ t → x * z + t) ((assoc ℕ+-isSemiGroup) (u * w) (v * w) (y * z)) ⟩
               x * z + (u * w + (v * w + y * z))
            ≡⟨ cong (\ t → x * z + (u * w + t)) (+-comm (v * w) (y * z)) ⟩
               x * z + (u * w + (y * z + v * w))
            ≡⟨ sym ((assoc ℕ+-isSemiGroup) (x * z) (u * w) (y * z + v * w)) ⟩
               x * z + u * w + (y * z + v * w)
            ∎
      ℤdistL : (x y z : ℤ) → x ** (y ++ z) ≡ (x ** y) ++ (x ** z)
      ℤdistL O O O = refl
      ℤdistL O O (I x x₁) = refl
      ℤdistL O (I x x₁) O = refl
      ℤdistL O (I x x₁) (I x₂ x₃) = refl
      ℤdistL (I x x₁) O O = refl
      ℤdistL (I x x₁) O (I x₂ x₃) = refl
      ℤdistL (I x x₁) (I x₂ x₃) O = refl
      ℤdistL (I x x₁) (I x₂ x₃) (I x₄ x₅) = cong₂ I (ℤdistL₁ x x₁ x₂ x₃ x₄ x₅) (ℤdistL₁ x x₁ x₃ x₂ x₅ x₄)
        where
          open PropEq.≡-Reasoning
          open IsSemiGroup
          ℤdistL₁ : (x y z u v w : ℕ) →
            x * (z + v) + y * (u + w) ≡ x * z + y * u + (x * v + y * w)
          ℤdistL₁ x y z u v w = begin
               x * (z + v) + y * (u + w)
            ≡⟨ cong (\ t → t + y * (u + w)) (*-distribˡ-+ x z v) ⟩
               x * z + x * v + y * (u + w)
            ≡⟨ cong (\ t → x * z + x * v + t) (*-distribˡ-+ y u w) ⟩
               x * z + x * v + (y * u + y * w)
            ≡⟨ +-assoc (x * z) (x * v) (y * u + y * w) ⟩
               x * z + (x * v + (y * u + y * w))
            ≡⟨ sym (cong (\ t → x * z + t) ((assoc ℕ+-isSemiGroup) (x * v) (y * u) (y * w))) ⟩
               x * z + ((x * v + y * u) + y * w)
            ≡⟨ cong (\ t → x * z + (t + y * w)) (+-comm (x * v) (y * u)) ⟩
               x * z + ((y * u + x * v) + y * w)
            ≡⟨ cong (\ t → x * z + t) ((assoc ℕ+-isSemiGroup) (y * u) (x * v) (y * w)) ⟩
               x * z + (y * u + (x * v + y * w))
            ≡⟨ sym ((assoc ℕ+-isSemiGroup) (x * z) (y * u) (x * v + y * w)) ⟩
               x * z + y * u + (x * v + y * w)
            ∎
-- ---------------------------

-- (-1) * (-1) = 1
minus : I 0 1 ** I 0 1 ≡ I 1 0
minus = refl


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat

{-# BUILTIN REWRITE _≡_ #-}

not : Bool → Bool
not true = false
not false = true

data Unit : Set where
  unit : Unit

postulate
  X : Unit → Set
  X-Nat : X unit ≡ Nat
  X-Bool : (u : Unit) → X u ≡ Bool
{-# REWRITE X-Nat #-}

0' : (u : Unit) → X u
0' unit = 0

{-# REWRITE X-Bool #-}

test : (u : Unit) → not (0' u) ≡ true
test unit = refl

ext: agda

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
open import Data.String using ( _++_ )
open import System.IO using ( _>>_ ; _>>=_ ; getStr ; putStr ; commit )

module System.IO.Examples.HelloUser where

main =
  putStr "What is your name?\n" >>
  commit >>
  getStr >>= λ name →
  putStr ("Hello, " ++ name ++ "\n") >>
  commit

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
{-

        Agda Implementors' Meeting VI

                  Göteborg
             May 24 - 30, 2007

                Hello Agda!

                Ulf Norell

-}

-- This is where the fun begins.
-- Unleashing datatypes, pattern matching and recursion.

module Datatypes where

{-

  Simple datatypes.

-}

-- Now which datatype should we start with...?

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

-- Let's start simple.
pred : Nat -> Nat
pred zero    = zero
pred (suc n) = n

-- Now let's do recursion.
_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

-- An aside on infix operators:
-- Any name containing _ can be used as a mixfix operator.
-- The arguments simply go in place of the _. For instance:

data Bool : Set where
  true  : Bool
  false : Bool

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

-- To declare the associativity and precedence of an operator
-- we write. In this case we need parenthesis around the else branch
-- if its precedence is lower than 10. For the condition and the then
-- branch we only need parenthesis for things like λs.
infix 10 if_then_else_

{-

  Parameterised datatypes

-}

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

infixr 50 _::_

-- The parameters are implicit arguments to the constructors.
nil : (A : Set) -> List A
nil A = [] {A}

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

{-

  Empty datatypes

-}

-- A very useful guy is the empty datatype.
data False : Set where

-- When pattern matching on an element of an empty type, something
-- interesting happens:

elim-False : {A : Set} -> False -> A
elim-False ()  -- Look Ma, no right hand side!

-- The pattern () is called an absurd pattern and matches elements
-- of an empty type.

{-

  What's next?

-}

-- Fun as they are, eventually you'll get bored with
-- inductive datatypes.

-- Move on to: Families.agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Numbers.Naturals.Semiring
open import Groups.FreeProduct.Definition
open import Groups.FreeProduct.Setoid
open import Groups.FreeProduct.Group
open import Groups.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Isomorphisms.Definition
open import LogicalFormulae
open import Numbers.Integers.Addition
open import Numbers.Integers.Definition
open import Groups.FreeGroup.Definition
open import Groups.FreeGroup.Word
open import Groups.FreeGroup.Group
open import Groups.FreeGroup.UniversalProperty
open import Setoids.Setoids

module Groups.FreeProduct.Lemmas {i : _} {I : Set i} (decidableIndex : (x y : I) → ((x ≡ y) || ((x ≡ y) → False))) where

private
  f : ReducedWord decidableIndex → ReducedSequence decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)
  f = universalPropertyFunction decidableIndex (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)) λ i → nonempty i (ofEmpty i (nonneg 1) λ ())

  freeProductIso : GroupHom (freeGroup decidableIndex) (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)) f
  freeProductIso = universalPropertyHom decidableIndex (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)) (λ i → nonempty i (ofEmpty i (nonneg 1) λ ()))

  freeProductInj : (x y : ReducedWord decidableIndex) → (decidableIndex =RP λ _ → ℤDecideEquality) (λ _ → ℤGroup) (f x) (f y) → x ≡ y
  freeProductInj empty empty pr = refl
  freeProductInj empty (prependLetter (ofLetter x₁) y x) pr = exFalso {!!}
  freeProductInj empty (prependLetter (ofInv x₁) y x) pr = {!!}
  freeProductInj (prependLetter letter x x₁) y pr = {!!}

freeProductZ : GroupsIsomorphic (freeGroup decidableIndex) (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup))
GroupsIsomorphic.isomorphism (freeProductZ) = universalPropertyFunction decidableIndex (FreeProductGroup decidableIndex (λ _ → ℤDecideEquality) (λ _ → ℤGroup)) λ i → nonempty i (ofEmpty i (nonneg 1) λ ())
GroupIso.groupHom (GroupsIsomorphic.proof (freeProductZ)) = freeProductIso
SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) = GroupHom.wellDefined (freeProductIso)
SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {x} {y} = freeProductInj x y
SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) = GroupHom.wellDefined freeProductIso
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {empty} = empty , record {}
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {nonempty i (ofEmpty .i (nonneg zero) nonZero)} = exFalso (nonZero refl)
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {nonempty i (ofEmpty .i (nonneg (succ x)) nonZero)} = prependLetter (ofLetter i) empty (wordEmpty refl) , {!!}
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {nonempty i (ofEmpty .i (negSucc x) nonZero)} = {!!}
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeProductZ)))) {nonempty i (prependLetter .i g nonZero x x₁)} = {!!}

freeProductNonAbelian : {!!}
freeProductNonAbelian = {!!}


text:
module Issue121 where

bad : Set → Set
bad A = A → A

data Bool : Set where
  true  : Bool
  false : Bool

F : Bool → Set → Set
F true  = bad
F false = λ A → A

data D : Set where
  nop : (b : Bool) → F b D → D

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Relation.Binary.Core

module PLRTree.Insert.Permutation {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_) where

open import Data.List
open import Data.Product renaming (_×_ to _∧_)
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import PLRTree {A}
open import PLRTree.Complete {A}
open import PLRTree.Compound {A}
open import PLRTree.Insert _≤_ tot≤
open import PLRTree.Insert.Properties _≤_ tot≤

mutual
  lemma-insert-/ : {t : PLRTree}(x : A) → Complete t → ∃ (λ xs → flatten (insert x t) / x ⟶ xs ∧ xs ∼ flatten t)
  lemma-insert-/ x leaf = [] , /head , ∼[]
  lemma-insert-/ x (perfect {l} {r} y cl _ l≃r)
      with tot≤ x y | l | r | l≃r
  ... | inj₁ x≤y | leaf | leaf | _  = y ∷ [] , /head , refl∼
  ... | inj₁ x≤y | leaf | node _ _ _ _ | ()
  ... | inj₁ x≤y | node perfect _ _ _ | leaf | ()
  ... | inj₁ x≤y | node perfect y' l' r' | node perfect y'' l'' r'' | _ =
                  let _l = node perfect y' l' r' ;
                       _r = node perfect y'' l'' r'' ;
                       flᵢfr∼yflfr = lemma++∼r (lemma-insert-∼ y cl)
                  in flatten (insert y _l) ++ flatten _r , /head , flᵢfr∼yflfr
  ... | inj₁ x≤y | node perfect _ _ _ | node left _ _ _ | ()
  ... | inj₁ x≤y | node perfect _ _ _ | node right _ _ _ | ()
  ... | inj₁ x≤y | node left _ _ _ | _ | ()
  ... | inj₁ x≤y | node right _ _ _ | _ | ()
  ... | inj₂ y≤x | leaf | leaf | _  = y ∷ [] , /tail /head , refl∼
  ... | inj₂ y≤x | leaf | node _ _ _ _ | ()
  ... | inj₂ y≤x | node perfect _ _ _ | leaf | ()
  ... | inj₂ y≤x | node perfect y' l' r' | node perfect y'' l'' r'' | _
      with lemma-insert-/ x cl
  ... | xs , flᵢ/x⟶xs , xs∼fl =
                  let _l = node perfect y' l' r' ;
                       _r = node perfect y'' l'' r'' ;
                       yflᵢfr/x⟶yxsfr = /tail (lemma++/r flᵢ/x⟶xs) ;
                       yflᵢfr∼yxsfr = ∼x /head /head (lemma++∼r xs∼fl)
                  in y ∷  xs ++ flatten _r , yflᵢfr/x⟶yxsfr , yflᵢfr∼yxsfr
  lemma-insert-/ x (perfect y cl _ l≃r) | inj₂ y≤x | node perfect _ _ _ | node left _ _ _ | ()
  lemma-insert-/ x (perfect y cl _ l≃r) | inj₂ y≤x | node perfect _ _ _ | node right _ _ _ | ()
  lemma-insert-/ x (perfect y cl _ l≃r) | inj₂ y≤x | node left _ _ _ | _ | ()
  lemma-insert-/ x (perfect y cl _ l≃r) | inj₂ y≤x | node right _ _ _ | _ | ()
  lemma-insert-/ x (left {l} {r} y cl _ _)
      with tot≤ x y
  ... | inj₁ x≤y
      with insert y l | lemma-insert-∼ y cl | lemma-insert-compound y l
  ... | node perfect y' l' r' | flᵢ∼yfl | compound =
                  let flᵢfr∼yflfr = lemma++∼r flᵢ∼yfl
                  in flatten (node perfect y' l' r') ++ flatten r , /head , flᵢfr∼yflfr
  ... | node left y' l' r' | flᵢ∼yfl | compound =
                  let flᵢfr∼yflfr = lemma++∼r flᵢ∼yfl
                  in flatten (node left y' l' r') ++ flatten r , /head , flᵢfr∼yflfr
  ... | node right y' l' r' | flᵢ∼yfl | compound =
                  let flᵢfr∼yflfr = lemma++∼r flᵢ∼yfl
                  in flatten (node right y' l' r') ++ flatten r , /head , flᵢfr∼yflfr
  lemma-insert-/ x (left {l} {r} y cl _ _) | inj₂ y≤x
      with insert x l | lemma-insert-/ x cl | lemma-insert-compound x l
  ... | node perfect _ _ _ | xs , flᵢ/x⟶xs , xs∼fl | compound =
                  let yflᵢfr/x⟶yxsfr = /tail (lemma++/r flᵢ/x⟶xs) ;
                       yflᵢfr∼yxsfr = ∼x /head /head (lemma++∼r xs∼fl)
                  in y ∷  xs ++ flatten r , yflᵢfr/x⟶yxsfr , yflᵢfr∼yxsfr
  ... | node left _ _ _ | xs , flᵢ/x⟶xs , xs∼fl | compound =
                  let yflᵢfr/x⟶yxsfr = /tail (lemma++/r flᵢ/x⟶xs) ;
                       yflᵢfr∼yxsfr = ∼x /head /head (lemma++∼r xs∼fl)
                  in y ∷  xs ++ flatten r , yflᵢfr/x⟶yxsfr , yflᵢfr∼yxsfr
  ... | node right _ _ _ | xs , flᵢ/x⟶xs , xs∼fl | compound =
                  let yflᵢfr/x⟶yxsfr = /tail (lemma++/r flᵢ/x⟶xs) ;
                       yflᵢfr∼yxsfr = ∼x /head /head (lemma++∼r xs∼fl)
                  in y ∷  xs ++ flatten r , yflᵢfr/x⟶yxsfr , yflᵢfr∼yxsfr
  lemma-insert-/ x (right {l} {r} y _ cr _)
    with tot≤ x y
  ... | inj₁ x≤y
      with insert y r | lemma-insert-∼ y cr | lemma-insert-compound y r
  ... | node perfect y' l' r' | frᵢ∼yfr | compound =
                  let flfrᵢ∼flyfr = lemma++∼l {flatten l} frᵢ∼yfr ;
                       flyfr∼yflfr = ∼x (lemma++/ {y} {flatten l}) /head refl∼ ;
                       flfrᵢ∼yflfr = trans∼ flfrᵢ∼flyfr flyfr∼yflfr
                  in flatten l ++ flatten (node perfect y' l' r') , /head , flfrᵢ∼yflfr
  ... | node left y' l' r' | frᵢ∼yfr | compound =
                  let flfrᵢ∼flyfr = lemma++∼l {flatten l} frᵢ∼yfr ;
                       flyfr∼yflfr = ∼x (lemma++/ {y} {flatten l}) /head refl∼ ;
                       flfrᵢ∼yflfr = trans∼ flfrᵢ∼flyfr flyfr∼yflfr
                  in flatten l ++ flatten (node left y' l' r') , /head , flfrᵢ∼yflfr
  ... | node right y' l' r' | frᵢ∼yfr | compound =
                  let flfrᵢ∼flyfr = lemma++∼l {flatten l} frᵢ∼yfr ;
                       flyfr∼yflfr = ∼x (lemma++/ {y} {flatten l}) /head refl∼ ;
                       flfrᵢ∼yflfr = trans∼ flfrᵢ∼flyfr flyfr∼yflfr
                  in flatten l ++ flatten (node right y' l' r') , /head , flfrᵢ∼yflfr
  lemma-insert-/ x (right {l} {r} y _ cr _) | inj₂ y≤x
      with insert x r | lemma-insert-/ x cr | lemma-insert-compound x r
  ... | node perfect y' l' r' | xs , frᵢ/x⟶xs , xs∼fr | compound =
                  let yflfrᵢ/x⟶yflxs = /tail (lemma++/l {x} {flatten l} frᵢ/x⟶xs) ;
                       yflfrᵢ∼yflxs = ∼x /head /head (lemma++∼l {flatten l} xs∼fr)
                  in y ∷  flatten l ++ xs , yflfrᵢ/x⟶yflxs , yflfrᵢ∼yflxs
  ... | node left y' l' r' | xs , frᵢ/x⟶xs , xs∼fr | compound =
                  let yflfrᵢ/x⟶yflxs = /tail (lemma++/l {x} {flatten l} frᵢ/x⟶xs) ;
                       yflfrᵢ∼yflxs = ∼x /head /head (lemma++∼l {flatten l} xs∼fr)
                  in y ∷  flatten l ++ xs , yflfrᵢ/x⟶yflxs , yflfrᵢ∼yflxs
  ... | node right y' l' r' | xs , frᵢ/x⟶xs , xs∼fr | compound =
                  let yflfrᵢ/x⟶yflxs = /tail (lemma++/l {x} {flatten l} frᵢ/x⟶xs) ;
                       yflfrᵢ∼yflxs = ∼x /head /head (lemma++∼l {flatten l} xs∼fr)
                  in y ∷  flatten l ++ xs , yflfrᵢ/x⟶yflxs , yflfrᵢ∼yflxs

  lemma-insert-∼ : {t : PLRTree}(x : A) → Complete t → flatten (insert x t) ∼ (x ∷ flatten t)
  lemma-insert-∼ x leaf = ∼x /head /head ∼[]
  lemma-insert-∼ x (perfect {l} {r} y cl _ l≃r)
      with tot≤ x y | l | r | l≃r
  ... | inj₁ x≤y | leaf | leaf | _  = ∼x /head /head (∼x /head /head ∼[])
  ... | inj₁ x≤y | leaf | node _ _ _ _ | ()
  ... | inj₁ x≤y | node perfect _ _ _ | leaf | ()
  ... | inj₁ x≤y | node perfect _ _ _ | node perfect _ _ _ | _  =
                  let flᵢfr∼yflfr = lemma++∼r (lemma-insert-∼ y cl)
                  in ∼x /head /head flᵢfr∼yflfr
  ... | inj₁ x≤y | node perfect _ _ _ | node left _ _ _ | ()
  ... | inj₁ x≤y | node perfect _ _ _ | node right _ _ _ | ()
  ... | inj₁ x≤y | node left _ _ _ | _ | ()
  ... | inj₁ x≤y | node right _ _ _ | _ | ()
  ... | inj₂ y≤x | leaf | leaf | _  = ∼x /head (/tail /head) (∼x /head /head ∼[])
  ... | inj₂ y≤x | leaf | node _ _ _ _ | ()
  ... | inj₂ y≤x | node perfect _ _ _ | leaf | ()
  ... | inj₂ y≤x | node perfect _ _ _ | node perfect _ _ _ | _
      with lemma-insert-/ x cl
  ... | xs , flᵢ/x⟶xs , xs∼fl =
                  let yflᵢfr/x⟶yxsfr = /tail (lemma++/r flᵢ/x⟶xs) ;
                       yxsfr∼yflfr = ∼x /head /head (lemma++∼r xs∼fl)
                  in ∼x yflᵢfr/x⟶yxsfr /head yxsfr∼yflfr
  lemma-insert-∼ x (perfect y cl _ l≃r) | inj₂ y≤x | node perfect _ _ _ | node left _ _ _ | ()
  lemma-insert-∼ x (perfect y cl _ l≃r) | inj₂ y≤x | node perfect _ _ _ | node right _ _ _ | ()
  lemma-insert-∼ x (perfect y cl _ l≃r) | inj₂ y≤x | node left _ _ _ | _ | ()
  lemma-insert-∼ x (perfect y cl _ l≃r) | inj₂ y≤x | node right _ _ _ | _ | ()
  lemma-insert-∼ x (left {l} {r} y cl _ _)
      with tot≤ x y
  ... | inj₁ x≤y
      with insert y l | lemma-insert-∼ y cl | lemma-insert-compound y l
  ... | node perfect _ _ _ | flᵢ∼yfl | compound =
                  let flᵢfr∼yflfr = lemma++∼r flᵢ∼yfl
                  in ∼x /head /head flᵢfr∼yflfr
  ... | node left _ _ _ | flᵢ∼yfl | compound =
                  let flᵢfr∼yflfr = lemma++∼r flᵢ∼yfl
                  in ∼x /head /head flᵢfr∼yflfr
  ... | node right _ _ _ | flᵢ∼yfl | compound =
                  let flᵢfr∼yflfr = lemma++∼r flᵢ∼yfl
                  in ∼x /head /head flᵢfr∼yflfr
  lemma-insert-∼ x (left {l} {r} y cl _ _) | inj₂ y≤x
      with insert x l | lemma-insert-/ x cl | lemma-insert-compound x l
  ... | node perfect _ _ _ | xs , flᵢ/x⟶xs , xs∼fl | compound =
                  let yflᵢfr/x⟶yxsfr = /tail (lemma++/r flᵢ/x⟶xs) ;
                       yxsfr∼yflfr = ∼x /head /head (lemma++∼r xs∼fl)
                  in ∼x yflᵢfr/x⟶yxsfr /head yxsfr∼yflfr
  ... | node left _ _ _ | xs , flᵢ/x⟶xs , xs∼fl | compound =
                  let yflᵢfr/x⟶yxsfr = /tail (lemma++/r flᵢ/x⟶xs) ;
                       yxsfr∼yflfr = ∼x /head /head (lemma++∼r xs∼fl)
                  in ∼x yflᵢfr/x⟶yxsfr /head yxsfr∼yflfr
  ... | node right _ _ _ | xs , flᵢ/x⟶xs , xs∼fl | compound =
                  let yflᵢfr/x⟶yxsfr = /tail (lemma++/r flᵢ/x⟶xs) ;
                       yxsfr∼yflfr = ∼x /head /head (lemma++∼r xs∼fl)
                  in ∼x yflᵢfr/x⟶yxsfr /head yxsfr∼yflfr
  lemma-insert-∼ x (right {l} {r} y _ cr _)
      with tot≤ x y
  ... | inj₁ x≤y
      with insert y r | lemma-insert-∼ y cr | lemma-insert-compound y r
  ... | node perfect _ _ _ | frᵢ∼yfr | compound =
                  let flyfr∼yflfr = ∼x (lemma++/ {y} {flatten l}) /head refl∼ ;
                       flfrᵢ∼flyfr = lemma++∼l {flatten l} frᵢ∼yfr ;
                       flfrᵢ∼yflfr = trans∼ flfrᵢ∼flyfr flyfr∼yflfr
                  in ∼x /head /head flfrᵢ∼yflfr
  ... | node left _ _ _ | frᵢ∼yfr | compound =
                  let flyfr∼yflfr = ∼x (lemma++/ {y} {flatten l}) /head refl∼ ;
                       flfrᵢ∼flyfr = lemma++∼l {flatten l} frᵢ∼yfr ;
                       flfrᵢ∼yflfr = trans∼ flfrᵢ∼flyfr flyfr∼yflfr
                  in ∼x /head /head flfrᵢ∼yflfr
  ... | node right _ _ _ | frᵢ∼yfr | compound =
                  let flyfr∼yflfr = ∼x (lemma++/ {y} {flatten l}) /head refl∼ ;
                       flfrᵢ∼flyfr = lemma++∼l {flatten l} frᵢ∼yfr ;
                       flfrᵢ∼yflfr = trans∼ flfrᵢ∼flyfr flyfr∼yflfr
                  in ∼x /head /head flfrᵢ∼yflfr
  lemma-insert-∼ x (right {l} {r} y _ cr _) | inj₂ y≤x
      with insert x r | lemma-insert-/ x cr | lemma-insert-compound x r
  ... | node perfect y' l' r' | xs , frᵢ/x⟶xs , xs∼fr | compound =
                  let yflfrᵢ/x⟶yflxs = /tail (lemma++/l {x} {flatten l} frᵢ/x⟶xs) ;
                       yflxs∼yflfr = ∼x /head /head (lemma++∼l {flatten l} xs∼fr)
                  in ∼x yflfrᵢ/x⟶yflxs /head yflxs∼yflfr
  ... | node left y' l' r' | xs , frᵢ/x⟶xs , xs∼fr | compound =
                  let yflfrᵢ/x⟶yflxs = /tail (lemma++/l {x} {flatten l} frᵢ/x⟶xs) ;
                       yflxs∼yflfr = ∼x /head /head (lemma++∼l {flatten l} xs∼fr)
                  in ∼x yflfrᵢ/x⟶yflxs /head yflxs∼yflfr
  ... | node right y' l' r' | xs , frᵢ/x⟶xs , xs∼fr | compound =
                  let yflfrᵢ/x⟶yflxs = /tail (lemma++/l {x} {flatten l} frᵢ/x⟶xs) ;
                       yflxs∼yflfr = ∼x /head /head (lemma++∼l {flatten l} xs∼fr)
                  in ∼x yflfrᵢ/x⟶yflxs /head yflxs∼yflfr

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Andreas, 2020-09-09, issue #4880
-- Parse all interleavings of hiding and irrelevance in non-dependent function space

module Issue4880 (A B : Set) where

postulate
  -- dependent
  -- * visible
  _ : A →   (_ : B) → A
  _ : A →  .(_ : B) → A
  _ : A → ..(_ : B) → A
  -- * hidden
  _ : A →   {_ : B} → A
  _ : A →  .{_ : B} → A
  _ : A → ..{_ : B} → A
  -- * instance
  _ : A →   ⦃ _ : B ⦄ → A
  _ : A →  .⦃ _ : B ⦄ → A
  _ : A → ..⦃ _ : B ⦄ → A

  -- non-dependent
  -- * visible
  _ : A →   B → A
  _ : A →  .B → A
  _ : A → ..B → A
  -- * visible, parenthesized
  _ : A →  .(B) → A
  _ : A → ..(B) → A
  _ : A →  (.B) → A
  _ : A → (..B) → A
  -- * hidden
  _ : A →   {B} → A
  _ : A →  .{B} → A
  _ : A → ..{B} → A
  _ : A →  {.B} → A
  _ : A → {..B} → A
  -- * instance
  _ : A →   ⦃ B ⦄ → A
  _ : A →  .⦃ B ⦄ → A
  _ : A → ..⦃ B ⦄ → A
  _ : A →  ⦃ .B ⦄ → A
  _ : A → ⦃ ..B ⦄ → A


text:
module OverloadedConstructors where

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

data Fin : Nat -> Set where
  zero : {n : Nat} -> Fin (suc n)
  suc  : {n : Nat} -> Fin n -> Fin (suc n)

three : Nat
three = suc (suc (suc zero))

ftwo : Fin three
ftwo = suc (suc zero)

inc : Nat -> Nat
inc = suc

{-
{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}
-}

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Equiv.PathSplit
open isPathSplitEquiv
open import Cubical.Modalities.Modality
open Modality

open import Cubical.Data.Empty as ⊥ using (⊥)
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.NatMinusOne as ℕ₋₁
open import Cubical.Data.Sigma
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.Nullification as Null hiding (rec; elim)

open import Cubical.HITs.Truncation.Base

open import Cubical.HITs.PropositionalTruncation as PropTrunc
  renaming (∥_∥ to ∥_∥₁; ∣_∣ to ∣_∣₁; squash to squash₁) using ()
open import Cubical.HITs.SetTruncation       as SetTrunc  using (∥_∥₂; ∣_∣₂; squash₂)
open import Cubical.HITs.GroupoidTruncation  as GpdTrunc  using (∥_∥₃; ∣_∣₃; squash₃)
open import Cubical.HITs.2GroupoidTruncation as 2GpdTrunc using (∥_∥₄; ∣_∣₄; squash₄)

private
  variable
    ℓ ℓ' : Level
    A B : Type ℓ

sphereFill : (n : ℕ₋₁) (f : S n → A) → Type _
sphereFill {A = A} n f = Σ[ top ∈ A ] ((x : S n) → top ≡ f x)

isSphereFilled : ℕ₋₁ → Type ℓ → Type ℓ
isSphereFilled n A = (f : S n → A) → sphereFill n f

isSphereFilledTrunc : {n : HLevel} → isSphereFilled (-1+ n) (hLevelTrunc n A)
isSphereFilledTrunc {n = zero}  f = hub f , ⊥.elim
isSphereFilledTrunc {n = suc n} f = hub f , spoke f

isSphereFilled→isOfHLevelSuc : {n : HLevel} → isSphereFilled (ℕ→ℕ₋₁ n) A → isOfHLevel (suc n) A
isSphereFilled→isOfHLevelSuc {A = A} {zero} h x y = sym (snd (h f) north) ∙ snd (h f) south
  where
    f : Susp ⊥ → A
    f north = x
    f south = y
isSphereFilled→isOfHLevelSuc {A = A} {suc n} h x y = isSphereFilled→isOfHLevelSuc (helper h x y)
  where
    helper : isSphereFilled (ℕ→ℕ₋₁ (suc n)) A → (x y : A) → isSphereFilled (ℕ→ℕ₋₁ n) (x ≡ y)
    helper h x y f = sym p ∙ q , r
      where
        f' : Susp (S (ℕ→ℕ₋₁ n)) → A
        f' north = x
        f' south = y
        f' (merid u i) = f u i

        p = snd (h f') north
        q = snd (h f') south

        r : (s : S (ℕ→ℕ₋₁ n)) → sym p ∙ q ≡ f s
        r s i j = hcomp (λ k → λ { (i = i0) → compPath-filler (sym p) q k j
                                 ; (i = i1) → snd (h f') (merid s j) k
                                 ; (j = i0) → p (k ∨ ~ i)
                                 ; (j = i1) → q k })
                        (p (~ i ∧ ~ j))

isOfHLevel→isSphereFilled : {n : HLevel} → isOfHLevel n A → isSphereFilled (-1+ n) A
isOfHLevel→isSphereFilled {n = zero} h f = fst h , λ _ → snd h _
isOfHLevel→isSphereFilled {n = suc zero} h f = f north , λ _ → h _ _
isOfHLevel→isSphereFilled {A = A} {suc (suc n)} h = helper λ x y → isOfHLevel→isSphereFilled (h x y)
  where
    helper : {n : HLevel} → ((x y : A) → isSphereFilled (-1+ n) (x ≡ y)) → isSphereFilled (suc₋₁ (-1+ n)) A
    helper {n} h f = l , r
      where
      l : A
      l = f north

      f' : S (-1+ n) → f north ≡ f south
      f' x i = f (merid x i)

      h' : sphereFill (-1+ n) f'
      h' = h (f north) (f south) f'

      r : (x : S (suc₋₁ (-1+ n))) → l ≡ f x
      r north = refl
      r south = h' .fst
      r (merid x i) j = hcomp (λ k → λ { (i = i0) → f north
                                       ; (i = i1) → h' .snd x (~ k) j
                                       ; (j = i0) → f north
                                       ; (j = i1) → f (merid x i) })
                              (f (merid x (i ∧ j)))

-- isNull (S n) A ≃ (isSphereFilled n A) × (∀ (x y : A) → isSphereFilled n (x ≡ y))

isOfHLevel→isSnNull : {n : HLevel} → isOfHLevel n A → isNull (S (-1+ n)) A
fst (sec (isOfHLevel→isSnNull h)) f     = fst (isOfHLevel→isSphereFilled h f)
snd (sec (isOfHLevel→isSnNull h)) f i s = snd (isOfHLevel→isSphereFilled h f) s i
fst (secCong (isOfHLevel→isSnNull h) x y) p = fst (isOfHLevel→isSphereFilled (isOfHLevelPath _ h x y) (funExt⁻ p))
snd (secCong (isOfHLevel→isSnNull h) x y) p i j s = snd (isOfHLevel→isSphereFilled (isOfHLevelPath _ h x y) (funExt⁻ p)) s i j

isSnNull→isOfHLevel : {n : HLevel} → isNull (S (-1+ n)) A → isOfHLevel n A
isSnNull→isOfHLevel {n = zero}  nA = fst (sec nA) ⊥.rec , λ y → fst (secCong nA _ y) (funExt ⊥.elim)
isSnNull→isOfHLevel {n = suc n} nA = isSphereFilled→isOfHLevelSuc (λ f → fst (sec nA) f , λ s i → snd (sec nA) f i s)

isOfHLevelTrunc : (n : HLevel) → isOfHLevel n (hLevelTrunc n A)
isOfHLevelTrunc zero    = hub ⊥.rec , λ _ → ≡hub ⊥.rec
isOfHLevelTrunc (suc n) = isSphereFilled→isOfHLevelSuc isSphereFilledTrunc

-- isOfHLevelTrunc n = isSnNull→isOfHLevel isNull-Null

-- hLevelTrunc n is a modality

rec : {n : HLevel}
      {B : Type ℓ'} →
      isOfHLevel n B →
      (A → B) →
      hLevelTrunc n A →
      B
rec h = Null.rec (isOfHLevel→isSnNull h)

elim : {n : HLevel}
       {B : hLevelTrunc n A → Type ℓ'}
       (hB : (x : hLevelTrunc n A) → isOfHLevel n (B x))
       (g : (a : A) → B (∣ a ∣))
       (x : hLevelTrunc n A) →
       B x
elim hB = Null.elim (λ x → isOfHLevel→isSnNull (hB x))

elim2 : {n : HLevel}
  {B : hLevelTrunc n A → hLevelTrunc n A → Type ℓ'}
  (hB : ((x y : hLevelTrunc n A) → isOfHLevel n (B x y)))
  (g : (a b : A) → B ∣ a ∣ ∣ b ∣)
  (x y : hLevelTrunc n A) →
  B x y
elim2 {n = n} hB g =
  elim (λ _ → isOfHLevelΠ n (λ _ → hB _ _))
    (λ a → elim (λ _ → hB _ _) (λ b → g a b))

elim3 : {n : HLevel}
  {B : (x y z : hLevelTrunc n A) → Type ℓ'}
  (hB : ((x y z : hLevelTrunc n A) → isOfHLevel n (B x y z)))
  (g : (a b c : A) → B (∣ a ∣) ∣ b ∣ ∣ c ∣)
  (x y z : hLevelTrunc n A) →
  B x y z
elim3 {n = n} hB g =
  elim2 (λ _ _ → isOfHLevelΠ n (hB _ _))
    (λ a b → elim (λ _ → hB _ _ _) (λ c → g a b c))

HLevelTruncModality : ∀ {ℓ} (n : HLevel) → Modality ℓ
isModal       (HLevelTruncModality n) = isOfHLevel n
isModalIsProp (HLevelTruncModality n) = isPropIsOfHLevel n
◯             (HLevelTruncModality n) = hLevelTrunc n
◯-isModal     (HLevelTruncModality n) = isOfHLevelTrunc n
η             (HLevelTruncModality n) = ∣_∣
◯-elim        (HLevelTruncModality n) = elim
◯-elim-β      (HLevelTruncModality n) = λ _ _ _ → refl
◯-=-isModal   (HLevelTruncModality n) = isOfHLevelPath n (isOfHLevelTrunc n)

truncIdempotentIso : (n : HLevel) → isOfHLevel n A → Iso A (hLevelTrunc n A)
truncIdempotentIso n hA = isModalToIso (HLevelTruncModality n) hA

truncIdempotent≃ : (n : HLevel) → isOfHLevel n A → A ≃ hLevelTrunc n A
truncIdempotent≃ n hA = ∣_∣ , isModalToIsEquiv (HLevelTruncModality n) hA

truncIdempotent : (n : HLevel) → isOfHLevel n A → hLevelTrunc n A ≡ A
truncIdempotent n hA = ua (invEquiv (truncIdempotent≃ n hA))

-- universal property

univTrunc : ∀ {ℓ} (n : HLevel) {B : TypeOfHLevel ℓ n} → Iso (hLevelTrunc n A → B .fst) (A → B .fst)
Iso.fun (univTrunc n {B , lev}) g a = g ∣ a ∣
Iso.inv (univTrunc n {B , lev}) = elim λ _ → lev
Iso.rightInv (univTrunc n {B , lev}) b = refl
Iso.leftInv (univTrunc n {B , lev}) b = funExt (elim (λ x → isOfHLevelPath _ lev _ _)
                                                     λ a → refl)

-- functorial action

map : {n : HLevel} {B : Type ℓ'} (g : A → B)
  → hLevelTrunc n A → hLevelTrunc n B
map g = rec (isOfHLevelTrunc _) (λ a → ∣ g a ∣)

mapCompIso : {n : HLevel} {B : Type ℓ'} → (Iso A B) → Iso (hLevelTrunc n A) (hLevelTrunc n B)
Iso.fun (mapCompIso g) = map (Iso.fun g)
Iso.inv (mapCompIso g) = map (Iso.inv g)
Iso.rightInv (mapCompIso g) = elim (λ x → isOfHLevelPath _ (isOfHLevelTrunc _) _ _) λ b → cong ∣_∣ (Iso.rightInv g b)
Iso.leftInv (mapCompIso g) = elim (λ x → isOfHLevelPath _ (isOfHLevelTrunc _) _ _) λ a → cong ∣_∣ (Iso.leftInv g a)

mapId : {n : HLevel} → ∀ t → map {n = n} (idfun A) t ≡ t
mapId {n = n} =
  elim (λ _ → isOfHLevelPath n (isOfHLevelTrunc n) _ _) (λ _ → refl)

-- equivalences to prop/set/groupoid truncations

propTruncTrunc1Iso : Iso ∥ A ∥₁ (∥ A ∥ 1)
Iso.fun propTruncTrunc1Iso = PropTrunc.elim (λ _ → isOfHLevelTrunc 1) ∣_∣
Iso.inv propTruncTrunc1Iso = elim (λ _ → squash₁) ∣_∣₁
Iso.rightInv propTruncTrunc1Iso = elim (λ _ → isOfHLevelPath 1 (isOfHLevelTrunc 1) _ _) (λ _ → refl)
Iso.leftInv propTruncTrunc1Iso = PropTrunc.elim (λ _ → isOfHLevelPath 1 squash₁ _ _) (λ _ → refl)

propTrunc≃Trunc1 : ∥ A ∥₁ ≃ ∥ A ∥ 1
propTrunc≃Trunc1 = isoToEquiv propTruncTrunc1Iso

propTrunc≡Trunc1 : ∥ A ∥₁ ≡ ∥ A ∥ 1
propTrunc≡Trunc1 = ua propTrunc≃Trunc1

setTruncTrunc2Iso : Iso ∥ A ∥₂ (∥ A ∥ 2)
Iso.fun setTruncTrunc2Iso = SetTrunc.elim (λ _ → isOfHLevelTrunc 2) ∣_∣
Iso.inv setTruncTrunc2Iso = elim (λ _ → squash₂) ∣_∣₂
Iso.rightInv setTruncTrunc2Iso = elim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _) (λ _ → refl)
Iso.leftInv setTruncTrunc2Iso = SetTrunc.elim (λ _ → isOfHLevelPath 2 squash₂ _ _) (λ _ → refl)

setTrunc≃Trunc2 : ∥ A ∥₂ ≃ ∥ A ∥ 2
setTrunc≃Trunc2 = isoToEquiv setTruncTrunc2Iso

propTrunc≡Trunc2 : ∥ A ∥₂ ≡ ∥ A ∥ 2
propTrunc≡Trunc2 = ua setTrunc≃Trunc2

groupoidTrunc≃Trunc3Iso : Iso ∥ A ∥₃ (∥ A ∥ 3)
Iso.fun groupoidTrunc≃Trunc3Iso = GpdTrunc.elim (λ _ → isOfHLevelTrunc 3) ∣_∣
Iso.inv groupoidTrunc≃Trunc3Iso = elim (λ _ → squash₃) ∣_∣₃
Iso.rightInv groupoidTrunc≃Trunc3Iso = elim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _) (λ _ → refl)
Iso.leftInv groupoidTrunc≃Trunc3Iso = GpdTrunc.elim (λ _ → isOfHLevelPath 3 squash₃ _ _) (λ _ → refl)

groupoidTrunc≃Trunc3 : ∥ A ∥₃ ≃ ∥ A ∥ 3
groupoidTrunc≃Trunc3 = isoToEquiv groupoidTrunc≃Trunc3Iso

groupoidTrunc≡Trunc3 : ∥ A ∥₃ ≡ ∥ A ∥ 3
groupoidTrunc≡Trunc3 = ua groupoidTrunc≃Trunc3

2GroupoidTrunc≃Trunc4Iso : Iso ∥ A ∥₄ (∥ A ∥ 4)
Iso.fun 2GroupoidTrunc≃Trunc4Iso = 2GpdTrunc.elim (λ _ → isOfHLevelTrunc 4) ∣_∣
Iso.inv 2GroupoidTrunc≃Trunc4Iso = elim (λ _ → squash₄) ∣_∣₄
Iso.rightInv 2GroupoidTrunc≃Trunc4Iso = elim (λ _ → isOfHLevelPath 4 (isOfHLevelTrunc 4) _ _) (λ _ → refl)
Iso.leftInv 2GroupoidTrunc≃Trunc4Iso = 2GpdTrunc.elim (λ _ → isOfHLevelPath 4 squash₄ _ _) (λ _ → refl)

2GroupoidTrunc≃Trunc4 : ∥ A ∥₄ ≃ ∥ A ∥ 4
2GroupoidTrunc≃Trunc4 =
  isoToEquiv
    (iso
      (2GpdTrunc.elim (λ _ → isOfHLevelTrunc 4) ∣_∣)
      (elim (λ _ → squash₄) ∣_∣₄)
      (elim (λ _ → isOfHLevelPath 4 (isOfHLevelTrunc 4) _ _) (λ _ → refl))
      (2GpdTrunc.elim (λ _ → isOfHLevelPath 4 squash₄ _ _) (λ _ → refl)))

2GroupoidTrunc≡Trunc4 : ∥ A ∥₄ ≡ ∥ A ∥ 4
2GroupoidTrunc≡Trunc4 = ua 2GroupoidTrunc≃Trunc4

isContr→isContrTrunc : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isContr A → isContr (hLevelTrunc n A)
isContr→isContrTrunc n contr = ∣ fst contr ∣ , (elim (λ _ → isOfHLevelPath n (isOfHLevelTrunc n) _ _) λ a → cong ∣_∣ (snd contr a))

truncOfProdIso : (n : ℕ) → Iso (hLevelTrunc n (A × B)) (hLevelTrunc n A × hLevelTrunc n B)
Iso.fun (truncOfProdIso n) = rec (isOfHLevelΣ n (isOfHLevelTrunc n) (λ _ → isOfHLevelTrunc n)) λ {(a , b) → ∣ a ∣ , ∣ b ∣}
Iso.inv (truncOfProdIso n) (a , b) = rec (isOfHLevelTrunc n)
                                          (λ a → rec (isOfHLevelTrunc n)
                                                      (λ b → ∣ a , b ∣)
                                                       b)
                                          a
Iso.rightInv (truncOfProdIso n) (a , b) =
  elim {B = λ a → Iso.fun (truncOfProdIso n) (Iso.inv (truncOfProdIso n) (a , b)) ≡ (a , b)}
       (λ _ → isOfHLevelPath n (isOfHLevelΣ n (isOfHLevelTrunc n) (λ _ → isOfHLevelTrunc n)) _ _)
       (λ a → elim {B = λ b → Iso.fun (truncOfProdIso n) (Iso.inv (truncOfProdIso n) (∣ a ∣ , b)) ≡ (∣ a ∣ , b)}
                    (λ _ → isOfHLevelPath n (isOfHLevelΣ n (isOfHLevelTrunc n) (λ _ → isOfHLevelTrunc n)) _ _)
                    (λ b → refl) b) a
Iso.leftInv (truncOfProdIso n) = elim (λ _ → isOfHLevelPath n (isOfHLevelTrunc n) _ _) λ a → refl

---- ∥ Ω A ∥ ₙ ≡ Ω ∥ A ∥ₙ₊₁  ----

abstract
  isOfHLevelTypeOfHLevel2 : ∀ n → isOfHLevel (suc n) (TypeOfHLevel ℓ n)
  isOfHLevelTypeOfHLevel2 n = isOfHLevelTypeOfHLevel n

  {- Proofs of Theorem 7.3.12. and Corollary 7.3.13. in the HoTT book  -}

module ΩTrunc where
  {- We define the fibration P to show a more general result  -}
  P : {X : Type ℓ} {n : HLevel} → ∥ X ∥ (suc n) → ∥ X ∥ (suc n) → Type ℓ
  P {n = n} x y =  elim2 (λ _ _  → isOfHLevelTypeOfHLevel2 (n))
                         (λ a b → ∥ a ≡ b ∥ n , isOfHLevelTrunc (n)) x y .fst

  {- We will need P to be of hLevel n + 3  -}
  hLevelP : {n : HLevel} (a b : ∥ B ∥ (suc n)) → isOfHLevel ((suc n)) (P a b)
  hLevelP {n = n} =
    elim2 (λ x y → isProp→isOfHLevelSuc (n) (isPropIsOfHLevel (suc n)))
          (λ a b → isOfHLevelSuc (n) (isOfHLevelTrunc (n)))

  {- decode function from P x y to x ≡ y -}
  decode-fun : {n : HLevel} (x y : ∥ B ∥ (suc n)) → P x y → x ≡ y
  decode-fun {n = n} =
    elim2 (λ u v → isOfHLevelΠ (suc n)
                                (λ _ → isOfHLevelSuc (suc n) (isOfHLevelTrunc (suc n)) u v))
          decode*
      where
      decode* : ∀ {n : HLevel} (u v : B)
              → P {n = n} ∣ u ∣ ∣ v ∣ → Path (∥ B ∥ (suc n)) ∣ u ∣ ∣ v ∣
      decode* {B = B} {n = zero} u v =
        rec ( isOfHLevelTrunc 1 ∣ u ∣ ∣ v ∣
            , λ _ → isOfHLevelSuc 1 (isOfHLevelTrunc 1) _ _ _ _) (cong ∣_∣)
      decode* {n = suc n} u v =
        rec (isOfHLevelTrunc (suc (suc n)) ∣ u ∣ ∣ v ∣) (cong ∣_∣)

  {- auxiliary function r used to define encode -}
  r : {m : HLevel} (u : ∥ B ∥ (suc m)) → P u u
  r = elim (λ x → hLevelP x x) (λ a → ∣ refl ∣)

  {- encode function from x ≡ y to P x y -}
  encode-fun : {n : HLevel} (x y : ∥ B ∥ (suc n)) → x ≡ y → P x y
  encode-fun x y p = transport (λ i → P x (p i)) (r x)

  {- We need the following two lemmas on the functions behaviour for refl -}
  dec-refl : {n : HLevel} (x : ∥ B ∥ (suc n)) → decode-fun x x (r x) ≡ refl
  dec-refl {n = zero} =
    elim (λ x → isOfHLevelSuc 1 (isOfHLevelSuc 1 (isOfHLevelTrunc 1) x x) _ _) (λ _ → refl)
  dec-refl {n = suc n} =
    elim (λ x → isOfHLevelSuc (suc n)
                  (isOfHLevelSuc (suc n)
                     (isOfHLevelTrunc (suc (suc n)) x x)
                     (decode-fun x x (r x)) refl))
         (λ _ → refl)

  enc-refl : {n : HLevel} (x : ∥ B ∥ (suc n)) → encode-fun x x refl ≡ r x
  enc-refl x j = transp (λ _ → P x x) j (r x)

  {- decode-fun is a right-inverse -}
  P-rinv : {n : HLevel} (u v : ∥ B ∥  (suc n)) (x : Path (∥ B ∥ (suc n)) u v)
         → decode-fun u v (encode-fun u v x) ≡ x
  P-rinv u v = J (λ y p → decode-fun u y (encode-fun u y p) ≡ p)
                 (cong (decode-fun u u) (enc-refl u) ∙ dec-refl u)

  {- decode-fun is a left-inverse -}
  P-linv : {n : HLevel} (u v : ∥ B ∥ (suc n )) (x : P u v)
         → encode-fun u v (decode-fun u v x) ≡ x
  P-linv {n = n} =
    elim2 (λ x y → isOfHLevelΠ (suc n)
                               (λ z → isOfHLevelSuc (suc n) (hLevelP x y) _ _))
          helper
    where
    helper : {n : HLevel} (a b : B) (p : P {n = n} ∣ a ∣ ∣ b ∣)
           → encode-fun _ _ (decode-fun ∣ a ∣ ∣ b ∣ p) ≡ p
    helper {n = zero} a b =
      elim (λ x → ( sym (isOfHLevelTrunc 0 .snd _) ∙ isOfHLevelTrunc 0 .snd x
                  , λ y → isOfHLevelSuc 1 (isOfHLevelSuc 0 (isOfHLevelTrunc 0)) _ _ _ _))
           (J (λ y p → encode-fun ∣ a ∣ ∣ y ∣ (decode-fun _ _ ∣ p ∣) ≡ ∣ p ∣)
              (enc-refl ∣ a ∣))
    helper {n = suc n} a b =
      elim (λ x → hLevelP {n = suc n} ∣ a ∣ ∣ b ∣ _ _)
           (J (λ y p → encode-fun {n = suc n} ∣ a ∣ ∣ y ∣ (decode-fun _ _ ∣ p ∣) ≡ ∣ p ∣)
              (enc-refl ∣ a ∣))

  {- The final Iso established -}
  IsoFinal : (n : HLevel) (x y : ∥ B ∥ (suc n)) → Iso (x ≡ y) (P x y)
  Iso.fun (IsoFinal _ x y) = encode-fun x y
  Iso.inv (IsoFinal _ x y) = decode-fun x y
  Iso.rightInv (IsoFinal _ x y) = P-linv x y
  Iso.leftInv (IsoFinal _ x y) = P-rinv x y

PathIdTrunc : {a b : A} (n : HLevel) → (Path (∥ A ∥ (suc n)) ∣ a ∣ ∣ b ∣) ≡ (∥ a ≡ b ∥ n)
PathIdTrunc n = isoToPath (ΩTrunc.IsoFinal n _ _)

PathΩ : {a : A} (n : HLevel) → (Path (∥ A ∥ (suc n)) ∣ a ∣ ∣ a ∣) ≡ (∥ a ≡ a ∥ n)
PathΩ n = PathIdTrunc n

{- Special case using direct defs of truncations -}
PathIdTrunc₀Iso : {a b : A} → Iso (∣ a ∣₂ ≡ ∣ b ∣₂) ∥ a ≡ b ∥₁
PathIdTrunc₀Iso = compIso (congIso setTruncTrunc2Iso)
                    (compIso (ΩTrunc.IsoFinal _ ∣ _ ∣ ∣ _ ∣)
                             (invIso propTruncTrunc1Iso))

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

truncOfTruncIso : (n m : HLevel) → Iso (hLevelTrunc n A) (hLevelTrunc n (hLevelTrunc (m + n) A))
Iso.fun (truncOfTruncIso n m) = elim (λ _ → isOfHLevelTrunc n) λ a → ∣ ∣ a ∣ ∣
Iso.inv (truncOfTruncIso {A = A} n m) =
  elim (λ _ → isOfHLevelTrunc n)
       (elim (λ _ → (isOfHLevelPlus m (isOfHLevelTrunc n )))
             λ a → ∣ a ∣)
Iso.rightInv (truncOfTruncIso {A = A} n m) =
  elim (λ x → isOfHLevelPath n (isOfHLevelTrunc n) _ _ )
               (elim (λ x → isOfHLevelPath (m + n) (isOfHLevelPlus m (isOfHLevelTrunc n)) _ _ )
                      λ a → refl)
Iso.leftInv (truncOfTruncIso n m) = elim (λ x → isOfHLevelPath n (isOfHLevelTrunc n) _ _) λ a → refl

truncOfTruncEq : (n m : ℕ) → (hLevelTrunc n A) ≃ (hLevelTrunc n (hLevelTrunc (m + n) A))
truncOfTruncEq n m = isoToEquiv (truncOfTruncIso n m)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


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

open import HoTT
open import cohomology.Theory
open import cohomology.PtdMapSequence
open import groups.ExactSequence
open import groups.Exactness
open import groups.HomSequence
open import groups.KernelImageUniqueFactorization

open import cw.CW

module cw.cohomology.FirstCohomologyGroup {i} (OT : OrdinaryTheory i)
  (⊙skel : ⊙Skeleton {i} 2) (ac : ⊙has-cells-with-choice 0 ⊙skel i) where

open OrdinaryTheory OT
open import cw.cohomology.TipAndAugment OT (⊙cw-take (lteSR lteS) ⊙skel)
open import cw.cohomology.WedgeOfCells OT
open import cw.cohomology.TipCoboundary OT (⊙cw-init ⊙skel)
open import cw.cohomology.HigherCoboundary OT ⊙skel
open import cw.cohomology.HigherCoboundaryGrid OT ⊙skel ac
open import cw.cohomology.GridPtdMap (⊙cw-incl-last (⊙cw-init ⊙skel)) (⊙cw-incl-last ⊙skel)
open import cw.cohomology.TipGrid OT (⊙cw-init ⊙skel) (⊙init-has-cells-with-choice ⊙skel ac)
open import cw.cohomology.TopGrid OT 1 (⊙cw-incl-last (⊙cw-init ⊙skel)) (⊙cw-incl-last ⊙skel)
open import cohomology.LongExactSequence cohomology-theory

private
  0≤2 : 0 ≤ 2
  0≤2 = lteSR lteS

  ac₀ = ⊙take-has-cells-with-choice 0≤2 ⊙skel ac

{-
              H
    Coker ≃ C(X₁)<------C(X₂) = C(X)
              ^           ^
              |           |
              |           |
           C(X₁/X₀)<---C(X₂/X₀) ≃ Ker
             WoC          G

    WoC := Wedges of Cells
-}

private
  G : Group i
  G = C 1 (⊙Cofiber (⊙cw-incl-tail 0≤2 ⊙skel))

  G-iso-Ker : G ≃ᴳ Ker.grp cw-co∂-last
  G-iso-Ker = Ker-cw-co∂-last

  H : Group i
  H = C 1 ⊙⟦ ⊙cw-init ⊙skel ⟧

  Coker-iso-H : CokerCo∂Head.grp ≃ᴳ H
  Coker-iso-H = Coker-cw-co∂-head

  G-to-C-cw : G →ᴳ C 1 ⊙⟦ ⊙skel ⟧
  G-to-C-cw = C-fmap 1 (⊙cfcod' (⊙cw-incl-tail 0≤2 ⊙skel))

  abstract
    G-to-C-cw-is-surj : is-surjᴳ G-to-C-cw
    G-to-C-cw-is-surj = Exact.K-trivial-implies-φ-is-surj
      (exact-seq-index 2 $ C-cofiber-exact-seq 0 (⊙cw-incl-tail 0≤2 ⊙skel))
      (CX₀-≠-is-trivial (pos-≠ (ℕ-S≠O 0)) ac₀)

  C-cw-to-H : C 1 ⊙⟦ ⊙skel ⟧ →ᴳ H
  C-cw-to-H = C-fmap 1 (⊙cw-incl-last ⊙skel)

  abstract
    C-cw-to-H-is-inj : is-injᴳ C-cw-to-H
    C-cw-to-H-is-inj = Exact.G-trivial-implies-ψ-is-inj
      (exact-seq-index 2 $ C-cofiber-exact-seq 0 (⊙cw-incl-last ⊙skel))
      (CXₙ/Xₙ₋₁-<-is-trivial ⊙skel ltS ac)

  C-WoC : Group i
  C-WoC = C 1 (⊙Cofiber (⊙cw-incl-last (⊙cw-init ⊙skel)))

  G-to-C-WoC : G →ᴳ C-WoC
  G-to-C-WoC = C-fmap 1 Y/X-to-Z/X

  C-WoC-to-H : C-WoC →ᴳ H
  C-WoC-to-H = C-fmap 1 (⊙cfcod' (⊙cw-incl-last (⊙cw-init ⊙skel)))

open import groups.KernelImage cw-co∂-last cw-co∂-head CX₁/X₀-is-abelian

C-cw-iso-ker/im : C 1 ⊙⟦ ⊙skel ⟧ ≃ᴳ Ker/Im
C-cw-iso-ker/im = H-iso-Ker/Im
  cw-co∂-last cw-co∂-head CX₁/X₀-is-abelian
  φ₁ φ₁-is-surj φ₂ φ₂-is-inj lemma-comm
  where
    φ₁ = G-to-C-cw ∘ᴳ GroupIso.g-hom G-iso-Ker
    abstract
      φ₁-is-surj : is-surjᴳ φ₁
      φ₁-is-surj = ∘-is-surj G-to-C-cw-is-surj (equiv-is-surj (GroupIso.g-is-equiv G-iso-Ker))

    φ₂ = GroupIso.g-hom Coker-iso-H ∘ᴳ C-cw-to-H
    abstract
      φ₂-is-inj : is-injᴳ φ₂
      φ₂-is-inj = ∘-is-inj (equiv-is-inj (GroupIso.g-is-equiv Coker-iso-H)) C-cw-to-H-is-inj

    abstract
      lemma-comm : ∀ g →
           GroupIso.g Coker-iso-H (GroupHom.f (C-cw-to-H ∘ᴳ G-to-C-cw) (GroupIso.g G-iso-Ker g))
        == q[ fst g ]
      lemma-comm g =
        GroupIso.g Coker-iso-H (GroupHom.f C-cw-to-H (GroupHom.f G-to-C-cw (GroupIso.g G-iso-Ker g)))
          =⟨ ap (GroupIso.g Coker-iso-H) (! (C-top-grid-commutes □$ᴳ GroupIso.g G-iso-Ker g)) ⟩
        GroupIso.g Coker-iso-H (GroupHom.f C-WoC-to-H (GroupHom.f G-to-C-WoC (GroupIso.g G-iso-Ker g)))
          =⟨ ap (GroupIso.g Coker-iso-H ∘ GroupHom.f C-WoC-to-H ∘ fst) (GroupIso.f-g G-iso-Ker g) ⟩
        GroupIso.g Coker-iso-H (GroupHom.f C-WoC-to-H (fst g))
          =⟨ GroupIso.g-f Coker-iso-H q[ fst g ] ⟩
        q[ fst g ]
          =∎

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Module.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.SIP

open import Cubical.Data.Sigma

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

open import Cubical.Reflection.RecordEquiv

open import Cubical.Algebra.Ring
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Group

open Iso

private
  variable
    ℓ ℓ' : Level

record IsLeftModule (R : Ring ℓ) {M : Type ℓ'}
  (0m : M)
  (_+_ : M → M → M)
  (-_ : M → M)
  (_⋆_ : ⟨ R ⟩ → M → M) : Type (ℓ-max ℓ ℓ') where

  constructor ismodule

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

  field
    +-isAbGroup : IsAbGroup 0m _+_ -_
    ⋆-assoc : (r s : ⟨ R ⟩) (x : M) → (r · s) ⋆ x ≡ r ⋆ (s ⋆ x)
    ⋆-ldist : (r s : ⟨ R ⟩) (x : M) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x)
    ⋆-rdist : (r : ⟨ R ⟩) (x y : M) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y)
    ⋆-lid   : (x : M) → 1r ⋆ x ≡ x

  open IsAbGroup +-isAbGroup public
    renaming
    ( assoc       to +-assoc
    ; identity    to +-identity
    ; lid         to +-lid
    ; rid         to +-rid
    ; inverse     to +-inv
    ; invl        to +-linv
    ; invr        to +-rinv
    ; comm        to +-comm
    ; isSemigroup to +-isSemigroup
    ; isMonoid    to +-isMonoid
    ; isGroup     to +-isGroup
    )

unquoteDecl IsLeftModuleIsoΣ = declareRecordIsoΣ IsLeftModuleIsoΣ (quote IsLeftModule)

record LeftModuleStr (R : Ring ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where

  constructor leftmodulestr

  field
    0m             : A
    _+_            : A → A → A
    -_             : A → A
    _⋆_            : ⟨ R ⟩ → A → A
    isLeftModule   : IsLeftModule R 0m _+_ -_ _⋆_

  open IsLeftModule isLeftModule public

LeftModule : (R : Ring ℓ) → ∀ ℓ' → Type (ℓ-max ℓ (ℓ-suc ℓ'))
LeftModule R ℓ' = Σ[ A ∈ Type ℓ' ] LeftModuleStr R A

module _ {R : Ring ℓ} where

  LeftModule→AbGroup : (M : LeftModule R ℓ') → AbGroup ℓ'
  LeftModule→AbGroup (_ , leftmodulestr _ _ _ _ isLeftModule) =
                     _ , abgroupstr _ _ _ (IsLeftModule.+-isAbGroup isLeftModule)

  isSetLeftModule : (M : LeftModule R ℓ') → isSet ⟨ M ⟩
  isSetLeftModule M = isSetAbGroup (LeftModule→AbGroup M)

  open RingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·s_)

  makeIsLeftModule : {M : Type ℓ'} {0m : M}
                  {_+_ : M → M → M} { -_ : M → M} {_⋆_ : ⟨ R ⟩ → M → M}
                  (isSet-M : isSet M)
                  (+-assoc :  (x y z : M) → x + (y + z) ≡ (x + y) + z)
                  (+-rid : (x : M) → x + 0m ≡ x)
                  (+-rinv : (x : M) → x + (- x) ≡ 0m)
                  (+-comm : (x y : M) → x + y ≡ y + x)
                  (⋆-assoc : (r s : ⟨ R ⟩) (x : M) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
                  (⋆-ldist : (r s : ⟨ R ⟩) (x : M) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
                  (⋆-rdist : (r : ⟨ R ⟩) (x y : M) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
                  (⋆-lid   : (x : M) → 1r ⋆ x ≡ x)
                → IsLeftModule R 0m _+_ -_ _⋆_
  makeIsLeftModule isSet-M +-assoc +-rid +-rinv +-comm ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid =
    ismodule (makeIsAbGroup isSet-M +-assoc +-rid +-rinv +-comm) ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid

record IsLeftModuleHom {R : Ring ℓ} {A B : Type ℓ'}
  (M : LeftModuleStr R A) (f : A → B) (N : LeftModuleStr R B)
  : Type (ℓ-max ℓ ℓ')
  where

  -- Shorter qualified names
  private
    module M = LeftModuleStr M
    module N = LeftModuleStr N

  field
    pres0 : f M.0m ≡ N.0m
    pres+ : (x y : A) → f (x M.+ y) ≡ f x N.+ f y
    pres- : (x : A) → f (M.- x) ≡ N.- (f x)
    pres⋆ : (r : ⟨ R ⟩) (y : A) → f (r M.⋆ y) ≡ r N.⋆ f y

LeftModuleHom : {R : Ring ℓ} (M N : LeftModule R ℓ') → Type (ℓ-max ℓ ℓ')
LeftModuleHom M N = Σ[ f ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsLeftModuleHom (M .snd) f (N .snd)

IsLeftModuleEquiv : {R : Ring ℓ} {A B : Type ℓ'}
  (M : LeftModuleStr R A) (e : A ≃ B) (N : LeftModuleStr R B)
  → Type (ℓ-max ℓ ℓ')
IsLeftModuleEquiv M e N = IsLeftModuleHom M (e .fst) N

LeftModuleEquiv : {R : Ring ℓ} (M N : LeftModule R ℓ') → Type (ℓ-max ℓ ℓ')
LeftModuleEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsLeftModuleEquiv (M .snd) e (N .snd)

isPropIsLeftModule : (R : Ring ℓ) {M : Type ℓ'}
  (0m : M)
  (_+_ : M → M → M)
  (-_ : M → M)
  (_⋆_ : ⟨ R ⟩ → M → M)
  → isProp (IsLeftModule R 0m _+_ -_ _⋆_)
isPropIsLeftModule R _ _ _ _ =
  isOfHLevelRetractFromIso 1 IsLeftModuleIsoΣ
    (isPropΣ (isPropIsAbGroup _ _ _)
      (λ ab →
        isProp× (isPropΠ3 λ _ _ _ → ab .is-set _ _)
          (isProp× (isPropΠ3 λ _ _ _ → ab .is-set _ _)
            (isProp× (isPropΠ3 λ _ _ _ → ab .is-set _ _)
              (isPropΠ λ _ → ab .is-set _ _)))))
  where
  open IsAbGroup

𝒮ᴰ-LeftModule : (R : Ring ℓ) → DUARel (𝒮-Univ ℓ') (LeftModuleStr R) (ℓ-max ℓ ℓ')
𝒮ᴰ-LeftModule R =
  𝒮ᴰ-Record (𝒮-Univ _) (IsLeftModuleEquiv {R = R})
    (fields:
      data[ 0m ∣ autoDUARel _ _ ∣ pres0 ]
      data[ _+_ ∣ autoDUARel _ _ ∣ pres+ ]
      data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
      data[ _⋆_ ∣ autoDUARel _ _ ∣ pres⋆ ]
      prop[ isLeftModule ∣ (λ _ _ → isPropIsLeftModule _ _ _ _ _) ])
  where
  open LeftModuleStr
  open IsLeftModuleHom

LeftModulePath : {R : Ring ℓ} (M N : LeftModule R ℓ') → (LeftModuleEquiv M N) ≃ (M ≡ N)
LeftModulePath {R = R} = ∫ (𝒮ᴰ-LeftModule R) .UARel.ua

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
open import Prelude
open import Nat
open import List
open import Int
open import Bij
open import delta-lemmas
open import Delta
open import NatDelta

max_stars_repo_name: nickcollins/dependent-dicts-agda

max_issues_repo_name: nickcollins/dependent-dicts-agda

max_forks_repo_name: nickcollins/dependent-dicts-agda


text:
module BasicIPC.Metatheory.Gentzen-BasicTarski where

open import BasicIPC.Syntax.Gentzen public
open import BasicIPC.Semantics.BasicTarski public

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)    γ = lookup i γ
eval (lam t)    γ = λ a → eval t (γ , a)
eval (app t u)  γ = eval t γ $ eval u γ
eval (pair t u) γ = eval t γ , eval u γ
eval (fst t)    γ = π₁ (eval t γ)
eval (snd t)    γ = π₂ (eval t γ)
eval unit       γ = ∙

-- Correctness of evaluation with respect to conversion.

-- FIXME: How to show this?
postulate
  oops₁ : ∀ {{_ : Model}} {A B Γ} {t : Γ , A ⊢ B} {u : Γ ⊢ A}
          → eval ([ top ≔ u ] t) ≡ (λ γ → eval t (γ , eval u γ))
  oops₂ : ∀ {{_ : Model}} {A B Γ} {t : Γ ⊢ A ▻ B}
          → eval t ≡ (λ γ a → eval (mono⊢ (weak⊆ {A = A}) t) (γ , a) a)

eval✓ : ∀ {{_ : Model}} {A Γ} {t t′ : Γ ⊢ A} → t ⋙ t′ → eval t ≡ eval t′
eval✓ refl⋙                    = refl
eval✓ (trans⋙ p q)             = trans (eval✓ p) (eval✓ q)
eval✓ (sym⋙ p)                 = sym (eval✓ p)
eval✓ (conglam⋙ {A} {B} p)     = cong (⟦λ⟧ {A} {B}) (eval✓ p)
eval✓ (congapp⋙ {A} {B} p q)   = cong² (_⟦$⟧_ {A} {B}) (eval✓ p) (eval✓ q)
eval✓ (congpair⋙ {A} {B} p q)  = cong² (_⟦,⟧_ {A} {B}) (eval✓ p) (eval✓ q)
eval✓ (congfst⋙ {A} {B} p)     = cong (⟦π₁⟧ {A} {B}) (eval✓ p)
eval✓ (congsnd⋙ {A} {B} p)     = cong (⟦π₂⟧ {A} {B}) (eval✓ p)
eval✓ (beta▻⋙ {A} {B} {t} {u}) = sym (oops₁ {A} {B} {_} {t} {u})
eval✓ (eta▻⋙ {A} {B} {t})      = oops₂ {A} {B} {_} {t}
eval✓ beta∧₁⋙                  = refl
eval✓ beta∧₂⋙                  = refl
eval✓ eta∧⋙                    = refl
eval✓ eta⊤⋙                   = refl

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Functional.Combinations where

open import Type

-- TODO: Generalize these. Probably by lists and foldᵣ of combination and rotation construction functions. Also categorically or dependently
rotate₃Fn₃Op₂ : ∀{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : Type{ℓ₂}} → (A → A → A → B) → (B → B → B) → (A → A → A → B)
rotate₃Fn₃Op₂(F)(_▫_) a b c = (F a b c) ▫ ((F b c a) ▫ (F c a b))

combine₃Fn₂Op₂ : ∀{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : Type{ℓ₂}} → (A → A → B) → (B → B → B) → (A → A → A → B)
combine₃Fn₂Op₂(F)(_▫_) a b c = (F a b) ▫ ((F a c) ▫ (F b c))

all₃Fn₁Op₂ : ∀{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : Type{ℓ₂}} → (A → B) → (B → B → B) → (A → A → A → B)
all₃Fn₁Op₂(F)(_▫_) a b c = (F a) ▫ ((F b) ▫ (F c))

combine₄Fn₃Op₂ : ∀{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : Type{ℓ₂}} → (A → A → A → B) → (B → B → B) → (A → A → A → A → B)
combine₄Fn₃Op₂(F)(_▫_) a b c d = (F a b c) ▫ ((F a b d) ▫ ((F a c d) ▫ (F b c d)))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- Andreas, 2013-03-15
-- Paolo Capriotti's formalization of Russell's paradox
{-# OPTIONS --cubical-compatible --type-in-type #-}
module Russell where

open import Common.Product
open import Common.Equality

data ⊥ : Set where

¬ : Set → Set
¬ A = A → ⊥

-- a model of set theory, uses Set : Set
data U : Set where
  set : (I : Set) → (I → U) → U

-- a set is regular if it doesn't contain itself
regular : U → Set
regular (set I f) = (i : I) → ¬ (f i ≡ set I f)

-- Russell's set: the set of all regular sets
R : U
R = set (Σ U regular) proj₁

-- R is not regular
R-nonreg : ¬ (regular R)
R-nonreg reg = reg (R , reg) refl

-- R is regular
R-reg : regular R
R-reg (x , reg) p = subst regular p reg (x , reg) p

-- contradiction

absurd : ⊥
absurd = R-nonreg R-reg


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

open import Cubical.Core.Everything
open import Cubical.Relation.Binary

module Cubical.Relation.Binary.Construct.NonStrictToStrict
  {a ℓ} {A : Type a} (_≤_ : Rel A ℓ) where

open import Cubical.Relation.Binary.Properties
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic hiding (_⇒_; ¬_)

open import Cubical.Data.Sigma
open import Cubical.Data.Sum.Base using (inl; inr)
open import Cubical.Data.Empty
open import Cubical.Foundations.Function using (_∘_; flip; id)
open import Cubical.Relation.Nullary
import Cubical.HITs.PropositionalTruncation as PT

------------------------------------------------------------------------
-- _≤_ can be turned into _<_ as follows:

_<_ : Rel A _
x < y = x ≤ y ⊓ x ≢ₚ y

------------------------------------------------------------------------
-- Relationship between relations

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = fst

<⇒≢ : _<_ ⇒ _≢ₚ_
<⇒≢ = snd

≤∧≢⇒< : ∀ {x y} → ⟨ x ≤ y ⟩ → ⟨ x ≢ₚ y ⟩ → ⟨ x < y ⟩
≤∧≢⇒< = _,_

<⇒≱ : Antisymmetric _≤_ → ∀ {x y} → ⟨ x < y ⟩ → ¬ ⟨ y ≤ x ⟩
<⇒≱ antisym (x≤y , x≢y) y≤x = x≢y (antisym x≤y y≤x)

≤⇒≯ : Antisymmetric _≤_ → ∀ {x y} → ⟨ x ≤ y ⟩ → ¬ ⟨ y < x ⟩
≤⇒≯ antisym x≤y y<x = <⇒≱ antisym y<x x≤y

≰⇒> : Reflexive _≤_ → Total _≤_ →
      ∀ {x y} → ¬ ⟨ x ≤ y ⟩ → ⟨ y < x ⟩
≰⇒> rfl total {x} {y} x≰y = PT.rec ((y < x) .snd) (λ {
    (inl x≤y) → elim (x≰y x≤y)
  ; (inr y≤x) → y≤x , x≰y ∘ reflx→fromeq _≤_ rfl ∘ PT.map sym
  }) (total x y)

≮⇒≥ : Discrete A → Reflexive _≤_ → Total _≤_ →
      ∀ {x y} → ¬ ⟨ x < y ⟩ → ⟨ y ≤ x ⟩
≮⇒≥ _≟_ ≤-refl _≤?_ {x} {y} x≮y with x ≟ y
... | yes x≈y = reflx→fromeq _≤_ ≤-refl ∣ sym x≈y ∣
... | no x≢y = PT.rec ((y ≤ x) .snd) (λ {
        (inl y≤x) → y≤x
      ; (inr x≤y) → elim (x≮y (x≤y , x≢y ∘ PT.rec (Discrete→isSet _≟_ _ _) id))
      }) (y ≤? x)
------------------------------------------------------------------------
-- Relational properties

<-toNotEq : ToNotEq _<_
<-toNotEq (_ , x≢y) x≡y = x≢y x≡y

<-irrefl : Irreflexive _<_
<-irrefl = tonoteq→irrefl _<_ <-toNotEq

<-transitive : IsPartialOrder _≤_ → Transitive _<_
<-transitive po (x≤y , x≢y) (y≤z , y≉z) =
  (transitive x≤y y≤z , x≢y ∘ antisym x≤y ∘ transitive y≤z ∘ fromEq ∘ PT.map sym)
  where open IsPartialOrder po

<-≤-trans : Transitive _≤_ → Antisymmetric _≤_ →
           Trans _<_ _≤_ _<_
<-≤-trans transitive antisym (x≤y , x≢y) y≤z =
  transitive x≤y y≤z , (λ x≡z → x≢y (antisym x≤y (Respectsʳ≡ₚ _≤_ (PT.map sym x≡z) y≤z)))

≤-<-trans : Transitive _≤_ → Antisymmetric _≤_ →
           Trans _≤_ _<_ _<_
≤-<-trans trans antisym x≤y (y≤z , y≢z) =
  trans x≤y y≤z , (λ x≡z → y≢z (antisym y≤z (Respectsˡ≡ₚ _≤_ x≡z x≤y)))

<-asym : Antisymmetric _≤_ → Asymmetric _<_
<-asym antisym (x≤y , x≢y) (y≤x , _) = x≢y (antisym x≤y y≤x)
{-
<-trichotomous : Discrete A → Antisymmetric _≤_ → Total _≤_ → Trichotomous _<_
<-trichotomous _≟_ antisym total x y with x ≟ y
... | yes x≡y = tri≡ (λ x<y → ?) x≡y (λ y<x → <-toNotEq y<x (PT.map sym x≡y))
... | no  x≢y with total x y
...   | inl x≤y = tri< (x≤y , x≢y) x≢y (x≢y ∘ antisym x≤y ∘ proj₁)
...   | inr y≤x = tri> (x≢y ∘ flip antisym y≤x ∘ proj₁) x≢y (y≤x , x≢y ∘ sym)
-}
<-decidable : Discrete A → Decidable _≤_ → Decidable _<_
<-decidable _≟_ _≤?_ x y with x ≤? y
... | no ¬p = no (¬p ∘ fst)
... | yes p with x ≟ y
...   | yes q = no (λ x<y → snd x<y ∣ q ∣)
...   | no ¬q = yes (p , ¬q ∘ PT.rec (Discrete→isSet _≟_ _ _) id)

------------------------------------------------------------------------
-- Structures
{-
isStrictPartialOrder : IsPartialOrder _≤_ → IsStrictPartialOrder _<_
isStrictPartialOrder po = record
  { irrefl     = <-irrefl
  ; transitive = <-transitive po
  } where open IsPartialOrder po

isStrictTotalOrder₁ : Discrete A → IsTotalOrder _≤_ →
                        IsStrictTotalOrder _<_
isStrictTotalOrder₁ ≟ tot = record
  { transitive = <-transitive isPartialOrder
  ; compare    = <-trichotomous ≟ antisym total
  } where open IsTotalOrder tot

isStrictTotalOrder₂ : IsDecTotalOrder _≤_ → IsStrictTotalOrder _<_
isStrictTotalOrder₂ dtot = isStrictTotalOrder₁ _≟_ isTotalOrder
  where open IsDecTotalOrder dtot
-}


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Connecting Nehemiah.Change.Term and Nehemiah.Change.Value.
------------------------------------------------------------------------

module Nehemiah.Change.Evaluation where

open import Nehemiah.Syntax.Type
open import Nehemiah.Syntax.Term
open import Nehemiah.Change.Type
open import Nehemiah.Change.Term
open import Nehemiah.Change.Value
open import Nehemiah.Denotation.Value
open import Nehemiah.Denotation.Evaluation

open import Relation.Binary.PropositionalEquality
open import Base.Denotation.Notation

import Parametric.Change.Evaluation
    ⟦_⟧Base ⟦_⟧Const ΔBase apply-base diff-base nil-base ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧
  as ChangeEvaluation

meaning-⊕-base : ChangeEvaluation.ApplyStructure
meaning-⊕-base base-int = refl
meaning-⊕-base base-bag = refl

meaning-⊝-base : ChangeEvaluation.DiffStructure
meaning-⊝-base base-int = refl
meaning-⊝-base base-bag = refl

meaning-onil-base : ChangeEvaluation.NilStructure
meaning-onil-base base-int = refl
meaning-onil-base base-bag = refl

open ChangeEvaluation.Structure meaning-⊕-base meaning-⊝-base meaning-onil-base public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Data.String where

import Data.List
import Data.Char
open   Data.List using (List)
open   Data.Char

postulate String : Set

{-# BUILTIN STRING String #-}

infixr 50 _++_

private
  primitive
    primStringAppend   : String -> String -> String
    primStringToList   : String -> List Char
    primStringFromList : List Char -> String

_++_     = primStringAppend
toList   = primStringToList
fromList = primStringFromList

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Dave.Algebra.Naturals.Excercises where
  open import Dave.Algebra.Naturals.Addition

  +-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
  +-rearrange m n p q = begin
    (m + n) + (p + q) ≡⟨ IsSemigroup.assoc ℕ-+-IsSemigroup m n (p + q) ⟩
    m + (n + (p + q)) ≡⟨ cong (λ a → m + a) (sym (IsSemigroup.assoc ℕ-+-IsSemigroup n p q)) ⟩
    m + ((n + p) + q) ≡⟨ sym (IsSemigroup.assoc ℕ-+-IsSemigroup m (n + p) q) ⟩
    (m + (n + p)) + q ∎

  +-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
  +-swap m n p = begin
    m + (n + p) ≡⟨ +-comm m (n + p) ⟩
    (n + p) + m ≡⟨ IsSemigroup.assoc ℕ-+-IsSemigroup n p m ⟩
    n + (p + m) ≡⟨ cong (λ a → n + a) (+-comm p m) ⟩
    n + (m + p) ∎