{-# OPTIONS --cubical-compatible #-}
module Terra.Classes.Contractible where
open import Terra.Data.Level.Variables
open import Terra.Data.Equality
open import Terra.Data.Function.Postulates

record Contractible (A : Set ℓ) : Set ℓ where
  constructor contr
  field
    contract : (a b : A) -> a ≡ b

open Contractible {{...}} public

contr-pullback : {A : Set ℓ} {B : Set ℓ′} -> Contractible B -> Contractible (A -> B)
contr-pullback (contr contract) = contr (λ a b → extensionality λ x →  contract (a x) (b x))

instance
  contr-pullback-instance : {A : Set ℓ} {B : Set ℓ′} -> {{Contractible B}} -> Contractible (A -> B)
  contr-pullback-instance {{c}} = contr-pullback c