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

open import lib.Basics
open import lib.types.Nat
open import lib.types.Group
open import lib.types.TLevel

module lib.types.Int where

data ℤ : Type₀ where
  pos : (n : ℕ) → ℤ
  negsucc : (n : ℕ) → ℤ

Int = ℤ

{-# BUILTIN INTEGER Int #-}
{-# BUILTIN INTEGERPOS pos #-}
{-# BUILTIN INTEGERNEGSUC negsucc #-}

{- literal overloading -}

instance
  ℤ-reader : FromNat ℤ
  FromNat.in-range ℤ-reader _ = ⊤
  FromNat.read ℤ-reader n = pos n

  ℤ-neg-reader : FromNeg ℤ
  FromNeg.in-range ℤ-neg-reader _ = ⊤
  FromNeg.read ℤ-neg-reader O = pos O
  FromNeg.read ℤ-neg-reader (S n) = negsucc n

{- succ and pred -}

succ : ℤ → ℤ
succ (pos n) = pos (S n)
succ (negsucc O) = pos O
succ (negsucc (S n)) = negsucc n

pred : ℤ → ℤ
pred (pos O) = negsucc O
pred (pos (S n)) = pos n
pred (negsucc n) = negsucc (S n)

abstract
  succ-pred : (n : ℤ) → succ (pred n) == n
  succ-pred (pos O) = idp
  succ-pred (pos (S n)) = idp
  succ-pred (negsucc n) = idp

  pred-succ : (n : ℤ) → pred (succ n) == n
  pred-succ (pos n) = idp
  pred-succ (negsucc O) = idp
  pred-succ (negsucc (S n)) = idp

succ-equiv : ℤ ≃ ℤ
succ-equiv = equiv succ pred succ-pred pred-succ

pred-injective : (z₁ z₂ : ℤ) → pred z₁ == pred z₂ → z₁ == z₂
pred-injective z₁ z₂ p = ! (succ-pred z₁) ∙ ap succ p ∙ succ-pred z₂

succ-injective : (z₁ z₂ : ℤ) → succ z₁ == succ z₂ → z₁ == z₂
succ-injective z₁ z₂ p = ! (pred-succ z₁) ∙ ap pred p ∙ pred-succ z₂

{- Converting between ℤ, ℕ, and ℕ₋₂ -}

ℤ-to-ℕ₋₂ : ℤ → ℕ₋₂
ℤ-to-ℕ₋₂ (pos m) = ⟨ m ⟩
ℤ-to-ℕ₋₂ (negsucc O) = -1
ℤ-to-ℕ₋₂ (negsucc _) = -2

ℕ-to-ℤ : ℕ → ℤ
ℕ-to-ℤ n = pos n

{- Proof that [ℤ] has decidable equality and hence is a set -}

private
  ℤ-get-pos : ℤ → ℕ
  ℤ-get-pos (pos n) = n
  ℤ-get-pos (negsucc n) = O

  ℤ-get-negsucc : ℤ → ℕ
  ℤ-get-negsucc (pos n) = O
  ℤ-get-negsucc (negsucc n) = n

  ℤ-negsucc≠pos-type : ℤ → Type₀
  ℤ-negsucc≠pos-type (pos n) = Empty
  ℤ-negsucc≠pos-type (negsucc n) = Unit

abstract
  pos-injective : (n m : ℕ) (p : pos n == pos m) → n == m
  pos-injective n m p = ap ℤ-get-pos p

  pos-≠ : {n m : ℕ} (p : n ≠ m) → pos n ≠ pos m
  pos-≠ p = p ∘ pos-injective _ _

  negsucc-injective : (n m : ℕ) (p : negsucc n == negsucc m) → n == m
  negsucc-injective n m p = ap ℤ-get-negsucc p

  ℤ-negsucc≠pos : (n m : ℕ) → negsucc n ≠ pos m
  ℤ-negsucc≠pos n m p = transport ℤ-negsucc≠pos-type p unit

  ℤ-pos≠negsucc : (n m : ℕ) → pos n ≠ negsucc m
  ℤ-pos≠negsucc n m p = transport ℤ-negsucc≠pos-type (! p) unit

  ℤ-has-dec-eq : has-dec-eq ℤ
  ℤ-has-dec-eq (pos n) (pos m) with ℕ-has-dec-eq n m
  ℤ-has-dec-eq (pos n) (pos m) | inl p = inl (ap pos p)
  ℤ-has-dec-eq (pos n) (pos m) | inr p⊥ = inr (pos-≠ p⊥)
  ℤ-has-dec-eq (pos n) (negsucc m) = inr (ℤ-pos≠negsucc n m)
  ℤ-has-dec-eq (negsucc n) (pos m) = inr (ℤ-negsucc≠pos n m)
  ℤ-has-dec-eq (negsucc n) (negsucc m) with ℕ-has-dec-eq n m
  ℤ-has-dec-eq (negsucc n) (negsucc m) | inl p = inl (ap negsucc p)
  ℤ-has-dec-eq (negsucc n) (negsucc m) | inr p⊥ = inr (λ p → p⊥ (negsucc-injective n m p))

  ℤ-is-set : is-set ℤ
  ℤ-is-set = dec-eq-is-set ℤ-has-dec-eq

ℤ-level = ℤ-is-set

{-
  ℤ is also a group!
-}

-- inv
ℤ~ : ℤ → ℤ
ℤ~ (pos (S n)) = negsucc n
ℤ~ (pos O) = pos O
ℤ~ (negsucc n) = pos (S n)

-- comp
infixl 80 _ℤ+_
_ℤ+_ : ℤ → ℤ → ℤ
pos O         ℤ+ z = z
pos (S n)     ℤ+ z = succ (pos n ℤ+ z)
negsucc O     ℤ+ z = pred z
negsucc (S n) ℤ+ z = pred (negsucc n ℤ+ z)

-- unit-l
ℤ+-unit-l : ∀ z → pos O ℤ+ z == z
ℤ+-unit-l _ = idp

-- unit-r
private
  ℤ+-unit-r-pos : ∀ n → pos n ℤ+ pos O == pos n
  ℤ+-unit-r-pos O     = idp
  ℤ+-unit-r-pos (S n) = ap succ $ ℤ+-unit-r-pos n

  ℤ+-unit-r-negsucc : ∀ n → negsucc n ℤ+ pos O == negsucc n
  ℤ+-unit-r-negsucc O     = idp
  ℤ+-unit-r-negsucc (S n) = ap pred $ ℤ+-unit-r-negsucc n

ℤ+-unit-r : ∀ z → z ℤ+ pos O == z
ℤ+-unit-r (pos n) = ℤ+-unit-r-pos n
ℤ+-unit-r (negsucc n) = ℤ+-unit-r-negsucc n

-- assoc
succ-ℤ+ : ∀ z₁ z₂ → succ z₁ ℤ+ z₂ == succ (z₁ ℤ+ z₂)
succ-ℤ+ (pos n) _ = idp
succ-ℤ+ (negsucc O) _ = ! $ succ-pred _
succ-ℤ+ (negsucc (S _)) _ = ! $ succ-pred _

pred-ℤ+ : ∀ z₁ z₂ → pred z₁ ℤ+ z₂ == pred (z₁ ℤ+ z₂)
pred-ℤ+ (negsucc _) _ = idp
pred-ℤ+ (pos O) _ = idp
pred-ℤ+ (pos (S n)) _ = ! $ pred-succ _

ℤ+-assoc : ∀ z₁ z₂ z₃ → (z₁ ℤ+ z₂) ℤ+ z₃ == z₁ ℤ+ (z₂ ℤ+ z₃)
ℤ+-assoc (pos O)      z₂ z₃ = idp
ℤ+-assoc (pos (S n₁)) z₂ z₃ =
  succ (pos n₁ ℤ+ z₂) ℤ+ z₃     =⟨ succ-ℤ+ (pos n₁ ℤ+ z₂) z₃ ⟩
  succ ((pos n₁ ℤ+ z₂) ℤ+ z₃)   =⟨ ap succ $ ℤ+-assoc (pos n₁) z₂ z₃ ⟩
  succ (pos n₁ ℤ+ (z₂ ℤ+ z₃))   ∎
ℤ+-assoc (negsucc O)      z₂ z₃ = pred-ℤ+ z₂ z₃
ℤ+-assoc (negsucc (S n₁)) z₂ z₃ =
  pred (negsucc n₁ ℤ+ z₂) ℤ+ z₃     =⟨ pred-ℤ+ (negsucc n₁ ℤ+ z₂) z₃ ⟩
  pred ((negsucc n₁ ℤ+ z₂) ℤ+ z₃)   =⟨ ap pred $ ℤ+-assoc (negsucc n₁) z₂ z₃ ⟩
  pred (negsucc n₁ ℤ+ (z₂ ℤ+ z₃))   ∎

--comm
ℤ+-succ : ∀ z₁ z₂ → z₁ ℤ+ succ z₂ == succ (z₁ ℤ+ z₂)
ℤ+-succ (pos O) z₂ = idp
ℤ+-succ (pos (S n)) z₂ = ap succ (ℤ+-succ (pos n) z₂)
ℤ+-succ (negsucc O) z₂ = pred-succ z₂ ∙ ! (succ-pred z₂)
ℤ+-succ (negsucc (S n)) z₂ =
  pred (negsucc n ℤ+ succ z₂)
    =⟨ ap pred (ℤ+-succ (negsucc n) z₂) ⟩
  pred (succ (negsucc n ℤ+ z₂))
    =⟨ pred-succ (negsucc n ℤ+ z₂) ⟩
  negsucc n ℤ+ z₂
    =⟨ ! $ succ-pred (negsucc n ℤ+ z₂) ⟩
  succ (pred (negsucc n ℤ+ z₂))
    ∎

ℤ+-pred : ∀ z₁ z₂ → z₁ ℤ+ pred z₂ == pred (z₁ ℤ+ z₂)
ℤ+-pred (pos O) z₂ = idp
ℤ+-pred (pos (S n)) z₂ =
  succ (pos n ℤ+ pred z₂)
    =⟨ ap succ (ℤ+-pred (pos n) z₂) ⟩
  succ (pred (pos n ℤ+ z₂))
    =⟨ succ-pred (pos n ℤ+ z₂) ⟩
  pos n ℤ+ z₂
    =⟨ ! $ pred-succ (pos n ℤ+ z₂) ⟩
  pred (succ (pos n ℤ+ z₂))
    ∎
ℤ+-pred (negsucc O) z₂ = idp
ℤ+-pred (negsucc (S n)) z₂ = ap pred (ℤ+-pred (negsucc n) z₂)

ℤ+-comm : ∀ z₁ z₂ → z₁ ℤ+ z₂ == z₂ ℤ+ z₁
ℤ+-comm (pos O) z₂ = ! $ ℤ+-unit-r z₂
ℤ+-comm (pos (S n₁)) z₂ =
  succ (pos n₁ ℤ+ z₂)
    =⟨ ℤ+-comm (pos n₁) z₂ |in-ctx succ ⟩
  succ (z₂ ℤ+ pos n₁)
    =⟨ ! $ ℤ+-succ z₂ (pos n₁) ⟩
  z₂ ℤ+ pos (S n₁)
    ∎
ℤ+-comm (negsucc O) z₂ =
  pred z₂
    =⟨ ! $ ℤ+-unit-r z₂ |in-ctx pred ⟩
  pred (z₂ ℤ+ pos O)
    =⟨ ! $ ℤ+-pred z₂ (pos O) ⟩
  z₂ ℤ+ negsucc O
    ∎
ℤ+-comm (negsucc (S n)) z₂ =
  pred (negsucc n ℤ+ z₂)
    =⟨ ℤ+-comm (negsucc n) z₂ |in-ctx pred ⟩
  pred (z₂ ℤ+ negsucc n)
    =⟨ ! $ ℤ+-pred z₂ (negsucc n) ⟩
  z₂ ℤ+ negsucc (S n)
    ∎

private
  pos-S-ℤ+-negsucc-S : ∀ n₁ n₂ → pos (S n₁) ℤ+ negsucc (S n₂) == pos n₁ ℤ+ negsucc n₂
  pos-S-ℤ+-negsucc-S O      n₂ = idp
  pos-S-ℤ+-negsucc-S (S n₁) n₂ = ap succ $ pos-S-ℤ+-negsucc-S n₁ n₂

  negsucc-S-ℤ+-pos-S : ∀ n₁ n₂ → negsucc (S n₁) ℤ+ pos (S n₂) == negsucc n₁ ℤ+ pos n₂
  negsucc-S-ℤ+-pos-S O      n₂ = idp
  negsucc-S-ℤ+-pos-S (S n₁) n₂ = ap pred $ negsucc-S-ℤ+-pos-S n₁ n₂

ℤ~-inv-r : ∀ z → z ℤ+ ℤ~ z == 0
ℤ~-inv-r (pos O)     = idp
ℤ~-inv-r (pos (S O)) = idp
ℤ~-inv-r (pos (S (S n))) =
  pos (S (S n)) ℤ+ negsucc (S n)  =⟨ pos-S-ℤ+-negsucc-S (S n) n ⟩
  pos (S n) ℤ+ negsucc n          =⟨ ℤ~-inv-r (pos (S n)) ⟩
  0                               ∎
ℤ~-inv-r (negsucc O) = idp
ℤ~-inv-r (negsucc (S n)) =
  negsucc (S n) ℤ+ pos (S (S n))  =⟨ negsucc-S-ℤ+-pos-S n (S n) ⟩
  negsucc n ℤ+ pos (S n)          =⟨ ℤ~-inv-r (negsucc n) ⟩
  0                               ∎

ℤ~-inv-l : ∀ z → ℤ~ z ℤ+ z == 0
ℤ~-inv-l (pos O) = idp
ℤ~-inv-l (pos (S n)) = ℤ~-inv-r (negsucc n)
ℤ~-inv-l (negsucc n) = ℤ~-inv-r (pos (S n))

ℤ-group-structure : GroupStructure ℤ
ℤ-group-structure = record
  { ident = 0
  ; inv = ℤ~
  ; comp = _ℤ+_
  ; unitl = ℤ+-unit-l
  ; unitr = ℤ+-unit-r
  ; assoc = ℤ+-assoc
  ; invr = ℤ~-inv-r
  ; invl = ℤ~-inv-l
  }

ℤ-group : Group₀
ℤ-group = group _ ℤ-is-set ℤ-group-structure

-- More properties about [ℤ~]

ℤ~-succ : ∀ z → ℤ~ (succ z) == pred (ℤ~ z)
ℤ~-succ (pos 0) = idp
ℤ~-succ (pos (S n)) = idp
ℤ~-succ (negsucc 0) = idp
ℤ~-succ (negsucc (S n)) = idp

ℤ~-pred : ∀ z → ℤ~ (pred z) == succ (ℤ~ z)
ℤ~-pred (pos 0) = idp
ℤ~-pred (pos 1) = idp
ℤ~-pred (pos (S (S n))) = idp
ℤ~-pred (negsucc 0) = idp
ℤ~-pred (negsucc (S n)) = idp

ℤ~-ℤ+ : ∀ z₁ z₂ → ℤ~ (z₁ ℤ+ z₂) == ℤ~ z₁ ℤ+ ℤ~ z₂
ℤ~-ℤ+ (pos 0)         z₂ = idp
ℤ~-ℤ+ (pos 1)         z₂ = ℤ~-succ z₂
ℤ~-ℤ+ (pos (S (S n))) z₂ =
  ℤ~-succ (pos (S n) ℤ+ z₂) ∙ ap pred (ℤ~-ℤ+ (pos (S n)) z₂)
ℤ~-ℤ+ (negsucc O)     z₂ = ℤ~-pred z₂
ℤ~-ℤ+ (negsucc (S n)) z₂ =
  ℤ~-pred (negsucc n ℤ+ z₂) ∙ ap succ (ℤ~-ℤ+ (negsucc n) z₂)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- Andreas, 2016-11-03, issue #2291 reported by Aerate

test = let {{_}} = _ in _

-- WAS: Internal error
-- NOW: Could not parse the left-hand side {{_}}

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue4130 where

module Foo where
  data D : Set where
    con : D

module Bar (S : Set) where
  open Foo public using (con)

open Bar using (con)
open Foo using (D; con)

data B : Set where
  tt : B
  ff : B

module _ (S : Set) where
  open Bar S
  f : D -> B
  -- 'con' is not ambiguous, because although 'con' may refer to
  -- 'Foo.D.con' or 'Bar.con', they are two different names of the
  -- same constructor.
  f con = tt

max_forks_repo_name: shlevy/agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

open import Cubical.Algebra
open import Cubical.Algebra.Monoid.Morphism
open import Cubical.Algebra.Properties

open import Cubical.Relation.Binary.Reasoning.Equality

private
  variable
    g h : Level

-- The following definitions of GroupHom and GroupEquiv are level-wise heterogeneous.
-- This allows for example to deduce that G ≡ F from a chain of isomorphisms
-- G ≃ H ≃ F, even if H does not lie in the same level as G and F.

record IsGroupHom (G : Group g) (H : Group h) (f : ⟨ G ⟩ → ⟨ H ⟩) : Type (ℓ-max g h) where
  constructor isgrouphom

  private
    module G = Group G
    module H = Group H

  field
    preservesOp : Homomorphic₂ f G._•_ H._•_

  preservesId : Homomorphic₀ f G.ε H.ε
  preservesId = H.cancelʳ _ (
    f G.ε H.• f G.ε ≡˘⟨ preservesOp G.ε G.ε ⟩
    f (G.ε G.• G.ε) ≡⟨ cong f (G.identityˡ G.ε) ⟩
    f G.ε           ≡˘⟨ H.identityˡ (f G.ε) ⟩
    H.ε H.• f G.ε   ∎)

  preservesInv : Homomorphic₁ f G._⁻¹ H._⁻¹
  preservesInv x = H.inv-uniqueʳ _ _ (
    f (x G.⁻¹) H.• f x ≡˘⟨ preservesOp (x G.⁻¹) x ⟩
    f (x G.⁻¹ G.• x)   ≡⟨ cong f (G.inverseˡ x) ⟩
    f G.ε              ≡⟨ preservesId ⟩
    H.ε                ∎)

record GroupHom (G : Group g) (H : Group h) : Type (ℓ-max g h) where
  constructor grouphom
  field
    fun : ⟨ G ⟩ → ⟨ H ⟩
    isHom : IsGroupHom G H fun

  open IsGroupHom isHom public

record GroupEquiv (G : Group g) (H : Group h) : Type (ℓ-max g h) where
  constructor groupequiv
  field
    eq : ⟨ G ⟩ ≃ ⟨ H ⟩
    isHom : IsGroupHom G H (equivFun eq)

  open IsGroupHom isHom public

  hom : GroupHom G H
  hom = grouphom (equivFun eq) isHom

instance
  GroupHomOperators : HomOperators (Group g) (Group h) (ℓ-max g h)
  GroupHomOperators = record { _⟶ᴴ_ = GroupHom; _≃ᴴ_ = GroupEquiv }

private
  variable
    G : Group g
    H : Group h

  isPropIsMonoidHom : {f : ⟨ G ⟩ → ⟨ H ⟩}
                      → isProp (IsMonoidHom (Group.monoid G) (Group.monoid H) f)
  isPropIsMonoidHom {G = G} {H = H} {f = f} (ismonoidhom aOp aId) (ismonoidhom bOp bId) =
    cong₂ ismonoidhom
      (isPropHomomorphic₂ (Group.is-set H) f (Group._•_ G) (Group._•_ H) aOp bOp)
      (isPropHomomorphic₀ (Group.is-set H) f (Group.ε   G) (Group.ε   H) aId bId)

  isPropIsGroupHom : {f : ⟨ G ⟩ → ⟨ H ⟩} → isProp (IsGroupHom G H f)
  isPropIsGroupHom {G = G} {H = H} {f = f} (isgrouphom aHom) (isgrouphom bHom) =
    cong isgrouphom
      (isPropHomomorphic₂ (Group.is-set H) f (Group._•_ G) (Group._•_ H) aHom bHom)

IsGroupHom→IsMonoidHom : {f : ⟨ G ⟩ → ⟨ H ⟩}
              → IsGroupHom G H f → IsMonoidHom (Group.monoid G) (Group.monoid H) f
IsGroupHom→IsMonoidHom hom .IsMonoidHom.preservesOp = hom .IsGroupHom.preservesOp
IsGroupHom→IsMonoidHom hom .IsMonoidHom.preservesId = IsGroupHom.preservesId hom

IsMonoidHom→IsGroupHom : {f : ⟨ G ⟩ → ⟨ H ⟩}
              → IsMonoidHom (Group.monoid G) (Group.monoid H) f → IsGroupHom G H f
IsMonoidHom→IsGroupHom hom .IsGroupHom.preservesOp = hom .IsMonoidHom.preservesOp

IsGroupHom≃IsMonoidHom : {f : ⟨ G ⟩ → ⟨ H ⟩}
              → IsGroupHom G H f ≃ IsMonoidHom (Group.monoid G) (Group.monoid H) f
IsGroupHom≃IsMonoidHom {G = G} {H = H} = isoToEquiv
    (iso IsGroupHom→IsMonoidHom
         IsMonoidHom→IsGroupHom
         (λ _ → isPropIsMonoidHom {G = G} {H = H} _ _)
         (λ _ → isPropIsGroupHom _ _))

GroupHom→MonoidHom : (G ⟶ᴴ H) → (Group.monoid G ⟶ᴴ Group.monoid H)
GroupHom→MonoidHom hom .MonoidHom.fun = hom .GroupHom.fun
GroupHom→MonoidHom hom .MonoidHom.isHom = IsGroupHom→IsMonoidHom (hom .GroupHom.isHom)

MonoidHom→GroupHom : (Group.monoid G ⟶ᴴ Group.monoid H) → (G ⟶ᴴ H)
MonoidHom→GroupHom hom .GroupHom.fun = hom .MonoidHom.fun
MonoidHom→GroupHom hom .GroupHom.isHom = IsMonoidHom→IsGroupHom (hom .MonoidHom.isHom)

GroupHom≃MonoidHom : (G ⟶ᴴ H) ≃ (Group.monoid G ⟶ᴴ Group.monoid H)
GroupHom≃MonoidHom {G = G} {H = H} =
    isoToEquiv (iso GroupHom→MonoidHom
                    MonoidHom→GroupHom
                    MonoidHom→GroupHom→MonoidHom
                    GroupHom→MonoidHom→GroupHom)
  where
    MonoidHom→GroupHom→MonoidHom :
      section (GroupHom→MonoidHom {G = G} {H = H}) (MonoidHom→GroupHom {G = G} {H = H})
    MonoidHom→GroupHom→MonoidHom (monoidhom fun prf) =
      cong₂ monoidhom refl (isPropIsMonoidHom {G = G} {H = H} _ _)

    GroupHom→MonoidHom→GroupHom :
      retract (GroupHom→MonoidHom {G = G} {H = H}) (MonoidHom→GroupHom {G = G} {H = H})
    GroupHom→MonoidHom→GroupHom (grouphom fun prf) =
      cong₂ grouphom refl (isPropIsGroupHom _ _)

GroupEquiv→MonoidEquiv : G ≃ᴴ H → Group.monoid G ≃ᴴ Group.monoid H
GroupEquiv→MonoidEquiv eq .MonoidEquiv.eq = eq .GroupEquiv.eq
GroupEquiv→MonoidEquiv eq .MonoidEquiv.isHom = IsGroupHom→IsMonoidHom (eq .GroupEquiv.isHom)

MonoidEquiv→GroupEquiv : Group.monoid G ≃ᴴ Group.monoid H → G ≃ᴴ H
MonoidEquiv→GroupEquiv eq .GroupEquiv.eq = eq .MonoidEquiv.eq
MonoidEquiv→GroupEquiv eq .GroupEquiv.isHom = IsMonoidHom→IsGroupHom (eq .MonoidEquiv.isHom)

GroupEquiv≃MonoidEquiv : G ≃ᴴ H ≃ Group.monoid G ≃ᴴ Group.monoid H
GroupEquiv≃MonoidEquiv {G = G} {H = H} =
    isoToEquiv (iso GroupEquiv→MonoidEquiv
                    MonoidEquiv→GroupEquiv
                    MonoidEquiv→GroupEquiv→MonoidEquiv
                    GroupEquiv→MonoidEquiv→GroupEquiv)
  where
    MonoidEquiv→GroupEquiv→MonoidEquiv :
      section (GroupEquiv→MonoidEquiv {G = G} {H = H}) (MonoidEquiv→GroupEquiv {G = G} {H = H})
    MonoidEquiv→GroupEquiv→MonoidEquiv (monoidequiv eq prf) =
      cong₂ monoidequiv refl (isPropIsMonoidHom {G = G} {H = H} _ _)

    GroupEquiv→MonoidEquiv→GroupEquiv :
      retract (GroupEquiv→MonoidEquiv {G = G} {H = H}) (MonoidEquiv→GroupEquiv {G = G} {H = H})
    GroupEquiv→MonoidEquiv→GroupEquiv (groupequiv eq prf) =
      cong₂ groupequiv refl (isPropIsGroupHom _ _)


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

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Vec.Base

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.RingSolver.NatAsAlmostRing
open import Cubical.Algebra.RingSolver.RawAlgebra renaming (⟨_⟩ to ⟨_⟩ᵣ)
open import Cubical.Algebra.RingSolver.CommRingSolver

-- In scope for debugging:
open import Cubical.Algebra.RingSolver.CommRingHornerForms

private
  variable
    ℓ : Level

module MultivariateSolving (R : CommRing {ℓ}) where
  -- In scope for debuggin:

  -- In scope for solver use:
  open CommRingStr (snd R)
  AsAlgebra = CommRing→RawℤAlgebra R

  X : ℤExpr R 3
  X = ∣ Fin.zero

  Y : ℤExpr R 3
  Y = ∣ (suc Fin.zero)

  Z : ℤExpr R 3
  Z = ∣ (suc (suc Fin.zero))

  _ : (x y z : (fst R)) → x · y · z ≡ z · y · x
  _ = λ x y z →
              let
                lhs = X ·' Y ·' Z
                rhs = Z ·' Y ·' X
              in solve R lhs rhs (x ∷ y ∷ z ∷ []) refl

  _ : (x y z : (fst R)) → x · (y + z) ≡ z · x + y · x
  _ = λ x y z →
              let
                lhs = X ·' (Y +' Z)
                rhs = Z ·' X +' Y ·' X
              in solve R lhs rhs (x ∷ y ∷ z ∷ []) refl

  _ : (x y z : (fst R)) → x · (y - z) ≡ (- z) · x + y · x
  _ = λ x y z →
              let
                lhs = X ·' (Y +' (-' Z))
                rhs = (-' Z) ·' X +' (Y ·' X)
              in solve R lhs rhs (x ∷ y ∷ z ∷ []) refl

  {-
    A bigger example, copied from 'Example.agda'
  -}
  _ : (x y z : (fst R)) → (x + y) · (x + y) · (x + y) · (x + y)
                ≡ x · x · x · x + (scalar R 4) · x · x · x · y + (scalar R 6) · x · x · y · y
                  +  (scalar R 4) · x · y · y · y + y · y · y · y
  _ = λ x y z → let
              lhs = (X +' Y) ·' (X +' Y) ·' (X +' Y) ·' (X +' Y)
              rhs = X ·' X ·' X ·' X
                  +' (K 4) ·' X ·' X ·' X ·' Y
                  +' (K 6) ·' X ·' X ·' Y ·' Y
                  +' (K 4) ·' X ·' Y ·' Y ·' Y
                  +' Y ·' Y ·' Y ·' Y
             in solve R lhs rhs (x ∷ y ∷ z ∷ []) refl

  _ : (x y z : (fst R)) → (x + y) · (x - y) ≡ (x · x - y · y)
  _ = λ x y z →
              let
                lhs = (X +' Y) ·' (X +' (-' Y))
                rhs = (X ·' X) +' (-' (Y ·' Y))
              in solve R lhs rhs (x ∷ y ∷ z ∷ []) refl


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.Instances.DirectSumFun where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat

open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.DirectSum.DirectSumFun.Base
open import Cubical.Algebra.DirectSum.DirectSumFun.Properties

private variable
  ℓ : Level

module _ (G : (n : ℕ) → Type ℓ) (Gstr : (n : ℕ) → AbGroupStr (G n)) where

  open AbGroupStr
  open DSF-properties G Gstr

  ⊕Fun-AbGr : AbGroup ℓ
  fst ⊕Fun-AbGr = ⊕Fun G Gstr
  0g (snd ⊕Fun-AbGr) = 0⊕Fun
  AbGroupStr._+_ (snd ⊕Fun-AbGr) = _+⊕Fun_
  - snd ⊕Fun-AbGr = Inv⊕Fun
  isAbGroup (snd ⊕Fun-AbGr) = makeIsAbGroup isSet⊕Fun +⊕FunAssoc +⊕FunRid +⊕FunInvR +⊕FunComm

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Data.Tree.Rose where

open import Prelude
open import Data.List

mutual
  Forest : Type a → Type a
  Forest A = List (Tree A)

  infixr 5 _&_
  record Tree {a} (A : Type a) : Type a where
    inductive
    constructor _&_
    field
      root : A
      children : Forest A
open Tree public

module WikiTree where
  open import Data.List.Syntax
  wikiTree : Tree ℕ
  wikiTree =
      1 &
        [ 2 &
            [ 5 &
                [ 9  & []
                , 10 & [] ]
            , 6 & [] ]
        , 3 & []
        , 4 &
            [ 7 &
                [ 11 & []
                , 12 & [] ]
            , 8 & [] ] ]

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --cubical #-}

module Demos.Printf where

open import Data.List
open import Data.String
open import Prelude
open import Data.Nat.Show

data Fstr : Type where
  [] : Fstr
  %s_ : Fstr → Fstr
  %i_ : Fstr → Fstr
  _∷_ : Char → Fstr → Fstr

parse : String → Fstr
parse = go ∘ unpack
  where
  go : List Char → Fstr
  go ('%' ∷ 's' ∷ xs) = %s go xs
  go ('%' ∷ 'i' ∷ xs) = %i go xs
  go [] = []
  go (x ∷ xs) = x ∷ go xs

Format : Fstr → Type
Format [] = String
Format (%s xs) = String → Format xs
Format (%i xs) = ℕ → Format xs
Format (x ∷ xs) = Format xs

format : (xs : Fstr) → Format xs
format = go pack
  where
  go : (List Char → String) → (xs : Fstr) → Format xs
  go k [] = k []
  go k (%s xs) s = go (k ∘ (unpack s ++_)) xs
  go k (%i xs) i = go (k ∘ (unpack (showℕ i) ++_)) xs
  go k (x ∷ xs)  = go (k ∘ (x ∷_)) xs

printf : (fstr : String) → Format (parse fstr)
printf fstr = format (parse fstr)

-- Example:
--
-- >>> printf "%s, %i: %s" "hello" 2 "you"
-- "hello, 2: you"


text:
{-# OPTIONS --cubical-compatible #-}

-- Andreas, 2020-02-07, instances of #906 needing --cubical-compatible to throw
-- off the termination checker.

module Issue906WithoutK where

module Issue3081 where

  postulate
    X : Set
    P : (x : X) → Set
    any : {X : Set} → X

  record W : Set where
    field
      x : X
      p : P x

  record Category : Set₁ where
    field
      z : W
      s : W → W

  {- Termination checking failed for the following functions:
       functor
     Problematic calls:
       W.x (functor .Category.s u)
       W.x (functor .Category.z)
  -}
  functor : Category
  functor .Category.z .W.x = any
  functor .Category.z .W.p = any
  functor .Category.s u .W.x = any
  functor .Category.s u .W.p = any

module Issue3081Ulf where

  open import Agda.Builtin.Nat

  record R : Set where
    field
      a : Nat
      b : Nat

  record S : Set where
    field
      r : R  -- works if we give r and h the same number of arguments
      h : Nat → R

  open R
  open S

  f : S
  f .r   .a = 0
  f .r   .b = f .r   .a
  f .h n .a = n
  f .h n .b = f .h n .a

-- Should all pass the termination checker.


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition
open import Setoids.Setoids
open import Setoids.Subset
open import Graphs.Definition

module Graphs.Bipartite where

Bipartite : {a b : _} {c : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) → Set _
Bipartite {V' = V'} {V = V} G = Sg (V' → Set) (λ partition → ((x y : V') → (Setoid._∼_ V x y) → partition x → partition y) & ((x : V') → (partition x) || ((partition x) → False)) & ((x y : V') → (Graph._<->_ G x y) → (partition x) → ((partition y) → False)))


text:
module Typing where
import IO.Primitive as Prim
--open import Data.Unit
open import ParseTree
open import Data.Nat
open import Data.List
open import Data.String
open import Data.Unit
{-# FOREIGN GHC
  import InteractWithAgda
#-}

postulate getTypes : List ParseTree -> ℕ -> List Expr -> String -> Prim.IO (List Expr)
{-# COMPILE GHC getTypes = getTypes #-}

postulate getEnvironment : List  ParseTree -> ℕ -> String -> Prim.IO (List TypeSignature)
{-# COMPILE GHC getEnvironment = getEnvironment #-}

postulate output : String -> Prim.IO ⊤
{-# COMPILE GHC output = output #-}


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

open import lib.Basics
open import lib.types.TLevel
open import lib.types.Pi
open import lib.types.Sigma
open import lib.NType2

module lib.types.Truncation where

module _ {i} where

  postulate  -- HIT
    Trunc : (n : ℕ₋₂) (A : Type i) → Type i
    [_] : {n : ℕ₋₂} {A : Type i} → A → Trunc n A
    instance Trunc-level : {n : ℕ₋₂} {A : Type i} → has-level n (Trunc n A)

  module TruncElim {n : ℕ₋₂} {A : Type i} {j} {P : Trunc n A → Type j}
    {{p : (x : Trunc n A) → has-level n (P x)}} (d : (a : A) → P [ a ]) where

    postulate  -- HIT
      f : Π (Trunc n A) P
      [_]-β : ∀ a → f [ a ] ↦ d a
    {-# REWRITE [_]-β #-}

open TruncElim public renaming (f to Trunc-elim)

module TruncRec {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} {{p : has-level n B}}
  (d : A → B) where

  private
    module M = TruncElim {{λ x → p}} d

  f : Trunc n A → B
  f = M.f

open TruncRec public renaming (f to Trunc-rec)

module TruncRecType {i j} {n : ℕ₋₂} {A : Type i} (d : A → n -Type j) where

  open TruncRec {{n -Type-level j}} d public

  flattening-Trunc : Σ (Trunc (S n) A) (fst ∘ f) ≃ Trunc (S n) (Σ A (fst ∘ d))
  flattening-Trunc = equiv to from to-from from-to where

    to-aux : (x : Trunc (S n) A) → (fst (f x) → Trunc (S n) (Σ A (fst ∘ d)))
    to-aux = Trunc-elim (λ a b → [ (a , b) ])

    to : Σ (Trunc (S n) A) (fst ∘ f) → Trunc (S n) (Σ A (fst ∘ d))
    to (x , y) = to-aux x y

    from-aux : Σ A (fst ∘ d) → Σ (Trunc (S n) A) (fst ∘ f)
    from-aux (a , b) = ([ a ] , b)

    from : Trunc (S n) (Σ A (fst ∘ d)) → Σ (Trunc (S n) A) (fst ∘ f)
    from = Trunc-rec {{Σ-level ⟨⟩ (λ x → raise-level _ (snd (f x)))}}
                     from-aux  where

    to-from : (x : Trunc (S n) (Σ A (fst ∘ d))) → to (from x) == x
    to-from = Trunc-elim (λ _ → idp)

    from-to-aux : (a : Trunc (S n) A) (b : fst (f a)) → from (to-aux a b) == (a , b)
    from-to-aux = Trunc-elim {{λ _ → Π-level (λ _ → =-preserves-level (Σ-level ⟨⟩ (λ x → raise-level _ (snd (f x)))))}}
                             (λ a b → idp)

    from-to : (x : Σ (Trunc (S n) A) (fst ∘ f)) → from (to x) == x
    from-to (a , b) = from-to-aux a b

⊙Trunc : ∀ {i} → ℕ₋₂ → Ptd i → Ptd i
⊙Trunc n ⊙[ A , a ] = ⊙[ Trunc n A , [ a ] ]

module _ {i} {n : ℕ₋₂} {A : Type i} where

  Trunc= : (a b : Trunc (S n) A) → n -Type i
  Trunc= = Trunc-elim (λ a → Trunc-elim ((λ b → (Trunc n (a == b) , Trunc-level))))

  Trunc=-equiv : (a b : Trunc (S n) A) → (a == b) ≃ fst (Trunc= a b)
  Trunc=-equiv a b = equiv (to a b) (from a b) (to-from a b) (from-to a b) where

    to-aux : (a : Trunc (S n) A) → fst (Trunc= a a)
    to-aux = Trunc-elim {{λ x → raise-level _ (snd (Trunc= x x))}}
                        (λ a → [ idp ])

    to : (a b : Trunc (S n) A) → (a == b → fst (Trunc= a b))
    to a .a idp = to-aux a

    from-aux : (a b : A) → a == b → [ a ] == [ b ] :> Trunc (S n) A
    from-aux a .a idp = idp

    from : (a b : Trunc (S n) A) → (fst (Trunc= a b) → a == b)
    from = Trunc-elim (λ a → Trunc-elim (λ b → Trunc-rec (from-aux a b)))

    to-from-aux : (a b : A) → (p : a == b) → to _ _ (from-aux a b p) == [ p ]
    to-from-aux a .a idp = idp

    to-from : (a b : Trunc (S n) A) (x : fst (Trunc= a b)) → to a b (from a b x) == x
    to-from = Trunc-elim {{λ x → Π-level (λ y → Π-level (λ _ → =-preserves-level (raise-level _ (snd (Trunc= x y)))))}}
              (λ a → Trunc-elim {{λ x → Π-level (λ _ → =-preserves-level (raise-level _ (snd (Trunc= [ a ] x))))}}
              (λ b → Trunc-elim
              (to-from-aux a b)))

    from-to-aux : (a : Trunc (S n) A) → from a a (to-aux a) == idp
    from-to-aux = Trunc-elim (λ _ → idp)

    from-to : (a b : Trunc (S n) A) (p : a == b) → from a b (to a b p) == p
    from-to a .a idp = from-to-aux a
  Trunc=-path : (a b : Trunc (S n) A) → (a == b) == fst (Trunc= a b)
  Trunc=-path a b = ua (Trunc=-equiv a b)

{- Universal property -}

abstract
  Trunc-rec-is-equiv : ∀ {i j} (n : ℕ₋₂) (A : Type i) (B : Type j)
    {{p : has-level n B}} → is-equiv (Trunc-rec {{p}} :> ((A → B) → (Trunc n A → B)))
  Trunc-rec-is-equiv n A B {{p}} = is-eq _ (λ f → f ∘ [_])
    (λ f → λ= (Trunc-elim (λ a → idp))) (λ f → idp)

Trunc-preserves-level : ∀ {i} {A : Type i} {n : ℕ₋₂} (m : ℕ₋₂)
 → has-level n A → has-level n (Trunc m A)
Trunc-preserves-level {n = ⟨-2⟩} _ p = has-level-in
  ([ contr-center p ] , Trunc-elim (λ a → ap [_] (contr-path p a)))
Trunc-preserves-level ⟨-2⟩ _ = contr-has-level Trunc-level
Trunc-preserves-level {n = (S n)} (S m) c = has-level-in (λ t₁ t₂ →
  Trunc-elim
    {{λ s₁ → prop-has-level-S {A = has-level n (s₁ == t₂)} has-level-is-prop}}
    (λ a₁ → Trunc-elim
      {{λ s₂ → prop-has-level-S {A = has-level n ([ a₁ ] == s₂)} has-level-is-prop}}
      (λ a₂ → equiv-preserves-level
      ((Trunc=-equiv [ a₁ ] [ a₂ ])⁻¹)
               {{Trunc-preserves-level {n = n} m (has-level-apply c a₁ a₂)}})
              t₂)
    t₁)

{- an n-type is equivalent to its n-truncation -}
unTrunc-equiv : ∀ {i} {n : ℕ₋₂} (A : Type i)
  {{_ : has-level n A}} → Trunc n A ≃ A
unTrunc-equiv A = equiv f [_] (λ _ → idp) g-f where
  f = Trunc-rec (idf _)
  g-f = Trunc-elim (λ _ → idp)

⊙unTrunc-equiv : ∀ {i} {n : ℕ₋₂} (X : Ptd i)
  {{_ : has-level n (de⊙ X)}} → ⊙Trunc n X ⊙≃ X
⊙unTrunc-equiv {n = n} X = ≃-to-⊙≃ (unTrunc-equiv (de⊙ X)) idp

-- Equivalence associated to the universal property
Trunc-extend-equiv : ∀ {i j} (n : ℕ₋₂) (A : Type i) (B : Type j)
  {{p : has-level n B}} → (A → B) ≃ (Trunc n A → B)
Trunc-extend-equiv n A B = (Trunc-rec , Trunc-rec-is-equiv n A B)

Trunc-fmap : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} → ((A → B) → (Trunc n A → Trunc n B))
Trunc-fmap f = Trunc-rec ([_] ∘ f)

⊙Trunc-fmap : ∀ {i j} {n : ℕ₋₂} {X : Ptd i} {Y : Ptd j} → ((X ⊙→ Y) → (⊙Trunc n X ⊙→ ⊙Trunc n Y))
⊙Trunc-fmap F = Trunc-fmap (fst F) , ap [_] (snd F)

Trunc-fmap2 : ∀ {i j k} {n : ℕ₋₂} {A : Type i} {B : Type j} {C : Type k}
  → ((A → B → C) → (Trunc n A → Trunc n B → Trunc n C))
Trunc-fmap2 f = Trunc-rec (λ a → Trunc-fmap (f a))

-- XXX What is the naming convention?
Trunc-fpmap : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} {f g : A → B}
  → f ∼ g → Trunc-fmap {n = n} f ∼ Trunc-fmap g
Trunc-fpmap h = Trunc-elim (ap [_] ∘ h)

Trunc-fmap-idf : ∀ {i} {n : ℕ₋₂} {A : Type i}
  → ∀ x → Trunc-fmap {n = n} (idf A) x == x
Trunc-fmap-idf =
  Trunc-elim (λ _ → idp)

Trunc-fmap-∘ : ∀ {i j k} {n : ℕ₋₂} {A : Type i} {B : Type j} {C : Type k}
  → (g : B → C) → (f : A → B)
  → ∀ x → Trunc-fmap {n = n} g (Trunc-fmap f x) == Trunc-fmap (g ∘ f) x
Trunc-fmap-∘ g f =
  Trunc-elim (λ _ → idp)

Trunc-csmap : ∀ {i₀ i₁ j₀ j₁} {n : ℕ₋₂}
  {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  {f : A₀ → B₀} {g : A₁ → B₁} {hA : A₀ → A₁} {hB : B₀ → B₁}
  → CommSquare f g hA hB
  → CommSquare (Trunc-fmap {n = n} f) (Trunc-fmap g) (Trunc-fmap hA) (Trunc-fmap hB)
Trunc-csmap (comm-sqr cs) = comm-sqr $ Trunc-elim (ap [_] ∘ cs)

{- Pushing concatentation through Trunc= -}
module _ {i} {n : ℕ₋₂} {A : Type i} where

  {- concatenation in Trunc= -}
  Trunc=-∙ : {ta tb tc : Trunc (S n) A}
    → fst (Trunc= ta tb) → fst (Trunc= tb tc) → fst (Trunc= ta tc)
  Trunc=-∙ {ta = ta} {tb = tb} {tc = tc} =
    Trunc-elim {P = λ ta → C ta tb tc}
      {{λ ta → level ta tb tc}}
      (λ a → Trunc-elim {P = λ tb → C [ a ] tb tc}
         {{λ tb → level [ a ] tb tc}}
         (λ b → Trunc-elim {P = λ tc → C [ a ] [ b ] tc}
                  {{λ tc → level [ a ] [ b ] tc}}
                  (λ c → Trunc-fmap2 _∙_)
                  tc)
         tb)
      ta
    where
    C : (ta tb tc : Trunc (S n) A) → Type i
    C ta tb tc = fst (Trunc= ta tb) → fst (Trunc= tb tc) → fst (Trunc= ta tc)

    level : (ta tb tc : Trunc (S n) A) → has-level (S n) (C ta tb tc)
    level ta tb tc = raise-level _ $
              Π-level (λ _ → Π-level (λ _ → snd (Trunc= ta tc)))

  {- XXX naming convention -}
  Trunc=-∙-comm : {x y z : Trunc (S n) A }
    (p : x == y) (q : y == z)
    →  –> (Trunc=-equiv x z) (p ∙ q)
    == Trunc=-∙ {ta = x} (–> (Trunc=-equiv x y) p) (–> (Trunc=-equiv y z) q)
  Trunc=-∙-comm {x = x} idp idp =
    Trunc-elim
       {P = λ x → –> (Trunc=-equiv x x) idp
               == Trunc=-∙ {ta = x} (–> (Trunc=-equiv x x) idp)
                                    (–> (Trunc=-equiv x x) idp)}
       {{λ x → raise-level _ $ =-preserves-level (snd (Trunc= x x))}}
       (λ a → idp)
       x

{- naturality of Trunc=-equiv -}

module _ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} (f : A → B) where
  Trunc=-fmap : ∀ (a₀ a₁ : Trunc (S n) A)
    → (fst (Trunc= {n = n} a₀ a₁) → fst (Trunc= {n = n} (Trunc-fmap f a₀) (Trunc-fmap f a₁)))
  Trunc=-fmap = Trunc-elim
    {P = λ a₀ → ∀ a₁ → (fst (Trunc= a₀ a₁) → fst (Trunc= (Trunc-fmap f a₀) (Trunc-fmap f a₁)))}
    {{λ a₀ → Π-level λ a₁ → Π-level λ _ → raise-level _ $ snd (Trunc= (Trunc-fmap f a₀) (Trunc-fmap f a₁))}}
    (λ a₀ → Trunc-elim
      {P = λ a₁ → (fst (Trunc= [ a₀ ] a₁) → fst (Trunc= [ f a₀ ] (Trunc-fmap f a₁)))}
      {{λ a₁ → Π-level λ _ → raise-level _ $ snd (Trunc= [ f a₀ ] (Trunc-fmap f a₁))}}
      (λ a₁ → Trunc-fmap (ap f)))

module _ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} (f : A → B) where
  Trunc=-equiv-nat : ∀ (a₀ a₁ : Trunc (S n) A) (p : a₀ == a₁)
     →  –> (Trunc=-equiv (Trunc-fmap f a₀) (Trunc-fmap f a₁)) (ap (Trunc-fmap f) p)
     == Trunc=-fmap f a₀ a₁ (–> (Trunc=-equiv a₀ a₁) p)
  Trunc=-equiv-nat a₀ .a₀ idp =
    Trunc-elim
      {P = λ a
        →  –> (Trunc=-equiv (Trunc-fmap f a) (Trunc-fmap f a)) idp
        == Trunc=-fmap f a a (–> (Trunc=-equiv a a) idp)}
      {{λ a → raise-level _ $ =-preserves-level $ snd ((Trunc= (Trunc-fmap f a) (Trunc-fmap f a)))}}
      (λ _ → idp)
      a₀

{- Truncation preserves equivalences - more convenient than univalence+ap
 - when we need to know the forward or backward function explicitly -}
module _ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j} where

  Trunc-isemap : {f : A → B} → is-equiv f → is-equiv (Trunc-fmap {n = n} f)
  Trunc-isemap {f-orig} ie = is-eq f g f-g g-f where
    f = Trunc-fmap f-orig
    g = Trunc-fmap (is-equiv.g ie)

    f-g : ∀ tb → f (g tb) == tb
    f-g = Trunc-elim (ap [_] ∘ is-equiv.f-g ie)

    g-f : ∀ ta → g (f ta) == ta
    g-f = Trunc-elim (ap [_] ∘ is-equiv.g-f ie)

  Trunc-emap : A ≃ B → Trunc n A ≃ Trunc n B
  Trunc-emap (f , f-ie) = Trunc-fmap f , Trunc-isemap f-ie

Trunc-csemap : ∀ {i₀ i₁ j₀ j₁} {n : ℕ₋₂}
  {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  {f : A₀ → B₀} {g : A₁ → B₁} {hA : A₀ → A₁} {hB : B₀ → B₁}
  → CommSquareEquiv f g hA hB
  → CommSquareEquiv (Trunc-fmap {n = n} f) (Trunc-fmap g) (Trunc-fmap hA) (Trunc-fmap hB)
Trunc-csemap (cs , hA-ise , hB-ise) = Trunc-csmap cs , Trunc-isemap hA-ise , Trunc-isemap hB-ise

transport-Trunc : ∀ {i j} {A : Type i} {n : ℕ₋₂} (P : A → Type j)
  {x y : A} (p : x == y) (b : P x)
  → transport (Trunc n ∘ P) p [ b ] == [ transport P p b ]
transport-Trunc _ idp _ = idp

Trunc-fuse : ∀ {i} (A : Type i) (m n : ℕ₋₂)
  → Trunc m (Trunc n A) ≃ Trunc (minT m n) A
Trunc-fuse A m n = equiv
  (Trunc-rec {{raise-level-≤T (minT≤l m n) Trunc-level}}
    (Trunc-rec {{raise-level-≤T (minT≤r m n) Trunc-level}}
      [_]))
  (Trunc-rec ([_] ∘ [_]))
  (Trunc-elim (λ _ → idp))
  (Trunc-elim (Trunc-elim
       {{λ _ → =-preserves-level (Trunc-preserves-level _ Trunc-level)}}
       (λ _ → idp)))
  where
      instance
        l : has-level (minT m n) (Trunc m (Trunc n A))
        l with (minT-out m n)
        l | inl p = transport (λ k → has-level k (Trunc m (Trunc n A)))
                              (! p) Trunc-level
        l | inr q = Trunc-preserves-level _
                      (transport (λ k → has-level k (Trunc n A))
                                 (! q) Trunc-level)

Trunc-fuse-≤ : ∀ {i} (A : Type i) {m n : ℕ₋₂} (m≤n : m ≤T n)
  → Trunc m (Trunc n A) ≃ Trunc m A
Trunc-fuse-≤ A m≤n = equiv
  (Trunc-rec (Trunc-rec {{raise-level-≤T m≤n Trunc-level}}
      [_]))
  (Trunc-rec ([_] ∘ [_]))
  (Trunc-elim (λ _ → idp))
  (Trunc-elim (Trunc-elim
       {{λ _ → =-preserves-level (Trunc-preserves-level _ Trunc-level)}}
       (λ _ → idp)))

{- Truncating a binary product is equivalent to truncating its components -}
Trunc-×-econv : ∀ {i} {j} (n : ℕ₋₂) (A : Type i) (B : Type j)
  → Trunc n (A × B) ≃ Trunc n A × Trunc n B
Trunc-×-econv n A B = equiv f g f-g g-f
  where
  f : Trunc n (A × B) → Trunc n A × Trunc n B
  f = Trunc-rec (λ {(a , b) → [ a ] , [ b ]})

  g : Trunc n A × Trunc n B → Trunc n (A × B)
  g (ta , tb) = Trunc-rec (λ a → Trunc-rec (λ b → [ a , b ]) tb) ta

  f-g : ∀ p → f (g p) == p
  f-g (ta , tb) = Trunc-elim
    {P = λ ta → f (g (ta , tb)) == (ta , tb)}
    (λ a → Trunc-elim
      {P = λ tb → f (g ([ a ] , tb)) == ([ a ] , tb)}
      (λ b → idp)
      tb)
    ta

  g-f : ∀ tab → g (f tab) == tab
  g-f = Trunc-elim
    {P = λ tab → g (f tab) == tab}
    (λ ab → idp)

Trunc-×-conv : ∀ {i} {j} (n : ℕ₋₂) (A : Type i) (B : Type j)
  → Trunc n (A × B) == Trunc n A × Trunc n B
Trunc-×-conv n A B = ua (Trunc-×-econv n A B)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import HoTT
open import homotopy.HSpace renaming (HSpaceStructure to HSS)
open import homotopy.Pi2HSusp
open import homotopy.WedgeExtension
open import lib.types.TwoSemiCategory
open import lib.two-semi-categories.FundamentalCategory

module homotopy.Pi2HSuspCompose {i} {X : Ptd i} {{_ : has-level 1 (de⊙ X)}}
  {{is-0-connected : is-connected 0 (de⊙ X)}} (H-X : HSS X)
  (H-X-assoc : associator H-X)
  (coh-assoc-unit-l-r-pentagon : coh-unit-l-r-pentagon H-X H-X-assoc)
  where

  private
    A = de⊙ X
    e = pt X

  open Pi2HSusp H-X public

  infixr 80 _∙₁_
  _∙₁_ : {x y z : Susp A} → Trunc 1 (x == y) → Trunc 1 (y == z) → Trunc 1 (x == z)
  _∙₁_ {x} {y} {z} p q = _∙ₜ_ {A = Susp A} {ta = [ x ]} {tb = [ y ]} {tc = [ z ]} p q

  module _ {k} {B : Type k} where

    add-path-inverse-l : {x y z : B}
      → (p : x == y) (q : x == z)
      → p == (q ∙ ! q) ∙ p
    add-path-inverse-l p q = ap (_∙ p) (! (!-inv-r q))

    add-path-inverse-r : {x y z : B}
      → (p : x == y) (r : y == z)
      → p == p ∙ (r ∙ ! r)
    add-path-inverse-r p r =
      ! (∙-unit-r p) ∙ ap (p ∙_) (! (!-inv-r r))

    abstract
      add-path-inverse-coh : {x y : B} (p : x == x) (q : x == y)
        → add-path-inverse-r p q ◃∙
          ap (_∙ (q ∙ ! q)) (add-path-inverse-l p q) ◃∙
          ∙-assoc (q ∙ ! q) p (q ∙ ! q) ◃∎
          =ₛ
          add-path-inverse-l p q ◃∙
          ap ((q ∙ ! q) ∙_) (add-path-inverse-r p q) ◃∎
      add-path-inverse-coh p idp =
        add-path-inverse-r p idp ◃∙
        idp ◃∙
        idp ◃∎
          =ₛ⟨ 1 & 1 & expand [] ⟩
        add-path-inverse-r p idp ◃∙
        idp ◃∎
          =ₛ⟨ 1 & 1 & expand [] ⟩
        add-path-inverse-r p idp ◃∎
          =ₛ₁⟨ ! (ap-idf (add-path-inverse-r p idp)) ⟩
        ap (λ q → q) (add-path-inverse-r p idp) ◃∎
          =ₛ⟨ 0 & 0 & contract ⟩
        add-path-inverse-l p idp ◃∙
        ap (λ q → q) (add-path-inverse-r p idp) ◃∎ ∎ₛ

  comp-l-seq : (a' : A) → η (μ e a') =-= η e ∙ η a'
  comp-l-seq a' =
    η (μ e a')
      =⟪ ap η (μ.unit-l a') ⟫
    η a'
      =⟪ add-path-inverse-l (η a') (merid e) ⟫
    η e ∙ η a' ∎∎

  comp-l : (a' : A) → η (μ e a') == η e ∙ η a'
  comp-l a' = ↯ (comp-l-seq a')

  comp-r-seq : (a : A) → η (μ a e) =-= η a ∙ η e
  comp-r-seq a =
    η (μ a e)
      =⟪ ap η (μ.unit-r a) ⟫
    η a
      =⟪ add-path-inverse-r (η a) (merid e) ⟫
    η a ∙ η e ∎∎

  comp-r : (a : A) → η (μ a e) == η a ∙ η e
  comp-r a = ↯ (comp-r-seq a)

  comp-lr-coh : comp-l e == comp-r e
  comp-lr-coh =
    ap2 (λ p₁ p₂ → ap η p₁ ∙ p₂)
        μ.coh
        (add-path-inverse-lr-coh (merid e))
    where
    add-path-inverse-lr-coh : {B : Type i} {b b' : B} (p : b == b')
      → add-path-inverse-l (p ∙ ! p) p == add-path-inverse-r (p ∙ ! p) p
    add-path-inverse-lr-coh idp = idp

  comp-l₁ : (a' : A) → [ η (μ e a') ]₁ == [ η e ∙ η a' ]₁
  comp-l₁ = ap [_]₁ ∘ comp-l

  comp-r₁ : (a : A) → [ η (μ a e) ]₁ == [ η a ∙ η e ]₁
  comp-r₁ = ap [_]₁ ∘ comp-r

  comp-args : args {i} {i} {A} {e} {A} {e}
  comp-args =
    record {
      m = -1; n = -1;
      P = λ a a' → (Q a a' , ⟨⟩);
      f = comp-r₁;
      g = comp-l₁;
      p = ap (ap [_]₁) (! comp-lr-coh)
    }
    where
    Q : A → A → Type i
    Q a a' = [ η (μ a a' ) ]₁ == [ η a ∙ η a' ]₁

  module Comp = WedgeExt {i} {i} {A} {e} {A} {e} comp-args

  comp : (a a' : A) → [ η (μ a a') ]₁ == [ η a ]₁ ∙₁ [ η a' ]₁
  comp = Comp.ext

  comp-unit-l : (a' : A) → comp e a' == comp-l₁ a'
  comp-unit-l a' = Comp.β-r a'

  comp-unit-r : (a : A) → comp a e == comp-r₁ a
  comp-unit-r a = Comp.β-l a

  module CoherenceProof (a' : A) where

    P : A → A → Type i
    P a a'' =
      comp (μ a a') a'' ◃∙
      ap (_∙₁ [ η a'' ]₁) (comp a a') ◃∙
      ap [_]₁ (∙-assoc (η a) (η a') (η a'')) ◃∎
      =ₛ
      ap ([_]₁ ∘ η) (H-X-assoc a a' a'') ◃∙
      comp a (μ a' a'') ◃∙
      ap ([ η a ]₁ ∙₁_) (comp a' a'') ◃∎

    P-is-prop : ∀ a a'' → is-prop (P a a'')
    P-is-prop a a'' = =ₛ-level (Trunc-level {n = 1})

    Q  : A → A → hProp i
    Q a a'' = P a a'' , P-is-prop a a''

    inner-coh :
      comp-r (μ e a') ◃∙
      ap (_∙ η e) (comp-l a') ◃∙
      ∙-assoc (η e) (η a') (η e) ◃∎
      =ₛ
      ap η (H-X-assoc e a' e) ◃∙
      comp-l (μ a' e) ◃∙
      ap (η e ∙_) (comp-r a') ◃∎
    inner-coh =
      comp-r (μ e a') ◃∙
      ap (_∙ η e) (comp-l a') ◃∙
      ∙-assoc (η e) (η a') (η e) ◃∎
        =ₛ⟨ 0 & 1 & expand (comp-r-seq (μ e a')) ⟩
      ap η (μ.unit-r (μ e a')) ◃∙
      add-path-inverse-r (η (μ e a')) (merid e) ◃∙
      ap (_∙ η e) (comp-l a') ◃∙
      ∙-assoc (η e) (η a') (η e) ◃∎
        =ₛ⟨ 2 & 1 & ap-seq-∙ (_∙ η e) (comp-l-seq a') ⟩
      ap η (μ.unit-r (μ e a')) ◃∙
      add-path-inverse-r (η (μ e a')) (merid e) ◃∙
      ap (_∙ η e) (ap η (μ.unit-l a')) ◃∙
      ap (_∙ η e) (add-path-inverse-l (η a') (merid e)) ◃∙
      ∙-assoc (η e) (η a') (η e) ◃∎
        =ₛ⟨ 1 & 2 & !ₛ $
            homotopy-naturality-from-idf (_∙ η e)
                                         (λ r → add-path-inverse-r r (merid e))
                                         (ap η (μ.unit-l a')) ⟩
      ap η (μ.unit-r (μ e a')) ◃∙
      ap η (μ.unit-l a') ◃∙
      add-path-inverse-r (η a') (merid e) ◃∙
      ap (_∙ η e) (add-path-inverse-l (η a') (merid e)) ◃∙
      ∙-assoc (η e) (η a') (η e) ◃∎
        =ₛ⟨ 2 & 3 & add-path-inverse-coh (η a') (merid e) ⟩
      ap η (μ.unit-r (μ e a')) ◃∙
      ap η (μ.unit-l a') ◃∙
      add-path-inverse-l (η a') (merid e) ◃∙
      ap (η e ∙_) (add-path-inverse-r (η a') (merid e)) ◃∎
        =ₛ⟨ 0 & 2 & ap-seq-=ₛ η (coh-assoc-unit-l-r-pentagon a') ⟩
      ap η (H-X-assoc e a' e) ◃∙
      ap η (μ.unit-l (μ a' e)) ◃∙
      ap η (μ.unit-r a') ◃∙
      add-path-inverse-l (η a') (merid e) ◃∙
      ap (η e ∙_) (add-path-inverse-r (η a') (merid e)) ◃∎
        =ₛ⟨ 2 & 2 &
            homotopy-naturality-from-idf (η e ∙_)
                                         (λ v → add-path-inverse-l v (merid e))
                                         (ap η (μ.unit-r a')) ⟩
      ap η (H-X-assoc e a' e) ◃∙
      ap η (μ.unit-l (μ a' e)) ◃∙
      add-path-inverse-l (η (μ a' e)) (merid e) ◃∙
      ap (η e ∙_) (ap η (μ.unit-r a')) ◃∙
      ap (η e ∙_) (add-path-inverse-r (η a') (merid e)) ◃∎
        =ₛ⟨ 3 & 2 & ∙-ap-seq (η e ∙_) (comp-r-seq a')⟩
      ap η (H-X-assoc e a' e) ◃∙
      ap η (μ.unit-l (μ a' e)) ◃∙
      add-path-inverse-l (η (μ a' e)) (merid e) ◃∙
      ap (η e ∙_) (comp-r a') ◃∎
        =ₛ⟨ 1 & 2 & contract ⟩
      ap η (H-X-assoc e a' e) ◃∙
      comp-l (μ a' e) ◃∙
      ap (η e ∙_) (comp-r a') ◃∎ ∎ₛ

    coh : P e e
    coh =
      comp (μ e a') e ◃∙
      ap (_∙₁ [ η e ]₁) (comp e a') ◃∙
      ap [_]₁ (∙-assoc (η e) (η a') (η e)) ◃∎
        =ₛ₁⟨ 0 & 1 & comp-unit-r (μ e a') ⟩
      comp-r₁ (μ e a') ◃∙
      ap (_∙₁ [ η e ]₁) (comp e a') ◃∙
      ap [_]₁ (∙-assoc (η e) (η a') (η e)) ◃∎
        =ₛ₁⟨ 1 & 1 & step₂ ⟩
      comp-r₁ (μ e a') ◃∙
      ap [_]₁ (ap (_∙ η e) (comp-l a')) ◃∙
      ap [_]₁ (∙-assoc (η e) (η a') (η e)) ◃∎
        =ₛ⟨ 0 & 3 & ap-seq-=ₛ [_]₁ inner-coh ⟩
      ap [_]₁ (ap η (H-X-assoc e a' e)) ◃∙
      comp-l₁ (μ a' e) ◃∙
      ap [_]₁ (ap (η e ∙_) (comp-r a')) ◃∎
        =ₛ₁⟨ 0 & 1 & ∘-ap [_]₁ η (H-X-assoc e a' e) ⟩
      ap ([_]₁ ∘ η) (H-X-assoc e a' e) ◃∙
      comp-l₁ (μ a' e) ◃∙
      ap [_]₁ (ap (η e ∙_) (comp-r a')) ◃∎
        =ₛ₁⟨ 1 & 1 & ! (comp-unit-l (μ a' e)) ⟩
      ap ([_]₁ ∘ η) (H-X-assoc e a' e) ◃∙
      comp e (μ a' e) ◃∙
      ap [_]₁ (ap (η e ∙_) (comp-r a')) ◃∎
        =ₛ₁⟨ 2 & 1 & step₈ ⟩
      ap ([_]₁ ∘ η) (H-X-assoc e a' e) ◃∙
      comp e (μ a' e) ◃∙
      ap ([ η e ]₁ ∙₁_) (comp a' e) ◃∎ ∎ₛ
      where
      step₂ : ap (_∙₁ [ η e ]₁) (comp e a') == ap [_]₁ (ap (_∙ η e) (comp-l a'))
      step₂ =
        ap (_∙₁ [ η e ]₁) (comp e a')
          =⟨ ap (ap (_∙₁ [ η e ]₁)) (comp-unit-l a') ⟩
        ap (_∙₁ [ η e ]₁) (comp-l₁ a')
          =⟨ ∘-ap (_∙₁ [ η e ]₁) [_]₁ (comp-l a') ⟩
        ap ([_]₁ ∘ (_∙ η e)) (comp-l a')
          =⟨ ap-∘ [_]₁ (_∙ η e) (comp-l a') ⟩
        ap [_]₁ (ap (_∙ η e) (comp-l a')) =∎
      step₈ : ap [_]₁ (ap (η e ∙_) (comp-r a')) == ap ([ η e ]₁ ∙₁_) (comp a' e)
      step₈ =
        ap [_]₁ (ap (η e ∙_) (comp-r a'))
          =⟨ ∘-ap [_]₁ (η e ∙_) (comp-r a') ⟩
        ap (λ v → [ η e ∙ v ]₁) (comp-r a')
          =⟨ ap-∘ ([ η e ]₁ ∙₁_) [_]₁ (comp-r a') ⟩
        ap ([ η e ]₁ ∙₁_) (comp-r₁ a')
          =⟨ ! (ap (ap ([ η e ]₁ ∙₁_)) (comp-unit-r a')) ⟩
        ap ([ η e ]₁ ∙₁_) (comp a' e) =∎

  abstract
    comp-coh : (a a' a'' : A)
      → comp (μ a a') a'' ◃∙
        ap (λ v → v ∙₁ [ η a'' ]₁) (comp a a') ◃∙
        ap [_]₁ (∙-assoc (η a) (η a') (η a'')) ◃∎
        =ₛ
        ap ([_]₁ ∘ η) (H-X-assoc a a' a'') ◃∙
        comp a (μ a' a'') ◃∙
        ap (λ v → [ η a ] ∙₁ v) (comp a' a'') ◃∎
    comp-coh a a' a'' =
      prop-over-connected {A = A} {a = e} {{is-0-connected}}
                          (λ a → CoherenceProof.Q a' a a'')
                          (prop-over-connected {A = A} {a = e} {{is-0-connected}}
                                              (λ a'' → CoherenceProof.Q a' e a'')
                                              (CoherenceProof.coh a')
                                              a'')
                          a

  comp-functor : (pentagon : coh-assoc-pentagon H-X H-X-assoc)
    → TwoSemiFunctor
        (HSpace-2-semi-category H-X {{⟨⟩}} H-X-assoc pentagon)
        (=ₜ-fundamental-cat (Susp (de⊙ X)))
  comp-functor _ =
    record
    { F₀ = λ _ → [ north ]
    ; F₁ = λ x → [ η x ]
    ; pres-comp = comp
    ; pres-comp-coh = comp-coh
    }

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module Basics where

_%_ : {A B : Set}{C : B -> Set}
      (f : (x : B) -> C x)(g : A -> B)(x : A) -> C (g x)
f % g = \x -> f (g x)

-- Logic

data   False : Set where
record True  : Set where

tt : True
tt = _

¬_ : Set -> Set
¬ A = A -> False

record ∃ {A : Set}(P : A -> Set) : Set where
  field
    witness : A
    proof   : P witness

∃-intro : {A : Set}{P : A -> Set}(x : A) -> P x -> ∃ P
∃-intro x p = record { witness = x; proof = p }

infixr 15 _/\_ _×_

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

_/\_ = _×_

-- Maybe

data Lift (A : Set) : Set where
  bot  : Lift A
  lift : A -> Lift A

_=<<_ : {A B : Set} -> (A -> Lift B) -> Lift A -> Lift B
f =<< bot    = bot
f =<< lift v = f v

-- Nat

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

-- Identity

infix 10 _==_

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

data Id {A : Set}(x : A) : Set where
  it : (y : A) -> x == y -> Id x

-- Booleans

data Bool : Set where
  true  : Bool
  false : Bool

data LR : Set where
  left  : LR
  right : LR

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

-- Lists

infixr 50 _::_

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

data Elem {A : Set}(x : A) : List A -> Set where
  hd : forall {xs} -> Elem x (x :: xs)
  tl : forall {y xs} -> Elem x xs -> Elem x (y :: xs)


text:
module Cryptol where

open import Bool
open import Nat
open import Eq

postulate
  Int    : Set
  Float  : Set
  Char   : Set
  String : Set

{-# BUILTIN INTEGER Int    #-}
{-# BUILTIN FLOAT   Float  #-}
{-# BUILTIN CHAR    Char   #-}
{-# BUILTIN STRING  String #-}

data List (A : Set) : Set where
  Nil  : List A
  Cons : A → List A → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL Nil #-}
{-# BUILTIN CONS Cons #-}

append : {A : Set} → List A → List A → List A
append Nil ys         = ys
append (Cons x xs) ys = Cons x (append xs ys)

infixr 5 _::_

data Vec (A : Set) : ℕ → Set where
  Nil  : Vec A Z
  _::_ : {n : ℕ} → A → Vec A n → Vec A (S n)

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

data Bit : Set where
  O : Bit
  I : Bit

Word : ℕ → Set
Word n = Vec Bit n

data SnocView {A : Set} : List A → Set where
  Nil : SnocView Nil
  Snoc : (xs : List A) → (x : A) → SnocView (append xs (Cons x Nil))

view : {A : Set} → (xs : List A) → SnocView xs
view Nil = Nil
view (Cons x xs) with view xs
view (Cons x _)      | Nil = Snoc Nil x
view (Cons x _)      | Snoc ys y = Snoc (Cons x ys) y

rotateRight : {A : Set} → List A → List A
rotateRight xs with view xs
rotateRight _ | Nil       = Nil
rotateRight _ | Snoc ys y = Cons y ys

take : ∀ {A m} → (n : ℕ) → Vec A (n + m) → Vec A n
take Z l             = Nil
take (S k) (x :: xs) = x :: take k xs

drop : ∀ {A m} → (n : ℕ) → Vec A (n + m) → Vec A m
drop Z xs            = xs
drop (S k) (x :: xs) = drop k xs

split : ∀ {A} → (n : ℕ) → (m : ℕ) → Vec A (m × n) → Vec (Vec A n) m
split n Z     Nil = Nil
split n (S k) xs  = (take n xs) :: (split n k (drop n xs))

concat : ∀ {A n m} → Vec (Vec A n) m → Vec A (m × n)
concat Nil = Nil
concat (xs :: xss) = xs ++ concat xss

postulate
  splitConcatLemma : ∀ {A : Set} → (m : ℕ) → (n : ℕ) → (xs : Vec A (m × n)) → concat (split n m xs) ≡ xs

takeDropLemma : ∀ {A : Set} → (n : ℕ) → (m : ℕ) → (xs : Vec A (n + m)) → ((take n xs) ++ (drop n xs)) ≡ xs
takeDropLemma Z m _ = Refl
takeDropLemma (S k) m (x :: xs) with ((take k xs) ++ (drop k xs)) | takeDropLemma k _ xs
takeDropLemma (S k) m (x :: xs) | ._ | Refl = Refl

data SplitView {A : Set} : {n : ℕ} → (m : ℕ) → Vec A (m × n) → Set where
 [_] : ∀ {m n} → (xss : Vec (Vec A n) m) → SplitView m (concat xss)

splitView : {A : Set} → (n : ℕ) → (m : ℕ) → (xs : Vec A (m × n)) → SplitView m xs
splitView n m xs with concat (split n m xs) | [ split n m xs ] | splitConcatLemma m n xs
splitView n m xs | _ | v | Refl = v

data TakeView (A : Set) (m : ℕ) (n : ℕ) : Vec A (m + n) → Set where
  Take : (xs : Vec A m) → (ys : Vec A n) → TakeView A m n (xs ++ ys)

--sv : {A : Set} → (n : ℕ) → (m : ℕ) → Vec a

swab : Word 32 → Word 32
swab xs with splitView 8 4 xs
swab _ | [ a :: b :: c :: d :: Nil ] = concat (b :: a :: c :: d :: Nil)

max_stars_repo_name: mjhopkins/PowerOfPi

max_issues_repo_name: mjhopkins/PowerOfPi

max_forks_repo_name: mjhopkins/PowerOfPi


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

open import Setoids.Setoids
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Groups.Definition
open import Groups.Actions.Definition
open import Sets.EquivalenceRelations

module Groups.Actions.Orbit where

data Orbit {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) : Set (a ⊔ b ⊔ c ⊔ d) where
  orbitElt : (g : A) → Orbit action x

orbitSetoid : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Setoid (Orbit action x)
Setoid._∼_ (orbitSetoid {T = T} action x) (orbitElt a) (orbitElt b) = Setoid._∼_ T (GroupAction.action action a x) (GroupAction.action action b x)
Equivalence.reflexive (Setoid.eq (orbitSetoid {T = T} action x)) {orbitElt g} = Equivalence.reflexive (Setoid.eq T)
Equivalence.symmetric (Setoid.eq (orbitSetoid {T = T} action x)) {orbitElt g} {orbitElt h} = Equivalence.symmetric (Setoid.eq T)
Equivalence.transitive (Setoid.eq (orbitSetoid {T = T} action x)) {orbitElt g} {orbitElt h} {orbitElt i} = Equivalence.transitive (Setoid.eq T)


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.Properties where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat renaming(_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec
open import Cubical.Data.Vec.OperationsNat

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Multivariate.Base

private variable
  ℓ ℓ' : Level

module Nth-Poly-structure (A' : CommRing ℓ) (n : ℕ) where

  private
    A = fst A'
    Ar = CommRing→Ring A'

  open CommRingStr (snd A')
  open RingTheory Ar

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

  poly-com-adv : (P Q R S : Poly A' n) →  ((P poly+ Q) poly+ (R poly+ S) ≡ (P poly+ R) poly+ (Q poly+ S))
  poly-com-adv P Q R S = ((P poly+ Q) poly+ (R poly+ S)  ≡⟨ poly+Assoc (P poly+ Q) R S ⟩
                         (((P poly+ Q) poly+ R) poly+ S) ≡⟨ cong (λ X → X poly+ S) (sym (poly+Assoc P Q R)) ⟩
                         ((P poly+ (Q poly+ R)) poly+ S) ≡⟨ cong (λ X → (P poly+ X) poly+ S) (poly+Comm Q R) ⟩
                         ((P poly+ (R poly+ Q)) poly+ S) ≡⟨ cong (λ X → X poly+ S) (poly+Assoc P R Q) ⟩
                         (((P poly+ R) poly+ Q) poly+ S) ≡⟨ sym (poly+Assoc (P poly+ R) Q S) ⟩
                         ((P poly+ R) poly+ (Q poly+ S)) ∎)

  poly+IdL : (P : Poly A' n) → 0P poly+ P ≡ P
  poly+IdL P = (poly+Comm 0P P) ∙ (poly+IdR P)

  polyInv : Poly A' n → Poly A' n
  polyInv = Poly-Rec-Set.f A' n (Poly A' n) trunc
            0P
            (λ v a → base v (- a))
            (λ PS RS → PS poly+ RS)
            poly+Assoc
            poly+IdR
            poly+Comm
            (λ v → base v (- 0r) ≡⟨ cong (base v) 0Selfinverse ⟩ base v 0r ≡⟨ base-0P v ⟩ 0P ∎)
            λ v a b → (base-poly+ v (- a) (- b)) ∙ (cong (base v) (-Dist a b))

  polyInvol : (P : Poly A' n) → polyInv (polyInv P) ≡ P
  polyInvol = Poly-Ind-Prop.f A' n (λ P → polyInv (polyInv P) ≡ P) (λ _ → trunc _ _)
              refl
              (λ v a → cong (base v) (-Idempotent a))
              λ {P Q} ind-P ind-Q → cong₂ _poly+_ ind-P ind-Q

  poly+InvR : (P : Poly A' n ) → P poly+ (polyInv P) ≡ 0P
  poly+InvR = Poly-Ind-Prop.f A' n (λ P → (P poly+ polyInv P) ≡ 0P) (λ _ → trunc _ _)
              (poly+IdR 0P)
              (λ v a → (base-poly+ v a (- a)) ∙ cong (base v) (+Rinv a) ∙ base-0P v)
              λ {P Q} ind-P ind-Q → ((P poly+ Q) poly+ ((polyInv P) poly+ (polyInv Q)))
                                              ≡⟨ poly-com-adv P Q (polyInv P) (polyInv Q) ⟩
                                     ((P poly+ polyInv P) poly+ (Q poly+ polyInv Q))
                                              ≡⟨ cong₂ _poly+_ ind-P ind-Q ⟩
                                     (0P poly+ 0P)
                                              ≡⟨ poly+IdR 0P ⟩
                                     0P ∎

  poly+InvL : (P  : Poly A' n) → (polyInv P) poly+ P ≡ 0P
  poly+InvL = Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
              (poly+IdR 0P)
              (λ v a → (base-poly+ v (- a) a) ∙ cong (base v) (snd (+Inv a)) ∙ base-0P v)
              λ {U V} ind-U ind-V → poly-com-adv (polyInv U) (polyInv V) U V
                                     ∙ cong₂ _poly+_ ind-U ind-V
                                     ∙ poly+IdR 0P

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

  _poly*_ : Poly A' n → Poly A' n → Poly A' n
  _poly*_ = -- Induction Left Argument
            Poly-Rec-Set.f A' n (Poly A' n → Poly A' n)
            (λ f g p q i j Q → trunc (f Q) (g Q) (λ X → p X Q) (λ X → q X Q) i j )
            (λ Q    → 0P)
            (λ v a  → -- Induction Right Argument
                       Poly-Rec-Set.f A' n (Poly A' n) trunc
                       0P
                       (λ v' a' → base (v +n-vec v') (a · a'))
                       _poly+_
                       poly+Assoc
                       poly+IdR
                       poly+Comm
                       (λ v' → (cong (base (v +n-vec v')) (0RightAnnihilates a)) ∙ (base-0P (v +n-vec v')))
                       λ v' b c → (base-poly+ (v +n-vec v') (a · b) (a · c))
                                   ∙ (cong (base (v +n-vec v')) (sym (·Rdist+ a b c))))
                       -- End Right induction
            (λ PS QS Q → (PS Q) poly+ (QS Q) )
            (λ PS QS RS i Q → poly+Assoc (PS Q) (QS Q) (RS Q) i)
            (λ PS i Q       → poly+IdR (PS Q) i)
            (λ PS QS i Q    → poly+Comm (PS Q) (QS Q) i)
            (λ v    → funExt (
                             -- Induction Right Argument
                             Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                             refl
                             (λ v' a' → (cong (base (v +n-vec v')) (0LeftAnnihilates a')) ∙ (base-0P (v +n-vec v')))
                             λ {P Q} ind-P ind-Q → (cong₂ _poly+_ ind-P ind-Q) ∙ (poly+IdR 0P) ))
                             -- End Right Induction
            λ v a b → funExt (
                             -- Induction Right Argument
                             Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                             (poly+IdR 0P)
                             (λ v' c → (base-poly+ (v +n-vec v') (a · c) (b · c))
                                        ∙ (cong (base (v +n-vec v')) (sym (·Ldist+ a b c))))
                             λ {P Q} ind-P ind-Q → (poly-com-adv _ _ _ _) ∙ (cong₂ _poly+_ ind-P ind-Q))
                             -- End Right Induction
            -- End Left Induction

  poly*Assoc : (P Q R : Poly A' n) → P poly* (Q poly* R) ≡ (P poly* Q) poly* R
  poly*Assoc = Poly-Ind-Prop.f A' n _
                (λ P p q i Q R j → trunc (P poly* (Q poly* R)) ((P poly* Q) poly* R) (p Q R) (q Q R) i j)
                (λ _ _ → refl)
                (λ v a → Poly-Ind-Prop.f A' n _
                          (λ Q p q i R j → trunc (base v a poly* (Q poly* R)) ((base v a poly* Q) poly* R) (p R) (q R) i j)
                          (λ _ → refl)
                          (λ v' a' → Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                                      refl
                                      (λ v'' a'' → cong₂ base (+n-vec-assoc v v' v'') (·Assoc a a' a''))
                                      (λ {U V} ind-U ind-V → cong₂ _poly+_ ind-U ind-V))
                          (λ {U V} ind-U ind-V R → cong₂ _poly+_ (ind-U R) (ind-V R)))
                λ {U V} ind-U ind-V Q R → cong₂ _poly+_ (ind-U Q R) (ind-V Q R)

  poly*AnnihilL : (P : Poly A' n) → 0P poly* P ≡ 0P
  poly*AnnihilL P = refl

  poly*AnnihilR : (P : Poly A' n) → P poly* 0P ≡ 0P
  poly*AnnihilR = Poly-Ind-Prop.f A' n (λ P → (P poly* 0P) ≡ 0P) (λ _ → trunc _ _)
                           refl
                           (λ _ _ → refl)
                           λ {P Q} ind-P ind-Q → (cong₂ _poly+_ ind-P ind-Q) ∙ (poly+IdR 0P)

  1P : Poly A' n
  1P = base (replicate zero) 1r

  poly*IdR : (P : Poly A' n) → P poly* 1P ≡ P
  poly*IdR = Poly-Ind-Prop.f A' n (λ P → (P poly* 1P) ≡ P) (λ _ → trunc _ _)
              refl
              (λ v a → cong₂ base (+n-vec-rid v) (·Rid a))
              (λ {P Q} ind-P ind-Q → cong₂ _poly+_ ind-P ind-Q)

  poly*IdL : (P : Poly A' n) → 1P poly* P ≡ P
  poly*IdL = Poly-Ind-Prop.f A' n (λ P → (1P poly* P) ≡ P) (λ _ → trunc _ _)
              refl
              (λ v a → cong₂ base (+n-vec-lid v) (·Lid a))
              λ {P Q} ind-P ind-Q → cong₂ _poly+_ ind-P ind-Q

  poly*DistR : (P Q R : Poly A' n) → P poly* (Q poly+ R) ≡ (P poly* Q) poly+ (P poly* R)
  poly*DistR = Poly-Ind-Prop.f A' n _
               (λ P p q i Q R j → trunc (P poly* (Q poly+ R)) ((P poly* Q) poly+ (P poly* R)) (p Q R) (q Q R) i j)
               (λ _ _ → sym (poly+IdR 0P))
               (λ v a → λ Q R → refl)
               λ {U V} ind-U ind-V Q R → (cong₂ _poly+_ (ind-U Q R) (ind-V Q R)) ∙ poly-com-adv (U poly* Q) (U poly* R) (V poly* Q) (V poly* R)

  poly*DistL : (P Q R : Poly A' n) → (P poly+ Q) poly* R ≡ (P poly* R) poly+ (Q poly* R)
  poly*DistL P Q R = refl

  poly*Comm : (P Q : Poly A' n) → P poly* Q ≡ Q poly* P
  poly*Comm = Poly-Ind-Prop.f A' n _
              (λ P p q i Q j → trunc (P poly* Q) (Q poly* P) (p Q) (q Q) i j)
              (λ Q → sym (poly*AnnihilR Q))
              (λ v a → Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                        refl
                        (λ v' a' → cong₂ base (+n-vec-comm v v') (·Comm a a'))
                        (λ {U V} ind-U ind-V → cong₂ _poly+_ ind-U ind-V))
              λ {U V} ind-U ind-V Q → ((cong₂ _poly+_ (ind-U Q) (ind-V Q)) ∙ sym (poly*DistR Q U V))

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
module AKS.Binary where

open import AKS.Binary.Base public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
import      Lvl

module Structure.Category.Category {ℓₒ ℓₘ ℓₑ : Lvl.Level} where

open import Structure.Category
open import Structure.Category.Functor.Equiv
open import Structure.Category.Functor
import      Structure.Category.Functor.Functors as Functors
open import Structure.Category.Functor.Functors.Proofs

open CategoryObject
open Functors.Wrapped

categoryCategory : Category{Obj = CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}} (_→ᶠᵘⁿᶜᵗᵒʳ_)
Category._∘_            categoryCategory = _∘ᶠᵘⁿᶜᵗᵒʳ_
Category.id             categoryCategory = idᶠᵘⁿᶜᵗᵒʳ
Category.binaryOperator categoryCategory = [∘ᶠᵘⁿᶜᵗᵒʳ]-binaryOperator
Category.associativity  categoryCategory = [∘ᶠᵘⁿᶜᵗᵒʳ]-associativity
Category.identity       categoryCategory = [∘ᶠᵘⁿᶜᵗᵒʳ]-identity

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K --safe #-}
-- verbatim dual of Categories.Category.Construction.Properties.Kleisli
module Categories.Category.Construction.Properties.CoKleisli where

open import Level
import Relation.Binary.PropositionalEquality as ≡

open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Category
open import Categories.Functor using (Functor; _∘F_)
open import Categories.Functor.Equivalence
open import Categories.Comonad
import Categories.Morphism.Reasoning as MR

open import Categories.Adjoint.Construction.CoKleisli
open import Categories.Category.Construction.CoKleisli

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

module _ {F : Functor 𝒞 𝒟} {G : Functor 𝒟 𝒞} (F⊣G : Adjoint F G) where
  private
    T : Comonad 𝒟
    T = adjoint⇒comonad F⊣G

    𝒟ₜ : Category _ _ _
    𝒟ₜ = CoKleisli T

    module 𝒞 = Category 𝒞
    module 𝒟 = Category 𝒟
    module 𝒟ₜ = Category 𝒟ₜ

    module T = Comonad T
    module F = Functor F
    module G = Functor G

    open Adjoint F⊣G

  -- Maclane's Comparison Functor
  ComparisonF : Functor 𝒟ₜ 𝒞
  ComparisonF = record
   { F₀ = λ X → G.F₀ X
   ; F₁ = λ {A} {B} f → 𝒞 [ (G.F₁ f) ∘ unit.η (G.F₀ A) ]
   ; identity = λ {A} → zag
   ; homomorphism = λ {X} {Y} {Z} {f} {g} → begin
      G.F₁ (g 𝒟.∘ F.F₁ (G.F₁ f) 𝒟.∘ F.F₁ (unit.η (G.F₀ X))) 𝒞.∘ unit.η (G.F₀ X)             ≈⟨ pushˡ G.homomorphism ⟩
      G.F₁ g 𝒞.∘ G.F₁ ((F.F₁ (G.F₁ f)) 𝒟.∘ F.F₁ (unit.η (G.F₀ X))) 𝒞.∘ unit.η (G.F₀ X)      ≈⟨ (refl⟩∘⟨ pushˡ G.homomorphism) ⟩
      G.F₁ g 𝒞.∘ G.F₁ (F.F₁ (G.F₁ f)) 𝒞.∘ G.F₁ (F.F₁ (unit.η (G.F₀ X))) 𝒞.∘ unit.η (G.F₀ X) ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ sym (unit.commute (unit.η (G.F₀ X))))) ⟩
      G.F₁ g 𝒞.∘ G.F₁ (F.F₁ (G.F₁ f)) 𝒞.∘ unit.η (G.F₀ (F.F₀ (G.F₀ X))) 𝒞.∘ unit.η (G.F₀ X) ≈⟨ (refl⟩∘⟨ pullˡ (sym (unit.commute (G.F₁ f)))) ⟩
      G.F₁ g 𝒞.∘ (unit.η (G.F₀ Y) 𝒞.∘ G.F₁ f) 𝒞.∘ unit.η (G.F₀ X)                           ≈⟨ MR.assoc²'' 𝒞 ⟩
      (G.F₁ g 𝒞.∘ unit.η (G.F₀ Y)) 𝒞.∘ G.F₁ f 𝒞.∘ unit.η (G.F₀ X)                           ∎
   ; F-resp-≈ = λ eq → 𝒞.∘-resp-≈ (G.F-resp-≈ eq) (Category.Equiv.refl 𝒞)
   }
   where
    open 𝒞.HomReasoning
    open 𝒞.Equiv
    open MR 𝒞

  private
    L = ComparisonF
    module L = Functor L
    module Gₜ = Functor (Forgetful T)
    module Fₜ = Functor (Cofree T)

  F∘L≡Forgetful : (F ∘F L) ≡F Forgetful T
  F∘L≡Forgetful = record
   { eq₀ = λ X → ≡.refl
   ; eq₁ = eq-1
   }
   where
   open 𝒟.HomReasoning
   open MR 𝒟
   eq-1 : {X Y : 𝒟.Obj} (f : F.F₀ (G.F₀ X) 𝒟.⇒ Y) → 𝒟.id 𝒟.∘ F.F₁ (G.F₁ f 𝒞.∘ unit.η (G.F₀ X)) 𝒟.≈ (F.F₁ (G.F₁ f) 𝒟.∘ F.F₁ (unit.η (G.F₀ X))) 𝒟.∘ 𝒟.id
   eq-1 {X} {Y} f = begin
    𝒟.id 𝒟.∘ F.F₁ (G.F₁ f 𝒞.∘ unit.η (G.F₀ X))          ≈⟨ id-comm-sym ⟩
    F.F₁ (G.F₁ f 𝒞.∘ unit.η (G.F₀ X)) 𝒟.∘ 𝒟.id          ≈⟨ (F.homomorphism ⟩∘⟨refl) ⟩
    (F.F₁ (G.F₁ f) 𝒟.∘ F.F₁ (unit.η (G.F₀ X))) 𝒟.∘ 𝒟.id ∎

  L∘Cofree≡G : (L ∘F Cofree T) ≡F G
  L∘Cofree≡G = record
   { eq₀ = λ X → ≡.refl
   ; eq₁ = eq-1
   }
   where
   open 𝒞.HomReasoning
   open MR 𝒞
   eq-1 : {X Y : 𝒟.Obj} (f : X 𝒟.⇒ Y) → 𝒞.id 𝒞.∘ G.F₁ (f 𝒟.∘ counit.η X) 𝒞.∘ unit.η (G.F₀ X) 𝒞.≈ G.F₁ f 𝒞.∘ 𝒞.id
   eq-1 {X} {Y} f = begin
    𝒞.id 𝒞.∘ G.F₁ (f 𝒟.∘ counit.η X) 𝒞.∘ unit.η (G.F₀ X)         ≈⟨ id-comm-sym ⟩
    (G.F₁ (f 𝒟.∘ counit.η X) 𝒞.∘ unit.η (G.F₀ X)) 𝒞.∘ 𝒞.id       ≈⟨ (pushˡ G.homomorphism ⟩∘⟨refl) ⟩
    (G.F₁ f 𝒞.∘ G.F₁ (counit.η X) 𝒞.∘ unit.η (G.F₀ X)) 𝒞.∘ 𝒞.id  ≈⟨ (elimʳ zag ⟩∘⟨refl) ⟩
    G.F₁ f 𝒞.∘ 𝒞.id                                              ∎

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module PatternSynonymImports2 where

open import PatternSynonyms
open import PatternSynonymImports

myzero' = z
myzero'' = myzero

list2 : List _
list2 = 1 ∷ []

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

{- This brief section introduces an alternative definition
   of n-connectedness defined purely using propositional truncation,
   in contrast to the standard one using n-truncations
   (The below observation has resulted in Exercise 7.6 of
   the HoTT book being modified accordingly).

   In detail, a type A is usually called n-connected if Trunc n A
   is contractible. Here, we show that n-connectedness of A can also
   be defined recursively as follows:
   * A is (-2)-connected,
   * A is (n+1)-connected iff A is merely inhabited and for all a₀, a₁ : A,
     the path space a₀ == a₁ is n-connected.

   This module is independent from the other files in this directory,
   using only the truncations with definitional computation from the library. -}
module Universe.Trunc.ConnectednessAlt where

open import lib.Basics
open import lib.NConnected
open import lib.NType2
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.TLevel
open import lib.types.Truncation
open import lib.types.Unit

open import Universe.Utility.General
open import Universe.Utility.TruncUniverse

-- Preliminary lemmata.
module _ where

  {- The structural lemma for the below equivalence of connectedness notions:
    Contractibility is equivalent to propositionality and mere inhabitation. -}
  contr-decompose : ∀ {i} {A : Type i} → is-contr A ≃ (Trunc ⟨-1⟩ A × is-prop A)
  contr-decompose {i} {A} = prop-equiv h k f g where
    h = is-contr-is-prop
    k = snd ((_ , Trunc-level) ×-≤ (_ , is-prop-is-prop))
    f = λ c → ([ fst c ] , contr-is-prop c)
    g = λ {(ta , s) → Trunc-rec h (flip inhab-prop-is-contr s) ta}

-- Everything here will happen in universe Type i.
module _ {i} where
  module _ {n : ℕ₋₂} where
    -- The dependent universal property over n-types.
    Trunc-dup : (A : Type i) (B : (ta : Trunc n A) → n -Type i)
              → Π (Trunc n A) (⟦_⟧ ∘ B) ≃ Π A (⟦_⟧ ∘ B ∘ [_])
    Trunc-dup A B = equiv
      (λ f → f ∘ [_]) (Trunc-elim (snd ∘ B)) (λ _ → idp)
      (λ f → λ= (Trunc-elim (snd ∘ (λ a → Path-≤ (B a) _ _)) (λ a → idp)))

    {- The truncation functor is applicative (here only a special case).
       Note the more elegant alternative of using the approach
       from TypeConstructors.agda with unicity of truncations. -}
    Trunc-×-equiv : {A B : Type i} → Trunc n (A × B) ≃ (Trunc n A × Trunc n B)
    Trunc-×-equiv {A} {B} = equiv f g f-g g-f where
      f = λ t → (Trunc-fmap fst t , Trunc-fmap snd t)
      g = λ {(ta , tb) → Trunc-rec Trunc-level
                  (λ a → Trunc-rec Trunc-level
                  (λ b → [ (a , b) ]) tb) ta}

      f-g = λ {(ta , tb) → Trunc-elim (λ ta → snd (T (ta , tb)))
                    (λ a → Trunc-elim (λ tb → snd (T ([ a ] , tb)))
                    (λ b → idp) tb) ta} where
        T : Trunc n A × Trunc n B → n -Type i
        T ts = Path-≤ ((_ , Trunc-level) ×-≤ (_ , Trunc-level)) (f (g ts)) ts

      g-f = Trunc-elim (λ _ → snd (Path-≤ (_ , Trunc-level) _ _)) (λ a → idp)

  {- The connectedness predicate from the library:
     is-connected : ℕ₋₂ → Type i → Type i
     is-connected n A = is-contr (Trunc n A) -}

  -- Our connectedness predicate defined using only propositional truncation.
  is-connected' : ℕ₋₂ → Type i → Type i
  is-connected' ⟨-2⟩  A = Lift ⊤
  is-connected' (S n) A = Trunc ⟨-1⟩ A × ((as : A × A) → is-connected' n (fst as == snd as))

  -- Both notions coincide.
  connected-equiv : (n : ℕ₋₂) (A : Type i) → is-connected n A ≃ is-connected' n A
  connected-equiv ⟨-2⟩  A = lift-equiv ⁻¹
                         ∘e contr-equiv-Unit (inhab-prop-is-contr Trunc-level is-contr-is-prop)

  connected-equiv (S n) A = equiv-Σ (fuse-Trunc A _ _) (λ _ → e) ∘e contr-decompose where
    e = is-prop (Trunc (S n) A)
      ≃⟨ curry-equiv ⁻¹ ⟩
        Π (Trunc (S n) A × Trunc (S n) A) (is-contr ∘ uncurry _==_)
      ≃⟨ equiv-Π-l _ (snd Trunc-×-equiv) ⁻¹ ⟩
        Π (Trunc (S n) (A × A)) (is-contr ∘ uncurry _==_ ∘ _)
      ≃⟨ Trunc-dup (A × A) (λ _ → (_ , raise-level-≤T (≤T-ap-S (-2≤T n)) is-contr-is-prop)) ⟩
        ((as : A × A) → is-contr ([ fst as ] == [ snd as ]))
      ≃⟨ equiv-Π-r (λ _ → equiv-level (Trunc=-equiv _ _)) ⟩
        Π (A × A) (is-connected n ∘ uncurry _==_)
      ≃⟨ equiv-Π-r (λ _ → connected-equiv n _) ⟩
        Π (A × A) (is-connected' n ∘ uncurry _==_)
      ≃∎

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
module Nat.Binary where

open import Data.Bool hiding (_≤_; _<_; _<?_)
open import Data.Empty
open import Data.List
open import Data.List.Properties
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Function
open import Nat.Class
open import Nat.Unary
  using (ℕ₁)
  renaming
    (zero to zero₁
    ; succ to succ₁
    ; _+_ to _+₁_
    ; rec to rec₁
    ; ind to ind₁
    ; rec-succ to rec₁-succ
    )
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open ≡-Reasoning

data ℕ₂ : Set where
  zero : ℕ₂
  pos : List Bool → ℕ₂

ind :
  (P : ℕ₂ → Set) →
  P zero →
  P (pos []) →
  (∀ {b bs} → P (pos bs) → P (pos (b ∷ bs))) →
  ∀ n →
  P n
ind P z u d zero = z
ind P z u d (pos []) = u
ind P z u d (pos (b ∷ bs)) = d (ind P z u d (pos bs))

succ⁺ : List Bool → List Bool
succ⁺ [] = false ∷ []
succ⁺ (false ∷ bs) = true ∷ bs
succ⁺ (true ∷ bs) = false ∷ succ⁺ bs

succ : ℕ₂ → ℕ₂
succ zero = pos []
succ (pos bs) = pos (succ⁺ bs)

-- TODO: try to build a rec implementation that computes the
-- predecessor to do unary recursion on binary numbers!  However, the
-- predecessor function must return a proof showing that its result is
-- less than its argument, otherwise Agda doesn't know if the
-- recursion will terminate

digitsFold : {B : Set} → (B → Bool → Bool → B) → B → ℕ₂ → ℕ₂ → B
digitsFold f z zero zero =
  f z false false
digitsFold f z zero (pos []) =
  f z false true
digitsFold f z zero (pos (b₂ ∷ bs₂)) =
  digitsFold f (f z false b₂) zero (pos bs₂)
digitsFold f z (pos []) zero =
  f z true false
digitsFold f z (pos []) (pos []) =
  f z true true
digitsFold f z (pos []) (pos (b₂ ∷ bs₂)) =
  digitsFold f (f z true b₂) zero (pos bs₂)
digitsFold f z (pos (b₁ ∷ bs₁)) zero =
  digitsFold f (f z b₁ false) (pos bs₁) zero
digitsFold f z (pos (b₁ ∷ bs₁)) (pos []) =
  digitsFold f (f z b₁ true) (pos bs₁) zero
digitsFold f z (pos (b₁ ∷ bs₁)) (pos (b₂ ∷ bs₂)) =
  digitsFold f (f z b₁ b₂) (pos bs₁) (pos bs₂)

adder : List Bool × Bool → Bool → Bool → List Bool × Bool
adder (bs , c) a b = (c xor (a xor b)) ∷ bs , (c ∧ (a xor b)) ∨ (a ∧ b)

revNormalize : List Bool → ℕ₂ → ℕ₂
revNormalize [] acc = acc
revNormalize (b ∷ rxs) (pos acc) = revNormalize rxs (pos (b ∷ acc))
revNormalize (false ∷ rxs) zero = revNormalize rxs zero
revNormalize (true ∷ rxs) zero = revNormalize rxs (pos [])

_+_ : ℕ₂ → ℕ₂ → ℕ₂
m + n =
  let rs , c = digitsFold adder ([] , false) m n
   in revNormalize (c ∷ rs) zero

_ : zero + zero ≡ zero
_ =
  begin
    zero + zero
  ≡⟨⟩
    let rs , c = digitsFold adder ([] , false) zero zero
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs , c = adder ([] , false) false false
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs = (false xor (false xor false)) ∷ []
        c = (false ∧ (false xor false)) ∨ (false ∧ false)
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs = false ∷ []
        c = false
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
     revNormalize (false ∷ false ∷ []) zero
  ≡⟨⟩
     revNormalize (false ∷ []) zero
  ≡⟨⟩
     revNormalize [] zero
  ≡⟨⟩
    zero
  ∎

_ : zero + pos [] ≡ pos []
_ =
  begin
    zero + pos []
  ≡⟨⟩
    let rs , c = digitsFold adder ([] , false) zero (pos [])
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs , c = adder ([] , false) false true
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs = (false xor (false xor true)) ∷ []
        c = (false ∧ (false xor true)) ∨ (false ∧ true)
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs = true ∷ []
        c = false
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
     revNormalize (false ∷ true ∷ []) zero
  ≡⟨⟩
     revNormalize (true ∷ []) zero
  ≡⟨⟩
     revNormalize [] (pos [])
  ≡⟨⟩
    pos []
  ∎

_ : zero + pos (false ∷ []) ≡ pos (false ∷ [])
_ =
  begin
    zero + pos (false ∷ [])
  ≡⟨⟩
    let rs , c = digitsFold adder ([] , false) zero (pos (false ∷ []))
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs , c = digitsFold adder (adder ([] , false) false false) zero (pos [])
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let bs′ = (false xor (false xor false)) ∷ []
        c′ = (false ∧ (false xor false)) ∨ (false ∧ false)
        rs , c = digitsFold adder (bs′ , c′) zero (pos [])
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs , c = digitsFold adder (false ∷ [] , false) zero (pos [])
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs , c = adder (false ∷ [] , false) false true
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs = (false xor (false xor true)) ∷ false ∷ []
        c = (false ∧ (false xor true)) ∨ (false ∧ true)
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
     revNormalize (false ∷ true ∷ false ∷ []) zero
  ≡⟨⟩
     revNormalize (true ∷ false ∷ []) zero
  ≡⟨⟩
     revNormalize (false ∷ []) (pos [])
  ≡⟨⟩
     revNormalize [] (pos (false ∷ []))
  ≡⟨⟩
    pos (false ∷ [])
  ∎

-- TODO Expand more zero + n examples
reverse-∷ :
  {A : Set} {x : A} {xs : List A} →
  reverse (x ∷ xs) ≡ reverse xs ++ (x ∷ [])
reverse-∷ {A} {x} {xs} =
  begin
    reverse (x ∷ xs)
  ≡⟨⟩
    foldl (flip _∷_) [] (x ∷ xs)
  ≡⟨⟩
    foldl (flip _∷_) (flip _∷_ [] x) xs
  ≡⟨⟩
    foldl (flip _∷_) (x ∷ []) xs
  ≡⟨ {!!} ⟩
    foldl (flip _∷_) [] xs ++ (x ∷ [])
  ≡⟨⟩
    reverse xs ++ (x ∷ [])
  ∎

reverse-∷-++ :
  {A : Set} {x : A} {xs ys : List A} →
  reverse (x ∷ xs) ++ ys ≡ reverse xs ++ x ∷ ys
reverse-∷-++ {A} {x} {[]} {ys} = refl
reverse-∷-++ {A} {x} {x′ ∷ xs′} {ys} =
  begin
    reverse (x ∷ x′ ∷ xs′) ++ ys
  ≡⟨ {!!} ⟩
    reverse (x′ ∷ xs′) ++ x ∷ ys
  ∎

adder-ca-false : ∀ {b bs} → adder (bs , false) false b ≡ (b ∷ bs , false)
adder-ca-false = refl

digitsFold-adder-zeroˡ-carry :
  ∀ {bs n} → proj₂ (digitsFold adder (bs , false) zero n) ≡ false
digitsFold-adder-zeroˡ-carry {n = zero} = refl
digitsFold-adder-zeroˡ-carry {n = pos []} = refl
digitsFold-adder-zeroˡ-carry {n = pos (b ∷ bs₂)} =
  digitsFold-adder-zeroˡ-carry {n = pos bs₂}

digitsFold-adder-zeroˡ-sum :
  ∀ {rs bs} →
  proj₁ (digitsFold adder (rs , false) zero (pos bs)) ≡ true ∷ reverse bs ++ rs
digitsFold-adder-zeroˡ-sum {rs} {[]} = refl
digitsFold-adder-zeroˡ-sum {rs} {b ∷ bs} =
  begin
    proj₁ (digitsFold adder (rs , false) zero (pos (b ∷ bs)))
  ≡⟨⟩
    proj₁ (digitsFold adder (b ∷ rs , false) zero (pos bs))
  ≡⟨ digitsFold-adder-zeroˡ-sum {b ∷ rs} {bs} ⟩
    true ∷ reverse bs ++ b ∷ rs
  ≡⟨ {!!} ⟩
    true ∷ reverse (b ∷ bs) ++ rs
  ∎

+-identityˡ : ∀ {n} → zero + n ≡ n
+-identityˡ {zero} = refl
+-identityˡ {pos []} = refl
+-identityˡ {pos (b ∷ bs)} =
  begin
    zero + pos (b ∷ bs)
  ≡⟨⟩
    let rs , c = digitsFold adder ([] , false) zero (pos (b ∷ bs))
     in revNormalize (c ∷ rs) zero
  ≡⟨⟩
    let rs , c = digitsFold adder (adder ([] , false) false b) zero (pos bs)
     in revNormalize (c ∷ rs) zero
  ≡⟨ {!!} ⟩
    pos (b ∷ bs)
  ∎

fromℕ₁ : ℕ₁ → ℕ₂
fromℕ₁ = rec₁ zero succ

fromℕ₁-succ : ∀ n → fromℕ₁ (succ₁ n) ≡ succ (fromℕ₁ n)
fromℕ₁-succ zero₁ = refl
fromℕ₁-succ (succ₁ n) =
  begin
    fromℕ₁ (succ₁ (succ₁ n))
  ≡⟨⟩
    rec₁ zero succ (succ₁ (succ₁ n))
  ≡⟨⟩
    rec₁ (succ zero) succ (succ₁ n)
  ≡⟨ rec₁-succ zero succ (succ₁ n) ⟩
    succ (rec₁ zero succ (succ₁ n))
  ≡⟨⟩
    succ (fromℕ₁ (succ₁ n))
  ∎

-- TODO Prove this using algebraic laws!
fromℕ₁-comm-+ : ∀ {m n} → fromℕ₁ (m +₁ n) ≡ fromℕ₁ m + fromℕ₁ n
fromℕ₁-comm-+ {zero₁} {zero₁} = refl
fromℕ₁-comm-+ {zero₁} {succ₁ n} =
  begin
    fromℕ₁ (zero₁ +₁ succ₁ n)
  ≡⟨⟩
    fromℕ₁ (succ₁ n)
  ≡⟨ fromℕ₁-succ n ⟩
    succ (fromℕ₁ n)
  ≡⟨ {!!} ⟩
    zero + succ (fromℕ₁ n)
  ≡⟨ cong (zero +_) (sym (fromℕ₁-succ n)) ⟩
    fromℕ₁ zero₁ + fromℕ₁ (succ₁ n)
  ∎
fromℕ₁-comm-+ {succ₁ m} {n} = {!!}

toℕ₁⁺ : List Bool → ℕ₁
toℕ₁⁺ [] = succ₁ zero₁
toℕ₁⁺ (b ∷ bs) = (if b then succ₁ else id) (toℕ₁⁺ bs +₁ toℕ₁⁺ bs)

toℕ₁ : ℕ₂ → ℕ₁
toℕ₁ zero = zero₁
toℕ₁ (pos bs) = toℕ₁⁺ bs

toℕ₁⁺-succ : ∀ bs → toℕ₁⁺ (succ⁺ bs) ≡ succ₁ (toℕ₁⁺ bs)
toℕ₁⁺-succ [] = refl
toℕ₁⁺-succ (false ∷ bs) = refl
toℕ₁⁺-succ (true ∷ bs) =
  begin
    toℕ₁⁺ (succ⁺ (true ∷ bs))
  ≡⟨⟩
    toℕ₁⁺ (false ∷ succ⁺ bs)
  ≡⟨⟩
    toℕ₁⁺ (succ⁺ bs) +₁ toℕ₁⁺ (succ⁺ bs)
  ≡⟨ cong (λ x → x +₁ toℕ₁⁺ (succ⁺ bs)) (toℕ₁⁺-succ bs) ⟩
    succ₁ (toℕ₁⁺ bs) +₁ toℕ₁⁺ (succ⁺ bs)
  ≡⟨ cong (λ x → succ₁ (toℕ₁⁺ bs) +₁ x) (toℕ₁⁺-succ bs) ⟩
    succ₁ (toℕ₁⁺ bs) +₁ succ₁ (toℕ₁⁺ bs)
  ≡⟨ +-succˡ {m = toℕ₁⁺ bs}  ⟩
    succ₁ (toℕ₁⁺ bs +₁ succ₁ (toℕ₁⁺ bs))
  ≡⟨ cong succ₁ (+-succʳ {m = toℕ₁⁺ bs}) ⟩
    succ₁ (succ₁ (toℕ₁⁺ bs +₁ toℕ₁⁺ bs))
  ≡⟨⟩
    succ₁ (toℕ₁⁺ (true ∷ bs))
  ∎

toℕ₁-succ : ∀ n → toℕ₁ (succ n) ≡ succ₁ (toℕ₁ n)
toℕ₁-succ zero = refl
toℕ₁-succ (pos bs) = toℕ₁⁺-succ bs

fromToℕ₁ : ∀ n → toℕ₁ (fromℕ₁ n) ≡ n
fromToℕ₁ zero₁ = refl
fromToℕ₁ (succ₁ n) =
  begin
    toℕ₁ (fromℕ₁ (succ₁ n))
  ≡⟨ cong toℕ₁ (fromℕ₁-succ n) ⟩
    toℕ₁ (succ (fromℕ₁ n))
  ≡⟨ toℕ₁-succ (fromℕ₁ n) ⟩
    succ₁ (toℕ₁ (fromℕ₁ n))
  ≡⟨ cong succ₁ (fromToℕ₁ n) ⟩
    succ₁ n
  ∎

toFromℕ₁⁺ : ∀ bs → fromℕ₁ (toℕ₁⁺ bs) ≡ pos bs
toFromℕ₁⁺ [] = refl
toFromℕ₁⁺ (false ∷ bs) =
  begin
    fromℕ₁ (toℕ₁⁺ (false ∷ bs))
  ≡⟨⟩
    fromℕ₁ (toℕ₁⁺ bs +₁ toℕ₁⁺ bs)
    -- TODO Fill in these holes!
  ≡⟨ {!!} ⟩
    fromℕ₁ (toℕ₁⁺ bs) + fromℕ₁ (toℕ₁⁺ bs)
  ≡⟨ cong (λ x → x + fromℕ₁ (toℕ₁⁺ bs)) (toFromℕ₁⁺ bs) ⟩
    pos bs + fromℕ₁ (toℕ₁⁺ bs)
  ≡⟨ cong (λ x → pos bs + x) (toFromℕ₁⁺ bs) ⟩
    pos bs + pos bs
  ≡⟨ {!!} ⟩
    pos (false ∷ bs)
  ∎
toFromℕ₁⁺ (true ∷ bs) = {!!}

toFromℕ₁ : ∀ n → fromℕ₁ (toℕ₁ n) ≡ n
toFromℕ₁ zero = refl
toFromℕ₁ (pos bs) = toFromℕ₁⁺ bs

instance
  Nat-ℕ₂ : Nat ℕ₂
  Nat-ℕ₂ = record
    { zero = zero
    ; succ = succ
    ; ind = {!!}
    ; _+_ = _+_
    ; +-zero = +-identityˡ
    ; +-succ = {!!}
    }

max_stars_repo_name: iblech/agda-quotients

max_issues_repo_name: iblech/agda-quotients

max_forks_repo_name: iblech/agda-quotients


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

module F1b where

open import Data.Unit
open import Data.Sum hiding (map; [_,_])
open import Data.Product hiding (map; ,_)
open import Function using (flip)
open import Relation.Binary.Core using (IsEquivalence; Reflexive; Symmetric; Transitive)
open import Relation.Binary

open import Groupoid

infixr 90 _⊗_
infixr 80 _⊕_
infixr 60 _∘_
infix  30 _⟷_

---------------------------------------------------------------------------
-- Paths

-- Path relation should be an equivalence
data Path {A : Set} : A → A → Set where
  _⇛_ : (x : A) → (y : A) → Path x y

data _≣⇛_ {A : Set} {a b : A} (x : Path a b) : Path a b → Set where
  refl⇛ : x ≣⇛ x

id⇛ : {A : Set} → (a : A) → Path a a
id⇛ a = a ⇛ a

ap : {A B : Set} → (f : A → B) → {a a' : A} → Path a a' → Path (f a) (f a')
ap f (a ⇛ a') = (f a) ⇛ (f a')

_∙⇛_ : {A : Set} {a b c : A} → Path b c → Path a b → Path a c
(b ⇛ c) ∙⇛ (a ⇛ .b) = a ⇛ c

_⇚ : {A : Set} {a b : A} → Path a b → Path b a
(x ⇛ y) ⇚ = y ⇛ x

lid⇛ : {A : Set} {x y : A} (α : Path x y) → (id⇛ y ∙⇛ α) ≣⇛ α
lid⇛ (x ⇛ y) = refl⇛

rid⇛ : {A : Set} {x y : A} (α : Path x y) → (α ∙⇛ id⇛ x) ≣⇛ α
rid⇛ (x ⇛ y) = refl⇛

assoc⇛ : {A : Set} {w x y z : A} (α : Path y z) (β : Path x y) (δ : Path w x) → ((α ∙⇛ β) ∙⇛ δ) ≣⇛ (α ∙⇛ (β ∙⇛ δ))
assoc⇛ (y ⇛ z) (x ⇛ .y) (w ⇛ .x) = refl⇛

l⇚ : {A : Set}  {x y : A} (α : Path x y) → ((α ⇚) ∙⇛ α) ≣⇛ id⇛ x
l⇚ (x ⇛ y) = refl⇛

r⇚ : {A : Set} {x y : A} (α : Path x y) → (α ∙⇛ (α ⇚)) ≣⇛ id⇛ y
r⇚ (x ⇛ y) = refl⇛

sym⇛ : {A : Set} {x y : A} {α β : Path x y} → α ≣⇛ β → β ≣⇛ α
sym⇛ refl⇛ = refl⇛

trans⇛ : {A : Set} {x y : A} {α β δ : Path x y} → α ≣⇛ β → β ≣⇛ δ → α ≣⇛ δ
trans⇛ refl⇛ refl⇛ = refl⇛

equiv≣⇛ : {A : Set} {x y : A} → IsEquivalence {_} {_} {Path x y} (_≣⇛_)
equiv≣⇛ = record { refl = refl⇛; sym = sym⇛; trans = trans⇛ }

resp≣⇛ : {A : Set} {x y z : A} {f h : Path y z} {g i : Path x y} →
  f ≣⇛ h → g ≣⇛ i → (f ∙⇛ g) ≣⇛ (h ∙⇛ i)
resp≣⇛ refl⇛ refl⇛ = refl⇛

------------------------------------------------------------------------------
-- pi types with exactly one level of reciprocals

data B0 : Set where
  ONE    : B0
  PLUS0  : B0 → B0 → B0
  TIMES0 : B0 → B0 → B0

-- interpretation of B0 as discrete groupoids

record 0-type : Set₁ where
  constructor G₀
  field
    ∣_∣₀ : Set

open 0-type public

plus : 0-type → 0-type → 0-type
plus t₁ t₂ = G₀ (∣ t₁ ∣₀ ⊎ ∣ t₂ ∣₀)

times : 0-type → 0-type → 0-type
times t₁ t₂ = G₀ (∣ t₁ ∣₀ × ∣ t₂ ∣₀)

⟦_⟧₀ : B0 → 0-type
⟦ ONE ⟧₀ = G₀ ⊤
⟦ PLUS0 b₁ b₂ ⟧₀ = plus ⟦ b₁ ⟧₀ ⟦ b₂ ⟧₀
⟦ TIMES0 b₁ b₂ ⟧₀ = times ⟦ b₁ ⟧₀ ⟦ b₂ ⟧₀

ı₀ : B0 → Set
ı₀ b = ∣ ⟦ b ⟧₀ ∣₀

point : (b : B0) → ı₀ b
point ONE = tt
point (PLUS0 b _) = inj₁ (point b)
point (TIMES0 b₀ b₁) = point b₀ , point b₁

-- isos

data _⟷_ : B0 → B0 → Set where
  -- +
  swap₊   : { b₁ b₂ : B0 } → PLUS0 b₁ b₂ ⟷ PLUS0 b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B0 } → PLUS0 b₁ (PLUS0 b₂ b₃) ⟷ PLUS0 (PLUS0 b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B0 } → PLUS0 (PLUS0 b₁ b₂) b₃ ⟷ PLUS0 b₁ (PLUS0 b₂ b₃)
  -- *
  unite⋆  : { b : B0 } → TIMES0 ONE b ⟷ b
  uniti⋆  : { b : B0 } → b ⟷ TIMES0 ONE b
  swap⋆   : { b₁ b₂ : B0 } → TIMES0 b₁ b₂ ⟷ TIMES0 b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B0 } → TIMES0 b₁ (TIMES0 b₂ b₃) ⟷ TIMES0 (TIMES0 b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B0 } → TIMES0 (TIMES0 b₁ b₂) b₃ ⟷ TIMES0 b₁ (TIMES0 b₂ b₃)
  -- * distributes over +
  dist    : { b₁ b₂ b₃ : B0 } →
            TIMES0 (PLUS0 b₁ b₂) b₃ ⟷ PLUS0 (TIMES0 b₁ b₃) (TIMES0 b₂ b₃)
  factor  : { b₁ b₂ b₃ : B0 } →
            PLUS0 (TIMES0 b₁ b₃) (TIMES0 b₂ b₃) ⟷ TIMES0 (PLUS0 b₁ b₂) b₃
  -- congruence
  id⟷   : { b : B0 } → b ⟷ b
  sym    : { b₁ b₂ : B0 } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
  _∘_    : { b₁ b₂ b₃ : B0 } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B0 } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS0 b₁ b₂ ⟷ PLUS0 b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B0 } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES0 b₁ b₂ ⟷ TIMES0 b₃ b₄)
{--
--}

-- interpret isos as paths

eval0 : {b₁ b₂ : B0} → (c : b₁ ⟷ b₂) → (x : ı₀ b₁) → ı₀ b₂
eval0 _ = {!!}

--comb0 : {b₁ b₂ : B0} → (c : b₁ ⟷ b₂) → (x : ı₀ b₁) → Path x (eval0 c x)
--comb0 _ = ?

------------------------------------------------------------------------------
-- interpretation of B1 types as 1-groupoids

data B1 : Set where
  LIFT0  : B0 → B1
  PLUS1  : B1 → B1 → B1
  TIMES1 : B1 → B1 → B1
  RECIP1 : B0 → B1

open 1Groupoid

allPaths : Set → 1Groupoid
allPaths a =  record
    { set = a
    ; _↝_ = Path
    ; _≈_ = _≣⇛_
    ; id = λ {x} → id⇛ x
    ; _∘_ = _∙⇛_
    ; _⁻¹ = _⇚
    ; lneutr = lid⇛
    ; rneutr = rid⇛
    ; assoc = assoc⇛
    ; linv = l⇚
    ; rinv = r⇚
    ; equiv = equiv≣⇛
    ;  ∘-resp-≈ = resp≣⇛}

⟦_⟧₁ : B1 → 1Groupoid
⟦ LIFT0 b0 ⟧₁ = discrete (ı₀ b0)
⟦ PLUS1 b₁ b₂ ⟧₁ = ⟦ b₁ ⟧₁ ⊎G ⟦ b₂ ⟧₁
⟦ TIMES1 b₁ b₂ ⟧₁ =  ⟦ b₁ ⟧₁ ×G ⟦ b₂ ⟧₁
⟦ RECIP1 b0 ⟧₁ = allPaths (ı₀ b0)

ı₁ : B1 → Set
ı₁ b = set ⟦ b ⟧₁

test10 = ⟦ LIFT0 ONE ⟧₁
test11 = ⟦ LIFT0 (PLUS0 ONE ONE) ⟧₁
test12 = ⟦ RECIP1 (PLUS0 ONE ONE) ⟧₁

-- interpret isos as functors

data _⟷₁_ : B1 → B1 → Set where
  -- +
  swap₊   : { b₁ b₂ : B1 } → PLUS1 b₁ b₂ ⟷₁ PLUS1 b₂ b₁
{--
  assocl₊ : { b₁ b₂ b₃ : B1 } → PLUS b₁ (PLUS b₂ b₃) ⟷₁ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B1 } → PLUS (PLUS b₁ b₂) b₃ ⟷₁ PLUS b₁ (PLUS b₂ b₃)
  -- *
--}
  unite⋆  : { b : B1 } → TIMES1 (LIFT0 ONE) b ⟷₁ b
  uniti⋆  : { b : B1 } → b ⟷₁ TIMES1 (LIFT0 ONE) b
{--
  swap⋆   : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷₁ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷₁ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷₁ TIMES b₁ (TIMES b₂ b₃)
  -- * distributes over +
  dist    : { b₁ b₂ b₃ : B } →
            TIMES (PLUS b₁ b₂) b₃ ⟷₁ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor  : { b₁ b₂ b₃ : B } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷₁ TIMES (PLUS b₁ b₂) b₃
  -- congruence
  id⟷₁   : { b : B } → b ⟷₁ b
  sym    : { b₁ b₂ : B } → (b₁ ⟷₁ b₂) → (b₂ ⟷₁ b₁)
  _∘_    : { b₁ b₂ b₃ : B } → (b₁ ⟷₁ b₂) → (b₂ ⟷₁ b₃) → (b₁ ⟷₁ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷₁ b₃) → (b₂ ⟷₁ b₄) → (PLUS b₁ b₂ ⟷₁ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷₁ b₃) → (b₂ ⟷₁ b₄) → (TIMES b₁ b₂ ⟷₁ TIMES b₃ b₄)
  η⋆ : (b : B0) → LIFT0 ONE ⟷₁ TIMES1 (LIFT0 b) (RECIP1 b)
  ε⋆ : (b : B0) → TIMES1 (LIFT0 b) (RECIP1 b) ⟷₁ LIFT0 ONE
--}

record 1-functor (A B : 1Groupoid) : Set where
  constructor 1F
  private module A = 1Groupoid A
  private module B = 1Groupoid B

  field
    F₀ : set A → set B
    F₁ : ∀ {X Y : set A} → A [ X , Y ] → B [ F₀ X , F₀ Y ]
    -- identity : ∀ {X} → B._≈_ (F₁ (A.id {X})) B.id
    -- F-resp-≈ : ∀ {X Y} {F G : A [ X , Y ]} → A._≈_ F G → B._≈_ (F₁ F) (F₁ G)

open 1-functor public

ipath : (b : B1) → ı₁ b → ı₁ b → Set
ipath b x y = Path {ı₁ b} x y

swap⊎ : {A B : Set} → A ⊎ B → B ⊎ A
swap⊎ (inj₁ a) = inj₂ a
swap⊎ (inj₂ b) = inj₁ b

intro1⋆ : {b : B1} {x y : ı₁ b} → ipath b x y → ipath (TIMES1 (LIFT0 ONE) b) (tt , x) (tt , y)
intro1⋆ (y ⇛ z) = (tt , y) ⇛ (tt , z)

objη⋆ : (b : B0) → ı₁ (LIFT0 ONE) → ı₁ (TIMES1 (LIFT0 b) (RECIP1 b))
objη⋆ b tt = point b , point b

objε⋆ : (b : B0) → ı₁ (TIMES1 (LIFT0 b) (RECIP1 b)) → ı₁ (LIFT0 ONE)
objε⋆ b (x , y) = tt

elim1∣₁ : (b : B1) → ı₁ (TIMES1 (LIFT0 ONE) b) → ı₁ b
elim1∣₁ b (tt , x) = x

intro1∣₁ : (b : B1) → ı₁ b → ı₁ (TIMES1 (LIFT0 ONE) b)
intro1∣₁ b x = (tt , x)

swapF : {b₁ b₂ : B1} →
      let G = ⟦ b₁ ⟧₁ ⊎G ⟦ b₂ ⟧₁
          G' = ⟦ b₂ ⟧₁ ⊎G ⟦ b₁ ⟧₁ in
      {X Y : set G} → G [ X , Y ] → G' [ swap⊎ X , swap⊎ Y ]
swapF {X = inj₁ _} {inj₁ _} f = f
swapF {X = inj₁ _} {inj₂ _} ()
swapF {X = inj₂ _} {inj₁ _} ()
swapF {X = inj₂ _} {inj₂ _} f = f

{-
eta : (b : B0) → List (ipath (LIFT0 ONE)) → List (ipath (TIMES1 (LIFT0 b) (RECIP1 b)))
-- note how the input list is not used at all!
eta b _ = prod (λ a a' → _↝_ (a , tt) (a' , tt)) (elems0 b) (elems0 b)

eps : (b : B0) → ipath (TIMES1 (LIFT0 b) (RECIP1 b)) → ipath (LIFT0 ONE)
eps b0 (a ⇛ b) = tt ⇛ tt
-}

Funite⋆ : {b₁ : B1} → ∀ {X Y : set (discrete (ı₀ ONE) ×G ⟦ b₁ ⟧₁)} →  DPath (proj₁ X) (proj₁ Y) ×  (_↝_ ⟦ b₁ ⟧₁) (proj₂ X) (proj₂ Y) →  _↝_ ⟦ b₁ ⟧₁ (proj₂ X) (proj₂ Y)
Funite⋆ {b₁} {tt , _} {tt , _} (reflD , y) = y

Funiti⋆ : {b₁ : B1} → ∀ {X Y : set (discrete (ı₀ ONE) ×G ⟦ b₁ ⟧₁)} →  _↝_ ⟦ b₁ ⟧₁ (proj₂ X) (proj₂ Y) → DPath (proj₁ X) (proj₁ Y) ×  (_↝_ ⟦ b₁ ⟧₁) (proj₂ X) (proj₂ Y)
Funiti⋆ y = reflD , y

mutual
  eval : {b₁ b₂ : B1} → (b₁ ⟷₁ b₂) → 1-functor ⟦ b₁ ⟧₁ ⟦ b₂ ⟧₁
  eval (swap₊ {b₁} {b₂}) = 1F swap⊎ (λ {X Y} → swapF {b₁} {b₂} {X} {Y})
  eval (unite⋆ {b}) = 1F (elim1∣₁ b) (Funite⋆ {b})
  eval (uniti⋆ {b}) = 1F (intro1∣₁ b) (Funiti⋆ {b})
--  eval (η⋆ b) = F₁ (objη⋆ b) (eta b )
--  eval (ε⋆ b) = F₁ (objε⋆ b) (map (eps b))

  evalB : {b₁ b₂ : B1} → (b₁ ⟷₁ b₂) → 1-functor ⟦ b₂ ⟧₁ ⟦ b₁ ⟧₁
  evalB (swap₊ {b₁} {b₂}) = 1F swap⊎ ((λ {X Y} → swapF {b₂} {b₁} {X} {Y}))
  evalB (unite⋆ {b}) = 1F (intro1∣₁ b) (Funiti⋆ {b})
  evalB (uniti⋆ {b}) = 1F (elim1∣₁ b) (Funite⋆ {b})
--  evalB (η⋆ b) = F₁ (objε⋆ b) (map (eps b))
--  evalB (ε⋆ b) = F₁ (objη⋆ b) (eta b)

{- eval assocl₊ = ? -- : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷₁ PLUS (PLUS b₁ b₂) b₃
eval assocr₊ = ? -- : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷₁ PLUS b₁ (PLUS b₂ b₃)
eval uniti⋆ = ? -- : { b : B } → b ⟷₁ TIMES ONE b
eval swap⋆ = ? --  : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷₁ TIMES b₂ b₁
eval assocl⋆ = ? -- : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷₁ TIMES (TIMES b₁ b₂) b₃
eval assocr⋆ = ? -- : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷₁ TIMES b₁ (TIMES b₂ b₃)
eval dist = ? -- : { b₁ b₂ b₃ : B } → TIMES (PLUS b₁ b₂) b₃ ⟷₁ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
eval factor = ? -- : { b₁ b₂ b₃ : B } → PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷₁ TIMES (PLUS b₁ b₂) b₃
eval id⟷₁ = ? --  : { b : B } → b ⟷₁ b
eval (sym c) = ? -- : { b₁ b₂ : B } → (b₁ ⟷₁ b₂) → (b₂ ⟷₁ b₁)
eval (c₁ ∘ c₂) = ? -- : { b₁ b₂ b₃ : B } → (b₁ ⟷₁ b₂) → (b₂ ⟷₁ b₃) → (b₁ ⟷₁ b₃)
eval (c₁ ⊕ c₂) = ? -- : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟷₁ b₃) → (b₂ ⟷₁ b₄) → (PLUS b₁ b₂ ⟷₁ PLUS b₃ b₄)
eval (c₁ ⊗ c₂) = ? -- : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟷₁ b₃) → (b₂ ⟷₁ b₄) → (TIMES b₁ b₂ ⟷₁ TIMES b₃ b₄)

---------------------------------------------------------------------------
--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module UnicodeEllipsis where

f : {A B : Set} → (A → B) → A → B
f g a with g a
… | x = x


text:
module LineEndings.Unix where

postulate ThisWorks : Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Level
open import Categories.Category.Core using (Category)
open import Categories.Category
open import Categories.Monad

module Categories.Adjoint.Construction.Adjunctions {o ℓ e} {C : Category o ℓ e} (M : Monad C)  where

open Category C

open import Categories.Adjoint
open import Categories.Functor
open import Categories.Morphism
open import Categories.Functor.Properties
open import Categories.NaturalTransformation.Core
open import Categories.NaturalTransformation.NaturalIsomorphism -- using (_≃_; unitorʳ; unitorˡ)
open import Categories.Morphism.Reasoning as MR
open import Categories.Tactic.Category

-- three things:
-- 1. the category of adjunctions splitting a given Monad
-- 2. the proof that EM(M) is the terminal object here
-- 3. the proof that KL(M) is the initial object here

record SplitObj : Set (suc o ⊔ suc ℓ ⊔ suc e) where
  field
    D : Category o ℓ e
    F : Functor C D
    G : Functor D C
    adj : F ⊣ G
    eqM : G ∘F F ≃ Monad.F M

record Split⇒ (X Y : SplitObj) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
  constructor Splitc⇒
  private
    module X = SplitObj X
    module Y = SplitObj Y
  field
    H : Functor X.D Y.D
    HF≃F' : H ∘F X.F ≃ Y.F
    G'H≃G : Y.G ∘F H ≃ X.G

Split : Monad C → Category _ _ _
Split M = record
  { Obj = SplitObj
  ; _⇒_ = Split⇒
  ; _≈_ = λ U V → Split⇒.H U ≃ Split⇒.H V
  ; id = split-id
  ; _∘_ = comp
  ; assoc = λ { {f = f} {g = g} {h = h} → associator (Split⇒.H f) (Split⇒.H g) (Split⇒.H h) }
  ; sym-assoc = λ { {f = f} {g = g} {h = h} → sym-associator (Split⇒.H f) (Split⇒.H g) (Split⇒.H h) }
  ; identityˡ = unitorˡ
  ; identityʳ = unitorʳ
  ; identity² = unitor²
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = _ⓘₕ_
  }
  where
  open NaturalTransformation
  split-id : {A : SplitObj} → Split⇒ A A
  split-id = record
    { H = Categories.Functor.id
    ; HF≃F' = unitorˡ
    ; G'H≃G = unitorʳ
    }
  comp : {A B X : SplitObj} → Split⇒ B X → Split⇒ A B → Split⇒ A X
  comp {A = A} {B = B} {X = X} (Splitc⇒ Hᵤ HF≃F'ᵤ G'H≃Gᵤ) (Splitc⇒ Hᵥ HF≃F'ᵥ G'H≃Gᵥ) = record
    { H = Hᵤ ∘F Hᵥ
    ; HF≃F' = HF≃F'ᵤ ⓘᵥ (Hᵤ ⓘˡ HF≃F'ᵥ) ⓘᵥ associator (SplitObj.F A) Hᵥ Hᵤ
    ; G'H≃G = G'H≃Gᵥ ⓘᵥ (G'H≃Gᵤ ⓘʳ Hᵥ) ⓘᵥ sym-associator Hᵥ Hᵤ (SplitObj.G X)
    }

open import Categories.Object.Terminal (Split M)
open import Categories.Object.Initial (Split M)
open import Categories.Category.Construction.EilenbergMoore
open import Categories.Category.Construction.Kleisli

EM-object : SplitObj
EM-object = record { D = {! EilenbergMoore M !}
                   ; F = {!   !}
                   ; G = {!   !}
                   ; adj = {!   !}
                   ; eqM = {!   !}
                   }

EM-terminal : IsTerminal EM-object
EM-terminal = {!   !}

max_stars_repo_name: tetrapharmakon/agda-categories

max_issues_repo_name: tetrapharmakon/agda-categories

max_forks_repo_name: tetrapharmakon/agda-categories


text:
module Dave.Structures.Definitions where
    open import Dave.Equality public

    op₁ : Set → Set
    op₁ A = A → A

    op₂ : Set → Set
    op₂ A = A → A → A

    associative : {A : Set} → op₂ A → Set
    associative _·_ = ∀ m n p → (m · n) · p ≡ m · (n · p)

    commutative : {A : Set} → op₂ A → Set
    commutative _·_ = ∀ m n → m · n ≡ n · m

    left-identity : {A : Set} → op₂ A → (e : A) → Set
    left-identity _·_ e = ∀ m → e · m ≡ m

    right-identity : {A : Set} → op₂ A → (e : A) → Set
    right-identity _·_ e = ∀ m → m · e ≡ m