module Id.Intro where

open import Agda.Primitive
open import Lib
open import Fam as _

--------------------------
--- Introduction rules ---
--------------------------

record Id-Intro (C : Fam) : Set where
  field Id  : ∀ {A : C .Ty} (x : C .Tm A) (y : C .Tm A) → C .Ty
        idp : ∀ {A : C .Ty} {x : C .Tm A} → C .Tm (Id {A} x x)

  IdFrom : ∀ {A} → C .Tm A → Set
  IdFrom x = Σ _ λ y → C .Tm (Id x y)

  IdFrom-center : ∀ {A x} → IdFrom {A} x
  IdFrom-center = _ , idp

  IdTo : ∀ {A} → C .Tm A → Set
  IdTo x = Σ _ λ y → C .Tm (Id y x)

  IdTo-center : ∀ {A x} → IdTo {A} x
  IdTo-center = _ , idp

  isContr : C .Ty → Set _
  isContr A = Σ (C .Tm A) λ a → ∀ b → C .Tm (Id a b)

  allPaths : C .Ty → Set _
  allPaths A = ∀ a b → C .Tm (Id {A} a b)

  isProp : C .Ty → Set _
  isProp A = ∀ a b → isContr (Id {A} a b)

instance
  Id-Intro-⊤ : Id-Intro Fam-⊤
  Id-Intro-⊤ .Id-Intro.Id _ _ = tt
  Id-Intro-⊤ .Id-Intro.idp = tt