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

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

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

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

  Ind : A → Set₁
  Ind a =
    {P : A → Set}
    → ((x : A) (y : I x) → (∀ z → C x y z → P z) → P x)
    → P a

  ind : (a : A) (i : I a) → (∀ x → C a i x → Ind x) → Ind a
  ind a i p = λ c → c a i λ x q → p x q c

  El-Ind :
    {P : A → Set}
    → (c : (x : A) (y : I x) → (∀ z → C x y z → P z) → P x)
    → (a : A) (p : Ind a)
    → P a
  El-Ind c a p = p c

  C-Ind :
    {P : A → Set}
    → (c : (x : A) (y : I x) → (∀ z → C x y z → P z) → P x)
    → (a : A) (i : I a) (p : (∀ x → C a i x → Ind x))
    → El-Ind c a (ind a i p) ≡ c a i λ x q → El-Ind c x (p x q)
  C-Ind c a i p = refl