text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRingSolver.HornerEval where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Int hiding (_+_ ; _·_ ; -_)
open import Cubical.Data.Vec
open import Cubical.Data.Bool

open import Cubical.Relation.Nullary.Base using (¬_; yes; no)

open import Cubical.Algebra.CommRingSolver.Utility
open import Cubical.Algebra.CommRingSolver.RawAlgebra
open import Cubical.Algebra.CommRingSolver.IntAsRawRing
open import Cubical.Algebra.CommRingSolver.HornerForms
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring

private
  variable
    ℓ ℓ' : Level

eval : {A : RawAlgebra ℤAsRawRing ℓ'}
       {n : ℕ} (P : IteratedHornerForms A n)
       → Vec ⟨ A ⟩ n → ⟨ A ⟩
eval {A = A} (const r) [] = RawAlgebra.scalar A r
eval {A = A} 0H (_ ∷ _) = RawAlgebra.0r A
eval {A = A} (P ·X+ Q) (x ∷ xs) =
     let open RawAlgebra A
         P' = (eval P (x ∷ xs))
         Q' = eval Q xs
     in if (isZero A P)
        then Q'
        else P' · x + Q'

module _ (R : CommRing ℓ) where
  private
    νR = CommRing→RawℤAlgebra R
  open CommRingStr (snd R)
  open RingTheory (CommRing→Ring R)
  open IteratedHornerOperations νR

  someCalculation : {x : fst R} → _ ≡ _
  someCalculation {x = x} =
    0r                   ≡⟨ sym (+IdR 0r) ⟩
    0r + 0r              ≡[ i ]⟨ 0LeftAnnihilates x (~ i) + 0r ⟩
    0r · x + 0r          ∎

  evalIsZero : {n : ℕ} (P : IteratedHornerForms νR n)
             → (l : Vec (fst R) n)
             → isZero νR P ≡ true
             → eval P l ≡ 0r
  evalIsZero (const (pos ℕ.zero)) [] isZeroP = refl
  evalIsZero (const (pos (ℕ.suc n))) [] isZeroP = byBoolAbsurdity isZeroP
  evalIsZero (const (negsuc _)) [] isZeroP = byBoolAbsurdity isZeroP
  evalIsZero 0H (x ∷ xs) _ = refl
  evalIsZero {n = ℕ.suc n} (P ·X+ Q) (x ∷ xs) isZeroPandQ with isZero νR P
  ... | true = eval Q xs   ≡⟨ evalIsZero Q xs isZeroQ ⟩
               0r ∎
               where isZeroQ = snd (extractFromAnd _ _ isZeroPandQ)
  ... | false = byBoolAbsurdity isZeroP
               where isZeroP = fst (extractFromAnd _ _ isZeroPandQ)

  computeEvalSummandIsZero :
               {n : ℕ}
               (P : IteratedHornerForms νR (ℕ.suc n))
               (Q : IteratedHornerForms νR n)
             → (xs : Vec (fst R) n)
             → (x : (fst R))
             → isZero νR P ≡ true
             → eval (P ·X+ Q) (x ∷ xs) ≡ eval Q xs
  computeEvalSummandIsZero P Q xs x isZeroP with isZero νR P
  ... | true = refl
  ... | false = byBoolAbsurdity isZeroP

  computeEvalNotZero :
               {n : ℕ}
               (P : IteratedHornerForms νR (ℕ.suc n))
               (Q : IteratedHornerForms νR n)
             → (xs : Vec (fst R) n)
             → (x : (fst R))
             → ¬ (isZero νR P ≡ true)
             → eval (P ·X+ Q) (x ∷ xs) ≡ (eval P (x ∷ xs)) · x + eval Q xs
  computeEvalNotZero P Q xs x notZeroP with isZero νR P
  ... | true = byBoolAbsurdity (sym (¬true→false true notZeroP))
  ... | false = refl

  combineCasesEval :
    {n : ℕ}  (P : IteratedHornerForms νR (ℕ.suc n)) (Q : IteratedHornerForms νR n)
    (x : (fst R)) (xs : Vec (fst R) n)
    →   eval (P ·X+ Q) (x ∷ xs)
      ≡ (eval P (x ∷ xs)) · x + eval Q xs
  combineCasesEval P Q x xs with isZero νR P ≟ true
  ... | yes p =
       eval (P ·X+ Q) (x ∷ xs)            ≡⟨ computeEvalSummandIsZero P Q xs x p ⟩
       eval Q xs                          ≡⟨ sym (+IdL _) ⟩
       0r + eval Q xs                     ≡[ i ]⟨ 0LeftAnnihilates x (~ i) + eval Q xs ⟩
       0r · x + eval Q xs                 ≡[ i ]⟨ (evalIsZero P (x ∷ xs) p (~ i)) · x + eval Q xs ⟩
       (eval P (x ∷ xs)) · x + eval Q xs ∎
  ... | no p  = computeEvalNotZero P Q xs x p

  compute+ₕEvalBothZero :
    (n : ℕ) (P Q : IteratedHornerForms νR (ℕ.suc n))
    (r s : IteratedHornerForms νR n)
    (x : (fst R)) (xs : Vec (fst R) n)
    → (isZero νR (P +ₕ Q) and isZero νR (r +ₕ s)) ≡ true
    → eval ((P ·X+ r) +ₕ (Q ·X+ s)) (x ∷ xs) ≡ eval ((P +ₕ Q) ·X+ (r +ₕ s)) (x ∷ xs)
  compute+ₕEvalBothZero n P Q r s x xs bothZero with isZero νR (P +ₕ Q) and isZero νR (r +ₕ s) | bothZero
  ... | true | p =
               eval {A = νR} 0H (x ∷ xs)                            ≡⟨ refl ⟩
               0r                                                   ≡⟨ someCalculation ⟩
               0r · x + 0r                                          ≡⟨ step1  ⟩
               (eval (P +ₕ Q) (x ∷ xs)) · x + eval (r +ₕ s) xs       ≡⟨ step2 ⟩
               eval ((P +ₕ Q) ·X+ (r +ₕ s)) (x ∷ xs) ∎
            where step1 : 0r · x + 0r ≡ (eval (P +ₕ Q) (x ∷ xs)) · x + eval (r +ₕ s) xs
                  step1 i = (evalIsZero (P +ₕ Q) (x ∷ xs) (fst (extractFromAnd _ _ (bothZero))) (~ i)) · x
                    + (evalIsZero (r +ₕ s) xs (snd (extractFromAnd _ _ (bothZero))) (~ i))
                  step2 = sym (combineCasesEval (P +ₕ Q) (r +ₕ s) x xs)
  ... | false | p = byBoolAbsurdity p

  compute+ₕEvalNotBothZero :
    (n : ℕ) (P Q : IteratedHornerForms νR (ℕ.suc n))
    (r s : IteratedHornerForms νR n)
    (x : (fst R)) (xs : Vec (fst R) n)
    → (isZero νR (P +ₕ Q) and isZero νR (r +ₕ s)) ≡ false
    → eval ((P ·X+ r) +ₕ (Q ·X+ s)) (x ∷ xs) ≡ eval ((P +ₕ Q) ·X+ (r +ₕ s)) (x ∷ xs)
  compute+ₕEvalNotBothZero n P Q r s _ _ notBothZero
    with isZero νR (P +ₕ Q) and isZero νR (r +ₕ s) | notBothZero
  ... | true | p = byBoolAbsurdity (sym p)
  ... | false | p = refl

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the `Reflects` construct
------------------------------------------------------------------------

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

module Relation.Nullary.Reflects where

open import Agda.Builtin.Equality
open import Data.Bool.Base
open import Data.Empty
open import Level
open import Relation.Nullary

private
  variable
    p : Level
    P : Set p

------------------------------------------------------------------------
-- `Reflects P b` is equivalent to `if b then P else ¬ P`.

-- These lemmas are intended to be used mostly when `b` is a value, so
-- that the `if` expressions have already been evaluated away.
-- In this case, `of` works like the relevant constructor (`ofⁿ` or
-- `ofʸ`), and `invert` strips off the constructor to just give either
-- the proof of `P` or the proof of `¬ P`.

of : ∀ {b} → if b then P else ¬ P → Reflects P b
of {b = false} ¬p = ofⁿ ¬p
of {b = true }  p = ofʸ p

invert : ∀ {b} → Reflects P b → if b then P else ¬ P
invert (ofʸ  p) = p
invert (ofⁿ ¬p) = ¬p

------------------------------------------------------------------------
-- Other lemmas

-- `Reflects` is deterministic.
det : ∀ {b b′} → Reflects P b → Reflects P b′ → b ≡ b′
det (ofʸ  p) (ofʸ  p′) = refl
det (ofʸ  p) (ofⁿ ¬p′) = ⊥-elim (¬p′ p)
det (ofⁿ ¬p) (ofʸ  p′) = ⊥-elim (¬p p′)
det (ofⁿ ¬p) (ofⁿ ¬p′) = refl

ext: agda


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

open import Cubical.Algebra.CommRing.Base public
open import Cubical.Algebra.CommRing.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


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

module Pim2Cat where

open import Level using (zero)
open import Data.Product using (_,_; _×_; proj₁; proj₂)

import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; isEquivalence)

open import Categories.Category using (Category)
open import Categories.Groupoid using (Groupoid)
open import Categories.Monoidal using (Monoidal)
open import Categories.Monoidal.Helpers using (module MonoidalHelperFunctors)
open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.Monoidal.Braided using (Braided)
open import Categories.Monoidal.Symmetric using (Symmetric)
open import Categories.RigCategory
  using (RigCategory; module BimonoidalHelperFunctors)

open import PiU using (U; PLUS; ZERO; TIMES; ONE)
open import PiLevelm2 using (_⟷_; collapse)

-- We will define a rig category whose objects are Pi types and whose
-- morphisms are the trivial equivalence that identifies all Pi types;
-- and where the equivalence of morphisms is propositional equality ≡

------------------------------------------------------------------------------
-- First it is a category

triv : {A B : U} → (f : A ⟷ B) → (collapse P.≡ f)
triv collapse = P.refl

Pim2Cat : Category zero zero zero
Pim2Cat = record
  { Obj = U
  ; _⇒_ = _⟷_
  ; _≡_ = P._≡_
  ; id = collapse
  ; _∘_ = λ _ _ → collapse
  ; assoc = P.refl
  ; identityˡ = λ {A} {B} {f} → triv f
  ; identityʳ = λ {A} {B} {f} → triv f
  ; equiv = P.isEquivalence
  ; ∘-resp-≡ = λ _ _ → P.refl
  }

-- and a groupoid

Pim2Groupoid : Groupoid Pim2Cat
Pim2Groupoid = record
  { _⁻¹ = λ _ → collapse
  ; iso = record { isoˡ = P.refl; isoʳ = P.refl }
  }

-- The additive structure is monoidal

PLUS-bifunctor : Bifunctor Pim2Cat Pim2Cat Pim2Cat
PLUS-bifunctor = record
  { F₀ = λ {( x , y) → PLUS x y}
  ; F₁ = λ {(x , y) → collapse}
  ; identity = P.refl
  ; homomorphism = P.refl
  ; F-resp-≡ = λ { (e₁ , e₂) → P.refl }
  }

module PLUSh = MonoidalHelperFunctors Pim2Cat PLUS-bifunctor ZERO

0PLUSx≡x : NaturalIsomorphism PLUSh.id⊗x PLUSh.x
0PLUSx≡x = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

xPLUS0≡x : NaturalIsomorphism PLUSh.x⊗id PLUSh.x
xPLUS0≡x = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

[xPLUSy]PLUSz≡xPLUS[yPLUSz] : NaturalIsomorphism PLUSh.[x⊗y]⊗z PLUSh.x⊗[y⊗z]
[xPLUSy]PLUSz≡xPLUS[yPLUSz] = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

CPMPLUS : Monoidal Pim2Cat
CPMPLUS = record
  { ⊗ = PLUS-bifunctor
   ; id = ZERO
   ; identityˡ = 0PLUSx≡x
   ; identityʳ = xPLUS0≡x
   ; assoc = [xPLUSy]PLUSz≡xPLUS[yPLUSz]
   ; triangle = P.refl
   ; pentagon = P.refl
   }

-- The multiplicative structure is also monoidal

TIMES-bifunctor : Bifunctor Pim2Cat Pim2Cat Pim2Cat
TIMES-bifunctor = record
  { F₀ = λ {( x , y) → TIMES x y}
  ; F₁ = λ {(x , y) → collapse }
  ; identity = P.refl
  ; homomorphism = P.refl
  ; F-resp-≡ = λ { (e₁ , e₂) → P.refl}
  }

module TIMESh = MonoidalHelperFunctors Pim2Cat TIMES-bifunctor ONE

1TIMESy≡y : NaturalIsomorphism TIMESh.id⊗x TIMESh.x
1TIMESy≡y = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

yTIMES1≡y : NaturalIsomorphism TIMESh.x⊗id TIMESh.x
yTIMES1≡y = record
  { F⇒G = record
    { η = λ X → collapse
    ;  commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

[xTIMESy]TIMESz≡xTIMES[yTIMESz] :
  NaturalIsomorphism TIMESh.[x⊗y]⊗z TIMESh.x⊗[y⊗z]
[xTIMESy]TIMESz≡xTIMES[yTIMESz] = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

CPMTIMES : Monoidal Pim2Cat
CPMTIMES = record
  { ⊗ = TIMES-bifunctor
  ; id = ONE
  ; identityˡ = 1TIMESy≡y
  ; identityʳ = yTIMES1≡y
  ; assoc = [xTIMESy]TIMESz≡xTIMES[yTIMESz]
  ; triangle = P.refl
  ; pentagon = P.refl
  }

-- The monoidal structures are symmetric

xPLUSy≈yPLUSx : NaturalIsomorphism PLUSh.x⊗y PLUSh.y⊗x
xPLUSy≈yPLUSx = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

BMPLUS : Braided CPMPLUS
BMPLUS = record
  { braid = xPLUSy≈yPLUSx
  ; unit-coh = P.refl
  ; hexagon₁ = P.refl
  ; hexagon₂ = P.refl
  }

xTIMESy≈yTIMESx : NaturalIsomorphism TIMESh.x⊗y TIMESh.y⊗x
xTIMESy≈yTIMESx = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

BMTIMES : Braided CPMTIMES
BMTIMES = record
  { braid = xTIMESy≈yTIMESx
  ; unit-coh = P.refl
  ; hexagon₁ = P.refl
  ; hexagon₂ = P.refl
  }

SBMPLUS : Symmetric BMPLUS
SBMPLUS = record { symmetry = P.refl }

SBMTIMES : Symmetric BMTIMES
SBMTIMES = record { symmetry = P.refl }

-- And finally the multiplicative structure distributes over the
-- additive one

module r = BimonoidalHelperFunctors BMPLUS BMTIMES

x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] : NaturalIsomorphism r.x⊗[y⊕z] r.[x⊗y]⊕[x⊗z]
x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record { isoˡ = P.refl
                       ; isoʳ = P.refl }
  }

[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] : NaturalIsomorphism r.[x⊕y]⊗z r.[x⊗z]⊕[y⊗z]
[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record { isoˡ = P.refl
                       ; isoʳ = P.refl }
  }

x⊗0≡0 : NaturalIsomorphism r.x⊗0 r.0↑
x⊗0≡0 = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

0⊗x≡0 : NaturalIsomorphism r.0⊗x r.0↑
0⊗x≡0 = record
  { F⇒G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; F⇐G = record
    { η = λ X → collapse
    ; commute = λ f → P.refl
    }
  ; iso = λ X → record
    { isoˡ = P.refl
    ; isoʳ = P.refl
    }
  }

TERig : RigCategory SBMPLUS SBMTIMES
TERig = record
  { distribₗ = x⊗[y⊕z]≡[x⊗y]⊕[x⊗z]
  ; distribᵣ = [x⊕y]⊗z≡[x⊗z]⊕[y⊗z]
  ; annₗ = 0⊗x≡0
  ; annᵣ = x⊗0≡0
  ; laplazaI = P.refl
  ; laplazaII = P.refl
  ; laplazaIV = P.refl
  ; laplazaVI = P.refl
  ; laplazaIX = P.refl
  ; laplazaX = P.refl
  ; laplazaXI = P.refl
  ; laplazaXIII = P.refl
  ; laplazaXV = P.refl
  ; laplazaXVI = P.refl
  ; laplazaXVII = P.refl
  ; laplazaXIX = P.refl
  ; laplazaXXIII = P.refl
  }

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --cubical #-}
module _ where

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

data ⊤ : Set where
  tt : ⊤

data S : Set where
  base : S
  loop : base ≡ base

postulate
  P' : base ≡ base → Set
  pl : P' loop

foo : P' loop
foo with tt
... | w = pl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

open import Cubical.Data.Sum.Base public
open import Cubical.Data.Sum.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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some code related to transitive closures that relies on the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Relation.Binary.Construct.Closure.Transitive.WithK where

open import Function
open import Relation.Binary
open import Relation.Binary.Construct.Closure.Transitive
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

module _ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} where

 ∼⁺⟨⟩-injectiveˡ : ∀ {x y z} {p r : x [ _∼_ ]⁺ y} {q s} →
                   (x [ _∼_ ]⁺ z ∋ x ∼⁺⟨ p ⟩ q) ≡ (x ∼⁺⟨ r ⟩ s) → p ≡ r
 ∼⁺⟨⟩-injectiveˡ refl = refl

 ∼⁺⟨⟩-injectiveʳ : ∀ {x y z} {p r : x [ _∼_ ]⁺ y} {q s} →
                   (x [ _∼_ ]⁺ z ∋ x ∼⁺⟨ p ⟩ q) ≡ (x ∼⁺⟨ r ⟩ s) → q ≡ s
 ∼⁺⟨⟩-injectiveʳ refl = refl


text:
-- Intuitionistic propositional calculus.
-- Hilbert-style formalisation of syntax.
-- Nested terms.

module IPC.Syntax.Hilbert where

open import IPC.Syntax.Common public

-- Derivations.

infix 3 _⊢_
data _⊢_ (Γ : Cx Ty) : Ty → Set where
  var   : ∀ {A}     → A ∈ Γ → Γ ⊢ A
  app   : ∀ {A B}   → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
  ci    : ∀ {A}     → Γ ⊢ A ▻ A
  ck    : ∀ {A B}   → Γ ⊢ A ▻ B ▻ A
  cs    : ∀ {A B C} → Γ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
  cpair : ∀ {A B}   → Γ ⊢ A ▻ B ▻ A ∧ B
  cfst  : ∀ {A B}   → Γ ⊢ A ∧ B ▻ A
  csnd  : ∀ {A B}   → Γ ⊢ A ∧ B ▻ B
  unit  : Γ ⊢ ⊤
  cboom : ∀ {C}     → Γ ⊢ ⊥ ▻ C
  cinl  : ∀ {A B}   → Γ ⊢ A ▻ A ∨ B
  cinr  : ∀ {A B}   → Γ ⊢ B ▻ A ∨ B
  ccase : ∀ {A B C} → Γ ⊢ A ∨ B ▻ (A ▻ C) ▻ (B ▻ C) ▻ C

infix 3 _⊢⋆_
_⊢⋆_ : Cx Ty → Cx Ty → Set
Γ ⊢⋆ ∅     = 𝟙
Γ ⊢⋆ Ξ , A = Γ ⊢⋆ Ξ × Γ ⊢ A

-- Monotonicity with respect to context inclusion.

mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
mono⊢ η (var i)   = var (mono∈ η i)
mono⊢ η (app t u) = app (mono⊢ η t) (mono⊢ η u)
mono⊢ η ci        = ci
mono⊢ η ck        = ck
mono⊢ η cs        = cs
mono⊢ η cpair     = cpair
mono⊢ η cfst      = cfst
mono⊢ η csnd      = csnd
mono⊢ η unit      = unit
mono⊢ η cboom     = cboom
mono⊢ η cinl      = cinl
mono⊢ η cinr      = cinr
mono⊢ η ccase     = ccase

mono⊢⋆ : ∀ {Γ″ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ Γ″ → Γ′ ⊢⋆ Γ″
mono⊢⋆ {∅}      η ∙        = ∙
mono⊢⋆ {Γ″ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Shorthand for variables.

v₀ : ∀ {A Γ} → Γ , A ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ} → Γ , A , B ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ} → Γ , A , B , C ⊢ A
v₂ = var i₂

-- Reflexivity.

refl⊢⋆ : ∀ {Γ} → Γ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

-- Deduction theorem.

lam : ∀ {A B Γ} → Γ , A ⊢ B → Γ ⊢ A ▻ B
lam (var top)     = ci
lam (var (pop i)) = app ck (var i)
lam (app t u)     = app (app cs (lam t)) (lam u)
lam ci            = app ck ci
lam ck            = app ck ck
lam cs            = app ck cs
lam cpair         = app ck cpair
lam cfst          = app ck cfst
lam csnd          = app ck csnd
lam unit          = app ck unit
lam cboom         = app ck cboom
lam cinl          = app ck cinl
lam cinr          = app ck cinr
lam ccase         = app ck ccase

lam⋆ : ∀ {Ξ Γ A} → Γ ⧺ Ξ ⊢ A → Γ ⊢ Ξ ▻⋯▻ A
lam⋆ {∅}     = I
lam⋆ {Ξ , B} = lam⋆ {Ξ} ∘ lam

lam⋆₀ : ∀ {Γ A} → Γ ⊢ A → ∅ ⊢ Γ ▻⋯▻ A
lam⋆₀ {∅}     = I
lam⋆₀ {Γ , B} = lam⋆₀ ∘ lam

-- Detachment theorem.

det : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ , A ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

det⋆ : ∀ {Ξ Γ A} → Γ ⊢ Ξ ▻⋯▻ A → Γ ⧺ Ξ ⊢ A
det⋆ {∅}     = I
det⋆ {Ξ , B} = det ∘ det⋆ {Ξ}

det⋆₀ : ∀ {Γ A} → ∅ ⊢ Γ ▻⋯▻ A → Γ ⊢ A
det⋆₀ {∅}     = I
det⋆₀ {Γ , B} = det ∘ det⋆₀

-- Cut and multicut.

cut : ∀ {A B Γ} → Γ ⊢ A → Γ , A ⊢ B → Γ ⊢ B
cut t u = app (lam u) t

multicut : ∀ {Ξ A Γ} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

-- Transitivity.

trans⊢⋆ : ∀ {Γ″ Γ′ Γ} → Γ ⊢⋆ Γ′ → Γ′ ⊢⋆ Γ″ → Γ ⊢⋆ Γ″
trans⊢⋆ {∅}      ts ∙        = ∙
trans⊢⋆ {Γ″ , A} ts (us , u) = trans⊢⋆ ts us , multicut ts u

-- Contraction.

ccont : ∀ {A B Γ} → Γ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ} → Γ , A , A ⊢ B → Γ , A ⊢ B
cont t = det (app ccont (lam (lam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ} → Γ , A , B ⊢ C → Γ , B , A ⊢ C
exch t = det (det (app cexch (lam (lam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C Γ} → Γ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ} → Γ , B ⊢ C → Γ , A ⊢ B → Γ , A ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

-- Useful theorems in functional form.

pair : ∀ {A B Γ} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
pair t u = app (app cpair t) u

fst : ∀ {A B Γ} → Γ ⊢ A ∧ B → Γ ⊢ A
fst t = app cfst t

snd : ∀ {A B Γ} → Γ ⊢ A ∧ B → Γ ⊢ B
snd t = app csnd t

boom : ∀ {C Γ} → Γ ⊢ ⊥ → Γ ⊢ C
boom t = app cboom t

inl : ∀ {A B Γ} → Γ ⊢ A → Γ ⊢ A ∨ B
inl t = app cinl t

inr : ∀ {A B Γ} → Γ ⊢ B → Γ ⊢ A ∨ B
inr t = app cinr t

case : ∀ {A B C Γ} → Γ ⊢ A ∨ B → Γ , A ⊢ C → Γ , B ⊢ C → Γ ⊢ C
case t u v = app (app (app ccase t) (lam u)) (lam v)

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ → Γ , A ⊢ B → Γ′ ⊢ A → Γ ⧺ Γ′ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

-- Convertibility.

data _⋙_ {Γ : Cx Ty} : ∀ {A} → Γ ⊢ A → Γ ⊢ A → Set where
  refl⋙     : ∀ {A} → {t : Γ ⊢ A}
                     → t ⋙ t

  trans⋙    : ∀ {A} → {t t′ t″ : Γ ⊢ A}
                     → t ⋙ t′ → t′ ⋙ t″
                     → t ⋙ t″

  sym⋙      : ∀ {A} → {t t′ : Γ ⊢ A}
                     → t ⋙ t′
                     → t′ ⋙ t

  congapp⋙  : ∀ {A B} → {t t′ : Γ ⊢ A ▻ B} → {u u′ : Γ ⊢ A}
                       → t ⋙ t′ → u ⋙ u′
                       → app t u ⋙ app t′ u′

  congi⋙    : ∀ {A} → {t t′ : Γ ⊢ A}
                     → t ⋙ t′
                     → app ci t ⋙ app ci t′

  congk⋙    : ∀ {A B} → {t t′ : Γ ⊢ A} → {u u′ : Γ ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app ck t) u ⋙ app (app ck t′) u′

  congs⋙    : ∀ {A B C} → {t t′ : Γ ⊢ A ▻ B ▻ C} → {u u′ : Γ ⊢ A ▻ B} → {v v′ : Γ ⊢ A}
                         → t ⋙ t′ → u ⋙ u′ → v ⋙ v′
                         → app (app (app cs t) u) v ⋙ app (app (app cs t′) u′) v′

  congpair⋙ : ∀ {A B} → {t t′ : Γ ⊢ A} → {u u′ : Γ ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app cpair t) u ⋙ app (app cpair t′) u′

  congfst⋙  : ∀ {A B} → {t t′ : Γ ⊢ A ∧ B}
                       → t ⋙ t′
                       → app cfst t ⋙ app cfst t′

  congsnd⋙  : ∀ {A B} → {t t′ : Γ ⊢ A ∧ B}
                       → t ⋙ t′
                       → app csnd t ⋙ app csnd t′

  congboom⋙ : ∀ {C} → {t t′ : Γ ⊢ ⊥}
                     → t ⋙ t′
                     → app (cboom {C = C}) t ⋙ app cboom t′

  conginl⋙  : ∀ {A B} → {t t′ : Γ ⊢ A}
                       → t ⋙ t′
                       → app (cinl {A = A} {B}) t ⋙ app cinl t′

  conginr⋙  : ∀ {A B} → {t t′ : Γ ⊢ B}
                       → t ⋙ t′
                       → app (cinr {A = A} {B}) t ⋙ app cinr t′

  congcase⋙ : ∀ {A B C} → {t t′ : Γ ⊢ A ∨ B} → {u u′ : Γ ⊢ A ▻ C} → {v v′ : Γ ⊢ B ▻ C}
                         → t ⋙ t′ → u ⋙ u′ → v ⋙ v′
                         → app (app (app ccase t) u) v ⋙ app (app (app ccase t′) u′) v′

  -- TODO: Verify this.
  beta▻ₖ⋙   : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                       → app (app ck t) u ⋙ t

  -- TODO: Verify this.
  beta▻ₛ⋙   : ∀ {A B C} → {t : Γ ⊢ A ▻ B ▻ C} → {u : Γ ⊢ A ▻ B} → {v : Γ ⊢ A}
                         → app (app (app cs t) u) v ⋙ app (app t v) (app u v)

  -- TODO: What about eta for ▻?

  beta∧₁⋙   : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                       → app cfst (app (app cpair t) u) ⋙ t

  beta∧₂⋙   : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                       → app csnd (app (app cpair t) u) ⋙ u

  eta∧⋙     : ∀ {A B} → {t : Γ ⊢ A ∧ B}
                       → t ⋙ app (app cpair (app cfst t)) (app csnd t)

  eta⊤⋙    : ∀ {t : Γ ⊢ ⊤} → t ⋙ unit

  -- TODO: Verify this.
  beta∨₁⋙   : ∀ {A B C} → {t : Γ ⊢ A} → {u : Γ ⊢ A ▻ C} → {v : Γ ⊢ B ▻ C}
               → app (app (app ccase (app cinl t)) u) v ⋙ app u t

  -- TODO: Verify this.
  beta∨₂⋙   : ∀ {A B C} → {t : Γ ⊢ B} → {u : Γ ⊢ A ▻ C} → {v : Γ ⊢ B ▻ C}
               → app (app (app ccase (app cinr t)) u) v ⋙ app v t

  -- TODO: What about eta and commuting conversions for ∨? What about ⊥?

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-

Add axioms (i.e., propositions) to a structure S without changing the definition of structured equivalence.

X ↦ Σ[ s ∈ S X ] (P X s) where (P X s) is a proposition for all X and s.

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Axioms where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Foundations.SIP
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ₁ ℓ₁' ℓ₂ : Level

AxiomsStructure : (S : Type ℓ → Type ℓ₁)
  (axioms : (X : Type ℓ) → S X → Type ℓ₂)
  → Type ℓ → Type (ℓ-max ℓ₁ ℓ₂)
AxiomsStructure S axioms X = Σ[ s ∈ S X ] (axioms X s)

AxiomsEquivStr : {S : Type ℓ → Type ℓ₁} (ι : StrEquiv S ℓ₁')
  (axioms : (X : Type ℓ) → S X → Type ℓ₂)
  → StrEquiv (AxiomsStructure S axioms) ℓ₁'
AxiomsEquivStr ι axioms (X , (s , a)) (Y , (t , b)) e = ι (X , s) (Y , t) e

axiomsUnivalentStr : {S : Type ℓ → Type ℓ₁}
  (ι : (A B : TypeWithStr ℓ S) → A .fst ≃ B .fst → Type ℓ₁')
  {axioms : (X : Type ℓ) → S X → Type ℓ₂}
  (axioms-are-Props : (X : Type ℓ) (s : S X) → isProp (axioms X s))
  (θ : UnivalentStr S ι)
  → UnivalentStr (AxiomsStructure S axioms) (AxiomsEquivStr ι axioms)
axiomsUnivalentStr {S = S} ι {axioms = axioms} axioms-are-Props θ {X , s , a} {Y , t , b} e =
  ι (X , s) (Y , t) e
    ≃⟨ θ e ⟩
  PathP (λ i → S (ua e i)) s t
    ≃⟨ invEquiv (Σ-contractSnd λ _ → isOfHLevelPathP' 0 (axioms-are-Props _ _) _ _) ⟩
  Σ[ p ∈ PathP (λ i → S (ua e i)) s t ] PathP (λ i → axioms (ua e i) (p i)) a b
    ≃⟨ ΣPath≃PathΣ ⟩
  PathP (λ i → AxiomsStructure S axioms (ua e i)) (s , a) (t , b)
  ■

inducedStructure : {S : Type ℓ → Type ℓ₁}
  {ι : (A B : TypeWithStr ℓ S) → A .fst ≃ B .fst → Type ℓ₁'}
  (θ : UnivalentStr S ι)
  {axioms : (X : Type ℓ) → S X → Type ℓ₂}
  (A : TypeWithStr ℓ (AxiomsStructure S axioms)) (B : TypeWithStr ℓ S)
  → (typ A , str A .fst) ≃[ ι ] B
  → TypeWithStr ℓ (AxiomsStructure S axioms)
inducedStructure θ {axioms} A B eqv =
  B .fst , B .snd , subst (uncurry axioms) (sip θ _ _ eqv) (A .snd .snd)

transferAxioms : {S : Type ℓ → Type ℓ₁}
  {ι : (A B : TypeWithStr ℓ S) → A .fst ≃ B .fst → Type ℓ₁'}
  (θ : UnivalentStr S ι)
  {axioms : (X : Type ℓ) → S X → Type ℓ₂}
  (A : TypeWithStr ℓ (AxiomsStructure S axioms)) (B : TypeWithStr ℓ S)
  → (typ A , str A .fst) ≃[ ι ] B
  → axioms (fst B) (snd B)
transferAxioms θ {axioms} A B eqv =
  subst (uncurry axioms) (sip θ _ _ eqv) (A .snd .snd)


text:
module OldBasicILP.Syntax.Common where

open import Common.ContextPair public


text:
module Algebra.LabelledGraph.Reasoning where

open import Algebra.Dioid
open import Algebra.LabelledGraph

-- Standard syntax sugar for writing equational proofs
infix 4 _≈_
data _≈_ {A B eq} {d : Dioid B eq} (x y : LabelledGraph d A) : Set where
    prove : x ≡ y -> x ≈ y

infix 1 begin_
begin_ : ∀ {A B eq} {d : Dioid B eq} {x y : LabelledGraph d A} -> x ≈ y -> x ≡ y
begin prove p = p

infixr 2 _≡⟨_⟩_
_≡⟨_⟩_ : ∀ {A B eq} {d : Dioid B eq} (x : LabelledGraph d A) {y z : LabelledGraph d A} -> x ≡ y -> y ≈ z -> x ≈ z
_ ≡⟨ p ⟩ prove q = prove (transitivity p q)

infix 3 _∎
_∎ : ∀ {A B eq} {d : Dioid B eq} (x : LabelledGraph d A) -> x ≈ x
_∎ _ = prove reflexivity

infixl 8 _>>_
_>>_ : ∀ {A B eq} {d : Dioid B eq} {x y z : LabelledGraph d A} -> x ≡ y -> y ≡ z -> x ≡ z
_>>_ = transitivity

L : ∀ {A B eq} {d : Dioid B eq} {x y z : LabelledGraph d A} {r : B} -> x ≡ y -> x [ r ]> z ≡ y [ r ]> z
L = left-congruence

R : ∀ {A B eq} {d : Dioid B eq} {x y z : LabelledGraph d A} {r : B} -> x ≡ y -> z [ r ]> x ≡ z [ r ]> y
R = right-congruence

max_stars_repo_name: snowleopard/alga-proofs

max_issues_repo_name: snowleopard/alga-proofs

max_forks_repo_name: snowleopard/alga-proofs


text:
module Type.Category.ExtensionalFunctionsCategory.HomFunctor where

import      Functional as Fn
open import Function.Proofs
open import Function.Equals
open import Function.Equals.Proofs
open import Logic.Predicate
import      Lvl
import      Relator.Equals.Proofs.Equiv
open import Structure.Category
open import Structure.Category.Dual
open import Structure.Category.Functor
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type.Category.ExtensionalFunctionsCategory
open import Type

private variable ℓ ℓₒ ℓₘ ℓₑ : Lvl.Level

-- Note: This is implicitly using the identity type as the equivalence for (_⟶_).
module _ {Obj : Type{ℓₒ}} {_⟶_ : Obj → Obj → Type{ℓₘ}} (C : Category(_⟶_)) where
  open Category(C)

  covariantHomFunctor : Obj → ((intro C) →ᶠᵘⁿᶜᵗᵒʳ typeExtensionalFnCategoryObject{ℓₘ})
  ∃.witness (covariantHomFunctor x) y = (x ⟶ y)
  Functor.map (∃.proof (covariantHomFunctor _)) = (_∘_)
  _⊜_.proof (Function.congruence (Functor.map-function (∃.proof (covariantHomFunctor _))) {f₁} {f₂} f₁f₂) {g} = congruence₂ₗ(_∘_) ⦃ binaryOperator ⦄ g f₁f₂
  _⊜_.proof (Functor.op-preserving (∃.proof (covariantHomFunctor _))) = Morphism.associativity(_∘_)
  _⊜_.proof (Functor.id-preserving (∃.proof (covariantHomFunctor _))) = Morphism.identityₗ(_∘_)(id)

  contravariantHomFunctor : Obj → (dual(intro C) →ᶠᵘⁿᶜᵗᵒʳ typeExtensionalFnCategoryObject{ℓₘ})
  ∃.witness (contravariantHomFunctor x) y = (y ⟶ x)
  Functor.map (∃.proof (contravariantHomFunctor _)) = Fn.swap(_∘_)
  _⊜_.proof (Function.congruence (Functor.map-function (∃.proof (contravariantHomFunctor _))) {g₁} {g₂} g₁g₂) {f} = congruence₂ᵣ(_∘_) ⦃ binaryOperator ⦄ f g₁g₂
  _⊜_.proof (Functor.op-preserving (∃.proof (contravariantHomFunctor _))) = symmetry(_) (Morphism.associativity(_∘_))
  _⊜_.proof (Functor.id-preserving (∃.proof (contravariantHomFunctor _))) = Morphism.identityᵣ(_∘_)(id)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K #-}
module pointed.core where

open import sum
open import equality.core
open import function.core
open import function.isomorphism.core

PSet : ∀ i → Set _
PSet i = Σ (Set i) λ X → X

PMap : ∀ {i j} → PSet i → PSet j → Set _
PMap (X , x) (Y , y) = Σ (X → Y) λ f → f x ≡ y

_∘P_ : ∀ {i j k}{𝓧 : PSet i}{𝓨 : PSet j}{𝓩 : PSet k}
     → PMap 𝓨 𝓩 → PMap 𝓧 𝓨 → PMap 𝓧 𝓩
(g , q) ∘P (f , p) = (g ∘ f , ap g p · q)

instance
  pmap-comp : ∀ {i j k} → Composition _ _ _ _ _ _
  pmap-comp {i}{j}{k} = record
    { U₁ = PSet i
    ; U₂ = PSet j
    ; U₃ = PSet k
    ; hom₁₂ = PMap
    ; hom₂₃ = PMap
    ; hom₁₃ = PMap
    ; _∘_ = _∘P_ }

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

open import lib.Basics

module lib.types.FreeGroup where

module _ {i} where

  private
    data #FreeGroup-aux (A : Type i) : Type i where
      #fg-nil : #FreeGroup-aux A
      _#fg::_ : A → #FreeGroup-aux A → #FreeGroup-aux A
      _#fg-inv::_ : A → #FreeGroup-aux A → #FreeGroup-aux A

    {- Is this okay?  The template is to have 'data' here,
     - but then the β rules for paths will not typecheck.
     -}
    record #FreeGroup (A : Type i) : Type i where
      constructor
        #freegroup
      field
        #freegroup-proj : #FreeGroup-aux A
        #freegroup-unit : Unit → Unit

  FreeGroup : (A : Type i) → Type i
  FreeGroup A = #FreeGroup A

  module _ {A : Type i} where

    fg-nil : FreeGroup A
    fg-nil = #freegroup #fg-nil _

    infixr 60 _fg::_
    _fg::_ : A → FreeGroup A → FreeGroup A
    a fg:: (#freegroup fg _) = #freegroup (a #fg:: fg) _

    infixr 60 _fg-inv::_
    _fg-inv::_ : A → FreeGroup A → FreeGroup A
    a fg-inv:: (#freegroup fg _) = #freegroup (a #fg-inv:: fg) _

    postulate  -- HIT
      fg-inv-l : ∀ (a : A) → (fg : FreeGroup A) → a fg-inv:: a     fg:: fg == fg
      fg-inv-r : ∀ (a : A) → (fg : FreeGroup A) → a fg::     a fg-inv:: fg == fg

    postulate  -- HIT
      FreeGroup-level : is-set (FreeGroup A)

    FreeGroup-is-set = FreeGroup-level

    module FreeGroupElim {j} {P : FreeGroup A → Type j}
      (p : (x : FreeGroup A) → is-set (P x)) (nil* : P fg-nil)
      (_fg::*_ : ∀ a {fg} (fg* : P fg) → P (a fg:: fg))
      (_fg-inv::*_ : ∀ a {fg} (fg* : P fg) → P (a fg-inv:: fg))
      (fg-inv-l* : ∀ a {fg} (fg* : P fg) → (a fg-inv::* (a     fg::* fg*)) == fg* [ P ↓ fg-inv-l a fg ] )
      (fg-inv-r* : ∀ a {fg} (fg* : P fg) → (a fg::*     (a fg-inv::* fg*)) == fg* [ P ↓ fg-inv-r a fg ]) where

      f : Π (FreeGroup A) P
      f = f-aux phantom phantom phantom where

        f-aux* : Π (#FreeGroup-aux A) (P ∘ (λ fg → #freegroup fg _))
        f-aux* #fg-nil = nil*
        f-aux* (a #fg:: fg) = a fg::* f-aux* fg
        f-aux* (a #fg-inv:: fg) = a fg-inv::* f-aux* fg

        f-aux : Phantom p → Phantom fg-inv-l* → Phantom fg-inv-r*
          → Π (FreeGroup A) P
        f-aux phantom phantom phantom (#freegroup fg _) = f-aux* fg

      postulate  -- HIT
        fg-inv-l-β : ∀ a fg → apd f (fg-inv-l a fg) == fg-inv-l* a (f fg)
        fg-inv-r-β : ∀ a fg → apd f (fg-inv-r a fg) == fg-inv-r* a (f fg)

open FreeGroupElim public renaming (f to FreeGroup-elim)

module FreeGroupRec {i} {A : Type i} {j} {B : Type j} (p : is-set B)
  (nil* : B) (_fg::*[_]_ : A → FreeGroup A → B → B) (_fg-inv::*[_]_ : A → FreeGroup A → B → B)
  (fg-inv-l* : ∀ a {fg} fg* → (a fg-inv::*[ a     fg:: fg ] (a     fg::*[ fg ] fg*)) == fg*)
  (fg-inv-r* : ∀ a {fg} fg* → (a     fg::*[ a fg-inv:: fg ] (a fg-inv::*[ fg ] fg*)) == fg*) where

  private
    module M = FreeGroupElim (λ x → p) nil*
      (λ a {fg} fg* → a     fg::*[ fg ] fg*)
      (λ a {fg} fg* → a fg-inv::*[ fg ] fg*)
      (λ a {fg} fg* → ↓-cst-in (fg-inv-l* a {fg} fg*))
      (λ a {fg} fg* → ↓-cst-in (fg-inv-r* a {fg} fg*))

  f : FreeGroup A → B
  f = M.f

open FreeGroupRec public renaming (f to FreeGroup-rec)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Commutative semirings with some additional structure ("almost"
-- commutative rings), used by the ring solver
------------------------------------------------------------------------

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

module Algebra.Solver.Ring.AlmostCommutativeRing where

open import Relation.Binary
open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties
import Algebra.Morphism as Morphism
open import Function
open import Level

------------------------------------------------------------------------
-- Definitions

record IsAlmostCommutativeRing
         {a ℓ} {A : Set a} (_≈_ : Rel A ℓ)
         (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
    -‿cong                : -_ Preserves _≈_ ⟶ _≈_
    -‿*-distribˡ          : ∀ x y → ((- x) * y)     ≈ (- (x * y))
    -‿+-comm              : ∀ x y → ((- x) + (- y)) ≈ (- (x + y))

  open IsCommutativeSemiring isCommutativeSemiring public

record AlmostCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier                 : Set c
    _≈_                     : Rel Carrier ℓ
    _+_                     : Op₂ Carrier
    _*_                     : Op₂ Carrier
    -_                      : Op₁ Carrier
    0#                      : Carrier
    1#                      : Carrier
    isAlmostCommutativeRing :
      IsAlmostCommutativeRing _≈_ _+_ _*_ -_ 0# 1#

  open IsAlmostCommutativeRing isAlmostCommutativeRing public

  commutativeSemiring : CommutativeSemiring _ _
  commutativeSemiring =
    record { isCommutativeSemiring = isCommutativeSemiring }

  open CommutativeSemiring commutativeSemiring public
         using ( +-semigroup; +-monoid; +-commutativeMonoid
               ; *-semigroup; *-monoid; *-commutativeMonoid
               ; semiring
               )

  rawRing : RawRing _
  rawRing = record
    { _+_ = _+_
    ; _*_ = _*_
    ; -_  = -_
    ; 0#  = 0#
    ; 1#  = 1#
    }

------------------------------------------------------------------------
-- Homomorphisms

record _-Raw-AlmostCommutative⟶_
         {r₁ r₂ r₃}
         (From : RawRing r₁)
         (To : AlmostCommutativeRing r₂ r₃) : Set (r₁ ⊔ r₂ ⊔ r₃) where
  private
    module F = RawRing From
    module T = AlmostCommutativeRing To
  open Morphism.Definitions F.Carrier T.Carrier T._≈_
  field
    ⟦_⟧    : Morphism
    +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
    *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
    -‿homo : Homomorphic₁ ⟦_⟧ F.-_  T.-_
    0-homo : Homomorphic₀ ⟦_⟧ F.0#  T.0#
    1-homo : Homomorphic₀ ⟦_⟧ F.1#  T.1#

-raw-almostCommutative⟶
  : ∀ {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂) →
    AlmostCommutativeRing.rawRing R -Raw-AlmostCommutative⟶ R
-raw-almostCommutative⟶ R = record
  { ⟦_⟧    = id
  ; +-homo = λ _ _ → refl
  ; *-homo = λ _ _ → refl
  ; -‿homo = λ _ → refl
  ; 0-homo = refl
  ; 1-homo = refl
  }
  where open AlmostCommutativeRing R

-- A homomorphism induces a notion of equivalence on the raw ring.

Induced-equivalence :
  ∀ {c₁ c₂ ℓ} {Coeff : RawRing c₁} {R : AlmostCommutativeRing c₂ ℓ} →
  Coeff -Raw-AlmostCommutative⟶ R → Rel (RawRing.Carrier Coeff) ℓ
Induced-equivalence {R = R} morphism a b = ⟦ a ⟧ ≈ ⟦ b ⟧
  where
  open AlmostCommutativeRing R
  open _-Raw-AlmostCommutative⟶_ morphism

------------------------------------------------------------------------
-- Conversions

-- Commutative rings are almost commutative rings.

fromCommutativeRing :
  ∀ {r₁ r₂} → CommutativeRing r₁ r₂ → AlmostCommutativeRing _ _
fromCommutativeRing CR = record
  { isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿cong                = -‿cong
      ; -‿*-distribˡ          = -‿*-distribˡ
      ; -‿+-comm              = ⁻¹-∙-comm
      }
  }
  where
  open CommutativeRing CR
  import Algebra.Properties.Ring as R; open R ring
  import Algebra.Properties.AbelianGroup as AG; open AG +-abelianGroup

-- Commutative semirings can be viewed as almost commutative rings by
-- using identity as the "almost negation".

fromCommutativeSemiring :
  ∀ {r₁ r₂} → CommutativeSemiring r₁ r₂ → AlmostCommutativeRing _ _
fromCommutativeSemiring CS = record
  { -_                      = id
  ; isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿cong                = id
      ; -‿*-distribˡ          = λ _ _ → refl
      ; -‿+-comm              = λ _ _ → refl
      }
  }
  where open CommutativeSemiring CS


text:
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

macro

  m : Term → TC ⊤
  m _ =
    bindTC (quoteTC (Set → @0 Set → Set)) λ t →
    typeError (termErr t ∷ [])

_ : Set
_ = m

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

import Level as L
open import Data.Fin hiding (fromℕ; toℕ)
open import Data.Nat
open import Data.Product
open import Data.List
open import Function renaming (_∘_ to _○_)

open import HoTT
open import FT
open import FT-Nat
import Equivalences as E
open import Path2Equiv

{--
1. postulate path2equiv
2. show that (FT, path) is equivalent to (FinSet, bijections) as categories
3. show that [[ ]]: (B, <->) -> (Set, function) is a functor
   [where (Set is Agda's Set)].
--}

{--
Categories, functors, etc. adapted from:
http://wiki.portal.chalmers.se/agda/uploads/Main.Libraries/20110915Category.agda

Consider using:
https://github.com/tomprince/agda-categories
https://github.com/tomprince/agda-categories/blob/master/Categories/Category.agda
--}

------------------------------------------------------------------
-- Categories

record Setoid (a b : L.Level) : Set (L.suc (a L.⊔ b)) where
  infix 2 _∼_
  field
    object : Set a
    _∼_ : object → object → Set b
    refl∼ : {x : object} → x ∼ x
    sym∼ : {x y : object} → x ∼ y → y ∼ x
    trans∼ : {x y z : object} → y ∼ z → x ∼ y → x ∼ z

strictSetoid : ∀ {a} → Set a → Setoid a a
strictSetoid A = record
  { object = A
  ; _∼_ = _≡_
  ; refl∼ = λ {x} → refl x
  ; sym∼ = !
  ; trans∼ = λ q p → p ∘ q
  }

∥_∥ : ∀ {a b c} {X : Set a} → (h : X → X → Setoid b c) → (x y : X) → Set b
∥ h ∥ x y = Setoid.object (h x y)

record Cat (a b c : L.Level) : Set (L.suc (a L.⊔ b L.⊔ c)) where
  field
    object : Set a
    hom : object → object → Setoid b c
    identity : (x : object) → ∥ hom ∥ x x
    comp : {x y z : object} → ∥ hom ∥ y z → ∥ hom ∥ x y → ∥ hom ∥ x z
    comp∼ : {x y z : object} →
             {g0 g1 : ∥ hom ∥ y z} → {f0 f1 : ∥ hom ∥ x y} →
             (g0∼g1 : let open Setoid (hom y z) in g0 ∼ g1) →
             (f0∼f1 : let open Setoid (hom x y) in f0 ∼ f1) →
             let open Setoid (hom x z) in comp g0 f0 ∼ comp g1 f1
    associativity∼ : {w x y z : object} →
      (f : ∥ hom ∥ y z) → (g : ∥ hom ∥ x y) → (h : ∥ hom ∥ w x) →
      let open Setoid (hom w z) in comp (comp f g) h ∼ comp f (comp g h)
    left-identity∼ : {x y : object} → (f : ∥ hom ∥ x y) →
      let open Setoid (hom x y) in comp (identity y) f ∼ f
    right-identity∼ : {x y : object} → (f : ∥ hom ∥ x y) →
      let open Setoid (hom x y) in comp f (identity x) ∼ f

-- the type of objects in category C
ob : ∀ {a b c} → Cat a b c → Set a
ob C = Cat.object C

-- the type of morphisms between two given objects in C
_〈_,_〉 : ∀ {a b c} → (C : Cat a b c) → ob C → ob C → Set b
C 〈 X , Y 〉 = ∥ Cat.hom C ∥ X Y

-- the type of identities of morphisms
_∣_∼_ : ∀ {a b c} → (C : Cat a b c) → {X Y : ob C} →
        C 〈 X , Y 〉 → C 〈 X , Y 〉 → Set c
_∣_∼_ C {X} {Y} f g = Setoid._∼_ (Cat.hom C X Y) f g

-- convenient abbreviation for identity morphism
idC : ∀ {a b c} → (C : Cat a b c) → (x : ob C) → C 〈 x , x 〉
idC C x = Cat.identity C x

-- convenient abbreviation for composition of morphisms
_∣_∘_ : ∀ {a b c} → (C : Cat a b c) → {x y z : ob C } →
        C 〈 y , z 〉 → C 〈 x , y 〉 → C 〈 x , z 〉
C ∣ g ∘ f = Cat.comp C g f

------------------------------------------------------------------
-- Functors
record _=>_ {a b c a' b' c'} (C : Cat a b c) (D : Cat a' b' c') :
  Set (a L.⊔ a' L.⊔ b L.⊔ b' L.⊔ c L.⊔ c') where
  field
    object : ob C  → ob D
    hom : {X Y : ob C} →
      C 〈 X , Y 〉 → D 〈 object X , object Y 〉
    hom∼ : {X Y : ob C} → (f g : C 〈 X , Y 〉) →
      (f∼g : C ∣ f ∼ g) → D ∣ hom f ∼ hom g
    identity∼ : {X : ob C} →
      D ∣ hom (idC C X) ∼ idC D (object X)
    comp∼ : {X Y Z : ob C} → (f : C 〈 Y , Z 〉) → (g : C 〈 X , Y 〉) →
      D ∣ hom (C ∣ f ∘ g) ∼ (D ∣ hom f ∘ hom g)

-- Applying the functor to objects
_`_ : ∀ {a b c a' b' c'} {X : Cat a b c} → {Y : Cat a' b' c'} →
  X => Y → ob X → ob Y
F ` x = _=>_.object F x

-- Applying the functor to morphisms
_``_ : ∀ {a b c a' b' c'} {X : Cat a b c} → {Y : Cat a' b' c'} →
  {x0 x1 : ob X} → (F : X => Y) → X 〈 x0 , x1 〉 → Y 〈 F ` x0 , F ` x1 〉
F `` f = _=>_.hom F f

------------------------------------------------------------------
-- The category (FinSet,bijections)
-- M, N, L are finite sets witnessed by their sizes m, n, l
-- F, G, H are bijections

-- bijections between two sets M and N
record Bijection (m n : ℕ) : Set where
  field
    f : Fin m → Fin n
    g : Fin n → Fin m
    injective  : {x y : Fin m} → f x ≡ f y → x ≡ y
    surjective : {x : Fin n} → f (g x) ≡ x

-- there is a bijection from each set to itself
idBijection : (m : ℕ) → Bijection m m
idBijection m = record {
    f = id ;
    g = id ;
    injective = id ;
    surjective = λ {x} → refl x
  }

-- composition of bijections
∘Bijection : {m n l : ℕ} → Bijection n l → Bijection m n → Bijection m l
∘Bijection G F = record {
    f = Bijection.f G ○ Bijection.f F ;
    g = Bijection.g F ○ Bijection.g G ;
    injective = λ α → Bijection.injective F (Bijection.injective G α) ;
    surjective = λ {x} →
      Bijection.f G (Bijection.f F (Bijection.g F (Bijection.g G x)))
        ≡⟨ ap (λ x → Bijection.f G x) (Bijection.surjective F) ⟩
      Bijection.f G (Bijection.g G x)
        ≡⟨ Bijection.surjective G ⟩
      x ∎
  }

-- two bijections are the "same" if they agree modulo ≡
∼Bijection : {m n : ℕ} → Bijection m n → Bijection m n → Set
∼Bijection F G = (Bijection.f F) E.∼ (Bijection.f G)

-- the set of all bijections between two sets M and N taken modulo ≡
BijectionSetoid : (m n : ℕ) → Setoid L.zero L.zero
BijectionSetoid m n = record {
    object = Bijection m n ;
    _∼_ = ∼Bijection ;
    refl∼ = λ {F} → E.refl∼ {f = Bijection.f F} ;
    sym∼ = λ {F} {G} →
             E.sym∼ {f = Bijection.f F} {g = Bijection.f G} ;
    trans∼ = λ {F} {G} {H} P Q →
               E.trans∼ {f = Bijection.f F}
                        {g = Bijection.f G}
                        {h = Bijection.f H}
                        Q P
    }

-- the category of finite sets and bijections
FinCat : Cat L.zero L.zero L.zero
FinCat = record {
          object = ℕ ;
          hom = BijectionSetoid ;
          identity = idBijection ;
          comp = λ G F → ∘Bijection G F ;
          comp∼ = λ {m} {n} {l} {G₀} {G₁} {F₀} {F₁} Q P x →
                    Bijection.f (∘Bijection G₀ F₀) x
                      ≡⟨ bydef ⟩
                    Bijection.f G₀ (Bijection.f F₀ x)
                      ≡⟨ ap (λ z → Bijection.f G₀ z) (P x) ⟩
                    Bijection.f G₀ (Bijection.f F₁ x)
                      ≡⟨ Q (Bijection.f F₁ x) ⟩
                    Bijection.f (∘Bijection G₁ F₁) x ∎ ;
          associativity∼  = λ F G H x →
            Bijection.f (∘Bijection F G) (Bijection.f H x)
              ≡⟨ bydef ⟩
            Bijection.f F (Bijection.f G (Bijection.f H x)) ∎ ;
          left-identity∼  = λ {m} {n} F x →
            Bijection.f (idBijection n) (Bijection.f F x)
              ≡⟨ bydef ⟩
            Bijection.f F x ∎ ;
          right-identity∼ = λ {m} {n} F x →
            Bijection.f F (Bijection.f (idBijection m) x)
              ≡⟨ bydef ⟩
            Bijection.f F x ∎
      }

------------------------------------------------------------------
-- The category (FinSet,HoTT-equivalence)
-- M, N, L are finite sets witnessed by their sizes m, n, l
-- F, G, H are equivalences

-- an equivalence (A ≃ B) consists of a function f : A → B
-- and a proof that it is an equivalence; the proof consists of
-- two functions g and h : B → A together with two proofs that
-- (f ○ g) ∼ id and (h ○ f) ∼ id
-- for now, I am suggesting that two such equivalences are the same
-- if the forward functions f are the same
∼Equiv : {m n : ℕ} → (Fin m E.≃ Fin n) → (Fin m E.≃ Fin n) → Set
∼Equiv F G = (proj₁ F) E.∼ (proj₁ G)

-- the set of all equivalences between two sets M and N taken modulo ≡
EquivSetoid : (m n : ℕ) → Setoid L.zero L.zero
EquivSetoid m n = record {
    object = (Fin m) E.≃ (Fin n) ;
    _∼_ = ∼Equiv ;
    refl∼ = λ {F} → E.refl∼ {f = proj₁ F} ;
    sym∼ = λ {F} {G} → E.sym∼ {f = proj₁ F} {g = proj₁ G} ;
    trans∼ = λ {F} {G} {H} P Q →
                E.trans∼ {f = proj₁ F} {g = proj₁ G} {h = proj₁ H} Q P
    }

FinCat' : Cat L.zero L.zero L.zero
FinCat' = record {
          object = ℕ ;
          hom = EquivSetoid ;
          identity = λ m → E.id≃ {A = Fin m} ;
          comp = λ q p → E.trans≃ p q ;
          comp∼ = λ {m} {n} {l} {G₀} {G₁} {F₀} {F₁} Q P x →
                    proj₁ (E.trans≃ F₀ G₀) x
                      ≡⟨ bydef ⟩
                    proj₁ G₀ (proj₁ F₀ x)
                      ≡⟨ ap (λ z → proj₁ G₀ z) (P x) ⟩
                    proj₁ G₀ (proj₁ F₁ x)
                      ≡⟨ Q (proj₁ F₁ x) ⟩
                    proj₁ (E.trans≃ F₁ G₁) x ∎ ;
          associativity∼  = λ F G H x → refl (proj₁ F (proj₁ G (proj₁ H x))) ;
          left-identity∼  = λ {m} {n} F x → refl (proj₁ F x) ;
          right-identity∼ = λ {m} {n} F x → refl (proj₁ F x)
      }

------------------------------------------------------------------
-- The category (FT,path)

-- evaluation
evalF : {b₁ b₂ : FT} → (b₁ ⇛ b₂) → ⟦ b₁ ⟧ → ⟦ b₂ ⟧
evalF p = proj₁ (path2equiv p)

-- could equivalently use sym≃ on the result of path2equiv p
evalB : {b₁ b₂ : FT} → (b₁ ⇛ b₂) → ⟦ b₂ ⟧ → ⟦ b₁ ⟧
evalB p = proj₁ (path2equiv (sym⇛ p))

-- equivalence of combinators
_∼c_ : {b₁ b₂ : FT} → (c₁ c₂ : b₁ ⇛ b₂) → Set
_∼c_ {b₁} {b₂} c₁ c₂ = (v : ⟦ b₁ ⟧) → evalF c₁ v ≡ evalF c₂ v

-- equivalence class of paths between two types
paths : FT → FT → Setoid L.zero L.zero
paths b₁ b₂ = record {
               object = b₁ ⇛ b₂ ;
               _∼_ = _∼c_ ;
               refl∼  = λ {c} v → refl (evalF c v) ;
               sym∼ = λ p v → ! (p v) ;
               trans∼ = λ q p v → (p v) ∘ (q v)
             }

-- the category of finite types and paths
FTCat : Cat L.zero L.zero L.zero
FTCat = record {
          object = FT ;
          hom = paths ;
          identity = λ b → id⇛ {b}  ;
          comp = λ c₂ c₁ → c₁ ◎ c₂ ;
          comp∼ = λ {b₀} {b₁} {b₂} {c₂} {c₂'} {c₁} {c₁'} q p v →
                    evalF (c₁ ◎ c₂) v
                      ≡⟨ bydef  ⟩
                    evalF c₂ (evalF c₁ v)
                      ≡⟨ ap (λ z → evalF c₂ z) (p v) ⟩
                    evalF c₂ (evalF c₁' v)
                      ≡⟨ q (evalF c₁' v) ⟩
                    evalF (c₁' ◎ c₂') v ∎ ;
          associativity∼  = λ r q p v →
            evalF (p ◎ (q ◎ r)) v
              ≡⟨ bydef ⟩
            evalF r (evalF q (evalF p v))
              ≡⟨ bydef ⟩
            evalF ((p ◎ q) ◎ r) v ∎ ;
          left-identity∼  = λ p v →
            evalF id⇛ (evalF p v)
              ≡⟨ bydef ⟩
             evalF p v ∎ ;
          right-identity∼ = λ p v →
            evalF p (evalF id⇛ v)
              ≡⟨ bydef ⟩
            evalF p v ∎
      }

------------------------------------------------------------------
{--
Two categories C and D are equivalent if we have:
- a functor F : C -> D
- a functor G : D -> C
- two natural isomorphisms ε : F ∘ G -> I_D and η : G ∘ F -> I_C

--}

ff : {m n : ℕ} → (Fin m E.≃ Fin n) → (fromℕ m ⇛ fromℕ n)
ff = {!!}

gg : {b₀ b₁ : FT} → (b₀ ⇛ b₁) → (Fin (suc (toℕ b₀)) E.≃ Fin (suc (toℕ b₁)))
gg = {!!}

-- functor from FinCat' to FTCat
fin2ft : FinCat' => FTCat
fin2ft = record {
    object = fromℕ ; -- (Fin 1) should map to ZERO
    hom = ff ;  --
    hom∼ = {!!} ;
    identity∼ = {!!} ;
    comp∼ = {!!}
  }

-- functor from FTCat to FinCat'
ft2fin : FTCat => FinCat'
ft2fin = record {
    object = λ b → suc (toℕ b) ; -- ZERO maps to (Fin 1)
    hom = gg ;
    hom∼ = {!!} ;
    identity∼ = {!!} ;
    comp∼ = {!!}
  }

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


text:
module L.Data.Bool.Core where

open import L.Base.Coproduct.Core
open import L.Base.Unit.Core

-- Deriving the introduction rule as a special case of Coproducts.
Bool : Set
Bool = ⊤ + ⊤

ff : Bool
ff = inr ⋆

tt : Bool
tt = inl ⋆

-- And the elimination rule
if : ∀{c} (C : Bool → Set c)
     → C tt → C ff → (e : Bool) → C e
if = λ C c d e → case C (λ _ → c) (λ _ → d) e

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


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

module HyperFalse where

open import Prelude hiding (false)

{-# NO_POSITIVITY_CHECK #-}
record _↬_ (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  inductive; constructor hyp
  field invoke : (B ↬ A) → B
open _↬_

yes? : ⊥ ↬ ⊥
yes? .invoke h = h .invoke h

no! : (⊥ ↬ ⊥) → ⊥
no! h = h .invoke h

boom : ⊥
boom = no! yes?

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2016-04-14 issue 1796 for rewrite

-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.size.solve:100 #-}
-- {-# OPTIONS -v tc.with.abstract:40 #-}

open import Common.Size
open import Common.Equality

data Either (A B : Set) : Set where
  left  : A → Either A B
  right : B → Either A B

either : {A B : Set} → Either A B →
  ∀{C : Set} → (A → C) → (B → C) → C
either (left a)  l r = l a
either (right b) l r = r b

data Nat : Size → Set where
  zero : ∀{i} → Nat (↑ i)
  suc  : ∀{i} → Nat i → Nat (↑ i)

primrec : ∀{ℓ} (C : Size → Set ℓ)
     → (z : ∀{i} → C i)
     → (s : ∀{i} → Nat i → C i → C (↑ i))
     → ∀{i} → Nat i → C i
primrec C z s zero    = z
primrec C z s (suc n) = s n (primrec C z s n)

case : ∀{i} → Nat i
     → ∀{ℓ} (C : Size → Set ℓ)
     → (z : ∀{i} → C i)
     → (s : ∀{i} → Nat i → C (↑ i))
     → C i
case n C z s = primrec C z (λ n r → s n) n

diff : ∀{i} → Nat i → ∀{j} → Nat j → Either (Nat i) (Nat j)
diff = primrec (λ i → ∀{j} → Nat j → Either (Nat i) (Nat j))
  -- case zero: the second number is bigger and the difference
  right
  -- case suc n:
  (λ{i} n r m  → case m (λ j → Either (Nat (↑ i)) (Nat j))
    -- subcase zero: the first number (suc n) is bigger and the difference
    (left (suc n))
    -- subcase suc m: recurse on (n,m)
     r)

gcd : ∀{i} → Nat i → ∀{j} → Nat j → Nat ∞
gcd zero m = m
gcd (suc n) zero = suc n
gcd (suc n) (suc m) = either (diff n m)
  (λ n' → gcd n' (suc m))
  (λ m' → gcd (suc n) m')

er : ∀{i} → Nat i → Nat ∞
er zero    = zero
er (suc n) = suc (er n)

diff-diag-erase : ∀{i} (n : Nat i) → diff (er n) (er n) ≡ right zero
diff-diag-erase zero    = refl
diff-diag-erase (suc n) = diff-diag-erase n

gcd-diag-erase : ∀{i} (n : Nat i) → gcd (er n) (er n) ≡ er n
gcd-diag-erase zero = refl
gcd-diag-erase (suc {i} n)
  rewrite diff-diag-erase n
          -- Before fix: diff-diag-erase {i} n.
          -- The {i} was necessary, otherwise rewrite failed
          -- because an unsolved size var prevented abstraction.
        | gcd-diag-erase n = refl

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Imports.Test where

open import Imports.Level

record Foo (ℓ : Level) : Set ℓ where

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Sigma using (Σ; _,_)

postulate
  F    : Set → Set₁
  P    : (A : Set) → F A → Set
  easy : {A : Set₁} → A

A : Set₁
A = Σ Set λ B → Σ (F B) (P B)

f : (X Y : A) → X ≡ Y
f (C , x , p) (D , y , q) = proof
  module _ where
  abstract

    proof : (C , x , p) ≡ (D , y , q)
    proof = easy

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Categories.Adjoint.Equivalence where

open import Level

open import Categories.Adjoint
open import Categories.Category
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism as ≃ using (_≃_; NaturalIsomorphism)
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

record ⊣Equivalence (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
  field
    unit   : idF ≃ (R ∘F L)
    counit : (L ∘F R) ≃ idF

  module unit = NaturalIsomorphism unit
  module counit = NaturalIsomorphism counit

  private
    module C = Category C
    module D = Category D
    module L = Functor L
    module R = Functor R
    module ℱ = Functor

  field
    zig : ∀ {A : C.Obj} → counit.⇒.η (L.F₀ A) D.∘ L.F₁ (unit.⇒.η A) D.≈ D.id

  zag : ∀ {B : D.Obj} → R.F₁ (counit.⇒.η B) C.∘ unit.⇒.η (R.F₀ B) C.≈ C.id
  zag {B} = F≃id⇒id (≃.sym unit) helper
    where open C
          open HomReasoning
          helper : R.F₁ (L.F₁ (R.F₁ (counit.⇒.η B) ∘ unit.⇒.η (R.F₀ B))) ≈ id
          helper = begin
            R.F₁ (L.F₁ (R.F₁ (counit.⇒.η B) ∘ unit.⇒.η (R.F₀ B)))               ≈⟨ ℱ.homomorphism (R ∘F L) ⟩
            R.F₁ (L.F₁ (R.F₁ (counit.⇒.η B))) ∘ R.F₁ (L.F₁ (unit.⇒.η (R.F₀ B))) ≈˘⟨ R.F-resp-≈ (F≃id-comm₁ counit) ⟩∘⟨refl ⟩
            R.F₁ (counit.⇒.η (L.F₀ (R.F₀ B))) ∘ R.F₁ (L.F₁ (unit.⇒.η (R.F₀ B))) ≈˘⟨ R.homomorphism ⟩
            R.F₁ (counit.⇒.η (L.F₀ (R.F₀ B)) D.∘ L.F₁ (unit.⇒.η (R.F₀ B)))      ≈⟨ R.F-resp-≈ zig ⟩
            R.F₁ D.id                                                           ≈⟨ R.identity ⟩
            id                                                                  ∎

  L⊣R : L ⊣ R
  L⊣R = record
    { unit   = unit.F⇒G
    ; counit = counit.F⇒G
    ; zig    = zig
    ; zag    = zag
    }

  module L⊣R = Adjoint L⊣R
  open L⊣R hiding (unit; counit; zig; zag) public

  R⊣L : R ⊣ L
  R⊣L = record
    { unit   = counit.F⇐G
    ; counit = unit.F⇐G
    ; zig    = λ {X} →
      let open C.HomReasoning
          open MR C
      in begin
        unit.⇐.η (R.F₀ X) C.∘ R.F₁ (counit.⇐.η X)
          ≈˘⟨ elimʳ zag ⟩
        (unit.⇐.η (R.F₀ X) C.∘ R.F₁ (counit.⇐.η X)) C.∘ (R.F₁ (counit.⇒.η X) C.∘ unit.⇒.η (R.F₀ X))
          ≈⟨ center ([ R ]-resp-∘ (counit.iso.isoˡ _) ○ R.identity) ⟩
        unit.⇐.η (R.F₀ X) C.∘ C.id C.∘ unit.⇒.η (R.F₀ X)
          ≈⟨ refl⟩∘⟨ C.identityˡ ⟩
        unit.⇐.η (R.F₀ X) C.∘ unit.⇒.η (R.F₀ X)
          ≈⟨ unit.iso.isoˡ _ ⟩
        C.id
          ∎
    ; zag    = λ {X} →
      let open D.HomReasoning
          open MR D
      in begin
        L.F₁ (unit.⇐.η X) D.∘ counit.⇐.η (L.F₀ X)
          ≈˘⟨ elimʳ zig ⟩
        (L.F₁ (unit.⇐.η X) D.∘ counit.⇐.η (L.F₀ X)) D.∘ counit.⇒.η (L.F₀ X) D.∘ L.F₁ (unit.⇒.η X)
          ≈⟨ center (counit.iso.isoˡ _) ⟩
        L.F₁ (unit.⇐.η X) D.∘ D.id D.∘ L.F₁ (unit.⇒.η X)
          ≈⟨ refl⟩∘⟨ D.identityˡ ⟩
        L.F₁ (unit.⇐.η X) D.∘ L.F₁ (unit.⇒.η X)
          ≈⟨ ([ L ]-resp-∘ (unit.iso.isoˡ _)) ○ L.identity ⟩
        D.id
          ∎
    }

  module R⊣L = Adjoint R⊣L

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
open import Relation.Binary.Core

module InsertSort.Everything {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import InsertSort.Impl1.Correctness.Order _≤_ tot≤
open import InsertSort.Impl1.Correctness.Permutation.Alternative _≤_ tot≤
open import InsertSort.Impl1.Correctness.Permutation.Base _≤_ tot≤

open import InsertSort.Impl2.Correctness.Order _≤_ tot≤
open import InsertSort.Impl2.Correctness.Permutation.Alternative _≤_ tot≤
open import InsertSort.Impl2.Correctness.Permutation.Base _≤_ tot≤

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
import cedille-options

module to-string (options : cedille-options.options) where

open import cedille-types
open import constants
open import syntax-util
open import ctxt
open import rename
open import general-util
open import datatype-util
open import type-util
open import free-vars
open import json

data expr-side : Set where
  left : expr-side
  right : expr-side
  neither : expr-side

is-left : expr-side → 𝔹
is-left left = tt
is-left _ = ff
is-right : expr-side → 𝔹
is-right right = tt
is-right _ = ff

exprd-eq : exprd → exprd → 𝔹
exprd-eq TERM TERM = tt
exprd-eq TYPE TYPE = tt
exprd-eq KIND KIND = tt
exprd-eq _ _ = ff

is-eq-op : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-eq-op{TERM} (VarSigma _) = tt
is-eq-op{TERM} (Rho _ _ _ _) = tt
is-eq-op{TERM} (Phi _ _ _) = tt
is-eq-op{TERM} (Delta _ _ _) = tt
is-eq-op _ = ff

pattern arrow-var = "_arrow_"
pattern TpArrow tp me tp' = TpAbs me arrow-var (Tkt tp) tp'
pattern KdArrow tk kd = KdAbs arrow-var tk kd

is-arrow : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-arrow {TYPE} (TpArrow _ _ _) = tt
is-arrow {KIND} (KdArrow _ _) = tt
is-arrow _ = ff

is-type-level-app : ∀ {ed} → ⟦ ed ⟧ → 𝔹
is-type-level-app {TYPE} (TpApp T tT) = tt
is-type-level-app _ = ff

{- need-parens e1 e2 s

   returns tt iff we need parens when e1 occurs as the given
   side s of parent expression e2. -}
need-parens : {ed : exprd} → {ed' : exprd} → ⟦ ed ⟧ → ⟦ ed' ⟧ → expr-side → 𝔹
need-parens {TYPE} {TYPE} (TpAbs _ _ _ _) (TpArrow _ _ _) left = tt
need-parens {TYPE} {TYPE} (TpIota _ _ _) (TpArrow _ _ _) left = tt
need-parens {KIND} {KIND} (KdAbs _ _ _) (KdArrow _ _) left = tt
need-parens {TYPE} {KIND} (TpAbs _ _ _ _) (KdArrow _ _) left = tt
need-parens {TYPE} {KIND} (TpIota _ _ _) (KdArrow _ _) left = tt
need-parens {TERM} {_} (Var x) p lr = ff
need-parens {TERM} {_} (Hole pi) p lr = ff
need-parens {TERM} {_} (IotaPair t₁ t₂ x Tₓ) p lr = ff
need-parens {TERM} {_} (IotaProj t n) p lr = ff
need-parens {TYPE} {_} (TpVar x) p lr = ff
need-parens {TYPE} {_} (TpEq t₁ t₂) p lr = ff
need-parens {TYPE} {_} (TpHole pi) p lr = ff
need-parens {KIND} {_} (KdHole pi) p lr = ff
need-parens {KIND} {_} KdStar p lr = ff
need-parens {_} {TERM} _ (IotaPair t₁ t₂ x Tₓ) lr = ff
need-parens {_} {TYPE} _ (TpEq t₁ t₂) lr = ff
need-parens {_} {TERM} _ (Beta ot ot') lr = ff
need-parens {_} {TERM} _ (Phi tₑ t₁ t₂) lr = is-left lr
need-parens {_} {TERM} _ (Rho _ _ _ _) right = ff
need-parens {_} {TERM} _ (Delta _ _ _) right = ff
need-parens {_} {TERM} _ (LetTm _ _ _ _ _) lr = ff
need-parens {_} {TERM} _ (LetTp _ _ _ _) lr = ff
need-parens {_} {TERM} _ (Lam _ _ _ _) lr = ff
need-parens {_} {TERM} _ (Mu _ _ _ _ _) right = ff
need-parens {_} {TYPE} _ (TpLam _ _ _) lr = ff
need-parens {_} {TYPE} _ (TpAbs _ _ _ _) lr = ff
need-parens {_} {KIND} _ (KdAbs _ _ _) neither = ff
need-parens {_} {TYPE} _ (TpIota _ _ _) lr = ff
need-parens {TERM} {_} (App t t') p lr = tt
need-parens {TERM} {_} (AppE t tT) p lr = tt
need-parens {TERM} {_} (Beta ot ot') p lr = ff
need-parens {TERM} {_} (Delta _ T t) p lr = tt
need-parens {TERM} {_} (Lam me x tk? t) p lr = tt
need-parens {TERM} {_} (LetTm me x T t t') p lr = tt
need-parens {TERM} {_} (LetTp x T t t') p lr = tt
need-parens {TERM} {_} (Phi tₑ t₁ t₂) p lr = tt
need-parens {TERM} {_} (Rho tₑ x Tₓ t) p lr = tt
need-parens {TERM} {_} (VarSigma t) p lr = ~ is-eq-op p
need-parens {TERM} {_} (Mu _ _ _ _ _) p lr = tt
need-parens {TERM} {_} (Sigma _ _ _ _ _) p lr = tt
need-parens {TYPE} {e} (TpAbs me x tk T) p lr = ~ exprd-eq e TYPE || ~ is-arrow p || is-left lr
need-parens {TYPE} {_} (TpIota x T₁ T₂) p lr = tt
need-parens {TYPE} {_} (TpApp T tT) p lr = ~ is-arrow p && (~ is-type-level-app p || is-right lr)
need-parens {TYPE} {_} (TpLam x tk T) p lr = tt
need-parens {KIND} {_} (KdAbs x tk k) p lr = ~ is-arrow p || is-left lr

pattern ced-ops-drop-spine = cedille-options.options.mk-options _ _ _ _ ff _ _ _ ff _ _
pattern ced-ops-conv-arr = cedille-options.options.mk-options _ _ _ _ _ _ _ _ ff _ _
pattern ced-ops-conv-abs = cedille-options.options.mk-options _ _ _ _ _ _ _ _ tt _ _

drop-spine : cedille-options.options → {ed : exprd} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧
drop-spine ops @ ced-ops-drop-spine = h
  where
  drop-mod-argse : (mod : args) → (actual : args) → args
  drop-mod-argse (ArgE _ :: asₘ) (ArgE _ :: asₐ) = drop-mod-argse asₘ asₐ
  drop-mod-argse (Arg _ :: asₘ) (Arg t :: asₐ) = drop-mod-argse asₘ asₐ
  drop-mod-argse (_ :: asₘ) asₐ@(Arg t :: _) = drop-mod-argse asₘ asₐ
  -- ^ Relevant term arg, so wait until we find its corresponding relevant module arg ^
  drop-mod-argse _ asₐ = asₐ

  drop-mod-args-term : ctxt → var × args → term
  drop-mod-args-term Γ (v , as) =
    let uqv = unqual-all (ctxt.qual Γ) v in
    flip recompose-apps (Var uqv) $
      maybe-else' (ifMaybe (~ v =string uqv) $ ctxt-get-qi Γ uqv)
        as λ qi → drop-mod-argse (snd qi) as

  drop-mod-args-type : ctxt → var × 𝕃 tmtp → type
  drop-mod-args-type Γ (v , as) =
    let uqv = unqual-all (ctxt.qual Γ) v in
    flip recompose-tpapps (TpVar uqv) $
      maybe-else' (ifMaybe (~ v =string uqv) $ ctxt-qualif-args-length Γ Erased uqv)
        as λ n → drop n as

  h : {ed : exprd} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧
  h {TERM} Γ t = maybe-else' (decompose-var-headed t) t (drop-mod-args-term Γ)
  h {TYPE} Γ T = maybe-else' (decompose-tpvar-headed T) T (drop-mod-args-type Γ)
  h Γ x = x
drop-spine ops Γ x = x

to-string-rewrite : {ed : exprd} → ctxt → cedille-options.options → ⟦ ed ⟧ → Σi exprd ⟦_⟧
to-string-rewrite{TYPE} Γ ced-ops-conv-arr (TpAbs me x (Tkt T) T') = , TpAbs me (if is-free-in x T' then x else arrow-var) (Tkt T) T'
to-string-rewrite{KIND} Γ ced-ops-conv-arr (KdAbs x tk k) = , KdAbs (if is-free-in x k then x else arrow-var) tk k
to-string-rewrite{TERM} Γ ops (VarSigma t) with to-string-rewrite Γ ops t
...| ,_ {TERM} (VarSigma t') = , t'
...| t? = , VarSigma t
to-string-rewrite Γ ops x = , drop-spine ops Γ x

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

open import pretty

use-newlines : 𝔹
use-newlines =
  ~ iszero (cedille-options.options.pretty-print-columns options)
  &&        cedille-options.options.pretty-print         options

doc-to-rope : DOC → rope
doc-to-rope = if use-newlines
  then pretty (cedille-options.options.pretty-print-columns options)
  else flatten-out

strM : Set
strM = {ed : exprd} → DOC → ℕ → 𝕃 tag → ctxt → maybe ⟦ ed ⟧ → expr-side → DOC × ℕ × 𝕃 tag

strEmpty : strM
strEmpty s n ts Γ pe lr = s , n , ts

to-stringh : {ed : exprd} → ⟦ ed ⟧ → strM

strM-Γ : (ctxt → strM) → strM
strM-Γ f s n ts Γ = f Γ s n ts Γ

infixr 2 _>>str_

_>>str_ : strM → strM → strM
(m >>str m') s n ts Γ pe lr with m s n ts Γ pe lr
(m >>str m') s n ts Γ pe lr | s' , n' , ts' = m' s' n' ts' Γ pe lr

strAdd : string → strM
strAdd s s' n ts Γ pe lr = s' <> TEXT [[ s ]] , n + string-length s , ts

strLine : strM
strLine s n ts Γ pe lr = s <> LINE , suc n , ts

strNest : ℕ → strM → strM
strNest i m s n ts Γ pe lr with m nil n ts Γ pe lr
...| s' , n' , ts' = s <> nest i s' , n' , ts'

strFold' : (ℕ → ℕ) → {ed : exprd} → 𝕃 (ℕ × strM) → ℕ → 𝕃 tag → ctxt → maybe ⟦ ed ⟧ → expr-side → 𝕃 (ℕ × DOC) × ℕ × 𝕃 tag
strFold' l [] n ts Γ pe lr = [] , n , ts
strFold' l ((i , x) :: []) n ts Γ pe lr with x nil n ts Γ pe lr
...| sₓ , nₓ , tsₓ = [ i , sₓ ] , nₓ , tsₓ
strFold' l ((i , x) :: xs) n ts Γ pe lr with x nil n ts Γ pe lr
...| sₓ , nₓ , tsₓ with strFold' l xs (l nₓ) tsₓ Γ pe lr
...| sₓₛ , nₓₛ , tsₓₛ = (i , sₓ) :: sₓₛ , nₓₛ , tsₓₛ

strFold : (ℕ → ℕ) → (𝕃 (ℕ × DOC) → DOC) → 𝕃 (ℕ × strM) → strM
strFold l f ms s n ts Γ pe lr with strFold' l ms n ts Γ pe lr
...| s' , n' , ts' = s <> f s' , n' , ts'

strFoldi : ℕ → (ℕ → ℕ) → (𝕃 DOC → DOC) → 𝕃 strM → strM
strFoldi i l f = strNest i ∘' strFold suc (f ∘' map snd) ∘' map (_,_ 0)

-- Either fit all args on one line, or give each their own line
strList : ℕ → 𝕃 strM → strM
strList i = strFoldi i suc λ ms → flatten (spread ms) :<|> stack ms

-- Fit as many args on each line as possible
-- (n = number of strM args)
-- (𝕃 strM so that optional args (nil) are possible)
strBreak : (n : ℕ) → fold n strM λ X → ℕ → 𝕃 strM → X
strBreak = h [] where
  h : 𝕃 (ℕ × strM) → (n : ℕ) → fold n strM λ X → ℕ → 𝕃 strM → X
  h ms (suc n) i m = h (map (_,_ i) m ++ ms) n
  h ms zero = strFold suc filln $ reverse ms

strBracket : char → strM → char → strM
strBracket l m r s n ts Γ pe lr with m nil (suc (suc n)) ts Γ pe lr
...| s' , n' , ts' = s <> bracket (char-to-string l) s' (char-to-string r) , suc (suc n') , ts'

strΓ' : defScope → var → strM → strM
strΓ' ds v m s n ts Γ =
  let gl = ds iff globalScope
      v' = if gl then (ctxt.mn Γ # v) else v in
  m s n ts
    (record Γ {
       qual = qualif-insert-params (ctxt.qual Γ) v' (unqual-local v) (if gl then ctxt.ps Γ else []);
       i = trie-insert (ctxt.i Γ) v' (var-decl , missing-location)
     })

strΓ : var → strM → strM
strΓ x m s n ts Γ = m s n ts (ctxt-var-decl x Γ)

ctxt-get-file-id : ctxt → (filename : string) → ℕ
ctxt-get-file-id = trie-lookup-else 0 ∘ ctxt.id-map

make-loc-tag : ctxt → (filename start-to end-to : string) → (start-from end-from : ℕ) → tag
make-loc-tag Γ fn s e = make-tag "loc"
  (("fn" , json-nat (ctxt-get-file-id Γ fn)) ::
   ("s" , json-raw [[ s ]]) :: ("e" , json-raw [[ e ]]) :: [])

var-loc-tag : ctxt → location → var → 𝕃 (string × 𝕃 tag)
var-loc-tag Γ ("missing" , "missing") x = []
var-loc-tag Γ ("" , _) x = []
var-loc-tag Γ (_ , "") x = []
var-loc-tag Γ (fn , pi) x =
  let fn-tag = "fn" , json-nat (ctxt-get-file-id Γ fn)
      s-tag = "s" , json-raw [[ pi ]]
      e-tag = "e" , json-raw [[ posinfo-plus-str pi x ]] in
  [ "loc" , fn-tag :: s-tag :: e-tag :: [] ]

var-tags : ctxt → var → var → 𝕃 (string × 𝕃 tag)
var-tags Γ qv uqv =
  (if qv =string qualif-var Γ uqv then id else ("shadowed" , []) ::_)
  (var-loc-tag Γ (ctxt-var-location Γ qv) uqv)

strAddTags : string → 𝕃 (string × 𝕃 tag) → strM
strAddTags sₙ tsₙ sₒ n tsₒ Γ pe lr =
  let n' = n + string-length sₙ in
  sₒ <> TEXT [[ sₙ ]] , n' , map (uncurry λ k vs → make-tag k vs n n') tsₙ ++ tsₒ

strVar : var → strM
strVar v = strM-Γ λ Γ →
  let uqv = unqual-local v -- $ unqual-all (ctxt-get-qualif Γ) v
      uqv' = if cedille-options.options.show-qualified-vars options then v else uqv in
  strAddTags uqv' (var-tags Γ (qualif-var Γ v) uqv)

strKvar : var → strM
strKvar v = strM-Γ λ Γ → strVar (unqual-all (ctxt.qual Γ) v)

-- Only necessary to unqual-local because of module parameters
strBvar : var → (class body : strM) → strM
strBvar v cm bm = strAdd (unqual-local v) >>str cm >>str strΓ' localScope v bm

strMetaVar : var → span-location → strM
strMetaVar x (fn , pi , pi') s n ts Γ pe lr =
  let n' = n + string-length x in
  s <> TEXT [[ x ]] , n' , make-loc-tag Γ fn pi pi' n n' :: ts

{-# TERMINATING #-}
term-to-stringh : term → strM
type-to-stringh : type → strM
kind-to-stringh : kind → strM
ctr-to-string : ctr → strM
case-to-string : case → strM
cases-to-string : cases → strM
caseArgs-to-string : case-args → strM → strM

params-to-string : params → strM
params-to-string' : strM → params → strM
params-to-string'' : params → strM → strM
optTerm-to-string : maybe term → char → char → 𝕃 strM
optClass-to-string : maybe tpkd → strM
optType-to-string : maybe char → maybe type → 𝕃 strM
arg-to-string : arg → strM
args-to-string : args → strM
binder-to-string : erased? → string
lam-to-string : erased? → string
arrowtype-to-string : erased? → string
vars-to-string : 𝕃 var → strM
bracketL : erased? → string
bracketR : erased? → string
braceL : erased? → string
braceR : erased? → string
opacity-to-string : opacity → string
hole-to-string : posinfo → strM

to-string-ed : {ed : exprd} → ⟦ ed ⟧ → strM
to-string-ed{TERM} = term-to-stringh
to-string-ed{TYPE} = type-to-stringh
to-string-ed{KIND} = kind-to-stringh

to-stringh' : {ed : exprd} → expr-side → ⟦ ed ⟧ → strM
to-stringh' {ed} lr t {ed'} s n ts Γ mp lr' =
  elim-Σi (to-string-rewrite Γ options t) λ t' →
  parens-if (maybe𝔹 mp (λ pe → need-parens t' pe lr)) (to-string-ed t') s n ts Γ (just t') lr
  where
  parens-if : 𝔹 → strM → strM
  parens-if p s = if p then (strAdd "(" >>str strNest 1 s >>str strAdd ")") else s

to-stringl : {ed : exprd} → ⟦ ed ⟧ → strM
to-stringr : {ed : exprd} → ⟦ ed ⟧ → strM
to-stringl = to-stringh' left
to-stringr = to-stringh' right
to-stringh = to-stringh' neither

set-parent : ∀ {ed} → ⟦ ed ⟧ → strM → strM
set-parent t m s n ts Γ _ lr = m s n ts Γ (just t) lr

apps-to-string : ∀ {ll : 𝔹} → (if ll then term else type) → strM
apps-to-string {tt} t with decompose-apps t
...| tₕ , as = set-parent t $ strList 2
                 (to-stringl tₕ :: map arg-to-string as)
apps-to-string {ff} T with decompose-tpapps T
...| Tₕ , as = set-parent T $ strList 2
                 (to-stringl Tₕ :: map arg-to-string (tmtps-to-args ff as))

lams-to-string : term → strM
lams-to-string t =
  elim-pair (decompose-lams-pretty t) λ xs b →
  set-parent t $ strFold suc filln $ foldr {B = 𝕃 (ℕ × strM)}
    (λ {(x , me , oc) r →
      (1 , (strAdd (lam-to-string me) >>str strAdd " " >>str
            strBvar x (strNest 4 (optClass-to-string oc)) (strAdd " ."))) ::
      map (map-snd $ strΓ' localScope x) r}) [ 2 , to-stringr b ] xs
  where
  decompose-lams-pretty : term → 𝕃 (var × erased? × maybe tpkd) × term
  decompose-lams-pretty = h [] where
    h : 𝕃 (var × erased? × maybe tpkd) → term → 𝕃 (var × erased? × maybe tpkd) × term
    h acc (Lam me x oc t) = h ((x , me , oc) :: acc) t
    h acc t = reverse acc , t

term-to-stringh (App t t') = apps-to-string (App t t')

term-to-stringh (AppE t tT) = apps-to-string (AppE t tT)

term-to-stringh (Beta t t') = strBreak 3
  0 [ strAdd "β" ]
  2 [ strAdd "<" >>str to-stringh (erase t ) >>str strAdd ">" ]
  2 [ strAdd "{" >>str to-stringh (erase t') >>str strAdd "}" ]

term-to-stringh (Delta _ T t) = strBreak 3
  0 [ strAdd "δ" ]
  2 [ to-stringl T >>str strAdd " -" ]
  1 [ to-stringr t ]

term-to-stringh (Hole pi) = hole-to-string pi

term-to-stringh (IotaPair t₁ t₂ x Tₓ) = strBreak 3
  1 [ strAdd "[ " >>str to-stringh t₁ >>str strAdd "," ]
  1 [ to-stringh t₂ ]
  1 [ strAdd "@ " >>str
      strBvar x (strAdd " . ") (strNest (5 + string-length x) (to-stringh Tₓ)) >>str
      strAdd " ]" ]

term-to-stringh (IotaProj t n) = to-stringh t >>str strAdd (if n iff ι1 then ".1" else ".2")

term-to-stringh (Lam me x oc t) =  lams-to-string (Lam me x oc t)

term-to-stringh (LetTm me x T t t') = strBreak 4
  1 [ strAdd (bracketL me) >>str strAdd (unqual-local x) ]
  5 ( optType-to-string (just ':') T )
  3 [ strAdd "= " >>str to-stringh t >>str strAdd (bracketR me) ]
  1 [ strΓ' localScope x (to-stringr t') ]

term-to-stringh (LetTp x k T t) = strBreak 4
  1 [ strAdd (bracketL NotErased) >>str strAdd (unqual-local x) ]
  5 [ strAdd ": " >>str to-stringh k ]
  3 [ strAdd "= " >>str to-stringh T >>str strAdd (bracketR NotErased) ]
  1 [ strΓ' localScope x (to-stringr t) ]

term-to-stringh (Phi tₑ t₁ t₂) = strBreak 3
  0 [ strAdd "φ " >>str to-stringl tₑ >>str strAdd " -" ]
  2 [ to-stringh t₁ ]
  2 [ strAdd "{ " >>str to-stringr (erase t₂) >>str strAdd " }" ]

term-to-stringh (Rho tₑ x Tₓ t) = strBreak 3
  0 [ strAdd "ρ " >>str to-stringl tₑ ]
  1 [ strAdd "@ " >>str strBvar x (strAdd " . ") (to-stringh (erase Tₓ)) ]
  1 [ strAdd "- " >>str strNest 2 (to-stringr t) ]

term-to-stringh (VarSigma t) = strAdd "ς " >>str to-stringh t

term-to-stringh (Var x) = strVar x

term-to-stringh (Mu x t ot t~ cs) =
  strAdd "μ " >>str
  strBvar x
    (strAdd " . " >>str strBreak 2
      2 [ to-stringl t ]
      3 ( optType-to-string (just '@') ot ))
    (strAdd " " >>str strBracket '{' (cases-to-string cs) '}')

term-to-stringh (Sigma ot t oT t~ cs) =
  strAdd "σ " >>str strBreak 3
    2 (maybe-else' {B = 𝕃 strM} ot []
         λ t → [ strAdd "<" >>str to-stringh t >>str strAdd ">" ])
    2 [ to-stringl t ]
    3 ( optType-to-string (just '@') oT ) >>str
  strAdd " " >>str strBracket '{' (cases-to-string cs) '}'

type-to-stringh (TpArrow T a T') = strBreak 2
  2 [ to-stringl T >>str strAdd (arrowtype-to-string a) ]
  2 [ to-stringr T' ]

type-to-stringh (TpAbs me x tk T) = strBreak 2
  3 [ strAdd (binder-to-string me ^ " ") >>str
      strBvar x (strAdd " : " >>str to-stringl -tk' tk >>str strAdd " .") strEmpty ]
  1 [ strΓ' localScope x (to-stringh T) ]

type-to-stringh (TpIota x T₁ T₂) = strBreak 2
  2 [ strAdd "ι " >>str
      strBvar x (strAdd " : " >>str to-stringh T₁ >>str strAdd " .") strEmpty ]
  2 [ strΓ' localScope x (to-stringh T₂) ]

type-to-stringh (TpApp T tT) = apps-to-string (TpApp T tT)

type-to-stringh (TpEq t₁ t₂) = strBreak 2
  2 [ strAdd "{ " >>str to-stringh (erase t₁) ]
  2 [ strAdd "≃ " >>str to-stringh (erase t₂) >>str strAdd " }" ]

type-to-stringh (TpHole pi) = hole-to-string pi

type-to-stringh (TpLam x tk T) = strBreak 2
  3 [ strAdd "λ " >>str
      strBvar x (strAdd " : " >>str to-stringh -tk' tk >>str strAdd " .") strEmpty ]
  1 [ strΓ' localScope x (to-stringr T) ]

type-to-stringh (TpVar x) = strVar x

kind-to-stringh (KdArrow k k') = strBreak 2
  2 [ to-stringl -tk' k >>str strAdd " ➔" ]
  2 [ to-stringr k' ]

kind-to-stringh (KdAbs x tk k) = strBreak 2
  4 [ strAdd "Π " >>str
      strBvar x (strAdd " : " >>str to-stringl -tk' tk >>str strAdd " .") strEmpty ]
  1 [ strΓ' localScope x (to-stringh k) ]

kind-to-stringh (KdHole pi) = hole-to-string pi

kind-to-stringh KdStar = strAdd "★"

hole-to-string pi = strM-Γ λ Γ → strAddTags "●" (var-loc-tag Γ (split-var pi) "●")

optTerm-to-string nothing c1 c2 = []
optTerm-to-string (just t) c1 c2 =
  [ strAdd (𝕃char-to-string (c1 :: [ ' ' ])) >>str
    to-stringh t >>str
    strAdd (𝕃char-to-string (' ' :: [ c2 ])) ]

optClass-to-string nothing = strEmpty
optClass-to-string (just atk) = strAdd " : " >>str to-stringh -tk' atk

optType-to-string pfx nothing = []
optType-to-string pfx (just T) =
  [ maybe-else strEmpty (λ pfx → strAdd (𝕃char-to-string (pfx :: [ ' ' ]))) pfx >>str to-stringh T ]

arg-to-string (Arg t) = to-stringr t
arg-to-string (ArgE (Ttm t)) = strAdd "-" >>str strNest 1 (to-stringr t)
arg-to-string (ArgE (Ttp T)) = strAdd "·" >>str strNest 2 (to-stringr T)

args-to-string = set-parent (App (Hole pi-gen) (Hole pi-gen)) ∘ foldr' strEmpty λ t x → strAdd " " >>str arg-to-string t >>str x

binder-to-string tt = "∀"
binder-to-string ff = "Π"

lam-to-string tt = "Λ"
lam-to-string ff = "λ"

arrowtype-to-string ff = " ➔"
arrowtype-to-string tt = " ➾"

opacity-to-string opacity-open = ""
opacity-to-string opacity-closed = "opaque "

vars-to-string [] = strEmpty
vars-to-string (v :: []) = strVar v
vars-to-string (v :: vs) = strVar v >>str strAdd " " >>str vars-to-string vs

ctr-to-string (Ctr x T) = strAdd x >>str strAdd " : " >>str to-stringh T

case-to-string (Case x as t _) =
  strM-Γ λ Γ →
  let as-f = λ x as → strVar x >>str caseArgs-to-string as (strAdd " ➔ " >>str to-stringr t) in
  case (env-lookup Γ x , options) of uncurry λ where
    (just (ctr-def mps T _ _ _ , _ , _)) ced-ops-drop-spine →
          as-f (unqual-all (ctxt.qual Γ) x) as
    _ _ → as-f x as

cases-to-string = h use-newlines where
  h : 𝔹 → cases → strM
  h _ [] = strEmpty
  h tt (m :: []) = strAdd "| " >>str case-to-string m
  h tt (m :: ms) = strAdd "| " >>str case-to-string m >>str strLine >>str h tt ms
  h ff (m :: []) = case-to-string m
  h ff (m :: ms) = case-to-string m >>str strAdd " | " >>str h ff ms

caseArgs-to-string [] m = m
caseArgs-to-string (CaseArg _ x (just (Tkk _)) :: as) m = strAdd " ·" >>str strBvar x strEmpty (caseArgs-to-string as m)
caseArgs-to-string (CaseArg ff x _ :: as) m = strAdd " " >>str strBvar x strEmpty (caseArgs-to-string as m)
caseArgs-to-string (CaseArg tt x _ :: as) m = strAdd " -" >>str strBvar x strEmpty (caseArgs-to-string as m)

braceL me = if me then "{" else "("
braceR me = if me then "}" else ")"

bracketL me = if me then "{ " else "[ "
bracketR me = if me then " } -" else " ] -"

param-to-string : param → (strM → strM) × strM
param-to-string (Param me v atk) =
  strΓ' localScope v ,
  (strAdd (braceL me) >>str
   strAdd (unqual-local v) >>str
   strAdd " : " >>str
   to-stringh -tk' atk >>str
   strAdd (braceR me))

params-to-string'' ps f = elim-pair (foldr (λ p → uncurry λ g ms → elim-pair (param-to-string p) λ h m → g ∘ h , m :: map h ms) (id , []) ps) λ g ms → strList 2 (strEmpty :: ms) >>str g f

params-to-string' f [] = f
params-to-string' f (p :: []) = elim-pair (param-to-string p) λ g m → m >>str g f
params-to-string' f (p :: ps) = elim-pair (param-to-string p) λ g m → m >>str strAdd " " >>str params-to-string' (g f) ps

params-to-string = params-to-string' strEmpty

strRun : ctxt → strM → rope
strRun Γ m = doc-to-rope $ fst $ m {TERM} NIL 0 [] Γ nothing neither

strRunTag : (name : string) → ctxt → strM → tagged-val
strRunTag name Γ m with m {TERM} NIL 0 [] Γ nothing neither
...| s , n , ts = name , doc-to-rope s , ts

to-stringe : {ed : exprd} → ⟦ ed ⟧ → strM
to-stringe = to-stringh ∘' (if cedille-options.options.erase-types options then erase else id)

to-string-tag : {ed : exprd} → string → ctxt → ⟦ ed ⟧ → tagged-val
to-string-tag name Γ t = strRunTag name Γ (to-stringe t)

to-string : {ed : exprd} → ctxt → ⟦ ed ⟧ → rope
to-string Γ t = strRun Γ (to-stringh t)

tpkd-to-stringe : tpkd → strM
tpkd-to-stringe = to-stringe -tk'_

tpkd-to-string : ctxt → tpkd → rope
tpkd-to-string Γ atk = strRun Γ (tpkd-to-stringe atk)

params-to-string-tag : string → ctxt → params → tagged-val
params-to-string-tag name Γ ps = strRunTag name Γ (params-to-string ps)


text:
data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero  + n = n
suc m + n = suc ?


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

open import lib.Basics

open import lib.types.Sigma
open import lib.types.Bool
open import lib.types.Truncation hiding (Trunc)

open import Pointed
open import Preliminaries hiding (_^_)

module Judgmental_Computation where

-- Chapter 6: On the Truncation's Judgmental
--            Computation Rule

{-
Recall the definition of the propositional
truncation that we use (Prelims.agda):

postulate
    ∣∣_∣∣ : ∀ {i} → (X : Type i) → Type i
    tr-is-prop : ∀ {i} {X : Type i} → is-prop (∣∣ X ∣∣)
    ∣_∣ : ∀ {i} {X : Type i} → X → ∣∣ X ∣∣
    tr-rec : ∀ {i j} {X : Type i} {P : Type j}
             → (is-prop P) → (X → P) →   ∣∣ X ∣∣ → P

We now redefine the propositional truncation so
that rec has the judgmental β rule. We use the
library implementation (library.types.Truncation).
However, we still only talk about the *propositional*
truncation (not the more general n-truncation).

This file is independent of (almost) all the other
files of the formalisation.
-}

-- The propositional truncation operator:
Trunc : ∀ {i} → Type i → Type i
Trunc = lib.types.Truncation.Trunc ⟨-1⟩

-- By definition, the truncation is propositional:
h-tr : ∀ {i} → (X : Type i) → is-prop (Trunc X)
h-tr X = Trunc-level

-- The projection.
∣_∣ : ∀ {i} → {X : Type i} → X → Trunc X
∣_∣ = [_]

-- The recursion principle, with judgmental computation.
rec : ∀ {i j} → {X : Type i} → {P : Type j}
      → (is-prop P) → (X → P) → Trunc X → P
rec = Trunc-rec

-- Similarly the induction principle.
ind : ∀ {i j} → {X : Type i} → {P : Trunc X → Type j}
      → ((z : Trunc X) → is-prop (P z))
      → ((x : X) → P ∣ x ∣) → (z : Trunc X) → P z
ind = Trunc-elim

-- Chapter 6.1: The Interval

-- Proposition 6.1.1
interval : Type₀
interval = Trunc Bool

i₁ : interval
i₁ = ∣ true ∣

i₂ : interval
i₂ = ∣ false ∣

seg : i₁ == i₂
seg = prop-has-all-paths (h-tr _) _ _

-- We prove that the interval has the "correct" recursion principle:
module interval {i} {Y : Type i} (y₁ y₂ : Y) (p : y₁ == y₂) where

  g : Bool → Σ Y λ y → y₁ == y
  g true = (y₁ , idp)
  g false = (y₂ , p)

  ĝ : interval → Σ Y λ y → y₁ == y
  ĝ = rec (contr-is-prop (pathfrom-is-contr _)) g

  f : interval → Y
  f = fst ∘ ĝ

  f-i₁ : f i₁ == y₁
  f-i₁ = idp

  f-i₂ : f i₂ == y₂
  f-i₂ = idp

  f-seg : ap f seg == p
  f-seg =
    ap f seg                  =⟨ idp ⟩
    ap (fst ∘ ĝ) seg          =⟨ ! (∘-ap _ _ _) ⟩
    (ap fst) (ap ĝ seg)       =⟨ ap (ap fst) (prop-has-all-paths (contr-is-set (pathfrom-is-contr _) _ _) _ _) ⟩
    (ap fst) (pair= p po-aux) =⟨ fst=-β p _ ⟩
    p                         ∎ where
      po-aux : idp == p [ _==_ y₁ ↓ p ]
      po-aux = from-transp (_==_ y₁) p (trans-pathfrom p idp)

-- Everything again outside the module:

interval-rec : ∀ {i} → {Y : Type i} → (y₁ y₂ : Y) → (p : y₁ == y₂) → (interval → Y)
interval-rec  = interval.f

interval-rec-i₁ : ∀ {i} → {Y : Type i} → (y₁ y₂ : Y) → (p : y₁ == y₂) → (interval-rec y₁ y₂ p) i₁ == y₁
interval-rec-i₁ = interval.f-i₁  -- or: λ _ _ _ → idp

interval-rec-i₂ : ∀ {i} →  {Y : Type i} → (y₁ y₂ : Y) → (p : y₁ == y₂) → (interval-rec y₁ y₂ p) i₂ == y₂
interval-rec-i₂ = interval.f-i₂  -- or: λ _ _ _ → idp

interval-rec-seg : ∀ {i} → {Y : Type i} → (y₁ y₂ : Y) → (p : y₁ == y₂) → ap (interval-rec y₁ y₂ p) seg == p
interval-rec-seg = interval.f-seg

-- Chapter 6.2: Function Extensionality

-- Lemma 6.2.1 (Shulman) / Corollary 6.2.2
interval→funext : ∀ {i j} → {X : Type i} → {Y : Type j} → (f g : (X → Y)) → ((x : X) → f x == g x) → f == g
interval→funext {X = X} {Y = Y} f g hom = ap i-x seg where

  x-i : X → interval → Y
  x-i x = interval-rec (f x) (g x) (hom x)

  i-x : interval → X → Y
  i-x i x = x-i x i

-- Thus, function extensionality holds automatically;
-- i.e. we could derive all lemmata in lib.types.Pi,
-- which we choose to import for convenience.
open import lib.types.Pi

-- Chapter 6.3: Judgmental Factorisation

-- We use the definitions from Chapter 5, but we
-- re-define them as our definition of "Trunc" has
-- chanced
factorizes : ∀ {i j} → {X : Type i} → {Y : Type j}
             → (f : X → Y) → Type (lmax i j)
factorizes {X = X} {Y = Y} f =
   Σ (Trunc X → Y)
     λ f' → (x : X) → f' ∣ x ∣ == f x

-- Proposition 6.3.1 - note the line   proof' = λ _ → idp
judgmental-factorizer : ∀ {i j} → {X : Type i} → {Y : Type j}
  → (f : X → Y) → factorizes f → factorizes f
judgmental-factorizer {X = X} {Y = Y} f (f₂ , proof) = f' , proof' where

  g : X → (z : Trunc X) → Σ Y λ y → y == f₂ z
  g x = λ z → f x , (f x       =⟨ ! (proof _) ⟩
                     f₂ ∣ x ∣  =⟨ ap f₂ (prop-has-all-paths (h-tr _) _ _) ⟩
                     f₂ z      ∎)

  g-codom-prop : is-prop ((z : Trunc X) → Σ Y λ y → y == f₂ z)
  g-codom-prop = contr-is-prop (Π-level (λ z → pathto-is-contr _))

  ĝ : Trunc X → (z : Trunc X) → Σ Y λ y → y == f₂ z
  ĝ = rec g-codom-prop g

  f' : Trunc X → Y
  f' = λ z → fst (ĝ z z)

  proof' : (x : X) → f' ∣ x ∣ == f x
  proof' = λ _ → idp

-- Proposition 6.3.2 - we need the induction principle, but with that,
-- it is actually simpler than the previous construction.
-- Still, it is nearly a replication.
factorizes-dep : ∀ {i j} → {X : Type i} → {Y : Trunc X → Type j}
  → (f : (x : X) → (Y ∣ x ∣)) → Type (lmax i j)
factorizes-dep {X = X} {Y = Y} f =
  Σ ((z : Trunc X) → Y z) λ f₂ → ((x : X) → f x == f₂ ∣ x ∣)

judgmental-factorizer-dep : ∀ {i j} → {X : Type i} → {Y : Trunc X → Type j}
  → (f : (x : X) → Y ∣ x ∣) → factorizes-dep {X = X} {Y = Y} f
  → factorizes-dep {X = X} {Y = Y} f
judgmental-factorizer-dep {X = X} {Y = Y} f (f₂ , proof) = f' , proof' where

  g : (x : X) → Σ (Y ∣ x ∣) λ y → y == f₂ ∣ x ∣
  g x = f x , proof x

  g-codom-prop : (z : Trunc X) → is-prop (Σ (Y z) λ y → y == f₂ z)
  g-codom-prop z = contr-is-prop (pathto-is-contr _)

  ĝ : (z : Trunc X) →  Σ (Y z) λ y → y == f₂ z
  ĝ = ind g-codom-prop g

  f' : (z : Trunc X) → Y z
  f' = fst ∘ ĝ

  proof' : (x : X) → f' ∣ x ∣ == f x
  proof' x = idp

-- Chapter 6.4: An Invertibility Paradox

{- The content of this section is partially taken from my
   formalisation of the contents of my original blog post;
   see

         http://homotopytypetheory.org/2013/10/28/

   for a discussion and

         http://red.cs.nott.ac.uk/~ngk/html-trunc-inverse/trunc-inverse.html

   for a formalisation (the slightly simpler formalization that is mentioned
   in the thesis ['Finally, we want to remark that te construction of myst
   doest not need the full strength of Proposition 6.3.1']).
-}

-- Definition 6.4.1
is-transitive : ∀ {i} → Type i → Type (lsucc i)
is-transitive {i} X = (x₁ x₂ : X) → _==_ {A = Type• i} (X , x₁) (X , x₂)

-- Example 6.4.2
module dec-trans {i} (X : Type i) (dec : has-dec-eq X) where

  module _ (x₁ x₂ : X) where

    -- I define a function X → X that switches x and x₀.
    switch : X → X
    switch = λ y → match dec y x₁
                     withl (λ _ → x₂)
                     withr (λ _ → match dec y x₂
                                    withl (λ _ → x₁)
                                    withr (λ _ → y))

    -- Rather tedious to prove, but completely straightforward:
    -- this map is its own inverse.
    switch-selfinverse : (y : X) → switch (switch y) == y
    switch-selfinverse y with dec y x₁
    switch-selfinverse y | inl _ with dec x₂ x₁
    switch-selfinverse y | inl y-x₁  | inl x-x₁ = x-x₁ ∙ ! y-x₁
    switch-selfinverse y | inl _     | inr _ with dec x₂ x₂
    switch-selfinverse y | inl y-x₁  | inr _     | inl _ = ! y-x₁
    switch-selfinverse y | inl _     | inr _     | inr ¬x₂-x₂ = Empty-elim {P = λ _ → x₂ == y} (¬x₂-x₂ idp)
    switch-selfinverse y | inr _ with dec y x₂
    switch-selfinverse y | inr _     | inl _ with dec x₂ x₁
    switch-selfinverse y | inr ¬x₂-x₁ | inl y-x₂  | inl x₂-x₁ = Empty-elim (¬x₂-x₁ (y-x₂ ∙ x₂-x₁))
    switch-selfinverse y | inr _     | inl _     | inr _ with dec x₁ x₁
    switch-selfinverse y | inr _     | inl y-x₂  | inr _ | inl _ = ! y-x₂
    switch-selfinverse y | inr _     | inl _     | inr _ | inr ¬x₁-x₁ = Empty-elim {P = λ _ → _ == y} (¬x₁-x₁ idp)
    switch-selfinverse y | inr _     | inr _ with dec y x₁
    switch-selfinverse y | inr ¬y-x₁ | inr _     | inl y-x₁ = Empty-elim {P = λ _ → x₂ == y} (¬y-x₁ y-x₁)
    switch-selfinverse y | inr _     | inr _     | inr _  with dec y x₂
    switch-selfinverse y | inr _     | inr ¬y-x₂ | inr _ | inl y-x₂ = Empty-elim {P = λ _ → x₁ == y} (¬y-x₂ y-x₂)
    switch-selfinverse y | inr _     | inr _     | inr _ | inr _ = idp

    switch-maps : switch x₂ == x₁
    switch-maps with dec x₂ x₁
    switch-maps | inl x₂-x₁ = x₂-x₁
    switch-maps | inr _ with dec x₂ x₂
    switch-maps | inr _ | inl _ = idp
    switch-maps | inr _ | inr ¬x-x = Empty-elim {P = λ _ → x₂ == x₁} (¬x-x idp)

    -- switch is an equivalence
    switch-eq : X ≃ X
    switch-eq = equiv switch switch
                      switch-selfinverse switch-selfinverse

  -- X is transitive:
  is-trans : is-transitive X
  is-trans x₁ x₂  = pair= (ua X-X) x₁-x₂ where
    X-X : X ≃ X
    X-X = switch-eq x₂ x₁
    x₁-x₂ : PathOver (idf (Type i)) (ua X-X) x₁ x₂
    x₁-x₂ = ↓-idf-ua-in X-X (switch-maps x₂ x₁)

-- Example 6.4.2 addendum: ℕ is transitive.
-- (Recall that we have defined _+_ ourselves,
-- so that it is defined by recursion on the
-- second argument - this is not important
-- here, but it is the reason why we hide _+_.)
open import lib.types.Nat hiding (_+_)

ℕ-trans : is-transitive ℕ
ℕ-trans = dec-trans.is-trans ℕ ℕ-has-dec-eq

-- Example 6.4.3
-- (Note that this does not need the univalence axiom)

-- Preparation
path-trans-aux : ∀ {i} → (X : Type i) → (x₁ x₂ x₃ : X) → (x₂ == x₃)
  → (p₁₂ : x₁ == x₂) → (p₁₃ : x₁ == x₃) →
  _==_ {A = Type• i} ((x₁ == x₂) , p₁₂) ((x₁ == x₃) , p₁₃)
path-trans-aux X x₁ .x₁ .x₁ p idp idp = idp

-- The proposition of Example 6.4.3
path-trans : ∀ {i} → (X : Type i) → (x₁ x₂ : X)
  → is-transitive (x₁ == x₂)
path-trans X x₁ x₂ = path-trans-aux X x₁ x₂ x₂ idp

-- In particular, loop spaces are transitive.
-- To show this, we choose postcomposition here -
-- whether the function exponentiation operator is more
-- convenient to use with pre- or postcomposition depends
-- on the concrete case.
infix 10 _^_
_^_ : ∀ {i} {A : Set i} → (A → A) → ℕ → A → A
f ^ 0   = idf _
f ^ S n = f ∘ (f ^ n)

loop-trans : ∀ {i} → (X : Type• i) → (n : ℕ)
  → is-transitive (fst ((Ω ^ (S n)) X))
loop-trans {i} X n = path-trans type point point where

  type : Type i
  type = fst ((Ω ^ n) X)

  point : type
  point = snd ((Ω ^ n) X)

-- We omit the formalisation for Examples 6.4.4, 6.4.5,
-- as they would require us to define
-- (or import) groups / are not essential

-- Finally: Theorem 6.4.6, the myst paradoxon
-- We need some preparations.
module constr-myst {i} (X : Type i) (x₀ : X) (t : is-transitive X) where

  f : X → Type• i
  f x = (X , x)

  f'' : Trunc X → Type• i
  f'' _ = (X , x₀)

  f-fact : factorizes f
  f-fact = f'' , (λ x → t x₀ x)

  f' : Trunc X → Type• i
  f' = fst (judgmental-factorizer f f-fact)

-- the myst function:
  myst : (z : Trunc X) → fst (f' z)
  myst = snd ∘ f'

  check : (x : X) → myst ∣ x ∣ == x
  check x = idp

  myst-∣_∣-is-id : myst ∘ ∣_∣ == idf X
  myst-∣_∣-is-id = λ= λ x → idp

-- Let us do Myst explicitly for ℕ:
open import lib.types.Nat

myst-ℕ = constr-myst.myst ℕ 0 (dec-trans.is-trans ℕ ℕ-has-dec-eq)

myst-∣_∣-is-id : (n : ℕ) → myst-ℕ ∣ n ∣ == n
myst-∣_∣-is-id n = idp

test : myst-ℕ ∣ 17 ∣ == 17
test = idp

max_stars_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Relation.Binary.Equality where

open import Light.Library.Relation.Binary using (Binary ; SelfBinary)
open import Light.Library.Relation using (Base)
open import Light.Variable.Levels
open import Light.Level using (Setω)
open import Light.Variable.Sets

-- Binary relation wrapper for equality. (Purely conventional.)
-- (To facilitate instance lookup.)

record Equality ⦃ base : Base ⦄ (𝕒 : Set aℓ) (𝕓 : Set bℓ) : Setω where
      constructor wrap
      field relation : Binary 𝕒 𝕓
      open Binary relation using () renaming (are to _≈_) public

SelfEquality : ∀ ⦃ base : Base ⦄ → Set aℓ → Setω
SelfEquality 𝕒 = Equality 𝕒 𝕒

open Equality ⦃ ... ⦄ using (_≈_) public
private module Eq = Equality ⦃ ... ⦄

relation : ∀ (𝕒 : Set aℓ) (𝕓 : Set bℓ) ⦃ base : Base ⦄ ⦃ equals : Equality 𝕒 𝕓 ⦄ → Binary 𝕒 𝕓
relation _ _ = Eq.relation

self‐relation : ∀ (𝕒 : Set aℓ) ⦃ base : Base ⦄ ⦃ equals : SelfEquality 𝕒 ⦄ → SelfBinary 𝕒
self‐relation _ = Eq.relation

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module Oscar.Category.Semifunctor where

open import Oscar.Category.Setoid
open import Oscar.Category.Semigroupoid
open import Oscar.Level

module _
  {𝔬₁ 𝔪₁ 𝔮₁} (semigroupoid₁ : Semigroupoid 𝔬₁ 𝔪₁ 𝔮₁)
  {𝔬₂ 𝔪₂ 𝔮₂} (semigroupoid₂ : Semigroupoid 𝔬₂ 𝔪₂ 𝔮₂)
  where

  private module 𝔊₁ = Semigroupoid semigroupoid₁
  private module 𝔊₂ = Semigroupoid semigroupoid₂

--   record IsSemifunctor
--     (μ : 𝔊₁.⋆ → 𝔊₂.⋆)
--     (𝔣 : ∀ {x y} → x 𝔊₁.↦ y → μ x 𝔊₂.↦ μ y)
--     : Set (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂) where
--     field
--       extensionality : ∀ {x y} {f₁ f₂ : x 𝔊₁.↦ y} → f₁ ≋ f₂ → 𝔣 f₁ ≋ 𝔣 f₂
--       distributivity : ∀ {x y} (f : x 𝔊₁.↦ y) {z} (g : y 𝔊₁.↦ z) → 𝔣 (g 𝔊₁.∙ f) ≋ 𝔣 g 𝔊₂.∙ 𝔣 f

-- open IsSemifunctor ⦃ … ⦄ public

-- record Semifunctor 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂ : Set (lsuc (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂)) where
--   field
--     semigroupoid₁ : Semigroupoid 𝔬₁ 𝔪₁ 𝔮₁
--     semigroupoid₂ : Semigroupoid 𝔬₂ 𝔪₂ 𝔮₂

--   module 𝔊₁ = Semigroupoid semigroupoid₁
--   module 𝔊₂ = Semigroupoid semigroupoid₂

--   field
--     μ : 𝔊₁.⋆ → 𝔊₂.⋆
--     𝔣 : ∀ {x y} → x 𝔊₁.↦ y → μ x 𝔊₂.↦ μ y
--     ⦃ isSemifunctor ⦄ : IsSemifunctor semigroupoid₁ semigroupoid₂ μ 𝔣

-- record Semigroupoids 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂ : Set (lsuc (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂)) where
--   constructor _,_
--   field
--     semigroupoid₁ : Semigroupoid 𝔬₁ 𝔪₁ 𝔮₁
--     semigroupoid₂ : Semigroupoid 𝔬₂ 𝔪₂ 𝔮₂

--   module 𝔊₁ = Semigroupoid semigroupoid₁
--   module 𝔊₂ = Semigroupoid semigroupoid₂

-- module _
--   {𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂} (semigroupoids : Semigroupoids 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂)
--   where
--   open Semigroupoids semigroupoids
--   record IsSemifunctor
--     {μ : 𝔊₁.⋆ → 𝔊₂.⋆}
--     (𝔣 : ∀ {x y} → x 𝔊₁.↦ y → μ x 𝔊₂.↦ μ y)
--     : Set (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂) where
--     instance _ = 𝔊₁.IsSetoid↦
--     instance _ = 𝔊₂.IsSetoid↦
--     field
--       extensionality : ∀ {x y} {f₁ f₂ : x 𝔊₁.↦ y} → f₁ ≋ f₂ → 𝔣 f₁ ≋ 𝔣 f₂
--       distributivity : ∀ {x y} (f : x 𝔊₁.↦ y) {z} (g : y 𝔊₁.↦ z) → 𝔣 (g 𝔊₁.∙ f) ≋ 𝔣 g 𝔊₂.∙ 𝔣 f

-- open IsSemifunctor ⦃ … ⦄ public

-- record Semifunctor 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂ : Set (lsuc (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂)) where
--   constructor _,_
--   field
--     semigroupoids : Semigroupoids 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂

--   open Semigroupoids semigroupoids public

--   field
--     {μ} : 𝔊₁.⋆ → 𝔊₂.⋆
--     𝔣 : ∀ {x y} → x 𝔊₁.↦ y → μ x 𝔊₂.↦ μ y
--     ⦃ isSemifunctor ⦄ : IsSemifunctor semigroupoids 𝔣
--   open IsSemifunctor isSemifunctor public


text:
module Issue561 where

open import Agda.Builtin.Bool
open import Issue561.Core

primitive
  primIsDigit : Char → Bool

main : IO Bool
main = return true


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

open import HoTT

module Extensions where

  ExtensionOf : ∀ {ℓ} {A B : Type ℓ} (f : A → B) (P : B → Type ℓ) (φ : (a : A) → P (f a)) → Type ℓ
  ExtensionOf {A = A} {B = B} f P φ = Σ (Π B P) (λ ψ → (a : A) → ψ (f a) == φ a)

  syntax ExtensionOf f P φ = ⟨ P ⟩⟨ φ ↗ f ⟩

  path-extension : ∀ {ℓ} {A B : Type ℓ} {f : A → B}
                   {P : B → Type ℓ} {φ : (a : A) → P (f a)}
                   (e₀ e₁ : ⟨ P ⟩⟨ φ ↗ f ⟩) →
                   ⟨ (λ b → fst e₀ b == fst e₁ b) ⟩⟨ (λ a → snd e₀ a ∙ ! (snd e₁ a)) ↗ f ⟩ ≃ (e₀ == e₁)
  path-extension {f = f} (ψ₀ , ε₀) (ψ₁ , ε₁) = equiv to {!!} {!!} {!!}

    where to : ExtensionOf f (λ b → ψ₀ b == ψ₁ b) (λ a → ε₀ a ∙ ! (ε₁ a)) → (ψ₀ , ε₀) == (ψ₁ , ε₁)
          to (α , β) = pair= (λ= α) {!!}

          from : (ψ₀ , ε₀) == (ψ₁ , ε₁) → ExtensionOf f (λ b → ψ₀ b == ψ₁ b) (λ a → ε₀ a ∙ ! (ε₁ a))
          from p = {!!}

    --       from : (e₀ == e₁) → ⟨ (λ b → fst e₀ b == fst e₁ b) ⟩⟨ (λ a → snd e₀ a ∙ ! (snd e₁ a)) ↗ f ⟩
    --       from = {!!}

  -- Definition equiv_path_extension `{Funext} {A B : Type} {f : A -> B}
  --            {P : B -> Type} {d : forall x:A, P (f x)}
  --            (ext ext' : ExtensionAlong f P d)
  -- : (ExtensionAlong f
  --                   (fun y => pr1 ext y = pr1 ext' y)
  --                   (fun x => pr2 ext x @ (pr2 ext' x)^))
  --   <~> ext = ext'.

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import IO using ( run ; putStrLn )
open import Web.URI using ( AURI ; toString ; http://_ ; _/_ )

module Web.URI.Examples.HelloWorld where

hw : AURI
hw = http://"example.com"/"hello"/"world"

main = run (putStrLn (toString hw))

max_stars_repo_name: agda/agda-web-uri

max_issues_repo_name: agda/agda-web-uri

max_forks_repo_name: agda/agda-web-uri