text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.ListedFiniteSet.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sum as ⊎ using (_⊎_; inl; inr)

open import Cubical.Functions.Logic

private
  variable
    ℓ : Level
    A B : Type ℓ

infixr 20 _∷_
-- infix 30 _∈_
infixr 5 _++_

data LFSet (A : Type ℓ) : Type ℓ where
  []    : LFSet A
  _∷_   : (x : A) → (xs : LFSet A) → LFSet A
  dup   : ∀ x xs   → x ∷ x ∷ xs ≡ x ∷ xs
  comm  : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  trunc : isSet (LFSet A)

-- Membership.
--
-- Doing some proofs with equational reasoning adds an extra "_∙ refl"
-- at the end.
-- We might want to avoid it, or come up with a more clever equational reasoning.
_∈_ : {A : Type ℓ} → A → LFSet A → hProp ℓ
z ∈ []                  = Lift ⊥.⊥ , isOfHLevelLift 1 isProp⊥
z ∈ (y ∷ xs)            = (z ≡ₚ y) ⊔ (z ∈ xs)
z ∈ dup x xs i          = proof i
  where
    -- proof : z ∈ (x ∷ x ∷ xs) ≡ z ∈ (x ∷ xs)
    proof = z ≡ₚ x  ⊔ (z ≡ₚ x ⊔ z ∈ xs) ≡⟨ ⊔-assoc (z ≡ₚ x) (z ≡ₚ x) (z ∈ xs) ⟩
            (z ≡ₚ x ⊔ z ≡ₚ x) ⊔ z ∈ xs  ≡⟨ cong (_⊔ (z ∈ xs)) (⊔-idem (z ≡ₚ x)) ⟩
            z ≡ₚ x            ⊔ z ∈ xs  ∎
z ∈ comm x y xs i       = proof i
  where
    -- proof : z ∈ (x ∷ y ∷ xs) ≡ z ∈ (y ∷ x ∷ xs)
    proof = z ≡ₚ x  ⊔ (z ≡ₚ y ⊔ z ∈ xs) ≡⟨ ⊔-assoc (z ≡ₚ x) (z ≡ₚ y) (z ∈ xs) ⟩
            (z ≡ₚ x ⊔ z ≡ₚ y) ⊔ z ∈ xs  ≡⟨ cong (_⊔ (z ∈ xs)) (⊔-comm (z ≡ₚ x) (z ≡ₚ y)) ⟩
            (z ≡ₚ y ⊔ z ≡ₚ x) ⊔ z ∈ xs  ≡⟨ sym (⊔-assoc (z ≡ₚ y) (z ≡ₚ x) (z ∈ xs)) ⟩
            z ≡ₚ y  ⊔ (z ≡ₚ x ⊔ z ∈ xs) ∎
x ∈ trunc xs ys p q i j = isSetHProp (x ∈ xs) (x ∈ ys) (cong (x ∈_) p) (cong (x ∈_) q) i j

module Elim {ℓ}
  {B : LFSet A → Type ℓ}
  ([]* : B [])
  (_∷*_ : (x : A) {xs : LFSet A} → B xs → B (x ∷ xs))
  (comm* : (x y : A) {xs : LFSet A} (b : B xs)
    → PathP (λ i → B (comm x y xs i)) (x ∷* (y ∷* b)) (y ∷* (x ∷* b)))
  (dup* : (x : A) {xs : LFSet A} (b : B xs)
    → PathP (λ i → B (dup x xs i)) (x ∷* (x ∷* b)) (x ∷* b))
  (trunc* : (xs : LFSet A) → isSet (B xs)) where

  f : ∀ x → B x
  f [] = []*
  f (x ∷ xs) = x ∷* f xs
  f (dup x xs i) = dup* x (f xs) i
  f (comm x y xs i) = comm* x y (f xs) i
  f (trunc x y p q i j) =
    isOfHLevel→isOfHLevelDep 2 trunc*
      (f x) (f y)
      (λ i → f (p i)) (λ i → f (q i))
      (trunc x y p q) i j

module Rec {ℓ} {B : Type ℓ}
  ([]* : B)
  (_∷*_ : (x : A) → B → B)
  (comm* : (x y : A) (xs : B) → (x ∷* (y ∷* xs)) ≡ (y ∷* (x ∷* xs)))
  (dup* : (x : A) (b : B) → (x ∷* (x ∷* b)) ≡ (x ∷* b))
  (trunc* : isSet B) where

  f : LFSet A → B
  f =
    Elim.f
      []* (λ x xs → x ∷* xs)
      (λ x y b → comm* x y b) (λ x b → dup* x b)
      λ _ → trunc*

module PropElim {ℓ}
  {B : LFSet A → Type ℓ}
  ([]* : B []) (_∷*_ : (x : A) {xs : LFSet A} → B xs → B (x ∷ xs))
  (trunc* : (xs : LFSet A) → isProp (B xs)) where

  f : ∀ x → B x
  f =
    Elim.f
      []* _∷*_
      (λ _ _ _ → isOfHLevel→isOfHLevelDep 1 trunc* _ _ _)
      (λ _ _ → isOfHLevel→isOfHLevelDep 1 trunc* _ _ _)
      λ xs → isProp→isSet (trunc* xs)

_++_ : ∀ (xs ys : LFSet A) → LFSet A
[]                  ++ ys = ys
(x ∷ xs)            ++ ys = x ∷ (xs ++ ys)
dup x xs i          ++ ys = dup x (xs ++ ys) i
comm x y xs i       ++ ys = comm x y (xs ++ ys) i
trunc xs zs p q i j ++ ys =
  trunc (xs ++ ys) (zs ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j

map : (A → B) → LFSet A → LFSet B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs
map f (dup x xs i) = dup (f x) (map f xs) i
map f (comm x y xs i) = comm (f x) (f y) (map f xs) i
map f (trunc xs ys p q i j) =
  trunc (map f xs) (map f ys) (cong (map f) p) (cong (map f) q) i j

disj-union : LFSet A → LFSet B → LFSet (A ⊎ B)
disj-union xs ys = map ⊎.inl xs ++ map ⊎.inr ys


text:
------------------------------------------------------------------------
-- Pointwise lifting of (binary) initial bag operators to parsers
------------------------------------------------------------------------

open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Binary.BagAndSetEquality
  using () renaming (_∼[_]_ to _List-∼[_]_)
open import Function.Related as Related using (Kind; SK-sym)

module TotalParserCombinators.Pointwise
  (R₁ R₂ : Set) {R₃ : Set}

  -- Some kinds of equality.
  {K : Set} (⌊_⌋ : K → Kind)

  -- An initial bag operator.
  (_∙_ : List R₁ → List R₂ → List R₃)

  -- The operator must preserve the given notions of equality.
  (_∙-cong_ : ∀ {k xs₁ xs₁′ xs₂ xs₂′} →
              xs₁ List-∼[ ⌊ k ⌋ ] xs₁′ → xs₂ List-∼[ ⌊ k ⌋ ] xs₂′ →
              (xs₁ ∙ xs₂) List-∼[ ⌊ k ⌋ ] (xs₁′ ∙ xs₂′))
  where

open import Codata.Musical.Notation
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Function.Inverse using (_↔_; module Inverse)

open import TotalParserCombinators.Congruence as C using (_∼[_]P_; _≅P_)
import TotalParserCombinators.Congruence.Sound as CS
open import TotalParserCombinators.Derivative as D
import TotalParserCombinators.InitialBag as I
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics using (_∈_·_)

------------------------------------------------------------------------
-- Lift

-- A lifting of the initial bag operator _∙_ to the level of parsers.
--
-- Note that this definition is closely related to Theorem 4.4 in
-- Brzozowski's paper "Derivatives of Regular Expressions".
--
-- Note also that _∙_ is allowed to pattern match on the input
-- indices, so it may not be obvious that lift preserves equality.
-- This fact is established explicitly below (by making use of
-- _∙-cong_).

lift : ∀ {Tok xs₁ xs₂} →
       Parser Tok R₁ xs₁ → Parser Tok R₂ xs₂ →
       Parser Tok R₃ (xs₁ ∙ xs₂)
lift p₁ p₂ =
    (token >>= λ t → ♯ lift (D t p₁) (D t p₂))
  ∣ return⋆ (initial-bag p₁ ∙ initial-bag p₂)

------------------------------------------------------------------------
-- Properties of lift

-- D distributes over lift.

D-lift : ∀ {Tok xs₁ xs₂ t}
         (p₁ : Parser Tok R₁ xs₁) (p₂ : Parser Tok R₂ xs₂) →
         D t (lift p₁ p₂) ≅P lift (D t p₁) (D t p₂)
D-lift {xs₁ = xs₁} {xs₂} {t} p₁ p₂ =
  D t (lift p₁ p₂)                               ≅⟨ D t (lift p₁ p₂) ∎ ⟩

  (return t >>= λ t → lift (D t p₁) (D t p₂)) ∣
    D t (return⋆ (xs₁ ∙ xs₂))                    ≅⟨ Monad.left-identity t (λ t → lift (D t p₁) (D t p₂)) ∣
                                                    D.D-return⋆ (xs₁ ∙ xs₂) ⟩
  lift (D t p₁) (D t p₂) ∣ fail                  ≅⟨ AdditiveMonoid.right-identity (lift (D t p₁) (D t p₂)) ⟩

  lift (D t p₁) (D t p₂)                         ∎
  where open C using (_≅⟨_⟩_; _∎; _∣_)

-- lift preserves equality.

lift-cong : ∀ {k Tok xs₁ xs₁′ xs₂ xs₂′}
              {p₁ : Parser Tok R₁ xs₁} {p₁′ : Parser Tok R₁ xs₁′}
              {p₂ : Parser Tok R₂ xs₂} {p₂′ : Parser Tok R₂ xs₂′} →
            p₁ ∼[ ⌊ k ⌋ ]P p₁′ → p₂ ∼[ ⌊ k ⌋ ]P p₂′ →
            lift p₁ p₂ ∼[ ⌊ k ⌋ ]P lift p₁′ p₂′
lift-cong {k} {xs₁ = xs₁} {xs₁′} {xs₂} {xs₂′} {p₁} {p₁′} {p₂} {p₂′}
  p₁≈p₁′ p₂≈p₂′ = lemma ∷ λ t → ♯ (
  D t (lift p₁ p₂)          ≅⟨ D-lift p₁ p₂ ⟩
  lift (D t p₁) (D t p₂)    ∼⟨ lift-cong (CS.D-cong p₁≈p₁′) (CS.D-cong p₂≈p₂′) ⟩
  lift (D t p₁′) (D t p₂′)  ≅⟨ sym (D-lift p₁′ p₂′) ⟩
  D t (lift p₁′ p₂′)        ∎)
  where
  open C using (_≅⟨_⟩_; _∼⟨_⟩_; _∎; sym; _∷_)

  lemma : (xs₁ ∙ xs₂) List-∼[ ⌊ k ⌋ ] (xs₁′ ∙ xs₂′)
  lemma = I.cong (CS.sound p₁≈p₁′) ∙-cong I.cong (CS.sound p₂≈p₂′)

-- Lifts a property from _∙_ to lift. For examples of its use, see
-- TotalParserCombinators.{And,AsymmetricChoice,Not}.

lift-property :
  (P : ∀ {ℓ} → (R₁ → Set ℓ) → (R₂ → Set ℓ) → (R₃ → Set ℓ) → Set ℓ)

  (P-cong :
   ∀ {ℓ}  {F₁  : R₁ → Set ℓ}  {F₂  : R₂ → Set ℓ}  {F₃  : R₃ → Set ℓ}
     {ℓ′} {F₁′ : R₁ → Set ℓ′} {F₂′ : R₂ → Set ℓ′} {F₃′ : R₃ → Set ℓ′} →
   (∀ x → F₁ x ↔ F₁′ x) → (∀ x → F₂ x ↔ F₂′ x) → (∀ x → F₃ x ↔ F₃′ x) →
   P F₁ F₂ F₃ ⇔ P F₁′ F₂′ F₃′) →

  (P-∙ :
     ∀ {xs₁ xs₂} →
     P (λ x → x ∈ xs₁) (λ x → x ∈ xs₂) (λ x → x ∈ (xs₁ ∙ xs₂))) →

  ∀ {Tok xs₁ xs₂ s}
  (p₁ : Parser Tok R₁ xs₁) (p₂ : Parser Tok R₂ xs₂) →
  P (λ x → x ∈ p₁ · s) (λ x → x ∈ p₂ · s) (λ x → x ∈ lift p₁ p₂ · s)

lift-property P P-cong P-∙ {s = []} p₁ p₂ =
  Equivalence.from
    (P (λ x → x ∈ p₁ · []) (λ x → x ∈ p₂ · [])
       (λ x → x ∈ lift p₁ p₂ · [])                            ∼⟨ P-cong (λ _ → I.correct) (λ _ → I.correct) (λ _ → I.correct) ⟩

     P (λ x → x ∈ initial-bag p₁) (λ x → x ∈ initial-bag p₂)
       (λ x → x ∈ (initial-bag p₁ ∙ initial-bag p₂))          ∎

    ) ⟨$⟩ P-∙
  where open Related.EquationalReasoning

lift-property P P-cong P-∙ {s = t ∷ s} p₁ p₂ =
   Equivalence.from
    (P (λ x → x ∈ p₁ · t ∷ s) (λ x → x ∈ p₂ · t ∷ s)
       (λ x → x ∈ lift p₁ p₂ · t ∷ s)                 ∼⟨ SK-sym $ P-cong (λ _ → D.correct) (λ _ → D.correct) (λ _ → D.correct) ⟩

     P (λ x → x ∈ D t p₁ · s) (λ x → x ∈ D t p₂ · s)
       (λ x → x ∈ D t (lift p₁ p₂) · s)               ∼⟨ P-cong (λ _ → _ ∎) (λ _ → _ ∎) (λ _ → CS.sound (D-lift p₁ p₂)) ⟩

     P (λ x → x ∈ D t p₁ · s) (λ x → x ∈ D t p₂ · s)
       (λ x → x ∈ lift (D t p₁) (D t p₂) · s)         ∎

    ) ⟨$⟩ lift-property P P-cong P-∙ (D t p₁) (D t p₂)
  where open Related.EquationalReasoning

ext: agda

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Everything where

import Library

import Terms
import Substitution
import SN
import SN.AntiRename
import Reduction
import SAT3
import DeclSN
import Soundness

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
------------------------------------------------------------------------
-- Code related to the paper "Higher Inductive Type Eliminators
-- Without Paths"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- Note that the code does not follow the paper exactly, and that some
-- of the code has been changed after the paper was published.

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

module README.HITs-without-paths where

import Equality
import Equality.Id
import Equality.Instances-related
import Equality.Path
import Equality.Path.Isomorphisms
import Equality.Propositional
import Function-universe
import H-level
import H-level.Truncation.Propositional
import Quotient
import Suspension

------------------------------------------------------------------------
-- 1: Introduction

-- The propositional truncation operator.

∥_∥ = H-level.Truncation.Propositional.∥_∥

-- Equality defined as an inductive family with a single constructor
-- refl.

_≡_ = Equality.Propositional._≡_

------------------------------------------------------------------------
-- 2: An Axiomatisation of Equality With J

-- The code uses an axiomatisation of "equality with J", as discussed
-- in the text. The axiomatisation is a little convoluted in order to
-- support using equality at all universe levels. Furthermore, also as
-- discussed in the text, the axiomatisation supports choosing
-- specific definitions for other functions, like cong, to make the
-- code more usable when it is instantiated with Cubical Agda paths
-- (for which the canonical definition of cong computes in a different
-- way than typical definitions obtained using J).

-- Equality and reflexivity.

≡-refl = Equality.Reflexive-relation

-- The J rule and its computation rule.

J-J-refl = Equality.Equality-with-J₀

-- Extended variants of the two definitions above.

Equivalence-relation⁺ = Equality.Equivalence-relation⁺
Equality-with-J       = Equality.Equality-with-J
Equality-with-paths   = Equality.Path.Equality-with-paths

-- The extended variants are inhabited for all universe levels if the
-- basic ones are inhabited for all universe levels.

J₀⇒Equivalence-relation⁺             = Equality.J₀⇒Equivalence-relation⁺
J₀⇒J                                 = Equality.J₀⇒J
Equality-with-J₀⇒Equality-with-paths =
  Equality.Path.Equality-with-J₀⇒Equality-with-paths

-- To see how the code is axiomatised, see the module header of, say,
-- Circle.

import Circle

-- Any two notions of equality satisfying the axioms are pointwise
-- isomorphic, and the isomorphisms map canonical proofs of
-- reflexivity to canonical proofs of reflexivity.
--
-- Note that in some cases the code uses bijections (_↔_) instead of
-- equivalences (_≃_).

instances-isomorphic =
  Equality.Instances-related.all-equality-types-isomorphic

-- Cubical Agda paths, the Cubical Agda identity type family, and a
-- definition of equality as an inductive family with a single
-- constructor refl are instances of the axioms. (The last instance is
-- for Equality-with-J rather than Equality-with-paths, because the
-- latter definition is defined in Cubical Agda, and the instance is
-- not.)

paths-instance            = Equality.Path.equality-with-paths
id-instance               = Equality.Id.equality-with-paths
inductive-family-instance = Equality.Propositional.equality-with-J

------------------------------------------------------------------------
-- 3: Homogeneous Paths

-- The path type constructor.

Path = Equality.Path._≡_

-- Zero and one.

0̲ = Equality.Path.0̲
1̲ = Equality.Path.1̲

-- Reflexivity.

reflᴾ = Equality.Path.refl

-- Minimum, maximum and negation.

min = Equality.Path.min
max = Equality.Path.max
-_  = Equality.Path.-_

-- The primitive transport operation.

open Equality.Path using (transport)

-- The J rule and transport-refl.

Jᴾ             = Equality.Path.elim
transport-refl = Equality.Path.transport-refl

-- Transitivity (more general than in the paper).

transᴾ = Equality.Path.htransʳ

------------------------------------------------------------------------
-- 4: Heterogeneous Paths

-- Pathᴴ.

Pathᴴ = Equality.Path.[_]_≡_

-- The eliminator elimᴾ for the propositional truncation operator.

module ∥_∥ where

  elimᴾ = H-level.Truncation.Propositional.elimᴾ′

-- Pathᴴ≡Path and Pathᴴ≃Path.

Pathᴴ≡Path = Equality.Path.heterogeneous≡homogeneous
Pathᴴ≃Path = Equality.Path.heterogeneous↔homogeneous

-- The lemma substᴾ.

substᴾ = Equality.Path.subst

-- The lemmas subst and subst-refl from the axiomatisation.

subst      = Equality.Equality-with-J.subst
subst-refl = Equality.Equality-with-J.subst-refl

-- The axiomatisation makes it possible to choose the implementations
-- of to-path and from-path.

to-path   = Equality.Path.Equality-with-paths.to-path
from-path = Equality.Path.Equality-with-paths.from-path

-- The code mostly uses a pointwise isomorphism between the arbitrary
-- notion of equality and paths instead of from-path and to-path.

≡↔≡ = Equality.Path.Derived-definitions-and-properties.≡↔≡

-- The lemmas subst≡substᴾ, subst≡≃Pathᴴ, subst≡→Pathᴴ and
-- subst≡→substᴾ≡ (which is formulated as a bijection).

subst≡substᴾ   = Equality.Path.Isomorphisms.subst≡subst
subst≡≃Pathᴴ   = Equality.Path.Isomorphisms.subst≡↔[]≡
subst≡→Pathᴴ   = Equality.Path.Isomorphisms.subst≡→[]≡
subst≡→substᴾ≡ = Equality.Path.Isomorphisms.subst≡↔subst≡

-- The lemmas congᴰ and congᴰ-refl from the axiomatisation.

congᴰ      = Equality.Equality-with-J.dcong
congᴰ-refl = Equality.Equality-with-J.dcong-refl

-- The lemmas congᴴ and congᴰᴾ.

congᴴ  = Equality.Path.hcong
congᴰᴾ = Equality.Path.dcong

-- The proofs congᴰ≡congᴰᴾ, congᴰᴾ≡congᴴ, congᴰ≡congᴴ and
-- dependent‐computation‐rule‐lemma.

congᴰ≡congᴰᴾ = Equality.Path.Isomorphisms.dcong≡dcong
congᴰᴾ≡congᴴ = Equality.Path.dcong≡hcong
congᴰ≡congᴴ = Equality.Path.Isomorphisms.dcong≡hcong
dependent‐computation‐rule‐lemma =
  Equality.Path.Isomorphisms.dcong-subst≡→[]≡

------------------------------------------------------------------------
-- 5: The Circle Without Paths

-- The circle and loop.

𝕊¹   = Circle.𝕊¹
loop = Circle.loop

-- The lemmas cong and cong-refl from the axiomatisation.

cong      = Equality.Equality-with-J.cong
cong-refl = Equality.Equality-with-J.cong-refl

-- The lemma non-dependent-computation-rule-lemma.

non-dependent-computation-rule-lemma =
  Equality.Path.Isomorphisms.cong-≡↔≡

-- The lemma trans, which is actually a part of the axiomatisation
-- that I use, but which can be proved using the J rule.

trans    = Equality.Equivalence-relation⁺.trans
J₀⇒trans = Equality.J₀⇒Equivalence-relation⁺

-- The lemma subst-const.

subst-const = Equality.Derived-definitions-and-properties.subst-const

-- The lemma congᴰ≡→cong≡.

congᴰ≡→cong≡ = Equality.Derived-definitions-and-properties.dcong≡→cong≡

-- Eliminators and computation rules.

module 𝕊¹ where

  elimᴾ     = Circle.elimᴾ
  recᴾ      = Circle.recᴾ
  elim      = Circle.elim
  elim-loop = Circle.elim-loop
  rec       = Circle.rec
  rec-loop  = Circle.rec-loop
  rec′      = Circle.rec′
  rec′-loop = Circle.rec′-loop

------------------------------------------------------------------------
-- 6: Set Quotients Without Paths

-- The definition of h-levels.

Contractible   = Equality.Derived-definitions-and-properties.Contractible
H-level        = H-level.H-level
Is-proposition = Equality.Derived-definitions-and-properties.Is-proposition
Is-set         = Equality.Derived-definitions-and-properties.Is-set

-- Set quotients.

_/_ = Quotient._/_

-- Some lemmas.

H-levelᴾ-suc≃H-levelᴾ-Pathᴴ = Equality.Path.H-level-suc↔H-level[]≡
index-irrelevant            = Equality.Path.index-irrelevant
transport-transport         = Equality.Path.transport∘transport
heterogeneous-irrelevance   = Equality.Path.heterogeneous-irrelevance
heterogeneous-UIP           = Equality.Path.heterogeneous-UIP
H-level≃H-levelᴾ            = Equality.Path.Isomorphisms.H-level↔H-level

-- A generalisation of Π-cong. Note that equality is provably
-- extensional in Cubical Agda.

Π-cong         = Function-universe.Π-cong
extensionality = Equality.Path.ext

-- Variants of the constructors.

[]-respects-relation = Quotient.[]-respects-relation
/-is-set             = Quotient./-is-set

-- Eliminators.

module _/_ where

  elimᴾ′ = Quotient.elimᴾ′
  elimᴾ  = Quotient.elimᴾ
  recᴾ   = Quotient.recᴾ
  elim   = Quotient.elim
  rec    = Quotient.rec

------------------------------------------------------------------------
-- 7: More Examples

-- Suspensions.

module Susp where

  Susp          = Suspension.Susp
  elimᴾ         = Suspension.elimᴾ
  recᴾ          = Suspension.recᴾ
  meridian      = Suspension.meridian
  elim          = Suspension.elim
  elim-meridian = Suspension.elim-meridian
  rec           = Suspension.rec
  rec-meridian  = Suspension.rec-meridian

-- The propositional truncation operator.

module Propositional-truncation where

  elimᴾ′  = H-level.Truncation.Propositional.elimᴾ′
  elimᴾ   = H-level.Truncation.Propositional.elimᴾ
  recᴾ    = H-level.Truncation.Propositional.recᴾ
  trivial = H-level.Truncation.Propositional.truncation-is-proposition
  elim    = H-level.Truncation.Propositional.elim
  rec     = H-level.Truncation.Propositional.rec

------------------------------------------------------------------------
-- 8: An Alternative Approach

-- Circle and Circleᴾ, combined into a single definition.

Circle = Circle.Circle

-- Circleᴾ≃Circle, circleᴾ and circle.

Circleᴾ≃Circle = Circle.Circle≃Circle
circleᴾ        = Circle.circleᴾ
circle         = Circle.circle

-- The computation rule for the higher constructor.

elim-loop-circle = Circle.elim-loop-circle

-- Alternative definitions of Circleᴾ≃Circle and circle that (at the
-- time of writing) do not give the "correct" computational behaviour
-- for the point constructor.

Circleᴾ≃Circle′ = Circle.Circle≃Circle′
circle′         = Circle.circle′

------------------------------------------------------------------------
-- 9: Discussion

-- The interval.

import Interval

-- Pushouts.

import Pushout

-- A general truncation operator.

import H-level.Truncation

-- The torus.

import Torus

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Prelude hiding (subst)

module Implicits.Substitutions.Term where

open import Implicits.Syntax.Type
open import Implicits.Syntax.Term

open import Data.Fin.Substitution
open import Data.Star as Star hiding (map)
open import Data.Star.Properties
open import Data.Vec hiding ([_])

open import Implicits.Substitutions.Type as TypeSubst using ()

module TermTypeSubst where

  module TermTypeApp {T} (l : Lift T Type) where
    open Lift l hiding (var)
    open TypeSubst.TypeApp l renaming (_/_ to _/tp_)

    infixl 8 _/_

    -- Apply a type substitution to a term
    _/_ : ∀ {ν μ n} → Term ν n → Sub T ν μ → Term μ n
    var x      / σ = var x
    Λ t        / σ = Λ (t / σ ↑)
    λ' a t     / σ = λ' (a /tp σ) (t / σ)
    t [ a ]    / σ = (t / σ) [ a /tp σ ]
    s · t      / σ = (s / σ) · (t / σ)
    ρ a t      / σ = ρ (a /tp σ) (t / σ)
    r ⟨⟩     / σ = (r / σ) ⟨⟩
    r with' e  / σ = (r / σ) with' (e / σ)

  open TypeSubst using (varLift; termLift; sub)

  module Lifted {T} (lift : Lift T Type) {n} where
    application : Application (λ ν → Term ν n) T
    application = record { _/_ = TermTypeApp._/_ lift {n = n} }

    open Application application public

  open Lifted termLift public

  -- apply a type variable substitution (renaming) to a term
  _/Var_ : ∀ {ν μ n} → Term ν n → Sub Fin ν μ → Term μ n
  _/Var_ = TermTypeApp._/_ varLift

  -- weaken a term with an additional type variable
  weaken : ∀ {ν n} → Term ν n → Term (suc ν) n
  weaken t = t /Var VarSubst.wk

  infix 8 _[/_]

  -- shorthand for single-variable type substitutions in terms
  _[/_] : ∀ {ν n} → Term (suc ν) n → Type ν → Term ν n
  t [/ b ] = t / sub b

module TermTermSubst where

  -- Substitutions of terms in terms
  TermSub : (ℕ → ℕ → Set) → ℕ → ℕ → ℕ → Set
  TermSub T ν m n = Sub (T ν) m n

  record TermLift (T : ℕ → ℕ → Set) : Set where
    infix 10 _↑tm _↑tp
    field
      lift : ∀ {ν n} → T ν n → Term ν n
      _↑tm : ∀ {ν m n} → TermSub T ν m n → TermSub T ν (suc m) (suc n)
      _↑tp : ∀ {ν m n} → TermSub T ν m n → TermSub T (suc ν) m n

  module TermTermApp {T} (l : TermLift T) where
    open TermLift l

    infixl 8 _/_

    -- Apply a term substitution to a term
    _/_ : ∀ {ν m n} → Term ν m → TermSub T ν m n → Term ν n
    var x      / σ = lift $ lookup x σ
    Λ t        / σ = Λ (t / σ ↑tp)
    λ' a t     / σ = λ' a (t / σ ↑tm)
    t [ a ]    / σ = (t / σ) [ a ]
    s · t      / σ = (s / σ) · (t / σ)
    ρ a t      / σ = ρ a (t / σ ↑tm)
    r ⟨⟩        / σ = (r / σ) ⟨⟩
    r with' e  / σ = (r / σ) with' (e / σ)

  Fin′ : ℕ → ℕ → Set
  Fin′ _ m = Fin m

  varLift : TermLift Fin′
  varLift = record { lift = var; _↑tm = VarSubst._↑; _↑tp = Prelude.id }

  infixl 8 _/Var_

  _/Var_ : ∀ {ν m n} → Term ν m → Sub Fin m n → Term ν n
  _/Var_ = TermTermApp._/_ varLift

  private
    module ExpandSimple {n : ℕ} where
      simple : Simple (Term n)
      simple = record { var = var; weaken = λ t → t /Var VarSubst.wk }

      open Simple simple public

  open ExpandSimple  using (_↑; simple)
  open TermTypeSubst using () renaming (weaken to weakenTp)

  termLift : TermLift Term
  termLift = record
    { lift = Prelude.id; _↑tm = _↑ ; _↑tp = λ ρ → map weakenTp ρ }

  private
    module ExpandSubst {ν : ℕ} where
      app : Application (Term ν) (Term ν)
      app = record { _/_ = TermTermApp._/_ termLift {ν = ν} }

      subst : Subst (Term ν)
      subst = record
        { simple      = simple
        ; application = app
        }

      open Subst subst public

  open ExpandSubst public hiding (var; simple)

  infix 8 _[/_]

  -- Shorthand for single-variable term substitutions in terms
  _[/_] : ∀ {ν n} → Term ν (suc n) → Term ν n → Term ν n
  s [/ t ] = s / sub t


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

module 13-implicitProofObligations where

module Imports where
  module L where
    open import Agda.Primitive public
      using (Level; _⊔_) renaming (lzero to zero; lsuc to suc)

  -- extract from Data.Unit
  record ⊤ : Set where
    constructor tt

  -- extract from Data.Empty
  data ⊥ : Set where

  ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
  ⊥-elim ()

  -- extract from Function
  id : ∀ {a} {A : Set a} → A → A
  id x = x

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

  _∘_ : ∀ {a b c}
          {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
        ((x : A) → C (g x))
  f ∘ g = λ x → f (g x)

  -- extract from Data.Bool
  data Bool : Set where
    true  : Bool
    false : Bool

  not : Bool → Bool
  not true  = false
  not false = true

  T : Bool → Set
  T true  = ⊤
  T false = ⊥

  -- extract from Relation.Nullary.Decidable and friends
  infix 3 ¬_

  ¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
  ¬ P = P → ⊥

  data Dec {p} (P : Set p) : Set p where
    yes : ( p :   P) → Dec P
    no  : (¬p : ¬ P) → Dec P
  ⌊_⌋ : ∀ {p} {P : Set p} → Dec P → Bool
  ⌊ yes _ ⌋ = true
  ⌊ no  _ ⌋ = false

  False : ∀ {p} {P : Set p} → Dec P → Set
  False Q = T (not ⌊ Q ⌋)

  -- extract from Relation.Binary.PropositionalEquality
  data _≡_ {a} {A : Set a} (x : A) : A → Set a where
    refl : x ≡ x

  cong : ∀ {a b} {A : Set a} {B : Set b}
         (f : A → B) {x y} → x ≡ y → f x ≡ f y
  cong f refl = refl

  _≢_ : ∀ {a} {A : Set a} → A → A → Set a
  x ≢ y = ¬ x ≡ y

  -- extract from Data.Nat
  data ℕ : Set where
    zero : ℕ
    suc  : (n : ℕ) → ℕ

  {-# BUILTIN NATURAL ℕ    #-}

  pred : ℕ → ℕ
  pred zero    = zero
  pred (suc n) = n

  infixl 6 _+_

  _+_ : ℕ → ℕ → ℕ
  -- zero  + n = n
  -- suc m + n = suc (m + n)
  zero  + n = n
  suc m + n = suc (m + n)

  _*_ : ℕ → ℕ → ℕ
  zero  * n = zero
  suc m * n = n + m * n

  _≟_ : (x y : ℕ) → Dec (x ≡ y)
  zero  ≟ zero   = yes refl
  suc m ≟ suc n  with m ≟ n
  suc m ≟ suc .m | yes refl = yes refl
  suc m ≟ suc n  | no prf   = no (prf ∘ cong pred)
  zero  ≟ suc n  = no λ()
  suc m ≟ zero   = no λ()

  -- extract from Data.Fin
  data Fin : ℕ → Set where
    zero : {n : ℕ} → Fin (suc n)
    suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

  -- A conversion: toℕ "n" = n.

  toℕ : ∀ {n} → Fin n → ℕ
  toℕ zero    = 0
  toℕ (suc i) = suc (toℕ i)

  -- extract from Data.Product
  record Σ {a b} (A : Set a) (B : A → Set b) : Set (a L.⊔ b) where
    constructor _,_
    field
      proj₁ : A
      proj₂ : B proj₁

  _×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a L.⊔ b)
  A × B = Σ A (λ (_ : A) → B)

  -- extract from Data.Nat.DivMod

  data DivMod : ℕ → ℕ → Set where
    result : {divisor : ℕ} (q : ℕ) (r : Fin divisor) →
             DivMod (toℕ r + q * divisor) divisor

  data DivMod' (dividend divisor : ℕ) : Set where
    result : (q : ℕ) (r : Fin divisor)
             (eq : dividend ≡ (toℕ r + q * divisor)) →
             DivMod' dividend divisor

  postulate
    _div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
    _divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
               DivMod dividend divisor
    _divMod'_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
                        DivMod' dividend divisor

open Imports

-- Begin of actual example!

postulate
  d : ℕ
  d≢0 : d ≢ 0
--  d≢0' : d ≢ 0

fromWitnessFalse : ∀ {p} {P : Set p} {Q : Dec P} → ¬ P → False Q
fromWitnessFalse {Q = yes p} ¬P = ⊥-elim $ ¬P p
fromWitnessFalse {Q = no ¬p} ¬P = tt

⋯ : {A : Set} → {{v : A}} → A
⋯ {{v}} = v

_divMod′_ : (dividend divisor : ℕ) {{ ≢0 : divisor ≢ 0 }} → ℕ × ℕ
_divMod′_ a d {{_}} with _divMod_ a d { fromWitnessFalse ⋯ }
._ divMod′ d | (result q r) = q , toℕ r

_div′_ : (dividend divisor : ℕ) {{ ≢0 : divisor ≢ 0 }} → ℕ
_div′_ a b {{_}} with a divMod′ b
a div′ b | (q , _) = q

--Agda can't resolve hiddens
-- test : {d≢0 : False (d ≟ 0)} → ℕ
-- test = 5 div d
-- test2 : {{d≢0 : d ≢ 0}} → ℕ
-- test2 = 5 div′ d

test3 = 5 div 2
test4 = 5 div′ 2
  where nz : 2 ≢ 0
        nz ()

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- Testing Agda internal term: @Var Nat Args@ when @Args ≠ []@
------------------------------------------------------------------------------

{-# OPTIONS --exact-split                    #-}
{-# OPTIONS --no-universe-polymorphism       #-}
{-# OPTIONS --universal-quantified-functions #-}
{-# OPTIONS --without-K                      #-}

module NonFOLAgdaInternalTermsVarNonEmptyArgumentsTerm where

postulate
  D   : Set
  _≡_ : D → D → Set

-- TODO: 2012-04-29. Are we using Koen's approach in the translation?
postulate f-refl : (f : D → D) → ∀ x → f x ≡ f x
{-# ATP prove f-refl #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

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

module _ where

data D (A : Set) : Set where
  c    : D A
  step : ∀ (x : D A) → c ≡ x

data _~_ {A : Set} : (x y : D A) → Set

record _~′_ {A : Set} (x y : D A) : Set where
  coinductive
  field
    force : x ~ y
open _~′_

data _~_ {A} where
  c~    : ∀ {x y : D A} → c ~ c
  step~ : ∀ {x y} → (p : x ~′ y) → PathP (λ i → step x i ~ step y i) c~ (p .force)

foo : ∀ {A : Set} (x y : D A) → (x ~ y) → Set₁
foo _ _ (step~ _ _) = {!!}
foo _ _ c~ = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Semirings.Definition

module Fields.CauchyCompletion.NearlyTotalOrder {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open PartiallyOrderedRing pRing
open Ring R
open Group additiveGroup
open Field F
open import Fields.Orders.Lemmas {F = F} {pRing} (record { oRing = order })
open import Setoids.Orders.Partial.Sequences pOrder

open import Rings.InitialRing R
open import Rings.Orders.Partial.Lemmas pRing
open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.Cauchy order
open import Rings.Orders.Total.AbsoluteValue order
open import Fields.Lemmas F
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Setoid order F
open import Fields.CauchyCompletion.Group order F
open import Fields.CauchyCompletion.Addition order F
open import Fields.CauchyCompletion.Approximation order F
open import Fields.CauchyCompletion.Comparison order F
open import Fields.CauchyCompletion.PartiallyOrderedRing order F
open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })

makeIncreasingLemma : (a : A) (s : Sequence A) → Sequence A
Sequence.head (makeIncreasingLemma a s) with totality a (Sequence.head s)
... | inl (inl x) = Sequence.head s
... | inl (inr x) = a
... | inr x = a
Sequence.tail (makeIncreasingLemma a s) = makeIncreasingLemma (Sequence.head (makeIncreasingLemma a s)) (Sequence.tail s)

makeIncreasingLemmaIsIncreasing : (a : A) (s : Sequence A) → WeaklyIncreasing (makeIncreasingLemma a s)
makeIncreasingLemmaIsIncreasing a s zero with totality a (Sequence.head s)
makeIncreasingLemmaIsIncreasing a s zero | inl (inl x) with totality (Sequence.head s) (Sequence.head (Sequence.tail s))
makeIncreasingLemmaIsIncreasing a s zero | inl (inl x) | inl (inl y) = inl y
makeIncreasingLemmaIsIncreasing a s zero | inl (inl x) | inl (inr y) = inr reflexive
makeIncreasingLemmaIsIncreasing a s zero | inl (inl x) | inr y = inr reflexive
makeIncreasingLemmaIsIncreasing a s zero | inl (inr x) with totality a (Sequence.head (Sequence.tail s))
... | inl (inl y) = inl y
... | inl (inr y) = inr reflexive
... | inr y = inr reflexive
makeIncreasingLemmaIsIncreasing a s zero | inr x with totality a (Sequence.head (Sequence.tail s))
... | inl (inl y) = inl y
... | inl (inr y) = inr reflexive
... | inr y = inr reflexive
makeIncreasingLemmaIsIncreasing a s (succ m) = makeIncreasingLemmaIsIncreasing (Sequence.head (makeIncreasingLemma a s)) (Sequence.tail s) m

makeIncreasing : Sequence A → Sequence A
Sequence.head (makeIncreasing x) = Sequence.head x
Sequence.tail (makeIncreasing x) = makeIncreasingLemma (Sequence.head x) (Sequence.tail x)

makeIncreasingIsIncreasing : (a : Sequence A) → WeaklyIncreasing (makeIncreasing a)
makeIncreasingIsIncreasing a zero with totality (Sequence.head a) (Sequence.head (Sequence.tail a))
... | inl (inl x) = inl x
... | inl (inr x) = inr reflexive
... | inr x = inr reflexive
makeIncreasingIsIncreasing a (succ m) = makeIncreasingLemmaIsIncreasing _ _ m

approximateIncreasingSeqRaw : CauchyCompletion → Sequence A
approximateIncreasingSeqRaw a = funcToSequence f
  where
    f : ℕ → A
    f n with allInvertible (fromN (succ n)) λ n=0 → irreflexive (<WellDefined reflexive n=0 (fromNPreservesOrder (0<1 nontrivial) (succIsPositive n)))
    ... | 1/n , prN = underlying (approximateBelow a 1/n (reciprocalPositive' (fromN (succ n)) 1/n (fromNPreservesOrder (0<1 nontrivial) (succIsPositive n)) prN))

approximateIncreasingSeq : CauchyCompletion → Sequence A
approximateIncreasingSeq a = makeIncreasing (approximateIncreasingSeqRaw a)

approximateIncreasingConverges : (a : CauchyCompletion) → cauchy (approximateIncreasingSeq a)
approximateIncreasingConverges a e 0<e = {!!}

approximateIncreasingIncreases : (a : CauchyCompletion) → WeaklyIncreasing (approximateIncreasingSeq a)
approximateIncreasingIncreases a = makeIncreasingIsIncreasing (approximateIncreasingSeqRaw a)

approximateIncreasing : CauchyCompletion → CauchyCompletion
approximateIncreasing a = record { elts = approximateIncreasingSeq a ; converges = approximateIncreasingConverges a }

approximateIncreasingEqual : (a : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid (approximateIncreasing a) a
approximateIncreasingEqual a e 0<e = {!!}

decideSign : (a : CauchyCompletion) → (Setoid._∼_ cauchyCompletionSetoid a (injection 0R) → False) → (a <Cr 0R) || (0R r<C a)
decideSign a a!=0 = {!!}
  where

private
  lemma : (a b : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid ((b +C (-C a)) +C a) b
  lemma a b = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((b +C (-C a)) +C a) }} {record { converges = CauchyCompletion.converges (b +C ((-C a) +C a)) }} {record { converges = CauchyCompletion.converges b }} (Group.+Associative' CGroup {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges (-C a) }} { record { converges = CauchyCompletion.converges a }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record {converges = CauchyCompletion.converges (b +C ((-C a) +C a))}} {record { converges = CauchyCompletion.converges (b +C (injection 0R))}} {record {converges = CauchyCompletion.converges b}} (Group.+WellDefinedRight CGroup {record {converges = CauchyCompletion.converges b}} {record {converges = CauchyCompletion.converges ((-C a) +C a)}} {record { converges = CauchyCompletion.converges (injection 0R)}} (Group.invLeft CGroup {record { converges = CauchyCompletion.converges a }})) (Group.identRight CGroup {record { converges = CauchyCompletion.converges b }}))

nearlyTotal : (a b : CauchyCompletion) → (Setoid._∼_ cauchyCompletionSetoid a b → False) → (a <C b) || (b <C a)
nearlyTotal a b a!=b with decideSign (b +C (-C a)) λ bad → a!=b (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges a  }} (transferToRight CGroup {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges a }} bad))
... | inl x = inr (<CWellDefined (lemma a b) (Group.identLeft CGroup {record { converges = CauchyCompletion.converges a }}) (PartiallyOrderedRing.orderRespectsAddition CpOrderedRing (<CRelaxR x) a))
... | inr x = inl (<CWellDefined (Group.identLeft CGroup {record { converges = CauchyCompletion.converges a }}) (lemma a b) (PartiallyOrderedRing.orderRespectsAddition CpOrderedRing (<CRelaxL x) a))


text:
------------------------------------------------------------------------
-- Identity and composition for higher lenses
------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

import Equality.Path as P

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

open P.Derived-definitions-and-properties eq

import Bi-invertibility
open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)

open import Bijection equality-with-J as Bij using (_↔_)
open import Category equality-with-J as C using (Category; Precategory)
import Circle eq as Circle
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
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 Trunc
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent.Higher eq
import Lens.Non-dependent.Traditional eq as Traditional
open import Lens.Non-dependent.Traditional.Combinators eq as TC
  using (Naive-category; Univalent)

private
  variable
    a b c d : Level
    A B C   : Type a

------------------------------------------------------------------------
-- Lens combinators

-- The definition of the identity lens is unique, if the get
-- function is required to be the identity (assuming univalence).

id-unique :
  {A : Type a} →
  Univalence a →
  (l₁ l₂ : Lens A A) →
  Lens.get l₁ ≡ P.id →
  Lens.get l₂ ≡ P.id →
  l₁ ≡ l₂
id-unique {A = A} univ l₁ l₂ get-l₁≡id get-l₂≡id =   $⟨ trans get-l₁≡id (sym get-l₂≡id) ⟩
  _≃_.to (_≃_.from f l₁′) ≡ _≃_.to (_≃_.from f l₂′)  ↝⟨ Eq.lift-equality ext ⟩
  _≃_.from f l₁′ ≡ _≃_.from f l₂′                    ↝⟨ _≃_.to $ Eq.≃-≡ (inverse f) {x = l₁′} {y = l₂′} ⟩
  l₁′ ≡ l₂′                                          ↝⟨ cong proj₁ ⟩□
  l₁ ≡ l₂                                            □
  where
  open Lens

  f : (A ≃ A) ≃ (∃ λ (l : Lens A A) → Is-equivalence (Lens.get l))
  f = ≃-≃-Σ-Lens-Is-equivalence-get univ

  is-equiv :
    (l : Lens A A) →
    get l ≡ P.id → Is-equivalence (get l)
  is-equiv _ get≡id =
    Eq.respects-extensional-equality
      (ext⁻¹ $ sym get≡id)
      (_≃_.is-equivalence Eq.id)

  l₁′ l₂′ : ∃ λ (l : Lens A A) → Is-equivalence (Lens.get l)
  l₁′ = l₁ , is-equiv l₁ get-l₁≡id
  l₂′ = l₂ , is-equiv l₂ get-l₂≡id

-- The result of composing two lenses is unique if the codomain type
-- is inhabited whenever it is merely inhabited, and we require that
-- the resulting setter function is defined in a certain way
-- (assuming univalence).

∘-unique :
  let open Lens in
  {A : Type a} {C : Type c} →
  Univalence (a ⊔ c) →
  (∥ C ∥ → C) →
  ((comp₁ , _) (comp₂ , _) :
     ∃ λ (comp : Lens B C → Lens A B → Lens A C) →
       ∀ l₁ l₂ a c →
         set (comp l₁ l₂) a c ≡ set l₂ a (set l₁ (get l₂ a) c)) →
  comp₁ ≡ comp₂
∘-unique {A = A} {C = C} univ ∥C∥→C
         (comp₁ , set₁) (comp₂ , set₂) =
  ⟨ext⟩ λ l₁ → ⟨ext⟩ λ l₂ →
    lenses-equal-if-setters-equal univ
      (comp₁ l₁ l₂) (comp₂ l₁ l₂) (λ _ → ∥C∥→C) $
      ⟨ext⟩ λ a → ⟨ext⟩ λ c →
        set (comp₁ l₁ l₂) a c           ≡⟨ set₁ _ _ _ _ ⟩
        set l₂ a (set l₁ (get l₂ a) c)  ≡⟨ sym $ set₂ _ _ _ _ ⟩∎
        set (comp₂ l₁ l₂) a c           ∎
  where
  open Lens

-- Identity lens.

id : Block "id" → Lens A A
id {A = A} ⊠ = record
  { R         = ∥ A ∥
  ; equiv     = A          ↔⟨ inverse ∥∥×↔ ⟩□
                ∥ A ∥ × A  □
  ; inhabited = P.id
  }

-- Composition of lenses.
--
-- Note that the domains are required to be at least as large as the
-- codomains; this should match many use-cases. Without this
-- restriction I failed to find a satisfactory definition of
-- composition. (I suspect that if Agda had had cumulativity, then
-- the domain and codomain could have lived in the same universe
-- without any problems.)
--
-- The composition operation matches on the lenses to ensure that it
-- does not unfold when applied to neutral lenses.
--
-- See also Lens.Non-dependent.Equivalent-preimages.⟨_⟩_⊚_.

infix 9 ⟨_,_⟩_∘_

⟨_,_⟩_∘_ :
  ∀ a b {A : Type (a ⊔ b ⊔ c)} {B : Type (b ⊔ c)} {C : Type c} →
  Lens B C → Lens A B → Lens A C
⟨_,_⟩_∘_ _ _ {A = A} {B} {C} l₁@(⟨ _ , _ , _ ⟩) l₂@(⟨ _ , _ , _ ⟩) =
  record
    { R         = R l₂ × R l₁
    ; equiv     = A                  ↝⟨ equiv l₂ ⟩
                  R l₂ × B           ↝⟨ F.id ×-cong equiv l₁ ⟩
                  R l₂ × (R l₁ × C)  ↔⟨ ×-assoc ⟩□
                  (R l₂ × R l₁) × C  □
    ; inhabited = ∥∥-map (get l₁) ⊚ inhabited l₂ ⊚ proj₁
    }
  where
  open Lens

-- The composition operation implements set in a certain way.

∘-set :
  let open Lens in
  ∀ ℓa ℓb {A : Type (ℓa ⊔ ℓb ⊔ c)} {B : Type (ℓb ⊔ c)} {C : Type c}
  (l₁ : Lens B C) (l₂ : Lens A B) a c →
  set (⟨ ℓa , ℓb ⟩ l₁ ∘ l₂) a c ≡ set l₂ a (set l₁ (get l₂ a) c)
∘-set _ _ ⟨ _ , _ , _ ⟩ ⟨ _ , _ , _ ⟩ _ _ = refl _

-- A variant of composition for lenses between types with the same
-- universe level.

infixr 9 _∘_

_∘_ :
  {A B C : Type a} →
  Lens B C → Lens A B → Lens A C
l₁ ∘ l₂ = ⟨ lzero , lzero ⟩ l₁ ∘ l₂

-- Other definitions of composition match ⟨_,_⟩_∘_, if the codomain
-- type is inhabited whenever it is merely inhabited, and the
-- resulting setter function is defined in a certain way (assuming
-- univalence).

composition≡∘ :
  let open Lens in
  ∀ a b {A : Type (a ⊔ b ⊔ c)} {B : Type (b ⊔ c)} {C : Type c} →
  Univalence (a ⊔ b ⊔ c) →
  (∥ C ∥ → C) →
  (comp : Lens B C → Lens A B → Lens A C) →
  (∀ l₁ l₂ a c →
     set (comp l₁ l₂) a c ≡ set l₂ a (set l₁ (get l₂ a) c)) →
  comp ≡ ⟨ a , b ⟩_∘_
composition≡∘ _ _ univ ∥C∥→C comp set-comp =
  ∘-unique univ ∥C∥→C (comp , set-comp)
    (_ , λ { ⟨ _ , _ , _ ⟩ ⟨ _ , _ , _ ⟩ _ _ → refl _ })

-- Identity and composition form a kind of precategory (assuming
-- univalence).

associativity :
  ∀ a b c
    {A : Type (a ⊔ b ⊔ c ⊔ d)} {B : Type (b ⊔ c ⊔ d)}
    {C : Type (c ⊔ d)} {D : Type d} →
  Univalence (a ⊔ b ⊔ c ⊔ d) →
  (l₁ : Lens C D) (l₂ : Lens B C) (l₃ : Lens A B) →
  ⟨ a ⊔ b , c ⟩ l₁ ∘ (⟨ a , b ⟩ l₂ ∘ l₃) ≡
  ⟨ a , b ⊔ c ⟩ (⟨ b , c ⟩ l₁ ∘ l₂) ∘ l₃
associativity _ _ _ univ ⟨ _ , _ , _ ⟩ ⟨ _ , _ , _ ⟩ ⟨ _ , _ , _ ⟩ =
  _↔_.from (equality-characterisation₁ ⊠ univ)
           (Eq.↔⇒≃ (inverse ×-assoc) , λ _ → refl _)

left-identity :
  ∀ bi a {A : Type (a ⊔ b)} {B : Type b} →
  Univalence (a ⊔ b) →
  (l : Lens A B) →
  ⟨ a , lzero ⟩ id bi ∘ l ≡ l
left-identity ⊠ _ {B = B} univ l@(⟨ _ , _ , _ ⟩) =
  _↔_.from (equality-characterisation₁ ⊠ univ)
    ( (R × ∥ B ∥  ↔⟨ lemma ⟩□
       R          □)
    , λ _ → refl _
    )
  where
  open Lens l

  lemma : R × ∥ B ∥ ↔ R
  lemma = record
    { surjection = record
      { logical-equivalence = record
        { to   = proj₁
        ; from = λ r → r , inhabited r
        }
      ; right-inverse-of = refl
      }
    ; left-inverse-of = λ { (r , _) →
        cong (λ x → r , x) $ truncation-is-proposition _ _ }
    }

right-identity :
  ∀ bi a {A : Type (a ⊔ b)} {B : Type b} →
  Univalence (a ⊔ b) →
  (l : Lens A B) →
  ⟨ lzero , a ⟩ l ∘ id bi ≡ l
right-identity ⊠ _ {A = A} univ l@(⟨ _ , _ , _ ⟩) =
  _↔_.from (equality-characterisation₁ ⊠ univ)
    ( (∥ A ∥ × R  ↔⟨ lemma ⟩□
       R          □)
    , λ _ → refl _
    )
  where
  open Lens l

  lemma : ∥ A ∥ × R ↔ R
  lemma = record
    { surjection = record
      { logical-equivalence = record
        { to   = proj₂
        ; from = λ r →   ∥∥-map (λ b → _≃_.from equiv (r , b))
                                (inhabited r)
                       , r
        }
      ; right-inverse-of = refl
      }
    ; left-inverse-of = λ { (_ , r) →
        cong (λ x → x , r) $ truncation-is-proposition _ _ }
    }

------------------------------------------------------------------------
-- Isomorphisms expressed using lens quasi-inverses

private
  module B {a} (b : Block "id") =
    Bi-invertibility equality-with-J (Type a) Lens (id b) _∘_
  module BM {a} (b : Block "id") (univ : Univalence a) = B.More
    b
    (left-identity b _ univ)
    (right-identity b _ univ)
    (associativity _ _ _ univ)

-- A form of isomorphism between types, expressed using lenses.

open B public
  using ()
  renaming (_≅_ to [_]_≅_;
            Has-quasi-inverse to Has-quasi-inverse)

-- Lenses with quasi-inverses can be converted to equivalences.

≅→≃ : ∀ b → [ b ] A ≅ B → A ≃ B
≅→≃
  ⊠
  (l@(⟨ _ , _ , _ ⟩) , l⁻¹@(⟨ _ , _ , _ ⟩) , l∘l⁻¹≡id , l⁻¹∘l≡id) =
  Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = get l
        ; from = get l⁻¹
        }
      ; right-inverse-of = λ b → cong (λ l → get l b) l∘l⁻¹≡id
      }
    ; left-inverse-of = λ a → cong (λ l → get l a) l⁻¹∘l≡id
    })
  where
  open Lens

-- There is a split surjection from [ b ] A ≅ B to A ≃ B (assuming
-- univalence).

≅↠≃ :
  {A B : Type a}
  (b : Block "id") →
  Univalence a →
  ([ b ] A ≅ B) ↠ (A ≃ B)
≅↠≃ {A = A} {B = B} b univ = record
  { logical-equivalence = record
    { to   = ≅→≃ b
    ; from = from b
    }
  ; right-inverse-of = ≅→≃∘from b
  }
  where
  from : ∀ b → A ≃ B → [ b ] A ≅ B
  from b A≃B = l , l⁻¹ , l∘l⁻¹≡id b , l⁻¹∘l≡id b
    where
    l   = ≃→lens′ A≃B
    l⁻¹ = ≃→lens′ (inverse A≃B)

    l∘l⁻¹≡id : ∀ b → l ∘ l⁻¹ ≡ id b
    l∘l⁻¹≡id ⊠ = _↔_.from (equality-characterisation₁ ⊠ univ)
      ( (∥ A ∥ × ∥ B ∥  ↝⟨ Eq.⇔→≃
                             (×-closure 1 truncation-is-proposition
                                          truncation-is-proposition)
                             truncation-is-proposition
                             proj₂
                             (λ b → ∥∥-map (_≃_.from A≃B) b , b) ⟩
         ∥ B ∥          □)
      , λ _ → cong₂ _,_
               (truncation-is-proposition _ _)
               (_≃_.right-inverse-of A≃B _)
      )

    l⁻¹∘l≡id : ∀ b → l⁻¹ ∘ l ≡ id b
    l⁻¹∘l≡id ⊠ = _↔_.from (equality-characterisation₁ ⊠ univ)
      ( (∥ B ∥ × ∥ A ∥  ↝⟨ Eq.⇔→≃
                             (×-closure 1 truncation-is-proposition
                                          truncation-is-proposition)
                             truncation-is-proposition
                             proj₂
                             (λ a → ∥∥-map (_≃_.to A≃B) a , a) ⟩
         ∥ A ∥          □)
      , λ _ → cong₂ _,_
                (truncation-is-proposition _ _)
                (_≃_.left-inverse-of A≃B _)
      )

  ≅→≃∘from : ∀ b A≃B → ≅→≃ b (from b A≃B) ≡ A≃B
  ≅→≃∘from ⊠ _ = Eq.lift-equality ext (refl _)

-- There is not necessarily a split surjection from
-- Is-equivalence (Lens.get l) to Has-quasi-inverse l, if l is a
-- lens between types in the same universe (assuming univalence).

¬Is-equivalence-get↠Has-quasi-inverse :
  (b : Block "id") →
  Univalence a →
  ¬ ({A B : Type a}
     (l : Lens A B) →
     Is-equivalence (Lens.get l) ↠ Has-quasi-inverse b l)
¬Is-equivalence-get↠Has-quasi-inverse b univ surj =
                                    $⟨ ⊤-contractible ⟩
  Contractible ⊤                    ↝⟨ H-level.respects-surjection lemma₃ 0 ⟩
  Contractible ((z : Z) → z ≡ z)    ↝⟨ mono₁ 0 ⟩
  Is-proposition ((z : Z) → z ≡ z)  ↝⟨ ¬-prop ⟩□
  ⊥                                 □
  where
  open Lens

  Z,¬-prop = Circle.¬-type-of-refl-propositional
  Z        = proj₁ Z,¬-prop
  ¬-prop   = proj₂ Z,¬-prop

  lemma₂ :
    ∀ b →
    (∃ λ (eq : R (id b) ≃ R (id b)) →
       (∀ z → _≃_.to eq (remainder (id b) z) ≡ remainder (id b) z)
         ×
       ((z : Z) → get (id b) z ≡ get (id b) z)) ≃
    ((z : Z) → z ≡ z)
  lemma₂ ⊠ =
    (∃ λ (eq : ∥ Z ∥ ≃ ∥ Z ∥) →
       ((z : Z) → _≃_.to eq ∣ z ∣ ≡ ∣ z ∣)
         ×
       ((z : Z) → z ≡ z))                   ↔⟨ (∃-cong λ _ → drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                                                Π-closure ext 0 λ _ →
                                                +⇒≡ truncation-is-proposition) ⟩

    (∥ Z ∥ ≃ ∥ Z ∥) × ((z : Z) → z ≡ z)     ↔⟨ drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                                               propositional⇒inhabited⇒contractible
                                                 (Eq.left-closure ext 0 truncation-is-proposition)
                                                 F.id ⟩□
    ((z : Z) → z ≡ z)                       □

  lemma₃ =
    ⊤                                                               ↔⟨ inverse $ _⇔_.to contractible⇔↔⊤ $
                                                                       propositional⇒inhabited⇒contractible
                                                                         (Eq.propositional ext _)
                                                                         (_≃_.is-equivalence Eq.id) ⟩

    Is-equivalence P.id                                             ↔⟨ ≡⇒↝ equivalence $ cong Is-equivalence $
                                                                       unblock b (λ b → _ ≡ get (id b)) (refl _) ⟩

    Is-equivalence (get (id b))                                     ↝⟨ surj (id b) ⟩

    Has-quasi-inverse b (id b)                                      ↔⟨ BM.Has-quasi-inverse≃id≡id-domain b univ
                                                                         (id b , left-identity b _ univ _ , right-identity b _ univ _) ⟩

    id b ≡ id b                                                     ↔⟨ equality-characterisation₂ ⊠ univ ⟩

    (∃ λ (eq : R (id b) ≃ R (id b)) →
       (∀ z → _≃_.to eq (remainder (id b) z) ≡ remainder (id b) z)
         ×
       (∀ z → get (id b) z ≡ get (id b) z))                         ↔⟨ lemma₂ b ⟩□

    ((z : Z) → z ≡ z)                                               □

-- See also ≃≃≅ below.

------------------------------------------------------------------------
-- Equivalences expressed using bi-invertibility for lenses

-- A form of equivalence between types, expressed using lenses.

open B public
  using ()
  renaming (_≊_ to [_]_≊_;
            Has-left-inverse to Has-left-inverse;
            Has-right-inverse to Has-right-inverse;
            Is-bi-invertible to Is-bi-invertible)
open BM public
  using ()
  renaming (equality-characterisation-≊ to equality-characterisation-≊)

-- Lenses with left inverses have propositional remainder types.

has-left-inverse→remainder-propositional :
  (b : Block "id")
  (l : Lens A B) →
  Has-left-inverse b l →
  Is-proposition (Lens.R l)
has-left-inverse→remainder-propositional
  ⊠ l@(⟨ _ , _ , _ ⟩) (l⁻¹@(⟨ _ , _ , _ ⟩) , l⁻¹∘l≡id) =
                                $⟨ get≡id→remainder-propositional
                                     (l⁻¹ ∘ l)
                                     (λ a → cong (flip get a) l⁻¹∘l≡id) ⟩
  Is-proposition (R (l⁻¹ ∘ l))  ↔⟨⟩
  Is-proposition (R l × R l⁻¹)  ↝⟨ H-level-×₁ (∥∥-map (remainder l⁻¹) ⊚ inhabited l) 1 ⟩□
  Is-proposition (R l)          □
  where
  open Lens

-- Lenses with right inverses have propositional remainder types.

has-right-inverse→remainder-propositional :
  (b : Block "id")
  (l : Lens A B) →
  Has-right-inverse b l →
  Is-proposition (Lens.R l)
has-right-inverse→remainder-propositional
  ⊠ l@(⟨ _ , _ , _ ⟩) (l⁻¹@(⟨ _ , _ , _ ⟩) , l∘l⁻¹≡id) =
                                $⟨ get≡id→remainder-propositional
                                     (l ∘ l⁻¹)
                                     (λ a → cong (flip get a) l∘l⁻¹≡id) ⟩
  Is-proposition (R (l ∘ l⁻¹))  ↔⟨⟩
  Is-proposition (R l⁻¹ × R l)  ↝⟨ H-level-×₂ (∥∥-map (remainder l⁻¹) ⊚ inhabited l) 1 ⟩□
  Is-proposition (R l)          □
  where
  open Lens

-- There is an equivalence between A ≃ B and [ b ] A ≊ B (assuming
-- univalence).

≃≃≊ :
  {A B : Type a}
  (b : Block "id") →
  Univalence a →
  (A ≃ B) ≃ ([ b ] A ≊ B)
≃≃≊ {A = A} {B = B} b univ = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = to b
      ; from = from b
      }
    ; right-inverse-of = to∘from b
    }
  ; left-inverse-of = from∘to b
  })
  where
  open Lens

  to : ∀ b → A ≃ B → [ b ] A ≊ B
  to b = B.≅→≊ b ⊚ _↠_.from (≅↠≃ b univ)

  from : ∀ b → [ b ] A ≊ B → A ≃ B
  from b = _↠_.to (≅↠≃ b univ) ⊚ _↠_.from (BM.≅↠≊ b univ)

  to∘from : ∀ b A≊B → to b (from b A≊B) ≡ A≊B
  to∘from b A≊B =
    _≃_.from (equality-characterisation-≊ b univ _ _) $
    _↔_.from (equality-characterisation₂ b univ)
      ( ∥B∥≃R  b A≊B
      , lemma₁ b A≊B
      , lemma₂ b A≊B
      )
    where
    l′ : ∀ b (A≊B : [ b ] A ≊ B) → Lens A B
    l′ b A≊B = proj₁ (to b (from b A≊B))

    ∥B∥≃R : ∀ b (A≊B@(l , _) : [ b ] A ≊ B) → ∥ B ∥ ≃ R l
    ∥B∥≃R b (l , (l-inv@(l⁻¹ , _) , _)) = Eq.⇔→≃
      truncation-is-proposition
      R-prop
      (Trunc.rec R-prop (remainder l ⊚ get l⁻¹))
      (inhabited l)
      where
      R-prop = has-left-inverse→remainder-propositional b l l-inv

    lemma₁ :
      ∀ b (A≊B@(l , _) : [ b ] A ≊ B) a →
      _≃_.to (∥B∥≃R b A≊B) (remainder (l′ b A≊B) a) ≡ remainder l a
    lemma₁
      ⊠
      ( l@(⟨ _ , _ , _ ⟩)
      , (l⁻¹@(⟨ _ , _ , _ ⟩) , l⁻¹∘l≡id)
      , (⟨ _ , _ , _ ⟩ , _)
      ) a =
      remainder l (get l⁻¹ (get l a))  ≡⟨⟩
      remainder l (get (l⁻¹ ∘ l) a)    ≡⟨ cong (λ l′ → remainder l (get l′ a)) l⁻¹∘l≡id ⟩
      remainder l (get (id ⊠) a)       ≡⟨⟩
      remainder l a                    ∎

    lemma₂ :
      ∀ b (A≊B@(l , _) : [ b ] A ≊ B) a →
      get (l′ b A≊B) a ≡ get l a
    lemma₂ ⊠
      (⟨ _ , _ , _ ⟩ , (⟨ _ , _ , _ ⟩ , _) , (⟨ _ , _ , _ ⟩ , _)) _ =
      refl _

  from∘to :
    ∀ b A≃B →
    _↠_.to (≅↠≃ b univ) (_↠_.from (BM.≅↠≊ b univ)
      (B.≅→≊ b (_↠_.from (≅↠≃ b univ) A≃B))) ≡
    A≃B
  from∘to ⊠ _ = Eq.lift-equality ext (refl _)

-- The right-to-left direction of ≃≃≊ maps bi-invertible lenses to
-- their getter functions.

to-from-≃≃≊≡get :
  (b : Block "id")
  (univ : Univalence a)
  (A≊B@(l , _) : [ b ] A ≊ B) →
  _≃_.to (_≃_.from (≃≃≊ b univ) A≊B) ≡ Lens.get l
to-from-≃≃≊≡get
  ⊠ _ (⟨ _ , _ , _ ⟩ , (⟨ _ , _ , _ ⟩ , _) , (⟨ _ , _ , _ ⟩ , _)) =
  refl _

-- A variant of ≃≃≊ that works even if A and B live in different
-- universes.
--
-- This variant came up in a discussion with Andrea Vezzosi.

≃≃≊′ :
  {A : Type a} {B : Type b}
  (b-id : Block "id") →
  Univalence (a ⊔ b) →
  (A ≃ B) ≃ ([ b-id ] ↑ b A ≊ ↑ a B)
≃≃≊′ {a = a} {b = b} {A = A} {B = B} b-id univ =
  A ≃ B                   ↔⟨ inverse $ Eq.≃-preserves-bijections ext Bij.↑↔ Bij.↑↔ ⟩
  ↑ b A ≃ ↑ a B           ↝⟨ ≃≃≊ b-id univ ⟩□
  [ b-id ] ↑ b A ≊ ↑ a B  □

-- The right-to-left direction of ≃≃≊′ maps bi-invertible lenses to a
-- variant of their getter functions.

to-from-≃≃≊′≡get :
  {A : Type a} {B : Type b}
  (b-id : Block "id")
  (univ : Univalence (a ⊔ b)) →
  (A≊B@(l , _) : [ b-id ] ↑ b A ≊ ↑ a B) →
  _≃_.to (_≃_.from (≃≃≊′ b-id univ) A≊B) ≡ lower ⊚ Lens.get l ⊚ lift
to-from-≃≃≊′≡get
  ⊠ _ (⟨ _ , _ , _ ⟩ , (⟨ _ , _ , _ ⟩ , _) , (⟨ _ , _ , _ ⟩ , _)) =
  refl _

-- The getter function of a bi-invertible lens is an equivalence
-- (assuming univalence).

Is-bi-invertible→Is-equivalence-get :
  {A : Type a}
  (b : Block "id") →
  Univalence a →
  (l : Lens A B) →
  Is-bi-invertible b l → Is-equivalence (Lens.get l)
Is-bi-invertible→Is-equivalence-get
  b@⊠ univ l@(⟨ _ , _ , _ ⟩)
  is-bi-inv@((⟨ _ , _ , _ ⟩ , _) , (⟨ _ , _ , _ ⟩ , _)) =
  _≃_.is-equivalence (_≃_.from (≃≃≊ b univ) (l , is-bi-inv))

-- If l is a lens between types in the same universe, then there is an
-- equivalence between "l is bi-invertible" and "the getter of l is an
-- equivalence" (assuming univalence).

Is-bi-invertible≃Is-equivalence-get :
  {A B : Type a}
  (b : Block "id") →
  Univalence a →
  (l : Lens A B) →
  Is-bi-invertible b l ≃ Is-equivalence (Lens.get l)
Is-bi-invertible≃Is-equivalence-get b univ l = Eq.⇔→≃
  (BM.Is-bi-invertible-propositional b univ l)
  (Eq.propositional ext _)
  (Is-bi-invertible→Is-equivalence-get b univ l)
  (λ is-equiv →

     let l′ = ≃→lens′ Eq.⟨ get l , is-equiv ⟩ in

                            $⟨ proj₂ (_≃_.to (≃≃≊ b univ) Eq.⟨ _ , is-equiv ⟩) ⟩
     Is-bi-invertible b l′  ↝⟨ subst (Is-bi-invertible b) (sym $ get-equivalence→≡≃→lens′ univ l is-equiv) ⟩□
     Is-bi-invertible b l   □)
  where
  open Lens

-- If A is a set, then there is an equivalence between [ b ] A ≊ B and
-- [ b ] A ≅ B (assuming univalence).

≊≃≅ :
  {A B : Type a}
  (b : Block "id") →
  Univalence a →
  Is-set A →
  ([ b ] A ≊ B) ≃ ([ b ] A ≅ B)
≊≃≅ b univ A-set =
  ∃-cong λ _ →
    BM.Is-bi-invertible≃Has-quasi-inverse-domain
      b univ
      (Is-set-closed-domain univ A-set)

------------------------------------------------------------------------
-- A category

-- If A is a set, then there is an equivalence between A ≃ B and
-- [ b ] A ≅ B (assuming univalence).

≃≃≅ :
  {A B : Type a}
  (b : Block "≃≃≅") →
  Univalence a →
  Is-set A →
  (A ≃ B) ≃ ([ b ] A ≅ B)
≃≃≅ {A = A} {B = B} b@⊠ univ A-set =
  A ≃ B        ↝⟨ ≃≃≊ b univ ⟩
  [ b ] A ≊ B  ↝⟨ ≊≃≅ b univ A-set ⟩□
  [ b ] A ≅ B  □

-- The equivalence ≃≃≅ maps identity to identity.

≃≃≅-id≡id :
  {A : Type a}
  (b : Block "≃≃≅") (univ : Univalence a) (A-set : Is-set A) →
  proj₁ (_≃_.to (≃≃≅ b univ A-set) F.id) ≡ id b
≃≃≅-id≡id ⊠ univ _ =
  _↔_.from (equality-characterisation₁ ⊠ univ)
    (F.id , λ _ → refl _)

-- Lenses between sets in the same universe form a precategory
-- (assuming univalence).

private

  precategory′ :
    Block "id" →
    Univalence a →
    C.Precategory′ (lsuc a) (lsuc a)
  precategory′ {a = a} b univ =
      Set a
    , (λ (A , A-set) (B , _) →
           Lens A B
         , Is-set-closed-domain univ A-set)
    , id b
    , _∘_
    , left-identity b lzero univ _
    , right-identity b lzero univ _
    , (λ {_ _ _ _ l₁ l₂ l₃} →
         associativity lzero lzero lzero univ l₃ l₂ l₁)

precategory :
  Block "precategory" →
  Univalence a →
  Precategory (lsuc a) (lsuc a)
precategory ⊠ univ .C.Precategory.precategory =
  block λ b → precategory′ b univ

-- Lenses between sets in the same universe form a category
-- (assuming univalence).

category :
  Block "category" →
  Univalence a →
  Category (lsuc a) (lsuc a)
category ⊠ univ =
  block λ b →
  C.precategory-with-Set-to-category
    ext
    (λ _ _ → univ)
    (proj₂ $ precategory′ b univ)
    (λ (_ , A-set) _ → ≃≃≅ b univ A-set)
    (λ (_ , A-set) → ≃≃≅-id≡id b univ A-set)

-- The precategory defined here is equal to the one defined in
-- Traditional, if the latter one is lifted (assuming univalence).

precategory≡precategory :
  (b : Block "precategory") →
  Univalence (lsuc a) →
  (univ : Univalence a) →
  precategory b univ ≡
  C.lift-precategory-Hom _ TC.precategory
precategory≡precategory ⊠ univ⁺ univ =
  block λ b →
  _↔_.to (C.equality-characterisation-Precategory ext univ⁺ univ⁺)
    ( F.id
    , (λ (X , X-set) (Y , _) →
         Lens X Y                    ↔⟨ Lens↔Traditional-lens b univ X-set ⟩
         Traditional.Lens X Y        ↔⟨ inverse Bij.↑↔ ⟩□
         ↑ _ (Traditional.Lens X Y)  □)
    , (λ (_ , X-set) → cong lift $ _↔_.from
         (Traditional.equality-characterisation-for-sets X-set)
         (refl _))
    , (λ (_ , X-set) (_ , Y-set) _ (lift l₁) (lift l₂) →
         cong lift (∘-lemma b X-set Y-set l₁ l₂))
    )
  where
  ∘-lemma :
    ∀ b (A-set : Is-set A) (B-set : Is-set B)
    (l₁ : Traditional.Lens B C) (l₂ : Traditional.Lens A B) →
    Lens.traditional-lens
      (_↠_.from (Lens↠Traditional-lens b B-set) l₁ ∘
       _↠_.from (Lens↠Traditional-lens b A-set) l₂) ≡
    l₁ TC.∘ l₂
  ∘-lemma ⊠ A-set _ _ _ =
    _↔_.from (Traditional.equality-characterisation-for-sets A-set)
      (refl _)

-- The category defined here is equal to the one defined in
-- Traditional, if the latter one is lifted (assuming univalence).

category≡category :
  (b : Block "category") →
  Univalence (lsuc a) →
  (univ : Univalence a) →
  category b univ ≡
  C.lift-category-Hom _ (TC.category univ)
category≡category b univ⁺ univ =
  _↔_.from (C.≡↔precategory≡precategory ext)
    (Category.precategory (category b univ)        ≡⟨ lemma b ⟩

     precategory b univ                            ≡⟨ precategory≡precategory b univ⁺ univ ⟩∎

     Category.precategory
       (C.lift-category-Hom _ (TC.category univ))  ∎)
  where
  lemma :
    ∀ b →
    Category.precategory (category b univ) ≡
    precategory b univ
  lemma ⊠ = refl _

-- Types in a fixed universe and higher lenses between them form a
-- naive category (assuming univalence).

naive-category :
  Block "id" →
  Univalence a →
  Naive-category (lsuc a) (lsuc a)
naive-category {a = a} b univ =
    Type a
  , Lens
  , id b
  , _∘_
  , left-identity b lzero univ
  , right-identity b lzero univ
  , associativity lzero lzero lzero univ

-- This category is univalent.
--
-- An anonymous reviewer asked if something like this could be proved,
-- given ≃≃≊. The proof of this result is due to Andrea Vezzosi.

univalent :
  (b : Block "id")
  (univ : Univalence a) →
  Univalent (naive-category b univ)
univalent b univ =
  BM.≡≃≊→Univalence-≊ b univ λ {A B} →
    A ≡ B        ↝⟨ ≡≃≃ univ ⟩
    A ≃ B        ↝⟨ ≃≃≊ b univ ⟩□
    [ b ] A ≊ B  □

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
------------------------------------------------------------------------------
-- Common stuff used by the gcd example
------------------------------------------------------------------------------

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

module LTC-PCF.Program.GCD.Partial.Definitions where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat.Divisibility.NotBy0
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Type

------------------------------------------------------------------------------
-- Common divisor.
CD : D → D → D → Set
CD m n cd = cd ∣ m ∧ cd ∣ n

-- Divisible for any common divisor.
Divisible : D → D → D → Set
Divisible m n gcd = ∀ cd → N cd → CD m n cd → cd ∣ gcd

-- Greatest that any common divisor.
GACD : D → D → D → Set
GACD m n gcd = ∀ cd → N cd → CD m n cd → cd ≤ gcd

-- Greatest common divisor specification.
gcdSpec : D → D → D → Set
gcdSpec m n gcd = CD m n gcd ∧ GACD m n gcd

x≢0≢y : D → D → Set
x≢0≢y m n = ¬ (m ≡ zero ∧ n ≡ zero)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

open import Data.Product
open import Data.Empty
open import Data.Sum
open import Data.Vec
open import Data.Fin
open import Data.Bool renaming (Bool to 𝔹)
open import Relation.Unary using (_∈_; _⊆_; _∉_)
open import Relation.Binary.Definitions
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

open import Common

open import is-lib.InfSys

module FairCompliance-IS {𝕋 : Set} (message : Message 𝕋) where

  open import SessionType message
  open import Session message
  open import Transitions message

  private
    U : Set
    U = SessionType × SessionType

  data FCompIS-RN : Set where
    client-end : FCompIS-RN
    oi io : FCompIS-RN

  data FCompCOIS-RN : Set where
    co-oi co-io : FCompCOIS-RN

  client-end-r : FinMetaRule U
  client-end-r .Ctx = Σ[ (S , T) ∈ SessionType × SessionType ] Win S × Defined T
  client-end-r .comp ((S , T) , _) =
    [] ,
    --------------------
    (S , T)

  OI-r : MetaRule U
  OI-r .Ctx = Σ[ (f , _) ∈ Continuation × Continuation ] Witness f
  OI-r .Pos ((f , _) , _) = Σ[ t ∈ 𝕋 ] t ∈ dom f
  OI-r .prems ((f , g) , _) (t , _) = f t .force , g t .force
  OI-r .conclu ((f , g) , _) = out f , inp g

  IO-r : MetaRule U
  IO-r .Ctx = Σ[ (_ , g) ∈ Continuation × Continuation ] Witness g
  IO-r .Pos ((_ , g) , _) = Σ[ t ∈ 𝕋 ] t ∈ dom g
  IO-r .prems ((f , g) , _) (t , _) = f t .force , g t .force
  IO-r .conclu ((f , g) , _) = inp f , out g

  co-OI-r : FinMetaRule U
  co-OI-r .Ctx = Σ[ (f , _ , x) ∈ Continuation × Continuation × 𝕋 ] x ∈ dom f
  co-OI-r .comp ((f , g , x) , _) =
    (f x .force , g x .force) ∷ [] ,
    --------------------
    (out f , inp g)

  co-IO-r : FinMetaRule U
  co-IO-r .Ctx = Σ[ (_ , g , x) ∈ Continuation × Continuation × 𝕋 ] x ∈ dom g
  co-IO-r .comp ((f , g , x) , _) =
    (f x .force , g x .force) ∷ [] ,
    --------------------
    (inp f , out g)

  FCompIS : IS U
  FCompIS .Names = FCompIS-RN
  FCompIS .rules client-end = from client-end-r
  FCompIS .rules oi = OI-r
  FCompIS .rules io = IO-r

  FCompCOIS : IS U
  FCompCOIS .Names = FCompCOIS-RN
  FCompCOIS .rules co-oi = from co-OI-r
  FCompCOIS .rules co-io = from co-IO-r

  _⊢_ : SessionType → SessionType → Set
  S ⊢ T = FCoInd⟦ FCompIS , FCompCOIS ⟧ (S , T)

  _⊢ᵢ_ : SessionType → SessionType → Set
  S ⊢ᵢ T = Ind⟦ FCompIS ∪ FCompCOIS ⟧ (S , T)

  {- Properties -}

  ¬nil-⊢ : ∀{S} → ¬ (nil ⊢ S)
  ¬nil-⊢ fc with fc .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (() , _)) , _) , refl , _

  ⊢ᵢ->succeed : ∀{S T} → S ⊢ᵢ T → MaySucceed (S # T)
  ⊢ᵢ->succeed (fold (inj₁ client-end , ((S , T) , (win , def)) , refl , _)) = (S # T) , ε , win#def win def
  ⊢ᵢ->succeed (fold (inj₁ oi , ((f , g) , (t , ok)) , refl , pr)) =
    let Sys' , red-Sys' , Succ = ⊢ᵢ->succeed (pr (t , ok)) in
    Sys' , sync (out ok) inp ◅ red-Sys' , Succ
  ⊢ᵢ->succeed (fold (inj₁ io , ((f , g) , (t , ok)) , refl , pr)) =
    let Sys' , red-Sys' , Succ = ⊢ᵢ->succeed (pr (t , ok)) in
    Sys' , sync inp (out ok) ◅ red-Sys' , Succ
  ⊢ᵢ->succeed (fold (inj₂ co-oi , (_ , ok-b) , refl , pr)) =
    let Sys' , red-Sys' , Succ = ⊢ᵢ->succeed (pr zero) in
    Sys' , sync (out ok-b) inp ◅ red-Sys' , Succ
  ⊢ᵢ->succeed (fold (inj₂ co-io , (_ , ok-b) , refl , pr)) =
    let Sys' , red-Sys' , Succ = ⊢ᵢ->succeed (pr zero) in
    Sys' , sync inp (out ok-b) ◅ red-Sys' , Succ

  maysucceed->⊢ᵢ : ∀{S T Sys} → Reductions (S # T) Sys → Success Sys → S ⊢ᵢ T
  maysucceed->⊢ᵢ ε (win#def win def) = apply-ind (inj₁ client-end) (_ , (win , def)) λ ()
  maysucceed->⊢ᵢ (sync (out ok) inp ◅ red) Succ =
    let rec = maysucceed->⊢ᵢ red Succ in
    apply-ind (inj₂ co-oi) (_ , ok) λ{zero → rec}
  maysucceed->⊢ᵢ (sync inp (out ok) ◅ red) Succ =
    let rec = maysucceed->⊢ᵢ red Succ in
    apply-ind (inj₂ co-io) (_ , ok) λ{zero → rec}

  {- Soundness -}

  fc-sound : ∀{S T} → S ⊢ T → FairComplianceS (S # T)
  fc-sound fc ε = ⊢ᵢ->succeed (fcoind-to-ind fc)
  fc-sound fc (x ◅ red) with fc .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (win , def)) , _) , refl , _ = ⊥-elim (success-not-reduce (win#def win def) x)
  fc-sound fc (sync (out ok) (inp {x = t}) ◅ red) | oi , (((f , _) , _) , _) , refl , pr = fc-sound (pr (t , ok)) red
  fc-sound fc (sync (inp {x = t}) (out ok) ◅ red) | io , (((_ , g) , _) , _) , refl , pr = fc-sound (pr (t , ok)) red

  {- Boundedness -}

  fc-bounded : ∀{S T} → FairComplianceS (S # T) → S ⊢ᵢ T
  fc-bounded fc =
    let _ , red-Sys , Succ = fc ε in
    maysucceed->⊢ᵢ red-Sys Succ

  {- Consistency -}

  fc-consistent : ∀{S T} → FairComplianceS (S # T) → ISF[ FCompIS ] (λ{(S , T) → FairComplianceS (S # T)}) (S , T)
  fc-consistent fc with fc ε
  ... | _ , ε , win#def win def = client-end , (_ , (win , def)) , refl , λ ()
  ... | _ , sync (out ok) (inp {x = t}) ◅ _ , _ =
    oi , (_ , (t , ok)) , refl , λ (t' , ok') red → fc (sync (out ok') (inp {x = t'}) ◅ red)
  ... | _ , sync (inp {x = t}) (out ok) ◅ _ , _ =
    io , (_ , (t , ok)) , refl , λ (t' , ok') red → fc (sync (inp {x = t'}) (out ok') ◅ red)

  {- Completeness -}

  fc-complete : ∀{S T} → FairComplianceS (S # T) → S ⊢ T
  fc-complete =
    let S = λ{(S , T) → FairComplianceS (S # T)} in
    bounded-coind[ FCompIS , FCompCOIS ] S fc-bounded fc-consistent

  {- Properties -}

  fci->defined : ∀{S T} → S ⊢ᵢ T → Defined S × Defined T
  fci->defined (fold (inj₁ client-end , (_ , (out _ , def)) , refl , _)) = out , def
  fci->defined (fold (inj₁ oi , _ , refl , _)) = out , inp
  fci->defined (fold (inj₁ io , _ , refl , _)) = inp , out
  fci->defined (fold (inj₂ co-oi , _ , refl , _)) = out , inp
  fci->defined (fold (inj₂ co-io , _ , refl , _)) = inp , out

  fc->defined : ∀{S T} → S ⊢ T → Defined S × Defined T
  fc->defined fc = fci->defined (fcoind-to-ind fc)

  no-fc-with-nil : ∀{S} → ¬ (S ⊢ nil)
  no-fc-with-nil fc with fc .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (_ , ())) , _) , refl , _

  {- Auxiliary for FS -}

  win⊢def : ∀{S} → Defined S → win ⊢ S
  win⊢def ok = apply-fcoind client-end (_ , (Win-win , ok)) λ ()

  ⊢-after-out : ∀{f g t} → t ∈ dom f → out f ⊢ inp g → f t .force ⊢ g t .force
  ⊢-after-out ok fc with fc .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (out e , _)) , _) , refl , _ = ⊥-elim (e _ ok)
  ... | oi , _ , refl , pr = pr (_ , ok)

  ⊢-after-in : ∀{f g t} → t ∈ dom g → inp f ⊢ out g → f t .force ⊢ g t .force
  ⊢-after-in ok fc with fc .CoInd⟦_⟧.unfold
  ... | client-end , ((_ , (() , _)) , _) , refl , _
  ... | io , _ , refl , pr = pr (_ , ok)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
{-# OPTIONS --without-K #-}
module container.m.from-nat.coalgebra where

open import level
open import sum
open import equality
open import function
open import sets.nat.core
open import sets.nat.struct
open import sets.unit
open import container.core
open import container.m.from-nat.core
open import container.m.from-nat.cone
open import hott.level

module _ {li la lb} (c : Container li la lb) where
  open Container c
  open import container.m.coalgebra c hiding (_≅_; module _≅_)

  Xⁱ : ℕ → I → Set (la ⊔ lb)
  Xⁱ zero = λ _ → ↑ _ ⊤
  Xⁱ (suc n) = F (Xⁱ n)

  πⁱ : ∀ n → Xⁱ (suc n) →ⁱ Xⁱ n
  πⁱ zero = λ _ _ → lift tt
  πⁱ (suc n) = imap (πⁱ n)

  module _ (i : I) where
    X : ℕ → Set (la ⊔ lb)
    X n = Xⁱ n i

    π : (n : ℕ) → X (suc n) → X n
    π n = πⁱ n i

    open Limit X π public
    open Limit-shift X π public
  open F-Limit c X π public

  pⁱ : (n : ℕ) → L →ⁱ Xⁱ n
  pⁱ n i = p i n

  βⁱ : (n : ℕ) → πⁱ n ∘ⁱ pⁱ (suc n) ≡ pⁱ n
  βⁱ n = funextⁱ (λ i → β i n)

  abstract
    outL-iso : ∀ i → F L i ≅ L i
    outL-iso i = lim-iso i ·≅ shift-iso i

    outL-lem₀ : (n : ℕ)(i : I)(x : F L i)
              → p i (suc n) (apply (outL-iso i) x) ≡ imap (pⁱ n) i x
    outL-lem₀ n i x = refl

    outL-lem₁' : (n : ℕ)(i : I)(x : F L i)
               → β i (suc n) (apply (outL-iso i) x)
               ≡ subst₂ (λ w₁ w₀ → π i (suc n) w₁ ≡ w₀)
                        (sym (outL-lem₀ (suc n) i x))
                        (sym (outL-lem₀ n i x))
                        (unapΣ (refl , funext λ b → proj₂ (proj₂ x b) n ))
    outL-lem₁' n i x = refl

  inL : F L →ⁱ L
  inL i = apply (outL-iso i)

  outL : L →ⁱ F L
  outL i = invert (outL-iso i)

  in-out : inL ∘ⁱ outL ≡ idⁱ
  in-out = funext λ i → funext λ x → _≅_.iso₂ (outL-iso i) x

  outL-lem₁ : (n : ℕ)(i : I)(x : F L i)
            → β i (suc n) (apply (outL-iso i) x)
            ≡ ap (π i (suc n)) (outL-lem₀ (suc n) i x)
            · unapΣ (refl , funext λ b → proj₂ (proj₂ x b) n)
            · sym (outL-lem₀ n i x)
  outL-lem₁ n i x = outL-lem₁' n i x
                  · subst-lem (outL-lem₀ (suc n) i x) (outL-lem₀ n i x)
                              (unapΣ (refl , funext (λ b → proj₂ (proj₂ x b) n)))
    where
      P : X i (suc (suc n)) → X i (suc n) → Set _
      P y x = π i (suc n) y ≡ x

      subst-lem : {y₁ y₂ : X i (suc (suc n))}{x₁ x₂ : X i (suc n)}
                → (p : y₁ ≡ y₂)(q : x₁ ≡ x₂)
                → (z : P y₂ x₂)
                → subst₂ P (sym p) (sym q) z ≡ ap (π i (suc n)) p · z · sym q
      subst-lem refl refl refl = refl

  𝓛 : Coalg _
  𝓛 = L , outL

  module _ {ℓ} (𝓩 : Coalg ℓ) where
    private
      Z = proj₁ 𝓩; θ = proj₂ 𝓩

    lim-coalg-iso : 𝓩 ⇒ 𝓛 ≅ ⊤
    lim-coalg-iso = begin
        ( Σ (Z →ⁱ L) λ f → outL ∘ⁱ f ≡ step f )
      ≅⟨ Σ-ap-iso refl≅ eq-lem ⟩
        ( Σ (Z →ⁱ L) λ f → inL ∘ⁱ outL ∘ⁱ f ≡ inL ∘ⁱ step f )
      ≅⟨ Ψ-lem ⟩
        ( Σ (Z →ⁱ L) λ f → inL ∘ⁱ outL ∘ⁱ f ≡ Ψ f  )
      ≅⟨ ( Σ-ap-iso refl≅ λ f → trans≡-iso (ap (λ h₁ → h₁ ∘ⁱ f) (sym in-out)) ) ⟩
        ( Σ (Z →ⁱ L) λ f → f ≡ Ψ f )
      ≅⟨ sym≅ (Σ-ap-iso isom λ _ → refl≅) ⟩
        ( Σ Cone λ c → apply isom c ≡ Ψ (apply isom c) )
      ≅⟨ ( Σ-ap-iso refl≅ λ c → trans≡-iso' (Φ-Ψ-comm c) ) ⟩
        ( Σ Cone λ c → apply isom c ≡ apply isom (Φ c) )
      ≅⟨ sym≅ (Σ-ap-iso refl≅ λ c → iso≡ isom ) ⟩
        ( Σ Cone λ c → c ≡ Φ c )
      ≅⟨ ( Σ-ap-iso refl≅ λ _ → refl≅ ) ⟩
        ( Σ Cone λ { (u , q) → (u , q) ≡ (Φ₀ u , Φ₁ u q) } )
      ≅⟨ (Σ-ap-iso refl≅ λ { (u , q) → sym≅ Σ-split-iso }) ⟩
        ( Σ Cone λ { (u , q) → Σ (u ≡ Φ₀ u) λ p → subst Cone₁ p q ≡ Φ₁ u q } )
      ≅⟨ record
           { to = λ { ((u , q) , p , r) → (u , p) , q , r }
           ; from = λ { ((u , p) , q , r) → (u , q) , p , r }
           ; iso₁ = λ { ((u , q) , p , r) → refl }
           ; iso₂ = λ { ((u , p) , q , r) → refl } } ⟩
        ( Σ (Σ Cone₀ λ u → u ≡ Φ₀ u) λ { (u , p)
        → Σ (Cone₁ u) λ q → subst Cone₁ p q ≡ Φ₁ u q } )
      ≅⟨ sym≅ ( Σ-ap-iso (sym≅ (contr-⊤-iso Fix₀-contr)) λ _ → refl≅ )
         ·≅ ×-left-unit ⟩
        ( Σ (Cone₁ u₀) λ q
        → subst Cone₁ (funext p₀) q ≡ Φ₁ u₀ q )
      ≅⟨ Fix₁-iso ⟩
        ⊤
      ∎
      where
        open cones c Xⁱ πⁱ 𝓩

        X₀-contr : ∀ i → contr (X i 0)
        X₀-contr i = ↑-level _ ⊤-contr

        Z→X₀-contr : contr (Z →ⁱ Xⁱ 0)
        Z→X₀-contr = Π-level λ i → Π-level λ _ → X₀-contr i

        step : ∀ {ly}{Y : I → Set ly} → (Z →ⁱ Y) → (Z →ⁱ F Y)
        step v = imap v ∘ⁱ θ

        Φ₀ : Cone₀ → Cone₀
        Φ₀ u 0 = λ _ _ → lift tt
        Φ₀ u (suc n) = step (u n)

        Φ₀' : Cone → Cone₀
        Φ₀' (u , q) = Φ₀ u

        Φ₁ : (u : Cone₀) → Cone₁ u → Cone₁ (Φ₀ u)
        Φ₁ u q zero = refl
        Φ₁ u q (suc n) = ap step (q n)

        Φ₁' : (c : Cone) → Cone₁ (Φ₀ (proj₁ c))
        Φ₁' (u , q) = Φ₁ u q

        Φ : Cone → Cone
        Φ (u , q) = (Φ₀ u , Φ₁ u q)

        u₀ : Cone₀
        u₀ zero = λ _ _ → lift tt
        u₀ (suc n) = step (u₀ n)

        p₀ : ∀ n → u₀ n ≡ Φ₀ u₀ n
        p₀ zero = refl
        p₀ (suc n) = refl

        Fix₀ : Set (ℓ ⊔ la ⊔ lb ⊔ li)
        Fix₀ = Σ Cone₀ λ u → u ≡ Φ₀ u

        Fix₁ : Fix₀ → Set (ℓ ⊔ la ⊔ lb ⊔ li)
        Fix₁ (u , p) = Σ (Cone₁ u) λ q → subst Cone₁ p q ≡ Φ₁ u q

        Fix₀-center : Fix₀
        Fix₀-center = u₀ , funext p₀

        Fix₀-iso : Fix₀ ≅ (∀ i → Z i → X i 0)
        Fix₀-iso = begin
            ( Σ Cone₀ λ u → u ≡ Φ₀ u )
          ≅⟨ ( Σ-ap-iso refl≅ λ u → sym≅ strong-funext-iso ·≅ ℕ-elim-shift ) ⟩
            ( Σ Cone₀ λ u → (u 0 ≡ λ _ _ → lift tt)
                          × (∀ n → u (suc n) ≡ step (u n)) )
          ≅⟨ ( Σ-ap-iso refl≅ λ u → (×-ap-iso (contr-⊤-iso (h↑ Z→X₀-contr _ _)) refl≅)
                                  ·≅ ×-left-unit ) ⟩
            ( Σ Cone₀ λ u → (∀ n → u (suc n) ≡ step (u n)) )
          ≅⟨ Limit-op.lim-contr (λ n → Z →ⁱ Xⁱ n) (λ n → step) ⟩
            (∀ i → Z i → X i 0)
          ∎
          where open ≅-Reasoning

        Fix₀-contr : contr Fix₀
        Fix₀-contr = Fix₀-center , contr⇒prop
          (iso-level (sym≅ Fix₀-iso) Z→X₀-contr) _

        Fix₁-iso : Fix₁ Fix₀-center ≅ ⊤
        Fix₁-iso = begin
            ( Σ (Cone₁ u₀) λ q → subst Cone₁ (funext p₀) q ≡ Φ₁ u₀ q )
          ≅⟨ ( Σ-ap-iso refl≅ λ q → sym≅ strong-funext-iso ) ⟩
            ( Σ (Cone₁ u₀) λ q → ∀ n → subst Cone₁ (funext p₀) q n ≡ Φ₁ u₀ q n )
          ≅⟨ ( Σ-ap-iso refl≅ λ q → Π-ap-iso refl≅ λ n
             → sym≅ (trans≡-iso (subst-lem _ _ p₀ q n)) ) ⟩
            ( Σ (Cone₁ u₀) λ q → ∀ n
            → subst₂ (P n) (p₀ (suc n)) (p₀ n) (q n) ≡ Φ₁ u₀ q n )
          ≅⟨ ( Σ-ap-iso refl≅ λ q → ℕ-elim-shift ) ⟩
            ( Σ (Cone₁ u₀) λ q
            → (q 0 ≡ Φ₁ u₀ q 0)
            × (∀ n → q (suc n) ≡ Φ₁ u₀ q (suc n)) )
          ≅⟨ ( Σ-ap-iso refl≅ λ q → ×-ap-iso (contr-⊤-iso (h↑ (h↑ Z→X₀-contr _ _) _ _))
                                             refl≅
                                  ·≅ ×-left-unit ) ⟩
            ( Σ (Cone₁ u₀) λ q
            → ∀ n → q (suc n) ≡ ap step (q n) )
          ≅⟨ Limit-op.lim-contr (λ n → πⁱ n ∘ⁱ u₀ (suc n) ≡ u₀ n) (λ n → ap step) ⟩
            ( πⁱ 0 ∘ⁱ u₀ 1 ≡ u₀ 0 )
          ≅⟨ contr-⊤-iso (h↑ Z→X₀-contr _ _) ⟩
            ⊤
          ∎
          where
            P = λ m x y → πⁱ m ∘ⁱ x ≡ y

            subst-lem₁ : (u v : Cone₀)(p : u ≡ v)(q : Cone₁ u)(n : ℕ)
                       → subst Cone₁ p q n
                       ≡ subst₂ (P n) (funext-inv p (suc n)) (funext-inv p n) (q n)
            subst-lem₁ u .u refl q n = refl

            subst-lem : (u v : Cone₀)(p : ∀ n → u n ≡ v n)(q : Cone₁ u)(n : ℕ)
                      → subst Cone₁ (funext p) q n
                      ≡ subst₂ (P n) (p (suc n)) (p n) (q n)
            subst-lem u v p q n = subst-lem₁ u v (funext p) q n
                                · ap (λ p → subst₂ (P n) (p (suc n)) (p n) (q n))
                                     (_≅_.iso₁ strong-funext-iso p)

            open ≅-Reasoning

        Ψ : (Z →ⁱ L) → (Z →ⁱ L)
        Ψ f = inL ∘ⁱ step f

        Ψ-lem : ( Σ (Z →ⁱ L) λ f → inL ∘ⁱ outL ∘ⁱ f ≡ inL ∘ⁱ step f)
              ≅ ( Σ (Z →ⁱ L) λ f → inL ∘ⁱ outL ∘ⁱ f ≡ Ψ f )
        Ψ-lem = Σ-ap-iso refl≅ λ f → refl≅

        Φ-Ψ-comm₀ : (f : Z →ⁱ L) → ∀ n i z
                  → p i n (Ψ f i z)
                  ≡ Φ₀' (invert isom f) n i z
        Φ-Ψ-comm₀ f 0 i z = h1⇒prop (h↑ (X₀-contr i)) _ _
        Φ-Ψ-comm₀ f (suc n) i z = outL-lem₀ n i (imap f i (θ i z))

        Φ-Ψ-comm₁' : (f : Z →ⁱ L) → ∀ n i z
                    → β i n (Ψ f i z)
                    ≡ ap (π i n) (Φ-Ψ-comm₀ f (suc n) i z)
                    · funext-invⁱ (Φ₁' (invert isom f) n) i z
                    · sym (Φ-Ψ-comm₀ f n i z)
        Φ-Ψ-comm₁' f 0 i z = h1⇒prop (h↑ (h↑ (X₀-contr i)) _ _) _ _
        Φ-Ψ-comm₁' f (suc n) i z = begin
            β i (suc n) (inL i (imap f i (θ i z)))
          ≡⟨ outL-lem₁ n i (imap f i (θ i z)) ⟩
            ( ap (π i (suc n)) (Φ-Ψ-comm₀ f (suc (suc n)) i z)
            · unapΣ (refl , funext λ b → β (r b) n (proj₂ (imap f i (θ i z)) b))
            · sym (Φ-Ψ-comm₀ f (suc n) i z) )
          ≡⟨ ap (λ ω → ap (π i (suc n)) (Φ-Ψ-comm₀ f (suc (suc n)) i z)
                     · ω · sym (Φ-Ψ-comm₀ f (suc n) i z))
                (lem (λ i x → β i n x) i z) ⟩
            ( ap (π i (suc n)) (Φ-Ψ-comm₀ f (suc (suc n)) i z)
            · funext-invⁱ (ap step (funextⁱ (λ i z → β i n (f i z)))) i z
            · sym (Φ-Ψ-comm₀ f (suc n) i z) )
          ∎
          where
            open ≡-Reasoning

            lem' : {u v : L →ⁱ Xⁱ n}(ω : u ≡ v)(i : I)(z : Z i)
                 → unapΣ (refl , funext λ b → funext-invⁱ ω (r b) (proj₂ (imap f i (θ i z)) b))
                 ≡ funext-invⁱ (ap step (funextⁱ (λ i z → funext-invⁱ ω i (f i z)))) i z
            lem' refl i z = begin
                unapΣ (refl , funext λ b → refl)
              ≡⟨ ap (λ ω → unapΣ (refl , ω)) (_≅_.iso₂ strong-funext-iso refl) ⟩
                refl
              ≡⟨ sym (ap (λ ω → funext-invⁱ (ap step ω) i z)
                         (_≅_.iso₂ funext-isoⁱ refl)) ⟩
               funext-invⁱ (ap step (funextⁱ (λ i z → refl))) i z
              ∎
              where
                open ≡-Reasoning

            lem : {u v : L →ⁱ Xⁱ n}(ω : (i : I)(x : L i) → u i x ≡ v i x)(i : I)(z : Z i)
                → unapΣ (refl , funext λ b → ω (r b) (proj₂ (imap f i (θ i z)) b))
                ≡ funext-invⁱ (ap step (funextⁱ (λ i z → ω i (f i z)))) i z
            lem {u}{v} = invert (Π-ap-iso funext-isoⁱ λ ω → refl≅) lem'

        Φ-Ψ-comm₁ : (f : Z →ⁱ L) → ∀ n i z
                   → funext-invⁱ (funextⁱ λ i z → β i n (Ψ f i z)) i z
                   ≡ ap (π i n) (Φ-Ψ-comm₀ f (suc n) i z)
                   · funext-invⁱ (Φ₁' (invert isom f) n) i z
                   · sym (Φ-Ψ-comm₀ f n i z)
        Φ-Ψ-comm₁ f n i z = ap (λ h → h i z)
                                (_≅_.iso₁ funext-isoⁱ (λ i z → β i n (Ψ f i z)))
                          · Φ-Ψ-comm₁' f n i z

        Φ-Ψ-comm' : (f : Z →ⁱ L) → invert isom (Ψ f) ≡ Φ (invert isom f)
        Φ-Ψ-comm' f = Cone-eq (Φ-Ψ-comm₀ f) (Φ-Ψ-comm₁ f)

        Φ-Ψ-comm : (c : Cone) → Ψ (apply isom c) ≡ apply isom (Φ c)
        Φ-Ψ-comm c = sym (_≅_.iso₂ isom (Ψ (apply isom c)))
                   · ap (apply isom)
                        (Φ-Ψ-comm' (apply isom c) · ap Φ (_≅_.iso₁ isom c))

        cone-comp₀ : (f : Z →ⁱ L)(n : ℕ)(i : I)(z : Z i)
                   → proj₁ (invert isom (Ψ f)) n i z
                   ≡ p i n (Ψ f i z)
        cone-comp₀ f n i z = refl

        cone-comp₁ : (f : Z →ⁱ L)(n : ℕ)
                   → proj₂ (invert isom (Ψ f)) n
                   ≡ funextⁱ (λ i z → β i n (Ψ f i z))
        cone-comp₁ f n = refl

        eq-lem : (f : Z →ⁱ L) → (outL ∘ⁱ f ≡ step f)
                              ≅ (inL ∘ⁱ outL ∘ⁱ f ≡ inL ∘ⁱ step f)
        eq-lem f = iso≡ ( Π-ap-iso refl≅ λ i
                        → Π-ap-iso refl≅ λ _
                        → outL-iso i )

        open ≅-Reasoning

    lim-terminal : contr (𝓩 ⇒ 𝓛)
    lim-terminal = iso-level (sym≅ lim-coalg-iso) ⊤-contr

  m-final : Final _
  m-final = 𝓛 , lim-terminal

  -- Theorem 7 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
  m-final-contr : contr (Final _)
  m-final-contr = m-final , λ fin → Final-prop m-final fin

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the heterogeneous prefix relation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Prefix.Heterogeneous.Properties where

open import Data.Empty
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
import Data.List.Relation.Unary.All.Properties as All
open import Data.List.Base as List hiding (map; uncons)
open import Data.List.Membership.Propositional.Properties using ([]∈inits)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix hiding (PrefixView; _++_)
open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (suc-injective)
open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; uncurry)
open import Function

open import Relation.Nullary using (yes; no; ¬_)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary as U using (Pred)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)

------------------------------------------------------------------------
-- First as a decidable partial order (once made homogeneous)

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  fromPointwise : Pointwise R ⇒ Prefix R
  fromPointwise []       = []
  fromPointwise (r ∷ rs) = r ∷ fromPointwise rs

  toPointwise : ∀ {as bs} → length as ≡ length bs →
                Prefix R as bs → Pointwise R as bs
  toPointwise {bs = []} eq [] = []
  toPointwise {bs = _ ∷ _} () []
  toPointwise eq (r ∷ rs) = r ∷ toPointwise (suc-injective eq) rs

module _ {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
         {R : REL A B r} {S : REL B C s} {T : REL A C t} where

  trans : Trans R S T → Trans (Prefix R) (Prefix S) (Prefix T)
  trans rs⇒t []       ss       = []
  trans rs⇒t (r ∷ rs) (s ∷ ss) = rs⇒t r s ∷ trans rs⇒t rs ss

module _ {a b r s e} {A : Set a} {B : Set b}
         {R : REL A B r} {S : REL B A s} {E : REL A B e} where

  antisym : Antisym R S E → Antisym (Prefix R) (Prefix S) (Pointwise E)
  antisym rs⇒e []       []       = []
  antisym rs⇒e (r ∷ rs) (s ∷ ss) = rs⇒e r s ∷ antisym rs⇒e rs ss

------------------------------------------------------------------------
-- length

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  length-mono : ∀ {as bs} → Prefix R as bs → length as ≤ length bs
  length-mono []       = z≤n
  length-mono (r ∷ rs) = s≤s (length-mono rs)

------------------------------------------------------------------------
-- _++_

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  ++⁺ : ∀ {as bs cs ds} → Pointwise R as bs →
        Prefix R cs ds → Prefix R (as ++ cs) (bs ++ ds)
  ++⁺ []       cs⊆ds = cs⊆ds
  ++⁺ (r ∷ rs) cs⊆ds = r ∷ (++⁺ rs cs⊆ds)

  ++⁻ : ∀ {as bs cs ds} → length as ≡ length bs →
        Prefix R (as ++ cs) (bs ++ ds) → Prefix R cs ds
  ++⁻ {[]}    {[]}    eq rs       = rs
  ++⁻ {_ ∷ _} {_ ∷ _} eq (_ ∷ rs) = ++⁻ (suc-injective eq) rs
  ++⁻ {[]} {_ ∷ _} ()
  ++⁻ {_ ∷ _} {[]} ()

------------------------------------------------------------------------
-- map

module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
         {R : REL C D r} where

  map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
         Prefix (λ a b → R (f a) (g b)) as bs →
         Prefix R (List.map f as) (List.map g bs)
  map⁺ f g []       = []
  map⁺ f g (r ∷ rs) = r ∷ map⁺ f g rs

  map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
         Prefix R (List.map f as) (List.map g bs) →
         Prefix (λ a b → R (f a) (g b)) as bs
  map⁻ {[]}     {bs}     f g rs       = []
  map⁻ {a ∷ as} {[]}     f g ()
  map⁻ {a ∷ as} {b ∷ bs} f g (r ∷ rs) = r ∷ map⁻ f g rs

------------------------------------------------------------------------
-- filter

module _ {a b r p q} {A : Set a} {B : Set b} {R : REL A B r}
         {P : Pred A p} {Q : Pred B q} (P? : U.Decidable P) (Q? : U.Decidable Q)
         (P⇒Q : ∀ {a b} → R a b → P a → Q b) (Q⇒P : ∀ {a b} → R a b → Q b → P a)
         where

  filter⁺ : ∀ {as bs} → Prefix R as bs → Prefix R (filter P? as) (filter Q? bs)
  filter⁺ [] = []
  filter⁺ {a ∷ as} {b ∷ bs} (r ∷ rs) with P? a | Q? b
  ... | yes pa | yes qb = r ∷ filter⁺ rs
  ... | yes pa | no ¬qb = ⊥-elim (¬qb (P⇒Q r pa))
  ... | no ¬pa | yes qb = ⊥-elim (¬pa (Q⇒P r qb))
  ... | no ¬pa | no ¬qb = filter⁺ rs

------------------------------------------------------------------------
-- take

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  take⁺ : ∀ {as bs} n → Prefix R as bs →
          Prefix R (take n as) (take n bs)
  take⁺ zero    rs       = []
  take⁺ (suc n) []       = []
  take⁺ (suc n) (r ∷ rs) = r ∷ take⁺ n rs

  take⁻ : ∀ {as bs} n →
          Prefix R (take n as) (take n bs) →
          Prefix R (drop n as) (drop n bs) →
          Prefix R as bs
  take⁻                   zero    hds       tls = tls
  take⁻ {[]}              (suc n) hds       tls = []
  take⁻ {a ∷ as} {[]}     (suc n) ()        tls
  take⁻ {a ∷ as} {b ∷ bs} (suc n) (r ∷ hds) tls = r ∷ take⁻ n hds tls

------------------------------------------------------------------------
-- drop

  drop⁺ : ∀ {as bs} n → Prefix R as bs → Prefix R (drop n as) (drop n bs)
  drop⁺ zero    rs       = rs
  drop⁺ (suc n) []       = []
  drop⁺ (suc n) (r ∷ rs) = drop⁺ n rs

  drop⁻ : ∀ {as bs} n → Pointwise R (take n as) (take n bs) →
          Prefix R (drop n as) (drop n bs) → Prefix R as bs
  drop⁻                 zero    hds       tls = tls
  drop⁻ {[]}            (suc n) hds       tls = []
  drop⁻ {_ ∷ _} {[]}    (suc n) ()        tls
  drop⁻ {_ ∷ _} {_ ∷ _} (suc n) (r ∷ hds) tls = r ∷ (drop⁻ n hds tls)

------------------------------------------------------------------------
-- replicate

  replicate⁺ : ∀ {m n a b} → m ≤ n → R a b →
               Prefix R (replicate m a) (replicate n b)
  replicate⁺ z≤n       r = []
  replicate⁺ (s≤s m≤n) r = r ∷ replicate⁺ m≤n r

  replicate⁻ : ∀ {m n a b} → m ≢ 0 →
               Prefix R (replicate m a) (replicate n b) → R a b
  replicate⁻ {zero}  {n}     m≢0 r  = ⊥-elim (m≢0 P.refl)
  replicate⁻ {suc m} {zero}  m≢0 ()
  replicate⁻ {suc m} {suc n} m≢0 rs = Prefix.head rs

------------------------------------------------------------------------
-- inits

module _ {a r} {A : Set a} {R : Rel A r} where

  inits⁺ : ∀ {as} → Pointwise R as as → All (flip (Prefix R) as) (inits as)
  inits⁺ []       = [] ∷ []
  inits⁺ (r ∷ rs) = [] ∷ All.map⁺ (All.map (r ∷_) (inits⁺ rs))

  inits⁻ : ∀ {as} → All (flip (Prefix R) as) (inits as) → Pointwise R as as
  inits⁻ {as = []}     rs       = []
  inits⁻ {as = a ∷ as} (r ∷ rs) =
    let (hd , tls) = All.unzip (All.map uncons (All.map⁻ rs)) in
    All.lookup hd ([]∈inits as) ∷ inits⁻ tls

------------------------------------------------------------------------
-- zip(With)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
         {d e f} {D : Set d} {E : Set e} {F : Set f}
         {r s t} {R : REL A D r} {S : REL B E s} {T : REL C F t} where

  zipWith⁺ : ∀ {as bs ds es} {f : A → B → C} {g : D → E → F} →
    (∀ {a b c d} → R a c → S b d → T (f a b) (g c d)) →
    Prefix R as ds → Prefix S bs es →
    Prefix T (zipWith f as bs) (zipWith g ds es)
  zipWith⁺ f []       ss       = []
  zipWith⁺ f (r ∷ rs) []       = []
  zipWith⁺ f (r ∷ rs) (s ∷ ss) = f r s ∷ zipWith⁺ f rs ss

module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
         {r s} {R : REL A C r} {S : REL B D s} where

  private
    R×S : REL (A × B) (C × D) _
    R×S (a , b) (c , d) = R a c × S b d

  zip⁺ : ∀ {as bs cs ds} → Prefix R as cs → Prefix S bs ds →
         Prefix R×S (zip as bs) (zip cs ds)
  zip⁺ = zipWith⁺ _,_

------------------------------------------------------------------------
-- Irrelevance

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  irrelevant : Irrelevant R → Irrelevant (Prefix R)
  irrelevant R-irr []       []         = P.refl
  irrelevant R-irr (r ∷ rs) (r′ ∷ rs′) =
    P.cong₂ _∷_ (R-irr r r′) (irrelevant R-irr rs rs′)

------------------------------------------------------------------------
-- Decidability

  prefix? : Decidable R → Decidable (Prefix R)
  prefix? R? []       bs       = yes []
  prefix? R? (a ∷ as) []       = no (λ ())
  prefix? R? (a ∷ as) (b ∷ bs) = Dec.map′ (uncurry _∷_) uncons
                               $ R? a b ×-dec prefix? R? as bs


text:
module Golden.Index where

open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Bool

lst : List Nat
lst = 1 ∷ 2 ∷ []

atDef : ∀ {a : Set} → a → List a -> Nat -> a
atDef def (x ∷ l) zero = x
atDef def (x ∷ l) (suc ix) = atDef def l ix
atDef def _ _ = def

l0 : Nat
l0 = atDef 0 lst 0

l1 : Nat
l1 = atDef 0 lst 1

l2 : Nat
l2 = atDef 0 lst 2

max_stars_repo_name: agda/agda-ocaml

max_issues_repo_name: agda/agda-ocaml

max_forks_repo_name: agda/agda-ocaml


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax TLC | Λ

type
  N   : 0-ary
  _↣_ : 2-ary | r30
  𝟙   : 0-ary
  _⊗_ : 2-ary | l40
  𝟘   : 0-ary
  _⊕_ : 2-ary | l30

term
  app   : α ↣ β  α  ->  β | _$_ l20
  lam   : α.β  ->  α ↣ β | ƛ_ r10
  unit  : 𝟙
  pair  : α  β  ->  α ⊗ β | ⟨_,_⟩
  fst   : α ⊗ β  ->  α
  snd   : α ⊗ β  ->  β
  abort : 𝟘  ->  α
  inl   : α  ->  α ⊕ β
  inr   : β  ->  α ⊕ β
  case  : α ⊕ β  α.γ  β.γ  ->  γ
  ze    : N
  su    : N  ->  N
  nrec  : N  α  (α,N).α  ->  α

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
  (𝟙η) u : 𝟙 |> u = unit
  (fβ) a : α  b : β |> fst (pair(a, b))      = a
  (sβ) a : α  b : β |> snd (pair(a, b))      = b
  (pη) p : α ⊗ β    |> pair (fst(p), snd(p)) = p
  (𝟘η) e : 𝟘  c : α |> abort(e) = c
  (lβ) a : α   f : α.γ  g : β.γ |> case (inl(a), x.f[x], y.g[y])      = f[a]
  (rβ) b : β   f : α.γ  g : β.γ |> case (inr(b), x.f[x], y.g[y])      = g[b]
  (cη) s : α ⊕ β  c : (α ⊕ β).γ |> case (s, x.c[inl(x)], y.c[inr(y)]) = c[s]
  (zeβ) z : α   s : (α,N).α        |> nrec (ze,       z, r m. s[r,m]) = z
  (suβ) z : α   s : (α,N).α  n : N |> nrec (su (n), z, r m. s[r,m]) = s[nrec (n, z, r m. s[r,m]), n]
  (ift) t f : α |> if (true, t, f) = t
  (iff) t f : α |> if (false, t, f) = f
-}

module TLC.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import TLC.Signature

private
  variable
    Γ Δ Π : Ctx
    α β γ : ΛT
    𝔛 : Familyₛ

-- Inductive term declaration
module Λ:Terms (𝔛 : Familyₛ) where

  data Λ : Familyₛ where
    var  : ℐ ⇾̣ Λ
    mvar : 𝔛 α Π → Sub Λ Π Γ → Λ α Γ

    _$_   : Λ (α ↣ β) Γ → Λ α Γ → Λ β Γ
    ƛ_    : Λ β (α ∙ Γ) → Λ (α ↣ β) Γ
    unit  : Λ 𝟙 Γ
    ⟨_,_⟩ : Λ α Γ → Λ β Γ → Λ (α ⊗ β) Γ
    fst   : Λ (α ⊗ β) Γ → Λ α Γ
    snd   : Λ (α ⊗ β) Γ → Λ β Γ
    abort : Λ 𝟘 Γ → Λ α Γ
    inl   : Λ α Γ → Λ (α ⊕ β) Γ
    inr   : Λ β Γ → Λ (α ⊕ β) Γ
    case  : Λ (α ⊕ β) Γ → Λ γ (α ∙ Γ) → Λ γ (β ∙ Γ) → Λ γ Γ
    ze    : Λ N Γ
    su    : Λ N Γ → Λ N Γ
    nrec  : Λ N Γ → Λ α Γ → Λ α (α ∙ N ∙ Γ) → Λ α Γ

  infixl 20 _$_
  infixr 10 ƛ_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Λᵃ : MetaAlg Λ
  Λᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (appₒ   ⋮ a , b)     → _$_   a b
      (lamₒ   ⋮ a)         → ƛ_    a
      (unitₒ  ⋮ _)         → unit
      (pairₒ  ⋮ a , b)     → ⟨_,_⟩ a b
      (fstₒ   ⋮ a)         → fst   a
      (sndₒ   ⋮ a)         → snd   a
      (abortₒ ⋮ a)         → abort a
      (inlₒ   ⋮ a)         → inl   a
      (inrₒ   ⋮ a)         → inr   a
      (caseₒ  ⋮ a , b , c) → case  a b c
      (zeₒ    ⋮ _)         → ze
      (suₒ    ⋮ a)         → su    a
      (nrecₒ  ⋮ a , b , c) → nrec  a b c
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Λᵃ = MetaAlg Λᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : Λ ⇾̣ 𝒜
    𝕊 : Sub Λ Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (_$_   a b)   = 𝑎𝑙𝑔 (appₒ   ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (ƛ_    a)     = 𝑎𝑙𝑔 (lamₒ   ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞  unit         = 𝑎𝑙𝑔 (unitₒ  ⋮ tt)
    𝕤𝕖𝕞 (⟨_,_⟩ a b)   = 𝑎𝑙𝑔 (pairₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (fst   a)     = 𝑎𝑙𝑔 (fstₒ   ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (snd   a)     = 𝑎𝑙𝑔 (sndₒ   ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (abort a)     = 𝑎𝑙𝑔 (abortₒ ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (inl   a)     = 𝑎𝑙𝑔 (inlₒ   ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (inr   a)     = 𝑎𝑙𝑔 (inrₒ   ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (case  a b c) = 𝑎𝑙𝑔 (caseₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b , 𝕤𝕖𝕞 c)
    𝕤𝕖𝕞  ze           = 𝑎𝑙𝑔 (zeₒ    ⋮ tt)
    𝕤𝕖𝕞 (su    a)     = 𝑎𝑙𝑔 (suₒ    ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (nrec  a b c) = 𝑎𝑙𝑔 (nrecₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b , 𝕤𝕖𝕞 c)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ Λᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ Λ α Γ) → 𝕤𝕖𝕞 (Λᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (appₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (lamₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (unitₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (pairₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (fstₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (sndₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (abortₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (inlₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (inrₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (caseₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (zeₒ    ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (suₒ    ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (nrecₒ  ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ Λ ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : Λ ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ Λᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : Λ α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub Λ Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (_$_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (ƛ_ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! unit = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (⟨_,_⟩ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (fst a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (snd a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (abort a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (inl a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (inr a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (case a b c) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b | 𝕤𝕖𝕞! c = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! ze = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (su a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (nrec a b c) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b | 𝕤𝕖𝕞! c = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
Λ:Syn : Syntax
Λ:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = Λ:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open Λ:Terms 𝔛 in record
    { ⊥ = Λ ⋉ Λᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax Λ:Syn public
open Λ:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands Λᵃ public
open import SOAS.Metatheory Λ:Syn public

-- Derived operations
true : Λ 𝔛 B Γ
true = inl unit
false : Λ 𝔛 B Γ
false = inr unit
if : Λ 𝔛 B Γ → Λ 𝔛 α Γ → Λ 𝔛 α Γ → Λ 𝔛 α Γ
if b t e = case b (Theory.𝕨𝕜 _ t) (Theory.𝕨𝕜 _ e)

plus : Λ 𝔛 (N ↣ N ↣ N) Γ
plus = ƛ (ƛ (nrec x₁ x₀ (su x₀)))

uncurry : Λ 𝔛 ((α ↣ β ↣ γ) ↣ (α ⊗ β) ↣ γ) Γ
uncurry = ƛ ƛ x₁ $ fst x₀ $ snd x₀

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas