text:
-- a hodge-podge of tests

module Test where

import Test.Class
import Test.EquivalenceExtensionṖroperty
import Test.EquivalenceṖroperty
import Test.EquivalentCandidates
import Test.EquivalentCandidates-2
import Test.Factsurj3
import Test.Functor -- FIXME doesn't work with open import Everything
import Test.ProblemWithDerivation
import Test.ProblemWithDerivation-2
import Test.ProblemWithDerivation-3
import Test.ProblemWithDerivation-4
import Test.ProblemWithDerivation-5
import Test.ProblemWithLevelZero
import Test.ProblemWithSym
import Test.ṖropertyFacts -- FIXME doesn't work with open import Everything
import Test.ṖropertyFactsSubstitunction
import Test.SubstitunctionPropId
import Test.Surjcollation -- FIXME remove commented import block?
import Test.Surjidentity
import Test.SurjidentityI
import Test.SurjidentityP
import Test.Symmetrical
import Test.SymmetricalSubstitunction
import Test.Test0
import Test.Test1
import Test.Test2
import Test.Test3
import Test.Test4
import Test.Test5
import Test.Test6
import Test.Test7
import Test.Thickandthin
import Test.Transassociativity
import Test.UnifiesSubstitunction
import Test.𝓢urjectivityWithOverlapping𝓢urjection


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

open import Agda.Builtin.Cubical.Path using (_≡_)
open import Agda.Builtin.Sigma using (Σ; fst; _,_)

postulate
  Is-proposition : Set → Set
  subst          : ∀ {A : Set} (P : A → Set) {x y} → x ≡ y → P x → P y

Proposition : Set₁
Proposition = Σ _ Is-proposition

data _/_ (A : Set) (R : A → A → Proposition) : Set where
  [_]  : A → A / R
  resp : ∀ {x y} → fst (R x y) → [ x ] ≡ [ y ]

variable
  A : Set
  R : A → A → Proposition

postulate
  F : (P : A / R → Set)
      (p-[] : ∀ x → P [ x ]) →
      (∀ {x y} (r : fst (R x y)) → subst P (resp r) (p-[] x) ≡ p-[] y) →
      Set

F' : (A : Set)
     (R : A → A → Proposition)
     (P : A / R → Set)
     (p-[] : ∀ x → P [ x ]) →
     (∀ {x y} (r : fst (R x y)) → subst P (resp r) (p-[] x) ≡ p-[] y) →
     Set
F' A R = F {A = A} {R = R}

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

module A where

  infix 0 c

  syntax c x = + x

  data D₁ : Set where
    b : D₁
    c : D₁ → D₁

module B where

  infix 1 c

  syntax c x = + x

  data D₂ : Set where
    c : A.D₁ → D₂

open A
open B

test₁ : D₂
test₁ = + + + b

test₂ : D₂ → D₁
test₂ (+ + x) = x
test₂ (+ b)   = + + + b

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Examples.TreeSum where

open import Calf.CostMonoid
open import Calf.CostMonoids using (ℕ²-ParCostMonoid)

parCostMonoid = ℕ²-ParCostMonoid
open ParCostMonoid parCostMonoid

open import Calf costMonoid
open import Calf.ParMetalanguage parCostMonoid
open import Calf.Types.Nat
open import Calf.Types.Bounded costMonoid

open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; module ≡-Reasoning)
open import Data.Nat as Nat using (_+_; _⊔_)
open import Data.Nat.Properties as N using ()
open import Data.Product

add : cmp (Π nat λ _ → Π nat λ _ → F nat)
add m n = step (F nat) (1 , 1) (ret (m + n))

add/cost : cmp (Π nat λ _ → Π nat λ _ → cost)
add/cost m n = (1 , 1) ⊕ 𝟘

add/cost/closed : cmp (Π nat λ _ → Π nat λ _ → cost)
add/cost/closed m n = (1 , 1)

add/cost≤add/cost/closed : ∀ m n → ◯ (add/cost m n ≤ add/cost/closed m n)
add/cost≤add/cost/closed m n u = ≤-reflexive (⊕-identityʳ (1 , 1))

add≤add/cost : ∀ m n → IsBounded nat (add m n) (add/cost m n)
add≤add/cost m n = bound/step (1 , 1) _ bound/ret

add≤add/cost/closed : ∀ m n → IsBounded nat (add m n) (add/cost/closed m n)
add≤add/cost/closed m n = bound/relax (add/cost≤add/cost/closed m n) (add≤add/cost m n)

data Tree : Set where
  leaf : val nat → Tree
  node : Tree → Tree → Tree

tree : tp pos
tree = U (meta Tree)

sum : cmp (Π tree λ _ → F nat)
sum (leaf x)     = ret x
sum (node t₁ t₂) =
  bind (F nat) (sum t₁ & sum t₂) λ (n₁ , n₂) →
    add n₁ n₂

sum/total : ∀ t → ◯ (∃ λ n → sum t ≡ ret n)
sum/total (leaf x)     u = x , refl
sum/total (node t₁ t₂) u =
  let (n₁ , ≡₁) = sum/total t₁ u
      (n₂ , ≡₂) = sum/total t₂ u
  in
  n₁ + n₂ , (
    let open ≡-Reasoning in
    begin
      (bind (F nat) (sum t₁ & sum t₂) λ (n₁ , n₂) →
        add n₁ n₂)
    ≡⟨ Eq.cong₂ (λ e₁ e₂ → bind (F nat) (e₁ & e₂) _) ≡₁ ≡₂ ⟩
      add n₁ n₂
    ≡⟨⟩
      step (F nat) (1 , 1) (ret (n₁ + n₂))
    ≡⟨ step/ext (F nat) _ (1 , 1) u ⟩
      ret (n₁ + n₂)
    ∎
  )

sum/cost : cmp (Π tree λ _ → cost)
sum/cost (leaf x)     = 𝟘
sum/cost (node t₁ t₂) =
  bind cost (sum t₁ & sum t₂) λ (n₁ , n₂) → (sum/cost t₁ ⊗ sum/cost t₂) ⊕
    add/cost/closed n₁ n₂

size : val tree → val nat
size (leaf x)     = 0
size (node t₁ t₂) = suc (size t₁ + size t₂)

depth : val tree → val nat
depth (leaf x)     = 0
depth (node t₁ t₂) = suc (depth t₁ ⊔ depth t₂)

sum/cost/closed : cmp (Π tree λ _ → cost)
sum/cost/closed t = size t , depth t

sum/cost≤sum/cost/closed : ∀ t → ◯ (sum/cost t ≤ sum/cost/closed t)
sum/cost≤sum/cost/closed (leaf x)     u = ≤-refl
sum/cost≤sum/cost/closed (node t₁ t₂) u =
  let (_ , ≡₁) = sum/total t₁ u
      (_ , ≡₂) = sum/total t₂ u
  in
  begin
    sum/cost (node t₁ t₂)
  ≡⟨⟩
    (bind cost (sum t₁ & sum t₂) λ (n₁ , n₂) → (sum/cost t₁ ⊗ sum/cost t₂) ⊕
      add/cost/closed n₁ n₂)
  ≡⟨ Eq.cong₂ (λ e₁ e₂ → bind cost (e₁ & e₂) λ (n₁ , n₂) → (sum/cost t₁ ⊗ sum/cost t₂) ⊕ _) ≡₁ ≡₂ ⟩
    sum/cost t₁ ⊗ sum/cost t₂ ⊕ (1 , 1)
  ≤⟨ ⊕-monoˡ-≤ (1 , 1) (⊗-mono-≤ (sum/cost≤sum/cost/closed t₁ u) (sum/cost≤sum/cost/closed t₂ u)) ⟩
    sum/cost/closed t₁ ⊗ sum/cost/closed t₂ ⊕ (1 , 1)
  ≡⟨⟩
    (size t₁ , depth t₁) ⊗ (size t₂ , depth t₂) ⊕ (1 , 1)
  ≡⟨⟩
    size t₁ + size t₂ + 1 , depth t₁ ⊔ depth t₂ + 1
  ≡⟨ Eq.cong₂ _,_ (N.+-comm _ 1) (N.+-comm _ 1) ⟩
    suc (size t₁ + size t₂) , suc (depth t₁ ⊔ depth t₂)
  ≡⟨⟩
    sum/cost/closed (node t₁ t₂)
  ∎
    where open ≤-Reasoning

sum≤sum/cost : ∀ t → IsBounded nat (sum t) (sum/cost t)
sum≤sum/cost (leaf x)     = bound/ret
sum≤sum/cost (node t₁ t₂) =
  bound/bind (sum/cost t₁ ⊗ sum/cost t₂) _ (bound/par (sum≤sum/cost t₁) (sum≤sum/cost t₂)) λ (n₁ , n₂) →
    add≤add/cost/closed n₁ n₂

sum≤sum/cost/closed : ∀ t → IsBounded nat (sum t) (sum/cost/closed t)
sum≤sum/cost/closed t = bound/relax (sum/cost≤sum/cost/closed t) (sum≤sum/cost t)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

module Categories.NaturalTransformation.Core where

open import Level

open import Categories.Category
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as MR

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

record NaturalTransformation {C : Category o ℓ e}
                             {D : Category o′ ℓ′ e′}
                             (F G : Functor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
  eta-equality
  private
    module F = Functor F
    module G = Functor G
  open F using (F₀; F₁)
  open Category D hiding (op)

  field
    η           : ∀ X → D [ F₀ X , G.F₀ X ]
    commute     : ∀ {X Y} (f : C [ X , Y ]) → η Y ∘ F₁ f ≈ G.F₁ f ∘ η X
    -- We introduce an extra proof to ensure the opposite of the opposite of a natural
    -- transformation is definitionally equal to itself.
    sym-commute : ∀ {X Y} (f : C [ X , Y ]) → G.F₁ f ∘ η X ≈ η Y ∘ F₁ f

  op : NaturalTransformation G.op F.op
  op = record
    { η           = η
    ; commute     = sym-commute
    ; sym-commute = commute
    }

-- Just like `Category`, we introduce a helper definition to ease the actual
-- construction of a natural transformation.
record NTHelper {C : Category o ℓ e}
                {D : Category o′ ℓ′ e′}
                (F G : Functor C D) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module G = Functor G
  open Functor F using (F₀; F₁)
  open Category D hiding (op)
  field
    η           : ∀ X → D [ F₀ X , G.F₀ X ]
    commute     : ∀ {X Y} (f : C [ X , Y ]) → η Y ∘ F₁ f ≈ G.F₁ f ∘ η X

ntHelper : ∀ {F G : Functor C D} → NTHelper F G → NaturalTransformation F G
ntHelper {D = D} α = record
  { η           = η
  ; commute     = commute
  ; sym-commute = λ f → Equiv.sym (commute f)
  }
  where open NTHelper α
        open Category D

id : ∀ {F : Functor C D} → NaturalTransformation F F
id {D = D} = ntHelper record
  { η = λ _ → D.id
  ; commute = λ _ → D.identityˡ ○ ⟺ D.identityʳ
  }
  where
  module D = Category D
  open D.HomReasoning

infixr 9 _∘ᵥ_ _∘ₕ_ _∘ˡ_ _∘ʳ_

-- "Vertical composition"
_∘ᵥ_ : ∀ {F G H : Functor C D} →
         NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
_∘ᵥ_ {C = C} {D = D} {F} {G} {H} X Y = ntHelper record
  { η       = λ q → D [ X.η q ∘ Y.η q ]
  ; commute = λ f → glue (X.commute f) (Y.commute f)
  }
  where module X = NaturalTransformation X
        module Y = NaturalTransformation Y
        open MR D

-- "Horizontal composition"
_∘ₕ_ : ∀ {F G : Functor C D} {H I : Functor D E} →
         NaturalTransformation H I → NaturalTransformation F G → NaturalTransformation (H ∘F F) (I ∘F G)
_∘ₕ_ {E = E} {F} {I = I} Y X = ntHelper record
  { η = λ q → E [ I₁ (X.η q) ∘ Y.η (F.F₀ q) ]
  ; commute = λ f → glue ([ I ]-resp-square (X.commute f)) (Y.commute (F.F₁ f))
  }
  where module F = Functor F
        module X = NaturalTransformation X
        module Y = NaturalTransformation Y
        open Functor I renaming (F₀ to I₀; F₁ to I₁)
        open MR E

_∘ˡ_ : ∀ {G H : Functor C D} (F : Functor D E) → NaturalTransformation G H → NaturalTransformation (F ∘F G) (F ∘F H)
_∘ˡ_ F α = ntHelper record
  { η       = λ X → F₁ (η X)
  ; commute = λ f → [ F ]-resp-square (commute f)
  }
  where open Functor F
        open NaturalTransformation α

_∘ʳ_ : ∀ {G H : Functor D E} → NaturalTransformation G H → (F : Functor C D) → NaturalTransformation (G ∘F F) (H ∘F F)
_∘ʳ_ {D = D} {E = E} {G = G} {H = H} α F = ntHelper record
  { η       = λ X → η (F₀ X)
  ; commute = λ f → commute (F₁ f)
  }
  where open Functor F
        open NaturalTransformation α

id∘id⇒id : {C : Category o ℓ e} → NaturalTransformation {C = C} {D = C} (idF ∘F idF) idF
id∘id⇒id {C = C} = ntHelper record { η = λ _ → Category.id C ; commute = λ f → MR.id-comm-sym C {f = f} }

id⇒id∘id : {C : Category o ℓ e} → NaturalTransformation {C = C} {D = C} idF (idF ∘F idF)
id⇒id∘id {C = C} = ntHelper record { η = λ _ → Category.id C ; commute = λ f → MR.id-comm-sym C {f = f} }

module _ {F : Functor C D} where
  open Category.HomReasoning D
  open Functor F
  open Category D
  open MR D
  private module D = Category D

  F⇒F∘id : NaturalTransformation F (F ∘F idF)
  F⇒F∘id = ntHelper record { η = λ _ → D.id ; commute = λ _ → id-comm-sym }

  F⇒id∘F : NaturalTransformation F (idF ∘F F)
  F⇒id∘F = ntHelper record { η = λ _ → D.id ; commute = λ _ → id-comm-sym }

  F∘id⇒F : NaturalTransformation (F ∘F idF) F
  F∘id⇒F = ntHelper record { η = λ _ → D.id ; commute = λ _ → id-comm-sym }

  id∘F⇒F : NaturalTransformation (idF ∘F F) F
  id∘F⇒F = ntHelper record { η = λ _ → D.id ; commute = λ _ → id-comm-sym }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------
-- An alternative characterisation of the information ordering, along
-- with related results
------------------------------------------------------------------------

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

open import Prelude hiding (⊥)

module Partiality-monad.Inductive.Alternative-order
         {a} {A : Type a} where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)

open import Bijection equality-with-J using (_↔_)
open import Double-negation equality-with-J as DN
open import Equality.Path.Isomorphisms.Univalence equality-with-paths
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc
open import Monad equality-with-J
open import Nat equality-with-J
open import Univalence-axiom equality-with-J

open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Eliminators

------------------------------------------------------------------------
-- An alternative characterisation of λ x y → now x ⊑ y

-- This characterisation uses a technique from the first edition of
-- the HoTT book (Theorems 11.3.16 and 11.3.32).
--
-- The characterisation was developed together with Paolo Capriotti.

-- A binary relation, defined using structural recursion.

private

  now[_]≲-args : A → Arguments-nd (lsuc a) a A
  now[ x ]≲-args = record
    { P  = Proposition a
    ; Q  = λ P Q → proj₁ P → proj₁ Q
    ; pe = Prelude.⊥ , ⊥-propositional
    ; po = λ y → ∥ x ≡ y ∥ , truncation-is-proposition
    ; pl = λ { s (now-x≲s[_] , _) → ∥ ∃ (λ n → proj₁ (now-x≲s[ n ])) ∥
                                  , truncation-is-proposition
             }
    ; pa = λ now-x≲y now-x≲z now-x≲y→now-x≲z now-x≲z→now-x≲y →
                                            $⟨ record { to = now-x≲y→now-x≲z; from = now-x≲z→now-x≲y } ⟩
             proj₁ now-x≲y ⇔ proj₁ now-x≲z  ↝⟨ _↔_.to (⇔↔≡″ ext prop-ext) ⟩□
             now-x≲y ≡ now-x≲z              □
    ; ps = ps
    ; qr = λ { _ (now-x≲y , _) →
               now-x≲y  ↝⟨ id ⟩□
               now-x≲y  □
             }
    ; qt = λ { _ _ (P , _) (Q , _) (R , _) P→Q Q→R →
               P  ↝⟨ P→Q ⟩
               Q  ↝⟨ Q→R ⟩□
               R  □
             }
    ; qe = λ { _ (now-x≲⊥ , _) →
               Prelude.⊥  ↝⟨ ⊥-elim ⟩□
               now-x≲⊥    □
             }
    ; qu = λ { s (now-x≲s[_] , _) n →
               proj₁ now-x≲s[ n ]                ↝⟨ ∣_∣ ∘ (n ,_) ⟩□
               ∥ ∃ (λ n → proj₁ now-x≲s[ n ]) ∥  □
             }
    ; ql = λ { s ub is-ub (now-x≲s[_] , _) now-x≲ub now-x≲s[]→now-x≲ub →
               ∥ ∃ (λ n → proj₁ now-x≲s[ n ]) ∥  ↝⟨ Trunc.rec (proj₂ now-x≲ub) (uncurry now-x≲s[]→now-x≲ub) ⟩□
               proj₁ now-x≲ub                    □
             }
    ; qp = λ _ now-x≲z → Π-closure ext 1 λ _ →
                         proj₂ now-x≲z
    }
    where
    abstract
      ps : Is-set (Proposition a)
      ps = Is-set-∃-Is-proposition ext prop-ext

infix 4 now[_]≲_

now[_]≲_ : A → A ⊥ → Type a
now[ x ]≲ y = proj₁ (⊥-rec-nd now[ x ]≲-args y)

-- The relation is propositional.

now[]≲-propositional : ∀ {x y} → Is-proposition (now[ x ]≲ y)
now[]≲-propositional = proj₂ (⊥-rec-nd now[ _ ]≲-args _)

-- If a computation terminates with a certain value, then all larger
-- computations terminate with the same value (according to now[_]≲_).

larger-terminate-with-same-value≲ :
  ∀ {x y} → x ⊑ y → ∀ {z} → now[ z ]≲ x → now[ z ]≲ y
larger-terminate-with-same-value≲ x⊑y =
  ⊑-rec-nd now[ _ ]≲-args x⊑y

-- "Evaluation" lemmas for now[_]≲_.

now[]≲never : ∀ {x} → (now[ x ]≲ never) ≡ Prelude.⊥
now[]≲never {x} =
  now[ x ]≲ never  ≡⟨ cong proj₁ (⊥-rec-nd-never now[ x ]≲-args) ⟩∎
  Prelude.⊥        ∎

now[]≲now : ∀ {x y} → (now[ x ]≲ now y) ≡ ∥ x ≡ y ∥
now[]≲now {x} {y} =
  now[ x ]≲ now y  ≡⟨ cong proj₁ (⊥-rec-nd-now now[ x ]≲-args y) ⟩∎
  ∥ x ≡ y ∥        ∎

now[]≲⨆ : ∀ {x s} → (now[ x ]≲ ⨆ s) ≡ ∥ (∃ λ n → now[ x ]≲ s [ n ]) ∥
now[]≲⨆ {x} {s} =
  now[ x ]≲ ⨆ s                    ≡⟨ cong proj₁ (⊥-rec-nd-⨆ now[ x ]≲-args s) ⟩∎
  ∥ (∃ λ n → now[ x ]≲ s [ n ]) ∥  ∎

-- now[_]≲_ is pointwise equivalent to λ x y → now x ⊑ y.

now⊑≃now[]≲ : ∀ {x y} → (now x ⊑ y) ≃ (now[ x ]≲ y)
now⊑≃now[]≲ {x} {y} =
  _↔_.to (Eq.⇔↔≃ ext ⊑-propositional now[]≲-propositional)
    (record { to   = now x ⊑ y                                ↝⟨ larger-terminate-with-same-value≲ ⟩
                     (∀ {z} → now[ z ]≲ now x → now[ z ]≲ y)  ↝⟨ (λ hyp {_} eq → hyp (≡⇒→ (sym now[]≲now) eq)) ⟩
                     (∀ {z} → ∥ z ≡ x ∥ → now[ z ]≲ y)        ↝⟨ (λ hyp → hyp ∣ refl ∣) ⟩□
                     now[ x ]≲ y                              □
            ; from = ⊥-rec-⊥ from-args _
            })
  where
  from-args : Arguments-⊥ a A
  from-args = record
    { P  = λ y → now[ x ]≲ y → now x ⊑ y
    ; pe = now[ x ]≲ never  ↝⟨ ≡⇒↝ _ now[]≲never ⟩
           Prelude.⊥        ↝⟨ ⊥-elim ⟩□
           now x ⊑ never    □
    ; po = λ y →
             now[ x ]≲ now y  ↝⟨ ≡⇒↝ _ now[]≲now ⟩

             ∥ x ≡ y ∥        ↝⟨ Trunc.rec ⊑-propositional (

               x ≡ y               ↝⟨ cong now ⟩
               now x ≡ now y       ↝⟨ flip (subst (now x ⊑_)) (⊑-refl _) ⟩□
               now x ⊑ now y       □) ⟩□

             now x ⊑ now y    □
    ; pl = λ s now-x≲s→now-x⊑s →
             now[ x ]≲ ⨆ s                    ↝⟨ ≡⇒↝ _ now[]≲⨆ ⟩

             ∥ ∃ (λ n → now[ x ]≲ s [ n ]) ∥  ↝⟨ Trunc.rec ⊑-propositional (uncurry λ n now-x≲s[n] →

               now x                               ⊑⟨ now-x≲s→now-x⊑s n now-x≲s[n] ⟩
               s [ n ]                             ⊑⟨ upper-bound s n ⟩■
               ⨆ s                                 ■) ⟩□

             now x ⊑ ⨆ s                      □
    ; pp = λ _ → Π-closure ext 1 λ _ →
                 ⊑-propositional
    }

------------------------------------------------------------------------
-- Some properties that follow from the equivalence between now[_]≲_
-- and λ x y → now x ⊑ y

-- An equivalence between "now x ⊑ never" and an empty type.
--
-- This lemma was proved together with Paolo Capriotti.

now⊑never≃⊥ : {x : A} → (now x ⊑ never) ≃ Prelude.⊥ {ℓ = a}
now⊑never≃⊥ {x} =
  now x ⊑ never    ↝⟨ now⊑≃now[]≲ ⟩
  now[ x ]≲ never  ↝⟨ ≡⇒↝ _ now[]≲never ⟩□
  Prelude.⊥        □

-- Defined values of the form now x are never smaller than or equal to
-- never.
--
-- This lemma was proved together with Paolo Capriotti.

now⋢never : (x : A) → ¬ now x ⊑ never
now⋢never x =
  now x ⊑ never  ↔⟨ now⊑never≃⊥ ⟩
  Prelude.⊥      ↝⟨ ⊥-elim ⟩□
  ⊥₀             □

-- Defined values of the form now x are never equal to never.

now≢never : (x : A) → now x ≢ never
now≢never x =
  now x ≡ never                  ↝⟨ _≃_.from equality-characterisation-⊥ ⟩
  now x ⊑ never × now x ⊒ never  ↝⟨ proj₁ ⟩
  now x ⊑ never                  ↝⟨ now⋢never x ⟩□
  ⊥₀                             □

-- There is an equivalence between "now x is smaller than or equal
-- to now y" and "x is merely equal to y".

now⊑now≃∥≡∥ : {x y : A} → (now x ⊑ now y) ≃ ∥ x ≡ y ∥
now⊑now≃∥≡∥ {x} {y} =
  now x ⊑ now y    ↝⟨ now⊑≃now[]≲ ⟩
  now[ x ]≲ now y  ↝⟨ ≡⇒↝ _ now[]≲now ⟩□
  ∥ x ≡ y ∥        □

-- There is an equivalence between "now x is equal to now y" and "x
-- is merely equal to y".

now≡now≃∥≡∥ : {x y : A} → (now x ≡ now y) ≃ ∥ x ≡ y ∥
now≡now≃∥≡∥ {x} {y} =
  now x ≡ now y                  ↝⟨ inverse equality-characterisation-⊥ ⟩
  now x ⊑ now y × now x ⊒ now y  ↝⟨ now⊑now≃∥≡∥ ×-cong now⊑now≃∥≡∥ ⟩
  ∥ x ≡ y ∥ × ∥ y ≡ x ∥          ↝⟨ _↔_.to (Eq.⇔↔≃ ext (×-closure 1 truncation-is-proposition
                                                                    truncation-is-proposition)
                                                       truncation-is-proposition)
                                           (record { to = proj₁
                                                   ; from = λ ∥x≡y∥ → ∥x≡y∥ , ∥∥-map sym ∥x≡y∥
                                                   }) ⟩□
  ∥ x ≡ y ∥                      □

-- There is an equivalence between "now x is smaller than or equal to
-- now y" and "now x is equal to now y".

now⊑now≃now≡now : {x y : A} → (now x ⊑ now y) ≃ (now x ≡ now y)
now⊑now≃now≡now {x} {y} =
  now x ⊑ now y  ↝⟨ now⊑now≃∥≡∥ ⟩
  ∥ x ≡ y ∥      ↝⟨ inverse now≡now≃∥≡∥ ⟩□
  now x ≡ now y  □

-- A computation can terminate with at most one value.

termination-value-merely-unique :
  ∀ {x y z} → x ⇓ y → x ⇓ z → ∥ y ≡ z ∥
termination-value-merely-unique {x} {y} {z} x⇓y x⇓z =
  _≃_.to now≡now≃∥≡∥ (
    now y  ≡⟨ sym x⇓y ⟩
    x      ≡⟨ x⇓z ⟩∎
    now z  ∎)

-- There is an equivalence between now x ⊑ ⨆ s and
-- ∥ ∃ (λ n → now x ⊑ s [ n ]) ∥.

now⊑⨆≃∥∃now⊑∥ :
  ∀ {s : Increasing-sequence A} {x} →
  (now x ⊑ ⨆ s) ≃ ∥ ∃ (λ n → now x ⊑ s [ n ]) ∥
now⊑⨆≃∥∃now⊑∥ {s} {x} =
  now x ⊑ ⨆ s                      ↝⟨ now⊑≃now[]≲ ⟩
  now[ x ]≲ ⨆ s                    ↝⟨ ≡⇒↝ _ now[]≲⨆ ⟩
  ∥ (∃ λ n → now[ x ]≲ s [ n ]) ∥  ↝⟨ ∥∥-cong (∃-cong λ _ → inverse now⊑≃now[]≲) ⟩□
  ∥ (∃ λ n → now x ⊑ s [ n ]) ∥    □

-- If x is larger than or equal to now y, then x is equal to now y.

now⊑→⇓ : ∀ {x} {y : A} → now y ⊑ x → x ⇓ y
now⊑→⇓ {x} {y} = ⊥-rec-⊥ (record
  { P  = λ x → now y ⊑ x → x ⇓ y
  ; pe = now y ⊑ never  ↝⟨ now⋢never y ⟩
         Prelude.⊥      ↝⟨ ⊥-elim ⟩□
         never ≡ now y  □
  ; po = λ x →
           now y ⊑ now x  ↔⟨ now⊑now≃∥≡∥ ⟩
           ∥ y ≡ x ∥      ↝⟨ ∥∥-map sym ⟩
           ∥ x ≡ y ∥      ↝⟨ Trunc.rec ⊥-is-set (cong now) ⟩□
           now x ≡ now y  □
  ; pl = λ s hyp →
           now y ⊑ ⨆ s                                  ↝⟨ (λ p → p , _≃_.to now⊑⨆≃∥∃now⊑∥ p) ⟩
           now y ⊑ ⨆ s × ∥ (∃ λ n → now y ⊑ s [ n ]) ∥  ↝⟨ uncurry (λ p → Trunc.rec ⊥-is-set (uncurry λ n →

               now y ⊑ s [ n ]                               ↝⟨ (λ now⊑ _ n≤m → ⊑-trans now⊑ (later-larger s n≤m)) ⟩
               (∀ m → n ≤ m → now y ⊑ s [ m ])               ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ → hyp _) ⟩
               (∀ m → n ≤ m → s [ m ] ≡ now y)               ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ → flip (subst (_ ⊑_)) (⊑-refl _)) ⟩
               (∀ m → n ≤ m → s [ m ] ⊑ now y)               ↝⟨ upper-bound-≤→upper-bound s ⟩
               (∀ n → s [ n ] ⊑ now y)                       ↝⟨ least-upper-bound _ _ ⟩
               ⨆ s ⊑ now y                                   ↝⟨ flip antisymmetry p ⟩□
               ⨆ s ≡ now y                                   □)) ⟩□

           ⨆ s ≡ now y                                  □
  ; pp = λ _ → Π-closure ext 1 λ _ →
               ⊥-is-set
  })
  x

-- If a computation terminates with a certain value, then all larger
-- computations terminate with the same value.
--
-- Capretta proved a similar result in "General Recursion via
-- Coinductive Types".

larger-terminate-with-same-value : {x y : A ⊥} → x ⊑ y → x ≼ y
larger-terminate-with-same-value now-x⊑y _ refl = now⊑→⇓ now-x⊑y

-- If one element in an increasing sequence terminates with a given
-- value, then this value is the sequence's least upper bound.

terminating-element-is-⨆ :
  ∀ (s : Increasing-sequence A) {n x} →
  s [ n ] ⇓ x → ⨆ s ⇓ x
terminating-element-is-⨆ s {n} {x} =
  larger-terminate-with-same-value (upper-bound s n) x

-- The relation _≼_ is contained in _⊑_.
--
-- Capretta proved a similar result in "General Recursion via
-- Coinductive Types".

≼→⊑ : {x y : A ⊥} → x ≼ y → x ⊑ y
≼→⊑ {x} {y} = ⊥-rec-⊥
  (record
     { P  = λ x → x ≼ y → x ⊑ y
     ; pe = never ≼ y  ↝⟨ (λ _ → never⊑ y) ⟩□
            never ⊑ y   □
     ; po = λ x →
              now x ≼ y              ↝⟨ (λ hyp → hyp x refl) ⟩
              y ⇓ x                  ↔⟨ inverse equality-characterisation-⊥ ⟩
              y ⊑ now x × y ⊒ now x  ↝⟨ proj₂ ⟩□
              now x ⊑ y              □
     ; pl = λ s s≼y→s⊑y →
              ⨆ s ≼ y                        ↝⟨ id ⟩
              (∀ z → ⨆ s ⇓ z → y ⇓ z)        ↝⟨ (λ hyp n z →

                s [ n ] ⇓ z                       ↝⟨ larger-terminate-with-same-value (upper-bound s n) z ⟩
                ⨆ s ⇓ z                           ↝⟨ hyp z ⟩□
                y ⇓ z                             □) ⟩

              (∀ n z → s [ n ] ⇓ z → y ⇓ z)  ↝⟨ id ⟩
              (∀ n → s [ n ] ≼ y)            ↝⟨ (λ hyp n → s≼y→s⊑y n (hyp n)) ⟩
              (∀ n → s [ n ] ⊑ y)            ↝⟨ least-upper-bound s y ⟩□
              ⨆ s ⊑ y                        □
     ; pp = λ _ →
              Π-closure ext 1 λ _ →
              ⊑-propositional
     })
  x

-- The two relations _≼_ and _⊑_ are pointwise equivalent.
--
-- Capretta proved a similar result in "General Recursion via
-- Coinductive Types".

≼≃⊑ : {x y : A ⊥} → (x ≼ y) ≃ (x ⊑ y)
≼≃⊑ = _↔_.to (Eq.⇔↔≃ ext ≼-propositional ⊑-propositional)
             (record { to   = ≼→⊑
                     ; from = larger-terminate-with-same-value
                     })

-- An alternative characterisation of _⇓_.

⇓≃now⊑ : ∀ {x} {y : A} → (x ⇓ y) ≃ (now y ⊑ x)
⇓≃now⊑ {x} {y} =
  _↔_.to (Eq.⇔↔≃ ext ⊥-is-set ⊑-propositional) (record
    { to   = x ≡ now y              ↔⟨ inverse equality-characterisation-⊥ ⟩
             x ⊑ now y × x ⊒ now y  ↝⟨ proj₂ ⟩□
             now y ⊑ x              □
    ; from = now y ⊑ x                  ↝⟨ larger-terminate-with-same-value ⟩
             (∀ z → now y ⇓ z → x ⇓ z)  ↝⟨ (λ hyp → hyp y refl) ⟩□
             x ⇓ y                      □
    })

-- Another alternative characterisation of _⇓_.

⇓≃now[]≲ : ∀ {x y} → (x ⇓ y) ≃ (now[ y ]≲ x)
⇓≃now[]≲ {x} {y} =
  x ⇓ y        ↝⟨ ⇓≃now⊑ ⟩
  now y ⊑ x    ↝⟨ now⊑≃now[]≲ ⟩□
  now[ y ]≲ x  □

-- Two corollaries of ⇓≃now[]≲.

never⇓≃⊥ : {x : A} → (never ⇓ x) ≃ Prelude.⊥ {ℓ = a}
never⇓≃⊥ {x = x} =
  never ≡ now x    ↝⟨ ⇓≃now[]≲ ⟩
  now[ x ]≲ never  ↝⟨ ≡⇒↝ _ now[]≲never ⟩□
  Prelude.⊥        □

⨆⇓≃∥∃⇓∥ :
  ∀ {s : Increasing-sequence A} {x} →
  (⨆ s ⇓ x) ≃ ∥ ∃ (λ n → s [ n ] ⇓ x) ∥
⨆⇓≃∥∃⇓∥ {s} {x} =
  ⨆ s ⇓ x                          ↝⟨ ⇓≃now[]≲ ⟩
  now[ x ]≲ ⨆ s                    ↝⟨ ≡⇒↝ _ now[]≲⨆ ⟩
  ∥ ∃ (λ n → now[ x ]≲ s [ n ]) ∥  ↝⟨ ∥∥-cong (∃-cong λ _ → inverse ⇓≃now[]≲) ⟩□
  ∥ ∃ (λ n → s [ n ] ⇓ x) ∥        □

-- If x does not terminate, then x is equal to never.

¬⇓→⇑ : {x : A ⊥} → ¬ (∃ λ y → x ⇓ y) → x ⇑
¬⇓→⇑ {x} = ⊥-rec-⊥
  (record
     { P  = λ x → ¬ (∃ λ y → x ⇓ y) → x ⇑
     ; pe = ¬ ∃ (never ⇓_)  ↝⟨ const refl ⟩□
            never ⇑         □
     ; po = λ x →
              ¬ ∃ (now x ⇓_) ↝⟨ _$ (x , refl) ⟩
              ⊥₀             ↝⟨ ⊥-elim ⟩□
              now x ⇑        □
     ; pl = λ s ih →
              ¬ ∃ (⨆ s ⇓_)                           ↔⟨ →-cong ext (∃-cong (λ _ → ⨆⇓≃∥∃⇓∥)) F.id ⟩
              ¬ ∃ (λ x → ∥ ∃ (λ n → s [ n ] ⇓ x) ∥)  ↝⟨ (λ { hyp (n , x , s[n]⇓x) → hyp (x , ∣ n , s[n]⇓x ∣) }) ⟩
              ¬ ∃ (λ n → ∃ λ x → s [ n ] ⇓ x)        ↝⟨ (λ hyp n → ih n (hyp ∘ (n ,_))) ⟩
              (∀ n → s [ n ] ⇑)                      ↝⟨ sym ∘ _↔_.to equality-characterisation-increasing ⟩
              constˢ never ≡ s                       ↝⟨ flip (subst (λ s → ⨆ s ⇑)) ⨆-const ⟩□
              ⨆ s ⇑                                  □
     ; pp = λ _ → Π-closure ext 1 λ _ →
                  ⊥-is-set
     })
  x

-- In the double-negation monad a computation is either terminating or
-- non-terminating.

now-or-never : (x : A ⊥) → ¬ ¬ ((∃ λ y → x ⇓ y) ⊎ x ⇑)
now-or-never x = run (map (⊎-map id ¬⇓→⇑) excluded-middle)

-- _⊑_ is a flat order, in the sense that distinct elements that are
-- distinct from never are unrelated.

flat-order : {x y : A ⊥} → x ≢ y → ¬ x ⇑ → ¬ y ⇑ → ¬ (x ⊑ y)
flat-order {x} {y} x≢y never≢x never≢y x⊑y = ¬¬¬⊥ $
  ¬⇑→¬¬⇓ never≢x >>= λ x⇓ →
  ¬⇑→¬¬⇓ never≢y >>= λ y⇓ →
  return (⊥-elim $ ¬x⇓×y⇓ (x⇓ , y⇓))
  where
  -- The computations x and y cannot both terminate.

  ¬x⇓×y⇓ : ¬ ((∃ λ z → x ⇓ z) × (∃ λ z → y ⇓ z))
  ¬x⇓×y⇓ ((xz , refl) , (yz , refl)) = x≢y (
    now xz      ≡⟨ _≃_.to now⊑now≃now≡now (

        now xz       ⊑⟨ x⊑y ⟩■
        now yz       ■) ⟩∎

    now yz      ∎)

  -- Computations that fail to be equal to never do not fail to
  -- terminate.

  ¬⇑→¬¬⇓ : {x : A ⊥} → ¬ x ⇑ → ¬¬ (∃ λ y → x ⇓ y)
  run (¬⇑→¬¬⇓ ¬x⇑) = ¬x⇑ ∘ ¬⇓→⇑

-- Some "constructors" for □.

□-never :
  ∀ {ℓ} {P : A → Type ℓ} →
  □ P never
□-never {P = P} y =
  never ⇓ y        ↔⟨ ⇓≃now[]≲ ⟩
  now[ y ]≲ never  ↔⟨ ≡⇒↝ bijection now[]≲never ⟩
  Prelude.⊥        ↝⟨ ⊥-elim ⟩□
  P y              □

□-now :
  ∀ {ℓ} {P : A → Type ℓ} {x} →
  Is-proposition (P x) →
  P x → □ P (now x)
□-now {P = P} {x} P-prop p y =
  now x ⇓ y  ↔⟨ now≡now≃∥≡∥ ⟩
  ∥ x ≡ y ∥  ↝⟨ (λ ∥x≡y∥ →
                   Trunc.rec (Trunc.rec (H-level-propositional ext 1)
                                        (λ x≡y → subst (Is-proposition ∘ P) x≡y P-prop)
                                        ∥x≡y∥)
                             (λ x≡y → subst P x≡y p)
                             ∥x≡y∥) ⟩□
  P y        □

□-⨆ :
  ∀ {ℓ} {P : A → Type ℓ} →
  (∀ x → Is-proposition (P x)) →
  ∀ {s} → (∀ n → □ P (s [ n ])) → □ P (⨆ s)
□-⨆ {P = P} P-prop {s} p y =
  ⨆ s ⇓ y                    ↔⟨ ⨆⇓≃∥∃⇓∥ ⟩
  ∥ ∃ (λ n → s [ n ] ⇓ y) ∥  ↝⟨ Trunc.rec (P-prop y) (uncurry λ n s[n]⇓y → p n y s[n]⇓y) ⟩□
  P y                        □

-- One "non-constructor" and one "constructor" for ◇.

◇-never :
  ∀ {ℓ} {P : A → Type ℓ} →
  ¬ ◇ P never
◇-never {P = P} =
  ◇ P never                      ↝⟨ id ⟩
  ∥ (∃ λ y → never ⇓ y × P y) ∥  ↝⟨ Trunc.rec ⊥-propositional (now≢never _ ∘ sym ∘ proj₁ ∘ proj₂) ⟩□
  ⊥₀                             □

◇-⨆ :
  ∀ {ℓ} {P : A → Type ℓ} →
  ∀ {s n} → ◇ P (s [ n ]) → ◇ P (⨆ s)
◇-⨆ {P = P} =
  ∥∥-map (Σ-map id (λ {x} → Σ-map {Q = λ _ → P x}
                                  (terminating-element-is-⨆ _) id))

------------------------------------------------------------------------
-- An alternative characterisation of _⊑_

-- This characterisation uses a technique from the first edition of
-- the HoTT book (Theorems 11.3.16 and 11.3.32).
--
-- The characterisation was developed together with Paolo Capriotti.

-- A binary relation, defined using structural recursion.

private

  ≲-args : Arguments-nd (lsuc a) a A
  ≲-args = record
    { P  = A ⊥ → Proposition a
    ; Q  = λ P Q → ∀ z → proj₁ (Q z) → proj₁ (P z)
    ; pe = λ _ → ↑ _ ⊤ , ↑-closure 1 (mono₁ 0 ⊤-contractible)
    ; po = λ x y → ⊥-rec-nd now[ x ]≲-args y
    ; pl = λ { _ (s[_]≲ , _) y → (∀ n → proj₁ (s[ n ]≲ y))
                               , Π-closure ext 1 λ n →
                                 proj₂ (s[ n ]≲ y)
             }
    ; pa = λ x≲ y≲ y≲→x≲ x≲→y≲ → ⟨ext⟩ λ z →
                                          $⟨ record { to = x≲→y≲ z; from = y≲→x≲ z } ⟩
             proj₁ (x≲ z) ⇔ proj₁ (y≲ z)  ↝⟨ _↔_.to (⇔↔≡″ ext prop-ext) ⟩□
             x≲ z ≡ y≲ z                  □
    ; ps = ps
    ; qr = λ _ x≲ z →
             proj₁ (x≲ z)  ↝⟨ id ⟩□
             proj₁ (x≲ z)  □
    ; qt = λ _ _ P Q R Q→P R→Q z →
             proj₁ (R z)  ↝⟨ R→Q z ⟩
             proj₁ (Q z)  ↝⟨ Q→P z ⟩□
             proj₁ (P z)  □
    ; qe = λ _ ⊥≲ z →
             proj₁ (⊥≲ z)  ↝⟨ _ ⟩□
             ↑ _ ⊤         □
    ; qu = λ { s (s[_]≲ , _) n z →
               (∀ m → proj₁ (s[ m ]≲ z))  ↝⟨ (_$ n) ⟩□
               proj₁ (s[ n ]≲ z)          □
             }
    ; ql = λ { _ _ _ (s[_]≲ , _) ub≲ ub≲→s[]≲ z →
               proj₁ (ub≲ z)              ↝⟨ flip (flip ub≲→s[]≲ z) ⟩□
               (∀ n → proj₁ (s[ n ]≲ z))  □
             }
    ; qp = λ x≲ y≲ → Π-closure ext 1 λ z →
                     Π-closure ext 1 λ _ →
                     proj₂ (x≲ z)
    }
    where
    abstract
      ps : Is-set (A ⊥ → Proposition a)
      ps =
        Π-closure ext 2 λ _ →
        Is-set-∃-Is-proposition ext prop-ext

infix 4 _≲_

_≲_ : A ⊥ → A ⊥ → Type a
x ≲ y = proj₁ (⊥-rec-nd ≲-args x y)

-- The relation is propositional.

≲-propositional : ∀ x y → Is-proposition (x ≲ y)
≲-propositional x y = proj₂ (⊥-rec-nd ≲-args x y)

-- A form of transitivity involving _⊑_ and _≲_.

⊑≲-trans : ∀ {x y} (z : A ⊥) → x ⊑ y → y ≲ z → x ≲ z
⊑≲-trans z x⊑y = ⊑-rec-nd ≲-args x⊑y z

-- "Evaluation" lemmas for _≲_.

never≲ : ∀ {y} → (never ≲ y) ≡ ↑ _ ⊤
never≲ {y} = cong (proj₁ ∘ (_$ _)) (
  ⊥-rec-nd ≲-args never  ≡⟨ ⊥-rec-nd-never ≲-args ⟩∎
  (λ _ → ↑ _ ⊤ , _)      ∎)

⨆≲ : ∀ {s y} → (⨆ s ≲ y) ≡ ∀ n → s [ n ] ≲ y
⨆≲ {s} {y} = cong (proj₁ ∘ (_$ _)) (
  ⊥-rec-nd ≲-args (⨆ s)            ≡⟨ ⊥-rec-nd-⨆ ≲-args s ⟩∎
  (λ y → (∀ n → s [ n ] ≲ y) , _)  ∎)

now≲ : ∀ {x y} → (now x ≲ y) ≡ (now[ x ]≲ y)
now≲ {x} {y} =
  now x ≲ y    ≡⟨ cong (proj₁ ∘ (_$ _)) (⊥-rec-nd-now ≲-args x) ⟩∎
  now[ x ]≲ y  ∎

now≲never : ∀ {x} → (now x ≲ never) ≡ Prelude.⊥
now≲never {x} =
  now x ≲ never    ≡⟨ now≲ ⟩
  now[ x ]≲ never  ≡⟨ now[]≲never ⟩∎
  Prelude.⊥        ∎

now≲now : ∀ {x y} → (now x ≲ now y) ≡ ∥ x ≡ y ∥
now≲now {x} {y} =
  now x ≲ now y    ≡⟨ now≲ ⟩
  now[ x ]≲ now y  ≡⟨ now[]≲now ⟩∎
  ∥ x ≡ y ∥        ∎

now≲⨆ : ∀ {x s} → (now x ≲ ⨆ s) ≡ ∥ (∃ λ n → now x ≲ s [ n ]) ∥
now≲⨆ {x} {s} =
  now x ≲ ⨆ s                      ≡⟨ now≲ ⟩
  now[ x ]≲ ⨆ s                    ≡⟨ now[]≲⨆ ⟩
  ∥ (∃ λ n → now[ x ]≲ s [ n ]) ∥  ≡⟨ cong (λ P → ∥ ∃ P ∥) (⟨ext⟩ λ _ → sym now≲) ⟩∎
  ∥ (∃ λ n → now x ≲ s [ n ]) ∥    ∎

-- _≲_ is reflexive.

≲-refl : ∀ x → x ≲ x
≲-refl = ⊥-rec-⊥ (record
  { pe =                $⟨ _ ⟩
         ↑ _ ⊤          ↝⟨ ≡⇒↝ bijection $ sym never≲ ⟩□
         never ≲ never  □
  ; po = λ x →            $⟨ ∣ refl ∣ ⟩
           ∥ x ≡ x ∥      ↝⟨ ≡⇒↝ bijection $ sym now≲now ⟩□
           now x ≲ now x  □
  ; pl = λ s →
           (∀ n → s [ n ] ≲ s [ n ])  ↝⟨ (λ s≲s n → ⨆-lemma s (s [ n ]) n (s≲s n)) ⟩
           (∀ n → s [ n ] ≲ ⨆ s)      ↔⟨ ≡⇒↝ bijection $ sym ⨆≲ ⟩□
           ⨆ s ≲ ⨆ s                  □
  ; pp = λ x → ≲-propositional x x
  })
  where
  ⨆-lemma : ∀ s x n → x ≲ s [ n ] → x ≲ ⨆ s
  ⨆-lemma s = ⊥-rec-⊥
    (record
       { P  = λ x → ∀ n → x ≲ s [ n ] → x ≲ ⨆ s
       ; pe = λ n →
                never ≲ s [ n ]  ↔⟨ ≡⇒↝ bijection $ never≲ ⟩
                ↑ _ ⊤            ↔⟨ ≡⇒↝ bijection $ sym never≲ ⟩□
                never ≲ ⨆ s      □
       ; po = λ x n →
                now x ≲ s [ n ]                ↝⟨ ∣_∣ ∘ (n ,_) ⟩
                ∥ (∃ λ n → now x ≲ s [ n ]) ∥  ↔⟨ ≡⇒↝ bijection $ sym now≲⨆ ⟩□
                now x ≲ ⨆ s                    □
       ; pl = λ s′ →
                (∀ m n → s′ [ m ] ≲ s [ n ] → s′ [ m ] ≲ ⨆ s)  ↝⟨ (λ hyp n s′≲s m → hyp m n (s′≲s m)) ⟩

                (∀ n → (∀ m → s′ [ m ] ≲ s [ n ]) →
                       (∀ m → s′ [ m ] ≲ ⨆ s))                 ↝⟨ ∀-cong _ (λ _ →
                                                                    ≡⇒↝ _ $ sym $ cong₂ (λ x y → x → y) ⨆≲ ⨆≲) ⟩□
                (∀ n → ⨆ s′ ≲ s [ n ] → ⨆ s′ ≲ ⨆ s)            □
       ; pp = λ x → Π-closure ext 1 λ _ →
                    Π-closure ext 1 λ _ →
                    ≲-propositional x (⨆ s)
       })

-- _⊑_ and _≲_ are pointwise equivalent.

⊑≃≲ : ∀ {x y} → (x ⊑ y) ≃ (x ≲ y)
⊑≃≲ {x} {y} =
  _↔_.to (Eq.⇔↔≃ ext ⊑-propositional (≲-propositional x y))
    (record { to   = λ x⊑y → ⊑≲-trans _ x⊑y (≲-refl y)
            ; from = ⊥-rec-⊥ from-args _ _
            })
  where
  from-args : Arguments-⊥ a A
  from-args = record
    { P  = λ x → ∀ y → x ≲ y → x ⊑ y
    ; pe = λ y _ → never⊑ y
    ; po = λ x y →
             now x ≲ y    ↝⟨ ≡⇒↝ _ now≲ ⟩
             now[ x ]≲ y  ↔⟨ inverse now⊑≃now[]≲ ⟩□
             now x ⊑ y    □
    ; pl = λ s s≲→s⊑ y →
             ⨆ s ≲ y              ↝⟨ ≡⇒↝ _ ⨆≲ ⟩
             (∀ n → s [ n ] ≲ y)  ↝⟨ (λ s[_]≲y n → s≲→s⊑ n y s[ n ]≲y) ⟩
             (∀ n → s [ n ] ⊑ y)  ↝⟨ least-upper-bound s y ⟩□
             ⨆ s ⊑ y              □
    ; pp = λ _ → Π-closure ext 1 λ _ →
                 Π-closure ext 1 λ _ →
                 ⊑-propositional
    }

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
------------------------------------------------------------------------------
-- Testing the translation of the universal quantified propositional symbols
------------------------------------------------------------------------------

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

module PropositionalSymbol where

postulate D : Set

postulate id : {P : Set} → P → P
{-# ATP prove id #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
-- 2014-06-02 Andrea & Andreas

module _ where

open import Common.Equality
open import Common.Product

postulate
  A : Set
  F : Set → Set

test : let M : Set
           M = _
           N : Set × Set → Set
           N = _
       in  ∀ {X : Set}
           → M ≡ F (N (X , X))
           × N (A , A) ≡ A
test = refl , refl

-- Here, we can prune the argument of N,
-- since M does not depend on X,
-- and the argument is a pair with a bad rigid
-- in *each* component.


text:
-- Semantics of syntactic kits and explicit substitutions
module Semantics.Substitution.Kits where

open import Syntax.Types
open import Syntax.Context renaming (_,_ to _,,_)
open import Syntax.Terms
open import Syntax.Substitution.Kits

open import Semantics.Types
open import Semantics.Context
open import Semantics.Terms

open import CategoryTheory.Categories
open import CategoryTheory.Instances.Reactive renaming (top to Top)
open import CategoryTheory.Functor
open import CategoryTheory.Comonad
open import TemporalOps.Diamond
open import TemporalOps.Box
open import TemporalOps.Linear

open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality as ≡
    using (_≡_ ; refl)

open Comonad W-□
private module F-□ = Functor F-□

-- Semantic interpretation of kits, grouping together
-- lemmas for the kit operations
record ⟦Kit⟧ {𝒮 : Schema} (k : Kit 𝒮) : Set where
    open Kit k
    field
        -- Interpretation of the syntactic entity of the given scheme
        ⟦_⟧ : ∀{A Δ} -> 𝒮 Δ A -> ⟦ Δ ⟧ₓ ⇴ ⟦ A ⟧ⱼ
        -- Variable conversion lemma
        ⟦𝓋⟧ : ∀ A Δ
           -> ⟦ 𝓋 {Δ ,, A} top ⟧ ≈ π₂
        -- Term conversion lemma
        ⟦𝓉⟧ : ∀{A Δ} (T : 𝒮 Δ A)
           -> ⟦ 𝓉 T ⟧ₘ ≈ ⟦ T ⟧
        -- Weakening map lemma
        ⟦𝓌⟧ : ∀ B {Δ A} (T : 𝒮 Δ A)
           -> ⟦ 𝓌 {B} T ⟧ ≈ ⟦ T ⟧ ∘ π₁
        -- Context stabilisation lemma
        ⟦𝒶⟧ : ∀{A Δ} (T : 𝒮 Δ (A always))
           -> F-□.fmap ⟦ 𝒶 T ⟧ ∘ ⟦ Δ ˢ⟧□ ≈ δ.at ⟦ A ⟧ₜ ∘ ⟦ T ⟧

-- | Interpretation of substitutions and combinators
module ⟦K⟧ {𝒮} {k : Kit 𝒮} (⟦k⟧ : ⟦Kit⟧ k) where
    open ⟦Kit⟧ ⟦k⟧
    open Kit k

    -- Denotation of substitutions as a map between contexts
    ⟦subst⟧ : ∀{Γ Δ} -> Subst 𝒮 Γ Δ -> ⟦ Δ ⟧ₓ ⇴ ⟦ Γ ⟧ₓ
    ⟦subst⟧ ●       = !
    ⟦subst⟧ (σ ▸ T) = ⟨ ⟦subst⟧ σ , ⟦ T ⟧ ⟩

    -- Simplified context stabilisation lemma for non-boxed stabilisation
    ⟦𝒶⟧′ : ∀{A Δ} (T : 𝒮 Δ (A always))
       -> ⟦ 𝒶 T ⟧ ∘ ⟦ Δ ˢ⟧ ≈ ⟦ T ⟧
    ⟦𝒶⟧′ {A} {Δ} T {n} {⟦Δ⟧} rewrite ⟦ˢ⟧-factor Δ {n} {⟦Δ⟧}
                           = □-≡ n n (⟦𝒶⟧ T) n

    -- Denotation of weakening
    ⟦⁺⟧ : ∀ A {Γ Δ} -> (σ : Subst 𝒮 Γ Δ)
       -> ⟦subst⟧ (_⁺_ {A} σ k) ≈ ⟦subst⟧ σ ∘ π₁
    ⟦⁺⟧ A ● = refl
    ⟦⁺⟧ A (_▸_ {B} σ T) {n} {a} rewrite ⟦⁺⟧ A σ {n} {a}
                                     | ⟦𝓌⟧ A T {n} {a} = refl
    -- Denotation of lifting
    ⟦↑⟧ : ∀ A {Δ Γ} -> (σ : Subst 𝒮 Γ Δ)
       -> ⟦subst⟧ (_↑_ {A} σ k) ≈ (⟦subst⟧ σ * id)
    ⟦↑⟧ A {Δ} ● {n} {a} rewrite ⟦𝓋⟧ A Δ {n} {a} = refl
    ⟦↑⟧ A {Δ} (σ ▸ T) {n} {a} rewrite ⟦⁺⟧ A σ {n} {a}
                                   | ⟦𝓌⟧ A T {n} {a}
                                   | ⟦𝓋⟧ A Δ {n} {a} = refl

    -- Denotation of stabilisation (naturality condition for ⟦_ˢ⟧□)
    ⟦↓ˢ⟧ : ∀ {Γ Δ} -> (σ : Subst 𝒮 Γ Δ)
       -> F-□.fmap (⟦subst⟧ (σ ↓ˢ k)) ∘ ⟦ Δ ˢ⟧□ ≈ ⟦ Γ ˢ⟧□ ∘ ⟦subst⟧ σ
    ⟦↓ˢ⟧ ● = refl
    ⟦↓ˢ⟧ (_▸_ {A now} σ T) {n} {a} rewrite ⟦↓ˢ⟧ σ {n} {a} = refl
    ⟦↓ˢ⟧ {Δ = Δ} (_▸_ {A always}{Γ} σ T) {n} {a}  = ext lemma
        where
        lemma : ∀ l -> (F-□.fmap (⟦subst⟧ ((σ ▸ T) ↓ˢ k)) ∘ ⟦ Δ ˢ⟧□) n a l
                     ≡ (⟦ Γ ,, A always ˢ⟧□ ∘ ⟦subst⟧ (σ ▸ T)) n a l
        lemma l rewrite □-≡ n l (⟦↓ˢ⟧ σ {n} {a}) l
                      | □-≡ n l (⟦𝒶⟧ T {n} {a}) l = refl

    -- Simplified denotation of stabilisation
    ⟦↓ˢ⟧′ : ∀ {Γ Δ} -> (σ : Subst 𝒮 Γ Δ)
       -> ⟦subst⟧ (σ ↓ˢ k) ∘ ⟦ Δ ˢ⟧ ≈ ⟦ Γ ˢ⟧ ∘ ⟦subst⟧ σ
    ⟦↓ˢ⟧′ {Γ} {Δ} σ {n} {a} rewrite ⟦ˢ⟧-factor Δ {n} {a}
                                | □-≡ n n (⟦↓ˢ⟧ σ {n} {a}) n
                                | ⟦ˢ⟧-factor Γ {n} {(⟦subst⟧ σ n a)} = refl

    -- Denotation of stabilisation idempotence
    ⟦ˢˢ⟧ : ∀ Γ -> F-□.fmap (⟦subst⟧ (Γ ˢˢₛ k)) ∘ ⟦ Γ ˢ ˢ⟧□ ∘ ⟦ Γ ˢ⟧ ≈ ⟦ Γ ˢ⟧□
    ⟦ˢˢ⟧ ∙ = refl
    ⟦ˢˢ⟧ (Γ ,, B now) = ⟦ˢˢ⟧ Γ
    ⟦ˢˢ⟧ (Γ ,, B always) {n} {⟦Γˢ⟧ , □⟦B⟧} = ext lemma
        where
        lemma : ∀ l → (F-□.fmap (⟦subst⟧ ((Γ ,, B always) ˢˢₛ k))
                        ∘ ⟦ (Γ ,, B always) ˢ ˢ⟧□
                        ∘ ⟦ Γ ,, B always ˢ⟧) n (⟦Γˢ⟧ , □⟦B⟧) l
                    ≡ (⟦ Γ ˢ⟧□ n ⟦Γˢ⟧ l , □⟦B⟧)
        lemma l rewrite ⟦𝓋⟧ (B always) (Γ ˢ ˢ) {l} {⟦ Γ ˢ ˢ⟧□ n (⟦ Γ ˢ⟧ n ⟦Γˢ⟧) l , □⟦B⟧}
                      | ⟦⁺⟧ (B always) (Γ ˢˢₛ k) {l} {(⟦ Γ ˢ ˢ⟧□ n (⟦ Γ ˢ⟧ n ⟦Γˢ⟧) l , □⟦B⟧)}
                      | □-≡ n l (⟦ˢˢ⟧ Γ {n} {⟦Γˢ⟧}) l = refl

    -- Denotation of identity substitution
    ⟦idₛ⟧ : ∀ {Γ} -> ⟦subst⟧ (idₛ {Γ} k) ≈ id
    ⟦idₛ⟧ {∙} = refl
    ⟦idₛ⟧ {Γ ,, A} {n} {⟦Γ⟧ , ⟦A⟧}
        rewrite ⟦⁺⟧ A {Γ} (idₛ k) {n} {⟦Γ⟧ , ⟦A⟧}
              | ⟦idₛ⟧ {Γ} {n} {⟦Γ⟧}
              | ⟦𝓋⟧ A Γ {n} {⟦Γ⟧ , ⟦A⟧} = refl

    -- | Other lemmas

    -- Substitution by the Γ ˢ ⊆ Γ subcontext substitution is the same as
    -- stabilising the context
    ⟦subst⟧-Γˢ⊆Γ : ∀ Γ -> ⟦subst⟧ (Γˢ⊆Γ Γ ⊆ₛ k) ≈ ⟦ Γ ˢ⟧
    ⟦subst⟧-Γˢ⊆Γ ∙ = refl
    ⟦subst⟧-Γˢ⊆Γ (Γ ,, A now) {n} {⟦Γ⟧ , ⟦A⟧}
        rewrite ⟦⁺⟧ (A now) (Γˢ⊆Γ Γ ⊆ₛ k) {n} {⟦Γ⟧ , ⟦A⟧} = ⟦subst⟧-Γˢ⊆Γ Γ
    ⟦subst⟧-Γˢ⊆Γ (Γ ,, A always) {n} {⟦Γ⟧ , ⟦A⟧}
        rewrite ⟦↑⟧ (A always) (Γˢ⊆Γ Γ ⊆ₛ k) {n} {⟦Γ⟧ , ⟦A⟧}
              | ⟦subst⟧-Γˢ⊆Γ Γ {n} {⟦Γ⟧} = refl

    -- Interpretation of substitution and selection can be commuted
    ⟦subst⟧-handle : ∀{Δ Γ A B C} -> (σ : Subst 𝒮 Γ Δ)
        -> {⟦C₁⟧ : ⟦ Γ ˢ ⟧ₓ ⊗   ⟦ A ⟧ₜ ⊗ ◇ ⟦ B ⟧ₜ ⇴ ◇ ⟦ C ⟧ₜ}
        -> {⟦C₂⟧ : ⟦ Γ ˢ ⟧ₓ ⊗ ◇ ⟦ A ⟧ₜ ⊗   ⟦ B ⟧ₜ ⇴ ◇ ⟦ C ⟧ₜ}
        -> {⟦C₃⟧ : ⟦ Γ ˢ ⟧ₓ ⊗   ⟦ A ⟧ₜ ⊗   ⟦ B ⟧ₜ ⇴ ◇ ⟦ C ⟧ₜ}
        -> (handle
            (⟦C₁⟧ ∘ (⟦subst⟧ (_↑_ {Event B now} (_↑_ {A now} (σ ↓ˢ k) k) k)))
            (⟦C₂⟧ ∘ (⟦subst⟧ (_↑_ {B now} (_↑_ {Event A now} (σ ↓ˢ k) k) k)))
            (⟦C₃⟧ ∘ (⟦subst⟧ (_↑_ {B now} (_↑_ {A now}       (σ ↓ˢ k) k) k))))
         ≈ handle ⟦C₁⟧ ⟦C₂⟧ ⟦C₃⟧ ∘ (⟦subst⟧ (σ ↓ˢ k) * id)
    ⟦subst⟧-handle {A = A} {B} σ {n = n} {⟦Δ⟧ , inj₁ (inj₁ (⟦A⟧ , ⟦◇B⟧))}
        rewrite ⟦↑⟧ (Event B now) (_↑_ {A now} (σ ↓ˢ k) k) {n} {(⟦Δ⟧ , ⟦A⟧) , ⟦◇B⟧}
              | ⟦↑⟧ (A now) (σ ↓ˢ k) {n} {⟦Δ⟧ , ⟦A⟧} = refl
    ⟦subst⟧-handle {A = A} {B} σ {n = n} {⟦Δ⟧ , inj₁ (inj₂ (⟦B⟧ , ⟦◇A⟧))}
        rewrite ⟦↑⟧ (B now) (_↑_ {Event A now} (σ ↓ˢ k) k) {n} {(⟦Δ⟧ , ⟦B⟧) , ⟦◇A⟧}
              | ⟦↑⟧ (Event A now) (σ ↓ˢ k) {n} {⟦Δ⟧ , ⟦B⟧} = refl
    ⟦subst⟧-handle {A = A} {B} σ {n = n} {⟦Δ⟧ , inj₂ (⟦A⟧ , ⟦B⟧)}
        rewrite ⟦↑⟧ (B now) (_↑_ {A now} (σ ↓ˢ k) k) {n} {(⟦Δ⟧ , ⟦A⟧) , ⟦B⟧}
              | ⟦↑⟧ (A now) (σ ↓ˢ k) {n} {⟦Δ⟧ , ⟦A⟧} = refl

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
------------------------------------------------------------------------
-- Some alternative definitions of the concept of being an equivalence
------------------------------------------------------------------------

-- Partly based on the blog post "Universal properties without
-- function extensionality" by Mike Shulman
-- (https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/),
-- and the corresponding code in the Coq HoTT library
-- (https://github.com/HoTT/HoTT).

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

open import Equality

module Equivalence.Path-split
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

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

open import Bijection eq as B using (_↔_)
open import Embedding eq using (Embedding)
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
open import Equivalence.Erased.Basics eq using (Is-equivalenceᴱ)
open import Function-universe eq as F hiding (id; _∘_)
open import H-level eq as H-level
open import H-level.Closure eq
open import Surjection eq using (Split-surjective; _↠_)

private
  variable
    a b c d p : Level
    A B       : Type a
    x y       : A
    f         : A → B
    k         : Kind
    n         : ℕ

------------------------------------------------------------------------
-- Path-split

-- An alternative definition of "Is-equivalence".

Path-split : {A : Type a} {B : Type b} → ℕ → (A → B) → Type (a ⊔ b)
Path-split zero    f = ↑ _ ⊤
Path-split (suc n) f =
  Split-surjective f ×
  (∀ x y → Path-split n (cong {x = x} {y = y} f))

private

  -- A lemma.

  eq→emb : Is-equivalence f → Is-equivalence (cong {x = x} {y = y} f)
  eq→emb eq =
    Embedding.is-embedding (from-isomorphism Eq.⟨ _ , eq ⟩) _ _

-- Equivalences are path-split.

Is-equivalence→Path-split : Is-equivalence f → Path-split n f
Is-equivalence→Path-split {n = zero}  eq = _
Is-equivalence→Path-split {n = suc n} eq =
    _≃_.split-surjective Eq.⟨ _ , eq ⟩
  , λ x y → Is-equivalence→Path-split (eq→emb eq)

private

  -- Path-split n f holds, for n ≥ 2, iff f is an equivalence.

  Path-split⇔Is-equivalence :
    Path-split (2 + n) f ⇔ Is-equivalence f
  Path-split⇔Is-equivalence {f = f} = record
    { to   = λ (s , p) →
               let inv    = proj₁ ∘ s
                   is-inv = proj₂ ∘ s
               in _≃_.is-equivalence $ Eq.↔⇒≃ (record
                    { surjection = record
                      { right-inverse-of = is-inv
                      }
                    ; left-inverse-of = λ x →  $⟨ is-inv (f x) ⟩
                        f (inv (f x)) ≡ f x    ↝⟨ proj₁ ∘ proj₁ (p _ _) ⟩
                        inv (f x) ≡ x          □
                    })
    ; from = Is-equivalence→Path-split
    }

-- If f is an equivalence, then Split-surjective f is contractible
-- (assuming extensionality).

Split-surjective-contractible-for-equivalences :
  ∀ {a b} {A : Type a} {B : Type b} {f : A → B} →
  Extensionality b (a ⊔ b) →
  Is-equivalence f →
  Contractible (Split-surjective f)
Split-surjective-contractible-for-equivalences
  {A = A} {B = B} {f = f} ext eq =

  propositional⇒inhabited⇒contractible
    (Π-closure ext 1 λ y →
     let surj : (∃ λ x → x ≡ _≃_.from A≃B y) ↠ (∃ λ x → f x ≡ y)
         surj = ∃-cong λ x →
           x ≡ _≃_.from A≃B y        ↔⟨ inverse $ Eq.≃-≡ A≃B ⟩
           f x ≡ f (_≃_.from A≃B y)  ↝⟨ ≡⇒↝ _ $ cong (_ ≡_) $ _≃_.right-inverse-of A≃B _ ⟩□
           f x ≡ y                   □
     in
     H-level.respects-surjection surj 1 $
     mono₁ 0 $
     singleton-contractible _)
    (_≃_.split-surjective A≃B)
  where
  A≃B : A ≃ B
  A≃B = Eq.⟨ _ , eq ⟩

-- If f is an equivalence, then Path-split n f is contractible
-- (assuming extensionality).

Path-split-contractible-for-equivalences :
  {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-equivalence f →
  Contractible (Path-split n f)
Path-split-contractible-for-equivalences {n = zero} _ _ =
  ↑-closure 0 $
  ⊤-contractible

Path-split-contractible-for-equivalences
  {a = a} {b = b} {n = suc n} {A = A} {B = B} {f = f} ext eq =

  ×-closure 0
    (Split-surjective-contractible-for-equivalences
       (lower-extensionality a lzero ext) eq)
    (Π-closure (lower-extensionality b lzero ext) 0 λ _ →
     Π-closure (lower-extensionality b lzero ext) 0 λ _ →
     Path-split-contractible-for-equivalences
        ext (eq→emb eq))

-- Path-split n is pointwise propositional for n ≥ 2 (assuming
-- extensionality).

Path-split-propositional :
  {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-proposition (Path-split (2 + n) f)
Path-split-propositional ext =
  [inhabited⇒contractible]⇒propositional λ p →
  Path-split-contractible-for-equivalences ext $
    _⇔_.to Path-split⇔Is-equivalence p

-- There is a bijection between Path-split n f, for n ≥ 2, and
-- Is-equivalence f (assuming extensionality).

Path-split↔Is-equivalence :
  {A : Type a} {B : Type b} {f : A → B} →
  Path-split (2 + n) f ↝[ a ⊔ b ∣ a ⊔ b ] Is-equivalence f
Path-split↔Is-equivalence =
  generalise-ext?-prop
    Path-split⇔Is-equivalence
    Path-split-propositional
    (λ ext → Eq.propositional ext _)

-- Another alternative definition of "Is-equivalence".

Path-split-∞ : {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Path-split-∞ f = ∀ n → Path-split n f

-- Path-split-∞ is pointwise propositional (assuming extensionality).

Path-split-∞-propositional :
  {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-proposition (Path-split-∞ f)
Path-split-∞-propositional ext =
  [inhabited⇒contractible]⇒propositional λ p →
  Π-closure (lower-extensionality _ lzero ext) 0 λ _ →
  Path-split-contractible-for-equivalences ext $
    _⇔_.to Path-split⇔Is-equivalence (p 2)

-- There is a bijection between Path-split-∞ f and Is-equivalence f
-- (assuming extensionality).

Path-split-∞↔Is-equivalence :
  {A : Type a} {B : Type b} {f : A → B} →
  Path-split-∞ f ↝[ a ⊔ b ∣ a ⊔ b ] Is-equivalence f
Path-split-∞↔Is-equivalence =
  generalise-ext?-prop
    (record
       { to   = λ p → _⇔_.to Path-split⇔Is-equivalence (p 2)
       ; from = λ eq _ → Is-equivalence→Path-split eq
       })
    Path-split-∞-propositional
    (λ ext → Eq.propositional ext _)

-- A preservation lemma for Path-split.

Path-split-cong :
  {A : Type a} {B : Type b} {C : Type c} {D : Type d}
  {f : A → B} {g : C → D} →
  Extensionality? k (a ⊔ b ⊔ c ⊔ d) (a ⊔ b ⊔ c ⊔ d) →
  (A≃C : A ≃ C) (B≃D : B ≃ D) →
  (∀ x → g (_≃_.to A≃C x) ≡ _≃_.to B≃D (f x)) →
  ∀ n → Path-split n f ↝[ k ] Path-split n g
Path-split-cong
  {a = a} {b = b} {c = c} {d = d} {k = k} {f = f} {g = g}
  ext A≃C B≃D hyp = λ where

  zero →
    ↑ _ ⊤  ↔⟨ B.↑↔ ⟩
    ⊤      ↔⟨ inverse B.↑↔ ⟩□
    ↑ _ ⊤  □

  (suc n) →

    (Split-surjective f                   ↔⟨⟩

     (∀ y → ∃ λ x → f x ≡ y)              ↝⟨ (Π-cong (lower-extensionality? k (a ⊔ c) lzero ext) B≃D λ y →
                                              Σ-cong A≃C λ x →

       (f x ≡ y)                                ↔⟨ inverse $ Eq.≃-≡ B≃D ⟩
       (_≃_.to B≃D (f x) ≡ _≃_.to B≃D y)        ↝⟨ ≡⇒↝ _ $ cong (_≡ _) $ sym $ hyp x ⟩□
       (g (_≃_.to A≃C x) ≡ _≃_.to B≃D y)        □) ⟩

     (∀ y → ∃ λ x → g x ≡ y)              ↔⟨⟩

     Split-surjective g                   □)

      ×-cong

    (Π-cong (lower-extensionality? k (b ⊔ d) lzero ext) A≃C λ x →
     Π-cong (lower-extensionality? k (b ⊔ d) lzero ext) A≃C λ y →
     Path-split-cong ext

       (x ≡ y                        ↝⟨ inverse $ Eq.≃-≡ A≃C ⟩□
        _≃_.to A≃C x ≡ _≃_.to A≃C y  □)

       (f x ≡ f y                            ↝⟨ inverse $ Eq.≃-≡ B≃D ⟩
        _≃_.to B≃D (f x) ≡ _≃_.to B≃D (f y)  ↝⟨ ≡⇒↝ _ $ cong₂ _≡_ (sym $ hyp x) (sym $ hyp y) ⟩□
        g (_≃_.to A≃C x) ≡ g (_≃_.to A≃C y)  □)

       (λ x≡y →
          cong g (cong (_≃_.to A≃C) x≡y)                            ≡⟨ cong-∘ _ _ _ ⟩

          cong (g ∘ _≃_.to A≃C) x≡y                                 ≡⟨ elim¹
                                                                         (λ {y} x≡y →
                                                                            cong (g ∘ _≃_.to A≃C) x≡y ≡
                                                                            trans (trans (hyp x) (cong (_≃_.to B≃D ∘ f) x≡y))
                                                                              (sym $ hyp y))
                                                                         (
            cong (g ∘ _≃_.to A≃C) (refl _)                                ≡⟨ cong-refl _ ⟩

            refl _                                                        ≡⟨ sym $ trans-symʳ _ ⟩

            trans (hyp x) (sym $ hyp x)                                   ≡⟨ cong (flip trans _) $
                                                                             trans (sym $ trans-reflʳ _) $
                                                                             cong (trans _) $ sym $ cong-refl _ ⟩∎
            trans (trans (hyp x) (cong (_≃_.to B≃D ∘ f) (refl _)))
              (sym $ hyp x)                                               ∎)
                                                                         _ ⟩
          trans (trans (hyp x) (cong (_≃_.to B≃D ∘ f) x≡y))
            (sym $ hyp y)                                           ≡⟨ trans (cong (flip trans _) $ sym $
                                                                              subst-trans _) $
                                                                       trans-subst ⟩
          subst (_ ≡_) (sym $ hyp y)
            (subst (_≡ _) (sym $ hyp x)
               (cong (_≃_.to B≃D ∘ f) x≡y))                         ≡⟨ trans (cong (subst _ _) $
                                                                              subst-in-terms-of-≡⇒↝ equivalence _ _ _) $
                                                                       subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
          _≃_.to (≡⇒↝ _ (cong (_ ≡_) (sym $ hyp y)))
            (_≃_.to (≡⇒↝ _ (cong (_≡ _) (sym $ hyp x)))
               (cong (_≃_.to B≃D ∘ f) x≡y))                         ≡⟨ cong (_$ cong (_≃_.to B≃D ∘ f) x≡y) $ sym $
                                                                       ≡⇒↝-trans equivalence ⟩
          _≃_.to
            (≡⇒↝ _ $
             trans (cong (_≡ _) (sym $ hyp x))
               (cong (_ ≡_) (sym $ hyp y)))
            (cong (_≃_.to B≃D ∘ f) x≡y)                             ≡⟨⟩

          _≃_.to (≡⇒↝ _ $ cong₂ _≡_ (sym $ hyp x) (sym $ hyp y))
            (cong (_≃_.to B≃D ∘ f) x≡y)                             ≡⟨ cong (_≃_.to (≡⇒↝ _ _)) $ sym $
                                                                       cong-∘ _ _ _ ⟩∎
          _≃_.to (≡⇒↝ _ $ cong₂ _≡_ (sym $ hyp x) (sym $ hyp y))
            (cong (_≃_.to B≃D) (cong f x≡y))                        ∎)

       n)

------------------------------------------------------------------------
-- Extendable along

-- Is-[ n ]-extendable-along-[ f ] P means that P is n-extendable
-- along f.

Is-[_]-extendable-along-[_] :
  {A : Type a} {B : Type b} →
  ℕ → (A → B) → (B → Type c) → Type (a ⊔ b ⊔ c)
Is-[ zero  ]-extendable-along-[ f ] P = ↑ _ ⊤
Is-[ suc n ]-extendable-along-[ f ] P =
  ((g : ∀ x → P (f x)) →
     ∃ λ (h : ∀ x → P x) → ∀ x → h (f x) ≡ g x) ×
  ((g h : ∀ x → P x) →
     Is-[ n ]-extendable-along-[ f ] (λ x → g x ≡ h x))

-- Is-∞-extendable-along-[ f ] P means that P is ∞-extendable along f.

Is-∞-extendable-along-[_] :
  {A : Type a} {B : Type b} →
  (A → B) → (B → Type c) → Type (a ⊔ b ⊔ c)
Is-∞-extendable-along-[ f ] P =
  ∀ n → Is-[ n ]-extendable-along-[ f ] P

-- In the presence of extensionality Is-[_]-extendable-along-[_] can
-- be expressed using Path-split.

Is-extendable-along≃Path-split :
  {A : Type a} {B : Type b} {P : B → Type p} {f : A → B} →
  Extensionality (a ⊔ b ⊔ p) (a ⊔ b ⊔ p) →
  ∀ n →
  Is-[ n ]-extendable-along-[ f ] P ≃
  Path-split n (λ (g : ∀ x → P x) → g ∘ f)
Is-extendable-along≃Path-split {a = a} {b = b} {p = p} {f = f} ext =
  λ where
    zero    → Eq.id
    (suc n) →
      (∀-cong (lower-extensionality b lzero ext) λ g →
       ∃-cong λ h →
         (∀ x → h (f x) ≡ g x)  ↝⟨ Eq.extensionality-isomorphism
                                     (lower-extensionality (b ⊔ p) (a ⊔ b) ext) ⟩□
         h ∘ f ≡ g              □)
        ×-cong
      (∀-cong (lower-extensionality a lzero ext) λ g →
       ∀-cong (lower-extensionality a lzero ext) λ h →
         Is-[ n ]-extendable-along-[ f ] (λ x → g x ≡ h x)  ↝⟨ Is-extendable-along≃Path-split ext n ⟩
         Path-split n (_∘ f)                                ↝⟨ Path-split-cong ext
                                                                 (Eq.extensionality-isomorphism ext₁)
                                                                 (Eq.extensionality-isomorphism ext₂)
                                                                 (λ eq →
          cong (_∘ f) (apply-ext (Eq.good-ext ext₁) eq)             ≡⟨ Eq.cong-pre-∘-good-ext ext₂ ext₁ _ ⟩∎
          apply-ext (Eq.good-ext ext₂) (eq ∘ f)                     ∎)
                                                                 n ⟩□
         Path-split n (cong (_∘ f))                         □)
  where
  ext₁ = lower-extensionality (a ⊔ p) (a ⊔ b) ext
  ext₂ = lower-extensionality (b ⊔ p) (a ⊔ b) ext

-- In the presence of extensionality Is-∞-extendable-along-[_] can
-- be expressed using Path-split-∞.

Is-∞-extendable-along≃Path-split-∞ :
  {A : Type a} {B : Type b} {P : B → Type p} {f : A → B} →
  Extensionality (a ⊔ b ⊔ p) (a ⊔ b ⊔ p) →
  Is-∞-extendable-along-[ f ] P ≃
  Path-split-∞ (λ (g : ∀ x → P x) → g ∘ f)
Is-∞-extendable-along≃Path-split-∞ ext =
  ∀-cong (lower-extensionality _ lzero ext) $
  Is-extendable-along≃Path-split ext

-- Is-[ 2 + n ]-extendable-along-[ f ] P is propositional (assuming
-- extensionality).

Is-extendable-along-propositional :
  {A : Type a} {B : Type b} {P : B → Type p} {f : A → B} →
  Extensionality (a ⊔ b ⊔ p) (a ⊔ b ⊔ p) →
  Is-proposition (Is-[ 2 + n ]-extendable-along-[ f ] P)
Is-extendable-along-propositional ext =
  H-level-cong _ 1 (inverse $ Is-extendable-along≃Path-split ext _) $
  Path-split-propositional ext

-- Is-∞-extendable-along-[ f ] P is propositional (assuming
-- extensionality).

Is-∞-extendable-along-propositional :
  {A : Type a} {B : Type b} {P : B → Type p} {f : A → B} →
  Extensionality (a ⊔ b ⊔ p) (a ⊔ b ⊔ p) →
  Is-proposition (Is-∞-extendable-along-[ f ] P)
Is-∞-extendable-along-propositional ext =
  H-level-cong _ 1 (inverse $ Is-∞-extendable-along≃Path-split-∞ ext) $
  Path-split-∞-propositional ext

-- In the presence of extensionality Is-∞-extendable-along-[_] can be
-- expressed using Is-equivalence.

Is-∞-extendable-along≃Is-equivalence :
  {A : Type a} {B : Type b} {P : B → Type p} {f : A → B} →
  Extensionality (a ⊔ b ⊔ p) (a ⊔ b ⊔ p) →
  Is-∞-extendable-along-[ f ] P ≃
  Is-equivalence (λ (g : ∀ x → P x) → g ∘ f)
Is-∞-extendable-along≃Is-equivalence {P = P} {f = f} ext =
  Is-∞-extendable-along-[ f ] P  ↝⟨ Is-∞-extendable-along≃Path-split-∞ ext ⟩
  Path-split-∞ (_∘ f)            ↝⟨ Path-split-∞↔Is-equivalence ext ⟩□
  Is-equivalence (_∘ f)          □

-- The definitions below are not taken directly from "Universal
-- properties without function extensionality".

-- A type B is P-null for a predicate P of type A → Type p if the
-- function const of type B → P x → B is an equivalence for each x.
--
-- This definition is based on one from "Modalities in Homotopy Type
-- Theory" by Rijke, Shulman and Spitters.

_-Null_ : {A : Type a} → (A → Type p) → Type b → Type (a ⊔ b ⊔ p)
P -Null B = ∀ x → Is-equivalence (const ⦂ (B → P x → B))

-- A variant of _-Null_ with erased proofs.

_-Nullᴱ_ : {A : Type a} → (A → Type p) → Type b → Type (a ⊔ b ⊔ p)
P -Nullᴱ B = ∀ x → Is-equivalenceᴱ (const ⦂ (B → P x → B))

-- Is-∞-extendable-along-[_] can sometimes be replaced by
-- Is-equivalence const.

Is-∞-extendable-along≃Is-equivalence-const :
  {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  Is-∞-extendable-along-[ (λ (_ : A) → lift tt) ] (λ (_ : ↑ a ⊤) → B) ≃
  Is-equivalence (const ⦂ (B → A → B))
Is-∞-extendable-along≃Is-equivalence-const {a = a} {A = A} {B = B} ext =
  Is-∞-extendable-along-[ (λ _ → lift tt) ] (λ (_ : ↑ a ⊤) → B)  ↝⟨ Is-∞-extendable-along≃Is-equivalence ext ⟩

  Is-equivalence (_∘ (λ _ → lift tt) ⦂ ((↑ a ⊤ → B) → (A → B)))  ↝⟨ inverse $
                                                                    Is-equivalence≃Is-equivalence-∘ʳ
                                                                      (_≃_.is-equivalence $ Eq.↔→≃ (_$ lift tt) const refl refl) ext ⟩□
  Is-equivalence (const ⦂ (B → A → B))                           □

-- A corollary of Is-∞-extendable-along≃Is-equivalence-const.

Π-Is-∞-extendable-along≃Null :
  {A : Type a} {P : A → Type p} {B : Type b} →
  Extensionality (a ⊔ b ⊔ p) (b ⊔ p) →
  (∀ x → Is-∞-extendable-along-[ (λ (_ : P x) → lift tt) ]
           (λ (_ : ↑ p ⊤) → B)) ≃
  P -Null B
Π-Is-∞-extendable-along≃Null {a = a} {p = p} {b = b} ext =
  ∀-cong (lower-extensionality (b ⊔ p) lzero ext) λ _ →
  Is-∞-extendable-along≃Is-equivalence-const
    (lower-extensionality a lzero ext)

private

  -- If const is an equivalence from Bool to B → Bool, then B is not
  -- not inhabited (assuming extensionality).

  Is-equivalence-const→¬¬ :
    {B : Type b} →
    Extensionality b lzero →
    Is-equivalence (const ⦂ (Bool → B → Bool)) →
    ¬ ¬ B
  Is-equivalence-const→¬¬ {B = B} ext =
    curry
      (Is-equivalence (const ⦂ (Bool → B → Bool)) × ¬ B  →⟨ Σ-map Eq.⟨ _ ,_⟩ (Eq.↔⇒≃ ∘ inverse ∘ B.⊥↔uninhabited) ⟩
       Bool ≃ (B → Bool) × B ≃ ⊥                         →⟨ (λ (≃B→ , B≃) → →-cong ext B≃ F.id F.∘ ≃B→) ⟩
       Bool ≃ (⊥ → Bool)                                 →⟨ Π⊥↔⊤ ext F.∘_ ⟩
       Bool ≃ ⊤                                          →⟨ (λ eq → _≃_.to (Eq.≃-≡ eq) (refl _)) ⟩
       true ≡ false                                      →⟨ Bool.true≢false ⟩□
       ⊥                                                 □)

  -- If const is an equivalence from Bool to B → Bool, and equality is
  -- decidable for B, then B is a proposition.

  Is-equivalence-const→Decidable-equality→Is-proposition :
    Is-equivalence (const ⦂ (Bool → B → Bool)) →
    Decidable-equality B →
    Is-proposition B
  Is-equivalence-const→Decidable-equality→Is-proposition
    {B = B} eq _≟_ x y = x≡y
    where
    lemma :
      (f g : B → Bool) → f ≢ g →
      (h : B → Bool) → f ≡ h ⊎ g ≡ h
    lemma =                                                        $⟨ helper ⟩
      ((x y : Bool) → x ≢ y → (z : Bool) → x ≡ z ⊎ y ≡ z)          →⟨ (Π-cong _ equiv λ x → Π-cong _ equiv λ y →
                                                                       →-cong-→ (→-cong-→ (_≃_.from (Eq.≃-≡ equiv)) id) $
                                                                       Π-cong _ equiv λ z →
                                                                       _≃_.from (Eq.≃-≡ equiv ⊎-cong Eq.≃-≡ equiv)) ⟩□
      ((f g : B → Bool) → f ≢ g → (h : B → Bool) → f ≡ h ⊎ g ≡ h)  □
      where
      equiv : Bool ≃ (B → Bool)
      equiv = Eq.⟨ _ , eq ⟩

      true≡⊎false≡ : (b : Bool) → true ≡ b ⊎ false ≡ b
      true≡⊎false≡ true  = inj₁ (refl _)
      true≡⊎false≡ false = inj₂ (refl _)

      helper : (x y : Bool) → x ≢ y → (z : Bool) → x ≡ z ⊎ y ≡ z
      helper true  true  t≢t = ⊥-elim $ t≢t (refl _)
      helper true  false _   = true≡⊎false≡
      helper false true  _   = _↔_.to ⊎-comm ∘ true≡⊎false≡
      helper false false f≢f = ⊥-elim $ f≢f (refl _)

    f₁ f₂ f₃ : B → Bool
    f₁ _ = true
    f₂ _ = false
    f₃ z = if x ≟ z then true else false

    f₁≢f₂ : f₁ ≢ f₂
    f₁≢f₂ f₁≡f₂ = Bool.true≢false $ cong (_$ x) f₁≡f₂

    f₁≡f₃→x≡y : f₁ ≡ f₃ → x ≡ y
    f₁≡f₃→x≡y f₁≡f₃ = helper (x ≟ y) (cong (_$ y) f₁≡f₃)
      where
      helper :
        (d : Dec (x ≡ y)) →
        true ≡ if d then true else false →
        x ≡ y
      helper (yes x≡y) _          = x≡y
      helper (no  _)   true≡false =
        ⊥-elim $ Bool.true≢false true≡false

    f₂≢f₃ : f₂ ≢ f₃
    f₂≢f₃ =
      f₂ ≡ f₃                                →⟨ cong (_$ x) ⟩
      false ≡ if x ≟ x then true else false  →⟨ flip trans (helper (x ≟ x)) ⟩
      false ≡ true                           →⟨ Bool.true≢false ∘ sym ⟩□
      ⊥                                      □
      where
      helper :
        (d : Dec (x ≡ x)) →
        if d then true else false ≡ true
      helper (yes _)  = refl _
      helper (no x≢x) = ⊥-elim $ x≢x $ refl _

    f₁≡⊎f₂≡ : (f : B → Bool) → f₁ ≡ f ⊎ f₂ ≡ f
    f₁≡⊎f₂≡ = lemma f₁ f₂ f₁≢f₂

    x≡y : x ≡ y
    x≡y with f₁≡⊎f₂≡ f₃
    … | inj₁ f₁≡f₃ = f₁≡f₃→x≡y f₁≡f₃
    … | inj₂ f₂≡f₃ = ⊥-elim $ f₂≢f₃ f₂≡f₃

-- If f is an equivalence, then n-extendability along f is
-- contractible (assuming extensionality).

Is-extendable-along-contractible-for-equivalences :
  {A : Type a} {B : Type b} {f : A → B} {P : B → Type p} →
  Extensionality (a ⊔ b ⊔ p) (a ⊔ b ⊔ p) →
  Is-equivalence f →
  ∀ n → Contractible (Is-[ n ]-extendable-along-[ f ] P)
Is-extendable-along-contractible-for-equivalences _ _ zero =
  ↑-closure 0 ⊤-contractible

Is-extendable-along-contractible-for-equivalences
  {a = a} {b = b} {p = p} {f = f} {P = P} ext eq (suc n) =

  ×-closure 0
    (Π-closure (lower-extensionality b lzero ext) 0 λ g →
                                                             $⟨ singleton-contractible _ ⟩
       Contractible (∃ λ h → h ≡ subst P (inv _) ∘ g ∘ f⁻¹)  ↝⟨ H-level-cong _ 0 (lemma g) ⦂ (_ → _) ⟩□
       Contractible (∃ λ h → ∀ x → h (f x) ≡ g x)            □)
    (Π-closure (lower-extensionality a lzero ext) 0 λ _ →
     Π-closure (lower-extensionality a lzero ext) 0 λ _ →
     Is-extendable-along-contractible-for-equivalences ext eq n)
  where
  f⁻¹ = _≃_.from Eq.⟨ _ , eq ⟩
  inv = _≃_.left-inverse-of (inverse Eq.⟨ _ , eq ⟩)

  lemma : ∀ _ → _ ≃ _
  lemma g =
    (∃ λ h → h ≡ subst P (inv _) ∘ g ∘ f⁻¹)  ↔⟨ (∃-cong λ h → inverse $
                                                 ∘from≡↔≡∘to′ (lower-extensionality p (a ⊔ b) ext) (inverse Eq.⟨ _ , eq ⟩)) ⟩
    (∃ λ h → h ∘ f ≡ g)                      ↝⟨ (∃-cong λ _ → inverse $
                                                 Eq.extensionality-isomorphism (lower-extensionality (b ⊔ p) (a ⊔ b) ext)) ⟩□
    (∃ λ h → ∀ x → h (f x) ≡ g x)            □

-- If f is an equivalence, then ∞-extendability along f is
-- contractible (assuming extensionality).

Is-∞-extendable-along-contractible-for-equivalences :
  {A : Type a} {B : Type b} {f : A → B} {P : B → Type p} →
  Extensionality (a ⊔ b ⊔ p) (a ⊔ b ⊔ p) →
  Is-equivalence f →
  Contractible (Is-∞-extendable-along-[ f ] P)
Is-∞-extendable-along-contractible-for-equivalences ext eq =
  Π-closure (lower-extensionality _ lzero ext) 0 λ n →
  Is-extendable-along-contractible-for-equivalences ext eq n

------------------------------------------------------------------------
-- Alternatives to Is-[_]-extendable-along-[_] and
-- Is-∞-extendable-along-[_]

-- A variant of Is-[_]-extendable-along-[_].

Is-[_]-extendable-along-const-tt-[_] :
  ℕ → Type a → Type b → Type (a ⊔ b)
Is-[ zero  ]-extendable-along-const-tt-[ A ] B = ↑ _ ⊤
Is-[ suc n ]-extendable-along-const-tt-[ A ] B =
  ((g : A → B) → ∃ λ (x : B) → ∀ y → x ≡ g y) ×
  ((x y : B) → Is-[ n ]-extendable-along-const-tt-[ A ] (x ≡ y))

-- A variant of Is-∞-extendable-along-[_].

Is-∞-extendable-along-const-tt-[_] :
  Type a → Type b → Type (a ⊔ b)
Is-∞-extendable-along-const-tt-[ A ] B =
  ∀ n → Is-[ n ]-extendable-along-const-tt-[ A ] B

-- In some cases Is-[_]-extendable-along-[_] and
-- Is-∞-extendable-along-[_] can be replaced by the variants.

≃Is-extendable-along-const-tt :
  {A : Type a} {B : Type b} →
  Extensionality? k (a ⊔ b) (a ⊔ b) →
  ∀ n →
  Is-[ n ]-extendable-along-[ (λ (_ : A) → lift tt) ]
    (λ (_ : ↑ a ⊤) → B) ↝[ k ]
  Is-[ n ]-extendable-along-const-tt-[ A ] B
≃Is-extendable-along-const-tt                 _   zero    = F.id
≃Is-extendable-along-const-tt {a = a} {k = k} ext (suc n) =
  (∀-cong ext λ _ →
   Σ-cong (Eq.↔→≃ (_$ lift tt) const refl refl) λ _ →
   F.id)
    ×-cong
  Π-cong ext′ (Eq.↔→≃ (_$ lift tt) const refl refl) λ _ →
  Π-cong ext′ (Eq.↔→≃ (_$ lift tt) const refl refl) λ _ →
  ≃Is-extendable-along-const-tt ext n
  where
  ext′ = lower-extensionality? k a lzero ext

≃Is-∞-extendable-along-const-tt :
  {A : Type a} {B : Type b} →
  Extensionality? k (a ⊔ b) (a ⊔ b) →
  Is-∞-extendable-along-[ (λ (_ : A) → lift tt) ] (λ (_ : ↑ a ⊤) → B)
    ↝[ k ]
  Is-∞-extendable-along-const-tt-[ A ] B
≃Is-∞-extendable-along-const-tt {k = k} ext =
  ∀-cong (lower-extensionality? k _ lzero ext) λ n →
  ≃Is-extendable-along-const-tt ext n

-- Preservation lemmas for Is-[_]-extendable-along-[_] and
-- Is-∞-extendable-along-[_].

Is-extendable-along-const-tt-cong :
  {A : Type a} {B : Type b} {C : Type c} →
  Extensionality? k (a ⊔ b ⊔ c) (a ⊔ b ⊔ c) →
  (A≃B : A ≃ B)
  (A→≃B→ : {C : Type c} → (A → C) ≃ (B → C)) →
  ({C : Type c} (f : A → C) (x : A) →
   _≃_.to A→≃B→ f (_≃_.to A≃B x) ≡ f x) →
  ∀ n →
  Is-[ n ]-extendable-along-const-tt-[ A ] C ↝[ k ]
  Is-[ n ]-extendable-along-const-tt-[ B ] C
Is-extendable-along-const-tt-cong _ _ _ _ zero =
  ↑ _ ⊤  ↔⟨ B.↑↔ ⟩
  ⊤      ↔⟨ inverse B.↑↔ ⟩□
  ↑ _ ⊤  □
Is-extendable-along-const-tt-cong
  {a = a} {b = b} {c = c} {k = k} ext A≃B A→≃B→ hyp (suc n) =

  (Π-cong ext A→≃B→ λ g →
   ∃-cong λ x →
   Π-cong (lower-extensionality? k c (a ⊔ b) ext) A≃B λ y →
     x ≡ g y                            ↝⟨ ≡⇒↝ _ $ cong (_ ≡_) $ sym $ hyp g y ⟩□
     x ≡ _≃_.to A→≃B→ g (_≃_.to A≃B y)  □)
    ×-cong
  (∀-cong (lower-extensionality? k (a ⊔ b) lzero ext) λ x →
   ∀-cong (lower-extensionality? k (a ⊔ b) lzero ext) λ y →
   Is-extendable-along-const-tt-cong ext A≃B A→≃B→ hyp n)

Is-∞-extendable-along-const-tt-cong :
  {A : Type a} {B : Type b} {C : Type c} →
  Extensionality? k (a ⊔ b ⊔ c) (a ⊔ b ⊔ c) →
  (A≃B : A ≃ B)
  (A→≃B→ : {C : Type c} → (A → C) ≃ (B → C)) →
  ({C : Type c} (f : A → C) (x : A) →
   _≃_.to A→≃B→ f (_≃_.to A≃B x) ≡ f x) →
  Is-∞-extendable-along-const-tt-[ A ] C ↝[ k ]
  Is-∞-extendable-along-const-tt-[ B ] C
Is-∞-extendable-along-const-tt-cong {k = k} ext A≃B A→≃B→ hyp =
  ∀-cong (lower-extensionality? k _ lzero ext) λ n →
  Is-extendable-along-const-tt-cong ext A≃B A→≃B→ hyp n

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Rational Literals
------------------------------------------------------------------------

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

module Data.Rational.Literals where

open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg
open import Data.Unit
open import Data.Nat
open import Data.Nat.Coprimality
open import Data.Integer
open import Data.Rational hiding (-_)

fromℤ : ℤ → ℚ
fromℤ z = record
  { numerator     = z
  ; denominator-1 = zero
  ; isCoprime     = sym (1-coprimeTo ∣ z ∣)
  }

number : Number ℚ
number = record
  { Constraint = λ _ → ⊤
  ; fromNat    = λ n → fromℤ (+ n)
  }

negative : Negative ℚ
negative = record
  { Constraint = λ _ → ⊤
  ; fromNeg    = λ n → fromℤ (- (+ n))
  }


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

open import Level hiding (lift)

open import Categories.Category
open import Categories.Functor

record F-Algebra {o ℓ e} {C : Category o ℓ e} (F : Endofunctor C) : Set (o ⊔ ℓ) where
  constructor _,_
  open Category C
  open Functor F
  field
    A : Obj
    α : F₀ A ⇒ A

lift : ∀ {o ℓ e} {C : Category o ℓ e} {F : Endofunctor C} → F-Algebra F → F-Algebra F
lift {F = F} (A , α) = record { A = F₀ A; α = F₁ α }
  where
  open Functor F

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import HoTT

{-
  Note: this module is for cohomology theories,
        so the commuting squares below do not
        care about the proof of pointedness,
        because any cohomology theory is independent
        of the possibly different proofs of pointedness.
-}

module homotopy.PtdMapSequence where

infix 15 _⊙⊣|
infixr 10 _⊙→⟨_⟩_

data PtdMapSequence {i} : (X : Ptd i) (Y : Ptd i) → Type (lsucc i) where
  _⊙⊣| : (X : Ptd i) → PtdMapSequence X X
  _⊙→⟨_⟩_ : (X : Ptd i) {Y Z : Ptd i}
    → (X ⊙→ Y) → PtdMapSequence Y Z
    → PtdMapSequence X Z

{- maps between two pointed map sequences -}

infix 15 _⊙↓|
infixr 10 _⊙↓⟨_⟩_

data PtdMapSeqMap {i₀ i₁} : {X₀ Y₀ : Ptd i₀} {X₁ Y₁ : Ptd i₁}
  (⊙seq₀ : PtdMapSequence X₀ Y₀) (⊙seq₁ : PtdMapSequence X₁ Y₁)
  (⊙hX : X₀ ⊙→ X₁) (⊙fY : Y₀ ⊙→ Y₁) → Type (lsucc (lmax i₀ i₁)) where
  _⊙↓| : {X₀ : Ptd i₀} {X₁ : Ptd i₁} (f : X₀ ⊙→ X₁) → PtdMapSeqMap (X₀ ⊙⊣|) (X₁ ⊙⊣|) f f
  _⊙↓⟨_⟩_ : ∀ {X₀ Y₀ Z₀ : Ptd i₀} {X₁ Y₁ Z₁ : Ptd i₁}
    → {⊙f₀ : X₀ ⊙→ Y₀} {⊙seq₀ : PtdMapSequence Y₀ Z₀}
    → {⊙f₁ : X₁ ⊙→ Y₁} {⊙seq₁ : PtdMapSequence Y₁ Z₁}
    → (⊙hX : X₀ ⊙→ X₁) {⊙hY : Y₀ ⊙→ Y₁} {⊙hZ : Z₀ ⊙→ Z₁}
    → CommSquare (fst ⊙f₀) (fst ⊙f₁) (fst ⊙hX) (fst ⊙hY)
    → PtdMapSeqMap ⊙seq₀ ⊙seq₁ ⊙hY ⊙hZ
    → PtdMapSeqMap (X₀ ⊙→⟨ ⊙f₀ ⟩ ⊙seq₀) (X₁ ⊙→⟨ ⊙f₁ ⟩ ⊙seq₁) ⊙hX ⊙hZ

{- equivalences between two pointed map sequences -}

is-⊙seq-equiv : ∀ {i₀ i₁} {X₀ Y₀ : Ptd i₀} {X₁ Y₁ : Ptd i₁}
  {⊙seq₀ : PtdMapSequence X₀ Y₀} {⊙seq₁ : PtdMapSequence X₁ Y₁}
  {⊙hX : X₀ ⊙→ X₁} {⊙hY : Y₀ ⊙→ Y₁}
  → PtdMapSeqMap ⊙seq₀ ⊙seq₁ ⊙hX ⊙hY
  → Type (lmax i₀ i₁)
is-⊙seq-equiv (⊙h ⊙↓|) = is-equiv (fst ⊙h)
is-⊙seq-equiv (⊙h ⊙↓⟨ _ ⟩ ⊙seq) = is-equiv (fst ⊙h) × is-⊙seq-equiv ⊙seq

PtdMapSeqEquiv : ∀ {i₀ i₁} {X₀ Y₀ : Ptd i₀} {X₁ Y₁ : Ptd i₁}
  (⊙seq₀ : PtdMapSequence X₀ Y₀) (⊙seq₁ : PtdMapSequence X₁ Y₁)
  (⊙hX : X₀ ⊙→ X₁) (⊙hY : Y₀ ⊙→ Y₁) → Type (lsucc (lmax i₀ i₁))
PtdMapSeqEquiv ⊙seq₀ ⊙seq₁ ⊙hX ⊙hY
  = Σ (PtdMapSeqMap ⊙seq₀ ⊙seq₁ ⊙hX ⊙hY) is-⊙seq-equiv

{- Doesn't seem useful.

infix 15 _⊙↕⊣|
infixr 10 _⊙↕⟨_⟩↕_

_⊙↕⊣| : ∀ {i} {X₀ X₁ : Ptd i} (⊙eq : X₀ ⊙≃ X₁)
  → PtdMapSequenceEquiv (X₀ ⊙⊣|) (X₁ ⊙⊣|) (⊙–> ⊙eq) (⊙–> ⊙eq)
⊙eq ⊙↕⊣| = (⊙–> ⊙eq ⊙↓⊣|) , snd ⊙eq

_⊙↕⟨_⟩↕_ : ∀ {i} {X₀ X₁ : Ptd i} → (⊙eqX : X₀ ⊙≃ X₁)
           → ∀ {Y₀ Y₁ : Ptd i} {⊙f : X₀ ⊙→ Y₀} {⊙g : X₁ ⊙→ Y₁} {⊙eqY : Y₀ ⊙≃ Y₁}
           → ⊙CommutingSquare ⊙f ⊙g (⊙–> ⊙eqX) (⊙–> ⊙eqY)
           → ∀ {Z₀ Z₁ : Ptd i} {⊙eqZ : Z₀ ⊙≃ Z₁} {⊙seq₀ : PtdMapSequence Y₀ Z₀} {⊙seq₁ : PtdMapSequence Y₁ Z₁}
           → PtdMapSequenceEquiv ⊙seq₀ ⊙seq₁ (⊙–> ⊙eqY) (⊙–> ⊙eqZ)
           → PtdMapSequenceEquiv (X₀ ⊙⟨ ⊙f ⟩→ ⊙seq₀) (X₁ ⊙⟨ ⊙g ⟩→ ⊙seq₁) (⊙–> ⊙eqX) (⊙–> ⊙eqZ)
(⊙hX , hX-is-equiv) ⊙↕⟨ sqr ⟩↕ (⊙seq-map , ⊙seq-map-is-equiv) =
  (⊙hX ⊙↓⟨ sqr ⟩↓ ⊙seq-map) , hX-is-equiv , ⊙seq-map-is-equiv
-}

private
  is-⊙seq-equiv-head : ∀ {i₀ i₁} {X₀ Y₀ : Ptd i₀} {X₁ Y₁ : Ptd i₁}
    {⊙seq₀ : PtdMapSequence X₀ Y₀} {⊙seq₁ : PtdMapSequence X₁ Y₁}
    {⊙hX : X₀ ⊙→ X₁} {⊙hY : Y₀ ⊙→ Y₁}
    {seq-map : PtdMapSeqMap ⊙seq₀ ⊙seq₁ ⊙hX ⊙hY}
    → is-⊙seq-equiv seq-map → is-equiv (fst ⊙hX)
  is-⊙seq-equiv-head {seq-map = ξ ⊙↓|} ise = ise
  is-⊙seq-equiv-head {seq-map = ξ ⊙↓⟨ _ ⟩ _} ise = fst ise

private
  ptd-map-seq-map-index-type : ∀ {i₀ i₁} {X₀ Y₀ : Ptd i₀} {X₁ Y₁ : Ptd i₁}
    {⊙seq₀ : PtdMapSequence X₀ Y₀} {⊙seq₁ : PtdMapSequence X₁ Y₁}
    {⊙hX : X₀ ⊙→ X₁} {⊙hY : Y₀ ⊙→ Y₁}
    → ℕ → PtdMapSeqMap ⊙seq₀ ⊙seq₁ ⊙hX ⊙hY → Type (lmax i₀ i₁)
  ptd-map-seq-map-index-type _     (_ ⊙↓|) = Lift ⊤
  ptd-map-seq-map-index-type O     (_⊙↓⟨_⟩_ {⊙f₀ = ⊙f₀} {⊙f₁ = ⊙f₁} ⊙hX {⊙hY} _ _)
    = CommSquare (fst ⊙f₀) (fst ⊙f₁) (fst ⊙hX) (fst ⊙hY)
  ptd-map-seq-map-index-type (S n) (_ ⊙↓⟨ _ ⟩ seq-map)
    = ptd-map-seq-map-index-type n seq-map

abstract
  ptd-map-seq-map-index : ∀ {i₀ i₁} {X₀ Y₀ : Ptd i₀} {X₁ Y₁ : Ptd i₁}
    {⊙seq₀ : PtdMapSequence X₀ Y₀} {⊙seq₁ : PtdMapSequence X₁ Y₁}
    {⊙hX : X₀ ⊙→ X₁} {⊙hY : Y₀ ⊙→ Y₁}
    (n : ℕ) (seq-map : PtdMapSeqMap ⊙seq₀ ⊙seq₁ ⊙hX ⊙hY)
    → ptd-map-seq-map-index-type n seq-map
  ptd-map-seq-map-index _     (_ ⊙↓|) = lift tt
  ptd-map-seq-map-index O     (_ ⊙↓⟨ □ ⟩ _) = □
  ptd-map-seq-map-index (S n) (_ ⊙↓⟨ _ ⟩ seq-map)
    = ptd-map-seq-map-index n seq-map

private
  ptd-map-seq-equiv-index-type : ∀ {i₀ i₁} {X₀ Y₀ : Ptd i₀} {X₁ Y₁ : Ptd i₁}
    {⊙seq₀ : PtdMapSequence X₀ Y₀} {⊙seq₁ : PtdMapSequence X₁ Y₁}
    {⊙hX : X₀ ⊙→ X₁} {⊙hY : Y₀ ⊙→ Y₁}
    → ℕ → PtdMapSeqMap ⊙seq₀ ⊙seq₁ ⊙hX ⊙hY → Type (lmax i₀ i₁)
  ptd-map-seq-equiv-index-type {⊙hX = ⊙hX} O _ = is-equiv (fst ⊙hX)
  ptd-map-seq-equiv-index-type (S _) (_ ⊙↓|) = Lift ⊤
  ptd-map-seq-equiv-index-type (S n) (_ ⊙↓⟨ _ ⟩ seq-map)
    = ptd-map-seq-equiv-index-type n seq-map

abstract
  ptd-map-seq-equiv-index : ∀ {i₀ i₁} {X₀ Y₀ : Ptd i₀} {X₁ Y₁ : Ptd i₁}
    {⊙seq₀ : PtdMapSequence X₀ Y₀} {⊙seq₁ : PtdMapSequence X₁ Y₁}
    {⊙hX : X₀ ⊙→ X₁} {⊙hY : Y₀ ⊙→ Y₁}
    (n : ℕ) (seq-equiv : PtdMapSeqEquiv ⊙seq₀ ⊙seq₁ ⊙hX ⊙hY)
    → ptd-map-seq-equiv-index-type n (fst seq-equiv)
  ptd-map-seq-equiv-index O     (seq-map , ise) = is-⊙seq-equiv-head ise
  ptd-map-seq-equiv-index (S _) ((_ ⊙↓|) , _) = lift tt
  ptd-map-seq-equiv-index (S n) ((_ ⊙↓⟨ _ ⟩ seq-map) , ise)
    = ptd-map-seq-equiv-index n (seq-map , snd ise)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Categories.Category using () renaming (Category to Setoid-Category)
open import Categories.Category.Monoidal

module Categories.Enriched.NaturalTransformation.NaturalIsomorphism
  {o ℓ e} {V : Setoid-Category o ℓ e} (M : Monoidal V) where

open import Level

open import Categories.Category.Construction.EnrichedFunctors M
open import Categories.Enriched.Category M
open import Categories.Enriched.Functor M renaming (id to idF)
open import Categories.Enriched.NaturalTransformation M renaming (id to idNT)
open import Categories.Functor.Properties using ([_]-resp-Iso)
open import Categories.Morphism as Morphism using (Iso)
open import Categories.Category.Monoidal.Reasoning M
open import Relation.Binary using (IsEquivalence)

open Setoid-Category V renaming (Obj to ObjV; id to idV)
module M = Monoidal M
open M hiding (unitorˡ; unitorʳ; associator)
open NaturalTransformation

module NaturalIsomorphism = Morphism._≅_
open NaturalIsomorphism

-- A natural isomorphism |α : F ≅ G : C → D| is an isomorphism of F
-- and G in the functor category [C , D] between C and D.

module _ {c d} {C : Category c} {D : Category d} where

  NaturalIsomorphism : (F G : Functor C D) → Set (ℓ ⊔ e ⊔ c)
  NaturalIsomorphism F G = F ≅ G
    where open Morphism (EnrichedFunctors C D) using (_≅_)

  -- A commonly used shorthand for NaturalIsomorphism

  infix 4 _≃_

  _≃_ = NaturalIsomorphism

  module _ {F G : Functor C D} where
    private
      module F = Functor F
      module G = Functor G
    open Morphism (Underlying D) using (_≅_)

    -- Natural isomorphisms are pointwise isomorphisms: each component
    -- |α [ X ]| is an isomorphism |F X ≅ G X|.

    infixl 16 _ᵢ[_]

    _ᵢ[_] : NaturalIsomorphism F G → ∀ X → F.₀ X ≅ G.₀ X
    α ᵢ[ X ] = record
      { from = from α [ X ]
      ; to   = to α   [ X ]
      ; iso  = record { isoˡ = isoˡ α ; isoʳ = isoʳ α }
      }

  ≃-isEquivalence : IsEquivalence _≃_
  ≃-isEquivalence = Morphism.≅-isEquivalence (EnrichedFunctors C D)

  module ≃ = IsEquivalence ≃-isEquivalence

  id : {F : Functor C D} → F ≃ F
  id = ≃.refl

  _⁻¹ : {F G : Functor C D} → F ≃ G → G ≃ F
  α ⁻¹ = ≃.sym α

  infixr 9 _ⓘᵥ_

  _ⓘᵥ_ : {F G H : Functor C D} → G ≃ H → F ≃ G → F ≃ H
  α ⓘᵥ β = ≃.trans β α

  private
    module D = Underlying D

  -- Left and right unitors

  unitorˡ : {F : Functor C D} → idF ∘F F ≃ F
  unitorˡ {F} = record
    { from = record
      { comp    = λ _ → D.id
      ; commute = (refl⟩∘⟨ refl⟩⊗⟨ identityˡ ⟩∘⟨refl) ○ comm
      }
    ; to = record
      { comp    = λ _ → D.id
      ; commute = comm ○ (refl⟩∘⟨ ⟺ identityˡ ⟩⊗⟨refl ⟩∘⟨refl)
      }
    ; iso = record { isoˡ = D.identity² ; isoʳ = D.identity² }
    }
    where comm = commute (idNT {F = F})

  unitorʳ : {F : Functor C D} → F ∘F idF ≃ F
  unitorʳ {F} = record
    { from = record
      { comp    = λ _ → D.id
      ; commute = (refl⟩∘⟨ refl⟩⊗⟨ identityʳ ⟩∘⟨refl) ○ comm
      }
    ; to = record
      { comp    = λ _ → D.id
      ; commute = comm ○ (refl⟩∘⟨ ⟺ identityʳ ⟩⊗⟨refl ⟩∘⟨refl)
      }
    ; iso = record { isoˡ = D.identity² ; isoʳ = D.identity² }
    }
    where comm = commute (idNT {F = F})

module _ {c d e} {C : Category c} {D : Category d} {E : Category e} where
  open NaturalIsomorphism

  -- Left- and right-hand composition with a functor

  infixr 9 _ⓘₕ_ _ⓘˡ_ _ⓘʳ_

  _ⓘˡ_ : {F G : Functor C D} (H : Functor D E) → F ≃ G → H ∘F F ≃ H ∘F G
  H ⓘˡ α = record
    { from = H ∘ˡ from α
    ; to   = H ∘ˡ to α
    ; iso  = record { isoˡ = iso.isoˡ ; isoʳ = iso.isoʳ }
    }
    where
      module iso {X} = Iso ([ UnderlyingFunctor H ]-resp-Iso (iso (α ᵢ[ X ])))

  _ⓘʳ_ : {G H : Functor D E} → G ≃ H → (F : Functor C D) → G ∘F F ≃ H ∘F F
  α ⓘʳ F = record
    { from = from α ∘ʳ F
    ; to   = to α   ∘ʳ F
    ; iso  = record { isoˡ = isoˡ (α ᵢ[ F.₀ _ ]) ; isoʳ = isoʳ (α ᵢ[ F.₀ _ ]) }
    }
    where module F = Functor F

  -- Horizontal composition

  _ⓘₕ_ : {H I : Functor D E} {F G : Functor C D} →
           H ≃ I → F ≃ G → (H ∘F F) ≃ (I ∘F G)
  _ⓘₕ_ {_} {I} {F} {_} α β = (I ⓘˡ β) ⓘᵥ (α ⓘʳ F)

module _ {b c d e} {B : Category b} {C : Category c}
                   {D : Category d} {E : Category e} where
  open NaturalIsomorphism
  private
    module E  = Category E
    module UE = Underlying E

  -- Associator

  associator : {F : Functor D E} {G : Functor C D} {H : Functor B C} →
               (F ∘F G) ∘F H ≃ F ∘F (G ∘F H)
  associator {F} {G} {H} = record
    { from = record
      { comp    = λ _ → E.id
      ; commute = (refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl) ○ comm
      }
    ; to = record
      { comp    = λ _ → E.id
      ; commute = comm ○ (refl⟩∘⟨ ⟺ assoc ⟩⊗⟨refl ⟩∘⟨refl)
      }
    ; iso = record { isoˡ = UE.identity² ; isoʳ = UE.identity² }
    }
    where comm = commute (idNT {F = F ∘F (G ∘F H)})

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
open import Agda.Builtin.Equality

postulate
  A : Set
  a : A
  b : A

mutual
  Meta : A → A → A → A
  Meta = ?

  _ : Meta a ≡ Meta b
  _ = refl


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.LeftAction where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.SIP

open import Cubical.Structures.Auto

module _ {ℓ ℓ' : Level} (A : Type ℓ') where

  LeftActionStructure : Type ℓ → Type (ℓ-max ℓ ℓ')
  LeftActionStructure X = A → X → X

  LeftActionEquivStr = AutoEquivStr LeftActionStructure

  leftActionUnivalentStr : UnivalentStr _ LeftActionEquivStr
  leftActionUnivalentStr = autoUnivalentStr LeftActionStructure

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Cubical.Categories.Functor where

open import Cubical.Foundations.Prelude
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Categories.Category

private
  variable
    ℓ𝒞 ℓ𝒞' ℓ𝒟 ℓ𝒟' : Level

record Functor (𝒞 : Precategory ℓ𝒞 ℓ𝒞') (𝒟 : Precategory ℓ𝒟 ℓ𝒟') : Type (ℓ-max (ℓ-max ℓ𝒞 ℓ𝒞') (ℓ-max ℓ𝒟 ℓ𝒟')) where
  no-eta-equality
  open Precategory

  field
    F-ob : 𝒞 .ob → 𝒟 .ob
    F-hom : {x y : 𝒞 .ob} → 𝒞 .hom x y → 𝒟 .hom (F-ob x) (F-ob y)
    F-idn : {x : 𝒞 .ob} → F-hom (𝒞 .idn x) ≡ 𝒟 .idn (F-ob x)
    F-seq : {x y z : 𝒞 .ob} (f : 𝒞 .hom x y) (g : 𝒞 .hom y z) → F-hom (𝒞 .seq f g) ≡ 𝒟 .seq (F-hom f) (F-hom g)

  is-full = (x y : _) (F[f] : 𝒟 .hom (F-ob x) (F-ob y)) → ∥ Σ (𝒞 .hom x y) (λ f → F-hom f ≡ F[f]) ∥
  is-faithful = (x y : _) (f g : 𝒞 .hom x y) → F-hom f ≡ F-hom g → f ≡ g

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
------------------------------------------------------------------------
-- A relational semantics which uses closures and environments
------------------------------------------------------------------------

module Lambda.Closure.Relational where

open import Codata.Musical.Notation
open import Data.Empty
open import Data.List hiding (lookup)
open import Data.Product
open import Data.Vec using (Vec; _∷_; []; lookup)
open import Function.Base
open import
  Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

open import Lambda.Syntax using (Tm; con; var; ƛ; _·_)
open Lambda.Syntax.Closure Tm
open import Lambda.VirtualMachine as VM
open VM.Relational
open StarReasoning _⟶_
open InfiniteSequence

------------------------------------------------------------------------
-- Big-step semantics

-- For terminating computations.

infix 4 _⊢_⇓_

data _⊢_⇓_ {n} (ρ : Env n) : Tm n → Value → Set where
  var : ∀ {x} → ρ ⊢ var x ⇓ lookup ρ x
  con : ∀ {i} → ρ ⊢ con i ⇓ con i
  ƛ   : ∀ {t} → ρ ⊢ ƛ t ⇓ ƛ t ρ
  app : ∀ {t₁ t₂ n t} {ρ′ : Env n} {v v′}
        (t₁⇓   : ρ ⊢ t₁ ⇓ ƛ t ρ′)
        (t₂⇓   : ρ ⊢ t₂ ⇓ v′)
        (t₁t₂⇓ : v′ ∷ ρ′ ⊢ t ⇓ v) →
        ρ ⊢ t₁ · t₂ ⇓ v

-- For non-terminating computations.

infix 4 _⊢_⇑

data _⊢_⇑ {n} (ρ : Env n) : Tm n → Set where
  app : ∀ {t₁ t₂ n t} {ρ′ : Env n} {v′}
        (t₁⇓   : ρ ⊢ t₁ ⇓ ƛ t ρ′)
        (t₂⇓   : ρ ⊢ t₂ ⇓ v′)
        (t₁t₂⇑ : ∞ (v′ ∷ ρ′ ⊢ t ⇑)) →
        ρ ⊢ t₁ · t₂ ⇑
  ·ˡ  : ∀ {t₁ t₂}
        (t₁⇑ : ∞ (ρ ⊢ t₁ ⇑)) →
        ρ ⊢ t₁ · t₂ ⇑
  ·ʳ  : ∀ {t₁ t₂ v}
        (t₁⇓ : ρ ⊢ t₁ ⇓ v)
        (t₂⇑ : ∞ (ρ ⊢ t₂ ⇑)) →
        ρ ⊢ t₁ · t₂ ⇑

-- For crashing computations.

infix 4 _⊢_↯

_⊢_↯ : ∀ {n} → Env n → Tm n → Set
ρ ⊢ t ↯ = ¬ (∃ λ v → ρ ⊢ t ⇓ v) × ¬ (ρ ⊢ t ⇑)

------------------------------------------------------------------------
-- The semantics is deterministic

deterministic⇓ : ∀ {n} {ρ : Env n} {t v₁ v₂} →
                 ρ ⊢ t ⇓ v₁ → ρ ⊢ t ⇓ v₂ → v₁ ≡ v₂
deterministic⇓ var                 var                    = P.refl
deterministic⇓ con                 con                    = P.refl
deterministic⇓ ƛ                   ƛ                      = P.refl
deterministic⇓ (app t₁⇓ t₂⇓ t₁t₂⇓) (app t₁⇓′ t₂⇓′ t₁t₂⇓′)
  with deterministic⇓ t₁⇓ t₁⇓′ | deterministic⇓ t₂⇓ t₂⇓′
... | P.refl | P.refl = deterministic⇓ t₁t₂⇓ t₁t₂⇓′

deterministic⇓⇑ : ∀ {n} {ρ : Env n} {t v} →
                  ρ ⊢ t ⇓ v → ρ ⊢ t ⇑ → ⊥
deterministic⇓⇑ var ()
deterministic⇓⇑ con ()
deterministic⇓⇑ ƛ   ()
deterministic⇓⇑ (app t₁⇓ t₂⇓ t₁t₂⇓) (app t₁⇓′ t₂⇓′ t₁t₂⇑)
  with deterministic⇓ t₁⇓ t₁⇓′ | deterministic⇓ t₂⇓ t₂⇓′
... | P.refl | P.refl = deterministic⇓⇑ t₁t₂⇓ (♭ t₁t₂⇑)
deterministic⇓⇑ (app t₁⇓ t₂⇓ t₁t₂⇓) (·ˡ t₁⇑)      =
  deterministic⇓⇑ t₁⇓ (♭ t₁⇑)
deterministic⇓⇑ (app t₁⇓ t₂⇓ t₁t₂⇓) (·ʳ t₁⇓′ t₂⇑) =
  deterministic⇓⇑ t₂⇓ (♭ t₂⇑)

------------------------------------------------------------------------
-- Compiler "correctness"

-- The proofs below establish that the compiler in
-- Lambda.VirtualMachine preserves the semantics above (_⊢_⇓_ and
-- _⊢_⇑, not necessarily _⊢_↯), given that the virtual machine is
-- deterministic.

correct⇓′ : ∀ {n ρ c s v} {t : Tm n} →
            ρ ⊢ t ⇓ v →
            ⟨ comp t c , s , comp-env ρ ⟩ ⟶⋆
            ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩
correct⇓′ {ρ = ρ} {c} {s} (var {x}) = begin
  ⟨ var x ∷ c , s                               , comp-env ρ ⟩ ⟶⟨ var ⟩
  ⟨         c , val (lookup (comp-env ρ) x) ∷ s , comp-env ρ ⟩ ≡⟨ P.cong (λ v → ⟨ c , val v ∷ s , comp-env ρ ⟩)
                                                                         (lookup-hom x ρ) ⟩
  ⟨         c , val (comp-val (lookup ρ x)) ∷ s , comp-env ρ ⟩ ∎
correct⇓′ {ρ = ρ} {c} {s} (con {i}) = begin
  ⟨ con i ∷ c ,                                     s , comp-env ρ ⟩ ⟶⟨ con ⟩
  ⟨         c , val (Lambda.Syntax.Closure.con i) ∷ s , comp-env ρ ⟩ ∎
correct⇓′ {ρ = ρ} {c} {s} (ƛ {t}) = begin
  ⟨ clo (comp t [ ret ]) ∷ c ,                          s , comp-env ρ ⟩ ⟶⟨ clo ⟩
  ⟨                        c , val (comp-val (ƛ t ρ)) ∷ s , comp-env ρ ⟩ ∎
correct⇓′ {ρ = ρ} {c} {s} {v} (app {t₁} {t₂} {t = t} {ρ′} {v′ = v′} t₁⇓ t₂⇓ t₁t₂⇓) = begin
  ⟨ comp t₁ (comp t₂ (app ∷ c)) ,                                               s ,               comp-env ρ  ⟩ ⟶⋆⟨ correct⇓′ t₁⇓ ⟩
  ⟨          comp t₂ (app ∷ c)  ,                     val (comp-val (ƛ t ρ′)) ∷ s ,               comp-env ρ  ⟩ ⟶⋆⟨ correct⇓′ t₂⇓ ⟩
  ⟨                   app ∷ c   , val (comp-val v′) ∷ val (comp-val (ƛ t ρ′)) ∷ s ,               comp-env ρ  ⟩ ⟶⟨ app ⟩
  ⟨ comp t [ ret ]              ,                          ret c (comp-env ρ) ∷ s , comp-val v′ ∷ comp-env ρ′ ⟩ ⟶⋆⟨ correct⇓′ t₁t₂⇓ ⟩
  ⟨        [ ret ]              ,       val (comp-val v) ∷ ret c (comp-env ρ) ∷ s , comp-val v′ ∷ comp-env ρ′ ⟩ ⟶⟨ ret ⟩
  ⟨                         c   ,       val (comp-val v) ∷                      s ,               comp-env ρ  ⟩ ∎

correct⇑′ : ∀ {n ρ c s} {t : Tm n} →
            ρ ⊢ t ⇑ → ⟨ comp t c , s , comp-env ρ ⟩ ⟶∞′
correct⇑′ {ρ = ρ} {c} {s} (app {t₁} {t₂} {t = t} {ρ′} {v′} t₁⇓ t₂⇓ t₁t₂⇑) =
  ⟨ comp t₁ (comp t₂ (app ∷ c)) ,                                               s ,               comp-env ρ  ⟩ ⟶⋆⟨ correct⇓′ t₁⇓ ⟩′
  ⟨          comp t₂ (app ∷ c)  ,                     val (comp-val (ƛ t ρ′)) ∷ s ,               comp-env ρ  ⟩ ⟶⋆⟨ correct⇓′ t₂⇓ ⟩′
  ⟨                   app ∷ c   , val (comp-val v′) ∷ val (comp-val (ƛ t ρ′)) ∷ s ,               comp-env ρ  ⟩ ⟶⟨ app ⟩′ ♯
 (⟨ comp t [ ret ]              ,                          ret c (comp-env ρ) ∷ s , comp-val v′ ∷ comp-env ρ′ ⟩ ⟶∞⟨ correct⇑′ (♭ t₁t₂⇑) ⟩)
correct⇑′ {ρ = ρ} {c} {s} (·ˡ {t₁} {t₂} t₁⇑) =
  ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩ ⟶∞⟨ correct⇑′ (♭ t₁⇑) ⟩
correct⇑′ {ρ = ρ} {c} {s} (·ʳ {t₁} {t₂} {v} t₁⇓ t₂⇑) =
  ⟨ comp t₁ (comp t₂ (app ∷ c)) ,                    s , comp-env ρ ⟩ ⟶⋆⟨ correct⇓′ t₁⇓ ⟩′
  ⟨          comp t₂ (app ∷ c)  , val (comp-val v) ∷ s , comp-env ρ ⟩ ⟶∞⟨ correct⇑′ (♭ t₂⇑) ⟩

correct⇓ : ∀ {t v} →
           [] ⊢ t ⇓ v →
           ∃ λ s → ⟨ comp t [] , [] , [] ⟩ ⟶⋆ s × s ⇓ comp-val v
correct⇓ t⇓ = (_ , correct⇓′ t⇓ , final)

correct⇑ : ∀ {t} → [] ⊢ t ⇑ → ⟨ comp t [] , [] , [] ⟩ ⟶∞
correct⇑ = InfiniteSequence.sound ∘ correct⇑′

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module Prelude where

data _==_ {A : Set}(x : A) : A → Set where
  refl : x == x

J : {A : Set} {x y : A} (P : (x y : A) → x == y -> Set) →
    (∀ z → P z z refl) → (p : x == y) → P x y p
J P h refl = h _

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module CompareLevel where

open import Common.Level

postulate
  X : Set
  Foo : (a b : Level) → Set (a ⊔ b) → Set
  Bar : Foo _ _ X  -- solve _1 ⊔ _2 = 0

postulate
  id    : ∀ {a}{A : Set a} → A → A
  apply : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → A → B
  a b   : Level
  Any   : (ℓ : Level) → Set ℓ
  any   : ∀ {ℓ} → Any ℓ

-- Too aggressive level solving can cause a problem here.
foo : Any (a ⊔ b)
foo =
  apply {_}{_} id any


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

module Categories.Category.Construction.Properties.Functors where

open import Categories.Category.Complete.Properties
  using ( Functors-Complete
        ; evalF-Continuous)
  public
open import Categories.Category.Cocomplete.Properties
  using (Functors-Cocomplete)
  public

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Andreas, 2012-01-10
-- {-# OPTIONS -v tc.constr.findInScope:50 #-}
module InstanceGuessesMeta2 where

open import Common.Level

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

record takeClass {a}
  (F : Set a → Set a)
  (G : Set a → ℕ → Set a) : Set (lsuc a) where
  field
    take : {A : Set a} → (n : ℕ) → F A → G A n

take : ∀ {a} {A : Set a} {F : Set a → Set a} {G : Set a → ℕ → Set a}
   {{takeA : takeClass F G}} →
   (n : ℕ) → F A → G A n
take {{takeA}} = takeClass.take takeA

postulate
  List : ∀ {a} → Set a → Set a
  BVec : ∀ {a} → Set a → ℕ → Set a
  toList : ∀ {a}{A : Set a}{n : ℕ} → BVec A n → List A
  -- universe polymorphic instance
  takeInstanceList : {a : Level} → takeClass (List {a = a}) BVec

take0 : {A : Set} → List A → BVec A zero
take0 l = take zero l

take1 : {A : Set} → List A → List A
take1 l = toList (take (suc zero) l)

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


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

module FOT.Agsy.AddTotality where

open import Relation.Binary.PropositionalEquality

infixl 9 _+_

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

postulate
  D    : Set
  zero : D
  succ : D → D

data N : D → Set where
  zN :               N zero
  sN : ∀ {n} → N n → N (succ n)

postulate
  _+_  : D → D → D
  +-0x : ∀ d →   zero   + d ≡ d
  +-Sx : ∀ d e → succ d + e ≡ succ (d + e)

+-N : ∀ {m n} → N m → N n → N (m + n)
+-N {m} {n} Nm Nn = {!-c -m -t 20!}  -- No solution found at time out (20s).

+-N₁ : ∀ {m n} → N m → N n → N (m + n)
+-N₁ zN Nn = {!-m!}   -- No solution found

+-N₁ (sN Nm) Nn = {!-m!} -- No solution found.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Relation.Unary.Monotone.Prefix {ℓ}{T : Set ℓ} where

open import Data.List.Prefix
open import Data.List as List
open import Data.List.Membership.Propositional
open import Data.List.All as All

open import Relation.Unary.Monotone (⊑-preorder {A = T})

instance
  open Monotone

  any-monotone : ∀ {x : T} → Monotone (λ xs → x ∈ xs)
  wk any-monotone ext l = ∈-⊒ l ext


text:
module Terms where

import Level
open import Data.Unit as Unit
open import Data.List as List
open import Data.Product as Product
open import Categories.Category using (Category)

open import Types

open import Common.Context GType
  using (Ctx; Var; zero; ctx-cat; ctx-bin-coproducts)
  renaming (succ to succ′)
open Categories.Category.Category ctx-cat
  renaming ( _⇒_ to _▹_
           ; _≡_ to _≈_
           ; _∘_ to _●_
           ; id  to ctx-id
           )
open import Categories.Object.BinaryCoproducts ctx-cat
open BinaryCoproducts ctx-bin-coproducts

-- | Signatures over which we can define terms
Sig = Ctx

-- | Typed patterns
data Pat : (a : GType) → Set where
  var′ : ∀{a : GType}       (x : Var [ a ] a)                 → Pat a
  κ₁′  : ∀{a₁ a₂ : GType}   (p : Pat a₁)           → Pat (a₁ ⊕ a₂)
  κ₂′  : ∀{a₁ a₂ : GType}   (p : Pat a₂)           → Pat (a₁ ⊕ a₂)
  α′   : ∀{a : Type [ tt ]} (p : Pat (unfold-μ a)) → Pat (μ a)

-- | Context defined by a pattern (this is either empty or contains a single
--   variable).
pat-ctx : ∀ {a} → Pat a → Ctx
pat-ctx {a} (var′ x) = [ a ]
pat-ctx     (κ₁′ x)  = pat-ctx x
pat-ctx     (κ₂′ x)  = pat-ctx x
pat-ctx     (α′ x)   = pat-ctx x

-- | Typed copatterns
data Copat : (a b : GType) → Set where
  ·    : ∀{a}                                                   → Copat a a
  app′ : ∀{a b c : GType}               (q : Copat (b ⇒ c) a)
                                        (p : Pat c)             → Copat c a
  π₁′  : ∀{a₁ a₂ a : GType}             (q : Copat (a₁ ⊗ a₂) a) → Copat a₁ a
  π₂′  : ∀{a₁ a₂ a : GType}             (q : Copat (a₁ ⊗ a₂) a) → Copat a₂ a
  ξ′   : ∀{b : Type [ tt ]} {a : GType} (q : Copat (ν b) a)     → Copat (unfold-ν b) a

-- | Context defined by a copattern
copat-ctx : ∀ { a b} → Copat a b → Ctx
copat-ctx ·          = []
copat-ctx (app′ q p) = (copat-ctx q) ∐ (pat-ctx p)
copat-ctx (π₁′ q)    = copat-ctx q
copat-ctx (π₂′ q)    = copat-ctx q
copat-ctx (ξ′ q)     = copat-ctx q

mutual
  -- | A clause { q₁ ↦ t₁ ; ... ; qₙ ↦ tₙ } defines the body of a λ-abstraction
  --   of the definition of a symbol in a signature.
  record Clause {Δ : Sig} {Γ : Ctx} {a : GType} : Set where
    inductive
    field
      body : List (
                  Σ GType (λ b →
                  Σ (Copat a b) (λ q →
                    (Term {Δ} ((copat-ctx q) ∐ Γ) b)))
             )

  -- | Terms typed in a context
  data Term {Δ : Sig} (Γ : Ctx) : GType → Set where
    var  : ∀{a : GType}       (x : Var Γ a)                 → Term Γ a
    κ₁   : ∀{a₁ a₂ : GType}   (t : Term {Δ} Γ a₁)           → Term Γ (a₁ ⊕ a₂)
    κ₂   : ∀{a₁ a₂ : GType}   (t : Term {Δ} Γ a₂)           → Term Γ (a₁ ⊕ a₂)
    α    : ∀{a : Type [ tt ]} (t : Term {Δ} Γ (unfold-μ a)) → Term Γ (μ a)
    app  : ∀{a b : GType}     (t : Term {Δ} Γ (a ⇒ b))
                              (s : Term {Δ} Γ a)            → Term Γ b
    π₁   : ∀{a₁ a₂ : GType}   (t : Term {Δ} Γ (a₁ ⊗ a₂))    → Term Γ a₁
    π₂   : ∀{a₁ a₂ : GType}   (t : Term {Δ} Γ (a₁ ⊗ a₂))    → Term Γ a₂
    ξ    : ∀{a : Type [ tt ]} (t : Term {Δ} Γ (ν a))        → Term Γ (unfold-ν a)
    svar : ∀{a : GType}       (f : Var Δ a)                 → Term Γ a
    abs  : ∀{a : GType}       (D : Clause {Δ} {Γ} {a})      → Term Γ a
    rlet : ∀{a : GType} {Δ' : Sig} →
           (Ω : Definition Δ') → Term {Δ ∐ Δ'} Γ a → Term {Δ} Γ a

  -- | A definition consists of a signature and its definition
  data DeclBlock : Sig → Set where
    empty : DeclBlock []

  record Definition (Δ : Sig) : Set where
    inductive
    field
      defs : List (Σ GType (λ a → (Var Δ a) × Clause {Δ} {[]} {a}))
open Definition

TermWDef : GType → Set
TermWDef a = Σ Sig (λ Δ → (Definition Δ) × (Term {Δ} [] a))

---------- Convenience
_↦_ : ∀{Δ : Sig} {Γ : Ctx} {a b : GType}
          (q : Copat a b) (t : Term {Δ} ((copat-ctx q) ∐ Γ) b) →
            (Σ GType (λ b →
              Σ (Copat a b) (λ q →
              (Term {Δ} ((copat-ctx q) ∐ Γ) b))))
_↦_ {b = b} q t = b , q , t

_≝_ : ∀{Δ : Sig} {a : GType}
      (f : Var Δ a) (c : Clause {Δ} {[]} {a}) →
        Σ GType (λ a → (Var Δ a) × Clause {Δ} {[]} {a})
_≝_ {a = a} f c = a , (f , c)

--------------------------------
------ Examples

-- 〈〉 : Term [] unit
-- 〈〉 = ?

{-
hd : ∀ {a : GType} → Term (Str a) → Term a
hd t = π₁ (ξ q)

hd′ : ∀ {a b : GType} → Copat (Str a) b → Copat a b
hd′ q = π₁′ (ξ′ q)

ones : TermWDef (Str Nat)
ones = Δ , def , (svar o)
  where
    Δ : Sig
    Δ = [ Str Nat ]
    o : Var [ Str Nat ] (Str Nat)
    o = zero
    o-def : Clause {[ Str Nat ]} {[]} {Str Nat}
    o-def = record
      { body =
        [ (· ↦ svar o) ]
      }
    def : Definition Δ
    def = record
      { defs =
        [ o ≝ o-def ]
      }
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox