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

{- Our goal in this file is to observe some structure possessed by the
   universes of types, reflexive graphs, type families, and so on. Somewhat
   more precisely, we develop an imperfect structure of internal model of type
   theory, with enough ingredients to get some type theoretic developments off
   the ground.

   We begin with the basic structure of type dependency, with operations for
   context extension, weakening, substitution, and identity morphisms (the
   `variable rule'). Once this structure is implemented, we introduce the
   structure of usual type constructors Σ, Π, Id, the unit type, and ℕ.

   The reason this is an `imperfect' notion of model structure is that
   in our internal model structure, we have identifications in the role of
   judgmental equalities. This leads to the usual coherence problem, which we
   do not attempt to solve. As we said before, our goal is merely to postulate
   enough equalities so that we can introduce and work with the type
   constructors. We then proceed to develop some examples.
-}

module models where

import Lecture15
open Lecture15 public

Contexts :
  ( l : Level) → UU (lsuc l)
Contexts l = UU l

Families :
  { l1 : Level} (l2 : Level) (ctx : Contexts l1) → UU (l1 ⊔ (lsuc l2))
Families l2 ctx = ctx → UU l2

Terms :
  { l1 l2 : Level} (l3 : Level)
  ( ctx : Contexts l1) (fam : Families l2 ctx) → UU (l1 ⊔ (l2 ⊔ (lsuc l3)))
Terms l3 ctx fam = (Γ : ctx) → (fam Γ) → UU l3

Context-Extensions :
  { l1 l2 : Level}
  ( ctx : Contexts l1) (fam : Families l2 ctx) → UU (l1 ⊔ l2)
Context-Extensions ctx fam = (Γ : ctx) → (fam Γ) → ctx

Family-Extensions :
  { l1 l2 : Level}
  ( ctx : Contexts l1) (fam : Families l2 ctx)
  ( ctx-ext : Context-Extensions ctx fam) → UU (l1 ⊔ l2)
Family-Extensions ctx fam ctx-ext =
  ( Γ : ctx) → (A : fam Γ) → (fam (ctx-ext Γ A)) → fam Γ

Model-Base :
  ( l1 l2 l3 : Level) → UU (lsuc l1 ⊔ (lsuc l2 ⊔ lsuc l3))
Model-Base l1 l2 l3 =
  Σ ( Contexts l1)
    ( λ ctx → Σ (Families l2 ctx)
      ( λ fam → Σ (Terms l3 ctx fam)
        ( λ tm → Σ (Context-Extensions ctx fam) (Family-Extensions ctx fam))))

Hom-Model-Base :
  { l1 l2 l3 l1' l2' l3' : Level} →
  Model-Base l1 l2 l3 → Model-Base l1' l2' l3' → UU _
Hom-Model-Base
  ( pair ctx (pair fam (pair tm (pair ctx-ext fam-ext))))
  ( pair ctx' (pair fam' (pair tm' (pair ctx-ext' fam-ext')))) =
   Σ ( ctx → ctx')
     ( λ h-ctx → Σ ((Γ : ctx) → (fam Γ) → (fam' (h-ctx Γ)))
       ( λ h-fam →
         Σ ((Γ : ctx) (A : fam Γ) → (tm Γ A) → tm' (h-ctx Γ) (h-fam Γ A))
         ( λ h-tm →
           Σ ( (Γ : ctx) (A : fam Γ) →
               Id
                 ( h-ctx (ctx-ext Γ A))
                 ( ctx-ext' (h-ctx Γ) (h-fam Γ A)))
             ( λ h-ctx-ext → (Γ : ctx) (A : fam Γ) (B : fam (ctx-ext Γ A)) →
               Id
                 ( h-fam Γ (fam-ext Γ A B))
                 ( fam-ext'
                   ( h-ctx Γ)
                   ( h-fam Γ A)
                   ( tr fam' (h-ctx-ext Γ A) (h-fam (ctx-ext Γ A) B)))))))

Assoc-Ctx-ext :
  { l1 l2 l3 : Level} (M : Model-Base l1 l2 l3) → UU (l1 ⊔ l2)
Assoc-Ctx-ext (pair ctx (pair fam (pair tm (pair ctx-ext fam-ext)))) =
  ( Γ : ctx) (A : fam Γ) (B : fam (ctx-ext Γ A)) →
    Id (ctx-ext (ctx-ext Γ A) B) (ctx-ext Γ (fam-ext Γ A B))

Slice-Model-Base :
  { l1 l2 l3 : Level} (M : Model-Base l1 l2 l3)
  ( assoc : Assoc-Ctx-ext M) →
  ( Γ : pr1 M) → Model-Base l2 l2 l3
Slice-Model-Base
  ( pair ctx (pair fam (pair tm (pair ctx-ext fam-ext)))) assoc Γ =
  pair (fam Γ)
    ( pair (λ A → fam (ctx-ext Γ A))
      ( pair (λ A B → tm (ctx-ext Γ A) B)
        ( pair (fam-ext Γ)
          ( λ A B C →
            fam-ext (ctx-ext Γ A) B (tr fam (inv (assoc Γ A B)) C)))))

Empty-context :
  { l1 l2 l3 : Level} (M : Model-Base l1 l2 l3) → UU l1
Empty-context M = pr1 M

Axiom-Empty-Context :
  { l1 l2 l3 : Level}
  (M : Model-Base l1 l2 l3) (empty-ctx : Empty-context M) → UU (l1 ⊔ l2)
Axiom-Empty-Context
  ( pair ctx (pair fam (pair tm (pair ctx-ext fam-ext)))) empty-ctx =
  is-equiv (ctx-ext empty-ctx)

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro


text:
-- An ATP local hint can be only a postulate, function or a data
-- constructor.

-- This error is detected by Syntax.Translation.ConcreteToAbstract.

module ATPBadLocalHint3 where

postulate
  D    : Set
  _≡_  : D → D → Set
  zero : D
  succ : D → D

data N : D → Set where
  zN :               N zero
  sN : ∀ {n} → N n → N (succ n)

refl : ∀ n → N n → n ≡ n
refl n Nn = prf
  where
    postulate prf : n ≡ n
    {-# ATP prove prf Nn #-}

ext: agda

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
------------------------------------------------------------------------
-- The reader monad transformer
------------------------------------------------------------------------

-- The interface is based on that used by the "mtl" package on
-- Hackage.

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

open import Equality

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

open import Prelude

open Derived-definitions-and-properties eq
open import Monad eq

-- The reader monad transformer, defined using a wrapper type to make
-- instance resolution easier.

record ReaderT {s} (S : Type s)
               (M : Type s → Type s)
               (A : Type s) : Type s where
  constructor wrap
  field
    run : S → M A

open ReaderT public

instance

  -- ReaderT is a "raw monad" transformer.

  raw-monad-transformer :
    ∀ {s} {S : Type s} →
    Raw-monad-transformer (ReaderT S)
  run (Raw-monad.return (Raw-monad-transformer.transform
                           raw-monad-transformer) x) =
    λ _ → return x
  run (Raw-monad._>>=_ (Raw-monad-transformer.transform
                          raw-monad-transformer) x f) =
    λ s → run x s >>= λ x → run (f x) s

  run (Raw-monad-transformer.liftʳ raw-monad-transformer m) =
    λ _ → m

  transform : ∀ {s} {S : Type s} {M} ⦃ is-raw-monad : Raw-monad M ⦄ →
              Raw-monad (ReaderT S M)
  transform = Raw-monad-transformer.transform raw-monad-transformer

-- ReaderT is a monad transformer (assuming extensionality).

monad-transformer :
  ∀ {s} {S : Type s} →
  Extensionality s s →
  Monad-transformer (ReaderT S)
Monad.raw-monad (Monad-transformer.transform (monad-transformer _)) =
  Raw-monad-transformer.transform raw-monad-transformer

Monad.left-identity (Monad-transformer.transform
                       (monad-transformer ext)) x f =
  cong wrap (apply-ext ext λ s →
    (return x >>= λ x → run (f x) s)  ≡⟨ left-identity _ _ ⟩∎
    run (f x) s                       ∎)

Monad.right-identity (Monad-transformer.transform
                        (monad-transformer ext)) x =
  cong wrap (apply-ext ext λ s →
    run x s >>= return  ≡⟨ right-identity _ ⟩∎
    run x s             ∎)

Monad.associativity (Monad-transformer.transform
                       (monad-transformer ext)) x f g =
  cong wrap (apply-ext ext λ s →
    (run x s >>= λ x → run (f x) s >>= λ x → run (g x) s)    ≡⟨ associativity _ _ _ ⟩∎
    ((run x s >>= λ x → run (f x) s) >>= λ x → run (g x) s)  ∎)

Monad-transformer.liftᵐ (monad-transformer _) = liftʳ

Monad-transformer.lift-return (monad-transformer ext) x =
  cong wrap (apply-ext ext λ _ →
    return x  ∎)

Monad-transformer.lift->>= (monad-transformer ext) x f =
  cong wrap (apply-ext ext λ _ →
    x >>= f  ∎)

-- Returns the "state".

ask : ∀ {s} {S : Type s} {M} ⦃ is-monad : Raw-monad M ⦄ →
      ReaderT S M S
run ask = return

-- Modifies the "state" in a given computation.

local : ∀ {s} {S : Type s} {M A} ⦃ is-monad : Raw-monad M ⦄ →
        (S → S) → ReaderT S M A → ReaderT S M A
run (local f m) = run m ∘ f

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Agda.Builtin.Equality
open import Agda.Primitive

record R a : Set (lsuc a) where
  field
    P : {A : Set a} → A → A → Set a

r : ∀ ℓ → R ℓ
R.P (r _) = _≡_

postulate
  cong  : ∀ {a b} {A : Set a} {B : Set b} {x y : A}
          (f : A → B) → R.P (r a) x y → R.P (r b) (f x) (f y)
  magic : ∀ {a} {A : Set a} {x y : A} (z : A) → y ≡ z → x ≡ z

record Raw-monad {f : Level → Level}
                 (M : ∀ {ℓ} → Set ℓ → Set (f ℓ)) ℓ₁ ℓ₂ :
                 Set (f ℓ₁ ⊔ f ℓ₂ ⊔ lsuc (ℓ₁ ⊔ ℓ₂)) where
  infixl 5 _>>=_
  field
    return : {A : Set ℓ₁} → A → M A
    _>>=_  : {A : Set ℓ₁} {B : Set ℓ₂} → M A → (A → M B) → M B

module Raw-monad⁺
  {f : Level → Level}
  {M : ∀ {ℓ} → Set ℓ → Set (f ℓ)}
  (m : ∀ {ℓ₁ ℓ₂} → Raw-monad M ℓ₁ ℓ₂)
  where

  private
    module M′ {ℓ₁ ℓ₂} = Raw-monad (m {ℓ₁ = ℓ₁} {ℓ₂ = ℓ₂})
  open M′ public using (_>>=_)

  return : ∀ {a} {A : Set a} → A → M A
  return = M′.return {ℓ₂ = lzero}

open Raw-monad⁺ ⦃ … ⦄ public

record Monad⁻ {f : Level → Level}
              (M : ∀ {ℓ} → Set ℓ → Set (f ℓ))
              ⦃ raw-monad : ∀ {ℓ₁ ℓ₂} → Raw-monad M ℓ₁ ℓ₂ ⦄
              ℓ₁ ℓ₂ ℓ₃ :
              Set (f ℓ₁ ⊔ f ℓ₂ ⊔ f ℓ₃ ⊔ lsuc (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  field
    associativity :
      {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃} →
      (x : M A) (f : A → M B) (g : B → M C) →
      x >>= (λ x → f x >>= g) ≡ x >>= f >>= g

module Monad⁻⁺
  {f : Level → Level}
  {M : ∀ {ℓ} → Set ℓ → Set (f ℓ)}
  ⦃ raw-monad : ∀ {ℓ₁ ℓ₂} → Raw-monad M ℓ₁ ℓ₂ ⦄
  (m : ∀ {ℓ₁ ℓ₂ ℓ₃} → Monad⁻ M ℓ₁ ℓ₂ ℓ₃)
  where

  private
    module M′ {ℓ₁ ℓ₂ ℓ₃} = Monad⁻ (m {ℓ₁ = ℓ₁} {ℓ₂ = ℓ₂} {ℓ₃ = ℓ₃})
  open M′ public

open Monad⁻⁺ ⦃ … ⦄ public

data Maybe {a} (A : Set a) : Set a where
  nothing : Maybe A
  just    : A → Maybe A

postulate
  maybe : ∀ {a b} {A : Set a} {B : Maybe A → Set b} →
          ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x

record MaybeT {ℓ}
              (f : Level → Level)
              (M : Set ℓ → Set (f ℓ))
              (A : Set ℓ) : Set (f ℓ) where
  constructor wrap
  field
    run : M (Maybe A)

open MaybeT

instance

  transformʳ :
    ∀ {ℓ₁ ℓ₂}
    {f : Level → Level}
    {M : ∀ {ℓ} → Set ℓ → Set (f ℓ)} →
    ⦃ raw-monad : ∀ {ℓ₁ ℓ₂} → Raw-monad M ℓ₁ ℓ₂ ⦄ →
    Raw-monad (MaybeT f M) ℓ₁ ℓ₂
  run (Raw-monad.return transformʳ x)   = return (just x)
  run (Raw-monad._>>=_  transformʳ x f) =
    run x >>= maybe (λ x → run (f x)) (return nothing)

transformᵐ :
  {f : Level → Level}
  {M : ∀ {ℓ} → Set ℓ → Set (f ℓ)}
  ⦃ raw-monad : ∀ {ℓ₁ ℓ₂} → Raw-monad M ℓ₁ ℓ₂ ⦄
  ⦃ monad : ∀ {ℓ₁ ℓ₂ ℓ₃} → Monad⁻ M ℓ₁ ℓ₂ ℓ₃ ⦄ →
  Monad⁻ (MaybeT f M) lzero lzero lzero
Monad⁻.associativity transformᵐ x f g = cong wrap (
  magic ((run x >>= maybe (λ x → run (f x)) (return nothing)) >>=
         maybe (λ x → run (g x)) (return nothing))
        (associativity _ _ _))

-- WAS: rejected in 2.6.0 with
-- No instance of type Raw-monad _M_345 ℓ₁ ℓ₂ was found in scope.

-- Should succeed.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Categories.2-Category.Categories where

open import Level
open import Data.Product

open import Categories.Category
open import Categories.2-Category
open import Categories.Functor using (module Functor) renaming (id to idF; _∘_ to _∘F_)
open import Categories.Functor.Constant
open import Categories.FunctorCategory
open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalTransformation
open import Categories.Product using (Product)

Categories : ∀ o ℓ e → 2-Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) (o ⊔ e)
Categories o ℓ e = record
  { Obj = Category o ℓ e
  ; _⇒_ = Functors
  ; id = λ {A} → Constant {D = Functors A A} idF
  ; —∘— = my-∘
  ; assoc = {!!}
  ; identityˡ = λ {A B} η → Heterogeneous.≡⇒∼ {C = Functors A B} {f = proj₂ η ∘₁ id} {proj₂ η} (Category.identityʳ B)
  ; identityʳ = λ {A B f g} η → Heterogeneous.≡⇒∼ {_} {_} {_} {C = Functors A B} {proj₁ f} {proj₁ g} {f = record {
                                                                                η =
                                                                                λ X →
                                                                                Category._∘_ B (Functor.F₁ (proj₁ g) (Category.id A))
                                                                                (NaturalTransformation.η (proj₁ η) X);
                                                                                commute = λ {a} {b} h → let open Category.HomReasoning B in begin
                    B [ B [ Functor.F₁ (proj₁ g) (Category.id A) ∘ NaturalTransformation.η (proj₁ η) b ] ∘ {!.Categories.NaturalTransformation.Core.F.F₁ (proj₁ f) (proj₁ g) h!} ]
                  ↓⟨ {!!} ⟩
                    B [ Functor.F₁ {!!} {!!} ∘ B [ Functor.F₁ (proj₁ g) (Category.id A) ∘ NaturalTransformation.η (proj₁ η) a ] ]
                  ∎ }
         } {proj₁ {_} {_} {_} {_} η} (Category.Equiv.trans B (Category.∘-resp-≡ˡ B (Functor.identity (proj₁ g))) (Category.identityˡ B))
  }
  where
  my-∘ : {A B C : Category o ℓ e} → Bifunctor (Functors B C) (Functors A B) (Functors A C)
  my-∘ {A} {B} {C} = record
    { F₀ = uncurry′ _∘F_
    ; F₁ = uncurry′ _∘₀_
    ; identity = λ {Fs} → Category.Equiv.trans C (Category.identityʳ C) (Functor.identity (proj₁ Fs))
    ; homomorphism = λ {_ _ _ f g} → Category.Equiv.sym C (interchange {α = proj₁ g} {proj₂ g} {proj₁ f} {proj₂ f})
    ; F-resp-≡ = λ {_ _ f g} → my-resp {f = f} {g}
    }
    where
    PF = Product (Functors B C) (Functors A B)

    .my-resp : ∀ {F G} {f g : PF [ F , G ]} → PF [ f ≡ g ] → Functors A C [ uncurry′ _∘₀_ f ≡ uncurry _∘₀_ g ]
    my-resp {f = f₁ , f₂} {g₁ , g₂} (f₁≡g₁ , f₂≡g₂) = ∘₀-resp-≡ {f = f₁} {g₁} {f₂} {g₂} f₁≡g₁ f₂≡g₂

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Data.Num where

open import Data.List using (List; []; _∷_; foldr)
open import Data.Nat
open ≤-Reasoning

open import Data.Nat.Etc
open import Data.Nat.DivMod
open import Data.Nat.DivMod.Properties using (div-mono)
open import Data.Nat.Properties using (m≤m+n; n≤m+n;_+-mono_; pred-mono; ∸-mono; ≰⇒>; n∸n≡0; +-∸-assoc; m+n∸n≡m)
open import Data.Nat.Properties.Simple using (+-right-identity; +-suc; +-assoc; +-comm; distribʳ-*-+)
open import Data.Fin.Properties using (bounded)
open import Data.Fin using (Fin; fromℕ≤; inject≤; #_)
    renaming (toℕ to F→N; fromℕ to N→F; zero to Fz; suc to Fs)
open import Data.Product
open import Data.Maybe

open import Induction.Nat using (rec; Rec)
import Level
open import Function
open import Data.Unit using (tt)
open import Relation.Nullary
open import Relation.Nullary.Decidable using (True; False; toWitness; toWitnessFalse; fromWitness; fromWitnessFalse)
open import Relation.Nullary.Negation using (contradiction; contraposition)
open import Relation.Binary

open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; sym; trans; inspect)
open PropEq.≡-Reasoning
    renaming (begin_ to beginEq_; _≡⟨_⟩_ to _≡Eq⟨_⟩_; _∎ to _∎Eq)
-- Surjective (ℕm):
--  base = 1, digits = {m ... (m + n) - 1}, m ≥ 1, n ≥ m
--  base > 1, digits = {m ... (m + n) - 1}, m ≥ 0, n ≥ max base (base × m)
-- Bijective:
--  base ≥ 1, digits = {1 .. base}
--
--  Digits:
--    Digit m n represents a Digit ranging from m to (m + n - 1)
--    e.g. Digit 2 0 2 = {0, 1}         for ordinary binary number
--         Digit 2 1 2 = {1, 2}         for zeroless binary number
--         Digit 2 0 3 = {0, 1, 2}      for redundant binary number
--
data Digit : (base from range : ℕ) → Set where
    -- unary digit: {0, 1 .. n-1}
    U0 : ∀ {n} → Fin n
         → {2≤n : True (2 ≤? n)} -- i.e. must have digit '1'
         → Digit 1 0 n
    -- unary digit: {m .. m+n-1}
    U1 : ∀ {m n}
         → Fin n
         → {m≤n : True (suc m ≤? n)}
         → Digit 1 (suc m) n
    -- k-adic digit: {m .. m+n-1}
    D  : ∀ {b m n}
         → Fin n
         → let base = suc (suc b) in
           {b≤n : True (base ≤? n)} → {bm≤n : True ((base * m) ≤? n)}
         → Digit base m n

-- without offset, {0 .. n-1}
D→F : ∀ {b m n} → Digit b m n → Fin n
D→F (U0 x) = x
D→F (U1 x) = x
D→F (D x) = x

-- with offset, {m .. m+n-1}
D→N : ∀ {b m n} → Digit b m n → ℕ
D→N {m = m} d = m + F→N (D→F d)

-- infix 4 _D≤_ -- _D<_ _≥′_ _>′_

-- data _D≤_ {b m n} (x : Digit b m n) : (y : Digit b m n) → Set where
--   D≤-refl :                          x D≤ x
--  D≤-step : ∀ {y} (xD≤y : x D≤ y) → x D≤
  -- ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n

private

    -- alias
    ℕ-isDecTotalOrder   = DecTotalOrder.isDecTotalOrder decTotalOrder
    ℕ-isTotalOrder      = IsDecTotalOrder.isTotalOrder ℕ-isDecTotalOrder
    ℕ-isPartialOrder    = IsTotalOrder.isPartialOrder ℕ-isTotalOrder
    ℕ-isPreorder        = IsPartialOrder.isPreorder ℕ-isPartialOrder
    ≤-refl      = IsPreorder.reflexive ℕ-isPreorder
    ≤-antisym   = IsPartialOrder.antisym ℕ-isPartialOrder
    ≤-total     = IsTotalOrder.total ℕ-isTotalOrder

    -- helper function for adding two 'Fin n' with offset 'm'
    -- (m + x) + (m + y) - m = m + x + y
    D+sum : ∀ {n} (m : ℕ) → (x y : Fin n) → ℕ
    D+sum m x y = m + (F→N x) + (F→N y)

maxpress-pred : ℕ → Set
maxpress-pred _ = ℕ → ℕ

maxpress-rec-struct : (x : ℕ) → Rec Level.zero maxpress-pred x → (bound : ℕ) → ℕ
maxpress-rec-struct zero p bound = 0
maxpress-rec-struct (suc x) p bound with bound ≤? suc (p bound)
maxpress-rec-struct (suc x) p bound | yes q = suc (p bound) ∸ bound
maxpress-rec-struct (suc x) p bound | no ¬q = suc (p bound)

-- if x ≥ bound, then substract bound from x, until x < bound
maxpress : (x bound : ℕ) → ℕ
maxpress = rec maxpress-pred maxpress-rec-struct

maxpressed<bound : (x bound : ℕ) → (≢0 : False (bound ≟ 0)) → maxpress x bound < bound
maxpressed<bound zero    zero        ()
maxpressed<bound zero    (suc bound) ≢0 = s≤s z≤n
maxpressed<bound (suc x) zero        ()
maxpressed<bound (suc x) (suc bound) ≢0 with suc bound ≤? suc (maxpress x (suc bound))
maxpressed<bound (suc x) (suc bound) ≢0 | yes p =
    begin
        suc (maxpress x (suc bound) ∸ bound)
    ≤⟨ ≤-refl (sym (+-∸-assoc 1 p)) ⟩
        suc (maxpress x (suc bound)) ∸ bound
    ≤⟨ ∸-mono {suc (maxpress x (suc bound))} {suc bound} {bound} {bound} (maxpressed<bound x (suc bound) tt) (≤-refl refl) ⟩
        suc bound ∸ bound
    ≤⟨ ≤-refl (m+n∸n≡m 1 bound) ⟩
        suc zero
    ≤⟨ s≤s z≤n ⟩
        suc bound
    ∎
maxpressed<bound (suc x) (suc bound) ≢0 | no ¬p = ≰⇒> ¬p

maxpress′ : (x bound : ℕ) → (≢0 : False (bound ≟ 0)) → Fin bound
maxpress′ x bound ≢0 = fromℕ≤ {maxpress x bound} (maxpressed<bound x bound ≢0)

_D+_ : ∀ {b m n} → Digit b m n → Digit b m n → Digit b m n
_D+_ {zero}                ()     ()
_D+_ {suc zero}            x      _      = x
_D+_ {suc (suc b)} {m} {n} (D x) (D y {b≤n} {bm≤n}) = D (maxpress′ (D+sum m x y) n n≢0) {b≤n} {bm≤n}
    where   n≢0 = fromWitnessFalse $ >⇒≢ $
                begin
                    suc zero
                ≤⟨ s≤s z≤n ⟩
                    suc (suc b)
                ≤⟨ toWitness b≤n ⟩
                    n
                ∎

--      2 ≤ base
--  ⇒  max * 2 ≤ max * base
--  ⇒  max * 2 / base ≤ max

{-
_D⊕_ : ∀ {b m n} → Digit b m n → Digit b m n → Maybe (Digit b m n)
_D⊕_                       (U0 x) y = just y
_D⊕_                       (U1 x) y = just y
_D⊕_ {suc (suc b)} {m} {n} (D x) (D y) with suc (D+sum m x y) ≤? n
_D⊕_ {suc (suc b)} {m} {n} (D x) (D y) | yes p = nothing
_D⊕_ {suc (suc b)} {m} {n} (D x) (D y {b≤n} {bm≤n}) | no ¬p with D+sum m x y divMod (suc (suc b)) | inspect (λ w → _divMod_ (D+sum m x y) (suc (suc b)) {≢0 = w}) tt
_D⊕_ {suc (suc b)} {m} {n} (D x) (D y {b≤n} {bm≤n}) | no ¬p | result quotient remainder property | PropEq.[ eq ] =
    let base = suc (suc b)
        sum = D+sum m x y
        quotient<n = begin
                suc quotient
            ≤⟨ div-mono base tt {!    !} ⟩
                {!   !}
            ≤⟨ {!   !} ⟩
                {!   !}
            ≤⟨ {!   !} ⟩
                {!   !}
            ≤⟨ {!   !} ⟩
                n
            ∎
    in  just (D (fromℕ≤ {quotient} quotient<n) {b≤n} {bm≤n})
-}
{-
    let base = suc (suc b)
        sum = D+sum m x y
        result quotient remainder property = _divMod_ sum base {tt}
        quotient<n = begin
                DivMod.quotient (sum divMod {! base  !})
            ≤⟨ {!   !} ⟩
                {!   !}
            ≤⟨ {!   !} ⟩
                {!   !}
            ≤⟨ {!   !} ⟩
                {!   !}
            ≤⟨ {!   !} ⟩
                n
            ∎
    in  just (D (fromℕ≤ {quotient} quotient<n) {b≤n} {bm≤n})
-}
{-

    begin
        {!   !}
    <⟨ {!   !} ⟩
        {!   !}
    <⟨ {!   !} ⟩
        {!   !}
    ∎

    begin
        {!   !}
    ≤⟨ {!    !} ⟩
        {!    !}
    ≤⟨ {!    !} ⟩
        {!   !}
    ≤⟨ {!    !} ⟩
        {!   !}
    ≤⟨ {!    !} ⟩
        {!   !}
    ∎
    beginEq
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ∎Eq
-}

data System : (base from range : ℕ) → Set where
    Sys : ∀ {b m n} → List (Digit (suc b) m n) → System (suc b) m n
{-
_S+_ : ∀ {b m n} → System b m n → System b m n → System b m n
Sys []       S+ Sys ys = Sys ys
Sys xs       S+ Sys [] = Sys xs
Sys (x ∷ xs) S+ Sys (y ∷ ys) = {! x  !}

S→N : ∀ {b m n} → System b m n → ℕ
S→N {zero} ()
S→N {suc b} (Sys list) = foldr (shift-then-add (suc b)) 0 list
    where   shift-then-add : ∀ {m n} → (b : ℕ) → Digit b m n → ℕ → ℕ
            shift-then-add b x acc = (D→N x) + (acc * b)
-}
--
--  Example
--

private
    one : Digit 2 1 2
    one = D Fz

    two : Digit 2 1 2
    two = D (Fs Fz)

    u0 : Digit 1 0 2
    u0 = U0 Fz

    u1 : Digit 1 1 1
    u1 = U1 Fz

    a0 : Digit 3 0 4
    a0 = D Fz

    a1 : Digit 3 0 4
    a1 = D (Fs Fz)

    a2 : Digit 3 0 4
    a2 = D (Fs (Fs Fz))

    a3 : Digit 3 0 4
    a3 = D (Fs (Fs (Fs Fz)))

    a : System 2 1 2
    a = Sys (one ∷ two ∷ two ∷ [])

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
-- Various small test cases that failed at some point or another
-- during the development of the parameter refinement feature.

module _ where

open import Agda.Primitive
open import Agda.Builtin.Nat hiding (_<_)
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.List

[_≡_] : ∀ {a} {A : Set a} (x y : A) → x ≡ y → A
[ x ≡ y ] refl = x

pattern ! = refl

module CoPatterns where
  record R : Set where
    field b : Nat
  open R

  sharp : Nat → R
  sharp n = f n
    where
      f : Nat → R
      b (f m) = m

  r₁ : (n : Nat) → R
  b (r₁ n) = n

  module _ (n : Nat) where
    r : R
    b r = n

  record Σ (A : Set) (B : A → Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B fst
  open Σ public

  data T : Nat → Set where
    zero : T zero
    suc  : ∀ {n} → T n → T (suc n)

  module _ (A : Set) where
    ex : Σ Nat T
    fst ex = suc zero
    snd ex = suc zero

module SimpleWith where
  module P (A : Set) where

    f : Nat → Nat
    f zero = 0
    f (suc n) with n
    f (suc n) | z = z

module MergeSort where
  data Vec (A : Set) : Nat → Set where
    []  : Vec A zero
    _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

  module Sort (A : Set) where

    merge : ∀ {n} → Vec A n → Vec A zero
    merge [] = []
    merge (x ∷ xs) = merge xs

module LetPatternBinding where
  record Wrap : Set where
    constructor wrap
    field wrapped : Nat

  fails : Wrap → Nat
  fails w = let wrap n = w in n

  record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
    constructor _,_
    field fst : A
          snd : B

  module _ (A B : Set) where

    const : A → B → A
    const x _ = x

    plus : A × B → A
    plus p = let a , b = p in const a b

module RefineStuff where
  module _ (x y : Nat) where

    foo : x ≡ suc y → Nat
    foo refl = y

  bar : (x y : Nat) → x ≡ y → Nat
  bar x y refl = y

  test : foo 2 1 refl ≡ 1
  test = refl

module Projections where
  module _ (X : Set) where

    record ∃ (a : Set) : Set where
      field
        witness : a

    f : ∃ X → X
    f r = ∃.witness r

module Delay where
  data Vec (A : Set) : Nat → Set where
     _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

  data Unit : Set where
    unit : Unit

  record DNat : Set₁ where
    field
      D     : Set
      force : D → Nat
  open DNat

  nonNil : ∀ {n} → Vec Unit n → Nat
  nonNil (i ∷ is) = suc (force f i)
    where
      f : DNat
      D     f      = Unit
      force f unit = zero

module Folds where

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

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

  module FoldAssoc
    {A : Set}(_∙_ : A → A → A)
    (assoc : ∀ x y z → ((x ∙ y) ∙ z) ≡ (x ∙ (y ∙ z))) where

    smashr = foldr _∙_
    smashl = foldl _∙_

    postulate
      foldl-plus : ∀ z₁ z₂ xs → smashl (z₁ ∙ z₂) xs ≡ (z₁ ∙ smashl z₂ xs)

    foldr=foldl : ∀ ∅ → (∀ x → (∅ ∙ x) ≡ (x ∙ ∅)) →
                  ∀ xs → Set
    foldr=foldl ∅ id []       = Nat
    foldr=foldl ∅ id (x ∷ xs) rewrite id x
                                     | foldl-plus x ∅ xs
                              = Nat

module With where
  data Vec (A : Set) : Nat → Set where
    []  : Vec A 0
    _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

  idV : ∀ {A n} → Vec A n → Vec A n
  idV [] = []
  idV (x ∷ xs) = x ∷ idV xs

  len : ∀ {A n} → Vec A n → Nat
  len {n = n} _ = n

  module _ (n : Nat) (xs : Vec Nat n) where

    f : Vec Nat n → Nat
    f [] = 0
    f (x ∷ ys) with idV ys
    f (x ∷ ys) | []     = [ n ≡ 1 ] !
    f (x ∷ ys) | z ∷ zs = [ n ≡ suc (suc (len zs)) ] !

module NestedWith where

  data Vec (A : Set) : Nat → Set where
    []  : Vec A 0
    cons : ∀ n → A → Vec A n → Vec A (suc n)

  module _ (X Y : Set) where

    f : ∀ n → Vec Nat n → Nat
    f _ [] = 0
    f .(suc m) (cons m x xs) with x
    f n (cons m x xs) | 0 = [ n ≡ suc m ] !
    f n (cons m x xs) | y with xs
    f n (cons m x xs) | y | []          = [ n ≡ 1 ] !
    f n (cons m x xs) | z | cons k y ys = [ n ≡ suc (suc k) ] !

module LetCase where
  record _×_ (A B : Set) : Set where
    constructor _,_
    field fst : A
          snd : B

  case_of_ : {A B : Set} → A → (A → B) → B
  case x of f = f x

  g : Nat × Nat → Nat
  g p = let a , b = p in
        case b of λ where
          zero    → a
          (suc b) → a

  f : Nat × (Nat × Nat) → Nat
  f p =
    let a , q = p
        b , c = q
    in  a + b + c

  module _ {a} {A : Set a} where
    h : List A → Nat → Nat → Nat
    h [] = λ _ _ → 0
    h (x ∷ xs) =
      let ys = xs in
      λ n → λ where m → h ys n m

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
------------------------------------------------------------------------
-- Indexed applicative functors
------------------------------------------------------------------------

-- Note that currently the applicative functor laws are not included
-- here.

module Category.Applicative.Indexed where

open import Data.Function
open import Data.Product
open import Category.Functor

IFun : Set → Set₁
IFun I = I → I → Set → Set

record RawIApplicative {I : Set} (F : IFun I) : Set₁ where
  infixl 4 _⊛_ _<⊛_ _⊛>_
  infix  4 _⊗_

  field
    pure : ∀ {i A} → A → F i i A
    _⊛_  : ∀ {i j k A B} → F i j (A → B) → F j k A → F i k B

  rawFunctor : ∀ {i j} → RawFunctor (F i j)
  rawFunctor = record
    { _<$>_ = λ g x → pure g ⊛ x
    }

  private
    open module RF {i j : I} =
           RawFunctor (rawFunctor {i = i} {j = j})
           public

  _<⊛_ : ∀ {i j k A B} → F i j A → F j k B → F i k A
  x <⊛ y = const <$> x ⊛ y

  _⊛>_ : ∀ {i j k A B} → F i j A → F j k B → F i k B
  x ⊛> y = flip const <$> x ⊛ y

  _⊗_ : ∀ {i j k A B} → F i j A → F j k B → F i k (A × B)
  x ⊗ y = (_,_) <$> x ⊛ y

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2017-08-24, issue #2253
--
-- Better error message for matching on abstract constructor.

-- {-# OPTIONS -v tc.lhs.split:30 #-}
-- {-# OPTIONS -v tc.lhs:30 #-}
-- {-# OPTIONS -v tc.lhs.flex:60 #-}

abstract
  data B : Set where
    x : B

data C : Set where
  c : B → C

f : C → C
f (c x) = c x

-- WAS:
--
-- Not in scope:
--   AbstractPatternShadowsConstructor.B.x
--     (did you mean 'x'?)
-- when checking that the pattern c x has type C

-- Expected:
--
-- Cannot split on abstract data type B
-- when checking that the pattern x has type B


text:
{-# OPTIONS --without-K --safe #-}
-- Actually, we're cheating (for expediency); this is
-- Symmetric Rig, not just Rig.
open import Categories.Category

module Categories.Category.RigCategory {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Data.Fin renaming (zero to 0F; suc to sucF)
open import Data.Product using (_,_)

open import Categories.Functor renaming (id to idF)
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Braided
open import Categories.Category.Monoidal.Symmetric
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.NaturalTransformation using (_∘ᵥ_; _∘ₕ_; _∘ˡ_; _∘ʳ_; NaturalTransformation)
open import Categories.Morphism C

-- Should probably split out Distributive Category out and make this be 'over' that.
record RigCategory {M⊎ M× : Monoidal C} (S⊎ : Symmetric M⊎)
   (S× : Symmetric M×) : Set (o ⊔ ℓ ⊔ e) where

  private
    module C = Category C

  open C hiding (_≈_)
  open Commutation
  module M⊎ = Monoidal M⊎
  module M× = Monoidal M×
  module S⊎ = Symmetric S⊎
  module S× = Symmetric S×
  open M⊎ renaming (_⊗₀_ to _⊕₀_; _⊗₁_ to _⊕₁_)
  open M×

  private
    0C : C.Obj
    0C = M⊎.unit
    1C : C.Obj
    1C = M×.unit

  private
    B⊗ : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X
    B⊗ {X} {Y} = S×.braiding.⇒.η (X , Y)
    B⊕ : ∀ {X Y} → X ⊕₀ Y ⇒ Y ⊕₀ X
    B⊕ {X} {Y} = S⊎.braiding.⇒.η (X , Y)

  field
    annₗ : ∀ {X} → 0C ⊗₀ X ≅ 0C
    annᵣ : ∀ {X} → X ⊗₀ 0C ≅ 0C
    distribₗ : ∀ {X Y Z} → X ⊗₀ (Y ⊕₀ Z) ≅ (X ⊗₀ Y) ⊕₀ (X ⊗₀ Z)
    distribᵣ : ∀ {X Y Z} → (X ⊕₀ Y) ⊗₀ Z ≅ (X ⊗₀ Z) ⊕₀ (Y ⊗₀ Z)

  private
    λ* : ∀ {X} → 0C ⊗₀ X ⇒ 0C
    λ* {X} = _≅_.from (annₗ {X})
    ρ* : ∀ {X} → X ⊗₀ 0C ⇒ 0C
    ρ* {X} = _≅_.from (annᵣ {X})
    module dl {X} {Y} {Z} = _≅_ (distribₗ {X} {Y} {Z})
    module dr {X} {Y} {Z} = _≅_ (distribᵣ {X} {Y} {Z})
    ⊗λ⇒ = M×.unitorˡ.from
    ⊗λ⇐ = M×.unitorˡ.to
    ⊗ρ⇒ = M×.unitorʳ.from
    ⊗ρ⇐ = M×.unitorʳ.to
    ⊗α⇒ = M×.associator.from
    ⊗α⇐ = M×.associator.to
    ⊕λ⇒ = M⊎.unitorˡ.from
    ⊕λ⇐ = M⊎.unitorˡ.to
    ⊕ρ⇒ = M⊎.unitorʳ.from
    ⊕ρ⇐ = M⊎.unitorʳ.to
    ⊕α⇒ = M⊎.associator.from
    ⊕α⇐ = M⊎.associator.to

  -- need II, IX, X, XV
  -- choose I, IV, VI, XI, XIII, XIX, XXIII and (XVI, XVII)
  field
    laplazaI : ∀ {A B C} →
      [ A ⊗₀ (B ⊕₀ C) ⇒ (A ⊗₀ C) ⊕₀ (A ⊗₀ B) ]⟨
        dl.from        ⇒⟨ (A ⊗₀ B) ⊕₀ (A ⊗₀ C) ⟩
        B⊕
      ≈
        C.id ⊗₁ B⊕    ⇒⟨ A ⊗₀ (C ⊕₀ B) ⟩
        dl.from
      ⟩
    laplazaII : ∀ {A B C} →
      [ (A ⊕₀ B) ⊗₀ C ⇒ (C ⊗₀ A) ⊕₀ (C ⊗₀ B) ]⟨
        B⊗             ⇒⟨ C ⊗₀ (A ⊕₀ B) ⟩
        dl.from
      ≈
        dr.from        ⇒⟨ (A ⊗₀ C) ⊕₀ (B ⊗₀ C) ⟩
        B⊗ ⊕₁ B⊗
      ⟩
    laplazaIV : {A B C D : Obj} →
      [ (A ⊕₀ B ⊕₀ C) ⊗₀ D ⇒ ((A ⊗₀ D) ⊕₀ (B ⊗₀ D)) ⊕₀ (C ⊗₀ D) ]⟨
         dr.from            ⇒⟨ (A ⊗₀ D) ⊕₀ ((B ⊕₀ C) ⊗₀ D) ⟩
         C.id ⊕₁ dr.from   ⇒⟨ (A ⊗₀ D) ⊕₀ ((B ⊗₀ D) ⊕₀ (C ⊗₀ D)) ⟩
         ⊕α⇐
      ≈
         ⊕α⇐ ⊗₁ C.id       ⇒⟨ ((A ⊕₀ B) ⊕₀ C) ⊗₀ D ⟩
         dr.from            ⇒⟨ ((A ⊕₀ B) ⊗₀ D) ⊕₀ (C ⊗₀ D) ⟩
         dr.from ⊕₁ C.id
      ⟩

    laplazaVI : {A B C D : Obj} →
      [ A ⊗₀ B ⊗₀ (C ⊕₀ D) ⇒ ((A ⊗₀ B) ⊗₀ C) ⊕₀ ((A ⊗₀ B) ⊗₀ D) ]⟨
          C.id ⊗₁ dl.from   ⇒⟨ A ⊗₀ ((B ⊗₀ C) ⊕₀ (B ⊗₀ D)) ⟩
          dl.from            ⇒⟨ (A ⊗₀ B ⊗₀ C) ⊕₀ (A ⊗₀ B ⊗₀ D) ⟩
          ⊗α⇐ ⊕₁ ⊗α⇐
      ≈
        ⊗α⇐                ⇒⟨ (A ⊗₀ B) ⊗₀ (C ⊕₀ D) ⟩
        dl.from
      ⟩
    laplazaIX : ∀ {A B C D} → [ (A ⊕₀ B) ⊗₀ (C ⊕₀ D) ⇒ (((A ⊗₀ C) ⊕₀ (B ⊗₀ C)) ⊕₀ (A ⊗₀ D)) ⊕₀ (B ⊗₀ D) ]⟨
        dr.from                ⇒⟨ (A ⊗₀ (C ⊕₀ D)) ⊕₀ (B ⊗₀ (C ⊕₀ D)) ⟩
        dl.from ⊕₁ dl.from     ⇒⟨ ((A ⊗₀ C) ⊕₀ (A ⊗₀ D)) ⊕₀ ((B ⊗₀ C) ⊕₀ (B ⊗₀ D)) ⟩
        ⊕α⇐                    ⇒⟨ (((A ⊗₀ C) ⊕₀ (A ⊗₀ D)) ⊕₀ (B ⊗₀ C)) ⊕₀ (B ⊗₀ D) ⟩
        ⊕α⇒ ⊕₁ C.id           ⇒⟨ ((A ⊗₀ C) ⊕₀ ((A ⊗₀ D) ⊕₀ (B ⊗₀ C))) ⊕₀ (B ⊗₀ D) ⟩
        (C.id ⊕₁ B⊕) ⊕₁ C.id  ⇒⟨ ((A ⊗₀ C) ⊕₀ ((B ⊗₀ C) ⊕₀ (A ⊗₀ D))) ⊕₀ (B ⊗₀ D) ⟩
        ⊕α⇐ ⊕₁ C.id
      ≈
        dl.from                ⇒⟨ ((A ⊕₀ B) ⊗₀ C) ⊕₀ ((A ⊕₀ B) ⊗₀ D) ⟩
        dr.from ⊕₁ dr.from     ⇒⟨ ((A ⊗₀ C) ⊕₀ (B ⊗₀ C)) ⊕₀ ((A ⊗₀ D) ⊕₀ (B ⊗₀ D))  ⟩
        ⊕α⇐
      ⟩
    laplazaX : [ 0C ⊗₀ 0C ⇒ 0C ]⟨ λ* ≈ ρ* ⟩
    laplazaXI : ∀ {A B} →
      [ 0C ⊗₀ (A ⊕₀ B) ⇒ 0C ]⟨
        dl.from   ⇒⟨ (0C ⊗₀ A) ⊕₀ (0C ⊗₀ B) ⟩
        λ* ⊕₁ λ*  ⇒⟨ 0C ⊕₀ 0C ⟩
        ⊕λ⇒
      ≈
        λ*
      ⟩
    laplazaXIII : [ 0C ⊗₀ 1C ⇒ 0C ]⟨ ⊗ρ⇒ ≈ λ* ⟩
    laplazaXV : ∀ {A : Obj} →
      [ A ⊗₀ 0C ⇒ 0C ]⟨
        ρ*
      ≈
        B⊗ ⇒⟨ 0C ⊗₀ A ⟩
        λ*
      ⟩
    laplazaXVI : ∀ {A B} → [ 0C ⊗₀ (A ⊗₀ B) ⇒ 0C ]⟨
        ⊗α⇐        ⇒⟨ (0C ⊗₀ A) ⊗₀ B ⟩
        λ* ⊗₁ C.id  ⇒⟨ 0C ⊗₀ B ⟩
        λ*
      ≈
        λ*
      ⟩
    laplazaXVII : ∀ {A B} → [ A ⊗₀ (0C ⊗₀ B) ⇒ 0C ]⟨
        ⊗α⇐        ⇒⟨ (A ⊗₀ 0C) ⊗₀ B ⟩
        ρ* ⊗₁ C.id ⇒⟨ 0C ⊗₀ B ⟩
        λ*
      ≈
        C.id ⊗₁ λ* ⇒⟨ A ⊗₀ 0C ⟩
        ρ*
      ⟩
    laplazaXIX : ∀ {A B} → [ A ⊗₀ (0C ⊕₀ B) ⇒ A ⊗₀ B ]⟨
        dl.from     ⇒⟨ (A ⊗₀ 0C) ⊕₀ (A ⊗₀ B) ⟩
        ρ* ⊕₁ C.id  ⇒⟨ 0C ⊕₀ (A ⊗₀ B) ⟩
        ⊕λ⇒
      ≈
        C.id ⊗₁ ⊕λ⇒
      ⟩
    laplazaXXIII : ∀ {A B} → [ 1C ⊗₀ (A ⊕₀ B) ⇒ (A ⊕₀ B) ]⟨
        ⊗λ⇒
      ≈
        dl.from ⇒⟨ (1C ⊗₀ A) ⊕₀ (1C ⊗₀ B) ⟩
        ⊗λ⇒ ⊕₁ ⊗λ⇒
      ⟩

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.QuotientRing where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Powerset

open import Cubical.Data.Nat
open import Cubical.Data.FinData

open import Cubical.HITs.SetQuotients using ([_]; squash/; elimProp2)
open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.Kernel
open import Cubical.Algebra.Ring
import Cubical.Algebra.Ring.QuotientRing as Ring

private
  variable
    ℓ ℓ' : Level

_/_ : (R : CommRing ℓ) → (I : IdealsIn R) → CommRing ℓ
R / I =
  fst asRing , commringstr _ _ _ _ _
                 (iscommring (RingStr.isRing (snd asRing))
                             (elimProp2 (λ _ _ → squash/ _ _)
                                        commEq))
   where
       asRing = (CommRing→Ring R) Ring./ (CommIdeal→Ideal I)
       _·/_ : fst asRing → fst asRing → fst asRing
       _·/_ = RingStr._·_ (snd asRing)
       commEq : (x y : fst R) → ([ x ] ·/ [ y ]) ≡ ([ y ] ·/ [ x ])
       commEq x y i = [ CommRingStr.·Comm (snd R) x y i ]

[_]/ : {R : CommRing ℓ} {I : IdealsIn R} → (a : fst R) → fst (R / I)
[ a ]/ = [ a ]

module Quotient-FGideal-CommRing-Ring
  (A : CommRing ℓ)
  (B : Ring ℓ')
  (g : RingHom (CommRing→Ring A) B)
  {n : ℕ}
  (v : FinVec ⟨ A ⟩ n)
  (gnull : (k : Fin n) → g $ v k ≡ RingStr.0r (snd B))
  where

  open RingStr (snd B) using (0r)

  zeroOnGeneratedIdeal : (x : ⟨ A ⟩) → x ∈ fst (generatedIdeal A v) → g $ x ≡ 0r
  zeroOnGeneratedIdeal x x∈FGIdeal =
    PT.elim
      (λ _ → isSetRing B (g $ x) 0r)
      (λ {(α , isLC) → subst _ (sym isLC) (cancelLinearCombination A B g _ α v gnull)})
      x∈FGIdeal

  inducedHom : RingHom (CommRing→Ring (A / (generatedIdeal _ v))) B
  inducedHom = Ring.UniversalProperty.inducedHom (CommRing→Ring A) (CommIdeal→Ideal ideal) g zeroOnGeneratedIdeal
    where ideal = generatedIdeal A v

module Quotient-FGideal-CommRing-CommRing
  (A : CommRing ℓ)
  (B : CommRing ℓ')
  (g : CommRingHom A B)
  {n : ℕ}
  (v : FinVec ⟨ A ⟩ n)
  (gnull : (k : Fin n) → g $ v k ≡ CommRingStr.0r (snd B))
  where

  inducedHom : CommRingHom (A / (generatedIdeal _ v)) B
  inducedHom = Quotient-FGideal-CommRing-Ring.inducedHom A (CommRing→Ring B) g v gnull

quotientHom : (R : CommRing ℓ) → (I : IdealsIn R) → CommRingHom R (R / I)
quotientHom R I = Ring.quotientHom (CommRing→Ring R) (CommIdeal→Ideal I)

module _ {R : CommRing ℓ} (I : IdealsIn R) where
  private
    π = quotientHom R I

  kernel≡I : kernelIdeal R (R / I) π ≡ I
  kernel≡I = cong Ideal→CommIdeal (Ring.kernel≡I (CommIdeal→Ideal I))

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 Data.Binary.Increment where

open import Data.Binary.Definition
open import Strict

inc : 𝔹 → 𝔹
inc 0ᵇ      = 1ᵇ 0ᵇ
inc (1ᵇ xs) = 2ᵇ xs
inc (2ᵇ xs) = 1ᵇ inc xs

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Agda.Builtin.Strict where

open import Agda.Builtin.Equality

primitive
  primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
  primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of binary relations to sigma types
------------------------------------------------------------------------

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

module Data.Product.Relation.Binary.Pointwise.Dependent where

open import Data.Product as Prod
open import Level
open import Function
open import Relation.Binary as B
  using (_⇒_; Setoid; IsEquivalence)
open import Relation.Binary.Indexed.Heterogeneous as I
  using (IREL; IRel; IndexedSetoid; IsIndexedEquivalence)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Pointwise lifting

infixr 4 _,_

record POINTWISE {a₁ a₂ b₁ b₂ ℓ₁ ℓ₂}
                 {A₁ : Set a₁} (B₁ : A₁ → Set b₁)
                 {A₂ : Set a₂} (B₂ : A₂ → Set b₂)
                 (_R₁_ : B.REL A₁ A₂ ℓ₁) (_R₂_ : IREL B₁ B₂ ℓ₂)
                 (xy₁ : Σ A₁ B₁) (xy₂ : Σ A₂ B₂)
                 : Set (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂ ⊔ ℓ₁ ⊔ ℓ₂) where
  constructor _,_
  field
    proj₁ : (proj₁ xy₁) R₁ (proj₁ xy₂)
    proj₂ : (proj₂ xy₁) R₂ (proj₂ xy₂)

open POINTWISE public

Pointwise : ∀ {a b ℓ₁ ℓ₂} {A : Set a} (B : A → Set b)
            (_R₁_ : B.Rel A ℓ₁) (_R₂_ : IRel B ℓ₂) → B.Rel (Σ A B) _
Pointwise B = POINTWISE B B

------------------------------------------------------------------------
-- Pointwise preserves many relational properties

module _ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b}
         {R : B.Rel A ℓ₁} {S : IRel B ℓ₂} where

  private
    R×S = Pointwise B R S

  refl : B.Reflexive R → I.Reflexive B S → B.Reflexive R×S
  refl refl₁ refl₂ = (refl₁ , refl₂)

  symmetric : B.Symmetric R → I.Symmetric B S → B.Symmetric R×S
  symmetric sym₁ sym₂ (x₁Rx₂ , y₁Ry₂) = (sym₁ x₁Rx₂ , sym₂ y₁Ry₂)

  transitive : B.Transitive R → I.Transitive B S → B.Transitive R×S
  transitive trans₁ trans₂ (x₁Rx₂ , y₁Ry₂) (x₂Rx₃ , y₂Ry₃) =
    (trans₁ x₁Rx₂ x₂Rx₃ , trans₂ y₁Ry₂ y₂Ry₃)

  isEquivalence : IsEquivalence R → IsIndexedEquivalence B S →
                  IsEquivalence R×S
  isEquivalence eq₁ eq₂ = record
    { refl  = refl       Eq.refl  IEq.refl
    ; sym   = symmetric  Eq.sym   IEq.sym
    ; trans = transitive Eq.trans IEq.trans
    } where
    module Eq = IsEquivalence eq₁
    module IEq = IsIndexedEquivalence eq₂

module _ {a b ℓ₁ ℓ₂} where

  setoid : (A : Setoid a ℓ₁) →
           IndexedSetoid (Setoid.Carrier A) b ℓ₂ →
           Setoid _ _
  setoid s₁ s₂ = record
    { isEquivalence = isEquivalence Eq.isEquivalence IEq.isEquivalence
    } where
    module Eq = Setoid s₁
    module IEq = IndexedSetoid s₂

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

Rel = Pointwise
{-# WARNING_ON_USAGE Rel
"Warning: Rel was deprecated in v0.15.
Please use Pointwise instead."
#-}

-- Version 0.15

REL = POINTWISE
{-# WARNING_ON_USAGE REL
"Warning: REL was deprecated in v1.0.
Please use POINTWISE instead."
#-}


text:
open import Mockingbird.Forest using (Forest)

module Mockingbird.Forest.Extensionality {b ℓ} (forest : Forest {b} {ℓ}) where

open import Algebra using (RightCongruent)
open import Relation.Binary using (Rel; IsEquivalence; Setoid)
open import Level using (_⊔_)

open Forest forest

-- TODO: if the arguments to the predicates is{Mockingbird,Thrush,Cardinal,...}
-- are made implicit, then x can be implicit too.
Similar : Rel Bird (b ⊔ ℓ)
Similar A₁ A₂ = ∀ x → A₁ ∙ x ≈ A₂ ∙ x

infix 4 _≋_
_≋_ = Similar

-- A forest is called extensional if similarity implies equality.
IsExtensional : Set (b ⊔ ℓ)
IsExtensional = ∀ {A₁ A₂} → A₁ ≋ A₂ → A₁ ≈ A₂

-- A record to be used as an instance argument.
record Extensional : Set (b ⊔ ℓ) where
  field
    ext : IsExtensional

open Extensional ⦃ ... ⦄ public

ext′ : ⦃ _ : Extensional ⦄ → ∀ {A₁ A₂} → (∀ {x} → A₁ ∙ x ≈ A₂ ∙ x) → A₁ ≈ A₂
ext′ A₁≋A₂ = ext λ _ → A₁≋A₂

-- Similarity is an equivalence relation.
≋-isEquivalence : IsEquivalence _≋_
≋-isEquivalence = record
  { refl = λ _ → refl
  ; sym = λ x≋y z → sym (x≋y z)
  ; trans = λ x≋y y≋z w → trans (x≋y w) (y≋z w)
  }

≋-congʳ : RightCongruent _≋_ _∙_
≋-congʳ {w} {x} {y} x≋y = λ _ → congʳ (x≋y w)

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
-- 2012-02-13 Andreas: testing correct polarity of data types
-- sized types are the only source of subtyping, I think...
-- {-# OPTIONS -v tc.polarity.set:10 #-}
-- {-# OPTIONS -v tc.size.solve:20 #-}

{-# OPTIONS --show-implicit #-}
{-# OPTIONS --sized-types #-}
module DataPolarity where

open import Common.Size

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {↑ size}
  suc  : {size : Size} -> Nat {size} -> Nat {↑ size}

data Pair (A : Set) : Set where
  _,_ : A -> A -> Pair A

split : {i : Size} → Nat {i} → Pair (Nat {i})
split zero = zero , zero
split (suc n) with split n
... | (l , r) = suc r , l
-- this should work, due to the monotonicity of Pair
-- without subtyping, Agda would complain about i != ↑ i

MyPair : Nat → Set → Set
MyPair zero A = Pair A
MyPair (suc n) A = MyPair n A
-- polarity should be preserved by functions

mysplit : {i : Size} → (n : Nat {i}) → MyPair (suc zero) (Nat {i})
mysplit zero = zero , zero
mysplit (suc n) with mysplit n
... | (l , r) = suc r , l

-- it should also work in modules

module M (s : Set1) where

  data P (A : Set) : Set where
    _,_ : A -> A -> P A

  sp : {i : Size} → (n : Nat {i}) → P (Nat {i})
  sp zero = zero , zero
  sp (suc n) with sp n
  ... | (l , r) = suc r , l

-- open import Common.Prelude

postulate A : Set

data Color : Set where
  red   : Color
  black : Color

data Bounds : Set where
  leftOf : Bounds → Bounds
  rightOf : Bounds → Bounds

-- works not:
data Tree' (β : Bounds) : {i : Size} -> Color → (Nat {∞}) → Set where
  lf : ∀ {i} → Tree' β {↑ i} black zero
  nr : ∀ {i n}(a : A) -- →  .(a is β)
     → Tree' (leftOf  β) {i} black n
     → Tree' (rightOf β) {i} black n
     → Tree' β {↑ i} red n
  nb : ∀ {i c n}(a : A) -- → .(a is β)
     → Tree' (leftOf β) {i} c n
     → Tree' (rightOf β) {i} black n
     → Tree' β {↑ i} black (suc n)

-- works:
data Tr (A : Set) : {i : Size} -> Color → Set where
  lf : ∀ {i} → Tr A {↑ i} black
  nr : ∀ {i}(a : A)
     → Tr A {i} black → Tr A {i} black
     → Tr A {↑ i} red
  nb : ∀ {i c}(a : A)
     → Tr A {i} c → Tr A {i} black
     → Tr A {↑ i} black

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import lib.Basics
open import lib.types.Bool
open import lib.types.FunctionSeq
open import lib.types.Pointed
open import lib.types.Suspension.Core
open import lib.types.Suspension.Iterated
open import lib.types.Suspension.Trunc
open import lib.types.TLevel
open import lib.types.Truncation

module lib.types.Suspension.IteratedTrunc where

module _ {i} (A : Type i) (m : ℕ₋₂) where

  Susp^-Trunc-swap : ∀ (n : ℕ)
    → Susp^ n (Trunc m A)
    → Trunc (⟨ n ⟩₋₂ +2+ m) (Susp^ n A)
  Susp^-Trunc-swap O = idf _
  Susp^-Trunc-swap (S n) =
    Susp-Trunc-swap (Susp^ n A) (⟨ n ⟩₋₂ +2+ m) ∘
    Susp-fmap (Susp^-Trunc-swap n)

  private
    to : ∀ n → Trunc (⟨ n ⟩₋₂ +2+ m) (Susp^ n (Trunc m A)) → Trunc (⟨ n ⟩₋₂ +2+ m) (Susp^ n A)
    to n = Trunc-rec {{Trunc-level}} (Susp^-Trunc-swap n)

    from : ∀ n → Trunc (⟨ n ⟩₋₂ +2+ m) (Susp^ n A) → Trunc (⟨ n ⟩₋₂ +2+ m) (Susp^ n (Trunc m A))
    from n = Trunc-fmap (Susp^-fmap n [_])

    abstract
      from-Susp^-Trunc-swap : ∀ n → from n ∘ Susp^-Trunc-swap n ∼ [_]
      from-Susp^-Trunc-swap O =
        Trunc-elim
          {P = λ s → from 0 (Susp^-Trunc-swap 0 s) == [ s ]}
          {{λ s → =-preserves-level Trunc-level}}
          (λ a → idp)
      from-Susp^-Trunc-swap (S n) x =
        (from (S n) $
         Susp-Trunc-swap (Susp^ n A) (⟨ n ⟩₋₂ +2+ m) $
         Susp-fmap (Susp^-Trunc-swap n) x)
          =⟨ ! $ Susp-Trunc-swap-natural (Susp^-fmap n [_]) (⟨ n ⟩₋₂ +2+ m) $
             Susp-fmap (Susp^-Trunc-swap n) x ⟩
        (Susp-Trunc-swap (Susp^ n (Trunc m A)) (⟨ n ⟩₋₂ +2+ m) $
         Susp-fmap (Trunc-fmap (Susp^-fmap n [_])) $
         Susp-fmap (Susp^-Trunc-swap n) x)
          =⟨ ap (Susp-Trunc-swap (Susp^ n (Trunc m A)) (⟨ n ⟩₋₂ +2+ m)) $
             ! $ Susp-fmap-∘ (Trunc-fmap (Susp^-fmap n [_])) (Susp^-Trunc-swap n) x ⟩
        (Susp-Trunc-swap (Susp^ n (Trunc m A)) (⟨ n ⟩₋₂ +2+ m) $
         Susp-fmap (from n ∘ Susp^-Trunc-swap n) x)
          =⟨ ap (Susp-Trunc-swap (Susp^ n (Trunc m A)) (⟨ n ⟩₋₂ +2+ m)) $
             ap (λ f → Susp-fmap f x) (λ= (from-Susp^-Trunc-swap n)) ⟩
        Susp-Trunc-swap (Susp^ n (Trunc m A)) (⟨ n ⟩₋₂ +2+ m) (Susp-fmap [_] x)
          =⟨ Susp-Trunc-swap-Susp-fmap-trunc (Susp^ n (Trunc m A)) (⟨ n ⟩₋₂ +2+ m) x ⟩
        [ x ] =∎

      from-to : ∀ n → from n ∘ to n ∼ idf _
      from-to n =
        Trunc-elim
          {P = λ t → from n (to n t) == t}
          {{λ t → =-preserves-level Trunc-level}}
          (from-Susp^-Trunc-swap n)

      Susp^-Trunc-swap-Susp^-fmap-trunc : ∀ n →
        Susp^-Trunc-swap n ∘ Susp^-fmap n [_] ∼ [_]
      Susp^-Trunc-swap-Susp^-fmap-trunc 0 s = idp
      Susp^-Trunc-swap-Susp^-fmap-trunc (S n) s =
        (Susp-Trunc-swap (Susp^ n A) (⟨ n ⟩₋₂ +2+ m) $
         Susp-fmap (Susp^-Trunc-swap n) $
         Susp^-fmap (S n) [_] s)
          =⟨ ap (Susp-Trunc-swap (Susp^ n A) (⟨ n ⟩₋₂ +2+ m)) $
             ! $ Susp-fmap-∘ (Susp^-Trunc-swap n) (Susp^-fmap n [_]) s ⟩
        (Susp-Trunc-swap (Susp^ n A) (⟨ n ⟩₋₂ +2+ m) $
         Susp-fmap (Susp^-Trunc-swap n ∘ Susp^-fmap n [_]) s)
          =⟨ ap (Susp-Trunc-swap (Susp^ n A) (⟨ n ⟩₋₂ +2+ m)) $
             app= (ap Susp-fmap (λ= (Susp^-Trunc-swap-Susp^-fmap-trunc n))) s ⟩
        Susp-Trunc-swap (Susp^ n A) (⟨ n ⟩₋₂ +2+ m) (Susp-fmap [_] s)
          =⟨ Susp-Trunc-swap-Susp-fmap-trunc (Susp^ n A) (⟨ n ⟩₋₂ +2+ m) s ⟩
        [ s ] =∎

      to-from : ∀ n → to n ∘ from n ∼ idf _
      to-from n = Trunc-elim {{λ t → =-preserves-level Trunc-level}}
                             (Susp^-Trunc-swap-Susp^-fmap-trunc n)

  Susp^-Trunc-equiv : ∀ (n : ℕ)
    → Trunc (⟨ n ⟩₋₂ +2+ m) (Susp^ n (Trunc m A)) ≃ Trunc (⟨ n ⟩₋₂ +2+ m) (Susp^ n A)
  Susp^-Trunc-equiv n = equiv (to n) (from n) (to-from n) (from-to n)

module _ {i} (X : Ptd i) (m : ℕ₋₂) where

  Susp^-Trunc-swap-pt : ∀ (n : ℕ)
    → Susp^-Trunc-swap (de⊙ X) m n (pt (⊙Susp^ n (⊙Trunc m X))) ==
      pt (⊙Trunc (⟨ n ⟩₋₂ +2+ m) (⊙Susp^ n X))
  Susp^-Trunc-swap-pt O = idp
  Susp^-Trunc-swap-pt (S n) = idp

  ⊙Susp^-Trunc-swap : ∀ (n : ℕ)
    → ⊙Susp^ n (⊙Trunc m X) ⊙→ ⊙Trunc (⟨ n ⟩₋₂ +2+ m) (⊙Susp^ n X)
  ⊙Susp^-Trunc-swap n = Susp^-Trunc-swap (de⊙ X) m n , Susp^-Trunc-swap-pt n

  ⊙Susp^-⊙Trunc-equiv : ∀ (n : ℕ)
    → ⊙Trunc (⟨ n ⟩₋₂ +2+ m) (⊙Susp^ n (⊙Trunc m X)) ⊙≃ ⊙Trunc (⟨ n ⟩₋₂ +2+ m) (⊙Susp^ n X)
  ⊙Susp^-⊙Trunc-equiv n =
    ⊙to , snd (Susp^-Trunc-equiv (de⊙ X) m n)
    where
    ⊙to : ⊙Trunc (⟨ n ⟩₋₂ +2+ m) (⊙Susp^ n (⊙Trunc m X))
       ⊙→ ⊙Trunc (⟨ n ⟩₋₂ +2+ m) (⊙Susp^ n X)
    ⊙to = ⊙Trunc-rec {{Trunc-level}} (⊙Susp^-Trunc-swap n)

module _ {i} {X Y : Ptd i} (f : X ⊙→ Y) (m : ℕ₋₂) where

  ⊙Susp^-Trunc-swap-natural : ∀ (n : ℕ)
    → ⊙Susp^-Trunc-swap Y m n ◃⊙∘
      ⊙Susp^-fmap n (⊙Trunc-fmap f) ◃⊙idf
      =⊙∘
      ⊙Trunc-fmap (⊙Susp^-fmap n f) ◃⊙∘
      ⊙Susp^-Trunc-swap X m n ◃⊙idf
  ⊙Susp^-Trunc-swap-natural O = =⊙∘-in (⊙λ= (⊙∘-unit-l _))
  ⊙Susp^-Trunc-swap-natural (S n) =
    ⊙Susp^-Trunc-swap Y m (S n) ◃⊙∘
    ⊙Susp^-fmap (S n) (⊙Trunc-fmap f) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙expand $
           ⊙Susp-Trunc-swap (Susp^ n (de⊙ Y)) (⟨ n ⟩₋₂ +2+ m) ◃⊙∘
           ⊙Susp-fmap (Susp^-Trunc-swap (de⊙ Y) m n) ◃⊙idf ⟩
    ⊙Susp-Trunc-swap (Susp^ n (de⊙ Y)) (⟨ n ⟩₋₂ +2+ m) ◃⊙∘
    ⊙Susp-fmap (Susp^-Trunc-swap (de⊙ Y) m n) ◃⊙∘
    ⊙Susp^-fmap (S n) (⊙Trunc-fmap f) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙Susp-fmap-seq-=⊙∘ $
           de⊙-seq-=⊙∘ $ ⊙Susp^-Trunc-swap-natural n ⟩
    ⊙Susp-Trunc-swap (Susp^ n (de⊙ Y)) (⟨ n ⟩₋₂ +2+ m) ◃⊙∘
    ⊙Susp-fmap (Trunc-fmap (Susp^-fmap n (fst f))) ◃⊙∘
    ⊙Susp-fmap (Susp^-Trunc-swap (de⊙ X) m n) ◃⊙idf
      =⊙∘⟨ 0 & 2 & =⊙∘-in
           {gs = ⊙Trunc-fmap (⊙Susp-fmap (Susp^-fmap n (fst f))) ◃⊙∘
                 ⊙Susp-Trunc-swap (Susp^ n (de⊙ X)) (⟨ n ⟩₋₂ +2+ m) ◃⊙idf} $
           ⊙Susp-Trunc-swap-natural (Susp^-fmap n (fst f)) (⟨ n ⟩₋₂ +2+ m) ⟩
    ⊙Trunc-fmap (⊙Susp-fmap (Susp^-fmap n (fst f))) ◃⊙∘
    ⊙Susp-Trunc-swap (Susp^ n (de⊙ X)) (⟨ n ⟩₋₂ +2+ m) ◃⊙∘
    ⊙Susp-fmap (Susp^-Trunc-swap (de⊙ X) m n) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙contract ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap (S n) f) ◃⊙∘
    ⊙Susp^-Trunc-swap X m (S n) ◃⊙idf ∎⊙∘

  ⊙Susp^-⊙Trunc-equiv-natural : ∀ (n : ℕ)
    → ⊙–> (⊙Susp^-⊙Trunc-equiv Y m n) ◃⊙∘
      ⊙Trunc-fmap (⊙Susp^-fmap n (⊙Trunc-fmap f)) ◃⊙idf
      =⊙∘
      ⊙Trunc-fmap (⊙Susp^-fmap n f) ◃⊙∘
      ⊙–> (⊙Susp^-⊙Trunc-equiv X m n) ◃⊙idf
  ⊙Susp^-⊙Trunc-equiv-natural n = =⊙∘-in $
    ⊙–> (⊙Susp^-⊙Trunc-equiv Y m n) ⊙∘
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙Trunc-fmap f))
      =⟨ ⊙Trunc-rec-⊙Trunc-fmap {{Trunc-level}}
           (⊙Susp^-Trunc-swap Y m n)
           (⊙Susp^-fmap n (⊙Trunc-fmap f)) ⟩
    ⊙Trunc-rec {{Trunc-level}} (⊙Susp^-Trunc-swap Y m n ⊙∘ ⊙Susp^-fmap n (⊙Trunc-fmap f))
      =⟨ ap (⊙Trunc-rec {{Trunc-level}}) $
         =⊙∘-out $ ⊙Susp^-Trunc-swap-natural n ⟩
    ⊙Trunc-rec {{Trunc-level}} (⊙Trunc-fmap (⊙Susp^-fmap n f) ⊙∘ ⊙Susp^-Trunc-swap X m n)
      =⟨ ⊙Trunc-rec-post-⊙∘ {{Trunc-level}} {{Trunc-level}}
           (⊙Trunc-fmap (⊙Susp^-fmap n f))
           (⊙Susp^-Trunc-swap X m n) ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap n f) ⊙∘ ⊙–> (⊙Susp^-⊙Trunc-equiv X m n) =∎

  ⊙Susp^-⊙Trunc-equiv-natural' : ∀ (n : ℕ)
    → ⊙<– (⊙Susp^-⊙Trunc-equiv Y m n) ◃⊙∘
      ⊙Trunc-fmap (⊙Susp^-fmap n f) ◃⊙idf
      =⊙∘
      ⊙Trunc-fmap (⊙Susp^-fmap n (⊙Trunc-fmap f)) ◃⊙∘
      ⊙<– (⊙Susp^-⊙Trunc-equiv X m n) ◃⊙idf
  ⊙Susp^-⊙Trunc-equiv-natural' n =
    ⊙<– (⊙Susp^-⊙Trunc-equiv Y m n) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-fmap n f) ◃⊙idf
      =⊙∘⟨ 2 & 0 & !⊙∘ $ ⊙<–-inv-r-=⊙∘ (⊙Susp^-⊙Trunc-equiv X m n) ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv Y m n) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-fmap n f) ◃⊙∘
    ⊙–> (⊙Susp^-⊙Trunc-equiv X m n) ◃⊙∘
    ⊙<– (⊙Susp^-⊙Trunc-equiv X m n) ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ $ ⊙Susp^-⊙Trunc-equiv-natural n ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv Y m n) ◃⊙∘
    ⊙–> (⊙Susp^-⊙Trunc-equiv Y m n) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙Trunc-fmap f)) ◃⊙∘
    ⊙<– (⊙Susp^-⊙Trunc-equiv X m n) ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙<–-inv-l-=⊙∘ (⊙Susp^-⊙Trunc-equiv Y m n) ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙Trunc-fmap f)) ◃⊙∘
    ⊙<– (⊙Susp^-⊙Trunc-equiv X m n) ◃⊙idf ∎⊙∘

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --no-sized-types --no-guardedness #-}
module Agda.Builtin.TrustMe where

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Erase

private
  postulate
    unsafePrimTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y

primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
primTrustMe = primEraseEquality unsafePrimTrustMe

{-# DISPLAY primEraseEquality unsafePrimTrustMe = primTrustMe #-}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Data.NatPlusOne.MoreNats.AssocNat.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Nat
open import Cubical.Data.NatPlusOne.MoreNats.AssocNat.Base
open import Cubical.Data.NatPlusOne renaming (ℕ₊₁ to Nat; one to one'; _+₁_ to _+₁'_)

Nat→ℕ₊₁ : Nat → ℕ₊₁
Nat→ℕ₊₁ one' = 1
Nat→ℕ₊₁ (2+ n) = 1 +₁ Nat→ℕ₊₁ (1+ n)

ℕ₊₁→Nat : ℕ₊₁ → Nat
ℕ₊₁→Nat one = 1
ℕ₊₁→Nat (a +₁ b) = ℕ₊₁→Nat a +₁' ℕ₊₁→Nat b
ℕ₊₁→Nat (assoc a b c i) = +₁-assoc (ℕ₊₁→Nat a) (ℕ₊₁→Nat b) (ℕ₊₁→Nat c) i
ℕ₊₁→Nat (trunc m n p q i j) =
  1+ (isSetℕ _ _ (λ k → -1+ (ℕ₊₁→Nat (p k))) (λ k → -1+ (ℕ₊₁→Nat (q k))) i j)

ℕ₊₁→Nat→ℕ₊₁ : ∀ n → ℕ₊₁→Nat (Nat→ℕ₊₁ n) ≡ n
ℕ₊₁→Nat→ℕ₊₁ one' = refl
ℕ₊₁→Nat→ℕ₊₁ (2+ n) = cong (1+_ ∘ suc ∘ -1+_) (ℕ₊₁→Nat→ℕ₊₁ (1+ n))

private
  Nat→ℕ₊₁-+ : ∀ a b → Nat→ℕ₊₁ (a +₁' b) ≡ Nat→ℕ₊₁ a +₁ Nat→ℕ₊₁ b
  Nat→ℕ₊₁-+ one' b = refl
  Nat→ℕ₊₁-+ (2+ a) b = cong (one +₁_) (Nat→ℕ₊₁-+ (1+ a) b)
    ∙ assoc one (Nat→ℕ₊₁ (1+ a)) (Nat→ℕ₊₁ b)

Nat→ℕ₊₁→Nat : ∀ n → Nat→ℕ₊₁ (ℕ₊₁→Nat n) ≡ n
Nat→ℕ₊₁→Nat = ElimProp.f (trunc _ _) (λ i → one)
  λ {a} {b} m n → Nat→ℕ₊₁-+ (ℕ₊₁→Nat a) (ℕ₊₁→Nat b) ∙ (λ i → m i +₁ n i)

ℕ₊₁≡Nat : ℕ₊₁ ≡ Nat
ℕ₊₁≡Nat = isoToPath (iso ℕ₊₁→Nat Nat→ℕ₊₁ ℕ₊₁→Nat→ℕ₊₁ Nat→ℕ₊₁→Nat)


text:
module UnsolvedMetas where

foo = ?


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use Data.List.Relation.Unary.Any
-- directly.
------------------------------------------------------------------------

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

module Data.List.Any where

open import Data.List.Relation.Unary.Any public


text:
module TypeTheory.Nat.AnotherMono.Structure where

open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Empty using (⊥)
open import Data.Product using (Σ; _×_; _,_)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_)

record Nat : Set₁ where
  field
    N        : Set
    zero     : N
    suc      : N → N
    ind      : (P : N → Set) → P zero → (∀ k → P k → P (suc k)) → ∀ n → P n
    ind-zero : ∀ P P-zero P-suc → ind P P-zero P-suc zero ≡ P-zero
    ind-suc  : ∀ P P-zero P-suc n → ind P P-zero P-suc (suc n) ≡
                                    P-suc n (ind P P-zero P-suc n)
    s≢z      : ∀ {n} → suc n ≢ zero

  0N : N
  0N = zero

  1N : N
  1N = suc zero

  z≢s : ∀ {n} → zero ≢ suc n
  z≢s = ≢-sym s≢z

  rec : {A : Set} → A → (A → A) → N → A
  rec {A} z s = ind (λ _ → A) z (λ _ → s)

  rec-zero : ∀ {A} (z : A) s → rec z s zero ≡ z
  rec-zero z s = ind-zero _ _ _

  rec-suc : ∀ {A} (z : A) s n → rec z s (suc n) ≡ s (rec z s n)
  rec-suc z s n = ind-suc _ _ _ _

  infixl 6 _+_
  infixl 7 _*_
  infix 4 _≤_ _<_ _≥_ _>_ _≰_

  -- Arithematic
  -- Addition
  _+_ : N → N → N
  m + n = rec n suc m

  -- Multiplication
  _*_ : N → N → N
  m * n = rec zero (n +_) m

  -- Order
  _≤_ : Rel N lzero
  m ≤ n = Σ N λ o → o + m ≡ n

  _<_ : Rel N lzero
  m < n = suc m ≤ n

  _≥_ : Rel N lzero
  m ≥ n = n ≤ m

  _>_ : Rel N lzero
  m > n = n < m

  _≰_ : Rel N lzero
  m ≰ n = ¬ m ≤ n

  _≮_ : Rel N lzero
  m ≮ n = ¬ m < n

  _≱_ : Rel N lzero
  m ≱ n = ¬ m ≥ n

  _≯_ : Rel N lzero
  m ≯ n = ¬ m > n


text:
module Main where

import univ
import cwf
import help
import proofs


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Unary relations
------------------------------------------------------------------------

module Relation.Unary where

open import Data.Empty
open import Function
open import Data.Unit hiding (setoid)
open import Data.Product
open import Data.Sum
open import Level
open import Relation.Nullary
open import Relation.Binary using (Setoid; IsEquivalence)

------------------------------------------------------------------------
-- Unary relations

Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Pred A ℓ = A → Set ℓ

------------------------------------------------------------------------
-- Unary relations can be seen as sets

-- I.e., they can be seen as subsets of the universe of discourse.

module _ {a} {A : Set a} -- The universe of discourse.
         where

  -- Set membership.

  infix 4 _∈_ _∉_

  _∈_ : ∀ {ℓ} → A → Pred A ℓ → Set _
  x ∈ P = P x

  _∉_ : ∀ {ℓ} → A → Pred A ℓ → Set _
  x ∉ P = ¬ x ∈ P

  -- The empty set.

  ∅ : Pred A zero
  ∅ = λ _ → ⊥

  -- The property of being empty.

  Empty : ∀ {ℓ} → Pred A ℓ → Set _
  Empty P = ∀ x → x ∉ P

  ∅-Empty : Empty ∅
  ∅-Empty x ()

  -- The universe, i.e. the subset containing all elements in A.

  U : Pred A zero
  U = λ _ → ⊤

  -- The property of being universal.

  Universal : ∀ {ℓ} → Pred A ℓ → Set _
  Universal P = ∀ x → x ∈ P

  U-Universal : Universal U
  U-Universal = λ _ → _

  -- Set complement.

  ∁ : ∀ {ℓ} → Pred A ℓ → Pred A ℓ
  ∁ P = λ x → x ∉ P

  ∁∅-Universal : Universal (∁ ∅)
  ∁∅-Universal = λ x x∈∅ → x∈∅

  ∁U-Empty : Empty (∁ U)
  ∁U-Empty = λ x x∈∁U → x∈∁U _

  -- P ⊆ Q means that P is a subset of Q. _⊆′_ is a variant of _⊆_.

  infix 4 _⊆_ _⊇_ _⊆′_ _⊇′_

  _⊆_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

  _⊆′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊆′ Q = ∀ x → x ∈ P → x ∈ Q

  _⊇_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  Q ⊇ P = P ⊆ Q

  _⊇′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  Q ⊇′ P = P ⊆′ Q

  ∅-⊆ : ∀ {ℓ} → (P : Pred A ℓ) → ∅ ⊆ P
  ∅-⊆ P ()

  ⊆-U : ∀ {ℓ} → (P : Pred A ℓ) → P ⊆ U
  ⊆-U P _ = _

  -- Positive version of non-disjointness, dual to inclusion.

  infix 4 _≬_

  _≬_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ≬ Q = ∃ λ x → x ∈ P × x ∈ Q

  -- Set union.

  infixr 6 _∪_

  _∪_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
  P ∪ Q = λ x → x ∈ P ⊎ x ∈ Q

  -- Set intersection.

  infixr 7 _∩_

  _∩_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
  P ∩ Q = λ x → x ∈ P × x ∈ Q

  -- Implication.

  infixl 8 _⇒_

  _⇒_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
  P ⇒ Q = λ x → x ∈ P → x ∈ Q

  -- Infinitary union and intersection.

  infix 9 ⋃ ⋂

  ⋃ : ∀ {ℓ i} (I : Set i) → (I → Pred A ℓ) → Pred A _
  ⋃ I P = λ x → Σ[ i ∈ I ] P i x

  syntax ⋃ I (λ i → P) = ⋃[ i ∶ I ] P

  ⋂ : ∀ {ℓ i} (I : Set i) → (I → Pred A ℓ) → Pred A _
  ⋂ I P = λ x → (i : I) → P i x

  syntax ⋂ I (λ i → P) = ⋂[ i ∶ I ] P

------------------------------------------------------------------------
-- Unary relation combinators

infixr 2 _⟨×⟩_
infixr 2 _⟨⊙⟩_
infixr 1 _⟨⊎⟩_
infixr 0 _⟨→⟩_
infixl 9 _⟨·⟩_
infixr 9 _⟨∘⟩_
infixr 2 _//_ _\\_

_⟨×⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
        Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨×⟩ Q) (x , y) = x ∈ P × y ∈ Q

_⟨⊙⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
        Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨⊙⟩ Q) (x , y) = x ∈ P ⊎ y ∈ Q

_⟨⊎⟩_ : ∀ {a b ℓ} {A : Set a} {B : Set b} →
        Pred A ℓ → Pred B ℓ → Pred (A ⊎ B) _
P ⟨⊎⟩ Q = [ P , Q ]

_⟨→⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
        Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
(P ⟨→⟩ Q) f = P ⊆ Q ∘ f

_⟨·⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
        (P : Pred A ℓ₁) (Q : Pred B ℓ₂) →
        (P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ Q ∘ uncurry (flip _$_)
(P ⟨·⟩ Q) (p , f) = f p

-- Converse.

_~ : ∀ {a b ℓ} {A : Set a} {B : Set b} →
     Pred (A × B) ℓ → Pred (B × A) ℓ
P ~ = P ∘ swap

-- Composition.

_⟨∘⟩_ : ∀ {a b c ℓ₁ ℓ₂} {A : Set a} {B : Set b} {C : Set c} →
        Pred (A × B) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × C) _
(P ⟨∘⟩ Q) (x , z) = ∃ λ y → (x , y) ∈ P × (y , z) ∈ Q

-- Post and pre-division.

_//_ : ∀ {a b c ℓ₁ ℓ₂} {A : Set a} {B : Set b} {C : Set c} →
       Pred (A × C) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × B) _
(P // Q) (x , y) = Q ∘ _,_ y ⊆ P ∘ _,_ x

_\\_ : ∀ {a b c ℓ₁ ℓ₂} {A : Set a} {B : Set b} {C : Set c} →
       Pred (A × C) ℓ₁ → Pred (A × B) ℓ₂ → Pred (B × C) _
P \\ Q = (P ~ // Q ~) ~

------------------------------------------------------------------------
-- Properties of unary relations

Decidable : ∀ {a ℓ} {A : Set a} (P : Pred A ℓ) → Set _
Decidable P = ∀ x → Dec (P x)