{-# OPTIONS --without-K --exact-split #-}

open import Agda.Builtin.Equality
open import Data.Product

-- Coinductive part of Proposition 6 of
-- "A topological reading of coinductive
--  predicates in Dependent Type Theory"

module Coinductive.Equivalences.Impredicative-Coind-types
  {A : Set}
  (I : A → Set)
  (C : (a : A) → I a → A → Set)
  where

  record CoInd (a : A) : Set₁ where
    field
      P : A → Set
      c : ∀ a i → P a → Σ A λ b → C a i b × P b
      p : P a

  El : (a : A) (i : I a) (p : CoInd a) → Σ A λ b → C a i b × CoInd b
  El a i record { P = P ; c = c ; p = p } with c a i p
  ... | b , q , r = b , q , record { P = P ; c = c ; p = r }

  coind :
    ∀ {P : A → Set}
    → (c : ∀ a i → P a → Σ A λ b → C a i b × P b)
    → (a : A) → P a → CoInd a
  coind {P} c a p = record { P = P ; c = c ; p = p }