text:
-- Generic term traversals
module Syntax.Substitution.Lemmas where

open import Syntax.Types
open import Syntax.Context
open import Syntax.Terms
open import Syntax.Substitution.Kits
open import Syntax.Substitution.Instances

open import Data.Sum
open import Relation.Binary.PropositionalEquality as ≡
    using (_≡_ ; refl ; sym ; cong ; subst)
open import Function using (id ; flip ; _∘_)
open ≡.≡-Reasoning

-- | Lemmas from substitutions
-- | Concrete instances of structural and substitution lemmas
-- | can be expressed as substituting traversals on terms

-- Weakening lemma
weakening : ∀{Γ Δ A} ->     Γ ⊆ Δ   ->   Γ ⊢ A
                           --------------------
                     ->           Δ ⊢ A
weakening s = substitute (weakₛ 𝒯ermₛ s)

-- Weakening lemma for computations
weakening′ : ∀{Γ Δ A} ->     Γ ⊆ Δ   ->   Γ ⊨ A
                           --------------------
                     ->           Δ ⊨ A
weakening′ s = substitute′ (weakₛ 𝒯ermₛ s)

-- Exchange lemma
exchange : ∀ Γ Γ′ Γ″ {A B C}
                     ->   Γ ⌊ A ⌋ Γ′ ⌊ B ⌋ Γ″ ⊢ C
                         ----------------------
                     ->   Γ ⌊ B ⌋ Γ′ ⌊ A ⌋ Γ″ ⊢ C
exchange Γ Γ′ Γ″ = substitute (exₛ 𝒯ermₛ Γ Γ′ Γ″)

-- Contraction lemma
contraction : ∀ Γ Γ′ Γ″ {A B}
                     ->   Γ ⌊ A ⌋ Γ′ ⌊ A ⌋ Γ″ ⊢ B
                         ----------------------
                     ->   Γ ⌊ A ⌋ Γ′ ⌊⌋ Γ″ ⊢ B
contraction Γ Γ′ Γ″ = substitute (contr-lₛ 𝒯ermₛ Γ Γ′ Γ″)

-- Substitution lemma
substitution : ∀ Γ Γ′ {A B}
                     ->  Γ ⌊⌋ Γ′ ⊢ A   ->   Γ ⌊ A ⌋ Γ′ ⊢ B
                        --------------------------------
                     ->           Γ ⌊⌋ Γ′ ⊢ B
substitution Γ Γ′ M = substitute (sub-midₛ 𝒯ermₛ Γ Γ′ M)

-- Substitution lemma for computational terms
substitution′ : ∀ Γ Γ′ {A B}
                     ->  Γ ⌊⌋ Γ′ ⊢ A   ->   Γ ⌊ A ⌋ Γ′ ⊨ B
                        --------------------------------
                     ->           Γ ⌊⌋ Γ′ ⊨ B
substitution′ Γ Γ′ M = substitute′ (sub-midₛ 𝒯ermₛ Γ Γ′ M)

-- Top substitution lemma
[_/] : ∀ {Γ A B}
                     ->  Γ ⊢ A   ->   Γ , A  ⊢ B
                        --------------------------
                     ->           Γ ⊢ B
[_/] M = substitute (sub-topₛ 𝒯ermₛ M)

-- Top substitution lemma for computational terms
[_/′] : ∀ {Γ A B}
                     ->  Γ ⊢ A   ->   Γ , A  ⊨ B
                        --------------------------
                     ->           Γ ⊨ B
[_/′] M = substitute′ (sub-topₛ 𝒯ermₛ M)

-- Top substitution of computation into a computation
⟨_/⟩ : ∀ {Γ A B}      ->  Γ ⊨ A now  ->   Γ ˢ , A now ⊨ B now
                        ------------------------------------
                     ->              Γ ⊨ B now
⟨ pure M               /⟩ D = substitute′ (sub-topˢₛ 𝒯ermₛ M) D
⟨ letSig S InC C       /⟩ D = letSig S InC ⟨ C /⟩ (substitute′ ((idₛ 𝒯erm) ⁺ 𝒯erm ↑ 𝒯erm) D)
⟨ (letEvt_In_ {Γ} E C) /⟩ D = letEvt E In  ⟨ C /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D)
⟨ select_↦_||_↦_||both↦_ {Γ} E₁ C₁ E₂ C₂ C₃ /⟩ D
                           = select E₁ ↦ ⟨ C₁ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D)
                                 || E₂ ↦ ⟨ C₂ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D)
                                 ||both↦ ⟨ C₃ /⟩ (substitute′ ((Γ ˢˢₛ 𝒯erm) ↑ 𝒯erm) D)

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
-- Record modules for no-eta records should not be irrelevant in
-- record even if all fields are irrelevant (cc #392).

open import Agda.Builtin.Equality

postulate A : Set

record Unit : Set where
  no-eta-equality
  postulate a : A

record Irr : Set where
  no-eta-equality
  field .unit : Unit
  postulate a : A

record Coind : Set where
  coinductive
  postulate a : A

typeOf : {A : Set} → A → Set
typeOf {A} _ = A

checkUnit : typeOf Unit.a ≡ (Unit → A)
checkUnit = refl

checkIrr : typeOf Irr.a ≡ (Irr → A)
checkIrr = refl

checkCoind : typeOf Coind.a ≡ (Coind → A)
checkCoind = refl

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Data.Bool using (Bool; true; false)
open import Data.Float using (Float)
open import Avionics.Maybe using (Maybe; just; nothing; _>>=_; map)
--open import Data.Maybe using (Maybe; just; nothing; _>>=_; map)
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import Level using (0ℓ; _⊔_) renaming (suc to lsuc)
open import Relation.Binary using (Decidable)
open import Relation.Binary.Definitions using (Transitive; Trans)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (False; ⌊_⌋; True)
open import Relation.Unary using (Pred; _∈_)

-- stack exec -- agda -c --ghc-dont-call-ghc --no-main code.agda

infix  4 _≤_ _≤ᵇ_ _≤?_

postulate
  ℝ : Set

  fromFloat : Float → Maybe ℝ
  toFloat : ℝ → Float

  0ℝ : ℝ

  _≤_ : ℝ → ℝ → Set
  _≤?_ : (m n : ℝ) → Dec (m ≤ n)

_≤ᵇ_ : ℝ → ℝ → Bool
p ≤ᵇ q = ⌊ p ≤? q ⌋

postulate
  √_ : (x : ℝ) → .{0≤x : True (0ℝ ≤? x)} → ℝ

--Subset : Set → Set _
--Subset A = Pred A 0ℓ
--
--postulate
--  [0,∞⟩ : Subset ℝ
--
--  √_ : (x : ℝ) → .{0≤x : x ∈ [0,∞⟩} → ℝ

{-# COMPILE GHC ℝ = type Double #-}

-- `fromFloat` should check whether it is a valid floating point
-- number
{-# COMPILE GHC fromFloat = \x -> Just x #-}
{-# COMPILE GHC toFloat = \x -> x #-}

{-# COMPILE GHC 0ℝ = 0 #-}

{-# FOREIGN GHC type UnitErase a b = () #-}
{-# COMPILE GHC _≤_ = type UnitErase #-}
--{-# COMPILE GHC _≤_ = \ _ _ -> () #-}
{-# COMPILE GHC _≤ᵇ_ = (<=) #-}

--{-# FOREIGN GHC type UnitErase erase = () #-}
--{-# COMPILE GHC [0,∞⟩ = type UnitErase #-}

-- TODO: Find out how to perform the `sqrt` of a value!!
--       Here lies the main problem of compilation failure!
{-# COMPILE GHC √_  = \x _ -> sqrt x #-}
-- Agda is actually doing the right thing not accepting dubious
-- translations of code into Haskell

export√ : Float → Maybe Float
export√ x = fromFloat x >>= sqrt >>= just ∘ toFloat
  where
    sqrt : ℝ → Maybe ℝ
    sqrt y with 0ℝ ≤ᵇ y
    ... | false = nothing
    ... | true = just ((√ y) {y≥0})
      where postulate y≥0 : True (0ℝ ≤? y)
      --where postulate y≥0 : y ∈ [0,∞⟩
{-# COMPILE GHC export√ as exportSqrt #-}


text:
-- Andreas, 2018-05-27, issue #3090, reported by anka-213
-- Parser should not raise internal error for invalid symbol in name

{-# BUILTIN NATURAL ( #-}

-- Should fail with a parse error, not internal error


text:
--------------------------------------------------------------------------------
-- This file contains functions to convert between agda terms and meta-cedille
-- terms
--------------------------------------------------------------------------------

module Conversion where

open import Class.Monad.Except
open import Data.String using (fromList; toList)
open import Data.Tree
open import Data.Tree.Instance
open import Data.Word using (toℕ)
open import Data.List using (uncons)

open import CoreTheory
open import Parse.TreeConvert

open import Prelude
open import Prelude.Strings

module _ {M : Set → Set} {{_ : Monad M}} {{_ : MonadExcept M String}} where
  private
    {-# TERMINATING #-} -- findOutermostConstructor returns a list of smaller terms
    buildConstructorTree : Context → PureTerm → Tree PureTerm
    buildConstructorTree Γ t with findOutermostConstructor t
    ... | t' , ts = Node t' $ map (buildConstructorTree Γ) $ reverse ts

    extractConstrId : PureTerm → M (ℕ ⊎ Char)
    extractConstrId (Var-P (Bound x)) = return $ inj₁ $ toℕ x
    extractConstrId (Var-P (Free x)) = throwError ("Not a constructor:" <+> x)
    extractConstrId (Char-P c) = return $ inj₂ c
    {-# CATCHALL #-}
    extractConstrId t = throwError ("Not a variable" <+> show t)

    {-# TERMINATING #-}
    extractConstrIdTree : Tree PureTerm → M (Tree (ℕ ⊎ Char))
    extractConstrIdTree (Node x y) = do
      x' ← extractConstrId x
      y' ← sequence (map extractConstrIdTree y)
      return $ Node x' y'

  record Unquote (A : Set) : Set where
    field
      conversionFunction : Tree (ℕ ⊎ Char) → Maybe A
      nameOfA            : String

    unquoteConstrs : Context → PureTerm → M A
    unquoteConstrs Γ t = do
      t' ← appendIfError (extractConstrIdTree $ buildConstructorTree Γ t)
                         ("Error while converting term" <+> show t
                         <+> "to a tree of constructors of a" <+> nameOfA <+> "!")
      maybeToError (conversionFunction t') ("Error while converting to" <+> nameOfA + ". Term:"
                                           <+> show t + "\nTree:\n" + show {{Tree-Show}} t')

  open Unquote {{...}} public

  instance
    Unquote-Stmt : Unquote Stmt
    Unquote-Stmt = record { conversionFunction = toStmt ; nameOfA = "statement" }

    Unquote-Term : Unquote AnnTerm
    Unquote-Term = record { conversionFunction = toTerm ; nameOfA = "term" }

    Unquote-String : Unquote String
    Unquote-String = record { conversionFunction = toName ; nameOfA = "string" }

    Unquote-StringList : Unquote (List String)
    Unquote-StringList = record { conversionFunction = toNameList ; nameOfA = "string list" }

record Quotable (A : Set) : Set₁ where
  field
    quoteToAnnTerm : A → AnnTerm

  quoteToPureTerm : A → PureTerm
  quoteToPureTerm = Erase ∘ quoteToAnnTerm

open Quotable {{...}} public

instance
  Quotable-ListChar : Quotable (List Char)
  Quotable-ListChar .quoteToAnnTerm [] = FreeVar "init$string$nil"
  Quotable-ListChar .quoteToAnnTerm (c ∷ cs) = FreeVar "init$string$cons" ⟪$⟫ Char-A c ⟪$⟫ quoteToAnnTerm cs

  Quotable-String : Quotable String
  Quotable-String .quoteToAnnTerm = quoteToAnnTerm ∘ toList

  Quotable-ListString : Quotable (List String)
  Quotable-ListString .quoteToAnnTerm [] = FreeVar "init$stringList$nil"
  Quotable-ListString .quoteToAnnTerm (x ∷ l) =
    FreeVar "init$stringList$cons" ⟪$⟫ quoteToAnnTerm x ⟪$⟫ quoteToAnnTerm l

  private
    Quotable-Index : Quotable 𝕀
    Quotable-Index .quoteToAnnTerm i with uncons (toList (show i))
    ... | nothing      = Sort-A □ -- impossible
    ... | just (x , i) = FreeVar ("init$index$" + fromList [ x ] + "_index'_") ⟪$⟫ quoteIndex' i
      where
        quoteIndex' : List Char → AnnTerm
        quoteIndex' [] = FreeVar "init$index'$"
        quoteIndex' (x ∷ xs) = FreeVar ("init$index'$" + fromList [ x ] + "_index'_") ⟪$⟫ quoteIndex' xs

  Quotable-AnnTerm : Quotable AnnTerm
  Quotable-AnnTerm .quoteToAnnTerm (Var-A (Bound x)) = FreeVar "init$term$_var_"
    ⟪$⟫ (FreeVar "init$var$_index_" ⟪$⟫ quoteToAnnTerm x)
  Quotable-AnnTerm .quoteToAnnTerm (Var-A (Free x)) = FreeVar "init$term$_var_"
    ⟪$⟫ (FreeVar "init$var$_string_" ⟪$⟫ quoteToAnnTerm x)
  Quotable-AnnTerm .quoteToAnnTerm (Sort-A ⋆) = FreeVar "init$term$_sort_" ⟪$⟫ FreeVar "init$sort$=ast="
  Quotable-AnnTerm .quoteToAnnTerm (Sort-A □) = FreeVar "init$term$_sort_" ⟪$⟫ FreeVar "init$sort$=sq="
  Quotable-AnnTerm .quoteToAnnTerm (Const-A CharT) =
    FreeVar "init$term$=Kappa=_const_" ⟪$⟫ FreeVar "init$const$Char"
  Quotable-AnnTerm .quoteToAnnTerm (Pr1-A t) = FreeVar "init$term$=pi=^space^_term_" ⟪$⟫ quoteToAnnTerm t
  Quotable-AnnTerm .quoteToAnnTerm (Pr2-A t) = FreeVar "init$term$=psi=^space^_term_" ⟪$⟫ quoteToAnnTerm t
  Quotable-AnnTerm .quoteToAnnTerm (Beta-A t t₁) =
    FreeVar "init$term$=beta=^space^_term_^space^_term_" ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (Delta-A t t₁) =
    FreeVar "init$term$=delta=^space^_term_^space^_term_" ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (Sigma-A t) = FreeVar "init$term$=sigma=^space^_term_" ⟪$⟫ quoteToAnnTerm t
  Quotable-AnnTerm .quoteToAnnTerm (App-A t t₁) =
    FreeVar "init$term$=lsquare=^space'^_term_^space^_term_^space'^=rsquare="
      ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (AppE-A t t₁) =
    FreeVar "init$term$=langle=^space'^_term_^space^_term_^space'^=rangle="
      ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (Rho-A t t₁ t₂) =
    FreeVar "init$term$=rho=^space^_term_^space^_string_^space'^=dot=^space'^_term_^space^_term_"
      ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm (List Char ∋ "_") -- TODO: add a name to rho?
      ⟪$⟫ quoteToAnnTerm t₁ ⟪$⟫ quoteToAnnTerm t₂
  Quotable-AnnTerm .quoteToAnnTerm (All-A x t t₁) =
    FreeVar "init$term$=forall=^space^_string_^space'^=colon=^space'^_term_^space^_term_"
      ⟪$⟫ quoteToAnnTerm x ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (Pi-A x t t₁) =
    FreeVar "init$term$=Pi=^space^_string_^space'^=colon=^space'^_term_^space^_term_"
      ⟪$⟫ quoteToAnnTerm x ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (Iota-A x t t₁) =
    FreeVar "init$term$=iota=^space^_string_^space'^=colon=^space'^_term_^space^_term_"
      ⟪$⟫ quoteToAnnTerm x ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (Lam-A x t t₁) =
    FreeVar "init$term$=lambda=^space^_string_^space'^=colon=^space'^_term_^space^_term_"
      ⟪$⟫ quoteToAnnTerm x ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (LamE-A x t t₁) =
    FreeVar "init$term$=Lambda=^space^_string_^space'^=colon=^space'^_term_^space^_term_"
      ⟪$⟫ quoteToAnnTerm x ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (Pair-A t t₁ t₂) =
    FreeVar "init$term$=lbrace=^space'^_term_^space'^=comma=^space'^_term_^space^_string_^space'^=dot=^space'^_term_^space'^=rbrace=" ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
      ⟪$⟫ quoteToAnnTerm (List Char ∋ "_") ⟪$⟫ quoteToAnnTerm t₂ -- TODO: add a name to pair?
  Quotable-AnnTerm .quoteToAnnTerm (Phi-A t t₁ t₂) =
    FreeVar "init$term$=phi=^space^_term_^space^_term_^space^_term_"
      ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁ ⟪$⟫ quoteToAnnTerm t₂
  Quotable-AnnTerm .quoteToAnnTerm (Eq-A t t₁) =
    FreeVar "init$term$=equal=^space^_term_^space^_term_"
      ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (M-A t) = FreeVar "init$term$=omega=^space^_term_" ⟪$⟫ quoteToAnnTerm t
  Quotable-AnnTerm .quoteToAnnTerm (Mu-A t t₁) =
    FreeVar "init$term$=mu=^space^_term_^space^_term_"
      ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (Epsilon-A t) =
    FreeVar "init$term$=epsilon=^space^_term_" ⟪$⟫ quoteToAnnTerm t
  Quotable-AnnTerm .quoteToAnnTerm (Gamma-A t t₁) =
    FreeVar "init$term$=zeta=CatchErr^space^_term_^space^_term_" ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁
  Quotable-AnnTerm .quoteToAnnTerm (Ev-A x x₁) = Sort-A □ -- TODO
  Quotable-AnnTerm .quoteToAnnTerm (Char-A x) = FreeVar "init$term$=kappa=_char_" ⟪$⟫ Char-A x
  Quotable-AnnTerm .quoteToAnnTerm (CharEq-A t t₁) =
    FreeVar "init$term$=gamma=^space^_term_^space^_term_" ⟪$⟫ quoteToAnnTerm t ⟪$⟫ quoteToAnnTerm t₁

  Quotable-PureTerm : Quotable PureTerm
  Quotable-PureTerm .quoteToAnnTerm t = Sort-A □ -- TODO

  Quotable-ListTerm : Quotable (List AnnTerm)
  Quotable-ListTerm .quoteToAnnTerm [] = FreeVar "init$termList$nil"
  Quotable-ListTerm .quoteToAnnTerm (x ∷ l) = FreeVar "init$termList$cons" ⟪$⟫ quoteToAnnTerm x ⟪$⟫ quoteToAnnTerm l

Quotable-NoQuoteAnnTerm : Quotable AnnTerm
Quotable-NoQuoteAnnTerm .quoteToAnnTerm t = t

record ProductData (L R : Set) : Set where
  field
    lType rType : AnnTerm
    l : L
    r : R

-- The type of results of executing a statement in the interpreter. This can be
-- returned back to the code via embedExecutionResult
MetaResult = List String × List AnnTerm

instance
  Quotable-MetaResult : Quotable MetaResult
  Quotable-MetaResult .quoteToAnnTerm (fst , snd) =
    FreeVar "init$metaResult$pair" ⟪$⟫ quoteToAnnTerm fst ⟪$⟫ quoteToAnnTerm snd

  Quotable-ProductData : ∀ {L R} ⦃ _ : Quotable L ⦄ ⦃ _ : Quotable R ⦄ → Quotable (ProductData L R)
  Quotable-ProductData .quoteToAnnTerm pDat = let open ProductData pDat in
    FreeVar "init$pair" ⟪$⟫ lType ⟪$⟫ rType ⟪$⟫ quoteToAnnTerm l ⟪$⟫ quoteToAnnTerm r

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

module Algebra.Construct.Free.Semilattice.Homomorphism where

open import Prelude
open import Algebra
open import Path.Reasoning

open import Algebra.Construct.Free.Semilattice.Definition
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Union

module _ {b} (semilattice : Semilattice b) where
  open Semilattice semilattice
  module _ (sIsSet : isSet 𝑆) (h : A → 𝑆) where
    μ′ : A ↘ 𝑆
    [ μ′ ]-set = sIsSet
    [ μ′ ] x ∷ xs = h x ∙ xs
    [ μ′ ][] = ε
    [ μ′ ]-dup x xs =
      h x ∙ (h x ∙ xs) ≡˘⟨ assoc (h x) (h x) xs ⟩
      (h x ∙ h x) ∙ xs ≡⟨ cong (_∙ xs) (idem (h x)) ⟩
      h x ∙ xs ∎
    [ μ′ ]-com x y xs =
      h x ∙ (h y ∙ xs) ≡˘⟨ assoc (h x) (h y) xs ⟩
      (h x ∙ h y) ∙ xs ≡⟨ cong (_∙ xs) (comm (h x) (h y)) ⟩
      (h y ∙ h x) ∙ xs ≡⟨ assoc (h y) (h x) xs ⟩
      h y ∙ (h x ∙ xs) ∎

    μ : 𝒦 A → 𝑆
    μ = [ μ′ ]↓

    ∙-hom′ : ∀ ys → xs ∈𝒦 A ⇒∥ μ xs ∙ μ ys ≡ μ (xs ∪ ys) ∥
    ∥ ∙-hom′ ys ∥-prop = sIsSet _ _
    ∥ ∙-hom′ ys ∥[] = ε∙ _
    ∥ ∙-hom′ ys ∥ x ∷ xs ⟨ Pxs ⟩ =
      μ (x ∷ xs) ∙ μ ys ≡⟨⟩
      (h x ∙ μ xs) ∙ μ ys ≡⟨ assoc (h x) (μ xs) (μ ys) ⟩
      h x ∙ (μ xs ∙ μ ys) ≡⟨ cong (h x ∙_) Pxs ⟩
      h x ∙ μ (xs ∪ ys) ≡⟨⟩
      μ ((x ∷ xs) ∪ ys) ∎

    ∙-hom : ∀ xs ys → μ xs ∙ μ ys ≡ μ (xs ∪ ys)
    ∙-hom xs ys = ∥ ∙-hom′ ys ∥⇓ xs

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module BTA5 where

open import Data.Nat hiding (_<_)
open import Data.Bool
open import Data.List

open import Data.Nat.Properties

open import Relation.Nullary

-----------------
-- CLEANUP (∈) : this is surely in the standard library
-----------------
-- More general purpose definitions (should also be in standard library)
-- list membership
infix 4 _∈_
data _∈_ {A : Set} : A → List A → Set where
  hd : ∀ {x xs} → x ∈ (x ∷ xs)
  tl : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)

data Type : Set where
  Int : Type
  Fun : Type → Type → Type

data AType : Set where
    AInt  : AType
    AFun  : AType → AType → AType
    D     : Type → AType

-- typed annotated expressions
ACtx = List AType

Ctx = List Type

-----------------------
-- CLEANUP (≤) : these properties are surely in the standard library
-----------------------
≤-refl : ∀ {n} → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

-----------------------
-- CLEANUP (≤) : these properties are surely in the standard library
-----------------------
≤-trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c
≤-trans z≤n q = z≤n
≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q)

-----------------------
-- CLEANUP (≤) : these properties are surely in the standard library
-----------------------
≤-suc-right : ∀ {m n} → m ≤ n → m ≤ suc n
≤-suc-right z≤n = z≤n
≤-suc-right (s≤s p) = s≤s (≤-suc-right p)

-----------------------
-- CLEANUP (≤) : these properties are surely in the standard library
-----------------------
≤-suc-left : ∀ {m n} → suc m ≤ n → m ≤ n
≤-suc-left (s≤s p) = ≤-suc-right p

data _↝_ : Ctx → Ctx → Set where
  ↝-refl   : ∀ {Γ}      → Γ ↝ Γ
  ↝-extend : ∀ {Γ Γ' τ} → Γ ↝ Γ' → Γ ↝ (τ ∷ Γ')

↝-≤ : ∀ Γ Γ' → Γ ↝ Γ' → length Γ ≤ length Γ'
↝-≤ .Γ' Γ' ↝-refl = ≤-refl
↝-≤ Γ .(τ ∷ Γ') (↝-extend {.Γ} {Γ'} {τ} Γ↝Γ') = ≤-suc-right (↝-≤ Γ Γ' Γ↝Γ')

↝-no-left : ∀ Γ τ → ¬ (τ ∷ Γ) ↝ Γ
↝-no-left Γ τ p = 1+n≰n (↝-≤ (τ ∷ Γ) Γ p)

↝-trans : ∀ {Γ Γ' Γ''} → Γ ↝ Γ' → Γ' ↝ Γ'' → Γ ↝ Γ''
↝-trans Γ↝Γ' ↝-refl = Γ↝Γ'
↝-trans Γ↝Γ' (↝-extend Γ'↝Γ'') = ↝-extend (↝-trans Γ↝Γ' Γ'↝Γ'')

lem : ∀ x y xs xs' → (x ∷ xs) ↝ xs' → xs ↝ (y ∷ xs')
lem x y xs .(x ∷ xs) ↝-refl = ↝-extend (↝-extend ↝-refl)
lem x y xs .(x' ∷ xs') (↝-extend {.(x ∷ xs)} {xs'} {x'} p) = ↝-extend (lem x x' xs xs' p)

data _↝_↝_ : Ctx → Ctx → Ctx → Set where
  ↝↝-base   : ∀ {Γ Γ''} → Γ ↝ Γ'' → Γ ↝ [] ↝ Γ''
  ↝↝-extend : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → (τ ∷ Γ) ↝ (τ ∷ Γ') ↝ (τ ∷ Γ'')

-- Typed residula expressions
data Exp'' (Γ : Ctx) : Type → Set where
  EVar : ∀ {τ} → τ ∈ Γ → Exp'' Γ τ
  EInt : ℕ → Exp'' Γ Int
  EAdd : Exp'' Γ Int → Exp'' Γ Int -> Exp'' Γ Int
  ELam : ∀ {τ τ'} → Exp'' (τ ∷ Γ) τ' → Exp'' Γ (Fun τ τ')
  EApp : ∀ {τ τ'} → Exp'' Γ (Fun τ τ')  → Exp'' Γ τ → Exp'' Γ τ'

data AExp (Δ : ACtx) : AType → Set where
  AVar : ∀ {α} → α ∈ Δ → AExp Δ α
  AInt : ℕ → AExp Δ AInt
  AAdd : AExp Δ AInt → AExp Δ AInt → AExp Δ AInt
  ALam : ∀ {α₁ α₂}   → AExp (α₂ ∷ Δ) α₁ → AExp Δ (AFun α₂ α₁)
  AApp : ∀ {α₁ α₂}   → AExp Δ (AFun α₂ α₁) → AExp Δ α₂ → AExp Δ α₁
  DInt : ℕ → AExp Δ (D Int)
  DAdd : AExp Δ (D Int) → AExp Δ (D Int) → AExp Δ (D Int)
  DLam : ∀ {α₁ α₂}   → AExp ((D α₂) ∷ Δ) (D α₁) → AExp Δ (D (Fun α₂ α₁))
  DApp : ∀ {α₁ α₂}   → AExp Δ (D (Fun α₂ α₁)) → AExp Δ (D α₂) → AExp Δ (D α₁)

-- -- index Γ = nesting level of dynamic definitions / dynamic environment
Imp'' : Ctx → AType → Set
Imp'' Γ (AInt) = ℕ
Imp'' Γ (AFun α₁ α₂) = ∀ {Γ'} → Γ ↝ Γ' → (Imp'' Γ' α₁ → Imp'' Γ' α₂)
Imp'' Γ (D σ) = Exp'' Γ σ

-- -- index = nesting level of dynamic definitions
data AEnv2 : Ctx → ACtx → Set where
  [] : AEnv2 [] []
  consS : ∀ {Γ Δ Γ'} → Γ ↝ Γ' → (α : AType) → Imp'' Γ' α → AEnv2 Γ Δ → AEnv2 Γ' (α ∷ Δ)
  consD : ∀ {Γ Δ} → (σ : Type) → Exp'' (σ ∷ Γ)  σ → AEnv2 Γ Δ → AEnv2 (σ ∷ Γ) (D σ ∷ Δ)

elevate-var : ∀ {Γ Γ' τ} → Γ ↝ Γ' → τ ∈ Γ → τ ∈ Γ'
elevate-var ↝-refl x = x
elevate-var (↝-extend Γ↝Γ') x = tl (elevate-var Γ↝Γ' x)

elevate-var2 : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → τ ∈ Γ → τ ∈ Γ''
elevate-var2 (↝↝-base x) x₁ = elevate-var x x₁
elevate-var2 (↝↝-extend Γ↝Γ'↝Γ'') hd = hd
elevate-var2 (↝↝-extend Γ↝Γ'↝Γ'') (tl x) = tl (elevate-var2 Γ↝Γ'↝Γ'' x)

elevate : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → Exp'' Γ τ → Exp'' Γ'' τ
elevate Γ↝Γ'↝Γ'' (EVar x) = EVar (elevate-var2 Γ↝Γ'↝Γ'' x)
elevate Γ↝Γ'↝Γ'' (EInt x) = EInt x
elevate Γ↝Γ'↝Γ'' (EAdd e e₁) = EAdd (elevate Γ↝Γ'↝Γ'' e) (elevate Γ↝Γ'↝Γ'' e₁)
elevate Γ↝Γ'↝Γ'' (ELam e) = ELam (elevate (↝↝-extend Γ↝Γ'↝Γ'') e)
elevate Γ↝Γ'↝Γ'' (EApp e e₁) = EApp (elevate Γ↝Γ'↝Γ'' e) (elevate Γ↝Γ'↝Γ'' e₁)

lift2 : ∀ {Γ Γ'} α → Γ ↝ Γ' → Imp'' Γ α → Imp'' Γ' α
lift2 AInt p v = v
lift2 (AFun x x₁) Γ↝Γ' v = λ Γ'↝Γ'' → v (↝-trans Γ↝Γ' Γ'↝Γ'')
lift2 (D x₁) Γ↝Γ' v = elevate (↝↝-base Γ↝Γ') v

lookup2 : ∀ {α Δ Γ Γ'} → Γ ↝ Γ' → AEnv2 Γ Δ → α ∈ Δ → Imp'' Γ' α
lookup2 Γ↝Γ' (consS p α v env) hd = lift2 α Γ↝Γ' v
lookup2 Γ↝Γ' (consS p α₁ v env) (tl x) = lookup2 (↝-trans p Γ↝Γ') env x
lookup2 Γ↝Γ' (consD α v env) hd = lift2 (D α) Γ↝Γ' v
lookup2 ↝-refl (consD α₁ v env) (tl x) = lookup2 (↝-extend ↝-refl) env x
lookup2 (↝-extend Γ↝Γ') (consD α₁ v env) (tl x) = lookup2 (lem α₁ _ _ _ Γ↝Γ') env x

pe2 : ∀ {α Δ Γ} → AExp Δ α → AEnv2 Γ Δ → Imp'' Γ α
pe2 (AVar x) env = lookup2 ↝-refl env x
pe2 (AInt x) env = x
pe2 (AAdd e₁ e₂) env = pe2 e₁ env + pe2 e₂ env
pe2 {AFun α₂ α₁} (ALam e) env = λ Γ↝Γ' → λ y → pe2 e (consS Γ↝Γ' α₂ y env)
pe2 (AApp e₁ e₂) env = ((pe2 e₁ env) ↝-refl) (pe2 e₂ env)
pe2 (DInt x) env = EInt x
pe2 (DAdd e e₁) env = EAdd (pe2 e env) (pe2 e₁ env)
pe2 {D (Fun σ₁ σ₂)} (DLam e) env = ELam (pe2 e (consD σ₁ (EVar hd) env))
                                                 -- ELam (pe2 (consS (↝-extend {τ = σ₁} ↝-refl) (D σ₁) (EVar hd) env)) works too;
                                                 -- it is probably a canonical solution, but I (Lu) do not see why...
pe2 (DApp e e₁) env = EApp (pe2 e env) (pe2 e₁ env)

module Examples where
  open import Relation.Binary.PropositionalEquality

  x : ∀ {α Δ} → AExp (α ∷ Δ) α
  x = AVar hd
  y : ∀ {α₁ α Δ} → AExp (α₁ ∷ α ∷ Δ) α
  y = AVar (tl hd)
  z : ∀ {α₁ α₂ α Δ} → AExp (α₁ ∷ α₂ ∷ α ∷ Δ) α
  z = AVar (tl (tl hd))

-- Dλ y → let f = λ x → x D+ y in Dλ z → f z
  term1 : AExp [] (D (Fun Int (Fun Int Int)))
  term1 = DLam (AApp (ALam (DLam (AApp (ALam y) x)))
                     ((ALam (DAdd x y))))

-- Dλ y → let f = λ x → (Dλ w → x D+ y) in Dλ z → f z
-- Dλ y → (λ f → Dλ z → f z) (λ x → (Dλ w → x D+ y))
  term2 : AExp [] (D (Fun Int (Fun Int Int)))
  term2 = DLam (AApp (ALam (DLam (AApp (ALam y) x)))
                     ((ALam (DLam {α₂ = Int} (DAdd y z)))))

  ex-pe-term1 : pe2 term1 [] ≡ ELam (ELam (EVar hd))
  ex-pe-term1 = refl

  ex-pe-term2 : pe2 term2 [] ≡ ELam (ELam (EVar hd))
  ex-pe-term2 = refl

-- end of file

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Argument relevance used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.Argument.Relevance where

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Re-exporting the builtins publically

open import Agda.Builtin.Reflection public using (Relevance)
open Relevance public

------------------------------------------------------------------------
-- Decidable equality

_≟_ : DecidableEquality Relevance
relevant   ≟ relevant   = yes refl
irrelevant ≟ irrelevant = yes refl
relevant   ≟ irrelevant = no λ()
irrelevant ≟ relevant   = no λ()


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

open import lib.Base
open import lib.Function
open import lib.Equivalence
open import lib.Univalence
open import lib.NType
open import lib.PathGroupoid

{-
A proof of function extensionality from the univalence axiom.
-}

module lib.Funext {i} {A : Type i} where

-- Naive non dependent function extensionality

module FunextNonDep {j} {B : Type j} {f g : A → B} (h : f ∼ g)
  where

  private
    equiv-comp : {B C : Type j} (e : B ≃ C)
      → is-equiv (λ (g : A → B) → (λ x → –> e (g x)))
    equiv-comp {B} e =
      equiv-induction (λ {B} e → is-equiv (λ (g : A → B) → (λ x → –> e (g x))))
                      (λ A' → snd (ide (A → A'))) e

    free-path-space-B : Type j
    free-path-space-B = Σ B (λ x → Σ B (λ y → x == y))

    d : A → free-path-space-B
    d x = (f x , (f x , idp))

    e : A → free-path-space-B
    e x = (f x , (g x , h x))

    abstract
      fst-is-equiv : is-equiv (λ (y : free-path-space-B) → fst y)
      fst-is-equiv =
        is-eq fst (λ z → (z , (z , idp))) (λ _ → idp)
          (λ x' → ap (λ x → (_ , x))
                        (contr-has-all-paths _ _))

      comp-fst-is-equiv : is-equiv (λ (f : A → free-path-space-B)
                                     → (λ x → fst (f x)))
      comp-fst-is-equiv = equiv-comp ((λ (y : free-path-space-B) → fst y),
                                     fst-is-equiv)

      d==e : d == e
      d==e = equiv-is-inj comp-fst-is-equiv _ _ idp

  λ=-nondep : f == g
  λ=-nondep = ap (λ f' x → fst (snd (f' x))) d==e

open FunextNonDep using (λ=-nondep)

-- Weak function extensionality (a product of contractible types is
-- contractible)
module WeakFunext {j} {P : A → Type j} (e : (x : A) → is-contr (P x)) where

  P-is-Unit : P == (λ x → Lift Unit)
  P-is-Unit = λ=-nondep (λ x → ua (contr-equiv-LiftUnit (e x)))

  abstract
    weak-λ= : is-contr (Π A P)
    weak-λ= = transport (λ Q → is-contr (Π A Q)) (! P-is-Unit)
                            (has-level-in ((λ x → lift unit) , (λ y → λ=-nondep (λ x → idp))))

-- Naive dependent function extensionality

module FunextDep {j} {P : A → Type j} {f g : Π A P} (h : f ∼ g)
  where

  open WeakFunext

  Q : A → Type j
  Q x = Σ (P x) (λ y → f x == y)

  abstract
    Q-is-contr : (x : A) → is-contr (Q x)
    Q-is-contr x = pathfrom-is-contr (f x)

    instance
      ΠAQ-is-contr : is-contr (Π A Q)
      ΠAQ-is-contr = weak-λ= Q-is-contr

  Q-f : Π A Q
  Q-f x = (f x , idp)

  Q-g : Π A Q
  Q-g x = (g x , h x)

  abstract
    Q-f==Q-g : Q-f == Q-g
    Q-f==Q-g = contr-has-all-paths Q-f Q-g

  λ= : f == g
  λ= = ap (λ u x → fst (u x)) Q-f==Q-g

-- Strong function extensionality

module StrongFunextDep {j} {P : A → Type j} where

  open FunextDep

  app= : ∀ {f g : Π A P} (p : f == g) → f ∼ g
  app= p x = ap (λ u → u x) p

  λ=-idp : (f : Π A P)
    → idp == λ= (λ x → idp {a = f x})
  λ=-idp f = ap (ap (λ u x → fst (u x)))
    (contr-has-all-paths {{=-preserves-level
                           (ΠAQ-is-contr (λ x → idp))}}
                         idp (Q-f==Q-g (λ x → idp)))

  λ=-η : {f g : Π A P} (p : f == g)
    → p == λ= (app= p)
  λ=-η {f} idp = λ=-idp f

  app=-β : {f g : Π A P} (h : f ∼ g) (x : A)
    → app= (λ= h) x == h x
  app=-β h = app=-path (Q-f==Q-g h)  where

    app=-path : {f : Π A P} {u v : (x : A) → Q (λ x → idp {a = f x}) x}
      (p : u == v) (x : A)
      → app= (ap (λ u x → fst (u x)) p) x == ! (snd (u x)) ∙ snd (v x)
    app=-path {u = u} idp x = ! (!-inv-l (snd (u x)))

  app=-is-equiv : {f g : Π A P} → is-equiv (app= {f = f} {g = g})
  app=-is-equiv = is-eq _ λ= (λ h → λ= (app=-β h)) (! ∘ λ=-η)

  λ=-is-equiv : {f g : Π A P}
    → is-equiv (λ= {f = f} {g = g})
  λ=-is-equiv = is-eq _ app= (! ∘ λ=-η) (λ h → λ= (app=-β h))

-- We only export the following

module _ {j} {P : A → Type j} {f g : Π A P} where

  app= : f == g → f ∼ g
  app= p x = ap (λ u → u x) p

  abstract
    λ= : f ∼ g → f == g
    λ= = FunextDep.λ=

    app=-β : (p : f ∼ g) (x : A) → app= (λ= p) x == p x
    app=-β = StrongFunextDep.app=-β

    λ=-η : (p : f == g) → p == λ= (app= p)
    λ=-η = StrongFunextDep.λ=-η

  λ=-equiv : (f ∼ g) ≃ (f == g)
  λ=-equiv = (λ= , λ=-is-equiv) where
    abstract
      λ=-is-equiv : is-equiv λ=
      λ=-is-equiv = StrongFunextDep.λ=-is-equiv

  app=-equiv : (f == g) ≃ (f ∼ g)
  app=-equiv = (app= , app=-is-equiv) where
    abstract
      app=-is-equiv : is-equiv app=
      app=-is-equiv = StrongFunextDep.app=-is-equiv

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Lec6Done where

open import Lec1Done

data List (X : Set) : Set where
  []   : List X
  _,-_ : X -> List X -> List X
infixr 4 _,-_

-- ListF : Set -> Set -> Set
-- ListF X T = One + (X * T)

mkList : {X : Set} -> One + (X * List X) -> List X
mkList (inl <>)        = []
mkList (inr (x , xs))  = x ,- xs

foldr : {X T : Set} -> ((One + (X * T)) -> T) -> List X -> T
foldr alg []         = alg (inl <>)
foldr alg (x ,- xs)  = alg (inr (x , foldr alg xs))

ex1 = foldr mkList (1 ,- 2 ,- 3 ,- [])

length : {X : Set} -> List X -> Nat
length = foldr \ { (inl <>) -> zero ; (inr (x , n)) -> suc n }

record CoList (X : Set) : Set where
  coinductive
  field
    force : One + (X * CoList X)
open CoList

[]~ : {X : Set} -> CoList X
force []~ = inl <>

_,~_ : {X : Set} -> X -> CoList X -> CoList X
force (x ,~ xs) = inr (x , xs)
infixr 4 _,~_

unfoldr : {X S : Set} -> (S -> (One + (X * S))) -> S -> CoList X
force (unfoldr coalg s) with coalg s
force (unfoldr coalg s) | inl <>       = inl <>
force (unfoldr coalg s) | inr (x , s') = inr (x , unfoldr coalg s')

ex2 = unfoldr force (1 ,~ 2 ,~ 3 ,~ []~)

repeat : {X : Set} -> X -> CoList X
repeat = unfoldr \ x -> inr (x , x)

prefix : {X : Set} -> Nat -> CoList X -> List X
prefix zero xs = []
prefix (suc n) xs with force xs
prefix (suc n) xs | inl <> = []
prefix (suc n) xs | inr (x , xs') = x ,- prefix n xs'

ex2' = prefix 3 ex2

record Stream (X : Set) : Set where
  coinductive
  field
    hdTl : X * Stream X
open Stream

forever : {X : Set} -> X -> Stream X
fst (hdTl (forever x)) = x
snd (hdTl (forever x)) = forever x

unfold : {X S : Set} -> (S -> X * S) -> S -> Stream X
fst (hdTl (unfold coalg s)) = fst (coalg s)
snd (hdTl (unfold coalg s)) = unfold coalg (snd (coalg s))

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
{-

This file contains:

- Properties of 2-groupoid truncations

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.2GroupoidTruncation.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.Foundations.Equiv
open import Cubical.Foundations.Univalence

open import Cubical.HITs.2GroupoidTruncation.Base

private
  variable
    ℓ : Level
    A : Type ℓ

rec : ∀ {B : Type ℓ} → is2Groupoid B → (A → B) → ∥ A ∥₄ → B
rec gB f ∣ x ∣₄ = f x
rec gB f (squash₄ _ _ _ _ _ _ t u i j k l) =
  gB _ _ _ _ _ _ (λ m n o → rec gB f (t m n o)) (λ m n o → rec gB f (u m n o))
     i j k l

elim : {B : ∥ A ∥₄ → Type ℓ}
       (bG : (x : ∥ A ∥₄) → is2Groupoid (B x))
       (f : (x : A) → B ∣ x ∣₄) (x : ∥ A ∥₄) → B x
elim bG f ∣ x ∣₄ = f x
elim bG f (squash₄ x y p q r s u v i j k l) =
  isOfHLevel→isOfHLevelDep 4 bG _ _ _ _ _ _
    (λ j k l → elim bG f (u j k l)) (λ j k l → elim bG f (v j k l))
    (squash₄ x y p q r s u v)
    i j k l

elim2 : {B : ∥ A ∥₄ → ∥ A ∥₄ → Type ℓ}
        (gB : ((x y : ∥ A ∥₄) → is2Groupoid (B x y)))
        (g : (a b : A) → B ∣ a ∣₄ ∣ b ∣₄)
        (x y : ∥ A ∥₄) → B x y
elim2 gB g = elim (λ _ → is2GroupoidΠ (λ _ → gB _ _))
                  (λ a → elim (λ _ → gB _ _) (g a))

elim3 : {B : (x y z : ∥ A ∥₄) → Type ℓ}
        (gB : ((x y z : ∥ A ∥₄) → is2Groupoid (B x y z)))
        (g : (a b c : A) → B ∣ a ∣₄ ∣ b ∣₄ ∣ c ∣₄)
        (x y z : ∥ A ∥₄) → B x y z
elim3 gB g = elim2 (λ _ _ → is2GroupoidΠ (λ _ → gB _ _ _))
                   (λ a b → elim (λ _ → gB _ _ _) (g a b))

2GroupoidTruncIs2Groupoid : is2Groupoid ∥ A ∥₄
2GroupoidTruncIs2Groupoid a b p q r s = squash₄ a b p q r s

2GroupoidTruncIdempotent≃ : is2Groupoid A → ∥ A ∥₄ ≃ A
2GroupoidTruncIdempotent≃ {A = A} hA = isoToEquiv f
  where
  f : Iso ∥ A ∥₄ A
  Iso.fun f = rec hA (idfun A)
  Iso.inv f x = ∣ x ∣₄
  Iso.rightInv f _ = refl
  Iso.leftInv f = elim (λ _ → isOfHLevelSuc 4 2GroupoidTruncIs2Groupoid _ _) (λ _ → refl)

2GroupoidTruncIdempotent : is2Groupoid A → ∥ A ∥₄ ≡ A
2GroupoidTruncIdempotent hA = ua (2GroupoidTruncIdempotent≃ hA)

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:
-- This module introduces parameterised datatypes.

module DataParameterised where

-- First some of our old friends.

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

data Bool : Set where
  false : Bool
  true  : Bool

-- A datatype can be parameterised over a telescope, (A : Set) in the case of
-- lists. The parameters are bound in the types of the constructors.

data List (A : Set) : Set where
  nil  : List A
  cons : A -> List A -> List A

-- When using the constructors the parameters to the datatype becomes implicit
-- arguments. In this case, the types of the constructors are :

--  nil  : {A : Set} -> List A
--  cons : {A : Set} -> A -> List A -> List A

-- So, we can write

--nilNat = nil {Nat}  -- the type of this will be List Nat

-- When pattern matching on elements of a parameterised datatype you cannot
-- refer to the parameters--it wouldn't make sense to pattern match on the
-- element type of the list. So you can say

null : {A : Set} -> List A -> Bool
null  nil       = true
null (cons _ _) = false

-- but not

-- null (nil  {A})     = true
-- null (cons {A} _ _) = false

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
------------------------------------------------------------------------------
-- Testing the translation of scheme's instances
------------------------------------------------------------------------------

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

module Instance where

-- A schema
-- Current translation: ∀ p q x. app(p,x) → app(q,x).
postulate
  D      : Set
  schema : (A B : D → Set) → ∀ {x} → A x → B x

-- Using the current translation, the ATPs can prove an instance of
-- the schema.
postulate
  d         : D
  A B       : D → Set
  instanceC : A d → B d
{-# ATP prove instanceC schema #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

module hSet where

  open import lib.Basics
  open import lib.Funext
  open import lib.NType2
  open import lib.types.Truncation
  open import lib.types.Bool
  open import PropT

  _is-a-set : {i : ULevel} (A : Type i) → Type i
  A is-a-set = is-set A

  -- To get an element a of the set A is to give a : ∈ A.
  ∈ : {i : ULevel} (A : hSet i) → Type i
  ∈ = fst

  set-is-a-set : {i : ULevel} (A : hSet i) → (∈ A) is-a-set
  set-is-a-set A = snd A

  -- Equality for sets, landing in Prop
  _==ₚ_ : {i : ULevel} {A : hSet i}
          → (x y : ∈ A) → PropT i
  _==ₚ_ {_} {A} x y = (x == y) , has-level-apply (set-is-a-set A) x y

  _=bool=_ : {i : ULevel} {A : Type i} {p : has-dec-eq A}
             → (x y : A) → Bool
  _=bool=_ {p = p} x y  = case (p x y)
    where case : Dec (x == y) → Bool
          case (inl _) = true
          case (inr _) = false

  ∥_∥₀ : ∀ {i} (A : Type i) → Type i
  ∥_∥₀ = Trunc 0

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


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

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)-- ¬ᵗ_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Function.Base using (_∋_; _$_; it)
open import Cubical.Foundations.Logic renaming
  ( inl to inlᵖ
  ; inr to inrᵖ
  ; _⇒_ to infixr 0 _⇒_                  -- shifting by -6
  ; _⇔_ to infixr -2 _⇔_                 --
  ; ∃[]-syntax to infix  -4 ∃[]-syntax   --
  ; ∃[∶]-syntax to infix  -4 ∃[∶]-syntax --
  ; ∀[∶]-syntax to infix  -4 ∀[∶]-syntax --
  ; ∀[]-syntax to infix  -4 ∀[]-syntax   --
  )
open import Cubical.Data.Unit.Base using (Unit)

import Data.Sum
import Cubical.Data.Sigma

import Cubical.Algebra.CommRing

import Cubical.Core.Primitives
import Agda.Builtin.Cubical.Glue
import Cubical.Foundations.Id

open import MoreLogic.Reasoning
open import MoreLogic.Definitions renaming (_ᵗ⇒_ to infixr 0 _ᵗ⇒_)
open import MoreLogic.Properties

open import Utils

open import MorePropAlgebra.Bundles
open import MorePropAlgebra.Definitions as Defs hiding (_≤''_)
open import MorePropAlgebra.Consequences

module MorePropAlgebra.Bridges1999 {ℓ ℓ'} (assumptions : PartiallyOrderedField {ℓ} {ℓ'}) where

import MorePropAlgebra.Properties.AlmostPartiallyOrderedField
-- module AlmostPartiallyOrderedField'Properties  = MorePropAlgebra.Properties.AlmostPartiallyOrderedField   record { PartiallyOrderedField assumptions }
-- module AlmostPartiallyOrderedField'            =                            AlmostPartiallyOrderedField   record { PartiallyOrderedField assumptions }
-- (      AlmostPartiallyOrderedField')           =                            AlmostPartiallyOrderedField ∋ record { PartiallyOrderedField assumptions }

-- module This = PartiallyOrderedField assumptions renaming (Carrier to F; _-_ to _-_)

-- import MorePropAlgebra.Booij2020
-- -- open MorePropAlgebra.Booij2020.Chapter4 AlmostPartiallyOrderedField' public
-- open MorePropAlgebra.Booij2020.Chapter4 (record { PartiallyOrderedField assumptions }) public
-- open +-<-ext+·-preserves-<⇒ (PartiallyOrderedField.+-<-ext assumptions) (PartiallyOrderedField.·-preserves-< assumptions) public
-- -- open AlmostPartiallyOrderedField'Properties -- using (_⁻¹; _≤''_)
-- -- open MorePropAlgebra.Properties.AlmostPartiallyOrderedField (record { PartiallyOrderedField assumptions }) public

-- remember opening this as the last one to omit prefixes
-- open import MorePropAlgebra.Properties.PartiallyOrderedField assumptions
-- open PartiallyOrderedField assumptions renaming (Carrier to F; _-_ to _-_)

import MorePropAlgebra.Booij2020
open MorePropAlgebra.Booij2020.Chapter4 (record { PartiallyOrderedField assumptions })
open +-<-ext+·-preserves-<⇒ (PartiallyOrderedField.+-<-ext assumptions) (PartiallyOrderedField.·-preserves-< assumptions)
-- open MorePropAlgebra.Properties.AlmostPartiallyOrderedField (record { PartiallyOrderedField assumptions }) hiding (_⁻¹)
open import MorePropAlgebra.Properties.PartiallyOrderedField assumptions
open PartiallyOrderedField assumptions renaming (Carrier to F; _-_ to _-_) hiding (_#_; _≤_)
open AlmostPartiallyOrderedField' using (_#_; _≤_)
open AlmostPartiallyOrderedField'Properties -- using (_⁻¹)

-- NOTE: we are proving Bridges' properties with Booij's definition of _≤_
--         which is some form of cheating
--       because we are interested in the properties, mostly
--         or rather to check our definitions for "completeness" against these properties
--       therefore our proofs differ from Brigdes' proofs
--         and this approach does not show that from R1-* and R2-* follows Prop-* as in the paper

private
  ≤⇒≤'' : ∀ x y → [ x ≤ y ] → [ x ≤'' y ]
  ≤⇒≤'' x y = ≤-⇔-≤'' x y .fst

  ≤''⇒≤ : ∀ x y → [ x ≤'' y ] → [ x ≤ y ]
  ≤''⇒≤ x y = ≤-⇔-≤'' x y .snd

  ≤-≡-≤'' : ∀ x y → (Liftᵖ {ℓ'} {ℓ} (x ≤ y)) ≡ (x ≤'' y)
  ≤-≡-≤'' x y = ⇔toPath ((≤⇒≤'' x y) ∘ (unliftᵖ (x ≤ y))) ((liftᵖ (x ≤ y)) ∘ (≤''⇒≤ x y))

is-0≡-0 : 0f ≡ - 0f
is-0≡-0 = sym (+-inv 0f .snd) ∙ (+-identity (- 0f) .fst)

-swaps-<ˡ : ∀ x y → [ (- x) < (- y) ⇒ y < x ]
-swaps-<ˡ x y =
  [ - x     < - y             ] ⇒⟨ +-preserves-< _ _ _ ⟩
  [ - x + x < - y + x         ] ⇒⟨ subst (λ p → [ p < - y + x ]) (+-linv x) ⟩
  [  0f     < - y + x         ] ⇒⟨ subst (λ p → [ 0f < p ]) (+-comm (- y) x) ⟩
  [  0f     <   x - y         ] ⇒⟨ +-preserves-< _ _ _ ⟩
  [  0f + y <  (x - y) + y    ] ⇒⟨ subst (λ p → [ p < (x - y) + y ]) (+-identity y .snd) ⟩
  [       y <  (x - y) + y    ] ⇒⟨ subst (λ p → [ y < p ]) (sym $ +-assoc x (- y) y) ⟩
  [       y <   x + (- y + y) ] ⇒⟨ subst (λ p → [ y < x + p ]) (+-linv y) ⟩
  [       y <   x + 0f        ] ⇒⟨ subst (λ p → [ y < p ]) (+-identity x .fst) ⟩
  [       y <   x             ] ◼

-- invInvo
-swaps-<ʳ : ∀ x y → [ x < y ⇒ (- y) < (- x) ]
-swaps-<ʳ x y =
  [     x <     y ] ⇒⟨ subst (λ p → [ p < y ]) (sym $ GroupLemmas'.invInvo x) ⟩
  [ - - x <     y ] ⇒⟨ subst (λ p → [ - - x < p ]) (sym $ GroupLemmas'.invInvo y) ⟩
  [ - - x < - - y ] ⇒⟨ -swaps-<ˡ (- x) (- y) ⟩
  [   - y <   - x ] ◼

-swaps-< : ∀ x y → [ x < y ⇔ (- y) < (- x) ]
-swaps-< x y .fst = -swaps-<ʳ x y
-swaps-< x y .snd = -swaps-<ˡ y x

·-reflects-<0 : ∀ x y → [ 0f < y ] → [ x · y < 0f ] → [ x < 0f ]
·-reflects-<0 x y 0<y x·y<0 = ·-reflects-< x 0f y 0<y  (subst (λ p → [ x · y < p ]) (sym $ RingTheory'.0-leftNullifies y) x·y<0)

-- NOTE: Brigdes writes `x ≠ y`  where we write   `x # y`
--                and `¬(x = y)` where we write `¬(x ≡ y)`

-- Heyting field axioms
R1-1 = ∀[ x ] ∀[ y ]              [ is-set ]            x + y ≡ˢ y + x
R1-2 = ∀[ x ] ∀[ y ] ∀[ z ]       [ is-set ]      (x + y) + z ≡ˢ x + (y + z)
R1-3 = ∀[ x ]                     [ is-set ]           0f + x ≡ˢ x
R1-4 = ∀[ x ]                     [ is-set ]        x + (- x) ≡ˢ 0f
R1-5 = ∀[ x ] ∀[ y ]              [ is-set ]            x · y ≡ˢ y · x
R1-6 = ∀[ x ] ∀[ y ] ∀[ z ]       [ is-set ]      (x · y) · z ≡ˢ x · (y · z)
R1-7 = ∀[ x ]                     [ is-set ]           1f · x ≡ˢ x
R1-8 = ∀[ x ] ∀[ p ∶ [ x # 0f ] ] [ is-set ] x · (x ⁻¹) {{p}} ≡ˢ 1f
R1-9 = ∀[ x ] ∀[ y ] ∀[ z ]       [ is-set ]      x · (y + z) ≡ˢ x · y + x · z

-- _<_ axioms
R2-1 = ∀[ x ] ∀[ y ]                                  ¬((x < y) ⊓ (y < x)) -- <-asym
R2-2 = ∀[ x ] ∀[ y ]   ( x < y)            ⇒ (∀[ z ]    (z < y) ⊔ (x < z)) -- <-cotrans
R2-3 = ∀[ x ] ∀[ y ]  ¬( x # y)            ⇒ [ is-set ]       x ≡ˢ y       -- #-tight
R2-4 = ∀[ x ] ∀[ y ]   ( x < y)            ⇒ (∀[ z ]    (x + z) < (y + z)) -- +-preserves-<
R2-5 = ∀[ x ] ∀[ y ]   (0f < x) ⇒ (0f < y) ⇒                 0f < x · y    -- ·-preserves-0<

-- Special properties of _<_
-- R3-1 Axiom of Archimedes: `∀(x ∈ ℝ) → ∃[ n ∈ ℤ ] x < n`
-- R3-2 The least-upper-bound principle:
--   Let S be a nonempty subset of R that is bounded
--   above relative to the relation ≥, such that for all real numbers α, β with α < β
--   either β is an upper bound of S or else there exists s ∈ S with s > α; then S has a
--   least upper bound.

-- derivable properties
Prop-1  = ∀[ x ]                                                            ¬(x < x) -- <-irrefl
Prop-2  = ∀[ x ]                                                              x ≤ x  -- ≤-refl
Prop-3  = ∀[ x ] ∀[ y ] ∀[ z ] (    x < y    ) ⇒ (y < z ) ⇒                   x < z  -- <-trans
Prop-4  = ∀[ x ] ∀[ y ]                                               ¬((x < y) ⊓ (y ≤ x))
Prop-5  = ∀[ x ] ∀[ y ] ∀[ z ] (    x ≤ y    ) ⇒ (y < z ) ⇒                   x < z  -- ≤-<-trans
Prop-6  = ∀[ x ] ∀[ y ] ∀[ z ] (    x < y    ) ⇒ (y ≤ z ) ⇒                   x < z  -- <-≤-trans
Prop-7  = ∀[ x ] ∀[ y ]                                               (¬(x < y) ⇔    (y ≤ x)) -- definition of ≤
Prop-8  = ∀[ x ] ∀[ y ]                                               (¬(x ≤ y) ⇔ ¬ ¬(y < x)) -- ≤ weaker than <
Prop-9  = ∀[ x ] ∀[ y ] ∀[ z ] (    y ≤ z    ) ⇒ (x ≤ y ) ⇒                  (x ≤ z) -- ≤-trans
Prop-10 = ∀[ x ] ∀[ y ]        (    x ≤ y    ) ⇒ (y ≤ x ) ⇒                        [ is-set ] x ≡ˢ y -- ≤-antisym
Prop-11 = ∀[ x ] ∀[ y ]                                               ¬((x < y) ⊓ ([ is-set ] x ≡ˢ y))
Prop-12 = ∀[ x ]               (   0f ≤ x    )            ⇒ ([ is-set ] x ≡ˢ 0f ⇔ (∀[ ε ] (0f < ε) ⇒ (x < ε)))
Prop-13 = ∀[ x ] ∀[ y ]        (   0f < x + y)            ⇒            (0f < x) ⊔ (0f < y)
Prop-14 = ∀[ x ]               (   0f < x    )            ⇒                 - x < 0f -- -flips-<0
Prop-15 = ∀[ x ] ∀[ y ] ∀[ z ] (    x < y    ) ⇒ (z < 0f) ⇒               y · z < x · z -- ·-preserves-<
Prop-16 = ∀[ x ]               (    x # 0f   )            ⇒                  0f < x · x -- sqr-positive
Prop-17 =                                                                    0f < 1f
Prop-18 = ∀[ x ]                                                             0f ≤ x · x -- sqr-nonnegative
Prop-19 = ∀[ x ]               (   0f < x    ) ⇒ (x < 1f) ⇒               x · x < x
Prop-20 = ∀[ x ]               ( - 1f < x    ) ⇒ (x < 1f) ⇒       ¬((x < x · x) ⊓ (- x < x · x))
Prop-21 = ∀[ x ]               (   0f < x · x)            ⇒                   x # 0f
Prop-22 = ∀[ x ]               (   0f < x    )            ⇒ Σᵖ[ p ∶ x # 0f ] (0f ≤ (x ⁻¹) {{p}})
-- Prop-23 `∀ m m' n n' → 0 < n → 0 < n' → (m / n > m' / n') ⇔ (m · n' > m' · n)`
-- Prop-24 `∀(n ∈ ℕ⁺) → (n ⁻¹ > 0)`
-- Prop-25 `x > 0 → y ≥ 0 → ∃[ n ∈ ℤ ] n · x > y`
-- Prop-26 `(x > 0) ⇒ (x ⁻¹ > 0)`
-- Prop-27 `(x · y > 0) ⇒ (x ≠ 0) ⊓ (y ≠ 0)`
-- Prop-28 `∀(x > 0) → ∃[ n ∈ ℕ⁺ ] x < n < x + 2`
-- Prop-29 `∀ a b → a < b → ∃[ q ∈ ℚ ] a < r < b`

r1-1 : ∀ x y                      →            x + y ≡ y + x        ; _ : [ R1-1 ]; _ = r1-1
r1-2 : ∀ x y z                    →      (x + y) + z ≡ x + (y + z)  ; _ : [ R1-2 ]; _ = r1-2
r1-3 : ∀ x                        →           0f + x ≡ x            ; _ : [ R1-3 ]; _ = r1-3
r1-4 : ∀ x                        →        x + (- x) ≡ 0f           ; _ : [ R1-4 ]; _ = r1-4
r1-5 : ∀ x y                      →            x · y ≡ y · x        ; _ : [ R1-5 ]; _ = r1-5
r1-6 : ∀ x y z                    →      (x · y) · z ≡ x · (y · z)  ; _ : [ R1-6 ]; _ = r1-6
r1-7 : ∀ x                        →           1f · x ≡ x            ; _ : [ R1-7 ]; _ = r1-7
r1-8 : ∀ x     → (p : [ x # 0f ]) → x · (x ⁻¹) {{p}} ≡ 1f           ; _ : [ R1-8 ]; _ = r1-8
r1-9 : ∀ x y z                    →      x · (y + z) ≡ x · y + x · z; _ : [ R1-9 ]; _ = r1-9

r1-1       =       +-comm
r1-2 x y z = sym $ +-assoc    x y z
r1-3 x     =       +-identity x .snd
r1-4 x     =       +-inv      x .fst
r1-5       =       ·-comm
r1-6 x y z = sym $ ·-assoc    x y z
r1-7 x     =       ·-identity x .snd
r1-8       =       ·-rinv
r1-9 x y z =       is-dist    x y z .fst

r2-1 : ∀ x y →                                    [ ¬((x < y) ⊓ (y < x)) ]; _ : [ R2-1 ]; _ = r2-1
r2-2 : ∀ x y → [    x < y  ]              → ∀ z → [   (z < y) ⊔ (x < z)  ]; _ : [ R2-2 ]; _ = r2-2
r2-3 : ∀ x y → [ ¬( x # y) ]              →                 x ≡ y         ; _ : [ R2-3 ]; _ = r2-3
r2-4 : ∀ x y → [    x < y  ]              → ∀ z → [ (x + z) < (y + z)    ]; _ : [ R2-4 ]; _ = r2-4
r2-5 : ∀ x y → [   0f < x  ] → [ 0f < y ] →       [      0f < x · y      ]; _ : [ R2-5 ]; _ = r2-5

r2-1 x y (x<y , y<x) = <-asym x y x<y y<x
r2-2 x y x<y z = pathTo⇒ (⊔-comm (x < z) (z < y)) (<-cotrans x y x<y z)
r2-3 = #-tight
r2-4 x y x<y z = +-preserves-< x y z x<y
r2-5 x y 0<x 0<y = subst (λ p → [ p < x · y ]) (RingTheory'.0-leftNullifies y) (·-preserves-< 0f x y 0<y 0<x)

prop-1   : ∀ x                             → [       ¬(x < x)         ]; _ : [ Prop-1  ]; _ = prop-1
prop-2   : ∀ x                             → [         x ≤ x          ]; _ : [ Prop-2  ]; _ = prop-2
prop-3   : ∀ x y z → [ x < y ] → [ y < z ] → [         x < z          ]; _ : [ Prop-3  ]; _ = prop-3
prop-4   : ∀ x y                           → [ ¬((x < y) ⊓ (y ≤ x))   ]; _ : [ Prop-4  ]; _ = prop-4
prop-5   : ∀ x y z → [ x ≤ y ] → [ y < z ] → [         x < z          ]; _ : [ Prop-5  ]; _ = prop-5
prop-6   : ∀ x y z → [ x < y ] → [ y ≤ z ] → [         x < z          ]; _ : [ Prop-6  ]; _ = prop-6
prop-7   : ∀ x y                           → [ (¬(x < y) ⇔    (y ≤ x))]; _ : [ Prop-7  ]; _ = prop-7
prop-8   : ∀ x y                           → [  ¬(x ≤ y) ⇔ ¬ ¬(y < x) ]; _ : [ Prop-8  ]; _ = prop-8
prop-9   : ∀ x y z → [ y ≤ z ] → [ x ≤ y ] → [         x ≤ z          ]; _ : [ Prop-9  ]; _ = prop-9
prop-10  : ∀ x y   → [ x ≤ y ] → [ y ≤ x ] →                   x ≡ y   ; _ : [ Prop-10 ]; _ = prop-10
prop-11  : ∀ x y                           → ¬ᵗ ([ x < y ] ×  (x ≡ y)) ; _ : [ Prop-11 ]; _ = prop-11

prop-12  : ∀ x     → [   0f ≤ x     ]              → [ [ is-set ] x ≡ˢ 0f ⇔ (∀[ ε ] (0f < ε) ⇒ (x < ε)) ]; _ : [ Prop-12 ]; _ = prop-12
prop-13  : ∀ x y   → [   0f < x + y ]              → [           (0f < x) ⊔ (0f < y)         ]; _ : [ Prop-13 ]; _ = prop-13
prop-14  : ∀ x     → [   0f < x     ]              → [                - x < 0f               ]; _ : [ Prop-14 ]; _ = prop-14
prop-14' : ∀ x     → [    x < 0f    ]              → [                 0f < - x              ]
prop-15  : ∀ x y z → [    x < y     ] → [ z < 0f ] → [              y · z < x · z            ]; _ : [ Prop-15 ]; _ = prop-15
prop-16  : ∀ x     → [    x # 0f    ]              → [                 0f < x · x            ]; _ : [ Prop-16 ]; _ = prop-16
prop-17  :                                           [                 0f < 1f               ]; _ : [ Prop-17 ]; _ = prop-17
prop-18  : ∀ x                                     → [                 0f ≤ x · x            ]; _ : [ Prop-18 ]; _ = prop-18
prop-19  : ∀ x     → [   0f < x     ] → [ x < 1f ] → [              x · x < x                ]; _ : [ Prop-19 ]; _ = prop-19
prop-20  : ∀ x     → [ - 1f < x     ] → [ x < 1f ] → [      ¬((x < x · x) ⊓ (- x < x · x))   ]; _ : [ Prop-20 ]; _ = prop-20
prop-21  : ∀ x     → [   0f < x · x ]              → [                  x # 0f               ]; _ : [ Prop-21 ]; _ = prop-21
prop-22  : ∀ x     → [   0f < x     ]              → Σ[ p ∈ [ x # 0f ] ] [ 0f ≤ (x ⁻¹) {{p}} ]; _ : [ Prop-22 ]; _ = prop-22
prop-22' : ∀ x     → [   0f < x     ]              → Σ[ p ∈ [ x # 0f ] ] [ 0f < (x ⁻¹) {{p}} ]

prop-1 = <-irrefl
prop-2 = ≤-refl
prop-3 = <-trans
prop-4 x y (x<y , y≤x) = y≤x x<y
prop-5 = ≤-<-trans
prop-6 = <-≤-trans
prop-7 x y .fst = λ x → x -- holds definitionally for Booij's _≤_
prop-7 x y .snd = λ x → x
prop-8  x y .fst = λ x → x -- holds definitionally for Booij's _≤_
prop-8  x y .snd = λ x → x -- holds definitionally for Booij's _≤_
prop-9  x y z y≤z x≤y = ≤-trans x y z x≤y y≤z
prop-10 = ≤-antisym
prop-11 x y (x<y , x≡y) = <-irrefl _ (pathTo⇒ (λ i → x≡y i < y) x<y)

fst (prop-12 x 0≤x) x≡0 y 0<y  = transport (λ i → [ x≡0 (~ i) < y ]) 0<y
-- suppose that x < ε for all ε > 0. If x > 0, then x < x, a contradiction; so 0 ≥ x. Thus x ≥ 0 and 0 ≥ x, and therefore x = 0.
-- this is just antisymmetry for different ≤s : ∀ x y → [ x ≤ y ] → [ y ≤'' x ] → x ≡ y
snd (prop-12 x 0≤x) [∀ε>0∶x<ε] = let x≤0 : [ x ≤ 0f ]
                                     x≤0 0<x = <-irrefl x ([∀ε>0∶x<ε] x 0<x)
                                 in ≤-antisym x 0f x≤0 0≤x

prop-13 x y 0<x+y = +-<-ext 0f 0f x y (subst (λ p → [ p < x + y ]) (sym (+-identity 0f .snd)) 0<x+y)

-- -x = 0 + (-x) < x + (-x) = 0
prop-14 x =
  [ 0f         < x         ] ⇒⟨ +-preserves-< 0f x (- x) ⟩
  [ 0f + (- x) < x + (- x) ] ⇒⟨ subst (λ p → [ 0f - x < p ]) (+-rinv x) ⟩
  [ 0f + (- x) < 0f        ] ⇒⟨ subst (λ p → [ p < 0f ]) (+-identity (- x) .snd) ⟩
  [       - x  < 0f        ] ◼

-- -x = 0 + (-x) < x + (-x) = 0
prop-14' x =
  [ x         < 0f         ] ⇒⟨ +-preserves-< x 0f (- x) ⟩
  [ x + (- x) < 0f + (- x) ] ⇒⟨ subst (λ p → [ x - x < p ]) (+-identity (- x) .snd) ⟩
  [ x + (- x) < (- x)      ] ⇒⟨ subst (λ p → [ p < - x ]) (+-rinv x) ⟩
  [       0f  < (- x)      ] ◼

-- since -z > 0 we have
-- -xz = x(-z) > y(-z) = -yz
-- so -xz + yz + xz > -yz + yz + xz
prop-15 x y z x<y z<0 = (
  [    x         <    y         ] ⇒⟨ ·-preserves-< x y (- z) (prop-14' z z<0) ⟩
  [    x · (- z) <    y · (- z) ] ⇒⟨ subst (λ p → [ p < y · (- z) ]) (RingTheory'.-commutesWithRight-· x z) ⟩
  [ - (x ·    z) <    y · (- z) ] ⇒⟨ subst (λ p → [ -(x · z) < p ]) (RingTheory'.-commutesWithRight-· y z) ⟩
  [ - (x ·    z) < - (y ·    z) ] ⇒⟨ -swaps-< (y · z) (x · z) .snd ⟩
  [    y ·    z  <    x ·    z  ] ◼) x<y

prop-16 x (inl x<0) = (
  [         x  < 0f            ] ⇒⟨ prop-14' x ⟩
  [ 0f         <  - x          ] ⇒⟨ ·-preserves-< 0f (- x) (- x) (prop-14' x x<0) ⟩
  [ 0f · (- x) < (- x) · (- x) ] ⇒⟨ subst (λ p → [ p < (- x) · (- x) ]) (RingTheory'.0-leftNullifies (- x)) ⟩
  [ 0f         < (- x) · (- x) ] ⇒⟨ subst (λ p → [ 0f < p ]) (RingTheory'.-commutesWithRight-· (- x) x) ⟩
  [ 0f         < - ((- x) · x) ] ⇒⟨ subst (λ p → [ 0f < - p ]) (RingTheory'.-commutesWithLeft-· x x) ⟩
  [ 0f         < - - (x · x)   ] ⇒⟨ subst (λ p → [ 0f < p ]) (GroupLemmas'.invInvo (x · x)) ⟩
  [ 0f         < x · x         ] ◼) x<0
prop-16 x (inr 0<x) = (
  [ 0f     < x     ] ⇒⟨ ·-preserves-< 0f x x 0<x ⟩
  [ 0f · x < x · x ] ⇒⟨ subst (λ p → [ p < x · x ]) (RingTheory'.0-leftNullifies x) ⟩
  [ 0f     < x · x ] ◼) 0<x

prop-17 = is-0<1

-- suppose x² < 0. Then ¬(x ≠ 0) by 16; so x = 0 and therefore x² = 0, a contradiction. Hence ¬(x² < 0) and therefore x² ≥ 0.
prop-18 x x²<0 = let ¬x#0 = contraposition (x # 0f) (0f < x · x) (prop-16 x) (<-asym (x · x) 0f x²<0)
                     x≡0  = r2-3 _ _ ¬x#0
                     x²≡0 = (λ i → x≡0 i · x≡0 i) ∙ RingTheory'.0-leftNullifies 0f
                 in transport (λ i → [ ¬ (x²≡0 (~ i) < 0f) ] ) (<-irrefl 0f) x²<0
prop-19 x  0<x x<1 = subst (λ p → [ x · x < p ]) (·-lid x) (·-preserves-< x 1f x 0<x x<1)

prop-20 x -1<x x<1 (x<x² , -x<x²) =
  -- Suppose that - 1 < x < 1 and that (x² > x ∧ x² > -x).
  let -- If x > 0, then x = x (-1) < x² < x(1) = x which contradicts our second assumption. Hence ¬(x > 0) and therefore x ≤ 0.
      argument1 : [ 0f < x ⇒ x · x < x ]
      argument1 0<x = subst (λ p → [ x · x < p ]) (·-identity x .snd) (·-preserves-< x 1f x 0<x x<1)
      x≤0 : [ x ≤ 0f ]
      x≤0 = contraposition (0f < x) (x · x < x) argument1 (<-asym _ _  x<x²)
      -- A similar argument shows that x ≥ 0.
      argument2 : [ x < 0f ⇒ x · x < - x ]
      argument2 x<0 = let 0<-x = subst (λ p → [ p < - x ]) (sym is-0≡-0) (-swaps-< x 0f .fst x<0)
                      in (
                        [  (- 1f) · (- x)  < x · (- x) ] ⇒⟨ subst (λ p → [ p < x · (- x) ]) (RingTheory'.-commutesWithLeft-· 1f (- x)) ⟩
                        [ -(  1f  · (- x)) < x · (- x) ] ⇒⟨ subst (λ p → [ - p < x · (- x) ]) (·-identity (- x) .snd) ⟩
                        [ -(         - x)  < x · (- x) ] ⇒⟨ subst (λ p → [ - - x < p ]) (RingTheory'.-commutesWithRight-· x x) ⟩
                        [ -(         - x)  < -(x · x)  ] ⇒⟨ -swaps-< (x · x) (- x) .snd ⟩
                        [            x · x < - x       ] ◼) (·-preserves-< (- 1f) x (- x) 0<-x -1<x)
      0≤x  : [ 0f ≤ x ]
      0≤x  = contraposition (x < 0f) (x · x < - x) argument2 (<-asym _ _ -x<x²)
      -- whence x = 0.
      x≡0  = ≤-antisym x 0f x≤0 0≤x
      -- But in that case we have -x = x² = x, again a contradiction.
      x<0  = subst (λ p → [   x < p ]) (RingTheory'.0-leftNullifies 0f) (subst (λ p → [   x < p · p ]) x≡0  x<x²)
      -x<0 = subst (λ p → [ - x < p ]) (RingTheory'.0-leftNullifies 0f) (subst (λ p → [ - x < p · p ]) x≡0 -x<x²)
      0<x  = -swaps-< 0f x .snd (subst (λ p → [ - x < p ]) is-0≡-0 -x<0)
  in <-asym _ _ 0<x x<0

-- Either x > 0 or x² > x.
prop-21 x  0<x² = case <-cotrans 0f (x · x) 0<x² x as (0f < x) ⊔ (x < x · x) ⇒ x # 0f of λ
  { (inl 0<x ) → inr 0<x
  -- In the latter case, either x² > -x or -x > x.
  ; (inr x<x²) → case <-cotrans x (x · x) x<x² (- x) as (x < - x) ⊔ (- x < x · x) ⇒ x # 0f of λ
    -- Suppose -x > x. Then x - x > x + x = 2x, so 0 > x.
    { (inl  x<-x) → let x<0 : [ x < 0f ]
                        x<0 = (
                          [ x     < - x          ] ⇒⟨ +-preserves-< x (- x) x ⟩
                          [ x + x < - x + x      ] ⇒⟨ subst (λ p → [ x + x < p ]) (+-inv x .snd) ⟩
                          [ x + x < 0f           ] ⇒⟨ subst (λ p → [ p + p < 0f ]) (sym $ ·-identity x .fst) ⟩
                          [ x · 1f + x · 1f < 0f ] ⇒⟨ subst (λ p → [ p < 0f ]) (sym $ is-dist x 1f 1f .fst) ⟩
                          [ x · (1f + 1f) < 0f   ] ⇒⟨ ·-reflects-<0 x (1f + 1f) (<-trans 0f 1f (1f + 1f) is-0<1 (subst (λ p → [ p < 1f + 1f ]) (+-identity 1f .snd) (+-preserves-< 0f 1f 1f is-0<1))) ⟩
                          [ x < 0f               ] ◼) x<-x
                    in inl x<0
    -- Thus we may assume that x² > x and x² < -x.
    ; (inr -x<x²) → case <-cotrans 0f 1f is-0<1 x as (0f < x) ⊔ (x < 1f) ⇒ x # 0f of λ
      -- then either x > 0 or 1 > x.
      { (inl 0<x) → inr 0<x
      -- In the latter case, if x > -1, then we cotradict 20; so 0 > -1 ≥ x
      ; (inr x<1) → let x≤-1 : [ x ≤ - 1f ]
                        x≤-1 -1<x = prop-20 x -1<x x<1 (x<x² , -x<x²)
                        -1<0 : [ - 1f < 0f ]
                        -1<0 = subst (λ p → [ - 1f < p ]) (sym is-0≡-0) (-swaps-< 0f 1f .fst is-0<1)
                    -- and therefore 0 > x.
                    in inl $ ≤-<-trans _ _ _ x≤-1 -1<0
      }
    }
  }

prop-22 x  0<x     = let instance _ = inr 0<x in it , <-asym _ _ (⁻¹-preserves-sign _ _ 0<x (·-rinv x it))
prop-22' x 0<x     = let instance _ = inr 0<x in it , ⁻¹-preserves-sign _ _ 0<x (·-rinv x it)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- Convenient syntax for equational reasoning
------------------------------------------------------------------------

-- Example use:

-- n*0≡0 : ∀ n → n * 0 ≡ 0
-- n*0≡0 zero    = refl
-- n*0≡0 (suc n) =
--   begin
--     suc n * 0
--   ≈⟨ byDef ⟩
--     n * 0 + 0
--   ≈⟨ n+0≡n _ ⟩
--     n * 0
--   ≈⟨ n*0≡0 n ⟩
--     0
--   ∎

open import Relation.Binary

module Relation.Binary.EqReasoning (s : Setoid) where

open Setoid s
import Relation.Binary.PreorderReasoning as PreR
open PreR preorder public
       renaming ( _∼⟨_⟩_  to _≈⟨_⟩_
                ; _≈⟨_⟩_  to _≡⟨_⟩_
                )

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- In this document we'll show that having `ifix :: ((k -> *) -> k -> *) -> k -> *` is enough to
-- get `fix :: (k -> k) -> k` for any particular `k`.

module IFixIsEnough where

open import Agda.Primitive

-- First, the definition of `IFix`:

{-# NO_POSITIVITY_CHECK #-}
data IFix {α φ} {A : Set α} (F : (A -> Set φ) -> A -> Set φ) (x : A) : Set φ where
  wrap : F (IFix F) x -> IFix F x

-- We'll be calling `F` a pattern functor and `x` an index.

open import Function

-- The simplest non-trivial case of an n-ary higher-kinded `fix` is

-- fix2 :: ((j -> k -> *) -> j -> k -> *) -> j -> k -> *

-- So we'll start from encoding this fixed-point combinator.

module FixProduct where
  -- In Agda it has the following signature:

  Fix₂ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set

  -- One way of getting this type is by going through type-level tuples.

  open import Data.Product

  -- Having (defined for clarity)

  Fixₓ : {A B : Set} -> ((A × B -> Set) -> A × B -> Set) -> A × B -> Set
  Fixₓ = IFix

  -- we can just sprinkle `curry` and `uncurry` in appropriate places and get the desired definition:

  ConciseFix₂ₓ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  ConciseFix₂ₓ F = curry (Fixₓ (uncurry ∘ F ∘ curry))

  -- which after some expansion becomes

  Fix₂ {A} {B} F = λ x y ->
    Fixₓ (λ Rec -> uncurry (F (λ x′ y′ -> Rec (x′ , y′)))) (x , y)

  -- The main idea here is that since `IFix` receives onle one index, we need to somehow package the
  -- two indices we have (`x` and `y`) together to get a single index. And the simplest solution is
  -- just to make a two-element tuple out of `x` and `y`.

  -- However, this simple solution does not apply to vanilla System F-omega, because we do not have
  -- type-level tuples there. Hence some another way of packaging things together is required.

module FixEncodedProduct where
  -- The fact that we only use tuples at the type level suggests the following encoding of them:

  _×̲_ : Set -> Set -> Set₁  -- Type \x\_-- to get ×̲.
  A ×̲ B = (A -> B -> Set) -> Set

  -- Which is just the usual Church encoding (okay-okay, Boehm-Berarducci encoding)

  _Church×_ : ∀ {ρ} -> Set -> Set -> Set (lsuc ρ)
  _Church×_ {ρ} A B = {R : Set ρ} -> (A -> B -> R) -> R

  -- with `R` (not the type of `R`, but `R` itself) instantiated to `Set`.

  -- Here is a combinator that allows to recurse over `A ×̲ B` just like `Fixₓ` from the above
  -- allowed to recurse over `A × B`:

  abstract  -- We'll be marking some things as `abstract` just to get nice output from Agda when
            -- we ask it to normalize things.
    Fixₓ̲ : {A B : Set} -> ((A ×̲ B -> Set) -> A ×̲ B -> Set) -> A ×̲ B -> Set  -- Type \_x\_-- to get ₓ̲.
    Fixₓ̲ = IFix

  -- Now we have `A ×̲ B -> Set` appearing thrice in a type signature. We can simplify this expression:

  -- A ×̲ B -> Set                    ~ (by definition)
  -- ((A -> B -> Set) -> Set) -> Set ~ (see below)
  -- A -> B -> Set

  -- The fact that we can go from `((A -> B -> Set) -> Set) -> Set` to `A -> B -> Set` is related to
  -- the fact that triple negation is equivalent to single negation in a type theory. In fact, we can
  -- go from any `((A -> R) -> R) -> R` to `A -> R` and vice versa as witnessed by

  module TripleNegation where
    tripleToSingle : ∀ {α ρ} {A : Set α} {R : Set ρ}
                   -> (((A -> R) -> R) -> R) -> A -> R
    tripleToSingle h x = h λ f -> f x

    singleToTriple : ∀ {α ρ} {A : Set α} {R : Set ρ}
                   -> (A -> R) -> ((A -> R) -> R) -> R
    singleToTriple f h = h f

  -- Here are the `curry` and `uncurry` combinators then:

  curryₓ̲ : ∀ {α β ρ} {A : Set α} {B : Set β} {R : Set ρ}
         -> (((A -> B -> R) -> R) -> R) -> A -> B -> R
  curryₓ̲ h x y = h λ f -> f x y

  abstract
    uncurryₓ̲ : ∀ {α β ρ} {A : Set α} {B : Set β} {R : Set ρ}
             -> (A -> B -> R) -> ((A -> B -> R) -> R) -> R
    uncurryₓ̲ f h = h f

  -- And the definition of `ConciseFix₂` following the same pattern as the one from the previous section:

  ConciseFix₂ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  ConciseFix₂ F = curryₓ̲ (Fixₓ̲ (uncurryₓ̲ ∘ F ∘ curryₓ̲))

  -- Compare to the previous one:

  -- ConciseFix₂ₓ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  -- ConciseFix₂ₓ F = curry (Fixₓ (uncurry ∘ F ∘ curry))

  -- We can now ask Agda to normalize `ConciseFix₂`. After some alpha-renaming we get

  NormedConciseFix₂ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  NormedConciseFix₂ {A} {B} F = λ x y ->
    Fixₓ̲ (λ Rec -> uncurryₓ̲ (F (λ x′ y′ -> Rec (λ On -> On x′ y′)))) (λ On -> On x y)

  -- which is very similar to what we had previously

  -- Fix₂ₓ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  -- Fix₂ₓ {A} {B} F = λ x y ->
  --   Fixₓ (λ Rec -> uncurry (F (λ x′ y′ -> Rec (x′ , y′)))) (x , y)

  -- except we now have `λ On -> On x y` instead of `(x , y)`. What is this new thing? Well:

  _,̲_ : {A B : Set} -> A -> B -> A ×̲ B  -- Type ,\_-- to get ,̲.
  _,̲_ {A} {B} x y = λ (On : A -> B -> Set) -> On x y

  -- it's just a new way to package `x` and `y` together without ever touching tuples-as-data. Here
  -- we use a function in order to turn two indices into a single one.
  -- `λ On -> On x y` is the Church-encoded version of `(x , y)` (where `_,_` constructs data).

  -- Using `_,̲_` for clarity we arrive at the following:

  Fix₂ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  Fix₂ {A} {B} F = λ x y ->
    Fixₓ̲ (λ Rec -> uncurryₓ̲ (F (λ x′ y′ -> Rec (x′ ,̲ y′)))) (x ,̲ y)

  -- Compare again to the definition from the previous section:

  -- Fix₂ₓ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  -- Fix₂ₓ {A} {B} F = λ x y ->
  --   Fixₓ (λ Rec -> uncurry (F (λ x′ y′ -> Rec (x′ , y′)))) (x , y)

  -- The pattern is clearly the same. But now we do not use any type-level data, only lambda abstractions
  -- and function applications which we do have at the type level in System F-omega, so it all is legal
  -- there.

module Direct where
  -- In this section we'll encode other higher-kinded `Fix`es in addition to `Fix₂` from
  -- the previous section.

  -- `Fix₂` with everything inlined and computed down to normal form looks like this:

  Fix₂ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  Fix₂ {A} {B} F = λ x y ->
    IFix (λ Rec Spine -> Spine (F λ x′ y′ -> Rec (λ On -> On x′ y′))) (λ On -> On x y)

  -- `Fix₃` is the same, just an additional argument `z` (and `z′`) is added here and there:

  Fix₃ : {A B C : Set} -> ((A -> B -> C -> Set) -> A -> B -> C -> Set) -> A -> B -> C -> Set
  Fix₃ F = λ x y z ->
    IFix (λ Rec Spine -> Spine (F λ x′ y′ z′ -> Rec (λ On -> On x′ y′ z′))) (λ On -> On x y z)

  -- Correspondingly, `Fix₁` is `Fix₂` minus `y` (and `y′`):

  Fix₁ : {A : Set} -> ((A -> Set) -> A -> Set) -> A -> Set
  Fix₁ F = λ x ->
    IFix (λ Rec Spine -> Spine (F λ x′ -> Rec (λ On -> On x′))) (λ On -> On x)

  -- But `Fix₁` has the same signature as `IFix`, so we can just define it as

  Fix₁′ : {A : Set} -> ((A -> Set) -> A -> Set) -> A -> Set
  Fix₁′ = IFix

  -- `Fix₀` can be defined in the same manner as `Fix₂`, except we strip off all indices and encode
  -- the empty tuple as `λ On -> On`.

  Fix₀ : (Set -> Set) -> Set
  Fix₀ F =
    IFix (λ Rec spine -> spine (F (Rec (λ On -> On)))) (λ On -> On)

  -- There is another way to define `Fix₀`, we can just pass a dummy argument as an index:

  Fix₀′′ : (Set -> Set) -> Set
  Fix₀′′ F = IFix (λ Rec ⊥ -> F (Rec ⊥)) ((A : Set) -> A)

  -- The argument is never used and is only needed, because we have to provide *some* index.

  -- Another way is to pass `F` itself as an index rather than some dummy argument:

  Fix₀′ : (Set -> Set) -> Set
  Fix₀′ = IFix λ Rec F -> F (Rec F)

  -- This is perhaps the nicest way.

module Generic where
  -- In this section we'll define `FixBy` which generalizes all of `Fix₀`, `Fix₁`, `Fix₂`, etc.

  -- In

  -- Fix₂ : {A B : Set} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
  -- Fix₂ {A} {B} F = λ x y ->
  --   IFix (λ Rec Spine -> Spine (F λ x′ y′ -> Rec (λ On -> On x′ y′))) (λ On -> On x y)

  -- we see that wherever `x` and `y` are bound, they're also packaged by `λ On -> On ...` and the
  -- entire thing is passed to something else. This holds for the inner

  -- λ x′ y′ -> Rec (λ On -> On x′ y′)

  -- as well as for the outer

  -- λ x y -> ... (λ On -> On x y)

  -- This pattern can be easily abstracted:

  FixBy : ∀ {κ φ} {K : Set κ} -> (((K -> Set φ) -> Set φ) -> K) -> (K -> K) -> K
  FixBy WithSpine F = WithSpine (IFix λ Rec Spine -> Spine (F (WithSpine Rec)))

  -- `WithSpine` encapsulates spine construction and feeds constructed spines to a continuation.

  -- Being equipped like that we can easily define an n-ary higher-kinded `fix` for any `n`:

  Fix₀ : ∀ {φ} -> (Set φ -> Set φ) -> Set φ
  Fix₀ = FixBy λ Cont -> Cont λ On -> On

  Fix₁ : ∀ {α φ} {A : Set α} -> ((A -> Set φ) -> A -> Set φ) -> A -> Set φ
  Fix₁ = FixBy λ Cont x -> Cont λ On -> On x

  Fix₂ : ∀ {α β φ} {A : Set α} {B : Set β}
       -> ((A -> B -> Set φ) -> A -> B -> Set φ) -> A -> B -> Set φ
  Fix₂ = FixBy λ Cont x y -> Cont λ On -> On x y

  Fix₃ : ∀ {α β γ φ} {A : Set α} {B : Set β} {C : Set γ}
       -> ((A -> B -> C -> Set φ) -> A -> B -> C -> Set φ) -> A -> B -> C -> Set φ
  Fix₃ = FixBy λ Cont x y z -> Cont λ On -> On x y z

module DirectGenericSame where
  open import Relation.Binary.PropositionalEquality

  -- The 'direct' and 'generic' encodings result in literally the same code. Here are a few examples:

  directIsGeneric₀ : ∀ {F} -> Direct.Fix₀ F ≡ Generic.Fix₀ F
  directIsGeneric₀ = refl

  directIsGeneric₁ : ∀ {A F} {x : A} -> Direct.Fix₁ F x ≡ Generic.Fix₁ F x
  directIsGeneric₁ = refl

  directIsGeneric₂ : ∀ {A B F} {x : A} {y : B} -> Direct.Fix₂ F x y ≡ Generic.Fix₂ F x y
  directIsGeneric₂ = refl

  directIsGeneric₃ : ∀ {A B C F} {x : A} {y : B} {z : C} -> Direct.Fix₃ F x y z ≡ Generic.Fix₃ F x y z
  directIsGeneric₃ = refl

-- Tests:

module Test where
  open import Data.Maybe.Base
  open Generic

  module Nat where
    Nat : Set
    Nat = Fix₀ Maybe

    pattern zero  = wrap nothing
    pattern suc n = wrap (just n)

    elimNat
        : {P : Nat -> Set}
        -> P zero
        -> (∀ n -> P n -> P (suc n))
        -> ∀ n
        -> P n
    elimNat z f  zero   = z
    elimNat z f (suc n) = f n (elimNat z f n)

  module List where
    data ListF (R : Set -> Set) A : Set where
      nilF  : ListF R A
      consF : A -> R A -> ListF R A

    List : Set -> Set
    List = Fix₁ ListF

    pattern []       = wrap nilF
    pattern _∷_ x xs = wrap (consF x xs)

    elimList
        : ∀ {A} {P : List A -> Set}
        -> P []
        -> (∀ x xs -> P xs -> P (x ∷ xs))
        -> ∀ xs
        -> P xs
    elimList z f  []      = z
    elimList z f (x ∷ xs) = f x xs (elimList z f xs)

  module InterleavedList where
    open import Data.Unit.Base
    open import Data.Bool.Base
    open import Data.Nat.Base
    open import Data.Sum.Base
    open import Data.Product

    InterleavedList : Set -> Set -> Set
    InterleavedList = Fix₂ λ Rec A B -> ⊤ ⊎ A × B × Rec B A

    pattern []          = wrap (inj₁ tt)
    pattern cons x y ps = wrap (inj₂ (x , y , ps))

    example_interleavedList : InterleavedList ℕ Bool
    example_interleavedList = cons 0 false ∘′ cons true 1 ∘′ cons 2 false $ []

    elimInterleavedList
        : ∀ {A B} {P : ∀ {A B} -> InterleavedList A B -> Set}
        -> (∀ {A B} -> P {A} {B} [])
        -> (∀ {A B} x y ps -> P {A} {B} ps -> P (cons x y ps))
        -> ∀ ps
        -> P {A} {B} ps
    elimInterleavedList z f  []           = z
    elimInterleavedList z f (cons x y ps) = f x y ps (elimInterleavedList z f ps)

module Unicode where
  -- This file uses the following unicode:
  -- ×̲ 0xD7 \x\_--

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


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

module Cubical.Categories.Presheaf.Properties where

open import Cubical.Categories.Category
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Functor
open import Cubical.Categories.Presheaf.Base
open import Cubical.Categories.Equivalence
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv using (fiber)
open import Cubical.Data.Sigma

import Cubical.Categories.Morphism as Morphism
import Cubical.Categories.Constructions.Slice as Slice
import Cubical.Categories.Constructions.Elements as Elements
import Cubical.Functions.Fibration as Fibration

private
  variable
    ℓ ℓ' : Level
    e e' : Level

-- (PreShv C) / F ≃ᶜ PreShv (∫ᴾ F)
module _ {ℓS : Level} (C : Precategory ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) where
  open Precategory
  open Functor
  open _≃ᶜ_
  open isEquivalence
  open NatTrans
  open NatIso
  open Slice (PreShv C ℓS) F ⦃ isCatPreShv {C = C} ⦄
  open Elements {C = C}

  open Fibration.ForSets

  -- specific case of fiber under natural transformation
  fibersEqIfRepsEqNatTrans : ∀ {A} (ϕ : A ⇒ F) {c x x'} {px : x ≡ x'} {a' : fiber (ϕ ⟦ c ⟧) x} {b' : fiber (ϕ ⟦ c ⟧) x'}
                  → fst a' ≡ fst b'
                  → PathP (λ i → fiber (ϕ ⟦ c ⟧) (px i)) a' b'
  fibersEqIfRepsEqNatTrans ϕ {c} {x} {x'} {px} {a , fiba} {b , fibb} p
    = fibersEqIfRepsEq {isSetB = snd (F ⟅ c ⟆)} (ϕ ⟦ c ⟧) p

  -- ========================================
  --            K : Slice → PreShv
  -- ========================================

  -- action on (slice) objects
  K-ob : (s : SliceCat .ob) → (PreShv (∫ᴾ F) ℓS .ob)
  -- we take (c , x) to the fiber in A of ϕ over x
  K-ob (sliceob {A} ϕ) .F-ob (c , x)
    = (fiber (ϕ ⟦ c ⟧) x)
    , isOfHLevelΣ 2 (snd (A ⟅ c ⟆)) λ _ → isSet→isGroupoid (snd (F ⟅ c ⟆)) _ _
  -- for morphisms, we just apply A ⟪ h ⟫ (plus equality proof)
  K-ob (sliceob {A} ϕ) .F-hom {d , y} {c , x} (h , com) (b , eq)
    = ((A ⟪ h ⟫) b)
    , ((ϕ ⟦ c ⟧) ((A ⟪ h ⟫) b)
    ≡[ i ]⟨ (ϕ .N-hom h) i b ⟩
      (F ⟪ h ⟫) ((ϕ ⟦ d ⟧) b)
    ≡[ i ]⟨ (F ⟪ h ⟫) (eq i) ⟩
      (F ⟪ h ⟫) y
    ≡⟨ sym com ⟩
      x
    ∎)
  -- functoriality follows from functoriality of A
  K-ob (sliceob {A} ϕ) .F-id {x = (c , x)}
    = funExt λ { (a , fibp)
                → fibersEqIfRepsEqNatTrans ϕ (λ i → A .F-id i a) }
  K-ob (sliceob {A} ϕ) .F-seq {x = (c , x)} {(d , y)} {(e , z)} (f' , eq1) (g' , eq2)
    = funExt λ { ( a , fibp )
                  → fibersEqIfRepsEqNatTrans ϕ (λ i → (A .F-seq f' g') i a) }

  -- action on morphisms (in this case, natural transformation)
  K-hom : {sA sB : SliceCat .ob}
        → (ε : SliceCat [ sA , sB ])
        → (K-ob sA) ⇒ (K-ob sB)
  K-hom {sA = s1@(sliceob {A} ϕ)} {s2@(sliceob {B} ψ)} (slicehom ε com) = natTrans η-ob (λ h → funExt (η-hom h))
    where
      P = K-ob s1
      Q = K-ob s2

      -- just apply the natural transformation (ε) we're given
      -- this ensures that we stay in the fiber over x due to the commutativity given by slicenesss
      η-ob : (el : (∫ᴾ F) .ob) → (fst (P ⟅ el ⟆) → fst (Q ⟅ el ⟆) )
      η-ob (c , x) (a , ϕa≡x) = ((ε ⟦ c ⟧) a) , εψ≡ϕ ∙ ϕa≡x
        where
          εψ≡ϕ : (ψ ⟦ c ⟧) ((ε ⟦ c ⟧) a) ≡ (ϕ ⟦ c ⟧) a
          εψ≡ϕ i = ((com i) ⟦ c ⟧) a

      η-hom : ∀ {el1 el2} (h : (∫ᴾ F) [ el1 , el2 ]) (ae : fst (P ⟅ el2 ⟆)) → η-ob el1 ((P ⟪ h ⟫) ae) ≡ (Q ⟪ h ⟫) (η-ob el2 ae)
      η-hom {el1 = (c , x)} {d , y} (h , eqh) (a , eqa)
        = fibersEqIfRepsEqNatTrans ψ (λ i → ε .N-hom h i a)

  K : Functor SliceCat (PreShv (∫ᴾ F) ℓS)
  K .F-ob = K-ob
  K .F-hom = K-hom
  K .F-id = makeNatTransPath
                          (funExt λ cx@(c , x)
                                  → funExt λ aeq@(a , eq)
                                            → fibersEqIfRepsEq {isSetB = snd (F ⟅ c ⟆)} _ refl)
  K .F-seq (slicehom α eqa) (slicehom β eqb)
    = makeNatTransPath
        (funExt λ cx@(c , x)
        → funExt λ aeq@(a , eq)
        → fibersEqIfRepsEq {isSetB = snd (F ⟅ c ⟆)} _ refl)

  -- ========================================
  --            L : PreShv → Slice
  -- ========================================

  -- action on objects (presheaves)
  L-ob : (P : PreShv (∫ᴾ F) ℓS .ob)
        → SliceCat .ob
  L-ob P = sliceob {S-ob = L-ob-ob} L-ob-hom
    where
      -- sends c to the disjoint union of all the images under P
      LF-ob : (c : C .ob) → (SET _) .ob
      LF-ob c = (Σ[ x ∈ fst (F ⟅ c ⟆) ] fst (P ⟅ c , x ⟆)) , isSetΣ (snd (F ⟅ c ⟆)) (λ x → snd (P ⟅ c , x ⟆))

      -- defines a function piecewise over the fibers by applying P
      LF-hom : ∀ {x y}
              → (f : C [ y , x ])
              → (SET _) [ LF-ob x , LF-ob y ]
      LF-hom {x = c} {d} f (x , a) = ((F ⟪ f ⟫) x) , (P ⟪ f , refl ⟫) a

      L-ob-ob : Functor (C ^op) (SET _)
      L-ob-ob .F-ob = LF-ob
      L-ob-ob .F-hom = LF-hom
      L-ob-ob .F-id {x = c}
        = funExt idFunExt
          where
            idFunExt : ∀ (un : fst (LF-ob c))
                      → (LF-hom (C .id c) un) ≡ un
            idFunExt (x , X) = ΣPathP (leftEq , rightEq)
              where
                leftEq : (F ⟪ C .id c ⟫) x ≡ x
                leftEq i = F .F-id i x

                rightEq : PathP (λ i → fst (P ⟅ c , leftEq i ⟆))
                          ((P ⟪ C .id c , refl ⟫) X) X
                rightEq = left ▷ right
                  where
                    -- the id morphism in (∫ᴾ F)
                    ∫id = C .id c , sym (funExt⁻ (F .F-id) x ∙ refl)

                    -- functoriality of P gives us close to what we want
                    right : (P ⟪ ∫id ⟫) X ≡ X
                    right i = P .F-id i X

                    -- but need to do more work to show that (C .id c , refl) ≡ ∫id
                    left : PathP (λ i → fst (P ⟅ c , leftEq i ⟆))
                                  ((P ⟪ C .id c , refl ⟫) X)
                                  ((P ⟪ ∫id ⟫) X)
                    left i = (P ⟪ ∫ᴾhomEq {F = F} (C .id c , refl) ∫id (λ i → (c , leftEq i)) refl refl i ⟫) X
      L-ob-ob .F-seq {x = c} {d} {e} f g
        = funExt seqFunEq
          where
            seqFunEq : ∀ (un : fst (LF-ob c))
                      → (LF-hom (g ⋆⟨ C ⟩ f) un) ≡ (LF-hom g) (LF-hom f un)
            seqFunEq un@(x , X) = ΣPathP (leftEq , rightEq)
              where
                -- the left component is comparing the action of F on x
                -- equality follows from functoriality of F
                -- leftEq : fst (LF-hom (g ⋆⟨ C ⟩ f) un) ≡ fst ((LF-hom g) (LF-hom f un))
                leftEq : (F ⟪ g ⋆⟨ C ⟩ f ⟫) x ≡ (F ⟪ g ⟫) ((F ⟪ f ⟫) x)
                leftEq i = F .F-seq f g i x

                -- on the right, equality also follows from functoriality of P
                -- but it's more complicated because of heterogeneity
                -- since leftEq is not a definitional equality
                rightEq : PathP (λ i → fst (P ⟅ e , leftEq i ⟆))
                                ((P ⟪ g ⋆⟨ C ⟩ f , refl ⟫) X)
                                ((P ⟪ g , refl ⟫) ((P ⟪ f , refl ⟫) X))
                rightEq = left ▷ right
                  where
                    -- functoriality of P only gets us to this weird composition on the left
                    right : (P ⟪ (g , refl) ⋆⟨ (∫ᴾ F) ⟩ (f , refl) ⟫) X ≡ (P ⟪ g , refl ⟫) ((P ⟪ f , refl ⟫) X)
                    right i = P .F-seq (f , refl) (g , refl) i X

                    -- so we need to show that this composition is actually equal to the one we want
                    left : PathP (λ i → fst (P ⟅ e , leftEq i ⟆))
                                  ((P ⟪ g ⋆⟨ C ⟩ f , refl ⟫) X)
                                  ((P ⟪ (g , refl) ⋆⟨ (∫ᴾ F) ⟩ (f , refl) ⟫) X)
                    left i = (P ⟪ ∫ᴾhomEq {F = F} (g ⋆⟨ C ⟩ f , refl) ((g , refl) ⋆⟨ (∫ᴾ F) ⟩ (f , refl)) (λ i → (e , leftEq i)) refl refl i ⟫) X
      L-ob-hom : L-ob-ob ⇒ F
      L-ob-hom .N-ob c (x , _) = x
      L-ob-hom .N-hom f = funExt λ (x , _) → refl

  -- action on morphisms (aka natural transformations between presheaves)
  -- is essentially the identity (plus equality proofs for naturality and slice commutativity)
  L-hom : ∀ {P Q} → PreShv (∫ᴾ F) ℓS [ P , Q ] →
        SliceCat [ L-ob P , L-ob Q ]
  L-hom {P} {Q} η = slicehom arr com
    where
      A = S-ob (L-ob P)
      ϕ = S-arr (L-ob P)
      B = S-ob (L-ob Q)
      ψ = S-arr (L-ob Q)
      arr : A ⇒ B
      arr .N-ob c (x , X) = x , ((η ⟦ c , x ⟧) X)
      arr .N-hom {c} {d} f = funExt natu
        where
          natuType : fst (A ⟅ c ⟆) → Type _
          natuType xX@(x , X) = ((F ⟪ f ⟫) x , (η ⟦ d , (F ⟪ f ⟫) x ⟧) ((P ⟪ f , refl ⟫) X)) ≡ ((F ⟪ f ⟫) x , (Q ⟪ f , refl ⟫) ((η ⟦ c , x ⟧) X))
          natu : ∀ (xX : fst (A ⟅ c ⟆)) → natuType xX
          natu (x , X) = ΣPathP (refl , λ i → (η .N-hom (f , refl) i) X)

      com : arr ⋆⟨ PreShv C ℓS ⟩ ψ ≡ ϕ
      com = makeNatTransPath (funExt comFunExt)
        where
          comFunExt : ∀ (c : C .ob)
                    → (arr ●ᵛ ψ) ⟦ c ⟧ ≡ ϕ ⟦ c ⟧
          comFunExt c = funExt λ x → refl

  L : Functor (PreShv (∫ᴾ F) ℓS) SliceCat
  L .F-ob = L-ob
  L .F-hom = L-hom
  L .F-id {cx} = SliceHom-≡-intro' (makeNatTransPath (funExt λ c → refl))
  L .F-seq {cx} {dy} P Q = SliceHom-≡-intro' (makeNatTransPath (funExt λ c → refl))

  -- ========================================
  --              η : 𝟙 ≅ LK
  -- ========================================

  module _ where
    open Iso
    open Morphism renaming (isIso to isIsoC)
    -- the iso we need
    -- a type is isomorphic to the disjoint union of all its fibers
    typeSectionIso : ∀ {A B : Type ℓS} {isSetB : isSet B} → (ϕ : A → B)
                  → Iso A (Σ[ b ∈ B ] fiber ϕ b)
    typeSectionIso ϕ .fun a = (ϕ a) , (a , refl)
    typeSectionIso ϕ .inv (b , (a , eq)) = a
    typeSectionIso {isSetB = isSetB} ϕ .rightInv (b , (a , eq))
      = ΣPathP (eq
                , ΣPathP (refl
                        , isOfHLevel→isOfHLevelDep 1 (λ b' → isSetB _ _) refl eq eq))
    typeSectionIso ϕ .leftInv a = refl

    -- the natural transformation
    -- just applies typeSectionIso
    ηTrans : 𝟙⟨ SliceCat ⟩ ⇒ (L ∘F K)
    ηTrans .N-ob sob@(sliceob {A} ϕ) = slicehom A⇒LK comm
      where
        LKA = S-ob  (L ⟅ K ⟅ sob ⟆ ⟆)
        ψ = S-arr  (L ⟅ K ⟅ sob ⟆ ⟆)

        A⇒LK : A ⇒ LKA
        A⇒LK .N-ob c = typeSectionIso {isSetB = snd (F ⟅ c ⟆)} (ϕ ⟦ c ⟧) .fun
        A⇒LK .N-hom {c} {d} f = funExt homFunExt
          where
            homFunExt : (x : fst (A ⟅ c ⟆))
                      → (((ϕ ⟦ d ⟧) ((A ⟪ f ⟫) x)) , ((A ⟪ f ⟫) x , refl))  ≡ ((F ⟪ f ⟫) ((ϕ ⟦ c ⟧) x) , (A ⟪ f ⟫) x , _)
            homFunExt x = ΣPathP ((λ i → (ϕ .N-hom f i) x) , fibersEqIfRepsEqNatTrans ϕ refl)

        comm : (A⇒LK) ●ᵛ ψ ≡ ϕ
        comm = makeNatTransPath (funExt λ x → refl)
    ηTrans .N-hom {sliceob {A} α} {sliceob {B} β} (slicehom ϕ eq)
      = SliceHom-≡-intro' (makeNatTransPath (funExt (λ c → funExt λ a → natFunExt c a)))
      where
        natFunExt : ∀ (c : C .ob) (a : fst (A ⟅ c ⟆))
                  → ((β ⟦ c ⟧) ((ϕ ⟦ c ⟧) a) , (ϕ ⟦ c ⟧) a , _) ≡ ((α ⟦ c ⟧) a , (ϕ ⟦ c ⟧) a , _)
        natFunExt c a = ΣPathP ((λ i → ((eq i) ⟦ c ⟧) a) , fibersEqIfRepsEqNatTrans β refl)

    -- isomorphism follows from typeSectionIso
    ηIso : ∀ (sob : SliceCat .ob)
          → isIsoC {C = SliceCat} (ηTrans ⟦ sob ⟧)
    ηIso sob@(sliceob ϕ) = sliceIso _ _ (FUNCTORIso _ _ _ isIsoCf)
      where
        isIsoCf : ∀ (c : C .ob)
                → isIsoC (ηTrans .N-ob sob .S-hom ⟦ c ⟧)
        isIsoCf c = CatIso→isIso (Iso→CatIso (typeSectionIso {isSetB = snd (F ⟅ c ⟆)} (ϕ ⟦ c ⟧)))

  -- ========================================
  --              ε : KL ≅ 𝟙
  -- ========================================

  module _ where
    open Iso
    open Morphism renaming (isIso to isIsoC)
    -- the iso we deserve
    -- says that a type family at x is isomorphic to the fiber over x of that type family packaged up
    typeFiberIso : ∀ {ℓ ℓ'} {A : Type ℓ} {isSetA : isSet A} {x} (B : A → Type ℓ')
                  → Iso (B x) (fiber {A = Σ[ a ∈ A ] B a} (λ (x , _) → x) x)
    typeFiberIso {x = x} _ .fun b = (x , b) , refl
    typeFiberIso _ .inv ((a , b) , eq) = subst _ eq b
    typeFiberIso {isSetA = isSetA} {x = x} B .rightInv ((a , b) , eq)
      = fibersEqIfRepsEq {isSetB = isSetA} (λ (x , _) → x) (ΣPathP (sym eq , symP (transport-filler (λ i → B (eq i)) b)))
    typeFiberIso {x = x} _ .leftInv b = sym (transport-filler refl b)

    -- the natural isomorphism
    -- applies typeFiberIso (inv)
    εTrans : (K ∘F L) ⇒ 𝟙⟨ PreShv (∫ᴾ F) ℓS ⟩
    εTrans .N-ob P = natTrans γ-ob (λ f → funExt (λ a → γ-homFunExt f a))
      where
        KLP = K ⟅ L ⟅ P ⟆ ⟆

        γ-ob : (el : (∫ᴾ F) .ob)
            → (fst (KLP ⟅ el ⟆) → fst (P ⟅ el ⟆) )
        γ-ob el@(c , _) = typeFiberIso {isSetA = snd (F ⟅ c ⟆)} (λ x → fst (P ⟅ c , x ⟆)) .inv

        -- naturality
        -- the annoying part is all the substs
        γ-homFunExt : ∀ {el2 el1} → (f' : (∫ᴾ F) [ el2 , el1 ])
              → (∀ (a : fst (KLP ⟅ el1 ⟆)) → γ-ob el2 ((KLP ⟪ f' ⟫) a) ≡ (P ⟪ f' ⟫) (γ-ob el1 a))
        γ-homFunExt {d , y} {c , x} f'@(f , comm) a@((x' , X') , eq) i
          = comp (λ j → fst (P ⟅ d , eq' j ⟆)) (λ j → λ { (i = i0) → left j
                                                        ; (i = i1) → right j }) ((P ⟪ f , refl ⟫) X')
            where
              -- fiber equality proof that we get from an application of KLP
              eq' = snd ((KLP ⟪ f' ⟫) a)

              -- top right of the commuting diagram
              -- "remove" the subst from the inside
              right : PathP (λ i → fst (P ⟅ d , eq' i ⟆)) ((P ⟪ f , refl ⟫) X') ((P ⟪ f , comm ⟫) (subst _ eq X'))
              right i = (P ⟪ f , refl≡comm i ⟫) (X'≡subst i)
                where
                  refl≡comm : PathP (λ i → (eq' i) ≡ (F ⟪ f ⟫) (eq i)) refl comm
                  refl≡comm = isOfHLevel→isOfHLevelDep 1 (λ (v , w) → snd (F ⟅ d ⟆) v ((F ⟪ f ⟫) w)) refl comm λ i → (eq' i , eq i)

                  X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst _ eq X')
                  X'≡subst = transport-filler (λ i → fst (P ⟅ c , eq i ⟆)) X'

              -- bottom left of the commuting diagram
              -- "remove" the subst from the outside
              left : PathP (λ i → fst (P ⟅ d , eq' i ⟆)) ((P ⟪ f , refl ⟫) X') (subst (λ v → fst (P ⟅ d , v ⟆)) eq' ((P ⟪ f , refl ⟫) X'))
              left = transport-filler (λ i → fst (P ⟅ d , eq' i ⟆)) ((P ⟪ f , refl ⟫) X')
    εTrans .N-hom {P} {Q} α = makeNatTransPath (funExt λ cx → funExt λ xX' → ε-homFunExt cx xX')
      where
        KLP = K ⟅ L ⟅ P ⟆ ⟆

        -- naturality of the above construction applies a similar argument as in `γ-homFunExt`
        ε-homFunExt : ∀ (cx@(c , x) : (∫ᴾ F) .ob) (xX'@((x' , X') , eq) : fst (KLP ⟅ cx ⟆))
                    → subst (λ v → fst (Q ⟅ c , v ⟆)) (snd ((K ⟪ L ⟪ α ⟫ ⟫ ⟦ cx ⟧) xX')) ((α ⟦ c , x' ⟧) X')
                    ≡ (α ⟦ c , x ⟧) (subst _ eq X')
        ε-homFunExt cx@(c , x) xX'@((x' , X') , eq) i
          = comp (λ j → fst (Q ⟅ c , eq j ⟆)) (λ j → λ { (i = i0) → left j
                                                        ; (i = i1) → right j }) ((α ⟦ c , x' ⟧) X')
          where
            eq' : x' ≡ x
            eq' = snd ((K ⟪ L ⟪ α ⟫ ⟫ ⟦ cx ⟧) xX')

            right : PathP (λ i → fst (Q ⟅ c , eq i ⟆)) ((α ⟦ c , x' ⟧) X') ((α ⟦ c , x ⟧) (subst _ eq X'))
            right i = (α ⟦ c , eq i ⟧) (X'≡subst i)
              where
                -- this is exactly the same as the one from before, can refactor?
                X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst _ eq X')
                X'≡subst = transport-filler _ _

            -- extracted out type since need to use in in 'left' body as well
            leftTy : (x' ≡ x) → Type _
            leftTy eq* = PathP (λ i → fst (Q ⟅ c , eq* i ⟆)) ((α ⟦ c , x' ⟧) X') (subst (λ v → fst (Q ⟅ c , v ⟆)) eq' ((α ⟦ c , x' ⟧) X'))

            left : leftTy eq
            left = subst
                    (λ eq* → leftTy eq*)
                    eq'≡eq
                    (transport-filler _ _)
              where
                eq'≡eq : eq' ≡ eq
                eq'≡eq = snd (F ⟅ c ⟆) _ _ eq' eq

    εIso : ∀ (P : PreShv (∫ᴾ F) ℓS .ob)
          → isIsoC {C = PreShv (∫ᴾ F) ℓS} (εTrans ⟦ P ⟧)
    εIso P = FUNCTORIso _ _ _ isIsoC'
      where
        isIsoC' : ∀ (cx : (∫ᴾ F) .ob)
                → isIsoC {C = SET _} ((εTrans ⟦ P ⟧) ⟦ cx ⟧)
        isIsoC' cx@(c , _) = CatIso→isIso (Iso→CatIso (invIso (typeFiberIso {isSetA = snd (F ⟅ c ⟆)} _)))

  -- putting it all together

  preshvSlice≃preshvElem : SliceCat ≃ᶜ PreShv (∫ᴾ F) ℓS
  preshvSlice≃preshvElem .func = K
  preshvSlice≃preshvElem .isEquiv .invFunc = L
  preshvSlice≃preshvElem .isEquiv .η .trans = ηTrans
  preshvSlice≃preshvElem .isEquiv .η .nIso = ηIso
  preshvSlice≃preshvElem .isEquiv .ε .trans = εTrans
  preshvSlice≃preshvElem .isEquiv .ε .nIso = εIso

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
import      Lvl
open import Type

module Data.IndexedList {ℓ ℓᵢ} (T : Type{ℓ}) {I : Type{ℓᵢ}} where

private variable i : I

record Index : Type{ℓᵢ Lvl.⊔ ℓ} where
  constructor intro
  field
    ∅   : I
    _⊰_ : T → I → I

module _ ((intro ∅ᵢ _⊰ᵢ_) : Index) where
  data IndexedList : I → Type{ℓᵢ Lvl.⊔ ℓ} where
    ∅   : IndexedList(∅ᵢ)
    _⊰_ : (x : T) → IndexedList(i) → IndexedList(x ⊰ᵢ i)

  infixr 1000 _⊰_

  private variable ℓₚ : Lvl.Level
  private variable index : Index
  private variable l : IndexedList i

  module _ (P : ∀{i} → IndexedList i → Type{ℓₚ}) where
    elim : P(∅) → (∀{i}(x)(l : IndexedList i) → P(l) → P(x ⊰ l)) → ((l : IndexedList i) → P(l))
    elim base next ∅       = base
    elim base next (x ⊰ l) = next x l (elim base next l)

module LongOper where
  pattern empty = ∅
  pattern prepend elem list = elem ⊰ list
pattern singleton x = x ⊰ ∅

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 _ where

open import Common.Prelude
open import Common.Reflection

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x _ = x

id : ∀ {a} {A : Set a} → A → A
id x = x

first : Tactic
first = give (def (quote const) [])

second : Tactic
second = give (def (quote const) (arg (argInfo visible relevant) (def (quote id) []) ∷ []))

number : Nat
number = unquote first 6 false

boolean : Bool
boolean = unquote second 5 true


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Presheaf where

open import Categories.Category
open import Categories.Functor

Presheaf : ∀ {o ℓ e} {o′ ℓ′ e′} (C : Category o ℓ e) (V : Category o′ ℓ′ e′) → Set _
Presheaf C V = Functor C.op V
  where module C = Category C

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2018-10-13, re issue #3244
--
-- Error should be raised when --no-prop and trying to use Prop
-- (universe-polymorphic or not).

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

data False {ℓ} : Prop ℓ where

-- Expected: Failure with error message


text:
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; []; _∷_; map)
open import Dipsy.Polarity renaming (pos to +; neg to -)

module Dipsy.Form
  (FOp : {n : ℕ} (as : Vec Polarity n) (b : Polarity) → Set)
  where

data Form : Set where
  op : {n : ℕ} {as : Vec Polarity n} {b : Polarity}
     → FOp as b → Vec Form n → Form

max_stars_repo_name: wenkokke/Dipsy

max_issues_repo_name: wenkokke/dipsy

max_forks_repo_name: wenkokke/dipsy


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

module Categories.Category.Monoidal.Structure where

open import Level

open import Categories.Category
open import Categories.Category.Monoidal.Core
open import Categories.Category.Monoidal.Braided
open import Categories.Category.Monoidal.Symmetric

record MonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U        : Category o ℓ e
    monoidal : Monoidal U

  module U        = Category U
  module monoidal = Monoidal monoidal

  open U public
  open monoidal public

record BraidedMonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U         : Category o ℓ e
    monoidal  : Monoidal U
    braided   : Braided monoidal

  module U        = Category U
  module monoidal = Monoidal monoidal
  module braided  = Braided braided

  monoidalCategory : MonoidalCategory o ℓ e
  monoidalCategory = record { U = U ; monoidal = monoidal }

  open U public
  open braided public

record SymmetricMonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U         : Category o ℓ e
    monoidal  : Monoidal U
    symmetric : Symmetric monoidal

  module U         = Category U
  module monoidal  = Monoidal monoidal
  module symmetric = Symmetric symmetric

  braidedMonoidalCategory : BraidedMonoidalCategory o ℓ e
  braidedMonoidalCategory = record
    { U        = U
    ; monoidal = monoidal
    ; braided  = symmetric.braided
    }

  open U public
  open symmetric public
  open BraidedMonoidalCategory braidedMonoidalCategory public
    using (monoidalCategory)

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: TOTBWF/agda-categories

max_forks_repo_name: TOTBWF/agda-categories


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

open import Level

-- This is really a degenerate version of Categories.Category.Instance.One
-- Here SingletonSet is not given an explicit name, it is an alias for Lift o ⊤
module Categories.Category.Instance.SingletonSet where

open import Data.Unit using (⊤; tt)
open import Relation.Binary.PropositionalEquality using (refl)

open import Categories.Category.Instance.Sets
open import Categories.Category.Instance.Setoids
import Categories.Object.Terminal as Term

module _ {o : Level} where
  open Term (Sets o)

  SingletonSet-⊤ : Terminal
  SingletonSet-⊤ = record { ⊤ = Lift o ⊤ ; !-unique = λ _ → refl }

module _ {c ℓ : Level} where
  open Term (Setoids c ℓ)

  SingletonSetoid-⊤ : Terminal
  SingletonSetoid-⊤ = record { ⊤ = record { Carrier = Lift c ⊤ ; _≈_ = λ _ _ → Lift ℓ ⊤ } }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------------
-- Well-founded induction on the relation LTC
------------------------------------------------------------------------------

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

module FOTC.Data.List.WF-Relation.LT-Cons.Induction.Acc.WF-I where

open import FOTC.Base
open import FOTC.Data.List
open import FOTC.Data.List.WF-Relation.LT-Cons
open import FOTC.Data.List.WF-Relation.LT-Cons.PropertiesI
open import FOTC.Data.List.WF-Relation.LT-Length
open import FOTC.Data.List.WF-Relation.LT-Length.Induction.Acc.WF-I
open import FOTC.Induction.WF

-- Parametrized modules
open module S = FOTC.Induction.WF.Subrelation {List} {LTC} LTC→LTL

------------------------------------------------------------------------------
-- The relation LTL is well-founded (using the subrelation combinator).
LTC-wf : WellFounded LTC
LTC-wf Lxs = well-founded LTL-wf Lxs

-- Well-founded induction on the relation LTC.
LTC-wfind : (A : D → Set) →
            (∀ {xs} → List xs → (∀ {ys} → List ys → LTC ys xs → A ys) → A xs) →
            ∀ {xs} → List xs → A xs
LTC-wfind A = WellFoundedInduction LTC-wf

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc