{- TODO: -}
module Cubical.Categories.Instances.Props where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure

open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.Categories.Category
open import Cubical.Categories.HLevels
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Instances.Thin
open import Cubical.Categories.Instances.Sets

private
  variable ℓ : Level

open Functor

PROP : ∀ ℓ → Category (ℓ-suc ℓ) ℓ
PROP ℓ = ThinCategory (hProp ℓ) (λ P Q → ⟨ P ⟩ → ⟨ Q ⟩)
  (λ {a} z → z)
  (λ {a} {b} {c} z z₁ z₂ → z₁ (z z₂))
  λ {b = Q} → isProp→ (Q .snd)

hasPropHomsPROP : hasPropHoms (PROP ℓ)
hasPropHomsPROP {y = Q} = isProp→ (Q .snd)

PROP→SET : Functor (PROP ℓ) (SET ℓ)
PROP→SET .F-ob P = ⟨ P ⟩ , (isProp→isSet (P .snd))
PROP→SET .F-hom = λ z → z
PROP→SET .F-id = refl
PROP→SET .F-seq = λ _ _ → refl