Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/no_internal_equality.md

Last active June 27, 2023 05:02
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save EduardoRFS/39e72727daba478baa904b36f73e6d6a to your computer and use it in GitHub Desktop.
Save EduardoRFS/39e72727daba478baa904b36f73e6d6a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
no_internal_equality.md 
!Unit ===
  %self(u). (P : %unroll Unit I_Unit unit I_unit -> Type) ->
    %unroll I_Unit unit I_unit P (%unroll unit I_unit) ->
    %unroll I_Unit unit I_unit P u;
!T_I_Unit ===
  %self(I_Unit). (unit : !T_unit) -> (I_unit : !T_I_unit) ->
    (P : %unroll Unit I_Unit unit I_unit -> Type) -> !Unit -> Type;
!T_unit ===
  %self(unit). (I_unit : !T_I_unit) -> !Unit;
!T_I_unit ===
  %self(I_unit). (P : %unroll Unit I_Unit unit I_unit -> Type) ->
    %unroll I_Unit unit I_unit P (%unroll unit I_unit) ->
    %unroll I_Unit unit I_unit P !unit;
!unit ===
  %fix(u). (P : %unroll Unit I_Unit unit I_unit -> Type) =>
    (x : P (%unroll unit I_unit)) => %unroll I_unit P x;

fix%Unit (I_Unit : !T_I_Unit) (unit : !T_unit) (I_unit : !T_I_unit) : Type = !Unit;
I_Unit : !T_I_Unit = %fix(I_Unit). unit => I_unit => P => %expand P;

fix%unit (I_unit : !T_I_unit) : !Unit = !unit;
I_unit : !T_I_unit = %fix(I_unit). P => %expand P;

Unit = %unroll Unit I_Unit unit I_unit;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment