reflexivity in Idris

reflexivity.idr

infixl 5 ⇔

data (⇔) : a -> b -> Type where
  Refl_ : x ⇔ x -- there is an identity, a function/path/morphism from a value of x of Type a to itself. /or to a value of an isomorphic type!/
  
  
fiveIsFive : 5 ⇔ 5
  -- this is a function of type "equality" parametrized by "5" and "5" and since it has a constructor and is thus populated (by Refl), the Type with this parameters is populated and it is a proof that five does, indeed, equal itself.
fiveIsFive = Refl_

  
twoPlusTwo : 2 + 2 ⇔ 4
twoPlusTwo = Refl_