text:
module src.Data.Zipper where

open import Agda.Builtin.Equality
open import Data.Nat
open import Data.Nat.Properties
open import Induction.WellFounded
open import Haskell.Prelude
open import Relation.Binary.PropositionalEquality

-- language extensions
{-# FOREIGN AGDA2HS
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}
#-}

-- imports
{-# FOREIGN AGDA2HS
import Control.Arrow (first)
import Control.Comonad
import Control.Lens hiding ((<.>))
import Control.Monad
import Data.Foldable
import Data.Functor.Apply
import Data.Functor.Extend
import Data.Function
import Data.List (unfoldr)
import Data.List.NonEmpty (NonEmpty ((:|)))
import Data.Semigroup.Foldable
import GHC.Generics
#-}

record Zipper (a : Set) : Set where
  constructor MkZipper
  field
    prefix : List a
    focus  : a
    suffix : List a
{-# COMPILE AGDA2HS Zipper #-}

open Zipper public

{-# FOREIGN AGDA2HS
deriving instance Show a => Show (Zipper a)
deriving instance Eq a => Eq (Zipper a)
deriving instance Generic a => Generic (Zipper a)
deriving instance Functor Zipper
deriving instance Foldable Zipper
deriving instance Traversable Zipper

makeLenses ''Zipper
#-}

{-# TERMINATING #-}
repeat : a → List a
repeat x = x ∷ repeat x

instance
  isFunctorZipper : Functor Zipper
  isFunctorZipper .fmap k
    record { prefix = p ; focus = f ; suffix = s } =
    record { prefix = map k p ; focus = k f ; suffix = map k s }

  isApplicativeZipper : Applicative Zipper
  isApplicativeZipper .pure a =
    record { prefix = repeat a ; focus = a ; suffix = repeat a }
  isApplicativeZipper ._<*>_
    record { prefix = p1 ; focus = f1 ; suffix = s1 }
    record { prefix = p2 ; focus = f2 ; suffix = s2 } =
      record { prefix = zipWith id p1 p2 ; focus = f1 f2 ; suffix = zipWith id s1 s2 }
  {-# COMPILE AGDA2HS isApplicativeZipper #-}

  isFoldableZipper : Foldable Zipper
  isFoldableZipper .foldMap k
    record { prefix = p ; focus = f ; suffix = s } =
      foldMap k p <> k f <> foldMap k s

  isTraversableZipper : Traversable Zipper
  isTraversableZipper .traverse k
    record { prefix = p ; focus = f ; suffix = s } =
    ⦇ MkZipper (traverse k p) (k f) (traverse k s) ⦈

  isSemigroupZipper : ∀ {a : Set} → ⦃ Semigroup a ⦄ → Semigroup (Zipper a)
  isSemigroupZipper ._<>_
    record { prefix = p1 ; focus = f1 ; suffix = s1 }
    record { prefix = p2 ; focus = f2 ; suffix = s2 } =
    record { prefix = zipWith (_<>_) p1 p2
           ; focus = f1 <> f2
           ; suffix = zipWith (_<>_) s1 s2 }
  {-# COMPILE AGDA2HS isSemigroupZipper #-}

{-# FOREIGN AGDA2HS
-- | Many of these instances are from Tony Morris's package, list-zipper
instance Apply Zipper where
  MkZipper l1 x1 r1 <.> MkZipper l2 x2 r2 =
    MkZipper (zipWith id l1 l2) (x1 x2) (zipWith id r1 r2)

instance Foldable1 Zipper where
  foldMap1 f (MkZipper [] x []) =
    f x
  foldMap1 f (MkZipper [] x (rh : rt)) =
    f x <> foldMap1 f (rh :| rt)
  foldMap1 f (MkZipper (lh : lt) x []) =
    foldMap1 f (lh :| lt) <> f x
  foldMap1 f (MkZipper (lh : lt) x (rh : rt)) =
    foldMap1 f (lh :| lt) <> f x <> foldMap1 f (rh :| rt)

instance Traversable1 Zipper where
  traverse1 f (MkZipper [] x []) =
    (\x' -> MkZipper [] x' []) <$> f x
  traverse1 f (MkZipper (lh : lt) x []) =
    (\l' x' -> MkZipper (toList l') x' []) <$> traverse1 f (lh :| lt) <.> f x
  traverse1 f (MkZipper [] x (rh : rt)) =
    (\x' r' -> MkZipper [] x' (toList r')) <$> f x <.> traverse1 f (rh :| rt)
  traverse1 f (MkZipper (lh : lt) x (rh : rt)) =
    (\l' x' r' -> MkZipper (toList l') x' (toList r'))
      <$> traverse1 f (lh :| lt) <.> f x <.> traverse1 f (rh :| rt)

instance Extend Zipper where
  duplicated z =
    let dup x = (x, x)
        unf f = unfoldr (fmap dup . f) z
     in MkZipper (unf left) z (unf right)

instance Comonad Zipper where
  duplicate = duplicated
  extract (MkZipper _ x _) = x
#-}

left : ∀ {a : Set} → Zipper a → Maybe (Zipper a)
left record { prefix = [] ; focus = f ; suffix = s } = Nothing
left record { prefix = x ∷ p ; focus = f ; suffix = s } =
  Just record { prefix = p ; focus = x ; suffix = f ∷ s }
{-# COMPILE AGDA2HS left #-}

right : ∀ {a : Set} → Zipper a → Maybe (Zipper a)
right record { prefix = p ; focus = f ; suffix = [] } = Nothing
right record { prefix = p ; focus = f ; suffix = x ∷ s } =
  Just record { prefix = f ∷ p ; focus = x ; suffix = s }
{-# COMPILE AGDA2HS right #-}

left-right : ∀ {a : Set} (z r : Zipper a) → right z ≡ Just r → left r ≡ Just z
left-right record { prefix = p ; focus = f ; suffix = (x ∷ s) }
         .(record { prefix = f ∷ p ; focus = x ; suffix = s }) refl = refl

right-left : ∀ {a : Set} (z r : Zipper a) → left z ≡ Just r → right r ≡ Just z
right-left record { prefix = (x ∷ p) ; focus = f ; suffix = s }
         .(record { prefix = p ; focus = x ; suffix = f ∷ s }) refl = refl

fromList : List a → Maybe (Zipper a)
fromList [] = Nothing
fromList (x ∷ xs) = Just record { prefix = [] ; focus = x ; suffix = xs }
{-# COMPILE AGDA2HS fromList #-}

unzipper : Zipper a → List a
unzipper record { prefix = p ; focus = f ; suffix = s } = reverse p ++ f ∷ s
{-# COMPILE AGDA2HS unzipper #-}

overlay : Zipper a → List a → Maybe (Zipper a)
overlay record { prefix = p ; focus = _ ; suffix = [] } [] = Nothing
overlay record { prefix = xs ; focus = _ ; suffix = (z ∷ zs) } [] =
  Just record { prefix = xs ; focus = z ; suffix = zs }
overlay record { prefix = xs ; focus = _ ; suffix = zs } (w ∷ ws) =
  Just record { prefix = xs ; focus = w ; suffix = ws ++ zs }
{-# COMPILE AGDA2HS overlay #-}

record MonadPlus (m : Set → Set) : Set₁ where
  field
    mzero : m a
    mplus : m a → m a → m a
    overlap ⦃ super ⦄ : Monad m

open MonadPlus ⦃ ... ⦄ public

{-# COMPILE AGDA2HS MonadPlus existing-class #-}

instance
  isListMonadPlus : MonadPlus List
  isListMonadPlus = record { mzero = [] ; mplus = _++_ }

zipper : ⦃ MonadPlus f ⦄ → (a → Bool) → List a → f (Zipper a)
zipper f xs = case break f xs of λ where
  (ys , z ∷ zs) →
    return record { prefix = reverse ys ; focus = z ; suffix = zs }
  _ → mzero
{-# COMPILE AGDA2HS zipper #-}

spanM : ⦃ Monad m ⦄ → ⦃ MonadPlus f ⦄ → (a → m Bool) → List a → m (f a × List a)
spanM _ [] = return (mzero , [])
spanM {m} {f} {a} {{M}} p (x ∷ xs) = do
  true <- p x
    where
      false → return (mzero , x ∷ xs)
  (ys , zs) <- spanM {m} {f} {a} {{M}} p xs
  return (mplus (return x) ys , zs)
{-# COMPILE AGDA2HS spanM #-}

infixr 1 _>=>_
_>=>_ : ⦃ Monad m ⦄ → (a → m b) → (b → m c) → a → m c
f >=> g = λ x → f x >>= g

infixr 1 _<=<_
_<=<_ : ⦃ Monad m ⦄ → (b → m c) → (a → m b) → a → m c
f <=< g = g >=> f

breakM : ⦃ Monad m ⦄ → ⦃ MonadPlus f ⦄ → (a → m Bool) → List a → m (f a × List a)
breakM p = spanM $ return ∘ not <=< p
{-# COMPILE AGDA2HS breakM #-}

zipperM
  : {a : Set}
  → {m : Set → Set}
  → {f : Set → Set}
  → ⦃ Monad m ⦄
  → ⦃ MonadPlus f ⦄
  → (a → m Bool)
  → List a
  → m (f (Zipper a))
zipperM {a} {_} {f} {{M}} k xs =
  breakM {{M}} {{isListMonadPlus}} k xs <&> λ where
    (ys , z ∷ zs) →
      return record { prefix = reverse ys ; focus = z ; suffix = zs }
    _ → mzero
{-# COMPILE AGDA2HS zipperM #-}

Traversal' : Set → Set → Set₁
Traversal' s a =
  ∀ {f : Set → Set} → ⦃ Applicative f ⦄ → (a → f a) → (s → f s)

items : Traversal' (Zipper a) a
items k z =
  ⦇ MkZipper (reverse <$> traverse k (reverse (prefix z)))
             (k (focus z))
             (traverse k (suffix z)) ⦈
{-# COMPILE AGDA2HS items #-}

scanPreState : {s : Set} → (a → s → (b × s)) → s → List a → List (b × s)
scanPreState f _ [] = []
scanPreState f s (x ∷ xs) =
  case f x s of λ where
    (b , s') → (b , s) ∷ scanPreState f s' xs
{-# COMPILE AGDA2HS scanPreState #-}

forward : {A : Set} → Zipper A → List A
forward z = focus z ∷ suffix z

measure : {A : Set}(f : A → ℕ) → Zipper A → ℕ
measure f z = sum (map (suc ∘ f) (forward z))

just-inj : {A : Set} {x y : A}
  → Just x ≡ Just y
  → x ≡ y
just-inj refl = refl

suffix-forward : {A : Set} {z z' : Zipper A}
  → right z ≡ Just z'
  → suffix z ≡ forward z'
suffix-forward {z = MkZipper prefix₁ focus₁ (x ∷ suffix₁)} H
  rewrite sym (just-inj H) = refl

measure-right-< : {A : Set} (m : A → ℕ) {z z' : Zipper A}
  → right z ≡ Just z'
  → measure m z' Data.Nat.< measure m z
measure-right-< m {z} {z'} H
  rewrite suffix-forward H = s≤s (m≤n+m _ _)

record ZipperMono (A : Set)(m : A → ℕ) : Set where
  constructor zippermono
  field
    func : Zipper A → Zipper A
    mono : ∀ z → measure m z ≡ measure m (func z)

open import Induction.WellFounded
open import Data.Nat.Induction

-- This version of survey shows that it terminates, but only if the function
-- passed is monotonic with respect to a measure on its input and output.
survey′ : {a : Set} (m : a → ℕ) → ZipperMono a m -> List a -> List a
survey′ {a} m (zippermono f mono) =
  maybe [] (λ z → go z (<-wellFounded _)) ∘ fromList
  where
    go : (z : Zipper a) → Acc Data.Nat._<_ (measure m z) → List a
    go z (acc rs) with f z | inspect f z
    ...| z' | [ eq ] with right z' | inspect right z'
    ...| Nothing | _ = unzipper z'
    ...| Just z''  | [ eq' ] =
      go z'' (rs (measure m z'')
         (≤-trans (measure-right-< m eq')
                  (≤-reflexive (trans (cong (measure m) (sym eq))
                               (sym (mono z))))))

{-# TERMINATING #-}
survey : {a : Set} → (Zipper a -> Zipper a) -> List a -> List a
survey {a} f = maybe [] go ∘ fromList
  where
    go : Zipper a → List a
    go z = let z' = f z in maybe (unzipper z') go (right z')
{-# COMPILE AGDA2HS survey #-}

{-# TERMINATING #-}
surveyM
  : {a : Set}
  → {m : Set → Set}
  → ⦃ Monad m ⦄
  → (Zipper a → m (Zipper a))
  → List a
  → m (List a)
surveyM {a} {m} f = maybe (return []) go ∘ fromList
  where
    go : Zipper a → m (List a)
    go z = do
      z' <- f z
      maybe (return (unzipper z')) go (right z')
{-# COMPILE AGDA2HS surveyM #-}

first : (a → b) → (a × c) → (b × c)
first f (a , c) = (f a , c)

mapUntils
  : (List a → List a)
  → (a → Maybe (List a × b))
  → List a
  → Maybe (List a × b)
mapUntils rev k [] = Nothing
mapUntils rev k (x ∷ xs) = case k x of λ where
  (Just (xs' , b)) → Just (rev xs' ++ xs , b)
  Nothing → first (λ xs → x ∷ xs) <$> mapUntils rev k xs
{-# COMPILE AGDA2HS mapUntils #-}

-- | Given a zipper list, attempt to locate an element first in the prefix,
--   then in the suffix, and allow for a transformation of that sub-zipper
--   list within the parent list, plus the generation of some datum.
mapLeftThenRightUntils :
  Zipper a → (Bool → a → Maybe (List a × b)) → Maybe (Zipper a × b)
mapLeftThenRightUntils {a} {b} z f =
  case mapUntils reverse (f true) (prefix z) of λ where
    (Just (p' , b)) → Just (record z { prefix = p' } , b)
    Nothing →
      case mapUntils id (f false) (suffix z) of λ where
        (Just (s' , b)) → Just (record z { suffix = s' } , b)
        Nothing → Nothing
{-# COMPILE AGDA2HS mapLeftThenRightUntils #-}

max_stars_repo_name: jwiegley/trade-journal

max_issues_repo_name: jwiegley/trade-journal

max_forks_repo_name: jwiegley/trade-journal


text:
module x09-747Decidable-hc where

-- Library

import Relation.Binary.PropositionalEquality as Eq
open        Eq                        using (_≡_; cong; refl; sym) -- added sym
open        Eq.≡-Reasoning
open import Data.Nat                  using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.Product              using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum                  using (_⊎_; inj₁; inj₂)
open import Relation.Nullary          using (¬_)
open import Relation.Nullary.Negation using () renaming (contradiction to ¬¬-intro)
open import Data.Unit                 using (⊤; tt)
open import Data.Empty                using (⊥; ⊥-elim)

-- Copied from 747Isomorphism.
record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_

-- Copied from 747Relations.

infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

-- examples proving inequalities and their negations

2≤4 : 2 ≤ 4
2≤4 = s≤s (s≤s z≤n)

¬4≤2 : ¬ (4 ≤ 2)
¬4≤2 = λ { (s≤s (s≤s ())) }

-- Bool values (computation)
data Bool : Set where
  true  : Bool
  false : Bool

-- Boolean comparison function
infix 4 _≤ᵇ_

_≤ᵇ_ : ℕ → ℕ → Bool
zero  ≤ᵇ zero  = true
zero  ≤ᵇ suc n = true
suc m ≤ᵇ zero  = false
suc m ≤ᵇ suc n = m ≤ᵇ n

-- PLFA steps through these computations using equational reasoning.

_ : (2 ≤ᵇ 4) ≡ true
_ =  refl

_ : (4 ≤ᵇ 2) ≡ false
_ = refl

-- Relating evidence and computation.

-- Boolean types (evidence)
T : Bool → Set
T true  = ⊤
T false = ⊥

T→≡ : ∀ (b : Bool) → T b → b ≡ true
T→≡ true tt = refl

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl = tt

≤ᵇ→≤ : ∀ (m n : ℕ) → T (m ≤ᵇ n) → m ≤ n
≤ᵇ→≤  zero    zero   t = z≤n
≤ᵇ→≤  zero   (suc n) t = z≤n
≤ᵇ→≤ (suc m) (suc n) t = s≤s (≤ᵇ→≤ m n t)

≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)
≤→≤ᵇ {zero} {zero}      z≤n  = tt
≤→≤ᵇ {zero} {suc n}     z≤n  = tt
≤→≤ᵇ               (s≤s m≤n) = ≤→≤ᵇ m≤n

-- computation and evidence

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

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    -------------
  →     m ≤     n
inv-s≤s (s≤s m≤n) = m≤n

-- helpers for defining _≤?_ (use these so examples will normalize)

¬s≤z : ∀ {m : ℕ} → ¬ (suc m ≤ zero)
¬s≤z = λ ()

¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
¬s≤s  {zero}  {zero} ¬m≤n = λ        sucm≤sucn  → ¬m≤n z≤n
¬s≤s  {zero} {suc n} ¬m≤n = λ        sucm≤sucn  → ¬m≤n z≤n
¬s≤s {suc m}  {zero} ¬m≤n = λ { (s≤s sucm≤sucn) → ¬m≤n sucm≤sucn }
¬s≤s {suc m} {suc n} ¬m≤n = λ { (s≤s sucm≤sucn) → ¬m≤n (s≤s (inv-s≤s sucm≤sucn)) }

-- Decidable ≤.

_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
zero  ≤? zero  = yes z≤n
zero  ≤? suc n = yes z≤n
suc m ≤? zero  = no (λ ())
suc m ≤? suc n
  with m ≤? n
... | yes  m≤n = yes (s≤s  m≤n)
... | no  ¬m≤n = no (¬s≤s ¬m≤n)

-- can also evaluate the LHS of these tests via C-c C-n
_ : 2 ≤? 4 ≡ yes (s≤s  (s≤s  z≤n))
_ = refl
_ : 4 ≤? 2 ≡ no (¬s≤s (¬s≤s ¬s≤z))
_ = refl

-- 747/PLFA exercise: DecLT (3 point)
-- Decidable strict equality.
-- You will need these helper functions as we did above.

¬z<z : ¬ (zero < zero)
¬z<z = λ ()

¬s<s : ∀ {m n : ℕ} → ¬ (m < n) → ¬ (suc m < suc n)
¬s<s ¬m<n = λ { (s<s sucm<sucn) → ¬m<n sucm<sucn }

¬s<z : ∀ {n : ℕ} → ¬ (suc n < zero)
¬s<z = λ ()

_<?_ : ∀ (m n : ℕ) → Dec (m < n)
zero  <? zero  = no (λ ())
zero  <? suc n = yes z<s
suc m <? zero  = no (λ ())
suc m <? suc n
  with m <? n
... | yes m<n = yes (s<s  m<n)
... | no ¬m<n = no (¬s<s ¬m<n)

_ : 2 <? 4 ≡ yes (s<s (s<s (z<s)))
_ = refl
_ : 4 <? 2 ≡ no (¬s<s (¬s<s ¬s<z))
_ = refl
_ : 3 <? 3 ≡ no (¬s<s (¬s<s (¬s<s ¬z<z)))
_ = refl

-- 747/PLFA exercise: DecNatEq (3 points)
-- Decidable equality for natural numbers.

_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
zero  ≡ℕ? zero  = yes refl
zero  ≡ℕ? suc n = no (λ ())
suc m ≡ℕ? zero  = no (λ ())
suc m ≡ℕ? suc n
  with m ≡ℕ? n
... | yes m≡n = yes (cong suc m≡n)
... | no ¬m≡n = no  λ { refl → ¬m≡n refl }

-- reusing ≤ᵇ and proofs of equivalence with ≤ to decide ≤
_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)
m ≤?′ n with m ≤ᵇ n | ≤ᵇ→≤ m n | ≤→≤ᵇ {m} {n}
... | true  | ⊤→m≤n |     _ = yes (⊤→m≤n tt)
... | false |     _ | m≤n→⊥ = no  (λ m≤n → m≤n→⊥ m≤n)

-- extract Bool value from Dec (aka "isYes")
⌊_⌋ : ∀ {A : Set} → Dec A → Bool
⌊ yes x ⌋ = true
⌊ no  x ⌋ = false

_≤ᵇ′_ : ℕ → ℕ → Bool
m ≤ᵇ′ n  =  ⌊ m ≤? n ⌋

-- If D is Dec A, then T ⌊ D ⌋ is inhabited exactly when A is inhabited.
toWitness : ∀ {A : Set} {D : Dec A} → T ⌊ D ⌋ → A
toWitness {_} {yes a} t = a

fromWitness : ∀ {A : Set} {D : Dec A} → A → T ⌊ D ⌋
fromWitness {_} {yes _} _ = tt
fromWitness {_} {no ¬A} a = ¬A a

-- handle "no" witnesses
isNo : ∀ {A : Set} → Dec A → Bool
isNo (yes _) = false
isNo (no  _) = true

toWitnessFalse : ∀ {A : Set} {D : Dec A} → T (isNo D) → ¬ A
toWitnessFalse {_} {no ¬A} _ = ¬A

fromWitnessFalse : ∀ {A : Set} {D : Dec A} → ¬ A → T (isNo D)
fromWitnessFalse {_} {yes A } ¬A = ¬A A
fromWitnessFalse {A} {no ¬A'} ¬A = tt

-- Agda standard library definitions for use of these.

True  : ∀ {A : Set} → (D : Dec A) → Set
True  Q = T ⌊ Q ⌋

False : ∀ {A : Set} → (D : Dec A) → Set
False Q = T (isNo Q)

-- concrete examples

≤ᵇ′→≤ : ∀ {m n : ℕ} → T (m ≤ᵇ′ n) → m ≤ n
≤ᵇ′→≤  =  toWitness

≤→≤ᵇ′ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ′ n)
≤→≤ᵇ′  =  fromWitness

-- BEST PRACTICE : use Decidables instead of Booleans.

-- Logical connectives for Decidables.

infixr 6 _∧_

_∧_ : Bool → Bool → Bool
true  ∧ true  = true
true  ∧ false = false
false ∧     _ = false

infixr 6 _×-dec_

_×-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A × B)
yes A ×-dec yes B = yes ⟨ A , B ⟩
yes _ ×-dec no ¬B = no (λ A×B → ¬B (proj₂ A×B))
no ¬A ×-dec yes B = no (λ A×B → ¬A (proj₁ A×B))
no  _ ×-dec no ¬B = no (λ A×B → ¬B (proj₂ A×B))

infixr 5 _∨_

_∨_ : Bool → Bool → Bool
true  ∨ _ = true
false ∨ r = r

infixr 5 _⊎-dec_

_⊎-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⊎ B)
yes A ⊎-dec yes _ = yes (inj₁ A)
yes A ⊎-dec no  _ = yes (inj₁ A)
no  _ ⊎-dec yes B = yes (inj₂ B)
no ¬A ⊎-dec no ¬B = no (λ { (inj₁ A) → ¬A A ; (inj₂ B) → ¬B B } )

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

¬? : ∀ {A : Set} → Dec A → Dec (¬ A)
¬? (yes A) = no (λ ¬A → ¬A A)
¬? (no ¬A) = yes ¬A

-- Boolean version of implication
_⊃_ : Bool → Bool → Bool
true  ⊃ true  = true
true  ⊃ false = false
false ⊃ _     = true

_→-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A → B)
_     →-dec yes B = yes (λ   _ →  B)
no ¬A →-dec     _ = yes (λ A   → ⊥-elim (¬A A))
yes A →-dec no ¬B = no  (λ A→B → ¬B (A→B A))

-- 747/PLFA exercise: ErasBoolDec (3 points)
-- Erasure relates boolean and decidable operations.

∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
∧-× (no  _) (no  _) = refl
∧-× (no  _) (yes _) = refl
∧-× (yes _) (no  _) = refl
∧-× (yes _) (yes _) = refl -- true ≡ true

∨-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
∨-× (no  _) (no  _) = refl
∨-× (no  _) (yes _) = refl
∨-× (yes _) (no  _) = refl
∨-× (yes _) (yes _) = refl

not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
not-¬ (yes _) = refl
not-¬ (no  _) = refl

-- 747/PLFA exercise: iff-erasure.

_iff_ : Bool → Bool → Bool
true  iff true  = true
false iff false = true
true  iff false = false
false iff true  = false

_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
yes A ⇔-dec yes B = yes (record { to = λ _ → B ; from = λ _ → A })
yes A ⇔-dec no ¬B = no  (λ A⇔B → ¬B (to   A⇔B A))
no ¬A ⇔-dec yes B = no  (λ A⇔B → ¬A (from A⇔B B))
no ¬A ⇔-dec no ¬B = yes (record { to = λ A → ⊥-elim (¬A A) ; from = λ B → ⊥-elim (¬B B) })

iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
iff-⇔ (yes _) (yes _) = refl
iff-⇔ (yes _) (no  _) = refl
iff-⇔ (no  _) (yes _) = refl
iff-⇔ (no ¬A) (no ¬B) = refl

-- proof by reflection (i.g., get Agda to construct proofs at compile time)

-- guarded version of monus
minus : (m n : ℕ) (n≤m : n ≤ m) → ℕ
minus      m   zero          _  = m
minus (suc m) (suc n) (s≤s m≤n) = minus m n m≤n

-- but must provide proofs
_ : minus 5 3 (s≤s (s≤s (s≤s z≤n))) ≡ 2
_ = refl

-- Agda will fill in an implicit record type if it can fill in all fields.
-- Since ⊤ is defined as a record type with no fields...
-- then Agda will compute a value of type True (n ≤? m).
_-_ : (m n : ℕ) {n≤m : True (n ≤? m)} → ℕ
_-_ m n {n≤m} = minus m n (toWitness n≤m)

-- then proofs no longer needed
_ : 5 - 3 ≡ 2
_ = refl

-- Use above to get Agda to compute parts of proofs that would be annoying for us to provide.

ext: agda

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

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

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


text:
module Numeral.Natural.Function where

open import Numeral.Natural
open import Numeral.Natural.Oper

-- Maximum function
-- Returns the greatest number
max : ℕ → ℕ → ℕ
max 𝟎      𝟎      = 𝟎
max (𝐒(a)) 𝟎      = 𝐒(a)
max 𝟎      (𝐒(b)) = 𝐒(b)
max (𝐒(a)) (𝐒(b)) = 𝐒(max a b)

-- Minimum function
-- Returns the smallest number
min : ℕ → ℕ → ℕ
min 𝟎      𝟎      = 𝟎
min (𝐒(_)) 𝟎      = 𝟎
min 𝟎      (𝐒(_)) = 𝟎
min (𝐒(a)) (𝐒(b)) = 𝐒(min a b)
-- min a b = (a + b) −₀ max(a)(b)

-- min and max as binary operators
infixl 100 _[max]_ _[min]_
_[max]_ = max
_[min]_ = min

-- Fibonacci numbers
fib : ℕ → ℕ
fib(𝟎)       = 𝟎
fib(𝐒(𝟎))    = 𝐒(𝟎)
fib(𝐒(𝐒(n))) = fib(n) + fib(𝐒(n))

arithmetic-sequence : ℕ → ℕ → (ℕ → ℕ)
arithmetic-sequence init diff 𝟎      = init
arithmetic-sequence init diff (𝐒(n)) = diff + arithmetic-sequence init diff n

geometric-sequence : ℕ → ℕ → (ℕ → ℕ)
geometric-sequence init diff 𝟎      = init
geometric-sequence init diff (𝐒(n)) = diff ⋅ arithmetic-sequence init diff n

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module BuildingBlock where

open import Data.Nat

--------------------------------------------------------------------------------
-- Binomial Tree

-- NodeList C n : list of C indexed from 0 to n
data NodeList (C : ℕ → Set) : ℕ → Set where
    Nil : C 0 → NodeList C 0
    Cons : ∀ {n} → C (suc n) → NodeList C n → NodeList C (suc n)

data BinomialTree (A : Set) : ℕ → Set where
    Leaf : A → BinomialTree A 0
    Node : ∀ {n} → A → NodeList (BinomialTree A) n → BinomialTree A (suc n)

-- examples
private
    ein : BinomialTree ℕ 0
    ein = Leaf 0

    zwei : BinomialTree ℕ 1
    zwei = Node 1
            (Nil (Leaf 0))

    fier' : BinomialTree ℕ 2
    fier' = Node 0
            (Cons (Node 1
                (Nil (Leaf 2)))
            (Nil (Leaf 3)))

--------------------------------------------------------------------------------
-- Pennants

data CompleteBinaryTree (A : Set) : ℕ → Set where
    Leaf : A → CompleteBinaryTree A 0
    Node : ∀ {n}  → A
                → CompleteBinaryTree A n
                → CompleteBinaryTree A n
                → CompleteBinaryTree A (suc n)

data Pennants (A : Set) : ℕ → Set where
    Leaf : A → Pennants A 0
    Node : ∀ {n}  → A
                → CompleteBinaryTree A n
                → Pennants A n

-- examples
private
    zweiP : Pennants ℕ 2
    zweiP = Node 0 (Node 1
                    (Node 2
                        (Leaf 3)
                        (Leaf 4))
                    (Node 5
                        (Leaf 6) (Leaf 7)))

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
-- Andreas, 2018-09-12, issue #3167
--
-- If --no-prop, then Set0 is the least sort and sort constraints
-- s <= Set0 should be solved by s = Set0.

{-# OPTIONS --no-prop #-}

-- (A : Set) can be inferred if Set0 is the bottom universe

data Wrap A : Set where
  wrap : A → Wrap A

-- Should succeed with --no-prop

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
module Equivalences where

open import Level
open import Data.Empty
open import Data.Sum renaming (map to _⊎→_)
open import Data.Product renaming (map to _×→_)
open import Function renaming (_∘_ to _○_)

open import SimpleHoTT

infix  4  _∼_   -- homotopy between two functions
infix  4  _≃_   -- type of equivalences
infix  2  _∎≃      -- equational reasoning for equivalences
infixr 2  _≃⟨_⟩_   -- equational reasoning for equivalences

-- Equivalences

_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
      (f g : (x : A) → P x) → Set (ℓ ⊔ ℓ')
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x

-- Lemma 2.4.2

refl∼ : {A B : Set} {f : A → B} → (f ∼ f)
refl∼ {A} {B} {f} x = refl (f x)

sym∼ : {A B : Set} {f g : A → B} → (f ∼ g) → (g ∼ f)
sym∼ H x = ! (H x)

trans∼ : {A B : Set} {f g h : A → B} → (f ∼ g) → (g ∼ h) → (f ∼ h)
trans∼ H G x = H x ∘ G x

--

record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkqinv
  field
    g : B → A
    α : (f ○ g) ∼ id
    β : (g ○ f) ∼ id

idqinv : ∀ {ℓ} → {A : Set ℓ} → qinv {ℓ} {ℓ} {A} {A} id
idqinv = record {
           g = id ;
           α = λ b → refl b ;
           β = λ a → refl a
         }

record isequiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkisequiv
  field
    g : B → A
    α : (f ○ g) ∼ id
    h : B → A
    β : (h ○ f) ∼ id

equiv₁ : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → qinv f → isequiv f
equiv₁ (mkqinv qg qα qβ) = mkisequiv qg qα qg qβ

equiv₂ : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → isequiv f → qinv f
equiv₂ {f = f} (mkisequiv ig iα ih iβ) =
  record {
    g = ig ;
    α = iα ;
    β = λ x → ig (f x)
                ≡⟨ ! (iβ (ig (f x))) ⟩
              ih (f (ig (f x)))
                ≡⟨ ap ih (iα (f x)) ⟩
              ih (f x)
                ≡⟨ iβ x ⟩
              x ∎
  }

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) isequiv

id≃ : ∀ {ℓ} {A : Set ℓ} → A ≃ A
id≃ = (id , equiv₁ idqinv)

sym≃ :  ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A ≃ B) → B ≃ A
sym≃ (A→B , equiv) with equiv₂ equiv
... | mkqinv g α β = g , equiv₁ (mkqinv A→B β α)

trans≃ : {A B C : Set} → A ≃ B → B ≃ C → A ≃ C
trans≃ (f , feq) (g , geq) with equiv₂ feq | equiv₂ geq
... | mkqinv ff fα fβ | mkqinv gg gα gβ =
  (g ○ f , equiv₁ (mkqinv
                    (ff ○ gg)
                    (λ c → g (f (ff (gg c)))
                             ≡⟨ ap g (fα (gg c)) ⟩
                           g (gg c)
                             ≡⟨ gα c ⟩
                           c ∎)
                    (λ a → ff (gg (g (f a)))
                             ≡⟨ ap ff (gβ (f a)) ⟩
                           ff (f a)
                             ≡⟨ fβ a ⟩
                           a ∎)))

-- equivalences are injective

_⋆_ : {A B : Set} → (A ≃ B) → (x : A) → B
(f , _) ⋆ x = f x

inj≃ : {A B : Set} → (eq : A ≃ B) → (x y : A) → (eq ⋆ x ≡ eq ⋆ y → x ≡ y)
inj≃ (f , mkisequiv g α h β) x y p = ! (β x) ∘ (ap h p ∘ β y)

-- equivalences for coproducts (Sec. 2.12)

codeqinv : {A B : Set} {a₀ : A} {x : A ⊎ B} → qinv (encode a₀ x)
codeqinv {A} {B} {a₀} {x} = record {
  g = decode a₀ x ;
  α = indCP
        (λ x → (c : code a₀ x) → encode a₀ x (decode a₀ x c) ≡ c)
        (λ a c → encode a₀ (inj₁ a) (decode a₀ (inj₁ a) c)
                   ≡⟨ bydef ⟩
                 encode a₀ (inj₁ a) (ap inj₁ c)
                   ≡⟨ bydef ⟩
                 transport (code a₀) (ap inj₁ c) (refl a₀)
                   ≡⟨ ! (transport-f inj₁ (code a₀) c (refl a₀)) ⟩
                 transport (λ a → code {A} {B} a₀ (inj₁ a)) c (refl a₀)
                   ≡⟨ bydef ⟩
                 transport (λ a → a₀ ≡ a) c (refl a₀)
                   ≡⟨ transportIdR c (refl a₀) ⟩
                 (refl a₀) ∘ c
                   ≡⟨ ! (unitTransL c) ⟩
                 c ∎)
        (λ b ())
        x ;
  β = λ p → basedPathInd
              (inj₁ a₀)
              (λ x p → decode a₀ x (encode a₀ x p) ≡ p)
              (decode a₀ (inj₁ a₀)
                (encode {A} {B} a₀ (inj₁ a₀) (refl (inj₁ a₀)))
                 ≡⟨ bydef ⟩
              (decode a₀ (inj₁ a₀)
                (transport (code {A} {B} a₀) (refl (inj₁ a₀)) (refl a₀)))
                 ≡⟨ bydef ⟩
              (decode a₀ (inj₁ a₀) (refl a₀))
                 ≡⟨ bydef ⟩
              (ap inj₁ (refl a₀))
                 ≡⟨ bydef ⟩
               refl (inj₁ a₀) ∎)
              x p }

thm2-12-5 : {A B : Set} → (a₀ : A) → (x : A ⊎ B) → (inj₁ a₀ ≡ x) ≃ code a₀ x
thm2-12-5 {A} {B} a₀ x = (encode a₀ x , equiv₁ codeqinv)

inj₁₁path : {A B : Set} → (a₁ a₂ : A) →
          (inj₁ {A = A} {B = B} a₁ ≡ inj₁ a₂) ≃ (a₁ ≡ a₂)
inj₁₁path a₁ a₂ = thm2-12-5 a₁ (inj₁ a₂)

inj₁₂path : {A B : Set} → (a : A) (b : B) → (inj₁ a ≡ inj₂ b) ≃ ⊥
inj₁₂path a b = thm2-12-5 a (inj₂ b)

-- Abbreviations for equivalence compositions

_≃⟨_⟩_ : (A : Set) {B C : Set} → (A ≃ B) → (B ≃ C) → (A ≃ C)
_ ≃⟨ p ⟩ q = trans≃ p q

_∎≃ : {ℓ : Level} {A : Set ℓ} → A ≃ A
_∎≃ {ℓ} {A} = id≃ {ℓ} {A}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Cubical.HITs.S1.Base public
open import Cubical.HITs.S1.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Prelude.List.Relations.Any where

open import Agda.Primitive

open import Prelude.Nat
open import Prelude.List.Base
open import Prelude.Equality

open import Prelude.List.Relations.All

data Any {a b} {A : Set a} (P : A → Set b) : List A → Set (a ⊔ b) where
  zero : ∀ {x xs} (p : P x) → Any P (x ∷ xs)
  suc  : ∀ {x xs} (i : Any P xs) → Any P (x ∷ xs)

pattern zero! = zero refl

infix 3 _∈_
_∈_ : ∀ {a} {A : Set a} → A → List A → Set a
x ∈ xs = Any (_≡_ x) xs

module _ {a b} {A : Set a} {P : A → Set b} where
  -- Delete

  deleteIx : ∀ xs → Any P xs → List A
  deleteIx (_ ∷ xs) (zero _) = xs
  deleteIx (x ∷ xs) (suc  i) = x ∷ deleteIx xs i

  deleteAllIx : ∀ {c} {Q : A → Set c} {xs} → All Q xs → (i : Any P xs) → All Q (deleteIx xs i)
  deleteAllIx (q ∷ qs) (zero _) = qs
  deleteAllIx (q ∷ qs) (suc i)  = q ∷ deleteAllIx qs i

forgetAny : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A} → Any P xs → Nat
forgetAny (zero _) = zero
forgetAny (suc  i) = suc (forgetAny i)

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
------------------------------------------------------------------------
-- Homotopy groups of pointed types
------------------------------------------------------------------------

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

import Equality.Path as P

module Pointed-type.Homotopy-group
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Equality.Groupoid equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J
open import Group equality-with-J as G using (Group; Abelian; _≃ᴳ_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation eq as T
open import Pointed-type equality-with-J as PT
  using (Pointed-type; _≃ᴮ_; Ω; Ω[_])

private
  variable
    a p q : Level
    P     : Pointed-type p
    n     : ℕ

-- Homotopy-group-[1+ n ] P is the (1+n)-th homotopy group of the
-- pointed type P.
--
-- This definition is taken from the HoTT book.

Homotopy-group-[1+_] : ℕ → Pointed-type a → Group a
Homotopy-group-[1+ n ] P = λ where
    .Group.Carrier        → Carrier
    .Group.Carrier-is-set → Carrier-is-set
    .Group._∘_            → _∘′_
    .Group.id             → id′
    .Group._⁻¹            → _⁻¹
    .Group.left-identity  → left-identity
    .Group.right-identity → right-identity
    .Group.assoc          → assoc
    .Group.left-inverse   → left-inverse
    .Group.right-inverse  → right-inverse
  where
  Carrier = ∥ proj₁ (Ω[ 1 + n ] P) ∥[1+ 1 ]
  _∘′_    = ∥∥-zip trans
  id′     = ∣ refl _ ∣
  _⁻¹     = ∥∥-map sym

  abstract

    Carrier-is-set : Is-set Carrier
    Carrier-is-set = truncation-has-correct-h-level 1

    left-identity : (x : Carrier) → (id′ ∘′ x) ≡ x
    left-identity = T.elim λ where
      .T.∣∣ʳ _      → cong ∣_∣ $ trans-reflˡ _
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1

    right-identity : (x : Carrier) → (x ∘′ id′) ≡ x
    right-identity = T.elim λ where
      .T.∣∣ʳ _      → cong ∣_∣ $ trans-reflʳ _
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1

    assoc : (x y z : Carrier) → (x ∘′ (y ∘′ z)) ≡ ((x ∘′ y) ∘′ z)
    assoc = T.elim λ where
      .T.h-levelʳ _ → Π-closure ext 2 λ _ →
                      Π-closure ext 2 λ _ →
                      mono₁ 2 $ truncation-has-correct-h-level 1
      .T.∣∣ʳ _      → T.elim λ where
        .T.h-levelʳ _ → Π-closure ext 2 λ _ →
                        mono₁ 2 $ truncation-has-correct-h-level 1
        .T.∣∣ʳ _      → T.elim λ where
          .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1
          .T.∣∣ʳ _      → cong ∣_∣ $ sym $ trans-assoc _ _ _

    left-inverse : (x : Carrier) → ((x ⁻¹) ∘′ x) ≡ id′
    left-inverse = T.elim λ where
      .T.∣∣ʳ _      → cong ∣_∣ $ trans-symˡ _
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1

    right-inverse : (x : Carrier) → (x ∘′ (x ⁻¹)) ≡ id′
    right-inverse = T.elim λ where
      .T.∣∣ʳ _      → cong ∣_∣ $ trans-symʳ _
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1

-- The fundamental group of a pointed type.
--
-- This definition is taken from the HoTT book.

Fundamental-group : Pointed-type a → Group a
Fundamental-group = Homotopy-group-[1+ 0 ]

-- The n-th homotopy group of a pointed type is abelian when n is at
-- least two.
--
-- (This result is stated in the HoTT book.)

abelian : ∀ n → Abelian (Homotopy-group-[1+ suc n ] P)
abelian n = T.elim λ where
  .T.h-levelʳ _ → Π-closure ext 2 λ _ →
                  mono₁ 2 $ truncation-has-correct-h-level 1
  .T.∣∣ʳ p      → T.elim λ where
    .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1
    .T.∣∣ʳ q      → cong ∣_∣ $ Ω[2+n]-commutative n p q

-- If there is a based equivalence between P and Q, then their
-- homotopy groups are isomorphic.

≃ᴮ→≃ᴳ :
  ∀ (P : Pointed-type p) (Q : Pointed-type q) n →
  P ≃ᴮ Q → Homotopy-group-[1+ n ] P ≃ᴳ Homotopy-group-[1+ n ] Q
≃ᴮ→≃ᴳ P Q n P≃Q = λ where
  .G.Homomorphic.related →
    ∥∥-cong (proj₁ (PT.Ω[ suc n ]-cong-≃ᴮ P≃Q))
  .G.Homomorphic.homomorphic → T.elim λ where
    .T.h-levelʳ _ → Π-closure ext 2 λ _ →
                    mono₁ 2 $ truncation-has-correct-h-level 1
    .T.∣∣ʳ _      → T.elim λ where
      .T.h-levelʳ _ → mono₁ 2 $ truncation-has-correct-h-level 1
      .T.∣∣ʳ _      → cong ∣_∣ (PT.Ω[1+ n ]-cong-≃ᴮ-trans P≃Q)

-- Homotopy-group-[1+ n ] commutes with PT._×_/G._×_.

Homotopy-group-[1+_]-× :
  ∀ n (P : Pointed-type p) (Q : Pointed-type q) →
  Homotopy-group-[1+ n ] (P PT.× Q) ≃ᴳ
  (Homotopy-group-[1+ n ] P G.× Homotopy-group-[1+ n ] Q)
Homotopy-group-[1+ n ]-× P Q = λ where
    .G.Homomorphic.related →
      ∥ proj₁ (Ω[ 1 + n ] (P PT.× Q)) ∥[1+ 1 ]                           ↝⟨ T.∥∥-cong (proj₁ PT.Ω[ 1 + n ]-×) ⟩
      ∥ proj₁ (Ω[ 1 + n ] P) × proj₁ (Ω[ 1 + n ] Q) ∥[1+ 1 ]             ↝⟨ inverse T.∥∥×∥∥≃∥×∥ ⟩□
      ∥ proj₁ (Ω[ 1 + n ] P) ∥[1+ 1 ] × ∥ proj₁ (Ω[ 1 + n ] Q) ∥[1+ 1 ]  □
    .G.Homomorphic.homomorphic → T.elim λ where
      .T.h-levelʳ _ → Π-closure ext 2 λ _ → s
      .T.∣∣ʳ p → T.elim λ where
        .T.h-levelʳ _ → s
        .T.∣∣ʳ q →
          Σ-map ∣_∣ ∣_∣ (_≃_.to (proj₁ PT.Ω[ 1 + n ]-×) (trans p q))  ≡⟨ cong (Σ-map ∣_∣ ∣_∣) PT.Ω[1+ n ]-×-trans ⟩∎

          (Σ-map ∣_∣ ∣_∣ $ Σ-zip trans trans
             (_≃_.to (proj₁ PT.Ω[ 1 + n ]-×) p)
             (_≃_.to (proj₁ PT.Ω[ 1 + n ]-×) q))                      ∎
  where
  s =
    mono₁ 2 $
    ×-closure 2
      (truncation-has-correct-h-level 1)
      (truncation-has-correct-h-level 1)

-- Homotopy-group-[1+ n ]′ P s is the (1+n)-th homotopy group of the
-- pointed type P.
--
-- The definition does not use set truncation. Instead a certain loop
-- space is required to be a set.

Homotopy-group-[1+_]′ :
  ∀ n (P : Pointed-type a) → Is-set (proj₁ (Ω[ 1 + n ] P)) → Group a
Homotopy-group-[1+ n ]′ P s = λ where
    .Group.Carrier        → Carrier
    .Group.Carrier-is-set → Carrier-is-set
    .Group._∘_            → _∘′_
    .Group.id             → id′
    .Group._⁻¹            → _⁻¹
    .Group.left-identity  → left-identity
    .Group.right-identity → right-identity
    .Group.assoc          → assoc
    .Group.left-inverse   → left-inverse
    .Group.right-inverse  → right-inverse
  where
  Carrier = proj₁ (Ω[ 1 + n ] P)
  _∘′_    = trans
  id′     = refl _
  _⁻¹     = sym

  abstract

    Carrier-is-set : Is-set Carrier
    Carrier-is-set = s

    left-identity : (x : Carrier) → (id′ ∘′ x) ≡ x
    left-identity _ = trans-reflˡ _

    right-identity : (x : Carrier) → (x ∘′ id′) ≡ x
    right-identity _ = trans-reflʳ _

    assoc : (x y z : Carrier) → (x ∘′ (y ∘′ z)) ≡ ((x ∘′ y) ∘′ z)
    assoc _ _ _ = sym $ trans-assoc _ _ _

    left-inverse : (x : Carrier) → ((x ⁻¹) ∘′ x) ≡ id′
    left-inverse _ = trans-symˡ _

    right-inverse : (x : Carrier) → (x ∘′ (x ⁻¹)) ≡ id′
    right-inverse _ = trans-symʳ _

-- The fundamental group of a pointed type.
--
-- The definition does not use set truncation. Instead a certain loop
-- space is required to be a set.

Fundamental-group′ :
  (P : Pointed-type a) → Is-set (proj₁ (Ω P)) → Group a
Fundamental-group′ = Homotopy-group-[1+ 0 ]′

-- Homotopy-group-[1+ n ]′ P s is isomorphic to
-- Homotopy-group-[1+ n ] P.

Homotopy-group-[1+]′≃ᴳHomotopy-group-[1+] :
  {s : Is-set (proj₁ (Ω[ 1 + n ] P))} →
  Homotopy-group-[1+ n ]′ P s ≃ᴳ Homotopy-group-[1+ n ] P
Homotopy-group-[1+]′≃ᴳHomotopy-group-[1+] {s = s} = λ where
  .G.Homomorphic.related →
    inverse $ Eq.↔⇒≃ $ _⇔_.to T.+⇔∥∥↔ (λ {_ _} → s)
  .G.Homomorphic.homomorphic p q →
    ∣ trans p q ∣  ≡⟨⟩
    ∣ trans p q ∣  ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

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

module Groups.Definition where

record Group {lvl1 lvl2} {A : Set lvl1} (S : Setoid {lvl1} {lvl2} A) (_·_ : A → A → A) : Set (lsuc lvl1 ⊔ lvl2) where
  open Setoid S
  field
    +WellDefined : {m n x y : A} → (m ∼ x) → (n ∼ y) → (m · n) ∼ (x · y)
    0G : A
    inverse : A → A
    +Associative : {a b c : A} → (a · (b · c)) ∼ (a · b) · c
    identRight : {a : A} → (a · 0G) ∼ a
    identLeft : {a : A} → (0G · a) ∼ a
    invLeft : {a : A} → (inverse a) · a ∼ 0G
    invRight : {a : A} → a · (inverse a) ∼ 0G
  +Associative' : {a b c : A} → ((a · b) · c) ∼ (a · (b · c))
  +Associative' = Equivalence.symmetric (Setoid.eq S) +Associative
  +WellDefinedLeft : {m x n : A} → (m ∼ n) → (m · x) ∼ (n · x)
  +WellDefinedLeft m=n = +WellDefined m=n (Equivalence.reflexive (Setoid.eq S))
  +WellDefinedRight : {m x y : A} → (x ∼ y) → (m · x) ∼ (m · y)
  +WellDefinedRight x=y = +WellDefined (Equivalence.reflexive (Setoid.eq S)) x=y


text:
-- Andreas, 2017-01-19, issue #2412, raised by bixuanzju

-- Agda should not insert hidden lambdas of possibly empty size types

open import Agda.Builtin.Size

data Nat i : Set where
  zero : Nat i
  suc  : {j : Size< i} (n : Nat j) → Nat i

recNat : (P : (i : Size) (n : Nat i) → Set)
  → (fz : ∀{i} → P i zero)
  → (fs : ∀{i}{j : Size< i} (n : Nat j) → P j n → P i (suc n))
  → ∀{i} (n : Nat i) → P i n
recNat P fz fs zero = fz
recNat P fz fs (suc n) = fs n (recNat P fz fs n)

-- This should pass.
-- Agda should not insert the λ {j : Size< i} → fs in the recursive call to recNat.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Nullary.Decidable where

open import Cubical.Core.Everything
open import Cubical.Data.Empty using (⊥)

private
  variable
    ℓ : Level

-- Negation
infix 3 ¬_

¬_ : Type ℓ → Type ℓ
¬ A = A → ⊥

-- Decidable types (inspired by standard library)
data Dec (P : Type ℓ) : Type ℓ where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

data IsYes {P : Type ℓ} : Dec P → Type ℓ where
  isYes : ∀ {x} → IsYes (yes x)

Discrete : Type ℓ → Type ℓ
Discrete A = ∀ x y → Dec (Path A x y)


text:
module Generic.Lib.Data.Pow where

open import Generic.Lib.Intro
open import Generic.Lib.Data.Nat
open import Generic.Lib.Data.Product

infixl 6 _^_

_^_ : ∀ {α} -> Set α -> ℕ -> Set α
A ^ 0     = ⊤
A ^ suc n = A × A ^ n

elimPow : ∀ {n α} {A : Set α} {b : ∀ {n} -> A ^ n -> Level}
        -> (B : ∀ {n} -> (xs : A ^ n) -> Set (b xs))
        -> (∀ {n} {xs : A ^ n} x -> B xs -> B (x , xs))
        -> B tt
        -> (xs : A ^ n)
        -> B xs
elimPow {0}     B f z  tt      = z
elimPow {suc n} B f z (x , xs) = f x (elimPow B f z xs)

foldPow : ∀ {n α β} {A : Set α}
        -> (B : ℕ -> Set β) -> (∀ {n} -> A -> B n -> B (suc n)) -> B 0 -> A ^ n -> B n
foldPow B f z xs = elimPow (λ {n} _ -> B n) (λ x y -> f x y) z xs

foldPow₁ : ∀ {n α} {A : Set α} -> (A -> A -> A) -> A ^ suc n -> A
foldPow₁ {0}     f (x , []) = x
foldPow₁ {suc n} f (x , xs) = f x (foldPow₁ f xs)

mapPow : ∀ {n α β} {A : Set α} {B : Set β} -> (A -> B) -> A ^ n -> B ^ n
mapPow f = foldPow (_ ^_) (_,_ ∘ f) tt

replicatePow : ∀ {α} {A : Set α} n -> A -> A ^ n
replicatePow  0      x = tt
replicatePow (suc n) x = x , replicatePow n x

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module Holes.Test.General where

open import Holes.Prelude
open PropEq using (_≡_; refl; cong; sym; trans)

open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

private
  +-zero : ∀ x → x + 0 ≡ x
  +-zero zero = refl
  +-zero (suc x) = cong suc (+-zero x)

  +-suc : ∀ x y → suc (x + y) ≡ x + suc y
  +-suc zero y = refl
  +-suc (suc x) y = cong suc (+-suc x y)

  +-comm : ∀ x y → x + y ≡ y + x
  +-comm zero y = sym (+-zero y)
  +-comm (suc x) y = trans (cong suc (+-comm x y)) (+-suc y x)

  data Fin : ℕ → Set where
    zero : ∀ {n} → Fin (suc n)
    suc : ∀ {n} → Fin n → Fin (suc n)

-- Expressions with free variables
test1 : ∀ x y z → ⌞ x + y ⌟ + z ≡ (y + x) + z
test1 x y z = cong! (+-comm x y)

-- NOTE: This works, but if you replace `y` by `_` in the above, there are
-- unsolved metas!
test1′ : ∀ x y z → x + y + z ≡ y + x + z
test1′ x y z = cong (λ h → h + z) (+-comm x _)

-- Multiple holes
test2 : ∀ x y z → x + ⌞ y + z ⌟ * ⌞ y + z ⌟ + y * z ≡ x + (z + y) * (z + y) + y * z
test2 x y z = cong! (+-comm y z)

-- Picking out one instance of a group of identical sub-expressions
test3 : ∀ x y z → x + ⌞ y + z ⌟ * (y + z) + y * z ≡ x + (z + y) * (y + z) + y * z
test3 x y z = cong! (+-comm y z)

-- Automatic symmetry
test4 : ∀ x y z → x + ⌞ y + z ⌟ * (y + z) + y * z ≡ x + (z + y) * (y + z) + y * z
test4 x y z = cong! (+-comm z y)

-- No hole on the LHS ⇒ hole around everything (notice automatic symmetry application)
test5 : ∀ x y → x + y ≡ y + x
test5 x y = cong! (+-comm y x)

-- Works in Π types
test6 : ∀ x y → (Fin ⌞ x + y ⌟ → ℕ) ≡ (Fin ⌞ y + x ⌟ → ℕ)
test6 x y = cong! (+-comm x y)

-- Constructors on the path
test7 : ∀ x y → ℕ.suc ⌞ x + y ⌟ ≡ suc (y + x)
test7 x y = cong! (+-comm x y)

-- -- Fails with a nice error message when holes contain different terms
-- fail1 : ∀ x y z → y ≡ x → ⌞ x ⌟ + ⌞ y ⌟ + z ≡ x + x + z
-- fail1 x y z eq = cong! eq

-- -- This is only provable in the presence of functional extensionality, so the
-- -- macro should obviously fail here. It would be nice if the error message
-- -- were improved though.
-- fail2 : ∀ (x y : ℕ) → (λ (f : ℕ → ℕ) → ⌞ f x + f y ⌟) ≡ (λ f → f y + f x)
-- fail2 x y = cong! (+-comm _ _)


text:
open import Data.Sum using ( _⊎_ )
open import FRP.LTL.RSet.Core using ( RSet )

module FRP.LTL.RSet.Sum where

infixr 2 _∨_

_∨_ : RSet → RSet → RSet
(A ∨ B) t = A t ⊎ B t

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text: module Generics.Mu.Conversion where

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
module ASN1.Untyped where

open import Data.Word8 using (Word8; _and_; _or_; _==_) renaming (primWord8fromNat to to𝕎; primWord8toNat to from𝕎)
open import Data.ByteString using (ByteString; Strict; empty; pack; fromChunks; toStrict)
open import Data.ByteString.Utf8 using (packStrict)
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_; _*_)
open import Data.List using (List; []; _∷_; concatMap)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_)
open import Data.String using (String)
open import Relation.Nullary using (Dec; yes; no)

open import ASN1.Util

-- only short (8-bit) tags are supported
Tag = Word8

-- length can be arbitrary big; TODO: restrict to Int64?
Len = ℕ

data Value : Set
data AST : Set

data Value where
  prim : (octets : ByteString Strict) → Value
  constr : (vs : List AST) → Value

data AST where
  tlv : (t : Tag) → (v : Value) → AST

private
  constructed-flag : Word8
  constructed-flag = to𝕎 0x20
  context-specific-flag : Word8
  context-specific-flag = to𝕎 0x80

constructed : Tag → Tag
constructed = _or constructed-flag

is-constructed : Tag → Bool
is-constructed t = (t and constructed-flag) == constructed-flag

context-specific : Tag → Tag
context-specific = _or context-specific-flag

is-context-specific : Tag → Bool
is-context-specific t = (t and context-specific-flag)  == context-specific-flag

universal : ℕ
universal = 0

tag : ℕ → Tag
tag = to𝕎

OID = List ℕ

-- basic asn.1 types
module _ where
  EXPLICIT : Tag → AST → AST
  EXPLICIT t v = tlv (context-specific t) (constr (v ∷ []))

  IMPLICIT : Tag → AST → AST
  IMPLICIT t (tlv _ vs) = tlv t vs

  NULL : AST
  NULL = tlv (tag 5) (prim empty)

  BOOLEAN : Bool → AST
  BOOLEAN b = tlv (tag 1) (prim (pack (bv b ∷ []))) where
    bv : Bool → Word8
    bv b with b
    ... | true = to𝕎 0xff
    ... | false = to𝕎 0

  INTEGER : ℕ → AST
  INTEGER n = tlv (to𝕎 2) (prim (pack (base256 n)))

  SEQUENCE : List AST → AST
  SEQUENCE vs = tlv (tag 16) (constr vs)

  SET : List AST → AST
  SET vs = tlv (tag 17) (constr vs)

  BIT-STRING : ℕ → ByteString Strict → AST
  BIT-STRING unused os = tlv (tag 3) (prim (toStrict (fromChunks ((pack (to𝕎 unused ∷ [])) ∷ os ∷ []))))

  OCTET-STRING : ByteString Strict → AST
  OCTET-STRING os = tlv (tag 4) (prim os)

  OBJECT-IDENTIFIER : OID → AST
  OBJECT-IDENTIFIER oid = tlv (to𝕎 6) (prim (pack (packOID oid))) where
    packOID : List ℕ → List Word8
    packOID [] = [] -- invalid oid
    packOID (n ∷ []) = to𝕎 n ∷ [] -- invalid oid
    packOID (n ∷ n′ ∷ ns) = concatMap base128 ((40 * n + n′) ∷ ns) where

  UTF8String : String → AST
  UTF8String s = tlv (to𝕎 12) (prim (packStrict s))

  GeneralizedTime : String → AST
  GeneralizedTime yyyymmddhhz = tlv (to𝕎 24) (prim (packStrict yyyymmddhhz))


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

$sig_string
-}

module ${syn_name}.Signature where

open import SOAS.Context

$type_decl
$derived_ty_ops

open import SOAS.Syntax.Signature $type public
open import SOAS.Syntax.Build $type public

-- Operator symbols
data ${sig}ₒ : Set where
  $operator_decl

-- Term signature
${sig}:Sig : Signature ${sig}ₒ
${sig}:Sig = sig λ
  { $sig_decl
  }

open Signature ${sig}:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module List.Permutation.Alternative.Correctness (A : Set) where

open import Data.List
open import List.Permutation.Alternative A renaming (_∼_ to _∼′_)
open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A

lemma-∼′-∼ : {xs ys : List A} → xs ∼′ ys → xs ∼ ys
lemma-∼′-∼ ∼refl = refl∼
lemma-∼′-∼ (∼trans xs∼′ys ys∼′zs) = trans∼ (lemma-∼′-∼ xs∼′ys) (lemma-∼′-∼ ys∼′zs)
lemma-∼′-∼ (∼head x xs∼′ys) = ∼x /head /head (lemma-∼′-∼ xs∼′ys)
lemma-∼′-∼ (∼swap xyxs∼′ys) = trans∼ (∼x /head (/tail /head) refl∼) (lemma-∼′-∼ xyxs∼′ys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import HoTT

module homotopy.PushoutSplit where

--        g     h
--     D --> B --> C    K = A ⊔^D B / (f,g)       d₁ = A <- D -> B
--    f|     |     |    L = K ⊔^B C / (right,h)   d₂ = K <- B -> C
--     v     v     v                              d  = A <- D -> C
--     A --> K --> L
--
module PushoutRSplit {i j k l} {A : Type i} {B : Type j} {C : Type k}
  {D : Type l} (f : D → A) (g : D → B) (h : B → C) where

  private
    d₁ : Span
    d₁ = span A B D f g

    d₂ : Span
    d₂ = span (Pushout d₁) C B right h

    d : Span
    d = span A C D f (h ∘ g)

  split-span-map : SpanMap d d₂
  split-span-map = span-map left (idf C) g (comm-sqr λ a → glue a) (comm-sqr λ _ → idp)

  module Split = PushoutFmap split-span-map

  split : Pushout d → Pushout d₂
  split = Split.f

  inner-span-map : SpanMap d₁ d
  inner-span-map = span-map (idf A) h (idf D) (comm-sqr λ _ → idp) (comm-sqr λ _ → idp)

  module Inner = PushoutFmap inner-span-map

  inner : Pushout d₁ → Pushout d
  inner = Inner.f

  module Merge = PushoutRec {d = d₂} {D = Pushout d}
    inner right (λ _ → idp)

  merge : Pushout d₂ → Pushout d
  merge = Merge.f

  private
    square-extend-tr : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ b : A}
      {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
      {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁} (q : a₁₀ == b)
      → Square p₀₋ p₋₀ p₋₁ p₁₋
      → Square p₀₋ (p₋₀ ∙ q) p₋₁ (! q ∙' p₁₋)
    square-extend-tr idp ids = ids

  split-inner : (k : Pushout d₁) → split (inner k) == left k
  split-inner = Pushout-elim
    (λ a → idp)
    (λ b → ! (glue b))
    (λ d → ↓-='-from-square $
      (ap-∘ split inner (glue d)
       ∙ ap (ap split) (Inner.glue-β d) ∙ Split.glue-β d)
      ∙v⊡ square-extend-tr (glue (g d)) vid-square)

  abstract
    split-merge : (l : Pushout d₂) → split (merge l) == l
    split-merge = Pushout-elim
      split-inner
      (λ c → idp)
      (λ b → ↓-∘=idf-from-square split merge $
        ap (ap split) (Merge.glue-β b) ∙v⊡ bl-square (glue b))

    merge-split : (l : Pushout d) → merge (split l) == l
    merge-split = Pushout-elim
      (λ a → idp)
      (λ c → idp)
      (λ d → ↓-∘=idf-in' merge split $
        ap merge (ap split (glue d))
          =⟨ ap (ap merge) (Split.glue-β d) ⟩
        ap merge (ap left (glue d) ∙ glue (g d))
          =⟨ ap-∙ merge (ap left (glue d)) (glue (g d)) ⟩
        ap merge (ap left (glue d)) ∙ ap merge (glue (g d))
          =⟨ ap2 _∙_ (∘-ap merge left (glue d)) (Merge.glue-β (g d)) ⟩
        ap inner (glue d) ∙ idp
          =⟨ ∙-unit-r _ ⟩
        ap inner (glue d)
          =⟨ Inner.glue-β d ⟩
        glue d ∎)

  split-equiv : Pushout d ≃ Pushout d₂
  split-equiv = equiv split merge split-merge merge-split

{-
  two-pushouts-left : lift ∘ left == left ∘ left
                      [ (λ E → (A → E)) ↓ two-pushouts ]
  two-pushouts-left = codomain-over-equiv _ _

  two-pushouts-right : lift ∘ right == right [ (λ E → (D → E)) ↓ two-pushouts ]
  two-pushouts-right = codomain-over-equiv _ _

  two-pushouts-inner : lift ∘ inner == left
                       [ (λ E → (Pushout d₁ → E)) ↓ two-pushouts ]
  two-pushouts-inner = codomain-over-equiv _ _ ▹ λ= split-inner
-}

rsplit-equiv = PushoutRSplit.split-equiv

--        h
--     D --> C    K = A ⊔^D C / (f,h)       d₁ = A <- D -> C
--    f|     |    L = B ⊔^A K / (g,left)    d₂ = B <- A -> K
--     v     v                              d  = B <- D -> C
--     A --> K
--    g|     |
--     v     v
--     B --> L

module PushoutLSplit {i j k l} {A : Type i} {B : Type j} {C : Type k}
  {D : Type l} (f : D → A) (g : A → B) (h : D → C) where

  private
    d₁ : Span
    d₁ = span A C D f h

    d₂ : Span
    d₂ = span B (Pushout d₁) A g left

    d : Span
    d = span B C D (g ∘ f) h

  split-span-map : SpanMap d d₂
  split-span-map = span-map (idf B) right f (comm-sqr λ _ → idp) (comm-sqr λ d → ! (glue d))

  module Split = PushoutFmap split-span-map

  split : Pushout d → Pushout d₂
  split = Split.f

  inner-span-map : SpanMap d₁ d
  inner-span-map = span-map g (idf C) (idf D) (comm-sqr λ _ → idp) (comm-sqr λ _ → idp)

  module Inner = PushoutFmap inner-span-map

  inner : Pushout d₁ → Pushout d
  inner = Inner.f

  module Merge = PushoutRec {d = d₂} {D = Pushout d}
    left inner (λ _ → idp)

  merge : Pushout d₂ → Pushout d
  merge = Merge.f

  private
    square-extend-tl : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ b : A}
      {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
      {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁} (q : b == a₀₀)
      → Square p₀₋ p₋₀ p₋₁ p₁₋
      → Square (q ∙' p₀₋) (q ∙' p₋₀) p₋₁ p₁₋
    square-extend-tl idp ids = ids

  split-inner : (k : Pushout d₁) → split (inner k) == right k
  split-inner = Pushout-elim
    (λ a → glue a)
    (λ c → idp)
    (λ d → ↓-='-from-square $
      (ap-∘ split inner (glue d)
       ∙ ap (ap split) (Inner.glue-β d) ∙ Split.glue-β d
       ∙ ap (λ p → glue (f d) ∙' ap right p) (!-! (glue d)))
      ∙v⊡ square-extend-tl (glue (f d)) vid-square)

  abstract
    split-merge : (l : Pushout d₂) → split (merge l) == l
    split-merge = Pushout-elim
      (λ b → idp)
      split-inner
      (λ a → ↓-∘=idf-from-square split merge $
        ap (ap split) (Merge.glue-β a) ∙v⊡ br-square (glue a))

    merge-split : (l : Pushout d) → merge (split l) == l
    merge-split = Pushout-elim
      (λ b → idp)
      (λ c → idp)
      (λ d → ↓-∘=idf-in' merge split $
        ap merge (ap split (glue d))
          =⟨ ap (ap merge) (Split.glue-β d) ⟩
        ap merge (glue (f d) ∙' ap right (! (! (glue d))))
          =⟨ ap-∙' merge (glue (f d)) (ap right (! (! (glue d)))) ⟩
        ap merge (glue (f d)) ∙' ap merge (ap right (! (! (glue d))))
          =⟨ ap2 _∙'_ (Merge.glue-β (f d)) (∘-ap merge right (! (! (glue d)))) ⟩
        idp ∙' ap inner (! (! (glue d)))
          =⟨ ∙'-unit-l _ ⟩
        ap inner (! (! (glue d)))
          =⟨ ap (ap inner) (!-! (glue d)) ⟩
        ap inner (glue d)
          =⟨ Inner.glue-β d ⟩
        glue d ∎)

  split-equiv : Pushout d ≃ Pushout d₂
  split-equiv = equiv split merge split-merge merge-split

lsplit-equiv = PushoutLSplit.split-equiv

{- TODO Update this part

--        g     h
--     Y --> Z --> W    K = X ⊔^Y Y / (f,g)        ps₁ = X <- Y -> Z
--    f|     |     |    L = Z ⊔^Z W / (left,h)     ps₂ = K <- Z -> W
--     v     v     v                               ps = X <- Y -> W
--     X --> K --> L
--
module TwoPushoutsPtd {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (f : Y ⊙→ X) (g : Y ⊙→ Z) (h : Z ⊙→ W) where

  private
    ps₁ = ⊙span X Z Y f g
    ps₂ = ⊙span (⊙Pushout ps₁) W Z (⊙right ps₁) h
    ps = ⊙span X W Y f (h ⊙∘ g)

  open TwoPushoutsEquiv (fst f) (fst g) (fst h)

  two-pushouts-ptd :
    ⊙Lift {j = lmax l (lmax k (lmax j i))} (⊙Pushout ps)
    == ⊙Pushout ps₂
  two-pushouts-ptd = ⊙ua (two-pushouts-equiv ∘e lift-equiv) idp

  two-pushouts-⊙left :
    ⊙lift ⊙∘ ⊙left ps == ⊙left ps₂ ⊙∘ ⊙left ps₁
    [ (λ V → X ⊙→ V) ↓ two-pushouts-ptd ]
  two-pushouts-⊙left = codomain-over-⊙equiv _ _ _

  two-pushouts-⊙right :
    ⊙lift ⊙∘ ⊙right ps == ⊙right ps₂
    [ (λ V → W ⊙→ V) ↓ two-pushouts-ptd ]
  two-pushouts-⊙right =
    codomain-over-⊙equiv _ _ _ ▹ pair= idp (lemma f g h)
    where
    lemma : {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
      (f : Y ⊙→ X) (g : Y ⊙→ Z) (h : Z ⊙→ W)
      → ap (TwoPushoutsEquiv.split (fst f) (fst g) (fst h)
               ∘ lower {j = lmax l (lmax k (lmax j i))})
              (snd (⊙lift ⊙∘ ⊙right (⊙span X W Y f (h ⊙∘ g))))
        ∙ idp
        ==  ap right (! (snd h)) ∙ ! (glue (pt Z))
            ∙' ap left (snd (⊙right (⊙span X Z Y f g)))
    lemma {Y = Y} (f , idp) (g , idp) (h , idp) =
      ap (2P.split ∘ lower) (ap lift (! (glue (pt Y))) ∙ idp) ∙ idp
        =⟨ ∙-unit-r _ ⟩
      ap (2P.split ∘ lower) (ap lift (! (glue (pt Y))) ∙ idp)
        =⟨ ∙-unit-r _ |in-ctx (ap (2P.split ∘ lower)) ⟩
      ap (2P.split ∘ lower) (ap lift (! (glue (pt Y))))
        =⟨ ∘-ap (2P.split ∘ lower) lift _ ⟩
      ap 2P.split (! (glue (pt Y)))
        =⟨ ap-! 2P.split (glue (pt Y)) ⟩
      ! (ap 2P.split (glue (pt Y)))
        =⟨ 2P.Split.glue-β (pt Y) |in-ctx ! ⟩
      ! (ap left (glue (pt Y)) ∙ glue (g (pt Y)))
        =⟨ !-∙ (ap left (glue (pt Y))) (glue (g (pt Y))) ⟩
      ! (glue (g (pt Y))) ∙ ! (ap left (glue (pt Y)))
        =⟨ !-ap left (glue (pt Y)) |in-ctx (λ w → ! (glue (g (pt Y))) ∙ w) ⟩
      ! (glue (g (pt Y))) ∙ ap left (! (glue (pt Y)))
        =⟨ ∙=∙' (! (glue (g (pt Y)))) (ap left (! (glue (pt Y)))) ⟩
      ! (glue (g (pt Y))) ∙' ap left (! (glue (pt Y))) ∎
      where
      module 2P = TwoPushoutsEquiv f g h

  two-pushouts-⊙inner : ⊙lift ⊙∘ (inner , idp) == ⊙left ps₂
    [ (λ V → ⊙Pushout ps₁ ⊙→ V) ↓ two-pushouts-ptd ]
  two-pushouts-⊙inner =
    codomain-over-⊙equiv _ _ _ ▹ ⊙λ= split-inner idp
-}

{-
open TwoPushoutsEquiv using () renaming (split-equiv to vsplit-pushouts-equiv)
  -- two-pushouts; two-pushouts-left; two-pushouts-right; two-pushouts-inner

open TwoPushoutsPtd
  using (two-pushouts-ptd; two-pushouts-⊙left; two-pushouts-⊙right;
         two-pushouts-⊙inner)
-}

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Algebra.Group.Group where

open import Algebra.Category
open import Algebra.Group.Monoid
open import Algebra.Group.Semigroup
open import Core

-- A group is a monoid where every element has an inverse.

record IsGroup {a r} (S : Semigroup {a} {r}) : Set (a ⊔ r) where
  open Semigroup S

  field isMonoid : IsMonoid S
  open IsMonoid isMonoid

  field iso : ∀ x → Iso x

  inv : A → A
  inv x = Iso.inv (iso x)

  field inv-cong : ∀ {x y} → x ≈ y → inv x ≈ inv y

  groupoid : Groupoid
  groupoid =
    record {
      category = category;
      iso = iso;
      inv-cong = inv-cong
    }

  open Groupoid groupoid public
    using (inv-invol)

record Group {a r} : Set (lsuc (a ⊔ r)) where
  field semigroup : Semigroup {a} {r}
  open Semigroup semigroup public

  field isGroup : IsGroup semigroup
  open IsGroup isGroup public

  monoid : Monoid
  monoid =
    record {
      semigroup = semigroup;
      isMonoid = isMonoid
    }

-- A group morphism is a function that maps the elements of one group to
-- another while preserving the compositional structure, the identity
-- and all inverses.

record GroupMorphism
           {ga gr ha hr}
           (G : Group {ga} {gr})
           (H : Group {ha} {hr})
           : Set (ga ⊔ gr ⊔ ha ⊔ hr)
       where

  private
    module G = Group G
    module H = Group H

  field monoidMorphism : MonoidMorphism G.monoid H.monoid
  open MonoidMorphism monoidMorphism public

  field inv-preserving : ∀ x → map (G.inv x) H.≈ H.inv (map x)

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.GradedRing.Base where

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

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring

open import Cubical.Algebra.GradedRing.DirectSumHIT

private variable
  ℓ ℓ' : Level

open AbGroupStr
open GradedRing-⊕HIT-index
open GradedRing-⊕HIT-⋆

-----------------------------------------------------------------------------
-- Definition

record IsGradedRing (R    : Ring (ℓ-max ℓ ℓ'))
                    (IdM  : Monoid ℓ)
                    (G    : (k : (fst IdM)) → Type ℓ')
                    (Gstr : (k : fst IdM) → AbGroupStr (G k))
                    (1⋆   : G (MonoidStr.ε (snd IdM)))
                    (_⋆_  : {k l : fst IdM} → G k → G l → G (MonoidStr._·_ (snd IdM) k l))
                    : Type (ℓ-max ℓ ℓ')
                    where

  constructor isgradedring

  private
    Idx = fst IdM
    open MonoidStr (snd IdM)

  field
    0-⋆     : {k l : Idx} → (b : G l) → (0g (Gstr k)) ⋆ b ≡ 0g (Gstr (k · l))
    ⋆-0     : {k l : Idx} → (a : G k) → a ⋆ (0g (Gstr l)) ≡ 0g (Gstr (k · l))
    ⋆Assoc  : {k l m : Idx} → (a : G k) → (b : G l) → (c : G m) →
              ((k · (l · m)) , (a ⋆ (b ⋆ c))) ≡ (((k · l) · m) , ((a ⋆ b) ⋆ c))
    ⋆IdR    : {k : Idx} → (a : G k) → ( k · ε , a ⋆ 1⋆ ) ≡ (k , a)
    ⋆IdL    : {l : Idx} → (b : G l) → ( ε · l , 1⋆ ⋆ b ) ≡ (l , b)
    ⋆DistR+ : {k l : Idx} → (a : G k) → (b c : G l) →
              a ⋆ ((Gstr l) ._+_ b c) ≡ Gstr (k · l) ._+_ (a ⋆ b) (a ⋆ c)
    ⋆DistL+ : {k l : Idx} → (a b : G k) → (c : G l) →
              ((Gstr k) ._+_ a b) ⋆ c ≡ Gstr (k · l) ._+_ (a ⋆ c) (b ⋆ c)
    equivRing : RingEquiv R (⊕HITgradedRing-Ring IdM G Gstr 1⋆ _⋆_
                             0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+)

record GradedRingStr (R : Ring (ℓ-max ℓ ℓ')) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where

  constructor gradedringstr

  field
    IdM  : Monoid ℓ
    G    : (k : (fst IdM)) → Type ℓ'
    Gstr : (k : fst IdM) → AbGroupStr (G k)
    1⋆   : G (MonoidStr.ε (snd IdM))
    _⋆_  : {k l : fst IdM} → G k → G l → G (MonoidStr._·_ (snd IdM) k l)
    isGradedRing : IsGradedRing R IdM G Gstr 1⋆ _⋆_

  open IsGradedRing isGradedRing public

GradedRing : ∀ ℓ ℓ' → Type (ℓ-suc (ℓ-max ℓ ℓ'))
GradedRing ℓ ℓ' = Σ[ R ∈ Ring (ℓ-max ℓ ℓ') ] GradedRingStr R

-----------------------------------------------------------------------------
-- make

open MonoidStr

makeIsGradedRing : {R : Ring (ℓ-max ℓ ℓ')} {IdM : Monoid ℓ}
                   {G       : (k : (fst IdM)) → Type ℓ'}
                   {Gstr    : (k : fst IdM) → AbGroupStr (G k)}
                   {1⋆      : G (ε (snd IdM))}
                   {_⋆_     : {k l : fst IdM} → G k → G l → G (_·_ (snd IdM) k l)}
                   (0-⋆     : {k l : fst IdM} (b : G l) → (0g (Gstr k) ⋆ b) ≡ 0g (Gstr ((snd IdM MonoidStr.· k) l)))
                   (⋆-0     : {k l : fst IdM} (a : G k) → (a ⋆ 0g (Gstr l)) ≡ 0g (Gstr ((snd IdM MonoidStr.· k) l)))
                   (⋆Assoc  : {k l m : fst IdM} (a : G k) (b : G l) (c : G m) →
                                 (((snd IdM ._·_ k) ((snd IdM ._·_ l) m) , (a ⋆ (b ⋆ c))))
                               ≡ ((snd IdM ._·_ ((snd IdM ._·_ k) l) m) , ((a ⋆ b) ⋆ c)))
                   (⋆IdR    : {k : fst IdM} → (a : G k) → ( snd IdM ._·_ k (snd IdM .ε) , a ⋆ 1⋆ ) ≡ (k , a))
                   (⋆IdL    : {l : fst IdM} → (b : G l) → ( snd IdM ._·_ (snd IdM .ε) l , 1⋆ ⋆ b ) ≡ (l , b))
                   (⋆DistR+ : {k l : fst IdM} → (a : G k) → (b c : G l) →
                              a ⋆ ((Gstr l) ._+_ b c) ≡ Gstr (snd IdM ._·_ k l) ._+_ (a ⋆ b) (a ⋆ c))
                   (⋆DistL+ : {k l : fst IdM} → (a b : G k) → (c : G l) →
                              ((Gstr k) ._+_ a b) ⋆ c ≡ Gstr (snd IdM ._·_ k l) ._+_ (a ⋆ c) (b ⋆ c))
                   (equivRing : RingEquiv R (⊕HITgradedRing-Ring IdM G Gstr 1⋆ _⋆_
                                             0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+))
           → IsGradedRing R IdM G Gstr 1⋆ _⋆_
makeIsGradedRing 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing =
  isgradedring 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing

makeGradedRing : (R : Ring (ℓ-max ℓ ℓ')) (IdM : Monoid ℓ)
                 (G      : (k : (fst IdM)) → Type ℓ')
                 (Gstr   : (k : fst IdM) → AbGroupStr (G k))
                 (1⋆     : G (ε (snd IdM)))
                 (_⋆_    : {k l : fst IdM} → G k → G l → G (_·_ (snd IdM) k l))
                 (0-⋆    : {k l : fst IdM} (b : G l) → (0g (Gstr k) ⋆ b) ≡ 0g (Gstr ((snd IdM MonoidStr.· k) l)))
                 (⋆-0    : {k l : fst IdM} (a : G k) → (a ⋆ 0g (Gstr l)) ≡ 0g (Gstr ((snd IdM MonoidStr.· k) l)))
                 (⋆Assoc : {k l m : fst IdM} (a : G k) (b : G l) (c : G m) →
                              (((snd IdM ._·_ k) ((snd IdM ._·_ l) m) , (a ⋆ (b ⋆ c))))
                            ≡ ((snd IdM ._·_ ((snd IdM ._·_ k) l) m) , ((a ⋆ b) ⋆ c)))
                 (⋆IdR    : {k : fst IdM} → (a : G k) → (snd IdM ._·_ k (snd IdM .ε) , a ⋆ 1⋆ ) ≡ (k , a))
                 (⋆IdL    : {l : fst IdM} → (b : G l) → (snd IdM ._·_ (snd IdM .ε) l , 1⋆ ⋆ b ) ≡ (l , b))
                 (⋆DistR+ : {k l : fst IdM} → (a : G k) → (b c : G l) →
                            a ⋆ ((Gstr l) ._+_ b c) ≡ Gstr (snd IdM ._·_ k l) ._+_ (a ⋆ b) (a ⋆ c))
                 (⋆DistL+ : {k l : fst IdM} → (a b : G k) → (c : G l) →
                            ((Gstr k) ._+_ a b) ⋆ c ≡ Gstr (snd IdM ._·_ k l) ._+_ (a ⋆ c) (b ⋆ c))
                 (equivRing : RingEquiv R (⊕HITgradedRing-Ring IdM G Gstr 1⋆ _⋆_
                                             0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+))
                  → GradedRing ℓ ℓ'
fst (makeGradedRing R IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing) = R
GradedRingStr.IdM (snd (makeGradedRing R IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing)) = IdM
GradedRingStr.G (snd (makeGradedRing R IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing)) = G
GradedRingStr.Gstr (snd (makeGradedRing R IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing)) = Gstr
GradedRingStr.1⋆ (snd (makeGradedRing R IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing)) = 1⋆
GradedRingStr._⋆_ (snd (makeGradedRing R IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing)) = _⋆_
GradedRingStr.isGradedRing (snd (makeGradedRing R IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing)) =
  makeIsGradedRing 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ equivRing

makeGradedRingSelf : (IdM : Monoid ℓ)
                     (G      : (k : (fst IdM)) → Type ℓ')
                     (Gstr   : (k : fst IdM) → AbGroupStr (G k))
                     (1⋆     : G (ε (snd IdM)))
                     (_⋆_    : {k l : fst IdM} → G k → G l → G (_·_ (snd IdM) k l))
                     (0-⋆    : {k l : fst IdM} (b : G l) → (0g (Gstr k) ⋆ b) ≡ 0g (Gstr ((snd IdM MonoidStr.· k) l)))
                     (⋆-0    : {k l : fst IdM} (a : G k) → (a ⋆ 0g (Gstr l)) ≡ 0g (Gstr ((snd IdM MonoidStr.· k) l)))
                     (⋆Assoc : {k l m : fst IdM} (a : G k) (b : G l) (c : G m) →
                                _≡_ {A = Σ[ k ∈ fst IdM ] G k} (((snd IdM ._·_ k) ((snd IdM ._·_ l) m) , (a ⋆ (b ⋆ c))))
                                                               ((snd IdM ._·_ ((snd IdM ._·_ k) l) m) , ((a ⋆ b) ⋆ c)))
                     (⋆IdR    : {k : fst IdM} → (a : G k) →
                                _≡_ {A = Σ[ k ∈ fst IdM ] G k} ( snd IdM ._·_ k (snd IdM .ε) , a ⋆ 1⋆ ) (k , a))
                     (⋆IdL    : {l : fst IdM} → (b : G l) →
                                _≡_ {A = Σ[ k ∈ fst IdM ] G k} ( snd IdM ._·_ (snd IdM .ε) l , 1⋆ ⋆ b ) (l , b))
                     (⋆DistR+ : {k l : fst IdM} → (a : G k) → (b c : G l) →
                                a ⋆ ((Gstr l) ._+_ b c) ≡ Gstr (snd IdM ._·_ k l) ._+_ (a ⋆ b) (a ⋆ c))
                     (⋆DistL+ : {k l : fst IdM} → (a b : G k) → (c : G l) →
                                ((Gstr k) ._+_ a b) ⋆ c ≡ Gstr (snd IdM ._·_ k l) ._+_ (a ⋆ c) (b ⋆ c))
                     → GradedRing ℓ ℓ'
makeGradedRingSelf IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+ =
  makeGradedRing (⊕HITgradedRing-Ring IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+)
                 IdM G Gstr 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+
                 ((idEquiv _) , (makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Unbundled.Properties where

-- The Obj-unbundled Category is equivalent (as a type) to the
-- usual kind. Quite straightforward and because of η, the proofs are just refl.

open import Data.Product using (Σ; _,_)
open import Level
open import Function using (_↔_; mk↔′)
open import Relation.Binary.PropositionalEquality using (refl)

open import Categories.Category.Core using (Category)
open import Categories.Category.Unbundled renaming (Category to Unb-Cat)

private
  variable
    o ℓ e : Level

unpack : Category o ℓ e → Σ (Set o) (λ Obj → Unb-Cat Obj ℓ e)
unpack C = C.Obj , record { C }
  where module C = Category C

unpack′ : (C : Category o ℓ e) → Unb-Cat (Category.Obj C) ℓ e
unpack′ C = record { C }
  where module C = Category C

pack : Σ (Set o) (λ Obj → Unb-Cat Obj ℓ e) → Category o ℓ e
pack (o , uc)  = record { Obj = o; UC }
  where module UC = Unb-Cat uc

pack′ :  {Obj : Set o} → Unb-Cat Obj ℓ e → Category o ℓ e
pack′ {Obj = o} uc  = record { Obj = o; UC }
  where module UC = Unb-Cat uc

equiv : (Category o ℓ e) ↔ (Σ (Set o) (λ Obj → Unb-Cat Obj ℓ e))
equiv = mk↔′ unpack pack (λ _ → refl) λ _ → refl

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.PartialFunctions where

-- Category of (Agda) Sets, and partial functions (modelled using Maybe).
-- Note that unlike for basic categories, this is named after the morphisms instead of the objects.

open import Data.Maybe using (Maybe; nothing; just; _>>=_; maybe)
open import Level
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as ≡
  using (_≗_; refl)

open import Categories.Category

private
  variable
    o : Level
    A B C D : Set o
    f g h : A → Maybe B

  _∘′_ : (B → Maybe C) → (A → Maybe B) → A → Maybe C
  f ∘′ g = λ a → g a >>= f

  ∘′-assoc : {h : C → Maybe D} {g : B → Maybe C} {f : A → Maybe B} → (h ∘′ g) ∘′ f ≗ h ∘′ (g ∘′ f)
  ∘′-assoc {h = h} {g} {f} a with f a
  ... | nothing = refl
  ... | just b = refl

  idˡ : {A B : Set o} {f : A → Maybe B} → just ∘′ f ≗ f
  idˡ {f = f} a = maybe {B = λ b → (b >>= just) ≡.≡ b} (λ x → refl) refl (f a)

  resp : {A B C : Set o} {f h : B → Maybe C} {g i : A → Maybe B} →
    f ≗ h → g ≗ i → (f ∘′ g) ≗ (h ∘′ i)
  resp {f = f} {h} {g} {i} f≡h g≡i a with g a | i a | g≡i a
  ... | just x | just .x | refl = f≡h x
  ... | just x | nothing | ()
  ... | nothing | just x | ()
  ... | nothing | nothing | _ = refl

PartialFunctions : ∀ o → Category (suc o) o o
PartialFunctions o = record
  { Obj = Set o
  ; _⇒_ = λ a b → a → Maybe b
  ; _≈_ = _≗_
  ; id = just
  ; _∘_ = _∘′_
  ; assoc = λ {_} {_} {_} {_} {f} {g} {h} → ∘′-assoc {h = h} {g} {f}
  ; sym-assoc = λ {_} {_} {_} {_} {f} {g} {h} a → ≡.sym (∘′-assoc {h = h} {g} {f} a)
  ; identityˡ = idˡ
  ; identityʳ = λ _ → refl
  ; identity² = idˡ
  ; equiv = λ {A} {B} → Setoid.isEquivalence (≡._→-setoid_ A (Maybe B))
  ; ∘-resp-≈ = resp
  }


text:
-- Andreas, 2013-02-27
module Issue385 where

import Common.Level
open import Common.Equality

loop : ∀ {A}{x : A} → x ≡ x
loop = loop

bad : Set
bad rewrite loop = ?
-- this used to loop, but should no longer, instead:

-- Cannot rewrite by equation of type {A : Set _3} {x : A} → x ≡ x
-- when checking that the clause bad rewrite loop = ? has type Set

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Data.List.Functions.Positional where

import      Lvl
open import Data.List
open import Data.Option
open import Type

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

-- A singleton list. A list with only a single element.
-- Example:
--   singleton(a) = [a]
singleton : T → List(T)
singleton elem = elem ⊰ ∅

-- The list without its first element (if there is one).
-- Example:
--   tail []      = []
--   tail [a]     = []
--   tail [a,b]   = [b]
--   tail [a,b,c] = [b,c]
tail : List(T) → List(T)
tail ∅ = ∅
tail (_ ⊰ l) = l

-- The first element of the list (head)
first : List(T) → Option(T)
first ∅       = Option.None
first (x ⊰ _) = Option.Some(x)

-- The last element of the list
last : List(T) → Option(T)
last ∅           = Option.None
last (x ⊰ ∅)     = Option.Some(x)
last (_ ⊰ y ⊰ l) = last (y ⊰ l)
-- TODO: Function equivalent to (foldₗ (const Option.Some) Option.None)? Prove if correct

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K #-}
module hott.level.sets where

open import level
open import decidable
open import sum
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.core
open import function.extensionality.proof
open import sets.empty
open import sets.unit
open import hott.level.core

-- ⊤ is contractible
⊤-contr : contr ⊤
⊤-contr = tt , λ { tt → refl }

-- ⊥ is propositional
⊥-prop : h 1 ⊥
⊥-prop x _ = ⊥-elim x

⊥-initial : ∀ {i} {A : Set i} → contr (⊥ → A)
⊥-initial = (λ ()) , (λ f → funext λ ())

-- Hedberg's theorem
hedberg : ∀ {i} {A : Set i}
        → ((x y : A) → Dec (x ≡ y))
        → h 2 A
hedberg {A = A} dec x y = prop⇒h1 ≡-prop
  where
    open ≡-Reasoning

    canonical : {x y : A} → x ≡ y → x ≡ y
    canonical {x} {y} p with dec x y
    ... | yes q = q
    ... | no _ = p

    canonical-const : {x y : A}
                    → (p q : x ≡ y)
                    → canonical p ≡ canonical q
    canonical-const {x} {y} p q with dec x y
    ... | yes _ = refl
    ... | no f = ⊥-elim (f p)

    canonical-inv : {x y : A}(p : x ≡ y)
                  → canonical p · sym (canonical refl) ≡ p
    canonical-inv refl = left-inverse (canonical refl)

    ≡-prop : {x y : A}(p q : x ≡ y) → p ≡ q
    ≡-prop p q = begin
        p
      ≡⟨ sym (canonical-inv p) ⟩
        canonical p · sym (canonical refl)
      ≡⟨ ap (λ z → z · sym (canonical refl))
              (canonical-const p q) ⟩
        canonical q · sym (canonical refl)
      ≡⟨ canonical-inv q ⟩
        q
      ∎

-- Bool is a set
private
  module BoolSet where
    open import sets.bool
    bool-set : h 2 Bool
    bool-set = hedberg _≟_
open BoolSet public

-- Nat is a set
private
  module NatSet where
    open import sets.nat.core
    nat-set : h 2 ℕ
    nat-set = hedberg _≟_
open NatSet public

-- Fin is a set
private
  module FinSet where
    open import sets.fin.core
    fin-set : ∀ n → h 2 (Fin n)
    fin-set n = hedberg _≟_
open FinSet public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
import      Lvl
open import Type

module Data.List.Relation.Sublist.Proofs {ℓ} {T : Type{ℓ}} where

open import Data.Boolean
import      Data.Either as Either
open import Data.List as List
open import Data.List.Functions as List hiding (skip)
open import Data.List.Proofs
open import Data.List.Relation.Sublist
open import Data.Tuple as Tuple using (_,_)
open import Functional
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Inductions
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Relator.Ordering
open import Structure.Relator.Ordering.Proofs
open import Structure.Relator.Properties

private variable ℓ₂ : Lvl.Level
private variable T₂ : Type{ℓ₂}
private variable a x y : T
private variable l l₁ l₂ l₃ : List(T)
private variable n : ℕ

[⊑]-reflexivity : (l ⊑ l)
[⊑]-reflexivity {∅}     = empty
[⊑]-reflexivity {a ⊰ l} = use([⊑]-reflexivity{l})

[⊑]-prepend : (l ⊑ x ⊰ l)
[⊑]-prepend {∅}     = skip empty
[⊑]-prepend {x ⊰ l} = skip [⊑]-reflexivity

[⊑]-without-[⊰] : ((x ⊰ l₁) ⊑ (y ⊰ l₂)) → (l₁ ⊑ l₂)
[⊑]-without-[⊰]                (use p)        = p
[⊑]-without-[⊰]                (skip(use p))  = skip p
[⊑]-without-[⊰] {x = x}{y = y} (skip(skip p)) = skip([⊑]-without-[⊰] {x = x}{y = y} (skip p))

[⊑]-transitivity : (l₁ ⊑ l₂) → (l₂ ⊑ l₃) → (l₁ ⊑ l₃)
[⊑]-transitivity empty       empty       = empty
[⊑]-transitivity empty       (skip l₂l₃) = skip l₂l₃
[⊑]-transitivity (use l₁l₂)  (use l₂l₃)  = use([⊑]-transitivity l₁l₂ l₂l₃)
[⊑]-transitivity (use l₁l₂)  (skip l₂l₃) = skip([⊑]-transitivity (use l₁l₂) l₂l₃)
[⊑]-transitivity (skip l₁l₂) (use l₂l₃)  = skip([⊑]-transitivity l₁l₂ l₂l₃)
[⊑]-transitivity (skip l₁l₂) (skip l₂l₃) = skip([⊑]-transitivity (skip l₁l₂) l₂l₃)

[⊑]-not-prepend : ¬((x ⊰ l) ⊑ l)
[⊑]-not-prepend {x} {x ⊰ l₂} (use  p) = [⊑]-not-prepend {x}{l₂} p
[⊑]-not-prepend {x} {y ⊰ _}  (skip p) = [⊑]-not-prepend([⊑]-without-[⊰] {y = y} (skip p))

[⊑]-antisymmetry : (l₂ ⊑ l₁) → (l₁ ⊑ l₂) → (l₁ ≡ l₂)
[⊑]-antisymmetry {∅}      {∅}       l        r        = [≡]-intro
[⊑]-antisymmetry {y ⊰ l₂} {.y ⊰ l₁} (use l)  r        = [≡]-with(y ⊰_) ([⊑]-antisymmetry l ([⊑]-without-[⊰] r))
[⊑]-antisymmetry {y ⊰ l₂} {.y ⊰ l₁} (skip l) (use r)  = [≡]-with(y ⊰_) ([⊑]-antisymmetry ([⊑]-without-[⊰] {y = y} (skip l)) r)
[⊑]-antisymmetry {y ⊰ l₂} {x ⊰ l₁}  (skip l) (skip r) = [⊥]-elim ([⊑]-not-prepend ([⊑]-transitivity (skip r) l))

[⊑]-minimum : (∅ ⊑ l)
[⊑]-minimum {∅}     = empty
[⊑]-minimum {a ⊰ l} = skip([⊑]-minimum{l})

[⊑]ᵣ-of-[++]ₗ : (l₁ ⊑ (l₂ ++ l₁))
[⊑]ᵣ-of-[++]ₗ {l₁}{∅}      = [⊑]-reflexivity
[⊑]ᵣ-of-[++]ₗ {l₁}{a ⊰ l₂} = skip{x = a}([⊑]ᵣ-of-[++]ₗ {l₁}{l₂})

[⊑]ᵣ-of-[++]ᵣ : (l₁ ⊑ (l₁ ++ l₂))
[⊑]ᵣ-of-[++]ᵣ {∅}     {l₂} = [⊑]-minimum
[⊑]ᵣ-of-[++]ᵣ {a ⊰ l₁}{l₂} = use([⊑]ᵣ-of-[++]ᵣ{l₁}{l₂})

[⊑]-tail : (tail l ⊑ l)
[⊑]-tail {∅}     = empty
[⊑]-tail {a ⊰ l} = skip [⊑]-reflexivity

[⊑]-map : ∀{f : T → T₂} → (l₁ ⊑ l₂) → (map f(l₁) ⊑ map f(l₂))
[⊑]-map empty    = empty
[⊑]-map (use  p) = use  ([⊑]-map p)
[⊑]-map (skip p) = skip ([⊑]-map p)

[⊑]-filter : ∀{f} → (filter f(l) ⊑ l)
[⊑]-filter {∅}         = empty
[⊑]-filter {x ⊰ l} {f} with f(x)
... | 𝑇 = use  ([⊑]-filter {l})
... | 𝐹 = skip ([⊑]-filter {l})

[⊑]-separate₂ : let (l₁ , l₂) = separate₂(l) in (l₁ ⊑ l) ∧ (l₂ ⊑ l)
Tuple.left  ([⊑]-separate₂ {∅})         = empty
Tuple.left  ([⊑]-separate₂ {x ⊰ ∅})     = [⊑]-reflexivity
Tuple.left  ([⊑]-separate₂ {x ⊰ y ⊰ l}) = use (skip (Tuple.left [⊑]-separate₂))
Tuple.right ([⊑]-separate₂ {∅})         = empty
Tuple.right ([⊑]-separate₂ {x ⊰ ∅})     = skip [⊑]-reflexivity
Tuple.right ([⊑]-separate₂ {x ⊰ y ⊰ l}) = skip (use (Tuple.right [⊑]-separate₂))

[⊑]-postpend : (l ⊑ postpend a l)
[⊑]-postpend {∅}     = skip empty
[⊑]-postpend {x ⊰ l} = use [⊑]-postpend

[⊑]-withoutIndex : (withoutIndex n l ⊑ l)
[⊑]-withoutIndex {𝟎}   {∅}     = empty
[⊑]-withoutIndex {𝐒 n} {∅}     = empty
[⊑]-withoutIndex {𝟎}   {x ⊰ l} = skip [⊑]-reflexivity
[⊑]-withoutIndex {𝐒 n} {x ⊰ l} = use [⊑]-withoutIndex

[⊑]-initial : (initial n l ⊑ l)
[⊑]-initial {𝟎}   {∅}     = empty
[⊑]-initial {𝐒 n} {∅}     = empty
[⊑]-initial {𝟎}   {x ⊰ l} = [⊑]-minimum
[⊑]-initial {𝐒 n} {x ⊰ l} = use [⊑]-initial

[⊑]-skip : (List.skip n l ⊑ l)
[⊑]-skip {𝟎}   {∅}     = empty
[⊑]-skip {𝐒 n} {∅}     = empty
[⊑]-skip {𝟎}   {x ⊰ l} = [⊑]-reflexivity
[⊑]-skip {𝐒 n} {x ⊰ l} = skip [⊑]-skip

[⊑]-empty : (l ⊑ ∅) → (l ≡ ∅)
[⊑]-empty {∅}     _ = [≡]-intro
[⊑]-empty {_ ⊰ _} ()

[⊑]-length : (l₁ ⊑ l₂) → (length(l₁) ≤ length(l₂))
[⊑]-length empty    = [≤]-minimum
[⊑]-length (use  p) = [≤]-with-[𝐒] ⦃ [⊑]-length p ⦄
[⊑]-length (skip p) = [≤]-predecessor ([≤]-with-[𝐒] ⦃ [⊑]-length p ⦄)

[⊏]-without-[⊰] : ((x ⊰ l₁) ⊏ (y ⊰ l₂)) → (l₁ ⊏ l₂)
[⊏]-without-[⊰]                (use p)         = p
[⊏]-without-[⊰]                (skip (use p))  = skip p
[⊏]-without-[⊰] {x = x}{y = y} (skip (skip p)) = skip ([⊑]-without-[⊰] {x = x}{y = y} (skip p))

[⊏]-irreflexivity : ¬(l ⊏ l)
[⊏]-irreflexivity {∅} ()
[⊏]-irreflexivity {x ⊰ l} p = [⊏]-irreflexivity {l} ([⊏]-without-[⊰] p)

[⊏]-to-[⊑] : (l₁ ⊏ l₂) → (l₁ ⊑ l₂)
[⊏]-to-[⊑] (use  p) = use ([⊏]-to-[⊑] p)
[⊏]-to-[⊑] (skip p) = skip p

[⊏]-skip-[⊰] : (l₁ ⊏ l₂) → (l₁ ⊏ (x ⊰ l₂))
[⊏]-skip-[⊰] (use p) = skip ([⊏]-to-[⊑] (use p))
[⊏]-skip-[⊰] (skip x) = skip (skip x)

[⊏]-transitivity : (l₁ ⊏ l₂) → (l₂ ⊏ l₃) → (l₁ ⊏ l₃)
[⊏]-transitivity p        (skip (skip q)) = skip(skip([⊑]-transitivity ([⊏]-to-[⊑] p) q))
[⊏]-transitivity (use p)  (use q)         = use ([⊏]-transitivity p q)
[⊏]-transitivity (use p)  (skip (use q))  = skip (use ([⊑]-transitivity ([⊏]-to-[⊑] p) q))
[⊏]-transitivity (skip p) (use q)         = skip([⊑]-transitivity p ([⊏]-to-[⊑] q))
[⊏]-transitivity (skip p) (skip (use q))  = skip(skip([⊑]-transitivity p q))

[⊏]-asymmetry : (l₂ ⊏ l₁) → (l₁ ⊏ l₂) → ⊥
[⊏]-asymmetry p q = [⊏]-irreflexivity([⊏]-transitivity p q)

[⊏]-minimum : (l ≡ ∅) ∨ (∅ ⊏ l)
[⊏]-minimum {∅}     = [∨]-introₗ [≡]-intro
[⊏]-minimum {x ⊰ l} = [∨]-introᵣ (skip [⊑]-minimum)

[⊏]-emptyₗ : (∅ ⊏ (x ⊰ l))
[⊏]-emptyₗ {l = ∅}     = skip empty
[⊏]-emptyₗ {l = x ⊰ l} = skip ([⊏]-to-[⊑] ([⊏]-emptyₗ {l = l}))

[⊏]-emptyᵣ : ¬(l ⊏ ∅)
[⊏]-emptyᵣ ()

[⊏]-length : (l₁ ⊏ l₂) → (length(l₁) < length(l₂))
[⊏]-length (use  p) = [≤]-with-[𝐒] ⦃ [⊏]-length p ⦄
[⊏]-length (skip p) = [≤]-with-[𝐒] ⦃ [⊑]-length p ⦄

[⊏]-prepend : (l ⊏ x ⊰ l)
[⊏]-prepend = skip [⊑]-reflexivity

[⊏]-postpend : (l ⊏ postpend x l)
[⊏]-postpend {∅}     = skip empty
[⊏]-postpend {a ⊰ l} = use ([⊏]-postpend {l})

[⊏]-map : ∀{f : T → T₂} → (l₁ ⊏ l₂) → (map f(l₁) ⊏ map f(l₂))
[⊏]-map (use  p) = use ([⊏]-map p)
[⊏]-map (skip p) = skip ([⊑]-map p)

[⊏]-tail : (∅ ⊏ l) → (tail l ⊏ l)
[⊏]-tail (skip _) = skip [⊑]-reflexivity

[⊏]-initial : (n < length(l)) → (initial n l ⊏ l)
[⊏]-initial {𝟎}   {x ⊰ l} p = [⊏]-emptyₗ
[⊏]-initial {𝐒 n} {x ⊰ l} p = use ([⊏]-initial {n} ([≤]-without-[𝐒] p))

[⊏]-skip : (𝟎 < n) → (n < length(l)) → (List.skip n l ⊏ l)
[⊏]-skip {𝐒 n} {x ⊰ l} p q = skip [⊑]-skip

[⊏]-withoutIndex : (n < length(l)) → (withoutIndex n l ⊏ l)
[⊏]-withoutIndex {𝟎}   {x ⊰ l} p = [⊏]-prepend
[⊏]-withoutIndex {𝐒 n} {x ⊰ l} p = use ([⊏]-withoutIndex ([≤]-without-[𝐒] p))

[⊏]-separate₂ : let (l₁ , l₂) = separate₂(l) in (2 ≤ length(l)) → ((l₁ ⊏ l) ∧ (l₂ ⊏ l))
[⊏]-separate₂ {x ⊰ ∅}     (succ())
Tuple.left  ([⊏]-separate₂ {x ⊰ y ⊰ l} (succ (succ min))) = use (skip (Tuple.left  [⊑]-separate₂))
Tuple.right ([⊏]-separate₂ {x ⊰ y ⊰ l} (succ (succ min))) = skip (use (Tuple.right [⊑]-separate₂))

[⊏]ᵣ-of-[++]ₗ : (∅ ⊏ l₂) → (l₁ ⊏ (l₂ ++ l₁))
[⊏]ᵣ-of-[++]ₗ {a ⊰ l₂} {l₁} (skip p) = skip([⊑]ᵣ-of-[++]ₗ {l₁}{l₂})

[⊏]ᵣ-of-[++]ᵣ : (∅ ⊏ l₂) → (l₁ ⊏ (l₁ ++ l₂))
[⊏]ᵣ-of-[++]ᵣ {a ⊰ l₂} {∅}      (skip p) = skip p
[⊏]ᵣ-of-[++]ᵣ {a ⊰ l₂} {b ⊰ l₁} (skip p) = use ([⊏]ᵣ-of-[++]ᵣ {a ⊰ l₂} {l₁} (skip p))

[⊑][⊏]-transitivity-like : (l₁ ⊑ l₂) → (l₂ ⊏ l₃) → (l₁ ⊏ l₃)
[⊑][⊏]-transitivity-like p        (skip q) = skip([⊑]-transitivity p q)
[⊑][⊏]-transitivity-like (use  p) (use  q) = use ([⊑][⊏]-transitivity-like p q)
[⊑][⊏]-transitivity-like (skip p) (use  q) = [⊏]-skip-[⊰] ([⊑][⊏]-transitivity-like p q)

instance
  [⊏][<]-on-length-sub : (_⊏_ {T = T}) ⊆₂ ((_<_) on₂ length)
  [⊏][<]-on-length-sub = intro [⊏]-length

module _ where
  open Structure.Relator.Ordering.Strict.Properties

  instance
    [<]-on-length-well-founded : WellFounded((_<_) on₂ (length {T = T}))
    [<]-on-length-well-founded = wellfounded-image-by-trans

  instance
    [⊏]-well-founded : WellFounded(_⊏_ {T = T})
    [⊏]-well-founded = accessibleₗ-sub₂ ⦃ [⊏][<]-on-length-sub ⦄

[⊑]-to-[⊏] : (l₁ ⊑ l₂) → ((l₁ ⊏ l₂) ∨ (length(l₁) ≡ length(l₂)))
[⊑]-to-[⊏] empty    = [∨]-introᵣ [≡]-intro
[⊑]-to-[⊏] (use p)  = Either.map use ([≡]-with(𝐒)) ([⊑]-to-[⊏] p)
[⊑]-to-[⊏] (skip p) = [∨]-introₗ (skip p)