text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to multiplication of integers
------------------------------------------------------------------------

module Data.Integer.Multiplication.Properties where

open import Algebra
  using (module CommutativeSemiring; CommutativeMonoid)
import Algebra.FunctionProperties
open import Algebra.Structures using (IsSemigroup; IsCommutativeMonoid)
open import Data.Integer
   using (ℤ; -[1+_]; +_; ∣_∣; sign; _◃_) renaming (_*_ to ℤ*)
open import Data.Nat
  using (suc; zero) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Product using (proj₂)
import Data.Nat.Properties as ℕ
open import Data.Sign using () renaming (_*_ to _S*_)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; cong; cong₂; isEquivalence)

open Algebra.FunctionProperties (_≡_ {A = ℤ})
open CommutativeSemiring ℕ.commutativeSemiring
  using (+-identity; *-comm) renaming (zero to *-zero)

------------------------------------------------------------------------
-- Multiplication and one form a commutative monoid

private

  identityˡ : LeftIdentity (+ 1) ℤ*
  identityˡ (+ zero ) = refl
  identityˡ -[1+  n ] rewrite proj₂ +-identity n = refl
  identityˡ (+ suc n) rewrite proj₂ +-identity n = refl

  comm : Commutative ℤ*
  comm -[1+ a ] -[1+ b ] rewrite *-comm (suc a) (suc b) = refl
  comm -[1+ a ] (+   b ) rewrite *-comm (suc a) b       = refl
  comm (+   a ) -[1+ b ] rewrite *-comm a       (suc b) = refl
  comm (+   a ) (+   b ) rewrite *-comm a       b       = refl

  lemma : ∀ a b c → c ℕ+ (b ℕ+ a ℕ* suc b) ℕ* suc c
                  ≡ c ℕ+ b ℕ* suc c ℕ+ a ℕ* suc (c ℕ+ b ℕ* suc c)
  lemma =
    solve 3 (λ a b c → c :+ (b :+ a :* (con 1 :+ b)) :* (con 1 :+ c)
                    := c :+ b :* (con 1 :+ c) :+
                       a :* (con 1 :+ (c :+ b :* (con 1 :+ c))))
            refl
    where open ℕ.SemiringSolver

  assoc : Associative ℤ*
  assoc (+ zero) _ _ = refl
  assoc x (+ zero) _ rewrite proj₂ *-zero ∣ x ∣ = refl
  assoc x y (+ zero) rewrite
      proj₂ *-zero ∣ y ∣
    | proj₂ *-zero ∣ x ∣
    | proj₂ *-zero ∣ sign x S* sign y ◃ ∣ x ∣ ℕ* ∣ y ∣ ∣
    = refl
  assoc -[1+ a  ] -[1+ b  ] (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
  assoc -[1+ a  ] (+ suc b) -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
  assoc (+ suc a) (+ suc b) (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
  assoc (+ suc a) -[1+ b  ] -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
  assoc -[1+ a  ] -[1+ b  ] -[1+ c  ] = cong -[1+_]     (lemma a b c)
  assoc -[1+ a  ] (+ suc b) (+ suc c) = cong -[1+_]     (lemma a b c)
  assoc (+ suc a) -[1+ b  ] (+ suc c) = cong -[1+_]     (lemma a b c)
  assoc (+ suc a) (+ suc b) -[1+ c  ] = cong -[1+_]     (lemma a b c)

  isSemigroup : IsSemigroup _ _
  isSemigroup = record
    { isEquivalence = isEquivalence
    ; assoc         = assoc
    ; ∙-cong        = cong₂ ℤ*
    }

  isCommutativeMonoid : IsCommutativeMonoid _≡_ ℤ* (+ 1)
  isCommutativeMonoid = record
    { isSemigroup = isSemigroup
    ; identityˡ   = identityˡ
    ; comm        = comm
    }

commutativeMonoid : CommutativeMonoid _ _
commutativeMonoid = record
  { Carrier             = ℤ
  ; _≈_                 = _≡_
  ; _∙_                 = ℤ*
  ; ε                   = + 1
  ; isCommutativeMonoid = isCommutativeMonoid
  }


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

open import LogicalFormulae
open import Lists.Lists
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Decidable.Sets
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Semiring

module Computability.LambdaCalculus.ChurchNumeral where

open import UnorderedSet.Definition ℕDecideEquality
open import Computability.LambdaCalculus.Definition

private
  iter : ℕ → Term
  iter zero = var 0
  iter (succ n) = apply (var 1) (iter n)

church : ℕ → Term
church n = lam 1 (lam 0 (iter n))

churchSucc : Term
churchSucc = lam 0 (lam 1 (lam 2 (apply (var 1) (apply (apply (var 0) (var 1)) (var 2)))))

ext: agda


text:
------------------------------------------------------------------------------
-- The FOTC streams type
------------------------------------------------------------------------------

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

module FOTC.Data.Stream.Type where

open import FOTC.Base
open import FOTC.Base.List

------------------------------------------------------------------------------
-- The FOTC streams type (co-inductive predicate for total streams).

-- Functional for the Stream predicate.
-- StreamF : (D → Set) → D → Set
-- StreamF A xs = ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs'

-- Stream is the greatest fixed-point of StreamF (by Stream-out and
-- Stream-coind).

postulate Stream : D → Set

postulate
-- Stream is a post-fixed point of StreamF, i.e.
--
-- Stream ≤ StreamF Stream.
  Stream-out : ∀ {xs} → Stream xs → ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Stream xs'
{-# ATP axiom Stream-out #-}

-- Stream is the greatest post-fixed point of StreamF, i.e.
--
-- ∀ A. A ≤ StreamF A ⇒ A ≤ Stream.
--
-- N.B. This is an axiom schema. Because in the automatic proofs we
-- *must* use an instance, we do not add this postulate as an ATP
-- axiom.
postulate
  Stream-coind :
    (A : D → Set) →
    -- A is post-fixed point of StreamF.
    (∀ {xs} → A xs → ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs') →
    -- Stream is greater than A.
    ∀ {xs} → A xs → Stream xs

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

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

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module Imports.NonTerminating where

Foo : Set
Foo = Foo

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import HoTT

module homotopy.S1SuspensionS0 where

{- To -}

module To = S¹Rec (north Bool) (merid _ false ∙ ! (merid _ true))

to : S¹ → Suspension Bool
to = To.f

{- From -}

from-merid : Bool → base == base
from-merid true = loop
from-merid false = idp

module From = SuspensionRec Bool base base from-merid

from : Suspension Bool → S¹
from = From.f

{- ToFrom and FromTo -}

postulate  -- TODO, easy and boring
  to-from : (x : Suspension Bool) → to (from x) == x
  from-to : (x : S¹) → from (to x) == x

e : S¹ ≃ Suspension Bool
e = equiv to from to-from from-to

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}

module Cubical.Algebra.Group.EilenbergMacLane.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.Path
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Transport

open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec; elim to trElim)
open import Cubical.HITs.EilenbergMacLane1 hiding (elim)
open import Cubical.Algebra.AbGroup.Base
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec) hiding (elim)
open import Cubical.HITs.Truncation
  renaming (elim to trElim ; rec to trRec ; rec2 to trRec2)
open import Cubical.Data.Nat hiding (_·_ ; elim)
open import Cubical.HITs.Susp
open import Cubical.Functions.Morphism
open import Cubical.Foundations.Path

private
  variable ℓ ℓ' : Level

  _* = AbGroup→Group

EM-raw : (G : AbGroup ℓ) (n : ℕ) → Type ℓ
EM-raw G zero = fst G
EM-raw G (suc zero) = EM₁ (G *)
EM-raw G (suc (suc n)) = Susp (EM-raw G (suc n))

ptEM-raw : {n : ℕ} {G : AbGroup ℓ} → EM-raw G n
ptEM-raw {n = zero} {G = G} = AbGroupStr.0g (snd G)
ptEM-raw {n = suc zero} {G = G} = embase
ptEM-raw {n = suc (suc n)} {G = G} = north

raw-elim : (G : AbGroup ℓ) (n : ℕ) {A : EM-raw G (suc n) → Type ℓ'}
            → ((x : _) → isOfHLevel (suc n) (A x) )
            → A ptEM-raw
            → (x : _) → A x
raw-elim G zero hlev b = elimProp _ hlev b
raw-elim G (suc n) hlev b north = b
raw-elim G (suc n) {A = A} hlev b south = subst A (merid ptEM-raw) b
raw-elim G (suc n) {A = A} hlev b (merid a i) = help a i
  where
  help : (a : _) → PathP (λ i → A (merid a i)) b (subst A (merid ptEM-raw) b)
  help = raw-elim G n (λ _ → isOfHLevelPathP' (suc n) (hlev _) _ _)
         λ i → transp (λ j → A (merid ptEM-raw (j ∧ i))) (~ i) b

EM : (G : AbGroup ℓ) (n : ℕ) → Type ℓ
EM G zero = EM-raw G zero
EM G (suc zero) = EM-raw G 1
EM G (suc (suc n)) = hLevelTrunc (4 + n) (EM-raw G (suc (suc n)))

0ₖ : {G : AbGroup ℓ} (n : ℕ) → EM G n
0ₖ {G = G} zero = AbGroupStr.0g (snd G)
0ₖ (suc zero) = embase
0ₖ (suc (suc n)) = ∣ ptEM-raw ∣

EM∙ : (G : AbGroup ℓ) (n : ℕ) → Pointed ℓ
EM∙ G n = EM G n , (0ₖ n)

EM-raw∙ : (G : AbGroup ℓ) (n : ℕ) → Pointed ℓ
EM-raw∙ G n = EM-raw G n , ptEM-raw

hLevelEM : (G : AbGroup ℓ) (n : ℕ) → isOfHLevel (2 + n) (EM G n)
hLevelEM G zero = AbGroupStr.is-set (snd G)
hLevelEM G (suc zero) = emsquash
hLevelEM G (suc (suc n)) = isOfHLevelTrunc (4 + n)

EM-raw→EM : (G : AbGroup ℓ) (n : ℕ) → EM-raw G n → EM G n
EM-raw→EM G zero x = x
EM-raw→EM G (suc zero) x = x
EM-raw→EM G (suc (suc n)) = ∣_∣

elim : {G : AbGroup ℓ} (n : ℕ) {A : EM G n → Type ℓ'}
        → ((x : _) → isOfHLevel (2 + n) (A x))
        → ((x : EM-raw G n) → A (EM-raw→EM G n x))
        → (x : _) → A x
elim zero hlev hyp x = hyp x
elim (suc zero) hlev hyp x = hyp x
elim (suc (suc n)) hlev hyp = trElim (λ _ → hlev _) hyp

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Cubical.HITs.Torus.Base public

-- open import Cubical.HITs.Torus.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import lib.Basics
open import lib.types.Pointed

module lib.types.Lift where

⊙Lift : ∀ {i j} → Ptd i → Ptd (lmax i j)
⊙Lift {j = j} (A , a) =  ⊙[ Lift {j = j} A , lift a ]

⊙lift : ∀ {i j} {X : Ptd i} → fst (X ⊙→ ⊙Lift {j = j} X)
⊙lift = (lift , idp)

⊙lower : ∀ {i j} {X : Ptd i} → fst (⊙Lift {j = j} X ⊙→ X)
⊙lower = (lower , idp)

Lift-level : ∀ {i j} {A : Type i} {n : ℕ₋₂} →
  has-level n A → has-level n (Lift {j = j} A)
Lift-level = equiv-preserves-level ((lift-equiv)⁻¹)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda


text:
{-# OPTIONS --without-K #-}
-- Large indices are not allowed --without-K

data Singleton {a} {A : Set a} : A → Set where
  [_] : ∀ x → Singleton x


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

-- Normalization by Evaluation for Call-By-Push-Value

module NfCBPV where

-- Imports from the Agda standard library.

open import Library hiding (_×̇_)

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)

pattern here! = here refl

-- We postulate a set of generic value types.
-- There are no operations defined on these types, thus,
-- they play the type of (universal) type variables.

postulate Base : Set

-- Variants (Σ) (and records (Π), resp.) can in principle have any number of
-- constructors (fields, resp.), including infinitely one.
-- In general, the constructor (field, resp.) names are given by a set I.
-- However, I : Set would make syntax already a big type, living in Set₁.
-- To keep it in Set₀, we only consider variants (records) with finitely
-- many constructors (fields), thus, I : ℕ.
-- Branching over I is then realized as functions out of El I, where
-- El I = { i | i < I} = Fin I.

set = ℕ
El  = Fin

-- Let I range over arities (constructor/field sets) and i over
-- constructor/field names.

variable
  I : set
  i : El I

-- The types of CBPV are classified into value types P : Ty⁺ which we
-- refer to as positive types, and computation types N : Ty⁻ which we
-- refer to as negative types.

mutual

  -- Value types

  data Ty⁺ : Set where
    base  : (o : Base) → Ty⁺                   -- Base type.
    _×̇_   : (P₁ P₂ : Ty⁺) → Ty⁺                -- Finite product (tensor).
    Σ̇     : (I : set) (Ps : El I → Ty⁺) → Ty⁺  -- Variant (sum).
    □̇     : (N : Ty⁻) → Ty⁺                    -- Thunk (U).

  -- Computation types

  data Ty⁻ : Set where
    ◇̇    : (P : Ty⁺) → Ty⁻                     -- Comp (F).
    Π̇    : (I : set) (Ns : El I → Ty⁻) → Ty⁻   -- Record (lazy product).
    _⇒̇_  : (P : Ty⁺) (N : Ty⁻) → Ty⁻           -- Function type.

-- In CBPV, a variable stands for a value.
-- Thus, environments only contain values,
-- and typing contexts only value types.

-- We use introduce syntax in an intrinsically well-typed way
-- with variables being de Bruijn indices into the typing context.
-- Thus, contexts are just lists of types.

Cxt = List Ty⁺

variable
  Γ Δ Φ            : Cxt
  P P₁ P₂ P' P′ Q  : Ty⁺
  N N₁ N₂ N' N′    : Ty⁻
  Ps               : El I → Ty⁺
  Ns               : El I → Ty⁻

-- Generic values

module _ (Var : Ty⁺ → Cxt → Set) (Comp : Ty⁻ → Cxt → Set) where

  -- Right non-invertible

  data Val' : (P : Ty⁺) (Γ : Cxt) → Set where
    var    : ∀{Γ P}      (x : Var P Γ)                      → Val' P Γ
    pair   : ∀{Γ P₁ P₂}  (v₁ : Val' P₁ Γ) (v₂ : Val' P₂ Γ)  → Val' (P₁ ×̇ P₂) Γ
    inj    : ∀{Γ I P} i  (v : Val' (P i) Γ)                 → Val' (Σ̇ I P) Γ
    thunk  : ∀{Γ N}      (t : Comp N Γ)                     → Val' (□̇ N) Γ

-- Terms

mutual

  Val = Val' _∈_ Comp

  data Comp : (N : Ty⁻) (Γ : Cxt) → Set where
    -- introductions
    ret    : ∀{Γ P}        (v : Val P Γ)             → Comp (◇̇ P) Γ
    rec    : ∀{Γ I N}      (t : ∀ i → Comp (N i) Γ)  → Comp (Π̇ I N) Γ
    abs    : ∀{Γ P N}      (t : Comp N (P ∷ Γ))      → Comp (P ⇒̇ N) Γ
    -- positive eliminations
    split  : ∀{Γ P₁ P₂ N}  (v : Val (P₁ ×̇ P₂) Γ)  (t : Comp N (P₂ ∷ P₁ ∷ Γ))     → Comp N Γ
    case   : ∀{Γ I Ps N}   (v : Val (Σ̇ I Ps) Γ)   (t : ∀ i → Comp N (Ps i ∷ Γ))  → Comp N Γ
    bind   : ∀{Γ P N}      (u : Comp (◇̇ P) Γ)     (t : Comp N (P ∷ Γ))           → Comp N Γ
    -- cut
    letv   : ∀{Γ P N}      (v : Val P Γ)          (t : Comp N (P ∷ Γ))           → Comp N Γ
    -- negative eliminations
    force  : ∀{Γ N}        (v : Val (□̇ N) Γ)                     → Comp N Γ
    prj    : ∀{Γ I Ns} i   (t : Comp (Π̇ I Ns) Γ)                 → Comp (Ns i) Γ
    app    : ∀{Γ P N}      (t : Comp (P ⇒̇ N) Γ)   (v : Val P Γ)  → Comp N Γ

-- Normal forms
------------------------------------------------------------------------

-- Normal values only reference variables of base type

NVar : (P : Ty⁺) (Γ : Cxt) → Set
NVar (base o) Γ = base o ∈ Γ
NVar _ _ = ⊥

-- Negative neutrals

module _ (Val : Ty⁺ → Cxt → Set) where

  -- Right non-invertible

  data Ne' : (N : Ty⁻) (Γ : Cxt) → Set where
    force  : ∀{Γ N}      (x : □̇ N ∈ Γ)                      → Ne' N Γ
    prj    : ∀{Γ I N} i  (t : Ne' (Π̇ I N) Γ)                → Ne' (N i) Γ
    app    : ∀{Γ P N}    (t : Ne' (P ⇒̇ N) Γ) (v : Val P Γ)  → Ne' N Γ

mutual

  NVal = Val' NVar Nf
  Ne   = Ne' NVal

  -- Cover monad

  data ◇ (J : Cxt → Set) (Γ : Cxt) : Set where
    return  : (j : J Γ)                                                  → ◇ J Γ
    bind    : ∀{P}      (u : Ne (◇̇ P) Γ)     (t :          ◇ J (P ∷ Γ))  → ◇ J Γ
    case    : ∀{I Ps}   (x : Σ̇ I Ps ∈ Γ)     (t : ∀ i → ◇ J (Ps i ∷ Γ))  → ◇ J Γ
    split   : ∀{P₁ P₂}  (x : (P₁ ×̇ P₂) ∈ Γ)  (t :    ◇ J (P₂ ∷ P₁ ∷ Γ))  → ◇ J Γ

  data NComp (Q : Ty⁺) (Γ : Cxt) : Set where
    ret    :           (v : NVal Q Γ)    → NComp Q Γ   -- Invoke RFoc
    ne     :           (n : Ne (◇̇ Q) Γ)  → NComp Q Γ   -- Finish with LFoc
      -- e.g. app (force f) x

    -- Use lemma LFoc
    bind   : ∀{P}      (u : Ne (◇̇ P) Γ)     (t : NComp Q (P ∷ Γ))           → NComp Q Γ

    -- Left invertible
    split  : ∀{P₁ P₂}  (x : (P₁ ×̇ P₂) ∈ Γ)  (t :    NComp Q (P₂ ∷ P₁ ∷ Γ))  → NComp Q Γ
    case   : ∀{I Ps}   (x : Σ̇ I Ps    ∈ Γ)  (t : ∀ i → NComp Q (Ps i ∷ Γ))  → NComp Q Γ

  -- Right invertible

  data Nf : (N : Ty⁻) (Γ : Cxt) → Set where
    ret   : ∀{Γ P}    (v : ◇ (NVal P) Γ)      → Nf (◇̇ P) Γ   -- Invoke RFoc
    ne    : ∀{Γ o}    (let N = ◇̇ (base o))
                      (n : ◇ (Ne N) Γ)        → Nf N Γ
    -- comp  : ∀{Γ P}   (t : NComp P Γ)        → Nf (◇̇ P) Γ
    rec   : ∀{Γ I N}  (t : ∀ i → Nf (N i) Γ)  → Nf (Π̇ I N) Γ
    abs   : ∀{Γ P N}  (t : Nf N (P ∷ Γ))      → Nf (P ⇒̇ N) Γ

-- Context-indexed sets
------------------------------------------------------------------------

ISet = (Γ : Cxt) → Set

variable
  A B C : ISet
  F G   : (i : El I) → ISet

-- Constructions on ISet

1̂ : ISet
1̂ Γ = ⊤

_×̂_ : (A B : ISet) → ISet
(A ×̂ B) Γ = A Γ × B Γ

Σ̂ : (I : set) (F : El I → ISet) → ISet
(Σ̂ I F) Γ = ∃ λ i → F i Γ

_⇒̂_ : (A B : ISet) → ISet
(A ⇒̂ B) Γ = A Γ → B Γ

Π̂ : (I : set) (F : El I → ISet) → ISet
(Π̂ I F) Γ = ∀ i → F i Γ

⟨_⟩ : (P : Ty⁺) (A : ISet) → ISet
⟨ P ⟩ A Γ = A (P ∷ Γ)

-- Morphisms between ISets

_→̇_ : (A B : Cxt → Set) → Set
A →̇ B = ∀{Γ} → A Γ → B Γ

⟨_⊙_⟩→̇_ : (P Q R : Cxt → Set) → Set
⟨ P ⊙ Q ⟩→̇ R = ∀{Γ} → P Γ → Q Γ → R Γ

⟨_⊙_⊙_⟩→̇_ : (P Q R S : Cxt → Set) → Set
⟨ P ⊙ Q ⊙ R ⟩→̇ S = ∀{Γ} → P Γ → Q Γ → R Γ → S Γ

Map : (F : (Cxt → Set) → Cxt → Set) → Set₁
Map F = ∀{A B : Cxt → Set} (f : A →̇ B) → F A →̇ F B

Π-map : (∀ i → F i →̇ G i) → Π̂ I F →̇ Π̂ I G
Π-map f r i = f i (r i)

-- -- Introductions and eliminations for ×̂

-- p̂air : ⟨ A ⊙ B ⟩→̇ (A ×̂ B)
-- p̂air a b = λ

-- Monotonicity
------------------------------------------------------------------------

-- Monotonization □ is a monoidal comonad

□ : (A : Cxt → Set) → Cxt → Set
□ A Γ = ∀{Δ} (τ : Γ ⊆ Δ) → A Δ

extract : □ A →̇ A
extract a = a ⊆-refl

duplicate : □ A →̇ □ (□ A)
duplicate a τ τ′ = a (⊆-trans τ τ′)

□-map : Map □
□-map f a τ = f (a τ)

extend : (□ A →̇ B) → □ A →̇ □ B
extend f = □-map f ∘ duplicate

□-weak : □ A →̇ ⟨ P ⟩ (□ A)
□-weak a τ = a (⊆-trans (_ ∷ʳ ⊆-refl) τ)

□-weak' : □ A →̇ □ (⟨ P ⟩ A)
□-weak' a τ = a (_ ∷ʳ τ)

□-sum : Σ̂ I (□ ∘ F) →̇ □ (Σ̂ I F)
□-sum (i , a) τ = i , a τ

-- Monoidality:

□-unit : 1̂ →̇ □ 1̂
□-unit = _

□-pair : ⟨ □ A ⊙ □ B ⟩→̇ □ (A ×̂ B)
□-pair a b τ = (a τ , b τ)

-- Strong functoriality

Map! : (F : (Cxt → Set) → Cxt → Set) → Set₁
Map! F = ∀{A B : Cxt → Set} → ⟨ □ (A ⇒̂ B) ⊙ F A ⟩→̇ F B

-- Monotonicity

Mon : (A : Cxt → Set) → Set
Mon A = A →̇ □ A

monVar : Mon (P ∈_)
monVar x τ = ⊆-lookup τ x

-- Positive ISets are monotone

□-mon : Mon (□ A)
□-mon = duplicate

1-mon : Mon 1̂
1-mon = □-unit

×-mon : Mon A → Mon B → Mon (A ×̂ B)
×-mon mA mB (a , b) = □-pair (mA a) (mB b)

Σ-mon : ((i : El I) → Mon (F i)) → Mon (Σ̂ I F)
Σ-mon m (i , a) = □-sum (i , m i a)

□-intro : Mon A → (A →̇ B) → (A →̇ □ B)
□-intro mA f = □-map f ∘ mA

-- Cover monad: a strong monad
------------------------------------------------------------------------

join : ◇ (◇ A) →̇ ◇ A
join (return c)  = c
join (bind u c)  = bind u (join c)
join (case x t)  = case x (join ∘ t)
join (split x c) = split x (join c)

◇-map : Map ◇
◇-map f (return  j) = return  (f j)
◇-map f (bind  u a) = bind  u (◇-map f a)
◇-map f (case  x t) = case  x (λ i → ◇-map f (t i))
◇-map f (split x a) = split x (◇-map f a)

◇-map! : Map! ◇
◇-map! f (return  j) = return  (extract f j)
◇-map! f (bind  u a) = bind  u (◇-map! (□-weak f) a)
◇-map! f (case  x t) = case  x (λ i → ◇-map! (□-weak f) (t i))
◇-map! f (split x a) = split x (◇-map! (□-weak (□-weak f)) a)

◇-bind : A →̇ ◇ B → ◇ A →̇ ◇ B
◇-bind f = join ∘ ◇-map f

◇-record : ◇ (Π̂ I F) →̇ Π̂ I (◇ ∘ F)
◇-record c i = ◇-map (_$ i) c

◇-fun : Mon A → ◇ (A ⇒̂ B) →̇ (A ⇒̂ ◇ B)
◇-fun mA c a = ◇-map! (λ τ f → f (mA a τ)) c

-- Monoidal functoriality

-- ◇-pair : ⟨ ◇ A ⊙ ◇ B ⟩→̇ ◇ (A ×̂ B)  -- does not hold!

◇-pair : ⟨ □ (◇ A) ⊙ ◇ (□ B) ⟩→̇ ◇ (A ×̂ B)
◇-pair ca = join ∘ ◇-map! λ τ b → ◇-map! (λ τ′ a → a , b τ′) (ca τ)

_⋉_ = ◇-pair

□◇-pair' : ⟨ □ (◇ A) ⊙ □ (◇ (□ B)) ⟩→̇ □ (◇ (A ×̂ B))
□◇-pair' ca cb τ = ◇-pair (□-mon ca τ) (cb τ)

□◇-pair : Mon B → ⟨ □ (◇ A) ⊙ □ (◇ B) ⟩→̇ □ (◇ (A ×̂ B))
□◇-pair mB ca cb τ = join $
  ◇-map! (λ τ₁ b → ◇-map! (λ τ₂ a → a , mB b τ₂) (ca (⊆-trans τ τ₁))) (cb τ)

◇□-pair' : ⟨ ◇ (□ A) ⊙ □ (◇ (□ B)) ⟩→̇ ◇ (□ (A ×̂ B))
◇□-pair' ca cb = join (◇-map! (λ τ a → ◇-map! (λ τ₁ b τ₂ → a (⊆-trans τ₁ τ₂) , b τ₂) (cb τ)) ca)

◇□-pair : ⟨ □ (◇ (□ A)) ⊙ ◇ (□ B) ⟩→̇ ◇ (□ (A ×̂ B))
◇□-pair ca cb = join (◇-map! (λ τ b → ◇-map! (λ τ₁ a τ₂ → a τ₂ , b (⊆-trans τ₁ τ₂)) (ca τ)) cb)

-- Runnability

Run : (A : Cxt → Set) → Set
Run A = ◇ A →̇ A

-- Negative ISets are runnable

◇-run : Run (◇ A)
◇-run = join

Π-run : (∀ i → Run (F i)) → Run (Π̂ I F)
Π-run f = Π-map f ∘ ◇-record

⇒-run : Mon A → Run B → Run (A ⇒̂ B)
⇒-run mA rB f = rB ∘ ◇-fun mA f

-- Bind for the ◇ monad

◇-elim : Run B → (A →̇ B) → ◇ A →̇ B
◇-elim rB f = rB ∘ ◇-map f

◇-elim! : Run B → ⟨ □ (A ⇒̂ B) ⊙ ◇ A ⟩→̇ B
◇-elim! rB f = rB ∘ ◇-map! f

◇-elim-□ : Run B → ⟨ □ (A ⇒̂ B) ⊙ □ (◇ A) ⟩→̇ □ B
◇-elim-□ rB f c = □-map (uncurry (◇-elim! rB)) (□-pair (□-mon f) c)

◇-elim-□-alt : Run B → ⟨ □ (A ⇒̂ B) ⊙ □ (◇ A) ⟩→̇ □ B
◇-elim-□-alt rB f c τ = ◇-elim! rB (□-mon f τ) (c τ)

bind! : Mon C → Run B → (C →̇ ◇ A) → (C →̇ (A ⇒̂ B)) → C →̇ B
bind! mC rB f k γ = ◇-elim! rB (λ τ a → k (mC γ τ) a) (f γ)

-- Type interpretation
------------------------------------------------------------------------

mutual
  ⟦_⟧⁺ : Ty⁺ → ISet
  ⟦ base o  ⟧⁺ = base o ∈_
  ⟦ P₁ ×̇ P₂ ⟧⁺ = ⟦ P₁ ⟧⁺ ×̂ ⟦ P₂ ⟧⁺
  ⟦ Σ̇ I P   ⟧⁺ = Σ̂ I λ i → ⟦ P i ⟧⁺
  ⟦ □̇ N     ⟧⁺ = □ ⟦ N ⟧⁻

  ⟦_⟧⁻ : Ty⁻ → ISet
  ⟦ ◇̇ P   ⟧⁻ = ◇ ⟦ P ⟧⁺
  ⟦ Π̇ I N ⟧⁻ = Π̂ I λ i → ⟦ N i ⟧⁻
  ⟦ P ⇒̇ N ⟧⁻ = ⟦ P ⟧⁺ ⇒̂ ⟦ N ⟧⁻

⟦_⟧ᶜ : Cxt → ISet
⟦_⟧ᶜ Γ Δ = All (λ P → ⟦ P ⟧⁺ Δ) Γ

-- ⟦ []    ⟧ᶜ = 1̂
-- ⟦ P ∷ Γ ⟧ᶜ = ⟦ Γ ⟧ᶜ ×̂ ⟦ P ⟧⁺

-- Positive types are monotone.

mon⁺ : (P : Ty⁺) → Mon ⟦ P ⟧⁺
mon⁺ (base o)  = monVar
mon⁺ (P₁ ×̇ P₂) = ×-mon (mon⁺ P₁) (mon⁺ P₂)
mon⁺ (Σ̇ I P)   = Σ-mon (mon⁺ ∘ P)
mon⁺ (□̇ N)     = □-mon

monᶜ : (Γ : Cxt) → Mon ⟦ Γ ⟧ᶜ
monᶜ Γ γ τ = All.map (λ {P} v → mon⁺ P v τ) γ

-- Negative types are runnable.

run⁻ : (N : Ty⁻) → Run ⟦ N ⟧⁻
run⁻ (◇̇ P)   = ◇-run
run⁻ (Π̇ I N) = Π-run (run⁻ ∘ N)
run⁻ (P ⇒̇ N) = ⇒-run (mon⁺ P) (run⁻ N)

-- monᶜ []      = 1-mon
-- monᶜ (P ∷ Γ) = ×-mon (monᶜ Γ) (mon⁺ P)

-- Interpretation
------------------------------------------------------------------------

mutual

  ⦅_⦆⁺ : Val P Γ → ⟦ Γ ⟧ᶜ →̇ ⟦ P ⟧⁺
  ⦅ var x ⦆⁺      = λ γ → All.lookup γ x
  ⦅ pair v₁ v₂ ⦆⁺ = < ⦅ v₁ ⦆⁺ , ⦅ v₂ ⦆⁺ >
  ⦅ inj i v ⦆⁺    = (i ,_) ∘ ⦅ v ⦆⁺
  ⦅ thunk t ⦆⁺    = □-intro (monᶜ _) ⦅ t ⦆⁻

  λ⦅_⦆⁻ : Comp N (P ∷ Γ) → ⟦ Γ ⟧ᶜ →̇ ⟦ P ⇒̇ N ⟧⁻
  λ⦅ t ⦆⁻ γ a = ⦅ t ⦆⁻ (a ∷ γ)

  ⦅_⦆⁻ : Comp N Γ → ⟦ Γ ⟧ᶜ →̇ ⟦ N ⟧⁻
  ⦅ ret v ⦆⁻ = return ∘ ⦅ v ⦆⁺
  ⦅ rec t ⦆⁻ = flip λ i → ⦅ t i ⦆⁻
  ⦅ abs t ⦆⁻ = λ⦅ t ⦆⁻
  ⦅ split v t ⦆⁻ γ = let (a₁ , a₂) = ⦅ v ⦆⁺ γ in ⦅ t ⦆⁻ (a₂ ∷ (a₁ ∷ γ))
  ⦅ case v t ⦆⁻  γ = let (i , a) = ⦅ v ⦆⁺ γ in  ⦅ t i ⦆⁻ (a ∷ γ)
  ⦅ bind {Γ = Γ} {N = N} t t₁ ⦆⁻ = bind! (monᶜ Γ) (run⁻ N) ⦅ t ⦆⁻ λ⦅ t₁ ⦆⁻
  ⦅ force v ⦆⁻  = extract ∘ ⦅ v ⦆⁺
  ⦅ prj i t ⦆⁻  = (_$ i) ∘ ⦅ t ⦆⁻
  ⦅ app t v ⦆⁻  = ⦅ t ⦆⁻  ˢ ⦅ v ⦆⁺
  ⦅ letv v t ⦆⁻ = λ⦅ t ⦆⁻ ˢ ⦅ v ⦆⁺

-- Reflection and reification

mutual

  fresh□◇□ : ∀ P {Γ} → ⟨ P ⟩ (□ (◇ (□ ⟦ P ⟧⁺))) Γ
  fresh□◇□ P = reflect⁺□ P ∘ monVar here!

  fresh□ : ∀ P {Γ} → ⟨ P ⟩ (□ (◇ ⟦ P ⟧⁺)) Γ
  fresh□ P = ◇-map extract ∘ reflect⁺□ P ∘ monVar here!
  fresh□ P = reflect⁺ P ∘ monVar here!

  fresh : ∀ {P Γ} → ⟨ P ⟩ (◇ ⟦ P ⟧⁺) Γ
  fresh {P} = ◇-map extract (reflect⁺□ P here!)
  fresh {P} = reflect⁺ P here!

  fresh◇ : ∀ {P Γ} → ⟨ P ⟩ (◇ (□ ⟦ P ⟧⁺)) Γ
  fresh◇ {P} = reflect⁺□ P here!
  fresh◇ {P} = ◇-map (mon⁺ P) fresh

  -- saves us use of Mon P in freshᶜ
  reflect⁺□ : (P : Ty⁺) → (P ∈_) →̇ (◇ (□ ⟦ P ⟧⁺))
  reflect⁺□ (base o)  x = return (monVar x)
  reflect⁺□ (P₁ ×̇ P₂) x = split x (◇□-pair (reflect⁺□ P₁ ∘ monVar (there here!)) fresh◇)
  reflect⁺□ (Σ̇ I Ps)  x = case x λ i → ◇-map (□-map (i ,_)) fresh◇
  reflect⁺□ (□̇ N)     x = return (□-mon (reflect⁻ N ∘ force ∘ monVar x))

  reflect⁺ : (P : Ty⁺) → (P ∈_) →̇ (◇ ⟦ P ⟧⁺)
  reflect⁺ (base o)  x = return x
  reflect⁺ (P₁ ×̇ P₂) x = split x (□-weak (fresh□ P₁) ⋉ fresh◇)
  reflect⁺ (Σ̇ I Ps)  x = case x λ i → ◇-map (i ,_) fresh
  reflect⁺ (□̇ N)     x = return λ τ → reflect⁻ N (force (monVar x τ))

  reflect⁻ : (N : Ty⁻) → Ne N →̇ ⟦ N ⟧⁻
  reflect⁻ (◇̇ P)    u = bind u fresh
  reflect⁻ (Π̇ I Ns) u = λ i → reflect⁻ (Ns i) (prj i u)
  reflect⁻ (P ⇒̇ N)  u = λ a → reflect⁻ N (app u (reify⁺ P a))

  reify⁺ : (P : Ty⁺) → ⟦ P ⟧⁺ →̇ NVal P
  reify⁺ (base o) = var
  reify⁺ (P₁ ×̇ P₂) (a₁ , a₂) = pair (reify⁺ P₁ a₁) (reify⁺ P₂ a₂)
  reify⁺ (Σ̇ I Ps)  (i  , a ) = inj i (reify⁺ (Ps i) a)
  reify⁺ (□̇ N) a = thunk (reify⁻ N a)

  reify⁻ : (N : Ty⁻) → □ ⟦ N ⟧⁻ →̇ Nf N
  reify⁻ (◇̇ P)    f = ret (◇-map (reify⁺ P) (extract f))
  reify⁻ (Π̇ I Ns) f = rec λ i → reify⁻ (Ns i) (□-map (_$ i) f)
  reify⁻ (P ⇒̇ N)  f = abs $ reify⁻ N $ ◇-elim-□ (run⁻ N) (□-weak f) $ fresh□ P

ext : (⟦ Γ ⟧ᶜ ×̂ ⟦ P ⟧⁺) →̇ ⟦ P ∷ Γ ⟧ᶜ
ext (γ , a) = a ∷ γ

◇-ext : ◇ (⟦ Γ ⟧ᶜ ×̂ ⟦ P ⟧⁺) →̇ ◇ ⟦ P ∷ Γ ⟧ᶜ
◇-ext = ◇-map ext

-- Without the use of ◇-mon!

freshᶜ : (Γ : Cxt) → □ (◇ ⟦ Γ ⟧ᶜ) Γ
freshᶜ []      = λ τ → return []
freshᶜ (P ∷ Γ) = ◇-ext ∘ □◇-pair' (□-weak (freshᶜ Γ)) (fresh□◇□ P)
freshᶜ (P ∷ Γ) = ◇-ext ∘ □◇-pair (mon⁺ P) (□-weak (freshᶜ Γ)) (fresh□ P)
freshᶜ (P ∷ Γ) = ◇-ext ∘ □◇-pair' (□-weak (freshᶜ Γ)) (◇-map (mon⁺ P) ∘ (fresh□ P))
freshᶜ (P ∷ Γ) = ◇-ext ∘ λ τ →
  (□-weak (□-mon (freshᶜ Γ)) τ)
  ⋉ ◇-map (mon⁺ P) (fresh□ P τ)

norm : Comp N →̇ Nf N
norm {N = N} {Γ = Γ} t = reify⁻ N $ □-map (run⁻ N ∘ ◇-map ⦅ t ⦆⁻) $ freshᶜ Γ
norm {N = N} {Γ = Γ} t = reify⁻ N $ run⁻ N ∘ ◇-map ⦅ t ⦆⁻ ∘ freshᶜ Γ

-- -}
-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


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

module Generics.Constructions.DecEq where

open import Generics.Prelude hiding (lookup; _≟_)
open import Generics.Telescope
open import Generics.Desc
open import Generics.All
open import Generics.HasDesc

import Generics.Helpers as Helpers

import Data.Fin.Properties as Fin
import Data.Product.Properties as Product

open import Relation.Nullary.Decidable as Decidable
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary using (DecidableEquality)
open import Relation.Nullary.Product

record DecEq {l} (A : Set l) : Set l where
  field _≟_ : DecidableEquality A

open DecEq ⦃...⦄ public

module _ {P I ℓ}
         {A : Indexed P I ℓ}
         (H : HasDesc {P} {I} {ℓ} A) where

  data HigherOrderArgumentsNotSupported : Set where

  -- Predicate preventing the use of Higher-order inductive arguments
  OnlyFO : ∀ {V} → ConDesc P V I → Setω
  OnlyFO (var _) = Liftω ⊤
  OnlyFO (π _ _ _) = Liftω HigherOrderArgumentsNotSupported
  OnlyFO (A ⊗ B) = OnlyFO A ×ω OnlyFO B

  open HasDesc H
  open Helpers P I DecEq (const ⊤) OnlyFO

  DecEqHelpers : ∀ p → Setω
  DecEqHelpers p = Helpers p D

  private irr≡ : ∀ {l} (A : Set l) (x y : Irr A) → x ≡ y
          irr≡ A (irrv _) (irrv _) = refl

  private module _ {p} (DH : DecEqHelpers p) where

    variable
      V : ExTele P
      v : ⟦ V ⟧tel p
      i : ⟦ I ⟧tel p

    mutual
      decEqIndArg-wf : ∀ (C : ConDesc P V I) → OnlyFO C
                     → (x y : ⟦ C ⟧IndArg A′ (p , v))
                     → AllIndArgω Acc C x
                     → AllIndArgω Acc C y
                     → Dec (x ≡ y)

      decEqIndArg-wf (var i) H x y ax ay = decEq-wf x y ax ay
      decEqIndArg-wf (A ⊗ B) (HA , HB) (xa , xb) (ya , yb) (axa , axb) (aya , ayb)
        = map′ (λ (p , q) → cong₂ _,_ p q)
            (λ p → cong proj₁ p , cong proj₂ p)
            (decEqIndArg-wf _ HA xa ya axa aya ×-dec decEqIndArg-wf _ HB xb yb axb ayb)
      decEqIndArg-wf (π i S C) ()

      decEqCon-wf : (C   : ConDesc P V I)
                    ⦃ H  : ConHelper p C ⦄
                    (x y : ⟦ C ⟧Con A′ (p , v , i))
                  → AllConω Acc C x
                  → AllConω Acc C y
                  → Dec (x ≡ y)
      decEqCon-wf ._ ⦃ var ⦄ refl refl _ _ = yes refl
      decEqCon-wf ._ ⦃ pi-irr ⦃ _ ⦄ ⦃ H ⦄ ⦄ (irrv _ , x) (irrv _ , y) ax ay
        with decEqCon-wf _ ⦃ H ⦄ x y ax ay
      ... | yes refl = yes refl
      ... | no p     = no (p ∘ λ {refl → refl})
      decEqCon-wf ._ ⦃ pi-rel ⦃ dec ⦄ ⦃ H ⦄ ⦄ (s₁ , x) (s₂ , y) ax ay
        with dec .DecEq._≟_ s₁ s₂
      ... | no p     = no (p ∘ (λ { refl → refl }))
      ... | yes refl with decEqCon-wf _ ⦃ H ⦄ x y ax ay
      ... | yes refl = yes refl
      ... | no  p    = no (p ∘ (λ { refl → refl }))
      decEqCon-wf ._ ⦃ prod ⦃ HA ⦄ ⦄ (xa , xb) (ya , yb) (axa , axb) (aya , ayb) =
        map′ (λ (p , q) → cong₂ _,_ p q)
             (λ p → cong proj₁ p , cong proj₂ p)
             (decEqIndArg-wf _ HA xa ya axa aya ×-dec decEqCon-wf _ xb yb axb ayb)

      decEqData-wf : (x y : ⟦ D ⟧Data A′ (p , i))
                   → AllDataω Acc D x
                   → AllDataω Acc D y
                   → Decω (x ≡ω y)
      decEqData-wf (k₁ , x) (k₂ , y) ax ay with k₁ Fin.≟ k₂
      decEqData-wf (k  , x) (k  , y) ax ay | yes refl with decEqCon-wf _ ⦃ lookupHelper DH k ⦄ x y ax ay
      decEqData-wf (k  , x) (k  , y) ax ay | yes refl | yes refl = yesω refl
      decEqData-wf (k  , x) (k  , y) ax ay | yes refl | no x≢y   = noω λ { refl → x≢y refl }
      decEqData-wf (k₁ , x) (k₂ , y) ax ay | no k₁≢k₂ =
        noω λ { refl → k₁≢k₂ refl }

      decEq-wf : (x y : A′ (p , i)) → Acc x → Acc y → Dec (x ≡ y)
      decEq-wf x y (acc ax) (acc ay) with decEqData-wf (split x) (split y) ax ay
      ... | yesω p = yes (split-injective p)
      ... | noω  p = no  (λ e → p (cong≡ω split e))

  deriveDecEq : ∀ {p} ⦃ DH : DecEqHelpers p ⦄ {i} → DecEq (A′ (p , i))
  deriveDecEq ⦃ DH ⦄ .DecEq._≟_ x y
    = decEq-wf DH x y (wf x) (wf y)

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
{-# OPTIONS -v tc.size:100 #-}
-- {-# OPTIONS -v tc.meta:100 #-}

open import Common.Size using (Size; Size<_)

postulate
  A : Set

record R (i₀ : Size) (x : A) : Set where
  coinductive
  field
    force : (j : Size< i₀) → R j x

postulate
  P : (A → Set) → Set
  f : (Q : A → Set) (x : A) {{ c : P Q }} → Q x → Q x
  g : (i₁ : Size) (x : A) → R i₁ x → R i₁ x

  instance
    c : {i₂ : Size} → P (R i₂)

accepted rejected : A → (x : A) (i₃ : Size) → R i₃ x → R i₃ x

accepted y x i r = g _ _ (f _ _ r)

rejected y x i r = g _ _ (f _ x r)


text:
-- Andreas, AIM XVIII, 2013-09-13
module ProjectionsTakeModuleTelAsParameters where

import Common.Level
open import Common.Equality

module M (A : Set) where

  record Prod (B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B
  open Prod public

open M -- underapplied open

-- module parameters are hidden in projections

myfst : {A B : Set} → Prod A B → A
myfst = fst

mysnd : {A B : Set} → Prod A B → B
mysnd p = snd p


text:
open import Relation.Binary.Core

module BBHeap.Heapify {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_
open import BBHeap.Insert _≤_ tot≤ trans≤
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List

heapify : List A → BBHeap bot
heapify [] = leaf
heapify (x ∷ xs) = insert {x = x} lebx (heapify xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- {-# OPTIONS -v tc.pos:10 #-}
-- Andreas, 2014-07-04

record R (A : Set) : Set where
  field f : R A

-- Should complain about missing 'inductive' or 'coinductive'.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.IntMod where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Monoid.Base
open import Cubical.Algebra.Semigroup.Base
open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.Bool
open import Cubical.Data.Fin
open import Cubical.Data.Fin.Arithmetic
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Algebra.Group.Instances.Unit
  renaming (Unit to UnitGroup)
open import Cubical.Algebra.Group.Instances.Bool
  renaming (Bool to BoolGroup)
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

open GroupStr
open IsGroup
open IsMonoid

ℤ/_ : ℕ → Group₀
ℤ/ zero = UnitGroup
fst (ℤ/ suc n) = Fin (suc n)
1g (snd (ℤ/ suc n)) = 0
GroupStr._·_ (snd (ℤ/ suc n)) = _+ₘ_
inv (snd (ℤ/ suc n)) = -ₘ_
IsSemigroup.is-set (isSemigroup (isMonoid (isGroup (snd (ℤ/ suc n))))) =
  isSetFin
IsSemigroup.assoc (isSemigroup (isMonoid (isGroup (snd (ℤ/ suc n))))) =
  λ x y z → sym (+ₘ-assoc x y z)
fst (identity (isMonoid (isGroup (snd (ℤ/ suc n)))) x) = +ₘ-rUnit x
snd (identity (isMonoid (isGroup (snd (ℤ/ suc n)))) x) = +ₘ-lUnit x
fst (inverse (isGroup (snd (ℤ/ suc n))) x) = +ₘ-rCancel x
snd (inverse (isGroup (snd (ℤ/ suc n))) x) = +ₘ-lCancel x

ℤ/1≅Unit : GroupIso (ℤ/ 1) UnitGroup
ℤ/1≅Unit = contrGroupIsoUnit isContrFin1

Bool≅ℤ/2 : GroupIso BoolGroup (ℤ/ 2)
Iso.fun (fst Bool≅ℤ/2) false = 1
Iso.fun (fst Bool≅ℤ/2) true = 0
Iso.inv (fst Bool≅ℤ/2) (zero , p) = true
Iso.inv (fst Bool≅ℤ/2) (suc zero , p) = false
Iso.inv (fst Bool≅ℤ/2) (suc (suc x) , p) =
  ⊥-rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p)))
Iso.rightInv (fst Bool≅ℤ/2) (zero , p) =
  Σ≡Prop (λ _ → m≤n-isProp) refl
Iso.rightInv (fst Bool≅ℤ/2) (suc zero , p) =
  Σ≡Prop (λ _ → m≤n-isProp) refl
Iso.rightInv (fst Bool≅ℤ/2) (suc (suc x) , p) =
  ⊥-rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p)))
Iso.leftInv (fst Bool≅ℤ/2) false = refl
Iso.leftInv (fst Bool≅ℤ/2) true = refl
snd Bool≅ℤ/2 =
  makeIsGroupHom λ { false false → refl
                   ; false true → refl
                   ; true false → refl
                   ; true true → refl}

ℤ/2≅Bool : GroupIso (ℤ/ 2) BoolGroup
ℤ/2≅Bool = invGroupIso Bool≅ℤ/2

max_stars_repo_name: FernandoLarrain/cubical

max_issues_repo_name: FernandoLarrain/cubical

max_forks_repo_name: FernandoLarrain/cubical


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module Mergesort.Impl1.Correctness.Permutation {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List
open import Data.Product
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A
open import List.Permutation.Pair A
open import List.Permutation.Pair.Properties A
open import Mergesort.Impl1 _≤_ tot≤
open import Size
open import SList
open import SList.Properties
open import SOList.Lower _≤_

lemma-deal : {ι : Size} → (xs : SList A {ι}) → unsize A xs ≈ unsize× A (deal xs)
lemma-deal snil = ≈[]l []
lemma-deal (x ∙ snil) = ≈[]r (x ∷ [])
lemma-deal (x ∙ (y ∙ xs))
    with lemma-deal xs
... | xs≈ys,zs = ≈xl (≈xr xs≈ys,zs)

lemma-merge : {ι ι' : Size}{b : Bound}(xs : SOList {ι} b)(ys : SOList {ι'} b) → forget (merge xs ys) ≈ (forget xs , forget ys)
lemma-merge onil ys = ≈[]l (forget ys)
lemma-merge xs onil
    with xs
... | onil = ≈[]r []
... | (:< {x = z} b≤z zs) = ≈[]r (z ∷ forget zs)
lemma-merge (:< {x = x} b≤x xs)  (:< {x = y} b≤y ys)
    with tot≤ x y
... | inj₁ x≤y = ≈xl (lemma-merge xs (:< (lexy x≤y) ys))
... | inj₂ y≤x = ≈xr (lemma-merge (:< (lexy y≤x) xs) ys)

lemma-mergesort : {ι : Size}(xs : SList A {↑ ι}) → unsize A xs ∼ forget (mergesort xs)
lemma-mergesort snil = ∼[]
lemma-mergesort (x ∙ snil) = ∼x /head /head ∼[]
lemma-mergesort (x ∙ (y ∙ xs)) = lemma≈ (≈xl (≈xr (lemma-deal xs))) (lemma-mergesort (x ∙ ys)) (lemma-mergesort (y ∙ zs)) (lemma-merge (mergesort (x ∙ ys)) (mergesort (y ∙ zs)))
                where d = deal xs
                      ys = proj₁ d
                      zs = proj₂ d

theorem-mergesort-∼ : (xs : List A) → xs ∼ (forget (mergesort (size A xs)))
theorem-mergesort-∼ xs = trans∼ (lemma-unsize-size A xs) (lemma-mergesort (size A xs))


text:
{-# OPTIONS --sized-types #-}
module SNat.Sum where

open import Relation.Binary.PropositionalEquality
open import Size
open import SNat

+-assoc-succ : (m n : SNat) → m + succ n ≡ succ (m + n)
+-assoc-succ zero n = refl
+-assoc-succ (succ m) n rewrite +-assoc-succ m n = refl

+-assoc-right : (a b c : SNat) → (a + b) + c ≡ a + (b + c)
+-assoc-right zero b c = refl
+-assoc-right (succ n) b c rewrite +-assoc-right n b c = refl

+-assoc-left : (a b c : SNat) → a + (b + c) ≡ (a + b) + c
+-assoc-left zero b c = refl
+-assoc-left (succ n) b c rewrite +-assoc-left  n b c = refl

+-id : (n : SNat) → n + zero ≡ n
+-id zero = refl
+-id (succ n) rewrite +-id n = refl

+-comm : (m n : SNat) → m + n ≡ n + m
+-comm zero n rewrite +-id n = refl
+-comm (succ m) n rewrite +-assoc-succ n m | +-comm m n = refl


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

module Data.Nat.WellFounded where

open import Prelude
open import Data.Nat
open import WellFounded

infix 4 _≤_ _<_
data _≤_ (n : ℕ) : ℕ → Type where
  n≤n : n ≤ n
  n≤s : ∀ {m} → n ≤ m → n ≤ suc m

_<_ : ℕ → ℕ → Type
n < m = suc n ≤ m

≤-wellFounded : WellFounded _<_
≤-wellFounded x = acc (go x)
  where
  go : ∀ n m → m < n → Acc _<_ m
  go (suc n) .n n≤n = acc (go n)
  go (suc n) m (n≤s m<n) = go n m m<n

open import Data.Nat.DivMod
open import Agda.Builtin.Nat using (div-helper)
import Data.Nat.Properties as ℕ

-- Bear in mind the following two functions will not compute
-- as currently subst (with --cubical) doesn't work on GADTs.
--
-- We could write the functions without using subst.
div2≤ : ∀ n → n ÷ 2 ≤ n
div2≤ n = subst (n ÷ 2 ≤_) (ℕ.+-idʳ n) (go zero n)
  where
  go : ∀ k n → div-helper k 1 n 1 ≤ n + k
  go k zero = n≤n
  go k (suc zero) = n≤s n≤n
  go k (suc (suc n)) = n≤s (subst (div-helper (suc k) 1 n 1 ≤_) (ℕ.+-suc n k) (go (suc k) n))

s≤s : ∀ {n m} → n ≤ m → suc n ≤ suc m
s≤s n≤n = n≤n
s≤s (n≤s x) = n≤s (s≤s x)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------------
-- Exclusive disjunction theorems
------------------------------------------------------------------------------

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

module FOL.ExclusiveDisjunction.TheoremsATP where

-- The theorems below are valid on intuitionistic logic and with an
-- empty domain.
open import FOL.Base hiding ( D≢∅ ; pem )
open import FOL.ExclusiveDisjunction.Base

------------------------------------------------------------------------------
-- We postulate some propositional formulae (which are translated as
-- 0-ary predicates).
postulate P Q : Set

-- We do not use the _⊻_ operator because its definition is not a
-- FOL-definition.

postulate
  p⊻q→p→¬q : ((P ∨ Q) ∧ ¬ (P ∧ Q)) → P → ¬ Q
{-# ATP prove p⊻q→p→¬q #-}

postulate
  p⊻q→q→¬p : ((P ∨ Q) ∧ ¬ (P ∧ Q)) → Q → ¬ P
{-# ATP prove p⊻q→q→¬p #-}

postulate
  p⊻q→¬p→q : ((P ∨ Q) ∧ ¬ (P ∧ Q)) → ¬ P → Q
{-# ATP prove p⊻q→¬p→q #-}

postulate
  p⊻q→¬q→p : ((P ∨ Q) ∧ ¬ (P ∧ Q)) → ¬ Q → P
{-# ATP prove p⊻q→¬q→p #-}

postulate
  ¬[p⊻q] : ¬ ((P ∨ Q) ∧ ¬ (P ∧ Q)) → ((P ∧ Q) ∨ (¬ P ∧ ¬ Q))
{-# ATP prove ¬[p⊻q] #-}


text:
-- Andreas, 2013-05-02 This ain't a bug, it is a feature.
-- {-# OPTIONS -v scope.name:10 #-}
module _ where

open import Common.Equality

module M where

  record R' : Set₁ where
    field
      X : Set

open M renaming (R' to R)

X : R → Set
X = R.X

-- Nisse:
-- The open directive did not mention the /module/ R, so (I think
-- that) the code above should be rejected.

-- Andreas:
-- NO, it is a feature that projections can also be accessed via
-- the record /type/.

-- Ulf:
-- According to the suggestion in 836, if you rename the module explicitly
-- the code above breaks (test/fail/Issue836.agda).


text:
module Generic.Reflection.DeriveEq where

open import Generic.Core
open import Generic.Function.FoldMono
open import Generic.Reflection.ReadData

fromToClausesOf : Data Type -> Name -> List Clause
fromToClausesOf (packData d a b cs ns) f = unmap (λ {a} -> clauseOf a) ns where
  vars : ℕ -> ℕ -> Type -> List (Maybe (String × ℕ) × ℕ)
  vars (suc i) j (explPi r s a b) = if isSomeName d a
    then (just (s , j) , i) ∷ vars i (suc j) b
    else (nothing      , i) ∷ vars i  j      b
  vars  i      j (pi       s a b) = vars i j b
  vars  i      j  b               = []

  clauseOf : Type -> Name -> Clause
  clauseOf c n = clause lhs rhs where
    es   = explPisToNames c
    i    = length es
    mxs  = vars i 0 c
    xs   = mapMaybe proj₁ mxs
    k    = length xs
    lhs  = explRelArg (patCon n (patVars es)) ∷ []
    lams = λ t -> foldr (explLam ∘ proj₁) t xs
    each = λ m i -> maybe (proj₂ >>> λ j -> pureVar (k ∸ suc j)) (pureVar (i + k)) m
    args = map (uncurry each) mxs
    grow = lams (vis appCon n args)
    rs   = mapMaybe (uncurry λ m i -> vis# 1 appDef f (pureVar i) <$ m) mxs
    rhs  = vis appDef (quote congn) $ reify k ∷ grow ∷ rs

toTypeOf : Data Type -> Name -> Type
toTypeOf (packData d a b cs ns) d′ = let ab = appendType a b; k = countPis ab in
  appendType (implicitize ab) $ appDef d (pisToArgVars k ab) ‵→ appDef d′ (pisToArgVars (suc k) ab)

fromTypeOf : Data Type -> Name -> Type
fromTypeOf (packData d a b cs ns) d′ = let ab = appendType a b; k  = countPis ab in
  appendType (implicitize ab) $ appDef d′ (pisToArgVars k ab) ‵→ appDef d (pisToArgVars (suc k) ab)

fromToTypeOf : Data Type -> Name -> Name -> Name -> Type
fromToTypeOf (packData d a b cs ns) d′ to from = let ab = appendType a b; k = countPis ab in
  appendType (implicitize ab) ∘ pi "x" (explRelArg (appDef d (pisToArgVars k ab))) $
    sate _≡_ (vis# 1 appDef from (vis# 1 appDef to (pureVar 0))) (pureVar 0)

injTypeOf : Data Type -> Name -> Type
injTypeOf (packData d a b cs ns) d′ =
  let ab  = appendType a b
      k   = countPis ab
      avs = pisToArgVars k ab
  in appendType (implicitize ab) $ sate _↦_ (appDef d avs) (appDef d′ avs)

deriveDesc : Name -> Data Type -> TC Name
deriveDesc d D =
  freshName (showName d ++ˢ "′") >>= λ d′ ->
  getType d >>= λ a ->
  declareDef (explRelArg d′) a >>
  d′ <$ (quoteData D >>= defineTerm d′)

deriveTo : Data Type -> Name -> Name -> TC Name
deriveTo D d′ fd =
  freshName ("to" ++ˢ showName d′) >>= λ to ->
  declareDef (explRelArg to) (toTypeOf D d′) >>
  to <$ defineTerm to (sateMacro gcoerce (pureDef fd))

deriveFrom : Data Type -> Name -> TC Name
deriveFrom D d′ =
  freshName ("from" ++ˢ showName d′) >>= λ from ->
  declareDef (explRelArg from) (fromTypeOf D d′) >>
  from <$ defineTerm from (guncoercePure D)

deriveFromTo : Data Type -> Name -> Name -> Name -> TC Name
deriveFromTo D d′ to from =
  freshName ("fromTo" ++ˢ showName d′) >>= λ from-to ->
  declareDef (explRelArg from-to) (fromToTypeOf D d′ to from) >>
  from-to <$ defineFun from-to (fromToClausesOf D from-to)

deriveInj : Data Type -> Name -> Name -> Name -> Name -> TC Name
deriveInj D d′ to from from-to =
  freshName ("inj" ++ˢ showName d′) >>= λ inj ->
  declareDef (explRelArg inj) (injTypeOf D d′) >>
  inj <$ defineTerm inj (sate packInj (pureDef to) (pureDef from) (pureDef from-to))

deriveEqTo : Name -> Name -> TC _
deriveEqTo e d =
  getData d >>= λ D ->
  deriveDesc d D >>= λ d′ ->
  deriveFold d D >>= λ f ->
  deriveTo D d′ f >>= λ to ->
  deriveFrom D d′ >>= λ from ->
  deriveFromTo D d′ to from >>= λ from-to ->
  deriveInj D d′ to from from-to >>= λ inj ->
  defineTerm e (sate viaInj (pureDef inj))

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
------------------------------------------------------------------------
-- M-types for indexed containers, defined using functions
------------------------------------------------------------------------

-- Based on "Non-wellfounded trees in Homotopy Type Theory" by Ahrens,
-- Capriotti and Spadotti.

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

open import Equality

module Container.Indexed.M.Function
  {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 Bijection using (_↔_)
open import Container.Indexed eq
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq as F hiding (id; _∘_)
open import H-level eq as H-level using (H-level)
open import H-level.Closure eq
import Nat eq as Nat
open import Surjection eq using (_↠_)
open import Tactic.Sigma-cong eq
open import Univalence-axiom eq

private
  variable
    a ℓ o p s             : Level
    A I O                 : Type a
    b ext ext₁ ext₂ i k x : A
    Q                     : A → Type p
    C                     : Container I s p
    n                     : ℕ

------------------------------------------------------------------------
-- Chains

-- Chains (indexed).

Chain : Type i → ∀ ℓ → Type (i ⊔ lsuc ℓ)
Chain {i = i} I ℓ =
  ∃ λ (P : ℕ → I → Type ℓ) → ∀ n → P (suc n) ⇾ P n

-- Limits of chains.

Limit : {I : Type i} → Chain I ℓ → I → Type ℓ
Limit (P , down) i =
  ∃ λ (f : ∀ n → P n i) →
    ∀ n → down n i (f (suc n)) ≡ f n

-- A kind of dependent universal property for limits.

universal-property-Π :
  {A : Type a} {I : Type i} {g : A → I} →
  (X@(P , down) : Chain I ℓ) →

  ((a : A) → Limit X (g a))
    ≃
  (∃ λ (f : ∀ n (a : A) → P n (g a)) →
     ∀ n a → down n (g a) (f (suc n) a) ≡ f n a)

universal-property-Π {g = g} X@(P , down) =
  (∀ a → Limit X (g a))                           ↔⟨⟩

  (∀ a → ∃ λ (f : ∀ n → P n (g a)) →
           ∀ n → down n (g a) (f (suc n)) ≡ f n)  ↔⟨ ΠΣ-comm ⟩

  (∃ λ (f : ∀ a n → P n (g a)) →
     ∀ a n → down n (g a) (f a (suc n)) ≡ f a n)  ↝⟨ Σ-cong-refl Π-comm (λ _ → Π-comm) ⟩□

  (∃ λ (f : ∀ n a → P n (g a)) →
     ∀ n a → down n (g a) (f (suc n) a) ≡ f n a)  □

-- A universal property for limits.

universal-property :
  {I : Type i} {P : I → Type p} →
  (X@(Q , down) : Chain I ℓ) →

  (P ⇾ Limit X)
    ↝[ i ∣ p ⊔ ℓ ]
  (∃ λ (f : ∀ n → P ⇾ Q n) →
     ∀ n i x → down n i (f (suc n) i x) ≡ f n i x)

universal-property {P = P} X@(Q , down) ext =
  (P ⇾ Limit X)                                     ↔⟨⟩

  (∀ i → P i → Limit X i)                           ↝⟨ (∀-cong ext λ _ → from-equivalence $ universal-property-Π X) ⟩

  (∀ i → ∃ λ (f : ∀ n → P i → Q n i) →
           ∀ n x → down n i (f (suc n) x) ≡ f n x)  ↔⟨ ΠΣ-comm ⟩

  (∃ λ (f : ∀ i n → P i → Q n i) →
     ∀ i n x → down n i (f i (suc n) x) ≡ f i n x)  ↝⟨ Σ-cong-refl Π-comm (λ _ → Π-comm) ⟩

  (∃ λ (f : ∀ n i → P i → Q n i) →
     ∀ n i x → down n i (f (suc n) i x) ≡ f n i x)  ↔⟨⟩

  (∃ λ (f : ∀ n → P ⇾ Q n) →
     ∀ n i x → down n i (f (suc n) i x) ≡ f n i x)  □

-- Cones.

Cone : {I : Type i} → (I → Type p) → Chain I ℓ → Type (i ⊔ p ⊔ ℓ)
Cone P (Q , down) =
  ∃ λ (f : ∀ n → P ⇾ Q n) →
    ∀ n → down n ∘⇾ f (suc n) ≡ f n

-- A variant of the non-dependent universal property.

universal-property-≃ :
  {I : Type i} {P : I → Type p} →
  Extensionality (i ⊔ p) (i ⊔ p ⊔ ℓ) →
  (X : Chain I ℓ) →

  (P ⇾ Limit X) ≃ Cone P X

universal-property-≃ {i = i} {p = p} {ℓ = ℓ} {P = P} ext X@(Q , down) =
  P ⇾ Limit X                                       ↝⟨ universal-property X (lower-extensionality p i ext) ⟩

  (∃ λ (f : ∀ n → P ⇾ Q n) →
     ∀ n i x → down n i (f (suc n) i x) ≡ f n i x)  ↝⟨ (∃-cong λ _ → ∀-cong (lower-extensionality _ lzero ext) λ _ →
                                                        ∀-cong (lower-extensionality p i ext) λ _ →
                                                        Eq.extensionality-isomorphism (lower-extensionality (i ⊔ p) (i ⊔ p) ext)) ⟩
  (∃ λ (f : ∀ n → P ⇾ Q n) →
     ∀ n i → down n i ∘ f (suc n) i ≡ f n i)        ↝⟨ (∃-cong λ _ → ∀-cong (lower-extensionality _ lzero ext) λ _ →
                                                        Eq.extensionality-isomorphism (lower-extensionality (i ⊔ p) (i ⊔ p) ext)) ⟩
  (∃ λ (f : ∀ n → P ⇾ Q n) →
     ∀ n → down n ∘⇾ f (suc n) ≡ f n)               ↔⟨⟩

  Cone P X                                          □

-- Shifts a chain one step.

shift : Chain I ℓ → Chain I ℓ
shift = Σ-map (_∘ suc) (_∘ suc)

-- Shifting does not affect the limit (assuming extensionality).
--
-- This is a variant of Lemma 12 in "Non-wellfounded trees in Homotopy
-- Type Theory".

Limit-shift :
  ∀ (X : Chain I ℓ) {i} →
  Limit (shift X) i ↝[ lzero ∣ ℓ ] Limit X i
Limit-shift {ℓ = ℓ} X@(P , down) {i = i} ext =
  Limit (shift X) i                                ↔⟨⟩

  (∃ λ (p : ∀ n → P (suc n) i) →
     ∀ n → down (suc n) i (p (suc n)) ≡ p n)       ↔⟨ (∃-cong λ _ → inverse $
                                                       drop-⊤-left-× λ _ →
                                                       _⇔_.to contractible⇔↔⊤ $
                                                       other-singleton-contractible _) ⟩
  (∃ λ (p : ∀ n → P (suc n) i) →
     (∃ λ (p₀ : P 0 i) → down 0 i (p 0) ≡ p₀) ×
     ∀ n → down (suc n) i (p (suc n)) ≡ p n)       ↔⟨ Σ-assoc F.∘
                                                      ∃-comm F.∘
                                                      (∃-cong λ _ → inverse Σ-assoc) ⟩
  (∃ λ ((p₀ , p) : P 0 i × (∀ n → P (suc n) i)) →
     down 0 i (p 0) ≡ p₀ ×
     ∀ n → down (suc n) i (p (suc n)) ≡ p n)       ↝⟨ inverse-ext?
                                                        (generalise-ext?
                                                           (_↠_.logical-equivalence lemma₂-↠)
                                                           (λ ext →
                                                                _↠_.right-inverse-of lemma₂-↠
                                                              , _↔_.left-inverse-of (lemma₂-↔ ext)))
                                                        ext ⟩
  (∃ λ (p : ∀ n → P n i) →
     ∀ n → down n i (p (suc n)) ≡ p n)             ↔⟨⟩

  Limit X i                                        □
  where
  lemma₁-↠ :
    {P : ℕ → Type ℓ} →
    (∀ n → P n) ↠ (P 0 × (∀ n → P (suc n)))
  lemma₁-↠ ._↠_.logical-equivalence ._⇔_.to   = λ p → p 0 , p ∘ suc
  lemma₁-↠ ._↠_.logical-equivalence ._⇔_.from = uncurry ℕ-case
  lemma₁-↠ ._↠_.right-inverse-of              = refl

  lemma₁-↔ :
    {P : ℕ → Type ℓ} →
    Extensionality lzero ℓ →
    (∀ n → P n) ↔ (P 0 × (∀ n → P (suc n)))
  lemma₁-↔ _   ._↔_.surjection      = lemma₁-↠
  lemma₁-↔ ext ._↔_.left-inverse-of = λ f →
    apply-ext ext $ ℕ-case (refl _) λ _ → refl _

  lemma₂-↠ : _ ↠ _
  lemma₂-↠ =
    (∃ λ (p : ∀ n → P n i) →
       ∀ n → down n i (p (suc n)) ≡ p n)              ↝⟨ (∃-cong λ _ → lemma₁-↠) ⟩

    (∃ λ (p : ∀ n → P n i) →
       down 0 i (p 1) ≡ p 0 ×
       ∀ n → down (suc n) i (p (2 + n)) ≡ p (1 + n))  ↝⟨ Σ-cong-id-↠ lemma₁-↠ ⟩□

    (∃ λ ((p₀ , p) : P 0 i × (∀ n → P (suc n) i)) →
       down 0 i (p 0) ≡ p₀ ×
       ∀ n → down (suc n) i (p (suc n)) ≡ p n)        □

  lemma₂-↔ : Extensionality lzero ℓ → _ ↔ _
  lemma₂-↔ ext =
    (∃ λ (p : ∀ n → P n i) →
       ∀ n → down n i (p (suc n)) ≡ p n)              ↝⟨ (∃-cong λ _ → lemma₁-↔ ext) ⟩

    (∃ λ (p : ∀ n → P n i) →
       down 0 i (p 1) ≡ p 0 ×
       ∀ n → down (suc n) i (p (2 + n)) ≡ p (1 + n))  ↝⟨ Σ-cong-id (Eq.↔⇒≃ $ lemma₁-↔ ext) ⟩□

    (∃ λ ((p₀ , p) : P 0 i × (∀ n → P (suc n) i)) →
       down 0 i (p 0) ≡ p₀ ×
       ∀ n → down (suc n) i (p (suc n)) ≡ p n)        □

------------------------------------------------------------------------
-- Cochains

-- Cochains (non-indexed).

Cochain : ∀ ℓ → Type (lsuc ℓ)
Cochain ℓ =
  ∃ λ (P : ℕ → Type ℓ) → ∀ n → P n → P (suc n)

-- There is a pointwise split surjection from the "limit" of a cochain
-- to the first element.

cochain-limit-↠ :
  ((P , up) : Cochain ℓ) →

  (∃ λ (p : ∀ n → P n) → ∀ n → p (suc n) ≡ up n (p n))
    ↠
  P 0
cochain-limit-↠ (_ , up) = λ where
  ._↠_.logical-equivalence ._⇔_.to   (p , _)     → p 0
  ._↠_.logical-equivalence ._⇔_.from p₀ .proj₁   → ℕ-rec p₀ up
  ._↠_.logical-equivalence ._⇔_.from p₀ .proj₂ _ → refl _
  ._↠_.right-inverse-of                          → refl

-- The "limit" of a cochain is pointwise equivalent to the first
-- element (assuming extensionality).
--
-- This is a variant of Lemma 11 in "Non-wellfounded trees in Homotopy
-- Type Theory".

cochain-limit :
  ((P , up) : Cochain ℓ) →

  (∃ λ (p : ∀ n → P n) → ∀ n → p (suc n) ≡ up n (p n))
    ↝[ lzero ∣ ℓ ]
  P 0
cochain-limit X@(_ , up) ext =
  generalise-ext?
  (_↠_.logical-equivalence cl)
  (λ ext → _↠_.right-inverse-of cl , from∘to ext)
  ext
  where
  cl = cochain-limit-↠ X

  open _↠_ cl

  from₁∘to : ∀ l n → proj₁ (from (to l)) n ≡ proj₁ l n
  from₁∘to _         zero    = refl _
  from₁∘to l@(p , q) (suc n) =
    up n (proj₁ (from (to l)) n)  ≡⟨ cong (up n) $ from₁∘to l n ⟩
    up n (p n)                    ≡⟨ sym $ q n ⟩∎
    p (suc n)                     ∎

  from∘to :
    Extensionality lzero _ →
    ∀ l → from (to l) ≡ l
  from∘to ext l@(p , q) = Σ-≡,≡→≡
    (apply-ext ext′ (from₁∘to l))
    (apply-ext ext λ n →

     subst (λ p → ∀ n → p (suc n) ≡ up n (p n))
       (apply-ext ext′ (from₁∘to l))
       (λ _ → refl _) n                                            ≡⟨ sym $ push-subst-application _ _ ⟩

     subst (λ p → p (suc n) ≡ up n (p n))
       (apply-ext ext′ (from₁∘to l))
       (refl _)                                                    ≡⟨ trans subst-in-terms-of-trans-and-cong $
                                                                      cong (trans _) $
                                                                      trans-reflˡ _ ⟩
     trans (sym $ cong (_$ suc n) (apply-ext ext′ (from₁∘to l)))
       (cong (λ p → up n (p n)) (apply-ext ext′ (from₁∘to l)))     ≡⟨ cong₂ trans
                                                                        (cong sym $ Eq.cong-good-ext ext _)
                                                                        (trans (sym $ cong-∘ _ _ _) $
                                                                         cong (cong _) $ Eq.cong-good-ext ext _) ⟩
     trans (sym $ from₁∘to l (suc n))
       (cong (up n) $ from₁∘to l n)                                ≡⟨⟩

     trans (sym $ trans (cong (up n) $ from₁∘to l n) (sym $ q n))
       (cong (up n) $ from₁∘to l n)                                ≡⟨ cong (flip trans _) $
                                                                      trans (sym-trans _ _) $
                                                                      cong (flip trans _) $
                                                                      sym-sym _ ⟩
     trans (trans (q n) (sym $ cong (up n) $ from₁∘to l n))
       (cong (up n) $ from₁∘to l n)                                ≡⟨ trans-[trans-sym]- _ _ ⟩∎

     q n                                                           ∎)
    where
    ext′ = Eq.good-ext ext

-- A variant of cochain-limit-↠ for simple cochains.

simple-cochain-limit-↠ :
  (∃ λ (f : ℕ → A) → ∀ n → f (suc n) ≡ f n) ↠ A
simple-cochain-limit-↠ = λ where
  ._↠_.logical-equivalence ._⇔_.to   (f , _)     → f 0
  ._↠_.logical-equivalence ._⇔_.from f₀ .proj₁ _ → f₀
  ._↠_.logical-equivalence ._⇔_.from f₀ .proj₂ _ → refl _
  ._↠_.right-inverse-of                          → refl

-- The first projection of the right-to-left direction of
-- simple-cochain-limit-↠ computes in a certain way.

_ : proj₁ (_↠_.from simple-cochain-limit-↠ x) n ≡ x
_ = refl _

-- A variant of cochain-limit for simple cochains.

simple-cochain-limit :
  {A : Type a} →
  (∃ λ (f : ℕ → A) → ∀ n → f (suc n) ≡ f n) ↝[ lzero ∣ a ] A
simple-cochain-limit =
  generalise-ext?
    (_↠_.logical-equivalence scl)
    (λ ext → _↠_.right-inverse-of scl , from∘to ext)
  where
  scl = simple-cochain-limit-↠

  open _↠_ scl

  from₁∘to : ∀ l n → proj₁ (from (to l)) n ≡ proj₁ l n
  from₁∘to _         zero    = refl _
  from₁∘to l@(f , p) (suc n) =
    proj₁ (from (to l)) n  ≡⟨ from₁∘to l n ⟩
    f n                    ≡⟨ sym $ p n ⟩∎
    f (suc n)              ∎

  from∘to :
    Extensionality lzero _ →
    ∀ l → from (to l) ≡ l
  from∘to ext l@(f , p) = Σ-≡,≡→≡
    (apply-ext ext′ (from₁∘to l))
    (apply-ext ext λ n →

     subst (λ f → ∀ n → f (suc n) ≡ f n)
       (apply-ext ext′ (from₁∘to l))
       (λ _ → refl _) n                                             ≡⟨ sym $ push-subst-application _ _ ⟩

     subst (λ f → f (suc n) ≡ f n)
       (apply-ext ext′ (from₁∘to l))
       (refl _)                                                     ≡⟨ trans subst-in-terms-of-trans-and-cong $
                                                                       cong (trans _) $
                                                                       trans-reflˡ _ ⟩
     trans (sym $ cong (_$ suc n) (apply-ext ext′ (from₁∘to l)))
       (cong (_$ n) (apply-ext ext′ (from₁∘to l)))                  ≡⟨ cong₂ trans
                                                                         (cong sym $ Eq.cong-good-ext ext _)
                                                                         (Eq.cong-good-ext ext _) ⟩
     trans (sym $ from₁∘to l (suc n)) (from₁∘to l n)                ≡⟨⟩

     trans (sym $ trans (from₁∘to l n) (sym $ p n)) (from₁∘to l n)  ≡⟨ cong (flip trans _) $
                                                                       trans (sym-trans _ _) $
                                                                       cong (flip trans _) $
                                                                       sym-sym _ ⟩

     trans (trans (p n) (sym $ from₁∘to l n)) (from₁∘to l n)        ≡⟨ trans-[trans-sym]- _ _ ⟩∎

     p n                                                            ∎)
    where
    ext′ = Eq.good-ext ext

-- The first projection of the right-to-left direction of
-- simple-cochain-limit computes in a certain way (at least when "k"
-- has certain values).

_ : proj₁ (_⇔_.from (simple-cochain-limit _) x) n ≡ x
_ = refl _

_ : proj₁ (_≃_.from (simple-cochain-limit ext) x) n ≡ x
_ = refl _

------------------------------------------------------------------------
-- Chains and containers

-- Containers can be applied to chains.

Container-chain :
  {I : Type i} {O : Type o} →
  Container₂ I O s p → Chain I ℓ → Chain O (s ⊔ p ⊔ ℓ)
Container-chain C = Σ-map (⟦ C ⟧ ∘_) (map C ∘_)

-- The polynomial functor (for a container C) of the limit of a chain
-- is pointwise equivalent to the limit of C applied to the chain
-- (assuming extensionality).
--
-- This is a variant of Lemma 13 in "Non-wellfounded trees in Homotopy
-- Type Theory".

⟦⟧-Limit≃ :
  {I : Type i} {O : Type o} →
  Extensionality p (s ⊔ p ⊔ ℓ) →
  (C : Container₂ I O s p) (X : Chain I ℓ) {o : O} →

  ⟦ C ⟧ (Limit X) o ≃ Limit (Container-chain C X) o
⟦⟧-Limit≃ {p = p} {s = s} {ℓ = ℓ} ext C X@(Q , down) {o = o} =

  ⟦ C ⟧ (Limit X) o                                            ↔⟨⟩

  (∃ λ (s : Shape C o) →
     (p : Position C s) → Limit X (index C p))                 ↝⟨ (∃-cong λ _ →
                                                                   universal-property-Π X) ⟩
  (∃ λ (s : Shape C o) →
   ∃ λ (f : ∀ n (p : Position C s) → Q n (index C p)) →
     ∀ n p → down n (index C p) (f (suc n) p) ≡ f n p)         ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                   ∀-cong (lower-extensionality p r ext) λ _ →
                                                                   Eq.extensionality-isomorphism (lower-extensionality p r ext)) ⟩
  (∃ λ (s : Shape C o) →
   ∃ λ (f : ∀ n (p : Position C s) → Q n (index C p)) →
     ∀ n → down n _ ∘ f (suc n) ≡ f n)                         ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∀-cong (lower-extensionality p r ext) λ _ →
                                                                   ≡⇒↝ _ $ cong (_≡ _) $ sym $
                                                                   subst-refl _ _) ⟩
  (∃ λ (s : Shape C o) →
   ∃ λ (f : ∀ n (p : Position C s) → Q n (index C p)) →
     ∀ n → subst (λ s → (p : Position C s) → Q n (index C p))
             (refl _) (down n _ ∘ f (suc n)) ≡
           f n)                                                ↝⟨ (Σ-cong (inverse $
                                                                           simple-cochain-limit {k = equivalence}
                                                                             (lower-extensionality p r ext)) λ _ →
                                                                   F.id) ⟩
  (∃ λ ((s , eq) : ∃ λ (s : ℕ → Shape C o) →
                     ∀ n → s (suc n) ≡ s n) →
   ∃ λ (f : ∀ n (p : Position C (s n)) → Q n (index C p)) →
     ∀ n → subst (λ s → (p : Position C s) → Q n (index C p))
             (eq n) (down n _ ∘ f (suc n)) ≡
           f n)                                                ↔⟨ (∃-cong λ _ →
                                                                   (∃-cong λ _ →
                                                                    (∀-cong (lower-extensionality p r ext) λ _ →
                                                                     Bijection.Σ-≡,≡↔≡) F.∘
                                                                    inverse ΠΣ-comm) F.∘
                                                                   ∃-comm) F.∘
                                                                  inverse Σ-assoc ⟩
  (∃ λ (s : ℕ → Shape C o) →
   ∃ λ (f : ∀ n (p : Position C (s n)) → Q n (index C p)) →
     ∀ n → (s (suc n) , down n _ ∘ f (suc n)) ≡ (s n , f n))   ↔⟨⟩

  (∃ λ (s : ℕ → Shape C o) →
   ∃ λ (f : ∀ n (p : Position C (s n)) → Q n (index C p)) →
     ∀ n → map C (down n) o (s (suc n) , f (suc n)) ≡
           (s n , f n))                                        ↝⟨ (inverse $ Σ-cong-id (Eq.↔⇒≃ ΠΣ-comm)) F.∘
                                                                  Eq.↔⇒≃ Σ-assoc ⟩
  (∃ λ (f : ∀ n → ∃ λ (s : Shape C o) →
                    (p : Position C s) → Q n (index C p)) →
     ∀ n → map C (down n) o (f (suc n)) ≡ f n)                 ↔⟨⟩

  Limit (Container-chain C X) o                                □
  where
  r = s ⊔ p ⊔ ℓ

------------------------------------------------------------------------
-- M-types

private

  -- Up-to C n is the n-fold application of ⟦ C ⟧ to something
  -- trivial.

  Up-to : {I : Type i} → Container I s p → ℕ → I → Type (i ⊔ s ⊔ p)
  Up-to C zero    = λ _ → ↑ _ ⊤
  Up-to C (suc n) = ⟦ C ⟧ (Up-to C n)

  -- Up-to C is downwards closed.

  down : ∀ n → Up-to C (suc n) ⇾ Up-to C n
  down zero    = _
  down (suc n) = map _ (down n)

-- One can combine Up-to and down into a chain.

M-chain : {I : Type i} → Container I s p → Chain I (i ⊔ s ⊔ p)
M-chain C = Up-to C , down

-- An M-type for a given container.

M : {I : Type i} → Container I s p → I → Type (i ⊔ s ⊔ p)
M C = Limit (M-chain C)

-- M C is, in a certain sense, a fixpoint of ⟦ C ⟧ (assuming
-- extensionality).

M-fixpoint :
  Block "M-fixpoint" →
  {I : Type i} →
  Extensionality p (i ⊔ s ⊔ p) →
  {C : Container I s p} {i : I} →
  ⟦ C ⟧ (M C) i ≃ M C i
M-fixpoint ⊠ ext {C = C} {i = i} =
  ⟦ C ⟧ (M C) i                            ↔⟨⟩
  ⟦ C ⟧ (Limit (M-chain C)) i              ↝⟨ ⟦⟧-Limit≃ ext C (M-chain C) ⟩
  Limit (Container-chain C (M-chain C)) i  ↔⟨⟩
  Limit (shift (M-chain C)) i              ↝⟨ Limit-shift (M-chain C) (lower-extensionality _ lzero ext) ⟩
  Limit (M-chain C) i                      ↔⟨⟩
  M C i                                    □

-- One direction of the fixpoint.

out-M :
  Block "M-fixpoint" →
  {I : Type i} {C : Container I s p} →
  Extensionality p (i ⊔ s ⊔ p) →
  M C ⇾ ⟦ C ⟧ (M C)
out-M b ext _ = _≃_.from (M-fixpoint b ext)

-- The other direction of the fixpoint.

in-M :
  Block "M-fixpoint" →
  {I : Type i} {C : Container I s p} →
  Extensionality p (i ⊔ s ⊔ p) →
  ⟦ C ⟧ (M C) ⇾ M C
in-M b ext _ = _≃_.to (M-fixpoint b ext)

-- A "computation" rule for in-M.

in-M≡ :
  (b : Block "M-fixpoint")
  {I : Type i}
  (ext : Extensionality p (i ⊔ s ⊔ p)) →
  let ext′ = apply-ext $ Eq.good-ext $
             lower-extensionality p (i ⊔ s ⊔ p) ext
  in
  {C : Container I s p} {i : I}
  (x@(s , f) : ⟦ C ⟧ (M C) i) →
  in-M b ext _ x ≡
  ( ℕ-case _ (λ n → s , λ p → proj₁ (f p) n)
  , ℕ-case (refl _) (λ n → cong (s ,_) $ ext′ λ p → proj₂ (f p) n)
  )
in-M≡ {i = i} {p = p} {s = sℓ} ⊠ ext {C = C} x@(s , f) =
  ( ℕ-case _ (λ n → s , λ p → proj₁ (f p) n)
  , ℕ-case (refl _)
      (λ n → Σ-≡,≡→≡
         (refl _)
         (≡⇒→
            (cong (_≡ λ p → proj₁ (f p) n) $ sym $
             subst-refl _ _)
            (ext′ λ p → proj₂ (f p) n)))
  )                                                                 ≡⟨ cong (ℕ-case _ (λ n → s , λ p → proj₁ (f p) n) ,_) $
                                                                       cong (ℕ-case (refl _)) $
                                                                       apply-ext (lower-extensionality _ lzero ext) lemma ⟩∎
  ( ℕ-case _ (λ n → s , λ p → proj₁ (f p) n)
  , ℕ-case (refl _) (λ n → cong (s ,_) $ ext′ λ p → proj₂ (f p) n)
  )                                                                 ∎
  where
  ext′ =
    apply-ext $
    Eq.good-ext $
    lower-extensionality p (i ⊔ sℓ ⊔ p) ext

  lemma = λ n →
    Σ-≡,≡→≡
      (refl _)
      (≡⇒→
         (cong (_≡ λ p → proj₁ (f p) n) $ sym $
          subst-refl _ _)
         (ext′ λ p → proj₂ (f p) n))                ≡⟨ Σ-≡,≡→≡-reflˡ _ ⟩

    cong (_ ,_)
         (trans (sym $ subst-refl _ _) $
          ≡⇒→
            (cong (_≡ λ p → proj₁ (f p) n) $ sym $
             subst-refl _ _)
            (ext′ λ p → proj₂ (f p) n))             ≡⟨ cong (cong (_ ,_)) $ cong (trans _) $ sym $
                                                       subst-id-in-terms-of-≡⇒↝ equivalence ⟩
    cong (_ ,_)
         (trans (sym $ subst-refl _ _) $
          subst id
            (cong (_≡ λ p → proj₁ (f p) n) $ sym $
             subst-refl _ _)
            (ext′ λ p → proj₂ (f p) n))             ≡⟨ cong (cong (_ ,_)) $ cong (trans _) $ sym $
                                                       subst-∘ _ _ _ ⟩
    cong (_ ,_)
         (trans (sym $ subst-refl _ _) $
          subst (_≡ λ p → proj₁ (f p) n)
            (sym $ subst-refl _ _)
            (ext′ λ p → proj₂ (f p) n))             ≡⟨ cong (cong (_ ,_)) $ cong (trans _) $
                                                       subst-trans _ ⟩
    cong (_ ,_)
         (trans (sym $ subst-refl _ _) $
          trans (subst-refl _ _)
            (ext′ λ p → proj₂ (f p) n))             ≡⟨ cong (cong (_ ,_)) $
                                                       trans-sym-[trans] _ _ ⟩∎
    cong (_ ,_) (ext′ λ p → proj₂ (f p) n)          ∎

-- A coalgebra defined using M and out-M.

M-coalgebra :
  Block "M-fixpoint" →
  {I : Type i} →
  Extensionality p (i ⊔ s ⊔ p) →
  (C : Container I s p) → Coalgebra C
M-coalgebra b ext C = M C , out-M b ext

-- Definitions used to implement unfold.

private
 module Unfold
  ((P , f) : Coalgebra C)
  where
  up : ∀ n → P ⇾ Up-to C n
  up zero    = _
  up (suc n) = map C (up n) ∘⇾ f

  ok : ∀ n → down n ∘⇾ up (suc n) ≡ up n
  ok zero    = refl _
  ok (suc n) =
    map C (down n ∘⇾ up (suc n)) ∘⇾ f  ≡⟨ cong (λ g → map C g ∘⇾ f) $ ok n ⟩∎
    map C (up n) ∘⇾ f                  ∎

-- A direct implementation of an unfold operation.

unfold :
  ((P , _) : Coalgebra C) →
  P ⇾ M C
unfold Y i p =
    (λ n → up n i p)
  , (λ n → cong (λ f → f i p) (ok n))
  where
  open Unfold Y

-- Definitions used to implement M-final.

private
 module M-final
  (b : Block "M-fixpoint")
  {I : Type i} {C : Container I s p}
  (ext : Extensionality p (i ⊔ s ⊔ p))
  (ext′ : Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p))
  (Y@(P , f) : Coalgebra C)
  where

  step : P ⇾ Q → P ⇾ ⟦ C ⟧ Q
  step h = map C h ∘⇾ f

  univ : Cone P (M-chain C) → P ⇾ M C
  univ = _≃_.from (universal-property-≃ ext′ (M-chain C))

  steps₁ : (∀ n → P ⇾ Up-to C n) → (∀ n → P ⇾ Up-to C n)
  steps₁ g n i p =
    ℕ-case
      {P = λ n → Up-to C n i}
      _
      (λ n → step (g n) i p)
      n

  Eq : (∀ n → P ⇾ Up-to C n) → Type (i ⊔ s ⊔ p)
  Eq g = ∀ n → down n ∘⇾ g (suc n) ≡ g n

  steps₂ : {g : ∀ n → P ⇾ Up-to C n} → Eq g → Eq (steps₁ g)
  steps₂         p zero    = refl _
  steps₂ {g = g} p (suc n) =
    down (suc n) ∘⇾ steps₁ g (suc (suc n))  ≡⟨⟩
    step (down n ∘⇾ g (suc n))              ≡⟨ cong step (p n) ⟩∎
    step (g n)                              ∎

  steps : Cone P (M-chain C) → Cone P (M-chain C)
  steps = Σ-map steps₁ steps₂

  ext-i : Extensionality i (i ⊔ s ⊔ p)
  ext-i = lower-extensionality (s ⊔ p) lzero ext′

  ext₀ : Extensionality lzero (i ⊔ s ⊔ p)
  ext₀ = lower-extensionality _ lzero ext

  ext₀′ :
    {A : Type} {P : A → Type (i ⊔ s ⊔ p)} →
    Extensionality′ A P
  ext₀′ = apply-ext (Eq.good-ext ext₀)

  ≡univ-steps : ∀ c → in-M b ext ∘⇾ step (univ c) ≡ univ (steps c)
  ≡univ-steps c@(g , eq) = apply-ext ext-i λ i → apply-ext ext′ λ p →
    in-M b ext i (step (univ c) i p)                                  ≡⟨ in-M≡ b ext (step (univ c) i p) ⟩

    ( (λ n → steps₁ g n i p)
    , ℕ-case (refl _)
        (λ n →
           cong (proj₁ (f i p) ,_)
             (ext‴ λ p′ →
              ext⁻¹ (ext⁻¹ (eq n) (index C p′)) (proj₂ (f i p) p′)))
    )                                                                 ≡⟨ cong ((λ n → steps₁ g n i p) ,_) $
                                                                         ext₀′ $ ℕ-case
                                                                           (
        refl _                                                              ≡⟨ sym $ ext⁻¹-refl _ {x = p} ⟩
        ext⁻¹ (refl _) p                                                    ≡⟨ cong (flip ext⁻¹ p) $ sym $ ext⁻¹-refl _ ⟩
        ext⁻¹ (ext⁻¹ {B = λ x → P x → ↑ _ ⊤} (refl _) i) p                  ≡⟨⟩
        ext⁻¹ (ext⁻¹ (steps₂ eq zero) i) p                                  ∎)
                                                                           (λ n →
        cong (proj₁ (f i p) ,_)
          (ext‴ λ p′ →
           ext⁻¹ (ext⁻¹ (eq n) (index C p′)) (proj₂ (f i p) p′))              ≡⟨ elim₁
                                                                                (λ eq →
                                                                                cong (proj₁ (f i p) ,_)
                                                                                (ext‴ λ p′ →
                                                                                ext⁻¹ (ext⁻¹ eq (index C p′)) (proj₂ (f i p) p′)) ≡
                                                                                ext⁻¹ (ext⁻¹ (cong (λ g → map C g ∘⇾ f) eq) i) p)
                                                                                (
            cong (proj₁ (f i p) ,_)
              (ext‴ λ p′ →
               ext⁻¹ (ext⁻¹ (refl (g n)) (index C p′))
                 (proj₂ (f i p) p′))                                                ≡⟨ (cong (cong _) $
                                                                                cong ext‴ $ ext‴ λ _ →
                                                                                trans (cong (flip ext⁻¹ _) $
                                                                                ext⁻¹-refl _) $
                                                                                ext⁻¹-refl _) ⟩

            cong (proj₁ (f i p) ,_) (ext‴ λ _ → refl _)                            ≡⟨ trans (cong (cong _) $
                                                                                Eq.good-ext-refl ext″ _) $
                                                                                cong-refl _ ⟩

            refl _                                                                  ≡⟨ sym $
                                                                                trans (cong (flip ext⁻¹ _) $
                                                                                trans (cong (flip ext⁻¹ _) $
                                                                                cong-refl _) $
                                                                                ext⁻¹-refl _) $
                                                                                ext⁻¹-refl _ ⟩∎
            ext⁻¹ (ext⁻¹ (cong step (refl (g n))) i) p                              ∎)
                                                                                (eq n) ⟩
        ext⁻¹ (ext⁻¹ (cong step (eq n)) i) p                                  ∎) ⟩

    ( (λ n → steps₁ g n i p)
    , (λ n → ext⁻¹ (ext⁻¹ (steps₂ eq n) i) p)
    )                                                                 ≡⟨⟩

    univ (steps c) i p                                                ∎
    where
    ext″ = lower-extensionality p (i ⊔ s ⊔ p) ext
    ext‴ = apply-ext (Eq.good-ext ext″)

  contr : Contractible (P ⇾ Up-to C 0)
  contr =
    Π-closure ext-i 0 λ _ →
    Π-closure ext′ 0 λ _ →
    ↑-closure 0 ⊤-contractible

  steps₁-fixpoint≃ :
    {g : ∀ n → P ⇾ Up-to C n} →
    (g ≡ steps₁ g) ≃ (∀ n → g (suc n) ≡ step (g n))
  steps₁-fixpoint≃ {g = g} =
    g ≡ steps₁ g                                             ↝⟨ inverse $ Eq.extensionality-isomorphism ext₀ ⟩

    (∀ n → g n ≡ steps₁ g n)                                 ↝⟨ Πℕ≃ ext₀ ⟩

    g 0 ≡ steps₁ g 0 × (∀ n → g (suc n) ≡ steps₁ g (suc n))  ↔⟨⟩

    (λ _ _ → lift tt) ≡ (λ _ _ → lift tt) ×
    (∀ n → g (suc n) ≡ step (g n))                           ↔⟨ (drop-⊤-left-× λ _ →
                                                                 _⇔_.to contractible⇔↔⊤ $
                                                                 H-level.⇒≡ 0 contr) ⟩□
    (∀ n → g (suc n) ≡ step (g n))                           □

  cochain₁ : Cochain (i ⊔ s ⊔ p)
  cochain₁ = (λ n → P ⇾ Up-to C n)
           , (λ _ → step)

  cl₁← : P ⇾ Up-to C 0 → ∀ n → P ⇾ Up-to C n
  cl₁← = proj₁ ∘ _↠_.from (cochain-limit-↠ cochain₁)

  ⇾↔⊤ : (P ⇾ Up-to C 0) ↔ ⊤
  ⇾↔⊤ = _⇔_.to contractible⇔↔⊤ contr

  g₀ : P ⇾ Up-to C 0
  g₀ = _↔_.from ⇾↔⊤ _

  steps₁-fixpoint : ∀ n → cl₁← g₀ n ≡ steps₁ (cl₁← g₀) n
  steps₁-fixpoint = ℕ-case (refl _) (λ _ → refl _)

  steps₁-fixpoint-lemma :
    {p : Eq (cl₁← g₀)} →
    subst Eq (_≃_.from steps₁-fixpoint≃ (λ _ → refl _)) p n ≡
    trans (p n) (steps₁-fixpoint n)
  steps₁-fixpoint-lemma {n = n} {p = p} =
    subst Eq (_≃_.from steps₁-fixpoint≃ (λ _ → refl _)) p n    ≡⟨⟩

    subst Eq (ext₀′ (ℕ-case _ (λ _ → refl _))) p n             ≡⟨ cong (λ eq → subst Eq eq p n) $
                                                                  cong ext₀′ $
                                                                  cong (flip ℕ-case _) $
                                                                  H-level.mono (Nat.zero≤ 2) contr _ _ ⟩

    subst Eq (ext₀′ steps₁-fixpoint) p n                       ≡⟨ sym $ push-subst-application _ _ ⟩

    subst (λ g → down n ∘⇾ g (suc n) ≡ g n)
      (ext₀′ steps₁-fixpoint) (p n)                            ≡⟨ trans subst-in-terms-of-trans-and-cong $
                                                                  cong (flip trans _) $ cong sym $ sym $
                                                                  cong-∘ _ _ _ ⟩
    trans (sym (cong (down n ∘⇾_)
                  (cong (_$ suc n) (ext₀′ steps₁-fixpoint))))
      (trans (p n) (cong (_$ n) (ext₀′ steps₁-fixpoint)))      ≡⟨ cong₂ (λ eq₁ eq₂ → trans (sym (cong (down n ∘⇾_) eq₁)) (trans _ eq₂))
                                                                    (Eq.cong-good-ext ext₀ _)
                                                                    (Eq.cong-good-ext ext₀ _) ⟩
    trans (sym (cong (down n ∘⇾_) (steps₁-fixpoint (suc n))))
      (trans (p n) (steps₁-fixpoint n))                        ≡⟨⟩

    trans (sym (cong (down n ∘⇾_) (refl _)))
      (trans (p n) (steps₁-fixpoint n))                        ≡⟨ trans (cong (flip trans _) $
                                                                         trans (cong sym $ cong-refl _)
                                                                         sym-refl) $
                                                                  trans-reflˡ _ ⟩∎
    trans (p n) (steps₁-fixpoint n)                            ∎

  cochain₂ : Cochain (i ⊔ s ⊔ p)
  cochain₂ = (λ n → down n ∘⇾ step (cl₁← g₀ n) ≡ cl₁← g₀ n)
           , (λ _ → cong step)

  equiv : Block "equiv" → (Y ⇨ M-coalgebra b ext C) ≃ ⊤
  equiv ⊠ =
    Y ⇨ M-coalgebra b ext C                                             ↔⟨⟩

    (∃ λ (h : P ⇾ M C) → out-M b ext ∘⇾ h ≡ step h)                     ↝⟨ (∃-cong λ _ → inverse $
                                                                            Eq.≃-≡ $ ∀-cong ext-i λ _ → ∀-cong ext′ λ _ →
                                                                            M-fixpoint b ext) ⟩
    (∃ λ (h : P ⇾ M C) →
       (in-M b ext ∘⇾ out-M b ext) ∘⇾ h ≡ in-M b ext ∘⇾ step h)         ↝⟨ (∃-cong λ h → ≡⇒↝ _ $ cong (_≡ in-M b ext ∘⇾ step h) $
                                                                            apply-ext ext-i λ _ → apply-ext ext′ λ _ →
                                                                            _≃_.right-inverse-of (M-fixpoint b ext) _) ⟩

    (∃ λ (h : P ⇾ M C) → h ≡ in-M b ext ∘⇾ step h)                      ↝⟨ (inverse $
                                                                            Σ-cong (inverse $ universal-property-≃ ext′ (M-chain C)) λ _ →
                                                                            F.id) ⟩
    (∃ λ (c : Cone P (M-chain C)) →
       univ c ≡ in-M b ext ∘⇾ step (univ c))                            ↝⟨ (∃-cong λ c → ≡⇒↝ _ $ cong (univ c ≡_) $ ≡univ-steps c) ⟩

    (∃ λ (c : Cone P (M-chain C)) → univ c ≡ univ (steps c))            ↝⟨ (∃-cong λ _ →
                                                                            Eq.≃-≡ $ inverse $ universal-property-≃ ext′ (M-chain C)) ⟩

    (∃ λ (c : Cone P (M-chain C)) → c ≡ steps c)                        ↔⟨ (∃-cong λ _ → inverse
                                                                            Bijection.Σ-≡,≡↔≡) ⟩
    (∃ λ ((g , p) : Cone P (M-chain C)) →
     ∃ λ (q : g ≡ steps₁ g) → subst Eq q p ≡ steps₂ p)                  ↔⟨ Σ-assoc F.∘
                                                                           (∃-cong λ _ → ∃-comm) F.∘
                                                                           inverse Σ-assoc ⟩
    (∃ λ ((g , q) : ∃ λ (g : ∀ n → P ⇾ Up-to C n) → g ≡ steps₁ g) →
     ∃ λ (p : Eq g) → subst Eq q p ≡ steps₂ p)                          ↝⟨ (inverse $
                                                                            Σ-cong (inverse $
                                                                                ∃-cong λ _ →
                                                                                steps₁-fixpoint≃) λ _ →
                                                                            F.id) ⟩
    (∃ λ ((g , q) : ∃ λ (g : ∀ n → P ⇾ Up-to C n) →
                      ∀ n → g (suc n) ≡ step (g n)) →
     ∃ λ (p : Eq g) →
       subst Eq (_≃_.from steps₁-fixpoint≃ q) p ≡ steps₂ p)             ↝⟨ (inverse $
                                                                            Σ-cong (inverse $
                                                                                cochain-limit cochain₁ {k = equivalence} ext₀) λ _ →
                                                                            F.id) ⟩
    (∃ λ (g : P ⇾ Up-to C 0) →
     ∃ λ (p : Eq (cl₁← g)) →
       subst Eq (_≃_.from steps₁-fixpoint≃ (λ _ → refl _)) p ≡
       steps₂ p)                                                        ↔⟨ drop-⊤-left-Σ ⇾↔⊤ ⟩

    (∃ λ (p : Eq (cl₁← g₀)) →
       subst Eq (_≃_.from steps₁-fixpoint≃ (λ _ → refl _)) p ≡
       steps₂ p)                                                        ↝⟨ (∃-cong λ _ → inverse $
                                                                            Eq.extensionality-isomorphism ext₀) ⟩
    (∃ λ (p : Eq (cl₁← g₀)) →
       ∀ n → subst Eq (_≃_.from steps₁-fixpoint≃ (λ _ → refl _)) p n ≡
             steps₂ p n)                                                ↝⟨ (∃-cong λ p → ∀-cong ext₀ λ n → ≡⇒↝ _ $ cong (_≡ steps₂ p n)
                                                                            steps₁-fixpoint-lemma) ⟩
    (∃ λ (p : Eq (cl₁← g₀)) →
       ∀ n → trans (p n) (steps₁-fixpoint n) ≡ steps₂ p n)              ↝⟨ (∃-cong λ _ → ∀-cong ext₀ λ _ → ≡⇒↝ _ $
                                                                            [trans≡]≡[≡trans-symʳ] _ _ _) ⟩
    (∃ λ (p : Eq (cl₁← g₀)) →
       ∀ n → p n ≡ trans (steps₂ p n) (sym (steps₁-fixpoint n)))        ↝⟨ (∃-cong λ _ →
                                                                            Πℕ≃ ext₀) ⟩
    (∃ λ (p : Eq (cl₁← g₀)) →
       p zero ≡ trans (steps₂ p zero) (sym (steps₁-fixpoint zero)) ×
       (∀ n → p (suc n) ≡
              trans (steps₂ p (suc n))
                (sym (steps₁-fixpoint (suc n)))))                       ↔⟨ (∃-cong λ _ → drop-⊤-left-× λ _ →
                                                                            _⇔_.to contractible⇔↔⊤ $
                                                                            H-level.⇒≡ 0 $ H-level.⇒≡ 0 contr) ⟩
    (∃ λ (p : Eq (cl₁← g₀)) →
       ∀ n → p (suc n) ≡
             trans (steps₂ p (suc n)) (sym (steps₁-fixpoint (suc n))))  ↔⟨⟩

    (∃ λ (p : Eq (cl₁← g₀)) →
       ∀ n → p (suc n) ≡
             trans (cong step (p n)) (sym (refl _)))                    ↝⟨ (∃-cong λ _ → ∀-cong ext₀ λ _ → ≡⇒↝ _ $ cong (_ ≡_) $
                                                                            trans (cong (trans _) sym-refl) $
                                                                            trans-reflʳ _) ⟩
    (∃ λ (p : Eq (cl₁← g₀)) →
       ∀ n → p (suc n) ≡ cong step (p n))                               ↝⟨ cochain-limit cochain₂ ext₀ ⟩

    down {C = C} 0 ∘⇾ step (cl₁← g₀ 0) ≡ cl₁← g₀ 0                      ↔⟨ _⇔_.to contractible⇔↔⊤ $
                                                                           H-level.⇒≡ 0 contr ⟩□
    ⊤                                                                   □

  -- The definition of M-final is set up so that it returns unfold Y
  -- rather than the function obtained directly from equiv. Here it is
  -- shown that the two functions are equal.

  ≡-unfold : ∀ b → proj₁ (_≃_.from (equiv b) _) ≡ unfold Y
  ≡-unfold ⊠ =
    apply-ext ext-i λ i → apply-ext ext′ λ p →
    Σ-≡,≡→≡
      (ext₀′ λ n → cong (λ f → f i p) (lemma₁ n))
      (lemma₃ i p)
    where

    -- Pieces of the function obtained from equiv.
    --
    -- These pieces are rather similar to pieces of unfold. I chose to
    -- implement unfold using explicit pattern matching rather than
    -- ℕ-rec to ensure that things do not unfold too much.

    up′ : ∀ n → P ⇾ Up-to C n
    up′ = ℕ-rec _ (λ _ ih → map C ih ∘⇾ f)

    ok′ : ∀ n → down n ∘⇾ up′ (suc n) ≡ up′ n
    ok′ = ℕ-rec
      (proj₁ (H-level.⇒≡ 0 contr))
      (λ _ → cong step)

    lemma₁ : ∀ n → up′ n ≡ Unfold.up Y n
    lemma₁ zero    = refl _
    lemma₁ (suc n) =
      step (up′ n)          ≡⟨ cong step $ lemma₁ n ⟩∎
      step (Unfold.up Y n)  ∎

    lemma₂ :
      ∀ n →
      trans (sym (cong (down n ∘⇾_) (lemma₁ (suc n))))
        (trans (ok′ n) (lemma₁ n)) ≡
      Unfold.ok Y n
    lemma₂ zero =
      trans (sym (cong (const _) (cong step (refl _))))
        (trans (proj₁ (H-level.⇒≡ 0 contr)) (refl _))    ≡⟨ trans (cong (flip trans _) $
                                                                   trans (cong sym $ cong-const _) $
                                                                   sym-refl) $
                                                            trans (trans-reflˡ _) $
                                                            trans-reflʳ _ ⟩

      proj₁ (H-level.⇒≡ 0 contr)                         ≡⟨ H-level.mono (Nat.zero≤ 2) contr _ _ ⟩∎

      refl _                                             ∎
    lemma₂ (suc n) =
      trans (sym (cong (down (1 + n) ∘⇾_) (lemma₁ (2 + n))))
        (trans (ok′ (1 + n)) (lemma₁ (1 + n)))                           ≡⟨⟩

      trans (sym (cong (map C (down n) ∘⇾_)
                    (cong step (lemma₁ (suc n)))))
        (trans (cong step (ok′ n)) (cong step (lemma₁ n)))               ≡⟨ cong (flip trans _) $ cong sym $
                                                                            cong-∘ _ _ _ ⟩
      trans (sym (cong ((map C (down n) ∘⇾_) ∘ step) (lemma₁ (suc n))))
        (trans (cong step (ok′ n)) (cong step (lemma₁ n)))               ≡⟨⟩

      trans (sym (cong (step ∘ (down n ∘⇾_)) (lemma₁ (suc n))))
        (trans (cong step (ok′ n)) (cong step (lemma₁ n)))               ≡⟨ sym $
                                                                            trans (cong-trans _ _ _) $
                                                                            cong₂ trans
                                                                              (trans (cong-sym _ _) $
                                                                               cong sym $ cong-∘ _ _ _)
                                                                              (cong-trans _ _ _) ⟩
      cong step
        (trans (sym (cong (down n ∘⇾_) (lemma₁ (suc n))))
           (trans (ok′ n) (lemma₁ n)))                                   ≡⟨ cong (cong _) $ lemma₂ n ⟩

      cong step (Unfold.ok Y n)                                          ≡⟨⟩

      Unfold.ok Y (1 + n)                                                ∎

    lemma₃ :
      ∀ i p →
      subst (λ f → ∀ n → down n i (f (suc n)) ≡ f n)
        (ext₀′ λ n → cong (λ f → f i p) (lemma₁ n))
        (cong (_$ p) ∘ cong (_$ i) ∘ ok′) ≡
      (λ n → cong (λ f → f i p) (Unfold.ok Y n))
    lemma₃ i p = ext₀′ λ n →
      subst (λ f → ∀ n → down n i (f (suc n)) ≡ f n)
        (ext₀′ λ n → cong (λ f → f i p) (lemma₁ n))
        (cong (_$ p) ∘ cong (_$ i) ∘ ok′) n                            ≡⟨ sym $
                                                                          push-subst-application _ _ ⟩
      subst (λ f → down n i (f (suc n)) ≡ f n)
        (ext₀′ λ n → cong (λ f → f i p) (lemma₁ n))
        (cong (_$ p) (cong (_$ i) (ok′ n)))                            ≡⟨ cong (subst (λ f → down n i (f (suc n)) ≡ f n) _) $
                                                                          cong-∘ _ _ _ ⟩
      subst (λ f → down n i (f (suc n)) ≡ f n)
        (ext₀′ λ n → cong (λ f → f i p) (lemma₁ n))
        (cong (λ f → f i p) (ok′ n))                                   ≡⟨ subst-in-terms-of-trans-and-cong ⟩

      trans (sym (cong (λ f → down n i (f (suc n)))
                    (ext₀′ λ n → cong (λ f → f i p) (lemma₁ n))))
        (trans (cong (λ f → f i p) (ok′ n))
           (cong (_$ n) (ext₀′ λ n → cong (λ f → f i p) (lemma₁ n))))  ≡⟨ cong₂ (λ eq₁ eq₂ →
                                                                                trans (sym eq₁) (trans (cong (λ f → f i p) (ok′ n)) eq₂))
                                                                            (trans (sym $ cong-∘ _ _ _) $
                                                                             cong (cong _) $
                                                                             Eq.cong-good-ext ext₀ _)
                                                                            (Eq.cong-good-ext ext₀ _) ⟩
      trans (sym (cong (down n i)
                    (cong (λ f → f i p) (lemma₁ (suc n)))))
        (trans (cong (λ f → f i p) (ok′ n))
           (cong (λ f → f i p) (lemma₁ n)))                            ≡⟨ cong (flip trans _) $ cong sym $
                                                                          cong-∘ _ _ _ ⟩
      trans (sym (cong (λ f → down n i (f i p)) (lemma₁ (suc n))))
        (trans (cong (λ f → f i p) (ok′ n))
           (cong (λ f → f i p) (lemma₁ n)))                            ≡⟨ sym $
                                                                          trans (cong-trans _ _ _) $
                                                                          cong₂ trans
                                                                            (trans (cong-sym _ _) $
                                                                             cong sym $
                                                                             cong-∘ _ _ _)
                                                                            (cong-trans _ _ _) ⟩
      cong (λ f → f i p)
        (trans (sym (cong (down n ∘⇾_) (lemma₁ (suc n))))
           (trans (ok′ n) (lemma₁ n)))                                 ≡⟨ cong (cong _) $ lemma₂ n ⟩∎

      cong (λ f → f i p) (Unfold.ok Y n)                               ∎

  unfold-lemma :
    Block "equiv" →
    out-M b ext ∘⇾ unfold Y ≡ map _ (unfold Y) ∘⇾ f
  unfold-lemma b′ =
    subst
       (λ h → out-M b ext ∘⇾ h ≡ map C h ∘⇾ f)
       (≡-unfold b′)
       (proj₂ (_≃_.from (equiv b′) _))

  unfold-morphism :
    Block "equiv" → Y ⇨ M-coalgebra b ext C
  unfold-morphism b = unfold Y , unfold-lemma b

  ≡-unfold-morphism : ∀ b → _≃_.from (equiv b) _ ≡ unfold-morphism b
  ≡-unfold-morphism b =
    Σ-≡,≡→≡ (≡-unfold b) (refl (unfold-lemma b))

  M-final : Contractible (Y ⇨ M-coalgebra b ext C)
  M-final =
    block λ b →
    _↔_.from (contractible↔≃⊤ ext′) $
    Eq.with-other-inverse
      (equiv b)
      (λ _ → unfold-morphism b)
      (λ _ → ≡-unfold-morphism b)

  -- Note that unfold is not blocked, but that the other pieces are.

  M-final-partly-blocked :
    Block "M-final" →
    Contractible (Y ⇨ M-coalgebra b ext C)
  M-final-partly-blocked _ .proj₁ .proj₁ = unfold Y
  M-final-partly-blocked ⊠ .proj₁ .proj₂ = M-final .proj₁ .proj₂
  M-final-partly-blocked ⊠ .proj₂        = M-final .proj₂

-- M-coalgebra b ext C is a final coalgebra (assuming extensionality).
--
-- This is a variant of Theorem 7 from "Non-wellfounded trees in
-- Homotopy Type Theory".

M-final :
  (b : Block "M-final")
  {I : Type i} {C : Container I s p} →
  (ext : Extensionality p (i ⊔ s ⊔ p)) →
  Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p) →
  Final (M-coalgebra b ext C)
M-final b ext ext′ Y =
  M-final.M-final-partly-blocked b ext ext′ Y b

-- The morphism returned by M-final is definitionally equal to an
-- instance of unfold.

_ :
  {Y : Coalgebra C} →
  proj₁ (proj₁ (M-final b ext₁ ext₂ Y)) ≡ unfold Y
_ = refl _

------------------------------------------------------------------------
-- H-levels

-- If the shape types of C have h-level n, then M C i has h-level n
-- (assuming extensionality).
--
-- This is a variant of Lemma 14 from "Non-wellfounded trees in
-- Homotopy Type Theory".

H-level-M :
  Extensionality p (i ⊔ s ⊔ p) →
  {I : Type i} {C : Container I s p} {i : I} →
  (∀ i → H-level n (Shape C i)) →
  H-level n (M C i)
H-level-M {p = p} {i = iℓ} {n = m} ext {C = C} hyp =
  Σ-closure m
    (Π-closure ext′ m
     H-level-Up-to) λ _ →
  Π-closure ext′ m $
  H-level.⇒≡ m ∘ H-level-Up-to
  where
  ext′ = lower-extensionality _ lzero ext

  step :
    ∀ P → (∀ {i} → H-level m (P i)) → (∀ {i} → H-level m (⟦ C ⟧ P i))
  step P h =
    Σ-closure m (hyp _) λ _ →
    Π-closure ext m λ _ →
    h

  H-level-Up-to : ∀ n → H-level m (Up-to C n i)
  H-level-Up-to (suc n) = step (Up-to C n) (H-level-Up-to n)
  H-level-Up-to zero    =
    ↑-closure m (H-level.mono (Nat.zero≤ m) ⊤-contractible)

-- If the shape types of C have h-level n, then F i has h-level n,
-- where F is the carrier of any final coalgebra of C, and "final
-- coalgebra" is defined using Final′. (Assuming extensionality.)

H-level-final-coalgebra′ :
  Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p) →
  {I : Type i} {C : Container I s p} {i : I} →
  (((X , _) , _) : Final-coalgebra′ C) →
  (∀ i → H-level n (Shape C i)) →
  H-level n (X i)
H-level-final-coalgebra′
  {i = iℓ} {s = s} {n = n} ext {C = C} {i = i} F@((X , _) , _) =
  block λ b →

  (∀ i → H-level n (Shape C i))  ↝⟨ H-level-M ext′ ⟩
  H-level n (M C i)              ↝⟨ H-level-cong _ n $
                                    carriers-of-final-coalgebras-equivalent′
                                      (Final-coalgebra→Final-coalgebra′ $
                                       M-coalgebra b ext′ C , M-final b ext′ ext)
                                      F _ ⟩□
  H-level n (X i)                □
  where
  ext′ = lower-extensionality (iℓ ⊔ s) lzero ext

-- The previous result holds also if Final-coalgebra′ is replaced by
-- Final-coalgebra.

H-level-final-coalgebra :
  Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p) →
  {I : Type i} {C : Container I s p} {i : I} →
  (((X , _) , _) : Final-coalgebra C) →
  (∀ i → H-level n (Shape C i)) →
  H-level n (X i)
H-level-final-coalgebra ext =
  H-level-final-coalgebra′ ext ∘
  Final-coalgebra→Final-coalgebra′

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
data Nat : Set where

record Ord (A : Set) : Set where
  field f : A → A

instance
  OrdNat : Ord Nat
  OrdNat = record { f = λ x → x }

postulate
  T : Nat → Set
  R : ∀ {A} {{_ : Ord A}} → A → Set

-- Before solving the type of m, instance search considers it to
-- be a potential candidate for Ord Nat. It then proceeds to check
-- uniqueness by comparing m and OrdNat. The problem was that this
-- left a constraint m == OrdNat that leaked into the state.
foo : Set
foo = ∀ (n : Nat) m → R n → T m


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

open import Data.Unit.Core

open import SimpleHoTT using (refl;_≡_)

------------------------------------------------------------------------
-- Inspect on steroids (borrowed from standard library)

-- Inspect on steroids can be used when you want to pattern match on
-- the result r of some expression e, and you also need to "remember"
-- that r ≡ e.

data Reveal_is_ {a} {A : Set a} (x : Hidden A) (y : A) : Set a where
  ⟪_⟫ : (eq : reveal x ≡ y) → Reveal x is y

inspect : ∀ {a b} {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal (hide f x) is (f x)
inspect f x = ⟪ refl (f x) ⟫

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- Andreas, 2015-06-28
-- {-# OPTIONS -v tc.polarity:20  #-}

open import Common.Size

-- List should be monotone in both arguments
-- (even as phantom type).

data List (i : Size) (A : Set) : Set where
  [] : List i A

castL : ∀{i A} → List i A → List ∞ A
castL x = x

castLL : ∀{i A} → List i (List i A) → List ∞ (List ∞ A)
castLL x = x

-- Stream should be antitone in the first and monotone in the second argument
-- (even with field `tail' missing).

record Stream (i : Size) (A : Set) : Set where
  coinductive
  field
    head : A

castS : ∀{i A} → Stream ∞ A → Stream i A
castS x = x

castSS : ∀{i A} → Stream ∞ (Stream ∞ A) → Stream i (Stream i A)
castSS x = x


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

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

module Rings.Orders.Total.Cauchy {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) where

open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.AbsoluteValue order

cauchy : Sequence A → Set (m ⊔ o)
cauchy s = ∀ (ε : A) → (Ring.0R R < ε) → Sg ℕ (λ N → ∀ {m n : ℕ} → (N <N m) → (N <N n) → abs (Ring._-R_ R (index s m) (index s n)) < ε)


text:
module Class.Listable where

open import Class.Equality

open import Data.List
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All.Properties
open import Data.List.Relation.Unary.Unique.Propositional
open import Data.List.Membership.Propositional
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

record Listable (A : Set) : Set where
  field
    listing  : List A
    unique   : Unique listing
    complete : (a : A) → a ∈ listing

  Listable→Eq : Eq A
  Listable→Eq ._≟_ a b = helper (complete a) (complete b) unique
    where
      helper : ∀ {a b} {l : List A} → (a ∈ l) → (b ∈ l) → Unique l → Dec (a ≡ b)
      helper {a} {b} {l} h h' u with l | h | h' | u
      ... | ._ | here refl | here refl | _      = yes refl
      ... | ._ | here refl | there h   | h' ∷ _ = no λ where refl → All¬⇒¬Any h' h
      ... | ._ | there h   | here refl | h' ∷ _ = no λ where refl → All¬⇒¬Any h' h
      ... | ._ | there h   | there h'  | _  ∷ u = helper h h' u

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille