text:
-- notes-01-monday.agda

open import Data.Nat
open import Data.Bool

f : ℕ → ℕ
f x = x + 2

{-
    f 3 =
  = (x + 2)[x:=3] =
  = 3 + 2 =
  = 5
-}

n : ℕ
n = 3

f' : ℕ → ℕ
f' = λ x → x + 2 -- λ function (nameless function)

{-
    f' 3 =
  = (λ x → x + 2) 3 =
  = (x + 2)[x := 3] = -- β-reduction
  = 3 + 2 =
  = 5
-}

g : ℕ → ℕ → ℕ -- currying
g = λ x → (λ y → x + y)

k : (ℕ → ℕ) → ℕ
k h = h 2 + h 3

{-
    k f =
  = f 2 + f 3 =
  = (2 + 2) + (3 + 2) =
  = 4 + 5 =
  = 9
-}

variable
  A B C : Set -- polymorphic: Set actually means "type"

id : A → A
id x = x

_∘_ : (B → C) → (A → B) → (A → C)
f ∘ g = λ x → f (g x)

{-
  A combinator is a high-order function that uses only function application and
  other combinators.
-}
K : A → B → A
K x y = x

S : (A → B → C) → (A → B) → A → C
S f g x = f x (g x)

-- in combinatory logic, every pure λ-term can be translated into S,K
-- λ x → f x = f -- η-equality

max_stars_repo_path: Type Theory/notes-01-monday.agda

max_issues_repo_path: Type Theory/notes-01-monday.agda

max_forks_repo_path: Type Theory/notes-01-monday.agda


text:
------------------------------------------------------------------------
-- Strict ω-continuous functions
------------------------------------------------------------------------

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

module Partiality-monad.Inductive.Strict-omega-continuous where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J hiding (_∘_)
open import Monad equality-with-J

import Partiality-algebra.Strict-omega-continuous as S
open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Eliminators
open import Partiality-monad.Inductive.Monad
open import Partiality-monad.Inductive.Monotone
open import Partiality-monad.Inductive.Omega-continuous

-- Definition of strict ω-continuous functions.

[_⊥→_⊥]-strict : ∀ {a b} → Type a → Type b → Type (a ⊔ b)
[ A ⊥→ B ⊥]-strict = S.[ partiality-algebra A ⟶ partiality-algebra B ]⊥

module [_⊥→_⊥]-strict
         {a b} {A : Type a} {B : Type b}
         (f : [ A ⊥→ B ⊥]-strict) =
         S.[_⟶_]⊥ f

open [_⊥→_⊥]-strict

-- Identity.

id-strict : ∀ {a} {A : Type a} → [ A ⊥→ A ⊥]-strict
id-strict = S.id⊥

-- Composition.

infixr 40 _∘-strict_

_∘-strict_ :
  ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
  [ B ⊥→ C ⊥]-strict → [ A ⊥→ B ⊥]-strict → [ A ⊥→ C ⊥]-strict
_∘-strict_ = S._∘⊥_

-- Equality characterisation lemma for strict ω-continuous functions.

equality-characterisation-strict :
  ∀ {a b} {A : Type a} {B : Type b} {f g : [ A ⊥→ B ⊥]-strict} →
  (∀ x → function f x ≡ function g x) ↔ f ≡ g
equality-characterisation-strict =
  S.equality-characterisation-strict

-- Composition is associative.

∘-strict-assoc :
  ∀ {a b c d} {A : Type a} {B : Type b} {C : Type c} {D : Type d}
  (f : [ C ⊥→ D ⊥]-strict) (g : [ B ⊥→ C ⊥]-strict)
  (h : [ A ⊥→ B ⊥]-strict) →
  f ∘-strict (g ∘-strict h) ≡ (f ∘-strict g) ∘-strict h
∘-strict-assoc = S.∘⊥-assoc

-- Strict ω-continuous functions satisfy an extra monad law.

>>=-∘-return :
  ∀ {a b} {A : Type a} {B : Type b} →
  (f : [ A ⊥→ B ⊥]-strict) →
  ∀ x → x >>=′ (function f ∘ return) ≡ function f x
>>=-∘-return fs = ⊥-rec-⊥
  (record
     { P  = λ x → x >>=′ (f ∘ return) ≡ f x
     ; pe = never >>=′ f ∘ return  ≡⟨ never->>= ⟩
            never                  ≡⟨ sym (strict fs) ⟩∎
            f never                ∎
     ; po = λ x →
              now x >>=′ f ∘ return  ≡⟨ now->>= ⟩∎
              f (now x)              ∎
     ; pl = λ s p →
              ⨆ s >>=′ (f ∘ return)     ≡⟨ ⨆->>= ⟩
              ⨆ ((f ∘ return) ∗-inc s)  ≡⟨ cong ⨆ (_↔_.to equality-characterisation-increasing λ n →

                (f ∘ return) ∗-inc s [ n ]   ≡⟨ p n ⟩∎
                [ f⊑ $ s ]-inc [ n ]         ∎) ⟩

              ⨆ [ f⊑ $ s ]-inc          ≡⟨ sym $ ω-continuous fs s ⟩∎
              f (⨆ s)                   ∎
     ; pp = λ _ → ⊥-is-set
     })
  where
  f⊑ = monotone-function fs
  f  = function fs

-- Strict ω-continuous functions from A ⊥ to B ⊥ are isomorphic to
-- functions from A to B ⊥.

partial↔strict :
  ∀ {a b} {A : Type a} {B : Type b} →
  (A → B ⊥) ↔ [ A ⊥→ B ⊥]-strict
partial↔strict {a} = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f → record
                 { ω-continuous-function = f ∗
                 ; strict                =
                     never >>=′ f  ≡⟨ never->>= ⟩∎
                     never         ∎
                 }
      ; from = λ f x → function f (return x)
      }
    ; right-inverse-of = λ f →
        _↔_.to equality-characterisation-strict λ x →
          x >>=′ (function f ∘ return)  ≡⟨ >>=-∘-return f x ⟩∎
          function f x                  ∎
    }
  ; left-inverse-of = λ f → ⟨ext⟩ λ x →
      return x >>=′ f  ≡⟨ Monad-laws.left-identity x f ⟩∎
      f x              ∎
  }

ext: agda

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
-- The positivity checker should not be run twice for the same mutual
-- block. (If we decide to turn Agda into a total program, then we may
-- want to revise this decision.)

{-# OPTIONS -vtc.pos.graph:5 #-}

module Positivity-once where

A : Set₁

module M where

  B : Set₁
  B = A

A = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- This module introduces built-in types and primitive functions.

module Introduction.Built-in where

{- Agda supports four built-in types :

    - integers,
    - floating point numbers,
    - characters, and
    - strings.

   Note that strings are not defined as lists of characters (as is the case in
   Haskell).

   To use the built-in types they first have to be bound to Agda types. The
   reason for this is that there are no predefined names in Agda.
-}

-- To be able to use the built-in types we first introduce a new set for each
-- built-in type.
postulate
  Int    : Set
  Float  : Set
  Char   : Set
  String : Set

-- We can then bind the built-in types to these new sets using the BUILTIN
-- pragma.
{-# BUILTIN INTEGER Int    #-}
{-# BUILTIN FLOAT   Float  #-}
{-# BUILTIN CHAR    Char   #-}
{-# BUILTIN STRING  String #-}

pi : Float
pi = 3.141593

forAll : Char
forAll = '∀'

hello : String
hello = "Hello World!"

-- There are no integer literals. Instead there are natural number literals. To
-- use these you have to tell the type checker which type to use for natural
-- numbers.

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

{-# BUILTIN NATURAL Nat  #-}

-- Now we can define
fortyTwo : Nat
fortyTwo = 42

-- To anything interesting with values of the built-in types we need functions
-- to manipulate them. To this end Agda provides a set of primitive functions.
-- To gain access to a primitive function one simply declares it. For instance,
-- the function for floating point addition is called primFloatPlus. See below
-- for a complete list of primitive functions. At the moment the name that you
-- bring into scope is always the name of the primitive function. In the future
-- we might allow a primitive function to be introduced with any name.

module FloatPlus where  -- We put it in a module to prevent it from clashing with
                      -- the plus function in the complete list of primitive
                      -- functions below.
  primitive
    primFloatPlus : Float -> Float -> Float

  twoPi = primFloatPlus pi pi

-- Some primitive functions returns elements of non-primitive types. For
-- instance, the integer comparison functions return booleans. To be able to
-- use these functions we have to explain which type to use for booleans.

data Bool : Set where
  false : Bool
  true  : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

module FloatLess where

  primitive
    primFloatLess : Float -> Float -> Bool

-- There are functions to convert a string to a list of characters, so we need
-- to say which list type to use.

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

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  nil  #-}
{-# BUILTIN CONS _::_ #-}

module StringToList where

  primitive
    primStringToList : String -> List Char

-- Below is a partial version of the complete list of primitive
-- functions.

primitive

    -- Integer functions
  primIntegerPlus     : Int -> Int -> Int
  primIntegerMinus    : Int -> Int -> Int
  primIntegerTimes    : Int -> Int -> Int
  primIntegerDiv      : Int -> Int -> Int  -- partial
  primIntegerMod      : Int -> Int -> Int  -- partial
  primIntegerEquality : Int -> Int -> Bool
  primIntegerLess     : Int -> Int -> Bool
  primIntegerAbs      : Int -> Nat
  primNatToInteger    : Nat -> Int
  primShowInteger     : Int -> String

    -- Floating point functions
  primIntegerToFloat : Int -> Float
  primFloatPlus      : Float -> Float -> Float
  primFloatMinus     : Float -> Float -> Float
  primFloatTimes     : Float -> Float -> Float
  primFloatDiv       : Float -> Float -> Float
  primFloatLess      : Float -> Float -> Bool
  primRound          : Float -> Int
  primFloor          : Float -> Int
  primCeiling        : Float -> Int
  primExp            : Float -> Float
  primLog            : Float -> Float     -- partial
  primSin            : Float -> Float
  primShowFloat      : Float -> String

    -- Character functions
  primCharEquality : Char -> Char -> Bool
  primIsLower      : Char -> Bool
  primIsDigit      : Char -> Bool
  primIsAlpha      : Char -> Bool
  primIsSpace      : Char -> Bool
  primIsAscii      : Char -> Bool
  primIsLatin1     : Char -> Bool
  primIsPrint      : Char -> Bool
  primIsHexDigit   : Char -> Bool
  primToUpper      : Char -> Char
  primToLower      : Char -> Char
  primCharToNat    : Char -> Nat
  primNatToChar    : Nat  -> Char -- partial
  primShowChar     : Char -> String

    -- String functions
  primStringToList   : String -> List Char
  primStringFromList : List Char -> String
  primStringAppend   : String -> String -> String
  primStringEquality : String -> String -> Bool
  primShowString     : String -> String

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{- Example by Andreas (2015-09-18) -}

{-# OPTIONS --rewriting --local-confluence-check #-}

open import Common.Prelude
open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

module _ (A : Set) where

  postulate
    plus0p :  ∀{x} → (x + zero) ≡ x

  {-# REWRITE plus0p #-}

max_forks_repo_name: shlevy/agda


text:
module <-trans where

open import Data.Nat using (ℕ)

open import Relations using (_<_; z<s; s<s)

<-trans : ∀ {m n p : ℕ}
  → m < n
  → n < p
    -----
  → m < p
<-trans z<s     (s<s _) = z<s
<-trans (s<s a) (s<s b) = s<s (<-trans a b)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module BTree {A : Set} where

open import Data.List

data BTree : Set where
  leaf : BTree
  node : A → BTree → BTree → BTree

flatten : BTree → List A
flatten leaf = []
flatten (node x l r) = (flatten l) ++ (x ∷ flatten r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module FunctorCat where

open import Categories
open import Functors
open import Naturals

FunctorCat : ∀{a b c d} → Cat {a}{b} → Cat {c}{d} → Cat
FunctorCat C D = record{
  Obj  = Fun C D;
  Hom  = NatT;
  iden = idNat;
  comp = compNat;
  idl  = idlNat;
  idr  = idrNat;
  ass  = λ{_}{_}{_}{_}{α}{β}{η} → assNat {α = α}{β}{η}}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module agdaFunction where

addOne : N -> N
addOne Z = suc Z
addOne (suc a) = suc (suc a)

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
{- modified from a bug report given to me by Ulf Norell, for a
   previous, incorrect version of bt-remove-min. -}

module braun-tree-test where

open import nat
open import list
open import product
open import sum
open import eq

import braun-tree

open braun-tree nat _<_

test : braun-tree 4
test = bt-node 2
        (bt-node 3 (bt-node 6 bt-empty bt-empty (inj₁ refl))
            bt-empty (inj₂ refl))
        (bt-node 4 bt-empty bt-empty (inj₁ refl))
        (inj₂ refl)

{-

to-list : ∀ {n} → braun-tree n → list nat

to-list {zero} _ = []

to-list {suc _} t with bt-remove-min t

to-list {suc _} t | x , t′ = x :: to-list t′

t : braun-tree 5

t = bt-insert 5 (bt-insert 3 (bt-insert 4 (bt-insert 2 (bt-insert 1 bt-empty))))

oops : to-list t ≡ (1 :: 2 :: 3 :: 4 :: 5 :: [])
oops = refl
-}

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --allow-unsolved-metas #-}

module Control.Monad.Free where

open import Prelude

data Free (F : Type a → Type a) (A : Type a) : Type (ℓsuc a) where
  lift : F A → Free F A

  return : A → Free F A
  _>>=_ : Free F B → (B → Free F A) → Free F A

  >>=-idˡ   : isSet A → (f : B → Free F A) (x : B) → (return x >>= f) ≡ f x
  >>=-idʳ   : isSet A → (x : Free F A) → (x >>= return) ≡ x
  >>=-assoc : isSet A → (xs : Free F C) (f : C → Free F B) (g : B → Free F A) → ((xs >>= f) >>= g) ≡ (xs >>= (λ x → f x >>= g))

  trunc : isSet A → isSet (Free F A)

data FreeF (F : Type a → Type a)  (P : ∀ {T} → Free F T → Type b) (A : Type a) : Type (ℓsuc a ℓ⊔ b) where
  liftF : F A → FreeF F P A
  returnF : A → FreeF F P A
  bindF : (xs : Free F B) (P⟨xs⟩ : P xs) (k : B → Free F A) (P⟨∘k⟩ : ∀ x → P (k x)) → FreeF F P A

private
  variable
    F : Type a → Type a
    G : Type b → Type b
    p : Level
    P : ∀ {T} → Free F T → Type p

⟪_⟫ : FreeF F P A → Free F A
⟪ liftF x ⟫ = lift x
⟪ returnF x ⟫ = return x
⟪ bindF xs P⟨xs⟩ k P⟨∘k⟩ ⟫ = xs >>= k

Alg : (F : Type a → Type a) (P : ∀ {T} → Free F T → Type b) → Type _
Alg F P = ∀ {A} → (xs : FreeF F P A) → P ⟪ xs ⟫

record Coherent {a p} {F : Type a → Type a} {P : ∀ {T} → Free F T → Type p} (ψ : Alg F P) : Type (ℓsuc a ℓ⊔ p) where
  field
    c-set : ∀ {T} → isSet T → ∀ xs → isSet (P {T = T} xs) -- possibly needs to be isSet T → isSet (P {T = T} xs)

    c->>=idˡ : ∀ (isb : isSet B) (f : A → Free F B) Pf x → ψ (bindF (return x) (ψ (returnF x)) f Pf) ≡[ i ≔ P (>>=-idˡ isb f x i) ]≡ Pf x
    c->>=idʳ : ∀ (isa : isSet A) (x : Free F A) Px → ψ (bindF x Px return (λ y → ψ (returnF y))) ≡[ i ≔ P (>>=-idʳ isa x i) ]≡ Px
    c->>=assoc : ∀ (isa : isSet A)
      (xs : Free F C) Pxs
      (f : C → Free F B) Pf
      (g : B → Free F A) Pg →
      ψ (bindF (xs >>= f) (ψ (bindF xs Pxs f Pf)) g Pg)
        ≡[ i ≔ P (>>=-assoc isa xs f g i) ]≡
          ψ (bindF xs Pxs (λ x → f x >>= g) λ x → ψ (bindF (f x) (Pf x) g Pg))
open Coherent public

Ψ : (F : Type a → Type a) (P : ∀ {T} → Free F T → Type p) → Type _
Ψ F P = Σ (Alg F P) Coherent

infixr 1 Ψ
syntax Ψ F (λ v → e) = Ψ[ v ⦂ F * ] ⇒ e

Φ : (Type a → Type a) → Type b → Type _
Φ A B = Ψ A (λ _ → B)

⟦_⟧ : Ψ F P → (xs : Free F A) → P xs
⟦ alg ⟧ (lift x) = alg .fst (liftF x)
⟦ alg ⟧ (return x) = alg .fst (returnF x)
⟦ alg ⟧ (xs >>= k) = alg .fst (bindF xs (⟦ alg ⟧ xs) k (⟦ alg ⟧ ∘ k))
⟦ alg ⟧ (>>=-idˡ iss f k i) = alg .snd .c->>=idˡ iss f (⟦ alg ⟧ ∘ f) k i
⟦ alg ⟧ (>>=-idʳ iss xs i) = alg .snd .c->>=idʳ iss xs (⟦ alg ⟧ xs) i
⟦ alg ⟧ (>>=-assoc iss xs f g i) = alg .snd .c->>=assoc iss xs (⟦ alg ⟧ xs) f (⟦ alg ⟧ ∘ f) g (⟦ alg ⟧ ∘ g) i
⟦ alg ⟧ (trunc AIsSet xs ys p q i j) =
  isOfHLevel→isOfHLevelDep 2
    (alg .snd .c-set AIsSet)
    (⟦ alg ⟧ xs) (⟦ alg ⟧ ys)
    (cong ⟦ alg ⟧ p) (cong ⟦ alg ⟧ q)
    (trunc AIsSet xs ys p q)
    i j

prop-coh : {alg : Alg F P} → (∀ {T} → isSet T → ∀ xs → isProp (P {T} xs)) → Coherent alg
prop-coh P-isProp .c-set TIsSet xs = isProp→isSet (P-isProp TIsSet xs)
prop-coh {P = P} P-isProp .c->>=idˡ iss f Pf x =
  toPathP (P-isProp iss (f x) (transp (λ i → P (>>=-idˡ iss f x i)) i0 _) _)
prop-coh {P = P} P-isProp .c->>=idʳ iss x Px =
  toPathP (P-isProp iss x (transp (λ i → P (>>=-idʳ iss x i)) i0 _) _)
prop-coh {P = P} P-isProp .c->>=assoc iss xs Pxs f Pf g Pg =
  toPathP (P-isProp iss (xs >>= (λ x → f x >>= g)) (transp (λ i → P (>>=-assoc iss xs f g i)) i0 _) _)

-- infix 4 _⊜_
-- record AnEquality (F : Type a → Type a) (A : Type a) : Type (ℓsuc a) where
--   constructor _⊜_
--   field lhs rhs : Free F A
-- open AnEquality public

-- EqualityProof-Alg : (F : Type a → Type a) (P : ∀ {A} → Free F A → AnEquality G A) → Type _
-- EqualityProof-Alg F P = Alg F (λ xs → let Pxs = P xs in lhs Pxs ≡ rhs Pxs)

-- eq-coh : {P : ∀ {A} → Free F A → AnEquality G A} {alg : EqualityProof-Alg F P} → Coherent alg
-- eq-coh {P = P} = prop-coh λ xs → let Pxs = P xs in trunc (lhs Pxs) (rhs Pxs)

open import Algebra

module _ {F : Type a → Type a} where
  freeMonad : SetMonad a (ℓsuc a)
  freeMonad .SetMonad.𝐹 = Free F
  freeMonad .SetMonad.isSetMonad .IsSetMonad._>>=_ = _>>=_
  freeMonad .SetMonad.isSetMonad .IsSetMonad.return = return
  freeMonad .SetMonad.isSetMonad .IsSetMonad.>>=-idˡ = >>=-idˡ
  freeMonad .SetMonad.isSetMonad .IsSetMonad.>>=-idʳ = >>=-idʳ
  freeMonad .SetMonad.isSetMonad .IsSetMonad.>>=-assoc = >>=-assoc
  freeMonad .SetMonad.isSetMonad .IsSetMonad.trunc = trunc

module _ {ℓ} (mon : SetMonad ℓ ℓ) where
  module F = SetMonad mon

  open F using (𝐹)

  module _ {G : Type ℓ → Type ℓ} (h : ∀ {T} → G T → 𝐹 T) where
    ⟦_⟧′ : Free G A → 𝐹 A
    ⟦ lift x ⟧′ = h x
    ⟦ return x ⟧′ = F.return x
    ⟦ xs >>= k ⟧′ = ⟦ xs ⟧′ F.>>= λ x → ⟦ k x ⟧′
    ⟦ >>=-idˡ iss f x i ⟧′ = F.>>=-idˡ iss (⟦_⟧′ ∘ f) x i
    ⟦ >>=-idʳ iss xs i ⟧′ = F.>>=-idʳ iss ⟦ xs ⟧′ i
    ⟦ >>=-assoc iss xs f g i ⟧′ = F.>>=-assoc iss ⟦ xs ⟧′ (⟦_⟧′ ∘ f) (⟦_⟧′ ∘ g) i

    ⟦ trunc iss xs ys p q i j ⟧′ =
      isOfHLevel→isOfHLevelDep 2
        (λ xs → F.trunc iss)
        ⟦ xs ⟧′ ⟦ ys ⟧′
        (cong ⟦_⟧′ p) (cong ⟦_⟧′ q)
        (trunc iss xs ys p q)
        i j

    module _ (hom : SetMonadHomomorphism freeMonad {F = G} ⟶ mon) where
      module Hom = SetMonadHomomorphism_⟶_ hom
      open Hom using (f)

      uniq-alg : (inv : ∀ {A : Type _} → (x : G A) → f (lift x) ≡ h x) → Ψ[ xs ⦂ G * ] ⇒ ⟦ xs ⟧′ ≡ f xs
      uniq-alg inv .snd = prop-coh λ iss xs → F.trunc iss _ _
      uniq-alg inv .fst (liftF x) = sym (inv x)
      uniq-alg inv .fst (returnF x) = sym (Hom.return-homo x)
      uniq-alg inv .fst (bindF xs P⟨xs⟩ k P⟨∘k⟩) = cong₂ F._>>=_ P⟨xs⟩ (funExt P⟨∘k⟩) ; Hom.>>=-homo xs k

      uniq : (inv : ∀ {A : Type _} → (x : G A) → f (lift x) ≡ h x) → (xs : Free G A) → ⟦ xs ⟧′ ≡ f xs
      uniq inv = ⟦ uniq-alg inv ⟧

open import Cubical.Foundations.HLevels using (isSetΠ)

module _ {ℓ} (fun : Functor ℓ ℓ) where
  open Functor fun using (map; 𝐹)
  module _ {B : Type ℓ} (BIsSet : isSet B) where

    cata-alg : (𝐹 B → B) → Ψ 𝐹 λ {T} _ → (T → B) → B
    cata-alg ϕ .fst (liftF x) h = ϕ (map h x)
    cata-alg ϕ .fst (returnF x) h = h x
    cata-alg ϕ .fst (bindF _ P⟨xs⟩ _ P⟨∘k⟩) h = P⟨xs⟩ (flip P⟨∘k⟩ h)
    cata-alg ϕ .snd .c-set _ _ = isSetΠ λ _ → BIsSet
    cata-alg ϕ .snd .c->>=idˡ isb f Pf x = refl
    cata-alg ϕ .snd .c->>=idʳ isa x Px = refl
    cata-alg ϕ .snd .c->>=assoc isa xs Pxs f Pf g Pg = refl

    cata : (A → B) → (𝐹 B → B) → Free 𝐹 A → B
    cata h ϕ xs = ⟦ cata-alg ϕ ⟧ xs h

_>>_ : Free F A → Free F B → Free F B
xs >> ys = xs >>= const ys

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module 747Quantifiers where

-- Library

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s) -- added ≤
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) -- added proj₂
open import Data.Sum using (_⊎_; inj₁; inj₂ ) -- added inj₁, inj₂
open import Function using (_∘_) -- added

-- Copied from 747Isomorphism.

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  constructor mk-≃
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_

-- Logical forall is, not surpringly, ∀.
-- Forall elimination is also function application.

∀-elim : ∀ {A : Set} {B : A → Set}
  → (L : ∀ (x : A) → B x)
  → (M : A)
    -----------------
  → B M
∀-elim L M = L M

-- In fact, A → B is nicer syntax for ∀ (_ : A) → B.

-- 747/PLFA exercise: ForAllDistProd (1 point)
-- Show that ∀ distributes over ×.
-- (The special case of → distributes over × was shown in the Connectives chapter.)

∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
  (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
∀-distrib-× = {!!}

-- 747/PLFA exercise: SumForAllImpForAllSum (1 point)
-- Show that a disjunction of foralls implies a forall of disjunctions.

⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
  (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x)  →  ∀ (x : A) → B x ⊎ C x
⊎∀-implies-∀⊎ ∀B⊎∀C = {!!}

-- Existential quantification can be defined as a pair:
-- a witness and a proof that the witness satisfies the property.

data Σ (A : Set) (B : A → Set) : Set where
  ⟨_,_⟩ : (x : A) → B x → Σ A B

-- Some convenient syntax.

Σ-syntax = Σ
infix 2 Σ-syntax
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

-- Unfortunately, we can use the RHS syntax in code,
-- but the LHS will show up in displays of goal and context.

-- This is equivalent to defining a dependent record type.

record Σ′ (A : Set) (B : A → Set) : Set where
  field
    proj₁′ : A
    proj₂′ : B proj₁′

-- By convention, the library uses ∃ when the domain of the bound variable is implicit.

∃ : ∀ {A : Set} (B : A → Set) → Set
∃ {A} B = Σ A B

-- More special syntax.

∃-syntax = ∃
syntax ∃-syntax (λ x → B) = ∃[ x ] B

-- Above we saw two ways of constructing an existential.
-- We eliminate an existential with a function that consumes the
-- witness and proof and reaches a conclusion C.

∃-elim : ∀ {A : Set} {B : A → Set} {C : Set}
  → (∀ x → B x → C)
  → ∃[ x ] B x
    ---------------
  → C
∃-elim f ⟨ x , y ⟩ = f x y

-- This is a generalization of currying (from Connectives).
-- currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)

∀∃-currying : ∀ {A : Set} {B : A → Set} {C : Set}
  → (∀ x → B x → C) ≃ (∃[ x ] B x → C)
_≃_.to ∀∃-currying f ⟨ x , x₁ ⟩ = f x x₁
_≃_.from ∀∃-currying e x x₁ = e ⟨ x , x₁ ⟩
_≃_.from∘to ∀∃-currying f = refl
_≃_.to∘from ∀∃-currying e = extensionality λ { ⟨ x , x₁ ⟩ → refl}

-- 747/PLFA exercise: ExistsDistSum (2 points)
-- Show that existentials distribute over disjunction.

∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
  ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
∃-distrib-⊎ = {!!}

-- 747/PLFA exercise: ExistsProdImpProdExists (1 point)
-- Show that existentials distribute over ×.

∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set} →
  ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
∃×-implies-×∃ = {!!}

-- An existential example: revisiting even/odd.

-- Recall the mutually-recursive definitions of even and odd.

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

-- An number is even iff it is double some other number.
-- A number is odd iff is one plus double some other number.
-- Proofs below.

even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] (    m * 2 ≡ n)
odd-∃  : ∀ {n : ℕ} →  odd n → ∃[ m ] (1 + m * 2 ≡ n)

even-∃ even-zero = ⟨ zero , refl ⟩
even-∃ (even-suc x) with odd-∃ x
even-∃ (even-suc x) | ⟨ x₁ , refl ⟩ = ⟨ suc x₁ , refl ⟩
odd-∃ (odd-suc x) with even-∃ x
odd-∃ (odd-suc x) | ⟨ x₁ , refl ⟩ = ⟨ x₁ , refl ⟩

∃-even : ∀ {n : ℕ} → ∃[ m ] (    m * 2 ≡ n) → even n
∃-odd  : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) →  odd n

∃-even ⟨ zero , refl ⟩ = even-zero
∃-even ⟨ suc x , refl ⟩ = even-suc (∃-odd ⟨ x , refl ⟩)
∃-odd ⟨ x , refl ⟩ = odd-suc (∃-even ⟨ x , refl ⟩)

-- PLFA exercise: what if we write the arithmetic more "naturally"?
-- (Proof gets harder but is still doable).

-- 747/PLFA exercise: AltLE (3 points)
-- An alternate definition of y ≤ z.
-- (Optional exercise: Is this an isomorphism?)

∃-≤ : ∀ {y z : ℕ} → ( (y ≤ z) ⇔ ( ∃[ x ] (y + x ≡ z) ) )
∃-≤ = {!!}

-- The negation of an existential is isomorphic to a universal of a negation.

¬∃≃∀¬ : ∀ {A : Set} {B : A → Set}
  → (¬ ∃[ x ] B x) ≃ ∀ x → ¬ B x
¬∃≃∀¬ = {!!}

-- 747/PLFA exercise: ExistsNegImpNegForAll (1 point)
-- Existence of negation implies negation of universal.

∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
  → ∃[ x ] (¬ B x)
    --------------
  → ¬ (∀ x → B x)
∃¬-implies-¬∀ ∃¬B = {!!}

-- The converse cannot be proved in intuitionistic logic.

-- PLFA exercise: isomorphism between naturals and existence of canonical binary.
-- This is essentially what we did at the end of 747Isomorphism.

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

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

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


text:
-- Andreas, 2014-01-09, illegal double hiding info in typed bindings.

postulate
  ok  : ({A} : Set) → Set
  bad : {{A} : Set} → Set


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

-- Definitions for the types of a polynomial stored in sparse horner
-- normal form.
--
-- These definitions ensure that the polynomial is actually in fully
-- canonical form, with no trailing zeroes, etc.

open import Polynomial.Parameters

module Polynomial.NormalForm.Definition
  {a ℓ}
  (coeffs : RawCoeff a ℓ)
  where

open import Polynomial.NormalForm.InjectionIndex

open import Relation.Nullary using (¬_)
open import Level            using (_⊔_)
open import Data.Empty       using (⊥)
open import Data.Unit        using (⊤)
open import Data.Nat         using (ℕ; suc; zero)
open import Data.Bool        using (T)
open import Data.List.Kleene public

infixl 6 _Δ_
record PowInd {c} (C : Set c) : Set c where
  inductive
  constructor _Δ_
  field
    coeff : C
    pow   : ℕ
open PowInd public

open RawCoeff coeffs

mutual
  -- A Polynomial is indexed by the number of variables it contains.
  infixl 6 _Π_
  record Poly (n : ℕ) : Set a where
    inductive
    constructor _Π_
    field
      {i}  : ℕ
      flat : FlatPoly i
      i≤n  : i ≤′ n

  data FlatPoly : ℕ → Set a where
    Κ : Carrier → FlatPoly zero
    Σ : ∀ {n} → (xs : Coeff n +) → .{xn : Norm xs} → FlatPoly (suc n)

  -- A list of coefficients, paired with the exponent *gap* from the
  -- preceding coefficient. In other words, to represent the
  -- polynomial:
  --
  --   3 + 2x² + 4x⁵ + 2x⁷
  --
  -- We write:
  --
  --   [(3,0),(2,1),(4,2),(2,1)]
  --
  -- Which can be thought of as a representation of the expression:
  --
  --   x⁰ * (3 + x * x¹ * (2 + x * x² * (4 + x * x¹ * (2 + x * 0))))
  --
  -- This is sparse Horner normal form.

  Coeff : ℕ → Set a
  Coeff n = PowInd (NonZero n)

  -- We disallow zeroes in the coefficient list. This condition alone
  -- is enough to ensure a unique representation for any polynomial.
  infixl 6 _≠0
  record NonZero (i : ℕ) : Set a where
    inductive
    constructor _≠0
    field
      poly : Poly i
      .{poly≠0} : ¬ Zero poly

  -- This predicate is used (in its negation) to ensure that no
  -- coefficient is zero, preventing any trailing zeroes.
  Zero : ∀ {n} → Poly n → Set
  Zero (Κ x Π _) = T (Zero-C x)
  Zero (Σ _ Π _) = ⊥

  -- This predicate is used to ensure that all polynomials are in
  -- normal form: if a particular level is constant, than it can
  -- be collapsed into the level below it.
  Norm : ∀ {i} → Coeff i + → Set
  Norm (_ Δ zero  & [])  = ⊥
  Norm (_ Δ zero  & ∹ _) = ⊤
  Norm (_ Δ suc _ & _)   = ⊤
open NonZero public
open Poly public

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


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

open import Sets.EquivalenceRelations
open import Functions.Definition
open import Functions.Lemmas
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas
open import Sets.Cardinality.Finite.Definition
open import LogicalFormulae
open import Groups.Definition
open import Groups.Groups
open import Groups.FiniteGroups.Definition
open import Groups.Abelian.Definition
open import Setoids.Setoids
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Integers.Integers
open import Numbers.Rationals.Definition
open import Numbers.Reals.Definition
open import Rings.Definition
open import Fields.FieldOfFractions.Setoid
open import Semirings.Definition
open import Numbers.Modulo.Definition
open import Numbers.Modulo.Group
open import Fields.Fields
open import Setoids.Subset
open import Rings.IntegralDomains.Definition
open import Fields.Lemmas
open import Rings.Examples.Examples

module LectureNotes.Groups.Lecture1 where

-- Examples

groupExample1 : Group (reflSetoid ℤ) (_+Z_)
groupExample1 = ℤGroup

groupExample2 : Group ℚSetoid (_+Q_)
groupExample2 = Ring.additiveGroup ℚRing

groupExample2' : Group ℝSetoid (_+R_)
groupExample2' = Ring.additiveGroup ℝRing

groupExample3 : Group (reflSetoid ℤ) (_-Z_) → False
groupExample3 record { +Associative = multAssoc } with multAssoc {nonneg 3} {nonneg 2} {nonneg 1}
groupExample3 record { +WellDefined = wellDefined } | ()

negSuccInjective : {a b : ℕ} → (negSucc a ≡ negSucc b) → a ≡ b
negSuccInjective {a} {.a} refl = refl

nonnegInjective : {a b : ℕ} → (nonneg a ≡ nonneg b) → a ≡ b
nonnegInjective {a} {.a} refl = refl

integersTimesNotGroup : Group (reflSetoid ℤ) (_*Z_) → False
integersTimesNotGroup = multiplicationNotGroup ℤRing λ ()

rationalsTimesNotGroup : Group ℚSetoid (_*Q_) → False
rationalsTimesNotGroup = multiplicationNotGroup ℚRing λ ()

QNonzeroGroup : Group _ _
QNonzeroGroup = fieldMultiplicativeGroup ℚField

-- TODO: {1, -1} is a group with *

ℤnIsGroup : (n : ℕ) → (0<n : 0 <N n) → _
ℤnIsGroup n pr = ℤnGroup n pr

-- Groups example 8.9 from lecture 1
data Weird : Set where
  e : Weird
  a : Weird
  b : Weird
  c : Weird

_+W_ : Weird → Weird → Weird
e +W t = t
a +W e = a
a +W a = e
a +W b = c
a +W c = b
b +W e = b
b +W a = c
b +W b = e
b +W c = a
c +W e = c
c +W a = b
c +W b = a
c +W c = e

+WAssoc : {x y z : Weird} → (x +W (y +W z)) ≡ (x +W y) +W z
+WAssoc {e} {y} {z} = refl
+WAssoc {a} {e} {z} = refl
+WAssoc {a} {a} {e} = refl
+WAssoc {a} {a} {a} = refl
+WAssoc {a} {a} {b} = refl
+WAssoc {a} {a} {c} = refl
+WAssoc {a} {b} {e} = refl
+WAssoc {a} {b} {a} = refl
+WAssoc {a} {b} {b} = refl
+WAssoc {a} {b} {c} = refl
+WAssoc {a} {c} {e} = refl
+WAssoc {a} {c} {a} = refl
+WAssoc {a} {c} {b} = refl
+WAssoc {a} {c} {c} = refl
+WAssoc {b} {e} {z} = refl
+WAssoc {b} {a} {e} = refl
+WAssoc {b} {a} {a} = refl
+WAssoc {b} {a} {b} = refl
+WAssoc {b} {a} {c} = refl
+WAssoc {b} {b} {e} = refl
+WAssoc {b} {b} {a} = refl
+WAssoc {b} {b} {b} = refl
+WAssoc {b} {b} {c} = refl
+WAssoc {b} {c} {e} = refl
+WAssoc {b} {c} {a} = refl
+WAssoc {b} {c} {b} = refl
+WAssoc {b} {c} {c} = refl
+WAssoc {c} {e} {z} = refl
+WAssoc {c} {a} {e} = refl
+WAssoc {c} {a} {a} = refl
+WAssoc {c} {a} {b} = refl
+WAssoc {c} {a} {c} = refl
+WAssoc {c} {b} {e} = refl
+WAssoc {c} {b} {a} = refl
+WAssoc {c} {b} {b} = refl
+WAssoc {c} {b} {c} = refl
+WAssoc {c} {c} {e} = refl
+WAssoc {c} {c} {a} = refl
+WAssoc {c} {c} {b} = refl
+WAssoc {c} {c} {c} = refl

weirdGroup : Group (reflSetoid Weird) _+W_
Group.+WellDefined weirdGroup = reflGroupWellDefined
Group.0G weirdGroup = e
Group.inverse weirdGroup t = t
Group.+Associative weirdGroup {r} {s} {t} = +WAssoc {r} {s} {t}
Group.identRight weirdGroup {e} = refl
Group.identRight weirdGroup {a} = refl
Group.identRight weirdGroup {b} = refl
Group.identRight weirdGroup {c} = refl
Group.identLeft weirdGroup {e} = refl
Group.identLeft weirdGroup {a} = refl
Group.identLeft weirdGroup {b} = refl
Group.identLeft weirdGroup {c} = refl
Group.invLeft weirdGroup {e} = refl
Group.invLeft weirdGroup {a} = refl
Group.invLeft weirdGroup {b} = refl
Group.invLeft weirdGroup {c} = refl
Group.invRight weirdGroup {e} = refl
Group.invRight weirdGroup {a} = refl
Group.invRight weirdGroup {b} = refl
Group.invRight weirdGroup {c} = refl

weirdAb : AbelianGroup weirdGroup
AbelianGroup.commutative weirdAb {e} {e} = refl
AbelianGroup.commutative weirdAb {e} {a} = refl
AbelianGroup.commutative weirdAb {e} {b} = refl
AbelianGroup.commutative weirdAb {e} {c} = refl
AbelianGroup.commutative weirdAb {a} {e} = refl
AbelianGroup.commutative weirdAb {a} {a} = refl
AbelianGroup.commutative weirdAb {a} {b} = refl
AbelianGroup.commutative weirdAb {a} {c} = refl
AbelianGroup.commutative weirdAb {b} {e} = refl
AbelianGroup.commutative weirdAb {b} {a} = refl
AbelianGroup.commutative weirdAb {b} {b} = refl
AbelianGroup.commutative weirdAb {b} {c} = refl
AbelianGroup.commutative weirdAb {c} {e} = refl
AbelianGroup.commutative weirdAb {c} {a} = refl
AbelianGroup.commutative weirdAb {c} {b} = refl
AbelianGroup.commutative weirdAb {c} {c} = refl

weirdProjection : Weird → FinSet 4
weirdProjection a = ofNat 0 (le 3 refl)
weirdProjection b = ofNat 1 (le 2 refl)
weirdProjection c = ofNat 2 (le 1 refl)
weirdProjection e = ofNat 3 (le zero refl)

weirdProjectionSurj : Surjection weirdProjection
weirdProjectionSurj fzero = a , refl
weirdProjectionSurj (fsucc fzero) = b , refl
weirdProjectionSurj (fsucc (fsucc fzero)) = c , refl
weirdProjectionSurj (fsucc (fsucc (fsucc fzero))) = e , refl
weirdProjectionSurj (fsucc (fsucc (fsucc (fsucc ()))))

weirdProjectionInj : (x y : Weird) → weirdProjection x ≡ weirdProjection y → Setoid._∼_ (reflSetoid Weird) x y
weirdProjectionInj e e fx=fy = refl
weirdProjectionInj e a ()
weirdProjectionInj e b ()
weirdProjectionInj e c ()
weirdProjectionInj a e ()
weirdProjectionInj a a fx=fy = refl
weirdProjectionInj a b ()
weirdProjectionInj a c ()
weirdProjectionInj b e ()
weirdProjectionInj b a ()
weirdProjectionInj b b fx=fy = refl
weirdProjectionInj b c ()
weirdProjectionInj c e ()
weirdProjectionInj c a ()
weirdProjectionInj c b ()
weirdProjectionInj c c fx=fy = refl

weirdFinite : FiniteGroup weirdGroup (FinSet 4)
SetoidToSet.project (FiniteGroup.toSet weirdFinite) = weirdProjection
SetoidToSet.wellDefined (FiniteGroup.toSet weirdFinite) x y = applyEquality weirdProjection
SetoidToSet.surj (FiniteGroup.toSet weirdFinite) = weirdProjectionSurj
SetoidToSet.inj (FiniteGroup.toSet weirdFinite) = weirdProjectionInj
FiniteSet.size (FiniteGroup.finite weirdFinite) = 4
FiniteSet.mapping (FiniteGroup.finite weirdFinite) = id
FiniteSet.bij (FiniteGroup.finite weirdFinite) = idIsBijective

weirdOrder : groupOrder weirdFinite ≡ 4
weirdOrder = refl


text:
open import Function using (_∘_)
open import Category.Functor
open import Category.Monad
open import Data.Fin as Fin using (Fin) renaming (suc to fs; zero to fz)
import Data.Fin.Properties as FinProps
open import Data.Maybe as Maybe using (Maybe; maybe; just; nothing)
open import Data.Nat as Nat using (ℕ; suc; zero;  _+_; _⊔_)
open import Data.Product using (Σ; ∃; _,_; proj₁; proj₂) renaming (_×_ to _∧_)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec as Vec using (Vec; []; _∷_; head; tail)
open import Data.Vec.Equality as VecEq
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; inspect; [_])

module Unification (Name : ℕ → Set) (decEqName : ∀ {k} (x y : Name k) → Dec (x ≡ y)) where

  open RawFunctor {{...}}
  open RawMonad {{...}} hiding (_<$>_)
  open DecSetoid {{...}} using (_≟_)

  instance MaybeFunctor = Maybe.functor

  instance MaybeMonad = Maybe.monad

  private natDecSetoid = PropEq.decSetoid Nat._≟_
  private finDecSetoid : ∀ {n} → DecSetoid _ _
          finDecSetoid {n} = FinProps.decSetoid n
  private nameDecSetoid : ∀ {k} → DecSetoid _ _
          nameDecSetoid {k} = PropEq.decSetoid (decEqName {k})

  -- defining terms
  data Term (n : ℕ) : Set where
    var : Fin n → Term n
    con : ∀ {k} (s : Name k) → (ts : Vec (Term n) k) → Term n

  -- defining decidable equality on terms
  mutual
    decEqTerm : ∀ {n} → (t₁ t₂ : Term n) → Dec (t₁ ≡ t₂)
    decEqTerm (var  x₁) (var x₂) with x₁ FinProps.≟ x₂
    decEqTerm (var .x₂) (var x₂) | yes refl = yes refl
    decEqTerm (var  x₁) (var x₂) | no x₁≢x₂ = no (x₁≢x₂ ∘ elim)
      where
      elim : ∀ {n} {x y : Fin n}
           → var x ≡ var y → x ≡ y
      elim {n} {x} {.x} refl = refl
    decEqTerm (var _)   (con _ _) = no (λ ())
    decEqTerm (con _ _) (var _)   = no (λ ())
    decEqTerm (con {k₁} s₁ ts₁) (con {k₂} s₂ ts₂) with k₁ Nat.≟ k₂
    decEqTerm (con {k₁} s₁ ts₁) (con {k₂} s₂ ts₂) | no k₁≢k₂ = no (k₁≢k₂ ∘ elim)
      where
      elim : ∀ {n k₁ k₂ s₁ s₂} {ts₁ : Vec (Term n) k₁} {ts₂ : Vec (Term n) k₂}
           → con {n} {k₁} s₁ ts₁ ≡ con {n} {k₂} s₂ ts₂ → k₁ ≡ k₂
      elim {n} {k} {.k} refl = refl
    decEqTerm (con {.k} s₁ ts₁) (con { k} s₂ ts₂) | yes refl with decEqName s₁ s₂
    decEqTerm (con s₁ ts₁) (con s₂ ts₂) | yes refl | no s₁≢s₂ = no (s₁≢s₂ ∘ elim)
      where
      elim : ∀ {n k s₁ s₂} {ts₁ ts₂ : Vec (Term n) k}
           → con s₁ ts₁ ≡ con s₂ ts₂ → s₁ ≡ s₂
      elim {n} {k} {s} {.s} refl = refl
    decEqTerm (con .s ts₁) (con s ts₂) | yes refl | yes refl with decEqVecTerm ts₁ ts₂
    decEqTerm (con .s ts₁) (con s ts₂) | yes refl | yes refl | no ts₁≢ts₂  = no (ts₁≢ts₂ ∘ elim)
      where
      elim : ∀ {n k s} {ts₁ ts₂ : Vec (Term n) k}
           → con s ts₁ ≡ con s ts₂ → ts₁ ≡ ts₂
      elim {n} {k} {s} {ts} {.ts} refl = refl
    decEqTerm (con .s .ts) (con s ts) | yes refl | yes refl | yes refl = yes refl

    decEqVecTerm : ∀ {n k} → (xs ys : Vec (Term n) k) → Dec (xs ≡ ys)
    decEqVecTerm [] [] = yes refl
    decEqVecTerm (x ∷ xs) ( y ∷  ys) with decEqTerm x y | decEqVecTerm xs ys
    decEqVecTerm (x ∷ xs) (.x ∷ .xs) | yes refl | yes refl = yes refl
    decEqVecTerm (x ∷ xs) ( y ∷  ys) | yes _    | no xs≢ys = no (xs≢ys ∘ cong tail)
    decEqVecTerm (x ∷ xs) ( y ∷  ys) | no x≢y   | _        = no (x≢y ∘ cong head)

  termDecSetoid : ∀ {n} → DecSetoid _ _
  termDecSetoid {n} = PropEq.decSetoid (decEqTerm {n})

  -- defining replacement function (written _◂ in McBride, 2003)

  mutual
    replace : ∀ {n m} → (Fin n → Term m) → Term n → Term m
    replace f (var i)  = f i
    replace f (con s ts) = con s (replaceChildren f ts)

    replaceChildren : ∀ {n m k} → (Fin n → Term m) → Vec (Term n) k → Vec (Term m) k
    replaceChildren f []       = []
    replaceChildren f (x ∷ xs) = replace f x ∷ (replaceChildren f xs)

  -- defining replacement composition

  _◇_ : ∀ {m n l} (f : Fin m → Term n) (g : Fin l → Term m) → Fin l → Term n
  _◇_ f g = replace f ∘ g

  -- defining thick and thin

  thin : {n : ℕ} -> Fin (suc n) -> Fin n -> Fin (suc n)
  thin  fz    y      = fs y
  thin (fs x)  fz   = fz
  thin (fs x) (fs y) = fs (thin x y)

  thick : {n : ℕ} -> (x y : Fin (suc n)) -> Maybe (Fin n)
  thick          fz    fz   = nothing
  thick          fz   (fs y) = just y
  thick {Nat.zero}  (fs ()) _
  thick {Nat.suc n} (fs x)  fz   = just fz
  thick {Nat.suc n} (fs x) (fs y) = fs <$> (thick x y)

  -- | defining an occurs check (**check** in McBride, 2003)
  mutual
    check : ∀ {n} (x : Fin (suc n)) (t : Term (suc n)) → Maybe (Term n)
    check x₁ (var x₂)   = var <$> thick x₁ x₂
    check x₁ (con s ts) = con s <$> checkChildren x₁ ts

    checkChildren : ∀ {n k} (x : Fin (suc n)) (ts : Vec (Term (suc n)) k) → Maybe (Vec (Term n) k)
    checkChildren x₁ [] = just []
    checkChildren x₁ (t ∷ ts) = check x₁ t >>= λ t' →
      checkChildren x₁ ts >>= λ ts' → return (t' ∷ ts')

  -- | datatype for substitutions (AList in McBride, 2003)
  data Subst : ℕ → ℕ → Set where
    nil  : ∀ {n}   → Subst n n
    snoc : ∀ {m n} → (s : Subst m n) → (t : Term m) → (x : Fin (suc m)) → Subst (suc m) n

  -- | substitutes t for x (**for** in McBride, 2003)
  _for_ : ∀ {n} (t : Term n) (x : Fin (suc n)) → Fin (suc n) → Term n
  _for_ t x y with thick x y
  _for_ t x y | just y' = var y'
  _for_ t x y | nothing = t

  -- | substitution application (**sub** in McBride, 2003)
  apply : ∀ {m n} → Subst m n → Fin m → Term n
  apply nil = var
  apply (snoc s t x) = (apply s) ◇ (t for x)

  -- | composes two substitutions
  _⊕_ : ∀ {l m n} → Subst m n → Subst l m → Subst l n
  s₁ ⊕ nil = s₁
  s₁ ⊕ (snoc s₂ t x) = snoc (s₁ ⊕ s₂) t x

  flexRigid : ∀ {n} → Fin n → Term n → Maybe (∃ (Subst n))
  flexRigid {zero} () t
  flexRigid {suc n} x t with check x t
  flexRigid {suc n} x t | nothing = nothing
  flexRigid {suc n} x t | just t' = just (n , snoc nil t' x)

  flexFlex : ∀ {n} → (x y : Fin n) → ∃ (Subst n)
  flexFlex {zero} () j
  flexFlex {suc n} x y with thick x y
  flexFlex {suc n} x y | nothing = (suc n , nil)
  flexFlex {suc n} x y | just  z = (n , snoc nil (var z) x)

  mutual
    unifyAcc : ∀ {m} → (t₁ t₂ : Term m) → ∃ (Subst m) → Maybe (∃ (Subst m))
    unifyAcc (con {k₁} s₁ ts₁) (con {k₂} s₂ ts₂) acc with k₁ Nat.≟ k₂
    unifyAcc (con {k₁} s₁ ts₁) (con {k₂} s₂ ts₂) acc | no k₁≢k₂ = nothing
    unifyAcc (con { k} s₁ ts₁) (con {.k} s₂ ts₂) acc | yes refl with decEqName s₁ s₂
    unifyAcc (con { k} s₁ ts₁) (con {.k} s₂ ts₂) acc | yes refl | no s₁≢s₂ = nothing
    unifyAcc (con { k} .s ts₁) (con {.k}  s ts₂) acc | yes refl | yes refl = unifyAccChildren ts₁ ts₂ acc
    unifyAcc (var x₁) (var x₂) (n , nil) = just (flexFlex x₁ x₂)
    unifyAcc (var x₁) t₂       (n , nil) = flexRigid x₁ t₂
    unifyAcc t₁       (var x₂) (n , nil) = flexRigid x₂ t₁
    unifyAcc t₁ t₂ (n , snoc s t' x) =
      ( λ s → proj₁ s , snoc (proj₂ s) t' x )
        <$> unifyAcc (replace (t' for x) t₁) (replace (t' for x) t₂) (n , s)

    unifyAccChildren : ∀ {n k} → (ts₁ ts₂ : Vec (Term n) k) → ∃ (Subst n) → Maybe (∃ (Subst n))
    unifyAccChildren []         []         acc = just acc
    unifyAccChildren (t₁ ∷ ts₁) (t₂ ∷ ts₂) acc = unifyAcc t₁ t₂ acc >>= unifyAccChildren ts₁ ts₂

  unify : ∀ {m} → (t₁ t₂ : Term m) → Maybe (∃ (Subst m))
  unify {m} t₁ t₂ = unifyAcc t₁ t₂ (m , nil)

max_stars_repo_name: wenkokke/FirstOrderUnificationInAgda

max_issues_repo_name: wenkokke/FirstOrderUnificationInAgda

max_forks_repo_name: wenkokke/FirstOrderUnificationInAgda


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

module SL where

open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality

-- Example from: Hofmann and Streicher. The groupoid model refutes
-- uniqueness of identity proofs.
thm₁ : ∀ n → n ≡ 0 ⊎ Σ ℕ (λ n' → n ≡ suc n')
thm₁ zero    = inj₁ refl
thm₁ (suc n) = inj₂ (n , refl)

postulate indℕ : (P : ℕ → Set) → P 0 → (∀ n → P n → P (suc n)) → ∀ n → P n

thm₂ : ∀ n → n ≡ 0 ⊎ Σ ℕ λ n' → n ≡ suc n'
thm₂ = indℕ P P0 is
  where
    P : ℕ → Set
    P m = m ≡ 0 ⊎ Σ ℕ λ m' → m ≡ suc m'

    P0 : P 0
    P0 = inj₁ refl

    is : ∀ m → P m → P (suc m)
    is m _ = inj₂ (m , refl)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Irrelevant where

open import Common.IO
open import Common.Nat
open import Common.Unit

A : Set
A = Nat

record R : Set where
  id : A → A
  id x = x

postulate r : R

id2 : .A → A → A
id2 x y = y

open R

main : IO Unit
main = printNat (id2 10 20) ,,
  printNat (id r 30) ,,
  return unit

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Fin.Subset.Cardinality where
  open import Data.Fin.Subset

  _∖_ : ∀ {n} → Subset n → Subset n → Subset n
  _∖_ {n} a b = a ∩ ∁ b

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


text:
------------------------------------------------------------------------------
-- Properties related with lists
------------------------------------------------------------------------------

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

module FOTC.Data.List.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Conat
open import FOTC.Data.List
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Congruence properties

postulate ++-leftCong : ∀ {xs ys zs} → xs ≡ ys → xs ++ zs ≡ ys ++ zs
{-# ATP prove ++-leftCong #-}

postulate mapCong₂ : ∀ {f xs ys} → xs ≡ ys → map f xs ≡ map f ys
{-# ATP prove mapCong₂ #-}

------------------------------------------------------------------------------
-- Totality properties

++-List : ∀ {xs ys} → List xs → List ys → List (xs ++ ys)
++-List {ys = ys} lnil Lys = prf
  where postulate prf : List ([] ++ ys)
        {-# ATP prove prf #-}

++-List {ys = ys} (lcons x {xs} Lxs) Lys = prf (++-List Lxs Lys)
  where postulate prf : List (xs ++ ys) → List ((x ∷ xs) ++ ys)
        {-# ATP prove prf #-}

map-List : ∀ f {xs} → List xs → List (map f xs)
map-List f lnil = prf
  where postulate prf : List (map f [])
        {-# ATP prove prf #-}
map-List f (lcons x {xs} Lxs) = prf (map-List f Lxs)
  where postulate prf : List (map f xs) → List (map f (x ∷ xs))
        {-# ATP prove prf #-}

rev-List : ∀ {xs ys} → List xs → List ys → List (rev xs ys)
rev-List {ys = ys} lnil Lys = prf
  where postulate prf : List (rev [] ys)
        {-# ATP prove prf #-}
rev-List {ys = ys} (lcons x {xs} Lxs) Lys = prf (rev-List Lxs (lcons x Lys))
  where postulate prf : List (rev xs (x ∷ ys)) → List (rev (x ∷ xs) ys)
        {-# ATP prove prf #-}

postulate reverse-List : ∀ {xs} → List xs → List (reverse xs)
{-# ATP prove reverse-List rev-List #-}

-- Length properties

length-replicate : ∀ x {n} → N n → length (replicate n x) ≡ n
length-replicate x nzero = prf
  where postulate prf : length (replicate zero x) ≡ zero
        {-# ATP prove prf #-}
length-replicate x (nsucc {n} Nn) = prf (length-replicate x Nn)
  where postulate prf : length (replicate n x) ≡ n →
                        length (replicate (succ₁ n) x) ≡ succ₁ n
        {-# ATP prove prf #-}

postulate lg-xs≡∞→lg-x∷xs≡∞ : ∀ x xs → length xs ≡ ∞ → length (x ∷ xs) ≡ ∞
{-# ATP prove lg-xs≡∞→lg-x∷xs≡∞ #-}

-- Append properties

++-leftIdentity : ∀ xs → [] ++ xs ≡ xs
++-leftIdentity = ++-[]

++-rightIdentity : ∀ {xs} → List xs → xs ++ [] ≡ xs
++-rightIdentity lnil = prf
  where postulate prf : [] ++ [] ≡ []
        {-# ATP prove prf #-}

++-rightIdentity (lcons x {xs} Lxs) = prf (++-rightIdentity Lxs)
  where postulate prf : xs ++ [] ≡ xs → (x ∷ xs) ++ [] ≡ x ∷ xs
        {-# ATP prove prf #-}

++-assoc : ∀ {xs} → List xs → ∀ ys zs → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc .{[]} lnil ys zs = prf
  where postulate prf : ([] ++ ys) ++ zs ≡ [] ++ ys ++ zs
        {-# ATP prove prf #-}

++-assoc .{x ∷ xs} (lcons x {xs} Lxs) ys zs = prf (++-assoc Lxs ys zs)
  where postulate prf : (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs →
                        ((x ∷ xs) ++ ys) ++ zs ≡ (x ∷ xs) ++ ys ++ zs
        {-# ATP prove prf #-}

-- Map properties

map-++ : ∀ f {xs} → List xs → ∀ ys → map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++ f lnil ys = prf
  where postulate prf : map f ([] ++ ys) ≡ map f [] ++ map f ys
        {-# ATP prove prf #-}

map-++ f (lcons x {xs} Lxs) ys = prf (map-++ f Lxs ys)
  where postulate prf : map f (xs ++ ys) ≡ map f xs ++ map f ys →
                        map f ((x ∷ xs) ++ ys) ≡ map f (x ∷ xs) ++ map f ys
        {-# ATP prove prf #-}

-- Reverse properties

postulate reverse-[x]≡[x] : ∀ x → reverse (x ∷ []) ≡ x ∷ []
{-# ATP prove reverse-[x]≡[x] #-}

rev-++ : ∀ {xs} → List xs → ∀ ys → rev xs ys ≡ rev xs [] ++ ys
rev-++ lnil ys = prf
  where postulate prf : rev [] ys ≡ rev [] [] ++ ys
        {-# ATP prove prf #-}
rev-++ (lcons x {xs} Lxs) ys = prf (rev-++ Lxs (x ∷ ys)) (rev-++ Lxs (x ∷ []))
  where postulate prf : rev xs (x ∷ ys) ≡ rev xs [] ++ x ∷ ys →
                        rev xs (x ∷ []) ≡ rev xs [] ++ x ∷ [] →
                        rev (x ∷ xs) ys ≡ rev (x ∷ xs) [] ++ ys
        {-# ATP prove prf ++-assoc rev-List #-}

reverse-++ : ∀ {xs ys} → List xs → List ys →
             reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ {ys = ys} lnil Lys = prf
  where postulate prf : reverse ([] ++ ys) ≡ reverse ys ++ reverse []
        {-# ATP prove prf ++-rightIdentity reverse-List #-}

reverse-++ (lcons x {xs} Lxs) lnil = prf
  where
  postulate prf : reverse ((x ∷ xs) ++ []) ≡ reverse [] ++ reverse (x ∷ xs)
  {-# ATP prove prf ++-rightIdentity #-}

reverse-++ (lcons x {xs} Lxs) (lcons y {ys} Lys) =
  prf (reverse-++ Lxs (lcons y Lys))
  where
  postulate prf : reverse (xs ++ y ∷ ys) ≡ reverse (y ∷ ys) ++
                                           reverse xs →
                  reverse ((x ∷ xs) ++ y ∷ ys) ≡ reverse (y ∷ ys) ++
                                                 reverse (x ∷ xs)
  {-# ATP prove prf reverse-List ++-List rev-++ ++-assoc #-}

reverse-∷ : ∀ x {ys} → List ys →
            reverse (x ∷ ys) ≡ reverse ys ++ (x ∷ [])
reverse-∷ x lnil = prf
  where postulate prf : reverse (x ∷ []) ≡ reverse [] ++ x ∷ []
        {-# ATP prove prf #-}

reverse-∷ x (lcons y {ys} Lys) = prf
  where postulate prf : reverse (x ∷ y ∷ ys) ≡ reverse (y ∷ ys) ++ x ∷ []
        {-# ATP prove prf reverse-[x]≡[x] reverse-++ #-}

reverse-involutive : ∀ {xs} → List xs → reverse (reverse xs) ≡ xs
reverse-involutive lnil = prf
  where postulate prf : reverse (reverse []) ≡ []
        {-# ATP prove prf #-}

reverse-involutive (lcons x {xs} Lxs) = prf (reverse-involutive Lxs)
  where
  postulate prf : reverse (reverse xs) ≡ xs →
                  reverse (reverse (x ∷ xs)) ≡ x ∷ xs
  {-# ATP prove prf rev-List reverse-++ ++-List ++-rightIdentity #-}


text:
module Issue3188.Issue3188a where

postulate String : Set
{-# BUILTIN STRING String #-}


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Reducibility {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties

open import Tools.Product

-- Valid types are reducible.
reducibleᵛ : ∀ {A Γ l}
             ([Γ] : ⊩ᵛ Γ)
           → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
           → Γ ⊩⟨ l ⟩ A
reducibleᵛ [Γ] [A] =
  let ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevance′ (subst-id _) (proj₁ ([A] ⊢Γ [id]))

-- Valid type equality is reducible.
reducibleEqᵛ : ∀ {A B Γ l}
               ([Γ] : ⊩ᵛ Γ)
               ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
             → Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A]
             → Γ ⊩⟨ l ⟩ A ≡ B / reducibleᵛ [Γ] [A]
reducibleEqᵛ {A = A} [Γ] [A] [A≡B] =
  let [σA] = reducibleᵛ {A = A} [Γ] [A]
      ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevanceEq″ (subst-id _) (subst-id _)
                      (proj₁ ([A] ⊢Γ [id])) [σA] ([A≡B] ⊢Γ [id])

-- Valid terms are reducible.
reducibleTermᵛ : ∀ {t A Γ l}
                 ([Γ] : ⊩ᵛ Γ)
                 ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
               → Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A]
               → Γ ⊩⟨ l ⟩ t ∷ A / reducibleᵛ [Γ] [A]
reducibleTermᵛ {A = A} [Γ] [A] [t] =
  let [σA] = reducibleᵛ {A = A} [Γ] [A]
      ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevanceTerm″ (subst-id _) (subst-id _)
                        (proj₁ ([A] ⊢Γ [id])) [σA] (proj₁ ([t] ⊢Γ [id]))

-- Valid term equality is reducible.
reducibleEqTermᵛ : ∀ {t u A Γ l}
                   ([Γ] : ⊩ᵛ Γ)
                   ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
                 → Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A]
                 → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / reducibleᵛ [Γ] [A]
reducibleEqTermᵛ {A = A} [Γ] [A] [t≡u] =
  let [σA] = reducibleᵛ {A = A} [Γ] [A]
      ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevanceEqTerm″ (subst-id _) (subst-id _) (subst-id _)
                          (proj₁ ([A] ⊢Γ [id])) [σA] ([t≡u] ⊢Γ [id])


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

module Cubical.HITs.DunceCap where

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

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Snd {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.Introductions.Fst

open import Tools.Product
import Tools.PropositionalEquality as PE

snd-subst*′ : ∀ {Γ l l′ F G t t′}
             ([F] : Γ ⊩⟨ l ⟩ F)
             ([ΣFG] : Γ ⊩⟨ l′ ⟩B⟨ BΣ ⟩ Σ F ▹ G)
             ([t′] : Γ ⊩⟨ l′ ⟩ t′ ∷ Σ F ▹ G / B-intr BΣ [ΣFG])
             → Γ ⊢ t ⇒* t′ ∷ Σ F ▹ G
             → Γ ⊢ snd t ⇒* snd t′ ∷ G [ fst t ]
snd-subst*′ [F] (noemb (Bᵣ F G D ⊢F ⊢G A≡A [F]₁ [G] G-ext)) _ (id x) with
              B-PE-injectivity BΣ (whnfRed* (red D) Σₙ)
... | PE.refl , PE.refl = id (sndⱼ ⊢F ⊢G x)
snd-subst*′ {Γ = Γ} {F = F} {G = G} {t = t} {t′ = t″} [F]
            [ΣFG]₀@(noemb (Bᵣ F₁ G₁ D ⊢F ⊢G A≡A [F]₁ [G] G-ext))
            [t″]
            t⇒*t″@(_⇨_ {t′ = t′} t⇒t′ t′⇒*t″) with
              B-PE-injectivity BΣ (whnfRed* (red D) Σₙ)
... | PE.refl , PE.refl =
  let [ΣFG] = B-intr BΣ [ΣFG]₀
      [t] , _ = redSubst*Term t⇒*t″ [ΣFG] [t″]
      [t′] , _ = redSubst*Term t′⇒*t″ [ΣFG] [t″]
      [t≡t′] : Γ ⊩⟨ _ ⟩ t ≡ t′ ∷ Σ F ▹ G / [ΣFG]
      [t≡t′] = proj₂ (redSubstTerm t⇒t′ [ΣFG] [t′])
      [fstt] : Γ ⊩⟨ _ ⟩ fst t ∷ F / [F]
      [fstt] = fst″ [F] [ΣFG] [t]
      [fstt′] : Γ ⊩⟨ _ ⟩ fst t′ ∷ F / [F]
      [fstt′] = fst″ [F] [ΣFG] [t′]
      [Gfstt] : Γ ⊩⟨ _ ⟩ G [ fst t ]
      [Gfstt] = substSΠ₁ BΣ [ΣFG] [F] [fstt]
      [Gfstt′] : Γ ⊩⟨ _ ⟩ G [ fst t′ ]
      [Gfstt′] = substSΠ₁ BΣ [ΣFG] [F] [fstt′]
      [fstt′≡fstt] : Γ ⊩⟨ _ ⟩ fst t′ ≡ fst t ∷ F / [F]
      [fstt′≡fstt] = symEqTerm [F] (fst-cong″ [F] [ΣFG] [t≡t′])
      [Gfstt′≡Gfstt] : Γ ⊩⟨ _ ⟩ G [ fst t′ ] ≡ G [ fst t ] / [Gfstt′]
      [Gfstt′≡Gfstt] = substSΠ₂ BΣ [ΣFG] (reflEq [ΣFG]) [F] [F] [fstt′] [fstt] [fstt′≡fstt] [Gfstt′] [Gfstt]
  in  snd-subst ⊢F ⊢G t⇒t′ ⇨ conv* (snd-subst*′ [F] [ΣFG]₀ [t″] t′⇒*t″)
                                               (≅-eq (escapeEq [Gfstt′] [Gfstt′≡Gfstt]))
snd-subst*′ [F] (emb 0<1 x) = snd-subst*′ [F] x

-- NOTE this has a horrible interface (and implementation)
snd-subst* : ∀ {Γ l l′ F G t t′}
             ([F] : Γ ⊩⟨ l ⟩ F)
             ([ΣFG] : Γ ⊩⟨ l′ ⟩ Σ F ▹ G)
             ([t′] : Γ ⊩⟨ l′ ⟩ t′ ∷ Σ F ▹ G / [ΣFG])
             → Γ ⊢ t ⇒* t′ ∷ Σ F ▹ G
             → Γ ⊢ snd t ⇒* snd t′ ∷ G [ fst t ]
snd-subst* [F] [ΣFG] [t′] t⇒*t′ =
  let [t′]′ = irrelevanceTerm [ΣFG] (B-intr BΣ (B-elim BΣ [ΣFG])) [t′]
  in  snd-subst*′ [F] (B-elim BΣ [ΣFG]) [t′]′ t⇒*t′

snd′ : ∀ {F G t Γ l l′}
       ([ΣFG] : Γ ⊩⟨ l ⟩B⟨ BΣ ⟩ Σ F ▹ G)
       ([t] : Γ ⊩⟨ l ⟩ t ∷ Σ F ▹ G / B-intr BΣ [ΣFG])
       ([Gfst] : Γ ⊩⟨ l′ ⟩ G [ fst t ])
       → Γ ⊩⟨ l′ ⟩ snd t ∷ G [ fst t ] / [Gfst]
snd′ {F = F} {G = G} {t = t} {Γ = Γ} {l = l} {l′ = l′}
     [ΣFG]@(noemb (Bᵣ F' G' D ⊢F ⊢G A≡A [F'] [G'] G-ext))
     [t]@(Σₜ p d pProd p≅p [fstp] [sndp]) [Gfst] with
       B-PE-injectivity BΣ (whnfRed* (red D) Σₙ)
... | PE.refl , PE.refl =
  let ⊢Γ = wf ⊢F
      [p] = Σₜ p (idRedTerm:*: (⊢u-redₜ d)) pProd p≅p [fstp] [sndp]

      [fstt] , [fstt≡fstp] = redSubst*Term (PE.subst (λ x → Γ ⊢ fst t ⇒* fst p ∷ x)
                                                     (PE.sym (wk-id F))
                                                     (fst-subst* ⊢F ⊢G (redₜ d)))
                                           ([F'] id ⊢Γ) [fstp]

      [Gfstt] = [G'] id ⊢Γ [fstt]
      [Gfstp] = [G'] id ⊢Γ [fstp]
      [Gfstt≡Gfstp] = G-ext id ⊢Γ [fstt] [fstp] [fstt≡fstp]

      [sndp] = convTerm₂ [Gfstt] [Gfstp] [Gfstt≡Gfstp] [sndp]

      [sndp] : Γ ⊩⟨ l′ ⟩ snd p ∷ G [ fst t ] / [Gfst]
      [sndp] = irrelevanceTerm′ (PE.cong (λ x → x [ fst t ]) (wk-lift-id G))
                                [Gfstt] [Gfst] [sndp]
  in  proj₁ (redSubst*Term (snd-subst* (PE.subst (λ x → Γ ⊩⟨ l ⟩ x) (wk-id F) ([F'] id ⊢Γ))
                                       (B-intr BΣ [ΣFG])
                                       [p]
                                       (redₜ d))
                           [Gfst]
                           [sndp])
snd′ (emb 0<1 x) = snd′ x

snd″ : ∀ {F G t Γ l l′}
       ([ΣFG] : Γ ⊩⟨ l ⟩ Σ F ▹ G)
       ([t] : Γ ⊩⟨ l ⟩ t ∷ Σ F ▹ G / [ΣFG])
       ([Gfst] : Γ ⊩⟨ l′ ⟩ G [ fst t ])
       → Γ ⊩⟨ l′ ⟩ snd t ∷ G [ fst t ] / [Gfst]
snd″ {t = t} {Γ = Γ} {l = l} [ΣFG] [t] [Gfst] =
  let [t]′ = irrelevanceTerm [ΣFG] (B-intr BΣ (Σ-elim [ΣFG])) [t]
  in  snd′ (Σ-elim [ΣFG]) [t]′ [Gfst]

snd-cong′ : ∀ {F G t t′ Γ l l′}
            ([ΣFG] : Γ ⊩⟨ l ⟩B⟨ BΣ ⟩ Σ F ▹ G)
            ([t] : Γ ⊩⟨ l ⟩ t ∷ Σ F ▹ G / B-intr BΣ [ΣFG])
            ([t′] : Γ ⊩⟨ l ⟩ t′ ∷ Σ F ▹ G / B-intr BΣ [ΣFG])
            ([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Σ F ▹ G / B-intr BΣ [ΣFG])
            ([Gfst] : Γ ⊩⟨ l′ ⟩ G [ fst t ])
            → Γ ⊩⟨ l′ ⟩ snd t ≡ snd t′ ∷ G [ fst t ] / [Gfst]
snd-cong′ {F} {G} {t} {t′} {Γ} {l} {l′}
          [ΣFG]@(noemb (Bᵣ F' G' D ⊢F ⊢G A≡A [F] [G] G-ext))
          [t]@(Σₜ p d pProd p≅p [fstp] [sndp])
          [t′]@(Σₜ p′ d′ pProd′ p′≅p′ [fstp′] [sndp′])
          [t≡t′]@(Σₜ₌ p₁ p′₁ d₁ d′₁ pProd₁ pProd′₁ p≅p′ [t]₁ [t′]₁ [fstp]₁ [fstp′]₁ [fst≡] [snd≡])
          [Gfst] with
            B-PE-injectivity BΣ (whnfRed* (red D) Σₙ)
          | whrDet*Term (redₜ d , productWhnf pProd) (redₜ d₁ , productWhnf pProd₁)
          | whrDet*Term (redₜ d′ , productWhnf pProd′) (redₜ d′₁ , productWhnf pProd′₁)
... | PE.refl , PE.refl | PE.refl | PE.refl =
  let ⊢Γ = wf ⊢F
      [p] : Γ ⊩⟨ l ⟩ p ∷ Σ F ▹ G / B-intr BΣ [ΣFG]
      [p] = Σₜ p (idRedTerm:*: (⊢u-redₜ d)) pProd p≅p [fstp] [sndp]
      [p′] : Γ ⊩⟨ l ⟩ p′ ∷ Σ F ▹ G / B-intr BΣ [ΣFG]
      [p′] = Σₜ p′ (idRedTerm:*: (⊢u-redₜ d′)) pProd′ p′≅p′ [fstp′] [sndp′]
      [F]′ = irrelevance′ (wk-id F) ([F] id ⊢Γ)

      [fstt] , [fstt≡fstp] = redSubst*Term (PE.subst (λ x → Γ ⊢ fst t ⇒* fst p ∷ x)
                                                     (PE.sym (wk-id F))
                                                     (fst-subst* ⊢F ⊢G (redₜ d)))
                                           ([F] id ⊢Γ) [fstp]
      [Gfstt≡Gfstp] = G-ext id ⊢Γ [fstt] [fstp] [fstt≡fstp]

      [sndp]′ : Γ ⊩⟨ l ⟩ snd p ∷ U.wk (lift id) G [ fst t ] / [G] id ⊢Γ [fstt]
      [sndp]′ = convTerm₂ ([G] id ⊢Γ [fstt]) ([G] id ⊢Γ [fstp]) [Gfstt≡Gfstp] [sndp]
      sndt⇒*sndp = snd-subst* [F]′ (B-intr BΣ [ΣFG]) [p] (redₜ d)
      [sndp]″ = irrelevanceTerm′ (PE.cong (λ x → x [ fst t ]) (wk-lift-id G))
                                 ([G] id ⊢Γ [fstt]) [Gfst]
                                 [sndp]′
      [sndt≡sndp] : Γ ⊩⟨ l′ ⟩ snd t ≡ snd p ∷ G [ fst t ] / [Gfst]
      [sndt≡sndp] = proj₂ (redSubst*Term sndt⇒*sndp [Gfst] [sndp]″)

      [snd≡]′ = convEqTerm₂ ([G] id ⊢Γ [fstt]) ([G] id ⊢Γ [fstp]₁) [Gfstt≡Gfstp] [snd≡]
      [sndp≡sndp′] : Γ ⊩⟨ l′ ⟩ snd p ≡ snd p′ ∷ G [ fst t ] / [Gfst]
      [sndp≡sndp′] = irrelevanceEqTerm′ (PE.cong (λ x → x [ fst t ]) (wk-lift-id G))
                                        ([G] id ⊢Γ [fstt]) [Gfst]
                                        [snd≡]′

      [fstt′] , [fstt′≡fstp′] = redSubst*Term (PE.subst (λ x → Γ ⊢ fst t′ ⇒* fst p′ ∷ x)
                                                     (PE.sym (wk-id F))
                                                     (fst-subst* ⊢F ⊢G (redₜ d′)))
                                           ([F] id ⊢Γ) [fstp′]
      [fstt≡fstt′] = irrelevanceEqTerm′ (PE.sym (wk-id F))
                                        [F]′ ([F] id ⊢Γ)
                                        (fst-cong′ [F]′ [ΣFG] [t≡t′])
      [fstt≡fstp′] = transEqTerm ([F] id ⊢Γ) [fstt≡fstt′] [fstt′≡fstp′]
      [Gfstt≡Gfstp′] = G-ext id ⊢Γ [fstt] [fstp′] [fstt≡fstp′]
      [sndp′]′ : Γ ⊩⟨ l ⟩ snd p′ ∷ U.wk (lift id) G [ fst t ] / [G] id ⊢Γ [fstt]
      [sndp′]′ = convTerm₂ ([G] id ⊢Γ [fstt]) ([G] id ⊢Γ [fstp′]) [Gfstt≡Gfstp′] [sndp′]
      [sndp′]″ = irrelevanceTerm′ (PE.cong (λ x → x [ fst t ]) (wk-lift-id G))
                                  ([G] id ⊢Γ [fstt]) [Gfst]
                                  [sndp′]′
      [Gfstt]′ = irrelevance′ (PE.cong (λ x → x [ fst t ]) (wk-lift-id G))
                              ([G] id ⊢Γ [fstt])
      [Gfstt≡Gfstt′] = irrelevanceEq″ (PE.cong (λ x → x [ fst t ]) (wk-lift-id G))
                                      (PE.cong (λ x → x [ fst t′ ]) (wk-lift-id G))
                                      ([G] id ⊢Γ [fstt]) [Gfstt]′
                                      (G-ext id ⊢Γ [fstt] [fstt′] [fstt≡fstt′])
      sndt′⇒*sndp′ : Γ ⊢ snd t′ ⇒* snd p′ ∷ G [ fst t ]
      sndt′⇒*sndp′ = conv* (snd-subst* [F]′ (B-intr BΣ [ΣFG]) [p′] (redₜ d′))
                           (≅-eq (≅-sym (escapeEq [Gfstt]′ [Gfstt≡Gfstt′])))
      [sndt′≡sndp′] : Γ ⊩⟨ l′ ⟩ snd t′ ≡ snd p′ ∷ G [ fst t ] / [Gfst]
      [sndt′≡sndp′] = proj₂ (redSubst*Term sndt′⇒*sndp′ [Gfst] [sndp′]″)

  in  transEqTerm [Gfst] [sndt≡sndp] (transEqTerm [Gfst] [sndp≡sndp′] (symEqTerm [Gfst] [sndt′≡sndp′]))
snd-cong′ {F} {G} (emb 0<1 x) = snd-cong′ x

snd-cong″ : ∀ {F G t t′ Γ l l′}
            ([ΣFG] : Γ ⊩⟨ l ⟩ Σ F ▹ G)
            ([t] : Γ ⊩⟨ l ⟩ t ∷ Σ F ▹ G / [ΣFG])
            ([t′] : Γ ⊩⟨ l ⟩ t′ ∷ Σ F ▹ G / [ΣFG])
            ([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Σ F ▹ G / [ΣFG])
            ([Gfst] : Γ ⊩⟨ l′ ⟩ G [ fst t ])
            → Γ ⊩⟨ l′ ⟩ snd t ≡ snd t′ ∷ G [ fst t ] / [Gfst]
snd-cong″ {F} {G} [ΣFG] [t] [t′] [t≡t′] [Gfst] =
  let [t] = irrelevanceTerm [ΣFG] (B-intr BΣ (Σ-elim [ΣFG])) [t]
      [t′] = irrelevanceTerm [ΣFG] (B-intr BΣ (Σ-elim [ΣFG])) [t′]
      [t≡t′] = irrelevanceEqTerm [ΣFG] (B-intr BΣ (Σ-elim [ΣFG])) [t≡t′]
  in  snd-cong′ (B-elim BΣ [ΣFG]) [t] [t′] [t≡t′] [Gfst]

snd-congᵛ : ∀ {F G t t′ Γ l}
            ([Γ] : ⊩ᵛ Γ)
            ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
            ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / [Γ] ∙ [F])
            ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G])
            ([t′] : Γ ⊩ᵛ⟨ l ⟩ t′ ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G])
            ([t≡t′] : Γ ⊩ᵛ⟨ l ⟩ t ≡ t′ ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G])
          → Γ ⊩ᵛ⟨ l ⟩ snd t ≡ snd t′ ∷ G [ fst t ] / [Γ] / substS {F} {G} [Γ] [F] [G] (fstᵛ {F} {G} {t} [Γ] [F] [G] [t])
snd-congᵛ {F} {G} {t} {t′} {Γ} {l} [Γ] [F] [G] [t] [t′] [t≡t′] {Δ} {σ} ⊢Δ [σ] =
  let [ΣFG] = Σᵛ {F} {G} [Γ] [F] [G]
      [fst] = fstᵛ {F} {G} {t} [Γ] [F] [G] [t]
      [Gfst] = substS {F} {G} [Γ] [F] [G] [fst]

      ⊩σΣFG = proj₁ ([ΣFG] ⊢Δ [σ])
      ⊩σt = proj₁ ([t] ⊢Δ [σ])
      ⊩σt′ = proj₁ ([t′] ⊢Δ [σ])
      σt≡σt′ = [t≡t′] ⊢Δ [σ]

      ⊩σGfst₁ = proj₁ ([Gfst] ⊢Δ [σ])
      ⊩σGfst = irrelevance′ (singleSubstLift G (fst t)) ⊩σGfst₁

      σsnd≡₁ = snd-cong″ ⊩σΣFG ⊩σt ⊩σt′ σt≡σt′ ⊩σGfst
      σsnd≡ = irrelevanceEqTerm′ (PE.sym (singleSubstLift G (fst t))) ⊩σGfst ⊩σGfst₁ σsnd≡₁
  in  σsnd≡

-- Validity of second projection
sndᵛ : ∀ {F G t Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
       ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / [Γ] ∙ [F])
       ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G])
       → Γ ⊩ᵛ⟨ l ⟩ snd t ∷ G [ fst t ] / [Γ] / substS {F} {G} [Γ] [F] [G] (fstᵛ {F} {G} {t} [Γ] [F] [G] [t])
sndᵛ {F} {G} {t} {Γ} {l} [Γ] [F] [G] [t] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [ΣFG] = Σᵛ {F} {G} [Γ] [F] [G]
      [Gfst] : Γ ⊩ᵛ⟨ l ⟩ G [ fst t ] / [Γ]
      [Gfst] = substS {F} {G} [Γ] [F] [G] (fstᵛ {F} {G} {t} [Γ] [F] [G] [t])

      σsnd : ∀ {Δ σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
           → Δ ⊩⟨ l ⟩ subst σ (snd t) ∷ subst σ (G [ fst t ]) / proj₁ ([Gfst] ⊢Δ [σ])
      σsnd {Δ} {σ} ⊢Δ [σ] =
        let ⊩σΣFG = proj₁ ([ΣFG] ⊢Δ [σ])
            ⊩σt = proj₁ ([t] ⊢Δ [σ])
            ⊩σGfstt = proj₁ ([Gfst] ⊢Δ [σ])
            ⊩σGfstt′ = PE.subst (λ x → Δ ⊩⟨ l ⟩ x) (singleSubstLift G (fst t)) ⊩σGfstt
            ⊩σsnd = snd″ ⊩σΣFG ⊩σt ⊩σGfstt′
        in  irrelevanceTerm′
              (PE.sym (singleSubstLift G (fst t)))
              ⊩σGfstt′  ⊩σGfstt
              ⊩σsnd

  in  σsnd ⊢Δ [σ] ,
      (λ {σ′} [σ′] [σ≡σ′] →
        let [σF] = proj₁ ([F] ⊢Δ [σ])
            [σΣFG] = proj₁ ([ΣFG] ⊢Δ [σ])
            [σ′ΣFG] = proj₁ ([ΣFG] ⊢Δ [σ′])
            [σΣFG≡σ′ΣFG] = proj₂ ([ΣFG] ⊢Δ [σ]) [σ′] [σ≡σ′]
            [σt] = proj₁ ([t] ⊢Δ [σ])
            [σ′t] = proj₁ ([t] ⊢Δ [σ′])
            [σ′t] : Δ ⊩⟨ l ⟩ subst σ′ t ∷ subst σ (Σ F ▹ G) / [σΣFG]
            [σ′t] = convTerm₂ [σΣFG] [σ′ΣFG] [σΣFG≡σ′ΣFG] [σ′t]
            [σt≡σ′t] = proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′]
            [σGfstt] = proj₁ ([Gfst] ⊢Δ [σ])
            [σGfstt]′ = PE.subst (λ x → _ ⊩⟨ l ⟩ x)
                                (singleSubstLift G (fst t))
                                [σGfstt]
            [sndt≡sndt′] = snd-cong″ [σΣFG] [σt] [σ′t] [σt≡σ′t] [σGfstt]′
        in  irrelevanceEqTerm′ (PE.sym (singleSubstLift G (fst t)))
                               [σGfstt]′ [σGfstt]
                               [sndt≡sndt′])


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue333 where

open import Common.Level

data Σ a b (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  _,_ : (x : A) → B x → Σ a b A B

P : ∀ a b (A : Set a) (B : Set b) → Set (a ⊔ b)
P a b A B = Σ a b A (λ _ → B)

postulate
  A B : Set
  foo : Σ lzero lzero A λ (y : A) → P lzero lzero A B

bar : Set₁
bar = helper foo
  where
  helper : (Σ _ _ A λ (y : A) → P _ _ _ _) → Set₁
  helper (y , (x⇓ , fy⇑)) = Set


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

open import Common.Prelude
open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

postulate
  f : Bool → Bool
  boolTrivial : ∀ (b c : Bool) → f b ≡ c

{-# REWRITE boolTrivial #-}

-- Should trigger an error that c is not bound on the lhs.


text:
module L.Base.Nat where

-- Reexport definitions
open import L.Base.Nat.Core public

-- Functions on Nats
pred : Nat → Nat
pred = ind (λ _ → Nat) zero (λ x _ → x)

infixl 6 _+_
infixl 7 _*_

_+_ : Nat → Nat → Nat
zero   + y = y
succ x + y = succ (x + y)

{-# BUILTIN NATPLUS _+_ #-}

_*_ : Nat → Nat → Nat
zero   * y = zero
succ x * y = y + x * y

{-# BUILTIN NATTIMES _*_ #-}

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
{-# OPTIONS --without-K  #-}
module sets.nat.solver where

open import decidable
open import equality
open import function.core
  hiding (const)
open import sets.nat.core
open import sets.nat.properties
open import sets.nat.ordering
open import sets.fin.core
  hiding (_≟_)
open import sets.vec.core
open import sets.vec.dependent

data Exp (n : ℕ) : Set where
  var : Fin n → Exp n
  const : ℕ → Exp n
  _:+_ : Exp n → Exp n → Exp n
infixl 6 _:+_

eval : ∀ {n} → (Fin n → ℕ) → Exp n → ℕ
eval env (var i) = env i
eval env (const x) = x
eval env (e₁ :+ e₂) = eval env e₁ + eval env e₂

NF : ℕ → Set
NF n = Vec ℕ n

evalNF' : ∀ {n} → (Fin n → ℕ) → NF n → ℕ
evalNF' _ [] = 0
evalNF' env (x ∷ xs) = x * env zero + evalNF' (env ∘' suc) xs

evalNF : ∀ {n} → (Fin n → ℕ) → NF (suc n) → ℕ
evalNF env xs = evalNF' (1 ∷∷ env) xs

decNF : ∀ {n}(xs ys : NF n) → Dec (xs ≡ ys)
decNF [] [] = yes refl
decNF (x ∷ xs) (y ∷ ys) with x ≟ y | decNF xs ys
decNF (x ∷ xs) (y ∷ ys) | _ | no u = no λ p → u (ap tail p)
decNF (x ∷ xs) (y ∷ ys) | no u | _ = no λ p → u (ap head p)
decNF (x ∷ xs) (y ∷ ys) | yes p | yes q = yes (ap₂ _∷_ p q)

emptyNF : ∀ {n} → NF n
emptyNF {zero} = []
emptyNF {suc n} = 0 ∷ emptyNF

eval-emptyNF : ∀ {n}(env : Fin n → ℕ) → evalNF' env emptyNF ≡ 0
eval-emptyNF {zero} env = refl
eval-emptyNF {suc n} env = eval-emptyNF {n} (env ∘' suc)

δ : ∀ {n} → Fin n → ℕ → NF n
δ zero val = val ∷ emptyNF
δ (suc i) val = 0 ∷ δ i val

eval-δ : ∀ {n}(i : Fin n)(val : ℕ)
       → (env : Fin n → ℕ)
       → evalNF' env (δ i val) ≡ val * env i
eval-δ zero val env = ap (_+_ (val * env zero)) (eval-emptyNF env)
                    · +-right-unit _
eval-δ (suc i) val env = eval-δ i val (env ∘' suc)

_+NF_ : ∀ {n} → NF n → NF n → NF n
[] +NF [] = []
(x ∷ xs) +NF (y ∷ ys) = (x + y) ∷ (xs +NF ys)

eval+NF : ∀ {n}(xs ys : NF n)(env : Fin n → ℕ)
        → evalNF' env (xs +NF ys)
        ≡ evalNF' env xs + evalNF' env ys
eval+NF [] [] env = refl
eval+NF (x ∷ xs) (y ∷ ys) env
  = ap₂ _+_ (right-distr x y (env zero)) (eval+NF xs ys (env ∘' suc))
  · lem (x * env zero) (y * env zero) (evalNF' (env ∘' suc) xs) (evalNF' (env ∘' suc) ys)
  where
    lem : ∀ a b c d → (a + b) + (c + d) ≡ (a + c) + (b + d)
    lem a b c d
      = +-associativity a b (c + d)
      · ap (_+_ a) (sym (+-associativity b c d))
      · ap (λ z → a + (z + d)) (+-commutativity b c)
      · ap (_+_ a) (+-associativity c b d)
      · sym (+-associativity a c (b + d))

nf : ∀ {n} → Exp n → NF (suc n)
nf (var i) = δ (suc i) 1
nf (const k) = δ zero k
nf (e₁ :+ e₂) = nf e₁ +NF nf e₂

nf-sound : ∀ {n}(env : Fin n → ℕ)(e : Exp n)
         → evalNF env (nf e) ≡ eval env e
nf-sound env (var i) = eval-δ i 1 env · +-right-unit (env i)
nf-sound env (const x) = ap (_+_ (x * 1)) (eval-emptyNF env)
                       · +-right-unit (x * 1)
                       · *-right-unit x
nf-sound env (e₁ :+ e₂) = eval+NF (nf e₁) (nf e₂) (1 ∷∷ env)
                        · ap₂ _+_ (nf-sound env e₁) (nf-sound env e₂)

HOTerm : ℕ → ℕ → Set
HOTerm n zero = Exp n
HOTerm n (suc i) = Exp n → HOTerm n i

private
  exp' : (n i : ℕ) → i ≤ n → HOTerm n i → (Fin i → Exp n) → Exp n
  exp' _ zero _ e _ = e
  exp' zero (suc i) () e f
  exp' (suc n) (suc i) p e f = exp' (suc n) i (trans≤ suc≤ p) (e (f zero)) (f ∘' suc)

exp : ∀ {n} → HOTerm n n → Exp n
exp {n} e = exp' n n refl≤ e var

solve : ∀ n (e₁ e₂ : Exp n){t : True (decNF (nf e₁) (nf e₂))}
      → (env : Fin n → ℕ)
      → eval env e₁ ≡ eval env e₂
solve n e₁ e₂ {t} env = sym (nf-sound env e₁)
                      · ap (evalNF env) (witness t)
                      · nf-sound env e₂

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-

   This module defines the basic opens of the Zariski lattice and proves that they're a basis of the lattice.
   It also contains the construction of the structure presheaf and a proof of the sheaf property on basic opens,
   using the theory developed in the module PreSheafFromUniversalProp and its toSheaf.lemma.
   Note that the structure sheaf is a functor into R-algebras and not just commutative rings.

-}

{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.ZariskiLattice.StructureSheaf where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Powerset using (ℙ ; ⊆-refl-consequence)
                                         renaming (_∈_ to _∈ₚ_ ; subst-∈ to subst-∈ₚ)

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_
                                      ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm
                                      ; ·-identityʳ to ·ℕ-rid)
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Data.Unit
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Poset

open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.Algebra
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.BinomialThm
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.RadicalIdeal
open import Cubical.Algebra.CommRing.Localisation.Base
open import Cubical.Algebra.CommRing.Localisation.UniversalProperty
open import Cubical.Algebra.CommRing.Localisation.InvertingElements
open import Cubical.Algebra.CommRing.Localisation.PullbackSquare
open import Cubical.Algebra.CommAlgebra.Base
open import Cubical.Algebra.CommAlgebra.Properties
open import Cubical.Algebra.CommAlgebra.Localisation
open import Cubical.Algebra.CommAlgebra.Instances.Unit
open import Cubical.Algebra.RingSolver.Reflection
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
open import Cubical.Algebra.DistLattice.Basis
open import Cubical.Algebra.DistLattice.BigOps
open import Cubical.Algebra.ZariskiLattice.Base
open import Cubical.Algebra.ZariskiLattice.UniversalProperty

open import Cubical.Categories.Category.Base hiding (_[_,_])
open import Cubical.Categories.Functor
open import Cubical.Categories.Limits.Pullback
open import Cubical.Categories.Instances.CommAlgebras
open import Cubical.Categories.Instances.DistLattice
open import Cubical.Categories.Instances.Semilattice
open import Cubical.Categories.DistLatticeSheaf

open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

open Iso
open BinaryRelation
open isEquivRel

private
  variable
    ℓ ℓ' : Level

module _ (R' : CommRing ℓ) where
 open CommRingStr ⦃...⦄
 open RingTheory (CommRing→Ring R')
 open CommIdeal R'
 open isCommIdeal

 open ZarLat R'
 open ZarLatUniversalProp R'
 open IsZarMap

 open Join ZariskiLattice
 open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice ZariskiLattice))
 open IsBasis

 private
  R = fst R'
  instance
   _ = snd R'
  ⟨_⟩ : R → CommIdeal
  ⟨ f ⟩ = ⟨ replicateFinVec 1 f ⟩[ R' ]
  ⟨_⟩ₚ : R × R → CommIdeal -- p is for pair
  ⟨ f , g ⟩ₚ = ⟨ replicateFinVec 1 f ++Fin replicateFinVec 1 g ⟩[ R' ]

 BasicOpens : ℙ ZL
 BasicOpens 𝔞 = (∃[ f ∈ R ] (D f ≡ 𝔞)) , isPropPropTrunc

 BO : Type (ℓ-suc ℓ)
 BO = Σ[ 𝔞 ∈ ZL ] (𝔞 ∈ₚ BasicOpens)

 basicOpensAreBasis : IsBasis ZariskiLattice BasicOpens
 contains1 basicOpensAreBasis = ∣ 1r , isZarMapD .pres1 ∣
 ∧lClosed basicOpensAreBasis 𝔞 𝔟 = map2
            λ (f , Df≡𝔞) (g , Dg≡𝔟) → (f · g) , isZarMapD .·≡∧ f g ∙ cong₂ (_∧z_) Df≡𝔞 Dg≡𝔟
 ⋁Basis basicOpensAreBasis = elimProp (λ _ → isPropPropTrunc) Σhelper
  where
  Σhelper : (a : Σ[ n ∈ ℕ ] FinVec R n)
          → ∃[ n ∈ ℕ ] Σ[ α ∈ FinVec ZL n ] (∀ i → α i ∈ₚ BasicOpens) × (⋁ α ≡ [ a ])
  Σhelper (n , α) = ∣ n , (D ∘ α) , (λ i → ∣ α i , refl ∣) , path ∣
   where
   path : ⋁ (D ∘ α) ≡ [ n , α ]
   path = funExt⁻ (cong fst ZLUniversalPropCorollary) _

 -- The structure presheaf on BO
 ZariskiCat = DistLatticeCategory ZariskiLattice

 BOCat : Category (ℓ-suc ℓ) (ℓ-suc ℓ)
 BOCat = ΣPropCat ZariskiCat BasicOpens

 private
  P : ZL → Type _
  P 𝔞 = Σ[ f ∈ R ] (D f ≡ 𝔞) -- the untruncated defining property

  𝓕 : Σ ZL P → CommAlgebra R' _
  𝓕 (_ , f , _) = R[1/ f ]AsCommAlgebra -- D(f) ↦ R[1/f]

  uniqueHom : ∀ (x y : Σ ZL P) → (fst x) ≤ (fst y) → isContr (CommAlgebraHom (𝓕 y) (𝓕 x))
  uniqueHom (𝔞 , f , p) (𝔟 , g , q) = contrHoms 𝔞 𝔟 f g p q
   where
   open InvertingElementsBase R'

   contrHoms : (𝔞 𝔟 : ZL) (f g : R) (p : D f ≡ 𝔞) (q : D g ≡ 𝔟)
             → 𝔞 ≤ 𝔟 → isContr (CommAlgebraHom R[1/ g ]AsCommAlgebra R[1/ f ]AsCommAlgebra)
   contrHoms 𝔞 𝔟 f g p q 𝔞≤𝔟 = R[1/g]HasAlgUniversalProp R[1/ f ]AsCommAlgebra
     λ s s∈[gⁿ|n≥0] → subst-∈ₚ (R[1/ f ]AsCommRing ˣ)
       (sym (·Rid (s /1))) --can't apply the lemma directly as we get mult with 1 somewhere
         (RadicalLemma.toUnit R' f g f∈√⟨g⟩ s s∈[gⁿ|n≥0])
    where
    open AlgLoc R' [ g ⁿ|n≥0] (powersFormMultClosedSubset g)
         renaming (S⁻¹RHasAlgUniversalProp to R[1/g]HasAlgUniversalProp)
    open S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) using (_/1)
    open RadicalIdeal R'

    private
     instance
      _ = snd R[1/ f ]AsCommRing

    Df≤Dg : D f ≤ D g
    Df≤Dg = subst2 _≤_ (sym p) (sym q) 𝔞≤𝔟

    radicalHelper : √ ⟨ f , g ⟩ₚ ≡ √ ⟨ g ⟩
    radicalHelper =
      isEquivRel→effectiveIso (λ _ _ → isSetCommIdeal _ _) ∼EquivRel _ _ .fun Df≤Dg

    f∈√⟨g⟩ : f ∈ √ ⟨ g ⟩
    f∈√⟨g⟩ = subst (f ∈_) radicalHelper (∈→∈√ _ _ (indInIdeal _ _ zero))

 open PreSheafFromUniversalProp ZariskiCat P 𝓕 uniqueHom
 BasisStructurePShf : Functor (BOCat ^op) (CommAlgebrasCategory R')
 BasisStructurePShf = universalPShf

 -- now prove the sheaf properties
 open SheafOnBasis ZariskiLattice (CommAlgebrasCategory R' {ℓ' = ℓ})
                   (TerminalCommAlgebra R') BasicOpens basicOpensAreBasis

 isSheafBasisStructurePShf : isDLBasisSheaf BasisStructurePShf
 fst isSheafBasisStructurePShf 0∈BO =
   transport (λ i → F-ob (0z , canonical0∈BO≡0∈BO i) ≡ UnitCommAlgebra R') R[1/0]≡0
   where
   open Functor ⦃...⦄
   instance
    _ = BasisStructurePShf

   canonical0∈BO : 0z ∈ₚ BasicOpens
   canonical0∈BO = ∣ 0r , isZarMapD .pres0 ∣

   canonical0∈BO≡0∈BO : canonical0∈BO ≡ 0∈BO
   canonical0∈BO≡0∈BO = BasicOpens 0z .snd _ _

   R[1/0]≡0 : R[1/ 0r ]AsCommAlgebra ≡ UnitCommAlgebra R'
   R[1/0]≡0 = uaCommAlgebra (e , eIsRHom)
    where
    open InvertingElementsBase R' using (isContrR[1/0])
    open IsAlgebraHom

    e : R[1/ 0r ]AsCommAlgebra .fst ≃ UnitCommAlgebra R' .fst
    e = isContr→Equiv isContrR[1/0] isContrUnit*

    eIsRHom : IsCommAlgebraEquiv (R[1/ 0r ]AsCommAlgebra .snd) e (UnitCommAlgebra R' .snd)
    pres0 eIsRHom = refl
    pres1 eIsRHom = refl
    pres+ eIsRHom _ _ = refl
    pres· eIsRHom _ _ = refl
    pres- eIsRHom _ = refl
    pres⋆ eIsRHom _ _ = refl

 snd isSheafBasisStructurePShf (𝔞 , 𝔞∈BO) (𝔟 , 𝔟∈BO) 𝔞∨𝔟∈BO = curriedHelper 𝔞 𝔟 𝔞∈BO 𝔟∈BO 𝔞∨𝔟∈BO
  where
  open condSquare
  {-
     here:
     BFsq (𝔞 , 𝔞∈BO) (𝔟 , 𝔟∈BO) 𝔞∨𝔟∈BO BasisStructurePShf =

     𝓞 (𝔞∨𝔟) → 𝓞 (𝔞)

       ↓         ↓

     𝓞 (𝔟)  →  𝓞 (𝔞∧𝔟)

  -}
  curriedHelper : (𝔞 𝔟 : ZL) (𝔞∈BO : 𝔞 ∈ₚ BasicOpens) (𝔟∈BO : 𝔟 ∈ₚ BasicOpens)
                  (𝔞∨𝔟∈BO : 𝔞 ∨z 𝔟 ∈ₚ BasicOpens)
                → isPullback (CommAlgebrasCategory R') _ _ _
                             (BFsq (𝔞 , 𝔞∈BO) (𝔟 , 𝔟∈BO) 𝔞∨𝔟∈BO BasisStructurePShf)
  curriedHelper 𝔞 𝔟 = elim3 (λ 𝔞∈BO 𝔟∈BO 𝔞∨𝔟∈BO → isPropIsPullback _ _ _ _
                            (BFsq (𝔞 , 𝔞∈BO) (𝔟 , 𝔟∈BO) 𝔞∨𝔟∈BO BasisStructurePShf))
                            Σhelper
   where
   -- write everything explicitly so things can type-check
   thePShfCospan : (a : Σ[ f ∈ R ] D f ≡ 𝔞) (b : Σ[ g ∈ R ] D g ≡ 𝔟)
                 → Cospan (CommAlgebrasCategory R')
   Cospan.l (thePShfCospan (f , Df≡𝔞) (g , Dg≡𝔟)) = BasisStructurePShf .Functor.F-ob (𝔟 , ∣ g , Dg≡𝔟 ∣)
   Cospan.m (thePShfCospan (f , Df≡𝔞) (g , Dg≡𝔟)) = BasisStructurePShf .Functor.F-ob
            (𝔞 ∧z 𝔟 , basicOpensAreBasis .∧lClosed 𝔞 𝔟 ∣ f , Df≡𝔞 ∣ ∣ g , Dg≡𝔟 ∣)
   Cospan.r (thePShfCospan (f , Df≡𝔞) (g , Dg≡𝔟)) = BasisStructurePShf .Functor.F-ob (𝔞 , ∣ f , Df≡𝔞 ∣)
   Cospan.s₁ (thePShfCospan (f , Df≡𝔞) (g , Dg≡𝔟)) = BasisStructurePShf .Functor.F-hom
             {x = (𝔟 , ∣ g , Dg≡𝔟 ∣)}
             {y = (𝔞 ∧z 𝔟 , basicOpensAreBasis .∧lClosed 𝔞 𝔟 ∣ f , Df≡𝔞 ∣ ∣ g , Dg≡𝔟 ∣)}
             (hom-∧₂  ZariskiLattice (CommAlgebrasCategory R' {ℓ' = ℓ}) (TerminalCommAlgebra R') 𝔞 𝔟)
   Cospan.s₂ (thePShfCospan (f , Df≡𝔞) (g , Dg≡𝔟)) = BasisStructurePShf .Functor.F-hom
             {x = (𝔞 , ∣ f , Df≡𝔞 ∣)}
             {y = (𝔞 ∧z 𝔟 , basicOpensAreBasis .∧lClosed 𝔞 𝔟 ∣ f , Df≡𝔞 ∣ ∣ g , Dg≡𝔟 ∣)}
             (hom-∧₁  ZariskiLattice (CommAlgebrasCategory R' {ℓ' = ℓ}) (TerminalCommAlgebra R') 𝔞 𝔟)

   Σhelper : (a : Σ[ f ∈ R ] D f ≡ 𝔞) (b : Σ[ g ∈ R ] D g ≡ 𝔟) (c : Σ[ h ∈ R ] D h ≡ 𝔞 ∨z 𝔟)
           → isPullback (CommAlgebrasCategory R') (thePShfCospan a b) _ _
                        (BFsq (𝔞 , ∣ a ∣) (𝔟 , ∣ b ∣) ∣ c ∣ BasisStructurePShf)
   Σhelper (f , Df≡𝔞) (g , Dg≡𝔟) (h , Dh≡𝔞∨𝔟) = toSheaf.lemma
           (𝔞 ∨z 𝔟 , ∣ h , Dh≡𝔞∨𝔟 ∣)
           (𝔞 , ∣ f , Df≡𝔞 ∣)
           (𝔟 , ∣ g , Dg≡𝔟 ∣)
           (𝔞 ∧z 𝔟 , basicOpensAreBasis .∧lClosed 𝔞 𝔟 ∣ f , Df≡𝔞 ∣ ∣ g , Dg≡𝔟 ∣)
           (Bsq (𝔞 , ∣ f , Df≡𝔞 ∣) (𝔟 , ∣ g , Dg≡𝔟 ∣) ∣ h , Dh≡𝔞∨𝔟 ∣)
           theAlgebraCospan theAlgebraPullback refl gPath fPath fgPath
    where
    open Exponentiation R'
    open RadicalIdeal R'
    open InvertingElementsBase R'
    open DoubleLoc R' h
    open S⁻¹RUniversalProp R' [ h ⁿ|n≥0] (powersFormMultClosedSubset h)
    open CommIdeal R[1/ h ]AsCommRing using () renaming (CommIdeal to CommIdealₕ ; _∈_ to _∈ₕ_)

    instance
     _ = snd R[1/ h ]AsCommRing

    ⟨_⟩ₕ : R[1/ h ] × R[1/ h ] → CommIdealₕ
    ⟨ x , y ⟩ₕ = ⟨ replicateFinVec 1 x ++Fin replicateFinVec 1 y ⟩[ R[1/ h ]AsCommRing ]

    -- the crucial algebraic fact:
    radicalPath : √ ⟨ h ⟩ ≡ √ ⟨ f , g ⟩ₚ
    radicalPath = isEquivRel→effectiveIso (λ _ _ → isSetCommIdeal _ _) ∼EquivRel _ _ .fun DHelper
     where
     DHelper : D h ≡ D f ∨z D g
     DHelper = Dh≡𝔞∨𝔟 ∙ cong₂ (_∨z_) (sym Df≡𝔞) (sym Dg≡𝔟)

    f∈√⟨h⟩ : f ∈ √ ⟨ h ⟩
    f∈√⟨h⟩ = subst (f ∈_) (sym radicalPath) (∈→∈√ _ _ (indInIdeal _ _ zero))

    g∈√⟨h⟩ : g ∈ √ ⟨ h ⟩
    g∈√⟨h⟩ = subst (g ∈_) (sym radicalPath) (∈→∈√ _ _ (indInIdeal _ _ (suc zero)))

    fg∈√⟨h⟩ : (f · g) ∈ √ ⟨ h ⟩
    fg∈√⟨h⟩ = √ ⟨ h ⟩ .snd .·Closed f g∈√⟨h⟩

    1∈fgIdeal : 1r ∈ₕ ⟨ (f /1) , (g /1) ⟩ₕ
    1∈fgIdeal = helper1 (subst (h ∈_) radicalPath (∈→∈√ _ _ (indInIdeal _ _ zero)))
     where
     helper1 : h ∈ √ ⟨ f , g ⟩ₚ
             → 1r ∈ₕ ⟨ (f /1) , (g /1) ⟩ₕ
     helper1 = PT.rec isPropPropTrunc (uncurry helper2)
      where
      helper2 : (n : ℕ)
              → h ^ n ∈ ⟨ f , g ⟩ₚ
              → 1r ∈ₕ ⟨ (f /1) , (g /1) ⟩ₕ
      helper2 n = map helper3
       where
       helper3 : Σ[ α ∈ FinVec R 2 ]
                  h ^ n ≡ linearCombination R' α (λ { zero → f ; (suc zero) → g })
               → Σ[ β ∈ FinVec R[1/ h ] 2 ]
                  1r ≡ linearCombination R[1/ h ]AsCommRing β
                                         λ { zero → f /1 ; (suc zero) → g /1 }
       helper3 (α , p) = β , path
        where
        β : FinVec R[1/ h ] 2
        β zero = [ α zero , h ^ n , ∣ n , refl ∣ ]
        β (suc zero) = [ α (suc zero) , h ^ n , ∣ n , refl ∣ ]

        path : 1r ≡ linearCombination R[1/ h ]AsCommRing β
                                      λ { zero → f /1 ; (suc zero) → g /1 }
        path = eq/ _ _ ((1r , ∣ 0 , refl ∣) , bigPath)
             ∙ cong (β zero · (f /1) +_) (sym (+Rid (β (suc zero) · (g /1))))
         where
         useSolver1 : ∀ hn → 1r · 1r · ((hn · 1r) · (hn · 1r)) ≡ hn · hn
         useSolver1 = solve R'

         useSolver2 : ∀ az f hn as g → hn · (az · f + (as · g + 0r))
                                      ≡ 1r · (az · f · (hn · 1r) + as · g · (hn · 1r)) · 1r
         useSolver2 = solve R'

         bigPath : 1r · 1r · ((h ^ n · 1r) · (h ^ n · 1r))
                 ≡ 1r · (α zero · f · (h ^ n · 1r) + α (suc zero) · g · (h ^ n · 1r)) · 1r
         bigPath = useSolver1 (h ^ n) ∙ cong (h ^ n ·_) p ∙ useSolver2 _ _ _ _ _

    {-

      We get the following pullback square in CommRings

        R[1/h]   →    R[1/h][1/f]
              ⌟
        ↓             ↓

        R[1/h][1/g] → R[1/h][1/fg]

      this lifts to a pullback in R-Algebras using PullbackFromCommRing
      as all for rings have canonical morphisms coming from R
      and all the triangles commute.

      Then using toSheaf.lemma we get the desired square

        R[1/h]  →  R[1/f]
              ⌟
        ↓          ↓

        R[1/g]  →  R[1/fg]

      by only providing paths between the corresponding vertices of the square.
      These paths are constructed using S⁻¹RAlgCharEquiv, which gives
      an equivalent characterization of the universal property of localization
      that can be found in e.g. Cor 3.2 of Atiyah-MacDonald

    -}

    theRingCospan = fgCospan R[1/ h ]AsCommRing (f /1) (g /1)
    theRingPullback = fgPullback R[1/ h ]AsCommRing (f /1) (g /1) 1∈fgIdeal

    R[1/h][1/f] = InvertingElementsBase.R[1/_] R[1/ h ]AsCommRing (f /1)
    R[1/h][1/f]AsCommRing = InvertingElementsBase.R[1/_]AsCommRing R[1/ h ]AsCommRing (f /1)
    R[1/h][1/g] = InvertingElementsBase.R[1/_] R[1/ h ]AsCommRing (g /1)
    R[1/h][1/g]AsCommRing = InvertingElementsBase.R[1/_]AsCommRing R[1/ h ]AsCommRing (g /1)
    R[1/h][1/fg] = InvertingElementsBase.R[1/_] R[1/ h ]AsCommRing ((f /1) · (g /1))
    R[1/h][1/fg]AsCommRing = InvertingElementsBase.R[1/_]AsCommRing
                               R[1/ h ]AsCommRing ((f /1) · (g /1))

    open IsRingHom
    /1/1AsCommRingHomFG : CommRingHom R' R[1/h][1/fg]AsCommRing
    fst /1/1AsCommRingHomFG r = [ [ r , 1r , ∣ 0 , refl ∣ ] , 1r , ∣ 0 , refl ∣ ]
    pres0 (snd /1/1AsCommRingHomFG) = refl
    pres1 (snd /1/1AsCommRingHomFG) = refl
    pres+ (snd /1/1AsCommRingHomFG) x y = cong [_] (≡-× (cong [_] (≡-×
                                         (cong₂ _+_ (useSolver x) (useSolver y))
                                         (Σ≡Prop (λ _ → isPropPropTrunc) (useSolver 1r))))
                                         (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·Rid 1r))))
      where
      useSolver : ∀ a → a ≡ a · 1r · (1r · 1r)
      useSolver = solve R'
    pres· (snd /1/1AsCommRingHomFG) x y = cong [_] (≡-× (cong [_] (≡-× refl
                                            (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·Rid 1r)))))
                                            (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·Rid 1r))))
    pres- (snd /1/1AsCommRingHomFG) x = refl

    open Cospan
    open Pullback
    open RingHoms
    isRHomR[1/h]→R[1/h][1/f] : theRingPullback .pbPr₂ ∘r /1AsCommRingHom ≡ /1/1AsCommRingHom f
    isRHomR[1/h]→R[1/h][1/f] = RingHom≡ (funExt (λ x → refl))

    isRHomR[1/h]→R[1/h][1/g] : theRingPullback .pbPr₁ ∘r /1AsCommRingHom ≡ /1/1AsCommRingHom g
    isRHomR[1/h]→R[1/h][1/g] = RingHom≡ (funExt (λ x → refl))

    isRHomR[1/h][1/f]→R[1/h][1/fg] : theRingCospan .s₂ ∘r /1/1AsCommRingHom f ≡ /1/1AsCommRingHomFG
    isRHomR[1/h][1/f]→R[1/h][1/fg] = RingHom≡ (funExt
      (λ x → cong [_] (≡-× (cong [_] (≡-× (cong (x ·_) (transportRefl 1r) ∙ ·Rid x)
          (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·Rid 1r))))
          (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·Rid 1r)))))

    isRHomR[1/h][1/g]→R[1/h][1/fg] : theRingCospan .s₁ ∘r /1/1AsCommRingHom g ≡ /1/1AsCommRingHomFG
    isRHomR[1/h][1/g]→R[1/h][1/fg] = RingHom≡ (funExt
      (λ x → cong [_] (≡-× (cong [_] (≡-× (cong (x ·_) (transportRefl 1r) ∙ ·Rid x)
          (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·Rid 1r))))
          (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·Rid 1r)))))

    open PullbackFromCommRing R' theRingCospan theRingPullback
         /1AsCommRingHom (/1/1AsCommRingHom f) (/1/1AsCommRingHom g) /1/1AsCommRingHomFG
    theAlgebraCospan = algCospan isRHomR[1/h]→R[1/h][1/f]
                                 isRHomR[1/h]→R[1/h][1/g]
                                 isRHomR[1/h][1/f]→R[1/h][1/fg]
                                 isRHomR[1/h][1/g]→R[1/h][1/fg]
    theAlgebraPullback = algPullback isRHomR[1/h]→R[1/h][1/f]
                                     isRHomR[1/h]→R[1/h][1/g]
                                     isRHomR[1/h][1/f]→R[1/h][1/fg]
                                     isRHomR[1/h][1/g]→R[1/h][1/fg]

    --and the three remaining paths
    fPath : theAlgebraCospan .r ≡ R[1/ f ]AsCommAlgebra
    fPath = doubleLocCancel f∈√⟨h⟩
     where
     open DoubleAlgLoc R' h f

    gPath : theAlgebraCospan .l ≡ R[1/ g ]AsCommAlgebra
    gPath = doubleLocCancel g∈√⟨h⟩
     where
     open DoubleAlgLoc R' h g

    fgPath : theAlgebraCospan .m ≡ R[1/ (f · g) ]AsCommAlgebra
    fgPath = path ∙ doubleLocCancel fg∈√⟨h⟩
     where
     open DoubleAlgLoc R' h (f · g)
     open CommAlgChar R'

     R[1/h][1/fg]AsCommRing' = InvertingElementsBase.R[1/_]AsCommRing R[1/ h ]AsCommRing ((f · g) /1)

     path : toCommAlg (R[1/h][1/fg]AsCommRing , /1/1AsCommRingHomFG)
          ≡ toCommAlg (R[1/h][1/fg]AsCommRing' , /1/1AsCommRingHom (f · g))
     path = cong toCommAlg (ΣPathP (p , q))
      where
      eqInR[1/h] : (f /1) · (g /1) ≡ (f · g) /1
      eqInR[1/h] = sym (/1AsCommRingHom .snd .pres· f g)

      p : R[1/h][1/fg]AsCommRing ≡ R[1/h][1/fg]AsCommRing'
      p i = InvertingElementsBase.R[1/_]AsCommRing R[1/ h ]AsCommRing (eqInR[1/h] i)

      q : PathP (λ i → CommRingHom R' (p i)) /1/1AsCommRingHomFG (/1/1AsCommRingHom (f · g))
      q = toPathP (RingHom≡ (funExt (
            λ x → cong [_] (≡-× (cong [_] (≡-× (transportRefl _ ∙ transportRefl x)
                (Σ≡Prop (λ _ → isPropPropTrunc) (transportRefl 1r))))
                (Σ≡Prop (λ _ → isPropPropTrunc) (transportRefl 1r))))))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


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

open import Agda.Builtin.Cubical.Path

-- Higher constructors must be erased when --erased-cubical is used.

data ∥_∥ (A : Set) : Set where
  ∣_∣     : A → ∥ A ∥
  trivial : (x y : ∥ A ∥) → x ≡ y