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

open import LogicalFormulae
open import Groups.Definition
open import Setoids.Setoids
open import Rings.Definition
open import Sets.EquivalenceRelations
open import Rings.Ideals.Definition
open import Rings.IntegralDomains.Definition
open import Rings.Ideals.Prime.Definition
open import Rings.Cosets

module Rings.Ideals.Prime.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) where

open Ring R
open Group additiveGroup
open Setoid S
open Equivalence eq
open import Rings.Ideals.Lemmas R

idealPrimeImpliesQuotientIntDom : PrimeIdeal i → IntegralDomain (cosetRing R i)
IntegralDomain.intDom (idealPrimeImpliesQuotientIntDom isPrime) {a} {b} ab=0 a!=0 = ans
  where
    ab=0' : pred (a * b)
    ab=0' = translate' i ab=0
    a!=0' : (pred a) → False
    a!=0' prA = a!=0 (translate i prA)
    ans' : pred b
    ans' = PrimeIdeal.isPrime isPrime ab=0' a!=0'
    ans : pred (inverse (Ring.0R (cosetRing R i)) + b)
    ans = translate i ans'
IntegralDomain.nontrivial (idealPrimeImpliesQuotientIntDom isPrime) 1=0 = PrimeIdeal.notContainedIsNotContained isPrime u
  where
    t : pred (Ring.1R (cosetRing R i))
    t = translate' i 1=0
    u : pred (PrimeIdeal.notContained isPrime)
    u = Ideal.isSubset i identIsIdent (Ideal.accumulatesTimes i {y = PrimeIdeal.notContained isPrime} t)

quotientIntDomImpliesIdealPrime : IntegralDomain (cosetRing R i) → PrimeIdeal i
quotientIntDomImpliesIdealPrime intDom = record { isPrime = isPrime ; notContained = Ring.1R R ; notContainedIsNotContained = notCon }
  where
    abstract
      notCon : pred 1R → False
      notCon 1=0 = IntegralDomain.nontrivial intDom (translate i 1=0)
      isPrime : {a b : A} → pred (a * b) → (pred a → False) → pred b
      isPrime {a} {b} predAB !predA = translate' i (IntegralDomain.intDom intDom (translate i predAB) λ t → !predA (translate' i t))

private
  dividesZero : {a : A} → generatedIdealPred R 0R a → a ∼ 0R
  dividesZero (c , pr) = symmetric (transitive (symmetric (transitive *Commutative timesZero)) pr)

zeroIdealPrimeImpliesIntDom : PrimeIdeal (generatedIdeal R 0R) → IntegralDomain R
IntegralDomain.intDom (zeroIdealPrimeImpliesIntDom record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) {a} {b} ab=0 a!=0 with isPrime {a} {b} (1R , transitive (transitive *Commutative timesZero) (symmetric ab=0)) (λ 0|a → a!=0 (dividesZero 0|a))
... | c , 0c=b = transitive (symmetric 0c=b) (transitive *Commutative timesZero)
IntegralDomain.nontrivial (zeroIdealPrimeImpliesIntDom record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) 1=0 = notContainedIsNotContained (notContained , transitive (*WellDefined (symmetric 1=0) reflexive) identIsIdent)

intDomImpliesZeroIdealPrime : IntegralDomain R → PrimeIdeal (generatedIdeal R 0R)
PrimeIdeal.isPrime (intDomImpliesZeroIdealPrime intDom) (c , 0=ab) 0not|a with IntegralDomain.intDom intDom (transitive (symmetric 0=ab) (transitive *Commutative timesZero)) (λ a=0 → 0not|a (0R , transitive timesZero (symmetric a=0)))
... | b=0 = 0R , transitive timesZero (symmetric b=0)
PrimeIdeal.notContained (intDomImpliesZeroIdealPrime intDom) = 1R
PrimeIdeal.notContainedIsNotContained (intDomImpliesZeroIdealPrime intDom) (c , 0c=1) = IntegralDomain.nontrivial intDom (symmetric (transitive (symmetric (transitive *Commutative timesZero)) 0c=1))

primeIdealWellDefined : {c : _} {pred2 : A → Set c} (ideal2 : Ideal R pred2) → ({x : A} → pred x → pred2 x) → ({x : A} → pred2 x → pred x) → PrimeIdeal i → PrimeIdeal ideal2
PrimeIdeal.isPrime (primeIdealWellDefined ideal2 predToPred2 pred2ToPred record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) p2ab notP2a = predToPred2 (isPrime (pred2ToPred p2ab) λ p → notP2a (predToPred2 p))
PrimeIdeal.notContained (primeIdealWellDefined ideal2 predToPred2 pred2ToPred record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) = notContained
PrimeIdeal.notContainedIsNotContained (primeIdealWellDefined ideal2 predToPred2 pred2ToPred record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) pred2Not = notContainedIsNotContained (pred2ToPred pred2Not)


text:
{-A
Polynomials over commutative rings
==================================
-}
{-# OPTIONS --safe #-}

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

module Cubical.Algebra.Polynomials.Univariate.Base where

open import Cubical.HITs.PropositionalTruncation
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Nat renaming (_+_ to _Nat+_; _·_ to _Nat·_) hiding (·-comm)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty.Base renaming (rec to ⊥rec )
open import Cubical.Data.Bool

open import Cubical.Algebra.Group hiding (Bool)
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

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

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

module PolyMod (R' : CommRing ℓ) where
  private
    R = fst R'
  open CommRingStr (snd R') public

-------------------------------------------------------------------------------------------
-- First definition of a polynomial.
-- A polynomial a₁ +  a₂x + ... + aⱼxʲ of degree j is represented as a list [a₁, a₂, ...,aⱼ]
-- modulo trailing zeros.
-------------------------------------------------------------------------------------------

  data Poly : Type ℓ where
    []    : Poly
    _∷_  : (a : R) → (p : Poly) → Poly
    drop0 : 0r ∷ [] ≡ []

  infixr 5 _∷_

  module Elim (B      : Poly → Type ℓ')
              ([]*    : B [])
              (cons*  : (r : R) (p : Poly) (b : B p) → B (r ∷ p))
              (drop0* : PathP (λ i → B (drop0 i)) (cons* 0r [] []*) []*) where

   f : (p : Poly) → B p
   f [] = []*
   f (x ∷ p) = cons* x p (f p)
   f (drop0 i) = drop0* i

  -- Given a proposition (as type) ϕ ranging over polynomials, we prove it by:
  -- ElimProp.f ϕ ⌜proof for base case []⌝ ⌜proof for induction case a ∷ p⌝
  --           ⌜proof that ϕ actually is a proposition over the domain of polynomials⌝
  module ElimProp (B : Poly → Type ℓ')
                  ([]* : B [])
                  (cons* : (r : R) (p : Poly) (b : B p) → B (r ∷ p))
                  (BProp : {p : Poly} → isProp (B p)) where
   f : (p : Poly) → B p
   f = Elim.f B []* cons* (toPathP (BProp (transport (λ i → B (drop0 i)) (cons* 0r [] []*)) []*))

  module Rec (B : Type ℓ')
             ([]* : B)
             (cons* : R → B → B)
             (drop0* : cons* 0r []* ≡ []*)
             (Bset : isSet B) where
    f : Poly → B
    f = Elim.f (λ _ → B) []* (λ r p b → cons* r b) drop0*

  module RecPoly ([]* : Poly) (cons* : R → Poly → Poly) (drop0* : cons* 0r []* ≡ []*) where
    f : Poly → Poly
    f [] = []*
    f (a ∷ p) = cons* a (f p)
    f (drop0 i) = drop0* i

--------------------------------------------------------------------------------------------------
-- Second definition of a polynomial. The purpose of this second definition is to
-- facilitate the proof that the first definition is a set. The two definitions are
-- then shown to be equivalent.
-- A polynomial a₀ +  a₁x + ... + aⱼxʲ of degree j is represented as a function f
-- such that for i ∈ ℕ we have  f(i) = aᵢ if i ≤ j, and 0 for i > j
--------------------------------------------------------------------------------------------------

  PolyFun : Type ℓ
  PolyFun = Σ[ p ∈ (ℕ → R) ] (∃[ n ∈ ℕ ] ((m : ℕ) → n ≤ m → p m ≡ 0r))

  isSetPolyFun : isSet PolyFun
  isSetPolyFun = isSetΣSndProp (isSetΠ (λ x → isSetCommRing R')) λ f x y → squash x y

  --construction of the function that represents the polynomial
  Poly→Fun : Poly → (ℕ → R)
  Poly→Fun [] = (λ _ → 0r)
  Poly→Fun (a ∷ p) = (λ n → if isZero n then a else Poly→Fun p (predℕ n))
  Poly→Fun (drop0 i) = lemma i
    where
    lemma : (λ n → if isZero n then 0r else 0r) ≡ (λ _ → 0r)
    lemma i zero = 0r
    lemma i (suc n) = 0r

  Poly→Prf : (p : Poly) → ∃[ n ∈ ℕ ] ((m : ℕ) → n ≤ m → (Poly→Fun p m ≡ 0r))
  Poly→Prf = ElimProp.f (λ p →  ∃[ n ∈ ℕ ] ((m : ℕ) → n ≤ m → (Poly→Fun p m ≡ 0r)))
                        ∣ 0 , (λ m ineq → refl) ∣
                        (λ r p → map ( λ (n , ineq) → (suc n) ,
                                       λ { zero h → ⊥rec (znots (sym (≤0→≡0 h))) ;
                                           (suc m) h → ineq m (pred-≤-pred h)
                                         }
                                     )
                        )
                        squash

  Poly→PolyFun : Poly → PolyFun
  Poly→PolyFun p = (Poly→Fun p) , (Poly→Prf p)

----------------------------------------------------
-- Start of code by Anders Mörtberg and Evan Cavallo

  at0 : (ℕ → R) → R
  at0 f = f 0

  atS : (ℕ → R) → (ℕ → R)
  atS f n = f (suc n)

  polyEq : (p p' : Poly) → Poly→Fun p ≡ Poly→Fun p' → p ≡ p'
  polyEq [] [] _ = refl
  polyEq [] (a ∷ p') α =
    sym drop0 ∙∙ cong₂ _∷_ (cong at0 α) (polyEq [] p' (cong atS α)) ∙∙ refl
  polyEq [] (drop0 j) α k =
    hcomp
      (λ l → λ
        { (j = i1) → drop0 l
        ; (k = i0) → drop0 l
        ; (k = i1) → drop0 (j ∧ l)
        })
      (is-set 0r 0r (cong at0 α) refl j k ∷ [])
  polyEq (a ∷ p) [] α =
    refl ∙∙ cong₂ _∷_ (cong at0 α) (polyEq p [] (cong atS α)) ∙∙ drop0
  polyEq (a ∷ p) (a₁ ∷ p') α =
    cong₂ _∷_ (cong at0 α) (polyEq p p' (cong atS α))
  polyEq (a ∷ p) (drop0 j) α k =
    hcomp -- filler
      (λ l → λ
        { (k = i0) → a ∷ p
        ; (k = i1) → drop0 (j ∧ l)
        ; (j = i0) → at0 (α k) ∷ polyEq p [] (cong atS α) k
        })
      (at0 (α k) ∷ polyEq p [] (cong atS α) k)
  polyEq (drop0 i) [] α k =
    hcomp
      (λ l → λ
        { (i = i1) → drop0 l
        ; (k = i0) → drop0 (i ∧ l)
        ; (k = i1) → drop0 l
        })
      (is-set 0r 0r (cong at0 α) refl i k ∷ [])
  polyEq (drop0 i) (a ∷ p') α k =
    hcomp -- filler
      (λ l → λ
        { (k = i0) → drop0 (i ∧ l)
        ; (k = i1) → a ∷ p'
        ; (i = i0) → at0 (α k) ∷ polyEq [] p' (cong atS α) k
        })
      (at0 (α k) ∷ polyEq [] p' (cong atS α) k)
  polyEq (drop0 i) (drop0 j) α k =
    hcomp
      (λ l → λ
        { (k = i0) → drop0 (i ∧ l)
        ; (k = i1) → drop0 (j ∧ l)
        ; (i = i0) (j = i0) → at0 (α k) ∷ []
        ; (i = i1) (j = i1) → drop0 l
        })
      (is-set 0r 0r (cong at0 α) refl (i ∧ j) k ∷ [])

  PolyFun→Poly+ : (q : PolyFun) → Σ[ p ∈ Poly ] Poly→Fun p ≡ q .fst
  PolyFun→Poly+ (f , pf) = rec lem (λ x → rem1 f (x .fst) (x .snd) ,
                                               funExt (rem2 f (fst x) (snd x))
                                   ) pf
    where
    lem : isProp (Σ[ p ∈ Poly ] Poly→Fun p ≡ f)
    lem (p , α) (p' , α') =
      ΣPathP (polyEq p p' (α ∙ sym α'), isProp→PathP (λ i → (isSetΠ λ _ → is-set) _ _) _ _)

    rem1 : (p : ℕ → R) (n : ℕ) → ((m : ℕ) → n ≤ m → p m ≡ 0r) → Poly
    rem1 p zero h = []
    rem1 p (suc n) h = p 0 ∷ rem1 (λ x → p (suc x)) n (λ m x → h (suc m) (suc-≤-suc x))

    rem2 : (f : ℕ → R) (n : ℕ) → (h : (m : ℕ) → n ≤ m → f m ≡ 0r) (m : ℕ) →
                                                                 Poly→Fun (rem1 f n h) m ≡ f m
    rem2 f zero h m = sym (h m zero-≤)
    rem2 f (suc n) h zero = refl
    rem2 f (suc n) h (suc m) = rem2 (λ x → f (suc x)) n (λ k p → h (suc k) (suc-≤-suc p)) m

  PolyFun→Poly : PolyFun → Poly
  PolyFun→Poly q = PolyFun→Poly+ q .fst

  PolyFun→Poly→PolyFun : (p : Poly) → PolyFun→Poly (Poly→PolyFun p) ≡ p
  PolyFun→Poly→PolyFun p = polyEq _ _ (PolyFun→Poly+ (Poly→PolyFun p) .snd)

--End of code by Mörtberg and Cavallo
-------------------------------------

  isSetPoly : isSet Poly
  isSetPoly = isSetRetract Poly→PolyFun
                           PolyFun→Poly
                           PolyFun→Poly→PolyFun
                           isSetPolyFun

ext: agda

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
-- This module gives an introduction to the module system of Agda.

module Introduction.Modules where

---------------------------------------------------------------------------
-- Simple sub-modules
---------------------------------------------------------------------------

-- As mentioned in 'Introduction.Basics' each file contains a single top-level
-- module. This module can contain any number of sub-modules. A sub-module is
-- declared in the same way as the top-level module, except that its name is
-- not qualified.

module Numbers where

  -- The contents of the top-level module do not have to be indented, but the
  -- contents of a sub-module do.

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

-- Outside a module its contents can be accessed using the name of the module.

one : Numbers.Nat
one = Numbers.suc Numbers.zero

-- Of course, this would get very tedious after a while, so to bring the
-- contents of a module into scope you can use an 'open' declaration.

open Numbers

two : Nat
two = suc one

-- When opening a module it is possible to control what names are brought into
-- scope. The open declaration supports three modifiers :

--  using (x1; ..; xn)    only bring x1 .. xn into scope
--  renaming (x to y;..)  bring y into scope and make it refer to the name x
--                        from the opened module.
--  hiding (x1; ..; xn)   bring everything except x1 .. xn into scope

-- The using and hiding modifiers can be combined with renaming but not with
-- each other.

-- For example, this will bring the names z and s (and nothing else) into
-- scope as new names for zero and suc.
open Numbers using () renaming (zero to z; suc to s)

-- We can now pattern match on the renamed constructors.
plus : Nat -> Nat -> Nat
plus  z    m = m
plus (s n) m = s (plus n m)

---------------------------------------------------------------------------
-- 'private' and 'abstract'
---------------------------------------------------------------------------

-- Above we saw how to control which names are brought into scope when opening
-- a module. It is also possible to restrict what is visible outside a module
-- by declaring things 'private'. Declaring something private will only prevent
-- someone from using it outside the module, it doesn't prevent it from showing
-- up after reduction, or from it to reduce.
-- To prevent something from reducing (effectively hiding the definition) it
-- can be declared 'abstract'.

module Datastructures where

  private

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

    _++_ : {A : Set} -> List A -> List A -> List A
    nil       ++ ys = ys
    (x :: xs) ++ ys = x :: (xs ++ ys)

    reverse : {A : Set} -> List A -> List A
    reverse  nil      = nil
    reverse (x :: xs) = reverse xs ++ (x :: nil)

  -- Not making the stack operations abstract will reveal the underlying
  -- implementation, even though it's private.
  Stack : Set -> Set
  Stack A = List A

  emptyS : {A : Set} -> Stack A
  emptyS = nil

  push : {A : Set} -> A -> Stack A -> Stack A
  push x xs = x :: xs

  abstract

    -- An abstract datatype doesn't reveal its constructors
    data Queue (A : Set) : Set where
      queue : (front back : List A) -> Queue A  -- invariant : if the front is
                                                -- empty, so is the back

    -- Abstraction is contagious, anything that pattern matches on a queue must
    -- also be abstract.
    private

      -- make sure the invariant is preserved
      flip : {A : Set} -> Queue A -> Queue A
      flip (queue nil back) = queue (reverse back) nil
      flip q                = q

    -- these functions will not reduce outside the module
    emptyQ : {A : Set} -> Queue A
    emptyQ = queue nil nil

    enqueue : {A : Set} -> A -> Queue A -> Queue A
    enqueue x (queue front back) = flip (queue front (x :: back))

open Datastructures

testS = push    zero emptyS
testQ = enqueue zero emptyQ

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Level

open import Categories.Category
open import Categories.Functor hiding (_≡_; _∘_)

record CartesianProperties {o₀ ℓ₀ e₀} {o₁ ℓ₁ e₁}
                           {E : Category o₀ ℓ₀ e₀} {B : Category o₁ ℓ₁ e₁}
                           {p : Functor E B} {e′ e} {φ : E [ e′ , e ]}
                           {e′′ : Category.Obj E} {ψ : E [ e′′ , e ]}
                           {g : B [ Functor.F₀ p e′′ , Functor.F₀ p e′ ]}
                           (pf : Category._≡_ B (Category._∘_ B (Functor.F₁ p φ) g) (Functor.F₁ p ψ)) : Set (o₀ ⊔ ℓ₀ ⊔ e₀ ⊔ ℓ₁ ⊔ e₁) where
  private module E = Category E
  private module B = Category B
  open B using (_∘_; _≡_)
  open E using () renaming (_∘_ to _∘E_; _≡_ to _≡E_)
  open Functor p renaming (F₀ to p₀; F₁ to p₁)

  field
    χ        : E [ e′′ , e′ ]
    ψ≡φ∘χ    : ψ ≡E φ ∘E χ
    p₁[χ]≡g  : p₁ χ ≡ g

    χ-unique : (f : E [ e′′ , e′ ]) → ψ ≡E φ ∘E f → p₁ f ≡ g → f ≡E χ

record Cartesian {o₀ ℓ₀ e₀} {o₁ ℓ₁ e₁} {E : Category o₀ ℓ₀ e₀} {B : Category o₁ ℓ₁ e₁} (p : Functor E B) {e′ e} (φ : E [ e′ , e ]) : Set (o₀ ⊔ ℓ₀ ⊔ e₀ ⊔ ℓ₁ ⊔ e₁) where
  private module E = Category E
  private module B = Category B
  open B using (_∘_; _≡_)
  open E using () renaming (_∘_ to _∘E_; _≡_ to _≡E_)
  open Functor p renaming (F₀ to p₀; F₁ to p₁)

  field
    properties : ∀ {e′′} (ψ : E [ e′′ , e ]) (g : B [ p₀ e′′ , p₀ e′ ]) (pf : p₁ φ ∘ g ≡ p₁ ψ) → CartesianProperties {p = p} pf

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- Paolo Capriotti's variant of higher lenses
------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

import Equality.Path as P

module Lens.Non-dependent.Higher.Capriotti
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

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

open import Bijection equality-with-J as B using (_↔_)
open import Coherently-constant eq using (Coherently-constant)
open import Equality.Decidable-UIP equality-with-J using (Constant)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
open import Preimage equality-with-J
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher eq as Higher
import Lens.Non-dependent.Higher.Capriotti.Variant eq as Variant
import Lens.Non-dependent.Traditional eq as Traditional

private
  variable
    a b p : Level
    A B   : Type a
    P Q   : A → Type p

------------------------------------------------------------------------
-- Coherently-constant

-- A preservation lemma for Coherently-constant.
--
-- Note that P and Q must target the same universe.

Coherently-constant-map :
  {P : A → Type p} {Q : B → Type p} →
  Univalence p →
  (f : B → A) →
  (∀ x → P (f x) ≃ Q x) →
  Coherently-constant P → Coherently-constant Q
Coherently-constant-map {P = P} {Q = Q} univ f P≃Q (R , P≡R) =
    R ∘ T.∥∥-map f
  , ⟨ext⟩ λ x → ≃⇒≡ univ
      (Q x        ↝⟨ inverse $ P≃Q x ⟩
       P (f x)    ↝⟨ ≡⇒≃ $ cong (_$ f x) P≡R ⟩□
       R ∣ f x ∣  □)

-- Coherently-constant is, in a certain sense, closed under Σ.
--
-- This lemma is due to Paolo Capriotti.

Coherently-constant-Σ :
  Coherently-constant P →
  Coherently-constant Q →
  Coherently-constant (λ x → ∃ λ (y : P x) → Q (x , y))
Coherently-constant-Σ {P = P} {Q = Q} (P′ , p) (Q′ , q) =
    (λ x → ∃ λ (y : P′ x) →
               Q′ (T.elim
                     (λ x → P′ x → ∥ ∃ P ∥)
                     (λ _ → Π-closure ext 1 λ _ →
                            T.truncation-is-proposition)
                     (λ x y → ∣ x , subst id (sym (p′ x)) y ∣)
                     x y))
  , (⟨ext⟩ λ x →

     ((∃ λ (y : P x) → Q (x , y))                                ≡⟨ (cong (uncurry Σ) $ Σ-≡,≡→≡ (p′ x) $ ⟨ext⟩ λ y →

        subst (λ P → P → Type _) (p′ x) (λ y → Q (x , y)) y          ≡⟨ subst-→-domain _ _ ⟩

        Q (x , subst id (sym (p′ x)) y)                              ≡⟨ cong (_$ (x , subst id (sym (p′ x)) y)) q ⟩∎

        Q′ ∣ x , subst id (sym (p′ x)) y ∣                           ∎) ⟩∎

      (∃ λ (y : P′ ∣ x ∣) → Q′ ∣ x , subst id (sym (p′ x)) y ∣)  ∎))
  where
  p′ : ∀ _ → _
  p′ x = cong (_$ x) p

-- If the domain of f is stable, then there is a split surjection from
-- Constant f to Coherently-constant f.
--
-- In "Notions of Anonymous Existence in Martin-Löf Type Theory" Kraus
-- Escardó, Coquand and Altenkirch prove that Constant f implies
-- Coherently-constant f when the domain of f is stable, and the other
-- direction holds without the assumption.

Constant↠Coherently-constant :
  {f : A → B} →
  (∥ A ∥ → A) →
  Constant f ↠ Coherently-constant f
Constant↠Coherently-constant {f = f} s = record
  { logical-equivalence = record
    { to   = λ c → f ∘ s
           , ⟨ext⟩ λ x → c x (s ∣ x ∣)
    ; from = λ (g , eq) x y →
        f x      ≡⟨ cong (_$ x) eq ⟩
        g ∣ x ∣  ≡⟨ cong g $ T.truncation-is-proposition ∣ x ∣ ∣ y ∣ ⟩
        g ∣ y ∣  ≡⟨ cong (_$ y) $ sym eq ⟩∎
        f y      ∎
    }
  ; right-inverse-of = λ (g , eq) → Σ-≡,≡→≡
      (f ∘ s        ≡⟨ cong (_∘ s) eq ⟩
       g ∘ ∣_∣ ∘ s  ≡⟨ (⟨ext⟩ λ x → cong g $ T.truncation-is-proposition ∣ s x ∣ x) ⟩∎
       g            ∎)
      (subst (λ g → f ≡ g ∘ ∣_∣)
         (trans (cong (_∘ s) eq)
            (⟨ext⟩ λ x →
             cong g (T.truncation-is-proposition ∣ s x ∣ x)))
         (⟨ext⟩ λ x →
          trans (cong (_$ x) eq)
            (trans (cong g (T.truncation-is-proposition
                              ∣ x ∣ (∣ s ∣ x ∣ ∣)))
               (cong (_$ s ∣ x ∣) (sym eq))))                            ≡⟨ trans (subst-∘ _ _ _) $
                                                                            sym trans-subst ⟩
       trans
         (⟨ext⟩ λ x →
          trans (cong (_$ x) eq)
            (trans (cong g (T.truncation-is-proposition
                              ∣ x ∣ (∣ s ∣ x ∣ ∣)))
               (cong (_$ s ∣ x ∣) (sym eq))))
         (cong (_∘ ∣_∣) $
          trans (cong (_∘ s) eq)
            (⟨ext⟩ λ x →
             cong g (T.truncation-is-proposition ∣ s x ∣ x)))            ≡⟨ cong₂ trans
                                                                              (trans (ext-trans _ _) $
                                                                               cong₂ trans
                                                                                (_≃_.right-inverse-of
                                                                                (Eq.extensionality-isomorphism bad-ext) _)
                                                                                (trans (ext-trans _ _) $
                                                                                cong (trans _) $
                                                                                cong ⟨ext⟩ $ ⟨ext⟩ λ _ →
                                                                                trans (sym $ cong-∘ _ _ _) $
                                                                                cong (cong _) $ cong-sym _ _))
                                                                              (trans (cong-trans _ _ _) $
                                                                               cong₂ trans
                                                                                (cong-∘ _ _ _)
                                                                                (cong-pre-∘-ext _)) ⟩
       trans
         (trans eq
            (trans (⟨ext⟩ λ x →
                    cong g (T.truncation-is-proposition
                              ∣ x ∣ (∣ s ∣ x ∣ ∣)))
               (⟨ext⟩ λ x → cong (_$ x) (sym (cong (_∘ s ∘ ∣_∣) eq)))))
         (trans (cong (_∘ s ∘ ∣_∣) eq)
            (⟨ext⟩ λ x →
             cong g (T.truncation-is-proposition
                       (∣ s ∣ x ∣ ∣) ∣ x ∣)))                            ≡⟨ trans (trans-assoc _ _ _) $
                                                                            cong (trans _) $
                                                                            trans (trans-assoc _ _ _) $
                                                                            cong₂ trans
                                                                              (trans (cong ⟨ext⟩ $ ⟨ext⟩ λ _ →
                                                                                trans (cong (cong _) $
                                                                                H-level.mono₁ 1 T.truncation-is-proposition _ _) $
                                                                                cong-sym _ _) $
                                                                               ext-sym _)
                                                                              (cong (flip trans _) $
                                                                               _≃_.right-inverse-of
                                                                                (Eq.extensionality-isomorphism bad-ext) _) ⟩
       trans eq
         (trans (sym $
                 ⟨ext⟩ λ x →
                 cong g (T.truncation-is-proposition
                           (∣ s ∣ x ∣ ∣) ∣ x ∣))
            (trans (sym (cong (_∘ s ∘ ∣_∣) eq))
               (trans (cong (_∘ s ∘ ∣_∣) eq)
                  (⟨ext⟩ λ x →
                   cong g (T.truncation-is-proposition
                          (∣ s ∣ x ∣ ∣) ∣ x ∣)))))                       ≡⟨ trans (cong (trans _) $
                                                                                trans (cong (trans _) $
                                                                                trans-sym-[trans] _ _) $
                                                                                trans-symˡ _) $
                                                                            trans-reflʳ _ ⟩∎
       eq                                                                ∎)
  }

------------------------------------------------------------------------
-- The lens type family

-- Higher lenses, as presented by Paolo Capriotti, who seems to have
-- been first to describe a notion of higher lens
-- (http://homotopytypetheory.org/2014/04/29/higher-lenses/).

Lens : Type a → Type b → Type (lsuc (a ⊔ b))
Lens A B = ∃ λ (get : A → B) → Coherently-constant (get ⁻¹_)

-- Some derived definitions (based on Paolo's presentation).

module Lens {A : Type a} {B : Type b} (l : Lens A B) where

  -- A getter.

  get : A → B
  get = proj₁ l

  -- A predicate.

  H : Pow a ∥ B ∥
  H = proj₁ (proj₂ l)

  -- An equality.

  get⁻¹-≡ : (get ⁻¹_) ≡ H ∘ ∣_∣
  get⁻¹-≡ = proj₂ (proj₂ l)

  -- An equivalence.

  get⁻¹-≃ : ∀ b → get ⁻¹ b ≃ H ∣ b ∣
  get⁻¹-≃ = ≡⇒≃ ∘ ext⁻¹ get⁻¹-≡

  -- All the getter's fibres are equivalent.

  get⁻¹-constant : (b₁ b₂ : B) → get ⁻¹ b₁ ≃ get ⁻¹ b₂
  get⁻¹-constant b₁ b₂ =
    get ⁻¹ b₁  ↝⟨ get⁻¹-≃ b₁ ⟩
    H ∣ b₁ ∣   ↝⟨ ≡⇒≃ $ cong H $ T.truncation-is-proposition _ _ ⟩
    H ∣ b₂ ∣   ↝⟨ inverse $ get⁻¹-≃ b₂ ⟩□
    get ⁻¹ b₂  □

  -- A setter.

  set : A → B → A
  set a b =                    $⟨ _≃_.to (get⁻¹-constant (get a) b) ⟩
    (get ⁻¹ get a → get ⁻¹ b)  ↝⟨ _$ (a , refl _) ⟩
    get ⁻¹ b                   ↝⟨ proj₁ ⟩□
    A                          □

instance

  -- The lenses defined above have getters and setters.

  has-getter-and-setter :
    Has-getter-and-setter (Lens {a = a} {b = b})
  has-getter-and-setter = record
    { get = Lens.get
    ; set = Lens.set
    }

------------------------------------------------------------------------
-- Equality characterisation lemmas

-- An equality characterisation lemma.

equality-characterisation₁ :
  {l₁ l₂ : Lens A B} →

  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)
equality-characterisation₁ {A = A} {B = B} {l₁ = l₁} {l₂ = l₂} =
  l₁ ≡ l₂                                                                ↝⟨ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ Σ-assoc ⟩

  ((get l₁ , H l₁) , get⁻¹-≡ l₁) ≡ ((get l₂ , H l₂) , get⁻¹-≡ l₂)        ↔⟨ inverse B.Σ-≡,≡↔≡ ⟩

  (∃ λ (eq : (get l₁ , H l₁) ≡ (get l₂ , H l₂)) →
     subst (λ (g , H) → g ⁻¹_ ≡ H ∘ ∣_∣) eq (get⁻¹-≡ l₁) ≡ get⁻¹-≡ l₂)   ↝⟨ (Σ-cong-contra ≡×≡↔≡ λ _ → F.id) ⟩

  (∃ λ ((g , h) : get l₁ ≡ get l₂ × H l₁ ≡ H l₂) →
     subst (λ (g , H) → g ⁻¹_ ≡ H ∘ ∣_∣) (cong₂ _,_ g h) (get⁻¹-≡ l₁) ≡
     get⁻¹-≡ l₂)                                                         ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     subst (λ (g , H) → g ⁻¹_ ≡ H ∘ ∣_∣) (cong₂ _,_ g h) (get⁻¹-≡ l₁) ≡
     get⁻¹-≡ l₂)                                                         ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ≡⇒↝ _ $ cong (_≡ _) $
                                                                             lemma _ _) ⟩
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     trans (sym (cong _⁻¹_ g)) (trans (get⁻¹-≡ l₁) (cong (_∘ ∣_∣) h)) ≡
     get⁻¹-≡ l₂)                                                         ↝⟨ (Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                             Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                             F.id) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (cong (_∘ ∣_∣) (⟨ext⟩ h))) ≡
     get⁻¹-≡ l₂)                                                         ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ≡⇒↝ _ $
                                                                             cong (λ eq → trans _ (trans _ eq) ≡ _) $
                                                                             cong-pre-∘-ext _) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)                                                         □
  where
  open Lens

  lemma : ∀ _ (h : H l₁ ≡ H l₂) → _
  lemma g h =
    subst (λ (g , H) → g ⁻¹_ ≡ H ∘ ∣_∣) (cong₂ _,_ g h) (get⁻¹-≡ l₁)     ≡⟨ subst-in-terms-of-trans-and-cong ⟩

    trans (sym (cong (λ (g , _) → g ⁻¹_) (cong₂ _,_ g h)))
      (trans (get⁻¹-≡ l₁) (cong (λ (_ , H) → H ∘ ∣_∣) (cong₂ _,_ g h)))  ≡⟨ cong₂ (λ p q → trans (sym p) (trans (get⁻¹-≡ l₁) q))
                                                                              (trans (sym $ cong-∘ _ _ _) $
                                                                               cong (cong _⁻¹_) $ cong-proj₁-cong₂-, _ _)
                                                                              (trans (sym $ cong-∘ _ _ _) $
                                                                               cong (cong (_∘ ∣_∣)) $ cong-proj₂-cong₂-, _ h) ⟩∎
    trans (sym (cong _⁻¹_ g)) (trans (get⁻¹-≡ l₁) (cong (_∘ ∣_∣) h))     ∎

-- Another equality characterisation lemma.

equality-characterisation₂ :
  {A : Type a} {B : Type b} {l₁ l₂ : Lens A B}
  (univ : Univalence (a ⊔ b)) →

  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (≃⇒≡ univ ∘ h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)
equality-characterisation₂ {A = A} {B = B} {l₁ = l₁} {l₂ = l₂} univ =
  l₁ ≡ l₂                                                   ↝⟨ equality-characterisation₁ ⟩

  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)                                            ↝⟨ (∃-cong λ _ →
                                                                Σ-cong-contra (∀-cong ext λ _ → inverse $ ≡≃≃ univ) λ _ → F.id) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (≃⇒≡ univ ∘ h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)                                            □
  where
  open Lens

------------------------------------------------------------------------
-- Conversions between different kinds of lenses

-- Variant.Coherently-constant P is equivalent to
-- Coherently-constant P (assuming univalence).

Variant-coherently-constant≃Coherently-constant :
  {P : A → Type p} →
  Univalence p →
  Variant.Coherently-constant P ≃ Coherently-constant P
Variant-coherently-constant≃Coherently-constant
  {A = A} {p = p} {P = P} univ =

  Variant.Coherently-constant P                     ↔⟨⟩
  (∃ λ (H : ∥ A ∥ → Type p) → ∀ b → P b ≃ H ∣ b ∣)  ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → inverse $ ≡≃≃ univ) ⟩
  (∃ λ (H : ∥ A ∥ → Type p) → ∀ b → P b ≡ H ∣ b ∣)  ↝⟨ (∃-cong λ _ → Eq.extensionality-isomorphism bad-ext) ⟩
  (∃ λ (H : ∥ A ∥ → Type p) → P ≡ H ∘ ∣_∣)          ↔⟨⟩
  Coherently-constant P                             □

-- The lenses defined above are equivalent to those defined in Variant
-- (assuming univalence).

Variant-lens≃Lens :
  {A : Type a} {B : Type b} →
  Block "conversion" →
  Univalence (a ⊔ b) →
  Variant.Lens A B ≃ Lens A B
Variant-lens≃Lens {a = a} {A = A} {B = B} ⊠ univ =
  Variant.Lens A B                                             ↔⟨⟩
  (∃ λ (get : A → B) → Variant.Coherently-constant (get ⁻¹_))  ↝⟨ (∃-cong λ _ → Variant-coherently-constant≃Coherently-constant univ) ⟩
  (∃ λ (get : A → B) → Coherently-constant (get ⁻¹_))          ↔⟨⟩
  Lens A B                                                     □

-- The conversion preserves getters and setters.

Variant-lens≃Lens-preserves-getters-and-setters :
  {A : Type a} {B : Type b}
  (bc : Block "conversion")
  (univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (Variant-lens≃Lens bc univ))
Variant-lens≃Lens-preserves-getters-and-setters
  {A = A} {B = B} bc@⊠ univ =
  Preserves-getters-and-setters-→-↠-⇔
    (_≃_.surjection (Variant-lens≃Lens bc univ)) λ l →
      refl _
    , ⟨ext⟩ λ a → ⟨ext⟩ λ b →
      (let eq₁ = cong (H l) $
                   T.truncation-is-proposition ∣ get l a ∣ ∣ b ∣
           eq₂ = ⟨ext⟩ (≃⇒≡ univ ∘ get⁻¹-≃ l)
       in
       proj₁ (_≃_.from (≡⇒≃ (cong (_$ b) eq₂))
                (≡⇒→ eq₁ (≡⇒→ (cong (_$ get l a) eq₂) (a , refl _))))   ≡⟨ cong₂ (λ p q → proj₁ (_≃_.from p (≡⇒→ eq₁ (_≃_.to q (a , refl _)))))
                                                                             (lemma l _)
                                                                             (lemma l _) ⟩∎
       proj₁ (_≃_.from (get⁻¹-≃ l b)
                (≡⇒→ eq₁ (_≃_.to (get⁻¹-≃ l (get l a)) (a , refl _))))  ∎)
  where
  open Variant.Lens

  lemma :
    ∀ (l : Variant.Lens A B) b →
    ≡⇒≃ (cong (_$ b) (⟨ext⟩ (≃⇒≡ univ ∘ get⁻¹-≃ l))) ≡ get⁻¹-≃ l b
  lemma l b =
    ≡⇒≃ (cong (_$ b) (⟨ext⟩ (≃⇒≡ univ ∘ get⁻¹-≃ l)))  ≡⟨ cong ≡⇒≃ $ cong-ext (≃⇒≡ univ ∘ get⁻¹-≃ l) ⟩
    ≡⇒≃ (≃⇒≡ univ (get⁻¹-≃ l b))                      ≡⟨ _≃_.right-inverse-of (≡≃≃ univ) _ ⟩∎
    get⁻¹-≃ l b                                       ∎

-- The lenses defined above are equivalent to those defined in Higher
-- (assuming univalence).

Lens≃Higher-lens :
  {A : Type a} {B : Type b} →
  Block "conversion" →
  Univalence (a ⊔ b) →
  Lens A B ≃ Higher.Lens A B
Lens≃Higher-lens {A = A} {B = B} bc univ =
  Lens A B          ↝⟨ inverse $ Variant-lens≃Lens bc univ ⟩
  Variant.Lens A B  ↝⟨ Variant.Lens≃Higher-lens bc univ ⟩□
  Higher.Lens A B   □

-- The conversion preserves getters and setters.

Lens≃Higher-lens-preserves-getters-and-setters :
  {A : Type a} {B : Type b}
  (bc : Block "conversion")
  (univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (Lens≃Higher-lens bc univ))
Lens≃Higher-lens-preserves-getters-and-setters bc univ =
  Preserves-getters-and-setters-⇔-∘
    {f = _≃_.logical-equivalence $ Variant.Lens≃Higher-lens bc univ}
    (Variant.Lens≃Higher-lens-preserves-getters-and-setters bc univ)
    (Preserves-getters-and-setters-⇔-inverse
       {f = _≃_.logical-equivalence $ Variant-lens≃Lens bc univ}
       (Variant-lens≃Lens-preserves-getters-and-setters bc univ))

-- An alternative proof showing that Lens A B is equivalent to
-- Higher.Lens A B (assuming univalence).
--
-- This proof was simplified following a suggestion by Paolo
-- Capriotti.
--
-- I have not proved that this equivalence preserves getters and
-- setters.

Lens≃Higher-lens′ :
  {A : Type a} {B : Type b} →
  Univalence (a ⊔ b) →
  Lens A B ≃ Higher.Lens A B
Lens≃Higher-lens′ {a = a} {b = b} {A = A} {B = B} univ =

  (∃ λ (g : A → B) → ∃ λ (H : Pow a ∥ B ∥) →
     (g ⁻¹_) ≡ H ∘ ∣_∣)                                  ↔⟨ Σ-cong lemma₂ (λ _ → ∃-cong (lemma₃ _)) ⟩

  (∃ λ (p : ∃ λ (P : Pow a B) → A ≃ ∃ P) →
   ∃ λ (H : Pow a ∥ B ∥) →
     proj₁ p ≡ H ∘ ∣_∣)                                  ↔⟨ ∃-comm ⟩

  (∃ λ (H : Pow a ∥ B ∥) →
   ∃ λ (p : ∃ λ (P : Pow a B) → A ≃ ∃ P) →
     proj₁ p ≡ H ∘ ∣_∣)                                  ↔⟨ (∃-cong λ _ → inverse Σ-assoc) ⟩

  (∃ λ (H : Pow a ∥ B ∥) →
   ∃ λ (P : Pow a B) →
      A ≃ ∃ P × P ≡ H ∘ ∣_∣)                             ↔⟨ (∃-cong λ _ → ∃-cong λ _ → ×-comm) ⟩

  (∃ λ (H : Pow a ∥ B ∥) →
   ∃ λ (P : Pow a B) →
      P ≡ H ∘ ∣_∣ × A ≃ ∃ P)                             ↔⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ eq →
                                                             Eq.≃-preserves ext F.id (∃-cong λ x → ≡⇒↝ _ (cong (_$ x) eq))) ⟩
  (∃ λ (H : Pow a ∥ B ∥) →
   ∃ λ (P : Pow a B) →
      P ≡ H ∘ ∣_∣ × A ≃ ∃ (H ∘ ∣_∣))                     ↔⟨ (∃-cong λ _ → Σ-assoc) ⟩

  (∃ λ (H : Pow a ∥ B ∥) →
   (∃ λ (P : Pow a B) → P ≡ H ∘ ∣_∣) ×
   A ≃ ∃ (H ∘ ∣_∣))                                      ↔⟨ (∃-cong λ _ →
                                                             drop-⊤-left-× λ _ →
                                                             _⇔_.to contractible⇔↔⊤ (singleton-contractible _)) ⟩

  (∃ λ (H : Pow a ∥ B ∥) → A ≃ ∃ (H ∘ ∣_∣))              ↔⟨ inverse $
                                                            Σ-cong (inverse $ Pow↔Fam a ext univ) (λ _ →
                                                            Eq.≃-preserves ext F.id F.id) ⟩

  (∃ λ (H : Fam a ∥ B ∥) → A ≃ ∃ ((proj₂ H ⁻¹_) ∘ ∣_∣))  ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (R : Type ℓ) →
   ∃ λ (f : R → ∥ B ∥) → A ≃ ∃ ((f ⁻¹_) ∘ ∣_∣))          ↔⟨ (∃-cong λ R → ∃-cong λ f →
                                                             Eq.≃-preserves ext F.id
                            (∃ ((f ⁻¹_) ∘ ∣_∣)                 ↔⟨ (∃-cong λ b → drop-⊤-right λ r →
                                                                     _⇔_.to contractible⇔↔⊤ $
                                                                       +⇒≡ T.truncation-is-proposition) ⟩
                             B × R                             ↔⟨ ×-comm ⟩□
                             R × B                             □)) ⟩

  (∃ λ (R : Type ℓ) → (R → ∥ B ∥) × (A ≃ (R × B)))       ↔⟨ (∃-cong λ _ → ×-comm) ⟩

  (∃ λ (R : Type ℓ) → (A ≃ (R × B)) × (R → ∥ B ∥))       ↔⟨ inverse Higher.Lens-as-Σ ⟩□

  Higher.Lens A B                                        □

  where
  ℓ = a ⊔ b

  lemma₁ : ∀ (g : A → B) b →
           g ⁻¹ b ↔ (g ∘ lower {ℓ = ℓ}) ⁻¹ b
  lemma₁ g b = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ { (a , ga≡b) → lift a , ga≡b }
        ; from = λ { (lift a , ga≡b) → a , ga≡b }
        }
      ; right-inverse-of = refl
      }
    ; left-inverse-of = refl
    }

  abstract

    lemma₂ : (A → B) ↔ ∃ λ (P : Pow a B) → A ≃ ∃ P
    lemma₂ = →↔Σ≃Σ ℓ ext univ

    lemma₃ :
      (g : A → B) (H : Pow a ∥ B ∥) →
      ((g ⁻¹_) ≡ H ∘ ∣_∣)
        ≃
      (proj₁ (_↔_.to lemma₂ g) ≡ H ∘ ∣_∣)
    lemma₃ g H =
      let lemma =
            F.id                 ≡⟨ sym ≡⇒↝-refl ⟩
            ≡⇒↝ _ (refl _)       ≡⟨ cong (≡⇒↝ _) $ sym sym-refl ⟩∎
            ≡⇒↝ _ (sym (refl _)) ∎
      in
      (g ⁻¹_) ≡ H ∘ ∣_∣                                            ↝⟨ inverse $ Eq.extensionality-isomorphism ext ⟩
      (∀ b → g ⁻¹ b ≡ H ∣ b ∣)                                     ↝⟨ ∀-cong ext (λ _ →
                                                                        ≡-preserves-≃ ext univ univ
                                                                          (Eq.↔⇒≃ $ lemma₁ _ _) F.id) ⟩
      (∀ b → (g ∘ lower) ⁻¹ b ≡ H ∣ b ∣)                           ↝⟨ Eq.extensionality-isomorphism ext ⟩
      ((g ∘ lower) ⁻¹_) ≡ H ∘ ∣_∣                                  ↝⟨ ≡⇒↝ _ $ cong (λ eq → (g ∘ lower ∘ _≃_.from eq ⁻¹_) ≡ H ∘ ∣_∣) lemma ⟩
      (g ∘ lower ∘ _≃_.from (≡⇒↝ _ (sym (refl _))) ⁻¹_) ≡ H ∘ ∣_∣  ↔⟨⟩
      proj₁ (_↔_.to lemma₂ g) ≡ H ∘ ∣_∣                            □

-- If the domain A is a set, then Traditional.Lens A B and Lens A B
-- are isomorphic (assuming univalence).

Lens↔Traditional-lens :
  {A : Type a} {B : Type b} →
  Block "conversion" →
  Univalence (a ⊔ b) →
  Is-set A →
  Lens A B ↔ Traditional.Lens A B
Lens↔Traditional-lens {A = A} {B} bc univ A-set =
  Lens A B              ↔⟨ Lens≃Higher-lens bc univ ⟩
  Higher.Lens A B       ↝⟨ Higher.Lens↔Traditional-lens bc univ A-set ⟩□
  Traditional.Lens A B  □

-- The isomorphism preserves getters and setters.

Lens↔Traditional-lens-preserves-getters-and-setters :
  {A : Type a} {B : Type b}
  (bc : Block "conversion")
  (univ : Univalence (a ⊔ b))
  (s : Is-set A) →
  Preserves-getters-and-setters-⇔ A B
    (_↔_.logical-equivalence (Lens↔Traditional-lens bc univ s))
Lens↔Traditional-lens-preserves-getters-and-setters bc univ s =
  Preserves-getters-and-setters-⇔-∘
    {f = _↔_.logical-equivalence $
           Higher.Lens↔Traditional-lens bc univ s}
    {g = _≃_.logical-equivalence $ Lens≃Higher-lens bc univ}
    (Higher.Lens↔Traditional-lens-preserves-getters-and-setters
       bc univ s)
    (Lens≃Higher-lens-preserves-getters-and-setters bc univ)

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
open import Common.Equality
open import Common.Prelude hiding (pred)

pred : Nat → Nat
pred = _∸ 1

T : Bool → Set
T = if_then ⊤ else ⊥

if : {A : Set} (b : Bool) → A → A → A
if b = if b then_else_

test₁ : Nat → Nat
test₁ = 5 +_

test₁-test : ∀ x → test₁ x ≡ 5 + x
test₁-test _ = refl

test₂ : Nat → Nat
test₂ = _* 5

test₂-test : ∀ x → test₂ x ≡ x * 5
test₂-test _ = refl

infixr 9 _∘_

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

test₃ : Nat → Nat
test₃ = (_* 5) ∘ (6 +_) ∘ (2 ∸_)

test₃-test : ∀ x → test₃ x ≡ (6 + (2 ∸ x)) * 5
test₃-test _ = refl

infixr 0 _⊚_

_⊚_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
f ⊚ g = λ x → f (g x)

test₃½ : Nat → Nat
test₃½ = _* 5 ⊚ 6 +_ ⊚ 2 ∸_

test₃½-test : ∀ x → test₃½ x ≡ (6 + (2 ∸ x)) * 5
test₃½-test _ = refl

test₄ : Nat → Nat → Nat
test₄ = Common.Prelude.if true then_else_

test₄-test : ∀ x y → test₄ x y ≡ x
test₄-test _ _ = refl

test₅ : Bool → Nat
test₅ = if_then 2 else 3

test₅-test : ∀ x → test₅ x ≡ (if x then 2 else 3)
test₅-test _ = refl

postulate
  foo_bar_ : (b₁ b₂ : Bool) → if b₁ then Nat else if b₂ then Bool else Nat

test₆ : (b : Bool) → if b then Bool else Nat
test₆ = foo false bar_

test₆-test : ∀ x → test₆ x ≡ (foo false bar x)
test₆-test _ = refl

test₇ : Nat → Nat
test₇ = (Common.Prelude._+ 2) ∘ (1 Common.Prelude.∸_)

test₇-test : ∀ x → test₇ x ≡ (1 Common.Prelude.∸ x) Common.Prelude.+ 2
test₇-test _ = refl

_test₈_ : Nat → Nat → Nat
_test₈_ = _*_

test₈-test : ∀ x y → (x test₈ y) ≡ x * y
test₈-test _ _ = refl

test₉ : Nat → Nat → Nat
test₉ = Common.Prelude._*_

test₉-test : ∀ x y → test₉ x y ≡ x Common.Prelude.* y
test₉-test _ _ = refl

data D : Set₂ where
  ⟨_⟩_ : Set → Set₁ → D

Test₁₀ : D → Set
Test₁₀ (⟨_⟩_ X _) = X

Test₁₁ : Set → Set
Test₁₁ ⟨_⟩ = ⟨_⟩

postulate
  ⟦_⟧ : Set → Set

Test₁₂ : Set → Set
Test₁₂ A = ⟦_⟧ A

Test₁₂-test : ∀ X → Test₁₂ X ≡ ⟦ X ⟧
Test₁₂-test _ = refl

module M where

  _! : Set₁ → Set₁
  X ! = X

Test₁₃ : Set₁
Test₁₃ = M._! Set

Test₁₄ : (x : Nat → Nat) → x ≡ suc → Set₁
Test₁₄ .(1 +_) refl = Set

_$_ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → A → B
f $ x = f x

test₁₅ : (((⊤ → Bool) → Bool) → Nat) → Nat
test₁₅ = _$ _$ _

postulate
  -_  : Nat → Nat
  _-_ : Nat → Nat → Nat

test₁₆ : Nat → Nat
test₁₆ = (-_)

test₁₆-test : ∀ x → test₁₆ x ≡ (- x)
test₁₆-test _ = refl

test₁₇ : (f : Nat → Nat) → f ≡ suc → Set₁
test₁₇ .(1 +_) refl = Set

test₁₈ : (section : Nat) → section +_ ≡ λ x → section + x
test₁₈ section = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Directed acyclic multigraphs
------------------------------------------------------------------------

-- A representation of DAGs, based on the idea underlying Martin
-- Erwig's FGL. Note that this representation does not aim to be
-- efficient.

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

module Data.Graph.Acyclic where

open import Level using (_⊔_)
open import Data.Nat.Base as Nat using (ℕ; zero; suc; _<′_)
import Data.Nat.Properties as Nat
open import Data.Fin as Fin
  using (Fin; Fin′; zero; suc; #_; toℕ; _≟_) renaming (_ℕ-ℕ_ to _-_)
import Data.Fin.Properties as FP
import Data.Fin.Permutation.Components as PC
open import Data.Product as Prod using (∃; _×_; _,_)
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Empty
open import Data.Unit.Base using (⊤; tt)
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Data.List.Base as List using (List; []; _∷_)
open import Function
open import Induction.Nat using (<′-rec; <′-Rec)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- A lemma

private

  lemma : ∀ n (i : Fin n) → n - suc i <′ n
  lemma zero    ()
  lemma (suc n) i  = Nat.≤⇒≤′ $ Nat.s≤s $ FP.nℕ-ℕi≤n n i

------------------------------------------------------------------------
-- Node contexts

record Context {ℓ e} (Node : Set ℓ) (Edge : Set e) (n : ℕ) : Set (ℓ ⊔ e) where
  constructor context
  field
    label      : Node
    successors : List (Edge × Fin n)

open Context public

-- Map for contexts.

module _ {ℓ₁ e₁} {N₁ : Set ℓ₁} {E₁ : Set e₁}
         {ℓ₂ e₂} {N₂ : Set ℓ₂} {E₂ : Set e₂} where

  cmap : ∀ {n} → (N₁ → N₂) → (List (E₁ × Fin n) → List (E₂ × Fin n)) →
         Context N₁ E₁ n → Context N₂ E₂ n
  cmap f g c = context (f (label c)) (g (successors c))

------------------------------------------------------------------------
-- Graphs

infixr 3 _&_

-- The DAGs are indexed on the number of nodes.

data Graph {ℓ e} (Node : Set ℓ) (Edge : Set e) : ℕ → Set (ℓ ⊔ e) where
  ∅   : Graph Node Edge 0
  _&_ : ∀ {n} (c : Context Node Edge n) (g : Graph Node Edge n) →
        Graph Node Edge (suc n)

private

  example : Graph ℕ ℕ 5
  example = context 0 [] &
            context 1 ((10 , # 1) ∷ (11 , # 1) ∷ []) &
            context 2 ((12 , # 0) ∷ []) &
            context 3 [] &
            context 4 [] &
            ∅

------------------------------------------------------------------------
-- Higher-order functions

module _ {ℓ e} {N : Set ℓ} {E : Set e} {t} where

-- "Fold right".

  foldr : (T : ℕ → Set t) →
          (∀ {n} → Context N E n → T n → T (suc n)) →
          T 0 →
          ∀ {m} → Graph N E m → T m
  foldr T _∙_ x ∅       = x
  foldr T _∙_ x (c & g) = c ∙ foldr T _∙_ x g

-- "Fold left".

  foldl : ∀ {n} (T : ℕ → Set t) →
          ((i : Fin n) → T (toℕ i) → Context N E (n - suc i) →
          T (suc (toℕ i))) →
          T 0 →
          Graph N E n → T n
  foldl T f x ∅       = x
  foldl T f x (c & g) = foldl (T ∘′ suc) (f ∘ suc) (f zero x c) g

module _ {ℓ₁ e₁} {N₁ : Set ℓ₁} {E₁ : Set e₁}
         {ℓ₂ e₂} {N₂ : Set ℓ₂} {E₂ : Set e₂} where

-- Maps over node contexts.

  map : (∀ {n} → Context N₁ E₁ n → Context N₂ E₂ n) →
        ∀ {n} → Graph N₁ E₁ n → Graph N₂ E₂ n
  map f = foldr _ (λ c → f c &_) ∅

-- Maps over node labels.

nmap : ∀ {ℓ₁ ℓ₂ e} {N₁ : Set ℓ₁} {N₂ : Set ℓ₂} {E : Set e} →
       ∀ {n} → (N₁ → N₂) → Graph N₁ E n → Graph N₂ E n
nmap f = map (cmap f id)

-- Maps over edge labels.

emap : ∀ {ℓ e₁ e₂} {N : Set ℓ} {E₁ : Set e₁} {E₂ : Set e₂} →
       ∀ {n} → (E₁ → E₂) → Graph N E₁ n → Graph N E₂ n
emap f = map (cmap id (List.map (Prod.map f id)))

-- Zips two graphs with the same number of nodes. Note that one of the
-- graphs has a type which restricts it to be completely disconnected.

zipWith : ∀ {ℓ₁ ℓ₂ ℓ e} {N₁ : Set ℓ₁} {N₂ : Set ℓ₂} {N : Set ℓ} {E : Set e} →
          ∀ {n} → (N₁ → N₂ → N) → Graph N₁ ⊥ n → Graph N₂ E n → Graph N E n
zipWith _∙_ ∅         ∅         = ∅
zipWith _∙_ (c₁ & g₁) (c₂ & g₂) =
  context (label c₁ ∙ label c₂) (successors c₂) & zipWith _∙_ g₁ g₂

------------------------------------------------------------------------
-- Specific graphs

-- A completeley disconnected graph.

disconnected : ∀ n → Graph ⊤ ⊥ n
disconnected zero    = ∅
disconnected (suc n) = context tt [] & disconnected n

-- A complete graph.

complete : ∀ n → Graph ⊤ ⊤ n
complete zero    = ∅
complete (suc n) =
  context tt (List.map (tt ,_) $ Vec.toList (Vec.allFin n)) &
  complete n

------------------------------------------------------------------------
-- Queries

module _ {ℓ e} {N : Set ℓ} {E : Set e} where

-- The top-most context.

  head : ∀ {n} → Graph N E (suc n) → Context N E n
  head (c & g) = c

-- The remaining graph.

  tail : ∀ {n} → Graph N E (suc n) → Graph N E n
  tail (c & g) = g

-- Finds the context and remaining graph corresponding to a given node
-- index.

  _[_] : ∀ {n} → Graph N E n → (i : Fin n) → Graph N E (suc (n - suc i))
  ∅       [ () ]
  (c & g) [ zero ]  = c & g
  (c & g) [ suc i ] = g [ i ]

-- The nodes of the graph (node number relative to "topmost" node ×
-- node label).

  nodes : ∀ {n} → Graph N E n → Vec (Fin n × N) n
  nodes = Vec.zip (Vec.allFin _) ∘
          foldr (Vec N) (λ c → label c ∷_) []

private

  test-nodes : nodes example ≡ (# 0 , 0) ∷ (# 1 , 1) ∷ (# 2 , 2) ∷
                               (# 3 , 3) ∷ (# 4 , 4) ∷ []
  test-nodes = P.refl

module _ {ℓ e} {N : Set ℓ} {E : Set e} where

-- Topological sort. Gives a vector where earlier nodes are never
-- successors of later nodes.

  topSort : ∀ {n} → Graph N E n → Vec (Fin n × N) n
  topSort = nodes

-- The edges of the graph (predecessor × edge label × successor).
--
-- The predecessor is a node number relative to the "topmost" node in
-- the graph, and the successor is a node number relative to the
-- predecessor.

  edges : ∀ {n} → Graph N E n → List (∃ λ i → E × Fin (n - suc i))
  edges {n} =
    foldl (λ _ → List (∃ λ i → E × Fin (n - suc i)))
          (λ i es c → es List.++ List.map (i ,_) (successors c))
          []

private

  test-edges : edges example ≡ (# 1 , 10 , # 1) ∷ (# 1 , 11 , # 1) ∷
                               (# 2 , 12 , # 0) ∷ []
  test-edges = P.refl

-- The successors of a given node i (edge label × node number relative
-- to i).

sucs : ∀ {ℓ e} {N : Set ℓ} {E : Set e} →
       ∀ {n} → Graph N E n → (i : Fin n) → List (E × Fin (n - suc i))
sucs g i = successors $ head (g [ i ])

private

  test-sucs : sucs example (# 1) ≡ (10 , # 1) ∷ (11 , # 1) ∷ []
  test-sucs = P.refl

-- The predecessors of a given node i (node number relative to i ×
-- edge label).

preds : ∀ {ℓ e} {N : Set ℓ} {E : Set e} →
        ∀ {n} → Graph N E n → (i : Fin n) → List (Fin′ i × E)
preds g       zero    = []
preds (c & g) (suc i) =
  List._++_ (List.mapMaybe (p i) $ successors c)
            (List.map (Prod.map suc id) $ preds g i)
  where
  p : ∀ {e} {E : Set e} {n} (i : Fin n) → E × Fin n → Maybe (Fin′ (suc i) × E)
  p i (e , j)  with i ≟ j
  p i (e , .i) | yes P.refl = just (zero , e)
  p i (e , j)  | no _       = nothing

private

  test-preds : preds example (# 3) ≡
               (# 1 , 10) ∷ (# 1 , 11) ∷ (# 2 , 12) ∷ []
  test-preds = P.refl

------------------------------------------------------------------------
-- Operations

-- Weakens a node label.

weaken : ∀ {n} {i : Fin n} → Fin (n - suc i) → Fin n
weaken {n} {i} j = Fin.inject≤ j (FP.nℕ-ℕi≤n n (suc i))

-- Labels each node with its node number.

number : ∀ {ℓ e} {N : Set ℓ} {E : Set e} →
         ∀ {n} → Graph N E n → Graph (Fin n × N) E n
number {N = N} {E} =
  foldr (λ n → Graph (Fin n × N) E n)
        (λ c g → cmap (zero ,_) id c & nmap (Prod.map suc id) g)
        ∅

private

  test-number : number example ≡
                (context (# 0 , 0) [] &
                 context (# 1 , 1) ((10 , # 1) ∷ (11 , # 1) ∷ []) &
                 context (# 2 , 2) ((12 , # 0) ∷ []) &
                 context (# 3 , 3) [] &
                 context (# 4 , 4) [] &
                 ∅)
  test-number = P.refl

-- Reverses all the edges in the graph.

reverse : ∀ {ℓ e} {N : Set ℓ} {E : Set e} →
          ∀ {n} → Graph N E n → Graph N E n
reverse {N = N} {E} g =
  foldl (Graph N E)
        (λ i g' c →
           context (label c)
                   (List.map (Prod.swap ∘ Prod.map PC.reverse id) $
                             preds g i)
           & g')
        ∅ g

private

  test-reverse : reverse (reverse example) ≡ example
  test-reverse = P.refl

------------------------------------------------------------------------
-- Views

-- Expands the subgraph induced by a given node into a tree (thus
-- losing all sharing).

data Tree {ℓ e} (N : Set ℓ) (E : Set e) : Set (ℓ ⊔ e) where
  node : (label : N) (successors : List (E × Tree N E)) → Tree N E

module _ {ℓ e} {N : Set ℓ} {E : Set e} where

  toTree : ∀ {n} → Graph N E n → Fin n → Tree N E
  toTree g i = <′-rec Pred expand _ (g [ i ])
    where
    Pred = λ n → Graph N E (suc n) → Tree N E

    expand : (n : ℕ) → <′-Rec Pred n → Pred n
    expand n rec (c & g) =
      node (label c)
           (List.map
              (Prod.map id (λ i → rec (n - suc i) (lemma n i) (g [ i ])))
              (successors c))

-- Performs the toTree expansion once for each node.

  toForest : ∀ {n} → Graph N E n → Vec (Tree N E) n
  toForest g = Vec.map (toTree g) (Vec.allFin _)

private

  test-toForest : toForest example ≡
                    let n3 = node 3 [] in
                    node 0 [] ∷
                    node 1 ((10 , n3) ∷ (11 , n3) ∷ []) ∷
                    node 2 ((12 , n3) ∷ []) ∷
                    node 3 [] ∷
                    node 4 [] ∷
                    []
  test-toForest = P.refl


text:
import cedille-options

module interactive-cmds (options : cedille-options.options) where

open import lib
open import functions
open import cedille-types
open import conversion
open import ctxt
open import general-util
open import monad-instances
open import spans options {id}
open import subst
open import syntax-util
open import to-string options
open import toplevel-state options {IO}
open import untyped-spans options {IO}
open import parser
open import rewriting
open import rename
open import classify options {id}
import spans options {IO} as io-spans
open import elaboration (record options {during-elaboration = ff})
open import elaboration-helpers (record options {during-elaboration = ff})
open import templates

private

  {- Parsing -}

  ll-ind : ∀ {X : language-level → Set} → X ll-term → X ll-type → X ll-kind →
             (ll : language-level) → X ll
  ll-ind t T k ll-term = t
  ll-ind t T k ll-type = T
  ll-ind t T k ll-kind = k

  ll-lift : language-level → Set
  ll-lift = ⟦_⟧ ∘ ll-ind TERM TYPE KIND

  ll-ind' : ∀ {X : Σ language-level ll-lift → Set} → (s : Σ language-level ll-lift) → ((t : term) → X (ll-term , t)) → ((T : type) → X (ll-type , T)) → ((k : kind) → X (ll-kind , k)) → X s
  ll-ind' (ll-term , t) tf Tf kf = tf t
  ll-ind' (ll-type , T) tf Tf kf = Tf T
  ll-ind' (ll-kind , k) tf Tf kf = kf k

  ll-disambiguate : ctxt → term → maybe type
  ll-disambiguate Γ (Var pi x) = ctxt-lookup-type-var Γ x ≫=maybe λ _ → just (TpVar pi x)
  ll-disambiguate Γ (App t NotErased t') = ll-disambiguate Γ t ≫=maybe λ T →
    just (TpAppt T t')
  ll-disambiguate Γ (AppTp t T') = ll-disambiguate Γ t ≫=maybe λ T → just (TpApp T T')
  ll-disambiguate Γ (Lam pi KeptLambda pi' x (SomeClass atk) t) =
    ll-disambiguate (ctxt-tk-decl pi' x atk Γ) t ≫=maybe λ T →
    just (TpLambda pi pi' x atk T)
  ll-disambiguate Γ (Parens pi t pi') = ll-disambiguate Γ t
  ll-disambiguate Γ (Let pi d t) =
    ll-disambiguate (Γ' d) t ≫=maybe λ T → just (TpLet pi d T)
    where
    Γ' : defTermOrType → ctxt
    Γ' (DefTerm pi' x (SomeType T) t) = ctxt-term-def pi' localScope OpacTrans x t T Γ
    Γ' (DefTerm pi' x NoType t) = ctxt-term-udef pi' localScope OpacTrans x t Γ
    Γ' (DefType pi' x k T) = ctxt-type-def pi' localScope OpacTrans x T k Γ
  ll-disambiguate Γ t = nothing

  parse-string : (ll : language-level) → string → maybe (ll-lift ll)
  parse-string ll s = case ll-ind {λ ll → string → Either string (ll-lift ll)}
    parseTerm parseType parseKind ll s of λ {(Left e) → nothing; (Right e) → just e}

  ttk = "term, type, or kind"

  parse-err-msg : (failed-to-parse : string) → (as-a : string) → string
  parse-err-msg failed-to-parse "" =
    "Failed to parse \\\\\"" ^ failed-to-parse ^ "\\\\\""
  parse-err-msg failed-to-parse as-a =
    "Failed to parse \\\\\"" ^ failed-to-parse ^ "\\\\\" as a " ^ as-a

  infixr 7 _≫nothing_ _-_!_≫parse_ _!_≫error_
  _≫nothing_ : ∀{ℓ}{A : Set ℓ} → maybe A → maybe A → maybe A
  (nothing ≫nothing m₂) = m₂
  (m₁ ≫nothing m₂) = m₁

  _-_!_≫parse_ : ∀{A B : Set} → (string → maybe A) → string →
                  (error-msg : string) → (A → string ⊎ B) → string ⊎ B
  (f - s ! e ≫parse f') = maybe-else (inj₁ (parse-err-msg s e)) f' (f s)

  _!_≫error_ : ∀{E A B : Set} → maybe A → E → (A → E ⊎ B) → E ⊎ B
  (just a ! e ≫error f) = f a
  (nothing ! e ≫error f) = inj₁ e

  parse-try : ∀ {X : Set} → ctxt → string → maybe
                (((ll : language-level) → ll-lift ll → X) → X)
  parse-try Γ s =
    maybe-map (λ t f → maybe-else (f ll-term t) (f ll-type) (ll-disambiguate Γ t))
      (parse-string ll-term s) ≫nothing
    maybe-map (λ T f → f ll-type T) (parse-string ll-type s) ≫nothing
    maybe-map (λ k f → f ll-kind k) (parse-string ll-kind s)

  string-to-𝔹 : string → maybe 𝔹
  string-to-𝔹 "tt" = just tt
  string-to-𝔹 "ff" = just ff
  string-to-𝔹 _ = nothing

  parse-ll : string → maybe language-level
  parse-ll "term" = just ll-term
  parse-ll "type" = just ll-type
  parse-ll "kind" = just ll-kind
  parse-ll _ = nothing

  {- Local Context -}

  record lci : Set where
    constructor mk-lci
    field ll : string; x : var; t : string; T : string; fn : string; pi : posinfo

  merge-lcis-ctxt : ctxt → 𝕃 string → ctxt
  merge-lcis-ctxt c = foldr merge-lci-ctxt c ∘ (sort-lcis ∘ strings-to-lcis) where
    strings-to-lcis : 𝕃 string → 𝕃 lci
    strings-to-lcis ss = strings-to-lcis-h ss [] where
      strings-to-lcis-h : 𝕃 string → 𝕃 lci → 𝕃 lci
      strings-to-lcis-h (ll :: x :: t :: T :: fn :: pi :: tl) items =
        strings-to-lcis-h tl (mk-lci ll x t T fn pi :: items)
      strings-to-lcis-h _ items = items

    language-level-type-of : language-level → language-level
    language-level-type-of ll-term = ll-type
    language-level-type-of _ = ll-kind

    merge-lci-ctxt : lci → ctxt → ctxt
    merge-lci-ctxt (mk-lci ll v t T fn pi) Γ =
      maybe-else Γ (λ Γ → Γ) (parse-ll ll ≫=maybe λ ll →
        parse-string (language-level-type-of ll) T ≫=maybe h ll (parse-string ll t)) where
      h : (ll : language-level) → maybe (ll-lift ll) →
          ll-lift (language-level-type-of ll) → maybe ctxt
      h ll-term (just t) T =
        just (ctxt-term-def pi localScope OpacTrans v t (qualif-type Γ T) Γ)
      h ll-type (just T) k =
        just (ctxt-type-def pi localScope OpacTrans v T (qualif-kind Γ k) Γ)
      h ll-term nothing T = just (ctxt-term-decl pi v T Γ)
      h ll-type nothing k = just (ctxt-type-decl pi v k Γ)
      h _ _ _ = nothing

    sort-lcis : 𝕃 lci → 𝕃 lci
    sort-lcis = list-merge-sort.merge-sort lci λ l l' →
                posinfo-to-ℕ (lci.pi l) > posinfo-to-ℕ (lci.pi l')
      where import list-merge-sort

  get-local-ctxt : ctxt → (pos : ℕ) → (local-ctxt : 𝕃 string) → ctxt
  get-local-ctxt Γ @ (mk-ctxt (fn , mn , _) _ is _ _) pi =
    merge-lcis-ctxt (foldr (flip ctxt-clear-symbol ∘ fst) Γ
      (flip filter (trie-mappings is) λ {(x , ci , fn' , pi') →
        fn =string fn' && posinfo-to-ℕ pi' > pi}))

  {- Helpers -}

  qualif-ed : ∀ {ed : exprd} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧
  qualif-ed{TERM} = qualif-term
  qualif-ed{TYPE} = qualif-type
  qualif-ed{KIND} = qualif-kind
  qualif-ed Γ e = e

  step-reduce : ∀ {ed : exprd} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧
  step-reduce Γ t = let t' = erase t in maybe-else t' id (step-reduceh Γ t') where
    step-reduceh : ∀ {ed : exprd} → ctxt → ⟦ ed ⟧ → maybe ⟦ ed ⟧
    step-reduceh{TERM} Γ (Var pi x) = ctxt-lookup-term-var-def Γ (qualif-var Γ x)
    step-reduceh{TYPE} Γ (TpVar pi x) = ctxt-lookup-type-var-def Γ (qualif-var Γ x)
    step-reduceh{TERM} Γ (App (Lam pi b pi' x oc t) me t') = just (subst Γ t' x t)
    step-reduceh{TYPE} Γ (TpApp (TpLambda pi pi' x (Tkk _) T) T') = just (subst Γ T' x T)
    step-reduceh{TYPE} Γ (TpAppt (TpLambda pi pi' x (Tkt _) T) t) = just (subst Γ t x T)
    step-reduceh{TERM} Γ (App t me t') = step-reduceh Γ t ≫=maybe λ t → just (App t me t')
    step-reduceh{TYPE} Γ (TpApp T T') = step-reduceh Γ T ≫=maybe λ T → just (TpApp T T')
    step-reduceh{TYPE} Γ (TpAppt T t) = step-reduceh Γ T ≫=maybe λ T → just (TpAppt T t)
    step-reduceh{TERM} Γ (Lam pi b pi' x oc t) = step-reduceh (ctxt-var-decl x Γ) t ≫=maybe λ t → just (Lam pi b pi' x oc t)
    step-reduceh{TYPE} Γ (TpLambda pi pi' x atk T) = step-reduceh (ctxt-var-decl x Γ) T ≫=maybe λ T → just (TpLambda pi pi' x atk T)
    step-reduceh{TERM} Γ (Let pi (DefTerm pi' x ot t') t) = just (subst Γ t' x t)
    step-reduceh{TYPE} Γ (TpLet pi (DefTerm pi' x ot t) T) = just (subst Γ t x T)
    step-reduceh{TYPE} Γ (TpLet pi (DefType pi' x k T') T) = just (subst Γ T' x T)
    step-reduceh Γ t = nothing

  parse-norm : string → maybe (∀ {ed : exprd} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧)
  parse-norm "all" = just λ Γ t → hnf Γ unfold-all t tt
  parse-norm "head" = just λ Γ t → hnf Γ unfold-head t tt
  parse-norm "once" = just λ Γ → step-reduce Γ ∘ erase
  parse-norm _ = nothing

  {- Command Executors -}

  normalize-cmd : ctxt → (str ll pi norm : string) → 𝕃 string → string ⊎ tagged-val
  normalize-cmd Γ str ll pi norm ls =
    parse-ll - ll ! "language-level" ≫parse λ ll' →
    string-to-ℕ - pi ! "natural number" ≫parse λ sp →
    parse-norm - norm ! "normalization method (all, head, once)" ≫parse λ norm →
    parse-string ll' - str ! ll ≫parse λ t →
      let Γ' = get-local-ctxt Γ sp ls in
    inj₂ (to-string-tag "" Γ' (norm Γ' (qualif-ed Γ' t)))

  normalize-prompt : ctxt → (str norm : string) → 𝕃 string → string ⊎ tagged-val
  normalize-prompt Γ str norm ls =
    parse-norm - norm ! "normalization method (all, head, once)" ≫parse λ norm →
    let Γ' = merge-lcis-ctxt Γ ls in
    parse-try Γ' - str ! ttk ≫parse λ f → f λ ll t →
    inj₂ (to-string-tag "" Γ' (norm Γ' (qualif-ed Γ' t)))

  erase-cmd : ctxt → (str ll pi : string) → 𝕃 string → string ⊎ tagged-val
  erase-cmd Γ str ll pi ls =
    parse-ll - ll ! "language-level" ≫parse λ ll' →
    string-to-ℕ - pi ! "natural number" ≫parse λ sp →
    parse-string ll' - str ! ll ≫parse λ t →
    let Γ' = get-local-ctxt Γ sp ls in
    inj₂ (to-string-tag "" Γ' (erase (qualif-ed Γ' t)))

  erase-prompt : ctxt → (str : string) → 𝕃 string → string ⊎ tagged-val
  erase-prompt Γ str ls =
    let Γ' = merge-lcis-ctxt Γ ls in
    parse-try Γ' - str ! ttk ≫parse λ f → f λ ll t →
    inj₂ (to-string-tag "" Γ' (erase (qualif-ed Γ' t)))

  private
    cmds-to-escaped-string : cmds → strM
    cmds-to-escaped-string (CmdsNext c cs) = cmd-to-string c $ strAdd "\\n\\n" ≫str cmds-to-escaped-string cs
    cmds-to-escaped-string CmdsStart = strEmpty

  data-cmd : ctxt → (encoding name ps is cs : string) → string ⊎ tagged-val
  data-cmd Γ encodingₛ x psₛ isₛ csₛ =
    string-to-𝔹 - encodingₛ ! "boolean" ≫parse λ encoding →
    parse-string ll-kind - psₛ ! "kind" ≫parse λ psₖ →
    parse-string ll-kind - isₛ ! "kind" ≫parse λ isₖ →
    parse-string ll-kind - csₛ ! "kind" ≫parse λ csₖ →
    let ps = map (λ {(Index x atk) → Decl posinfo-gen posinfo-gen Erased x atk posinfo-gen}) $ kind-to-indices Γ psₖ
        cs = map (λ {(Index x (Tkt T)) → Ctr x T; (Index x (Tkk k)) → Ctr x $ mtpvar "ErrorExpectedTypeNotKind"}) $ kind-to-indices empty-ctxt csₖ
        is = kind-to-indices (add-constructors-to-ctxt cs $ add-parameters-to-ctxt ps $ Γ) isₖ
        picked-encoding = if encoding then mendler-encoding else mendler-simple-encoding
        defs = datatype-encoding.mk-defs picked-encoding Γ $ Data x ps is cs in
    inj₂ $ strRunTag "" Γ $ cmds-to-escaped-string $ fst defs

  br-cmd : ctxt → (str qed : string) → 𝕃 string → IO ⊤
  br-cmd Γ str qed ls =
    let Γ' = merge-lcis-ctxt Γ ls in
    maybe-else
      (return (io-spans.spans-to-rope (io-spans.global-error "Parse error" nothing)))
      (λ s → s >>= return ∘ io-spans.spans-to-rope)
      (parse-try {maybe (IO io-spans.spans)} Γ' str ≫=maybe λ f → f λ where
         ll-term t → just (untyped-term-spans t Γ' io-spans.empty-spans >>= return ∘ (snd ∘ snd))
         ll-type T →
           parse-string ll-term qed ≫=maybe λ q →
           case check-term q (just $ qualif-type Γ' T) Γ' empty-spans of λ where
             (triv , _ , ss @ (regular-spans nothing _)) →
               just (putStrLn "inhabited: Type inhabited" >> untyped-type-spans T Γ' io-spans.empty-spans >>= return ∘ (snd ∘ snd))
             (triv , _ , _) →
               just (untyped-type-spans T Γ' io-spans.empty-spans >>= return ∘ (snd ∘ snd))
         ll-kind k →
           just (untyped-kind-spans k Γ' io-spans.empty-spans >>= return ∘ (snd ∘ snd)))
      >>= putRopeLn

  conv-cmd : ctxt → (ll str1 str2 : string) → 𝕃 string → string ⊎ tagged-val
  conv-cmd Γ ll s1 s2 ls =
    parse-ll - ll ! "language-level" ≫parse λ ll' →
    parse-string ll' - s1 ! ll ≫parse λ t1 →
    parse-string ll' - s2 ! ll ≫parse λ t2 →
    let Γ' = merge-lcis-ctxt Γ ls; t2 = erase (qualif-ed Γ' t2) in
    if ll-ind {λ ll → ctxt → ll-lift ll → ll-lift ll → 𝔹}
         conv-term conv-type conv-kind ll' Γ' (qualif-ed Γ' t1) t2
      then inj₂ (to-string-tag "" Γ' t2)
      else inj₁ "Inconvertible"

  rewrite-cmd : ctxt → (span-str : string) → (input-str : string) →
                (use-hnf : string) → (local-ctxt : 𝕃 string) → string ⊎ tagged-val
  rewrite-cmd Γ ss is hd ls =
    string-to-𝔹 - hd ! "boolean" ≫parse λ use-hnf →
    let Γ = merge-lcis-ctxt Γ ls in
    parse-try Γ - ss ! ttk ≫parse λ f → f λ ll ss →
    parse-try Γ - is ! ttk ≫parse λ f → (f λ where
      ll-term t → (case check-term t nothing Γ empty-spans of λ
          {(just T , _ , regular-spans nothing _) → just T; _ → nothing})
        ! "Error when synthesizing a type for the input term" ≫error λ where
          (TpEq _ t₁ t₂ _) → inj₂ (t₁ , t₂)
          _ → inj₁ "Synthesized a non-equational type from the input term"
      ll-type (TpEq _ t₁ t₂ _) → inj₂ (t₁ , t₂)
      ll-type _ → inj₁ "Expected the input expression to be a term, but got a type"
      ll-kind _ → inj₁ "Expected the input expression to be a term, but got a kind")
    ≫=⊎ uncurry λ t₁ t₂ →
    let x = fresh-var "x" (ctxt-binds-var Γ) empty-renamectxt
        f = ll-ind {λ ll → ctxt → term → var → ll-lift ll → ll-lift ll}
              subst subst subst ll Γ t₂ x in
    case (ll-ind {λ ll → ll-lift ll → ctxt → 𝔹 → maybe stringset →
                         term → term → var → ℕ → ll-lift ll × ℕ × ℕ}
      rewrite-term rewrite-type rewrite-kind ll (qualif-ed Γ ss) Γ
      use-hnf nothing (Beta posinfo-gen NoTerm NoTerm) t₁ x 0) of λ where
        (e , 0 , _) → inj₁ "No rewrites could be performed"
        (e , _ , _) → inj₂ (strRunTag "" Γ
          (to-stringh (erase (f e)) ≫str strAdd "§" ≫str strAdd x ≫str strAdd "§" ≫str to-stringh (erase e)))

  {- Commands -}

  tv-to-rope : string ⊎ tagged-val → rope
  tv-to-rope (inj₁ s) = [[ "{\"error\":\"" ]] ⊹⊹ [[ s ]] ⊹⊹ [[ "\"}" ]]
  tv-to-rope (inj₂ (_ , v , ts)) =
    [[ "{" ]] ⊹⊹ tagged-val-to-rope 0 ("value" , v , ts) ⊹⊹ [[ "}" ]]

  interactive-cmd-h : ctxt → 𝕃 string → string ⊎ tagged-val
  interactive-cmd-h Γ ("normalize" :: input :: ll :: sp :: norm :: lc) =
    normalize-cmd Γ input ll sp norm lc
  interactive-cmd-h Γ ("erase" :: input :: ll :: sp :: lc) =
    erase-cmd Γ input ll sp lc
  interactive-cmd-h Γ ("normalizePrompt" :: input :: norm :: lc) =
    normalize-prompt Γ input norm lc
  interactive-cmd-h Γ ("erasePrompt" :: input :: lc) =
    erase-prompt Γ input lc
  interactive-cmd-h Γ ("conv" :: ll :: ss :: is :: lc) =
    conv-cmd Γ ll ss is lc
  interactive-cmd-h Γ ("rewrite" :: ss :: is :: head :: lc) =
    rewrite-cmd Γ ss is head lc
  interactive-cmd-h Γ ("data" :: encoding :: x :: ps :: is :: cs :: []) =
    data-cmd Γ encoding x ps is cs
  interactive-cmd-h Γ cs =
    inj₁ ("Unknown interactive cmd: " ^ 𝕃-to-string (λ s → s) ", " cs)

interactive-cmd : 𝕃 string → toplevel-state → IO ⊤
interactive-cmd ("br" :: input :: qed :: lc) ts = br-cmd (toplevel-state.Γ ts) input qed lc
interactive-cmd ls ts = putRopeLn (tv-to-rope (interactive-cmd-h (toplevel-state.Γ ts) ls))

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
open import Agda.Primitive
open import Categories.Category

module SecondOrder.IndexedCategory where

  IndexedCategory : ∀ {i o l e} (I : Set i) (𝒞 : Category o l e) → Category (i ⊔ o) (i ⊔ l) (i ⊔ e)
  IndexedCategory I 𝒞 =
    let open Category 𝒞 in
    record
      { Obj = I → Obj
      ; _⇒_ = λ A B → ∀ i → A i ⇒ B i
      ; _≈_ = λ f g → ∀ i → f i ≈ g i
      ; id = λ i → id
      ; _∘_ = λ f g i → f i ∘ g i
      ; assoc = λ i → assoc
      ; sym-assoc = λ i → sym-assoc
      ; identityˡ = λ i → identityˡ
      ; identityʳ = λ i → identityʳ
      ; identity² = λ i → identity²
      ; equiv = record { refl = λ i → Equiv.refl
                       ; sym = λ ξ i → Equiv.sym (ξ i) ; trans = λ ζ ξ i → Equiv.trans (ζ i) (ξ i) }
      ; ∘-resp-≈ = λ ζ ξ i → ∘-resp-≈ (ζ i) (ξ i)
      }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed applicative functors
------------------------------------------------------------------------

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

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

module Category.Applicative.Indexed where

open import Category.Functor using (RawFunctor)
open import Data.Product using (_×_; _,_)
open import Function
open import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)

IFun : ∀ {i} → Set i → (ℓ : Level) → Set _
IFun I ℓ = I → I → Set ℓ → Set ℓ

------------------------------------------------------------------------
-- Type, and usual combinators

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

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

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

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

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

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

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

  zipWith : ∀ {i j k A B C} → (A → B → C) → F i j A → F j k B → F i k C
  zipWith f x y = f <$> x ⊛ y

  zip : ∀ {i j k A B} → F i j A → F j k B → F i k (A × B)
  zip = zipWith _,_

------------------------------------------------------------------------
-- Applicative with a zero

record RawIApplicativeZero
       {i f} {I : Set i} (F : IFun I f) :
       Set (i ⊔ suc f) where
  field
    applicative : RawIApplicative F
    ∅           : ∀ {i j A} → F i j A

  open RawIApplicative applicative public

------------------------------------------------------------------------
-- Alternative functors: `F i j A` is a monoid

record RawIAlternative
       {i f} {I : Set i} (F : IFun I f) :
       Set (i ⊔ suc f) where
  infixr 3 _∣_
  field
    applicativeZero : RawIApplicativeZero F
    _∣_             : ∀ {i j A} → F i j A → F i j A → F i j A

  open RawIApplicativeZero applicativeZero public

------------------------------------------------------------------------
-- Applicative functor morphisms, specialised to propositional
-- equality.

record Morphism {i f} {I : Set i} {F₁ F₂ : IFun I f}
                (A₁ : RawIApplicative F₁)
                (A₂ : RawIApplicative F₂) : Set (i ⊔ suc f) where
  module A₁ = RawIApplicative A₁
  module A₂ = RawIApplicative A₂
  field
    op      : ∀ {i j X} → F₁ i j X → F₂ i j X
    op-pure : ∀ {i X} (x : X) → op (A₁.pure {i = i} x) ≡ A₂.pure x
    op-⊛    : ∀ {i j k X Y} (f : F₁ i j (X → Y)) (x : F₁ j k X) →
              op (f A₁.⊛ x) ≡ (op f A₂.⊛ op x)

  op-<$> : ∀ {i j X Y} (f : X → Y) (x : F₁ i j X) →
           op (f A₁.<$> x) ≡ (f A₂.<$> op x)
  op-<$> f x = begin
    op (A₁._⊛_ (A₁.pure f) x)       ≡⟨ op-⊛ _ _ ⟩
    A₂._⊛_ (op (A₁.pure f)) (op x)  ≡⟨ P.cong₂ A₂._⊛_ (op-pure _) P.refl ⟩
    A₂._⊛_ (A₂.pure f) (op x)       ∎
    where open P.≡-Reasoning


text:
open import Prelude

module Typed
  (Name   : Set)

  -- Data stuff
  (Datatype : Name -> List (List Name))

  -- Effect stuff
  (Effect : Set)
  (_⊆_    : Effect -> Effect -> Set)
  (Monad  : Effect -> Set -> Set)
  (return : forall {M A} -> A -> Monad M A)
  (map    : forall {M A B} -> (A -> B) -> Monad M A -> Monad M B)
  (join   : forall {M A} -> Monad M (Monad M A) -> Monad M A)
  (morph  : forall {M N} -> M ⊆ N -> (A : Set) -> Monad M A -> Monad N A)
  where

_=<<_ : forall {M A B} -> (A -> Monad M B) -> Monad M A -> Monad M B
k =<< m = join (map k m)

_>>=_ : forall {M A B} -> Monad M A -> (A -> Monad M B) -> Monad M B
m >>= k = k =<< m

infixl 50 _<*>_

_<*>_ : forall {M A B} -> Monad M (A -> B) -> Monad M A -> Monad M B
f <*> x = f >>= \f -> x >>= \x -> return (f x)

infixr 80 _⟶_
infix 100 [_]_

data VTy : Set

data CTy : Set where
  _⟶_  : VTy -> CTy -> CTy
  [_]_ : Effect -> VTy -> CTy

data VTy where
  ⟨_⟩   : CTy -> VTy
  TyCon : Name -> VTy

Cxt = List VTy

data ExC : Effect -> Cxt -> CTy -> Set
data InV : Effect -> Cxt -> VTy -> Set

data InC : Cxt -> CTy -> Set where

  ƛ_  : forall {V C Γ} ->
        InC (Γ ◄ V) C -> InC Γ (V ⟶ C)

  exC : forall {M N Γ V} ->
        ExC M Γ ([ N ] V) -> N ⊆ M -> InC Γ ([ M ] V)

  inV : forall {M Γ V} ->
        InV M Γ V -> InC Γ ([ M ] V)

InDs : Effect -> Cxt -> List Name -> Set

data InV where

  ⟪_⟫ : forall {M Γ C} -> InC Γ C -> InV M Γ ⟨ C ⟩

  ⟦_⟧ : forall {M Γ V} -> InC Γ ([ M ] V) -> InV M Γ V

  con : forall {M Γ D args} ->
        args ∈ Datatype D -> InDs M Γ args -> InV M Γ (TyCon D)

InDs M Γ = Box (\D -> InV M Γ (TyCon D))

data ExC where

  var : forall {M Γ V} -> V ∈ Γ -> ExC M Γ ([ M ] V)

  _•_ : forall {M Γ V C} ->
        ExC M Γ (V ⟶ C) -> InV M Γ V -> ExC M Γ C

Els : _

data El : Name -> Set where
  el : forall {args D} -> args ∈ Datatype D -> Els args -> El D

Els = Box El

VTy⟦_⟧ : VTy -> Set

CTy⟦_⟧ : CTy -> Set
CTy⟦ V ⟶ C   ⟧ = VTy⟦ V ⟧ -> CTy⟦ C ⟧
CTy⟦ [ M ] V ⟧ = Monad M VTy⟦ V ⟧

VTy⟦ ⟨ C ⟩   ⟧ = CTy⟦ C ⟧
VTy⟦ TyCon D ⟧ = El D

Env = Box VTy⟦_⟧

inC⟦_⟧ : forall {Γ C} -> InC Γ C -> Env Γ -> CTy⟦ C ⟧

inDs⟦_⟧ : forall {M Γ Ds} ->
          InDs M Γ Ds -> Env Γ -> Monad M (Els Ds)

inV⟦_⟧ : forall {M Γ V} -> InV M Γ V -> Env Γ -> Monad M VTy⟦ V ⟧
inV⟦ ⟪ c ⟫    ⟧ ρ = return (inC⟦ c ⟧ ρ)
inV⟦ ⟦ c ⟧    ⟧ ρ = inC⟦ c ⟧ ρ
inV⟦ con x Ds ⟧ ρ = return (el x) <*> inDs⟦ Ds ⟧ ρ

inDs⟦ ⟨⟩     ⟧ ρ = return ⟨⟩
inDs⟦ Ds ◃ v ⟧ ρ = return _◃_ <*> inDs⟦ Ds ⟧ ρ <*> inV⟦ v ⟧ ρ

exC⟦_⟧ : forall {M Γ C} -> ExC M Γ C -> Env Γ -> Monad M CTy⟦ C ⟧

inC⟦ ƛ c     ⟧ ρ = \v -> inC⟦ c ⟧ (ρ ◃ v)
inC⟦ exC c m ⟧ ρ = morph m _ =<< exC⟦ c ⟧ ρ
inC⟦ inV v   ⟧ ρ = inV⟦ v ⟧ ρ

exC⟦ var x ⟧ ρ = return (return (ρ ! x))
exC⟦ f • s ⟧ ρ = exC⟦ f ⟧ ρ <*> inV⟦ s ⟧ ρ


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

open import Functions.Definition
open import Numbers.Naturals.Definition
open import Sets.FinSet.Definition

module Sets.Cardinality.Finite.Definition where

record FiniteSet {a : _} (A : Set a) : Set a where
  field
    size : ℕ
    mapping : FinSet size → A
    bij : Bijection mapping


text:
{-# OPTIONS --without-K --safe #-}
module Util.Prelude where

open import Data.Bool public using
  (Bool ; true ; false)
open import Data.Empty public using
  (⊥ ; ⊥-elim)
open import Data.Fin public using
  (Fin ; zero ; suc)
open import Data.List public using
  (List ; [] ; _∷_)
open import Data.Maybe public using
  (Maybe ; just ; nothing)
open import Data.Nat public using
  (ℕ ; zero ; suc)
open import Data.Product public using
  (Σ ; ∃ ; Σ-syntax ; ∃-syntax ; _×_ ; _,_ ; proj₁ ; proj₂)
open import Data.Sum public using
  (_⊎_ ; inj₁ ; inj₂)
open import Data.Unit public using
  (⊤)
open import Data.Vec public using
  (Vec ; [] ; _∷_)
open import Function public using
  (id ; _∘_ ; _∘′_ ; _$_ ; _on_)
open import Level public using
  (Level ; 0ℓ) renaming
  (zero to lzero ; suc to lsuc ; _⊔_ to _⊔ℓ_)
open import Relation.Nullary public using
  (¬_ ; Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality public using
  ( _≡_ ; _≢_ ; refl ; sym ; trans ; cong ; cong₂ ; subst ; subst₂
  ; module ≡-Reasoning )

infix 1 triangle⟨_⟩⟨_⟩⟨_⟩

triangle⟨_⟩⟨_⟩⟨_⟩ : ∀ {a} {A : Set a} x {y z : A}
  → y ≡ x
  → z ≡ x
  → y ≡ z
triangle⟨ x ⟩⟨ y≡x ⟩⟨ z≡x ⟩ = trans y≡x (sym z≡x)

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


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

open import Categories.Adjoint
open import Categories.Category
open import Categories.Functor renaming (id to idF)

module Categories.Adjoint.Monadic.Properties {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′}
                                             {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) where

open import Level
open import Function using (_$_)

open import Categories.Adjoint.Properties
open import Categories.Adjoint.Monadic
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.NaturalTransformation
open import Categories.Monad

open import Categories.Diagram.Coequalizer

open import Categories.Category.Construction.EilenbergMoore
open import Categories.Category.Construction.Properties.EilenbergMoore

open import Categories.Morphism
import Categories.Morphism.Reasoning as MR

private
  module L = Functor L
  module R = Functor R

  module 𝒞 = Category 𝒞
  module 𝒟 = Category 𝒟

  module adjoint = Adjoint adjoint

  T : Monad 𝒞
  T = adjoint⇒monad adjoint

  𝒞ᵀ : Category _ _ _
  𝒞ᵀ = EilenbergMoore T

  Comparison : Functor 𝒟 𝒞ᵀ
  Comparison = ComparisonF adjoint

  module Comparison = Functor Comparison

-- If we have a coequalizer of the following diagram for every T-algabra, then the comparison functor has a left adjoint.
module _ (has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))) where

  open Coequalizer

  Comparison⁻¹ : Functor 𝒞ᵀ 𝒟
  Comparison⁻¹ = record
    { F₀ = λ M → obj (has-coequalizer M)
    ; F₁ = λ {M} {N} α → coequalize (has-coequalizer M) $ begin
      𝒟 [ 𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr α) ] ∘ L.F₁ (Module.action M) ]                             ≈⟨ pullʳ (⟺ L.homomorphism) ⟩
      𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (𝒞 [ Module⇒.arr α ∘ Module.action M ]) ]                                    ≈⟨ refl⟩∘⟨ L.F-resp-≈ (Module⇒.commute α) ⟩
      𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (𝒞 [ Module.action N ∘ R.F₁ (L.F₁ (Module⇒.arr α)) ]) ]                      ≈⟨ refl⟩∘⟨ L.homomorphism ⟩
      𝒟 [ arr (has-coequalizer N) ∘ 𝒟 [ L.F₁ (Module.action N) ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ]               ≈⟨ pullˡ (equality (has-coequalizer N)) ⟩
      𝒟 [ 𝒟 [ arr (has-coequalizer N) ∘ adjoint.counit.η (L.F₀ (Module.A N)) ] ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ≈⟨ extendˡ (adjoint.counit.commute (L.F₁ (Module⇒.arr α))) ⟩
      𝒟 [ 𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr α) ] ∘ adjoint.counit.η (L.₀ (Module.A M)) ]                ∎
    ; identity = λ {A} → ⟺ $ unique (has-coequalizer A) $ begin
      𝒟 [ arr (has-coequalizer A) ∘ L.F₁ 𝒞.id ] ≈⟨ refl⟩∘⟨ L.identity ⟩
      𝒟 [ arr (has-coequalizer A) ∘ 𝒟.id ]      ≈⟨ id-comm ⟩
      𝒟 [ 𝒟.id ∘ arr (has-coequalizer A) ]      ∎
    ; homomorphism = λ {X} {Y} {Z} {f} {g} → ⟺ $ unique (has-coequalizer X) $ begin
      𝒟 [ arr (has-coequalizer Z) ∘ L.F₁ (𝒞 [ Module⇒.arr g ∘ Module⇒.arr f ]) ]                              ≈⟨ 𝒟.∘-resp-≈ʳ L.homomorphism ○ 𝒟.sym-assoc ⟩
      𝒟 [ 𝒟 [ arr (has-coequalizer Z) ∘ L.F₁ (Module⇒.arr g) ] ∘ L.F₁ (Module⇒.arr f) ]                       ≈⟨ universal (has-coequalizer Y) ⟩∘⟨refl ⟩
      𝒟 [ 𝒟 [ coequalize (has-coequalizer Y) _ ∘ arr (has-coequalizer Y) ] ∘ L.F₁ (Module⇒.arr f) ]            ≈⟨ extendˡ (universal (has-coequalizer X)) ⟩
      𝒟 [ 𝒟 [ coequalize (has-coequalizer Y) _ ∘ coequalize (has-coequalizer X) _ ] ∘ arr (has-coequalizer X) ] ∎
    ; F-resp-≈ = λ {A} {B} {f} {g} eq → unique (has-coequalizer A) $ begin
      𝒟 [ arr (has-coequalizer B) ∘ L.F₁ (Module⇒.arr g) ]            ≈⟨ refl⟩∘⟨ L.F-resp-≈ (𝒞.Equiv.sym eq) ⟩
      𝒟 [ arr (has-coequalizer B) ∘ L.F₁ (Module⇒.arr f) ]            ≈⟨ universal (has-coequalizer A) ⟩
      𝒟 [ coequalize (has-coequalizer A) _ ∘ arr (has-coequalizer A) ] ∎
    }
    where
      open 𝒟.HomReasoning
      open MR 𝒟

  private
    module Comparison⁻¹ = Functor Comparison⁻¹

  Comparison⁻¹⊣Comparison : Comparison⁻¹ ⊣ Comparison
  Adjoint.unit Comparison⁻¹⊣Comparison = ntHelper record
    { η = λ M → record
      { arr = 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ]
      ; commute = begin
        𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ]                                                      ≈⟨ pullʳ (adjoint.unit.commute (Module.action M)) ⟩
        -- It would be nice to have a reasoning combinator doing this "⟺ homomorphism ... homomorphism" pattern
        𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ]                          ≈⟨ pullˡ (⟺ R.homomorphism) ⟩
        𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ L.F₁ (Module.action M) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ]                                 ≈⟨ (R.F-resp-≈ (equality (has-coequalizer M)) ⟩∘⟨refl) ⟩
        𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ adjoint.counit.η (L.F₀ (Module.A M)) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ]                   ≈⟨ (R.homomorphism ⟩∘⟨refl) ⟩
        𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ R.F₁ (adjoint.counit.η (L.F₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ]            ≈⟨ cancelʳ adjoint.zag ⟩
        -- FIXME Use something like cancel here
        R.F₁ (arr (has-coequalizer M))                                                                                ≈˘⟨ R.F-resp-≈ (𝒟.identityʳ) ⟩
        R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟.id ])                                                                                ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ adjoint.zig) ⟩
        R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟 [ adjoint.counit.η (L.F₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ])                          ≈⟨ R.F-resp-≈ (MR.extendʳ 𝒟 (adjoint.counit.sym-commute (arr (has-coequalizer M)))) ⟩
        R.F₁ (𝒟 [ adjoint.counit.η (obj (has-coequalizer M)) ∘ 𝒟 [ L.F₁ (R.F₁ (arr (has-coequalizer M))) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ])      ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ L.homomorphism) ⟩
        R.F₁ (𝒟 [ adjoint.counit.η (obj (has-coequalizer M)) ∘ L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M)])])               ≈⟨ R.homomorphism ⟩
        𝒞 [ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ∘ R.F₁ (L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M)])) ]       ∎
      }
    ; commute = λ {M} {N} f → begin
      𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ adjoint.unit.η (Module.A N) ] ∘ Module⇒.arr f ]                           ≈⟨ extendˡ (adjoint.unit.commute (Module⇒.arr f)) ⟩
      𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ R.F₁ (L.F₁ (Module⇒.arr f)) ] ∘ adjoint.unit.η (Module.A M) ]             ≈˘⟨ R.homomorphism ⟩∘⟨refl ⟩
      𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr f) ]) ∘ adjoint.unit.η (Module.A M) ]                    ≈⟨ R.F-resp-≈ (universal (has-coequalizer M)) ⟩∘⟨refl ⟩
      𝒞 [ R.F₁ (𝒟 [ (coequalize (has-coequalizer M) _) ∘ (arr (has-coequalizer M)) ]) ∘ adjoint.unit.η (Module.A M) ]    ≈⟨ pushˡ R.homomorphism ⟩
      𝒞 [ R.F₁ (coequalize (has-coequalizer M) _) ∘ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ] ∎
    }
    where
      open 𝒞.HomReasoning
      open MR 𝒞
  Adjoint.counit Comparison⁻¹⊣Comparison = ntHelper record
    { η = λ X → coequalize (has-coequalizer (Comparison.F₀ X)) (adjoint.counit.commute (adjoint.counit.η X))
    ; commute = λ {X} {Y} f → begin
      𝒟 [ coequalize (has-coequalizer (Comparison.F₀ Y)) _ ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ]  ≈⟨ unique (has-coequalizer (Comparison.F₀ X)) (adjoint.counit.sym-commute f ○ pushˡ (universal (has-coequalizer (Comparison.F₀ Y))) ○ pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩
      coequalize (has-coequalizer (Comparison.F₀ X)) (extendˡ (adjoint.counit.commute (adjoint.counit.η X)))     ≈˘⟨ unique (has-coequalizer (Comparison.F₀ X)) (pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩
      𝒟 [ f ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ]                                                 ∎
    }
    where
      open 𝒟.HomReasoning
      open MR 𝒟
  Adjoint.zig Comparison⁻¹⊣Comparison {X} = begin
    𝒟 [ coequalize (has-coequalizer (Comparison.F₀ (Comparison⁻¹.F₀ X))) _ ∘ coequalize (has-coequalizer X) _ ] ≈⟨ unique (has-coequalizer X) (⟺ adjoint.RLadjunct≈id ○ pushˡ (universal (has-coequalizer (Comparison.F₀ (Comparison⁻¹.F₀ X)))) ○ pushʳ (universal (has-coequalizer X))) ⟩
    coequalize (has-coequalizer X) {h = arr (has-coequalizer X)} (equality (has-coequalizer X))                 ≈˘⟨ unique (has-coequalizer X) (⟺ 𝒟.identityˡ) ⟩
    𝒟.id                                                                                ∎
    where
      open 𝒟.HomReasoning
      open MR 𝒟
  Adjoint.zag Comparison⁻¹⊣Comparison {A} = begin
    𝒞 [ R.F₁ (coequalize (has-coequalizer (Comparison.F₀ A)) _) ∘  𝒞 [ R.F₁ (arr (has-coequalizer (Comparison.F₀ A))) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩
    𝒞 [ R.F₁ (𝒟 [ coequalize (has-coequalizer (Comparison.F₀ A)) _ ∘ arr (has-coequalizer (Comparison.F₀ A)) ]) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ]         ≈˘⟨ R.F-resp-≈ (universal (has-coequalizer (Comparison.F₀ A))) ⟩∘⟨refl ⟩
    𝒞 [ R.F₁ (adjoint.counit.η A) ∘ adjoint.unit.η (R.F₀ A) ]                                                                                ≈⟨ adjoint.zag ⟩
    𝒞.id                                                                                ∎
    where
      open 𝒞.HomReasoning
      open MR 𝒞

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --universe-polymorphism #-}
open import Common.Prelude
open import Common.Level
open import Common.Reflect

module UnquoteSetOmega where

`Level : Term
`Level = def (quote Level) []

``Level : Type
``Level = el (lit 0) `Level

-- while building the syntax of ∀ ℓ → Set ℓ (of type Setω) is harmless
`∀ℓ→Setℓ : Term
`∀ℓ→Setℓ = pi (arg (arginfo visible relevant) ``Level) (el (lit 0) (sort (set (var 0 []))))

-- unquoting it is harmfull
∀ℓ→Setℓ = unquote `∀ℓ→Setℓ

max_stars_repo_name: larrytheliquid/agda


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

open import lib.Basics
open import lib.types.Truncation
open import lib.types.Pi

module lib.types.Choice where

unchoose : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : A → Type j}
  → Trunc n (Π A B) → Π A (Trunc n ∘ B)
unchoose = Trunc-rec (Π-level λ _ → Trunc-level) (λ f → [_] ∘ f)

has-choice : ∀ {i} (n : ℕ₋₂) (A : Type i) j → Type (lmax i (lsucc j))
has-choice {i} n A j = (B : A → Type j) → is-equiv (unchoose {n = n} {A} {B})

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

module Data.Binary.Multiplication where

open import Data.Binary.Definition
open import Data.Binary.Addition

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

infixl 7 _*_
_*_ : 𝔹 → 𝔹 → 𝔹
0ᵇ    * ys = 0ᵇ
1ᵇ xs * ys = ys + double (ys * xs)
2ᵇ xs * ys = double (ys + ys * xs)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- Instantiation of Contractive for functions
------------------------------------------------------------------------

-- Taken from the paper.

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Contractive
open import Level

module Contractive.Function
         {A B : Set}
         {_<_ : Rel A zero}
         (isWFO : IsWellFoundedOrder _<_)
         (dec : Decidable _<_)
         (proof-irrelevance :
            ∀ {a a'} (p₁ p₂ : a < a') → p₁ ≡ p₂)
         where

open import Relation.Nullary
open import Relation.Unary
open import Data.Empty

ofe : OFE
ofe = record
  { Carrier            = A
  ; Domain             = A → B
  ; _<_                = _<_
  ; isWellFoundedOrder = isWFO
  ; Eq                 = λ a f g → f a ≡ g a
  ; isEquivalence      = λ _ → record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }

open OFE ofe hiding (_<_)

private

  limU : (A → (A → B)) → A → B
  limU f a' = f a' a'

  lim↓ : B → ∀ a → (∀ x → x < a → A → B) → A → B
  lim↓ b a f a' with dec a' a
  lim↓ b a f a' | yes a'<a = f a' a'<a a'
  lim↓ b a f a' | no  a'≮a = b

  isLimit↓ : ∀ b a {fam : Family (↓ a)} →
             IsCoherent fam → IsLimit fam (lim↓ b a fam)
  isLimit↓ b a {fam} coh {a'} a'<a with dec a' a
  isLimit↓ b a {fam} coh {a'} a'<a | no  a'≮a  = ⊥-elim (a'≮a a'<a)
  isLimit↓ b a {fam} coh {a'} a'<a | yes a'<a₂ =
    cong (λ p → fam a' p a') (proof-irrelevance a'<a a'<a₂)

-- The paper implicitly assumes that B is non-empty.

cofe : B → COFE
cofe b = record
  { ofe      = ofe
  ; limU     = limU
  ; isLimitU = λ _ _ → refl
  ; lim↓     = lim↓ b
  ; isLimit↓ = isLimit↓ b
  }

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


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

open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

postulate
  A : Set
  f : A → A
  a b c : A
  fa-to-b : f a ≡ b
  fx-to-c : ∀ x → f x ≡ c

{-# REWRITE fa-to-b #-}
{-# REWRITE fx-to-c #-}

test₁ : f a ≡ b
test₁ = refl

x : A

test₂ : f x ≡ c
test₂ = refl

x = a


text:
data Type : Set where
  A B : Type

f : Type → Type → Type
f A t = t
f t = {!t!}

-- WAS: Case-splitting t yields an internal error on Agda/TypeChecking/Coverage.hs:467

-- SHOULD: produce the following definition:
-- f : Type → Type → Type
-- f A t = t
-- f B = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda