Library Exercise_3_5_2_18


Require Import Utf8.


Exercise 3.5.2.18

Problem

Consider the olog
          F        has as first child        C
     ----------  --------------------->  ---------
    | a father |                        | a child |
     ----------  <---------------------  ---------
                       has as father
What path equivalence declarations would be appropriate for this olog? You can use f : F C and h: C F if you prefer.